NO

Initial ITS
Start location: l28
   0: l0 -> l1 : i^0'=i^post0, destflag^0'=destflag^post0, nodecount^0'=nodecount^post0, k^0'=k^post0, h^0'=h^post0, __lengthofvisited^0'=__lengthofvisited^post0, min^0'=min^post0, j^0'=j^post0, edgecount^0'=edgecount^post0, sourceflag^0'=sourceflag^post0, k_1^0'=k_1^post0, (-sourceflag^post0+sourceflag^0 == 0 /\ -k^post0+k^0 == 0 /\ destflag^0-destflag^post0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post0 == 0 /\ -min^post0+min^0 == 0 /\ -k_1^post0+k_1^0 == 0 /\ -j^post0+j^0 == 0 /\ -edgecount^post0+edgecount^0 == 0 /\ i^0-i^post0 == 0 /\ nodecount^0-nodecount^post0 == 0 /\ h^0-h^post0 == 0), cost: 1
  42: l1 -> l2 : i^0'=i^post42, destflag^0'=destflag^post42, nodecount^0'=nodecount^post42, k^0'=k^post42, h^0'=h^post42, __lengthofvisited^0'=__lengthofvisited^post42, min^0'=min^post42, j^0'=j^post42, edgecount^0'=edgecount^post42, sourceflag^0'=sourceflag^post42, k_1^0'=k_1^post42, (-__lengthofvisited^post42+__lengthofvisited^0 == 0 /\ -j^post42+j^0 == 0 /\ h^0-h^post42 == 0 /\ min^0-min^post42 == 0 /\ destflag^0-destflag^post42 == 0 /\ -k_1^post42+k_1^0 == 0 /\ -sourceflag^post42+sourceflag^0 == 0 /\ -i^0+nodecount^0 <= 0 /\ i^post42 == 0 /\ -nodecount^post42+nodecount^0 == 0 /\ -edgecount^post42+edgecount^0 == 0 /\ k^0-k^post42 == 0), cost: 1
  43: l1 -> l0 : i^0'=i^post43, destflag^0'=destflag^post43, nodecount^0'=nodecount^post43, k^0'=k^post43, h^0'=h^post43, __lengthofvisited^0'=__lengthofvisited^post43, min^0'=min^post43, j^0'=j^post43, edgecount^0'=edgecount^post43, sourceflag^0'=sourceflag^post43, k_1^0'=k_1^post43, (__lengthofvisited^0-__lengthofvisited^post43 == 0 /\ -min^post43+min^0 == 0 /\ -k^post43+k^0 == 0 /\ -k_1^post43+k_1^0 == 0 /\ -1-i^0+i^post43 == 0 /\ nodecount^0-nodecount^post43 == 0 /\ edgecount^0-edgecount^post43 == 0 /\ destflag^0-destflag^post43 == 0 /\ -j^post43+j^0 == 0 /\ h^0-h^post43 == 0 /\ -sourceflag^post43+sourceflag^0 == 0 /\ 1+i^0-nodecount^0 <= 0), cost: 1
   1: l2 -> l3 : i^0'=i^post1, destflag^0'=destflag^post1, nodecount^0'=nodecount^post1, k^0'=k^post1, h^0'=h^post1, __lengthofvisited^0'=__lengthofvisited^post1, min^0'=min^post1, j^0'=j^post1, edgecount^0'=edgecount^post1, sourceflag^0'=sourceflag^post1, k_1^0'=k_1^post1, (i^0-i^post1 == 0 /\ nodecount^0-nodecount^post1 == 0 /\ -h^post1+h^0 == 0 /\ -edgecount^post1+edgecount^0 == 0 /\ k^0-k^post1 == 0 /\ -min^post1+min^0 == 0 /\ -__lengthofvisited^post1+__lengthofvisited^0 == 0 /\ destflag^0-destflag^post1 == 0 /\ j^0-j^post1 == 0 /\ -sourceflag^post1+sourceflag^0 == 0 /\ -k_1^post1+k_1^0 == 0), cost: 1
  39: l3 -> l4 : i^0'=i^post39, destflag^0'=destflag^post39, nodecount^0'=nodecount^post39, k^0'=k^post39, h^0'=h^post39, __lengthofvisited^0'=__lengthofvisited^post39, min^0'=min^post39, j^0'=j^post39, edgecount^0'=edgecount^post39, sourceflag^0'=sourceflag^post39, k_1^0'=k_1^post39, (nodecount^0-nodecount^post39 == 0 /\ -edgecount^post39+edgecount^0 == 0 /\ -k_1^post39+k_1^0 == 0 /\ -1-i^0+nodecount^0 <= 0 /\ i^0-i^post39 == 0 /\ -h^post39+h^0 == 0 /\ -__lengthofvisited^post39+__lengthofvisited^0 == 0 /\ -sourceflag^post39+sourceflag^0 == 0 /\ j^0-j^post39 == 0 /\ k^post39 == 0 /\ -destflag^post39+destflag^0 == 0 /\ -min^post39+min^0 == 0), cost: 1
  40: l3 -> l2 : i^0'=i^post40, destflag^0'=destflag^post40, nodecount^0'=nodecount^post40, k^0'=k^post40, h^0'=h^post40, __lengthofvisited^0'=__lengthofvisited^post40, min^0'=min^post40, j^0'=j^post40, edgecount^0'=edgecount^post40, sourceflag^0'=sourceflag^post40, k_1^0'=k_1^post40, (-k^post40+k^0 == 0 /\ min^0-min^post40 == 0 /\ -edgecount^post40+edgecount^0 == 0 /\ sourceflag^0-sourceflag^post40 == 0 /\ h^0-h^post40 == 0 /\ -nodecount^post40+nodecount^0 == 0 /\ -j^post40+j^0 == 0 /\ -k_1^post40+k_1^0 == 0 /\ destflag^0-destflag^post40 == 0 /\ __lengthofvisited^0-__lengthofvisited^post40 == 0 /\ 2+i^0-nodecount^0 <= 0 /\ -1-i^0+i^post40 == 0), cost: 1
   2: l4 -> l5 : i^0'=i^post2, destflag^0'=destflag^post2, nodecount^0'=nodecount^post2, k^0'=k^post2, h^0'=h^post2, __lengthofvisited^0'=__lengthofvisited^post2, min^0'=min^post2, j^0'=j^post2, edgecount^0'=edgecount^post2, sourceflag^0'=sourceflag^post2, k_1^0'=k_1^post2, (h^0-h^post2 == 0 /\ -__lengthofvisited^post2+__lengthofvisited^0 == 0 /\ -nodecount^post2+nodecount^0 == 0 /\ min^0-min^post2 == 0 /\ -k_1^post2+k_1^0 == 0 /\ -j^post2+j^0 == 0 /\ -sourceflag^post2+sourceflag^0 == 0 /\ destflag^0-destflag^post2 == 0 /\ i^0-i^post2 == 0 /\ -edgecount^post2+edgecount^0 == 0 /\ k^0-k^post2 == 0), cost: 1
  36: l5 -> l26 : i^0'=i^post36, destflag^0'=destflag^post36, nodecount^0'=nodecount^post36, k^0'=k^post36, h^0'=h^post36, __lengthofvisited^0'=__lengthofvisited^post36, min^0'=min^post36, j^0'=j^post36, edgecount^0'=edgecount^post36, sourceflag^0'=sourceflag^post36, k_1^0'=k_1^post36, (k^0-k^post36 == 0 /\ -min^post36+min^0 == 0 /\ j^0-j^post36 == 0 /\ __lengthofvisited^0-__lengthofvisited^post36 == 0 /\ -sourceflag^post36+sourceflag^0 == 0 /\ -k_1^post36+k_1^0 == 0 /\ edgecount^0-edgecount^post36 == 0 /\ nodecount^0-nodecount^post36 == 0 /\ -1+nodecount^0-k^0 <= 0 /\ -h^post36+h^0 == 0 /\ destflag^0-destflag^post36 == 0 /\ i^0-i^post36 == 0 /\ 1-nodecount^0+k^0 <= 0), cost: 1
  37: l5 -> l25 : i^0'=i^post37, destflag^0'=destflag^post37, nodecount^0'=nodecount^post37, k^0'=k^post37, h^0'=h^post37, __lengthofvisited^0'=__lengthofvisited^post37, min^0'=min^post37, j^0'=j^post37, edgecount^0'=edgecount^post37, sourceflag^0'=sourceflag^post37, k_1^0'=k_1^post37, (-destflag^post37+destflag^0 == 0 /\ -edgecount^post37+edgecount^0 == 0 /\ min^0-min^post37 == 0 /\ -nodecount^post37+nodecount^0 == 0 /\ k^0-k^post37 == 0 /\ -__lengthofvisited^post37+__lengthofvisited^0 == 0 /\ nodecount^0-k^0 <= 0 /\ -j^post37+j^0 == 0 /\ i^0-i^post37 == 0 /\ -k_1^post37+k_1^0 == 0 /\ -sourceflag^post37+sourceflag^0 == 0 /\ h^0-h^post37 == 0), cost: 1
  38: l5 -> l25 : i^0'=i^post38, destflag^0'=destflag^post38, nodecount^0'=nodecount^post38, k^0'=k^post38, h^0'=h^post38, __lengthofvisited^0'=__lengthofvisited^post38, min^0'=min^post38, j^0'=j^post38, edgecount^0'=edgecount^post38, sourceflag^0'=sourceflag^post38, k_1^0'=k_1^post38, (__lengthofvisited^0-__lengthofvisited^post38 == 0 /\ edgecount^0-edgecount^post38 == 0 /\ -k^post38+k^0 == 0 /\ destflag^0-destflag^post38 == 0 /\ 2-nodecount^0+k^0 <= 0 /\ i^0-i^post38 == 0 /\ nodecount^0-nodecount^post38 == 0 /\ h^0-h^post38 == 0 /\ -j^post38+j^0 == 0 /\ -sourceflag^post38+sourceflag^0 == 0 /\ -k_1^post38+k_1^0 == 0 /\ -min^post38+min^0 == 0), cost: 1
   3: l6 -> l7 : i^0'=i^post3, destflag^0'=destflag^post3, nodecount^0'=nodecount^post3, k^0'=k^post3, h^0'=h^post3, __lengthofvisited^0'=__lengthofvisited^post3, min^0'=min^post3, j^0'=j^post3, edgecount^0'=edgecount^post3, sourceflag^0'=sourceflag^post3, k_1^0'=k_1^post3, (-1+k_1^post3-k_1^0 == 0 /\ -sourceflag^post3+sourceflag^0 == 0 /\ -h^post3+h^0 == 0 /\ -min^post3+min^0 == 0 /\ edgecount^0-edgecount^post3 == 0 /\ nodecount^0-nodecount^post3 == 0 /\ j^0-j^post3 == 0 /\ destflag^0-destflag^post3 == 0 /\ -__lengthofvisited^post3+__lengthofvisited^0 == 0 /\ i^0-i^post3 == 0 /\ k^0-k^post3 == 0), cost: 1
  18: l7 -> l18 : i^0'=i^post18, destflag^0'=destflag^post18, nodecount^0'=nodecount^post18, k^0'=k^post18, h^0'=h^post18, __lengthofvisited^0'=__lengthofvisited^post18, min^0'=min^post18, j^0'=j^post18, edgecount^0'=edgecount^post18, sourceflag^0'=sourceflag^post18, k_1^0'=k_1^post18, (edgecount^0-edgecount^post18 == 0 /\ -k_1^post18+k_1^0 == 0 /\ -k^post18+k^0 == 0 /\ destflag^0-destflag^post18 == 0 /\ __lengthofvisited^0-__lengthofvisited^post18 == 0 /\ nodecount^0-nodecount^post18 == 0 /\ -sourceflag^post18+sourceflag^0 == 0 /\ h^0-h^post18 == 0 /\ -j^post18+j^0 == 0 /\ i^0-i^post18 == 0 /\ -min^post18+min^0 == 0), cost: 1
   4: l8 -> l6 : i^0'=i^post4, destflag^0'=destflag^post4, nodecount^0'=nodecount^post4, k^0'=k^post4, h^0'=h^post4, __lengthofvisited^0'=__lengthofvisited^post4, min^0'=min^post4, j^0'=j^post4, edgecount^0'=edgecount^post4, sourceflag^0'=sourceflag^post4, k_1^0'=k_1^post4, (-sourceflag^post4+sourceflag^0 == 0 /\ -destflag^post4+destflag^0 == 0 /\ min^0-min^post4 == 0 /\ -k_1^post4+k_1^0 == 0 /\ 1-destflag^0 <= 0 /\ -edgecount^post4+edgecount^0 == 0 /\ i^0-i^post4 == 0 /\ k^0-k^post4 == 0 /\ nodecount^0-nodecount^post4 == 0 /\ h^0-h^post4 == 0 /\ j^0-j^post4 == 0 /\ -__lengthofvisited^post4+__lengthofvisited^0 == 0), cost: 1
   5: l8 -> l6 : i^0'=i^post5, destflag^0'=destflag^post5, nodecount^0'=nodecount^post5, k^0'=k^post5, h^0'=h^post5, __lengthofvisited^0'=__lengthofvisited^post5, min^0'=min^post5, j^0'=j^post5, edgecount^0'=edgecount^post5, sourceflag^0'=sourceflag^post5, k_1^0'=k_1^post5, (-j^post5+j^0 == 0 /\ -edgecount^post5+edgecount^0 == 0 /\ 1+destflag^0 <= 0 /\ -sourceflag^post5+sourceflag^0 == 0 /\ -k_1^post5+k_1^0 == 0 /\ -k^post5+k^0 == 0 /\ h^0-h^post5 == 0 /\ -min^post5+min^0 == 0 /\ i^0-i^post5 == 0 /\ destflag^0-destflag^post5 == 0 /\ __lengthofvisited^0-__lengthofvisited^post5 == 0 /\ nodecount^0-nodecount^post5 == 0), cost: 1
   6: l8 -> l6 : i^0'=i^post6, destflag^0'=destflag^post6, nodecount^0'=nodecount^post6, k^0'=k^post6, h^0'=h^post6, __lengthofvisited^0'=__lengthofvisited^post6, min^0'=min^post6, j^0'=j^post6, edgecount^0'=edgecount^post6, sourceflag^0'=sourceflag^post6, k_1^0'=k_1^post6, (-h^post6+h^0 == 0 /\ -__lengthofvisited^post6+__lengthofvisited^0 == 0 /\ destflag^0 <= 0 /\ i^0-i^post6 == 0 /\ k^0-k^post6 == 0 /\ -sourceflag^post6+sourceflag^0 == 0 /\ -k_1^post6+k_1^0 == 0 /\ -destflag^0 <= 0 /\ -min^post6+min^0 == 0 /\ destflag^0-destflag^post6 == 0 /\ j^0-j^post6 == 0 /\ -edgecount^post6+edgecount^0 == 0 /\ nodecount^0-nodecount^post6 == 0), cost: 1
   7: l9 -> l6 : i^0'=i^post7, destflag^0'=destflag^post7, nodecount^0'=nodecount^post7, k^0'=k^post7, h^0'=h^post7, __lengthofvisited^0'=__lengthofvisited^post7, min^0'=min^post7, j^0'=j^post7, edgecount^0'=edgecount^post7, sourceflag^0'=sourceflag^post7, k_1^0'=k_1^post7, (-edgecount^post7+edgecount^0 == 0 /\ -k^post7+k^0 == 0 /\ -k_1^post7+k_1^0 == 0 /\ 1-sourceflag^0 <= 0 /\ -__lengthofvisited^post7+__lengthofvisited^0 == 0 /\ min^0-min^post7 == 0 /\ h^0-h^post7 == 0 /\ destflag^0-destflag^post7 == 0 /\ i^0-i^post7 == 0 /\ nodecount^0-nodecount^post7 == 0 /\ -sourceflag^post7+sourceflag^0 == 0 /\ -j^post7+j^0 == 0), cost: 1
   8: l9 -> l6 : i^0'=i^post8, destflag^0'=destflag^post8, nodecount^0'=nodecount^post8, k^0'=k^post8, h^0'=h^post8, __lengthofvisited^0'=__lengthofvisited^post8, min^0'=min^post8, j^0'=j^post8, edgecount^0'=edgecount^post8, sourceflag^0'=sourceflag^post8, k_1^0'=k_1^post8, (edgecount^0-edgecount^post8 == 0 /\ -sourceflag^post8+sourceflag^0 == 0 /\ destflag^0-destflag^post8 == 0 /\ __lengthofvisited^0-__lengthofvisited^post8 == 0 /\ -min^post8+min^0 == 0 /\ -j^post8+j^0 == 0 /\ nodecount^0-nodecount^post8 == 0 /\ 1+sourceflag^0 <= 0 /\ h^0-h^post8 == 0 /\ -k_1^post8+k_1^0 == 0 /\ i^0-i^post8 == 0 /\ -k^post8+k^0 == 0), cost: 1
   9: l9 -> l8 : i^0'=i^post9, destflag^0'=destflag^post9, nodecount^0'=nodecount^post9, k^0'=k^post9, h^0'=h^post9, __lengthofvisited^0'=__lengthofvisited^post9, min^0'=min^post9, j^0'=j^post9, edgecount^0'=edgecount^post9, sourceflag^0'=sourceflag^post9, k_1^0'=k_1^post9, (-sourceflag^post9+sourceflag^0 == 0 /\ -h^post9+h^0 == 0 /\ -sourceflag^0 <= 0 /\ k^0-k^post9 == 0 /\ -k_1^post9+k_1^0 == 0 /\ -destflag^post9+destflag^0 == 0 /\ min^0-min^post9 == 0 /\ i^0-i^post9 == 0 /\ -edgecount^post9+edgecount^0 == 0 /\ nodecount^0-nodecount^post9 == 0 /\ sourceflag^0 <= 0 /\ j^0-j^post9 == 0 /\ -__lengthofvisited^post9+__lengthofvisited^0 == 0), cost: 1
  10: l10 -> l11 : i^0'=i^post10, destflag^0'=destflag^post10, nodecount^0'=nodecount^post10, k^0'=k^post10, h^0'=h^post10, __lengthofvisited^0'=__lengthofvisited^post10, min^0'=min^post10, j^0'=j^post10, edgecount^0'=edgecount^post10, sourceflag^0'=sourceflag^post10, k_1^0'=k_1^post10, (i^0-i^post10 == 0 /\ min^0-min^post10 == 0 /\ sourceflag^0-sourceflag^post10 == 0 /\ -nodecount^post10+nodecount^0 == 0 /\ -edgecount^post10+edgecount^0 == 0 /\ h^0-h^post10 == 0 /\ -j^post10+j^0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post10 == 0 /\ -k^post10+k^0 == 0 /\ destflag^0-destflag^post10 == 0 /\ -k_1^post10+k_1^0 == 0), cost: 1
  32: l11 -> l7 : i^0'=i^post32, destflag^0'=destflag^post32, nodecount^0'=nodecount^post32, k^0'=k^post32, h^0'=h^post32, __lengthofvisited^0'=__lengthofvisited^post32, min^0'=min^post32, j^0'=j^post32, edgecount^0'=edgecount^post32, sourceflag^0'=sourceflag^post32, k_1^0'=k_1^post32, (k_1^post32 == 0 /\ -j^post32+j^0 == 0 /\ -__lengthofvisited^post32+__lengthofvisited^0 == 0 /\ h^0-h^post32 == 0 /\ min^0-min^post32 == 0 /\ destflag^0-destflag^post32 == 0 /\ -sourceflag^post32+sourceflag^0 == 0 /\ -i^0+edgecount^0 <= 0 /\ -nodecount^post32+nodecount^0 == 0 /\ i^0-i^post32 == 0 /\ -edgecount^post32+edgecount^0 == 0 /\ k^0-k^post32 == 0), cost: 1
  33: l11 -> l10 : i^0'=i^post33, destflag^0'=destflag^post33, nodecount^0'=nodecount^post33, k^0'=k^post33, h^0'=h^post33, __lengthofvisited^0'=__lengthofvisited^post33, min^0'=min^post33, j^0'=j^post33, edgecount^0'=edgecount^post33, sourceflag^0'=sourceflag^post33, k_1^0'=k_1^post33, (1+i^0-edgecount^0 <= 0 /\ __lengthofvisited^0-__lengthofvisited^post33 == 0 /\ -sourceflag^post33+sourceflag^0 == 0 /\ -1+i^post33-i^0 == 0 /\ -k^post33+k^0 == 0 /\ destflag^0-destflag^post33 == 0 /\ -edgecount^post33+edgecount^0 == 0 /\ -k_1^post33+k_1^0 == 0 /\ h^0-h^post33 == 0 /\ -j^post33+j^0 == 0 /\ nodecount^0-nodecount^post33 == 0 /\ -min^post33+min^0 == 0), cost: 1
  11: l12 -> l13 : i^0'=i^post11, destflag^0'=destflag^post11, nodecount^0'=nodecount^post11, k^0'=k^post11, h^0'=h^post11, __lengthofvisited^0'=__lengthofvisited^post11, min^0'=min^post11, j^0'=j^post11, edgecount^0'=edgecount^post11, sourceflag^0'=sourceflag^post11, k_1^0'=k_1^post11, (i^0-i^post11 == 0 /\ -h^post11+h^0 == 0 /\ nodecount^0-nodecount^post11 == 0 /\ -edgecount^post11+edgecount^0 == 0 /\ destflag^0-destflag^post11 == 0 /\ __lengthofvisited^0-__lengthofvisited^post11 == 0 /\ -sourceflag^post11+sourceflag^0 == 0 /\ -min^post11+min^0 == 0 /\ -1-j^0+j^post11 == 0 /\ -k_1^post11+k_1^0 == 0 /\ k^0-k^post11 == 0), cost: 1
  41: l13 -> l15 : i^0'=i^post41, destflag^0'=destflag^post41, nodecount^0'=nodecount^post41, k^0'=k^post41, h^0'=h^post41, __lengthofvisited^0'=__lengthofvisited^post41, min^0'=min^post41, j^0'=j^post41, edgecount^0'=edgecount^post41, sourceflag^0'=sourceflag^post41, k_1^0'=k_1^post41, (k^0-k^post41 == 0 /\ -min^post41+min^0 == 0 /\ i^0-i^post41 == 0 /\ nodecount^0-nodecount^post41 == 0 /\ edgecount^0-edgecount^post41 == 0 /\ -h^post41+h^0 == 0 /\ -__lengthofvisited^post41+__lengthofvisited^0 == 0 /\ j^0-j^post41 == 0 /\ destflag^0-destflag^post41 == 0 /\ -sourceflag^post41+sourceflag^0 == 0 /\ -k_1^post41+k_1^0 == 0), cost: 1
  12: l14 -> l12 : i^0'=i^post12, destflag^0'=destflag^post12, nodecount^0'=nodecount^post12, k^0'=k^post12, h^0'=h^post12, __lengthofvisited^0'=__lengthofvisited^post12, min^0'=min^post12, j^0'=j^post12, edgecount^0'=edgecount^post12, sourceflag^0'=sourceflag^post12, k_1^0'=k_1^post12, (h^0-h^post12 == 0 /\ -__lengthofvisited^post12+__lengthofvisited^0 == 0 /\ min^0-min^post12 == 0 /\ -j^post12+j^0 == 0 /\ -sourceflag^post12+sourceflag^0 == 0 /\ -k_1^post12+k_1^0 == 0 /\ -nodecount^post12+nodecount^0 == 0 /\ destflag^0-destflag^post12 == 0 /\ i^0-i^post12 == 0 /\ k^0-k^post12 == 0 /\ -edgecount^post12+edgecount^0 == 0), cost: 1
  13: l14 -> l12 : i^0'=i^post13, destflag^0'=destflag^post13, nodecount^0'=nodecount^post13, k^0'=k^post13, h^0'=h^post13, __lengthofvisited^0'=__lengthofvisited^post13, min^0'=min^post13, j^0'=j^post13, edgecount^0'=edgecount^post13, sourceflag^0'=sourceflag^post13, k_1^0'=k_1^post13, (__lengthofvisited^0-__lengthofvisited^post13 == 0 /\ -sourceflag^post13+sourceflag^0 == 0 /\ -min^post13+min^0 == 0 /\ -k^post13+k^0 == 0 /\ -j^post13+j^0 == 0 /\ -edgecount^post13+edgecount^0 == 0 /\ destflag^post13 == 0 /\ h^0-h^post13 == 0 /\ -k_1^post13+k_1^0 == 0 /\ -i^post13+i^0 == 0 /\ nodecount^0-nodecount^post13 == 0), cost: 1
  14: l14 -> l12 : i^0'=i^post14, destflag^0'=destflag^post14, nodecount^0'=nodecount^post14, k^0'=k^post14, h^0'=h^post14, __lengthofvisited^0'=__lengthofvisited^post14, min^0'=min^post14, j^0'=j^post14, edgecount^0'=edgecount^post14, sourceflag^0'=sourceflag^post14, k_1^0'=k_1^post14, (-h^post14+h^0 == 0 /\ -sourceflag^post14+sourceflag^0 == 0 /\ k^0-k^post14 == 0 /\ -__lengthofvisited^post14+__lengthofvisited^0 == 0 /\ -k_1^post14+k_1^0 == 0 /\ j^0-j^post14 == 0 /\ i^0-i^post14 == 0 /\ -edgecount^post14+edgecount^0 == 0 /\ -min^post14+min^0 == 0 /\ nodecount^0-nodecount^post14 == 0 /\ destflag^0-destflag^post14 == 0), cost: 1
  15: l15 -> l9 : i^0'=i^post15, destflag^0'=destflag^post15, nodecount^0'=nodecount^post15, k^0'=k^post15, h^0'=h^post15, __lengthofvisited^0'=__lengthofvisited^post15, min^0'=min^post15, j^0'=j^post15, edgecount^0'=edgecount^post15, sourceflag^0'=sourceflag^post15, k_1^0'=k_1^post15, (-j^post15+j^0 == 0 /\ -k_1^post15+k_1^0 == 0 /\ nodecount^0-nodecount^post15 == 0 /\ nodecount^0-j^0 <= 0 /\ -edgecount^post15+edgecount^0 == 0 /\ -sourceflag^post15+sourceflag^0 == 0 /\ i^0-i^post15 == 0 /\ -k^post15+k^0 == 0 /\ h^0-h^post15 == 0 /\ -min^post15+min^0 == 0 /\ destflag^0-destflag^post15 == 0 /\ __lengthofvisited^0-__lengthofvisited^post15 == 0), cost: 1
  16: l15 -> l14 : i^0'=i^post16, destflag^0'=destflag^post16, nodecount^0'=nodecount^post16, k^0'=k^post16, h^0'=h^post16, __lengthofvisited^0'=__lengthofvisited^post16, min^0'=min^post16, j^0'=j^post16, edgecount^0'=edgecount^post16, sourceflag^0'=sourceflag^post16, k_1^0'=k_1^post16, (-h^post16+h^0 == 0 /\ j^0-j^post16 == 0 /\ destflag^0-destflag^post16 == 0 /\ __lengthofvisited^0-__lengthofvisited^post16 == 0 /\ -sourceflag^post16+sourceflag^0 == 0 /\ -k_1^post16+k_1^0 == 0 /\ nodecount^0-nodecount^post16 == 0 /\ 1-nodecount^0+j^0 <= 0 /\ edgecount^0-edgecount^post16 == 0 /\ -min^post16+min^0 == 0 /\ i^0-i^post16 == 0 /\ k^0-k^post16 == 0), cost: 1
  17: l16 -> l17 : i^0'=i^post17, destflag^0'=destflag^post17, nodecount^0'=nodecount^post17, k^0'=k^post17, h^0'=h^post17, __lengthofvisited^0'=__lengthofvisited^post17, min^0'=min^post17, j^0'=j^post17, edgecount^0'=edgecount^post17, sourceflag^0'=sourceflag^post17, k_1^0'=k_1^post17, (-destflag^post17+destflag^0 == 0 /\ -__lengthofvisited^post17+__lengthofvisited^0 == 0 /\ -sourceflag^post17+sourceflag^0 == 0 /\ -k_1^post17+k_1^0 == 0 /\ -1+j^post17-j^0 == 0 /\ min^0-min^post17 == 0 /\ -nodecount^post17+nodecount^0 == 0 /\ k^0-k^post17 == 0 /\ h^0-h^post17 == 0 /\ i^0-i^post17 == 0 /\ -edgecount^post17+edgecount^0 == 0), cost: 1
  34: l17 -> l20 : i^0'=i^post34, destflag^0'=destflag^post34, nodecount^0'=nodecount^post34, k^0'=k^post34, h^0'=h^post34, __lengthofvisited^0'=__lengthofvisited^post34, min^0'=min^post34, j^0'=j^post34, edgecount^0'=edgecount^post34, sourceflag^0'=sourceflag^post34, k_1^0'=k_1^post34, (-edgecount^post34+edgecount^0 == 0 /\ -k_1^post34+k_1^0 == 0 /\ k^0-k^post34 == 0 /\ i^0-i^post34 == 0 /\ -__lengthofvisited^post34+__lengthofvisited^0 == 0 /\ -sourceflag^post34+sourceflag^0 == 0 /\ j^0-j^post34 == 0 /\ -min^post34+min^0 == 0 /\ nodecount^0-nodecount^post34 == 0 /\ -h^post34+h^0 == 0 /\ destflag^0-destflag^post34 == 0), cost: 1
  30: l18 -> l4 : i^0'=i^post30, destflag^0'=destflag^post30, nodecount^0'=nodecount^post30, k^0'=k^post30, h^0'=h^post30, __lengthofvisited^0'=__lengthofvisited^post30, min^0'=min^post30, j^0'=j^post30, edgecount^0'=edgecount^post30, sourceflag^0'=sourceflag^post30, k_1^0'=k_1^post30, (sourceflag^0-sourceflag^post30 == 0 /\ destflag^0-destflag^post30 == 0 /\ __lengthofvisited^0-__lengthofvisited^post30 == 0 /\ i^0-i^post30 == 0 /\ -min^post30+min^0 == 0 /\ edgecount^0-k_1^0 <= 0 /\ -j^post30+j^0 == 0 /\ -1+k^post30-k^0 == 0 /\ -k_1^post30+k_1^0 == 0 /\ h^0-h^post30 == 0 /\ -edgecount^post30+edgecount^0 == 0 /\ -nodecount^post30+nodecount^0 == 0), cost: 1
  31: l18 -> l22 : i^0'=i^post31, destflag^0'=destflag^post31, nodecount^0'=nodecount^post31, k^0'=k^post31, h^0'=h^post31, __lengthofvisited^0'=__lengthofvisited^post31, min^0'=min^post31, j^0'=j^post31, edgecount^0'=edgecount^post31, sourceflag^0'=sourceflag^post31, k_1^0'=k_1^post31, (1-edgecount^0+k_1^0 <= 0 /\ h^post31 == 0 /\ destflag^0-destflag^post31 == 0 /\ j^0-j^post31 == 0 /\ __lengthofvisited^0-__lengthofvisited^post31 == 0 /\ edgecount^0-edgecount^post31 == 0 /\ -sourceflag^post31+sourceflag^0 == 0 /\ nodecount^0-nodecount^post31 == 0 /\ -k_1^post31+k_1^0 == 0 /\ -min^post31+min^0 == 0 /\ i^0-i^post31 == 0 /\ k^0-k^post31 == 0), cost: 1
  19: l19 -> l16 : i^0'=i^post19, destflag^0'=destflag^post19, nodecount^0'=nodecount^post19, k^0'=k^post19, h^0'=h^post19, __lengthofvisited^0'=__lengthofvisited^post19, min^0'=min^post19, j^0'=j^post19, edgecount^0'=edgecount^post19, sourceflag^0'=sourceflag^post19, k_1^0'=k_1^post19, (-sourceflag^post19+sourceflag^0 == 0 /\ -h^post19+h^0 == 0 /\ k^0-k^post19 == 0 /\ -edgecount^post19+edgecount^0 == 0 /\ min^0-min^post19 == 0 /\ -k_1^post19+k_1^0 == 0 /\ -destflag^post19+destflag^0 == 0 /\ i^0-i^post19 == 0 /\ nodecount^0-nodecount^post19 == 0 /\ j^0-j^post19 == 0 /\ -__lengthofvisited^post19+__lengthofvisited^0 == 0), cost: 1
  20: l19 -> l16 : i^0'=i^post20, destflag^0'=destflag^post20, nodecount^0'=nodecount^post20, k^0'=k^post20, h^0'=h^post20, __lengthofvisited^0'=__lengthofvisited^post20, min^0'=min^post20, j^0'=j^post20, edgecount^0'=edgecount^post20, sourceflag^0'=sourceflag^post20, k_1^0'=k_1^post20, (__lengthofvisited^0-__lengthofvisited^post20 == 0 /\ -j^post20+j^0 == 0 /\ -k^post20+k^0 == 0 /\ -k_1^post20+k_1^0 == 0 /\ h^0-h^post20 == 0 /\ i^0-i^post20 == 0 /\ -edgecount^post20+edgecount^0 == 0 /\ -min^post20+min^0 == 0 /\ nodecount^0-nodecount^post20 == 0 /\ -1+sourceflag^post20 == 0 /\ destflag^0-destflag^post20 == 0), cost: 1
  21: l19 -> l16 : i^0'=i^post21, destflag^0'=destflag^post21, nodecount^0'=nodecount^post21, k^0'=k^post21, h^0'=h^post21, __lengthofvisited^0'=__lengthofvisited^post21, min^0'=min^post21, j^0'=j^post21, edgecount^0'=edgecount^post21, sourceflag^0'=sourceflag^post21, k_1^0'=k_1^post21, (-h^post21+h^0 == 0 /\ i^0-i^post21 == 0 /\ -__lengthofvisited^post21+__lengthofvisited^0 == 0 /\ nodecount^0-nodecount^post21 == 0 /\ -edgecount^post21+edgecount^0 == 0 /\ k^0-k^post21 == 0 /\ -sourceflag^post21+sourceflag^0 == 0 /\ -k_1^post21+k_1^0 == 0 /\ -min^post21+min^0 == 0 /\ j^0-j^post21 == 0 /\ destflag^0-destflag^post21 == 0), cost: 1
  22: l20 -> l13 : i^0'=i^post22, destflag^0'=destflag^post22, nodecount^0'=nodecount^post22, k^0'=k^post22, h^0'=h^post22, __lengthofvisited^0'=__lengthofvisited^post22, min^0'=min^post22, j^0'=j^post22, edgecount^0'=edgecount^post22, sourceflag^0'=sourceflag^post22, k_1^0'=k_1^post22, (nodecount^0-j^0 <= 0 /\ j^post22 == 0 /\ -__lengthofvisited^post22+__lengthofvisited^0 == 0 /\ h^0-h^post22 == 0 /\ min^0-min^post22 == 0 /\ -sourceflag^post22+sourceflag^0 == 0 /\ -k_1^post22+k_1^0 == 0 /\ -1+destflag^post22 == 0 /\ -nodecount^post22+nodecount^0 == 0 /\ i^0-i^post22 == 0 /\ k^0-k^post22 == 0 /\ -edgecount^post22+edgecount^0 == 0), cost: 1
  23: l20 -> l19 : i^0'=i^post23, destflag^0'=destflag^post23, nodecount^0'=nodecount^post23, k^0'=k^post23, h^0'=h^post23, __lengthofvisited^0'=__lengthofvisited^post23, min^0'=min^post23, j^0'=j^post23, edgecount^0'=edgecount^post23, sourceflag^0'=sourceflag^post23, k_1^0'=k_1^post23, (-sourceflag^post23+sourceflag^0 == 0 /\ j^0-j^post23 == 0 /\ __lengthofvisited^0-__lengthofvisited^post23 == 0 /\ -k_1^post23+k_1^0 == 0 /\ -k^post23+k^0 == 0 /\ 1-nodecount^0+j^0 <= 0 /\ nodecount^0-nodecount^post23 == 0 /\ destflag^0-destflag^post23 == 0 /\ edgecount^0-edgecount^post23 == 0 /\ -min^post23+min^0 == 0 /\ h^0-h^post23 == 0 /\ i^0-i^post23 == 0), cost: 1
  24: l21 -> l22 : i^0'=i^post24, destflag^0'=destflag^post24, nodecount^0'=nodecount^post24, k^0'=k^post24, h^0'=h^post24, __lengthofvisited^0'=__lengthofvisited^post24, min^0'=min^post24, j^0'=j^post24, edgecount^0'=edgecount^post24, sourceflag^0'=sourceflag^post24, k_1^0'=k_1^post24, (-k_1^post24+k_1^0 == 0 /\ -destflag^post24+destflag^0 == 0 /\ -__lengthofvisited^post24+__lengthofvisited^0 == 0 /\ -1-h^0+h^post24 == 0 /\ min^0-min^post24 == 0 /\ -edgecount^post24+edgecount^0 == 0 /\ i^0-i^post24 == 0 /\ k^0-k^post24 == 0 /\ -sourceflag^post24+sourceflag^0 == 0 /\ nodecount^0-nodecount^post24 == 0 /\ -j^post24+j^0 == 0), cost: 1
  27: l22 -> l24 : i^0'=i^post27, destflag^0'=destflag^post27, nodecount^0'=nodecount^post27, k^0'=k^post27, h^0'=h^post27, __lengthofvisited^0'=__lengthofvisited^post27, min^0'=min^post27, j^0'=j^post27, edgecount^0'=edgecount^post27, sourceflag^0'=sourceflag^post27, k_1^0'=k_1^post27, (min^0-min^post27 == 0 /\ -k^post27+k^0 == 0 /\ sourceflag^0-sourceflag^post27 == 0 /\ -k_1^post27+k_1^0 == 0 /\ h^0-h^post27 == 0 /\ destflag^0-destflag^post27 == 0 /\ __lengthofvisited^0-__lengthofvisited^post27 == 0 /\ -j^post27+j^0 == 0 /\ -nodecount^post27+nodecount^0 == 0 /\ i^0-i^post27 == 0 /\ -edgecount^post27+edgecount^0 == 0), cost: 1
  25: l23 -> l21 : i^0'=i^post25, destflag^0'=destflag^post25, nodecount^0'=nodecount^post25, k^0'=k^post25, h^0'=h^post25, __lengthofvisited^0'=__lengthofvisited^post25, min^0'=min^post25, j^0'=j^post25, edgecount^0'=edgecount^post25, sourceflag^0'=sourceflag^post25, k_1^0'=k_1^post25, (-k_1^post25+k_1^0 == 0 /\ min^post25-h^0 == 0 /\ sourceflag^0-sourceflag^post25 == 0 /\ -edgecount^post25+edgecount^0 == 0 /\ -nodecount^post25+nodecount^0 == 0 /\ i^0-i^post25 == 0 /\ -k^post25+k^0 == 0 /\ h^0-h^post25 == 0 /\ destflag^0-destflag^post25 == 0 /\ __lengthofvisited^0-__lengthofvisited^post25 == 0 /\ -j^post25+j^0 == 0), cost: 1
  26: l23 -> l21 : i^0'=i^post26, destflag^0'=destflag^post26, nodecount^0'=nodecount^post26, k^0'=k^post26, h^0'=h^post26, __lengthofvisited^0'=__lengthofvisited^post26, min^0'=min^post26, j^0'=j^post26, edgecount^0'=edgecount^post26, sourceflag^0'=sourceflag^post26, k_1^0'=k_1^post26, (-k_1^post26+k_1^0 == 0 /\ nodecount^0-nodecount^post26 == 0 /\ k^0-k^post26 == 0 /\ -__lengthofvisited^post26+__lengthofvisited^0 == 0 /\ -h^post26+h^0 == 0 /\ -edgecount^post26+edgecount^0 == 0 /\ -sourceflag^post26+sourceflag^0 == 0 /\ i^0-i^post26 == 0 /\ destflag^0-destflag^post26 == 0 /\ -min^post26+min^0 == 0 /\ j^0-j^post26 == 0), cost: 1
  28: l24 -> l17 : i^0'=i^post28, destflag^0'=destflag^post28, nodecount^0'=nodecount^post28, k^0'=k^post28, h^0'=h^post28, __lengthofvisited^0'=__lengthofvisited^post28, min^0'=min^post28, j^0'=j^post28, edgecount^0'=edgecount^post28, sourceflag^0'=sourceflag^post28, k_1^0'=k_1^post28, (sourceflag^post28 == 0 /\ edgecount^0-edgecount^post28 == 0 /\ -k^post28+k^0 == 0 /\ destflag^0-destflag^post28 == 0 /\ __lengthofvisited^0-__lengthofvisited^post28 == 0 /\ j^post28 == 0 /\ i^0-i^post28 == 0 /\ nodecount^0-nodecount^post28 == 0 /\ h^0-h^post28 == 0 /\ -k_1^post28+k_1^0 == 0 /\ -min^post28+min^0 == 0 /\ -h^0+edgecount^0 <= 0), cost: 1
  29: l24 -> l23 : i^0'=i^post29, destflag^0'=destflag^post29, nodecount^0'=nodecount^post29, k^0'=k^post29, h^0'=h^post29, __lengthofvisited^0'=__lengthofvisited^post29, min^0'=min^post29, j^0'=j^post29, edgecount^0'=edgecount^post29, sourceflag^0'=sourceflag^post29, k_1^0'=k_1^post29, (-destflag^post29+destflag^0 == 0 /\ -edgecount^post29+edgecount^0 == 0 /\ -k_1^post29+k_1^0 == 0 /\ -__lengthofvisited^post29+__lengthofvisited^0 == 0 /\ k^0-k^post29 == 0 /\ min^0-min^post29 == 0 /\ i^0-i^post29 == 0 /\ 1+h^0-edgecount^0 <= 0 /\ nodecount^0-nodecount^post29 == 0 /\ -sourceflag^post29+sourceflag^0 == 0 /\ h^0-h^post29 == 0 /\ -j^post29+j^0 == 0), cost: 1
  35: l25 -> l10 : i^0'=i^post35, destflag^0'=destflag^post35, nodecount^0'=nodecount^post35, k^0'=k^post35, h^0'=h^post35, __lengthofvisited^0'=__lengthofvisited^post35, min^0'=min^post35, j^0'=j^post35, edgecount^0'=edgecount^post35, sourceflag^0'=sourceflag^post35, k_1^0'=k_1^post35, (min^post35 == 0 /\ -k_1^post35+k_1^0 == 0 /\ sourceflag^0-sourceflag^post35 == 0 /\ -edgecount^post35+edgecount^0 == 0 /\ -nodecount^post35+nodecount^0 == 0 /\ h^0-h^post35 == 0 /\ -k^post35+k^0 == 0 /\ destflag^0-destflag^post35 == 0 /\ __lengthofvisited^0-__lengthofvisited^post35 == 0 /\ i^post35 == 0 /\ -j^post35+j^0 == 0), cost: 1
  44: l27 -> l0 : i^0'=i^post44, destflag^0'=destflag^post44, nodecount^0'=nodecount^post44, k^0'=k^post44, h^0'=h^post44, __lengthofvisited^0'=__lengthofvisited^post44, min^0'=min^post44, j^0'=j^post44, edgecount^0'=edgecount^post44, sourceflag^0'=sourceflag^post44, k_1^0'=k_1^post44, (-destflag^post44+destflag^0 == 0 /\ -edgecount^post44+edgecount^0 == 0 /\ min^0-min^post44 == 0 /\ __lengthofvisited^post44-edgecount^0 == 0 /\ k^0-k^post44 == 0 /\ nodecount^0-nodecount^post44 == 0 /\ -k_1^post44+k_1^0 == 0 /\ h^0-h^post44 == 0 /\ -1+i^post44 == 0 /\ -sourceflag^post44+sourceflag^0 == 0 /\ -j^post44+j^0 == 0), cost: 1
  45: l28 -> l27 : i^0'=i^post45, destflag^0'=destflag^post45, nodecount^0'=nodecount^post45, k^0'=k^post45, h^0'=h^post45, __lengthofvisited^0'=__lengthofvisited^post45, min^0'=min^post45, j^0'=j^post45, edgecount^0'=edgecount^post45, sourceflag^0'=sourceflag^post45, k_1^0'=k_1^post45, (-edgecount^post45+edgecount^0 == 0 /\ sourceflag^0-sourceflag^post45 == 0 /\ -k_1^post45+k_1^0 == 0 /\ h^0-h^post45 == 0 /\ -nodecount^post45+nodecount^0 == 0 /\ i^0-i^post45 == 0 /\ -min^post45+min^0 == 0 /\ -j^post45+j^0 == 0 /\ -k^post45+k^0 == 0 /\ destflag^0-destflag^post45 == 0 /\ __lengthofvisited^0-__lengthofvisited^post45 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l28
   0: l0 -> l1 : i^0'=i^post0, destflag^0'=destflag^post0, nodecount^0'=nodecount^post0, k^0'=k^post0, h^0'=h^post0, __lengthofvisited^0'=__lengthofvisited^post0, min^0'=min^post0, j^0'=j^post0, edgecount^0'=edgecount^post0, sourceflag^0'=sourceflag^post0, k_1^0'=k_1^post0, (-sourceflag^post0+sourceflag^0 == 0 /\ -k^post0+k^0 == 0 /\ destflag^0-destflag^post0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post0 == 0 /\ -min^post0+min^0 == 0 /\ -k_1^post0+k_1^0 == 0 /\ -j^post0+j^0 == 0 /\ -edgecount^post0+edgecount^0 == 0 /\ i^0-i^post0 == 0 /\ nodecount^0-nodecount^post0 == 0 /\ h^0-h^post0 == 0), cost: 1
  42: l1 -> l2 : i^0'=i^post42, destflag^0'=destflag^post42, nodecount^0'=nodecount^post42, k^0'=k^post42, h^0'=h^post42, __lengthofvisited^0'=__lengthofvisited^post42, min^0'=min^post42, j^0'=j^post42, edgecount^0'=edgecount^post42, sourceflag^0'=sourceflag^post42, k_1^0'=k_1^post42, (-__lengthofvisited^post42+__lengthofvisited^0 == 0 /\ -j^post42+j^0 == 0 /\ h^0-h^post42 == 0 /\ min^0-min^post42 == 0 /\ destflag^0-destflag^post42 == 0 /\ -k_1^post42+k_1^0 == 0 /\ -sourceflag^post42+sourceflag^0 == 0 /\ -i^0+nodecount^0 <= 0 /\ i^post42 == 0 /\ -nodecount^post42+nodecount^0 == 0 /\ -edgecount^post42+edgecount^0 == 0 /\ k^0-k^post42 == 0), cost: 1
  43: l1 -> l0 : i^0'=i^post43, destflag^0'=destflag^post43, nodecount^0'=nodecount^post43, k^0'=k^post43, h^0'=h^post43, __lengthofvisited^0'=__lengthofvisited^post43, min^0'=min^post43, j^0'=j^post43, edgecount^0'=edgecount^post43, sourceflag^0'=sourceflag^post43, k_1^0'=k_1^post43, (__lengthofvisited^0-__lengthofvisited^post43 == 0 /\ -min^post43+min^0 == 0 /\ -k^post43+k^0 == 0 /\ -k_1^post43+k_1^0 == 0 /\ -1-i^0+i^post43 == 0 /\ nodecount^0-nodecount^post43 == 0 /\ edgecount^0-edgecount^post43 == 0 /\ destflag^0-destflag^post43 == 0 /\ -j^post43+j^0 == 0 /\ h^0-h^post43 == 0 /\ -sourceflag^post43+sourceflag^0 == 0 /\ 1+i^0-nodecount^0 <= 0), cost: 1
   1: l2 -> l3 : i^0'=i^post1, destflag^0'=destflag^post1, nodecount^0'=nodecount^post1, k^0'=k^post1, h^0'=h^post1, __lengthofvisited^0'=__lengthofvisited^post1, min^0'=min^post1, j^0'=j^post1, edgecount^0'=edgecount^post1, sourceflag^0'=sourceflag^post1, k_1^0'=k_1^post1, (i^0-i^post1 == 0 /\ nodecount^0-nodecount^post1 == 0 /\ -h^post1+h^0 == 0 /\ -edgecount^post1+edgecount^0 == 0 /\ k^0-k^post1 == 0 /\ -min^post1+min^0 == 0 /\ -__lengthofvisited^post1+__lengthofvisited^0 == 0 /\ destflag^0-destflag^post1 == 0 /\ j^0-j^post1 == 0 /\ -sourceflag^post1+sourceflag^0 == 0 /\ -k_1^post1+k_1^0 == 0), cost: 1
  39: l3 -> l4 : i^0'=i^post39, destflag^0'=destflag^post39, nodecount^0'=nodecount^post39, k^0'=k^post39, h^0'=h^post39, __lengthofvisited^0'=__lengthofvisited^post39, min^0'=min^post39, j^0'=j^post39, edgecount^0'=edgecount^post39, sourceflag^0'=sourceflag^post39, k_1^0'=k_1^post39, (nodecount^0-nodecount^post39 == 0 /\ -edgecount^post39+edgecount^0 == 0 /\ -k_1^post39+k_1^0 == 0 /\ -1-i^0+nodecount^0 <= 0 /\ i^0-i^post39 == 0 /\ -h^post39+h^0 == 0 /\ -__lengthofvisited^post39+__lengthofvisited^0 == 0 /\ -sourceflag^post39+sourceflag^0 == 0 /\ j^0-j^post39 == 0 /\ k^post39 == 0 /\ -destflag^post39+destflag^0 == 0 /\ -min^post39+min^0 == 0), cost: 1
  40: l3 -> l2 : i^0'=i^post40, destflag^0'=destflag^post40, nodecount^0'=nodecount^post40, k^0'=k^post40, h^0'=h^post40, __lengthofvisited^0'=__lengthofvisited^post40, min^0'=min^post40, j^0'=j^post40, edgecount^0'=edgecount^post40, sourceflag^0'=sourceflag^post40, k_1^0'=k_1^post40, (-k^post40+k^0 == 0 /\ min^0-min^post40 == 0 /\ -edgecount^post40+edgecount^0 == 0 /\ sourceflag^0-sourceflag^post40 == 0 /\ h^0-h^post40 == 0 /\ -nodecount^post40+nodecount^0 == 0 /\ -j^post40+j^0 == 0 /\ -k_1^post40+k_1^0 == 0 /\ destflag^0-destflag^post40 == 0 /\ __lengthofvisited^0-__lengthofvisited^post40 == 0 /\ 2+i^0-nodecount^0 <= 0 /\ -1-i^0+i^post40 == 0), cost: 1
   2: l4 -> l5 : i^0'=i^post2, destflag^0'=destflag^post2, nodecount^0'=nodecount^post2, k^0'=k^post2, h^0'=h^post2, __lengthofvisited^0'=__lengthofvisited^post2, min^0'=min^post2, j^0'=j^post2, edgecount^0'=edgecount^post2, sourceflag^0'=sourceflag^post2, k_1^0'=k_1^post2, (h^0-h^post2 == 0 /\ -__lengthofvisited^post2+__lengthofvisited^0 == 0 /\ -nodecount^post2+nodecount^0 == 0 /\ min^0-min^post2 == 0 /\ -k_1^post2+k_1^0 == 0 /\ -j^post2+j^0 == 0 /\ -sourceflag^post2+sourceflag^0 == 0 /\ destflag^0-destflag^post2 == 0 /\ i^0-i^post2 == 0 /\ -edgecount^post2+edgecount^0 == 0 /\ k^0-k^post2 == 0), cost: 1
  37: l5 -> l25 : i^0'=i^post37, destflag^0'=destflag^post37, nodecount^0'=nodecount^post37, k^0'=k^post37, h^0'=h^post37, __lengthofvisited^0'=__lengthofvisited^post37, min^0'=min^post37, j^0'=j^post37, edgecount^0'=edgecount^post37, sourceflag^0'=sourceflag^post37, k_1^0'=k_1^post37, (-destflag^post37+destflag^0 == 0 /\ -edgecount^post37+edgecount^0 == 0 /\ min^0-min^post37 == 0 /\ -nodecount^post37+nodecount^0 == 0 /\ k^0-k^post37 == 0 /\ -__lengthofvisited^post37+__lengthofvisited^0 == 0 /\ nodecount^0-k^0 <= 0 /\ -j^post37+j^0 == 0 /\ i^0-i^post37 == 0 /\ -k_1^post37+k_1^0 == 0 /\ -sourceflag^post37+sourceflag^0 == 0 /\ h^0-h^post37 == 0), cost: 1
  38: l5 -> l25 : i^0'=i^post38, destflag^0'=destflag^post38, nodecount^0'=nodecount^post38, k^0'=k^post38, h^0'=h^post38, __lengthofvisited^0'=__lengthofvisited^post38, min^0'=min^post38, j^0'=j^post38, edgecount^0'=edgecount^post38, sourceflag^0'=sourceflag^post38, k_1^0'=k_1^post38, (__lengthofvisited^0-__lengthofvisited^post38 == 0 /\ edgecount^0-edgecount^post38 == 0 /\ -k^post38+k^0 == 0 /\ destflag^0-destflag^post38 == 0 /\ 2-nodecount^0+k^0 <= 0 /\ i^0-i^post38 == 0 /\ nodecount^0-nodecount^post38 == 0 /\ h^0-h^post38 == 0 /\ -j^post38+j^0 == 0 /\ -sourceflag^post38+sourceflag^0 == 0 /\ -k_1^post38+k_1^0 == 0 /\ -min^post38+min^0 == 0), cost: 1
   3: l6 -> l7 : i^0'=i^post3, destflag^0'=destflag^post3, nodecount^0'=nodecount^post3, k^0'=k^post3, h^0'=h^post3, __lengthofvisited^0'=__lengthofvisited^post3, min^0'=min^post3, j^0'=j^post3, edgecount^0'=edgecount^post3, sourceflag^0'=sourceflag^post3, k_1^0'=k_1^post3, (-1+k_1^post3-k_1^0 == 0 /\ -sourceflag^post3+sourceflag^0 == 0 /\ -h^post3+h^0 == 0 /\ -min^post3+min^0 == 0 /\ edgecount^0-edgecount^post3 == 0 /\ nodecount^0-nodecount^post3 == 0 /\ j^0-j^post3 == 0 /\ destflag^0-destflag^post3 == 0 /\ -__lengthofvisited^post3+__lengthofvisited^0 == 0 /\ i^0-i^post3 == 0 /\ k^0-k^post3 == 0), cost: 1
  18: l7 -> l18 : i^0'=i^post18, destflag^0'=destflag^post18, nodecount^0'=nodecount^post18, k^0'=k^post18, h^0'=h^post18, __lengthofvisited^0'=__lengthofvisited^post18, min^0'=min^post18, j^0'=j^post18, edgecount^0'=edgecount^post18, sourceflag^0'=sourceflag^post18, k_1^0'=k_1^post18, (edgecount^0-edgecount^post18 == 0 /\ -k_1^post18+k_1^0 == 0 /\ -k^post18+k^0 == 0 /\ destflag^0-destflag^post18 == 0 /\ __lengthofvisited^0-__lengthofvisited^post18 == 0 /\ nodecount^0-nodecount^post18 == 0 /\ -sourceflag^post18+sourceflag^0 == 0 /\ h^0-h^post18 == 0 /\ -j^post18+j^0 == 0 /\ i^0-i^post18 == 0 /\ -min^post18+min^0 == 0), cost: 1
   4: l8 -> l6 : i^0'=i^post4, destflag^0'=destflag^post4, nodecount^0'=nodecount^post4, k^0'=k^post4, h^0'=h^post4, __lengthofvisited^0'=__lengthofvisited^post4, min^0'=min^post4, j^0'=j^post4, edgecount^0'=edgecount^post4, sourceflag^0'=sourceflag^post4, k_1^0'=k_1^post4, (-sourceflag^post4+sourceflag^0 == 0 /\ -destflag^post4+destflag^0 == 0 /\ min^0-min^post4 == 0 /\ -k_1^post4+k_1^0 == 0 /\ 1-destflag^0 <= 0 /\ -edgecount^post4+edgecount^0 == 0 /\ i^0-i^post4 == 0 /\ k^0-k^post4 == 0 /\ nodecount^0-nodecount^post4 == 0 /\ h^0-h^post4 == 0 /\ j^0-j^post4 == 0 /\ -__lengthofvisited^post4+__lengthofvisited^0 == 0), cost: 1
   5: l8 -> l6 : i^0'=i^post5, destflag^0'=destflag^post5, nodecount^0'=nodecount^post5, k^0'=k^post5, h^0'=h^post5, __lengthofvisited^0'=__lengthofvisited^post5, min^0'=min^post5, j^0'=j^post5, edgecount^0'=edgecount^post5, sourceflag^0'=sourceflag^post5, k_1^0'=k_1^post5, (-j^post5+j^0 == 0 /\ -edgecount^post5+edgecount^0 == 0 /\ 1+destflag^0 <= 0 /\ -sourceflag^post5+sourceflag^0 == 0 /\ -k_1^post5+k_1^0 == 0 /\ -k^post5+k^0 == 0 /\ h^0-h^post5 == 0 /\ -min^post5+min^0 == 0 /\ i^0-i^post5 == 0 /\ destflag^0-destflag^post5 == 0 /\ __lengthofvisited^0-__lengthofvisited^post5 == 0 /\ nodecount^0-nodecount^post5 == 0), cost: 1
   6: l8 -> l6 : i^0'=i^post6, destflag^0'=destflag^post6, nodecount^0'=nodecount^post6, k^0'=k^post6, h^0'=h^post6, __lengthofvisited^0'=__lengthofvisited^post6, min^0'=min^post6, j^0'=j^post6, edgecount^0'=edgecount^post6, sourceflag^0'=sourceflag^post6, k_1^0'=k_1^post6, (-h^post6+h^0 == 0 /\ -__lengthofvisited^post6+__lengthofvisited^0 == 0 /\ destflag^0 <= 0 /\ i^0-i^post6 == 0 /\ k^0-k^post6 == 0 /\ -sourceflag^post6+sourceflag^0 == 0 /\ -k_1^post6+k_1^0 == 0 /\ -destflag^0 <= 0 /\ -min^post6+min^0 == 0 /\ destflag^0-destflag^post6 == 0 /\ j^0-j^post6 == 0 /\ -edgecount^post6+edgecount^0 == 0 /\ nodecount^0-nodecount^post6 == 0), cost: 1
   7: l9 -> l6 : i^0'=i^post7, destflag^0'=destflag^post7, nodecount^0'=nodecount^post7, k^0'=k^post7, h^0'=h^post7, __lengthofvisited^0'=__lengthofvisited^post7, min^0'=min^post7, j^0'=j^post7, edgecount^0'=edgecount^post7, sourceflag^0'=sourceflag^post7, k_1^0'=k_1^post7, (-edgecount^post7+edgecount^0 == 0 /\ -k^post7+k^0 == 0 /\ -k_1^post7+k_1^0 == 0 /\ 1-sourceflag^0 <= 0 /\ -__lengthofvisited^post7+__lengthofvisited^0 == 0 /\ min^0-min^post7 == 0 /\ h^0-h^post7 == 0 /\ destflag^0-destflag^post7 == 0 /\ i^0-i^post7 == 0 /\ nodecount^0-nodecount^post7 == 0 /\ -sourceflag^post7+sourceflag^0 == 0 /\ -j^post7+j^0 == 0), cost: 1
   8: l9 -> l6 : i^0'=i^post8, destflag^0'=destflag^post8, nodecount^0'=nodecount^post8, k^0'=k^post8, h^0'=h^post8, __lengthofvisited^0'=__lengthofvisited^post8, min^0'=min^post8, j^0'=j^post8, edgecount^0'=edgecount^post8, sourceflag^0'=sourceflag^post8, k_1^0'=k_1^post8, (edgecount^0-edgecount^post8 == 0 /\ -sourceflag^post8+sourceflag^0 == 0 /\ destflag^0-destflag^post8 == 0 /\ __lengthofvisited^0-__lengthofvisited^post8 == 0 /\ -min^post8+min^0 == 0 /\ -j^post8+j^0 == 0 /\ nodecount^0-nodecount^post8 == 0 /\ 1+sourceflag^0 <= 0 /\ h^0-h^post8 == 0 /\ -k_1^post8+k_1^0 == 0 /\ i^0-i^post8 == 0 /\ -k^post8+k^0 == 0), cost: 1
   9: l9 -> l8 : i^0'=i^post9, destflag^0'=destflag^post9, nodecount^0'=nodecount^post9, k^0'=k^post9, h^0'=h^post9, __lengthofvisited^0'=__lengthofvisited^post9, min^0'=min^post9, j^0'=j^post9, edgecount^0'=edgecount^post9, sourceflag^0'=sourceflag^post9, k_1^0'=k_1^post9, (-sourceflag^post9+sourceflag^0 == 0 /\ -h^post9+h^0 == 0 /\ -sourceflag^0 <= 0 /\ k^0-k^post9 == 0 /\ -k_1^post9+k_1^0 == 0 /\ -destflag^post9+destflag^0 == 0 /\ min^0-min^post9 == 0 /\ i^0-i^post9 == 0 /\ -edgecount^post9+edgecount^0 == 0 /\ nodecount^0-nodecount^post9 == 0 /\ sourceflag^0 <= 0 /\ j^0-j^post9 == 0 /\ -__lengthofvisited^post9+__lengthofvisited^0 == 0), cost: 1
  10: l10 -> l11 : i^0'=i^post10, destflag^0'=destflag^post10, nodecount^0'=nodecount^post10, k^0'=k^post10, h^0'=h^post10, __lengthofvisited^0'=__lengthofvisited^post10, min^0'=min^post10, j^0'=j^post10, edgecount^0'=edgecount^post10, sourceflag^0'=sourceflag^post10, k_1^0'=k_1^post10, (i^0-i^post10 == 0 /\ min^0-min^post10 == 0 /\ sourceflag^0-sourceflag^post10 == 0 /\ -nodecount^post10+nodecount^0 == 0 /\ -edgecount^post10+edgecount^0 == 0 /\ h^0-h^post10 == 0 /\ -j^post10+j^0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post10 == 0 /\ -k^post10+k^0 == 0 /\ destflag^0-destflag^post10 == 0 /\ -k_1^post10+k_1^0 == 0), cost: 1
  32: l11 -> l7 : i^0'=i^post32, destflag^0'=destflag^post32, nodecount^0'=nodecount^post32, k^0'=k^post32, h^0'=h^post32, __lengthofvisited^0'=__lengthofvisited^post32, min^0'=min^post32, j^0'=j^post32, edgecount^0'=edgecount^post32, sourceflag^0'=sourceflag^post32, k_1^0'=k_1^post32, (k_1^post32 == 0 /\ -j^post32+j^0 == 0 /\ -__lengthofvisited^post32+__lengthofvisited^0 == 0 /\ h^0-h^post32 == 0 /\ min^0-min^post32 == 0 /\ destflag^0-destflag^post32 == 0 /\ -sourceflag^post32+sourceflag^0 == 0 /\ -i^0+edgecount^0 <= 0 /\ -nodecount^post32+nodecount^0 == 0 /\ i^0-i^post32 == 0 /\ -edgecount^post32+edgecount^0 == 0 /\ k^0-k^post32 == 0), cost: 1
  33: l11 -> l10 : i^0'=i^post33, destflag^0'=destflag^post33, nodecount^0'=nodecount^post33, k^0'=k^post33, h^0'=h^post33, __lengthofvisited^0'=__lengthofvisited^post33, min^0'=min^post33, j^0'=j^post33, edgecount^0'=edgecount^post33, sourceflag^0'=sourceflag^post33, k_1^0'=k_1^post33, (1+i^0-edgecount^0 <= 0 /\ __lengthofvisited^0-__lengthofvisited^post33 == 0 /\ -sourceflag^post33+sourceflag^0 == 0 /\ -1+i^post33-i^0 == 0 /\ -k^post33+k^0 == 0 /\ destflag^0-destflag^post33 == 0 /\ -edgecount^post33+edgecount^0 == 0 /\ -k_1^post33+k_1^0 == 0 /\ h^0-h^post33 == 0 /\ -j^post33+j^0 == 0 /\ nodecount^0-nodecount^post33 == 0 /\ -min^post33+min^0 == 0), cost: 1
  11: l12 -> l13 : i^0'=i^post11, destflag^0'=destflag^post11, nodecount^0'=nodecount^post11, k^0'=k^post11, h^0'=h^post11, __lengthofvisited^0'=__lengthofvisited^post11, min^0'=min^post11, j^0'=j^post11, edgecount^0'=edgecount^post11, sourceflag^0'=sourceflag^post11, k_1^0'=k_1^post11, (i^0-i^post11 == 0 /\ -h^post11+h^0 == 0 /\ nodecount^0-nodecount^post11 == 0 /\ -edgecount^post11+edgecount^0 == 0 /\ destflag^0-destflag^post11 == 0 /\ __lengthofvisited^0-__lengthofvisited^post11 == 0 /\ -sourceflag^post11+sourceflag^0 == 0 /\ -min^post11+min^0 == 0 /\ -1-j^0+j^post11 == 0 /\ -k_1^post11+k_1^0 == 0 /\ k^0-k^post11 == 0), cost: 1
  41: l13 -> l15 : i^0'=i^post41, destflag^0'=destflag^post41, nodecount^0'=nodecount^post41, k^0'=k^post41, h^0'=h^post41, __lengthofvisited^0'=__lengthofvisited^post41, min^0'=min^post41, j^0'=j^post41, edgecount^0'=edgecount^post41, sourceflag^0'=sourceflag^post41, k_1^0'=k_1^post41, (k^0-k^post41 == 0 /\ -min^post41+min^0 == 0 /\ i^0-i^post41 == 0 /\ nodecount^0-nodecount^post41 == 0 /\ edgecount^0-edgecount^post41 == 0 /\ -h^post41+h^0 == 0 /\ -__lengthofvisited^post41+__lengthofvisited^0 == 0 /\ j^0-j^post41 == 0 /\ destflag^0-destflag^post41 == 0 /\ -sourceflag^post41+sourceflag^0 == 0 /\ -k_1^post41+k_1^0 == 0), cost: 1
  12: l14 -> l12 : i^0'=i^post12, destflag^0'=destflag^post12, nodecount^0'=nodecount^post12, k^0'=k^post12, h^0'=h^post12, __lengthofvisited^0'=__lengthofvisited^post12, min^0'=min^post12, j^0'=j^post12, edgecount^0'=edgecount^post12, sourceflag^0'=sourceflag^post12, k_1^0'=k_1^post12, (h^0-h^post12 == 0 /\ -__lengthofvisited^post12+__lengthofvisited^0 == 0 /\ min^0-min^post12 == 0 /\ -j^post12+j^0 == 0 /\ -sourceflag^post12+sourceflag^0 == 0 /\ -k_1^post12+k_1^0 == 0 /\ -nodecount^post12+nodecount^0 == 0 /\ destflag^0-destflag^post12 == 0 /\ i^0-i^post12 == 0 /\ k^0-k^post12 == 0 /\ -edgecount^post12+edgecount^0 == 0), cost: 1
  13: l14 -> l12 : i^0'=i^post13, destflag^0'=destflag^post13, nodecount^0'=nodecount^post13, k^0'=k^post13, h^0'=h^post13, __lengthofvisited^0'=__lengthofvisited^post13, min^0'=min^post13, j^0'=j^post13, edgecount^0'=edgecount^post13, sourceflag^0'=sourceflag^post13, k_1^0'=k_1^post13, (__lengthofvisited^0-__lengthofvisited^post13 == 0 /\ -sourceflag^post13+sourceflag^0 == 0 /\ -min^post13+min^0 == 0 /\ -k^post13+k^0 == 0 /\ -j^post13+j^0 == 0 /\ -edgecount^post13+edgecount^0 == 0 /\ destflag^post13 == 0 /\ h^0-h^post13 == 0 /\ -k_1^post13+k_1^0 == 0 /\ -i^post13+i^0 == 0 /\ nodecount^0-nodecount^post13 == 0), cost: 1
  14: l14 -> l12 : i^0'=i^post14, destflag^0'=destflag^post14, nodecount^0'=nodecount^post14, k^0'=k^post14, h^0'=h^post14, __lengthofvisited^0'=__lengthofvisited^post14, min^0'=min^post14, j^0'=j^post14, edgecount^0'=edgecount^post14, sourceflag^0'=sourceflag^post14, k_1^0'=k_1^post14, (-h^post14+h^0 == 0 /\ -sourceflag^post14+sourceflag^0 == 0 /\ k^0-k^post14 == 0 /\ -__lengthofvisited^post14+__lengthofvisited^0 == 0 /\ -k_1^post14+k_1^0 == 0 /\ j^0-j^post14 == 0 /\ i^0-i^post14 == 0 /\ -edgecount^post14+edgecount^0 == 0 /\ -min^post14+min^0 == 0 /\ nodecount^0-nodecount^post14 == 0 /\ destflag^0-destflag^post14 == 0), cost: 1
  15: l15 -> l9 : i^0'=i^post15, destflag^0'=destflag^post15, nodecount^0'=nodecount^post15, k^0'=k^post15, h^0'=h^post15, __lengthofvisited^0'=__lengthofvisited^post15, min^0'=min^post15, j^0'=j^post15, edgecount^0'=edgecount^post15, sourceflag^0'=sourceflag^post15, k_1^0'=k_1^post15, (-j^post15+j^0 == 0 /\ -k_1^post15+k_1^0 == 0 /\ nodecount^0-nodecount^post15 == 0 /\ nodecount^0-j^0 <= 0 /\ -edgecount^post15+edgecount^0 == 0 /\ -sourceflag^post15+sourceflag^0 == 0 /\ i^0-i^post15 == 0 /\ -k^post15+k^0 == 0 /\ h^0-h^post15 == 0 /\ -min^post15+min^0 == 0 /\ destflag^0-destflag^post15 == 0 /\ __lengthofvisited^0-__lengthofvisited^post15 == 0), cost: 1
  16: l15 -> l14 : i^0'=i^post16, destflag^0'=destflag^post16, nodecount^0'=nodecount^post16, k^0'=k^post16, h^0'=h^post16, __lengthofvisited^0'=__lengthofvisited^post16, min^0'=min^post16, j^0'=j^post16, edgecount^0'=edgecount^post16, sourceflag^0'=sourceflag^post16, k_1^0'=k_1^post16, (-h^post16+h^0 == 0 /\ j^0-j^post16 == 0 /\ destflag^0-destflag^post16 == 0 /\ __lengthofvisited^0-__lengthofvisited^post16 == 0 /\ -sourceflag^post16+sourceflag^0 == 0 /\ -k_1^post16+k_1^0 == 0 /\ nodecount^0-nodecount^post16 == 0 /\ 1-nodecount^0+j^0 <= 0 /\ edgecount^0-edgecount^post16 == 0 /\ -min^post16+min^0 == 0 /\ i^0-i^post16 == 0 /\ k^0-k^post16 == 0), cost: 1
  17: l16 -> l17 : i^0'=i^post17, destflag^0'=destflag^post17, nodecount^0'=nodecount^post17, k^0'=k^post17, h^0'=h^post17, __lengthofvisited^0'=__lengthofvisited^post17, min^0'=min^post17, j^0'=j^post17, edgecount^0'=edgecount^post17, sourceflag^0'=sourceflag^post17, k_1^0'=k_1^post17, (-destflag^post17+destflag^0 == 0 /\ -__lengthofvisited^post17+__lengthofvisited^0 == 0 /\ -sourceflag^post17+sourceflag^0 == 0 /\ -k_1^post17+k_1^0 == 0 /\ -1+j^post17-j^0 == 0 /\ min^0-min^post17 == 0 /\ -nodecount^post17+nodecount^0 == 0 /\ k^0-k^post17 == 0 /\ h^0-h^post17 == 0 /\ i^0-i^post17 == 0 /\ -edgecount^post17+edgecount^0 == 0), cost: 1
  34: l17 -> l20 : i^0'=i^post34, destflag^0'=destflag^post34, nodecount^0'=nodecount^post34, k^0'=k^post34, h^0'=h^post34, __lengthofvisited^0'=__lengthofvisited^post34, min^0'=min^post34, j^0'=j^post34, edgecount^0'=edgecount^post34, sourceflag^0'=sourceflag^post34, k_1^0'=k_1^post34, (-edgecount^post34+edgecount^0 == 0 /\ -k_1^post34+k_1^0 == 0 /\ k^0-k^post34 == 0 /\ i^0-i^post34 == 0 /\ -__lengthofvisited^post34+__lengthofvisited^0 == 0 /\ -sourceflag^post34+sourceflag^0 == 0 /\ j^0-j^post34 == 0 /\ -min^post34+min^0 == 0 /\ nodecount^0-nodecount^post34 == 0 /\ -h^post34+h^0 == 0 /\ destflag^0-destflag^post34 == 0), cost: 1
  30: l18 -> l4 : i^0'=i^post30, destflag^0'=destflag^post30, nodecount^0'=nodecount^post30, k^0'=k^post30, h^0'=h^post30, __lengthofvisited^0'=__lengthofvisited^post30, min^0'=min^post30, j^0'=j^post30, edgecount^0'=edgecount^post30, sourceflag^0'=sourceflag^post30, k_1^0'=k_1^post30, (sourceflag^0-sourceflag^post30 == 0 /\ destflag^0-destflag^post30 == 0 /\ __lengthofvisited^0-__lengthofvisited^post30 == 0 /\ i^0-i^post30 == 0 /\ -min^post30+min^0 == 0 /\ edgecount^0-k_1^0 <= 0 /\ -j^post30+j^0 == 0 /\ -1+k^post30-k^0 == 0 /\ -k_1^post30+k_1^0 == 0 /\ h^0-h^post30 == 0 /\ -edgecount^post30+edgecount^0 == 0 /\ -nodecount^post30+nodecount^0 == 0), cost: 1
  31: l18 -> l22 : i^0'=i^post31, destflag^0'=destflag^post31, nodecount^0'=nodecount^post31, k^0'=k^post31, h^0'=h^post31, __lengthofvisited^0'=__lengthofvisited^post31, min^0'=min^post31, j^0'=j^post31, edgecount^0'=edgecount^post31, sourceflag^0'=sourceflag^post31, k_1^0'=k_1^post31, (1-edgecount^0+k_1^0 <= 0 /\ h^post31 == 0 /\ destflag^0-destflag^post31 == 0 /\ j^0-j^post31 == 0 /\ __lengthofvisited^0-__lengthofvisited^post31 == 0 /\ edgecount^0-edgecount^post31 == 0 /\ -sourceflag^post31+sourceflag^0 == 0 /\ nodecount^0-nodecount^post31 == 0 /\ -k_1^post31+k_1^0 == 0 /\ -min^post31+min^0 == 0 /\ i^0-i^post31 == 0 /\ k^0-k^post31 == 0), cost: 1
  19: l19 -> l16 : i^0'=i^post19, destflag^0'=destflag^post19, nodecount^0'=nodecount^post19, k^0'=k^post19, h^0'=h^post19, __lengthofvisited^0'=__lengthofvisited^post19, min^0'=min^post19, j^0'=j^post19, edgecount^0'=edgecount^post19, sourceflag^0'=sourceflag^post19, k_1^0'=k_1^post19, (-sourceflag^post19+sourceflag^0 == 0 /\ -h^post19+h^0 == 0 /\ k^0-k^post19 == 0 /\ -edgecount^post19+edgecount^0 == 0 /\ min^0-min^post19 == 0 /\ -k_1^post19+k_1^0 == 0 /\ -destflag^post19+destflag^0 == 0 /\ i^0-i^post19 == 0 /\ nodecount^0-nodecount^post19 == 0 /\ j^0-j^post19 == 0 /\ -__lengthofvisited^post19+__lengthofvisited^0 == 0), cost: 1
  20: l19 -> l16 : i^0'=i^post20, destflag^0'=destflag^post20, nodecount^0'=nodecount^post20, k^0'=k^post20, h^0'=h^post20, __lengthofvisited^0'=__lengthofvisited^post20, min^0'=min^post20, j^0'=j^post20, edgecount^0'=edgecount^post20, sourceflag^0'=sourceflag^post20, k_1^0'=k_1^post20, (__lengthofvisited^0-__lengthofvisited^post20 == 0 /\ -j^post20+j^0 == 0 /\ -k^post20+k^0 == 0 /\ -k_1^post20+k_1^0 == 0 /\ h^0-h^post20 == 0 /\ i^0-i^post20 == 0 /\ -edgecount^post20+edgecount^0 == 0 /\ -min^post20+min^0 == 0 /\ nodecount^0-nodecount^post20 == 0 /\ -1+sourceflag^post20 == 0 /\ destflag^0-destflag^post20 == 0), cost: 1
  21: l19 -> l16 : i^0'=i^post21, destflag^0'=destflag^post21, nodecount^0'=nodecount^post21, k^0'=k^post21, h^0'=h^post21, __lengthofvisited^0'=__lengthofvisited^post21, min^0'=min^post21, j^0'=j^post21, edgecount^0'=edgecount^post21, sourceflag^0'=sourceflag^post21, k_1^0'=k_1^post21, (-h^post21+h^0 == 0 /\ i^0-i^post21 == 0 /\ -__lengthofvisited^post21+__lengthofvisited^0 == 0 /\ nodecount^0-nodecount^post21 == 0 /\ -edgecount^post21+edgecount^0 == 0 /\ k^0-k^post21 == 0 /\ -sourceflag^post21+sourceflag^0 == 0 /\ -k_1^post21+k_1^0 == 0 /\ -min^post21+min^0 == 0 /\ j^0-j^post21 == 0 /\ destflag^0-destflag^post21 == 0), cost: 1
  22: l20 -> l13 : i^0'=i^post22, destflag^0'=destflag^post22, nodecount^0'=nodecount^post22, k^0'=k^post22, h^0'=h^post22, __lengthofvisited^0'=__lengthofvisited^post22, min^0'=min^post22, j^0'=j^post22, edgecount^0'=edgecount^post22, sourceflag^0'=sourceflag^post22, k_1^0'=k_1^post22, (nodecount^0-j^0 <= 0 /\ j^post22 == 0 /\ -__lengthofvisited^post22+__lengthofvisited^0 == 0 /\ h^0-h^post22 == 0 /\ min^0-min^post22 == 0 /\ -sourceflag^post22+sourceflag^0 == 0 /\ -k_1^post22+k_1^0 == 0 /\ -1+destflag^post22 == 0 /\ -nodecount^post22+nodecount^0 == 0 /\ i^0-i^post22 == 0 /\ k^0-k^post22 == 0 /\ -edgecount^post22+edgecount^0 == 0), cost: 1
  23: l20 -> l19 : i^0'=i^post23, destflag^0'=destflag^post23, nodecount^0'=nodecount^post23, k^0'=k^post23, h^0'=h^post23, __lengthofvisited^0'=__lengthofvisited^post23, min^0'=min^post23, j^0'=j^post23, edgecount^0'=edgecount^post23, sourceflag^0'=sourceflag^post23, k_1^0'=k_1^post23, (-sourceflag^post23+sourceflag^0 == 0 /\ j^0-j^post23 == 0 /\ __lengthofvisited^0-__lengthofvisited^post23 == 0 /\ -k_1^post23+k_1^0 == 0 /\ -k^post23+k^0 == 0 /\ 1-nodecount^0+j^0 <= 0 /\ nodecount^0-nodecount^post23 == 0 /\ destflag^0-destflag^post23 == 0 /\ edgecount^0-edgecount^post23 == 0 /\ -min^post23+min^0 == 0 /\ h^0-h^post23 == 0 /\ i^0-i^post23 == 0), cost: 1
  24: l21 -> l22 : i^0'=i^post24, destflag^0'=destflag^post24, nodecount^0'=nodecount^post24, k^0'=k^post24, h^0'=h^post24, __lengthofvisited^0'=__lengthofvisited^post24, min^0'=min^post24, j^0'=j^post24, edgecount^0'=edgecount^post24, sourceflag^0'=sourceflag^post24, k_1^0'=k_1^post24, (-k_1^post24+k_1^0 == 0 /\ -destflag^post24+destflag^0 == 0 /\ -__lengthofvisited^post24+__lengthofvisited^0 == 0 /\ -1-h^0+h^post24 == 0 /\ min^0-min^post24 == 0 /\ -edgecount^post24+edgecount^0 == 0 /\ i^0-i^post24 == 0 /\ k^0-k^post24 == 0 /\ -sourceflag^post24+sourceflag^0 == 0 /\ nodecount^0-nodecount^post24 == 0 /\ -j^post24+j^0 == 0), cost: 1
  27: l22 -> l24 : i^0'=i^post27, destflag^0'=destflag^post27, nodecount^0'=nodecount^post27, k^0'=k^post27, h^0'=h^post27, __lengthofvisited^0'=__lengthofvisited^post27, min^0'=min^post27, j^0'=j^post27, edgecount^0'=edgecount^post27, sourceflag^0'=sourceflag^post27, k_1^0'=k_1^post27, (min^0-min^post27 == 0 /\ -k^post27+k^0 == 0 /\ sourceflag^0-sourceflag^post27 == 0 /\ -k_1^post27+k_1^0 == 0 /\ h^0-h^post27 == 0 /\ destflag^0-destflag^post27 == 0 /\ __lengthofvisited^0-__lengthofvisited^post27 == 0 /\ -j^post27+j^0 == 0 /\ -nodecount^post27+nodecount^0 == 0 /\ i^0-i^post27 == 0 /\ -edgecount^post27+edgecount^0 == 0), cost: 1
  25: l23 -> l21 : i^0'=i^post25, destflag^0'=destflag^post25, nodecount^0'=nodecount^post25, k^0'=k^post25, h^0'=h^post25, __lengthofvisited^0'=__lengthofvisited^post25, min^0'=min^post25, j^0'=j^post25, edgecount^0'=edgecount^post25, sourceflag^0'=sourceflag^post25, k_1^0'=k_1^post25, (-k_1^post25+k_1^0 == 0 /\ min^post25-h^0 == 0 /\ sourceflag^0-sourceflag^post25 == 0 /\ -edgecount^post25+edgecount^0 == 0 /\ -nodecount^post25+nodecount^0 == 0 /\ i^0-i^post25 == 0 /\ -k^post25+k^0 == 0 /\ h^0-h^post25 == 0 /\ destflag^0-destflag^post25 == 0 /\ __lengthofvisited^0-__lengthofvisited^post25 == 0 /\ -j^post25+j^0 == 0), cost: 1
  26: l23 -> l21 : i^0'=i^post26, destflag^0'=destflag^post26, nodecount^0'=nodecount^post26, k^0'=k^post26, h^0'=h^post26, __lengthofvisited^0'=__lengthofvisited^post26, min^0'=min^post26, j^0'=j^post26, edgecount^0'=edgecount^post26, sourceflag^0'=sourceflag^post26, k_1^0'=k_1^post26, (-k_1^post26+k_1^0 == 0 /\ nodecount^0-nodecount^post26 == 0 /\ k^0-k^post26 == 0 /\ -__lengthofvisited^post26+__lengthofvisited^0 == 0 /\ -h^post26+h^0 == 0 /\ -edgecount^post26+edgecount^0 == 0 /\ -sourceflag^post26+sourceflag^0 == 0 /\ i^0-i^post26 == 0 /\ destflag^0-destflag^post26 == 0 /\ -min^post26+min^0 == 0 /\ j^0-j^post26 == 0), cost: 1
  28: l24 -> l17 : i^0'=i^post28, destflag^0'=destflag^post28, nodecount^0'=nodecount^post28, k^0'=k^post28, h^0'=h^post28, __lengthofvisited^0'=__lengthofvisited^post28, min^0'=min^post28, j^0'=j^post28, edgecount^0'=edgecount^post28, sourceflag^0'=sourceflag^post28, k_1^0'=k_1^post28, (sourceflag^post28 == 0 /\ edgecount^0-edgecount^post28 == 0 /\ -k^post28+k^0 == 0 /\ destflag^0-destflag^post28 == 0 /\ __lengthofvisited^0-__lengthofvisited^post28 == 0 /\ j^post28 == 0 /\ i^0-i^post28 == 0 /\ nodecount^0-nodecount^post28 == 0 /\ h^0-h^post28 == 0 /\ -k_1^post28+k_1^0 == 0 /\ -min^post28+min^0 == 0 /\ -h^0+edgecount^0 <= 0), cost: 1
  29: l24 -> l23 : i^0'=i^post29, destflag^0'=destflag^post29, nodecount^0'=nodecount^post29, k^0'=k^post29, h^0'=h^post29, __lengthofvisited^0'=__lengthofvisited^post29, min^0'=min^post29, j^0'=j^post29, edgecount^0'=edgecount^post29, sourceflag^0'=sourceflag^post29, k_1^0'=k_1^post29, (-destflag^post29+destflag^0 == 0 /\ -edgecount^post29+edgecount^0 == 0 /\ -k_1^post29+k_1^0 == 0 /\ -__lengthofvisited^post29+__lengthofvisited^0 == 0 /\ k^0-k^post29 == 0 /\ min^0-min^post29 == 0 /\ i^0-i^post29 == 0 /\ 1+h^0-edgecount^0 <= 0 /\ nodecount^0-nodecount^post29 == 0 /\ -sourceflag^post29+sourceflag^0 == 0 /\ h^0-h^post29 == 0 /\ -j^post29+j^0 == 0), cost: 1
  35: l25 -> l10 : i^0'=i^post35, destflag^0'=destflag^post35, nodecount^0'=nodecount^post35, k^0'=k^post35, h^0'=h^post35, __lengthofvisited^0'=__lengthofvisited^post35, min^0'=min^post35, j^0'=j^post35, edgecount^0'=edgecount^post35, sourceflag^0'=sourceflag^post35, k_1^0'=k_1^post35, (min^post35 == 0 /\ -k_1^post35+k_1^0 == 0 /\ sourceflag^0-sourceflag^post35 == 0 /\ -edgecount^post35+edgecount^0 == 0 /\ -nodecount^post35+nodecount^0 == 0 /\ h^0-h^post35 == 0 /\ -k^post35+k^0 == 0 /\ destflag^0-destflag^post35 == 0 /\ __lengthofvisited^0-__lengthofvisited^post35 == 0 /\ i^post35 == 0 /\ -j^post35+j^0 == 0), cost: 1
  44: l27 -> l0 : i^0'=i^post44, destflag^0'=destflag^post44, nodecount^0'=nodecount^post44, k^0'=k^post44, h^0'=h^post44, __lengthofvisited^0'=__lengthofvisited^post44, min^0'=min^post44, j^0'=j^post44, edgecount^0'=edgecount^post44, sourceflag^0'=sourceflag^post44, k_1^0'=k_1^post44, (-destflag^post44+destflag^0 == 0 /\ -edgecount^post44+edgecount^0 == 0 /\ min^0-min^post44 == 0 /\ __lengthofvisited^post44-edgecount^0 == 0 /\ k^0-k^post44 == 0 /\ nodecount^0-nodecount^post44 == 0 /\ -k_1^post44+k_1^0 == 0 /\ h^0-h^post44 == 0 /\ -1+i^post44 == 0 /\ -sourceflag^post44+sourceflag^0 == 0 /\ -j^post44+j^0 == 0), cost: 1
  45: l28 -> l27 : i^0'=i^post45, destflag^0'=destflag^post45, nodecount^0'=nodecount^post45, k^0'=k^post45, h^0'=h^post45, __lengthofvisited^0'=__lengthofvisited^post45, min^0'=min^post45, j^0'=j^post45, edgecount^0'=edgecount^post45, sourceflag^0'=sourceflag^post45, k_1^0'=k_1^post45, (-edgecount^post45+edgecount^0 == 0 /\ sourceflag^0-sourceflag^post45 == 0 /\ -k_1^post45+k_1^0 == 0 /\ h^0-h^post45 == 0 /\ -nodecount^post45+nodecount^0 == 0 /\ i^0-i^post45 == 0 /\ -min^post45+min^0 == 0 /\ -j^post45+j^0 == 0 /\ -k^post45+k^0 == 0 /\ destflag^0-destflag^post45 == 0 /\ __lengthofvisited^0-__lengthofvisited^post45 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : i^0'=i^post0, destflag^0'=destflag^post0, nodecount^0'=nodecount^post0, k^0'=k^post0, h^0'=h^post0, __lengthofvisited^0'=__lengthofvisited^post0, min^0'=min^post0, j^0'=j^post0, edgecount^0'=edgecount^post0, sourceflag^0'=sourceflag^post0, k_1^0'=k_1^post0, (-sourceflag^post0+sourceflag^0 == 0 /\ -k^post0+k^0 == 0 /\ destflag^0-destflag^post0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post0 == 0 /\ -min^post0+min^0 == 0 /\ -k_1^post0+k_1^0 == 0 /\ -j^post0+j^0 == 0 /\ -edgecount^post0+edgecount^0 == 0 /\ i^0-i^post0 == 0 /\ nodecount^0-nodecount^post0 == 0 /\ h^0-h^post0 == 0), cost: 1
