NO


Termination: (Ranking Functions Found)
------------
eval_main_bb1_in: < < 10 -v_i.0 -v_j.0 >, < -1 -v_i.0 + v_j.0 > >
eval_main_bb2_in: < < 10 -v_i.0 -v_j.0 >, < -1 -v_i.0 + v_j.0 > >
eval_main_bb3_in: < < 10 -v_i.0 -v_j.0 >, < -1 -v_i.0 + v_j.0 > >
eval_main_bb4_in: < < 10 -v_i.0 -v_j.0 >, < -2 -v_i.0 + v_j.0 > >
eval_main_bb5_in: < < 10 -v_i.0 -v_j.0 >, < -v_3 + v_j.0 > >
eval_main_bb6_in: < < 10 -v_i.0 -v_j.0 >, < -1 -v_i.0 + v_j.0 > >
eval_main_bb8_in: < < 10 -v_i.0 -v_j.0 >, < -3 -v_i.0 + v_j.0 > >
n_eval_main_bb1_in___29: < < 1 + v_j_P0 > >
n_eval_main_bb1_in___54: < < 0 > >
n_eval_main_bb1_in___67: < < 16 * v_0 -8 * v_10 > >
n_eval_main_bb2_in___10: < < v_j_P0 > >
n_eval_main_bb2_in___45: < < 16 * v_0 -8 * v_5 > >
n_eval_main_bb2_in___47: < < -2 * v_10 > >
n_eval_main_bb3_in___44: < < 16 * v_0 -8 * v_j_P0 > >
n_eval_main_bb3_in___46: < < -v_8 > >
n_eval_main_bb3_in___9: < < v_j_P0 > >
n_eval_main_bb4_in___43: < < 0 > >


NON-Termination:
----------------
SCC:
+--transitions: t12
+--nodes: n_n_eval_main_bb1_in___55___4
Closed walk: 1 -> t12
Reachability checked!
- Recurrent Set Found:
{
	-1 + v_17 -v_j_P4_P == 0,
	v_j_P3 -v_j_P3_P == 0,
	-5 + v_j_P1_P == 0,
	-5 + v_j_P0_P == 0,
	v_i_P3 -v_i_P3_P == 0,
	4 + v_3 -v_i_P1_P == 0,
	4 + v_3 -v_i_P0_P == 0,
	-6 + v_9_P == 0,
	4 + v_3 -v_8_P == 0,
	-2 + v_3 -v_6_P == 0,
	-5 + v_5_P == 0,
	3 + v_3 -v_3_P == 0,
	1 + v_17 -v_21_P == 0,
	-1 + v_17 -v_20_P == 0,
	2 * v_17 -v_18_P == 0,
	v_17 -v_17_P == 0,
	v_16 -v_16_P == 0,
	v_15 -v_15_P == 0,
	v_13 -v_13_P == 0,
	-4 + v_10_P == 0,
	v_0 -v_0_P == 0,
	-1 + v_17 -v_j_P4 == 0,
	-5 + v_j_P1 == 0,
	-5 + v_j_P0 == 0,
	1 + v_3 -v_i_P1 == 0,
	1 + v_3 -v_i_P0 == 0,
	-6 + v_9 == 0,
	1 + v_3 -v_8 == 0,
	-5 + v_3 -v_6 == 0,
	-5 + v_5 == 0,
	1 + v_17 -v_21 == 0,
	-1 + v_17 -v_20 == 0,
	2 * v_17 -v_18 == 0,
	-4 + v_10 == 0,
	-2 -v_0 + v_17 >= 0,
	6 -v_17 >= 0,
	-8 + 2 * v_0 + v_17 >= 0,
	-14 + v_17 + v_3 >= 0
}
Connected Subgraphs where we couldn't prove Termination:
--------------------------------------------------------
SCC:
+--transitions: t9
+--nodes: n_n_eval_main_bb1_in___20___7
SCC:
+--transitions: t8
+--nodes: n_n_eval_main_bb1_in___7___5


method 2