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