YES
Time: 0.042

Problem:
 Equations:
  
 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:
    
   TRS:
    
  Qed