(ignored inputs)COMMENT R_3 in p.14 of \cite{Oku98} 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 Final result: CR /local-scratch/hzankl/2012/cops2012/75.trs: Success(CR) (1 msec.)