# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• 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

We consider the following cutpoint-transitions:
 0 17 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 3 24 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 4 31 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 38 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
and for every transition t, a duplicate t is considered.

### 2 Transition Removal

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

 12: 0 11: 0 0: 0 1: 0 4: 0 5: 0 2: 0 3: 0 6: 0 7: 0 8: 0 9: 0 10: 0 12: −6 11: −7 0: −8 1: −8 4: −8 5: −8 0_var_snapshot: −8 0*: −8 4_var_snapshot: −8 4*: −8 2: −11 3: −11 6: −11 7: −11 8: −11 9: −11 3_var_snapshot: −11 3*: −11 8_var_snapshot: −11 8*: −11 10: −14
Hints:
 18 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 25 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 32 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 39 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 0 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 1 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 2 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 3 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 4 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 5 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 6 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 8 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 9 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 10 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 11 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 12 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 14 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 7 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 13 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 15 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 16 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

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 ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_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 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0

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 ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_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 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0

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 ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_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 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0

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 ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_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 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0

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 ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_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 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0

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 ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_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 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0

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 ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_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 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_0 ≤ 0

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 ≤ 0ret_RandomInteger15_postret_RandomInteger15_post ≤ 0ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0ret_RandomInteger15_0ret_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 ≤ 0TotalTime4_post + TotalTime4_post ≤ 0TotalTime4_postTotalTime4_post ≤ 0TotalTime4_0 + TotalTime4_0 ≤ 0TotalTime4_0TotalTime4_0 ≤ 0StopTime3_post + StopTime3_post ≤ 0StopTime3_postStopTime3_post ≤ 0StopTime3_0 + StopTime3_0 ≤ 0StopTime3_0StopTime3_0 ≤ 0StartTime2_post + StartTime2_post ≤ 0StartTime2_postStartTime2_post ≤ 0StartTime2_0 + StartTime2_0 ≤ 0StartTime2_0StartTime2_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0Ptotal11_post + Ptotal11_post ≤ 0Ptotal11_postPtotal11_post ≤ 0Ptotal11_0 + Ptotal11_0 ≤ 0Ptotal11_0Ptotal11_0 ≤ 0Postotal_post + Postotal_post ≤ 0Postotal_postPostotal_post ≤ 0Postotal_0 + Postotal_0 ≤ 0Postotal_0Postotal_0 ≤ 0Poscnt_post + Poscnt_post ≤ 0Poscnt_postPoscnt_post ≤ 0Poscnt_0 + Poscnt_0 ≤ 0Poscnt_0Poscnt_0 ≤ 0Pcnt13_post + Pcnt13_post ≤ 0Pcnt13_postPcnt13_post ≤ 0Pcnt13_0 + Pcnt13_0 ≤ 0Pcnt13_0Pcnt13_0 ≤ 0OuterIndex6_post + OuterIndex6_post ≤ 0OuterIndex6_postOuterIndex6_post ≤ 0OuterIndex6_0 + OuterIndex6_0 ≤ 0OuterIndex6_0OuterIndex6_0 ≤ 0Outer9_post + Outer9_post ≤ 0Outer9_postOuter9_post ≤ 0Outer9_0 + Outer9_0 ≤ 0Outer9_0Outer9_0 ≤ 0Ntotal12_post + Ntotal12_post ≤ 0Ntotal12_postNtotal12_post ≤ 0Ntotal12_0 + Ntotal12_0 ≤ 0Ntotal12_0Ntotal12_0 ≤ 0Negtotal_post + Negtotal_post ≤ 0Negtotal_postNegtotal_post ≤ 0Negtotal_0 + Negtotal_0 ≤ 0Negtotal_0Negtotal_0 ≤ 0Negcnt_post + Negcnt_post ≤ 0Negcnt_postNegcnt_post ≤ 0Negcnt_0 + Negcnt_0 ≤ 0Negcnt_0Negcnt_0 ≤ 0Ncnt14_post + Ncnt14_post ≤ 0Ncnt14_postNcnt14_post ≤ 0Ncnt14_0 + Ncnt14_0 ≤ 0Ncnt14_0Ncnt14_0 ≤ 0InnerIndex7_post + InnerIndex7_post ≤ 0InnerIndex7_postInnerIndex7_post ≤ 0InnerIndex7_0 + InnerIndex7_0 ≤ 0InnerIndex7_0InnerIndex7_0 ≤ 0Inner10_post + Inner10_post ≤ 0Inner10_postInner10_post ≤ 0Inner10_0 + Inner10_0 ≤ 0Inner10_0Inner10_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.

 2: −3⋅Outer9_0 + 3⋅___const_10_0 3: −3⋅Outer9_0 + 3⋅___const_10_0 6: −3⋅Outer9_0 + 3⋅___const_10_0 7: −3⋅Outer9_0 + 3⋅___const_10_0 8: 2 − 3⋅Outer9_0 + 3⋅___const_10_0 9: 1 − 3⋅Outer9_0 + 3⋅___const_10_0 3_var_snapshot: −3⋅Outer9_0 + 3⋅___const_10_0 3*: −3⋅Outer9_0 + 3⋅___const_10_0 8_var_snapshot: 2 − 3⋅Outer9_0 + 3⋅___const_10_0 8*: 2 − 3⋅Outer9_0 + 3⋅___const_10_0
