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