LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
2 103 2: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0
5 110 5: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0
8 117 8: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0
10 124 10: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0
13 131 13: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0
18 138 18: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0
19 145 19: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0
30 152 30: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0
37 159 37: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0
38 166 38: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 11, 13, 14, 16, 17, 18, 19, 20, 21, 22, 25, 26, 27, 28, 29, 30, 31, 32, 33, 47, 58, 61, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 98, 101, 102 using the following ranking functions, which are bounded by −81.

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

3 Location Addition

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

2* 106 2: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

4 Location Addition

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

2 104 2_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

5 Location Addition

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

5* 113 5: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

6 Location Addition

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

5 111 5_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

7 Location Addition

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

8* 120 8: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

8 Location Addition

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

8 118 8_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

9 Location Addition

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

10* 127 10: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

10 Location Addition

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

10 125 10_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

11 Location Addition

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

13* 134 13: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

12 Location Addition

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

13 132 13_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

13 Location Addition

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

18* 141 18: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

14 Location Addition

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

18 139 18_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

15 Location Addition

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

19* 148 19: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

16 Location Addition

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

19 146 19_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

17 Location Addition

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

30* 155 30: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

18 Location Addition

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

30 153 30_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

19 Location Addition

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

37* 162 37: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

20 Location Addition

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

37 160 37_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

21 Location Addition

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

38* 169 38: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

22 Location Addition

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

38 167 38_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 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 ≤ 0nj_post + nj_post ≤ 0nj_postnj_post ≤ 0nj_0 + nj_0 ≤ 0nj_0nj_0 ≤ 0ni_post + ni_post ≤ 0ni_postni_post ≤ 0ni_0 + ni_0 ≤ 0ni_0ni_0 ≤ 0nSum_post + nSum_post ≤ 0nSum_postnSum_post ≤ 0nSum_0 + nSum_0 ≤ 0nSum_0nSum_0 ≤ 0nSumRow_post + nSumRow_post ≤ 0nSumRow_postnSumRow_post ≤ 0nSumRow_0 + nSumRow_0 ≤ 0nSumRow_0nSumRow_0 ≤ 0nSumDiag2_post + nSumDiag2_post ≤ 0nSumDiag2_postnSumDiag2_post ≤ 0nSumDiag2_0 + nSumDiag2_0 ≤ 0nSumDiag2_0nSumDiag2_0 ≤ 0nSumDiag1_post + nSumDiag1_post ≤ 0nSumDiag1_postnSumDiag1_post ≤ 0nSumDiag1_0 + nSumDiag1_0 ≤ 0nSumDiag1_0nSumDiag1_0 ≤ 0nSumCol_post + nSumCol_post ≤ 0nSumCol_postnSumCol_post ≤ 0nSumCol_0 + nSumCol_0 ≤ 0nSumCol_0nSumCol_0 ≤ 0nN_post + nN_post ≤ 0nN_postnN_post ≤ 0nN_0 + nN_0 ≤ 0nN_0nN_0 ≤ 0nDim_post + nDim_post ≤ 0nDim_postnDim_post ≤ 0nDim_0 + nDim_0 ≤ 0nDim_0nDim_0 ≤ 0bSymmetry_post + bSymmetry_post ≤ 0bSymmetry_postbSymmetry_post ≤ 0bSymmetry_0 + bSymmetry_0 ≤ 0bSymmetry_0bSymmetry_0 ≤ 0bSum_post + bSum_post ≤ 0bSum_postbSum_post ≤ 0bSum_0 + bSum_0 ≤ 0bSum_0bSum_0 ≤ 0bDomain_post + bDomain_post ≤ 0bDomain_postbDomain_post ≤ 0bDomain_0 + bDomain_0 ≤ 0bDomain_0bDomain_0 ≤ 0bDistinct_post + bDistinct_post ≤ 0bDistinct_postbDistinct_post ≤ 0bDistinct_0 + bDistinct_0 ≤ 0bDistinct_0bDistinct_0 ≤ 0

23 SCC Decomposition

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

23.1 SCC Subproblem 1/7

Here we consider the SCC { 10, 35, 38, 39, 52, 53, 54, 55, 10_var_snapshot, 10*, 38_var_snapshot, 38* }.

23.1.1 Transition Removal

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

10: 2 + 8⋅nDim_0 − 8⋅nj_0
35: 8⋅nDim_0 − 8⋅nj_0
38: −1 + 8⋅nDim_0 − 8⋅nj_0
39: −1 + 8⋅nDim_0 − 8⋅nj_0
52: −4 + 8⋅nDim_0 − 8⋅nj_0
53: −5 + 8⋅nDim_0 − 8⋅nj_0
54: −3 + 8⋅nDim_0 − 8⋅nj_0
55: −2 + 8⋅nDim_0 − 8⋅nj_0
10_var_snapshot: 1 + 8⋅nDim_0 − 8⋅nj_0
10*: 2 + 8⋅nDim_0 − 8⋅nj_0
38_var_snapshot: −1 + 8⋅nDim_0 − 8⋅nj_0
38*: −1 + 8⋅nDim_0 − 8⋅nj_0

