NO

Initial ITS
Start location: l8
   0: l0 -> l1 : cnt_38^0'=cnt_38^post0, lt_21^0'=lt_21^post0, lt_16^0'=lt_16^post0, a_6^0'=a_6^post0, lt_18^0'=lt_18^post0, h_13^0'=h_13^post0, x_5^0'=x_5^post0, lt_23^0'=lt_23^post0, e_10^0'=e_10^post0, c_8^0'=c_8^post0, lt_20^0'=lt_20^post0, lt_15^0'=lt_15^post0, lt_25^0'=lt_25^post0, Result_4^0'=Result_4^post0, g_12^0'=g_12^post0, d_9^0'=d_9^post0, lt_22^0'=lt_22^post0, lt_17^0'=lt_17^post0, b_7^0'=b_7^post0, lt_19^0'=lt_19^post0, lt_14^0'=lt_14^post0, lt_24^0'=lt_24^post0, f_11^0'=f_11^post0, (0 == 0 /\ lt_15^0-lt_15^post0 == 0 /\ lt_19^0-lt_19^post0 == 0 /\ -e_10^post0+e_10^0 == 0 /\ -f_11^post0+f_11^0 == 0 /\ -lt_17^post0+lt_17^0 == 0 /\ lt_23^0-lt_23^post0 == 0 /\ -x_5^post0+x_5^0 == 0 /\ lt_21^0-lt_21^post0 == 0 /\ -lt_14^post0+lt_14^0 == 0 /\ -lt_24^post0+lt_24^0 == 0 /\ -c_8^post0+c_8^0 == 0 /\ -b_7^post0+b_7^0 == 0 /\ -lt_20^post0+lt_20^0 == 0 /\ lt_25^0-lt_25^post0 == 0 /\ lt_16^0-lt_16^post0 == 0 /\ lt_22^0-lt_22^post0 == 0 /\ h_13^0-h_13^post0 == 0 /\ g_12^0-g_12^post0 == 0 /\ d_9^0-d_9^post0 == 0 /\ lt_18^0-lt_18^post0 == 0 /\ cnt_38^0-cnt_38^post0 == 0 /\ a_6^0-a_6^post0 == 0), cost: 1
   1: l2 -> l3 : cnt_38^0'=cnt_38^post1, lt_21^0'=lt_21^post1, lt_16^0'=lt_16^post1, a_6^0'=a_6^post1, lt_18^0'=lt_18^post1, h_13^0'=h_13^post1, x_5^0'=x_5^post1, lt_23^0'=lt_23^post1, e_10^0'=e_10^post1, c_8^0'=c_8^post1, lt_20^0'=lt_20^post1, lt_15^0'=lt_15^post1, lt_25^0'=lt_25^post1, Result_4^0'=Result_4^post1, g_12^0'=g_12^post1, d_9^0'=d_9^post1, lt_22^0'=lt_22^post1, lt_17^0'=lt_17^post1, b_7^0'=b_7^post1, lt_19^0'=lt_19^post1, lt_14^0'=lt_14^post1, lt_24^0'=lt_24^post1, f_11^0'=f_11^post1, (0 == 0 /\ lt_15^0-lt_15^post1 == 0 /\ -lt_24^post1+lt_24^0 == 0 /\ lt_23^0-lt_23^post1 == 0 /\ e_10^post1-d_9^post1 == 0 /\ lt_25^0-lt_25^post1 == 0 /\ cnt_38^0-cnt_38^post1 == 0 /\ lt_16^0-lt_16^post1 == 0 /\ -x_5^post1+a_6^post1 == 0 /\ -lt_22^post1+lt_22^0 == 0 /\ -b_7^post1+c_8^post1 == 0 /\ -Result_4^post1+Result_4^0 == 0 /\ d_9^post1-c_8^post1 == 0 /\ h_13^post1-g_12^post1 == 0 /\ lt_21^0-lt_21^post1 == 0 /\ -lt_17^post1+lt_17^0 == 0 /\ -lt_14^post1+lt_14^0 == 0 /\ -e_10^post1+f_11^post1 == 0 /\ lt_18^0-lt_18^post1 == 0 /\ -lt_20^post1+lt_20^0 == 0 /\ -lt_19^post1+lt_19^0 == 0 /\ -f_11^post1+g_12^post1 == 0 /\ -a_6^post1+b_7^post1 == 0), cost: 1
   2: l3 -> l0 : cnt_38^0'=cnt_38^post2, lt_21^0'=lt_21^post2, lt_16^0'=lt_16^post2, a_6^0'=a_6^post2, lt_18^0'=lt_18^post2, h_13^0'=h_13^post2, x_5^0'=x_5^post2, lt_23^0'=lt_23^post2, e_10^0'=e_10^post2, c_8^0'=c_8^post2, lt_20^0'=lt_20^post2, lt_15^0'=lt_15^post2, lt_25^0'=lt_25^post2, Result_4^0'=Result_4^post2, g_12^0'=g_12^post2, d_9^0'=d_9^post2, lt_22^0'=lt_22^post2, lt_17^0'=lt_17^post2, b_7^0'=b_7^post2, lt_19^0'=lt_19^post2, lt_14^0'=lt_14^post2, lt_24^0'=lt_24^post2, f_11^0'=f_11^post2, (0 == 0 /\ -a_6^post2+a_6^0 == 0 /\ -f_11^post2+f_11^0 == 0 /\ c_8^0-c_8^post2 == 0 /\ lt_16^0-lt_16^post2 == 0 /\ -b_7^post2+b_7^0 == 0 /\ x_5^0-x_5^post2 == 0 /\ lt_18^0-lt_18^post2 == 0 /\ e_10^0-e_10^post2 == 0 /\ h_13^0-h_13^post2 == 0 /\ -Result_4^post2+Result_4^0 == 0 /\ -lt_25^10 <= 0 /\ lt_23^0-lt_23^post2 == 0 /\ -lt_22^post2+lt_22^0 == 0 /\ d_9^0-d_9^post2 == 0 /\ -lt_17^post2+lt_17^0 == 0 /\ -cnt_38^0+lt_25^10 == 0 /\ cnt_38^0-cnt_38^post2 == 0 /\ lt_24^10 <= 0 /\ lt_20^0-lt_20^post2 == 0 /\ lt_21^0-lt_21^post2 == 0 /\ -lt_14^post2+lt_14^0 == 0 /\ -lt_19^post2+lt_19^0 == 0 /\ -cnt_38^0+lt_24^10 == 0 /\ -lt_15^post2+lt_15^0 == 0 /\ -g_12^post2+g_12^0 == 0), cost: 1
   3: l3 -> l0 : cnt_38^0'=cnt_38^post3, lt_21^0'=lt_21^post3, lt_16^0'=lt_16^post3, a_6^0'=a_6^post3, lt_18^0'=lt_18^post3, h_13^0'=h_13^post3, x_5^0'=x_5^post3, lt_23^0'=lt_23^post3, e_10^0'=e_10^post3, c_8^0'=c_8^post3, lt_20^0'=lt_20^post3, lt_15^0'=lt_15^post3, lt_25^0'=lt_25^post3, Result_4^0'=Result_4^post3, g_12^0'=g_12^post3, d_9^0'=d_9^post3, lt_22^0'=lt_22^post3, lt_17^0'=lt_17^post3, b_7^0'=b_7^post3, lt_19^0'=lt_19^post3, lt_14^0'=lt_14^post3, lt_24^0'=lt_24^post3, f_11^0'=f_11^post3, (0 == 0 /\ lt_18^10 <= 0 /\ -lt_19^10 <= 0 /\ -lt_14^post3+lt_14^0 == 0 /\ -lt_20^post3+lt_20^0 == 0 /\ -Result_4^post3+Result_4^0 == 0 /\ x_5^0-x_5^post3 == 0 /\ -lt_15^post3+lt_15^0 == 0 /\ lt_21^0-lt_21^post3 == 0 /\ -f_11^post3+f_11^0 == 0 /\ -cnt_38^0+lt_23^10 == 0 /\ a_6^0-a_6^post3 == 0 /\ -b_7^post3+b_7^0 == 0 /\ cnt_38^0-cnt_38^post3 == 0 /\ g_12^0-g_12^post3 == 0 /\ c_8^0-c_8^post3 == 0 /\ -cnt_38^0+lt_24^110 == 0 /\ -lt_25^110 <= 0 /\ e_10^0-e_10^post3 == 0 /\ d_9^0-d_9^post3 == 0 /\ h_13^0-h_13^post3 == 0 /\ 1-lt_24^110 <= 0 /\ lt_16^0-lt_16^post3 == 0 /\ -lt_17^post3+lt_17^0 == 0 /\ -cnt_38^0+lt_25^110 == 0), cost: 1
   4: l3 -> l1 : cnt_38^0'=cnt_38^post4, lt_21^0'=lt_21^post4, lt_16^0'=lt_16^post4, a_6^0'=a_6^post4, lt_18^0'=lt_18^post4, h_13^0'=h_13^post4, x_5^0'=x_5^post4, lt_23^0'=lt_23^post4, e_10^0'=e_10^post4, c_8^0'=c_8^post4, lt_20^0'=lt_20^post4, lt_15^0'=lt_15^post4, lt_25^0'=lt_25^post4, Result_4^0'=Result_4^post4, g_12^0'=g_12^post4, d_9^0'=d_9^post4, lt_22^0'=lt_22^post4, lt_17^0'=lt_17^post4, b_7^0'=b_7^post4, lt_19^0'=lt_19^post4, lt_14^0'=lt_14^post4, lt_24^0'=lt_24^post4, f_11^0'=f_11^post4, (0 == 0 /\ -cnt_38^0+lt_25^120 == 0 /\ -lt_19^110 <= 0 /\ -lt_14^post4+lt_14^0 == 0 /\ -d_9^post4+d_9^0 == 0 /\ lt_15^0-lt_15^post4 == 0 /\ g_12^0-g_12^post4 == 0 /\ -lt_23^post4+lt_23^0 == 0 /\ -c_8^post4+c_8^0 == 0 /\ lt_18^11 <= 0 /\ lt_21^10-cnt_38^0 == 0 /\ -b_7^post4+b_7^0 == 0 /\ -f_11^post4+f_11^0 == 0 /\ h_13^0-h_13^post4 == 0 /\ x_5^0-x_5^post4 == 0 /\ a_6^0-a_6^post4 == 0 /\ -lt_22^post4+lt_22^0 == 0 /\ e_10^0-e_10^post4 == 0 /\ 1+lt_25^120 <= 0 /\ cnt_38^0-cnt_38^post4 == 0 /\ -lt_24^post4+lt_24^0 == 0 /\ lt_16^0-lt_16^post4 == 0 /\ -lt_17^post4+lt_17^0 == 0), cost: 1
   5: l3 -> l4 : cnt_38^0'=cnt_38^post5, lt_21^0'=lt_21^post5, lt_16^0'=lt_16^post5, a_6^0'=a_6^post5, lt_18^0'=lt_18^post5, h_13^0'=h_13^post5, x_5^0'=x_5^post5, lt_23^0'=lt_23^post5, e_10^0'=e_10^post5, c_8^0'=c_8^post5, lt_20^0'=lt_20^post5, lt_15^0'=lt_15^post5, lt_25^0'=lt_25^post5, Result_4^0'=Result_4^post5, g_12^0'=g_12^post5, d_9^0'=d_9^post5, lt_22^0'=lt_22^post5, lt_17^0'=lt_17^post5, b_7^0'=b_7^post5, lt_19^0'=lt_19^post5, lt_14^0'=lt_14^post5, lt_24^0'=lt_24^post5, f_11^0'=f_11^post5, (0 == 0 /\ -lt_20^post5+lt_20^0 == 0 /\ -a_6^post5+a_6^0 == 0 /\ -cnt_38^0+lt_23^110 == 0 /\ -lt_14^post5+lt_14^0 == 0 /\ x_5^0-x_5^post5 == 0 /\ -d_9^post5+d_9^0 == 0 /\ -e_10^post5+e_10^0 == 0 /\ -lt_19^120 <= 0 /\ c_8^0-c_8^post5 == 0 /\ Result_4^0-Result_4^post5 == 0 /\ -lt_25^130 <= 0 /\ -cnt_38^0+lt_24^120 == 0 /\ cnt_38^0-cnt_38^post5 == 0 /\ -cnt_38^0+lt_25^130 == 0 /\ 1-lt_24^120 <= 0 /\ -g_12^post5+g_12^0 == 0 /\ lt_21^0-lt_21^post5 == 0 /\ -f_11^post5+f_11^0 == 0 /\ 1-lt_18^120 <= 0 /\ -b_7^post5+b_7^0 == 0 /\ h_13^0-h_13^post5 == 0 /\ -lt_15^post5+lt_15^0 == 0), cost: 1
   7: l3 -> l5 : cnt_38^0'=cnt_38^post7, lt_21^0'=lt_21^post7, lt_16^0'=lt_16^post7, a_6^0'=a_6^post7, lt_18^0'=lt_18^post7, h_13^0'=h_13^post7, x_5^0'=x_5^post7, lt_23^0'=lt_23^post7, e_10^0'=e_10^post7, c_8^0'=c_8^post7, lt_20^0'=lt_20^post7, lt_15^0'=lt_15^post7, lt_25^0'=lt_25^post7, Result_4^0'=Result_4^post7, g_12^0'=g_12^post7, d_9^0'=d_9^post7, lt_22^0'=lt_22^post7, lt_17^0'=lt_17^post7, b_7^0'=b_7^post7, lt_19^0'=lt_19^post7, lt_14^0'=lt_14^post7, lt_24^0'=lt_24^post7, f_11^0'=f_11^post7, (0 == 0 /\ lt_18^0-lt_18^post7 == 0 /\ a_6^0-a_6^post7 == 0 /\ x_5^0-x_5^post7 == 0 /\ e_10^0-e_10^post7 == 0 /\ -cnt_38^0+lt_25^140 == 0 /\ -lt_25^140 <= 0 /\ -b_7^post7+b_7^0 == 0 /\ lt_21^0-lt_21^post7 == 0 /\ 1+lt_19^130 <= 0 /\ lt_16^0-lt_16^post7 == 0 /\ cnt_38^0-cnt_38^post7 == 0 /\ -g_12^post7+g_12^0 == 0 /\ Result_4^0-Result_4^post7 == 0 /\ lt_17^0-lt_17^post7 == 0 /\ -cnt_38^0+lt_23^120 == 0 /\ c_8^0-c_8^post7 == 0 /\ -d_9^post7+d_9^0 == 0 /\ -lt_20^post7+lt_20^0 == 0 /\ h_13^0-h_13^post7 == 0 /\ -cnt_38^0+lt_24^130 == 0 /\ -f_11^post7+f_11^0 == 0 /\ 1-lt_24^130 <= 0), cost: 1
   9: l3 -> l6 : cnt_38^0'=cnt_38^post9, lt_21^0'=lt_21^post9, lt_16^0'=lt_16^post9, a_6^0'=a_6^post9, lt_18^0'=lt_18^post9, h_13^0'=h_13^post9, x_5^0'=x_5^post9, lt_23^0'=lt_23^post9, e_10^0'=e_10^post9, c_8^0'=c_8^post9, lt_20^0'=lt_20^post9, lt_15^0'=lt_15^post9, lt_25^0'=lt_25^post9, Result_4^0'=Result_4^post9, g_12^0'=g_12^post9, d_9^0'=d_9^post9, lt_22^0'=lt_22^post9, lt_17^0'=lt_17^post9, b_7^0'=b_7^post9, lt_19^0'=lt_19^post9, lt_14^0'=lt_14^post9, lt_24^0'=lt_24^post9, f_11^0'=f_11^post9, (0 == 0 /\ Result_4^0-Result_4^post9 == 0 /\ -f_11^post9+f_11^0 == 0 /\ b_7^0-b_7^post9 == 0 /\ lt_15^0-lt_15^post9 == 0 /\ g_12^0-g_12^post9 == 0 /\ cnt_38^0-cnt_38^post9 == 0 /\ -lt_23^post9+lt_23^0 == 0 /\ 1+lt_25^150 <= 0 /\ -d_9^post9+d_9^0 == 0 /\ -x_5^post9+x_5^0 == 0 /\ a_6^0-a_6^post9 == 0 /\ 1-lt_18^130 <= 0 /\ -lt_24^post9+lt_24^0 == 0 /\ h_13^0-h_13^post9 == 0 /\ -cnt_38^0+lt_25^150 == 0 /\ -c_8^post9+c_8^0 == 0 /\ -lt_14^post9+lt_14^0 == 0 /\ -cnt_38^0+lt_21^110 == 0 /\ -lt_19^140 <= 0 /\ lt_22^0-lt_22^post9 == 0 /\ e_10^0-e_10^post9 == 0), cost: 1
  11: l3 -> l7 : cnt_38^0'=cnt_38^post11, lt_21^0'=lt_21^post11, lt_16^0'=lt_16^post11, a_6^0'=a_6^post11, lt_18^0'=lt_18^post11, h_13^0'=h_13^post11, x_5^0'=x_5^post11, lt_23^0'=lt_23^post11, e_10^0'=e_10^post11, c_8^0'=c_8^post11, lt_20^0'=lt_20^post11, lt_15^0'=lt_15^post11, lt_25^0'=lt_25^post11, Result_4^0'=Result_4^post11, g_12^0'=g_12^post11, d_9^0'=d_9^post11, lt_22^0'=lt_22^post11, lt_17^0'=lt_17^post11, b_7^0'=b_7^post11, lt_19^0'=lt_19^post11, lt_14^0'=lt_14^post11, lt_24^0'=lt_24^post11, f_11^0'=f_11^post11, (0 == 0 /\ -f_11^post11+f_11^0 == 0 /\ -lt_17^post11+lt_17^0 == 0 /\ -e_10^post11+e_10^0 == 0 /\ -b_7^post11+b_7^0 == 0 /\ g_12^0-g_12^post11 == 0 /\ -lt_18^post11+lt_18^0 == 0 /\ 1+lt_19^150 <= 0 /\ lt_16^0-lt_16^post11 == 0 /\ -lt_22^post11+lt_22^0 == 0 /\ 1+lt_25^160 <= 0 /\ -lt_24^post11+lt_24^0 == 0 /\ x_5^0-x_5^post11 == 0 /\ a_6^0-a_6^post11 == 0 /\ lt_23^0-lt_23^post11 == 0 /\ -cnt_38^0+lt_21^120 == 0 /\ -Result_4^post11+Result_4^0 == 0 /\ h_13^0-h_13^post11 == 0 /\ -cnt_38^0+lt_25^160 == 0 /\ cnt_38^0-cnt_38^post11 == 0 /\ -c_8^post11+c_8^0 == 0 /\ d_9^0-d_9^post11 == 0), cost: 1
   6: l4 -> l3 : cnt_38^0'=cnt_38^post6, lt_21^0'=lt_21^post6, lt_16^0'=lt_16^post6, a_6^0'=a_6^post6, lt_18^0'=lt_18^post6, h_13^0'=h_13^post6, x_5^0'=x_5^post6, lt_23^0'=lt_23^post6, e_10^0'=e_10^post6, c_8^0'=c_8^post6, lt_20^0'=lt_20^post6, lt_15^0'=lt_15^post6, lt_25^0'=lt_25^post6, Result_4^0'=Result_4^post6, g_12^0'=g_12^post6, d_9^0'=d_9^post6, lt_22^0'=lt_22^post6, lt_17^0'=lt_17^post6, b_7^0'=b_7^post6, lt_19^0'=lt_19^post6, lt_14^0'=lt_14^post6, lt_24^0'=lt_24^post6, f_11^0'=f_11^post6, (lt_20^0-lt_20^post6 == 0 /\ h_13^0-h_13^post6 == 0 /\ -lt_18^post6+lt_18^0 == 0 /\ lt_14^0-lt_14^post6 == 0 /\ -lt_19^post6+lt_19^0 == 0 /\ -b_7^post6+b_7^0 == 0 /\ -c_8^post6+c_8^0 == 0 /\ -lt_15^post6+lt_15^0 == 0 /\ -lt_25^post6+lt_25^0 == 0 /\ x_5^0-x_5^post6 == 0 /\ -f_11^post6+f_11^0 == 0 /\ lt_21^0-lt_21^post6 == 0 /\ -lt_22^post6+lt_22^0 == 0 /\ lt_16^0-lt_16^post6 == 0 /\ a_6^0-a_6^post6 == 0 /\ cnt_38^0-cnt_38^post6 == 0 /\ -d_9^post6+d_9^0 == 0 /\ lt_17^0-lt_17^post6 == 0 /\ lt_23^0-lt_23^post6 == 0 /\ lt_24^0-lt_24^post6 == 0 /\ e_10^0-e_10^post6 == 0 /\ -g_12^post6+g_12^0 == 0 /\ Result_4^0-Result_4^post6 == 0), cost: 1
   8: l5 -> l3 : cnt_38^0'=cnt_38^post8, lt_21^0'=lt_21^post8, lt_16^0'=lt_16^post8, a_6^0'=a_6^post8, lt_18^0'=lt_18^post8, h_13^0'=h_13^post8, x_5^0'=x_5^post8, lt_23^0'=lt_23^post8, e_10^0'=e_10^post8, c_8^0'=c_8^post8, lt_20^0'=lt_20^post8, lt_15^0'=lt_15^post8, lt_25^0'=lt_25^post8, Result_4^0'=Result_4^post8, g_12^0'=g_12^post8, d_9^0'=d_9^post8, lt_22^0'=lt_22^post8, lt_17^0'=lt_17^post8, b_7^0'=b_7^post8, lt_19^0'=lt_19^post8, lt_14^0'=lt_14^post8, lt_24^0'=lt_24^post8, f_11^0'=f_11^post8, (lt_16^0-lt_16^post8 == 0 /\ e_10^0-e_10^post8 == 0 /\ -lt_19^post8+lt_19^0 == 0 /\ -lt_22^post8+lt_22^0 == 0 /\ -lt_15^post8+lt_15^0 == 0 /\ -g_12^post8+g_12^0 == 0 /\ -d_9^post8+d_9^0 == 0 /\ -lt_25^post8+lt_25^0 == 0 /\ lt_23^0-lt_23^post8 == 0 /\ -lt_24^post8+lt_24^0 == 0 /\ -b_7^post8+b_7^0 == 0 /\ h_13^0-h_13^post8 == 0 /\ cnt_38^0-cnt_38^post8 == 0 /\ Result_4^0-Result_4^post8 == 0 /\ lt_20^0-lt_20^post8 == 0 /\ a_6^0-a_6^post8 == 0 /\ -lt_17^post8+lt_17^0 == 0 /\ -f_11^post8+f_11^0 == 0 /\ x_5^0-x_5^post8 == 0 /\ c_8^0-c_8^post8 == 0 /\ -lt_14^post8+lt_14^0 == 0 /\ lt_18^0-lt_18^post8 == 0 /\ -lt_21^post8+lt_21^0 == 0), cost: 1
  10: l6 -> l3 : cnt_38^0'=cnt_38^post10, lt_21^0'=lt_21^post10, lt_16^0'=lt_16^post10, a_6^0'=a_6^post10, lt_18^0'=lt_18^post10, h_13^0'=h_13^post10, x_5^0'=x_5^post10, lt_23^0'=lt_23^post10, e_10^0'=e_10^post10, c_8^0'=c_8^post10, lt_20^0'=lt_20^post10, lt_15^0'=lt_15^post10, lt_25^0'=lt_25^post10, Result_4^0'=Result_4^post10, g_12^0'=g_12^post10, d_9^0'=d_9^post10, lt_22^0'=lt_22^post10, lt_17^0'=lt_17^post10, b_7^0'=b_7^post10, lt_19^0'=lt_19^post10, lt_14^0'=lt_14^post10, lt_24^0'=lt_24^post10, f_11^0'=f_11^post10, (Result_4^0-Result_4^post10 == 0 /\ x_5^0-x_5^post10 == 0 /\ c_8^0-c_8^post10 == 0 /\ h_13^0-h_13^post10 == 0 /\ cnt_38^0-cnt_38^post10 == 0 /\ lt_21^0-lt_21^post10 == 0 /\ -lt_24^post10+lt_24^0 == 0 /\ -f_11^post10+f_11^0 == 0 /\ -lt_17^post10+lt_17^0 == 0 /\ -lt_23^post10+lt_23^0 == 0 /\ e_10^0-e_10^post10 == 0 /\ -d_9^post10+d_9^0 == 0 /\ lt_18^0-lt_18^post10 == 0 /\ lt_20^0-lt_20^post10 == 0 /\ lt_22^0-lt_22^post10 == 0 /\ -lt_19^post10+lt_19^0 == 0 /\ lt_25^0-lt_25^post10 == 0 /\ -lt_15^post10+lt_15^0 == 0 /\ -g_12^post10+g_12^0 == 0 /\ -b_7^post10+b_7^0 == 0 /\ -a_6^post10+a_6^0 == 0 /\ -lt_14^post10+lt_14^0 == 0 /\ -lt_16^post10+lt_16^0 == 0), cost: 1
  12: l7 -> l3 : cnt_38^0'=cnt_38^post12, lt_21^0'=lt_21^post12, lt_16^0'=lt_16^post12, a_6^0'=a_6^post12, lt_18^0'=lt_18^post12, h_13^0'=h_13^post12, x_5^0'=x_5^post12, lt_23^0'=lt_23^post12, e_10^0'=e_10^post12, c_8^0'=c_8^post12, lt_20^0'=lt_20^post12, lt_15^0'=lt_15^post12, lt_25^0'=lt_25^post12, Result_4^0'=Result_4^post12, g_12^0'=g_12^post12, d_9^0'=d_9^post12, lt_22^0'=lt_22^post12, lt_17^0'=lt_17^post12, b_7^0'=b_7^post12, lt_19^0'=lt_19^post12, lt_14^0'=lt_14^post12, lt_24^0'=lt_24^post12, f_11^0'=f_11^post12, (-lt_18^post12+lt_18^0 == 0 /\ -Result_4^post12+Result_4^0 == 0 /\ -lt_19^post12+lt_19^0 == 0 /\ -b_7^post12+b_7^0 == 0 /\ lt_20^0-lt_20^post12 == 0 /\ -lt_15^post12+lt_15^0 == 0 /\ -lt_14^post12+lt_14^0 == 0 /\ x_5^0-x_5^post12 == 0 /\ -lt_25^post12+lt_25^0 == 0 /\ -c_8^post12+c_8^0 == 0 /\ lt_21^0-lt_21^post12 == 0 /\ cnt_38^0-cnt_38^post12 == 0 /\ lt_16^0-lt_16^post12 == 0 /\ a_6^0-a_6^post12 == 0 /\ -lt_22^post12+lt_22^0 == 0 /\ lt_23^0-lt_23^post12 == 0 /\ lt_24^0-lt_24^post12 == 0 /\ e_10^0-e_10^post12 == 0 /\ -d_9^post12+d_9^0 == 0 /\ -g_12^post12+g_12^0 == 0 /\ lt_17^0-lt_17^post12 == 0 /\ h_13^0-h_13^post12 == 0 /\ -f_11^post12+f_11^0 == 0), cost: 1
  13: l8 -> l2 : cnt_38^0'=cnt_38^post13, lt_21^0'=lt_21^post13, lt_16^0'=lt_16^post13, a_6^0'=a_6^post13, lt_18^0'=lt_18^post13, h_13^0'=h_13^post13, x_5^0'=x_5^post13, lt_23^0'=lt_23^post13, e_10^0'=e_10^post13, c_8^0'=c_8^post13, lt_20^0'=lt_20^post13, lt_15^0'=lt_15^post13, lt_25^0'=lt_25^post13, Result_4^0'=Result_4^post13, g_12^0'=g_12^post13, d_9^0'=d_9^post13, lt_22^0'=lt_22^post13, lt_17^0'=lt_17^post13, b_7^0'=b_7^post13, lt_19^0'=lt_19^post13, lt_14^0'=lt_14^post13, lt_24^0'=lt_24^post13, f_11^0'=f_11^post13, (e_10^0-e_10^post13 == 0 /\ -lt_22^post13+lt_22^0 == 0 /\ lt_23^0-lt_23^post13 == 0 /\ lt_14^0-lt_14^post13 == 0 /\ -lt_18^post13+lt_18^0 == 0 /\ -lt_19^post13+lt_19^0 == 0 /\ -lt_25^post13+lt_25^0 == 0 /\ -b_7^post13+b_7^0 == 0 /\ -g_12^post13+g_12^0 == 0 /\ lt_21^0-lt_21^post13 == 0 /\ lt_16^0-lt_16^post13 == 0 /\ x_5^0-x_5^post13 == 0 /\ -d_9^post13+d_9^0 == 0 /\ cnt_38^0-cnt_38^post13 == 0 /\ c_8^0-c_8^post13 == 0 /\ lt_20^0-lt_20^post13 == 0 /\ lt_24^0-lt_24^post13 == 0 /\ Result_4^0-Result_4^post13 == 0 /\ a_6^0-a_6^post13 == 0 /\ -lt_17^post13+lt_17^0 == 0 /\ -f_11^post13+f_11^0 == 0 /\ -lt_15^post13+lt_15^0 == 0 /\ h_13^0-h_13^post13 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l8
   1: l2 -> l3 : cnt_38^0'=cnt_38^post1, lt_21^0'=lt_21^post1, lt_16^0'=lt_16^post1, a_6^0'=a_6^post1, lt_18^0'=lt_18^post1, h_13^0'=h_13^post1, x_5^0'=x_5^post1, lt_23^0'=lt_23^post1, e_10^0'=e_10^post1, c_8^0'=c_8^post1, lt_20^0'=lt_20^post1, lt_15^0'=lt_15^post1, lt_25^0'=lt_25^post1, Result_4^0'=Result_4^post1, g_12^0'=g_12^post1, d_9^0'=d_9^post1, lt_22^0'=lt_22^post1, lt_17^0'=lt_17^post1, b_7^0'=b_7^post1, lt_19^0'=lt_19^post1, lt_14^0'=lt_14^post1, lt_24^0'=lt_24^post1, f_11^0'=f_11^post1, (0 == 0 /\ lt_15^0-lt_15^post1 == 0 /\ -lt_24^post1+lt_24^0 == 0 /\ lt_23^0-lt_23^post1 == 0 /\ e_10^post1-d_9^post1 == 0 /\ lt_25^0-lt_25^post1 == 0 /\ cnt_38^0-cnt_38^post1 == 0 /\ lt_16^0-lt_16^post1 == 0 /\ -x_5^post1+a_6^post1 == 0 /\ -lt_22^post1+lt_22^0 == 0 /\ -b_7^post1+c_8^post1 == 0 /\ -Result_4^post1+Result_4^0 == 0 /\ d_9^post1-c_8^post1 == 0 /\ h_13^post1-g_12^post1 == 0 /\ lt_21^0-lt_21^post1 == 0 /\ -lt_17^post1+lt_17^0 == 0 /\ -lt_14^post1+lt_14^0 == 0 /\ -e_10^post1+f_11^post1 == 0 /\ lt_18^0-lt_18^post1 == 0 /\ -lt_20^post1+lt_20^0 == 0 /\ -lt_19^post1+lt_19^0 == 0 /\ -f_11^post1+g_12^post1 == 0 /\ -a_6^post1+b_7^post1 == 0), cost: 1
   5: l3 -> l4 : cnt_38^0'=cnt_38^post5, lt_21^0'=lt_21^post5, lt_16^0'=lt_16^post5, a_6^0'=a_6^post5, lt_18^0'=lt_18^post5, h_13^0'=h_13^post5, x_5^0'=x_5^post5, lt_23^0'=lt_23^post5, e_10^0'=e_10^post5, c_8^0'=c_8^post5, lt_20^0'=lt_20^post5, lt_15^0'=lt_15^post5, lt_25^0'=lt_25^post5, Result_4^0'=Result_4^post5, g_12^0'=g_12^post5, d_9^0'=d_9^post5, lt_22^0'=lt_22^post5, lt_17^0'=lt_17^post5, b_7^0'=b_7^post5, lt_19^0'=lt_19^post5, lt_14^0'=lt_14^post5, lt_24^0'=lt_24^post5, f_11^0'=f_11^post5, (0 == 0 /\ -lt_20^post5+lt_20^0 == 0 /\ -a_6^post5+a_6^0 == 0 /\ -cnt_38^0+lt_23^110 == 0 /\ -lt_14^post5+lt_14^0 == 0 /\ x_5^0-x_5^post5 == 0 /\ -d_9^post5+d_9^0 == 0 /\ -e_10^post5+e_10^0 == 0 /\ -lt_19^120 <= 0 /\ c_8^0-c_8^post5 == 0 /\ Result_4^0-Result_4^post5 == 0 /\ -lt_25^130 <= 0 /\ -cnt_38^0+lt_24^120 == 0 /\ cnt_38^0-cnt_38^post5 == 0 /\ -cnt_38^0+lt_25^130 == 0 /\ 1-lt_24^120 <= 0 /\ -g_12^post5+g_12^0 == 0 /\ lt_21^0-lt_21^post5 == 0 /\ -f_11^post5+f_11^0 == 0 /\ 1-lt_18^120 <= 0 /\ -b_7^post5+b_7^0 == 0 /\ h_13^0-h_13^post5 == 0 /\ -lt_15^post5+lt_15^0 == 0), cost: 1
   7: l3 -> l5 : cnt_38^0'=cnt_38^post7, lt_21^0'=lt_21^post7, lt_16^0'=lt_16^post7, a_6^0'=a_6^post7, lt_18^0'=lt_18^post7, h_13^0'=h_13^post7, x_5^0'=x_5^post7, lt_23^0'=lt_23^post7, e_10^0'=e_10^post7, c_8^0'=c_8^post7, lt_20^0'=lt_20^post7, lt_15^0'=lt_15^post7, lt_25^0'=lt_25^post7, Result_4^0'=Result_4^post7, g_12^0'=g_12^post7, d_9^0'=d_9^post7, lt_22^0'=lt_22^post7, lt_17^0'=lt_17^post7, b_7^0'=b_7^post7, lt_19^0'=lt_19^post7, lt_14^0'=lt_14^post7, lt_24^0'=lt_24^post7, f_11^0'=f_11^post7, (0 == 0 /\ lt_18^0-lt_18^post7 == 0 /\ a_6^0-a_6^post7 == 0 /\ x_5^0-x_5^post7 == 0 /\ e_10^0-e_10^post7 == 0 /\ -cnt_38^0+lt_25^140 == 0 /\ -lt_25^140 <= 0 /\ -b_7^post7+b_7^0 == 0 /\ lt_21^0-lt_21^post7 == 0 /\ 1+lt_19^130 <= 0 /\ lt_16^0-lt_16^post7 == 0 /\ cnt_38^0-cnt_38^post7 == 0 /\ -g_12^post7+g_12^0 == 0 /\ Result_4^0-Result_4^post7 == 0 /\ lt_17^0-lt_17^post7 == 0 /\ -cnt_38^0+lt_23^120 == 0 /\ c_8^0-c_8^post7 == 0 /\ -d_9^post7+d_9^0 == 0 /\ -lt_20^post7+lt_20^0 == 0 /\ h_13^0-h_13^post7 == 0 /\ -cnt_38^0+lt_24^130 == 0 /\ -f_11^post7+f_11^0 == 0 /\ 1-lt_24^130 <= 0), cost: 1
   9: l3 -> l6 : cnt_38^0'=cnt_38^post9, lt_21^0'=lt_21^post9, lt_16^0'=lt_16^post9, a_6^0'=a_6^post9, lt_18^0'=lt_18^post9, h_13^0'=h_13^post9, x_5^0'=x_5^post9, lt_23^0'=lt_23^post9, e_10^0'=e_10^post9, c_8^0'=c_8^post9, lt_20^0'=lt_20^post9, lt_15^0'=lt_15^post9, lt_25^0'=lt_25^post9, Result_4^0'=Result_4^post9, g_12^0'=g_12^post9, d_9^0'=d_9^post9, lt_22^0'=lt_22^post9, lt_17^0'=lt_17^post9, b_7^0'=b_7^post9, lt_19^0'=lt_19^post9, lt_14^0'=lt_14^post9, lt_24^0'=lt_24^post9, f_11^0'=f_11^post9, (0 == 0 /\ Result_4^0-Result_4^post9 == 0 /\ -f_11^post9+f_11^0 == 0 /\ b_7^0-b_7^post9 == 0 /\ lt_15^0-lt_15^post9 == 0 /\ g_12^0-g_12^post9 == 0 /\ cnt_38^0-cnt_38^post9 == 0 /\ -lt_23^post9+lt_23^0 == 0 /\ 1+lt_25^150 <= 0 /\ -d_9^post9+d_9^0 == 0 /\ -x_5^post9+x_5^0 == 0 /\ a_6^0-a_6^post9 == 0 /\ 1-lt_18^130 <= 0 /\ -lt_24^post9+lt_24^0 == 0 /\ h_13^0-h_13^post9 == 0 /\ -cnt_38^0+lt_25^150 == 0 /\ -c_8^post9+c_8^0 == 0 /\ -lt_14^post9+lt_14^0 == 0 /\ -cnt_38^0+lt_21^110 == 0 /\ -lt_19^140 <= 0 /\ lt_22^0-lt_22^post9 == 0 /\ e_10^0-e_10^post9 == 0), cost: 1
  11: l3 -> l7 : cnt_38^0'=cnt_38^post11, lt_21^0'=lt_21^post11, lt_16^0'=lt_16^post11, a_6^0'=a_6^post11, lt_18^0'=lt_18^post11, h_13^0'=h_13^post11, x_5^0'=x_5^post11, lt_23^0'=lt_23^post11, e_10^0'=e_10^post11, c_8^0'=c_8^post11, lt_20^0'=lt_20^post11, lt_15^0'=lt_15^post11, lt_25^0'=lt_25^post11, Result_4^0'=Result_4^post11, g_12^0'=g_12^post11, d_9^0'=d_9^post11, lt_22^0'=lt_22^post11, lt_17^0'=lt_17^post11, b_7^0'=b_7^post11, lt_19^0'=lt_19^post11, lt_14^0'=lt_14^post11, lt_24^0'=lt_24^post11, f_11^0'=f_11^post11, (0 == 0 /\ -f_11^post11+f_11^0 == 0 /\ -lt_17^post11+lt_17^0 == 0 /\ -e_10^post11+e_10^0 == 0 /\ -b_7^post11+b_7^0 == 0 /\ g_12^0-g_12^post11 == 0 /\ -lt_18^post11+lt_18^0 == 0 /\ 1+lt_19^150 <= 0 /\ lt_16^0-lt_16^post11 == 0 /\ -lt_22^post11+lt_22^0 == 0 /\ 1+lt_25^160 <= 0 /\ -lt_24^post11+lt_24^0 == 0 /\ x_5^0-x_5^post11 == 0 /\ a_6^0-a_6^post11 == 0 /\ lt_23^0-lt_23^post11 == 0 /\ -cnt_38^0+lt_21^120 == 0 /\ -Result_4^post11+Result_4^0 == 0 /\ h_13^0-h_13^post11 == 0 /\ -cnt_38^0+lt_25^160 == 0 /\ cnt_38^0-cnt_38^post11 == 0 /\ -c_8^post11+c_8^0 == 0 /\ d_9^0-d_9^post11 == 0), cost: 1
   6: l4 -> l3 : cnt_38^0'=cnt_38^post6, lt_21^0'=lt_21^post6, lt_16^0'=lt_16^post6, a_6^0'=a_6^post6, lt_18^0'=lt_18^post6, h_13^0'=h_13^post6, x_5^0'=x_5^post6, lt_23^0'=lt_23^post6, e_10^0'=e_10^post6, c_8^0'=c_8^post6, lt_20^0'=lt_20^post6, lt_15^0'=lt_15^post6, lt_25^0'=lt_25^post6, Result_4^0'=Result_4^post6, g_12^0'=g_12^post6, d_9^0'=d_9^post6, lt_22^0'=lt_22^post6, lt_17^0'=lt_17^post6, b_7^0'=b_7^post6, lt_19^0'=lt_19^post6, lt_14^0'=lt_14^post6, lt_24^0'=lt_24^post6, f_11^0'=f_11^post6, (lt_20^0-lt_20^post6 == 0 /\ h_13^0-h_13^post6 == 0 /\ -lt_18^post6+lt_18^0 == 0 /\ lt_14^0-lt_14^post6 == 0 /\ -lt_19^post6+lt_19^0 == 0 /\ -b_7^post6+b_7^0 == 0 /\ -c_8^post6+c_8^0 == 0 /\ -lt_15^post6+lt_15^0 == 0 /\ -lt_25^post6+lt_25^0 == 0 /\ x_5^0-x_5^post6 == 0 /\ -f_11^post6+f_11^0 == 0 /\ lt_21^0-lt_21^post6 == 0 /\ -lt_22^post6+lt_22^0 == 0 /\ lt_16^0-lt_16^post6 == 0 /\ a_6^0-a_6^post6 == 0 /\ cnt_38^0-cnt_38^post6 == 0 /\ -d_9^post6+d_9^0 == 0 /\ lt_17^0-lt_17^post6 == 0 /\ lt_23^0-lt_23^post6 == 0 /\ lt_24^0-lt_24^post6 == 0 /\ e_10^0-e_10^post6 == 0 /\ -g_12^post6+g_12^0 == 0 /\ Result_4^0-Result_4^post6 == 0), cost: 1
   8: l5 -> l3 : cnt_38^0'=cnt_38^post8, lt_21^0'=lt_21^post8, lt_16^0'=lt_16^post8, a_6^0'=a_6^post8, lt_18^0'=lt_18^post8, h_13^0'=h_13^post8, x_5^0'=x_5^post8, lt_23^0'=lt_23^post8, e_10^0'=e_10^post8, c_8^0'=c_8^post8, lt_20^0'=lt_20^post8, lt_15^0'=lt_15^post8, lt_25^0'=lt_25^post8, Result_4^0'=Result_4^post8, g_12^0'=g_12^post8, d_9^0'=d_9^post8, lt_22^0'=lt_22^post8, lt_17^0'=lt_17^post8, b_7^0'=b_7^post8, lt_19^0'=lt_19^post8, lt_14^0'=lt_14^post8, lt_24^0'=lt_24^post8, f_11^0'=f_11^post8, (lt_16^0-lt_16^post8 == 0 /\ e_10^0-e_10^post8 == 0 /\ -lt_19^post8+lt_19^0 == 0 /\ -lt_22^post8+lt_22^0 == 0 /\ -lt_15^post8+lt_15^0 == 0 /\ -g_12^post8+g_12^0 == 0 /\ -d_9^post8+d_9^0 == 0 /\ -lt_25^post8+lt_25^0 == 0 /\ lt_23^0-lt_23^post8 == 0 /\ -lt_24^post8+lt_24^0 == 0 /\ -b_7^post8+b_7^0 == 0 /\ h_13^0-h_13^post8 == 0 /\ cnt_38^0-cnt_38^post8 == 0 /\ Result_4^0-Result_4^post8 == 0 /\ lt_20^0-lt_20^post8 == 0 /\ a_6^0-a_6^post8 == 0 /\ -lt_17^post8+lt_17^0 == 0 /\ -f_11^post8+f_11^0 == 0 /\ x_5^0-x_5^post8 == 0 /\ c_8^0-c_8^post8 == 0 /\ -lt_14^post8+lt_14^0 == 0 /\ lt_18^0-lt_18^post8 == 0 /\ -lt_21^post8+lt_21^0 == 0), cost: 1
  10: l6 -> l3 : cnt_38^0'=cnt_38^post10, lt_21^0'=lt_21^post10, lt_16^0'=lt_16^post10, a_6^0'=a_6^post10, lt_18^0'=lt_18^post10, h_13^0'=h_13^post10, x_5^0'=x_5^post10, lt_23^0'=lt_23^post10, e_10^0'=e_10^post10, c_8^0'=c_8^post10, lt_20^0'=lt_20^post10, lt_15^0'=lt_15^post10, lt_25^0'=lt_25^post10, Result_4^0'=Result_4^post10, g_12^0'=g_12^post10, d_9^0'=d_9^post10, lt_22^0'=lt_22^post10, lt_17^0'=lt_17^post10, b_7^0'=b_7^post10, lt_19^0'=lt_19^post10, lt_14^0'=lt_14^post10, lt_24^0'=lt_24^post10, f_11^0'=f_11^post10, (Result_4^0-Result_4^post10 == 0 /\ x_5^0-x_5^post10 == 0 /\ c_8^0-c_8^post10 == 0 /\ h_13^0-h_13^post10 == 0 /\ cnt_38^0-cnt_38^post10 == 0 /\ lt_21^0-lt_21^post10 == 0 /\ -lt_24^post10+lt_24^0 == 0 /\ -f_11^post10+f_11^0 == 0 /\ -lt_17^post10+lt_17^0 == 0 /\ -lt_23^post10+lt_23^0 == 0 /\ e_10^0-e_10^post10 == 0 /\ -d_9^post10+d_9^0 == 0 /\ lt_18^0-lt_18^post10 == 0 /\ lt_20^0-lt_20^post10 == 0 /\ lt_22^0-lt_22^post10 == 0 /\ -lt_19^post10+lt_19^0 == 0 /\ lt_25^0-lt_25^post10 == 0 /\ -lt_15^post10+lt_15^0 == 0 /\ -g_12^post10+g_12^0 == 0 /\ -b_7^post10+b_7^0 == 0 /\ -a_6^post10+a_6^0 == 0 /\ -lt_14^post10+lt_14^0 == 0 /\ -lt_16^post10+lt_16^0 == 0), cost: 1
  12: l7 -> l3 : cnt_38^0'=cnt_38^post12, lt_21^0'=lt_21^post12, lt_16^0'=lt_16^post12, a_6^0'=a_6^post12, lt_18^0'=lt_18^post12, h_13^0'=h_13^post12, x_5^0'=x_5^post12, lt_23^0'=lt_23^post12, e_10^0'=e_10^post12, c_8^0'=c_8^post12, lt_20^0'=lt_20^post12, lt_15^0'=lt_15^post12, lt_25^0'=lt_25^post12, Result_4^0'=Result_4^post12, g_12^0'=g_12^post12, d_9^0'=d_9^post12, lt_22^0'=lt_22^post12, lt_17^0'=lt_17^post12, b_7^0'=b_7^post12, lt_19^0'=lt_19^post12, lt_14^0'=lt_14^post12, lt_24^0'=lt_24^post12, f_11^0'=f_11^post12, (-lt_18^post12+lt_18^0 == 0 /\ -Result_4^post12+Result_4^0 == 0 /\ -lt_19^post12+lt_19^0 == 0 /\ -b_7^post12+b_7^0 == 0 /\ lt_20^0-lt_20^post12 == 0 /\ -lt_15^post12+lt_15^0 == 0 /\ -lt_14^post12+lt_14^0 == 0 /\ x_5^0-x_5^post12 == 0 /\ -lt_25^post12+lt_25^0 == 0 /\ -c_8^post12+c_8^0 == 0 /\ lt_21^0-lt_21^post12 == 0 /\ cnt_38^0-cnt_38^post12 == 0 /\ lt_16^0-lt_16^post12 == 0 /\ a_6^0-a_6^post12 == 0 /\ -lt_22^post12+lt_22^0 == 0 /\ lt_23^0-lt_23^post12 == 0 /\ lt_24^0-lt_24^post12 == 0 /\ e_10^0-e_10^post12 == 0 /\ -d_9^post12+d_9^0 == 0 /\ -g_12^post12+g_12^0 == 0 /\ lt_17^0-lt_17^post12 == 0 /\ h_13^0-h_13^post12 == 0 /\ -f_11^post12+f_11^0 == 0), cost: 1
  13: l8 -> l2 : cnt_38^0'=cnt_38^post13, lt_21^0'=lt_21^post13, lt_16^0'=lt_16^post13, a_6^0'=a_6^post13, lt_18^0'=lt_18^post13, h_13^0'=h_13^post13, x_5^0'=x_5^post13, lt_23^0'=lt_23^post13, e_10^0'=e_10^post13, c_8^0'=c_8^post13, lt_20^0'=lt_20^post13, lt_15^0'=lt_15^post13, lt_25^0'=lt_25^post13, Result_4^0'=Result_4^post13, g_12^0'=g_12^post13, d_9^0'=d_9^post13, lt_22^0'=lt_22^post13, lt_17^0'=lt_17^post13, b_7^0'=b_7^post13, lt_19^0'=lt_19^post13, lt_14^0'=lt_14^post13, lt_24^0'=lt_24^post13, f_11^0'=f_11^post13, (e_10^0-e_10^post13 == 0 /\ -lt_22^post13+lt_22^0 == 0 /\ lt_23^0-lt_23^post13 == 0 /\ lt_14^0-lt_14^post13 == 0 /\ -lt_18^post13+lt_18^0 == 0 /\ -lt_19^post13+lt_19^0 == 0 /\ -lt_25^post13+lt_25^0 == 0 /\ -b_7^post13+b_7^0 == 0 /\ -g_12^post13+g_12^0 == 0 /\ lt_21^0-lt_21^post13 == 0 /\ lt_16^0-lt_16^post13 == 0 /\ x_5^0-x_5^post13 == 0 /\ -d_9^post13+d_9^0 == 0 /\ cnt_38^0-cnt_38^post13 == 0 /\ c_8^0-c_8^post13 == 0 /\ lt_20^0-lt_20^post13 == 0 /\ lt_24^0-lt_24^post13 == 0 /\ Result_4^0-Result_4^post13 == 0 /\ a_6^0-a_6^post13 == 0 /\ -lt_17^post13+lt_17^0 == 0 /\ -f_11^post13+f_11^0 == 0 /\ -lt_15^post13+lt_15^0 == 0 /\ h_13^0-h_13^post13 == 0), cost: 1


