YES

This TRS is terminating using the additive interpretation 
first(delta9, X8, X7) =  + 1*X7 + 1*X8 + 1
nil(delta8) =  + 3
add(delta7, X6, X5) =  + 1*X5 + 1*X6 + 2
dbl(delta6, X4) =  + 1*X4 + 2
s(delta5) =  + 2
0(delta4) =  + 3
terms(delta3, X3) =  + 1*X3 + 3
sqr(delta2, X2) =  + 1*X2 + 2
recip(delta1, X1) =  + 1*X1 + 0
cons(delta0, X0) =  + 1*X0 + 0
first_tau_1(delta9) = 
first_tau_2(delta9) = 
add_tau_1(delta7) = 
add_tau_2(delta7) = 
dbl_tau_1(delta6) = 
terms_tau_1(delta3) = 
sqr_tau_1(delta2) = 
recip_tau_1(delta1) = 
cons_tau_1(delta0) = 

Time: 0.002365 seconds
SUCCESS

Statistics:
Number of monomials: 27
Last formula building started for bound 3
Last SAT solving started for bound 3