MAYBE
Time: 0.022

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)
  orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
  orAC(x3,x4) -> orAC(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)
  orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
  orAC(x4,x3) -> orAC(x3,x4)
 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