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 and Steinbach's AC-KBO, where for both cases partial precedences were allowed. Columns 3 and 4 correspond to Korovin & Voronkov's AC-KBO >kv and the simplification order >'kv, respectively. Finally, 5 corresponds to our AC-KBO with subterm coefficients, where again partial precedences are allowed. For all settings we used 4 input and 5 output bits.

 012345
A95_bincoeff 0.012 0.007 0.010 0.012 0.013 0.128
A95_finite_comm_monoid 0.012 0.016 0.014 0.025 0.044 0.300
A95_homomorphism 0.009 0.008 0.008 0.008 0.009 0.041
A95_integers 0.014 0.012 0.012 0.013 0.013 0.136
A95_listaddition 0.014 0.014 0.018 0.017 0.017 0.193
A95_listaddition2 0.016 0.019 0.015 0.019 0.018 0.166
A95_naturals 0.010 0.013 0.011 0.013 0.012 0.130
A95_proplogic 0.010 0.008 0.008 0.009 0.009 0.012
A95_proplogic2 0.009 0.012 0.009 0.009 0.012 0.041
AC01 0.011 0.013 0.011 0.011 0.011 0.031
AC02 0.015 0.009 0.008 0.011 0.006 0.032
AC03 0.011 0.008 0.008 0.008 0.008 0.103
AC04 0.011 0.008 0.009 0.008 0.008 0.152
AC05 0.011 0.013 0.009 0.010 0.011 0.009
AC06 0.016 0.013 0.009 0.011 0.010 0.215
AC07 0.012 0.011 0.014 0.014 0.009 0.013
AC08 0.014 0.011 0.014 0.012 0.010 0.190
AC09 0.013 0.010 0.009 0.009 0.008 0.126
AC10 0.013 0.009 0.009 0.008 0.008 0.112
AC11 0.034 0.036 0.020 0.039 0.049 0.348
AC12 0.022 0.015 0.012 0.019 0.022 0.391
AC13 0.013 0.008 0.008 0.008 0.011 0.116
AC14 0.011 0.012 0.007 0.009 0.007 0.098
AC15 0.011 0.014 0.010 0.016 0.016 0.111
AC16 0.020 0.009 0.011 0.008 0.008 0.226
AC17 0.013 0.008 0.011 0.012 0.011 0.282
AC18 0.024 0.011 0.014 0.011 0.011 0.607
AC19 0.026 0.020 0.014 0.032 0.046 0.514
AC20 0.014 0.009 0.008 0.009 0.008 0.142
AC21 0.041 0.017 0.018 0.020 0.021 1.189
AC22 0.031 0.015 0.013 0.013 0.014 0.970
AC23 0.021 0.011 0.010 0.014 0.010 0.495
AC24 0.018 0.009 0.011 0.010 0.009 0.265
AC26 0.014 0.008 0.009 0.008 0.011 0.246
AC27 0.020 0.009 0.009 0.010 0.010 0.294
AC28 0.014 0.008 0.008 0.009 0.011 0.008
AC29 0.019 0.067 0.061 0.171 0.181 0.290
AC41 0.011 0.008 0.009 0.010 0.009 0.162
AC47 0.019 0.012 0.011 0.012 0.016 0.345
AC48 0.012 0.010 0.007 0.008 0.008 0.075
AC49 0.014 0.008 0.009 0.009 0.009 0.009
AC50 0.016 0.010 0.010 0.011 0.011 0.011
AC51 0.014 0.011 0.012 0.009 0.009 0.138
AC52 0.020 0.008 0.010 0.008 0.010 0.131
AC53 0.008 0.010 0.008 0.008 0.009 0.007
AC54 0.013 0.011 0.010 0.012 0.011 0.012
BAG_complete-noand 0.508 0.064 0.065 0.175 0.175 4.927
BAG_complete 0.126 0.040 0.034 0.060 0.056 3.270
BAG_nokinds-noand 0.099 0.023 0.028 0.044 0.045 1.472
BAG_nokinds 0.043 0.019 0.020 0.025 0.028 1.171
BAG_nosorts-noand 0.046 0.015 0.015 0.021 0.022 0.593
BAG_nosorts 0.025 0.013 0.011 0.012 0.013 0.371
DP93_d2 0.017 0.009 0.008 0.009 0.010 0.220
DP93_d3 0.016 0.009 0.011 0.010 0.009 0.296
GK01_eqtheory_add 0.011 0.008 0.008 0.008 0.008 0.132
ICS 0.010 0.007 0.010 0.007 0.008 0.009
IJCAR_AC1 0.012 0.009 0.009 0.010 0.010 0.151
K00_Ex4-2-30 0.010 0.013 0.011 0.011 0.010 0.106
K00_Ex5-4-2 0.010 0.006 0.009 0.006 0.006 0.049
K00_max 0.018 0.010 0.013 0.009 0.009 0.009
LS94_G0 0.011 0.014 0.013 0.015 0.015 0.020
LS94_G2 0.014 0.109 0.111 0.120 0.114 1.102
MU98_binarith1 0.016 0.011 0.015 0.012 0.011 0.216
MU98_binarith2 0.015 0.009 0.011 0.012 0.009 0.290
MU98_multisets 0.019 0.010 0.009 0.011 0.011 0.140
MU98_ternary_addition 0.023 0.019 0.018 0.020 0.018 0.619
MU98_ternary_arith 0.027 0.013 0.014 0.011 0.012 0.579
RENAMED-BOOL_complete-noand 0.703 0.065 0.068 0.217 0.247 5.146
RENAMED-BOOL_complete 0.152 0.039 0.040 0.064 0.064 3.821
RENAMED-BOOL_nokinds-noand 0.155 0.036 0.037 0.065 0.065 2.103
RENAMED-BOOL_nokinds 0.070 0.027 0.027 0.038 0.039 1.800
RENAMED-BOOL_nosorts-noand 0.052 0.021 0.027 0.031 0.032 0.579
RENAMED-BOOL_nosorts 0.031 0.016 0.016 0.019 0.018 0.433
abelian_groups 0.009 0.013 0.012 0.014 0.012 0.012
abelian_groups_action 0.009 0.013 0.014 0.012 0.012 0.043
abelian_groups_action_complete 0.013 0.016 0.014 0.016 0.016 0.231
abelian_groups_comm_action 0.016 0.009 0.009 0.008 0.008 2.518
abelian_groups_homomorphism 0.010 0.013 0.012 0.012 0.012 0.054
ackbo_vs_kv1 0.010 0.010 0.009 0.010 0.011 0.156
ackbo_vs_kv2 0.024 0.018 0.015 0.020 0.020 0.363
anf 0.012 0.008 0.007 0.008 0.008 0.108
arithmetic 0.012 0.007 0.008 0.007 0.008 0.097
arithmetic_exp 0.013 0.010 0.009 0.010 0.009 0.192
assoc_comm_ring_unit 0.010 0.008 0.010 0.010 0.007 0.059
assoc_ring_unit 0.011 0.008 0.008 0.008 0.007 0.118
bag-sum-prod-bin 0.021 0.011 0.014 0.011 0.011 0.374
bag-sum-prod-distr 0.023 0.014 0.013 0.013 0.012 0.415
bag-sum-prod 0.016 0.010 0.010 0.011 0.012 0.300
bimodule 0.018 0.014 0.012 0.012 0.013 0.300
bimodule_comm_ring 0.017 0.010 0.011 0.011 0.012 0.302
bool_ring 0.010 0.007 0.010 0.008 0.007 0.054
boolean_rings 0.015 0.009 0.012 0.011 0.009 0.160
comm_assoc_ring_homomorphism 0.015 0.012 0.009 0.010 0.011 0.240
comm_monoid 0.008 0.007 0.007 0.006 0.007 0.007
differ 0.025 0.010 0.010 0.011 0.013 0.965
distr_lattice 0.012 0.011 0.007 0.007 0.008 0.044
example10 0.009 0.017 0.012 0.013 0.013 0.051
example_kv 0.071 0.014 0.009 0.013 0.013 0.311
field 0.012 0.008 0.008 0.008 0.009 0.132
finite_group 0.013 0.037 0.036 0.040 0.040 0.275
height 0.012 0.023 0.021 0.024 0.025 0.145
intersect 0.015 0.011 0.008 0.015 0.009 0.132
inverse_property 0.009 0.008 0.007 0.007 0.007 0.007
kusakari1 0.012 0.009 0.009 0.008 0.009 0.172
kv_vs_ackbo1 0.010 0.012 0.009 0.011 0.016 0.360
kv_vs_ackbo2 0.025 0.015 0.015 0.021 0.026 0.494
lattice 0.012 0.008 0.012 0.007 0.008 0.008
lie_ring 0.013 0.010 0.011 0.010 0.009 0.223
max 0.016 0.009 0.008 0.008 0.008 0.008
max2 0.011 0.008 0.008 0.007 0.008 0.007
module 0.014 0.010 0.010 0.009 0.011 0.244
module_comm_ring 0.015 0.011 0.009 0.016 0.010 0.210
multisets 0.015 0.009 0.009 0.009 0.009 0.148
multisets_binary 0.015 0.009 0.011 0.009 0.009 0.138
nondeterministic_machines 0.021 0.007 0.008 0.008 0.008 0.225
popplestone_robot 0.016 0.011 0.014 0.012 0.012 0.502
rationals 0.070 0.032 0.029 0.033 0.035 4.990
ring 0.010 0.007 0.007 0.007 0.008 0.072
ring_unit 0.012 0.009 0.008 0.010 0.008 0.075
ring_unit_chomo 0.014 0.010 0.009 0.009 0.010 0.155
ring_unit_homo 0.013 0.008 0.010 0.008 0.009 0.118
semilattice 0.008 0.006 0.006 0.008 0.006 0.007
semiring 0.012 0.008 0.007 0.008 0.008 0.067
semiring_unit_chomo 0.012 0.010 0.010 0.009 0.009 0.146
semiring_unit_homo1 0.013 0.008 0.009 0.009 0.009 0.115
semiring_unit_homo5 0.013 0.010 0.014 0.010 0.010 0.246
sequent_modulo 0.069 0.029 0.028 0.033 0.034 4.561
strange_addition 0.009 0.008 0.010 0.011 0.007 0.007
sum 0.015 0.011 0.008 0.008 0.008 0.008
totality 0.042 0.024 0.014 0.026 0.030 0.292
successes63 32 23 30 30 37
total time2.779 1.692 1.633 2.03 2.078 47.117

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 -st -nt -direct'
3./ttt2 -t -s 'ackbo -ib 4 -ob 5 -kv -direct'
4./ttt2 -t -s 'ackbo -ib 4 -ob 5 -kv2 -direct'
5./ttt2 -t -s 'ackbo -ib 4 -ob 5 -sc -direct -nt'