YES
Time: 0.346

Problem:
 Equations:
  orAC(orAC(x2,x3),x4) -> orAC(x2,orAC(x3,x4))
  orAC(x2,x3) -> orAC(x3,x2)
  andAC(andAC(x2,x3),x4) -> andAC(x2,andAC(x3,x4))
  andAC(x2,x3) -> andAC(x3,x2)
  orAC(x2,orAC(x3,x4)) -> orAC(orAC(x2,x3),x4)
  orAC(x3,x2) -> orAC(x2,x3)
  andAC(x2,andAC(x3,x4)) -> andAC(andAC(x2,x3),x4)
  andAC(x3,x2) -> andAC(x2,x3)
 TRS:
  not(not(x)) -> x
  orAC(not(x),not(y)) -> not(andAC(x,y))

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
               [4 4]     [0]
   [not](x0) = [1 0]x0 + [4],
   
                            
   [andAC](x0, x1) = x0 + x1,
   
                              [8]
   [orAC](x0, x1) = x0 + x1 + [2]
  orientation:
                 [20 16]    [16]         
   not(not(x)) = [4  4 ]x + [4 ] >= x = x
   
                         [4 4]    [4 4]    [8 ]    [4 4]    [4 4]    [0]                  
   orAC(not(x),not(y)) = [1 0]x + [1 0]y + [10] >= [1 0]x + [1 0]y + [4] = not(andAC(x,y))
  problem:
   Equations:
    orAC(orAC(x2,x3),x4) -> orAC(x2,orAC(x3,x4))
    orAC(x2,x3) -> orAC(x3,x2)
    andAC(andAC(x2,x3),x4) -> andAC(x2,andAC(x3,x4))
    andAC(x2,x3) -> andAC(x3,x2)
    orAC(x2,orAC(x3,x4)) -> orAC(orAC(x2,x3),x4)
    orAC(x3,x2) -> orAC(x2,x3)
    andAC(x2,andAC(x3,x4)) -> andAC(andAC(x2,x3),x4)
    andAC(x3,x2) -> andAC(x2,x3)
   TRS:
    
  Qed