WORST_CASE(Omega(0),?)

Initial ITS
Start location: l8
   0: l0 -> l1 : seed^0'=seed^post0, z117^0'=z117^post0, tmp38^0'=tmp38^post0, __const_7^0'=__const_7^post0, tmp510^0'=tmp510^post0, tmp1316^0'=tmp1316^post0, z319^0'=z319^post0, tmp1013^0'=tmp1013^post0, i^0'=i^post0, tmp712^0'=tmp712^post0, tmp27^0'=tmp27^post0, z521^0'=z521^post0, __const_64^0'=__const_64^post0, tmp1215^0'=tmp1215^post0, tmp05^0'=tmp05^post0, z218^0'=z218^post0, tmp49^0'=tmp49^post0, ctr23^0'=ctr23^post0, tmp611^0'=tmp611^post0, tmp16^0'=tmp16^post0, z420^0'=z420^post0, tmp1114^0'=tmp1114^post0, (z319^0-z319^post0 == 0 /\ __const_7^0-__const_7^post0 == 0 /\ -tmp27^post0+tmp27^0 == 0 /\ -tmp1114^post0+tmp1114^0 == 0 /\ tmp38^0-tmp38^post0 == 0 /\ tmp16^0-tmp16^post0 == 0 /\ -z420^post0+z420^0 == 0 /\ ctr23^post0-__const_7^0 == 0 /\ -tmp1215^post0+tmp1215^0 == 0 /\ -tmp1013^post0+tmp1013^0 == 0 /\ -tmp05^post0+tmp05^0 == 0 /\ tmp611^0-tmp611^post0 == 0 /\ -i^0+__const_64^0 <= 0 /\ __const_64^0-__const_64^post0 == 0 /\ tmp1316^0-tmp1316^post0 == 0 /\ tmp49^0-tmp49^post0 == 0 /\ -z218^post0+z218^0 == 0 /\ seed^0-seed^post0 == 0 /\ i^0-i^post0 == 0 /\ tmp712^0-tmp712^post0 == 0 /\ -z117^post0+z117^0 == 0 /\ -z521^post0+z521^0 == 0 /\ tmp510^0-tmp510^post0 == 0), cost: 1
   1: l0 -> l2 : seed^0'=seed^post1, z117^0'=z117^post1, tmp38^0'=tmp38^post1, __const_7^0'=__const_7^post1, tmp510^0'=tmp510^post1, tmp1316^0'=tmp1316^post1, z319^0'=z319^post1, tmp1013^0'=tmp1013^post1, i^0'=i^post1, tmp712^0'=tmp712^post1, tmp27^0'=tmp27^post1, z521^0'=z521^post1, __const_64^0'=__const_64^post1, tmp1215^0'=tmp1215^post1, tmp05^0'=tmp05^post1, z218^0'=z218^post1, tmp49^0'=tmp49^post1, ctr23^0'=ctr23^post1, tmp611^0'=tmp611^post1, tmp16^0'=tmp16^post1, z420^0'=z420^post1, tmp1114^0'=tmp1114^post1, (0 == 0 /\ tmp1215^0-tmp1215^post1 == 0 /\ -tmp05^post1+tmp05^0 == 0 /\ -z420^post1+z420^0 == 0 /\ -z521^post1+z521^0 == 0 /\ 1+i^0-__const_64^0 <= 0 /\ -tmp16^post1+tmp16^0 == 0 /\ tmp27^0-tmp27^post1 == 0 /\ -z218^post1+z218^0 == 0 /\ tmp38^0-tmp38^post1 == 0 /\ tmp712^0-tmp712^post1 == 0 /\ -ctr23^post1+ctr23^0 == 0 /\ -tmp611^post1+tmp611^0 == 0 /\ -tmp1114^post1+tmp1114^0 == 0 /\ __const_7^0-__const_7^post1 == 0 /\ tmp49^0-tmp49^post1 == 0 /\ -1+i^post1-i^0 == 0 /\ z117^0-z117^post1 == 0 /\ -tmp510^post1+tmp510^0 == 0 /\ -__const_64^post1+__const_64^0 == 0 /\ tmp1013^0-tmp1013^post1 == 0 /\ z319^0-z319^post1 == 0 /\ -tmp1316^post1+tmp1316^0 == 0), cost: 1
   5: l1 -> l6 : seed^0'=seed^post5, z117^0'=z117^post5, tmp38^0'=tmp38^post5, __const_7^0'=__const_7^post5, tmp510^0'=tmp510^post5, tmp1316^0'=tmp1316^post5, z319^0'=z319^post5, tmp1013^0'=tmp1013^post5, i^0'=i^post5, tmp712^0'=tmp712^post5, tmp27^0'=tmp27^post5, z521^0'=z521^post5, __const_64^0'=__const_64^post5, tmp1215^0'=tmp1215^post5, tmp05^0'=tmp05^post5, z218^0'=z218^post5, tmp49^0'=tmp49^post5, ctr23^0'=ctr23^post5, tmp611^0'=tmp611^post5, tmp16^0'=tmp16^post5, z420^0'=z420^post5, tmp1114^0'=tmp1114^post5, (-z420^post5+z420^0 == 0 /\ -tmp16^post5+tmp16^0 == 0 /\ z319^0-z319^post5 == 0 /\ __const_64^0-__const_64^post5 == 0 /\ -z521^post5+z521^0 == 0 /\ -tmp05^post5+tmp05^0 == 0 /\ -ctr23^post5+ctr23^0 == 0 /\ tmp1316^0-tmp1316^post5 == 0 /\ -tmp611^post5+tmp611^0 == 0 /\ z218^0-z218^post5 == 0 /\ tmp510^0-tmp510^post5 == 0 /\ seed^0-seed^post5 == 0 /\ -tmp1215^post5+tmp1215^0 == 0 /\ tmp38^0-tmp38^post5 == 0 /\ __const_7^0-__const_7^post5 == 0 /\ z117^0-z117^post5 == 0 /\ -tmp27^post5+tmp27^0 == 0 /\ i^0-i^post5 == 0 /\ tmp712^0-tmp712^post5 == 0 /\ tmp1013^0-tmp1013^post5 == 0 /\ -tmp1114^post5+tmp1114^0 == 0 /\ -tmp49^post5+tmp49^0 == 0), cost: 1
   4: l2 -> l0 : seed^0'=seed^post4, z117^0'=z117^post4, tmp38^0'=tmp38^post4, __const_7^0'=__const_7^post4, tmp510^0'=tmp510^post4, tmp1316^0'=tmp1316^post4, z319^0'=z319^post4, tmp1013^0'=tmp1013^post4, i^0'=i^post4, tmp712^0'=tmp712^post4, tmp27^0'=tmp27^post4, z521^0'=z521^post4, __const_64^0'=__const_64^post4, tmp1215^0'=tmp1215^post4, tmp05^0'=tmp05^post4, z218^0'=z218^post4, tmp49^0'=tmp49^post4, ctr23^0'=ctr23^post4, tmp611^0'=tmp611^post4, tmp16^0'=tmp16^post4, z420^0'=z420^post4, tmp1114^0'=tmp1114^post4, (tmp1013^0-tmp1013^post4 == 0 /\ -tmp1114^post4+tmp1114^0 == 0 /\ -tmp49^post4+tmp49^0 == 0 /\ -tmp1215^post4+tmp1215^0 == 0 /\ tmp1316^0-tmp1316^post4 == 0 /\ -tmp16^post4+tmp16^0 == 0 /\ seed^0-seed^post4 == 0 /\ z117^0-z117^post4 == 0 /\ -z420^post4+z420^0 == 0 /\ -tmp712^post4+tmp712^0 == 0 /\ tmp510^0-tmp510^post4 == 0 /\ -tmp611^post4+tmp611^0 == 0 /\ tmp38^0-tmp38^post4 == 0 /\ i^0-i^post4 == 0 /\ z521^0-z521^post4 == 0 /\ -z319^post4+z319^0 == 0 /\ -__const_64^post4+__const_64^0 == 0 /\ __const_7^0-__const_7^post4 == 0 /\ z218^0-z218^post4 == 0 /\ -tmp27^post4+tmp27^0 == 0 /\ -ctr23^post4+ctr23^0 == 0 /\ -tmp05^post4+tmp05^0 == 0), cost: 1
   2: l3 -> l4 : seed^0'=seed^post2, z117^0'=z117^post2, tmp38^0'=tmp38^post2, __const_7^0'=__const_7^post2, tmp510^0'=tmp510^post2, tmp1316^0'=tmp1316^post2, z319^0'=z319^post2, tmp1013^0'=tmp1013^post2, i^0'=i^post2, tmp712^0'=tmp712^post2, tmp27^0'=tmp27^post2, z521^0'=z521^post2, __const_64^0'=__const_64^post2, tmp1215^0'=tmp1215^post2, tmp05^0'=tmp05^post2, z218^0'=z218^post2, tmp49^0'=tmp49^post2, ctr23^0'=ctr23^post2, tmp611^0'=tmp611^post2, tmp16^0'=tmp16^post2, z420^0'=z420^post2, tmp1114^0'=tmp1114^post2, (-z218^post2+z218^0 == 0 /\ z521^0-z521^post2 == 0 /\ seed^0-seed^post2 == 0 /\ -tmp1114^post2+tmp1114^0 == 0 /\ __const_7^0-__const_7^post2 == 0 /\ -tmp49^post2+tmp49^0 == 0 /\ -ctr23^post2+ctr23^0 == 0 /\ tmp27^0-tmp27^post2 == 0 /\ tmp510^0-tmp510^post2 == 0 /\ -tmp712^post2+tmp712^0 == 0 /\ tmp1316^0-tmp1316^post2 == 0 /\ i^0-i^post2 == 0 /\ -z420^post2+z420^0 == 0 /\ 1+ctr23^0 <= 0 /\ tmp1013^0-tmp1013^post2 == 0 /\ -z319^post2+z319^0 == 0 /\ -tmp611^post2+tmp611^0 == 0 /\ tmp05^0-tmp05^post2 == 0 /\ -__const_64^post2+__const_64^0 == 0 /\ -tmp1215^post2+tmp1215^0 == 0 /\ -tmp38^post2+tmp38^0 == 0 /\ -tmp16^post2+tmp16^0 == 0 /\ z117^0-z117^post2 == 0), cost: 1
   3: l3 -> l5 : seed^0'=seed^post3, z117^0'=z117^post3, tmp38^0'=tmp38^post3, __const_7^0'=__const_7^post3, tmp510^0'=tmp510^post3, tmp1316^0'=tmp1316^post3, z319^0'=z319^post3, tmp1013^0'=tmp1013^post3, i^0'=i^post3, tmp712^0'=tmp712^post3, tmp27^0'=tmp27^post3, z521^0'=z521^post3, __const_64^0'=__const_64^post3, tmp1215^0'=tmp1215^post3, tmp05^0'=tmp05^post3, z218^0'=z218^post3, tmp49^0'=tmp49^post3, ctr23^0'=ctr23^post3, tmp611^0'=tmp611^post3, tmp16^0'=tmp16^post3, z420^0'=z420^post3, tmp1114^0'=tmp1114^post3, (0 == 0 /\ i^0-i^post3 == 0 /\ __const_7^0-__const_7^post3 == 0 /\ -tmp49^10-tmp611^10+z319^10 == 0 /\ -tmp510^10-tmp712^10+z420^10 == 0 /\ 1+ctr23^post3-ctr23^0 == 0 /\ seed^0-seed^post3 == 0 /\ tmp27^post3+tmp1215^post3-tmp16^post3 == 0 /\ -tmp49^10+z117^20-tmp712^10 == 0 /\ -ctr23^0 <= 0 /\ -tmp38^post3+tmp1013^post3-tmp05^post3 == 0 /\ -z521^post3-z319^20+z319^post3 == 0 /\ -__const_64^post3+__const_64^0 == 0 /\ z420^post3-z521^post3-z420^20 == 0 /\ -tmp27^post3-tmp16^post3+tmp1114^post3 == 0 /\ tmp38^post3-tmp05^post3+tmp1316^post3 == 0 /\ -tmp510^10-tmp611^10+z218^10 == 0), cost: 1
   6: l5 -> l3 : seed^0'=seed^post6, z117^0'=z117^post6, tmp38^0'=tmp38^post6, __const_7^0'=__const_7^post6, tmp510^0'=tmp510^post6, tmp1316^0'=tmp1316^post6, z319^0'=z319^post6, tmp1013^0'=tmp1013^post6, i^0'=i^post6, tmp712^0'=tmp712^post6, tmp27^0'=tmp27^post6, z521^0'=z521^post6, __const_64^0'=__const_64^post6, tmp1215^0'=tmp1215^post6, tmp05^0'=tmp05^post6, z218^0'=z218^post6, tmp49^0'=tmp49^post6, ctr23^0'=ctr23^post6, tmp611^0'=tmp611^post6, tmp16^0'=tmp16^post6, z420^0'=z420^post6, tmp1114^0'=tmp1114^post6, (-tmp27^post6+tmp27^0 == 0 /\ tmp712^0-tmp712^post6 == 0 /\ tmp16^0-tmp16^post6 == 0 /\ seed^0-seed^post6 == 0 /\ tmp38^0-tmp38^post6 == 0 /\ -tmp1114^post6+tmp1114^0 == 0 /\ __const_7^0-__const_7^post6 == 0 /\ -tmp05^post6+tmp05^0 == 0 /\ -z420^post6+z420^0 == 0 /\ -tmp1013^post6+tmp1013^0 == 0 /\ -i^post6+i^0 == 0 /\ tmp611^0-tmp611^post6 == 0 /\ tmp510^0-tmp510^post6 == 0 /\ __const_64^0-__const_64^post6 == 0 /\ -z218^post6+z218^0 == 0 /\ tmp1316^0-tmp1316^post6 == 0 /\ tmp49^0-tmp49^post6 == 0 /\ z319^0-z319^post6 == 0 /\ -tmp1215^post6+tmp1215^0 == 0 /\ -ctr23^post6+ctr23^0 == 0 /\ z117^0-z117^post6 == 0 /\ -z521^post6+z521^0 == 0), cost: 1
   7: l6 -> l5 : seed^0'=seed^post7, z117^0'=z117^post7, tmp38^0'=tmp38^post7, __const_7^0'=__const_7^post7, tmp510^0'=tmp510^post7, tmp1316^0'=tmp1316^post7, z319^0'=z319^post7, tmp1013^0'=tmp1013^post7, i^0'=i^post7, tmp712^0'=tmp712^post7, tmp27^0'=tmp27^post7, z521^0'=z521^post7, __const_64^0'=__const_64^post7, tmp1215^0'=tmp1215^post7, tmp05^0'=tmp05^post7, z218^0'=z218^post7, tmp49^0'=tmp49^post7, ctr23^0'=ctr23^post7, tmp611^0'=tmp611^post7, tmp16^0'=tmp16^post7, z420^0'=z420^post7, tmp1114^0'=tmp1114^post7, (-tmp1316^post7+tmp1316^0 == 0 /\ -tmp1114^post7+tmp1114^0 == 0 /\ -i^post7+i^0 == 0 /\ tmp27^0-tmp27^post7 == 0 /\ -tmp1013^post7+tmp1013^0 == 0 /\ tmp1215^0-tmp1215^post7 == 0 /\ -z521^post7+z521^0 == 0 /\ -tmp16^post7+tmp16^0 == 0 /\ z117^0-z117^post7 == 0 /\ seed^0-seed^post7 == 0 /\ -z420^post7+z420^0 == 0 /\ tmp712^0-tmp712^post7 == 0 /\ -__const_7^0+ctr23^post7 == 0 /\ tmp49^0-tmp49^post7 == 0 /\ tmp38^0-tmp38^post7 == 0 /\ 1+ctr23^0 <= 0 /\ -tmp510^post7+tmp510^0 == 0 /\ -z218^post7+z218^0 == 0 /\ -__const_64^post7+__const_64^0 == 0 /\ __const_7^0-__const_7^post7 == 0 /\ -tmp611^post7+tmp611^0 == 0 /\ -tmp05^post7+tmp05^0 == 0 /\ z319^0-z319^post7 == 0), cost: 1
   8: l6 -> l1 : seed^0'=seed^post8, z117^0'=z117^post8, tmp38^0'=tmp38^post8, __const_7^0'=__const_7^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=z319^post8, tmp1013^0'=tmp1013^post8, i^0'=i^post8, tmp712^0'=tmp712^post8, tmp27^0'=tmp27^post8, z521^0'=z521^post8, __const_64^0'=__const_64^post8, tmp1215^0'=tmp1215^post8, tmp05^0'=tmp05^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=ctr23^post8, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, (0 == 0 /\ -z420^210-z521^post8+z420^post8 == 0 /\ seed^0-seed^post8 == 0 /\ z218^110-tmp510^110-tmp611^110 == 0 /\ -ctr23^0 <= 0 /\ 1+ctr23^post8-ctr23^0 == 0 /\ -tmp49^11+z117^210-tmp712^110 == 0 /\ -i^post8+i^0 == 0 /\ tmp27^post8-tmp16^post8+tmp1215^post8 == 0 /\ z420^110-tmp712^110-tmp510^110 == 0 /\ z319^110-tmp49^11-tmp611^110 == 0 /\ __const_64^0-__const_64^post8 == 0 /\ __const_7^0-__const_7^post8 == 0 /\ -tmp27^post8-tmp16^post8+tmp1114^post8 == 0 /\ -tmp05^post8+tmp1316^post8+tmp38^post8 == 0 /\ tmp1013^post8-tmp05^post8-tmp38^post8 == 0 /\ -z319^210-z521^post8+z319^post8 == 0), cost: 1
   9: l7 -> l2 : seed^0'=seed^post9, z117^0'=z117^post9, tmp38^0'=tmp38^post9, __const_7^0'=__const_7^post9, tmp510^0'=tmp510^post9, tmp1316^0'=tmp1316^post9, z319^0'=z319^post9, tmp1013^0'=tmp1013^post9, i^0'=i^post9, tmp712^0'=tmp712^post9, tmp27^0'=tmp27^post9, z521^0'=z521^post9, __const_64^0'=__const_64^post9, tmp1215^0'=tmp1215^post9, tmp05^0'=tmp05^post9, z218^0'=z218^post9, tmp49^0'=tmp49^post9, ctr23^0'=ctr23^post9, tmp611^0'=tmp611^post9, tmp16^0'=tmp16^post9, z420^0'=z420^post9, tmp1114^0'=tmp1114^post9, (-z218^post9+z218^0 == 0 /\ z117^0-z117^post9 == 0 /\ -tmp510^post9+tmp510^0 == 0 /\ tmp712^0-tmp712^post9 == 0 /\ tmp16^0-tmp16^post9 == 0 /\ -ctr23^post9+ctr23^0 == 0 /\ i^post9 == 0 /\ -tmp1013^post9+tmp1013^0 == 0 /\ tmp38^0-tmp38^post9 == 0 /\ seed^post9 == 0 /\ __const_64^0-__const_64^post9 == 0 /\ tmp49^0-tmp49^post9 == 0 /\ -tmp1114^post9+tmp1114^0 == 0 /\ -tmp611^post9+tmp611^0 == 0 /\ z319^0-z319^post9 == 0 /\ z420^0-z420^post9 == 0 /\ __const_7^0-__const_7^post9 == 0 /\ -tmp1215^post9+tmp1215^0 == 0 /\ -tmp05^post9+tmp05^0 == 0 /\ tmp1316^0-tmp1316^post9 == 0 /\ -z521^post9+z521^0 == 0 /\ tmp27^0-tmp27^post9 == 0), cost: 1
  10: l8 -> l7 : seed^0'=seed^post10, z117^0'=z117^post10, tmp38^0'=tmp38^post10, __const_7^0'=__const_7^post10, tmp510^0'=tmp510^post10, tmp1316^0'=tmp1316^post10, z319^0'=z319^post10, tmp1013^0'=tmp1013^post10, i^0'=i^post10, tmp712^0'=tmp712^post10, tmp27^0'=tmp27^post10, z521^0'=z521^post10, __const_64^0'=__const_64^post10, tmp1215^0'=tmp1215^post10, tmp05^0'=tmp05^post10, z218^0'=z218^post10, tmp49^0'=tmp49^post10, ctr23^0'=ctr23^post10, tmp611^0'=tmp611^post10, tmp16^0'=tmp16^post10, z420^0'=z420^post10, tmp1114^0'=tmp1114^post10, (-tmp1114^post10+tmp1114^0 == 0 /\ -tmp611^post10+tmp611^0 == 0 /\ -tmp1316^post10+tmp1316^0 == 0 /\ seed^0-seed^post10 == 0 /\ z117^0-z117^post10 == 0 /\ -__const_64^post10+__const_64^0 == 0 /\ -z420^post10+z420^0 == 0 /\ z319^0-z319^post10 == 0 /\ __const_7^0-__const_7^post10 == 0 /\ ctr23^0-ctr23^post10 == 0 /\ -z521^post10+z521^0 == 0 /\ tmp1215^0-tmp1215^post10 == 0 /\ -i^post10+i^0 == 0 /\ -tmp05^post10+tmp05^0 == 0 /\ tmp27^0-tmp27^post10 == 0 /\ tmp1013^0-tmp1013^post10 == 0 /\ tmp510^0-tmp510^post10 == 0 /\ tmp38^0-tmp38^post10 == 0 /\ tmp712^0-tmp712^post10 == 0 /\ -tmp16^post10+tmp16^0 == 0 /\ -z218^post10+z218^0 == 0 /\ tmp49^0-tmp49^post10 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l8
   0: l0 -> l1 : seed^0'=seed^post0, z117^0'=z117^post0, tmp38^0'=tmp38^post0, __const_7^0'=__const_7^post0, tmp510^0'=tmp510^post0, tmp1316^0'=tmp1316^post0, z319^0'=z319^post0, tmp1013^0'=tmp1013^post0, i^0'=i^post0, tmp712^0'=tmp712^post0, tmp27^0'=tmp27^post0, z521^0'=z521^post0, __const_64^0'=__const_64^post0, tmp1215^0'=tmp1215^post0, tmp05^0'=tmp05^post0, z218^0'=z218^post0, tmp49^0'=tmp49^post0, ctr23^0'=ctr23^post0, tmp611^0'=tmp611^post0, tmp16^0'=tmp16^post0, z420^0'=z420^post0, tmp1114^0'=tmp1114^post0, (z319^0-z319^post0 == 0 /\ __const_7^0-__const_7^post0 == 0 /\ -tmp27^post0+tmp27^0 == 0 /\ -tmp1114^post0+tmp1114^0 == 0 /\ tmp38^0-tmp38^post0 == 0 /\ tmp16^0-tmp16^post0 == 0 /\ -z420^post0+z420^0 == 0 /\ ctr23^post0-__const_7^0 == 0 /\ -tmp1215^post0+tmp1215^0 == 0 /\ -tmp1013^post0+tmp1013^0 == 0 /\ -tmp05^post0+tmp05^0 == 0 /\ tmp611^0-tmp611^post0 == 0 /\ -i^0+__const_64^0 <= 0 /\ __const_64^0-__const_64^post0 == 0 /\ tmp1316^0-tmp1316^post0 == 0 /\ tmp49^0-tmp49^post0 == 0 /\ -z218^post0+z218^0 == 0 /\ seed^0-seed^post0 == 0 /\ i^0-i^post0 == 0 /\ tmp712^0-tmp712^post0 == 0 /\ -z117^post0+z117^0 == 0 /\ -z521^post0+z521^0 == 0 /\ tmp510^0-tmp510^post0 == 0), cost: 1
   1: l0 -> l2 : seed^0'=seed^post1, z117^0'=z117^post1, tmp38^0'=tmp38^post1, __const_7^0'=__const_7^post1, tmp510^0'=tmp510^post1, tmp1316^0'=tmp1316^post1, z319^0'=z319^post1, tmp1013^0'=tmp1013^post1, i^0'=i^post1, tmp712^0'=tmp712^post1, tmp27^0'=tmp27^post1, z521^0'=z521^post1, __const_64^0'=__const_64^post1, tmp1215^0'=tmp1215^post1, tmp05^0'=tmp05^post1, z218^0'=z218^post1, tmp49^0'=tmp49^post1, ctr23^0'=ctr23^post1, tmp611^0'=tmp611^post1, tmp16^0'=tmp16^post1, z420^0'=z420^post1, tmp1114^0'=tmp1114^post1, (0 == 0 /\ tmp1215^0-tmp1215^post1 == 0 /\ -tmp05^post1+tmp05^0 == 0 /\ -z420^post1+z420^0 == 0 /\ -z521^post1+z521^0 == 0 /\ 1+i^0-__const_64^0 <= 0 /\ -tmp16^post1+tmp16^0 == 0 /\ tmp27^0-tmp27^post1 == 0 /\ -z218^post1+z218^0 == 0 /\ tmp38^0-tmp38^post1 == 0 /\ tmp712^0-tmp712^post1 == 0 /\ -ctr23^post1+ctr23^0 == 0 /\ -tmp611^post1+tmp611^0 == 0 /\ -tmp1114^post1+tmp1114^0 == 0 /\ __const_7^0-__const_7^post1 == 0 /\ tmp49^0-tmp49^post1 == 0 /\ -1+i^post1-i^0 == 0 /\ z117^0-z117^post1 == 0 /\ -tmp510^post1+tmp510^0 == 0 /\ -__const_64^post1+__const_64^0 == 0 /\ tmp1013^0-tmp1013^post1 == 0 /\ z319^0-z319^post1 == 0 /\ -tmp1316^post1+tmp1316^0 == 0), cost: 1
   5: l1 -> l6 : seed^0'=seed^post5, z117^0'=z117^post5, tmp38^0'=tmp38^post5, __const_7^0'=__const_7^post5, tmp510^0'=tmp510^post5, tmp1316^0'=tmp1316^post5, z319^0'=z319^post5, tmp1013^0'=tmp1013^post5, i^0'=i^post5, tmp712^0'=tmp712^post5, tmp27^0'=tmp27^post5, z521^0'=z521^post5, __const_64^0'=__const_64^post5, tmp1215^0'=tmp1215^post5, tmp05^0'=tmp05^post5, z218^0'=z218^post5, tmp49^0'=tmp49^post5, ctr23^0'=ctr23^post5, tmp611^0'=tmp611^post5, tmp16^0'=tmp16^post5, z420^0'=z420^post5, tmp1114^0'=tmp1114^post5, (-z420^post5+z420^0 == 0 /\ -tmp16^post5+tmp16^0 == 0 /\ z319^0-z319^post5 == 0 /\ __const_64^0-__const_64^post5 == 0 /\ -z521^post5+z521^0 == 0 /\ -tmp05^post5+tmp05^0 == 0 /\ -ctr23^post5+ctr23^0 == 0 /\ tmp1316^0-tmp1316^post5 == 0 /\ -tmp611^post5+tmp611^0 == 0 /\ z218^0-z218^post5 == 0 /\ tmp510^0-tmp510^post5 == 0 /\ seed^0-seed^post5 == 0 /\ -tmp1215^post5+tmp1215^0 == 0 /\ tmp38^0-tmp38^post5 == 0 /\ __const_7^0-__const_7^post5 == 0 /\ z117^0-z117^post5 == 0 /\ -tmp27^post5+tmp27^0 == 0 /\ i^0-i^post5 == 0 /\ tmp712^0-tmp712^post5 == 0 /\ tmp1013^0-tmp1013^post5 == 0 /\ -tmp1114^post5+tmp1114^0 == 0 /\ -tmp49^post5+tmp49^0 == 0), cost: 1
   4: l2 -> l0 : seed^0'=seed^post4, z117^0'=z117^post4, tmp38^0'=tmp38^post4, __const_7^0'=__const_7^post4, tmp510^0'=tmp510^post4, tmp1316^0'=tmp1316^post4, z319^0'=z319^post4, tmp1013^0'=tmp1013^post4, i^0'=i^post4, tmp712^0'=tmp712^post4, tmp27^0'=tmp27^post4, z521^0'=z521^post4, __const_64^0'=__const_64^post4, tmp1215^0'=tmp1215^post4, tmp05^0'=tmp05^post4, z218^0'=z218^post4, tmp49^0'=tmp49^post4, ctr23^0'=ctr23^post4, tmp611^0'=tmp611^post4, tmp16^0'=tmp16^post4, z420^0'=z420^post4, tmp1114^0'=tmp1114^post4, (tmp1013^0-tmp1013^post4 == 0 /\ -tmp1114^post4+tmp1114^0 == 0 /\ -tmp49^post4+tmp49^0 == 0 /\ -tmp1215^post4+tmp1215^0 == 0 /\ tmp1316^0-tmp1316^post4 == 0 /\ -tmp16^post4+tmp16^0 == 0 /\ seed^0-seed^post4 == 0 /\ z117^0-z117^post4 == 0 /\ -z420^post4+z420^0 == 0 /\ -tmp712^post4+tmp712^0 == 0 /\ tmp510^0-tmp510^post4 == 0 /\ -tmp611^post4+tmp611^0 == 0 /\ tmp38^0-tmp38^post4 == 0 /\ i^0-i^post4 == 0 /\ z521^0-z521^post4 == 0 /\ -z319^post4+z319^0 == 0 /\ -__const_64^post4+__const_64^0 == 0 /\ __const_7^0-__const_7^post4 == 0 /\ z218^0-z218^post4 == 0 /\ -tmp27^post4+tmp27^0 == 0 /\ -ctr23^post4+ctr23^0 == 0 /\ -tmp05^post4+tmp05^0 == 0), cost: 1
   3: l3 -> l5 : seed^0'=seed^post3, z117^0'=z117^post3, tmp38^0'=tmp38^post3, __const_7^0'=__const_7^post3, tmp510^0'=tmp510^post3, tmp1316^0'=tmp1316^post3, z319^0'=z319^post3, tmp1013^0'=tmp1013^post3, i^0'=i^post3, tmp712^0'=tmp712^post3, tmp27^0'=tmp27^post3, z521^0'=z521^post3, __const_64^0'=__const_64^post3, tmp1215^0'=tmp1215^post3, tmp05^0'=tmp05^post3, z218^0'=z218^post3, tmp49^0'=tmp49^post3, ctr23^0'=ctr23^post3, tmp611^0'=tmp611^post3, tmp16^0'=tmp16^post3, z420^0'=z420^post3, tmp1114^0'=tmp1114^post3, (0 == 0 /\ i^0-i^post3 == 0 /\ __const_7^0-__const_7^post3 == 0 /\ -tmp49^10-tmp611^10+z319^10 == 0 /\ -tmp510^10-tmp712^10+z420^10 == 0 /\ 1+ctr23^post3-ctr23^0 == 0 /\ seed^0-seed^post3 == 0 /\ tmp27^post3+tmp1215^post3-tmp16^post3 == 0 /\ -tmp49^10+z117^20-tmp712^10 == 0 /\ -ctr23^0 <= 0 /\ -tmp38^post3+tmp1013^post3-tmp05^post3 == 0 /\ -z521^post3-z319^20+z319^post3 == 0 /\ -__const_64^post3+__const_64^0 == 0 /\ z420^post3-z521^post3-z420^20 == 0 /\ -tmp27^post3-tmp16^post3+tmp1114^post3 == 0 /\ tmp38^post3-tmp05^post3+tmp1316^post3 == 0 /\ -tmp510^10-tmp611^10+z218^10 == 0), cost: 1
   6: l5 -> l3 : seed^0'=seed^post6, z117^0'=z117^post6, tmp38^0'=tmp38^post6, __const_7^0'=__const_7^post6, tmp510^0'=tmp510^post6, tmp1316^0'=tmp1316^post6, z319^0'=z319^post6, tmp1013^0'=tmp1013^post6, i^0'=i^post6, tmp712^0'=tmp712^post6, tmp27^0'=tmp27^post6, z521^0'=z521^post6, __const_64^0'=__const_64^post6, tmp1215^0'=tmp1215^post6, tmp05^0'=tmp05^post6, z218^0'=z218^post6, tmp49^0'=tmp49^post6, ctr23^0'=ctr23^post6, tmp611^0'=tmp611^post6, tmp16^0'=tmp16^post6, z420^0'=z420^post6, tmp1114^0'=tmp1114^post6, (-tmp27^post6+tmp27^0 == 0 /\ tmp712^0-tmp712^post6 == 0 /\ tmp16^0-tmp16^post6 == 0 /\ seed^0-seed^post6 == 0 /\ tmp38^0-tmp38^post6 == 0 /\ -tmp1114^post6+tmp1114^0 == 0 /\ __const_7^0-__const_7^post6 == 0 /\ -tmp05^post6+tmp05^0 == 0 /\ -z420^post6+z420^0 == 0 /\ -tmp1013^post6+tmp1013^0 == 0 /\ -i^post6+i^0 == 0 /\ tmp611^0-tmp611^post6 == 0 /\ tmp510^0-tmp510^post6 == 0 /\ __const_64^0-__const_64^post6 == 0 /\ -z218^post6+z218^0 == 0 /\ tmp1316^0-tmp1316^post6 == 0 /\ tmp49^0-tmp49^post6 == 0 /\ z319^0-z319^post6 == 0 /\ -tmp1215^post6+tmp1215^0 == 0 /\ -ctr23^post6+ctr23^0 == 0 /\ z117^0-z117^post6 == 0 /\ -z521^post6+z521^0 == 0), cost: 1
   7: l6 -> l5 : seed^0'=seed^post7, z117^0'=z117^post7, tmp38^0'=tmp38^post7, __const_7^0'=__const_7^post7, tmp510^0'=tmp510^post7, tmp1316^0'=tmp1316^post7, z319^0'=z319^post7, tmp1013^0'=tmp1013^post7, i^0'=i^post7, tmp712^0'=tmp712^post7, tmp27^0'=tmp27^post7, z521^0'=z521^post7, __const_64^0'=__const_64^post7, tmp1215^0'=tmp1215^post7, tmp05^0'=tmp05^post7, z218^0'=z218^post7, tmp49^0'=tmp49^post7, ctr23^0'=ctr23^post7, tmp611^0'=tmp611^post7, tmp16^0'=tmp16^post7, z420^0'=z420^post7, tmp1114^0'=tmp1114^post7, (-tmp1316^post7+tmp1316^0 == 0 /\ -tmp1114^post7+tmp1114^0 == 0 /\ -i^post7+i^0 == 0 /\ tmp27^0-tmp27^post7 == 0 /\ -tmp1013^post7+tmp1013^0 == 0 /\ tmp1215^0-tmp1215^post7 == 0 /\ -z521^post7+z521^0 == 0 /\ -tmp16^post7+tmp16^0 == 0 /\ z117^0-z117^post7 == 0 /\ seed^0-seed^post7 == 0 /\ -z420^post7+z420^0 == 0 /\ tmp712^0-tmp712^post7 == 0 /\ -__const_7^0+ctr23^post7 == 0 /\ tmp49^0-tmp49^post7 == 0 /\ tmp38^0-tmp38^post7 == 0 /\ 1+ctr23^0 <= 0 /\ -tmp510^post7+tmp510^0 == 0 /\ -z218^post7+z218^0 == 0 /\ -__const_64^post7+__const_64^0 == 0 /\ __const_7^0-__const_7^post7 == 0 /\ -tmp611^post7+tmp611^0 == 0 /\ -tmp05^post7+tmp05^0 == 0 /\ z319^0-z319^post7 == 0), cost: 1
   8: l6 -> l1 : seed^0'=seed^post8, z117^0'=z117^post8, tmp38^0'=tmp38^post8, __const_7^0'=__const_7^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=z319^post8, tmp1013^0'=tmp1013^post8, i^0'=i^post8, tmp712^0'=tmp712^post8, tmp27^0'=tmp27^post8, z521^0'=z521^post8, __const_64^0'=__const_64^post8, tmp1215^0'=tmp1215^post8, tmp05^0'=tmp05^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=ctr23^post8, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, (0 == 0 /\ -z420^210-z521^post8+z420^post8 == 0 /\ seed^0-seed^post8 == 0 /\ z218^110-tmp510^110-tmp611^110 == 0 /\ -ctr23^0 <= 0 /\ 1+ctr23^post8-ctr23^0 == 0 /\ -tmp49^11+z117^210-tmp712^110 == 0 /\ -i^post8+i^0 == 0 /\ tmp27^post8-tmp16^post8+tmp1215^post8 == 0 /\ z420^110-tmp712^110-tmp510^110 == 0 /\ z319^110-tmp49^11-tmp611^110 == 0 /\ __const_64^0-__const_64^post8 == 0 /\ __const_7^0-__const_7^post8 == 0 /\ -tmp27^post8-tmp16^post8+tmp1114^post8 == 0 /\ -tmp05^post8+tmp1316^post8+tmp38^post8 == 0 /\ tmp1013^post8-tmp05^post8-tmp38^post8 == 0 /\ -z319^210-z521^post8+z319^post8 == 0), cost: 1
   9: l7 -> l2 : seed^0'=seed^post9, z117^0'=z117^post9, tmp38^0'=tmp38^post9, __const_7^0'=__const_7^post9, tmp510^0'=tmp510^post9, tmp1316^0'=tmp1316^post9, z319^0'=z319^post9, tmp1013^0'=tmp1013^post9, i^0'=i^post9, tmp712^0'=tmp712^post9, tmp27^0'=tmp27^post9, z521^0'=z521^post9, __const_64^0'=__const_64^post9, tmp1215^0'=tmp1215^post9, tmp05^0'=tmp05^post9, z218^0'=z218^post9, tmp49^0'=tmp49^post9, ctr23^0'=ctr23^post9, tmp611^0'=tmp611^post9, tmp16^0'=tmp16^post9, z420^0'=z420^post9, tmp1114^0'=tmp1114^post9, (-z218^post9+z218^0 == 0 /\ z117^0-z117^post9 == 0 /\ -tmp510^post9+tmp510^0 == 0 /\ tmp712^0-tmp712^post9 == 0 /\ tmp16^0-tmp16^post9 == 0 /\ -ctr23^post9+ctr23^0 == 0 /\ i^post9 == 0 /\ -tmp1013^post9+tmp1013^0 == 0 /\ tmp38^0-tmp38^post9 == 0 /\ seed^post9 == 0 /\ __const_64^0-__const_64^post9 == 0 /\ tmp49^0-tmp49^post9 == 0 /\ -tmp1114^post9+tmp1114^0 == 0 /\ -tmp611^post9+tmp611^0 == 0 /\ z319^0-z319^post9 == 0 /\ z420^0-z420^post9 == 0 /\ __const_7^0-__const_7^post9 == 0 /\ -tmp1215^post9+tmp1215^0 == 0 /\ -tmp05^post9+tmp05^0 == 0 /\ tmp1316^0-tmp1316^post9 == 0 /\ -z521^post9+z521^0 == 0 /\ tmp27^0-tmp27^post9 == 0), cost: 1
  10: l8 -> l7 : seed^0'=seed^post10, z117^0'=z117^post10, tmp38^0'=tmp38^post10, __const_7^0'=__const_7^post10, tmp510^0'=tmp510^post10, tmp1316^0'=tmp1316^post10, z319^0'=z319^post10, tmp1013^0'=tmp1013^post10, i^0'=i^post10, tmp712^0'=tmp712^post10, tmp27^0'=tmp27^post10, z521^0'=z521^post10, __const_64^0'=__const_64^post10, tmp1215^0'=tmp1215^post10, tmp05^0'=tmp05^post10, z218^0'=z218^post10, tmp49^0'=tmp49^post10, ctr23^0'=ctr23^post10, tmp611^0'=tmp611^post10, tmp16^0'=tmp16^post10, z420^0'=z420^post10, tmp1114^0'=tmp1114^post10, (-tmp1114^post10+tmp1114^0 == 0 /\ -tmp611^post10+tmp611^0 == 0 /\ -tmp1316^post10+tmp1316^0 == 0 /\ seed^0-seed^post10 == 0 /\ z117^0-z117^post10 == 0 /\ -__const_64^post10+__const_64^0 == 0 /\ -z420^post10+z420^0 == 0 /\ z319^0-z319^post10 == 0 /\ __const_7^0-__const_7^post10 == 0 /\ ctr23^0-ctr23^post10 == 0 /\ -z521^post10+z521^0 == 0 /\ tmp1215^0-tmp1215^post10 == 0 /\ -i^post10+i^0 == 0 /\ -tmp05^post10+tmp05^0 == 0 /\ tmp27^0-tmp27^post10 == 0 /\ tmp1013^0-tmp1013^post10 == 0 /\ tmp510^0-tmp510^post10 == 0 /\ tmp38^0-tmp38^post10 == 0 /\ tmp712^0-tmp712^post10 == 0 /\ -tmp16^post10+tmp16^0 == 0 /\ -z218^post10+z218^0 == 0 /\ tmp49^0-tmp49^post10 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : seed^0'=seed^post0, z117^0'=z117^post0, tmp38^0'=tmp38^post0, __const_7^0'=__const_7^post0, tmp510^0'=tmp510^post0, tmp1316^0'=tmp1316^post0, z319^0'=z319^post0, tmp1013^0'=tmp1013^post0, i^0'=i^post0, tmp712^0'=tmp712^post0, tmp27^0'=tmp27^post0, z521^0'=z521^post0, __const_64^0'=__const_64^post0, tmp1215^0'=tmp1215^post0, tmp05^0'=tmp05^post0, z218^0'=z218^post0, tmp49^0'=tmp49^post0, ctr23^0'=ctr23^post0, tmp611^0'=tmp611^post0, tmp16^0'=tmp16^post0, z420^0'=z420^post0, tmp1114^0'=tmp1114^post0, (z319^0-z319^post0 == 0 /\ __const_7^0-__const_7^post0 == 0 /\ -tmp27^post0+tmp27^0 == 0 /\ -tmp1114^post0+tmp1114^0 == 0 /\ tmp38^0-tmp38^post0 == 0 /\ tmp16^0-tmp16^post0 == 0 /\ -z420^post0+z420^0 == 0 /\ ctr23^post0-__const_7^0 == 0 /\ -tmp1215^post0+tmp1215^0 == 0 /\ -tmp1013^post0+tmp1013^0 == 0 /\ -tmp05^post0+tmp05^0 == 0 /\ tmp611^0-tmp611^post0 == 0 /\ -i^0+__const_64^0 <= 0 /\ __const_64^0-__const_64^post0 == 0 /\ tmp1316^0-tmp1316^post0 == 0 /\ tmp49^0-tmp49^post0 == 0 /\ -z218^post0+z218^0 == 0 /\ seed^0-seed^post0 == 0 /\ i^0-i^post0 == 0 /\ tmp712^0-tmp712^post0 == 0 /\ -z117^post0+z117^0 == 0 /\ -z521^post0+z521^0 == 0 /\ tmp510^0-tmp510^post0 == 0), cost: 1
New rule:
l0 -> l1 : ctr23^0'=__const_7^0, -i^0+__const_64^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l0 -> l2 : seed^0'=seed^post1, z117^0'=z117^post1, tmp38^0'=tmp38^post1, __const_7^0'=__const_7^post1, tmp510^0'=tmp510^post1, tmp1316^0'=tmp1316^post1, z319^0'=z319^post1, tmp1013^0'=tmp1013^post1, i^0'=i^post1, tmp712^0'=tmp712^post1, tmp27^0'=tmp27^post1, z521^0'=z521^post1, __const_64^0'=__const_64^post1, tmp1215^0'=tmp1215^post1, tmp05^0'=tmp05^post1, z218^0'=z218^post1, tmp49^0'=tmp49^post1, ctr23^0'=ctr23^post1, tmp611^0'=tmp611^post1, tmp16^0'=tmp16^post1, z420^0'=z420^post1, tmp1114^0'=tmp1114^post1, (0 == 0 /\ tmp1215^0-tmp1215^post1 == 0 /\ -tmp05^post1+tmp05^0 == 0 /\ -z420^post1+z420^0 == 0 /\ -z521^post1+z521^0 == 0 /\ 1+i^0-__const_64^0 <= 0 /\ -tmp16^post1+tmp16^0 == 0 /\ tmp27^0-tmp27^post1 == 0 /\ -z218^post1+z218^0 == 0 /\ tmp38^0-tmp38^post1 == 0 /\ tmp712^0-tmp712^post1 == 0 /\ -ctr23^post1+ctr23^0 == 0 /\ -tmp611^post1+tmp611^0 == 0 /\ -tmp1114^post1+tmp1114^0 == 0 /\ __const_7^0-__const_7^post1 == 0 /\ tmp49^0-tmp49^post1 == 0 /\ -1+i^post1-i^0 == 0 /\ z117^0-z117^post1 == 0 /\ -tmp510^post1+tmp510^0 == 0 /\ -__const_64^post1+__const_64^0 == 0 /\ tmp1013^0-tmp1013^post1 == 0 /\ z319^0-z319^post1 == 0 /\ -tmp1316^post1+tmp1316^0 == 0), cost: 1
New rule:
l0 -> l2 : seed^0'=seed^post1, i^0'=1+i^0, 1+i^0-__const_64^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l3 -> l5 : seed^0'=seed^post3, z117^0'=z117^post3, tmp38^0'=tmp38^post3, __const_7^0'=__const_7^post3, tmp510^0'=tmp510^post3, tmp1316^0'=tmp1316^post3, z319^0'=z319^post3, tmp1013^0'=tmp1013^post3, i^0'=i^post3, tmp712^0'=tmp712^post3, tmp27^0'=tmp27^post3, z521^0'=z521^post3, __const_64^0'=__const_64^post3, tmp1215^0'=tmp1215^post3, tmp05^0'=tmp05^post3, z218^0'=z218^post3, tmp49^0'=tmp49^post3, ctr23^0'=ctr23^post3, tmp611^0'=tmp611^post3, tmp16^0'=tmp16^post3, z420^0'=z420^post3, tmp1114^0'=tmp1114^post3, (0 == 0 /\ i^0-i^post3 == 0 /\ __const_7^0-__const_7^post3 == 0 /\ -tmp49^10-tmp611^10+z319^10 == 0 /\ -tmp510^10-tmp712^10+z420^10 == 0 /\ 1+ctr23^post3-ctr23^0 == 0 /\ seed^0-seed^post3 == 0 /\ tmp27^post3+tmp1215^post3-tmp16^post3 == 0 /\ -tmp49^10+z117^20-tmp712^10 == 0 /\ -ctr23^0 <= 0 /\ -tmp38^post3+tmp1013^post3-tmp05^post3 == 0 /\ -z521^post3-z319^20+z319^post3 == 0 /\ -__const_64^post3+__const_64^0 == 0 /\ z420^post3-z521^post3-z420^20 == 0 /\ -tmp27^post3-tmp16^post3+tmp1114^post3 == 0 /\ tmp38^post3-tmp05^post3+tmp1316^post3 == 0 /\ -tmp510^10-tmp611^10+z218^10 == 0), cost: 1
New rule:
l3 -> l5 : z117^0'=z117^post3, tmp38^0'=tmp05^post3-tmp1316^post3, tmp510^0'=tmp510^post3, tmp1316^0'=tmp1316^post3, z319^0'=z319^post3, tmp1013^0'=2*tmp05^post3-tmp1316^post3, tmp712^0'=tmp712^post3, tmp27^0'=-tmp16^post3+tmp1114^post3, z521^0'=-z319^20+z319^post3, tmp1215^0'=2*tmp16^post3-tmp1114^post3, tmp05^0'=tmp05^post3, z218^0'=z218^post3, tmp49^0'=tmp49^post3, ctr23^0'=-1+ctr23^0, tmp611^0'=tmp611^post3, tmp16^0'=tmp16^post3, z420^0'=z420^20-z319^20+z319^post3, tmp1114^0'=tmp1114^post3, ctr23^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l0 : seed^0'=seed^post4, z117^0'=z117^post4, tmp38^0'=tmp38^post4, __const_7^0'=__const_7^post4, tmp510^0'=tmp510^post4, tmp1316^0'=tmp1316^post4, z319^0'=z319^post4, tmp1013^0'=tmp1013^post4, i^0'=i^post4, tmp712^0'=tmp712^post4, tmp27^0'=tmp27^post4, z521^0'=z521^post4, __const_64^0'=__const_64^post4, tmp1215^0'=tmp1215^post4, tmp05^0'=tmp05^post4, z218^0'=z218^post4, tmp49^0'=tmp49^post4, ctr23^0'=ctr23^post4, tmp611^0'=tmp611^post4, tmp16^0'=tmp16^post4, z420^0'=z420^post4, tmp1114^0'=tmp1114^post4, (tmp1013^0-tmp1013^post4 == 0 /\ -tmp1114^post4+tmp1114^0 == 0 /\ -tmp49^post4+tmp49^0 == 0 /\ -tmp1215^post4+tmp1215^0 == 0 /\ tmp1316^0-tmp1316^post4 == 0 /\ -tmp16^post4+tmp16^0 == 0 /\ seed^0-seed^post4 == 0 /\ z117^0-z117^post4 == 0 /\ -z420^post4+z420^0 == 0 /\ -tmp712^post4+tmp712^0 == 0 /\ tmp510^0-tmp510^post4 == 0 /\ -tmp611^post4+tmp611^0 == 0 /\ tmp38^0-tmp38^post4 == 0 /\ i^0-i^post4 == 0 /\ z521^0-z521^post4 == 0 /\ -z319^post4+z319^0 == 0 /\ -__const_64^post4+__const_64^0 == 0 /\ __const_7^0-__const_7^post4 == 0 /\ z218^0-z218^post4 == 0 /\ -tmp27^post4+tmp27^0 == 0 /\ -ctr23^post4+ctr23^0 == 0 /\ -tmp05^post4+tmp05^0 == 0), cost: 1
New rule:
l2 -> l0 : TRUE, cost: 1

Applied preprocessing
Original rule:
l1 -> l6 : seed^0'=seed^post5, z117^0'=z117^post5, tmp38^0'=tmp38^post5, __const_7^0'=__const_7^post5, tmp510^0'=tmp510^post5, tmp1316^0'=tmp1316^post5, z319^0'=z319^post5, tmp1013^0'=tmp1013^post5, i^0'=i^post5, tmp712^0'=tmp712^post5, tmp27^0'=tmp27^post5, z521^0'=z521^post5, __const_64^0'=__const_64^post5, tmp1215^0'=tmp1215^post5, tmp05^0'=tmp05^post5, z218^0'=z218^post5, tmp49^0'=tmp49^post5, ctr23^0'=ctr23^post5, tmp611^0'=tmp611^post5, tmp16^0'=tmp16^post5, z420^0'=z420^post5, tmp1114^0'=tmp1114^post5, (-z420^post5+z420^0 == 0 /\ -tmp16^post5+tmp16^0 == 0 /\ z319^0-z319^post5 == 0 /\ __const_64^0-__const_64^post5 == 0 /\ -z521^post5+z521^0 == 0 /\ -tmp05^post5+tmp05^0 == 0 /\ -ctr23^post5+ctr23^0 == 0 /\ tmp1316^0-tmp1316^post5 == 0 /\ -tmp611^post5+tmp611^0 == 0 /\ z218^0-z218^post5 == 0 /\ tmp510^0-tmp510^post5 == 0 /\ seed^0-seed^post5 == 0 /\ -tmp1215^post5+tmp1215^0 == 0 /\ tmp38^0-tmp38^post5 == 0 /\ __const_7^0-__const_7^post5 == 0 /\ z117^0-z117^post5 == 0 /\ -tmp27^post5+tmp27^0 == 0 /\ i^0-i^post5 == 0 /\ tmp712^0-tmp712^post5 == 0 /\ tmp1013^0-tmp1013^post5 == 0 /\ -tmp1114^post5+tmp1114^0 == 0 /\ -tmp49^post5+tmp49^0 == 0), cost: 1
New rule:
l1 -> l6 : TRUE, cost: 1

Applied preprocessing
Original rule:
l5 -> l3 : seed^0'=seed^post6, z117^0'=z117^post6, tmp38^0'=tmp38^post6, __const_7^0'=__const_7^post6, tmp510^0'=tmp510^post6, tmp1316^0'=tmp1316^post6, z319^0'=z319^post6, tmp1013^0'=tmp1013^post6, i^0'=i^post6, tmp712^0'=tmp712^post6, tmp27^0'=tmp27^post6, z521^0'=z521^post6, __const_64^0'=__const_64^post6, tmp1215^0'=tmp1215^post6, tmp05^0'=tmp05^post6, z218^0'=z218^post6, tmp49^0'=tmp49^post6, ctr23^0'=ctr23^post6, tmp611^0'=tmp611^post6, tmp16^0'=tmp16^post6, z420^0'=z420^post6, tmp1114^0'=tmp1114^post6, (-tmp27^post6+tmp27^0 == 0 /\ tmp712^0-tmp712^post6 == 0 /\ tmp16^0-tmp16^post6 == 0 /\ seed^0-seed^post6 == 0 /\ tmp38^0-tmp38^post6 == 0 /\ -tmp1114^post6+tmp1114^0 == 0 /\ __const_7^0-__const_7^post6 == 0 /\ -tmp05^post6+tmp05^0 == 0 /\ -z420^post6+z420^0 == 0 /\ -tmp1013^post6+tmp1013^0 == 0 /\ -i^post6+i^0 == 0 /\ tmp611^0-tmp611^post6 == 0 /\ tmp510^0-tmp510^post6 == 0 /\ __const_64^0-__const_64^post6 == 0 /\ -z218^post6+z218^0 == 0 /\ tmp1316^0-tmp1316^post6 == 0 /\ tmp49^0-tmp49^post6 == 0 /\ z319^0-z319^post6 == 0 /\ -tmp1215^post6+tmp1215^0 == 0 /\ -ctr23^post6+ctr23^0 == 0 /\ z117^0-z117^post6 == 0 /\ -z521^post6+z521^0 == 0), cost: 1
New rule:
l5 -> l3 : TRUE, cost: 1

Applied preprocessing
Original rule:
l6 -> l5 : seed^0'=seed^post7, z117^0'=z117^post7, tmp38^0'=tmp38^post7, __const_7^0'=__const_7^post7, tmp510^0'=tmp510^post7, tmp1316^0'=tmp1316^post7, z319^0'=z319^post7, tmp1013^0'=tmp1013^post7, i^0'=i^post7, tmp712^0'=tmp712^post7, tmp27^0'=tmp27^post7, z521^0'=z521^post7, __const_64^0'=__const_64^post7, tmp1215^0'=tmp1215^post7, tmp05^0'=tmp05^post7, z218^0'=z218^post7, tmp49^0'=tmp49^post7, ctr23^0'=ctr23^post7, tmp611^0'=tmp611^post7, tmp16^0'=tmp16^post7, z420^0'=z420^post7, tmp1114^0'=tmp1114^post7, (-tmp1316^post7+tmp1316^0 == 0 /\ -tmp1114^post7+tmp1114^0 == 0 /\ -i^post7+i^0 == 0 /\ tmp27^0-tmp27^post7 == 0 /\ -tmp1013^post7+tmp1013^0 == 0 /\ tmp1215^0-tmp1215^post7 == 0 /\ -z521^post7+z521^0 == 0 /\ -tmp16^post7+tmp16^0 == 0 /\ z117^0-z117^post7 == 0 /\ seed^0-seed^post7 == 0 /\ -z420^post7+z420^0 == 0 /\ tmp712^0-tmp712^post7 == 0 /\ -__const_7^0+ctr23^post7 == 0 /\ tmp49^0-tmp49^post7 == 0 /\ tmp38^0-tmp38^post7 == 0 /\ 1+ctr23^0 <= 0 /\ -tmp510^post7+tmp510^0 == 0 /\ -z218^post7+z218^0 == 0 /\ -__const_64^post7+__const_64^0 == 0 /\ __const_7^0-__const_7^post7 == 0 /\ -tmp611^post7+tmp611^0 == 0 /\ -tmp05^post7+tmp05^0 == 0 /\ z319^0-z319^post7 == 0), cost: 1
New rule:
l6 -> l5 : ctr23^0'=__const_7^0, 1+ctr23^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l6 -> l1 : seed^0'=seed^post8, z117^0'=z117^post8, tmp38^0'=tmp38^post8, __const_7^0'=__const_7^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=z319^post8, tmp1013^0'=tmp1013^post8, i^0'=i^post8, tmp712^0'=tmp712^post8, tmp27^0'=tmp27^post8, z521^0'=z521^post8, __const_64^0'=__const_64^post8, tmp1215^0'=tmp1215^post8, tmp05^0'=tmp05^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=ctr23^post8, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, (0 == 0 /\ -z420^210-z521^post8+z420^post8 == 0 /\ seed^0-seed^post8 == 0 /\ z218^110-tmp510^110-tmp611^110 == 0 /\ -ctr23^0 <= 0 /\ 1+ctr23^post8-ctr23^0 == 0 /\ -tmp49^11+z117^210-tmp712^110 == 0 /\ -i^post8+i^0 == 0 /\ tmp27^post8-tmp16^post8+tmp1215^post8 == 0 /\ z420^110-tmp712^110-tmp510^110 == 0 /\ z319^110-tmp49^11-tmp611^110 == 0 /\ __const_64^0-__const_64^post8 == 0 /\ __const_7^0-__const_7^post8 == 0 /\ -tmp27^post8-tmp16^post8+tmp1114^post8 == 0 /\ -tmp05^post8+tmp1316^post8+tmp38^post8 == 0 /\ tmp1013^post8-tmp05^post8-tmp38^post8 == 0 /\ -z319^210-z521^post8+z319^post8 == 0), cost: 1
New rule:
l6 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-1+ctr23^0, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, ctr23^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l7 -> l2 : seed^0'=seed^post9, z117^0'=z117^post9, tmp38^0'=tmp38^post9, __const_7^0'=__const_7^post9, tmp510^0'=tmp510^post9, tmp1316^0'=tmp1316^post9, z319^0'=z319^post9, tmp1013^0'=tmp1013^post9, i^0'=i^post9, tmp712^0'=tmp712^post9, tmp27^0'=tmp27^post9, z521^0'=z521^post9, __const_64^0'=__const_64^post9, tmp1215^0'=tmp1215^post9, tmp05^0'=tmp05^post9, z218^0'=z218^post9, tmp49^0'=tmp49^post9, ctr23^0'=ctr23^post9, tmp611^0'=tmp611^post9, tmp16^0'=tmp16^post9, z420^0'=z420^post9, tmp1114^0'=tmp1114^post9, (-z218^post9+z218^0 == 0 /\ z117^0-z117^post9 == 0 /\ -tmp510^post9+tmp510^0 == 0 /\ tmp712^0-tmp712^post9 == 0 /\ tmp16^0-tmp16^post9 == 0 /\ -ctr23^post9+ctr23^0 == 0 /\ i^post9 == 0 /\ -tmp1013^post9+tmp1013^0 == 0 /\ tmp38^0-tmp38^post9 == 0 /\ seed^post9 == 0 /\ __const_64^0-__const_64^post9 == 0 /\ tmp49^0-tmp49^post9 == 0 /\ -tmp1114^post9+tmp1114^0 == 0 /\ -tmp611^post9+tmp611^0 == 0 /\ z319^0-z319^post9 == 0 /\ z420^0-z420^post9 == 0 /\ __const_7^0-__const_7^post9 == 0 /\ -tmp1215^post9+tmp1215^0 == 0 /\ -tmp05^post9+tmp05^0 == 0 /\ tmp1316^0-tmp1316^post9 == 0 /\ -z521^post9+z521^0 == 0 /\ tmp27^0-tmp27^post9 == 0), cost: 1
New rule:
l7 -> l2 : seed^0'=0, i^0'=0, TRUE, cost: 1

Applied preprocessing
Original rule:
l8 -> l7 : seed^0'=seed^post10, z117^0'=z117^post10, tmp38^0'=tmp38^post10, __const_7^0'=__const_7^post10, tmp510^0'=tmp510^post10, tmp1316^0'=tmp1316^post10, z319^0'=z319^post10, tmp1013^0'=tmp1013^post10, i^0'=i^post10, tmp712^0'=tmp712^post10, tmp27^0'=tmp27^post10, z521^0'=z521^post10, __const_64^0'=__const_64^post10, tmp1215^0'=tmp1215^post10, tmp05^0'=tmp05^post10, z218^0'=z218^post10, tmp49^0'=tmp49^post10, ctr23^0'=ctr23^post10, tmp611^0'=tmp611^post10, tmp16^0'=tmp16^post10, z420^0'=z420^post10, tmp1114^0'=tmp1114^post10, (-tmp1114^post10+tmp1114^0 == 0 /\ -tmp611^post10+tmp611^0 == 0 /\ -tmp1316^post10+tmp1316^0 == 0 /\ seed^0-seed^post10 == 0 /\ z117^0-z117^post10 == 0 /\ -__const_64^post10+__const_64^0 == 0 /\ -z420^post10+z420^0 == 0 /\ z319^0-z319^post10 == 0 /\ __const_7^0-__const_7^post10 == 0 /\ ctr23^0-ctr23^post10 == 0 /\ -z521^post10+z521^0 == 0 /\ tmp1215^0-tmp1215^post10 == 0 /\ -i^post10+i^0 == 0 /\ -tmp05^post10+tmp05^0 == 0 /\ tmp27^0-tmp27^post10 == 0 /\ tmp1013^0-tmp1013^post10 == 0 /\ tmp510^0-tmp510^post10 == 0 /\ tmp38^0-tmp38^post10 == 0 /\ tmp712^0-tmp712^post10 == 0 /\ -tmp16^post10+tmp16^0 == 0 /\ -z218^post10+z218^0 == 0 /\ tmp49^0-tmp49^post10 == 0), cost: 1
New rule:
l8 -> l7 : TRUE, cost: 1

Simplified rules
Start location: l8
  11: l0 -> l1 : ctr23^0'=__const_7^0, -i^0+__const_64^0 <= 0, cost: 1
  12: l0 -> l2 : seed^0'=seed^post1, i^0'=1+i^0, 1+i^0-__const_64^0 <= 0, cost: 1
  15: l1 -> l6 : TRUE, cost: 1
  14: l2 -> l0 : TRUE, cost: 1
  13: l3 -> l5 : z117^0'=z117^post3, tmp38^0'=tmp05^post3-tmp1316^post3, tmp510^0'=tmp510^post3, tmp1316^0'=tmp1316^post3, z319^0'=z319^post3, tmp1013^0'=2*tmp05^post3-tmp1316^post3, tmp712^0'=tmp712^post3, tmp27^0'=-tmp16^post3+tmp1114^post3, z521^0'=-z319^20+z319^post3, tmp1215^0'=2*tmp16^post3-tmp1114^post3, tmp05^0'=tmp05^post3, z218^0'=z218^post3, tmp49^0'=tmp49^post3, ctr23^0'=-1+ctr23^0, tmp611^0'=tmp611^post3, tmp16^0'=tmp16^post3, z420^0'=z420^20-z319^20+z319^post3, tmp1114^0'=tmp1114^post3, ctr23^0 >= 0, cost: 1
  16: l5 -> l3 : TRUE, cost: 1
  17: l6 -> l5 : ctr23^0'=__const_7^0, 1+ctr23^0 <= 0, cost: 1
  18: l6 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-1+ctr23^0, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, ctr23^0 >= 0, cost: 1
  19: l7 -> l2 : seed^0'=0, i^0'=0, TRUE, cost: 1
  20: l8 -> l7 : TRUE, cost: 1


Eliminating location l7 by chaining:

Applied chaining
First rule:
l8 -> l7 : TRUE, cost: 1
Second rule:
l7 -> l2 : seed^0'=0, i^0'=0, TRUE, cost: 1
New rule:
l8 -> l2 : seed^0'=0, i^0'=0, TRUE, cost: 2

Applied deletion
Removed the following rules: 19 20

Eliminating location l3 by chaining:

Applied chaining
First rule:
l5 -> l3 : TRUE, cost: 1
Second rule:
l3 -> l5 : z117^0'=z117^post3, tmp38^0'=tmp05^post3-tmp1316^post3, tmp510^0'=tmp510^post3, tmp1316^0'=tmp1316^post3, z319^0'=z319^post3, tmp1013^0'=2*tmp05^post3-tmp1316^post3, tmp712^0'=tmp712^post3, tmp27^0'=-tmp16^post3+tmp1114^post3, z521^0'=-z319^20+z319^post3, tmp1215^0'=2*tmp16^post3-tmp1114^post3, tmp05^0'=tmp05^post3, z218^0'=z218^post3, tmp49^0'=tmp49^post3, ctr23^0'=-1+ctr23^0, tmp611^0'=tmp611^post3, tmp16^0'=tmp16^post3, z420^0'=z420^20-z319^20+z319^post3, tmp1114^0'=tmp1114^post3, ctr23^0 >= 0, cost: 1
New rule:
l5 -> l5 : z117^0'=z117^post3, tmp38^0'=tmp05^post3-tmp1316^post3, tmp510^0'=tmp510^post3, tmp1316^0'=tmp1316^post3, z319^0'=z319^post3, tmp1013^0'=2*tmp05^post3-tmp1316^post3, tmp712^0'=tmp712^post3, tmp27^0'=-tmp16^post3+tmp1114^post3, z521^0'=-z319^20+z319^post3, tmp1215^0'=2*tmp16^post3-tmp1114^post3, tmp05^0'=tmp05^post3, z218^0'=z218^post3, tmp49^0'=tmp49^post3, ctr23^0'=-1+ctr23^0, tmp611^0'=tmp611^post3, tmp16^0'=tmp16^post3, z420^0'=z420^20-z319^20+z319^post3, tmp1114^0'=tmp1114^post3, ctr23^0 >= 0, cost: 2

Applied deletion
Removed the following rules: 13 16

Eliminated locations on linear paths
Start location: l8
  11: l0 -> l1 : ctr23^0'=__const_7^0, -i^0+__const_64^0 <= 0, cost: 1
  12: l0 -> l2 : seed^0'=seed^post1, i^0'=1+i^0, 1+i^0-__const_64^0 <= 0, cost: 1
  15: l1 -> l6 : TRUE, cost: 1
  14: l2 -> l0 : TRUE, cost: 1
  22: l5 -> l5 : z117^0'=z117^post3, tmp38^0'=tmp05^post3-tmp1316^post3, tmp510^0'=tmp510^post3, tmp1316^0'=tmp1316^post3, z319^0'=z319^post3, tmp1013^0'=2*tmp05^post3-tmp1316^post3, tmp712^0'=tmp712^post3, tmp27^0'=-tmp16^post3+tmp1114^post3, z521^0'=-z319^20+z319^post3, tmp1215^0'=2*tmp16^post3-tmp1114^post3, tmp05^0'=tmp05^post3, z218^0'=z218^post3, tmp49^0'=tmp49^post3, ctr23^0'=-1+ctr23^0, tmp611^0'=tmp611^post3, tmp16^0'=tmp16^post3, z420^0'=z420^20-z319^20+z319^post3, tmp1114^0'=tmp1114^post3, ctr23^0 >= 0, cost: 2
  17: l6 -> l5 : ctr23^0'=__const_7^0, 1+ctr23^0 <= 0, cost: 1
  18: l6 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-1+ctr23^0, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, ctr23^0 >= 0, cost: 1
  21: l8 -> l2 : seed^0'=0, i^0'=0, TRUE, cost: 2


Applied acceleration
Original rule:
l5 -> l5 : z117^0'=z117^post3, tmp38^0'=tmp05^post3-tmp1316^post3, tmp510^0'=tmp510^post3, tmp1316^0'=tmp1316^post3, z319^0'=z319^post3, tmp1013^0'=2*tmp05^post3-tmp1316^post3, tmp712^0'=tmp712^post3, tmp27^0'=-tmp16^post3+tmp1114^post3, z521^0'=-z319^20+z319^post3, tmp1215^0'=2*tmp16^post3-tmp1114^post3, tmp05^0'=tmp05^post3, z218^0'=z218^post3, tmp49^0'=tmp49^post3, ctr23^0'=-1+ctr23^0, tmp611^0'=tmp611^post3, tmp16^0'=tmp16^post3, z420^0'=z420^20-z319^20+z319^post3, tmp1114^0'=tmp1114^post3, ctr23^0 >= 0, cost: 2
New rule:
l5 -> l5 : z117^0'=z117^post3, tmp38^0'=tmp05^post3-tmp1316^post3, tmp510^0'=tmp510^post3, tmp1316^0'=tmp1316^post3, z319^0'=z319^post3, tmp1013^0'=2*tmp05^post3-tmp1316^post3, tmp712^0'=tmp712^post3, tmp27^0'=-tmp16^post3+tmp1114^post3, z521^0'=-z319^20+z319^post3, tmp1215^0'=2*tmp16^post3-tmp1114^post3, tmp05^0'=tmp05^post3, z218^0'=z218^post3, tmp49^0'=tmp49^post3, ctr23^0'=-n+ctr23^0, tmp611^0'=tmp611^post3, tmp16^0'=tmp16^post3, z420^0'=z420^20-z319^20+z319^post3, tmp1114^0'=tmp1114^post3, (1-n+ctr23^0 >= 0 /\ -1+n >= 0), cost: 2*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_DBhMll.txt

Applied instantiation
Original rule:
l5 -> l5 : z117^0'=z117^post3, tmp38^0'=tmp05^post3-tmp1316^post3, tmp510^0'=tmp510^post3, tmp1316^0'=tmp1316^post3, z319^0'=z319^post3, tmp1013^0'=2*tmp05^post3-tmp1316^post3, tmp712^0'=tmp712^post3, tmp27^0'=-tmp16^post3+tmp1114^post3, z521^0'=-z319^20+z319^post3, tmp1215^0'=2*tmp16^post3-tmp1114^post3, tmp05^0'=tmp05^post3, z218^0'=z218^post3, tmp49^0'=tmp49^post3, ctr23^0'=-n+ctr23^0, tmp611^0'=tmp611^post3, tmp16^0'=tmp16^post3, z420^0'=z420^20-z319^20+z319^post3, tmp1114^0'=tmp1114^post3, (1-n+ctr23^0 >= 0 /\ -1+n >= 0), cost: 2*n
New rule:
l5 -> l5 : z117^0'=z117^post3, tmp38^0'=tmp05^post3-tmp1316^post3, tmp510^0'=tmp510^post3, tmp1316^0'=tmp1316^post3, z319^0'=z319^post3, tmp1013^0'=2*tmp05^post3-tmp1316^post3, tmp712^0'=tmp712^post3, tmp27^0'=-tmp16^post3+tmp1114^post3, z521^0'=-z319^20+z319^post3, tmp1215^0'=2*tmp16^post3-tmp1114^post3, tmp05^0'=tmp05^post3, z218^0'=z218^post3, tmp49^0'=tmp49^post3, ctr23^0'=-1, tmp611^0'=tmp611^post3, tmp16^0'=tmp16^post3, z420^0'=z420^20-z319^20+z319^post3, tmp1114^0'=tmp1114^post3, (0 >= 0 /\ ctr23^0 >= 0), cost: 2+2*ctr23^0

Applied simplification
Original rule:
l5 -> l5 : z117^0'=z117^post3, tmp38^0'=tmp05^post3-tmp1316^post3, tmp510^0'=tmp510^post3, tmp1316^0'=tmp1316^post3, z319^0'=z319^post3, tmp1013^0'=2*tmp05^post3-tmp1316^post3, tmp712^0'=tmp712^post3, tmp27^0'=-tmp16^post3+tmp1114^post3, z521^0'=-z319^20+z319^post3, tmp1215^0'=2*tmp16^post3-tmp1114^post3, tmp05^0'=tmp05^post3, z218^0'=z218^post3, tmp49^0'=tmp49^post3, ctr23^0'=-1, tmp611^0'=tmp611^post3, tmp16^0'=tmp16^post3, z420^0'=z420^20-z319^20+z319^post3, tmp1114^0'=tmp1114^post3, (0 >= 0 /\ ctr23^0 >= 0), cost: 2+2*ctr23^0
New rule:
l5 -> l5 : z117^0'=z117^post3, tmp38^0'=tmp05^post3-tmp1316^post3, tmp510^0'=tmp510^post3, tmp1316^0'=tmp1316^post3, z319^0'=z319^post3, tmp1013^0'=2*tmp05^post3-tmp1316^post3, tmp712^0'=tmp712^post3, tmp27^0'=-tmp16^post3+tmp1114^post3, z521^0'=-z319^20+z319^post3, tmp1215^0'=2*tmp16^post3-tmp1114^post3, tmp05^0'=tmp05^post3, z218^0'=z218^post3, tmp49^0'=tmp49^post3, ctr23^0'=-1, tmp611^0'=tmp611^post3, tmp16^0'=tmp16^post3, z420^0'=z420^20-z319^20+z319^post3, tmp1114^0'=tmp1114^post3, ctr23^0 >= 0, cost: 2+2*ctr23^0

Applied deletion
Removed the following rules: 22

Accelerated simple loops
Start location: l8
  11: l0 -> l1 : ctr23^0'=__const_7^0, -i^0+__const_64^0 <= 0, cost: 1
  12: l0 -> l2 : seed^0'=seed^post1, i^0'=1+i^0, 1+i^0-__const_64^0 <= 0, cost: 1
  15: l1 -> l6 : TRUE, cost: 1
  14: l2 -> l0 : TRUE, cost: 1
  24: l5 -> l5 : z117^0'=z117^post3, tmp38^0'=tmp05^post3-tmp1316^post3, tmp510^0'=tmp510^post3, tmp1316^0'=tmp1316^post3, z319^0'=z319^post3, tmp1013^0'=2*tmp05^post3-tmp1316^post3, tmp712^0'=tmp712^post3, tmp27^0'=-tmp16^post3+tmp1114^post3, z521^0'=-z319^20+z319^post3, tmp1215^0'=2*tmp16^post3-tmp1114^post3, tmp05^0'=tmp05^post3, z218^0'=z218^post3, tmp49^0'=tmp49^post3, ctr23^0'=-1, tmp611^0'=tmp611^post3, tmp16^0'=tmp16^post3, z420^0'=z420^20-z319^20+z319^post3, tmp1114^0'=tmp1114^post3, ctr23^0 >= 0, cost: 2+2*ctr23^0
  17: l6 -> l5 : ctr23^0'=__const_7^0, 1+ctr23^0 <= 0, cost: 1
  18: l6 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-1+ctr23^0, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, ctr23^0 >= 0, cost: 1
  21: l8 -> l2 : seed^0'=0, i^0'=0, TRUE, cost: 2


Applied chaining
First rule:
l6 -> l5 : ctr23^0'=__const_7^0, 1+ctr23^0 <= 0, cost: 1
Second rule:
l5 -> l5 : z117^0'=z117^post3, tmp38^0'=tmp05^post3-tmp1316^post3, tmp510^0'=tmp510^post3, tmp1316^0'=tmp1316^post3, z319^0'=z319^post3, tmp1013^0'=2*tmp05^post3-tmp1316^post3, tmp712^0'=tmp712^post3, tmp27^0'=-tmp16^post3+tmp1114^post3, z521^0'=-z319^20+z319^post3, tmp1215^0'=2*tmp16^post3-tmp1114^post3, tmp05^0'=tmp05^post3, z218^0'=z218^post3, tmp49^0'=tmp49^post3, ctr23^0'=-1, tmp611^0'=tmp611^post3, tmp16^0'=tmp16^post3, z420^0'=z420^20-z319^20+z319^post3, tmp1114^0'=tmp1114^post3, ctr23^0 >= 0, cost: 2+2*ctr23^0
New rule:
l6 -> l5 : z117^0'=z117^post3, tmp38^0'=tmp05^post3-tmp1316^post3, tmp510^0'=tmp510^post3, tmp1316^0'=tmp1316^post3, z319^0'=z319^post3, tmp1013^0'=2*tmp05^post3-tmp1316^post3, tmp712^0'=tmp712^post3, tmp27^0'=-tmp16^post3+tmp1114^post3, z521^0'=-z319^20+z319^post3, tmp1215^0'=2*tmp16^post3-tmp1114^post3, tmp05^0'=tmp05^post3, z218^0'=z218^post3, tmp49^0'=tmp49^post3, ctr23^0'=-1, tmp611^0'=tmp611^post3, tmp16^0'=tmp16^post3, z420^0'=z420^20-z319^20+z319^post3, tmp1114^0'=tmp1114^post3, (__const_7^0 >= 0 /\ 1+ctr23^0 <= 0), cost: 3+2*__const_7^0

Applied deletion
Removed the following rules: 24

Chained accelerated rules with incoming rules
Start location: l8
  11: l0 -> l1 : ctr23^0'=__const_7^0, -i^0+__const_64^0 <= 0, cost: 1
  12: l0 -> l2 : seed^0'=seed^post1, i^0'=1+i^0, 1+i^0-__const_64^0 <= 0, cost: 1
  15: l1 -> l6 : TRUE, cost: 1
  14: l2 -> l0 : TRUE, cost: 1
  17: l6 -> l5 : ctr23^0'=__const_7^0, 1+ctr23^0 <= 0, cost: 1
  18: l6 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-1+ctr23^0, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, ctr23^0 >= 0, cost: 1
  25: l6 -> l5 : z117^0'=z117^post3, tmp38^0'=tmp05^post3-tmp1316^post3, tmp510^0'=tmp510^post3, tmp1316^0'=tmp1316^post3, z319^0'=z319^post3, tmp1013^0'=2*tmp05^post3-tmp1316^post3, tmp712^0'=tmp712^post3, tmp27^0'=-tmp16^post3+tmp1114^post3, z521^0'=-z319^20+z319^post3, tmp1215^0'=2*tmp16^post3-tmp1114^post3, tmp05^0'=tmp05^post3, z218^0'=z218^post3, tmp49^0'=tmp49^post3, ctr23^0'=-1, tmp611^0'=tmp611^post3, tmp16^0'=tmp16^post3, z420^0'=z420^20-z319^20+z319^post3, tmp1114^0'=tmp1114^post3, (__const_7^0 >= 0 /\ 1+ctr23^0 <= 0), cost: 3+2*__const_7^0
  21: l8 -> l2 : seed^0'=0, i^0'=0, TRUE, cost: 2


Removed unreachable locations and irrelevant leafs
Start location: l8
  11: l0 -> l1 : ctr23^0'=__const_7^0, -i^0+__const_64^0 <= 0, cost: 1
  12: l0 -> l2 : seed^0'=seed^post1, i^0'=1+i^0, 1+i^0-__const_64^0 <= 0, cost: 1
  15: l1 -> l6 : TRUE, cost: 1
  14: l2 -> l0 : TRUE, cost: 1
  18: l6 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-1+ctr23^0, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, ctr23^0 >= 0, cost: 1
  21: l8 -> l2 : seed^0'=0, i^0'=0, TRUE, cost: 2


Eliminating location l6 by chaining:

Applied chaining
First rule:
l1 -> l6 : TRUE, cost: 1
Second rule:
l6 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-1+ctr23^0, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, ctr23^0 >= 0, cost: 1
New rule:
l1 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-1+ctr23^0, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, ctr23^0 >= 0, cost: 2

Applied deletion
Removed the following rules: 15 18

Eliminated locations on linear paths
Start location: l8
  11: l0 -> l1 : ctr23^0'=__const_7^0, -i^0+__const_64^0 <= 0, cost: 1
  12: l0 -> l2 : seed^0'=seed^post1, i^0'=1+i^0, 1+i^0-__const_64^0 <= 0, cost: 1
  26: l1 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-1+ctr23^0, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, ctr23^0 >= 0, cost: 2
  14: l2 -> l0 : TRUE, cost: 1
  21: l8 -> l2 : seed^0'=0, i^0'=0, TRUE, cost: 2


Applied acceleration
Original rule:
l1 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-1+ctr23^0, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, ctr23^0 >= 0, cost: 2
New rule:
l1 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-n0+ctr23^0, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, (-1+n0 >= 0 /\ 1-n0+ctr23^0 >= 0), cost: 2*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_cOmpgb.txt

Applied instantiation
Original rule:
l1 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-n0+ctr23^0, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, (-1+n0 >= 0 /\ 1-n0+ctr23^0 >= 0), cost: 2*n0
New rule:
l1 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-1, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, (0 >= 0 /\ ctr23^0 >= 0), cost: 2+2*ctr23^0

Applied simplification
Original rule:
l1 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-1, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, (0 >= 0 /\ ctr23^0 >= 0), cost: 2+2*ctr23^0
New rule:
l1 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-1, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, ctr23^0 >= 0, cost: 2+2*ctr23^0

Applied deletion
Removed the following rules: 26

Accelerated simple loops
Start location: l8
  11: l0 -> l1 : ctr23^0'=__const_7^0, -i^0+__const_64^0 <= 0, cost: 1
  12: l0 -> l2 : seed^0'=seed^post1, i^0'=1+i^0, 1+i^0-__const_64^0 <= 0, cost: 1
  28: l1 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-1, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, ctr23^0 >= 0, cost: 2+2*ctr23^0
  14: l2 -> l0 : TRUE, cost: 1
  21: l8 -> l2 : seed^0'=0, i^0'=0, TRUE, cost: 2


Applied chaining
First rule:
l0 -> l1 : ctr23^0'=__const_7^0, -i^0+__const_64^0 <= 0, cost: 1
Second rule:
l1 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-1, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, ctr23^0 >= 0, cost: 2+2*ctr23^0
New rule:
l0 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-1, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, (__const_7^0 >= 0 /\ -i^0+__const_64^0 <= 0), cost: 3+2*__const_7^0

Applied deletion
Removed the following rules: 28

Chained accelerated rules with incoming rules
Start location: l8
  11: l0 -> l1 : ctr23^0'=__const_7^0, -i^0+__const_64^0 <= 0, cost: 1
  12: l0 -> l2 : seed^0'=seed^post1, i^0'=1+i^0, 1+i^0-__const_64^0 <= 0, cost: 1
  29: l0 -> l1 : z117^0'=z117^post8, tmp38^0'=tmp38^post8, tmp510^0'=tmp510^post8, tmp1316^0'=tmp1316^post8, z319^0'=-z420^210+z319^210+z420^post8, tmp1013^0'=tmp1316^post8+2*tmp38^post8, tmp712^0'=tmp712^post8, tmp27^0'=-tmp16^post8+tmp1114^post8, z521^0'=-z420^210+z420^post8, tmp1215^0'=2*tmp16^post8-tmp1114^post8, tmp05^0'=tmp1316^post8+tmp38^post8, z218^0'=z218^post8, tmp49^0'=tmp49^post8, ctr23^0'=-1, tmp611^0'=tmp611^post8, tmp16^0'=tmp16^post8, z420^0'=z420^post8, tmp1114^0'=tmp1114^post8, (__const_7^0 >= 0 /\ -i^0+__const_64^0 <= 0), cost: 3+2*__const_7^0
  14: l2 -> l0 : TRUE, cost: 1
  21: l8 -> l2 : seed^0'=0, i^0'=0, TRUE, cost: 2


Removed unreachable locations and irrelevant leafs
Start location: l8
  12: l0 -> l2 : seed^0'=seed^post1, i^0'=1+i^0, 1+i^0-__const_64^0 <= 0, cost: 1
  14: l2 -> l0 : TRUE, cost: 1
  21: l8 -> l2 : seed^0'=0, i^0'=0, TRUE, cost: 2


Eliminating location l0 by chaining:

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

Applied deletion
Removed the following rules: 12 14

Eliminated locations on linear paths
Start location: l8
  30: l2 -> l2 : seed^0'=seed^post1, i^0'=1+i^0, 1+i^0-__const_64^0 <= 0, cost: 2
  21: l8 -> l2 : seed^0'=0, i^0'=0, TRUE, cost: 2


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

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

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

Applied deletion
Removed the following rules: 30

Accelerated simple loops
Start location: l8
  32: l2 -> l2 : seed^0'=seed^post1, i^0'=__const_64^0, -1-i^0+__const_64^0 >= 0, cost: -2*i^0+2*__const_64^0
  21: l8 -> l2 : seed^0'=0, i^0'=0, TRUE, cost: 2


Applied chaining
First rule:
l8 -> l2 : seed^0'=0, i^0'=0, TRUE, cost: 2
Second rule:
l2 -> l2 : seed^0'=seed^post1, i^0'=__const_64^0, -1-i^0+__const_64^0 >= 0, cost: -2*i^0+2*__const_64^0
New rule:
l8 -> l2 : seed^0'=seed^post1, i^0'=__const_64^0, -1+__const_64^0 >= 0, cost: 2+2*__const_64^0

Applied deletion
Removed the following rules: 32

Chained accelerated rules with incoming rules
Start location: l8
  21: l8 -> l2 : seed^0'=0, i^0'=0, TRUE, cost: 2
  33: l8 -> l2 : seed^0'=seed^post1, i^0'=__const_64^0, -1+__const_64^0 >= 0, cost: 2+2*__const_64^0


Removed unreachable locations and irrelevant leafs
Start location: l8
  <empty>


Computing asymptotic complexity

Proved the following lower bound
Complexity:  Unknown
Cpx degree: ?

Solved cost: 0
Rule cost:   0