YES

This TRS is terminating using the restricteddeltasimple interpretation 
0(delta13) =  + 2 + 0*delta13
plus(delta12, X19, X18) =  + 1*X18 + 1*X19 + 0 + 3*X18*delta12 + 0*X19*delta12 + 0*delta12
s(delta11, X17) =  + 1*X17 + 3 + 0*X17*delta11 + 0*delta11
U11(delta10, X16, X15, X14) =  + 1*X14 + 1*X15 + 1*X16 + 3 + 0*X14*delta10 + 3*X15*delta10 + 3*X16*delta10 + 3*delta10
activate(delta9, X13) =  + 1*X13 + 0 + 0*X13*delta9 + 1*delta9
tt(delta8) =  + 0 + 3*delta8
U12(delta7, X12, X11, X10) =  + 1*X10 + 1*X11 + 1*X12 + 3 + 0*X10*delta7 + 3*X11*delta7 + 3*X12*delta7 + 0*delta7
plus_tau_1(delta12) =  + 1(delta12/(1 + 0 * delta12))
plus_tau_2(delta12) =  + 1(delta12/(1 + 3 * delta12))
s_tau_1(delta11) =  + 1(delta11/(1 + 0 * delta11))
U11_tau_1(delta10) =  + 1(delta10/(1 + 3 * delta10))
U11_tau_2(delta10) =  + 1(delta10/(1 + 3 * delta10))
U11_tau_3(delta10) =  + 1(delta10/(1 + 0 * delta10))
activate_tau_1(delta9) =  + 1(delta9/(1 + 0 * delta9))
U12_tau_1(delta7) =  + 1(delta7/(1 + 3 * delta7))
U12_tau_2(delta7) =  + 1(delta7/(1 + 3 * delta7))
U12_tau_3(delta7) =  + 1(delta7/(1 + 0 * delta7))

Time: 6.279882 seconds
SUCCESS

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