Applied preprocessing
Original rule:
l2 -> l3 : cnt_38^0'=cnt_38^post1, lt_21^0'=lt_21^post1, lt_16^0'=lt_16^post1, a_6^0'=a_6^post1, lt_18^0'=lt_18^post1, h_13^0'=h_13^post1, x_5^0'=x_5^post1, lt_23^0'=lt_23^post1, e_10^0'=e_10^post1, c_8^0'=c_8^post1, lt_20^0'=lt_20^post1, lt_15^0'=lt_15^post1, lt_25^0'=lt_25^post1, Result_4^0'=Result_4^post1, g_12^0'=g_12^post1, d_9^0'=d_9^post1, lt_22^0'=lt_22^post1, lt_17^0'=lt_17^post1, b_7^0'=b_7^post1, lt_19^0'=lt_19^post1, lt_14^0'=lt_14^post1, lt_24^0'=lt_24^post1, f_11^0'=f_11^post1, (0 == 0 /\ lt_15^0-lt_15^post1 == 0 /\ -lt_24^post1+lt_24^0 == 0 /\ lt_23^0-lt_23^post1 == 0 /\ e_10^post1-d_9^post1 == 0 /\ lt_25^0-lt_25^post1 == 0 /\ cnt_38^0-cnt_38^post1 == 0 /\ lt_16^0-lt_16^post1 == 0 /\ -x_5^post1+a_6^post1 == 0 /\ -lt_22^post1+lt_22^0 == 0 /\ -b_7^post1+c_8^post1 == 0 /\ -Result_4^post1+Result_4^0 == 0 /\ d_9^post1-c_8^post1 == 0 /\ h_13^post1-g_12^post1 == 0 /\ lt_21^0-lt_21^post1 == 0 /\ -lt_17^post1+lt_17^0 == 0 /\ -lt_14^post1+lt_14^0 == 0 /\ -e_10^post1+f_11^post1 == 0 /\ lt_18^0-lt_18^post1 == 0 /\ -lt_20^post1+lt_20^0 == 0 /\ -lt_19^post1+lt_19^0 == 0 /\ -f_11^post1+g_12^post1 == 0 /\ -a_6^post1+b_7^post1 == 0), cost: 1
New rule:
l2 -> l3 : a_6^0'=c_8^post1, h_13^0'=c_8^post1, x_5^0'=c_8^post1, e_10^0'=c_8^post1, c_8^0'=c_8^post1, g_12^0'=c_8^post1, d_9^0'=c_8^post1, b_7^0'=c_8^post1, f_11^0'=c_8^post1, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l3 -> l4 : cnt_38^0'=cnt_38^post5, lt_21^0'=lt_21^post5, lt_16^0'=lt_16^post5, a_6^0'=a_6^post5, lt_18^0'=lt_18^post5, h_13^0'=h_13^post5, x_5^0'=x_5^post5, lt_23^0'=lt_23^post5, e_10^0'=e_10^post5, c_8^0'=c_8^post5, lt_20^0'=lt_20^post5, lt_15^0'=lt_15^post5, lt_25^0'=lt_25^post5, Result_4^0'=Result_4^post5, g_12^0'=g_12^post5, d_9^0'=d_9^post5, lt_22^0'=lt_22^post5, lt_17^0'=lt_17^post5, b_7^0'=b_7^post5, lt_19^0'=lt_19^post5, lt_14^0'=lt_14^post5, lt_24^0'=lt_24^post5, f_11^0'=f_11^post5, (0 == 0 /\ -lt_20^post5+lt_20^0 == 0 /\ -a_6^post5+a_6^0 == 0 /\ -cnt_38^0+lt_23^110 == 0 /\ -lt_14^post5+lt_14^0 == 0 /\ x_5^0-x_5^post5 == 0 /\ -d_9^post5+d_9^0 == 0 /\ -e_10^post5+e_10^0 == 0 /\ -lt_19^120 <= 0 /\ c_8^0-c_8^post5 == 0 /\ Result_4^0-Result_4^post5 == 0 /\ -lt_25^130 <= 0 /\ -cnt_38^0+lt_24^120 == 0 /\ cnt_38^0-cnt_38^post5 == 0 /\ -cnt_38^0+lt_25^130 == 0 /\ 1-lt_24^120 <= 0 /\ -g_12^post5+g_12^0 == 0 /\ lt_21^0-lt_21^post5 == 0 /\ -f_11^post5+f_11^0 == 0 /\ 1-lt_18^120 <= 0 /\ -b_7^post5+b_7^0 == 0 /\ h_13^0-h_13^post5 == 0 /\ -lt_15^post5+lt_15^0 == 0), cost: 1
New rule:
l3 -> l4 : lt_16^0'=lt_16^post5, lt_18^0'=lt_18^post5, lt_23^0'=lt_23^post5, lt_25^0'=lt_25^post5, lt_22^0'=lt_22^post5, lt_17^0'=lt_17^post5, lt_19^0'=lt_19^post5, lt_24^0'=lt_24^post5, -1+cnt_38^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l4 -> l3 : cnt_38^0'=cnt_38^post6, lt_21^0'=lt_21^post6, lt_16^0'=lt_16^post6, a_6^0'=a_6^post6, lt_18^0'=lt_18^post6, h_13^0'=h_13^post6, x_5^0'=x_5^post6, lt_23^0'=lt_23^post6, e_10^0'=e_10^post6, c_8^0'=c_8^post6, lt_20^0'=lt_20^post6, lt_15^0'=lt_15^post6, lt_25^0'=lt_25^post6, Result_4^0'=Result_4^post6, g_12^0'=g_12^post6, d_9^0'=d_9^post6, lt_22^0'=lt_22^post6, lt_17^0'=lt_17^post6, b_7^0'=b_7^post6, lt_19^0'=lt_19^post6, lt_14^0'=lt_14^post6, lt_24^0'=lt_24^post6, f_11^0'=f_11^post6, (lt_20^0-lt_20^post6 == 0 /\ h_13^0-h_13^post6 == 0 /\ -lt_18^post6+lt_18^0 == 0 /\ lt_14^0-lt_14^post6 == 0 /\ -lt_19^post6+lt_19^0 == 0 /\ -b_7^post6+b_7^0 == 0 /\ -c_8^post6+c_8^0 == 0 /\ -lt_15^post6+lt_15^0 == 0 /\ -lt_25^post6+lt_25^0 == 0 /\ x_5^0-x_5^post6 == 0 /\ -f_11^post6+f_11^0 == 0 /\ lt_21^0-lt_21^post6 == 0 /\ -lt_22^post6+lt_22^0 == 0 /\ lt_16^0-lt_16^post6 == 0 /\ a_6^0-a_6^post6 == 0 /\ cnt_38^0-cnt_38^post6 == 0 /\ -d_9^post6+d_9^0 == 0 /\ lt_17^0-lt_17^post6 == 0 /\ lt_23^0-lt_23^post6 == 0 /\ lt_24^0-lt_24^post6 == 0 /\ e_10^0-e_10^post6 == 0 /\ -g_12^post6+g_12^0 == 0 /\ Result_4^0-Result_4^post6 == 0), cost: 1
New rule:
l4 -> l3 : TRUE, cost: 1

