YES
Time: 0.012

Problem:
 Equations:
  
 TRS:
  or(x,y) -> xorAC(x,xorAC(y,andAC(x,y)))
  not(x) -> xorAC(x,1())
  xorAC(x,x) -> 0()
  xorAC(0(),x) -> x
  andAC(xorAC(x,y),z) -> xorAC(andAC(x,z),andAC(y,z))
  andAC(x,x) -> x

Proof:
 AC-RPO Processor:
  precedence:
   not > or > andAC > xorAC > 0 > 1
  status:
   or:mul  
  problem:
   Equations:
    
   TRS:
    
  Qed