012
A95_bincoeff 0.44 1.40 2.25
A95_finite_comm_monoid 2.40 2.42 2.53
A95_homomorphism 0.16 0.16 0.19
A95_integers 1.09 1.37 2.55
A95_listaddition 16.87 17.66 21.27
A95_listaddition2 ∞ ∞ ∞
A95_naturals 0.46 0.50 0.94
A95_proplogic 2.45 2.42 2.46
A95_proplogic2 0.10 0.10 0.13
DP93_d2 5.97 2.51 6.72
DP93_d3 29.21 11.60 54.98
GK01_eqtheory_add 53.27 76.59 ∞
ICS 0.97 0.97 1.00
K00_ex5_4_2 ∞ ∞ ∞
K00_max 0.27 0.29 1.60
LS94_G0 1.04 1.50 1.67
LS94_G2 ∞ ∞ ∞
MU98_balanced_ternary_add ∞ ∞ ∞
MU98_binarith1 ∞ 1.22 2.15
MU98_binarith1b ∞ ∞ ∞
MU98_binarith2 ∞ ∞ ∞
MU98_multisets 2.22 ⊥ ⊥
MU98_ternary_add ∞ ∞ ∞
MU98_ternary_arith ∞ ∞ ∞
abelian_groups 0.93 1.27 1.33
abelian_groups_action ⊥ 3.76 4.12
abelian_groups_comm_action ∞ ∞ ∞
abelian_groups_homomorphism 4.28 7.03 7.38
anf ∞ ∞ ∞
arithmetic 3.81 ∞ ∞
arithmetic_exp ∞ ∞ ∞
assoc_comm_ring_unit 6.50 ∞ ∞
assoc_ring_unit 9.15 ∞ ∞
bimodule 109.29 ∞ ∞
bimodule_comm_ring ∞ ∞ ∞
bool_ring 8.47 ∞ ∞
comm_assoc_ring_homomorphism ∞ ∞ ∞
comm_monoid 0.02 0.02 0.03
distr_lattice ∞ ∞ ∞
example10 ⊥ ⊥ ⊥
field 9.06 ∞ ∞
finite_group 5.25 5.95 6.45
height 1.34 0.99 1.59
inverse_property ⊥ ⊥ ⊥
lattice ∞ ∞ ∞
lie_ring ∞ ∞ ∞
max 0.27 0.29 1.61
max2 0.28 0.33 1.61
module 33.22 ∞ ∞
module_comm_ring ∞ ∞ ∞
multisets 2.15 ⊥ ⊥
multisets_binary 4.47 ∞ ∞
nondeterministic_machines ∞ ∞ ∞
popplestone_robot ∞ ∞ ∞
ring 8.59 ∞ ∞
ring_unit 8.18 ∞ ∞
ring_unit_chomo ∞ ∞ ∞
ring_unit_homo ∞ ∞ ∞
semilattice 0.78 0.78 0.78
semiring 2.70 ∞ ⊥
semiring_unit_chomo ∞ ∞ ∞
semiring_unit_homo1 ∞ ∞ ∞
semiring_unit_homo5 ∞ ∞ ∞
slothrop_equiv_proofs ∞ ∞ ∞
slothrop_equiv_proofs2 ∞ ∞ ∞
strange_addition 0.12 0.13 0.32
sum 0.29 0.31 1.53
successes37 26 25
total time6336.07 8341.57 8527.19
∅ time9.08297297297297 5.445 5.0876

Legend
0./mkbtt -ct -st -cp prime -T 1.5 -t 200 -th theories/ac.trs -it acrpo
1./mkbtt -ct -st -cp prime -T 1.5 -t 200 -th theories/ac.trs -it 'ackbo -ib 2 -ob 3'
2./mkbtt -ct -st -cp prime -T 1.5 -t 200 -th theories/ac.trs -it 'ackbo -ib 2 -ob 3 -sc'