WORST_CASE(Omega(0),?)

Initial ITS
Start location: l15
   0: l0 -> l1 : __const_100^0'=__const_100^post0, Index7^0'=Index7^post0, fact3^0'=fact3^post0, Temp6^0'=Temp6^post0, Index2^0'=Index2^post0, i8^0'=i8^post0, __const_99^0'=__const_99^post0, Sorted5^0'=Sorted5^post0, factor^0'=factor^post0, (Sorted5^post0 == 0 /\ Index2^0-Index2^post0 == 0 /\ -factor^post0+factor^0 == 0 /\ -1+i8^post0 == 0 /\ 1+__const_100^0-Index2^0 <= 0 /\ fact3^0-fact3^post0 == 0 /\ __const_100^0-__const_100^post0 == 0 /\ Index7^0-Index7^post0 == 0 /\ -__const_99^post0+__const_99^0 == 0 /\ Temp6^0-Temp6^post0 == 0), cost: 1
   1: l0 -> l2 : __const_100^0'=__const_100^post1, Index7^0'=Index7^post1, fact3^0'=fact3^post1, Temp6^0'=Temp6^post1, Index2^0'=Index2^post1, i8^0'=i8^post1, __const_99^0'=__const_99^post1, Sorted5^0'=Sorted5^post1, factor^0'=factor^post1, (-factor^post1+factor^0 == 0 /\ -Sorted5^post1+Sorted5^0 == 0 /\ -1+Index2^post1-Index2^0 == 0 /\ -__const_99^post1+__const_99^0 == 0 /\ __const_100^0-__const_100^post1 == 0 /\ fact3^0-fact3^post1 == 0 /\ -Index7^post1+Index7^0 == 0 /\ -i8^post1+i8^0 == 0 /\ Temp6^0-Temp6^post1 == 0 /\ -__const_100^0+Index2^0 <= 0), cost: 1
  10: l1 -> l10 : __const_100^0'=__const_100^post10, Index7^0'=Index7^post10, fact3^0'=fact3^post10, Temp6^0'=Temp6^post10, Index2^0'=Index2^post10, i8^0'=i8^post10, __const_99^0'=__const_99^post10, Sorted5^0'=Sorted5^post10, factor^0'=factor^post10, (fact3^0-fact3^post10 == 0 /\ -factor^post10+factor^0 == 0 /\ Temp6^0-Temp6^post10 == 0 /\ -i8^post10+i8^0 == 0 /\ Sorted5^0-Sorted5^post10 == 0 /\ Index7^0-Index7^post10 == 0 /\ -__const_99^post10+__const_99^0 == 0 /\ -Index2^post10+Index2^0 == 0 /\ __const_100^0-__const_100^post10 == 0), cost: 1
   2: l2 -> l0 : __const_100^0'=__const_100^post2, Index7^0'=Index7^post2, fact3^0'=fact3^post2, Temp6^0'=Temp6^post2, Index2^0'=Index2^post2, i8^0'=i8^post2, __const_99^0'=__const_99^post2, Sorted5^0'=Sorted5^post2, factor^0'=factor^post2, (Index7^0-Index7^post2 == 0 /\ Sorted5^0-Sorted5^post2 == 0 /\ -factor^post2+factor^0 == 0 /\ Temp6^0-Temp6^post2 == 0 /\ -i8^post2+i8^0 == 0 /\ __const_100^0-__const_100^post2 == 0 /\ fact3^0-fact3^post2 == 0 /\ __const_99^0-__const_99^post2 == 0 /\ -Index2^post2+Index2^0 == 0), cost: 1
   3: l3 -> l4 : __const_100^0'=__const_100^post3, Index7^0'=Index7^post3, fact3^0'=fact3^post3, Temp6^0'=Temp6^post3, Index2^0'=Index2^post3, i8^0'=i8^post3, __const_99^0'=__const_99^post3, Sorted5^0'=Sorted5^post3, factor^0'=factor^post3, (-Sorted5^post3+Sorted5^0 == 0 /\ -__const_99^post3+__const_99^0 == 0 /\ -factor^post3+factor^0 == 0 /\ -Temp6^post3+Temp6^0 == 0 /\ Index2^0-Index2^post3 == 0 /\ __const_100^0-__const_100^post3 == 0 /\ -fact3^post3+fact3^0 == 0 /\ Index7^0-Index7^post3 == 0 /\ -i8^post3+i8^0 == 0), cost: 1
   4: l5 -> l3 : __const_100^0'=__const_100^post4, Index7^0'=Index7^post4, fact3^0'=fact3^post4, Temp6^0'=Temp6^post4, Index2^0'=Index2^post4, i8^0'=i8^post4, __const_99^0'=__const_99^post4, Sorted5^0'=Sorted5^post4, factor^0'=factor^post4, (__const_100^0-__const_100^post4 == 0 /\ -__const_99^post4+__const_99^0 == 0 /\ -fact3^post4+fact3^0 == 0 /\ i8^0-i8^post4 == 0 /\ -Temp6^post4+Temp6^0 == 0 /\ -Sorted5^post4+Sorted5^0 == 0 /\ -factor^post4+factor^0 == 0 /\ Index2^0-Index2^post4 == 0 /\ Index7^0-Index7^post4 == 0), cost: 1
   5: l6 -> l7 : __const_100^0'=__const_100^post5, Index7^0'=Index7^post5, fact3^0'=fact3^post5, Temp6^0'=Temp6^post5, Index2^0'=Index2^post5, i8^0'=i8^post5, __const_99^0'=__const_99^post5, Sorted5^0'=Sorted5^post5, factor^0'=factor^post5, (-Temp6^post5+Temp6^0 == 0 /\ -Index7^post5+Index7^0 == 0 /\ -factor^post5+factor^0 == 0 /\ i8^0-i8^post5 == 0 /\ -Sorted5^post5+Sorted5^0 == 0 /\ __const_100^0-__const_100^post5 == 0 /\ fact3^0-fact3^post5 == 0 /\ -__const_99^post5+__const_99^0 == 0 /\ Index2^0-Index2^post5 == 0), cost: 1
   6: l7 -> l1 : __const_100^0'=__const_100^post6, Index7^0'=Index7^post6, fact3^0'=fact3^post6, Temp6^0'=Temp6^post6, Index2^0'=Index2^post6, i8^0'=i8^post6, __const_99^0'=__const_99^post6, Sorted5^0'=Sorted5^post6, factor^0'=factor^post6, (fact3^0-fact3^post6 == 0 /\ -Sorted5^0 <= 0 /\ -factor^post6+factor^0 == 0 /\ Sorted5^0-Sorted5^post6 == 0 /\ -1+i8^post6-i8^0 == 0 /\ Index7^0-Index7^post6 == 0 /\ Temp6^0-Temp6^post6 == 0 /\ Sorted5^0 <= 0 /\ __const_100^0-__const_100^post6 == 0 /\ __const_99^0-__const_99^post6 == 0 /\ -Index2^post6+Index2^0 == 0), cost: 1
   7: l7 -> l5 : __const_100^0'=__const_100^post7, Index7^0'=Index7^post7, fact3^0'=fact3^post7, Temp6^0'=Temp6^post7, Index2^0'=Index2^post7, i8^0'=i8^post7, __const_99^0'=__const_99^post7, Sorted5^0'=Sorted5^post7, factor^0'=factor^post7, (Index7^0-Index7^post7 == 0 /\ -fact3^post7+fact3^0 == 0 /\ -i8^post7+i8^0 == 0 /\ 1-Sorted5^0 <= 0 /\ -Index2^post7+Index2^0 == 0 /\ __const_99^0-__const_99^post7 == 0 /\ -Sorted5^post7+Sorted5^0 == 0 /\ -factor^post7+factor^0 == 0 /\ Temp6^0-Temp6^post7 == 0 /\ -__const_100^post7+__const_100^0 == 0), cost: 1
   8: l7 -> l5 : __const_100^0'=__const_100^post8, Index7^0'=Index7^post8, fact3^0'=fact3^post8, Temp6^0'=Temp6^post8, Index2^0'=Index2^post8, i8^0'=i8^post8, __const_99^0'=__const_99^post8, Sorted5^0'=Sorted5^post8, factor^0'=factor^post8, (-Sorted5^post8+Sorted5^0 == 0 /\ -factor^post8+factor^0 == 0 /\ Index7^0-Index7^post8 == 0 /\ Index2^0-Index2^post8 == 0 /\ __const_99^0-__const_99^post8 == 0 /\ __const_100^0-__const_100^post8 == 0 /\ -Temp6^post8+Temp6^0 == 0 /\ 1+Sorted5^0 <= 0 /\ -fact3^post8+fact3^0 == 0 /\ -i8^post8+i8^0 == 0), cost: 1
   9: l8 -> l9 : __const_100^0'=__const_100^post9, Index7^0'=Index7^post9, fact3^0'=fact3^post9, Temp6^0'=Temp6^post9, Index2^0'=Index2^post9, i8^0'=i8^post9, __const_99^0'=__const_99^post9, Sorted5^0'=Sorted5^post9, factor^0'=factor^post9, (-factor^post9+factor^0 == 0 /\ -Sorted5^post9+Sorted5^0 == 0 /\ Index2^0-Index2^post9 == 0 /\ -1+Index7^post9-Index7^0 == 0 /\ -__const_99^post9+__const_99^0 == 0 /\ i8^0-i8^post9 == 0 /\ fact3^0-fact3^post9 == 0 /\ -Temp6^post9+Temp6^0 == 0 /\ __const_100^0-__const_100^post9 == 0), cost: 1
  17: l9 -> l13 : __const_100^0'=__const_100^post17, Index7^0'=Index7^post17, fact3^0'=fact3^post17, Temp6^0'=Temp6^post17, Index2^0'=Index2^post17, i8^0'=i8^post17, __const_99^0'=__const_99^post17, Sorted5^0'=Sorted5^post17, factor^0'=factor^post17, (-fact3^post17+fact3^0 == 0 /\ Index2^0-Index2^post17 == 0 /\ i8^0-i8^post17 == 0 /\ -factor^post17+factor^0 == 0 /\ -__const_99^post17+__const_99^0 == 0 /\ Index7^0-Index7^post17 == 0 /\ -Temp6^post17+Temp6^0 == 0 /\ -Sorted5^post17+Sorted5^0 == 0 /\ __const_100^0-__const_100^post17 == 0), cost: 1
  18: l10 -> l3 : __const_100^0'=__const_100^post18, Index7^0'=Index7^post18, fact3^0'=fact3^post18, Temp6^0'=Temp6^post18, Index2^0'=Index2^post18, i8^0'=i8^post18, __const_99^0'=__const_99^post18, Sorted5^0'=Sorted5^post18, factor^0'=factor^post18, (Index7^0-Index7^post18 == 0 /\ -factor^post18+factor^0 == 0 /\ -__const_99^post18+__const_99^0 == 0 /\ __const_100^0-__const_100^post18 == 0 /\ Index2^0-Index2^post18 == 0 /\ i8^0-i8^post18 == 0 /\ Temp6^0-Temp6^post18 == 0 /\ fact3^0-fact3^post18 == 0 /\ -Sorted5^post18+Sorted5^0 == 0 /\ 1-i8^0+__const_99^0 <= 0), cost: 1
  19: l10 -> l9 : __const_100^0'=__const_100^post19, Index7^0'=Index7^post19, fact3^0'=fact3^post19, Temp6^0'=Temp6^post19, Index2^0'=Index2^post19, i8^0'=i8^post19, __const_99^0'=__const_99^post19, Sorted5^0'=Sorted5^post19, factor^0'=factor^post19, (-Index2^post19+Index2^0 == 0 /\ -__const_99^post19+__const_99^0 == 0 /\ -factor^post19+factor^0 == 0 /\ __const_100^0-__const_100^post19 == 0 /\ fact3^0-fact3^post19 == 0 /\ Temp6^0-Temp6^post19 == 0 /\ i8^0-__const_99^0 <= 0 /\ -1+Sorted5^post19 == 0 /\ -i8^post19+i8^0 == 0 /\ -1+Index7^post19 == 0), cost: 1
  11: l11 -> l8 : __const_100^0'=__const_100^post11, Index7^0'=Index7^post11, fact3^0'=fact3^post11, Temp6^0'=Temp6^post11, Index2^0'=Index2^post11, i8^0'=i8^post11, __const_99^0'=__const_99^post11, Sorted5^0'=Sorted5^post11, factor^0'=factor^post11, (0 == 0 /\ -i8^post11+i8^0 == 0 /\ __const_99^0-__const_99^post11 == 0 /\ -factor^post11+factor^0 == 0 /\ Index7^0-Index7^post11 == 0 /\ -Index2^post11+Index2^0 == 0 /\ Sorted5^post11 == 0 /\ __const_100^0-__const_100^post11 == 0 /\ fact3^0-fact3^post11 == 0), cost: 1
  12: l11 -> l8 : __const_100^0'=__const_100^post12, Index7^0'=Index7^post12, fact3^0'=fact3^post12, Temp6^0'=Temp6^post12, Index2^0'=Index2^post12, i8^0'=i8^post12, __const_99^0'=__const_99^post12, Sorted5^0'=Sorted5^post12, factor^0'=factor^post12, (-factor^post12+factor^0 == 0 /\ Index7^0-Index7^post12 == 0 /\ -Sorted5^post12+Sorted5^0 == 0 /\ Index2^0-Index2^post12 == 0 /\ __const_99^0-__const_99^post12 == 0 /\ -Temp6^post12+Temp6^0 == 0 /\ __const_100^0-__const_100^post12 == 0 /\ -i8^post12+i8^0 == 0 /\ -fact3^post12+fact3^0 == 0), cost: 1
  13: l12 -> l11 : __const_100^0'=__const_100^post13, Index7^0'=Index7^post13, fact3^0'=fact3^post13, Temp6^0'=Temp6^post13, Index2^0'=Index2^post13, i8^0'=i8^post13, __const_99^0'=__const_99^post13, Sorted5^0'=Sorted5^post13, factor^0'=factor^post13, (-Sorted5^post13+Sorted5^0 == 0 /\ -__const_100^0+Index7^0+i8^0 <= 0 /\ Index7^0-Index7^post13 == 0 /\ -__const_99^post13+__const_99^0 == 0 /\ i8^0-i8^post13 == 0 /\ -Temp6^post13+Temp6^0 == 0 /\ __const_100^0-__const_100^post13 == 0 /\ fact3^0-fact3^post13 == 0 /\ -factor^post13+factor^0 == 0 /\ Index2^0-Index2^post13 == 0), cost: 1
  14: l12 -> l6 : __const_100^0'=__const_100^post14, Index7^0'=Index7^post14, fact3^0'=fact3^post14, Temp6^0'=Temp6^post14, Index2^0'=Index2^post14, i8^0'=i8^post14, __const_99^0'=__const_99^post14, Sorted5^0'=Sorted5^post14, factor^0'=factor^post14, (1+__const_100^0-Index7^0-i8^0 <= 0 /\ -__const_99^post14+__const_99^0 == 0 /\ -Index2^post14+Index2^0 == 0 /\ __const_100^0-__const_100^post14 == 0 /\ fact3^0-fact3^post14 == 0 /\ -Sorted5^post14+Sorted5^0 == 0 /\ Temp6^0-Temp6^post14 == 0 /\ Index7^0-Index7^post14 == 0 /\ -factor^post14+factor^0 == 0 /\ -i8^post14+i8^0 == 0), cost: 1
  15: l13 -> l6 : __const_100^0'=__const_100^post15, Index7^0'=Index7^post15, fact3^0'=fact3^post15, Temp6^0'=Temp6^post15, Index2^0'=Index2^post15, i8^0'=i8^post15, __const_99^0'=__const_99^post15, Sorted5^0'=Sorted5^post15, factor^0'=factor^post15, (__const_100^0-__const_100^post15 == 0 /\ fact3^0-fact3^post15 == 0 /\ 1-Index7^0+__const_99^0 <= 0 /\ Sorted5^0-Sorted5^post15 == 0 /\ Temp6^0-Temp6^post15 == 0 /\ -Index2^post15+Index2^0 == 0 /\ -__const_99^post15+__const_99^0 == 0 /\ -factor^post15+factor^0 == 0 /\ -i8^post15+i8^0 == 0 /\ Index7^0-Index7^post15 == 0), cost: 1
  16: l13 -> l12 : __const_100^0'=__const_100^post16, Index7^0'=Index7^post16, fact3^0'=fact3^post16, Temp6^0'=Temp6^post16, Index2^0'=Index2^post16, i8^0'=i8^post16, __const_99^0'=__const_99^post16, Sorted5^0'=Sorted5^post16, factor^0'=factor^post16, (Index7^0-Index7^post16 == 0 /\ -i8^post16+i8^0 == 0 /\ -fact3^post16+fact3^0 == 0 /\ Index7^0-__const_99^0 <= 0 /\ __const_99^0-__const_99^post16 == 0 /\ -factor^post16+factor^0 == 0 /\ -Index2^post16+Index2^0 == 0 /\ __const_100^0-__const_100^post16 == 0 /\ -Sorted5^post16+Sorted5^0 == 0 /\ Temp6^0-Temp6^post16 == 0), cost: 1
  20: l14 -> l2 : __const_100^0'=__const_100^post20, Index7^0'=Index7^post20, fact3^0'=fact3^post20, Temp6^0'=Temp6^post20, Index2^0'=Index2^post20, i8^0'=i8^post20, __const_99^0'=__const_99^post20, Sorted5^0'=Sorted5^post20, factor^0'=factor^post20, (Temp6^0-Temp6^post20 == 0 /\ fact3^post20-factor^post20 == 0 /\ Index7^0-Index7^post20 == 0 /\ -1+Index2^post20 == 0 /\ -Sorted5^post20+Sorted5^0 == 0 /\ __const_100^0-__const_100^post20 == 0 /\ -i8^post20+i8^0 == 0 /\ __const_99^0-__const_99^post20 == 0 /\ 1+factor^post20 == 0), cost: 1
  21: l15 -> l14 : __const_100^0'=__const_100^post21, Index7^0'=Index7^post21, fact3^0'=fact3^post21, Temp6^0'=Temp6^post21, Index2^0'=Index2^post21, i8^0'=i8^post21, __const_99^0'=__const_99^post21, Sorted5^0'=Sorted5^post21, factor^0'=factor^post21, (i8^0-i8^post21 == 0 /\ __const_100^0-__const_100^post21 == 0 /\ -Temp6^post21+Temp6^0 == 0 /\ -Sorted5^post21+Sorted5^0 == 0 /\ Index2^0-Index2^post21 == 0 /\ -fact3^post21+fact3^0 == 0 /\ Index7^0-Index7^post21 == 0 /\ -factor^post21+factor^0 == 0 /\ -__const_99^post21+__const_99^0 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l15
   0: l0 -> l1 : __const_100^0'=__const_100^post0, Index7^0'=Index7^post0, fact3^0'=fact3^post0, Temp6^0'=Temp6^post0, Index2^0'=Index2^post0, i8^0'=i8^post0, __const_99^0'=__const_99^post0, Sorted5^0'=Sorted5^post0, factor^0'=factor^post0, (Sorted5^post0 == 0 /\ Index2^0-Index2^post0 == 0 /\ -factor^post0+factor^0 == 0 /\ -1+i8^post0 == 0 /\ 1+__const_100^0-Index2^0 <= 0 /\ fact3^0-fact3^post0 == 0 /\ __const_100^0-__const_100^post0 == 0 /\ Index7^0-Index7^post0 == 0 /\ -__const_99^post0+__const_99^0 == 0 /\ Temp6^0-Temp6^post0 == 0), cost: 1
   1: l0 -> l2 : __const_100^0'=__const_100^post1, Index7^0'=Index7^post1, fact3^0'=fact3^post1, Temp6^0'=Temp6^post1, Index2^0'=Index2^post1, i8^0'=i8^post1, __const_99^0'=__const_99^post1, Sorted5^0'=Sorted5^post1, factor^0'=factor^post1, (-factor^post1+factor^0 == 0 /\ -Sorted5^post1+Sorted5^0 == 0 /\ -1+Index2^post1-Index2^0 == 0 /\ -__const_99^post1+__const_99^0 == 0 /\ __const_100^0-__const_100^post1 == 0 /\ fact3^0-fact3^post1 == 0 /\ -Index7^post1+Index7^0 == 0 /\ -i8^post1+i8^0 == 0 /\ Temp6^0-Temp6^post1 == 0 /\ -__const_100^0+Index2^0 <= 0), cost: 1
  10: l1 -> l10 : __const_100^0'=__const_100^post10, Index7^0'=Index7^post10, fact3^0'=fact3^post10, Temp6^0'=Temp6^post10, Index2^0'=Index2^post10, i8^0'=i8^post10, __const_99^0'=__const_99^post10, Sorted5^0'=Sorted5^post10, factor^0'=factor^post10, (fact3^0-fact3^post10 == 0 /\ -factor^post10+factor^0 == 0 /\ Temp6^0-Temp6^post10 == 0 /\ -i8^post10+i8^0 == 0 /\ Sorted5^0-Sorted5^post10 == 0 /\ Index7^0-Index7^post10 == 0 /\ -__const_99^post10+__const_99^0 == 0 /\ -Index2^post10+Index2^0 == 0 /\ __const_100^0-__const_100^post10 == 0), cost: 1
   2: l2 -> l0 : __const_100^0'=__const_100^post2, Index7^0'=Index7^post2, fact3^0'=fact3^post2, Temp6^0'=Temp6^post2, Index2^0'=Index2^post2, i8^0'=i8^post2, __const_99^0'=__const_99^post2, Sorted5^0'=Sorted5^post2, factor^0'=factor^post2, (Index7^0-Index7^post2 == 0 /\ Sorted5^0-Sorted5^post2 == 0 /\ -factor^post2+factor^0 == 0 /\ Temp6^0-Temp6^post2 == 0 /\ -i8^post2+i8^0 == 0 /\ __const_100^0-__const_100^post2 == 0 /\ fact3^0-fact3^post2 == 0 /\ __const_99^0-__const_99^post2 == 0 /\ -Index2^post2+Index2^0 == 0), cost: 1
   5: l6 -> l7 : __const_100^0'=__const_100^post5, Index7^0'=Index7^post5, fact3^0'=fact3^post5, Temp6^0'=Temp6^post5, Index2^0'=Index2^post5, i8^0'=i8^post5, __const_99^0'=__const_99^post5, Sorted5^0'=Sorted5^post5, factor^0'=factor^post5, (-Temp6^post5+Temp6^0 == 0 /\ -Index7^post5+Index7^0 == 0 /\ -factor^post5+factor^0 == 0 /\ i8^0-i8^post5 == 0 /\ -Sorted5^post5+Sorted5^0 == 0 /\ __const_100^0-__const_100^post5 == 0 /\ fact3^0-fact3^post5 == 0 /\ -__const_99^post5+__const_99^0 == 0 /\ Index2^0-Index2^post5 == 0), cost: 1
   6: l7 -> l1 : __const_100^0'=__const_100^post6, Index7^0'=Index7^post6, fact3^0'=fact3^post6, Temp6^0'=Temp6^post6, Index2^0'=Index2^post6, i8^0'=i8^post6, __const_99^0'=__const_99^post6, Sorted5^0'=Sorted5^post6, factor^0'=factor^post6, (fact3^0-fact3^post6 == 0 /\ -Sorted5^0 <= 0 /\ -factor^post6+factor^0 == 0 /\ Sorted5^0-Sorted5^post6 == 0 /\ -1+i8^post6-i8^0 == 0 /\ Index7^0-Index7^post6 == 0 /\ Temp6^0-Temp6^post6 == 0 /\ Sorted5^0 <= 0 /\ __const_100^0-__const_100^post6 == 0 /\ __const_99^0-__const_99^post6 == 0 /\ -Index2^post6+Index2^0 == 0), cost: 1
   9: l8 -> l9 : __const_100^0'=__const_100^post9, Index7^0'=Index7^post9, fact3^0'=fact3^post9, Temp6^0'=Temp6^post9, Index2^0'=Index2^post9, i8^0'=i8^post9, __const_99^0'=__const_99^post9, Sorted5^0'=Sorted5^post9, factor^0'=factor^post9, (-factor^post9+factor^0 == 0 /\ -Sorted5^post9+Sorted5^0 == 0 /\ Index2^0-Index2^post9 == 0 /\ -1+Index7^post9-Index7^0 == 0 /\ -__const_99^post9+__const_99^0 == 0 /\ i8^0-i8^post9 == 0 /\ fact3^0-fact3^post9 == 0 /\ -Temp6^post9+Temp6^0 == 0 /\ __const_100^0-__const_100^post9 == 0), cost: 1
  17: l9 -> l13 : __const_100^0'=__const_100^post17, Index7^0'=Index7^post17, fact3^0'=fact3^post17, Temp6^0'=Temp6^post17, Index2^0'=Index2^post17, i8^0'=i8^post17, __const_99^0'=__const_99^post17, Sorted5^0'=Sorted5^post17, factor^0'=factor^post17, (-fact3^post17+fact3^0 == 0 /\ Index2^0-Index2^post17 == 0 /\ i8^0-i8^post17 == 0 /\ -factor^post17+factor^0 == 0 /\ -__const_99^post17+__const_99^0 == 0 /\ Index7^0-Index7^post17 == 0 /\ -Temp6^post17+Temp6^0 == 0 /\ -Sorted5^post17+Sorted5^0 == 0 /\ __const_100^0-__const_100^post17 == 0), cost: 1
  19: l10 -> l9 : __const_100^0'=__const_100^post19, Index7^0'=Index7^post19, fact3^0'=fact3^post19, Temp6^0'=Temp6^post19, Index2^0'=Index2^post19, i8^0'=i8^post19, __const_99^0'=__const_99^post19, Sorted5^0'=Sorted5^post19, factor^0'=factor^post19, (-Index2^post19+Index2^0 == 0 /\ -__const_99^post19+__const_99^0 == 0 /\ -factor^post19+factor^0 == 0 /\ __const_100^0-__const_100^post19 == 0 /\ fact3^0-fact3^post19 == 0 /\ Temp6^0-Temp6^post19 == 0 /\ i8^0-__const_99^0 <= 0 /\ -1+Sorted5^post19 == 0 /\ -i8^post19+i8^0 == 0 /\ -1+Index7^post19 == 0), cost: 1
  11: l11 -> l8 : __const_100^0'=__const_100^post11, Index7^0'=Index7^post11, fact3^0'=fact3^post11, Temp6^0'=Temp6^post11, Index2^0'=Index2^post11, i8^0'=i8^post11, __const_99^0'=__const_99^post11, Sorted5^0'=Sorted5^post11, factor^0'=factor^post11, (0 == 0 /\ -i8^post11+i8^0 == 0 /\ __const_99^0-__const_99^post11 == 0 /\ -factor^post11+factor^0 == 0 /\ Index7^0-Index7^post11 == 0 /\ -Index2^post11+Index2^0 == 0 /\ Sorted5^post11 == 0 /\ __const_100^0-__const_100^post11 == 0 /\ fact3^0-fact3^post11 == 0), cost: 1
  12: l11 -> l8 : __const_100^0'=__const_100^post12, Index7^0'=Index7^post12, fact3^0'=fact3^post12, Temp6^0'=Temp6^post12, Index2^0'=Index2^post12, i8^0'=i8^post12, __const_99^0'=__const_99^post12, Sorted5^0'=Sorted5^post12, factor^0'=factor^post12, (-factor^post12+factor^0 == 0 /\ Index7^0-Index7^post12 == 0 /\ -Sorted5^post12+Sorted5^0 == 0 /\ Index2^0-Index2^post12 == 0 /\ __const_99^0-__const_99^post12 == 0 /\ -Temp6^post12+Temp6^0 == 0 /\ __const_100^0-__const_100^post12 == 0 /\ -i8^post12+i8^0 == 0 /\ -fact3^post12+fact3^0 == 0), cost: 1
  13: l12 -> l11 : __const_100^0'=__const_100^post13, Index7^0'=Index7^post13, fact3^0'=fact3^post13, Temp6^0'=Temp6^post13, Index2^0'=Index2^post13, i8^0'=i8^post13, __const_99^0'=__const_99^post13, Sorted5^0'=Sorted5^post13, factor^0'=factor^post13, (-Sorted5^post13+Sorted5^0 == 0 /\ -__const_100^0+Index7^0+i8^0 <= 0 /\ Index7^0-Index7^post13 == 0 /\ -__const_99^post13+__const_99^0 == 0 /\ i8^0-i8^post13 == 0 /\ -Temp6^post13+Temp6^0 == 0 /\ __const_100^0-__const_100^post13 == 0 /\ fact3^0-fact3^post13 == 0 /\ -factor^post13+factor^0 == 0 /\ Index2^0-Index2^post13 == 0), cost: 1
  14: l12 -> l6 : __const_100^0'=__const_100^post14, Index7^0'=Index7^post14, fact3^0'=fact3^post14, Temp6^0'=Temp6^post14, Index2^0'=Index2^post14, i8^0'=i8^post14, __const_99^0'=__const_99^post14, Sorted5^0'=Sorted5^post14, factor^0'=factor^post14, (1+__const_100^0-Index7^0-i8^0 <= 0 /\ -__const_99^post14+__const_99^0 == 0 /\ -Index2^post14+Index2^0 == 0 /\ __const_100^0-__const_100^post14 == 0 /\ fact3^0-fact3^post14 == 0 /\ -Sorted5^post14+Sorted5^0 == 0 /\ Temp6^0-Temp6^post14 == 0 /\ Index7^0-Index7^post14 == 0 /\ -factor^post14+factor^0 == 0 /\ -i8^post14+i8^0 == 0), cost: 1
  15: l13 -> l6 : __const_100^0'=__const_100^post15, Index7^0'=Index7^post15, fact3^0'=fact3^post15, Temp6^0'=Temp6^post15, Index2^0'=Index2^post15, i8^0'=i8^post15, __const_99^0'=__const_99^post15, Sorted5^0'=Sorted5^post15, factor^0'=factor^post15, (__const_100^0-__const_100^post15 == 0 /\ fact3^0-fact3^post15 == 0 /\ 1-Index7^0+__const_99^0 <= 0 /\ Sorted5^0-Sorted5^post15 == 0 /\ Temp6^0-Temp6^post15 == 0 /\ -Index2^post15+Index2^0 == 0 /\ -__const_99^post15+__const_99^0 == 0 /\ -factor^post15+factor^0 == 0 /\ -i8^post15+i8^0 == 0 /\ Index7^0-Index7^post15 == 0), cost: 1
  16: l13 -> l12 : __const_100^0'=__const_100^post16, Index7^0'=Index7^post16, fact3^0'=fact3^post16, Temp6^0'=Temp6^post16, Index2^0'=Index2^post16, i8^0'=i8^post16, __const_99^0'=__const_99^post16, Sorted5^0'=Sorted5^post16, factor^0'=factor^post16, (Index7^0-Index7^post16 == 0 /\ -i8^post16+i8^0 == 0 /\ -fact3^post16+fact3^0 == 0 /\ Index7^0-__const_99^0 <= 0 /\ __const_99^0-__const_99^post16 == 0 /\ -factor^post16+factor^0 == 0 /\ -Index2^post16+Index2^0 == 0 /\ __const_100^0-__const_100^post16 == 0 /\ -Sorted5^post16+Sorted5^0 == 0 /\ Temp6^0-Temp6^post16 == 0), cost: 1
  20: l14 -> l2 : __const_100^0'=__const_100^post20, Index7^0'=Index7^post20, fact3^0'=fact3^post20, Temp6^0'=Temp6^post20, Index2^0'=Index2^post20, i8^0'=i8^post20, __const_99^0'=__const_99^post20, Sorted5^0'=Sorted5^post20, factor^0'=factor^post20, (Temp6^0-Temp6^post20 == 0 /\ fact3^post20-factor^post20 == 0 /\ Index7^0-Index7^post20 == 0 /\ -1+Index2^post20 == 0 /\ -Sorted5^post20+Sorted5^0 == 0 /\ __const_100^0-__const_100^post20 == 0 /\ -i8^post20+i8^0 == 0 /\ __const_99^0-__const_99^post20 == 0 /\ 1+factor^post20 == 0), cost: 1
  21: l15 -> l14 : __const_100^0'=__const_100^post21, Index7^0'=Index7^post21, fact3^0'=fact3^post21, Temp6^0'=Temp6^post21, Index2^0'=Index2^post21, i8^0'=i8^post21, __const_99^0'=__const_99^post21, Sorted5^0'=Sorted5^post21, factor^0'=factor^post21, (i8^0-i8^post21 == 0 /\ __const_100^0-__const_100^post21 == 0 /\ -Temp6^post21+Temp6^0 == 0 /\ -Sorted5^post21+Sorted5^0 == 0 /\ Index2^0-Index2^post21 == 0 /\ -fact3^post21+fact3^0 == 0 /\ Index7^0-Index7^post21 == 0 /\ -factor^post21+factor^0 == 0 /\ -__const_99^post21+__const_99^0 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : __const_100^0'=__const_100^post0, Index7^0'=Index7^post0, fact3^0'=fact3^post0, Temp6^0'=Temp6^post0, Index2^0'=Index2^post0, i8^0'=i8^post0, __const_99^0'=__const_99^post0, Sorted5^0'=Sorted5^post0, factor^0'=factor^post0, (Sorted5^post0 == 0 /\ Index2^0-Index2^post0 == 0 /\ -factor^post0+factor^0 == 0 /\ -1+i8^post0 == 0 /\ 1+__const_100^0-Index2^0 <= 0 /\ fact3^0-fact3^post0 == 0 /\ __const_100^0-__const_100^post0 == 0 /\ Index7^0-Index7^post0 == 0 /\ -__const_99^post0+__const_99^0 == 0 /\ Temp6^0-Temp6^post0 == 0), cost: 1
