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