MAYBE
Time: 1.472

Problem:
 Equations:
  pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5))
  pAC(x3,x4) -> pAC(x4,x3)
  mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5))
  mAC(x3,x4) -> mAC(x4,x3)
  gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5))
  gAC(x3,x4) -> gAC(x4,x3)
  pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5)
  pAC(x4,x3) -> pAC(x3,x4)
  mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5)
  mAC(x4,x3) -> mAC(x3,x4)
  gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5)
  gAC(x4,x3) -> gAC(x3,x4)
 TRS:
  pAC(x,zero()) -> x
  pAC(i(x),x) -> zero()
  mAC(one(),x) -> x
  mAC(x,one()) -> x
  mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y))
  mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z))
  gAC(x,n()) -> x
  gAC(x,inv(x)) -> n()
  sm(x,sm(y,z)) -> sm(mAC(x,y),z)
  sm(one(),z) -> z
  gAC(sm(x,z),sm(y,z)) -> sm(pAC(x,y),z)
  sm(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z))
  smm(x,smm(y,z)) -> smm(mAC(x,y),z)
  smm(one(),z) -> z
  gAC(smm(x,z),smm(y,z)) -> smm(pAC(x,y),z)
  smm(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z))

Proof:
 DP Processor:
  Equations#:
   p{AC,#}(pAC(x3,x4),x5) -> p{AC,#}(x3,pAC(x4,x5))
   p{AC,#}(x3,x4) -> p{AC,#}(x4,x3)
   m{AC,#}(mAC(x3,x4),x5) -> m{AC,#}(x3,mAC(x4,x5))
   m{AC,#}(x3,x4) -> m{AC,#}(x4,x3)
   g{AC,#}(gAC(x3,x4),x5) -> g{AC,#}(x3,gAC(x4,x5))
   g{AC,#}(x3,x4) -> g{AC,#}(x4,x3)
   p{AC,#}(x3,pAC(x4,x5)) -> p{AC,#}(pAC(x3,x4),x5)
   p{AC,#}(x4,x3) -> p{AC,#}(x3,x4)
   m{AC,#}(x3,mAC(x4,x5)) -> m{AC,#}(mAC(x3,x4),x5)
   m{AC,#}(x4,x3) -> m{AC,#}(x3,x4)
   g{AC,#}(x3,gAC(x4,x5)) -> g{AC,#}(gAC(x3,x4),x5)
   g{AC,#}(x4,x3) -> g{AC,#}(x3,x4)
  DPs:
   m{AC,#}(z,pAC(x,y)) -> m{AC,#}(z,y)
   m{AC,#}(z,pAC(x,y)) -> m{AC,#}(z,x)
   m{AC,#}(z,pAC(x,y)) -> p{AC,#}(mAC(z,x),mAC(z,y))
   m{AC,#}(pAC(x,y),z) -> m{AC,#}(y,z)
   m{AC,#}(pAC(x,y),z) -> m{AC,#}(x,z)
   m{AC,#}(pAC(x,y),z) -> p{AC,#}(mAC(x,z),mAC(y,z))
   sm#(x,sm(y,z)) -> m{AC,#}(x,y)
   sm#(x,sm(y,z)) -> sm#(mAC(x,y),z)
   g{AC,#}(sm(x,z),sm(y,z)) -> p{AC,#}(x,y)
   g{AC,#}(sm(x,z),sm(y,z)) -> sm#(pAC(x,y),z)
   sm#(x,gAC(y,z)) -> sm#(x,z)
   sm#(x,gAC(y,z)) -> sm#(x,y)
   sm#(x,gAC(y,z)) -> g{AC,#}(sm(x,y),sm(x,z))
   smm#(x,smm(y,z)) -> m{AC,#}(x,y)
   smm#(x,smm(y,z)) -> smm#(mAC(x,y),z)
   g{AC,#}(smm(x,z),smm(y,z)) -> p{AC,#}(x,y)
   g{AC,#}(smm(x,z),smm(y,z)) -> smm#(pAC(x,y),z)
   smm#(x,gAC(y,z)) -> smm#(x,z)
   smm#(x,gAC(y,z)) -> smm#(x,y)
   smm#(x,gAC(y,z)) -> g{AC,#}(smm(x,y),smm(x,z))
   p{AC,#}(x6,pAC(x,zero())) -> p{AC,#}(x6,x)
   p{AC,#}(x7,pAC(i(x),x)) -> p{AC,#}(x7,zero())
   m{AC,#}(x8,mAC(one(),x)) -> m{AC,#}(x8,x)
   m{AC,#}(x9,mAC(x,one())) -> m{AC,#}(x9,x)
   m{AC,#}(x10,mAC(z,pAC(x,y))) -> m{AC,#}(z,y)
   m{AC,#}(x10,mAC(z,pAC(x,y))) -> m{AC,#}(z,x)
   m{AC,#}(x10,mAC(z,pAC(x,y))) -> p{AC,#}(mAC(z,x),mAC(z,y))
   m{AC,#}(x10,mAC(z,pAC(x,y))) -> m{AC,#}(x10,pAC(mAC(z,x),mAC(z,y)))
   m{AC,#}(x11,mAC(pAC(x,y),z)) -> m{AC,#}(y,z)
   m{AC,#}(x11,mAC(pAC(x,y),z)) -> m{AC,#}(x,z)
   m{AC,#}(x11,mAC(pAC(x,y),z)) -> p{AC,#}(mAC(x,z),mAC(y,z))
   m{AC,#}(x11,mAC(pAC(x,y),z)) -> m{AC,#}(x11,pAC(mAC(x,z),mAC(y,z)))
   g{AC,#}(x12,gAC(x,n())) -> g{AC,#}(x12,x)
   g{AC,#}(x13,gAC(x,inv(x))) -> g{AC,#}(x13,n())
   g{AC,#}(x14,gAC(sm(x,z),sm(y,z))) -> p{AC,#}(x,y)
   g{AC,#}(x14,gAC(sm(x,z),sm(y,z))) -> sm#(pAC(x,y),z)
   g{AC,#}(x14,gAC(sm(x,z),sm(y,z))) -> g{AC,#}(x14,sm(pAC(x,y),z))
   g{AC,#}(x15,gAC(smm(x,z),smm(y,z))) -> p{AC,#}(x,y)
   g{AC,#}(x15,gAC(smm(x,z),smm(y,z))) -> smm#(pAC(x,y),z)
   g{AC,#}(x15,gAC(smm(x,z),smm(y,z))) -> g{AC,#}(x15,smm(pAC(x,y),z))
  Equations:
   pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5))
   pAC(x3,x4) -> pAC(x4,x3)
   mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5))
   mAC(x3,x4) -> mAC(x4,x3)
   gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5))
   gAC(x3,x4) -> gAC(x4,x3)
   pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5)
   pAC(x4,x3) -> pAC(x3,x4)
   mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5)
   mAC(x4,x3) -> mAC(x3,x4)
   gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5)
   gAC(x4,x3) -> gAC(x3,x4)
  TRS:
   pAC(x,zero()) -> x
   pAC(i(x),x) -> zero()
   mAC(one(),x) -> x
   mAC(x,one()) -> x
   mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y))
   mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z))
   gAC(x,n()) -> x
   gAC(x,inv(x)) -> n()
   sm(x,sm(y,z)) -> sm(mAC(x,y),z)
   sm(one(),z) -> z
   gAC(sm(x,z),sm(y,z)) -> sm(pAC(x,y),z)
   sm(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z))
   smm(x,smm(y,z)) -> smm(mAC(x,y),z)
   smm(one(),z) -> z
   gAC(smm(x,z),smm(y,z)) -> smm(pAC(x,y),z)
   smm(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z))
  S:
   p{AC,#}(pAC(x16,x17),x18) -> p{AC,#}(x16,x17)
   p{AC,#}(x16,pAC(x17,x18)) -> p{AC,#}(x17,x18)
   m{AC,#}(mAC(x16,x17),x18) -> m{AC,#}(x16,x17)
   m{AC,#}(x16,mAC(x17,x18)) -> m{AC,#}(x17,x18)
   g{AC,#}(gAC(x16,x17),x18) -> g{AC,#}(x16,x17)
   g{AC,#}(x16,gAC(x17,x18)) -> g{AC,#}(x17,x18)
  AC-EDG Processor:
   Equations#:
    p{AC,#}(pAC(x3,x4),x5) -> p{AC,#}(x3,pAC(x4,x5))
    p{AC,#}(x3,x4) -> p{AC,#}(x4,x3)
    m{AC,#}(mAC(x3,x4),x5) -> m{AC,#}(x3,mAC(x4,x5))
    m{AC,#}(x3,x4) -> m{AC,#}(x4,x3)
    g{AC,#}(gAC(x3,x4),x5) -> g{AC,#}(x3,gAC(x4,x5))
    g{AC,#}(x3,x4) -> g{AC,#}(x4,x3)
    p{AC,#}(x3,pAC(x4,x5)) -> p{AC,#}(pAC(x3,x4),x5)
    p{AC,#}(x4,x3) -> p{AC,#}(x3,x4)
    m{AC,#}(x3,mAC(x4,x5)) -> m{AC,#}(mAC(x3,x4),x5)
    m{AC,#}(x4,x3) -> m{AC,#}(x3,x4)
    g{AC,#}(x3,gAC(x4,x5)) -> g{AC,#}(gAC(x3,x4),x5)
    g{AC,#}(x4,x3) -> g{AC,#}(x3,x4)
   DPs:
    m{AC,#}(z,pAC(x,y)) -> m{AC,#}(z,y)
    m{AC,#}(z,pAC(x,y)) -> m{AC,#}(z,x)
    m{AC,#}(z,pAC(x,y)) -> p{AC,#}(mAC(z,x),mAC(z,y))
    m{AC,#}(pAC(x,y),z) -> m{AC,#}(y,z)
    m{AC,#}(pAC(x,y),z) -> m{AC,#}(x,z)
    m{AC,#}(pAC(x,y),z) -> p{AC,#}(mAC(x,z),mAC(y,z))
    sm#(x,sm(y,z)) -> m{AC,#}(x,y)
    sm#(x,sm(y,z)) -> sm#(mAC(x,y),z)
    g{AC,#}(sm(x,z),sm(y,z)) -> p{AC,#}(x,y)
    g{AC,#}(sm(x,z),sm(y,z)) -> sm#(pAC(x,y),z)
    sm#(x,gAC(y,z)) -> sm#(x,z)
    sm#(x,gAC(y,z)) -> sm#(x,y)
    sm#(x,gAC(y,z)) -> g{AC,#}(sm(x,y),sm(x,z))
    smm#(x,smm(y,z)) -> m{AC,#}(x,y)
    smm#(x,smm(y,z)) -> smm#(mAC(x,y),z)
    g{AC,#}(smm(x,z),smm(y,z)) -> p{AC,#}(x,y)
    g{AC,#}(smm(x,z),smm(y,z)) -> smm#(pAC(x,y),z)
    smm#(x,gAC(y,z)) -> smm#(x,z)
    smm#(x,gAC(y,z)) -> smm#(x,y)
    smm#(x,gAC(y,z)) -> g{AC,#}(smm(x,y),smm(x,z))
    p{AC,#}(x6,pAC(x,zero())) -> p{AC,#}(x6,x)
    p{AC,#}(x7,pAC(i(x),x)) -> p{AC,#}(x7,zero())
    m{AC,#}(x8,mAC(one(),x)) -> m{AC,#}(x8,x)
    m{AC,#}(x9,mAC(x,one())) -> m{AC,#}(x9,x)
    m{AC,#}(x10,mAC(z,pAC(x,y))) -> m{AC,#}(z,y)
    m{AC,#}(x10,mAC(z,pAC(x,y))) -> m{AC,#}(z,x)
    m{AC,#}(x10,mAC(z,pAC(x,y))) -> p{AC,#}(mAC(z,x),mAC(z,y))
    m{AC,#}(x10,mAC(z,pAC(x,y))) -> m{AC,#}(x10,pAC(mAC(z,x),mAC(z,y)))
    m{AC,#}(x11,mAC(pAC(x,y),z)) -> m{AC,#}(y,z)
    m{AC,#}(x11,mAC(pAC(x,y),z)) -> m{AC,#}(x,z)
    m{AC,#}(x11,mAC(pAC(x,y),z)) -> p{AC,#}(mAC(x,z),mAC(y,z))
    m{AC,#}(x11,mAC(pAC(x,y),z)) -> m{AC,#}(x11,pAC(mAC(x,z),mAC(y,z)))
    g{AC,#}(x12,gAC(x,n())) -> g{AC,#}(x12,x)
    g{AC,#}(x13,gAC(x,inv(x))) -> g{AC,#}(x13,n())
    g{AC,#}(x14,gAC(sm(x,z),sm(y,z))) -> p{AC,#}(x,y)
    g{AC,#}(x14,gAC(sm(x,z),sm(y,z))) -> sm#(pAC(x,y),z)
    g{AC,#}(x14,gAC(sm(x,z),sm(y,z))) -> g{AC,#}(x14,sm(pAC(x,y),z))
    g{AC,#}(x15,gAC(smm(x,z),smm(y,z))) -> p{AC,#}(x,y)
    g{AC,#}(x15,gAC(smm(x,z),smm(y,z))) -> smm#(pAC(x,y),z)
    g{AC,#}(x15,gAC(smm(x,z),smm(y,z))) -> g{AC,#}(x15,smm(pAC(x,y),z))
   Equations:
    pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5))
    pAC(x3,x4) -> pAC(x4,x3)
    mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5))
    mAC(x3,x4) -> mAC(x4,x3)
    gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5))
    gAC(x3,x4) -> gAC(x4,x3)
    pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5)
    pAC(x4,x3) -> pAC(x3,x4)
    mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5)
    mAC(x4,x3) -> mAC(x3,x4)
    gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5)
    gAC(x4,x3) -> gAC(x3,x4)
   TRS:
    pAC(x,zero()) -> x
    pAC(i(x),x) -> zero()
    mAC(one(),x) -> x
    mAC(x,one()) -> x
    mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y))
    mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z))
    gAC(x,n()) -> x
    gAC(x,inv(x)) -> n()
    sm(x,sm(y,z)) -> sm(mAC(x,y),z)
    sm(one(),z) -> z
    gAC(sm(x,z),sm(y,z)) -> sm(pAC(x,y),z)
    sm(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z))
    smm(x,smm(y,z)) -> smm(mAC(x,y),z)
    smm(one(),z) -> z
    gAC(smm(x,z),smm(y,z)) -> smm(pAC(x,y),z)
    smm(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z))
   S:
    p{AC,#}(pAC(x16,x17),x18) -> p{AC,#}(x16,x17)
    p{AC,#}(x16,pAC(x17,x18)) -> p{AC,#}(x17,x18)
    m{AC,#}(mAC(x16,x17),x18) -> m{AC,#}(x16,x17)
    m{AC,#}(x16,mAC(x17,x18)) -> m{AC,#}(x17,x18)
    g{AC,#}(gAC(x16,x17),x18) -> g{AC,#}(x16,x17)
    g{AC,#}(x16,gAC(x17,x18)) -> g{AC,#}(x17,x18)
   Open