# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• Initial Location: 16
• Transitions: (pre-variables and post-variables)  0 0 1: − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 2 1 3: − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 4 2 5: − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 6 3 7: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 20 − Index15_0 ≤ 0 ∧ −1 − Inner14_0 + Inner14_post ≤ 0 ∧ 1 + Inner14_0 − Inner14_post ≤ 0 ∧ Inner14_0 − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_post ≤ 0 ∧ − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 6 4 8: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −19 + Index15_0 ≤ 0 ∧ −1 − Index15_0 + Index15_post ≤ 0 ∧ 1 + Index15_0 − Index15_post ≤ 0 ∧ Index15_0 − Index15_post ≤ 0 ∧ − Index15_0 + Index15_post ≤ 0 ∧ − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 9 5 10: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 20 − Inner14_0 ≤ 0 ∧ −1 − Outer13_0 + Outer13_post ≤ 0 ∧ 1 + Outer13_0 − Outer13_post ≤ 0 ∧ Outer13_0 − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_post ≤ 0 ∧ − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 9 6 8: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −19 + Inner14_0 ≤ 0 ∧ Index15_post ≤ 0 ∧ − Index15_post ≤ 0 ∧ Index15_0 − Index15_post ≤ 0 ∧ − Index15_0 + Index15_post ≤ 0 ∧ − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 11 7 12: 20 − Outer13_0 ≤ 0 ∧ − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 11 8 7: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −19 + Outer13_0 ≤ 0 ∧ Inner14_post ≤ 0 ∧ − Inner14_post ≤ 0 ∧ Inner14_0 − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_post ≤ 0 ∧ − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 13 9 14: − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 10 10 11: − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 14 11 4: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 20 − InnerIndex9_0 ≤ 0 ∧ −1 − OuterIndex8_0 + OuterIndex8_post ≤ 0 ∧ 1 + OuterIndex8_0 − OuterIndex8_post ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_post ≤ 0 ∧ − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 14 12 13: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −19 + InnerIndex9_0 ≤ 0 ∧ − Seed_post + ret_RandomInteger17_post ≤ 0 ∧ Seed_post − ret_RandomInteger17_post ≤ 0 ∧ −1 − InnerIndex9_0 + InnerIndex9_post ≤ 0 ∧ 1 + InnerIndex9_0 − InnerIndex9_post ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_post ≤ 0 ∧ Seed_0 − Seed_post ≤ 0 ∧ − Seed_0 + Seed_post ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 5 13 10: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 20 − OuterIndex8_0 ≤ 0 ∧ Outer13_post ≤ 0 ∧ − Outer13_post ≤ 0 ∧ Outer13_0 − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_post ≤ 0 ∧ − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 5 14 13: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −19 + OuterIndex8_0 ≤ 0 ∧ InnerIndex9_post ≤ 0 ∧ − InnerIndex9_post ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_post ≤ 0 ∧ − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 7 15 9: − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 8 16 6: − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 3 17 0: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 20 − InnerIndex6_0 ≤ 0 ∧ −1 − OuterIndex5_0 + OuterIndex5_post ≤ 0 ∧ 1 + OuterIndex5_0 − OuterIndex5_post ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_post ≤ 0 ∧ − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 3 18 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −19 + InnerIndex6_0 ≤ 0 ∧ − Seed_post + ret_RandomInteger16_post ≤ 0 ∧ Seed_post − ret_RandomInteger16_post ≤ 0 ∧ −1 − InnerIndex6_0 + InnerIndex6_post ≤ 0 ∧ 1 + InnerIndex6_0 − InnerIndex6_post ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_post ≤ 0 ∧ Seed_0 − Seed_post ≤ 0 ∧ − Seed_0 + Seed_post ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 1 19 4: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 20 − OuterIndex5_0 ≤ 0 ∧ OuterIndex8_post ≤ 0 ∧ − OuterIndex8_post ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_post ≤ 0 ∧ − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 1 20 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −19 + OuterIndex5_0 ≤ 0 ∧ InnerIndex6_post ≤ 0 ∧ − InnerIndex6_post ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_post ≤ 0 ∧ − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 15 21 0: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ Seed_post ≤ 0 ∧ − Seed_post ≤ 0 ∧ OuterIndex5_post ≤ 0 ∧ − OuterIndex5_post ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_post ≤ 0 ∧ Seed_0 − Seed_post ≤ 0 ∧ − Seed_0 + Seed_post ≤ 0 ∧ − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 16 22 15: − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0

## Proof

The following invariants are asserted.

 0: TRUE 1: TRUE 2: TRUE 3: TRUE 4: 20 − OuterIndex5_0 ≤ 0 5: 20 − OuterIndex5_0 ≤ 0 6: 20 − OuterIndex5_0 ≤ 0 ∧ 20 − OuterIndex8_0 ≤ 0 7: 20 − OuterIndex5_0 ≤ 0 ∧ 20 − OuterIndex8_0 ≤ 0 8: 20 − OuterIndex5_0 ≤ 0 ∧ 20 − OuterIndex8_0 ≤ 0 9: 20 − OuterIndex5_0 ≤ 0 ∧ 20 − OuterIndex8_0 ≤ 0 10: 20 − OuterIndex5_0 ≤ 0 ∧ 20 − OuterIndex8_0 ≤ 0 11: 20 − OuterIndex5_0 ≤ 0 ∧ 20 − OuterIndex8_0 ≤ 0 12: 20 − OuterIndex5_0 ≤ 0 ∧ 20 − OuterIndex8_0 ≤ 0 ∧ 20 − Outer13_0 ≤ 0 13: 20 − OuterIndex5_0 ≤ 0 14: 20 − OuterIndex5_0 ≤ 0 15: TRUE 16: TRUE

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (0) TRUE 1 (1) TRUE 2 (2) TRUE 3 (3) TRUE 4 (4) 20 − OuterIndex5_0 ≤ 0 5 (5) 20 − OuterIndex5_0 ≤ 0 6 (6) 20 − OuterIndex5_0 ≤ 0 ∧ 20 − OuterIndex8_0 ≤ 0 7 (7) 20 − OuterIndex5_0 ≤ 0 ∧ 20 − OuterIndex8_0 ≤ 0 8 (8) 20 − OuterIndex5_0 ≤ 0 ∧ 20 − OuterIndex8_0 ≤ 0 9 (9) 20 − OuterIndex5_0 ≤ 0 ∧ 20 − OuterIndex8_0 ≤ 0 10 (10) 20 − OuterIndex5_0 ≤ 0 ∧ 20 − OuterIndex8_0 ≤ 0 11 (11) 20 − OuterIndex5_0 ≤ 0 ∧ 20 − OuterIndex8_0 ≤ 0 12 (12) 20 − OuterIndex5_0 ≤ 0 ∧ 20 − OuterIndex8_0 ≤ 0 ∧ 20 − Outer13_0 ≤ 0 13 (13) 20 − OuterIndex5_0 ≤ 0 14 (14) 20 − OuterIndex5_0 ≤ 0 15 (15) TRUE 16 (16) TRUE
• initial node: 16
• cover edges:
• transition edges:  0 0 1 1 19 4 1 20 2 2 1 3 3 17 0 3 18 2 4 2 5 5 13 10 5 14 13 6 3 7 6 4 8 7 15 9 8 16 6 9 5 10 9 6 8 10 10 11 11 7 12 11 8 7 13 9 14 14 11 4 14 12 13 15 21 0 16 22 15

