MAYBE
Time: 0.333

Problem:
 Equations:
  pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5))
  pAC(x3,x4) -> pAC(x4,x3)
  pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5)
  pAC(x4,x3) -> pAC(x3,x4)
 TRS:
  pAC(x,zero()) -> x
  pAC(i(x),x) -> zero()
  m(zero(),x) -> zero()
  m(x,zero()) -> zero()
  m(one(),x) -> x
  m(x,one()) -> x
  g1(one()) -> one()
  g2(one()) -> one()
  m(x,m(y,z)) -> m(m(x,y),z)
  m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y))
  m(pAC(x,y),z) -> pAC(m(x,z),m(y,z))
  m(g1(x),g1(y)) -> g1(m(x,y))
  m(g2(x),g2(y)) -> g2(m(x,y))
  m(g2(x),g1(y)) -> m(g1(y),g2(x))

Proof:
 DP Processor:
  Equations#:
   p{AC,#}(pAC(x3,x4),x5) -> p{AC,#}(x3,pAC(x4,x5))
   p{AC,#}(x3,x4) -> p{AC,#}(x4,x3)
   p{AC,#}(x3,pAC(x4,x5)) -> p{AC,#}(pAC(x3,x4),x5)
   p{AC,#}(x4,x3) -> p{AC,#}(x3,x4)
  DPs:
   m#(x,m(y,z)) -> m#(x,y)
   m#(x,m(y,z)) -> m#(m(x,y),z)
   m#(z,pAC(x,y)) -> m#(z,y)
   m#(z,pAC(x,y)) -> m#(z,x)
   m#(z,pAC(x,y)) -> p{AC,#}(m(z,x),m(z,y))
   m#(pAC(x,y),z) -> m#(y,z)
   m#(pAC(x,y),z) -> m#(x,z)
   m#(pAC(x,y),z) -> p{AC,#}(m(x,z),m(y,z))
   m#(g1(x),g1(y)) -> m#(x,y)
   m#(g1(x),g1(y)) -> g1#(m(x,y))
   m#(g2(x),g2(y)) -> m#(x,y)
   m#(g2(x),g2(y)) -> g2#(m(x,y))
   m#(g2(x),g1(y)) -> m#(g1(y),g2(x))
   p{AC,#}(x6,pAC(x,zero())) -> p{AC,#}(x6,x)
   p{AC,#}(x7,pAC(i(x),x)) -> p{AC,#}(x7,zero())
  Equations:
   pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5))
   pAC(x3,x4) -> pAC(x4,x3)
   pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5)
   pAC(x4,x3) -> pAC(x3,x4)
  TRS:
   pAC(x,zero()) -> x
   pAC(i(x),x) -> zero()
   m(zero(),x) -> zero()
   m(x,zero()) -> zero()
   m(one(),x) -> x
   m(x,one()) -> x
   g1(one()) -> one()
   g2(one()) -> one()
   m(x,m(y,z)) -> m(m(x,y),z)
   m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y))
   m(pAC(x,y),z) -> pAC(m(x,z),m(y,z))
   m(g1(x),g1(y)) -> g1(m(x,y))
   m(g2(x),g2(y)) -> g2(m(x,y))
   m(g2(x),g1(y)) -> m(g1(y),g2(x))
  S:
   p{AC,#}(pAC(x8,x9),x10) -> p{AC,#}(x8,x9)
   p{AC,#}(x8,pAC(x9,x10)) -> p{AC,#}(x9,x10)
  AC-EDG Processor:
   Equations#:
    p{AC,#}(pAC(x3,x4),x5) -> p{AC,#}(x3,pAC(x4,x5))
    p{AC,#}(x3,x4) -> p{AC,#}(x4,x3)
    p{AC,#}(x3,pAC(x4,x5)) -> p{AC,#}(pAC(x3,x4),x5)
    p{AC,#}(x4,x3) -> p{AC,#}(x3,x4)
   DPs:
    m#(x,m(y,z)) -> m#(x,y)
    m#(x,m(y,z)) -> m#(m(x,y),z)
    m#(z,pAC(x,y)) -> m#(z,y)
    m#(z,pAC(x,y)) -> m#(z,x)
    m#(z,pAC(x,y)) -> p{AC,#}(m(z,x),m(z,y))
    m#(pAC(x,y),z) -> m#(y,z)
    m#(pAC(x,y),z) -> m#(x,z)
    m#(pAC(x,y),z) -> p{AC,#}(m(x,z),m(y,z))
    m#(g1(x),g1(y)) -> m#(x,y)
    m#(g1(x),g1(y)) -> g1#(m(x,y))
    m#(g2(x),g2(y)) -> m#(x,y)
    m#(g2(x),g2(y)) -> g2#(m(x,y))
    m#(g2(x),g1(y)) -> m#(g1(y),g2(x))
    p{AC,#}(x6,pAC(x,zero())) -> p{AC,#}(x6,x)
    p{AC,#}(x7,pAC(i(x),x)) -> p{AC,#}(x7,zero())
   Equations:
    pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5))
    pAC(x3,x4) -> pAC(x4,x3)
    pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5)
    pAC(x4,x3) -> pAC(x3,x4)
   TRS:
    pAC(x,zero()) -> x
    pAC(i(x),x) -> zero()
    m(zero(),x) -> zero()
    m(x,zero()) -> zero()
    m(one(),x) -> x
    m(x,one()) -> x
    g1(one()) -> one()
    g2(one()) -> one()
    m(x,m(y,z)) -> m(m(x,y),z)
    m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y))
    m(pAC(x,y),z) -> pAC(m(x,z),m(y,z))
    m(g1(x),g1(y)) -> g1(m(x,y))
    m(g2(x),g2(y)) -> g2(m(x,y))
    m(g2(x),g1(y)) -> m(g1(y),g2(x))
   S:
    p{AC,#}(pAC(x8,x9),x10) -> p{AC,#}(x8,x9)
    p{AC,#}(x8,pAC(x9,x10)) -> p{AC,#}(x9,x10)
   Open