YES

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