YES
Time: 0.227

Problem:
 Equations:
  +AC(+AC(x2,x3),x4) -> +AC(x2,+AC(x3,x4))
  +AC(x2,x3) -> +AC(x3,x2)
  *AC(*AC(x2,x3),x4) -> *AC(x2,*AC(x3,x4))
  *AC(x2,x3) -> *AC(x3,x2)
  +AC(x2,+AC(x3,x4)) -> +AC(+AC(x2,x3),x4)
  +AC(x3,x2) -> +AC(x2,x3)
  *AC(x2,*AC(x3,x4)) -> *AC(*AC(x2,x3),x4)
  *AC(x3,x2) -> *AC(x2,x3)
 TRS:
  dx(X()) -> 1()
  dx(0()) -> 0()
  dx(1()) -> 0()
  dx(a()) -> 0()
  dx(+AC(f,g)) -> +AC(dx(f),dx(g))
  dx(*AC(f,g)) -> +AC(*AC(dx(f),g),*AC(dx(g),f))
  dx(-(f,g)) -> -(dx(f),dx(g))
  dx(neg(f)) -> neg(dx(f))
  dx(/(f,g)) -> -(/(dx(f),g),/(*AC(dx(g),f),exp(g,2())))
  dx(ln(f)) -> /(dx(f),f)
  dx(exp(f,g)) -> +AC(*AC(dx(f),*AC(exp(f,-(g,1())),g)),*AC(dx(g),*AC(exp(f,g),ln(f))))

