YES (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 unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow 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 30.trs: Success(CR) (17 msec.)