LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
2 99 2: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0
3 106 3: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0
6 113 6: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0
11 120 11: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0
13 127 13: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0
15 134 15: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0
20 141 20: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0
23 148 23: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0
25 155 25: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0
28 162 28: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0
33 169 33: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0
34 176 34: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0
37 183 37: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0
40 190 40: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0
41 197 41: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0
43 204 43: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 0, 16, 32, 46, 51, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 97, 98 using the following ranking functions, which are bounded by −63.

58: 0
57: 0
39: 0
40: 0
41: 0
42: 0
27: 0
28: 0
29: 0
30: 0
31: 0
32: 0
33: 0
36: 0
14: 0
15: 0
16: 0
17: 0
18: 0
19: 0
20: 0
22: 0
23: 0
24: 0
3: 0
4: 0
5: 0
6: 0
7: 0
8: 0
9: 0
10: 0
11: 0
12: 0
0: 0
2: 0
13: 0
21: 0
25: 0
26: 0
34: 0
35: 0
37: 0
38: 0
43: 0
44: 0
51: 0
52: 0
53: 0
54: 0
55: 0
56: 0
1: 0
50: 0
49: 0
48: 0
47: 0
45: 0
46: 0
58: −15
57: −16
39: −17
40: −17
41: −17
42: −17
40_var_snapshot: −17
40*: −17
41_var_snapshot: −17
41*: −17
27: −20
28: −20
29: −20
30: −20
31: −20
32: −20
33: −20
36: −20
28_var_snapshot: −20
28*: −20
33_var_snapshot: −20
33*: −20
14: −23
15: −23
16: −23
17: −23
18: −23
19: −23
20: −23
22: −23
23: −23
24: −23
15_var_snapshot: −23
15*: −23
20_var_snapshot: −23
20*: −23
23_var_snapshot: −23
23*: −23
3: −28
4: −28
5: −28
6: −28
7: −28
8: −28
9: −28
10: −28
11: −28
12: −28
3_var_snapshot: −28
3*: −28
6_var_snapshot: −28
6*: −28
11_var_snapshot: −28
11*: −28
2: −33
21: −33
25: −33
26: −33
34: −33
35: −33
37: −33
38: −33
43: −33
44: −33
51: −33
52: −33
53: −33
54: −33
55: −33
56: −33
0: −33
13: −33
2_var_snapshot: −33
2*: −33
13_var_snapshot: −33
13*: −33
25_var_snapshot: −33
25*: −33
34_var_snapshot: −33
34*: −33
37_var_snapshot: −33
37*: −33
43_var_snapshot: −33
43*: −33
1: −44
50: −45
49: −46
48: −47
47: −48
45: −49
46: −50

3 Location Addition

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

2* 102 2: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

4 Location Addition

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

2 100 2_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

5 Location Addition

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

3* 109 3: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

6 Location Addition

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

3 107 3_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

7 Location Addition

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

6* 116 6: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

8 Location Addition

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

6 114 6_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

9 Location Addition

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

11* 123 11: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

10 Location Addition

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

11 121 11_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

11 Location Addition

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

13* 130 13: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

12 Location Addition

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

13 128 13_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

13 Location Addition

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

15* 137 15: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

14 Location Addition

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

15 135 15_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

15 Location Addition

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

20* 144 20: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

16 Location Addition

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

20 142 20_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

17 Location Addition

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

23* 151 23: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

18 Location Addition

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

23 149 23_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

19 Location Addition

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

25* 158 25: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

20 Location Addition

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

25 156 25_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

21 Location Addition

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

28* 165 28: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

22 Location Addition

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

28 163 28_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

23 Location Addition

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

33* 172 33: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

24 Location Addition

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

33 170 33_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

25 Location Addition

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

34* 179 34: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

26 Location Addition

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

34 177 34_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

27 Location Addition

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

37* 186 37: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

28 Location Addition

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

37 184 37_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

29 Location Addition

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

40* 193 40: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

30 Location Addition

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

40 191 40_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

31 Location Addition

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

41* 200 41: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

32 Location Addition

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

41 198 41_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

33 Location Addition

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

43* 207 43: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

34 Location Addition

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

