mkbTT experiments

View:
  none PCP BCP MCP CCP 
  (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 7 /  0.07 7 0/2 0.00  0.07 7 0/2 0.00  0.08 7 0/2 0.00  0.07 7 0/2 0.00  
ASK93-2 ∞ ∞ ∞ ∞ ∞ 
ASK93-5 ∞ ∞ ∞ ∞ ∞ 
ASK93-6 39.64 98 /  39.64 98 0/18 0.01  39.25 98 0/18 0.00  39.57 98 0/18 0.01  39.88 98 0/18 0.02  
BD94-collapse 0.11 14 /  0.11 14 0/1 0.00  0.10 14 0/1 0.00  0.10 14 0/1 0.00  0.11 14 0/1 0.00  
BD94-peano 0.10 10 /  0.10 10 0/6 0.00  0.10 10 0/6 0.00  0.10 10 0/6 0.00  0.09 10 0/6 0.00  
BD94-sqrt 0.03 6 /  0.03 6 0/1 0.00  0.03 6 0/1 0.00  0.03 6 0/1 0.00  0.03 6 0/1 0.00  
BGK94-D08 121.59 2564 /  130.69 2520 13/1284 0.31  129.00 2534 13/1284 0.55  131.02 2485 13/1287 1.32  130.95 2564 7/1287 1.42  
BGK94-D10 123.42 4354 /  ∞ 463.04 7499 171/5178 1.71  38.37 1730 40/1071 0.53  38.61 1795 26/1083 0.59  
BGK94-D12 107.32 4145 /  ∞ ∞ 40.12 1864 40/1100 0.55  40.94 1927 26/1112 0.61  
BGK94-D16 128.02 4690 /  394.69 8650 127/4480 0.94  405.59 8867 117/4529 1.05  41.68 2028 40/1112 0.58  42.56 2091 26/1124 0.65  
BGK94-M08 ∞ ∞ ∞ ∞ ∞ 
BGK94-M10 ∞ ∞ ∞ ∞ ∞ 
BGK94-M12 ∞ ∞ ∞ ∞ ∞ 
BGK94-M14 ∞ ∞ ∞ ∞ ∞ 
BGK94-Z22W ∞ ∞ ∞ ∞ ∞ 
BH96-fac8_theory 0.36 16 /  0.37 16 0/8 0.00  0.35 16 0/8 0.00  0.38 16 0/8 0.00  0.35 16 0/8 0.00  
Chr89-A2 38.22 2480 /  38.40 2407 23/1810 0.20  38.60 2415 23/1804 0.26  38.84 2278 47/1834 0.77  38.74 2294 41/1830 0.87  
Chr89-A24 ∞ ∞ ∞ ∞ ∞ 
Chr89-A3 157.59 2203 /  164.39 2599 24/1051 0.39  163.62 2617 24/1050 0.65  171.20 2510 54/1058 1.15  166.80 2096 26/875 1.53  
HR94-1 ∞ ∞ ∞ ∞ ∞ 
HR94-2 ∞ ∞ ∞ ∞ ∞ 
KH11-aufgabe3-2 0.02 3 /  0.02 3 0/0 0.00  0.02 3 0/0 0.00  0.02 3 0/0 0.00  0.02 3 0/0 0.00  
KH11-aufgabe3-3 0.03 4 /  0.03 4 0/0 0.00  0.03 4 0/0 0.00  0.03 4 0/0 0.00  0.03 4 0/0 0.00  
KH11-fggx 0.08 11 /  0.09 11 0/3 0.00  0.08 11 0/3 0.00  0.09 11 0/3 0.00  0.08 11 0/3 0.00  
KH11-fib 3.00 131 /  3.03 131 0/30 0.00  3.01 131 0/30 0.00  3.02 124 0/30 0.01  2.98 124 0/30 0.01  
KH11-kb-fail ⊥ ⊥ ⊥ ⊥ ⊥ 
KH11-kb-fail1 ⊥ ⊥ ⊥ ⊥ ⊥ 
KH11-lr-theory 5.18 762 /  5.13 713 17/541 0.04  5.07 718 17/538 0.06  5.11 659 32/543 0.19  5.17 656 28/542 0.22  
KH11-rl-theory 429.91 21649 /  39.73 4626 91/2992 0.30  40.85 4691 79/2989 0.37  ∞ ∞ 
KK99-linear_assoc 0.10 14 /  0.10 14 0/6 0.00  0.10 14 0/6 0.00  0.10 14 0/6 0.00  0.11 14 0/6 0.00  
Les83-fib 0.70 53 /  0.69 52 0/25 0.00  0.70 52 0/25 0.00  0.71 50 0/25 0.00  0.69 50 0/25 0.00  
Les83-subset 0.37 30 /  0.36 30 0/8 0.00  0.37 30 0/8 0.00  0.37 30 0/8 0.00  0.37 30 0/8 0.00  
LS06-CGE4 ∞ ∞ ∞ ∞ ∞ 
LS06-CGE5 ∞ ∞ ∞ ∞ ∞ 
LS94-G0 1.64 245 /  1.67 236 7/151 0.01  1.65 238 7/151 0.01  1.65 231 15/152 0.03  1.66 231 15/152 0.04  
LS94-G1 ∞ ∞ ∞ ∞ ∞ 
LS94-G2 ∞ ∞ ∞ ∞ ∞ 
LS94-G3 ∞ ∞ ∞ ∞ ∞ 
LS94-P1 ∞ ∞ ∞ ∞ ∞ 
OKW95-dt1_theory 3.12 114 /  3.14 114 0/41 0.00  3.15 114 0/41 0.00  3.11 103 0/41 0.01  3.13 103 0/41 0.02  
Sim91-sims2 ∞ ∞ ∞ ∞ ∞ 
SK90-3.01 4.62 557 /  4.57 543 7/311 0.02  4.65 545 7/311 0.04  6.47 539 13/373 0.13  6.57 542 13/377 0.15  
SK90-3.02 0.11 16 /  0.10 16 0/6 0.00  0.10 16 0/6 0.00  0.10 16 0/6 0.00  0.11 16 0/6 0.00  
SK90-3.03 2.19 289 /  2.17 259 6/208 0.02  2.15 266 6/206 0.03  39.88 2925 23/1682 1.39  40.54 3004 20/1680 1.54  
SK90-3.04 4.51 574 /  4.58 554 13/471 0.03  4.61 554 13/471 0.05  4.49 494 63/475 0.13  4.61 507 63/475 0.14  
SK90-3.05 81.99 5025 /  76.46 4186 110/3589 0.55  76.10 4214 105/3519 0.69  38.46 1731 207/2032 2.01  37.24 1694 188/2015 2.18  
SK90-3.06 16.08 1597 /  15.97 1534 10/678 0.05  16.22 1539 10/677 0.08  15.90 1360 26/686 0.26  15.78 1366 25/685 0.28  
SK90-3.07 73.05 4531 /  89.79 5548 37/2807 0.32  90.57 5606 35/2798 0.46  109.31 5406 73/3719 3.67  107.81 5461 66/3722 3.87  
SK90-3.08 0.13 21 /  0.12 21 0/7 0.00  0.12 21 0/7 0.00  0.12 21 0/7 0.00  0.13 21 0/7 0.00  
SK90-3.09 ∞ ∞ ∞ ∞ ∞ 
SK90-3.10 0.06 8 /  0.07 8 0/4 0.00  0.06 8 0/4 0.00  0.06 8 0/4 0.00  0.06 8 0/4 0.00  
SK90-3.11 0.08 13 /  0.08 13 0/3 0.00  0.08 13 0/3 0.00  0.08 13 0/3 0.00  0.08 13 0/3 0.00  
SK90-3.12 ⊥ ⊥ ⊥ ⊥ ⊥ 
SK90-3.13 0.50 34 /  0.49 34 0/17 0.00  0.48 34 0/17 0.00  0.50 34 0/17 0.00  0.48 34 0/17 0.00  
SK90-3.14 0.51 41 /  0.49 41 0/21 0.00  0.49 41 0/21 0.00  0.51 41 0/21 0.00  0.50 41 0/21 0.00  
SK90-3.15 0.27 28 /  0.27 26 2/16 0.00  0.28 26 2/16 0.00  0.27 26 2/16 0.00  0.28 28 0/16 0.00  
SK90-3.16 0.04 7 /  0.04 7 0/3 0.00  0.04 7 0/3 0.00  0.04 6 1/3 0.00  0.04 6 1/3 0.00  
SK90-3.17 0.20 26 /  0.20 24 0/20 0.00  0.20 26 0/20 0.00  0.20 24 0/20 0.00  0.22 26 0/20 0.00  
SK90-3.18 0.86 78 /  0.85 78 0/43 0.00  0.86 78 0/43 0.00  0.86 78 0/43 0.01  0.87 78 0/43 0.01  
SK90-3.19 2.17 80 /  2.14 80 0/41 0.00  2.11 80 0/41 0.00  2.13 80 0/41 0.01  2.20 80 0/41 0.01  
SK90-3.20 1.35 46 /  1.33 46 0/27 0.00  1.31 46 0/27 0.00  1.34 46 0/27 0.00  1.30 46 0/27 0.00  
SK90-3.21 0.64 76 /  0.66 76 0/23 0.00  0.67 76 0/23 0.00  0.63 76 0/23 0.00  0.64 76 0/23 0.00  
SK90-3.22 ∞ ∞ ∞ ∞ ∞ 
SK90-3.23 1.10 70 /  1.08 70 0/35 0.00  1.09 70 0/35 0.00  1.07 70 0/35 0.01  1.11 70 0/35 0.01  
SK90-3.24 0.09 16 /  0.09 16 0/0 0.00  0.09 16 0/0 0.00  0.09 16 0/0 0.00  0.09 16 0/0 0.00  
SK90-3.25 0.08 8 /  0.08 8 0/3 0.00  0.08 8 0/3 0.00  0.08 8 0/3 0.00  0.09 8 0/3 0.00  
SK90-3.26 ∞ ∞ ∞ ∞ ∞ 
SK90-3.27 38.16 2004 /  37.65 2004 0/402 0.04  36.72 2004 0/402 0.04  65.21 2724 2/481 0.27  45.04 2256 2/413 0.31  
SK90-3.28 223.80 1501 /  224.25 1501 0/460 0.16  225.63 1501 0/460 0.23  224.83 1501 0/460 0.41  225.09 1501 0/460 0.42  
SK90-3.29 3.91 94 /  3.93 94 0/28 0.00  3.88 94 0/28 0.00  3.88 94 0/28 0.01  3.79 94 0/28 0.01  
SK90-3.30 0.05 11 /  0.05 11 0/1 0.00  0.05 11 0/1 0.00  0.05 11 0/1 0.00  0.05 11 0/1 0.00  
SK90-3.31 0.04 4 /  0.04 4 0/1 0.00  0.04 4 0/1 0.00  0.04 4 0/1 0.00  0.04 4 0/1 0.00  
SK90-3.32 0.03 5 /  0.03 5 0/1 0.00  0.03 5 0/1 0.00  0.03 5 0/1 0.00  0.03 5 0/1 0.00  
SK90-3.33 0.04 7 /  0.04 7 0/2 0.00  0.04 7 0/2 0.00  0.04 7 0/2 0.00  0.04 7 0/2 0.00  
slothrop-ackermann 0.12 14 /  0.11 14 0/6 0.00  0.11 14 0/6 0.00  0.12 14 0/6 0.00  0.12 14 0/6 0.00  
slothrop-cge 33.45 2354 /  33.25 2263 9/973 0.06  33.28 2286 9/973 0.09  35.41 2468 19/1138 0.36  35.59 2470 18/1138 0.41  
slothrop-cge3 ∞ ∞ ∞ ∞ ⊥ 
slothrop-endo 4.55 667 /  4.53 658 9/313 0.02  4.60 660 9/313 0.03  4.66 638 14/314 0.06  4.63 639 13/314 0.07  
slothrop-equiv_proofs 7.34 513 /  7.47 513 0/214 0.01  7.37 513 0/214 0.01  7.40 513 0/214 0.04  7.35 513 0/214 0.03  
slothrop-equiv_proofs_or 7.32 513 /  7.38 513 0/214 0.01  7.38 513 0/214 0.02  7.36 513 0/214 0.03  7.43 513 0/214 0.03  
slothrop-fgh 0.03 8 /  0.03 8 0/0 0.00  0.03 8 0/0 0.00  0.03 8 0/0 0.00  0.03 8 0/0 0.00  
slothrop-groups 1.18 236 /  1.15 228 7/152 0.01  1.18 230 7/152 0.01  1.16 224 11/153 0.03  1.20 225 10/153 0.04  
slothrop-groups_conj 0.65 124 /  0.67 122 6/78 0.00  0.66 122 6/78 0.01  0.62 118 9/78 0.01  0.63 118 6/77 0.02  
slothrop-hard 0.03 3 /  0.03 3 0/1 0.00  0.03 3 0/1 0.00  0.03 3 0/1 0.00  0.03 3 0/1 0.00  
slothrop-nlp-2b ∞ ∞ ∞ ∞ ∞ 
TPDB-AProVE_07_thiemann27 ∞ ∞ ∞ ∞ ∞ 
TPDB-secr10 ∞ ∞ ∞ 474.87 4929 61/3368 4.88  447.21 5015 40/3038 5.84  
TPDB-secr4 22.47 968 /  22.56 968 0/344 0.03  22.32 968 0/344 0.03  22.38 955 0/344 0.14  22.41 964 0/344 0.14  
TPDB-z115 91.06 1881 /  90.91 1881 0/394 0.06  91.29 1881 0/394 0.14  90.54 1807 4/396 0.25  90.86 1870 1/396 0.27  
TPTP-BOO027-1_theory 0.14 10 /  0.13 10 0/1 0.00  0.13 10 0/1 0.00  0.13 10 0/1 0.00  0.14 10 0/1 0.00  
TPTP-COL053-1_theory 0.03 4 /  0.03 4 0/1 0.00  0.03 4 0/1 0.00  0.03 4 0/1 0.00  0.04 4 0/1 0.00  
TPTP-COL056-1_theory 0.11 12 /  0.12 12 0/3 0.00  0.11 12 0/3 0.00  0.11 12 0/3 0.00  0.11 12 0/3 0.00  
TPTP-COL060-1_theory 0.07 2 /  0.08 2 0/0 0.00  0.07 2 0/0 0.00  0.07 2 0/0 0.00  0.07 2 0/0 0.00  
TPTP-COL085-1_theory 0.01 1 /  0.01 1 0/0 0.00  0.01 1 0/0 0.00  0.01 1 0/0 0.00  0.01 1 0/0 0.00  
TPTP-GRP010-4_theory 14.92 914 /  11.66 743 10/608 0.06  11.76 747 10/608 0.08  8.61 609 28/419 0.14  8.29 590 27/401 0.14  
TPTP-GRP011-4_theory 2.54 351 /  2.50 343 8/198 0.01  2.52 345 8/198 0.02  2.51 332 16/199 0.04  2.54 332 15/199 0.04  
TPTP-GRP012-4_theory 0.83 217 /  0.82 208 7/141 0.01  0.84 210 7/141 0.01  0.82 203 15/142 0.03  0.83 202 15/142 0.03  
TPTP-GRP393-2_theory 0.04 6 /  0.04 6 0/2 0.00  0.04 6 0/2 0.00  0.04 6 0/2 0.00  0.04 6 0/2 0.00  
TPTP-GRP394-3_theory 1.16 236 /  1.17 228 7/152 0.01  1.20 230 7/152 0.01  1.15 222 13/153 0.03  1.20 222 12/153 0.03  
TPTP-GRP454-1_theory 9.60 704 /  4.31 449 17/248 0.03  4.31 453 17/248 0.04  6.28 496 34/327 0.13  7.16 580 29/332 0.16  
TPTP-GRP457-1_theory 9.67 704 /  4.33 449 17/248 0.03  4.31 453 17/248 0.04  6.32 496 34/327 0.13  7.14 580 29/332 0.16  
TPTP-GRP460-1_theory 22.93 1686 /  12.44 934 27/894 0.12  12.16 936 27/893 0.15  ∞ ∞ 
TPTP-GRP463-1_theory 23.01 1686 /  12.41 934 27/894 0.12  12.38 936 27/893 0.15  ∞ ∞ 
TPTP-GRP481-1_theory 141.10 6868 /  91.07 4792 59/2730 0.47  92.41 4812 55/2710 0.62  63.95 4092 53/2448 2.16  84.22 4284 154/2744 2.85  
TPTP-GRP484-1_theory 475.10 11330 /  126.79 5529 42/3230 0.63  128.14 5626 41/3244 0.78  204.41 5948 157/4840 5.61  195.34 6063 136/4555 5.64  
TPTP-GRP487-1_theory 144.21 4853 /  156.20 4396 76/3057 0.55  101.41 3494 35/2329 0.47  122.23 3820 154/2809 2.91  137.53 3777 140/2930 3.17  
TPTP-GRP490-1_theory 391.44 8374 /  139.60 4690 65/3000 0.47  ∞ 120.79 3517 198/3076 2.91  115.40 3204 196/3140 3.06  
TPTP-GRP493-1_theory 93.69 6502 /  180.26 11512 45/5118 0.75  184.70 11766 38/5097 0.90  155.36 8700 107/5644 6.50  162.80 9486 93/5631 7.17  
TPTP-GRP496-1_theory 134.63 5528 /  123.17 4597 69/3625 0.51  123.61 4637 50/3595 0.68  123.03 4378 305/3914 3.42  85.02 3458 249/3052 2.85  
TPTP-HWC004-1_theory 0.24 36 /  0.25 36 0/0 0.00  0.25 36 0/0 0.00  0.25 36 0/0 0.00  0.24 36 0/0 0.00  
TPTP-HWC004-2_theory 0.11 14 /  0.11 14 0/0 0.00  0.11 14 0/0 0.00  0.13 14 0/0 0.00  0.11 14 0/0 0.00  
TPTP-SWV262-2_theory 0.11 7 /  0.10 7 0/4 0.00  0.10 7 0/4 0.00  0.10 7 0/4 0.00  0.11 7 0/4 0.00  
WS06-proofreduction 237.90 1682 /  237.69 1682 0/688 0.04  238.11 1682 0/688 0.07  237.96 1682 0/688 0.16  238.41 1682 0/688 0.16  
successes 87 85 85 85 85 
average time 40.1 30.16 33.54 32.13 31.44 
redundant CPs (process) 0 994 999 1923 1756 
time/checking 0 7.4 10.64 43.43 47.22 

Explanation:
(1) total time
(2) number of nodes
(3) redundant critical pairs for successful process/all processes
(4) time for checking