AC-KBO
Home
AC-KBO
experiments downloads

Completion Experiments

AC-KBO Experiments

The following table collects results obtained with mkbtt running normalized completion with different versions of AC-KBO. A tarball containing all input systems 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 200 seconds. Each termination call had a timeout of 1.5 seconds, and the primality critical pair criterion was used.

The columns correspond to the following settings. Column 0 uses AC-RPO. Columns 1 and 2 apply our version of AC-KBO, in the latter case allowing partial precedences. Columns 3 and 4 use Steinbach's AC-KBO, in the latter case allowing partial precedences. Columns 5 and 6 correspond to Korovin & Voronkov's AC-KBO >kv and the simplification order >'kv, respectively. Finally, 7 and 8 correspond to our AC-KBO with subterm coefficients, where for 8 partial precedences are allowed. For all settings we used 2 input and 3 output bits.

 012345678
A95_bincoeff 0.21 ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞
A95_finite_comm_monoid 0.13 0.12 0.13 0.13 0.13 0.16 0.21 0.50 0.51
A95_homomorphism 0.07 0.07 0.07 0.10 0.09 0.07 0.07 0.08 0.09
A95_integers 0.41 0.55 0.48 0.43 0.40 0.57 0.55 0.86 0.81
A95_listaddition 0.88 0.97 0.84 0.57 0.54 0.95 0.96 2.49 2.27
A95_listaddition2 0.82 0.93 0.80 ⊥ 0.54 0.93 0.98 1.76 1.60
A95_naturals 0.28 0.28 0.24 ⊥ 0.22 0.26 0.25 0.42 0.38
A95_proplogic 0.11 0.09 0.07 ⊥ 0.08 0.09 0.09 0.09 0.10
A95_proplogic2 0.09 0.09 0.08 ⊥ 0.08 0.08 0.08 0.13 0.12
DP93_d2 0.80 ∞ ∞ ∞ ∞ ∞ ∞ 1.50 1.47
DP93_d3 1.97 ∞ ∞ ∞ ∞ ∞ ∞ 4.40 4.29
GK01_eqtheory_add ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞
ICS 0.04 0.03 0.03 0.03 0.03 0.03 0.03 0.03 0.04
K00_ex5_4_2 0.17 0.16 0.19 0.18 0.18 0.16 0.17 0.24 0.25
K00_max ⊥ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞
LS94_G0 0.25 0.28 0.26 0.27 0.25 0.27 0.28 0.32 0.29
LS94_G2 0.27 0.47 0.44 0.51 0.47 0.48 0.50 1.14 1.16
MU98_balanced_ternary_add ⊥ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞
MU98_binarith1 ⊥ 0.43 0.43 0.19 0.19 0.44 0.46 1.26 1.26
MU98_binarith1b ⊥ ∞ ∞ ∞ ∞ ∞ ∞ 3.35 3.31
MU98_binarith2 ∞ ∞ ∞ ⊥ ∞ ∞ ∞ ∞ ∞
MU98_multisets 0.56 ∞ ∞ ⊥ ∞ ∞ ∞ ∞ ∞
MU98_ternary_add ⊥ 1.83 1.69 0.39 0.41 1.77 1.84 9.93 10.33
MU98_ternary_arith ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞
abelian_groups 0.06 0.05 0.05 0.05 0.05 0.05 0.06 0.05 0.05
abelian_groups_action 0.41 0.74 0.70 0.72 0.71 0.73 0.70 1.02 1.00
abelian_groups_comm_action ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥
abelian_groups_homomorphism 0.14 0.17 0.15 0.15 0.15 0.17 0.16 0.19 0.18
anf ∞ ∞ ∞ ⊥ ∞ ∞ ∞ ∞ ∞
arithmetic ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥
arithmetic_exp ∞ ∞ ∞ ⊥ ∞ ∞ ∞ ∞ ∞
assoc_comm_ring_unit 0.10 0.13 0.10 ⊥ 0.12 0.11 0.11 0.13 0.11
assoc_ring_unit ∞ ∞ ∞ ∞ ∞ ∞ ∞ ⊥ ⊥
bimodule ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞
bimodule_comm_ring ∞ ∞ ∞ ⊥ ∞ ∞ ∞ ∞ ∞
bool_ring ∞ ∞ ∞ ⊥ ⊥ ∞ ∞ ∞ ∞
comm_assoc_ring_homomorphism ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞
comm_monoid 0.02 0.02 0.02 0.02 0.02 0.02 0.02 0.02 0.02
distr_lattice ∞ ∞ ∞ ⊥ ∞ ∞ ∞ ∞ ∞
example10 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥
field 1.86 1.20 1.05 ∞ ∞ 1.17 1.21 4.02 3.92
finite_group 0.18 0.26 0.24 0.23 0.22 0.25 0.23 0.40 0.38
height ∞ 0.46 0.40 ⊥ 0.43 0.46 0.46 0.66 0.59
inverse_property 0.06 0.06 0.06 0.06 0.05 0.05 0.06 0.06 0.06
lattice 0.05 0.07 0.06 ⊥ 0.06 0.06 0.06 0.06 0.06
lie_ring ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞
max ⊥ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞
max2 ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞
module ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞
module_comm_ring ∞ ∞ ∞ ⊥ ∞ ∞ ∞ ∞ ∞
multisets 0.51 ∞ ∞ ⊥ ∞ ∞ ∞ ∞ ∞
multisets_binary 1.17 ∞ ∞ ⊥ ∞ ∞ ∞ ∞ ∞
nondeterministic_machines ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞
popplestone_robot ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞
ring ∞ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥
ring_unit ∞ ∞ ∞ ∞ ∞ ∞ ∞ ⊥ ⊥
ring_unit_chomo ∞ ∞ ∞ ∞ ∞ ∞ ∞ ⊥ ⊥
ring_unit_homo ∞ ∞ ∞ ∞ ∞ ∞ ∞ ⊥ ⊥
semilattice 0.02 0.02 0.02 0.02 0.02 0.02 0.02 0.02 0.02
semiring ⊥ ∞ ∞ ⊥ ⊥ ∞ ∞ ⊥ ⊥
semiring_unit_chomo ∞ ∞ ∞ ∞ ∞ ∞ ∞ ⊥ ⊥
semiring_unit_homo1 ∞ ∞ ∞ ∞ ∞ ∞ ∞ ⊥ ⊥
semiring_unit_homo5 ∞ ∞ ∞ ∞ ∞ ∞ ∞ ⊥ ⊥
slothrop_equiv_proofs ⊥ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞
slothrop_equiv_proofs2 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥
strange_addition ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞
sum ⊥ ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞
successes28 25 25 17 24 25 25 28 28
total time 1701.64 2279.48 2278.60 1854.05 2235.44 2279.35 2279.56 1725.13 1724.67
∅ time0.42 0.38 0.34 0.24 0.23 0.37 0.38 1.25 1.24

Legend
0./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'acrpo -direct'
1./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'ackbo -ib 2 -ob 3 -direct'
2./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'ackbo -ib 2 -ob 3 -direct -nt'
3./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'ackbo -ib 2 -ob 3 -direct -st'
4./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'ackbo -ib 2 -ob 3 -direct -st -nt'
5./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'ackbo -ib 2 -ob 3 -direct -kv'
6./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'ackbo -ib 2 -ob 3 -direct -kv2'
7./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'ackbo -ib 2 -ob 3 -direct -sc'
8./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'ackbo -ib 2 -ob 3 -direct -sc -nt'