YES
Time: 1.281

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:
  plusAC(x,0()) -> x
  plusAC(x,x) -> x
  plusAC(T(x),x) -> T(x)
  plusAC(T(plusAC(x,y)),x) -> T(plusAC(x,y))
  L(T(x)) -> L(x)
  L(plusAC(T(y),x)) -> plusAC(L(plusAC(x,y)),L(y))
  T(T(x)) -> T(x)
  T(plusAC(T(y),x)) -> plusAC(T(plusAC(x,y)),T(y))

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
             [4  2 ]     [0 ]
   [L](x0) = [3  12]x0 + [12],
   
             [1 4]     [0]
   [T](x0) = [2 1]x0 + [1],
   
         [11]
   [0] = [0 ],
   
                                [1]
   [plusAC](x0, x1) = x0 + x1 + [0]
  orientation:
                       [12]         
   plusAC(x,0()) = x + [0 ] >= x = x
   
                 [2 0]    [1]         
   plusAC(x,x) = [0 2]x + [0] >= x = x
   
                    [2 4]    [1]    [1 4]    [0]       
   plusAC(T(x),x) = [2 2]x + [1] >= [2 1]x + [1] = T(x)
   
                              [2 4]    [1 4]    [2]    [1 4]    [1 4]    [1]                 
   plusAC(T(plusAC(x,y)),x) = [2 2]x + [2 1]y + [3] >= [2 1]x + [2 1]y + [3] = T(plusAC(x,y))
   
             [8  18]    [2 ]    [4  2 ]    [0 ]       
   L(T(x)) = [27 24]x + [24] >= [3  12]x + [12] = L(x)
   
                       [4  2 ]    [8  18]    [6 ]    [4  2 ]    [8  4 ]    [5 ]                              
   L(plusAC(T(y),x)) = [3  12]x + [27 24]y + [27] >= [3  12]x + [6  24]y + [27] = plusAC(L(plusAC(x,y)),L(y))
   
             [9 8]    [4]    [1 4]    [0]       
   T(T(x)) = [4 9]x + [2] >= [2 1]x + [1] = T(x)
   
                       [1 4]    [9 8]    [5]    [1 4]    [2 8]    [2]                              
   T(plusAC(T(y),x)) = [2 1]x + [4 9]y + [4] >= [2 1]x + [4 2]y + [4] = plusAC(T(plusAC(x,y)),T(y))
  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