mkbTT experiments

View:
  NV PI DT none 
  (1)(2)(3)(4) (1)(2)(3)(4) (1)(2)(3)(4) (1)(2)(3)(4) 
AD93-Z22     
ASK93-1 0.06 0 0 17  0.07 0 0 14  0.06 0 0 17  0.07 0 0 14  
ASK93-2     
ASK93-5     
ASK93-6 37.75 0 0 6  38.08 0 0 7  37.64 0 0 6  39.64 0 0 6  
BD94-collapse 0.10 0 0 20  0.11 0 0 18  0.11 0 0 18  0.11 0 0 18  
BD94-peano 0.10 0 0 10  0.11 0 0 9  0.10 0 0 10  0.10 0 0 10  
BD94-sqrt 0.03 0 0 0  0.03 0 0 0  0.03 0 0 0  0.03 0 0 0  
BGK94-D08 127.85 0 3 16  130.26 0 0 17  122.08 0 0 12  121.59 0 0 11  
BGK94-D10 144.55 0 7 29  148.39 0 0 31  125.74 0 0 20  123.42 0 0 18  
BGK94-D12 124.92 0 8 28  128.42 0 0 31  110.27 0 0 20  107.32 0 0 17  
BGK94-D16 150.35 0 9 31  159.90 0 0 35  132.80 0 0 22  128.02 0 0 19  
BGK94-M08     
BGK94-M10     
BGK94-M12     
BGK94-M14     
BGK94-Z22W     
BH96-fac8_theory 0.34 0 0 6  0.35 0 0 6  0.34 0 0 6  0.36 0 0 6  
Chr89-A2 42.50 0 4 23  41.93 0 0 22  38.81 0 0 16  38.22 0 0 15  
Chr89-A24     
Chr89-A3 160.87 0 1 9  160.25 0 0 9  159.43 0 0 9  157.59 0 0 8  
HR94-1     
HR94-2     
KH11-aufgabe3-2 0.02 0 0 0  0.02 0 0 0  0.02 0 0 0  0.02 0 0 0  
KH11-aufgabe3-3 0.03 0 0 0  0.03 0 0 0  0.03 0 0 0  0.03 0 0 0  
KH11-fggx 0.08 0 0 13  0.09 0 0 11  0.08 0 0 13  0.08 0 0 13  
KH11-fib 2.93 0 1 8  2.99 0 0 9  2.93 0 0 7  3.00 0 0 7  
KH11-kb-fail     
KH11-kb-fail1     
KH11-lr-theory 5.65 0 5 32  5.74 0 0 33  5.03 0 0 25  5.18 0 1 22  
KH11-rl-theory   440.25 0 0 64  429.91 0 0 63  
KK99-linear_assoc 0.09 0 0 11  0.10 0 0 10  0.10 0 0 10  0.10 0 0 10  
Les83-fib 0.71 0 1 8  0.70 0 0 10  0.69 0 0 7  0.70 0 0 7  
Les83-subset 0.37 0 3 14  0.38 0 0 16  0.36 0 0 14  0.37 0 0 14  
LS06-CGE4     
LS06-CGE5     
LS94-G0 1.72 1 3 20  1.77 1 0 23  1.65 1 0 18  1.64 1 1 15  
LS94-G1     
LS94-G2     
LS94-G3     
LS94-P1     
OKW95-dt1_theory 3.14 0 1 7  3.11 0 0 7  3.06 0 0 6  3.12 0 0 6  
Sim91-sims2     
SK90-3.01 4.87 0 4 27  7.18 0 0 27  6.85 0 0 22  4.62 0 0 21  
SK90-3.02 0.10 0 0 10  0.11 0 0 9  0.10 0 0 10  0.11 0 0 9  
SK90-3.03 2.34 0 3 26  2.37 0 0 29  2.23 0 0 23  2.19 0 0 20  
SK90-3.04 5.09 0 4 26  5.19 0 0 28  4.63 0 0 21  4.51 0 0 18  
SK90-3.05 102.31 0 6 35  26.67 0 0 27  23.90 0 0 20  81.99 0 0 19  
SK90-3.06 17.27 0 6 27  17.71 0 0 28  16.28 0 0 23  16.08 0 0 21  
SK90-3.07 81.69 0 7 33  81.88 0 0 33  75.06 0 0 26  73.05 0 0 23  
SK90-3.08 0.13 0 0 23  0.13 0 0 23  0.12 0 0 25  0.13 0 0 23  
SK90-3.09     
SK90-3.10 0.07 0 0 14  0.07 0 0 14  0.06 0 0 17  0.06 0 0 17  
SK90-3.11 0.08 0 0 13  0.08 0 0 13  0.08 0 0 13  0.08 0 0 13  
SK90-3.12     
SK90-3.13 0.48 0 0 8  0.48 0 0 8  0.48 0 0 6  0.50 0 0 6  
SK90-3.14 0.52 0 2 12  0.52 0 0 12  0.50 0 0 10  0.51 0 0 10  
SK90-3.15 0.29 0 0 14  0.29 0 0 14  0.27 0 0 11  0.27 0 0 11  
SK90-3.16 0.04 0 0 25  0.04 0 0 25  0.04 0 0 25  0.04 0 0 0  
SK90-3.17 0.21 0 0 10  0.22 0 0 18  0.22 0 0 14  0.20 0 0 10  
SK90-3.18 0.86 0 2 15  0.87 0 0 17  0.84 0 0 13  0.86 0 0 12  
SK90-3.19 2.14 0 0 6  2.15 0 0 7  2.15 0 0 5  2.17 0 0 5  
SK90-3.20 1.31 0 1 7  1.29 0 0 8  1.29 0 0 7  1.35 0 0 5  
SK90-3.21 0.64 0 2 16  0.64 0 0 17  0.61 0 0 15  0.64 0 0 14  
SK90-3.22     
SK90-3.23 1.10 0 2 15  1.13 0 0 17  1.06 0 0 15  1.10 0 1 15  
SK90-3.24 0.09 0 0 22  0.09 0 0 22  0.09 0 0 22  0.09 0 0 22  
SK90-3.25 0.08 0 0 13  0.09 0 0 11  0.08 0 0 13  0.08 0 0 0  
SK90-3.26     
SK90-3.27 37.87 0 4 28  45.45 0 0 40  38.07 0 0 27  38.16 0 0 26  
SK90-3.28 223.75 0 0 5  224.13 0 0 5  221.31 0 0 5  223.80 0 0 5  
SK90-3.29 3.77 0 1 8  3.86 0 0 9  3.83 0 0 8  3.91 0 0 7  
SK90-3.30 0.05 0 0 20  0.06 0 0 17  0.05 0 0 20  0.05 0 0 20  
SK90-3.31 0.04 0 0 0  0.04 0 0 0  0.04 0 0 0  0.04 0 0 0  
SK90-3.32 0.03 0 0 0  0.03 0 0 0  0.03 0 0 0  0.03 0 0 0  
SK90-3.33 0.04 0 0 25  0.04 0 0 25  0.04 0 0 25  0.04 0 0 25  
slothrop-ackermann 0.11 0 0 9  0.12 0 0 17  0.11 0 0 9  0.12 0 0 8  
slothrop-cge 35.02 0 4 20  35.91 0 0 21  33.64 0 0 16  33.45 0 0 15  
slothrop-cge3     
slothrop-endo 4.83 0 4 24  5.07 0 0 26  4.57 0 0 21  4.55 0 0 18  
slothrop-equiv_proofs 7.66 0 3 14  7.91 0 0 16  7.39 0 0 10  7.34 0 0 10  
slothrop-equiv_proofs_or 7.77 0 3 14  7.80 0 0 16  7.29 0 0 10  7.32 0 0 10  
slothrop-fgh 0.03 0 0 33  0.04 0 0 25  0.03 0 0 33  0.03 0 0 33  
slothrop-groups 1.26 0 3 25  1.30 0 0 28  1.19 0 0 22  1.18 1 1 19  
slothrop-groups_conj 0.69 0 3 20  0.70 0 0 23  0.65 0 0 20  0.65 0 0 17  
slothrop-hard 0.04 0 0 0  0.04 0 0 0  0.03 0 0 0  0.03 0 0 0  
slothrop-nlp-2b     
TPDB-AProVE_07_thiemann27     
TPDB-secr10     
TPDB-secr4 22.33 0 2 16  22.73 0 0 16  21.99 0 0 14  22.47 0 0 14  
TPDB-z115 92.26 0 1 13  92.60 0 0 13  89.63 0 0 12  91.06 0 0 12  
TPTP-BOO027-1_theory 0.14 0 0 7  0.12 0 0 8  0.12 0 0 8  0.14 0 0 7  
TPTP-COL053-1_theory 0.03 0 0 0  0.04 0 0 0  0.03 0 0 0  0.03 0 0 0  
TPTP-COL056-1_theory 0.12 0 0 8  0.11 0 0 9  0.11 0 0 9  0.11 0 0 9  
TPTP-COL060-1_theory 0.07 0 0 0  0.08 0 0 0  0.07 0 0 0  0.07 0 0 0  
TPTP-COL085-1_theory 0.01 0 0 0  0.01 0 0 0  0.01 0 0 0  0.01 0 0 0  
TPTP-GRP010-4_theory 16.39 0 4 26  16.48 0 0 27  15.34 0 0 21  14.92 0 1 19  
TPTP-GRP011-4_theory 2.62 0 3 20  2.63 0 0 22  2.50 0 0 17  2.54 0 0 15  
TPTP-GRP012-4_theory 0.91 0 4 32  0.95 0 0 36  0.86 0 0 29  0.83 0 0 24  
TPTP-GRP393-2_theory 0.05 0 0 20  0.04 0 0 25  0.04 0 0 0  0.04 0 0 0  
TPTP-GRP394-3_theory 1.27 1 3 24  1.30 0 0 28  1.19 0 0 23  1.16 0 1 20  
TPTP-GRP454-1_theory 10.21 0 5 27  12.70 0 0 28  11.99 0 0 24  9.60 1 1 22  
TPTP-GRP457-1_theory 10.24 0 5 27  12.38 0 0 28  12.00 0 0 24  9.67 1 1 22  
TPTP-GRP460-1_theory 25.74 0 6 37  26.24 0 0 37  23.46 0 0 32  22.93 1 1 29  
TPTP-GRP463-1_theory 25.78 0 6 37  26.17 0 0 37  23.99 0 0 32  23.01 1 1 29  
TPTP-GRP481-1_theory 163.31 0 8 47  141.57 0 0 49  129.40 0 0 41  141.10 0 1 38  
TPTP-GRP484-1_theory  388.61 0 0 33  348.25 0 0 24  475.10 0 0 22  
TPTP-GRP487-1_theory 160.35 0 6 35  147.33 0 0 36  133.08 0 0 30  144.21 0 1 28  
TPTP-GRP490-1_theory 428.30 0 6 37  435.14 0 0 36  398.44 0 0 30  391.44 0 0 29  
TPTP-GRP493-1_theory 119.98 0 9 45  130.32 0 0 48  98.68 0 0 31  93.69 0 0 28  
TPTP-GRP496-1_theory 145.23 0 7 38  148.33 0 0 39  136.26 0 0 33  134.63 0 1 31  
TPTP-HWC004-1_theory 0.25 0 4 24  0.24 0 0 25  0.24 0 0 25  0.24 0 0 25  
TPTP-HWC004-2_theory 0.11 0 0 18  0.11 0 0 18  0.12 0 0 17  0.11 0 0 18  
TPTP-SWV262-2_theory 0.10 0 0 10  0.10 0 0 10  0.10 0 0 0  0.11 0 0 0  
WS06-proofreduction 241.30 0 1 3  238.63 0 0 3  236.96 0 0 2  237.90 0 0 2  
successes 85 86 87 87 
average time 33.13 36.62 38.18 40.1 
time/variants 6.78 7.6 8.17 8.79 
time/encompassments 135.89 6.67 7.2 10.5 
time/maintenance 1.16 1.79 1.26 0.83 
time/rewriting 734.57 865.35 876.76 854.61 

Explanation:
(1) total time
(2) time for variant retrieval
(3) time for encompassment retrieval
(4) time for rewriting