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

  mascott CiME
  AC ACU AG old auto    
1.93 82 1.89 70 0.10 8 3.71 163 0.10 8 ?
    12.35 49   12.47 49 ?
1.58 77 2.43 61 0.01 5 1.59 101 0.01 5 0.05 input
181.73 928 173.50 993 4.79 104 57.09 658 13.00 114 0.05 input
14.86 503 15.15 483 83.57 1156 13.04 562 13.83 483 ?
22.91 501 28.51 466 7.20 301 150.11 1239 0.05 9 0.1 input
125.27 756 85.91 429 242.64 1445 150.11 1239 18.59 424 0.1 input
2.87 199 2.76 185 - 2.69 224 3.04 185 ?  
18.10 816 17.54 781 - 18.66 973 17.26 781 ?  
0.3 26 0.2 17 - 0.3 32 0.3 26 ?  
    15.40 486   15.16 486 ?
    216.67 457   145.14 400 ?  
1.12 22 1.27 23 - 5.39 70 1.12 21 0.1 input
1.45 4 - - 0.33 11 1.47 4 ?  
119.55 991 77.15 668 214.49 1391   203.03 1391 0.07 input
85.15 938 88.97 863   72.43 871 9.80 253 0.1 input
3.33 209 3.57 192 - 10.91 291 3.52 193 0.1 input
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.