The following shows Cora's results on the first-order integer TRSs in the TPDB, using a one-minute timeout.

For comparison, the results from AProVE's innermost evaluation of integer TRSs are included (but note that this is a weaker property than full termination). The evaluation details can be found at the evaluation page for the 2023 termination competition.

Filename Termination Computability AProVE
01 YES 0.35 YES 0.38 YES
02 YES 0.33 YES 0.42 YES
03 YES 0.42 YES 0.49 YES
04 YES 0.18 YES 0.20 YES
05 YES 0.17 YES 0.18 YES
06 YES 0.15 YES 0.17 YES
07 YES 0.14 YES 0.18 YES
08 YES 0.41 YES 0.41 YES
09 YES 0.53 YES 0.53 YES
10 YES 0.68 YES 0.69 YES
11 YES 0.49 YES 0.50 YES
13 YES 0.49 YES 0.50 YES
15 YES 0.95 YES 0.95 YES
16 YES 1.13 YES 1.15 YES
17 YES 1.90 YES 1.77 YES
18 YES 1.81 YES 1.79 YES
19 YES 2.00 YES 1.99 YES
20 YES 0.41 YES 0.41 YES
21 YES 0.50 YES 0.53 YES
22 YES 2.10 YES 2.00 YES
23 YES 3.45 YES 3.17 YES
24 YES 0.77 YES 0.73 YES
a.01 YES 3.58 YES 3.63 YES
A01 MAYBE 1.62 MAYBE 1.37 YES
a.02 YES 1.07 YES 1.04 TIMEOUT
A02 MAYBE 0.24 MAYBE 0.17 YES
a.03 YES 30.54 YES 31.92 YES
A03 MAYBE 1.72 MAYBE 1.38 YES
a.04 YES 0.40 YES 0.42 YES
A04 MAYBE 1.83 MAYBE 1.38 YES
a.05 YES 0.36 YES 0.36 YES
A05 YES 0.23 YES 0.25 YES
a.06 YES 0.45 YES 0.41 YES
A06 MAYBE 0.31 MAYBE 0.24 YES
a.07 YES 0.46 YES 0.50 YES
A07 MAYBE 4.09 MAYBE 3.72 YES
a.08 YES 0.33 YES 0.34 YES
A08 MAYBE 0.32 MAYBE 0.24 TIMEOUT
a.09 YES 0.45 YES 0.45 YES
A09 MAYBE 1.06 MAYBE 0.68 YES
a.10 YES 1.00 YES 1.02 YES
A10 MAYBE 1.07 MAYBE 0.67 YES
a.11 MAYBE 13.71 MAYBE 11.80 YES
A11 MAYBE 0.23 MAYBE 0.17 YES
A12 MAYBE 0.23 MAYBE 0.16 YES
A13 MAYBE 4.67 MAYBE 3.49 YES
A14 MAYBE 2.85 MAYBE 2.30 YES
A15 MAYBE 1.38 MAYBE 1.29 TIMEOUT
A16 YES 0.29 YES 0.29 TIMEOUT
A17 MAYBE 2.46 MAYBE 1.80 TIMEOUT
abstractions YES 0.86 YES 0.80 YES
ackTen MAYBE 1.18 MAYBE 0.57 TIMEOUT
c.01 YES 2.89 YES 2.80 YES
c.02 YES 2.84 YES 2.81 YES
c.03 YES 1.14 YES 1.10 YES
c.04 YES 0.65 YES 0.64 YES
c.05 YES 1.82 YES 1.81 YES
choice MAYBE 1.53 MAYBE 0.67 YES
collatz MAYBE 1.36 MAYBE 0.95 TIMEOUT
complete1 YES 0.46 YES 0.34 YES
complete2 MAYBE 0.53 MAYBE 0.23 YES
complete3 YES 1.98 YES 1.77 YES
complete4 YES 0.80 YES 0.77 YES
conv YES 0.52 YES 0.51 YES
countdown MAYBE 0.22 MAYBE 0.17 YES
countUpExp MAYBE 1.85 MAYBE 1.36 YES
countup MAYBE 0.21 MAYBE 0.18 YES
countUpNo YES 0.15 YES 0.13 YES
csharp1 YES 0.22 YES 0.20 YES
csharp2 YES 0.23 YES 0.22 YES
csharp3 YES 0.22 YES 0.21 YES
div YES 0.49 YES 0.41 YES
divMinus MAYBE 1.72 MAYBE 1.26 YES
eratosthenes MAYBE 2.79 MAYBE 1.61 YES
eratosthenes_small MAYBE 1.62 MAYBE 0.93 YES
Ex04 MAYBE 0.45 MAYBE 0.29 TIMEOUT
Ex09 MAYBE 0.42 MAYBE 0.34 YES
extra1 MAYBE 0.21 MAYBE 0.18 YES
extra2 MAYBE 0.28 MAYBE 0.23 YES
f91 MAYBE 0.45 MAYBE 0.29 TIMEOUT
gcd_minmax YES 1.00 YES 1.00 YES
incList YES 0.20 YES 0.21 YES
increase1 YES 0.37 YES 0.36 YES
increase2 YES 0.79 YES 0.76 YES
increase3 YES 1.27 YES 1.29 YES
increase4 YES 0.36 YES 0.31 YES
indirect MAYBE 2.70 MAYBE 2.49 YES
log_RTA08 YES 0.43 YES 0.37 YES
log_RTA09 MAYBE 1.77 MAYBE 1.20 YES
maxsort MAYBE 0.67 MAYBE 0.52 TIMEOUT
minsort MAYBE 0.99 MAYBE 0.59 YES
mult YES 0.47 YES 0.40 YES
poly1 MAYBE 0.87 MAYBE 0.29 TIMEOUT
poly2 MAYBE 0.47 MAYBE 0.28 TIMEOUT
poly3 MAYBE 3.53 MAYBE 1.11 TIMEOUT
poly4 YES 2.39 YES 2.40 YES
powFast MAYBE 7.24 MAYBE 6.12 YES
pow MAYBE 1.87 MAYBE 1.38 YES
practical1 YES 1.93 YES 1.85 YES
practical2 MAYBE 27.13 MAYBE 22.31 TIMEOUT
practical3 TIMEOUT MAYBE 51.07 TIMEOUT
quicksort MAYBE 1.20 MAYBE 0.84 YES
random_full YES 0.77 YES 0.69 YES
random_full_no_wrap YES 0.72 YES 0.73 YES
randomFullUpDown MAYBE 1.20 MAYBE 0.79 YES
random YES 0.42 YES 0.42 YES
random_no_wrap YES 0.41 YES 0.41 YES
round MAYBE 0.47 MAYBE 0.35 YES
sqrt_new MAYBE 1.90 MAYBE 1.37 YES
sqrt_patrs YES 0.46 YES 0.45 YES
sum MAYBE 1.70 MAYBE 1.34 YES
sumto YES 0.37 YES 0.40 YES
sumto_no_if YES 0.37 YES 0.38 YES
terminate YES 1.21 MAYBE 0.38 YES
thousand MAYBE 0.21 MAYBE 0.21 YES
unsatCond1 YES 0.15 YES 0.15 YES
unsatCond2 YES 0.18 YES 0.17 YES
Total YES 69 68 102
Total NO 0 0 0
Total MAYBE 47 49 0
Total TIMEOUT 1 0 15
Average Runtime 1.27 1.28