New rule:
l0 -> l1 : TRUE, cost: 1

Applied preprocessing
Original rule:
l2 -> l3 : i^0'=i^post1, destflag^0'=destflag^post1, nodecount^0'=nodecount^post1, k^0'=k^post1, h^0'=h^post1, __lengthofvisited^0'=__lengthofvisited^post1, min^0'=min^post1, j^0'=j^post1, edgecount^0'=edgecount^post1, sourceflag^0'=sourceflag^post1, k_1^0'=k_1^post1, (i^0-i^post1 == 0 /\ nodecount^0-nodecount^post1 == 0 /\ -h^post1+h^0 == 0 /\ -edgecount^post1+edgecount^0 == 0 /\ k^0-k^post1 == 0 /\ -min^post1+min^0 == 0 /\ -__lengthofvisited^post1+__lengthofvisited^0 == 0 /\ destflag^0-destflag^post1 == 0 /\ j^0-j^post1 == 0 /\ -sourceflag^post1+sourceflag^0 == 0 /\ -k_1^post1+k_1^0 == 0), cost: 1
New rule:
l2 -> l3 : TRUE, cost: 1

Applied preprocessing
Original rule:
l4 -> l5 : i^0'=i^post2, destflag^0'=destflag^post2, nodecount^0'=nodecount^post2, k^0'=k^post2, h^0'=h^post2, __lengthofvisited^0'=__lengthofvisited^post2, min^0'=min^post2, j^0'=j^post2, edgecount^0'=edgecount^post2, sourceflag^0'=sourceflag^post2, k_1^0'=k_1^post2, (h^0-h^post2 == 0 /\ -__lengthofvisited^post2+__lengthofvisited^0 == 0 /\ -nodecount^post2+nodecount^0 == 0 /\ min^0-min^post2 == 0 /\ -k_1^post2+k_1^0 == 0 /\ -j^post2+j^0 == 0 /\ -sourceflag^post2+sourceflag^0 == 0 /\ destflag^0-destflag^post2 == 0 /\ i^0-i^post2 == 0 /\ -edgecount^post2+edgecount^0 == 0 /\ k^0-k^post2 == 0), cost: 1
New rule:
l4 -> l5 : TRUE, cost: 1

