YES

---- CR(R)
---- [Knuth and Bendix, 1970]
R:
+(0(),y) -> y
+(s(x),y) -> s(+(x,y))
s(s(x)) -> x
CP(R):
+(___y20,___y22) -> s(+(s(___y20),___y22))
s(___y23) -> s(___y23)