YES
(VAR X ALPHA BETA)
(RULES 
dx(X) -> one
dx(a) -> zero
dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
dx(neg(ALPHA)) -> neg(dx(ALPHA))
dx(div(ALPHA,BETA)) -> minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two))))
dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA)
dx(exp(ALPHA,BETA)) -> plus(times(BETA,times(exp(ALPHA,minus(BETA,one)),dx(ALPHA))),times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA))))
)

Proving termination of rewriting for polo2:

-> Dependency pairs:
nF_dx(plus(ALPHA,BETA)) -> nF_dx(ALPHA)
nF_dx(plus(ALPHA,BETA)) -> nF_dx(BETA)
nF_dx(times(ALPHA,BETA)) -> nF_dx(ALPHA)
nF_dx(times(ALPHA,BETA)) -> nF_dx(BETA)
nF_dx(minus(ALPHA,BETA)) -> nF_dx(ALPHA)
nF_dx(minus(ALPHA,BETA)) -> nF_dx(BETA)
nF_dx(neg(ALPHA)) -> nF_dx(ALPHA)
nF_dx(div(ALPHA,BETA)) -> nF_dx(ALPHA)
nF_dx(div(ALPHA,BETA)) -> nF_dx(BETA)
nF_dx(ln(ALPHA)) -> nF_dx(ALPHA)
nF_dx(exp(ALPHA,BETA)) -> nF_dx(ALPHA)
nF_dx(exp(ALPHA,BETA)) -> nF_dx(BETA)

-> Proof of termination for polo2_1:
-> -> Dependency pairs in cycle:
nF_dx(plus(ALPHA,BETA)) -> nF_dx(ALPHA)
nF_dx(exp(ALPHA,BETA)) -> nF_dx(BETA)
nF_dx(exp(ALPHA,BETA)) -> nF_dx(ALPHA)
nF_dx(ln(ALPHA)) -> nF_dx(ALPHA)
nF_dx(div(ALPHA,BETA)) -> nF_dx(BETA)
nF_dx(div(ALPHA,BETA)) -> nF_dx(ALPHA)
nF_dx(neg(ALPHA)) -> nF_dx(ALPHA)
nF_dx(minus(ALPHA,BETA)) -> nF_dx(BETA)
nF_dx(minus(ALPHA,BETA)) -> nF_dx(ALPHA)
nF_dx(times(ALPHA,BETA)) -> nF_dx(BETA)
nF_dx(times(ALPHA,BETA)) -> nF_dx(ALPHA)
nF_dx(plus(ALPHA,BETA)) -> nF_dx(BETA)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.