Applied preprocessing
Original rule:
l6 -> l7 : i^0'=i^post3, destflag^0'=destflag^post3, nodecount^0'=nodecount^post3, k^0'=k^post3, h^0'=h^post3, __lengthofvisited^0'=__lengthofvisited^post3, min^0'=min^post3, j^0'=j^post3, edgecount^0'=edgecount^post3, sourceflag^0'=sourceflag^post3, k_1^0'=k_1^post3, (-1+k_1^post3-k_1^0 == 0 /\ -sourceflag^post3+sourceflag^0 == 0 /\ -h^post3+h^0 == 0 /\ -min^post3+min^0 == 0 /\ edgecount^0-edgecount^post3 == 0 /\ nodecount^0-nodecount^post3 == 0 /\ j^0-j^post3 == 0 /\ destflag^0-destflag^post3 == 0 /\ -__lengthofvisited^post3+__lengthofvisited^0 == 0 /\ i^0-i^post3 == 0 /\ k^0-k^post3 == 0), cost: 1
New rule:
l6 -> l7 : k_1^0'=1+k_1^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l8 -> l6 : i^0'=i^post4, destflag^0'=destflag^post4, nodecount^0'=nodecount^post4, k^0'=k^post4, h^0'=h^post4, __lengthofvisited^0'=__lengthofvisited^post4, min^0'=min^post4, j^0'=j^post4, edgecount^0'=edgecount^post4, sourceflag^0'=sourceflag^post4, k_1^0'=k_1^post4, (-sourceflag^post4+sourceflag^0 == 0 /\ -destflag^post4+destflag^0 == 0 /\ min^0-min^post4 == 0 /\ -k_1^post4+k_1^0 == 0 /\ 1-destflag^0 <= 0 /\ -edgecount^post4+edgecount^0 == 0 /\ i^0-i^post4 == 0 /\ k^0-k^post4 == 0 /\ nodecount^0-nodecount^post4 == 0 /\ h^0-h^post4 == 0 /\ j^0-j^post4 == 0 /\ -__lengthofvisited^post4+__lengthofvisited^0 == 0), cost: 1
New rule:
l8 -> l6 : -1+destflag^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l8 -> l6 : i^0'=i^post5, destflag^0'=destflag^post5, nodecount^0'=nodecount^post5, k^0'=k^post5, h^0'=h^post5, __lengthofvisited^0'=__lengthofvisited^post5, min^0'=min^post5, j^0'=j^post5, edgecount^0'=edgecount^post5, sourceflag^0'=sourceflag^post5, k_1^0'=k_1^post5, (-j^post5+j^0 == 0 /\ -edgecount^post5+edgecount^0 == 0 /\ 1+destflag^0 <= 0 /\ -sourceflag^post5+sourceflag^0 == 0 /\ -k_1^post5+k_1^0 == 0 /\ -k^post5+k^0 == 0 /\ h^0-h^post5 == 0 /\ -min^post5+min^0 == 0 /\ i^0-i^post5 == 0 /\ destflag^0-destflag^post5 == 0 /\ __lengthofvisited^0-__lengthofvisited^post5 == 0 /\ nodecount^0-nodecount^post5 == 0), cost: 1
New rule:
l8 -> l6 : 1+destflag^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l8 -> l6 : i^0'=i^post6, destflag^0'=destflag^post6, nodecount^0'=nodecount^post6, k^0'=k^post6, h^0'=h^post6, __lengthofvisited^0'=__lengthofvisited^post6, min^0'=min^post6, j^0'=j^post6, edgecount^0'=edgecount^post6, sourceflag^0'=sourceflag^post6, k_1^0'=k_1^post6, (-h^post6+h^0 == 0 /\ -__lengthofvisited^post6+__lengthofvisited^0 == 0 /\ destflag^0 <= 0 /\ i^0-i^post6 == 0 /\ k^0-k^post6 == 0 /\ -sourceflag^post6+sourceflag^0 == 0 /\ -k_1^post6+k_1^0 == 0 /\ -destflag^0 <= 0 /\ -min^post6+min^0 == 0 /\ destflag^0-destflag^post6 == 0 /\ j^0-j^post6 == 0 /\ -edgecount^post6+edgecount^0 == 0 /\ nodecount^0-nodecount^post6 == 0), cost: 1
New rule:
l8 -> l6 : destflag^0 == 0, cost: 1

