MAYBE
Time: 0.421

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:
 DP Processor:
  Equations#:
   xor{AC,#}(xorAC(x3,x4),x5) -> xor{AC,#}(x3,xorAC(x4,x5))
   xor{AC,#}(x3,x4) -> xor{AC,#}(x4,x3)
   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)
   xor{AC,#}(x3,xorAC(x4,x5)) -> xor{AC,#}(xorAC(x3,x4),x5)
   xor{AC,#}(x4,x3) -> xor{AC,#}(x3,x4)
   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:
   and{AC,#}(xorAC(x,y),z) -> and{AC,#}(y,z)
   and{AC,#}(xorAC(x,y),z) -> and{AC,#}(x,z)
   and{AC,#}(xorAC(x,y),z) -> xor{AC,#}(andAC(x,z),andAC(y,z))
   impl#(x,y) -> xor{AC,#}(T(),x)
   impl#(x,y) -> and{AC,#}(x,y)
   impl#(x,y) -> xor{AC,#}(andAC(x,y),xorAC(T(),x))
   or{AC,#}(x,y) -> xor{AC,#}(x,y)
   or{AC,#}(x,y) -> and{AC,#}(x,y)
   or{AC,#}(x,y) -> xor{AC,#}(andAC(x,y),xorAC(x,y))
   equiv#(x,y) -> xor{AC,#}(T(),y)
   equiv#(x,y) -> xor{AC,#}(xorAC(T(),y),x)
   neg#(x) -> xor{AC,#}(T(),x)
   xor{AC,#}(x6,xorAC(F(),x)) -> xor{AC,#}(x6,x)
   xor{AC,#}(x7,xorAC(neg(x),x)) -> xor{AC,#}(x7,F())
   and{AC,#}(x8,andAC(T(),x)) -> and{AC,#}(x8,x)
   and{AC,#}(x9,andAC(F(),x)) -> and{AC,#}(x9,F())
   and{AC,#}(x10,andAC(x,x)) -> and{AC,#}(x10,x)
   and{AC,#}(x11,andAC(xorAC(x,y),z)) -> and{AC,#}(y,z)
   and{AC,#}(x11,andAC(xorAC(x,y),z)) -> and{AC,#}(x,z)
   and{AC,#}(x11,andAC(xorAC(x,y),z)) -> xor{AC,#}(andAC(x,z),andAC(y,z))
   and{AC,#}(x11,andAC(xorAC(x,y),z)) -> and{AC,#}(x11,xorAC(andAC(x,z),andAC(y,z)))
   xor{AC,#}(x12,xorAC(x,x)) -> xor{AC,#}(x12,F())
   or{AC,#}(x13,orAC(x,y)) -> xor{AC,#}(x,y)
   or{AC,#}(x13,orAC(x,y)) -> and{AC,#}(x,y)
   or{AC,#}(x13,orAC(x,y)) -> xor{AC,#}(andAC(x,y),xorAC(x,y))
   or{AC,#}(x13,orAC(x,y)) -> or{AC,#}(x13,xorAC(andAC(x,y),xorAC(x,y)))
  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)
  S:
   xor{AC,#}(xorAC(x14,x15),x16) -> xor{AC,#}(x14,x15)
   xor{AC,#}(x14,xorAC(x15,x16)) -> xor{AC,#}(x15,x16)
   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#:
    xor{AC,#}(xorAC(x3,x4),x5) -> xor{AC,#}(x3,xorAC(x4,x5))
    xor{AC,#}(x3,x4) -> xor{AC,#}(x4,x3)
    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)
    xor{AC,#}(x3,xorAC(x4,x5)) -> xor{AC,#}(xorAC(x3,x4),x5)
    xor{AC,#}(x4,x3) -> xor{AC,#}(x3,x4)
    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:
    and{AC,#}(xorAC(x,y),z) -> and{AC,#}(y,z)
    and{AC,#}(xorAC(x,y),z) -> and{AC,#}(x,z)
    and{AC,#}(xorAC(x,y),z) -> xor{AC,#}(andAC(x,z),andAC(y,z))
    impl#(x,y) -> xor{AC,#}(T(),x)
    impl#(x,y) -> and{AC,#}(x,y)
    impl#(x,y) -> xor{AC,#}(andAC(x,y),xorAC(T(),x))
    or{AC,#}(x,y) -> xor{AC,#}(x,y)
    or{AC,#}(x,y) -> and{AC,#}(x,y)
    or{AC,#}(x,y) -> xor{AC,#}(andAC(x,y),xorAC(x,y))
    equiv#(x,y) -> xor{AC,#}(T(),y)
    equiv#(x,y) -> xor{AC,#}(xorAC(T(),y),x)
    neg#(x) -> xor{AC,#}(T(),x)
    xor{AC,#}(x6,xorAC(F(),x)) -> xor{AC,#}(x6,x)
    xor{AC,#}(x7,xorAC(neg(x),x)) -> xor{AC,#}(x7,F())
    and{AC,#}(x8,andAC(T(),x)) -> and{AC,#}(x8,x)
    and{AC,#}(x9,andAC(F(),x)) -> and{AC,#}(x9,F())
    and{AC,#}(x10,andAC(x,x)) -> and{AC,#}(x10,x)
    and{AC,#}(x11,andAC(xorAC(x,y),z)) -> and{AC,#}(y,z)
    and{AC,#}(x11,andAC(xorAC(x,y),z)) -> and{AC,#}(x,z)
    and{AC,#}(x11,andAC(xorAC(x,y),z)) -> xor{AC,#}(andAC(x,z),andAC(y,z))
    and{AC,#}(x11,andAC(xorAC(x,y),z)) -> and{AC,#}(x11,xorAC(andAC(x,z),andAC(y,z)))
    xor{AC,#}(x12,xorAC(x,x)) -> xor{AC,#}(x12,F())
    or{AC,#}(x13,orAC(x,y)) -> xor{AC,#}(x,y)
    or{AC,#}(x13,orAC(x,y)) -> and{AC,#}(x,y)
    or{AC,#}(x13,orAC(x,y)) -> xor{AC,#}(andAC(x,y),xorAC(x,y))
    or{AC,#}(x13,orAC(x,y)) -> or{AC,#}(x13,xorAC(andAC(x,y),xorAC(x,y)))
   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)
   S:
    xor{AC,#}(xorAC(x14,x15),x16) -> xor{AC,#}(x14,x15)
    xor{AC,#}(x14,xorAC(x15,x16)) -> xor{AC,#}(x15,x16)
    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