The following shows Cora's results on a number of benchmarks collected by the authors. This tests for termination and universal computability respectively.

Moreover, in some cases public / private symbols are indicated. Then, for termination we consider all start terms, and for computability we consider only starting terms where all symbols are public. (If the public/private status of a symbol is not indicated, then it is public.)

Filename Termination Computability
complist YES 0.17 YES 0.18
factcps YES 0.48 YES 0.52
gcd YES 0.90 YES 1.00
lambda MAYBE 0.11 MAYBE 0.11
nondetnonterm MAYBE 0.35 MAYBE 0.18
nonterminate MAYBE 0.51 MAYBE 0.55
private MAYBE 0.51 YES 0.47
random MAYBE 0.39 MAYBE 0.16
theorval YES 0.81 YES 0.79
add YES 0.19 YES 0.19
ex_01_take YES 0.23 YES 0.23
ex_02_iterate MAYBE 0.23 MAYBE 0.17
ex_05_take YES 0.18 YES 0.18
ex_06_factfold YES 0.42 YES 0.50
ex_08_readint YES 0.14 YES 0.19
ex_09_rec YES 0.34 YES 0.30
exp YES 0.39 YES 0.46
factunit YES 0.34 YES 0.37
map YES 0.21 YES 0.24
muldifference YES 0.22 MAYBE 0.17
nonterminate MAYBE 0.37 MAYBE 0.51
sum YES 0.29 YES 0.33
ack YES 0.26 YES 0.33
basic YES 0.16 YES 0.20
eval YES 0.34 YES 0.38
impossible MAYBE 0.20 MAYBE 0.19
mutually_recursive_value_criterion YES 2.66 YES 2.57
sum2 YES 0.27 YES 0.28
Total YES 20 20
Total NO 0 0
Total MAYBE 8 8
Total TIMEOUT 0 0
Average Runtime 0.45 0.48