MAYBE
Time: 0.238

Problem:
 Equations:
  pAC(pAC(x4,x5),x6) -> pAC(x4,pAC(x5,x6))
  pAC(x4,x5) -> pAC(x5,x4)
  pAC(x4,pAC(x5,x6)) -> pAC(pAC(x4,x5),x6)
  pAC(x5,x4) -> pAC(x4,x5)
 TRS:
  pAC(zero(),x) -> x
  pAC(i(x),x) -> zero()
  phi(zero(),y1) -> y1
  phi(y1,phi(y2,x)) -> phi(pAC(y1,y2),x)
  phi(g1(x),g2(y1)) -> phi(g2(y1),g1(x))
  g1(zero()) -> zero()
  g2(zero()) -> zero()
  g1(pAC(x,y)) -> pAC(g1(x),g1(y))
  g2(pAC(x,y)) -> pAC(g2(x),g2(y))

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