Applied preprocessing
Original rule:
l3 -> l5 : cnt_38^0'=cnt_38^post7, lt_21^0'=lt_21^post7, lt_16^0'=lt_16^post7, a_6^0'=a_6^post7, lt_18^0'=lt_18^post7, h_13^0'=h_13^post7, x_5^0'=x_5^post7, lt_23^0'=lt_23^post7, e_10^0'=e_10^post7, c_8^0'=c_8^post7, lt_20^0'=lt_20^post7, lt_15^0'=lt_15^post7, lt_25^0'=lt_25^post7, Result_4^0'=Result_4^post7, g_12^0'=g_12^post7, d_9^0'=d_9^post7, lt_22^0'=lt_22^post7, lt_17^0'=lt_17^post7, b_7^0'=b_7^post7, lt_19^0'=lt_19^post7, lt_14^0'=lt_14^post7, lt_24^0'=lt_24^post7, f_11^0'=f_11^post7, (0 == 0 /\ lt_18^0-lt_18^post7 == 0 /\ a_6^0-a_6^post7 == 0 /\ x_5^0-x_5^post7 == 0 /\ e_10^0-e_10^post7 == 0 /\ -cnt_38^0+lt_25^140 == 0 /\ -lt_25^140 <= 0 /\ -b_7^post7+b_7^0 == 0 /\ lt_21^0-lt_21^post7 == 0 /\ 1+lt_19^130 <= 0 /\ lt_16^0-lt_16^post7 == 0 /\ cnt_38^0-cnt_38^post7 == 0 /\ -g_12^post7+g_12^0 == 0 /\ Result_4^0-Result_4^post7 == 0 /\ lt_17^0-lt_17^post7 == 0 /\ -cnt_38^0+lt_23^120 == 0 /\ c_8^0-c_8^post7 == 0 /\ -d_9^post7+d_9^0 == 0 /\ -lt_20^post7+lt_20^0 == 0 /\ h_13^0-h_13^post7 == 0 /\ -cnt_38^0+lt_24^130 == 0 /\ -f_11^post7+f_11^0 == 0 /\ 1-lt_24^130 <= 0), cost: 1
New rule:
l3 -> l5 : lt_23^0'=lt_23^post7, lt_15^0'=lt_15^post7, lt_25^0'=lt_25^post7, lt_22^0'=lt_22^post7, lt_19^0'=lt_19^post7, lt_14^0'=lt_14^post7, lt_24^0'=lt_24^post7, -1+cnt_38^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l5 -> l3 : cnt_38^0'=cnt_38^post8, lt_21^0'=lt_21^post8, lt_16^0'=lt_16^post8, a_6^0'=a_6^post8, lt_18^0'=lt_18^post8, h_13^0'=h_13^post8, x_5^0'=x_5^post8, lt_23^0'=lt_23^post8, e_10^0'=e_10^post8, c_8^0'=c_8^post8, lt_20^0'=lt_20^post8, lt_15^0'=lt_15^post8, lt_25^0'=lt_25^post8, Result_4^0'=Result_4^post8, g_12^0'=g_12^post8, d_9^0'=d_9^post8, lt_22^0'=lt_22^post8, lt_17^0'=lt_17^post8, b_7^0'=b_7^post8, lt_19^0'=lt_19^post8, lt_14^0'=lt_14^post8, lt_24^0'=lt_24^post8, f_11^0'=f_11^post8, (lt_16^0-lt_16^post8 == 0 /\ e_10^0-e_10^post8 == 0 /\ -lt_19^post8+lt_19^0 == 0 /\ -lt_22^post8+lt_22^0 == 0 /\ -lt_15^post8+lt_15^0 == 0 /\ -g_12^post8+g_12^0 == 0 /\ -d_9^post8+d_9^0 == 0 /\ -lt_25^post8+lt_25^0 == 0 /\ lt_23^0-lt_23^post8 == 0 /\ -lt_24^post8+lt_24^0 == 0 /\ -b_7^post8+b_7^0 == 0 /\ h_13^0-h_13^post8 == 0 /\ cnt_38^0-cnt_38^post8 == 0 /\ Result_4^0-Result_4^post8 == 0 /\ lt_20^0-lt_20^post8 == 0 /\ a_6^0-a_6^post8 == 0 /\ -lt_17^post8+lt_17^0 == 0 /\ -f_11^post8+f_11^0 == 0 /\ x_5^0-x_5^post8 == 0 /\ c_8^0-c_8^post8 == 0 /\ -lt_14^post8+lt_14^0 == 0 /\ lt_18^0-lt_18^post8 == 0 /\ -lt_21^post8+lt_21^0 == 0), cost: 1
New rule:
l5 -> l3 : TRUE, cost: 1

