YES
Time: 0.330

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:
 DP Processor:
  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)
  DPs:
   +{AC,#}(a(),*AC(b(),c())) -> *{AC,#}(a(),c())
   +{AC,#}(a(),*AC(b(),c())) -> +{AC,#}(b(),f(*AC(a(),c())))
   *{AC,#}(a(),+AC(b(),c())) -> +{AC,#}(a(),c())
   *{AC,#}(a(),+AC(b(),c())) -> *{AC,#}(b(),f(+AC(a(),c())))
   +{AC,#}(x3,+AC(a(),*AC(b(),c()))) -> *{AC,#}(a(),c())
   +{AC,#}(x3,+AC(a(),*AC(b(),c()))) -> +{AC,#}(b(),f(*AC(a(),c())))
   +{AC,#}(x3,+AC(a(),*AC(b(),c()))) -> +{AC,#}(x3,+AC(b(),f(*AC(a(),c()))))
   *{AC,#}(x4,*AC(a(),+AC(b(),c()))) -> +{AC,#}(a(),c())
   *{AC,#}(x4,*AC(a(),+AC(b(),c()))) -> *{AC,#}(b(),f(+AC(a(),c())))
   *{AC,#}(x4,*AC(a(),+AC(b(),c()))) -> *{AC,#}(x4,*AC(b(),f(+AC(a(),c()))))
  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())))
  S:
   +{AC,#}(+AC(x5,x6),x7) -> +{AC,#}(x5,x6)
   +{AC,#}(x5,+AC(x6,x7)) -> +{AC,#}(x6,x7)
   *{AC,#}(*AC(x5,x6),x7) -> *{AC,#}(x5,x6)
   *{AC,#}(x5,*AC(x6,x7)) -> *{AC,#}(x6,x7)
  AC-EDG Processor:
   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)
   DPs:
    +{AC,#}(a(),*AC(b(),c())) -> *{AC,#}(a(),c())
    +{AC,#}(a(),*AC(b(),c())) -> +{AC,#}(b(),f(*AC(a(),c())))
    *{AC,#}(a(),+AC(b(),c())) -> +{AC,#}(a(),c())
    *{AC,#}(a(),+AC(b(),c())) -> *{AC,#}(b(),f(+AC(a(),c())))
    +{AC,#}(x3,+AC(a(),*AC(b(),c()))) -> *{AC,#}(a(),c())
    +{AC,#}(x3,+AC(a(),*AC(b(),c()))) -> +{AC,#}(b(),f(*AC(a(),c())))
    +{AC,#}(x3,+AC(a(),*AC(b(),c()))) -> +{AC,#}(x3,+AC(b(),f(*AC(a(),c()))))
    *{AC,#}(x4,*AC(a(),+AC(b(),c()))) -> +{AC,#}(a(),c())
    *{AC,#}(x4,*AC(a(),+AC(b(),c()))) -> *{AC,#}(b(),f(+AC(a(),c())))
    *{AC,#}(x4,*AC(a(),+AC(b(),c()))) -> *{AC,#}(x4,*AC(b(),f(+AC(a(),c()))))
   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())))
   S:
    +{AC,#}(+AC(x5,x6),x7) -> +{AC,#}(x5,x6)
    +{AC,#}(x5,+AC(x6,x7)) -> +{AC,#}(x6,x7)
    *{AC,#}(*AC(x5,x6),x7) -> *{AC,#}(x5,x6)
    *{AC,#}(x5,*AC(x6,x7)) -> *{AC,#}(x6,x7)
   SCC Processor:
    #sccs: 2
    #rules: 2
    #arcs: 10/100
    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)
    DPs:
     +{AC,#}(x3,+AC(a(),*AC(b(),c()))) -> +{AC,#}(x3,+AC(b(),f(*AC(a(),c()))))
    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())))
    S:
     +{AC,#}(+AC(x5,x6),x7) -> +{AC,#}(x5,x6)
     +{AC,#}(x5,+AC(x6,x7)) -> +{AC,#}(x6,x7)
     *{AC,#}(*AC(x5,x6),x7) -> *{AC,#}(x5,x6)
     *{AC,#}(x5,*AC(x6,x7)) -> *{AC,#}(x6,x7)
    AC-DP unlabeling:
     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)
     DPs:
      +AC(x3,+AC(a(),*AC(b(),c()))) -> +AC(x3,+AC(b(),f(*AC(a(),c()))))
     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())))
     S:
      +AC(+AC(x5,x6),x7) -> +AC(x5,x6)
      +AC(x5,+AC(x6,x7)) -> +AC(x6,x7)
      *AC(*AC(x5,x6),x7) -> *AC(x5,x6)
      *AC(x5,*AC(x6,x7)) -> *AC(x6,x7)
     Usable Rule Processor:
      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)
      DPs:
       +AC(x3,+AC(a(),*AC(b(),c()))) -> +AC(x3,+AC(b(),f(*AC(a(),c()))))
      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:
       
      S:
       +AC(+AC(x5,x6),x7) -> +AC(x5,x6)
       +AC(x5,+AC(x6,x7)) -> +AC(x6,x7)
       *AC(*AC(x5,x6),x7) -> *AC(x5,x6)
       *AC(x5,*AC(x6,x7)) -> *AC(x6,x7)
      AC-KBO Processor:
       argument filtering:
        pi(+AC) = [0,1]
        pi(*AC) = [0,1]
        pi(a) = []
        pi(b) = []
        pi(c) = []
        pi(f) = []
       precedence:
        f > c ~ b ~ a > *AC ~ +AC
        weight function:
         [f](x0) = 1,
         
         [c] = 6,
         
         [b] = 4,
         
         [a] = 2,
         
         [*AC](x0, x1) = x0 + x1,
         
         [+AC](x0, x1) = x0 + x1 + 4
         usable rules:
          
         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)
          DPs:
           
          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:
           
          S:
           +AC(+AC(x5,x6),x7) -> +AC(x5,x6)
           +AC(x5,+AC(x6,x7)) -> +AC(x6,x7)
           *AC(*AC(x5,x6),x7) -> *AC(x5,x6)
           *AC(x5,*AC(x6,x7)) -> *AC(x6,x7)
         Qed
     
     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)
     DPs:
      *{AC,#}(x4,*AC(a(),+AC(b(),c()))) -> *{AC,#}(x4,*AC(b(),f(+AC(a(),c()))))
     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())))
     S:
      +{AC,#}(+AC(x5,x6),x7) -> +{AC,#}(x5,x6)
      +{AC,#}(x5,+AC(x6,x7)) -> +{AC,#}(x6,x7)
      *{AC,#}(*AC(x5,x6),x7) -> *{AC,#}(x5,x6)
      *{AC,#}(x5,*AC(x6,x7)) -> *{AC,#}(x6,x7)
     AC-DP unlabeling:
      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)
      DPs:
       *AC(x4,*AC(a(),+AC(b(),c()))) -> *AC(x4,*AC(b(),f(+AC(a(),c()))))
      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())))
      S:
       +AC(+AC(x5,x6),x7) -> +AC(x5,x6)
       +AC(x5,+AC(x6,x7)) -> +AC(x6,x7)
       *AC(*AC(x5,x6),x7) -> *AC(x5,x6)
       *AC(x5,*AC(x6,x7)) -> *AC(x6,x7)
      Usable Rule Processor:
       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)
       DPs:
        *AC(x4,*AC(a(),+AC(b(),c()))) -> *AC(x4,*AC(b(),f(+AC(a(),c()))))
       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:
        
       S:
        +AC(+AC(x5,x6),x7) -> +AC(x5,x6)
        +AC(x5,+AC(x6,x7)) -> +AC(x6,x7)
        *AC(*AC(x5,x6),x7) -> *AC(x5,x6)
        *AC(x5,*AC(x6,x7)) -> *AC(x6,x7)
       AC-KBO Processor:
        argument filtering:
         pi(+AC) = [0,1]
         pi(*AC) = [0,1]
         pi(a) = []
         pi(b) = []
         pi(c) = []
         pi(f) = 0
        precedence:
         f > c ~ a > +AC > *AC > b
         weight function:
          [f](x0) = x0,
          
          [c] = 1,
          
          [b] = 6,
          
          [a] = 1,
          
          [*AC](x0, x1) = x0 + x1,
          
          [+AC](x0, x1) = x0 + x1 + 4
          usable rules:
           
          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)
           DPs:
            
           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:
            
           S:
            +AC(+AC(x5,x6),x7) -> +AC(x5,x6)
            +AC(x5,+AC(x6,x7)) -> +AC(x6,x7)
            *AC(*AC(x5,x6),x7) -> *AC(x5,x6)
            *AC(x5,*AC(x6,x7)) -> *AC(x6,x7)
          Qed