YES

This TRS is terminating using the restricteddeltasimple interpretation 
rem(delta13, X15, X14) =  + 1*X14 + 1*X15 + 0 + 1*X14*delta13 + 0*X15*delta13 + 1*delta13
f(delta12, X13, X12) =  + 1*X12 + 0*X13 + 1 + 1*X12*delta12 + 1*X13*delta12 + 1*delta12
g(delta11, X11, X10) =  + 0*X10 + 1*X11 + 1 + 1*X10*delta11 + 0*X11*delta11 + 0*delta11
s(delta10, X9) =  + 1*X9 + 1 + 0*X9*delta10 + 0*delta10
nil(delta9) =  + 0 + 1*delta9
norm(delta8, X8) =  + 1*X8 + 0 + 1*X8*delta8 + 0*delta8
0(delta7) =  + 0 + 0*delta7
rem_tau_1(delta13) =  + 1(delta13/(1 + 0 * delta13))
rem_tau_2(delta13) =  + 1(delta13/(1 + 1 * delta13))
f_tau_1(delta12) =  + 1(delta12/(0 + 1 * delta12))
f_tau_2(delta12) =  + 1(delta12/(1 + 1 * delta12))
g_tau_1(delta11) =  + 1(delta11/(1 + 0 * delta11))
g_tau_2(delta11) =  + 1(delta11/(0 + 1 * delta11))
s_tau_1(delta10) =  + 1(delta10/(1 + 0 * delta10))
norm_tau_1(delta8) =  + 1(delta8/(1 + 1 * delta8))

Time: 0.052726 seconds
SUCCESS

Statistics:
Number of monomials: 376
Last formula building started for bound 1
Last SAT solving started for bound 1