### 2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 0 23 0: − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 2 30 2: − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 4 37 4: − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 7 44 7: − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 8 51 8: − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 10 58 10: − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0 13 65 13: − ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0 ∧ ret_RandomInteger17_post − ret_RandomInteger17_post ≤ 0 ∧ − ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0 ∧ ret_RandomInteger17_0 − ret_RandomInteger17_0 ≤ 0 ∧ − ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0 ∧ ret_RandomInteger16_post − ret_RandomInteger16_post ≤ 0 ∧ − ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0 ∧ ret_RandomInteger16_0 − ret_RandomInteger16_0 ≤ 0 ∧ − Seed_post + Seed_post ≤ 0 ∧ Seed_post − Seed_post ≤ 0 ∧ − Seed_0 + Seed_0 ≤ 0 ∧ Seed_0 − Seed_0 ≤ 0 ∧ − OuterIndex8_post + OuterIndex8_post ≤ 0 ∧ OuterIndex8_post − OuterIndex8_post ≤ 0 ∧ − OuterIndex8_0 + OuterIndex8_0 ≤ 0 ∧ OuterIndex8_0 − OuterIndex8_0 ≤ 0 ∧ − OuterIndex5_post + OuterIndex5_post ≤ 0 ∧ OuterIndex5_post − OuterIndex5_post ≤ 0 ∧ − OuterIndex5_0 + OuterIndex5_0 ≤ 0 ∧ OuterIndex5_0 − OuterIndex5_0 ≤ 0 ∧ − Outer13_post + Outer13_post ≤ 0 ∧ Outer13_post − Outer13_post ≤ 0 ∧ − Outer13_0 + Outer13_0 ≤ 0 ∧ Outer13_0 − Outer13_0 ≤ 0 ∧ − InnerIndex9_post + InnerIndex9_post ≤ 0 ∧ InnerIndex9_post − InnerIndex9_post ≤ 0 ∧ − InnerIndex9_0 + InnerIndex9_0 ≤ 0 ∧ InnerIndex9_0 − InnerIndex9_0 ≤ 0 ∧ − InnerIndex6_post + InnerIndex6_post ≤ 0 ∧ InnerIndex6_post − InnerIndex6_post ≤ 0 ∧ − InnerIndex6_0 + InnerIndex6_0 ≤ 0 ∧ InnerIndex6_0 − InnerIndex6_0 ≤ 0 ∧ − Inner14_post + Inner14_post ≤ 0 ∧ Inner14_post − Inner14_post ≤ 0 ∧ − Inner14_0 + Inner14_0 ≤ 0 ∧ Inner14_0 − Inner14_0 ≤ 0 ∧ − Index15_post + Index15_post ≤ 0 ∧ Index15_post − Index15_post ≤ 0 ∧ − Index15_0 + Index15_0 ≤ 0 ∧ Index15_0 − Index15_0 ≤ 0
and for every transition t, a duplicate t is considered.

### 3 Transition Removal

We remove transitions 7, 13, 19, 21, 22 using the following ranking functions, which are bounded by −29.

 16: 0 15: 0 0: 0 1: 0 2: 0 3: 0 4: 0 5: 0 13: 0 14: 0 6: 0 7: 0 8: 0 9: 0 10: 0 11: 0 12: 0 16: −7 15: −8 0: −9 1: −9 2: −9 3: −9 0_var_snapshot: −9 0*: −9 2_var_snapshot: −9 2*: −9 4: −12 5: −12 13: −12 14: −12 4_var_snapshot: −12 4*: −12 13_var_snapshot: −12 13*: −12 6: −15 7: −15 8: −15 9: −15 10: −15 11: −15 7_var_snapshot: −15 7*: −15 8_var_snapshot: −15 8*: −15 10_var_snapshot: −15 10*: −15 12: −20
Hints:
 24 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] ] 31 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] ] 38 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] ] 45 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] ] 52 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] ] 59 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] ] 66 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 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] ] 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] ] 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] ] 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] ] 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] ] 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] ] 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] ] 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] ] 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] ] 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] ] 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] ] 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] ] 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] ] 15 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] ] 16 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] ] 17 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] ] 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] ] 20 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] ] 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] ] 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] ] 19 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] ] 21 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] ] 22 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] ]

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