Applied preprocessing
Original rule:
l9 -> l6 : i^0'=i^post7, destflag^0'=destflag^post7, nodecount^0'=nodecount^post7, k^0'=k^post7, h^0'=h^post7, __lengthofvisited^0'=__lengthofvisited^post7, min^0'=min^post7, j^0'=j^post7, edgecount^0'=edgecount^post7, sourceflag^0'=sourceflag^post7, k_1^0'=k_1^post7, (-edgecount^post7+edgecount^0 == 0 /\ -k^post7+k^0 == 0 /\ -k_1^post7+k_1^0 == 0 /\ 1-sourceflag^0 <= 0 /\ -__lengthofvisited^post7+__lengthofvisited^0 == 0 /\ min^0-min^post7 == 0 /\ h^0-h^post7 == 0 /\ destflag^0-destflag^post7 == 0 /\ i^0-i^post7 == 0 /\ nodecount^0-nodecount^post7 == 0 /\ -sourceflag^post7+sourceflag^0 == 0 /\ -j^post7+j^0 == 0), cost: 1
New rule:
l9 -> l6 : -1+sourceflag^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l9 -> l6 : i^0'=i^post8, destflag^0'=destflag^post8, nodecount^0'=nodecount^post8, k^0'=k^post8, h^0'=h^post8, __lengthofvisited^0'=__lengthofvisited^post8, min^0'=min^post8, j^0'=j^post8, edgecount^0'=edgecount^post8, sourceflag^0'=sourceflag^post8, k_1^0'=k_1^post8, (edgecount^0-edgecount^post8 == 0 /\ -sourceflag^post8+sourceflag^0 == 0 /\ destflag^0-destflag^post8 == 0 /\ __lengthofvisited^0-__lengthofvisited^post8 == 0 /\ -min^post8+min^0 == 0 /\ -j^post8+j^0 == 0 /\ nodecount^0-nodecount^post8 == 0 /\ 1+sourceflag^0 <= 0 /\ h^0-h^post8 == 0 /\ -k_1^post8+k_1^0 == 0 /\ i^0-i^post8 == 0 /\ -k^post8+k^0 == 0), cost: 1
New rule:
l9 -> l6 : 1+sourceflag^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l9 -> l8 : i^0'=i^post9, destflag^0'=destflag^post9, nodecount^0'=nodecount^post9, k^0'=k^post9, h^0'=h^post9, __lengthofvisited^0'=__lengthofvisited^post9, min^0'=min^post9, j^0'=j^post9, edgecount^0'=edgecount^post9, sourceflag^0'=sourceflag^post9, k_1^0'=k_1^post9, (-sourceflag^post9+sourceflag^0 == 0 /\ -h^post9+h^0 == 0 /\ -sourceflag^0 <= 0 /\ k^0-k^post9 == 0 /\ -k_1^post9+k_1^0 == 0 /\ -destflag^post9+destflag^0 == 0 /\ min^0-min^post9 == 0 /\ i^0-i^post9 == 0 /\ -edgecount^post9+edgecount^0 == 0 /\ nodecount^0-nodecount^post9 == 0 /\ sourceflag^0 <= 0 /\ j^0-j^post9 == 0 /\ -__lengthofvisited^post9+__lengthofvisited^0 == 0), cost: 1
New rule:
l9 -> l8 : sourceflag^0 == 0, cost: 1

Applied preprocessing
Original rule:
l10 -> l11 : i^0'=i^post10, destflag^0'=destflag^post10, nodecount^0'=nodecount^post10, k^0'=k^post10, h^0'=h^post10, __lengthofvisited^0'=__lengthofvisited^post10, min^0'=min^post10, j^0'=j^post10, edgecount^0'=edgecount^post10, sourceflag^0'=sourceflag^post10, k_1^0'=k_1^post10, (i^0-i^post10 == 0 /\ min^0-min^post10 == 0 /\ sourceflag^0-sourceflag^post10 == 0 /\ -nodecount^post10+nodecount^0 == 0 /\ -edgecount^post10+edgecount^0 == 0 /\ h^0-h^post10 == 0 /\ -j^post10+j^0 == 0 /\ __lengthofvisited^0-__lengthofvisited^post10 == 0 /\ -k^post10+k^0 == 0 /\ destflag^0-destflag^post10 == 0 /\ -k_1^post10+k_1^0 == 0), cost: 1
New rule:
l10 -> l11 : TRUE, cost: 1

Applied preprocessing
Original rule:
l12 -> l13 : i^0'=i^post11, destflag^0'=destflag^post11, nodecount^0'=nodecount^post11, k^0'=k^post11, h^0'=h^post11, __lengthofvisited^0'=__lengthofvisited^post11, min^0'=min^post11, j^0'=j^post11, edgecount^0'=edgecount^post11, sourceflag^0'=sourceflag^post11, k_1^0'=k_1^post11, (i^0-i^post11 == 0 /\ -h^post11+h^0 == 0 /\ nodecount^0-nodecount^post11 == 0 /\ -edgecount^post11+edgecount^0 == 0 /\ destflag^0-destflag^post11 == 0 /\ __lengthofvisited^0-__lengthofvisited^post11 == 0 /\ -sourceflag^post11+sourceflag^0 == 0 /\ -min^post11+min^0 == 0 /\ -1-j^0+j^post11 == 0 /\ -k_1^post11+k_1^0 == 0 /\ k^0-k^post11 == 0), cost: 1
New rule:
l12 -> l13 : j^0'=1+j^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l14 -> l12 : i^0'=i^post12, destflag^0'=destflag^post12, nodecount^0'=nodecount^post12, k^0'=k^post12, h^0'=h^post12, __lengthofvisited^0'=__lengthofvisited^post12, min^0'=min^post12, j^0'=j^post12, edgecount^0'=edgecount^post12, sourceflag^0'=sourceflag^post12, k_1^0'=k_1^post12, (h^0-h^post12 == 0 /\ -__lengthofvisited^post12+__lengthofvisited^0 == 0 /\ min^0-min^post12 == 0 /\ -j^post12+j^0 == 0 /\ -sourceflag^post12+sourceflag^0 == 0 /\ -k_1^post12+k_1^0 == 0 /\ -nodecount^post12+nodecount^0 == 0 /\ destflag^0-destflag^post12 == 0 /\ i^0-i^post12 == 0 /\ k^0-k^post12 == 0 /\ -edgecount^post12+edgecount^0 == 0), cost: 1
New rule:
l14 -> l12 : TRUE, cost: 1

Applied preprocessing
Original rule:
l14 -> l12 : i^0'=i^post13, destflag^0'=destflag^post13, nodecount^0'=nodecount^post13, k^0'=k^post13, h^0'=h^post13, __lengthofvisited^0'=__lengthofvisited^post13, min^0'=min^post13, j^0'=j^post13, edgecount^0'=edgecount^post13, sourceflag^0'=sourceflag^post13, k_1^0'=k_1^post13, (__lengthofvisited^0-__lengthofvisited^post13 == 0 /\ -sourceflag^post13+sourceflag^0 == 0 /\ -min^post13+min^0 == 0 /\ -k^post13+k^0 == 0 /\ -j^post13+j^0 == 0 /\ -edgecount^post13+edgecount^0 == 0 /\ destflag^post13 == 0 /\ h^0-h^post13 == 0 /\ -k_1^post13+k_1^0 == 0 /\ -i^post13+i^0 == 0 /\ nodecount^0-nodecount^post13 == 0), cost: 1
New rule:
l14 -> l12 : destflag^0'=0, TRUE, cost: 1

Applied preprocessing
Original rule:
l14 -> l12 : i^0'=i^post14, destflag^0'=destflag^post14, nodecount^0'=nodecount^post14, k^0'=k^post14, h^0'=h^post14, __lengthofvisited^0'=__lengthofvisited^post14, min^0'=min^post14, j^0'=j^post14, edgecount^0'=edgecount^post14, sourceflag^0'=sourceflag^post14, k_1^0'=k_1^post14, (-h^post14+h^0 == 0 /\ -sourceflag^post14+sourceflag^0 == 0 /\ k^0-k^post14 == 0 /\ -__lengthofvisited^post14+__lengthofvisited^0 == 0 /\ -k_1^post14+k_1^0 == 0 /\ j^0-j^post14 == 0 /\ i^0-i^post14 == 0 /\ -edgecount^post14+edgecount^0 == 0 /\ -min^post14+min^0 == 0 /\ nodecount^0-nodecount^post14 == 0 /\ destflag^0-destflag^post14 == 0), cost: 1
New rule:
l14 -> l12 : TRUE, cost: 1

Applied preprocessing
Original rule:
l15 -> l9 : i^0'=i^post15, destflag^0'=destflag^post15, nodecount^0'=nodecount^post15, k^0'=k^post15, h^0'=h^post15, __lengthofvisited^0'=__lengthofvisited^post15, min^0'=min^post15, j^0'=j^post15, edgecount^0'=edgecount^post15, sourceflag^0'=sourceflag^post15, k_1^0'=k_1^post15, (-j^post15+j^0 == 0 /\ -k_1^post15+k_1^0 == 0 /\ nodecount^0-nodecount^post15 == 0 /\ nodecount^0-j^0 <= 0 /\ -edgecount^post15+edgecount^0 == 0 /\ -sourceflag^post15+sourceflag^0 == 0 /\ i^0-i^post15 == 0 /\ -k^post15+k^0 == 0 /\ h^0-h^post15 == 0 /\ -min^post15+min^0 == 0 /\ destflag^0-destflag^post15 == 0 /\ __lengthofvisited^0-__lengthofvisited^post15 == 0), cost: 1
New rule:
l15 -> l9 : nodecount^0-j^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l15 -> l14 : i^0'=i^post16, destflag^0'=destflag^post16, nodecount^0'=nodecount^post16, k^0'=k^post16, h^0'=h^post16, __lengthofvisited^0'=__lengthofvisited^post16, min^0'=min^post16, j^0'=j^post16, edgecount^0'=edgecount^post16, sourceflag^0'=sourceflag^post16, k_1^0'=k_1^post16, (-h^post16+h^0 == 0 /\ j^0-j^post16 == 0 /\ destflag^0-destflag^post16 == 0 /\ __lengthofvisited^0-__lengthofvisited^post16 == 0 /\ -sourceflag^post16+sourceflag^0 == 0 /\ -k_1^post16+k_1^0 == 0 /\ nodecount^0-nodecount^post16 == 0 /\ 1-nodecount^0+j^0 <= 0 /\ edgecount^0-edgecount^post16 == 0 /\ -min^post16+min^0 == 0 /\ i^0-i^post16 == 0 /\ k^0-k^post16 == 0), cost: 1
New rule:
l15 -> l14 : 1-nodecount^0+j^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l16 -> l17 : i^0'=i^post17, destflag^0'=destflag^post17, nodecount^0'=nodecount^post17, k^0'=k^post17, h^0'=h^post17, __lengthofvisited^0'=__lengthofvisited^post17, min^0'=min^post17, j^0'=j^post17, edgecount^0'=edgecount^post17, sourceflag^0'=sourceflag^post17, k_1^0'=k_1^post17, (-destflag^post17+destflag^0 == 0 /\ -__lengthofvisited^post17+__lengthofvisited^0 == 0 /\ -sourceflag^post17+sourceflag^0 == 0 /\ -k_1^post17+k_1^0 == 0 /\ -1+j^post17-j^0 == 0 /\ min^0-min^post17 == 0 /\ -nodecount^post17+nodecount^0 == 0 /\ k^0-k^post17 == 0 /\ h^0-h^post17 == 0 /\ i^0-i^post17 == 0 /\ -edgecount^post17+edgecount^0 == 0), cost: 1
New rule:
l16 -> l17 : j^0'=1+j^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l7 -> l18 : i^0'=i^post18, destflag^0'=destflag^post18, nodecount^0'=nodecount^post18, k^0'=k^post18, h^0'=h^post18, __lengthofvisited^0'=__lengthofvisited^post18, min^0'=min^post18, j^0'=j^post18, edgecount^0'=edgecount^post18, sourceflag^0'=sourceflag^post18, k_1^0'=k_1^post18, (edgecount^0-edgecount^post18 == 0 /\ -k_1^post18+k_1^0 == 0 /\ -k^post18+k^0 == 0 /\ destflag^0-destflag^post18 == 0 /\ __lengthofvisited^0-__lengthofvisited^post18 == 0 /\ nodecount^0-nodecount^post18 == 0 /\ -sourceflag^post18+sourceflag^0 == 0 /\ h^0-h^post18 == 0 /\ -j^post18+j^0 == 0 /\ i^0-i^post18 == 0 /\ -min^post18+min^0 == 0), cost: 1
New rule:
l7 -> l18 : TRUE, cost: 1

Applied preprocessing
Original rule:
l19 -> l16 : i^0'=i^post19, destflag^0'=destflag^post19, nodecount^0'=nodecount^post19, k^0'=k^post19, h^0'=h^post19, __lengthofvisited^0'=__lengthofvisited^post19, min^0'=min^post19, j^0'=j^post19, edgecount^0'=edgecount^post19, sourceflag^0'=sourceflag^post19, k_1^0'=k_1^post19, (-sourceflag^post19+sourceflag^0 == 0 /\ -h^post19+h^0 == 0 /\ k^0-k^post19 == 0 /\ -edgecount^post19+edgecount^0 == 0 /\ min^0-min^post19 == 0 /\ -k_1^post19+k_1^0 == 0 /\ -destflag^post19+destflag^0 == 0 /\ i^0-i^post19 == 0 /\ nodecount^0-nodecount^post19 == 0 /\ j^0-j^post19 == 0 /\ -__lengthofvisited^post19+__lengthofvisited^0 == 0), cost: 1
New rule:
l19 -> l16 : TRUE, cost: 1

Applied preprocessing
Original rule:
l19 -> l16 : i^0'=i^post20, destflag^0'=destflag^post20, nodecount^0'=nodecount^post20, k^0'=k^post20, h^0'=h^post20, __lengthofvisited^0'=__lengthofvisited^post20, min^0'=min^post20, j^0'=j^post20, edgecount^0'=edgecount^post20, sourceflag^0'=sourceflag^post20, k_1^0'=k_1^post20, (__lengthofvisited^0-__lengthofvisited^post20 == 0 /\ -j^post20+j^0 == 0 /\ -k^post20+k^0 == 0 /\ -k_1^post20+k_1^0 == 0 /\ h^0-h^post20 == 0 /\ i^0-i^post20 == 0 /\ -edgecount^post20+edgecount^0 == 0 /\ -min^post20+min^0 == 0 /\ nodecount^0-nodecount^post20 == 0 /\ -1+sourceflag^post20 == 0 /\ destflag^0-destflag^post20 == 0), cost: 1
New rule:
l19 -> l16 : sourceflag^0'=1, TRUE, cost: 1

Applied preprocessing
Original rule:
l19 -> l16 : i^0'=i^post21, destflag^0'=destflag^post21, nodecount^0'=nodecount^post21, k^0'=k^post21, h^0'=h^post21, __lengthofvisited^0'=__lengthofvisited^post21, min^0'=min^post21, j^0'=j^post21, edgecount^0'=edgecount^post21, sourceflag^0'=sourceflag^post21, k_1^0'=k_1^post21, (-h^post21+h^0 == 0 /\ i^0-i^post21 == 0 /\ -__lengthofvisited^post21+__lengthofvisited^0 == 0 /\ nodecount^0-nodecount^post21 == 0 /\ -edgecount^post21+edgecount^0 == 0 /\ k^0-k^post21 == 0 /\ -sourceflag^post21+sourceflag^0 == 0 /\ -k_1^post21+k_1^0 == 0 /\ -min^post21+min^0 == 0 /\ j^0-j^post21 == 0 /\ destflag^0-destflag^post21 == 0), cost: 1
New rule:
l19 -> l16 : TRUE, cost: 1

Applied preprocessing
Original rule:
l20 -> l13 : i^0'=i^post22, destflag^0'=destflag^post22, nodecount^0'=nodecount^post22, k^0'=k^post22, h^0'=h^post22, __lengthofvisited^0'=__lengthofvisited^post22, min^0'=min^post22, j^0'=j^post22, edgecount^0'=edgecount^post22, sourceflag^0'=sourceflag^post22, k_1^0'=k_1^post22, (nodecount^0-j^0 <= 0 /\ j^post22 == 0 /\ -__lengthofvisited^post22+__lengthofvisited^0 == 0 /\ h^0-h^post22 == 0 /\ min^0-min^post22 == 0 /\ -sourceflag^post22+sourceflag^0 == 0 /\ -k_1^post22+k_1^0 == 0 /\ -1+destflag^post22 == 0 /\ -nodecount^post22+nodecount^0 == 0 /\ i^0-i^post22 == 0 /\ k^0-k^post22 == 0 /\ -edgecount^post22+edgecount^0 == 0), cost: 1
New rule:
l20 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l20 -> l19 : i^0'=i^post23, destflag^0'=destflag^post23, nodecount^0'=nodecount^post23, k^0'=k^post23, h^0'=h^post23, __lengthofvisited^0'=__lengthofvisited^post23, min^0'=min^post23, j^0'=j^post23, edgecount^0'=edgecount^post23, sourceflag^0'=sourceflag^post23, k_1^0'=k_1^post23, (-sourceflag^post23+sourceflag^0 == 0 /\ j^0-j^post23 == 0 /\ __lengthofvisited^0-__lengthofvisited^post23 == 0 /\ -k_1^post23+k_1^0 == 0 /\ -k^post23+k^0 == 0 /\ 1-nodecount^0+j^0 <= 0 /\ nodecount^0-nodecount^post23 == 0 /\ destflag^0-destflag^post23 == 0 /\ edgecount^0-edgecount^post23 == 0 /\ -min^post23+min^0 == 0 /\ h^0-h^post23 == 0 /\ i^0-i^post23 == 0), cost: 1
New rule:
l20 -> l19 : 1-nodecount^0+j^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l21 -> l22 : i^0'=i^post24, destflag^0'=destflag^post24, nodecount^0'=nodecount^post24, k^0'=k^post24, h^0'=h^post24, __lengthofvisited^0'=__lengthofvisited^post24, min^0'=min^post24, j^0'=j^post24, edgecount^0'=edgecount^post24, sourceflag^0'=sourceflag^post24, k_1^0'=k_1^post24, (-k_1^post24+k_1^0 == 0 /\ -destflag^post24+destflag^0 == 0 /\ -__lengthofvisited^post24+__lengthofvisited^0 == 0 /\ -1-h^0+h^post24 == 0 /\ min^0-min^post24 == 0 /\ -edgecount^post24+edgecount^0 == 0 /\ i^0-i^post24 == 0 /\ k^0-k^post24 == 0 /\ -sourceflag^post24+sourceflag^0 == 0 /\ nodecount^0-nodecount^post24 == 0 /\ -j^post24+j^0 == 0), cost: 1
New rule:
l21 -> l22 : h^0'=1+h^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l23 -> l21 : i^0'=i^post25, destflag^0'=destflag^post25, nodecount^0'=nodecount^post25, k^0'=k^post25, h^0'=h^post25, __lengthofvisited^0'=__lengthofvisited^post25, min^0'=min^post25, j^0'=j^post25, edgecount^0'=edgecount^post25, sourceflag^0'=sourceflag^post25, k_1^0'=k_1^post25, (-k_1^post25+k_1^0 == 0 /\ min^post25-h^0 == 0 /\ sourceflag^0-sourceflag^post25 == 0 /\ -edgecount^post25+edgecount^0 == 0 /\ -nodecount^post25+nodecount^0 == 0 /\ i^0-i^post25 == 0 /\ -k^post25+k^0 == 0 /\ h^0-h^post25 == 0 /\ destflag^0-destflag^post25 == 0 /\ __lengthofvisited^0-__lengthofvisited^post25 == 0 /\ -j^post25+j^0 == 0), cost: 1
New rule:
l23 -> l21 : min^0'=h^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l23 -> l21 : i^0'=i^post26, destflag^0'=destflag^post26, nodecount^0'=nodecount^post26, k^0'=k^post26, h^0'=h^post26, __lengthofvisited^0'=__lengthofvisited^post26, min^0'=min^post26, j^0'=j^post26, edgecount^0'=edgecount^post26, sourceflag^0'=sourceflag^post26, k_1^0'=k_1^post26, (-k_1^post26+k_1^0 == 0 /\ nodecount^0-nodecount^post26 == 0 /\ k^0-k^post26 == 0 /\ -__lengthofvisited^post26+__lengthofvisited^0 == 0 /\ -h^post26+h^0 == 0 /\ -edgecount^post26+edgecount^0 == 0 /\ -sourceflag^post26+sourceflag^0 == 0 /\ i^0-i^post26 == 0 /\ destflag^0-destflag^post26 == 0 /\ -min^post26+min^0 == 0 /\ j^0-j^post26 == 0), cost: 1
New rule:
l23 -> l21 : TRUE, cost: 1

Applied preprocessing
Original rule:
l22 -> l24 : i^0'=i^post27, destflag^0'=destflag^post27, nodecount^0'=nodecount^post27, k^0'=k^post27, h^0'=h^post27, __lengthofvisited^0'=__lengthofvisited^post27, min^0'=min^post27, j^0'=j^post27, edgecount^0'=edgecount^post27, sourceflag^0'=sourceflag^post27, k_1^0'=k_1^post27, (min^0-min^post27 == 0 /\ -k^post27+k^0 == 0 /\ sourceflag^0-sourceflag^post27 == 0 /\ -k_1^post27+k_1^0 == 0 /\ h^0-h^post27 == 0 /\ destflag^0-destflag^post27 == 0 /\ __lengthofvisited^0-__lengthofvisited^post27 == 0 /\ -j^post27+j^0 == 0 /\ -nodecount^post27+nodecount^0 == 0 /\ i^0-i^post27 == 0 /\ -edgecount^post27+edgecount^0 == 0), cost: 1
New rule:
l22 -> l24 : TRUE, cost: 1

