(ignored inputs)COMMENT Example 9 of \cite{Gra96caap} Rewrite Rules: [ f(a) -> f(f(a)), a -> b, f(?x) -> f(b) ] Apply Direct Methods... Inner CPs: [ f(b) = f(f(a)) ] Outer CPs: [ f(f(a)) = f(b) ] not Overlay, check Termination... unknown/not Terminating unknown Knuth&Bendix Linear unknown Development Closed Strongly Closed Direct Methods: CR Final result: CR /local-scratch/hzankl/2012/cops2012/36.trs: Success(CR) (0 msec.)