WORST_CASE(Omega(0),?) Initial ITS Start location: l17 0: l0 -> l1 : j^0'=j^post0, __const_5^0'=__const_5^post0, source^0'=source^post0, i^0'=i^post0, __const_16^0'=__const_16^post0, y^0'=y^post0, nodecount^0'=nodecount^post0, edgecount^0'=edgecount^post0, x^0'=x^post0, (-i^0+nodecount^0 <= 0 /\ __const_16^0-__const_16^post0 == 0 /\ -x^post0+x^0 == 0 /\ y^0-y^post0 == 0 /\ source^0-source^post0 == 0 /\ j^0-j^post0 == 0 /\ __const_5^0-__const_5^post0 == 0 /\ -edgecount^post0+edgecount^0 == 0 /\ -nodecount^post0+nodecount^0 == 0 /\ i^0-i^post0 == 0), cost: 1 1: l0 -> l2 : j^0'=j^post1, __const_5^0'=__const_5^post1, source^0'=source^post1, i^0'=i^post1, __const_16^0'=__const_16^post1, y^0'=y^post1, nodecount^0'=nodecount^post1, edgecount^0'=edgecount^post1, x^0'=x^post1, (-x^post1+x^0 == 0 /\ -edgecount^post1+edgecount^0 == 0 /\ -nodecount^post1+nodecount^0 == 0 /\ -1-i^0+i^post1 == 0 /\ j^0-j^post1 == 0 /\ 1+i^0-nodecount^0 <= 0 /\ source^0-source^post1 == 0 /\ -__const_5^post1+__const_5^0 == 0 /\ -y^post1+y^0 == 0 /\ -__const_16^post1+__const_16^0 == 0), cost: 1 22: l2 -> l0 : j^0'=j^post22, __const_5^0'=__const_5^post22, source^0'=source^post22, i^0'=i^post22, __const_16^0'=__const_16^post22, y^0'=y^post22, nodecount^0'=nodecount^post22, edgecount^0'=edgecount^post22, x^0'=x^post22, (__const_16^0-__const_16^post22 == 0 /\ -source^post22+source^0 == 0 /\ -i^post22+i^0 == 0 /\ -x^post22+x^0 == 0 /\ y^0-y^post22 == 0 /\ -nodecount^post22+nodecount^0 == 0 /\ __const_5^0-__const_5^post22 == 0 /\ j^0-j^post22 == 0 /\ -edgecount^post22+edgecount^0 == 0), cost: 1 2: l3 -> l4 : j^0'=j^post2, __const_5^0'=__const_5^post2, source^0'=source^post2, i^0'=i^post2, __const_16^0'=__const_16^post2, y^0'=y^post2, nodecount^0'=nodecount^post2, edgecount^0'=edgecount^post2, x^0'=x^post2, (__const_5^0-__const_5^post2 == 0 /\ edgecount^0-edgecount^post2 == 0 /\ -x^post2+x^0 == 0 /\ -y^post2+y^0 == 0 /\ j^0-j^post2 == 0 /\ source^0-source^post2 == 0 /\ -1-i^0+i^post2 == 0 /\ nodecount^0-nodecount^post2 == 0 /\ -__const_16^post2+__const_16^0 == 0), cost: 1 3: l3 -> l1 : j^0'=j^post3, __const_5^0'=__const_5^post3, source^0'=source^post3, i^0'=i^post3, __const_16^0'=__const_16^post3, y^0'=y^post3, nodecount^0'=nodecount^post3, edgecount^0'=edgecount^post3, x^0'=x^post3, (-edgecount^post3+edgecount^0 == 0 /\ -nodecount^post3+nodecount^0 == 0 /\ -x^post3+x^0 == 0 /\ -i^post3+i^0 == 0 /\ __const_16^0-__const_16^post3 == 0 /\ j^0-j^post3 == 0 /\ -source^post3+source^0 == 0 /\ __const_5^0-__const_5^post3 == 0 /\ -y^post3+y^0 == 0), cost: 1 21: l4 -> l5 : j^0'=j^post21, __const_5^0'=__const_5^post21, source^0'=source^post21, i^0'=i^post21, __const_16^0'=__const_16^post21, y^0'=y^post21, nodecount^0'=nodecount^post21, edgecount^0'=edgecount^post21, x^0'=x^post21, (y^0-y^post21 == 0 /\ j^0-j^post21 == 0 /\ -i^post21+i^0 == 0 /\ -edgecount^post21+edgecount^0 == 0 /\ __const_16^0-__const_16^post21 == 0 /\ -source^post21+source^0 == 0 /\ __const_5^0-__const_5^post21 == 0 /\ -x^post21+x^0 == 0 /\ -nodecount^post21+nodecount^0 == 0), cost: 1 4: l5 -> l2 : j^0'=j^post4, __const_5^0'=__const_5^post4, source^0'=source^post4, i^0'=i^post4, __const_16^0'=__const_16^post4, y^0'=y^post4, nodecount^0'=nodecount^post4, edgecount^0'=edgecount^post4, x^0'=x^post4, (i^post4 == 0 /\ j^0-j^post4 == 0 /\ -nodecount^post4+nodecount^0 == 0 /\ -source^post4+source^0 == 0 /\ y^0-y^post4 == 0 /\ -edgecount^post4+edgecount^0 == 0 /\ -x^post4+x^0 == 0 /\ __const_16^0-__const_16^post4 == 0 /\ -i^0+edgecount^0 <= 0 /\ __const_5^0-__const_5^post4 == 0), cost: 1 5: l5 -> l3 : j^0'=j^post5, __const_5^0'=__const_5^post5, source^0'=source^post5, i^0'=i^post5, __const_16^0'=__const_16^post5, y^0'=y^post5, nodecount^0'=nodecount^post5, edgecount^0'=edgecount^post5, x^0'=x^post5, (0 == 0 /\ -i^post5+i^0 == 0 /\ -__const_5^post5+__const_5^0 == 0 /\ 1+i^0-edgecount^0 <= 0 /\ -edgecount^post5+edgecount^0 == 0 /\ j^0-j^post5 == 0 /\ source^0-source^post5 == 0 /\ -nodecount^post5+nodecount^0 == 0 /\ __const_16^0-__const_16^post5 == 0), cost: 1 6: l6 -> l7 : j^0'=j^post6, __const_5^0'=__const_5^post6, source^0'=source^post6, i^0'=i^post6, __const_16^0'=__const_16^post6, y^0'=y^post6, nodecount^0'=nodecount^post6, edgecount^0'=edgecount^post6, x^0'=x^post6, (-y^post6+y^0 == 0 /\ source^0-source^post6 == 0 /\ -1-j^0+j^post6 == 0 /\ -x^post6+x^0 == 0 /\ edgecount^0-edgecount^post6 == 0 /\ __const_5^0-__const_5^post6 == 0 /\ i^0-i^post6 == 0 /\ nodecount^0-nodecount^post6 == 0 /\ -__const_16^post6+__const_16^0 == 0), cost: 1 20: l7 -> l8 : j^0'=j^post20, __const_5^0'=__const_5^post20, source^0'=source^post20, i^0'=i^post20, __const_16^0'=__const_16^post20, y^0'=y^post20, nodecount^0'=nodecount^post20, edgecount^0'=edgecount^post20, x^0'=x^post20, (i^0-i^post20 == 0 /\ -__const_16^post20+__const_16^0 == 0 /\ __const_5^0-__const_5^post20 == 0 /\ -source^post20+source^0 == 0 /\ -x^post20+x^0 == 0 /\ -edgecount^post20+edgecount^0 == 0 /\ j^0-j^post20 == 0 /\ -y^post20+y^0 == 0 /\ nodecount^0-nodecount^post20 == 0), cost: 1 7: l8 -> l9 : j^0'=j^post7, __const_5^0'=__const_5^post7, source^0'=source^post7, i^0'=i^post7, __const_16^0'=__const_16^post7, y^0'=y^post7, nodecount^0'=nodecount^post7, edgecount^0'=edgecount^post7, x^0'=x^post7, (__const_5^0-__const_5^post7 == 0 /\ -source^post7+source^0 == 0 /\ -1-i^0+i^post7 == 0 /\ -y^post7+y^0 == 0 /\ -j^0+edgecount^0 <= 0 /\ -__const_16^post7+__const_16^0 == 0 /\ nodecount^0-nodecount^post7 == 0 /\ -edgecount^post7+edgecount^0 == 0 /\ -x^post7+x^0 == 0 /\ -j^post7+j^0 == 0), cost: 1 8: l8 -> l6 : j^0'=j^post8, __const_5^0'=__const_5^post8, source^0'=source^post8, i^0'=i^post8, __const_16^0'=__const_16^post8, y^0'=y^post8, nodecount^0'=nodecount^post8, edgecount^0'=edgecount^post8, x^0'=x^post8, (0 == 0 /\ -edgecount^post8+edgecount^0 == 0 /\ 1+j^0-edgecount^0 <= 0 /\ __const_5^0-__const_5^post8 == 0 /\ __const_16^0-__const_16^post8 == 0 /\ nodecount^0-nodecount^post8 == 0 /\ j^0-j^post8 == 0 /\ -i^post8+i^0 == 0 /\ -source^post8+source^0 == 0), cost: 1 19: l9 -> l10 : j^0'=j^post19, __const_5^0'=__const_5^post19, source^0'=source^post19, i^0'=i^post19, __const_16^0'=__const_16^post19, y^0'=y^post19, nodecount^0'=nodecount^post19, edgecount^0'=edgecount^post19, x^0'=x^post19, (-__const_16^post19+__const_16^0 == 0 /\ -edgecount^post19+edgecount^0 == 0 /\ -nodecount^post19+nodecount^0 == 0 /\ -x^post19+x^0 == 0 /\ j^0-j^post19 == 0 /\ source^0-source^post19 == 0 /\ i^0-i^post19 == 0 /\ -__const_5^post19+__const_5^0 == 0 /\ -y^post19+y^0 == 0), cost: 1 9: l10 -> l4 : j^0'=j^post9, __const_5^0'=__const_5^post9, source^0'=source^post9, i^0'=i^post9, __const_16^0'=__const_16^post9, y^0'=y^post9, nodecount^0'=nodecount^post9, edgecount^0'=edgecount^post9, x^0'=x^post9, (-x^post9+x^0 == 0 /\ i^post9 == 0 /\ -edgecount^post9+edgecount^0 == 0 /\ -i^0+nodecount^0 <= 0 /\ __const_16^0-__const_16^post9 == 0 /\ -nodecount^post9+nodecount^0 == 0 /\ y^0-y^post9 == 0 /\ source^0-source^post9 == 0 /\ -__const_5^post9+__const_5^0 == 0 /\ j^0-j^post9 == 0), cost: 1 10: l10 -> l7 : j^0'=j^post10, __const_5^0'=__const_5^post10, source^0'=source^post10, i^0'=i^post10, __const_16^0'=__const_16^post10, y^0'=y^post10, nodecount^0'=nodecount^post10, edgecount^0'=edgecount^post10, x^0'=x^post10, (source^0-source^post10 == 0 /\ j^post10 == 0 /\ -x^post10+x^0 == 0 /\ i^0-i^post10 == 0 /\ -y^post10+y^0 == 0 /\ edgecount^0-edgecount^post10 == 0 /\ 1+i^0-nodecount^0 <= 0 /\ __const_5^0-__const_5^post10 == 0 /\ -nodecount^post10+nodecount^0 == 0 /\ -__const_16^post10+__const_16^0 == 0), cost: 1 11: l11 -> l12 : j^0'=j^post11, __const_5^0'=__const_5^post11, source^0'=source^post11, i^0'=i^post11, __const_16^0'=__const_16^post11, y^0'=y^post11, nodecount^0'=nodecount^post11, edgecount^0'=edgecount^post11, x^0'=x^post11, (edgecount^0-edgecount^post11 == 0 /\ -y^post11+y^0 == 0 /\ nodecount^0-nodecount^post11 == 0 /\ -x^post11+x^0 == 0 /\ __const_5^0-__const_5^post11 == 0 /\ -__const_16^post11+__const_16^0 == 0 /\ i^0-i^post11 == 0 /\ j^0-j^post11 == 0 /\ source^0-source^post11 == 0), cost: 1 12: l12 -> l13 : j^0'=j^post12, __const_5^0'=__const_5^post12, source^0'=source^post12, i^0'=i^post12, __const_16^0'=__const_16^post12, y^0'=y^post12, nodecount^0'=nodecount^post12, edgecount^0'=edgecount^post12, x^0'=x^post12, (-x^post12+x^0 == 0 /\ __const_5^0-__const_5^post12 == 0 /\ -edgecount^post12+edgecount^0 == 0 /\ __const_16^0-__const_16^post12 == 0 /\ nodecount^0-nodecount^post12 == 0 /\ j^0-j^post12 == 0 /\ -y^post12+y^0 == 0 /\ -source^post12+source^0 == 0 /\ -1+i^post12-i^0 == 0), cost: 1 13: l13 -> l14 : j^0'=j^post13, __const_5^0'=__const_5^post13, source^0'=source^post13, i^0'=i^post13, __const_16^0'=__const_16^post13, y^0'=y^post13, nodecount^0'=nodecount^post13, edgecount^0'=edgecount^post13, x^0'=x^post13, (-edgecount^post13+edgecount^0 == 0 /\ __const_5^0-__const_5^post13 == 0 /\ -nodecount^post13+nodecount^0 == 0 /\ y^0-y^post13 == 0 /\ -i^post13+i^0 == 0 /\ j^0-j^post13 == 0 /\ source^0-source^post13 == 0 /\ -x^post13+x^0 == 0 /\ __const_16^0-__const_16^post13 == 0), cost: 1 17: l14 -> l9 : j^0'=j^post17, __const_5^0'=__const_5^post17, source^0'=source^post17, i^0'=i^post17, __const_16^0'=__const_16^post17, y^0'=y^post17, nodecount^0'=nodecount^post17, edgecount^0'=edgecount^post17, x^0'=x^post17, (-source^post17+source^0 == 0 /\ __const_16^0-__const_16^post17 == 0 /\ i^post17 == 0 /\ -i^0+nodecount^0 <= 0 /\ y^0-y^post17 == 0 /\ -x^post17+x^0 == 0 /\ -nodecount^post17+nodecount^0 == 0 /\ __const_5^0-__const_5^post17 == 0 /\ -edgecount^post17+edgecount^0 == 0 /\ j^0-j^post17 == 0), cost: 1 18: l14 -> l15 : j^0'=j^post18, __const_5^0'=__const_5^post18, source^0'=source^post18, i^0'=i^post18, __const_16^0'=__const_16^post18, y^0'=y^post18, nodecount^0'=nodecount^post18, edgecount^0'=edgecount^post18, x^0'=x^post18, (__const_5^0-__const_5^post18 == 0 /\ -x^post18+x^0 == 0 /\ 1+i^0-nodecount^0 <= 0 /\ -nodecount^post18+nodecount^0 == 0 /\ j^0-j^post18 == 0 /\ __const_16^0-__const_16^post18 == 0 /\ y^0-y^post18 == 0 /\ i^0-i^post18 == 0 /\ source^0-source^post18 == 0 /\ -edgecount^post18+edgecount^0 == 0), cost: 1 14: l15 -> l11 : j^0'=j^post14, __const_5^0'=__const_5^post14, source^0'=source^post14, i^0'=i^post14, __const_16^0'=__const_16^post14, y^0'=y^post14, nodecount^0'=nodecount^post14, edgecount^0'=edgecount^post14, x^0'=x^post14, (-nodecount^post14+nodecount^0 == 0 /\ -__const_16^post14+__const_16^0 == 0 /\ j^0-j^post14 == 0 /\ source^0-source^post14 == 0 /\ -edgecount^post14+edgecount^0 == 0 /\ i^0-i^post14 == 0 /\ 1+source^0-i^0 <= 0 /\ __const_5^0-__const_5^post14 == 0 /\ -x^post14+x^0 == 0 /\ -y^post14+y^0 == 0), cost: 1 15: l15 -> l11 : j^0'=j^post15, __const_5^0'=__const_5^post15, source^0'=source^post15, i^0'=i^post15, __const_16^0'=__const_16^post15, y^0'=y^post15, nodecount^0'=nodecount^post15, edgecount^0'=edgecount^post15, x^0'=x^post15, (j^0-j^post15 == 0 /\ source^0-source^post15 == 0 /\ edgecount^0-edgecount^post15 == 0 /\ i^0-i^post15 == 0 /\ 1-source^0+i^0 <= 0 /\ -__const_16^post15+__const_16^0 == 0 /\ -nodecount^post15+nodecount^0 == 0 /\ -x^post15+x^0 == 0 /\ -y^post15+y^0 == 0 /\ __const_5^0-__const_5^post15 == 0), cost: 1 16: l15 -> l12 : j^0'=j^post16, __const_5^0'=__const_5^post16, source^0'=source^post16, i^0'=i^post16, __const_16^0'=__const_16^post16, y^0'=y^post16, nodecount^0'=nodecount^post16, edgecount^0'=edgecount^post16, x^0'=x^post16, (__const_5^0-__const_5^post16 == 0 /\ -y^post16+y^0 == 0 /\ -source^post16+source^0 == 0 /\ nodecount^0-nodecount^post16 == 0 /\ -source^0+i^0 <= 0 /\ -x^post16+x^0 == 0 /\ -__const_16^post16+__const_16^0 == 0 /\ j^0-j^post16 == 0 /\ -edgecount^post16+edgecount^0 == 0 /\ source^0-i^0 <= 0 /\ i^0-i^post16 == 0), cost: 1 23: l16 -> l13 : j^0'=j^post23, __const_5^0'=__const_5^post23, source^0'=source^post23, i^0'=i^post23, __const_16^0'=__const_16^post23, y^0'=y^post23, nodecount^0'=nodecount^post23, edgecount^0'=edgecount^post23, x^0'=x^post23, (-__const_5^post23+__const_5^0 == 0 /\ edgecount^post23-__const_16^0 == 0 /\ __const_16^0-__const_16^post23 == 0 /\ j^0-j^post23 == 0 /\ -x^post23+x^0 == 0 /\ y^0-y^post23 == 0 /\ source^post23 == 0 /\ i^post23 == 0 /\ -__const_5^0+nodecount^post23 == 0), cost: 1 24: l17 -> l16 : j^0'=j^post24, __const_5^0'=__const_5^post24, source^0'=source^post24, i^0'=i^post24, __const_16^0'=__const_16^post24, y^0'=y^post24, nodecount^0'=nodecount^post24, edgecount^0'=edgecount^post24, x^0'=x^post24, (j^0-j^post24 == 0 /\ source^0-source^post24 == 0 /\ -y^post24+y^0 == 0 /\ i^0-i^post24 == 0 /\ edgecount^0-edgecount^post24 == 0 /\ -x^post24+x^0 == 0 /\ -__const_16^post24+__const_16^0 == 0 /\ -nodecount^post24+nodecount^0 == 0 /\ __const_5^0-__const_5^post24 == 0), cost: 1 Removed unreachable rules and leafs Start location: l17 1: l0 -> l2 : j^0'=j^post1, __const_5^0'=__const_5^post1, source^0'=source^post1, i^0'=i^post1, __const_16^0'=__const_16^post1, y^0'=y^post1, nodecount^0'=nodecount^post1, edgecount^0'=edgecount^post1, x^0'=x^post1, (-x^post1+x^0 == 0 /\ -edgecount^post1+edgecount^0 == 0 /\ -nodecount^post1+nodecount^0 == 0 /\ -1-i^0+i^post1 == 0 /\ j^0-j^post1 == 0 /\ 1+i^0-nodecount^0 <= 0 /\ source^0-source^post1 == 0 /\ -__const_5^post1+__const_5^0 == 0 /\ -y^post1+y^0 == 0 /\ -__const_16^post1+__const_16^0 == 0), cost: 1 22: l2 -> l0 : j^0'=j^post22, __const_5^0'=__const_5^post22, source^0'=source^post22, i^0'=i^post22, __const_16^0'=__const_16^post22, y^0'=y^post22, nodecount^0'=nodecount^post22, edgecount^0'=edgecount^post22, x^0'=x^post22, (__const_16^0-__const_16^post22 == 0 /\ -source^post22+source^0 == 0 /\ -i^post22+i^0 == 0 /\ -x^post22+x^0 == 0 /\ y^0-y^post22 == 0 /\ -nodecount^post22+nodecount^0 == 0 /\ __const_5^0-__const_5^post22 == 0 /\ j^0-j^post22 == 0 /\ -edgecount^post22+edgecount^0 == 0), cost: 1 2: l3 -> l4 : j^0'=j^post2, __const_5^0'=__const_5^post2, source^0'=source^post2, i^0'=i^post2, __const_16^0'=__const_16^post2, y^0'=y^post2, nodecount^0'=nodecount^post2, edgecount^0'=edgecount^post2, x^0'=x^post2, (__const_5^0-__const_5^post2 == 0 /\ edgecount^0-edgecount^post2 == 0 /\ -x^post2+x^0 == 0 /\ -y^post2+y^0 == 0 /\ j^0-j^post2 == 0 /\ source^0-source^post2 == 0 /\ -1-i^0+i^post2 == 0 /\ nodecount^0-nodecount^post2 == 0 /\ -__const_16^post2+__const_16^0 == 0), cost: 1 21: l4 -> l5 : j^0'=j^post21, __const_5^0'=__const_5^post21, source^0'=source^post21, i^0'=i^post21, __const_16^0'=__const_16^post21, y^0'=y^post21, nodecount^0'=nodecount^post21, edgecount^0'=edgecount^post21, x^0'=x^post21, (y^0-y^post21 == 0 /\ j^0-j^post21 == 0 /\ -i^post21+i^0 == 0 /\ -edgecount^post21+edgecount^0 == 0 /\ __const_16^0-__const_16^post21 == 0 /\ -source^post21+source^0 == 0 /\ __const_5^0-__const_5^post21 == 0 /\ -x^post21+x^0 == 0 /\ -nodecount^post21+nodecount^0 == 0), cost: 1 4: l5 -> l2 : j^0'=j^post4, __const_5^0'=__const_5^post4, source^0'=source^post4, i^0'=i^post4, __const_16^0'=__const_16^post4, y^0'=y^post4, nodecount^0'=nodecount^post4, edgecount^0'=edgecount^post4, x^0'=x^post4, (i^post4 == 0 /\ j^0-j^post4 == 0 /\ -nodecount^post4+nodecount^0 == 0 /\ -source^post4+source^0 == 0 /\ y^0-y^post4 == 0 /\ -edgecount^post4+edgecount^0 == 0 /\ -x^post4+x^0 == 0 /\ __const_16^0-__const_16^post4 == 0 /\ -i^0+edgecount^0 <= 0 /\ __const_5^0-__const_5^post4 == 0), cost: 1 5: l5 -> l3 : j^0'=j^post5, __const_5^0'=__const_5^post5, source^0'=source^post5, i^0'=i^post5, __const_16^0'=__const_16^post5, y^0'=y^post5, nodecount^0'=nodecount^post5, edgecount^0'=edgecount^post5, x^0'=x^post5, (0 == 0 /\ -i^post5+i^0 == 0 /\ -__const_5^post5+__const_5^0 == 0 /\ 1+i^0-edgecount^0 <= 0 /\ -edgecount^post5+edgecount^0 == 0 /\ j^0-j^post5 == 0 /\ source^0-source^post5 == 0 /\ -nodecount^post5+nodecount^0 == 0 /\ __const_16^0-__const_16^post5 == 0), cost: 1 6: l6 -> l7 : j^0'=j^post6, __const_5^0'=__const_5^post6, source^0'=source^post6, i^0'=i^post6, __const_16^0'=__const_16^post6, y^0'=y^post6, nodecount^0'=nodecount^post6, edgecount^0'=edgecount^post6, x^0'=x^post6, (-y^post6+y^0 == 0 /\ source^0-source^post6 == 0 /\ -1-j^0+j^post6 == 0 /\ -x^post6+x^0 == 0 /\ edgecount^0-edgecount^post6 == 0 /\ __const_5^0-__const_5^post6 == 0 /\ i^0-i^post6 == 0 /\ nodecount^0-nodecount^post6 == 0 /\ -__const_16^post6+__const_16^0 == 0), cost: 1 20: l7 -> l8 : j^0'=j^post20, __const_5^0'=__const_5^post20, source^0'=source^post20, i^0'=i^post20, __const_16^0'=__const_16^post20, y^0'=y^post20, nodecount^0'=nodecount^post20, edgecount^0'=edgecount^post20, x^0'=x^post20, (i^0-i^post20 == 0 /\ -__const_16^post20+__const_16^0 == 0 /\ __const_5^0-__const_5^post20 == 0 /\ -source^post20+source^0 == 0 /\ -x^post20+x^0 == 0 /\ -edgecount^post20+edgecount^0 == 0 /\ j^0-j^post20 == 0 /\ -y^post20+y^0 == 0 /\ nodecount^0-nodecount^post20 == 0), cost: 1 7: l8 -> l9 : j^0'=j^post7, __const_5^0'=__const_5^post7, source^0'=source^post7, i^0'=i^post7, __const_16^0'=__const_16^post7, y^0'=y^post7, nodecount^0'=nodecount^post7, edgecount^0'=edgecount^post7, x^0'=x^post7, (__const_5^0-__const_5^post7 == 0 /\ -source^post7+source^0 == 0 /\ -1-i^0+i^post7 == 0 /\ -y^post7+y^0 == 0 /\ -j^0+edgecount^0 <= 0 /\ -__const_16^post7+__const_16^0 == 0 /\ nodecount^0-nodecount^post7 == 0 /\ -edgecount^post7+edgecount^0 == 0 /\ -x^post7+x^0 == 0 /\ -j^post7+j^0 == 0), cost: 1 8: l8 -> l6 : j^0'=j^post8, __const_5^0'=__const_5^post8, source^0'=source^post8, i^0'=i^post8, __const_16^0'=__const_16^post8, y^0'=y^post8, nodecount^0'=nodecount^post8, edgecount^0'=edgecount^post8, x^0'=x^post8, (0 == 0 /\ -edgecount^post8+edgecount^0 == 0 /\ 1+j^0-edgecount^0 <= 0 /\ __const_5^0-__const_5^post8 == 0 /\ __const_16^0-__const_16^post8 == 0 /\ nodecount^0-nodecount^post8 == 0 /\ j^0-j^post8 == 0 /\ -i^post8+i^0 == 0 /\ -source^post8+source^0 == 0), cost: 1 19: l9 -> l10 : j^0'=j^post19, __const_5^0'=__const_5^post19, source^0'=source^post19, i^0'=i^post19, __const_16^0'=__const_16^post19, y^0'=y^post19, nodecount^0'=nodecount^post19, edgecount^0'=edgecount^post19, x^0'=x^post19, (-__const_16^post19+__const_16^0 == 0 /\ -edgecount^post19+edgecount^0 == 0 /\ -nodecount^post19+nodecount^0 == 0 /\ -x^post19+x^0 == 0 /\ j^0-j^post19 == 0 /\ source^0-source^post19 == 0 /\ i^0-i^post19 == 0 /\ -__const_5^post19+__const_5^0 == 0 /\ -y^post19+y^0 == 0), cost: 1 9: l10 -> l4 : j^0'=j^post9, __const_5^0'=__const_5^post9, source^0'=source^post9, i^0'=i^post9, __const_16^0'=__const_16^post9, y^0'=y^post9, nodecount^0'=nodecount^post9, edgecount^0'=edgecount^post9, x^0'=x^post9, (-x^post9+x^0 == 0 /\ i^post9 == 0 /\ -edgecount^post9+edgecount^0 == 0 /\ -i^0+nodecount^0 <= 0 /\ __const_16^0-__const_16^post9 == 0 /\ -nodecount^post9+nodecount^0 == 0 /\ y^0-y^post9 == 0 /\ source^0-source^post9 == 0 /\ -__const_5^post9+__const_5^0 == 0 /\ j^0-j^post9 == 0), cost: 1 10: l10 -> l7 : j^0'=j^post10, __const_5^0'=__const_5^post10, source^0'=source^post10, i^0'=i^post10, __const_16^0'=__const_16^post10, y^0'=y^post10, nodecount^0'=nodecount^post10, edgecount^0'=edgecount^post10, x^0'=x^post10, (source^0-source^post10 == 0 /\ j^post10 == 0 /\ -x^post10+x^0 == 0 /\ i^0-i^post10 == 0 /\ -y^post10+y^0 == 0 /\ edgecount^0-edgecount^post10 == 0 /\ 1+i^0-nodecount^0 <= 0 /\ __const_5^0-__const_5^post10 == 0 /\ -nodecount^post10+nodecount^0 == 0 /\ -__const_16^post10+__const_16^0 == 0), cost: 1 11: l11 -> l12 : j^0'=j^post11, __const_5^0'=__const_5^post11, source^0'=source^post11, i^0'=i^post11, __const_16^0'=__const_16^post11, y^0'=y^post11, nodecount^0'=nodecount^post11, edgecount^0'=edgecount^post11, x^0'=x^post11, (edgecount^0-edgecount^post11 == 0 /\ -y^post11+y^0 == 0 /\ nodecount^0-nodecount^post11 == 0 /\ -x^post11+x^0 == 0 /\ __const_5^0-__const_5^post11 == 0 /\ -__const_16^post11+__const_16^0 == 0 /\ i^0-i^post11 == 0 /\ j^0-j^post11 == 0 /\ source^0-source^post11 == 0), cost: 1 12: l12 -> l13 : j^0'=j^post12, __const_5^0'=__const_5^post12, source^0'=source^post12, i^0'=i^post12, __const_16^0'=__const_16^post12, y^0'=y^post12, nodecount^0'=nodecount^post12, edgecount^0'=edgecount^post12, x^0'=x^post12, (-x^post12+x^0 == 0 /\ __const_5^0-__const_5^post12 == 0 /\ -edgecount^post12+edgecount^0 == 0 /\ __const_16^0-__const_16^post12 == 0 /\ nodecount^0-nodecount^post12 == 0 /\ j^0-j^post12 == 0 /\ -y^post12+y^0 == 0 /\ -source^post12+source^0 == 0 /\ -1+i^post12-i^0 == 0), cost: 1 13: l13 -> l14 : j^0'=j^post13, __const_5^0'=__const_5^post13, source^0'=source^post13, i^0'=i^post13, __const_16^0'=__const_16^post13, y^0'=y^post13, nodecount^0'=nodecount^post13, edgecount^0'=edgecount^post13, x^0'=x^post13, (-edgecount^post13+edgecount^0 == 0 /\ __const_5^0-__const_5^post13 == 0 /\ -nodecount^post13+nodecount^0 == 0 /\ y^0-y^post13 == 0 /\ -i^post13+i^0 == 0 /\ j^0-j^post13 == 0 /\ source^0-source^post13 == 0 /\ -x^post13+x^0 == 0 /\ __const_16^0-__const_16^post13 == 0), cost: 1 17: l14 -> l9 : j^0'=j^post17, __const_5^0'=__const_5^post17, source^0'=source^post17, i^0'=i^post17, __const_16^0'=__const_16^post17, y^0'=y^post17, nodecount^0'=nodecount^post17, edgecount^0'=edgecount^post17, x^0'=x^post17, (-source^post17+source^0 == 0 /\ __const_16^0-__const_16^post17 == 0 /\ i^post17 == 0 /\ -i^0+nodecount^0 <= 0 /\ y^0-y^post17 == 0 /\ -x^post17+x^0 == 0 /\ -nodecount^post17+nodecount^0 == 0 /\ __const_5^0-__const_5^post17 == 0 /\ -edgecount^post17+edgecount^0 == 0 /\ j^0-j^post17 == 0), cost: 1 18: l14 -> l15 : j^0'=j^post18, __const_5^0'=__const_5^post18, source^0'=source^post18, i^0'=i^post18, __const_16^0'=__const_16^post18, y^0'=y^post18, nodecount^0'=nodecount^post18, edgecount^0'=edgecount^post18, x^0'=x^post18, (__const_5^0-__const_5^post18 == 0 /\ -x^post18+x^0 == 0 /\ 1+i^0-nodecount^0 <= 0 /\ -nodecount^post18+nodecount^0 == 0 /\ j^0-j^post18 == 0 /\ __const_16^0-__const_16^post18 == 0 /\ y^0-y^post18 == 0 /\ i^0-i^post18 == 0 /\ source^0-source^post18 == 0 /\ -edgecount^post18+edgecount^0 == 0), cost: 1 14: l15 -> l11 : j^0'=j^post14, __const_5^0'=__const_5^post14, source^0'=source^post14, i^0'=i^post14, __const_16^0'=__const_16^post14, y^0'=y^post14, nodecount^0'=nodecount^post14, edgecount^0'=edgecount^post14, x^0'=x^post14, (-nodecount^post14+nodecount^0 == 0 /\ -__const_16^post14+__const_16^0 == 0 /\ j^0-j^post14 == 0 /\ source^0-source^post14 == 0 /\ -edgecount^post14+edgecount^0 == 0 /\ i^0-i^post14 == 0 /\ 1+source^0-i^0 <= 0 /\ __const_5^0-__const_5^post14 == 0 /\ -x^post14+x^0 == 0 /\ -y^post14+y^0 == 0), cost: 1 15: l15 -> l11 : j^0'=j^post15, __const_5^0'=__const_5^post15, source^0'=source^post15, i^0'=i^post15, __const_16^0'=__const_16^post15, y^0'=y^post15, nodecount^0'=nodecount^post15, edgecount^0'=edgecount^post15, x^0'=x^post15, (j^0-j^post15 == 0 /\ source^0-source^post15 == 0 /\ edgecount^0-edgecount^post15 == 0 /\ i^0-i^post15 == 0 /\ 1-source^0+i^0 <= 0 /\ -__const_16^post15+__const_16^0 == 0 /\ -nodecount^post15+nodecount^0 == 0 /\ -x^post15+x^0 == 0 /\ -y^post15+y^0 == 0 /\ __const_5^0-__const_5^post15 == 0), cost: 1 16: l15 -> l12 : j^0'=j^post16, __const_5^0'=__const_5^post16, source^0'=source^post16, i^0'=i^post16, __const_16^0'=__const_16^post16, y^0'=y^post16, nodecount^0'=nodecount^post16, edgecount^0'=edgecount^post16, x^0'=x^post16, (__const_5^0-__const_5^post16 == 0 /\ -y^post16+y^0 == 0 /\ -source^post16+source^0 == 0 /\ nodecount^0-nodecount^post16 == 0 /\ -source^0+i^0 <= 0 /\ -x^post16+x^0 == 0 /\ -__const_16^post16+__const_16^0 == 0 /\ j^0-j^post16 == 0 /\ -edgecount^post16+edgecount^0 == 0 /\ source^0-i^0 <= 0 /\ i^0-i^post16 == 0), cost: 1 23: l16 -> l13 : j^0'=j^post23, __const_5^0'=__const_5^post23, source^0'=source^post23, i^0'=i^post23, __const_16^0'=__const_16^post23, y^0'=y^post23, nodecount^0'=nodecount^post23, edgecount^0'=edgecount^post23, x^0'=x^post23, (-__const_5^post23+__const_5^0 == 0 /\ edgecount^post23-__const_16^0 == 0 /\ __const_16^0-__const_16^post23 == 0 /\ j^0-j^post23 == 0 /\ -x^post23+x^0 == 0 /\ y^0-y^post23 == 0 /\ source^post23 == 0 /\ i^post23 == 0 /\ -__const_5^0+nodecount^post23 == 0), cost: 1 24: l17 -> l16 : j^0'=j^post24, __const_5^0'=__const_5^post24, source^0'=source^post24, i^0'=i^post24, __const_16^0'=__const_16^post24, y^0'=y^post24, nodecount^0'=nodecount^post24, edgecount^0'=edgecount^post24, x^0'=x^post24, (j^0-j^post24 == 0 /\ source^0-source^post24 == 0 /\ -y^post24+y^0 == 0 /\ i^0-i^post24 == 0 /\ edgecount^0-edgecount^post24 == 0 /\ -x^post24+x^0 == 0 /\ -__const_16^post24+__const_16^0 == 0 /\ -nodecount^post24+nodecount^0 == 0 /\ __const_5^0-__const_5^post24 == 0), cost: 1 Applied preprocessing Original rule: l0 -> l2 : j^0'=j^post1, __const_5^0'=__const_5^post1, source^0'=source^post1, i^0'=i^post1, __const_16^0'=__const_16^post1, y^0'=y^post1, nodecount^0'=nodecount^post1, edgecount^0'=edgecount^post1, x^0'=x^post1, (-x^post1+x^0 == 0 /\ -edgecount^post1+edgecount^0 == 0 /\ -nodecount^post1+nodecount^0 == 0 /\ -1-i^0+i^post1 == 0 /\ j^0-j^post1 == 0 /\ 1+i^0-nodecount^0 <= 0 /\ source^0-source^post1 == 0 /\ -__const_5^post1+__const_5^0 == 0 /\ -y^post1+y^0 == 0 /\ -__const_16^post1+__const_16^0 == 0), cost: 1 New rule: l0 -> l2 : i^0'=1+i^0, 1+i^0-nodecount^0 <= 0, cost: 1 Applied preprocessing Original rule: l3 -> l4 : j^0'=j^post2, __const_5^0'=__const_5^post2, source^0'=source^post2, i^0'=i^post2, __const_16^0'=__const_16^post2, y^0'=y^post2, nodecount^0'=nodecount^post2, edgecount^0'=edgecount^post2, x^0'=x^post2, (__const_5^0-__const_5^post2 == 0 /\ edgecount^0-edgecount^post2 == 0 /\ -x^post2+x^0 == 0 /\ -y^post2+y^0 == 0 /\ j^0-j^post2 == 0 /\ source^0-source^post2 == 0 /\ -1-i^0+i^post2 == 0 /\ nodecount^0-nodecount^post2 == 0 /\ -__const_16^post2+__const_16^0 == 0), cost: 1 New rule: l3 -> l4 : i^0'=1+i^0, TRUE, cost: 1 Applied preprocessing Original rule: l5 -> l2 : j^0'=j^post4, __const_5^0'=__const_5^post4, source^0'=source^post4, i^0'=i^post4, __const_16^0'=__const_16^post4, y^0'=y^post4, nodecount^0'=nodecount^post4, edgecount^0'=edgecount^post4, x^0'=x^post4, (i^post4 == 0 /\ j^0-j^post4 == 0 /\ -nodecount^post4+nodecount^0 == 0 /\ -source^post4+source^0 == 0 /\ y^0-y^post4 == 0 /\ -edgecount^post4+edgecount^0 == 0 /\ -x^post4+x^0 == 0 /\ __const_16^0-__const_16^post4 == 0 /\ -i^0+edgecount^0 <= 0 /\ __const_5^0-__const_5^post4 == 0), cost: 1 New rule: l5 -> l2 : i^0'=0, -i^0+edgecount^0 <= 0, cost: 1 Applied preprocessing Original rule: l5 -> l3 : j^0'=j^post5, __const_5^0'=__const_5^post5, source^0'=source^post5, i^0'=i^post5, __const_16^0'=__const_16^post5, y^0'=y^post5, nodecount^0'=nodecount^post5, edgecount^0'=edgecount^post5, x^0'=x^post5, (0 == 0 /\ -i^post5+i^0 == 0 /\ -__const_5^post5+__const_5^0 == 0 /\ 1+i^0-edgecount^0 <= 0 /\ -edgecount^post5+edgecount^0 == 0 /\ j^0-j^post5 == 0 /\ source^0-source^post5 == 0 /\ -nodecount^post5+nodecount^0 == 0 /\ __const_16^0-__const_16^post5 == 0), cost: 1 New rule: l5 -> l3 : y^0'=y^post5, x^0'=x^post5, 1+i^0-edgecount^0 <= 0, cost: 1 Applied preprocessing Original rule: l6 -> l7 : j^0'=j^post6, __const_5^0'=__const_5^post6, source^0'=source^post6, i^0'=i^post6, __const_16^0'=__const_16^post6, y^0'=y^post6, nodecount^0'=nodecount^post6, edgecount^0'=edgecount^post6, x^0'=x^post6, (-y^post6+y^0 == 0 /\ source^0-source^post6 == 0 /\ -1-j^0+j^post6 == 0 /\ -x^post6+x^0 == 0 /\ edgecount^0-edgecount^post6 == 0 /\ __const_5^0-__const_5^post6 == 0 /\ i^0-i^post6 == 0 /\ nodecount^0-nodecount^post6 == 0 /\ -__const_16^post6+__const_16^0 == 0), cost: 1 New rule: l6 -> l7 : j^0'=1+j^0, TRUE, cost: 1 Applied preprocessing Original rule: l8 -> l9 : j^0'=j^post7, __const_5^0'=__const_5^post7, source^0'=source^post7, i^0'=i^post7, __const_16^0'=__const_16^post7, y^0'=y^post7, nodecount^0'=nodecount^post7, edgecount^0'=edgecount^post7, x^0'=x^post7, (__const_5^0-__const_5^post7 == 0 /\ -source^post7+source^0 == 0 /\ -1-i^0+i^post7 == 0 /\ -y^post7+y^0 == 0 /\ -j^0+edgecount^0 <= 0 /\ -__const_16^post7+__const_16^0 == 0 /\ nodecount^0-nodecount^post7 == 0 /\ -edgecount^post7+edgecount^0 == 0 /\ -x^post7+x^0 == 0 /\ -j^post7+j^0 == 0), cost: 1 New rule: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 Applied preprocessing Original rule: l8 -> l6 : j^0'=j^post8, __const_5^0'=__const_5^post8, source^0'=source^post8, i^0'=i^post8, __const_16^0'=__const_16^post8, y^0'=y^post8, nodecount^0'=nodecount^post8, edgecount^0'=edgecount^post8, x^0'=x^post8, (0 == 0 /\ -edgecount^post8+edgecount^0 == 0 /\ 1+j^0-edgecount^0 <= 0 /\ __const_5^0-__const_5^post8 == 0 /\ __const_16^0-__const_16^post8 == 0 /\ nodecount^0-nodecount^post8 == 0 /\ j^0-j^post8 == 0 /\ -i^post8+i^0 == 0 /\ -source^post8+source^0 == 0), cost: 1 New rule: l8 -> l6 : y^0'=y^post8, x^0'=x^post8, 1+j^0-edgecount^0 <= 0, cost: 1 Applied preprocessing Original rule: l10 -> l4 : j^0'=j^post9, __const_5^0'=__const_5^post9, source^0'=source^post9, i^0'=i^post9, __const_16^0'=__const_16^post9, y^0'=y^post9, nodecount^0'=nodecount^post9, edgecount^0'=edgecount^post9, x^0'=x^post9, (-x^post9+x^0 == 0 /\ i^post9 == 0 /\ -edgecount^post9+edgecount^0 == 0 /\ -i^0+nodecount^0 <= 0 /\ __const_16^0-__const_16^post9 == 0 /\ -nodecount^post9+nodecount^0 == 0 /\ y^0-y^post9 == 0 /\ source^0-source^post9 == 0 /\ -__const_5^post9+__const_5^0 == 0 /\ j^0-j^post9 == 0), cost: 1 New rule: l10 -> l4 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 Applied preprocessing Original rule: l10 -> l7 : j^0'=j^post10, __const_5^0'=__const_5^post10, source^0'=source^post10, i^0'=i^post10, __const_16^0'=__const_16^post10, y^0'=y^post10, nodecount^0'=nodecount^post10, edgecount^0'=edgecount^post10, x^0'=x^post10, (source^0-source^post10 == 0 /\ j^post10 == 0 /\ -x^post10+x^0 == 0 /\ i^0-i^post10 == 0 /\ -y^post10+y^0 == 0 /\ edgecount^0-edgecount^post10 == 0 /\ 1+i^0-nodecount^0 <= 0 /\ __const_5^0-__const_5^post10 == 0 /\ -nodecount^post10+nodecount^0 == 0 /\ -__const_16^post10+__const_16^0 == 0), cost: 1 New rule: l10 -> l7 : j^0'=0, 1+i^0-nodecount^0 <= 0, cost: 1 Applied preprocessing Original rule: l11 -> l12 : j^0'=j^post11, __const_5^0'=__const_5^post11, source^0'=source^post11, i^0'=i^post11, __const_16^0'=__const_16^post11, y^0'=y^post11, nodecount^0'=nodecount^post11, edgecount^0'=edgecount^post11, x^0'=x^post11, (edgecount^0-edgecount^post11 == 0 /\ -y^post11+y^0 == 0 /\ nodecount^0-nodecount^post11 == 0 /\ -x^post11+x^0 == 0 /\ __const_5^0-__const_5^post11 == 0 /\ -__const_16^post11+__const_16^0 == 0 /\ i^0-i^post11 == 0 /\ j^0-j^post11 == 0 /\ source^0-source^post11 == 0), cost: 1 New rule: l11 -> l12 : TRUE, cost: 1 Applied preprocessing Original rule: l12 -> l13 : j^0'=j^post12, __const_5^0'=__const_5^post12, source^0'=source^post12, i^0'=i^post12, __const_16^0'=__const_16^post12, y^0'=y^post12, nodecount^0'=nodecount^post12, edgecount^0'=edgecount^post12, x^0'=x^post12, (-x^post12+x^0 == 0 /\ __const_5^0-__const_5^post12 == 0 /\ -edgecount^post12+edgecount^0 == 0 /\ __const_16^0-__const_16^post12 == 0 /\ nodecount^0-nodecount^post12 == 0 /\ j^0-j^post12 == 0 /\ -y^post12+y^0 == 0 /\ -source^post12+source^0 == 0 /\ -1+i^post12-i^0 == 0), cost: 1 New rule: l12 -> l13 : i^0'=1+i^0, TRUE, cost: 1 Applied preprocessing Original rule: l13 -> l14 : j^0'=j^post13, __const_5^0'=__const_5^post13, source^0'=source^post13, i^0'=i^post13, __const_16^0'=__const_16^post13, y^0'=y^post13, nodecount^0'=nodecount^post13, edgecount^0'=edgecount^post13, x^0'=x^post13, (-edgecount^post13+edgecount^0 == 0 /\ __const_5^0-__const_5^post13 == 0 /\ -nodecount^post13+nodecount^0 == 0 /\ y^0-y^post13 == 0 /\ -i^post13+i^0 == 0 /\ j^0-j^post13 == 0 /\ source^0-source^post13 == 0 /\ -x^post13+x^0 == 0 /\ __const_16^0-__const_16^post13 == 0), cost: 1 New rule: l13 -> l14 : TRUE, cost: 1 Applied preprocessing Original rule: l15 -> l11 : j^0'=j^post14, __const_5^0'=__const_5^post14, source^0'=source^post14, i^0'=i^post14, __const_16^0'=__const_16^post14, y^0'=y^post14, nodecount^0'=nodecount^post14, edgecount^0'=edgecount^post14, x^0'=x^post14, (-nodecount^post14+nodecount^0 == 0 /\ -__const_16^post14+__const_16^0 == 0 /\ j^0-j^post14 == 0 /\ source^0-source^post14 == 0 /\ -edgecount^post14+edgecount^0 == 0 /\ i^0-i^post14 == 0 /\ 1+source^0-i^0 <= 0 /\ __const_5^0-__const_5^post14 == 0 /\ -x^post14+x^0 == 0 /\ -y^post14+y^0 == 0), cost: 1 New rule: l15 -> l11 : 1+source^0-i^0 <= 0, cost: 1 Applied preprocessing Original rule: l15 -> l11 : j^0'=j^post15, __const_5^0'=__const_5^post15, source^0'=source^post15, i^0'=i^post15, __const_16^0'=__const_16^post15, y^0'=y^post15, nodecount^0'=nodecount^post15, edgecount^0'=edgecount^post15, x^0'=x^post15, (j^0-j^post15 == 0 /\ source^0-source^post15 == 0 /\ edgecount^0-edgecount^post15 == 0 /\ i^0-i^post15 == 0 /\ 1-source^0+i^0 <= 0 /\ -__const_16^post15+__const_16^0 == 0 /\ -nodecount^post15+nodecount^0 == 0 /\ -x^post15+x^0 == 0 /\ -y^post15+y^0 == 0 /\ __const_5^0-__const_5^post15 == 0), cost: 1 New rule: l15 -> l11 : 1-source^0+i^0 <= 0, cost: 1 Applied preprocessing Original rule: l15 -> l12 : j^0'=j^post16, __const_5^0'=__const_5^post16, source^0'=source^post16, i^0'=i^post16, __const_16^0'=__const_16^post16, y^0'=y^post16, nodecount^0'=nodecount^post16, edgecount^0'=edgecount^post16, x^0'=x^post16, (__const_5^0-__const_5^post16 == 0 /\ -y^post16+y^0 == 0 /\ -source^post16+source^0 == 0 /\ nodecount^0-nodecount^post16 == 0 /\ -source^0+i^0 <= 0 /\ -x^post16+x^0 == 0 /\ -__const_16^post16+__const_16^0 == 0 /\ j^0-j^post16 == 0 /\ -edgecount^post16+edgecount^0 == 0 /\ source^0-i^0 <= 0 /\ i^0-i^post16 == 0), cost: 1 New rule: l15 -> l12 : -source^0+i^0 == 0, cost: 1 Applied preprocessing Original rule: l14 -> l9 : j^0'=j^post17, __const_5^0'=__const_5^post17, source^0'=source^post17, i^0'=i^post17, __const_16^0'=__const_16^post17, y^0'=y^post17, nodecount^0'=nodecount^post17, edgecount^0'=edgecount^post17, x^0'=x^post17, (-source^post17+source^0 == 0 /\ __const_16^0-__const_16^post17 == 0 /\ i^post17 == 0 /\ -i^0+nodecount^0 <= 0 /\ y^0-y^post17 == 0 /\ -x^post17+x^0 == 0 /\ -nodecount^post17+nodecount^0 == 0 /\ __const_5^0-__const_5^post17 == 0 /\ -edgecount^post17+edgecount^0 == 0 /\ j^0-j^post17 == 0), cost: 1 New rule: l14 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 Applied preprocessing Original rule: l14 -> l15 : j^0'=j^post18, __const_5^0'=__const_5^post18, source^0'=source^post18, i^0'=i^post18, __const_16^0'=__const_16^post18, y^0'=y^post18, nodecount^0'=nodecount^post18, edgecount^0'=edgecount^post18, x^0'=x^post18, (__const_5^0-__const_5^post18 == 0 /\ -x^post18+x^0 == 0 /\ 1+i^0-nodecount^0 <= 0 /\ -nodecount^post18+nodecount^0 == 0 /\ j^0-j^post18 == 0 /\ __const_16^0-__const_16^post18 == 0 /\ y^0-y^post18 == 0 /\ i^0-i^post18 == 0 /\ source^0-source^post18 == 0 /\ -edgecount^post18+edgecount^0 == 0), cost: 1 New rule: l14 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 1 Applied preprocessing Original rule: l9 -> l10 : j^0'=j^post19, __const_5^0'=__const_5^post19, source^0'=source^post19, i^0'=i^post19, __const_16^0'=__const_16^post19, y^0'=y^post19, nodecount^0'=nodecount^post19, edgecount^0'=edgecount^post19, x^0'=x^post19, (-__const_16^post19+__const_16^0 == 0 /\ -edgecount^post19+edgecount^0 == 0 /\ -nodecount^post19+nodecount^0 == 0 /\ -x^post19+x^0 == 0 /\ j^0-j^post19 == 0 /\ source^0-source^post19 == 0 /\ i^0-i^post19 == 0 /\ -__const_5^post19+__const_5^0 == 0 /\ -y^post19+y^0 == 0), cost: 1 New rule: l9 -> l10 : TRUE, cost: 1 Applied preprocessing Original rule: l7 -> l8 : j^0'=j^post20, __const_5^0'=__const_5^post20, source^0'=source^post20, i^0'=i^post20, __const_16^0'=__const_16^post20, y^0'=y^post20, nodecount^0'=nodecount^post20, edgecount^0'=edgecount^post20, x^0'=x^post20, (i^0-i^post20 == 0 /\ -__const_16^post20+__const_16^0 == 0 /\ __const_5^0-__const_5^post20 == 0 /\ -source^post20+source^0 == 0 /\ -x^post20+x^0 == 0 /\ -edgecount^post20+edgecount^0 == 0 /\ j^0-j^post20 == 0 /\ -y^post20+y^0 == 0 /\ nodecount^0-nodecount^post20 == 0), cost: 1 New rule: l7 -> l8 : TRUE, cost: 1 Applied preprocessing Original rule: l4 -> l5 : j^0'=j^post21, __const_5^0'=__const_5^post21, source^0'=source^post21, i^0'=i^post21, __const_16^0'=__const_16^post21, y^0'=y^post21, nodecount^0'=nodecount^post21, edgecount^0'=edgecount^post21, x^0'=x^post21, (y^0-y^post21 == 0 /\ j^0-j^post21 == 0 /\ -i^post21+i^0 == 0 /\ -edgecount^post21+edgecount^0 == 0 /\ __const_16^0-__const_16^post21 == 0 /\ -source^post21+source^0 == 0 /\ __const_5^0-__const_5^post21 == 0 /\ -x^post21+x^0 == 0 /\ -nodecount^post21+nodecount^0 == 0), cost: 1 New rule: l4 -> l5 : TRUE, cost: 1 Applied preprocessing Original rule: l2 -> l0 : j^0'=j^post22, __const_5^0'=__const_5^post22, source^0'=source^post22, i^0'=i^post22, __const_16^0'=__const_16^post22, y^0'=y^post22, nodecount^0'=nodecount^post22, edgecount^0'=edgecount^post22, x^0'=x^post22, (__const_16^0-__const_16^post22 == 0 /\ -source^post22+source^0 == 0 /\ -i^post22+i^0 == 0 /\ -x^post22+x^0 == 0 /\ y^0-y^post22 == 0 /\ -nodecount^post22+nodecount^0 == 0 /\ __const_5^0-__const_5^post22 == 0 /\ j^0-j^post22 == 0 /\ -edgecount^post22+edgecount^0 == 0), cost: 1 New rule: l2 -> l0 : TRUE, cost: 1 Applied preprocessing Original rule: l16 -> l13 : j^0'=j^post23, __const_5^0'=__const_5^post23, source^0'=source^post23, i^0'=i^post23, __const_16^0'=__const_16^post23, y^0'=y^post23, nodecount^0'=nodecount^post23, edgecount^0'=edgecount^post23, x^0'=x^post23, (-__const_5^post23+__const_5^0 == 0 /\ edgecount^post23-__const_16^0 == 0 /\ __const_16^0-__const_16^post23 == 0 /\ j^0-j^post23 == 0 /\ -x^post23+x^0 == 0 /\ y^0-y^post23 == 0 /\ source^post23 == 0 /\ i^post23 == 0 /\ -__const_5^0+nodecount^post23 == 0), cost: 1 New rule: l16 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 1 Applied preprocessing Original rule: l17 -> l16 : j^0'=j^post24, __const_5^0'=__const_5^post24, source^0'=source^post24, i^0'=i^post24, __const_16^0'=__const_16^post24, y^0'=y^post24, nodecount^0'=nodecount^post24, edgecount^0'=edgecount^post24, x^0'=x^post24, (j^0-j^post24 == 0 /\ source^0-source^post24 == 0 /\ -y^post24+y^0 == 0 /\ i^0-i^post24 == 0 /\ edgecount^0-edgecount^post24 == 0 /\ -x^post24+x^0 == 0 /\ -__const_16^post24+__const_16^0 == 0 /\ -nodecount^post24+nodecount^0 == 0 /\ __const_5^0-__const_5^post24 == 0), cost: 1 New rule: l17 -> l16 : TRUE, cost: 1 Simplified rules Start location: l17 25: l0 -> l2 : i^0'=1+i^0, 1+i^0-nodecount^0 <= 0, cost: 1 45: l2 -> l0 : TRUE, cost: 1 26: l3 -> l4 : i^0'=1+i^0, TRUE, cost: 1 44: l4 -> l5 : TRUE, cost: 1 27: l5 -> l2 : i^0'=0, -i^0+edgecount^0 <= 0, cost: 1 28: l5 -> l3 : y^0'=y^post5, x^0'=x^post5, 1+i^0-edgecount^0 <= 0, cost: 1 29: l6 -> l7 : j^0'=1+j^0, TRUE, cost: 1 43: l7 -> l8 : TRUE, cost: 1 30: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 31: l8 -> l6 : y^0'=y^post8, x^0'=x^post8, 1+j^0-edgecount^0 <= 0, cost: 1 42: l9 -> l10 : TRUE, cost: 1 32: l10 -> l4 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 33: l10 -> l7 : j^0'=0, 1+i^0-nodecount^0 <= 0, cost: 1 34: l11 -> l12 : TRUE, cost: 1 35: l12 -> l13 : i^0'=1+i^0, TRUE, cost: 1 36: l13 -> l14 : TRUE, cost: 1 40: l14 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 41: l14 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 1 37: l15 -> l11 : 1+source^0-i^0 <= 0, cost: 1 38: l15 -> l11 : 1-source^0+i^0 <= 0, cost: 1 39: l15 -> l12 : -source^0+i^0 == 0, cost: 1 46: l16 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 1 47: l17 -> l16 : TRUE, cost: 1 Eliminating location l16 by chaining: Applied chaining First rule: l17 -> l16 : TRUE, cost: 1 Second rule: l16 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 1 New rule: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 Applied deletion Removed the following rules: 46 47 Eliminating location l3 by chaining: Applied chaining First rule: l5 -> l3 : y^0'=y^post5, x^0'=x^post5, 1+i^0-edgecount^0 <= 0, cost: 1 Second rule: l3 -> l4 : i^0'=1+i^0, TRUE, cost: 1 New rule: l5 -> l4 : i^0'=1+i^0, y^0'=y^post5, x^0'=x^post5, 1+i^0-edgecount^0 <= 0, cost: 2 Applied deletion Removed the following rules: 26 28 Eliminating location l0 by chaining: Applied chaining First rule: l2 -> l0 : TRUE, cost: 1 Second rule: l0 -> l2 : i^0'=1+i^0, 1+i^0-nodecount^0 <= 0, cost: 1 New rule: l2 -> l2 : i^0'=1+i^0, 1+i^0-nodecount^0 <= 0, cost: 2 Applied deletion Removed the following rules: 25 45 Eliminating location l6 by chaining: Applied chaining First rule: l8 -> l6 : y^0'=y^post8, x^0'=x^post8, 1+j^0-edgecount^0 <= 0, cost: 1 Second rule: l6 -> l7 : j^0'=1+j^0, TRUE, cost: 1 New rule: l8 -> l7 : j^0'=1+j^0, y^0'=y^post8, x^0'=x^post8, 1+j^0-edgecount^0 <= 0, cost: 2 Applied deletion Removed the following rules: 29 31 Eliminated locations on linear paths Start location: l17 50: l2 -> l2 : i^0'=1+i^0, 1+i^0-nodecount^0 <= 0, cost: 2 44: l4 -> l5 : TRUE, cost: 1 27: l5 -> l2 : i^0'=0, -i^0+edgecount^0 <= 0, cost: 1 49: l5 -> l4 : i^0'=1+i^0, y^0'=y^post5, x^0'=x^post5, 1+i^0-edgecount^0 <= 0, cost: 2 43: l7 -> l8 : TRUE, cost: 1 30: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 51: l8 -> l7 : j^0'=1+j^0, y^0'=y^post8, x^0'=x^post8, 1+j^0-edgecount^0 <= 0, cost: 2 42: l9 -> l10 : TRUE, cost: 1 32: l10 -> l4 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 33: l10 -> l7 : j^0'=0, 1+i^0-nodecount^0 <= 0, cost: 1 34: l11 -> l12 : TRUE, cost: 1 35: l12 -> l13 : i^0'=1+i^0, TRUE, cost: 1 36: l13 -> l14 : TRUE, cost: 1 40: l14 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 41: l14 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 1 37: l15 -> l11 : 1+source^0-i^0 <= 0, cost: 1 38: l15 -> l11 : 1-source^0+i^0 <= 0, cost: 1 39: l15 -> l12 : -source^0+i^0 == 0, cost: 1 48: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 Applied acceleration Original rule: l2 -> l2 : i^0'=1+i^0, 1+i^0-nodecount^0 <= 0, cost: 2 New rule: l2 -> l2 : i^0'=n+i^0, (n >= 0 /\ -n-i^0+nodecount^0 >= 0), cost: 2*n Sub-proof via acceration calculus written to file:///tmp/tmpnam_gDlgaJ.txt Applied instantiation Original rule: l2 -> l2 : i^0'=n+i^0, (n >= 0 /\ -n-i^0+nodecount^0 >= 0), cost: 2*n New rule: l2 -> l2 : i^0'=nodecount^0, (0 >= 0 /\ -i^0+nodecount^0 >= 0), cost: -2*i^0+2*nodecount^0 Applied simplification Original rule: l2 -> l2 : i^0'=nodecount^0, (0 >= 0 /\ -i^0+nodecount^0 >= 0), cost: -2*i^0+2*nodecount^0 New rule: l2 -> l2 : i^0'=nodecount^0, -i^0+nodecount^0 >= 0, cost: -2*i^0+2*nodecount^0 Applied deletion Removed the following rules: 50 Accelerated simple loops Start location: l17 53: l2 -> l2 : i^0'=nodecount^0, -i^0+nodecount^0 >= 0, cost: -2*i^0+2*nodecount^0 44: l4 -> l5 : TRUE, cost: 1 27: l5 -> l2 : i^0'=0, -i^0+edgecount^0 <= 0, cost: 1 49: l5 -> l4 : i^0'=1+i^0, y^0'=y^post5, x^0'=x^post5, 1+i^0-edgecount^0 <= 0, cost: 2 43: l7 -> l8 : TRUE, cost: 1 30: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 51: l8 -> l7 : j^0'=1+j^0, y^0'=y^post8, x^0'=x^post8, 1+j^0-edgecount^0 <= 0, cost: 2 42: l9 -> l10 : TRUE, cost: 1 32: l10 -> l4 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 33: l10 -> l7 : j^0'=0, 1+i^0-nodecount^0 <= 0, cost: 1 34: l11 -> l12 : TRUE, cost: 1 35: l12 -> l13 : i^0'=1+i^0, TRUE, cost: 1 36: l13 -> l14 : TRUE, cost: 1 40: l14 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 41: l14 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 1 37: l15 -> l11 : 1+source^0-i^0 <= 0, cost: 1 38: l15 -> l11 : 1-source^0+i^0 <= 0, cost: 1 39: l15 -> l12 : -source^0+i^0 == 0, cost: 1 48: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 Applied chaining First rule: l5 -> l2 : i^0'=0, -i^0+edgecount^0 <= 0, cost: 1 Second rule: l2 -> l2 : i^0'=nodecount^0, -i^0+nodecount^0 >= 0, cost: -2*i^0+2*nodecount^0 New rule: l5 -> l2 : i^0'=nodecount^0, (nodecount^0 >= 0 /\ -i^0+edgecount^0 <= 0), cost: 1+2*nodecount^0 Applied deletion Removed the following rules: 53 Chained accelerated rules with incoming rules Start location: l17 44: l4 -> l5 : TRUE, cost: 1 27: l5 -> l2 : i^0'=0, -i^0+edgecount^0 <= 0, cost: 1 49: l5 -> l4 : i^0'=1+i^0, y^0'=y^post5, x^0'=x^post5, 1+i^0-edgecount^0 <= 0, cost: 2 54: l5 -> l2 : i^0'=nodecount^0, (nodecount^0 >= 0 /\ -i^0+edgecount^0 <= 0), cost: 1+2*nodecount^0 43: l7 -> l8 : TRUE, cost: 1 30: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 51: l8 -> l7 : j^0'=1+j^0, y^0'=y^post8, x^0'=x^post8, 1+j^0-edgecount^0 <= 0, cost: 2 42: l9 -> l10 : TRUE, cost: 1 32: l10 -> l4 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 33: l10 -> l7 : j^0'=0, 1+i^0-nodecount^0 <= 0, cost: 1 34: l11 -> l12 : TRUE, cost: 1 35: l12 -> l13 : i^0'=1+i^0, TRUE, cost: 1 36: l13 -> l14 : TRUE, cost: 1 40: l14 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 41: l14 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 1 37: l15 -> l11 : 1+source^0-i^0 <= 0, cost: 1 38: l15 -> l11 : 1-source^0+i^0 <= 0, cost: 1 39: l15 -> l12 : -source^0+i^0 == 0, cost: 1 48: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l17 44: l4 -> l5 : TRUE, cost: 1 49: l5 -> l4 : i^0'=1+i^0, y^0'=y^post5, x^0'=x^post5, 1+i^0-edgecount^0 <= 0, cost: 2 43: l7 -> l8 : TRUE, cost: 1 30: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 51: l8 -> l7 : j^0'=1+j^0, y^0'=y^post8, x^0'=x^post8, 1+j^0-edgecount^0 <= 0, cost: 2 42: l9 -> l10 : TRUE, cost: 1 32: l10 -> l4 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 33: l10 -> l7 : j^0'=0, 1+i^0-nodecount^0 <= 0, cost: 1 34: l11 -> l12 : TRUE, cost: 1 35: l12 -> l13 : i^0'=1+i^0, TRUE, cost: 1 36: l13 -> l14 : TRUE, cost: 1 40: l14 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 41: l14 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 1 37: l15 -> l11 : 1+source^0-i^0 <= 0, cost: 1 38: l15 -> l11 : 1-source^0+i^0 <= 0, cost: 1 39: l15 -> l12 : -source^0+i^0 == 0, cost: 1 48: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 Eliminating location l5 by chaining: Applied chaining First rule: l4 -> l5 : TRUE, cost: 1 Second rule: l5 -> l4 : i^0'=1+i^0, y^0'=y^post5, x^0'=x^post5, 1+i^0-edgecount^0 <= 0, cost: 2 New rule: l4 -> l4 : i^0'=1+i^0, y^0'=y^post5, x^0'=x^post5, 1+i^0-edgecount^0 <= 0, cost: 3 Applied deletion Removed the following rules: 44 49 Eliminated locations on linear paths Start location: l17 55: l4 -> l4 : i^0'=1+i^0, y^0'=y^post5, x^0'=x^post5, 1+i^0-edgecount^0 <= 0, cost: 3 43: l7 -> l8 : TRUE, cost: 1 30: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 51: l8 -> l7 : j^0'=1+j^0, y^0'=y^post8, x^0'=x^post8, 1+j^0-edgecount^0 <= 0, cost: 2 42: l9 -> l10 : TRUE, cost: 1 32: l10 -> l4 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 33: l10 -> l7 : j^0'=0, 1+i^0-nodecount^0 <= 0, cost: 1 34: l11 -> l12 : TRUE, cost: 1 35: l12 -> l13 : i^0'=1+i^0, TRUE, cost: 1 36: l13 -> l14 : TRUE, cost: 1 40: l14 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 41: l14 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 1 37: l15 -> l11 : 1+source^0-i^0 <= 0, cost: 1 38: l15 -> l11 : 1-source^0+i^0 <= 0, cost: 1 39: l15 -> l12 : -source^0+i^0 == 0, cost: 1 48: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 Applied acceleration Original rule: l4 -> l4 : i^0'=1+i^0, y^0'=y^post5, x^0'=x^post5, 1+i^0-edgecount^0 <= 0, cost: 3 New rule: l4 -> l4 : i^0'=i^0+n0, y^0'=y^post5, x^0'=x^post5, (-i^0-n0+edgecount^0 >= 0 /\ -1+n0 >= 0), cost: 3*n0 Sub-proof via acceration calculus written to file:///tmp/tmpnam_iBINdL.txt Applied instantiation Original rule: l4 -> l4 : i^0'=i^0+n0, y^0'=y^post5, x^0'=x^post5, (-i^0-n0+edgecount^0 >= 0 /\ -1+n0 >= 0), cost: 3*n0 New rule: l4 -> l4 : i^0'=edgecount^0, y^0'=y^post5, x^0'=x^post5, (0 >= 0 /\ -1-i^0+edgecount^0 >= 0), cost: -3*i^0+3*edgecount^0 Applied simplification Original rule: l4 -> l4 : i^0'=edgecount^0, y^0'=y^post5, x^0'=x^post5, (0 >= 0 /\ -1-i^0+edgecount^0 >= 0), cost: -3*i^0+3*edgecount^0 New rule: l4 -> l4 : i^0'=edgecount^0, y^0'=y^post5, x^0'=x^post5, -1-i^0+edgecount^0 >= 0, cost: -3*i^0+3*edgecount^0 Applied deletion Removed the following rules: 55 Accelerated simple loops Start location: l17 57: l4 -> l4 : i^0'=edgecount^0, y^0'=y^post5, x^0'=x^post5, -1-i^0+edgecount^0 >= 0, cost: -3*i^0+3*edgecount^0 43: l7 -> l8 : TRUE, cost: 1 30: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 51: l8 -> l7 : j^0'=1+j^0, y^0'=y^post8, x^0'=x^post8, 1+j^0-edgecount^0 <= 0, cost: 2 42: l9 -> l10 : TRUE, cost: 1 32: l10 -> l4 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 33: l10 -> l7 : j^0'=0, 1+i^0-nodecount^0 <= 0, cost: 1 34: l11 -> l12 : TRUE, cost: 1 35: l12 -> l13 : i^0'=1+i^0, TRUE, cost: 1 36: l13 -> l14 : TRUE, cost: 1 40: l14 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 41: l14 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 1 37: l15 -> l11 : 1+source^0-i^0 <= 0, cost: 1 38: l15 -> l11 : 1-source^0+i^0 <= 0, cost: 1 39: l15 -> l12 : -source^0+i^0 == 0, cost: 1 48: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 Applied chaining First rule: l10 -> l4 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 Second rule: l4 -> l4 : i^0'=edgecount^0, y^0'=y^post5, x^0'=x^post5, -1-i^0+edgecount^0 >= 0, cost: -3*i^0+3*edgecount^0 New rule: l10 -> l4 : i^0'=edgecount^0, y^0'=y^post5, x^0'=x^post5, (-i^0+nodecount^0 <= 0 /\ -1+edgecount^0 >= 0), cost: 1+3*edgecount^0 Applied deletion Removed the following rules: 57 Chained accelerated rules with incoming rules Start location: l17 43: l7 -> l8 : TRUE, cost: 1 30: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 51: l8 -> l7 : j^0'=1+j^0, y^0'=y^post8, x^0'=x^post8, 1+j^0-edgecount^0 <= 0, cost: 2 42: l9 -> l10 : TRUE, cost: 1 32: l10 -> l4 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 33: l10 -> l7 : j^0'=0, 1+i^0-nodecount^0 <= 0, cost: 1 58: l10 -> l4 : i^0'=edgecount^0, y^0'=y^post5, x^0'=x^post5, (-i^0+nodecount^0 <= 0 /\ -1+edgecount^0 >= 0), cost: 1+3*edgecount^0 34: l11 -> l12 : TRUE, cost: 1 35: l12 -> l13 : i^0'=1+i^0, TRUE, cost: 1 36: l13 -> l14 : TRUE, cost: 1 40: l14 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 41: l14 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 1 37: l15 -> l11 : 1+source^0-i^0 <= 0, cost: 1 38: l15 -> l11 : 1-source^0+i^0 <= 0, cost: 1 39: l15 -> l12 : -source^0+i^0 == 0, cost: 1 48: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l17 43: l7 -> l8 : TRUE, cost: 1 30: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 51: l8 -> l7 : j^0'=1+j^0, y^0'=y^post8, x^0'=x^post8, 1+j^0-edgecount^0 <= 0, cost: 2 42: l9 -> l10 : TRUE, cost: 1 33: l10 -> l7 : j^0'=0, 1+i^0-nodecount^0 <= 0, cost: 1 34: l11 -> l12 : TRUE, cost: 1 35: l12 -> l13 : i^0'=1+i^0, TRUE, cost: 1 36: l13 -> l14 : TRUE, cost: 1 40: l14 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 41: l14 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 1 37: l15 -> l11 : 1+source^0-i^0 <= 0, cost: 1 38: l15 -> l11 : 1-source^0+i^0 <= 0, cost: 1 39: l15 -> l12 : -source^0+i^0 == 0, cost: 1 48: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 Eliminating location l10 by chaining: Applied chaining First rule: l9 -> l10 : TRUE, cost: 1 Second rule: l10 -> l7 : j^0'=0, 1+i^0-nodecount^0 <= 0, cost: 1 New rule: l9 -> l7 : j^0'=0, 1+i^0-nodecount^0 <= 0, cost: 2 Applied deletion Removed the following rules: 33 42 Eliminated locations on linear paths Start location: l17 43: l7 -> l8 : TRUE, cost: 1 30: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 51: l8 -> l7 : j^0'=1+j^0, y^0'=y^post8, x^0'=x^post8, 1+j^0-edgecount^0 <= 0, cost: 2 59: l9 -> l7 : j^0'=0, 1+i^0-nodecount^0 <= 0, cost: 2 34: l11 -> l12 : TRUE, cost: 1 35: l12 -> l13 : i^0'=1+i^0, TRUE, cost: 1 36: l13 -> l14 : TRUE, cost: 1 40: l14 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 41: l14 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 1 37: l15 -> l11 : 1+source^0-i^0 <= 0, cost: 1 38: l15 -> l11 : 1-source^0+i^0 <= 0, cost: 1 39: l15 -> l12 : -source^0+i^0 == 0, cost: 1 48: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 Eliminating location l14 by chaining: Applied chaining First rule: l13 -> l14 : TRUE, cost: 1 Second rule: l14 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1 New rule: l13 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 2 Applied chaining First rule: l13 -> l14 : TRUE, cost: 1 Second rule: l14 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 1 New rule: l13 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 2 Applied deletion Removed the following rules: 36 40 41 Eliminating location l8 by chaining: Applied chaining First rule: l7 -> l8 : TRUE, cost: 1 Second rule: l8 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 1 New rule: l7 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 2 Applied chaining First rule: l7 -> l8 : TRUE, cost: 1 Second rule: l8 -> l7 : j^0'=1+j^0, y^0'=y^post8, x^0'=x^post8, 1+j^0-edgecount^0 <= 0, cost: 2 New rule: l7 -> l7 : j^0'=1+j^0, y^0'=y^post8, x^0'=x^post8, 1+j^0-edgecount^0 <= 0, cost: 3 Applied deletion Removed the following rules: 30 43 51 Eliminating location l11 by chaining: Applied chaining First rule: l15 -> l11 : 1+source^0-i^0 <= 0, cost: 1 Second rule: l11 -> l12 : TRUE, cost: 1 New rule: l15 -> l12 : 1+source^0-i^0 <= 0, cost: 2 Applied chaining First rule: l15 -> l11 : 1-source^0+i^0 <= 0, cost: 1 Second rule: l11 -> l12 : TRUE, cost: 1 New rule: l15 -> l12 : 1-source^0+i^0 <= 0, cost: 2 Applied deletion Removed the following rules: 34 37 38 Eliminating location l12 by chaining: Applied chaining First rule: l15 -> l12 : -source^0+i^0 == 0, cost: 1 Second rule: l12 -> l13 : i^0'=1+i^0, TRUE, cost: 1 New rule: l15 -> l13 : i^0'=1+i^0, -source^0+i^0 == 0, cost: 2 Applied chaining First rule: l15 -> l12 : 1+source^0-i^0 <= 0, cost: 2 Second rule: l12 -> l13 : i^0'=1+i^0, TRUE, cost: 1 New rule: l15 -> l13 : i^0'=1+i^0, 1+source^0-i^0 <= 0, cost: 3 Applied chaining First rule: l15 -> l12 : 1-source^0+i^0 <= 0, cost: 2 Second rule: l12 -> l13 : i^0'=1+i^0, TRUE, cost: 1 New rule: l15 -> l13 : i^0'=1+i^0, 1-source^0+i^0 <= 0, cost: 3 Applied deletion Removed the following rules: 35 39 64 65 Eliminated locations on tree-shaped paths Start location: l17 62: l7 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 2 63: l7 -> l7 : j^0'=1+j^0, y^0'=y^post8, x^0'=x^post8, 1+j^0-edgecount^0 <= 0, cost: 3 59: l9 -> l7 : j^0'=0, 1+i^0-nodecount^0 <= 0, cost: 2 60: l13 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 2 61: l13 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 2 66: l15 -> l13 : i^0'=1+i^0, -source^0+i^0 == 0, cost: 2 67: l15 -> l13 : i^0'=1+i^0, 1+source^0-i^0 <= 0, cost: 3 68: l15 -> l13 : i^0'=1+i^0, 1-source^0+i^0 <= 0, cost: 3 48: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 Applied acceleration Original rule: l7 -> l7 : j^0'=1+j^0, y^0'=y^post8, x^0'=x^post8, 1+j^0-edgecount^0 <= 0, cost: 3 New rule: l7 -> l7 : j^0'=j^0+n1, y^0'=y^post8, x^0'=x^post8, (-j^0-n1+edgecount^0 >= 0 /\ -1+n1 >= 0), cost: 3*n1 Sub-proof via acceration calculus written to file:///tmp/tmpnam_bKLlkK.txt Applied instantiation Original rule: l7 -> l7 : j^0'=j^0+n1, y^0'=y^post8, x^0'=x^post8, (-j^0-n1+edgecount^0 >= 0 /\ -1+n1 >= 0), cost: 3*n1 New rule: l7 -> l7 : j^0'=edgecount^0, y^0'=y^post8, x^0'=x^post8, (0 >= 0 /\ -1-j^0+edgecount^0 >= 0), cost: -3*j^0+3*edgecount^0 Applied simplification Original rule: l7 -> l7 : j^0'=edgecount^0, y^0'=y^post8, x^0'=x^post8, (0 >= 0 /\ -1-j^0+edgecount^0 >= 0), cost: -3*j^0+3*edgecount^0 New rule: l7 -> l7 : j^0'=edgecount^0, y^0'=y^post8, x^0'=x^post8, -1-j^0+edgecount^0 >= 0, cost: -3*j^0+3*edgecount^0 Applied deletion Removed the following rules: 63 Accelerated simple loops Start location: l17 62: l7 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 2 70: l7 -> l7 : j^0'=edgecount^0, y^0'=y^post8, x^0'=x^post8, -1-j^0+edgecount^0 >= 0, cost: -3*j^0+3*edgecount^0 59: l9 -> l7 : j^0'=0, 1+i^0-nodecount^0 <= 0, cost: 2 60: l13 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 2 61: l13 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 2 66: l15 -> l13 : i^0'=1+i^0, -source^0+i^0 == 0, cost: 2 67: l15 -> l13 : i^0'=1+i^0, 1+source^0-i^0 <= 0, cost: 3 68: l15 -> l13 : i^0'=1+i^0, 1-source^0+i^0 <= 0, cost: 3 48: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 Applied chaining First rule: l9 -> l7 : j^0'=0, 1+i^0-nodecount^0 <= 0, cost: 2 Second rule: l7 -> l7 : j^0'=edgecount^0, y^0'=y^post8, x^0'=x^post8, -1-j^0+edgecount^0 >= 0, cost: -3*j^0+3*edgecount^0 New rule: l9 -> l7 : j^0'=edgecount^0, y^0'=y^post8, x^0'=x^post8, (-1+edgecount^0 >= 0 /\ 1+i^0-nodecount^0 <= 0), cost: 2+3*edgecount^0 Applied deletion Removed the following rules: 70 Chained accelerated rules with incoming rules Start location: l17 62: l7 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 2 59: l9 -> l7 : j^0'=0, 1+i^0-nodecount^0 <= 0, cost: 2 71: l9 -> l7 : j^0'=edgecount^0, y^0'=y^post8, x^0'=x^post8, (-1+edgecount^0 >= 0 /\ 1+i^0-nodecount^0 <= 0), cost: 2+3*edgecount^0 60: l13 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 2 61: l13 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 2 66: l15 -> l13 : i^0'=1+i^0, -source^0+i^0 == 0, cost: 2 67: l15 -> l13 : i^0'=1+i^0, 1+source^0-i^0 <= 0, cost: 3 68: l15 -> l13 : i^0'=1+i^0, 1-source^0+i^0 <= 0, cost: 3 48: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 Eliminating location l15 by chaining: Applied chaining First rule: l13 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 2 Second rule: l15 -> l13 : i^0'=1+i^0, -source^0+i^0 == 0, cost: 2 New rule: l13 -> l13 : i^0'=1+i^0, (1+i^0-nodecount^0 <= 0 /\ -source^0+i^0 == 0), cost: 4 Applied chaining First rule: l13 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 2 Second rule: l15 -> l13 : i^0'=1+i^0, 1+source^0-i^0 <= 0, cost: 3 New rule: l13 -> l13 : i^0'=1+i^0, (1+i^0-nodecount^0 <= 0 /\ 1+source^0-i^0 <= 0), cost: 5 Applied chaining First rule: l13 -> l15 : 1+i^0-nodecount^0 <= 0, cost: 2 Second rule: l15 -> l13 : i^0'=1+i^0, 1-source^0+i^0 <= 0, cost: 3 New rule: l13 -> l13 : i^0'=1+i^0, (1+i^0-nodecount^0 <= 0 /\ 1-source^0+i^0 <= 0), cost: 5 Applied deletion Removed the following rules: 61 66 67 68 Eliminating location l7 by chaining: Applied chaining First rule: l9 -> l7 : j^0'=0, 1+i^0-nodecount^0 <= 0, cost: 2 Second rule: l7 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 2 New rule: l9 -> l9 : j^0'=0, i^0'=1+i^0, (1+i^0-nodecount^0 <= 0 /\ edgecount^0 <= 0), cost: 4 Applied chaining First rule: l9 -> l7 : j^0'=edgecount^0, y^0'=y^post8, x^0'=x^post8, (-1+edgecount^0 >= 0 /\ 1+i^0-nodecount^0 <= 0), cost: 2+3*edgecount^0 Second rule: l7 -> l9 : i^0'=1+i^0, -j^0+edgecount^0 <= 0, cost: 2 New rule: l9 -> l9 : j^0'=edgecount^0, i^0'=1+i^0, y^0'=y^post8, x^0'=x^post8, (0 <= 0 /\ -1+edgecount^0 >= 0 /\ 1+i^0-nodecount^0 <= 0), cost: 4+3*edgecount^0 Applied simplification Original rule: l9 -> l9 : j^0'=edgecount^0, i^0'=1+i^0, y^0'=y^post8, x^0'=x^post8, (0 <= 0 /\ -1+edgecount^0 >= 0 /\ 1+i^0-nodecount^0 <= 0), cost: 4+3*edgecount^0 New rule: l9 -> l9 : j^0'=edgecount^0, i^0'=1+i^0, y^0'=y^post8, x^0'=x^post8, (-1+edgecount^0 >= 0 /\ 1+i^0-nodecount^0 <= 0), cost: 4+3*edgecount^0 Applied deletion Removed the following rules: 59 62 71 Eliminated locations on tree-shaped paths Start location: l17 75: l9 -> l9 : j^0'=0, i^0'=1+i^0, (1+i^0-nodecount^0 <= 0 /\ edgecount^0 <= 0), cost: 4 76: l9 -> l9 : j^0'=edgecount^0, i^0'=1+i^0, y^0'=y^post8, x^0'=x^post8, (-1+edgecount^0 >= 0 /\ 1+i^0-nodecount^0 <= 0), cost: 4+3*edgecount^0 60: l13 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 2 72: l13 -> l13 : i^0'=1+i^0, (1+i^0-nodecount^0 <= 0 /\ -source^0+i^0 == 0), cost: 4 73: l13 -> l13 : i^0'=1+i^0, (1+i^0-nodecount^0 <= 0 /\ 1+source^0-i^0 <= 0), cost: 5 74: l13 -> l13 : i^0'=1+i^0, (1+i^0-nodecount^0 <= 0 /\ 1-source^0+i^0 <= 0), cost: 5 48: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 Applied acceleration Original rule: l9 -> l9 : j^0'=0, i^0'=1+i^0, (1+i^0-nodecount^0 <= 0 /\ edgecount^0 <= 0), cost: 4 New rule: l9 -> l9 : j^0'=0, i^0'=n2+i^0, (-1+n2 >= 0 /\ -edgecount^0 >= 0 /\ -n2-i^0+nodecount^0 >= 0), cost: 4*n2 Sub-proof via acceration calculus written to file:///tmp/tmpnam_NpFfBI.txt Applied instantiation Original rule: l9 -> l9 : j^0'=0, i^0'=n2+i^0, (-1+n2 >= 0 /\ -edgecount^0 >= 0 /\ -n2-i^0+nodecount^0 >= 0), cost: 4*n2 New rule: l9 -> l9 : j^0'=0, i^0'=nodecount^0, (0 >= 0 /\ -edgecount^0 >= 0 /\ -1-i^0+nodecount^0 >= 0), cost: -4*i^0+4*nodecount^0 Applied acceleration Original rule: l9 -> l9 : j^0'=edgecount^0, i^0'=1+i^0, y^0'=y^post8, x^0'=x^post8, (-1+edgecount^0 >= 0 /\ 1+i^0-nodecount^0 <= 0), cost: 4+3*edgecount^0 New rule: l9 -> l9 : j^0'=edgecount^0, i^0'=i^0+n3, y^0'=y^post8, x^0'=x^post8, (-1+n3 >= 0 /\ -i^0+nodecount^0-n3 >= 0 /\ -1+edgecount^0 >= 0), cost: 3*edgecount^0*n3+4*n3 Sub-proof via acceration calculus written to file:///tmp/tmpnam_HpiPCg.txt Applied instantiation Original rule: l9 -> l9 : j^0'=edgecount^0, i^0'=i^0+n3, y^0'=y^post8, x^0'=x^post8, (-1+n3 >= 0 /\ -i^0+nodecount^0-n3 >= 0 /\ -1+edgecount^0 >= 0), cost: 3*edgecount^0*n3+4*n3 New rule: l9 -> l9 : j^0'=edgecount^0, i^0'=nodecount^0, y^0'=y^post8, x^0'=x^post8, (0 >= 0 /\ -1+edgecount^0 >= 0 /\ -1-i^0+nodecount^0 >= 0), cost: -3*(i^0-nodecount^0)*edgecount^0-4*i^0+4*nodecount^0 Applied simplification Original rule: l9 -> l9 : j^0'=0, i^0'=nodecount^0, (0 >= 0 /\ -edgecount^0 >= 0 /\ -1-i^0+nodecount^0 >= 0), cost: -4*i^0+4*nodecount^0 New rule: l9 -> l9 : j^0'=0, i^0'=nodecount^0, (edgecount^0 <= 0 /\ -1-i^0+nodecount^0 >= 0), cost: -4*i^0+4*nodecount^0 Applied simplification Original rule: l9 -> l9 : j^0'=edgecount^0, i^0'=nodecount^0, y^0'=y^post8, x^0'=x^post8, (0 >= 0 /\ -1+edgecount^0 >= 0 /\ -1-i^0+nodecount^0 >= 0), cost: -3*(i^0-nodecount^0)*edgecount^0-4*i^0+4*nodecount^0 New rule: l9 -> l9 : j^0'=edgecount^0, i^0'=nodecount^0, y^0'=y^post8, x^0'=x^post8, (-1+edgecount^0 >= 0 /\ -1-i^0+nodecount^0 >= 0), cost: -3*(i^0-nodecount^0)*edgecount^0-4*i^0+4*nodecount^0 Applied deletion Removed the following rules: 75 76 Applied acceleration Original rule: l13 -> l13 : i^0'=1+i^0, (1+i^0-nodecount^0 <= 0 /\ 1+source^0-i^0 <= 0), cost: 5 New rule: l13 -> l13 : i^0'=n5+i^0, (-1-source^0+i^0 >= 0 /\ n5 >= 0 /\ -n5-i^0+nodecount^0 >= 0), cost: 5*n5 Sub-proof via acceration calculus written to file:///tmp/tmpnam_fnPGJm.txt Applied instantiation Original rule: l13 -> l13 : i^0'=n5+i^0, (-1-source^0+i^0 >= 0 /\ n5 >= 0 /\ -n5-i^0+nodecount^0 >= 0), cost: 5*n5 New rule: l13 -> l13 : i^0'=nodecount^0, (0 >= 0 /\ -i^0+nodecount^0 >= 0 /\ -1-source^0+i^0 >= 0), cost: -5*i^0+5*nodecount^0 Applied acceleration Original rule: l13 -> l13 : i^0'=1+i^0, (1+i^0-nodecount^0 <= 0 /\ 1-source^0+i^0 <= 0), cost: 5 New rule: l13 -> l13 : i^0'=i^0+n6, (source^0-i^0-n6 >= 0 /\ n6 >= 0 /\ -i^0+nodecount^0-n6 >= 0), cost: 5*n6 Sub-proof via acceration calculus written to file:///tmp/tmpnam_hflHlL.txt Applied instantiation Original rule: l13 -> l13 : i^0'=i^0+n6, (source^0-i^0-n6 >= 0 /\ n6 >= 0 /\ -i^0+nodecount^0-n6 >= 0), cost: 5*n6 New rule: l13 -> l13 : i^0'=nodecount^0, (0 >= 0 /\ -i^0+nodecount^0 >= 0 /\ source^0-nodecount^0 >= 0), cost: -5*i^0+5*nodecount^0 Applied instantiation Original rule: l13 -> l13 : i^0'=i^0+n6, (source^0-i^0-n6 >= 0 /\ n6 >= 0 /\ -i^0+nodecount^0-n6 >= 0), cost: 5*n6 New rule: l13 -> l13 : i^0'=source^0, (0 >= 0 /\ -source^0+nodecount^0 >= 0 /\ source^0-i^0 >= 0), cost: 5*source^0-5*i^0 Applied simplification Original rule: l13 -> l13 : i^0'=nodecount^0, (0 >= 0 /\ -i^0+nodecount^0 >= 0 /\ -1-source^0+i^0 >= 0), cost: -5*i^0+5*nodecount^0 New rule: l13 -> l13 : i^0'=nodecount^0, (-i^0+nodecount^0 >= 0 /\ -1-source^0+i^0 >= 0), cost: -5*i^0+5*nodecount^0 Applied simplification Original rule: l13 -> l13 : i^0'=nodecount^0, (0 >= 0 /\ -i^0+nodecount^0 >= 0 /\ source^0-nodecount^0 >= 0), cost: -5*i^0+5*nodecount^0 New rule: l13 -> l13 : i^0'=nodecount^0, (-i^0+nodecount^0 >= 0 /\ source^0-nodecount^0 >= 0), cost: -5*i^0+5*nodecount^0 Applied simplification Original rule: l13 -> l13 : i^0'=source^0, (0 >= 0 /\ -source^0+nodecount^0 >= 0 /\ source^0-i^0 >= 0), cost: 5*source^0-5*i^0 New rule: l13 -> l13 : i^0'=source^0, (-source^0+nodecount^0 >= 0 /\ source^0-i^0 >= 0), cost: 5*source^0-5*i^0 Applied deletion Removed the following rules: 73 74 Accelerated simple loops Start location: l17 79: l9 -> l9 : j^0'=0, i^0'=nodecount^0, (edgecount^0 <= 0 /\ -1-i^0+nodecount^0 >= 0), cost: -4*i^0+4*nodecount^0 80: l9 -> l9 : j^0'=edgecount^0, i^0'=nodecount^0, y^0'=y^post8, x^0'=x^post8, (-1+edgecount^0 >= 0 /\ -1-i^0+nodecount^0 >= 0), cost: -3*(i^0-nodecount^0)*edgecount^0-4*i^0+4*nodecount^0 60: l13 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 2 72: l13 -> l13 : i^0'=1+i^0, (1+i^0-nodecount^0 <= 0 /\ -source^0+i^0 == 0), cost: 4 84: l13 -> l13 : i^0'=nodecount^0, (-i^0+nodecount^0 >= 0 /\ -1-source^0+i^0 >= 0), cost: -5*i^0+5*nodecount^0 85: l13 -> l13 : i^0'=nodecount^0, (-i^0+nodecount^0 >= 0 /\ source^0-nodecount^0 >= 0), cost: -5*i^0+5*nodecount^0 86: l13 -> l13 : i^0'=source^0, (-source^0+nodecount^0 >= 0 /\ source^0-i^0 >= 0), cost: 5*source^0-5*i^0 48: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 Applied chaining First rule: l13 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 2 Second rule: l9 -> l9 : j^0'=0, i^0'=nodecount^0, (edgecount^0 <= 0 /\ -1-i^0+nodecount^0 >= 0), cost: -4*i^0+4*nodecount^0 New rule: l13 -> l9 : j^0'=0, i^0'=nodecount^0, (-i^0+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0 /\ edgecount^0 <= 0), cost: 2+4*nodecount^0 Applied chaining First rule: l13 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 2 Second rule: l9 -> l9 : j^0'=edgecount^0, i^0'=nodecount^0, y^0'=y^post8, x^0'=x^post8, (-1+edgecount^0 >= 0 /\ -1-i^0+nodecount^0 >= 0), cost: -3*(i^0-nodecount^0)*edgecount^0-4*i^0+4*nodecount^0 New rule: l13 -> l9 : j^0'=edgecount^0, i^0'=nodecount^0, y^0'=y^post8, x^0'=x^post8, (-i^0+nodecount^0 <= 0 /\ -1+edgecount^0 >= 0 /\ -1+nodecount^0 >= 0), cost: 2+3*nodecount^0*edgecount^0+4*nodecount^0 Applied deletion Removed the following rules: 79 80 Applied chaining First rule: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 Second rule: l13 -> l13 : i^0'=1+i^0, (1+i^0-nodecount^0 <= 0 /\ -source^0+i^0 == 0), cost: 4 New rule: l17 -> l13 : source^0'=0, i^0'=1, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, -1+__const_5^0 >= 0, cost: 6 Applied chaining First rule: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 Second rule: l13 -> l13 : i^0'=nodecount^0, (-i^0+nodecount^0 >= 0 /\ source^0-nodecount^0 >= 0), cost: -5*i^0+5*nodecount^0 New rule: l17 -> l13 : source^0'=0, i^0'=__const_5^0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, __const_5^0 == 0, cost: 2+5*__const_5^0 Applied chaining First rule: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 Second rule: l13 -> l13 : i^0'=source^0, (-source^0+nodecount^0 >= 0 /\ source^0-i^0 >= 0), cost: 5*source^0-5*i^0 New rule: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, __const_5^0 >= 0, cost: 2 Applied deletion Removed the following rules: 72 84 85 86 Chained accelerated rules with incoming rules Start location: l17 60: l13 -> l9 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 2 87: l13 -> l9 : j^0'=0, i^0'=nodecount^0, (-i^0+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0 /\ edgecount^0 <= 0), cost: 2+4*nodecount^0 88: l13 -> l9 : j^0'=edgecount^0, i^0'=nodecount^0, y^0'=y^post8, x^0'=x^post8, (-i^0+nodecount^0 <= 0 /\ -1+edgecount^0 >= 0 /\ -1+nodecount^0 >= 0), cost: 2+3*nodecount^0*edgecount^0+4*nodecount^0 48: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, TRUE, cost: 2 89: l17 -> l13 : source^0'=0, i^0'=1, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, -1+__const_5^0 >= 0, cost: 6 90: l17 -> l13 : source^0'=0, i^0'=__const_5^0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, __const_5^0 == 0, cost: 2+5*__const_5^0 91: l17 -> l13 : source^0'=0, i^0'=0, nodecount^0'=__const_5^0, edgecount^0'=__const_16^0, __const_5^0 >= 0, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l17 Computing asymptotic complexity Proved the following lower bound Complexity: Unknown Cpx degree: ? Solved cost: 0 Rule cost: 0