MAYBE
Time: 0.171

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)
  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)
 TRS:
  or(x,y) -> xorAC(x,xorAC(y,andAC(x,y)))
  not(x) -> xorAC(x,1())
  xorAC(x,x) -> 0()
  xorAC(0(),x) -> x
  andAC(xorAC(x,y),z) -> xorAC(andAC(x,z),andAC(y,z))
  andAC(x,x) -> 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)
   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)
  DPs:
   or#(x,y) -> and{AC,#}(x,y)
   or#(x,y) -> xor{AC,#}(y,andAC(x,y))
   or#(x,y) -> xor{AC,#}(x,xorAC(y,andAC(x,y)))
   not#(x) -> xor{AC,#}(x,1())
   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))
   xor{AC,#}(x6,xorAC(x,x)) -> xor{AC,#}(x6,0())
   xor{AC,#}(x7,xorAC(0(),x)) -> xor{AC,#}(x7,x)
   and{AC,#}(x8,andAC(xorAC(x,y),z)) -> and{AC,#}(y,z)
   and{AC,#}(x8,andAC(xorAC(x,y),z)) -> and{AC,#}(x,z)
   and{AC,#}(x8,andAC(xorAC(x,y),z)) -> xor{AC,#}(andAC(x,z),andAC(y,z))
   and{AC,#}(x8,andAC(xorAC(x,y),z)) -> and{AC,#}(x8,xorAC(andAC(x,z),andAC(y,z)))
   and{AC,#}(x9,andAC(x,x)) -> and{AC,#}(x9,x)
  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)
   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)
  TRS:
   or(x,y) -> xorAC(x,xorAC(y,andAC(x,y)))
   not(x) -> xorAC(x,1())
   xorAC(x,x) -> 0()
   xorAC(0(),x) -> x
   andAC(xorAC(x,y),z) -> xorAC(andAC(x,z),andAC(y,z))
   andAC(x,x) -> x
  S:
   xor{AC,#}(xorAC(x10,x11),x12) -> xor{AC,#}(x10,x11)
   xor{AC,#}(x10,xorAC(x11,x12)) -> xor{AC,#}(x11,x12)
   and{AC,#}(andAC(x10,x11),x12) -> and{AC,#}(x10,x11)
   and{AC,#}(x10,andAC(x11,x12)) -> and{AC,#}(x11,x12)
  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)
    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)
   DPs:
    or#(x,y) -> and{AC,#}(x,y)
    or#(x,y) -> xor{AC,#}(y,andAC(x,y))
    or#(x,y) -> xor{AC,#}(x,xorAC(y,andAC(x,y)))
    not#(x) -> xor{AC,#}(x,1())
    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))
    xor{AC,#}(x6,xorAC(x,x)) -> xor{AC,#}(x6,0())
    xor{AC,#}(x7,xorAC(0(),x)) -> xor{AC,#}(x7,x)
    and{AC,#}(x8,andAC(xorAC(x,y),z)) -> and{AC,#}(y,z)
    and{AC,#}(x8,andAC(xorAC(x,y),z)) -> and{AC,#}(x,z)
    and{AC,#}(x8,andAC(xorAC(x,y),z)) -> xor{AC,#}(andAC(x,z),andAC(y,z))
    and{AC,#}(x8,andAC(xorAC(x,y),z)) -> and{AC,#}(x8,xorAC(andAC(x,z),andAC(y,z)))
    and{AC,#}(x9,andAC(x,x)) -> and{AC,#}(x9,x)
   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)
    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)
   TRS:
    or(x,y) -> xorAC(x,xorAC(y,andAC(x,y)))
    not(x) -> xorAC(x,1())
    xorAC(x,x) -> 0()
    xorAC(0(),x) -> x
    andAC(xorAC(x,y),z) -> xorAC(andAC(x,z),andAC(y,z))
    andAC(x,x) -> x
   S:
    xor{AC,#}(xorAC(x10,x11),x12) -> xor{AC,#}(x10,x11)
    xor{AC,#}(x10,xorAC(x11,x12)) -> xor{AC,#}(x11,x12)
    and{AC,#}(andAC(x10,x11),x12) -> and{AC,#}(x10,x11)
    and{AC,#}(x10,andAC(x11,x12)) -> and{AC,#}(x11,x12)
   Open