Applied preprocessing
Original rule:
l24 -> l17 : i^0'=i^post28, destflag^0'=destflag^post28, nodecount^0'=nodecount^post28, k^0'=k^post28, h^0'=h^post28, __lengthofvisited^0'=__lengthofvisited^post28, min^0'=min^post28, j^0'=j^post28, edgecount^0'=edgecount^post28, sourceflag^0'=sourceflag^post28, k_1^0'=k_1^post28, (sourceflag^post28 == 0 /\ edgecount^0-edgecount^post28 == 0 /\ -k^post28+k^0 == 0 /\ destflag^0-destflag^post28 == 0 /\ __lengthofvisited^0-__lengthofvisited^post28 == 0 /\ j^post28 == 0 /\ i^0-i^post28 == 0 /\ nodecount^0-nodecount^post28 == 0 /\ h^0-h^post28 == 0 /\ -k_1^post28+k_1^0 == 0 /\ -min^post28+min^0 == 0 /\ -h^0+edgecount^0 <= 0), cost: 1
New rule:
l24 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l24 -> l23 : i^0'=i^post29, destflag^0'=destflag^post29, nodecount^0'=nodecount^post29, k^0'=k^post29, h^0'=h^post29, __lengthofvisited^0'=__lengthofvisited^post29, min^0'=min^post29, j^0'=j^post29, edgecount^0'=edgecount^post29, sourceflag^0'=sourceflag^post29, k_1^0'=k_1^post29, (-destflag^post29+destflag^0 == 0 /\ -edgecount^post29+edgecount^0 == 0 /\ -k_1^post29+k_1^0 == 0 /\ -__lengthofvisited^post29+__lengthofvisited^0 == 0 /\ k^0-k^post29 == 0 /\ min^0-min^post29 == 0 /\ i^0-i^post29 == 0 /\ 1+h^0-edgecount^0 <= 0 /\ nodecount^0-nodecount^post29 == 0 /\ -sourceflag^post29+sourceflag^0 == 0 /\ h^0-h^post29 == 0 /\ -j^post29+j^0 == 0), cost: 1
New rule:
l24 -> l23 : 1+h^0-edgecount^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l18 -> l4 : i^0'=i^post30, destflag^0'=destflag^post30, nodecount^0'=nodecount^post30, k^0'=k^post30, h^0'=h^post30, __lengthofvisited^0'=__lengthofvisited^post30, min^0'=min^post30, j^0'=j^post30, edgecount^0'=edgecount^post30, sourceflag^0'=sourceflag^post30, k_1^0'=k_1^post30, (sourceflag^0-sourceflag^post30 == 0 /\ destflag^0-destflag^post30 == 0 /\ __lengthofvisited^0-__lengthofvisited^post30 == 0 /\ i^0-i^post30 == 0 /\ -min^post30+min^0 == 0 /\ edgecount^0-k_1^0 <= 0 /\ -j^post30+j^0 == 0 /\ -1+k^post30-k^0 == 0 /\ -k_1^post30+k_1^0 == 0 /\ h^0-h^post30 == 0 /\ -edgecount^post30+edgecount^0 == 0 /\ -nodecount^post30+nodecount^0 == 0), cost: 1
New rule:
l18 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l18 -> l22 : i^0'=i^post31, destflag^0'=destflag^post31, nodecount^0'=nodecount^post31, k^0'=k^post31, h^0'=h^post31, __lengthofvisited^0'=__lengthofvisited^post31, min^0'=min^post31, j^0'=j^post31, edgecount^0'=edgecount^post31, sourceflag^0'=sourceflag^post31, k_1^0'=k_1^post31, (1-edgecount^0+k_1^0 <= 0 /\ h^post31 == 0 /\ destflag^0-destflag^post31 == 0 /\ j^0-j^post31 == 0 /\ __lengthofvisited^0-__lengthofvisited^post31 == 0 /\ edgecount^0-edgecount^post31 == 0 /\ -sourceflag^post31+sourceflag^0 == 0 /\ nodecount^0-nodecount^post31 == 0 /\ -k_1^post31+k_1^0 == 0 /\ -min^post31+min^0 == 0 /\ i^0-i^post31 == 0 /\ k^0-k^post31 == 0), cost: 1
New rule:
l18 -> l22 : h^0'=0, 1-edgecount^0+k_1^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l11 -> l7 : i^0'=i^post32, destflag^0'=destflag^post32, nodecount^0'=nodecount^post32, k^0'=k^post32, h^0'=h^post32, __lengthofvisited^0'=__lengthofvisited^post32, min^0'=min^post32, j^0'=j^post32, edgecount^0'=edgecount^post32, sourceflag^0'=sourceflag^post32, k_1^0'=k_1^post32, (k_1^post32 == 0 /\ -j^post32+j^0 == 0 /\ -__lengthofvisited^post32+__lengthofvisited^0 == 0 /\ h^0-h^post32 == 0 /\ min^0-min^post32 == 0 /\ destflag^0-destflag^post32 == 0 /\ -sourceflag^post32+sourceflag^0 == 0 /\ -i^0+edgecount^0 <= 0 /\ -nodecount^post32+nodecount^0 == 0 /\ i^0-i^post32 == 0 /\ -edgecount^post32+edgecount^0 == 0 /\ k^0-k^post32 == 0), cost: 1
New rule:
l11 -> l7 : k_1^0'=0, -i^0+edgecount^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l11 -> l10 : i^0'=i^post33, destflag^0'=destflag^post33, nodecount^0'=nodecount^post33, k^0'=k^post33, h^0'=h^post33, __lengthofvisited^0'=__lengthofvisited^post33, min^0'=min^post33, j^0'=j^post33, edgecount^0'=edgecount^post33, sourceflag^0'=sourceflag^post33, k_1^0'=k_1^post33, (1+i^0-edgecount^0 <= 0 /\ __lengthofvisited^0-__lengthofvisited^post33 == 0 /\ -sourceflag^post33+sourceflag^0 == 0 /\ -1+i^post33-i^0 == 0 /\ -k^post33+k^0 == 0 /\ destflag^0-destflag^post33 == 0 /\ -edgecount^post33+edgecount^0 == 0 /\ -k_1^post33+k_1^0 == 0 /\ h^0-h^post33 == 0 /\ -j^post33+j^0 == 0 /\ nodecount^0-nodecount^post33 == 0 /\ -min^post33+min^0 == 0), cost: 1
New rule:
l11 -> l10 : i^0'=1+i^0, 1+i^0-edgecount^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l17 -> l20 : i^0'=i^post34, destflag^0'=destflag^post34, nodecount^0'=nodecount^post34, k^0'=k^post34, h^0'=h^post34, __lengthofvisited^0'=__lengthofvisited^post34, min^0'=min^post34, j^0'=j^post34, edgecount^0'=edgecount^post34, sourceflag^0'=sourceflag^post34, k_1^0'=k_1^post34, (-edgecount^post34+edgecount^0 == 0 /\ -k_1^post34+k_1^0 == 0 /\ k^0-k^post34 == 0 /\ i^0-i^post34 == 0 /\ -__lengthofvisited^post34+__lengthofvisited^0 == 0 /\ -sourceflag^post34+sourceflag^0 == 0 /\ j^0-j^post34 == 0 /\ -min^post34+min^0 == 0 /\ nodecount^0-nodecount^post34 == 0 /\ -h^post34+h^0 == 0 /\ destflag^0-destflag^post34 == 0), cost: 1
New rule:
l17 -> l20 : TRUE, cost: 1

Applied preprocessing
Original rule:
l25 -> l10 : i^0'=i^post35, destflag^0'=destflag^post35, nodecount^0'=nodecount^post35, k^0'=k^post35, h^0'=h^post35, __lengthofvisited^0'=__lengthofvisited^post35, min^0'=min^post35, j^0'=j^post35, edgecount^0'=edgecount^post35, sourceflag^0'=sourceflag^post35, k_1^0'=k_1^post35, (min^post35 == 0 /\ -k_1^post35+k_1^0 == 0 /\ sourceflag^0-sourceflag^post35 == 0 /\ -edgecount^post35+edgecount^0 == 0 /\ -nodecount^post35+nodecount^0 == 0 /\ h^0-h^post35 == 0 /\ -k^post35+k^0 == 0 /\ destflag^0-destflag^post35 == 0 /\ __lengthofvisited^0-__lengthofvisited^post35 == 0 /\ i^post35 == 0 /\ -j^post35+j^0 == 0), cost: 1
New rule:
l25 -> l10 : i^0'=0, min^0'=0, TRUE, cost: 1

Applied preprocessing
Original rule:
l5 -> l25 : i^0'=i^post37, destflag^0'=destflag^post37, nodecount^0'=nodecount^post37, k^0'=k^post37, h^0'=h^post37, __lengthofvisited^0'=__lengthofvisited^post37, min^0'=min^post37, j^0'=j^post37, edgecount^0'=edgecount^post37, sourceflag^0'=sourceflag^post37, k_1^0'=k_1^post37, (-destflag^post37+destflag^0 == 0 /\ -edgecount^post37+edgecount^0 == 0 /\ min^0-min^post37 == 0 /\ -nodecount^post37+nodecount^0 == 0 /\ k^0-k^post37 == 0 /\ -__lengthofvisited^post37+__lengthofvisited^0 == 0 /\ nodecount^0-k^0 <= 0 /\ -j^post37+j^0 == 0 /\ i^0-i^post37 == 0 /\ -k_1^post37+k_1^0 == 0 /\ -sourceflag^post37+sourceflag^0 == 0 /\ h^0-h^post37 == 0), cost: 1
New rule:
l5 -> l25 : nodecount^0-k^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l5 -> l25 : i^0'=i^post38, destflag^0'=destflag^post38, nodecount^0'=nodecount^post38, k^0'=k^post38, h^0'=h^post38, __lengthofvisited^0'=__lengthofvisited^post38, min^0'=min^post38, j^0'=j^post38, edgecount^0'=edgecount^post38, sourceflag^0'=sourceflag^post38, k_1^0'=k_1^post38, (__lengthofvisited^0-__lengthofvisited^post38 == 0 /\ edgecount^0-edgecount^post38 == 0 /\ -k^post38+k^0 == 0 /\ destflag^0-destflag^post38 == 0 /\ 2-nodecount^0+k^0 <= 0 /\ i^0-i^post38 == 0 /\ nodecount^0-nodecount^post38 == 0 /\ h^0-h^post38 == 0 /\ -j^post38+j^0 == 0 /\ -sourceflag^post38+sourceflag^0 == 0 /\ -k_1^post38+k_1^0 == 0 /\ -min^post38+min^0 == 0), cost: 1
New rule:
l5 -> l25 : 2-nodecount^0+k^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l3 -> l4 : i^0'=i^post39, destflag^0'=destflag^post39, nodecount^0'=nodecount^post39, k^0'=k^post39, h^0'=h^post39, __lengthofvisited^0'=__lengthofvisited^post39, min^0'=min^post39, j^0'=j^post39, edgecount^0'=edgecount^post39, sourceflag^0'=sourceflag^post39, k_1^0'=k_1^post39, (nodecount^0-nodecount^post39 == 0 /\ -edgecount^post39+edgecount^0 == 0 /\ -k_1^post39+k_1^0 == 0 /\ -1-i^0+nodecount^0 <= 0 /\ i^0-i^post39 == 0 /\ -h^post39+h^0 == 0 /\ -__lengthofvisited^post39+__lengthofvisited^0 == 0 /\ -sourceflag^post39+sourceflag^0 == 0 /\ j^0-j^post39 == 0 /\ k^post39 == 0 /\ -destflag^post39+destflag^0 == 0 /\ -min^post39+min^0 == 0), cost: 1
New rule:
l3 -> l4 : k^0'=0, -1-i^0+nodecount^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l3 -> l2 : i^0'=i^post40, destflag^0'=destflag^post40, nodecount^0'=nodecount^post40, k^0'=k^post40, h^0'=h^post40, __lengthofvisited^0'=__lengthofvisited^post40, min^0'=min^post40, j^0'=j^post40, edgecount^0'=edgecount^post40, sourceflag^0'=sourceflag^post40, k_1^0'=k_1^post40, (-k^post40+k^0 == 0 /\ min^0-min^post40 == 0 /\ -edgecount^post40+edgecount^0 == 0 /\ sourceflag^0-sourceflag^post40 == 0 /\ h^0-h^post40 == 0 /\ -nodecount^post40+nodecount^0 == 0 /\ -j^post40+j^0 == 0 /\ -k_1^post40+k_1^0 == 0 /\ destflag^0-destflag^post40 == 0 /\ __lengthofvisited^0-__lengthofvisited^post40 == 0 /\ 2+i^0-nodecount^0 <= 0 /\ -1-i^0+i^post40 == 0), cost: 1
New rule:
l3 -> l2 : i^0'=1+i^0, 2+i^0-nodecount^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l13 -> l15 : i^0'=i^post41, destflag^0'=destflag^post41, nodecount^0'=nodecount^post41, k^0'=k^post41, h^0'=h^post41, __lengthofvisited^0'=__lengthofvisited^post41, min^0'=min^post41, j^0'=j^post41, edgecount^0'=edgecount^post41, sourceflag^0'=sourceflag^post41, k_1^0'=k_1^post41, (k^0-k^post41 == 0 /\ -min^post41+min^0 == 0 /\ i^0-i^post41 == 0 /\ nodecount^0-nodecount^post41 == 0 /\ edgecount^0-edgecount^post41 == 0 /\ -h^post41+h^0 == 0 /\ -__lengthofvisited^post41+__lengthofvisited^0 == 0 /\ j^0-j^post41 == 0 /\ destflag^0-destflag^post41 == 0 /\ -sourceflag^post41+sourceflag^0 == 0 /\ -k_1^post41+k_1^0 == 0), cost: 1
New rule:
l13 -> l15 : TRUE, cost: 1

Applied preprocessing
Original rule:
l1 -> l2 : i^0'=i^post42, destflag^0'=destflag^post42, nodecount^0'=nodecount^post42, k^0'=k^post42, h^0'=h^post42, __lengthofvisited^0'=__lengthofvisited^post42, min^0'=min^post42, j^0'=j^post42, edgecount^0'=edgecount^post42, sourceflag^0'=sourceflag^post42, k_1^0'=k_1^post42, (-__lengthofvisited^post42+__lengthofvisited^0 == 0 /\ -j^post42+j^0 == 0 /\ h^0-h^post42 == 0 /\ min^0-min^post42 == 0 /\ destflag^0-destflag^post42 == 0 /\ -k_1^post42+k_1^0 == 0 /\ -sourceflag^post42+sourceflag^0 == 0 /\ -i^0+nodecount^0 <= 0 /\ i^post42 == 0 /\ -nodecount^post42+nodecount^0 == 0 /\ -edgecount^post42+edgecount^0 == 0 /\ k^0-k^post42 == 0), cost: 1
New rule:
l1 -> l2 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l0 : i^0'=i^post43, destflag^0'=destflag^post43, nodecount^0'=nodecount^post43, k^0'=k^post43, h^0'=h^post43, __lengthofvisited^0'=__lengthofvisited^post43, min^0'=min^post43, j^0'=j^post43, edgecount^0'=edgecount^post43, sourceflag^0'=sourceflag^post43, k_1^0'=k_1^post43, (__lengthofvisited^0-__lengthofvisited^post43 == 0 /\ -min^post43+min^0 == 0 /\ -k^post43+k^0 == 0 /\ -k_1^post43+k_1^0 == 0 /\ -1-i^0+i^post43 == 0 /\ nodecount^0-nodecount^post43 == 0 /\ edgecount^0-edgecount^post43 == 0 /\ destflag^0-destflag^post43 == 0 /\ -j^post43+j^0 == 0 /\ h^0-h^post43 == 0 /\ -sourceflag^post43+sourceflag^0 == 0 /\ 1+i^0-nodecount^0 <= 0), cost: 1
New rule:
l1 -> l0 : i^0'=1+i^0, 1+i^0-nodecount^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l27 -> l0 : i^0'=i^post44, destflag^0'=destflag^post44, nodecount^0'=nodecount^post44, k^0'=k^post44, h^0'=h^post44, __lengthofvisited^0'=__lengthofvisited^post44, min^0'=min^post44, j^0'=j^post44, edgecount^0'=edgecount^post44, sourceflag^0'=sourceflag^post44, k_1^0'=k_1^post44, (-destflag^post44+destflag^0 == 0 /\ -edgecount^post44+edgecount^0 == 0 /\ min^0-min^post44 == 0 /\ __lengthofvisited^post44-edgecount^0 == 0 /\ k^0-k^post44 == 0 /\ nodecount^0-nodecount^post44 == 0 /\ -k_1^post44+k_1^0 == 0 /\ h^0-h^post44 == 0 /\ -1+i^post44 == 0 /\ -sourceflag^post44+sourceflag^0 == 0 /\ -j^post44+j^0 == 0), cost: 1
New rule:
l27 -> l0 : i^0'=1, __lengthofvisited^0'=edgecount^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l28 -> l27 : i^0'=i^post45, destflag^0'=destflag^post45, nodecount^0'=nodecount^post45, k^0'=k^post45, h^0'=h^post45, __lengthofvisited^0'=__lengthofvisited^post45, min^0'=min^post45, j^0'=j^post45, edgecount^0'=edgecount^post45, sourceflag^0'=sourceflag^post45, k_1^0'=k_1^post45, (-edgecount^post45+edgecount^0 == 0 /\ sourceflag^0-sourceflag^post45 == 0 /\ -k_1^post45+k_1^0 == 0 /\ h^0-h^post45 == 0 /\ -nodecount^post45+nodecount^0 == 0 /\ i^0-i^post45 == 0 /\ -min^post45+min^0 == 0 /\ -j^post45+j^0 == 0 /\ -k^post45+k^0 == 0 /\ destflag^0-destflag^post45 == 0 /\ __lengthofvisited^0-__lengthofvisited^post45 == 0), cost: 1
New rule:
l28 -> l27 : TRUE, cost: 1

Simplified rules
Start location: l28
  46: l0 -> l1 : TRUE, cost: 1
  85: l1 -> l2 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1
  86: l1 -> l0 : i^0'=1+i^0, 1+i^0-nodecount^0 <= 0, cost: 1
  47: l2 -> l3 : TRUE, cost: 1
  82: l3 -> l4 : k^0'=0, -1-i^0+nodecount^0 <= 0, cost: 1
  83: l3 -> l2 : i^0'=1+i^0, 2+i^0-nodecount^0 <= 0, cost: 1
  48: l4 -> l5 : TRUE, cost: 1
  80: l5 -> l25 : nodecount^0-k^0 <= 0, cost: 1
  81: l5 -> l25 : 2-nodecount^0+k^0 <= 0, cost: 1
  49: l6 -> l7 : k_1^0'=1+k_1^0, TRUE, cost: 1
  63: l7 -> l18 : TRUE, cost: 1
  50: l8 -> l6 : -1+destflag^0 >= 0, cost: 1
  51: l8 -> l6 : 1+destflag^0 <= 0, cost: 1
  52: l8 -> l6 : destflag^0 == 0, cost: 1
  53: l9 -> l6 : -1+sourceflag^0 >= 0, cost: 1
  54: l9 -> l6 : 1+sourceflag^0 <= 0, cost: 1
  55: l9 -> l8 : sourceflag^0 == 0, cost: 1
  56: l10 -> l11 : TRUE, cost: 1
  76: l11 -> l7 : k_1^0'=0, -i^0+edgecount^0 <= 0, cost: 1
  77: l11 -> l10 : i^0'=1+i^0, 1+i^0-edgecount^0 <= 0, cost: 1
  57: l12 -> l13 : j^0'=1+j^0, TRUE, cost: 1
  84: l13 -> l15 : TRUE, cost: 1
  58: l14 -> l12 : TRUE, cost: 1
  59: l14 -> l12 : destflag^0'=0, TRUE, cost: 1
  60: l15 -> l9 : nodecount^0-j^0 <= 0, cost: 1
  61: l15 -> l14 : 1-nodecount^0+j^0 <= 0, cost: 1
  62: l16 -> l17 : j^0'=1+j^0, TRUE, cost: 1
  78: l17 -> l20 : TRUE, cost: 1
  74: l18 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 1
  75: l18 -> l22 : h^0'=0, 1-edgecount^0+k_1^0 <= 0, cost: 1
  64: l19 -> l16 : TRUE, cost: 1
  65: l19 -> l16 : sourceflag^0'=1, TRUE, cost: 1
  66: l20 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 1
  67: l20 -> l19 : 1-nodecount^0+j^0 <= 0, cost: 1
  68: l21 -> l22 : h^0'=1+h^0, TRUE, cost: 1
  71: l22 -> l24 : TRUE, cost: 1
  69: l23 -> l21 : min^0'=h^0, TRUE, cost: 1
  70: l23 -> l21 : TRUE, cost: 1
  72: l24 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 1
  73: l24 -> l23 : 1+h^0-edgecount^0 <= 0, cost: 1
  79: l25 -> l10 : i^0'=0, min^0'=0, TRUE, cost: 1
  87: l27 -> l0 : i^0'=1, __lengthofvisited^0'=edgecount^0, TRUE, cost: 1
  88: l28 -> l27 : TRUE, cost: 1


Eliminating location l27 by chaining:

Applied chaining
First rule:
l28 -> l27 : TRUE, cost: 1
Second rule:
l27 -> l0 : i^0'=1, __lengthofvisited^0'=edgecount^0, TRUE, cost: 1
New rule:
l28 -> l0 : i^0'=1, __lengthofvisited^0'=edgecount^0, TRUE, cost: 2

Applied deletion
Removed the following rules: 87 88

Eliminated locations on linear paths
Start location: l28
  46: l0 -> l1 : TRUE, cost: 1
  85: l1 -> l2 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1
  86: l1 -> l0 : i^0'=1+i^0, 1+i^0-nodecount^0 <= 0, cost: 1
  47: l2 -> l3 : TRUE, cost: 1
  82: l3 -> l4 : k^0'=0, -1-i^0+nodecount^0 <= 0, cost: 1
  83: l3 -> l2 : i^0'=1+i^0, 2+i^0-nodecount^0 <= 0, cost: 1
  48: l4 -> l5 : TRUE, cost: 1
  80: l5 -> l25 : nodecount^0-k^0 <= 0, cost: 1
  81: l5 -> l25 : 2-nodecount^0+k^0 <= 0, cost: 1
  49: l6 -> l7 : k_1^0'=1+k_1^0, TRUE, cost: 1
  63: l7 -> l18 : TRUE, cost: 1
  50: l8 -> l6 : -1+destflag^0 >= 0, cost: 1
  51: l8 -> l6 : 1+destflag^0 <= 0, cost: 1
  52: l8 -> l6 : destflag^0 == 0, cost: 1
  53: l9 -> l6 : -1+sourceflag^0 >= 0, cost: 1
  54: l9 -> l6 : 1+sourceflag^0 <= 0, cost: 1
  55: l9 -> l8 : sourceflag^0 == 0, cost: 1
  56: l10 -> l11 : TRUE, cost: 1
  76: l11 -> l7 : k_1^0'=0, -i^0+edgecount^0 <= 0, cost: 1
  77: l11 -> l10 : i^0'=1+i^0, 1+i^0-edgecount^0 <= 0, cost: 1
  57: l12 -> l13 : j^0'=1+j^0, TRUE, cost: 1
  84: l13 -> l15 : TRUE, cost: 1
  58: l14 -> l12 : TRUE, cost: 1
  59: l14 -> l12 : destflag^0'=0, TRUE, cost: 1
  60: l15 -> l9 : nodecount^0-j^0 <= 0, cost: 1
  61: l15 -> l14 : 1-nodecount^0+j^0 <= 0, cost: 1
  62: l16 -> l17 : j^0'=1+j^0, TRUE, cost: 1
  78: l17 -> l20 : TRUE, cost: 1
  74: l18 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 1
  75: l18 -> l22 : h^0'=0, 1-edgecount^0+k_1^0 <= 0, cost: 1
  64: l19 -> l16 : TRUE, cost: 1
  65: l19 -> l16 : sourceflag^0'=1, TRUE, cost: 1
  66: l20 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 1
  67: l20 -> l19 : 1-nodecount^0+j^0 <= 0, cost: 1
  68: l21 -> l22 : h^0'=1+h^0, TRUE, cost: 1
  71: l22 -> l24 : TRUE, cost: 1
  69: l23 -> l21 : min^0'=h^0, TRUE, cost: 1
  70: l23 -> l21 : TRUE, cost: 1
  72: l24 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 1
  73: l24 -> l23 : 1+h^0-edgecount^0 <= 0, cost: 1
  79: l25 -> l10 : i^0'=0, min^0'=0, TRUE, cost: 1
  89: l28 -> l0 : i^0'=1, __lengthofvisited^0'=edgecount^0, TRUE, cost: 2


Eliminating location l1 by chaining:

Applied chaining
First rule:
l0 -> l1 : TRUE, cost: 1
Second rule:
l1 -> l2 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 1
New rule:
l0 -> l2 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 2

Applied chaining
First rule:
l0 -> l1 : TRUE, cost: 1
Second rule:
l1 -> l0 : i^0'=1+i^0, 1+i^0-nodecount^0 <= 0, cost: 1
New rule:
l0 -> l0 : i^0'=1+i^0, 1+i^0-nodecount^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 46 85 86

Eliminating location l3 by chaining:

Applied chaining
First rule:
l2 -> l3 : TRUE, cost: 1
Second rule:
l3 -> l4 : k^0'=0, -1-i^0+nodecount^0 <= 0, cost: 1
New rule:
l2 -> l4 : k^0'=0, -1-i^0+nodecount^0 <= 0, cost: 2

Applied chaining
First rule:
l2 -> l3 : TRUE, cost: 1
Second rule:
l3 -> l2 : i^0'=1+i^0, 2+i^0-nodecount^0 <= 0, cost: 1
New rule:
l2 -> l2 : i^0'=1+i^0, 2+i^0-nodecount^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 47 82 83

Eliminating location l5 by chaining:

Applied chaining
First rule:
l4 -> l5 : TRUE, cost: 1
Second rule:
l5 -> l25 : nodecount^0-k^0 <= 0, cost: 1
New rule:
l4 -> l25 : nodecount^0-k^0 <= 0, cost: 2

Applied chaining
First rule:
l4 -> l5 : TRUE, cost: 1
Second rule:
l5 -> l25 : 2-nodecount^0+k^0 <= 0, cost: 1
New rule:
l4 -> l25 : 2-nodecount^0+k^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 48 80 81

Eliminating location l11 by chaining:

Applied chaining
First rule:
l10 -> l11 : TRUE, cost: 1
Second rule:
l11 -> l7 : k_1^0'=0, -i^0+edgecount^0 <= 0, cost: 1
New rule:
l10 -> l7 : k_1^0'=0, -i^0+edgecount^0 <= 0, cost: 2

Applied chaining
First rule:
l10 -> l11 : TRUE, cost: 1
Second rule:
l11 -> l10 : i^0'=1+i^0, 1+i^0-edgecount^0 <= 0, cost: 1
New rule:
l10 -> l10 : i^0'=1+i^0, 1+i^0-edgecount^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 56 76 77

Eliminating location l18 by chaining:

Applied chaining
First rule:
l7 -> l18 : TRUE, cost: 1
Second rule:
l18 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 1
New rule:
l7 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 2

Applied chaining
First rule:
l7 -> l18 : TRUE, cost: 1
Second rule:
l18 -> l22 : h^0'=0, 1-edgecount^0+k_1^0 <= 0, cost: 1
New rule:
l7 -> l22 : h^0'=0, 1-edgecount^0+k_1^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 63 74 75

Eliminating location l24 by chaining:

Applied chaining
First rule:
l22 -> l24 : TRUE, cost: 1
Second rule:
l24 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 1
New rule:
l22 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 2

Applied chaining
First rule:
l22 -> l24 : TRUE, cost: 1
Second rule:
l24 -> l23 : 1+h^0-edgecount^0 <= 0, cost: 1
New rule:
l22 -> l23 : 1+h^0-edgecount^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 71 72 73

Eliminating location l20 by chaining:

Applied chaining
First rule:
l17 -> l20 : TRUE, cost: 1
Second rule:
l20 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 1
New rule:
l17 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 2

Applied chaining
First rule:
l17 -> l20 : TRUE, cost: 1
Second rule:
l20 -> l19 : 1-nodecount^0+j^0 <= 0, cost: 1
New rule:
l17 -> l19 : 1-nodecount^0+j^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 66 67 78

Eliminating location l15 by chaining:

Applied chaining
First rule:
l13 -> l15 : TRUE, cost: 1
Second rule:
l15 -> l9 : nodecount^0-j^0 <= 0, cost: 1
New rule:
l13 -> l9 : nodecount^0-j^0 <= 0, cost: 2

Applied chaining
First rule:
l13 -> l15 : TRUE, cost: 1
Second rule:
l15 -> l14 : 1-nodecount^0+j^0 <= 0, cost: 1
New rule:
l13 -> l14 : 1-nodecount^0+j^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 60 61 84

Eliminating location l8 by chaining:

Applied chaining
First rule:
l9 -> l8 : sourceflag^0 == 0, cost: 1
Second rule:
l8 -> l6 : -1+destflag^0 >= 0, cost: 1
New rule:
l9 -> l6 : (-1+destflag^0 >= 0 /\ sourceflag^0 == 0), cost: 2

Applied chaining
First rule:
l9 -> l8 : sourceflag^0 == 0, cost: 1
Second rule:
l8 -> l6 : 1+destflag^0 <= 0, cost: 1
New rule:
l9 -> l6 : (1+destflag^0 <= 0 /\ sourceflag^0 == 0), cost: 2