Applied preprocessing
Original rule:
l3 -> l6 : cnt_38^0'=cnt_38^post9, lt_21^0'=lt_21^post9, lt_16^0'=lt_16^post9, a_6^0'=a_6^post9, lt_18^0'=lt_18^post9, h_13^0'=h_13^post9, x_5^0'=x_5^post9, lt_23^0'=lt_23^post9, e_10^0'=e_10^post9, c_8^0'=c_8^post9, lt_20^0'=lt_20^post9, lt_15^0'=lt_15^post9, lt_25^0'=lt_25^post9, Result_4^0'=Result_4^post9, g_12^0'=g_12^post9, d_9^0'=d_9^post9, lt_22^0'=lt_22^post9, lt_17^0'=lt_17^post9, b_7^0'=b_7^post9, lt_19^0'=lt_19^post9, lt_14^0'=lt_14^post9, lt_24^0'=lt_24^post9, f_11^0'=f_11^post9, (0 == 0 /\ Result_4^0-Result_4^post9 == 0 /\ -f_11^post9+f_11^0 == 0 /\ b_7^0-b_7^post9 == 0 /\ lt_15^0-lt_15^post9 == 0 /\ g_12^0-g_12^post9 == 0 /\ cnt_38^0-cnt_38^post9 == 0 /\ -lt_23^post9+lt_23^0 == 0 /\ 1+lt_25^150 <= 0 /\ -d_9^post9+d_9^0 == 0 /\ -x_5^post9+x_5^0 == 0 /\ a_6^0-a_6^post9 == 0 /\ 1-lt_18^130 <= 0 /\ -lt_24^post9+lt_24^0 == 0 /\ h_13^0-h_13^post9 == 0 /\ -cnt_38^0+lt_25^150 == 0 /\ -c_8^post9+c_8^0 == 0 /\ -lt_14^post9+lt_14^0 == 0 /\ -cnt_38^0+lt_21^110 == 0 /\ -lt_19^140 <= 0 /\ lt_22^0-lt_22^post9 == 0 /\ e_10^0-e_10^post9 == 0), cost: 1
New rule:
l3 -> l6 : lt_21^0'=lt_21^post9, lt_16^0'=lt_16^post9, lt_18^0'=lt_18^post9, lt_20^0'=lt_20^post9, lt_25^0'=lt_25^post9, lt_17^0'=lt_17^post9, lt_19^0'=lt_19^post9, 1+cnt_38^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l6 -> l3 : cnt_38^0'=cnt_38^post10, lt_21^0'=lt_21^post10, lt_16^0'=lt_16^post10, a_6^0'=a_6^post10, lt_18^0'=lt_18^post10, h_13^0'=h_13^post10, x_5^0'=x_5^post10, lt_23^0'=lt_23^post10, e_10^0'=e_10^post10, c_8^0'=c_8^post10, lt_20^0'=lt_20^post10, lt_15^0'=lt_15^post10, lt_25^0'=lt_25^post10, Result_4^0'=Result_4^post10, g_12^0'=g_12^post10, d_9^0'=d_9^post10, lt_22^0'=lt_22^post10, lt_17^0'=lt_17^post10, b_7^0'=b_7^post10, lt_19^0'=lt_19^post10, lt_14^0'=lt_14^post10, lt_24^0'=lt_24^post10, f_11^0'=f_11^post10, (Result_4^0-Result_4^post10 == 0 /\ x_5^0-x_5^post10 == 0 /\ c_8^0-c_8^post10 == 0 /\ h_13^0-h_13^post10 == 0 /\ cnt_38^0-cnt_38^post10 == 0 /\ lt_21^0-lt_21^post10 == 0 /\ -lt_24^post10+lt_24^0 == 0 /\ -f_11^post10+f_11^0 == 0 /\ -lt_17^post10+lt_17^0 == 0 /\ -lt_23^post10+lt_23^0 == 0 /\ e_10^0-e_10^post10 == 0 /\ -d_9^post10+d_9^0 == 0 /\ lt_18^0-lt_18^post10 == 0 /\ lt_20^0-lt_20^post10 == 0 /\ lt_22^0-lt_22^post10 == 0 /\ -lt_19^post10+lt_19^0 == 0 /\ lt_25^0-lt_25^post10 == 0 /\ -lt_15^post10+lt_15^0 == 0 /\ -g_12^post10+g_12^0 == 0 /\ -b_7^post10+b_7^0 == 0 /\ -a_6^post10+a_6^0 == 0 /\ -lt_14^post10+lt_14^0 == 0 /\ -lt_16^post10+lt_16^0 == 0), cost: 1
New rule:
l6 -> l3 : TRUE, cost: 1

