YES
Time: 1.293

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

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