YES
Time: 0.309

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 > c ~ b ~ a ~ *AC ~ +AC
   weight function:
    [f](x0) = x0,
    
    [c] = 2,
    
    [b] = 15,
    
    [a] = 2,
    
    [*AC](x0, x1) = x0 + x1 + 2,
    
    [+AC](x0, x1) = x0 + x1 + 2
   problem:
    Equations:
     
    TRS:
     
   Qed