(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 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: [ f(g(a)) = g(b), g(b) = f(g(a)) ] unknown Okui (Simultaneous CPs) unknown Strongly Depth-Preserving & 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 /local-scratch/hzankl/2012/cops2012/22.trs: Success(CR) (2 msec.)