YES
Time: 0.091

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: 1
  interpretation:
   [s](x0) = 14x0 + 13,
   
   [g](x0, x1) = 2x0 + 2x1 + 4,
   
   [0] = 1,
   
   [fAC](x0, x1) = x0 + x1 + 8
  orientation:
   g(0(),fAC(x,x)) = 4x + 22 >= x = x
   
   g(x,s(y)) = 2x + 28y + 30 >= 2x + 2y + 22 = g(fAC(x,y),0())
   
   g(s(x),y) = 28x + 2y + 30 >= 2x + 2y + 22 = g(fAC(x,y),0())
   
   g(fAC(x,y),0()) = 2x + 2y + 22 >= 2x + 2y + 20 = 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