mkbTT experiments

View:
  LPO KBO LPO+KBO POLY MATRIX TKBO 
  (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 1 5 57  0.07 1 5 71  0.09 1 5 67  0.13 1 5 77  0.19 1 5 84  0.13 1 5 77  
ASK93-2 ∞ ∞ ∞ ∞ ∞ ∞ 
ASK93-5 ∞ ∞ ∞ ∞ ∞ ∞ 
ASK93-6 28.29 402 915 50  34.76 402 915 59  31.98 402 915 56  262.56 377 937 95  185.62 449 1015 90  262.31 377 937 95  
BD94-collapse 0.17 3 12 65  0.18 3 12 67  0.20 3 12 70  0.22 3 12 73  0.22 3 12 77  0.19 3 12 74  
BD94-peano 0.11 2 8 64  ∞ 0.15 3 8 73  ⊥ ⊥ ⊥ 
BD94-sqrt 0.06 0 4 50  0.08 0 4 63  0.08 0 4 63  0.11 0 4 64  0.19 0 4 84  0.10 0 4 70  
BGK94-D08 34.35 13 543 30  56.40 20 794 26  122.82 8 1336 30  86.50 38 598 78  ∞ 78.14 38 598 86  
BGK94-D10 97.25 13 643 14  69.23 2 785 21  ∞ ⊥ ∞ ⊥ 
BGK94-D12 151.10 12 669 11  63.54 2 717 21  60.94 12 789 33  ⊥ ∞ ⊥ 
BGK94-D16 304.83 11 702 7  53.34 2 633 22  136.38 4 889 18  ⊥ ∞ ⊥ 
BGK94-M08 ∞ ∞ ∞ ∞ ∞ ∞ 
BGK94-M10 ∞ ∞ ∞ ∞ ∞ ∞ 
BGK94-M12 ∞ ∞ ∞ ∞ ∞ ∞ 
BGK94-M14 ∞ ∞ ∞ ∞ ∞ ∞ 
BGK94-Z22W ∞ ∞ ∞ ∞ ∞ ∞ 
BH96-fac8_theory 0.38 10 30 79  1.07 8 84 81  0.55 12 34 82  8.25 12 100 97  14.28 14 114 98  7.85 12 100 98  
Chr89-A2 11.24 5 193 22  211.23 1 554 5  33.93 17 392 23  123.78 2 663 53  ∞ 107.02 2 663 61  
Chr89-A24 ∞ ∞ ∞ ∞ ∞ ∞ 
Chr89-A3 ∞ ∞ 478.08 154 3190 22  ∞ ∞ 460.49 215 2267 56  
HR94-1 ∞ ∞ ∞ ⊥ ∞ ⊥ 
HR94-2 ∞ ∞ ∞ ⊥ ∞ ⊥ 
KH11-aufgabe3-2 0.03 1 2 33  0.03 1 2 67  0.03 1 2 67  0.04 1 2 50  0.04 1 2 75  0.03 1 2 67  
KH11-aufgabe3-3 0.05 0 3 60  0.05 0 3 60  0.06 0 3 50  0.05 0 3 60  0.14 0 3 79  0.04 0 3 50  
KH11-fggx 0.10 1 6 60  0.11 2 6 55  0.13 2 6 62  0.14 2 6 64  0.19 2 6 74  0.13 2 6 69  
KH11-fib 2.02 41 135 71  ∞ 2.58 45 139 74  108.73 42 747 93  ⊥ 102.52 42 747 96  
KH11-kb-fail ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 
KH11-kb-fail1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 
KH11-lr-theory 1.10 1 31 29  1.65 4 44 28  1.85 5 44 32  9.35 9 96 62  ∞ 7.74 9 96 73  
KH11-rl-theory 5.39 1 55 13  360.39 0 266 1  16.03 5 129 16  ∞ ∞ ∞ 
KK99-linear_assoc 0.06 1 4 50  0.07 1 4 57  0.08 1 4 63  0.21 3 6 81  0.21 3 6 81  0.18 3 6 83  
Les83-fib 0.35 2 24 66  ∞ 0.49 4 26 69  ⊥ ⊥ ⊥ 
Les83-subset 0.43 5 27 60  ∞ 0.52 5 27 67  ∞ ∞ ∞ 
LS06-CGE4 ⊥ ⊥ ⊥ ⊥ ∞ ⊥ 
LS06-CGE5 ⊥ ⊥ ∞ ⊥ ∞ ⊥ 
LS94-G0 0.72 1 27 39  0.78 3 27 40  0.84 3 27 43  2.95 5 47 74  ⊥ 2.70 5 47 83  
LS94-G1 ∞ ∞ ∞ ∞ ∞ ∞ 
LS94-G2 ∞ ∞ ∞ ⊥ ∞ ⊥ 
LS94-G3 ∞ ∞ ∞ ⊥ ∞ ⊥ 
LS94-P1 ∞ ∞ ∞ ∞ ∞ ∞ 
OKW95-dt1_theory 2.00 22 134 68  ∞ 2.87 29 148 72  ⊥ ⊥ ⊥ 
Sim91-sims2 ∞ ∞ ∞ ⊥ ⊥ ⊥ 
SK90-3.01 0.92 2 38 40  1.45 7 48 35  1.60 7 48 41  7.19 13 109 67  45.74 9 218 79  6.20 13 109 75  
SK90-3.02 0.11 1 7 55  0.11 1 7 55  0.13 1 7 62  0.22 1 7 77  0.27 1 7 81  0.21 1 7 81  
SK90-3.03 3.93 3 103 28  21.77 14 233 16  23.15 14 233 21  65.39 17 336 53  ⊥ 56.26 17 336 60  
SK90-3.04 1.20 1 39 30  ∞ 1.40 2 39 34  10.44 11 126 59  ∞ 8.50 11 126 72  
SK90-3.05 11.05 3 119 13  6.80 1 123 26  11.33 3 119 16  39.41 13 265 37  62.11 8 223 65  30.89 13 265 47  
SK90-3.06 ∞ ∞ ∞ ∞ ∞ ∞ 
SK90-3.07 ∞ ∞ ∞ ∞ ∞ ∞ 
SK90-3.08 0.18 2 10 50  0.18 2 10 50  0.22 2 10 59  0.22 2 10 59  0.66 2 10 86  0.20 2 10 55  
SK90-3.09 ∞ ∞ ∞ ∞ ∞ ∞ 
SK90-3.10 0.13 0 8 54  0.15 0 8 53  0.16 0 8 63  0.15 0 8 60  0.40 0 8 85  0.14 0 8 64  
SK90-3.11 0.11 0 7 55  0.13 0 7 62  0.14 0 7 64  0.13 0 7 69  0.29 0 7 83  0.13 0 7 62  
SK90-3.12 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 
SK90-3.13 0.43 3 30 65  0.42 3 30 67  0.51 3 30 71  1.36 11 33 90  1.51 11 33 91  1.26 11 33 94  
SK90-3.14 0.41 5 30 63  0.53 9 34 62  0.59 9 34 68  1.32 9 34 86  1.21 7 26 88  1.21 9 34 90  
SK90-3.15 ⊥ 0.33 2 16 58  0.35 2 16 60  0.57 3 16 75  0.86 3 16 83  0.52 3 16 81  
SK90-3.16 0.08 0 5 50  0.10 0 5 60  0.11 0 5 64  0.14 0 5 71  0.26 0 5 85  0.13 0 5 77  
SK90-3.17 0.12 1 8 50  0.15 1 10 53  0.20 2 10 55  0.34 3 10 74  0.41 3 10 78  0.30 3 10 83  
SK90-3.18 0.41 2 24 56  ∞ 0.79 7 35 61  2.15 7 35 86  ⊥ 1.96 7 35 90  
SK90-3.19 0.57 5 43 68  0.70 9 45 66  0.81 9 45 70  4.69 25 81 89  2.70 6 47 91  4.30 25 81 95  
SK90-3.20 0.74 7 52 69  1.20 19 75 70  1.40 19 75 74  6.03 31 90 92  ⊥ 5.58 31 90 96  
SK90-3.21 0.46 3 27 52  0.70 7 43 60  0.83 7 43 66  1.76 7 43 84  2.15 3 33 89  1.62 7 43 88  
SK90-3.22 ∞ ∞ ∞ ∞ ⊥ ∞ 
SK90-3.23 0.84 12 42 46  1.06 16 48 49  1.17 16 48 52  2.39 16 48 77  2.50 15 46 79  2.27 16 48 81  
SK90-3.24 0.11 3 8 55  0.12 3 8 58  0.14 3 8 64  0.14 3 8 64  0.15 3 8 67  0.13 3 8 69  
SK90-3.25 0.07 1 4 43  0.06 1 4 50  0.08 1 4 63  0.13 1 4 77  0.25 1 4 88  0.12 1 4 83  
SK90-3.26 ∞ ∞ ∞ ∞ ⊥ ∞ 
SK90-3.27 7.87 0 68 15  29.05 2 121 5  30.01 2 121 8  24.14 0 82 56  ∞ 23.35 0 82 58  
SK90-3.28 189.40 2 1330 12  118.96 133 2226 33  134.09 135 2242 40  ∞ 187.88 56 879 88  ∞ 
SK90-3.29 1.87 33 106 61  2.81 47 134 62  3.07 47 134 65  16.56 51 168 90  14.63 49 168 87  16.19 51 168 92  
SK90-3.30 0.08 0 4 50  0.08 0 4 63  0.10 0 4 60  0.13 0 4 69  0.15 0 4 73  0.12 0 4 75  
SK90-3.31 0.06 1 4 67  0.09 1 6 67  0.08 1 4 63  0.15 1 4 80  0.14 1 4 79  0.14 1 4 79  
SK90-3.32 0.06 0 4 50  0.06 0 4 67  0.07 0 4 57  0.07 0 4 57  0.12 0 4 75  0.07 0 4 57  
SK90-3.33 0.08 0 5 50  0.09 0 5 56  0.09 0 5 67  0.10 0 5 60  0.17 0 5 82  0.09 0 5 67  
slothrop-ackermann 0.08 1 6 63  ⊥ 0.12 2 6 67  ⊥ ⊥ ⊥ 
slothrop-cge ⊥ ⊥ ⊥ ⊥ ∞ ⊥ 
slothrop-cge3 ⊥ ⊥ ⊥ ⊥ ∞ ⊥ 
slothrop-endo 10.89 0 105 16  ∞ ∞ ∞ ∞ ∞ 
slothrop-equiv_proofs ⊥ ⊥ ⊥ ⊥ ∞ ⊥ 
slothrop-equiv_proofs_or ⊥ ⊥ ⊥ ⊥ ∞ ⊥ 
slothrop-fgh 0.05 0 3 60  0.06 0 3 50  0.06 0 3 67  0.07 0 3 71  0.07 0 3 57  0.07 0 3 57  
slothrop-groups 0.88 0 23 28  9.15 0 62 9  9.43 0 62 11  31.03 0 138 50  ⊥ 27.43 0 138 56  
slothrop-groups_conj 0.29 0 12 38  0.38 1 16 42  0.42 1 16 50  0.91 2 21 68  ⊥ 0.78 2 21 78  
slothrop-hard 0.04 1 3 50  0.04 1 3 75  0.05 1 3 60  0.07 1 3 71  0.08 1 3 75  0.06 1 3 67  
slothrop-nlp-2b ∞ ∞ ∞ ∞ ⊥ ∞ 
TPDB-AProVE_07_thiemann27 ∞ ∞ ∞ ⊥ ⊥ ⊥ 
TPDB-secr10 12.95 3 131 14  340.52 25 646 4  338.71 25 646 5  365.42 17 477 31  32.35 5 116 77  324.23 17 477 37  
TPDB-secr4 23.21 31 318 18  16.87 24 307 23  18.92 25 307 28  45.66 2 350 54  39.22 13 313 74  43.22 2 350 57  
TPDB-z115 ∞ 76.81 115 690 12  80.41 115 690 16  122.49 45 602 47  ⊥ 115.25 45 602 50  
TPTP-BOO027-1_theory 0.13 0 7 46  0.15 0 7 53  0.17 0 7 53  0.34 0 7 79  0.84 0 7 90  0.34 0 7 82  
TPTP-COL053-1_theory 0.03 0 2 67  0.03 1 2 33  0.04 1 2 50  0.05 1 2 80  0.06 1 2 67  0.05 1 2 80  
TPTP-COL056-1_theory 0.11 2 10 82  0.14 5 10 71  0.16 5 10 75  0.26 5 10 81  0.27 5 10 81  0.24 5 10 88  
TPTP-COL060-1_theory ⊥ 0.05 0 4 80  0.06 0 4 83  0.12 0 4 83  0.13 0 4 92  0.12 0 4 83  
TPTP-COL085-1_theory 0.02 0 1 50  0.02 0 1 50  0.02 0 1 50  0.02 0 1 50  0.03 0 1 67  0.02 0 1 50  
TPTP-GRP010-4_theory 2.51 5 82 35  2.68 8 82 35  2.86 8 82 40  17.39 15 198 76  ∞ 15.52 15 198 85  
TPTP-GRP011-4_theory 0.66 0 23 38  0.72 1 23 39  0.78 1 23 44  3.72 2 46 76  ∞ 3.43 2 46 81  
TPTP-GRP012-4_theory 0.42 0 14 31  0.48 1 14 33  0.51 1 14 37  1.36 2 22 57  ⊥ 1.13 2 22 69  
TPTP-GRP393-2_theory 0.04 0 2 50  0.03 0 2 67  0.04 0 2 50  0.06 1 2 50  0.06 1 2 67  0.06 1 2 67  
TPTP-GRP394-3_theory 0.51 0 17 33  0.55 1 17 35  0.59 1 17 39  1.95 2 35 66  ⊥ 1.65 2 35 75  
TPTP-GRP454-1_theory 27.54 0 271 15  7.91 15 177 28  8.68 15 177 35  13.54 15 177 58  ⊥ 11.87 15 177 66  
TPTP-GRP457-1_theory 27.25 0 271 14  7.92 15 177 29  8.67 15 177 35  13.64 15 177 59  ⊥ 11.84 15 177 66  
TPTP-GRP460-1_theory 78.39 4 369 9  21.30 22 202 13  25.66 17 237 18  34.81 22 229 43  ∞ 27.97 22 229 53  
TPTP-GRP463-1_theory 75.55 4 369 9  21.29 22 202 13  25.65 17 237 18  34.82 22 229 43  ∞ 27.54 22 229 53  
TPTP-GRP481-1_theory 35.43 0 306 14  16.15 11 178 15  17.23 11 178 20  ∞ ∞ ∞ 
TPTP-GRP484-1_theory ∞ 178.06 0 781 9  185.91 0 781 12  ∞ ∞ ∞ 
TPTP-GRP487-1_theory ∞ 93.14 28 658 13  96.62 28 658 17  ∞ ⊥ ∞ 
TPTP-GRP490-1_theory 134.94 0 572 9  152.74 27 794 11  159.83 27 794 14  ∞ ∞ ∞ 
TPTP-GRP493-1_theory ∞ 55.22 0 294 9  56.18 0 294 11  ∞ ∞ ∞ 
TPTP-GRP496-1_theory 137.76 0 583 11  128.16 34 690 12  145.88 33 716 14  ∞ ∞ ∞ 
TPTP-HWC004-1_theory 0.34 2 16 41  0.37 2 16 46  0.40 2 16 50  0.47 2 16 57  0.79 2 16 75  0.45 2 16 58  
TPTP-HWC004-2_theory 0.16 2 12 63  0.17 2 12 65  0.21 2 12 71  0.25 2 12 72  0.29 2 12 76  0.22 2 12 73  
TPTP-SWV262-2_theory 0.10 3 7 60  0.11 3 7 64  0.11 3 7 73  0.29 3 7 86  0.34 3 7 88  0.28 3 7 89  
WS06-proofreduction ∞ ∞ ∞ ⊥ ∞ ⊥ 
successes 75 72 80 64 44 65 
average time 19.09 30.16 28.6 23.08 13.64 27.77 
total termination % 13 12 19 60 84 63 

Explanation:
(1) total time
(2) number of processes
(3) number of termination checks
(4) percentage of time spent on termination checks