LTS Termination Proof

by T2Cert

Input

• Initial Location: 18
• Transitions: (pre-variables and post-variables)

  0	0	1:		2 − n_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  0	1	1:		n_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  0	2	2:		−1 + n_0 ≤ 0 ∧ 1 − n_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  3	3	4:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − j_0 + m2_0 ≤ 0 ∧ −1 − m_0 + m_post ≤ 0 ∧ 1 + m_0 − m_post ≤ 0 ∧ m_0 − m_post ≤ 0 ∧ − m_0 + m_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  3	4	5:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ j_0 − m2_0 ≤ 0 ∧ − k_0 + tmp_post ≤ 0 ∧ k_0 − tmp_post ≤ 0 ∧ 1 − k_0 + k_post ≤ 0 ∧ −1 + k_0 − k_post ≤ 0 ∧ −1 − j_0 + j_post ≤ 0 ∧ 1 + j_0 − j_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ k_0 − k_post ≤ 0 ∧ − k_0 + k_post ≤ 0 ∧ pt1_0 − pt1_post ≤ 0 ∧ − pt1_0 + pt1_post ≤ 0 ∧ pt2_0 − pt2_post ≤ 0 ∧ − pt2_0 + pt2_post ≤ 0 ∧ qt1_0 − qt1_post ≤ 0 ∧ − qt1_0 + qt1_post ≤ 0 ∧ qt2_0 − qt2_post ≤ 0 ∧ − qt2_0 + qt2_post ≤ 0 ∧ tmp_0 − tmp_post ≤ 0 ∧ − tmp_0 + tmp_post ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0
  4	5	6:		− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  7	6	8:		− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  9	7	5:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − j_0 + m_0 ≤ 0 ∧ k_post − m_0 ≤ 0 ∧ − k_post + m_0 ≤ 0 ∧ −1 + j_post ≤ 0 ∧ 1 − j_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ k_0 − k_post ≤ 0 ∧ − k_0 + k_post ≤ 0 ∧ m2_0 − m2_post ≤ 0 ∧ − m2_0 + m2_post ≤ 0 ∧ pp_0 − pp_post ≤ 0 ∧ − pp_0 + pp_post ≤ 0 ∧ qq_0 − qq_post ≤ 0 ∧ − qq_0 + qq_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0
  9	8	10:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ j_0 − m_0 ≤ 0 ∧ −1 − j_0 + j_post ≤ 0 ∧ 1 + j_0 − j_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ sgd_0 − sgd_post ≤ 0 ∧ − sgd_0 + sgd_post ≤ 0 ∧ sgn_0 − sgn_post ≤ 0 ∧ − sgn_0 + sgn_post ≤ 0 ∧ shn_0 − shn_post ≤ 0 ∧ − shn_0 + shn_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0
  11	9	10:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 + j_post ≤ 0 ∧ 1 − j_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ sgd_0 − sgd_post ≤ 0 ∧ − sgd_0 + sgd_post ≤ 0 ∧ sgn_0 − sgn_post ≤ 0 ∧ − sgn_0 + sgn_post ≤ 0 ∧ shn_0 − shn_post ≤ 0 ∧ − shn_0 + shn_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0
  12	10	13:		− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  14	11	11:		1 − m1_0 + n_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  14	12	11:		1 + m1_0 − n_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  14	13	2:		m1_0 − n_0 ≤ 0 ∧ − m1_0 + n_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  13	14	14:		1 − j_0 + m_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  13	15	12:		0 ≤ 0 ∧ 0 ≤ 0 ∧ j_0 − m_0 ≤ 0 ∧ −1 − j_0 + j_post ≤ 0 ∧ 1 + j_0 − j_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0
  15	16	12:		0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 + j_post ≤ 0 ∧ 1 − j_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0
  10	17	9:		− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  16	18	15:		1 − sd_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  16	19	15:		1 + sd_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  16	20	15:		sd_0 ≤ 0 ∧ − sd_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  8	21	16:		1 − j_0 + m_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  8	22	7:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ j_0 − m_0 ≤ 0 ∧ −1 − j_0 + j_post ≤ 0 ∧ 1 + j_0 − j_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ sd_0 − sd_post ≤ 0 ∧ − sd_0 + sd_post ≤ 0 ∧ sxn_0 − sxn_post ≤ 0 ∧ − sxn_0 + sxn_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0
  5	23	3:		− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  6	24	2:		1 − m_0 + n_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  6	25	7:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ m_0 − n_0 ≤ 0 ∧ −1 + m1_post − m_0 ≤ 0 ∧ 1 − m1_post + m_0 ≤ 0 ∧ −1 + j_post ≤ 0 ∧ 1 − j_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ m1_0 − m1_post ≤ 0 ∧ − m1_0 + m1_post ≤ 0 ∧ sd_0 − sd_post ≤ 0 ∧ − sd_0 + sd_post ≤ 0 ∧ sxn_0 − sxn_post ≤ 0 ∧ − sxn_0 + sxn_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0
  1	26	4:		0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 + m_post ≤ 0 ∧ 1 − m_post ≤ 0 ∧ m_0 − m_post ≤ 0 ∧ − m_0 + m_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  17	27	0:		− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  18	28	17:		− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

