MAYBE
Time: 0.011

Problem:
 Equations:
  +AC(+AC(x2,x3),x4) -> +AC(x2,+AC(x3,x4))
  +AC(x2,x3) -> +AC(x3,x2)
  +AC(x2,+AC(x3,x4)) -> +AC(+AC(x2,x3),x4)
  +AC(x3,x2) -> +AC(x2,x3)
 TRS:
  +AC(g(x),g(y)) -> g(+AC(g(a()),+AC(x,y)))

Proof:
 Open