YES
Time: 0.018

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-KBO Processor:
  precedence:
   f > b ~ *AC ~ +AC > c ~ a
   weight function:
    w0 = 1
    w(c) = 8
    w(b) = 5
    w(a) = 4
    w(f) = w(*AC) = w(+AC) = 0
   problem:
    Equations:
     
    TRS:
     
   Qed