NO


NON-Termination:
----------------
SCC:
+--transitions: t1,t10,t11,t2,t3,t4,t5
+--nodes: l1,l2,l3,l4,l8
Closed walk: 6 -> t10, t11, t1, t3, t4, t5
deterministic: Forced for: X0, X0, Local0, Local0, Local0
Reachability checked!
- Recurrent Set Found:
{
	-13 + Local0 == 0,
	-14 + x_5_post == 0,
	-14 + X4 == 0,
	-14 + X3 == 0,
	-14 + X2 == 0,
	-15 + X1 == 0,
	-15 + X0 == 0,
	-14 + x_5_0 == 0
}
method 1