(ignored inputs)COMMENT Example 3.4.23 of \cite{Gra96thesis} Rewrite Rules: [ f(a) -> b, f(a) -> f(c), a -> d, f(d) -> b, f(c) -> b, d -> c ] Apply Direct Methods... Inner CPs: [ f(d) = b, f(d) = f(c), f(c) = b ] Outer CPs: [ b = f(c) ] not Overlay, check Termination... Terminating, WCR Knuth&Bendix Direct Methods: CR Final result: CR /local-scratch/hzankl/2012/cops2012/40.trs: Success(CR) (0 msec.)