YES This TRS is terminating using the restricteddeltasimple interpretation activate(delta13, X9) = + 1*X9 + 0 + 0*X9*delta13 + 2*delta13 g(delta12, X8) = + 0*X8 + 0 + 1*X8*delta12 + 1*delta12 a(delta11) = + 0 + 2*delta11 n__f(delta10, X7) = + 0*X7 + 2 + 2*X7*delta10 + 1*delta10 n__a(delta9) = + 0 + 1*delta9 n__g(delta8, X6) = + 0*X6 + 0 + 1*X6*delta8 + 0*delta8 f(delta7, X5) = + 0*X5 + 2 + 2*X5*delta7 + 2*delta7 activate_tau_1(delta13) = + 1(delta13/(1 + 0 * delta13)) g_tau_1(delta12) = + 1(delta12/(0 + 1 * delta12)) n__f_tau_1(delta10) = + 1(delta10/(0 + 2 * delta10)) n__g_tau_1(delta8) = + 1(delta8/(0 + 1 * delta8)) f_tau_1(delta7) = + 1(delta7/(0 + 2 * delta7)) Time: 12.061979 seconds SUCCESS Statistics: Number of monomials: 521 Last formula building started for bound 3 Last SAT solving started for bound 3