LTS Termination Proof

by T2Cert

Input

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

  0	0	1:		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
  2	1	1:		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
  2	2	3:		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
  3	3	2:		− 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
  4	4	0:		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
  4	5	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
  4	6	5:		−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
  6	7	3:		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
  6	8	7:		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
  7	9	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
  8	10	7:		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
  9	11	8:		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
  9	12	8:		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
  9	13	5:		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
  10	14	9:		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
  10	15	11:		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
  11	16	10:		− 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
  12	17	11:		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
  13	18	12:		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
  13	19	12:		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
  13	20	12:		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
  14	21	13:		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
  14	22	15:		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
  16	23	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
  15	24	14:		− 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
  17	25	5:		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
  17	26	15:		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	27	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
  18	28	16:		− 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, 4, 5, 6, 13, 23, 25, 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.

1* 32 1: − 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