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