New rule:
l0 -> l1 : i8^0'=1, Sorted5^0'=0, 1+__const_100^0-Index2^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l0 -> l2 : __const_100^0'=__const_100^post1, Index7^0'=Index7^post1, fact3^0'=fact3^post1, Temp6^0'=Temp6^post1, Index2^0'=Index2^post1, i8^0'=i8^post1, __const_99^0'=__const_99^post1, Sorted5^0'=Sorted5^post1, factor^0'=factor^post1, (-factor^post1+factor^0 == 0 /\ -Sorted5^post1+Sorted5^0 == 0 /\ -1+Index2^post1-Index2^0 == 0 /\ -__const_99^post1+__const_99^0 == 0 /\ __const_100^0-__const_100^post1 == 0 /\ fact3^0-fact3^post1 == 0 /\ -Index7^post1+Index7^0 == 0 /\ -i8^post1+i8^0 == 0 /\ Temp6^0-Temp6^post1 == 0 /\ -__const_100^0+Index2^0 <= 0), cost: 1
New rule:
l0 -> l2 : Index2^0'=1+Index2^0, -__const_100^0+Index2^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l0 : __const_100^0'=__const_100^post2, Index7^0'=Index7^post2, fact3^0'=fact3^post2, Temp6^0'=Temp6^post2, Index2^0'=Index2^post2, i8^0'=i8^post2, __const_99^0'=__const_99^post2, Sorted5^0'=Sorted5^post2, factor^0'=factor^post2, (Index7^0-Index7^post2 == 0 /\ Sorted5^0-Sorted5^post2 == 0 /\ -factor^post2+factor^0 == 0 /\ Temp6^0-Temp6^post2 == 0 /\ -i8^post2+i8^0 == 0 /\ __const_100^0-__const_100^post2 == 0 /\ fact3^0-fact3^post2 == 0 /\ __const_99^0-__const_99^post2 == 0 /\ -Index2^post2+Index2^0 == 0), cost: 1
New rule:
l2 -> l0 : TRUE, cost: 1

