AC-KBO
Home
AC-KBO
experiments downloads

Completion 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 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.

 01234
A95_bincoeff 0.15 ∞ ∞ ⊥ ⊥
A95_finite_comm_monoid 0.12 0.11 0.51 0.16 0.39
A95_homomorphism 0.06 0.07 0.07 0.09 0.18
A95_integers 0.39 0.43 0.79 ⊥ ⊥
A95_listaddition 0.71 0.76 2.32 ⊥ ⊥
A95_listaddition2 0.75 0.75 1.66 ⊥ ⊥
A95_naturals 0.26 0.22 0.39 0.42 1.27
A95_proplogic 0.10 0.12 0.11 0.12 0.26
A95_proplogic2 0.08 0.07 0.13 ⊥ 5.02
DP93_d2 0.66 ∞ 1.36 0.59 2.97
DP93_d3 1.62 ∞ 3.92 1.47 20.33
GK01_eqtheory_add ∞ ∞ ∞ ∞ ∞
ICS 0.03 0.04 0.04 0.04 0.05
K00_ex5_4_2 0.15 0.16 0.23 0.22 0.63
K00_max ⊥ ∞ ∞ ∞ ⊥
LS94_G0 0.22 0.25 0.29 ⊥ ⊥
LS94_G2 0.24 0.45 1.15 ⊥ 1.11
MU98_balanced_ternary_add ⊥ ∞ ∞ ⊥ ∞
MU98_binarith1 ⊥ 0.38 1.32 ⊥ ⊥
MU98_binarith1b ⊥ ∞ 2.94 ⊥ ⊥
MU98_binarith2 ∞ ∞ ∞ ∞ ∞
MU98_multisets 0.47 ∞ ∞ ∞ ∞
MU98_ternary_add ⊥ 1.54 9.42 ⊥ ∞
MU98_ternary_arith ∞ ∞ ∞ ⊥ ∞
abelian_groups 0.05 0.05 0.06 0.07 0.10
abelian_groups_action 0.35 0.64 0.94 1.46 6.02
abelian_groups_comm_action ⊥ ⊥ ⊥ ⊥ ∞
abelian_groups_homomorphism 0.13 0.14 0.17 ⊥ ⊥
anf ∞ ∞ ∞ ⊥ ⊥
arithmetic ⊥ ⊥ ⊥ ⊥ ⊥
arithmetic_exp ∞ ∞ ∞ ∞ ∞
assoc_comm_ring_unit 0.10 0.11 0.12 0.13 0.32
assoc_ring_unit ∞ ∞ ⊥ ⊥ ⊥
bimodule ∞ ∞ ∞ ∞ ∞
bimodule_comm_ring ∞ ∞ ∞ ∞ ∞
bool_ring ∞ ∞ ∞ ⊥ ⊥
comm_assoc_ring_homomorphism ∞ ∞ ∞ ∞ ∞
comm_monoid 0.02 0.02 0.03 0.02 0.04
distr_lattice ∞ ∞ ∞ ∞ ∞
example10 ⊥ ⊥ ⊥ ⊥ ⊥
field 1.62 0.93 3.57 ⊥ ⊥
finite_group 0.19 0.20 0.36 0.23 0.50
height ∞ 0.37 0.57 0.59 2.00
inverse_property 0.06 0.07 0.07 0.10 0.25
lattice 0.08 0.06 0.06 0.09 0.22
lie_ring ∞ ∞ ∞ ∞ ∞
max ⊥ ∞ ∞ ∞ ⊥
max2 ∞ ∞ ∞ ∞ ⊥
module ∞ ∞ ∞ ∞ ∞
module_comm_ring ∞ ∞ ∞ ∞ ∞
multisets 0.47 ∞ ∞ ⊥ ⊥
multisets_binary 0.99 ∞ ∞ ∞ ∞
nondeterministic_machines ∞ ∞ ∞ ∞ ⊥
popplestone_robot ∞ ∞ ∞ ∞ ∞
ring ∞ ⊥ ⊥ ⊥ ⊥
ring_unit ∞ ∞ ⊥ ⊥ ⊥
ring_unit_chomo ∞ ∞ ⊥ ⊥ ∞
ring_unit_homo ∞ ∞ ⊥ ⊥ ⊥
semilattice 0.02 0.01 0.03 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 28 17 19
total time234010.09 252007.95 234032.63 300005.82 288041.68
∅ time0.360 0.318 1.165 0.342 2.194

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 -nt'
2./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'ackbo -ib 2 -ob 3 -direct -sc -nt'
3./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'matrix -ac -ib 2 -ob 3 -dim 1 -direct'
4./mkbtt -ct -st -cp prime -T 1.5 -t 200 -s 'matrix -ac -ib 2 -ob 3 -dim 2 -direct'