2 Transition Removal

We remove transitions 0, 1, 2, 13, 24, 26, 27, 28 using the following ranking functions, which are bounded by −25.

3 Location Addition

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

4* 32 4: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − sxn_post + sxn_post ≤ 0 ∧ sxn_post − sxn_post ≤ 0 ∧ − sxn_0 + sxn_0 ≤ 0 ∧ sxn_0 − sxn_0 ≤ 0 ∧ − shn_post + shn_post ≤ 0 ∧ shn_post − shn_post ≤ 0 ∧ − shn_0 + shn_0 ≤ 0 ∧ shn_0 − shn_0 ≤ 0 ∧ − sgn_post + sgn_post ≤ 0 ∧ sgn_post − sgn_post ≤ 0 ∧ − sgn_0 + sgn_0 ≤ 0 ∧ sgn_0 − sgn_0 ≤ 0 ∧ − sgd_post + sgd_post ≤ 0 ∧ sgd_post − sgd_post ≤ 0 ∧ − sgd_0 + sgd_0 ≤ 0 ∧ sgd_0 − sgd_0 ≤ 0 ∧ − sd_post + sd_post ≤ 0 ∧ sd_post − sd_post ≤ 0 ∧ − sd_0 + sd_0 ≤ 0 ∧ sd_0 − sd_0 ≤ 0 ∧ − qt2_post + qt2_post ≤ 0 ∧ qt2_post − qt2_post ≤ 0 ∧ − qt2_0 + qt2_0 ≤ 0 ∧ qt2_0 − qt2_0 ≤ 0 ∧ − qt1_post + qt1_post ≤ 0 ∧ qt1_post − qt1_post ≤ 0 ∧ − qt1_0 + qt1_0 ≤ 0 ∧ qt1_0 − qt1_0 ≤ 0 ∧ − qq_post + qq_post ≤ 0 ∧ qq_post − qq_post ≤ 0 ∧ − qq_0 + qq_0 ≤ 0 ∧ qq_0 − qq_0 ≤ 0 ∧ − pt2_post + pt2_post ≤ 0 ∧ pt2_post − pt2_post ≤ 0 ∧ − pt2_0 + pt2_0 ≤ 0 ∧ pt2_0 − pt2_0 ≤ 0 ∧ − pt1_post + pt1_post ≤ 0 ∧ pt1_post − pt1_post ≤ 0 ∧ − pt1_0 + pt1_0 ≤ 0 ∧ pt1_0 − pt1_0 ≤ 0 ∧ − pp_post + pp_post ≤ 0 ∧ pp_post − pp_post ≤ 0 ∧ − pp_0 + pp_0 ≤ 0 ∧ pp_0 − pp_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − m2_post + m2_post ≤ 0 ∧ m2_post − m2_post ≤ 0 ∧ − m2_0 + m2_0 ≤ 0 ∧ m2_0 − m2_0 ≤ 0 ∧ − m1_post + m1_post ≤ 0 ∧ m1_post − m1_post ≤ 0 ∧ − m1_0 + m1_0 ≤ 0 ∧ m1_0 − m1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0