(ignored inputs)COMMENT Exercise 6.18 of \cite{BN98} Rewrite Rules: [ f(g(?x,a,b)) -> ?x, p(a) -> c, g(f(h(c,d)),?x,?y) -> h(p(?x),q(?x)), q(b) -> d ] Apply Direct Methods... Inner CPs: [ f(h(p(a),q(a))) = f(h(c,d)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth&Bendix Direct Methods: not CR Final result: not CR /local-scratch/hzankl/2012/cops2012/5.trs: Success(not CR) (1 msec.)