YES

---- CR(R)
---- [Knuth and Bendix, 1970]
R:
f(f(x,y),z) -> f(x,f(y,z))
f(1(),x) -> x
CP(R):
f(f(___y1,f(___y2,___y3)),___y6) -> f(f(___y1,___y2),f(___y3,___y6))
f(___y11,___y14) -> f(1(),f(___y11,___y14))