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