23.1.2 Transition Removal

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

10: −6 + bSum_post + 4⋅nDim_0 − 4⋅ni_0
35: −8 + bSum_post + 4⋅nDim_0 − 4⋅ni_0
38: 2 + 4⋅nDim_0 − 4⋅ni_0
39: 4⋅nDim_0 − 4⋅ni_0
52: −3 + 4⋅nDim_0 − 4⋅ni_0
53: −4 + 4⋅nDim_0 − 4⋅ni_0 + tmp___5_0
54: −2 + 4⋅nDim_0 − 4⋅ni_0
55: −1 + 4⋅nDim_0 − 4⋅ni_0
10_var_snapshot: −7 + bSum_post + 4⋅nDim_0 − 4⋅ni_0
10*: −5 + bSum_post + 4⋅nDim_0 − 4⋅ni_0
38_var_snapshot: 1 + 4⋅nDim_0 − 4⋅ni_0
38*: 3 + 4⋅nDim_0 − 4⋅ni_0

23.1.3 Transition Removal

We remove transitions 125, 127, 167, 169, 60, 63, 87, 88, 89, 90, 91, 92, 93, 94, 96 using the following ranking functions, which are bounded by −7.

10: −5
35: −7
38: 3
39: 1
52: −2
53: −3
54: −1
55: 0
10_var_snapshot: −6
10*: −4
38_var_snapshot: 2
38*: 4

23.1.4 Splitting Cut-Point Transitions

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

23.1.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 124.

23.1.4.1.1 Splitting Cut-Point Transitions

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

23.1.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 166.

23.1.4.2.1 Splitting Cut-Point Transitions

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

23.2 SCC Subproblem 2/7

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

23.2.1 Transition Removal

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

0: −3 + 9⋅nDim_0 − 9⋅ni_0
1: −4 + 9⋅nDim_0 − 9⋅ni_0
2: 3 + 9⋅nDim_0 − 9⋅ni_0
3: −2 + 9⋅nDim_0 − 9⋅ni_0
4: −1 + 9⋅nDim_0 − 9⋅ni_0
7: 9⋅nDim_0 − 9⋅ni_0
8: 9⋅nDim_0 − 9⋅ni_0
9: 1 + 9⋅nDim_0 − 9⋅ni_0
2_var_snapshot: 2 + 9⋅nDim_0 − 9⋅ni_0
2*: 4 + 9⋅nDim_0 − 9⋅ni_0
8_var_snapshot: 9⋅nDim_0 − 9⋅ni_0
8*: 9⋅nDim_0 − 9⋅ni_0

23.2.2 Transition Removal

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

0: −4 + 4⋅nDim_0 − 4⋅nj_0
1: −5 + 4⋅nDim_0 − 4⋅nj_0 + tmp___4_0
2: −7 + 4⋅nDim_0 − 4⋅nj_0 + tmp___4_0
3: −3 + 4⋅nDim_0 − 4⋅nj_0
4: −2 + 4⋅nDim_0 − 4⋅nj_0
7: −1 + 4⋅nDim_0 − 4⋅nj_0
8: 1 + 4⋅nDim_0 − 4⋅nj_0
9: −9 + 4⋅nDim_0 − 4⋅nj_0 + tmp___4_0
2_var_snapshot: −8 + 4⋅nDim_0 − 4⋅nj_0 + tmp___4_0
2*: −6 + 4⋅nDim_0 − 4⋅nj_0 + tmp___4_0
8_var_snapshot: 4⋅nDim_0 − 4⋅nj_0
8*: 2 + 4⋅nDim_0 − 4⋅nj_0

23.2.3 Transition Removal

We remove transitions 104, 106, 118, 120, 0, 1, 2, 3, 4, 5, 6, 7, 9, 41, 49 using the following ranking functions, which are bounded by −9.

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

23.2.4 Splitting Cut-Point Transitions

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

23.2.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 103.

23.2.4.1.1 Splitting Cut-Point Transitions

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

23.2.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 117.

23.2.4.2.1 Splitting Cut-Point Transitions

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

23.3 SCC Subproblem 3/7

Here we consider the SCC { 17, 18, 18_var_snapshot, 18* }.

23.3.1 Transition Removal

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

17: −1 + 4⋅nDim_0 − 4⋅ni_0
18: 1 + 4⋅nDim_0 − 4⋅ni_0
18_var_snapshot: 4⋅nDim_0 − 4⋅ni_0
18*: 2 + 4⋅nDim_0 − 4⋅ni_0

23.3.2 Transition Removal

We remove transitions 141, 35 using the following ranking functions, which are bounded by −1.

17: −1
18: 1
18_var_snapshot: 0
18*: 2

23.3.3 Transition Removal

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

17: 0
18: 1
18_var_snapshot: 0
18*: 0

23.3.4 Splitting Cut-Point Transitions

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

23.3.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 138.

23.3.4.1.1 Splitting Cut-Point Transitions

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

23.4 SCC Subproblem 4/7

Here we consider the SCC { 19, 20, 19_var_snapshot, 19* }.

