NO Initial ITS Start location: l8 Program variables: a_6^0 b_7^0 c_8^0 cnt_38^0 d_9^0 e_10^0 f_11^0 g_12^0 h_13^0 lt_14^0 lt_15^0 lt_16^0 lt_17^0 lt_18^0 lt_19^0 lt_20^0 lt_21^0 lt_22^0 lt_23^0 lt_24^0 lt_25^0 result_4^0 x_5^0 0: l0 -> l1 : a_6^0'=a_6^post1, b_7^0'=b_7^post1, c_8^0'=c_8^post1, cnt_38^0'=cnt_38^post1, d_9^0'=d_9^post1, e_10^0'=e_10^post1, f_11^0'=f_11^post1, g_12^0'=g_12^post1, h_13^0'=h_13^post1, lt_14^0'=lt_14^post1, lt_15^0'=lt_15^post1, lt_16^0'=lt_16^post1, lt_17^0'=lt_17^post1, lt_18^0'=lt_18^post1, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, lt_22^0'=lt_22^post1, lt_23^0'=lt_23^post1, lt_24^0'=lt_24^post1, lt_25^0'=lt_25^post1, result_4^0'=result_4^post1, x_5^0'=x_5^post1, (0 == 0 /\ lt_19^0-lt_19^post1 == 0 /\ -x_5^post1+x_5^0 == 0 /\ -f_11^post1+f_11^0 == 0 /\ -lt_17^post1+lt_17^0 == 0 /\ -lt_14^post1+lt_14^0 == 0 /\ -lt_16^post1+lt_16^0 == 0 /\ b_7^0-b_7^post1 == 0 /\ g_12^0-g_12^post1 == 0 /\ lt_18^0-lt_18^post1 == 0 /\ -lt_24^post1+lt_24^0 == 0 /\ lt_22^0-lt_22^post1 == 0 /\ -cnt_38^post1+cnt_38^0 == 0 /\ c_8^0-c_8^post1 == 0 /\ lt_23^0-lt_23^post1 == 0 /\ e_10^0-e_10^post1 == 0 /\ lt_25^0-lt_25^post1 == 0 /\ lt_15^0-lt_15^post1 == 0 /\ d_9^0-d_9^post1 == 0 /\ h_13^0-h_13^post1 == 0 /\ -lt_21^post1+lt_21^0 == 0 /\ -a_6^post1+a_6^0 == 0 /\ lt_20^0-lt_20^post1 == 0), cost: 1 1: l2 -> l3 : a_6^0'=a_6^post2, b_7^0'=b_7^post2, c_8^0'=c_8^post2, cnt_38^0'=cnt_38^post2, d_9^0'=d_9^post2, e_10^0'=e_10^post2, f_11^0'=f_11^post2, g_12^0'=g_12^post2, h_13^0'=h_13^post2, lt_14^0'=lt_14^post2, lt_15^0'=lt_15^post2, lt_16^0'=lt_16^post2, lt_17^0'=lt_17^post2, lt_18^0'=lt_18^post2, lt_19^0'=lt_19^post2, lt_20^0'=lt_20^post2, lt_21^0'=lt_21^post2, lt_22^0'=lt_22^post2, lt_23^0'=lt_23^post2, lt_24^0'=lt_24^post2, lt_25^0'=lt_25^post2, result_4^0'=result_4^post2, x_5^0'=x_5^post2, (0 == 0 /\ -result_4^post2+result_4^0 == 0 /\ b_7^post2-a_6^post2 == 0 /\ lt_18^0-lt_18^post2 == 0 /\ -e_10^post2+f_11^post2 == 0 /\ -cnt_38^post2+cnt_38^0 == 0 /\ g_12^post2-f_11^post2 == 0 /\ lt_17^0-lt_17^post2 == 0 /\ lt_15^0-lt_15^post2 == 0 /\ lt_20^0-lt_20^post2 == 0 /\ -g_12^post2+h_13^post2 == 0 /\ -lt_25^post2+lt_25^0 == 0 /\ -b_7^post2+c_8^post2 == 0 /\ -c_8^post2+d_9^post2 == 0 /\ -lt_22^post2+lt_22^0 == 0 /\ -lt_21^post2+lt_21^0 == 0 /\ e_10^post2-d_9^post2 == 0 /\ lt_23^0-lt_23^post2 == 0 /\ -lt_19^post2+lt_19^0 == 0 /\ -lt_16^post2+lt_16^0 == 0 /\ lt_24^0-lt_24^post2 == 0 /\ -lt_14^post2+lt_14^0 == 0 /\ -x_5^post2+a_6^post2 == 0), cost: 1 2: l3 -> l0 : a_6^0'=a_6^post3, b_7^0'=b_7^post3, c_8^0'=c_8^post3, cnt_38^0'=cnt_38^post3, d_9^0'=d_9^post3, e_10^0'=e_10^post3, f_11^0'=f_11^post3, g_12^0'=g_12^post3, h_13^0'=h_13^post3, lt_14^0'=lt_14^post3, lt_15^0'=lt_15^post3, lt_16^0'=lt_16^post3, lt_17^0'=lt_17^post3, lt_18^0'=lt_18^post3, lt_19^0'=lt_19^post3, lt_20^0'=lt_20^post3, lt_21^0'=lt_21^post3, lt_22^0'=lt_22^post3, lt_23^0'=lt_23^post3, lt_24^0'=lt_24^post3, lt_25^0'=lt_25^post3, result_4^0'=result_4^post3, x_5^0'=x_5^post3, (0 == 0 /\ -result_4^post3+result_4^0 == 0 /\ -e_10^post3+e_10^0 == 0 /\ -c_8^post3+c_8^0 == 0 /\ -cnt_38^post3+cnt_38^0 == 0 /\ lt_18^0-lt_18^post3 == 0 /\ lt_24^1 <= 0 /\ -a_6^post3+a_6^0 == 0 /\ lt_22^0-lt_22^post3 == 0 /\ lt_19^0-lt_19^post3 == 0 /\ -x_5^post3+x_5^0 == 0 /\ lt_23^0-lt_23^post3 == 0 /\ -lt_20^post3+lt_20^0 == 0 /\ lt_15^0-lt_15^post3 == 0 /\ lt_24^1-cnt_38^0 == 0 /\ -lt_14^post3+lt_14^0 == 0 /\ -lt_21^post3+lt_21^0 == 0 /\ g_12^0-g_12^post3 == 0 /\ b_7^0-b_7^post3 == 0 /\ -lt_17^post3+lt_17^0 == 0 /\ -lt_16^post3+lt_16^0 == 0 /\ h_13^0-h_13^post3 == 0 /\ -lt_25^1 <= 0 /\ d_9^0-d_9^post3 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ -f_11^post3+f_11^0 == 0), cost: 1 3: l3 -> l0 : a_6^0'=a_6^post4, b_7^0'=b_7^post4, c_8^0'=c_8^post4, cnt_38^0'=cnt_38^post4, d_9^0'=d_9^post4, e_10^0'=e_10^post4, f_11^0'=f_11^post4, g_12^0'=g_12^post4, h_13^0'=h_13^post4, lt_14^0'=lt_14^post4, lt_15^0'=lt_15^post4, lt_16^0'=lt_16^post4, lt_17^0'=lt_17^post4, lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_20^0'=lt_20^post4, lt_21^0'=lt_21^post4, lt_22^0'=lt_22^post4, lt_23^0'=lt_23^post4, lt_24^0'=lt_24^post4, lt_25^0'=lt_25^post4, result_4^0'=result_4^post4, x_5^0'=x_5^post4, (0 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ g_12^0-g_12^post4 == 0 /\ result_4^0-result_4^post4 == 0 /\ h_13^0-h_13^post4 == 0 /\ -lt_14^post4+lt_14^0 == 0 /\ -lt_16^post4+lt_16^0 == 0 /\ -lt_21^post4+lt_21^0 == 0 /\ -cnt_38^post4+cnt_38^0 == 0 /\ d_9^0-d_9^post4 == 0 /\ 1-lt_24^1 <= 0 /\ lt_24^1-cnt_38^0 == 0 /\ -a_6^post4+a_6^0 == 0 /\ -x_5^post4+x_5^0 == 0 /\ -lt_19^1 <= 0 /\ lt_18^1 <= 0 /\ lt_17^0-lt_17^post4 == 0 /\ c_8^0-c_8^post4 == 0 /\ lt_20^0-lt_20^post4 == 0 /\ e_10^0-e_10^post4 == 0 /\ -lt_25^1 <= 0 /\ lt_15^0-lt_15^post4 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ -f_11^post4+f_11^0 == 0 /\ -b_7^post4+b_7^0 == 0), cost: 1 4: l3 -> l1 : a_6^0'=a_6^post5, b_7^0'=b_7^post5, c_8^0'=c_8^post5, cnt_38^0'=cnt_38^post5, d_9^0'=d_9^post5, e_10^0'=e_10^post5, f_11^0'=f_11^post5, g_12^0'=g_12^post5, h_13^0'=h_13^post5, lt_14^0'=lt_14^post5, lt_15^0'=lt_15^post5, lt_16^0'=lt_16^post5, lt_17^0'=lt_17^post5, lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, lt_22^0'=lt_22^post5, lt_23^0'=lt_23^post5, lt_24^0'=lt_24^post5, lt_25^0'=lt_25^post5, result_4^0'=result_4^post5, x_5^0'=x_5^post5, (0 == 0 /\ lt_17^0-lt_17^post5 == 0 /\ lt_23^0-lt_23^post5 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ -lt_22^post5+lt_22^0 == 0 /\ lt_14^0-lt_14^post5 == 0 /\ lt_24^0-lt_24^post5 == 0 /\ e_10^0-e_10^post5 == 0 /\ h_13^0-h_13^post5 == 0 /\ -lt_16^post5+lt_16^0 == 0 /\ 1+lt_25^1 <= 0 /\ -cnt_38^post5+cnt_38^0 == 0 /\ -lt_19^1 <= 0 /\ -d_9^post5+d_9^0 == 0 /\ lt_18^1 <= 0 /\ -b_7^post5+b_7^0 == 0 /\ -a_6^post5+a_6^0 == 0 /\ f_11^0-f_11^post5 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ c_8^0-c_8^post5 == 0 /\ -x_5^post5+x_5^0 == 0 /\ -lt_15^post5+lt_15^0 == 0 /\ -g_12^post5+g_12^0 == 0), cost: 1 5: l3 -> l4 : a_6^0'=a_6^post6, b_7^0'=b_7^post6, c_8^0'=c_8^post6, cnt_38^0'=cnt_38^post6, d_9^0'=d_9^post6, e_10^0'=e_10^post6, f_11^0'=f_11^post6, g_12^0'=g_12^post6, h_13^0'=h_13^post6, lt_14^0'=lt_14^post6, lt_15^0'=lt_15^post6, lt_16^0'=lt_16^post6, lt_17^0'=lt_17^post6, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, lt_21^0'=lt_21^post6, lt_22^0'=lt_22^post6, lt_23^0'=lt_23^post6, lt_24^0'=lt_24^post6, lt_25^0'=lt_25^post6, result_4^0'=result_4^post6, x_5^0'=x_5^post6, (0 == 0 /\ -lt_14^post6+lt_14^0 == 0 /\ -f_11^post6+f_11^0 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ -a_6^post6+a_6^0 == 0 /\ -x_5^post6+x_5^0 == 0 /\ g_12^0-g_12^post6 == 0 /\ 1-lt_18^1 <= 0 /\ c_8^0-c_8^post6 == 0 /\ 1-lt_24^1 <= 0 /\ lt_24^1-cnt_38^0 == 0 /\ lt_20^0-lt_20^post6 == 0 /\ -lt_21^post6+lt_21^0 == 0 /\ -cnt_38^post6+cnt_38^0 == 0 /\ e_10^0-e_10^post6 == 0 /\ -lt_19^1 <= 0 /\ -b_7^post6+b_7^0 == 0 /\ lt_15^0-lt_15^post6 == 0 /\ -lt_25^1 <= 0 /\ -cnt_38^0+lt_25^1 == 0 /\ h_13^0-h_13^post6 == 0 /\ -result_4^post6+result_4^0 == 0 /\ -d_9^post6+d_9^0 == 0), cost: 1 7: l3 -> l5 : a_6^0'=a_6^post8, b_7^0'=b_7^post8, c_8^0'=c_8^post8, cnt_38^0'=cnt_38^post8, d_9^0'=d_9^post8, e_10^0'=e_10^post8, f_11^0'=f_11^post8, g_12^0'=g_12^post8, h_13^0'=h_13^post8, lt_14^0'=lt_14^post8, lt_15^0'=lt_15^post8, lt_16^0'=lt_16^post8, lt_17^0'=lt_17^post8, lt_18^0'=lt_18^post8, lt_19^0'=lt_19^post8, lt_20^0'=lt_20^post8, lt_21^0'=lt_21^post8, lt_22^0'=lt_22^post8, lt_23^0'=lt_23^post8, lt_24^0'=lt_24^post8, lt_25^0'=lt_25^post8, result_4^0'=result_4^post8, x_5^0'=x_5^post8, (0 == 0 /\ lt_17^0-lt_17^post8 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ -result_4^post8+result_4^0 == 0 /\ -b_7^post8+b_7^0 == 0 /\ lt_20^0-lt_20^post8 == 0 /\ -d_9^post8+d_9^0 == 0 /\ e_10^0-e_10^post8 == 0 /\ 1+lt_19^1 <= 0 /\ -x_5^post8+x_5^0 == 0 /\ 1-lt_24^1 <= 0 /\ lt_24^1-cnt_38^0 == 0 /\ -lt_18^post8+lt_18^0 == 0 /\ -g_12^post8+g_12^0 == 0 /\ -lt_16^post8+lt_16^0 == 0 /\ c_8^0-c_8^post8 == 0 /\ h_13^0-h_13^post8 == 0 /\ -a_6^post8+a_6^0 == 0 /\ -lt_25^1 <= 0 /\ lt_21^0-lt_21^post8 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ f_11^0-f_11^post8 == 0 /\ cnt_38^0-cnt_38^post8 == 0), cost: 1 9: l3 -> l6 : a_6^0'=a_6^post10, b_7^0'=b_7^post10, c_8^0'=c_8^post10, cnt_38^0'=cnt_38^post10, d_9^0'=d_9^post10, e_10^0'=e_10^post10, f_11^0'=f_11^post10, g_12^0'=g_12^post10, h_13^0'=h_13^post10, lt_14^0'=lt_14^post10, lt_15^0'=lt_15^post10, lt_16^0'=lt_16^post10, lt_17^0'=lt_17^post10, lt_18^0'=lt_18^post10, lt_19^0'=lt_19^post10, lt_20^0'=lt_20^post10, lt_21^0'=lt_21^post10, lt_22^0'=lt_22^post10, lt_23^0'=lt_23^post10, lt_24^0'=lt_24^post10, lt_25^0'=lt_25^post10, result_4^0'=result_4^post10, x_5^0'=x_5^post10, (0 == 0 /\ lt_23^0-lt_23^post10 == 0 /\ -d_9^post10+d_9^0 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ e_10^0-e_10^post10 == 0 /\ -lt_22^post10+lt_22^0 == 0 /\ 1-lt_18^1 <= 0 /\ -result_4^post10+result_4^0 == 0 /\ c_8^0-c_8^post10 == 0 /\ -x_5^post10+x_5^0 == 0 /\ -g_12^post10+g_12^0 == 0 /\ 1+lt_25^1 <= 0 /\ lt_14^0-lt_14^post10 == 0 /\ -lt_19^1 <= 0 /\ -b_7^post10+b_7^0 == 0 /\ -a_6^post10+a_6^0 == 0 /\ h_13^0-h_13^post10 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ cnt_38^0-cnt_38^post10 == 0 /\ -lt_15^post10+lt_15^0 == 0 /\ lt_24^0-lt_24^post10 == 0 /\ f_11^0-f_11^post10 == 0), cost: 1 11: l3 -> l7 : a_6^0'=a_6^post12, b_7^0'=b_7^post12, c_8^0'=c_8^post12, cnt_38^0'=cnt_38^post12, d_9^0'=d_9^post12, e_10^0'=e_10^post12, f_11^0'=f_11^post12, g_12^0'=g_12^post12, h_13^0'=h_13^post12, lt_14^0'=lt_14^post12, lt_15^0'=lt_15^post12, lt_16^0'=lt_16^post12, lt_17^0'=lt_17^post12, lt_18^0'=lt_18^post12, lt_19^0'=lt_19^post12, lt_20^0'=lt_20^post12, lt_21^0'=lt_21^post12, lt_22^0'=lt_22^post12, lt_23^0'=lt_23^post12, lt_24^0'=lt_24^post12, lt_25^0'=lt_25^post12, result_4^0'=result_4^post12, x_5^0'=x_5^post12, (0 == 0 /\ lt_22^0-lt_22^post12 == 0 /\ e_10^0-e_10^post12 == 0 /\ -x_5^post12+x_5^0 == 0 /\ -b_7^post12+b_7^0 == 0 /\ -a_6^post12+a_6^0 == 0 /\ c_8^0-c_8^post12 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ lt_16^0-lt_16^post12 == 0 /\ -h_13^post12+h_13^0 == 0 /\ -f_11^post12+f_11^0 == 0 /\ -lt_23^post12+lt_23^0 == 0 /\ 1+lt_19^1 <= 0 /\ 1+lt_25^1 <= 0 /\ -d_9^post12+d_9^0 == 0 /\ g_12^0-g_12^post12 == 0 /\ -result_4^post12+result_4^0 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ -lt_24^post12+lt_24^0 == 0 /\ -lt_17^post12+lt_17^0 == 0 /\ -cnt_38^post12+cnt_38^0 == 0 /\ lt_18^0-lt_18^post12 == 0), cost: 1 6: l4 -> l3 : a_6^0'=a_6^post7, b_7^0'=b_7^post7, c_8^0'=c_8^post7, cnt_38^0'=cnt_38^post7, d_9^0'=d_9^post7, e_10^0'=e_10^post7, f_11^0'=f_11^post7, g_12^0'=g_12^post7, h_13^0'=h_13^post7, lt_14^0'=lt_14^post7, lt_15^0'=lt_15^post7, lt_16^0'=lt_16^post7, lt_17^0'=lt_17^post7, lt_18^0'=lt_18^post7, lt_19^0'=lt_19^post7, lt_20^0'=lt_20^post7, lt_21^0'=lt_21^post7, lt_22^0'=lt_22^post7, lt_23^0'=lt_23^post7, lt_24^0'=lt_24^post7, lt_25^0'=lt_25^post7, result_4^0'=result_4^post7, x_5^0'=x_5^post7, (g_12^0-g_12^post7 == 0 /\ result_4^0-result_4^post7 == 0 /\ lt_25^0-lt_25^post7 == 0 /\ lt_18^0-lt_18^post7 == 0 /\ h_13^0-h_13^post7 == 0 /\ -cnt_38^post7+cnt_38^0 == 0 /\ -lt_24^post7+lt_24^0 == 0 /\ -lt_14^post7+lt_14^0 == 0 /\ -b_7^post7+b_7^0 == 0 /\ -x_5^post7+x_5^0 == 0 /\ -lt_17^post7+lt_17^0 == 0 /\ c_8^0-c_8^post7 == 0 /\ lt_15^0-lt_15^post7 == 0 /\ lt_19^0-lt_19^post7 == 0 /\ d_9^0-d_9^post7 == 0 /\ -lt_20^post7+lt_20^0 == 0 /\ e_10^0-e_10^post7 == 0 /\ -a_6^post7+a_6^0 == 0 /\ -f_11^post7+f_11^0 == 0 /\ -lt_21^post7+lt_21^0 == 0 /\ lt_22^0-lt_22^post7 == 0 /\ lt_23^0-lt_23^post7 == 0 /\ -lt_16^post7+lt_16^0 == 0), cost: 1 8: l5 -> l3 : a_6^0'=a_6^post9, b_7^0'=b_7^post9, c_8^0'=c_8^post9, cnt_38^0'=cnt_38^post9, d_9^0'=d_9^post9, e_10^0'=e_10^post9, f_11^0'=f_11^post9, g_12^0'=g_12^post9, h_13^0'=h_13^post9, lt_14^0'=lt_14^post9, lt_15^0'=lt_15^post9, lt_16^0'=lt_16^post9, lt_17^0'=lt_17^post9, lt_18^0'=lt_18^post9, lt_19^0'=lt_19^post9, lt_20^0'=lt_20^post9, lt_21^0'=lt_21^post9, lt_22^0'=lt_22^post9, lt_23^0'=lt_23^post9, lt_24^0'=lt_24^post9, lt_25^0'=lt_25^post9, result_4^0'=result_4^post9, x_5^0'=x_5^post9, (-cnt_38^post9+cnt_38^0 == 0 /\ -b_7^post9+b_7^0 == 0 /\ lt_14^0-lt_14^post9 == 0 /\ -a_6^post9+a_6^0 == 0 /\ -d_9^post9+d_9^0 == 0 /\ c_8^0-c_8^post9 == 0 /\ h_13^0-h_13^post9 == 0 /\ -lt_19^post9+lt_19^0 == 0 /\ -lt_16^post9+lt_16^0 == 0 /\ -result_4^post9+result_4^0 == 0 /\ -lt_21^post9+lt_21^0 == 0 /\ lt_18^0-lt_18^post9 == 0 /\ -g_12^post9+g_12^0 == 0 /\ lt_23^0-lt_23^post9 == 0 /\ lt_20^0-lt_20^post9 == 0 /\ e_10^0-e_10^post9 == 0 /\ -lt_17^post9+lt_17^0 == 0 /\ lt_15^0-lt_15^post9 == 0 /\ -lt_22^post9+lt_22^0 == 0 /\ lt_25^0-lt_25^post9 == 0 /\ -lt_24^post9+lt_24^0 == 0 /\ -x_5^post9+x_5^0 == 0 /\ -f_11^post9+f_11^0 == 0), cost: 1 10: l6 -> l3 : a_6^0'=a_6^post11, b_7^0'=b_7^post11, c_8^0'=c_8^post11, cnt_38^0'=cnt_38^post11, d_9^0'=d_9^post11, e_10^0'=e_10^post11, f_11^0'=f_11^post11, g_12^0'=g_12^post11, h_13^0'=h_13^post11, lt_14^0'=lt_14^post11, lt_15^0'=lt_15^post11, lt_16^0'=lt_16^post11, lt_17^0'=lt_17^post11, lt_18^0'=lt_18^post11, lt_19^0'=lt_19^post11, lt_20^0'=lt_20^post11, lt_21^0'=lt_21^post11, lt_22^0'=lt_22^post11, lt_23^0'=lt_23^post11, lt_24^0'=lt_24^post11, lt_25^0'=lt_25^post11, result_4^0'=result_4^post11, x_5^0'=x_5^post11, (-lt_18^post11+lt_18^0 == 0 /\ lt_20^0-lt_20^post11 == 0 /\ -result_4^post11+result_4^0 == 0 /\ -d_9^post11+d_9^0 == 0 /\ e_10^0-e_10^post11 == 0 /\ -b_7^post11+b_7^0 == 0 /\ -a_6^post11+a_6^0 == 0 /\ lt_23^0-lt_23^post11 == 0 /\ -x_5^post11+x_5^0 == 0 /\ -lt_16^post11+lt_16^0 == 0 /\ lt_24^0-lt_24^post11 == 0 /\ -g_12^post11+g_12^0 == 0 /\ lt_14^0-lt_14^post11 == 0 /\ -lt_22^post11+lt_22^0 == 0 /\ c_8^0-c_8^post11 == 0 /\ -lt_25^post11+lt_25^0 == 0 /\ h_13^0-h_13^post11 == 0 /\ -lt_21^post11+lt_21^0 == 0 /\ -lt_19^post11+lt_19^0 == 0 /\ -lt_15^post11+lt_15^0 == 0 /\ lt_17^0-lt_17^post11 == 0 /\ f_11^0-f_11^post11 == 0 /\ cnt_38^0-cnt_38^post11 == 0), cost: 1 12: l7 -> l3 : a_6^0'=a_6^post13, b_7^0'=b_7^post13, c_8^0'=c_8^post13, cnt_38^0'=cnt_38^post13, d_9^0'=d_9^post13, e_10^0'=e_10^post13, f_11^0'=f_11^post13, g_12^0'=g_12^post13, h_13^0'=h_13^post13, lt_14^0'=lt_14^post13, lt_15^0'=lt_15^post13, lt_16^0'=lt_16^post13, lt_17^0'=lt_17^post13, lt_18^0'=lt_18^post13, lt_19^0'=lt_19^post13, lt_20^0'=lt_20^post13, lt_21^0'=lt_21^post13, lt_22^0'=lt_22^post13, lt_23^0'=lt_23^post13, lt_24^0'=lt_24^post13, lt_25^0'=lt_25^post13, result_4^0'=result_4^post13, x_5^0'=x_5^post13, (lt_19^0-lt_19^post13 == 0 /\ c_8^0-c_8^post13 == 0 /\ g_12^0-g_12^post13 == 0 /\ -a_6^post13+a_6^0 == 0 /\ -b_7^post13+b_7^0 == 0 /\ h_13^0-h_13^post13 == 0 /\ -cnt_38^post13+cnt_38^0 == 0 /\ d_9^0-d_9^post13 == 0 /\ lt_22^0-lt_22^post13 == 0 /\ -lt_24^post13+lt_24^0 == 0 /\ lt_23^0-lt_23^post13 == 0 /\ lt_18^0-lt_18^post13 == 0 /\ -x_5^post13+x_5^0 == 0 /\ -lt_14^post13+lt_14^0 == 0 /\ -lt_16^post13+lt_16^0 == 0 /\ lt_25^0-lt_25^post13 == 0 /\ e_10^0-e_10^post13 == 0 /\ -result_4^post13+result_4^0 == 0 /\ -lt_21^post13+lt_21^0 == 0 /\ -f_11^post13+f_11^0 == 0 /\ lt_15^0-lt_15^post13 == 0 /\ lt_20^0-lt_20^post13 == 0 /\ -lt_17^post13+lt_17^0 == 0), cost: 1 13: l8 -> l2 : a_6^0'=a_6^post14, b_7^0'=b_7^post14, c_8^0'=c_8^post14, cnt_38^0'=cnt_38^post14, d_9^0'=d_9^post14, e_10^0'=e_10^post14, f_11^0'=f_11^post14, g_12^0'=g_12^post14, h_13^0'=h_13^post14, lt_14^0'=lt_14^post14, lt_15^0'=lt_15^post14, lt_16^0'=lt_16^post14, lt_17^0'=lt_17^post14, lt_18^0'=lt_18^post14, lt_19^0'=lt_19^post14, lt_20^0'=lt_20^post14, lt_21^0'=lt_21^post14, lt_22^0'=lt_22^post14, lt_23^0'=lt_23^post14, lt_24^0'=lt_24^post14, lt_25^0'=lt_25^post14, result_4^0'=result_4^post14, x_5^0'=x_5^post14, (c_8^0-c_8^post14 == 0 /\ -b_7^post14+b_7^0 == 0 /\ -result_4^post14+result_4^0 == 0 /\ -a_6^post14+a_6^0 == 0 /\ -cnt_38^post14+cnt_38^0 == 0 /\ lt_17^0-lt_17^post14 == 0 /\ -x_5^post14+x_5^0 == 0 /\ lt_18^0-lt_18^post14 == 0 /\ d_9^0-d_9^post14 == 0 /\ lt_15^0-lt_15^post14 == 0 /\ lt_20^0-lt_20^post14 == 0 /\ -lt_21^post14+lt_21^0 == 0 /\ -lt_25^post14+lt_25^0 == 0 /\ -lt_22^post14+lt_22^0 == 0 /\ e_10^0-e_10^post14 == 0 /\ -lt_19^post14+lt_19^0 == 0 /\ -f_11^post14+f_11^0 == 0 /\ lt_23^0-lt_23^post14 == 0 /\ -g_12^post14+g_12^0 == 0 /\ -lt_14^post14+lt_14^0 == 0 /\ -lt_16^post14+lt_16^0 == 0 /\ h_13^0-h_13^post14 == 0 /\ lt_24^0-lt_24^post14 == 0), cost: 1 Chained Linear Paths Start location: l8 Program variables: a_6^0 b_7^0 c_8^0 cnt_38^0 d_9^0 e_10^0 f_11^0 g_12^0 h_13^0 lt_14^0 lt_15^0 lt_16^0 lt_17^0 lt_18^0 lt_19^0 lt_20^0 lt_21^0 lt_22^0 lt_23^0 lt_24^0 lt_25^0 result_4^0 x_5^0 0: l0 -> l1 : a_6^0'=a_6^post1, b_7^0'=b_7^post1, c_8^0'=c_8^post1, cnt_38^0'=cnt_38^post1, d_9^0'=d_9^post1, e_10^0'=e_10^post1, f_11^0'=f_11^post1, g_12^0'=g_12^post1, h_13^0'=h_13^post1, lt_14^0'=lt_14^post1, lt_15^0'=lt_15^post1, lt_16^0'=lt_16^post1, lt_17^0'=lt_17^post1, lt_18^0'=lt_18^post1, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, lt_22^0'=lt_22^post1, lt_23^0'=lt_23^post1, lt_24^0'=lt_24^post1, lt_25^0'=lt_25^post1, result_4^0'=result_4^post1, x_5^0'=x_5^post1, (0 == 0 /\ lt_19^0-lt_19^post1 == 0 /\ -x_5^post1+x_5^0 == 0 /\ -f_11^post1+f_11^0 == 0 /\ -lt_17^post1+lt_17^0 == 0 /\ -lt_14^post1+lt_14^0 == 0 /\ -lt_16^post1+lt_16^0 == 0 /\ b_7^0-b_7^post1 == 0 /\ g_12^0-g_12^post1 == 0 /\ lt_18^0-lt_18^post1 == 0 /\ -lt_24^post1+lt_24^0 == 0 /\ lt_22^0-lt_22^post1 == 0 /\ -cnt_38^post1+cnt_38^0 == 0 /\ c_8^0-c_8^post1 == 0 /\ lt_23^0-lt_23^post1 == 0 /\ e_10^0-e_10^post1 == 0 /\ lt_25^0-lt_25^post1 == 0 /\ lt_15^0-lt_15^post1 == 0 /\ d_9^0-d_9^post1 == 0 /\ h_13^0-h_13^post1 == 0 /\ -lt_21^post1+lt_21^0 == 0 /\ -a_6^post1+a_6^0 == 0 /\ lt_20^0-lt_20^post1 == 0), cost: 1 2: l3 -> l0 : a_6^0'=a_6^post3, b_7^0'=b_7^post3, c_8^0'=c_8^post3, cnt_38^0'=cnt_38^post3, d_9^0'=d_9^post3, e_10^0'=e_10^post3, f_11^0'=f_11^post3, g_12^0'=g_12^post3, h_13^0'=h_13^post3, lt_14^0'=lt_14^post3, lt_15^0'=lt_15^post3, lt_16^0'=lt_16^post3, lt_17^0'=lt_17^post3, lt_18^0'=lt_18^post3, lt_19^0'=lt_19^post3, lt_20^0'=lt_20^post3, lt_21^0'=lt_21^post3, lt_22^0'=lt_22^post3, lt_23^0'=lt_23^post3, lt_24^0'=lt_24^post3, lt_25^0'=lt_25^post3, result_4^0'=result_4^post3, x_5^0'=x_5^post3, (0 == 0 /\ -result_4^post3+result_4^0 == 0 /\ -e_10^post3+e_10^0 == 0 /\ -c_8^post3+c_8^0 == 0 /\ -cnt_38^post3+cnt_38^0 == 0 /\ lt_18^0-lt_18^post3 == 0 /\ lt_24^1 <= 0 /\ -a_6^post3+a_6^0 == 0 /\ lt_22^0-lt_22^post3 == 0 /\ lt_19^0-lt_19^post3 == 0 /\ -x_5^post3+x_5^0 == 0 /\ lt_23^0-lt_23^post3 == 0 /\ -lt_20^post3+lt_20^0 == 0 /\ lt_15^0-lt_15^post3 == 0 /\ lt_24^1-cnt_38^0 == 0 /\ -lt_14^post3+lt_14^0 == 0 /\ -lt_21^post3+lt_21^0 == 0 /\ g_12^0-g_12^post3 == 0 /\ b_7^0-b_7^post3 == 0 /\ -lt_17^post3+lt_17^0 == 0 /\ -lt_16^post3+lt_16^0 == 0 /\ h_13^0-h_13^post3 == 0 /\ -lt_25^1 <= 0 /\ d_9^0-d_9^post3 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ -f_11^post3+f_11^0 == 0), cost: 1 3: l3 -> l0 : a_6^0'=a_6^post4, b_7^0'=b_7^post4, c_8^0'=c_8^post4, cnt_38^0'=cnt_38^post4, d_9^0'=d_9^post4, e_10^0'=e_10^post4, f_11^0'=f_11^post4, g_12^0'=g_12^post4, h_13^0'=h_13^post4, lt_14^0'=lt_14^post4, lt_15^0'=lt_15^post4, lt_16^0'=lt_16^post4, lt_17^0'=lt_17^post4, lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_20^0'=lt_20^post4, lt_21^0'=lt_21^post4, lt_22^0'=lt_22^post4, lt_23^0'=lt_23^post4, lt_24^0'=lt_24^post4, lt_25^0'=lt_25^post4, result_4^0'=result_4^post4, x_5^0'=x_5^post4, (0 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ g_12^0-g_12^post4 == 0 /\ result_4^0-result_4^post4 == 0 /\ h_13^0-h_13^post4 == 0 /\ -lt_14^post4+lt_14^0 == 0 /\ -lt_16^post4+lt_16^0 == 0 /\ -lt_21^post4+lt_21^0 == 0 /\ -cnt_38^post4+cnt_38^0 == 0 /\ d_9^0-d_9^post4 == 0 /\ 1-lt_24^1 <= 0 /\ lt_24^1-cnt_38^0 == 0 /\ -a_6^post4+a_6^0 == 0 /\ -x_5^post4+x_5^0 == 0 /\ -lt_19^1 <= 0 /\ lt_18^1 <= 0 /\ lt_17^0-lt_17^post4 == 0 /\ c_8^0-c_8^post4 == 0 /\ lt_20^0-lt_20^post4 == 0 /\ e_10^0-e_10^post4 == 0 /\ -lt_25^1 <= 0 /\ lt_15^0-lt_15^post4 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ -f_11^post4+f_11^0 == 0 /\ -b_7^post4+b_7^0 == 0), cost: 1 4: l3 -> l1 : a_6^0'=a_6^post5, b_7^0'=b_7^post5, c_8^0'=c_8^post5, cnt_38^0'=cnt_38^post5, d_9^0'=d_9^post5, e_10^0'=e_10^post5, f_11^0'=f_11^post5, g_12^0'=g_12^post5, h_13^0'=h_13^post5, lt_14^0'=lt_14^post5, lt_15^0'=lt_15^post5, lt_16^0'=lt_16^post5, lt_17^0'=lt_17^post5, lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, lt_22^0'=lt_22^post5, lt_23^0'=lt_23^post5, lt_24^0'=lt_24^post5, lt_25^0'=lt_25^post5, result_4^0'=result_4^post5, x_5^0'=x_5^post5, (0 == 0 /\ lt_17^0-lt_17^post5 == 0 /\ lt_23^0-lt_23^post5 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ -lt_22^post5+lt_22^0 == 0 /\ lt_14^0-lt_14^post5 == 0 /\ lt_24^0-lt_24^post5 == 0 /\ e_10^0-e_10^post5 == 0 /\ h_13^0-h_13^post5 == 0 /\ -lt_16^post5+lt_16^0 == 0 /\ 1+lt_25^1 <= 0 /\ -cnt_38^post5+cnt_38^0 == 0 /\ -lt_19^1 <= 0 /\ -d_9^post5+d_9^0 == 0 /\ lt_18^1 <= 0 /\ -b_7^post5+b_7^0 == 0 /\ -a_6^post5+a_6^0 == 0 /\ f_11^0-f_11^post5 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ c_8^0-c_8^post5 == 0 /\ -x_5^post5+x_5^0 == 0 /\ -lt_15^post5+lt_15^0 == 0 /\ -g_12^post5+g_12^0 == 0), cost: 1 15: l3 -> l3 : a_6^0'=a_6^post7, b_7^0'=b_7^post7, c_8^0'=c_8^post7, cnt_38^0'=cnt_38^post7, d_9^0'=d_9^post7, e_10^0'=e_10^post7, f_11^0'=f_11^post7, g_12^0'=g_12^post7, h_13^0'=h_13^post7, lt_14^0'=lt_14^post7, lt_15^0'=lt_15^post7, lt_16^0'=lt_16^post7, lt_17^0'=lt_17^post7, lt_18^0'=lt_18^post7, lt_19^0'=lt_19^post7, lt_20^0'=lt_20^post7, lt_21^0'=lt_21^post7, lt_22^0'=lt_22^post7, lt_23^0'=lt_23^post7, lt_24^0'=lt_24^post7, lt_25^0'=lt_25^post7, result_4^0'=result_4^post7, x_5^0'=x_5^post7, (0 == 0 /\ -f_11^post7+f_11^post6 == 0 /\ -lt_14^post6+lt_14^0 == 0 /\ -f_11^post6+f_11^0 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ -a_6^post6+a_6^0 == 0 /\ lt_16^post6-lt_16^post7 == 0 /\ -lt_15^post7+lt_15^post6 == 0 /\ -x_5^post6+x_5^0 == 0 /\ -lt_18^post7+lt_18^post6 == 0 /\ -lt_14^post7+lt_14^post6 == 0 /\ lt_25^post6-lt_25^post7 == 0 /\ h_13^post6-h_13^post7 == 0 /\ g_12^0-g_12^post6 == 0 /\ 1-lt_18^1 <= 0 /\ result_4^post6-result_4^post7 == 0 /\ c_8^0-c_8^post6 == 0 /\ d_9^post6-d_9^post7 == 0 /\ 1-lt_24^1 <= 0 /\ -a_6^post7+a_6^post6 == 0 /\ -cnt_38^post7+cnt_38^post6 == 0 /\ lt_23^post6-lt_23^post7 == 0 /\ -g_12^post7+g_12^post6 == 0 /\ c_8^post6-c_8^post7 == 0 /\ lt_24^1-cnt_38^0 == 0 /\ -lt_17^post7+lt_17^post6 == 0 /\ -x_5^post7+x_5^post6 == 0 /\ e_10^post6-e_10^post7 == 0 /\ lt_22^post6-lt_22^post7 == 0 /\ lt_20^0-lt_20^post6 == 0 /\ -lt_21^post6+lt_21^0 == 0 /\ -cnt_38^post6+cnt_38^0 == 0 /\ e_10^0-e_10^post6 == 0 /\ lt_19^post6-lt_19^post7 == 0 /\ -lt_19^1 <= 0 /\ -b_7^post6+b_7^0 == 0 /\ lt_15^0-lt_15^post6 == 0 /\ -lt_25^1 <= 0 /\ -lt_20^post7+lt_20^post6 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ b_7^post6-b_7^post7 == 0 /\ h_13^0-h_13^post6 == 0 /\ -result_4^post6+result_4^0 == 0 /\ -lt_21^post7+lt_21^post6 == 0 /\ lt_24^post6-lt_24^post7 == 0 /\ -d_9^post6+d_9^0 == 0), cost: 1 16: l3 -> l3 : a_6^0'=a_6^post9, b_7^0'=b_7^post9, c_8^0'=c_8^post9, cnt_38^0'=cnt_38^post9, d_9^0'=d_9^post9, e_10^0'=e_10^post9, f_11^0'=f_11^post9, g_12^0'=g_12^post9, h_13^0'=h_13^post9, lt_14^0'=lt_14^post9, lt_15^0'=lt_15^post9, lt_16^0'=lt_16^post9, lt_17^0'=lt_17^post9, lt_18^0'=lt_18^post9, lt_19^0'=lt_19^post9, lt_20^0'=lt_20^post9, lt_21^0'=lt_21^post9, lt_22^0'=lt_22^post9, lt_23^0'=lt_23^post9, lt_24^0'=lt_24^post9, lt_25^0'=lt_25^post9, result_4^0'=result_4^post9, x_5^0'=x_5^post9, (0 == 0 /\ lt_17^0-lt_17^post8 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ -result_4^post9+result_4^post8 == 0 /\ -result_4^post8+result_4^0 == 0 /\ -b_7^post8+b_7^0 == 0 /\ lt_20^0-lt_20^post8 == 0 /\ -lt_21^post9+lt_21^post8 == 0 /\ -d_9^post8+d_9^0 == 0 /\ e_10^0-e_10^post8 == 0 /\ -lt_23^post9+lt_23^post8 == 0 /\ g_12^post8-g_12^post9 == 0 /\ -lt_16^post9+lt_16^post8 == 0 /\ 1+lt_19^1 <= 0 /\ -x_5^post8+x_5^0 == 0 /\ b_7^post8-b_7^post9 == 0 /\ 1-lt_24^1 <= 0 /\ -lt_24^post9+lt_24^post8 == 0 /\ a_6^post8-a_6^post9 == 0 /\ lt_24^1-cnt_38^0 == 0 /\ d_9^post8-d_9^post9 == 0 /\ -lt_18^post8+lt_18^0 == 0 /\ -g_12^post8+g_12^0 == 0 /\ -lt_16^post8+lt_16^0 == 0 /\ -cnt_38^post9+cnt_38^post8 == 0 /\ -lt_22^post9+lt_22^post8 == 0 /\ lt_14^post8-lt_14^post9 == 0 /\ c_8^0-c_8^post8 == 0 /\ lt_15^post8-lt_15^post9 == 0 /\ -lt_17^post9+lt_17^post8 == 0 /\ lt_25^post8-lt_25^post9 == 0 /\ h_13^0-h_13^post8 == 0 /\ -a_6^post8+a_6^0 == 0 /\ -lt_25^1 <= 0 /\ c_8^post8-c_8^post9 == 0 /\ lt_21^0-lt_21^post8 == 0 /\ e_10^post8-e_10^post9 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ -f_11^post9+f_11^post8 == 0 /\ -x_5^post9+x_5^post8 == 0 /\ -lt_19^post9+lt_19^post8 == 0 /\ lt_18^post8-lt_18^post9 == 0 /\ h_13^post8-h_13^post9 == 0 /\ f_11^0-f_11^post8 == 0 /\ cnt_38^0-cnt_38^post8 == 0 /\ -lt_20^post9+lt_20^post8 == 0), cost: 1 17: l3 -> l3 : a_6^0'=a_6^post11, b_7^0'=b_7^post11, c_8^0'=c_8^post11, cnt_38^0'=cnt_38^post11, d_9^0'=d_9^post11, e_10^0'=e_10^post11, f_11^0'=f_11^post11, g_12^0'=g_12^post11, h_13^0'=h_13^post11, lt_14^0'=lt_14^post11, lt_15^0'=lt_15^post11, lt_16^0'=lt_16^post11, lt_17^0'=lt_17^post11, lt_18^0'=lt_18^post11, lt_19^0'=lt_19^post11, lt_20^0'=lt_20^post11, lt_21^0'=lt_21^post11, lt_22^0'=lt_22^post11, lt_23^0'=lt_23^post11, lt_24^0'=lt_24^post11, lt_25^0'=lt_25^post11, result_4^0'=result_4^post11, x_5^0'=x_5^post11, (0 == 0 /\ -h_13^post11+h_13^post10 == 0 /\ lt_23^post10-lt_23^post11 == 0 /\ x_5^post10-x_5^post11 == 0 /\ lt_23^0-lt_23^post10 == 0 /\ -d_9^post10+d_9^0 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ e_10^0-e_10^post10 == 0 /\ -lt_22^post10+lt_22^0 == 0 /\ 1-lt_18^1 <= 0 /\ -result_4^post10+result_4^0 == 0 /\ lt_22^post10-lt_22^post11 == 0 /\ lt_17^post10-lt_17^post11 == 0 /\ -e_10^post11+e_10^post10 == 0 /\ result_4^post10-result_4^post11 == 0 /\ c_8^0-c_8^post10 == 0 /\ b_7^post10-b_7^post11 == 0 /\ -lt_15^post11+lt_15^post10 == 0 /\ -x_5^post10+x_5^0 == 0 /\ lt_20^post10-lt_20^post11 == 0 /\ -g_12^post10+g_12^0 == 0 /\ -lt_16^post11+lt_16^post10 == 0 /\ -cnt_38^post11+cnt_38^post10 == 0 /\ 1+lt_25^1 <= 0 /\ lt_24^post10-lt_24^post11 == 0 /\ lt_14^0-lt_14^post10 == 0 /\ lt_19^post10-lt_19^post11 == 0 /\ -d_9^post11+d_9^post10 == 0 /\ -lt_19^1 <= 0 /\ -b_7^post10+b_7^0 == 0 /\ c_8^post10-c_8^post11 == 0 /\ -lt_14^post11+lt_14^post10 == 0 /\ -a_6^post10+a_6^0 == 0 /\ h_13^0-h_13^post10 == 0 /\ -lt_18^post11+lt_18^post10 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ lt_25^post10-lt_25^post11 == 0 /\ -lt_21^post11+lt_21^post10 == 0 /\ -f_11^post11+f_11^post10 == 0 /\ cnt_38^0-cnt_38^post10 == 0 /\ -g_12^post11+g_12^post10 == 0 /\ -lt_15^post10+lt_15^0 == 0 /\ a_6^post10-a_6^post11 == 0 /\ lt_24^0-lt_24^post10 == 0 /\ f_11^0-f_11^post10 == 0), cost: 1 18: l3 -> l3 : a_6^0'=a_6^post13, b_7^0'=b_7^post13, c_8^0'=c_8^post13, cnt_38^0'=cnt_38^post13, d_9^0'=d_9^post13, e_10^0'=e_10^post13, f_11^0'=f_11^post13, g_12^0'=g_12^post13, h_13^0'=h_13^post13, lt_14^0'=lt_14^post13, lt_15^0'=lt_15^post13, lt_16^0'=lt_16^post13, lt_17^0'=lt_17^post13, lt_18^0'=lt_18^post13, lt_19^0'=lt_19^post13, lt_20^0'=lt_20^post13, lt_21^0'=lt_21^post13, lt_22^0'=lt_22^post13, lt_23^0'=lt_23^post13, lt_24^0'=lt_24^post13, lt_25^0'=lt_25^post13, result_4^0'=result_4^post13, x_5^0'=x_5^post13, (0 == 0 /\ lt_22^0-lt_22^post12 == 0 /\ e_10^0-e_10^post12 == 0 /\ -x_5^post12+x_5^0 == 0 /\ -b_7^post12+b_7^0 == 0 /\ h_13^post12-h_13^post13 == 0 /\ -a_6^post12+a_6^0 == 0 /\ c_8^0-c_8^post12 == 0 /\ lt_25^post12-lt_25^post13 == 0 /\ -b_7^post13+b_7^post12 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ d_9^post12-d_9^post13 == 0 /\ lt_16^0-lt_16^post12 == 0 /\ -h_13^post12+h_13^0 == 0 /\ -f_11^post12+f_11^0 == 0 /\ cnt_38^post12-cnt_38^post13 == 0 /\ lt_20^post12-lt_20^post13 == 0 /\ -lt_23^post12+lt_23^0 == 0 /\ 1+lt_19^1 <= 0 /\ lt_14^post12-lt_14^post13 == 0 /\ lt_23^post12-lt_23^post13 == 0 /\ -lt_16^post13+lt_16^post12 == 0 /\ g_12^post12-g_12^post13 == 0 /\ 1+lt_25^1 <= 0 /\ lt_17^post12-lt_17^post13 == 0 /\ -x_5^post13+x_5^post12 == 0 /\ -d_9^post12+d_9^0 == 0 /\ lt_22^post12-lt_22^post13 == 0 /\ g_12^0-g_12^post12 == 0 /\ lt_21^post12-lt_21^post13 == 0 /\ lt_15^post12-lt_15^post13 == 0 /\ e_10^post12-e_10^post13 == 0 /\ -result_4^post12+result_4^0 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ -lt_24^post12+lt_24^0 == 0 /\ a_6^post12-a_6^post13 == 0 /\ -lt_17^post12+lt_17^0 == 0 /\ f_11^post12-f_11^post13 == 0 /\ lt_18^post12-lt_18^post13 == 0 /\ lt_19^post12-lt_19^post13 == 0 /\ -result_4^post13+result_4^post12 == 0 /\ -cnt_38^post12+cnt_38^0 == 0 /\ lt_24^post12-lt_24^post13 == 0 /\ -c_8^post13+c_8^post12 == 0 /\ lt_18^0-lt_18^post12 == 0), cost: 1 14: l8 -> l3 : a_6^0'=a_6^post2, b_7^0'=b_7^post2, c_8^0'=c_8^post2, cnt_38^0'=cnt_38^post2, d_9^0'=d_9^post2, e_10^0'=e_10^post2, f_11^0'=f_11^post2, g_12^0'=g_12^post2, h_13^0'=h_13^post2, lt_14^0'=lt_14^post2, lt_15^0'=lt_15^post2, lt_16^0'=lt_16^post2, lt_17^0'=lt_17^post2, lt_18^0'=lt_18^post2, lt_19^0'=lt_19^post2, lt_20^0'=lt_20^post2, lt_21^0'=lt_21^post2, lt_22^0'=lt_22^post2, lt_23^0'=lt_23^post2, lt_24^0'=lt_24^post2, lt_25^0'=lt_25^post2, result_4^0'=result_4^post2, x_5^0'=x_5^post2, (0 == 0 /\ c_8^0-c_8^post14 == 0 /\ lt_17^post14-lt_17^post2 == 0 /\ lt_23^post14-lt_23^post2 == 0 /\ -b_7^post14+b_7^0 == 0 /\ b_7^post2-a_6^post2 == 0 /\ -result_4^post14+result_4^0 == 0 /\ -a_6^post14+a_6^0 == 0 /\ lt_22^post14-lt_22^post2 == 0 /\ -cnt_38^post14+cnt_38^0 == 0 /\ -e_10^post2+f_11^post2 == 0 /\ g_12^post2-f_11^post2 == 0 /\ lt_15^post14-lt_15^post2 == 0 /\ lt_17^0-lt_17^post14 == 0 /\ -x_5^post14+x_5^0 == 0 /\ lt_25^post14-lt_25^post2 == 0 /\ lt_18^0-lt_18^post14 == 0 /\ d_9^0-d_9^post14 == 0 /\ lt_20^post14-lt_20^post2 == 0 /\ lt_19^post14-lt_19^post2 == 0 /\ cnt_38^post14-cnt_38^post2 == 0 /\ lt_15^0-lt_15^post14 == 0 /\ -g_12^post2+h_13^post2 == 0 /\ lt_20^0-lt_20^post14 == 0 /\ lt_14^post14-lt_14^post2 == 0 /\ -b_7^post2+c_8^post2 == 0 /\ -c_8^post2+d_9^post2 == 0 /\ -lt_21^post14+lt_21^0 == 0 /\ -lt_25^post14+lt_25^0 == 0 /\ -lt_22^post14+lt_22^0 == 0 /\ e_10^post2-d_9^post2 == 0 /\ result_4^post14-result_4^post2 == 0 /\ e_10^0-e_10^post14 == 0 /\ lt_21^post14-lt_21^post2 == 0 /\ lt_18^post14-lt_18^post2 == 0 /\ -lt_19^post14+lt_19^0 == 0 /\ -f_11^post14+f_11^0 == 0 /\ lt_23^0-lt_23^post14 == 0 /\ -g_12^post14+g_12^0 == 0 /\ lt_16^post14-lt_16^post2 == 0 /\ -lt_14^post14+lt_14^0 == 0 /\ -lt_16^post14+lt_16^0 == 0 /\ h_13^0-h_13^post14 == 0 /\ lt_24^0-lt_24^post14 == 0 /\ lt_24^post14-lt_24^post2 == 0 /\ -x_5^post2+a_6^post2 == 0), cost: 1 Eliminating location l2 by chaining: Applied chaining First rule: l8 -> l2 : a_6^0'=a_6^post14, b_7^0'=b_7^post14, c_8^0'=c_8^post14, cnt_38^0'=cnt_38^post14, d_9^0'=d_9^post14, e_10^0'=e_10^post14, f_11^0'=f_11^post14, g_12^0'=g_12^post14, h_13^0'=h_13^post14, lt_14^0'=lt_14^post14, lt_15^0'=lt_15^post14, lt_16^0'=lt_16^post14, lt_17^0'=lt_17^post14, lt_18^0'=lt_18^post14, lt_19^0'=lt_19^post14, lt_20^0'=lt_20^post14, lt_21^0'=lt_21^post14, lt_22^0'=lt_22^post14, lt_23^0'=lt_23^post14, lt_24^0'=lt_24^post14, lt_25^0'=lt_25^post14, result_4^0'=result_4^post14, x_5^0'=x_5^post14, (c_8^0-c_8^post14 == 0 /\ -b_7^post14+b_7^0 == 0 /\ -result_4^post14+result_4^0 == 0 /\ -a_6^post14+a_6^0 == 0 /\ -cnt_38^post14+cnt_38^0 == 0 /\ lt_17^0-lt_17^post14 == 0 /\ -x_5^post14+x_5^0 == 0 /\ lt_18^0-lt_18^post14 == 0 /\ d_9^0-d_9^post14 == 0 /\ lt_15^0-lt_15^post14 == 0 /\ lt_20^0-lt_20^post14 == 0 /\ -lt_21^post14+lt_21^0 == 0 /\ -lt_25^post14+lt_25^0 == 0 /\ -lt_22^post14+lt_22^0 == 0 /\ e_10^0-e_10^post14 == 0 /\ -lt_19^post14+lt_19^0 == 0 /\ -f_11^post14+f_11^0 == 0 /\ lt_23^0-lt_23^post14 == 0 /\ -g_12^post14+g_12^0 == 0 /\ -lt_14^post14+lt_14^0 == 0 /\ -lt_16^post14+lt_16^0 == 0 /\ h_13^0-h_13^post14 == 0 /\ lt_24^0-lt_24^post14 == 0), cost: 1 Second rule: l2 -> l3 : a_6^0'=a_6^post2, b_7^0'=b_7^post2, c_8^0'=c_8^post2, cnt_38^0'=cnt_38^post2, d_9^0'=d_9^post2, e_10^0'=e_10^post2, f_11^0'=f_11^post2, g_12^0'=g_12^post2, h_13^0'=h_13^post2, lt_14^0'=lt_14^post2, lt_15^0'=lt_15^post2, lt_16^0'=lt_16^post2, lt_17^0'=lt_17^post2, lt_18^0'=lt_18^post2, lt_19^0'=lt_19^post2, lt_20^0'=lt_20^post2, lt_21^0'=lt_21^post2, lt_22^0'=lt_22^post2, lt_23^0'=lt_23^post2, lt_24^0'=lt_24^post2, lt_25^0'=lt_25^post2, result_4^0'=result_4^post2, x_5^0'=x_5^post2, (0 == 0 /\ -result_4^post2+result_4^0 == 0 /\ b_7^post2-a_6^post2 == 0 /\ lt_18^0-lt_18^post2 == 0 /\ -e_10^post2+f_11^post2 == 0 /\ -cnt_38^post2+cnt_38^0 == 0 /\ g_12^post2-f_11^post2 == 0 /\ lt_17^0-lt_17^post2 == 0 /\ lt_15^0-lt_15^post2 == 0 /\ lt_20^0-lt_20^post2 == 0 /\ -g_12^post2+h_13^post2 == 0 /\ -lt_25^post2+lt_25^0 == 0 /\ -b_7^post2+c_8^post2 == 0 /\ -c_8^post2+d_9^post2 == 0 /\ -lt_22^post2+lt_22^0 == 0 /\ -lt_21^post2+lt_21^0 == 0 /\ e_10^post2-d_9^post2 == 0 /\ lt_23^0-lt_23^post2 == 0 /\ -lt_19^post2+lt_19^0 == 0 /\ -lt_16^post2+lt_16^0 == 0 /\ lt_24^0-lt_24^post2 == 0 /\ -lt_14^post2+lt_14^0 == 0 /\ -x_5^post2+a_6^post2 == 0), cost: 1 New rule: l8 -> l3 : a_6^0'=a_6^post2, b_7^0'=b_7^post2, c_8^0'=c_8^post2, cnt_38^0'=cnt_38^post2, d_9^0'=d_9^post2, e_10^0'=e_10^post2, f_11^0'=f_11^post2, g_12^0'=g_12^post2, h_13^0'=h_13^post2, lt_14^0'=lt_14^post2, lt_15^0'=lt_15^post2, lt_16^0'=lt_16^post2, lt_17^0'=lt_17^post2, lt_18^0'=lt_18^post2, lt_19^0'=lt_19^post2, lt_20^0'=lt_20^post2, lt_21^0'=lt_21^post2, lt_22^0'=lt_22^post2, lt_23^0'=lt_23^post2, lt_24^0'=lt_24^post2, lt_25^0'=lt_25^post2, result_4^0'=result_4^post2, x_5^0'=x_5^post2, (0 == 0 /\ c_8^0-c_8^post14 == 0 /\ lt_17^post14-lt_17^post2 == 0 /\ lt_23^post14-lt_23^post2 == 0 /\ -b_7^post14+b_7^0 == 0 /\ b_7^post2-a_6^post2 == 0 /\ -result_4^post14+result_4^0 == 0 /\ -a_6^post14+a_6^0 == 0 /\ lt_22^post14-lt_22^post2 == 0 /\ -cnt_38^post14+cnt_38^0 == 0 /\ -e_10^post2+f_11^post2 == 0 /\ g_12^post2-f_11^post2 == 0 /\ lt_15^post14-lt_15^post2 == 0 /\ lt_17^0-lt_17^post14 == 0 /\ -x_5^post14+x_5^0 == 0 /\ lt_25^post14-lt_25^post2 == 0 /\ lt_18^0-lt_18^post14 == 0 /\ d_9^0-d_9^post14 == 0 /\ lt_20^post14-lt_20^post2 == 0 /\ lt_19^post14-lt_19^post2 == 0 /\ cnt_38^post14-cnt_38^post2 == 0 /\ lt_15^0-lt_15^post14 == 0 /\ -g_12^post2+h_13^post2 == 0 /\ lt_20^0-lt_20^post14 == 0 /\ lt_14^post14-lt_14^post2 == 0 /\ -b_7^post2+c_8^post2 == 0 /\ -c_8^post2+d_9^post2 == 0 /\ -lt_21^post14+lt_21^0 == 0 /\ -lt_25^post14+lt_25^0 == 0 /\ -lt_22^post14+lt_22^0 == 0 /\ e_10^post2-d_9^post2 == 0 /\ result_4^post14-result_4^post2 == 0 /\ e_10^0-e_10^post14 == 0 /\ lt_21^post14-lt_21^post2 == 0 /\ lt_18^post14-lt_18^post2 == 0 /\ -lt_19^post14+lt_19^0 == 0 /\ -f_11^post14+f_11^0 == 0 /\ lt_23^0-lt_23^post14 == 0 /\ -g_12^post14+g_12^0 == 0 /\ lt_16^post14-lt_16^post2 == 0 /\ -lt_14^post14+lt_14^0 == 0 /\ -lt_16^post14+lt_16^0 == 0 /\ h_13^0-h_13^post14 == 0 /\ lt_24^0-lt_24^post14 == 0 /\ lt_24^post14-lt_24^post2 == 0 /\ -x_5^post2+a_6^post2 == 0), cost: 1 Applied deletion Removed the following rules: 1 13 Eliminating location l4 by chaining: Applied chaining First rule: l3 -> l4 : a_6^0'=a_6^post6, b_7^0'=b_7^post6, c_8^0'=c_8^post6, cnt_38^0'=cnt_38^post6, d_9^0'=d_9^post6, e_10^0'=e_10^post6, f_11^0'=f_11^post6, g_12^0'=g_12^post6, h_13^0'=h_13^post6, lt_14^0'=lt_14^post6, lt_15^0'=lt_15^post6, lt_16^0'=lt_16^post6, lt_17^0'=lt_17^post6, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, lt_21^0'=lt_21^post6, lt_22^0'=lt_22^post6, lt_23^0'=lt_23^post6, lt_24^0'=lt_24^post6, lt_25^0'=lt_25^post6, result_4^0'=result_4^post6, x_5^0'=x_5^post6, (0 == 0 /\ -lt_14^post6+lt_14^0 == 0 /\ -f_11^post6+f_11^0 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ -a_6^post6+a_6^0 == 0 /\ -x_5^post6+x_5^0 == 0 /\ g_12^0-g_12^post6 == 0 /\ 1-lt_18^1 <= 0 /\ c_8^0-c_8^post6 == 0 /\ 1-lt_24^1 <= 0 /\ lt_24^1-cnt_38^0 == 0 /\ lt_20^0-lt_20^post6 == 0 /\ -lt_21^post6+lt_21^0 == 0 /\ -cnt_38^post6+cnt_38^0 == 0 /\ e_10^0-e_10^post6 == 0 /\ -lt_19^1 <= 0 /\ -b_7^post6+b_7^0 == 0 /\ lt_15^0-lt_15^post6 == 0 /\ -lt_25^1 <= 0 /\ -cnt_38^0+lt_25^1 == 0 /\ h_13^0-h_13^post6 == 0 /\ -result_4^post6+result_4^0 == 0 /\ -d_9^post6+d_9^0 == 0), cost: 1 Second rule: l4 -> l3 : a_6^0'=a_6^post7, b_7^0'=b_7^post7, c_8^0'=c_8^post7, cnt_38^0'=cnt_38^post7, d_9^0'=d_9^post7, e_10^0'=e_10^post7, f_11^0'=f_11^post7, g_12^0'=g_12^post7, h_13^0'=h_13^post7, lt_14^0'=lt_14^post7, lt_15^0'=lt_15^post7, lt_16^0'=lt_16^post7, lt_17^0'=lt_17^post7, lt_18^0'=lt_18^post7, lt_19^0'=lt_19^post7, lt_20^0'=lt_20^post7, lt_21^0'=lt_21^post7, lt_22^0'=lt_22^post7, lt_23^0'=lt_23^post7, lt_24^0'=lt_24^post7, lt_25^0'=lt_25^post7, result_4^0'=result_4^post7, x_5^0'=x_5^post7, (g_12^0-g_12^post7 == 0 /\ result_4^0-result_4^post7 == 0 /\ lt_25^0-lt_25^post7 == 0 /\ lt_18^0-lt_18^post7 == 0 /\ h_13^0-h_13^post7 == 0 /\ -cnt_38^post7+cnt_38^0 == 0 /\ -lt_24^post7+lt_24^0 == 0 /\ -lt_14^post7+lt_14^0 == 0 /\ -b_7^post7+b_7^0 == 0 /\ -x_5^post7+x_5^0 == 0 /\ -lt_17^post7+lt_17^0 == 0 /\ c_8^0-c_8^post7 == 0 /\ lt_15^0-lt_15^post7 == 0 /\ lt_19^0-lt_19^post7 == 0 /\ d_9^0-d_9^post7 == 0 /\ -lt_20^post7+lt_20^0 == 0 /\ e_10^0-e_10^post7 == 0 /\ -a_6^post7+a_6^0 == 0 /\ -f_11^post7+f_11^0 == 0 /\ -lt_21^post7+lt_21^0 == 0 /\ lt_22^0-lt_22^post7 == 0 /\ lt_23^0-lt_23^post7 == 0 /\ -lt_16^post7+lt_16^0 == 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^post7, b_7^0'=b_7^post7, c_8^0'=c_8^post7, cnt_38^0'=cnt_38^post7, d_9^0'=d_9^post7, e_10^0'=e_10^post7, f_11^0'=f_11^post7, g_12^0'=g_12^post7, h_13^0'=h_13^post7, lt_14^0'=lt_14^post7, lt_15^0'=lt_15^post7, lt_16^0'=lt_16^post7, lt_17^0'=lt_17^post7, lt_18^0'=lt_18^post7, lt_19^0'=lt_19^post7, lt_20^0'=lt_20^post7, lt_21^0'=lt_21^post7, lt_22^0'=lt_22^post7, lt_23^0'=lt_23^post7, lt_24^0'=lt_24^post7, lt_25^0'=lt_25^post7, result_4^0'=result_4^post7, x_5^0'=x_5^post7, (0 == 0 /\ -f_11^post7+f_11^post6 == 0 /\ -lt_14^post6+lt_14^0 == 0 /\ -f_11^post6+f_11^0 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ -a_6^post6+a_6^0 == 0 /\ lt_16^post6-lt_16^post7 == 0 /\ -lt_15^post7+lt_15^post6 == 0 /\ -x_5^post6+x_5^0 == 0 /\ -lt_18^post7+lt_18^post6 == 0 /\ -lt_14^post7+lt_14^post6 == 0 /\ lt_25^post6-lt_25^post7 == 0 /\ h_13^post6-h_13^post7 == 0 /\ g_12^0-g_12^post6 == 0 /\ 1-lt_18^1 <= 0 /\ result_4^post6-result_4^post7 == 0 /\ c_8^0-c_8^post6 == 0 /\ d_9^post6-d_9^post7 == 0 /\ 1-lt_24^1 <= 0 /\ -a_6^post7+a_6^post6 == 0 /\ -cnt_38^post7+cnt_38^post6 == 0 /\ lt_23^post6-lt_23^post7 == 0 /\ -g_12^post7+g_12^post6 == 0 /\ c_8^post6-c_8^post7 == 0 /\ lt_24^1-cnt_38^0 == 0 /\ -lt_17^post7+lt_17^post6 == 0 /\ -x_5^post7+x_5^post6 == 0 /\ e_10^post6-e_10^post7 == 0 /\ lt_22^post6-lt_22^post7 == 0 /\ lt_20^0-lt_20^post6 == 0 /\ -lt_21^post6+lt_21^0 == 0 /\ -cnt_38^post6+cnt_38^0 == 0 /\ e_10^0-e_10^post6 == 0 /\ lt_19^post6-lt_19^post7 == 0 /\ -lt_19^1 <= 0 /\ -b_7^post6+b_7^0 == 0 /\ lt_15^0-lt_15^post6 == 0 /\ -lt_25^1 <= 0 /\ -lt_20^post7+lt_20^post6 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ b_7^post6-b_7^post7 == 0 /\ h_13^0-h_13^post6 == 0 /\ -result_4^post6+result_4^0 == 0 /\ -lt_21^post7+lt_21^post6 == 0 /\ lt_24^post6-lt_24^post7 == 0 /\ -d_9^post6+d_9^0 == 0), cost: 1 Applied deletion Removed the following rules: 5 6 Eliminating location l5 by chaining: Applied chaining First rule: l3 -> l5 : a_6^0'=a_6^post8, b_7^0'=b_7^post8, c_8^0'=c_8^post8, cnt_38^0'=cnt_38^post8, d_9^0'=d_9^post8, e_10^0'=e_10^post8, f_11^0'=f_11^post8, g_12^0'=g_12^post8, h_13^0'=h_13^post8, lt_14^0'=lt_14^post8, lt_15^0'=lt_15^post8, lt_16^0'=lt_16^post8, lt_17^0'=lt_17^post8, lt_18^0'=lt_18^post8, lt_19^0'=lt_19^post8, lt_20^0'=lt_20^post8, lt_21^0'=lt_21^post8, lt_22^0'=lt_22^post8, lt_23^0'=lt_23^post8, lt_24^0'=lt_24^post8, lt_25^0'=lt_25^post8, result_4^0'=result_4^post8, x_5^0'=x_5^post8, (0 == 0 /\ lt_17^0-lt_17^post8 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ -result_4^post8+result_4^0 == 0 /\ -b_7^post8+b_7^0 == 0 /\ lt_20^0-lt_20^post8 == 0 /\ -d_9^post8+d_9^0 == 0 /\ e_10^0-e_10^post8 == 0 /\ 1+lt_19^1 <= 0 /\ -x_5^post8+x_5^0 == 0 /\ 1-lt_24^1 <= 0 /\ lt_24^1-cnt_38^0 == 0 /\ -lt_18^post8+lt_18^0 == 0 /\ -g_12^post8+g_12^0 == 0 /\ -lt_16^post8+lt_16^0 == 0 /\ c_8^0-c_8^post8 == 0 /\ h_13^0-h_13^post8 == 0 /\ -a_6^post8+a_6^0 == 0 /\ -lt_25^1 <= 0 /\ lt_21^0-lt_21^post8 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ f_11^0-f_11^post8 == 0 /\ cnt_38^0-cnt_38^post8 == 0), cost: 1 Second rule: l5 -> l3 : a_6^0'=a_6^post9, b_7^0'=b_7^post9, c_8^0'=c_8^post9, cnt_38^0'=cnt_38^post9, d_9^0'=d_9^post9, e_10^0'=e_10^post9, f_11^0'=f_11^post9, g_12^0'=g_12^post9, h_13^0'=h_13^post9, lt_14^0'=lt_14^post9, lt_15^0'=lt_15^post9, lt_16^0'=lt_16^post9, lt_17^0'=lt_17^post9, lt_18^0'=lt_18^post9, lt_19^0'=lt_19^post9, lt_20^0'=lt_20^post9, lt_21^0'=lt_21^post9, lt_22^0'=lt_22^post9, lt_23^0'=lt_23^post9, lt_24^0'=lt_24^post9, lt_25^0'=lt_25^post9, result_4^0'=result_4^post9, x_5^0'=x_5^post9, (-cnt_38^post9+cnt_38^0 == 0 /\ -b_7^post9+b_7^0 == 0 /\ lt_14^0-lt_14^post9 == 0 /\ -a_6^post9+a_6^0 == 0 /\ -d_9^post9+d_9^0 == 0 /\ c_8^0-c_8^post9 == 0 /\ h_13^0-h_13^post9 == 0 /\ -lt_19^post9+lt_19^0 == 0 /\ -lt_16^post9+lt_16^0 == 0 /\ -result_4^post9+result_4^0 == 0 /\ -lt_21^post9+lt_21^0 == 0 /\ lt_18^0-lt_18^post9 == 0 /\ -g_12^post9+g_12^0 == 0 /\ lt_23^0-lt_23^post9 == 0 /\ lt_20^0-lt_20^post9 == 0 /\ e_10^0-e_10^post9 == 0 /\ -lt_17^post9+lt_17^0 == 0 /\ lt_15^0-lt_15^post9 == 0 /\ -lt_22^post9+lt_22^0 == 0 /\ lt_25^0-lt_25^post9 == 0 /\ -lt_24^post9+lt_24^0 == 0 /\ -x_5^post9+x_5^0 == 0 /\ -f_11^post9+f_11^0 == 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^post9, b_7^0'=b_7^post9, c_8^0'=c_8^post9, cnt_38^0'=cnt_38^post9, d_9^0'=d_9^post9, e_10^0'=e_10^post9, f_11^0'=f_11^post9, g_12^0'=g_12^post9, h_13^0'=h_13^post9, lt_14^0'=lt_14^post9, lt_15^0'=lt_15^post9, lt_16^0'=lt_16^post9, lt_17^0'=lt_17^post9, lt_18^0'=lt_18^post9, lt_19^0'=lt_19^post9, lt_20^0'=lt_20^post9, lt_21^0'=lt_21^post9, lt_22^0'=lt_22^post9, lt_23^0'=lt_23^post9, lt_24^0'=lt_24^post9, lt_25^0'=lt_25^post9, result_4^0'=result_4^post9, x_5^0'=x_5^post9, (0 == 0 /\ lt_17^0-lt_17^post8 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ -result_4^post9+result_4^post8 == 0 /\ -result_4^post8+result_4^0 == 0 /\ -b_7^post8+b_7^0 == 0 /\ lt_20^0-lt_20^post8 == 0 /\ -lt_21^post9+lt_21^post8 == 0 /\ -d_9^post8+d_9^0 == 0 /\ e_10^0-e_10^post8 == 0 /\ -lt_23^post9+lt_23^post8 == 0 /\ g_12^post8-g_12^post9 == 0 /\ -lt_16^post9+lt_16^post8 == 0 /\ 1+lt_19^1 <= 0 /\ -x_5^post8+x_5^0 == 0 /\ b_7^post8-b_7^post9 == 0 /\ 1-lt_24^1 <= 0 /\ -lt_24^post9+lt_24^post8 == 0 /\ a_6^post8-a_6^post9 == 0 /\ lt_24^1-cnt_38^0 == 0 /\ d_9^post8-d_9^post9 == 0 /\ -lt_18^post8+lt_18^0 == 0 /\ -g_12^post8+g_12^0 == 0 /\ -lt_16^post8+lt_16^0 == 0 /\ -cnt_38^post9+cnt_38^post8 == 0 /\ -lt_22^post9+lt_22^post8 == 0 /\ lt_14^post8-lt_14^post9 == 0 /\ c_8^0-c_8^post8 == 0 /\ lt_15^post8-lt_15^post9 == 0 /\ -lt_17^post9+lt_17^post8 == 0 /\ lt_25^post8-lt_25^post9 == 0 /\ h_13^0-h_13^post8 == 0 /\ -a_6^post8+a_6^0 == 0 /\ -lt_25^1 <= 0 /\ c_8^post8-c_8^post9 == 0 /\ lt_21^0-lt_21^post8 == 0 /\ e_10^post8-e_10^post9 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ -f_11^post9+f_11^post8 == 0 /\ -x_5^post9+x_5^post8 == 0 /\ -lt_19^post9+lt_19^post8 == 0 /\ lt_18^post8-lt_18^post9 == 0 /\ h_13^post8-h_13^post9 == 0 /\ f_11^0-f_11^post8 == 0 /\ cnt_38^0-cnt_38^post8 == 0 /\ -lt_20^post9+lt_20^post8 == 0), cost: 1 Applied deletion Removed the following rules: 7 8 Eliminating location l6 by chaining: Applied chaining First rule: l3 -> l6 : a_6^0'=a_6^post10, b_7^0'=b_7^post10, c_8^0'=c_8^post10, cnt_38^0'=cnt_38^post10, d_9^0'=d_9^post10, e_10^0'=e_10^post10, f_11^0'=f_11^post10, g_12^0'=g_12^post10, h_13^0'=h_13^post10, lt_14^0'=lt_14^post10, lt_15^0'=lt_15^post10, lt_16^0'=lt_16^post10, lt_17^0'=lt_17^post10, lt_18^0'=lt_18^post10, lt_19^0'=lt_19^post10, lt_20^0'=lt_20^post10, lt_21^0'=lt_21^post10, lt_22^0'=lt_22^post10, lt_23^0'=lt_23^post10, lt_24^0'=lt_24^post10, lt_25^0'=lt_25^post10, result_4^0'=result_4^post10, x_5^0'=x_5^post10, (0 == 0 /\ lt_23^0-lt_23^post10 == 0 /\ -d_9^post10+d_9^0 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ e_10^0-e_10^post10 == 0 /\ -lt_22^post10+lt_22^0 == 0 /\ 1-lt_18^1 <= 0 /\ -result_4^post10+result_4^0 == 0 /\ c_8^0-c_8^post10 == 0 /\ -x_5^post10+x_5^0 == 0 /\ -g_12^post10+g_12^0 == 0 /\ 1+lt_25^1 <= 0 /\ lt_14^0-lt_14^post10 == 0 /\ -lt_19^1 <= 0 /\ -b_7^post10+b_7^0 == 0 /\ -a_6^post10+a_6^0 == 0 /\ h_13^0-h_13^post10 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ cnt_38^0-cnt_38^post10 == 0 /\ -lt_15^post10+lt_15^0 == 0 /\ lt_24^0-lt_24^post10 == 0 /\ f_11^0-f_11^post10 == 0), cost: 1 Second rule: l6 -> l3 : a_6^0'=a_6^post11, b_7^0'=b_7^post11, c_8^0'=c_8^post11, cnt_38^0'=cnt_38^post11, d_9^0'=d_9^post11, e_10^0'=e_10^post11, f_11^0'=f_11^post11, g_12^0'=g_12^post11, h_13^0'=h_13^post11, lt_14^0'=lt_14^post11, lt_15^0'=lt_15^post11, lt_16^0'=lt_16^post11, lt_17^0'=lt_17^post11, lt_18^0'=lt_18^post11, lt_19^0'=lt_19^post11, lt_20^0'=lt_20^post11, lt_21^0'=lt_21^post11, lt_22^0'=lt_22^post11, lt_23^0'=lt_23^post11, lt_24^0'=lt_24^post11, lt_25^0'=lt_25^post11, result_4^0'=result_4^post11, x_5^0'=x_5^post11, (-lt_18^post11+lt_18^0 == 0 /\ lt_20^0-lt_20^post11 == 0 /\ -result_4^post11+result_4^0 == 0 /\ -d_9^post11+d_9^0 == 0 /\ e_10^0-e_10^post11 == 0 /\ -b_7^post11+b_7^0 == 0 /\ -a_6^post11+a_6^0 == 0 /\ lt_23^0-lt_23^post11 == 0 /\ -x_5^post11+x_5^0 == 0 /\ -lt_16^post11+lt_16^0 == 0 /\ lt_24^0-lt_24^post11 == 0 /\ -g_12^post11+g_12^0 == 0 /\ lt_14^0-lt_14^post11 == 0 /\ -lt_22^post11+lt_22^0 == 0 /\ c_8^0-c_8^post11 == 0 /\ -lt_25^post11+lt_25^0 == 0 /\ h_13^0-h_13^post11 == 0 /\ -lt_21^post11+lt_21^0 == 0 /\ -lt_19^post11+lt_19^0 == 0 /\ -lt_15^post11+lt_15^0 == 0 /\ lt_17^0-lt_17^post11 == 0 /\ f_11^0-f_11^post11 == 0 /\ cnt_38^0-cnt_38^post11 == 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^post11, b_7^0'=b_7^post11, c_8^0'=c_8^post11, cnt_38^0'=cnt_38^post11, d_9^0'=d_9^post11, e_10^0'=e_10^post11, f_11^0'=f_11^post11, g_12^0'=g_12^post11, h_13^0'=h_13^post11, lt_14^0'=lt_14^post11, lt_15^0'=lt_15^post11, lt_16^0'=lt_16^post11, lt_17^0'=lt_17^post11, lt_18^0'=lt_18^post11, lt_19^0'=lt_19^post11, lt_20^0'=lt_20^post11, lt_21^0'=lt_21^post11, lt_22^0'=lt_22^post11, lt_23^0'=lt_23^post11, lt_24^0'=lt_24^post11, lt_25^0'=lt_25^post11, result_4^0'=result_4^post11, x_5^0'=x_5^post11, (0 == 0 /\ -h_13^post11+h_13^post10 == 0 /\ lt_23^post10-lt_23^post11 == 0 /\ x_5^post10-x_5^post11 == 0 /\ lt_23^0-lt_23^post10 == 0 /\ -d_9^post10+d_9^0 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ e_10^0-e_10^post10 == 0 /\ -lt_22^post10+lt_22^0 == 0 /\ 1-lt_18^1 <= 0 /\ -result_4^post10+result_4^0 == 0 /\ lt_22^post10-lt_22^post11 == 0 /\ lt_17^post10-lt_17^post11 == 0 /\ -e_10^post11+e_10^post10 == 0 /\ result_4^post10-result_4^post11 == 0 /\ c_8^0-c_8^post10 == 0 /\ b_7^post10-b_7^post11 == 0 /\ -lt_15^post11+lt_15^post10 == 0 /\ -x_5^post10+x_5^0 == 0 /\ lt_20^post10-lt_20^post11 == 0 /\ -g_12^post10+g_12^0 == 0 /\ -lt_16^post11+lt_16^post10 == 0 /\ -cnt_38^post11+cnt_38^post10 == 0 /\ 1+lt_25^1 <= 0 /\ lt_24^post10-lt_24^post11 == 0 /\ lt_14^0-lt_14^post10 == 0 /\ lt_19^post10-lt_19^post11 == 0 /\ -d_9^post11+d_9^post10 == 0 /\ -lt_19^1 <= 0 /\ -b_7^post10+b_7^0 == 0 /\ c_8^post10-c_8^post11 == 0 /\ -lt_14^post11+lt_14^post10 == 0 /\ -a_6^post10+a_6^0 == 0 /\ h_13^0-h_13^post10 == 0 /\ -lt_18^post11+lt_18^post10 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ lt_25^post10-lt_25^post11 == 0 /\ -lt_21^post11+lt_21^post10 == 0 /\ -f_11^post11+f_11^post10 == 0 /\ cnt_38^0-cnt_38^post10 == 0 /\ -g_12^post11+g_12^post10 == 0 /\ -lt_15^post10+lt_15^0 == 0 /\ a_6^post10-a_6^post11 == 0 /\ lt_24^0-lt_24^post10 == 0 /\ f_11^0-f_11^post10 == 0), cost: 1 Applied deletion Removed the following rules: 9 10 Eliminating location l7 by chaining: Applied chaining First rule: l3 -> l7 : a_6^0'=a_6^post12, b_7^0'=b_7^post12, c_8^0'=c_8^post12, cnt_38^0'=cnt_38^post12, d_9^0'=d_9^post12, e_10^0'=e_10^post12, f_11^0'=f_11^post12, g_12^0'=g_12^post12, h_13^0'=h_13^post12, lt_14^0'=lt_14^post12, lt_15^0'=lt_15^post12, lt_16^0'=lt_16^post12, lt_17^0'=lt_17^post12, lt_18^0'=lt_18^post12, lt_19^0'=lt_19^post12, lt_20^0'=lt_20^post12, lt_21^0'=lt_21^post12, lt_22^0'=lt_22^post12, lt_23^0'=lt_23^post12, lt_24^0'=lt_24^post12, lt_25^0'=lt_25^post12, result_4^0'=result_4^post12, x_5^0'=x_5^post12, (0 == 0 /\ lt_22^0-lt_22^post12 == 0 /\ e_10^0-e_10^post12 == 0 /\ -x_5^post12+x_5^0 == 0 /\ -b_7^post12+b_7^0 == 0 /\ -a_6^post12+a_6^0 == 0 /\ c_8^0-c_8^post12 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ lt_16^0-lt_16^post12 == 0 /\ -h_13^post12+h_13^0 == 0 /\ -f_11^post12+f_11^0 == 0 /\ -lt_23^post12+lt_23^0 == 0 /\ 1+lt_19^1 <= 0 /\ 1+lt_25^1 <= 0 /\ -d_9^post12+d_9^0 == 0 /\ g_12^0-g_12^post12 == 0 /\ -result_4^post12+result_4^0 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ -lt_24^post12+lt_24^0 == 0 /\ -lt_17^post12+lt_17^0 == 0 /\ -cnt_38^post12+cnt_38^0 == 0 /\ lt_18^0-lt_18^post12 == 0), cost: 1 Second rule: l7 -> l3 : a_6^0'=a_6^post13, b_7^0'=b_7^post13, c_8^0'=c_8^post13, cnt_38^0'=cnt_38^post13, d_9^0'=d_9^post13, e_10^0'=e_10^post13, f_11^0'=f_11^post13, g_12^0'=g_12^post13, h_13^0'=h_13^post13, lt_14^0'=lt_14^post13, lt_15^0'=lt_15^post13, lt_16^0'=lt_16^post13, lt_17^0'=lt_17^post13, lt_18^0'=lt_18^post13, lt_19^0'=lt_19^post13, lt_20^0'=lt_20^post13, lt_21^0'=lt_21^post13, lt_22^0'=lt_22^post13, lt_23^0'=lt_23^post13, lt_24^0'=lt_24^post13, lt_25^0'=lt_25^post13, result_4^0'=result_4^post13, x_5^0'=x_5^post13, (lt_19^0-lt_19^post13 == 0 /\ c_8^0-c_8^post13 == 0 /\ g_12^0-g_12^post13 == 0 /\ -a_6^post13+a_6^0 == 0 /\ -b_7^post13+b_7^0 == 0 /\ h_13^0-h_13^post13 == 0 /\ -cnt_38^post13+cnt_38^0 == 0 /\ d_9^0-d_9^post13 == 0 /\ lt_22^0-lt_22^post13 == 0 /\ -lt_24^post13+lt_24^0 == 0 /\ lt_23^0-lt_23^post13 == 0 /\ lt_18^0-lt_18^post13 == 0 /\ -x_5^post13+x_5^0 == 0 /\ -lt_14^post13+lt_14^0 == 0 /\ -lt_16^post13+lt_16^0 == 0 /\ lt_25^0-lt_25^post13 == 0 /\ e_10^0-e_10^post13 == 0 /\ -result_4^post13+result_4^0 == 0 /\ -lt_21^post13+lt_21^0 == 0 /\ -f_11^post13+f_11^0 == 0 /\ lt_15^0-lt_15^post13 == 0 /\ lt_20^0-lt_20^post13 == 0 /\ -lt_17^post13+lt_17^0 == 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^post13, b_7^0'=b_7^post13, c_8^0'=c_8^post13, cnt_38^0'=cnt_38^post13, d_9^0'=d_9^post13, e_10^0'=e_10^post13, f_11^0'=f_11^post13, g_12^0'=g_12^post13, h_13^0'=h_13^post13, lt_14^0'=lt_14^post13, lt_15^0'=lt_15^post13, lt_16^0'=lt_16^post13, lt_17^0'=lt_17^post13, lt_18^0'=lt_18^post13, lt_19^0'=lt_19^post13, lt_20^0'=lt_20^post13, lt_21^0'=lt_21^post13, lt_22^0'=lt_22^post13, lt_23^0'=lt_23^post13, lt_24^0'=lt_24^post13, lt_25^0'=lt_25^post13, result_4^0'=result_4^post13, x_5^0'=x_5^post13, (0 == 0 /\ lt_22^0-lt_22^post12 == 0 /\ e_10^0-e_10^post12 == 0 /\ -x_5^post12+x_5^0 == 0 /\ -b_7^post12+b_7^0 == 0 /\ h_13^post12-h_13^post13 == 0 /\ -a_6^post12+a_6^0 == 0 /\ c_8^0-c_8^post12 == 0 /\ lt_25^post12-lt_25^post13 == 0 /\ -b_7^post13+b_7^post12 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ d_9^post12-d_9^post13 == 0 /\ lt_16^0-lt_16^post12 == 0 /\ -h_13^post12+h_13^0 == 0 /\ -f_11^post12+f_11^0 == 0 /\ cnt_38^post12-cnt_38^post13 == 0 /\ lt_20^post12-lt_20^post13 == 0 /\ -lt_23^post12+lt_23^0 == 0 /\ 1+lt_19^1 <= 0 /\ lt_14^post12-lt_14^post13 == 0 /\ lt_23^post12-lt_23^post13 == 0 /\ -lt_16^post13+lt_16^post12 == 0 /\ g_12^post12-g_12^post13 == 0 /\ 1+lt_25^1 <= 0 /\ lt_17^post12-lt_17^post13 == 0 /\ -x_5^post13+x_5^post12 == 0 /\ -d_9^post12+d_9^0 == 0 /\ lt_22^post12-lt_22^post13 == 0 /\ g_12^0-g_12^post12 == 0 /\ lt_21^post12-lt_21^post13 == 0 /\ lt_15^post12-lt_15^post13 == 0 /\ e_10^post12-e_10^post13 == 0 /\ -result_4^post12+result_4^0 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ -lt_24^post12+lt_24^0 == 0 /\ a_6^post12-a_6^post13 == 0 /\ -lt_17^post12+lt_17^0 == 0 /\ f_11^post12-f_11^post13 == 0 /\ lt_18^post12-lt_18^post13 == 0 /\ lt_19^post12-lt_19^post13 == 0 /\ -result_4^post13+result_4^post12 == 0 /\ -cnt_38^post12+cnt_38^0 == 0 /\ lt_24^post12-lt_24^post13 == 0 /\ -c_8^post13+c_8^post12 == 0 /\ lt_18^0-lt_18^post12 == 0), cost: 1 Applied deletion Removed the following rules: 11 12 Simplified Transitions Start location: l8 Program variables: a_6^0 b_7^0 c_8^0 cnt_38^0 d_9^0 e_10^0 f_11^0 g_12^0 h_13^0 lt_14^0 lt_15^0 lt_16^0 lt_17^0 lt_18^0 lt_19^0 lt_20^0 lt_21^0 lt_22^0 lt_23^0 lt_24^0 lt_25^0 result_4^0 x_5^0 19: l0 -> l1 : result_4^0'=result_4^post1, T, cost: 1 20: l3 -> l0 : lt_24^0'=lt_24^post3, lt_25^0'=lt_25^post3, (-cnt_38^0 <= 0 /\ cnt_38^0 <= 0), cost: 1 21: l3 -> l0 : lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_22^0'=lt_22^post4, lt_23^0'=lt_23^post4, lt_24^0'=lt_24^post4, lt_25^0'=lt_25^post4, (-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 22: l3 -> l1 : lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, lt_25^0'=lt_25^post5, result_4^0'=result_4^post5, (1+cnt_38^0 <= 0), cost: 1 24: l3 -> l3 : lt_16^0'=lt_16^post6, lt_17^0'=lt_17^post6, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_22^0'=lt_22^post6, lt_23^0'=lt_23^post6, lt_24^0'=lt_24^post6, lt_25^0'=lt_25^post6, (-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 25: l3 -> l3 : lt_14^0'=lt_14^post8, lt_15^0'=lt_15^post8, lt_19^0'=lt_19^post8, lt_22^0'=lt_22^post8, lt_23^0'=lt_23^post8, lt_24^0'=lt_24^post8, lt_25^0'=lt_25^post8, (-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 26: l3 -> l3 : lt_16^0'=lt_16^post10, lt_17^0'=lt_17^post10, lt_18^0'=lt_18^post10, lt_19^0'=lt_19^post10, lt_20^0'=lt_20^post10, lt_21^0'=lt_21^post10, lt_25^0'=lt_25^post10, (1+cnt_38^0 <= 0), cost: 1 27: l3 -> l3 : lt_14^0'=lt_14^post12, lt_15^0'=lt_15^post12, lt_19^0'=lt_19^post12, lt_20^0'=lt_20^post12, lt_21^0'=lt_21^post12, lt_25^0'=lt_25^post12, (1+cnt_38^0 <= 0), cost: 1 23: l8 -> l3 : a_6^0'=x_5^post2, b_7^0'=x_5^post2, c_8^0'=x_5^post2, d_9^0'=x_5^post2, e_10^0'=x_5^post2, f_11^0'=x_5^post2, g_12^0'=x_5^post2, h_13^0'=x_5^post2, x_5^0'=x_5^post2, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : a_6^0'=a_6^post1, b_7^0'=b_7^post1, c_8^0'=c_8^post1, cnt_38^0'=cnt_38^post1, d_9^0'=d_9^post1, e_10^0'=e_10^post1, f_11^0'=f_11^post1, g_12^0'=g_12^post1, h_13^0'=h_13^post1, lt_14^0'=lt_14^post1, lt_15^0'=lt_15^post1, lt_16^0'=lt_16^post1, lt_17^0'=lt_17^post1, lt_18^0'=lt_18^post1, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, lt_22^0'=lt_22^post1, lt_23^0'=lt_23^post1, lt_24^0'=lt_24^post1, lt_25^0'=lt_25^post1, result_4^0'=result_4^post1, x_5^0'=x_5^post1, (0 == 0 /\ lt_19^0-lt_19^post1 == 0 /\ -x_5^post1+x_5^0 == 0 /\ -f_11^post1+f_11^0 == 0 /\ -lt_17^post1+lt_17^0 == 0 /\ -lt_14^post1+lt_14^0 == 0 /\ -lt_16^post1+lt_16^0 == 0 /\ b_7^0-b_7^post1 == 0 /\ g_12^0-g_12^post1 == 0 /\ lt_18^0-lt_18^post1 == 0 /\ -lt_24^post1+lt_24^0 == 0 /\ lt_22^0-lt_22^post1 == 0 /\ -cnt_38^post1+cnt_38^0 == 0 /\ c_8^0-c_8^post1 == 0 /\ lt_23^0-lt_23^post1 == 0 /\ e_10^0-e_10^post1 == 0 /\ lt_25^0-lt_25^post1 == 0 /\ lt_15^0-lt_15^post1 == 0 /\ d_9^0-d_9^post1 == 0 /\ h_13^0-h_13^post1 == 0 /\ -lt_21^post1+lt_21^0 == 0 /\ -a_6^post1+a_6^0 == 0 /\ lt_20^0-lt_20^post1 == 0), cost: 1 New rule: l0 -> l1 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^0, result_4^0'=result_4^post1, x_5^0'=x_5^0, 0 == 0, cost: 1 propagated equality lt_19^post1 = lt_19^0 propagated equality x_5^post1 = x_5^0 propagated equality f_11^post1 = f_11^0 propagated equality lt_17^post1 = lt_17^0 propagated equality lt_14^post1 = lt_14^0 propagated equality lt_16^post1 = lt_16^0 propagated equality b_7^post1 = b_7^0 propagated equality g_12^post1 = g_12^0 propagated equality lt_18^post1 = lt_18^0 propagated equality lt_24^post1 = lt_24^0 propagated equality lt_22^post1 = lt_22^0 propagated equality cnt_38^post1 = cnt_38^0 propagated equality c_8^post1 = c_8^0 propagated equality lt_23^post1 = lt_23^0 propagated equality e_10^post1 = e_10^0 propagated equality lt_25^post1 = lt_25^0 propagated equality lt_15^post1 = lt_15^0 propagated equality d_9^post1 = d_9^0 propagated equality h_13^post1 = h_13^0 propagated equality lt_21^post1 = lt_21^0 propagated equality a_6^post1 = a_6^0 propagated equality lt_20^post1 = lt_20^0 Simplified Guard Original rule: l0 -> l1 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^0, result_4^0'=result_4^post1, x_5^0'=x_5^0, 0 == 0, cost: 1 New rule: l0 -> l1 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^0, result_4^0'=result_4^post1, x_5^0'=x_5^0, T, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^0, result_4^0'=result_4^post1, x_5^0'=x_5^0, T, cost: 1 New rule: l0 -> l1 : result_4^0'=result_4^post1, T, cost: 1 Propagated Equalities Original rule: l3 -> l0 : a_6^0'=a_6^post3, b_7^0'=b_7^post3, c_8^0'=c_8^post3, cnt_38^0'=cnt_38^post3, d_9^0'=d_9^post3, e_10^0'=e_10^post3, f_11^0'=f_11^post3, g_12^0'=g_12^post3, h_13^0'=h_13^post3, lt_14^0'=lt_14^post3, lt_15^0'=lt_15^post3, lt_16^0'=lt_16^post3, lt_17^0'=lt_17^post3, lt_18^0'=lt_18^post3, lt_19^0'=lt_19^post3, lt_20^0'=lt_20^post3, lt_21^0'=lt_21^post3, lt_22^0'=lt_22^post3, lt_23^0'=lt_23^post3, lt_24^0'=lt_24^post3, lt_25^0'=lt_25^post3, result_4^0'=result_4^post3, x_5^0'=x_5^post3, (0 == 0 /\ -result_4^post3+result_4^0 == 0 /\ -e_10^post3+e_10^0 == 0 /\ -c_8^post3+c_8^0 == 0 /\ -cnt_38^post3+cnt_38^0 == 0 /\ lt_18^0-lt_18^post3 == 0 /\ lt_24^1 <= 0 /\ -a_6^post3+a_6^0 == 0 /\ lt_22^0-lt_22^post3 == 0 /\ lt_19^0-lt_19^post3 == 0 /\ -x_5^post3+x_5^0 == 0 /\ lt_23^0-lt_23^post3 == 0 /\ -lt_20^post3+lt_20^0 == 0 /\ lt_15^0-lt_15^post3 == 0 /\ lt_24^1-cnt_38^0 == 0 /\ -lt_14^post3+lt_14^0 == 0 /\ -lt_21^post3+lt_21^0 == 0 /\ g_12^0-g_12^post3 == 0 /\ b_7^0-b_7^post3 == 0 /\ -lt_17^post3+lt_17^0 == 0 /\ -lt_16^post3+lt_16^0 == 0 /\ h_13^0-h_13^post3 == 0 /\ -lt_25^1 <= 0 /\ d_9^0-d_9^post3 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ -f_11^post3+f_11^0 == 0), cost: 1 New rule: l3 -> l0 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^post3, lt_25^0'=lt_25^post3, result_4^0'=result_4^0, x_5^0'=x_5^0, (0 == 0 /\ lt_24^1 <= 0 /\ lt_24^1-cnt_38^0 == 0 /\ -lt_25^1 <= 0 /\ -cnt_38^0+lt_25^1 == 0), cost: 1 propagated equality result_4^post3 = result_4^0 propagated equality e_10^post3 = e_10^0 propagated equality c_8^post3 = c_8^0 propagated equality cnt_38^post3 = cnt_38^0 propagated equality lt_18^post3 = lt_18^0 propagated equality a_6^post3 = a_6^0 propagated equality lt_22^post3 = lt_22^0 propagated equality lt_19^post3 = lt_19^0 propagated equality x_5^post3 = x_5^0 propagated equality lt_23^post3 = lt_23^0 propagated equality lt_20^post3 = lt_20^0 propagated equality lt_15^post3 = lt_15^0 propagated equality lt_14^post3 = lt_14^0 propagated equality lt_21^post3 = lt_21^0 propagated equality g_12^post3 = g_12^0 propagated equality b_7^post3 = b_7^0 propagated equality lt_17^post3 = lt_17^0 propagated equality lt_16^post3 = lt_16^0 propagated equality h_13^post3 = h_13^0 propagated equality d_9^post3 = d_9^0 propagated equality f_11^post3 = f_11^0 Propagated Equalities Original rule: l3 -> l0 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^post3, lt_25^0'=lt_25^post3, result_4^0'=result_4^0, x_5^0'=x_5^0, (0 == 0 /\ lt_24^1 <= 0 /\ lt_24^1-cnt_38^0 == 0 /\ -lt_25^1 <= 0 /\ -cnt_38^0+lt_25^1 == 0), cost: 1 New rule: l3 -> l0 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^post3, lt_25^0'=lt_25^post3, result_4^0'=result_4^0, x_5^0'=x_5^0, (0 == 0 /\ -cnt_38^0 <= 0 /\ cnt_38^0 <= 0), cost: 1 propagated equality lt_24^1 = cnt_38^0 propagated equality lt_25^1 = cnt_38^0 Simplified Guard Original rule: l3 -> l0 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^post3, lt_25^0'=lt_25^post3, result_4^0'=result_4^0, x_5^0'=x_5^0, (0 == 0 /\ -cnt_38^0 <= 0 /\ cnt_38^0 <= 0), cost: 1 New rule: l3 -> l0 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^post3, lt_25^0'=lt_25^post3, result_4^0'=result_4^0, x_5^0'=x_5^0, (-cnt_38^0 <= 0 /\ cnt_38^0 <= 0), cost: 1 made implied equalities explicit Original rule: l3 -> l0 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^post3, lt_25^0'=lt_25^post3, result_4^0'=result_4^0, x_5^0'=x_5^0, (-cnt_38^0 <= 0 /\ cnt_38^0 <= 0), cost: 1 New rule: l3 -> l0 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^post3, lt_25^0'=lt_25^post3, result_4^0'=result_4^0, x_5^0'=x_5^0, (-cnt_38^0 <= 0 /\ -cnt_38^0 == 0 /\ cnt_38^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l3 -> l0 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^post3, lt_25^0'=lt_25^post3, result_4^0'=result_4^0, x_5^0'=x_5^0, (-cnt_38^0 <= 0 /\ cnt_38^0 <= 0), cost: 1 New rule: l3 -> l0 : lt_24^0'=lt_24^post3, lt_25^0'=lt_25^post3, (-cnt_38^0 <= 0 /\ cnt_38^0 <= 0), cost: 1 Propagated Equalities Original rule: l3 -> l0 : a_6^0'=a_6^post4, b_7^0'=b_7^post4, c_8^0'=c_8^post4, cnt_38^0'=cnt_38^post4, d_9^0'=d_9^post4, e_10^0'=e_10^post4, f_11^0'=f_11^post4, g_12^0'=g_12^post4, h_13^0'=h_13^post4, lt_14^0'=lt_14^post4, lt_15^0'=lt_15^post4, lt_16^0'=lt_16^post4, lt_17^0'=lt_17^post4, lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_20^0'=lt_20^post4, lt_21^0'=lt_21^post4, lt_22^0'=lt_22^post4, lt_23^0'=lt_23^post4, lt_24^0'=lt_24^post4, lt_25^0'=lt_25^post4, result_4^0'=result_4^post4, x_5^0'=x_5^post4, (0 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ g_12^0-g_12^post4 == 0 /\ result_4^0-result_4^post4 == 0 /\ h_13^0-h_13^post4 == 0 /\ -lt_14^post4+lt_14^0 == 0 /\ -lt_16^post4+lt_16^0 == 0 /\ -lt_21^post4+lt_21^0 == 0 /\ -cnt_38^post4+cnt_38^0 == 0 /\ d_9^0-d_9^post4 == 0 /\ 1-lt_24^1 <= 0 /\ lt_24^1-cnt_38^0 == 0 /\ -a_6^post4+a_6^0 == 0 /\ -x_5^post4+x_5^0 == 0 /\ -lt_19^1 <= 0 /\ lt_18^1 <= 0 /\ lt_17^0-lt_17^post4 == 0 /\ c_8^0-c_8^post4 == 0 /\ lt_20^0-lt_20^post4 == 0 /\ e_10^0-e_10^post4 == 0 /\ -lt_25^1 <= 0 /\ lt_15^0-lt_15^post4 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ -f_11^post4+f_11^0 == 0 /\ -b_7^post4+b_7^0 == 0), cost: 1 New rule: l3 -> l0 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post4, lt_23^0'=lt_23^post4, lt_24^0'=lt_24^post4, lt_25^0'=lt_25^post4, result_4^0'=result_4^0, x_5^0'=x_5^0, (0 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ 1-lt_24^1 <= 0 /\ lt_24^1-cnt_38^0 == 0 /\ -lt_19^1 <= 0 /\ lt_18^1 <= 0 /\ -lt_25^1 <= 0 /\ -cnt_38^0+lt_25^1 == 0), cost: 1 propagated equality g_12^post4 = g_12^0 propagated equality result_4^post4 = result_4^0 propagated equality h_13^post4 = h_13^0 propagated equality lt_14^post4 = lt_14^0 propagated equality lt_16^post4 = lt_16^0 propagated equality lt_21^post4 = lt_21^0 propagated equality cnt_38^post4 = cnt_38^0 propagated equality d_9^post4 = d_9^0 propagated equality a_6^post4 = a_6^0 propagated equality x_5^post4 = x_5^0 propagated equality lt_17^post4 = lt_17^0 propagated equality c_8^post4 = c_8^0 propagated equality lt_20^post4 = lt_20^0 propagated equality e_10^post4 = e_10^0 propagated equality lt_15^post4 = lt_15^0 propagated equality f_11^post4 = f_11^0 propagated equality b_7^post4 = b_7^0 Propagated Equalities Original rule: l3 -> l0 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post4, lt_23^0'=lt_23^post4, lt_24^0'=lt_24^post4, lt_25^0'=lt_25^post4, result_4^0'=result_4^0, x_5^0'=x_5^0, (0 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ 1-lt_24^1 <= 0 /\ lt_24^1-cnt_38^0 == 0 /\ -lt_19^1 <= 0 /\ lt_18^1 <= 0 /\ -lt_25^1 <= 0 /\ -cnt_38^0+lt_25^1 == 0), cost: 1 New rule: l3 -> l0 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post4, lt_23^0'=lt_23^post4, lt_24^0'=lt_24^post4, lt_25^0'=lt_25^post4, result_4^0'=result_4^0, x_5^0'=x_5^0, (0 == 0 /\ -lt_19^1 <= 0 /\ lt_18^1 <= 0 /\ -cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 propagated equality lt_23^1 = cnt_38^0 propagated equality lt_24^1 = cnt_38^0 propagated equality lt_25^1 = cnt_38^0 Simplified Guard Original rule: l3 -> l0 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post4, lt_23^0'=lt_23^post4, lt_24^0'=lt_24^post4, lt_25^0'=lt_25^post4, result_4^0'=result_4^0, x_5^0'=x_5^0, (0 == 0 /\ -lt_19^1 <= 0 /\ lt_18^1 <= 0 /\ -cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 New rule: l3 -> l0 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post4, lt_23^0'=lt_23^post4, lt_24^0'=lt_24^post4, lt_25^0'=lt_25^post4, result_4^0'=result_4^0, x_5^0'=x_5^0, (-lt_19^1 <= 0 /\ lt_18^1 <= 0 /\ -cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: l3 -> l0 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post4, lt_23^0'=lt_23^post4, lt_24^0'=lt_24^post4, lt_25^0'=lt_25^post4, result_4^0'=result_4^0, x_5^0'=x_5^0, (-lt_19^1 <= 0 /\ lt_18^1 <= 0 /\ -cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 New rule: l3 -> l0 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post4, lt_23^0'=lt_23^post4, lt_24^0'=lt_24^post4, lt_25^0'=lt_25^post4, result_4^0'=result_4^0, x_5^0'=x_5^0, (-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l3 -> l0 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post4, lt_23^0'=lt_23^post4, lt_24^0'=lt_24^post4, lt_25^0'=lt_25^post4, result_4^0'=result_4^0, x_5^0'=x_5^0, (-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 New rule: l3 -> l0 : lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_22^0'=lt_22^post4, lt_23^0'=lt_23^post4, lt_24^0'=lt_24^post4, lt_25^0'=lt_25^post4, (-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 Propagated Equalities Original rule: l3 -> l1 : a_6^0'=a_6^post5, b_7^0'=b_7^post5, c_8^0'=c_8^post5, cnt_38^0'=cnt_38^post5, d_9^0'=d_9^post5, e_10^0'=e_10^post5, f_11^0'=f_11^post5, g_12^0'=g_12^post5, h_13^0'=h_13^post5, lt_14^0'=lt_14^post5, lt_15^0'=lt_15^post5, lt_16^0'=lt_16^post5, lt_17^0'=lt_17^post5, lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, lt_22^0'=lt_22^post5, lt_23^0'=lt_23^post5, lt_24^0'=lt_24^post5, lt_25^0'=lt_25^post5, result_4^0'=result_4^post5, x_5^0'=x_5^post5, (0 == 0 /\ lt_17^0-lt_17^post5 == 0 /\ lt_23^0-lt_23^post5 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ -lt_22^post5+lt_22^0 == 0 /\ lt_14^0-lt_14^post5 == 0 /\ lt_24^0-lt_24^post5 == 0 /\ e_10^0-e_10^post5 == 0 /\ h_13^0-h_13^post5 == 0 /\ -lt_16^post5+lt_16^0 == 0 /\ 1+lt_25^1 <= 0 /\ -cnt_38^post5+cnt_38^0 == 0 /\ -lt_19^1 <= 0 /\ -d_9^post5+d_9^0 == 0 /\ lt_18^1 <= 0 /\ -b_7^post5+b_7^0 == 0 /\ -a_6^post5+a_6^0 == 0 /\ f_11^0-f_11^post5 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ c_8^0-c_8^post5 == 0 /\ -x_5^post5+x_5^0 == 0 /\ -lt_15^post5+lt_15^0 == 0 /\ -g_12^post5+g_12^0 == 0), cost: 1 New rule: l3 -> l1 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post5, result_4^0'=result_4^post5, x_5^0'=x_5^0, (0 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ 1+lt_25^1 <= 0 /\ -lt_19^1 <= 0 /\ lt_18^1 <= 0 /\ -cnt_38^0+lt_25^1 == 0), cost: 1 propagated equality lt_17^post5 = lt_17^0 propagated equality lt_23^post5 = lt_23^0 propagated equality lt_22^post5 = lt_22^0 propagated equality lt_14^post5 = lt_14^0 propagated equality lt_24^post5 = lt_24^0 propagated equality e_10^post5 = e_10^0 propagated equality h_13^post5 = h_13^0 propagated equality lt_16^post5 = lt_16^0 propagated equality cnt_38^post5 = cnt_38^0 propagated equality d_9^post5 = d_9^0 propagated equality b_7^post5 = b_7^0 propagated equality a_6^post5 = a_6^0 propagated equality f_11^post5 = f_11^0 propagated equality c_8^post5 = c_8^0 propagated equality x_5^post5 = x_5^0 propagated equality lt_15^post5 = lt_15^0 propagated equality g_12^post5 = g_12^0 Propagated Equalities Original rule: l3 -> l1 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post5, result_4^0'=result_4^post5, x_5^0'=x_5^0, (0 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ 1+lt_25^1 <= 0 /\ -lt_19^1 <= 0 /\ lt_18^1 <= 0 /\ -cnt_38^0+lt_25^1 == 0), cost: 1 New rule: l3 -> l1 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post5, result_4^0'=result_4^post5, x_5^0'=x_5^0, (0 == 0 /\ 1+cnt_38^0 <= 0 /\ -lt_19^1 <= 0 /\ lt_18^1 <= 0), cost: 1 propagated equality lt_21^1 = cnt_38^0 propagated equality lt_25^1 = cnt_38^0 Simplified Guard Original rule: l3 -> l1 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post5, result_4^0'=result_4^post5, x_5^0'=x_5^0, (0 == 0 /\ 1+cnt_38^0 <= 0 /\ -lt_19^1 <= 0 /\ lt_18^1 <= 0), cost: 1 New rule: l3 -> l1 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post5, result_4^0'=result_4^post5, x_5^0'=x_5^0, (1+cnt_38^0 <= 0 /\ -lt_19^1 <= 0 /\ lt_18^1 <= 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: l3 -> l1 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post5, result_4^0'=result_4^post5, x_5^0'=x_5^0, (1+cnt_38^0 <= 0 /\ -lt_19^1 <= 0 /\ lt_18^1 <= 0), cost: 1 New rule: l3 -> l1 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post5, result_4^0'=result_4^post5, x_5^0'=x_5^0, (1+cnt_38^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l3 -> l1 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post5, result_4^0'=result_4^post5, x_5^0'=x_5^0, (1+cnt_38^0 <= 0), cost: 1 New rule: l3 -> l1 : lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, lt_25^0'=lt_25^post5, result_4^0'=result_4^post5, (1+cnt_38^0 <= 0), cost: 1 Propagated Equalities Original rule: l8 -> l3 : a_6^0'=a_6^post2, b_7^0'=b_7^post2, c_8^0'=c_8^post2, cnt_38^0'=cnt_38^post2, d_9^0'=d_9^post2, e_10^0'=e_10^post2, f_11^0'=f_11^post2, g_12^0'=g_12^post2, h_13^0'=h_13^post2, lt_14^0'=lt_14^post2, lt_15^0'=lt_15^post2, lt_16^0'=lt_16^post2, lt_17^0'=lt_17^post2, lt_18^0'=lt_18^post2, lt_19^0'=lt_19^post2, lt_20^0'=lt_20^post2, lt_21^0'=lt_21^post2, lt_22^0'=lt_22^post2, lt_23^0'=lt_23^post2, lt_24^0'=lt_24^post2, lt_25^0'=lt_25^post2, result_4^0'=result_4^post2, x_5^0'=x_5^post2, (0 == 0 /\ c_8^0-c_8^post14 == 0 /\ lt_17^post14-lt_17^post2 == 0 /\ lt_23^post14-lt_23^post2 == 0 /\ -b_7^post14+b_7^0 == 0 /\ b_7^post2-a_6^post2 == 0 /\ -result_4^post14+result_4^0 == 0 /\ -a_6^post14+a_6^0 == 0 /\ lt_22^post14-lt_22^post2 == 0 /\ -cnt_38^post14+cnt_38^0 == 0 /\ -e_10^post2+f_11^post2 == 0 /\ g_12^post2-f_11^post2 == 0 /\ lt_15^post14-lt_15^post2 == 0 /\ lt_17^0-lt_17^post14 == 0 /\ -x_5^post14+x_5^0 == 0 /\ lt_25^post14-lt_25^post2 == 0 /\ lt_18^0-lt_18^post14 == 0 /\ d_9^0-d_9^post14 == 0 /\ lt_20^post14-lt_20^post2 == 0 /\ lt_19^post14-lt_19^post2 == 0 /\ cnt_38^post14-cnt_38^post2 == 0 /\ lt_15^0-lt_15^post14 == 0 /\ -g_12^post2+h_13^post2 == 0 /\ lt_20^0-lt_20^post14 == 0 /\ lt_14^post14-lt_14^post2 == 0 /\ -b_7^post2+c_8^post2 == 0 /\ -c_8^post2+d_9^post2 == 0 /\ -lt_21^post14+lt_21^0 == 0 /\ -lt_25^post14+lt_25^0 == 0 /\ -lt_22^post14+lt_22^0 == 0 /\ e_10^post2-d_9^post2 == 0 /\ result_4^post14-result_4^post2 == 0 /\ e_10^0-e_10^post14 == 0 /\ lt_21^post14-lt_21^post2 == 0 /\ lt_18^post14-lt_18^post2 == 0 /\ -lt_19^post14+lt_19^0 == 0 /\ -f_11^post14+f_11^0 == 0 /\ lt_23^0-lt_23^post14 == 0 /\ -g_12^post14+g_12^0 == 0 /\ lt_16^post14-lt_16^post2 == 0 /\ -lt_14^post14+lt_14^0 == 0 /\ -lt_16^post14+lt_16^0 == 0 /\ h_13^0-h_13^post14 == 0 /\ lt_24^0-lt_24^post14 == 0 /\ lt_24^post14-lt_24^post2 == 0 /\ -x_5^post2+a_6^post2 == 0), cost: 1 New rule: l8 -> l3 : a_6^0'=x_5^post2, b_7^0'=x_5^post2, c_8^0'=x_5^post2, cnt_38^0'=cnt_38^post14, d_9^0'=x_5^post2, e_10^0'=x_5^post2, f_11^0'=x_5^post2, g_12^0'=x_5^post2, h_13^0'=x_5^post2, lt_14^0'=lt_14^post14, lt_15^0'=lt_15^post14, lt_16^0'=lt_16^post14, lt_17^0'=lt_17^post14, lt_18^0'=lt_18^post14, lt_19^0'=lt_19^post14, lt_20^0'=lt_20^post14, lt_21^0'=lt_21^post14, lt_22^0'=lt_22^post14, lt_23^0'=lt_23^post14, lt_24^0'=lt_24^post14, lt_25^0'=lt_25^post14, result_4^0'=result_4^post14, x_5^0'=x_5^post2, (0 == 0 /\ c_8^0-c_8^post14 == 0 /\ -b_7^post14+b_7^0 == 0 /\ -result_4^post14+result_4^0 == 0 /\ -a_6^post14+a_6^0 == 0 /\ -cnt_38^post14+cnt_38^0 == 0 /\ lt_17^0-lt_17^post14 == 0 /\ -x_5^post14+x_5^0 == 0 /\ lt_18^0-lt_18^post14 == 0 /\ d_9^0-d_9^post14 == 0 /\ lt_15^0-lt_15^post14 == 0 /\ lt_20^0-lt_20^post14 == 0 /\ -lt_21^post14+lt_21^0 == 0 /\ -lt_25^post14+lt_25^0 == 0 /\ -lt_22^post14+lt_22^0 == 0 /\ e_10^0-e_10^post14 == 0 /\ -lt_19^post14+lt_19^0 == 0 /\ -f_11^post14+f_11^0 == 0 /\ lt_23^0-lt_23^post14 == 0 /\ -g_12^post14+g_12^0 == 0 /\ -lt_14^post14+lt_14^0 == 0 /\ -lt_16^post14+lt_16^0 == 0 /\ h_13^0-h_13^post14 == 0 /\ lt_24^0-lt_24^post14 == 0), cost: 1 propagated equality lt_17^post2 = lt_17^post14 propagated equality lt_23^post2 = lt_23^post14 propagated equality a_6^post2 = b_7^post2 propagated equality lt_22^post2 = lt_22^post14 propagated equality e_10^post2 = f_11^post2 propagated equality f_11^post2 = g_12^post2 propagated equality lt_15^post2 = lt_15^post14 propagated equality lt_25^post2 = lt_25^post14 propagated equality lt_20^post2 = lt_20^post14 propagated equality lt_19^post2 = lt_19^post14 propagated equality cnt_38^post2 = cnt_38^post14 propagated equality g_12^post2 = h_13^post2 propagated equality lt_14^post2 = lt_14^post14 propagated equality b_7^post2 = c_8^post2 propagated equality c_8^post2 = d_9^post2 propagated equality d_9^post2 = h_13^post2 propagated equality result_4^post2 = result_4^post14 propagated equality lt_21^post2 = lt_21^post14 propagated equality lt_18^post2 = lt_18^post14 propagated equality lt_16^post2 = lt_16^post14 propagated equality lt_24^post2 = lt_24^post14 propagated equality h_13^post2 = x_5^post2 Propagated Equalities Original rule: l8 -> l3 : a_6^0'=x_5^post2, b_7^0'=x_5^post2, c_8^0'=x_5^post2, cnt_38^0'=cnt_38^post14, d_9^0'=x_5^post2, e_10^0'=x_5^post2, f_11^0'=x_5^post2, g_12^0'=x_5^post2, h_13^0'=x_5^post2, lt_14^0'=lt_14^post14, lt_15^0'=lt_15^post14, lt_16^0'=lt_16^post14, lt_17^0'=lt_17^post14, lt_18^0'=lt_18^post14, lt_19^0'=lt_19^post14, lt_20^0'=lt_20^post14, lt_21^0'=lt_21^post14, lt_22^0'=lt_22^post14, lt_23^0'=lt_23^post14, lt_24^0'=lt_24^post14, lt_25^0'=lt_25^post14, result_4^0'=result_4^post14, x_5^0'=x_5^post2, (0 == 0 /\ c_8^0-c_8^post14 == 0 /\ -b_7^post14+b_7^0 == 0 /\ -result_4^post14+result_4^0 == 0 /\ -a_6^post14+a_6^0 == 0 /\ -cnt_38^post14+cnt_38^0 == 0 /\ lt_17^0-lt_17^post14 == 0 /\ -x_5^post14+x_5^0 == 0 /\ lt_18^0-lt_18^post14 == 0 /\ d_9^0-d_9^post14 == 0 /\ lt_15^0-lt_15^post14 == 0 /\ lt_20^0-lt_20^post14 == 0 /\ -lt_21^post14+lt_21^0 == 0 /\ -lt_25^post14+lt_25^0 == 0 /\ -lt_22^post14+lt_22^0 == 0 /\ e_10^0-e_10^post14 == 0 /\ -lt_19^post14+lt_19^0 == 0 /\ -f_11^post14+f_11^0 == 0 /\ lt_23^0-lt_23^post14 == 0 /\ -g_12^post14+g_12^0 == 0 /\ -lt_14^post14+lt_14^0 == 0 /\ -lt_16^post14+lt_16^0 == 0 /\ h_13^0-h_13^post14 == 0 /\ lt_24^0-lt_24^post14 == 0), cost: 1 New rule: l8 -> l3 : a_6^0'=x_5^post2, b_7^0'=x_5^post2, c_8^0'=x_5^post2, cnt_38^0'=cnt_38^0, d_9^0'=x_5^post2, e_10^0'=x_5^post2, f_11^0'=x_5^post2, g_12^0'=x_5^post2, h_13^0'=x_5^post2, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^0, result_4^0'=result_4^0, x_5^0'=x_5^post2, 0 == 0, cost: 1 propagated equality c_8^post14 = c_8^0 propagated equality b_7^post14 = b_7^0 propagated equality result_4^post14 = result_4^0 propagated equality a_6^post14 = a_6^0 propagated equality cnt_38^post14 = cnt_38^0 propagated equality lt_17^post14 = lt_17^0 propagated equality x_5^post14 = x_5^0 propagated equality lt_18^post14 = lt_18^0 propagated equality d_9^post14 = d_9^0 propagated equality lt_15^post14 = lt_15^0 propagated equality lt_20^post14 = lt_20^0 propagated equality lt_21^post14 = lt_21^0 propagated equality lt_25^post14 = lt_25^0 propagated equality lt_22^post14 = lt_22^0 propagated equality e_10^post14 = e_10^0 propagated equality lt_19^post14 = lt_19^0 propagated equality f_11^post14 = f_11^0 propagated equality lt_23^post14 = lt_23^0 propagated equality g_12^post14 = g_12^0 propagated equality lt_14^post14 = lt_14^0 propagated equality lt_16^post14 = lt_16^0 propagated equality h_13^post14 = h_13^0 propagated equality lt_24^post14 = lt_24^0 Simplified Guard Original rule: l8 -> l3 : a_6^0'=x_5^post2, b_7^0'=x_5^post2, c_8^0'=x_5^post2, cnt_38^0'=cnt_38^0, d_9^0'=x_5^post2, e_10^0'=x_5^post2, f_11^0'=x_5^post2, g_12^0'=x_5^post2, h_13^0'=x_5^post2, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^0, result_4^0'=result_4^0, x_5^0'=x_5^post2, 0 == 0, cost: 1 New rule: l8 -> l3 : a_6^0'=x_5^post2, b_7^0'=x_5^post2, c_8^0'=x_5^post2, cnt_38^0'=cnt_38^0, d_9^0'=x_5^post2, e_10^0'=x_5^post2, f_11^0'=x_5^post2, g_12^0'=x_5^post2, h_13^0'=x_5^post2, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^0, result_4^0'=result_4^0, x_5^0'=x_5^post2, T, cost: 1 Removed Trivial Updates Original rule: l8 -> l3 : a_6^0'=x_5^post2, b_7^0'=x_5^post2, c_8^0'=x_5^post2, cnt_38^0'=cnt_38^0, d_9^0'=x_5^post2, e_10^0'=x_5^post2, f_11^0'=x_5^post2, g_12^0'=x_5^post2, h_13^0'=x_5^post2, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^0, result_4^0'=result_4^0, x_5^0'=x_5^post2, T, cost: 1 New rule: l8 -> l3 : a_6^0'=x_5^post2, b_7^0'=x_5^post2, c_8^0'=x_5^post2, d_9^0'=x_5^post2, e_10^0'=x_5^post2, f_11^0'=x_5^post2, g_12^0'=x_5^post2, h_13^0'=x_5^post2, x_5^0'=x_5^post2, T, cost: 1 Propagated Equalities Original rule: l3 -> l3 : a_6^0'=a_6^post7, b_7^0'=b_7^post7, c_8^0'=c_8^post7, cnt_38^0'=cnt_38^post7, d_9^0'=d_9^post7, e_10^0'=e_10^post7, f_11^0'=f_11^post7, g_12^0'=g_12^post7, h_13^0'=h_13^post7, lt_14^0'=lt_14^post7, lt_15^0'=lt_15^post7, lt_16^0'=lt_16^post7, lt_17^0'=lt_17^post7, lt_18^0'=lt_18^post7, lt_19^0'=lt_19^post7, lt_20^0'=lt_20^post7, lt_21^0'=lt_21^post7, lt_22^0'=lt_22^post7, lt_23^0'=lt_23^post7, lt_24^0'=lt_24^post7, lt_25^0'=lt_25^post7, result_4^0'=result_4^post7, x_5^0'=x_5^post7, (0 == 0 /\ -f_11^post7+f_11^post6 == 0 /\ -lt_14^post6+lt_14^0 == 0 /\ -f_11^post6+f_11^0 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ -a_6^post6+a_6^0 == 0 /\ lt_16^post6-lt_16^post7 == 0 /\ -lt_15^post7+lt_15^post6 == 0 /\ -x_5^post6+x_5^0 == 0 /\ -lt_18^post7+lt_18^post6 == 0 /\ -lt_14^post7+lt_14^post6 == 0 /\ lt_25^post6-lt_25^post7 == 0 /\ h_13^post6-h_13^post7 == 0 /\ g_12^0-g_12^post6 == 0 /\ 1-lt_18^1 <= 0 /\ result_4^post6-result_4^post7 == 0 /\ c_8^0-c_8^post6 == 0 /\ d_9^post6-d_9^post7 == 0 /\ 1-lt_24^1 <= 0 /\ -a_6^post7+a_6^post6 == 0 /\ -cnt_38^post7+cnt_38^post6 == 0 /\ lt_23^post6-lt_23^post7 == 0 /\ -g_12^post7+g_12^post6 == 0 /\ c_8^post6-c_8^post7 == 0 /\ lt_24^1-cnt_38^0 == 0 /\ -lt_17^post7+lt_17^post6 == 0 /\ -x_5^post7+x_5^post6 == 0 /\ e_10^post6-e_10^post7 == 0 /\ lt_22^post6-lt_22^post7 == 0 /\ lt_20^0-lt_20^post6 == 0 /\ -lt_21^post6+lt_21^0 == 0 /\ -cnt_38^post6+cnt_38^0 == 0 /\ e_10^0-e_10^post6 == 0 /\ lt_19^post6-lt_19^post7 == 0 /\ -lt_19^1 <= 0 /\ -b_7^post6+b_7^0 == 0 /\ lt_15^0-lt_15^post6 == 0 /\ -lt_25^1 <= 0 /\ -lt_20^post7+lt_20^post6 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ b_7^post6-b_7^post7 == 0 /\ h_13^0-h_13^post6 == 0 /\ -result_4^post6+result_4^0 == 0 /\ -lt_21^post7+lt_21^post6 == 0 /\ lt_24^post6-lt_24^post7 == 0 /\ -d_9^post6+d_9^0 == 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^post6, b_7^0'=b_7^post6, c_8^0'=c_8^post6, cnt_38^0'=cnt_38^post6, d_9^0'=d_9^post6, e_10^0'=e_10^post6, f_11^0'=f_11^post6, g_12^0'=g_12^post6, h_13^0'=h_13^post6, lt_14^0'=lt_14^post6, lt_15^0'=lt_15^post6, lt_16^0'=lt_16^post6, lt_17^0'=lt_17^post6, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, lt_21^0'=lt_21^post6, lt_22^0'=lt_22^post6, lt_23^0'=lt_23^post6, lt_24^0'=lt_24^post6, lt_25^0'=lt_25^post6, result_4^0'=result_4^post6, x_5^0'=x_5^post6, (0 == 0 /\ -lt_14^post6+lt_14^0 == 0 /\ -f_11^post6+f_11^0 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ -a_6^post6+a_6^0 == 0 /\ -x_5^post6+x_5^0 == 0 /\ g_12^0-g_12^post6 == 0 /\ 1-lt_18^1 <= 0 /\ c_8^0-c_8^post6 == 0 /\ 1-lt_24^1 <= 0 /\ lt_24^1-cnt_38^0 == 0 /\ lt_20^0-lt_20^post6 == 0 /\ -lt_21^post6+lt_21^0 == 0 /\ -cnt_38^post6+cnt_38^0 == 0 /\ e_10^0-e_10^post6 == 0 /\ -lt_19^1 <= 0 /\ -b_7^post6+b_7^0 == 0 /\ lt_15^0-lt_15^post6 == 0 /\ -lt_25^1 <= 0 /\ -cnt_38^0+lt_25^1 == 0 /\ h_13^0-h_13^post6 == 0 /\ -result_4^post6+result_4^0 == 0 /\ -d_9^post6+d_9^0 == 0), cost: 1 propagated equality f_11^post7 = f_11^post6 propagated equality lt_16^post7 = lt_16^post6 propagated equality lt_15^post7 = lt_15^post6 propagated equality lt_18^post7 = lt_18^post6 propagated equality lt_14^post7 = lt_14^post6 propagated equality lt_25^post7 = lt_25^post6 propagated equality h_13^post7 = h_13^post6 propagated equality result_4^post7 = result_4^post6 propagated equality d_9^post7 = d_9^post6 propagated equality a_6^post7 = a_6^post6 propagated equality cnt_38^post7 = cnt_38^post6 propagated equality lt_23^post7 = lt_23^post6 propagated equality g_12^post7 = g_12^post6 propagated equality c_8^post7 = c_8^post6 propagated equality lt_17^post7 = lt_17^post6 propagated equality x_5^post7 = x_5^post6 propagated equality e_10^post7 = e_10^post6 propagated equality lt_22^post7 = lt_22^post6 propagated equality lt_19^post7 = lt_19^post6 propagated equality lt_20^post7 = lt_20^post6 propagated equality b_7^post7 = b_7^post6 propagated equality lt_21^post7 = lt_21^post6 propagated equality lt_24^post7 = lt_24^post6 Propagated Equalities Original rule: l3 -> l3 : a_6^0'=a_6^post6, b_7^0'=b_7^post6, c_8^0'=c_8^post6, cnt_38^0'=cnt_38^post6, d_9^0'=d_9^post6, e_10^0'=e_10^post6, f_11^0'=f_11^post6, g_12^0'=g_12^post6, h_13^0'=h_13^post6, lt_14^0'=lt_14^post6, lt_15^0'=lt_15^post6, lt_16^0'=lt_16^post6, lt_17^0'=lt_17^post6, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, lt_21^0'=lt_21^post6, lt_22^0'=lt_22^post6, lt_23^0'=lt_23^post6, lt_24^0'=lt_24^post6, lt_25^0'=lt_25^post6, result_4^0'=result_4^post6, x_5^0'=x_5^post6, (0 == 0 /\ -lt_14^post6+lt_14^0 == 0 /\ -f_11^post6+f_11^0 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ -a_6^post6+a_6^0 == 0 /\ -x_5^post6+x_5^0 == 0 /\ g_12^0-g_12^post6 == 0 /\ 1-lt_18^1 <= 0 /\ c_8^0-c_8^post6 == 0 /\ 1-lt_24^1 <= 0 /\ lt_24^1-cnt_38^0 == 0 /\ lt_20^0-lt_20^post6 == 0 /\ -lt_21^post6+lt_21^0 == 0 /\ -cnt_38^post6+cnt_38^0 == 0 /\ e_10^0-e_10^post6 == 0 /\ -lt_19^1 <= 0 /\ -b_7^post6+b_7^0 == 0 /\ lt_15^0-lt_15^post6 == 0 /\ -lt_25^1 <= 0 /\ -cnt_38^0+lt_25^1 == 0 /\ h_13^0-h_13^post6 == 0 /\ -result_4^post6+result_4^0 == 0 /\ -d_9^post6+d_9^0 == 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^post6, lt_17^0'=lt_17^post6, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post6, lt_23^0'=lt_23^post6, lt_24^0'=lt_24^post6, lt_25^0'=lt_25^post6, result_4^0'=result_4^0, x_5^0'=x_5^0, (0 == 0 /\ 1-lt_18^1 <= 0 /\ -lt_19^1 <= 0 /\ -cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 propagated equality lt_14^post6 = lt_14^0 propagated equality f_11^post6 = f_11^0 propagated equality lt_23^1 = cnt_38^0 propagated equality a_6^post6 = a_6^0 propagated equality x_5^post6 = x_5^0 propagated equality g_12^post6 = g_12^0 propagated equality c_8^post6 = c_8^0 propagated equality lt_24^1 = cnt_38^0 propagated equality lt_20^post6 = lt_20^0 propagated equality lt_21^post6 = lt_21^0 propagated equality cnt_38^post6 = cnt_38^0 propagated equality e_10^post6 = e_10^0 propagated equality b_7^post6 = b_7^0 propagated equality lt_15^post6 = lt_15^0 propagated equality lt_25^1 = cnt_38^0 propagated equality h_13^post6 = h_13^0 propagated equality result_4^post6 = result_4^0 propagated equality d_9^post6 = d_9^0 Simplified Guard Original rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^post6, lt_17^0'=lt_17^post6, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post6, lt_23^0'=lt_23^post6, lt_24^0'=lt_24^post6, lt_25^0'=lt_25^post6, result_4^0'=result_4^0, x_5^0'=x_5^0, (0 == 0 /\ 1-lt_18^1 <= 0 /\ -lt_19^1 <= 0 /\ -cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^post6, lt_17^0'=lt_17^post6, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post6, lt_23^0'=lt_23^post6, lt_24^0'=lt_24^post6, lt_25^0'=lt_25^post6, result_4^0'=result_4^0, x_5^0'=x_5^0, (1-lt_18^1 <= 0 /\ -lt_19^1 <= 0 /\ -cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^post6, lt_17^0'=lt_17^post6, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post6, lt_23^0'=lt_23^post6, lt_24^0'=lt_24^post6, lt_25^0'=lt_25^post6, result_4^0'=result_4^0, x_5^0'=x_5^0, (1-lt_18^1 <= 0 /\ -lt_19^1 <= 0 /\ -cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^post6, lt_17^0'=lt_17^post6, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post6, lt_23^0'=lt_23^post6, lt_24^0'=lt_24^post6, lt_25^0'=lt_25^post6, result_4^0'=result_4^0, x_5^0'=x_5^0, (-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^post6, lt_17^0'=lt_17^post6, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post6, lt_23^0'=lt_23^post6, lt_24^0'=lt_24^post6, lt_25^0'=lt_25^post6, result_4^0'=result_4^0, x_5^0'=x_5^0, (-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 New rule: l3 -> l3 : lt_16^0'=lt_16^post6, lt_17^0'=lt_17^post6, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_22^0'=lt_22^post6, lt_23^0'=lt_23^post6, lt_24^0'=lt_24^post6, lt_25^0'=lt_25^post6, (-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 Propagated Equalities Original rule: l3 -> l3 : a_6^0'=a_6^post9, b_7^0'=b_7^post9, c_8^0'=c_8^post9, cnt_38^0'=cnt_38^post9, d_9^0'=d_9^post9, e_10^0'=e_10^post9, f_11^0'=f_11^post9, g_12^0'=g_12^post9, h_13^0'=h_13^post9, lt_14^0'=lt_14^post9, lt_15^0'=lt_15^post9, lt_16^0'=lt_16^post9, lt_17^0'=lt_17^post9, lt_18^0'=lt_18^post9, lt_19^0'=lt_19^post9, lt_20^0'=lt_20^post9, lt_21^0'=lt_21^post9, lt_22^0'=lt_22^post9, lt_23^0'=lt_23^post9, lt_24^0'=lt_24^post9, lt_25^0'=lt_25^post9, result_4^0'=result_4^post9, x_5^0'=x_5^post9, (0 == 0 /\ lt_17^0-lt_17^post8 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ -result_4^post9+result_4^post8 == 0 /\ -result_4^post8+result_4^0 == 0 /\ -b_7^post8+b_7^0 == 0 /\ lt_20^0-lt_20^post8 == 0 /\ -lt_21^post9+lt_21^post8 == 0 /\ -d_9^post8+d_9^0 == 0 /\ e_10^0-e_10^post8 == 0 /\ -lt_23^post9+lt_23^post8 == 0 /\ g_12^post8-g_12^post9 == 0 /\ -lt_16^post9+lt_16^post8 == 0 /\ 1+lt_19^1 <= 0 /\ -x_5^post8+x_5^0 == 0 /\ b_7^post8-b_7^post9 == 0 /\ 1-lt_24^1 <= 0 /\ -lt_24^post9+lt_24^post8 == 0 /\ a_6^post8-a_6^post9 == 0 /\ lt_24^1-cnt_38^0 == 0 /\ d_9^post8-d_9^post9 == 0 /\ -lt_18^post8+lt_18^0 == 0 /\ -g_12^post8+g_12^0 == 0 /\ -lt_16^post8+lt_16^0 == 0 /\ -cnt_38^post9+cnt_38^post8 == 0 /\ -lt_22^post9+lt_22^post8 == 0 /\ lt_14^post8-lt_14^post9 == 0 /\ c_8^0-c_8^post8 == 0 /\ lt_15^post8-lt_15^post9 == 0 /\ -lt_17^post9+lt_17^post8 == 0 /\ lt_25^post8-lt_25^post9 == 0 /\ h_13^0-h_13^post8 == 0 /\ -a_6^post8+a_6^0 == 0 /\ -lt_25^1 <= 0 /\ c_8^post8-c_8^post9 == 0 /\ lt_21^0-lt_21^post8 == 0 /\ e_10^post8-e_10^post9 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ -f_11^post9+f_11^post8 == 0 /\ -x_5^post9+x_5^post8 == 0 /\ -lt_19^post9+lt_19^post8 == 0 /\ lt_18^post8-lt_18^post9 == 0 /\ h_13^post8-h_13^post9 == 0 /\ f_11^0-f_11^post8 == 0 /\ cnt_38^0-cnt_38^post8 == 0 /\ -lt_20^post9+lt_20^post8 == 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^post8, b_7^0'=b_7^post8, c_8^0'=c_8^post8, cnt_38^0'=cnt_38^post8, d_9^0'=d_9^post8, e_10^0'=e_10^post8, f_11^0'=f_11^post8, g_12^0'=g_12^post8, h_13^0'=h_13^post8, lt_14^0'=lt_14^post8, lt_15^0'=lt_15^post8, lt_16^0'=lt_16^post8, lt_17^0'=lt_17^post8, lt_18^0'=lt_18^post8, lt_19^0'=lt_19^post8, lt_20^0'=lt_20^post8, lt_21^0'=lt_21^post8, lt_22^0'=lt_22^post8, lt_23^0'=lt_23^post8, lt_24^0'=lt_24^post8, lt_25^0'=lt_25^post8, result_4^0'=result_4^post8, x_5^0'=x_5^post8, (0 == 0 /\ lt_17^0-lt_17^post8 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ -result_4^post8+result_4^0 == 0 /\ -b_7^post8+b_7^0 == 0 /\ lt_20^0-lt_20^post8 == 0 /\ -d_9^post8+d_9^0 == 0 /\ e_10^0-e_10^post8 == 0 /\ 1+lt_19^1 <= 0 /\ -x_5^post8+x_5^0 == 0 /\ 1-lt_24^1 <= 0 /\ lt_24^1-cnt_38^0 == 0 /\ -lt_18^post8+lt_18^0 == 0 /\ -g_12^post8+g_12^0 == 0 /\ -lt_16^post8+lt_16^0 == 0 /\ c_8^0-c_8^post8 == 0 /\ h_13^0-h_13^post8 == 0 /\ -a_6^post8+a_6^0 == 0 /\ -lt_25^1 <= 0 /\ lt_21^0-lt_21^post8 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ f_11^0-f_11^post8 == 0 /\ cnt_38^0-cnt_38^post8 == 0), cost: 1 propagated equality result_4^post9 = result_4^post8 propagated equality lt_21^post9 = lt_21^post8 propagated equality lt_23^post9 = lt_23^post8 propagated equality g_12^post9 = g_12^post8 propagated equality lt_16^post9 = lt_16^post8 propagated equality b_7^post9 = b_7^post8 propagated equality lt_24^post9 = lt_24^post8 propagated equality a_6^post9 = a_6^post8 propagated equality d_9^post9 = d_9^post8 propagated equality cnt_38^post9 = cnt_38^post8 propagated equality lt_22^post9 = lt_22^post8 propagated equality lt_14^post9 = lt_14^post8 propagated equality lt_15^post9 = lt_15^post8 propagated equality lt_17^post9 = lt_17^post8 propagated equality lt_25^post9 = lt_25^post8 propagated equality c_8^post9 = c_8^post8 propagated equality e_10^post9 = e_10^post8 propagated equality f_11^post9 = f_11^post8 propagated equality x_5^post9 = x_5^post8 propagated equality lt_19^post9 = lt_19^post8 propagated equality lt_18^post9 = lt_18^post8 propagated equality h_13^post9 = h_13^post8 propagated equality lt_20^post9 = lt_20^post8 Propagated Equalities Original rule: l3 -> l3 : a_6^0'=a_6^post8, b_7^0'=b_7^post8, c_8^0'=c_8^post8, cnt_38^0'=cnt_38^post8, d_9^0'=d_9^post8, e_10^0'=e_10^post8, f_11^0'=f_11^post8, g_12^0'=g_12^post8, h_13^0'=h_13^post8, lt_14^0'=lt_14^post8, lt_15^0'=lt_15^post8, lt_16^0'=lt_16^post8, lt_17^0'=lt_17^post8, lt_18^0'=lt_18^post8, lt_19^0'=lt_19^post8, lt_20^0'=lt_20^post8, lt_21^0'=lt_21^post8, lt_22^0'=lt_22^post8, lt_23^0'=lt_23^post8, lt_24^0'=lt_24^post8, lt_25^0'=lt_25^post8, result_4^0'=result_4^post8, x_5^0'=x_5^post8, (0 == 0 /\ lt_17^0-lt_17^post8 == 0 /\ lt_23^1-cnt_38^0 == 0 /\ -result_4^post8+result_4^0 == 0 /\ -b_7^post8+b_7^0 == 0 /\ lt_20^0-lt_20^post8 == 0 /\ -d_9^post8+d_9^0 == 0 /\ e_10^0-e_10^post8 == 0 /\ 1+lt_19^1 <= 0 /\ -x_5^post8+x_5^0 == 0 /\ 1-lt_24^1 <= 0 /\ lt_24^1-cnt_38^0 == 0 /\ -lt_18^post8+lt_18^0 == 0 /\ -g_12^post8+g_12^0 == 0 /\ -lt_16^post8+lt_16^0 == 0 /\ c_8^0-c_8^post8 == 0 /\ h_13^0-h_13^post8 == 0 /\ -a_6^post8+a_6^0 == 0 /\ -lt_25^1 <= 0 /\ lt_21^0-lt_21^post8 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ f_11^0-f_11^post8 == 0 /\ cnt_38^0-cnt_38^post8 == 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^post8, lt_15^0'=lt_15^post8, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post8, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post8, lt_23^0'=lt_23^post8, lt_24^0'=lt_24^post8, lt_25^0'=lt_25^post8, result_4^0'=result_4^0, x_5^0'=x_5^0, (0 == 0 /\ 1+lt_19^1 <= 0 /\ -cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 propagated equality lt_17^post8 = lt_17^0 propagated equality lt_23^1 = cnt_38^0 propagated equality result_4^post8 = result_4^0 propagated equality b_7^post8 = b_7^0 propagated equality lt_20^post8 = lt_20^0 propagated equality d_9^post8 = d_9^0 propagated equality e_10^post8 = e_10^0 propagated equality x_5^post8 = x_5^0 propagated equality lt_24^1 = cnt_38^0 propagated equality lt_18^post8 = lt_18^0 propagated equality g_12^post8 = g_12^0 propagated equality lt_16^post8 = lt_16^0 propagated equality c_8^post8 = c_8^0 propagated equality h_13^post8 = h_13^0 propagated equality a_6^post8 = a_6^0 propagated equality lt_21^post8 = lt_21^0 propagated equality lt_25^1 = cnt_38^0 propagated equality f_11^post8 = f_11^0 propagated equality cnt_38^post8 = cnt_38^0 Simplified Guard Original rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^post8, lt_15^0'=lt_15^post8, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post8, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post8, lt_23^0'=lt_23^post8, lt_24^0'=lt_24^post8, lt_25^0'=lt_25^post8, result_4^0'=result_4^0, x_5^0'=x_5^0, (0 == 0 /\ 1+lt_19^1 <= 0 /\ -cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^post8, lt_15^0'=lt_15^post8, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post8, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post8, lt_23^0'=lt_23^post8, lt_24^0'=lt_24^post8, lt_25^0'=lt_25^post8, result_4^0'=result_4^0, x_5^0'=x_5^0, (1+lt_19^1 <= 0 /\ -cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^post8, lt_15^0'=lt_15^post8, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post8, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post8, lt_23^0'=lt_23^post8, lt_24^0'=lt_24^post8, lt_25^0'=lt_25^post8, result_4^0'=result_4^0, x_5^0'=x_5^0, (1+lt_19^1 <= 0 /\ -cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^post8, lt_15^0'=lt_15^post8, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post8, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post8, lt_23^0'=lt_23^post8, lt_24^0'=lt_24^post8, lt_25^0'=lt_25^post8, result_4^0'=result_4^0, x_5^0'=x_5^0, (-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^post8, lt_15^0'=lt_15^post8, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post8, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, lt_22^0'=lt_22^post8, lt_23^0'=lt_23^post8, lt_24^0'=lt_24^post8, lt_25^0'=lt_25^post8, result_4^0'=result_4^0, x_5^0'=x_5^0, (-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 New rule: l3 -> l3 : lt_14^0'=lt_14^post8, lt_15^0'=lt_15^post8, lt_19^0'=lt_19^post8, lt_22^0'=lt_22^post8, lt_23^0'=lt_23^post8, lt_24^0'=lt_24^post8, lt_25^0'=lt_25^post8, (-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 Propagated Equalities Original rule: l3 -> l3 : a_6^0'=a_6^post11, b_7^0'=b_7^post11, c_8^0'=c_8^post11, cnt_38^0'=cnt_38^post11, d_9^0'=d_9^post11, e_10^0'=e_10^post11, f_11^0'=f_11^post11, g_12^0'=g_12^post11, h_13^0'=h_13^post11, lt_14^0'=lt_14^post11, lt_15^0'=lt_15^post11, lt_16^0'=lt_16^post11, lt_17^0'=lt_17^post11, lt_18^0'=lt_18^post11, lt_19^0'=lt_19^post11, lt_20^0'=lt_20^post11, lt_21^0'=lt_21^post11, lt_22^0'=lt_22^post11, lt_23^0'=lt_23^post11, lt_24^0'=lt_24^post11, lt_25^0'=lt_25^post11, result_4^0'=result_4^post11, x_5^0'=x_5^post11, (0 == 0 /\ -h_13^post11+h_13^post10 == 0 /\ lt_23^post10-lt_23^post11 == 0 /\ x_5^post10-x_5^post11 == 0 /\ lt_23^0-lt_23^post10 == 0 /\ -d_9^post10+d_9^0 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ e_10^0-e_10^post10 == 0 /\ -lt_22^post10+lt_22^0 == 0 /\ 1-lt_18^1 <= 0 /\ -result_4^post10+result_4^0 == 0 /\ lt_22^post10-lt_22^post11 == 0 /\ lt_17^post10-lt_17^post11 == 0 /\ -e_10^post11+e_10^post10 == 0 /\ result_4^post10-result_4^post11 == 0 /\ c_8^0-c_8^post10 == 0 /\ b_7^post10-b_7^post11 == 0 /\ -lt_15^post11+lt_15^post10 == 0 /\ -x_5^post10+x_5^0 == 0 /\ lt_20^post10-lt_20^post11 == 0 /\ -g_12^post10+g_12^0 == 0 /\ -lt_16^post11+lt_16^post10 == 0 /\ -cnt_38^post11+cnt_38^post10 == 0 /\ 1+lt_25^1 <= 0 /\ lt_24^post10-lt_24^post11 == 0 /\ lt_14^0-lt_14^post10 == 0 /\ lt_19^post10-lt_19^post11 == 0 /\ -d_9^post11+d_9^post10 == 0 /\ -lt_19^1 <= 0 /\ -b_7^post10+b_7^0 == 0 /\ c_8^post10-c_8^post11 == 0 /\ -lt_14^post11+lt_14^post10 == 0 /\ -a_6^post10+a_6^0 == 0 /\ h_13^0-h_13^post10 == 0 /\ -lt_18^post11+lt_18^post10 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ lt_25^post10-lt_25^post11 == 0 /\ -lt_21^post11+lt_21^post10 == 0 /\ -f_11^post11+f_11^post10 == 0 /\ cnt_38^0-cnt_38^post10 == 0 /\ -g_12^post11+g_12^post10 == 0 /\ -lt_15^post10+lt_15^0 == 0 /\ a_6^post10-a_6^post11 == 0 /\ lt_24^0-lt_24^post10 == 0 /\ f_11^0-f_11^post10 == 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^post10, b_7^0'=b_7^post10, c_8^0'=c_8^post10, cnt_38^0'=cnt_38^post10, d_9^0'=d_9^post10, e_10^0'=e_10^post10, f_11^0'=f_11^post10, g_12^0'=g_12^post10, h_13^0'=h_13^post10, lt_14^0'=lt_14^post10, lt_15^0'=lt_15^post10, lt_16^0'=lt_16^post10, lt_17^0'=lt_17^post10, lt_18^0'=lt_18^post10, lt_19^0'=lt_19^post10, lt_20^0'=lt_20^post10, lt_21^0'=lt_21^post10, lt_22^0'=lt_22^post10, lt_23^0'=lt_23^post10, lt_24^0'=lt_24^post10, lt_25^0'=lt_25^post10, result_4^0'=result_4^post10, x_5^0'=x_5^post10, (0 == 0 /\ lt_23^0-lt_23^post10 == 0 /\ -d_9^post10+d_9^0 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ e_10^0-e_10^post10 == 0 /\ -lt_22^post10+lt_22^0 == 0 /\ 1-lt_18^1 <= 0 /\ -result_4^post10+result_4^0 == 0 /\ c_8^0-c_8^post10 == 0 /\ -x_5^post10+x_5^0 == 0 /\ -g_12^post10+g_12^0 == 0 /\ 1+lt_25^1 <= 0 /\ lt_14^0-lt_14^post10 == 0 /\ -lt_19^1 <= 0 /\ -b_7^post10+b_7^0 == 0 /\ -a_6^post10+a_6^0 == 0 /\ h_13^0-h_13^post10 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ cnt_38^0-cnt_38^post10 == 0 /\ -lt_15^post10+lt_15^0 == 0 /\ lt_24^0-lt_24^post10 == 0 /\ f_11^0-f_11^post10 == 0), cost: 1 propagated equality h_13^post11 = h_13^post10 propagated equality lt_23^post11 = lt_23^post10 propagated equality x_5^post11 = x_5^post10 propagated equality lt_22^post11 = lt_22^post10 propagated equality lt_17^post11 = lt_17^post10 propagated equality e_10^post11 = e_10^post10 propagated equality result_4^post11 = result_4^post10 propagated equality b_7^post11 = b_7^post10 propagated equality lt_15^post11 = lt_15^post10 propagated equality lt_20^post11 = lt_20^post10 propagated equality lt_16^post11 = lt_16^post10 propagated equality cnt_38^post11 = cnt_38^post10 propagated equality lt_24^post11 = lt_24^post10 propagated equality lt_19^post11 = lt_19^post10 propagated equality d_9^post11 = d_9^post10 propagated equality c_8^post11 = c_8^post10 propagated equality lt_14^post11 = lt_14^post10 propagated equality lt_18^post11 = lt_18^post10 propagated equality lt_25^post11 = lt_25^post10 propagated equality lt_21^post11 = lt_21^post10 propagated equality f_11^post11 = f_11^post10 propagated equality g_12^post11 = g_12^post10 propagated equality a_6^post11 = a_6^post10 Propagated Equalities Original rule: l3 -> l3 : a_6^0'=a_6^post10, b_7^0'=b_7^post10, c_8^0'=c_8^post10, cnt_38^0'=cnt_38^post10, d_9^0'=d_9^post10, e_10^0'=e_10^post10, f_11^0'=f_11^post10, g_12^0'=g_12^post10, h_13^0'=h_13^post10, lt_14^0'=lt_14^post10, lt_15^0'=lt_15^post10, lt_16^0'=lt_16^post10, lt_17^0'=lt_17^post10, lt_18^0'=lt_18^post10, lt_19^0'=lt_19^post10, lt_20^0'=lt_20^post10, lt_21^0'=lt_21^post10, lt_22^0'=lt_22^post10, lt_23^0'=lt_23^post10, lt_24^0'=lt_24^post10, lt_25^0'=lt_25^post10, result_4^0'=result_4^post10, x_5^0'=x_5^post10, (0 == 0 /\ lt_23^0-lt_23^post10 == 0 /\ -d_9^post10+d_9^0 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ e_10^0-e_10^post10 == 0 /\ -lt_22^post10+lt_22^0 == 0 /\ 1-lt_18^1 <= 0 /\ -result_4^post10+result_4^0 == 0 /\ c_8^0-c_8^post10 == 0 /\ -x_5^post10+x_5^0 == 0 /\ -g_12^post10+g_12^0 == 0 /\ 1+lt_25^1 <= 0 /\ lt_14^0-lt_14^post10 == 0 /\ -lt_19^1 <= 0 /\ -b_7^post10+b_7^0 == 0 /\ -a_6^post10+a_6^0 == 0 /\ h_13^0-h_13^post10 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ cnt_38^0-cnt_38^post10 == 0 /\ -lt_15^post10+lt_15^0 == 0 /\ lt_24^0-lt_24^post10 == 0 /\ f_11^0-f_11^post10 == 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^post10, lt_17^0'=lt_17^post10, lt_18^0'=lt_18^post10, lt_19^0'=lt_19^post10, lt_20^0'=lt_20^post10, lt_21^0'=lt_21^post10, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post10, result_4^0'=result_4^0, x_5^0'=x_5^0, (0 == 0 /\ 1-lt_18^1 <= 0 /\ 1+cnt_38^0 <= 0 /\ -lt_19^1 <= 0), cost: 1 propagated equality lt_23^post10 = lt_23^0 propagated equality d_9^post10 = d_9^0 propagated equality lt_21^1 = cnt_38^0 propagated equality e_10^post10 = e_10^0 propagated equality lt_22^post10 = lt_22^0 propagated equality result_4^post10 = result_4^0 propagated equality c_8^post10 = c_8^0 propagated equality x_5^post10 = x_5^0 propagated equality g_12^post10 = g_12^0 propagated equality lt_14^post10 = lt_14^0 propagated equality b_7^post10 = b_7^0 propagated equality a_6^post10 = a_6^0 propagated equality h_13^post10 = h_13^0 propagated equality lt_25^1 = cnt_38^0 propagated equality cnt_38^post10 = cnt_38^0 propagated equality lt_15^post10 = lt_15^0 propagated equality lt_24^post10 = lt_24^0 propagated equality f_11^post10 = f_11^0 Simplified Guard Original rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^post10, lt_17^0'=lt_17^post10, lt_18^0'=lt_18^post10, lt_19^0'=lt_19^post10, lt_20^0'=lt_20^post10, lt_21^0'=lt_21^post10, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post10, result_4^0'=result_4^0, x_5^0'=x_5^0, (0 == 0 /\ 1-lt_18^1 <= 0 /\ 1+cnt_38^0 <= 0 /\ -lt_19^1 <= 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^post10, lt_17^0'=lt_17^post10, lt_18^0'=lt_18^post10, lt_19^0'=lt_19^post10, lt_20^0'=lt_20^post10, lt_21^0'=lt_21^post10, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post10, result_4^0'=result_4^0, x_5^0'=x_5^0, (1-lt_18^1 <= 0 /\ 1+cnt_38^0 <= 0 /\ -lt_19^1 <= 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^post10, lt_17^0'=lt_17^post10, lt_18^0'=lt_18^post10, lt_19^0'=lt_19^post10, lt_20^0'=lt_20^post10, lt_21^0'=lt_21^post10, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post10, result_4^0'=result_4^0, x_5^0'=x_5^0, (1-lt_18^1 <= 0 /\ 1+cnt_38^0 <= 0 /\ -lt_19^1 <= 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^post10, lt_17^0'=lt_17^post10, lt_18^0'=lt_18^post10, lt_19^0'=lt_19^post10, lt_20^0'=lt_20^post10, lt_21^0'=lt_21^post10, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post10, result_4^0'=result_4^0, x_5^0'=x_5^0, (1+cnt_38^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^0, lt_15^0'=lt_15^0, lt_16^0'=lt_16^post10, lt_17^0'=lt_17^post10, lt_18^0'=lt_18^post10, lt_19^0'=lt_19^post10, lt_20^0'=lt_20^post10, lt_21^0'=lt_21^post10, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post10, result_4^0'=result_4^0, x_5^0'=x_5^0, (1+cnt_38^0 <= 0), cost: 1 New rule: l3 -> l3 : lt_16^0'=lt_16^post10, lt_17^0'=lt_17^post10, lt_18^0'=lt_18^post10, lt_19^0'=lt_19^post10, lt_20^0'=lt_20^post10, lt_21^0'=lt_21^post10, lt_25^0'=lt_25^post10, (1+cnt_38^0 <= 0), cost: 1 Propagated Equalities Original rule: l3 -> l3 : a_6^0'=a_6^post13, b_7^0'=b_7^post13, c_8^0'=c_8^post13, cnt_38^0'=cnt_38^post13, d_9^0'=d_9^post13, e_10^0'=e_10^post13, f_11^0'=f_11^post13, g_12^0'=g_12^post13, h_13^0'=h_13^post13, lt_14^0'=lt_14^post13, lt_15^0'=lt_15^post13, lt_16^0'=lt_16^post13, lt_17^0'=lt_17^post13, lt_18^0'=lt_18^post13, lt_19^0'=lt_19^post13, lt_20^0'=lt_20^post13, lt_21^0'=lt_21^post13, lt_22^0'=lt_22^post13, lt_23^0'=lt_23^post13, lt_24^0'=lt_24^post13, lt_25^0'=lt_25^post13, result_4^0'=result_4^post13, x_5^0'=x_5^post13, (0 == 0 /\ lt_22^0-lt_22^post12 == 0 /\ e_10^0-e_10^post12 == 0 /\ -x_5^post12+x_5^0 == 0 /\ -b_7^post12+b_7^0 == 0 /\ h_13^post12-h_13^post13 == 0 /\ -a_6^post12+a_6^0 == 0 /\ c_8^0-c_8^post12 == 0 /\ lt_25^post12-lt_25^post13 == 0 /\ -b_7^post13+b_7^post12 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ d_9^post12-d_9^post13 == 0 /\ lt_16^0-lt_16^post12 == 0 /\ -h_13^post12+h_13^0 == 0 /\ -f_11^post12+f_11^0 == 0 /\ cnt_38^post12-cnt_38^post13 == 0 /\ lt_20^post12-lt_20^post13 == 0 /\ -lt_23^post12+lt_23^0 == 0 /\ 1+lt_19^1 <= 0 /\ lt_14^post12-lt_14^post13 == 0 /\ lt_23^post12-lt_23^post13 == 0 /\ -lt_16^post13+lt_16^post12 == 0 /\ g_12^post12-g_12^post13 == 0 /\ 1+lt_25^1 <= 0 /\ lt_17^post12-lt_17^post13 == 0 /\ -x_5^post13+x_5^post12 == 0 /\ -d_9^post12+d_9^0 == 0 /\ lt_22^post12-lt_22^post13 == 0 /\ g_12^0-g_12^post12 == 0 /\ lt_21^post12-lt_21^post13 == 0 /\ lt_15^post12-lt_15^post13 == 0 /\ e_10^post12-e_10^post13 == 0 /\ -result_4^post12+result_4^0 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ -lt_24^post12+lt_24^0 == 0 /\ a_6^post12-a_6^post13 == 0 /\ -lt_17^post12+lt_17^0 == 0 /\ f_11^post12-f_11^post13 == 0 /\ lt_18^post12-lt_18^post13 == 0 /\ lt_19^post12-lt_19^post13 == 0 /\ -result_4^post13+result_4^post12 == 0 /\ -cnt_38^post12+cnt_38^0 == 0 /\ lt_24^post12-lt_24^post13 == 0 /\ -c_8^post13+c_8^post12 == 0 /\ lt_18^0-lt_18^post12 == 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^post12, b_7^0'=b_7^post12, c_8^0'=c_8^post12, cnt_38^0'=cnt_38^post12, d_9^0'=d_9^post12, e_10^0'=e_10^post12, f_11^0'=f_11^post12, g_12^0'=g_12^post12, h_13^0'=h_13^post12, lt_14^0'=lt_14^post12, lt_15^0'=lt_15^post12, lt_16^0'=lt_16^post12, lt_17^0'=lt_17^post12, lt_18^0'=lt_18^post12, lt_19^0'=lt_19^post12, lt_20^0'=lt_20^post12, lt_21^0'=lt_21^post12, lt_22^0'=lt_22^post12, lt_23^0'=lt_23^post12, lt_24^0'=lt_24^post12, lt_25^0'=lt_25^post12, result_4^0'=result_4^post12, x_5^0'=x_5^post12, (0 == 0 /\ lt_22^0-lt_22^post12 == 0 /\ e_10^0-e_10^post12 == 0 /\ -x_5^post12+x_5^0 == 0 /\ -b_7^post12+b_7^0 == 0 /\ -a_6^post12+a_6^0 == 0 /\ c_8^0-c_8^post12 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ lt_16^0-lt_16^post12 == 0 /\ -h_13^post12+h_13^0 == 0 /\ -f_11^post12+f_11^0 == 0 /\ -lt_23^post12+lt_23^0 == 0 /\ 1+lt_19^1 <= 0 /\ 1+lt_25^1 <= 0 /\ -d_9^post12+d_9^0 == 0 /\ g_12^0-g_12^post12 == 0 /\ -result_4^post12+result_4^0 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ -lt_24^post12+lt_24^0 == 0 /\ -lt_17^post12+lt_17^0 == 0 /\ -cnt_38^post12+cnt_38^0 == 0 /\ lt_18^0-lt_18^post12 == 0), cost: 1 propagated equality h_13^post13 = h_13^post12 propagated equality lt_25^post13 = lt_25^post12 propagated equality b_7^post13 = b_7^post12 propagated equality d_9^post13 = d_9^post12 propagated equality cnt_38^post13 = cnt_38^post12 propagated equality lt_20^post13 = lt_20^post12 propagated equality lt_14^post13 = lt_14^post12 propagated equality lt_23^post13 = lt_23^post12 propagated equality lt_16^post13 = lt_16^post12 propagated equality g_12^post13 = g_12^post12 propagated equality lt_17^post13 = lt_17^post12 propagated equality x_5^post13 = x_5^post12 propagated equality lt_22^post13 = lt_22^post12 propagated equality lt_21^post13 = lt_21^post12 propagated equality lt_15^post13 = lt_15^post12 propagated equality e_10^post13 = e_10^post12 propagated equality a_6^post13 = a_6^post12 propagated equality f_11^post13 = f_11^post12 propagated equality lt_18^post13 = lt_18^post12 propagated equality lt_19^post13 = lt_19^post12 propagated equality result_4^post13 = result_4^post12 propagated equality lt_24^post13 = lt_24^post12 propagated equality c_8^post13 = c_8^post12 Propagated Equalities Original rule: l3 -> l3 : a_6^0'=a_6^post12, b_7^0'=b_7^post12, c_8^0'=c_8^post12, cnt_38^0'=cnt_38^post12, d_9^0'=d_9^post12, e_10^0'=e_10^post12, f_11^0'=f_11^post12, g_12^0'=g_12^post12, h_13^0'=h_13^post12, lt_14^0'=lt_14^post12, lt_15^0'=lt_15^post12, lt_16^0'=lt_16^post12, lt_17^0'=lt_17^post12, lt_18^0'=lt_18^post12, lt_19^0'=lt_19^post12, lt_20^0'=lt_20^post12, lt_21^0'=lt_21^post12, lt_22^0'=lt_22^post12, lt_23^0'=lt_23^post12, lt_24^0'=lt_24^post12, lt_25^0'=lt_25^post12, result_4^0'=result_4^post12, x_5^0'=x_5^post12, (0 == 0 /\ lt_22^0-lt_22^post12 == 0 /\ e_10^0-e_10^post12 == 0 /\ -x_5^post12+x_5^0 == 0 /\ -b_7^post12+b_7^0 == 0 /\ -a_6^post12+a_6^0 == 0 /\ c_8^0-c_8^post12 == 0 /\ lt_21^1-cnt_38^0 == 0 /\ lt_16^0-lt_16^post12 == 0 /\ -h_13^post12+h_13^0 == 0 /\ -f_11^post12+f_11^0 == 0 /\ -lt_23^post12+lt_23^0 == 0 /\ 1+lt_19^1 <= 0 /\ 1+lt_25^1 <= 0 /\ -d_9^post12+d_9^0 == 0 /\ g_12^0-g_12^post12 == 0 /\ -result_4^post12+result_4^0 == 0 /\ -cnt_38^0+lt_25^1 == 0 /\ -lt_24^post12+lt_24^0 == 0 /\ -lt_17^post12+lt_17^0 == 0 /\ -cnt_38^post12+cnt_38^0 == 0 /\ lt_18^0-lt_18^post12 == 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^post12, lt_15^0'=lt_15^post12, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post12, lt_20^0'=lt_20^post12, lt_21^0'=lt_21^post12, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post12, result_4^0'=result_4^0, x_5^0'=x_5^0, (0 == 0 /\ 1+lt_19^1 <= 0 /\ 1+cnt_38^0 <= 0), cost: 1 propagated equality lt_22^post12 = lt_22^0 propagated equality e_10^post12 = e_10^0 propagated equality x_5^post12 = x_5^0 propagated equality b_7^post12 = b_7^0 propagated equality a_6^post12 = a_6^0 propagated equality c_8^post12 = c_8^0 propagated equality lt_21^1 = cnt_38^0 propagated equality lt_16^post12 = lt_16^0 propagated equality h_13^post12 = h_13^0 propagated equality f_11^post12 = f_11^0 propagated equality lt_23^post12 = lt_23^0 propagated equality d_9^post12 = d_9^0 propagated equality g_12^post12 = g_12^0 propagated equality result_4^post12 = result_4^0 propagated equality lt_25^1 = cnt_38^0 propagated equality lt_24^post12 = lt_24^0 propagated equality lt_17^post12 = lt_17^0 propagated equality cnt_38^post12 = cnt_38^0 propagated equality lt_18^post12 = lt_18^0 Simplified Guard Original rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^post12, lt_15^0'=lt_15^post12, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post12, lt_20^0'=lt_20^post12, lt_21^0'=lt_21^post12, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post12, result_4^0'=result_4^0, x_5^0'=x_5^0, (0 == 0 /\ 1+lt_19^1 <= 0 /\ 1+cnt_38^0 <= 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^post12, lt_15^0'=lt_15^post12, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post12, lt_20^0'=lt_20^post12, lt_21^0'=lt_21^post12, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post12, result_4^0'=result_4^0, x_5^0'=x_5^0, (1+lt_19^1 <= 0 /\ 1+cnt_38^0 <= 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^post12, lt_15^0'=lt_15^post12, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post12, lt_20^0'=lt_20^post12, lt_21^0'=lt_21^post12, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post12, result_4^0'=result_4^0, x_5^0'=x_5^0, (1+lt_19^1 <= 0 /\ 1+cnt_38^0 <= 0), cost: 1 New rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^post12, lt_15^0'=lt_15^post12, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post12, lt_20^0'=lt_20^post12, lt_21^0'=lt_21^post12, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post12, result_4^0'=result_4^0, x_5^0'=x_5^0, (1+cnt_38^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l3 -> l3 : a_6^0'=a_6^0, b_7^0'=b_7^0, c_8^0'=c_8^0, cnt_38^0'=cnt_38^0, d_9^0'=d_9^0, e_10^0'=e_10^0, f_11^0'=f_11^0, g_12^0'=g_12^0, h_13^0'=h_13^0, lt_14^0'=lt_14^post12, lt_15^0'=lt_15^post12, lt_16^0'=lt_16^0, lt_17^0'=lt_17^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post12, lt_20^0'=lt_20^post12, lt_21^0'=lt_21^post12, lt_22^0'=lt_22^0, lt_23^0'=lt_23^0, lt_24^0'=lt_24^0, lt_25^0'=lt_25^post12, result_4^0'=result_4^0, x_5^0'=x_5^0, (1+cnt_38^0 <= 0), cost: 1 New rule: l3 -> l3 : lt_14^0'=lt_14^post12, lt_15^0'=lt_15^post12, lt_19^0'=lt_19^post12, lt_20^0'=lt_20^post12, lt_21^0'=lt_21^post12, lt_25^0'=lt_25^post12, (1+cnt_38^0 <= 0), cost: 1 Step with 23 Trace 23[T] Blocked [{}, {}] Step with 20 Trace 23[T], 20[(-cnt_38^0 <= 0 /\ cnt_38^0 <= 0)] Blocked [{}, {}, {}] Step with 19 Trace 23[T], 20[(-cnt_38^0 <= 0 /\ cnt_38^0 <= 0)], 19[T] Blocked [{}, {}, {}, {}] Backtrack Trace 23[T], 20[(-cnt_38^0 <= 0 /\ cnt_38^0 <= 0)] Blocked [{}, {}, {19[T]}] Backtrack Trace 23[T] Blocked [{}, {20[T]}] Step with 21 Trace 23[T], 21[(-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0)] Blocked [{}, {20[T]}, {}] Step with 19 Trace 23[T], 21[(-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0)], 19[T] Blocked [{}, {20[T]}, {}, {}] Backtrack Trace 23[T], 21[(-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0)] Blocked [{}, {20[T]}, {19[T]}] Backtrack Trace 23[T] Blocked [{}, {20[T], 21[T]}] Step with 22 Trace 23[T], 22[(1+cnt_38^0 <= 0)] Blocked [{}, {20[T], 21[T]}, {}] Backtrack Trace 23[T] Blocked [{}, {20[T], 21[T], 22[T]}] Step with 24 Trace 23[T], 24[(-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0)] Blocked [{}, {20[T], 21[T], 22[T]}, {}] Nonterm Start location: l8 Program variables: a_6^0 b_7^0 c_8^0 cnt_38^0 d_9^0 e_10^0 f_11^0 g_12^0 h_13^0 lt_14^0 lt_15^0 lt_16^0 lt_17^0 lt_18^0 lt_19^0 lt_20^0 lt_21^0 lt_22^0 lt_23^0 lt_24^0 lt_25^0 result_4^0 x_5^0 19: l0 -> l1 : result_4^0'=result_4^post1, T, cost: 1 20: l3 -> l0 : lt_24^0'=lt_24^post3, lt_25^0'=lt_25^post3, (-cnt_38^0 <= 0 /\ cnt_38^0 <= 0), cost: 1 21: l3 -> l0 : lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_22^0'=lt_22^post4, lt_23^0'=lt_23^post4, lt_24^0'=lt_24^post4, lt_25^0'=lt_25^post4, (-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 22: l3 -> l1 : lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, lt_25^0'=lt_25^post5, result_4^0'=result_4^post5, (1+cnt_38^0 <= 0), cost: 1 24: l3 -> l3 : lt_16^0'=lt_16^post6, lt_17^0'=lt_17^post6, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_22^0'=lt_22^post6, lt_23^0'=lt_23^post6, lt_24^0'=lt_24^post6, lt_25^0'=lt_25^post6, (-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 25: l3 -> l3 : lt_14^0'=lt_14^post8, lt_15^0'=lt_15^post8, lt_19^0'=lt_19^post8, lt_22^0'=lt_22^post8, lt_23^0'=lt_23^post8, lt_24^0'=lt_24^post8, lt_25^0'=lt_25^post8, (-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 26: l3 -> l3 : lt_16^0'=lt_16^post10, lt_17^0'=lt_17^post10, lt_18^0'=lt_18^post10, lt_19^0'=lt_19^post10, lt_20^0'=lt_20^post10, lt_21^0'=lt_21^post10, lt_25^0'=lt_25^post10, (1+cnt_38^0 <= 0), cost: 1 27: l3 -> l3 : lt_14^0'=lt_14^post12, lt_15^0'=lt_15^post12, lt_19^0'=lt_19^post12, lt_20^0'=lt_20^post12, lt_21^0'=lt_21^post12, lt_25^0'=lt_25^post12, (1+cnt_38^0 <= 0), cost: 1 28: l3 -> LoAT_sink : (-1+cnt_38^0 >= 0 /\ cnt_38^0 >= 0 /\ -1+n >= 0), cost: NONTERM 23: l8 -> l3 : a_6^0'=x_5^post2, b_7^0'=x_5^post2, c_8^0'=x_5^post2, d_9^0'=x_5^post2, e_10^0'=x_5^post2, f_11^0'=x_5^post2, g_12^0'=x_5^post2, h_13^0'=x_5^post2, x_5^0'=x_5^post2, T, cost: 1 Certificate of Non-Termination Original rule: l3 -> l3 : lt_16^0'=lt_16^post6, lt_17^0'=lt_17^post6, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_22^0'=lt_22^post6, lt_23^0'=lt_23^post6, lt_24^0'=lt_24^post6, lt_25^0'=lt_25^post6, (-cnt_38^0 <= 0 /\ 1-cnt_38^0 <= 0), cost: 1 New rule: l3 -> LoAT_sink : (-1+cnt_38^0 >= 0 /\ cnt_38^0 >= 0 /\ -1+n >= 0), cost: NONTERM -1+cnt_38^0 >= 0 [0]: monotonic increase yields -1+cnt_38^0 >= 0 cnt_38^0 >= 0 [0]: monotonic increase yields cnt_38^0 >= 0, dependencies: -1+cnt_38^0 >= 0 Replacement map: {-1+cnt_38^0 >= 0 -> -1+cnt_38^0 >= 0, cnt_38^0 >= 0 -> cnt_38^0 >= 0} Step with 28 Trace 23[T], 28[(-1+cnt_38^0 >= 0 /\ cnt_38^0 >= 0 /\ -1+n >= 0)] Blocked [{}, {20[T], 21[T], 22[T]}, {28[T]}] Refute Counterexample [ a_6^0=0 b_7^0=0 c_8^0=0 cnt_38^0=1 d_9^0=0 e_10^0=0 f_11^0=0 g_12^0=0 h_13^0=0 lt_14^0=0 lt_15^0=0 lt_16^0=0 lt_17^0=0 lt_18^0=0 lt_19^0=0 lt_20^0=0 lt_21^0=0 lt_22^0=0 lt_23^0=0 lt_24^0=0 lt_25^0=0 result_4^0=0 x_5^0=0 ] 23 [ a_6^0=a_6^0 b_7^0=b_7^0 c_8^0=c_8^0 cnt_38^0=1 d_9^0=d_9^0 e_10^0=e_10^0 f_11^0=f_11^0 g_12^0=g_12^0 h_13^0=h_13^0 lt_14^0=0 lt_15^0=0 lt_16^0=0 lt_17^0=0 lt_18^0=0 lt_19^0=0 lt_20^0=0 lt_21^0=0 lt_22^0=0 lt_23^0=0 lt_24^0=0 lt_25^0=0 result_4^0=0 x_5^0=x_5^0 ] 28 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b