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