(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS eval_sipmamergesort_init_start)) (VAR v_52 v_53 v_6 v_i_5 v_m_0 v_n v_p_0 v_q_1 v_q_3 v_r_1 v_r_3 v_up_0) (RULES eval_sipmamergesort_init_start(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb0_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_bb0_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_0(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_0(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_1(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_1(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_2(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_2(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_3(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_3(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_4(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_4(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_5(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_5(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_6(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_6(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_7(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_7(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_8(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_8(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_9(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_9(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_10(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_10(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_11(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_11(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_12(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_12(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_13(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_13(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_14(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_14(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_15(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_15(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_16(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_16(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_17(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_17(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_18(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_18(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_19(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_19(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_20(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_20(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_21(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_21(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_22(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_22(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_23(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_23(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_24(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_24(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_25(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_25(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_26(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) eval_sipmamergesort_init_26(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb1_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, 1, v_q_1, v_q_3, v_r_1, v_r_3, 1)) eval_sipmamergesort_init_bb1_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb2_in(v_52, v_53, v_6, v_i_5, v_n, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ v_up_0 > 0 ] eval_sipmamergesort_init_bb1_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb2_in(v_52, v_53, v_6, v_i_5, v_n, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ v_up_0 = 0 ] eval_sipmamergesort_init_bb2_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb3_in(v_52, v_53, v_m_0 - 2*v_p_0, v_i_5, v_m_0, v_n, v_p_0, v_p_0, v_q_3, v_p_0, v_r_3, v_up_0)) [ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ v_m_0 >= v_p_0 /\ v_m_0 - v_p_0 >= v_p_0 ] eval_sipmamergesort_init_bb2_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb3_in(v_52, v_53, 0, v_i_5, v_m_0, v_n, v_p_0, v_p_0, v_q_3, v_m_0 - v_p_0, v_r_3, v_up_0)) [ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ v_m_0 >= v_p_0 /\ v_m_0 - v_p_0 < v_p_0 ] eval_sipmamergesort_init_bb2_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb3_in(v_52, v_53, 0, v_i_5, v_m_0, v_n, v_p_0, v_m_0, v_q_3, 0, v_r_3, v_up_0)) [ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ v_m_0 < v_p_0 /\ 0 < v_p_0 ] eval_sipmamergesort_init_bb3_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb4_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ v_q_1 > 0 /\ v_r_1 > 0 ] eval_sipmamergesort_init_bb3_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb7_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_1, v_up_0)) [ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ v_q_1 <= 0 ] eval_sipmamergesort_init_bb3_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb7_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_1, v_up_0)) [ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ v_r_1 <= 0 ] eval_sipmamergesort_init_bb4_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb5_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_q_1 - 1 >= 0 /\ v_p_0 + v_q_1 - 2 >= 0 /\ v_m_0 + v_q_1 - 2 >= 0 /\ v_up_0 + v_q_1 - 1 >= 0 /\ -v_up_0 + v_q_1 >= 0 /\ v_r_1 + v_q_1 - 2 >= 0 /\ v_p_0 - 1 >= 0 /\ v_m_0 + v_p_0 - 2 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ v_r_1 + v_p_0 - 2 >= 0 /\ v_m_0 - 1 >= 0 /\ v_up_0 + v_m_0 - 1 >= 0 /\ -v_up_0 + v_m_0 >= 0 /\ v_r_1 + v_m_0 - 2 >= 0 /\ -v_up_0 + 1 >= 0 /\ v_r_1 - v_up_0 >= 0 /\ v_up_0 >= 0 /\ v_r_1 + v_up_0 - 1 >= 0 /\ v_r_1 - 1 >= 0 /\ nondef_0 < nondef_1 ] eval_sipmamergesort_init_bb4_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb6_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_q_1 - 1 >= 0 /\ v_p_0 + v_q_1 - 2 >= 0 /\ v_m_0 + v_q_1 - 2 >= 0 /\ v_up_0 + v_q_1 - 1 >= 0 /\ -v_up_0 + v_q_1 >= 0 /\ v_r_1 + v_q_1 - 2 >= 0 /\ v_p_0 - 1 >= 0 /\ v_m_0 + v_p_0 - 2 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ v_r_1 + v_p_0 - 2 >= 0 /\ v_m_0 - 1 >= 0 /\ v_up_0 + v_m_0 - 1 >= 0 /\ -v_up_0 + v_m_0 >= 0 /\ v_r_1 + v_m_0 - 2 >= 0 /\ -v_up_0 + 1 >= 0 /\ v_r_1 - v_up_0 >= 0 /\ v_up_0 >= 0 /\ v_r_1 + v_up_0 - 1 >= 0 /\ v_r_1 - 1 >= 0 /\ nondef_0 >= nondef_1 ] eval_sipmamergesort_init_bb5_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb3_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1 - 1, v_q_3, v_r_1, v_r_3, v_up_0)) [ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_q_1 - 1 >= 0 /\ v_p_0 + v_q_1 - 2 >= 0 /\ v_m_0 + v_q_1 - 2 >= 0 /\ v_up_0 + v_q_1 - 1 >= 0 /\ -v_up_0 + v_q_1 >= 0 /\ v_r_1 + v_q_1 - 2 >= 0 /\ v_p_0 - 1 >= 0 /\ v_m_0 + v_p_0 - 2 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ v_r_1 + v_p_0 - 2 >= 0 /\ v_m_0 - 1 >= 0 /\ v_up_0 + v_m_0 - 1 >= 0 /\ -v_up_0 + v_m_0 >= 0 /\ v_r_1 + v_m_0 - 2 >= 0 /\ -v_up_0 + 1 >= 0 /\ v_r_1 - v_up_0 >= 0 /\ v_up_0 >= 0 /\ v_r_1 + v_up_0 - 1 >= 0 /\ v_r_1 - 1 >= 0 ] eval_sipmamergesort_init_bb6_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb3_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1 - 1, v_r_3, v_up_0)) [ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_q_1 - 1 >= 0 /\ v_p_0 + v_q_1 - 2 >= 0 /\ v_m_0 + v_q_1 - 2 >= 0 /\ v_up_0 + v_q_1 - 1 >= 0 /\ -v_up_0 + v_q_1 >= 0 /\ v_r_1 + v_q_1 - 2 >= 0 /\ v_p_0 - 1 >= 0 /\ v_m_0 + v_p_0 - 2 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ v_r_1 + v_p_0 - 2 >= 0 /\ v_m_0 - 1 >= 0 /\ v_up_0 + v_m_0 - 1 >= 0 /\ -v_up_0 + v_m_0 >= 0 /\ v_r_1 + v_m_0 - 2 >= 0 /\ -v_up_0 + 1 >= 0 /\ v_r_1 - v_up_0 >= 0 /\ v_up_0 >= 0 /\ v_r_1 + v_up_0 - 1 >= 0 /\ v_r_1 - 1 >= 0 ] eval_sipmamergesort_init_bb7_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb8_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ v_r_1 - v_r_3 >= 0 /\ v_r_3 > 0 ] eval_sipmamergesort_init_bb7_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb9_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_1, v_r_1, v_r_3, v_up_0)) [ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ v_r_1 - v_r_3 >= 0 /\ v_r_3 <= 0 ] eval_sipmamergesort_init_bb8_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb7_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3 - 1, v_up_0)) [ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ v_r_3 + v_p_0 - 2 >= 0 /\ v_r_1 + v_p_0 - 2 >= 0 /\ -v_up_0 + 1 >= 0 /\ v_r_3 - v_up_0 >= 0 /\ v_r_1 - v_up_0 >= 0 /\ v_up_0 >= 0 /\ v_r_3 + v_up_0 - 1 >= 0 /\ v_r_1 + v_up_0 - 1 >= 0 /\ v_r_1 - v_r_3 >= 0 /\ v_r_3 - 1 >= 0 /\ v_r_1 + v_r_3 - 2 >= 0 /\ v_r_1 - 1 >= 0 ] eval_sipmamergesort_init_bb9_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb10_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 /\ v_q_3 > 0 ] eval_sipmamergesort_init_bb9_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb11_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 /\ v_q_3 <= 0 ] eval_sipmamergesort_init_bb10_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb9_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3 - 1, v_r_1, v_r_3, v_up_0)) [ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ v_q_3 - 1 >= 0 /\ v_q_1 + v_q_3 - 2 >= 0 /\ v_p_0 + v_q_3 - 2 >= 0 /\ v_m_0 + v_q_3 - 2 >= 0 /\ v_up_0 + v_q_3 - 1 >= 0 /\ -v_up_0 + v_q_3 >= 0 /\ -v_r_3 + v_q_3 - 1 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_q_1 - 1 >= 0 /\ v_p_0 + v_q_1 - 2 >= 0 /\ v_m_0 + v_q_1 - 2 >= 0 /\ v_up_0 + v_q_1 - 1 >= 0 /\ -v_up_0 + v_q_1 >= 0 /\ -v_r_3 + v_q_1 - 1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_m_0 + v_p_0 - 2 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ v_m_0 - 1 >= 0 /\ v_up_0 + v_m_0 - 1 >= 0 /\ -v_up_0 + v_m_0 >= 0 /\ -v_r_3 + v_m_0 - 1 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 ] eval_sipmamergesort_init_bb11_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_77(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ v_up_0 - v_q_3 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 ] eval_sipmamergesort_init_77(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_78(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ v_up_0 - v_q_3 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 ] eval_sipmamergesort_init_78(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_79(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ v_up_0 - v_q_3 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 ] eval_sipmamergesort_init_79(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_80(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ v_up_0 - v_q_3 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 ] eval_sipmamergesort_init_80(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_81(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ v_up_0 - v_q_3 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 ] eval_sipmamergesort_init_81(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb2_in(v_52, v_53, v_6, v_i_5, v_6, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ v_up_0 - v_q_3 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 /\ v_6 > 0 ] eval_sipmamergesort_init_81(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb12_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ v_up_0 - v_q_3 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 /\ v_6 <= 0 ] eval_sipmamergesort_init_bb12_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_83(-v_up_0 + 1, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ -v_6 - v_q_3 >= 0 /\ v_up_0 - v_q_3 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_p_0 - 1 >= 0 /\ -v_6 + v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ -v_6 >= 0 /\ v_up_0 - v_6 >= 0 /\ -v_up_0 - v_6 + 1 >= 0 /\ -v_r_3 - v_6 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 ] eval_sipmamergesort_init_83(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_84(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ -v_6 - v_q_3 >= 0 /\ v_up_0 - v_q_3 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_52 - v_q_3 >= 0 /\ -v_52 - v_q_3 + 1 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_p_0 - 1 >= 0 /\ -v_6 + v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ v_52 + v_p_0 - 1 >= 0 /\ -v_52 + v_p_0 - 1 >= 0 /\ -v_6 >= 0 /\ v_up_0 - v_6 >= 0 /\ -v_up_0 - v_6 + 1 >= 0 /\ -v_r_3 - v_6 >= 0 /\ v_52 - v_6 >= 0 /\ -v_52 - v_6 + 1 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_52 - v_up_0 + 1 >= 0 /\ -v_52 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ v_52 + v_up_0 - 1 >= 0 /\ -v_52 + v_up_0 + 1 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 /\ v_52 - v_r_3 >= 0 /\ -v_52 - v_r_3 + 1 >= 0 /\ -v_52 + 1 >= 0 /\ v_52 >= 0 ] eval_sipmamergesort_init_84(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_85(v_52, 2*v_p_0, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ -v_6 - v_q_3 >= 0 /\ v_up_0 - v_q_3 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_52 - v_q_3 >= 0 /\ -v_52 - v_q_3 + 1 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_p_0 - 1 >= 0 /\ -v_6 + v_p_0 - 1 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ v_52 + v_p_0 - 1 >= 0 /\ -v_52 + v_p_0 - 1 >= 0 /\ -v_6 >= 0 /\ v_up_0 - v_6 >= 0 /\ -v_up_0 - v_6 + 1 >= 0 /\ -v_r_3 - v_6 >= 0 /\ v_52 - v_6 >= 0 /\ -v_52 - v_6 + 1 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_52 - v_up_0 + 1 >= 0 /\ -v_52 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ v_52 + v_up_0 - 1 >= 0 /\ -v_52 + v_up_0 + 1 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 /\ v_52 - v_r_3 >= 0 /\ -v_52 - v_r_3 + 1 >= 0 /\ -v_52 + 1 >= 0 /\ v_52 >= 0 ] eval_sipmamergesort_init_85(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_86(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ -v_6 - v_q_3 >= 0 /\ v_53 - v_q_3 - 2 >= 0 /\ v_up_0 - v_q_3 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_52 - v_q_3 >= 0 /\ -v_52 - v_q_3 + 1 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_53 - v_q_1 - 1 >= 0 /\ v_53 - v_p_0 - 1 >= 0 /\ v_p_0 - 1 >= 0 /\ -v_6 + v_p_0 - 1 >= 0 /\ v_53 + v_p_0 - 3 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ v_52 + v_p_0 - 1 >= 0 /\ -v_52 + v_p_0 - 1 >= 0 /\ -v_6 >= 0 /\ v_53 - v_6 - 2 >= 0 /\ v_up_0 - v_6 >= 0 /\ -v_up_0 - v_6 + 1 >= 0 /\ -v_r_3 - v_6 >= 0 /\ v_52 - v_6 >= 0 /\ -v_52 - v_6 + 1 >= 0 /\ v_53 - 2 >= 0 /\ v_up_0 + v_53 - 3 >= 0 /\ -v_up_0 + v_53 - 1 >= 0 /\ -v_r_3 + v_53 - 2 >= 0 /\ v_52 + v_53 - 2 >= 0 /\ -v_52 + v_53 - 2 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_52 - v_up_0 + 1 >= 0 /\ -v_52 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ v_52 + v_up_0 - 1 >= 0 /\ -v_52 + v_up_0 + 1 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 /\ v_52 - v_r_3 >= 0 /\ -v_52 - v_r_3 + 1 >= 0 /\ -v_52 + 1 >= 0 /\ v_52 >= 0 ] eval_sipmamergesort_init_86(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb1_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_53, v_q_1, v_q_3, v_r_1, v_r_3, v_52)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ -v_6 - v_q_3 >= 0 /\ v_53 - v_q_3 - 2 >= 0 /\ v_up_0 - v_q_3 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_52 - v_q_3 >= 0 /\ -v_52 - v_q_3 + 1 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_53 - v_q_1 - 1 >= 0 /\ v_53 - v_p_0 - 1 >= 0 /\ v_p_0 - 1 >= 0 /\ -v_6 + v_p_0 - 1 >= 0 /\ v_53 + v_p_0 - 3 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ v_52 + v_p_0 - 1 >= 0 /\ -v_52 + v_p_0 - 1 >= 0 /\ -v_6 >= 0 /\ v_53 - v_6 - 2 >= 0 /\ v_up_0 - v_6 >= 0 /\ -v_up_0 - v_6 + 1 >= 0 /\ -v_r_3 - v_6 >= 0 /\ v_52 - v_6 >= 0 /\ -v_52 - v_6 + 1 >= 0 /\ v_53 - 2 >= 0 /\ v_up_0 + v_53 - 3 >= 0 /\ -v_up_0 + v_53 - 1 >= 0 /\ -v_r_3 + v_53 - 2 >= 0 /\ v_52 + v_53 - 2 >= 0 /\ -v_52 + v_53 - 2 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_52 - v_up_0 + 1 >= 0 /\ -v_52 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ v_52 + v_up_0 - 1 >= 0 /\ -v_52 + v_up_0 + 1 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 /\ v_52 - v_r_3 >= 0 /\ -v_52 - v_r_3 + 1 >= 0 /\ -v_52 + 1 >= 0 /\ v_52 >= 0 /\ v_53 < v_n ] eval_sipmamergesort_init_86(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb13_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ -v_6 - v_q_3 >= 0 /\ v_53 - v_q_3 - 2 >= 0 /\ v_up_0 - v_q_3 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_52 - v_q_3 >= 0 /\ -v_52 - v_q_3 + 1 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_53 - v_q_1 - 1 >= 0 /\ v_53 - v_p_0 - 1 >= 0 /\ v_p_0 - 1 >= 0 /\ -v_6 + v_p_0 - 1 >= 0 /\ v_53 + v_p_0 - 3 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ v_52 + v_p_0 - 1 >= 0 /\ -v_52 + v_p_0 - 1 >= 0 /\ -v_6 >= 0 /\ v_53 - v_6 - 2 >= 0 /\ v_up_0 - v_6 >= 0 /\ -v_up_0 - v_6 + 1 >= 0 /\ -v_r_3 - v_6 >= 0 /\ v_52 - v_6 >= 0 /\ -v_52 - v_6 + 1 >= 0 /\ v_53 - 2 >= 0 /\ v_up_0 + v_53 - 3 >= 0 /\ -v_up_0 + v_53 - 1 >= 0 /\ -v_r_3 + v_53 - 2 >= 0 /\ v_52 + v_53 - 2 >= 0 /\ -v_52 + v_53 - 2 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_52 - v_up_0 + 1 >= 0 /\ -v_52 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ v_52 + v_up_0 - 1 >= 0 /\ -v_52 + v_up_0 + 1 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 /\ v_52 - v_r_3 >= 0 /\ -v_52 - v_r_3 + 1 >= 0 /\ -v_52 + 1 >= 0 /\ v_52 >= 0 /\ v_53 >= v_n ] eval_sipmamergesort_init_bb13_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb14_in(v_52, v_53, v_6, 1, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ -v_6 - v_q_3 >= 0 /\ v_53 - v_q_3 - 2 >= 0 /\ v_up_0 - v_q_3 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_52 - v_q_3 >= 0 /\ -v_52 - v_q_3 + 1 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_53 - v_q_1 - 1 >= 0 /\ v_53 - v_p_0 - 1 >= 0 /\ v_p_0 - 1 >= 0 /\ -v_6 + v_p_0 - 1 >= 0 /\ v_53 + v_p_0 - 3 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ v_52 + v_p_0 - 1 >= 0 /\ -v_52 + v_p_0 - 1 >= 0 /\ v_53 - v_n >= 0 /\ -v_6 >= 0 /\ v_53 - v_6 - 2 >= 0 /\ v_up_0 - v_6 >= 0 /\ -v_up_0 - v_6 + 1 >= 0 /\ -v_r_3 - v_6 >= 0 /\ v_52 - v_6 >= 0 /\ -v_52 - v_6 + 1 >= 0 /\ v_53 - 2 >= 0 /\ v_up_0 + v_53 - 3 >= 0 /\ -v_up_0 + v_53 - 1 >= 0 /\ -v_r_3 + v_53 - 2 >= 0 /\ v_52 + v_53 - 2 >= 0 /\ -v_52 + v_53 - 2 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_52 - v_up_0 + 1 >= 0 /\ -v_52 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ v_52 + v_up_0 - 1 >= 0 /\ -v_52 + v_up_0 + 1 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 /\ v_52 - v_r_3 >= 0 /\ -v_52 - v_r_3 + 1 >= 0 /\ -v_52 + 1 >= 0 /\ v_52 >= 0 /\ v_52 = 0 ] eval_sipmamergesort_init_bb13_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb16_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ -v_6 - v_q_3 >= 0 /\ v_53 - v_q_3 - 2 >= 0 /\ v_up_0 - v_q_3 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_52 - v_q_3 >= 0 /\ -v_52 - v_q_3 + 1 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_53 - v_q_1 - 1 >= 0 /\ v_53 - v_p_0 - 1 >= 0 /\ v_p_0 - 1 >= 0 /\ -v_6 + v_p_0 - 1 >= 0 /\ v_53 + v_p_0 - 3 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ v_52 + v_p_0 - 1 >= 0 /\ -v_52 + v_p_0 - 1 >= 0 /\ v_53 - v_n >= 0 /\ -v_6 >= 0 /\ v_53 - v_6 - 2 >= 0 /\ v_up_0 - v_6 >= 0 /\ -v_up_0 - v_6 + 1 >= 0 /\ -v_r_3 - v_6 >= 0 /\ v_52 - v_6 >= 0 /\ -v_52 - v_6 + 1 >= 0 /\ v_53 - 2 >= 0 /\ v_up_0 + v_53 - 3 >= 0 /\ -v_up_0 + v_53 - 1 >= 0 /\ -v_r_3 + v_53 - 2 >= 0 /\ v_52 + v_53 - 2 >= 0 /\ -v_52 + v_53 - 2 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_52 - v_up_0 + 1 >= 0 /\ -v_52 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ v_52 + v_up_0 - 1 >= 0 /\ -v_52 + v_up_0 + 1 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 /\ v_52 - v_r_3 >= 0 /\ -v_52 - v_r_3 + 1 >= 0 /\ -v_52 + 1 >= 0 /\ v_52 >= 0 /\ v_52 > 0 ] eval_sipmamergesort_init_bb14_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb15_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ v_i_5 - v_q_3 - 1 >= 0 /\ -v_6 - v_q_3 >= 0 /\ v_53 - v_q_3 - 2 >= 0 /\ v_up_0 - v_q_3 - 1 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_52 - v_q_3 >= 0 /\ -v_52 - v_q_3 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_53 - v_q_1 - 1 >= 0 /\ v_53 - v_p_0 - 1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_i_5 + v_p_0 - 2 >= 0 /\ -v_6 + v_p_0 - 1 >= 0 /\ v_53 + v_p_0 - 3 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ v_52 + v_p_0 - 1 >= 0 /\ -v_52 + v_p_0 - 1 >= 0 /\ v_53 - v_n >= 0 /\ v_i_5 - 1 >= 0 /\ -v_6 + v_i_5 - 1 >= 0 /\ v_53 + v_i_5 - 3 >= 0 /\ v_up_0 + v_i_5 - 2 >= 0 /\ -v_up_0 + v_i_5 >= 0 /\ -v_r_3 + v_i_5 - 1 >= 0 /\ v_52 + v_i_5 - 1 >= 0 /\ -v_52 + v_i_5 - 1 >= 0 /\ -v_6 >= 0 /\ v_53 - v_6 - 2 >= 0 /\ v_up_0 - v_6 - 1 >= 0 /\ -v_up_0 - v_6 + 1 >= 0 /\ -v_r_3 - v_6 >= 0 /\ v_52 - v_6 >= 0 /\ -v_52 - v_6 >= 0 /\ v_53 - 2 >= 0 /\ v_up_0 + v_53 - 3 >= 0 /\ -v_up_0 + v_53 - 1 >= 0 /\ -v_r_3 + v_53 - 2 >= 0 /\ v_52 + v_53 - 2 >= 0 /\ -v_52 + v_53 - 2 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_52 - v_up_0 + 1 >= 0 /\ -v_52 - v_up_0 + 1 >= 0 /\ v_up_0 - 1 >= 0 /\ -v_r_3 + v_up_0 - 1 >= 0 /\ v_52 + v_up_0 - 1 >= 0 /\ -v_52 + v_up_0 - 1 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 /\ v_52 - v_r_3 >= 0 /\ -v_52 - v_r_3 >= 0 /\ -v_52 >= 0 /\ v_52 >= 0 /\ v_i_5 <= v_n ] eval_sipmamergesort_init_bb14_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb16_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ v_i_5 - v_q_3 - 1 >= 0 /\ -v_6 - v_q_3 >= 0 /\ v_53 - v_q_3 - 2 >= 0 /\ v_up_0 - v_q_3 - 1 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_52 - v_q_3 >= 0 /\ -v_52 - v_q_3 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_53 - v_q_1 - 1 >= 0 /\ v_53 - v_p_0 - 1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_i_5 + v_p_0 - 2 >= 0 /\ -v_6 + v_p_0 - 1 >= 0 /\ v_53 + v_p_0 - 3 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ v_52 + v_p_0 - 1 >= 0 /\ -v_52 + v_p_0 - 1 >= 0 /\ v_53 - v_n >= 0 /\ v_i_5 - 1 >= 0 /\ -v_6 + v_i_5 - 1 >= 0 /\ v_53 + v_i_5 - 3 >= 0 /\ v_up_0 + v_i_5 - 2 >= 0 /\ -v_up_0 + v_i_5 >= 0 /\ -v_r_3 + v_i_5 - 1 >= 0 /\ v_52 + v_i_5 - 1 >= 0 /\ -v_52 + v_i_5 - 1 >= 0 /\ -v_6 >= 0 /\ v_53 - v_6 - 2 >= 0 /\ v_up_0 - v_6 - 1 >= 0 /\ -v_up_0 - v_6 + 1 >= 0 /\ -v_r_3 - v_6 >= 0 /\ v_52 - v_6 >= 0 /\ -v_52 - v_6 >= 0 /\ v_53 - 2 >= 0 /\ v_up_0 + v_53 - 3 >= 0 /\ -v_up_0 + v_53 - 1 >= 0 /\ -v_r_3 + v_53 - 2 >= 0 /\ v_52 + v_53 - 2 >= 0 /\ -v_52 + v_53 - 2 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_52 - v_up_0 + 1 >= 0 /\ -v_52 - v_up_0 + 1 >= 0 /\ v_up_0 - 1 >= 0 /\ -v_r_3 + v_up_0 - 1 >= 0 /\ v_52 + v_up_0 - 1 >= 0 /\ -v_52 + v_up_0 - 1 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 /\ v_52 - v_r_3 >= 0 /\ -v_52 - v_r_3 >= 0 /\ -v_52 >= 0 /\ v_52 >= 0 /\ v_i_5 > v_n ] eval_sipmamergesort_init_bb15_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_bb14_in(v_52, v_53, v_6, v_i_5 + 1, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_n - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ v_i_5 - v_q_3 - 1 >= 0 /\ -v_6 - v_q_3 >= 0 /\ v_53 - v_q_3 - 2 >= 0 /\ v_up_0 - v_q_3 - 1 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_52 - v_q_3 >= 0 /\ -v_52 - v_q_3 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_53 - v_q_1 - 1 >= 0 /\ v_53 - v_p_0 - 1 >= 0 /\ v_p_0 - 1 >= 0 /\ v_n + v_p_0 - 2 >= 0 /\ v_i_5 + v_p_0 - 2 >= 0 /\ -v_6 + v_p_0 - 1 >= 0 /\ v_53 + v_p_0 - 3 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ v_52 + v_p_0 - 1 >= 0 /\ -v_52 + v_p_0 - 1 >= 0 /\ v_53 - v_n >= 0 /\ v_n - 1 >= 0 /\ v_i_5 + v_n - 2 >= 0 /\ -v_i_5 + v_n >= 0 /\ -v_6 + v_n - 1 >= 0 /\ v_53 + v_n - 3 >= 0 /\ v_up_0 + v_n - 2 >= 0 /\ -v_up_0 + v_n >= 0 /\ -v_r_3 + v_n - 1 >= 0 /\ v_52 + v_n - 1 >= 0 /\ -v_52 + v_n - 1 >= 0 /\ v_53 - v_i_5 >= 0 /\ v_i_5 - 1 >= 0 /\ -v_6 + v_i_5 - 1 >= 0 /\ v_53 + v_i_5 - 3 >= 0 /\ v_up_0 + v_i_5 - 2 >= 0 /\ -v_up_0 + v_i_5 >= 0 /\ -v_r_3 + v_i_5 - 1 >= 0 /\ v_52 + v_i_5 - 1 >= 0 /\ -v_52 + v_i_5 - 1 >= 0 /\ -v_6 >= 0 /\ v_53 - v_6 - 2 >= 0 /\ v_up_0 - v_6 - 1 >= 0 /\ -v_up_0 - v_6 + 1 >= 0 /\ -v_r_3 - v_6 >= 0 /\ v_52 - v_6 >= 0 /\ -v_52 - v_6 >= 0 /\ v_53 - 2 >= 0 /\ v_up_0 + v_53 - 3 >= 0 /\ -v_up_0 + v_53 - 1 >= 0 /\ -v_r_3 + v_53 - 2 >= 0 /\ v_52 + v_53 - 2 >= 0 /\ -v_52 + v_53 - 2 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_52 - v_up_0 + 1 >= 0 /\ -v_52 - v_up_0 + 1 >= 0 /\ v_up_0 - 1 >= 0 /\ -v_r_3 + v_up_0 - 1 >= 0 /\ v_52 + v_up_0 - 1 >= 0 /\ -v_52 + v_up_0 - 1 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 /\ v_52 - v_r_3 >= 0 /\ -v_52 - v_r_3 >= 0 /\ -v_52 >= 0 /\ v_52 >= 0 ] eval_sipmamergesort_init_bb16_in(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0) -> Com_1(eval_sipmamergesort_init_stop(v_52, v_53, v_6, v_i_5, v_m_0, v_n, v_p_0, v_q_1, v_q_3, v_r_1, v_r_3, v_up_0)) [ -v_q_3 >= 0 /\ v_q_1 - v_q_3 >= 0 /\ v_p_0 - v_q_3 - 1 >= 0 /\ v_m_0 - v_q_3 >= 0 /\ -v_6 - v_q_3 >= 0 /\ v_53 - v_q_3 - 2 >= 0 /\ v_up_0 - v_q_3 >= 0 /\ -v_up_0 - v_q_3 + 1 >= 0 /\ -v_r_3 - v_q_3 >= 0 /\ v_52 - v_q_3 >= 0 /\ -v_52 - v_q_3 + 1 >= 0 /\ v_p_0 - v_q_1 >= 0 /\ v_m_0 - v_q_1 >= 0 /\ v_53 - v_q_1 - 1 >= 0 /\ v_53 - v_p_0 - 1 >= 0 /\ v_p_0 - 1 >= 0 /\ -v_6 + v_p_0 - 1 >= 0 /\ v_53 + v_p_0 - 3 >= 0 /\ v_up_0 + v_p_0 - 2 >= 0 /\ -v_up_0 + v_p_0 >= 0 /\ -v_r_3 + v_p_0 - 1 >= 0 /\ v_52 + v_p_0 - 1 >= 0 /\ -v_52 + v_p_0 - 1 >= 0 /\ v_53 - v_n >= 0 /\ -v_6 >= 0 /\ v_53 - v_6 - 2 >= 0 /\ v_up_0 - v_6 >= 0 /\ -v_up_0 - v_6 + 1 >= 0 /\ -v_r_3 - v_6 >= 0 /\ v_52 - v_6 >= 0 /\ -v_52 - v_6 + 1 >= 0 /\ v_53 - 2 >= 0 /\ v_up_0 + v_53 - 3 >= 0 /\ -v_up_0 + v_53 - 1 >= 0 /\ -v_r_3 + v_53 - 2 >= 0 /\ v_52 + v_53 - 2 >= 0 /\ -v_52 + v_53 - 2 >= 0 /\ -v_up_0 + 1 >= 0 /\ -v_r_3 - v_up_0 + 1 >= 0 /\ v_52 - v_up_0 + 1 >= 0 /\ -v_52 - v_up_0 + 1 >= 0 /\ v_up_0 >= 0 /\ -v_r_3 + v_up_0 >= 0 /\ v_52 + v_up_0 - 1 >= 0 /\ -v_52 + v_up_0 + 1 >= 0 /\ -v_r_3 >= 0 /\ v_r_1 - v_r_3 >= 0 /\ v_52 - v_r_3 >= 0 /\ -v_52 - v_r_3 + 1 >= 0 /\ -v_52 + 1 >= 0 /\ v_52 >= 0 ] )