YES
Time: 0.024

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:
 AC-KBO Processor:
  precedence:
   f > a > b > c ~ *AC ~ +AC
   weight function:
    w0 = 2
    w(c) = w(b) = 3
    w(a) = 2
    w(f) = w(*AC) = w(+AC) = 0
   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:
     
   Qed