# 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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − Index15_0 + ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ 1 + Index15_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − Inner14_0 + ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ 1 + Inner14_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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: − Outer13_0 + ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ 1 + Outer13_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − InnerIndex9_0 + ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ 1 + InnerIndex9_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − OuterIndex8_0 + ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ 1 + OuterIndex8_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − InnerIndex6_0 + ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ 1 + InnerIndex6_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − OuterIndex5_0 + ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ 1 + OuterIndex5_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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

### 1 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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_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.

### 2 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, 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, 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, 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] ] 0 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 1 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 2 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 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, 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, 0] ] 12 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 14 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 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, 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, 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, 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, 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, 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, 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, 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 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_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 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_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 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_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 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_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 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_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 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_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 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_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 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_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 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_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 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_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 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_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 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_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 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_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 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_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

### 17 SCC Decomposition

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

### 17.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* }.

### 17.1.1 Transition Removal

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

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

### 17.1.2 Transition Removal

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

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

### 17.1.3 Transition Removal

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

 6: −1 − 3⋅Index15_0 + 3⋅___const_20_0 7: −3 − 3⋅Index15_0 + 3⋅___const_20_0 8: −3⋅Index15_0 + 3⋅___const_20_0 9: −4 − 3⋅Index15_0 + 3⋅___const_20_0 10: −6 − 3⋅Index15_0 + 3⋅___const_20_0 11: −8 − 3⋅Index15_0 + 3⋅___const_20_0 7_var_snapshot: −4 − 3⋅Index15_0 + 3⋅___const_20_0 7*: −2 − 3⋅Index15_0 + 3⋅___const_20_0 8_var_snapshot: −3⋅Index15_0 + 3⋅___const_20_0 8*: 1 − 3⋅Index15_0 + 3⋅___const_20_0 10_var_snapshot: −7 − 3⋅Index15_0 + 3⋅___const_20_0 10*: −5 − 3⋅Index15_0 + 3⋅___const_20_0
Hints:
 45 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3] ] 47 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3] ] 52 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3] ] 54 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3] ] 59 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3] ] 61 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3] ] 3 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3] ] 4 lexStrict[ [0, 0, 0, 0, 3, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 5 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3] ] 10 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3] ] 15 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3] ] 16 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3] ]

### 17.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 −9.

 6: −1 7: −3 8: 1 9: −5 10: −7 11: −9 7_var_snapshot: −4 7*: −2 8_var_snapshot: 0 8*: 2 10_var_snapshot: −8 10*: −6
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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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.1.5 Splitting Cut-Point Transitions

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

### 17.1.5.1 Cut-Point Subproblem 1/3

Here we consider cut-point transition 44.

### 17.1.5.1.1 Splitting Cut-Point Transitions

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

### 17.1.5.2 Cut-Point Subproblem 2/3

Here we consider cut-point transition 51.

### 17.1.5.2.1 Splitting Cut-Point Transitions

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

### 17.1.5.3 Cut-Point Subproblem 3/3

Here we consider cut-point transition 58.

### 17.1.5.3.1 Splitting Cut-Point Transitions

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

### 17.2 SCC Subproblem 2/3

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

### 17.2.1 Transition Removal

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

 4: 1 − 7⋅OuterIndex8_0 + 7⋅___const_20_0 5: −7⋅OuterIndex8_0 + 7⋅___const_20_0 13: −4 − 7⋅OuterIndex8_0 + 7⋅___const_20_0 14: −4 − 7⋅OuterIndex8_0 + 7⋅___const_20_0 4_var_snapshot: −7⋅OuterIndex8_0 + 7⋅___const_20_0 4*: 2 − 7⋅OuterIndex8_0 + 7⋅___const_20_0 13_var_snapshot: −4 − 7⋅OuterIndex8_0 + 7⋅___const_20_0 13*: −4 − 7⋅OuterIndex8_0 + 7⋅___const_20_0
Hints:
 38 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 7, 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, 7, 0, 0, 0, 0, 0, 0, 0, 0, 7, 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, 7, 0, 0, 0, 0, 0, 0, 0, 0, 7, 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, 7, 0, 0, 0, 0, 0, 0, 0, 0, 7, 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, 7, 0, 0, 0, 0, 0, 0, 0, 0, 7, 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, 7, 0, 0, 0, 0, 0, 0, 0, 0, 7, 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, 7, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 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, 7, 0, 0, 0, 0, 7, 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, 7, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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.2.2 Transition Removal

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

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

### 17.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: 2 14: 0 4_var_snapshot: −3 4*: −1 13_var_snapshot: 1 13*: 3
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, 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, 0, 0] ] 66 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] ] 68 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] ] 2 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 9 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 11 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 17.2.4 Splitting Cut-Point Transitions

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

### 17.2.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 37.

### 17.2.4.1.1 Splitting Cut-Point Transitions

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

### 17.2.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 65.

### 17.2.4.2.1 Splitting Cut-Point Transitions

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

### 17.3 SCC Subproblem 3/3

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

### 17.3.1 Transition Removal

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

 0: 1 − 7⋅OuterIndex5_0 + 7⋅___const_20_0 1: −7⋅OuterIndex5_0 + 7⋅___const_20_0 2: −4 − 7⋅OuterIndex5_0 + 7⋅___const_20_0 3: −4 − 7⋅OuterIndex5_0 + 7⋅___const_20_0 0_var_snapshot: −7⋅OuterIndex5_0 + 7⋅___const_20_0 0*: 2 − 7⋅OuterIndex5_0 + 7⋅___const_20_0 2_var_snapshot: −4 − 7⋅OuterIndex5_0 + 7⋅___const_20_0 2*: −4 − 7⋅OuterIndex5_0 + 7⋅___const_20_0
Hints:
 24 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 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, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 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, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 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, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 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, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 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, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 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, 7, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 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, 7, 0, 0, 0, 0, 0, 0, 0, 0, 7, 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, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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.3.2 Transition Removal

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

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

### 17.3.3 Transition Removal

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

 0: −1 1: −3 2: 3 3: 1 0_var_snapshot: −2 0*: 0 2_var_snapshot: 2 2*: 4
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, 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, 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, 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, 0, 0, 0] ] 0 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 1 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 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, 0, 0, 0, 0] ]

### 17.3.4 Splitting Cut-Point Transitions

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

### 17.3.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 23.

### 17.3.4.1.1 Splitting Cut-Point Transitions

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

### 17.3.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 30.

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