MAYBE
Time: 0.013

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:
 Open