mkbTT mkbTT mkbTT  MaxComp MaxComp 
  LPO KBO LPO+KBO  LPO KBO 
  (1)(2)(3)(4) (1)(2)(3)(4) (1)(2)(3)(4)  (1) (1) 
AD93-Z22 ∞ ∞ ∞  ⊥ ⊥ 
ASK93-1 0.06 4 1 5  0.06 4 1 5  0.05 4 1 5   0.03  0.01  
ASK93-2 ∞ ∞ ∞  ∞ ∞ 
ASK93-5 ∞ ∞ ∞  ⊥ ⊥ 
ASK93-6 21.46 17 402 915  27.18 17 402 915  19.25 17 402 915   0.69  0.58  
BD94-collapse 0.15 8 3 12  0.16 8 3 12  0.11 8 3 12   0.01  0.01  
BD94-peano 0.09 5 2 8  ∞ 0.08 5 3 8   0.00  ∞ 
BD94-sqrt 0.06 5 0 4  0.07 5 0 4  0.03 5 0 4   0.00  0.01  
BGK94-D08 24.34 123 14 583  238.82 337 2 2179  71.59 166 12 1143   0.49  ∞ 
BGK94-D10 43.84 168 13 628  35.64 131 1 798  95.26 204 4 1275   0.61  ∞ 
BGK94-D12 53.09 162 13 602  43.83 128 2 824  73.94 168 14 1005   0.85  ∞ 
BGK94-D16 176.28 170 12 739  31.33 124 32 745  85.12 171 3 956   34.01  ∞ 
BGK94-M08 ∞ ∞ ∞  0.17  0.34  
BGK94-M10 ∞ ∞ ∞  0.57  ⊥ 
BGK94-M12 ∞ ∞ ∞  39.57  ⊥ 
BGK94-M14 ∞ ∞ ∞  ∞ ⊥ 
BGK94-Z22W ∞ ∞ ∞  ⊥ ∞ 
BH96-fac8_theory 0.32 7 10 30  0.91 14 8 84  0.34 7 12 34   0.00  0.03  
Chr89-A2 6.96 69 5 197  172.44 156 1 638  17.37 75 17 403   0.72  0.68  
Chr89-A24 ∞ ∞ ∞  ∞ ∞ 
Chr89-A3 ∞ 234.03 308 1 1805  245.15 308 1 1805   2.34  407.64  
HR94-1 ∞ ∞ ∞  ⊥ ⊥ 
HR94-2 ∞ ∞ ∞  ⊥ ⊥ 
KK99-linear_assoc 0.05 3 1 4  0.06 3 1 4  0.05 3 1 4   0.00  0.00  
Les83-fib 0.29 10 2 24  ∞ 0.32 10 4 26   0.00  ∞ 
Les83-subset 0.47 13 5 27  ∞ 0.41 13 5 27   0.01  ∞ 
LS06-CGE4 ⊥ ⊥ ⊥  ∞ ∞ 
LS06-CGE5 ⊥ ⊥ ∞  ∞ ∞ 
LS94-G0 0.47 19 1 27  0.50 19 3 27  0.42 19 3 27   0.03  0.04  
LS94-G1 ∞ ∞ ∞  ∞ ∞ 
LS94-G2 ∞ ∞ ∞  ⊥ ∞ 
LS94-G3 ∞ ∞ ∞  ⊥ ∞ 
LS94-P1 ∞ ∞ ∞  ∞ ⊥ 
OKW95-dt1_theory 1.50 18 22 134  2.69 22 21 208  1.86 18 29 148   40.76  ∞ 
Sim91-sims2 ∞ ∞ ∞  ⊥ ⊥ 
SK90-3.01 0.70 22 2 40  0.92 23 7 47  0.88 23 7 47   0.06  0.44  
SK90-3.02 0.08 4 1 7  0.08 4 1 7  0.07 4 1 7   0.01  0.01  
SK90-3.03 2.58 60 3 102  8.88 52 13 183  9.60 52 13 183   0.75  0.03  
SK90-3.04 0.65 17 1 39  ∞ 0.67 17 2 39   1.40  ⊥ 
SK90-3.05 2.09 39 3 81  2.09 43 1 85  1.96 39 3 81   0.24  0.23  
SK90-3.06 ∞ ∞ ∞  0.63  ∞ 
SK90-3.07 116.86 194 0 466  ∞ 156.36 201 1 636   2.18  ⊥ 
SK90-3.08 0.14 9 2 10  0.16 9 2 10  0.10 9 2 10   0.01  0.02  
SK90-3.09 ∞ ∞ ∞  ⊥ ⊥ 
SK90-3.10 0.12 9 0 8  0.13 9 0 8  0.07 9 0 8   0.00  0.01  
SK90-3.11 0.08 7 0 7  0.10 7 0 7  0.07 7 0 7   0.01  0.01  
SK90-3.12 ⊥ 0.66 17 2 28  0.72 17 2 28   ⊥ ⊥ 
SK90-3.13 0.34 10 3 30  0.36 10 3 30  0.34 10 3 30   0.01  0.01  
SK90-3.14 0.34 10 5 30  0.41 10 9 34  0.38 10 9 34   0.01  0.10  
SK90-3.15 ⊥ 0.24 11 2 16  0.21 11 2 16   ⊥ 0.01  
SK90-3.16 0.07 6 0 5  0.08 6 0 5  0.04 6 0 5   0.00  0.01  
SK90-3.17 0.10 6 1 8  0.12 6 1 10  0.13 6 2 10   0.01  0.01  
SK90-3.18 0.32 12 2 24  ∞ 0.51 12 7 35   0.01  ⊥ 
SK90-3.19 0.47 11 5 43  0.55 11 9 45  0.56 11 9 45   0.06  10.33  
SK90-3.20 0.61 13 7 52  0.93 13 19 75  0.95 13 19 75   0.95  ∞ 
SK90-3.21 0.36 13 3 27  0.57 13 7 43  0.54 13 7 43   0.02  0.02  
SK90-3.22 ∞ ∞ ∞  3.20  5.65  
SK90-3.23 0.64 18 12 42  0.80 19 16 48  0.74 19 16 48   92.83  0.11  
SK90-3.24 0.09 5 3 8  0.10 5 3 8  0.07 5 3 8   0.01  0.01  
SK90-3.25 0.05 3 1 4  0.04 3 1 4  0.04 3 1 4   0.30  0.00  
SK90-3.26 ∞ ∞ ∞  ∞ ⊥ 
SK90-3.27 5.64 28 0 76  23.37 39 5 136  23.92 39 5 136   17.71  0.39  
SK90-3.28 130.67 118 2 1293  74.29 37 131 2208  86.09 37 133 2224   15.93  ⊥ 
SK90-3.29 1.49 14 33 106  2.21 13 47 134  2.06 13 47 134   0.54  ⊥ 
SK90-3.30 0.06 6 0 4  0.08 6 0 4  0.04 6 0 4   0.01  0.01  
SK90-3.31 0.05 4 1 4  0.09 5 1 6  0.04 4 1 4   0.00  0.01  
SK90-3.32 0.05 5 0 4  0.06 5 0 4  0.03 5 0 4   0.00  0.00  
SK90-3.33 0.08 6 0 5  0.09 6 0 5  0.04 6 0 5   0.00  0.00  
slothrop-ackermann 0.07 4 1 6  ⊥ 0.07 4 2 6   0.00  ⊥ 
slothrop-cge ⊥ ⊥ ⊥  ∞ ∞ 
slothrop-cge3 ⊥ ⊥ ⊥  ∞ ∞ 
slothrop-endo 5.46 70 0 105  ∞ ∞  0.46  0.28  
slothrop-equiv_proofs ⊥ ⊥ ⊥  ⊥ ⊥ 
slothrop-fgh 0.05 6 0 3  0.06 6 0 3  0.03 6 0 3   0.00  0.01  
slothrop-groups 0.54 21 0 23  3.75 40 0 63  3.92 40 0 63   0.05  0.07  
slothrop-groups_conj 0.20 11 0 12  0.24 11 1 15  0.22 11 1 15   0.02  0.83  
slothrop-hard 0.03 3 1 3  0.04 3 1 3  0.03 3 1 3   0.00  0.02  
slothrop-nlp-2b ∞ ∞ ∞  ⊥ ⊥ 
TPTP-BOO027-1_theory 0.10 6 0 6  0.11 6 0 6  0.08 6 0 6   0.01  0.01  
TPTP-COL053-1_theory 0.02 2 0 2  0.03 2 1 2  0.03 2 1 2   0.00  0.00  
TPTP-COL056-1_theory 0.10 4 2 10  0.12 4 5 10  0.12 4 5 10   0.00  0.55  
TPTP-COL060-1_theory ⊥ 0.05 3 0 4  0.05 3 0 4   ⊥ 0.00  
TPTP-COL085-1_theory 0.01 2 0 1  0.02 2 0 1  0.01 2 0 1   0.00  0.00  
TPTP-GRP010-4_theory 1.58 32 6 81  1.66 32 9 81  1.50 32 9 81   0.20  0.08  
TPTP-GRP011-4_theory 0.47 18 0 23  0.49 18 1 23  0.42 18 1 23   0.06  0.07  
TPTP-GRP012-4_theory 0.29 13 0 14  0.30 13 1 14  0.24 13 1 14   0.02  0.02  
TPTP-GRP393-2_theory 0.03 2 0 2  0.03 2 0 2  0.04 2 0 2   0.00  0.00  
TPTP-GRP394-3_theory 0.33 15 0 17  0.37 15 1 17  0.28 15 1 17   0.04  0.05  
TPTP-GRP454-1_theory 16.57 170 0 271  3.14 41 12 120  3.39 41 12 120   2.04  0.09  
TPTP-GRP457-1_theory 16.18 170 0 271  3.15 41 12 120  3.37 41 12 120   2.04  1.20  
TPTP-GRP460-1_theory 12.52 131 4 187  33.74 129 10 391  29.87 119 11 342   0.69  2.29  
TPTP-GRP463-1_theory 12.10 131 4 187  34.54 129 10 391  29.98 119 11 342   1.41  2.55  
TPTP-GRP481-1_theory 49.32 263 0 401  13.77 105 8 209  13.99 104 9 212   1.87  49.39  
TPTP-GRP484-1_theory 102.07 399 0 625  70.90 221 35 920  77.43 221 35 920   0.38  10.72  
TPTP-GRP487-1_theory ∞ 59.21 183 0 810  64.31 183 0 810   0.76  5.57  
TPTP-GRP490-1_theory 74.59 326 4 503  52.04 162 35 630  57.03 162 35 630   0.63  10.39  
TPTP-GRP493-1_theory ∞ 37.49 150 0 327  39.68 150 0 327   4.19  2.18  
TPTP-GRP496-1_theory 65.96 326 0 474  59.66 196 28 613  56.55 190 24 579   0.70  8.88  
TPTP-HWC004-1_theory 0.30 11 2 16  0.32 11 2 16  0.24 11 2 16   0.02  0.01  
TPTP-HWC004-2_theory 0.16 7 2 12  0.16 7 2 12  0.13 7 2 12   0.00  0.01  
TPTP-SWV262-2_theory 0.08 4 3 7  0.09 4 3 7  0.06 4 3 7   0.02  0.03  
WS06-proofreduction ⊥ ∞ ∞  ⊥ ∞ 
successes 69 67 74  77 61 
average time 13.82 19.11 17.32  3.55 8.56 

Explanation:
(1) total time
(2) control loop iterations
(3) processes
(4) termination checks