43 205 43_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0nl2_post + nl2_post ≤ 0nl2_postnl2_post ≤ 0nl2_0 + nl2_0 ≤ 0nl2_0nl2_0 ≤ 0nl1_post + nl1_post ≤ 0nl1_postnl1_post ≤ 0nl1_0 + nl1_0 ≤ 0nl1_0nl1_0 ≤ 0nk2_post + nk2_post ≤ 0nk2_postnk2_post ≤ 0nk2_0 + nk2_0 ≤ 0nk2_0nk2_0 ≤ 0nk1_post + nk1_post ≤ 0nk1_postnk1_post ≤ 0nk1_0 + nk1_0 ≤ 0nk1_0nk1_0 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0nj2_post + nj2_post ≤ 0nj2_postnj2_post ≤ 0nj2_0 + nj2_0 ≤ 0nj2_0nj2_0 ≤ 0nj1_post + nj1_post ≤ 0nj1_postnj1_post ≤ 0nj1_0 + nj1_0 ≤ 0nj1_0nj1_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0ni2_post + ni2_post ≤ 0ni2_postni2_post ≤ 0ni2_0 + ni2_0 ≤ 0ni2_0ni2_0 ≤ 0ni1_post + ni1_post ≤ 0ni1_postni1_post ≤ 0ni1_0 + ni1_0 ≤ 0ni1_0ni1_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0n2_post + n2_post ≤ 0n2_postn2_post ≤ 0n2_0 + n2_0 ≤ 0n2_0n2_0 ≤ 0bSquares_post + bSquares_post ≤ 0bSquares_postbSquares_post ≤ 0bSquares_0 + bSquares_0 ≤ 0bSquares_0bSquares_0 ≤ 0bRows_post + bRows_post ≤ 0bRows_postbRows_post ≤ 0bRows_0 + bRows_0 ≤ 0bRows_0bRows_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bCols_post + bCols_post ≤ 0bCols_postbCols_post ≤ 0bCols_0 + bCols_0 ≤ 0bCols_0bCols_0 ≤ 0

35 SCC Decomposition

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

35.1 SCC Subproblem 1/5

Here we consider the SCC { 2, 21, 25, 26, 34, 35, 37, 38, 43, 44, 51, 52, 53, 54, 55, 56, 0, 13, 2_var_snapshot, 2*, 13_var_snapshot, 13*, 25_var_snapshot, 25*, 34_var_snapshot, 34*, 37_var_snapshot, 37*, 43_var_snapshot, 43* }.

35.1.1 Transition Removal

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

2: 5⋅n_0 − 5⋅ni_0
21: 5⋅n_0 − 5⋅ni_0
25: 5⋅n_0 − 5⋅ni_0
26: 5⋅n_0 − 5⋅ni_0
34: 5⋅n_0 − 5⋅ni_0
35: 5⋅n_0 − 5⋅ni_0
37: 5⋅n_0 − 5⋅ni_0
38: 5⋅n_0 − 5⋅ni_0
43: 5⋅n_0 − 5⋅ni_0
44: 5⋅n_0 − 5⋅ni_0
51: 5⋅n_0 − 5⋅ni_0
52: 5⋅n_0 − 5⋅ni_0
53: 5⋅n_0 − 5⋅ni_0
54: 5⋅n_0 − 5⋅ni_0
55: 5⋅n_0 − 5⋅ni_0
56: 5⋅n_0 − 5⋅ni_0
0: 1 + 5⋅n_0 − 5⋅ni_0
13: 3 + 5⋅n_0 − 5⋅ni_0
2_var_snapshot: 5⋅n_0 − 5⋅ni_0
2*: 5⋅n_0 − 5⋅ni_0
13_var_snapshot: 2 + 5⋅n_0 − 5⋅ni_0
13*: 4 + 5⋅n_0 − 5⋅ni_0
25_var_snapshot: 5⋅n_0 − 5⋅ni_0
25*: 5⋅n_0 − 5⋅ni_0
34_var_snapshot: 5⋅n_0 − 5⋅ni_0
34*: 5⋅n_0 − 5⋅ni_0
37_var_snapshot: 5⋅n_0 − 5⋅ni_0
37*: 5⋅n_0 − 5⋅ni_0
43_var_snapshot: 5⋅n_0 − 5⋅ni_0
43*: 5⋅n_0 − 5⋅ni_0

