---- 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))
*(1(),x) -> x
*(x,+(y,z)) -> +(*(x,y),*(x,z))
*(*(x,y),z) -> *(x,*(y,z))
*(x,y) -> *(y,x)
*(x,0()) -> 0()
*(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))
*(x,y) -> +(*(x,y),*(x,0()))
*(x,+(y,z)) -> +(*(x,y),*(x,+(0(),z)))
*(x,y) -> +(*(x,0()),*(x,y))
*(x,+(y,z)) -> +(*(x,+(0(),y)),*(x,z))
0() -> -(0())
0() -> +(-(+(0(),x)),x)
-(0()) -> +(-(x),-(-(x)))
-(0()) -> +(-(x),-(+(-(+(x,y)),y)))
-(0()) -> +(-(-(x)),-(x))
-(0()) -> +(-(+(-(+(x,y)),x)),-(y))
*(x,0()) -> +(*(x,y),*(x,-(y)))
*(x,0()) -> +(*(x,y),*(x,+(-(+(y,z)),z)))
*(x,0()) -> +(*(x,-(y)),*(x,y))
*(x,0()) -> +(*(x,+(-(+(y,z)),y)),*(x,z))
+(0(),0()) -> 0()
-(0()) -> 0()
*(x,0()) -> -(*(x,0()))
+(x,-(x)) -> 0()
-(x) -> -(x)
*(x,y) -> -(*(x,-(y)))
+(-(x),-(y),x,y) -> 0()
-(+(-(x),-(y))) -> +(x,y)
*(x,+(-(y),-(z))) -> -(*(x,+(y,z)))
+(x,y) -> +(*(1(),x),*(1(),y))
*(x,+(y,z)) -> +(*(1(),x,y),*(1(),x,z))
0() -> 0()
*(x,0()) -> 0()
-(x) -> -(*(1(),x))
*(x,-(y)) -> -(*(1(),x,y))
+(*(1(),x,y),*(1(),x,z)) -> *(x,+(y,z))
+(*(1(),x),*(1(),y)) -> +(x,y)
+(*(x,0(),y),*(x,0(),z)) -> 0()
+(*(0(),x),*(0(),y)) -> 0()
+(*(x,-(y),z),*(x,-(y),w)) -> -(*(x,+(z,w),y))
+(*(-(x),y),*(-(x),z)) -> -(*(+(y,z),x))
0() -> *(x,0())
0() -> 0()
0() -> +(*(x,0(),y),*(x,0(),z))
0() -> +(*(0(),x),*(0(),y))
0() -> -(*(x,0(),y))
0() -> -(*(0(),x))
-(*(1(),x,y)) -> *(x,-(y))
-(*(1(),x)) -> -(x)
-(*(x,+(y,z),w)) -> +(*(x,-(w),y),*(x,-(w),z))
-(*(+(x,y),z)) -> +(*(-(z),x),*(-(z),y))
-(*(x,0(),y)) -> 0()
-(*(0(),x)) -> 0()
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)
x -> *(1(),x)
*(x,y) -> *(1(),y,x)
x -> *(x,1())
*(x,y) -> *(y,1(),x)
*(x,y) -> *(x,y,1())
*(x,y,z) -> *(x,y,1(),z)
*(x,y) -> *(x,1(),y)
*(x,y,z) -> *(x,1(),y,z)
*(x,y) -> *(1(),x,y)
*(x,y,z) -> *(1(),x,y,z)
*(x,y) -> *(x,1(),y)
*(x,y,z) -> *(x,1(),y,z)
*(x,y) -> *(1(),x,y)
*(x,y,z) -> *(1(),x,y,z)
*(x,y) -> *(x,y,1())
*(x,y,z) -> *(x,y,1(),z)
*(x,y) -> *(x,1(),y)
*(x,y,z) -> *(x,1(),y,z)
*(x,y) -> *(1(),x,y)
*(x,y,z) -> *(1(),x,y,z)
*(x,y) -> *(x,y,1())
*(x,y,z) -> *(x,y,1(),z)
*(x,y) -> *(x,1(),y)
*(x,y,z) -> *(x,1(),y,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))
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)) -> *(y,x,-(z))
-(*(x,y)) -> *(x,-(y))
-(*(x,y,z)) -> *(y,-(z),x)
-(*(x,y)) -> *(-(y),x)
-(*(x,y,z,w)) -> *(x,-(w),y,z)
-(*(x,y,z)) -> *(-(z),x,y)
-(*(x,y,z,w)) -> *(x,y,-(w),z)
-(*(x,y,z)) -> *(x,-(z),y)
-(*(x,y,z,w)) -> *(x,y,z,-(w))
-(*(x,y,z)) -> *(x,y,-(z))
*(-(*(x,y,z)),w) -> *(x,-(z),y,w)
*(-(*(x,y)),z) -> *(-(y),x,z)
*(-(*(x,y,z)),w) -> *(x,y,-(z),w)
*(-(*(x,y)),z) -> *(x,-(y),z)
-(*(x,y,z,w)) -> *(x,-(w),y,z)
-(*(x,y,z)) -> *(-(z),x,y)
-(*(x,y,z,w)) -> *(x,y,-(w),z)
-(*(x,y,z)) -> *(x,-(z),y)
-(*(x,y,z,w)) -> *(x,y,z,-(w))
-(*(x,y,z)) -> *(x,y,-(z))
*(x,-(*(y,z,w))) -> *(x,y,-(w),z)
*(x,-(*(y,z))) -> *(x,-(z),y)
*(x,-(*(y,z,w))) -> *(x,y,z,-(w))
*(x,-(*(y,z))) -> *(x,y,-(z))