Completion Test Database: Results
Equational System
mkbtt-lpo
maxcomp-lpo
mkbtt-kbo
maxcomp-kbo
mkbtt-full
slothrop
AD93_Z22.trs
∞
∞
∞
∞
∞
∞
ASK93_1.trs
0.01
0.10
0.02
0.01
0.01
0.98
ASK93_2.trs
∞
∞
∞
∞
∞
∞
ASK93_5.trs
∞
∞
∞
∞
∞
∞
ASK93_6.trs
16.75
1.06
10.93
0.83
5.73
10.81
aufgabe3_2.trs
0.01
0.00
0.01
0.00
0.00
0.95
aufgabe3_3.trs
0.01
0.00
0.01
0.00
0.01
0.87
BD94_collapse.trs
0.05
0.01
0.08
0.01
0.03
1.18
BD94_peano.trs
0.03
0.00
∞
∞
0.02
1.22
BD94_sqrt.trs
0.02
0.00
0.03
0.01
0.02
1.00
BGK94_D08.trs
∞
0.70
∞
∞
∞
∞
BGK94_D10.trs
∞
0.88
∞
∞
51.49
∞
BGK94_D12.trs
∞
1.18
∞
∞
52.44
∞
BGK94_D16.trs
∞
37.48
∞
∞
74.91
∞
BGK94_M08.trs
0.74
0.24
1.25
0.49
0.59
7.72
BGK94_M10.trs
1.20
0.81
2.24
∞
0.94
20.97
BGK94_M12.trs
1.83
41.69
3.65
∞
1.42
27.18
BGK94_M14.trs
2.73
∞
5.73
∞
2.06
25.88
BGK94_Z22W.trs
∞
∞
∞
∞
∞
∞
BH96_fac8_theory.trs
0.11
0.02
0.52
0.06
0.07
2.07
Chr89_A2.trs
4.21
0.99
4.81
0.95
95.76
182.93
Chr89_A24.trs
∞
∞
∞
∞
∞
∞
Chr89_A3.trs
40.06
3.17
20.85
∞
∞
∞
fggx.trs
0.01
0.01
0.02
0.01
0.01
0.98
fib.trs
0.87
100.32
∞
∞
0.85
7.18
HR94_1.trs
∞
∞
∞
∞
∞
∞
HR94_2.trs
∞
∞
∞
∞
∞
∞
kb_fail.trs
fail
fail
fail
∞
fail
fail
kb_fail1.trs
fail
fail
fail
fail
fail
fail
KK99_linear_assoc.trs
0.02
0.00
0.02
0.01
0.03
0.83
Les83_fib.trs
0.10
0.01
∞
∞
0.23
2.82
Les83_subset.trs
0.22
0.01
∞
∞
0.09
3.27
lr_theory.trs
0.35
0.11
0.45
2.89
1.74
7.90
LS06_CGE4.trs
∞
∞
∞
∞
∞
∞
LS06_CGE5.trs
∞
∞
∞
∞
∞
∞
LS94_G0.trs
0.52
0.05
0.71
0.06
1.28
5.90
LS94_G1.trs
∞
∞
∞
∞
∞
∞
LS94_G2.trs
∞
∞
∞
∞
∞
∞
LS94_G3.trs
∞
∞
∞
∞
∞
∞
LS94_P1.trs
∞
∞
∞
∞
∞
∞
OKW95_dt1_theory.trs
0.78
46.15
∞
∞
0.91
6.22
rl_theory.trs
2.36
0.17
∞
1.19
1.76
8.07
Sim91_sims2.trs
∞
∞
∞
∞
∞
∞
SK90_3.01.trs
1.20
0.09
2.23
0.61
4.16
18.85
SK90_3.02.trs
0.03
0.01
0.03
0.02
0.05
0.97
SK90_3.03.trs
4.69
1.01
3.88
0.05
1.59
5.54
SK90_3.04.trs
6.72
1.75
∞
∞
99.98
∞
SK90_3.05.trs
1.58
0.35
1.07
0.33
3.46
∞
SK90_3.06.trs
4.22
0.90
∞
∞
∞
∞
SK90_3.07.trs
∞
3.03
∞
∞
∞
∞
SK90_3.08.trs
0.08
0.01
0.06
0.03
0.05
1.18
SK90_3.09.trs
∞
∞
∞
∞
∞
∞
SK90_3.10.trs
0.03
0.01
0.03
0.01
0.02
0.92
SK90_3.11.trs
0.03
0.01
0.03
0.01
0.02
1.02
SK90_3.12.trs
fail
fail
fail
fail
fail
fail
SK90_3.13.trs
0.17
0.02
0.16
0.02
0.17
1.33
SK90_3.14.trs
0.13
0.01
0.21
0.16
0.15
1.65
SK90_3.15.trs
∞
∞
0.12
0.02
0.08
1.39
SK90_3.16.trs
0.02
0.01
0.03
0.01
0.01
0.80
SK90_3.17.trs
0.05
0.01
0.04
0.01
0.08
1.25
SK90_3.18.trs
0.15
0.01
∞
∞
0.30
3.50
SK90_3.19.trs
0.15
0.09
0.26
15.11
0.32
2.73
SK90_3.20.trs
0.35
1.34
0.42
∞
0.46
2.65
SK90_3.21.trs
0.16
0.04
0.25
0.03
0.19
85.81
SK90_3.22.trs
∞
4.03
∞
8.03
∞
∞
SK90_3.23.trs
0.30
96.93
0.43
0.19
0.37
4.72
SK90_3.24.trs
0.04
0.02
0.04
0.01
0.04
1.26
SK90_3.25.trs
0.02
0.43
0.02
0.01
0.03
0.99
SK90_3.26.trs
∞
∞
∞
∞
∞
∞
SK90_3.27.trs
13.31
21.09
36.47
0.53
72.31
∞
SK90_3.28.trs
∞
20.23
53.58
∞
∞
110.76
SK90_3.29.trs
2.29
0.86
3.91
1.75
2.02
5.27
SK90_3.30.trs
0.03
0.01
0.03
0.02
0.02
0.76
SK90_3.31.trs
0.03
0.01
0.04
0.01
0.01
0.84
SK90_3.32.trs
0.01
0.00
0.01
0.00
0.01
0.74
SK90_3.33.trs
0.03
0.00
0.02
0.01
0.02
0.91
slothrop_ackermann.trs
0.02
0.00
∞
∞
0.03
0.68
slothrop_cge.trs
∞
∞
∞
∞
173.03
∞
slothrop_cge3.trs
∞
∞
∞
∞
∞
∞
slothrop_endo.trs
∞
0.62
∞
0.38
3.88
7.60
slothrop_equiv_proofs.trs
fail
fail
∞
∞
2.52
262.32
slothrop_equiv_proofs_or.trs
fail
fail
∞
∞
2.81
∞
slothrop_fgh.trs
0.01
0.01
0.01
0.01
0.00
0.73
slothrop_groups.trs
0.45
0.08
∞
0.08
0.54
2.22
slothrop_groups_conj.trs
0.11
0.02
0.18
1.10
0.21
2.49
slothrop_hard.trs
0.01
0.00
0.01
0.02
0.01
0.69
slothrop_nlp-2b.trs
∞
∞
∞
∞
∞
∞
TPDB_secret2006_torpa_secr10.trs
2.21
0.17
14.34
0.55
9.15
50.46
TPDB_secret2006_torpa_secr4.trs
4.77
35.69
15.25
31.62
17.10
35.56
TPDB_thiemann27.trs
∞
∞
∞
∞
∞
∞
TPDB_zantema_z115.trs
∞
0.73
5.67
42.63
15.27
203.69
TPTP_BOO027-1_theory.trs
0.04
0.02
0.04
0.01
0.03
1.37
TPTP_COL053-1_theory.trs
0.01
0.00
0.01
0.00
0.01
0.67
TPTP_COL056-1_theory.trs
0.04
0.01
0.03
0.87
0.03
0.82
TPTP_COL060-1_theory.trs
fail
fail
0.01
0.00
0.02
1.14
TPTP_COL085-1_theory.trs
0.00
0.00
0.00
0.00
0.00
0.66
TPTP_GRP010-4_theory.trs
1.52
0.27
2.21
0.11
6.02
231.47
TPTP_GRP011-4_theory.trs
0.48
0.09
0.62
0.10
0.63
25.42
TPTP_GRP012-4_theory.trs
0.28
0.03
0.34
0.03
0.48
2.13
TPTP_GRP393-2_theory.trs
0.01
0.00
0.01
0.00
0.01
0.68
TPTP_GRP394-3_theory.trs
0.33
0.06
0.42
0.07
0.51
2.68
TPTP_GRP454-1_theory.trs
17.13
2.65
49.63
0.14
109.87
∞
TPTP_GRP457-1_theory.trs
17.18
2.66
49.98
1.62
112.73
∞
TPTP_GRP460-1_theory.trs
∞
0.89
17.74
2.91
16.99
∞
TPTP_GRP463-1_theory.trs
∞
1.76
17.80
3.26
16.91
∞
TPTP_GRP481-1_theory.trs
∞
2.40
∞
57.20
∞
69.56
TPTP_GRP484-1_theory.trs
∞
0.52
∞
13.52
∞
∞
TPTP_GRP487-1_theory.trs
∞
1.00
∞
7.05
∞
fail
TPTP_GRP490-1_theory.trs
∞
0.84
168.93
13.21
∞
∞
TPTP_GRP493-1_theory.trs
∞
5.13
40.54
2.83
∞
∞
TPTP_GRP496-1_theory.trs
∞
0.90
∞
11.13
∞
241.10
TPTP_HWC004-1_theory.trs
0.13
0.03
0.09
0.01
0.14
1.32
TPTP_HWC004-2_theory.trs
0.05
0.01
0.04
0.01
0.03
1.09
TPTP_SWV262-2_theory.trs
0.03
0.02
0.03
0.05
0.03
0.88
WS06_proofreduction.trs
∞
∞
∞
∞
162.66
∞