35.1.2 Transition Removal

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

2: 2 + 11⋅n_0 − 11⋅nj_0
21: 11⋅n_0 − 11⋅nj_0
25: −7 + 11⋅n_0 − 11⋅nj_0
26: −7 + 11⋅n_0 − 11⋅nj_0
34: −7 + 11⋅n_0 − 11⋅nj_0
35: −7 + 11⋅n_0 − 11⋅nj_0
37: −7 + 11⋅n_0 − 11⋅nj_0
38: −7 + 11⋅n_0 − 11⋅nj_0
43: −7 + 11⋅n_0 − 11⋅nj_0
44: −7 + 11⋅n_0 − 11⋅nj_0
51: −7 + 11⋅n_0 − 11⋅nj_0
52: −7 + 11⋅n_0 − 11⋅nj_0
53: −7 + 11⋅n_0 − 11⋅nj_0
54: −7 + 11⋅n_0 − 11⋅nj_0
55: −7 + 11⋅n_0 − 11⋅nj_0
56: −7 + 11⋅n_0 − 11⋅nj_0
0: −4 + 11⋅n_0 − 11⋅nj_0
13: −2 + 11⋅n_0 − 11⋅nj_0
2_var_snapshot: 1 + 11⋅n_0 − 11⋅nj_0
2*: 3 + 11⋅n_0 − 11⋅nj_0
13_var_snapshot: −3 + 11⋅n_0 − 11⋅nj_0
13*: −1 + 11⋅n_0 − 11⋅nj_0
25_var_snapshot: −7 + 11⋅n_0 − 11⋅nj_0
25*: −7 + 11⋅n_0 − 11⋅nj_0
34_var_snapshot: −7 + 11⋅n_0 − 11⋅nj_0
34*: −7 + 11⋅n_0 − 11⋅nj_0
37_var_snapshot: −7 + 11⋅n_0 − 11⋅nj_0
37*: −7 + 11⋅n_0 − 11⋅nj_0
43_var_snapshot: −7 + 11⋅n_0 − 11⋅nj_0
43*: −7 + 11⋅n_0 − 11⋅nj_0

35.1.3 Transition Removal

We remove transitions 100, 102, 128, 130, 18, 29, 92, 94 using the following ranking functions, which are bounded by −8.

2: −2
21: −4
25: 0
26: 0
34: 0
35: 0
37: 0
38: 0
43: 0
44: 0
51: 0
52: 0
53: 0
54: 0
55: 0
56: 0
0: −8
13: −6
2_var_snapshot: −3
2*: −1
13_var_snapshot: −7
13*: −5
25_var_snapshot: 0
25*: 0
34_var_snapshot: 0
34*: 0
37_var_snapshot: 0
37*: 0
43_var_snapshot: 0
43*: 0

35.1.4 Transition Removal

We remove transition 93 using the following ranking functions, which are bounded by 19.

2: 0
21: 0
25: 10 + 12⋅n_0 − 12⋅nk1_0
26: 8 + 12⋅n_0 − 12⋅nk1_0
34: 12⋅n_0 − 12⋅nk1_0
35: 12⋅n_0 − 12⋅nk1_0
37: 12⋅n_0 − 12⋅nk1_0
38: 12⋅n_0 − 12⋅nk1_0
43: 12⋅n_0 − 12⋅nk1_0
44: 12⋅n_0 − 12⋅nk1_0
51: 12⋅n_0 − 12⋅nk1_0
52: 12⋅n_0 − 12⋅nk1_0
53: 12⋅n_0 − 12⋅nk1_0
54: 12⋅n_0 − 12⋅nk1_0
55: 12⋅n_0 − 12⋅nk1_0
56: 12⋅n_0 − 12⋅nk1_0
0: 0
13: 0
2_var_snapshot: 0
2*: 0
13_var_snapshot: 0
13*: 0
25_var_snapshot: 9 + 12⋅n_0 − 12⋅nk1_0
25*: 11 + 12⋅n_0 − 12⋅nk1_0
34_var_snapshot: 12⋅n_0 − 12⋅nk1_0
34*: 12⋅n_0 − 12⋅nk1_0
37_var_snapshot: 12⋅n_0 − 12⋅nk1_0
37*: 12⋅n_0 − 12⋅nk1_0
43_var_snapshot: 12⋅n_0 − 12⋅nk1_0
43*: 12⋅n_0 − 12⋅nk1_0

