MAYBE
Time: 0.010

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:
 Open