YES
Time: 0.170

Problem:
 Equations:
  pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
  pAC(x6,x7) -> pAC(x7,x6)
  pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
  pAC(x7,x6) -> pAC(x6,x7)
 TRS:
  pAC(x,0()) -> x
  pAC(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(pAC(x,u),pAC(y,v),pAC(z,w))
  m(T(x),T(y)) -> T(pAC(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))

Proof:
 DP Processor:
  Equations#:
   p{AC,#}(pAC(x6,x7),x8) -> p{AC,#}(x6,pAC(x7,x8))
   p{AC,#}(x6,x7) -> p{AC,#}(x7,x6)
   p{AC,#}(x6,pAC(x7,x8)) -> p{AC,#}(pAC(x6,x7),x8)
   p{AC,#}(x7,x6) -> p{AC,#}(x6,x7)
  DPs:
   m#(x,m(y,z)) -> m#(x,y)
   m#(x,m(y,z)) -> m#(m(x,y),z)
   i#(m(x,y)) -> i#(x)
   i#(m(x,y)) -> i#(y)
   i#(m(x,y)) -> m#(i(y),i(x))
   m#(Tr(x,y,z),Tr(u,v,w)) -> p{AC,#}(z,w)
   m#(Tr(x,y,z),Tr(u,v,w)) -> p{AC,#}(y,v)
   m#(Tr(x,y,z),Tr(u,v,w)) -> p{AC,#}(x,u)
   m#(T(x),T(y)) -> p{AC,#}(x,y)
   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))
   p{AC,#}(x9,pAC(x,0())) -> p{AC,#}(x9,x)
   p{AC,#}(x10,pAC(minus(x),x)) -> p{AC,#}(x10,0())
  Equations:
   pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
   pAC(x6,x7) -> pAC(x7,x6)
   pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
   pAC(x7,x6) -> pAC(x6,x7)
  TRS:
   pAC(x,0()) -> x
   pAC(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(pAC(x,u),pAC(y,v),pAC(z,w))
   m(T(x),T(y)) -> T(pAC(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))
  S:
   p{AC,#}(pAC(x11,x12),x13) -> p{AC,#}(x11,x12)
   p{AC,#}(x11,pAC(x12,x13)) -> p{AC,#}(x12,x13)
  AC-EDG Processor:
   Equations#:
    p{AC,#}(pAC(x6,x7),x8) -> p{AC,#}(x6,pAC(x7,x8))
    p{AC,#}(x6,x7) -> p{AC,#}(x7,x6)
    p{AC,#}(x6,pAC(x7,x8)) -> p{AC,#}(pAC(x6,x7),x8)
    p{AC,#}(x7,x6) -> p{AC,#}(x6,x7)
   DPs:
    m#(x,m(y,z)) -> m#(x,y)
    m#(x,m(y,z)) -> m#(m(x,y),z)
    i#(m(x,y)) -> i#(x)
    i#(m(x,y)) -> i#(y)
    i#(m(x,y)) -> m#(i(y),i(x))
    m#(Tr(x,y,z),Tr(u,v,w)) -> p{AC,#}(z,w)
    m#(Tr(x,y,z),Tr(u,v,w)) -> p{AC,#}(y,v)
    m#(Tr(x,y,z),Tr(u,v,w)) -> p{AC,#}(x,u)
    m#(T(x),T(y)) -> p{AC,#}(x,y)
    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))
    p{AC,#}(x9,pAC(x,0())) -> p{AC,#}(x9,x)
    p{AC,#}(x10,pAC(minus(x),x)) -> p{AC,#}(x10,0())
   Equations:
    pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
    pAC(x6,x7) -> pAC(x7,x6)
    pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
    pAC(x7,x6) -> pAC(x6,x7)
   TRS:
    pAC(x,0()) -> x
    pAC(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(pAC(x,u),pAC(y,v),pAC(z,w))
    m(T(x),T(y)) -> T(pAC(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))
   S:
    p{AC,#}(pAC(x11,x12),x13) -> p{AC,#}(x11,x12)
    p{AC,#}(x11,pAC(x12,x13)) -> p{AC,#}(x12,x13)
   SCC Processor:
    #sccs: 3
    #rules: 6
    #arcs: 45/196
    Equations#:
     p{AC,#}(pAC(x6,x7),x8) -> p{AC,#}(x6,pAC(x7,x8))
     p{AC,#}(x6,x7) -> p{AC,#}(x7,x6)
     p{AC,#}(x6,pAC(x7,x8)) -> p{AC,#}(pAC(x6,x7),x8)
     p{AC,#}(x7,x6) -> p{AC,#}(x6,x7)
    DPs:
     i#(m(x,y)) -> i#(y)
     i#(m(x,y)) -> i#(x)
    Equations:
     pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
     pAC(x6,x7) -> pAC(x7,x6)
     pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
     pAC(x7,x6) -> pAC(x6,x7)
    TRS:
     pAC(x,0()) -> x
     pAC(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(pAC(x,u),pAC(y,v),pAC(z,w))
     m(T(x),T(y)) -> T(pAC(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))
    S:
     p{AC,#}(pAC(x11,x12),x13) -> p{AC,#}(x11,x12)
     p{AC,#}(x11,pAC(x12,x13)) -> p{AC,#}(x12,x13)
    AC-DP unlabeling:
     Equations#:
      pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
      pAC(x6,x7) -> pAC(x7,x6)
      pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
      pAC(x7,x6) -> pAC(x6,x7)
     DPs:
      i#(m(x,y)) -> i#(y)
      i#(m(x,y)) -> i#(x)
     Equations:
      pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
      pAC(x6,x7) -> pAC(x7,x6)
      pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
      pAC(x7,x6) -> pAC(x6,x7)
     TRS:
      pAC(x,0()) -> x
      pAC(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(pAC(x,u),pAC(y,v),pAC(z,w))
      m(T(x),T(y)) -> T(pAC(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))
     S:
      pAC(pAC(x11,x12),x13) -> pAC(x11,x12)
      pAC(x11,pAC(x12,x13)) -> pAC(x12,x13)
     Usable Rule Processor:
      Equations#:
       pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
       pAC(x6,x7) -> pAC(x7,x6)
       pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
       pAC(x7,x6) -> pAC(x6,x7)
      DPs:
       i#(m(x,y)) -> i#(y)
       i#(m(x,y)) -> i#(x)
      Equations:
       pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
       pAC(x6,x7) -> pAC(x7,x6)
       pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
       pAC(x7,x6) -> pAC(x6,x7)
      TRS:
       
      S:
       pAC(pAC(x11,x12),x13) -> pAC(x11,x12)
       pAC(x11,pAC(x12,x13)) -> pAC(x12,x13)
      AC-RPO Processor:
       argument filtering:
        pi(pAC) = []
        pi(m) = [0,1]
        pi(i#) = [0]
       precedence:
        m > i# > pAC
       status:
        m:mul  
       problem:
        Equations#:
         pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
         pAC(x6,x7) -> pAC(x7,x6)
         pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
         pAC(x7,x6) -> pAC(x6,x7)
        DPs:
         
        Equations:
         pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
         pAC(x6,x7) -> pAC(x7,x6)
         pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
         pAC(x7,x6) -> pAC(x6,x7)
        TRS:
         
        S:
         pAC(pAC(x11,x12),x13) -> pAC(x11,x12)
         pAC(x11,pAC(x12,x13)) -> pAC(x12,x13)
       Qed
    
    Equations#:
     p{AC,#}(pAC(x6,x7),x8) -> p{AC,#}(x6,pAC(x7,x8))
     p{AC,#}(x6,x7) -> p{AC,#}(x7,x6)
     p{AC,#}(x6,pAC(x7,x8)) -> p{AC,#}(pAC(x6,x7),x8)
     p{AC,#}(x7,x6) -> p{AC,#}(x6,x7)
    DPs:
     m#(x,m(y,z)) -> m#(m(x,y),z)
     m#(x,m(y,z)) -> m#(x,y)
    Equations:
     pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
     pAC(x6,x7) -> pAC(x7,x6)
     pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
     pAC(x7,x6) -> pAC(x6,x7)
    TRS:
     pAC(x,0()) -> x
     pAC(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(pAC(x,u),pAC(y,v),pAC(z,w))
     m(T(x),T(y)) -> T(pAC(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))
    S:
     p{AC,#}(pAC(x11,x12),x13) -> p{AC,#}(x11,x12)
     p{AC,#}(x11,pAC(x12,x13)) -> p{AC,#}(x12,x13)
    AC-DP unlabeling:
     Equations#:
      pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
      pAC(x6,x7) -> pAC(x7,x6)
      pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
      pAC(x7,x6) -> pAC(x6,x7)
     DPs:
      m#(x,m(y,z)) -> m#(m(x,y),z)
      m#(x,m(y,z)) -> m#(x,y)
     Equations:
      pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
      pAC(x6,x7) -> pAC(x7,x6)
      pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
      pAC(x7,x6) -> pAC(x6,x7)
     TRS:
      pAC(x,0()) -> x
      pAC(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(pAC(x,u),pAC(y,v),pAC(z,w))
      m(T(x),T(y)) -> T(pAC(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))
     S:
      pAC(pAC(x11,x12),x13) -> pAC(x11,x12)
      pAC(x11,pAC(x12,x13)) -> pAC(x12,x13)
     Usable Rule Processor:
      Equations#:
       pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
       pAC(x6,x7) -> pAC(x7,x6)
       pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
       pAC(x7,x6) -> pAC(x6,x7)
      DPs:
       m#(x,m(y,z)) -> m#(m(x,y),z)
       m#(x,m(y,z)) -> m#(x,y)
      Equations:
       pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
       pAC(x6,x7) -> pAC(x7,x6)
       pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
       pAC(x7,x6) -> pAC(x6,x7)
      TRS:
       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
       m(x,i(x)) -> I()
       m(x,m(i(x),y)) -> y
       m(Tr(x,y,z),Tr(u,v,w)) -> Tr(pAC(x,u),pAC(y,v),pAC(z,w))
       m(T(x),T(y)) -> T(pAC(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))
       pAC(x,0()) -> x
       pAC(minus(x),x) -> 0()
      S:
       pAC(pAC(x11,x12),x13) -> pAC(x11,x12)
       pAC(x11,pAC(x12,x13)) -> pAC(x12,x13)
      AC-RPO Processor:
       argument filtering:
        pi(pAC) = [0,1]
        pi(0) = []
        pi(minus) = []
        pi(I) = []
        pi(m) = [0,1]
        pi(i) = 0
        pi(Tr) = 2
        pi(T) = 0
        pi(M) = []
        pi(m#) = [1]
       precedence:
        I > M > i > pAC > m > m# > Tr > T > minus > 0
       status:
        m#:lex  Tr:mul  m:lex  
       problem:
        Equations#:
         pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
         pAC(x6,x7) -> pAC(x7,x6)
         pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
         pAC(x7,x6) -> pAC(x6,x7)
        DPs:
         
        Equations:
         pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
         pAC(x6,x7) -> pAC(x7,x6)
         pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
         pAC(x7,x6) -> pAC(x6,x7)
        TRS:
         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
         m(x,i(x)) -> I()
         m(x,m(i(x),y)) -> y
         m(Tr(x,y,z),Tr(u,v,w)) -> Tr(pAC(x,u),pAC(y,v),pAC(z,w))
         m(T(x),T(y)) -> T(pAC(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))
         pAC(x,0()) -> x
         pAC(minus(x),x) -> 0()
        S:
         pAC(pAC(x11,x12),x13) -> pAC(x11,x12)
         pAC(x11,pAC(x12,x13)) -> pAC(x12,x13)
       Qed
    
    Equations#:
     p{AC,#}(pAC(x6,x7),x8) -> p{AC,#}(x6,pAC(x7,x8))
     p{AC,#}(x6,x7) -> p{AC,#}(x7,x6)
     p{AC,#}(x6,pAC(x7,x8)) -> p{AC,#}(pAC(x6,x7),x8)
     p{AC,#}(x7,x6) -> p{AC,#}(x6,x7)
    DPs:
     p{AC,#}(x10,pAC(minus(x),x)) -> p{AC,#}(x10,0())
     p{AC,#}(x9,pAC(x,0())) -> p{AC,#}(x9,x)
    Equations:
     pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
     pAC(x6,x7) -> pAC(x7,x6)
     pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
     pAC(x7,x6) -> pAC(x6,x7)
    TRS:
     pAC(x,0()) -> x
     pAC(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(pAC(x,u),pAC(y,v),pAC(z,w))
     m(T(x),T(y)) -> T(pAC(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))
    S:
     p{AC,#}(pAC(x11,x12),x13) -> p{AC,#}(x11,x12)
     p{AC,#}(x11,pAC(x12,x13)) -> p{AC,#}(x12,x13)
    AC-DP unlabeling:
     Equations#:
      pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
      pAC(x6,x7) -> pAC(x7,x6)
      pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
      pAC(x7,x6) -> pAC(x6,x7)
     DPs:
      pAC(x10,pAC(minus(x),x)) -> pAC(x10,0())
      pAC(x9,pAC(x,0())) -> pAC(x9,x)
     Equations:
      pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
      pAC(x6,x7) -> pAC(x7,x6)
      pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
      pAC(x7,x6) -> pAC(x6,x7)
     TRS:
      pAC(x,0()) -> x
      pAC(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(pAC(x,u),pAC(y,v),pAC(z,w))
      m(T(x),T(y)) -> T(pAC(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))
     S:
      pAC(pAC(x11,x12),x13) -> pAC(x11,x12)
      pAC(x11,pAC(x12,x13)) -> pAC(x12,x13)
     Usable Rule Processor:
      Equations#:
       pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
       pAC(x6,x7) -> pAC(x7,x6)
       pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
       pAC(x7,x6) -> pAC(x6,x7)
      DPs:
       pAC(x10,pAC(minus(x),x)) -> pAC(x10,0())
       pAC(x9,pAC(x,0())) -> pAC(x9,x)
      Equations:
       pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
       pAC(x6,x7) -> pAC(x7,x6)
       pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
       pAC(x7,x6) -> pAC(x6,x7)
      TRS:
       pAC(x,0()) -> x
       pAC(minus(x),x) -> 0()
      S:
       pAC(pAC(x11,x12),x13) -> pAC(x11,x12)
       pAC(x11,pAC(x12,x13)) -> pAC(x12,x13)
      AC-RPO Processor:
       argument filtering:
        pi(pAC) = [0,1]
        pi(0) = []
        pi(minus) = []
       precedence:
        minus > 0 > pAC
       status:
        
       problem:
        Equations#:
         pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
         pAC(x6,x7) -> pAC(x7,x6)
         pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
         pAC(x7,x6) -> pAC(x6,x7)
        DPs:
         
        Equations:
         pAC(pAC(x6,x7),x8) -> pAC(x6,pAC(x7,x8))
         pAC(x6,x7) -> pAC(x7,x6)
         pAC(x6,pAC(x7,x8)) -> pAC(pAC(x6,x7),x8)
         pAC(x7,x6) -> pAC(x6,x7)
        TRS:
         pAC(x,0()) -> x
         pAC(minus(x),x) -> 0()
        S:
         pAC(pAC(x11,x12),x13) -> pAC(x11,x12)
         pAC(x11,pAC(x12,x13)) -> pAC(x12,x13)
       Qed