# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• Initial Location: 13
• Transitions: (pre-variables and post-variables)  0 0 1: − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − m13_post + m13_post ≤ 0 ∧ m13_post − m13_post ≤ 0 ∧ − m13_0 + m13_0 ≤ 0 ∧ m13_0 − m13_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 2 1 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − a15_0 + ret_max24_post ≤ 0 ∧ a15_0 − ret_max24_post ≤ 0 ∧ − ret_max24_post + tmp___0_post ≤ 0 ∧ ret_max24_post − tmp___0_post ≤ 0 ∧ ret_max24_0 − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_post ≤ 0 ∧ tmp___0_0 − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_post ≤ 0 ∧ z_0 − z_post ≤ 0 ∧ − z_0 + z_post ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − m13_post + m13_post ≤ 0 ∧ m13_post − m13_post ≤ 0 ∧ − m13_0 + m13_0 ≤ 0 ∧ m13_0 − m13_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 4 2 5: 1 − x_promoted_1_0 + y_promoted_2_0 ≤ 0 ∧ − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − m13_post + m13_post ≤ 0 ∧ m13_post − m13_post ≤ 0 ∧ − m13_0 + m13_0 ≤ 0 ∧ m13_0 − m13_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 4 3 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ x_promoted_1_0 − y_promoted_2_0 ≤ 0 ∧ tmp9_0 − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_post ≤ 0 ∧ − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − m13_post + m13_post ≤ 0 ∧ m13_post − m13_post ≤ 0 ∧ − m13_0 + m13_0 ≤ 0 ∧ m13_0 − m13_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 6 4 2: 1 − a15_0 + c17_0 ≤ 0 ∧ − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − m13_post + m13_post ≤ 0 ∧ m13_post − m13_post ≤ 0 ∧ − m13_0 + m13_0 ≤ 0 ∧ m13_0 − m13_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 6 5 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ a15_0 − c17_0 ≤ 0 ∧ tmp923_0 − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_post ≤ 0 ∧ − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − m13_post + m13_post ≤ 0 ∧ m13_post − m13_post ≤ 0 ∧ − m13_0 + m13_0 ≤ 0 ∧ m13_0 − m13_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 7 6 6: 1 − a15_0 + b16_0 ≤ 0 ∧ − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − m13_post + m13_post ≤ 0 ∧ m13_post − m13_post ≤ 0 ∧ − m13_0 + m13_0 ≤ 0 ∧ m13_0 − m13_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 7 7 6: 0 ≤ 0 ∧ 0 ≤ 0 ∧ a15_0 − b16_0 ≤ 0 ∧ tmp620_0 − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_post ≤ 0 ∧ − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − m13_post + m13_post ≤ 0 ∧ m13_post − m13_post ≤ 0 ∧ − m13_0 + m13_0 ≤ 0 ∧ m13_0 − m13_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 8 8 9: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − b11_0 + c12_0 ≤ 0 ∧ − c12_0 + m13_post ≤ 0 ∧ c12_0 − m13_post ≤ 0 ∧ m13_0 − m13_post ≤ 0 ∧ − m13_0 + m13_post ≤ 0 ∧ − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 8 9 9: 0 ≤ 0 ∧ 0 ≤ 0 ∧ b11_0 − c12_0 ≤ 0 ∧ − b11_0 + m13_post ≤ 0 ∧ b11_0 − m13_post ≤ 0 ∧ m13_0 − m13_post ≤ 0 ∧ − m13_0 + m13_post ≤ 0 ∧ − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 9 10 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − m13_0 + ret_min14_post ≤ 0 ∧ m13_0 − ret_min14_post ≤ 0 ∧ − ret_min14_post + tmp_post ≤ 0 ∧ ret_min14_post − tmp_post ≤ 0 ∧ − tmp_post − x_promoted_1_0 + x_promoted_1_post ≤ 0 ∧ tmp_post + x_promoted_1_0 − x_promoted_1_post ≤ 0 ∧ ret_min14_0 − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_post ≤ 0 ∧ tmp_0 − tmp_post ≤ 0 ∧ − tmp_0 + tmp_post ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_post ≤ 0 ∧ − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − m13_post + m13_post ≤ 0 ∧ m13_post − m13_post ≤ 0 ∧ − m13_0 + m13_0 ≤ 0 ∧ m13_0 − m13_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 10 11 9: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − a10_0 + c12_0 ≤ 0 ∧ − c12_0 + m13_post ≤ 0 ∧ c12_0 − m13_post ≤ 0 ∧ m13_0 − m13_post ≤ 0 ∧ − m13_0 + m13_post ≤ 0 ∧ − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 10 12 9: 0 ≤ 0 ∧ 0 ≤ 0 ∧ a10_0 − c12_0 ≤ 0 ∧ − a10_0 + m13_post ≤ 0 ∧ a10_0 − m13_post ≤ 0 ∧ m13_0 − m13_post ≤ 0 ∧ − m13_0 + m13_post ≤ 0 ∧ − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 11 13 8: 1 − a10_0 + b11_0 ≤ 0 ∧ − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − m13_post + m13_post ≤ 0 ∧ m13_post − m13_post ≤ 0 ∧ − m13_0 + m13_0 ≤ 0 ∧ m13_0 − m13_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 11 14 10: a10_0 − b11_0 ≤ 0 ∧ − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − m13_post + m13_post ≤ 0 ∧ m13_post − m13_post ≤ 0 ∧ − m13_0 + m13_0 ≤ 0 ∧ m13_0 − m13_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 5 15 7: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − x_promoted_1_0 + z_0 ≤ 0 ∧ a15_post − z_0 ≤ 0 ∧ − a15_post + z_0 ≤ 0 ∧ b16_post − y_promoted_2_0 ≤ 0 ∧ − b16_post + y_promoted_2_0 ≤ 0 ∧ c17_post − x_promoted_1_0 ≤ 0 ∧ − c17_post + x_promoted_1_0 ≤ 0 ∧ a15_0 − a15_post ≤ 0 ∧ − a15_0 + a15_post ≤ 0 ∧ b16_0 − b16_post ≤ 0 ∧ − b16_0 + b16_post ≤ 0 ∧ c17_0 − c17_post ≤ 0 ∧ − c17_0 + c17_post ≤ 0 ∧ − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − m13_post + m13_post ≤ 0 ∧ m13_post − m13_post ≤ 0 ∧ − m13_0 + m13_0 ≤ 0 ∧ m13_0 − m13_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 5 16 11: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ x_promoted_1_0 − z_0 ≤ 0 ∧ a10_post − x_promoted_1_0 ≤ 0 ∧ − a10_post + x_promoted_1_0 ≤ 0 ∧ b11_post − y_promoted_2_0 ≤ 0 ∧ − b11_post + y_promoted_2_0 ≤ 0 ∧ c12_post − z_0 ≤ 0 ∧ − c12_post + z_0 ≤ 0 ∧ a10_0 − a10_post ≤ 0 ∧ − a10_0 + a10_post ≤ 0 ∧ b11_0 − b11_post ≤ 0 ∧ − b11_0 + b11_post ≤ 0 ∧ c12_0 − c12_post ≤ 0 ∧ − c12_0 + c12_post ≤ 0 ∧ − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − m13_post + m13_post ≤ 0 ∧ m13_post − m13_post ≤ 0 ∧ − m13_0 + m13_0 ≤ 0 ∧ m13_0 − m13_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 3 17 0: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − y_promoted_2_0 + z_0 ≤ 0 ∧ tmp___1_post − y_promoted_2_0 + z_0 ≤ 0 ∧ − tmp___1_post + y_promoted_2_0 − z_0 ≤ 0 ∧ tmp___1_0 − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_post ≤ 0 ∧ − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_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 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − m13_post + m13_post ≤ 0 ∧ m13_post − m13_post ≤ 0 ∧ − m13_0 + m13_0 ≤ 0 ∧ m13_0 − m13_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 3 18 0: 0 ≤ 0 ∧ 0 ≤ 0 ∧ y_promoted_2_0 − z_0 ≤ 0 ∧ tmp___1_post − y_promoted_2_0 − z_0 ≤ 0 ∧ − tmp___1_post + y_promoted_2_0 + z_0 ≤ 0 ∧ tmp___1_0 − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_post ≤ 0 ∧ − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_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 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − m13_post + m13_post ≤ 0 ∧ m13_post − m13_post ≤ 0 ∧ − m13_0 + m13_0 ≤ 0 ∧ m13_0 − m13_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 12 19 4: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − ___const_10_0 + x_promoted_1_post ≤ 0 ∧ ___const_10_0 − x_promoted_1_post ≤ 0 ∧ −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_post ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_post ≤ 0 ∧ z_0 − z_post ≤ 0 ∧ − z_0 + z_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − m13_post + m13_post ≤ 0 ∧ m13_post − m13_post ≤ 0 ∧ − m13_0 + m13_0 ≤ 0 ∧ m13_0 − m13_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 13 20 12: − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − y_promoted_2_post + y_promoted_2_post ≤ 0 ∧ y_promoted_2_post − y_promoted_2_post ≤ 0 ∧ − y_promoted_2_0 + y_promoted_2_0 ≤ 0 ∧ y_promoted_2_0 − y_promoted_2_0 ≤ 0 ∧ − x_promoted_1_post + x_promoted_1_post ≤ 0 ∧ x_promoted_1_post − x_promoted_1_post ≤ 0 ∧ − x_promoted_1_0 + x_promoted_1_0 ≤ 0 ∧ x_promoted_1_0 − x_promoted_1_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp9_post + tmp9_post ≤ 0 ∧ tmp9_post − tmp9_post ≤ 0 ∧ − tmp9_0 + tmp9_0 ≤ 0 ∧ tmp9_0 − tmp9_0 ≤ 0 ∧ − tmp923_post + tmp923_post ≤ 0 ∧ tmp923_post − tmp923_post ≤ 0 ∧ − tmp923_0 + tmp923_0 ≤ 0 ∧ tmp923_0 − tmp923_0 ≤ 0 ∧ − tmp620_post + tmp620_post ≤ 0 ∧ tmp620_post − tmp620_post ≤ 0 ∧ − tmp620_0 + tmp620_0 ≤ 0 ∧ tmp620_0 − tmp620_0 ≤ 0 ∧ − ret_min14_post + ret_min14_post ≤ 0 ∧ ret_min14_post − ret_min14_post ≤ 0 ∧ − ret_min14_0 + ret_min14_0 ≤ 0 ∧ ret_min14_0 − ret_min14_0 ≤ 0 ∧ − ret_max24_post + ret_max24_post ≤ 0 ∧ ret_max24_post − ret_max24_post ≤ 0 ∧ − ret_max24_0 + ret_max24_0 ≤ 0 ∧ ret_max24_0 − ret_max24_0 ≤ 0 ∧ − m13_post + m13_post ≤ 0 ∧ m13_post − m13_post ≤ 0 ∧ − m13_0 + m13_0 ≤ 0 ∧ m13_0 − m13_0 ≤ 0 ∧ − c17_post + c17_post ≤ 0 ∧ c17_post − c17_post ≤ 0 ∧ − c17_0 + c17_0 ≤ 0 ∧ c17_0 − c17_0 ≤ 0 ∧ − c12_post + c12_post ≤ 0 ∧ c12_post − c12_post ≤ 0 ∧ − c12_0 + c12_0 ≤ 0 ∧ c12_0 − c12_0 ≤ 0 ∧ − b16_post + b16_post ≤ 0 ∧ b16_post − b16_post ≤ 0 ∧ − b16_0 + b16_0 ≤ 0 ∧ b16_0 − b16_0 ≤ 0 ∧ − b11_post + b11_post ≤ 0 ∧ b11_post − b11_post ≤ 0 ∧ − b11_0 + b11_0 ≤ 0 ∧ b11_0 − b11_0 ≤ 0 ∧ − a15_post + a15_post ≤ 0 ∧ a15_post − a15_post ≤ 0 ∧ − a15_0 + a15_0 ≤ 0 ∧ a15_0 − a15_0 ≤ 0 ∧ − a10_post + a10_post ≤ 0 ∧ a10_post − a10_post ≤ 0 ∧ − a10_0 + a10_0 ≤ 0 ∧ a10_0 − a10_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0

