YES
Time: 0.282

Problem:
 Equations:
  plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
  plusAC(x2,x3) -> plusAC(x3,x2)
  plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
  plusAC(x3,x2) -> plusAC(x2,x3)
 TRS:
  f(plusAC(x,y)) -> plusAC(f(x),f(y))
  plusAC(x,0()) -> 0()
  f(0()) -> 0()

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
         [0]
   [0] = [6],
   
             [2 4]     [2]
   [f](x0) = [0 4]x0 + [4],
   
                                [4]
   [plusAC](x0, x1) = x0 + x1 + [2]
  orientation:
                    [2 4]    [2 4]    [18]    [2 4]    [2 4]    [8 ]                    
   f(plusAC(x,y)) = [0 4]x + [0 4]y + [12] >= [0 4]x + [0 4]y + [10] = plusAC(f(x),f(y))
   
                       [4]    [0]      
   plusAC(x,0()) = x + [8] >= [6] = 0()
   
            [26]    [0]      
   f(0()) = [28] >= [6] = 0()
  problem:
   Equations:
    plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
    plusAC(x2,x3) -> plusAC(x3,x2)
    plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
    plusAC(x3,x2) -> plusAC(x2,x3)
   TRS:
    
  Qed