0* 26 0: ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0ret_RandomInteger17_postret_RandomInteger17_post ≤ 0ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0ret_RandomInteger17_0ret_RandomInteger17_0 ≤ 0ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0ret_RandomInteger16_postret_RandomInteger16_post ≤ 0ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0ret_RandomInteger16_0ret_RandomInteger16_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0OuterIndex8_post + OuterIndex8_post ≤ 0OuterIndex8_postOuterIndex8_post ≤ 0OuterIndex8_0 + OuterIndex8_0 ≤ 0OuterIndex8_0OuterIndex8_0 ≤ 0OuterIndex5_post + OuterIndex5_post ≤ 0OuterIndex5_postOuterIndex5_post ≤ 0OuterIndex5_0 + OuterIndex5_0 ≤ 0OuterIndex5_0OuterIndex5_0 ≤ 0Outer13_post + Outer13_post ≤ 0Outer13_postOuter13_post ≤ 0Outer13_0 + Outer13_0 ≤ 0Outer13_0Outer13_0 ≤ 0InnerIndex9_post + InnerIndex9_post ≤ 0InnerIndex9_postInnerIndex9_post ≤ 0InnerIndex9_0 + InnerIndex9_0 ≤ 0InnerIndex9_0InnerIndex9_0 ≤ 0InnerIndex6_post + InnerIndex6_post ≤ 0InnerIndex6_postInnerIndex6_post ≤ 0InnerIndex6_0 + InnerIndex6_0 ≤ 0InnerIndex6_0InnerIndex6_0 ≤ 0Inner14_post + Inner14_post ≤ 0Inner14_postInner14_post ≤ 0Inner14_0 + Inner14_0 ≤ 0Inner14_0Inner14_0 ≤ 0Index15_post + Index15_post ≤ 0Index15_postIndex15_post ≤ 0Index15_0 + Index15_0 ≤ 0Index15_0Index15_0 ≤ 0

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

0 24 0_var_snapshot: ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0ret_RandomInteger17_postret_RandomInteger17_post ≤ 0ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0ret_RandomInteger17_0ret_RandomInteger17_0 ≤ 0ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0ret_RandomInteger16_postret_RandomInteger16_post ≤ 0ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0ret_RandomInteger16_0ret_RandomInteger16_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0OuterIndex8_post + OuterIndex8_post ≤ 0OuterIndex8_postOuterIndex8_post ≤ 0OuterIndex8_0 + OuterIndex8_0 ≤ 0OuterIndex8_0OuterIndex8_0 ≤ 0OuterIndex5_post + OuterIndex5_post ≤ 0OuterIndex5_postOuterIndex5_post ≤ 0OuterIndex5_0 + OuterIndex5_0 ≤ 0OuterIndex5_0OuterIndex5_0 ≤ 0Outer13_post + Outer13_post ≤ 0Outer13_postOuter13_post ≤ 0Outer13_0 + Outer13_0 ≤ 0Outer13_0Outer13_0 ≤ 0InnerIndex9_post + InnerIndex9_post ≤ 0InnerIndex9_postInnerIndex9_post ≤ 0InnerIndex9_0 + InnerIndex9_0 ≤ 0InnerIndex9_0InnerIndex9_0 ≤ 0InnerIndex6_post + InnerIndex6_post ≤ 0InnerIndex6_postInnerIndex6_post ≤ 0InnerIndex6_0 + InnerIndex6_0 ≤ 0InnerIndex6_0InnerIndex6_0 ≤ 0Inner14_post + Inner14_post ≤ 0Inner14_postInner14_post ≤ 0Inner14_0 + Inner14_0 ≤ 0Inner14_0Inner14_0 ≤ 0Index15_post + Index15_post ≤ 0Index15_postIndex15_post ≤ 0Index15_0 + Index15_0 ≤ 0Index15_0Index15_0 ≤ 0

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

2* 33 2: ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0ret_RandomInteger17_postret_RandomInteger17_post ≤ 0ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0ret_RandomInteger17_0ret_RandomInteger17_0 ≤ 0ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0ret_RandomInteger16_postret_RandomInteger16_post ≤ 0ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0ret_RandomInteger16_0ret_RandomInteger16_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0OuterIndex8_post + OuterIndex8_post ≤ 0OuterIndex8_postOuterIndex8_post ≤ 0OuterIndex8_0 + OuterIndex8_0 ≤ 0OuterIndex8_0OuterIndex8_0 ≤ 0OuterIndex5_post + OuterIndex5_post ≤ 0OuterIndex5_postOuterIndex5_post ≤ 0OuterIndex5_0 + OuterIndex5_0 ≤ 0OuterIndex5_0OuterIndex5_0 ≤ 0Outer13_post + Outer13_post ≤ 0Outer13_postOuter13_post ≤ 0Outer13_0 + Outer13_0 ≤ 0Outer13_0Outer13_0 ≤ 0InnerIndex9_post + InnerIndex9_post ≤ 0InnerIndex9_postInnerIndex9_post ≤ 0InnerIndex9_0 + InnerIndex9_0 ≤ 0InnerIndex9_0InnerIndex9_0 ≤ 0InnerIndex6_post + InnerIndex6_post ≤ 0InnerIndex6_postInnerIndex6_post ≤ 0InnerIndex6_0 + InnerIndex6_0 ≤ 0InnerIndex6_0InnerIndex6_0 ≤ 0Inner14_post + Inner14_post ≤ 0Inner14_postInner14_post ≤ 0Inner14_0 + Inner14_0 ≤ 0Inner14_0Inner14_0 ≤ 0Index15_post + Index15_post ≤ 0Index15_postIndex15_post ≤ 0Index15_0 + Index15_0 ≤ 0Index15_0Index15_0 ≤ 0

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

2 31 2_var_snapshot: ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0ret_RandomInteger17_postret_RandomInteger17_post ≤ 0ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0ret_RandomInteger17_0ret_RandomInteger17_0 ≤ 0ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0ret_RandomInteger16_postret_RandomInteger16_post ≤ 0ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0ret_RandomInteger16_0ret_RandomInteger16_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0OuterIndex8_post + OuterIndex8_post ≤ 0OuterIndex8_postOuterIndex8_post ≤ 0OuterIndex8_0 + OuterIndex8_0 ≤ 0OuterIndex8_0OuterIndex8_0 ≤ 0OuterIndex5_post + OuterIndex5_post ≤ 0OuterIndex5_postOuterIndex5_post ≤ 0OuterIndex5_0 + OuterIndex5_0 ≤ 0OuterIndex5_0OuterIndex5_0 ≤ 0Outer13_post + Outer13_post ≤ 0Outer13_postOuter13_post ≤ 0Outer13_0 + Outer13_0 ≤ 0Outer13_0Outer13_0 ≤ 0InnerIndex9_post + InnerIndex9_post ≤ 0InnerIndex9_postInnerIndex9_post ≤ 0InnerIndex9_0 + InnerIndex9_0 ≤ 0InnerIndex9_0InnerIndex9_0 ≤ 0InnerIndex6_post + InnerIndex6_post ≤ 0InnerIndex6_postInnerIndex6_post ≤ 0InnerIndex6_0 + InnerIndex6_0 ≤ 0InnerIndex6_0InnerIndex6_0 ≤ 0Inner14_post + Inner14_post ≤ 0Inner14_postInner14_post ≤ 0Inner14_0 + Inner14_0 ≤ 0Inner14_0Inner14_0 ≤ 0Index15_post + Index15_post ≤ 0Index15_postIndex15_post ≤ 0Index15_0 + Index15_0 ≤ 0Index15_0Index15_0 ≤ 0

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

