YES (ignored inputs)COMMENT doi:10.1007/3-540-61064-2_39 [10] Example 2 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama 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 ] Left-Linear, not Right-Linear (inner) Parallel CPs: [ f(a,a') = b {}, f(a',a) = b {}, f(a',a') = b {} ] Toyama (Parallel CPs) Direct Methods: CR Combined result: CR 30.trs: Success(CR) (0 msec.)