35.1.5 Transition Removal

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

2: 0
21: 0
25: −1 + 5⋅n_0 − 5⋅nl1_0
26: −3 + 5⋅n_0 − 5⋅nl1_0
34: 2 + 5⋅n_0 − 5⋅nl1_0
35: 5⋅n_0 − 5⋅nl1_0
37: −1 + 5⋅n_0 − 5⋅nl1_0
38: −1 + 5⋅n_0 − 5⋅nl1_0
43: −1 + 5⋅n_0 − 5⋅nl1_0
44: −1 + 5⋅n_0 − 5⋅nl1_0
51: −1 + 5⋅n_0 − 5⋅nl1_0
52: −1 + 5⋅n_0 − 5⋅nl1_0
53: −1 + 5⋅n_0 − 5⋅nl1_0
54: −1 + 5⋅n_0 − 5⋅nl1_0
55: −1 + 5⋅n_0 − 5⋅nl1_0
56: −1 + 5⋅n_0 − 5⋅nl1_0
0: 0
13: 0
2_var_snapshot: 0
2*: 0
13_var_snapshot: 0
13*: 0
25_var_snapshot: −2 + 5⋅n_0 − 5⋅nl1_0
25*: 5⋅n_0 − 5⋅nl1_0
34_var_snapshot: 1 + 5⋅n_0 − 5⋅nl1_0
34*: 3 + 5⋅n_0 − 5⋅nl1_0
37_var_snapshot: −1 + 5⋅n_0 − 5⋅nl1_0
37*: −1 + 5⋅n_0 − 5⋅nl1_0
43_var_snapshot: −1 + 5⋅n_0 − 5⋅nl1_0
43*: −1 + 5⋅n_0 − 5⋅nl1_0

35.1.6 Transition Removal

We remove transitions 156, 158, 177, 179, 34, 45, 87, 90 using the following ranking functions, which are bounded by −8.

2: 0
21: 0
25: −6
26: −8
34: −2
35: −4
37: 0
38: 0
43: 0
44: 0
51: 0
52: 0
53: 0
54: 0
55: 0
56: 0
0: 0
13: 0
2_var_snapshot: 0
2*: 0
13_var_snapshot: 0
13*: 0
25_var_snapshot: −7
25*: −5
34_var_snapshot: −3
34*: −1
37_var_snapshot: 0
37*: 0
43_var_snapshot: 0
43*: 0

35.1.7 Transition Removal

We remove transition 88 using the following ranking functions, which are bounded by 19.

2: 0
21: 0
25: 0
26: 0
34: 0
35: 0
37: 10 + 12⋅n_0 − 12⋅nk2_0
38: 8 + 12⋅n_0 − 12⋅nk2_0
43: 12⋅n_0 − 12⋅nk2_0
44: 12⋅n_0 − 12⋅nk2_0
51: 12⋅n_0 − 12⋅nk2_0
52: 12⋅n_0 − 12⋅nk2_0
53: 12⋅n_0 − 12⋅nk2_0
54: 12⋅n_0 − 12⋅nk2_0
55: 12⋅n_0 − 12⋅nk2_0
56: 12⋅n_0 − 12⋅nk2_0
0: 0
13: 0
2_var_snapshot: 0
2*: 0
13_var_snapshot: 0
13*: 0
25_var_snapshot: 0
25*: 0
34_var_snapshot: 0
34*: 0
37_var_snapshot: 9 + 12⋅n_0 − 12⋅nk2_0
37*: 11 + 12⋅n_0 − 12⋅nk2_0
43_var_snapshot: 12⋅n_0 − 12⋅nk2_0
43*: 12⋅n_0 − 12⋅nk2_0

35.1.8 Transition Removal

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

