YES (ignored inputs)COMMENT the following rules are removed from the original TRS g ( x ) -> h ( a ( ) ) h ( x ) -> e ( ) Rewrite Rules: [ a -> c, c -> a, d -> a, b -> d, a -> b, a -> e, d -> e ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ c = b, c = e, a = e, b = e ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth & Bendix Linear unknown Development Closed unknown Strongly Closed unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Simultaneous CPs: [ b = c, e = c, e = a, c = b, e = b, c = e, b = e, a = e ] unknown Okui (Simultaneous CPs) unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping check Locally Decreasing Diagrams by Rule Labelling... Critical Pair by Rules <4, 0> preceded by [] joinable by a reduction of rules <[([],3),([],2)], [([],1)]> joinable by a reduction of rules <[], [([],1),([],4)]> joinable by a reduction of rules <[([],3),([],6)], [([],1),([],5)]> Critical Pair by Rules <5, 0> preceded by [] joinable by a reduction of rules <[], [([],1),([],5)]> Critical Pair by Rules <6, 2> preceded by [] joinable by a reduction of rules <[], [([],5)]> Critical Pair by Rules <5, 4> preceded by [] joinable by a reduction of rules <[], [([],3),([],6)]> Satisfiable by 5>4,1>3>7,6>2; ; 4,1>5>3>6,7>2 Diagram Decreasing Direct Methods: CR Combined result: CR /tmp/fileAcn0HY.trs: Success(CR) (15 msec.)