Applied chaining
First rule:
l9 -> l8 : sourceflag^0 == 0, cost: 1
Second rule:
l8 -> l6 : destflag^0 == 0, cost: 1
New rule:
l9 -> l6 : (destflag^0 == 0 /\ sourceflag^0 == 0), cost: 2

Applied deletion
Removed the following rules: 50 51 52 55

Eliminating location l12 by chaining:

Applied chaining
First rule:
l14 -> l12 : TRUE, cost: 1
Second rule:
l12 -> l13 : j^0'=1+j^0, TRUE, cost: 1
New rule:
l14 -> l13 : j^0'=1+j^0, TRUE, cost: 2

Applied chaining
First rule:
l14 -> l12 : destflag^0'=0, TRUE, cost: 1
Second rule:
l12 -> l13 : j^0'=1+j^0, TRUE, cost: 1
New rule:
l14 -> l13 : destflag^0'=0, j^0'=1+j^0, TRUE, cost: 2

Applied deletion
Removed the following rules: 57 58 59

Eliminating location l16 by chaining:

Applied chaining
First rule:
l19 -> l16 : TRUE, cost: 1
Second rule:
l16 -> l17 : j^0'=1+j^0, TRUE, cost: 1
New rule:
l19 -> l17 : j^0'=1+j^0, TRUE, cost: 2

Applied chaining
First rule:
l19 -> l16 : sourceflag^0'=1, TRUE, cost: 1
Second rule:
l16 -> l17 : j^0'=1+j^0, TRUE, cost: 1
New rule:
l19 -> l17 : j^0'=1+j^0, sourceflag^0'=1, TRUE, cost: 2

Applied deletion
Removed the following rules: 62 64 65

Eliminating location l21 by chaining:

Applied chaining
First rule:
l23 -> l21 : min^0'=h^0, TRUE, cost: 1
Second rule:
l21 -> l22 : h^0'=1+h^0, TRUE, cost: 1
New rule:
l23 -> l22 : h^0'=1+h^0, min^0'=h^0, TRUE, cost: 2

Applied chaining
First rule:
l23 -> l21 : TRUE, cost: 1
Second rule:
l21 -> l22 : h^0'=1+h^0, TRUE, cost: 1
New rule:
l23 -> l22 : h^0'=1+h^0, TRUE, cost: 2

Applied deletion
Removed the following rules: 68 69 70

Eliminated locations on tree-shaped paths
Start location: l28
  90: l0 -> l2 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 2
  91: l0 -> l0 : i^0'=1+i^0, 1+i^0-nodecount^0 <= 0, cost: 2
  92: l2 -> l4 : k^0'=0, -1-i^0+nodecount^0 <= 0, cost: 2
  93: l2 -> l2 : i^0'=1+i^0, 2+i^0-nodecount^0 <= 0, cost: 2
  94: l4 -> l25 : nodecount^0-k^0 <= 0, cost: 2
  95: l4 -> l25 : 2-nodecount^0+k^0 <= 0, cost: 2
  49: l6 -> l7 : k_1^0'=1+k_1^0, TRUE, cost: 1
  98: l7 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 2
  99: l7 -> l22 : h^0'=0, 1-edgecount^0+k_1^0 <= 0, cost: 2
  53: l9 -> l6 : -1+sourceflag^0 >= 0, cost: 1
  54: l9 -> l6 : 1+sourceflag^0 <= 0, cost: 1
 106: l9 -> l6 : (-1+destflag^0 >= 0 /\ sourceflag^0 == 0), cost: 2
 107: l9 -> l6 : (1+destflag^0 <= 0 /\ sourceflag^0 == 0), cost: 2
 108: l9 -> l6 : (destflag^0 == 0 /\ sourceflag^0 == 0), cost: 2
  96: l10 -> l7 : k_1^0'=0, -i^0+edgecount^0 <= 0, cost: 2
  97: l10 -> l10 : i^0'=1+i^0, 1+i^0-edgecount^0 <= 0, cost: 2
 104: l13 -> l9 : nodecount^0-j^0 <= 0, cost: 2
 105: l13 -> l14 : 1-nodecount^0+j^0 <= 0, cost: 2
 109: l14 -> l13 : j^0'=1+j^0, TRUE, cost: 2
 110: l14 -> l13 : destflag^0'=0, j^0'=1+j^0, TRUE, cost: 2
 102: l17 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 2
 103: l17 -> l19 : 1-nodecount^0+j^0 <= 0, cost: 2
 111: l19 -> l17 : j^0'=1+j^0, TRUE, cost: 2
 112: l19 -> l17 : j^0'=1+j^0, sourceflag^0'=1, TRUE, cost: 2
 100: l22 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 2
 101: l22 -> l23 : 1+h^0-edgecount^0 <= 0, cost: 2
 113: l23 -> l22 : h^0'=1+h^0, min^0'=h^0, TRUE, cost: 2
 114: l23 -> l22 : h^0'=1+h^0, TRUE, cost: 2
  79: l25 -> l10 : i^0'=0, min^0'=0, TRUE, cost: 1
  89: l28 -> l0 : i^0'=1, __lengthofvisited^0'=edgecount^0, TRUE, cost: 2


Applied acceleration
Original rule:
l0 -> l0 : i^0'=1+i^0, 1+i^0-nodecount^0 <= 0, cost: 2
New rule:
l0 -> l0 : i^0'=i^0+n, (n >= 0 /\ -i^0+nodecount^0-n >= 0), cost: 2*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_pdecFO.txt

Applied instantiation
Original rule:
l0 -> l0 : i^0'=i^0+n, (n >= 0 /\ -i^0+nodecount^0-n >= 0), cost: 2*n
New rule:
l0 -> l0 : i^0'=nodecount^0, (0 >= 0 /\ -i^0+nodecount^0 >= 0), cost: -2*i^0+2*nodecount^0

Applied simplification
Original rule:
l0 -> l0 : i^0'=nodecount^0, (0 >= 0 /\ -i^0+nodecount^0 >= 0), cost: -2*i^0+2*nodecount^0
New rule:
l0 -> l0 : i^0'=nodecount^0, -i^0+nodecount^0 >= 0, cost: -2*i^0+2*nodecount^0

Applied deletion
Removed the following rules: 91

Applied acceleration
Original rule:
l2 -> l2 : i^0'=1+i^0, 2+i^0-nodecount^0 <= 0, cost: 2
New rule:
l2 -> l2 : i^0'=n0+i^0, (n0 >= 0 /\ -1-n0-i^0+nodecount^0 >= 0), cost: 2*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ifFnNM.txt

Applied instantiation
Original rule:
l2 -> l2 : i^0'=n0+i^0, (n0 >= 0 /\ -1-n0-i^0+nodecount^0 >= 0), cost: 2*n0
New rule:
l2 -> l2 : i^0'=-1+nodecount^0, (0 >= 0 /\ -1-i^0+nodecount^0 >= 0), cost: -2-2*i^0+2*nodecount^0

Applied simplification
Original rule:
l2 -> l2 : i^0'=-1+nodecount^0, (0 >= 0 /\ -1-i^0+nodecount^0 >= 0), cost: -2-2*i^0+2*nodecount^0
New rule:
l2 -> l2 : i^0'=-1+nodecount^0, -1-i^0+nodecount^0 >= 0, cost: -2-2*i^0+2*nodecount^0

Applied deletion
Removed the following rules: 93

Applied acceleration
Original rule:
l10 -> l10 : i^0'=1+i^0, 1+i^0-edgecount^0 <= 0, cost: 2
New rule:
l10 -> l10 : i^0'=i^0+n1, (n1 >= 0 /\ -i^0-n1+edgecount^0 >= 0), cost: 2*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_nmoFdd.txt

Applied instantiation
Original rule:
l10 -> l10 : i^0'=i^0+n1, (n1 >= 0 /\ -i^0-n1+edgecount^0 >= 0), cost: 2*n1
New rule:
l10 -> l10 : i^0'=edgecount^0, (0 >= 0 /\ -i^0+edgecount^0 >= 0), cost: -2*i^0+2*edgecount^0

Applied simplification
Original rule:
l10 -> l10 : i^0'=edgecount^0, (0 >= 0 /\ -i^0+edgecount^0 >= 0), cost: -2*i^0+2*edgecount^0
New rule:
l10 -> l10 : i^0'=edgecount^0, -i^0+edgecount^0 >= 0, cost: -2*i^0+2*edgecount^0

Applied deletion
Removed the following rules: 97

Accelerated simple loops
Start location: l28
  90: l0 -> l2 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 2
 116: l0 -> l0 : i^0'=nodecount^0, -i^0+nodecount^0 >= 0, cost: -2*i^0+2*nodecount^0
  92: l2 -> l4 : k^0'=0, -1-i^0+nodecount^0 <= 0, cost: 2
 118: l2 -> l2 : i^0'=-1+nodecount^0, -1-i^0+nodecount^0 >= 0, cost: -2-2*i^0+2*nodecount^0
  94: l4 -> l25 : nodecount^0-k^0 <= 0, cost: 2
  95: l4 -> l25 : 2-nodecount^0+k^0 <= 0, cost: 2
  49: l6 -> l7 : k_1^0'=1+k_1^0, TRUE, cost: 1
  98: l7 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 2
  99: l7 -> l22 : h^0'=0, 1-edgecount^0+k_1^0 <= 0, cost: 2
  53: l9 -> l6 : -1+sourceflag^0 >= 0, cost: 1
  54: l9 -> l6 : 1+sourceflag^0 <= 0, cost: 1
 106: l9 -> l6 : (-1+destflag^0 >= 0 /\ sourceflag^0 == 0), cost: 2
 107: l9 -> l6 : (1+destflag^0 <= 0 /\ sourceflag^0 == 0), cost: 2
 108: l9 -> l6 : (destflag^0 == 0 /\ sourceflag^0 == 0), cost: 2
  96: l10 -> l7 : k_1^0'=0, -i^0+edgecount^0 <= 0, cost: 2
 120: l10 -> l10 : i^0'=edgecount^0, -i^0+edgecount^0 >= 0, cost: -2*i^0+2*edgecount^0
 104: l13 -> l9 : nodecount^0-j^0 <= 0, cost: 2
 105: l13 -> l14 : 1-nodecount^0+j^0 <= 0, cost: 2
 109: l14 -> l13 : j^0'=1+j^0, TRUE, cost: 2
 110: l14 -> l13 : destflag^0'=0, j^0'=1+j^0, TRUE, cost: 2
 102: l17 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 2
 103: l17 -> l19 : 1-nodecount^0+j^0 <= 0, cost: 2
 111: l19 -> l17 : j^0'=1+j^0, TRUE, cost: 2
 112: l19 -> l17 : j^0'=1+j^0, sourceflag^0'=1, TRUE, cost: 2
 100: l22 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 2
 101: l22 -> l23 : 1+h^0-edgecount^0 <= 0, cost: 2
 113: l23 -> l22 : h^0'=1+h^0, min^0'=h^0, TRUE, cost: 2
 114: l23 -> l22 : h^0'=1+h^0, TRUE, cost: 2
  79: l25 -> l10 : i^0'=0, min^0'=0, TRUE, cost: 1
  89: l28 -> l0 : i^0'=1, __lengthofvisited^0'=edgecount^0, TRUE, cost: 2


Applied chaining
First rule:
l28 -> l0 : i^0'=1, __lengthofvisited^0'=edgecount^0, TRUE, cost: 2
Second rule:
l0 -> l0 : i^0'=nodecount^0, -i^0+nodecount^0 >= 0, cost: -2*i^0+2*nodecount^0
New rule:
l28 -> l0 : i^0'=nodecount^0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2*nodecount^0

Applied deletion
Removed the following rules: 116

Applied chaining
First rule:
l0 -> l2 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 2
Second rule:
l2 -> l2 : i^0'=-1+nodecount^0, -1-i^0+nodecount^0 >= 0, cost: -2-2*i^0+2*nodecount^0
New rule:
l0 -> l2 : i^0'=-1+nodecount^0, (-1+nodecount^0 >= 0 /\ -i^0+nodecount^0 <= 0), cost: 2*nodecount^0

Applied deletion
Removed the following rules: 118

Applied chaining
First rule:
l25 -> l10 : i^0'=0, min^0'=0, TRUE, cost: 1
Second rule:
l10 -> l10 : i^0'=edgecount^0, -i^0+edgecount^0 >= 0, cost: -2*i^0+2*edgecount^0
New rule:
l25 -> l10 : i^0'=edgecount^0, min^0'=0, edgecount^0 >= 0, cost: 1+2*edgecount^0

Applied deletion
Removed the following rules: 120

Chained accelerated rules with incoming rules
Start location: l28
  90: l0 -> l2 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 2
 122: l0 -> l2 : i^0'=-1+nodecount^0, (-1+nodecount^0 >= 0 /\ -i^0+nodecount^0 <= 0), cost: 2*nodecount^0
  92: l2 -> l4 : k^0'=0, -1-i^0+nodecount^0 <= 0, cost: 2
  94: l4 -> l25 : nodecount^0-k^0 <= 0, cost: 2
  95: l4 -> l25 : 2-nodecount^0+k^0 <= 0, cost: 2
  49: l6 -> l7 : k_1^0'=1+k_1^0, TRUE, cost: 1
  98: l7 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 2
  99: l7 -> l22 : h^0'=0, 1-edgecount^0+k_1^0 <= 0, cost: 2
  53: l9 -> l6 : -1+sourceflag^0 >= 0, cost: 1
  54: l9 -> l6 : 1+sourceflag^0 <= 0, cost: 1
 106: l9 -> l6 : (-1+destflag^0 >= 0 /\ sourceflag^0 == 0), cost: 2
 107: l9 -> l6 : (1+destflag^0 <= 0 /\ sourceflag^0 == 0), cost: 2
 108: l9 -> l6 : (destflag^0 == 0 /\ sourceflag^0 == 0), cost: 2
  96: l10 -> l7 : k_1^0'=0, -i^0+edgecount^0 <= 0, cost: 2
 104: l13 -> l9 : nodecount^0-j^0 <= 0, cost: 2
 105: l13 -> l14 : 1-nodecount^0+j^0 <= 0, cost: 2
 109: l14 -> l13 : j^0'=1+j^0, TRUE, cost: 2
 110: l14 -> l13 : destflag^0'=0, j^0'=1+j^0, TRUE, cost: 2
 102: l17 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 2
 103: l17 -> l19 : 1-nodecount^0+j^0 <= 0, cost: 2
 111: l19 -> l17 : j^0'=1+j^0, TRUE, cost: 2
 112: l19 -> l17 : j^0'=1+j^0, sourceflag^0'=1, TRUE, cost: 2
 100: l22 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 2
 101: l22 -> l23 : 1+h^0-edgecount^0 <= 0, cost: 2
 113: l23 -> l22 : h^0'=1+h^0, min^0'=h^0, TRUE, cost: 2
 114: l23 -> l22 : h^0'=1+h^0, TRUE, cost: 2
  79: l25 -> l10 : i^0'=0, min^0'=0, TRUE, cost: 1
 123: l25 -> l10 : i^0'=edgecount^0, min^0'=0, edgecount^0 >= 0, cost: 1+2*edgecount^0
  89: l28 -> l0 : i^0'=1, __lengthofvisited^0'=edgecount^0, TRUE, cost: 2
 121: l28 -> l0 : i^0'=nodecount^0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2*nodecount^0


Eliminating location l0 by chaining:

Applied chaining
First rule:
l28 -> l0 : i^0'=1, __lengthofvisited^0'=edgecount^0, TRUE, cost: 2
Second rule:
l0 -> l2 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 2
New rule:
l28 -> l2 : i^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 4

Applied chaining
First rule:
l28 -> l0 : i^0'=1, __lengthofvisited^0'=edgecount^0, TRUE, cost: 2
Second rule:
l0 -> l2 : i^0'=-1+nodecount^0, (-1+nodecount^0 >= 0 /\ -i^0+nodecount^0 <= 0), cost: 2*nodecount^0
New rule:
l28 -> l2 : i^0'=-1+nodecount^0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 2+2*nodecount^0

Applied chaining
First rule:
l28 -> l0 : i^0'=nodecount^0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2*nodecount^0
Second rule:
l0 -> l2 : i^0'=0, -i^0+nodecount^0 <= 0, cost: 2
New rule:
l28 -> l2 : i^0'=0, __lengthofvisited^0'=edgecount^0, (0 <= 0 /\ -1+nodecount^0 >= 0), cost: 2+2*nodecount^0

Applied simplification
Original rule:
l28 -> l2 : i^0'=0, __lengthofvisited^0'=edgecount^0, (0 <= 0 /\ -1+nodecount^0 >= 0), cost: 2+2*nodecount^0
New rule:
l28 -> l2 : i^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2+2*nodecount^0