2: 0
21: 0
25: 0
26: 0
34: 0
35: 0
37: −2 + 8⋅n_0 − 8⋅nl2_0
38: −4 + 8⋅n_0 − 8⋅nl2_0
43: 1 + 8⋅n_0 − 8⋅nl2_0
44: 8⋅n_0 − 8⋅nl2_0
51: −5 + 8⋅n_0 − 8⋅nl2_0
52: −4 + 8⋅n_0 − 8⋅nl2_0
53: −3 + 8⋅n_0 − 8⋅nl2_0
54: −2 + 8⋅n_0 − 8⋅nl2_0
55: −2 + 8⋅n_0 − 8⋅nl2_0
56: −1 + 8⋅n_0 − 8⋅nl2_0
0: 0
13: 0
2_var_snapshot: 0
2*: 0
13_var_snapshot: 0
13*: 0
25_var_snapshot: 0
25*: 0
34_var_snapshot: 0
34*: 0
37_var_snapshot: −3 + 8⋅n_0 − 8⋅nl2_0
37*: −1 + 8⋅n_0 − 8⋅nl2_0
43_var_snapshot: 1 + 8⋅n_0 − 8⋅nl2_0
43*: 2 + 8⋅n_0 − 8⋅nl2_0

35.1.9 Transition Removal

We remove transitions 184, 186, 205, 207, 48, 53, 73, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85 using the following ranking functions, which are bounded by −11.

2: 0
21: 0
25: 0
26: 0
34: 0
35: 0
37: −9
38: −11
43: −5
44: −7
51: −3
52: −2
53: −1
54: 0
55: 1
56: 2
0: 0
13: 0
2_var_snapshot: 0
2*: 0
13_var_snapshot: 0
13*: 0
25_var_snapshot: 0
25*: 0
34_var_snapshot: 0
34*: 0
37_var_snapshot: −10
37*: −8
43_var_snapshot: −6
43*: −4

35.1.10 Splitting Cut-Point Transitions

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

35.1.10.1 Cut-Point Subproblem 1/6

Here we consider cut-point transition 99.

35.1.10.1.1 Splitting Cut-Point Transitions

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

35.1.10.2 Cut-Point Subproblem 2/6

Here we consider cut-point transition 127.

35.1.10.2.1 Splitting Cut-Point Transitions

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

35.1.10.3 Cut-Point Subproblem 3/6

Here we consider cut-point transition 155.

35.1.10.3.1 Splitting Cut-Point Transitions

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

35.1.10.4 Cut-Point Subproblem 4/6

Here we consider cut-point transition 176.

35.1.10.4.1 Splitting Cut-Point Transitions

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

35.1.10.5 Cut-Point Subproblem 5/6

Here we consider cut-point transition 183.

35.1.10.5.1 Splitting Cut-Point Transitions

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

35.1.10.6 Cut-Point Subproblem 6/6

Here we consider cut-point transition 204.

35.1.10.6.1 Splitting Cut-Point Transitions

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

35.2 SCC Subproblem 2/5

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

35.2.1 Transition Removal

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

3: −2 + 5⋅n2_0 − 5⋅nj_0
4: −2 + 5⋅n2_0 − 5⋅nj_0
5: −2 + 5⋅n2_0 − 5⋅nj_0
6: −2 + 5⋅n2_0 − 5⋅nj_0
7: −2 + 5⋅n2_0 − 5⋅nj_0
8: −2 + 5⋅n2_0 − 5⋅nj_0
9: −2 + 5⋅n2_0 − 5⋅nj_0
10: −2 + 5⋅n2_0 − 5⋅nj_0
11: 1 + 5⋅n2_0 − 5⋅nj_0
12: −1 + 5⋅n2_0 − 5⋅nj_0
3_var_snapshot: −2 + 5⋅n2_0 − 5⋅nj_0
3*: −2 + 5⋅n2_0 − 5⋅nj_0
6_var_snapshot: −2 + 5⋅n2_0 − 5⋅nj_0
6*: −2 + 5⋅n2_0 − 5⋅nj_0
11_var_snapshot: 5⋅n2_0 − 5⋅nj_0
11*: 2 + 5⋅n2_0 − 5⋅nj_0

35.2.2 Transition Removal

