YES
Time: 0.015

Problem:
 Equations:
  
 TRS:
  xorAC(F(),x) -> x
  xorAC(neg(x),x) -> F()
  andAC(T(),x) -> x
  andAC(F(),x) -> F()
  andAC(x,x) -> x
  andAC(xorAC(x,y),z) -> xorAC(andAC(x,z),andAC(y,z))
  xorAC(x,x) -> F()
  impl(x,y) -> xorAC(andAC(x,y),xorAC(T(),x))
  orAC(x,y) -> xorAC(andAC(x,y),xorAC(x,y))
  equiv(x,y) -> xorAC(xorAC(T(),y),x)
  neg(x) -> xorAC(T(),x)

Proof:
 AC-RPO Processor:
  precedence:
   equiv > impl > neg > T > orAC > andAC > xorAC > F
  status:
   equiv:mul  impl:mul  
  problem:
   Equations:
    
   TRS:
    
  Qed