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