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