YES ---- CR(R) ---- R : left-linear, C : CR and CP-closing, and Cdup/R : SN R: f(f(x,y),z) -> f(x,f(y,z)) f(x,y) -> f(y,x) CP(R): f(f(___y1,f(___y2,___y3)),___y6) -> f(f(___y1,___y2),f(___y3,___y6)) f(___y7,f(___y8,___y9)) -> f(___y9,f(___y7,___y8)) f(___y13,f(___y14,___y15)) -> f(___y14,f(___y15,___y13)) f(f(___y13,___y12),___y16) -> f(___y12,f(___y13,___y16)) critical-pair-closing system C: f(f(x,y),z) -> f(x,f(y,z)) f(x,y) -> f(y,x) CR(C): see below. ---- CR(R) ---- R : linear and strongly closed [Huet, 1980] R: f(f(x,y),z) -> f(x,f(y,z)) f(x,y) -> f(y,x) CP(R): f(f(___y21,f(___y22,___y23)),___y26) -> f(f(___y21,___y22),f(___y23,___y26)) f(___y27,f(___y28,___y29)) -> f(___y29,f(___y27,___y28)) f(___y33,f(___y34,___y35)) -> f(___y34,f(___y35,___y33)) f(f(___y33,___y32),___y36) -> f(___y32,f(___y33,___y36))