by T2Cert
0 | 0 | 1: | 1 − j_0 + n_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
0 | 1 | 2: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ j_0 − n_0 ≤ 0 ∧ temp_post − tmp_post ≤ 0 ∧ − temp_post + tmp_post ≤ 0 ∧ temp_0 − temp_post ≤ 0 ∧ − temp_0 + temp_post ≤ 0 ∧ tmp_0 − tmp_post ≤ 0 ∧ − tmp_0 + tmp_post ≤ 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 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
3 | 2 | 0: | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
4 | 3 | 5: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − j_0 + j_post ≤ 0 ∧ 1 + j_0 − j_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
6 | 4 | 4: | 1 − i_0 + n_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
6 | 5 | 7: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ i_0 − n_0 ≤ 0 ∧ −1 − i_0 + i_post ≤ 0 ∧ 1 + i_0 − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
7 | 6 | 6: | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
8 | 7 | 7: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ dum_0 − dum_post ≤ 0 ∧ − dum_0 + dum_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
9 | 8 | 4: | j_0 − n_0 ≤ 0 ∧ − j_0 + n_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
9 | 9 | 8: | 1 − j_0 + n_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
9 | 10 | 8: | 1 + j_0 − n_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
10 | 11 | 9: | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
10 | 12 | 9: | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
10 | 13 | 9: | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
11 | 14 | 10: | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
12 | 15 | 11: | 1 − k_0 + n_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
12 | 16 | 13: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ k_0 − n_0 ≤ 0 ∧ −1 − k_0 + k_post ≤ 0 ∧ 1 + k_0 − k_post ≤ 0 ∧ dum_0 − dum_post ≤ 0 ∧ − dum_0 + dum_post ≤ 0 ∧ k_0 − k_post ≤ 0 ∧ − k_0 + k_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
13 | 17 | 12: | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
14 | 18 | 11: | − imax_0 + j_0 ≤ 0 ∧ imax_0 − j_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
14 | 19 | 13: | 1 + imax_0 − j_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
14 | 20 | 13: | 1 − imax_0 + j_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
15 | 21 | 16: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − i_0 + i_post ≤ 0 ∧ 1 + i_0 − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
17 | 22 | 15: | 1 − big_0 + dum_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
17 | 23 | 15: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ big_0 − dum_0 ≤ 0 ∧ big_post − dum_0 ≤ 0 ∧ − big_post + dum_0 ≤ 0 ∧ − i_0 + imax_post ≤ 0 ∧ i_0 − imax_post ≤ 0 ∧ big_0 − big_post ≤ 0 ∧ − big_0 + big_post ≤ 0 ∧ imax_0 − imax_post ≤ 0 ∧ − imax_0 + imax_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 | |
18 | 24 | 5: | 1 − i_0 + n_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
18 | 25 | 3: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ i_0 − n_0 ≤ 0 ∧ big_post ≤ 0 ∧ − big_post ≤ 0 ∧ big_0 − big_post ≤ 0 ∧ − big_0 + big_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 | |
19 | 26 | 17: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ j_0 − k_0 ≤ 0 ∧ dum_0 − dum_post ≤ 0 ∧ − dum_0 + dum_post ≤ 0 ∧ tmp___0_0 − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
19 | 27 | 20: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − j_0 + k_0 ≤ 0 ∧ −1 − k_0 + k_post ≤ 0 ∧ 1 + k_0 − k_post ≤ 0 ∧ k_0 − k_post ≤ 0 ∧ − k_0 + k_post ≤ 0 ∧ sum_0 − sum_post ≤ 0 ∧ − sum_0 + sum_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
20 | 28 | 19: | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
21 | 29 | 14: | 1 − i_0 + n_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
21 | 30 | 20: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ i_0 − n_0 ≤ 0 ∧ sum_0 − sum_post ≤ 0 ∧ − sum_0 + sum_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
22 | 31 | 18: | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
16 | 32 | 21: | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
23 | 33 | 24: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ i_0 − k_0 ≤ 0 ∧ −1 − i_0 + i_post ≤ 0 ∧ 1 + i_0 − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
23 | 34 | 25: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − i_0 + k_0 ≤ 0 ∧ −1 − k_0 + k_post ≤ 0 ∧ 1 + k_0 − k_post ≤ 0 ∧ k_0 − k_post ≤ 0 ∧ − k_0 + k_post ≤ 0 ∧ sum_0 − sum_post ≤ 0 ∧ − sum_0 + sum_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
25 | 35 | 23: | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
26 | 36 | 16: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ − i_0 + j_0 ≤ 0 ∧ big_post ≤ 0 ∧ − big_post ≤ 0 ∧ big_0 − big_post ≤ 0 ∧ − big_0 + big_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 | |
26 | 37 | 25: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + i_0 − j_0 ≤ 0 ∧ sum_0 − sum_post ≤ 0 ∧ − sum_0 + sum_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
24 | 38 | 26: | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
27 | 39 | 28: | 1 − j_0 + n_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
27 | 40 | 24: | j_0 − n_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
5 | 41 | 27: | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
29 | 42 | 22: | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
30 | 43 | 22: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − i_0 + i_post ≤ 0 ∧ 1 + i_0 − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
1 | 44 | 30: | 1 − big_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
1 | 45 | 30: | 1 + big_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
1 | 46 | 30: | big_0 ≤ 0 ∧ − big_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
31 | 47 | 3: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − j_0 + j_post ≤ 0 ∧ 1 + j_0 − j_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
2 | 48 | 31: | − big_0 + temp_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 | |
2 | 49 | 31: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + big_0 − temp_0 ≤ 0 ∧ big_post − temp_0 ≤ 0 ∧ − big_post + temp_0 ≤ 0 ∧ big_0 − big_post ≤ 0 ∧ − big_0 + big_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 | |
32 | 50 | 29: | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 |
3 | 51 | : | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 |
5 | 58 | : | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 |
7 | 65 | : | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 |
13 | 72 | : | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 |
16 | 79 | : | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 |
20 | 86 | : | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 |
22 | 93 | : | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 |
24 | 100 | : | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 |
25 | 107 | : | − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0 |
We remove transitions
, , , using the following ranking functions, which are bounded by −31.32: | 0 |
29: | 0 |
0: | 0 |
1: | 0 |
2: | 0 |
3: | 0 |
18: | 0 |
22: | 0 |
30: | 0 |
31: | 0 |
4: | 0 |
5: | 0 |
6: | 0 |
7: | 0 |
8: | 0 |
9: | 0 |
10: | 0 |
11: | 0 |
12: | 0 |
13: | 0 |
14: | 0 |
15: | 0 |
16: | 0 |
17: | 0 |
19: | 0 |
20: | 0 |
21: | 0 |
23: | 0 |
24: | 0 |
25: | 0 |
26: | 0 |
27: | 0 |
28: | 0 |
: | −6 |
: | −7 |
: | −8 |
: | −8 |
: | −8 |
: | −8 |
: | −8 |
: | −8 |
: | −8 |
: | −8 |
: | −8 |
: | −8 |
: | −8 |
: | −8 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −11 |
: | −24 |
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
54 : − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
52 : − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
61 : − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
59 : − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
68 : − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
66 : − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
75 : − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
73 : − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
82 : − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
80 : − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
89 : − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
87 : − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
96 : − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
94 : − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
103 : − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
101 : − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
110 : − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
108 : − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
We consider subproblems for each of the 2 SCC(s) of the program graph.
Here we consider the SCC {
, , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , }.We remove transition
using the following ranking functions, which are bounded by −1.: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −3 − 5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −2 − 5⋅i_0 + 5⋅n_0 |
: | −1 − 5⋅i_0 + 5⋅n_0 |
: | −1 − 5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5 − 5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5 − 5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −1 − 5⋅i_0 + 5⋅n_0 |
: | −1 − 5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5⋅i_0 + 5⋅n_0 |
: | −5 − 5⋅i_0 + 5⋅n_0 |
: | −5 − 5⋅i_0 + 5⋅n_0 |
We remove transition
using the following ranking functions, which are bounded by 0.: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 1 |
: | 0 |
: | 1 |
: | 1 |
: | 1 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 1 |
: | 1 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
We remove transition
using the following ranking functions, which are bounded by 1.: | −22 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −21 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −19 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −17 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −16 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −15 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −14 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −13 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −11 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −9 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −4 + 4⋅j_0 − 4⋅k_0 |
: | −6 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −3 + 4⋅j_0 − 4⋅k_0 |
: | −2 + 4⋅j_0 − 4⋅k_0 |
: | 4⋅j_0 − 4⋅k_0 |
: | −8 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −7 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −2 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −5 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −4 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −1 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | 1 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −20 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −18 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −12 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −10 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −7 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −5 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −1 + 4⋅j_0 − 4⋅k_0 |
: | 1 + 4⋅j_0 − 4⋅k_0 |
: | −3 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −1 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −6 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
: | −4 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0 |
We remove transitions 87, , , , using the following ranking functions, which are bounded by −4.
: | −20 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | 1 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −20 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −18 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −17 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −16 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −15 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −14 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −13 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −11 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −9 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −4 |
: | −6 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −3 |
: | −2 |
: | 0 |
: | −8 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −7 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −2 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −5 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −4 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −1 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | 2 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −19 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −18 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −12 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −10 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −7 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −5 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −1 |
: | 1 |
: | −3 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −1 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −6 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
: | −4 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0 |
We remove transition 89 using the following ranking functions, which are bounded by −1.
: | −20 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | 1 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −19 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −17 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −16 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −15 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −14 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −13 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −12 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −12 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −10 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | 0 |
: | −7 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | 0 |
: | 0 |
: | −1 |
: | −9 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −8 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −3 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −7 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −5 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −1 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | 2 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −18 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −16 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −12 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −11 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −8 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −6 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | 0 |
: | 0 |
: | −4 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −2 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −7 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
: | −6 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0 |
We remove transition
using the following ranking functions, which are bounded by −1.: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | 0 |
: | − i_0 + n_0 |
: | 0 |
: | 0 |
: | 0 |
: | − i_0 + n_0 |
: | −1 − i_0 + n_0 |
: | − i_0 + n_0 |
: | −1 − i_0 + n_0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | 0 |
: | 0 |
: | − i_0 + n_0 |
: | − i_0 + n_0 |
: | −1 − i_0 + n_0 |
: | −1 − i_0 + n_0 |
We remove transition
using the following ranking functions, which are bounded by −10.: | −13 − 16⋅j_0 + 16⋅n_0 |
: | 1 − 16⋅j_0 + 16⋅n_0 |
: | −12 − 16⋅j_0 + 16⋅n_0 |
: | −10 − 16⋅j_0 + 16⋅n_0 |
: | −9 − 16⋅j_0 + 16⋅n_0 |
: | −9 − 16⋅j_0 + 16⋅n_0 |
: | −8 − 16⋅j_0 + 16⋅n_0 |
: | −7 − 16⋅j_0 + 16⋅n_0 |
: | −7 − 16⋅j_0 + 16⋅n_0 |
: | −7 − 16⋅j_0 + 16⋅n_0 |
: | −6 − 16⋅j_0 + 16⋅n_0 |
: | 0 |
: | −3 − 16⋅j_0 + 16⋅n_0 |
: | 0 |
: | 0 |
: | 0 |
: | −5 − 16⋅j_0 + 16⋅n_0 |
: | −1 − 16⋅j_0 + 16⋅n_0 |
: | −1 − 16⋅j_0 + 16⋅n_0 |
: | −1 − 16⋅j_0 + 16⋅n_0 |
: | −1 − 16⋅j_0 + 16⋅n_0 |
: | −1 − 16⋅j_0 + 16⋅n_0 |
: | −16⋅j_0 + 16⋅n_0 |
: | 2 − 16⋅j_0 + 16⋅n_0 |
: | −11 − 16⋅j_0 + 16⋅n_0 |
: | −9 − 16⋅j_0 + 16⋅n_0 |
: | −7 − 16⋅j_0 + 16⋅n_0 |
: | −7 − 16⋅j_0 + 16⋅n_0 |
: | −4 − 16⋅j_0 + 16⋅n_0 |
: | −2 − 16⋅j_0 + 16⋅n_0 |
: | 0 |
: | 0 |
: | −1 − 16⋅j_0 + 16⋅n_0 |
: | −1 − 16⋅j_0 + 16⋅n_0 |
: | −1 − 16⋅j_0 + 16⋅n_0 |
: | −1 − 16⋅j_0 + 16⋅n_0 |
We remove transition
using the following ranking functions, which are bounded by 12.: | −17 + 20⋅imax_0 − 20⋅j_0 |
: | 1 + 20⋅imax_0 − 20⋅j_0 |
: | −16 + 20⋅imax_0 − 20⋅j_0 |
: | −14 + 20⋅imax_0 − 20⋅j_0 |
: | −12 + 20⋅imax_0 − 20⋅j_0 |
: | −11 + 20⋅imax_0 − 20⋅j_0 |
: | −10 + 20⋅imax_0 − 20⋅j_0 |
: | −9 + 20⋅imax_0 − 20⋅j_0 |
: | −8 + 20⋅imax_0 − 20⋅j_0 |
: | −8 + 20⋅imax_0 − 20⋅j_0 |
: | −7 + 20⋅imax_0 − 20⋅j_0 |
: | 0 |
: | −4 + 20⋅imax_0 − 20⋅j_0 |
: | 0 |
: | 0 |
: | 0 |
: | −6 + 20⋅imax_0 − 20⋅j_0 |
: | −2 + 20⋅imax_0 − 20⋅j_0 |
: | −2 + 20⋅imax_0 − 20⋅j_0 |
: | −2 + 20⋅imax_0 − 20⋅j_0 |
: | −2 + 20⋅imax_0 − 20⋅j_0 |
: | −1 + 20⋅imax_0 − 20⋅j_0 |
: | 20⋅imax_0 − 20⋅j_0 |
: | 2 + 20⋅imax_0 − 20⋅j_0 |
: | −15 + 20⋅imax_0 − 20⋅j_0 |
: | −13 + 20⋅imax_0 − 20⋅j_0 |
: | −8 + 20⋅imax_0 − 20⋅j_0 |
: | −8 + 20⋅imax_0 − 20⋅j_0 |
: | −5 + 20⋅imax_0 − 20⋅j_0 |
: | −3 + 20⋅imax_0 − 20⋅j_0 |
: | 0 |
: | 0 |
: | −2 + 20⋅imax_0 − 20⋅j_0 |
: | −2 + 20⋅imax_0 − 20⋅j_0 |
: | −2 + 20⋅imax_0 − 20⋅j_0 |
: | −2 + 20⋅imax_0 − 20⋅j_0 |
We remove transition
using the following ranking functions, which are bounded by 7.: | −16 − 18⋅j_0 + 18⋅n_0 |
: | 1 − 18⋅j_0 + 18⋅n_0 |
: | −15 − 18⋅j_0 + 18⋅n_0 |
: | −13 − 18⋅j_0 + 18⋅n_0 |
: | −11 − 18⋅j_0 + 18⋅n_0 |
: | −10 − 18⋅j_0 + 18⋅n_0 |
: | −9 − 18⋅j_0 + 18⋅n_0 |
: | −8 − 18⋅j_0 + 18⋅n_0 |
: | −7 − 18⋅j_0 + 18⋅n_0 |
: | −7 − 18⋅j_0 + 18⋅n_0 |
: | −6 − 18⋅j_0 + 18⋅n_0 |
: | 0 |
: | −3 − 18⋅j_0 + 18⋅n_0 |
: | 0 |
: | 0 |
: | 0 |
: | −5 − 18⋅j_0 + 18⋅n_0 |
: | −1 − 18⋅j_0 + 18⋅n_0 |
: | −1 − 18⋅j_0 + 18⋅n_0 |
: | −1 − 18⋅j_0 + 18⋅n_0 |
: | −1 − 18⋅j_0 + 18⋅n_0 |
: | −1 − 18⋅j_0 + 18⋅n_0 |
: | −18⋅j_0 + 18⋅n_0 |
: | 2 − 18⋅j_0 + 18⋅n_0 |
: | −14 − 18⋅j_0 + 18⋅n_0 |
: | −12 − 18⋅j_0 + 18⋅n_0 |
: | −7 − 18⋅j_0 + 18⋅n_0 |
: | −7 − 18⋅j_0 + 18⋅n_0 |
: | −4 − 18⋅j_0 + 18⋅n_0 |
: | −2 − 18⋅j_0 + 18⋅n_0 |
: | 0 |
: | 0 |
: | −1 − 18⋅j_0 + 18⋅n_0 |
: | −1 − 18⋅j_0 + 18⋅n_0 |
: | −1 − 18⋅j_0 + 18⋅n_0 |
: | −1 − 18⋅j_0 + 18⋅n_0 |
We remove transition
using the following ranking functions, which are bounded by −3.: | −10 − 4⋅i_0 − 14⋅j_0 + 18⋅n_0 |
: | 2 − 4⋅i_0 − 14⋅j_0 + 18⋅n_0 |
: | −8 − 4⋅i_0 − 14⋅j_0 + 18⋅n_0 |
: | −6 − 4⋅i_0 − 14⋅j_0 + 18⋅n_0 |
: | −4 − 4⋅i_0 − 14⋅j_0 + 18⋅n_0 |
: | −20 − 4⋅i_0 + 4⋅j_0 |
: | −18 − 4⋅i_0 + 4⋅j_0 |
: | −16 − 4⋅i_0 + 4⋅j_0 |
: | −16 − 4⋅i_0 + 4⋅j_0 |
: | −16 − 4⋅i_0 + 4⋅j_0 |
: | −14 − 4⋅i_0 + 4⋅j_0 |
: | 0 |
: | −8 − 4⋅i_0 + 4⋅j_0 |
: | 0 |
: | 0 |
: | 0 |
: | −12 − 4⋅i_0 + 4⋅j_0 |
: | −7 − 4⋅i_0 + 4⋅j_0 |
: | −4 − 4⋅i_0 + 4⋅j_0 |
: | −7 − 4⋅i_0 + 4⋅j_0 |
: | −6 − 4⋅i_0 + 4⋅j_0 |
: | −2 − 4⋅i_0 − 14⋅j_0 + 18⋅n_0 |
: | −4⋅i_0 − 14⋅j_0 + 18⋅n_0 |
: | 4 − 4⋅i_0 − 14⋅j_0 + 18⋅n_0 |
: | −6 − 4⋅i_0 − 14⋅j_0 + 18⋅n_0 |
: | −5 − 4⋅i_0 − 14⋅j_0 + 18⋅n_0 |
: | −16 − 4⋅i_0 + 4⋅j_0 |
: | −16 − 4⋅i_0 + 4⋅j_0 |
: | −10 − 4⋅i_0 + 4⋅j_0 |
: | −6 − 4⋅i_0 + 4⋅j_0 |
: | 0 |
: | 0 |
: | −5 − 4⋅i_0 + 4⋅j_0 |
: | −4 − 4⋅i_0 + 4⋅j_0 |
: | −7 − 4⋅i_0 + 4⋅j_0 |
: | −7 − 4⋅i_0 + 4⋅j_0 |
We remove transitions 59, 61, 66, 68, , , , , , , using the following ranking functions, which are bounded by −2.
: | 3 |
: | 1 |
: | 6 |
: | 8 |
: | 10 |
: | −12 + 23⋅j_0 − 23⋅n_0 |
: | −11 + 23⋅j_0 − 23⋅n_0 |
: | −11 + 23⋅j_0 − 23⋅n_0 |
: | −10 + 23⋅j_0 − 23⋅n_0 |
: | −10 + 23⋅j_0 − 23⋅n_0 |
: | −9 + 23⋅j_0 − 23⋅n_0 |
: | 0 |
: | −6 + 23⋅j_0 − 23⋅n_0 |
: | 0 |
: | 0 |
: | 0 |
: | −8 + 23⋅j_0 − 23⋅n_0 |
: | 23⋅j_0 − 23⋅n_0 |
: | −3 + 23⋅j_0 − 23⋅n_0 |
: | 23⋅j_0 − 23⋅n_0 |
: | −5 + 23⋅j_0 − 23⋅n_0 |
: | −1 |
: | 0 |
: | 2 |
: | 7 |
: | 9 |
: | −10 + 23⋅j_0 − 23⋅n_0 |
: | −10 + 23⋅j_0 − 23⋅n_0 |
: | −7 + 23⋅j_0 − 23⋅n_0 |
: | −5 + 23⋅j_0 − 23⋅n_0 |
: | 0 |
: | 0 |
: | −4 + 23⋅j_0 − 23⋅n_0 |
: | −2 + 23⋅j_0 − 23⋅n_0 |
: | 23⋅j_0 − 23⋅n_0 |
: | 23⋅j_0 − 23⋅n_0 |
We remove transitions
, using the following ranking functions, which are bounded by −6.: | 0 |
: | 0 |
: | 0 |
: | 1 |
: | 0 |
: | −8 − 4⋅k_0 + 4⋅n_0 |
: | −7 − 4⋅k_0 + 4⋅n_0 |
: | −6 − 4⋅k_0 + 4⋅n_0 |
: | −5 − 4⋅k_0 + 4⋅n_0 |
: | −4 − 4⋅k_0 + 4⋅n_0 |
: | −2 − 4⋅k_0 + 4⋅n_0 |
: | 0 |
: | −3 + 4⋅i_0 − 4⋅k_0 |
: | 0 |
: | 0 |
: | 0 |
: | −5 + 4⋅i_0 − 4⋅k_0 |
: | 7 + 4⋅i_0 − 4⋅k_0 |
: | 1 + 4⋅i_0 − 4⋅k_0 |
: | 9 + 4⋅i_0 − 4⋅k_0 |
: | −1 + 4⋅i_0 − 4⋅k_0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | −5 − 4⋅k_0 + 4⋅n_0 |
: | −3 − 4⋅k_0 + 4⋅n_0 |
: | −4 + 4⋅i_0 − 4⋅k_0 |
: | −2 + 4⋅i_0 − 4⋅k_0 |
: | 0 |
: | 0 |
: | 4⋅i_0 − 4⋅k_0 |
: | 2 + 4⋅i_0 − 4⋅k_0 |
: | 8 + 4⋅i_0 − 4⋅k_0 |
: | 10 + 4⋅i_0 − 4⋅k_0 |
We remove transitions 73, 75, 80, 82, 101, 103, 108, 110, , , , , , , , , , , , , , using the following ranking functions, which are bounded by −13.
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | −13 |
: | −12 |
: | −11 |
: | −10 |
: | −8 |
: | −6 |
: | 0 |
: | −3 |
: | 0 |
: | 0 |
: | 0 |
: | −5 |
: | 3 |
: | 1 |
: | 5 |
: | −1 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | −9 |
: | −7 |
: | −4 |
: | −2 |
: | 0 |
: | 0 |
: | 0 |
: | 2 |
: | 4 |
: | 6 |
We consider 7 subproblems corresponding to sets of cut-point transitions as follows.
There remain no cut-point transition to consider. Hence the cooperation termination is trivial.
There remain no cut-point transition to consider. Hence the cooperation termination is trivial.
There remain no cut-point transition to consider. Hence the cooperation termination is trivial.
There remain no cut-point transition to consider. Hence the cooperation termination is trivial.
There remain no cut-point transition to consider. Hence the cooperation termination is trivial.
There remain no cut-point transition to consider. Hence the cooperation termination is trivial.
There remain no cut-point transition to consider. Hence the cooperation termination is trivial.
Here we consider the SCC {
, , , , , , , , , , , }.We remove transition
using the following ranking functions, which are bounded by 0.: | −3⋅i_0 + 3⋅n_0 |
: | −3⋅i_0 + 3⋅n_0 |
: | −3⋅i_0 + 3⋅n_0 |
: | −3⋅i_0 + 3⋅n_0 |
: | −1 − 3⋅i_0 + 3⋅n_0 |
: | −3⋅i_0 + 3⋅n_0 |
: | 1 − 3⋅i_0 + 3⋅n_0 |
: | 2 − 3⋅i_0 + 3⋅n_0 |
: | −3⋅i_0 + 3⋅n_0 |
: | −3⋅i_0 + 3⋅n_0 |
: | 1 − 3⋅i_0 + 3⋅n_0 |
: | 2 − 3⋅i_0 + 3⋅n_0 |
We remove transition
using the following ranking functions, which are bounded by 0.: | 1 − 13⋅j_0 + 13⋅n_0 |
: | −13⋅j_0 + 13⋅n_0 |
: | −13⋅j_0 + 13⋅n_0 |
: | 3 − 13⋅j_0 + 13⋅n_0 |
: | −1 − 13⋅j_0 + 13⋅n_0 |
: | −8 − 13⋅j_0 + 13⋅n_0 |
: | −5 − 13⋅j_0 + 13⋅n_0 |
: | −3 − 13⋅j_0 + 13⋅n_0 |
: | 2 − 13⋅j_0 + 13⋅n_0 |
: | 4 − 13⋅j_0 + 13⋅n_0 |
: | −4 − 13⋅j_0 + 13⋅n_0 |
: | −2 − 13⋅j_0 + 13⋅n_0 |
We remove transitions 52, 54, 94, 96, , , , , , , , , , using the following ranking functions, which are bounded by −11.
: | −5 |
: | −6 |
: | 0 |
: | −3 |
: | −7 |
: | −1 |
: | −11 |
: | −9 |
: | −4 |
: | −2 |
: | −10 |
: | −8 |
We consider 2 subproblems corresponding to sets of cut-point transitions as follows.
There remain no cut-point transition to consider. Hence the cooperation termination is trivial.
There remain no cut-point transition to consider. Hence the cooperation termination is trivial.
T2Cert