mkbTT experiments

  LPO KBO TKBO LPO+KBO TOTAL1 TOTAL2 
  (1)(2)(3)(4) (1)(2)(3)(4) (1)(2)(3)(4) (1)(2)(3)(4) (1)(2)(3)(4) (1)(2)(3)(4) 
AD93-Z22 ∞ ∞ ∞ ∞ ∞ ∞ 
ASK93-1 0.06 4 1 5  0.08 4 1 5  0.11 4 1 5  0.10 4 1 5  0.19 4 1 5  0.22 4 1 5  
ASK93-2 ∞ ∞ ∞ ∞ ∞ ∞ 
ASK93-5 ∞ ∞ ∞ ∞ ∞ ∞ 
ASK93-6 21.95 17 402 915  27.57 17 402 915  208.22 19 377 937  32.40 17 402 915  95.60 17 402 915  101.56 17 402 915  
BD94-collapse 0.13 8 3 12  0.15 8 3 12  0.18 8 3 12  0.22 8 3 12  0.15 8 3 12  0.28 8 3 12  
BD94-peano 0.09 5 2 8  ∞ ∞ 0.14 5 3 8  0.11 5 3 8  0.17 5 3 8  
BD94-sqrt 0.06 5 0 4  0.06 5 0 4  0.09 5 0 4  0.11 5 0 4  0.07 5 0 4  0.13 5 0 4  
BGK94-D08 131.47 229 6 844  17.62 82 33 515  298.90 141 32 1484  41.66 141 0 724  ∞ ∞ 
BGK94-D10 252.81 206 3 789  18.58 88 7 549  91.67 110 16 587  35.18 106 13 763  261.30 76 3 580  233.46 80 5 596  
BGK94-D12 ∞ 18.76 88 9 549  ∞ 34.65 105 13 755  ∞ 262.05 79 12 631  
BGK94-D16 ∞ 19.90 88 13 559  63.65 94 16 518  44.59 119 13 808  ∞ 232.88 81 4 607  
BGK94-M08 ∞ ∞ ∞ ∞ ∞ ∞ 
BGK94-M10 ∞ ∞ ∞ ∞ ∞ ∞ 
BGK94-M12 ∞ ∞ ∞ ∞ ∞ ∞ 
BGK94-M14 ∞ ∞ ∞ ∞ ∞ ∞ 
BGK94-Z22W ∞ ∞ ∞ ∞ ∞ ∞ 
BH96-fac8_theory 0.32 7 10 30  0.92 14 8 84  7.07 14 12 108  0.55 7 12 34  1.17 7 14 34  1.11 7 14 34  
Chr89-A2 7.12 59 5 179  185.24 149 1 599  95.63 118 2 709  ∞ 125.05 102 4 435  71.73 102 4 435  
Chr89-A24 ∞ ∞ ∞ ∞ ∞ ∞ 
Chr89-A3 ∞ 105.86 223 1 1263  ∞ 244.94 80 301 2554  ∞ ∞ 
HR94-1 ∞ ∞ ∞ ∞ ∞ ∞ 
HR94-2 ∞ ∞ ∞ ∞ ∞ ∞ 
KH11-aufgabe3-2 0.02 2 1 2  0.03 2 1 2  0.03 2 1 2  0.04 2 1 2  0.03 2 1 2  0.04 2 1 2  
KH11-aufgabe3-3 0.04 4 0 3  0.04 4 0 3  0.04 4 0 3  0.07 4 0 3  0.04 4 0 3  0.08 4 0 3  
KH11-fggx 0.07 5 1 6  0.09 5 2 6  0.11 5 2 6  0.13 5 2 6  0.09 5 2 6  0.15 5 2 6  
KH11-fib 1.76 11 41 135  ∞ ∞ 2.56 11 45 139  18.01 11 55 141  15.73 11 55 141  
KH11-kb-fail 0.05 5 0 3  0.05 5 0 3  0.05 5 0 3  0.08 5 0 3  0.05 5 0 3  0.09 5 0 3  
KH11-kb-fail1 0.07 5 1 5  0.06 5 1 5  0.07 5 1 5  0.10 5 1 5  0.08 5 1 5  0.12 5 1 5  
KH11-lr-theory 0.84 20 1 31  1.15 23 4 44  6.74 37 9 92  3.93 37 9 92  15.84 37 9 92  7.45 37 9 92  
KH11-rl-theory 4.26 38 1 55  244.91 91 0 246  293.17 118 0 358  4.47 38 8 100  19.51 38 8 100  10.53 38 9 100  
KK99-linear_assoc 0.05 3 1 4  0.05 3 1 4  0.16 3 3 6  0.10 3 3 6  0.21 3 3 6  0.12 3 3 6  
Les83-fib 0.29 10 2 24  ∞ ∞ 0.64 10 6 34  4.02 10 8 36  3.57 10 8 36  
Les83-subset 0.36 13 5 27  ∞ ∞ 0.55 13 5 27  0.80 13 5 27  1.13 13 5 27  
LS06-CGE4 ∞ ∞ ∞ ∞ ∞ ∞ 
LS06-CGE5 ∞ ∞ ∞ ∞ ∞ ∞ 
LS94-G0 0.48 19 1 27  0.52 19 3 27  2.20 23 5 47  1.17 23 7 47  8.84 23 7 47  3.14 23 7 47  
LS94-G1 ∞ ∞ ∞ ∞ ∞ ∞ 
LS94-G2 ∞ ∞ ∞ ∞ ∞ ∞ 
LS94-G3 ∞ ∞ ∞ ∞ ∞ ∞ 
LS94-P1 ∞ ∞ ∞ ∞ ∞ ∞ 
OKW95-dt1_theory 1.54 18 22 134  ∞ ∞ 2.64 18 29 148  16.95 18 36 148  16.02 18 36 148  
Sim91-sims2 ∞ ∞ ∞ ∞ ∞ ∞ 
SK90-3.01 0.75 22 2 40  0.96 23 7 47  7.74 43 15 139  5.28 43 19 169  32.54 43 19 169  11.27 43 19 169  
SK90-3.02 0.08 4 1 7  0.09 4 1 7  0.18 4 1 7  0.13 4 1 7  0.40 4 1 7  0.16 4 1 7  
SK90-3.03 3.47 44 3 76  11.60 52 14 193  18.41 47 19 200  ∞ 153.23 72 23 363  122.69 72 23 363  
SK90-3.04 0.76 17 1 39  ∞ 7.41 43 11 125  2.73 34 4 86  33.57 43 11 125  28.48 43 11 125  
SK90-3.05 13.57 55 1 118  4.14 52 1 107  36.36 74 6 255  14.95 55 1 118  104.20 75 10 338  65.86 73 6 249  
SK90-3.06 ∞ ∞ ∞ ∞ ∞ ∞ 
SK90-3.07 ∞ ∞ ∞ ∞ ∞ ∞ 
SK90-3.08 0.14 9 2 10  0.15 9 2 10  0.16 9 2 10  0.22 9 2 10  0.14 9 2 10  0.27 9 2 10  
SK90-3.09 ∞ ∞ ∞ ∞ ∞ ∞ 
SK90-3.10 0.11 9 0 8  0.12 9 0 8  0.12 9 0 8  0.20 9 0 8  0.12 9 0 8  0.24 9 0 8  
SK90-3.11 0.09 7 0 7  0.10 7 0 7  0.11 7 0 7  0.17 7 0 7  0.24 7 0 7  0.32 7 0 7  
SK90-3.12 0.24 12 0 12  0.31 13 1 15  0.51 13 1 15  0.45 13 1 15  0.74 13 1 15  0.83 13 1 15  
SK90-3.13 0.34 10 3 30  0.35 10 3 30  1.11 7 11 33  0.43 7 7 25  3.50 7 15 33  3.12 7 15 33  
SK90-3.14 0.34 10 5 30  0.42 10 9 34  1.08 10 9 34  0.67 10 9 34  0.43 10 9 34  0.70 10 9 34  
SK90-3.15 ∞ 0.25 11 2 16  0.46 11 3 16  0.37 11 3 16  0.67 11 3 16  0.87 11 3 16  
SK90-3.16 0.07 6 0 5  0.08 6 0 5  0.11 6 0 5  0.13 6 0 5  0.08 6 0 5  0.16 6 0 5  
SK90-3.17 0.10 6 1 8  0.11 6 1 10  0.26 6 3 10  0.20 6 2 10  0.47 6 4 10  0.76 6 4 10  
SK90-3.18 0.31 12 2 24  ∞ 1.64 12 7 35  0.72 12 7 35  3.15 12 8 35  3.01 12 8 35  
SK90-3.19 0.51 11 5 43  0.57 11 9 45  3.53 11 25 81  1.26 11 19 65  16.90 11 31 89  13.94 11 33 89  
SK90-3.20 0.60 13 7 52  0.92 13 19 75  4.58 13 31 90  1.45 13 23 80  8.33 13 31 90  7.89 13 31 90  
SK90-3.21 0.38 13 3 27  0.58 13 7 43  1.43 13 7 43  0.91 13 7 43  0.58 13 7 43  0.94 13 7 43  
SK90-3.22 ∞ ∞ ∞ ∞ ∞ ∞ 
SK90-3.23 0.68 18 12 42  0.87 19 16 48  1.90 19 16 48  1.13 19 16 48  1.64 19 16 48  1.99 19 16 48  
SK90-3.24 0.10 5 3 8  0.10 5 3 8  0.12 5 3 8  0.15 5 3 8  0.10 5 3 8  0.20 5 3 8  
SK90-3.25 0.05 3 1 4  0.05 3 1 4  0.10 3 1 4  0.07 3 1 4  0.12 3 1 4  0.11 3 1 4  
SK90-3.26 ∞ ∞ ∞ ∞ ∞ ∞ 
SK90-3.27 5.47 23 0 68  21.15 28 2 121  18.21 25 0 82  23.05 28 2 121  66.25 28 2 121  48.49 28 2 121  
SK90-3.28 130.79 111 2 1330  75.22 37 133 2226  ∞ 101.67 37 135 2242  ∞ ∞ 
SK90-3.29 1.53 14 33 106  2.22 13 47 134  13.07 15 51 168  3.14 13 47 134  29.32 15 51 168  20.59 15 51 168  
SK90-3.30 0.07 6 0 4  0.07 6 0 4  0.11 6 0 4  0.11 6 0 4  0.07 6 0 4  0.14 6 0 4  
SK90-3.31 0.05 4 1 4  0.08 5 1 6  0.12 4 1 4  0.09 4 1 4  0.06 4 1 4  0.11 4 1 4  
SK90-3.32 0.05 5 0 4  0.06 5 0 4  0.06 5 0 4  0.09 5 0 4  0.06 5 0 4  0.11 5 0 4  
SK90-3.33 0.07 6 0 5  0.08 6 0 5  0.08 6 0 5  0.11 6 0 5  0.07 6 0 5  0.15 6 0 5  
slothrop-ackermann 0.07 4 1 6  ∞ ∞ 0.15 4 3 8  0.33 4 3 8  0.23 4 3 8  
slothrop-cge ∞ ∞ ∞ ∞ ∞ ∞ 
slothrop-cge3 ∞ ∞ ∞ ∞ ∞ ∞ 
slothrop-endo 9.41 70 0 105  ∞ ∞ 3.33 30 10 111  34.44 31 19 135  24.46 31 19 135  
slothrop-equiv_proofs ∞ ∞ ∞ ∞ ∞ ∞ 
slothrop-equiv_proofs_or ∞ ∞ ∞ ∞ ∞ ∞ 
slothrop-fgh 0.05 6 0 3  0.06 6 0 3  0.06 6 0 3  0.09 6 0 3  0.05 6 0 3  0.10 6 0 3  
slothrop-groups 0.64 21 0 23  7.81 40 0 63  10.87 41 0 81  0.99 21 3 35  3.90 21 3 35  1.56 21 3 35  
slothrop-groups_conj 0.22 11 0 12  0.26 11 1 16  0.59 11 2 19  0.59 13 3 26  2.10 13 3 26  0.69 13 3 26  
slothrop-hard 0.03 3 1 3  0.04 3 1 3  0.05 3 1 3  0.06 3 1 3  0.04 3 1 3  0.07 3 1 3  
slothrop-nlp-2b ∞ ∞ ∞ ∞ ∞ ∞ 
TPDB-AProVE_07_thiemann27 ∞ ∞ ∞ ∞ ∞ ∞ 
TPDB-secr10 9.60 53 3 131  270.60 127 25 646  ∞ 278.96 127 25 646  ∞ ∞ 
TPDB-secr4 17.54 74 31 318  12.67 52 24 307  33.44 61 5 351  15.13 53 25 307  76.27 64 31 351  72.96 62 30 349  
TPDB-z115 ∞ 51.92 43 115 690  65.02 42 83 530  57.63 43 115 690  228.50 49 124 935  194.43 44 118 787  
TPTP-BOO027-1_theory 0.10 6 0 6  0.10 6 0 6  0.23 6 0 6  0.16 6 0 6  0.18 6 0 6  0.24 6 0 6  
TPTP-COL053-1_theory 0.02 2 0 2  0.03 2 1 2  0.04 2 1 2  0.04 2 1 2  0.03 2 1 2  0.04 2 1 2  
TPTP-COL056-1_theory 0.11 4 2 10  0.11 4 5 10  0.21 4 5 10  0.19 4 5 10  0.12 4 5 10  0.21 4 5 10  
TPTP-COL060-1_theory ∞ 0.05 3 0 4  0.10 3 0 4  0.07 3 0 4  0.22 3 0 4  0.21 3 0 4  
TPTP-COL085-1_theory 0.01 2 0 1  0.02 2 0 1  0.02 2 0 1  0.03 2 0 1  0.02 2 0 1  0.03 2 0 1  
TPTP-COL086-1_theory 0.02 2 0 1  0.02 2 0 1  0.02 2 0 1  0.03 2 0 1  0.02 2 0 1  0.04 2 0 1  
TPTP-GRP010-4_theory 2.58 46 5 98  2.52 46 8 98  13.54 61 15 202  9.00 69 23 257  53.51 67 26 257  28.94 68 25 255  
TPTP-GRP011-4_theory 0.51 18 0 23  0.54 18 1 23  2.91 27 2 46  1.41 27 3 46  9.10 27 3 46  4.30 27 3 46  
TPTP-GRP012-4_theory 0.30 13 0 14  0.32 13 1 14  0.94 17 2 22  0.71 17 3 22  2.30 17 3 22  0.81 17 3 22  
TPTP-GRP192-1_theory 4.96 52 1 75  5.07 53 0 71  30.85 71 7 448  14.30 71 2 134  165.45 70 8 438  172.61 70 8 438  
TPTP-GRP393-2_theory 0.03 2 0 2  0.02 2 0 2  0.04 2 1 2  0.04 2 1 2  0.07 2 1 2  0.05 2 1 2  
TPTP-GRP394-3_theory 0.37 15 0 17  0.40 15 1 17  1.45 21 2 35  0.99 21 3 35  4.66 21 3 35  1.70 21 3 35  
TPTP-GRP430-1_theory ∞ ∞ ∞ ∞ ∞ ∞ 
TPTP-GRP433-1_theory ∞ ∞ ∞ ∞ ∞ ∞ 
TPTP-GRP434-1_theory ∞ ∞ ∞ ∞ ∞ ∞ 
TPTP-GRP442-1_theory ∞ ∞ ∞ ∞ ∞ ∞ 
TPTP-GRP445-1_theory ∞ 5.75 52 2 62  11.40 52 2 62  5.48 48 2 58  12.98 52 2 62  11.66 48 2 58  
TPTP-GRP447-1_theory ∞ 5.87 52 2 62  11.28 52 2 62  5.53 48 2 58  12.86 52 2 62  11.66 48 2 58  
TPTP-GRP451-1_theory ∞ ∞ 122.15 141 5 292  ∞ ∞ ∞ 
TPTP-GRP452-1_theory ∞ ∞ 122.64 141 5 292  ∞ ∞ ∞ 
TPTP-GRP454-1_theory 4.38 59 4 112  2.52 33 12 85  4.15 33 12 85  3.03 33 12 85  7.22 33 12 85  7.01 33 12 85  
TPTP-GRP457-1_theory 4.47 59 4 112  2.56 33 12 85  4.15 33 12 85  3.12 33 12 85  7.24 33 12 85  6.96 33 12 85  
TPTP-GRP458-1_theory 4.30 59 4 111  2.44 33 12 84  4.14 33 12 84  3.25 33 12 84  6.93 33 12 84  6.67 33 12 84  
TPTP-GRP460-1_theory 20.32 98 0 156  8.99 84 15 160  14.82 85 16 163  11.00 85 16 163  18.90 85 16 163  19.98 85 16 163  
TPTP-GRP461-1_theory 20.46 98 0 155  8.89 84 15 159  14.98 85 16 162  11.35 85 16 162  18.46 85 16 162  19.55 85 16 162  
TPTP-GRP463-1_theory 20.45 98 0 156  8.97 84 15 160  14.79 85 16 163  11.29 85 16 163  18.83 85 16 163  19.66 85 16 163  
TPTP-GRP466-1_theory ∞ ∞ ∞ ∞ ∞ ∞ 
TPTP-GRP472-1_theory ∞ ∞ ∞ ∞ ∞ ∞ 
TPTP-GRP478-1_theory ∞ ∞ ∞ ∞ ∞ ∞ 
TPTP-GRP481-1_theory 26.31 122 0 201  11.93 86 11 179  ∞ 16.81 89 11 197  25.13 87 15 186  34.15 90 15 204  
TPTP-GRP482-1_theory 25.29 122 0 201  11.80 86 11 179  ∞ 16.39 89 11 197  24.92 87 15 186  34.00 90 15 204  
TPTP-GRP484-1_theory 21.68 129 0 205  74.71 174 18 471  ∞ 105.65 183 27 541  ∞ ∞ 
TPTP-GRP486-1_theory 21.32 129 0 205  74.84 174 18 471  ∞ 107.15 183 27 541  ∞ ∞ 
TPTP-GRP487-1_theory 59.49 177 0 252  80.65 200 1 978  ∞ 94.98 203 3 995  ∞ ∞ 
TPTP-GRP490-1_theory 254.96 236 0 373  71.98 183 35 611  ∞ 98.17 203 34 674  ∞ ∞ 
TPTP-GRP493-1_theory ∞ 41.22 140 0 253  ∞ 54.62 147 1 305  151.06 143 0 310  168.02 147 1 338  
TPTP-GRP496-1_theory 78.39 214 0 343  93.58 206 30 743  ∞ 83.68 187 23 552  ∞ 266.72 176 32 664  
TPTP-GRP499-1_theory ∞ ∞ ∞ ∞ ∞ ∞ 
TPTP-HWC004-1_theory 0.31 11 2 16  0.33 11 2 16  0.39 11 2 16  0.41 11 2 16  0.34 11 2 16  0.52 11 2 16  
TPTP-HWC004-2_theory 0.17 7 2 12  0.16 7 2 12  0.22 7 2 12  0.24 7 2 12  0.18 7 2 12  0.27 7 2 12  
TPTP-LCL407-2_theory 5.11 51 9 153  8.17 72 7 181  15.79 69 9 189  11.86 71 13 232  39.03 54 16 216  35.09 54 16 216  
TPTP-SWV243-2_theory 0.08 4 1 7  ∞ 0.30 4 1 7  0.14 4 1 7  1.01 4 1 7  0.71 4 1 7  
TPTP-SWV262-2_theory 0.09 4 3 7  0.10 4 3 7  0.23 4 3 7  0.13 4 3 7  0.09 4 3 7  0.15 4 3 7  
TPTP-SYN080-1_theory 0.01 2 0 0  0.01 2 0 0  0.01 2 0 0  0.01 2 0 0  0.01 2 0 0  0.01 2 0 0  
TPTP-SYN083-1_theory 0.02 2 0 2  0.03 2 0 2  0.04 2 1 2  0.04 2 1 2  0.07 2 1 2  0.05 2 1 2  
TPTP-SYN305-1_theory 0.00 1 0 0  0.00 1 0 0  0.00 1 0 0  0.00 1 0 0  0.00 1 0 0  0.00 1 0 0  
WS06-proofreduction ∞ ∞ ∞ ∞ ∞ ∞ 
successes 89 88 81 96 87 90 
average time 13.47 18.53 20.85 17.07 22.43 27.13 

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