Combining WANDA with various first-order termination provers on a specific subset of the TPDB

This group of experiments considers WANDA's power when combined with various different first-order termination tools. Experiments were done on the TPDB 2017: this is the same as the TPDB 2018, except it does not include the most recent batch of benchmarks: the directory Hamana_Kikuchi_18/. The benchmarks are presented in the order: Mixed_HO_10/, Kop_11/, Mixed_HO_12/, Kop_13/, Hamana_17/, Hamana_17/Blanqui_15/, Uncurried_Applicative_11/.

Filename	aprove	natt	muterm	natt+aprove	noprover
applicative	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
apply	YES 0.05	YES 0.04	YES 0.04	YES 0.04	YES 0.05
app	YES 0.00	YES 0.00	YES 0.00	YES 0.00	YES 0.00
counterex1	NO 0.00	NO 0.00	NO 0.00	NO 0.00	NO 0.00
counterex2	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
curry1	YES 0.00	YES 0.00	YES 0.00	YES 0.00	YES 0.00
curry	YES 0.00	YES 0.00	YES 0.00	YES 0.00	YES 0.01
deriv	TIMEOUT	TIMEOUT	TIMEOUT	TIMEOUT	TIMEOUT
eval	YES 0.64	YES 0.18	YES 0.16	YES 0.17	YES 0.10
extrec	YES 0.14	YES 0.14	YES 0.16	YES 0.15	YES 0.17
filter	YES 0.03	YES 0.03	YES 0.03	YES 0.03	YES 0.03
findzero	YES 1.11	YES 0.64	YES 0.65	YES 0.71	YES 0.64
foldl	YES 0.26	YES 0.28	YES 0.28	YES 0.27	YES 0.27
foobar	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
from	YES 0.93	YES 0.45	YES 0.42	YES 0.43	YES 0.46
hrsdif1	NO 0.00	NO 0.00	NO 0.00	NO 0.00	NO 0.00
hrsdif2	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
if	YES 0.65	YES 0.21	YES 0.20	YES 0.21	YES 0.23
inlamb	YES 0.01	YES 0.00	YES 0.00	YES 0.00	YES 0.00
iterative	YES 1.02	YES 1.02	YES 1.10	YES 1.13	YES 1.24
lambda1	NO 0.00	NO 0.00	NO 0.00	NO 0.00	NO 0.00
lambda2	NO 1.63	MAYBE	MAYBE	NO 0.96	MAYBE
lambda3	YES 0.04	YES 0.02	YES 0.01	YES 0.02	YES 0.02
length	YES 0.10	YES 0.11	YES 0.10	YES 0.11	YES 0.11
loopy	YES 0.02	YES 0.02	YES 0.02	YES 0.02	YES 0.04
map	YES 0.01	YES 0.02	YES 0.02	YES 0.02	YES 0.02
noabs	YES 0.04	YES 0.04	YES 0.04	YES 0.04	YES 0.05
onearg	YES 0.18	YES 0.18	YES 0.19	YES 0.18	YES 0.21
ordrec	YES 0.34	YES 0.34	YES 0.36	YES 0.37	YES 0.35
plode	YES 0.29	YES 0.31	YES 0.32	YES 0.32	YES 0.33
prefixsum	YES 0.12	YES 0.12	YES 0.12	YES 0.12	YES 0.14
prenex	YES 0.11	YES 0.11	YES 0.12	YES 0.11	YES 0.13
process	YES 3.04	YES 3.15	YES 3.18	YES 3.17	YES 3.61
qsort	YES 1.53	YES 1.05	YES 1.05	YES 1.08	YES 1.14
rec	YES 0.10	YES 0.10	YES 0.10	YES 0.10	YES 0.11
reverse	YES 0.57	YES 0.57	YES 0.57	YES 0.57	YES 0.71
sdu	YES 0.27	YES 0.27	YES 0.28	YES 0.29	YES 0.34
sort	YES 2.01	YES 2.02	YES 2.20	YES 2.09	YES 2.32
uncurry	YES 0.01	YES 0.01	YES 0.01	YES 0.01	YES 0.01
zipWith	YES 1.07	YES 0.41	YES 0.40	YES 0.42	YES 0.45
average	YES 0.58	YES 0.08	YES 0.09	YES 0.07	YES 0.09
lambda5	NO 0.00	NO 0.00	NO 0.00	NO 0.00	NO 0.00
merge	YES 0.04	YES 0.06	YES 0.05	YES 0.05	YES 0.07
noneating	YES 0.48	YES 0.03	YES 0.03	YES 0.03	YES 0.04
shuffle	YES 0.09	YES 0.09	YES 0.09	YES 0.09	YES 0.16
twice	YES 0.10	YES 0.10	YES 0.10	YES 0.11	YES 0.17
fuhs11frocos_a	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
listrepeat	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
prefixshuffle	YES 1.48	YES 0.84	YES 0.89	YES 0.84	YES 0.93
prenex_modif1	YES 0.07	YES 0.07	YES 0.07	YES 0.07	YES 0.07
sqr	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
tailrecgen	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
twice_modif4	YES 0.05	YES 0.05	YES 0.05	YES 0.05	YES 0.05
fuhkop11frocos	YES 0.07	YES 0.07	YES 0.07	YES 0.07	YES 0.07
fuhkop12rta1	YES 0.11	YES 0.11	YES 0.11	YES 0.11	YES 0.12
fuhkop12rta2	YES 0.84	YES 0.16	YES 0.16	YES 0.17	YES 0.18
kop11cai1	YES 0.51	YES 0.53	YES 0.50	YES 0.54	YES 0.50
kop11cai2	YES 0.01	YES 0.01	YES 0.01	YES 0.01	YES 0.01
kop12lmcs1	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
kop12lmcs2	YES 0.09	YES 0.09	YES 0.09	YES 0.09	YES 0.10
kop12thesis_ex2.11	YES 0.22	YES 0.25	YES 0.23	YES 0.22	YES 0.24
kop12thesis_ex7.23	YES 0.04	YES 0.05	YES 0.04	YES 0.04	YES 0.05
kop12thesis_ex7.45_1	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
kop12thesis_ex7.45_2	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
kop12thesis_sec3.3.3	YES 0.03	YES 0.03	YES 0.03	YES 0.03	YES 0.03
churchNum2	TIMEOUT	TIMEOUT	TIMEOUT	TIMEOUT	TIMEOUT
churchNum	TIMEOUT	TIMEOUT	TIMEOUT	TIMEOUT	TIMEOUT
DicosmoKesner93	YES 1.44	YES 0.17	YES 0.13	YES 0.17	YES 0.19
gstate	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
kripke	YES 0.51	YES 0.03	YES 0.02	YES 0.03	YES 0.02
lambda_prod	YES 0.52	YES 0.04	YES 0.03	YES 0.03	YES 0.02
lambda_sum	YES 0.03	YES 0.03	YES 0.03	YES 0.03	YES 0.03
monad	YES 0.05	YES 0.05	YES 0.05	YES 0.05	YES 0.05
pical	YES 0.04	YES 0.04	YES 0.04	YES 0.04	YES 0.04
restriction	YES 7.09	YES 7.32	YES 7.43	YES 7.65	YES 7.71
slml	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
SystemT	YES 0.06	YES 0.06	YES 0.07	YES 0.07	YES 0.06
typed_lamUNC	YES 0.01	YES 0.01	YES 0.01	YES 0.01	YES 0.01
typed_lam	YES 0.01	YES 0.01	YES 0.01	YES 0.01	YES 0.01
ysllc	YES 0.06	YES 0.06	YES 0.07	YES 0.06	YES 0.06
01GoedelT	YES 0.11	YES 0.12	YES 0.11	YES 0.11	YES 0.11
02Ackermann	YES 0.12	YES 0.11	YES 0.11	YES 0.11	YES 0.11
03minus	YES 0.00	YES 0.00	YES 0.00	YES 0.00	YES 0.00
04arrow	YES 0.00	YES 0.00	YES 0.00	YES 0.00	YES 0.00
05height	YES 0.00	YES 0.00	YES 0.00	YES 0.00	YES 0.00
06plusmult	YES 0.17	YES 0.18	YES 0.18	YES 0.18	YES 0.18
07ordinal	YES 0.01	YES 0.01	YES 0.01	YES 0.01	YES 0.01
09ex	YES 0.00	YES 0.00	YES 0.00	YES 0.00	YES 0.00
AotoYamada_05__001	NO 0.00	NO 0.00	NO 0.00	NO 0.00	NO 0.00
AotoYamada_05__002	YES 0.13	YES 0.13	YES 0.13	YES 0.12	YES 0.14
AotoYamada_05__003	NO 0.00	NO 0.00	NO 0.00	NO 0.00	NO 0.00
AotoYamada_05__004	YES 0.02	YES 0.02	YES 0.02	YES 0.03	YES 0.03
AotoYamada_05__005	YES 0.00	YES 0.00	YES 0.00	YES 0.00	YES 0.00
AotoYamada_05__006	YES 0.03	YES 0.03	YES 0.03	YES 0.03	YES 0.04
AotoYamada_05__007	YES 0.05	YES 0.05	YES 0.06	YES 0.06	YES 0.05
AotoYamada_05__009	YES 0.05	YES 0.05	YES 0.05	YES 0.06	YES 0.06
AotoYamada_05__010	YES 0.41	YES 0.42	YES 0.44	YES 0.40	YES 0.45
AotoYamada_05__011	YES 0.05	YES 0.05	YES 0.05	YES 0.05	YES 0.05
AotoYamada_05__012	YES 0.05	YES 0.05	YES 0.06	YES 0.06	YES 0.06
AotoYamada_05__013	YES 0.07	YES 0.07	YES 0.07	YES 0.07	YES 0.07
AotoYamada_05__014	YES 0.40	YES 0.42	YES 0.44	YES 0.41	YES 0.45
AotoYamada_05__015	YES 0.21	YES 0.22	YES 0.21	YES 0.22	YES 0.22
AotoYamada_05__016	YES 0.48	YES 0.51	YES 0.48	YES 0.48	YES 0.52
AotoYamada_05__017	YES 0.00	YES 0.00	YES 0.00	YES 0.00	YES 0.01
AotoYamada_05__019	YES 0.06	YES 0.06	YES 0.07	YES 0.06	YES 0.06
AotoYamada_05__020	YES 0.10	YES 0.10	YES 0.13	YES 0.11	YES 0.10
AotoYamada_05__021	YES 0.46	YES 0.48	YES 0.48	YES 0.48	YES 0.47
AotoYamada_05__022	YES 0.06	YES 0.05	YES 0.05	YES 0.05	YES 0.05
AotoYamada_05__023	YES 0.01	YES 0.01	YES 0.01	YES 0.01	YES 0.01
AotoYamada_05__024	YES 0.02	YES 0.02	YES 0.02	YES 0.02	YES 0.02
AotoYamada_05__025	YES 0.00	YES 0.00	YES 0.00	YES 0.00	YES 0.00
AotoYamada_05__026	YES 0.12	YES 0.12	YES 0.12	YES 0.12	YES 0.12
AotoYamada_05__027	YES 0.05	YES 0.05	YES 0.05	YES 0.05	YES 0.05
AotoYamada_05__028	YES 0.02	YES 0.02	YES 0.02	YES 0.03	YES 0.02
AotoYamada_05__Ex1SimplyTyped	YES 0.02	YES 0.02	YES 0.02	YES 0.02	YES 0.02
AotoYamada_05__Ex5TermProof	YES 0.35	YES 0.35	YES 0.39	YES 0.38	YES 0.36
Applicative_05__BTreeMember	YES 0.11	YES 0.11	YES 0.11	YES 0.11	YES 0.11
Applicative_05__Ex2_6_1Composition	YES 0.01	YES 0.01	YES 0.01	YES 0.02	YES 0.01
Applicative_05__Ex2_8_1ConstSubstFix	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
Applicative_05__Ex2PrimRec	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
Applicative_05__Ex3Lists	YES 0.06	YES 0.06	YES 0.06	YES 0.06	YES 0.06
Applicative_05__Ex4MapList	YES 0.04	YES 0.04	YES 0.04	YES 0.04	YES 0.04
Applicative_05__Ex5Folding	YES 0.26	YES 0.28	YES 0.27	YES 0.28	YES 0.28
Applicative_05__Ex5Sorting	YES 3.43	YES 3.57	YES 3.57	YES 3.71	YES 3.63
Applicative_05__Ex6_11	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
Applicative_05__Ex6Folding	YES 0.43	YES 0.44	YES 0.45	YES 0.44	YES 0.46
Applicative_05__Ex6Recursor	YES 0.07	YES 0.07	YES 0.08	YES 0.07	YES 0.07
Applicative_05__Ex7_9	YES 0.89	YES 0.22	YES 0.26	YES 0.23	YES 0.22
Applicative_05__Ex7OrdinalRec	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
Applicative_05__Ex7Sorting	YES 1.29	YES 1.26	YES 1.39	YES 1.24	YES 1.31
Applicative_05__Ex9Maps	YES 11.92	YES 12.32	YES 11.51	YES 12.21	YES 11.52
Applicative_05__Hamming	NO 0.00	NO 0.00	NO 0.00	NO 0.00	NO 0.00
Applicative_05__mapDivMinusHard	YES 0.78	YES 0.14	YES 0.14	YES 0.14	MAYBE
Applicative_05__mapDivMinus	YES 0.73	YES 0.11	YES 0.11	YES 0.12	YES 0.12
Applicative_05__ReverseLastInit	YES 0.28	YES 0.27	YES 0.27	YES 0.29	YES 0.27
Applicative_05__TakeDropWhile	YES 0.05	YES 0.05	YES 0.05	YES 0.05	YES 0.06
Applicative_05__termMonTypes	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
Applicative_05__TreeFlatten	YES 0.09	YES 0.10	YES 0.09	YES 0.09	YES 0.09
Applicative_05__TreeHeight	YES 0.05	YES 0.05	YES 0.05	YES 0.05	YES 0.05
Applicative_05__TreeLevels	YES 0.07	YES 0.07	YES 0.07	YES 0.07	YES 0.07
Applicative_05__TreeMap	YES 0.34	YES 0.34	YES 0.34	YES 0.35	YES 0.34
Applicative_05__TreeSize	YES 0.04	YES 0.04	YES 0.04	YES 0.06	YES 0.04
Applicative_05__TypeEx3	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
Applicative_05__TypeEx5	NO 0.00	NO 0.00	NO 0.00	NO 0.00	NO 0.00
Applicative_AG01_innermost__#4.10	NO 1.51	MAYBE	MAYBE	NO 0.95	MAYBE
Applicative_AG01_innermost__#4.13	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
Applicative_AG01_innermost__#4.15	NO 1.67	MAYBE	MAYBE	NO 0.91	MAYBE
Applicative_AG01_innermost__#4.17	NO 2.09	MAYBE	MAYBE	NO 0.99	MAYBE
Applicative_AG01_innermost__#4.19	TIMEOUT	MAYBE	TIMEOUT	TIMEOUT	MAYBE
Applicative_AG01_innermost__#4.22	YES 2.58	YES 0.25	YES 0.24	YES 0.30	YES 0.24
Applicative_AG01_innermost__#4.24	YES 2.49	YES 0.34	YES 0.33	YES 0.37	YES 0.30
Applicative_AG01_innermost__#4.26	YES 1.10	YES 0.35	YES 0.33	YES 0.34	MAYBE
Applicative_AG01_innermost__#4.28	YES 0.66	YES 0.23	YES 0.23	YES 0.25	MAYBE
Applicative_AG01_innermost__#4.2	NO 1.86	MAYBE	MAYBE	NO 0.95	MAYBE
Applicative_AG01_innermost__#4.34	YES 1.06	YES 0.32	YES 0.32	YES 0.32	YES 0.38
Applicative_AG01_innermost__#4.36	YES 1.66	YES 0.71	YES 0.75	YES 0.67	YES 0.76
Applicative_AG01_innermost__#4.3	NO 1.45	MAYBE	MAYBE	NO 0.85	MAYBE
Applicative_AG01_innermost__#4.5	NO 0.00	NO 0.00	NO 0.00	NO 0.00	NO 0.00
Applicative_AG01_innermost__#4.7	NO 1.81	MAYBE	MAYBE	NO 0.90	MAYBE
Applicative_AG01_innermost__#4.8	MAYBE	MAYBE	MAYBE	MAYBE	MAYBE
Applicative_first_order_05__01	YES 0.11	YES 0.11	YES 0.11	YES 0.13	YES 0.13
Applicative_first_order_05__02	YES 0.12	YES 0.11	YES 0.11	YES 0.13	YES 0.12
Applicative_first_order_05__06	YES 0.15	YES 0.14	YES 0.14	YES 0.15	YES 0.14
Applicative_first_order_05__08	YES 0.42	YES 0.46	YES 0.43	YES 0.42	YES 0.44
Applicative_first_order_05__11	YES 1.71	YES 1.50	YES 1.64	YES 1.52	YES 1.68
Applicative_first_order_05__12	YES 1.00	YES 0.82	YES 0.86	YES 0.95	YES 0.81
Applicative_first_order_05__13	YES 18.35	YES 0.89	YES 0.88	TIMEOUT	YES 0.44
Applicative_first_order_05__17	YES 0.17	YES 0.15	YES 0.15	YES 0.19	YES 0.14
Applicative_first_order_05__18	YES 0.24	YES 0.21	YES 0.24	YES 0.25	YES 0.23
Applicative_first_order_05__21	YES 0.91	YES 0.30	YES 0.29	YES 0.38	MAYBE
Applicative_first_order_05__29	YES 0.62	YES 0.63	YES 0.63	YES 0.72	YES 0.67
Applicative_first_order_05__30	YES 0.53	YES 0.51	YES 0.47	YES 0.50	YES 0.48
Applicative_first_order_05__#3.10	YES 1.80	YES 0.70	YES 0.80	YES 0.80	YES 0.91
Applicative_first_order_05__#3.13	YES 1.71	YES 0.71	YES 0.76	YES 0.73	YES 0.80
Applicative_first_order_05__#3.16	YES 0.45	YES 0.40	YES 0.39	YES 0.49	YES 0.40
Applicative_first_order_05__#3.18	YES 1.05	YES 0.33	YES 0.29	YES 0.34	YES 0.34
Applicative_first_order_05__31	YES 0.77	YES 0.66	YES 0.67	YES 0.76	YES 0.72
Applicative_first_order_05__#3.22	YES 0.96	YES 0.22	YES 0.42	YES 0.23	YES 3.95
Applicative_first_order_05__#3.25	YES 0.63	YES 0.15	YES 0.17	YES 0.15	YES 0.17
Applicative_first_order_05__#3.27	YES 0.13	YES 0.12	YES 0.12	YES 0.12	YES 0.12
Applicative_first_order_05__#3.2	YES 1.00	YES 0.27	YES 0.26	YES 0.29	YES 0.30
Applicative_first_order_05__#3.32	YES 0.56	YES 0.16	YES 0.15	YES 0.17	YES 0.15
Applicative_first_order_05__#3.36	YES 1.13	YES 0.29	YES 0.29	YES 0.31	YES 0.33
Applicative_first_order_05__#3.38	YES 1.03	YES 0.30	YES 0.30	YES 0.32	YES 0.34
Applicative_first_order_05__33	TIMEOUT	MAYBE	TIMEOUT	TIMEOUT	MAYBE
Applicative_first_order_05__#3.40	YES 1.43	MAYBE	YES 1.58	TIMEOUT	MAYBE
Applicative_first_order_05__#3.45	YES 0.71	YES 0.17	YES 0.16	YES 0.22	YES 0.15
Applicative_first_order_05__#3.48	YES 0.84	YES 0.24	YES 0.22	YES 0.29	YES 0.24
Applicative_first_order_05__#3.52	YES 0.76	YES 0.17	YES 0.16	YES 0.16	YES 0.15
Applicative_first_order_05__#3.55	YES 1.62	YES 0.64	YES 0.60	YES 0.65	YES 0.74
Applicative_first_order_05__#3.57	YES 1.38	YES 0.62	YES 0.68	YES 0.71	YES 0.81
Applicative_first_order_05__#3.6	YES 1.22	YES 0.39	YES 0.44	YES 0.38	YES 0.47
Applicative_first_order_05__#3.8	YES 1.13	YES 0.42	YES 0.44	YES 0.44	YES 0.48
Applicative_first_order_05__hydra	YES 0.86	YES 0.25	YES 0.25	YES 0.27	YES 0.23
Applicative_first_order_05__minsort	TIMEOUT	MAYBE	TIMEOUT	TIMEOUT	MAYBE
Applicative_first_order_05__motivation	YES 1.08	YES 0.23	YES 0.23	YES 0.43	YES 0.26
Applicative_first_order_05__perfect2	YES 1.21	YES 0.36	YES 0.34	YES 0.41	YES 0.37
Applicative_first_order_05__perfect	YES 0.96	YES 0.33	YES 0.31	YES 0.36	YES 0.30
Total YES	155	154	155	153	150
Total NO	16	9	9	16	9
Total MAYBE	21	32	28	21	36
Total TIMEOUT	6	3	6	8	3
Average Runtime	0.72	0.37	0.38	0.41	0.41