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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_0 ≤ 0
5 110 5: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_0 ≤ 0
8 117 8: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_0 ≤ 0
10 124 10: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_0 ≤ 0
13 131 13: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_0 ≤ 0
18 138 18: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_0 ≤ 0
19 145 19: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_0 ≤ 0
30 152 30: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_0 ≤ 0
37 159 37: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_0 ≤ 0
38 166 38: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___7_post + tmp___7_post ≤ 0 ∧ tmp___7_post − tmp___7_post ≤ 0 ∧ − tmp___7_0 + tmp___7_0 ≤ 0 ∧ tmp___7_0 − tmp___7_0 ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nSum_post + nSum_post ≤ 0 ∧ nSum_post − nSum_post ≤ 0 ∧ − nSum_0 + nSum_0 ≤ 0 ∧ nSum_0 − nSum_0 ≤ 0 ∧ − nSumRow_post + nSumRow_post ≤ 0 ∧ nSumRow_post − nSumRow_post ≤ 0 ∧ − nSumRow_0 + nSumRow_0 ≤ 0 ∧ nSumRow_0 − nSumRow_0 ≤ 0 ∧ − nSumDiag2_post + nSumDiag2_post ≤ 0 ∧ nSumDiag2_post − nSumDiag2_post ≤ 0 ∧ − nSumDiag2_0 + nSumDiag2_0 ≤ 0 ∧ nSumDiag2_0 − nSumDiag2_0 ≤ 0 ∧ − nSumDiag1_post + nSumDiag1_post ≤ 0 ∧ nSumDiag1_post − nSumDiag1_post ≤ 0 ∧ − nSumDiag1_0 + nSumDiag1_0 ≤ 0 ∧ nSumDiag1_0 − nSumDiag1_0 ≤ 0 ∧ − nSumCol_post + nSumCol_post ≤ 0 ∧ nSumCol_post − nSumCol_post ≤ 0 ∧ − nSumCol_0 + nSumCol_0 ≤ 0 ∧ nSumCol_0 − nSumCol_0 ≤ 0 ∧ − nN_post + nN_post ≤ 0 ∧ nN_post − nN_post ≤ 0 ∧ − nN_0 + nN_0 ≤ 0 ∧ nN_0 − nN_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − bSymmetry_post + bSymmetry_post ≤ 0 ∧ bSymmetry_post − bSymmetry_post ≤ 0 ∧ − bSymmetry_0 + bSymmetry_0 ≤ 0 ∧ bSymmetry_0 − bSymmetry_0 ≤ 0 ∧ − bSum_post + bSum_post ≤ 0 ∧ bSum_post − bSum_post ≤ 0 ∧ − bSum_0 + bSum_0 ≤ 0 ∧ bSum_0 − bSum_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bDistinct_post + bDistinct_post ≤ 0 ∧ bDistinct_post − bDistinct_post ≤ 0 ∧ − bDistinct_0 + bDistinct_0 ≤ 0 ∧ bDistinct_0 − bDistinct_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