MAYBE
Time: 4.644

Problem:
 Equations:
  +AC(+AC(x0,x1),x2) -> +AC(x0,+AC(x1,x2))
  +AC(x0,x1) -> +AC(x1,x0)
  *AC(*AC(x0,x1),x2) -> *AC(x0,*AC(x1,x2))
  *AC(x0,x1) -> *AC(x1,x0)
  +AC(x0,+AC(x1,x2)) -> +AC(+AC(x0,x1),x2)
  +AC(x1,x0) -> +AC(x0,x1)
  *AC(x0,*AC(x1,x2)) -> *AC(*AC(x0,x1),x2)
  *AC(x1,x0) -> *AC(x0,x1)
 TRS:
  +AC(a(),*AC(b(),c())) -> +AC(b(),f(*AC(a(),c())))
  *AC(a(),+AC(b(),c())) -> *AC(b(),f(+AC(a(),c())))

Proof:
 Open