Applied preprocessing
Original rule:
l6 -> l7 : __const_100^0'=__const_100^post5, Index7^0'=Index7^post5, fact3^0'=fact3^post5, Temp6^0'=Temp6^post5, Index2^0'=Index2^post5, i8^0'=i8^post5, __const_99^0'=__const_99^post5, Sorted5^0'=Sorted5^post5, factor^0'=factor^post5, (-Temp6^post5+Temp6^0 == 0 /\ -Index7^post5+Index7^0 == 0 /\ -factor^post5+factor^0 == 0 /\ i8^0-i8^post5 == 0 /\ -Sorted5^post5+Sorted5^0 == 0 /\ __const_100^0-__const_100^post5 == 0 /\ fact3^0-fact3^post5 == 0 /\ -__const_99^post5+__const_99^0 == 0 /\ Index2^0-Index2^post5 == 0), cost: 1
New rule:
l6 -> l7 : TRUE, cost: 1

Applied preprocessing
Original rule:
l7 -> l1 : __const_100^0'=__const_100^post6, Index7^0'=Index7^post6, fact3^0'=fact3^post6, Temp6^0'=Temp6^post6, Index2^0'=Index2^post6, i8^0'=i8^post6, __const_99^0'=__const_99^post6, Sorted5^0'=Sorted5^post6, factor^0'=factor^post6, (fact3^0-fact3^post6 == 0 /\ -Sorted5^0 <= 0 /\ -factor^post6+factor^0 == 0 /\ Sorted5^0-Sorted5^post6 == 0 /\ -1+i8^post6-i8^0 == 0 /\ Index7^0-Index7^post6 == 0 /\ Temp6^0-Temp6^post6 == 0 /\ Sorted5^0 <= 0 /\ __const_100^0-__const_100^post6 == 0 /\ __const_99^0-__const_99^post6 == 0 /\ -Index2^post6+Index2^0 == 0), cost: 1
New rule:
l7 -> l1 : i8^0'=1+i8^0, Sorted5^0 == 0, cost: 1

