YES

This TRS is terminating using the restricteddeltasimple interpretation 
top(delta15, X15) =  + 0*X15 + 0 + 4*X15*delta15 + 0*delta15
ok(delta14, X14) =  + 1*X14 + 4 + 7*X14*delta14 + 4*delta14
proper(delta13, X13) =  + 1*X13 + 0 + 1*X13*delta13 + 0*delta13
active(delta12, X12) =  + 1*X12 + 3 + 7*X12*delta12 + 7*delta12
f(delta11, X11) =  + 1*X11 + 1 + 2*X11*delta11 + 0*delta11
h(delta10, X10) =  + 1*X10 + 1 + 2*X10*delta10 + 0*delta10
g(delta9, X9) =  + 1*X9 + 1 + 4*X9*delta9 + 0*delta9
mark(delta8, X8) =  + 1*X8 + 1 + 1*X8*delta8 + 0*delta8
top_tau_1(delta15) =  + 1(delta15/(0 + 4 * delta15))
ok_tau_1(delta14) =  + 1(delta14/(1 + 7 * delta14))
proper_tau_1(delta13) =  + 1(delta13/(1 + 1 * delta13))
active_tau_1(delta12) =  + 1(delta12/(1 + 7 * delta12))
f_tau_1(delta11) =  + 1(delta11/(1 + 2 * delta11))
h_tau_1(delta10) =  + 1(delta10/(1 + 2 * delta10))
g_tau_1(delta9) =  + 1(delta9/(1 + 4 * delta9))
mark_tau_1(delta8) =  + 1(delta8/(1 + 1 * delta8))

Time: 50.210440 seconds
SUCCESS

Statistics:
Number of monomials: 982
Last formula building started for bound 7
Last SAT solving started for bound 7