We remove transitions 121, 123, 13, 96 using the following ranking functions, which are bounded by −4.

3: 0
4: 0
5: 0
6: 0
7: 0
8: 0
9: 0
10: 0
11: −2
12: −4
3_var_snapshot: 0
3*: 0
6_var_snapshot: 0
6*: 0
11_var_snapshot: −3
11*: −1

35.2.3 Transition Removal

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

3: 10 + 12⋅n2_0 − 12⋅ni1_0
4: 8 + 12⋅n2_0 − 12⋅ni1_0
5: 12⋅n2_0 − 12⋅ni1_0
6: 12⋅n2_0 − 12⋅ni1_0
7: 12⋅n2_0 − 12⋅ni1_0
8: 12⋅n2_0 − 12⋅ni1_0
9: 12⋅n2_0 − 12⋅ni1_0
10: 12⋅n2_0 − 12⋅ni1_0
11: 0
12: 0
3_var_snapshot: 9 + 12⋅n2_0 − 12⋅ni1_0
3*: 11 + 12⋅n2_0 − 12⋅ni1_0
6_var_snapshot: 12⋅n2_0 − 12⋅ni1_0
6*: 12⋅n2_0 − 12⋅ni1_0
11_var_snapshot: 0
11*: 0

35.2.4 Transition Removal

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

3: −3 + 11⋅n2_0 − 11⋅ni2_0
4: −5 + 11⋅n2_0 − 11⋅ni2_0
5: −8 + 11⋅n2_0 − 11⋅ni2_0
6: 1 + 11⋅n2_0 − 11⋅ni2_0
7: −7 + 11⋅n2_0 − 11⋅ni2_0
8: −6 + 11⋅n2_0 − 11⋅ni2_0
9: −5 + 11⋅n2_0 − 11⋅ni2_0
10: −1 + 11⋅n2_0 − 11⋅ni2_0
11: 0
12: 0
3_var_snapshot: −4 + 11⋅n2_0 − 11⋅ni2_0
3*: −2 + 11⋅n2_0 − 11⋅ni2_0
6_var_snapshot: 11⋅n2_0 − 11⋅ni2_0
6*: 2 + 11⋅n2_0 − 11⋅ni2_0
11_var_snapshot: 0
11*: 0

35.2.5 Transition Removal

We remove transitions 107, 109, 114, 116, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 15 using the following ranking functions, which are bounded by −10.

3: −8
4: −10
5: −2
6: −4
7: −1
8: 0
9: 1
10: −6
11: 0
12: 0
3_var_snapshot: −9
3*: −7
6_var_snapshot: −5
6*: −3
11_var_snapshot: 0
11*: 0

35.2.6 Splitting Cut-Point Transitions

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

35.2.6.1 Cut-Point Subproblem 1/3

Here we consider cut-point transition 106.

35.2.6.1.1 Splitting Cut-Point Transitions

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

35.2.6.2 Cut-Point Subproblem 2/3

Here we consider cut-point transition 113.

35.2.6.2.1 Splitting Cut-Point Transitions

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

35.2.6.3 Cut-Point Subproblem 3/3

Here we consider cut-point transition 120.

35.2.6.3.1 Splitting Cut-Point Transitions

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

35.3 SCC Subproblem 3/5

Here we consider the SCC { 14, 15, 16, 17, 18, 19, 20, 22, 23, 24, 15_var_snapshot, 15*, 20_var_snapshot, 20*, 23_var_snapshot, 23* }.

35.3.1 Transition Removal

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

14: 5⋅n2_0 − 5⋅ni_0
15: 5⋅n2_0 − 5⋅ni_0
16: 5⋅n2_0 − 5⋅ni_0
17: 5⋅n2_0 − 5⋅ni_0
18: 5⋅n2_0 − 5⋅ni_0
19: 5⋅n2_0 − 5⋅ni_0
20: 5⋅n2_0 − 5⋅ni_0
22: 5⋅n2_0 − 5⋅ni_0
23: 3 + 5⋅n2_0 − 5⋅ni_0
24: 1 + 5⋅n2_0 − 5⋅ni_0
15_var_snapshot: 5⋅n2_0 − 5⋅ni_0
15*: 5⋅n2_0 − 5⋅ni_0
20_var_snapshot: 5⋅n2_0 − 5⋅ni_0
20*: 5⋅n2_0 − 5⋅ni_0
23_var_snapshot: 2 + 5⋅n2_0 − 5⋅ni_0
23*: 4 + 5⋅n2_0 − 5⋅ni_0