Proof:
 DP Processor:
  Equations#:
   +{AC,#}(+AC(x2,x3),x4) -> +{AC,#}(x2,+AC(x3,x4))
   +{AC,#}(x2,x3) -> +{AC,#}(x3,x2)
   *{AC,#}(*AC(x2,x3),x4) -> *{AC,#}(x2,*AC(x3,x4))
   *{AC,#}(x2,x3) -> *{AC,#}(x3,x2)
   +{AC,#}(x2,+AC(x3,x4)) -> +{AC,#}(+AC(x2,x3),x4)
   +{AC,#}(x3,x2) -> +{AC,#}(x2,x3)
   *{AC,#}(x2,*AC(x3,x4)) -> *{AC,#}(*AC(x2,x3),x4)
   *{AC,#}(x3,x2) -> *{AC,#}(x2,x3)
  DPs:
   dx#(+AC(f,g)) -> dx#(g)
   dx#(+AC(f,g)) -> dx#(f)
   dx#(*AC(f,g)) -> dx#(g)
   dx#(*AC(f,g)) -> dx#(f)
   dx#(-(f,g)) -> dx#(g)
   dx#(-(f,g)) -> dx#(f)
   dx#(neg(f)) -> dx#(f)
   dx#(/(f,g)) -> dx#(g)
   dx#(/(f,g)) -> dx#(f)
   dx#(ln(f)) -> dx#(f)
   dx#(exp(f,g)) -> dx#(g)
   dx#(exp(f,g)) -> dx#(f)
  Equations:
   +AC(+AC(x2,x3),x4) -> +AC(x2,+AC(x3,x4))
   +AC(x2,x3) -> +AC(x3,x2)
   *AC(*AC(x2,x3),x4) -> *AC(x2,*AC(x3,x4))
   *AC(x2,x3) -> *AC(x3,x2)
   +AC(x2,+AC(x3,x4)) -> +AC(+AC(x2,x3),x4)
   +AC(x3,x2) -> +AC(x2,x3)
   *AC(x2,*AC(x3,x4)) -> *AC(*AC(x2,x3),x4)
   *AC(x3,x2) -> *AC(x2,x3)
  TRS:
   dx(X()) -> 1()
   dx(0()) -> 0()
   dx(1()) -> 0()
   dx(a()) -> 0()
   dx(+AC(f,g)) -> +AC(dx(f),dx(g))
   dx(*AC(f,g)) -> +AC(*AC(dx(f),g),*AC(dx(g),f))
   dx(-(f,g)) -> -(dx(f),dx(g))
   dx(neg(f)) -> neg(dx(f))
   dx(/(f,g)) -> -(/(dx(f),g),/(*AC(dx(g),f),exp(g,2())))
   dx(ln(f)) -> /(dx(f),f)
   dx(exp(f,g)) -> +AC(*AC(dx(f),*AC(exp(f,-(g,1())),g)),*AC(dx(g),*AC(exp(f,g),ln(f))))
  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(x2,x3),x4) -> +AC(x2,+AC(x3,x4))
    +AC(x2,x3) -> +AC(x3,x2)
    *AC(*AC(x2,x3),x4) -> *AC(x2,*AC(x3,x4))
    *AC(x2,x3) -> *AC(x3,x2)
    +AC(x2,+AC(x3,x4)) -> +AC(+AC(x2,x3),x4)
    +AC(x3,x2) -> +AC(x2,x3)
    *AC(x2,*AC(x3,x4)) -> *AC(*AC(x2,x3),x4)
    *AC(x3,x2) -> *AC(x2,x3)
   DPs:
    dx#(+AC(f,g)) -> dx#(g)
    dx#(+AC(f,g)) -> dx#(f)
    dx#(*AC(f,g)) -> dx#(g)
    dx#(*AC(f,g)) -> dx#(f)
    dx#(-(f,g)) -> dx#(g)
    dx#(-(f,g)) -> dx#(f)
    dx#(neg(f)) -> dx#(f)
    dx#(/(f,g)) -> dx#(g)
    dx#(/(f,g)) -> dx#(f)
    dx#(ln(f)) -> dx#(f)
    dx#(exp(f,g)) -> dx#(g)
    dx#(exp(f,g)) -> dx#(f)
   Equations:
    +AC(+AC(x2,x3),x4) -> +AC(x2,+AC(x3,x4))
    +AC(x2,x3) -> +AC(x3,x2)
    *AC(*AC(x2,x3),x4) -> *AC(x2,*AC(x3,x4))
    *AC(x2,x3) -> *AC(x3,x2)
    +AC(x2,+AC(x3,x4)) -> +AC(+AC(x2,x3),x4)
    +AC(x3,x2) -> +AC(x2,x3)
    *AC(x2,*AC(x3,x4)) -> *AC(*AC(x2,x3),x4)
    *AC(x3,x2) -> *AC(x2,x3)
   TRS:
    dx(X()) -> 1()
    dx(0()) -> 0()
    dx(1()) -> 0()
    dx(a()) -> 0()
    dx(+AC(f,g)) -> +AC(dx(f),dx(g))
    dx(*AC(f,g)) -> +AC(*AC(dx(f),g),*AC(dx(g),f))
    dx(-(f,g)) -> -(dx(f),dx(g))
    dx(neg(f)) -> neg(dx(f))
    dx(/(f,g)) -> -(/(dx(f),g),/(*AC(dx(g),f),exp(g,2())))
    dx(ln(f)) -> /(dx(f),f)
    dx(exp(f,g)) -> +AC(*AC(dx(f),*AC(exp(f,-(g,1())),g)),*AC(dx(g),*AC(exp(f,g),ln(f))))
   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(x2,x3),x4) -> +AC(x2,+AC(x3,x4))
     +AC(x2,x3) -> +AC(x3,x2)
     *AC(*AC(x2,x3),x4) -> *AC(x2,*AC(x3,x4))
     *AC(x2,x3) -> *AC(x3,x2)
     +AC(x2,+AC(x3,x4)) -> +AC(+AC(x2,x3),x4)
     +AC(x3,x2) -> +AC(x2,x3)
     *AC(x2,*AC(x3,x4)) -> *AC(*AC(x2,x3),x4)
     *AC(x3,x2) -> *AC(x2,x3)
    DPs:
     dx#(+AC(f,g)) -> dx#(g)
     dx#(+AC(f,g)) -> dx#(f)
     dx#(*AC(f,g)) -> dx#(g)
     dx#(*AC(f,g)) -> dx#(f)
     dx#(-(f,g)) -> dx#(g)
     dx#(-(f,g)) -> dx#(f)
     dx#(neg(f)) -> dx#(f)
     dx#(/(f,g)) -> dx#(g)
     dx#(/(f,g)) -> dx#(f)
     dx#(ln(f)) -> dx#(f)
     dx#(exp(f,g)) -> dx#(g)
     dx#(exp(f,g)) -> dx#(f)
    Equations:
     +AC(+AC(x2,x3),x4) -> +AC(x2,+AC(x3,x4))
     +AC(x2,x3) -> +AC(x3,x2)
     *AC(*AC(x2,x3),x4) -> *AC(x2,*AC(x3,x4))
     *AC(x2,x3) -> *AC(x3,x2)
     +AC(x2,+AC(x3,x4)) -> +AC(+AC(x2,x3),x4)
     +AC(x3,x2) -> +AC(x2,x3)
     *AC(x2,*AC(x3,x4)) -> *AC(*AC(x2,x3),x4)
     *AC(x3,x2) -> *AC(x2,x3)
    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(-) = [0,1]
      pi(neg) = 0
      pi(/) = [0,1]
      pi(exp) = [0,1]
      pi(ln) = 0
      pi(dx#) = [0]
     precedence:
      dx# > ln ~ exp ~ / ~ neg ~ - ~ +AC ~ *AC
      weight function:
       [dx#](x0) = 2x0,
       
       [ln](x0) = x0,
       
       [exp](x0, x1) = x0 + x1,
       
       [/](x0, x1) = 4x0 + x1,
       
       [neg](x0) = x0,
       
       [-](x0, x1) = 2x0 + 2x1 + 2,
       
       [+AC](x0, x1) = x0 + x1 + 2,
       
       [*AC](x0, x1) = x0 + x1 + 1
       usable rules:
        
       problem:
        Equations#:
         +AC(+AC(x2,x3),x4) -> +AC(x2,+AC(x3,x4))
         +AC(x2,x3) -> +AC(x3,x2)
         *AC(*AC(x2,x3),x4) -> *AC(x2,*AC(x3,x4))
         *AC(x2,x3) -> *AC(x3,x2)
         +AC(x2,+AC(x3,x4)) -> +AC(+AC(x2,x3),x4)
         +AC(x3,x2) -> +AC(x2,x3)
         *AC(x2,*AC(x3,x4)) -> *AC(*AC(x2,x3),x4)
         *AC(x3,x2) -> *AC(x2,x3)
        DPs:
         dx#(neg(f)) -> dx#(f)
         dx#(ln(f)) -> dx#(f)
        Equations:
         +AC(+AC(x2,x3),x4) -> +AC(x2,+AC(x3,x4))
         +AC(x2,x3) -> +AC(x3,x2)
         *AC(*AC(x2,x3),x4) -> *AC(x2,*AC(x3,x4))
         *AC(x2,x3) -> *AC(x3,x2)
         +AC(x2,+AC(x3,x4)) -> +AC(+AC(x2,x3),x4)
         +AC(x3,x2) -> +AC(x2,x3)
         *AC(x2,*AC(x3,x4)) -> *AC(*AC(x2,x3),x4)
         *AC(x3,x2) -> *AC(x2,x3)
        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)
       Restore Modifier:
        Equations#:
         +AC(+AC(x2,x3),x4) -> +AC(x2,+AC(x3,x4))
         +AC(x2,x3) -> +AC(x3,x2)
         *AC(*AC(x2,x3),x4) -> *AC(x2,*AC(x3,x4))
         *AC(x2,x3) -> *AC(x3,x2)
         +AC(x2,+AC(x3,x4)) -> +AC(+AC(x2,x3),x4)
         +AC(x3,x2) -> +AC(x2,x3)
         *AC(x2,*AC(x3,x4)) -> *AC(*AC(x2,x3),x4)
         *AC(x3,x2) -> *AC(x2,x3)
        DPs:
         dx#(neg(f)) -> dx#(f)
         dx#(ln(f)) -> dx#(f)
        Equations:
         +AC(+AC(x2,x3),x4) -> +AC(x2,+AC(x3,x4))
         +AC(x2,x3) -> +AC(x3,x2)
         *AC(*AC(x2,x3),x4) -> *AC(x2,*AC(x3,x4))
         *AC(x2,x3) -> *AC(x3,x2)
         +AC(x2,+AC(x3,x4)) -> +AC(+AC(x2,x3),x4)
         +AC(x3,x2) -> +AC(x2,x3)
         *AC(x2,*AC(x3,x4)) -> *AC(*AC(x2,x3),x4)
         *AC(x3,x2) -> *AC(x2,x3)
        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-DP unlabeling:
         Equations#:
          +AC(+AC(x2,x3),x4) -> +AC(x2,+AC(x3,x4))
          +AC(x2,x3) -> +AC(x3,x2)
          *AC(*AC(x2,x3),x4) -> *AC(x2,*AC(x3,x4))
          *AC(x2,x3) -> *AC(x3,x2)
          +AC(x2,+AC(x3,x4)) -> +AC(+AC(x2,x3),x4)
          +AC(x3,x2) -> +AC(x2,x3)
          *AC(x2,*AC(x3,x4)) -> *AC(*AC(x2,x3),x4)
          *AC(x3,x2) -> *AC(x2,x3)
         DPs:
          dx#(neg(f)) -> dx#(f)
          dx#(ln(f)) -> dx#(f)
         Equations:
          +AC(+AC(x2,x3),x4) -> +AC(x2,+AC(x3,x4))
          +AC(x2,x3) -> +AC(x3,x2)
          *AC(*AC(x2,x3),x4) -> *AC(x2,*AC(x3,x4))
          *AC(x2,x3) -> *AC(x3,x2)
          +AC(x2,+AC(x3,x4)) -> +AC(+AC(x2,x3),x4)
          +AC(x3,x2) -> +AC(x2,x3)
          *AC(x2,*AC(x3,x4)) -> *AC(*AC(x2,x3),x4)
          *AC(x3,x2) -> *AC(x2,x3)
         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(neg) = [0]
           pi(ln) = [0]
           pi(dx#) = [0]
          precedence:
           dx# ~ ln ~ neg
           weight function:
            [dx#](x0) = 2x0 + 4,
            
            [ln](x0) = 4x0 + 5,
            
            [neg](x0) = 2x0 + 5
            usable rules:
             
            problem:
             Equations#:
              +AC(+AC(x2,x3),x4) -> +AC(x2,+AC(x3,x4))
              +AC(x2,x3) -> +AC(x3,x2)
              *AC(*AC(x2,x3),x4) -> *AC(x2,*AC(x3,x4))
              *AC(x2,x3) -> *AC(x3,x2)
              +AC(x2,+AC(x3,x4)) -> +AC(+AC(x2,x3),x4)
              +AC(x3,x2) -> +AC(x2,x3)
              *AC(x2,*AC(x3,x4)) -> *AC(*AC(x2,x3),x4)
              *AC(x3,x2) -> *AC(x2,x3)
             DPs:
              
             Equations:
              +AC(+AC(x2,x3),x4) -> +AC(x2,+AC(x3,x4))
              +AC(x2,x3) -> +AC(x3,x2)
              *AC(*AC(x2,x3),x4) -> *AC(x2,*AC(x3,x4))
              *AC(x2,x3) -> *AC(x3,x2)
              +AC(x2,+AC(x3,x4)) -> +AC(+AC(x2,x3),x4)
              +AC(x3,x2) -> +AC(x2,x3)
              *AC(x2,*AC(x3,x4)) -> *AC(*AC(x2,x3),x4)
              *AC(x3,x2) -> *AC(x2,x3)
             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