YES
Time: 0.074

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