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 ∧ − 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 ∧ − 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 ∧ − 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 ∧ − 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 ∧ − 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 ∧ 10 − Inner10_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 ∧ − 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:	−9 + Inner10_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 ∧ − 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 ∧ 10 − Outer9_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 ∧ −1500 + StopTime3_post ≤ 0 ∧ 1500 − StopTime3_post ≤ 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 ∧ − 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 ∧ −9 + Outer9_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 ∧ − 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 ∧ − 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 ∧ − 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 ∧ 10 − InnerIndex7_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 ∧ − 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 ∧ −9 + InnerIndex7_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 ∧ − 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 ∧ 10 − OuterIndex6_0 ≤ 0 ∧ −1000 + StartTime2_post ≤ 0 ∧ 1000 − StartTime2_post ≤ 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 ∧ − 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 ∧ −9 + OuterIndex6_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 ∧ − 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 ∧ − 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 ∧ − 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 Invariant Updates

The following invariants are asserted.

0:	TRUE
1:	TRUE
2:	10 − OuterIndex6_0 ≤ 0 ∧ −1000 + StartTime2_post ≤ 0 ∧ 1000 − StartTime2_post ≤ 0 ∧ −1000 + StartTime2_0 ≤ 0 ∧ 1000 − StartTime2_0 ≤ 0
3:	10 − OuterIndex6_0 ≤ 0 ∧ −1000 + StartTime2_post ≤ 0 ∧ 1000 − StartTime2_post ≤ 0 ∧ −1000 + StartTime2_0 ≤ 0 ∧ 1000 − StartTime2_0 ≤ 0
4:	TRUE
5:	TRUE
6:	10 − OuterIndex6_0 ≤ 0 ∧ −1000 + StartTime2_post ≤ 0 ∧ 1000 − StartTime2_post ≤ 0 ∧ −1000 + StartTime2_0 ≤ 0 ∧ 1000 − StartTime2_0 ≤ 0
7:	10 − OuterIndex6_0 ≤ 0 ∧ −1000 + StartTime2_post ≤ 0 ∧ 1000 − StartTime2_post ≤ 0 ∧ −1000 + StartTime2_0 ≤ 0 ∧ 1000 − StartTime2_0 ≤ 0
8:	10 − OuterIndex6_0 ≤ 0 ∧ −1000 + StartTime2_post ≤ 0 ∧ 1000 − StartTime2_post ≤ 0 ∧ −1000 + StartTime2_0 ≤ 0 ∧ 1000 − StartTime2_0 ≤ 0
9:	10 − OuterIndex6_0 ≤ 0 ∧ −1000 + StartTime2_post ≤ 0 ∧ 1000 − StartTime2_post ≤ 0 ∧ −1000 + StartTime2_0 ≤ 0 ∧ 1000 − StartTime2_0 ≤ 0
10:	10 − OuterIndex6_0 ≤ 0 ∧ −1000 + StartTime2_post ≤ 0 ∧ 1000 − StartTime2_post ≤ 0 ∧ 10 − Outer9_0 ≤ 0 ∧ −1000 + StartTime2_0 ≤ 0 ∧ 1000 − StartTime2_0 ≤ 0 ∧ −1500 + StopTime3_post ≤ 0 ∧ 1500 − StopTime3_post ≤ 0 ∧ −1500 + StopTime3_0 ≤ 0 ∧ 1500 − StopTime3_0 ≤ 0
11:	TRUE
12:	TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

nodes (location) invariant:

0	(0)	TRUE
1	(1)	TRUE
2	(2)	10 − OuterIndex6_0 ≤ 0 ∧ −1000 + StartTime2_post ≤ 0 ∧ 1000 − StartTime2_post ≤ 0 ∧ −1000 + StartTime2_0 ≤ 0 ∧ 1000 − StartTime2_0 ≤ 0
3	(3)	10 − OuterIndex6_0 ≤ 0 ∧ −1000 + StartTime2_post ≤ 0 ∧ 1000 − StartTime2_post ≤ 0 ∧ −1000 + StartTime2_0 ≤ 0 ∧ 1000 − StartTime2_0 ≤ 0
4	(4)	TRUE
5	(5)	TRUE
6	(6)	10 − OuterIndex6_0 ≤ 0 ∧ −1000 + StartTime2_post ≤ 0 ∧ 1000 − StartTime2_post ≤ 0 ∧ −1000 + StartTime2_0 ≤ 0 ∧ 1000 − StartTime2_0 ≤ 0
7	(7)	10 − OuterIndex6_0 ≤ 0 ∧ −1000 + StartTime2_post ≤ 0 ∧ 1000 − StartTime2_post ≤ 0 ∧ −1000 + StartTime2_0 ≤ 0 ∧ 1000 − StartTime2_0 ≤ 0
8	(8)	10 − OuterIndex6_0 ≤ 0 ∧ −1000 + StartTime2_post ≤ 0 ∧ 1000 − StartTime2_post ≤ 0 ∧ −1000 + StartTime2_0 ≤ 0 ∧ 1000 − StartTime2_0 ≤ 0
9	(9)	10 − OuterIndex6_0 ≤ 0 ∧ −1000 + StartTime2_post ≤ 0 ∧ 1000 − StartTime2_post ≤ 0 ∧ −1000 + StartTime2_0 ≤ 0 ∧ 1000 − StartTime2_0 ≤ 0
10	(10)	10 − OuterIndex6_0 ≤ 0 ∧ −1000 + StartTime2_post ≤ 0 ∧ 1000 − StartTime2_post ≤ 0 ∧ 10 − Outer9_0 ≤ 0 ∧ −1000 + StartTime2_0 ≤ 0 ∧ 1000 − StartTime2_0 ≤ 0 ∧ −1500 + StopTime3_post ≤ 0 ∧ 1500 − StopTime3_post ≤ 0 ∧ −1500 + StopTime3_0 ≤ 0 ∧ 1500 − StopTime3_0 ≤ 0
11	(11)	TRUE
12	(12)	TRUE

