MAYBE
Time: 0.030

Problem:
 Equations:
  fAC(fAC(x5,x6),x7) -> fAC(x5,fAC(x6,x7))
  fAC(x5,x6) -> fAC(x6,x5)
  fAC(x5,fAC(x6,x7)) -> fAC(fAC(x5,x6),x7)
  fAC(x6,x5) -> fAC(x5,x6)
 TRS:
  fAC(h(x1),fAC(h(a()),g(a()))) -> h(x1)
  fAC(g(x1),fAC(h(a()),g(a()))) -> g(x1)
  fAC(a(),x1) -> fAC(h(x1),h(a()))
  fAC(a(),x1) -> fAC(g(x1),g(a()))
  fAC(g(x2),h(x1)) -> fAC(g(x1),h(x2))

Proof:
 Open