4* 40 4: ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0ret_RandomInteger17_postret_RandomInteger17_post ≤ 0ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0ret_RandomInteger17_0ret_RandomInteger17_0 ≤ 0ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0ret_RandomInteger16_postret_RandomInteger16_post ≤ 0ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0ret_RandomInteger16_0ret_RandomInteger16_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0OuterIndex8_post + OuterIndex8_post ≤ 0OuterIndex8_postOuterIndex8_post ≤ 0OuterIndex8_0 + OuterIndex8_0 ≤ 0OuterIndex8_0OuterIndex8_0 ≤ 0OuterIndex5_post + OuterIndex5_post ≤ 0OuterIndex5_postOuterIndex5_post ≤ 0OuterIndex5_0 + OuterIndex5_0 ≤ 0OuterIndex5_0OuterIndex5_0 ≤ 0Outer13_post + Outer13_post ≤ 0Outer13_postOuter13_post ≤ 0Outer13_0 + Outer13_0 ≤ 0Outer13_0Outer13_0 ≤ 0InnerIndex9_post + InnerIndex9_post ≤ 0InnerIndex9_postInnerIndex9_post ≤ 0InnerIndex9_0 + InnerIndex9_0 ≤ 0InnerIndex9_0InnerIndex9_0 ≤ 0InnerIndex6_post + InnerIndex6_post ≤ 0InnerIndex6_postInnerIndex6_post ≤ 0InnerIndex6_0 + InnerIndex6_0 ≤ 0InnerIndex6_0InnerIndex6_0 ≤ 0Inner14_post + Inner14_post ≤ 0Inner14_postInner14_post ≤ 0Inner14_0 + Inner14_0 ≤ 0Inner14_0Inner14_0 ≤ 0Index15_post + Index15_post ≤ 0Index15_postIndex15_post ≤ 0Index15_0 + Index15_0 ≤ 0Index15_0Index15_0 ≤ 0

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

4 38 4_var_snapshot: ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0ret_RandomInteger17_postret_RandomInteger17_post ≤ 0ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0ret_RandomInteger17_0ret_RandomInteger17_0 ≤ 0ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0ret_RandomInteger16_postret_RandomInteger16_post ≤ 0ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0ret_RandomInteger16_0ret_RandomInteger16_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0OuterIndex8_post + OuterIndex8_post ≤ 0OuterIndex8_postOuterIndex8_post ≤ 0OuterIndex8_0 + OuterIndex8_0 ≤ 0OuterIndex8_0OuterIndex8_0 ≤ 0OuterIndex5_post + OuterIndex5_post ≤ 0OuterIndex5_postOuterIndex5_post ≤ 0OuterIndex5_0 + OuterIndex5_0 ≤ 0OuterIndex5_0OuterIndex5_0 ≤ 0Outer13_post + Outer13_post ≤ 0Outer13_postOuter13_post ≤ 0Outer13_0 + Outer13_0 ≤ 0Outer13_0Outer13_0 ≤ 0InnerIndex9_post + InnerIndex9_post ≤ 0InnerIndex9_postInnerIndex9_post ≤ 0InnerIndex9_0 + InnerIndex9_0 ≤ 0InnerIndex9_0InnerIndex9_0 ≤ 0InnerIndex6_post + InnerIndex6_post ≤ 0InnerIndex6_postInnerIndex6_post ≤ 0InnerIndex6_0 + InnerIndex6_0 ≤ 0InnerIndex6_0InnerIndex6_0 ≤ 0Inner14_post + Inner14_post ≤ 0Inner14_postInner14_post ≤ 0Inner14_0 + Inner14_0 ≤ 0Inner14_0Inner14_0 ≤ 0Index15_post + Index15_post ≤ 0Index15_postIndex15_post ≤ 0Index15_0 + Index15_0 ≤ 0Index15_0Index15_0 ≤ 0

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

7* 47 7: ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0ret_RandomInteger17_postret_RandomInteger17_post ≤ 0ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0ret_RandomInteger17_0ret_RandomInteger17_0 ≤ 0ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0ret_RandomInteger16_postret_RandomInteger16_post ≤ 0ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0ret_RandomInteger16_0ret_RandomInteger16_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0OuterIndex8_post + OuterIndex8_post ≤ 0OuterIndex8_postOuterIndex8_post ≤ 0OuterIndex8_0 + OuterIndex8_0 ≤ 0OuterIndex8_0OuterIndex8_0 ≤ 0OuterIndex5_post + OuterIndex5_post ≤ 0OuterIndex5_postOuterIndex5_post ≤ 0OuterIndex5_0 + OuterIndex5_0 ≤ 0OuterIndex5_0OuterIndex5_0 ≤ 0Outer13_post + Outer13_post ≤ 0Outer13_postOuter13_post ≤ 0Outer13_0 + Outer13_0 ≤ 0Outer13_0Outer13_0 ≤ 0InnerIndex9_post + InnerIndex9_post ≤ 0InnerIndex9_postInnerIndex9_post ≤ 0InnerIndex9_0 + InnerIndex9_0 ≤ 0InnerIndex9_0InnerIndex9_0 ≤ 0InnerIndex6_post + InnerIndex6_post ≤ 0InnerIndex6_postInnerIndex6_post ≤ 0InnerIndex6_0 + InnerIndex6_0 ≤ 0InnerIndex6_0InnerIndex6_0 ≤ 0Inner14_post + Inner14_post ≤ 0Inner14_postInner14_post ≤ 0Inner14_0 + Inner14_0 ≤ 0Inner14_0Inner14_0 ≤ 0Index15_post + Index15_post ≤ 0Index15_postIndex15_post ≤ 0Index15_0 + Index15_0 ≤ 0Index15_0Index15_0 ≤ 0

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

