The following experiments were conducted on a Intel Core Duo @ 1.4 GHz.

  mkbtt CiME
  AC ACU AG old auto    
LS94_G0 1.93 82 1.89 70 0.10 8 3.71 163 0.10 8 ?
LS94_G2 ∞   ∞   12.35 49 ∞   12.47 49 ?
abelian_groups 1.58 77 2.43 61 0.01 5 1.59 101 0.01 5 0.05 input
abelian_groups_homomorphism 181.73 928 173.50 993 4.79 104 57.09 658 13.00 114 0.05 input
arithmetic 2 14.86 503 15.15 483 83.57 1156 13.04 562 13.83 483 ?
assoc_comm_ring_unit 3 22.91 501 28.51 466 7.20 301 150.11 1239 0.05 9 0.1 input
binary arithmetic 1 2.87 199 2.76 185 - 2.69 224 3.04 185 ?  
ternary arithmetic 1 18.10 816 17.54 781 - 18.66 973 17.26 781 ?  
Example 4.1 0.3 26 0.2 17 - 0.3 32 0.3 26 ?  
Example 5.1 ∞   ∞   15.40 486 ∞   15.16 486 ?
Example 5.2 ∞   ∞   216.67 457 ∞   145.14 400 ?  
semiring 2 3.33 209 3.57 192 - 10.91 291 3.52 193 0.1 input
sum 1.44 4 - - 0.40 18 1.44 4 ?

Explanation of Symbols
∞ timeout (300 seconds)
? no appropriate reduction order known that could be used by CiME
- theory not applicable for problem
⊥ failure of completion

Sources of Problems
1 C. Marché and X.Urbain. Modular and incremental proofs of AC-termination. JSC, 38(1):873–897, 2004
2 K. Kusakari. Termination, AC-Termination and Dependency Pairs of Term Rewriting Systems. Ph.D. Thesis, JAIST, 2000
3 P. LeChenadec. Canonical Forms in Finitely Presented Algebras. Pitman, 1986
4 W. Gehrke. Detailed Catalogue of Canonical Term Rewriting Systems Generated Automatically. RISC Report Series 92-64, University of Linz, 1992
5 these finite group representations were obtained by making groups from the following paper Abelian: S. Linton and D. Shand. Some group theoretic examples with completion theorem provers. Journal of Automated Reasoning, 17(2):145-169, 1996.
The remaining problems were added by the authors.