MAYBE
Time: 0.015

Problem:
 Equations:
  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)
  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:
  eqC(x,x) -> true()
  not(eqC(x,y)) -> neqC(x,y)
  not(neqC(x,y)) -> eqC(x,y)
  not(true()) -> false()
  not(false()) -> true()
  not(not(x)) -> x
  not(andAC(x,y)) -> orAC(not(x),not(y))
  not(orAC(x,y)) -> andAC(not(x),not(y))
  neqC(x,x) -> false()
  orAC(andAC(x,y),z) -> andAC(orAC(x,z),orAC(y,z))
  orAC(x,x) -> x
  orAC(x,true()) -> true()
  orAC(x,false()) -> x
  andAC(x,x) -> x
  andAC(x,true()) -> x
  andAC(x,false()) -> false()
  andAC(x,orAC(x,y)) -> x

Proof:
 Open