YES (ignored inputs)COMMENT doi:10.1007/978-3-642-12251-4_20 [32] Example 3.2 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>5,7,2,3>8,9,4; g(0)h(0); 2>1>6>5,7,3>8,9,4 Diagram Decreasing Direct Methods: CR Combined result: CR 111.trs: Success(CR) (14 msec.)