Applied preprocessing
Original rule:
l8 -> l9 : __const_100^0'=__const_100^post9, Index7^0'=Index7^post9, fact3^0'=fact3^post9, Temp6^0'=Temp6^post9, Index2^0'=Index2^post9, i8^0'=i8^post9, __const_99^0'=__const_99^post9, Sorted5^0'=Sorted5^post9, factor^0'=factor^post9, (-factor^post9+factor^0 == 0 /\ -Sorted5^post9+Sorted5^0 == 0 /\ Index2^0-Index2^post9 == 0 /\ -1+Index7^post9-Index7^0 == 0 /\ -__const_99^post9+__const_99^0 == 0 /\ i8^0-i8^post9 == 0 /\ fact3^0-fact3^post9 == 0 /\ -Temp6^post9+Temp6^0 == 0 /\ __const_100^0-__const_100^post9 == 0), cost: 1
New rule:
l8 -> l9 : Index7^0'=1+Index7^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l1 -> l10 : __const_100^0'=__const_100^post10, Index7^0'=Index7^post10, fact3^0'=fact3^post10, Temp6^0'=Temp6^post10, Index2^0'=Index2^post10, i8^0'=i8^post10, __const_99^0'=__const_99^post10, Sorted5^0'=Sorted5^post10, factor^0'=factor^post10, (fact3^0-fact3^post10 == 0 /\ -factor^post10+factor^0 == 0 /\ Temp6^0-Temp6^post10 == 0 /\ -i8^post10+i8^0 == 0 /\ Sorted5^0-Sorted5^post10 == 0 /\ Index7^0-Index7^post10 == 0 /\ -__const_99^post10+__const_99^0 == 0 /\ -Index2^post10+Index2^0 == 0 /\ __const_100^0-__const_100^post10 == 0), cost: 1
New rule:
l1 -> l10 : TRUE, cost: 1

Applied preprocessing
Original rule:
l11 -> l8 : __const_100^0'=__const_100^post11, Index7^0'=Index7^post11, fact3^0'=fact3^post11, Temp6^0'=Temp6^post11, Index2^0'=Index2^post11, i8^0'=i8^post11, __const_99^0'=__const_99^post11, Sorted5^0'=Sorted5^post11, factor^0'=factor^post11, (0 == 0 /\ -i8^post11+i8^0 == 0 /\ __const_99^0-__const_99^post11 == 0 /\ -factor^post11+factor^0 == 0 /\ Index7^0-Index7^post11 == 0 /\ -Index2^post11+Index2^0 == 0 /\ Sorted5^post11 == 0 /\ __const_100^0-__const_100^post11 == 0 /\ fact3^0-fact3^post11 == 0), cost: 1
New rule:
l11 -> l8 : Temp6^0'=Temp6^post11, Sorted5^0'=0, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l11 -> l8 : __const_100^0'=__const_100^post12, Index7^0'=Index7^post12, fact3^0'=fact3^post12, Temp6^0'=Temp6^post12, Index2^0'=Index2^post12, i8^0'=i8^post12, __const_99^0'=__const_99^post12, Sorted5^0'=Sorted5^post12, factor^0'=factor^post12, (-factor^post12+factor^0 == 0 /\ Index7^0-Index7^post12 == 0 /\ -Sorted5^post12+Sorted5^0 == 0 /\ Index2^0-Index2^post12 == 0 /\ __const_99^0-__const_99^post12 == 0 /\ -Temp6^post12+Temp6^0 == 0 /\ __const_100^0-__const_100^post12 == 0 /\ -i8^post12+i8^0 == 0 /\ -fact3^post12+fact3^0 == 0), cost: 1
New rule:
l11 -> l8 : TRUE, cost: 1

Applied preprocessing
Original rule:
l12 -> l11 : __const_100^0'=__const_100^post13, Index7^0'=Index7^post13, fact3^0'=fact3^post13, Temp6^0'=Temp6^post13, Index2^0'=Index2^post13, i8^0'=i8^post13, __const_99^0'=__const_99^post13, Sorted5^0'=Sorted5^post13, factor^0'=factor^post13, (-Sorted5^post13+Sorted5^0 == 0 /\ -__const_100^0+Index7^0+i8^0 <= 0 /\ Index7^0-Index7^post13 == 0 /\ -__const_99^post13+__const_99^0 == 0 /\ i8^0-i8^post13 == 0 /\ -Temp6^post13+Temp6^0 == 0 /\ __const_100^0-__const_100^post13 == 0 /\ fact3^0-fact3^post13 == 0 /\ -factor^post13+factor^0 == 0 /\ Index2^0-Index2^post13 == 0), cost: 1
New rule:
l12 -> l11 : -__const_100^0+Index7^0+i8^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l12 -> l6 : __const_100^0'=__const_100^post14, Index7^0'=Index7^post14, fact3^0'=fact3^post14, Temp6^0'=Temp6^post14, Index2^0'=Index2^post14, i8^0'=i8^post14, __const_99^0'=__const_99^post14, Sorted5^0'=Sorted5^post14, factor^0'=factor^post14, (1+__const_100^0-Index7^0-i8^0 <= 0 /\ -__const_99^post14+__const_99^0 == 0 /\ -Index2^post14+Index2^0 == 0 /\ __const_100^0-__const_100^post14 == 0 /\ fact3^0-fact3^post14 == 0 /\ -Sorted5^post14+Sorted5^0 == 0 /\ Temp6^0-Temp6^post14 == 0 /\ Index7^0-Index7^post14 == 0 /\ -factor^post14+factor^0 == 0 /\ -i8^post14+i8^0 == 0), cost: 1
New rule:
l12 -> l6 : 1+__const_100^0-Index7^0-i8^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l13 -> l6 : __const_100^0'=__const_100^post15, Index7^0'=Index7^post15, fact3^0'=fact3^post15, Temp6^0'=Temp6^post15, Index2^0'=Index2^post15, i8^0'=i8^post15, __const_99^0'=__const_99^post15, Sorted5^0'=Sorted5^post15, factor^0'=factor^post15, (__const_100^0-__const_100^post15 == 0 /\ fact3^0-fact3^post15 == 0 /\ 1-Index7^0+__const_99^0 <= 0 /\ Sorted5^0-Sorted5^post15 == 0 /\ Temp6^0-Temp6^post15 == 0 /\ -Index2^post15+Index2^0 == 0 /\ -__const_99^post15+__const_99^0 == 0 /\ -factor^post15+factor^0 == 0 /\ -i8^post15+i8^0 == 0 /\ Index7^0-Index7^post15 == 0), cost: 1
New rule:
l13 -> l6 : 1-Index7^0+__const_99^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l13 -> l12 : __const_100^0'=__const_100^post16, Index7^0'=Index7^post16, fact3^0'=fact3^post16, Temp6^0'=Temp6^post16, Index2^0'=Index2^post16, i8^0'=i8^post16, __const_99^0'=__const_99^post16, Sorted5^0'=Sorted5^post16, factor^0'=factor^post16, (Index7^0-Index7^post16 == 0 /\ -i8^post16+i8^0 == 0 /\ -fact3^post16+fact3^0 == 0 /\ Index7^0-__const_99^0 <= 0 /\ __const_99^0-__const_99^post16 == 0 /\ -factor^post16+factor^0 == 0 /\ -Index2^post16+Index2^0 == 0 /\ __const_100^0-__const_100^post16 == 0 /\ -Sorted5^post16+Sorted5^0 == 0 /\ Temp6^0-Temp6^post16 == 0), cost: 1
New rule:
l13 -> l12 : Index7^0-__const_99^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l9 -> l13 : __const_100^0'=__const_100^post17, Index7^0'=Index7^post17, fact3^0'=fact3^post17, Temp6^0'=Temp6^post17, Index2^0'=Index2^post17, i8^0'=i8^post17, __const_99^0'=__const_99^post17, Sorted5^0'=Sorted5^post17, factor^0'=factor^post17, (-fact3^post17+fact3^0 == 0 /\ Index2^0-Index2^post17 == 0 /\ i8^0-i8^post17 == 0 /\ -factor^post17+factor^0 == 0 /\ -__const_99^post17+__const_99^0 == 0 /\ Index7^0-Index7^post17 == 0 /\ -Temp6^post17+Temp6^0 == 0 /\ -Sorted5^post17+Sorted5^0 == 0 /\ __const_100^0-__const_100^post17 == 0), cost: 1
New rule:
l9 -> l13 : TRUE, cost: 1

Applied preprocessing
Original rule:
l10 -> l9 : __const_100^0'=__const_100^post19, Index7^0'=Index7^post19, fact3^0'=fact3^post19, Temp6^0'=Temp6^post19, Index2^0'=Index2^post19, i8^0'=i8^post19, __const_99^0'=__const_99^post19, Sorted5^0'=Sorted5^post19, factor^0'=factor^post19, (-Index2^post19+Index2^0 == 0 /\ -__const_99^post19+__const_99^0 == 0 /\ -factor^post19+factor^0 == 0 /\ __const_100^0-__const_100^post19 == 0 /\ fact3^0-fact3^post19 == 0 /\ Temp6^0-Temp6^post19 == 0 /\ i8^0-__const_99^0 <= 0 /\ -1+Sorted5^post19 == 0 /\ -i8^post19+i8^0 == 0 /\ -1+Index7^post19 == 0), cost: 1
New rule:
l10 -> l9 : Index7^0'=1, Sorted5^0'=1, i8^0-__const_99^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l14 -> l2 : __const_100^0'=__const_100^post20, Index7^0'=Index7^post20, fact3^0'=fact3^post20, Temp6^0'=Temp6^post20, Index2^0'=Index2^post20, i8^0'=i8^post20, __const_99^0'=__const_99^post20, Sorted5^0'=Sorted5^post20, factor^0'=factor^post20, (Temp6^0-Temp6^post20 == 0 /\ fact3^post20-factor^post20 == 0 /\ Index7^0-Index7^post20 == 0 /\ -1+Index2^post20 == 0 /\ -Sorted5^post20+Sorted5^0 == 0 /\ __const_100^0-__const_100^post20 == 0 /\ -i8^post20+i8^0 == 0 /\ __const_99^0-__const_99^post20 == 0 /\ 1+factor^post20 == 0), cost: 1
New rule:
l14 -> l2 : fact3^0'=-1, Index2^0'=1, factor^0'=-1, TRUE, cost: 1

Applied preprocessing
Original rule:
l15 -> l14 : __const_100^0'=__const_100^post21, Index7^0'=Index7^post21, fact3^0'=fact3^post21, Temp6^0'=Temp6^post21, Index2^0'=Index2^post21, i8^0'=i8^post21, __const_99^0'=__const_99^post21, Sorted5^0'=Sorted5^post21, factor^0'=factor^post21, (i8^0-i8^post21 == 0 /\ __const_100^0-__const_100^post21 == 0 /\ -Temp6^post21+Temp6^0 == 0 /\ -Sorted5^post21+Sorted5^0 == 0 /\ Index2^0-Index2^post21 == 0 /\ -fact3^post21+fact3^0 == 0 /\ Index7^0-Index7^post21 == 0 /\ -factor^post21+factor^0 == 0 /\ -__const_99^post21+__const_99^0 == 0), cost: 1
New rule:
l15 -> l14 : TRUE, cost: 1

Simplified rules
Start location: l15
  22: l0 -> l1 : i8^0'=1, Sorted5^0'=0, 1+__const_100^0-Index2^0 <= 0, cost: 1
  23: l0 -> l2 : Index2^0'=1+Index2^0, -__const_100^0+Index2^0 <= 0, cost: 1
  28: l1 -> l10 : TRUE, cost: 1
  24: l2 -> l0 : TRUE, cost: 1
  25: l6 -> l7 : TRUE, cost: 1
  26: l7 -> l1 : i8^0'=1+i8^0, Sorted5^0 == 0, cost: 1
  27: l8 -> l9 : Index7^0'=1+Index7^0, TRUE, cost: 1
  35: l9 -> l13 : TRUE, cost: 1
  36: l10 -> l9 : Index7^0'=1, Sorted5^0'=1, i8^0-__const_99^0 <= 0, cost: 1
  29: l11 -> l8 : Temp6^0'=Temp6^post11, Sorted5^0'=0, 0 == 0, cost: 1
  30: l11 -> l8 : TRUE, cost: 1
  31: l12 -> l11 : -__const_100^0+Index7^0+i8^0 <= 0, cost: 1
  32: l12 -> l6 : 1+__const_100^0-Index7^0-i8^0 <= 0, cost: 1
  33: l13 -> l6 : 1-Index7^0+__const_99^0 <= 0, cost: 1
  34: l13 -> l12 : Index7^0-__const_99^0 <= 0, cost: 1
  37: l14 -> l2 : fact3^0'=-1, Index2^0'=1, factor^0'=-1, TRUE, cost: 1
  38: l15 -> l14 : TRUE, cost: 1