23.4.1 Transition Removal

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

19: −1 + 4⋅nDim_0 − 4⋅ni_0
20: −3 + 4⋅nDim_0 − 4⋅ni_0
19_var_snapshot: −2 + 4⋅nDim_0 − 4⋅ni_0
19*: 4⋅nDim_0 − 4⋅ni_0

23.4.2 Transition Removal

We remove transitions 148, 24 using the following ranking functions, which are bounded by −3.

19: −1
20: −3
19_var_snapshot: −2
19*: 0

23.4.3 Transition Removal

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

19: 1
20: 0
19_var_snapshot: 0
19*: 0

23.4.4 Splitting Cut-Point Transitions

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

23.4.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 145.

23.4.4.1.1 Splitting Cut-Point Transitions

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

23.5 SCC Subproblem 5/7

Here we consider the SCC { 5, 6, 13, 14, 25, 26, 27, 28, 5_var_snapshot, 5*, 13_var_snapshot, 13* }.

23.5.1 Transition Removal

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

5: 10 + 12⋅nN_0 − 12⋅ni_0
6: 8 + 12⋅nN_0 − 12⋅ni_0
13: 12⋅nN_0 − 12⋅ni_0
14: 12⋅nN_0 − 12⋅ni_0
25: 12⋅nN_0 − 12⋅ni_0
26: 12⋅nN_0 − 12⋅ni_0
27: 12⋅nN_0 − 12⋅ni_0
28: 12⋅nN_0 − 12⋅ni_0
5_var_snapshot: 9 + 12⋅nN_0 − 12⋅ni_0
5*: 11 + 12⋅nN_0 − 12⋅ni_0
13_var_snapshot: 12⋅nN_0 − 12⋅ni_0
13*: 12⋅nN_0 − 12⋅ni_0

23.5.2 Transition Removal

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

5: −2 + 8⋅nN_0 − 8⋅nj_0
6: −4 + 8⋅nN_0 − 8⋅nj_0
13: 2 + 8⋅nN_0 − 8⋅nj_0
14: 8⋅nN_0 − 8⋅nj_0
25: −4 + 8⋅nN_0 − 8⋅nj_0
26: −3 + 8⋅nN_0 − 8⋅nj_0
27: −2 + 8⋅nN_0 − 8⋅nj_0
28: −1 + 8⋅nN_0 − 8⋅nj_0
5_var_snapshot: −3 + 8⋅nN_0 − 8⋅nj_0
5*: −1 + 8⋅nN_0 − 8⋅nj_0
13_var_snapshot: 1 + 8⋅nN_0 − 8⋅nj_0
13*: 3 + 8⋅nN_0 − 8⋅nj_0

23.5.3 Transition Removal

We remove transitions 111, 113, 132, 134, 8, 15, 36, 37, 38, 39, 40, 42, 43, 44, 45 using the following ranking functions, which are bounded by −10.

5: −8
6: −10
13: −4
14: −6
25: −2
26: −1
27: 0
28: 1
5_var_snapshot: −9
5*: −7
13_var_snapshot: −5
13*: −3

23.5.4 Splitting Cut-Point Transitions

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

23.5.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 110.

23.5.4.1.1 Splitting Cut-Point Transitions

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

23.5.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 131.

23.5.4.2.1 Splitting Cut-Point Transitions

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

23.6 SCC Subproblem 6/7

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

23.6.1 Transition Removal

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

29: −5 + 8⋅nN_0 − 8⋅ni_0
30: 1 + 8⋅nN_0 − 8⋅ni_0
31: −4 + 8⋅nN_0 − 8⋅ni_0
32: −3 + 8⋅nN_0 − 8⋅ni_0
33: −2 + 8⋅nN_0 − 8⋅ni_0
34: −1 + 8⋅nN_0 − 8⋅ni_0
30_var_snapshot: 8⋅nN_0 − 8⋅ni_0
30*: 2 + 8⋅nN_0 − 8⋅ni_0

23.6.2 Transition Removal

We remove transitions 153, 155, 50, 51, 52, 53, 54, 55, 56, 57, 100 using the following ranking functions, which are bounded by −6.

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

23.6.3 Splitting Cut-Point Transitions

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

23.6.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 152.

23.6.3.1.1 Splitting Cut-Point Transitions

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

23.7 SCC Subproblem 7/7

Here we consider the SCC { 36, 37, 37_var_snapshot, 37* }.

23.7.1 Transition Removal

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

36: −1 + 4⋅nN_0 − 4⋅ni_0
37: 1 + 4⋅nN_0 − 4⋅ni_0
37_var_snapshot: 4⋅nN_0 − 4⋅ni_0
37*: 2 + 4⋅nN_0 − 4⋅ni_0

23.7.2 Transition Removal

We remove transitions 162, 95 using the following ranking functions, which are bounded by −1.

36: −1
37: 1
37_var_snapshot: 0
37*: 2

23.7.3 Transition Removal

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

36: 0
37: 1
37_var_snapshot: 0
37*: 0

23.7.4 Splitting Cut-Point Transitions

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

23.7.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 159.

23.7.4.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert