The following experiments were conducted on a Intel Core Duo @ 1.4 GHz.
| ∞ | timeout (300 seconds) |
| ? | no appropriate reduction order known that could be used by CiME |
| - | theory not applicable for problem |
| ⊥ | failure of completion |
| 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. | |