35.3.2 Transition Removal

We remove transition 31 using the following ranking functions, which are bounded by 10.

14: 5⋅n2_0 − 5⋅nj1_0
15: 5⋅n2_0 − 5⋅nj1_0
16: 5⋅n2_0 − 5⋅nj1_0
17: 5⋅n2_0 − 5⋅nj1_0
18: 5⋅n2_0 − 5⋅nj1_0
19: 5⋅n2_0 − 5⋅nj1_0
20: 3 + 5⋅n2_0 − 5⋅nj1_0
22: 1 + 5⋅n2_0 − 5⋅nj1_0
23: −1 + 5⋅n2_0 − 5⋅nj1_0
24: −3 + 5⋅n2_0 − 5⋅nj1_0
15_var_snapshot: 5⋅n2_0 − 5⋅nj1_0
15*: 5⋅n2_0 − 5⋅nj1_0
20_var_snapshot: 2 + 5⋅n2_0 − 5⋅nj1_0
20*: 4 + 5⋅n2_0 − 5⋅nj1_0
23_var_snapshot: −2 + 5⋅n2_0 − 5⋅nj1_0
23*: 5⋅n2_0 − 5⋅nj1_0

35.3.3 Transition Removal

We remove transition 28 using the following ranking functions, which are bounded by 11.

14: −10 + 13⋅n2_0 − 13⋅nj2_0
15: 1 + 13⋅n2_0 − 13⋅nj2_0
16: −9 + 13⋅n2_0 − 13⋅nj2_0
17: −8 + 13⋅n2_0 − 13⋅nj2_0
18: −7 + 13⋅n2_0 − 13⋅nj2_0
19: −1 + 13⋅n2_0 − 13⋅nj2_0
20: −3 + 13⋅n2_0 − 13⋅nj2_0
22: −5 + 13⋅n2_0 − 13⋅nj2_0
23: −7 + 13⋅n2_0 − 13⋅nj2_0
24: −8 + 13⋅n2_0 − 13⋅nj2_0
15_var_snapshot: 13⋅n2_0 − 13⋅nj2_0
15*: 2 + 13⋅n2_0 − 13⋅nj2_0
20_var_snapshot: −4 + 13⋅n2_0 − 13⋅nj2_0
20*: −2 + 13⋅n2_0 − 13⋅nj2_0
23_var_snapshot: −7 + 13⋅n2_0 − 13⋅nj2_0
23*: −6 + 13⋅n2_0 − 13⋅nj2_0

35.3.4 Transition Removal

We remove transitions 135, 137, 142, 144, 149, 151, 19, 20, 21, 22, 23, 24, 25, 26, 27, 30, 72, 74, 89 using the following ranking functions, which are bounded by −9.

14: 3
15: 1
16: 4
17: 5
18: 6
19: −1
20: −3
22: −5
23: −7
24: −9
15_var_snapshot: 0
15*: 2
20_var_snapshot: −4
20*: −2
23_var_snapshot: −8
23*: −6

35.3.5 Splitting Cut-Point Transitions

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

35.3.5.1 Cut-Point Subproblem 1/3

Here we consider cut-point transition 134.

35.3.5.1.1 Splitting Cut-Point Transitions

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

35.3.5.2 Cut-Point Subproblem 2/3

Here we consider cut-point transition 141.

35.3.5.2.1 Splitting Cut-Point Transitions

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

35.3.5.3 Cut-Point Subproblem 3/3

Here we consider cut-point transition 148.

35.3.5.3.1 Splitting Cut-Point Transitions

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

35.4 SCC Subproblem 4/5

Here we consider the SCC { 27, 28, 29, 30, 31, 32, 33, 36, 28_var_snapshot, 28*, 33_var_snapshot, 33* }.

35.4.1 Transition Removal

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

