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

  mascott CiME
  internal AProVe muterm    
abelian_groups 10.75 9.32 2.98 0.05 input
abelian_groups_homomorphism 75.63 82.67 16.26 0.05 input
arithmetic ⊥ 25.46 15.53 ?  
assoc_comm_ring_unit3 ⊥ 65.04 47.34 0.1 input
assoc_ring_unit3 ⊥ 247.72 158.03 0.1 input
binary_arithmetic (1)1 ⊥ 10.67 2.10 ?  
binary_arithmetic (2) ⊥ 78.20 23.05 ?  
comm_monoid 0.50 0.71 0.03 0.01 input
Example 5.4.22 4.9 5.91 0.42 0.01 input
ICS4 6.9 7.23 5.96 0.01 input
max2 ⊥ 8.31 0.29 ?  
module ∞ ∞ ∞ x input
multisets_binary ∞ 120.96 9.33 ?  
nondeterministic machine4 ∞ ∞ ∞ 0.2 input
ring3 ⊥ 228.01 113.26 0.07 input
ring_unit3 ⊥ 201.45 80.81 0.1 input
semiring ⊥ 25.51 12.77 0.1 input
semilattice 5.4 6.51 5.06 0.01 input
strange addition ⊥ ∞ 0.72 ?  
sum ⊥ 7.66 0.32 ?  

Explanation of Symbols
∞ timeout (300 seconds)
? no appropriate reduction order known that could be used by CiME
x error
⊥ 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

Mascott Commands
internal mascott -t 300 -T 10 -ct -st -it 'dp; matrix -dim 2 -ib 2 -direct'
AProVe mascott -t 300 -T 10 -ct -st -tp callaprove
muterm mascott -t 300 -T 3 -ct -st -tp callmuterm