(VAR x y z u v w)
(THEORY (AC p))
(RULES
p(x,0) -> x
p(minus(x),x) -> 0
m(I,x) -> x
m(i(x),x) -> I
m(x,m(y,z)) -> m(m(x,y),z)
m(i(x),m(x,y)) -> y
m(x,I) -> x
i(I) -> I
i(i(x)) -> x
m(x,i(x)) -> I
m(x,m(i(x),y)) -> y
i(m(x,y)) -> m(i(y),i(x))
m(Tr(x,y,z),Tr(u,v,w)) -> Tr(p(x,u),p(y,v),p(z,w))
m(T(x),T(y)) -> T(p(x,y))
m(M,M) -> I
m(T(z),Tr(x,0,0)) -> m(Tr(x,0,0),T(z))
m(T(z),M) -> m(M,T(minus(z)))
m(Tr(x,y,z),M) -> m(M,Tr(minus(x),minus(y),z))
)