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. Columns 0 and 1 apply our version of AC-KBO, the latter allows partial precedences. Columns 2 and 3 use Steinbach's version, the latter allows partial precedences. Finally, 4 and 5 correspond to our AC-KBO with subterm coefficients, where again 5 allows partial precedences. For all settings we used 4 input and 5 output bits.

 012345
A95_bincoeff 0.008 0.008 0.018 0.009 0.121 0.158
A95_finite_comm_monoid 0.019 0.015 0.015 0.022 0.285 0.306
A95_homomorphism 0.022 0.057 0.031 0.011 0.109 0.084
A95_integers 0.014 0.015 0.014 0.012 0.134 0.141
A95_listaddition 0.017 0.014 0.018 0.019 0.187 0.175
A95_listaddition2 0.019 0.016 0.018 0.016 0.178 0.174
A95_naturals 0.013 0.010 0.013 0.013 0.124 0.117
A95_proplogic 0.012 0.013 0.010 0.014 0.009 0.009
A95_proplogic2 0.011 0.009 0.009 0.009 0.050 0.040
AC01 0.008 0.008 0.013 0.007 0.031 0.029
AC02 0.011 0.007 0.010 0.007 0.032 0.034
AC03 0.009 0.009 0.008 0.011 0.120 0.102
AC04 0.011 0.007 0.009 0.008 0.158 0.143
AC05 0.012 0.009 0.009 0.010 0.009 0.010
AC06 0.009 0.009 0.010 0.010 0.192 0.205
AC07 0.014 0.010 0.011 0.010 0.010 0.010
AC08 0.011 0.010 0.013 0.010 0.191 0.201
AC09 0.011 0.012 0.012 0.009 0.129 0.119
AC10 0.010 0.008 0.007 0.007 0.091 0.091
AC11 0.036 0.027 0.020 0.020 0.377 0.350
AC12 0.015 0.015 0.012 0.011 0.390 0.397
AC13 0.011 0.009 0.013 0.009 0.118 0.116
AC14 0.008 0.008 0.008 0.008 0.092 0.092
AC15 0.016 0.015 0.011 0.011 0.120 0.112
AC16 0.011 0.010 0.008 0.012 0.257 0.229
AC17 0.015 0.009 0.009 0.009 0.311 0.322
AC18 0.012 0.011 0.014 0.013 0.619 0.553
AC19 0.033 0.024 0.020 0.014 0.527 0.480
AC20 0.008 0.009 0.012 0.009 0.160 0.143
AC21 0.020 0.024 0.020 0.019 1.427 1.263
AC22 0.015 0.014 0.013 0.013 1.093 1.102
AC23 0.010 0.011 0.012 0.011 0.545 0.547
AC24 0.013 0.008 0.009 0.009 0.289 0.266
AC26 0.009 0.009 0.011 0.008 0.227 0.245
AC27 0.017 0.014 0.010 0.011 0.287 0.273
AC28 0.008 0.011 0.009 0.008 0.008 0.008
AC29 0.181 0.067 0.174 0.065 0.489 0.297
AC41 0.009 0.009 0.009 0.009 0.159 0.164
AC47 0.012 0.011 0.012 0.011 0.545 0.318
AC48 0.008 0.011 0.012 0.008 0.072 0.069
AC49 0.009 0.011 0.008 0.012 0.009 0.008
AC50 0.012 0.018 0.010 0.012 0.020 0.015
AC51 0.010 0.010 0.009 0.008 0.139 0.121
AC52 0.013 0.009 0.010 0.007 0.133 0.131
AC53 0.011 0.008 0.007 0.007 0.007 0.007
AC54 0.011 0.013 0.011 0.011 0.012 0.011
BAG_complete-noand 0.167 0.063 0.170 0.080 42.544 5.720
BAG_complete 0.058 0.034 0.060 0.033 4.372 3.464
BAG_nokinds-noand 0.044 0.027 0.049 0.026 2.169 1.646
BAG_nokinds 0.023 0.019 0.024 0.021 1.606 1.306
BAG_nosorts-noand 0.022 0.015 0.020 0.016 0.840 0.557
BAG_nosorts 0.016 0.014 0.012 0.014 0.434 0.371
DP93_d2 0.008 0.011 0.008 0.009 0.226 0.205
DP93_d3 0.009 0.010 0.011 0.011 0.303 0.324
GK01_eqtheory_add 0.009 0.008 0.007 0.011 0.148 0.142
ICS 0.010 0.008 0.012 0.008 0.007 0.007
IJCAR_AC1 0.009 0.012 0.010 0.012 0.170 0.153
K00_Ex4-2-30 0.011 0.010 0.011 0.012 0.118 0.114
K00_Ex5-4-2 0.007 0.007 0.008 0.012 0.045 0.054
K00_max 0.008 0.009 0.013 0.011 0.009 0.008
LS94_G0 0.019 0.018 0.015 0.014 0.023 0.022
LS94_G2 0.111 0.118 0.115 0.117 1.185 1.107
MU98_binarith1 0.013 0.015 0.013 0.017 0.249 0.217
MU98_binarith2 0.010 0.010 0.009 0.008 0.270 0.266
MU98_multisets 0.012 0.016 0.010 0.009 0.165 0.163
MU98_ternary_addition 0.018 0.025 0.022 0.019 0.751 0.701
MU98_ternary_arith 0.014 0.011 0.016 0.012 0.550 0.589
abelian_groups 0.012 0.012 0.011 0.020 0.014 0.013
abelian_groups_action 0.012 0.016 0.012 0.014 0.042 0.040
abelian_groups_action_complete 0.015 0.017 0.015 0.016 0.226 0.210
abelian_groups_comm_action 0.011 0.010 0.010 0.009 3.736 2.724
abelian_groups_homomorphism 0.012 0.015 0.013 0.011 0.052 0.051
ackbo_vs_kv1 0.012 0.011 0.009 0.009 0.147 0.150
ackbo_vs_kv2 0.021 0.019 0.017 0.017 0.417 0.364
anf 0.008 0.007 0.007 0.007 0.121 0.108
arithmetic 0.009 0.008 0.008 0.009 0.111 0.105
arithmetic_exp 0.009 0.010 0.009 0.009 0.194 0.192
assoc_comm_ring_unit 0.007 0.007 0.007 0.007 0.057 0.057
assoc_ring_unit 0.009 0.009 0.008 0.011 0.111 0.110
bag-sum-prod-bin 0.013 0.012 0.013 0.011 0.422 0.375
bag-sum-prod-distr 0.011 0.011 0.012 0.010 0.427 0.415
bag-sum-prod 0.016 0.011 0.012 0.010 0.311 0.276
bimodule 0.013 0.011 0.018 0.012 0.346 0.325
bimodule_comm_ring 0.012 0.011 0.013 0.011 0.352 0.277
bool_ring 0.010 0.008 0.009 0.008 0.076 0.058
boolean_rings 0.014 0.013 0.009 0.010 0.141 0.140
comm_assoc_ring_homomorphism 0.011 0.010 0.011 0.011 0.205 0.202
comm_monoid 0.009 0.007 0.008 0.008 0.007 0.012
differ 0.014 0.011 0.012 0.011 1.156 0.964
distr_lattice 0.007 0.007 0.008 0.007 0.051 0.048
example10 0.012 0.011 0.011 0.011 0.059 0.055
example_kv 0.013 0.012 0.010 0.009 0.316 0.341
field 0.009 0.010 0.010 0.009 0.124 0.120
finite_group 0.044 0.036 0.036 0.037 0.307 0.296
height 0.023 0.017 0.019 0.020 0.159 0.142
intersect 0.011 0.013 0.010 0.010 0.151 0.151
inverse_property 0.007 0.007 0.007 0.008 0.007 0.007
kusakari1 0.009 0.008 0.008 0.009 0.187 0.180
kv_vs_ackbo1 0.010 0.009 0.009 0.008 0.306 0.342
kv_vs_ackbo2 0.020 0.016 0.016 0.014 0.572 0.495
lattice 0.007 0.011 0.007 0.012 0.007 0.009
lie_ring 0.009 0.009 0.009 0.008 0.223 0.222
max 0.009 0.008 0.012 0.007 0.008 0.008
max2 0.009 0.009 0.013 0.008 0.012 0.010
module 0.011 0.011 0.012 0.010 0.237 0.224
module_comm_ring 0.011 0.010 0.010 0.009 0.234 0.194
multisets 0.011 0.008 0.011 0.010 0.154 0.136
multisets_binary 0.014 0.013 0.010 0.009 0.160 0.139
nondeterministic_machines 0.008 0.008 0.008 0.007 0.236 0.240
popplestone_robot 0.013 0.011 0.013 0.013 0.599 0.452
rationals 0.035 0.029 0.041 0.029 4.753 4.601
ring 0.008 0.007 0.007 0.007 0.077 0.076
ring_unit 0.010 0.008 0.009 0.009 0.081 0.075
ring_unit_chomo 0.010 0.009 0.013 0.009 0.170 0.165
ring_unit_homo 0.008 0.009 0.009 0.010 0.134 0.120
semilattice 0.006 0.008 0.006 0.009 0.007 0.007
semiring 0.007 0.007 0.007 0.007 0.066 0.068
semiring_unit_chomo 0.009 0.008 0.008 0.009 0.149 0.156
semiring_unit_homo1 0.010 0.011 0.010 0.008 0.127 0.106
semiring_unit_homo5 0.012 0.010 0.011 0.012 0.230 0.273
sequent_modulo 0.042 0.031 0.036 0.030 5.194 4.024
strange_addition 0.010 0.009 0.008 0.008 0.008 0.008
sum 0.009 0.009 0.009 0.009 0.013 0.013
totality 0.025 0.018 0.014 0.013 ⊥ 0.309
successes31 32 17 23 36 37
total time2.1 1.764 2.016 1.676 150.565 47.903

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