LTS Termination Proof

by T2Cert

Input

• Initial Location: 12
• Transitions: (pre-variables and post-variables)

  0	0	1:		− ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0
  2	1	3:		0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − Inner10_0 + Inner10_post ≤ 0 ∧ 1 + Inner10_0 − Inner10_post ≤ 0 ∧ Inner10_0 − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_post ≤ 0 ∧ − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0
  4	2	5:		− ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0
  6	3	2:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − Pcnt13_0 + Pcnt13_post ≤ 0 ∧ 1 + Pcnt13_0 − Pcnt13_post ≤ 0 ∧ Pcnt13_0 − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_post ≤ 0 ∧ Ptotal11_0 − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_post ≤ 0 ∧ − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0
  6	4	2:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − Ncnt14_0 + Ncnt14_post ≤ 0 ∧ 1 + Ncnt14_0 − Ncnt14_post ≤ 0 ∧ Ncnt14_0 − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_post ≤ 0 ∧ Ntotal12_0 − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_post ≤ 0 ∧ − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0
  7	5	8:		0 ≤ 0 ∧ 0 ≤ 0 ∧ − Inner10_0 + ___const_10_0 ≤ 0 ∧ −1 − Outer9_0 + Outer9_post ≤ 0 ∧ 1 + Outer9_0 − Outer9_post ≤ 0 ∧ Outer9_0 − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_post ≤ 0 ∧ − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0
  7	6	6:		1 + Inner10_0 − ___const_10_0 ≤ 0 ∧ − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0
  9	7	10:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − Outer9_0 + ___const_10_0 ≤ 0 ∧ Postotal_post − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Ptotal11_0 ≤ 0 ∧ − Pcnt13_0 + Poscnt_post ≤ 0 ∧ Pcnt13_0 − Poscnt_post ≤ 0 ∧ Negtotal_post − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Ntotal12_0 ≤ 0 ∧ − Ncnt14_0 + Negcnt_post ≤ 0 ∧ Ncnt14_0 − Negcnt_post ≤ 0 ∧ StopTime3_post − ___const_1500_0 ≤ 0 ∧ − StopTime3_post + ___const_1500_0 ≤ 0 ∧ Negcnt_0 − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_post ≤ 0 ∧ Negtotal_0 − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_post ≤ 0 ∧ Poscnt_0 − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_post ≤ 0 ∧ Postotal_0 − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_post ≤ 0 ∧ StopTime3_0 − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_post ≤ 0 ∧ TotalTime4_0 − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_post ≤ 0 ∧ − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0
  9	8	3:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + Outer9_0 − ___const_10_0 ≤ 0 ∧ Inner10_post ≤ 0 ∧ − Inner10_post ≤ 0 ∧ Inner10_0 − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_post ≤ 0 ∧ − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0
  8	9	9:		− ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0
  3	10	7:		− ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0
  5	11	0:		0 ≤ 0 ∧ 0 ≤ 0 ∧ − InnerIndex7_0 + ___const_10_0 ≤ 0 ∧ −1 − OuterIndex6_0 + OuterIndex6_post ≤ 0 ∧ 1 + OuterIndex6_0 − OuterIndex6_post ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_post ≤ 0 ∧ − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0
  5	12	4:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + InnerIndex7_0 − ___const_10_0 ≤ 0 ∧ − Seed_post + ret_RandomInteger15_post ≤ 0 ∧ Seed_post − ret_RandomInteger15_post ≤ 0 ∧ −1 − InnerIndex7_0 + InnerIndex7_post ≤ 0 ∧ 1 + InnerIndex7_0 − InnerIndex7_post ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_post ≤ 0 ∧ Seed_0 − Seed_post ≤ 0 ∧ − Seed_0 + Seed_post ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_post ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0
  1	13	8:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − OuterIndex6_0 + ___const_10_0 ≤ 0 ∧ StartTime2_post − ___const_1000_0 ≤ 0 ∧ − StartTime2_post + ___const_1000_0 ≤ 0 ∧ Ptotal11_post ≤ 0 ∧ − Ptotal11_post ≤ 0 ∧ Ntotal12_post ≤ 0 ∧ − Ntotal12_post ≤ 0 ∧ Pcnt13_post ≤ 0 ∧ − Pcnt13_post ≤ 0 ∧ Ncnt14_post ≤ 0 ∧ − Ncnt14_post ≤ 0 ∧ Outer9_post ≤ 0 ∧ − Outer9_post ≤ 0 ∧ Ncnt14_0 − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_post ≤ 0 ∧ Ntotal12_0 − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_post ≤ 0 ∧ Outer9_0 − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_post ≤ 0 ∧ Pcnt13_0 − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_post ≤ 0 ∧ Ptotal11_0 − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_post ≤ 0 ∧ StartTime2_0 − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_post ≤ 0 ∧ − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0
  1	14	4:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + OuterIndex6_0 − ___const_10_0 ≤ 0 ∧ InnerIndex7_post ≤ 0 ∧ − InnerIndex7_post ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_post ≤ 0 ∧ − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0
  11	15	0:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ Seed_post ≤ 0 ∧ − Seed_post ≤ 0 ∧ OuterIndex6_post ≤ 0 ∧ − OuterIndex6_post ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_post ≤ 0 ∧ Seed_0 − Seed_post ≤ 0 ∧ − Seed_0 + Seed_post ≤ 0 ∧ − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0
  12	16	11:		− ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

