YES (ignored inputs)COMMENT reduction failed Rewrite Rules: [ f(?x) -> ?x, f(?x) -> f(f(?x)) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ?x = f(f(?x)) ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth & Bendix Linear Development Closed Direct Methods: CR Combined result: CR /tmp/fileODe4Yv.trs: Success(CR) (0 msec.)