## Proof

The following invariants are asserted.

 0: −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 1: −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 2: −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 ∧ −1 + z_0 ≤ 0 ∧ 1 − z_0 ≤ 0 ∧ −1 + a15_post ≤ 0 ∧ −2 + b16_post ≤ 0 ∧ −1 + a15_0 ≤ 0 3: −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 4: −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 ∧ −1 + z_0 ≤ 0 ∧ 1 − z_0 ≤ 0 5: −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 ∧ −1 + z_0 ≤ 0 ∧ 1 − z_0 ≤ 0 6: −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 ∧ −1 + z_0 ≤ 0 ∧ 1 − z_0 ≤ 0 ∧ −1 + a15_post ≤ 0 ∧ −2 + b16_post ≤ 0 ∧ −1 + a15_0 ≤ 0 7: −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 ∧ −1 + z_0 ≤ 0 ∧ 1 − z_0 ≤ 0 ∧ −1 + a15_post ≤ 0 ∧ −2 + b16_post ≤ 0 ∧ −1 + a15_0 ≤ 0 ∧ −2 + b16_0 ≤ 0 8: −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ −1 + x_promoted_1_0 ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 ∧ −1 + z_0 ≤ 0 ∧ 1 − z_0 ≤ 0 ∧ −1 + a10_post ≤ 0 ∧ −2 + b11_post ≤ 0 ∧ −1 + c12_post ≤ 0 ∧ −1 + a10_0 ≤ 0 ∧ b11_0 ≤ 0 ∧ −1 + c12_0 ≤ 0 9: −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ −1 + x_promoted_1_0 ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 ∧ −1 + z_0 ≤ 0 ∧ 1 − z_0 ≤ 0 ∧ −1 + a10_post ≤ 0 ∧ −2 + b11_post ≤ 0 ∧ −1 + c12_post ≤ 0 ∧ −1 + a10_0 ≤ 0 10: −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ −1 + x_promoted_1_0 ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 ∧ −1 + z_0 ≤ 0 ∧ 1 − z_0 ≤ 0 ∧ −1 + a10_post ≤ 0 ∧ −2 + b11_post ≤ 0 ∧ −1 + c12_post ≤ 0 ∧ −1 + a10_0 ≤ 0 ∧ −2 + b11_0 ≤ 0 ∧ −1 + c12_0 ≤ 0 11: −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ −1 + x_promoted_1_0 ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 ∧ −1 + z_0 ≤ 0 ∧ 1 − z_0 ≤ 0 ∧ −1 + a10_post ≤ 0 ∧ −2 + b11_post ≤ 0 ∧ −1 + c12_post ≤ 0 ∧ −1 + a10_0 ≤ 0 ∧ −2 + b11_0 ≤ 0 ∧ −1 + c12_0 ≤ 0 12: TRUE 13: TRUE

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (0) −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 1 (1) −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 2 (2) −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 ∧ −1 + z_0 ≤ 0 ∧ 1 − z_0 ≤ 0 ∧ −1 + a15_post ≤ 0 ∧ −2 + b16_post ≤ 0 ∧ −1 + a15_0 ≤ 0 3 (3) −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 4 (4) −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 ∧ −1 + z_0 ≤ 0 ∧ 1 − z_0 ≤ 0 5 (5) −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 ∧ −1 + z_0 ≤ 0 ∧ 1 − z_0 ≤ 0 6 (6) −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 ∧ −1 + z_0 ≤ 0 ∧ 1 − z_0 ≤ 0 ∧ −1 + a15_post ≤ 0 ∧ −2 + b16_post ≤ 0 ∧ −1 + a15_0 ≤ 0 7 (7) −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 ∧ −1 + z_0 ≤ 0 ∧ 1 − z_0 ≤ 0 ∧ −1 + a15_post ≤ 0 ∧ −2 + b16_post ≤ 0 ∧ −1 + a15_0 ≤ 0 ∧ −2 + b16_0 ≤ 0 8 (8) −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ −1 + x_promoted_1_0 ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 ∧ −1 + z_0 ≤ 0 ∧ 1 − z_0 ≤ 0 ∧ −1 + a10_post ≤ 0 ∧ −2 + b11_post ≤ 0 ∧ −1 + c12_post ≤ 0 ∧ −1 + a10_0 ≤ 0 ∧ b11_0 ≤ 0 ∧ −1 + c12_0 ≤ 0 9 (9) −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ −1 + x_promoted_1_0 ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 ∧ −1 + z_0 ≤ 0 ∧ 1 − z_0 ≤ 0 ∧ −1 + a10_post ≤ 0 ∧ −2 + b11_post ≤ 0 ∧ −1 + c12_post ≤ 0 ∧ −1 + a10_0 ≤ 0 10 (10) −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ −1 + x_promoted_1_0 ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 ∧ −1 + z_0 ≤ 0 ∧ 1 − z_0 ≤ 0 ∧ −1 + a10_post ≤ 0 ∧ −2 + b11_post ≤ 0 ∧ −1 + c12_post ≤ 0 ∧ −1 + a10_0 ≤ 0 ∧ −2 + b11_0 ≤ 0 ∧ −1 + c12_0 ≤ 0 11 (11) −2 + y_promoted_2_post ≤ 0 ∧ 2 − y_promoted_2_post ≤ 0 ∧ −1 + z_post ≤ 0 ∧ 1 − z_post ≤ 0 ∧ −1 + x_promoted_1_0 ≤ 0 ∧ −2 + y_promoted_2_0 ≤ 0 ∧ 2 − y_promoted_2_0 ≤ 0 ∧ −1 + z_0 ≤ 0 ∧ 1 − z_0 ≤ 0 ∧ −1 + a10_post ≤ 0 ∧ −2 + b11_post ≤ 0 ∧ −1 + c12_post ≤ 0 ∧ −1 + a10_0 ≤ 0 ∧ −2 + b11_0 ≤ 0 ∧ −1 + c12_0 ≤ 0 12 (12) TRUE 13 (13) TRUE
• initial node: 13
• cover edges:
• transition edges:  0 0 1 2 1 3 3 17 0 3 18 0 4 2 5 4 3 3 5 15 7 5 16 11 6 4 2 6 5 2 7 6 6 7 7 6 8 8 9 8 9 9 9 10 3 10 11 9 10 12 9 11 13 8 11 14 10 12 19 4 13 20 12

### 2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
and for every transition t, a duplicate t is considered.

### 3 Transition Removal

We remove transitions 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20 using the following ranking functions, which are bounded by −30.

 13: 0 12: 0 4: 0 5: 0 7: 0 6: 0 2: 0 11: 0 8: 0 10: 0 9: 0 3: 0 0: 0 1: 0 13: −15 12: −16 4: −17 5: −18 7: −19 6: −20 2: −21 11: −22 8: −23 10: −24 9: −25 3: −26 0: −27 1: −28

### 4 SCC Decomposition

There exist no SCC in the program graph.

T2Cert

• version: 1.0