YES
Time: 0.017

Problem:
 Equations:
  
 TRS:
  fAC(x,g(y,z)) -> g(fAC(x,y),fAC(x,z))
  fAC(x,u1(y)) -> u1(fAC(x,y))
  fAC(x,u2(y)) -> u2(fAC(x,y))
  u1(g(x,y)) -> g(u1(x),u1(y))
  u2(g(x,y)) -> g(u2(x),u2(y))
  u2(u1(x)) -> u1(u2(x))

Proof:
 AC-RPO Processor:
  precedence:
   fAC > u2 > u1 > g
  status:
   g:mul  
  problem:
   Equations:
    
   TRS:
    
  Qed