YES
Time: 0.303

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: 2
  interpretation:
             [1 4]     [0]
   [g](x0) = [1 2]x0 + [4],
   
             [1 0]     [6]
   [i](x0) = [0 0]x0 + [8],
   
           [4]
   [one] = [3],
   
                             [0]
   [fAC](x0, x1) = x0 + x1 + [4]
  orientation:
                      [4]         
   fAC(x,one()) = x + [7] >= x = x
   
                 [2 0]    [6 ]    [4]        
   fAC(i(x),x) = [0 1]x + [12] >= [3] = one()
   
              [16]    [4]        
   g(one()) = [14] >= [3] = one()
   
                 [1 4]    [1 4]    [16]    [1 4]    [1 4]    [0 ]                 
   g(fAC(x,y)) = [1 2]x + [1 2]y + [12] >= [1 2]x + [1 2]y + [12] = 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