LTS Termination Proof

by T2Cert

Input

Integer Transition System

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

We consider the following cutpoint-transitions:

4	29	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
5	36	5:	− 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	43	7:	− 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	50	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	57	12:	− 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

and for every transition t, a duplicate t is considered.

2 Transition Removal

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

18:	0
17:	0
0:	0
1:	0
3:	0
4:	0
5:	0
6:	0
7:	0
8:	0
9:	0
10:	0
11:	0
12:	0
13:	0
14:	0
15:	0
16:	0
2:	0
18:	−7
17:	−8
0:	−9
1:	−10
3:	−11
4:	−11
5:	−11
6:	−11
7:	−11
8:	−11
9:	−11
10:	−11
11:	−11
12:	−11
13:	−11
14:	−11
15:	−11
16:	−11
4_var_snapshot:	−11
4*:	−11
5_var_snapshot:	−11
5*:	−11
7_var_snapshot:	−11
7*:	−11
10_var_snapshot:	−11
10*:	−11
12_var_snapshot:	−11
12*:	−11
2:	−23

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

4 Location Addition

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

4 30 4_var_snapshot: − 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

5 Location Addition

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

5* 39 5: − 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 Location Addition

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

5 37 5_var_snapshot: − 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 Location Addition

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

7* 46 7: − 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 Location Addition

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

7 44 7_var_snapshot: − 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 Location Addition

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

10* 53 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

10 Location Addition

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

10 51 10_var_snapshot: − 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

11 Location Addition

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

12* 60 12: − 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 Location Addition

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

12 58 12_var_snapshot: − 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 SCC Decomposition

We consider subproblems for each of the 1 SCC(s) of the program graph.

13.1 SCC Subproblem 1/1

Here we consider the SCC { 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 4_var_snapshot, 4*, 5_var_snapshot, 5*, 7_var_snapshot, 7*, 10_var_snapshot, 10*, 12_var_snapshot, 12* }.

13.1.1 Transition Removal

We remove transition 25 using the following ranking functions, which are bounded by −1.

3:	−16 − 19⋅m_0 + 19⋅n_0
4:	1 − 19⋅m_0 + 19⋅n_0
5:	−16 − 19⋅m_0 + 19⋅n_0
6:	−19⋅m_0 + 19⋅n_0
7:	−10 − 19⋅m_0 + 19⋅n_0
8:	−10 − 19⋅m_0 + 19⋅n_0
9:	−15 − 19⋅m_0 + 19⋅n_0
10:	−15 − 19⋅m_0 + 19⋅n_0
11:	−14 − 19⋅m_0 + 19⋅n_0
12:	−12 − 19⋅m_0 + 19⋅n_0
13:	−12 − 19⋅m_0 + 19⋅n_0
14:	−13 − 19⋅m_0 + 19⋅n_0
15:	−11 − 19⋅m_0 + 19⋅n_0
16:	−10 − 19⋅m_0 + 19⋅n_0
4_var_snapshot:	1 − 19⋅m_0 + 19⋅n_0
4*:	2 − 19⋅m_0 + 19⋅n_0
5_var_snapshot:	−16 − 19⋅m_0 + 19⋅n_0
5*:	−16 − 19⋅m_0 + 19⋅n_0
7_var_snapshot:	−10 − 19⋅m_0 + 19⋅n_0
7*:	−10 − 19⋅m_0 + 19⋅n_0
10_var_snapshot:	−15 − 19⋅m_0 + 19⋅n_0
10*:	−15 − 19⋅m_0 + 19⋅n_0
12_var_snapshot:	−12 − 19⋅m_0 + 19⋅n_0
12*:	−12 − 19⋅m_0 + 19⋅n_0

13.1.2 Transition Removal

We remove transitions 7, 9, 11, 12, 14, 16, 19, 20, 21 using the following ranking functions, which are bounded by −5.

3:	−8⋅j_0 + 3⋅k_0 − 3⋅m_0
4:	1 − 8⋅j_0 + 3⋅k_0 − 3⋅m_post
5:	2 − 8⋅j_0 + 3⋅k_0 − 3⋅m_0
6:	−1 − 8⋅j_0 + 3⋅k_0 − 3⋅m_post
7:	2
8:	2
9:	−4
10:	−4
11:	−3
12:	−1
13:	−1
14:	−2
15:	0
16:	1
4_var_snapshot:	−8⋅j_0 + 3⋅k_0 − 3⋅m_post
4*:	2 − 8⋅j_0 + 3⋅k_0 − 3⋅m_post
5_var_snapshot:	1 − 8⋅j_0 + 3⋅k_0 − 3⋅m_0
5*:	3 − 8⋅j_0 + 3⋅k_0 − 3⋅m_0
7_var_snapshot:	2
7*:	2
10_var_snapshot:	−4
10*:	−4
12_var_snapshot:	−1
12*:	−1

