WORST_CASE(Omega(0),?)

Initial ITS
Start location: l16
   0: l0 -> l1 : Outer13^0'=Outer13^post0, Inner14^0'=Inner14^post0, ret_RandomInteger17^0'=ret_RandomInteger17^post0, OuterIndex8^0'=OuterIndex8^post0, InnerIndex9^0'=InnerIndex9^post0, Index15^0'=Index15^post0, ret_RandomInteger16^0'=ret_RandomInteger16^post0, OuterIndex5^0'=OuterIndex5^post0, InnerIndex6^0'=InnerIndex6^post0, Seed^0'=Seed^post0, (-OuterIndex8^post0+OuterIndex8^0 == 0 /\ Inner14^0-Inner14^post0 == 0 /\ Index15^0-Index15^post0 == 0 /\ ret_RandomInteger16^0-ret_RandomInteger16^post0 == 0 /\ -OuterIndex5^post0+OuterIndex5^0 == 0 /\ -Seed^post0+Seed^0 == 0 /\ Outer13^0-Outer13^post0 == 0 /\ -InnerIndex6^post0+InnerIndex6^0 == 0 /\ -InnerIndex9^post0+InnerIndex9^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post0 == 0), cost: 1
  19: l1 -> l4 : Outer13^0'=Outer13^post19, Inner14^0'=Inner14^post19, ret_RandomInteger17^0'=ret_RandomInteger17^post19, OuterIndex8^0'=OuterIndex8^post19, InnerIndex9^0'=InnerIndex9^post19, Index15^0'=Index15^post19, ret_RandomInteger16^0'=ret_RandomInteger16^post19, OuterIndex5^0'=OuterIndex5^post19, InnerIndex6^0'=InnerIndex6^post19, Seed^0'=Seed^post19, (InnerIndex6^0-InnerIndex6^post19 == 0 /\ -ret_RandomInteger16^post19+ret_RandomInteger16^0 == 0 /\ -Seed^post19+Seed^0 == 0 /\ -Index15^post19+Index15^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post19 == 0 /\ InnerIndex9^0-InnerIndex9^post19 == 0 /\ OuterIndex8^post19 == 0 /\ -Inner14^post19+Inner14^0 == 0 /\ 20-OuterIndex5^0 <= 0 /\ -OuterIndex5^post19+OuterIndex5^0 == 0 /\ Outer13^0-Outer13^post19 == 0), cost: 1
  20: l1 -> l2 : Outer13^0'=Outer13^post20, Inner14^0'=Inner14^post20, ret_RandomInteger17^0'=ret_RandomInteger17^post20, OuterIndex8^0'=OuterIndex8^post20, InnerIndex9^0'=InnerIndex9^post20, Index15^0'=Index15^post20, ret_RandomInteger16^0'=ret_RandomInteger16^post20, OuterIndex5^0'=OuterIndex5^post20, InnerIndex6^0'=InnerIndex6^post20, Seed^0'=Seed^post20, (InnerIndex6^post20 == 0 /\ Outer13^0-Outer13^post20 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post20 == 0 /\ -OuterIndex5^post20+OuterIndex5^0 == 0 /\ -19+OuterIndex5^0 <= 0 /\ -ret_RandomInteger16^post20+ret_RandomInteger16^0 == 0 /\ Inner14^0-Inner14^post20 == 0 /\ -Seed^post20+Seed^0 == 0 /\ -Index15^post20+Index15^0 == 0 /\ InnerIndex9^0-InnerIndex9^post20 == 0 /\ OuterIndex8^0-OuterIndex8^post20 == 0), cost: 1
   1: l2 -> l3 : Outer13^0'=Outer13^post1, Inner14^0'=Inner14^post1, ret_RandomInteger17^0'=ret_RandomInteger17^post1, OuterIndex8^0'=OuterIndex8^post1, InnerIndex9^0'=InnerIndex9^post1, Index15^0'=Index15^post1, ret_RandomInteger16^0'=ret_RandomInteger16^post1, OuterIndex5^0'=OuterIndex5^post1, InnerIndex6^0'=InnerIndex6^post1, Seed^0'=Seed^post1, (ret_RandomInteger16^0-ret_RandomInteger16^post1 == 0 /\ -InnerIndex9^post1+InnerIndex9^0 == 0 /\ -Seed^post1+Seed^0 == 0 /\ Inner14^0-Inner14^post1 == 0 /\ -OuterIndex8^post1+OuterIndex8^0 == 0 /\ Index15^0-Index15^post1 == 0 /\ -ret_RandomInteger17^post1+ret_RandomInteger17^0 == 0 /\ -OuterIndex5^post1+OuterIndex5^0 == 0 /\ Outer13^0-Outer13^post1 == 0 /\ -InnerIndex6^post1+InnerIndex6^0 == 0), cost: 1
  17: l3 -> l0 : Outer13^0'=Outer13^post17, Inner14^0'=Inner14^post17, ret_RandomInteger17^0'=ret_RandomInteger17^post17, OuterIndex8^0'=OuterIndex8^post17, InnerIndex9^0'=InnerIndex9^post17, Index15^0'=Index15^post17, ret_RandomInteger16^0'=ret_RandomInteger16^post17, OuterIndex5^0'=OuterIndex5^post17, InnerIndex6^0'=InnerIndex6^post17, Seed^0'=Seed^post17, (InnerIndex9^0-InnerIndex9^post17 == 0 /\ -Index15^post17+Index15^0 == 0 /\ 20-InnerIndex6^0 <= 0 /\ -1-OuterIndex5^0+OuterIndex5^post17 == 0 /\ -InnerIndex6^post17+InnerIndex6^0 == 0 /\ OuterIndex8^0-OuterIndex8^post17 == 0 /\ Outer13^0-Outer13^post17 == 0 /\ -Inner14^post17+Inner14^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post17 == 0 /\ -ret_RandomInteger16^post17+ret_RandomInteger16^0 == 0 /\ -Seed^post17+Seed^0 == 0), cost: 1
  18: l3 -> l2 : Outer13^0'=Outer13^post18, Inner14^0'=Inner14^post18, ret_RandomInteger17^0'=ret_RandomInteger17^post18, OuterIndex8^0'=OuterIndex8^post18, InnerIndex9^0'=InnerIndex9^post18, Index15^0'=Index15^post18, ret_RandomInteger16^0'=ret_RandomInteger16^post18, OuterIndex5^0'=OuterIndex5^post18, InnerIndex6^0'=InnerIndex6^post18, Seed^0'=Seed^post18, (0 == 0 /\ -Index15^post18+Index15^0 == 0 /\ InnerIndex9^0-InnerIndex9^post18 == 0 /\ -1+InnerIndex6^post18-InnerIndex6^0 == 0 /\ OuterIndex8^0-OuterIndex8^post18 == 0 /\ -19+InnerIndex6^0 <= 0 /\ ret_RandomInteger16^post18-Seed^post18 == 0 /\ Outer13^0-Outer13^post18 == 0 /\ Inner14^0-Inner14^post18 == 0 /\ OuterIndex5^0-OuterIndex5^post18 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post18 == 0), cost: 1
   2: l4 -> l5 : Outer13^0'=Outer13^post2, Inner14^0'=Inner14^post2, ret_RandomInteger17^0'=ret_RandomInteger17^post2, OuterIndex8^0'=OuterIndex8^post2, InnerIndex9^0'=InnerIndex9^post2, Index15^0'=Index15^post2, ret_RandomInteger16^0'=ret_RandomInteger16^post2, OuterIndex5^0'=OuterIndex5^post2, InnerIndex6^0'=InnerIndex6^post2, Seed^0'=Seed^post2, (ret_RandomInteger16^0-ret_RandomInteger16^post2 == 0 /\ -InnerIndex9^post2+InnerIndex9^0 == 0 /\ -Seed^post2+Seed^0 == 0 /\ -OuterIndex8^post2+OuterIndex8^0 == 0 /\ Index15^0-Index15^post2 == 0 /\ Inner14^0-Inner14^post2 == 0 /\ -ret_RandomInteger17^post2+ret_RandomInteger17^0 == 0 /\ -OuterIndex5^post2+OuterIndex5^0 == 0 /\ Outer13^0-Outer13^post2 == 0 /\ -InnerIndex6^post2+InnerIndex6^0 == 0), cost: 1
  13: l5 -> l10 : Outer13^0'=Outer13^post13, Inner14^0'=Inner14^post13, ret_RandomInteger17^0'=ret_RandomInteger17^post13, OuterIndex8^0'=OuterIndex8^post13, InnerIndex9^0'=InnerIndex9^post13, Index15^0'=Index15^post13, ret_RandomInteger16^0'=ret_RandomInteger16^post13, OuterIndex5^0'=OuterIndex5^post13, InnerIndex6^0'=InnerIndex6^post13, Seed^0'=Seed^post13, (ret_RandomInteger16^0-ret_RandomInteger16^post13 == 0 /\ -InnerIndex9^post13+InnerIndex9^0 == 0 /\ -OuterIndex8^post13+OuterIndex8^0 == 0 /\ 20-OuterIndex8^0 <= 0 /\ Inner14^0-Inner14^post13 == 0 /\ -InnerIndex6^post13+InnerIndex6^0 == 0 /\ Index15^0-Index15^post13 == 0 /\ -ret_RandomInteger17^post13+ret_RandomInteger17^0 == 0 /\ Outer13^post13 == 0 /\ -OuterIndex5^post13+OuterIndex5^0 == 0 /\ -Seed^post13+Seed^0 == 0), cost: 1
  14: l5 -> l13 : Outer13^0'=Outer13^post14, Inner14^0'=Inner14^post14, ret_RandomInteger17^0'=ret_RandomInteger17^post14, OuterIndex8^0'=OuterIndex8^post14, InnerIndex9^0'=InnerIndex9^post14, Index15^0'=Index15^post14, ret_RandomInteger16^0'=ret_RandomInteger16^post14, OuterIndex5^0'=OuterIndex5^post14, InnerIndex6^0'=InnerIndex6^post14, Seed^0'=Seed^post14, (Index15^0-Index15^post14 == 0 /\ -19+OuterIndex8^0 <= 0 /\ Outer13^0-Outer13^post14 == 0 /\ Inner14^0-Inner14^post14 == 0 /\ InnerIndex9^post14 == 0 /\ -Seed^post14+Seed^0 == 0 /\ -OuterIndex5^post14+OuterIndex5^0 == 0 /\ -InnerIndex6^post14+InnerIndex6^0 == 0 /\ -ret_RandomInteger17^post14+ret_RandomInteger17^0 == 0 /\ OuterIndex8^0-OuterIndex8^post14 == 0 /\ -ret_RandomInteger16^post14+ret_RandomInteger16^0 == 0), cost: 1
   3: l6 -> l7 : Outer13^0'=Outer13^post3, Inner14^0'=Inner14^post3, ret_RandomInteger17^0'=ret_RandomInteger17^post3, OuterIndex8^0'=OuterIndex8^post3, InnerIndex9^0'=InnerIndex9^post3, Index15^0'=Index15^post3, ret_RandomInteger16^0'=ret_RandomInteger16^post3, OuterIndex5^0'=OuterIndex5^post3, InnerIndex6^0'=InnerIndex6^post3, Seed^0'=Seed^post3, (Outer13^0-Outer13^post3 == 0 /\ -ret_RandomInteger16^post3+ret_RandomInteger16^0 == 0 /\ -Index15^post3+Index15^0 == 0 /\ OuterIndex5^0-OuterIndex5^post3 == 0 /\ -InnerIndex6^post3+InnerIndex6^0 == 0 /\ 20-Index15^0 <= 0 /\ -ret_RandomInteger17^post3+ret_RandomInteger17^0 == 0 /\ InnerIndex9^0-InnerIndex9^post3 == 0 /\ OuterIndex8^0-OuterIndex8^post3 == 0 /\ -1-Inner14^0+Inner14^post3 == 0 /\ -Seed^post3+Seed^0 == 0), cost: 1
   4: l6 -> l8 : Outer13^0'=Outer13^post4, Inner14^0'=Inner14^post4, ret_RandomInteger17^0'=ret_RandomInteger17^post4, OuterIndex8^0'=OuterIndex8^post4, InnerIndex9^0'=InnerIndex9^post4, Index15^0'=Index15^post4, ret_RandomInteger16^0'=ret_RandomInteger16^post4, OuterIndex5^0'=OuterIndex5^post4, InnerIndex6^0'=InnerIndex6^post4, Seed^0'=Seed^post4, (-ret_RandomInteger16^post4+ret_RandomInteger16^0 == 0 /\ InnerIndex9^0-InnerIndex9^post4 == 0 /\ OuterIndex8^0-OuterIndex8^post4 == 0 /\ -InnerIndex6^post4+InnerIndex6^0 == 0 /\ OuterIndex5^0-OuterIndex5^post4 == 0 /\ -Seed^post4+Seed^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post4 == 0 /\ -Outer13^post4+Outer13^0 == 0 /\ Inner14^0-Inner14^post4 == 0 /\ -19+Index15^0 <= 0 /\ -1+Index15^post4-Index15^0 == 0), cost: 1
  15: l7 -> l9 : Outer13^0'=Outer13^post15, Inner14^0'=Inner14^post15, ret_RandomInteger17^0'=ret_RandomInteger17^post15, OuterIndex8^0'=OuterIndex8^post15, InnerIndex9^0'=InnerIndex9^post15, Index15^0'=Index15^post15, ret_RandomInteger16^0'=ret_RandomInteger16^post15, OuterIndex5^0'=OuterIndex5^post15, InnerIndex6^0'=InnerIndex6^post15, Seed^0'=Seed^post15, (-OuterIndex5^post15+OuterIndex5^0 == 0 /\ Outer13^0-Outer13^post15 == 0 /\ -InnerIndex9^post15+InnerIndex9^0 == 0 /\ Inner14^0-Inner14^post15 == 0 /\ Index15^0-Index15^post15 == 0 /\ -Seed^post15+Seed^0 == 0 /\ -InnerIndex6^post15+InnerIndex6^0 == 0 /\ OuterIndex8^0-OuterIndex8^post15 == 0 /\ -ret_RandomInteger16^post15+ret_RandomInteger16^0 == 0 /\ -ret_RandomInteger17^post15+ret_RandomInteger17^0 == 0), cost: 1
  16: l8 -> l6 : Outer13^0'=Outer13^post16, Inner14^0'=Inner14^post16, ret_RandomInteger17^0'=ret_RandomInteger17^post16, OuterIndex8^0'=OuterIndex8^post16, InnerIndex9^0'=InnerIndex9^post16, Index15^0'=Index15^post16, ret_RandomInteger16^0'=ret_RandomInteger16^post16, OuterIndex5^0'=OuterIndex5^post16, InnerIndex6^0'=InnerIndex6^post16, Seed^0'=Seed^post16, (-ret_RandomInteger17^post16+ret_RandomInteger17^0 == 0 /\ -InnerIndex6^post16+InnerIndex6^0 == 0 /\ Outer13^0-Outer13^post16 == 0 /\ -ret_RandomInteger16^post16+ret_RandomInteger16^0 == 0 /\ InnerIndex9^0-InnerIndex9^post16 == 0 /\ OuterIndex8^0-OuterIndex8^post16 == 0 /\ -Seed^post16+Seed^0 == 0 /\ -Index15^post16+Index15^0 == 0 /\ OuterIndex5^0-OuterIndex5^post16 == 0 /\ Inner14^0-Inner14^post16 == 0), cost: 1
   5: l9 -> l10 : Outer13^0'=Outer13^post5, Inner14^0'=Inner14^post5, ret_RandomInteger17^0'=ret_RandomInteger17^post5, OuterIndex8^0'=OuterIndex8^post5, InnerIndex9^0'=InnerIndex9^post5, Index15^0'=Index15^post5, ret_RandomInteger16^0'=ret_RandomInteger16^post5, OuterIndex5^0'=OuterIndex5^post5, InnerIndex6^0'=InnerIndex6^post5, Seed^0'=Seed^post5, (-ret_RandomInteger16^post5+ret_RandomInteger16^0 == 0 /\ OuterIndex8^0-OuterIndex8^post5 == 0 /\ InnerIndex9^0-InnerIndex9^post5 == 0 /\ -Index15^post5+Index15^0 == 0 /\ -InnerIndex6^post5+InnerIndex6^0 == 0 /\ OuterIndex5^0-OuterIndex5^post5 == 0 /\ -1-Outer13^0+Outer13^post5 == 0 /\ -Seed^post5+Seed^0 == 0 /\ Inner14^0-Inner14^post5 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post5 == 0 /\ 20-Inner14^0 <= 0), cost: 1
   6: l9 -> l8 : Outer13^0'=Outer13^post6, Inner14^0'=Inner14^post6, ret_RandomInteger17^0'=ret_RandomInteger17^post6, OuterIndex8^0'=OuterIndex8^post6, InnerIndex9^0'=InnerIndex9^post6, Index15^0'=Index15^post6, ret_RandomInteger16^0'=ret_RandomInteger16^post6, OuterIndex5^0'=OuterIndex5^post6, InnerIndex6^0'=InnerIndex6^post6, Seed^0'=Seed^post6, (InnerIndex9^0-InnerIndex9^post6 == 0 /\ -InnerIndex6^post6+InnerIndex6^0 == 0 /\ Index15^post6 == 0 /\ OuterIndex8^0-OuterIndex8^post6 == 0 /\ Outer13^0-Outer13^post6 == 0 /\ -Inner14^post6+Inner14^0 == 0 /\ -OuterIndex5^post6+OuterIndex5^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post6 == 0 /\ -19+Inner14^0 <= 0 /\ -ret_RandomInteger16^post6+ret_RandomInteger16^0 == 0 /\ -Seed^post6+Seed^0 == 0), cost: 1
  10: l10 -> l11 : Outer13^0'=Outer13^post10, Inner14^0'=Inner14^post10, ret_RandomInteger17^0'=ret_RandomInteger17^post10, OuterIndex8^0'=OuterIndex8^post10, InnerIndex9^0'=InnerIndex9^post10, Index15^0'=Index15^post10, ret_RandomInteger16^0'=ret_RandomInteger16^post10, OuterIndex5^0'=OuterIndex5^post10, InnerIndex6^0'=InnerIndex6^post10, Seed^0'=Seed^post10, (-OuterIndex8^post10+OuterIndex8^0 == 0 /\ Outer13^0-Outer13^post10 == 0 /\ -Seed^post10+Seed^0 == 0 /\ Inner14^0-Inner14^post10 == 0 /\ Index15^0-Index15^post10 == 0 /\ -OuterIndex5^post10+OuterIndex5^0 == 0 /\ ret_RandomInteger16^0-ret_RandomInteger16^post10 == 0 /\ InnerIndex9^0-InnerIndex9^post10 == 0 /\ -InnerIndex6^post10+InnerIndex6^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post10 == 0), cost: 1
   7: l11 -> l12 : Outer13^0'=Outer13^post7, Inner14^0'=Inner14^post7, ret_RandomInteger17^0'=ret_RandomInteger17^post7, OuterIndex8^0'=OuterIndex8^post7, InnerIndex9^0'=InnerIndex9^post7, Index15^0'=Index15^post7, ret_RandomInteger16^0'=ret_RandomInteger16^post7, OuterIndex5^0'=OuterIndex5^post7, InnerIndex6^0'=InnerIndex6^post7, Seed^0'=Seed^post7, (-OuterIndex5^post7+OuterIndex5^0 == 0 /\ -Index15^post7+Index15^0 == 0 /\ Outer13^0-Outer13^post7 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post7 == 0 /\ Inner14^0-Inner14^post7 == 0 /\ InnerIndex6^0-InnerIndex6^post7 == 0 /\ InnerIndex9^0-InnerIndex9^post7 == 0 /\ -Seed^post7+Seed^0 == 0 /\ 20-Outer13^0 <= 0 /\ OuterIndex8^0-OuterIndex8^post7 == 0 /\ -ret_RandomInteger16^post7+ret_RandomInteger16^0 == 0), cost: 1
   8: l11 -> l7 : Outer13^0'=Outer13^post8, Inner14^0'=Inner14^post8, ret_RandomInteger17^0'=ret_RandomInteger17^post8, OuterIndex8^0'=OuterIndex8^post8, InnerIndex9^0'=InnerIndex9^post8, Index15^0'=Index15^post8, ret_RandomInteger16^0'=ret_RandomInteger16^post8, OuterIndex5^0'=OuterIndex5^post8, InnerIndex6^0'=InnerIndex6^post8, Seed^0'=Seed^post8, (Inner14^post8 == 0 /\ Outer13^0-Outer13^post8 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post8 == 0 /\ -Seed^post8+Seed^0 == 0 /\ InnerIndex9^0-InnerIndex9^post8 == 0 /\ -InnerIndex6^post8+InnerIndex6^0 == 0 /\ -ret_RandomInteger16^post8+ret_RandomInteger16^0 == 0 /\ -OuterIndex5^post8+OuterIndex5^0 == 0 /\ OuterIndex8^0-OuterIndex8^post8 == 0 /\ -Index15^post8+Index15^0 == 0 /\ -19+Outer13^0 <= 0), cost: 1
   9: l13 -> l14 : Outer13^0'=Outer13^post9, Inner14^0'=Inner14^post9, ret_RandomInteger17^0'=ret_RandomInteger17^post9, OuterIndex8^0'=OuterIndex8^post9, InnerIndex9^0'=InnerIndex9^post9, Index15^0'=Index15^post9, ret_RandomInteger16^0'=ret_RandomInteger16^post9, OuterIndex5^0'=OuterIndex5^post9, InnerIndex6^0'=InnerIndex6^post9, Seed^0'=Seed^post9, (-ret_RandomInteger16^post9+ret_RandomInteger16^0 == 0 /\ -Inner14^post9+Inner14^0 == 0 /\ -Seed^post9+Seed^0 == 0 /\ -Index15^post9+Index15^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post9 == 0 /\ InnerIndex6^0-InnerIndex6^post9 == 0 /\ OuterIndex8^0-OuterIndex8^post9 == 0 /\ InnerIndex9^0-InnerIndex9^post9 == 0 /\ Outer13^0-Outer13^post9 == 0 /\ -OuterIndex5^post9+OuterIndex5^0 == 0), cost: 1
  11: l14 -> l4 : Outer13^0'=Outer13^post11, Inner14^0'=Inner14^post11, ret_RandomInteger17^0'=ret_RandomInteger17^post11, OuterIndex8^0'=OuterIndex8^post11, InnerIndex9^0'=InnerIndex9^post11, Index15^0'=Index15^post11, ret_RandomInteger16^0'=ret_RandomInteger16^post11, OuterIndex5^0'=OuterIndex5^post11, InnerIndex6^0'=InnerIndex6^post11, Seed^0'=Seed^post11, (-1+OuterIndex8^post11-OuterIndex8^0 == 0 /\ 20-InnerIndex9^0 <= 0 /\ -Seed^post11+Seed^0 == 0 /\ -OuterIndex5^post11+OuterIndex5^0 == 0 /\ Index15^0-Index15^post11 == 0 /\ ret_RandomInteger16^0-ret_RandomInteger16^post11 == 0 /\ Outer13^0-Outer13^post11 == 0 /\ -InnerIndex6^post11+InnerIndex6^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post11 == 0 /\ InnerIndex9^0-InnerIndex9^post11 == 0 /\ Inner14^0-Inner14^post11 == 0), cost: 1
  12: l14 -> l13 : Outer13^0'=Outer13^post12, Inner14^0'=Inner14^post12, ret_RandomInteger17^0'=ret_RandomInteger17^post12, OuterIndex8^0'=OuterIndex8^post12, InnerIndex9^0'=InnerIndex9^post12, Index15^0'=Index15^post12, ret_RandomInteger16^0'=ret_RandomInteger16^post12, OuterIndex5^0'=OuterIndex5^post12, InnerIndex6^0'=InnerIndex6^post12, Seed^0'=Seed^post12, (0 == 0 /\ ret_RandomInteger17^post12-Seed^post12 == 0 /\ -19+InnerIndex9^0 <= 0 /\ -OuterIndex8^post12+OuterIndex8^0 == 0 /\ ret_RandomInteger16^0-ret_RandomInteger16^post12 == 0 /\ -InnerIndex6^post12+InnerIndex6^0 == 0 /\ Outer13^0-Outer13^post12 == 0 /\ -1+InnerIndex9^post12-InnerIndex9^0 == 0 /\ Inner14^0-Inner14^post12 == 0 /\ Index15^0-Index15^post12 == 0 /\ -OuterIndex5^post12+OuterIndex5^0 == 0), cost: 1
  21: l15 -> l0 : Outer13^0'=Outer13^post21, Inner14^0'=Inner14^post21, ret_RandomInteger17^0'=ret_RandomInteger17^post21, OuterIndex8^0'=OuterIndex8^post21, InnerIndex9^0'=InnerIndex9^post21, Index15^0'=Index15^post21, ret_RandomInteger16^0'=ret_RandomInteger16^post21, OuterIndex5^0'=OuterIndex5^post21, InnerIndex6^0'=InnerIndex6^post21, Seed^0'=Seed^post21, (ret_RandomInteger17^0-ret_RandomInteger17^post21 == 0 /\ -OuterIndex8^post21+OuterIndex8^0 == 0 /\ OuterIndex5^post21 == 0 /\ Outer13^0-Outer13^post21 == 0 /\ Inner14^0-Inner14^post21 == 0 /\ Index15^0-Index15^post21 == 0 /\ ret_RandomInteger16^0-ret_RandomInteger16^post21 == 0 /\ InnerIndex9^0-InnerIndex9^post21 == 0 /\ Seed^post21 == 0 /\ -InnerIndex6^post21+InnerIndex6^0 == 0), cost: 1
  22: l16 -> l15 : Outer13^0'=Outer13^post22, Inner14^0'=Inner14^post22, ret_RandomInteger17^0'=ret_RandomInteger17^post22, OuterIndex8^0'=OuterIndex8^post22, InnerIndex9^0'=InnerIndex9^post22, Index15^0'=Index15^post22, ret_RandomInteger16^0'=ret_RandomInteger16^post22, OuterIndex5^0'=OuterIndex5^post22, InnerIndex6^0'=InnerIndex6^post22, Seed^0'=Seed^post22, (Index15^0-Index15^post22 == 0 /\ -InnerIndex9^post22+InnerIndex9^0 == 0 /\ ret_RandomInteger16^0-ret_RandomInteger16^post22 == 0 /\ -OuterIndex5^post22+OuterIndex5^0 == 0 /\ -InnerIndex6^post22+InnerIndex6^0 == 0 /\ -OuterIndex8^post22+OuterIndex8^0 == 0 /\ -Seed^post22+Seed^0 == 0 /\ Outer13^0-Outer13^post22 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post22 == 0 /\ Inner14^0-Inner14^post22 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l16
   0: l0 -> l1 : Outer13^0'=Outer13^post0, Inner14^0'=Inner14^post0, ret_RandomInteger17^0'=ret_RandomInteger17^post0, OuterIndex8^0'=OuterIndex8^post0, InnerIndex9^0'=InnerIndex9^post0, Index15^0'=Index15^post0, ret_RandomInteger16^0'=ret_RandomInteger16^post0, OuterIndex5^0'=OuterIndex5^post0, InnerIndex6^0'=InnerIndex6^post0, Seed^0'=Seed^post0, (-OuterIndex8^post0+OuterIndex8^0 == 0 /\ Inner14^0-Inner14^post0 == 0 /\ Index15^0-Index15^post0 == 0 /\ ret_RandomInteger16^0-ret_RandomInteger16^post0 == 0 /\ -OuterIndex5^post0+OuterIndex5^0 == 0 /\ -Seed^post0+Seed^0 == 0 /\ Outer13^0-Outer13^post0 == 0 /\ -InnerIndex6^post0+InnerIndex6^0 == 0 /\ -InnerIndex9^post0+InnerIndex9^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post0 == 0), cost: 1
  19: l1 -> l4 : Outer13^0'=Outer13^post19, Inner14^0'=Inner14^post19, ret_RandomInteger17^0'=ret_RandomInteger17^post19, OuterIndex8^0'=OuterIndex8^post19, InnerIndex9^0'=InnerIndex9^post19, Index15^0'=Index15^post19, ret_RandomInteger16^0'=ret_RandomInteger16^post19, OuterIndex5^0'=OuterIndex5^post19, InnerIndex6^0'=InnerIndex6^post19, Seed^0'=Seed^post19, (InnerIndex6^0-InnerIndex6^post19 == 0 /\ -ret_RandomInteger16^post19+ret_RandomInteger16^0 == 0 /\ -Seed^post19+Seed^0 == 0 /\ -Index15^post19+Index15^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post19 == 0 /\ InnerIndex9^0-InnerIndex9^post19 == 0 /\ OuterIndex8^post19 == 0 /\ -Inner14^post19+Inner14^0 == 0 /\ 20-OuterIndex5^0 <= 0 /\ -OuterIndex5^post19+OuterIndex5^0 == 0 /\ Outer13^0-Outer13^post19 == 0), cost: 1
  20: l1 -> l2 : Outer13^0'=Outer13^post20, Inner14^0'=Inner14^post20, ret_RandomInteger17^0'=ret_RandomInteger17^post20, OuterIndex8^0'=OuterIndex8^post20, InnerIndex9^0'=InnerIndex9^post20, Index15^0'=Index15^post20, ret_RandomInteger16^0'=ret_RandomInteger16^post20, OuterIndex5^0'=OuterIndex5^post20, InnerIndex6^0'=InnerIndex6^post20, Seed^0'=Seed^post20, (InnerIndex6^post20 == 0 /\ Outer13^0-Outer13^post20 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post20 == 0 /\ -OuterIndex5^post20+OuterIndex5^0 == 0 /\ -19+OuterIndex5^0 <= 0 /\ -ret_RandomInteger16^post20+ret_RandomInteger16^0 == 0 /\ Inner14^0-Inner14^post20 == 0 /\ -Seed^post20+Seed^0 == 0 /\ -Index15^post20+Index15^0 == 0 /\ InnerIndex9^0-InnerIndex9^post20 == 0 /\ OuterIndex8^0-OuterIndex8^post20 == 0), cost: 1
   1: l2 -> l3 : Outer13^0'=Outer13^post1, Inner14^0'=Inner14^post1, ret_RandomInteger17^0'=ret_RandomInteger17^post1, OuterIndex8^0'=OuterIndex8^post1, InnerIndex9^0'=InnerIndex9^post1, Index15^0'=Index15^post1, ret_RandomInteger16^0'=ret_RandomInteger16^post1, OuterIndex5^0'=OuterIndex5^post1, InnerIndex6^0'=InnerIndex6^post1, Seed^0'=Seed^post1, (ret_RandomInteger16^0-ret_RandomInteger16^post1 == 0 /\ -InnerIndex9^post1+InnerIndex9^0 == 0 /\ -Seed^post1+Seed^0 == 0 /\ Inner14^0-Inner14^post1 == 0 /\ -OuterIndex8^post1+OuterIndex8^0 == 0 /\ Index15^0-Index15^post1 == 0 /\ -ret_RandomInteger17^post1+ret_RandomInteger17^0 == 0 /\ -OuterIndex5^post1+OuterIndex5^0 == 0 /\ Outer13^0-Outer13^post1 == 0 /\ -InnerIndex6^post1+InnerIndex6^0 == 0), cost: 1
  17: l3 -> l0 : Outer13^0'=Outer13^post17, Inner14^0'=Inner14^post17, ret_RandomInteger17^0'=ret_RandomInteger17^post17, OuterIndex8^0'=OuterIndex8^post17, InnerIndex9^0'=InnerIndex9^post17, Index15^0'=Index15^post17, ret_RandomInteger16^0'=ret_RandomInteger16^post17, OuterIndex5^0'=OuterIndex5^post17, InnerIndex6^0'=InnerIndex6^post17, Seed^0'=Seed^post17, (InnerIndex9^0-InnerIndex9^post17 == 0 /\ -Index15^post17+Index15^0 == 0 /\ 20-InnerIndex6^0 <= 0 /\ -1-OuterIndex5^0+OuterIndex5^post17 == 0 /\ -InnerIndex6^post17+InnerIndex6^0 == 0 /\ OuterIndex8^0-OuterIndex8^post17 == 0 /\ Outer13^0-Outer13^post17 == 0 /\ -Inner14^post17+Inner14^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post17 == 0 /\ -ret_RandomInteger16^post17+ret_RandomInteger16^0 == 0 /\ -Seed^post17+Seed^0 == 0), cost: 1
  18: l3 -> l2 : Outer13^0'=Outer13^post18, Inner14^0'=Inner14^post18, ret_RandomInteger17^0'=ret_RandomInteger17^post18, OuterIndex8^0'=OuterIndex8^post18, InnerIndex9^0'=InnerIndex9^post18, Index15^0'=Index15^post18, ret_RandomInteger16^0'=ret_RandomInteger16^post18, OuterIndex5^0'=OuterIndex5^post18, InnerIndex6^0'=InnerIndex6^post18, Seed^0'=Seed^post18, (0 == 0 /\ -Index15^post18+Index15^0 == 0 /\ InnerIndex9^0-InnerIndex9^post18 == 0 /\ -1+InnerIndex6^post18-InnerIndex6^0 == 0 /\ OuterIndex8^0-OuterIndex8^post18 == 0 /\ -19+InnerIndex6^0 <= 0 /\ ret_RandomInteger16^post18-Seed^post18 == 0 /\ Outer13^0-Outer13^post18 == 0 /\ Inner14^0-Inner14^post18 == 0 /\ OuterIndex5^0-OuterIndex5^post18 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post18 == 0), cost: 1
   2: l4 -> l5 : Outer13^0'=Outer13^post2, Inner14^0'=Inner14^post2, ret_RandomInteger17^0'=ret_RandomInteger17^post2, OuterIndex8^0'=OuterIndex8^post2, InnerIndex9^0'=InnerIndex9^post2, Index15^0'=Index15^post2, ret_RandomInteger16^0'=ret_RandomInteger16^post2, OuterIndex5^0'=OuterIndex5^post2, InnerIndex6^0'=InnerIndex6^post2, Seed^0'=Seed^post2, (ret_RandomInteger16^0-ret_RandomInteger16^post2 == 0 /\ -InnerIndex9^post2+InnerIndex9^0 == 0 /\ -Seed^post2+Seed^0 == 0 /\ -OuterIndex8^post2+OuterIndex8^0 == 0 /\ Index15^0-Index15^post2 == 0 /\ Inner14^0-Inner14^post2 == 0 /\ -ret_RandomInteger17^post2+ret_RandomInteger17^0 == 0 /\ -OuterIndex5^post2+OuterIndex5^0 == 0 /\ Outer13^0-Outer13^post2 == 0 /\ -InnerIndex6^post2+InnerIndex6^0 == 0), cost: 1
  13: l5 -> l10 : Outer13^0'=Outer13^post13, Inner14^0'=Inner14^post13, ret_RandomInteger17^0'=ret_RandomInteger17^post13, OuterIndex8^0'=OuterIndex8^post13, InnerIndex9^0'=InnerIndex9^post13, Index15^0'=Index15^post13, ret_RandomInteger16^0'=ret_RandomInteger16^post13, OuterIndex5^0'=OuterIndex5^post13, InnerIndex6^0'=InnerIndex6^post13, Seed^0'=Seed^post13, (ret_RandomInteger16^0-ret_RandomInteger16^post13 == 0 /\ -InnerIndex9^post13+InnerIndex9^0 == 0 /\ -OuterIndex8^post13+OuterIndex8^0 == 0 /\ 20-OuterIndex8^0 <= 0 /\ Inner14^0-Inner14^post13 == 0 /\ -InnerIndex6^post13+InnerIndex6^0 == 0 /\ Index15^0-Index15^post13 == 0 /\ -ret_RandomInteger17^post13+ret_RandomInteger17^0 == 0 /\ Outer13^post13 == 0 /\ -OuterIndex5^post13+OuterIndex5^0 == 0 /\ -Seed^post13+Seed^0 == 0), cost: 1
  14: l5 -> l13 : Outer13^0'=Outer13^post14, Inner14^0'=Inner14^post14, ret_RandomInteger17^0'=ret_RandomInteger17^post14, OuterIndex8^0'=OuterIndex8^post14, InnerIndex9^0'=InnerIndex9^post14, Index15^0'=Index15^post14, ret_RandomInteger16^0'=ret_RandomInteger16^post14, OuterIndex5^0'=OuterIndex5^post14, InnerIndex6^0'=InnerIndex6^post14, Seed^0'=Seed^post14, (Index15^0-Index15^post14 == 0 /\ -19+OuterIndex8^0 <= 0 /\ Outer13^0-Outer13^post14 == 0 /\ Inner14^0-Inner14^post14 == 0 /\ InnerIndex9^post14 == 0 /\ -Seed^post14+Seed^0 == 0 /\ -OuterIndex5^post14+OuterIndex5^0 == 0 /\ -InnerIndex6^post14+InnerIndex6^0 == 0 /\ -ret_RandomInteger17^post14+ret_RandomInteger17^0 == 0 /\ OuterIndex8^0-OuterIndex8^post14 == 0 /\ -ret_RandomInteger16^post14+ret_RandomInteger16^0 == 0), cost: 1
   3: l6 -> l7 : Outer13^0'=Outer13^post3, Inner14^0'=Inner14^post3, ret_RandomInteger17^0'=ret_RandomInteger17^post3, OuterIndex8^0'=OuterIndex8^post3, InnerIndex9^0'=InnerIndex9^post3, Index15^0'=Index15^post3, ret_RandomInteger16^0'=ret_RandomInteger16^post3, OuterIndex5^0'=OuterIndex5^post3, InnerIndex6^0'=InnerIndex6^post3, Seed^0'=Seed^post3, (Outer13^0-Outer13^post3 == 0 /\ -ret_RandomInteger16^post3+ret_RandomInteger16^0 == 0 /\ -Index15^post3+Index15^0 == 0 /\ OuterIndex5^0-OuterIndex5^post3 == 0 /\ -InnerIndex6^post3+InnerIndex6^0 == 0 /\ 20-Index15^0 <= 0 /\ -ret_RandomInteger17^post3+ret_RandomInteger17^0 == 0 /\ InnerIndex9^0-InnerIndex9^post3 == 0 /\ OuterIndex8^0-OuterIndex8^post3 == 0 /\ -1-Inner14^0+Inner14^post3 == 0 /\ -Seed^post3+Seed^0 == 0), cost: 1
   4: l6 -> l8 : Outer13^0'=Outer13^post4, Inner14^0'=Inner14^post4, ret_RandomInteger17^0'=ret_RandomInteger17^post4, OuterIndex8^0'=OuterIndex8^post4, InnerIndex9^0'=InnerIndex9^post4, Index15^0'=Index15^post4, ret_RandomInteger16^0'=ret_RandomInteger16^post4, OuterIndex5^0'=OuterIndex5^post4, InnerIndex6^0'=InnerIndex6^post4, Seed^0'=Seed^post4, (-ret_RandomInteger16^post4+ret_RandomInteger16^0 == 0 /\ InnerIndex9^0-InnerIndex9^post4 == 0 /\ OuterIndex8^0-OuterIndex8^post4 == 0 /\ -InnerIndex6^post4+InnerIndex6^0 == 0 /\ OuterIndex5^0-OuterIndex5^post4 == 0 /\ -Seed^post4+Seed^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post4 == 0 /\ -Outer13^post4+Outer13^0 == 0 /\ Inner14^0-Inner14^post4 == 0 /\ -19+Index15^0 <= 0 /\ -1+Index15^post4-Index15^0 == 0), cost: 1
  15: l7 -> l9 : Outer13^0'=Outer13^post15, Inner14^0'=Inner14^post15, ret_RandomInteger17^0'=ret_RandomInteger17^post15, OuterIndex8^0'=OuterIndex8^post15, InnerIndex9^0'=InnerIndex9^post15, Index15^0'=Index15^post15, ret_RandomInteger16^0'=ret_RandomInteger16^post15, OuterIndex5^0'=OuterIndex5^post15, InnerIndex6^0'=InnerIndex6^post15, Seed^0'=Seed^post15, (-OuterIndex5^post15+OuterIndex5^0 == 0 /\ Outer13^0-Outer13^post15 == 0 /\ -InnerIndex9^post15+InnerIndex9^0 == 0 /\ Inner14^0-Inner14^post15 == 0 /\ Index15^0-Index15^post15 == 0 /\ -Seed^post15+Seed^0 == 0 /\ -InnerIndex6^post15+InnerIndex6^0 == 0 /\ OuterIndex8^0-OuterIndex8^post15 == 0 /\ -ret_RandomInteger16^post15+ret_RandomInteger16^0 == 0 /\ -ret_RandomInteger17^post15+ret_RandomInteger17^0 == 0), cost: 1
  16: l8 -> l6 : Outer13^0'=Outer13^post16, Inner14^0'=Inner14^post16, ret_RandomInteger17^0'=ret_RandomInteger17^post16, OuterIndex8^0'=OuterIndex8^post16, InnerIndex9^0'=InnerIndex9^post16, Index15^0'=Index15^post16, ret_RandomInteger16^0'=ret_RandomInteger16^post16, OuterIndex5^0'=OuterIndex5^post16, InnerIndex6^0'=InnerIndex6^post16, Seed^0'=Seed^post16, (-ret_RandomInteger17^post16+ret_RandomInteger17^0 == 0 /\ -InnerIndex6^post16+InnerIndex6^0 == 0 /\ Outer13^0-Outer13^post16 == 0 /\ -ret_RandomInteger16^post16+ret_RandomInteger16^0 == 0 /\ InnerIndex9^0-InnerIndex9^post16 == 0 /\ OuterIndex8^0-OuterIndex8^post16 == 0 /\ -Seed^post16+Seed^0 == 0 /\ -Index15^post16+Index15^0 == 0 /\ OuterIndex5^0-OuterIndex5^post16 == 0 /\ Inner14^0-Inner14^post16 == 0), cost: 1
   5: l9 -> l10 : Outer13^0'=Outer13^post5, Inner14^0'=Inner14^post5, ret_RandomInteger17^0'=ret_RandomInteger17^post5, OuterIndex8^0'=OuterIndex8^post5, InnerIndex9^0'=InnerIndex9^post5, Index15^0'=Index15^post5, ret_RandomInteger16^0'=ret_RandomInteger16^post5, OuterIndex5^0'=OuterIndex5^post5, InnerIndex6^0'=InnerIndex6^post5, Seed^0'=Seed^post5, (-ret_RandomInteger16^post5+ret_RandomInteger16^0 == 0 /\ OuterIndex8^0-OuterIndex8^post5 == 0 /\ InnerIndex9^0-InnerIndex9^post5 == 0 /\ -Index15^post5+Index15^0 == 0 /\ -InnerIndex6^post5+InnerIndex6^0 == 0 /\ OuterIndex5^0-OuterIndex5^post5 == 0 /\ -1-Outer13^0+Outer13^post5 == 0 /\ -Seed^post5+Seed^0 == 0 /\ Inner14^0-Inner14^post5 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post5 == 0 /\ 20-Inner14^0 <= 0), cost: 1
   6: l9 -> l8 : Outer13^0'=Outer13^post6, Inner14^0'=Inner14^post6, ret_RandomInteger17^0'=ret_RandomInteger17^post6, OuterIndex8^0'=OuterIndex8^post6, InnerIndex9^0'=InnerIndex9^post6, Index15^0'=Index15^post6, ret_RandomInteger16^0'=ret_RandomInteger16^post6, OuterIndex5^0'=OuterIndex5^post6, InnerIndex6^0'=InnerIndex6^post6, Seed^0'=Seed^post6, (InnerIndex9^0-InnerIndex9^post6 == 0 /\ -InnerIndex6^post6+InnerIndex6^0 == 0 /\ Index15^post6 == 0 /\ OuterIndex8^0-OuterIndex8^post6 == 0 /\ Outer13^0-Outer13^post6 == 0 /\ -Inner14^post6+Inner14^0 == 0 /\ -OuterIndex5^post6+OuterIndex5^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post6 == 0 /\ -19+Inner14^0 <= 0 /\ -ret_RandomInteger16^post6+ret_RandomInteger16^0 == 0 /\ -Seed^post6+Seed^0 == 0), cost: 1
  10: l10 -> l11 : Outer13^0'=Outer13^post10, Inner14^0'=Inner14^post10, ret_RandomInteger17^0'=ret_RandomInteger17^post10, OuterIndex8^0'=OuterIndex8^post10, InnerIndex9^0'=InnerIndex9^post10, Index15^0'=Index15^post10, ret_RandomInteger16^0'=ret_RandomInteger16^post10, OuterIndex5^0'=OuterIndex5^post10, InnerIndex6^0'=InnerIndex6^post10, Seed^0'=Seed^post10, (-OuterIndex8^post10+OuterIndex8^0 == 0 /\ Outer13^0-Outer13^post10 == 0 /\ -Seed^post10+Seed^0 == 0 /\ Inner14^0-Inner14^post10 == 0 /\ Index15^0-Index15^post10 == 0 /\ -OuterIndex5^post10+OuterIndex5^0 == 0 /\ ret_RandomInteger16^0-ret_RandomInteger16^post10 == 0 /\ InnerIndex9^0-InnerIndex9^post10 == 0 /\ -InnerIndex6^post10+InnerIndex6^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post10 == 0), cost: 1
   8: l11 -> l7 : Outer13^0'=Outer13^post8, Inner14^0'=Inner14^post8, ret_RandomInteger17^0'=ret_RandomInteger17^post8, OuterIndex8^0'=OuterIndex8^post8, InnerIndex9^0'=InnerIndex9^post8, Index15^0'=Index15^post8, ret_RandomInteger16^0'=ret_RandomInteger16^post8, OuterIndex5^0'=OuterIndex5^post8, InnerIndex6^0'=InnerIndex6^post8, Seed^0'=Seed^post8, (Inner14^post8 == 0 /\ Outer13^0-Outer13^post8 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post8 == 0 /\ -Seed^post8+Seed^0 == 0 /\ InnerIndex9^0-InnerIndex9^post8 == 0 /\ -InnerIndex6^post8+InnerIndex6^0 == 0 /\ -ret_RandomInteger16^post8+ret_RandomInteger16^0 == 0 /\ -OuterIndex5^post8+OuterIndex5^0 == 0 /\ OuterIndex8^0-OuterIndex8^post8 == 0 /\ -Index15^post8+Index15^0 == 0 /\ -19+Outer13^0 <= 0), cost: 1
   9: l13 -> l14 : Outer13^0'=Outer13^post9, Inner14^0'=Inner14^post9, ret_RandomInteger17^0'=ret_RandomInteger17^post9, OuterIndex8^0'=OuterIndex8^post9, InnerIndex9^0'=InnerIndex9^post9, Index15^0'=Index15^post9, ret_RandomInteger16^0'=ret_RandomInteger16^post9, OuterIndex5^0'=OuterIndex5^post9, InnerIndex6^0'=InnerIndex6^post9, Seed^0'=Seed^post9, (-ret_RandomInteger16^post9+ret_RandomInteger16^0 == 0 /\ -Inner14^post9+Inner14^0 == 0 /\ -Seed^post9+Seed^0 == 0 /\ -Index15^post9+Index15^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post9 == 0 /\ InnerIndex6^0-InnerIndex6^post9 == 0 /\ OuterIndex8^0-OuterIndex8^post9 == 0 /\ InnerIndex9^0-InnerIndex9^post9 == 0 /\ Outer13^0-Outer13^post9 == 0 /\ -OuterIndex5^post9+OuterIndex5^0 == 0), cost: 1
  11: l14 -> l4 : Outer13^0'=Outer13^post11, Inner14^0'=Inner14^post11, ret_RandomInteger17^0'=ret_RandomInteger17^post11, OuterIndex8^0'=OuterIndex8^post11, InnerIndex9^0'=InnerIndex9^post11, Index15^0'=Index15^post11, ret_RandomInteger16^0'=ret_RandomInteger16^post11, OuterIndex5^0'=OuterIndex5^post11, InnerIndex6^0'=InnerIndex6^post11, Seed^0'=Seed^post11, (-1+OuterIndex8^post11-OuterIndex8^0 == 0 /\ 20-InnerIndex9^0 <= 0 /\ -Seed^post11+Seed^0 == 0 /\ -OuterIndex5^post11+OuterIndex5^0 == 0 /\ Index15^0-Index15^post11 == 0 /\ ret_RandomInteger16^0-ret_RandomInteger16^post11 == 0 /\ Outer13^0-Outer13^post11 == 0 /\ -InnerIndex6^post11+InnerIndex6^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post11 == 0 /\ InnerIndex9^0-InnerIndex9^post11 == 0 /\ Inner14^0-Inner14^post11 == 0), cost: 1
  12: l14 -> l13 : Outer13^0'=Outer13^post12, Inner14^0'=Inner14^post12, ret_RandomInteger17^0'=ret_RandomInteger17^post12, OuterIndex8^0'=OuterIndex8^post12, InnerIndex9^0'=InnerIndex9^post12, Index15^0'=Index15^post12, ret_RandomInteger16^0'=ret_RandomInteger16^post12, OuterIndex5^0'=OuterIndex5^post12, InnerIndex6^0'=InnerIndex6^post12, Seed^0'=Seed^post12, (0 == 0 /\ ret_RandomInteger17^post12-Seed^post12 == 0 /\ -19+InnerIndex9^0 <= 0 /\ -OuterIndex8^post12+OuterIndex8^0 == 0 /\ ret_RandomInteger16^0-ret_RandomInteger16^post12 == 0 /\ -InnerIndex6^post12+InnerIndex6^0 == 0 /\ Outer13^0-Outer13^post12 == 0 /\ -1+InnerIndex9^post12-InnerIndex9^0 == 0 /\ Inner14^0-Inner14^post12 == 0 /\ Index15^0-Index15^post12 == 0 /\ -OuterIndex5^post12+OuterIndex5^0 == 0), cost: 1
  21: l15 -> l0 : Outer13^0'=Outer13^post21, Inner14^0'=Inner14^post21, ret_RandomInteger17^0'=ret_RandomInteger17^post21, OuterIndex8^0'=OuterIndex8^post21, InnerIndex9^0'=InnerIndex9^post21, Index15^0'=Index15^post21, ret_RandomInteger16^0'=ret_RandomInteger16^post21, OuterIndex5^0'=OuterIndex5^post21, InnerIndex6^0'=InnerIndex6^post21, Seed^0'=Seed^post21, (ret_RandomInteger17^0-ret_RandomInteger17^post21 == 0 /\ -OuterIndex8^post21+OuterIndex8^0 == 0 /\ OuterIndex5^post21 == 0 /\ Outer13^0-Outer13^post21 == 0 /\ Inner14^0-Inner14^post21 == 0 /\ Index15^0-Index15^post21 == 0 /\ ret_RandomInteger16^0-ret_RandomInteger16^post21 == 0 /\ InnerIndex9^0-InnerIndex9^post21 == 0 /\ Seed^post21 == 0 /\ -InnerIndex6^post21+InnerIndex6^0 == 0), cost: 1
  22: l16 -> l15 : Outer13^0'=Outer13^post22, Inner14^0'=Inner14^post22, ret_RandomInteger17^0'=ret_RandomInteger17^post22, OuterIndex8^0'=OuterIndex8^post22, InnerIndex9^0'=InnerIndex9^post22, Index15^0'=Index15^post22, ret_RandomInteger16^0'=ret_RandomInteger16^post22, OuterIndex5^0'=OuterIndex5^post22, InnerIndex6^0'=InnerIndex6^post22, Seed^0'=Seed^post22, (Index15^0-Index15^post22 == 0 /\ -InnerIndex9^post22+InnerIndex9^0 == 0 /\ ret_RandomInteger16^0-ret_RandomInteger16^post22 == 0 /\ -OuterIndex5^post22+OuterIndex5^0 == 0 /\ -InnerIndex6^post22+InnerIndex6^0 == 0 /\ -OuterIndex8^post22+OuterIndex8^0 == 0 /\ -Seed^post22+Seed^0 == 0 /\ Outer13^0-Outer13^post22 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post22 == 0 /\ Inner14^0-Inner14^post22 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : Outer13^0'=Outer13^post0, Inner14^0'=Inner14^post0, ret_RandomInteger17^0'=ret_RandomInteger17^post0, OuterIndex8^0'=OuterIndex8^post0, InnerIndex9^0'=InnerIndex9^post0, Index15^0'=Index15^post0, ret_RandomInteger16^0'=ret_RandomInteger16^post0, OuterIndex5^0'=OuterIndex5^post0, InnerIndex6^0'=InnerIndex6^post0, Seed^0'=Seed^post0, (-OuterIndex8^post0+OuterIndex8^0 == 0 /\ Inner14^0-Inner14^post0 == 0 /\ Index15^0-Index15^post0 == 0 /\ ret_RandomInteger16^0-ret_RandomInteger16^post0 == 0 /\ -OuterIndex5^post0+OuterIndex5^0 == 0 /\ -Seed^post0+Seed^0 == 0 /\ Outer13^0-Outer13^post0 == 0 /\ -InnerIndex6^post0+InnerIndex6^0 == 0 /\ -InnerIndex9^post0+InnerIndex9^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post0 == 0), cost: 1
New rule:
l0 -> l1 : TRUE, cost: 1

Applied preprocessing
Original rule:
l2 -> l3 : Outer13^0'=Outer13^post1, Inner14^0'=Inner14^post1, ret_RandomInteger17^0'=ret_RandomInteger17^post1, OuterIndex8^0'=OuterIndex8^post1, InnerIndex9^0'=InnerIndex9^post1, Index15^0'=Index15^post1, ret_RandomInteger16^0'=ret_RandomInteger16^post1, OuterIndex5^0'=OuterIndex5^post1, InnerIndex6^0'=InnerIndex6^post1, Seed^0'=Seed^post1, (ret_RandomInteger16^0-ret_RandomInteger16^post1 == 0 /\ -InnerIndex9^post1+InnerIndex9^0 == 0 /\ -Seed^post1+Seed^0 == 0 /\ Inner14^0-Inner14^post1 == 0 /\ -OuterIndex8^post1+OuterIndex8^0 == 0 /\ Index15^0-Index15^post1 == 0 /\ -ret_RandomInteger17^post1+ret_RandomInteger17^0 == 0 /\ -OuterIndex5^post1+OuterIndex5^0 == 0 /\ Outer13^0-Outer13^post1 == 0 /\ -InnerIndex6^post1+InnerIndex6^0 == 0), cost: 1
New rule:
l2 -> l3 : TRUE, cost: 1

Applied preprocessing
Original rule:
l4 -> l5 : Outer13^0'=Outer13^post2, Inner14^0'=Inner14^post2, ret_RandomInteger17^0'=ret_RandomInteger17^post2, OuterIndex8^0'=OuterIndex8^post2, InnerIndex9^0'=InnerIndex9^post2, Index15^0'=Index15^post2, ret_RandomInteger16^0'=ret_RandomInteger16^post2, OuterIndex5^0'=OuterIndex5^post2, InnerIndex6^0'=InnerIndex6^post2, Seed^0'=Seed^post2, (ret_RandomInteger16^0-ret_RandomInteger16^post2 == 0 /\ -InnerIndex9^post2+InnerIndex9^0 == 0 /\ -Seed^post2+Seed^0 == 0 /\ -OuterIndex8^post2+OuterIndex8^0 == 0 /\ Index15^0-Index15^post2 == 0 /\ Inner14^0-Inner14^post2 == 0 /\ -ret_RandomInteger17^post2+ret_RandomInteger17^0 == 0 /\ -OuterIndex5^post2+OuterIndex5^0 == 0 /\ Outer13^0-Outer13^post2 == 0 /\ -InnerIndex6^post2+InnerIndex6^0 == 0), cost: 1
New rule:
l4 -> l5 : TRUE, cost: 1

Applied preprocessing
Original rule:
l6 -> l7 : Outer13^0'=Outer13^post3, Inner14^0'=Inner14^post3, ret_RandomInteger17^0'=ret_RandomInteger17^post3, OuterIndex8^0'=OuterIndex8^post3, InnerIndex9^0'=InnerIndex9^post3, Index15^0'=Index15^post3, ret_RandomInteger16^0'=ret_RandomInteger16^post3, OuterIndex5^0'=OuterIndex5^post3, InnerIndex6^0'=InnerIndex6^post3, Seed^0'=Seed^post3, (Outer13^0-Outer13^post3 == 0 /\ -ret_RandomInteger16^post3+ret_RandomInteger16^0 == 0 /\ -Index15^post3+Index15^0 == 0 /\ OuterIndex5^0-OuterIndex5^post3 == 0 /\ -InnerIndex6^post3+InnerIndex6^0 == 0 /\ 20-Index15^0 <= 0 /\ -ret_RandomInteger17^post3+ret_RandomInteger17^0 == 0 /\ InnerIndex9^0-InnerIndex9^post3 == 0 /\ OuterIndex8^0-OuterIndex8^post3 == 0 /\ -1-Inner14^0+Inner14^post3 == 0 /\ -Seed^post3+Seed^0 == 0), cost: 1
New rule:
l6 -> l7 : Inner14^0'=1+Inner14^0, -20+Index15^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l6 -> l8 : Outer13^0'=Outer13^post4, Inner14^0'=Inner14^post4, ret_RandomInteger17^0'=ret_RandomInteger17^post4, OuterIndex8^0'=OuterIndex8^post4, InnerIndex9^0'=InnerIndex9^post4, Index15^0'=Index15^post4, ret_RandomInteger16^0'=ret_RandomInteger16^post4, OuterIndex5^0'=OuterIndex5^post4, InnerIndex6^0'=InnerIndex6^post4, Seed^0'=Seed^post4, (-ret_RandomInteger16^post4+ret_RandomInteger16^0 == 0 /\ InnerIndex9^0-InnerIndex9^post4 == 0 /\ OuterIndex8^0-OuterIndex8^post4 == 0 /\ -InnerIndex6^post4+InnerIndex6^0 == 0 /\ OuterIndex5^0-OuterIndex5^post4 == 0 /\ -Seed^post4+Seed^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post4 == 0 /\ -Outer13^post4+Outer13^0 == 0 /\ Inner14^0-Inner14^post4 == 0 /\ -19+Index15^0 <= 0 /\ -1+Index15^post4-Index15^0 == 0), cost: 1
New rule:
l6 -> l8 : Index15^0'=1+Index15^0, -19+Index15^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l9 -> l10 : Outer13^0'=Outer13^post5, Inner14^0'=Inner14^post5, ret_RandomInteger17^0'=ret_RandomInteger17^post5, OuterIndex8^0'=OuterIndex8^post5, InnerIndex9^0'=InnerIndex9^post5, Index15^0'=Index15^post5, ret_RandomInteger16^0'=ret_RandomInteger16^post5, OuterIndex5^0'=OuterIndex5^post5, InnerIndex6^0'=InnerIndex6^post5, Seed^0'=Seed^post5, (-ret_RandomInteger16^post5+ret_RandomInteger16^0 == 0 /\ OuterIndex8^0-OuterIndex8^post5 == 0 /\ InnerIndex9^0-InnerIndex9^post5 == 0 /\ -Index15^post5+Index15^0 == 0 /\ -InnerIndex6^post5+InnerIndex6^0 == 0 /\ OuterIndex5^0-OuterIndex5^post5 == 0 /\ -1-Outer13^0+Outer13^post5 == 0 /\ -Seed^post5+Seed^0 == 0 /\ Inner14^0-Inner14^post5 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post5 == 0 /\ 20-Inner14^0 <= 0), cost: 1
New rule:
l9 -> l10 : Outer13^0'=1+Outer13^0, -20+Inner14^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l9 -> l8 : Outer13^0'=Outer13^post6, Inner14^0'=Inner14^post6, ret_RandomInteger17^0'=ret_RandomInteger17^post6, OuterIndex8^0'=OuterIndex8^post6, InnerIndex9^0'=InnerIndex9^post6, Index15^0'=Index15^post6, ret_RandomInteger16^0'=ret_RandomInteger16^post6, OuterIndex5^0'=OuterIndex5^post6, InnerIndex6^0'=InnerIndex6^post6, Seed^0'=Seed^post6, (InnerIndex9^0-InnerIndex9^post6 == 0 /\ -InnerIndex6^post6+InnerIndex6^0 == 0 /\ Index15^post6 == 0 /\ OuterIndex8^0-OuterIndex8^post6 == 0 /\ Outer13^0-Outer13^post6 == 0 /\ -Inner14^post6+Inner14^0 == 0 /\ -OuterIndex5^post6+OuterIndex5^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post6 == 0 /\ -19+Inner14^0 <= 0 /\ -ret_RandomInteger16^post6+ret_RandomInteger16^0 == 0 /\ -Seed^post6+Seed^0 == 0), cost: 1
New rule:
l9 -> l8 : Index15^0'=0, -19+Inner14^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l11 -> l7 : Outer13^0'=Outer13^post8, Inner14^0'=Inner14^post8, ret_RandomInteger17^0'=ret_RandomInteger17^post8, OuterIndex8^0'=OuterIndex8^post8, InnerIndex9^0'=InnerIndex9^post8, Index15^0'=Index15^post8, ret_RandomInteger16^0'=ret_RandomInteger16^post8, OuterIndex5^0'=OuterIndex5^post8, InnerIndex6^0'=InnerIndex6^post8, Seed^0'=Seed^post8, (Inner14^post8 == 0 /\ Outer13^0-Outer13^post8 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post8 == 0 /\ -Seed^post8+Seed^0 == 0 /\ InnerIndex9^0-InnerIndex9^post8 == 0 /\ -InnerIndex6^post8+InnerIndex6^0 == 0 /\ -ret_RandomInteger16^post8+ret_RandomInteger16^0 == 0 /\ -OuterIndex5^post8+OuterIndex5^0 == 0 /\ OuterIndex8^0-OuterIndex8^post8 == 0 /\ -Index15^post8+Index15^0 == 0 /\ -19+Outer13^0 <= 0), cost: 1
New rule:
l11 -> l7 : Inner14^0'=0, -19+Outer13^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l13 -> l14 : Outer13^0'=Outer13^post9, Inner14^0'=Inner14^post9, ret_RandomInteger17^0'=ret_RandomInteger17^post9, OuterIndex8^0'=OuterIndex8^post9, InnerIndex9^0'=InnerIndex9^post9, Index15^0'=Index15^post9, ret_RandomInteger16^0'=ret_RandomInteger16^post9, OuterIndex5^0'=OuterIndex5^post9, InnerIndex6^0'=InnerIndex6^post9, Seed^0'=Seed^post9, (-ret_RandomInteger16^post9+ret_RandomInteger16^0 == 0 /\ -Inner14^post9+Inner14^0 == 0 /\ -Seed^post9+Seed^0 == 0 /\ -Index15^post9+Index15^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post9 == 0 /\ InnerIndex6^0-InnerIndex6^post9 == 0 /\ OuterIndex8^0-OuterIndex8^post9 == 0 /\ InnerIndex9^0-InnerIndex9^post9 == 0 /\ Outer13^0-Outer13^post9 == 0 /\ -OuterIndex5^post9+OuterIndex5^0 == 0), cost: 1
New rule:
l13 -> l14 : TRUE, cost: 1

Applied preprocessing
Original rule:
l10 -> l11 : Outer13^0'=Outer13^post10, Inner14^0'=Inner14^post10, ret_RandomInteger17^0'=ret_RandomInteger17^post10, OuterIndex8^0'=OuterIndex8^post10, InnerIndex9^0'=InnerIndex9^post10, Index15^0'=Index15^post10, ret_RandomInteger16^0'=ret_RandomInteger16^post10, OuterIndex5^0'=OuterIndex5^post10, InnerIndex6^0'=InnerIndex6^post10, Seed^0'=Seed^post10, (-OuterIndex8^post10+OuterIndex8^0 == 0 /\ Outer13^0-Outer13^post10 == 0 /\ -Seed^post10+Seed^0 == 0 /\ Inner14^0-Inner14^post10 == 0 /\ Index15^0-Index15^post10 == 0 /\ -OuterIndex5^post10+OuterIndex5^0 == 0 /\ ret_RandomInteger16^0-ret_RandomInteger16^post10 == 0 /\ InnerIndex9^0-InnerIndex9^post10 == 0 /\ -InnerIndex6^post10+InnerIndex6^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post10 == 0), cost: 1
New rule:
l10 -> l11 : TRUE, cost: 1

Applied preprocessing
Original rule:
l14 -> l4 : Outer13^0'=Outer13^post11, Inner14^0'=Inner14^post11, ret_RandomInteger17^0'=ret_RandomInteger17^post11, OuterIndex8^0'=OuterIndex8^post11, InnerIndex9^0'=InnerIndex9^post11, Index15^0'=Index15^post11, ret_RandomInteger16^0'=ret_RandomInteger16^post11, OuterIndex5^0'=OuterIndex5^post11, InnerIndex6^0'=InnerIndex6^post11, Seed^0'=Seed^post11, (-1+OuterIndex8^post11-OuterIndex8^0 == 0 /\ 20-InnerIndex9^0 <= 0 /\ -Seed^post11+Seed^0 == 0 /\ -OuterIndex5^post11+OuterIndex5^0 == 0 /\ Index15^0-Index15^post11 == 0 /\ ret_RandomInteger16^0-ret_RandomInteger16^post11 == 0 /\ Outer13^0-Outer13^post11 == 0 /\ -InnerIndex6^post11+InnerIndex6^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post11 == 0 /\ InnerIndex9^0-InnerIndex9^post11 == 0 /\ Inner14^0-Inner14^post11 == 0), cost: 1
New rule:
l14 -> l4 : OuterIndex8^0'=1+OuterIndex8^0, -20+InnerIndex9^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l14 -> l13 : Outer13^0'=Outer13^post12, Inner14^0'=Inner14^post12, ret_RandomInteger17^0'=ret_RandomInteger17^post12, OuterIndex8^0'=OuterIndex8^post12, InnerIndex9^0'=InnerIndex9^post12, Index15^0'=Index15^post12, ret_RandomInteger16^0'=ret_RandomInteger16^post12, OuterIndex5^0'=OuterIndex5^post12, InnerIndex6^0'=InnerIndex6^post12, Seed^0'=Seed^post12, (0 == 0 /\ ret_RandomInteger17^post12-Seed^post12 == 0 /\ -19+InnerIndex9^0 <= 0 /\ -OuterIndex8^post12+OuterIndex8^0 == 0 /\ ret_RandomInteger16^0-ret_RandomInteger16^post12 == 0 /\ -InnerIndex6^post12+InnerIndex6^0 == 0 /\ Outer13^0-Outer13^post12 == 0 /\ -1+InnerIndex9^post12-InnerIndex9^0 == 0 /\ Inner14^0-Inner14^post12 == 0 /\ Index15^0-Index15^post12 == 0 /\ -OuterIndex5^post12+OuterIndex5^0 == 0), cost: 1
New rule:
l14 -> l13 : ret_RandomInteger17^0'=Seed^post12, InnerIndex9^0'=1+InnerIndex9^0, Seed^0'=Seed^post12, -19+InnerIndex9^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l5 -> l10 : Outer13^0'=Outer13^post13, Inner14^0'=Inner14^post13, ret_RandomInteger17^0'=ret_RandomInteger17^post13, OuterIndex8^0'=OuterIndex8^post13, InnerIndex9^0'=InnerIndex9^post13, Index15^0'=Index15^post13, ret_RandomInteger16^0'=ret_RandomInteger16^post13, OuterIndex5^0'=OuterIndex5^post13, InnerIndex6^0'=InnerIndex6^post13, Seed^0'=Seed^post13, (ret_RandomInteger16^0-ret_RandomInteger16^post13 == 0 /\ -InnerIndex9^post13+InnerIndex9^0 == 0 /\ -OuterIndex8^post13+OuterIndex8^0 == 0 /\ 20-OuterIndex8^0 <= 0 /\ Inner14^0-Inner14^post13 == 0 /\ -InnerIndex6^post13+InnerIndex6^0 == 0 /\ Index15^0-Index15^post13 == 0 /\ -ret_RandomInteger17^post13+ret_RandomInteger17^0 == 0 /\ Outer13^post13 == 0 /\ -OuterIndex5^post13+OuterIndex5^0 == 0 /\ -Seed^post13+Seed^0 == 0), cost: 1
New rule:
l5 -> l10 : Outer13^0'=0, -20+OuterIndex8^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l5 -> l13 : Outer13^0'=Outer13^post14, Inner14^0'=Inner14^post14, ret_RandomInteger17^0'=ret_RandomInteger17^post14, OuterIndex8^0'=OuterIndex8^post14, InnerIndex9^0'=InnerIndex9^post14, Index15^0'=Index15^post14, ret_RandomInteger16^0'=ret_RandomInteger16^post14, OuterIndex5^0'=OuterIndex5^post14, InnerIndex6^0'=InnerIndex6^post14, Seed^0'=Seed^post14, (Index15^0-Index15^post14 == 0 /\ -19+OuterIndex8^0 <= 0 /\ Outer13^0-Outer13^post14 == 0 /\ Inner14^0-Inner14^post14 == 0 /\ InnerIndex9^post14 == 0 /\ -Seed^post14+Seed^0 == 0 /\ -OuterIndex5^post14+OuterIndex5^0 == 0 /\ -InnerIndex6^post14+InnerIndex6^0 == 0 /\ -ret_RandomInteger17^post14+ret_RandomInteger17^0 == 0 /\ OuterIndex8^0-OuterIndex8^post14 == 0 /\ -ret_RandomInteger16^post14+ret_RandomInteger16^0 == 0), cost: 1
New rule:
l5 -> l13 : InnerIndex9^0'=0, -19+OuterIndex8^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l7 -> l9 : Outer13^0'=Outer13^post15, Inner14^0'=Inner14^post15, ret_RandomInteger17^0'=ret_RandomInteger17^post15, OuterIndex8^0'=OuterIndex8^post15, InnerIndex9^0'=InnerIndex9^post15, Index15^0'=Index15^post15, ret_RandomInteger16^0'=ret_RandomInteger16^post15, OuterIndex5^0'=OuterIndex5^post15, InnerIndex6^0'=InnerIndex6^post15, Seed^0'=Seed^post15, (-OuterIndex5^post15+OuterIndex5^0 == 0 /\ Outer13^0-Outer13^post15 == 0 /\ -InnerIndex9^post15+InnerIndex9^0 == 0 /\ Inner14^0-Inner14^post15 == 0 /\ Index15^0-Index15^post15 == 0 /\ -Seed^post15+Seed^0 == 0 /\ -InnerIndex6^post15+InnerIndex6^0 == 0 /\ OuterIndex8^0-OuterIndex8^post15 == 0 /\ -ret_RandomInteger16^post15+ret_RandomInteger16^0 == 0 /\ -ret_RandomInteger17^post15+ret_RandomInteger17^0 == 0), cost: 1
New rule:
l7 -> l9 : TRUE, cost: 1

Applied preprocessing
Original rule:
l8 -> l6 : Outer13^0'=Outer13^post16, Inner14^0'=Inner14^post16, ret_RandomInteger17^0'=ret_RandomInteger17^post16, OuterIndex8^0'=OuterIndex8^post16, InnerIndex9^0'=InnerIndex9^post16, Index15^0'=Index15^post16, ret_RandomInteger16^0'=ret_RandomInteger16^post16, OuterIndex5^0'=OuterIndex5^post16, InnerIndex6^0'=InnerIndex6^post16, Seed^0'=Seed^post16, (-ret_RandomInteger17^post16+ret_RandomInteger17^0 == 0 /\ -InnerIndex6^post16+InnerIndex6^0 == 0 /\ Outer13^0-Outer13^post16 == 0 /\ -ret_RandomInteger16^post16+ret_RandomInteger16^0 == 0 /\ InnerIndex9^0-InnerIndex9^post16 == 0 /\ OuterIndex8^0-OuterIndex8^post16 == 0 /\ -Seed^post16+Seed^0 == 0 /\ -Index15^post16+Index15^0 == 0 /\ OuterIndex5^0-OuterIndex5^post16 == 0 /\ Inner14^0-Inner14^post16 == 0), cost: 1
New rule:
l8 -> l6 : TRUE, cost: 1

Applied preprocessing
Original rule:
l3 -> l0 : Outer13^0'=Outer13^post17, Inner14^0'=Inner14^post17, ret_RandomInteger17^0'=ret_RandomInteger17^post17, OuterIndex8^0'=OuterIndex8^post17, InnerIndex9^0'=InnerIndex9^post17, Index15^0'=Index15^post17, ret_RandomInteger16^0'=ret_RandomInteger16^post17, OuterIndex5^0'=OuterIndex5^post17, InnerIndex6^0'=InnerIndex6^post17, Seed^0'=Seed^post17, (InnerIndex9^0-InnerIndex9^post17 == 0 /\ -Index15^post17+Index15^0 == 0 /\ 20-InnerIndex6^0 <= 0 /\ -1-OuterIndex5^0+OuterIndex5^post17 == 0 /\ -InnerIndex6^post17+InnerIndex6^0 == 0 /\ OuterIndex8^0-OuterIndex8^post17 == 0 /\ Outer13^0-Outer13^post17 == 0 /\ -Inner14^post17+Inner14^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post17 == 0 /\ -ret_RandomInteger16^post17+ret_RandomInteger16^0 == 0 /\ -Seed^post17+Seed^0 == 0), cost: 1
New rule:
l3 -> l0 : OuterIndex5^0'=1+OuterIndex5^0, -20+InnerIndex6^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l3 -> l2 : Outer13^0'=Outer13^post18, Inner14^0'=Inner14^post18, ret_RandomInteger17^0'=ret_RandomInteger17^post18, OuterIndex8^0'=OuterIndex8^post18, InnerIndex9^0'=InnerIndex9^post18, Index15^0'=Index15^post18, ret_RandomInteger16^0'=ret_RandomInteger16^post18, OuterIndex5^0'=OuterIndex5^post18, InnerIndex6^0'=InnerIndex6^post18, Seed^0'=Seed^post18, (0 == 0 /\ -Index15^post18+Index15^0 == 0 /\ InnerIndex9^0-InnerIndex9^post18 == 0 /\ -1+InnerIndex6^post18-InnerIndex6^0 == 0 /\ OuterIndex8^0-OuterIndex8^post18 == 0 /\ -19+InnerIndex6^0 <= 0 /\ ret_RandomInteger16^post18-Seed^post18 == 0 /\ Outer13^0-Outer13^post18 == 0 /\ Inner14^0-Inner14^post18 == 0 /\ OuterIndex5^0-OuterIndex5^post18 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post18 == 0), cost: 1
New rule:
l3 -> l2 : ret_RandomInteger16^0'=Seed^post18, InnerIndex6^0'=1+InnerIndex6^0, Seed^0'=Seed^post18, -19+InnerIndex6^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l4 : Outer13^0'=Outer13^post19, Inner14^0'=Inner14^post19, ret_RandomInteger17^0'=ret_RandomInteger17^post19, OuterIndex8^0'=OuterIndex8^post19, InnerIndex9^0'=InnerIndex9^post19, Index15^0'=Index15^post19, ret_RandomInteger16^0'=ret_RandomInteger16^post19, OuterIndex5^0'=OuterIndex5^post19, InnerIndex6^0'=InnerIndex6^post19, Seed^0'=Seed^post19, (InnerIndex6^0-InnerIndex6^post19 == 0 /\ -ret_RandomInteger16^post19+ret_RandomInteger16^0 == 0 /\ -Seed^post19+Seed^0 == 0 /\ -Index15^post19+Index15^0 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post19 == 0 /\ InnerIndex9^0-InnerIndex9^post19 == 0 /\ OuterIndex8^post19 == 0 /\ -Inner14^post19+Inner14^0 == 0 /\ 20-OuterIndex5^0 <= 0 /\ -OuterIndex5^post19+OuterIndex5^0 == 0 /\ Outer13^0-Outer13^post19 == 0), cost: 1
New rule:
l1 -> l4 : OuterIndex8^0'=0, -20+OuterIndex5^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l2 : Outer13^0'=Outer13^post20, Inner14^0'=Inner14^post20, ret_RandomInteger17^0'=ret_RandomInteger17^post20, OuterIndex8^0'=OuterIndex8^post20, InnerIndex9^0'=InnerIndex9^post20, Index15^0'=Index15^post20, ret_RandomInteger16^0'=ret_RandomInteger16^post20, OuterIndex5^0'=OuterIndex5^post20, InnerIndex6^0'=InnerIndex6^post20, Seed^0'=Seed^post20, (InnerIndex6^post20 == 0 /\ Outer13^0-Outer13^post20 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post20 == 0 /\ -OuterIndex5^post20+OuterIndex5^0 == 0 /\ -19+OuterIndex5^0 <= 0 /\ -ret_RandomInteger16^post20+ret_RandomInteger16^0 == 0 /\ Inner14^0-Inner14^post20 == 0 /\ -Seed^post20+Seed^0 == 0 /\ -Index15^post20+Index15^0 == 0 /\ InnerIndex9^0-InnerIndex9^post20 == 0 /\ OuterIndex8^0-OuterIndex8^post20 == 0), cost: 1
New rule:
l1 -> l2 : InnerIndex6^0'=0, -19+OuterIndex5^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l15 -> l0 : Outer13^0'=Outer13^post21, Inner14^0'=Inner14^post21, ret_RandomInteger17^0'=ret_RandomInteger17^post21, OuterIndex8^0'=OuterIndex8^post21, InnerIndex9^0'=InnerIndex9^post21, Index15^0'=Index15^post21, ret_RandomInteger16^0'=ret_RandomInteger16^post21, OuterIndex5^0'=OuterIndex5^post21, InnerIndex6^0'=InnerIndex6^post21, Seed^0'=Seed^post21, (ret_RandomInteger17^0-ret_RandomInteger17^post21 == 0 /\ -OuterIndex8^post21+OuterIndex8^0 == 0 /\ OuterIndex5^post21 == 0 /\ Outer13^0-Outer13^post21 == 0 /\ Inner14^0-Inner14^post21 == 0 /\ Index15^0-Index15^post21 == 0 /\ ret_RandomInteger16^0-ret_RandomInteger16^post21 == 0 /\ InnerIndex9^0-InnerIndex9^post21 == 0 /\ Seed^post21 == 0 /\ -InnerIndex6^post21+InnerIndex6^0 == 0), cost: 1
New rule:
l15 -> l0 : OuterIndex5^0'=0, Seed^0'=0, TRUE, cost: 1

Applied preprocessing
Original rule:
l16 -> l15 : Outer13^0'=Outer13^post22, Inner14^0'=Inner14^post22, ret_RandomInteger17^0'=ret_RandomInteger17^post22, OuterIndex8^0'=OuterIndex8^post22, InnerIndex9^0'=InnerIndex9^post22, Index15^0'=Index15^post22, ret_RandomInteger16^0'=ret_RandomInteger16^post22, OuterIndex5^0'=OuterIndex5^post22, InnerIndex6^0'=InnerIndex6^post22, Seed^0'=Seed^post22, (Index15^0-Index15^post22 == 0 /\ -InnerIndex9^post22+InnerIndex9^0 == 0 /\ ret_RandomInteger16^0-ret_RandomInteger16^post22 == 0 /\ -OuterIndex5^post22+OuterIndex5^0 == 0 /\ -InnerIndex6^post22+InnerIndex6^0 == 0 /\ -OuterIndex8^post22+OuterIndex8^0 == 0 /\ -Seed^post22+Seed^0 == 0 /\ Outer13^0-Outer13^post22 == 0 /\ ret_RandomInteger17^0-ret_RandomInteger17^post22 == 0 /\ Inner14^0-Inner14^post22 == 0), cost: 1
New rule:
l16 -> l15 : TRUE, cost: 1

Simplified rules
Start location: l16
  23: l0 -> l1 : TRUE, cost: 1
  41: l1 -> l4 : OuterIndex8^0'=0, -20+OuterIndex5^0 >= 0, cost: 1
  42: l1 -> l2 : InnerIndex6^0'=0, -19+OuterIndex5^0 <= 0, cost: 1
  24: l2 -> l3 : TRUE, cost: 1
  39: l3 -> l0 : OuterIndex5^0'=1+OuterIndex5^0, -20+InnerIndex6^0 >= 0, cost: 1
  40: l3 -> l2 : ret_RandomInteger16^0'=Seed^post18, InnerIndex6^0'=1+InnerIndex6^0, Seed^0'=Seed^post18, -19+InnerIndex6^0 <= 0, cost: 1
  25: l4 -> l5 : TRUE, cost: 1
  35: l5 -> l10 : Outer13^0'=0, -20+OuterIndex8^0 >= 0, cost: 1
  36: l5 -> l13 : InnerIndex9^0'=0, -19+OuterIndex8^0 <= 0, cost: 1
  26: l6 -> l7 : Inner14^0'=1+Inner14^0, -20+Index15^0 >= 0, cost: 1
  27: l6 -> l8 : Index15^0'=1+Index15^0, -19+Index15^0 <= 0, cost: 1
  37: l7 -> l9 : TRUE, cost: 1
  38: l8 -> l6 : TRUE, cost: 1
  28: l9 -> l10 : Outer13^0'=1+Outer13^0, -20+Inner14^0 >= 0, cost: 1
  29: l9 -> l8 : Index15^0'=0, -19+Inner14^0 <= 0, cost: 1
  32: l10 -> l11 : TRUE, cost: 1
  30: l11 -> l7 : Inner14^0'=0, -19+Outer13^0 <= 0, cost: 1
  31: l13 -> l14 : TRUE, cost: 1
  33: l14 -> l4 : OuterIndex8^0'=1+OuterIndex8^0, -20+InnerIndex9^0 >= 0, cost: 1
  34: l14 -> l13 : ret_RandomInteger17^0'=Seed^post12, InnerIndex9^0'=1+InnerIndex9^0, Seed^0'=Seed^post12, -19+InnerIndex9^0 <= 0, cost: 1
  43: l15 -> l0 : OuterIndex5^0'=0, Seed^0'=0, TRUE, cost: 1
  44: l16 -> l15 : TRUE, cost: 1


Eliminating location l15 by chaining:

Applied chaining
First rule:
l16 -> l15 : TRUE, cost: 1
Second rule:
l15 -> l0 : OuterIndex5^0'=0, Seed^0'=0, TRUE, cost: 1
New rule:
l16 -> l0 : OuterIndex5^0'=0, Seed^0'=0, TRUE, cost: 2

Applied deletion
Removed the following rules: 43 44

Eliminating location l11 by chaining:

Applied chaining
First rule:
l10 -> l11 : TRUE, cost: 1
Second rule:
l11 -> l7 : Inner14^0'=0, -19+Outer13^0 <= 0, cost: 1
New rule:
l10 -> l7 : Inner14^0'=0, -19+Outer13^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 30 32

Eliminated locations on linear paths
Start location: l16
  23: l0 -> l1 : TRUE, cost: 1
  41: l1 -> l4 : OuterIndex8^0'=0, -20+OuterIndex5^0 >= 0, cost: 1
  42: l1 -> l2 : InnerIndex6^0'=0, -19+OuterIndex5^0 <= 0, cost: 1
  24: l2 -> l3 : TRUE, cost: 1
  39: l3 -> l0 : OuterIndex5^0'=1+OuterIndex5^0, -20+InnerIndex6^0 >= 0, cost: 1
  40: l3 -> l2 : ret_RandomInteger16^0'=Seed^post18, InnerIndex6^0'=1+InnerIndex6^0, Seed^0'=Seed^post18, -19+InnerIndex6^0 <= 0, cost: 1
  25: l4 -> l5 : TRUE, cost: 1
  35: l5 -> l10 : Outer13^0'=0, -20+OuterIndex8^0 >= 0, cost: 1
  36: l5 -> l13 : InnerIndex9^0'=0, -19+OuterIndex8^0 <= 0, cost: 1
  26: l6 -> l7 : Inner14^0'=1+Inner14^0, -20+Index15^0 >= 0, cost: 1
  27: l6 -> l8 : Index15^0'=1+Index15^0, -19+Index15^0 <= 0, cost: 1
  37: l7 -> l9 : TRUE, cost: 1
  38: l8 -> l6 : TRUE, cost: 1
  28: l9 -> l10 : Outer13^0'=1+Outer13^0, -20+Inner14^0 >= 0, cost: 1
  29: l9 -> l8 : Index15^0'=0, -19+Inner14^0 <= 0, cost: 1
  46: l10 -> l7 : Inner14^0'=0, -19+Outer13^0 <= 0, cost: 2
  31: l13 -> l14 : TRUE, cost: 1
  33: l14 -> l4 : OuterIndex8^0'=1+OuterIndex8^0, -20+InnerIndex9^0 >= 0, cost: 1
  34: l14 -> l13 : ret_RandomInteger17^0'=Seed^post12, InnerIndex9^0'=1+InnerIndex9^0, Seed^0'=Seed^post12, -19+InnerIndex9^0 <= 0, cost: 1
  45: l16 -> l0 : OuterIndex5^0'=0, Seed^0'=0, TRUE, cost: 2


Eliminating location l1 by chaining:

Applied chaining
First rule:
l0 -> l1 : TRUE, cost: 1
Second rule:
l1 -> l4 : OuterIndex8^0'=0, -20+OuterIndex5^0 >= 0, cost: 1
New rule:
l0 -> l4 : OuterIndex8^0'=0, -20+OuterIndex5^0 >= 0, cost: 2

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

Applied deletion
Removed the following rules: 23 41 42

Eliminating location l3 by chaining:

Applied chaining
First rule:
l2 -> l3 : TRUE, cost: 1
Second rule:
l3 -> l0 : OuterIndex5^0'=1+OuterIndex5^0, -20+InnerIndex6^0 >= 0, cost: 1
New rule:
l2 -> l0 : OuterIndex5^0'=1+OuterIndex5^0, -20+InnerIndex6^0 >= 0, cost: 2

Applied chaining
First rule:
l2 -> l3 : TRUE, cost: 1
Second rule:
l3 -> l2 : ret_RandomInteger16^0'=Seed^post18, InnerIndex6^0'=1+InnerIndex6^0, Seed^0'=Seed^post18, -19+InnerIndex6^0 <= 0, cost: 1
New rule:
l2 -> l2 : ret_RandomInteger16^0'=Seed^post18, InnerIndex6^0'=1+InnerIndex6^0, Seed^0'=Seed^post18, -19+InnerIndex6^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 24 39 40

Eliminating location l5 by chaining:

Applied chaining
First rule:
l4 -> l5 : TRUE, cost: 1
Second rule:
l5 -> l10 : Outer13^0'=0, -20+OuterIndex8^0 >= 0, cost: 1
New rule:
l4 -> l10 : Outer13^0'=0, -20+OuterIndex8^0 >= 0, cost: 2

Applied chaining
First rule:
l4 -> l5 : TRUE, cost: 1
Second rule:
l5 -> l13 : InnerIndex9^0'=0, -19+OuterIndex8^0 <= 0, cost: 1
New rule:
l4 -> l13 : InnerIndex9^0'=0, -19+OuterIndex8^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 25 35 36

Eliminating location l9 by chaining:

Applied chaining
First rule:
l7 -> l9 : TRUE, cost: 1
Second rule:
l9 -> l10 : Outer13^0'=1+Outer13^0, -20+Inner14^0 >= 0, cost: 1
New rule:
l7 -> l10 : Outer13^0'=1+Outer13^0, -20+Inner14^0 >= 0, cost: 2

Applied chaining
First rule:
l7 -> l9 : TRUE, cost: 1
Second rule:
l9 -> l8 : Index15^0'=0, -19+Inner14^0 <= 0, cost: 1
New rule:
l7 -> l8 : Index15^0'=0, -19+Inner14^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 28 29 37

Eliminating location l6 by chaining:

Applied chaining
First rule:
l8 -> l6 : TRUE, cost: 1
Second rule:
l6 -> l7 : Inner14^0'=1+Inner14^0, -20+Index15^0 >= 0, cost: 1
New rule:
l8 -> l7 : Inner14^0'=1+Inner14^0, -20+Index15^0 >= 0, cost: 2

Applied chaining
First rule:
l8 -> l6 : TRUE, cost: 1
Second rule:
l6 -> l8 : Index15^0'=1+Index15^0, -19+Index15^0 <= 0, cost: 1
New rule:
l8 -> l8 : Index15^0'=1+Index15^0, -19+Index15^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 26 27 38

Eliminating location l14 by chaining:

Applied chaining
First rule:
l13 -> l14 : TRUE, cost: 1
Second rule:
l14 -> l4 : OuterIndex8^0'=1+OuterIndex8^0, -20+InnerIndex9^0 >= 0, cost: 1
New rule:
l13 -> l4 : OuterIndex8^0'=1+OuterIndex8^0, -20+InnerIndex9^0 >= 0, cost: 2

Applied chaining
First rule:
l13 -> l14 : TRUE, cost: 1
Second rule:
l14 -> l13 : ret_RandomInteger17^0'=Seed^post12, InnerIndex9^0'=1+InnerIndex9^0, Seed^0'=Seed^post12, -19+InnerIndex9^0 <= 0, cost: 1
New rule:
l13 -> l13 : ret_RandomInteger17^0'=Seed^post12, InnerIndex9^0'=1+InnerIndex9^0, Seed^0'=Seed^post12, -19+InnerIndex9^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 31 33 34

Eliminated locations on tree-shaped paths
Start location: l16
  47: l0 -> l4 : OuterIndex8^0'=0, -20+OuterIndex5^0 >= 0, cost: 2
  48: l0 -> l2 : InnerIndex6^0'=0, -19+OuterIndex5^0 <= 0, cost: 2
  49: l2 -> l0 : OuterIndex5^0'=1+OuterIndex5^0, -20+InnerIndex6^0 >= 0, cost: 2
  50: l2 -> l2 : ret_RandomInteger16^0'=Seed^post18, InnerIndex6^0'=1+InnerIndex6^0, Seed^0'=Seed^post18, -19+InnerIndex6^0 <= 0, cost: 2
  51: l4 -> l10 : Outer13^0'=0, -20+OuterIndex8^0 >= 0, cost: 2
  52: l4 -> l13 : InnerIndex9^0'=0, -19+OuterIndex8^0 <= 0, cost: 2
  53: l7 -> l10 : Outer13^0'=1+Outer13^0, -20+Inner14^0 >= 0, cost: 2
  54: l7 -> l8 : Index15^0'=0, -19+Inner14^0 <= 0, cost: 2
  55: l8 -> l7 : Inner14^0'=1+Inner14^0, -20+Index15^0 >= 0, cost: 2
  56: l8 -> l8 : Index15^0'=1+Index15^0, -19+Index15^0 <= 0, cost: 2
  46: l10 -> l7 : Inner14^0'=0, -19+Outer13^0 <= 0, cost: 2
  57: l13 -> l4 : OuterIndex8^0'=1+OuterIndex8^0, -20+InnerIndex9^0 >= 0, cost: 2
  58: l13 -> l13 : ret_RandomInteger17^0'=Seed^post12, InnerIndex9^0'=1+InnerIndex9^0, Seed^0'=Seed^post12, -19+InnerIndex9^0 <= 0, cost: 2
  45: l16 -> l0 : OuterIndex5^0'=0, Seed^0'=0, TRUE, cost: 2


Applied acceleration
Original rule:
l2 -> l2 : ret_RandomInteger16^0'=Seed^post18, InnerIndex6^0'=1+InnerIndex6^0, Seed^0'=Seed^post18, -19+InnerIndex6^0 <= 0, cost: 2
New rule:
l2 -> l2 : ret_RandomInteger16^0'=Seed^post18, InnerIndex6^0'=n+InnerIndex6^0, Seed^0'=Seed^post18, (20-n-InnerIndex6^0 >= 0 /\ -1+n >= 0), cost: 2*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_kfHHiE.txt

Applied instantiation
Original rule:
l2 -> l2 : ret_RandomInteger16^0'=Seed^post18, InnerIndex6^0'=n+InnerIndex6^0, Seed^0'=Seed^post18, (20-n-InnerIndex6^0 >= 0 /\ -1+n >= 0), cost: 2*n
New rule:
l2 -> l2 : ret_RandomInteger16^0'=Seed^post18, InnerIndex6^0'=20, Seed^0'=Seed^post18, (0 >= 0 /\ 19-InnerIndex6^0 >= 0), cost: 40-2*InnerIndex6^0

Applied simplification
Original rule:
l2 -> l2 : ret_RandomInteger16^0'=Seed^post18, InnerIndex6^0'=20, Seed^0'=Seed^post18, (0 >= 0 /\ 19-InnerIndex6^0 >= 0), cost: 40-2*InnerIndex6^0
New rule:
l2 -> l2 : ret_RandomInteger16^0'=Seed^post18, InnerIndex6^0'=20, Seed^0'=Seed^post18, -19+InnerIndex6^0 <= 0, cost: 40-2*InnerIndex6^0

Applied deletion
Removed the following rules: 50

Applied acceleration
Original rule:
l8 -> l8 : Index15^0'=1+Index15^0, -19+Index15^0 <= 0, cost: 2
New rule:
l8 -> l8 : Index15^0'=n0+Index15^0, (20-n0-Index15^0 >= 0 /\ n0 >= 0), cost: 2*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_FMJada.txt

Applied instantiation
Original rule:
l8 -> l8 : Index15^0'=n0+Index15^0, (20-n0-Index15^0 >= 0 /\ n0 >= 0), cost: 2*n0
New rule:
l8 -> l8 : Index15^0'=20, (0 >= 0 /\ 20-Index15^0 >= 0), cost: 40-2*Index15^0

Applied simplification
Original rule:
l8 -> l8 : Index15^0'=20, (0 >= 0 /\ 20-Index15^0 >= 0), cost: 40-2*Index15^0
New rule:
l8 -> l8 : Index15^0'=20, -20+Index15^0 <= 0, cost: 40-2*Index15^0

Applied deletion
Removed the following rules: 56

Applied acceleration
Original rule:
l13 -> l13 : ret_RandomInteger17^0'=Seed^post12, InnerIndex9^0'=1+InnerIndex9^0, Seed^0'=Seed^post12, -19+InnerIndex9^0 <= 0, cost: 2
New rule:
l13 -> l13 : ret_RandomInteger17^0'=Seed^post12, InnerIndex9^0'=InnerIndex9^0+n1, Seed^0'=Seed^post12, (-1+n1 >= 0 /\ 20-InnerIndex9^0-n1 >= 0), cost: 2*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ljekjJ.txt

Applied instantiation
Original rule:
l13 -> l13 : ret_RandomInteger17^0'=Seed^post12, InnerIndex9^0'=InnerIndex9^0+n1, Seed^0'=Seed^post12, (-1+n1 >= 0 /\ 20-InnerIndex9^0-n1 >= 0), cost: 2*n1
New rule:
l13 -> l13 : ret_RandomInteger17^0'=Seed^post12, InnerIndex9^0'=20, Seed^0'=Seed^post12, (0 >= 0 /\ 19-InnerIndex9^0 >= 0), cost: 40-2*InnerIndex9^0

Applied simplification
Original rule:
l13 -> l13 : ret_RandomInteger17^0'=Seed^post12, InnerIndex9^0'=20, Seed^0'=Seed^post12, (0 >= 0 /\ 19-InnerIndex9^0 >= 0), cost: 40-2*InnerIndex9^0
New rule:
l13 -> l13 : ret_RandomInteger17^0'=Seed^post12, InnerIndex9^0'=20, Seed^0'=Seed^post12, -19+InnerIndex9^0 <= 0, cost: 40-2*InnerIndex9^0

Applied deletion
Removed the following rules: 58

Accelerated simple loops
Start location: l16
  47: l0 -> l4 : OuterIndex8^0'=0, -20+OuterIndex5^0 >= 0, cost: 2
  48: l0 -> l2 : InnerIndex6^0'=0, -19+OuterIndex5^0 <= 0, cost: 2
  49: l2 -> l0 : OuterIndex5^0'=1+OuterIndex5^0, -20+InnerIndex6^0 >= 0, cost: 2
  60: l2 -> l2 : ret_RandomInteger16^0'=Seed^post18, InnerIndex6^0'=20, Seed^0'=Seed^post18, -19+InnerIndex6^0 <= 0, cost: 40-2*InnerIndex6^0
  51: l4 -> l10 : Outer13^0'=0, -20+OuterIndex8^0 >= 0, cost: 2
  52: l4 -> l13 : InnerIndex9^0'=0, -19+OuterIndex8^0 <= 0, cost: 2
  53: l7 -> l10 : Outer13^0'=1+Outer13^0, -20+Inner14^0 >= 0, cost: 2
  54: l7 -> l8 : Index15^0'=0, -19+Inner14^0 <= 0, cost: 2
  55: l8 -> l7 : Inner14^0'=1+Inner14^0, -20+Index15^0 >= 0, cost: 2
  62: l8 -> l8 : Index15^0'=20, -20+Index15^0 <= 0, cost: 40-2*Index15^0
  46: l10 -> l7 : Inner14^0'=0, -19+Outer13^0 <= 0, cost: 2
  57: l13 -> l4 : OuterIndex8^0'=1+OuterIndex8^0, -20+InnerIndex9^0 >= 0, cost: 2
  64: l13 -> l13 : ret_RandomInteger17^0'=Seed^post12, InnerIndex9^0'=20, Seed^0'=Seed^post12, -19+InnerIndex9^0 <= 0, cost: 40-2*InnerIndex9^0
  45: l16 -> l0 : OuterIndex5^0'=0, Seed^0'=0, TRUE, cost: 2


Applied chaining
First rule:
l0 -> l2 : InnerIndex6^0'=0, -19+OuterIndex5^0 <= 0, cost: 2
Second rule:
l2 -> l2 : ret_RandomInteger16^0'=Seed^post18, InnerIndex6^0'=20, Seed^0'=Seed^post18, -19+InnerIndex6^0 <= 0, cost: 40-2*InnerIndex6^0
New rule:
l0 -> l2 : ret_RandomInteger16^0'=Seed^post18, InnerIndex6^0'=20, Seed^0'=Seed^post18, -19+OuterIndex5^0 <= 0, cost: 42

Applied deletion
Removed the following rules: 60

Applied chaining
First rule:
l7 -> l8 : Index15^0'=0, -19+Inner14^0 <= 0, cost: 2
Second rule:
l8 -> l8 : Index15^0'=20, -20+Index15^0 <= 0, cost: 40-2*Index15^0
New rule:
l7 -> l8 : Index15^0'=20, -19+Inner14^0 <= 0, cost: 42

Applied deletion
Removed the following rules: 62

Applied chaining
First rule:
l4 -> l13 : InnerIndex9^0'=0, -19+OuterIndex8^0 <= 0, cost: 2
Second rule:
l13 -> l13 : ret_RandomInteger17^0'=Seed^post12, InnerIndex9^0'=20, Seed^0'=Seed^post12, -19+InnerIndex9^0 <= 0, cost: 40-2*InnerIndex9^0
New rule:
l4 -> l13 : ret_RandomInteger17^0'=Seed^post12, InnerIndex9^0'=20, Seed^0'=Seed^post12, -19+OuterIndex8^0 <= 0, cost: 42

Applied deletion
Removed the following rules: 64

Chained accelerated rules with incoming rules
Start location: l16
  47: l0 -> l4 : OuterIndex8^0'=0, -20+OuterIndex5^0 >= 0, cost: 2
  48: l0 -> l2 : InnerIndex6^0'=0, -19+OuterIndex5^0 <= 0, cost: 2
  65: l0 -> l2 : ret_RandomInteger16^0'=Seed^post18, InnerIndex6^0'=20, Seed^0'=Seed^post18, -19+OuterIndex5^0 <= 0, cost: 42
  49: l2 -> l0 : OuterIndex5^0'=1+OuterIndex5^0, -20+InnerIndex6^0 >= 0, cost: 2
  51: l4 -> l10 : Outer13^0'=0, -20+OuterIndex8^0 >= 0, cost: 2
  52: l4 -> l13 : InnerIndex9^0'=0, -19+OuterIndex8^0 <= 0, cost: 2
  67: l4 -> l13 : ret_RandomInteger17^0'=Seed^post12, InnerIndex9^0'=20, Seed^0'=Seed^post12, -19+OuterIndex8^0 <= 0, cost: 42
  53: l7 -> l10 : Outer13^0'=1+Outer13^0, -20+Inner14^0 >= 0, cost: 2
  54: l7 -> l8 : Index15^0'=0, -19+Inner14^0 <= 0, cost: 2
  66: l7 -> l8 : Index15^0'=20, -19+Inner14^0 <= 0, cost: 42
  55: l8 -> l7 : Inner14^0'=1+Inner14^0, -20+Index15^0 >= 0, cost: 2
  46: l10 -> l7 : Inner14^0'=0, -19+Outer13^0 <= 0, cost: 2
  57: l13 -> l4 : OuterIndex8^0'=1+OuterIndex8^0, -20+InnerIndex9^0 >= 0, cost: 2
  45: l16 -> l0 : OuterIndex5^0'=0, Seed^0'=0, TRUE, cost: 2


Eliminating location l2 by chaining:

Applied chaining
First rule:
l0 -> l2 : ret_RandomInteger16^0'=Seed^post18, InnerIndex6^0'=20, Seed^0'=Seed^post18, -19+OuterIndex5^0 <= 0, cost: 42
Second rule:
l2 -> l0 : OuterIndex5^0'=1+OuterIndex5^0, -20+InnerIndex6^0 >= 0, cost: 2
New rule:
l0 -> l0 : ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=1+OuterIndex5^0, InnerIndex6^0'=20, Seed^0'=Seed^post18, (0 >= 0 /\ -19+OuterIndex5^0 <= 0), cost: 44

Applied simplification
Original rule:
l0 -> l0 : ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=1+OuterIndex5^0, InnerIndex6^0'=20, Seed^0'=Seed^post18, (0 >= 0 /\ -19+OuterIndex5^0 <= 0), cost: 44
New rule:
l0 -> l0 : ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=1+OuterIndex5^0, InnerIndex6^0'=20, Seed^0'=Seed^post18, -19+OuterIndex5^0 <= 0, cost: 44

Applied deletion
Removed the following rules: 48 49 65

Eliminating location l13 by chaining:

Applied chaining
First rule:
l4 -> l13 : ret_RandomInteger17^0'=Seed^post12, InnerIndex9^0'=20, Seed^0'=Seed^post12, -19+OuterIndex8^0 <= 0, cost: 42
Second rule:
l13 -> l4 : OuterIndex8^0'=1+OuterIndex8^0, -20+InnerIndex9^0 >= 0, cost: 2
New rule:
l4 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=1+OuterIndex8^0, InnerIndex9^0'=20, Seed^0'=Seed^post12, (0 >= 0 /\ -19+OuterIndex8^0 <= 0), cost: 44

Applied simplification
Original rule:
l4 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=1+OuterIndex8^0, InnerIndex9^0'=20, Seed^0'=Seed^post12, (0 >= 0 /\ -19+OuterIndex8^0 <= 0), cost: 44
New rule:
l4 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=1+OuterIndex8^0, InnerIndex9^0'=20, Seed^0'=Seed^post12, -19+OuterIndex8^0 <= 0, cost: 44

Applied deletion
Removed the following rules: 52 57 67

Eliminating location l8 by chaining:

Applied chaining
First rule:
l7 -> l8 : Index15^0'=20, -19+Inner14^0 <= 0, cost: 42
Second rule:
l8 -> l7 : Inner14^0'=1+Inner14^0, -20+Index15^0 >= 0, cost: 2
New rule:
l7 -> l7 : Inner14^0'=1+Inner14^0, Index15^0'=20, (0 >= 0 /\ -19+Inner14^0 <= 0), cost: 44

Applied simplification
Original rule:
l7 -> l7 : Inner14^0'=1+Inner14^0, Index15^0'=20, (0 >= 0 /\ -19+Inner14^0 <= 0), cost: 44
New rule:
l7 -> l7 : Inner14^0'=1+Inner14^0, Index15^0'=20, -19+Inner14^0 <= 0, cost: 44

Applied deletion
Removed the following rules: 54 55 66

Eliminated locations on tree-shaped paths
Start location: l16
  47: l0 -> l4 : OuterIndex8^0'=0, -20+OuterIndex5^0 >= 0, cost: 2
  68: l0 -> l0 : ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=1+OuterIndex5^0, InnerIndex6^0'=20, Seed^0'=Seed^post18, -19+OuterIndex5^0 <= 0, cost: 44
  51: l4 -> l10 : Outer13^0'=0, -20+OuterIndex8^0 >= 0, cost: 2
  69: l4 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=1+OuterIndex8^0, InnerIndex9^0'=20, Seed^0'=Seed^post12, -19+OuterIndex8^0 <= 0, cost: 44
  53: l7 -> l10 : Outer13^0'=1+Outer13^0, -20+Inner14^0 >= 0, cost: 2
  70: l7 -> l7 : Inner14^0'=1+Inner14^0, Index15^0'=20, -19+Inner14^0 <= 0, cost: 44
  46: l10 -> l7 : Inner14^0'=0, -19+Outer13^0 <= 0, cost: 2
  45: l16 -> l0 : OuterIndex5^0'=0, Seed^0'=0, TRUE, cost: 2


Applied acceleration
Original rule:
l0 -> l0 : ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=1+OuterIndex5^0, InnerIndex6^0'=20, Seed^0'=Seed^post18, -19+OuterIndex5^0 <= 0, cost: 44
New rule:
l0 -> l0 : ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=n2+OuterIndex5^0, InnerIndex6^0'=20, Seed^0'=Seed^post18, (20-n2-OuterIndex5^0 >= 0 /\ -1+n2 >= 0), cost: 44*n2
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ClPfhg.txt

Applied instantiation
Original rule:
l0 -> l0 : ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=n2+OuterIndex5^0, InnerIndex6^0'=20, Seed^0'=Seed^post18, (20-n2-OuterIndex5^0 >= 0 /\ -1+n2 >= 0), cost: 44*n2
New rule:
l0 -> l0 : ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=20, InnerIndex6^0'=20, Seed^0'=Seed^post18, (0 >= 0 /\ 19-OuterIndex5^0 >= 0), cost: 880-44*OuterIndex5^0

Applied simplification
Original rule:
l0 -> l0 : ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=20, InnerIndex6^0'=20, Seed^0'=Seed^post18, (0 >= 0 /\ 19-OuterIndex5^0 >= 0), cost: 880-44*OuterIndex5^0
New rule:
l0 -> l0 : ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=20, InnerIndex6^0'=20, Seed^0'=Seed^post18, -19+OuterIndex5^0 <= 0, cost: 880-44*OuterIndex5^0

Applied deletion
Removed the following rules: 68

Applied acceleration
Original rule:
l4 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=1+OuterIndex8^0, InnerIndex9^0'=20, Seed^0'=Seed^post12, -19+OuterIndex8^0 <= 0, cost: 44
New rule:
l4 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=OuterIndex8^0+n3, InnerIndex9^0'=20, Seed^0'=Seed^post12, (-1+n3 >= 0 /\ 20-OuterIndex8^0-n3 >= 0), cost: 44*n3
Sub-proof via acceration calculus written to file:///tmp/tmpnam_gBIcjO.txt

Applied instantiation
Original rule:
l4 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=OuterIndex8^0+n3, InnerIndex9^0'=20, Seed^0'=Seed^post12, (-1+n3 >= 0 /\ 20-OuterIndex8^0-n3 >= 0), cost: 44*n3
New rule:
l4 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=20, InnerIndex9^0'=20, Seed^0'=Seed^post12, (0 >= 0 /\ 19-OuterIndex8^0 >= 0), cost: 880-44*OuterIndex8^0

Applied simplification
Original rule:
l4 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=20, InnerIndex9^0'=20, Seed^0'=Seed^post12, (0 >= 0 /\ 19-OuterIndex8^0 >= 0), cost: 880-44*OuterIndex8^0
New rule:
l4 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=20, InnerIndex9^0'=20, Seed^0'=Seed^post12, -19+OuterIndex8^0 <= 0, cost: 880-44*OuterIndex8^0

Applied deletion
Removed the following rules: 69

Applied acceleration
Original rule:
l7 -> l7 : Inner14^0'=1+Inner14^0, Index15^0'=20, -19+Inner14^0 <= 0, cost: 44
New rule:
l7 -> l7 : Inner14^0'=Inner14^0+n4, Index15^0'=20, (-1+n4 >= 0 /\ 20-Inner14^0-n4 >= 0), cost: 44*n4
Sub-proof via acceration calculus written to file:///tmp/tmpnam_iGaPGo.txt

Applied instantiation
Original rule:
l7 -> l7 : Inner14^0'=Inner14^0+n4, Index15^0'=20, (-1+n4 >= 0 /\ 20-Inner14^0-n4 >= 0), cost: 44*n4
New rule:
l7 -> l7 : Inner14^0'=20, Index15^0'=20, (0 >= 0 /\ 19-Inner14^0 >= 0), cost: 880-44*Inner14^0

Applied simplification
Original rule:
l7 -> l7 : Inner14^0'=20, Index15^0'=20, (0 >= 0 /\ 19-Inner14^0 >= 0), cost: 880-44*Inner14^0
New rule:
l7 -> l7 : Inner14^0'=20, Index15^0'=20, -19+Inner14^0 <= 0, cost: 880-44*Inner14^0

Applied deletion
Removed the following rules: 70

Accelerated simple loops
Start location: l16
  47: l0 -> l4 : OuterIndex8^0'=0, -20+OuterIndex5^0 >= 0, cost: 2
  72: l0 -> l0 : ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=20, InnerIndex6^0'=20, Seed^0'=Seed^post18, -19+OuterIndex5^0 <= 0, cost: 880-44*OuterIndex5^0
  51: l4 -> l10 : Outer13^0'=0, -20+OuterIndex8^0 >= 0, cost: 2
  74: l4 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=20, InnerIndex9^0'=20, Seed^0'=Seed^post12, -19+OuterIndex8^0 <= 0, cost: 880-44*OuterIndex8^0
  53: l7 -> l10 : Outer13^0'=1+Outer13^0, -20+Inner14^0 >= 0, cost: 2
  76: l7 -> l7 : Inner14^0'=20, Index15^0'=20, -19+Inner14^0 <= 0, cost: 880-44*Inner14^0
  46: l10 -> l7 : Inner14^0'=0, -19+Outer13^0 <= 0, cost: 2
  45: l16 -> l0 : OuterIndex5^0'=0, Seed^0'=0, TRUE, cost: 2


Applied chaining
First rule:
l16 -> l0 : OuterIndex5^0'=0, Seed^0'=0, TRUE, cost: 2
Second rule:
l0 -> l0 : ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=20, InnerIndex6^0'=20, Seed^0'=Seed^post18, -19+OuterIndex5^0 <= 0, cost: 880-44*OuterIndex5^0
New rule:
l16 -> l0 : ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=20, InnerIndex6^0'=20, Seed^0'=Seed^post18, -19 <= 0, cost: 882

Applied deletion
Removed the following rules: 72

Applied chaining
First rule:
l0 -> l4 : OuterIndex8^0'=0, -20+OuterIndex5^0 >= 0, cost: 2
Second rule:
l4 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=20, InnerIndex9^0'=20, Seed^0'=Seed^post12, -19+OuterIndex8^0 <= 0, cost: 880-44*OuterIndex8^0
New rule:
l0 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=20, InnerIndex9^0'=20, Seed^0'=Seed^post12, -20+OuterIndex5^0 >= 0, cost: 882

Applied deletion
Removed the following rules: 74

Applied chaining
First rule:
l10 -> l7 : Inner14^0'=0, -19+Outer13^0 <= 0, cost: 2
Second rule:
l7 -> l7 : Inner14^0'=20, Index15^0'=20, -19+Inner14^0 <= 0, cost: 880-44*Inner14^0
New rule:
l10 -> l7 : Inner14^0'=20, Index15^0'=20, -19+Outer13^0 <= 0, cost: 882

Applied deletion
Removed the following rules: 76

Chained accelerated rules with incoming rules
Start location: l16
  47: l0 -> l4 : OuterIndex8^0'=0, -20+OuterIndex5^0 >= 0, cost: 2
  78: l0 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=20, InnerIndex9^0'=20, Seed^0'=Seed^post12, -20+OuterIndex5^0 >= 0, cost: 882
  51: l4 -> l10 : Outer13^0'=0, -20+OuterIndex8^0 >= 0, cost: 2
  53: l7 -> l10 : Outer13^0'=1+Outer13^0, -20+Inner14^0 >= 0, cost: 2
  46: l10 -> l7 : Inner14^0'=0, -19+Outer13^0 <= 0, cost: 2
  79: l10 -> l7 : Inner14^0'=20, Index15^0'=20, -19+Outer13^0 <= 0, cost: 882
  45: l16 -> l0 : OuterIndex5^0'=0, Seed^0'=0, TRUE, cost: 2
  77: l16 -> l0 : ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=20, InnerIndex6^0'=20, Seed^0'=Seed^post18, -19 <= 0, cost: 882


Eliminating location l0 by chaining:

Applied chaining
First rule:
l16 -> l0 : ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=20, InnerIndex6^0'=20, Seed^0'=Seed^post18, -19 <= 0, cost: 882
Second rule:
l0 -> l4 : OuterIndex8^0'=0, -20+OuterIndex5^0 >= 0, cost: 2
New rule:
l16 -> l4 : OuterIndex8^0'=0, ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=20, InnerIndex6^0'=20, Seed^0'=Seed^post18, (0 >= 0 /\ -19 <= 0), cost: 884

Applied chaining
First rule:
l16 -> l0 : ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=20, InnerIndex6^0'=20, Seed^0'=Seed^post18, -19 <= 0, cost: 882
Second rule:
l0 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=20, InnerIndex9^0'=20, Seed^0'=Seed^post12, -20+OuterIndex5^0 >= 0, cost: 882
New rule:
l16 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=20, InnerIndex9^0'=20, ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=20, InnerIndex6^0'=20, Seed^0'=Seed^post12, (0 >= 0 /\ -19 <= 0), cost: 1764

Applied deletion
Removed the following rules: 45 47 77 78

Eliminating location l7 by chaining:

Applied chaining
First rule:
l10 -> l7 : Inner14^0'=20, Index15^0'=20, -19+Outer13^0 <= 0, cost: 882
Second rule:
l7 -> l10 : Outer13^0'=1+Outer13^0, -20+Inner14^0 >= 0, cost: 2
New rule:
l10 -> l10 : Outer13^0'=1+Outer13^0, Inner14^0'=20, Index15^0'=20, (0 >= 0 /\ -19+Outer13^0 <= 0), cost: 884

Applied simplification
Original rule:
l10 -> l10 : Outer13^0'=1+Outer13^0, Inner14^0'=20, Index15^0'=20, (0 >= 0 /\ -19+Outer13^0 <= 0), cost: 884
New rule:
l10 -> l10 : Outer13^0'=1+Outer13^0, Inner14^0'=20, Index15^0'=20, -19+Outer13^0 <= 0, cost: 884

Applied deletion
Removed the following rules: 46 53 79

Eliminated locations on tree-shaped paths
Start location: l16
  51: l4 -> l10 : Outer13^0'=0, -20+OuterIndex8^0 >= 0, cost: 2
  82: l10 -> l10 : Outer13^0'=1+Outer13^0, Inner14^0'=20, Index15^0'=20, -19+Outer13^0 <= 0, cost: 884
  80: l16 -> l4 : OuterIndex8^0'=0, ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=20, InnerIndex6^0'=20, Seed^0'=Seed^post18, (0 >= 0 /\ -19 <= 0), cost: 884
  81: l16 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=20, InnerIndex9^0'=20, ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=20, InnerIndex6^0'=20, Seed^0'=Seed^post12, (0 >= 0 /\ -19 <= 0), cost: 1764


Applied acceleration
Original rule:
l10 -> l10 : Outer13^0'=1+Outer13^0, Inner14^0'=20, Index15^0'=20, -19+Outer13^0 <= 0, cost: 884
New rule:
l10 -> l10 : Outer13^0'=Outer13^0+n5, Inner14^0'=20, Index15^0'=20, (20-Outer13^0-n5 >= 0 /\ -1+n5 >= 0), cost: 884*n5
Sub-proof via acceration calculus written to file:///tmp/tmpnam_DEpaOe.txt

Applied instantiation
Original rule:
l10 -> l10 : Outer13^0'=Outer13^0+n5, Inner14^0'=20, Index15^0'=20, (20-Outer13^0-n5 >= 0 /\ -1+n5 >= 0), cost: 884*n5
New rule:
l10 -> l10 : Outer13^0'=20, Inner14^0'=20, Index15^0'=20, (0 >= 0 /\ 19-Outer13^0 >= 0), cost: 17680-884*Outer13^0

Applied simplification
Original rule:
l10 -> l10 : Outer13^0'=20, Inner14^0'=20, Index15^0'=20, (0 >= 0 /\ 19-Outer13^0 >= 0), cost: 17680-884*Outer13^0
New rule:
l10 -> l10 : Outer13^0'=20, Inner14^0'=20, Index15^0'=20, -19+Outer13^0 <= 0, cost: 17680-884*Outer13^0

Applied deletion
Removed the following rules: 82

Accelerated simple loops
Start location: l16
  51: l4 -> l10 : Outer13^0'=0, -20+OuterIndex8^0 >= 0, cost: 2
  84: l10 -> l10 : Outer13^0'=20, Inner14^0'=20, Index15^0'=20, -19+Outer13^0 <= 0, cost: 17680-884*Outer13^0
  80: l16 -> l4 : OuterIndex8^0'=0, ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=20, InnerIndex6^0'=20, Seed^0'=Seed^post18, (0 >= 0 /\ -19 <= 0), cost: 884
  81: l16 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=20, InnerIndex9^0'=20, ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=20, InnerIndex6^0'=20, Seed^0'=Seed^post12, (0 >= 0 /\ -19 <= 0), cost: 1764


Applied chaining
First rule:
l4 -> l10 : Outer13^0'=0, -20+OuterIndex8^0 >= 0, cost: 2
Second rule:
l10 -> l10 : Outer13^0'=20, Inner14^0'=20, Index15^0'=20, -19+Outer13^0 <= 0, cost: 17680-884*Outer13^0
New rule:
l4 -> l10 : Outer13^0'=20, Inner14^0'=20, Index15^0'=20, -20+OuterIndex8^0 >= 0, cost: 17682

Applied deletion
Removed the following rules: 84

Chained accelerated rules with incoming rules
Start location: l16
  51: l4 -> l10 : Outer13^0'=0, -20+OuterIndex8^0 >= 0, cost: 2
  85: l4 -> l10 : Outer13^0'=20, Inner14^0'=20, Index15^0'=20, -20+OuterIndex8^0 >= 0, cost: 17682
  80: l16 -> l4 : OuterIndex8^0'=0, ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=20, InnerIndex6^0'=20, Seed^0'=Seed^post18, (0 >= 0 /\ -19 <= 0), cost: 884
  81: l16 -> l4 : ret_RandomInteger17^0'=Seed^post12, OuterIndex8^0'=20, InnerIndex9^0'=20, ret_RandomInteger16^0'=Seed^post18, OuterIndex5^0'=20, InnerIndex6^0'=20, Seed^0'=Seed^post12, (0 >= 0 /\ -19 <= 0), cost: 1764


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


Computing asymptotic complexity

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

Solved cost: 0
Rule cost:   0