7 45 7_var_snapshot: ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0ret_RandomInteger17_postret_RandomInteger17_post ≤ 0ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0ret_RandomInteger17_0ret_RandomInteger17_0 ≤ 0ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0ret_RandomInteger16_postret_RandomInteger16_post ≤ 0ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0ret_RandomInteger16_0ret_RandomInteger16_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0OuterIndex8_post + OuterIndex8_post ≤ 0OuterIndex8_postOuterIndex8_post ≤ 0OuterIndex8_0 + OuterIndex8_0 ≤ 0OuterIndex8_0OuterIndex8_0 ≤ 0OuterIndex5_post + OuterIndex5_post ≤ 0OuterIndex5_postOuterIndex5_post ≤ 0OuterIndex5_0 + OuterIndex5_0 ≤ 0OuterIndex5_0OuterIndex5_0 ≤ 0Outer13_post + Outer13_post ≤ 0Outer13_postOuter13_post ≤ 0Outer13_0 + Outer13_0 ≤ 0Outer13_0Outer13_0 ≤ 0InnerIndex9_post + InnerIndex9_post ≤ 0InnerIndex9_postInnerIndex9_post ≤ 0InnerIndex9_0 + InnerIndex9_0 ≤ 0InnerIndex9_0InnerIndex9_0 ≤ 0InnerIndex6_post + InnerIndex6_post ≤ 0InnerIndex6_postInnerIndex6_post ≤ 0InnerIndex6_0 + InnerIndex6_0 ≤ 0InnerIndex6_0InnerIndex6_0 ≤ 0Inner14_post + Inner14_post ≤ 0Inner14_postInner14_post ≤ 0Inner14_0 + Inner14_0 ≤ 0Inner14_0Inner14_0 ≤ 0Index15_post + Index15_post ≤ 0Index15_postIndex15_post ≤ 0Index15_0 + Index15_0 ≤ 0Index15_0Index15_0 ≤ 0

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

8* 54 8: ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0ret_RandomInteger17_postret_RandomInteger17_post ≤ 0ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0ret_RandomInteger17_0ret_RandomInteger17_0 ≤ 0ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0ret_RandomInteger16_postret_RandomInteger16_post ≤ 0ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0ret_RandomInteger16_0ret_RandomInteger16_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0OuterIndex8_post + OuterIndex8_post ≤ 0OuterIndex8_postOuterIndex8_post ≤ 0OuterIndex8_0 + OuterIndex8_0 ≤ 0OuterIndex8_0OuterIndex8_0 ≤ 0OuterIndex5_post + OuterIndex5_post ≤ 0OuterIndex5_postOuterIndex5_post ≤ 0OuterIndex5_0 + OuterIndex5_0 ≤ 0OuterIndex5_0OuterIndex5_0 ≤ 0Outer13_post + Outer13_post ≤ 0Outer13_postOuter13_post ≤ 0Outer13_0 + Outer13_0 ≤ 0Outer13_0Outer13_0 ≤ 0InnerIndex9_post + InnerIndex9_post ≤ 0InnerIndex9_postInnerIndex9_post ≤ 0InnerIndex9_0 + InnerIndex9_0 ≤ 0InnerIndex9_0InnerIndex9_0 ≤ 0InnerIndex6_post + InnerIndex6_post ≤ 0InnerIndex6_postInnerIndex6_post ≤ 0InnerIndex6_0 + InnerIndex6_0 ≤ 0InnerIndex6_0InnerIndex6_0 ≤ 0Inner14_post + Inner14_post ≤ 0Inner14_postInner14_post ≤ 0Inner14_0 + Inner14_0 ≤ 0Inner14_0Inner14_0 ≤ 0Index15_post + Index15_post ≤ 0Index15_postIndex15_post ≤ 0Index15_0 + Index15_0 ≤ 0Index15_0Index15_0 ≤ 0

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

8 52 8_var_snapshot: ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0ret_RandomInteger17_postret_RandomInteger17_post ≤ 0ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0ret_RandomInteger17_0ret_RandomInteger17_0 ≤ 0ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0ret_RandomInteger16_postret_RandomInteger16_post ≤ 0ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0ret_RandomInteger16_0ret_RandomInteger16_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0OuterIndex8_post + OuterIndex8_post ≤ 0OuterIndex8_postOuterIndex8_post ≤ 0OuterIndex8_0 + OuterIndex8_0 ≤ 0OuterIndex8_0OuterIndex8_0 ≤ 0OuterIndex5_post + OuterIndex5_post ≤ 0OuterIndex5_postOuterIndex5_post ≤ 0OuterIndex5_0 + OuterIndex5_0 ≤ 0OuterIndex5_0OuterIndex5_0 ≤ 0Outer13_post + Outer13_post ≤ 0Outer13_postOuter13_post ≤ 0Outer13_0 + Outer13_0 ≤ 0Outer13_0Outer13_0 ≤ 0InnerIndex9_post + InnerIndex9_post ≤ 0InnerIndex9_postInnerIndex9_post ≤ 0InnerIndex9_0 + InnerIndex9_0 ≤ 0InnerIndex9_0InnerIndex9_0 ≤ 0InnerIndex6_post + InnerIndex6_post ≤ 0InnerIndex6_postInnerIndex6_post ≤ 0InnerIndex6_0 + InnerIndex6_0 ≤ 0InnerIndex6_0InnerIndex6_0 ≤ 0Inner14_post + Inner14_post ≤ 0Inner14_postInner14_post ≤ 0Inner14_0 + Inner14_0 ≤ 0Inner14_0Inner14_0 ≤ 0Index15_post + Index15_post ≤ 0Index15_postIndex15_post ≤ 0Index15_0 + Index15_0 ≤ 0Index15_0Index15_0 ≤ 0

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