Applied preprocessing
Original rule:
l3 -> l7 : cnt_38^0'=cnt_38^post11, lt_21^0'=lt_21^post11, lt_16^0'=lt_16^post11, a_6^0'=a_6^post11, lt_18^0'=lt_18^post11, h_13^0'=h_13^post11, x_5^0'=x_5^post11, lt_23^0'=lt_23^post11, e_10^0'=e_10^post11, c_8^0'=c_8^post11, lt_20^0'=lt_20^post11, lt_15^0'=lt_15^post11, lt_25^0'=lt_25^post11, Result_4^0'=Result_4^post11, g_12^0'=g_12^post11, d_9^0'=d_9^post11, lt_22^0'=lt_22^post11, lt_17^0'=lt_17^post11, b_7^0'=b_7^post11, lt_19^0'=lt_19^post11, lt_14^0'=lt_14^post11, lt_24^0'=lt_24^post11, f_11^0'=f_11^post11, (0 == 0 /\ -f_11^post11+f_11^0 == 0 /\ -lt_17^post11+lt_17^0 == 0 /\ -e_10^post11+e_10^0 == 0 /\ -b_7^post11+b_7^0 == 0 /\ g_12^0-g_12^post11 == 0 /\ -lt_18^post11+lt_18^0 == 0 /\ 1+lt_19^150 <= 0 /\ lt_16^0-lt_16^post11 == 0 /\ -lt_22^post11+lt_22^0 == 0 /\ 1+lt_25^160 <= 0 /\ -lt_24^post11+lt_24^0 == 0 /\ x_5^0-x_5^post11 == 0 /\ a_6^0-a_6^post11 == 0 /\ lt_23^0-lt_23^post11 == 0 /\ -cnt_38^0+lt_21^120 == 0 /\ -Result_4^post11+Result_4^0 == 0 /\ h_13^0-h_13^post11 == 0 /\ -cnt_38^0+lt_25^160 == 0 /\ cnt_38^0-cnt_38^post11 == 0 /\ -c_8^post11+c_8^0 == 0 /\ d_9^0-d_9^post11 == 0), cost: 1
New rule:
l3 -> l7 : lt_21^0'=lt_21^post11, lt_20^0'=lt_20^post11, lt_15^0'=lt_15^post11, lt_25^0'=lt_25^post11, lt_19^0'=lt_19^post11, lt_14^0'=lt_14^post11, 1+cnt_38^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l7 -> l3 : cnt_38^0'=cnt_38^post12, lt_21^0'=lt_21^post12, lt_16^0'=lt_16^post12, a_6^0'=a_6^post12, lt_18^0'=lt_18^post12, h_13^0'=h_13^post12, x_5^0'=x_5^post12, lt_23^0'=lt_23^post12, e_10^0'=e_10^post12, c_8^0'=c_8^post12, lt_20^0'=lt_20^post12, lt_15^0'=lt_15^post12, lt_25^0'=lt_25^post12, Result_4^0'=Result_4^post12, g_12^0'=g_12^post12, d_9^0'=d_9^post12, lt_22^0'=lt_22^post12, lt_17^0'=lt_17^post12, b_7^0'=b_7^post12, lt_19^0'=lt_19^post12, lt_14^0'=lt_14^post12, lt_24^0'=lt_24^post12, f_11^0'=f_11^post12, (-lt_18^post12+lt_18^0 == 0 /\ -Result_4^post12+Result_4^0 == 0 /\ -lt_19^post12+lt_19^0 == 0 /\ -b_7^post12+b_7^0 == 0 /\ lt_20^0-lt_20^post12 == 0 /\ -lt_15^post12+lt_15^0 == 0 /\ -lt_14^post12+lt_14^0 == 0 /\ x_5^0-x_5^post12 == 0 /\ -lt_25^post12+lt_25^0 == 0 /\ -c_8^post12+c_8^0 == 0 /\ lt_21^0-lt_21^post12 == 0 /\ cnt_38^0-cnt_38^post12 == 0 /\ lt_16^0-lt_16^post12 == 0 /\ a_6^0-a_6^post12 == 0 /\ -lt_22^post12+lt_22^0 == 0 /\ lt_23^0-lt_23^post12 == 0 /\ lt_24^0-lt_24^post12 == 0 /\ e_10^0-e_10^post12 == 0 /\ -d_9^post12+d_9^0 == 0 /\ -g_12^post12+g_12^0 == 0 /\ lt_17^0-lt_17^post12 == 0 /\ h_13^0-h_13^post12 == 0 /\ -f_11^post12+f_11^0 == 0), cost: 1
New rule:
l7 -> l3 : TRUE, cost: 1

