YES (ignored inputs)COMMENT Example 3.2 of \cite{KS10} doi: http://dx.doi.org/10.1007/978-3-642-12251-4_20 Rewrite Rules: [ a -> b, a -> c, a -> e, b -> d, c -> a, d -> a, d -> e, g(?x) -> h(a), h(?x) -> e ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ b = c, b = e, c = e, a = 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: [ c = b, e = b, b = c, e = c, b = e, c = e, e = a, 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 <1, 0> preceded by [] joinable by a reduction of rules <[([],4),([],0)], []> joinable by a reduction of rules <[([],4)], [([],3),([],5)]> joinable by a reduction of rules <[([],4),([],2)], [([],3),([],6)]> Critical Pair by Rules <2, 0> preceded by [] joinable by a reduction of rules <[], [([],3),([],6)]> Critical Pair by Rules <2, 1> preceded by [] joinable by a reduction of rules <[], [([],4),([],2)]> Critical Pair by Rules <6, 5> preceded by [] joinable by a reduction of rules <[], [([],2)]> Satisfiable by 1>6>2,3,5,7>4,8,9; g(0)h(0); 2>1>6>3,5,7>4,8,9 Diagram Decreasing Direct Methods: CR Final result: CR 111.trs: Success(CR) (10 msec.)