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