10* 61 10: ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0ret_RandomInteger17_postret_RandomInteger17_post ≤ 0ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0ret_RandomInteger17_0ret_RandomInteger17_0 ≤ 0ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0ret_RandomInteger16_postret_RandomInteger16_post ≤ 0ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0ret_RandomInteger16_0ret_RandomInteger16_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0OuterIndex8_post + OuterIndex8_post ≤ 0OuterIndex8_postOuterIndex8_post ≤ 0OuterIndex8_0 + OuterIndex8_0 ≤ 0OuterIndex8_0OuterIndex8_0 ≤ 0OuterIndex5_post + OuterIndex5_post ≤ 0OuterIndex5_postOuterIndex5_post ≤ 0OuterIndex5_0 + OuterIndex5_0 ≤ 0OuterIndex5_0OuterIndex5_0 ≤ 0Outer13_post + Outer13_post ≤ 0Outer13_postOuter13_post ≤ 0Outer13_0 + Outer13_0 ≤ 0Outer13_0Outer13_0 ≤ 0InnerIndex9_post + InnerIndex9_post ≤ 0InnerIndex9_postInnerIndex9_post ≤ 0InnerIndex9_0 + InnerIndex9_0 ≤ 0InnerIndex9_0InnerIndex9_0 ≤ 0InnerIndex6_post + InnerIndex6_post ≤ 0InnerIndex6_postInnerIndex6_post ≤ 0InnerIndex6_0 + InnerIndex6_0 ≤ 0InnerIndex6_0InnerIndex6_0 ≤ 0Inner14_post + Inner14_post ≤ 0Inner14_postInner14_post ≤ 0Inner14_0 + Inner14_0 ≤ 0Inner14_0Inner14_0 ≤ 0Index15_post + Index15_post ≤ 0Index15_postIndex15_post ≤ 0Index15_0 + Index15_0 ≤ 0Index15_0Index15_0 ≤ 0

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

10 59 10_var_snapshot: ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0ret_RandomInteger17_postret_RandomInteger17_post ≤ 0ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0ret_RandomInteger17_0ret_RandomInteger17_0 ≤ 0ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0ret_RandomInteger16_postret_RandomInteger16_post ≤ 0ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0ret_RandomInteger16_0ret_RandomInteger16_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0OuterIndex8_post + OuterIndex8_post ≤ 0OuterIndex8_postOuterIndex8_post ≤ 0OuterIndex8_0 + OuterIndex8_0 ≤ 0OuterIndex8_0OuterIndex8_0 ≤ 0OuterIndex5_post + OuterIndex5_post ≤ 0OuterIndex5_postOuterIndex5_post ≤ 0OuterIndex5_0 + OuterIndex5_0 ≤ 0OuterIndex5_0OuterIndex5_0 ≤ 0Outer13_post + Outer13_post ≤ 0Outer13_postOuter13_post ≤ 0Outer13_0 + Outer13_0 ≤ 0Outer13_0Outer13_0 ≤ 0InnerIndex9_post + InnerIndex9_post ≤ 0InnerIndex9_postInnerIndex9_post ≤ 0InnerIndex9_0 + InnerIndex9_0 ≤ 0InnerIndex9_0InnerIndex9_0 ≤ 0InnerIndex6_post + InnerIndex6_post ≤ 0InnerIndex6_postInnerIndex6_post ≤ 0InnerIndex6_0 + InnerIndex6_0 ≤ 0InnerIndex6_0InnerIndex6_0 ≤ 0Inner14_post + Inner14_post ≤ 0Inner14_postInner14_post ≤ 0Inner14_0 + Inner14_0 ≤ 0Inner14_0Inner14_0 ≤ 0Index15_post + Index15_post ≤ 0Index15_postIndex15_post ≤ 0Index15_0 + Index15_0 ≤ 0Index15_0Index15_0 ≤ 0

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

13* 68 13: ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0ret_RandomInteger17_postret_RandomInteger17_post ≤ 0ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0ret_RandomInteger17_0ret_RandomInteger17_0 ≤ 0ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0ret_RandomInteger16_postret_RandomInteger16_post ≤ 0ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0ret_RandomInteger16_0ret_RandomInteger16_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0OuterIndex8_post + OuterIndex8_post ≤ 0OuterIndex8_postOuterIndex8_post ≤ 0OuterIndex8_0 + OuterIndex8_0 ≤ 0OuterIndex8_0OuterIndex8_0 ≤ 0OuterIndex5_post + OuterIndex5_post ≤ 0OuterIndex5_postOuterIndex5_post ≤ 0OuterIndex5_0 + OuterIndex5_0 ≤ 0OuterIndex5_0OuterIndex5_0 ≤ 0Outer13_post + Outer13_post ≤ 0Outer13_postOuter13_post ≤ 0Outer13_0 + Outer13_0 ≤ 0Outer13_0Outer13_0 ≤ 0InnerIndex9_post + InnerIndex9_post ≤ 0InnerIndex9_postInnerIndex9_post ≤ 0InnerIndex9_0 + InnerIndex9_0 ≤ 0InnerIndex9_0InnerIndex9_0 ≤ 0InnerIndex6_post + InnerIndex6_post ≤ 0InnerIndex6_postInnerIndex6_post ≤ 0InnerIndex6_0 + InnerIndex6_0 ≤ 0InnerIndex6_0InnerIndex6_0 ≤ 0Inner14_post + Inner14_post ≤ 0Inner14_postInner14_post ≤ 0Inner14_0 + Inner14_0 ≤ 0Inner14_0Inner14_0 ≤ 0Index15_post + Index15_post ≤ 0Index15_postIndex15_post ≤ 0Index15_0 + Index15_0 ≤ 0Index15_0Index15_0 ≤ 0

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

