mkbTT experiments

View:
  MAX SUM SLOTHROP SIZE/AGE OLD MAX' 
  (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.07 4 2 5  0.07 4 2 5  0.08 4 2 5  0.07 4 2 5  0.07 4 2 5  0.06 4 2 5  
ASK93-2 ∞ ∞ ∞ ∞ ∞ ∞ 
ASK93-5 ∞ ∞ ∞ ∞ ∞ ∞ 
ASK93-6 37.82 17 402 915  29.52 17 338 757  ∞ ∞ 109.28 21 627 1575  32.21 17 288 737  
BD94-collapse 0.11 8 3 12  0.10 8 3 12  0.12 10 3 14  0.10 9 3 12  0.11 8 3 12  0.11 8 3 12  
BD94-peano 0.10 5 3 8  0.10 5 3 8  0.13 5 3 9  0.20 7 2 12  0.11 5 3 8  0.10 5 3 8  
BD94-sqrt 0.03 5 0 4  0.03 5 0 4  0.03 5 0 4  0.03 5 0 4  0.03 5 0 4  0.03 5 0 4  
BGK94-D08 127.63 96 72 1716  217.03 205 21 2379  ∞ ∞ 373.34 156 71 2088  ∞ 
BGK94-D10 37.82 95 2 711  102.68 107 34 1443  ∞ ∞ 176.23 136 1 1318  96.24 137 19 1060  
BGK94-D12 39.59 95 11 725  133.67 110 103 1708  ∞ ∞ 254.03 158 19 1383  116.69 139 51 1239  
BGK94-D16 41.32 96 11 733  175.62 117 123 1971  ∞ ∞ ∞ 174.21 152 57 1705  
BGK94-M08 ∞ ∞ 397.12 122 13 324  ∞ ∞ 21.68 22 9 30  
BGK94-M10 ∞ ∞ ∞ ∞ ∞ ∞ 
BGK94-M12 ∞ ∞ ∞ ∞ ∞ ∞ 
BGK94-M14 ∞ ∞ ∞ ∞ ∞ ∞ 
BGK94-Z22W ∞ ∞ ∞ ∞ ∞ ∞ 
BH96-fac8_theory 0.36 7 15 34  0.34 7 15 32  0.38 7 15 33  0.57 9 27 56  0.34 7 15 32  0.35 7 15 32  
Chr89-A2 38.34 108 1 444  96.78 137 2 629  ∞ ∞ 74.33 97 13 349  300.94 272 5 807  
Chr89-A24 ∞ ∞ ∞ ∞ ∞ ∞ 
Chr89-A3 170.05 69 80 1664  ∞ ∞ ∞ ∞ ∞ 
HR94-1 ∞ ∞ ∞ ∞ ∞ ∞ 
HR94-2 ∞ ∞ ∞ ∞ ∞ ∞ 
KH11-aufgabe3-2 0.02 2 1 2  0.02 2 1 2  0.02 2 1 2  0.02 2 1 2  0.02 2 1 2  0.02 2 1 2  
KH11-aufgabe3-3 0.03 4 0 3  0.02 4 0 3  0.03 4 0 3  0.03 4 0 3  0.03 4 0 3  0.03 4 0 3  
KH11-fggx 0.08 5 2 6  0.08 5 2 6  0.05 4 1 4  0.06 5 1 5  0.05 4 1 4  0.07 5 2 6  
KH11-fib 2.98 13 49 157  2.32 13 49 127  5.29 11 83 255  4.44 14 66 225  2.35 12 45 125  2.22 11 45 117  
KH11-kb-fail ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 
KH11-kb-fail1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 
KH11-lr-theory 4.97 37 8 92  3.66 37 6 65  ∞ ∞ 290.00 117 7 425  3.65 36 6 62  
KH11-rl-theory ∞ 4.13 39 5 72  ∞ 21.50 87 4 150  ∞ 4.48 40 5 72  
KK99-linear_assoc 0.11 3 3 6  0.10 3 3 6  0.10 3 3 6  0.11 3 3 6  0.12 3 3 6  0.10 3 3 6  
Les83-fib 0.69 10 14 38  0.66 10 14 36  1.19 10 14 63  0.75 12 9 36  0.66 10 14 36  0.66 10 14 36  
Les83-subset 0.38 13 5 27  0.38 13 5 27  0.60 15 5 32  0.37 13 5 27  0.37 13 5 27  0.37 13 5 27  
LS06-CGE4 ∞ ⊥ ∞ ∞ ⊥ ⊥ 
LS06-CGE5 ∞ ∞ ∞ ∞ ∞ ∞ 
LS94-G0 1.64 23 7 47  3.05 30 7 74  20.98 56 7 98  6.02 38 7 81  6.75 38 7 79  3.69 31 7 82  
LS94-G1 ∞ ∞ ∞ ∞ ∞ ∞ 
LS94-G2 ∞ ∞ ∞ ∞ ∞ ∞ 
LS94-G3 ∞ ∞ ∞ ∞ ∞ ∞ 
LS94-P1 ∞ ∞ ∞ ∞ ∞ ∞ 
OKW95-dt1_theory 3.15 18 55 154  3.56 19 63 170  3.22 12 31 161  3.34 17 39 175  3.66 17 39 184  3.67 19 63 172  
Sim91-sims2 ∞ ∞ ∞ ∞ ∞ ∞ 
SK90-3.01 6.53 44 17 153  7.81 59 17 139  90.95 102 12 325  20.86 96 3 154  3.30 30 4 69  10.71 66 17 147  
SK90-3.02 0.11 4 1 7  0.10 4 1 7  0.10 4 1 7  0.26 6 2 13  0.10 4 1 7  0.10 4 1 7  
SK90-3.03 40.16 69 18 284  2.83 36 5 57  90.23 53 4 134  6.75 48 8 100  ∞ 2.66 38 5 56  
SK90-3.04 4.53 40 5 103  87.79 132 5 348  69.38 76 5 248  177.60 198 3 394  50.30 89 4 269  118.02 145 5 360  
SK90-3.05 38.39 98 12 371  11.03 59 6 142  ∞ ⊥ 217.81 97 10 356  11.00 58 6 138  
SK90-3.06 15.76 71 11 306  ∞ ∞ ∞ ⊥ ∞ 
SK90-3.07 108.70 161 17 688  ∞ ∞ ∞ ∞ ∞ 
SK90-3.08 0.12 9 2 10  0.23 14 2 17  0.29 15 2 18  0.16 12 2 13  0.17 12 2 13  0.18 12 2 13  
SK90-3.09 ∞ ∞ ∞ ∞ ∞ ∞ 
SK90-3.10 0.06 9 0 8  0.06 9 0 8  0.07 9 0 8  0.06 9 0 8  0.07 9 0 8  0.06 9 0 8  
SK90-3.11 0.08 7 0 7  0.08 7 0 7  0.29 9 3 19  0.08 7 0 7  0.08 7 0 7  0.08 7 0 7  
SK90-3.12 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 
SK90-3.13 0.50 7 15 33  0.57 8 15 37  0.56 7 15 36  0.89 10 19 50  0.60 8 15 38  0.56 8 15 37  
SK90-3.14 0.50 10 9 34  0.47 10 9 31  0.43 9 7 28  0.71 16 9 47  0.50 10 9 31  0.48 10 9 31  
SK90-3.15 0.27 11 3 16  0.29 11 3 16  0.31 11 3 16  0.32 12 3 17  0.29 11 3 16  0.28 11 3 16  
SK90-3.16 0.04 6 0 5  0.04 6 0 5  0.04 6 0 5  0.04 6 0 5  0.04 6 0 5  0.04 6 0 5  
SK90-3.17 0.21 6 4 10  0.27 7 4 11  0.32 7 4 13  0.23 6 4 12  0.30 7 4 13  0.20 6 4 10  
SK90-3.18 0.86 12 10 35  0.87 12 10 35  0.99 12 7 41  1.19 15 6 47  0.85 12 10 35  0.87 12 10 35  
SK90-3.19 2.11 11 35 89  0.90 12 19 47  1.96 10 31 91  1.43 14 27 69  0.75 11 15 39  1.97 14 27 87  
SK90-3.20 1.34 13 31 90  1.52 13 31 95  2.22 12 31 113  1.51 15 31 97  1.29 12 31 79  1.29 13 31 80  
SK90-3.21 0.64 13 7 43  0.56 13 7 37  16.26 72 0 257  1.96 21 19 96  1.71 16 15 76  0.59 13 7 37  
SK90-3.22 ∞ ∞ ∞ 49.25 99 0 285  ∞ ∞ 
SK90-3.23 1.09 19 16 48  1.29 22 18 51  1.54 23 16 51  1.10 24 15 42  2.05 27 19 66  1.38 21 19 52  
SK90-3.24 0.10 5 3 8  0.09 5 3 8  0.12 6 2 7  0.09 6 3 7  0.08 5 3 7  0.08 5 3 7  
SK90-3.25 0.08 3 1 4  0.08 3 1 4  0.09 3 1 4  0.08 3 1 4  0.08 3 1 4  0.08 3 1 4  
SK90-3.26 ∞ ∞ ∞ ∞ ∞ ∞ 
SK90-3.27 68.57 40 4 155  255.45 73 7 320  343.36 69 1 460  467.75 57 10 332  29.22 33 2 139  473.74 106 10 381  
SK90-3.28 221.65 42 122 2410  135.17 43 51 1988  ∞ 452.37 124 65 2598  ∞ ∞ 
SK90-3.29 3.87 15 69 170  3.66 16 44 176  4.85 15 64 154  5.90 24 57 232  5.68 18 54 232  6.12 18 54 230  
SK90-3.30 0.05 6 0 4  0.05 6 0 4  0.05 6 0 4  0.05 6 0 4  0.05 6 0 4  0.05 6 0 4  
SK90-3.31 0.04 4 1 4  0.05 4 1 5  0.04 4 1 4  0.05 4 1 5  0.05 4 1 5  0.04 4 1 5  
SK90-3.32 0.03 5 0 4  0.03 5 0 4  0.04 5 0 4  0.03 5 0 4  0.03 5 0 4  0.03 5 0 4  
SK90-3.33 0.05 6 0 5  0.04 5 0 4  0.04 6 0 5  0.03 5 0 4  0.03 5 0 4  0.03 5 0 4  
slothrop-ackermann 0.11 4 4 8  0.12 4 4 8  0.12 4 4 8  0.20 6 6 14  0.14 5 5 10  0.12 4 4 8  
slothrop-cge 35.46 73 14 377  ⊥ ∞ 166.70 153 25 812  59.90 75 19 471  ⊥ 
slothrop-cge3 ⊥ ∞ ∞ ∞ 141.34 83 53 829  ⊥ 
slothrop-endo 4.75 30 13 116  4.22 33 10 117  ∞ 33.49 95 9 219  24.73 55 8 220  4.49 33 10 117  
slothrop-equiv_proofs 7.54 37 5 96  7.17 37 5 90  39.02 48 8 180  73.47 128 9 277  11.81 38 7 114  7.37 37 5 90  
slothrop-equiv_proofs_or 7.49 37 5 96  7.00 37 5 90  38.77 48 8 180  73.30 128 9 277  11.73 38 7 114  7.21 37 5 90  
slothrop-fgh 0.03 6 0 3  0.02 4 0 3  0.03 6 0 3  0.04 5 0 3  0.03 5 0 3  0.03 4 0 3  
slothrop-groups 1.16 21 3 35  1.32 25 3 34  20.97 67 0 96  8.44 50 3 73  4.81 37 3 63  1.43 25 3 38  
slothrop-groups_conj 0.64 13 3 25  0.69 15 3 24  1.05 14 3 34  0.79 15 3 25  0.52 12 3 22  0.69 15 3 24  
slothrop-hard 0.03 3 1 3  0.03 3 1 3  0.03 3 1 3  0.04 3 1 3  0.03 3 1 3  0.03 3 1 3  
slothrop-nlp-2b ∞ ∞ ∞ ∞ ∞ ∞ 
TPDB-AProVE_07_thiemann27 ∞ ∞ ∞ ∞ ∞ ∞ 
TPDB-secr10 446.22 169 20 573  9.45 29 8 134  134.40 66 26 486  105.80 91 18 379  14.78 33 10 171  10.76 33 8 136  
TPDB-secr4 22.02 52 26 308  11.69 30 27 193  67.40 63 6 543  18.79 61 7 240  48.35 83 2 431  13.76 32 33 177  
TPDB-z115 89.25 43 115 690  30.04 29 78 343  ∞ 291.71 132 43 1240  53.90 32 84 396  153.46 52 102 794  
TPTP-BOO027-1_theory 0.13 7 0 7  0.14 7 0 7  0.15 7 0 7  0.15 7 0 7  0.14 7 0 7  0.14 7 0 7  
TPTP-COL053-1_theory 0.04 2 1 2  0.03 2 1 2  0.03 2 1 2  0.03 2 1 2  0.04 2 1 2  0.04 2 1 2  
TPTP-COL056-1_theory 0.12 4 5 10  0.12 4 5 10  0.13 4 5 10  0.15 6 5 12  0.14 6 5 12  0.11 4 5 10  
TPTP-COL060-1_theory 0.07 3 0 4  0.07 3 0 4  0.07 3 0 4  0.07 3 0 4  0.07 3 0 4  0.07 3 0 4  
TPTP-COL085-1_theory 0.01 2 0 1  0.01 2 0 1  0.01 2 0 1  0.01 2 0 1  0.01 2 0 1  0.01 2 0 1  
TPTP-GRP010-4_theory 8.49 49 27 220  9.89 63 20 237  61.73 71 13 332  405.25 321 19 1670  52.53 89 24 366  29.40 83 37 445  
TPTP-GRP011-4_theory 2.45 26 6 77  2.26 32 4 53  63.63 81 5 248  273.43 170 13 699  6.19 39 6 92  2.34 32 4 53  
TPTP-GRP012-4_theory 0.81 17 3 22  1.36 22 3 33  15.26 46 3 57  3.53 33 3 46  2.67 27 3 35  1.56 23 3 37  
TPTP-GRP393-2_theory 0.04 2 1 2  0.04 2 1 2  0.04 2 1 2  0.05 2 1 2  0.04 2 1 2  0.04 2 1 2  
TPTP-GRP394-3_theory 1.17 21 3 35  1.58 28 3 39  15.68 56 2 81  7.40 47 3 66  2.88 29 3 42  1.59 28 3 39  
TPTP-GRP454-1_theory 6.18 41 12 123  207.87 220 12 693  ∞ ∞ ⊥ 166.33 199 31 1056  
TPTP-GRP457-1_theory 6.20 41 12 123  208.49 220 12 693  ∞ ∞ ∞ 164.88 199 31 1056  
TPTP-GRP460-1_theory ∞ 18.77 93 8 154  ∞ 50.90 117 6 381  93.08 113 11 209  38.08 117 7 235  
TPTP-GRP463-1_theory ∞ 18.82 93 8 154  ∞ ∞ 59.96 92 1 189  39.04 117 7 235  
TPTP-GRP481-1_theory 64.00 142 16 302  34.19 125 10 198  ∞ 341.48 191 7 341  438.78 256 2 520  38.64 130 9 185  
TPTP-GRP484-1_theory 204.49 249 3 1035  92.10 207 14 371  ∞ ∞ 350.52 164 0 282  107.72 201 13 350  
TPTP-GRP487-1_theory 123.42 197 33 764  137.04 235 27 795  ∞ ∞ ∞ 228.45 251 22 800  
TPTP-GRP490-1_theory 119.93 219 30 625  ∞ ∞ ∞ ∞ ∞ 
TPTP-GRP493-1_theory 152.35 241 0 483  56.13 129 0 234  ∞ 324.35 176 6 488  ∞ 190.70 230 0 348  
TPTP-GRP496-1_theory 121.25 209 21 588  ∞ ∞ ∞ ∞ ∞ 
TPTP-HWC004-1_theory 0.25 11 2 16  0.24 11 2 16  0.15 11 2 12  0.22 11 2 16  0.25 11 2 16  0.26 11 2 16  
TPTP-HWC004-2_theory 0.11 7 2 12  0.11 7 2 12  0.07 7 2 8  0.11 7 2 12  0.11 7 2 12  0.12 7 2 12  
TPTP-SWV262-2_theory 0.11 4 3 7  0.10 4 3 7  0.12 4 3 8  0.18 6 3 10  0.12 4 3 8  0.10 4 3 7  
WS06-proofreduction 238.79 91 31 763  233.97 94 30 737  ∞ ∞ 223.00 81 17 676  286.51 100 30 819  
successes 85 82 62 70 76 81 
average time 31.63 29.03 24.4 48.69 42.24 35.65 

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