YES
Time: 0.464

Problem:
 Equations:
  fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
  fAC(x3,x4) -> fAC(x4,x3)
  fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
  fAC(x4,x3) -> fAC(x3,x4)
 TRS:
  g(fAC(x,y)) -> fAC(g(x),g(y))
  fAC(a(),g(g(a()))) -> fAC(g(a()),g(a()))

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
         [3]
   [a] = [2],
   
             [2 1]     [0]
   [g](x0) = [2 0]x0 + [4],
   
                             [2]
   [fAC](x0, x1) = x0 + x1 + [0]
  orientation:
                 [2 1]    [2 1]    [4]    [2 1]    [2 1]    [2]                 
   g(fAC(x,y)) = [2 0]x + [2 0]y + [8] >= [2 0]x + [2 0]y + [8] = fAC(g(x),g(y))
   
                        [31]    [18]                     
   fAC(a(),g(g(a()))) = [22] >= [20] = fAC(g(a()),g(a()))
  problem:
   Equations:
    fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
    fAC(x3,x4) -> fAC(x4,x3)
    fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
    fAC(x4,x3) -> fAC(x3,x4)
   TRS:
    
  Qed