13 66 13_var_snapshot: ret_RandomInteger17_post + ret_RandomInteger17_post ≤ 0ret_RandomInteger17_postret_RandomInteger17_post ≤ 0ret_RandomInteger17_0 + ret_RandomInteger17_0 ≤ 0ret_RandomInteger17_0ret_RandomInteger17_0 ≤ 0ret_RandomInteger16_post + ret_RandomInteger16_post ≤ 0ret_RandomInteger16_postret_RandomInteger16_post ≤ 0ret_RandomInteger16_0 + ret_RandomInteger16_0 ≤ 0ret_RandomInteger16_0ret_RandomInteger16_0 ≤ 0Seed_post + Seed_post ≤ 0Seed_postSeed_post ≤ 0Seed_0 + Seed_0 ≤ 0Seed_0Seed_0 ≤ 0OuterIndex8_post + OuterIndex8_post ≤ 0OuterIndex8_postOuterIndex8_post ≤ 0OuterIndex8_0 + OuterIndex8_0 ≤ 0OuterIndex8_0OuterIndex8_0 ≤ 0OuterIndex5_post + OuterIndex5_post ≤ 0OuterIndex5_postOuterIndex5_post ≤ 0OuterIndex5_0 + OuterIndex5_0 ≤ 0OuterIndex5_0OuterIndex5_0 ≤ 0Outer13_post + Outer13_post ≤ 0Outer13_postOuter13_post ≤ 0Outer13_0 + Outer13_0 ≤ 0Outer13_0Outer13_0 ≤ 0InnerIndex9_post + InnerIndex9_post ≤ 0InnerIndex9_postInnerIndex9_post ≤ 0InnerIndex9_0 + InnerIndex9_0 ≤ 0InnerIndex9_0InnerIndex9_0 ≤ 0InnerIndex6_post + InnerIndex6_post ≤ 0InnerIndex6_postInnerIndex6_post ≤ 0InnerIndex6_0 + InnerIndex6_0 ≤ 0InnerIndex6_0InnerIndex6_0 ≤ 0Inner14_post + Inner14_post ≤ 0Inner14_postInner14_post ≤ 0Inner14_0 + Inner14_0 ≤ 0Inner14_0Inner14_0 ≤ 0Index15_post + Index15_post ≤ 0Index15_postIndex15_post ≤ 0Index15_0 + Index15_0 ≤ 0Index15_0Index15_0 ≤ 0

### 18 SCC Decomposition

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

### 18.1 SCC Subproblem 1/3

Here we consider the SCC { 6, 7, 8, 9, 10, 11, 7_var_snapshot, 7*, 8_var_snapshot, 8*, 10_var_snapshot, 10* }.

### 18.1.1 Transition Removal

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

 6: −9⋅Outer13_0 7: −9⋅Outer13_0 8: −9⋅Outer13_0 9: −9⋅Outer13_0 10: 3 − 9⋅Outer13_0 11: 1 − 9⋅Outer13_0 7_var_snapshot: −9⋅Outer13_0 7*: −9⋅Outer13_0 8_var_snapshot: −9⋅Outer13_0 8*: −9⋅Outer13_0 10_var_snapshot: 2 − 9⋅Outer13_0 10*: 4 − 9⋅Outer13_0
Hints:
 45 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, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 47 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, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 52 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, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 54 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, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 59 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, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 61 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, 9, 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, 9, 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, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 5 lexWeak[ [0, 0, 0, 0, 0, 0, 9, 0, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 9, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 15 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, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 16 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, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 18.1.2 Transition Removal

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

 6: −5⋅Inner14_0 7: 3 − 5⋅Inner14_0 8: −5⋅Inner14_0 9: 1 − 5⋅Inner14_0 10: 20 − 5⋅Inner14_0 − OuterIndex8_0 11: −1 − 5⋅Inner14_0 − OuterIndex8_0 7_var_snapshot: 2 − 5⋅Inner14_0 7*: 4 − 5⋅Inner14_0 8_var_snapshot: −5⋅Inner14_0 8*: −5⋅Inner14_0 10_var_snapshot: −5⋅Inner14_0 − OuterIndex8_0 10*: 1 − 5⋅Inner14_0
Hints:
 45 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, 5, 0, 0, 0, 0] ] 47 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, 5, 0, 0, 0, 0] ] 52 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, 5, 0, 0, 0, 0] ] 54 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, 5, 0, 0, 0, 0] ] 59 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0] ] 61 lexWeak[ [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0] ] 3 lexWeak[ [0, 0, 0, 0, 0, 0, 5, 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] ] 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, 5] ] 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, 5, 0, 0, 0, 0] ] 6 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, 5] , [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] ] 10 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0] ] 15 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, 5, 0, 0, 0, 0] ] 16 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, 5, 0, 0, 0, 0] ]

### 18.1.3 Transition Removal

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

 6: −20 − 22⋅Index15_0 7: −60 − 22⋅Index15_0 8: −22⋅Index15_0 9: −20 − 22⋅Index15_0 − 4⋅OuterIndex8_0 10: −20 − 22⋅Index15_0 − 2⋅OuterIndex5_0 − 4⋅OuterIndex8_0 11: −1 − 22⋅Index15_0 − 4⋅OuterIndex5_0 − 4⋅OuterIndex8_0 7_var_snapshot: −22⋅Index15_0 − 4⋅OuterIndex8_0 7*: −40 − 22⋅Index15_0 8_var_snapshot: −22⋅Index15_0 8*: 1 − 22⋅Index15_0 10_var_snapshot: −22⋅Index15_0 − 4⋅OuterIndex5_0 − 4⋅OuterIndex8_0 10*: −22⋅Index15_0 − 2⋅OuterIndex5_0 − 4⋅OuterIndex8_0
Hints:
 45 lexWeak[ [0, 4, 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, 22] ] 47 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, 22] ] 52 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, 22] ] 54 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, 22] ] 59 lexWeak[ [2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 22] ] 61 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 22] ] 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, 22] ] 4 lexStrict[ [0, 0, 0, 0, 0, 0, 22, 0, 22, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 22, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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[ [2, 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, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 22] ] 10 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 22] ] 15 lexWeak[ [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, 22] ] 16 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, 22] ]

### 18.1.4 Transition Removal

We remove transitions 45, 47, 52, 54, 59, 61, 3, 5, 10, 15, 16 using the following ranking functions, which are bounded by −81.

 6: −20 + 4⋅OuterIndex8_0 7: 20 8: OuterIndex5_0 + 4⋅OuterIndex8_0 9: −20 10: −60 11: −5⋅OuterIndex8_0 7_var_snapshot: 0 7*: −40 + 4⋅OuterIndex8_0 8_var_snapshot: 4⋅OuterIndex8_0 8*: 2⋅OuterIndex5_0 + 4⋅OuterIndex8_0 10_var_snapshot: −80 10*: −40
