(ignored inputs)COMMENT R_2 in p.14 of \cite{Oku98} Rewrite Rules: [ a -> c, b -> c, f(a,b) -> d, f(?x,c) -> f(c,c), f(c,?x) -> f(c,c), d -> f(a,c), d -> f(c,b) ] Apply Direct Methods... Inner CPs: [ f(c,b) = d, f(a,c) = d ] Outer CPs: [ f(c,c) = f(c,c), f(a,c) = f(c,b) ] not Overlay, check Termination... unknown/not Terminating unknown Knuth&Bendix Linear unknown Development Closed Strongly Closed Direct Methods: CR Final result: CR /local-scratch/hzankl/2012/cops2012/74.trs: Success(CR) (1 msec.)