(ignored inputs)COMMENT Example 2 of \cite{Gra96caap} Rewrite Rules: [ f(a,a) -> b, a -> a', f(a',?x) -> f(?x,?x), f(?x,a') -> f(?x,?x), f(a',a') -> b, b -> f(a',a') ] Apply Direct Methods... Inner CPs: [ f(a',a) = b, f(a,a') = b ] Outer CPs: [ f(a',a') = f(a',a'), f(a',a') = b, f(a',a') = b ] not Overlay, check Termination... unknown/not Terminating unknown Knuth&Bendix Left-Linear, not Right-Linear unknown Development Closed inner CP cond (upside-parallel) innter CP Cond (outside) unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: [ f(a,a') = b {}, f(a',a) = b {}, f(a',a') = b {} ] Toyama (Parallel CPs) Direct Methods: CR Final result: CR /local-scratch/hzankl/2012/cops2012/30.trs: Success(CR) (20 msec.)