YES

---- CR(R)
---- [Jouannaud and Kirchner, 1986]
R:
+(0(),y) -> y
+(s(x),y) -> s(+(x,y))
+(+(x,y),z) -> +(x,+(y,z))
+(x,y) -> +(y,x)
CP_AC(R):
s(x) -> s(+(x,0()))
+(s(x),y) -> s(+(x,0(),y))
s(+(x,0())) -> s(x)
s(+(x,0(),y)) -> +(s(x),y)
x -> +(0(),x)
+(x,y) -> +(0(),y,x)
x -> +(x,0())
+(x,y) -> +(y,0(),x)
+(x,y) -> +(x,y,0())
+(x,y,z) -> +(x,y,0(),z)
+(x,y) -> +(x,0(),y)
+(x,y,z) -> +(x,0(),y,z)
+(x,y) -> +(0(),x,y)
+(x,y,z) -> +(0(),x,y,z)
+(x,y) -> +(x,0(),y)
+(x,y,z) -> +(x,0(),y,z)
+(x,y) -> +(0(),x,y)
+(x,y,z) -> +(0(),x,y,z)
+(x,y) -> +(x,y,0())
+(x,y,z) -> +(x,y,0(),z)
+(x,y) -> +(x,0(),y)
+(x,y,z) -> +(x,0(),y,z)
+(x,y) -> +(0(),x,y)
+(x,y,z) -> +(0(),x,y,z)
+(x,y) -> +(x,y,0())
+(x,y,z) -> +(x,y,0(),z)
+(x,y) -> +(x,0(),y)
+(x,y,z) -> +(x,0(),y,z)
s(+(x,y)) -> +(s(x),y)
s(+(x,y,z)) -> +(s(x),z,y)
s(+(x,y)) -> +(y,s(x))
s(+(x,y,z)) -> +(z,s(x),y)
s(+(x,y,z)) -> +(y,z,s(x))
s(+(x,y,z,w)) -> +(y,z,s(x),w)
s(+(x,y,z)) -> +(y,s(x),z)
s(+(x,y,z,w)) -> +(y,s(x),z,w)
s(+(x,y,z)) -> +(s(x),y,z)
s(+(x,y,z,w)) -> +(s(x),y,z,w)
+(s(+(x,y)),z) -> +(y,s(x),z)
+(s(+(x,y,z)),w) -> +(y,s(x),z,w)
+(s(+(x,y)),z) -> +(s(x),y,z)
+(s(+(x,y,z)),w) -> +(s(x),y,z,w)
s(+(x,y,z)) -> +(y,z,s(x))
s(+(x,y,z,w)) -> +(y,z,s(x),w)
s(+(x,y,z)) -> +(y,s(x),z)
s(+(x,y,z,w)) -> +(y,s(x),z,w)
s(+(x,y,z)) -> +(s(x),y,z)
s(+(x,y,z,w)) -> +(s(x),y,z,w)
+(x,s(+(y,z))) -> +(x,z,s(y))
+(x,s(+(y,z,w))) -> +(x,z,s(y),w)
+(x,s(+(y,z))) -> +(x,s(y),z)
+(x,s(+(y,z,w))) -> +(x,s(y),z,w)