MAYBE
Time: 0.015

Problem:
 Equations:
  xorAC(xorAC(x3,x4),x5) -> xorAC(x3,xorAC(x4,x5))
  xorAC(x3,x4) -> xorAC(x4,x3)
  andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
  andAC(x3,x4) -> andAC(x4,x3)
  xorAC(x3,xorAC(x4,x5)) -> xorAC(xorAC(x3,x4),x5)
  xorAC(x4,x3) -> xorAC(x3,x4)
  andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
  andAC(x4,x3) -> andAC(x3,x4)
 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:
 Open