The power of various setups on a specific subset of the Termination Problem Database

This group of experiments considers WANDA's power both without restrictions, and various techniques in isolation. Experiments were done on a subset of the TPDB 2018: the benchmarks in the directories Uncurried_Applicative_11/ and Hamana_Kikuchi_18/ were removed. Both of these directories contain many benchmarks that are essentially first-order systems, with just a few very simple higher-order rules. The benchmarks are presented in the order: Mixed_HO_10/, Kop_11/, Mixed_HO_12/, Kop_13/, Hamana_17/, Hamana_17/Blanqui_15/.

Filename full rr horpo poly dp static dynamic nofo nosimp
applicative MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE
apply YES 0.05 MAYBE MAYBE MAYBE YES 0.01 YES 0.01 YES 0.01 YES 0.04 YES 0.06
app YES 0.00 YES 0.00 YES 0.00 YES 0.00 YES 0.00 YES 0.00 YES 0.00 YES 0.00 YES 0.01
counterex1 NO 0.00 MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE NO 0.00 NO 0.00
counterex2 MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE
curry1 YES 0.00 YES 0.00 YES 0.01 YES 0.00 YES 0.00 YES 0.54 YES 0.00 YES 0.00 YES 0.00
curry YES 0.01 YES 0.01 YES 0.02 YES 0.01 YES 0.00 YES 0.00 YES 0.01 YES 0.01 YES 0.01
deriv TIMEOUT TIMEOUT MAYBE TIMEOUT TIMEOUT MAYBE TIMEOUT TIMEOUT TIMEOUT
eval YES 0.69 MAYBE MAYBE MAYBE YES 0.81 MAYBE YES 0.54 YES 0.09 YES 1.18
extrec YES 0.14 YES 0.16 YES 0.09 MAYBE YES 0.64 YES 0.52 YES 1.05 YES 0.15 YES 0.21
filter YES 0.03 YES 0.03 YES 0.30 YES 0.03 YES 0.63 YES 0.70 YES 0.52 YES 0.03 YES 0.04
findzero YES 1.08 MAYBE MAYBE MAYBE YES 1.13 MAYBE YES 0.79 YES 0.72 YES 1.85
foldl YES 0.27 YES 0.26 YES 0.10 MAYBE YES 0.21 YES 0.01 YES 0.20 YES 0.28 YES 0.33
foobar MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE
from YES 1.17 MAYBE MAYBE MAYBE YES 0.97 YES 1.00 YES 1.75 YES 0.43 YES 1.39
hrsdif1 NO 0.00 MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE NO 0.00 NO 0.00
hrsdif2 MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE
if YES 0.73 MAYBE MAYBE MAYBE YES 0.73 YES 0.61 YES 0.83 YES 0.20 YES 1.45
inlamb YES 0.00 YES 0.00 YES 0.01 YES 0.02 YES 0.00 YES 0.00 YES 0.00 YES 0.00 YES 0.00
iterative YES 1.02 YES 1.03 YES 0.23 MAYBE YES 0.60 MAYBE YES 0.50 YES 1.09 YES 1.29
lambda1 NO 0.00 MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE NO 0.00 NO 0.00
lambda2 NO 1.82 MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE NO 3.00
lambda3 YES 0.02 MAYBE MAYBE MAYBE YES 0.00 MAYBE YES 0.00 YES 0.02 YES 0.02
length YES 0.11 YES 0.10 YES 0.12 MAYBE YES 0.01 YES 0.01 YES 0.05 YES 0.11 YES 0.14
loopy YES 0.02 YES 0.02 YES 0.04 YES 0.02 YES 0.01 YES 0.00 YES 0.01 YES 0.02 YES 0.03
map YES 0.02 YES 0.02 YES 0.05 YES 0.02 YES 0.00 YES 0.01 YES 0.02 YES 0.02 YES 0.03
noabs YES 0.04 MAYBE MAYBE MAYBE YES 0.02 MAYBE YES 0.02 YES 0.04 YES 0.08
onearg YES 0.19 YES 0.17 YES 0.17 YES 0.04 YES 0.53 YES 0.44 YES 0.46 YES 0.17 YES 0.29
ordrec YES 0.38 MAYBE MAYBE MAYBE YES 0.29 YES 0.01 MAYBE YES 0.37 YES 0.50
plode YES 0.31 YES 0.30 YES 0.12 MAYBE YES 1.39 YES 0.01 YES 1.16 YES 0.35 YES 0.41
prefixsum YES 0.12 MAYBE MAYBE MAYBE YES 0.05 YES 0.04 MAYBE YES 0.19 YES 0.18
prenex YES 0.12 YES 0.11 MAYBE YES 0.11 YES 0.33 MAYBE YES 0.32 YES 0.14 YES 0.18
process YES 3.21 YES 3.82 MAYBE YES 0.46 YES 2.54 MAYBE YES 2.27 YES 3.35 YES 3.79
qsort YES 1.62 MAYBE MAYBE MAYBE YES 1.51 YES 1.31 YES 1.35 YES 1.17 YES 2.17
rec YES 0.10 YES 0.14 YES 0.06 MAYBE YES 0.00 YES 0.01 YES 0.04 YES 0.11 YES 0.12
reverse YES 0.61 YES 0.56 YES 0.20 MAYBE YES 14.94 YES 0.64 YES 13.21 YES 0.61 YES 0.79
sdu YES 0.27 YES 0.27 YES 0.55 YES 0.30 YES 0.97 MAYBE YES 0.82 YES 0.33 YES 0.37
sort YES 2.06 YES 2.07 YES 0.45 MAYBE YES 0.65 YES 0.74 YES 6.23 YES 2.16 YES 2.74
uncurry YES 0.01 YES 0.01 YES 0.03 YES 0.01 YES 0.81 YES 0.70 YES 0.50 YES 0.01 YES 0.01
zipWith YES 1.14 MAYBE MAYBE MAYBE YES 1.35 YES 0.87 YES 1.09 YES 0.44 YES 2.15
average YES 0.59 MAYBE MAYBE MAYBE YES 0.65 MAYBE YES 0.59 YES 0.09 YES 0.97
lambda5 NO 0.00 MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE NO 0.00 NO 0.00
merge YES 0.05 YES 0.05 MAYBE YES 0.05 YES 0.65 YES 0.61 YES 0.54 YES 0.06 YES 0.07
noneating YES 0.52 MAYBE MAYBE MAYBE YES 0.66 YES 0.58 YES 0.54 YES 0.02 YES 1.15
shuffle YES 0.09 YES 0.10 MAYBE YES 0.09 YES 0.81 YES 0.79 YES 0.74 YES 0.09 YES 0.17
twice YES 0.11 MAYBE MAYBE MAYBE YES 0.05 MAYBE YES 0.04 YES 0.11 YES 0.16
fuhs11frocos_a MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE
listrepeat MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE
prefixshuffle YES 1.61 MAYBE MAYBE MAYBE YES 1.67 YES 1.19 MAYBE YES 0.94 YES 2.89
prenex_modif1 YES 0.07 YES 0.07 MAYBE YES 0.09 YES 0.20 YES 0.07 YES 0.18 YES 0.07 YES 0.25
sqr MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE
tailrecgen MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE
twice_modif4 YES 0.05 MAYBE MAYBE MAYBE YES 0.02 MAYBE YES 0.03 YES 0.05 YES 0.07
fuhkop11frocos YES 0.07 YES 0.08 YES 0.18 YES 0.09 YES 0.77 YES 0.77 YES 0.78 YES 0.07 YES 0.09
fuhkop12rta1 YES 0.11 YES 0.11 MAYBE YES 0.11 YES 0.75 YES 0.63 YES 0.70 YES 0.11 YES 0.11
fuhkop12rta2 YES 0.86 MAYBE MAYBE MAYBE YES 1.10 YES 0.80 YES 0.79 YES 0.17 YES 0.92
kop11cai1 YES 0.51 YES 0.50 YES 0.27 MAYBE YES 1.46 MAYBE YES 1.10 YES 0.54 YES 0.50
kop11cai2 YES 0.01 YES 0.01 YES 0.02 YES 0.01 YES 0.00 MAYBE YES 0.00 YES 0.01 YES 0.01
kop12lmcs1 MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE
kop12lmcs2 YES 0.09 MAYBE MAYBE MAYBE YES 0.07 YES 0.00 MAYBE YES 0.09 YES 0.11
kop12thesis_ex2.11 YES 0.21 YES 0.22 YES 0.09 MAYBE YES 0.01 YES 0.01 YES 0.34 YES 0.22 YES 0.22
kop12thesis_ex7.23 YES 0.05 YES 0.05 MAYBE YES 0.05 YES 0.01 YES 0.00 YES 0.02 YES 0.04 YES 0.05
kop12thesis_ex7.45_1 MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE
kop12thesis_ex7.45_2 MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE
kop12thesis_sec3.3.3 YES 0.03 MAYBE MAYBE MAYBE YES 0.00 YES 0.00 YES 0.00 YES 0.03 YES 0.03
churchNum2 TIMEOUT TIMEOUT TIMEOUT TIMEOUT TIMEOUT TIMEOUT TIMEOUT TIMEOUT TIMEOUT
churchNum TIMEOUT TIMEOUT TIMEOUT TIMEOUT TIMEOUT MAYBE TIMEOUT TIMEOUT TIMEOUT
DicosmoKesner93 YES 1.00 MAYBE MAYBE MAYBE YES 0.51 YES 0.52 MAYBE YES 0.15 YES 1.27
gstate MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE
kripke YES 0.52 MAYBE MAYBE MAYBE YES 0.70 YES 0.54 MAYBE YES 0.03 YES 0.64
lambda_prod YES 0.53 MAYBE MAYBE MAYBE YES 0.59 YES 0.58 MAYBE YES 0.03 YES 0.68
lambda_sum YES 0.03 MAYBE MAYBE MAYBE YES 0.01 YES 0.01 MAYBE YES 0.04 YES 0.43
monad YES 0.07 YES 0.05 MAYBE YES 0.04 YES 0.25 YES 0.02 YES 0.24 YES 0.07 TIMEOUT
pical YES 0.04 YES 0.04 MAYBE YES 0.03 YES 0.75 TIMEOUT YES 0.60 YES 0.05 YES 0.07
restriction YES 7.36 MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE YES 9.77 YES 6.82
slml MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE MAYBE TIMEOUT MAYBE
SystemT YES 0.07 TIMEOUT MAYBE TIMEOUT YES 0.02 YES 0.01 TIMEOUT YES 0.09 TIMEOUT
typed_lamUNC YES 0.01 MAYBE MAYBE MAYBE YES 0.01 YES 0.01 MAYBE YES 0.01 YES 0.11
typed_lam YES 0.01 MAYBE MAYBE MAYBE YES 0.00 YES 0.00 MAYBE YES 0.02 YES 0.10
ysllc YES 0.07 MAYBE MAYBE MAYBE YES 0.01 YES 0.01 MAYBE YES 0.08 YES 0.31
01GoedelT YES 0.11 YES 0.11 YES 0.07 TIMEOUT YES 0.01 YES 0.01 YES 0.05 YES 0.16 TIMEOUT
02Ackermann YES 0.12 YES 0.12 YES 0.06 MAYBE YES 0.60 YES 0.72 YES 0.55 YES 0.14 YES 0.14
03minus YES 0.00 YES 0.00 YES 0.02 YES 0.00 YES 0.57 YES 0.52 YES 0.53 YES 0.01 YES 0.00
04arrow YES 0.00 YES 0.00 YES 0.04 YES 0.00 YES 0.53 YES 0.55 YES 0.51 YES 0.01 YES 0.00
05height YES 0.01 YES 0.01 YES 0.06 YES 0.00 YES 0.55 YES 0.58 YES 0.60 YES 0.01 YES 0.00
06plusmult YES 0.18 YES 0.18 YES 0.17 YES 0.07 YES 0.58 YES 0.56 YES 0.56 YES 0.24 YES 0.18
07ordinal YES 0.01 YES 0.00 MAYBE YES 0.01 YES 0.03 YES 0.01 YES 0.03 YES 0.01 YES 0.01
09ex YES 0.00 YES 0.00 YES 0.01 YES 0.02 YES 0.00 MAYBE YES 0.00 YES 0.01 YES 0.13
Total YES 67 39 29 27 66 51 54 67 64
Total NO 5 0 0 0 0 0 0 4 5
Total MAYBE 13 45 57 56 19 35 30 13 13
Total TIMEOUT 3 4 2 5 3 2 4 4 6
Average Runtime 0.45 0.27 0.12 0.06 0.69 0.35 0.81 0.37 0.63