NO


Termination: (Ranking Functions Found)
------------
l0: < < -i_0 + nodecount_0, 0 > >
l1: < < -1 -i_0 + nodecount_0, -1 -i_0 + nodecount_0 > >
l10: < < -k_0 + nodecount_0 > >
l11: < < -k_0 + nodecount_0 > >
l12: < < -k_0 + nodecount_0 > >
l13: < < -k_0 + nodecount_0 > >
l14: < < -k_0 + nodecount_0 > >
l15: < < -k_0 + nodecount_0 > >
l16: < < -k_0 + nodecount_0 > >
l17: < < -k_0 + nodecount_0 > >
l18: < < -k_0 + nodecount_0 > >
l19: < < -k_0 + nodecount_0 > >
l2: < < 1 -i_0 + nodecount_0, 0 > >
l20: < < -k_0 + nodecount_0 > >
l21: < < -k_0 + nodecount_0 > >
l22: < < -k_0 + nodecount_0 > >
l23: < < -k_0 + nodecount_0 > >
l24: < < -k_0 + nodecount_0 > >
l25: < < -k_0 + nodecount_0 > >
l3: < < -i_0 + nodecount_0, -i_0 + nodecount_0 > >
l4: < < 1 -k_0 + nodecount_0 > >
l5: < < 1 -k_0 + nodecount_0 > >
l6: < < -k_0 + nodecount_0 > >
l7: < < -k_0 + nodecount_0 > >
l8: < < -k_0 + nodecount_0 > >
l9: < < -k_0 + nodecount_0 > >


NON-Termination:
----------------
SCC:
+--transitions: t10,t11,t12,t13,t14,t15,t16,t17,t18,t19,t2,t20,t21,t22,t23,t24,t25,t26,t27,t28,t29,t3,t30,t31,t32,t33,t34,t35,t37,t4,t41,t5,t6,t7,t9
+--nodes: l10,l11,l12,l13,l14,l15,l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l4,l5,l6,l7,l8,l9
Closed walk: 7 -> t2, t37, t35, t10, t32, t18, t30
Reachability checked!
- Recurrent Set Found:
{
	sourceflag_0 -sourceflag_post == 0,
	nodecount_0 -nodecount_post == 0,
	min_post == 0,
	k_1_post == 0,
	1 + k_0 -k_post == 0,
	j_0 -j_post == 0,
	i_post == 0,
	h_0 -h_post == 0,
	___lengthofvisited_0 -edgecount_post == 0,
	destflag_0 -destflag_post == 0,
	___lengthofvisited_0 -___lengthofvisited_post == 0,
	sourceflag_0 -X65 == 0,
	nodecount_0 -X64 == 0,
	X63 == 0,
	X62 == 0,
	k_0 -X61 == 0,
	j_0 -X60 == 0,
	X59 == 0,
	h_0 -X58 == 0,
	___lengthofvisited_0 -X57 == 0,
	destflag_0 -X56 == 0,
	___lengthofvisited_0 -X55 == 0,
	sourceflag_0 -X54 == 0,
	nodecount_0 -X53 == 0,
	X52 == 0,
	X51 == 0,
	k_0 -X50 == 0,
	j_0 -X49 == 0,
	X48 == 0,
	h_0 -X47 == 0,
	___lengthofvisited_0 -X46 == 0,
	destflag_0 -X45 == 0,
	___lengthofvisited_0 -X44 == 0,
	sourceflag_0 -X43 == 0,
	nodecount_0 -X42 == 0,
	X41 == 0,
	k_1_0 -X40 == 0,
	k_0 -X39 == 0,
	j_0 -X38 == 0,
	X37 == 0,
	h_0 -X36 == 0,
	___lengthofvisited_0 -X35 == 0,
	destflag_0 -X34 == 0,
	___lengthofvisited_0 -X33 == 0,
	sourceflag_0 -X32 == 0,
	nodecount_0 -X31 == 0,
	X30 == 0,
	k_1_0 -X29 == 0,
	k_0 -X28 == 0,
	j_0 -X27 == 0,
	X26 == 0,
	h_0 -X25 == 0,
	___lengthofvisited_0 -X24 == 0,
	destflag_0 -X23 == 0,
	___lengthofvisited_0 -X22 == 0,
	sourceflag_0 -X21 == 0,
	nodecount_0 -X20 == 0,
	min_0 -X19 == 0,
	k_1_0 -X18 == 0,
	k_0 -X17 == 0,
	j_0 -X16 == 0,
	i_0 -X15 == 0,
	h_0 -X14 == 0,
	___lengthofvisited_0 -X13 == 0,
	destflag_0 -X12 == 0,
	___lengthofvisited_0 -X11 == 0,
	sourceflag_0 -X10 == 0,
	nodecount_0 -X9 == 0,
	min_0 -X8 == 0,
	k_1_0 -X7 == 0,
	k_0 -X6 == 0,
	j_0 -X5 == 0,
	i_0 -X4 == 0,
	h_0 -X3 == 0,
	___lengthofvisited_0 -X2 == 0,
	destflag_0 -X1 == 0,
	___lengthofvisited_0 -X0 == 0,
	___lengthofvisited_0 -edgecount_0 == 0,
	k_0 -nodecount_0 >= 0,
	k_0 >= 0,
	-___lengthofvisited_0 >= 0
}
Connected Subgraphs where we couldn't prove Termination:
--------------------------------------------------------
SCC:
+--transitions: t43
+--nodes: l0,l1
SCC:
+--transitions: t40
+--nodes: l2,l3


method 1