YES

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