Applied chaining
First rule:
l28 -> l0 : i^0'=nodecount^0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2*nodecount^0
Second rule:
l0 -> l2 : i^0'=-1+nodecount^0, (-1+nodecount^0 >= 0 /\ -i^0+nodecount^0 <= 0), cost: 2*nodecount^0
New rule:
l28 -> l2 : i^0'=-1+nodecount^0, __lengthofvisited^0'=edgecount^0, (0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4*nodecount^0

Applied simplification
Original rule:
l28 -> l2 : i^0'=-1+nodecount^0, __lengthofvisited^0'=edgecount^0, (0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4*nodecount^0
New rule:
l28 -> l2 : i^0'=-1+nodecount^0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 4*nodecount^0

Applied deletion
Removed the following rules: 89 90 121 122

Eliminating location l25 by chaining:

Applied chaining
First rule:
l4 -> l25 : nodecount^0-k^0 <= 0, cost: 2
Second rule:
l25 -> l10 : i^0'=0, min^0'=0, TRUE, cost: 1
New rule:
l4 -> l10 : i^0'=0, min^0'=0, nodecount^0-k^0 <= 0, cost: 3

Applied chaining
First rule:
l4 -> l25 : nodecount^0-k^0 <= 0, cost: 2
Second rule:
l25 -> l10 : i^0'=edgecount^0, min^0'=0, edgecount^0 >= 0, cost: 1+2*edgecount^0
New rule:
l4 -> l10 : i^0'=edgecount^0, min^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 >= 0), cost: 3+2*edgecount^0

Applied chaining
First rule:
l4 -> l25 : 2-nodecount^0+k^0 <= 0, cost: 2
Second rule:
l25 -> l10 : i^0'=0, min^0'=0, TRUE, cost: 1
New rule:
l4 -> l10 : i^0'=0, min^0'=0, 2-nodecount^0+k^0 <= 0, cost: 3

Applied chaining
First rule:
l4 -> l25 : 2-nodecount^0+k^0 <= 0, cost: 2
Second rule:
l25 -> l10 : i^0'=edgecount^0, min^0'=0, edgecount^0 >= 0, cost: 1+2*edgecount^0
New rule:
l4 -> l10 : i^0'=edgecount^0, min^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 >= 0), cost: 3+2*edgecount^0

Applied deletion
Removed the following rules: 79 94 95 123

Eliminating location l23 by chaining:

Applied chaining
First rule:
l22 -> l23 : 1+h^0-edgecount^0 <= 0, cost: 2
Second rule:
l23 -> l22 : h^0'=1+h^0, min^0'=h^0, TRUE, cost: 2
New rule:
l22 -> l22 : h^0'=1+h^0, min^0'=h^0, 1+h^0-edgecount^0 <= 0, cost: 4

Applied chaining
First rule:
l22 -> l23 : 1+h^0-edgecount^0 <= 0, cost: 2
Second rule:
l23 -> l22 : h^0'=1+h^0, TRUE, cost: 2
New rule:
l22 -> l22 : h^0'=1+h^0, 1+h^0-edgecount^0 <= 0, cost: 4

Applied deletion
Removed the following rules: 101 113 114

Eliminating location l19 by chaining:

Applied chaining
First rule:
l17 -> l19 : 1-nodecount^0+j^0 <= 0, cost: 2
Second rule:
l19 -> l17 : j^0'=1+j^0, TRUE, cost: 2
New rule:
l17 -> l17 : j^0'=1+j^0, 1-nodecount^0+j^0 <= 0, cost: 4

Applied chaining
First rule:
l17 -> l19 : 1-nodecount^0+j^0 <= 0, cost: 2
Second rule:
l19 -> l17 : j^0'=1+j^0, sourceflag^0'=1, TRUE, cost: 2
New rule:
l17 -> l17 : j^0'=1+j^0, sourceflag^0'=1, 1-nodecount^0+j^0 <= 0, cost: 4

Applied deletion
Removed the following rules: 103 111 112

Eliminating location l9 by chaining:

Applied chaining
First rule:
l13 -> l9 : nodecount^0-j^0 <= 0, cost: 2
Second rule:
l9 -> l6 : -1+sourceflag^0 >= 0, cost: 1
New rule:
l13 -> l6 : (nodecount^0-j^0 <= 0 /\ -1+sourceflag^0 >= 0), cost: 3

Applied chaining
First rule:
l13 -> l9 : nodecount^0-j^0 <= 0, cost: 2
Second rule:
l9 -> l6 : 1+sourceflag^0 <= 0, cost: 1
New rule:
l13 -> l6 : (nodecount^0-j^0 <= 0 /\ 1+sourceflag^0 <= 0), cost: 3

Applied chaining
First rule:
l13 -> l9 : nodecount^0-j^0 <= 0, cost: 2
Second rule:
l9 -> l6 : (-1+destflag^0 >= 0 /\ sourceflag^0 == 0), cost: 2
New rule:
l13 -> l6 : (nodecount^0-j^0 <= 0 /\ -1+destflag^0 >= 0 /\ sourceflag^0 == 0), cost: 4

Applied chaining
First rule:
l13 -> l9 : nodecount^0-j^0 <= 0, cost: 2
Second rule:
l9 -> l6 : (1+destflag^0 <= 0 /\ sourceflag^0 == 0), cost: 2
New rule:
l13 -> l6 : (nodecount^0-j^0 <= 0 /\ 1+destflag^0 <= 0 /\ sourceflag^0 == 0), cost: 4

Applied chaining
First rule:
l13 -> l9 : nodecount^0-j^0 <= 0, cost: 2
Second rule:
l9 -> l6 : (destflag^0 == 0 /\ sourceflag^0 == 0), cost: 2
New rule:
l13 -> l6 : (nodecount^0-j^0 <= 0 /\ destflag^0 == 0 /\ sourceflag^0 == 0), cost: 4

Applied deletion
Removed the following rules: 53 54 104 106 107 108

Eliminating location l14 by chaining:

Applied chaining
First rule:
l13 -> l14 : 1-nodecount^0+j^0 <= 0, cost: 2
Second rule:
l14 -> l13 : j^0'=1+j^0, TRUE, cost: 2
New rule:
l13 -> l13 : j^0'=1+j^0, 1-nodecount^0+j^0 <= 0, cost: 4

Applied chaining
First rule:
l13 -> l14 : 1-nodecount^0+j^0 <= 0, cost: 2
Second rule:
l14 -> l13 : destflag^0'=0, j^0'=1+j^0, TRUE, cost: 2
New rule:
l13 -> l13 : destflag^0'=0, j^0'=1+j^0, 1-nodecount^0+j^0 <= 0, cost: 4

Applied deletion
Removed the following rules: 105 109 110

Eliminated locations on tree-shaped paths
Start location: l28
  92: l2 -> l4 : k^0'=0, -1-i^0+nodecount^0 <= 0, cost: 2
 128: l4 -> l10 : i^0'=0, min^0'=0, nodecount^0-k^0 <= 0, cost: 3
 129: l4 -> l10 : i^0'=edgecount^0, min^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 >= 0), cost: 3+2*edgecount^0
 130: l4 -> l10 : i^0'=0, min^0'=0, 2-nodecount^0+k^0 <= 0, cost: 3
 131: l4 -> l10 : i^0'=edgecount^0, min^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 >= 0), cost: 3+2*edgecount^0
  49: l6 -> l7 : k_1^0'=1+k_1^0, TRUE, cost: 1
  98: l7 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 2
  99: l7 -> l22 : h^0'=0, 1-edgecount^0+k_1^0 <= 0, cost: 2
  96: l10 -> l7 : k_1^0'=0, -i^0+edgecount^0 <= 0, cost: 2
 136: l13 -> l6 : (nodecount^0-j^0 <= 0 /\ -1+sourceflag^0 >= 0), cost: 3
 137: l13 -> l6 : (nodecount^0-j^0 <= 0 /\ 1+sourceflag^0 <= 0), cost: 3
 138: l13 -> l6 : (nodecount^0-j^0 <= 0 /\ -1+destflag^0 >= 0 /\ sourceflag^0 == 0), cost: 4
 139: l13 -> l6 : (nodecount^0-j^0 <= 0 /\ 1+destflag^0 <= 0 /\ sourceflag^0 == 0), cost: 4
 140: l13 -> l6 : (nodecount^0-j^0 <= 0 /\ destflag^0 == 0 /\ sourceflag^0 == 0), cost: 4
 141: l13 -> l13 : j^0'=1+j^0, 1-nodecount^0+j^0 <= 0, cost: 4
 142: l13 -> l13 : destflag^0'=0, j^0'=1+j^0, 1-nodecount^0+j^0 <= 0, cost: 4
 102: l17 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 2
 134: l17 -> l17 : j^0'=1+j^0, 1-nodecount^0+j^0 <= 0, cost: 4
 135: l17 -> l17 : j^0'=1+j^0, sourceflag^0'=1, 1-nodecount^0+j^0 <= 0, cost: 4
 100: l22 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 2
 132: l22 -> l22 : h^0'=1+h^0, min^0'=h^0, 1+h^0-edgecount^0 <= 0, cost: 4
 133: l22 -> l22 : h^0'=1+h^0, 1+h^0-edgecount^0 <= 0, cost: 4
 124: l28 -> l2 : i^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 4
 125: l28 -> l2 : i^0'=-1+nodecount^0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 2+2*nodecount^0
 126: l28 -> l2 : i^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2+2*nodecount^0
 127: l28 -> l2 : i^0'=-1+nodecount^0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 4*nodecount^0


Applied acceleration
Original rule:
l13 -> l13 : j^0'=1+j^0, 1-nodecount^0+j^0 <= 0, cost: 4
New rule:
l13 -> l13 : j^0'=j^0+n2, (n2 >= 0 /\ nodecount^0-j^0-n2 >= 0), cost: 4*n2
Sub-proof via acceration calculus written to file:///tmp/tmpnam_JHnAok.txt

Applied instantiation
Original rule:
l13 -> l13 : j^0'=j^0+n2, (n2 >= 0 /\ nodecount^0-j^0-n2 >= 0), cost: 4*n2
New rule:
l13 -> l13 : j^0'=nodecount^0, (0 >= 0 /\ nodecount^0-j^0 >= 0), cost: 4*nodecount^0-4*j^0

Applied acceleration
Original rule:
l13 -> l13 : destflag^0'=0, j^0'=1+j^0, 1-nodecount^0+j^0 <= 0, cost: 4
New rule:
l13 -> l13 : destflag^0'=0, j^0'=n3+j^0, (-n3+nodecount^0-j^0 >= 0 /\ -1+n3 >= 0), cost: 4*n3
Sub-proof via acceration calculus written to file:///tmp/tmpnam_mFpMko.txt

Applied instantiation
Original rule:
l13 -> l13 : destflag^0'=0, j^0'=n3+j^0, (-n3+nodecount^0-j^0 >= 0 /\ -1+n3 >= 0), cost: 4*n3
New rule:
l13 -> l13 : destflag^0'=0, j^0'=nodecount^0, (0 >= 0 /\ -1+nodecount^0-j^0 >= 0), cost: 4*nodecount^0-4*j^0

Applied simplification
Original rule:
l13 -> l13 : j^0'=nodecount^0, (0 >= 0 /\ nodecount^0-j^0 >= 0), cost: 4*nodecount^0-4*j^0
New rule:
l13 -> l13 : j^0'=nodecount^0, nodecount^0-j^0 >= 0, cost: 4*nodecount^0-4*j^0

Applied simplification
Original rule:
l13 -> l13 : destflag^0'=0, j^0'=nodecount^0, (0 >= 0 /\ -1+nodecount^0-j^0 >= 0), cost: 4*nodecount^0-4*j^0
New rule:
l13 -> l13 : destflag^0'=0, j^0'=nodecount^0, -1+nodecount^0-j^0 >= 0, cost: 4*nodecount^0-4*j^0

Applied deletion
Removed the following rules: 141 142

Applied acceleration
Original rule:
l17 -> l17 : j^0'=1+j^0, 1-nodecount^0+j^0 <= 0, cost: 4
New rule:
l17 -> l17 : j^0'=j^0+n8, (nodecount^0-j^0-n8 >= 0 /\ n8 >= 0), cost: 4*n8
Sub-proof via acceration calculus written to file:///tmp/tmpnam_NNajnE.txt

Applied instantiation
Original rule:
l17 -> l17 : j^0'=j^0+n8, (nodecount^0-j^0-n8 >= 0 /\ n8 >= 0), cost: 4*n8
New rule:
l17 -> l17 : j^0'=nodecount^0, (0 >= 0 /\ nodecount^0-j^0 >= 0), cost: 4*nodecount^0-4*j^0

Applied acceleration
Original rule:
l17 -> l17 : j^0'=1+j^0, sourceflag^0'=1, 1-nodecount^0+j^0 <= 0, cost: 4
New rule:
l17 -> l17 : j^0'=n9+j^0, sourceflag^0'=1, (-1+n9 >= 0 /\ nodecount^0-n9-j^0 >= 0), cost: 4*n9
Sub-proof via acceration calculus written to file:///tmp/tmpnam_KLlLKf.txt

Applied instantiation
Original rule:
l17 -> l17 : j^0'=n9+j^0, sourceflag^0'=1, (-1+n9 >= 0 /\ nodecount^0-n9-j^0 >= 0), cost: 4*n9
New rule:
l17 -> l17 : j^0'=nodecount^0, sourceflag^0'=1, (0 >= 0 /\ -1+nodecount^0-j^0 >= 0), cost: 4*nodecount^0-4*j^0

Applied simplification
Original rule:
l17 -> l17 : j^0'=nodecount^0, (0 >= 0 /\ nodecount^0-j^0 >= 0), cost: 4*nodecount^0-4*j^0
New rule:
l17 -> l17 : j^0'=nodecount^0, nodecount^0-j^0 >= 0, cost: 4*nodecount^0-4*j^0

Applied simplification
Original rule:
l17 -> l17 : j^0'=nodecount^0, sourceflag^0'=1, (0 >= 0 /\ -1+nodecount^0-j^0 >= 0), cost: 4*nodecount^0-4*j^0
New rule:
l17 -> l17 : j^0'=nodecount^0, sourceflag^0'=1, -1+nodecount^0-j^0 >= 0, cost: 4*nodecount^0-4*j^0

Applied deletion
Removed the following rules: 134 135

Applied acceleration
Original rule:
l22 -> l22 : h^0'=1+h^0, min^0'=h^0, 1+h^0-edgecount^0 <= 0, cost: 4
New rule:
l22 -> l22 : h^0'=n14+h^0, min^0'=-1+n14+h^0, (-1+n14 >= 0 /\ -n14-h^0+edgecount^0 >= 0), cost: 4*n14
Sub-proof via acceration calculus written to file:///tmp/tmpnam_eHaLiC.txt

Applied instantiation
Original rule:
l22 -> l22 : h^0'=n14+h^0, min^0'=-1+n14+h^0, (-1+n14 >= 0 /\ -n14-h^0+edgecount^0 >= 0), cost: 4*n14
New rule:
l22 -> l22 : h^0'=edgecount^0, min^0'=-1+edgecount^0, (0 >= 0 /\ -1-h^0+edgecount^0 >= 0), cost: -4*h^0+4*edgecount^0

Applied acceleration
Original rule:
l22 -> l22 : h^0'=1+h^0, 1+h^0-edgecount^0 <= 0, cost: 4
New rule:
l22 -> l22 : h^0'=h^0+n15, (n15 >= 0 /\ -h^0-n15+edgecount^0 >= 0), cost: 4*n15
Sub-proof via acceration calculus written to file:///tmp/tmpnam_JOONNo.txt

Applied instantiation
Original rule:
l22 -> l22 : h^0'=h^0+n15, (n15 >= 0 /\ -h^0-n15+edgecount^0 >= 0), cost: 4*n15
New rule:
l22 -> l22 : h^0'=edgecount^0, (0 >= 0 /\ -h^0+edgecount^0 >= 0), cost: -4*h^0+4*edgecount^0

Applied simplification
Original rule:
l22 -> l22 : h^0'=edgecount^0, min^0'=-1+edgecount^0, (0 >= 0 /\ -1-h^0+edgecount^0 >= 0), cost: -4*h^0+4*edgecount^0
New rule:
l22 -> l22 : h^0'=edgecount^0, min^0'=-1+edgecount^0, -1-h^0+edgecount^0 >= 0, cost: -4*h^0+4*edgecount^0

Applied simplification
Original rule:
l22 -> l22 : h^0'=edgecount^0, (0 >= 0 /\ -h^0+edgecount^0 >= 0), cost: -4*h^0+4*edgecount^0
New rule:
l22 -> l22 : h^0'=edgecount^0, -h^0+edgecount^0 >= 0, cost: -4*h^0+4*edgecount^0

Applied deletion
Removed the following rules: 132 133

Accelerated simple loops
Start location: l28
  92: l2 -> l4 : k^0'=0, -1-i^0+nodecount^0 <= 0, cost: 2
 128: l4 -> l10 : i^0'=0, min^0'=0, nodecount^0-k^0 <= 0, cost: 3
 129: l4 -> l10 : i^0'=edgecount^0, min^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 >= 0), cost: 3+2*edgecount^0
 130: l4 -> l10 : i^0'=0, min^0'=0, 2-nodecount^0+k^0 <= 0, cost: 3
 131: l4 -> l10 : i^0'=edgecount^0, min^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 >= 0), cost: 3+2*edgecount^0
  49: l6 -> l7 : k_1^0'=1+k_1^0, TRUE, cost: 1
  98: l7 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 2
  99: l7 -> l22 : h^0'=0, 1-edgecount^0+k_1^0 <= 0, cost: 2
  96: l10 -> l7 : k_1^0'=0, -i^0+edgecount^0 <= 0, cost: 2
 136: l13 -> l6 : (nodecount^0-j^0 <= 0 /\ -1+sourceflag^0 >= 0), cost: 3
 137: l13 -> l6 : (nodecount^0-j^0 <= 0 /\ 1+sourceflag^0 <= 0), cost: 3
 138: l13 -> l6 : (nodecount^0-j^0 <= 0 /\ -1+destflag^0 >= 0 /\ sourceflag^0 == 0), cost: 4
 139: l13 -> l6 : (nodecount^0-j^0 <= 0 /\ 1+destflag^0 <= 0 /\ sourceflag^0 == 0), cost: 4
 140: l13 -> l6 : (nodecount^0-j^0 <= 0 /\ destflag^0 == 0 /\ sourceflag^0 == 0), cost: 4
 145: l13 -> l13 : j^0'=nodecount^0, nodecount^0-j^0 >= 0, cost: 4*nodecount^0-4*j^0
 146: l13 -> l13 : destflag^0'=0, j^0'=nodecount^0, -1+nodecount^0-j^0 >= 0, cost: 4*nodecount^0-4*j^0
 102: l17 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 2
 149: l17 -> l17 : j^0'=nodecount^0, nodecount^0-j^0 >= 0, cost: 4*nodecount^0-4*j^0
 150: l17 -> l17 : j^0'=nodecount^0, sourceflag^0'=1, -1+nodecount^0-j^0 >= 0, cost: 4*nodecount^0-4*j^0
 100: l22 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 2
 153: l22 -> l22 : h^0'=edgecount^0, min^0'=-1+edgecount^0, -1-h^0+edgecount^0 >= 0, cost: -4*h^0+4*edgecount^0
 154: l22 -> l22 : h^0'=edgecount^0, -h^0+edgecount^0 >= 0, cost: -4*h^0+4*edgecount^0
 124: l28 -> l2 : i^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 4
 125: l28 -> l2 : i^0'=-1+nodecount^0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 2+2*nodecount^0
 126: l28 -> l2 : i^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2+2*nodecount^0
 127: l28 -> l2 : i^0'=-1+nodecount^0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 4*nodecount^0


Applied chaining
First rule:
l17 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 2
Second rule:
l13 -> l13 : j^0'=nodecount^0, nodecount^0-j^0 >= 0, cost: 4*nodecount^0-4*j^0
New rule:
l17 -> l13 : destflag^0'=1, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0), cost: 2+4*nodecount^0

Applied chaining
First rule:
l17 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 2
Second rule:
l13 -> l13 : destflag^0'=0, j^0'=nodecount^0, -1+nodecount^0-j^0 >= 0, cost: 4*nodecount^0-4*j^0
New rule:
l17 -> l13 : destflag^0'=0, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 2+4*nodecount^0

Applied deletion
Removed the following rules: 145 146

Applied chaining
First rule:
l22 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 2
Second rule:
l17 -> l17 : j^0'=nodecount^0, nodecount^0-j^0 >= 0, cost: 4*nodecount^0-4*j^0
New rule:
l22 -> l17 : j^0'=nodecount^0, sourceflag^0'=0, (nodecount^0 >= 0 /\ -h^0+edgecount^0 <= 0), cost: 2+4*nodecount^0

Applied chaining
First rule:
l22 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 2
Second rule:
l17 -> l17 : j^0'=nodecount^0, sourceflag^0'=1, -1+nodecount^0-j^0 >= 0, cost: 4*nodecount^0-4*j^0
New rule:
l22 -> l17 : j^0'=nodecount^0, sourceflag^0'=1, (-1+nodecount^0 >= 0 /\ -h^0+edgecount^0 <= 0), cost: 2+4*nodecount^0

Applied deletion
Removed the following rules: 149 150

Applied chaining
First rule:
l7 -> l22 : h^0'=0, 1-edgecount^0+k_1^0 <= 0, cost: 2
Second rule:
l22 -> l22 : h^0'=edgecount^0, min^0'=-1+edgecount^0, -1-h^0+edgecount^0 >= 0, cost: -4*h^0+4*edgecount^0
New rule:
l7 -> l22 : h^0'=edgecount^0, min^0'=-1+edgecount^0, (1-edgecount^0+k_1^0 <= 0 /\ -1+edgecount^0 >= 0), cost: 2+4*edgecount^0

Applied chaining
First rule:
l7 -> l22 : h^0'=0, 1-edgecount^0+k_1^0 <= 0, cost: 2
Second rule:
l22 -> l22 : h^0'=edgecount^0, -h^0+edgecount^0 >= 0, cost: -4*h^0+4*edgecount^0
New rule:
l7 -> l22 : h^0'=edgecount^0, (1-edgecount^0+k_1^0 <= 0 /\ edgecount^0 >= 0), cost: 2+4*edgecount^0

Applied deletion
Removed the following rules: 153 154

Chained accelerated rules with incoming rules
Start location: l28
  92: l2 -> l4 : k^0'=0, -1-i^0+nodecount^0 <= 0, cost: 2
 128: l4 -> l10 : i^0'=0, min^0'=0, nodecount^0-k^0 <= 0, cost: 3
 129: l4 -> l10 : i^0'=edgecount^0, min^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 >= 0), cost: 3+2*edgecount^0
 130: l4 -> l10 : i^0'=0, min^0'=0, 2-nodecount^0+k^0 <= 0, cost: 3
 131: l4 -> l10 : i^0'=edgecount^0, min^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 >= 0), cost: 3+2*edgecount^0
  49: l6 -> l7 : k_1^0'=1+k_1^0, TRUE, cost: 1
  98: l7 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 2
  99: l7 -> l22 : h^0'=0, 1-edgecount^0+k_1^0 <= 0, cost: 2
 159: l7 -> l22 : h^0'=edgecount^0, min^0'=-1+edgecount^0, (1-edgecount^0+k_1^0 <= 0 /\ -1+edgecount^0 >= 0), cost: 2+4*edgecount^0
 160: l7 -> l22 : h^0'=edgecount^0, (1-edgecount^0+k_1^0 <= 0 /\ edgecount^0 >= 0), cost: 2+4*edgecount^0
  96: l10 -> l7 : k_1^0'=0, -i^0+edgecount^0 <= 0, cost: 2
 136: l13 -> l6 : (nodecount^0-j^0 <= 0 /\ -1+sourceflag^0 >= 0), cost: 3
 137: l13 -> l6 : (nodecount^0-j^0 <= 0 /\ 1+sourceflag^0 <= 0), cost: 3
 138: l13 -> l6 : (nodecount^0-j^0 <= 0 /\ -1+destflag^0 >= 0 /\ sourceflag^0 == 0), cost: 4
 139: l13 -> l6 : (nodecount^0-j^0 <= 0 /\ 1+destflag^0 <= 0 /\ sourceflag^0 == 0), cost: 4
 140: l13 -> l6 : (nodecount^0-j^0 <= 0 /\ destflag^0 == 0 /\ sourceflag^0 == 0), cost: 4
 102: l17 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 2
 155: l17 -> l13 : destflag^0'=1, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0), cost: 2+4*nodecount^0
 156: l17 -> l13 : destflag^0'=0, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 2+4*nodecount^0
 100: l22 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 2
 157: l22 -> l17 : j^0'=nodecount^0, sourceflag^0'=0, (nodecount^0 >= 0 /\ -h^0+edgecount^0 <= 0), cost: 2+4*nodecount^0
 158: l22 -> l17 : j^0'=nodecount^0, sourceflag^0'=1, (-1+nodecount^0 >= 0 /\ -h^0+edgecount^0 <= 0), cost: 2+4*nodecount^0
 124: l28 -> l2 : i^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 4
 125: l28 -> l2 : i^0'=-1+nodecount^0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 2+2*nodecount^0
 126: l28 -> l2 : i^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2+2*nodecount^0
 127: l28 -> l2 : i^0'=-1+nodecount^0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 4*nodecount^0


Eliminating location l2 by chaining:

Applied chaining
First rule:
l28 -> l2 : i^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 4
Second rule:
l2 -> l4 : k^0'=0, -1-i^0+nodecount^0 <= 0, cost: 2
New rule:
l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 6

Applied chaining
First rule:
l28 -> l2 : i^0'=-1+nodecount^0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 2+2*nodecount^0
Second rule:
l2 -> l4 : k^0'=0, -1-i^0+nodecount^0 <= 0, cost: 2
New rule:
l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, (0 <= 0 /\ -1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0

Applied simplification
Original rule:
l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, (0 <= 0 /\ -1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0
New rule:
l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0

Applied chaining
First rule:
l28 -> l2 : i^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2+2*nodecount^0
Second rule:
l2 -> l4 : k^0'=0, -1-i^0+nodecount^0 <= 0, cost: 2
New rule:
l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0

Applied chaining
First rule:
l28 -> l2 : i^0'=-1+nodecount^0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 4*nodecount^0
Second rule:
l2 -> l4 : k^0'=0, -1-i^0+nodecount^0 <= 0, cost: 2
New rule:
l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, (0 <= 0 /\ -1+nodecount^0 >= 0), cost: 2+4*nodecount^0

Applied simplification
Original rule:
l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, (0 <= 0 /\ -1+nodecount^0 >= 0), cost: 2+4*nodecount^0
New rule:
l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2+4*nodecount^0

Applied deletion
Removed the following rules: 92 124 125 126 127

Eliminating location l10 by chaining:

Applied chaining
First rule:
l4 -> l10 : i^0'=0, min^0'=0, nodecount^0-k^0 <= 0, cost: 3
Second rule:
l10 -> l7 : k_1^0'=0, -i^0+edgecount^0 <= 0, cost: 2
New rule:
l4 -> l7 : i^0'=0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0), cost: 5

Applied chaining
First rule:
l4 -> l10 : i^0'=edgecount^0, min^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 >= 0), cost: 3+2*edgecount^0
Second rule:
l10 -> l7 : k_1^0'=0, -i^0+edgecount^0 <= 0, cost: 2
New rule:
l4 -> l7 : i^0'=edgecount^0, min^0'=0, k_1^0'=0, (0 <= 0 /\ nodecount^0-k^0 <= 0 /\ edgecount^0 >= 0), cost: 5+2*edgecount^0

Applied simplification
Original rule:
l4 -> l7 : i^0'=edgecount^0, min^0'=0, k_1^0'=0, (0 <= 0 /\ nodecount^0-k^0 <= 0 /\ edgecount^0 >= 0), cost: 5+2*edgecount^0
New rule:
l4 -> l7 : i^0'=edgecount^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 >= 0), cost: 5+2*edgecount^0

Applied chaining
First rule:
l4 -> l10 : i^0'=0, min^0'=0, 2-nodecount^0+k^0 <= 0, cost: 3
Second rule:
l10 -> l7 : k_1^0'=0, -i^0+edgecount^0 <= 0, cost: 2
New rule:
l4 -> l7 : i^0'=0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 <= 0), cost: 5

Applied chaining
First rule:
l4 -> l10 : i^0'=edgecount^0, min^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 >= 0), cost: 3+2*edgecount^0
Second rule:
l10 -> l7 : k_1^0'=0, -i^0+edgecount^0 <= 0, cost: 2
New rule:
l4 -> l7 : i^0'=edgecount^0, min^0'=0, k_1^0'=0, (0 <= 0 /\ 2-nodecount^0+k^0 <= 0 /\ edgecount^0 >= 0), cost: 5+2*edgecount^0

Applied simplification
Original rule:
l4 -> l7 : i^0'=edgecount^0, min^0'=0, k_1^0'=0, (0 <= 0 /\ 2-nodecount^0+k^0 <= 0 /\ edgecount^0 >= 0), cost: 5+2*edgecount^0
New rule:
l4 -> l7 : i^0'=edgecount^0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 >= 0), cost: 5+2*edgecount^0

Applied deletion
Removed the following rules: 96 128 129 130 131

Eliminating location l22 by chaining:

Applied chaining
First rule:
l7 -> l22 : h^0'=0, 1-edgecount^0+k_1^0 <= 0, cost: 2
Second rule:
l22 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 2
New rule:
l7 -> l17 : h^0'=0, j^0'=0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ edgecount^0 <= 0), cost: 4

Applied chaining
First rule:
l7 -> l22 : h^0'=0, 1-edgecount^0+k_1^0 <= 0, cost: 2
Second rule:
l22 -> l17 : j^0'=nodecount^0, sourceflag^0'=0, (nodecount^0 >= 0 /\ -h^0+edgecount^0 <= 0), cost: 2+4*nodecount^0
New rule:
l7 -> l17 : h^0'=0, j^0'=nodecount^0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ nodecount^0 >= 0 /\ edgecount^0 <= 0), cost: 4+4*nodecount^0

Applied chaining
First rule:
l7 -> l22 : h^0'=0, 1-edgecount^0+k_1^0 <= 0, cost: 2
Second rule:
l22 -> l17 : j^0'=nodecount^0, sourceflag^0'=1, (-1+nodecount^0 >= 0 /\ -h^0+edgecount^0 <= 0), cost: 2+4*nodecount^0
New rule:
l7 -> l17 : h^0'=0, j^0'=nodecount^0, sourceflag^0'=1, (1-edgecount^0+k_1^0 <= 0 /\ -1+nodecount^0 >= 0 /\ edgecount^0 <= 0), cost: 4+4*nodecount^0

Applied chaining
First rule:
l7 -> l22 : h^0'=edgecount^0, min^0'=-1+edgecount^0, (1-edgecount^0+k_1^0 <= 0 /\ -1+edgecount^0 >= 0), cost: 2+4*edgecount^0
Second rule:
l22 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 2
New rule:
l7 -> l17 : h^0'=edgecount^0, min^0'=-1+edgecount^0, j^0'=0, sourceflag^0'=0, (0 <= 0 /\ 1-edgecount^0+k_1^0 <= 0 /\ -1+edgecount^0 >= 0), cost: 4+4*edgecount^0

Applied simplification
Original rule:
l7 -> l17 : h^0'=edgecount^0, min^0'=-1+edgecount^0, j^0'=0, sourceflag^0'=0, (0 <= 0 /\ 1-edgecount^0+k_1^0 <= 0 /\ -1+edgecount^0 >= 0), cost: 4+4*edgecount^0
New rule:
l7 -> l17 : h^0'=edgecount^0, min^0'=-1+edgecount^0, j^0'=0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ -1+edgecount^0 >= 0), cost: 4+4*edgecount^0

Applied chaining
First rule:
l7 -> l22 : h^0'=edgecount^0, min^0'=-1+edgecount^0, (1-edgecount^0+k_1^0 <= 0 /\ -1+edgecount^0 >= 0), cost: 2+4*edgecount^0
Second rule:
l22 -> l17 : j^0'=nodecount^0, sourceflag^0'=0, (nodecount^0 >= 0 /\ -h^0+edgecount^0 <= 0), cost: 2+4*nodecount^0
New rule:
l7 -> l17 : h^0'=edgecount^0, min^0'=-1+edgecount^0, j^0'=nodecount^0, sourceflag^0'=0, (0 <= 0 /\ 1-edgecount^0+k_1^0 <= 0 /\ nodecount^0 >= 0 /\ -1+edgecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0

Applied simplification
Original rule:
l7 -> l17 : h^0'=edgecount^0, min^0'=-1+edgecount^0, j^0'=nodecount^0, sourceflag^0'=0, (0 <= 0 /\ 1-edgecount^0+k_1^0 <= 0 /\ nodecount^0 >= 0 /\ -1+edgecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0
New rule:
l7 -> l17 : h^0'=edgecount^0, min^0'=-1+edgecount^0, j^0'=nodecount^0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ nodecount^0 >= 0 /\ -1+edgecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0

Applied chaining
First rule:
l7 -> l22 : h^0'=edgecount^0, min^0'=-1+edgecount^0, (1-edgecount^0+k_1^0 <= 0 /\ -1+edgecount^0 >= 0), cost: 2+4*edgecount^0
Second rule:
l22 -> l17 : j^0'=nodecount^0, sourceflag^0'=1, (-1+nodecount^0 >= 0 /\ -h^0+edgecount^0 <= 0), cost: 2+4*nodecount^0
New rule:
l7 -> l17 : h^0'=edgecount^0, min^0'=-1+edgecount^0, j^0'=nodecount^0, sourceflag^0'=1, (0 <= 0 /\ 1-edgecount^0+k_1^0 <= 0 /\ -1+edgecount^0 >= 0 /\ -1+nodecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0

Applied simplification
Original rule:
l7 -> l17 : h^0'=edgecount^0, min^0'=-1+edgecount^0, j^0'=nodecount^0, sourceflag^0'=1, (0 <= 0 /\ 1-edgecount^0+k_1^0 <= 0 /\ -1+edgecount^0 >= 0 /\ -1+nodecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0
New rule:
l7 -> l17 : h^0'=edgecount^0, min^0'=-1+edgecount^0, j^0'=nodecount^0, sourceflag^0'=1, (1-edgecount^0+k_1^0 <= 0 /\ -1+edgecount^0 >= 0 /\ -1+nodecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0

Applied chaining
First rule:
l7 -> l22 : h^0'=edgecount^0, (1-edgecount^0+k_1^0 <= 0 /\ edgecount^0 >= 0), cost: 2+4*edgecount^0
Second rule:
l22 -> l17 : j^0'=0, sourceflag^0'=0, -h^0+edgecount^0 <= 0, cost: 2
New rule:
l7 -> l17 : h^0'=edgecount^0, j^0'=0, sourceflag^0'=0, (0 <= 0 /\ 1-edgecount^0+k_1^0 <= 0 /\ edgecount^0 >= 0), cost: 4+4*edgecount^0

Applied simplification
Original rule:
l7 -> l17 : h^0'=edgecount^0, j^0'=0, sourceflag^0'=0, (0 <= 0 /\ 1-edgecount^0+k_1^0 <= 0 /\ edgecount^0 >= 0), cost: 4+4*edgecount^0
New rule:
l7 -> l17 : h^0'=edgecount^0, j^0'=0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ edgecount^0 >= 0), cost: 4+4*edgecount^0

Applied chaining
First rule:
l7 -> l22 : h^0'=edgecount^0, (1-edgecount^0+k_1^0 <= 0 /\ edgecount^0 >= 0), cost: 2+4*edgecount^0
Second rule:
l22 -> l17 : j^0'=nodecount^0, sourceflag^0'=0, (nodecount^0 >= 0 /\ -h^0+edgecount^0 <= 0), cost: 2+4*nodecount^0
New rule:
l7 -> l17 : h^0'=edgecount^0, j^0'=nodecount^0, sourceflag^0'=0, (0 <= 0 /\ 1-edgecount^0+k_1^0 <= 0 /\ nodecount^0 >= 0 /\ edgecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0

Applied simplification
Original rule:
l7 -> l17 : h^0'=edgecount^0, j^0'=nodecount^0, sourceflag^0'=0, (0 <= 0 /\ 1-edgecount^0+k_1^0 <= 0 /\ nodecount^0 >= 0 /\ edgecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0
New rule:
l7 -> l17 : h^0'=edgecount^0, j^0'=nodecount^0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ nodecount^0 >= 0 /\ edgecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0

Applied chaining
First rule:
l7 -> l22 : h^0'=edgecount^0, (1-edgecount^0+k_1^0 <= 0 /\ edgecount^0 >= 0), cost: 2+4*edgecount^0
Second rule:
l22 -> l17 : j^0'=nodecount^0, sourceflag^0'=1, (-1+nodecount^0 >= 0 /\ -h^0+edgecount^0 <= 0), cost: 2+4*nodecount^0
New rule:
l7 -> l17 : h^0'=edgecount^0, j^0'=nodecount^0, sourceflag^0'=1, (0 <= 0 /\ 1-edgecount^0+k_1^0 <= 0 /\ -1+nodecount^0 >= 0 /\ edgecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0

Applied simplification
Original rule:
l7 -> l17 : h^0'=edgecount^0, j^0'=nodecount^0, sourceflag^0'=1, (0 <= 0 /\ 1-edgecount^0+k_1^0 <= 0 /\ -1+nodecount^0 >= 0 /\ edgecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0
New rule:
l7 -> l17 : h^0'=edgecount^0, j^0'=nodecount^0, sourceflag^0'=1, (1-edgecount^0+k_1^0 <= 0 /\ -1+nodecount^0 >= 0 /\ edgecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0

Applied deletion
Removed the following rules: 99 100 157 158 159 160

Eliminating location l13 by chaining:

Applied chaining
First rule:
l17 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 2
Second rule:
l13 -> l6 : (nodecount^0-j^0 <= 0 /\ -1+sourceflag^0 >= 0), cost: 3
New rule:
l17 -> l6 : destflag^0'=1, j^0'=0, (nodecount^0-j^0 <= 0 /\ nodecount^0 <= 0 /\ -1+sourceflag^0 >= 0), cost: 5

Applied chaining
First rule:
l17 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 2
Second rule:
l13 -> l6 : (nodecount^0-j^0 <= 0 /\ 1+sourceflag^0 <= 0), cost: 3
New rule:
l17 -> l6 : destflag^0'=1, j^0'=0, (nodecount^0-j^0 <= 0 /\ nodecount^0 <= 0 /\ 1+sourceflag^0 <= 0), cost: 5

Applied chaining
First rule:
l17 -> l13 : destflag^0'=1, j^0'=0, nodecount^0-j^0 <= 0, cost: 2
Second rule:
l13 -> l6 : (nodecount^0-j^0 <= 0 /\ -1+destflag^0 >= 0 /\ sourceflag^0 == 0), cost: 4
New rule:
l17 -> l6 : destflag^0'=1, j^0'=0, (0 >= 0 /\ nodecount^0-j^0 <= 0 /\ nodecount^0 <= 0 /\ sourceflag^0 == 0), cost: 6

Applied simplification
Original rule:
l17 -> l6 : destflag^0'=1, j^0'=0, (0 >= 0 /\ nodecount^0-j^0 <= 0 /\ nodecount^0 <= 0 /\ sourceflag^0 == 0), cost: 6
New rule:
l17 -> l6 : destflag^0'=1, j^0'=0, (nodecount^0-j^0 <= 0 /\ nodecount^0 <= 0 /\ sourceflag^0 == 0), cost: 6

Applied chaining
First rule:
l17 -> l13 : destflag^0'=1, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0), cost: 2+4*nodecount^0
Second rule:
l13 -> l6 : (nodecount^0-j^0 <= 0 /\ -1+sourceflag^0 >= 0), cost: 3
New rule:
l17 -> l6 : destflag^0'=1, j^0'=nodecount^0, (0 <= 0 /\ nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0 /\ -1+sourceflag^0 >= 0), cost: 5+4*nodecount^0

Applied simplification
Original rule:
l17 -> l6 : destflag^0'=1, j^0'=nodecount^0, (0 <= 0 /\ nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0 /\ -1+sourceflag^0 >= 0), cost: 5+4*nodecount^0
New rule:
l17 -> l6 : destflag^0'=1, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0 /\ -1+sourceflag^0 >= 0), cost: 5+4*nodecount^0

Applied chaining
First rule:
l17 -> l13 : destflag^0'=1, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0), cost: 2+4*nodecount^0
Second rule:
l13 -> l6 : (nodecount^0-j^0 <= 0 /\ 1+sourceflag^0 <= 0), cost: 3
New rule:
l17 -> l6 : destflag^0'=1, j^0'=nodecount^0, (0 <= 0 /\ nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0 /\ 1+sourceflag^0 <= 0), cost: 5+4*nodecount^0

Applied simplification
Original rule:
l17 -> l6 : destflag^0'=1, j^0'=nodecount^0, (0 <= 0 /\ nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0 /\ 1+sourceflag^0 <= 0), cost: 5+4*nodecount^0
New rule:
l17 -> l6 : destflag^0'=1, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0 /\ 1+sourceflag^0 <= 0), cost: 5+4*nodecount^0

Applied chaining
First rule:
l17 -> l13 : destflag^0'=1, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0), cost: 2+4*nodecount^0
Second rule:
l13 -> l6 : (nodecount^0-j^0 <= 0 /\ -1+destflag^0 >= 0 /\ sourceflag^0 == 0), cost: 4
New rule:
l17 -> l6 : destflag^0'=1, j^0'=nodecount^0, (0 <= 0 /\ 0 >= 0 /\ nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0 /\ sourceflag^0 == 0), cost: 6+4*nodecount^0

Applied simplification
Original rule:
l17 -> l6 : destflag^0'=1, j^0'=nodecount^0, (0 <= 0 /\ 0 >= 0 /\ nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0 /\ sourceflag^0 == 0), cost: 6+4*nodecount^0
New rule:
l17 -> l6 : destflag^0'=1, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0 /\ sourceflag^0 == 0), cost: 6+4*nodecount^0

Applied chaining
First rule:
l17 -> l13 : destflag^0'=0, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 2+4*nodecount^0
Second rule:
l13 -> l6 : (nodecount^0-j^0 <= 0 /\ -1+sourceflag^0 >= 0), cost: 3
New rule:
l17 -> l6 : destflag^0'=0, j^0'=nodecount^0, (0 <= 0 /\ nodecount^0-j^0 <= 0 /\ -1+sourceflag^0 >= 0 /\ -1+nodecount^0 >= 0), cost: 5+4*nodecount^0

Applied simplification
Original rule:
l17 -> l6 : destflag^0'=0, j^0'=nodecount^0, (0 <= 0 /\ nodecount^0-j^0 <= 0 /\ -1+sourceflag^0 >= 0 /\ -1+nodecount^0 >= 0), cost: 5+4*nodecount^0
New rule:
l17 -> l6 : destflag^0'=0, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ -1+sourceflag^0 >= 0 /\ -1+nodecount^0 >= 0), cost: 5+4*nodecount^0

Applied chaining
First rule:
l17 -> l13 : destflag^0'=0, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 2+4*nodecount^0
Second rule:
l13 -> l6 : (nodecount^0-j^0 <= 0 /\ 1+sourceflag^0 <= 0), cost: 3
New rule:
l17 -> l6 : destflag^0'=0, j^0'=nodecount^0, (0 <= 0 /\ nodecount^0-j^0 <= 0 /\ -1+nodecount^0 >= 0 /\ 1+sourceflag^0 <= 0), cost: 5+4*nodecount^0

Applied simplification
Original rule:
l17 -> l6 : destflag^0'=0, j^0'=nodecount^0, (0 <= 0 /\ nodecount^0-j^0 <= 0 /\ -1+nodecount^0 >= 0 /\ 1+sourceflag^0 <= 0), cost: 5+4*nodecount^0
New rule:
l17 -> l6 : destflag^0'=0, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ -1+nodecount^0 >= 0 /\ 1+sourceflag^0 <= 0), cost: 5+4*nodecount^0

Applied chaining
First rule:
l17 -> l13 : destflag^0'=0, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 2+4*nodecount^0
Second rule:
l13 -> l6 : (nodecount^0-j^0 <= 0 /\ destflag^0 == 0 /\ sourceflag^0 == 0), cost: 4
New rule:
l17 -> l6 : destflag^0'=0, j^0'=nodecount^0, (0 <= 0 /\ 0 == 0 /\ nodecount^0-j^0 <= 0 /\ -1+nodecount^0 >= 0 /\ sourceflag^0 == 0), cost: 6+4*nodecount^0

Applied simplification
Original rule:
l17 -> l6 : destflag^0'=0, j^0'=nodecount^0, (0 <= 0 /\ 0 == 0 /\ nodecount^0-j^0 <= 0 /\ -1+nodecount^0 >= 0 /\ sourceflag^0 == 0), cost: 6+4*nodecount^0
New rule:
l17 -> l6 : destflag^0'=0, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ -1+nodecount^0 >= 0 /\ sourceflag^0 == 0), cost: 6+4*nodecount^0

Applied partial deletion
Original rule:
l17 -> l13 : destflag^0'=1, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0), cost: 2+4*nodecount^0
New rule:
l17 -> [35] : (nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0), cost: 2+4*nodecount^0

Applied partial deletion
Original rule:
l17 -> l13 : destflag^0'=0, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 2+4*nodecount^0
New rule:
l17 -> [35] : (nodecount^0-j^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 2+4*nodecount^0

Applied deletion
Removed the following rules: 102 136 137 138 139 140 155 156

Eliminated locations on tree-shaped paths
Start location: l28
 165: l4 -> l7 : i^0'=0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0), cost: 5
 166: l4 -> l7 : i^0'=edgecount^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 >= 0), cost: 5+2*edgecount^0
 167: l4 -> l7 : i^0'=0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 <= 0), cost: 5
 168: l4 -> l7 : i^0'=edgecount^0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 >= 0), cost: 5+2*edgecount^0
  49: l6 -> l7 : k_1^0'=1+k_1^0, TRUE, cost: 1
  98: l7 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 2
 169: l7 -> l17 : h^0'=0, j^0'=0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ edgecount^0 <= 0), cost: 4
 170: l7 -> l17 : h^0'=0, j^0'=nodecount^0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ nodecount^0 >= 0 /\ edgecount^0 <= 0), cost: 4+4*nodecount^0
 171: l7 -> l17 : h^0'=0, j^0'=nodecount^0, sourceflag^0'=1, (1-edgecount^0+k_1^0 <= 0 /\ -1+nodecount^0 >= 0 /\ edgecount^0 <= 0), cost: 4+4*nodecount^0
 172: l7 -> l17 : h^0'=edgecount^0, min^0'=-1+edgecount^0, j^0'=0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ -1+edgecount^0 >= 0), cost: 4+4*edgecount^0
 173: l7 -> l17 : h^0'=edgecount^0, min^0'=-1+edgecount^0, j^0'=nodecount^0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ nodecount^0 >= 0 /\ -1+edgecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0
 174: l7 -> l17 : h^0'=edgecount^0, min^0'=-1+edgecount^0, j^0'=nodecount^0, sourceflag^0'=1, (1-edgecount^0+k_1^0 <= 0 /\ -1+edgecount^0 >= 0 /\ -1+nodecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0
 175: l7 -> l17 : h^0'=edgecount^0, j^0'=0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ edgecount^0 >= 0), cost: 4+4*edgecount^0
 176: l7 -> l17 : h^0'=edgecount^0, j^0'=nodecount^0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ nodecount^0 >= 0 /\ edgecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0
 177: l7 -> l17 : h^0'=edgecount^0, j^0'=nodecount^0, sourceflag^0'=1, (1-edgecount^0+k_1^0 <= 0 /\ -1+nodecount^0 >= 0 /\ edgecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0
 178: l17 -> l6 : destflag^0'=1, j^0'=0, (nodecount^0-j^0 <= 0 /\ nodecount^0 <= 0 /\ -1+sourceflag^0 >= 0), cost: 5
 179: l17 -> l6 : destflag^0'=1, j^0'=0, (nodecount^0-j^0 <= 0 /\ nodecount^0 <= 0 /\ 1+sourceflag^0 <= 0), cost: 5
 180: l17 -> l6 : destflag^0'=1, j^0'=0, (nodecount^0-j^0 <= 0 /\ nodecount^0 <= 0 /\ sourceflag^0 == 0), cost: 6
 181: l17 -> l6 : destflag^0'=1, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0 /\ -1+sourceflag^0 >= 0), cost: 5+4*nodecount^0
 182: l17 -> l6 : destflag^0'=1, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0 /\ 1+sourceflag^0 <= 0), cost: 5+4*nodecount^0
 183: l17 -> l6 : destflag^0'=1, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0 /\ sourceflag^0 == 0), cost: 6+4*nodecount^0
 184: l17 -> l6 : destflag^0'=0, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ -1+sourceflag^0 >= 0 /\ -1+nodecount^0 >= 0), cost: 5+4*nodecount^0
 185: l17 -> l6 : destflag^0'=0, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ -1+nodecount^0 >= 0 /\ 1+sourceflag^0 <= 0), cost: 5+4*nodecount^0
 186: l17 -> l6 : destflag^0'=0, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ -1+nodecount^0 >= 0 /\ sourceflag^0 == 0), cost: 6+4*nodecount^0
 187: l17 -> [35] : (nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0), cost: 2+4*nodecount^0
 188: l17 -> [35] : (nodecount^0-j^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 2+4*nodecount^0
 161: l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 6
 162: l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0
 163: l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0
 164: l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2+4*nodecount^0


Applied pruning (of leafs and parallel rules):
Start location: l28
 165: l4 -> l7 : i^0'=0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0), cost: 5
 166: l4 -> l7 : i^0'=edgecount^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 >= 0), cost: 5+2*edgecount^0
 167: l4 -> l7 : i^0'=0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 <= 0), cost: 5
 168: l4 -> l7 : i^0'=edgecount^0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 >= 0), cost: 5+2*edgecount^0
  49: l6 -> l7 : k_1^0'=1+k_1^0, TRUE, cost: 1
  98: l7 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 2
 169: l7 -> l17 : h^0'=0, j^0'=0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ edgecount^0 <= 0), cost: 4
 170: l7 -> l17 : h^0'=0, j^0'=nodecount^0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ nodecount^0 >= 0 /\ edgecount^0 <= 0), cost: 4+4*nodecount^0
 172: l7 -> l17 : h^0'=edgecount^0, min^0'=-1+edgecount^0, j^0'=0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ -1+edgecount^0 >= 0), cost: 4+4*edgecount^0
 173: l7 -> l17 : h^0'=edgecount^0, min^0'=-1+edgecount^0, j^0'=nodecount^0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ nodecount^0 >= 0 /\ -1+edgecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0
 175: l7 -> l17 : h^0'=edgecount^0, j^0'=0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ edgecount^0 >= 0), cost: 4+4*edgecount^0
 178: l17 -> l6 : destflag^0'=1, j^0'=0, (nodecount^0-j^0 <= 0 /\ nodecount^0 <= 0 /\ -1+sourceflag^0 >= 0), cost: 5
 179: l17 -> l6 : destflag^0'=1, j^0'=0, (nodecount^0-j^0 <= 0 /\ nodecount^0 <= 0 /\ 1+sourceflag^0 <= 0), cost: 5
 181: l17 -> l6 : destflag^0'=1, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0 /\ -1+sourceflag^0 >= 0), cost: 5+4*nodecount^0
 182: l17 -> l6 : destflag^0'=1, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ nodecount^0 >= 0 /\ 1+sourceflag^0 <= 0), cost: 5+4*nodecount^0
 184: l17 -> l6 : destflag^0'=0, j^0'=nodecount^0, (nodecount^0-j^0 <= 0 /\ -1+sourceflag^0 >= 0 /\ -1+nodecount^0 >= 0), cost: 5+4*nodecount^0
 161: l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 6
 162: l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0
 163: l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0
 164: l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2+4*nodecount^0


Eliminating location l17 by chaining:

Applied partial deletion
Original rule:
l7 -> l17 : h^0'=0, j^0'=nodecount^0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ nodecount^0 >= 0 /\ edgecount^0 <= 0), cost: 4+4*nodecount^0
New rule:
l7 -> [36] : (1-edgecount^0+k_1^0 <= 0 /\ nodecount^0 >= 0 /\ edgecount^0 <= 0), cost: 4+4*nodecount^0

Applied partial deletion
Original rule:
l7 -> l17 : h^0'=edgecount^0, min^0'=-1+edgecount^0, j^0'=0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ -1+edgecount^0 >= 0), cost: 4+4*edgecount^0
New rule:
l7 -> [36] : (1-edgecount^0+k_1^0 <= 0 /\ -1+edgecount^0 >= 0), cost: 4+4*edgecount^0

Applied partial deletion
Original rule:
l7 -> l17 : h^0'=edgecount^0, min^0'=-1+edgecount^0, j^0'=nodecount^0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ nodecount^0 >= 0 /\ -1+edgecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0
New rule:
l7 -> [36] : (1-edgecount^0+k_1^0 <= 0 /\ nodecount^0 >= 0 /\ -1+edgecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0

Applied partial deletion
Original rule:
l7 -> l17 : h^0'=edgecount^0, j^0'=0, sourceflag^0'=0, (1-edgecount^0+k_1^0 <= 0 /\ edgecount^0 >= 0), cost: 4+4*edgecount^0
New rule:
l7 -> [36] : (1-edgecount^0+k_1^0 <= 0 /\ edgecount^0 >= 0), cost: 4+4*edgecount^0

Applied deletion
Removed the following rules: 169 170 172 173 175 178 179 181 182 184

Eliminated locations on tree-shaped paths
Start location: l28
 165: l4 -> l7 : i^0'=0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0), cost: 5
 166: l4 -> l7 : i^0'=edgecount^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 >= 0), cost: 5+2*edgecount^0
 167: l4 -> l7 : i^0'=0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 <= 0), cost: 5
 168: l4 -> l7 : i^0'=edgecount^0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 >= 0), cost: 5+2*edgecount^0
  49: l6 -> l7 : k_1^0'=1+k_1^0, TRUE, cost: 1
  98: l7 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 2
 189: l7 -> [36] : (1-edgecount^0+k_1^0 <= 0 /\ nodecount^0 >= 0 /\ edgecount^0 <= 0), cost: 4+4*nodecount^0
 190: l7 -> [36] : (1-edgecount^0+k_1^0 <= 0 /\ -1+edgecount^0 >= 0), cost: 4+4*edgecount^0
 191: l7 -> [36] : (1-edgecount^0+k_1^0 <= 0 /\ nodecount^0 >= 0 /\ -1+edgecount^0 >= 0), cost: 4+4*nodecount^0+4*edgecount^0
 192: l7 -> [36] : (1-edgecount^0+k_1^0 <= 0 /\ edgecount^0 >= 0), cost: 4+4*edgecount^0
 161: l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 6
 162: l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0
 163: l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0
 164: l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2+4*nodecount^0


Applied pruning (of leafs and parallel rules):
Start location: l28
 165: l4 -> l7 : i^0'=0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0), cost: 5
 166: l4 -> l7 : i^0'=edgecount^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 >= 0), cost: 5+2*edgecount^0
 167: l4 -> l7 : i^0'=0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 <= 0), cost: 5
 168: l4 -> l7 : i^0'=edgecount^0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 >= 0), cost: 5+2*edgecount^0
  98: l7 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 2
 161: l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 6
 162: l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0
 163: l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0
 164: l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2+4*nodecount^0


Eliminating location l7 by chaining:

Applied chaining
First rule:
l4 -> l7 : i^0'=0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0), cost: 5
Second rule:
l7 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 2
New rule:
l4 -> l4 : i^0'=0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0), cost: 7

Applied chaining
First rule:
l4 -> l7 : i^0'=edgecount^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 >= 0), cost: 5+2*edgecount^0
Second rule:
l7 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 2
New rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0), cost: 7+2*edgecount^0

Applied chaining
First rule:
l4 -> l7 : i^0'=0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 <= 0), cost: 5
Second rule:
l7 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 2
New rule:
l4 -> l4 : i^0'=0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 <= 0), cost: 7

Applied chaining
First rule:
l4 -> l7 : i^0'=edgecount^0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 >= 0), cost: 5+2*edgecount^0
Second rule:
l7 -> l4 : k^0'=1+k^0, edgecount^0-k_1^0 <= 0, cost: 2
New rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0), cost: 7+2*edgecount^0

Applied deletion
Removed the following rules: 98 165 166 167 168

Eliminated locations on tree-shaped paths
Start location: l28
 193: l4 -> l4 : i^0'=0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0), cost: 7
 194: l4 -> l4 : i^0'=edgecount^0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0), cost: 7+2*edgecount^0
 195: l4 -> l4 : i^0'=0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 <= 0), cost: 7
 196: l4 -> l4 : i^0'=edgecount^0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0), cost: 7+2*edgecount^0
 161: l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 6
 162: l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0
 163: l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0
 164: l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2+4*nodecount^0


Applied simplification
Original rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0), cost: 7+2*edgecount^0
New rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 == 0), cost: 7+2*edgecount^0

