YES
Time: 0.357

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(x,one()) -> x
  fAC(i(x),x) -> one()
  phi(one(),y1) -> y1
  phi(y1,phi(y2,x)) -> phi(fAC(y1,y2),x)

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
                   [9 2]     [1 2]     [2]
   [phi](x0, x1) = [5 5]x0 + [1 1]x1 + [3],
   
             [2 0]     [8 ]
   [i](x0) = [0 0]x0 + [12],
   
           [3]
   [one] = [1],
   
                             [0]
   [fAC](x0, x1) = x0 + x1 + [1]
  orientation:
                      [3]         
   fAC(x,one()) = x + [2] >= x = x
   
                 [3 0]    [8 ]    [3]        
   fAC(i(x),x) = [0 1]x + [13] >= [1] = one()
   
                   [1 2]     [31]           
   phi(one(),y1) = [1 1]y1 + [23] >= y1 = y1
   
                       [3 4]    [9 2]     [19 12]     [10]    [1 2]    [9 2]     [9 2]     [4]                    
   phi(y1,phi(y2,x)) = [2 3]x + [5 5]y1 + [14 7 ]y2 + [8 ] >= [1 1]x + [5 5]y1 + [5 5]y2 + [8] = phi(fAC(y1,y2),x)
  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