YES
Time: 0.051

Problem:
 Equations:
  fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
  fAC(x2,x3) -> fAC(x3,x2)
  fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
  fAC(x3,x2) -> fAC(x2,x3)
 TRS:
  fAC(x,one()) -> x
  fAC(i(x),x) -> one()
  g(one()) -> one()
  g(fAC(x,y)) -> fAC(g(x),g(y))

Proof:
 Matrix Interpretation Processor:
  dimension: 1
  interpretation:
   [g](x0) = 3x0,
   
   [i](x0) = x0 + 13,
   
   [one] = 10,
   
   [fAC](x0, x1) = x0 + x1 + 1
  orientation:
   fAC(x,one()) = x + 11 >= x = x
   
   fAC(i(x),x) = 2x + 14 >= 10 = one()
   
   g(one()) = 30 >= 10 = one()
   
   g(fAC(x,y)) = 3x + 3y + 3 >= 3x + 3y + 1 = fAC(g(x),g(y))
  problem:
   Equations:
    fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
    fAC(x2,x3) -> fAC(x3,x2)
    fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
    fAC(x3,x2) -> fAC(x2,x3)
   TRS:
    
  Qed