YES(?,POLY) * Step 1: TrivialSCCs WORST_CASE(?,POLY) + 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 WORST_CASE(?,POLY) + 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: AddSinks WORST_CASE(?,POLY) + 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: AddSinks + Details: () * Step 4: UnsatPaths WORST_CASE(?,POLY) + 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] 45. 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) -> exitus616(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) True (?,1) 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) ;(exitus616,8)} Flow Graph: [0->{1},1->{2},2->{3},3->{4,5},4->{6,45},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,45},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},45->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(5,16),(7,8),(27,28),(41,32)] * Step 5: LooptreeTransformer WORST_CASE(?,POLY) + 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] 45. 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) -> exitus616(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) True (?,1) 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) ;(exitus616,8)} Flow Graph: [0->{1},1->{2},2->{3},3->{4,5},4->{6,45},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,45},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} ,45->{}] + Applied Processor: LooptreeTransformer + 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] | +- 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] * Step 6: SizeAbstraction WORST_CASE(?,POLY) + 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] 45. 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) -> exitus616(v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0) True (?,1) 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) ;(exitus616,8)} Flow Graph: [0->{1},1->{2},2->{3},3->{4,5},4->{6,45},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,45},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} ,45->{}] ,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] | +- 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]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0,0.0,0.0.0,0.1,0.1.0] eval_realheapsort_start ~> eval_realheapsort_bb0_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb0_in ~> eval_realheapsort_0 [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_0 ~> eval_realheapsort_1 [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_1 ~> eval_realheapsort_2 [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_2 ~> eval_realheapsort_bb16_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_2 ~> eval_realheapsort_bb1_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= K, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb16_in ~> eval_realheapsort_stop [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb1_in ~> eval_realheapsort_bb2_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_k_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb2_in ~> eval_realheapsort__critedge_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb2_in ~> eval_realheapsort_bb3_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort__critedge_in ~> eval_realheapsort_28 [v_33 <= v_N, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb3_in ~> eval_realheapsort__critedge_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb3_in ~> eval_realheapsort_bb4_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_28 ~> eval_realheapsort_29 [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb4_in ~> eval_realheapsort_bb2_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_N, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_29 ~> eval_realheapsort_bb1_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_33, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb1_in ~> eval_realheapsort_bb5_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb5_in ~> eval_realheapsort_30 [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_30 ~> eval_realheapsort_31 [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_31 ~> eval_realheapsort_32 [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_32 ~> eval_realheapsort_33 [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_33 ~> eval_realheapsort_34 [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_34 ~> eval_realheapsort_35 [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_35 ~> eval_realheapsort_36 [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_36 ~> eval_realheapsort_37 [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_37 ~> eval_realheapsort_38 [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_38 ~> eval_realheapsort_39 [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_39 ~> eval_realheapsort_bb6_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= 0*K, v_m_0 <= v_m_0] eval_realheapsort_bb6_in ~> eval_realheapsort_bb16_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb6_in ~> eval_realheapsort_bb7_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb7_in ~> eval_realheapsort_bb8_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= 0*K, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb8_in ~> eval_realheapsort_bb15_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb8_in ~> eval_realheapsort_bb9_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb15_in ~> eval_realheapsort_85 [v_33 <= v_33, v_90 <= v_k_0 + v_k_1, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb9_in ~> eval_realheapsort_bb10_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb9_in ~> eval_realheapsort_bb11_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_85 ~> eval_realheapsort_86 [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb10_in ~> eval_realheapsort_bb12_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb10_in ~> eval_realheapsort_bb11_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb11_in ~> eval_realheapsort_bb13_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_j_1 + v_k_0] eval_realheapsort_86 ~> eval_realheapsort_bb6_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_90, v_m_0 <= v_m_0] eval_realheapsort_bb13_in ~> eval_realheapsort_bb8_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_N, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb13_in ~> eval_realheapsort_bb14_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb12_in ~> eval_realheapsort_bb13_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_j_1 + v_k_0] eval_realheapsort_bb14_in ~> eval_realheapsort_bb8_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_m_0, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb16_in ~> exitus616 [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] + Loop: [0.0 <= v_N + v_k_0] eval_realheapsort_bb1_in ~> eval_realheapsort_bb2_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_k_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_29 ~> eval_realheapsort_bb1_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_33, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_28 ~> eval_realheapsort_29 [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort__critedge_in ~> eval_realheapsort_28 [v_33 <= v_N, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb2_in ~> eval_realheapsort__critedge_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb4_in ~> eval_realheapsort_bb2_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_N, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb3_in ~> eval_realheapsort_bb4_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb2_in ~> eval_realheapsort_bb3_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb3_in ~> eval_realheapsort__critedge_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] + Loop: [0.0.0 <= K + 2*v_j_0] eval_realheapsort_bb2_in ~> eval_realheapsort_bb3_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb4_in ~> eval_realheapsort_bb2_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_N, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb3_in ~> eval_realheapsort_bb4_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] + Loop: [0.1 <= 2*K + v_90 + v_N + v_k_1] eval_realheapsort_bb6_in ~> eval_realheapsort_bb7_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_86 ~> eval_realheapsort_bb6_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_90, v_m_0 <= v_m_0] eval_realheapsort_85 ~> eval_realheapsort_86 [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb15_in ~> eval_realheapsort_85 [v_33 <= v_33, v_90 <= v_k_0 + v_k_1, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb8_in ~> eval_realheapsort_bb15_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb7_in ~> eval_realheapsort_bb8_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= 0*K, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb13_in ~> eval_realheapsort_bb8_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_N, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb11_in ~> eval_realheapsort_bb13_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_j_1 + v_k_0] eval_realheapsort_bb9_in ~> eval_realheapsort_bb11_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb8_in ~> eval_realheapsort_bb9_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb14_in ~> eval_realheapsort_bb8_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_m_0, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb13_in ~> eval_realheapsort_bb14_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb12_in ~> eval_realheapsort_bb13_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_j_1 + v_k_0] eval_realheapsort_bb10_in ~> eval_realheapsort_bb12_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb9_in ~> eval_realheapsort_bb10_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb10_in ~> eval_realheapsort_bb11_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] + Loop: [0.1.0 <= 2*K + v_N + v_j_1] eval_realheapsort_bb8_in ~> eval_realheapsort_bb9_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb14_in ~> eval_realheapsort_bb8_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_m_0, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb13_in ~> eval_realheapsort_bb14_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb11_in ~> eval_realheapsort_bb13_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_j_1 + v_k_0] eval_realheapsort_bb9_in ~> eval_realheapsort_bb11_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb10_in ~> eval_realheapsort_bb11_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb9_in ~> eval_realheapsort_bb10_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] eval_realheapsort_bb12_in ~> eval_realheapsort_bb13_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_j_1 + v_k_0] eval_realheapsort_bb10_in ~> eval_realheapsort_bb12_in [v_33 <= v_33, v_90 <= v_90, v_N <= v_N, v_j_0 <= v_j_0, v_j_1 <= v_j_1, v_k_0 <= v_k_0, v_k_1 <= v_k_1, v_m_0 <= v_m_0] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,v_33,v_90,v_N,v_j_0,v_j_1,v_k_0,v_k_1,v_m_0,0.0,0.0.0,0.1,0.1.0] eval_realheapsort_start ~> eval_realheapsort_bb0_in [] eval_realheapsort_bb0_in ~> eval_realheapsort_0 [] eval_realheapsort_0 ~> eval_realheapsort_1 [] eval_realheapsort_1 ~> eval_realheapsort_2 [] eval_realheapsort_2 ~> eval_realheapsort_bb16_in [] eval_realheapsort_2 ~> eval_realheapsort_bb1_in [K ~=> v_k_0] eval_realheapsort_bb16_in ~> eval_realheapsort_stop [] eval_realheapsort_bb1_in ~> eval_realheapsort_bb2_in [v_k_0 ~=> v_j_0] eval_realheapsort_bb2_in ~> eval_realheapsort__critedge_in [] eval_realheapsort_bb2_in ~> eval_realheapsort_bb3_in [] eval_realheapsort__critedge_in ~> eval_realheapsort_28 [v_N ~=> v_33] eval_realheapsort_bb3_in ~> eval_realheapsort__critedge_in [] eval_realheapsort_bb3_in ~> eval_realheapsort_bb4_in [] eval_realheapsort_28 ~> eval_realheapsort_29 [] eval_realheapsort_bb4_in ~> eval_realheapsort_bb2_in [v_N ~=> v_j_0] eval_realheapsort_29 ~> eval_realheapsort_bb1_in [v_33 ~=> v_k_0] eval_realheapsort_bb1_in ~> eval_realheapsort_bb5_in [] eval_realheapsort_bb5_in ~> eval_realheapsort_30 [] eval_realheapsort_30 ~> eval_realheapsort_31 [] eval_realheapsort_31 ~> eval_realheapsort_32 [] eval_realheapsort_32 ~> eval_realheapsort_33 [] eval_realheapsort_33 ~> eval_realheapsort_34 [] eval_realheapsort_34 ~> eval_realheapsort_35 [] eval_realheapsort_35 ~> eval_realheapsort_36 [] eval_realheapsort_36 ~> eval_realheapsort_37 [] eval_realheapsort_37 ~> eval_realheapsort_38 [] eval_realheapsort_38 ~> eval_realheapsort_39 [] eval_realheapsort_39 ~> eval_realheapsort_bb6_in [K ~=> v_k_1] eval_realheapsort_bb6_in ~> eval_realheapsort_bb16_in [] eval_realheapsort_bb6_in ~> eval_realheapsort_bb7_in [] eval_realheapsort_bb7_in ~> eval_realheapsort_bb8_in [K ~=> v_j_1] eval_realheapsort_bb8_in ~> eval_realheapsort_bb15_in [] eval_realheapsort_bb8_in ~> eval_realheapsort_bb9_in [] eval_realheapsort_bb15_in ~> eval_realheapsort_85 [v_k_0 ~+> v_90,v_k_1 ~+> v_90] eval_realheapsort_bb9_in ~> eval_realheapsort_bb10_in [] eval_realheapsort_bb9_in ~> eval_realheapsort_bb11_in [] eval_realheapsort_85 ~> eval_realheapsort_86 [] eval_realheapsort_bb10_in ~> eval_realheapsort_bb12_in [] eval_realheapsort_bb10_in ~> eval_realheapsort_bb11_in [] eval_realheapsort_bb11_in ~> eval_realheapsort_bb13_in [v_j_1 ~+> v_m_0,v_k_0 ~+> v_m_0] eval_realheapsort_86 ~> eval_realheapsort_bb6_in [v_90 ~=> v_k_1] eval_realheapsort_bb13_in ~> eval_realheapsort_bb8_in [v_N ~=> v_j_1] eval_realheapsort_bb13_in ~> eval_realheapsort_bb14_in [] eval_realheapsort_bb12_in ~> eval_realheapsort_bb13_in [v_j_1 ~+> v_m_0,v_k_0 ~+> v_m_0] eval_realheapsort_bb14_in ~> eval_realheapsort_bb8_in [v_m_0 ~=> v_j_1] eval_realheapsort_bb16_in ~> exitus616 [] + Loop: [v_N ~+> 0.0,v_k_0 ~+> 0.0] eval_realheapsort_bb1_in ~> eval_realheapsort_bb2_in [v_k_0 ~=> v_j_0] eval_realheapsort_29 ~> eval_realheapsort_bb1_in [v_33 ~=> v_k_0] eval_realheapsort_28 ~> eval_realheapsort_29 [] eval_realheapsort__critedge_in ~> eval_realheapsort_28 [v_N ~=> v_33] eval_realheapsort_bb2_in ~> eval_realheapsort__critedge_in [] eval_realheapsort_bb4_in ~> eval_realheapsort_bb2_in [v_N ~=> v_j_0] eval_realheapsort_bb3_in ~> eval_realheapsort_bb4_in [] eval_realheapsort_bb2_in ~> eval_realheapsort_bb3_in [] eval_realheapsort_bb3_in ~> eval_realheapsort__critedge_in [] + Loop: [K ~+> 0.0.0,v_j_0 ~*> 0.0.0] eval_realheapsort_bb2_in ~> eval_realheapsort_bb3_in [] eval_realheapsort_bb4_in ~> eval_realheapsort_bb2_in [v_N ~=> v_j_0] eval_realheapsort_bb3_in ~> eval_realheapsort_bb4_in [] + Loop: [v_90 ~+> 0.1,v_N ~+> 0.1,v_k_1 ~+> 0.1,K ~*> 0.1] eval_realheapsort_bb6_in ~> eval_realheapsort_bb7_in [] eval_realheapsort_86 ~> eval_realheapsort_bb6_in [v_90 ~=> v_k_1] eval_realheapsort_85 ~> eval_realheapsort_86 [] eval_realheapsort_bb15_in ~> eval_realheapsort_85 [v_k_0 ~+> v_90,v_k_1 ~+> v_90] eval_realheapsort_bb8_in ~> eval_realheapsort_bb15_in [] eval_realheapsort_bb7_in ~> eval_realheapsort_bb8_in [K ~=> v_j_1] eval_realheapsort_bb13_in ~> eval_realheapsort_bb8_in [v_N ~=> v_j_1] eval_realheapsort_bb11_in ~> eval_realheapsort_bb13_in [v_j_1 ~+> v_m_0,v_k_0 ~+> v_m_0] eval_realheapsort_bb9_in ~> eval_realheapsort_bb11_in [] eval_realheapsort_bb8_in ~> eval_realheapsort_bb9_in [] eval_realheapsort_bb14_in ~> eval_realheapsort_bb8_in [v_m_0 ~=> v_j_1] eval_realheapsort_bb13_in ~> eval_realheapsort_bb14_in [] eval_realheapsort_bb12_in ~> eval_realheapsort_bb13_in [v_j_1 ~+> v_m_0,v_k_0 ~+> v_m_0] eval_realheapsort_bb10_in ~> eval_realheapsort_bb12_in [] eval_realheapsort_bb9_in ~> eval_realheapsort_bb10_in [] eval_realheapsort_bb10_in ~> eval_realheapsort_bb11_in [] + Loop: [v_N ~+> 0.1.0,v_j_1 ~+> 0.1.0,K ~*> 0.1.0] eval_realheapsort_bb8_in ~> eval_realheapsort_bb9_in [] eval_realheapsort_bb14_in ~> eval_realheapsort_bb8_in [v_m_0 ~=> v_j_1] eval_realheapsort_bb13_in ~> eval_realheapsort_bb14_in [] eval_realheapsort_bb11_in ~> eval_realheapsort_bb13_in [v_j_1 ~+> v_m_0,v_k_0 ~+> v_m_0] eval_realheapsort_bb9_in ~> eval_realheapsort_bb11_in [] eval_realheapsort_bb10_in ~> eval_realheapsort_bb11_in [] eval_realheapsort_bb9_in ~> eval_realheapsort_bb10_in [] eval_realheapsort_bb12_in ~> eval_realheapsort_bb13_in [v_j_1 ~+> v_m_0,v_k_0 ~+> v_m_0] eval_realheapsort_bb10_in ~> eval_realheapsort_bb12_in [] + Applied Processor: LareProcessor + Details: eval_realheapsort_start ~> eval_realheapsort_stop [v_N ~=> v_33 ,v_N ~=> v_j_0 ,v_N ~=> v_j_1 ,v_N ~=> v_k_0 ,K ~=> v_j_0 ,K ~=> v_j_1 ,K ~=> v_k_0 ,K ~=> v_k_1 ,v_90 ~+> 0.1 ,v_90 ~+> tick ,v_N ~+> v_90 ,v_N ~+> v_j_1 ,v_N ~+> v_k_1 ,v_N ~+> v_m_0 ,v_N ~+> 0.0 ,v_N ~+> 0.1 ,v_N ~+> 0.1.0 ,v_N ~+> tick ,tick ~+> tick ,K ~+> v_90 ,K ~+> v_j_1 ,K ~+> v_k_1 ,K ~+> v_m_0 ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> tick ,v_90 ~*> v_j_1 ,v_90 ~*> v_k_1 ,v_90 ~*> tick ,v_N ~*> v_90 ,v_N ~*> v_j_1 ,v_N ~*> v_k_1 ,v_N ~*> v_m_0 ,v_N ~*> 0.0.0 ,v_N ~*> 0.1.0 ,v_N ~*> tick ,K ~*> v_90 ,K ~*> v_j_1 ,K ~*> v_k_1 ,K ~*> v_m_0 ,K ~*> 0.0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> tick ,v_90 ~^> v_j_1 ,v_N ~^> v_j_1 ,K ~^> v_j_1] eval_realheapsort_start ~> exitus616 [v_N ~=> v_33 ,v_N ~=> v_j_0 ,v_N ~=> v_j_1 ,v_N ~=> v_k_0 ,K ~=> v_j_0 ,K ~=> v_j_1 ,K ~=> v_k_0 ,K ~=> v_k_1 ,v_90 ~+> 0.1 ,v_90 ~+> tick ,v_N ~+> v_90 ,v_N ~+> v_j_1 ,v_N ~+> v_k_1 ,v_N ~+> v_m_0 ,v_N ~+> 0.0 ,v_N ~+> 0.1 ,v_N ~+> 0.1.0 ,v_N ~+> tick ,tick ~+> tick ,K ~+> v_90 ,K ~+> v_j_1 ,K ~+> v_k_1 ,K ~+> v_m_0 ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> tick ,v_90 ~*> v_j_1 ,v_90 ~*> v_k_1 ,v_90 ~*> tick ,v_N ~*> v_90 ,v_N ~*> v_j_1 ,v_N ~*> v_k_1 ,v_N ~*> v_m_0 ,v_N ~*> 0.0.0 ,v_N ~*> 0.1.0 ,v_N ~*> tick ,K ~*> v_90 ,K ~*> v_j_1 ,K ~*> v_k_1 ,K ~*> v_m_0 ,K ~*> 0.0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> tick ,v_90 ~^> v_j_1 ,v_N ~^> v_j_1 ,K ~^> v_j_1] + eval_realheapsort_bb1_in> [v_N ~=> v_33 ,v_N ~=> v_j_0 ,v_N ~=> v_k_0 ,v_k_0 ~=> v_j_0 ,v_N ~+> 0.0 ,v_N ~+> tick ,v_k_0 ~+> 0.0 ,v_k_0 ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,v_N ~*> 0.0.0 ,v_N ~*> tick ,v_k_0 ~*> 0.0.0 ,v_k_0 ~*> tick ,K ~*> tick] + eval_realheapsort_bb3_in> [v_N ~=> v_j_0 ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,v_j_0 ~*> 0.0.0 ,v_j_0 ~*> tick] eval_realheapsort_bb2_in> [v_N ~=> v_j_0 ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,v_j_0 ~*> 0.0.0 ,v_j_0 ~*> tick] + eval_realheapsort_bb6_in> [v_N ~=> v_j_1 ,K ~=> v_j_1 ,v_90 ~+> 0.1 ,v_90 ~+> tick ,v_N ~+> v_j_1 ,v_N ~+> v_m_0 ,v_N ~+> 0.1 ,v_N ~+> 0.1.0 ,v_N ~+> tick ,v_k_0 ~+> v_90 ,v_k_0 ~+> v_j_1 ,v_k_0 ~+> v_k_1 ,v_k_0 ~+> v_m_0 ,v_k_0 ~+> 0.1.0 ,v_k_0 ~+> tick ,v_k_1 ~+> v_90 ,v_k_1 ~+> v_k_1 ,v_k_1 ~+> 0.1 ,v_k_1 ~+> tick ,tick ~+> tick ,K ~+> v_j_1 ,K ~+> v_m_0 ,K ~+> 0.1.0 ,K ~+> tick ,v_90 ~*> v_j_1 ,v_90 ~*> v_k_1 ,v_90 ~*> tick ,v_N ~*> v_j_1 ,v_N ~*> v_k_1 ,v_N ~*> v_m_0 ,v_N ~*> 0.1.0 ,v_N ~*> tick ,v_k_0 ~*> v_90 ,v_k_0 ~*> v_j_1 ,v_k_0 ~*> v_k_1 ,v_k_0 ~*> v_m_0 ,v_k_0 ~*> 0.1.0 ,v_k_0 ~*> tick ,v_k_1 ~*> v_j_1 ,v_k_1 ~*> v_k_1 ,v_k_1 ~*> tick ,K ~*> v_j_1 ,K ~*> v_k_1 ,K ~*> v_m_0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> tick ,v_90 ~^> v_j_1 ,v_N ~^> v_j_1 ,v_k_1 ~^> v_j_1 ,K ~^> v_j_1] + eval_realheapsort_bb8_in> [v_N ~+> 0.1.0 ,v_N ~+> tick ,v_j_1 ~+> v_j_1 ,v_j_1 ~+> v_m_0 ,v_j_1 ~+> 0.1.0 ,v_j_1 ~+> tick ,v_k_0 ~+> v_j_1 ,v_k_0 ~+> v_m_0 ,tick ~+> tick ,v_N ~*> v_j_1 ,v_j_1 ~*> v_j_1 ,v_k_0 ~*> v_j_1 ,v_k_0 ~*> v_m_0 ,K ~*> v_j_1 ,K ~*> 0.1.0 ,K ~*> tick] eval_realheapsort_bb13_in> [v_N ~+> 0.1.0 ,v_N ~+> tick ,v_j_1 ~+> v_j_1 ,v_j_1 ~+> v_m_0 ,v_j_1 ~+> 0.1.0 ,v_j_1 ~+> tick ,v_k_0 ~+> v_j_1 ,v_k_0 ~+> v_m_0 ,tick ~+> tick ,v_N ~*> v_j_1 ,v_N ~*> v_m_0 ,v_j_1 ~*> v_j_1 ,v_j_1 ~*> v_m_0 ,v_k_0 ~*> v_j_1 ,v_k_0 ~*> v_m_0 ,K ~*> v_j_1 ,K ~*> v_m_0 ,K ~*> 0.1.0 ,K ~*> tick] YES(?,POLY)