YES
Time: 0.105

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: 2
  interpretation:
         [12]
   [1] = [7 ],
   
         [8]
   [0] = [0],
   
                              [8]
   [orAC](x0, x1) = x0 + x1 + [1],
   
                               [3]
   [andAC](x0, x1) = x0 + x1 + [4]
  orientation:
                      [11]    [8]      
   andAC(x,0()) = x + [4 ] >= [0] = 0()
   
                      [15]         
   andAC(x,1()) = x + [11] >= x = x
   
                [2 0]    [3]         
   andAC(x,x) = [0 2]x + [4] >= x = x
   
                     [16]         
   orAC(x,0()) = x + [1 ] >= x = x
   
                     [20]    [12]      
   orAC(x,1()) = x + [8 ] >= [7 ] = 1()
   
               [2 0]    [8]         
   orAC(x,x) = [0 2]x + [1] >= 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