YES
Time: 0.097

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:
  fAC(i(x),fAC(x,y)) -> y

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
             [1 0]     [8]
   [i](x0) = [0 0]x0 + [0],
   
                          
   [fAC](x0, x1) = x0 + x1
  orientation:
                        [2 0]        [8]         
   fAC(i(x),fAC(x,y)) = [0 1]x + y + [0] >= y = y
  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