MAYBE
Time: 0.009

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))
  fAC(x,u3(y)) -> u3(fAC(x,y))
  u1(g(x,y)) -> g(u1(x),u1(y))
  u2(g(x,y)) -> g(u2(x),u2(y))
  u3(g(x,y)) -> g(u3(x),u3(y))
  u2(u1(x)) -> u1(u2(x))
  u3(u1(x)) -> u1(u3(x))
  u3(u2(x)) -> u2(u3(x))

Proof:
 Open