2 Transition Removal

We remove transitions 7, 13, 15, 16 using the following ranking functions, which are bounded by −21.

3 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

0* 20 0: − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0

4 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

0 18 0_var_snapshot: − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0

5 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

3* 27 3: − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0

6 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

3 25 3_var_snapshot: − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0

7 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

4* 34 4: − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0

8 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

4 32 4_var_snapshot: − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0

9 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

8* 41 8: − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0

10 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

8 39 8_var_snapshot: − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − ___const_1500_0 + ___const_1500_0 ≤ 0 ∧ ___const_1500_0 − ___const_1500_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 ∧ − ___const_1000_0 + ___const_1000_0 ≤ 0 ∧ ___const_1000_0 − ___const_1000_0 ≤ 0 ∧ − TotalTime4_post + TotalTime4_post ≤ 0 ∧ TotalTime4_post − TotalTime4_post ≤ 0 ∧ − TotalTime4_0 + TotalTime4_0 ≤ 0 ∧ TotalTime4_0 − TotalTime4_0 ≤ 0 ∧ − StopTime3_post + StopTime3_post ≤ 0 ∧ StopTime3_post − StopTime3_post ≤ 0 ∧ − StopTime3_0 + StopTime3_0 ≤ 0 ∧ StopTime3_0 − StopTime3_0 ≤ 0 ∧ − StartTime2_post + StartTime2_post ≤ 0 ∧ StartTime2_post − StartTime2_post ≤ 0 ∧ − StartTime2_0 + StartTime2_0 ≤ 0 ∧ StartTime2_0 − StartTime2_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − Ptotal11_post + Ptotal11_post ≤ 0 ∧ Ptotal11_post − Ptotal11_post ≤ 0 ∧ − Ptotal11_0 + Ptotal11_0 ≤ 0 ∧ Ptotal11_0 − Ptotal11_0 ≤ 0 ∧ − Postotal_post + Postotal_post ≤ 0 ∧ Postotal_post − Postotal_post ≤ 0 ∧ − Postotal_0 + Postotal_0 ≤ 0 ∧ Postotal_0 − Postotal_0 ≤ 0 ∧ − Poscnt_post + Poscnt_post ≤ 0 ∧ Poscnt_post − Poscnt_post ≤ 0 ∧ − Poscnt_0 + Poscnt_0 ≤ 0 ∧ Poscnt_0 − Poscnt_0 ≤ 0 ∧ − Pcnt13_post + Pcnt13_post ≤ 0 ∧ Pcnt13_post − Pcnt13_post ≤ 0 ∧ − Pcnt13_0 + Pcnt13_0 ≤ 0 ∧ Pcnt13_0 − Pcnt13_0 ≤ 0 ∧ − OuterIndex6_post + OuterIndex6_post ≤ 0 ∧ OuterIndex6_post − OuterIndex6_post ≤ 0 ∧ − OuterIndex6_0 + OuterIndex6_0 ≤ 0 ∧ OuterIndex6_0 − OuterIndex6_0 ≤ 0 ∧ − Outer9_post + Outer9_post ≤ 0 ∧ Outer9_post − Outer9_post ≤ 0 ∧ − Outer9_0 + Outer9_0 ≤ 0 ∧ Outer9_0 − Outer9_0 ≤ 0 ∧ − Ntotal12_post + Ntotal12_post ≤ 0 ∧ Ntotal12_post − Ntotal12_post ≤ 0 ∧ − Ntotal12_0 + Ntotal12_0 ≤ 0 ∧ Ntotal12_0 − Ntotal12_0 ≤ 0 ∧ − Negtotal_post + Negtotal_post ≤ 0 ∧ Negtotal_post − Negtotal_post ≤ 0 ∧ − Negtotal_0 + Negtotal_0 ≤ 0 ∧ Negtotal_0 − Negtotal_0 ≤ 0 ∧ − Negcnt_post + Negcnt_post ≤ 0 ∧ Negcnt_post − Negcnt_post ≤ 0 ∧ − Negcnt_0 + Negcnt_0 ≤ 0 ∧ Negcnt_0 − Negcnt_0 ≤ 0 ∧ − Ncnt14_post + Ncnt14_post ≤ 0 ∧ Ncnt14_post − Ncnt14_post ≤ 0 ∧ − Ncnt14_0 + Ncnt14_0 ≤ 0 ∧ Ncnt14_0 − Ncnt14_0 ≤ 0 ∧ − InnerIndex7_post + InnerIndex7_post ≤ 0 ∧ InnerIndex7_post − InnerIndex7_post ≤ 0 ∧ − InnerIndex7_0 + InnerIndex7_0 ≤ 0 ∧ InnerIndex7_0 − InnerIndex7_0 ≤ 0 ∧ − Inner10_post + Inner10_post ≤ 0 ∧ Inner10_post − Inner10_post ≤ 0 ∧ − Inner10_0 + Inner10_0 ≤ 0 ∧ Inner10_0 − Inner10_0 ≤ 0

