YES
Time: 0.028

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:
  andAC(x,0()) -> 0()
  andAC(x,1()) -> x
  andAC(x,x) -> x
  orAC(x,0()) -> x
  orAC(x,1()) -> 1()
  orAC(x,x) -> x

Proof:
 Matrix Interpretation Processor:
  dimension: 1
  interpretation:
   [1] = 0,
   
   [0] = 0,
   
   [orAC](x0, x1) = x0 + x1 + 8,
   
   [andAC](x0, x1) = x0 + x1 + 1
  orientation:
   andAC(x,0()) = x + 1 >= 0 = 0()
   
   andAC(x,1()) = x + 1 >= x = x
   
   andAC(x,x) = 2x + 1 >= x = x
   
   orAC(x,0()) = x + 8 >= x = x
   
   orAC(x,1()) = x + 8 >= 0 = 1()
   
   orAC(x,x) = 2x + 8 >= x = x
  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:
    
  Qed