YES * Step 1: TrivialSCCs YES + Considered Problem: Rules: 0. eval_realheapsort_start(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb0_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) True (1,1) 1. eval_realheapsort_bb0_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_0(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) True (?,1) 2. eval_realheapsort_0(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_1(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) True (?,1) 3. eval_realheapsort_1(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_2(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) True (?,1) 4. eval_realheapsort_2(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb16_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [2 >= v_N] (?,1) 5. eval_realheapsort_2(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb1_in(v_33,v_90,v_N,v_j_0,v_j_1,1,v_k_1,v_m_0) [-1 + v_N >= 2] (?,1) 6. eval_realheapsort_bb16_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_stop(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) True (?,1) 7. eval_realheapsort_bb1_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb2_in(v_33,v_90,v_N,v_k_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -3 + v_N >= 0 && -1 + v_N >= v_k_0] (?,1) 8. eval_realheapsort_bb2_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort__critedge_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -3 + v_N >= 0 && 0 >= v_j_0] 9. eval_realheapsort_bb2_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb3_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -3 + v_N >= 0 && -1 + v_j_0 >= 0] 10. eval_realheapsort__critedge_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_28(1 + v_k_0,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -3 + v_N >= 0] 11. eval_realheapsort_bb3_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort__critedge_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_k_0 >= 0 && -2 + v_j_0 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -1 + v_j_0 >= 0 && -4 + v_N + v_j_0 >= 0 && -3 + v_N >= 0 && v_j_0 >= 0 && nondef_0 >= 0 && 1 + -2*nondef_0 + v_j_0 >= 0 && 1 >= 1 + -2*nondef_0 + v_j_0] 12. eval_realheapsort_bb3_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb4_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_k_0 >= 0 && -2 + v_j_0 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -1 + v_j_0 >= 0 && -4 + v_N + v_j_0 >= 0 && -3 + v_N >= 0 && v_j_0 >= 0 && nondef_0 >= 0 && 1 + -2*nondef_0 + v_j_0 >= 0 && 1 >= 1 + -2*nondef_0 + v_j_0] 13. eval_realheapsort_28(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_29(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_33 + -1*v_k_0 >= 0 && -1 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -3 + v_33 + v_k_0 >= 0 && 1 + -1*v_33 + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -1 + v_33 + -1*v_j_0 >= 0 && -3 + v_N >= 0 && -5 + v_33 + v_N >= 0 && -1*v_33 + v_N >= 0 && -2 + v_33 >= 0] 14. eval_realheapsort_bb4_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb2_in(v_33,v_90,v_N,-1 + nondef_3,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_k_0 >= 0 && -2 + v_j_0 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -1 + v_j_0 >= 0 && -4 + v_N + v_j_0 >= 0 && -3 + v_N >= 0 && v_j_0 >= 0 && nondef_1 >= 0 && 1 + -2*nondef_1 + v_j_0 >= 0 && 1 >= 1 + -2*nondef_1 + v_j_0 && nondef_2 >= 0 && 1 + -2*nondef_2 + v_j_0 >= 0 && 1 >= 1 + -2*nondef_2 + v_j_0 && nondef_3 >= 0 && 1 + -2*nondef_3 + v_j_0 >= 0 && 1 >= 1 + -2*nondef_3 + v_j_0] 15. eval_realheapsort_29(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb1_in(v_33,v_90,v_N,v_j_0,v_j_1,v_33,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_33 + -1*v_k_0 >= 0 && -1 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -3 + v_33 + v_k_0 >= 0 && 1 + -1*v_33 + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -1 + v_33 + -1*v_j_0 >= 0 && -3 + v_N >= 0 && -5 + v_33 + v_N >= 0 && -1*v_33 + v_N >= 0 && -2 + v_33 >= 0] 16. eval_realheapsort_bb1_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb5_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -3 + v_N >= 0 && -1 + v_k_0 >= -1 + v_N] (?,1) 17. eval_realheapsort_bb5_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_30(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (?,1) 18. eval_realheapsort_30(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_31(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (?,1) 19. eval_realheapsort_31(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_32(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (?,1) 20. eval_realheapsort_32(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_33(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (?,1) 21. eval_realheapsort_33(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_34(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (?,1) 22. eval_realheapsort_34(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_35(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (?,1) 23. eval_realheapsort_35(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_36(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (?,1) 24. eval_realheapsort_36(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_37(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (?,1) 25. eval_realheapsort_37(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_38(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (?,1) 26. eval_realheapsort_38(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_39(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (?,1) 27. eval_realheapsort_39(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb6_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,0,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (?,1) 28. eval_realheapsort_bb6_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb16_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [v_k_1 >= 0 (?,1) && -3 + v_k_0 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0 && -1 + v_k_1 >= -2 + v_N] 29. eval_realheapsort_bb6_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb7_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [v_k_1 >= 0 (?,1) && -3 + v_k_0 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0 && -2 + v_N >= v_k_1] 30. eval_realheapsort_bb7_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb8_in(v_33,v_90,v_N,v_j_0,0,v_k_0,v_k_1,v_m_0) [-2 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -2 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] 31. eval_realheapsort_bb8_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb15_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [v_k_1 >= 0 (?,1) && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0 && 2*v_j_1 >= -2 + v_N + -1*v_k_1] 32. eval_realheapsort_bb8_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb9_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [v_k_1 >= 0 (?,1) && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0 && -2 + v_N + -1*v_k_1 >= 1 + 2*v_j_1] 33. eval_realheapsort_bb15_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_85(v_33,1 + v_k_1,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [v_k_1 >= 0 (?,1) && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0] 34. eval_realheapsort_bb9_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb10_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -3 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -3 + -1*v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0 && -3 + v_N + -1*v_k_1 >= 1 + 2*v_j_1] 35. eval_realheapsort_bb9_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb11_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -3 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -3 + -1*v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0 && 1 + 2*v_j_1 = -2 + v_N + -1*v_k_1] 36. eval_realheapsort_85(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_86(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_90 + -1*v_k_1 >= 0 (?,1) && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -1 + v_90 + v_k_1 >= 0 && 1 + -1*v_90 + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -4 + v_90 + v_k_0 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -1 + v_90 + v_j_1 >= 0 && -3 + v_N >= 0 && -4 + v_90 + v_N >= 0 && -1 + v_90 >= 0] 37. eval_realheapsort_bb10_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb12_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-4 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -4 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -4 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -4 + v_N + v_k_1 >= 0 && -4 + v_k_0 >= 0 && -4 + v_j_1 + v_k_0 >= 0 && -4 + -1*v_j_1 + v_k_0 >= 0 && -8 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -4 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -4 + v_N + v_j_1 >= 0 && -4 + v_N >= 0] 38. eval_realheapsort_bb10_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb11_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-4 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -4 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -4 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -4 + v_N + v_k_1 >= 0 && -4 + v_k_0 >= 0 && -4 + v_j_1 + v_k_0 >= 0 && -4 + -1*v_j_1 + v_k_0 >= 0 && -8 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -4 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -4 + v_N + v_j_1 >= 0 && -4 + v_N >= 0] 39. eval_realheapsort_bb11_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb13_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,1 + 2*v_j_1) [-3 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -3 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -3 + -1*v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0] 40. eval_realheapsort_86(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb6_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_90,v_m_0) [-1 + v_90 + -1*v_k_1 >= 0 (?,1) && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -1 + v_90 + v_k_1 >= 0 && 1 + -1*v_90 + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -4 + v_90 + v_k_0 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -1 + v_90 + v_j_1 >= 0 && -3 + v_N >= 0 && -4 + v_90 + v_N >= 0 && -1 + v_90 >= 0] 41. eval_realheapsort_bb13_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb8_in(v_33,v_90,v_N,v_j_0,v_N,v_k_0,v_k_1,v_m_0) [-1 + v_m_0 >= 0 (?,1) && -1 + v_k_1 + v_m_0 >= 0 && -4 + v_k_0 + v_m_0 >= 0 && -1 + v_j_1 + v_m_0 >= 0 && -1 + -1*v_j_1 + v_m_0 >= 0 && -4 + v_N + v_m_0 >= 0 && -3 + v_k_0 + -1*v_k_1 >= 0 && -3 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -3 + -1*v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0] 42. eval_realheapsort_bb13_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb14_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_m_0 >= 0 (?,1) && -1 + v_k_1 + v_m_0 >= 0 && -4 + v_k_0 + v_m_0 >= 0 && -1 + v_j_1 + v_m_0 >= 0 && -1 + -1*v_j_1 + v_m_0 >= 0 && -4 + v_N + v_m_0 >= 0 && -3 + v_k_0 + -1*v_k_1 >= 0 && -3 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -3 + -1*v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0] 43. eval_realheapsort_bb12_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb13_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,2 + 2*v_j_1) [-4 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -4 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -4 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -4 + v_N + v_k_1 >= 0 && -4 + v_k_0 >= 0 && -4 + v_j_1 + v_k_0 >= 0 && -4 + -1*v_j_1 + v_k_0 >= 0 && -8 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -4 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -4 + v_N + v_j_1 >= 0 && -4 + v_N >= 0] 44. eval_realheapsort_bb14_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb8_in(v_33,v_90,v_N,v_j_0,v_m_0,v_k_0,v_k_1,v_m_0) [-1 + v_m_0 >= 0 (?,1) && -1 + v_k_1 + v_m_0 >= 0 && -4 + v_k_0 + v_m_0 >= 0 && -1 + v_j_1 + v_m_0 >= 0 && -1 + -1*v_j_1 + v_m_0 >= 0 && -4 + v_N + v_m_0 >= 0 && -3 + v_k_0 + -1*v_k_1 >= 0 && -3 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -3 + -1*v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0] Signature: {(eval_realheapsort_0,8) ;(eval_realheapsort_1,8) ;(eval_realheapsort_2,8) ;(eval_realheapsort_28,8) ;(eval_realheapsort_29,8) ;(eval_realheapsort_30,8) ;(eval_realheapsort_31,8) ;(eval_realheapsort_32,8) ;(eval_realheapsort_33,8) ;(eval_realheapsort_34,8) ;(eval_realheapsort_35,8) ;(eval_realheapsort_36,8) ;(eval_realheapsort_37,8) ;(eval_realheapsort_38,8) ;(eval_realheapsort_39,8) ;(eval_realheapsort_85,8) ;(eval_realheapsort_86,8) ;(eval_realheapsort__critedge_in,8) ;(eval_realheapsort_bb0_in,8) ;(eval_realheapsort_bb10_in,8) ;(eval_realheapsort_bb11_in,8) ;(eval_realheapsort_bb12_in,8) ;(eval_realheapsort_bb13_in,8) ;(eval_realheapsort_bb14_in,8) ;(eval_realheapsort_bb15_in,8) ;(eval_realheapsort_bb16_in,8) ;(eval_realheapsort_bb1_in,8) ;(eval_realheapsort_bb2_in,8) ;(eval_realheapsort_bb3_in,8) ;(eval_realheapsort_bb4_in,8) ;(eval_realheapsort_bb5_in,8) ;(eval_realheapsort_bb6_in,8) ;(eval_realheapsort_bb7_in,8) ;(eval_realheapsort_bb8_in,8) ;(eval_realheapsort_bb9_in,8) ;(eval_realheapsort_start,8) ;(eval_realheapsort_stop,8)} Flow Graph: [0->{1},1->{2},2->{3},3->{4,5},4->{6},5->{7,16},6->{},7->{8,9},8->{10},9->{11,12},10->{13},11->{10} ,12->{14},13->{15},14->{8,9},15->{7,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,29},28->{6},29->{30},30->{31,32},31->{33},32->{34,35},33->{36} ,34->{37,38},35->{39},36->{40},37->{43},38->{39},39->{41,42},40->{28,29},41->{31,32},42->{44},43->{41,42} ,44->{31,32}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths YES + Considered Problem: Rules: 0. eval_realheapsort_start(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb0_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) True (1,1) 1. eval_realheapsort_bb0_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_0(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) True (1,1) 2. eval_realheapsort_0(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_1(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) True (1,1) 3. eval_realheapsort_1(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_2(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) True (1,1) 4. eval_realheapsort_2(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb16_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [2 >= v_N] (1,1) 5. eval_realheapsort_2(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb1_in(v_33,v_90,v_N,v_j_0,v_j_1,1,v_k_1,v_m_0) [-1 + v_N >= 2] (1,1) 6. eval_realheapsort_bb16_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_stop(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) True (1,1) 7. eval_realheapsort_bb1_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb2_in(v_33,v_90,v_N,v_k_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -3 + v_N >= 0 && -1 + v_N >= v_k_0] (?,1) 8. eval_realheapsort_bb2_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort__critedge_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -3 + v_N >= 0 && 0 >= v_j_0] 9. eval_realheapsort_bb2_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb3_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -3 + v_N >= 0 && -1 + v_j_0 >= 0] 10. eval_realheapsort__critedge_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_28(1 + v_k_0,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -3 + v_N >= 0] 11. eval_realheapsort_bb3_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort__critedge_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_k_0 >= 0 && -2 + v_j_0 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -1 + v_j_0 >= 0 && -4 + v_N + v_j_0 >= 0 && -3 + v_N >= 0 && v_j_0 >= 0 && nondef_0 >= 0 && 1 + -2*nondef_0 + v_j_0 >= 0 && 1 >= 1 + -2*nondef_0 + v_j_0] 12. eval_realheapsort_bb3_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb4_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_k_0 >= 0 && -2 + v_j_0 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -1 + v_j_0 >= 0 && -4 + v_N + v_j_0 >= 0 && -3 + v_N >= 0 && v_j_0 >= 0 && nondef_0 >= 0 && 1 + -2*nondef_0 + v_j_0 >= 0 && 1 >= 1 + -2*nondef_0 + v_j_0] 13. eval_realheapsort_28(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_29(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_33 + -1*v_k_0 >= 0 && -1 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -3 + v_33 + v_k_0 >= 0 && 1 + -1*v_33 + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -1 + v_33 + -1*v_j_0 >= 0 && -3 + v_N >= 0 && -5 + v_33 + v_N >= 0 && -1*v_33 + v_N >= 0 && -2 + v_33 >= 0] 14. eval_realheapsort_bb4_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb2_in(v_33,v_90,v_N,-1 + nondef_3,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_k_0 >= 0 && -2 + v_j_0 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -1 + v_j_0 >= 0 && -4 + v_N + v_j_0 >= 0 && -3 + v_N >= 0 && v_j_0 >= 0 && nondef_1 >= 0 && 1 + -2*nondef_1 + v_j_0 >= 0 && 1 >= 1 + -2*nondef_1 + v_j_0 && nondef_2 >= 0 && 1 + -2*nondef_2 + v_j_0 >= 0 && 1 >= 1 + -2*nondef_2 + v_j_0 && nondef_3 >= 0 && 1 + -2*nondef_3 + v_j_0 >= 0 && 1 >= 1 + -2*nondef_3 + v_j_0] 15. eval_realheapsort_29(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb1_in(v_33,v_90,v_N,v_j_0,v_j_1,v_33,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_33 + -1*v_k_0 >= 0 && -1 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -3 + v_33 + v_k_0 >= 0 && 1 + -1*v_33 + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -1 + v_33 + -1*v_j_0 >= 0 && -3 + v_N >= 0 && -5 + v_33 + v_N >= 0 && -1*v_33 + v_N >= 0 && -2 + v_33 >= 0] 16. eval_realheapsort_bb1_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb5_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -3 + v_N >= 0 && -1 + v_k_0 >= -1 + v_N] (1,1) 17. eval_realheapsort_bb5_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_30(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 18. eval_realheapsort_30(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_31(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 19. eval_realheapsort_31(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_32(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 20. eval_realheapsort_32(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_33(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 21. eval_realheapsort_33(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_34(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 22. eval_realheapsort_34(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_35(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 23. eval_realheapsort_35(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_36(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 24. eval_realheapsort_36(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_37(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 25. eval_realheapsort_37(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_38(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 26. eval_realheapsort_38(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_39(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 27. eval_realheapsort_39(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb6_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,0,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 28. eval_realheapsort_bb6_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb16_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [v_k_1 >= 0 (1,1) && -3 + v_k_0 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0 && -1 + v_k_1 >= -2 + v_N] 29. eval_realheapsort_bb6_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb7_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [v_k_1 >= 0 (?,1) && -3 + v_k_0 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0 && -2 + v_N >= v_k_1] 30. eval_realheapsort_bb7_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb8_in(v_33,v_90,v_N,v_j_0,0,v_k_0,v_k_1,v_m_0) [-2 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -2 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] 31. eval_realheapsort_bb8_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb15_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [v_k_1 >= 0 (?,1) && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0 && 2*v_j_1 >= -2 + v_N + -1*v_k_1] 32. eval_realheapsort_bb8_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb9_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [v_k_1 >= 0 (?,1) && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0 && -2 + v_N + -1*v_k_1 >= 1 + 2*v_j_1] 33. eval_realheapsort_bb15_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_85(v_33,1 + v_k_1,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [v_k_1 >= 0 (?,1) && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0] 34. eval_realheapsort_bb9_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb10_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -3 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -3 + -1*v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0 && -3 + v_N + -1*v_k_1 >= 1 + 2*v_j_1] 35. eval_realheapsort_bb9_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb11_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -3 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -3 + -1*v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0 && 1 + 2*v_j_1 = -2 + v_N + -1*v_k_1] 36. eval_realheapsort_85(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_86(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_90 + -1*v_k_1 >= 0 (?,1) && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -1 + v_90 + v_k_1 >= 0 && 1 + -1*v_90 + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -4 + v_90 + v_k_0 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -1 + v_90 + v_j_1 >= 0 && -3 + v_N >= 0 && -4 + v_90 + v_N >= 0 && -1 + v_90 >= 0] 37. eval_realheapsort_bb10_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb12_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-4 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -4 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -4 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -4 + v_N + v_k_1 >= 0 && -4 + v_k_0 >= 0 && -4 + v_j_1 + v_k_0 >= 0 && -4 + -1*v_j_1 + v_k_0 >= 0 && -8 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -4 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -4 + v_N + v_j_1 >= 0 && -4 + v_N >= 0] 38. eval_realheapsort_bb10_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb11_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-4 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -4 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -4 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -4 + v_N + v_k_1 >= 0 && -4 + v_k_0 >= 0 && -4 + v_j_1 + v_k_0 >= 0 && -4 + -1*v_j_1 + v_k_0 >= 0 && -8 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -4 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -4 + v_N + v_j_1 >= 0 && -4 + v_N >= 0] 39. eval_realheapsort_bb11_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb13_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,1 + 2*v_j_1) [-3 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -3 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -3 + -1*v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0] 40. eval_realheapsort_86(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb6_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_90,v_m_0) [-1 + v_90 + -1*v_k_1 >= 0 (?,1) && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -1 + v_90 + v_k_1 >= 0 && 1 + -1*v_90 + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -4 + v_90 + v_k_0 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -1 + v_90 + v_j_1 >= 0 && -3 + v_N >= 0 && -4 + v_90 + v_N >= 0 && -1 + v_90 >= 0] 41. eval_realheapsort_bb13_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb8_in(v_33,v_90,v_N,v_j_0,v_N,v_k_0,v_k_1,v_m_0) [-1 + v_m_0 >= 0 (?,1) && -1 + v_k_1 + v_m_0 >= 0 && -4 + v_k_0 + v_m_0 >= 0 && -1 + v_j_1 + v_m_0 >= 0 && -1 + -1*v_j_1 + v_m_0 >= 0 && -4 + v_N + v_m_0 >= 0 && -3 + v_k_0 + -1*v_k_1 >= 0 && -3 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -3 + -1*v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0] 42. eval_realheapsort_bb13_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb14_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_m_0 >= 0 (?,1) && -1 + v_k_1 + v_m_0 >= 0 && -4 + v_k_0 + v_m_0 >= 0 && -1 + v_j_1 + v_m_0 >= 0 && -1 + -1*v_j_1 + v_m_0 >= 0 && -4 + v_N + v_m_0 >= 0 && -3 + v_k_0 + -1*v_k_1 >= 0 && -3 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -3 + -1*v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0] 43. eval_realheapsort_bb12_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb13_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,2 + 2*v_j_1) [-4 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -4 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -4 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -4 + v_N + v_k_1 >= 0 && -4 + v_k_0 >= 0 && -4 + v_j_1 + v_k_0 >= 0 && -4 + -1*v_j_1 + v_k_0 >= 0 && -8 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -4 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -4 + v_N + v_j_1 >= 0 && -4 + v_N >= 0] 44. eval_realheapsort_bb14_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb8_in(v_33,v_90,v_N,v_j_0,v_m_0,v_k_0,v_k_1,v_m_0) [-1 + v_m_0 >= 0 (?,1) && -1 + v_k_1 + v_m_0 >= 0 && -4 + v_k_0 + v_m_0 >= 0 && -1 + v_j_1 + v_m_0 >= 0 && -1 + -1*v_j_1 + v_m_0 >= 0 && -4 + v_N + v_m_0 >= 0 && -3 + v_k_0 + -1*v_k_1 >= 0 && -3 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -3 + -1*v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0] Signature: {(eval_realheapsort_0,8) ;(eval_realheapsort_1,8) ;(eval_realheapsort_2,8) ;(eval_realheapsort_28,8) ;(eval_realheapsort_29,8) ;(eval_realheapsort_30,8) ;(eval_realheapsort_31,8) ;(eval_realheapsort_32,8) ;(eval_realheapsort_33,8) ;(eval_realheapsort_34,8) ;(eval_realheapsort_35,8) ;(eval_realheapsort_36,8) ;(eval_realheapsort_37,8) ;(eval_realheapsort_38,8) ;(eval_realheapsort_39,8) ;(eval_realheapsort_85,8) ;(eval_realheapsort_86,8) ;(eval_realheapsort__critedge_in,8) ;(eval_realheapsort_bb0_in,8) ;(eval_realheapsort_bb10_in,8) ;(eval_realheapsort_bb11_in,8) ;(eval_realheapsort_bb12_in,8) ;(eval_realheapsort_bb13_in,8) ;(eval_realheapsort_bb14_in,8) ;(eval_realheapsort_bb15_in,8) ;(eval_realheapsort_bb16_in,8) ;(eval_realheapsort_bb1_in,8) ;(eval_realheapsort_bb2_in,8) ;(eval_realheapsort_bb3_in,8) ;(eval_realheapsort_bb4_in,8) ;(eval_realheapsort_bb5_in,8) ;(eval_realheapsort_bb6_in,8) ;(eval_realheapsort_bb7_in,8) ;(eval_realheapsort_bb8_in,8) ;(eval_realheapsort_bb9_in,8) ;(eval_realheapsort_start,8) ;(eval_realheapsort_stop,8)} Flow Graph: [0->{1},1->{2},2->{3},3->{4,5},4->{6},5->{7,16},6->{},7->{8,9},8->{10},9->{11,12},10->{13},11->{10} ,12->{14},13->{15},14->{8,9},15->{7,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,29},28->{6},29->{30},30->{31,32},31->{33},32->{34,35},33->{36} ,34->{37,38},35->{39},36->{40},37->{43},38->{39},39->{41,42},40->{28,29},41->{31,32},42->{44},43->{41,42} ,44->{31,32}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(5,16),(7,8),(27,28),(41,32)] * Step 3: Looptree YES + Considered Problem: Rules: 0. eval_realheapsort_start(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb0_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) True (1,1) 1. eval_realheapsort_bb0_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_0(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) True (1,1) 2. eval_realheapsort_0(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_1(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) True (1,1) 3. eval_realheapsort_1(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_2(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) True (1,1) 4. eval_realheapsort_2(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb16_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [2 >= v_N] (1,1) 5. eval_realheapsort_2(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb1_in(v_33,v_90,v_N,v_j_0,v_j_1,1,v_k_1,v_m_0) [-1 + v_N >= 2] (1,1) 6. eval_realheapsort_bb16_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_stop(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) True (1,1) 7. eval_realheapsort_bb1_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb2_in(v_33,v_90,v_N,v_k_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -3 + v_N >= 0 && -1 + v_N >= v_k_0] (?,1) 8. eval_realheapsort_bb2_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort__critedge_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -3 + v_N >= 0 && 0 >= v_j_0] 9. eval_realheapsort_bb2_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb3_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -3 + v_N >= 0 && -1 + v_j_0 >= 0] 10. eval_realheapsort__critedge_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_28(1 + v_k_0,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -3 + v_N >= 0] 11. eval_realheapsort_bb3_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort__critedge_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_k_0 >= 0 && -2 + v_j_0 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -1 + v_j_0 >= 0 && -4 + v_N + v_j_0 >= 0 && -3 + v_N >= 0 && v_j_0 >= 0 && nondef_0 >= 0 && 1 + -2*nondef_0 + v_j_0 >= 0 && 1 >= 1 + -2*nondef_0 + v_j_0] 12. eval_realheapsort_bb3_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb4_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_k_0 >= 0 && -2 + v_j_0 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -1 + v_j_0 >= 0 && -4 + v_N + v_j_0 >= 0 && -3 + v_N >= 0 && v_j_0 >= 0 && nondef_0 >= 0 && 1 + -2*nondef_0 + v_j_0 >= 0 && 1 >= 1 + -2*nondef_0 + v_j_0] 13. eval_realheapsort_28(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_29(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_33 + -1*v_k_0 >= 0 && -1 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -3 + v_33 + v_k_0 >= 0 && 1 + -1*v_33 + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -1 + v_33 + -1*v_j_0 >= 0 && -3 + v_N >= 0 && -5 + v_33 + v_N >= 0 && -1*v_33 + v_N >= 0 && -2 + v_33 >= 0] 14. eval_realheapsort_bb4_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb2_in(v_33,v_90,v_N,-1 + nondef_3,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_k_0 >= 0 && -2 + v_j_0 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -1 + v_j_0 >= 0 && -4 + v_N + v_j_0 >= 0 && -3 + v_N >= 0 && v_j_0 >= 0 && nondef_1 >= 0 && 1 + -2*nondef_1 + v_j_0 >= 0 && 1 >= 1 + -2*nondef_1 + v_j_0 && nondef_2 >= 0 && 1 + -2*nondef_2 + v_j_0 >= 0 && 1 >= 1 + -2*nondef_2 + v_j_0 && nondef_3 >= 0 && 1 + -2*nondef_3 + v_j_0 >= 0 && 1 >= 1 + -2*nondef_3 + v_j_0] 15. eval_realheapsort_29(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb1_in(v_33,v_90,v_N,v_j_0,v_j_1,v_33,v_k_1,v_m_0) [-1 + v_N + -1*v_k_0 >= 0 (?,1) && -1 + v_33 + -1*v_k_0 >= 0 && -1 + v_k_0 >= 0 && -1*v_j_0 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -3 + v_33 + v_k_0 >= 0 && 1 + -1*v_33 + v_k_0 >= 0 && -1 + v_N + -1*v_j_0 >= 0 && -1 + v_33 + -1*v_j_0 >= 0 && -3 + v_N >= 0 && -5 + v_33 + v_N >= 0 && -1*v_33 + v_N >= 0 && -2 + v_33 >= 0] 16. eval_realheapsort_bb1_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb5_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_k_0 >= 0 && -4 + v_N + v_k_0 >= 0 && -3 + v_N >= 0 && -1 + v_k_0 >= -1 + v_N] (1,1) 17. eval_realheapsort_bb5_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_30(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 18. eval_realheapsort_30(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_31(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 19. eval_realheapsort_31(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_32(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 20. eval_realheapsort_32(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_33(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 21. eval_realheapsort_33(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_34(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 22. eval_realheapsort_34(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_35(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 23. eval_realheapsort_35(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_36(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 24. eval_realheapsort_36(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_37(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 25. eval_realheapsort_37(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_38(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 26. eval_realheapsort_38(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_39(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 27. eval_realheapsort_39(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb6_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,0,v_m_0) [-3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] (1,1) 28. eval_realheapsort_bb6_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb16_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [v_k_1 >= 0 (1,1) && -3 + v_k_0 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0 && -1 + v_k_1 >= -2 + v_N] 29. eval_realheapsort_bb6_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb7_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [v_k_1 >= 0 (?,1) && -3 + v_k_0 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0 && -2 + v_N >= v_k_1] 30. eval_realheapsort_bb7_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb8_in(v_33,v_90,v_N,v_j_0,0,v_k_0,v_k_1,v_m_0) [-2 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -2 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N >= 0] 31. eval_realheapsort_bb8_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb15_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [v_k_1 >= 0 (?,1) && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0 && 2*v_j_1 >= -2 + v_N + -1*v_k_1] 32. eval_realheapsort_bb8_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb9_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [v_k_1 >= 0 (?,1) && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0 && -2 + v_N + -1*v_k_1 >= 1 + 2*v_j_1] 33. eval_realheapsort_bb15_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_85(v_33,1 + v_k_1,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [v_k_1 >= 0 (?,1) && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0] 34. eval_realheapsort_bb9_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb10_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -3 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -3 + -1*v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0 && -3 + v_N + -1*v_k_1 >= 1 + 2*v_j_1] 35. eval_realheapsort_bb9_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb11_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-3 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -3 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -3 + -1*v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0 && 1 + 2*v_j_1 = -2 + v_N + -1*v_k_1] 36. eval_realheapsort_85(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_86(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_90 + -1*v_k_1 >= 0 (?,1) && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -1 + v_90 + v_k_1 >= 0 && 1 + -1*v_90 + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -4 + v_90 + v_k_0 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -1 + v_90 + v_j_1 >= 0 && -3 + v_N >= 0 && -4 + v_90 + v_N >= 0 && -1 + v_90 >= 0] 37. eval_realheapsort_bb10_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb12_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-4 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -4 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -4 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -4 + v_N + v_k_1 >= 0 && -4 + v_k_0 >= 0 && -4 + v_j_1 + v_k_0 >= 0 && -4 + -1*v_j_1 + v_k_0 >= 0 && -8 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -4 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -4 + v_N + v_j_1 >= 0 && -4 + v_N >= 0] 38. eval_realheapsort_bb10_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb11_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-4 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -4 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -4 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -4 + v_N + v_k_1 >= 0 && -4 + v_k_0 >= 0 && -4 + v_j_1 + v_k_0 >= 0 && -4 + -1*v_j_1 + v_k_0 >= 0 && -8 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -4 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -4 + v_N + v_j_1 >= 0 && -4 + v_N >= 0] 39. eval_realheapsort_bb11_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb13_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,1 + 2*v_j_1) [-3 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -3 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -3 + -1*v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0] 40. eval_realheapsort_86(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb6_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_90,v_m_0) [-1 + v_90 + -1*v_k_1 >= 0 (?,1) && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -1 + v_90 + v_k_1 >= 0 && 1 + -1*v_90 + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -4 + v_90 + v_k_0 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -1 + v_90 + v_j_1 >= 0 && -3 + v_N >= 0 && -4 + v_90 + v_N >= 0 && -1 + v_90 >= 0] 41. eval_realheapsort_bb13_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb8_in(v_33,v_90,v_N,v_j_0,v_N,v_k_0,v_k_1,v_m_0) [-1 + v_m_0 >= 0 (?,1) && -1 + v_k_1 + v_m_0 >= 0 && -4 + v_k_0 + v_m_0 >= 0 && -1 + v_j_1 + v_m_0 >= 0 && -1 + -1*v_j_1 + v_m_0 >= 0 && -4 + v_N + v_m_0 >= 0 && -3 + v_k_0 + -1*v_k_1 >= 0 && -3 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -3 + -1*v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0] 42. eval_realheapsort_bb13_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb14_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) [-1 + v_m_0 >= 0 (?,1) && -1 + v_k_1 + v_m_0 >= 0 && -4 + v_k_0 + v_m_0 >= 0 && -1 + v_j_1 + v_m_0 >= 0 && -1 + -1*v_j_1 + v_m_0 >= 0 && -4 + v_N + v_m_0 >= 0 && -3 + v_k_0 + -1*v_k_1 >= 0 && -3 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -3 + -1*v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0] 43. eval_realheapsort_bb12_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb13_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,2 + 2*v_j_1) [-4 + v_k_0 + -1*v_k_1 >= 0 (?,1) && -4 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -4 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -4 + v_N + v_k_1 >= 0 && -4 + v_k_0 >= 0 && -4 + v_j_1 + v_k_0 >= 0 && -4 + -1*v_j_1 + v_k_0 >= 0 && -8 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -4 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -4 + v_N + v_j_1 >= 0 && -4 + v_N >= 0] 44. eval_realheapsort_bb14_in(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) -> eval_realheapsort_bb8_in(v_33,v_90,v_N,v_j_0,v_m_0,v_k_0,v_k_1,v_m_0) [-1 + v_m_0 >= 0 (?,1) && -1 + v_k_1 + v_m_0 >= 0 && -4 + v_k_0 + v_m_0 >= 0 && -1 + v_j_1 + v_m_0 >= 0 && -1 + -1*v_j_1 + v_m_0 >= 0 && -4 + v_N + v_m_0 >= 0 && -3 + v_k_0 + -1*v_k_1 >= 0 && -3 + v_N + -1*v_k_1 >= 0 && v_k_1 >= 0 && -3 + v_k_0 + v_k_1 >= 0 && v_j_1 + v_k_1 >= 0 && -3 + v_N + v_k_1 >= 0 && -3 + v_k_0 >= 0 && -3 + v_j_1 + v_k_0 >= 0 && -3 + -1*v_j_1 + v_k_0 >= 0 && -6 + v_N + v_k_0 >= 0 && -1*v_N + v_k_0 >= 0 && -3 + v_N + -1*v_j_1 >= 0 && v_j_1 >= 0 && -3 + v_N + v_j_1 >= 0 && -3 + v_N >= 0] Signature: {(eval_realheapsort_0,8) ;(eval_realheapsort_1,8) ;(eval_realheapsort_2,8) ;(eval_realheapsort_28,8) ;(eval_realheapsort_29,8) ;(eval_realheapsort_30,8) ;(eval_realheapsort_31,8) ;(eval_realheapsort_32,8) ;(eval_realheapsort_33,8) ;(eval_realheapsort_34,8) ;(eval_realheapsort_35,8) ;(eval_realheapsort_36,8) ;(eval_realheapsort_37,8) ;(eval_realheapsort_38,8) ;(eval_realheapsort_39,8) ;(eval_realheapsort_85,8) ;(eval_realheapsort_86,8) ;(eval_realheapsort__critedge_in,8) ;(eval_realheapsort_bb0_in,8) ;(eval_realheapsort_bb10_in,8) ;(eval_realheapsort_bb11_in,8) ;(eval_realheapsort_bb12_in,8) ;(eval_realheapsort_bb13_in,8) ;(eval_realheapsort_bb14_in,8) ;(eval_realheapsort_bb15_in,8) ;(eval_realheapsort_bb16_in,8) ;(eval_realheapsort_bb1_in,8) ;(eval_realheapsort_bb2_in,8) ;(eval_realheapsort_bb3_in,8) ;(eval_realheapsort_bb4_in,8) ;(eval_realheapsort_bb5_in,8) ;(eval_realheapsort_bb6_in,8) ;(eval_realheapsort_bb7_in,8) ;(eval_realheapsort_bb8_in,8) ;(eval_realheapsort_bb9_in,8) ;(eval_realheapsort_start,8) ;(eval_realheapsort_stop,8)} Flow Graph: [0->{1},1->{2},2->{3},3->{4,5},4->{6},5->{7},6->{},7->{9},8->{10},9->{11,12},10->{13},11->{10},12->{14} ,13->{15},14->{8,9},15->{7,16},16->{17},17->{18},18->{19},19->{20},20->{21},21->{22},22->{23},23->{24} ,24->{25},25->{26},26->{27},27->{29},28->{6},29->{30},30->{31,32},31->{33},32->{34,35},33->{36},34->{37,38} ,35->{39},36->{40},37->{43},38->{39},39->{41,42},40->{28,29},41->{31},42->{44},43->{41,42},44->{31,32}] + 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] | +- p:[7,15,13,10,8,14,12,9,11] c: [15] | | | `- p:[9,14,12] c: [14] | `- p:[29,40,36,33,31,30,41,39,35,32,44,42,43,37,34,38] c: [30] | `- p:[32,44,42,39,35,38,34,43,37] c: [44] YES