YES
Time: 0.044

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-RPO Processor:
  precedence:
   *AC > +AC > f > c > b > a
  status:
   
  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