YES
Time: 0.048

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: 1
  interpretation:
   [0] = 0,
   
   [f](x0) = 9x0 + 13,
   
   [plusAC](x0, x1) = x0 + x1 + 2
  orientation:
   f(plusAC(x,y)) = 9x + 9y + 31 >= 9x + 9y + 28 = plusAC(f(x),f(y))
   
   plusAC(x,0()) = x + 2 >= 0 = 0()
   
   f(0()) = 13 >= 0 = 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