NO * Step 1: TrivialSCCs NO + Considered Problem: Rules: 0. 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) -> 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) True (1,1) 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_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) True (?,1) 2. 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_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) True (?,1) 3. 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_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) True (?,1) 4. 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_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) True (?,1) 5. 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_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) True (?,1) 6. 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_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) True (?,1) 7. 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_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) True (?,1) 8. 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_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) True (?,1) 9. 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_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) True (?,1) 10. 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_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) True (?,1) 11. 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_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) True (?,1) 12. 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_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) True (?,1) 13. 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_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) True (?,1) 14. 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_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) True (?,1) 15. 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_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) True (?,1) 16. 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_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) True (?,1) 17. 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_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) True (?,1) 18. 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_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) True (?,1) 19. 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_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) True (?,1) 20. 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_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) True (?,1) 21. 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_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) True (?,1) 22. 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_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) True (?,1) 23. 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_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) True (?,1) 24. 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_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) True (?,1) 25. 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_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) True (?,1) 26. 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_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) True (?,1) 27. 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_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) True (?,1) 28. 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_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) True (?,1) 29. 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) -> 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) [-1 + v_p_0 >= 0 (?,1) && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_up_0 >= 0] 30. 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) -> 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) [-1 + v_p_0 >= 0 (?,1) && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && v_up_0 = 0] 31. 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) -> 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[-1 + v_p_0 >= 0 (?,1) ,v_up_0) && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && v_m_0 >= v_p_0 && v_m_0 + -1*v_p_0 >= v_p_0] 32. 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) -> 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 + -1*v_p_0,v_r_3 [-1 + v_p_0 >= 0 (?,1) ,v_up_0) && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && v_m_0 >= v_p_0 && -1 + v_p_0 >= v_m_0 + -1*v_p_0] 33. 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) -> 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) [-1 + v_p_0 >= 0 (?,1) && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_p_0 >= v_m_0 && -1 + v_p_0 >= 0] 34. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_q_1 >= 0 && -1 + v_r_1 >= 0] 35. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && 0 >= v_q_1] 36. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && 0 >= v_r_1] 37. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_q_1 >= 0 && -2 + v_p_0 + v_q_1 >= 0 && -2 + v_m_0 + v_q_1 >= 0 && -1 + v_q_1 + v_up_0 >= 0 && v_q_1 + -1*v_up_0 >= 0 && -2 + v_q_1 + v_r_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_m_0 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -2 + v_p_0 + v_r_1 >= 0 && -1 + v_m_0 >= 0 && -1 + v_m_0 + v_up_0 >= 0 && v_m_0 + -1*v_up_0 >= 0 && -2 + v_m_0 + v_r_1 >= 0 && 1 + -1*v_up_0 >= 0 && v_r_1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_r_1 + v_up_0 >= 0 && -1 + v_r_1 >= 0 && -1 + nondef_1 >= nondef_0] 38. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_q_1 >= 0 && -2 + v_p_0 + v_q_1 >= 0 && -2 + v_m_0 + v_q_1 >= 0 && -1 + v_q_1 + v_up_0 >= 0 && v_q_1 + -1*v_up_0 >= 0 && -2 + v_q_1 + v_r_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_m_0 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -2 + v_p_0 + v_r_1 >= 0 && -1 + v_m_0 >= 0 && -1 + v_m_0 + v_up_0 >= 0 && v_m_0 + -1*v_up_0 >= 0 && -2 + v_m_0 + v_r_1 >= 0 && 1 + -1*v_up_0 >= 0 && v_r_1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_r_1 + v_up_0 >= 0 && -1 + v_r_1 >= 0 && nondef_0 >= nondef_1] 39. 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) -> eval_sipmamergesort_init_bb3_in(v_52,v_53,v_6,v_i_5,v_m_0,v_n,v_p_0,-1 + v_q_1,v_q_3,v_r_1,v_r_3 [v_p_0 + -1*v_q_1 >= 0 (?,1) ,v_up_0) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_q_1 >= 0 && -2 + v_p_0 + v_q_1 >= 0 && -2 + v_m_0 + v_q_1 >= 0 && -1 + v_q_1 + v_up_0 >= 0 && v_q_1 + -1*v_up_0 >= 0 && -2 + v_q_1 + v_r_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_m_0 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -2 + v_p_0 + v_r_1 >= 0 && -1 + v_m_0 >= 0 && -1 + v_m_0 + v_up_0 >= 0 && v_m_0 + -1*v_up_0 >= 0 && -2 + v_m_0 + v_r_1 >= 0 && 1 + -1*v_up_0 >= 0 && v_r_1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_r_1 + v_up_0 >= 0 && -1 + v_r_1 >= 0] 40. 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) -> 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,-1 + v_r_1,v_r_3 [v_p_0 + -1*v_q_1 >= 0 (?,1) ,v_up_0) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_q_1 >= 0 && -2 + v_p_0 + v_q_1 >= 0 && -2 + v_m_0 + v_q_1 >= 0 && -1 + v_q_1 + v_up_0 >= 0 && v_q_1 + -1*v_up_0 >= 0 && -2 + v_q_1 + v_r_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_m_0 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -2 + v_p_0 + v_r_1 >= 0 && -1 + v_m_0 >= 0 && -1 + v_m_0 + v_up_0 >= 0 && v_m_0 + -1*v_up_0 >= 0 && -2 + v_m_0 + v_r_1 >= 0 && 1 + -1*v_up_0 >= 0 && v_r_1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_r_1 + v_up_0 >= 0 && -1 + v_r_1 >= 0] 41. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && v_r_1 + -1*v_r_3 >= 0 && -1 + v_r_3 >= 0] 42. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && v_r_1 + -1*v_r_3 >= 0 && 0 >= v_r_3] 43. 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) -> 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,-1 + v_r_3 [v_p_0 + -1*v_q_1 >= 0 (?,1) ,v_up_0) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -2 + v_p_0 + v_r_3 >= 0 && -2 + v_p_0 + v_r_1 >= 0 && 1 + -1*v_up_0 >= 0 && v_r_3 + -1*v_up_0 >= 0 && v_r_1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_r_3 + v_up_0 >= 0 && -1 + v_r_1 + v_up_0 >= 0 && v_r_1 + -1*v_r_3 >= 0 && -1 + v_r_3 >= 0 && -2 + v_r_1 + v_r_3 >= 0 && -1 + v_r_1 >= 0] 44. 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) -> 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 + -1*v_q_3 >= 0 (?,1) && v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && -1 + v_q_3 >= 0] 45. 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) -> 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 + -1*v_q_3 >= 0 (?,1) && v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && 0 >= v_q_3] 46. 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) -> 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,-1 + v_q_3,v_r_1,v_r_3 [v_q_1 + -1*v_q_3 >= 0 (?,1) ,v_up_0) && v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1 + v_q_3 >= 0 && -2 + v_q_1 + v_q_3 >= 0 && -2 + v_p_0 + v_q_3 >= 0 && -2 + v_m_0 + v_q_3 >= 0 && -1 + v_q_3 + v_up_0 >= 0 && v_q_3 + -1*v_up_0 >= 0 && -1 + v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_q_1 >= 0 && -2 + v_p_0 + v_q_1 >= 0 && -2 + v_m_0 + v_q_1 >= 0 && -1 + v_q_1 + v_up_0 >= 0 && v_q_1 + -1*v_up_0 >= 0 && -1 + v_q_1 + -1*v_r_3 >= 0 && -1 + v_p_0 >= 0 && -2 + v_m_0 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_m_0 >= 0 && -1 + v_m_0 + v_up_0 >= 0 && v_m_0 + -1*v_up_0 >= 0 && -1 + v_m_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 47. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 48. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 49. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 50. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 51. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 52. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && -1 + v_6 >= 0] 53. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && 0 >= v_6] 54. 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) -> eval_sipmamergesort_init_83(1 + -1*v_up_0,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_q_3 >= 0 (?,1) ,v_up_0) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 55. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0] 56. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0] 57. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0] 58. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0 && -1 + v_n >= v_53] 59. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0 && v_53 >= v_n] 60. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && v_53 + -1*v_n >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0 && v_52 = 0] 61. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && v_53 + -1*v_n >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0 && -1 + v_52 >= 0] 62. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1 + v_i_5 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1 + -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -2 + v_i_5 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && v_53 + -1*v_n >= 0 && -1 + v_i_5 >= 0 && -1 + -1*v_6 + v_i_5 >= 0 && -3 + v_53 + v_i_5 >= 0 && -2 + v_i_5 + v_up_0 >= 0 && v_i_5 + -1*v_up_0 >= 0 && -1 + v_i_5 + -1*v_r_3 >= 0 && -1 + v_52 + v_i_5 >= 0 && -1 + -1*v_52 + v_i_5 >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1 + -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && -1 + v_up_0 >= 0 && -1 + -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && -1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && -1*v_52 + -1*v_r_3 >= 0 && -1*v_52 >= 0 && v_52 >= 0 && v_n >= v_i_5] 63. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1 + v_i_5 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1 + -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -2 + v_i_5 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && v_53 + -1*v_n >= 0 && -1 + v_i_5 >= 0 && -1 + -1*v_6 + v_i_5 >= 0 && -3 + v_53 + v_i_5 >= 0 && -2 + v_i_5 + v_up_0 >= 0 && v_i_5 + -1*v_up_0 >= 0 && -1 + v_i_5 + -1*v_r_3 >= 0 && -1 + v_52 + v_i_5 >= 0 && -1 + -1*v_52 + v_i_5 >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1 + -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && -1 + v_up_0 >= 0 && -1 + -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && -1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && -1*v_52 + -1*v_r_3 >= 0 && -1*v_52 >= 0 && v_52 >= 0 && -1 + v_i_5 >= v_n] 64. 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) -> eval_sipmamergesort_init_bb14_in(v_52,v_53,v_6,1 + 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_q_3 >= 0 (?,1) ,v_up_0) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && -1 + v_n + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1 + v_i_5 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1 + -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -2 + v_n + v_p_0 >= 0 && -2 + v_i_5 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && v_53 + -1*v_n >= 0 && -1 + v_n >= 0 && -2 + v_i_5 + v_n >= 0 && -1*v_i_5 + v_n >= 0 && -1 + -1*v_6 + v_n >= 0 && -3 + v_53 + v_n >= 0 && -2 + v_n + v_up_0 >= 0 && v_n + -1*v_up_0 >= 0 && -1 + v_n + -1*v_r_3 >= 0 && -1 + v_52 + v_n >= 0 && -1 + -1*v_52 + v_n >= 0 && v_53 + -1*v_i_5 >= 0 && -1 + v_i_5 >= 0 && -1 + -1*v_6 + v_i_5 >= 0 && -3 + v_53 + v_i_5 >= 0 && -2 + v_i_5 + v_up_0 >= 0 && v_i_5 + -1*v_up_0 >= 0 && -1 + v_i_5 + -1*v_r_3 >= 0 && -1 + v_52 + v_i_5 >= 0 && -1 + -1*v_52 + v_i_5 >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1 + -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && -1 + v_up_0 >= 0 && -1 + -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && -1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && -1*v_52 + -1*v_r_3 >= 0 && -1*v_52 >= 0 && v_52 >= 0] 65. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && v_53 + -1*v_n >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0] Signature: {(eval_sipmamergesort_init_0,12) ;(eval_sipmamergesort_init_1,12) ;(eval_sipmamergesort_init_10,12) ;(eval_sipmamergesort_init_11,12) ;(eval_sipmamergesort_init_12,12) ;(eval_sipmamergesort_init_13,12) ;(eval_sipmamergesort_init_14,12) ;(eval_sipmamergesort_init_15,12) ;(eval_sipmamergesort_init_16,12) ;(eval_sipmamergesort_init_17,12) ;(eval_sipmamergesort_init_18,12) ;(eval_sipmamergesort_init_19,12) ;(eval_sipmamergesort_init_2,12) ;(eval_sipmamergesort_init_20,12) ;(eval_sipmamergesort_init_21,12) ;(eval_sipmamergesort_init_22,12) ;(eval_sipmamergesort_init_23,12) ;(eval_sipmamergesort_init_24,12) ;(eval_sipmamergesort_init_25,12) ;(eval_sipmamergesort_init_26,12) ;(eval_sipmamergesort_init_3,12) ;(eval_sipmamergesort_init_4,12) ;(eval_sipmamergesort_init_5,12) ;(eval_sipmamergesort_init_6,12) ;(eval_sipmamergesort_init_7,12) ;(eval_sipmamergesort_init_77,12) ;(eval_sipmamergesort_init_78,12) ;(eval_sipmamergesort_init_79,12) ;(eval_sipmamergesort_init_8,12) ;(eval_sipmamergesort_init_80,12) ;(eval_sipmamergesort_init_81,12) ;(eval_sipmamergesort_init_83,12) ;(eval_sipmamergesort_init_84,12) ;(eval_sipmamergesort_init_85,12) ;(eval_sipmamergesort_init_86,12) ;(eval_sipmamergesort_init_9,12) ;(eval_sipmamergesort_init_bb0_in,12) ;(eval_sipmamergesort_init_bb10_in,12) ;(eval_sipmamergesort_init_bb11_in,12) ;(eval_sipmamergesort_init_bb12_in,12) ;(eval_sipmamergesort_init_bb13_in,12) ;(eval_sipmamergesort_init_bb14_in,12) ;(eval_sipmamergesort_init_bb15_in,12) ;(eval_sipmamergesort_init_bb16_in,12) ;(eval_sipmamergesort_init_bb1_in,12) ;(eval_sipmamergesort_init_bb2_in,12) ;(eval_sipmamergesort_init_bb3_in,12) ;(eval_sipmamergesort_init_bb4_in,12) ;(eval_sipmamergesort_init_bb5_in,12) ;(eval_sipmamergesort_init_bb6_in,12) ;(eval_sipmamergesort_init_bb7_in,12) ;(eval_sipmamergesort_init_bb8_in,12) ;(eval_sipmamergesort_init_bb9_in,12) ;(eval_sipmamergesort_init_start,12) ;(eval_sipmamergesort_init_stop,12)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8},8->{9},9->{10},10->{11},11->{12},12->{13} ,13->{14},14->{15},15->{16},16->{17},17->{18},18->{19},19->{20},20->{21},21->{22},22->{23},23->{24},24->{25} ,25->{26},26->{27},27->{28},28->{29,30},29->{31,32,33},30->{31,32,33},31->{34,35,36},32->{34,35,36},33->{34 ,35,36},34->{37,38},35->{41,42},36->{41,42},37->{39},38->{40},39->{34,35,36},40->{34,35,36},41->{43},42->{44 ,45},43->{41,42},44->{46},45->{47},46->{44,45},47->{48},48->{49},49->{50},50->{51},51->{52,53},52->{31,32 ,33},53->{54},54->{55},55->{56},56->{57},57->{58,59},58->{29,30},59->{60,61},60->{62,63},61->{65},62->{64} ,63->{65},64->{62,63},65->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths NO + Considered Problem: Rules: 0. 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) -> 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) True (1,1) 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_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) True (1,1) 2. 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_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) True (1,1) 3. 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_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) True (1,1) 4. 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_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) True (1,1) 5. 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_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) True (1,1) 6. 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_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) True (1,1) 7. 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_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) True (1,1) 8. 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_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) True (1,1) 9. 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_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) True (1,1) 10. 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_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) True (1,1) 11. 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_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) True (1,1) 12. 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_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) True (1,1) 13. 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_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) True (1,1) 14. 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_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) True (1,1) 15. 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_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) True (1,1) 16. 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_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) True (1,1) 17. 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_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) True (1,1) 18. 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_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) True (1,1) 19. 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_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) True (1,1) 20. 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_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) True (1,1) 21. 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_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) True (1,1) 22. 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_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) True (1,1) 23. 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_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) True (1,1) 24. 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_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) True (1,1) 25. 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_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) True (1,1) 26. 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_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) True (1,1) 27. 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_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) True (1,1) 28. 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_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) True (1,1) 29. 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) -> 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) [-1 + v_p_0 >= 0 (?,1) && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_up_0 >= 0] 30. 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) -> 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) [-1 + v_p_0 >= 0 (?,1) && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && v_up_0 = 0] 31. 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) -> 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[-1 + v_p_0 >= 0 (?,1) ,v_up_0) && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && v_m_0 >= v_p_0 && v_m_0 + -1*v_p_0 >= v_p_0] 32. 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) -> 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 + -1*v_p_0,v_r_3 [-1 + v_p_0 >= 0 (?,1) ,v_up_0) && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && v_m_0 >= v_p_0 && -1 + v_p_0 >= v_m_0 + -1*v_p_0] 33. 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) -> 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) [-1 + v_p_0 >= 0 (?,1) && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_p_0 >= v_m_0 && -1 + v_p_0 >= 0] 34. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_q_1 >= 0 && -1 + v_r_1 >= 0] 35. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && 0 >= v_q_1] 36. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && 0 >= v_r_1] 37. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_q_1 >= 0 && -2 + v_p_0 + v_q_1 >= 0 && -2 + v_m_0 + v_q_1 >= 0 && -1 + v_q_1 + v_up_0 >= 0 && v_q_1 + -1*v_up_0 >= 0 && -2 + v_q_1 + v_r_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_m_0 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -2 + v_p_0 + v_r_1 >= 0 && -1 + v_m_0 >= 0 && -1 + v_m_0 + v_up_0 >= 0 && v_m_0 + -1*v_up_0 >= 0 && -2 + v_m_0 + v_r_1 >= 0 && 1 + -1*v_up_0 >= 0 && v_r_1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_r_1 + v_up_0 >= 0 && -1 + v_r_1 >= 0 && -1 + nondef_1 >= nondef_0] 38. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_q_1 >= 0 && -2 + v_p_0 + v_q_1 >= 0 && -2 + v_m_0 + v_q_1 >= 0 && -1 + v_q_1 + v_up_0 >= 0 && v_q_1 + -1*v_up_0 >= 0 && -2 + v_q_1 + v_r_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_m_0 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -2 + v_p_0 + v_r_1 >= 0 && -1 + v_m_0 >= 0 && -1 + v_m_0 + v_up_0 >= 0 && v_m_0 + -1*v_up_0 >= 0 && -2 + v_m_0 + v_r_1 >= 0 && 1 + -1*v_up_0 >= 0 && v_r_1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_r_1 + v_up_0 >= 0 && -1 + v_r_1 >= 0 && nondef_0 >= nondef_1] 39. 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) -> eval_sipmamergesort_init_bb3_in(v_52,v_53,v_6,v_i_5,v_m_0,v_n,v_p_0,-1 + v_q_1,v_q_3,v_r_1,v_r_3 [v_p_0 + -1*v_q_1 >= 0 (?,1) ,v_up_0) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_q_1 >= 0 && -2 + v_p_0 + v_q_1 >= 0 && -2 + v_m_0 + v_q_1 >= 0 && -1 + v_q_1 + v_up_0 >= 0 && v_q_1 + -1*v_up_0 >= 0 && -2 + v_q_1 + v_r_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_m_0 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -2 + v_p_0 + v_r_1 >= 0 && -1 + v_m_0 >= 0 && -1 + v_m_0 + v_up_0 >= 0 && v_m_0 + -1*v_up_0 >= 0 && -2 + v_m_0 + v_r_1 >= 0 && 1 + -1*v_up_0 >= 0 && v_r_1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_r_1 + v_up_0 >= 0 && -1 + v_r_1 >= 0] 40. 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) -> 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,-1 + v_r_1,v_r_3 [v_p_0 + -1*v_q_1 >= 0 (?,1) ,v_up_0) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_q_1 >= 0 && -2 + v_p_0 + v_q_1 >= 0 && -2 + v_m_0 + v_q_1 >= 0 && -1 + v_q_1 + v_up_0 >= 0 && v_q_1 + -1*v_up_0 >= 0 && -2 + v_q_1 + v_r_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_m_0 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -2 + v_p_0 + v_r_1 >= 0 && -1 + v_m_0 >= 0 && -1 + v_m_0 + v_up_0 >= 0 && v_m_0 + -1*v_up_0 >= 0 && -2 + v_m_0 + v_r_1 >= 0 && 1 + -1*v_up_0 >= 0 && v_r_1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_r_1 + v_up_0 >= 0 && -1 + v_r_1 >= 0] 41. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && v_r_1 + -1*v_r_3 >= 0 && -1 + v_r_3 >= 0] 42. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && v_r_1 + -1*v_r_3 >= 0 && 0 >= v_r_3] 43. 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) -> 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,-1 + v_r_3 [v_p_0 + -1*v_q_1 >= 0 (?,1) ,v_up_0) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -2 + v_p_0 + v_r_3 >= 0 && -2 + v_p_0 + v_r_1 >= 0 && 1 + -1*v_up_0 >= 0 && v_r_3 + -1*v_up_0 >= 0 && v_r_1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_r_3 + v_up_0 >= 0 && -1 + v_r_1 + v_up_0 >= 0 && v_r_1 + -1*v_r_3 >= 0 && -1 + v_r_3 >= 0 && -2 + v_r_1 + v_r_3 >= 0 && -1 + v_r_1 >= 0] 44. 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) -> 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 + -1*v_q_3 >= 0 (?,1) && v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && -1 + v_q_3 >= 0] 45. 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) -> 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 + -1*v_q_3 >= 0 (?,1) && v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && 0 >= v_q_3] 46. 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) -> 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,-1 + v_q_3,v_r_1,v_r_3 [v_q_1 + -1*v_q_3 >= 0 (?,1) ,v_up_0) && v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1 + v_q_3 >= 0 && -2 + v_q_1 + v_q_3 >= 0 && -2 + v_p_0 + v_q_3 >= 0 && -2 + v_m_0 + v_q_3 >= 0 && -1 + v_q_3 + v_up_0 >= 0 && v_q_3 + -1*v_up_0 >= 0 && -1 + v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_q_1 >= 0 && -2 + v_p_0 + v_q_1 >= 0 && -2 + v_m_0 + v_q_1 >= 0 && -1 + v_q_1 + v_up_0 >= 0 && v_q_1 + -1*v_up_0 >= 0 && -1 + v_q_1 + -1*v_r_3 >= 0 && -1 + v_p_0 >= 0 && -2 + v_m_0 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_m_0 >= 0 && -1 + v_m_0 + v_up_0 >= 0 && v_m_0 + -1*v_up_0 >= 0 && -1 + v_m_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 47. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 48. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 49. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 50. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 51. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 52. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && -1 + v_6 >= 0] 53. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && 0 >= v_6] 54. 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) -> eval_sipmamergesort_init_83(1 + -1*v_up_0,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_q_3 >= 0 (?,1) ,v_up_0) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 55. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0] 56. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0] 57. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0] 58. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0 && -1 + v_n >= v_53] 59. 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) -> 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) [-1*v_q_3 >= 0 (1,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0 && v_53 >= v_n] 60. 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) -> 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) [-1*v_q_3 >= 0 (1,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && v_53 + -1*v_n >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0 && v_52 = 0] 61. 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) -> 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) [-1*v_q_3 >= 0 (1,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && v_53 + -1*v_n >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0 && -1 + v_52 >= 0] 62. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1 + v_i_5 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1 + -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -2 + v_i_5 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && v_53 + -1*v_n >= 0 && -1 + v_i_5 >= 0 && -1 + -1*v_6 + v_i_5 >= 0 && -3 + v_53 + v_i_5 >= 0 && -2 + v_i_5 + v_up_0 >= 0 && v_i_5 + -1*v_up_0 >= 0 && -1 + v_i_5 + -1*v_r_3 >= 0 && -1 + v_52 + v_i_5 >= 0 && -1 + -1*v_52 + v_i_5 >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1 + -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && -1 + v_up_0 >= 0 && -1 + -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && -1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && -1*v_52 + -1*v_r_3 >= 0 && -1*v_52 >= 0 && v_52 >= 0 && v_n >= v_i_5] 63. 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) -> 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) [-1*v_q_3 >= 0 (1,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1 + v_i_5 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1 + -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -2 + v_i_5 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && v_53 + -1*v_n >= 0 && -1 + v_i_5 >= 0 && -1 + -1*v_6 + v_i_5 >= 0 && -3 + v_53 + v_i_5 >= 0 && -2 + v_i_5 + v_up_0 >= 0 && v_i_5 + -1*v_up_0 >= 0 && -1 + v_i_5 + -1*v_r_3 >= 0 && -1 + v_52 + v_i_5 >= 0 && -1 + -1*v_52 + v_i_5 >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1 + -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && -1 + v_up_0 >= 0 && -1 + -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && -1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && -1*v_52 + -1*v_r_3 >= 0 && -1*v_52 >= 0 && v_52 >= 0 && -1 + v_i_5 >= v_n] 64. 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) -> eval_sipmamergesort_init_bb14_in(v_52,v_53,v_6,1 + 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_q_3 >= 0 (?,1) ,v_up_0) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && -1 + v_n + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1 + v_i_5 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1 + -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -2 + v_n + v_p_0 >= 0 && -2 + v_i_5 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && v_53 + -1*v_n >= 0 && -1 + v_n >= 0 && -2 + v_i_5 + v_n >= 0 && -1*v_i_5 + v_n >= 0 && -1 + -1*v_6 + v_n >= 0 && -3 + v_53 + v_n >= 0 && -2 + v_n + v_up_0 >= 0 && v_n + -1*v_up_0 >= 0 && -1 + v_n + -1*v_r_3 >= 0 && -1 + v_52 + v_n >= 0 && -1 + -1*v_52 + v_n >= 0 && v_53 + -1*v_i_5 >= 0 && -1 + v_i_5 >= 0 && -1 + -1*v_6 + v_i_5 >= 0 && -3 + v_53 + v_i_5 >= 0 && -2 + v_i_5 + v_up_0 >= 0 && v_i_5 + -1*v_up_0 >= 0 && -1 + v_i_5 + -1*v_r_3 >= 0 && -1 + v_52 + v_i_5 >= 0 && -1 + -1*v_52 + v_i_5 >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1 + -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && -1 + v_up_0 >= 0 && -1 + -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && -1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && -1*v_52 + -1*v_r_3 >= 0 && -1*v_52 >= 0 && v_52 >= 0] 65. 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) -> 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) [-1*v_q_3 >= 0 (1,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && v_53 + -1*v_n >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0] Signature: {(eval_sipmamergesort_init_0,12) ;(eval_sipmamergesort_init_1,12) ;(eval_sipmamergesort_init_10,12) ;(eval_sipmamergesort_init_11,12) ;(eval_sipmamergesort_init_12,12) ;(eval_sipmamergesort_init_13,12) ;(eval_sipmamergesort_init_14,12) ;(eval_sipmamergesort_init_15,12) ;(eval_sipmamergesort_init_16,12) ;(eval_sipmamergesort_init_17,12) ;(eval_sipmamergesort_init_18,12) ;(eval_sipmamergesort_init_19,12) ;(eval_sipmamergesort_init_2,12) ;(eval_sipmamergesort_init_20,12) ;(eval_sipmamergesort_init_21,12) ;(eval_sipmamergesort_init_22,12) ;(eval_sipmamergesort_init_23,12) ;(eval_sipmamergesort_init_24,12) ;(eval_sipmamergesort_init_25,12) ;(eval_sipmamergesort_init_26,12) ;(eval_sipmamergesort_init_3,12) ;(eval_sipmamergesort_init_4,12) ;(eval_sipmamergesort_init_5,12) ;(eval_sipmamergesort_init_6,12) ;(eval_sipmamergesort_init_7,12) ;(eval_sipmamergesort_init_77,12) ;(eval_sipmamergesort_init_78,12) ;(eval_sipmamergesort_init_79,12) ;(eval_sipmamergesort_init_8,12) ;(eval_sipmamergesort_init_80,12) ;(eval_sipmamergesort_init_81,12) ;(eval_sipmamergesort_init_83,12) ;(eval_sipmamergesort_init_84,12) ;(eval_sipmamergesort_init_85,12) ;(eval_sipmamergesort_init_86,12) ;(eval_sipmamergesort_init_9,12) ;(eval_sipmamergesort_init_bb0_in,12) ;(eval_sipmamergesort_init_bb10_in,12) ;(eval_sipmamergesort_init_bb11_in,12) ;(eval_sipmamergesort_init_bb12_in,12) ;(eval_sipmamergesort_init_bb13_in,12) ;(eval_sipmamergesort_init_bb14_in,12) ;(eval_sipmamergesort_init_bb15_in,12) ;(eval_sipmamergesort_init_bb16_in,12) ;(eval_sipmamergesort_init_bb1_in,12) ;(eval_sipmamergesort_init_bb2_in,12) ;(eval_sipmamergesort_init_bb3_in,12) ;(eval_sipmamergesort_init_bb4_in,12) ;(eval_sipmamergesort_init_bb5_in,12) ;(eval_sipmamergesort_init_bb6_in,12) ;(eval_sipmamergesort_init_bb7_in,12) ;(eval_sipmamergesort_init_bb8_in,12) ;(eval_sipmamergesort_init_bb9_in,12) ;(eval_sipmamergesort_init_start,12) ;(eval_sipmamergesort_init_stop,12)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8},8->{9},9->{10},10->{11},11->{12},12->{13} ,13->{14},14->{15},15->{16},16->{17},17->{18},18->{19},19->{20},20->{21},21->{22},22->{23},23->{24},24->{25} ,25->{26},26->{27},27->{28},28->{29,30},29->{31,32,33},30->{31,32,33},31->{34,35,36},32->{34,35,36},33->{34 ,35,36},34->{37,38},35->{41,42},36->{41,42},37->{39},38->{40},39->{34,35,36},40->{34,35,36},41->{43},42->{44 ,45},43->{41,42},44->{46},45->{47},46->{44,45},47->{48},48->{49},49->{50},50->{51},51->{52,53},52->{31,32 ,33},53->{54},54->{55},55->{56},56->{57},57->{58,59},58->{29,30},59->{60,61},60->{62,63},61->{65},62->{64} ,63->{65},64->{62,63},65->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(28,30) ,(31,35) ,(31,36) ,(32,35) ,(33,34) ,(36,41) ,(39,36) ,(40,35)] * Step 3: Looptree NO + Considered Problem: Rules: 0. 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) -> 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) True (1,1) 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_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) True (1,1) 2. 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_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) True (1,1) 3. 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_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) True (1,1) 4. 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_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) True (1,1) 5. 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_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) True (1,1) 6. 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_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) True (1,1) 7. 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_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) True (1,1) 8. 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_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) True (1,1) 9. 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_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) True (1,1) 10. 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_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) True (1,1) 11. 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_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) True (1,1) 12. 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_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) True (1,1) 13. 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_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) True (1,1) 14. 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_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) True (1,1) 15. 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_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) True (1,1) 16. 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_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) True (1,1) 17. 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_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) True (1,1) 18. 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_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) True (1,1) 19. 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_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) True (1,1) 20. 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_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) True (1,1) 21. 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_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) True (1,1) 22. 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_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) True (1,1) 23. 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_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) True (1,1) 24. 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_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) True (1,1) 25. 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_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) True (1,1) 26. 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_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) True (1,1) 27. 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_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) True (1,1) 28. 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_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) True (1,1) 29. 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) -> 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) [-1 + v_p_0 >= 0 (?,1) && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_up_0 >= 0] 30. 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) -> 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) [-1 + v_p_0 >= 0 (?,1) && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && v_up_0 = 0] 31. 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) -> 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[-1 + v_p_0 >= 0 (?,1) ,v_up_0) && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && v_m_0 >= v_p_0 && v_m_0 + -1*v_p_0 >= v_p_0] 32. 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) -> 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 + -1*v_p_0,v_r_3 [-1 + v_p_0 >= 0 (?,1) ,v_up_0) && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && v_m_0 >= v_p_0 && -1 + v_p_0 >= v_m_0 + -1*v_p_0] 33. 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) -> 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) [-1 + v_p_0 >= 0 (?,1) && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_p_0 >= v_m_0 && -1 + v_p_0 >= 0] 34. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_q_1 >= 0 && -1 + v_r_1 >= 0] 35. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && 0 >= v_q_1] 36. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && 0 >= v_r_1] 37. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_q_1 >= 0 && -2 + v_p_0 + v_q_1 >= 0 && -2 + v_m_0 + v_q_1 >= 0 && -1 + v_q_1 + v_up_0 >= 0 && v_q_1 + -1*v_up_0 >= 0 && -2 + v_q_1 + v_r_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_m_0 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -2 + v_p_0 + v_r_1 >= 0 && -1 + v_m_0 >= 0 && -1 + v_m_0 + v_up_0 >= 0 && v_m_0 + -1*v_up_0 >= 0 && -2 + v_m_0 + v_r_1 >= 0 && 1 + -1*v_up_0 >= 0 && v_r_1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_r_1 + v_up_0 >= 0 && -1 + v_r_1 >= 0 && -1 + nondef_1 >= nondef_0] 38. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_q_1 >= 0 && -2 + v_p_0 + v_q_1 >= 0 && -2 + v_m_0 + v_q_1 >= 0 && -1 + v_q_1 + v_up_0 >= 0 && v_q_1 + -1*v_up_0 >= 0 && -2 + v_q_1 + v_r_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_m_0 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -2 + v_p_0 + v_r_1 >= 0 && -1 + v_m_0 >= 0 && -1 + v_m_0 + v_up_0 >= 0 && v_m_0 + -1*v_up_0 >= 0 && -2 + v_m_0 + v_r_1 >= 0 && 1 + -1*v_up_0 >= 0 && v_r_1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_r_1 + v_up_0 >= 0 && -1 + v_r_1 >= 0 && nondef_0 >= nondef_1] 39. 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) -> eval_sipmamergesort_init_bb3_in(v_52,v_53,v_6,v_i_5,v_m_0,v_n,v_p_0,-1 + v_q_1,v_q_3,v_r_1,v_r_3 [v_p_0 + -1*v_q_1 >= 0 (?,1) ,v_up_0) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_q_1 >= 0 && -2 + v_p_0 + v_q_1 >= 0 && -2 + v_m_0 + v_q_1 >= 0 && -1 + v_q_1 + v_up_0 >= 0 && v_q_1 + -1*v_up_0 >= 0 && -2 + v_q_1 + v_r_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_m_0 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -2 + v_p_0 + v_r_1 >= 0 && -1 + v_m_0 >= 0 && -1 + v_m_0 + v_up_0 >= 0 && v_m_0 + -1*v_up_0 >= 0 && -2 + v_m_0 + v_r_1 >= 0 && 1 + -1*v_up_0 >= 0 && v_r_1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_r_1 + v_up_0 >= 0 && -1 + v_r_1 >= 0] 40. 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) -> 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,-1 + v_r_1,v_r_3 [v_p_0 + -1*v_q_1 >= 0 (?,1) ,v_up_0) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_q_1 >= 0 && -2 + v_p_0 + v_q_1 >= 0 && -2 + v_m_0 + v_q_1 >= 0 && -1 + v_q_1 + v_up_0 >= 0 && v_q_1 + -1*v_up_0 >= 0 && -2 + v_q_1 + v_r_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_m_0 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -2 + v_p_0 + v_r_1 >= 0 && -1 + v_m_0 >= 0 && -1 + v_m_0 + v_up_0 >= 0 && v_m_0 + -1*v_up_0 >= 0 && -2 + v_m_0 + v_r_1 >= 0 && 1 + -1*v_up_0 >= 0 && v_r_1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_r_1 + v_up_0 >= 0 && -1 + v_r_1 >= 0] 41. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && v_r_1 + -1*v_r_3 >= 0 && -1 + v_r_3 >= 0] 42. 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) -> 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 + -1*v_q_1 >= 0 (?,1) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && 1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && v_r_1 + -1*v_r_3 >= 0 && 0 >= v_r_3] 43. 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) -> 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,-1 + v_r_3 [v_p_0 + -1*v_q_1 >= 0 (?,1) ,v_up_0) && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -2 + v_p_0 + v_r_3 >= 0 && -2 + v_p_0 + v_r_1 >= 0 && 1 + -1*v_up_0 >= 0 && v_r_3 + -1*v_up_0 >= 0 && v_r_1 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1 + v_r_3 + v_up_0 >= 0 && -1 + v_r_1 + v_up_0 >= 0 && v_r_1 + -1*v_r_3 >= 0 && -1 + v_r_3 >= 0 && -2 + v_r_1 + v_r_3 >= 0 && -1 + v_r_1 >= 0] 44. 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) -> 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 + -1*v_q_3 >= 0 (?,1) && v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && -1 + v_q_3 >= 0] 45. 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) -> 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 + -1*v_q_3 >= 0 (?,1) && v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && 0 >= v_q_3] 46. 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) -> 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,-1 + v_q_3,v_r_1,v_r_3 [v_q_1 + -1*v_q_3 >= 0 (?,1) ,v_up_0) && v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1 + v_q_3 >= 0 && -2 + v_q_1 + v_q_3 >= 0 && -2 + v_p_0 + v_q_3 >= 0 && -2 + v_m_0 + v_q_3 >= 0 && -1 + v_q_3 + v_up_0 >= 0 && v_q_3 + -1*v_up_0 >= 0 && -1 + v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_q_1 >= 0 && -2 + v_p_0 + v_q_1 >= 0 && -2 + v_m_0 + v_q_1 >= 0 && -1 + v_q_1 + v_up_0 >= 0 && v_q_1 + -1*v_up_0 >= 0 && -1 + v_q_1 + -1*v_r_3 >= 0 && -1 + v_p_0 >= 0 && -2 + v_m_0 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_m_0 >= 0 && -1 + v_m_0 + v_up_0 >= 0 && v_m_0 + -1*v_up_0 >= 0 && -1 + v_m_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 47. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 48. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 49. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 50. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 51. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 52. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && -1 + v_6 >= 0] 53. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && 0 >= v_6] 54. 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) -> eval_sipmamergesort_init_83(1 + -1*v_up_0,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_q_3 >= 0 (?,1) ,v_up_0) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0] 55. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0] 56. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0] 57. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0] 58. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0 && -1 + v_n >= v_53] 59. 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) -> 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) [-1*v_q_3 >= 0 (1,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0 && v_53 >= v_n] 60. 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) -> 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) [-1*v_q_3 >= 0 (1,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && v_53 + -1*v_n >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0 && v_52 = 0] 61. 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) -> 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) [-1*v_q_3 >= 0 (1,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && v_53 + -1*v_n >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0 && -1 + v_52 >= 0] 62. 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) -> 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) [-1*v_q_3 >= 0 (?,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1 + v_i_5 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1 + -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -2 + v_i_5 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && v_53 + -1*v_n >= 0 && -1 + v_i_5 >= 0 && -1 + -1*v_6 + v_i_5 >= 0 && -3 + v_53 + v_i_5 >= 0 && -2 + v_i_5 + v_up_0 >= 0 && v_i_5 + -1*v_up_0 >= 0 && -1 + v_i_5 + -1*v_r_3 >= 0 && -1 + v_52 + v_i_5 >= 0 && -1 + -1*v_52 + v_i_5 >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1 + -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && -1 + v_up_0 >= 0 && -1 + -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && -1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && -1*v_52 + -1*v_r_3 >= 0 && -1*v_52 >= 0 && v_52 >= 0 && v_n >= v_i_5] 63. 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) -> 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) [-1*v_q_3 >= 0 (1,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1 + v_i_5 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1 + -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -2 + v_i_5 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && v_53 + -1*v_n >= 0 && -1 + v_i_5 >= 0 && -1 + -1*v_6 + v_i_5 >= 0 && -3 + v_53 + v_i_5 >= 0 && -2 + v_i_5 + v_up_0 >= 0 && v_i_5 + -1*v_up_0 >= 0 && -1 + v_i_5 + -1*v_r_3 >= 0 && -1 + v_52 + v_i_5 >= 0 && -1 + -1*v_52 + v_i_5 >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1 + -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && -1 + v_up_0 >= 0 && -1 + -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && -1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && -1*v_52 + -1*v_r_3 >= 0 && -1*v_52 >= 0 && v_52 >= 0 && -1 + v_i_5 >= v_n] 64. 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) -> eval_sipmamergesort_init_bb14_in(v_52,v_53,v_6,1 + 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_q_3 >= 0 (?,1) ,v_up_0) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && -1 + v_n + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1 + v_i_5 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1 + -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -2 + v_n + v_p_0 >= 0 && -2 + v_i_5 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && v_53 + -1*v_n >= 0 && -1 + v_n >= 0 && -2 + v_i_5 + v_n >= 0 && -1*v_i_5 + v_n >= 0 && -1 + -1*v_6 + v_n >= 0 && -3 + v_53 + v_n >= 0 && -2 + v_n + v_up_0 >= 0 && v_n + -1*v_up_0 >= 0 && -1 + v_n + -1*v_r_3 >= 0 && -1 + v_52 + v_n >= 0 && -1 + -1*v_52 + v_n >= 0 && v_53 + -1*v_i_5 >= 0 && -1 + v_i_5 >= 0 && -1 + -1*v_6 + v_i_5 >= 0 && -3 + v_53 + v_i_5 >= 0 && -2 + v_i_5 + v_up_0 >= 0 && v_i_5 + -1*v_up_0 >= 0 && -1 + v_i_5 + -1*v_r_3 >= 0 && -1 + v_52 + v_i_5 >= 0 && -1 + -1*v_52 + v_i_5 >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1 + -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && -1 + v_up_0 >= 0 && -1 + -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && -1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && -1*v_52 + -1*v_r_3 >= 0 && -1*v_52 >= 0 && v_52 >= 0] 65. 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) -> 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) [-1*v_q_3 >= 0 (1,1) && v_q_1 + -1*v_q_3 >= 0 && -1 + v_p_0 + -1*v_q_3 >= 0 && v_m_0 + -1*v_q_3 >= 0 && -1*v_6 + -1*v_q_3 >= 0 && -2 + v_53 + -1*v_q_3 >= 0 && -1*v_q_3 + v_up_0 >= 0 && 1 + -1*v_q_3 + -1*v_up_0 >= 0 && -1*v_q_3 + -1*v_r_3 >= 0 && v_52 + -1*v_q_3 >= 0 && 1 + -1*v_52 + -1*v_q_3 >= 0 && v_p_0 + -1*v_q_1 >= 0 && v_m_0 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_q_1 >= 0 && -1 + v_53 + -1*v_p_0 >= 0 && -1 + v_p_0 >= 0 && -1 + -1*v_6 + v_p_0 >= 0 && -3 + v_53 + v_p_0 >= 0 && -2 + v_p_0 + v_up_0 >= 0 && v_p_0 + -1*v_up_0 >= 0 && -1 + v_p_0 + -1*v_r_3 >= 0 && -1 + v_52 + v_p_0 >= 0 && -1 + -1*v_52 + v_p_0 >= 0 && v_53 + -1*v_n >= 0 && -1*v_6 >= 0 && -2 + v_53 + -1*v_6 >= 0 && -1*v_6 + v_up_0 >= 0 && 1 + -1*v_6 + -1*v_up_0 >= 0 && -1*v_6 + -1*v_r_3 >= 0 && v_52 + -1*v_6 >= 0 && 1 + -1*v_52 + -1*v_6 >= 0 && -2 + v_53 >= 0 && -3 + v_53 + v_up_0 >= 0 && -1 + v_53 + -1*v_up_0 >= 0 && -2 + v_53 + -1*v_r_3 >= 0 && -2 + v_52 + v_53 >= 0 && -2 + -1*v_52 + v_53 >= 0 && 1 + -1*v_up_0 >= 0 && 1 + -1*v_r_3 + -1*v_up_0 >= 0 && 1 + v_52 + -1*v_up_0 >= 0 && 1 + -1*v_52 + -1*v_up_0 >= 0 && v_up_0 >= 0 && -1*v_r_3 + v_up_0 >= 0 && -1 + v_52 + v_up_0 >= 0 && 1 + -1*v_52 + v_up_0 >= 0 && -1*v_r_3 >= 0 && v_r_1 + -1*v_r_3 >= 0 && v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 + -1*v_r_3 >= 0 && 1 + -1*v_52 >= 0 && v_52 >= 0] Signature: {(eval_sipmamergesort_init_0,12) ;(eval_sipmamergesort_init_1,12) ;(eval_sipmamergesort_init_10,12) ;(eval_sipmamergesort_init_11,12) ;(eval_sipmamergesort_init_12,12) ;(eval_sipmamergesort_init_13,12) ;(eval_sipmamergesort_init_14,12) ;(eval_sipmamergesort_init_15,12) ;(eval_sipmamergesort_init_16,12) ;(eval_sipmamergesort_init_17,12) ;(eval_sipmamergesort_init_18,12) ;(eval_sipmamergesort_init_19,12) ;(eval_sipmamergesort_init_2,12) ;(eval_sipmamergesort_init_20,12) ;(eval_sipmamergesort_init_21,12) ;(eval_sipmamergesort_init_22,12) ;(eval_sipmamergesort_init_23,12) ;(eval_sipmamergesort_init_24,12) ;(eval_sipmamergesort_init_25,12) ;(eval_sipmamergesort_init_26,12) ;(eval_sipmamergesort_init_3,12) ;(eval_sipmamergesort_init_4,12) ;(eval_sipmamergesort_init_5,12) ;(eval_sipmamergesort_init_6,12) ;(eval_sipmamergesort_init_7,12) ;(eval_sipmamergesort_init_77,12) ;(eval_sipmamergesort_init_78,12) ;(eval_sipmamergesort_init_79,12) ;(eval_sipmamergesort_init_8,12) ;(eval_sipmamergesort_init_80,12) ;(eval_sipmamergesort_init_81,12) ;(eval_sipmamergesort_init_83,12) ;(eval_sipmamergesort_init_84,12) ;(eval_sipmamergesort_init_85,12) ;(eval_sipmamergesort_init_86,12) ;(eval_sipmamergesort_init_9,12) ;(eval_sipmamergesort_init_bb0_in,12) ;(eval_sipmamergesort_init_bb10_in,12) ;(eval_sipmamergesort_init_bb11_in,12) ;(eval_sipmamergesort_init_bb12_in,12) ;(eval_sipmamergesort_init_bb13_in,12) ;(eval_sipmamergesort_init_bb14_in,12) ;(eval_sipmamergesort_init_bb15_in,12) ;(eval_sipmamergesort_init_bb16_in,12) ;(eval_sipmamergesort_init_bb1_in,12) ;(eval_sipmamergesort_init_bb2_in,12) ;(eval_sipmamergesort_init_bb3_in,12) ;(eval_sipmamergesort_init_bb4_in,12) ;(eval_sipmamergesort_init_bb5_in,12) ;(eval_sipmamergesort_init_bb6_in,12) ;(eval_sipmamergesort_init_bb7_in,12) ;(eval_sipmamergesort_init_bb8_in,12) ;(eval_sipmamergesort_init_bb9_in,12) ;(eval_sipmamergesort_init_start,12) ;(eval_sipmamergesort_init_stop,12)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8},8->{9},9->{10},10->{11},11->{12},12->{13} ,13->{14},14->{15},15->{16},16->{17},17->{18},18->{19},19->{20},20->{21},21->{22},22->{23},23->{24},24->{25} ,25->{26},26->{27},27->{28},28->{29},29->{31,32,33},30->{31,32,33},31->{34},32->{34,36},33->{35,36},34->{37 ,38},35->{41,42},36->{42},37->{39},38->{40},39->{34,35},40->{34,36},41->{43},42->{44,45},43->{41,42} ,44->{46},45->{47},46->{44,45},47->{48},48->{49},49->{50},50->{51},51->{52,53},52->{31,32,33},53->{54} ,54->{55},55->{56},56->{57},57->{58,59},58->{29,30},59->{60,61},60->{62,63},61->{65},62->{64},63->{65} ,64->{62,63},65->{}] + Applied Processor: Looptree + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65] | +- p:[29,58,57,56,55,54,53,51,50,49,48,47,45,42,35,33,30,52,39,37,34,31,32,40,38,36,43,41,46,44] c: [58] | | | `- p:[31,52,51,50,49,48,47,45,42,35,33,39,37,34,32,40,38,36,43,41,46,44] c: [] | `- p:[62,64] c: [64] NO