Hints:
 45 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] ] 47 lexStrict[ [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, 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] ] 52 lexStrict[ [1, 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] , [1, 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] ] 54 lexStrict[ [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [2, 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] ] 59 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] ] 61 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] ] 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, 4, 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] ] 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] ] 10 lexStrict[ [0, 5, 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, 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] ] 16 lexStrict[ [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, 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] ]

### 18.1.5 Splitting Cut-Point Transitions

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

### 18.1.5.1 Cut-Point Subproblem 1/3

Here we consider cut-point transition 44.

### 18.1.5.1.1 Splitting Cut-Point Transitions

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

### 18.1.5.2 Cut-Point Subproblem 2/3

Here we consider cut-point transition 51.

### 18.1.5.2.1 Splitting Cut-Point Transitions

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

### 18.1.5.3 Cut-Point Subproblem 3/3

Here we consider cut-point transition 58.

### 18.1.5.3.1 Splitting Cut-Point Transitions

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

### 18.2 SCC Subproblem 2/3

Here we consider the SCC { 4, 5, 13, 14, 4_var_snapshot, 4*, 13_var_snapshot, 13* }.

### 18.2.1 Transition Removal

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

 4: 3 − 5⋅OuterIndex8_0 5: 1 − 5⋅OuterIndex8_0 13: −5⋅OuterIndex8_0 14: −5⋅OuterIndex8_0 4_var_snapshot: 2 − 5⋅OuterIndex8_0 4*: 4 − 5⋅OuterIndex8_0 13_var_snapshot: −5⋅OuterIndex8_0 13*: −5⋅OuterIndex8_0
Hints:
 38 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] ] 40 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] ] 66 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] ] 68 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] ] 2 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] ] 9 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] ] 11 lexWeak[ [0, 0, 0, 0, 0, 5, 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] ] 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, 5, 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, 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, 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] ]

### 18.2.2 Transition Removal

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

 4: −4⋅InnerIndex9_0 − 2⋅OuterIndex5_0 5: −1 − 4⋅InnerIndex9_0 − 2⋅OuterIndex5_0 13: 2 − 4⋅InnerIndex9_0 14: −4⋅InnerIndex9_0 4_var_snapshot: −1 − 4⋅InnerIndex9_0 − 2⋅OuterIndex5_0 4*: 20 − 4⋅InnerIndex9_0 − 2⋅OuterIndex5_0 13_var_snapshot: 1 − 4⋅InnerIndex9_0 13*: 3 − 4⋅InnerIndex9_0
Hints:
 38 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 40 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 66 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, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 68 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, 4, 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, 2, 0, 0, 0, 0, 0, 0, 0, 4, 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, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 11 lexWeak[ [2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 12 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 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, 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] ]

### 18.2.3 Transition Removal

We remove transitions 38, 40, 66, 68, 2, 9, 11 using the following ranking functions, which are bounded by −4.

 4: −2 5: −4 13: 1 + OuterIndex5_0 14: 0 4_var_snapshot: −3 4*: −1 13_var_snapshot: OuterIndex5_0 13*: 2 + OuterIndex5_0
Hints:
 38 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] ] 40 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] ] 66 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 68 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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] ] 9 lexStrict[ [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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] ]

### 18.2.4 Splitting Cut-Point Transitions

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

### 18.2.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 37.

### 18.2.4.1.1 Splitting Cut-Point Transitions

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

### 18.2.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 65.

### 18.2.4.2.1 Splitting Cut-Point Transitions

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

### 18.3 SCC Subproblem 3/3

Here we consider the SCC { 0, 1, 2, 3, 0_var_snapshot, 0*, 2_var_snapshot, 2* }.

### 18.3.1 Transition Removal

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

 0: 1 − 4⋅OuterIndex5_0 1: −4⋅OuterIndex5_0 2: −1 − 4⋅OuterIndex5_0 3: −1 − 4⋅OuterIndex5_0 0_var_snapshot: −4⋅OuterIndex5_0 0*: 2 − 4⋅OuterIndex5_0 2_var_snapshot: −1 − 4⋅OuterIndex5_0 2*: −1 − 4⋅OuterIndex5_0
Hints:
 24 lexWeak[ [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] ] 26 lexWeak[ [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] ] 31 lexWeak[ [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] ] 33 lexWeak[ [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 lexWeak[ [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] ] 1 lexWeak[ [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] ] 17 lexWeak[ [0, 0, 0, 0, 4, 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] ] 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, 4, 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, 4, 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] ]

### 18.3.2 Transition Removal

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

 0: −6⋅InnerIndex6_0 1: −2 − 6⋅InnerIndex6_0 2: 2 − 4⋅InnerIndex6_0 3: −4⋅InnerIndex6_0 0_var_snapshot: −1 − 6⋅InnerIndex6_0 0*: 20 − 6⋅InnerIndex6_0 2_var_snapshot: 1 − 4⋅InnerIndex6_0 2*: 3 − 4⋅InnerIndex6_0
Hints:
 24 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, 6, 0, 0, 0, 0, 0, 0, 0, 0] ] 26 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, 6, 0, 0, 0, 0, 0, 0, 0, 0] ] 31 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, 4, 0, 0, 0, 0, 0, 0, 0, 0] ] 33 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, 4, 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, 6, 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, 4, 0, 0, 0, 0, 0, 0, 0, 0] ] 17 lexWeak[ [0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0] ] 18 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 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, 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] ]

### 18.3.3 Transition Removal

We remove transitions 24, 26, 31, 33, 0, 1, 17 using the following ranking functions, which are bounded by −4.

 0: −2 1: −4 2: 2 3: 0 0_var_snapshot: −3 0*: −1 2_var_snapshot: 1 2*: 3
Hints:
 24 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] ] 26 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] ] 31 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] ] 33 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 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] ] 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] ] 17 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] ]

### 18.3.4 Splitting Cut-Point Transitions

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

### 18.3.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 23.

### 18.3.4.1.1 Splitting Cut-Point Transitions

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

### 18.3.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 30.

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