13.1.3 Transition Removal

We remove transition 22 using the following ranking functions, which are bounded by −2.

3:	−1 − j_0 + 3⋅k_0 + m2_0
4:	−3 − j_0 + 3⋅k_0 + m2_0
5:	1 − j_0 + 3⋅k_0 + m2_0
6:	−5 − j_0 + 3⋅k_0 + m2_0
7:	1 − 4⋅j_0 + 4⋅m_0
8:	−1 − 4⋅j_0 + 4⋅m_0
9:	−2 − 3⋅j_0 + 3⋅m_0
10:	−3⋅j_0 + 3⋅m_0
11:	0
12:	−3⋅j_0 + 3⋅m_0
13:	−2 − 3⋅j_0 + 3⋅m_0
14:	0
15:	0
16:	0
4_var_snapshot:	−4 − j_0 + 3⋅k_0 + m2_0
4*:	−2 − j_0 + 3⋅k_0 + m2_0
5_var_snapshot:	− j_0 + 3⋅k_0 + m2_0
5*:	2 − j_0 + 3⋅k_0 + m2_0
7_var_snapshot:	−4⋅j_0 + 4⋅m_0
7*:	2 − 4⋅j_0 + 4⋅m_0
10_var_snapshot:	−1 − 3⋅j_0 + 3⋅m_0
10*:	1 − 3⋅j_0 + 3⋅m_0
12_var_snapshot:	−1 − 3⋅j_0 + 3⋅m_0
12*:	1 − 3⋅j_0 + 3⋅m_0

13.1.4 Transition Removal

We remove transitions 44, 46, 6, 18 using the following ranking functions, which are bounded by −2.

3:	−1 − 4⋅j_0 + 4⋅m2_0
4:	−3 − 4⋅j_0 + 4⋅m2_0
5:	1 − 4⋅j_0 + 4⋅m2_0
6:	−5 − 4⋅j_0 + 4⋅m2_0
7:	0
8:	−2
9:	0
10:	0
11:	0
12:	0
13:	0
14:	0
15:	0
16:	1
4_var_snapshot:	−4 − 4⋅j_0 + 4⋅m2_0
4*:	−2 − 4⋅j_0 + 4⋅m2_0
5_var_snapshot:	−4⋅j_0 + 4⋅m2_0
5*:	2 − 4⋅j_0 + 4⋅m2_0
7_var_snapshot:	−1
7*:	1
10_var_snapshot:	0
10*:	0
12_var_snapshot:	0
12*:	0

13.1.5 Transition Removal

We remove transition 15 using the following ranking functions, which are bounded by −1.

3:	−1 − 2⋅j_0 + k_0 + 2⋅m2_0
4:	−3 − 2⋅j_0 + k_0 + 2⋅m2_0
5:	−2⋅j_0 + k_0 + 2⋅m2_0
6:	−5 − 2⋅j_0 + k_0 + 2⋅m2_0
7:	0
8:	0
9:	0
10:	0
11:	0
12:	1 − 2⋅j_0 + 2⋅m_0
13:	−2⋅j_0 + 2⋅m_0
14:	0
15:	0
16:	0
4_var_snapshot:	−4 − 2⋅j_0 + k_0 + 2⋅m2_0
4*:	−2 − 2⋅j_0 + k_0 + 2⋅m2_0
5_var_snapshot:	−2⋅j_0 + k_0 + 2⋅m2_0
5*:	1 − 2⋅j_0 + k_0 + 2⋅m2_0
7_var_snapshot:	0
7*:	0
10_var_snapshot:	0
10*:	0
12_var_snapshot:	−2⋅j_0 + 2⋅m_0
12*:	1 − 2⋅j_0 + 2⋅m_0

13.1.6 Transition Removal

We remove transitions 58, 60, 8, 10 using the following ranking functions, which are bounded by −3.