Eliminating location l14 by chaining:

Applied chaining
First rule:
l15 -> l14 : TRUE, cost: 1
Second rule:
l14 -> l2 : fact3^0'=-1, Index2^0'=1, factor^0'=-1, TRUE, cost: 1
New rule:
l15 -> l2 : fact3^0'=-1, Index2^0'=1, factor^0'=-1, TRUE, cost: 2

Applied deletion
Removed the following rules: 37 38

Eliminating location l10 by chaining:

Applied chaining
First rule:
l1 -> l10 : TRUE, cost: 1
Second rule:
l10 -> l9 : Index7^0'=1, Sorted5^0'=1, i8^0-__const_99^0 <= 0, cost: 1
New rule:
l1 -> l9 : Index7^0'=1, Sorted5^0'=1, i8^0-__const_99^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 28 36

Eliminating location l7 by chaining:

Applied chaining
First rule:
l6 -> l7 : TRUE, cost: 1
Second rule:
l7 -> l1 : i8^0'=1+i8^0, Sorted5^0 == 0, cost: 1
New rule:
l6 -> l1 : i8^0'=1+i8^0, Sorted5^0 == 0, cost: 2

Applied deletion
Removed the following rules: 25 26

Eliminated locations on linear paths
Start location: l15
  22: l0 -> l1 : i8^0'=1, Sorted5^0'=0, 1+__const_100^0-Index2^0 <= 0, cost: 1
  23: l0 -> l2 : Index2^0'=1+Index2^0, -__const_100^0+Index2^0 <= 0, cost: 1
  40: l1 -> l9 : Index7^0'=1, Sorted5^0'=1, i8^0-__const_99^0 <= 0, cost: 2
  24: l2 -> l0 : TRUE, cost: 1
  41: l6 -> l1 : i8^0'=1+i8^0, Sorted5^0 == 0, cost: 2
  27: l8 -> l9 : Index7^0'=1+Index7^0, TRUE, cost: 1
  35: l9 -> l13 : TRUE, cost: 1
  29: l11 -> l8 : Temp6^0'=Temp6^post11, Sorted5^0'=0, 0 == 0, cost: 1
  30: l11 -> l8 : TRUE, cost: 1
  31: l12 -> l11 : -__const_100^0+Index7^0+i8^0 <= 0, cost: 1
  32: l12 -> l6 : 1+__const_100^0-Index7^0-i8^0 <= 0, cost: 1
  33: l13 -> l6 : 1-Index7^0+__const_99^0 <= 0, cost: 1
  34: l13 -> l12 : Index7^0-__const_99^0 <= 0, cost: 1
  39: l15 -> l2 : fact3^0'=-1, Index2^0'=1, factor^0'=-1, TRUE, cost: 2


Eliminating location l0 by chaining:

Applied chaining
First rule:
l2 -> l0 : TRUE, cost: 1
Second rule:
l0 -> l1 : i8^0'=1, Sorted5^0'=0, 1+__const_100^0-Index2^0 <= 0, cost: 1
New rule:
l2 -> l1 : i8^0'=1, Sorted5^0'=0, 1+__const_100^0-Index2^0 <= 0, cost: 2

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

Applied deletion
Removed the following rules: 22 23 24

Eliminating location l13 by chaining:

Applied chaining
First rule:
l9 -> l13 : TRUE, cost: 1
Second rule:
l13 -> l6 : 1-Index7^0+__const_99^0 <= 0, cost: 1
New rule:
l9 -> l6 : 1-Index7^0+__const_99^0 <= 0, cost: 2

Applied chaining
First rule:
l9 -> l13 : TRUE, cost: 1
Second rule:
l13 -> l12 : Index7^0-__const_99^0 <= 0, cost: 1
New rule:
l9 -> l12 : Index7^0-__const_99^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 33 34 35

Eliminating location l11 by chaining:

Applied chaining
First rule:
l12 -> l11 : -__const_100^0+Index7^0+i8^0 <= 0, cost: 1
Second rule:
l11 -> l8 : Temp6^0'=Temp6^post11, Sorted5^0'=0, 0 == 0, cost: 1
New rule:
l12 -> l8 : Temp6^0'=Temp6^post11, Sorted5^0'=0, (0 == 0 /\ -__const_100^0+Index7^0+i8^0 <= 0), cost: 2

Applied simplification
Original rule:
l12 -> l8 : Temp6^0'=Temp6^post11, Sorted5^0'=0, (0 == 0 /\ -__const_100^0+Index7^0+i8^0 <= 0), cost: 2
New rule:
l12 -> l8 : Temp6^0'=Temp6^post11, Sorted5^0'=0, -__const_100^0+Index7^0+i8^0 <= 0, cost: 2

Applied chaining
First rule:
l12 -> l11 : -__const_100^0+Index7^0+i8^0 <= 0, cost: 1
Second rule:
l11 -> l8 : TRUE, cost: 1
New rule:
l12 -> l8 : -__const_100^0+Index7^0+i8^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 29 30 31

Eliminated locations on tree-shaped paths
Start location: l15
  40: l1 -> l9 : Index7^0'=1, Sorted5^0'=1, i8^0-__const_99^0 <= 0, cost: 2
  42: l2 -> l1 : i8^0'=1, Sorted5^0'=0, 1+__const_100^0-Index2^0 <= 0, cost: 2
  43: l2 -> l2 : Index2^0'=1+Index2^0, -__const_100^0+Index2^0 <= 0, cost: 2
  41: l6 -> l1 : i8^0'=1+i8^0, Sorted5^0 == 0, cost: 2
  27: l8 -> l9 : Index7^0'=1+Index7^0, TRUE, cost: 1
  44: l9 -> l6 : 1-Index7^0+__const_99^0 <= 0, cost: 2
  45: l9 -> l12 : Index7^0-__const_99^0 <= 0, cost: 2
  32: l12 -> l6 : 1+__const_100^0-Index7^0-i8^0 <= 0, cost: 1
  46: l12 -> l8 : Temp6^0'=Temp6^post11, Sorted5^0'=0, -__const_100^0+Index7^0+i8^0 <= 0, cost: 2
  47: l12 -> l8 : -__const_100^0+Index7^0+i8^0 <= 0, cost: 2
  39: l15 -> l2 : fact3^0'=-1, Index2^0'=1, factor^0'=-1, TRUE, cost: 2


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

Applied instantiation
Original rule:
l2 -> l2 : Index2^0'=Index2^0+n, (1+__const_100^0-Index2^0-n >= 0 /\ n >= 0), cost: 2*n
New rule:
l2 -> l2 : Index2^0'=1+__const_100^0, (0 >= 0 /\ 1+__const_100^0-Index2^0 >= 0), cost: 2+2*__const_100^0-2*Index2^0

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

Applied deletion
Removed the following rules: 43

Accelerated simple loops
Start location: l15
  40: l1 -> l9 : Index7^0'=1, Sorted5^0'=1, i8^0-__const_99^0 <= 0, cost: 2
  42: l2 -> l1 : i8^0'=1, Sorted5^0'=0, 1+__const_100^0-Index2^0 <= 0, cost: 2
  49: l2 -> l2 : Index2^0'=1+__const_100^0, 1+__const_100^0-Index2^0 >= 0, cost: 2+2*__const_100^0-2*Index2^0
  41: l6 -> l1 : i8^0'=1+i8^0, Sorted5^0 == 0, cost: 2
  27: l8 -> l9 : Index7^0'=1+Index7^0, TRUE, cost: 1
  44: l9 -> l6 : 1-Index7^0+__const_99^0 <= 0, cost: 2
  45: l9 -> l12 : Index7^0-__const_99^0 <= 0, cost: 2
  32: l12 -> l6 : 1+__const_100^0-Index7^0-i8^0 <= 0, cost: 1
  46: l12 -> l8 : Temp6^0'=Temp6^post11, Sorted5^0'=0, -__const_100^0+Index7^0+i8^0 <= 0, cost: 2
  47: l12 -> l8 : -__const_100^0+Index7^0+i8^0 <= 0, cost: 2
  39: l15 -> l2 : fact3^0'=-1, Index2^0'=1, factor^0'=-1, TRUE, cost: 2


Applied chaining
First rule:
l15 -> l2 : fact3^0'=-1, Index2^0'=1, factor^0'=-1, TRUE, cost: 2
Second rule:
l2 -> l2 : Index2^0'=1+__const_100^0, 1+__const_100^0-Index2^0 >= 0, cost: 2+2*__const_100^0-2*Index2^0
New rule:
l15 -> l2 : fact3^0'=-1, Index2^0'=1+__const_100^0, factor^0'=-1, __const_100^0 >= 0, cost: 2+2*__const_100^0

Applied deletion
Removed the following rules: 49

Chained accelerated rules with incoming rules
Start location: l15
  40: l1 -> l9 : Index7^0'=1, Sorted5^0'=1, i8^0-__const_99^0 <= 0, cost: 2
  42: l2 -> l1 : i8^0'=1, Sorted5^0'=0, 1+__const_100^0-Index2^0 <= 0, cost: 2
  41: l6 -> l1 : i8^0'=1+i8^0, Sorted5^0 == 0, cost: 2
  27: l8 -> l9 : Index7^0'=1+Index7^0, TRUE, cost: 1
  44: l9 -> l6 : 1-Index7^0+__const_99^0 <= 0, cost: 2
  45: l9 -> l12 : Index7^0-__const_99^0 <= 0, cost: 2
  32: l12 -> l6 : 1+__const_100^0-Index7^0-i8^0 <= 0, cost: 1
  46: l12 -> l8 : Temp6^0'=Temp6^post11, Sorted5^0'=0, -__const_100^0+Index7^0+i8^0 <= 0, cost: 2
  47: l12 -> l8 : -__const_100^0+Index7^0+i8^0 <= 0, cost: 2
  39: l15 -> l2 : fact3^0'=-1, Index2^0'=1, factor^0'=-1, TRUE, cost: 2
  50: l15 -> l2 : fact3^0'=-1, Index2^0'=1+__const_100^0, factor^0'=-1, __const_100^0 >= 0, cost: 2+2*__const_100^0


Eliminating location l2 by chaining:

Applied chaining
First rule:
l15 -> l2 : fact3^0'=-1, Index2^0'=1, factor^0'=-1, TRUE, cost: 2
Second rule:
l2 -> l1 : i8^0'=1, Sorted5^0'=0, 1+__const_100^0-Index2^0 <= 0, cost: 2
New rule:
l15 -> l1 : fact3^0'=-1, Index2^0'=1, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 <= 0, cost: 4

Applied chaining
First rule:
l15 -> l2 : fact3^0'=-1, Index2^0'=1+__const_100^0, factor^0'=-1, __const_100^0 >= 0, cost: 2+2*__const_100^0
Second rule:
l2 -> l1 : i8^0'=1, Sorted5^0'=0, 1+__const_100^0-Index2^0 <= 0, cost: 2
New rule:
l15 -> l1 : fact3^0'=-1, Index2^0'=1+__const_100^0, i8^0'=1, Sorted5^0'=0, factor^0'=-1, (0 <= 0 /\ __const_100^0 >= 0), cost: 4+2*__const_100^0

Applied simplification
Original rule:
l15 -> l1 : fact3^0'=-1, Index2^0'=1+__const_100^0, i8^0'=1, Sorted5^0'=0, factor^0'=-1, (0 <= 0 /\ __const_100^0 >= 0), cost: 4+2*__const_100^0
New rule:
l15 -> l1 : fact3^0'=-1, Index2^0'=1+__const_100^0, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 >= 0, cost: 4+2*__const_100^0

Applied deletion
Removed the following rules: 39 42 50

Eliminating location l12 by chaining:

Applied chaining
First rule:
l9 -> l12 : Index7^0-__const_99^0 <= 0, cost: 2
Second rule:
l12 -> l6 : 1+__const_100^0-Index7^0-i8^0 <= 0, cost: 1
New rule:
l9 -> l6 : (1+__const_100^0-Index7^0-i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0), cost: 3

Applied chaining
First rule:
l9 -> l12 : Index7^0-__const_99^0 <= 0, cost: 2
Second rule:
l12 -> l8 : Temp6^0'=Temp6^post11, Sorted5^0'=0, -__const_100^0+Index7^0+i8^0 <= 0, cost: 2
New rule:
l9 -> l8 : Temp6^0'=Temp6^post11, Sorted5^0'=0, (-__const_100^0+Index7^0+i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0), cost: 4

Applied chaining
First rule:
l9 -> l12 : Index7^0-__const_99^0 <= 0, cost: 2
Second rule:
l12 -> l8 : -__const_100^0+Index7^0+i8^0 <= 0, cost: 2
New rule:
l9 -> l8 : (-__const_100^0+Index7^0+i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0), cost: 4

Applied deletion
Removed the following rules: 32 45 46 47

