YES (ignored inputs)COMMENT Example 5 of \cite{GL06} Rewrite Rules: [ g(a) -> f(g(a)), g(b) -> c(a), a -> b, f(?x) -> h(?x), h(?x) -> c(b) ] Apply Direct Methods... Inner CPs: [ g(b) = f(g(a)) ] Outer CPs: [ ] not Overlay, check Termination... unknown/not Terminating unknown Knuth & Bendix Linear unknown Development Closed unknown Strongly Closed unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow inner CP cond (upside-parallel) innter CP Cond (outside) unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Simultaneous CPs: [ g(b) = f(g(a)), f(g(a)) = g(b) ] 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 <2, 0> preceded by [(g,1)] joinable by a reduction of rules <[([],1),([(c,1)],2)], [([],3),([],4)]> Satisfiable by 1,3,5>2,4; c(0)f(0)g(0)h(0); 1,3,5>2,4 Diagram Decreasing Direct Methods: CR Final result: CR 22.trs: Success(CR) (6 msec.)