YES
Time: 1.233

Problem:
 Equations:
  fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
  fAC(x2,x3) -> fAC(x3,x2)
  fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
  fAC(x3,x2) -> fAC(x2,x3)
 TRS:
  fAC(g(fAC(h(a()),a())),a()) -> fAC(h(a()),fAC(a(),a()))
  fAC(h(a()),g(a())) -> fAC(g(h(a())),a())
  fAC(g(h(a())),fAC(fAC(a(),a()),a())) -> fAC(g(fAC(h(a()),a())),a())
  fAC(h(a()),a()) -> fAC(h(a()),b())
  fAC(i(x,y),fAC(a(),y)) -> fAC(g(i(x,y)),y)

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
                 [1 0]     [8 4]     [8]
   [i](x0, x1) = [0 0]x0 + [0 0]x1 + [0],
   
         [0]
   [b] = [0],
   
             [1 4]  
   [g](x0) = [0 1]x0,
   
             [1 0]  
   [h](x0) = [0 0]x0,
   
         [4]
   [a] = [1],
   
                             [1]
   [fAC](x0, x1) = x0 + x1 + [0]
  orientation:
                                 [18]    [14]                           
   fAC(g(fAC(h(a()),a())),a()) = [2 ] >= [2 ] = fAC(h(a()),fAC(a(),a()))
   
                        [13]    [9]                     
   fAC(h(a()),g(a())) = [1 ] >= [1] = fAC(g(h(a())),a())
   
                                          [19]    [18]                              
   fAC(g(h(a())),fAC(fAC(a(),a()),a())) = [3 ] >= [2 ] = fAC(g(fAC(h(a()),a())),a())
   
                     [9]    [5]                  
   fAC(h(a()),a()) = [1] >= [0] = fAC(h(a()),b())
   
                            [1 0]    [9 4]    [14]    [1 0]    [9 4]    [9]                   
   fAC(i(x,y),fAC(a(),y)) = [0 0]x + [0 1]y + [1 ] >= [0 0]x + [0 1]y + [0] = fAC(g(i(x,y)),y)
  problem:
   Equations:
    fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
    fAC(x2,x3) -> fAC(x3,x2)
    fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
    fAC(x3,x2) -> fAC(x2,x3)
   TRS:
    
  Qed