YES
Time: 0.466

Problem:
 Equations:
  fAC(fAC(x1,x2),x3) -> fAC(x1,fAC(x2,x3))
  fAC(x1,x2) -> fAC(x2,x1)
  fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3)
  fAC(x2,x1) -> fAC(x1,x2)
 TRS:
  fAC(g(g(x)),x) -> fAC(g(x),g(x))
  fAC(fAC(x,x),g(x)) -> fAC(x,h(x))

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
             [2 3]     [2]
   [h](x0) = [4 0]x0 + [4],
   
             [4 3]     [2]
   [g](x0) = [4 0]x0 + [3],
   
                             [5 ]
   [fAC](x0, x1) = x0 + x1 + [12]
  orientation:
                    [29 12]    [24]    [8 6]    [9 ]                 
   fAC(g(g(x)),x) = [16 13]x + [23] >= [8 0]x + [18] = fAC(g(x),g(x))
   
                        [6 3]    [12]    [3 3]    [7 ]              
   fAC(fAC(x,x),g(x)) = [4 2]x + [27] >= [4 1]x + [16] = fAC(x,h(x))
  problem:
   Equations:
    fAC(fAC(x1,x2),x3) -> fAC(x1,fAC(x2,x3))
    fAC(x1,x2) -> fAC(x2,x1)
    fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3)
    fAC(x2,x1) -> fAC(x1,x2)
   TRS:
    
  Qed