YES
Time: 0.646

Problem:
 Equations:
  fAC(fAC(x0,x1),x2) -> fAC(x0,fAC(x1,x2))
  fAC(x0,x1) -> fAC(x1,x0)
  fAC(x0,fAC(x1,x2)) -> fAC(fAC(x0,x1),x2)
  fAC(x1,x0) -> fAC(x0,x1)
 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(b(),fAC(b(),b()))) -> fAC(g(fAC(h(a()),a())),a())
  fAC(h(a()),a()) -> fAC(h(a()),b())

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
         [7]
   [b] = [1],
   
             [1 1]     [0]
   [g](x0) = [0 2]x0 + [5],
   
             [1 1]  
   [h](x0) = [0 0]x0,
   
         [8]
   [a] = [1],
   
                             [0]
   [fAC](x0, x1) = x0 + x1 + [1]
  orientation:
                                 [27]    [25]                           
   fAC(g(fAC(h(a()),a())),a()) = [11] >= [4 ] = fAC(h(a()),fAC(a(),a()))
   
                        [18]    [17]                     
   fAC(h(a()),g(a())) = [8 ] >= [7 ] = fAC(g(h(a())),a())
   
                                          [30]    [27]                              
   fAC(g(h(a())),fAC(b(),fAC(b(),b()))) = [11] >= [11] = fAC(g(fAC(h(a()),a())),a())
   
                     [17]    [16]                  
   fAC(h(a()),a()) = [2 ] >= [2 ] = fAC(h(a()),b())
  problem:
   Equations:
    fAC(fAC(x0,x1),x2) -> fAC(x0,fAC(x1,x2))
    fAC(x0,x1) -> fAC(x1,x0)
    fAC(x0,fAC(x1,x2)) -> fAC(fAC(x0,x1),x2)
    fAC(x1,x0) -> fAC(x0,x1)
   TRS:
    
  Qed