Applied preprocessing
Original rule:
l8 -> l2 : cnt_38^0'=cnt_38^post13, lt_21^0'=lt_21^post13, lt_16^0'=lt_16^post13, a_6^0'=a_6^post13, lt_18^0'=lt_18^post13, h_13^0'=h_13^post13, x_5^0'=x_5^post13, lt_23^0'=lt_23^post13, e_10^0'=e_10^post13, c_8^0'=c_8^post13, lt_20^0'=lt_20^post13, lt_15^0'=lt_15^post13, lt_25^0'=lt_25^post13, Result_4^0'=Result_4^post13, g_12^0'=g_12^post13, d_9^0'=d_9^post13, lt_22^0'=lt_22^post13, lt_17^0'=lt_17^post13, b_7^0'=b_7^post13, lt_19^0'=lt_19^post13, lt_14^0'=lt_14^post13, lt_24^0'=lt_24^post13, f_11^0'=f_11^post13, (e_10^0-e_10^post13 == 0 /\ -lt_22^post13+lt_22^0 == 0 /\ lt_23^0-lt_23^post13 == 0 /\ lt_14^0-lt_14^post13 == 0 /\ -lt_18^post13+lt_18^0 == 0 /\ -lt_19^post13+lt_19^0 == 0 /\ -lt_25^post13+lt_25^0 == 0 /\ -b_7^post13+b_7^0 == 0 /\ -g_12^post13+g_12^0 == 0 /\ lt_21^0-lt_21^post13 == 0 /\ lt_16^0-lt_16^post13 == 0 /\ x_5^0-x_5^post13 == 0 /\ -d_9^post13+d_9^0 == 0 /\ cnt_38^0-cnt_38^post13 == 0 /\ c_8^0-c_8^post13 == 0 /\ lt_20^0-lt_20^post13 == 0 /\ lt_24^0-lt_24^post13 == 0 /\ Result_4^0-Result_4^post13 == 0 /\ a_6^0-a_6^post13 == 0 /\ -lt_17^post13+lt_17^0 == 0 /\ -f_11^post13+f_11^0 == 0 /\ -lt_15^post13+lt_15^0 == 0 /\ h_13^0-h_13^post13 == 0), cost: 1
New rule:
l8 -> l2 : TRUE, cost: 1

Simplified rules
Start location: l8
  14: l2 -> l3 : a_6^0'=c_8^post1, h_13^0'=c_8^post1, x_5^0'=c_8^post1, e_10^0'=c_8^post1, c_8^0'=c_8^post1, g_12^0'=c_8^post1, d_9^0'=c_8^post1, b_7^0'=c_8^post1, f_11^0'=c_8^post1, 0 == 0, cost: 1
  15: l3 -> l4 : lt_16^0'=lt_16^post5, lt_18^0'=lt_18^post5, lt_23^0'=lt_23^post5, lt_25^0'=lt_25^post5, lt_22^0'=lt_22^post5, lt_17^0'=lt_17^post5, lt_19^0'=lt_19^post5, lt_24^0'=lt_24^post5, -1+cnt_38^0 >= 0, cost: 1
  17: l3 -> l5 : lt_23^0'=lt_23^post7, lt_15^0'=lt_15^post7, lt_25^0'=lt_25^post7, lt_22^0'=lt_22^post7, lt_19^0'=lt_19^post7, lt_14^0'=lt_14^post7, lt_24^0'=lt_24^post7, -1+cnt_38^0 >= 0, cost: 1
  19: l3 -> l6 : lt_21^0'=lt_21^post9, lt_16^0'=lt_16^post9, lt_18^0'=lt_18^post9, lt_20^0'=lt_20^post9, lt_25^0'=lt_25^post9, lt_17^0'=lt_17^post9, lt_19^0'=lt_19^post9, 1+cnt_38^0 <= 0, cost: 1
  21: l3 -> l7 : lt_21^0'=lt_21^post11, lt_20^0'=lt_20^post11, lt_15^0'=lt_15^post11, lt_25^0'=lt_25^post11, lt_19^0'=lt_19^post11, lt_14^0'=lt_14^post11, 1+cnt_38^0 <= 0, cost: 1
  16: l4 -> l3 : TRUE, cost: 1
  18: l5 -> l3 : TRUE, cost: 1
  20: l6 -> l3 : TRUE, cost: 1
  22: l7 -> l3 : TRUE, cost: 1
  23: l8 -> l2 : TRUE, cost: 1


Eliminating location l2 by chaining:

Applied chaining
First rule:
l8 -> l2 : TRUE, cost: 1
Second rule:
l2 -> l3 : a_6^0'=c_8^post1, h_13^0'=c_8^post1, x_5^0'=c_8^post1, e_10^0'=c_8^post1, c_8^0'=c_8^post1, g_12^0'=c_8^post1, d_9^0'=c_8^post1, b_7^0'=c_8^post1, f_11^0'=c_8^post1, 0 == 0, cost: 1
New rule:
l8 -> l3 : a_6^0'=c_8^post1, h_13^0'=c_8^post1, x_5^0'=c_8^post1, e_10^0'=c_8^post1, c_8^0'=c_8^post1, g_12^0'=c_8^post1, d_9^0'=c_8^post1, b_7^0'=c_8^post1, f_11^0'=c_8^post1, 0 == 0, cost: 2

Applied deletion
Removed the following rules: 14 23

Eliminating location l4 by chaining:

