The following shows Cora's results on a variety of benchmarks in the higher order union beta category of the termination problem database, limited to those benchmarks that do not contain abstraction. We have tested both termination and universal computability of various rewriting strategies.

Filename full termination innermost termination cbv termination computability innermost computability cbv computability
Applicative_AG01_innermost__#4.17 MAYBE 0.70 MAYBE 0.60 MAYBE 0.58 MAYBE 0.36 MAYBE 0.52 MAYBE 0.55
AotoYamada_05__027 YES 0.27 YES 0.26 YES 0.27 YES 0.28 YES 0.23 YES 0.27
Applicative_05__Ex9Maps YES 0.26 YES 0.27 YES 0.27 YES 0.31 YES 0.26 YES 0.25
Applicative_first_order_05__#3.55 MAYBE 1.94 MAYBE 2.04 MAYBE 2.06 MAYBE 0.62 MAYBE 1.82 MAYBE 1.92
Applicative_first_order_05__08 YES 0.98 YES 0.94 YES 0.98 YES 0.96 YES 0.86 YES 0.94
02Ackermann YES 0.28 YES 0.35 YES 0.31 YES 0.31 YES 0.25 YES 0.27
AotoYamada_05__007 YES 0.26 YES 0.27 YES 0.29 YES 0.26 YES 0.24 YES 0.23
fuhkop11frocos YES 0.52 YES 0.44 YES 0.45 MAYBE 0.29 YES 0.34 YES 0.36
Applicative_05__mapDivMinus YES 0.44 YES 0.45 YES 0.44 MAYBE 0.31 YES 0.36 YES 0.37
Applicative_05__Ex7_9 YES 0.90 YES 0.57 YES 0.60 MAYBE 0.44 YES 0.50 YES 0.53
AotoYamada_05__002 YES 0.25 YES 0.23 YES 0.25 YES 0.24 YES 0.21 YES 0.22
h36 TIMEOUT TIMEOUT TIMEOUT MAYBE 9.86 TIMEOUT TIMEOUT
lambda3 MAYBE 0.16 MAYBE 0.15 MAYBE 0.15 MAYBE 0.16 MAYBE 0.15 MAYBE 0.15
shuffle MAYBE 0.46 MAYBE 0.51 MAYBE 0.50 MAYBE 0.34 MAYBE 0.50 MAYBE 0.50
Applicative_first_order_05__#3.6 MAYBE 1.38 MAYBE 1.02 MAYBE 1.10 MAYBE 0.49 MAYBE 1.02 MAYBE 1.07
Applicative_05__Ex4MapList YES 0.27 YES 0.21 YES 0.21 YES 0.20 YES 0.20 YES 0.22
Applicative_05__TreeLevels MAYBE 0.65 MAYBE 0.54 MAYBE 0.56 MAYBE 0.48 MAYBE 0.47 MAYBE 0.45
AotoYamada_05__024 YES 0.20 YES 0.27 YES 0.19 YES 0.21 YES 0.19 YES 0.18
Applicative_first_order_05__#3.27 YES 0.41 YES 0.49 YES 0.45 YES 0.40 YES 0.41 YES 0.44
Applicative_first_order_05__hydra YES 0.40 YES 0.43 YES 0.45 YES 0.40 YES 0.36 YES 0.38
Applicative_05__Ex6_11 MAYBE 0.24 MAYBE 0.21 MAYBE 0.19 MAYBE 0.18 MAYBE 0.15 MAYBE 0.15
AotoYamada_05__005 YES 0.23 YES 0.21 YES 0.20 YES 0.23 YES 0.19 YES 0.20
AotoYamada_05__012 YES 0.31 YES 0.29 YES 0.28 YES 0.29 YES 0.27 YES 0.25
Applicative_05__ReverseLastInit YES 0.29 YES 0.32 YES 0.32 YES 0.33 YES 0.26 YES 0.27
Applicative_first_order_05__12 TIMEOUT YES 1.17 YES 1.49 MAYBE 0.73 YES 1.07 YES 1.11
Applicative_AG01_innermost__#4.26 MAYBE 0.96 MAYBE 0.70 MAYBE 0.68 MAYBE 0.42 MAYBE 0.64 MAYBE 0.60
Applicative_05__Ex3Lists YES 0.59 YES 0.62 YES 0.56 YES 0.58 YES 0.55 YES 0.55
Applicative_AG01_innermost__#4.3 MAYBE 0.49 MAYBE 0.47 MAYBE 0.41 MAYBE 0.29 MAYBE 0.43 MAYBE 0.41
app YES 0.14 YES 0.14 YES 0.21 YES 0.16 YES 0.14 YES 0.16
Applicative_05__Ex7OrdinalRec MAYBE 0.20 MAYBE 0.22 MAYBE 0.23 MAYBE 0.16 MAYBE 0.14 MAYBE 0.17
AotoYamada_05__013 YES 0.40 YES 0.33 YES 0.31 YES 0.33 YES 0.32 YES 0.35
Applicative_05__TreeSize MAYBE 0.58 MAYBE 0.47 MAYBE 0.43 MAYBE 0.41 MAYBE 0.41 MAYBE 0.43
map YES 0.19 YES 0.20 YES 0.21 YES 0.21 YES 0.18 YES 0.19
AotoYamada_05__011 YES 0.27 YES 0.27 YES 0.27 YES 0.25 YES 0.27 YES 0.25
Applicative_first_order_05__11 YES 2.76 YES 2.73 YES 2.61 YES 2.68 YES 2.53 YES 2.58
Applicative_first_order_05__#3.57 MAYBE 1.32 MAYBE 1.22 MAYBE 1.25 MAYBE 0.60 MAYBE 1.19 MAYBE 1.11
counterex2 MAYBE 0.19 MAYBE 0.21 MAYBE 0.20 MAYBE 0.18 MAYBE 0.16 MAYBE 0.17
AotoYamada_05__Ex1SimplyTyped YES 0.26 YES 0.25 YES 0.25 YES 0.24 YES 0.23 YES 0.23
Applicative_first_order_05__#3.48 MAYBE 1.03 MAYBE 1.04 MAYBE 0.99 MAYBE 0.56 MAYBE 0.96 MAYBE 0.92
Applicative_first_order_05__#3.10 MAYBE 2.53 MAYBE 3.02 MAYBE 2.72 MAYBE 0.70 MAYBE 2.78 MAYBE 2.88
Applicative_05__TreeHeight MAYBE 0.64 MAYBE 0.44 MAYBE 0.43 MAYBE 0.39 MAYBE 0.42 MAYBE 0.44
Applicative_first_order_05__#3.18 TIMEOUT YES 0.79 YES 0.76 MAYBE 0.55 YES 0.76 YES 0.76
AotoYamada_05__Ex5TermProof YES 0.35 YES 0.31 YES 0.29 YES 0.33 YES 0.30 YES 0.32
findzero MAYBE 0.24 MAYBE 0.24 MAYBE 0.24 MAYBE 0.18 MAYBE 0.16 MAYBE 0.17
Applicative_first_order_05__#3.52 YES 0.37 YES 0.41 YES 0.37 YES 0.37 YES 0.39 YES 0.34
Applicative_05__Ex2_6_1Composition YES 0.15 YES 0.16 YES 0.15 YES 0.15 YES 0.15 YES 0.16
eval MAYBE 0.22 MAYBE 0.21 MAYBE 0.19 MAYBE 0.20 MAYBE 0.16 MAYBE 0.14
Applicative_first_order_05__#3.8 MAYBE 0.74 MAYBE 0.70 MAYBE 0.64 MAYBE 0.37 MAYBE 0.66 MAYBE 0.61
AotoYamada_05__009 YES 0.27 YES 0.25 YES 0.26 YES 0.27 YES 0.26 YES 0.25
Applicative_AG01_innermost__#4.36 MAYBE 1.74 MAYBE 2.34 MAYBE 2.12 MAYBE 0.57 MAYBE 2.08 MAYBE 2.08
Applicative_first_order_05__02 YES 0.35 YES 0.31 YES 0.29 YES 0.32 YES 0.35 YES 0.30
AotoYamada_05__025 YES 0.15 YES 0.15 YES 0.15 YES 0.23 YES 0.19 YES 0.15
kop12thesis_ex7.45_1 MAYBE 0.68 MAYBE 0.99 MAYBE 0.94 MAYBE 0.41 MAYBE 0.63 MAYBE 0.66
Applicative_05__termMonTypes MAYBE 0.24 MAYBE 0.34 MAYBE 0.28 MAYBE 0.22 MAYBE 0.26 MAYBE 0.27
Applicative_first_order_05__21 MAYBE 0.70 MAYBE 0.53 MAYBE 0.53 MAYBE 0.46 MAYBE 0.50 MAYBE 0.53
AotoYamada_05__017 YES 0.17 YES 0.15 YES 0.17 YES 0.18 YES 0.16 YES 0.19
apply YES 0.20 YES 0.20 YES 0.21 YES 0.22 YES 0.19 YES 0.29
uncurry YES 0.16 YES 0.23 YES 0.15 YES 0.20 YES 0.19 YES 0.18
Applicative_05__TakeDropWhile YES 0.28 YES 0.27 YES 0.25 YES 0.27 YES 0.24 YES 0.26
Applicative_first_order_05__#3.16 YES 0.49 YES 0.55 YES 0.45 YES 0.49 YES 0.45 YES 0.45
fuhs11frocos_a MAYBE 0.30 MAYBE 0.34 MAYBE 0.30 MAYBE 0.21 MAYBE 0.28 MAYBE 0.28
Applicative_05__TreeMap MAYBE 0.34 MAYBE 0.39 MAYBE 0.31 MAYBE 0.28 MAYBE 0.30 MAYBE 0.31
Applicative_05__Ex5Folding YES 0.31 YES 0.32 YES 0.31 YES 0.36 YES 0.31 YES 0.32
lambda2 MAYBE 0.39 MAYBE 0.46 MAYBE 0.43 MAYBE 0.28 MAYBE 0.58 MAYBE 0.53
Applicative_AG01_innermost__#4.7 MAYBE 0.61 MAYBE 0.46 MAYBE 0.42 MAYBE 0.28 MAYBE 0.46 MAYBE 0.52
Applicative_05__Ex7Sorting YES 0.44 YES 0.49 YES 0.44 YES 0.42 YES 0.49 YES 0.55
Applicative_first_order_05__#3.13 MAYBE 9.37 MAYBE 3.09 MAYBE 2.89 MAYBE 0.57 MAYBE 2.95 MAYBE 3.23
04arrow YES 0.37 YES 0.38 YES 0.30 MAYBE 0.27 YES 0.34 YES 0.34
plode YES 0.26 YES 0.26 YES 0.22 YES 0.27 YES 0.27 YES 0.24
Applicative_05__Ex6Folding YES 0.21 YES 0.23 YES 0.20 YES 0.22 YES 0.21 YES 0.24
AotoYamada_05__016 YES 0.31 YES 0.34 YES 0.32 YES 0.34 YES 0.29 YES 0.35
AotoYamada_05__006 YES 0.22 YES 0.21 YES 0.29 YES 0.24 YES 0.22 YES 0.21
Applicative_first_order_05__29 YES 0.50 YES 0.53 YES 0.49 YES 0.48 YES 0.48 YES 0.52
Applicative_AG01_innermost__#4.2 MAYBE 0.65 MAYBE 0.53 MAYBE 0.48 MAYBE 0.32 MAYBE 0.53 MAYBE 0.69
AotoYamada_05__001 MAYBE 0.25 MAYBE 0.25 MAYBE 0.28 MAYBE 0.20 MAYBE 0.28 MAYBE 0.25
AotoYamada_05__022 YES 0.24 YES 0.24 YES 0.26 YES 0.26 YES 0.24 YES 0.29
lambda5 MAYBE 0.16 MAYBE 0.22 MAYBE 0.19 MAYBE 0.15 MAYBE 0.14 MAYBE 0.18
Applicative_first_order_05__#3.36 YES 0.88 YES 0.72 YES 0.66 MAYBE 0.46 YES 0.70 YES 0.87
AotoYamada_05__010 YES 0.36 YES 0.35 YES 0.36 YES 0.37 YES 0.35 YES 0.36
AotoYamada_05__004 YES 0.31 YES 0.28 YES 0.26 YES 0.23 YES 0.29 YES 0.27
AotoYamada_05__014 YES 0.38 YES 0.34 YES 0.36 YES 0.40 YES 0.36 YES 0.34
Applicative_first_order_05__perfect YES 0.44 YES 0.41 YES 0.40 YES 0.46 YES 0.44 YES 0.42
rec YES 0.22 YES 0.20 YES 0.19 YES 0.23 YES 0.19 YES 0.26
AotoYamada_05__003 MAYBE 0.26 MAYBE 0.31 MAYBE 0.33 MAYBE 0.22 MAYBE 0.26 MAYBE 0.27
Applicative_05__TypeEx5 MAYBE 0.25 MAYBE 0.27 MAYBE 0.30 MAYBE 0.28 MAYBE 0.27 MAYBE 0.28
AotoYamada_05__015 YES 0.31 YES 0.28 YES 0.28 YES 0.27 YES 0.26 YES 0.29
Applicative_first_order_05__33 MAYBE 1.38 MAYBE 1.11 MAYBE 1.09 MAYBE 0.68 MAYBE 1.10 MAYBE 1.19
Applicative_AG01_innermost__#4.22 YES 0.36 YES 0.40 YES 0.40 YES 0.37 YES 0.38 YES 0.38
Applicative_first_order_05__17 YES 0.57 YES 0.55 YES 0.54 YES 0.54 YES 0.55 YES 0.53
Applicative_AG01_innermost__#4.13 MAYBE 0.59 MAYBE 0.47 MAYBE 0.40 MAYBE 0.27 MAYBE 0.42 MAYBE 0.49
Applicative_first_order_05__30 TIMEOUT YES 1.19 YES 1.09 MAYBE 0.64 YES 1.06 YES 1.22
hrsdif2 MAYBE 0.29 MAYBE 0.26 MAYBE 0.23 MAYBE 0.22 MAYBE 0.20 MAYBE 0.31
Applicative_first_order_05__#3.38 MAYBE 1.03 MAYBE 0.94 MAYBE 0.86 MAYBE 0.40 MAYBE 0.88 MAYBE 0.99
Applicative_first_order_05__13 MAYBE 1.40 MAYBE 1.63 MAYBE 1.56 MAYBE 1.12 MAYBE 1.62 MAYBE 1.72
Applicative_first_order_05__#3.2 MAYBE 0.76 MAYBE 0.57 MAYBE 0.53 MAYBE 0.38 MAYBE 0.49 MAYBE 0.61
05height YES 0.25 YES 0.25 YES 0.22 YES 0.24 YES 0.24 YES 0.24
Applicative_AG01_innermost__#4.8 MAYBE 0.56 MAYBE 0.54 MAYBE 0.48 MAYBE 0.37 MAYBE 0.50 MAYBE 0.50
03minus YES 0.20 YES 0.19 YES 0.19 YES 0.23 YES 0.22 YES 0.19
Applicative_AG01_innermost__#4.15 MAYBE 0.86 MAYBE 0.65 MAYBE 0.58 MAYBE 0.45 MAYBE 0.62 MAYBE 0.70
Applicative_first_order_05__#3.32 YES 0.33 YES 0.32 YES 0.28 YES 0.29 YES 0.29 YES 0.41
AotoYamada_05__023 YES 0.24 YES 0.25 YES 0.20 YES 0.23 YES 0.21 YES 0.23
Applicative_first_order_05__01 YES 0.35 YES 0.35 YES 0.29 YES 0.34 YES 0.29 YES 0.35
06plusmult YES 0.60 YES 0.64 YES 0.59 YES 0.61 YES 0.59 YES 0.71
fuhkop12rta1 MAYBE 0.46 MAYBE 0.54 MAYBE 0.47 MAYBE 0.32 MAYBE 0.51 MAYBE 0.57
Applicative_05__Hamming MAYBE 2.14 MAYBE 1.38 MAYBE 1.32 MAYBE 1.14 MAYBE 1.35 MAYBE 1.86
Applicative_first_order_05__#3.25 MAYBE 0.56 MAYBE 0.55 MAYBE 0.50 MAYBE 0.29 MAYBE 0.50 MAYBE 0.73
Applicative_first_order_05__minsort MAYBE 1.41 MAYBE 1.40 MAYBE 1.29 MAYBE 0.78 MAYBE 1.23 MAYBE 1.45
Applicative_AG01_innermost__#4.10 MAYBE 0.55 MAYBE 0.43 MAYBE 0.44 MAYBE 0.33 MAYBE 0.43 MAYBE 0.41
Applicative_first_order_05__motivation MAYBE 0.69 MAYBE 0.80 MAYBE 0.71 MAYBE 0.48 MAYBE 0.75 MAYBE 0.71
merge YES 0.49 YES 0.41 YES 0.45 MAYBE 0.37 YES 0.36 YES 0.40
Applicative_05__BTreeMember YES 0.33 YES 0.34 YES 0.34 YES 0.35 YES 0.30 YES 0.34
Applicative_first_order_05__perfect2 TIMEOUT YES 0.88 YES 0.89 MAYBE 0.72 YES 0.83 YES 0.81
AotoYamada_05__026 YES 0.23 YES 0.23 YES 0.20 YES 0.23 YES 0.20 YES 0.19
Applicative_AG01_innermost__#4.5 MAYBE 0.33 MAYBE 0.41 MAYBE 0.37 MAYBE 0.31 MAYBE 0.39 MAYBE 0.41
Applicative_AG01_innermost__#4.19 MAYBE 0.69 MAYBE 0.72 MAYBE 0.75 MAYBE 0.36 MAYBE 0.65 MAYBE 0.71
kop12thesis_ex7.45_2 MAYBE 0.66 MAYBE 0.91 MAYBE 1.01 MAYBE 0.36 MAYBE 0.65 MAYBE 0.56
if YES 0.31 YES 0.42 YES 0.41 MAYBE 0.21 YES 0.30 YES 0.32
average MAYBE 0.21 MAYBE 0.21 MAYBE 0.24 MAYBE 0.14 MAYBE 0.17 MAYBE 0.17
filter YES 0.29 YES 0.27 YES 0.25 YES 0.25 YES 0.26 YES 0.24
Applicative_AG01_innermost__#4.34 YES 0.95 YES 0.68 YES 0.69 MAYBE 0.44 YES 0.64 YES 0.71
curry1 YES 0.19 YES 0.19 YES 0.16 YES 0.16 YES 0.15 YES 0.15
Applicative_05__Ex6Recursor YES 0.20 YES 0.21 YES 0.18 YES 0.18 YES 0.17 YES 0.19
Applicative_first_order_05__#3.40 TIMEOUT TIMEOUT TIMEOUT MAYBE 0.55 TIMEOUT TIMEOUT
Applicative_AG01_innermost__#4.24 YES 0.46 YES 0.46 YES 0.49 YES 0.42 YES 0.44 YES 0.43
lambda1 MAYBE 0.18 MAYBE 0.19 MAYBE 0.17 MAYBE 0.13 MAYBE 0.16 MAYBE 0.15
noabs MAYBE 0.17 MAYBE 0.17 MAYBE 0.20 MAYBE 0.14 MAYBE 0.15 MAYBE 0.15
Applicative_05__Ex5Sorting YES 0.50 YES 0.41 YES 0.46 YES 0.42 YES 0.43 YES 0.40
Applicative_first_order_05__06 YES 0.33 YES 0.33 YES 0.35 YES 0.30 YES 0.32 YES 0.35
Applicative_first_order_05__18 YES 0.40 YES 0.42 YES 0.39 YES 0.37 YES 0.40 YES 0.41
Applicative_05__Ex2_8_1ConstSubstFix MAYBE 0.25 MAYBE 0.27 MAYBE 0.26 MAYBE 0.19 MAYBE 0.30 MAYBE 0.27
Applicative_05__mapDivMinusHard MAYBE 0.53 MAYBE 0.46 MAYBE 0.47 MAYBE 0.30 MAYBE 0.45 MAYBE 0.42
Applicative_AG01_innermost__#4.28 MAYBE 0.60 MAYBE 0.49 MAYBE 0.47 MAYBE 0.29 MAYBE 0.46 MAYBE 0.47
Applicative_first_order_05__#3.45 YES 0.73 YES 0.53 YES 0.48 MAYBE 0.33 YES 0.51 YES 0.48
Applicative_05__TreeFlatten MAYBE 0.51 MAYBE 0.46 MAYBE 0.44 MAYBE 0.37 MAYBE 0.42 MAYBE 0.43
AotoYamada_05__028 YES 0.21 YES 0.21 YES 0.26 YES 0.20 YES 0.20 YES 0.26
foobar MAYBE 0.21 MAYBE 0.17 MAYBE 0.16 MAYBE 0.15 MAYBE 0.15 MAYBE 0.15
AotoYamada_05__019 YES 0.14 YES 0.18 YES 0.16 YES 0.18 YES 0.17 YES 0.16
Applicative_first_order_05__#3.22 MAYBE 1.01 MAYBE 0.92 MAYBE 0.92 MAYBE 0.48 MAYBE 0.85 MAYBE 0.86
AotoYamada_05__020 YES 0.26 YES 0.28 YES 0.26 YES 0.28 YES 0.26 YES 0.25
AotoYamada_05__021 YES 0.37 YES 0.37 YES 0.36 YES 0.33 YES 0.38 YES 0.32
Total YES 75 79 79 66 79 79
Total NO 0 0 0 0 0 0
Total MAYBE 59 59 59 74 59 59
Total TIMEOUT 6 2 2 0 2 2
Average Runtime 0.38 0.40 0.39 0.34 0.37 0.39