3:	−1 − 3⋅j_0 + 3⋅m2_0
4:	−3 − 3⋅j_0 + 3⋅m2_0
5:	1 − 3⋅j_0 + 3⋅m2_0
6:	−5 − 3⋅j_0 + 3⋅m2_0
7:	0
8:	0
9:	−2 − 3⋅j_0 + 3⋅m_0
10:	−1 − 3⋅j_0 + 3⋅m_0
11:	0
12:	0
13:	−2
14:	0
15:	0
16:	0
4_var_snapshot:	−4 − 3⋅j_0 + 3⋅m2_0
4*:	−2 − 3⋅j_0 + 3⋅m2_0
5_var_snapshot:	−3⋅j_0 + 3⋅m2_0
5*:	2 − 3⋅j_0 + 3⋅m2_0
7_var_snapshot:	0
7*:	0
10_var_snapshot:	−2 − 3⋅j_0 + 3⋅m_0
10*:	−3⋅j_0 + 3⋅m_0
12_var_snapshot:	−1
12*:	1

13.1.7 Transition Removal

We remove transitions 51, 53, 17 using the following ranking functions, which are bounded by −2.

3:	−1 − 2⋅j_0 + 2⋅k_0 + 2⋅m2_0
4:	−3 − 2⋅j_0 + 2⋅k_0 + 2⋅m2_0
5:	1 − 2⋅j_0 + 2⋅k_0 + 2⋅m2_0
6:	−5 − 2⋅j_0 + 2⋅k_0 + 2⋅m2_0
7:	0
8:	0
9:	−2
10:	0
11:	0
12:	0
13:	0
14:	0
15:	0
16:	0
4_var_snapshot:	−4 − 2⋅j_0 + 2⋅k_0 + 2⋅m2_0
4*:	−2 − 2⋅j_0 + 2⋅k_0 + 2⋅m2_0
5_var_snapshot:	−2⋅j_0 + 2⋅k_0 + 2⋅m2_0
5*:	2 − 2⋅j_0 + 2⋅k_0 + 2⋅m2_0
7_var_snapshot:	0
7*:	0
10_var_snapshot:	−1
10*:	1
12_var_snapshot:	0
12*:	0

13.1.8 Transition Removal

We remove transition 4 using the following ranking functions, which are bounded by −2.

3:	−1 − 4⋅j_0 + 4⋅m2_0
4:	−3 − 4⋅j_0 + 4⋅m2_0
5:	1 − 4⋅j_0 + 4⋅m2_0
6:	−5 − 4⋅j_0 + 4⋅m2_0
7:	0
8:	0
9:	0
10:	0
11:	0
12:	0
13:	0
14:	0
15:	0
16:	0
4_var_snapshot:	−4 − 4⋅j_0 + 4⋅m2_0
4*:	−2 − 4⋅j_0 + 4⋅m2_0
5_var_snapshot:	−4⋅j_0 + 4⋅m2_0
5*:	2 − 4⋅j_0 + 4⋅m2_0
7_var_snapshot:	0
7*:	0
10_var_snapshot:	0
10*:	0
12_var_snapshot:	0
12*:	0

13.1.9 Transition Removal

We remove transitions 30, 32, 37, 39, 3, 5, 23 using the following ranking functions, which are bounded by −5.

3:	−1
4:	−3
5:	1
6:	−5
7:	0
8:	0
9:	0
10:	0
11:	0
12:	0
13:	0
14:	0
15:	0
16:	0
4_var_snapshot:	−4
4*:	−2
5_var_snapshot:	0
5*:	2
7_var_snapshot:	0
7*:	0
10_var_snapshot:	0
10*:	0
12_var_snapshot:	0
12*:	0

13.1.10 Splitting Cut-Point Transitions

We consider 5 subproblems corresponding to sets of cut-point transitions as follows.

13.1.10.1 Cut-Point Subproblem 1/5

Here we consider cut-point transition 29.

13.1.10.1.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

13.1.10.2 Cut-Point Subproblem 2/5

Here we consider cut-point transition 36.

13.1.10.2.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

13.1.10.3 Cut-Point Subproblem 3/5

Here we consider cut-point transition 43.

13.1.10.3.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

13.1.10.4 Cut-Point Subproblem 4/5

Here we consider cut-point transition 50.

13.1.10.4.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

13.1.10.5 Cut-Point Subproblem 5/5

Here we consider cut-point transition 57.

13.1.10.5.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

Tool configuration

T2Cert

version: 1.0