YES
Time: 0.183

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,i(x)) -> zero()
  pAC(i(x),x) -> zero()
  pAC(zero(),x) -> x
  pAC(x,zero()) -> x
  pAC(a(),pAC(a(),pAC(a(),pAC(a(),pAC(a(),pAC(a(),a())))))) -> zero()
  pAC(b(),pAC(b(),pAC(b(),pAC(b(),pAC(b(),pAC(b(),b())))))) -> zero()
  pAC(a(),pAC(b(),pAC(a(),b()))) -> zero()
  pAC(i(a()),pAC(b(),pAC(i(a()),pAC(b(),pAC(i(a()),b()))))) -> zero()

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:
   p{AC,#}(x6,pAC(x,i(x))) -> p{AC,#}(x6,zero())
   p{AC,#}(x7,pAC(i(x),x)) -> p{AC,#}(x7,zero())
   p{AC,#}(x8,pAC(zero(),x)) -> p{AC,#}(x8,x)
   p{AC,#}(x9,pAC(x,zero())) -> p{AC,#}(x9,x)
   p{AC,#}(x10,pAC(a(),pAC(a(),pAC(a(),pAC(a(),pAC(a(),pAC(a(),a()))))))) -> p{AC,#}(x10,zero())
   p{AC,#}(x11,pAC(b(),pAC(b(),pAC(b(),pAC(b(),pAC(b(),pAC(b(),b()))))))) -> p{AC,#}(x11,zero())
   p{AC,#}(x12,pAC(a(),pAC(b(),pAC(a(),b())))) -> p{AC,#}(x12,zero())
   p{AC,#}(x13,pAC(i(a()),pAC(b(),pAC(i(a()),pAC(b(),pAC(i(a()),b())))))) -> p{AC,#}(x13,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,i(x)) -> zero()
   pAC(i(x),x) -> zero()
   pAC(zero(),x) -> x
   pAC(x,zero()) -> x
   pAC(a(),pAC(a(),pAC(a(),pAC(a(),pAC(a(),pAC(a(),a())))))) -> zero()
   pAC(b(),pAC(b(),pAC(b(),pAC(b(),pAC(b(),pAC(b(),b())))))) -> zero()
   pAC(a(),pAC(b(),pAC(a(),b()))) -> zero()
   pAC(i(a()),pAC(b(),pAC(i(a()),pAC(b(),pAC(i(a()),b()))))) -> zero()
  S:
   p{AC,#}(pAC(x14,x15),x16) -> p{AC,#}(x14,x15)
   p{AC,#}(x14,pAC(x15,x16)) -> p{AC,#}(x15,x16)
  AC-DP unlabeling:
   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)
   DPs:
    pAC(x6,pAC(x,i(x))) -> pAC(x6,zero())
    pAC(x7,pAC(i(x),x)) -> pAC(x7,zero())
    pAC(x8,pAC(zero(),x)) -> pAC(x8,x)
    pAC(x9,pAC(x,zero())) -> pAC(x9,x)
    pAC(x10,pAC(a(),pAC(a(),pAC(a(),pAC(a(),pAC(a(),pAC(a(),a()))))))) -> pAC(x10,zero())
    pAC(x11,pAC(b(),pAC(b(),pAC(b(),pAC(b(),pAC(b(),pAC(b(),b()))))))) -> pAC(x11,zero())
    pAC(x12,pAC(a(),pAC(b(),pAC(a(),b())))) -> pAC(x12,zero())
    pAC(x13,pAC(i(a()),pAC(b(),pAC(i(a()),pAC(b(),pAC(i(a()),b())))))) -> pAC(x13,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,i(x)) -> zero()
    pAC(i(x),x) -> zero()
    pAC(zero(),x) -> x
    pAC(x,zero()) -> x
    pAC(a(),pAC(a(),pAC(a(),pAC(a(),pAC(a(),pAC(a(),a())))))) -> zero()
    pAC(b(),pAC(b(),pAC(b(),pAC(b(),pAC(b(),pAC(b(),b())))))) -> zero()
    pAC(a(),pAC(b(),pAC(a(),b()))) -> zero()
    pAC(i(a()),pAC(b(),pAC(i(a()),pAC(b(),pAC(i(a()),b()))))) -> zero()
   S:
    pAC(pAC(x14,x15),x16) -> pAC(x14,x15)
    pAC(x14,pAC(x15,x16)) -> pAC(x15,x16)
   AC-RPO Processor:
    argument filtering:
     pi(pAC) = [0,1]
     pi(i) = []
     pi(zero) = []
     pi(a) = []
     pi(b) = []
    precedence:
     a > b > pAC > zero > i
    status:
     
    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)
     DPs:
      
     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,i(x)) -> zero()
      pAC(i(x),x) -> zero()
      pAC(zero(),x) -> x
      pAC(x,zero()) -> x
      pAC(a(),pAC(a(),pAC(a(),pAC(a(),pAC(a(),pAC(a(),a())))))) -> zero()
      pAC(b(),pAC(b(),pAC(b(),pAC(b(),pAC(b(),pAC(b(),b())))))) -> zero()
      pAC(a(),pAC(b(),pAC(a(),b()))) -> zero()
      pAC(i(a()),pAC(b(),pAC(i(a()),pAC(b(),pAC(i(a()),b()))))) -> zero()
     S:
      pAC(pAC(x14,x15),x16) -> pAC(x14,x15)
      pAC(x14,pAC(x15,x16)) -> pAC(x15,x16)
    Qed