YES
  TPA v.1.0

Result: TRS is terminating

Default interpretations for symbols are not printed. For polynomial interpretations
and semantic labelling over N\{0,1} defaults are 2 for constants, identity for unary
symbols and x+y-2 for binary symbols. For semantic labelling over {0,1} (booleans)
defaults are 0 for constants, identity for unary symbols and disjunction for binary symbols.

[1]  TRS loaded from input file:
(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))))

[2]  All the rules of this TRS can be oriented with RPO with the following precedence:
Precedence:
dx > one
dx > zero
dx > plus
dx > times
dx > minus
dx > neg
dx > div
dx > exp
dx > two
dx > ln


../tpdb/TRS/Rubio/polo2.trs, 0.01, Y
Couldn't open file <60>: 60: No such file or directory