NO


Termination: (Ranking Functions Found)
------------
n_eval_main_bb1_in___6: < < v_0 + v_1 -v_x_P0 > >
n_eval_main_bb2_in___5: < < -1 + v_0 + v_1 -v_8 > >


NON-Termination:
----------------
SCC:
+--transitions: t4,t5,t6,t7
+--nodes: n_n_eval_main_bb1_in___2___2,n_n_eval_main_bb1_in___4___3,n_n_eval_main_bb2_in___1___1
Closed walk: 3 -> t4, t5, t7
Reachability checked!
- Recurrent Set Found:
{
	-1 + v_y_P0_P == 0,
	1 + v_8 -v_x_P0_P == 0,
	1 + v_7 -v_res_P0_P == 0,
	v_9_P == 0,
	1 + v_8 -v_8_P == 0,
	1 + v_7 -v_7_P == 0,
	-1 + v_1_P == 0,
	v_0 -v_0_P == 0,
	X15 == 0,
	1 + v_8 -X14 == 0,
	v_7 -X13 == 0,
	X12 == 0,
	1 + v_8 -X11 == 0,
	v_7 -X10 == 0,
	-1 + X9 == 0,
	v_0 -X8 == 0,
	X7 == 0,
	1 + v_8 -X6 == 0,
	v_7 -X5 == 0,
	X4 == 0,
	1 + v_8 -X3 == 0,
	v_7 -X2 == 0,
	-1 + X1 == 0,
	v_0 -X0 == 0,
	-1 + v_y_P0 == 0,
	v_8 -v_x_P0 == 0,
	v_7 -v_res_P0 == 0,
	v_9 == 0,
	-1 + v_1 == 0,
	-1 + v_0 >= 0,
	-1 + v_7 >= 0,
	-v_0 -v_7 + v_8 >= 0
}
method 2