The following shows Cora's results on a variety of benchmarks which we have crafted ourselves, both testing for termination and universal computability of various rewriting strategies.

Filename full termination innermost termination cbv termination computability innermost computability cbv computability
add YES 0.19 YES 0.19 YES 0.18 YES 0.20 YES 0.21 YES 0.21
ex_01_take YES 0.19 YES 0.19 YES 0.19 YES 0.21 YES 0.21 YES 0.21
ex_02_iterate MAYBE 0.25 MAYBE 0.28 MAYBE 0.28 MAYBE 0.21 MAYBE 0.25 MAYBE 0.27
ex_05_take YES 0.20 YES 0.19 YES 0.21 YES 0.20 YES 0.19 YES 0.21
ex_06_factfold YES 0.40 YES 0.40 YES 0.44 YES 0.38 YES 0.44 YES 0.46
ex_08_readint YES 0.16 YES 0.16 YES 0.18 YES 0.16 YES 0.17 YES 0.18
ex_09_rec YES 0.27 YES 0.28 YES 0.38 YES 0.30 YES 0.36 YES 0.44
exp YES 0.44 YES 0.41 YES 0.42 YES 0.43 YES 0.44 YES 0.48
factunit YES 0.38 YES 0.32 YES 0.31 YES 0.32 YES 0.37 YES 0.39
map YES 0.23 YES 0.22 YES 0.23 YES 0.22 YES 0.25 YES 0.26
muldifference YES 0.25 YES 0.26 YES 0.27 MAYBE 0.17 YES 0.25 YES 0.30
nonterminate MAYBE 0.54 MAYBE 0.61 MAYBE 0.66 MAYBE 0.42 MAYBE 0.67 MAYBE 0.71
sum YES 0.28 YES 0.29 YES 0.32 YES 0.29 YES 0.33 YES 0.32
complist YES 0.19 YES 0.19 YES 0.18 YES 0.20 YES 0.19 YES 0.21
factcps YES 0.47 YES 0.51 YES 0.47 YES 0.49 YES 0.56 YES 0.53
fsum MAYBE 0.74 MAYBE 0.87 MAYBE 0.89 MAYBE 0.57 MAYBE 0.89 MAYBE 0.94
gcd YES 1.04 YES 0.85 YES 1.09 YES 1.08 YES 0.93 YES 1.14
lambda MAYBE 0.16 MAYBE 0.18 MAYBE 0.16 MAYBE 0.16 MAYBE 0.16 MAYBE 0.15
nondetnonterm MAYBE 0.39 MAYBE 0.65 YES 0.16 MAYBE 0.25 MAYBE 0.71 YES 0.19
private YES 0.44 YES 0.44 YES 0.46 YES 0.49 YES 0.46 YES 0.61
random MAYBE 0.42 MAYBE 0.63 YES 0.18 MAYBE 0.18 MAYBE 0.74 YES 0.27
theorval YES 0.64 YES 0.36 YES 0.38 YES 0.79 YES 0.43 YES 0.43
nested_loop MAYBE 6.46 YES 2.78 YES 2.60 MAYBE 6.05 YES 3.24 YES 2.96
count_up MAYBE 1.65 YES 0.53 YES 0.54 MAYBE 1.56 YES 0.54 YES 0.59
skipfold2 YES 0.57 YES 0.52 YES 0.62 MAYBE 0.30 YES 0.60 YES 0.70
skipfold YES 0.64 YES 0.55 YES 0.67 MAYBE 0.39 YES 0.64 YES 0.81
nested_loop_invariant MAYBE 6.49 MAYBE 2.67 MAYBE 2.57 MAYBE 6.56 MAYBE 3.06 MAYBE 3.03
ack YES 0.27 YES 0.33 YES 0.26 YES 0.27 YES 0.30 YES 0.28
basic YES 0.20 YES 0.20 YES 0.17 YES 0.22 YES 0.22 YES 0.26
eval YES 0.41 YES 0.38 YES 0.35 YES 0.38 YES 0.41 YES 0.43
extended YES 0.21 YES 0.24 YES 0.26 MAYBE 0.24 YES 0.25 YES 0.31
impossible MAYBE 0.20 MAYBE 0.30 MAYBE 0.49 MAYBE 0.22 MAYBE 0.30 MAYBE 0.55
lopstrs24 MAYBE 0.90 MAYBE 0.89 MAYBE 0.86 MAYBE 0.53 MAYBE 0.96 MAYBE 0.90
mutually_recursive_value_criterion YES 2.28 YES 0.46 YES 0.47 YES 2.51 YES 0.49 YES 0.49
nohorpo MAYBE 0.36 MAYBE 0.55 MAYBE 1.03 MAYBE 0.22 MAYBE 0.65 MAYBE 1.06
orientation YES 0.77 YES 0.43 YES 0.51 MAYBE 0.74 YES 0.45 YES 0.47
sorted YES 0.18 YES 0.18 YES 0.18 YES 0.18 YES 0.18 YES 0.21
sum2 YES 0.28 YES 0.26 YES 0.27 YES 0.37 YES 0.30 YES 0.30
Total YES 26 28 30 21 28 30
Total NO 0 0 0 0 0 0
Total MAYBE 12 10 8 17 10 8
Total TIMEOUT 0 0 0 0 0 0
Average Runtime 0.44 0.43 0.43 0.46 0.47 0.48