initial node: 12
cover edges:
transition edges:

0 0 1

1 13 8

1 14 4

2 1 3

3 10 7

4 2 5

5 11 0

5 12 4

6 3 2

6 4 2

7 5 8

7 6 6

8 9 9

9 7 10

9 8 3

11 15 0

12 16 11

2 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 ∧ − 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 ∧ − 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 ∧ − 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 ∧ − 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.

3 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

4 Location Addition

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

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

5 Location Addition

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

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

6 Location Addition

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

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

7 Location Addition

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

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

8 Location Addition

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

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

9 Location Addition

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

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

10 Location Addition

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

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

11 Location Addition

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

8 39 8_var_snapshot: − ret_RandomInteger15_post + ret_RandomInteger15_post ≤ 0 ∧ ret_RandomInteger15_post − ret_RandomInteger15_post ≤ 0 ∧ − ret_RandomInteger15_0 + ret_RandomInteger15_0 ≤ 0 ∧ ret_RandomInteger15_0 − ret_RandomInteger15_0 ≤ 0 ∧ − 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

12 SCC Decomposition

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

12.1 SCC Subproblem 1/2

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

12.1.1 Transition Removal

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

2:	−3001⋅Outer9_0
3:	−3001⋅Outer9_0
6:	−3001⋅Outer9_0
7:	−3001⋅Outer9_0
8:	−3001⋅Outer9_0 + 3⋅StartTime2_post
9:	1000 − 3001⋅Outer9_0
3_var_snapshot:	−3001⋅Outer9_0
3*:	−3001⋅Outer9_0
8_var_snapshot:	−3001⋅Outer9_0 + 2⋅StartTime2_0
8*:	−3001⋅Outer9_0 + 3⋅StartTime2_post

12.1.2 Transition Removal

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

2:	−4002⋅Inner10_0 − StartTime2_0
3:	−4002⋅Inner10_0 + 3⋅StartTime2_0
6:	−4002⋅Inner10_0 − StartTime2_0 + StartTime2_post
7:	−4002⋅Inner10_0 + StartTime2_post
8:	−3000 − 4002⋅Inner10_0 + StartTime2_0 + StartTime2_post
9:	999 − 4002⋅Inner10_0 − 3⋅StartTime2_post
3_var_snapshot:	1000 − 4002⋅Inner10_0 + StartTime2_post
3*:	2001 − 4002⋅Inner10_0 + StartTime2_0
8_var_snapshot:	−4002⋅Inner10_0 + StartTime2_0 − 3⋅StartTime2_post
8*:	−1000 − 4002⋅Inner10_0 + StartTime2_post

12.1.3 Transition Removal

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

2:	3002
3:	3⋅StartTime2_0
6:	3003
7:	− StartTime2_0 + 2⋅StartTime2_post
8:	−1000
9:	−1 − 2⋅StartTime2_0
3_var_snapshot:	2⋅StartTime2_post
3*:	1 + 3⋅StartTime2_0
8_var_snapshot:	−2⋅StartTime2_0
8*:	0

12.1.4 Splitting Cut-Point Transitions

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

12.1.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 24.

12.1.4.1.1 Splitting Cut-Point Transitions

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

12.1.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 38.

12.1.4.2.1 Splitting Cut-Point Transitions

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

12.2 SCC Subproblem 2/2

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

12.2.1 Transition Removal

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

0:	1 − 4⋅OuterIndex6_0
1:	−4⋅OuterIndex6_0
4:	−1 − 4⋅OuterIndex6_0
5:	−1 − 4⋅OuterIndex6_0
0_var_snapshot:	−4⋅OuterIndex6_0
0*:	2 − 4⋅OuterIndex6_0
4_var_snapshot:	−1 − 4⋅OuterIndex6_0
4*:	−1 − 4⋅OuterIndex6_0

12.2.2 Transition Removal

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

0:	−11 − 4⋅InnerIndex7_0
1:	−13 − 4⋅InnerIndex7_0
4:	2 − 4⋅InnerIndex7_0
5:	−4⋅InnerIndex7_0
0_var_snapshot:	−12 − 4⋅InnerIndex7_0
0*:	−1 − 4⋅InnerIndex7_0
4_var_snapshot:	1 − 4⋅InnerIndex7_0
4*:	3 − 4⋅InnerIndex7_0

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

12.2.4 Splitting Cut-Point Transitions

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

12.2.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 17.

12.2.4.1.1 Splitting Cut-Point Transitions

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

12.2.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 31.

12.2.4.2.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert

version: 1.0

0	0 1
1	13 8
1	14 4
2	1 3
3	10 7
4	2 5
5	11 0
5	12 4
6	3 2
6	4 2
7	5 8
7	6 6
8	9 9
9	7 10
9	8 3
11	15 0
12	16 11