NO (ignored inputs)COMMENT reduction failed 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 Combined result: not CR /tmp/filemdkM8F.trs: Success(not CR) (0 msec.)