AC-KBO
Home
AC-KBO
experiments downloads

Termination Experiments

AC-KBO Experiments

The following table collects results obtained with TTT2 running different versions of AC-KBO. A tarball containing all input problems can be found here.

Results in one row were obtained in parallel and run on a server equipped with eight dual-core AMD Opteron processors 885 running at a clock rate of 2.6GHz with 64GB of main memory, for each setting with a timeout of 60 seconds.

The columns correspond to the following settings. Column 0 applies AC-RPO. Columns 1 and 2 apply our version of AC-KBO, in the latter case with subterm coefficients. For both cases partial precedences were allowed. Column 3 applies linear polynomials and column 4 applies two-dimensional matrix interpretations. In the settings corresponding to columns 2 to 4 four bits were allowed for coefficients, and five bits to represent the result.

  0 1 2 3 4
A95_bincoeff 0.014 0.013 0.047 0.112 0.616
A95_finite_comm_monoid 0.013 0.016 0.040 0.080 0.270
A95_homomorphism 0.013 0.009 0.019 0.048 0.282
A95_integers 0.017 0.015 0.075 0.129 0.938
A95_listaddition 0.017 0.016 0.078 0.116 0.758
A95_listaddition2 0.014 0.016 0.031 0.130 0.715
A95_naturals 0.012 0.016 0.052 0.132 0.842
A95_proplogic 0.011 0.012 0.012 0.028 0.105
A95_proplogic2 0.010 0.011 0.015 0.044 0.346
AC01 0.011 0.010 0.020 0.031 0.181
AC02 0.010 0.010 0.018 0.030 0.193
AC03 0.014 0.011 0.040 0.104 0.667
AC04 0.014 0.013 0.092 0.142 1.122
AC05 0.012 0.012 0.011 0.227 1.370
AC06 0.016 0.012 0.072 0.228 1.417
AC07 0.012 0.011 0.012 0.210 1.440
AC08 0.020 0.015 0.077 0.201 1.220
AC09 0.016 0.011 0.025 0.163 0.867
AC10 0.014 0.008 0.017 0.085 0.659
AC11 0.035 0.033 0.132 1.078 0.646
AC12 0.017 0.018 0.082 0.174 1.263
AC13 0.013 0.011 0.024 0.126 0.856
AC14 0.013 0.011 0.024 0.099 0.682
AC15 0.013 0.014 0.029 0.067 0.466
AC16 0.021 0.012 0.054 0.168 1.281
AC17 0.016 0.011 0.065 0.198 1.362
AC18 0.031 0.013 0.236 0.412 2.842
AC19 0.028 0.026 0.177 1.312 1.233
AC20 0.014 0.013 0.092 0.165 1.088
AC21 0.042 0.019 0.851 0.729 5.048
AC22 0.030 0.016 0.260 0.587 4.259
AC23 0.022 0.011 0.081 0.273 1.928
AC24 0.017 0.011 0.060 0.169 1.162
AC26 0.017 0.010 0.024 0.177 1.124
AC27 0.020 0.013 0.066 0.251 1.543
AC28 0.015 0.010 0.010 0.372 4.143
AC29 0.025 0.057 0.255 0.207 2.366
AC41 0.011 0.013 0.134 0.147 1.163
AC42 0.018 0.013 0.164 0.179 2.409
AC43 0.017 0.013 0.148 0.195 0.974
AC44 0.016 0.013 0.249 0.288 2.226
AC45 0.018 0.015 0.233 0.216 1.241
AC46 0.024 0.017 1.357 0.741 30.535
AC47 0.021 0.015 0.291 0.318 2.434
AC48 0.017 0.009 0.017 0.089 0.469
AC49 0.012 0.009 0.011 0.807 3.122
AC50 0.015 0.013 0.013 1.045 12.571
AC51 0.014 0.010 0.029 0.062 0.435
AC52 0.022 0.009 0.019 0.087 0.593
AC53 0.011 0.009 0.009 0.070 0.539
AC54 0.014 0.014 0.015 0.376 3.008
BAG_complete-noand 0.489 0.058 5.828 2.697 22.132
BAG_complete 0.128 0.039 3.032 1.350 12.225
BAG_nokinds-noand 0.100 0.028 1.236 1.166 6.959
BAG_nokinds 0.046 0.021 0.963 0.790 7.233
BAG_nosorts-noand 0.046 0.021 0.319 0.410 2.940
BAG_nosorts 0.026 0.013 0.137 0.332 2.174
DP93_d2 0.014 0.008 0.127 0.177 1.279
DP93_d3 0.021 0.012 0.233 0.277 2.507
GK01_eqtheory_add 0.012 0.011 0.120 0.126 0.752
ICS 0.012 0.010 0.008 0.012 0.034
IJCAR_AC1 0.018 0.013 0.107 0.221 1.284
K00_Ex4-2-30 0.017 0.012 0.050 0.091 0.640
K00_Ex5-4-2 0.014 0.007 0.032 0.036 0.308
K00_max 0.015 0.010 0.009 0.413 11.164
LS94_G0 0.013 0.014 0.016 0.101 1.099
LS94_G2 0.020 0.117 0.061 0.183 0.926
MU98_binarith1 0.017 0.015 0.070 0.128 0.876
MU98_binarith2 0.018 0.011 0.068 0.201 1.168
MU98_multisets 0.017 0.014 0.081 0.167 0.920
MU98_ternary_addition 0.024 0.022 0.240 0.285 1.365
MU98_ternary_arith 0.025 0.013 0.195 0.355 2.697
PEANO-NAT_complete-noand 2.596 0.152 12.193 5.946 ⊥
PEANO-NAT_complete 0.443 0.068 6.335 2.514 34.958
PEANO-NAT_nokinds-noand 0.335 0.043 3.888 1.998 26.315
PEANO-NAT_nokinds 0.118 0.035 3.079 1.568 20.682
PEANO-NAT_nosorts-noand 0.072 0.022 1.497 0.780 3.687
PEANO-NAT_nosorts 0.046 0.020 1.038 0.579 10.419
RENAMED-BOOL_complete-noand 0.660 0.059 4.838 2.646 23.212
RENAMED-BOOL_complete 0.135 0.038 3.464 1.315 9.241
RENAMED-BOOL_nokinds-noand 0.154 0.035 1.666 1.085 7.079
RENAMED-BOOL_nokinds 0.065 0.030 1.282 0.830 5.733
RENAMED-BOOL_nosorts-noand 0.052 0.021 0.435 0.354 1.968
RENAMED-BOOL_nosorts 0.028 0.017 0.242 0.257 1.635
abelian_groups 0.009 0.013 0.009 0.015 0.044
abelian_groups_action 0.013 0.016 0.027 0.047 0.357
abelian_groups_action_complete 0.017 0.015 0.053 0.154 1.293
abelian_groups_comm_action 0.015 0.013 2.520 0.306 1.648
abelian_groups_homomorphism 0.010 0.014 0.016 0.051 0.303
ackbo_vs_kv1 0.014 0.011 0.045 0.067 0.464
ackbo_vs_kv2 0.029 0.022 0.248 1.233 0.861
anf 0.014 0.015 0.021 0.084 0.510
arithmetic 0.013 0.010 0.020 0.085 0.684
arithmetic_exp 0.014 0.010 0.054 0.186 1.208
assoc_comm_ring_unit 0.011 0.010 0.016 0.061 0.363
assoc_ring_unit 0.011 0.009 0.055 0.125 0.848
bag-sum-prod-bin 0.022 0.017 0.137 0.326 2.032
bag-sum-prod-distr 0.029 0.016 0.139 0.362 2.325
bag-sum-prod 0.019 0.012 0.100 0.248 1.786
bimodule 0.020 0.016 0.155 0.356 2.664
bimodule_comm_ring 0.020 0.015 0.099 0.278 2.320
bool_ring 0.013 0.011 0.015 0.056 0.374
boolean_rings 0.022 0.015 0.022 0.125 0.677
comm_assoc_ring_homomorphism 0.012 0.013 0.139 0.238 1.313
comm_monoid 0.012 0.011 0.009 0.016 0.025
differ 0.025 0.011 0.326 0.476 3.137
distr_lattice 0.012 0.008 0.010 0.043 0.300
example10 0.011 0.012 0.028 0.030 0.095
example_kv 0.109 0.013 0.050 0.176 1.157
field 0.014 0.012 0.054 0.114 0.734
finite_group 0.013 0.032 0.041 0.086 0.300
height 0.012 0.023 0.048 0.144 1.168
intersect 0.016 0.011 0.062 0.163 0.904
inverse_property 0.012 0.010 0.012 0.020 0.097
kusakari1 0.016 0.011 0.069 0.068 0.418
kv_vs_ackbo1 0.012 0.016 0.192 0.118 4.492
kv_vs_ackbo2 0.027 0.016 0.318 0.163 1.226
lattice 0.012 0.010 0.008 0.025 0.154
lie_ring 0.013 0.010 0.055 0.166 1.068
maude2 0.029 0.017 0.727 0.543 11.640
max 0.016 0.009 0.009 0.383 8.915
max2 0.012 0.008 0.010 0.291 3.635
module 0.017 0.011 0.105 0.228 1.827
module_comm_ring 0.014 0.014 0.059 0.199 1.254
multisets 0.019 0.010 0.070 0.145 0.902
multisets_binary 0.017 0.011 0.042 0.133 0.812
my_addition 0.011 0.010 0.008 0.181 52.327
nondeterministic_machines 0.022 0.010 0.061 0.171 1.188
popplestone_robot 0.018 0.015 0.399 0.412 3.972
rationals 0.070 0.030 2.806 2.156 18.154
ring 0.012 0.013 0.026 0.062 0.472
ring_unit 0.011 0.011 0.023 0.082 0.563
ring_unit_chomo 0.015 0.010 0.041 0.155 1.071
ring_unit_homo 0.017 0.011 0.034 0.116 0.727
semilattice 0.009 0.007 0.012 0.009 0.012
semiring 0.011 0.008 0.015 0.071 0.464
semiring_unit_chomo 0.016 0.014 0.039 0.186 1.220
semiring_unit_homo1 0.012 0.011 0.033 0.125 0.733
semiring_unit_homo5 0.016 0.016 0.112 0.282 1.732
sequent_modulo 0.069 0.032 2.056 2.110 20.381
slothrop_equiv_proofs 0.038 0.023 0.040 0.204 1.410
slothrop_equiv_proofs2 0.015 0.018 0.030 0.009 0.009
strange_addition 0.011 0.009 0.008 0.158 52.118
sum 0.018 0.010 0.008 0.438 7.032
totality 0.044 0.024 0.074 1.155 4.644
successes63 32 37 24 28
total time7.877 2.568 70.872 59.029 629.193

Legend
0./ttt2 -t -s 'acrpo -direct'
1./ttt2 -t -s 'ackbo -ib 4 -ob 5 -direct -nt'
2./ttt2 -t -s 'ackbo -ib 4 -ob 5 -sc -direct -nt'
3./ttt2 -t -s 'matrix -ac -dim 1 -ib 4 -ob 5 -direct'
4./ttt2 -t -s 'matrix -ac -dim 2 -ib 4 -ob 5 -direct'