NO Initial ITS Start location: l14 0: l0 -> l1 : tmp_8^0'=tmp_8^post0, __disjvr_0^0'=__disjvr_0^post0, y_6^0'=y_6^post0, __disjvr_2^0'=__disjvr_2^post0, Result_4^0'=Result_4^post0, x_5^0'=x_5^post0, __disjvr_1^0'=__disjvr_1^post0, z_7^0'=z_7^post0, (-z_7^post0+z_7^0 == 0 /\ -__disjvr_1^post0+__disjvr_1^0 == 0 /\ tmp_8^0-tmp_8^post0 == 0 /\ -__disjvr_2^post0+__disjvr_2^0 == 0 /\ y_6^0-y_6^post0 == 0 /\ -__disjvr_0^post0+__disjvr_0^0 == 0 /\ x_5^0-x_5^post0 == 0 /\ Result_4^0-Result_4^post0 == 0), cost: 1 7: l1 -> l7 : tmp_8^0'=tmp_8^post7, __disjvr_0^0'=__disjvr_0^post7, y_6^0'=y_6^post7, __disjvr_2^0'=__disjvr_2^post7, Result_4^0'=Result_4^post7, x_5^0'=x_5^post7, __disjvr_1^0'=__disjvr_1^post7, z_7^0'=z_7^post7, (1-y_6^0+x_5^0 <= 0 /\ tmp_8^0-tmp_8^post7 == 0 /\ Result_4^0-Result_4^post7 == 0 /\ -z_7^post7+z_7^0 == 0 /\ __disjvr_1^0-__disjvr_1^post7 == 0 /\ -y_6^post7+y_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post7 == 0 /\ -x_5^post7+x_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post7 == 0), cost: 1 8: l1 -> l8 : tmp_8^0'=tmp_8^post8, __disjvr_0^0'=__disjvr_0^post8, y_6^0'=y_6^post8, __disjvr_2^0'=__disjvr_2^post8, Result_4^0'=Result_4^post8, x_5^0'=x_5^post8, __disjvr_1^0'=__disjvr_1^post8, z_7^0'=z_7^post8, (0 == 0 /\ y_6^0-y_6^post8 == 0 /\ y_6^0-x_5^0 <= 0 /\ -z_7^post8+z_7^0 == 0 /\ -__disjvr_2^post8+__disjvr_2^0 == 0 /\ x_5^0-x_5^post8 == 0 /\ __disjvr_0^0-__disjvr_0^post8 == 0 /\ tmp_8^0-tmp_8^post8 == 0 /\ -__disjvr_1^post8+__disjvr_1^0 == 0), cost: 1 1: l2 -> l3 : tmp_8^0'=tmp_8^post1, __disjvr_0^0'=__disjvr_0^post1, y_6^0'=y_6^post1, __disjvr_2^0'=__disjvr_2^post1, Result_4^0'=Result_4^post1, x_5^0'=x_5^post1, __disjvr_1^0'=__disjvr_1^post1, z_7^0'=z_7^post1, (0 == 0 /\ -tmp_8^post1 <= 0 /\ __disjvr_0^0-__disjvr_0^post1 == 0 /\ __disjvr_2^0-__disjvr_2^post1 == 0 /\ -__disjvr_1^post1+__disjvr_1^0 == 0 /\ -z_7^post1+z_7^0 == 0 /\ -x_5^post1+x_5^0 == 0 /\ -Result_4^post1+Result_4^0 == 0 /\ tmp_8^post1 <= 0 /\ 1+y_6^0-z_7^0 <= 0 /\ -y_6^post1+y_6^0 == 0), cost: 1 2: l2 -> l5 : tmp_8^0'=tmp_8^post2, __disjvr_0^0'=__disjvr_0^post2, y_6^0'=y_6^post2, __disjvr_2^0'=__disjvr_2^post2, Result_4^0'=Result_4^post2, x_5^0'=x_5^post2, __disjvr_1^0'=__disjvr_1^post2, z_7^0'=z_7^post2, (0 == 0 /\ -z_7^post2+z_7^0 == 0 /\ y_6^0-y_6^post2 == 0 /\ -x_5^post2+x_5^0 == 0 /\ Result_4^0-Result_4^post2 == 0 /\ -__disjvr_0^post2+__disjvr_0^0 == 0 /\ 1+y_6^0-z_7^0 <= 0 /\ -__disjvr_1^post2+__disjvr_1^0 == 0 /\ __disjvr_2^0-__disjvr_2^post2 == 0), cost: 1 6: l2 -> l1 : tmp_8^0'=tmp_8^post6, __disjvr_0^0'=__disjvr_0^post6, y_6^0'=y_6^post6, __disjvr_2^0'=__disjvr_2^post6, Result_4^0'=Result_4^post6, x_5^0'=x_5^post6, __disjvr_1^0'=__disjvr_1^post6, z_7^0'=z_7^post6, (-__disjvr_2^post6+__disjvr_2^0 == 0 /\ -1-x_5^0+x_5^post6 == 0 /\ y_6^0-y_6^post6 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ tmp_8^0-tmp_8^post6 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0 /\ -y_6^0+z_7^0 <= 0 /\ -z_7^post6+z_7^0 == 0 /\ Result_4^0-Result_4^post6 == 0), cost: 1 14: l3 -> l11 : tmp_8^0'=tmp_8^post14, __disjvr_0^0'=__disjvr_0^post14, y_6^0'=y_6^post14, __disjvr_2^0'=__disjvr_2^post14, Result_4^0'=Result_4^post14, x_5^0'=x_5^post14, __disjvr_1^0'=__disjvr_1^post14, z_7^0'=z_7^post14, (0 == 0 /\ tmp_8^post14 <= 0 /\ __disjvr_0^0-__disjvr_0^post14 == 0 /\ -y_6^post14+y_6^0 == 0 /\ -z_7^post14+z_7^0 == 0 /\ -__disjvr_1^post14+__disjvr_1^0 == 0 /\ -tmp_8^post14 <= 0 /\ __disjvr_2^0-__disjvr_2^post14 == 0 /\ -x_5^post14+x_5^0 == 0 /\ 1+y_6^0-z_7^0 <= 0 /\ -Result_4^post14+Result_4^0 == 0), cost: 1 16: l3 -> l12 : tmp_8^0'=tmp_8^post16, __disjvr_0^0'=__disjvr_0^post16, y_6^0'=y_6^post16, __disjvr_2^0'=__disjvr_2^post16, Result_4^0'=Result_4^post16, x_5^0'=x_5^post16, __disjvr_1^0'=__disjvr_1^post16, z_7^0'=z_7^post16, (0 == 0 /\ __disjvr_0^0-__disjvr_0^post16 == 0 /\ -x_5^post16+x_5^0 == 0 /\ -Result_4^post16+Result_4^0 == 0 /\ -__disjvr_1^post16+__disjvr_1^0 == 0 /\ __disjvr_2^0-__disjvr_2^post16 == 0 /\ -z_7^post16+z_7^0 == 0 /\ -y_6^post16+y_6^0 == 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 1 3: l5 -> l6 : tmp_8^0'=tmp_8^post3, __disjvr_0^0'=__disjvr_0^post3, y_6^0'=y_6^post3, __disjvr_2^0'=__disjvr_2^post3, Result_4^0'=Result_4^post3, x_5^0'=x_5^post3, __disjvr_1^0'=__disjvr_1^post3, z_7^0'=z_7^post3, (__disjvr_0^0-__disjvr_0^post3 == 0 /\ -y_6^post3+y_6^0 == 0 /\ -x_5^post3+x_5^0 == 0 /\ -__disjvr_1^post3+__disjvr_1^0 == 0 /\ tmp_8^0-tmp_8^post3 == 0 /\ -__disjvr_0^0+__disjvr_0^post3 == 0 /\ -Result_4^post3+Result_4^0 == 0 /\ -z_7^post3+z_7^0 == 0 /\ __disjvr_2^0-__disjvr_2^post3 == 0), cost: 1 4: l6 -> l4 : tmp_8^0'=tmp_8^post4, __disjvr_0^0'=__disjvr_0^post4, y_6^0'=y_6^post4, __disjvr_2^0'=__disjvr_2^post4, Result_4^0'=Result_4^post4, x_5^0'=x_5^post4, __disjvr_1^0'=__disjvr_1^post4, z_7^0'=z_7^post4, (tmp_8^0-tmp_8^post4 == 0 /\ -__disjvr_2^post4+__disjvr_2^0 == 0 /\ Result_4^0-Result_4^post4 == 0 /\ -__disjvr_1^post4+__disjvr_1^0 == 0 /\ __disjvr_0^0-__disjvr_0^post4 == 0 /\ -1-y_6^0+y_6^post4 == 0 /\ x_5^0-x_5^post4 == 0 /\ -z_7^post4+z_7^0 == 0), cost: 1 5: l4 -> l2 : tmp_8^0'=tmp_8^post5, __disjvr_0^0'=__disjvr_0^post5, y_6^0'=y_6^post5, __disjvr_2^0'=__disjvr_2^post5, Result_4^0'=Result_4^post5, x_5^0'=x_5^post5, __disjvr_1^0'=__disjvr_1^post5, z_7^0'=z_7^post5, (-__disjvr_1^post5+__disjvr_1^0 == 0 /\ -z_7^post5+z_7^0 == 0 /\ tmp_8^0-tmp_8^post5 == 0 /\ -Result_4^post5+Result_4^0 == 0 /\ -x_5^post5+x_5^0 == 0 /\ __disjvr_2^0-__disjvr_2^post5 == 0 /\ -y_6^post5+y_6^0 == 0 /\ __disjvr_0^0-__disjvr_0^post5 == 0), cost: 1 9: l7 -> l3 : tmp_8^0'=tmp_8^post9, __disjvr_0^0'=__disjvr_0^post9, y_6^0'=y_6^post9, __disjvr_2^0'=__disjvr_2^post9, Result_4^0'=Result_4^post9, x_5^0'=x_5^post9, __disjvr_1^0'=__disjvr_1^post9, z_7^0'=z_7^post9, (0 == 0 /\ -y_6^post9+y_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post9 == 0 /\ __disjvr_1^0-__disjvr_1^post9 == 0 /\ __disjvr_0^0-__disjvr_0^post9 == 0 /\ -z_7^post9+z_7^0 == 0 /\ tmp_8^post9 <= 0 /\ -tmp_8^post9 <= 0 /\ -x_5^post9+x_5^0 == 0 /\ 1+y_6^0-z_7^0 <= 0 /\ -Result_4^post9+Result_4^0 == 0), cost: 1 10: l7 -> l9 : tmp_8^0'=tmp_8^post10, __disjvr_0^0'=__disjvr_0^post10, y_6^0'=y_6^post10, __disjvr_2^0'=__disjvr_2^post10, Result_4^0'=Result_4^post10, x_5^0'=x_5^post10, __disjvr_1^0'=__disjvr_1^post10, z_7^0'=z_7^post10, (0 == 0 /\ y_6^0-y_6^post10 == 0 /\ -__disjvr_1^post10+__disjvr_1^0 == 0 /\ -z_7^post10+z_7^0 == 0 /\ x_5^0-x_5^post10 == 0 /\ -__disjvr_2^post10+__disjvr_2^0 == 0 /\ -Result_4^post10+Result_4^0 == 0 /\ 1+y_6^0-z_7^0 <= 0 /\ __disjvr_0^0-__disjvr_0^post10 == 0), cost: 1 13: l7 -> l1 : tmp_8^0'=tmp_8^post13, __disjvr_0^0'=__disjvr_0^post13, y_6^0'=y_6^post13, __disjvr_2^0'=__disjvr_2^post13, Result_4^0'=Result_4^post13, x_5^0'=x_5^post13, __disjvr_1^0'=__disjvr_1^post13, z_7^0'=z_7^post13, (Result_4^0-Result_4^post13 == 0 /\ tmp_8^0-tmp_8^post13 == 0 /\ -__disjvr_1^post13+__disjvr_1^0 == 0 /\ -__disjvr_2^post13+__disjvr_2^0 == 0 /\ y_6^0-y_6^post13 == 0 /\ -1+x_5^post13-x_5^0 == 0 /\ -y_6^0+z_7^0 <= 0 /\ -__disjvr_0^post13+__disjvr_0^0 == 0 /\ -z_7^post13+z_7^0 == 0), cost: 1 11: l9 -> l10 : tmp_8^0'=tmp_8^post11, __disjvr_0^0'=__disjvr_0^post11, y_6^0'=y_6^post11, __disjvr_2^0'=__disjvr_2^post11, Result_4^0'=Result_4^post11, x_5^0'=x_5^post11, __disjvr_1^0'=__disjvr_1^post11, z_7^0'=z_7^post11, (tmp_8^0-tmp_8^post11 == 0 /\ Result_4^0-Result_4^post11 == 0 /\ -y_6^post11+y_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post11 == 0 /\ __disjvr_0^0-__disjvr_0^post11 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ -z_7^post11+z_7^0 == 0 /\ -x_5^post11+x_5^0 == 0 /\ __disjvr_1^post11-__disjvr_1^0 == 0), cost: 1 12: l10 -> l2 : tmp_8^0'=tmp_8^post12, __disjvr_0^0'=__disjvr_0^post12, y_6^0'=y_6^post12, __disjvr_2^0'=__disjvr_2^post12, Result_4^0'=Result_4^post12, x_5^0'=x_5^post12, __disjvr_1^0'=__disjvr_1^post12, z_7^0'=z_7^post12, (__disjvr_0^0-__disjvr_0^post12 == 0 /\ -Result_4^post12+Result_4^0 == 0 /\ -z_7^post12+z_7^0 == 0 /\ -x_5^post12+x_5^0 == 0 /\ -tmp_8^post12+tmp_8^0 == 0 /\ -1+y_6^post12-y_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post12 == 0 /\ -__disjvr_1^post12+__disjvr_1^0 == 0), cost: 1 15: l11 -> l3 : tmp_8^0'=tmp_8^post15, __disjvr_0^0'=__disjvr_0^post15, y_6^0'=y_6^post15, __disjvr_2^0'=__disjvr_2^post15, Result_4^0'=Result_4^post15, x_5^0'=x_5^post15, __disjvr_1^0'=__disjvr_1^post15, z_7^0'=z_7^post15, (-__disjvr_0^post15+__disjvr_0^0 == 0 /\ -__disjvr_1^post15+__disjvr_1^0 == 0 /\ -z_7^post15+z_7^0 == 0 /\ y_6^0-y_6^post15 == 0 /\ tmp_8^0-tmp_8^post15 == 0 /\ __disjvr_2^0-__disjvr_2^post15 == 0 /\ Result_4^0-Result_4^post15 == 0 /\ x_5^0-x_5^post15 == 0), cost: 1 17: l12 -> l13 : tmp_8^0'=tmp_8^post17, __disjvr_0^0'=__disjvr_0^post17, y_6^0'=y_6^post17, __disjvr_2^0'=__disjvr_2^post17, Result_4^0'=Result_4^post17, x_5^0'=x_5^post17, __disjvr_1^0'=__disjvr_1^post17, z_7^0'=z_7^post17, (tmp_8^0-tmp_8^post17 == 0 /\ -__disjvr_2^post17+__disjvr_2^0 == 0 /\ y_6^0-y_6^post17 == 0 /\ -z_7^post17+z_7^0 == 0 /\ __disjvr_2^post17-__disjvr_2^0 == 0 /\ -x_5^post17+x_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post17 == 0 /\ Result_4^0-Result_4^post17 == 0 /\ -__disjvr_1^post17+__disjvr_1^0 == 0), cost: 1 18: l13 -> l2 : tmp_8^0'=tmp_8^post18, __disjvr_0^0'=__disjvr_0^post18, y_6^0'=y_6^post18, __disjvr_2^0'=__disjvr_2^post18, Result_4^0'=Result_4^post18, x_5^0'=x_5^post18, __disjvr_1^0'=__disjvr_1^post18, z_7^0'=z_7^post18, (-z_7^post18+z_7^0 == 0 /\ __disjvr_0^0-__disjvr_0^post18 == 0 /\ -__disjvr_1^post18+__disjvr_1^0 == 0 /\ tmp_8^0-tmp_8^post18 == 0 /\ -Result_4^post18+Result_4^0 == 0 /\ -x_5^post18+x_5^0 == 0 /\ -1+y_6^post18-y_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post18 == 0), cost: 1 19: l14 -> l0 : tmp_8^0'=tmp_8^post19, __disjvr_0^0'=__disjvr_0^post19, y_6^0'=y_6^post19, __disjvr_2^0'=__disjvr_2^post19, Result_4^0'=Result_4^post19, x_5^0'=x_5^post19, __disjvr_1^0'=__disjvr_1^post19, z_7^0'=z_7^post19, (y_6^0-y_6^post19 == 0 /\ tmp_8^0-tmp_8^post19 == 0 /\ -__disjvr_2^post19+__disjvr_2^0 == 0 /\ -z_7^post19+z_7^0 == 0 /\ x_5^0-x_5^post19 == 0 /\ -__disjvr_0^post19+__disjvr_0^0 == 0 /\ -__disjvr_1^post19+__disjvr_1^0 == 0 /\ -Result_4^post19+Result_4^0 == 0), cost: 1 Removed unreachable rules and leafs Start location: l14 0: l0 -> l1 : tmp_8^0'=tmp_8^post0, __disjvr_0^0'=__disjvr_0^post0, y_6^0'=y_6^post0, __disjvr_2^0'=__disjvr_2^post0, Result_4^0'=Result_4^post0, x_5^0'=x_5^post0, __disjvr_1^0'=__disjvr_1^post0, z_7^0'=z_7^post0, (-z_7^post0+z_7^0 == 0 /\ -__disjvr_1^post0+__disjvr_1^0 == 0 /\ tmp_8^0-tmp_8^post0 == 0 /\ -__disjvr_2^post0+__disjvr_2^0 == 0 /\ y_6^0-y_6^post0 == 0 /\ -__disjvr_0^post0+__disjvr_0^0 == 0 /\ x_5^0-x_5^post0 == 0 /\ Result_4^0-Result_4^post0 == 0), cost: 1 7: l1 -> l7 : tmp_8^0'=tmp_8^post7, __disjvr_0^0'=__disjvr_0^post7, y_6^0'=y_6^post7, __disjvr_2^0'=__disjvr_2^post7, Result_4^0'=Result_4^post7, x_5^0'=x_5^post7, __disjvr_1^0'=__disjvr_1^post7, z_7^0'=z_7^post7, (1-y_6^0+x_5^0 <= 0 /\ tmp_8^0-tmp_8^post7 == 0 /\ Result_4^0-Result_4^post7 == 0 /\ -z_7^post7+z_7^0 == 0 /\ __disjvr_1^0-__disjvr_1^post7 == 0 /\ -y_6^post7+y_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post7 == 0 /\ -x_5^post7+x_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post7 == 0), cost: 1 1: l2 -> l3 : tmp_8^0'=tmp_8^post1, __disjvr_0^0'=__disjvr_0^post1, y_6^0'=y_6^post1, __disjvr_2^0'=__disjvr_2^post1, Result_4^0'=Result_4^post1, x_5^0'=x_5^post1, __disjvr_1^0'=__disjvr_1^post1, z_7^0'=z_7^post1, (0 == 0 /\ -tmp_8^post1 <= 0 /\ __disjvr_0^0-__disjvr_0^post1 == 0 /\ __disjvr_2^0-__disjvr_2^post1 == 0 /\ -__disjvr_1^post1+__disjvr_1^0 == 0 /\ -z_7^post1+z_7^0 == 0 /\ -x_5^post1+x_5^0 == 0 /\ -Result_4^post1+Result_4^0 == 0 /\ tmp_8^post1 <= 0 /\ 1+y_6^0-z_7^0 <= 0 /\ -y_6^post1+y_6^0 == 0), cost: 1 2: l2 -> l5 : tmp_8^0'=tmp_8^post2, __disjvr_0^0'=__disjvr_0^post2, y_6^0'=y_6^post2, __disjvr_2^0'=__disjvr_2^post2, Result_4^0'=Result_4^post2, x_5^0'=x_5^post2, __disjvr_1^0'=__disjvr_1^post2, z_7^0'=z_7^post2, (0 == 0 /\ -z_7^post2+z_7^0 == 0 /\ y_6^0-y_6^post2 == 0 /\ -x_5^post2+x_5^0 == 0 /\ Result_4^0-Result_4^post2 == 0 /\ -__disjvr_0^post2+__disjvr_0^0 == 0 /\ 1+y_6^0-z_7^0 <= 0 /\ -__disjvr_1^post2+__disjvr_1^0 == 0 /\ __disjvr_2^0-__disjvr_2^post2 == 0), cost: 1 6: l2 -> l1 : tmp_8^0'=tmp_8^post6, __disjvr_0^0'=__disjvr_0^post6, y_6^0'=y_6^post6, __disjvr_2^0'=__disjvr_2^post6, Result_4^0'=Result_4^post6, x_5^0'=x_5^post6, __disjvr_1^0'=__disjvr_1^post6, z_7^0'=z_7^post6, (-__disjvr_2^post6+__disjvr_2^0 == 0 /\ -1-x_5^0+x_5^post6 == 0 /\ y_6^0-y_6^post6 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ tmp_8^0-tmp_8^post6 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0 /\ -y_6^0+z_7^0 <= 0 /\ -z_7^post6+z_7^0 == 0 /\ Result_4^0-Result_4^post6 == 0), cost: 1 14: l3 -> l11 : tmp_8^0'=tmp_8^post14, __disjvr_0^0'=__disjvr_0^post14, y_6^0'=y_6^post14, __disjvr_2^0'=__disjvr_2^post14, Result_4^0'=Result_4^post14, x_5^0'=x_5^post14, __disjvr_1^0'=__disjvr_1^post14, z_7^0'=z_7^post14, (0 == 0 /\ tmp_8^post14 <= 0 /\ __disjvr_0^0-__disjvr_0^post14 == 0 /\ -y_6^post14+y_6^0 == 0 /\ -z_7^post14+z_7^0 == 0 /\ -__disjvr_1^post14+__disjvr_1^0 == 0 /\ -tmp_8^post14 <= 0 /\ __disjvr_2^0-__disjvr_2^post14 == 0 /\ -x_5^post14+x_5^0 == 0 /\ 1+y_6^0-z_7^0 <= 0 /\ -Result_4^post14+Result_4^0 == 0), cost: 1 16: l3 -> l12 : tmp_8^0'=tmp_8^post16, __disjvr_0^0'=__disjvr_0^post16, y_6^0'=y_6^post16, __disjvr_2^0'=__disjvr_2^post16, Result_4^0'=Result_4^post16, x_5^0'=x_5^post16, __disjvr_1^0'=__disjvr_1^post16, z_7^0'=z_7^post16, (0 == 0 /\ __disjvr_0^0-__disjvr_0^post16 == 0 /\ -x_5^post16+x_5^0 == 0 /\ -Result_4^post16+Result_4^0 == 0 /\ -__disjvr_1^post16+__disjvr_1^0 == 0 /\ __disjvr_2^0-__disjvr_2^post16 == 0 /\ -z_7^post16+z_7^0 == 0 /\ -y_6^post16+y_6^0 == 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 1 3: l5 -> l6 : tmp_8^0'=tmp_8^post3, __disjvr_0^0'=__disjvr_0^post3, y_6^0'=y_6^post3, __disjvr_2^0'=__disjvr_2^post3, Result_4^0'=Result_4^post3, x_5^0'=x_5^post3, __disjvr_1^0'=__disjvr_1^post3, z_7^0'=z_7^post3, (__disjvr_0^0-__disjvr_0^post3 == 0 /\ -y_6^post3+y_6^0 == 0 /\ -x_5^post3+x_5^0 == 0 /\ -__disjvr_1^post3+__disjvr_1^0 == 0 /\ tmp_8^0-tmp_8^post3 == 0 /\ -__disjvr_0^0+__disjvr_0^post3 == 0 /\ -Result_4^post3+Result_4^0 == 0 /\ -z_7^post3+z_7^0 == 0 /\ __disjvr_2^0-__disjvr_2^post3 == 0), cost: 1 4: l6 -> l4 : tmp_8^0'=tmp_8^post4, __disjvr_0^0'=__disjvr_0^post4, y_6^0'=y_6^post4, __disjvr_2^0'=__disjvr_2^post4, Result_4^0'=Result_4^post4, x_5^0'=x_5^post4, __disjvr_1^0'=__disjvr_1^post4, z_7^0'=z_7^post4, (tmp_8^0-tmp_8^post4 == 0 /\ -__disjvr_2^post4+__disjvr_2^0 == 0 /\ Result_4^0-Result_4^post4 == 0 /\ -__disjvr_1^post4+__disjvr_1^0 == 0 /\ __disjvr_0^0-__disjvr_0^post4 == 0 /\ -1-y_6^0+y_6^post4 == 0 /\ x_5^0-x_5^post4 == 0 /\ -z_7^post4+z_7^0 == 0), cost: 1 5: l4 -> l2 : tmp_8^0'=tmp_8^post5, __disjvr_0^0'=__disjvr_0^post5, y_6^0'=y_6^post5, __disjvr_2^0'=__disjvr_2^post5, Result_4^0'=Result_4^post5, x_5^0'=x_5^post5, __disjvr_1^0'=__disjvr_1^post5, z_7^0'=z_7^post5, (-__disjvr_1^post5+__disjvr_1^0 == 0 /\ -z_7^post5+z_7^0 == 0 /\ tmp_8^0-tmp_8^post5 == 0 /\ -Result_4^post5+Result_4^0 == 0 /\ -x_5^post5+x_5^0 == 0 /\ __disjvr_2^0-__disjvr_2^post5 == 0 /\ -y_6^post5+y_6^0 == 0 /\ __disjvr_0^0-__disjvr_0^post5 == 0), cost: 1 9: l7 -> l3 : tmp_8^0'=tmp_8^post9, __disjvr_0^0'=__disjvr_0^post9, y_6^0'=y_6^post9, __disjvr_2^0'=__disjvr_2^post9, Result_4^0'=Result_4^post9, x_5^0'=x_5^post9, __disjvr_1^0'=__disjvr_1^post9, z_7^0'=z_7^post9, (0 == 0 /\ -y_6^post9+y_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post9 == 0 /\ __disjvr_1^0-__disjvr_1^post9 == 0 /\ __disjvr_0^0-__disjvr_0^post9 == 0 /\ -z_7^post9+z_7^0 == 0 /\ tmp_8^post9 <= 0 /\ -tmp_8^post9 <= 0 /\ -x_5^post9+x_5^0 == 0 /\ 1+y_6^0-z_7^0 <= 0 /\ -Result_4^post9+Result_4^0 == 0), cost: 1 10: l7 -> l9 : tmp_8^0'=tmp_8^post10, __disjvr_0^0'=__disjvr_0^post10, y_6^0'=y_6^post10, __disjvr_2^0'=__disjvr_2^post10, Result_4^0'=Result_4^post10, x_5^0'=x_5^post10, __disjvr_1^0'=__disjvr_1^post10, z_7^0'=z_7^post10, (0 == 0 /\ y_6^0-y_6^post10 == 0 /\ -__disjvr_1^post10+__disjvr_1^0 == 0 /\ -z_7^post10+z_7^0 == 0 /\ x_5^0-x_5^post10 == 0 /\ -__disjvr_2^post10+__disjvr_2^0 == 0 /\ -Result_4^post10+Result_4^0 == 0 /\ 1+y_6^0-z_7^0 <= 0 /\ __disjvr_0^0-__disjvr_0^post10 == 0), cost: 1 13: l7 -> l1 : tmp_8^0'=tmp_8^post13, __disjvr_0^0'=__disjvr_0^post13, y_6^0'=y_6^post13, __disjvr_2^0'=__disjvr_2^post13, Result_4^0'=Result_4^post13, x_5^0'=x_5^post13, __disjvr_1^0'=__disjvr_1^post13, z_7^0'=z_7^post13, (Result_4^0-Result_4^post13 == 0 /\ tmp_8^0-tmp_8^post13 == 0 /\ -__disjvr_1^post13+__disjvr_1^0 == 0 /\ -__disjvr_2^post13+__disjvr_2^0 == 0 /\ y_6^0-y_6^post13 == 0 /\ -1+x_5^post13-x_5^0 == 0 /\ -y_6^0+z_7^0 <= 0 /\ -__disjvr_0^post13+__disjvr_0^0 == 0 /\ -z_7^post13+z_7^0 == 0), cost: 1 11: l9 -> l10 : tmp_8^0'=tmp_8^post11, __disjvr_0^0'=__disjvr_0^post11, y_6^0'=y_6^post11, __disjvr_2^0'=__disjvr_2^post11, Result_4^0'=Result_4^post11, x_5^0'=x_5^post11, __disjvr_1^0'=__disjvr_1^post11, z_7^0'=z_7^post11, (tmp_8^0-tmp_8^post11 == 0 /\ Result_4^0-Result_4^post11 == 0 /\ -y_6^post11+y_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post11 == 0 /\ __disjvr_0^0-__disjvr_0^post11 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ -z_7^post11+z_7^0 == 0 /\ -x_5^post11+x_5^0 == 0 /\ __disjvr_1^post11-__disjvr_1^0 == 0), cost: 1 12: l10 -> l2 : tmp_8^0'=tmp_8^post12, __disjvr_0^0'=__disjvr_0^post12, y_6^0'=y_6^post12, __disjvr_2^0'=__disjvr_2^post12, Result_4^0'=Result_4^post12, x_5^0'=x_5^post12, __disjvr_1^0'=__disjvr_1^post12, z_7^0'=z_7^post12, (__disjvr_0^0-__disjvr_0^post12 == 0 /\ -Result_4^post12+Result_4^0 == 0 /\ -z_7^post12+z_7^0 == 0 /\ -x_5^post12+x_5^0 == 0 /\ -tmp_8^post12+tmp_8^0 == 0 /\ -1+y_6^post12-y_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post12 == 0 /\ -__disjvr_1^post12+__disjvr_1^0 == 0), cost: 1 15: l11 -> l3 : tmp_8^0'=tmp_8^post15, __disjvr_0^0'=__disjvr_0^post15, y_6^0'=y_6^post15, __disjvr_2^0'=__disjvr_2^post15, Result_4^0'=Result_4^post15, x_5^0'=x_5^post15, __disjvr_1^0'=__disjvr_1^post15, z_7^0'=z_7^post15, (-__disjvr_0^post15+__disjvr_0^0 == 0 /\ -__disjvr_1^post15+__disjvr_1^0 == 0 /\ -z_7^post15+z_7^0 == 0 /\ y_6^0-y_6^post15 == 0 /\ tmp_8^0-tmp_8^post15 == 0 /\ __disjvr_2^0-__disjvr_2^post15 == 0 /\ Result_4^0-Result_4^post15 == 0 /\ x_5^0-x_5^post15 == 0), cost: 1 17: l12 -> l13 : tmp_8^0'=tmp_8^post17, __disjvr_0^0'=__disjvr_0^post17, y_6^0'=y_6^post17, __disjvr_2^0'=__disjvr_2^post17, Result_4^0'=Result_4^post17, x_5^0'=x_5^post17, __disjvr_1^0'=__disjvr_1^post17, z_7^0'=z_7^post17, (tmp_8^0-tmp_8^post17 == 0 /\ -__disjvr_2^post17+__disjvr_2^0 == 0 /\ y_6^0-y_6^post17 == 0 /\ -z_7^post17+z_7^0 == 0 /\ __disjvr_2^post17-__disjvr_2^0 == 0 /\ -x_5^post17+x_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post17 == 0 /\ Result_4^0-Result_4^post17 == 0 /\ -__disjvr_1^post17+__disjvr_1^0 == 0), cost: 1 18: l13 -> l2 : tmp_8^0'=tmp_8^post18, __disjvr_0^0'=__disjvr_0^post18, y_6^0'=y_6^post18, __disjvr_2^0'=__disjvr_2^post18, Result_4^0'=Result_4^post18, x_5^0'=x_5^post18, __disjvr_1^0'=__disjvr_1^post18, z_7^0'=z_7^post18, (-z_7^post18+z_7^0 == 0 /\ __disjvr_0^0-__disjvr_0^post18 == 0 /\ -__disjvr_1^post18+__disjvr_1^0 == 0 /\ tmp_8^0-tmp_8^post18 == 0 /\ -Result_4^post18+Result_4^0 == 0 /\ -x_5^post18+x_5^0 == 0 /\ -1+y_6^post18-y_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post18 == 0), cost: 1 19: l14 -> l0 : tmp_8^0'=tmp_8^post19, __disjvr_0^0'=__disjvr_0^post19, y_6^0'=y_6^post19, __disjvr_2^0'=__disjvr_2^post19, Result_4^0'=Result_4^post19, x_5^0'=x_5^post19, __disjvr_1^0'=__disjvr_1^post19, z_7^0'=z_7^post19, (y_6^0-y_6^post19 == 0 /\ tmp_8^0-tmp_8^post19 == 0 /\ -__disjvr_2^post19+__disjvr_2^0 == 0 /\ -z_7^post19+z_7^0 == 0 /\ x_5^0-x_5^post19 == 0 /\ -__disjvr_0^post19+__disjvr_0^0 == 0 /\ -__disjvr_1^post19+__disjvr_1^0 == 0 /\ -Result_4^post19+Result_4^0 == 0), cost: 1 Applied preprocessing Original rule: l0 -> l1 : tmp_8^0'=tmp_8^post0, __disjvr_0^0'=__disjvr_0^post0, y_6^0'=y_6^post0, __disjvr_2^0'=__disjvr_2^post0, Result_4^0'=Result_4^post0, x_5^0'=x_5^post0, __disjvr_1^0'=__disjvr_1^post0, z_7^0'=z_7^post0, (-z_7^post0+z_7^0 == 0 /\ -__disjvr_1^post0+__disjvr_1^0 == 0 /\ tmp_8^0-tmp_8^post0 == 0 /\ -__disjvr_2^post0+__disjvr_2^0 == 0 /\ y_6^0-y_6^post0 == 0 /\ -__disjvr_0^post0+__disjvr_0^0 == 0 /\ x_5^0-x_5^post0 == 0 /\ Result_4^0-Result_4^post0 == 0), cost: 1 New rule: l0 -> l1 : TRUE, cost: 1 Applied preprocessing Original rule: l2 -> l3 : tmp_8^0'=tmp_8^post1, __disjvr_0^0'=__disjvr_0^post1, y_6^0'=y_6^post1, __disjvr_2^0'=__disjvr_2^post1, Result_4^0'=Result_4^post1, x_5^0'=x_5^post1, __disjvr_1^0'=__disjvr_1^post1, z_7^0'=z_7^post1, (0 == 0 /\ -tmp_8^post1 <= 0 /\ __disjvr_0^0-__disjvr_0^post1 == 0 /\ __disjvr_2^0-__disjvr_2^post1 == 0 /\ -__disjvr_1^post1+__disjvr_1^0 == 0 /\ -z_7^post1+z_7^0 == 0 /\ -x_5^post1+x_5^0 == 0 /\ -Result_4^post1+Result_4^0 == 0 /\ tmp_8^post1 <= 0 /\ 1+y_6^0-z_7^0 <= 0 /\ -y_6^post1+y_6^0 == 0), cost: 1 New rule: l2 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 Applied preprocessing Original rule: l2 -> l5 : tmp_8^0'=tmp_8^post2, __disjvr_0^0'=__disjvr_0^post2, y_6^0'=y_6^post2, __disjvr_2^0'=__disjvr_2^post2, Result_4^0'=Result_4^post2, x_5^0'=x_5^post2, __disjvr_1^0'=__disjvr_1^post2, z_7^0'=z_7^post2, (0 == 0 /\ -z_7^post2+z_7^0 == 0 /\ y_6^0-y_6^post2 == 0 /\ -x_5^post2+x_5^0 == 0 /\ Result_4^0-Result_4^post2 == 0 /\ -__disjvr_0^post2+__disjvr_0^0 == 0 /\ 1+y_6^0-z_7^0 <= 0 /\ -__disjvr_1^post2+__disjvr_1^0 == 0 /\ __disjvr_2^0-__disjvr_2^post2 == 0), cost: 1 New rule: l2 -> l5 : tmp_8^0'=tmp_8^post2, 1+y_6^0-z_7^0 <= 0, cost: 1 Applied preprocessing Original rule: l5 -> l6 : tmp_8^0'=tmp_8^post3, __disjvr_0^0'=__disjvr_0^post3, y_6^0'=y_6^post3, __disjvr_2^0'=__disjvr_2^post3, Result_4^0'=Result_4^post3, x_5^0'=x_5^post3, __disjvr_1^0'=__disjvr_1^post3, z_7^0'=z_7^post3, (__disjvr_0^0-__disjvr_0^post3 == 0 /\ -y_6^post3+y_6^0 == 0 /\ -x_5^post3+x_5^0 == 0 /\ -__disjvr_1^post3+__disjvr_1^0 == 0 /\ tmp_8^0-tmp_8^post3 == 0 /\ -__disjvr_0^0+__disjvr_0^post3 == 0 /\ -Result_4^post3+Result_4^0 == 0 /\ -z_7^post3+z_7^0 == 0 /\ __disjvr_2^0-__disjvr_2^post3 == 0), cost: 1 New rule: l5 -> l6 : 0 == 0, cost: 1 Applied preprocessing Original rule: l6 -> l4 : tmp_8^0'=tmp_8^post4, __disjvr_0^0'=__disjvr_0^post4, y_6^0'=y_6^post4, __disjvr_2^0'=__disjvr_2^post4, Result_4^0'=Result_4^post4, x_5^0'=x_5^post4, __disjvr_1^0'=__disjvr_1^post4, z_7^0'=z_7^post4, (tmp_8^0-tmp_8^post4 == 0 /\ -__disjvr_2^post4+__disjvr_2^0 == 0 /\ Result_4^0-Result_4^post4 == 0 /\ -__disjvr_1^post4+__disjvr_1^0 == 0 /\ __disjvr_0^0-__disjvr_0^post4 == 0 /\ -1-y_6^0+y_6^post4 == 0 /\ x_5^0-x_5^post4 == 0 /\ -z_7^post4+z_7^0 == 0), cost: 1 New rule: l6 -> l4 : y_6^0'=1+y_6^0, TRUE, cost: 1 Applied preprocessing Original rule: l4 -> l2 : tmp_8^0'=tmp_8^post5, __disjvr_0^0'=__disjvr_0^post5, y_6^0'=y_6^post5, __disjvr_2^0'=__disjvr_2^post5, Result_4^0'=Result_4^post5, x_5^0'=x_5^post5, __disjvr_1^0'=__disjvr_1^post5, z_7^0'=z_7^post5, (-__disjvr_1^post5+__disjvr_1^0 == 0 /\ -z_7^post5+z_7^0 == 0 /\ tmp_8^0-tmp_8^post5 == 0 /\ -Result_4^post5+Result_4^0 == 0 /\ -x_5^post5+x_5^0 == 0 /\ __disjvr_2^0-__disjvr_2^post5 == 0 /\ -y_6^post5+y_6^0 == 0 /\ __disjvr_0^0-__disjvr_0^post5 == 0), cost: 1 New rule: l4 -> l2 : TRUE, cost: 1 Applied preprocessing Original rule: l2 -> l1 : tmp_8^0'=tmp_8^post6, __disjvr_0^0'=__disjvr_0^post6, y_6^0'=y_6^post6, __disjvr_2^0'=__disjvr_2^post6, Result_4^0'=Result_4^post6, x_5^0'=x_5^post6, __disjvr_1^0'=__disjvr_1^post6, z_7^0'=z_7^post6, (-__disjvr_2^post6+__disjvr_2^0 == 0 /\ -1-x_5^0+x_5^post6 == 0 /\ y_6^0-y_6^post6 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ tmp_8^0-tmp_8^post6 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0 /\ -y_6^0+z_7^0 <= 0 /\ -z_7^post6+z_7^0 == 0 /\ Result_4^0-Result_4^post6 == 0), cost: 1 New rule: l2 -> l1 : x_5^0'=1+x_5^0, -y_6^0+z_7^0 <= 0, cost: 1 Applied preprocessing Original rule: l1 -> l7 : tmp_8^0'=tmp_8^post7, __disjvr_0^0'=__disjvr_0^post7, y_6^0'=y_6^post7, __disjvr_2^0'=__disjvr_2^post7, Result_4^0'=Result_4^post7, x_5^0'=x_5^post7, __disjvr_1^0'=__disjvr_1^post7, z_7^0'=z_7^post7, (1-y_6^0+x_5^0 <= 0 /\ tmp_8^0-tmp_8^post7 == 0 /\ Result_4^0-Result_4^post7 == 0 /\ -z_7^post7+z_7^0 == 0 /\ __disjvr_1^0-__disjvr_1^post7 == 0 /\ -y_6^post7+y_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post7 == 0 /\ -x_5^post7+x_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post7 == 0), cost: 1 New rule: l1 -> l7 : 1-y_6^0+x_5^0 <= 0, cost: 1 Applied preprocessing Original rule: l7 -> l3 : tmp_8^0'=tmp_8^post9, __disjvr_0^0'=__disjvr_0^post9, y_6^0'=y_6^post9, __disjvr_2^0'=__disjvr_2^post9, Result_4^0'=Result_4^post9, x_5^0'=x_5^post9, __disjvr_1^0'=__disjvr_1^post9, z_7^0'=z_7^post9, (0 == 0 /\ -y_6^post9+y_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post9 == 0 /\ __disjvr_1^0-__disjvr_1^post9 == 0 /\ __disjvr_0^0-__disjvr_0^post9 == 0 /\ -z_7^post9+z_7^0 == 0 /\ tmp_8^post9 <= 0 /\ -tmp_8^post9 <= 0 /\ -x_5^post9+x_5^0 == 0 /\ 1+y_6^0-z_7^0 <= 0 /\ -Result_4^post9+Result_4^0 == 0), cost: 1 New rule: l7 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 Applied preprocessing Original rule: l7 -> l9 : tmp_8^0'=tmp_8^post10, __disjvr_0^0'=__disjvr_0^post10, y_6^0'=y_6^post10, __disjvr_2^0'=__disjvr_2^post10, Result_4^0'=Result_4^post10, x_5^0'=x_5^post10, __disjvr_1^0'=__disjvr_1^post10, z_7^0'=z_7^post10, (0 == 0 /\ y_6^0-y_6^post10 == 0 /\ -__disjvr_1^post10+__disjvr_1^0 == 0 /\ -z_7^post10+z_7^0 == 0 /\ x_5^0-x_5^post10 == 0 /\ -__disjvr_2^post10+__disjvr_2^0 == 0 /\ -Result_4^post10+Result_4^0 == 0 /\ 1+y_6^0-z_7^0 <= 0 /\ __disjvr_0^0-__disjvr_0^post10 == 0), cost: 1 New rule: l7 -> l9 : tmp_8^0'=tmp_8^post10, 1+y_6^0-z_7^0 <= 0, cost: 1 Applied preprocessing Original rule: l9 -> l10 : tmp_8^0'=tmp_8^post11, __disjvr_0^0'=__disjvr_0^post11, y_6^0'=y_6^post11, __disjvr_2^0'=__disjvr_2^post11, Result_4^0'=Result_4^post11, x_5^0'=x_5^post11, __disjvr_1^0'=__disjvr_1^post11, z_7^0'=z_7^post11, (tmp_8^0-tmp_8^post11 == 0 /\ Result_4^0-Result_4^post11 == 0 /\ -y_6^post11+y_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post11 == 0 /\ __disjvr_0^0-__disjvr_0^post11 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ -z_7^post11+z_7^0 == 0 /\ -x_5^post11+x_5^0 == 0 /\ __disjvr_1^post11-__disjvr_1^0 == 0), cost: 1 New rule: l9 -> l10 : 0 == 0, cost: 1 Applied preprocessing Original rule: l10 -> l2 : tmp_8^0'=tmp_8^post12, __disjvr_0^0'=__disjvr_0^post12, y_6^0'=y_6^post12, __disjvr_2^0'=__disjvr_2^post12, Result_4^0'=Result_4^post12, x_5^0'=x_5^post12, __disjvr_1^0'=__disjvr_1^post12, z_7^0'=z_7^post12, (__disjvr_0^0-__disjvr_0^post12 == 0 /\ -Result_4^post12+Result_4^0 == 0 /\ -z_7^post12+z_7^0 == 0 /\ -x_5^post12+x_5^0 == 0 /\ -tmp_8^post12+tmp_8^0 == 0 /\ -1+y_6^post12-y_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post12 == 0 /\ -__disjvr_1^post12+__disjvr_1^0 == 0), cost: 1 New rule: l10 -> l2 : y_6^0'=1+y_6^0, TRUE, cost: 1 Applied preprocessing Original rule: l7 -> l1 : tmp_8^0'=tmp_8^post13, __disjvr_0^0'=__disjvr_0^post13, y_6^0'=y_6^post13, __disjvr_2^0'=__disjvr_2^post13, Result_4^0'=Result_4^post13, x_5^0'=x_5^post13, __disjvr_1^0'=__disjvr_1^post13, z_7^0'=z_7^post13, (Result_4^0-Result_4^post13 == 0 /\ tmp_8^0-tmp_8^post13 == 0 /\ -__disjvr_1^post13+__disjvr_1^0 == 0 /\ -__disjvr_2^post13+__disjvr_2^0 == 0 /\ y_6^0-y_6^post13 == 0 /\ -1+x_5^post13-x_5^0 == 0 /\ -y_6^0+z_7^0 <= 0 /\ -__disjvr_0^post13+__disjvr_0^0 == 0 /\ -z_7^post13+z_7^0 == 0), cost: 1 New rule: l7 -> l1 : x_5^0'=1+x_5^0, -y_6^0+z_7^0 <= 0, cost: 1 Applied preprocessing Original rule: l3 -> l11 : tmp_8^0'=tmp_8^post14, __disjvr_0^0'=__disjvr_0^post14, y_6^0'=y_6^post14, __disjvr_2^0'=__disjvr_2^post14, Result_4^0'=Result_4^post14, x_5^0'=x_5^post14, __disjvr_1^0'=__disjvr_1^post14, z_7^0'=z_7^post14, (0 == 0 /\ tmp_8^post14 <= 0 /\ __disjvr_0^0-__disjvr_0^post14 == 0 /\ -y_6^post14+y_6^0 == 0 /\ -z_7^post14+z_7^0 == 0 /\ -__disjvr_1^post14+__disjvr_1^0 == 0 /\ -tmp_8^post14 <= 0 /\ __disjvr_2^0-__disjvr_2^post14 == 0 /\ -x_5^post14+x_5^0 == 0 /\ 1+y_6^0-z_7^0 <= 0 /\ -Result_4^post14+Result_4^0 == 0), cost: 1 New rule: l3 -> l11 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 Applied preprocessing Original rule: l11 -> l3 : tmp_8^0'=tmp_8^post15, __disjvr_0^0'=__disjvr_0^post15, y_6^0'=y_6^post15, __disjvr_2^0'=__disjvr_2^post15, Result_4^0'=Result_4^post15, x_5^0'=x_5^post15, __disjvr_1^0'=__disjvr_1^post15, z_7^0'=z_7^post15, (-__disjvr_0^post15+__disjvr_0^0 == 0 /\ -__disjvr_1^post15+__disjvr_1^0 == 0 /\ -z_7^post15+z_7^0 == 0 /\ y_6^0-y_6^post15 == 0 /\ tmp_8^0-tmp_8^post15 == 0 /\ __disjvr_2^0-__disjvr_2^post15 == 0 /\ Result_4^0-Result_4^post15 == 0 /\ x_5^0-x_5^post15 == 0), cost: 1 New rule: l11 -> l3 : TRUE, cost: 1 Applied preprocessing Original rule: l3 -> l12 : tmp_8^0'=tmp_8^post16, __disjvr_0^0'=__disjvr_0^post16, y_6^0'=y_6^post16, __disjvr_2^0'=__disjvr_2^post16, Result_4^0'=Result_4^post16, x_5^0'=x_5^post16, __disjvr_1^0'=__disjvr_1^post16, z_7^0'=z_7^post16, (0 == 0 /\ __disjvr_0^0-__disjvr_0^post16 == 0 /\ -x_5^post16+x_5^0 == 0 /\ -Result_4^post16+Result_4^0 == 0 /\ -__disjvr_1^post16+__disjvr_1^0 == 0 /\ __disjvr_2^0-__disjvr_2^post16 == 0 /\ -z_7^post16+z_7^0 == 0 /\ -y_6^post16+y_6^0 == 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 1 New rule: l3 -> l12 : tmp_8^0'=tmp_8^post16, 1+y_6^0-z_7^0 <= 0, cost: 1 Applied preprocessing Original rule: l12 -> l13 : tmp_8^0'=tmp_8^post17, __disjvr_0^0'=__disjvr_0^post17, y_6^0'=y_6^post17, __disjvr_2^0'=__disjvr_2^post17, Result_4^0'=Result_4^post17, x_5^0'=x_5^post17, __disjvr_1^0'=__disjvr_1^post17, z_7^0'=z_7^post17, (tmp_8^0-tmp_8^post17 == 0 /\ -__disjvr_2^post17+__disjvr_2^0 == 0 /\ y_6^0-y_6^post17 == 0 /\ -z_7^post17+z_7^0 == 0 /\ __disjvr_2^post17-__disjvr_2^0 == 0 /\ -x_5^post17+x_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post17 == 0 /\ Result_4^0-Result_4^post17 == 0 /\ -__disjvr_1^post17+__disjvr_1^0 == 0), cost: 1 New rule: l12 -> l13 : 0 == 0, cost: 1 Applied preprocessing Original rule: l13 -> l2 : tmp_8^0'=tmp_8^post18, __disjvr_0^0'=__disjvr_0^post18, y_6^0'=y_6^post18, __disjvr_2^0'=__disjvr_2^post18, Result_4^0'=Result_4^post18, x_5^0'=x_5^post18, __disjvr_1^0'=__disjvr_1^post18, z_7^0'=z_7^post18, (-z_7^post18+z_7^0 == 0 /\ __disjvr_0^0-__disjvr_0^post18 == 0 /\ -__disjvr_1^post18+__disjvr_1^0 == 0 /\ tmp_8^0-tmp_8^post18 == 0 /\ -Result_4^post18+Result_4^0 == 0 /\ -x_5^post18+x_5^0 == 0 /\ -1+y_6^post18-y_6^0 == 0 /\ __disjvr_2^0-__disjvr_2^post18 == 0), cost: 1 New rule: l13 -> l2 : y_6^0'=1+y_6^0, TRUE, cost: 1 Applied preprocessing Original rule: l14 -> l0 : tmp_8^0'=tmp_8^post19, __disjvr_0^0'=__disjvr_0^post19, y_6^0'=y_6^post19, __disjvr_2^0'=__disjvr_2^post19, Result_4^0'=Result_4^post19, x_5^0'=x_5^post19, __disjvr_1^0'=__disjvr_1^post19, z_7^0'=z_7^post19, (y_6^0-y_6^post19 == 0 /\ tmp_8^0-tmp_8^post19 == 0 /\ -__disjvr_2^post19+__disjvr_2^0 == 0 /\ -z_7^post19+z_7^0 == 0 /\ x_5^0-x_5^post19 == 0 /\ -__disjvr_0^post19+__disjvr_0^0 == 0 /\ -__disjvr_1^post19+__disjvr_1^0 == 0 /\ -Result_4^post19+Result_4^0 == 0), cost: 1 New rule: l14 -> l0 : TRUE, cost: 1 Simplified rules Start location: l14 20: l0 -> l1 : TRUE, cost: 1 27: l1 -> l7 : 1-y_6^0+x_5^0 <= 0, cost: 1 21: l2 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 22: l2 -> l5 : tmp_8^0'=tmp_8^post2, 1+y_6^0-z_7^0 <= 0, cost: 1 26: l2 -> l1 : x_5^0'=1+x_5^0, -y_6^0+z_7^0 <= 0, cost: 1 33: l3 -> l11 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 35: l3 -> l12 : tmp_8^0'=tmp_8^post16, 1+y_6^0-z_7^0 <= 0, cost: 1 23: l5 -> l6 : 0 == 0, cost: 1 24: l6 -> l4 : y_6^0'=1+y_6^0, TRUE, cost: 1 25: l4 -> l2 : TRUE, cost: 1 28: l7 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 29: l7 -> l9 : tmp_8^0'=tmp_8^post10, 1+y_6^0-z_7^0 <= 0, cost: 1 32: l7 -> l1 : x_5^0'=1+x_5^0, -y_6^0+z_7^0 <= 0, cost: 1 30: l9 -> l10 : 0 == 0, cost: 1 31: l10 -> l2 : y_6^0'=1+y_6^0, TRUE, cost: 1 34: l11 -> l3 : TRUE, cost: 1 36: l12 -> l13 : 0 == 0, cost: 1 37: l13 -> l2 : y_6^0'=1+y_6^0, TRUE, cost: 1 38: l14 -> l0 : TRUE, cost: 1 Eliminating location l0 by chaining: Applied chaining First rule: l14 -> l0 : TRUE, cost: 1 Second rule: l0 -> l1 : TRUE, cost: 1 New rule: l14 -> l1 : TRUE, cost: 2 Applied deletion Removed the following rules: 20 38 Eliminating location l9 by chaining: Applied chaining First rule: l7 -> l9 : tmp_8^0'=tmp_8^post10, 1+y_6^0-z_7^0 <= 0, cost: 1 Second rule: l9 -> l10 : 0 == 0, cost: 1 New rule: l7 -> l10 : tmp_8^0'=tmp_8^post10, (0 == 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 2 Applied simplification Original rule: l7 -> l10 : tmp_8^0'=tmp_8^post10, (0 == 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 2 New rule: l7 -> l10 : tmp_8^0'=tmp_8^post10, 1+y_6^0-z_7^0 <= 0, cost: 2 Applied deletion Removed the following rules: 29 30 Eliminating location l10 by chaining: Applied chaining First rule: l7 -> l10 : tmp_8^0'=tmp_8^post10, 1+y_6^0-z_7^0 <= 0, cost: 2 Second rule: l10 -> l2 : y_6^0'=1+y_6^0, TRUE, cost: 1 New rule: l7 -> l2 : tmp_8^0'=tmp_8^post10, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 3 Applied deletion Removed the following rules: 31 40 Eliminating location l5 by chaining: Applied chaining First rule: l2 -> l5 : tmp_8^0'=tmp_8^post2, 1+y_6^0-z_7^0 <= 0, cost: 1 Second rule: l5 -> l6 : 0 == 0, cost: 1 New rule: l2 -> l6 : tmp_8^0'=tmp_8^post2, (0 == 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 2 Applied simplification Original rule: l2 -> l6 : tmp_8^0'=tmp_8^post2, (0 == 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 2 New rule: l2 -> l6 : tmp_8^0'=tmp_8^post2, 1+y_6^0-z_7^0 <= 0, cost: 2 Applied deletion Removed the following rules: 22 23 Eliminating location l6 by chaining: Applied chaining First rule: l2 -> l6 : tmp_8^0'=tmp_8^post2, 1+y_6^0-z_7^0 <= 0, cost: 2 Second rule: l6 -> l4 : y_6^0'=1+y_6^0, TRUE, cost: 1 New rule: l2 -> l4 : tmp_8^0'=tmp_8^post2, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 3 Applied deletion Removed the following rules: 24 42 Eliminating location l4 by chaining: Applied chaining First rule: l2 -> l4 : tmp_8^0'=tmp_8^post2, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 3 Second rule: l4 -> l2 : TRUE, cost: 1 New rule: l2 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 4 Applied deletion Removed the following rules: 25 43 Eliminating location l11 by chaining: Applied chaining First rule: l3 -> l11 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 Second rule: l11 -> l3 : TRUE, cost: 1 New rule: l3 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 2 Applied deletion Removed the following rules: 33 34 Eliminating location l12 by chaining: Applied chaining First rule: l3 -> l12 : tmp_8^0'=tmp_8^post16, 1+y_6^0-z_7^0 <= 0, cost: 1 Second rule: l12 -> l13 : 0 == 0, cost: 1 New rule: l3 -> l13 : tmp_8^0'=tmp_8^post16, (0 == 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 2 Applied simplification Original rule: l3 -> l13 : tmp_8^0'=tmp_8^post16, (0 == 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 2 New rule: l3 -> l13 : tmp_8^0'=tmp_8^post16, 1+y_6^0-z_7^0 <= 0, cost: 2 Applied deletion Removed the following rules: 35 36 Eliminating location l13 by chaining: Applied chaining First rule: l3 -> l13 : tmp_8^0'=tmp_8^post16, 1+y_6^0-z_7^0 <= 0, cost: 2 Second rule: l13 -> l2 : y_6^0'=1+y_6^0, TRUE, cost: 1 New rule: l3 -> l2 : tmp_8^0'=tmp_8^post16, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 3 Applied deletion Removed the following rules: 37 46 Eliminated locations on linear paths Start location: l14 27: l1 -> l7 : 1-y_6^0+x_5^0 <= 0, cost: 1 21: l2 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 26: l2 -> l1 : x_5^0'=1+x_5^0, -y_6^0+z_7^0 <= 0, cost: 1 44: l2 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 4 45: l3 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 2 47: l3 -> l2 : tmp_8^0'=tmp_8^post16, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 3 28: l7 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 32: l7 -> l1 : x_5^0'=1+x_5^0, -y_6^0+z_7^0 <= 0, cost: 1 41: l7 -> l2 : tmp_8^0'=tmp_8^post10, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 3 39: l14 -> l1 : TRUE, cost: 2 Applied acceleration Original rule: l2 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 4 New rule: l2 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=y_6^0+n, (-1+n >= 0 /\ -y_6^0-n+z_7^0 >= 0), cost: 4*n Sub-proof via acceration calculus written to file:///tmp/tmpnam_BiFOnN.txt Applied instantiation Original rule: l2 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=y_6^0+n, (-1+n >= 0 /\ -y_6^0-n+z_7^0 >= 0), cost: 4*n New rule: l2 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, (0 >= 0 /\ -1-y_6^0+z_7^0 >= 0), cost: -4*y_6^0+4*z_7^0 Applied simplification Original rule: l2 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, (0 >= 0 /\ -1-y_6^0+z_7^0 >= 0), cost: -4*y_6^0+4*z_7^0 New rule: l2 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, -1-y_6^0+z_7^0 >= 0, cost: -4*y_6^0+4*z_7^0 Applied deletion Removed the following rules: 44 Applied nonterm Original rule: l3 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 2 New rule: l3 -> [16] : (-1-y_6^0+z_7^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_hgJeCf.txt Applied deletion Removed the following rules: 45 Accelerated simple loops Start location: l14 27: l1 -> l7 : 1-y_6^0+x_5^0 <= 0, cost: 1 21: l2 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 26: l2 -> l1 : x_5^0'=1+x_5^0, -y_6^0+z_7^0 <= 0, cost: 1 49: l2 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, -1-y_6^0+z_7^0 >= 0, cost: -4*y_6^0+4*z_7^0 47: l3 -> l2 : tmp_8^0'=tmp_8^post16, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 3 50: l3 -> [16] : (-1-y_6^0+z_7^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM 28: l7 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 32: l7 -> l1 : x_5^0'=1+x_5^0, -y_6^0+z_7^0 <= 0, cost: 1 41: l7 -> l2 : tmp_8^0'=tmp_8^post10, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 3 39: l14 -> l1 : TRUE, cost: 2 Applied chaining First rule: l7 -> l2 : tmp_8^0'=tmp_8^post10, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 3 Second rule: l2 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, -1-y_6^0+z_7^0 >= 0, cost: -4*y_6^0+4*z_7^0 New rule: l7 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, -2-y_6^0+z_7^0 >= 0, cost: -1-4*y_6^0+4*z_7^0 Applied chaining First rule: l3 -> l2 : tmp_8^0'=tmp_8^post16, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 3 Second rule: l2 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, -1-y_6^0+z_7^0 >= 0, cost: -4*y_6^0+4*z_7^0 New rule: l3 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, -2-y_6^0+z_7^0 >= 0, cost: -1-4*y_6^0+4*z_7^0 Applied deletion Removed the following rules: 49 Applied chaining First rule: l2 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 Second rule: l3 -> [16] : (-1-y_6^0+z_7^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l2 -> [16] : 1+y_6^0-z_7^0 <= 0, cost: NONTERM Applied chaining First rule: l7 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 Second rule: l3 -> [16] : (-1-y_6^0+z_7^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM New rule: l7 -> [16] : 1+y_6^0-z_7^0 <= 0, cost: NONTERM Applied deletion Removed the following rules: 50 Chained accelerated rules with incoming rules Start location: l14 27: l1 -> l7 : 1-y_6^0+x_5^0 <= 0, cost: 1 21: l2 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 26: l2 -> l1 : x_5^0'=1+x_5^0, -y_6^0+z_7^0 <= 0, cost: 1 53: l2 -> [16] : 1+y_6^0-z_7^0 <= 0, cost: NONTERM 47: l3 -> l2 : tmp_8^0'=tmp_8^post16, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 3 52: l3 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, -2-y_6^0+z_7^0 >= 0, cost: -1-4*y_6^0+4*z_7^0 28: l7 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 32: l7 -> l1 : x_5^0'=1+x_5^0, -y_6^0+z_7^0 <= 0, cost: 1 41: l7 -> l2 : tmp_8^0'=tmp_8^post10, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 3 51: l7 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, -2-y_6^0+z_7^0 >= 0, cost: -1-4*y_6^0+4*z_7^0 54: l7 -> [16] : 1+y_6^0-z_7^0 <= 0, cost: NONTERM 39: l14 -> l1 : TRUE, cost: 2 Eliminating location l7 by chaining: Applied chaining First rule: l1 -> l7 : 1-y_6^0+x_5^0 <= 0, cost: 1 Second rule: l7 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 New rule: l1 -> l3 : tmp_8^0'=0, (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 2 Applied chaining First rule: l1 -> l7 : 1-y_6^0+x_5^0 <= 0, cost: 1 Second rule: l7 -> l1 : x_5^0'=1+x_5^0, -y_6^0+z_7^0 <= 0, cost: 1 New rule: l1 -> l1 : x_5^0'=1+x_5^0, (1-y_6^0+x_5^0 <= 0 /\ -y_6^0+z_7^0 <= 0), cost: 2 Applied chaining First rule: l1 -> l7 : 1-y_6^0+x_5^0 <= 0, cost: 1 Second rule: l7 -> l2 : tmp_8^0'=tmp_8^post10, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 3 New rule: l1 -> l2 : tmp_8^0'=tmp_8^post10, y_6^0'=1+y_6^0, (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 4 Applied chaining First rule: l1 -> l7 : 1-y_6^0+x_5^0 <= 0, cost: 1 Second rule: l7 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, -2-y_6^0+z_7^0 >= 0, cost: -1-4*y_6^0+4*z_7^0 New rule: l1 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, (1-y_6^0+x_5^0 <= 0 /\ -2-y_6^0+z_7^0 >= 0), cost: -4*y_6^0+4*z_7^0 Applied chaining First rule: l1 -> l7 : 1-y_6^0+x_5^0 <= 0, cost: 1 Second rule: l7 -> [16] : 1+y_6^0-z_7^0 <= 0, cost: NONTERM New rule: l1 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: NONTERM Applied deletion Removed the following rules: 27 28 32 41 51 54 Eliminated locations on tree-shaped paths Start location: l14 55: l1 -> l3 : tmp_8^0'=0, (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 2 56: l1 -> l1 : x_5^0'=1+x_5^0, (1-y_6^0+x_5^0 <= 0 /\ -y_6^0+z_7^0 <= 0), cost: 2 57: l1 -> l2 : tmp_8^0'=tmp_8^post10, y_6^0'=1+y_6^0, (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 4 58: l1 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, (1-y_6^0+x_5^0 <= 0 /\ -2-y_6^0+z_7^0 >= 0), cost: -4*y_6^0+4*z_7^0 59: l1 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: NONTERM 21: l2 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 26: l2 -> l1 : x_5^0'=1+x_5^0, -y_6^0+z_7^0 <= 0, cost: 1 53: l2 -> [16] : 1+y_6^0-z_7^0 <= 0, cost: NONTERM 47: l3 -> l2 : tmp_8^0'=tmp_8^post16, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 3 52: l3 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, -2-y_6^0+z_7^0 >= 0, cost: -1-4*y_6^0+4*z_7^0 39: l14 -> l1 : TRUE, cost: 2 Applied acceleration Original rule: l1 -> l1 : x_5^0'=1+x_5^0, (1-y_6^0+x_5^0 <= 0 /\ -y_6^0+z_7^0 <= 0), cost: 2 New rule: l1 -> l1 : x_5^0'=n1+x_5^0, (n1 >= 0 /\ -n1+y_6^0-x_5^0 >= 0 /\ y_6^0-z_7^0 >= 0), cost: 2*n1 Sub-proof via acceration calculus written to file:///tmp/tmpnam_ekCHbK.txt Applied instantiation Original rule: l1 -> l1 : x_5^0'=n1+x_5^0, (n1 >= 0 /\ -n1+y_6^0-x_5^0 >= 0 /\ y_6^0-z_7^0 >= 0), cost: 2*n1 New rule: l1 -> l1 : x_5^0'=y_6^0, (0 >= 0 /\ y_6^0-x_5^0 >= 0 /\ y_6^0-z_7^0 >= 0), cost: 2*y_6^0-2*x_5^0 Applied simplification Original rule: l1 -> l1 : x_5^0'=y_6^0, (0 >= 0 /\ y_6^0-x_5^0 >= 0 /\ y_6^0-z_7^0 >= 0), cost: 2*y_6^0-2*x_5^0 New rule: l1 -> l1 : x_5^0'=y_6^0, (y_6^0-x_5^0 >= 0 /\ y_6^0-z_7^0 >= 0), cost: 2*y_6^0-2*x_5^0 Applied deletion Removed the following rules: 56 Accelerated simple loops Start location: l14 55: l1 -> l3 : tmp_8^0'=0, (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 2 57: l1 -> l2 : tmp_8^0'=tmp_8^post10, y_6^0'=1+y_6^0, (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 4 58: l1 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, (1-y_6^0+x_5^0 <= 0 /\ -2-y_6^0+z_7^0 >= 0), cost: -4*y_6^0+4*z_7^0 59: l1 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: NONTERM 61: l1 -> l1 : x_5^0'=y_6^0, (y_6^0-x_5^0 >= 0 /\ y_6^0-z_7^0 >= 0), cost: 2*y_6^0-2*x_5^0 21: l2 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 26: l2 -> l1 : x_5^0'=1+x_5^0, -y_6^0+z_7^0 <= 0, cost: 1 53: l2 -> [16] : 1+y_6^0-z_7^0 <= 0, cost: NONTERM 47: l3 -> l2 : tmp_8^0'=tmp_8^post16, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 3 52: l3 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, -2-y_6^0+z_7^0 >= 0, cost: -1-4*y_6^0+4*z_7^0 39: l14 -> l1 : TRUE, cost: 2 Applied chaining First rule: l2 -> l1 : x_5^0'=1+x_5^0, -y_6^0+z_7^0 <= 0, cost: 1 Second rule: l1 -> l1 : x_5^0'=y_6^0, (y_6^0-x_5^0 >= 0 /\ y_6^0-z_7^0 >= 0), cost: 2*y_6^0-2*x_5^0 New rule: l2 -> l1 : x_5^0'=y_6^0, (-1+y_6^0-x_5^0 >= 0 /\ y_6^0-z_7^0 >= 0), cost: -1+2*y_6^0-2*x_5^0 Applied chaining First rule: l14 -> l1 : TRUE, cost: 2 Second rule: l1 -> l1 : x_5^0'=y_6^0, (y_6^0-x_5^0 >= 0 /\ y_6^0-z_7^0 >= 0), cost: 2*y_6^0-2*x_5^0 New rule: l14 -> l1 : x_5^0'=y_6^0, (y_6^0-x_5^0 >= 0 /\ y_6^0-z_7^0 >= 0), cost: 2+2*y_6^0-2*x_5^0 Applied deletion Removed the following rules: 61 Chained accelerated rules with incoming rules Start location: l14 55: l1 -> l3 : tmp_8^0'=0, (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 2 57: l1 -> l2 : tmp_8^0'=tmp_8^post10, y_6^0'=1+y_6^0, (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 4 58: l1 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, (1-y_6^0+x_5^0 <= 0 /\ -2-y_6^0+z_7^0 >= 0), cost: -4*y_6^0+4*z_7^0 59: l1 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: NONTERM 21: l2 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 26: l2 -> l1 : x_5^0'=1+x_5^0, -y_6^0+z_7^0 <= 0, cost: 1 53: l2 -> [16] : 1+y_6^0-z_7^0 <= 0, cost: NONTERM 62: l2 -> l1 : x_5^0'=y_6^0, (-1+y_6^0-x_5^0 >= 0 /\ y_6^0-z_7^0 >= 0), cost: -1+2*y_6^0-2*x_5^0 47: l3 -> l2 : tmp_8^0'=tmp_8^post16, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 3 52: l3 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, -2-y_6^0+z_7^0 >= 0, cost: -1-4*y_6^0+4*z_7^0 39: l14 -> l1 : TRUE, cost: 2 63: l14 -> l1 : x_5^0'=y_6^0, (y_6^0-x_5^0 >= 0 /\ y_6^0-z_7^0 >= 0), cost: 2+2*y_6^0-2*x_5^0 Eliminated location l1 Start location: l14 21: l2 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 53: l2 -> [16] : 1+y_6^0-z_7^0 <= 0, cost: NONTERM 68: l2 -> [18] : (-1+y_6^0-x_5^0 >= 0 /\ y_6^0-z_7^0 >= 0), cost: -1+2*y_6^0-2*x_5^0 47: l3 -> l2 : tmp_8^0'=tmp_8^post16, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 3 52: l3 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, -2-y_6^0+z_7^0 >= 0, cost: -1-4*y_6^0+4*z_7^0 64: l14 -> l3 : tmp_8^0'=0, (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 4 65: l14 -> l2 : tmp_8^0'=tmp_8^post10, y_6^0'=1+y_6^0, (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 6 66: l14 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, (1-y_6^0+x_5^0 <= 0 /\ -2-y_6^0+z_7^0 >= 0), cost: 2-4*y_6^0+4*z_7^0 67: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: NONTERM 69: l14 -> [18] : (y_6^0-x_5^0 >= 0 /\ y_6^0-z_7^0 >= 0), cost: 2+2*y_6^0-2*x_5^0 Applied pruning (of leafs and parallel rules): Start location: l14 21: l2 -> l3 : tmp_8^0'=0, 1+y_6^0-z_7^0 <= 0, cost: 1 53: l2 -> [16] : 1+y_6^0-z_7^0 <= 0, cost: NONTERM 47: l3 -> l2 : tmp_8^0'=tmp_8^post16, y_6^0'=1+y_6^0, 1+y_6^0-z_7^0 <= 0, cost: 3 52: l3 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, -2-y_6^0+z_7^0 >= 0, cost: -1-4*y_6^0+4*z_7^0 64: l14 -> l3 : tmp_8^0'=0, (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 4 65: l14 -> l2 : tmp_8^0'=tmp_8^post10, y_6^0'=1+y_6^0, (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 6 66: l14 -> l2 : tmp_8^0'=tmp_8^post2, y_6^0'=z_7^0, (1-y_6^0+x_5^0 <= 0 /\ -2-y_6^0+z_7^0 >= 0), cost: 2-4*y_6^0+4*z_7^0 67: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: NONTERM Eliminated location l2 Start location: l14 70: l3 -> l3 : tmp_8^0'=0, y_6^0'=1+y_6^0, 2+y_6^0-z_7^0 <= 0, cost: 4 71: l3 -> [16] : 2+y_6^0-z_7^0 <= 0, cost: NONTERM 74: l3 -> [19] : -2-y_6^0+z_7^0 >= 0, cost: -1-4*y_6^0+4*z_7^0 64: l14 -> l3 : tmp_8^0'=0, (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 4 67: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: NONTERM 72: l14 -> l3 : tmp_8^0'=0, y_6^0'=1+y_6^0, (1-y_6^0+x_5^0 <= 0 /\ 2+y_6^0-z_7^0 <= 0), cost: 7 73: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 2+y_6^0-z_7^0 <= 0), cost: NONTERM 75: l14 -> [19] : (1-y_6^0+x_5^0 <= 0 /\ -2-y_6^0+z_7^0 >= 0), cost: 2-4*y_6^0+4*z_7^0 Applied pruning (of leafs and parallel rules): Start location: l14 70: l3 -> l3 : tmp_8^0'=0, y_6^0'=1+y_6^0, 2+y_6^0-z_7^0 <= 0, cost: 4 71: l3 -> [16] : 2+y_6^0-z_7^0 <= 0, cost: NONTERM 64: l14 -> l3 : tmp_8^0'=0, (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 4 67: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: NONTERM 72: l14 -> l3 : tmp_8^0'=0, y_6^0'=1+y_6^0, (1-y_6^0+x_5^0 <= 0 /\ 2+y_6^0-z_7^0 <= 0), cost: 7 73: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 2+y_6^0-z_7^0 <= 0), cost: NONTERM Applied acceleration Original rule: l3 -> l3 : tmp_8^0'=0, y_6^0'=1+y_6^0, 2+y_6^0-z_7^0 <= 0, cost: 4 New rule: l3 -> l3 : tmp_8^0'=0, y_6^0'=y_6^0+n2, (-1+n2 >= 0 /\ -1-y_6^0-n2+z_7^0 >= 0), cost: 4*n2 Sub-proof via acceration calculus written to file:///tmp/tmpnam_fOlbAi.txt Applied instantiation Original rule: l3 -> l3 : tmp_8^0'=0, y_6^0'=y_6^0+n2, (-1+n2 >= 0 /\ -1-y_6^0-n2+z_7^0 >= 0), cost: 4*n2 New rule: l3 -> l3 : tmp_8^0'=0, y_6^0'=-1+z_7^0, (0 >= 0 /\ -2-y_6^0+z_7^0 >= 0), cost: -4-4*y_6^0+4*z_7^0 Applied simplification Original rule: l3 -> l3 : tmp_8^0'=0, y_6^0'=-1+z_7^0, (0 >= 0 /\ -2-y_6^0+z_7^0 >= 0), cost: -4-4*y_6^0+4*z_7^0 New rule: l3 -> l3 : tmp_8^0'=0, y_6^0'=-1+z_7^0, -2-y_6^0+z_7^0 >= 0, cost: -4-4*y_6^0+4*z_7^0 Applied deletion Removed the following rules: 70 Accelerated simple loops Start location: l14 71: l3 -> [16] : 2+y_6^0-z_7^0 <= 0, cost: NONTERM 77: l3 -> l3 : tmp_8^0'=0, y_6^0'=-1+z_7^0, -2-y_6^0+z_7^0 >= 0, cost: -4-4*y_6^0+4*z_7^0 64: l14 -> l3 : tmp_8^0'=0, (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 4 67: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: NONTERM 72: l14 -> l3 : tmp_8^0'=0, y_6^0'=1+y_6^0, (1-y_6^0+x_5^0 <= 0 /\ 2+y_6^0-z_7^0 <= 0), cost: 7 73: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 2+y_6^0-z_7^0 <= 0), cost: NONTERM Applied chaining First rule: l14 -> l3 : tmp_8^0'=0, (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 4 Second rule: l3 -> l3 : tmp_8^0'=0, y_6^0'=-1+z_7^0, -2-y_6^0+z_7^0 >= 0, cost: -4-4*y_6^0+4*z_7^0 New rule: l14 -> l3 : tmp_8^0'=0, y_6^0'=-1+z_7^0, (1-y_6^0+x_5^0 <= 0 /\ -2-y_6^0+z_7^0 >= 0), cost: -4*y_6^0+4*z_7^0 Applied chaining First rule: l14 -> l3 : tmp_8^0'=0, y_6^0'=1+y_6^0, (1-y_6^0+x_5^0 <= 0 /\ 2+y_6^0-z_7^0 <= 0), cost: 7 Second rule: l3 -> l3 : tmp_8^0'=0, y_6^0'=-1+z_7^0, -2-y_6^0+z_7^0 >= 0, cost: -4-4*y_6^0+4*z_7^0 New rule: l14 -> l3 : tmp_8^0'=0, y_6^0'=-1+z_7^0, (1-y_6^0+x_5^0 <= 0 /\ -3-y_6^0+z_7^0 >= 0), cost: -1-4*y_6^0+4*z_7^0 Applied deletion Removed the following rules: 77 Chained accelerated rules with incoming rules Start location: l14 71: l3 -> [16] : 2+y_6^0-z_7^0 <= 0, cost: NONTERM 64: l14 -> l3 : tmp_8^0'=0, (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 4 67: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: NONTERM 72: l14 -> l3 : tmp_8^0'=0, y_6^0'=1+y_6^0, (1-y_6^0+x_5^0 <= 0 /\ 2+y_6^0-z_7^0 <= 0), cost: 7 73: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 2+y_6^0-z_7^0 <= 0), cost: NONTERM 78: l14 -> l3 : tmp_8^0'=0, y_6^0'=-1+z_7^0, (1-y_6^0+x_5^0 <= 0 /\ -2-y_6^0+z_7^0 >= 0), cost: -4*y_6^0+4*z_7^0 79: l14 -> l3 : tmp_8^0'=0, y_6^0'=-1+z_7^0, (1-y_6^0+x_5^0 <= 0 /\ -3-y_6^0+z_7^0 >= 0), cost: -1-4*y_6^0+4*z_7^0 Eliminating location l3 by chaining: Applied chaining First rule: l14 -> l3 : tmp_8^0'=0, (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: 4 Second rule: l3 -> [16] : 2+y_6^0-z_7^0 <= 0, cost: NONTERM New rule: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 2+y_6^0-z_7^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: NONTERM Applied simplification Original rule: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 2+y_6^0-z_7^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: NONTERM New rule: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 2+y_6^0-z_7^0 <= 0), cost: NONTERM Applied chaining First rule: l14 -> l3 : tmp_8^0'=0, y_6^0'=1+y_6^0, (1-y_6^0+x_5^0 <= 0 /\ 2+y_6^0-z_7^0 <= 0), cost: 7 Second rule: l3 -> [16] : 2+y_6^0-z_7^0 <= 0, cost: NONTERM New rule: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 2+y_6^0-z_7^0 <= 0 /\ 3+y_6^0-z_7^0 <= 0), cost: NONTERM Applied simplification Original rule: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 2+y_6^0-z_7^0 <= 0 /\ 3+y_6^0-z_7^0 <= 0), cost: NONTERM New rule: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 3+y_6^0-z_7^0 <= 0), cost: NONTERM Applied partial deletion Original rule: l14 -> l3 : tmp_8^0'=0, y_6^0'=-1+z_7^0, (1-y_6^0+x_5^0 <= 0 /\ -2-y_6^0+z_7^0 >= 0), cost: -4*y_6^0+4*z_7^0 New rule: l14 -> [21] : (1-y_6^0+x_5^0 <= 0 /\ -2-y_6^0+z_7^0 >= 0), cost: -4*y_6^0+4*z_7^0 Applied partial deletion Original rule: l14 -> l3 : tmp_8^0'=0, y_6^0'=-1+z_7^0, (1-y_6^0+x_5^0 <= 0 /\ -3-y_6^0+z_7^0 >= 0), cost: -1-4*y_6^0+4*z_7^0 New rule: l14 -> [21] : (1-y_6^0+x_5^0 <= 0 /\ -3-y_6^0+z_7^0 >= 0), cost: -1-4*y_6^0+4*z_7^0 Applied deletion Removed the following rules: 64 71 72 78 79 Eliminated locations on tree-shaped paths Start location: l14 67: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0), cost: NONTERM 73: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 2+y_6^0-z_7^0 <= 0), cost: NONTERM 80: l14 -> [16] : (1-y_6^0+x_5^0 <= 0 /\ 3+y_6^0-z_7^0 <= 0), cost: NONTERM 81: l14 -> [21] : (1-y_6^0+x_5^0 <= 0 /\ -2-y_6^0+z_7^0 >= 0), cost: -4*y_6^0+4*z_7^0 82: l14 -> [21] : (1-y_6^0+x_5^0 <= 0 /\ -3-y_6^0+z_7^0 >= 0), cost: -1-4*y_6^0+4*z_7^0 Computing asymptotic complexity Proved nontermination of rule 67 via SMT. Proved the following lower bound Complexity: Nonterm Cpx degree: Nonterm Solved cost: NONTERM Rule cost: NONTERM Rule guard: (1-y_6^0+x_5^0 <= 0 /\ 1+y_6^0-z_7^0 <= 0)