11 SCC Decomposition

We consider subproblems for each of the 2 SCC(s) of the program graph.

11.1 SCC Subproblem 1/2

Here we consider the SCC { 2, 3, 6, 7, 8, 9, 3_var_snapshot, 3*, 8_var_snapshot, 8* }.

11.1.1 Transition Removal

We remove transition 8 using the following ranking functions, which are bounded by 3.

11.1.2 Transition Removal

We remove transition 6 using the following ranking functions, which are bounded by 3.

11.1.3 Transition Removal

We remove transitions 25, 27, 39, 41, 3, 4, 5, 9, 10 using the following ranking functions, which are bounded by −5.

11.1.4 Transition Removal

We remove transition 1 using the following ranking functions, which are bounded by −1.

11.1.5 Splitting Cut-Point Transitions

We consider 2 subproblems corresponding to sets of cut-point transitions as follows.

11.1.5.1 Cut-Point Subproblem 1/2

11.1.5.1.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

11.1.5.2 Cut-Point Subproblem 2/2

11.1.5.2.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

11.2 SCC Subproblem 2/2

Here we consider the SCC { 0, 1, 4, 5, 0_var_snapshot, 0*, 4_var_snapshot, 4* }.

11.2.1 Transition Removal

We remove transition 14 using the following ranking functions, which are bounded by 7.

11.2.2 Transition Removal

We remove transition 12 using the following ranking functions, which are bounded by 3.

11.2.3 Transition Removal

We remove transitions 18, 20, 32, 34, 0, 2, 11 using the following ranking functions, which are bounded by −3.

11.2.4 Splitting Cut-Point Transitions

We consider 2 subproblems corresponding to sets of cut-point transitions as follows.

11.2.4.1 Cut-Point Subproblem 1/2

11.2.4.1.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

11.2.4.2 Cut-Point Subproblem 2/2

11.2.4.2.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

Tool configuration

T2Cert

• version: 1.0