Input TRS:
    1: dx(X) -> one()
    2: dx(a()) -> zero()
    3: dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
    4: dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
    5: dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
    6: dx(neg(ALPHA)) -> neg(dx(ALPHA))
    7: dx(div(ALPHA,BETA)) -> minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
    8: dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA)
    9: dx(exp(ALPHA,BETA)) -> plus(times(BETA,times(exp(ALPHA,minus(BETA,one())),dx(ALPHA))),times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA))))
Number of strict rules: 9
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #dx(neg(ALPHA)) -> #dx(ALPHA)
   #2: #dx(exp(ALPHA,BETA)) -> #dx(ALPHA)
   #3: #dx(exp(ALPHA,BETA)) -> #dx(BETA)
   #4: #dx(div(ALPHA,BETA)) -> #dx(ALPHA)
   #5: #dx(div(ALPHA,BETA)) -> #dx(BETA)
   #6: #dx(minus(ALPHA,BETA)) -> #dx(ALPHA)
   #7: #dx(minus(ALPHA,BETA)) -> #dx(BETA)
   #8: #dx(plus(ALPHA,BETA)) -> #dx(ALPHA)
   #9: #dx(plus(ALPHA,BETA)) -> #dx(BETA)
   #10: #dx(ln(ALPHA)) -> #dx(ALPHA)
   #11: #dx(times(ALPHA,BETA)) -> #dx(ALPHA)
   #12: #dx(times(ALPHA,BETA)) -> #dx(BETA)
Number of SCCs: 1, DPs: 12, edges: 144
	SCC { #1..12 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
  zero()	weight: 0
     a()	weight: 0
    ln(x1)	weight: (/ 1 2) + x1
 minus(x1,x2)	weight: (/ 1 2) + x1 + x2
  #dx(x1)	weight: x1
   div(x1,x2)	weight: (/ 1 2) + x1 + x2
   two()	weight: 0
    dx(x1)	weight: 0
   one()	weight: 0
 times(x1,x2)	weight: (/ 1 2) + x1 + x2
   neg(x1)	weight: (/ 1 2) + x1
  plus(x1,x2)	weight: (/ 1 2) + x1 + x2
   exp(x1,x2)	weight: (/ 1 2) + x1 + x2
    Usable rules: { }
    Removed DPs: #1..12
Number of SCCs: 0, DPs: 0, edges: 0
YES