Eliminated locations on tree-shaped paths
Start location: l15
  40: l1 -> l9 : Index7^0'=1, Sorted5^0'=1, i8^0-__const_99^0 <= 0, cost: 2
  41: l6 -> l1 : i8^0'=1+i8^0, Sorted5^0 == 0, cost: 2
  27: l8 -> l9 : Index7^0'=1+Index7^0, TRUE, cost: 1
  44: l9 -> l6 : 1-Index7^0+__const_99^0 <= 0, cost: 2
  53: l9 -> l6 : (1+__const_100^0-Index7^0-i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0), cost: 3
  54: l9 -> l8 : Temp6^0'=Temp6^post11, Sorted5^0'=0, (-__const_100^0+Index7^0+i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0), cost: 4
  55: l9 -> l8 : (-__const_100^0+Index7^0+i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0), cost: 4
  51: l15 -> l1 : fact3^0'=-1, Index2^0'=1, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 <= 0, cost: 4
  52: l15 -> l1 : fact3^0'=-1, Index2^0'=1+__const_100^0, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 >= 0, cost: 4+2*__const_100^0


Eliminating location l6 by chaining:

Applied chaining
First rule:
l9 -> l6 : 1-Index7^0+__const_99^0 <= 0, cost: 2
Second rule:
l6 -> l1 : i8^0'=1+i8^0, Sorted5^0 == 0, cost: 2
New rule:
l9 -> l1 : i8^0'=1+i8^0, (1-Index7^0+__const_99^0 <= 0 /\ Sorted5^0 == 0), cost: 4

Applied chaining
First rule:
l9 -> l6 : (1+__const_100^0-Index7^0-i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0), cost: 3
Second rule:
l6 -> l1 : i8^0'=1+i8^0, Sorted5^0 == 0, cost: 2
New rule:
l9 -> l1 : i8^0'=1+i8^0, (1+__const_100^0-Index7^0-i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0 /\ Sorted5^0 == 0), cost: 5

Applied deletion
Removed the following rules: 41 44 53

Eliminating location l8 by chaining:

Applied chaining
First rule:
l9 -> l8 : Temp6^0'=Temp6^post11, Sorted5^0'=0, (-__const_100^0+Index7^0+i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0), cost: 4
Second rule:
l8 -> l9 : Index7^0'=1+Index7^0, TRUE, cost: 1
New rule:
l9 -> l9 : Index7^0'=1+Index7^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (-__const_100^0+Index7^0+i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0), cost: 5

Applied chaining
First rule:
l9 -> l8 : (-__const_100^0+Index7^0+i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0), cost: 4
Second rule:
l8 -> l9 : Index7^0'=1+Index7^0, TRUE, cost: 1
New rule:
l9 -> l9 : Index7^0'=1+Index7^0, (-__const_100^0+Index7^0+i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0), cost: 5

Applied deletion
Removed the following rules: 27 54 55

Eliminated locations on tree-shaped paths
Start location: l15
  40: l1 -> l9 : Index7^0'=1, Sorted5^0'=1, i8^0-__const_99^0 <= 0, cost: 2
  56: l9 -> l1 : i8^0'=1+i8^0, (1-Index7^0+__const_99^0 <= 0 /\ Sorted5^0 == 0), cost: 4
  57: l9 -> l1 : i8^0'=1+i8^0, (1+__const_100^0-Index7^0-i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0 /\ Sorted5^0 == 0), cost: 5
  58: l9 -> l9 : Index7^0'=1+Index7^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (-__const_100^0+Index7^0+i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0), cost: 5
  59: l9 -> l9 : Index7^0'=1+Index7^0, (-__const_100^0+Index7^0+i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0), cost: 5
  51: l15 -> l1 : fact3^0'=-1, Index2^0'=1, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 <= 0, cost: 4
  52: l15 -> l1 : fact3^0'=-1, Index2^0'=1+__const_100^0, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 >= 0, cost: 4+2*__const_100^0


Applied acceleration
Original rule:
l9 -> l9 : Index7^0'=1+Index7^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (-__const_100^0+Index7^0+i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0), cost: 5
New rule:
l9 -> l9 : Index7^0'=Index7^0+n0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (1-Index7^0-n0+__const_99^0 >= 0 /\ -1+n0 >= 0 /\ 1+__const_100^0-Index7^0-n0-i8^0 >= 0), cost: 5*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_pPKjEH.txt