Applied chaining
First rule:
l3 -> l4 : lt_16^0'=lt_16^post5, lt_18^0'=lt_18^post5, lt_23^0'=lt_23^post5, lt_25^0'=lt_25^post5, lt_22^0'=lt_22^post5, lt_17^0'=lt_17^post5, lt_19^0'=lt_19^post5, lt_24^0'=lt_24^post5, -1+cnt_38^0 >= 0, cost: 1
Second rule:
l4 -> l3 : TRUE, cost: 1
New rule:
l3 -> l3 : lt_16^0'=lt_16^post5, lt_18^0'=lt_18^post5, lt_23^0'=lt_23^post5, lt_25^0'=lt_25^post5, lt_22^0'=lt_22^post5, lt_17^0'=lt_17^post5, lt_19^0'=lt_19^post5, lt_24^0'=lt_24^post5, -1+cnt_38^0 >= 0, cost: 2

Applied deletion
Removed the following rules: 15 16

Eliminating location l5 by chaining:

Applied chaining
First rule:
l3 -> l5 : lt_23^0'=lt_23^post7, lt_15^0'=lt_15^post7, lt_25^0'=lt_25^post7, lt_22^0'=lt_22^post7, lt_19^0'=lt_19^post7, lt_14^0'=lt_14^post7, lt_24^0'=lt_24^post7, -1+cnt_38^0 >= 0, cost: 1
Second rule:
l5 -> l3 : TRUE, cost: 1
New rule:
l3 -> l3 : lt_23^0'=lt_23^post7, lt_15^0'=lt_15^post7, lt_25^0'=lt_25^post7, lt_22^0'=lt_22^post7, lt_19^0'=lt_19^post7, lt_14^0'=lt_14^post7, lt_24^0'=lt_24^post7, -1+cnt_38^0 >= 0, cost: 2

Applied deletion
Removed the following rules: 17 18

Eliminating location l6 by chaining:

Applied chaining
First rule:
l3 -> l6 : lt_21^0'=lt_21^post9, lt_16^0'=lt_16^post9, lt_18^0'=lt_18^post9, lt_20^0'=lt_20^post9, lt_25^0'=lt_25^post9, lt_17^0'=lt_17^post9, lt_19^0'=lt_19^post9, 1+cnt_38^0 <= 0, cost: 1
Second rule:
l6 -> l3 : TRUE, cost: 1
New rule:
l3 -> l3 : lt_21^0'=lt_21^post9, lt_16^0'=lt_16^post9, lt_18^0'=lt_18^post9, lt_20^0'=lt_20^post9, lt_25^0'=lt_25^post9, lt_17^0'=lt_17^post9, lt_19^0'=lt_19^post9, 1+cnt_38^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 19 20

Eliminating location l7 by chaining:

Applied chaining
First rule:
l3 -> l7 : lt_21^0'=lt_21^post11, lt_20^0'=lt_20^post11, lt_15^0'=lt_15^post11, lt_25^0'=lt_25^post11, lt_19^0'=lt_19^post11, lt_14^0'=lt_14^post11, 1+cnt_38^0 <= 0, cost: 1
Second rule:
l7 -> l3 : TRUE, cost: 1
New rule:
l3 -> l3 : lt_21^0'=lt_21^post11, lt_20^0'=lt_20^post11, lt_15^0'=lt_15^post11, lt_25^0'=lt_25^post11, lt_19^0'=lt_19^post11, lt_14^0'=lt_14^post11, 1+cnt_38^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 21 22

Eliminated locations on linear paths
Start location: l8
  25: l3 -> l3 : lt_16^0'=lt_16^post5, lt_18^0'=lt_18^post5, lt_23^0'=lt_23^post5, lt_25^0'=lt_25^post5, lt_22^0'=lt_22^post5, lt_17^0'=lt_17^post5, lt_19^0'=lt_19^post5, lt_24^0'=lt_24^post5, -1+cnt_38^0 >= 0, cost: 2
  26: l3 -> l3 : lt_23^0'=lt_23^post7, lt_15^0'=lt_15^post7, lt_25^0'=lt_25^post7, lt_22^0'=lt_22^post7, lt_19^0'=lt_19^post7, lt_14^0'=lt_14^post7, lt_24^0'=lt_24^post7, -1+cnt_38^0 >= 0, cost: 2
  27: l3 -> l3 : lt_21^0'=lt_21^post9, lt_16^0'=lt_16^post9, lt_18^0'=lt_18^post9, lt_20^0'=lt_20^post9, lt_25^0'=lt_25^post9, lt_17^0'=lt_17^post9, lt_19^0'=lt_19^post9, 1+cnt_38^0 <= 0, cost: 2
  28: l3 -> l3 : lt_21^0'=lt_21^post11, lt_20^0'=lt_20^post11, lt_15^0'=lt_15^post11, lt_25^0'=lt_25^post11, lt_19^0'=lt_19^post11, lt_14^0'=lt_14^post11, 1+cnt_38^0 <= 0, cost: 2
  24: l8 -> l3 : a_6^0'=c_8^post1, h_13^0'=c_8^post1, x_5^0'=c_8^post1, e_10^0'=c_8^post1, c_8^0'=c_8^post1, g_12^0'=c_8^post1, d_9^0'=c_8^post1, b_7^0'=c_8^post1, f_11^0'=c_8^post1, 0 == 0, cost: 2