27: 5⋅n2_0 − 5⋅ni_0
28: 5⋅n2_0 − 5⋅ni_0
29: 5⋅n2_0 − 5⋅ni_0
30: 5⋅n2_0 − 5⋅ni_0
31: 5⋅n2_0 − 5⋅ni_0
32: 5⋅n2_0 − 5⋅ni_0
33: 3 + 5⋅n2_0 − 5⋅ni_0
36: 1 + 5⋅n2_0 − 5⋅ni_0
28_var_snapshot: 5⋅n2_0 − 5⋅ni_0
28*: 5⋅n2_0 − 5⋅ni_0
33_var_snapshot: 2 + 5⋅n2_0 − 5⋅ni_0
33*: 4 + 5⋅n2_0 − 5⋅ni_0

35.4.2 Transition Removal

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

27: −5 + 8⋅n2_0 − 8⋅nj_0
28: 1 + 8⋅n2_0 − 8⋅nj_0
29: −4 + 8⋅n2_0 − 8⋅nj_0
30: −3 + 8⋅n2_0 − 8⋅nj_0
31: −2 + 8⋅n2_0 − 8⋅nj_0
32: −1 + 8⋅n2_0 − 8⋅nj_0
33: −3 + 8⋅n2_0 − 8⋅nj_0
36: −5 + 8⋅n2_0 − 8⋅nj_0
28_var_snapshot: 8⋅n2_0 − 8⋅nj_0
28*: 2 + 8⋅n2_0 − 8⋅nj_0
33_var_snapshot: −4 + 8⋅n2_0 − 8⋅nj_0
33*: −2 + 8⋅n2_0 − 8⋅nj_0

35.4.3 Transition Removal

We remove transitions 163, 165, 170, 172, 35, 36, 37, 38, 39, 40, 41, 42, 43, 56, 57 using the following ranking functions, which are bounded by −5.

27: 3
28: 1
29: 4
30: 5
31: 6
32: −1
33: −3
36: −5
28_var_snapshot: 0
28*: 2
33_var_snapshot: −4
33*: −2

35.4.4 Splitting Cut-Point Transitions

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

35.4.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 162.

35.4.4.1.1 Splitting Cut-Point Transitions

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

35.4.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 169.

35.4.4.2.1 Splitting Cut-Point Transitions

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

35.5 SCC Subproblem 5/5

Here we consider the SCC { 39, 40, 41, 42, 40_var_snapshot, 40*, 41_var_snapshot, 41* }.

35.5.1 Transition Removal

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

39: 5⋅n2_0 − 5⋅ni_0
40: 3 + 5⋅n2_0 − 5⋅ni_0
41: 5⋅n2_0 − 5⋅ni_0
42: 1 + 5⋅n2_0 − 5⋅ni_0
40_var_snapshot: 2 + 5⋅n2_0 − 5⋅ni_0
40*: 4 + 5⋅n2_0 − 5⋅ni_0
41_var_snapshot: 5⋅n2_0 − 5⋅ni_0
41*: 5⋅n2_0 − 5⋅ni_0

35.5.2 Transition Removal

We remove transition 50 using the following ranking functions, which are bounded by 2.

39: −1 + 4⋅n2_0 − 4⋅nj_0
40: −3 + 4⋅n2_0 − 4⋅nj_0
41: 1 + 4⋅n2_0 − 4⋅nj_0
42: −5 + 4⋅n2_0 − 4⋅nj_0
40_var_snapshot: −4 + 4⋅n2_0 − 4⋅nj_0
40*: −2 + 4⋅n2_0 − 4⋅nj_0
41_var_snapshot: 4⋅n2_0 − 4⋅nj_0
41*: 2 + 4⋅n2_0 − 4⋅nj_0

35.5.3 Transition Removal

We remove transitions 191, 193, 198, 200, 49, 54, 55 using the following ranking functions, which are bounded by −5.

39: −1
40: −3
41: 1
42: −5
40_var_snapshot: −4
40*: −2
41_var_snapshot: 0
41*: 2

35.5.4 Splitting Cut-Point Transitions

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

35.5.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 190.

35.5.4.1.1 Splitting Cut-Point Transitions

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

35.5.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 197.

35.5.4.2.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert