YES

---- CR(R)
---- [Jouannaud and Kirchner, 1986]
R:
+(x,0()) -> x
+(x,s(y)) -> s(+(x,y))
*(x,0()) -> 0()
*(x,s(y)) -> +(*(x,y),x)
+(+(x,y),z) -> +(x,+(y,z))
+(x,y) -> +(y,x)
*(*(x,y),z) -> *(x,*(y,z))
*(x,y) -> *(y,x)
*(x,+(y,z)) -> +(*(x,y),*(x,z))
CP_AC(R):
+(x,s(y)) -> s(+(x,0(),y))
s(x) -> s(+(0(),x))
*(x,+(y,z)) -> +(*(x,+(y,0())),*(x,z))
*(x,y) -> +(*(x,0()),*(x,y))
*(x,+(y,z)) -> +(*(x,y),*(x,+(z,0())))
*(x,y) -> +(*(x,y),*(x,0()))
s(+(x,0(),y)) -> +(x,s(y))
s(+(0(),x)) -> s(x)
*(x,s(+(y,z,w))) -> +(*(x,+(y,s(w))),*(x,z))
*(x,s(+(y,z))) -> +(*(x,s(z)),*(x,y))
*(x,s(+(y,z,w))) -> +(*(x,y),*(x,+(z,s(w))))
*(x,s(+(y,z))) -> +(*(x,y),*(x,s(z)))
0() -> +(*(x,0(),y),*(x,0()))
0() -> +(*(0(),x),0())
0() -> +(*(x,0(),y),*(x,0(),z))
0() -> +(*(0(),x),*(0(),y))
+(*(x,0(),y),*(x,0())) -> 0()
+(*(0(),x),0()) -> 0()
+(*(x,+(y,z),w),*(x,+(y,z))) -> +(*(x,s(w),y),*(x,s(w),z))
+(*(+(x,y),z),x,y) -> +(*(s(z),x),*(s(z),y))
+(*(x,0(),y),*(x,0(),z)) -> 0()
+(*(0(),x),*(0(),y)) -> 0()
+(*(x,s(y),z),*(x,s(y),w)) -> +(*(x,+(z,w),y),*(x,+(z,w)))
+(*(s(x),y),*(s(x),z)) -> +(*(+(y,z),x),y,z)
+(x,y) -> +(y,x,0())
x -> +(x,0())
+(x,y) -> +(y,0(),x)
x -> +(0(),x)
+(x,y,z) -> +(x,0(),y,z)
+(x,y) -> +(0(),x,y)
+(x,y,z) -> +(x,y,0(),z)
+(x,y) -> +(x,0(),y)
+(x,y,z) -> +(x,y,z,0())
+(x,y) -> +(x,y,0())
+(x,y,z) -> +(x,0(),y,z)
+(x,y) -> +(0(),x,y)
+(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) -> +(x,y,0(),z)
+(x,y) -> +(x,0(),y)
+(x,y,z) -> +(x,y,z,0())
+(x,y) -> +(x,y,0())
+(x,y,z) -> +(x,y,0(),z)
+(x,y) -> +(x,0(),y)
+(x,y,z) -> +(x,y,z,0())
+(x,y) -> +(x,y,0())
s(+(x,y,z)) -> +(y,x,s(z))
s(+(x,y)) -> +(x,s(y))
s(+(x,y,z)) -> +(y,s(z),x)
s(+(x,y)) -> +(s(y),x)
s(+(x,y,z,w)) -> +(x,s(w),y,z)
s(+(x,y,z)) -> +(s(z),x,y)
s(+(x,y,z,w)) -> +(x,y,s(w),z)
s(+(x,y,z)) -> +(x,s(z),y)
s(+(x,y,z,w)) -> +(x,y,z,s(w))
s(+(x,y,z)) -> +(x,y,s(z))
+(s(+(x,y,z)),w) -> +(x,s(z),y,w)
+(s(+(x,y)),z) -> +(s(y),x,z)
+(s(+(x,y,z)),w) -> +(x,y,s(z),w)
+(s(+(x,y)),z) -> +(x,s(y),z)
s(+(x,y,z,w)) -> +(x,s(w),y,z)
s(+(x,y,z)) -> +(s(z),x,y)
s(+(x,y,z,w)) -> +(x,y,s(w),z)
s(+(x,y,z)) -> +(x,s(z),y)
s(+(x,y,z,w)) -> +(x,y,z,s(w))
s(+(x,y,z)) -> +(x,y,s(z))
+(x,s(+(y,z,w))) -> +(x,y,s(w),z)
+(x,s(+(y,z))) -> +(x,s(z),y)
+(x,s(+(y,z,w))) -> +(x,y,z,s(w))
+(x,s(+(y,z))) -> +(x,y,s(z))
0() -> *(x,y,0())
0() -> *(x,0())
0() -> *(x,0(),y)
0() -> *(0(),x)
0() -> *(x,0(),y,z)
0() -> *(0(),x,y)
0() -> *(x,y,0(),z)
0() -> *(x,0(),y)
0() -> *(x,y,z,0())
0() -> *(x,y,0())
*(0(),x) -> *(y,0(),z,x)
*(0(),x) -> *(0(),y,x)
*(0(),x) -> *(y,z,0(),x)
*(0(),x) -> *(y,0(),x)
0() -> *(x,0(),y,z)
0() -> *(0(),x,y)
0() -> *(x,y,0(),z)
0() -> *(x,0(),y)
0() -> *(x,y,z,0())
0() -> *(x,y,0())
*(x,0()) -> *(x,y,0(),z)
*(x,0()) -> *(x,0(),y)
*(x,0()) -> *(x,y,z,0())
*(x,0()) -> *(x,y,0())
+(*(x,y,z),*(x,y)) -> *(y,x,s(z))
+(*(x,y),x) -> *(x,s(y))
+(*(x,y,z),*(x,y)) -> *(y,s(z),x)
+(*(x,y),x) -> *(s(y),x)
+(*(x,y,z,w),*(x,y,z)) -> *(x,s(w),y,z)
+(*(x,y,z),*(x,y)) -> *(s(z),x,y)
+(*(x,y,z,w),*(x,y,z)) -> *(x,y,s(w),z)
+(*(x,y,z),*(x,y)) -> *(x,s(z),y)
+(*(x,y,z,w),*(x,y,z)) -> *(x,y,z,s(w))
+(*(x,y,z),*(x,y)) -> *(x,y,s(z))
*(+(*(x,y,z),*(x,y)),w) -> *(x,s(z),y,w)
*(+(*(x,y),x),z) -> *(s(y),x,z)
*(+(*(x,y,z),*(x,y)),w) -> *(x,y,s(z),w)
*(+(*(x,y),x),z) -> *(x,s(y),z)
+(*(x,y,z,w),*(x,y,z)) -> *(x,s(w),y,z)
+(*(x,y,z),*(x,y)) -> *(s(z),x,y)
+(*(x,y,z,w),*(x,y,z)) -> *(x,y,s(w),z)
+(*(x,y,z),*(x,y)) -> *(x,s(z),y)
+(*(x,y,z,w),*(x,y,z)) -> *(x,y,z,s(w))
+(*(x,y,z),*(x,y)) -> *(x,y,s(z))
*(x,+(*(y,z,w),*(y,z))) -> *(x,y,s(w),z)
*(x,+(*(y,z),y)) -> *(x,s(z),y)
*(x,+(*(y,z,w),*(y,z))) -> *(x,y,z,s(w))
*(x,+(*(y,z),y)) -> *(x,y,s(z))
+(*(x,y,z),*(x,y,w)) -> *(y,x,+(z,w))
+(*(x,y),*(x,z)) -> *(x,+(y,z))
+(*(x,y,z),*(x,y,w)) -> *(y,+(z,w),x)
+(*(x,y),*(x,z)) -> *(+(y,z),x)
+(*(x,y,z,w),*(x,y,z,x1)) -> *(x,+(w,x1),y,z)
+(*(x,y,z),*(x,y,w)) -> *(+(z,w),x,y)
+(*(x,y,z,w),*(x,y,z,x1)) -> *(x,y,+(w,x1),z)
+(*(x,y,z),*(x,y,w)) -> *(x,+(z,w),y)
+(*(x,y,z,w),*(x,y,z,x1)) -> *(x,y,z,+(w,x1))
+(*(x,y,z),*(x,y,w)) -> *(x,y,+(z,w))
*(+(*(x,y,z),*(x,y,w)),x1) -> *(x,+(z,w),y,x1)
*(+(*(x,y),*(x,z)),w) -> *(+(y,z),x,w)
*(+(*(x,y,z),*(x,y,w)),x1) -> *(x,y,+(z,w),x1)
*(+(*(x,y),*(x,z)),w) -> *(x,+(y,z),w)
+(*(x,y,z,w),*(x,y,z,x1)) -> *(x,+(w,x1),y,z)
+(*(x,y,z),*(x,y,w)) -> *(+(z,w),x,y)
+(*(x,y,z,w),*(x,y,z,x1)) -> *(x,y,+(w,x1),z)
+(*(x,y,z),*(x,y,w)) -> *(x,+(z,w),y)
+(*(x,y,z,w),*(x,y,z,x1)) -> *(x,y,z,+(w,x1))
+(*(x,y,z),*(x,y,w)) -> *(x,y,+(z,w))
*(x,+(*(y,z,w),*(y,z,x1))) -> *(x,y,+(w,x1),z)
*(x,+(*(y,z),*(y,w))) -> *(x,+(z,w),y)
*(x,+(*(y,z,w),*(y,z,x1))) -> *(x,y,z,+(w,x1))
*(x,+(*(y,z),*(y,w))) -> *(x,y,+(z,w))