YES

This TRS is terminating using the restricteddeltasimple interpretation 
s(delta11, X11) =  + 1*X11 + 1 + 0*X11*delta11 + 0*delta11
0(delta10) =  + 1 + 0*delta10
plus(delta9, X10, X9) =  + 1*X9 + 1*X10 + 0 + 1*X9*delta9 + 0*X10*delta9 + 0*delta9
tt(delta8) =  + 0 + 1*delta8
and(delta7, X8, X7) =  + 1*X7 + 1*X8 + 0 + 0*X7*delta7 + 0*X8*delta7 + 1*delta7
activate(delta6, X6) =  + 1*X6 + 0 + 0*X6*delta6 + 1*delta6
s_tau_1(delta11) =  + 1(delta11/(1 + 0 * delta11))
plus_tau_1(delta9) =  + 1(delta9/(1 + 0 * delta9))
plus_tau_2(delta9) =  + 1(delta9/(1 + 1 * delta9))
and_tau_1(delta7) =  + 1(delta7/(1 + 0 * delta7))
and_tau_2(delta7) =  + 1(delta7/(1 + 0 * delta7))
activate_tau_1(delta6) =  + 1(delta6/(1 + 0 * delta6))

Time: 0.011018 seconds
SUCCESS

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