Applied simplification
Original rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0), cost: 7+2*edgecount^0
New rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 == 0), cost: 7+2*edgecount^0

Simplified simple loops
Start location: l28
 193: l4 -> l4 : i^0'=0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0), cost: 7
 195: l4 -> l4 : i^0'=0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 <= 0), cost: 7
 197: l4 -> l4 : i^0'=edgecount^0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 == 0), cost: 7+2*edgecount^0
 198: l4 -> l4 : i^0'=edgecount^0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 == 0), cost: 7+2*edgecount^0
 161: l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 6
 162: l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0
 163: l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0
 164: l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2+4*nodecount^0


Applied nonterm
Original rule:
l4 -> l4 : i^0'=0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0), cost: 7
New rule:
l4 -> [37] : (-edgecount^0 >= 0 /\ -1+n20 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ajEjPI.txt

Applied acceleration
Original rule:
l4 -> l4 : i^0'=0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 <= 0), cost: 7
New rule:
l4 -> l4 : i^0'=0, k^0'=n21+k^0, min^0'=0, k_1^0'=0, (-edgecount^0 >= 0 /\ -1-n21+nodecount^0-k^0 >= 0 /\ -1+n21 >= 0), cost: 7*n21
Sub-proof via acceration calculus written to file:///tmp/tmpnam_hpBfMO.txt

Applied instantiation
Original rule:
l4 -> l4 : i^0'=0, k^0'=n21+k^0, min^0'=0, k_1^0'=0, (-edgecount^0 >= 0 /\ -1-n21+nodecount^0-k^0 >= 0 /\ -1+n21 >= 0), cost: 7*n21
New rule:
l4 -> l4 : i^0'=0, k^0'=-1+nodecount^0, min^0'=0, k_1^0'=0, (0 >= 0 /\ -edgecount^0 >= 0 /\ -2+nodecount^0-k^0 >= 0), cost: -7+7*nodecount^0-7*k^0

Applied nonterm
Original rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 == 0), cost: 7+2*edgecount^0
New rule:
l4 -> [37] : (-1+n22 >= 0 /\ -edgecount^0 >= 0 /\ edgecount^0 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_dmpHLk.txt

Applied acceleration
Original rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (2-nodecount^0+k^0 <= 0 /\ edgecount^0 == 0), cost: 7+2*edgecount^0
New rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=k^0+n23, min^0'=0, k_1^0'=0, (-1+n23 >= 0 /\ -edgecount^0 >= 0 /\ -1+nodecount^0-k^0-n23 >= 0 /\ edgecount^0 >= 0), cost: 2*n23*edgecount^0+7*n23
Sub-proof via acceration calculus written to file:///tmp/tmpnam_obiBda.txt

Applied instantiation
Original rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=k^0+n23, min^0'=0, k_1^0'=0, (-1+n23 >= 0 /\ -edgecount^0 >= 0 /\ -1+nodecount^0-k^0-n23 >= 0 /\ edgecount^0 >= 0), cost: 2*n23*edgecount^0+7*n23
New rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=-1+nodecount^0, min^0'=0, k_1^0'=0, (0 >= 0 /\ -edgecount^0 >= 0 /\ -2+nodecount^0-k^0 >= 0 /\ edgecount^0 >= 0), cost: -7+7*nodecount^0-7*k^0+2*(-1+nodecount^0-k^0)*edgecount^0

Applied chaining
First rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 == 0), cost: 7+2*edgecount^0
Second rule:
l4 -> l4 : i^0'=0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0), cost: 7
New rule:
l4 -> l4 : i^0'=0, k^0'=2+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 == 0), cost: 14+2*edgecount^0

Applied nonterm
Original rule:
l4 -> l4 : i^0'=0, k^0'=2+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 == 0), cost: 14+2*edgecount^0
New rule:
l4 -> [37] : (-1+n25 >= 0 /\ -edgecount^0 >= 0 /\ edgecount^0 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_AlNELH.txt

Applied chaining
First rule:
l4 -> l4 : i^0'=0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0), cost: 7
Second rule:
l4 -> [37] : (-1+n25 >= 0 /\ -edgecount^0 >= 0 /\ edgecount^0 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM
New rule:
l4 -> [37] : (-1+n25 >= 0 /\ -edgecount^0 >= 0 /\ nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0 /\ 1-nodecount^0+k^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l4 -> l4 : i^0'=0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0), cost: 7
Second rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 == 0), cost: 7+2*edgecount^0
New rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=2+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 == 0), cost: 14+2*edgecount^0

Applied nonterm
Original rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=2+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 == 0), cost: 14+2*edgecount^0
New rule:
l4 -> [37] : (-edgecount^0 >= 0 /\ -1+n27 >= 0 /\ edgecount^0 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_lKMiFE.txt

Applied chaining
First rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=1+k^0, min^0'=0, k_1^0'=0, (nodecount^0-k^0 <= 0 /\ edgecount^0 == 0), cost: 7+2*edgecount^0
Second rule:
l4 -> [37] : (-edgecount^0 >= 0 /\ -1+n27 >= 0 /\ edgecount^0 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM
New rule:
l4 -> [37] : (-edgecount^0 >= 0 /\ nodecount^0-k^0 <= 0 /\ -1+n27 >= 0 /\ edgecount^0 >= 0 /\ edgecount^0 == 0 /\ 1-nodecount^0+k^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [37] : (-edgecount^0 >= 0 /\ -1+n20 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM
New rule:
l4 -> [37] : (-1+n20 >= 0 /\ edgecount^0 <= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> l4 : i^0'=0, k^0'=-1+nodecount^0, min^0'=0, k_1^0'=0, (0 >= 0 /\ -edgecount^0 >= 0 /\ -2+nodecount^0-k^0 >= 0), cost: -7+7*nodecount^0-7*k^0
New rule:
l4 -> l4 : i^0'=0, k^0'=-1+nodecount^0, min^0'=0, k_1^0'=0, (-2+nodecount^0-k^0 >= 0 /\ edgecount^0 <= 0), cost: -7+7*nodecount^0-7*k^0

Applied simplification
Original rule:
l4 -> [37] : (-1+n22 >= 0 /\ -edgecount^0 >= 0 /\ edgecount^0 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM
New rule:
l4 -> [37] : (-1+n22 >= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=-1+nodecount^0, min^0'=0, k_1^0'=0, (0 >= 0 /\ -edgecount^0 >= 0 /\ -2+nodecount^0-k^0 >= 0 /\ edgecount^0 >= 0), cost: -7+7*nodecount^0-7*k^0+2*(-1+nodecount^0-k^0)*edgecount^0
New rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=-1+nodecount^0, min^0'=0, k_1^0'=0, (-2+nodecount^0-k^0 >= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0), cost: -7+7*nodecount^0-7*k^0+2*(-1+nodecount^0-k^0)*edgecount^0

Applied simplification
Original rule:
l4 -> [37] : (-1+n25 >= 0 /\ -edgecount^0 >= 0 /\ edgecount^0 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM
New rule:
l4 -> [37] : (-1+n25 >= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [37] : (-1+n25 >= 0 /\ -edgecount^0 >= 0 /\ nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0 /\ 1-nodecount^0+k^0 >= 0), cost: NONTERM
New rule:
l4 -> [37] : (-1+n25 >= 0 /\ nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [37] : (-edgecount^0 >= 0 /\ -1+n27 >= 0 /\ edgecount^0 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM
New rule:
l4 -> [37] : (-1+n27 >= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l4 -> [37] : (-edgecount^0 >= 0 /\ nodecount^0-k^0 <= 0 /\ -1+n27 >= 0 /\ edgecount^0 >= 0 /\ edgecount^0 == 0 /\ 1-nodecount^0+k^0 >= 0), cost: NONTERM
New rule:
l4 -> [37] : (nodecount^0-k^0 <= 0 /\ -1+n27 >= 0 /\ edgecount^0 == 0), cost: NONTERM

Applied deletion
Removed the following rules: 193 195 197 198

Accelerated simple loops
Start location: l28
 207: l4 -> [37] : (-1+n20 >= 0 /\ edgecount^0 <= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM
 208: l4 -> l4 : i^0'=0, k^0'=-1+nodecount^0, min^0'=0, k_1^0'=0, (-2+nodecount^0-k^0 >= 0 /\ edgecount^0 <= 0), cost: -7+7*nodecount^0-7*k^0
 209: l4 -> [37] : (-1+n22 >= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM
 210: l4 -> l4 : i^0'=edgecount^0, k^0'=-1+nodecount^0, min^0'=0, k_1^0'=0, (-2+nodecount^0-k^0 >= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0), cost: -7+7*nodecount^0-7*k^0+2*(-1+nodecount^0-k^0)*edgecount^0
 211: l4 -> [37] : (-1+n25 >= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM
 212: l4 -> [37] : (-1+n25 >= 0 /\ nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0), cost: NONTERM
 213: l4 -> [37] : (-1+n27 >= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM
 214: l4 -> [37] : (nodecount^0-k^0 <= 0 /\ -1+n27 >= 0 /\ edgecount^0 == 0), cost: NONTERM
 161: l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 6
 162: l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0
 163: l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0
 164: l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2+4*nodecount^0


Applied chaining
First rule:
l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 6
Second rule:
l4 -> [37] : (-1+n20 >= 0 /\ edgecount^0 <= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM
New rule:
l28 -> [37] : (nodecount^0 <= 0 /\ edgecount^0 <= 0), cost: NONTERM

Applied chaining
First rule:
l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2+4*nodecount^0
Second rule:
l4 -> l4 : i^0'=0, k^0'=-1+nodecount^0, min^0'=0, k_1^0'=0, (-2+nodecount^0-k^0 >= 0 /\ edgecount^0 <= 0), cost: -7+7*nodecount^0-7*k^0
New rule:
l28 -> l4 : i^0'=0, k^0'=-1+nodecount^0, __lengthofvisited^0'=edgecount^0, min^0'=0, k_1^0'=0, (-2+nodecount^0 >= 0 /\ edgecount^0 <= 0), cost: -5+11*nodecount^0

Applied chaining
First rule:
l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 6
Second rule:
l4 -> [37] : (-1+n22 >= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM
New rule:
l28 -> [37] : (nodecount^0 <= 0 /\ edgecount^0 == 0), cost: NONTERM

Applied chaining
First rule:
l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2+4*nodecount^0
Second rule:
l4 -> l4 : i^0'=edgecount^0, k^0'=-1+nodecount^0, min^0'=0, k_1^0'=0, (-2+nodecount^0-k^0 >= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0), cost: -7+7*nodecount^0-7*k^0+2*(-1+nodecount^0-k^0)*edgecount^0
New rule:
l28 -> l4 : i^0'=edgecount^0, k^0'=-1+nodecount^0, __lengthofvisited^0'=edgecount^0, min^0'=0, k_1^0'=0, (-2+nodecount^0 >= 0 /\ edgecount^0 == 0), cost: -5+11*nodecount^0+2*(-1+nodecount^0)*edgecount^0

Applied chaining
First rule:
l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 6
Second rule:
l4 -> [37] : (-1+n25 >= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM
New rule:
l28 -> [37] : (nodecount^0 <= 0 /\ edgecount^0 == 0), cost: NONTERM

Applied chaining
First rule:
l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 6
Second rule:
l4 -> [37] : (-1+n25 >= 0 /\ nodecount^0-k^0 <= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0), cost: NONTERM
New rule:
l28 -> [37] : (nodecount^0 <= 0 /\ edgecount^0 == 0), cost: NONTERM

Applied chaining
First rule:
l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 6
Second rule:
l4 -> [37] : (-1+n27 >= 0 /\ edgecount^0 <= 0 /\ edgecount^0 >= 0 /\ -nodecount^0+k^0 >= 0), cost: NONTERM
New rule:
l28 -> [37] : (nodecount^0 <= 0 /\ edgecount^0 == 0), cost: NONTERM

Applied chaining
First rule:
l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 6
Second rule:
l4 -> [37] : (nodecount^0-k^0 <= 0 /\ -1+n27 >= 0 /\ edgecount^0 == 0), cost: NONTERM
New rule:
l28 -> [37] : (nodecount^0 <= 0 /\ edgecount^0 == 0), cost: NONTERM

Applied deletion
Removed the following rules: 207 208 209 210 211 212 213 214

Chained accelerated rules with incoming rules
Start location: l28
 161: l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 <= 0, cost: 6
 162: l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0
 163: l28 -> l4 : i^0'=0, k^0'=0, __lengthofvisited^0'=edgecount^0, (-1+nodecount^0 <= 0 /\ -1+nodecount^0 >= 0), cost: 4+2*nodecount^0
 164: l28 -> l4 : i^0'=-1+nodecount^0, k^0'=0, __lengthofvisited^0'=edgecount^0, -1+nodecount^0 >= 0, cost: 2+4*nodecount^0
 215: l28 -> [37] : (nodecount^0 <= 0 /\ edgecount^0 <= 0), cost: NONTERM
 216: l28 -> l4 : i^0'=0, k^0'=-1+nodecount^0, __lengthofvisited^0'=edgecount^0, min^0'=0, k_1^0'=0, (-2+nodecount^0 >= 0 /\ edgecount^0 <= 0), cost: -5+11*nodecount^0
 217: l28 -> [37] : (nodecount^0 <= 0 /\ edgecount^0 == 0), cost: NONTERM
 218: l28 -> l4 : i^0'=edgecount^0, k^0'=-1+nodecount^0, __lengthofvisited^0'=edgecount^0, min^0'=0, k_1^0'=0, (-2+nodecount^0 >= 0 /\ edgecount^0 == 0), cost: -5+11*nodecount^0+2*(-1+nodecount^0)*edgecount^0


Removed unreachable locations and irrelevant leafs
Start location: l28
 215: l28 -> [37] : (nodecount^0 <= 0 /\ edgecount^0 <= 0), cost: NONTERM
 217: l28 -> [37] : (nodecount^0 <= 0 /\ edgecount^0 == 0), cost: NONTERM


Computing asymptotic complexity
Proved nontermination of rule 215 via SMT.

Proved the following lower bound
Complexity:  Nonterm
Cpx degree: Nonterm

Solved cost: NONTERM
Rule cost:   NONTERM
Rule guard:  (nodecount^0 <= 0 /\ edgecount^0 <= 0)