Hints:
 25 lexWeak[ [0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 27 lexWeak[ [0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 39 lexWeak[ [0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 41 lexWeak[ [0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 1 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 3 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 4 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 5 lexWeak[ [0, 0, 0, 0, 3, 0, 3, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 6 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 8 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 9 lexWeak[ [0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 10 lexWeak[ [0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 11.1.2 Transition Removal

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

 2: −2 − 5⋅Inner10_0 + 5⋅___const_10_0 3: 1 − 5⋅Inner10_0 + 5⋅___const_10_0 6: −2 − 5⋅Inner10_0 + 5⋅___const_10_0 7: −1 − 5⋅Inner10_0 + 5⋅___const_10_0 8: −3 − 5⋅Inner10_0 + 5⋅___const_10_0 9: −4 − 5⋅Inner10_0 + 5⋅___const_10_0 3_var_snapshot: −5⋅Inner10_0 + 5⋅___const_10_0 3*: 2 − 5⋅Inner10_0 + 5⋅___const_10_0 8_var_snapshot: −4 − 5⋅Inner10_0 + 5⋅___const_10_0 8*: −2 − 5⋅Inner10_0 + 5⋅___const_10_0
Hints:
 25 lexWeak[ [0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] ] 27 lexWeak[ [0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] ] 39 lexWeak[ [0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] ] 41 lexWeak[ [0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] ] 1 lexWeak[ [0, 0, 0, 5, 0, 5, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 3 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] ] 4 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] ] 5 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] ] 6 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] , [5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 9 lexWeak[ [0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] ] 10 lexWeak[ [0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5] ]

### 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.

 2: 3 3: 1 6: 4 7: −1 8: −3 9: −5 3_var_snapshot: 0 3*: 2 8_var_snapshot: −4 8*: −2
Hints:
 25 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 27 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 39 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 41 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 1 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 3 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 4 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 5 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 9 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 10 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 11.1.4 Transition Removal

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

 2: 1 3: 0 6: 0 7: 0 8: 0 9: 0 3_var_snapshot: 0 3*: 0 8_var_snapshot: 0 8*: 0
Hints:
 1 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 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

Here we consider cut-point transition 24.

### 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

Here we consider cut-point transition 38.

### 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.

 0: 1 − 8⋅OuterIndex6_0 + 8⋅___const_10_0 1: −8⋅OuterIndex6_0 + 8⋅___const_10_0 4: −5 − 8⋅OuterIndex6_0 + 8⋅___const_10_0 5: −5 − 8⋅OuterIndex6_0 + 8⋅___const_10_0 0_var_snapshot: −8⋅OuterIndex6_0 + 8⋅___const_10_0 0*: 2 − 8⋅OuterIndex6_0 + 8⋅___const_10_0 4_var_snapshot: −5 − 8⋅OuterIndex6_0 + 8⋅___const_10_0 4*: −5 − 8⋅OuterIndex6_0 + 8⋅___const_10_0
Hints:
 18 lexWeak[ [0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0] ] 20 lexWeak[ [0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0] ] 32 lexWeak[ [0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0] ] 34 lexWeak[ [0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0] ] 0 lexWeak[ [0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0] ] 2 lexWeak[ [0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0] ] 11 lexWeak[ [0, 0, 0, 0, 8, 0, 8, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 12 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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] ] 14 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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] , [0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 11.2.2 Transition Removal

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

 0: −2 − 4⋅InnerIndex7_0 + 4⋅___const_10_0 1: −4 − 4⋅InnerIndex7_0 + 4⋅___const_10_0 4: 2 − 4⋅InnerIndex7_0 + 4⋅___const_10_0 5: −4⋅InnerIndex7_0 + 4⋅___const_10_0 0_var_snapshot: −3 − 4⋅InnerIndex7_0 + 4⋅___const_10_0 0*: −1 − 4⋅InnerIndex7_0 + 4⋅___const_10_0 4_var_snapshot: 1 − 4⋅InnerIndex7_0 + 4⋅___const_10_0 4*: 3 − 4⋅InnerIndex7_0 + 4⋅___const_10_0
Hints:
 18 lexWeak[ [0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0] ] 20 lexWeak[ [0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0] ] 32 lexWeak[ [0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0] ] 34 lexWeak[ [0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0] ] 0 lexWeak[ [0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0] ] 2 lexWeak[ [0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0] ] 11 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0] ] 12 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 4, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 11.2.3 Transition Removal

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

 0: −2 1: −4 4: 2 5: 0 0_var_snapshot: −3 0*: −1 4_var_snapshot: 1 4*: 3
Hints:
 18 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 20 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 32 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 34 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 0 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 2 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 11 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 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

Here we consider cut-point transition 17.

### 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

Here we consider cut-point transition 31.

### 11.2.4.2.1 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0