Applied nonterm
Original rule:
l3 -> l3 : lt_16^0'=lt_16^post5, lt_18^0'=lt_18^post5, lt_23^0'=lt_23^post5, lt_25^0'=lt_25^post5, lt_22^0'=lt_22^post5, lt_17^0'=lt_17^post5, lt_19^0'=lt_19^post5, lt_24^0'=lt_24^post5, -1+cnt_38^0 >= 0, cost: 2
New rule:
l3 -> [9] : (-1+n >= 0 /\ -1+cnt_38^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_KAPNaa.txt

Applied nonterm
Original rule:
l3 -> l3 : lt_23^0'=lt_23^post7, lt_15^0'=lt_15^post7, lt_25^0'=lt_25^post7, lt_22^0'=lt_22^post7, lt_19^0'=lt_19^post7, lt_14^0'=lt_14^post7, lt_24^0'=lt_24^post7, -1+cnt_38^0 >= 0, cost: 2
New rule:
l3 -> [9] : (-1+n0 >= 0 /\ -1+cnt_38^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_bpOOJc.txt

Applied nonterm
Original rule:
l3 -> l3 : lt_21^0'=lt_21^post9, lt_16^0'=lt_16^post9, lt_18^0'=lt_18^post9, lt_20^0'=lt_20^post9, lt_25^0'=lt_25^post9, lt_17^0'=lt_17^post9, lt_19^0'=lt_19^post9, 1+cnt_38^0 <= 0, cost: 2
New rule:
l3 -> [9] : (-1-cnt_38^0 >= 0 /\ -1+n1 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_EMNiJN.txt

Applied nonterm
Original rule:
l3 -> l3 : lt_21^0'=lt_21^post11, lt_20^0'=lt_20^post11, lt_15^0'=lt_15^post11, lt_25^0'=lt_25^post11, lt_19^0'=lt_19^post11, lt_14^0'=lt_14^post11, 1+cnt_38^0 <= 0, cost: 2
New rule:
l3 -> [9] : (-1-cnt_38^0 >= 0 /\ -1+n2 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_bgMHmN.txt

Applied chaining
First rule:
l3 -> l3 : lt_21^0'=lt_21^post11, lt_20^0'=lt_20^post11, lt_15^0'=lt_15^post11, lt_25^0'=lt_25^post11, lt_19^0'=lt_19^post11, lt_14^0'=lt_14^post11, 1+cnt_38^0 <= 0, cost: 2
Second rule:
l3 -> l3 : lt_21^0'=lt_21^post9, lt_16^0'=lt_16^post9, lt_18^0'=lt_18^post9, lt_20^0'=lt_20^post9, lt_25^0'=lt_25^post9, lt_17^0'=lt_17^post9, lt_19^0'=lt_19^post9, 1+cnt_38^0 <= 0, cost: 2
New rule:
l3 -> l3 : lt_21^0'=lt_21^post9, lt_16^0'=lt_16^post9, lt_18^0'=lt_18^post9, lt_20^0'=lt_20^post9, lt_15^0'=lt_15^post11, lt_25^0'=lt_25^post9, lt_17^0'=lt_17^post9, lt_19^0'=lt_19^post9, lt_14^0'=lt_14^post11, 1+cnt_38^0 <= 0, cost: 4

Applied nonterm
Original rule:
l3 -> l3 : lt_21^0'=lt_21^post9, lt_16^0'=lt_16^post9, lt_18^0'=lt_18^post9, lt_20^0'=lt_20^post9, lt_15^0'=lt_15^post11, lt_25^0'=lt_25^post9, lt_17^0'=lt_17^post9, lt_19^0'=lt_19^post9, lt_14^0'=lt_14^post11, 1+cnt_38^0 <= 0, cost: 4
New rule:
l3 -> [9] : (-1-cnt_38^0 >= 0 /\ -1+n3 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_nNoCma.txt

Applied chaining
First rule:
l3 -> l3 : lt_21^0'=lt_21^post9, lt_16^0'=lt_16^post9, lt_18^0'=lt_18^post9, lt_20^0'=lt_20^post9, lt_25^0'=lt_25^post9, lt_17^0'=lt_17^post9, lt_19^0'=lt_19^post9, 1+cnt_38^0 <= 0, cost: 2
Second rule:
l3 -> [9] : (-1-cnt_38^0 >= 0 /\ -1+n3 >= 0), cost: NONTERM
New rule:
l3 -> [9] : (1+cnt_38^0 <= 0 /\ -1-cnt_38^0 >= 0 /\ -1+n3 >= 0), cost: NONTERM

Applied chaining
First rule:
l3 -> l3 : lt_21^0'=lt_21^post9, lt_16^0'=lt_16^post9, lt_18^0'=lt_18^post9, lt_20^0'=lt_20^post9, lt_25^0'=lt_25^post9, lt_17^0'=lt_17^post9, lt_19^0'=lt_19^post9, 1+cnt_38^0 <= 0, cost: 2
Second rule:
l3 -> l3 : lt_21^0'=lt_21^post11, lt_20^0'=lt_20^post11, lt_15^0'=lt_15^post11, lt_25^0'=lt_25^post11, lt_19^0'=lt_19^post11, lt_14^0'=lt_14^post11, 1+cnt_38^0 <= 0, cost: 2
New rule:
l3 -> l3 : lt_21^0'=lt_21^post11, lt_16^0'=lt_16^post9, lt_18^0'=lt_18^post9, lt_20^0'=lt_20^post11, lt_15^0'=lt_15^post11, lt_25^0'=lt_25^post11, lt_17^0'=lt_17^post9, lt_19^0'=lt_19^post11, lt_14^0'=lt_14^post11, 1+cnt_38^0 <= 0, cost: 4

Applied nonterm
Original rule:
l3 -> l3 : lt_21^0'=lt_21^post11, lt_16^0'=lt_16^post9, lt_18^0'=lt_18^post9, lt_20^0'=lt_20^post11, lt_15^0'=lt_15^post11, lt_25^0'=lt_25^post11, lt_17^0'=lt_17^post9, lt_19^0'=lt_19^post11, lt_14^0'=lt_14^post11, 1+cnt_38^0 <= 0, cost: 4
New rule:
l3 -> [9] : (-1+n4 >= 0 /\ -1-cnt_38^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_pgmiNM.txt

Applied chaining
First rule:
l3 -> l3 : lt_21^0'=lt_21^post11, lt_20^0'=lt_20^post11, lt_15^0'=lt_15^post11, lt_25^0'=lt_25^post11, lt_19^0'=lt_19^post11, lt_14^0'=lt_14^post11, 1+cnt_38^0 <= 0, cost: 2
Second rule:
l3 -> [9] : (-1+n4 >= 0 /\ -1-cnt_38^0 >= 0), cost: NONTERM
New rule:
l3 -> [9] : (-1+n4 >= 0 /\ 1+cnt_38^0 <= 0 /\ -1-cnt_38^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l3 -> l3 : lt_23^0'=lt_23^post7, lt_15^0'=lt_15^post7, lt_25^0'=lt_25^post7, lt_22^0'=lt_22^post7, lt_19^0'=lt_19^post7, lt_14^0'=lt_14^post7, lt_24^0'=lt_24^post7, -1+cnt_38^0 >= 0, cost: 2
Second rule:
l3 -> l3 : lt_16^0'=lt_16^post5, lt_18^0'=lt_18^post5, lt_23^0'=lt_23^post5, lt_25^0'=lt_25^post5, lt_22^0'=lt_22^post5, lt_17^0'=lt_17^post5, lt_19^0'=lt_19^post5, lt_24^0'=lt_24^post5, -1+cnt_38^0 >= 0, cost: 2
New rule:
l3 -> l3 : lt_16^0'=lt_16^post5, lt_18^0'=lt_18^post5, lt_23^0'=lt_23^post5, lt_15^0'=lt_15^post7, lt_25^0'=lt_25^post5, lt_22^0'=lt_22^post5, lt_17^0'=lt_17^post5, lt_19^0'=lt_19^post5, lt_14^0'=lt_14^post7, lt_24^0'=lt_24^post5, -1+cnt_38^0 >= 0, cost: 4

Applied nonterm
Original rule:
l3 -> l3 : lt_16^0'=lt_16^post5, lt_18^0'=lt_18^post5, lt_23^0'=lt_23^post5, lt_15^0'=lt_15^post7, lt_25^0'=lt_25^post5, lt_22^0'=lt_22^post5, lt_17^0'=lt_17^post5, lt_19^0'=lt_19^post5, lt_14^0'=lt_14^post7, lt_24^0'=lt_24^post5, -1+cnt_38^0 >= 0, cost: 4
New rule:
l3 -> [9] : (-1+n5 >= 0 /\ -1+cnt_38^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_DfgiCA.txt

Applied chaining
First rule:
l3 -> l3 : lt_16^0'=lt_16^post5, lt_18^0'=lt_18^post5, lt_23^0'=lt_23^post5, lt_25^0'=lt_25^post5, lt_22^0'=lt_22^post5, lt_17^0'=lt_17^post5, lt_19^0'=lt_19^post5, lt_24^0'=lt_24^post5, -1+cnt_38^0 >= 0, cost: 2
Second rule:
l3 -> [9] : (-1+n5 >= 0 /\ -1+cnt_38^0 >= 0), cost: NONTERM
New rule:
l3 -> [9] : (-1+n5 >= 0 /\ -1+cnt_38^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l3 -> l3 : lt_16^0'=lt_16^post5, lt_18^0'=lt_18^post5, lt_23^0'=lt_23^post5, lt_25^0'=lt_25^post5, lt_22^0'=lt_22^post5, lt_17^0'=lt_17^post5, lt_19^0'=lt_19^post5, lt_24^0'=lt_24^post5, -1+cnt_38^0 >= 0, cost: 2
Second rule:
l3 -> l3 : lt_23^0'=lt_23^post7, lt_15^0'=lt_15^post7, lt_25^0'=lt_25^post7, lt_22^0'=lt_22^post7, lt_19^0'=lt_19^post7, lt_14^0'=lt_14^post7, lt_24^0'=lt_24^post7, -1+cnt_38^0 >= 0, cost: 2
New rule:
l3 -> l3 : lt_16^0'=lt_16^post5, lt_18^0'=lt_18^post5, lt_23^0'=lt_23^post7, lt_15^0'=lt_15^post7, lt_25^0'=lt_25^post7, lt_22^0'=lt_22^post7, lt_17^0'=lt_17^post5, lt_19^0'=lt_19^post7, lt_14^0'=lt_14^post7, lt_24^0'=lt_24^post7, -1+cnt_38^0 >= 0, cost: 4

Applied nonterm
Original rule:
l3 -> l3 : lt_16^0'=lt_16^post5, lt_18^0'=lt_18^post5, lt_23^0'=lt_23^post7, lt_15^0'=lt_15^post7, lt_25^0'=lt_25^post7, lt_22^0'=lt_22^post7, lt_17^0'=lt_17^post5, lt_19^0'=lt_19^post7, lt_14^0'=lt_14^post7, lt_24^0'=lt_24^post7, -1+cnt_38^0 >= 0, cost: 4
New rule:
l3 -> [9] : (-1+n6 >= 0 /\ -1+cnt_38^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_kpnOpN.txt

Applied chaining
First rule:
l3 -> l3 : lt_23^0'=lt_23^post7, lt_15^0'=lt_15^post7, lt_25^0'=lt_25^post7, lt_22^0'=lt_22^post7, lt_19^0'=lt_19^post7, lt_14^0'=lt_14^post7, lt_24^0'=lt_24^post7, -1+cnt_38^0 >= 0, cost: 2
Second rule:
l3 -> [9] : (-1+n6 >= 0 /\ -1+cnt_38^0 >= 0), cost: NONTERM
New rule:
l3 -> [9] : (-1+n6 >= 0 /\ -1+cnt_38^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l3 -> [9] : (-1-cnt_38^0 >= 0 /\ -1+n1 >= 0), cost: NONTERM
New rule:
l3 -> [9] : (1+cnt_38^0 <= 0 /\ -1+n1 >= 0), cost: NONTERM

Applied simplification
Original rule:
l3 -> [9] : (-1-cnt_38^0 >= 0 /\ -1+n2 >= 0), cost: NONTERM
New rule:
l3 -> [9] : (1+cnt_38^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM

Applied simplification
Original rule:
l3 -> [9] : (-1-cnt_38^0 >= 0 /\ -1+n3 >= 0), cost: NONTERM
New rule:
l3 -> [9] : (1+cnt_38^0 <= 0 /\ -1+n3 >= 0), cost: NONTERM

Applied simplification
Original rule:
l3 -> [9] : (1+cnt_38^0 <= 0 /\ -1-cnt_38^0 >= 0 /\ -1+n3 >= 0), cost: NONTERM
New rule:
l3 -> [9] : (1+cnt_38^0 <= 0 /\ -1+n3 >= 0), cost: NONTERM

Applied simplification
Original rule:
l3 -> [9] : (-1+n4 >= 0 /\ -1-cnt_38^0 >= 0), cost: NONTERM
New rule:
l3 -> [9] : (-1+n4 >= 0 /\ 1+cnt_38^0 <= 0), cost: NONTERM

Applied simplification
Original rule:
l3 -> [9] : (-1+n4 >= 0 /\ 1+cnt_38^0 <= 0 /\ -1-cnt_38^0 >= 0), cost: NONTERM
New rule:
l3 -> [9] : (-1+n4 >= 0 /\ 1+cnt_38^0 <= 0), cost: NONTERM

Applied deletion
Removed the following rules: 25 26 27 28

Accelerated simple loops
Start location: l8
  29: l3 -> [9] : (-1+n >= 0 /\ -1+cnt_38^0 >= 0), cost: NONTERM
  30: l3 -> [9] : (-1+n0 >= 0 /\ -1+cnt_38^0 >= 0), cost: NONTERM
  37: l3 -> [9] : (-1+n5 >= 0 /\ -1+cnt_38^0 >= 0), cost: NONTERM
  38: l3 -> [9] : (-1+n6 >= 0 /\ -1+cnt_38^0 >= 0), cost: NONTERM
  39: l3 -> [9] : (1+cnt_38^0 <= 0 /\ -1+n1 >= 0), cost: NONTERM
  40: l3 -> [9] : (1+cnt_38^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM
  41: l3 -> [9] : (1+cnt_38^0 <= 0 /\ -1+n3 >= 0), cost: NONTERM
  42: l3 -> [9] : (-1+n4 >= 0 /\ 1+cnt_38^0 <= 0), cost: NONTERM
  24: l8 -> l3 : a_6^0'=c_8^post1, h_13^0'=c_8^post1, x_5^0'=c_8^post1, e_10^0'=c_8^post1, c_8^0'=c_8^post1, g_12^0'=c_8^post1, d_9^0'=c_8^post1, b_7^0'=c_8^post1, f_11^0'=c_8^post1, 0 == 0, cost: 2


Applied chaining
First rule:
l8 -> l3 : a_6^0'=c_8^post1, h_13^0'=c_8^post1, x_5^0'=c_8^post1, e_10^0'=c_8^post1, c_8^0'=c_8^post1, g_12^0'=c_8^post1, d_9^0'=c_8^post1, b_7^0'=c_8^post1, f_11^0'=c_8^post1, 0 == 0, cost: 2
Second rule:
l3 -> [9] : (-1+n >= 0 /\ -1+cnt_38^0 >= 0), cost: NONTERM
New rule:
l8 -> [9] : -1+cnt_38^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l8 -> l3 : a_6^0'=c_8^post1, h_13^0'=c_8^post1, x_5^0'=c_8^post1, e_10^0'=c_8^post1, c_8^0'=c_8^post1, g_12^0'=c_8^post1, d_9^0'=c_8^post1, b_7^0'=c_8^post1, f_11^0'=c_8^post1, 0 == 0, cost: 2
Second rule:
l3 -> [9] : (-1+n0 >= 0 /\ -1+cnt_38^0 >= 0), cost: NONTERM
New rule:
l8 -> [9] : -1+cnt_38^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l8 -> l3 : a_6^0'=c_8^post1, h_13^0'=c_8^post1, x_5^0'=c_8^post1, e_10^0'=c_8^post1, c_8^0'=c_8^post1, g_12^0'=c_8^post1, d_9^0'=c_8^post1, b_7^0'=c_8^post1, f_11^0'=c_8^post1, 0 == 0, cost: 2
Second rule:
l3 -> [9] : (-1+n5 >= 0 /\ -1+cnt_38^0 >= 0), cost: NONTERM
New rule:
l8 -> [9] : -1+cnt_38^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l8 -> l3 : a_6^0'=c_8^post1, h_13^0'=c_8^post1, x_5^0'=c_8^post1, e_10^0'=c_8^post1, c_8^0'=c_8^post1, g_12^0'=c_8^post1, d_9^0'=c_8^post1, b_7^0'=c_8^post1, f_11^0'=c_8^post1, 0 == 0, cost: 2
Second rule:
l3 -> [9] : (-1+n6 >= 0 /\ -1+cnt_38^0 >= 0), cost: NONTERM
New rule:
l8 -> [9] : -1+cnt_38^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l8 -> l3 : a_6^0'=c_8^post1, h_13^0'=c_8^post1, x_5^0'=c_8^post1, e_10^0'=c_8^post1, c_8^0'=c_8^post1, g_12^0'=c_8^post1, d_9^0'=c_8^post1, b_7^0'=c_8^post1, f_11^0'=c_8^post1, 0 == 0, cost: 2
Second rule:
l3 -> [9] : (1+cnt_38^0 <= 0 /\ -1+n1 >= 0), cost: NONTERM
New rule:
l8 -> [9] : 1+cnt_38^0 <= 0, cost: NONTERM

Applied chaining
First rule:
l8 -> l3 : a_6^0'=c_8^post1, h_13^0'=c_8^post1, x_5^0'=c_8^post1, e_10^0'=c_8^post1, c_8^0'=c_8^post1, g_12^0'=c_8^post1, d_9^0'=c_8^post1, b_7^0'=c_8^post1, f_11^0'=c_8^post1, 0 == 0, cost: 2
Second rule:
l3 -> [9] : (1+cnt_38^0 <= 0 /\ -1+n2 >= 0), cost: NONTERM
New rule:
l8 -> [9] : 1+cnt_38^0 <= 0, cost: NONTERM

Applied chaining
First rule:
l8 -> l3 : a_6^0'=c_8^post1, h_13^0'=c_8^post1, x_5^0'=c_8^post1, e_10^0'=c_8^post1, c_8^0'=c_8^post1, g_12^0'=c_8^post1, d_9^0'=c_8^post1, b_7^0'=c_8^post1, f_11^0'=c_8^post1, 0 == 0, cost: 2
Second rule:
l3 -> [9] : (1+cnt_38^0 <= 0 /\ -1+n3 >= 0), cost: NONTERM
New rule:
l8 -> [9] : 1+cnt_38^0 <= 0, cost: NONTERM

Applied chaining
First rule:
l8 -> l3 : a_6^0'=c_8^post1, h_13^0'=c_8^post1, x_5^0'=c_8^post1, e_10^0'=c_8^post1, c_8^0'=c_8^post1, g_12^0'=c_8^post1, d_9^0'=c_8^post1, b_7^0'=c_8^post1, f_11^0'=c_8^post1, 0 == 0, cost: 2
Second rule:
l3 -> [9] : (-1+n4 >= 0 /\ 1+cnt_38^0 <= 0), cost: NONTERM
New rule:
l8 -> [9] : 1+cnt_38^0 <= 0, cost: NONTERM

Applied deletion
Removed the following rules: 29 30 37 38 39 40 41 42

Chained accelerated rules with incoming rules
Start location: l8
  24: l8 -> l3 : a_6^0'=c_8^post1, h_13^0'=c_8^post1, x_5^0'=c_8^post1, e_10^0'=c_8^post1, c_8^0'=c_8^post1, g_12^0'=c_8^post1, d_9^0'=c_8^post1, b_7^0'=c_8^post1, f_11^0'=c_8^post1, 0 == 0, cost: 2
  43: l8 -> [9] : -1+cnt_38^0 >= 0, cost: NONTERM
  44: l8 -> [9] : 1+cnt_38^0 <= 0, cost: NONTERM


Removed unreachable locations and irrelevant leafs
Start location: l8
  43: l8 -> [9] : -1+cnt_38^0 >= 0, cost: NONTERM
  44: l8 -> [9] : 1+cnt_38^0 <= 0, cost: NONTERM


Computing asymptotic complexity
Proved nontermination of rule 43 via SMT.

Proved the following lower bound
Complexity:  Nonterm
Cpx degree: Nonterm

Solved cost: NONTERM
Rule cost:   NONTERM
Rule guard:  -1+cnt_38^0 >= 0