YES
Time: 0.640

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(0(),fAC(x,x)) -> x
  g(x,s(y)) -> g(fAC(x,y),0())
  g(s(x),y) -> g(fAC(x,y),0())
  g(fAC(x,y),0()) -> fAC(g(x,0()),g(y,0()))

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
             [2 0]     [3 ]
   [s](x0) = [1 0]x0 + [11],
   
                 [4 0]     [5 1]     [0]
   [g](x0, x1) = [1 0]x0 + [2 1]x1 + [1],
   
         [0]
   [0] = [0],
   
                             [2]
   [fAC](x0, x1) = x0 + x1 + [0]
  orientation:
                     [10 2 ]    [10]         
   g(0(),fAC(x,x)) = [4  2 ]x + [5 ] >= x = x
   
               [4 0]    [11 0 ]    [26]    [4 0]    [4 0]    [8]                  
   g(x,s(y)) = [1 0]x + [5  0 ]y + [18] >= [1 0]x + [1 0]y + [3] = g(fAC(x,y),0())
   
               [8 0]    [5 1]    [12]    [4 0]    [4 0]    [8]                  
   g(s(x),y) = [2 0]x + [2 1]y + [4 ] >= [1 0]x + [1 0]y + [3] = g(fAC(x,y),0())
   
                     [4 0]    [4 0]    [8]    [4 0]    [4 0]    [2]                         
   g(fAC(x,y),0()) = [1 0]x + [1 0]y + [3] >= [1 0]x + [1 0]y + [2] = fAC(g(x,0()),g(y,0()))
  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