mkbTT experiments

View:
  none PCP BCP CCP MCP 
  (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 7 /  0.06 7 0/2 0.00  0.07 7 0/2 0.00  0.06 7 0/2 0.00  0.07 7 0/2 0.00  
ASK93-2 ∞ ∞ ∞ ∞ ∞ 
ASK93-5 ∞ ∞ ∞ ∞ ∞ 
ASK93-6 27.85 90 /  27.80 90 0/19 0.00  27.86 90 0/19 0.00  27.87 90 0/19 0.01  27.89 90 0/19 0.01  
BD94-collapse 0.10 14 /  0.11 14 0/1 0.00  0.11 14 0/1 0.00  0.10 14 0/1 0.00  0.11 14 0/1 0.00  
BD94-peano 0.09 10 /  0.09 10 0/6 0.00  0.10 10 0/6 0.00  0.09 10 0/6 0.00  0.10 10 0/6 0.00  
BD94-sqrt 0.03 6 /  0.04 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 206.92 4973 /  171.67 5787 80/3262 0.66  172.39 5792 78/3262 1.08  215.03 4844 70/2535 3.72  157.46 5120 224/3096 2.91  
BGK94-D10 84.60 2837 /  84.25 2679 25/1579 0.17  84.05 2685 25/1579 0.24  85.49 2594 26/1585 0.82  83.66 2505 44/1586 0.76  
BGK94-D12 108.31 3051 /  106.95 2889 25/1629 0.21  107.61 2895 25/1629 0.28  108.78 2818 24/1645 0.98  107.97 2726 41/1646 0.89  
BGK94-D16 148.48 3672 /  148.70 3505 25/1763 0.27  148.41 3511 25/1763 0.35  149.39 3386 24/1747 1.29  146.74 3269 41/1748 1.18  
BGK94-M08 ∞ ∞ ∞ ∞ ∞ 
BGK94-M10 ∞ ∞ ∞ ∞ ∞ 
BGK94-M12 ∞ ∞ ∞ ∞ ∞ 
BGK94-M14 ∞ ∞ ∞ ∞ ∞ 
BGK94-Z22W ∞ ∞ ∞ ∞ ∞ 
BH96-fac8_theory 0.29 16 /  0.30 16 0/8 0.00  0.30 16 0/8 0.00  0.31 16 0/8 0.00  0.29 16 0/8 0.00  
Chr89-A2 85.79 3690 /  73.42 3322 30/2680 0.28  74.02 3331 29/2669 0.41  79.43 3139 68/2818 1.44  78.75 3106 75/2825 1.29  
Chr89-A24 ∞ ∞ ∞ ∞ ∞ 
Chr89-A3 88.85 4625 /  ∞ ∞ 92.80 4082 102/3100 2.05  ∞ 
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.02 4 /  0.02 4 0/0 0.00  0.02 4 0/0 0.00  0.02 4 0/0 0.00  0.02 4 0/0 0.00  
KH11-fggx 0.06 11 /  0.06 11 0/3 0.00  0.07 11 0/3 0.00  0.07 11 0/3 0.00  0.07 11 0/3 0.00  
KH11-fib 1.86 105 /  1.89 105 0/28 0.00  1.85 105 0/28 0.00  1.88 101 0/28 0.01  1.85 101 0/28 0.01  
KH11-kb-fail ⊥ ⊥ ⊥ ⊥ ⊥ 
KH11-kb-fail1 ⊥ ⊥ ⊥ ⊥ ⊥ 
KH11-lr-theory 2.67 570 /  2.63 538 9/464 0.03  2.64 538 9/461 0.04  2.65 487 23/466 0.18  2.62 489 25/469 0.16  
KH11-rl-theory 2.97 629 /  2.91 597 10/504 0.03  2.93 597 9/504 0.05  2.99 542 23/505 0.20  2.95 543 26/509 0.18  
KK99-linear_assoc 0.09 14 /  0.10 14 0/6 0.00  0.08 14 0/6 0.00  0.09 14 0/6 0.00  0.08 14 0/6 0.00  
Les83-fib 0.55 53 /  0.55 52 0/25 0.00  0.56 52 0/25 0.00  0.54 50 0/25 0.00  0.55 50 0/25 0.00  
Les83-subset 0.34 30 /  0.34 30 0/8 0.00  0.33 30 0/8 0.00  0.33 30 0/8 0.00  0.33 30 0/8 0.00  
LS06-CGE4 ⊥ ⊥ ⊥ ⊥ ⊥ 
LS06-CGE5 ∞ ∞ ∞ ∞ ∞ 
LS94-G0 2.53 343 /  2.51 308 16/236 0.01  2.54 316 16/236 0.02  2.56 303 37/244 0.07  2.53 295 38/244 0.05  
LS94-G1 ∞ ∞ ∞ ∞ ∞ 
LS94-G2 ∞ ∞ ∞ ∞ ∞ 
LS94-G3 ∞ ∞ ∞ ∞ ∞ 
LS94-P1 ∞ ∞ ∞ ∞ ∞ 
OKW95-dt1_theory 2.87 114 /  2.82 114 0/41 0.00  2.88 114 0/41 0.01  2.85 103 0/41 0.02  2.84 103 0/41 0.02  
Sim91-sims2 ∞ ∞ ∞ ∞ ∞ 
SK90-3.01 4.68 727 /  4.71 679 16/439 0.04  4.68 683 16/439 0.05  6.02 720 28/540 0.29  6.00 714 29/540 0.27  
SK90-3.02 0.10 16 /  0.09 16 0/6 0.00  0.09 16 0/6 0.00  0.10 16 0/6 0.00  0.09 16 0/6 0.00  
SK90-3.03 2.06 435 /  2.01 403 8/321 0.03  2.03 412 8/319 0.04  2.19 356 46/323 0.18  2.16 347 47/322 0.17  
SK90-3.04 110.74 8351 /  87.75 6682 469/6441 0.77  88.70 6683 463/6440 1.02  70.61 5007 763/6042 3.57  72.00 5162 792/6166 3.23  
SK90-3.05 19.28 3058 /  16.44 2431 81/1718 0.28  16.80 2499 77/1711 0.35  8.24 862 170/941 0.68  7.81 828 181/922 0.60  
SK90-3.06 ∞ ∞ ∞ ⊥ ∞ 
SK90-3.07 ∞ ∞ ∞ ∞ ∞ 
SK90-3.08 0.19 21 /  0.20 21 0/10 0.00  0.19 21 0/10 0.00  0.19 21 0/10 0.00  0.18 21 0/10 0.00  
SK90-3.09 ∞ ∞ ∞ ∞ ∞ 
SK90-3.10 0.06 8 /  0.06 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.09 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.44 38 /  0.44 38 0/21 0.00  0.44 38 0/21 0.00  0.44 38 0/21 0.00  0.47 38 0/21 0.00  
SK90-3.14 0.41 41 /  0.39 41 0/21 0.00  0.41 41 0/21 0.00  0.38 41 0/21 0.00  0.41 41 0/21 0.00  
SK90-3.15 0.23 28 /  0.23 26 2/16 0.00  0.22 26 2/16 0.00  0.23 28 0/16 0.00  0.23 26 2/16 0.00  
SK90-3.16 0.04 7 /  0.04 7 0/3 0.00  0.04 7 0/3 0.00  0.03 6 1/3 0.00  0.04 6 1/3 0.00  
SK90-3.17 0.20 43 /  0.20 39 0/28 0.00  0.19 41 0/28 0.00  0.20 36 0/29 0.01  0.19 34 0/29 0.01  
SK90-3.18 0.67 78 /  0.68 78 0/43 0.00  0.68 78 0/43 0.00  0.67 78 0/43 0.01  0.66 78 0/43 0.01  
SK90-3.19 0.67 69 /  0.67 69 0/34 0.00  0.68 69 0/34 0.00  0.67 69 0/34 0.01  0.68 69 0/34 0.01  
SK90-3.20 1.22 46 /  1.23 46 0/27 0.00  1.24 46 0/27 0.00  1.25 46 0/27 0.00  1.25 46 0/27 0.00  
SK90-3.21 0.50 76 /  0.51 76 0/23 0.00  0.47 76 0/23 0.00  0.52 76 0/23 0.00  0.50 76 0/23 0.00  
SK90-3.22 ∞ ∞ ∞ ∞ ∞ 
SK90-3.23 1.08 76 /  1.15 76 0/44 0.00  1.11 76 0/44 0.00  1.15 76 0/44 0.01  1.15 76 0/44 0.01  
SK90-3.24 0.08 16 /  0.08 16 0/0 0.00  0.09 16 0/0 0.00  0.08 16 0/0 0.00  0.08 16 0/0 0.00  
SK90-3.25 0.07 8 /  0.07 8 0/3 0.00  0.07 8 0/3 0.00  0.07 8 0/3 0.00  0.07 8 0/3 0.00  
SK90-3.26 ∞ ∞ ∞ ∞ ∞ 
SK90-3.27 122.12 2977 /  128.25 2977 0/719 0.12  126.98 2977 0/719 0.10  257.53 3993 2/936 1.17  241.38 3947 2/964 0.96  
SK90-3.28 117.37 1579 /  117.92 1579 0/481 0.09  117.98 1579 0/481 0.11  117.93 1691 0/497 0.26  117.83 1679 0/497 0.25  
SK90-3.29 3.16 68 /  3.21 68 0/34 0.00  3.17 68 0/34 0.00  3.21 68 0/34 0.01  3.17 68 0/34 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.05 4 0/1 0.00  0.04 4 0/1 0.00  0.04 4 0/1 0.00  0.05 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.03 7 /  0.03 7 0/2 0.00  0.03 7 0/2 0.00  0.03 7 0/2 0.00  0.03 7 0/2 0.00  
slothrop-ackermann 0.10 14 /  0.09 14 0/6 0.00  0.10 14 0/6 0.00  0.10 14 0/6 0.00  0.09 14 0/6 0.00  
slothrop-cge ⊥ ⊥ ⊥ ⊥ ⊥ 
slothrop-cge3 ∞ ∞ ∞ 462.10 22778 529/11413 12.77  456.95 21658 649/11774 11.50  
slothrop-endo 3.29 591 /  3.36 582 8/310 0.02  3.36 585 8/310 0.03  3.35 569 15/311 0.06  3.37 567 16/311 0.06  
slothrop-equiv_proofs 6.52 515 /  6.51 515 0/214 0.01  6.50 515 0/214 0.02  6.62 515 0/214 0.04  6.50 515 0/214 0.04  
slothrop-equiv_proofs_or 6.48 515 /  6.56 515 0/214 0.01  6.53 515 0/214 0.02  6.52 515 0/214 0.04  6.49 515 0/214 0.04  
slothrop-fgh 0.02 6 /  0.02 6 0/0 0.00  0.02 6 0/0 0.00  0.02 6 0/0 0.00  0.02 6 0/0 0.00  
slothrop-groups 1.00 241 /  0.98 233 10/172 0.01  0.98 235 10/172 0.01  0.99 230 15/173 0.04  0.99 228 16/173 0.03  
slothrop-groups_conj 0.51 130 /  0.49 128 6/88 0.01  0.49 128 6/88 0.01  0.51 122 10/88 0.02  0.49 122 11/88 0.01  
slothrop-hard 0.03 3 /  0.03 3 0/1 0.00  0.04 3 0/1 0.00  0.03 3 0/1 0.00  0.04 3 0/1 0.00  
slothrop-nlp-2b ∞ ∞ ∞ ∞ ∞ 
TPDB-AProVE_07_thiemann27 ∞ ∞ ∞ ∞ ∞ 
TPDB-secr10 8.87 689 /  8.90 689 0/340 0.03  8.93 689 0/340 0.03  8.73 663 11/341 0.18  8.46 623 29/343 0.15  
TPDB-secr4 10.65 536 /  10.72 536 0/180 0.01  10.63 536 0/180 0.02  10.68 536 0/180 0.06  10.70 536 0/180 0.06  
TPDB-z115 25.98 1197 /  26.19 1197 0/254 0.02  26.12 1197 0/254 0.04  25.95 1160 11/254 0.11  26.33 1148 14/254 0.10  
TPTP-BOO027-1_theory 0.12 10 /  0.13 10 0/1 0.00  0.12 10 0/1 0.00  0.12 10 0/1 0.00  0.12 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.03 4 0/1 0.00  
TPTP-COL056-1_theory 0.11 12 /  0.11 12 0/3 0.00  0.10 12 0/3 0.00  0.11 12 0/3 0.00  0.10 12 0/3 0.00  
TPTP-COL060-1_theory 0.07 2 /  0.07 2 0/0 0.00  0.06 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 7.82 835 /  7.79 788 16/492 0.05  7.88 790 16/492 0.07  7.73 747 29/489 0.21  7.69 732 37/492 0.19  
TPTP-GRP011-4_theory 1.83 338 /  1.80 319 11/218 0.01  1.80 324 11/218 0.02  1.83 309 15/220 0.05  1.81 304 17/220 0.04  
TPTP-GRP012-4_theory 1.02 309 /  0.98 274 16/216 0.01  0.99 282 16/216 0.02  1.02 269 32/223 0.06  1.00 262 33/223 0.05  
TPTP-GRP393-2_theory 0.03 6 /  0.03 6 0/2 0.00  0.04 6 0/2 0.00  0.03 6 0/2 0.00  0.03 6 0/2 0.00  
TPTP-GRP394-3_theory 1.21 317 /  1.21 288 14/212 0.01  1.22 293 14/212 0.02  1.22 278 24/215 0.05  1.21 273 24/215 0.04  
TPTP-GRP454-1_theory 140.28 8924 /  29.54 2130 73/1872 0.24  29.70 2142 73/1871 0.33  121.25 5548 122/4036 4.21  182.29 8091 146/5815 7.03  
TPTP-GRP457-1_theory 138.84 8924 /  29.51 2130 73/1872 0.24  29.83 2142 73/1871 0.33  121.44 5548 122/4036 4.22  184.25 8091 146/5815 7.11  
TPTP-GRP460-1_theory 26.36 2652 /  12.54 1451 45/1331 0.19  12.62 1462 41/1330 0.23  53.97 2787 223/3235 3.47  14.79 1171 121/1455 1.26  
TPTP-GRP463-1_theory 26.40 2652 /  12.71 1451 45/1331 0.19  12.78 1462 41/1330 0.24  53.15 2787 223/3235 3.44  14.90 1171 121/1455 1.27  
TPTP-GRP481-1_theory 430.73 21292 /  39.46 2880 67/2323 0.38  22.19 2249 48/1618 0.28  24.60 2407 119/2144 2.56  26.85 2469 137/2308 2.50  
TPTP-GRP484-1_theory ∞ 97.23 5218 115/4035 0.77  98.09 5286 101/4026 0.94  91.61 4171 182/4003 4.59  78.28 3928 202/3868 4.23  
TPTP-GRP487-1_theory 136.23 5404 /  230.21 7747 89/5450 1.51  158.86 5510 77/4285 1.34  108.21 3545 255/3217 3.36  116.25 3698 263/3194 3.19  
TPTP-GRP490-1_theory ∞ ∞ ∞ ∞ ∞ 
TPTP-GRP493-1_theory 72.57 7358 /  66.56 7041 106/3310 0.45  68.33 7211 92/3299 0.53  100.78 8835 298/4075 4.16  48.04 4360 291/3074 2.53  
TPTP-GRP496-1_theory ∞ ∞ ∞ 469.69 12623 431/10936 21.40  ∞ 
TPTP-HWC004-1_theory 0.25 36 /  0.24 36 0/0 0.00  0.25 36 0/0 0.00  0.26 36 0/0 0.00  0.25 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.12 14 0/0 0.00  0.11 14 0/0 0.00  
TPTP-SWV262-2_theory 0.09 7 /  0.09 7 0/4 0.00  0.08 7 0/4 0.00  0.08 7 0/4 0.00  0.09 7 0/4 0.00  
WS06-proofreduction 227.83 1703 /  227.92 1703 0/722 0.04  228.32 1703 0/722 0.07  228.13 1703 0/722 0.17  228.19 1703 0/722 0.17  
successes 82 82 82 85 83 
average time 29.59 22.15 21.13 37.13 30.12 
redundant CPs (process) 0 1490 1409 4073 3841 
time/checking 0 7.2 8.75 82.26 54.59 

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