MAYBE
Time: 3.736

Problem:
 Equations:
  
 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