YES

---- CR(R)
---- [Knuth and Bendix, 1970]
R:
a(a(x)) -> a(b(a(x)))
b(a(b(x))) -> a(c(a(x)))
CP(R):
a(a(b(a(___y1)))) -> a(b(a(a(___y1))))
b(a(a(c(a(___y7))))) -> a(c(a(a(b(___y7)))))