MAYBE
Time: 0.350

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:
 DP Processor:
  Equations#:
   and{AC,#}(andAC(x3,x4),x5) -> and{AC,#}(x3,andAC(x4,x5))
   and{AC,#}(x3,x4) -> and{AC,#}(x4,x3)
   or{AC,#}(orAC(x3,x4),x5) -> or{AC,#}(x3,orAC(x4,x5))
   or{AC,#}(x3,x4) -> or{AC,#}(x4,x3)
   and{AC,#}(x3,andAC(x4,x5)) -> and{AC,#}(andAC(x3,x4),x5)
   and{AC,#}(x4,x3) -> and{AC,#}(x3,x4)
   or{AC,#}(x3,orAC(x4,x5)) -> or{AC,#}(orAC(x3,x4),x5)
   or{AC,#}(x4,x3) -> or{AC,#}(x3,x4)
  DPs:
   not#(eqC(x,y)) -> neq{C,#}(x,y)
   not#(neqC(x,y)) -> eq{C,#}(x,y)
   not#(andAC(x,y)) -> not#(y)
   not#(andAC(x,y)) -> not#(x)
   not#(andAC(x,y)) -> or{AC,#}(not(x),not(y))
   not#(orAC(x,y)) -> not#(y)
   not#(orAC(x,y)) -> not#(x)
   not#(orAC(x,y)) -> and{AC,#}(not(x),not(y))
   or{AC,#}(andAC(x,y),z) -> or{AC,#}(y,z)
   or{AC,#}(andAC(x,y),z) -> or{AC,#}(x,z)
   or{AC,#}(andAC(x,y),z) -> and{AC,#}(orAC(x,z),orAC(y,z))
   or{AC,#}(x6,orAC(andAC(x,y),z)) -> or{AC,#}(y,z)
   or{AC,#}(x6,orAC(andAC(x,y),z)) -> or{AC,#}(x,z)
   or{AC,#}(x6,orAC(andAC(x,y),z)) -> and{AC,#}(orAC(x,z),orAC(y,z))
   or{AC,#}(x6,orAC(andAC(x,y),z)) -> or{AC,#}(x6,andAC(orAC(x,z),orAC(y,z)))
   or{AC,#}(x7,orAC(x,x)) -> or{AC,#}(x7,x)
   or{AC,#}(x8,orAC(x,true())) -> or{AC,#}(x8,true())
   or{AC,#}(x9,orAC(x,false())) -> or{AC,#}(x9,x)
   and{AC,#}(x10,andAC(x,x)) -> and{AC,#}(x10,x)
   and{AC,#}(x11,andAC(x,true())) -> and{AC,#}(x11,x)
   and{AC,#}(x12,andAC(x,false())) -> and{AC,#}(x12,false())
   and{AC,#}(x13,andAC(x,orAC(x,y))) -> and{AC,#}(x13,x)
  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
  S:
   and{AC,#}(andAC(x14,x15),x16) -> and{AC,#}(x14,x15)
   and{AC,#}(x14,andAC(x15,x16)) -> and{AC,#}(x15,x16)
   or{AC,#}(orAC(x14,x15),x16) -> or{AC,#}(x14,x15)
   or{AC,#}(x14,orAC(x15,x16)) -> or{AC,#}(x15,x16)
  AC-EDG Processor:
   Equations#:
    and{AC,#}(andAC(x3,x4),x5) -> and{AC,#}(x3,andAC(x4,x5))
    and{AC,#}(x3,x4) -> and{AC,#}(x4,x3)
    or{AC,#}(orAC(x3,x4),x5) -> or{AC,#}(x3,orAC(x4,x5))
    or{AC,#}(x3,x4) -> or{AC,#}(x4,x3)
    and{AC,#}(x3,andAC(x4,x5)) -> and{AC,#}(andAC(x3,x4),x5)
    and{AC,#}(x4,x3) -> and{AC,#}(x3,x4)
    or{AC,#}(x3,orAC(x4,x5)) -> or{AC,#}(orAC(x3,x4),x5)
    or{AC,#}(x4,x3) -> or{AC,#}(x3,x4)
   DPs:
    not#(eqC(x,y)) -> neq{C,#}(x,y)
    not#(neqC(x,y)) -> eq{C,#}(x,y)
    not#(andAC(x,y)) -> not#(y)
    not#(andAC(x,y)) -> not#(x)
    not#(andAC(x,y)) -> or{AC,#}(not(x),not(y))
    not#(orAC(x,y)) -> not#(y)
    not#(orAC(x,y)) -> not#(x)
    not#(orAC(x,y)) -> and{AC,#}(not(x),not(y))
    or{AC,#}(andAC(x,y),z) -> or{AC,#}(y,z)
    or{AC,#}(andAC(x,y),z) -> or{AC,#}(x,z)
    or{AC,#}(andAC(x,y),z) -> and{AC,#}(orAC(x,z),orAC(y,z))
    or{AC,#}(x6,orAC(andAC(x,y),z)) -> or{AC,#}(y,z)
    or{AC,#}(x6,orAC(andAC(x,y),z)) -> or{AC,#}(x,z)
    or{AC,#}(x6,orAC(andAC(x,y),z)) -> and{AC,#}(orAC(x,z),orAC(y,z))
    or{AC,#}(x6,orAC(andAC(x,y),z)) -> or{AC,#}(x6,andAC(orAC(x,z),orAC(y,z)))
    or{AC,#}(x7,orAC(x,x)) -> or{AC,#}(x7,x)
    or{AC,#}(x8,orAC(x,true())) -> or{AC,#}(x8,true())
    or{AC,#}(x9,orAC(x,false())) -> or{AC,#}(x9,x)
    and{AC,#}(x10,andAC(x,x)) -> and{AC,#}(x10,x)
    and{AC,#}(x11,andAC(x,true())) -> and{AC,#}(x11,x)
    and{AC,#}(x12,andAC(x,false())) -> and{AC,#}(x12,false())
    and{AC,#}(x13,andAC(x,orAC(x,y))) -> and{AC,#}(x13,x)
   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
   S:
    and{AC,#}(andAC(x14,x15),x16) -> and{AC,#}(x14,x15)
    and{AC,#}(x14,andAC(x15,x16)) -> and{AC,#}(x15,x16)
    or{AC,#}(orAC(x14,x15),x16) -> or{AC,#}(x14,x15)
    or{AC,#}(x14,orAC(x15,x16)) -> or{AC,#}(x15,x16)
   Open