NO Initial ITS Start location: l11 0: l0 -> l1 : e^0'=e^post0, b^0'=b^post0, d^0'=d^post0, a^0'=a^post0, c^0'=c^post0, (b^20-b^10 == 0 /\ d^post0-d^30 == 0 /\ -e^10+e^20 == 0 /\ a^30-a^20 == 0 /\ e^post0-e^30 == 0 /\ -a^0+a^10 == 0 /\ e^30-e^20 == 0 /\ d^10-d^0 == 0 /\ c^30-c^20 == 0 /\ -c^30+c^post0 == 0 /\ c^10-c^0 == 0 /\ -d^10+d^20 == 0 /\ d^30-d^20 == 0 /\ -b^0+b^10 == 0 /\ -a^10+a^20 == 0 /\ -b^30+b^post0 == 0 /\ -e^0 <= 0 /\ -e^0+e^10 == 0 /\ -b^20+b^30 == 0 /\ c^20-c^10 == 0 /\ -a^30+a^post0 == 0), cost: 1 1: l0 -> l2 : e^0'=e^post1, b^0'=b^post1, d^0'=d^post1, a^0'=a^post1, c^0'=c^post1, (1+e^0 <= 0 /\ -e^0+e^post1 == 0 /\ -b^0+b^post1 == 0 /\ c^post1-c^0 == 0 /\ a^post1-a^0 == 0 /\ -d^0+d^post1 == 0), cost: 1 6: l2 -> l5 : e^0'=e^post6, b^0'=b^post6, d^0'=d^post6, a^0'=a^post6, c^0'=c^post6, (-b^0+b^post6 == 0 /\ -e^0+e^post6 == 0 /\ -a^0+a^post6 == 0 /\ -d^0+d^post6 == 0 /\ c^post6-c^0 == 0 /\ -a^0 <= 0), cost: 1 7: l2 -> l6 : e^0'=e^post7, b^0'=b^post7, d^0'=d^post7, a^0'=a^post7, c^0'=c^post7, (1+a^0 <= 0 /\ -c^0+c^110 == 0 /\ -d^310+d^post7 == 0 /\ d^310-d^210 == 0 /\ -b^210+b^310+a^210 == 0 /\ a^post7-a^310 == 0 /\ -c^210+c^310 == 0 /\ -a^0+a^11 == 0 /\ a^210+a^11 == 0 /\ e^210-e^110 == 0 /\ -b^0+b^110 == 0 /\ d^110-d^0 == 0 /\ b^post7-b^310 == 0 /\ c^210-c^110 == 0 /\ e^310-e^210 == 0 /\ -e^310+e^post7+a^310 == 0 /\ -d^110+d^210 == 0 /\ -e^0+e^110 == 0 /\ -a^210+a^310 == 0 /\ c^post7-c^310 == 0 /\ b^210-b^110 == 0), cost: 1 2: l3 -> l0 : e^0'=e^post2, b^0'=b^post2, d^0'=d^post2, a^0'=a^post2, c^0'=c^post2, (b^post2-b^0 == 0 /\ c^post2-c^0 == 0 /\ -a^0+a^post2 == 0 /\ -d^0+d^post2 == 0 /\ -e^0+e^post2 == 0 /\ d^0-c^0 <= 0), cost: 1 3: l3 -> l2 : e^0'=e^post3, b^0'=b^post3, d^0'=d^post3, a^0'=a^post3, c^0'=c^post3, (-b^0+b^post3 == 0 /\ -e^0+e^post3 == 0 /\ d^post3-d^0 == 0 /\ c^post3-c^0 == 0 /\ a^post3-a^0 == 0 /\ 1-d^0+c^0 <= 0), cost: 1 4: l4 -> l3 : e^0'=e^post4, b^0'=b^post4, d^0'=d^post4, a^0'=a^post4, c^0'=c^post4, (-b^0+b^post4 == 0 /\ -e^0+e^post4 == 0 /\ -a^0+a^post4 == 0 /\ -d^0+d^post4 == 0 /\ -b^0 <= 0 /\ c^post4-c^0 == 0), cost: 1 5: l4 -> l2 : e^0'=e^post5, b^0'=b^post5, d^0'=d^post5, a^0'=a^post5, c^0'=c^post5, (-e^0+e^post5 == 0 /\ 1+b^0 <= 0 /\ c^post5-c^0 == 0 /\ -d^0+d^post5 == 0 /\ a^post5-a^0 == 0 /\ -b^0+b^post5 == 0), cost: 1 16: l5 -> l10 : e^0'=e^post16, b^0'=b^post16, d^0'=d^post16, a^0'=a^post16, c^0'=c^post16, (a^post16-a^0 == 0 /\ -b^0+b^post16 == 0 /\ -b^0 <= 0 /\ -e^0+e^post16 == 0 /\ -d^0+d^post16 == 0 /\ c^post16-c^0 == 0), cost: 1 17: l5 -> l6 : e^0'=e^post17, b^0'=b^post17, d^0'=d^post17, a^0'=a^post17, c^0'=c^post17, (d^post17-d^350 == 0 /\ -d^0+d^150 == 0 /\ -a^0+a^15 == 0 /\ b^250+b^150 == 0 /\ -e^0+e^150 == 0 /\ e^post17-e^350 == 0 /\ -a^350+a^post17 == 0 /\ a^350-a^250+b^350 == 0 /\ -b^350+b^post17 == 0 /\ 1+b^0 <= 0 /\ -b^0+b^150 == 0 /\ -b^250+b^350 == 0 /\ e^250-e^150 == 0 /\ c^350-c^250 == 0 /\ d^250-d^150 == 0 /\ -c^350+b^350+c^post17 == 0 /\ -e^250+e^350 == 0 /\ a^250-a^15 == 0 /\ -d^250+d^350 == 0 /\ -c^150+c^250 == 0 /\ c^150-c^0 == 0), cost: 1 18: l6 -> l8 : e^0'=e^post18, b^0'=b^post18, d^0'=d^post18, a^0'=a^post18, c^0'=c^post18, (-e^0+e^post18 == 0 /\ -b^0+b^post18 == 0 /\ c^post18-c^0 == 0 /\ -d^0+d^post18 == 0 /\ a^post18-a^0 == 0), cost: 1 8: l7 -> l6 : e^0'=e^post8, b^0'=b^post8, d^0'=d^post8, a^0'=a^post8, c^0'=c^post8, (-e^0+e^post8 == 0 /\ -a^0+a^post8 == 0 /\ b^post8-b^0 == 0 /\ c^post8-c^0 == 0 /\ -d^0+d^post8 == 0 /\ -e^0 <= 0), cost: 1 9: l7 -> l6 : e^0'=e^post9, b^0'=b^post9, d^0'=d^post9, a^0'=a^post9, c^0'=c^post9, (-d^120+d^220 == 0 /\ -a^12+a^220 == 0 /\ -e^0+e^120 == 0 /\ 1+e^0 <= 0 /\ c^220-c^120 == 0 /\ c^320-c^220 == 0 /\ -b^120+b^220 == 0 /\ b^120-b^0 == 0 /\ -c^0+c^120 == 0 /\ e^220+e^120 == 0 /\ d^120-d^0 == 0 /\ e^post9-e^320 == 0 /\ a^12-a^0 == 0 /\ e^post9-a^320+a^post9 == 0 /\ -c^320+c^post9 == 0 /\ -b^320+b^post9 == 0 /\ -d^320+d^post9 == 0 /\ -b^220+b^320 == 0 /\ -e^220+e^320 == 0 /\ d^320+e^320-d^220 == 0 /\ a^320-a^220 == 0), cost: 1 10: l8 -> l4 : e^0'=e^post10, b^0'=b^post10, d^0'=d^post10, a^0'=a^post10, c^0'=c^post10, (c^post10-c^0 == 0 /\ -a^0+a^post10 == 0 /\ -d^0+d^post10 == 0 /\ e^post10-e^0 == 0 /\ -a^0 <= 0 /\ -b^0+b^post10 == 0), cost: 1 11: l8 -> l2 : e^0'=e^post11, b^0'=b^post11, d^0'=d^post11, a^0'=a^post11, c^0'=c^post11, (1+a^0 <= 0 /\ a^post11-a^0 == 0 /\ -c^0+c^post11 == 0 /\ -b^0+b^post11 == 0 /\ -e^0+e^post11 == 0 /\ d^post11-d^0 == 0), cost: 1 12: l9 -> l7 : e^0'=e^post12, b^0'=b^post12, d^0'=d^post12, a^0'=a^post12, c^0'=c^post12, (-d^0 <= 0 /\ -d^0+d^post12 == 0 /\ c^post12-c^0 == 0 /\ -b^0+b^post12 == 0 /\ a^post12-a^0 == 0 /\ -e^0+e^post12 == 0), cost: 1 13: l9 -> l6 : e^0'=e^post13, b^0'=b^post13, d^0'=d^post13, a^0'=a^post13, c^0'=c^post13, (b^post13-b^330 == 0 /\ -e^0+e^130 == 0 /\ d^330-e^330+e^post13 == 0 /\ -b^0+b^130 == 0 /\ a^230-a^13 == 0 /\ c^230-c^130 == 0 /\ b^230-b^130 == 0 /\ -a^0+a^13 == 0 /\ d^330-d^230 == 0 /\ -d^330+d^post13 == 0 /\ -a^330+a^post13 == 0 /\ c^130-c^0 == 0 /\ d^330-c^230+c^330 == 0 /\ e^230-e^130 == 0 /\ -c^330+c^post13 == 0 /\ -b^230+b^330 == 0 /\ -d^0+d^130 == 0 /\ -e^230+e^330 == 0 /\ d^230+d^130 == 0 /\ 1+d^0 <= 0 /\ -a^230+a^330 == 0), cost: 1 14: l10 -> l9 : e^0'=e^post14, b^0'=b^post14, d^0'=d^post14, a^0'=a^post14, c^0'=c^post14, (-a^0+a^post14 == 0 /\ c^post14-c^0 == 0 /\ -d^0+d^post14 == 0 /\ -c^0 <= 0 /\ -b^0+b^post14 == 0 /\ -e^0+e^post14 == 0), cost: 1 15: l10 -> l6 : e^0'=e^post15, b^0'=b^post15, d^0'=d^post15, a^0'=a^post15, c^0'=c^post15, (c^340+d^post15-d^340 == 0 /\ e^post15-e^340 == 0 /\ e^340-e^240 == 0 /\ -d^240+d^340 == 0 /\ -a^240+a^340 == 0 /\ -e^0+e^140 == 0 /\ -c^240+c^340 == 0 /\ -a^0+a^14 == 0 /\ -e^140+e^240 == 0 /\ d^140-d^0 == 0 /\ a^post15-a^340 == 0 /\ c^140-c^0 == 0 /\ -b^0+b^140 == 0 /\ a^240-a^14 == 0 /\ -c^340+c^post15 == 0 /\ 1+c^0 <= 0 /\ c^240+c^140 == 0 /\ -b^340+b^post15 == 0 /\ -d^140+d^240 == 0 /\ b^240-b^140 == 0 /\ -b^240+b^340+c^340 == 0), cost: 1 19: l11 -> l6 : e^0'=e^post19, b^0'=b^post19, d^0'=d^post19, a^0'=a^post19, c^0'=c^post19, (a^0-a^post19 == 0 /\ d^0-d^post19 == 0 /\ b^0-b^post19 == 0 /\ e^0-e^post19 == 0 /\ -c^post19+c^0 == 0), cost: 1 Removed unreachable rules and leafs Start location: l11 1: l0 -> l2 : e^0'=e^post1, b^0'=b^post1, d^0'=d^post1, a^0'=a^post1, c^0'=c^post1, (1+e^0 <= 0 /\ -e^0+e^post1 == 0 /\ -b^0+b^post1 == 0 /\ c^post1-c^0 == 0 /\ a^post1-a^0 == 0 /\ -d^0+d^post1 == 0), cost: 1 6: l2 -> l5 : e^0'=e^post6, b^0'=b^post6, d^0'=d^post6, a^0'=a^post6, c^0'=c^post6, (-b^0+b^post6 == 0 /\ -e^0+e^post6 == 0 /\ -a^0+a^post6 == 0 /\ -d^0+d^post6 == 0 /\ c^post6-c^0 == 0 /\ -a^0 <= 0), cost: 1 7: l2 -> l6 : e^0'=e^post7, b^0'=b^post7, d^0'=d^post7, a^0'=a^post7, c^0'=c^post7, (1+a^0 <= 0 /\ -c^0+c^110 == 0 /\ -d^310+d^post7 == 0 /\ d^310-d^210 == 0 /\ -b^210+b^310+a^210 == 0 /\ a^post7-a^310 == 0 /\ -c^210+c^310 == 0 /\ -a^0+a^11 == 0 /\ a^210+a^11 == 0 /\ e^210-e^110 == 0 /\ -b^0+b^110 == 0 /\ d^110-d^0 == 0 /\ b^post7-b^310 == 0 /\ c^210-c^110 == 0 /\ e^310-e^210 == 0 /\ -e^310+e^post7+a^310 == 0 /\ -d^110+d^210 == 0 /\ -e^0+e^110 == 0 /\ -a^210+a^310 == 0 /\ c^post7-c^310 == 0 /\ b^210-b^110 == 0), cost: 1 2: l3 -> l0 : e^0'=e^post2, b^0'=b^post2, d^0'=d^post2, a^0'=a^post2, c^0'=c^post2, (b^post2-b^0 == 0 /\ c^post2-c^0 == 0 /\ -a^0+a^post2 == 0 /\ -d^0+d^post2 == 0 /\ -e^0+e^post2 == 0 /\ d^0-c^0 <= 0), cost: 1 3: l3 -> l2 : e^0'=e^post3, b^0'=b^post3, d^0'=d^post3, a^0'=a^post3, c^0'=c^post3, (-b^0+b^post3 == 0 /\ -e^0+e^post3 == 0 /\ d^post3-d^0 == 0 /\ c^post3-c^0 == 0 /\ a^post3-a^0 == 0 /\ 1-d^0+c^0 <= 0), cost: 1 4: l4 -> l3 : e^0'=e^post4, b^0'=b^post4, d^0'=d^post4, a^0'=a^post4, c^0'=c^post4, (-b^0+b^post4 == 0 /\ -e^0+e^post4 == 0 /\ -a^0+a^post4 == 0 /\ -d^0+d^post4 == 0 /\ -b^0 <= 0 /\ c^post4-c^0 == 0), cost: 1 5: l4 -> l2 : e^0'=e^post5, b^0'=b^post5, d^0'=d^post5, a^0'=a^post5, c^0'=c^post5, (-e^0+e^post5 == 0 /\ 1+b^0 <= 0 /\ c^post5-c^0 == 0 /\ -d^0+d^post5 == 0 /\ a^post5-a^0 == 0 /\ -b^0+b^post5 == 0), cost: 1 16: l5 -> l10 : e^0'=e^post16, b^0'=b^post16, d^0'=d^post16, a^0'=a^post16, c^0'=c^post16, (a^post16-a^0 == 0 /\ -b^0+b^post16 == 0 /\ -b^0 <= 0 /\ -e^0+e^post16 == 0 /\ -d^0+d^post16 == 0 /\ c^post16-c^0 == 0), cost: 1 17: l5 -> l6 : e^0'=e^post17, b^0'=b^post17, d^0'=d^post17, a^0'=a^post17, c^0'=c^post17, (d^post17-d^350 == 0 /\ -d^0+d^150 == 0 /\ -a^0+a^15 == 0 /\ b^250+b^150 == 0 /\ -e^0+e^150 == 0 /\ e^post17-e^350 == 0 /\ -a^350+a^post17 == 0 /\ a^350-a^250+b^350 == 0 /\ -b^350+b^post17 == 0 /\ 1+b^0 <= 0 /\ -b^0+b^150 == 0 /\ -b^250+b^350 == 0 /\ e^250-e^150 == 0 /\ c^350-c^250 == 0 /\ d^250-d^150 == 0 /\ -c^350+b^350+c^post17 == 0 /\ -e^250+e^350 == 0 /\ a^250-a^15 == 0 /\ -d^250+d^350 == 0 /\ -c^150+c^250 == 0 /\ c^150-c^0 == 0), cost: 1 18: l6 -> l8 : e^0'=e^post18, b^0'=b^post18, d^0'=d^post18, a^0'=a^post18, c^0'=c^post18, (-e^0+e^post18 == 0 /\ -b^0+b^post18 == 0 /\ c^post18-c^0 == 0 /\ -d^0+d^post18 == 0 /\ a^post18-a^0 == 0), cost: 1 8: l7 -> l6 : e^0'=e^post8, b^0'=b^post8, d^0'=d^post8, a^0'=a^post8, c^0'=c^post8, (-e^0+e^post8 == 0 /\ -a^0+a^post8 == 0 /\ b^post8-b^0 == 0 /\ c^post8-c^0 == 0 /\ -d^0+d^post8 == 0 /\ -e^0 <= 0), cost: 1 9: l7 -> l6 : e^0'=e^post9, b^0'=b^post9, d^0'=d^post9, a^0'=a^post9, c^0'=c^post9, (-d^120+d^220 == 0 /\ -a^12+a^220 == 0 /\ -e^0+e^120 == 0 /\ 1+e^0 <= 0 /\ c^220-c^120 == 0 /\ c^320-c^220 == 0 /\ -b^120+b^220 == 0 /\ b^120-b^0 == 0 /\ -c^0+c^120 == 0 /\ e^220+e^120 == 0 /\ d^120-d^0 == 0 /\ e^post9-e^320 == 0 /\ a^12-a^0 == 0 /\ e^post9-a^320+a^post9 == 0 /\ -c^320+c^post9 == 0 /\ -b^320+b^post9 == 0 /\ -d^320+d^post9 == 0 /\ -b^220+b^320 == 0 /\ -e^220+e^320 == 0 /\ d^320+e^320-d^220 == 0 /\ a^320-a^220 == 0), cost: 1 10: l8 -> l4 : e^0'=e^post10, b^0'=b^post10, d^0'=d^post10, a^0'=a^post10, c^0'=c^post10, (c^post10-c^0 == 0 /\ -a^0+a^post10 == 0 /\ -d^0+d^post10 == 0 /\ e^post10-e^0 == 0 /\ -a^0 <= 0 /\ -b^0+b^post10 == 0), cost: 1 11: l8 -> l2 : e^0'=e^post11, b^0'=b^post11, d^0'=d^post11, a^0'=a^post11, c^0'=c^post11, (1+a^0 <= 0 /\ a^post11-a^0 == 0 /\ -c^0+c^post11 == 0 /\ -b^0+b^post11 == 0 /\ -e^0+e^post11 == 0 /\ d^post11-d^0 == 0), cost: 1 12: l9 -> l7 : e^0'=e^post12, b^0'=b^post12, d^0'=d^post12, a^0'=a^post12, c^0'=c^post12, (-d^0 <= 0 /\ -d^0+d^post12 == 0 /\ c^post12-c^0 == 0 /\ -b^0+b^post12 == 0 /\ a^post12-a^0 == 0 /\ -e^0+e^post12 == 0), cost: 1 13: l9 -> l6 : e^0'=e^post13, b^0'=b^post13, d^0'=d^post13, a^0'=a^post13, c^0'=c^post13, (b^post13-b^330 == 0 /\ -e^0+e^130 == 0 /\ d^330-e^330+e^post13 == 0 /\ -b^0+b^130 == 0 /\ a^230-a^13 == 0 /\ c^230-c^130 == 0 /\ b^230-b^130 == 0 /\ -a^0+a^13 == 0 /\ d^330-d^230 == 0 /\ -d^330+d^post13 == 0 /\ -a^330+a^post13 == 0 /\ c^130-c^0 == 0 /\ d^330-c^230+c^330 == 0 /\ e^230-e^130 == 0 /\ -c^330+c^post13 == 0 /\ -b^230+b^330 == 0 /\ -d^0+d^130 == 0 /\ -e^230+e^330 == 0 /\ d^230+d^130 == 0 /\ 1+d^0 <= 0 /\ -a^230+a^330 == 0), cost: 1 14: l10 -> l9 : e^0'=e^post14, b^0'=b^post14, d^0'=d^post14, a^0'=a^post14, c^0'=c^post14, (-a^0+a^post14 == 0 /\ c^post14-c^0 == 0 /\ -d^0+d^post14 == 0 /\ -c^0 <= 0 /\ -b^0+b^post14 == 0 /\ -e^0+e^post14 == 0), cost: 1 15: l10 -> l6 : e^0'=e^post15, b^0'=b^post15, d^0'=d^post15, a^0'=a^post15, c^0'=c^post15, (c^340+d^post15-d^340 == 0 /\ e^post15-e^340 == 0 /\ e^340-e^240 == 0 /\ -d^240+d^340 == 0 /\ -a^240+a^340 == 0 /\ -e^0+e^140 == 0 /\ -c^240+c^340 == 0 /\ -a^0+a^14 == 0 /\ -e^140+e^240 == 0 /\ d^140-d^0 == 0 /\ a^post15-a^340 == 0 /\ c^140-c^0 == 0 /\ -b^0+b^140 == 0 /\ a^240-a^14 == 0 /\ -c^340+c^post15 == 0 /\ 1+c^0 <= 0 /\ c^240+c^140 == 0 /\ -b^340+b^post15 == 0 /\ -d^140+d^240 == 0 /\ b^240-b^140 == 0 /\ -b^240+b^340+c^340 == 0), cost: 1 19: l11 -> l6 : e^0'=e^post19, b^0'=b^post19, d^0'=d^post19, a^0'=a^post19, c^0'=c^post19, (a^0-a^post19 == 0 /\ d^0-d^post19 == 0 /\ b^0-b^post19 == 0 /\ e^0-e^post19 == 0 /\ -c^post19+c^0 == 0), cost: 1 Applied preprocessing Original rule: l0 -> l2 : e^0'=e^post1, b^0'=b^post1, d^0'=d^post1, a^0'=a^post1, c^0'=c^post1, (1+e^0 <= 0 /\ -e^0+e^post1 == 0 /\ -b^0+b^post1 == 0 /\ c^post1-c^0 == 0 /\ a^post1-a^0 == 0 /\ -d^0+d^post1 == 0), cost: 1 New rule: l0 -> l2 : 1+e^0 <= 0, cost: 1 Applied preprocessing Original rule: l3 -> l0 : e^0'=e^post2, b^0'=b^post2, d^0'=d^post2, a^0'=a^post2, c^0'=c^post2, (b^post2-b^0 == 0 /\ c^post2-c^0 == 0 /\ -a^0+a^post2 == 0 /\ -d^0+d^post2 == 0 /\ -e^0+e^post2 == 0 /\ d^0-c^0 <= 0), cost: 1 New rule: l3 -> l0 : d^0-c^0 <= 0, cost: 1 Applied preprocessing Original rule: l3 -> l2 : e^0'=e^post3, b^0'=b^post3, d^0'=d^post3, a^0'=a^post3, c^0'=c^post3, (-b^0+b^post3 == 0 /\ -e^0+e^post3 == 0 /\ d^post3-d^0 == 0 /\ c^post3-c^0 == 0 /\ a^post3-a^0 == 0 /\ 1-d^0+c^0 <= 0), cost: 1 New rule: l3 -> l2 : 1-d^0+c^0 <= 0, cost: 1 Applied preprocessing Original rule: l4 -> l3 : e^0'=e^post4, b^0'=b^post4, d^0'=d^post4, a^0'=a^post4, c^0'=c^post4, (-b^0+b^post4 == 0 /\ -e^0+e^post4 == 0 /\ -a^0+a^post4 == 0 /\ -d^0+d^post4 == 0 /\ -b^0 <= 0 /\ c^post4-c^0 == 0), cost: 1 New rule: l4 -> l3 : b^0 >= 0, cost: 1 Applied preprocessing Original rule: l4 -> l2 : e^0'=e^post5, b^0'=b^post5, d^0'=d^post5, a^0'=a^post5, c^0'=c^post5, (-e^0+e^post5 == 0 /\ 1+b^0 <= 0 /\ c^post5-c^0 == 0 /\ -d^0+d^post5 == 0 /\ a^post5-a^0 == 0 /\ -b^0+b^post5 == 0), cost: 1 New rule: l4 -> l2 : 1+b^0 <= 0, cost: 1 Applied preprocessing Original rule: l2 -> l5 : e^0'=e^post6, b^0'=b^post6, d^0'=d^post6, a^0'=a^post6, c^0'=c^post6, (-b^0+b^post6 == 0 /\ -e^0+e^post6 == 0 /\ -a^0+a^post6 == 0 /\ -d^0+d^post6 == 0 /\ c^post6-c^0 == 0 /\ -a^0 <= 0), cost: 1 New rule: l2 -> l5 : a^0 >= 0, cost: 1 Applied preprocessing Original rule: l2 -> l6 : e^0'=e^post7, b^0'=b^post7, d^0'=d^post7, a^0'=a^post7, c^0'=c^post7, (1+a^0 <= 0 /\ -c^0+c^110 == 0 /\ -d^310+d^post7 == 0 /\ d^310-d^210 == 0 /\ -b^210+b^310+a^210 == 0 /\ a^post7-a^310 == 0 /\ -c^210+c^310 == 0 /\ -a^0+a^11 == 0 /\ a^210+a^11 == 0 /\ e^210-e^110 == 0 /\ -b^0+b^110 == 0 /\ d^110-d^0 == 0 /\ b^post7-b^310 == 0 /\ c^210-c^110 == 0 /\ e^310-e^210 == 0 /\ -e^310+e^post7+a^310 == 0 /\ -d^110+d^210 == 0 /\ -e^0+e^110 == 0 /\ -a^210+a^310 == 0 /\ c^post7-c^310 == 0 /\ b^210-b^110 == 0), cost: 1 New rule: l2 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 1 Applied preprocessing Original rule: l7 -> l6 : e^0'=e^post8, b^0'=b^post8, d^0'=d^post8, a^0'=a^post8, c^0'=c^post8, (-e^0+e^post8 == 0 /\ -a^0+a^post8 == 0 /\ b^post8-b^0 == 0 /\ c^post8-c^0 == 0 /\ -d^0+d^post8 == 0 /\ -e^0 <= 0), cost: 1 New rule: l7 -> l6 : e^0 >= 0, cost: 1 Applied preprocessing Original rule: l7 -> l6 : e^0'=e^post9, b^0'=b^post9, d^0'=d^post9, a^0'=a^post9, c^0'=c^post9, (-d^120+d^220 == 0 /\ -a^12+a^220 == 0 /\ -e^0+e^120 == 0 /\ 1+e^0 <= 0 /\ c^220-c^120 == 0 /\ c^320-c^220 == 0 /\ -b^120+b^220 == 0 /\ b^120-b^0 == 0 /\ -c^0+c^120 == 0 /\ e^220+e^120 == 0 /\ d^120-d^0 == 0 /\ e^post9-e^320 == 0 /\ a^12-a^0 == 0 /\ e^post9-a^320+a^post9 == 0 /\ -c^320+c^post9 == 0 /\ -b^320+b^post9 == 0 /\ -d^320+d^post9 == 0 /\ -b^220+b^320 == 0 /\ -e^220+e^320 == 0 /\ d^320+e^320-d^220 == 0 /\ a^320-a^220 == 0), cost: 1 New rule: l7 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, 1+e^0 <= 0, cost: 1 Applied preprocessing Original rule: l8 -> l4 : e^0'=e^post10, b^0'=b^post10, d^0'=d^post10, a^0'=a^post10, c^0'=c^post10, (c^post10-c^0 == 0 /\ -a^0+a^post10 == 0 /\ -d^0+d^post10 == 0 /\ e^post10-e^0 == 0 /\ -a^0 <= 0 /\ -b^0+b^post10 == 0), cost: 1 New rule: l8 -> l4 : a^0 >= 0, cost: 1 Applied preprocessing Original rule: l8 -> l2 : e^0'=e^post11, b^0'=b^post11, d^0'=d^post11, a^0'=a^post11, c^0'=c^post11, (1+a^0 <= 0 /\ a^post11-a^0 == 0 /\ -c^0+c^post11 == 0 /\ -b^0+b^post11 == 0 /\ -e^0+e^post11 == 0 /\ d^post11-d^0 == 0), cost: 1 New rule: l8 -> l2 : 1+a^0 <= 0, cost: 1 Applied preprocessing Original rule: l9 -> l7 : e^0'=e^post12, b^0'=b^post12, d^0'=d^post12, a^0'=a^post12, c^0'=c^post12, (-d^0 <= 0 /\ -d^0+d^post12 == 0 /\ c^post12-c^0 == 0 /\ -b^0+b^post12 == 0 /\ a^post12-a^0 == 0 /\ -e^0+e^post12 == 0), cost: 1 New rule: l9 -> l7 : d^0 >= 0, cost: 1 Applied preprocessing Original rule: l9 -> l6 : e^0'=e^post13, b^0'=b^post13, d^0'=d^post13, a^0'=a^post13, c^0'=c^post13, (b^post13-b^330 == 0 /\ -e^0+e^130 == 0 /\ d^330-e^330+e^post13 == 0 /\ -b^0+b^130 == 0 /\ a^230-a^13 == 0 /\ c^230-c^130 == 0 /\ b^230-b^130 == 0 /\ -a^0+a^13 == 0 /\ d^330-d^230 == 0 /\ -d^330+d^post13 == 0 /\ -a^330+a^post13 == 0 /\ c^130-c^0 == 0 /\ d^330-c^230+c^330 == 0 /\ e^230-e^130 == 0 /\ -c^330+c^post13 == 0 /\ -b^230+b^330 == 0 /\ -d^0+d^130 == 0 /\ -e^230+e^330 == 0 /\ d^230+d^130 == 0 /\ 1+d^0 <= 0 /\ -a^230+a^330 == 0), cost: 1 New rule: l9 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, 1+d^0 <= 0, cost: 1 Applied preprocessing Original rule: l10 -> l9 : e^0'=e^post14, b^0'=b^post14, d^0'=d^post14, a^0'=a^post14, c^0'=c^post14, (-a^0+a^post14 == 0 /\ c^post14-c^0 == 0 /\ -d^0+d^post14 == 0 /\ -c^0 <= 0 /\ -b^0+b^post14 == 0 /\ -e^0+e^post14 == 0), cost: 1 New rule: l10 -> l9 : c^0 >= 0, cost: 1 Applied preprocessing Original rule: l10 -> l6 : e^0'=e^post15, b^0'=b^post15, d^0'=d^post15, a^0'=a^post15, c^0'=c^post15, (c^340+d^post15-d^340 == 0 /\ e^post15-e^340 == 0 /\ e^340-e^240 == 0 /\ -d^240+d^340 == 0 /\ -a^240+a^340 == 0 /\ -e^0+e^140 == 0 /\ -c^240+c^340 == 0 /\ -a^0+a^14 == 0 /\ -e^140+e^240 == 0 /\ d^140-d^0 == 0 /\ a^post15-a^340 == 0 /\ c^140-c^0 == 0 /\ -b^0+b^140 == 0 /\ a^240-a^14 == 0 /\ -c^340+c^post15 == 0 /\ 1+c^0 <= 0 /\ c^240+c^140 == 0 /\ -b^340+b^post15 == 0 /\ -d^140+d^240 == 0 /\ b^240-b^140 == 0 /\ -b^240+b^340+c^340 == 0), cost: 1 New rule: l10 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, 1+c^0 <= 0, cost: 1 Applied preprocessing Original rule: l5 -> l10 : e^0'=e^post16, b^0'=b^post16, d^0'=d^post16, a^0'=a^post16, c^0'=c^post16, (a^post16-a^0 == 0 /\ -b^0+b^post16 == 0 /\ -b^0 <= 0 /\ -e^0+e^post16 == 0 /\ -d^0+d^post16 == 0 /\ c^post16-c^0 == 0), cost: 1 New rule: l5 -> l10 : b^0 >= 0, cost: 1 Applied preprocessing Original rule: l5 -> l6 : e^0'=e^post17, b^0'=b^post17, d^0'=d^post17, a^0'=a^post17, c^0'=c^post17, (d^post17-d^350 == 0 /\ -d^0+d^150 == 0 /\ -a^0+a^15 == 0 /\ b^250+b^150 == 0 /\ -e^0+e^150 == 0 /\ e^post17-e^350 == 0 /\ -a^350+a^post17 == 0 /\ a^350-a^250+b^350 == 0 /\ -b^350+b^post17 == 0 /\ 1+b^0 <= 0 /\ -b^0+b^150 == 0 /\ -b^250+b^350 == 0 /\ e^250-e^150 == 0 /\ c^350-c^250 == 0 /\ d^250-d^150 == 0 /\ -c^350+b^350+c^post17 == 0 /\ -e^250+e^350 == 0 /\ a^250-a^15 == 0 /\ -d^250+d^350 == 0 /\ -c^150+c^250 == 0 /\ c^150-c^0 == 0), cost: 1 New rule: l5 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, 1+b^0 <= 0, cost: 1 Applied preprocessing Original rule: l6 -> l8 : e^0'=e^post18, b^0'=b^post18, d^0'=d^post18, a^0'=a^post18, c^0'=c^post18, (-e^0+e^post18 == 0 /\ -b^0+b^post18 == 0 /\ c^post18-c^0 == 0 /\ -d^0+d^post18 == 0 /\ a^post18-a^0 == 0), cost: 1 New rule: l6 -> l8 : TRUE, cost: 1 Applied preprocessing Original rule: l11 -> l6 : e^0'=e^post19, b^0'=b^post19, d^0'=d^post19, a^0'=a^post19, c^0'=c^post19, (a^0-a^post19 == 0 /\ d^0-d^post19 == 0 /\ b^0-b^post19 == 0 /\ e^0-e^post19 == 0 /\ -c^post19+c^0 == 0), cost: 1 New rule: l11 -> l6 : TRUE, cost: 1 Simplified rules Start location: l11 20: l0 -> l2 : 1+e^0 <= 0, cost: 1 25: l2 -> l5 : a^0 >= 0, cost: 1 26: l2 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 1 21: l3 -> l0 : d^0-c^0 <= 0, cost: 1 22: l3 -> l2 : 1-d^0+c^0 <= 0, cost: 1 23: l4 -> l3 : b^0 >= 0, cost: 1 24: l4 -> l2 : 1+b^0 <= 0, cost: 1 35: l5 -> l10 : b^0 >= 0, cost: 1 36: l5 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, 1+b^0 <= 0, cost: 1 37: l6 -> l8 : TRUE, cost: 1 27: l7 -> l6 : e^0 >= 0, cost: 1 28: l7 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, 1+e^0 <= 0, cost: 1 29: l8 -> l4 : a^0 >= 0, cost: 1 30: l8 -> l2 : 1+a^0 <= 0, cost: 1 31: l9 -> l7 : d^0 >= 0, cost: 1 32: l9 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, 1+d^0 <= 0, cost: 1 33: l10 -> l9 : c^0 >= 0, cost: 1 34: l10 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, 1+c^0 <= 0, cost: 1 38: l11 -> l6 : TRUE, cost: 1 Eliminating location l0 by chaining: Applied chaining First rule: l3 -> l0 : d^0-c^0 <= 0, cost: 1 Second rule: l0 -> l2 : 1+e^0 <= 0, cost: 1 New rule: l3 -> l2 : (1+e^0 <= 0 /\ d^0-c^0 <= 0), cost: 2 Applied deletion Removed the following rules: 20 21 Eliminated locations on linear paths Start location: l11 25: l2 -> l5 : a^0 >= 0, cost: 1 26: l2 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 1 22: l3 -> l2 : 1-d^0+c^0 <= 0, cost: 1 39: l3 -> l2 : (1+e^0 <= 0 /\ d^0-c^0 <= 0), cost: 2 23: l4 -> l3 : b^0 >= 0, cost: 1 24: l4 -> l2 : 1+b^0 <= 0, cost: 1 35: l5 -> l10 : b^0 >= 0, cost: 1 36: l5 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, 1+b^0 <= 0, cost: 1 37: l6 -> l8 : TRUE, cost: 1 27: l7 -> l6 : e^0 >= 0, cost: 1 28: l7 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, 1+e^0 <= 0, cost: 1 29: l8 -> l4 : a^0 >= 0, cost: 1 30: l8 -> l2 : 1+a^0 <= 0, cost: 1 31: l9 -> l7 : d^0 >= 0, cost: 1 32: l9 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, 1+d^0 <= 0, cost: 1 33: l10 -> l9 : c^0 >= 0, cost: 1 34: l10 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, 1+c^0 <= 0, cost: 1 38: l11 -> l6 : TRUE, cost: 1 Eliminating location l8 by chaining: Applied chaining First rule: l6 -> l8 : TRUE, cost: 1 Second rule: l8 -> l4 : a^0 >= 0, cost: 1 New rule: l6 -> l4 : a^0 >= 0, cost: 2 Applied chaining First rule: l6 -> l8 : TRUE, cost: 1 Second rule: l8 -> l2 : 1+a^0 <= 0, cost: 1 New rule: l6 -> l2 : 1+a^0 <= 0, cost: 2 Applied deletion Removed the following rules: 29 30 37 Eliminating location l5 by chaining: Applied chaining First rule: l2 -> l5 : a^0 >= 0, cost: 1 Second rule: l5 -> l10 : b^0 >= 0, cost: 1 New rule: l2 -> l10 : (b^0 >= 0 /\ a^0 >= 0), cost: 2 Applied chaining First rule: l2 -> l5 : a^0 >= 0, cost: 1 Second rule: l5 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, 1+b^0 <= 0, cost: 1 New rule: l2 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 2 Applied deletion Removed the following rules: 25 35 36 Eliminating location l9 by chaining: Applied chaining First rule: l10 -> l9 : c^0 >= 0, cost: 1 Second rule: l9 -> l7 : d^0 >= 0, cost: 1 New rule: l10 -> l7 : (d^0 >= 0 /\ c^0 >= 0), cost: 2 Applied chaining First rule: l10 -> l9 : c^0 >= 0, cost: 1 Second rule: l9 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, 1+d^0 <= 0, cost: 1 New rule: l10 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (c^0 >= 0 /\ 1+d^0 <= 0), cost: 2 Applied deletion Removed the following rules: 31 32 33 Eliminating location l3 by chaining: Applied chaining First rule: l4 -> l3 : b^0 >= 0, cost: 1 Second rule: l3 -> l2 : 1-d^0+c^0 <= 0, cost: 1 New rule: l4 -> l2 : (b^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 2 Applied chaining First rule: l4 -> l3 : b^0 >= 0, cost: 1 Second rule: l3 -> l2 : (1+e^0 <= 0 /\ d^0-c^0 <= 0), cost: 2 New rule: l4 -> l2 : (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0-c^0 <= 0), cost: 3 Applied deletion Removed the following rules: 22 23 39 Eliminated locations on tree-shaped paths Start location: l11 26: l2 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 1 42: l2 -> l10 : (b^0 >= 0 /\ a^0 >= 0), cost: 2 43: l2 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 2 24: l4 -> l2 : 1+b^0 <= 0, cost: 1 46: l4 -> l2 : (b^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 2 47: l4 -> l2 : (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0-c^0 <= 0), cost: 3 40: l6 -> l4 : a^0 >= 0, cost: 2 41: l6 -> l2 : 1+a^0 <= 0, cost: 2 27: l7 -> l6 : e^0 >= 0, cost: 1 28: l7 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, 1+e^0 <= 0, cost: 1 34: l10 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, 1+c^0 <= 0, cost: 1 44: l10 -> l7 : (d^0 >= 0 /\ c^0 >= 0), cost: 2 45: l10 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (c^0 >= 0 /\ 1+d^0 <= 0), cost: 2 38: l11 -> l6 : TRUE, cost: 1 Eliminating location l4 by chaining: Applied chaining First rule: l6 -> l4 : a^0 >= 0, cost: 2 Second rule: l4 -> l2 : 1+b^0 <= 0, cost: 1 New rule: l6 -> l2 : (1+b^0 <= 0 /\ a^0 >= 0), cost: 3 Applied chaining First rule: l6 -> l4 : a^0 >= 0, cost: 2 Second rule: l4 -> l2 : (b^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 2 New rule: l6 -> l2 : (b^0 >= 0 /\ a^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 4 Applied chaining First rule: l6 -> l4 : a^0 >= 0, cost: 2 Second rule: l4 -> l2 : (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0-c^0 <= 0), cost: 3 New rule: l6 -> l2 : (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 5 Applied deletion Removed the following rules: 24 40 46 47 Eliminating location l10 by chaining: Applied chaining First rule: l2 -> l10 : (b^0 >= 0 /\ a^0 >= 0), cost: 2 Second rule: l10 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, 1+c^0 <= 0, cost: 1 New rule: l2 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0), cost: 3 Applied chaining First rule: l2 -> l10 : (b^0 >= 0 /\ a^0 >= 0), cost: 2 Second rule: l10 -> l7 : (d^0 >= 0 /\ c^0 >= 0), cost: 2 New rule: l2 -> l7 : (b^0 >= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0), cost: 4 Applied chaining First rule: l2 -> l10 : (b^0 >= 0 /\ a^0 >= 0), cost: 2 Second rule: l10 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (c^0 >= 0 /\ 1+d^0 <= 0), cost: 2 New rule: l2 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 4 Applied deletion Removed the following rules: 34 42 44 45 Eliminated locations on tree-shaped paths Start location: l11 26: l2 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 1 43: l2 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 2 51: l2 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0), cost: 3 52: l2 -> l7 : (b^0 >= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0), cost: 4 53: l2 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 4 41: l6 -> l2 : 1+a^0 <= 0, cost: 2 48: l6 -> l2 : (1+b^0 <= 0 /\ a^0 >= 0), cost: 3 49: l6 -> l2 : (b^0 >= 0 /\ a^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 4 50: l6 -> l2 : (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 5 27: l7 -> l6 : e^0 >= 0, cost: 1 28: l7 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, 1+e^0 <= 0, cost: 1 38: l11 -> l6 : TRUE, cost: 1 Eliminating location l2 by chaining: Applied chaining First rule: l6 -> l2 : 1+a^0 <= 0, cost: 2 Second rule: l2 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 1 New rule: l6 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 3 Applied chaining First rule: l6 -> l2 : (1+b^0 <= 0 /\ a^0 >= 0), cost: 3 Second rule: l2 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 2 New rule: l6 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 5 Applied chaining First rule: l6 -> l2 : (b^0 >= 0 /\ a^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 4 Second rule: l2 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0), cost: 3 New rule: l6 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 7 Applied chaining First rule: l6 -> l2 : (b^0 >= 0 /\ a^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 4 Second rule: l2 -> l7 : (b^0 >= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0), cost: 4 New rule: l6 -> l7 : (b^0 >= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 8 Applied simplification Original rule: l6 -> l7 : (b^0 >= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 8 New rule: l6 -> l7 : (b^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 8 Applied chaining First rule: l6 -> l2 : (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 5 Second rule: l2 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0), cost: 3 New rule: l6 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ d^0-c^0 <= 0), cost: 8 Applied chaining First rule: l6 -> l2 : (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 5 Second rule: l2 -> l7 : (b^0 >= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0), cost: 4 New rule: l6 -> l7 : (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0 /\ c^0 >= 0), cost: 9 Applied simplification Original rule: l6 -> l7 : (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0 /\ c^0 >= 0), cost: 9 New rule: l6 -> l7 : (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 9 Applied chaining First rule: l6 -> l2 : (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 5 Second rule: l2 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 4 New rule: l6 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 9 Applied simplification Original rule: l6 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 9 New rule: l6 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 9 Applied deletion Removed the following rules: 26 41 43 48 49 50 51 52 53 Eliminated locations on tree-shaped paths Start location: l11 54: l6 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 3 55: l6 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 5 56: l6 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 7 57: l6 -> l7 : (b^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 8 58: l6 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ d^0-c^0 <= 0), cost: 8 59: l6 -> l7 : (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 9 60: l6 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 9 27: l7 -> l6 : e^0 >= 0, cost: 1 28: l7 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, 1+e^0 <= 0, cost: 1 38: l11 -> l6 : TRUE, cost: 1 Accelerated simple loops Start location: l11 54: l6 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 3 55: l6 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 5 56: l6 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 7 57: l6 -> l7 : (b^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 8 58: l6 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ d^0-c^0 <= 0), cost: 8 59: l6 -> l7 : (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 9 60: l6 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 9 27: l7 -> l6 : e^0 >= 0, cost: 1 28: l7 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, 1+e^0 <= 0, cost: 1 38: l11 -> l6 : TRUE, cost: 1 Applied chaining First rule: l7 -> l6 : e^0 >= 0, cost: 1 Second rule: l6 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 3 New rule: l7 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, (e^0 >= 0 /\ 1+a^0 <= 0), cost: 4 Applied chaining First rule: l7 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, 1+e^0 <= 0, cost: 1 Second rule: l6 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 3 New rule: l7 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (1+e^0 <= 0 /\ 1+e^0+a^0 <= 0), cost: 4 Applied chaining First rule: l11 -> l6 : TRUE, cost: 1 Second rule: l6 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 3 New rule: l11 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 4 Applied chaining First rule: l7 -> l6 : e^0 >= 0, cost: 1 Second rule: l6 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 5 New rule: l7 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (e^0 >= 0 /\ 1+b^0 <= 0 /\ a^0 >= 0), cost: 6 Applied chaining First rule: l7 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, 1+e^0 <= 0, cost: 1 Second rule: l6 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 5 New rule: l7 -> l6 : e^0'=-e^0, b^0'=-b^0, d^0'=e^0+d^0, a^0'=e^0+b^0+a^0, c^0'=b^0+c^0, (1+e^0 <= 0 /\ 1+b^0 <= 0 /\ e^0+a^0 >= 0), cost: 6 Applied chaining First rule: l11 -> l6 : TRUE, cost: 1 Second rule: l6 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 5 New rule: l11 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 6 Applied chaining First rule: l7 -> l6 : e^0 >= 0, cost: 1 Second rule: l6 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 7 New rule: l7 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (e^0 >= 0 /\ b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 8 Applied chaining First rule: l7 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, 1+e^0 <= 0, cost: 1 Second rule: l6 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 7 New rule: l7 -> l6 : e^0'=-e^0, b^0'=b^0+c^0, d^0'=e^0+d^0+c^0, a^0'=e^0+a^0, c^0'=-c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ 1-e^0-d^0+c^0 <= 0 /\ e^0+a^0 >= 0 /\ 1+c^0 <= 0), cost: 8 Applied chaining First rule: l11 -> l6 : TRUE, cost: 1 Second rule: l6 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 7 New rule: l11 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 8 Applied chaining First rule: l11 -> l6 : TRUE, cost: 1 Second rule: l6 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ d^0-c^0 <= 0), cost: 8 New rule: l11 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ d^0-c^0 <= 0), cost: 9 Applied chaining First rule: l11 -> l6 : TRUE, cost: 1 Second rule: l6 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 9 New rule: l11 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 10 Applied deletion Removed the following rules: 54 55 56 58 60 Chained accelerated rules with incoming rules Start location: l11 57: l6 -> l7 : (b^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 8 59: l6 -> l7 : (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 9 27: l7 -> l6 : e^0 >= 0, cost: 1 28: l7 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, 1+e^0 <= 0, cost: 1 61: l7 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, (e^0 >= 0 /\ 1+a^0 <= 0), cost: 4 62: l7 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (1+e^0 <= 0 /\ 1+e^0+a^0 <= 0), cost: 4 64: l7 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (e^0 >= 0 /\ 1+b^0 <= 0 /\ a^0 >= 0), cost: 6 65: l7 -> l6 : e^0'=-e^0, b^0'=-b^0, d^0'=e^0+d^0, a^0'=e^0+b^0+a^0, c^0'=b^0+c^0, (1+e^0 <= 0 /\ 1+b^0 <= 0 /\ e^0+a^0 >= 0), cost: 6 67: l7 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (e^0 >= 0 /\ b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 8 68: l7 -> l6 : e^0'=-e^0, b^0'=b^0+c^0, d^0'=e^0+d^0+c^0, a^0'=e^0+a^0, c^0'=-c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ 1-e^0-d^0+c^0 <= 0 /\ e^0+a^0 >= 0 /\ 1+c^0 <= 0), cost: 8 38: l11 -> l6 : TRUE, cost: 1 63: l11 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 4 66: l11 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 6 69: l11 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 8 70: l11 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ d^0-c^0 <= 0), cost: 9 71: l11 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 10 Eliminating location l7 by chaining: Applied chaining First rule: l6 -> l7 : (b^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 8 Second rule: l7 -> l6 : e^0 >= 0, cost: 1 New rule: l6 -> l6 : (e^0 >= 0 /\ b^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 9 Applied chaining First rule: l6 -> l7 : (b^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 8 Second rule: l7 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, 1+e^0 <= 0, cost: 1 New rule: l6 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 9 Applied chaining First rule: l6 -> l7 : (b^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 8 Second rule: l7 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (1+e^0 <= 0 /\ 1+e^0+a^0 <= 0), cost: 4 New rule: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 12 Applied simplification Original rule: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 12 New rule: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 12 Applied chaining First rule: l6 -> l7 : (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 9 Second rule: l7 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, 1+e^0 <= 0, cost: 1 New rule: l6 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 10 Applied chaining First rule: l6 -> l7 : (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 9 Second rule: l7 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (1+e^0 <= 0 /\ 1+e^0+a^0 <= 0), cost: 4 New rule: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 13 Applied simplification Original rule: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 13 New rule: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ d^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 13 Applied deletion Removed the following rules: 27 28 57 59 61 62 64 65 67 68 Eliminated locations on tree-shaped paths Start location: l11 72: l6 -> l6 : (e^0 >= 0 /\ b^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 9 73: l6 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 9 74: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 12 75: l6 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 10 76: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ d^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 13 38: l11 -> l6 : TRUE, cost: 1 63: l11 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 4 66: l11 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 6 69: l11 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 8 70: l11 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ d^0-c^0 <= 0), cost: 9 71: l11 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 10 Applied pruning (of leafs and parallel rules): Start location: l11 72: l6 -> l6 : (e^0 >= 0 /\ b^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 9 73: l6 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 9 74: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 12 75: l6 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 10 76: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ d^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 13 38: l11 -> l6 : TRUE, cost: 1 63: l11 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 4 66: l11 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 6 69: l11 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 8 71: l11 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 10 Applied nonterm Original rule: l6 -> l6 : (e^0 >= 0 /\ b^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 9 New rule: l6 -> [13] : (e^0 >= 0 /\ b^0 >= 0 /\ -1+d^0-c^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ n12 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_ogjEac.txt Applied deletion Removed the following rules: 72 Accelerated simple loops Start location: l11 73: l6 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 9 74: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 12 75: l6 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 10 76: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ d^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 13 77: l6 -> [13] : (e^0 >= 0 /\ b^0 >= 0 /\ -1+d^0-c^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ n12 >= 0), cost: NONTERM 38: l11 -> l6 : TRUE, cost: 1 63: l11 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 4 66: l11 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 6 69: l11 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 8 71: l11 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 10 Applied chaining First rule: l11 -> l6 : TRUE, cost: 1 Second rule: l6 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 9 New rule: l11 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 10 Applied chaining First rule: l11 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 4 Second rule: l6 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 9 New rule: l11 -> l6 : e^0'=-e^0-a^0, b^0'=b^0+a^0, d^0'=e^0+d^0+a^0, a^0'=e^0, (1+a^0 <= 0 /\ 1+e^0+a^0 <= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0 /\ b^0+a^0 >= 0), cost: 13 Applied chaining First rule: l11 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 6 Second rule: l6 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 9 New rule: l11 -> l6 : e^0'=-e^0, b^0'=-b^0, d^0'=e^0+d^0, a^0'=e^0+b^0+a^0, c^0'=b^0+c^0, (1+e^0 <= 0 /\ 1+b^0-d^0+c^0 <= 0 /\ 1+b^0 <= 0 /\ b^0+c^0 >= 0 /\ b^0+a^0 >= 0), cost: 15 Applied chaining First rule: l11 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 8 Second rule: l6 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 9 New rule: l11 -> l6 : e^0'=-e^0, b^0'=b^0+c^0, d^0'=e^0+d^0+c^0, a^0'=e^0+a^0, c^0'=-c^0, (1+e^0 <= 0 /\ b^0+c^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0-2*c^0 <= 0), cost: 17 Applied chaining First rule: l11 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 10 Second rule: l6 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 9 New rule: l11 -> l6 : e^0'=-e^0-d^0, d^0'=e^0, a^0'=e^0+d^0+a^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0+c^0 >= 0 /\ 1+2*d^0+c^0 <= 0 /\ a^0 >= 0), cost: 19 Applied chaining First rule: l11 -> l6 : TRUE, cost: 1 Second rule: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 12 New rule: l11 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 13 Applied chaining First rule: l11 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 4 Second rule: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 12 New rule: l11 -> l6 : e^0'=-a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0+a^0, a^0'=-e^0, (1+a^0 <= 0 /\ 1+e^0 <= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0 /\ b^0+a^0 >= 0), cost: 16 Applied chaining First rule: l11 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 6 Second rule: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 12 New rule: l11 -> l6 : e^0'=b^0+a^0, b^0'=e^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-b^0-a^0, c^0'=b^0+c^0, (1+b^0-d^0+c^0 <= 0 /\ 1+e^0+b^0+a^0 <= 0 /\ 1+b^0 <= 0 /\ b^0+c^0 >= 0 /\ b^0+a^0 >= 0), cost: 18 Applied chaining First rule: l11 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 8 Second rule: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 12 New rule: l11 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0+c^0, d^0'=e^0+d^0+c^0, a^0'=-e^0-a^0, c^0'=-c^0, (b^0+c^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0-2*c^0 <= 0), cost: 20 Applied chaining First rule: l11 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 10 Second rule: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 12 New rule: l11 -> l6 : e^0'=a^0, b^0'=e^0+b^0+d^0+a^0, d^0'=e^0, a^0'=-e^0-d^0-a^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ 1+e^0+d^0+a^0 <= 0 /\ d^0+c^0 >= 0 /\ 1+2*d^0+c^0 <= 0 /\ a^0 >= 0), cost: 22 Applied chaining First rule: l11 -> l6 : TRUE, cost: 1 Second rule: l6 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 10 New rule: l11 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 11 Applied chaining First rule: l11 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 4 Second rule: l6 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 10 New rule: l11 -> l6 : e^0'=-e^0-a^0, b^0'=b^0+a^0, d^0'=e^0+d^0+a^0, a^0'=e^0, (1+a^0 <= 0 /\ d^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ d^0-c^0 <= 0 /\ b^0+a^0 >= 0), cost: 14 Applied chaining First rule: l11 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 6 Second rule: l6 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 10 New rule: l11 -> l6 : e^0'=-e^0, b^0'=-b^0, d^0'=e^0+d^0, a^0'=e^0+b^0+a^0, c^0'=b^0+c^0, (-b^0+d^0-c^0 <= 0 /\ 1+e^0 <= 0 /\ 1+b^0 <= 0 /\ d^0 >= 0 /\ b^0+a^0 >= 0), cost: 16 Applied chaining First rule: l11 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 8 Second rule: l6 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 10 New rule: l11 -> l6 : e^0'=-e^0, b^0'=b^0+c^0, d^0'=e^0+d^0+c^0, a^0'=e^0+a^0, c^0'=-c^0, (d^0+2*c^0 <= 0 /\ 1+e^0 <= 0 /\ b^0+c^0 >= 0 /\ d^0+c^0 >= 0 /\ a^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 18 Applied chaining First rule: l11 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 10 Second rule: l6 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 10 New rule: l11 -> l6 : e^0'=-e^0-d^0, d^0'=e^0, a^0'=e^0+d^0+a^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ -2*d^0-c^0 <= 0 /\ 1+d^0 <= 0), cost: 20 Applied chaining First rule: l11 -> l6 : TRUE, cost: 1 Second rule: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ d^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 13 New rule: l11 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ d^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 14 Applied chaining First rule: l11 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 4 Second rule: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ d^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 13 New rule: l11 -> l6 : e^0'=-a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0+a^0, a^0'=-e^0, (1+a^0 <= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ d^0-c^0 <= 0 /\ b^0+a^0 >= 0), cost: 17 Applied chaining First rule: l11 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 6 Second rule: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ d^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 13 New rule: l11 -> l6 : e^0'=b^0+a^0, b^0'=e^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-b^0-a^0, c^0'=b^0+c^0, (-b^0+d^0-c^0 <= 0 /\ 1+e^0+b^0+a^0 <= 0 /\ 1+b^0 <= 0 /\ d^0 >= 0 /\ b^0+a^0 >= 0), cost: 19 Applied chaining First rule: l11 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 8 Second rule: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ d^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 13 New rule: l11 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0+c^0, d^0'=e^0+d^0+c^0, a^0'=-e^0-a^0, c^0'=-c^0, (d^0+2*c^0 <= 0 /\ b^0+c^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ d^0+c^0 >= 0 /\ a^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 21 Applied chaining First rule: l11 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 10 Second rule: l6 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ d^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 13 New rule: l11 -> l6 : e^0'=a^0, b^0'=e^0+b^0+d^0+a^0, d^0'=e^0, a^0'=-e^0-d^0-a^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ 1+e^0+d^0+a^0 <= 0 /\ a^0 >= 0 /\ -2*d^0-c^0 <= 0 /\ 1+d^0 <= 0), cost: 23 Applied chaining First rule: l11 -> l6 : TRUE, cost: 1 Second rule: l6 -> [13] : (e^0 >= 0 /\ b^0 >= 0 /\ -1+d^0-c^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ n12 >= 0), cost: NONTERM New rule: l11 -> [13] : (e^0 >= 0 /\ b^0 >= 0 /\ -1+d^0-c^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0), cost: NONTERM Applied chaining First rule: l11 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 4 Second rule: l6 -> [13] : (e^0 >= 0 /\ b^0 >= 0 /\ -1+d^0-c^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ n12 >= 0), cost: NONTERM New rule: l11 -> [13] : (1+a^0 <= 0 /\ -1+d^0-c^0 >= 0 /\ e^0+a^0 >= 0 /\ c^0 >= 0 /\ b^0+a^0 >= 0), cost: NONTERM Applied chaining First rule: l11 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 6 Second rule: l6 -> [13] : (e^0 >= 0 /\ b^0 >= 0 /\ -1+d^0-c^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ n12 >= 0), cost: NONTERM New rule: l11 -> [13] : (e^0 >= 0 /\ 1+b^0 <= 0 /\ b^0+c^0 >= 0 /\ -1-b^0+d^0-c^0 >= 0 /\ b^0+a^0 >= 0), cost: NONTERM Applied chaining First rule: l11 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 8 Second rule: l6 -> [13] : (e^0 >= 0 /\ b^0 >= 0 /\ -1+d^0-c^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ n12 >= 0), cost: NONTERM New rule: l11 -> [13] : (e^0 >= 0 /\ b^0+c^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ -1+d^0+2*c^0 >= 0), cost: NONTERM Applied deletion Removed the following rules: 73 74 75 76 77 Chained accelerated rules with incoming rules Start location: l11 38: l11 -> l6 : TRUE, cost: 1 63: l11 -> l6 : e^0'=e^0+a^0, b^0'=b^0+a^0, a^0'=-a^0, 1+a^0 <= 0, cost: 4 66: l11 -> l6 : b^0'=-b^0, a^0'=b^0+a^0, c^0'=b^0+c^0, (1+b^0 <= 0 /\ a^0 >= 0), cost: 6 69: l11 -> l6 : b^0'=b^0+c^0, d^0'=d^0+c^0, c^0'=-c^0, (b^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0+c^0 <= 0), cost: 8 71: l11 -> l6 : e^0'=e^0+d^0, d^0'=-d^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1+d^0 <= 0), cost: 10 78: l11 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 10 79: l11 -> l6 : e^0'=-e^0-a^0, b^0'=b^0+a^0, d^0'=e^0+d^0+a^0, a^0'=e^0, (1+a^0 <= 0 /\ 1+e^0+a^0 <= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0 /\ b^0+a^0 >= 0), cost: 13 80: l11 -> l6 : e^0'=-e^0, b^0'=-b^0, d^0'=e^0+d^0, a^0'=e^0+b^0+a^0, c^0'=b^0+c^0, (1+e^0 <= 0 /\ 1+b^0-d^0+c^0 <= 0 /\ 1+b^0 <= 0 /\ b^0+c^0 >= 0 /\ b^0+a^0 >= 0), cost: 15 81: l11 -> l6 : e^0'=-e^0, b^0'=b^0+c^0, d^0'=e^0+d^0+c^0, a^0'=e^0+a^0, c^0'=-c^0, (1+e^0 <= 0 /\ b^0+c^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0-2*c^0 <= 0), cost: 17 82: l11 -> l6 : e^0'=-e^0-d^0, d^0'=e^0, a^0'=e^0+d^0+a^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0+c^0 >= 0 /\ 1+2*d^0+c^0 <= 0 /\ a^0 >= 0), cost: 19 83: l11 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 13 84: l11 -> l6 : e^0'=-a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0+a^0, a^0'=-e^0, (1+a^0 <= 0 /\ 1+e^0 <= 0 /\ c^0 >= 0 /\ 1-d^0+c^0 <= 0 /\ b^0+a^0 >= 0), cost: 16 85: l11 -> l6 : e^0'=b^0+a^0, b^0'=e^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-b^0-a^0, c^0'=b^0+c^0, (1+b^0-d^0+c^0 <= 0 /\ 1+e^0+b^0+a^0 <= 0 /\ 1+b^0 <= 0 /\ b^0+c^0 >= 0 /\ b^0+a^0 >= 0), cost: 18 86: l11 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0+c^0, d^0'=e^0+d^0+c^0, a^0'=-e^0-a^0, c^0'=-c^0, (b^0+c^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ 1-d^0-2*c^0 <= 0), cost: 20 87: l11 -> l6 : e^0'=a^0, b^0'=e^0+b^0+d^0+a^0, d^0'=e^0, a^0'=-e^0-d^0-a^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ 1+e^0+d^0+a^0 <= 0 /\ d^0+c^0 >= 0 /\ 1+2*d^0+c^0 <= 0 /\ a^0 >= 0), cost: 22 88: l11 -> l6 : e^0'=-e^0, d^0'=e^0+d^0, a^0'=e^0+a^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 11 89: l11 -> l6 : e^0'=-e^0-a^0, b^0'=b^0+a^0, d^0'=e^0+d^0+a^0, a^0'=e^0, (1+a^0 <= 0 /\ d^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ d^0-c^0 <= 0 /\ b^0+a^0 >= 0), cost: 14 90: l11 -> l6 : e^0'=-e^0, b^0'=-b^0, d^0'=e^0+d^0, a^0'=e^0+b^0+a^0, c^0'=b^0+c^0, (-b^0+d^0-c^0 <= 0 /\ 1+e^0 <= 0 /\ 1+b^0 <= 0 /\ d^0 >= 0 /\ b^0+a^0 >= 0), cost: 16 91: l11 -> l6 : e^0'=-e^0, b^0'=b^0+c^0, d^0'=e^0+d^0+c^0, a^0'=e^0+a^0, c^0'=-c^0, (d^0+2*c^0 <= 0 /\ 1+e^0 <= 0 /\ b^0+c^0 >= 0 /\ d^0+c^0 >= 0 /\ a^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 18 92: l11 -> l6 : e^0'=-e^0-d^0, d^0'=e^0, a^0'=e^0+d^0+a^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ a^0 >= 0 /\ -2*d^0-c^0 <= 0 /\ 1+d^0 <= 0), cost: 20 93: l11 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-a^0, (b^0 >= 0 /\ d^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ a^0 >= 0 /\ d^0-c^0 <= 0), cost: 14 94: l11 -> l6 : e^0'=-a^0, b^0'=e^0+b^0+a^0, d^0'=e^0+d^0+a^0, a^0'=-e^0, (1+a^0 <= 0 /\ 1+e^0 <= 0 /\ d^0 >= 0 /\ d^0-c^0 <= 0 /\ b^0+a^0 >= 0), cost: 17 95: l11 -> l6 : e^0'=b^0+a^0, b^0'=e^0+a^0, d^0'=e^0+d^0, a^0'=-e^0-b^0-a^0, c^0'=b^0+c^0, (-b^0+d^0-c^0 <= 0 /\ 1+e^0+b^0+a^0 <= 0 /\ 1+b^0 <= 0 /\ d^0 >= 0 /\ b^0+a^0 >= 0), cost: 19 96: l11 -> l6 : e^0'=a^0, b^0'=e^0+b^0+a^0+c^0, d^0'=e^0+d^0+c^0, a^0'=-e^0-a^0, c^0'=-c^0, (d^0+2*c^0 <= 0 /\ b^0+c^0 >= 0 /\ 1+e^0+a^0 <= 0 /\ d^0+c^0 >= 0 /\ a^0 >= 0 /\ 1-d^0+c^0 <= 0), cost: 21 97: l11 -> l6 : e^0'=a^0, b^0'=e^0+b^0+d^0+a^0, d^0'=e^0, a^0'=-e^0-d^0-a^0, c^0'=d^0+c^0, (b^0 >= 0 /\ 1+e^0 <= 0 /\ 1+e^0+d^0+a^0 <= 0 /\ a^0 >= 0 /\ -2*d^0-c^0 <= 0 /\ 1+d^0 <= 0), cost: 23 98: l11 -> [13] : (e^0 >= 0 /\ b^0 >= 0 /\ -1+d^0-c^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0), cost: NONTERM 99: l11 -> [13] : (1+a^0 <= 0 /\ -1+d^0-c^0 >= 0 /\ e^0+a^0 >= 0 /\ c^0 >= 0 /\ b^0+a^0 >= 0), cost: NONTERM 100: l11 -> [13] : (e^0 >= 0 /\ 1+b^0 <= 0 /\ b^0+c^0 >= 0 /\ -1-b^0+d^0-c^0 >= 0 /\ b^0+a^0 >= 0), cost: NONTERM 101: l11 -> [13] : (e^0 >= 0 /\ b^0+c^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ -1+d^0+2*c^0 >= 0), cost: NONTERM Removed unreachable locations and irrelevant leafs Start location: l11 98: l11 -> [13] : (e^0 >= 0 /\ b^0 >= 0 /\ -1+d^0-c^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0), cost: NONTERM 99: l11 -> [13] : (1+a^0 <= 0 /\ -1+d^0-c^0 >= 0 /\ e^0+a^0 >= 0 /\ c^0 >= 0 /\ b^0+a^0 >= 0), cost: NONTERM 100: l11 -> [13] : (e^0 >= 0 /\ 1+b^0 <= 0 /\ b^0+c^0 >= 0 /\ -1-b^0+d^0-c^0 >= 0 /\ b^0+a^0 >= 0), cost: NONTERM 101: l11 -> [13] : (e^0 >= 0 /\ b^0+c^0 >= 0 /\ a^0 >= 0 /\ 1+c^0 <= 0 /\ -1+d^0+2*c^0 >= 0), cost: NONTERM Computing asymptotic complexity Proved nontermination of rule 98 via SMT. Proved the following lower bound Complexity: Nonterm Cpx degree: Nonterm Solved cost: NONTERM Rule cost: NONTERM Rule guard: (e^0 >= 0 /\ b^0 >= 0 /\ -1+d^0-c^0 >= 0 /\ a^0 >= 0 /\ c^0 >= 0)