(ignored inputs)COMMENT Exercise 6.5{a} of \cite{BN98} Rewrite Rules: [ f(g(f(?x))) -> ?x, f(g(?x)) -> g(f(?x)) ] Apply Direct Methods... Inner CPs: [ f(g(g(f(?x_1)))) = g(?x_1), f(g(?x)) = g(f(?x)) ] Outer CPs: [ ?x = g(f(f(?x))) ] not Overlay, check Termination... Terminating, not WCR Knuth&Bendix Direct Methods: not CR Final result: not CR /local-scratch/hzankl/2012/cops2012/10.trs: Success(not CR) (4 msec.)