Applied instantiation
Original rule:
l9 -> l9 : Index7^0'=Index7^0+n0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (1-Index7^0-n0+__const_99^0 >= 0 /\ -1+n0 >= 0 /\ 1+__const_100^0-Index7^0-n0-i8^0 >= 0), cost: 5*n0
New rule:
l9 -> l9 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (0 >= 0 /\ __const_100^0-Index7^0-i8^0 >= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 5+5*__const_100^0-5*Index7^0-5*i8^0

Applied instantiation
Original rule:
l9 -> l9 : Index7^0'=Index7^0+n0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (1-Index7^0-n0+__const_99^0 >= 0 /\ -1+n0 >= 0 /\ 1+__const_100^0-Index7^0-n0-i8^0 >= 0), cost: 5*n0
New rule:
l9 -> l9 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (0 >= 0 /\ -Index7^0+__const_99^0 >= 0 /\ __const_100^0-i8^0-__const_99^0 >= 0), cost: 5-5*Index7^0+5*__const_99^0

Applied acceleration
Original rule:
l9 -> l9 : Index7^0'=1+Index7^0, (-__const_100^0+Index7^0+i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0), cost: 5
New rule:
l9 -> l9 : Index7^0'=Index7^0+n1, (n1 >= 0 /\ 1+__const_100^0-Index7^0-i8^0-n1 >= 0 /\ 1-Index7^0+__const_99^0-n1 >= 0), cost: 5*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_LnhAEK.txt

Applied instantiation
Original rule:
l9 -> l9 : Index7^0'=Index7^0+n1, (n1 >= 0 /\ 1+__const_100^0-Index7^0-i8^0-n1 >= 0 /\ 1-Index7^0+__const_99^0-n1 >= 0), cost: 5*n1
New rule:
l9 -> l9 : Index7^0'=1+__const_100^0-i8^0, (0 >= 0 /\ 1+__const_100^0-Index7^0-i8^0 >= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 5+5*__const_100^0-5*Index7^0-5*i8^0

Applied instantiation
Original rule:
l9 -> l9 : Index7^0'=Index7^0+n1, (n1 >= 0 /\ 1+__const_100^0-Index7^0-i8^0-n1 >= 0 /\ 1-Index7^0+__const_99^0-n1 >= 0), cost: 5*n1
New rule:
l9 -> l9 : Index7^0'=1+__const_99^0, (0 >= 0 /\ 1-Index7^0+__const_99^0 >= 0 /\ __const_100^0-i8^0-__const_99^0 >= 0), cost: 5-5*Index7^0+5*__const_99^0

Applied simplification
Original rule:
l9 -> l9 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (0 >= 0 /\ __const_100^0-Index7^0-i8^0 >= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 5+5*__const_100^0-5*Index7^0-5*i8^0
New rule:
l9 -> l9 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (__const_100^0-Index7^0-i8^0 >= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 5+5*__const_100^0-5*Index7^0-5*i8^0

Applied simplification
Original rule:
l9 -> l9 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (0 >= 0 /\ -Index7^0+__const_99^0 >= 0 /\ __const_100^0-i8^0-__const_99^0 >= 0), cost: 5-5*Index7^0+5*__const_99^0
New rule:
l9 -> l9 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (-Index7^0+__const_99^0 >= 0 /\ __const_100^0-i8^0-__const_99^0 >= 0), cost: 5-5*Index7^0+5*__const_99^0

Applied simplification
Original rule:
l9 -> l9 : Index7^0'=1+__const_100^0-i8^0, (0 >= 0 /\ 1+__const_100^0-Index7^0-i8^0 >= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 5+5*__const_100^0-5*Index7^0-5*i8^0
New rule:
l9 -> l9 : Index7^0'=1+__const_100^0-i8^0, (1+__const_100^0-Index7^0-i8^0 >= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 5+5*__const_100^0-5*Index7^0-5*i8^0

Applied simplification
Original rule:
l9 -> l9 : Index7^0'=1+__const_99^0, (0 >= 0 /\ 1-Index7^0+__const_99^0 >= 0 /\ __const_100^0-i8^0-__const_99^0 >= 0), cost: 5-5*Index7^0+5*__const_99^0
New rule:
l9 -> l9 : Index7^0'=1+__const_99^0, (1-Index7^0+__const_99^0 >= 0 /\ __const_100^0-i8^0-__const_99^0 >= 0), cost: 5-5*Index7^0+5*__const_99^0

Applied deletion
Removed the following rules: 58 59

Accelerated simple loops
Start location: l15
  40: l1 -> l9 : Index7^0'=1, Sorted5^0'=1, i8^0-__const_99^0 <= 0, cost: 2
  56: l9 -> l1 : i8^0'=1+i8^0, (1-Index7^0+__const_99^0 <= 0 /\ Sorted5^0 == 0), cost: 4
  57: l9 -> l1 : i8^0'=1+i8^0, (1+__const_100^0-Index7^0-i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0 /\ Sorted5^0 == 0), cost: 5
  64: l9 -> l9 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (__const_100^0-Index7^0-i8^0 >= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 5+5*__const_100^0-5*Index7^0-5*i8^0
  65: l9 -> l9 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (-Index7^0+__const_99^0 >= 0 /\ __const_100^0-i8^0-__const_99^0 >= 0), cost: 5-5*Index7^0+5*__const_99^0
  66: l9 -> l9 : Index7^0'=1+__const_100^0-i8^0, (1+__const_100^0-Index7^0-i8^0 >= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 5+5*__const_100^0-5*Index7^0-5*i8^0
  67: l9 -> l9 : Index7^0'=1+__const_99^0, (1-Index7^0+__const_99^0 >= 0 /\ __const_100^0-i8^0-__const_99^0 >= 0), cost: 5-5*Index7^0+5*__const_99^0
  51: l15 -> l1 : fact3^0'=-1, Index2^0'=1, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 <= 0, cost: 4
  52: l15 -> l1 : fact3^0'=-1, Index2^0'=1+__const_100^0, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 >= 0, cost: 4+2*__const_100^0


Applied chaining
First rule:
l1 -> l9 : Index7^0'=1, Sorted5^0'=1, i8^0-__const_99^0 <= 0, cost: 2
Second rule:
l9 -> l9 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (__const_100^0-Index7^0-i8^0 >= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 5+5*__const_100^0-5*Index7^0-5*i8^0
New rule:
l1 -> l9 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (-1+__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 2+5*__const_100^0-5*i8^0

Applied chaining
First rule:
l1 -> l9 : Index7^0'=1, Sorted5^0'=1, i8^0-__const_99^0 <= 0, cost: 2
Second rule:
l9 -> l9 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (-Index7^0+__const_99^0 >= 0 /\ __const_100^0-i8^0-__const_99^0 >= 0), cost: 5-5*Index7^0+5*__const_99^0
New rule:
l1 -> l9 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (__const_100^0-i8^0-__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ i8^0-__const_99^0 <= 0), cost: 2+5*__const_99^0

Applied chaining
First rule:
l1 -> l9 : Index7^0'=1, Sorted5^0'=1, i8^0-__const_99^0 <= 0, cost: 2
Second rule:
l9 -> l9 : Index7^0'=1+__const_100^0-i8^0, (1+__const_100^0-Index7^0-i8^0 >= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 5+5*__const_100^0-5*Index7^0-5*i8^0
New rule:
l1 -> l9 : Index7^0'=1+__const_100^0-i8^0, Sorted5^0'=1, (__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 2+5*__const_100^0-5*i8^0

Applied chaining
First rule:
l1 -> l9 : Index7^0'=1, Sorted5^0'=1, i8^0-__const_99^0 <= 0, cost: 2
Second rule:
l9 -> l9 : Index7^0'=1+__const_99^0, (1-Index7^0+__const_99^0 >= 0 /\ __const_100^0-i8^0-__const_99^0 >= 0), cost: 5-5*Index7^0+5*__const_99^0
New rule:
l1 -> l9 : Index7^0'=1+__const_99^0, Sorted5^0'=1, (__const_99^0 >= 0 /\ __const_100^0-i8^0-__const_99^0 >= 0 /\ i8^0-__const_99^0 <= 0), cost: 2+5*__const_99^0

Applied deletion
Removed the following rules: 64 65 66 67

Chained accelerated rules with incoming rules
Start location: l15
  40: l1 -> l9 : Index7^0'=1, Sorted5^0'=1, i8^0-__const_99^0 <= 0, cost: 2
  68: l1 -> l9 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (-1+__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 2+5*__const_100^0-5*i8^0
  69: l1 -> l9 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (__const_100^0-i8^0-__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ i8^0-__const_99^0 <= 0), cost: 2+5*__const_99^0
  70: l1 -> l9 : Index7^0'=1+__const_100^0-i8^0, Sorted5^0'=1, (__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 2+5*__const_100^0-5*i8^0
  71: l1 -> l9 : Index7^0'=1+__const_99^0, Sorted5^0'=1, (__const_99^0 >= 0 /\ __const_100^0-i8^0-__const_99^0 >= 0 /\ i8^0-__const_99^0 <= 0), cost: 2+5*__const_99^0
  56: l9 -> l1 : i8^0'=1+i8^0, (1-Index7^0+__const_99^0 <= 0 /\ Sorted5^0 == 0), cost: 4
  57: l9 -> l1 : i8^0'=1+i8^0, (1+__const_100^0-Index7^0-i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0 /\ Sorted5^0 == 0), cost: 5
  51: l15 -> l1 : fact3^0'=-1, Index2^0'=1, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 <= 0, cost: 4
  52: l15 -> l1 : fact3^0'=-1, Index2^0'=1+__const_100^0, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 >= 0, cost: 4+2*__const_100^0


Eliminating location l9 by chaining:

Applied chaining
First rule:
l1 -> l9 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (-1+__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 2+5*__const_100^0-5*i8^0
Second rule:
l9 -> l1 : i8^0'=1+i8^0, (1-Index7^0+__const_99^0 <= 0 /\ Sorted5^0 == 0), cost: 4
New rule:
l1 -> l1 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (0 == 0 /\ -1+__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 6+5*__const_100^0-5*i8^0

Applied simplification
Original rule:
l1 -> l1 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (0 == 0 /\ -1+__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 6+5*__const_100^0-5*i8^0
New rule:
l1 -> l1 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (-1+__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 6+5*__const_100^0-5*i8^0

Applied chaining
First rule:
l1 -> l9 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (-1+__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 2+5*__const_100^0-5*i8^0
Second rule:
l9 -> l1 : i8^0'=1+i8^0, (1+__const_100^0-Index7^0-i8^0 <= 0 /\ Index7^0-__const_99^0 <= 0 /\ Sorted5^0 == 0), cost: 5
New rule:
l1 -> l1 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (0 <= 0 /\ 0 == 0 /\ -1+__const_100^0-i8^0 >= 0 /\ 1+__const_100^0-i8^0-__const_99^0 <= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 7+5*__const_100^0-5*i8^0

Applied simplification
Original rule:
l1 -> l1 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (0 <= 0 /\ 0 == 0 /\ -1+__const_100^0-i8^0 >= 0 /\ 1+__const_100^0-i8^0-__const_99^0 <= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 7+5*__const_100^0-5*i8^0
New rule:
l1 -> l1 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (-1+__const_100^0-i8^0 >= 0 /\ 1+__const_100^0-i8^0-__const_99^0 <= 0 /\ i8^0-__const_99^0 <= 0), cost: 7+5*__const_100^0-5*i8^0

Applied chaining
First rule:
l1 -> l9 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (__const_100^0-i8^0-__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ i8^0-__const_99^0 <= 0), cost: 2+5*__const_99^0
Second rule:
l9 -> l1 : i8^0'=1+i8^0, (1-Index7^0+__const_99^0 <= 0 /\ Sorted5^0 == 0), cost: 4
New rule:
l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (0 <= 0 /\ 0 == 0 /\ __const_100^0-i8^0-__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ i8^0-__const_99^0 <= 0), cost: 6+5*__const_99^0

Applied simplification
Original rule:
l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (0 <= 0 /\ 0 == 0 /\ __const_100^0-i8^0-__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ i8^0-__const_99^0 <= 0), cost: 6+5*__const_99^0
New rule:
l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (__const_100^0-i8^0-__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ i8^0-__const_99^0 <= 0), cost: 6+5*__const_99^0

Applied partial deletion
Original rule:
l1 -> l9 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, Sorted5^0'=0, (__const_100^0-i8^0-__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ i8^0-__const_99^0 <= 0), cost: 2+5*__const_99^0
New rule:
l1 -> [18] : (__const_100^0-i8^0-__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ i8^0-__const_99^0 <= 0), cost: 2+5*__const_99^0

Applied partial deletion
Original rule:
l1 -> l9 : Index7^0'=1+__const_100^0-i8^0, Sorted5^0'=1, (__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 2+5*__const_100^0-5*i8^0
New rule:
l1 -> [18] : (__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 2+5*__const_100^0-5*i8^0

Applied partial deletion
Original rule:
l1 -> l9 : Index7^0'=1+__const_99^0, Sorted5^0'=1, (__const_99^0 >= 0 /\ __const_100^0-i8^0-__const_99^0 >= 0 /\ i8^0-__const_99^0 <= 0), cost: 2+5*__const_99^0
New rule:
l1 -> [18] : (__const_99^0 >= 0 /\ __const_100^0-i8^0-__const_99^0 >= 0 /\ i8^0-__const_99^0 <= 0), cost: 2+5*__const_99^0

Applied deletion
Removed the following rules: 40 56 57 68 69 70 71

Eliminated locations on tree-shaped paths
Start location: l15
  72: l1 -> l1 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (-1+__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 6+5*__const_100^0-5*i8^0
  73: l1 -> l1 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (-1+__const_100^0-i8^0 >= 0 /\ 1+__const_100^0-i8^0-__const_99^0 <= 0 /\ i8^0-__const_99^0 <= 0), cost: 7+5*__const_100^0-5*i8^0
  74: l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (__const_100^0-i8^0-__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ i8^0-__const_99^0 <= 0), cost: 6+5*__const_99^0
  75: l1 -> [18] : (__const_100^0-i8^0-__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ i8^0-__const_99^0 <= 0), cost: 2+5*__const_99^0
  76: l1 -> [18] : (__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 2+5*__const_100^0-5*i8^0
  77: l1 -> [18] : (__const_99^0 >= 0 /\ __const_100^0-i8^0-__const_99^0 >= 0 /\ i8^0-__const_99^0 <= 0), cost: 2+5*__const_99^0
  51: l15 -> l1 : fact3^0'=-1, Index2^0'=1, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 <= 0, cost: 4
  52: l15 -> l1 : fact3^0'=-1, Index2^0'=1+__const_100^0, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 >= 0, cost: 4+2*__const_100^0


Applied pruning (of leafs and parallel rules):
Start location: l15
  72: l1 -> l1 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (-1+__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 6+5*__const_100^0-5*i8^0
  73: l1 -> l1 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (-1+__const_100^0-i8^0 >= 0 /\ 1+__const_100^0-i8^0-__const_99^0 <= 0 /\ i8^0-__const_99^0 <= 0), cost: 7+5*__const_100^0-5*i8^0
  74: l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (__const_100^0-i8^0-__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ i8^0-__const_99^0 <= 0), cost: 6+5*__const_99^0
  51: l15 -> l1 : fact3^0'=-1, Index2^0'=1, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 <= 0, cost: 4
  52: l15 -> l1 : fact3^0'=-1, Index2^0'=1+__const_100^0, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 >= 0, cost: 4+2*__const_100^0


Applied simplification
Original rule:
l1 -> l1 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (-1+__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 >= 0), cost: 6+5*__const_100^0-5*i8^0
New rule:
l1 -> l1 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (-1+__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 == 0), cost: 6+5*__const_100^0-5*i8^0

Simplified simple loops
Start location: l15
  73: l1 -> l1 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (-1+__const_100^0-i8^0 >= 0 /\ 1+__const_100^0-i8^0-__const_99^0 <= 0 /\ i8^0-__const_99^0 <= 0), cost: 7+5*__const_100^0-5*i8^0
  74: l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (__const_100^0-i8^0-__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ i8^0-__const_99^0 <= 0), cost: 6+5*__const_99^0
  78: l1 -> l1 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (-1+__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 == 0), cost: 6+5*__const_100^0-5*i8^0
  51: l15 -> l1 : fact3^0'=-1, Index2^0'=1, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 <= 0, cost: 4
  52: l15 -> l1 : fact3^0'=-1, Index2^0'=1+__const_100^0, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 >= 0, cost: 4+2*__const_100^0


Applied acceleration
Original rule:
l1 -> l1 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (-1+__const_100^0-i8^0 >= 0 /\ 1+__const_100^0-i8^0-__const_99^0 <= 0 /\ i8^0-__const_99^0 <= 0), cost: 7+5*__const_100^0-5*i8^0
New rule:
l1 -> l1 : Index7^0'=2+__const_100^0-n8-i8^0, Temp6^0'=Temp6^post11, i8^0'=n8+i8^0, Sorted5^0'=0, (__const_100^0-n8-i8^0 >= 0 /\ -1-__const_100^0+i8^0+__const_99^0 >= 0 /\ 1-n8-i8^0+__const_99^0 >= 0 /\ -1+n8 >= 0), cost: 19/2*n8+5*__const_100^0*n8-5*n8*i8^0-5/2*n8^2
Sub-proof via acceration calculus written to file:///tmp/tmpnam_DepHce.txt

Applied instantiation
Original rule:
l1 -> l1 : Index7^0'=2+__const_100^0-n8-i8^0, Temp6^0'=Temp6^post11, i8^0'=n8+i8^0, Sorted5^0'=0, (__const_100^0-n8-i8^0 >= 0 /\ -1-__const_100^0+i8^0+__const_99^0 >= 0 /\ 1-n8-i8^0+__const_99^0 >= 0 /\ -1+n8 >= 0), cost: 19/2*n8+5*__const_100^0*n8-5*n8*i8^0-5/2*n8^2
New rule:
l1 -> l1 : Index7^0'=2, Temp6^0'=Temp6^post11, i8^0'=__const_100^0, Sorted5^0'=0, (0 >= 0 /\ -1-__const_100^0+i8^0+__const_99^0 >= 0 /\ -1+__const_100^0-i8^0 >= 0 /\ 1-__const_100^0+__const_99^0 >= 0), cost: 19/2*__const_100^0+5*__const_100^0*(__const_100^0-i8^0)-5*i8^0*(__const_100^0-i8^0)-19/2*i8^0-5/2*(__const_100^0-i8^0)^2

Applied instantiation
Original rule:
l1 -> l1 : Index7^0'=2+__const_100^0-n8-i8^0, Temp6^0'=Temp6^post11, i8^0'=n8+i8^0, Sorted5^0'=0, (__const_100^0-n8-i8^0 >= 0 /\ -1-__const_100^0+i8^0+__const_99^0 >= 0 /\ 1-n8-i8^0+__const_99^0 >= 0 /\ -1+n8 >= 0), cost: 19/2*n8+5*__const_100^0*n8-5*n8*i8^0-5/2*n8^2
New rule:
l1 -> l1 : Index7^0'=1+__const_100^0-__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+__const_99^0, Sorted5^0'=0, (0 >= 0 /\ -1-__const_100^0+i8^0+__const_99^0 >= 0 /\ -1+__const_100^0-__const_99^0 >= 0 /\ -i8^0+__const_99^0 >= 0), cost: 19/2-5/2*(-1+i8^0-__const_99^0)^2+5*(-1+i8^0-__const_99^0)*i8^0-19/2*i8^0+19/2*__const_99^0-5*__const_100^0*(-1+i8^0-__const_99^0)

Applied acceleration
Original rule:
l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (__const_100^0-i8^0-__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ i8^0-__const_99^0 <= 0), cost: 6+5*__const_99^0
New rule:
l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=i8^0+n9, Sorted5^0'=0, (-1+n9 >= 0 /\ 1+__const_100^0-i8^0-__const_99^0-n9 >= 0 /\ -1+__const_99^0 >= 0 /\ 1-i8^0+__const_99^0-n9 >= 0), cost: 5*__const_99^0*n9+6*n9
Sub-proof via acceration calculus written to file:///tmp/tmpnam_nlbljJ.txt

Applied instantiation
Original rule:
l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=i8^0+n9, Sorted5^0'=0, (-1+n9 >= 0 /\ 1+__const_100^0-i8^0-__const_99^0-n9 >= 0 /\ -1+__const_99^0 >= 0 /\ 1-i8^0+__const_99^0-n9 >= 0), cost: 5*__const_99^0*n9+6*n9
New rule:
l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+__const_100^0-__const_99^0, Sorted5^0'=0, (0 >= 0 /\ __const_100^0-i8^0-__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ -__const_100^0+2*__const_99^0 >= 0), cost: 6+6*__const_100^0-6*i8^0-6*__const_99^0+5*__const_99^0*(1+__const_100^0-i8^0-__const_99^0)

Applied instantiation
Original rule:
l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=i8^0+n9, Sorted5^0'=0, (-1+n9 >= 0 /\ 1+__const_100^0-i8^0-__const_99^0-n9 >= 0 /\ -1+__const_99^0 >= 0 /\ 1-i8^0+__const_99^0-n9 >= 0), cost: 5*__const_99^0*n9+6*n9
New rule:
l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+__const_99^0, Sorted5^0'=0, (0 >= 0 /\ __const_100^0-2*__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ -i8^0+__const_99^0 >= 0), cost: 6-6*i8^0+6*__const_99^0-5*(-1+i8^0-__const_99^0)*__const_99^0

Applied simplification
Original rule:
l1 -> l1 : Index7^0'=2, Temp6^0'=Temp6^post11, i8^0'=__const_100^0, Sorted5^0'=0, (0 >= 0 /\ -1-__const_100^0+i8^0+__const_99^0 >= 0 /\ -1+__const_100^0-i8^0 >= 0 /\ 1-__const_100^0+__const_99^0 >= 0), cost: 19/2*__const_100^0+5*__const_100^0*(__const_100^0-i8^0)-5*i8^0*(__const_100^0-i8^0)-19/2*i8^0-5/2*(__const_100^0-i8^0)^2
New rule:
l1 -> l1 : Index7^0'=2, Temp6^0'=Temp6^post11, i8^0'=__const_100^0, Sorted5^0'=0, (-1-__const_100^0+i8^0+__const_99^0 >= 0 /\ -1+__const_100^0-i8^0 >= 0 /\ 1-__const_100^0+__const_99^0 >= 0), cost: 19/2*__const_100^0+5*__const_100^0*(__const_100^0-i8^0)-5*i8^0*(__const_100^0-i8^0)-19/2*i8^0-5/2*(__const_100^0-i8^0)^2

Applied simplification
Original rule:
l1 -> l1 : Index7^0'=1+__const_100^0-__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+__const_99^0, Sorted5^0'=0, (0 >= 0 /\ -1-__const_100^0+i8^0+__const_99^0 >= 0 /\ -1+__const_100^0-__const_99^0 >= 0 /\ -i8^0+__const_99^0 >= 0), cost: 19/2-5/2*(-1+i8^0-__const_99^0)^2+5*(-1+i8^0-__const_99^0)*i8^0-19/2*i8^0+19/2*__const_99^0-5*__const_100^0*(-1+i8^0-__const_99^0)
New rule:
l1 -> l1 : Index7^0'=1+__const_100^0-__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+__const_99^0, Sorted5^0'=0, (-1-__const_100^0+i8^0+__const_99^0 >= 0 /\ -1+__const_100^0-__const_99^0 >= 0 /\ -i8^0+__const_99^0 >= 0), cost: 19/2-5/2*(-1+i8^0-__const_99^0)^2+5*(-1+i8^0-__const_99^0)*i8^0-19/2*i8^0+19/2*__const_99^0-5*__const_100^0*(-1+i8^0-__const_99^0)

Applied simplification
Original rule:
l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+__const_100^0-__const_99^0, Sorted5^0'=0, (0 >= 0 /\ __const_100^0-i8^0-__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ -__const_100^0+2*__const_99^0 >= 0), cost: 6+6*__const_100^0-6*i8^0-6*__const_99^0+5*__const_99^0*(1+__const_100^0-i8^0-__const_99^0)
New rule:
l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+__const_100^0-__const_99^0, Sorted5^0'=0, (__const_100^0-i8^0-__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ -__const_100^0+2*__const_99^0 >= 0), cost: 6+6*__const_100^0-6*i8^0-6*__const_99^0+5*__const_99^0*(1+__const_100^0-i8^0-__const_99^0)

Applied simplification
Original rule:
l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+__const_99^0, Sorted5^0'=0, (0 >= 0 /\ __const_100^0-2*__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ -i8^0+__const_99^0 >= 0), cost: 6-6*i8^0+6*__const_99^0-5*(-1+i8^0-__const_99^0)*__const_99^0
New rule:
l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+__const_99^0, Sorted5^0'=0, (__const_100^0-2*__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ -i8^0+__const_99^0 >= 0), cost: 6-6*i8^0+6*__const_99^0-5*(-1+i8^0-__const_99^0)*__const_99^0

Applied deletion
Removed the following rules: 73 74

Accelerated simple loops
Start location: l15
  78: l1 -> l1 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (-1+__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 == 0), cost: 6+5*__const_100^0-5*i8^0
  83: l1 -> l1 : Index7^0'=2, Temp6^0'=Temp6^post11, i8^0'=__const_100^0, Sorted5^0'=0, (-1-__const_100^0+i8^0+__const_99^0 >= 0 /\ -1+__const_100^0-i8^0 >= 0 /\ 1-__const_100^0+__const_99^0 >= 0), cost: 19/2*__const_100^0+5*__const_100^0*(__const_100^0-i8^0)-5*i8^0*(__const_100^0-i8^0)-19/2*i8^0-5/2*(__const_100^0-i8^0)^2
  84: l1 -> l1 : Index7^0'=1+__const_100^0-__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+__const_99^0, Sorted5^0'=0, (-1-__const_100^0+i8^0+__const_99^0 >= 0 /\ -1+__const_100^0-__const_99^0 >= 0 /\ -i8^0+__const_99^0 >= 0), cost: 19/2-5/2*(-1+i8^0-__const_99^0)^2+5*(-1+i8^0-__const_99^0)*i8^0-19/2*i8^0+19/2*__const_99^0-5*__const_100^0*(-1+i8^0-__const_99^0)
  85: l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+__const_100^0-__const_99^0, Sorted5^0'=0, (__const_100^0-i8^0-__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ -__const_100^0+2*__const_99^0 >= 0), cost: 6+6*__const_100^0-6*i8^0-6*__const_99^0+5*__const_99^0*(1+__const_100^0-i8^0-__const_99^0)
  86: l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+__const_99^0, Sorted5^0'=0, (__const_100^0-2*__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ -i8^0+__const_99^0 >= 0), cost: 6-6*i8^0+6*__const_99^0-5*(-1+i8^0-__const_99^0)*__const_99^0
  51: l15 -> l1 : fact3^0'=-1, Index2^0'=1, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 <= 0, cost: 4
  52: l15 -> l1 : fact3^0'=-1, Index2^0'=1+__const_100^0, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 >= 0, cost: 4+2*__const_100^0


Applied chaining
First rule:
l15 -> l1 : fact3^0'=-1, Index2^0'=1+__const_100^0, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 >= 0, cost: 4+2*__const_100^0
Second rule:
l1 -> l1 : Index7^0'=1+__const_100^0-i8^0, Temp6^0'=Temp6^post11, i8^0'=1+i8^0, Sorted5^0'=0, (-1+__const_100^0-i8^0 >= 0 /\ i8^0-__const_99^0 <= 0 /\ -__const_100^0+i8^0+__const_99^0 == 0), cost: 6+5*__const_100^0-5*i8^0
New rule:
l15 -> l1 : Index7^0'=__const_100^0, fact3^0'=-1, Temp6^0'=Temp6^post11, Index2^0'=1+__const_100^0, i8^0'=2, Sorted5^0'=0, factor^0'=-1, (-1+__const_99^0 >= 0 /\ 1-__const_100^0+__const_99^0 == 0), cost: 5+7*__const_100^0

Applied chaining
First rule:
l15 -> l1 : fact3^0'=-1, Index2^0'=1+__const_100^0, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 >= 0, cost: 4+2*__const_100^0
Second rule:
l1 -> l1 : Index7^0'=2, Temp6^0'=Temp6^post11, i8^0'=__const_100^0, Sorted5^0'=0, (-1-__const_100^0+i8^0+__const_99^0 >= 0 /\ -1+__const_100^0-i8^0 >= 0 /\ 1-__const_100^0+__const_99^0 >= 0), cost: 19/2*__const_100^0+5*__const_100^0*(__const_100^0-i8^0)-5*i8^0*(__const_100^0-i8^0)-19/2*i8^0-5/2*(__const_100^0-i8^0)^2
New rule:
l15 -> l1 : Index7^0'=2, fact3^0'=-1, Temp6^0'=Temp6^post11, Index2^0'=1+__const_100^0, i8^0'=__const_100^0, Sorted5^0'=0, factor^0'=-1, (-2+__const_100^0 >= 0 /\ -__const_100^0+__const_99^0 >= 0), cost: -1/2-5/2*(-1+__const_100^0)^2+13/2*__const_100^0+5*__const_100^0*(-1+__const_100^0)

Applied chaining
First rule:
l15 -> l1 : fact3^0'=-1, Index2^0'=1+__const_100^0, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 >= 0, cost: 4+2*__const_100^0
Second rule:
l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+__const_100^0-__const_99^0, Sorted5^0'=0, (__const_100^0-i8^0-__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ -__const_100^0+2*__const_99^0 >= 0), cost: 6+6*__const_100^0-6*i8^0-6*__const_99^0+5*__const_99^0*(1+__const_100^0-i8^0-__const_99^0)
New rule:
l15 -> l1 : Index7^0'=1+__const_99^0, fact3^0'=-1, Temp6^0'=Temp6^post11, Index2^0'=1+__const_100^0, i8^0'=1+__const_100^0-__const_99^0, Sorted5^0'=0, factor^0'=-1, (-1+__const_100^0-__const_99^0 >= 0 /\ -__const_100^0+2*__const_99^0 >= 0), cost: 4+8*__const_100^0+5*__const_99^0*(__const_100^0-__const_99^0)-6*__const_99^0

Applied chaining
First rule:
l15 -> l1 : fact3^0'=-1, Index2^0'=1+__const_100^0, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 >= 0, cost: 4+2*__const_100^0
Second rule:
l1 -> l1 : Index7^0'=1+__const_99^0, Temp6^0'=Temp6^post11, i8^0'=1+__const_99^0, Sorted5^0'=0, (__const_100^0-2*__const_99^0 >= 0 /\ -1+__const_99^0 >= 0 /\ -i8^0+__const_99^0 >= 0), cost: 6-6*i8^0+6*__const_99^0-5*(-1+i8^0-__const_99^0)*__const_99^0
New rule:
l15 -> l1 : Index7^0'=1+__const_99^0, fact3^0'=-1, Temp6^0'=Temp6^post11, Index2^0'=1+__const_100^0, i8^0'=1+__const_99^0, Sorted5^0'=0, factor^0'=-1, (__const_100^0-2*__const_99^0 >= 0 /\ -1+__const_99^0 >= 0), cost: 4+2*__const_100^0+5*__const_99^0^2+6*__const_99^0

Applied deletion
Removed the following rules: 78 83 84 85 86

Chained accelerated rules with incoming rules
Start location: l15
  51: l15 -> l1 : fact3^0'=-1, Index2^0'=1, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 <= 0, cost: 4
  52: l15 -> l1 : fact3^0'=-1, Index2^0'=1+__const_100^0, i8^0'=1, Sorted5^0'=0, factor^0'=-1, __const_100^0 >= 0, cost: 4+2*__const_100^0
  87: l15 -> l1 : Index7^0'=__const_100^0, fact3^0'=-1, Temp6^0'=Temp6^post11, Index2^0'=1+__const_100^0, i8^0'=2, Sorted5^0'=0, factor^0'=-1, (-1+__const_99^0 >= 0 /\ 1-__const_100^0+__const_99^0 == 0), cost: 5+7*__const_100^0
  88: l15 -> l1 : Index7^0'=2, fact3^0'=-1, Temp6^0'=Temp6^post11, Index2^0'=1+__const_100^0, i8^0'=__const_100^0, Sorted5^0'=0, factor^0'=-1, (-2+__const_100^0 >= 0 /\ -__const_100^0+__const_99^0 >= 0), cost: -1/2-5/2*(-1+__const_100^0)^2+13/2*__const_100^0+5*__const_100^0*(-1+__const_100^0)
  89: l15 -> l1 : Index7^0'=1+__const_99^0, fact3^0'=-1, Temp6^0'=Temp6^post11, Index2^0'=1+__const_100^0, i8^0'=1+__const_100^0-__const_99^0, Sorted5^0'=0, factor^0'=-1, (-1+__const_100^0-__const_99^0 >= 0 /\ -__const_100^0+2*__const_99^0 >= 0), cost: 4+8*__const_100^0+5*__const_99^0*(__const_100^0-__const_99^0)-6*__const_99^0
  90: l15 -> l1 : Index7^0'=1+__const_99^0, fact3^0'=-1, Temp6^0'=Temp6^post11, Index2^0'=1+__const_100^0, i8^0'=1+__const_99^0, Sorted5^0'=0, factor^0'=-1, (__const_100^0-2*__const_99^0 >= 0 /\ -1+__const_99^0 >= 0), cost: 4+2*__const_100^0+5*__const_99^0^2+6*__const_99^0


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


Computing asymptotic complexity

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

Solved cost: 0
Rule cost:   0