LTS Termination Proof

by T2Cert

Input

• 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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  12	19	4:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −10 + x_promoted_1_post ≤ 0 ∧ 10 − 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
  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

Proof

1 Invariant Updates

The following invariants are asserted.

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)		−10 + x_promoted_1_post ≤ 0 ∧ 10 − 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 ∧ −10 + x_promoted_1_0 ≤ 0 ∧ 10 − 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 + a15_post ≤ 0 ∧ −2 + b16_post ≤ 0 ∧ −10 + c17_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)		−10 + x_promoted_1_post ≤ 0 ∧ 10 − 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 ∧ −10 + x_promoted_1_0 ≤ 0 ∧ 10 − 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
  5		(5)		−10 + x_promoted_1_post ≤ 0 ∧ 10 − 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 ∧ −10 + x_promoted_1_0 ≤ 0 ∧ 10 − 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
  6		(6)		−10 + x_promoted_1_post ≤ 0 ∧ 10 − 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 ∧ −10 + x_promoted_1_0 ≤ 0 ∧ 10 − 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 + a15_post ≤ 0 ∧ −2 + b16_post ≤ 0 ∧ −10 + c17_post ≤ 0 ∧ −1 + a15_0 ≤ 0 ∧ −10 + c17_0 ≤ 0
  7		(7)		−10 + x_promoted_1_post ≤ 0 ∧ 10 − 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 ∧ −10 + x_promoted_1_0 ≤ 0 ∧ 10 − 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 + a15_post ≤ 0 ∧ −2 + b16_post ≤ 0 ∧ −10 + c17_post ≤ 0 ∧ −1 + a15_0 ≤ 0 ∧ −2 + b16_0 ≤ 0 ∧ −10 + c17_0 ≤ 0
  8		(8)		−10 + x_promoted_1_post ≤ 0 ∧ 10 − 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 ∧ 10 − x_promoted_1_0 ≤ 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)		−10 + x_promoted_1_post ≤ 0 ∧ 10 − 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 ∧ 10 − x_promoted_1_0 ≤ 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)		−10 + x_promoted_1_post ≤ 0 ∧ 10 − 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 ∧ 10 − x_promoted_1_0 ≤ 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)		−10 + x_promoted_1_post ≤ 0 ∧ 10 − 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 ∧ 10 − x_promoted_1_0 ≤ 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

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.

4 SCC Decomposition

There exist no SCC in the program graph.

Tool configuration

T2Cert

• version: 1.0