WORST_CASE(Omega(0),?) Initial ITS Start location: l18 0: l0 -> l1 : i7^0'=i7^post0, i13^0'=i13^post0, i^0'=i^post0, i17^0'=i17^post0, i11^0'=i11^post0, tmp___0^0'=tmp___0^post0, i9^0'=i9^post0, i15^0'=i15^post0, tmp^0'=tmp^post0, (i11^0-i11^post0 == 0 /\ -tmp^post0+tmp^0 == 0 /\ tmp___0^0-tmp___0^post0 == 0 /\ i^0-i^post0 == 0 /\ i7^0-i7^post0 == 0 /\ i13^0-i13^post0 == 0 /\ -i15^post0+i15^0 == 0 /\ -i9^post0+i9^0 == 0 /\ i17^0-i17^post0 == 0), cost: 1 22: l1 -> l5 : i7^0'=i7^post22, i13^0'=i13^post22, i^0'=i^post22, i17^0'=i17^post22, i11^0'=i11^post22, tmp___0^0'=tmp___0^post22, i9^0'=i9^post22, i15^0'=i15^post22, tmp^0'=tmp^post22, (i9^10 == 0 /\ i7^0-i7^post22 == 0 /\ i17^0-i17^post22 == 0 /\ -tmp___0^post22+tmp___0^0 == 0 /\ 50-i7^0 <= 0 /\ i^0-i^post22 == 0 /\ -i11^post22+i11^0 == 0 /\ -tmp^post22+tmp^0 == 0 /\ -i15^post22+i15^0 == 0 /\ i13^0-i13^post22 == 0 /\ i9^post22 == 0), cost: 1 23: l1 -> l0 : i7^0'=i7^post23, i13^0'=i13^post23, i^0'=i^post23, i17^0'=i17^post23, i11^0'=i11^post23, tmp___0^0'=tmp___0^post23, i9^0'=i9^post23, i15^0'=i15^post23, tmp^0'=tmp^post23, (-i11^post23+i11^0 == 0 /\ i15^0-i15^post23 == 0 /\ i17^0-i17^post23 == 0 /\ -tmp^post23+tmp^0 == 0 /\ -1-i7^0+i7^post23 == 0 /\ i13^0-i13^post23 == 0 /\ i9^0-i9^post23 == 0 /\ -49+i7^0 <= 0 /\ -tmp___0^post23+tmp___0^0 == 0 /\ i^0-i^post23 == 0), cost: 1 1: l2 -> l3 : i7^0'=i7^post1, i13^0'=i13^post1, i^0'=i^post1, i17^0'=i17^post1, i11^0'=i11^post1, tmp___0^0'=tmp___0^post1, i9^0'=i9^post1, i15^0'=i15^post1, tmp^0'=tmp^post1, (-tmp^post1+tmp^0 == 0 /\ -i15^post1+i15^0 == 0 /\ -i9^post1+i9^0 == 0 /\ i7^0-i7^post1 == 0 /\ i^0-i^post1 == 0 /\ -i13^post1+i13^0 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -i11^post1+i11^0 == 0 /\ i17^0-i17^post1 == 0 /\ 50-i^0 <= 0), cost: 1 2: l2 -> l4 : i7^0'=i7^post2, i13^0'=i13^post2, i^0'=i^post2, i17^0'=i17^post2, i11^0'=i11^post2, tmp___0^0'=tmp___0^post2, i9^0'=i9^post2, i15^0'=i15^post2, tmp^0'=tmp^post2, (-49+i^0 <= 0 /\ -1-i^0+i^post2 == 0 /\ i13^0-i13^post2 == 0 /\ i15^0-i15^post2 == 0 /\ -tmp^post2+tmp^0 == 0 /\ i17^0-i17^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ i7^0-i7^post2 == 0 /\ i9^0-i9^post2 == 0 /\ -i11^post2+i11^0 == 0), cost: 1 21: l4 -> l2 : i7^0'=i7^post21, i13^0'=i13^post21, i^0'=i^post21, i17^0'=i17^post21, i11^0'=i11^post21, tmp___0^0'=tmp___0^post21, i9^0'=i9^post21, i15^0'=i15^post21, tmp^0'=tmp^post21, (-tmp^post21+tmp^0 == 0 /\ -i9^post21+i9^0 == 0 /\ -i15^post21+i15^0 == 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ -i17^post21+i17^0 == 0 /\ i13^0-i13^post21 == 0 /\ i11^0-i11^post21 == 0 /\ i7^0-i7^post21 == 0 /\ i^0-i^post21 == 0), cost: 1 3: l5 -> l6 : i7^0'=i7^post3, i13^0'=i13^post3, i^0'=i^post3, i17^0'=i17^post3, i11^0'=i11^post3, tmp___0^0'=tmp___0^post3, i9^0'=i9^post3, i15^0'=i15^post3, tmp^0'=tmp^post3, (-i15^post3+i15^0 == 0 /\ -i9^post3+i9^0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ -i17^post3+i17^0 == 0 /\ i11^0-i11^post3 == 0 /\ i7^0-i7^post3 == 0 /\ -i^post3+i^0 == 0 /\ i13^0-i13^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0), cost: 1 19: l6 -> l9 : i7^0'=i7^post19, i13^0'=i13^post19, i^0'=i^post19, i17^0'=i17^post19, i11^0'=i11^post19, tmp___0^0'=tmp___0^post19, i9^0'=i9^post19, i15^0'=i15^post19, tmp^0'=tmp^post19, (i13^0-i13^post19 == 0 /\ i11^10 == 0 /\ -i^post19+i^0 == 0 /\ tmp___0^0-tmp___0^post19 == 0 /\ -i9^post19+i9^0 == 0 /\ -tmp^post19+tmp^0 == 0 /\ i7^0-i7^post19 == 0 /\ 50-i9^0 <= 0 /\ i11^post19 == 0 /\ -i17^post19+i17^0 == 0 /\ -i15^post19+i15^0 == 0), cost: 1 20: l6 -> l5 : i7^0'=i7^post20, i13^0'=i13^post20, i^0'=i^post20, i17^0'=i17^post20, i11^0'=i11^post20, tmp___0^0'=tmp___0^post20, i9^0'=i9^post20, i15^0'=i15^post20, tmp^0'=tmp^post20, (-1+i9^post20-i9^0 == 0 /\ i11^0-i11^post20 == 0 /\ tmp___0^0-tmp___0^post20 == 0 /\ i7^0-i7^post20 == 0 /\ -i^post20+i^0 == 0 /\ -49+i9^0 <= 0 /\ -i15^post20+i15^0 == 0 /\ -tmp^post20+tmp^0 == 0 /\ i13^0-i13^post20 == 0 /\ -i17^post20+i17^0 == 0), cost: 1 4: l7 -> l4 : i7^0'=i7^post4, i13^0'=i13^post4, i^0'=i^post4, i17^0'=i17^post4, i11^0'=i11^post4, tmp___0^0'=tmp___0^post4, i9^0'=i9^post4, i15^0'=i15^post4, tmp^0'=tmp^post4, (i^post4 == 0 /\ i7^0-i7^post4 == 0 /\ -i9^post4+i9^0 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ -i17^post4+i17^0 == 0 /\ -i15^post4+i15^0 == 0 /\ -tmp^post4+tmp^0 == 0 /\ i11^0-i11^post4 == 0 /\ i13^0-i13^post4 == 0 /\ 50-i17^0 <= 0), cost: 1 5: l7 -> l8 : i7^0'=i7^post5, i13^0'=i13^post5, i^0'=i^post5, i17^0'=i17^post5, i11^0'=i11^post5, tmp___0^0'=tmp___0^post5, i9^0'=i9^post5, i15^0'=i15^post5, tmp^0'=tmp^post5, (-49+i17^0 <= 0 /\ -i13^post5+i13^0 == 0 /\ -tmp^post5+tmp^0 == 0 /\ -1+i17^post5-i17^0 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ -i15^post5+i15^0 == 0 /\ i7^0-i7^post5 == 0 /\ i^0-i^post5 == 0 /\ -i9^post5+i9^0 == 0 /\ i11^0-i11^post5 == 0), cost: 1 18: l8 -> l7 : i7^0'=i7^post18, i13^0'=i13^post18, i^0'=i^post18, i17^0'=i17^post18, i11^0'=i11^post18, tmp___0^0'=tmp___0^post18, i9^0'=i9^post18, i15^0'=i15^post18, tmp^0'=tmp^post18, (-i11^post18+i11^0 == 0 /\ -i15^post18+i15^0 == 0 /\ -i9^post18+i9^0 == 0 /\ -tmp^post18+tmp^0 == 0 /\ i7^0-i7^post18 == 0 /\ i^0-i^post18 == 0 /\ i17^0-i17^post18 == 0 /\ -i13^post18+i13^0 == 0 /\ -tmp___0^post18+tmp___0^0 == 0), cost: 1 6: l9 -> l10 : i7^0'=i7^post6, i13^0'=i13^post6, i^0'=i^post6, i17^0'=i17^post6, i11^0'=i11^post6, tmp___0^0'=tmp___0^post6, i9^0'=i9^post6, i15^0'=i15^post6, tmp^0'=tmp^post6, (-tmp___0^post6+tmp___0^0 == 0 /\ i^0-i^post6 == 0 /\ -tmp^post6+tmp^0 == 0 /\ i15^0-i15^post6 == 0 /\ i13^0-i13^post6 == 0 /\ i17^0-i17^post6 == 0 /\ i7^0-i7^post6 == 0 /\ i9^0-i9^post6 == 0 /\ -i11^post6+i11^0 == 0), cost: 1 16: l10 -> l13 : i7^0'=i7^post16, i13^0'=i13^post16, i^0'=i^post16, i17^0'=i17^post16, i11^0'=i11^post16, tmp___0^0'=tmp___0^post16, i9^0'=i9^post16, i15^0'=i15^post16, tmp^0'=tmp^post16, (i^post16 == 0 /\ i11^0-i11^post16 == 0 /\ 50-i11^0 <= 0 /\ tmp___0^0-tmp___0^post16 == 0 /\ -tmp^post16+tmp^0 == 0 /\ -i9^post16+i9^0 == 0 /\ i13^0-i13^post16 == 0 /\ -i17^post16+i17^0 == 0 /\ -i15^post16+i15^0 == 0 /\ i7^0-i7^post16 == 0), cost: 1 17: l10 -> l9 : i7^0'=i7^post17, i13^0'=i13^post17, i^0'=i^post17, i17^0'=i17^post17, i11^0'=i11^post17, tmp___0^0'=tmp___0^post17, i9^0'=i9^post17, i15^0'=i15^post17, tmp^0'=tmp^post17, (-1-i11^0+i11^post17 == 0 /\ i13^0-i13^post17 == 0 /\ -tmp^post17+tmp^0 == 0 /\ -i9^post17+i9^0 == 0 /\ i7^0-i7^post17 == 0 /\ tmp___0^0-tmp___0^post17 == 0 /\ i17^0-i17^post17 == 0 /\ -49+i11^0 <= 0 /\ i^0-i^post17 == 0 /\ -i15^post17+i15^0 == 0), cost: 1 7: l11 -> l8 : i7^0'=i7^post7, i13^0'=i13^post7, i^0'=i^post7, i17^0'=i17^post7, i11^0'=i11^post7, tmp___0^0'=tmp___0^post7, i9^0'=i9^post7, i15^0'=i15^post7, tmp^0'=tmp^post7, (i17^post7 == 0 /\ -i15^post7+i15^0 == 0 /\ i13^0-i13^post7 == 0 /\ i17^10 == 0 /\ -i^post7+i^0 == 0 /\ -tmp^post7+tmp^0 == 0 /\ i9^0-i9^post7 == 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ i7^0-i7^post7 == 0 /\ 50-i15^0 <= 0 /\ -i11^post7+i11^0 == 0), cost: 1 8: l11 -> l12 : i7^0'=i7^post8, i13^0'=i13^post8, i^0'=i^post8, i17^0'=i17^post8, i11^0'=i11^post8, tmp___0^0'=tmp___0^post8, i9^0'=i9^post8, i15^0'=i15^post8, tmp^0'=tmp^post8, (tmp___0^0-tmp___0^post8 == 0 /\ i7^0-i7^post8 == 0 /\ -i17^post8+i17^0 == 0 /\ -49+i15^0 <= 0 /\ i11^0-i11^post8 == 0 /\ -i^post8+i^0 == 0 /\ i13^0-i13^post8 == 0 /\ -i9^post8+i9^0 == 0 /\ -1+i15^post8-i15^0 == 0 /\ -tmp^post8+tmp^0 == 0), cost: 1 15: l12 -> l11 : i7^0'=i7^post15, i13^0'=i13^post15, i^0'=i^post15, i17^0'=i17^post15, i11^0'=i11^post15, tmp___0^0'=tmp___0^post15, i9^0'=i9^post15, i15^0'=i15^post15, tmp^0'=tmp^post15, (i13^0-i13^post15 == 0 /\ -tmp___0^post15+tmp___0^0 == 0 /\ -i^post15+i^0 == 0 /\ i9^0-i9^post15 == 0 /\ -tmp^post15+tmp^0 == 0 /\ -i11^post15+i11^0 == 0 /\ i7^0-i7^post15 == 0 /\ -i15^post15+i15^0 == 0 /\ i17^0-i17^post15 == 0), cost: 1 9: l13 -> l14 : i7^0'=i7^post9, i13^0'=i13^post9, i^0'=i^post9, i17^0'=i17^post9, i11^0'=i11^post9, tmp___0^0'=tmp___0^post9, i9^0'=i9^post9, i15^0'=i15^post9, tmp^0'=tmp^post9, (-i15^post9+i15^0 == 0 /\ -i17^post9+i17^0 == 0 /\ -tmp^post9+tmp^0 == 0 /\ i7^0-i7^post9 == 0 /\ i^0-i^post9 == 0 /\ tmp___0^0-tmp___0^post9 == 0 /\ -i13^post9+i13^0 == 0 /\ i11^0-i11^post9 == 0 /\ -i9^post9+i9^0 == 0), cost: 1 13: l14 -> l16 : i7^0'=i7^post13, i13^0'=i13^post13, i^0'=i^post13, i17^0'=i17^post13, i11^0'=i11^post13, tmp___0^0'=tmp___0^post13, i9^0'=i9^post13, i15^0'=i15^post13, tmp^0'=tmp^post13, (i13^10 == 0 /\ i7^0-i7^post13 == 0 /\ i17^0-i17^post13 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ i^0-i^post13 == 0 /\ -i11^post13+i11^0 == 0 /\ -i15^post13+i15^0 == 0 /\ i9^0-i9^post13 == 0 /\ 50-i^0 <= 0 /\ i13^post13 == 0 /\ -tmp^post13+tmp^0 == 0), cost: 1 14: l14 -> l13 : i7^0'=i7^post14, i13^0'=i13^post14, i^0'=i^post14, i17^0'=i17^post14, i11^0'=i11^post14, tmp___0^0'=tmp___0^post14, i9^0'=i9^post14, i15^0'=i15^post14, tmp^0'=tmp^post14, (-49+i^0 <= 0 /\ i7^0-i7^post14 == 0 /\ i15^0-i15^post14 == 0 /\ i17^0-i17^post14 == 0 /\ -i11^post14+i11^0 == 0 /\ -i9^post14+i9^0 == 0 /\ -1-i^0+i^post14 == 0 /\ -tmp^post14+tmp^0 == 0 /\ -tmp___0^post14+tmp___0^0 == 0 /\ i13^0-i13^post14 == 0), cost: 1 10: l15 -> l12 : i7^0'=i7^post10, i13^0'=i13^post10, i^0'=i^post10, i17^0'=i17^post10, i11^0'=i11^post10, tmp___0^0'=tmp___0^post10, i9^0'=i9^post10, i15^0'=i15^post10, tmp^0'=tmp^post10, (i11^0-i11^post10 == 0 /\ i15^10 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ 50-i13^0 <= 0 /\ i7^0-i7^post10 == 0 /\ i13^0-i13^post10 == 0 /\ -i9^post10+i9^0 == 0 /\ i15^post10 == 0 /\ i^0-i^post10 == 0 /\ -tmp^post10+tmp^0 == 0 /\ -i17^post10+i17^0 == 0), cost: 1 11: l15 -> l16 : i7^0'=i7^post11, i13^0'=i13^post11, i^0'=i^post11, i17^0'=i17^post11, i11^0'=i11^post11, tmp___0^0'=tmp___0^post11, i9^0'=i9^post11, i15^0'=i15^post11, tmp^0'=tmp^post11, (-i^post11+i^0 == 0 /\ -tmp^post11+tmp^0 == 0 /\ i7^0-i7^post11 == 0 /\ -tmp___0^post11+tmp___0^0 == 0 /\ -49+i13^0 <= 0 /\ -1-i13^0+i13^post11 == 0 /\ i9^0-i9^post11 == 0 /\ i17^0-i17^post11 == 0 /\ -i15^post11+i15^0 == 0 /\ -i11^post11+i11^0 == 0), cost: 1 12: l16 -> l15 : i7^0'=i7^post12, i13^0'=i13^post12, i^0'=i^post12, i17^0'=i17^post12, i11^0'=i11^post12, tmp___0^0'=tmp___0^post12, i9^0'=i9^post12, i15^0'=i15^post12, tmp^0'=tmp^post12, (i11^0-i11^post12 == 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ -i15^post12+i15^0 == 0 /\ -tmp^post12+tmp^0 == 0 /\ -i9^post12+i9^0 == 0 /\ i13^0-i13^post12 == 0 /\ i^0-i^post12 == 0 /\ -i17^post12+i17^0 == 0 /\ i7^0-i7^post12 == 0), cost: 1 24: l17 -> l0 : i7^0'=i7^post24, i13^0'=i13^post24, i^0'=i^post24, i17^0'=i17^post24, i11^0'=i11^post24, tmp___0^0'=tmp___0^post24, i9^0'=i9^post24, i15^0'=i15^post24, tmp^0'=tmp^post24, (0 == 0 /\ i13^0-i13^post24 == 0 /\ i7^10 == 0 /\ i^post24 == 0 /\ i9^0-i9^post24 == 0 /\ -i15^post24+i15^0 == 0 /\ i7^post24 == 0 /\ i17^0-i17^post24 == 0 /\ -i11^post24+i11^0 == 0), cost: 1 25: l18 -> l17 : i7^0'=i7^post25, i13^0'=i13^post25, i^0'=i^post25, i17^0'=i17^post25, i11^0'=i11^post25, tmp___0^0'=tmp___0^post25, i9^0'=i9^post25, i15^0'=i15^post25, tmp^0'=tmp^post25, (-i15^post25+i15^0 == 0 /\ i11^0-i11^post25 == 0 /\ tmp___0^0-tmp___0^post25 == 0 /\ -tmp^post25+tmp^0 == 0 /\ i13^0-i13^post25 == 0 /\ -i9^post25+i9^0 == 0 /\ -i17^post25+i17^0 == 0 /\ i7^0-i7^post25 == 0 /\ i^0-i^post25 == 0), cost: 1 Removed unreachable rules and leafs Start location: l18 0: l0 -> l1 : i7^0'=i7^post0, i13^0'=i13^post0, i^0'=i^post0, i17^0'=i17^post0, i11^0'=i11^post0, tmp___0^0'=tmp___0^post0, i9^0'=i9^post0, i15^0'=i15^post0, tmp^0'=tmp^post0, (i11^0-i11^post0 == 0 /\ -tmp^post0+tmp^0 == 0 /\ tmp___0^0-tmp___0^post0 == 0 /\ i^0-i^post0 == 0 /\ i7^0-i7^post0 == 0 /\ i13^0-i13^post0 == 0 /\ -i15^post0+i15^0 == 0 /\ -i9^post0+i9^0 == 0 /\ i17^0-i17^post0 == 0), cost: 1 22: l1 -> l5 : i7^0'=i7^post22, i13^0'=i13^post22, i^0'=i^post22, i17^0'=i17^post22, i11^0'=i11^post22, tmp___0^0'=tmp___0^post22, i9^0'=i9^post22, i15^0'=i15^post22, tmp^0'=tmp^post22, (i9^10 == 0 /\ i7^0-i7^post22 == 0 /\ i17^0-i17^post22 == 0 /\ -tmp___0^post22+tmp___0^0 == 0 /\ 50-i7^0 <= 0 /\ i^0-i^post22 == 0 /\ -i11^post22+i11^0 == 0 /\ -tmp^post22+tmp^0 == 0 /\ -i15^post22+i15^0 == 0 /\ i13^0-i13^post22 == 0 /\ i9^post22 == 0), cost: 1 23: l1 -> l0 : i7^0'=i7^post23, i13^0'=i13^post23, i^0'=i^post23, i17^0'=i17^post23, i11^0'=i11^post23, tmp___0^0'=tmp___0^post23, i9^0'=i9^post23, i15^0'=i15^post23, tmp^0'=tmp^post23, (-i11^post23+i11^0 == 0 /\ i15^0-i15^post23 == 0 /\ i17^0-i17^post23 == 0 /\ -tmp^post23+tmp^0 == 0 /\ -1-i7^0+i7^post23 == 0 /\ i13^0-i13^post23 == 0 /\ i9^0-i9^post23 == 0 /\ -49+i7^0 <= 0 /\ -tmp___0^post23+tmp___0^0 == 0 /\ i^0-i^post23 == 0), cost: 1 2: l2 -> l4 : i7^0'=i7^post2, i13^0'=i13^post2, i^0'=i^post2, i17^0'=i17^post2, i11^0'=i11^post2, tmp___0^0'=tmp___0^post2, i9^0'=i9^post2, i15^0'=i15^post2, tmp^0'=tmp^post2, (-49+i^0 <= 0 /\ -1-i^0+i^post2 == 0 /\ i13^0-i13^post2 == 0 /\ i15^0-i15^post2 == 0 /\ -tmp^post2+tmp^0 == 0 /\ i17^0-i17^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ i7^0-i7^post2 == 0 /\ i9^0-i9^post2 == 0 /\ -i11^post2+i11^0 == 0), cost: 1 21: l4 -> l2 : i7^0'=i7^post21, i13^0'=i13^post21, i^0'=i^post21, i17^0'=i17^post21, i11^0'=i11^post21, tmp___0^0'=tmp___0^post21, i9^0'=i9^post21, i15^0'=i15^post21, tmp^0'=tmp^post21, (-tmp^post21+tmp^0 == 0 /\ -i9^post21+i9^0 == 0 /\ -i15^post21+i15^0 == 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ -i17^post21+i17^0 == 0 /\ i13^0-i13^post21 == 0 /\ i11^0-i11^post21 == 0 /\ i7^0-i7^post21 == 0 /\ i^0-i^post21 == 0), cost: 1 3: l5 -> l6 : i7^0'=i7^post3, i13^0'=i13^post3, i^0'=i^post3, i17^0'=i17^post3, i11^0'=i11^post3, tmp___0^0'=tmp___0^post3, i9^0'=i9^post3, i15^0'=i15^post3, tmp^0'=tmp^post3, (-i15^post3+i15^0 == 0 /\ -i9^post3+i9^0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ -i17^post3+i17^0 == 0 /\ i11^0-i11^post3 == 0 /\ i7^0-i7^post3 == 0 /\ -i^post3+i^0 == 0 /\ i13^0-i13^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0), cost: 1 19: l6 -> l9 : i7^0'=i7^post19, i13^0'=i13^post19, i^0'=i^post19, i17^0'=i17^post19, i11^0'=i11^post19, tmp___0^0'=tmp___0^post19, i9^0'=i9^post19, i15^0'=i15^post19, tmp^0'=tmp^post19, (i13^0-i13^post19 == 0 /\ i11^10 == 0 /\ -i^post19+i^0 == 0 /\ tmp___0^0-tmp___0^post19 == 0 /\ -i9^post19+i9^0 == 0 /\ -tmp^post19+tmp^0 == 0 /\ i7^0-i7^post19 == 0 /\ 50-i9^0 <= 0 /\ i11^post19 == 0 /\ -i17^post19+i17^0 == 0 /\ -i15^post19+i15^0 == 0), cost: 1 20: l6 -> l5 : i7^0'=i7^post20, i13^0'=i13^post20, i^0'=i^post20, i17^0'=i17^post20, i11^0'=i11^post20, tmp___0^0'=tmp___0^post20, i9^0'=i9^post20, i15^0'=i15^post20, tmp^0'=tmp^post20, (-1+i9^post20-i9^0 == 0 /\ i11^0-i11^post20 == 0 /\ tmp___0^0-tmp___0^post20 == 0 /\ i7^0-i7^post20 == 0 /\ -i^post20+i^0 == 0 /\ -49+i9^0 <= 0 /\ -i15^post20+i15^0 == 0 /\ -tmp^post20+tmp^0 == 0 /\ i13^0-i13^post20 == 0 /\ -i17^post20+i17^0 == 0), cost: 1 4: l7 -> l4 : i7^0'=i7^post4, i13^0'=i13^post4, i^0'=i^post4, i17^0'=i17^post4, i11^0'=i11^post4, tmp___0^0'=tmp___0^post4, i9^0'=i9^post4, i15^0'=i15^post4, tmp^0'=tmp^post4, (i^post4 == 0 /\ i7^0-i7^post4 == 0 /\ -i9^post4+i9^0 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ -i17^post4+i17^0 == 0 /\ -i15^post4+i15^0 == 0 /\ -tmp^post4+tmp^0 == 0 /\ i11^0-i11^post4 == 0 /\ i13^0-i13^post4 == 0 /\ 50-i17^0 <= 0), cost: 1 5: l7 -> l8 : i7^0'=i7^post5, i13^0'=i13^post5, i^0'=i^post5, i17^0'=i17^post5, i11^0'=i11^post5, tmp___0^0'=tmp___0^post5, i9^0'=i9^post5, i15^0'=i15^post5, tmp^0'=tmp^post5, (-49+i17^0 <= 0 /\ -i13^post5+i13^0 == 0 /\ -tmp^post5+tmp^0 == 0 /\ -1+i17^post5-i17^0 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ -i15^post5+i15^0 == 0 /\ i7^0-i7^post5 == 0 /\ i^0-i^post5 == 0 /\ -i9^post5+i9^0 == 0 /\ i11^0-i11^post5 == 0), cost: 1 18: l8 -> l7 : i7^0'=i7^post18, i13^0'=i13^post18, i^0'=i^post18, i17^0'=i17^post18, i11^0'=i11^post18, tmp___0^0'=tmp___0^post18, i9^0'=i9^post18, i15^0'=i15^post18, tmp^0'=tmp^post18, (-i11^post18+i11^0 == 0 /\ -i15^post18+i15^0 == 0 /\ -i9^post18+i9^0 == 0 /\ -tmp^post18+tmp^0 == 0 /\ i7^0-i7^post18 == 0 /\ i^0-i^post18 == 0 /\ i17^0-i17^post18 == 0 /\ -i13^post18+i13^0 == 0 /\ -tmp___0^post18+tmp___0^0 == 0), cost: 1 6: l9 -> l10 : i7^0'=i7^post6, i13^0'=i13^post6, i^0'=i^post6, i17^0'=i17^post6, i11^0'=i11^post6, tmp___0^0'=tmp___0^post6, i9^0'=i9^post6, i15^0'=i15^post6, tmp^0'=tmp^post6, (-tmp___0^post6+tmp___0^0 == 0 /\ i^0-i^post6 == 0 /\ -tmp^post6+tmp^0 == 0 /\ i15^0-i15^post6 == 0 /\ i13^0-i13^post6 == 0 /\ i17^0-i17^post6 == 0 /\ i7^0-i7^post6 == 0 /\ i9^0-i9^post6 == 0 /\ -i11^post6+i11^0 == 0), cost: 1 16: l10 -> l13 : i7^0'=i7^post16, i13^0'=i13^post16, i^0'=i^post16, i17^0'=i17^post16, i11^0'=i11^post16, tmp___0^0'=tmp___0^post16, i9^0'=i9^post16, i15^0'=i15^post16, tmp^0'=tmp^post16, (i^post16 == 0 /\ i11^0-i11^post16 == 0 /\ 50-i11^0 <= 0 /\ tmp___0^0-tmp___0^post16 == 0 /\ -tmp^post16+tmp^0 == 0 /\ -i9^post16+i9^0 == 0 /\ i13^0-i13^post16 == 0 /\ -i17^post16+i17^0 == 0 /\ -i15^post16+i15^0 == 0 /\ i7^0-i7^post16 == 0), cost: 1 17: l10 -> l9 : i7^0'=i7^post17, i13^0'=i13^post17, i^0'=i^post17, i17^0'=i17^post17, i11^0'=i11^post17, tmp___0^0'=tmp___0^post17, i9^0'=i9^post17, i15^0'=i15^post17, tmp^0'=tmp^post17, (-1-i11^0+i11^post17 == 0 /\ i13^0-i13^post17 == 0 /\ -tmp^post17+tmp^0 == 0 /\ -i9^post17+i9^0 == 0 /\ i7^0-i7^post17 == 0 /\ tmp___0^0-tmp___0^post17 == 0 /\ i17^0-i17^post17 == 0 /\ -49+i11^0 <= 0 /\ i^0-i^post17 == 0 /\ -i15^post17+i15^0 == 0), cost: 1 7: l11 -> l8 : i7^0'=i7^post7, i13^0'=i13^post7, i^0'=i^post7, i17^0'=i17^post7, i11^0'=i11^post7, tmp___0^0'=tmp___0^post7, i9^0'=i9^post7, i15^0'=i15^post7, tmp^0'=tmp^post7, (i17^post7 == 0 /\ -i15^post7+i15^0 == 0 /\ i13^0-i13^post7 == 0 /\ i17^10 == 0 /\ -i^post7+i^0 == 0 /\ -tmp^post7+tmp^0 == 0 /\ i9^0-i9^post7 == 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ i7^0-i7^post7 == 0 /\ 50-i15^0 <= 0 /\ -i11^post7+i11^0 == 0), cost: 1 8: l11 -> l12 : i7^0'=i7^post8, i13^0'=i13^post8, i^0'=i^post8, i17^0'=i17^post8, i11^0'=i11^post8, tmp___0^0'=tmp___0^post8, i9^0'=i9^post8, i15^0'=i15^post8, tmp^0'=tmp^post8, (tmp___0^0-tmp___0^post8 == 0 /\ i7^0-i7^post8 == 0 /\ -i17^post8+i17^0 == 0 /\ -49+i15^0 <= 0 /\ i11^0-i11^post8 == 0 /\ -i^post8+i^0 == 0 /\ i13^0-i13^post8 == 0 /\ -i9^post8+i9^0 == 0 /\ -1+i15^post8-i15^0 == 0 /\ -tmp^post8+tmp^0 == 0), cost: 1 15: l12 -> l11 : i7^0'=i7^post15, i13^0'=i13^post15, i^0'=i^post15, i17^0'=i17^post15, i11^0'=i11^post15, tmp___0^0'=tmp___0^post15, i9^0'=i9^post15, i15^0'=i15^post15, tmp^0'=tmp^post15, (i13^0-i13^post15 == 0 /\ -tmp___0^post15+tmp___0^0 == 0 /\ -i^post15+i^0 == 0 /\ i9^0-i9^post15 == 0 /\ -tmp^post15+tmp^0 == 0 /\ -i11^post15+i11^0 == 0 /\ i7^0-i7^post15 == 0 /\ -i15^post15+i15^0 == 0 /\ i17^0-i17^post15 == 0), cost: 1 9: l13 -> l14 : i7^0'=i7^post9, i13^0'=i13^post9, i^0'=i^post9, i17^0'=i17^post9, i11^0'=i11^post9, tmp___0^0'=tmp___0^post9, i9^0'=i9^post9, i15^0'=i15^post9, tmp^0'=tmp^post9, (-i15^post9+i15^0 == 0 /\ -i17^post9+i17^0 == 0 /\ -tmp^post9+tmp^0 == 0 /\ i7^0-i7^post9 == 0 /\ i^0-i^post9 == 0 /\ tmp___0^0-tmp___0^post9 == 0 /\ -i13^post9+i13^0 == 0 /\ i11^0-i11^post9 == 0 /\ -i9^post9+i9^0 == 0), cost: 1 13: l14 -> l16 : i7^0'=i7^post13, i13^0'=i13^post13, i^0'=i^post13, i17^0'=i17^post13, i11^0'=i11^post13, tmp___0^0'=tmp___0^post13, i9^0'=i9^post13, i15^0'=i15^post13, tmp^0'=tmp^post13, (i13^10 == 0 /\ i7^0-i7^post13 == 0 /\ i17^0-i17^post13 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ i^0-i^post13 == 0 /\ -i11^post13+i11^0 == 0 /\ -i15^post13+i15^0 == 0 /\ i9^0-i9^post13 == 0 /\ 50-i^0 <= 0 /\ i13^post13 == 0 /\ -tmp^post13+tmp^0 == 0), cost: 1 14: l14 -> l13 : i7^0'=i7^post14, i13^0'=i13^post14, i^0'=i^post14, i17^0'=i17^post14, i11^0'=i11^post14, tmp___0^0'=tmp___0^post14, i9^0'=i9^post14, i15^0'=i15^post14, tmp^0'=tmp^post14, (-49+i^0 <= 0 /\ i7^0-i7^post14 == 0 /\ i15^0-i15^post14 == 0 /\ i17^0-i17^post14 == 0 /\ -i11^post14+i11^0 == 0 /\ -i9^post14+i9^0 == 0 /\ -1-i^0+i^post14 == 0 /\ -tmp^post14+tmp^0 == 0 /\ -tmp___0^post14+tmp___0^0 == 0 /\ i13^0-i13^post14 == 0), cost: 1 10: l15 -> l12 : i7^0'=i7^post10, i13^0'=i13^post10, i^0'=i^post10, i17^0'=i17^post10, i11^0'=i11^post10, tmp___0^0'=tmp___0^post10, i9^0'=i9^post10, i15^0'=i15^post10, tmp^0'=tmp^post10, (i11^0-i11^post10 == 0 /\ i15^10 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ 50-i13^0 <= 0 /\ i7^0-i7^post10 == 0 /\ i13^0-i13^post10 == 0 /\ -i9^post10+i9^0 == 0 /\ i15^post10 == 0 /\ i^0-i^post10 == 0 /\ -tmp^post10+tmp^0 == 0 /\ -i17^post10+i17^0 == 0), cost: 1 11: l15 -> l16 : i7^0'=i7^post11, i13^0'=i13^post11, i^0'=i^post11, i17^0'=i17^post11, i11^0'=i11^post11, tmp___0^0'=tmp___0^post11, i9^0'=i9^post11, i15^0'=i15^post11, tmp^0'=tmp^post11, (-i^post11+i^0 == 0 /\ -tmp^post11+tmp^0 == 0 /\ i7^0-i7^post11 == 0 /\ -tmp___0^post11+tmp___0^0 == 0 /\ -49+i13^0 <= 0 /\ -1-i13^0+i13^post11 == 0 /\ i9^0-i9^post11 == 0 /\ i17^0-i17^post11 == 0 /\ -i15^post11+i15^0 == 0 /\ -i11^post11+i11^0 == 0), cost: 1 12: l16 -> l15 : i7^0'=i7^post12, i13^0'=i13^post12, i^0'=i^post12, i17^0'=i17^post12, i11^0'=i11^post12, tmp___0^0'=tmp___0^post12, i9^0'=i9^post12, i15^0'=i15^post12, tmp^0'=tmp^post12, (i11^0-i11^post12 == 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ -i15^post12+i15^0 == 0 /\ -tmp^post12+tmp^0 == 0 /\ -i9^post12+i9^0 == 0 /\ i13^0-i13^post12 == 0 /\ i^0-i^post12 == 0 /\ -i17^post12+i17^0 == 0 /\ i7^0-i7^post12 == 0), cost: 1 24: l17 -> l0 : i7^0'=i7^post24, i13^0'=i13^post24, i^0'=i^post24, i17^0'=i17^post24, i11^0'=i11^post24, tmp___0^0'=tmp___0^post24, i9^0'=i9^post24, i15^0'=i15^post24, tmp^0'=tmp^post24, (0 == 0 /\ i13^0-i13^post24 == 0 /\ i7^10 == 0 /\ i^post24 == 0 /\ i9^0-i9^post24 == 0 /\ -i15^post24+i15^0 == 0 /\ i7^post24 == 0 /\ i17^0-i17^post24 == 0 /\ -i11^post24+i11^0 == 0), cost: 1 25: l18 -> l17 : i7^0'=i7^post25, i13^0'=i13^post25, i^0'=i^post25, i17^0'=i17^post25, i11^0'=i11^post25, tmp___0^0'=tmp___0^post25, i9^0'=i9^post25, i15^0'=i15^post25, tmp^0'=tmp^post25, (-i15^post25+i15^0 == 0 /\ i11^0-i11^post25 == 0 /\ tmp___0^0-tmp___0^post25 == 0 /\ -tmp^post25+tmp^0 == 0 /\ i13^0-i13^post25 == 0 /\ -i9^post25+i9^0 == 0 /\ -i17^post25+i17^0 == 0 /\ i7^0-i7^post25 == 0 /\ i^0-i^post25 == 0), cost: 1 Applied preprocessing Original rule: l0 -> l1 : i7^0'=i7^post0, i13^0'=i13^post0, i^0'=i^post0, i17^0'=i17^post0, i11^0'=i11^post0, tmp___0^0'=tmp___0^post0, i9^0'=i9^post0, i15^0'=i15^post0, tmp^0'=tmp^post0, (i11^0-i11^post0 == 0 /\ -tmp^post0+tmp^0 == 0 /\ tmp___0^0-tmp___0^post0 == 0 /\ i^0-i^post0 == 0 /\ i7^0-i7^post0 == 0 /\ i13^0-i13^post0 == 0 /\ -i15^post0+i15^0 == 0 /\ -i9^post0+i9^0 == 0 /\ i17^0-i17^post0 == 0), cost: 1 New rule: l0 -> l1 : TRUE, cost: 1 Applied preprocessing Original rule: l2 -> l4 : i7^0'=i7^post2, i13^0'=i13^post2, i^0'=i^post2, i17^0'=i17^post2, i11^0'=i11^post2, tmp___0^0'=tmp___0^post2, i9^0'=i9^post2, i15^0'=i15^post2, tmp^0'=tmp^post2, (-49+i^0 <= 0 /\ -1-i^0+i^post2 == 0 /\ i13^0-i13^post2 == 0 /\ i15^0-i15^post2 == 0 /\ -tmp^post2+tmp^0 == 0 /\ i17^0-i17^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ i7^0-i7^post2 == 0 /\ i9^0-i9^post2 == 0 /\ -i11^post2+i11^0 == 0), cost: 1 New rule: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 Applied preprocessing Original rule: l5 -> l6 : i7^0'=i7^post3, i13^0'=i13^post3, i^0'=i^post3, i17^0'=i17^post3, i11^0'=i11^post3, tmp___0^0'=tmp___0^post3, i9^0'=i9^post3, i15^0'=i15^post3, tmp^0'=tmp^post3, (-i15^post3+i15^0 == 0 /\ -i9^post3+i9^0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ -i17^post3+i17^0 == 0 /\ i11^0-i11^post3 == 0 /\ i7^0-i7^post3 == 0 /\ -i^post3+i^0 == 0 /\ i13^0-i13^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0), cost: 1 New rule: l5 -> l6 : TRUE, cost: 1 Applied preprocessing Original rule: l7 -> l4 : i7^0'=i7^post4, i13^0'=i13^post4, i^0'=i^post4, i17^0'=i17^post4, i11^0'=i11^post4, tmp___0^0'=tmp___0^post4, i9^0'=i9^post4, i15^0'=i15^post4, tmp^0'=tmp^post4, (i^post4 == 0 /\ i7^0-i7^post4 == 0 /\ -i9^post4+i9^0 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ -i17^post4+i17^0 == 0 /\ -i15^post4+i15^0 == 0 /\ -tmp^post4+tmp^0 == 0 /\ i11^0-i11^post4 == 0 /\ i13^0-i13^post4 == 0 /\ 50-i17^0 <= 0), cost: 1 New rule: l7 -> l4 : i^0'=0, -50+i17^0 >= 0, cost: 1 Applied preprocessing Original rule: l7 -> l8 : i7^0'=i7^post5, i13^0'=i13^post5, i^0'=i^post5, i17^0'=i17^post5, i11^0'=i11^post5, tmp___0^0'=tmp___0^post5, i9^0'=i9^post5, i15^0'=i15^post5, tmp^0'=tmp^post5, (-49+i17^0 <= 0 /\ -i13^post5+i13^0 == 0 /\ -tmp^post5+tmp^0 == 0 /\ -1+i17^post5-i17^0 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ -i15^post5+i15^0 == 0 /\ i7^0-i7^post5 == 0 /\ i^0-i^post5 == 0 /\ -i9^post5+i9^0 == 0 /\ i11^0-i11^post5 == 0), cost: 1 New rule: l7 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 1 Applied preprocessing Original rule: l9 -> l10 : i7^0'=i7^post6, i13^0'=i13^post6, i^0'=i^post6, i17^0'=i17^post6, i11^0'=i11^post6, tmp___0^0'=tmp___0^post6, i9^0'=i9^post6, i15^0'=i15^post6, tmp^0'=tmp^post6, (-tmp___0^post6+tmp___0^0 == 0 /\ i^0-i^post6 == 0 /\ -tmp^post6+tmp^0 == 0 /\ i15^0-i15^post6 == 0 /\ i13^0-i13^post6 == 0 /\ i17^0-i17^post6 == 0 /\ i7^0-i7^post6 == 0 /\ i9^0-i9^post6 == 0 /\ -i11^post6+i11^0 == 0), cost: 1 New rule: l9 -> l10 : TRUE, cost: 1 Applied preprocessing Original rule: l11 -> l8 : i7^0'=i7^post7, i13^0'=i13^post7, i^0'=i^post7, i17^0'=i17^post7, i11^0'=i11^post7, tmp___0^0'=tmp___0^post7, i9^0'=i9^post7, i15^0'=i15^post7, tmp^0'=tmp^post7, (i17^post7 == 0 /\ -i15^post7+i15^0 == 0 /\ i13^0-i13^post7 == 0 /\ i17^10 == 0 /\ -i^post7+i^0 == 0 /\ -tmp^post7+tmp^0 == 0 /\ i9^0-i9^post7 == 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ i7^0-i7^post7 == 0 /\ 50-i15^0 <= 0 /\ -i11^post7+i11^0 == 0), cost: 1 New rule: l11 -> l8 : i17^0'=0, -50+i15^0 >= 0, cost: 1 Applied preprocessing Original rule: l11 -> l12 : i7^0'=i7^post8, i13^0'=i13^post8, i^0'=i^post8, i17^0'=i17^post8, i11^0'=i11^post8, tmp___0^0'=tmp___0^post8, i9^0'=i9^post8, i15^0'=i15^post8, tmp^0'=tmp^post8, (tmp___0^0-tmp___0^post8 == 0 /\ i7^0-i7^post8 == 0 /\ -i17^post8+i17^0 == 0 /\ -49+i15^0 <= 0 /\ i11^0-i11^post8 == 0 /\ -i^post8+i^0 == 0 /\ i13^0-i13^post8 == 0 /\ -i9^post8+i9^0 == 0 /\ -1+i15^post8-i15^0 == 0 /\ -tmp^post8+tmp^0 == 0), cost: 1 New rule: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1 Applied preprocessing Original rule: l13 -> l14 : i7^0'=i7^post9, i13^0'=i13^post9, i^0'=i^post9, i17^0'=i17^post9, i11^0'=i11^post9, tmp___0^0'=tmp___0^post9, i9^0'=i9^post9, i15^0'=i15^post9, tmp^0'=tmp^post9, (-i15^post9+i15^0 == 0 /\ -i17^post9+i17^0 == 0 /\ -tmp^post9+tmp^0 == 0 /\ i7^0-i7^post9 == 0 /\ i^0-i^post9 == 0 /\ tmp___0^0-tmp___0^post9 == 0 /\ -i13^post9+i13^0 == 0 /\ i11^0-i11^post9 == 0 /\ -i9^post9+i9^0 == 0), cost: 1 New rule: l13 -> l14 : TRUE, cost: 1 Applied preprocessing Original rule: l15 -> l12 : i7^0'=i7^post10, i13^0'=i13^post10, i^0'=i^post10, i17^0'=i17^post10, i11^0'=i11^post10, tmp___0^0'=tmp___0^post10, i9^0'=i9^post10, i15^0'=i15^post10, tmp^0'=tmp^post10, (i11^0-i11^post10 == 0 /\ i15^10 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ 50-i13^0 <= 0 /\ i7^0-i7^post10 == 0 /\ i13^0-i13^post10 == 0 /\ -i9^post10+i9^0 == 0 /\ i15^post10 == 0 /\ i^0-i^post10 == 0 /\ -tmp^post10+tmp^0 == 0 /\ -i17^post10+i17^0 == 0), cost: 1 New rule: l15 -> l12 : i15^0'=0, -50+i13^0 >= 0, cost: 1 Applied preprocessing Original rule: l15 -> l16 : i7^0'=i7^post11, i13^0'=i13^post11, i^0'=i^post11, i17^0'=i17^post11, i11^0'=i11^post11, tmp___0^0'=tmp___0^post11, i9^0'=i9^post11, i15^0'=i15^post11, tmp^0'=tmp^post11, (-i^post11+i^0 == 0 /\ -tmp^post11+tmp^0 == 0 /\ i7^0-i7^post11 == 0 /\ -tmp___0^post11+tmp___0^0 == 0 /\ -49+i13^0 <= 0 /\ -1-i13^0+i13^post11 == 0 /\ i9^0-i9^post11 == 0 /\ i17^0-i17^post11 == 0 /\ -i15^post11+i15^0 == 0 /\ -i11^post11+i11^0 == 0), cost: 1 New rule: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 Applied preprocessing Original rule: l16 -> l15 : i7^0'=i7^post12, i13^0'=i13^post12, i^0'=i^post12, i17^0'=i17^post12, i11^0'=i11^post12, tmp___0^0'=tmp___0^post12, i9^0'=i9^post12, i15^0'=i15^post12, tmp^0'=tmp^post12, (i11^0-i11^post12 == 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ -i15^post12+i15^0 == 0 /\ -tmp^post12+tmp^0 == 0 /\ -i9^post12+i9^0 == 0 /\ i13^0-i13^post12 == 0 /\ i^0-i^post12 == 0 /\ -i17^post12+i17^0 == 0 /\ i7^0-i7^post12 == 0), cost: 1 New rule: l16 -> l15 : TRUE, cost: 1 Applied preprocessing Original rule: l14 -> l16 : i7^0'=i7^post13, i13^0'=i13^post13, i^0'=i^post13, i17^0'=i17^post13, i11^0'=i11^post13, tmp___0^0'=tmp___0^post13, i9^0'=i9^post13, i15^0'=i15^post13, tmp^0'=tmp^post13, (i13^10 == 0 /\ i7^0-i7^post13 == 0 /\ i17^0-i17^post13 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ i^0-i^post13 == 0 /\ -i11^post13+i11^0 == 0 /\ -i15^post13+i15^0 == 0 /\ i9^0-i9^post13 == 0 /\ 50-i^0 <= 0 /\ i13^post13 == 0 /\ -tmp^post13+tmp^0 == 0), cost: 1 New rule: l14 -> l16 : i13^0'=0, -50+i^0 >= 0, cost: 1 Applied preprocessing Original rule: l14 -> l13 : i7^0'=i7^post14, i13^0'=i13^post14, i^0'=i^post14, i17^0'=i17^post14, i11^0'=i11^post14, tmp___0^0'=tmp___0^post14, i9^0'=i9^post14, i15^0'=i15^post14, tmp^0'=tmp^post14, (-49+i^0 <= 0 /\ i7^0-i7^post14 == 0 /\ i15^0-i15^post14 == 0 /\ i17^0-i17^post14 == 0 /\ -i11^post14+i11^0 == 0 /\ -i9^post14+i9^0 == 0 /\ -1-i^0+i^post14 == 0 /\ -tmp^post14+tmp^0 == 0 /\ -tmp___0^post14+tmp___0^0 == 0 /\ i13^0-i13^post14 == 0), cost: 1 New rule: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 Applied preprocessing Original rule: l12 -> l11 : i7^0'=i7^post15, i13^0'=i13^post15, i^0'=i^post15, i17^0'=i17^post15, i11^0'=i11^post15, tmp___0^0'=tmp___0^post15, i9^0'=i9^post15, i15^0'=i15^post15, tmp^0'=tmp^post15, (i13^0-i13^post15 == 0 /\ -tmp___0^post15+tmp___0^0 == 0 /\ -i^post15+i^0 == 0 /\ i9^0-i9^post15 == 0 /\ -tmp^post15+tmp^0 == 0 /\ -i11^post15+i11^0 == 0 /\ i7^0-i7^post15 == 0 /\ -i15^post15+i15^0 == 0 /\ i17^0-i17^post15 == 0), cost: 1 New rule: l12 -> l11 : TRUE, cost: 1 Applied preprocessing Original rule: l10 -> l13 : i7^0'=i7^post16, i13^0'=i13^post16, i^0'=i^post16, i17^0'=i17^post16, i11^0'=i11^post16, tmp___0^0'=tmp___0^post16, i9^0'=i9^post16, i15^0'=i15^post16, tmp^0'=tmp^post16, (i^post16 == 0 /\ i11^0-i11^post16 == 0 /\ 50-i11^0 <= 0 /\ tmp___0^0-tmp___0^post16 == 0 /\ -tmp^post16+tmp^0 == 0 /\ -i9^post16+i9^0 == 0 /\ i13^0-i13^post16 == 0 /\ -i17^post16+i17^0 == 0 /\ -i15^post16+i15^0 == 0 /\ i7^0-i7^post16 == 0), cost: 1 New rule: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 Applied preprocessing Original rule: l10 -> l9 : i7^0'=i7^post17, i13^0'=i13^post17, i^0'=i^post17, i17^0'=i17^post17, i11^0'=i11^post17, tmp___0^0'=tmp___0^post17, i9^0'=i9^post17, i15^0'=i15^post17, tmp^0'=tmp^post17, (-1-i11^0+i11^post17 == 0 /\ i13^0-i13^post17 == 0 /\ -tmp^post17+tmp^0 == 0 /\ -i9^post17+i9^0 == 0 /\ i7^0-i7^post17 == 0 /\ tmp___0^0-tmp___0^post17 == 0 /\ i17^0-i17^post17 == 0 /\ -49+i11^0 <= 0 /\ i^0-i^post17 == 0 /\ -i15^post17+i15^0 == 0), cost: 1 New rule: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 Applied preprocessing Original rule: l8 -> l7 : i7^0'=i7^post18, i13^0'=i13^post18, i^0'=i^post18, i17^0'=i17^post18, i11^0'=i11^post18, tmp___0^0'=tmp___0^post18, i9^0'=i9^post18, i15^0'=i15^post18, tmp^0'=tmp^post18, (-i11^post18+i11^0 == 0 /\ -i15^post18+i15^0 == 0 /\ -i9^post18+i9^0 == 0 /\ -tmp^post18+tmp^0 == 0 /\ i7^0-i7^post18 == 0 /\ i^0-i^post18 == 0 /\ i17^0-i17^post18 == 0 /\ -i13^post18+i13^0 == 0 /\ -tmp___0^post18+tmp___0^0 == 0), cost: 1 New rule: l8 -> l7 : TRUE, cost: 1 Applied preprocessing Original rule: l6 -> l9 : i7^0'=i7^post19, i13^0'=i13^post19, i^0'=i^post19, i17^0'=i17^post19, i11^0'=i11^post19, tmp___0^0'=tmp___0^post19, i9^0'=i9^post19, i15^0'=i15^post19, tmp^0'=tmp^post19, (i13^0-i13^post19 == 0 /\ i11^10 == 0 /\ -i^post19+i^0 == 0 /\ tmp___0^0-tmp___0^post19 == 0 /\ -i9^post19+i9^0 == 0 /\ -tmp^post19+tmp^0 == 0 /\ i7^0-i7^post19 == 0 /\ 50-i9^0 <= 0 /\ i11^post19 == 0 /\ -i17^post19+i17^0 == 0 /\ -i15^post19+i15^0 == 0), cost: 1 New rule: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 Applied preprocessing Original rule: l6 -> l5 : i7^0'=i7^post20, i13^0'=i13^post20, i^0'=i^post20, i17^0'=i17^post20, i11^0'=i11^post20, tmp___0^0'=tmp___0^post20, i9^0'=i9^post20, i15^0'=i15^post20, tmp^0'=tmp^post20, (-1+i9^post20-i9^0 == 0 /\ i11^0-i11^post20 == 0 /\ tmp___0^0-tmp___0^post20 == 0 /\ i7^0-i7^post20 == 0 /\ -i^post20+i^0 == 0 /\ -49+i9^0 <= 0 /\ -i15^post20+i15^0 == 0 /\ -tmp^post20+tmp^0 == 0 /\ i13^0-i13^post20 == 0 /\ -i17^post20+i17^0 == 0), cost: 1 New rule: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 Applied preprocessing Original rule: l4 -> l2 : i7^0'=i7^post21, i13^0'=i13^post21, i^0'=i^post21, i17^0'=i17^post21, i11^0'=i11^post21, tmp___0^0'=tmp___0^post21, i9^0'=i9^post21, i15^0'=i15^post21, tmp^0'=tmp^post21, (-tmp^post21+tmp^0 == 0 /\ -i9^post21+i9^0 == 0 /\ -i15^post21+i15^0 == 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ -i17^post21+i17^0 == 0 /\ i13^0-i13^post21 == 0 /\ i11^0-i11^post21 == 0 /\ i7^0-i7^post21 == 0 /\ i^0-i^post21 == 0), cost: 1 New rule: l4 -> l2 : TRUE, cost: 1 Applied preprocessing Original rule: l1 -> l5 : i7^0'=i7^post22, i13^0'=i13^post22, i^0'=i^post22, i17^0'=i17^post22, i11^0'=i11^post22, tmp___0^0'=tmp___0^post22, i9^0'=i9^post22, i15^0'=i15^post22, tmp^0'=tmp^post22, (i9^10 == 0 /\ i7^0-i7^post22 == 0 /\ i17^0-i17^post22 == 0 /\ -tmp___0^post22+tmp___0^0 == 0 /\ 50-i7^0 <= 0 /\ i^0-i^post22 == 0 /\ -i11^post22+i11^0 == 0 /\ -tmp^post22+tmp^0 == 0 /\ -i15^post22+i15^0 == 0 /\ i13^0-i13^post22 == 0 /\ i9^post22 == 0), cost: 1 New rule: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 Applied preprocessing Original rule: l1 -> l0 : i7^0'=i7^post23, i13^0'=i13^post23, i^0'=i^post23, i17^0'=i17^post23, i11^0'=i11^post23, tmp___0^0'=tmp___0^post23, i9^0'=i9^post23, i15^0'=i15^post23, tmp^0'=tmp^post23, (-i11^post23+i11^0 == 0 /\ i15^0-i15^post23 == 0 /\ i17^0-i17^post23 == 0 /\ -tmp^post23+tmp^0 == 0 /\ -1-i7^0+i7^post23 == 0 /\ i13^0-i13^post23 == 0 /\ i9^0-i9^post23 == 0 /\ -49+i7^0 <= 0 /\ -tmp___0^post23+tmp___0^0 == 0 /\ i^0-i^post23 == 0), cost: 1 New rule: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 Applied preprocessing Original rule: l17 -> l0 : i7^0'=i7^post24, i13^0'=i13^post24, i^0'=i^post24, i17^0'=i17^post24, i11^0'=i11^post24, tmp___0^0'=tmp___0^post24, i9^0'=i9^post24, i15^0'=i15^post24, tmp^0'=tmp^post24, (0 == 0 /\ i13^0-i13^post24 == 0 /\ i7^10 == 0 /\ i^post24 == 0 /\ i9^0-i9^post24 == 0 /\ -i15^post24+i15^0 == 0 /\ i7^post24 == 0 /\ i17^0-i17^post24 == 0 /\ -i11^post24+i11^0 == 0), cost: 1 New rule: l17 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 1 Applied preprocessing Original rule: l18 -> l17 : i7^0'=i7^post25, i13^0'=i13^post25, i^0'=i^post25, i17^0'=i17^post25, i11^0'=i11^post25, tmp___0^0'=tmp___0^post25, i9^0'=i9^post25, i15^0'=i15^post25, tmp^0'=tmp^post25, (-i15^post25+i15^0 == 0 /\ i11^0-i11^post25 == 0 /\ tmp___0^0-tmp___0^post25 == 0 /\ -tmp^post25+tmp^0 == 0 /\ i13^0-i13^post25 == 0 /\ -i9^post25+i9^0 == 0 /\ -i17^post25+i17^0 == 0 /\ i7^0-i7^post25 == 0 /\ i^0-i^post25 == 0), cost: 1 New rule: l18 -> l17 : TRUE, cost: 1 Simplified rules Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 27: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 46: l4 -> l2 : TRUE, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 29: l7 -> l4 : i^0'=0, -50+i17^0 >= 0, cost: 1 30: l7 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 1 43: l8 -> l7 : TRUE, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 32: l11 -> l8 : i17^0'=0, -50+i15^0 >= 0, cost: 1 33: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1 40: l12 -> l11 : TRUE, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, -50+i^0 >= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, -50+i13^0 >= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 49: l17 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 1 50: l18 -> l17 : TRUE, cost: 1 Eliminating location l17 by chaining: Applied chaining First rule: l18 -> l17 : TRUE, cost: 1 Second rule: l17 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 1 New rule: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Applied deletion Removed the following rules: 49 50 Eliminating location l2 by chaining: Applied chaining First rule: l4 -> l2 : TRUE, cost: 1 Second rule: l2 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 New rule: l4 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 2 Applied deletion Removed the following rules: 27 46 Eliminated locations on linear paths Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 52: l4 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 2 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 29: l7 -> l4 : i^0'=0, -50+i17^0 >= 0, cost: 1 30: l7 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 1 43: l8 -> l7 : TRUE, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 32: l11 -> l8 : i17^0'=0, -50+i15^0 >= 0, cost: 1 33: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1 40: l12 -> l11 : TRUE, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, -50+i^0 >= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, -50+i13^0 >= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Applied acceleration Original rule: l4 -> l4 : i^0'=1+i^0, -49+i^0 <= 0, cost: 2 New rule: l4 -> l4 : i^0'=i^0+n, (50-i^0-n >= 0 /\ n >= 0), cost: 2*n Sub-proof via acceration calculus written to file:///tmp/tmpnam_aCeieg.txt Applied instantiation Original rule: l4 -> l4 : i^0'=i^0+n, (50-i^0-n >= 0 /\ n >= 0), cost: 2*n New rule: l4 -> l4 : i^0'=50, (0 >= 0 /\ 50-i^0 >= 0), cost: 100-2*i^0 Applied simplification Original rule: l4 -> l4 : i^0'=50, (0 >= 0 /\ 50-i^0 >= 0), cost: 100-2*i^0 New rule: l4 -> l4 : i^0'=50, -50+i^0 <= 0, cost: 100-2*i^0 Applied deletion Removed the following rules: 52 Accelerated simple loops Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 54: l4 -> l4 : i^0'=50, -50+i^0 <= 0, cost: 100-2*i^0 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 29: l7 -> l4 : i^0'=0, -50+i17^0 >= 0, cost: 1 30: l7 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 1 43: l8 -> l7 : TRUE, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 32: l11 -> l8 : i17^0'=0, -50+i15^0 >= 0, cost: 1 33: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1 40: l12 -> l11 : TRUE, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, -50+i^0 >= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, -50+i13^0 >= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Applied chaining First rule: l7 -> l4 : i^0'=0, -50+i17^0 >= 0, cost: 1 Second rule: l4 -> l4 : i^0'=50, -50+i^0 <= 0, cost: 100-2*i^0 New rule: l7 -> l4 : i^0'=50, -50+i17^0 >= 0, cost: 101 Applied deletion Removed the following rules: 54 Chained accelerated rules with incoming rules Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 29: l7 -> l4 : i^0'=0, -50+i17^0 >= 0, cost: 1 30: l7 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 1 55: l7 -> l4 : i^0'=50, -50+i17^0 >= 0, cost: 101 43: l8 -> l7 : TRUE, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 32: l11 -> l8 : i17^0'=0, -50+i15^0 >= 0, cost: 1 33: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1 40: l12 -> l11 : TRUE, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, -50+i^0 >= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, -50+i13^0 >= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 30: l7 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 1 43: l8 -> l7 : TRUE, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 32: l11 -> l8 : i17^0'=0, -50+i15^0 >= 0, cost: 1 33: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1 40: l12 -> l11 : TRUE, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, -50+i^0 >= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, -50+i13^0 >= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Eliminating location l7 by chaining: Applied chaining First rule: l8 -> l7 : TRUE, cost: 1 Second rule: l7 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 1 New rule: l8 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 2 Applied deletion Removed the following rules: 30 43 Eliminated locations on linear paths Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 56: l8 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 2 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 32: l11 -> l8 : i17^0'=0, -50+i15^0 >= 0, cost: 1 33: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1 40: l12 -> l11 : TRUE, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, -50+i^0 >= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, -50+i13^0 >= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Applied acceleration Original rule: l8 -> l8 : i17^0'=1+i17^0, -49+i17^0 <= 0, cost: 2 New rule: l8 -> l8 : i17^0'=i17^0+n0, (50-i17^0-n0 >= 0 /\ n0 >= 0), cost: 2*n0 Sub-proof via acceration calculus written to file:///tmp/tmpnam_oOApGO.txt Applied instantiation Original rule: l8 -> l8 : i17^0'=i17^0+n0, (50-i17^0-n0 >= 0 /\ n0 >= 0), cost: 2*n0 New rule: l8 -> l8 : i17^0'=50, (0 >= 0 /\ 50-i17^0 >= 0), cost: 100-2*i17^0 Applied simplification Original rule: l8 -> l8 : i17^0'=50, (0 >= 0 /\ 50-i17^0 >= 0), cost: 100-2*i17^0 New rule: l8 -> l8 : i17^0'=50, -50+i17^0 <= 0, cost: 100-2*i17^0 Applied deletion Removed the following rules: 56 Accelerated simple loops Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 58: l8 -> l8 : i17^0'=50, -50+i17^0 <= 0, cost: 100-2*i17^0 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 32: l11 -> l8 : i17^0'=0, -50+i15^0 >= 0, cost: 1 33: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1 40: l12 -> l11 : TRUE, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, -50+i^0 >= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, -50+i13^0 >= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Applied chaining First rule: l11 -> l8 : i17^0'=0, -50+i15^0 >= 0, cost: 1 Second rule: l8 -> l8 : i17^0'=50, -50+i17^0 <= 0, cost: 100-2*i17^0 New rule: l11 -> l8 : i17^0'=50, -50+i15^0 >= 0, cost: 101 Applied deletion Removed the following rules: 58 Chained accelerated rules with incoming rules Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 32: l11 -> l8 : i17^0'=0, -50+i15^0 >= 0, cost: 1 33: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1 59: l11 -> l8 : i17^0'=50, -50+i15^0 >= 0, cost: 101 40: l12 -> l11 : TRUE, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, -50+i^0 >= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, -50+i13^0 >= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 33: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1 40: l12 -> l11 : TRUE, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, -50+i^0 >= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, -50+i13^0 >= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Eliminating location l11 by chaining: Applied chaining First rule: l12 -> l11 : TRUE, cost: 1 Second rule: l11 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 1 New rule: l12 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 2 Applied deletion Removed the following rules: 33 40 Eliminated locations on linear paths Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 60: l12 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 2 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, -50+i^0 >= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, -50+i13^0 >= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Applied acceleration Original rule: l12 -> l12 : i15^0'=1+i15^0, -49+i15^0 <= 0, cost: 2 New rule: l12 -> l12 : i15^0'=n1+i15^0, (n1 >= 0 /\ 50-n1-i15^0 >= 0), cost: 2*n1 Sub-proof via acceration calculus written to file:///tmp/tmpnam_AeoJeL.txt Applied instantiation Original rule: l12 -> l12 : i15^0'=n1+i15^0, (n1 >= 0 /\ 50-n1-i15^0 >= 0), cost: 2*n1 New rule: l12 -> l12 : i15^0'=50, (0 >= 0 /\ 50-i15^0 >= 0), cost: 100-2*i15^0 Applied simplification Original rule: l12 -> l12 : i15^0'=50, (0 >= 0 /\ 50-i15^0 >= 0), cost: 100-2*i15^0 New rule: l12 -> l12 : i15^0'=50, -50+i15^0 <= 0, cost: 100-2*i15^0 Applied deletion Removed the following rules: 60 Accelerated simple loops Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 62: l12 -> l12 : i15^0'=50, -50+i15^0 <= 0, cost: 100-2*i15^0 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, -50+i^0 >= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, -50+i13^0 >= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Applied chaining First rule: l15 -> l12 : i15^0'=0, -50+i13^0 >= 0, cost: 1 Second rule: l12 -> l12 : i15^0'=50, -50+i15^0 <= 0, cost: 100-2*i15^0 New rule: l15 -> l12 : i15^0'=50, -50+i13^0 >= 0, cost: 101 Applied deletion Removed the following rules: 62 Chained accelerated rules with incoming rules Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, -50+i^0 >= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 35: l15 -> l12 : i15^0'=0, -50+i13^0 >= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 63: l15 -> l12 : i15^0'=50, -50+i13^0 >= 0, cost: 101 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, -50+i^0 >= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 36: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 37: l16 -> l15 : TRUE, cost: 1 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Eliminating location l15 by chaining: Applied chaining First rule: l16 -> l15 : TRUE, cost: 1 Second rule: l15 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 1 New rule: l16 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 2 Applied deletion Removed the following rules: 36 37 Eliminated locations on linear paths Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, -50+i^0 >= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 64: l16 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 2 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Applied acceleration Original rule: l16 -> l16 : i13^0'=1+i13^0, -49+i13^0 <= 0, cost: 2 New rule: l16 -> l16 : i13^0'=i13^0+n2, (n2 >= 0 /\ 50-i13^0-n2 >= 0), cost: 2*n2 Sub-proof via acceration calculus written to file:///tmp/tmpnam_lOkEdn.txt Applied instantiation Original rule: l16 -> l16 : i13^0'=i13^0+n2, (n2 >= 0 /\ 50-i13^0-n2 >= 0), cost: 2*n2 New rule: l16 -> l16 : i13^0'=50, (0 >= 0 /\ 50-i13^0 >= 0), cost: 100-2*i13^0 Applied simplification Original rule: l16 -> l16 : i13^0'=50, (0 >= 0 /\ 50-i13^0 >= 0), cost: 100-2*i13^0 New rule: l16 -> l16 : i13^0'=50, -50+i13^0 <= 0, cost: 100-2*i13^0 Applied deletion Removed the following rules: 64 Accelerated simple loops Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, -50+i^0 >= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 66: l16 -> l16 : i13^0'=50, -50+i13^0 <= 0, cost: 100-2*i13^0 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Applied chaining First rule: l14 -> l16 : i13^0'=0, -50+i^0 >= 0, cost: 1 Second rule: l16 -> l16 : i13^0'=50, -50+i13^0 <= 0, cost: 100-2*i13^0 New rule: l14 -> l16 : i13^0'=50, -50+i^0 >= 0, cost: 101 Applied deletion Removed the following rules: 66 Chained accelerated rules with incoming rules Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 34: l13 -> l14 : TRUE, cost: 1 38: l14 -> l16 : i13^0'=0, -50+i^0 >= 0, cost: 1 39: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 67: l14 -> l16 : i13^0'=50, -50+i^0 >= 0, cost: 101 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 34: l13 -> l14 : TRUE, cost: 1 39: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Eliminating location l14 by chaining: Applied chaining First rule: l13 -> l14 : TRUE, cost: 1 Second rule: l14 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 1 New rule: l13 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 2 Applied deletion Removed the following rules: 34 39 Eliminated locations on linear paths Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 68: l13 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 2 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Applied acceleration Original rule: l13 -> l13 : i^0'=1+i^0, -49+i^0 <= 0, cost: 2 New rule: l13 -> l13 : i^0'=n3+i^0, (50-n3-i^0 >= 0 /\ n3 >= 0), cost: 2*n3 Sub-proof via acceration calculus written to file:///tmp/tmpnam_dJonLF.txt Applied instantiation Original rule: l13 -> l13 : i^0'=n3+i^0, (50-n3-i^0 >= 0 /\ n3 >= 0), cost: 2*n3 New rule: l13 -> l13 : i^0'=50, (0 >= 0 /\ 50-i^0 >= 0), cost: 100-2*i^0 Applied simplification Original rule: l13 -> l13 : i^0'=50, (0 >= 0 /\ 50-i^0 >= 0), cost: 100-2*i^0 New rule: l13 -> l13 : i^0'=50, -50+i^0 <= 0, cost: 100-2*i^0 Applied deletion Removed the following rules: 68 Accelerated simple loops Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 70: l13 -> l13 : i^0'=50, -50+i^0 <= 0, cost: 100-2*i^0 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Applied chaining First rule: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 Second rule: l13 -> l13 : i^0'=50, -50+i^0 <= 0, cost: 100-2*i^0 New rule: l10 -> l13 : i^0'=50, -50+i11^0 >= 0, cost: 101 Applied deletion Removed the following rules: 70 Chained accelerated rules with incoming rules Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 41: l10 -> l13 : i^0'=0, -50+i11^0 >= 0, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 71: l10 -> l13 : i^0'=50, -50+i11^0 >= 0, cost: 101 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 31: l9 -> l10 : TRUE, cost: 1 42: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Eliminating location l10 by chaining: Applied chaining First rule: l9 -> l10 : TRUE, cost: 1 Second rule: l10 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 1 New rule: l9 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 2 Applied deletion Removed the following rules: 31 42 Eliminated locations on linear paths Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 72: l9 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 2 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Applied acceleration Original rule: l9 -> l9 : i11^0'=1+i11^0, -49+i11^0 <= 0, cost: 2 New rule: l9 -> l9 : i11^0'=i11^0+n4, (n4 >= 0 /\ 50-i11^0-n4 >= 0), cost: 2*n4 Sub-proof via acceration calculus written to file:///tmp/tmpnam_fMHhel.txt Applied instantiation Original rule: l9 -> l9 : i11^0'=i11^0+n4, (n4 >= 0 /\ 50-i11^0-n4 >= 0), cost: 2*n4 New rule: l9 -> l9 : i11^0'=50, (0 >= 0 /\ 50-i11^0 >= 0), cost: 100-2*i11^0 Applied simplification Original rule: l9 -> l9 : i11^0'=50, (0 >= 0 /\ 50-i11^0 >= 0), cost: 100-2*i11^0 New rule: l9 -> l9 : i11^0'=50, -50+i11^0 <= 0, cost: 100-2*i11^0 Applied deletion Removed the following rules: 72 Accelerated simple loops Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 74: l9 -> l9 : i11^0'=50, -50+i11^0 <= 0, cost: 100-2*i11^0 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Applied chaining First rule: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 Second rule: l9 -> l9 : i11^0'=50, -50+i11^0 <= 0, cost: 100-2*i11^0 New rule: l6 -> l9 : i11^0'=50, -50+i9^0 >= 0, cost: 101 Applied deletion Removed the following rules: 74 Chained accelerated rules with incoming rules Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 44: l6 -> l9 : i11^0'=0, -50+i9^0 >= 0, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 75: l6 -> l9 : i11^0'=50, -50+i9^0 >= 0, cost: 101 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 28: l5 -> l6 : TRUE, cost: 1 45: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Eliminating location l6 by chaining: Applied chaining First rule: l5 -> l6 : TRUE, cost: 1 Second rule: l6 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 1 New rule: l5 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 2 Applied deletion Removed the following rules: 28 45 Eliminated locations on linear paths Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 76: l5 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 2 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Applied acceleration Original rule: l5 -> l5 : i9^0'=1+i9^0, -49+i9^0 <= 0, cost: 2 New rule: l5 -> l5 : i9^0'=i9^0+n5, (50-i9^0-n5 >= 0 /\ n5 >= 0), cost: 2*n5 Sub-proof via acceration calculus written to file:///tmp/tmpnam_AincFE.txt Applied instantiation Original rule: l5 -> l5 : i9^0'=i9^0+n5, (50-i9^0-n5 >= 0 /\ n5 >= 0), cost: 2*n5 New rule: l5 -> l5 : i9^0'=50, (0 >= 0 /\ 50-i9^0 >= 0), cost: 100-2*i9^0 Applied simplification Original rule: l5 -> l5 : i9^0'=50, (0 >= 0 /\ 50-i9^0 >= 0), cost: 100-2*i9^0 New rule: l5 -> l5 : i9^0'=50, -50+i9^0 <= 0, cost: 100-2*i9^0 Applied deletion Removed the following rules: 76 Accelerated simple loops Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 78: l5 -> l5 : i9^0'=50, -50+i9^0 <= 0, cost: 100-2*i9^0 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Applied chaining First rule: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 Second rule: l5 -> l5 : i9^0'=50, -50+i9^0 <= 0, cost: 100-2*i9^0 New rule: l1 -> l5 : i9^0'=50, -50+i7^0 >= 0, cost: 101 Applied deletion Removed the following rules: 78 Chained accelerated rules with incoming rules Start location: l18 26: l0 -> l1 : TRUE, cost: 1 47: l1 -> l5 : i9^0'=0, -50+i7^0 >= 0, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 79: l1 -> l5 : i9^0'=50, -50+i7^0 >= 0, cost: 101 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l18 26: l0 -> l1 : TRUE, cost: 1 48: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Eliminating location l1 by chaining: Applied chaining First rule: l0 -> l1 : TRUE, cost: 1 Second rule: l1 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 1 New rule: l0 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 2 Applied deletion Removed the following rules: 26 48 Eliminated locations on linear paths Start location: l18 80: l0 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 2 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Applied acceleration Original rule: l0 -> l0 : i7^0'=1+i7^0, -49+i7^0 <= 0, cost: 2 New rule: l0 -> l0 : i7^0'=i7^0+n6, (50-i7^0-n6 >= 0 /\ n6 >= 0), cost: 2*n6 Sub-proof via acceration calculus written to file:///tmp/tmpnam_gJMpkA.txt Applied instantiation Original rule: l0 -> l0 : i7^0'=i7^0+n6, (50-i7^0-n6 >= 0 /\ n6 >= 0), cost: 2*n6 New rule: l0 -> l0 : i7^0'=50, (0 >= 0 /\ 50-i7^0 >= 0), cost: 100-2*i7^0 Applied simplification Original rule: l0 -> l0 : i7^0'=50, (0 >= 0 /\ 50-i7^0 >= 0), cost: 100-2*i7^0 New rule: l0 -> l0 : i7^0'=50, -50+i7^0 <= 0, cost: 100-2*i7^0 Applied deletion Removed the following rules: 80 Accelerated simple loops Start location: l18 82: l0 -> l0 : i7^0'=50, -50+i7^0 <= 0, cost: 100-2*i7^0 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Applied chaining First rule: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 Second rule: l0 -> l0 : i7^0'=50, -50+i7^0 <= 0, cost: 100-2*i7^0 New rule: l18 -> l0 : i7^0'=50, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, (0 == 0 /\ -50 <= 0), cost: 102 Applied deletion Removed the following rules: 82 Chained accelerated rules with incoming rules Start location: l18 51: l18 -> l0 : i7^0'=0, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, 0 == 0, cost: 2 83: l18 -> l0 : i7^0'=50, i^0'=0, tmp___0^0'=tmp___0^post24, tmp^0'=tmp^post24, (0 == 0 /\ -50 <= 0), cost: 102 Removed unreachable locations and irrelevant leafs Start location: l18 Computing asymptotic complexity Proved the following lower bound Complexity: Unknown Cpx degree: ? Solved cost: 0 Rule cost: 0