NO (ignored inputs)COMMENT reduction failed Rewrite Rules: [ f(h(a,c)) -> h(f(b),h(c,h(c,h(f(h(b,b)),a)))), h(h(h(f(b),c),b),h(a,h(a,c))) -> h(f(b),h(c,b)), a -> h(h(b,b),b), c -> a ] Apply Direct Methods... Inner CPs: [ f(h(h(h(b,b),b),c)) = h(f(b),h(c,h(c,h(f(h(b,b)),a)))), f(h(a,a)) = h(f(b),h(c,h(c,h(f(h(b,b)),a)))), h(h(h(f(b),c),b),h(h(h(b,b),b),h(a,c))) = h(f(b),h(c,b)), h(h(h(f(b),c),b),h(a,h(h(h(b,b),b),c))) = h(f(b),h(c,b)), h(h(h(f(b),a),b),h(a,h(a,c))) = h(f(b),h(c,b)), h(h(h(f(b),c),b),h(a,h(a,a))) = h(f(b),h(c,b)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Combined result: not CR /tmp/fileWynYLX.trs: Success(not CR) (54 msec.)