YES * Step 1: TrivialSCCs YES + Considered Problem: Rules: 0. eval_heapsort_start(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb0_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 1. eval_heapsort_bb0_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 2. eval_heapsort_0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 3. eval_heapsort_1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 4. eval_heapsort_2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 5. eval_heapsort_3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 6. eval_heapsort_4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 7. eval_heapsort_5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 8. eval_heapsort_6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 9. eval_heapsort_7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 10. eval_heapsort_8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 11. eval_heapsort_9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,1,v_max_1,v_max_3,v_size) True (?,1) 12. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= 0 && 0 >= v_size] (?,1) 13. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= 0 && -1 + v_size >= 0 && v_i_0 >= 1] (?,1) 14. eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_stop(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= 0] (?,1) 15. eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_i_0,v_max_3,v_size) [-1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -1 + v_i_0 >= 0 && -1 + 2*v_i_0 >= v_size] (?,1) 16. eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb3_in(v_13,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -1 + v_i_0 >= 0 && v_size >= 2*v_i_0] (?,1) 17. eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1,v_size) [-1 + v_size >= 0 (?,1) && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && -1 + v_4 >= v_size] 18. eval_heapsort_bb3_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb4_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-2 + v_size >= 0 (?,1) && -3 + v_i_0 + v_size >= 0 && -1 + -1*v_i_0 + v_size >= 0 && -5 + v_4 + v_size >= 0 && -4 + v_2 + v_size >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && v_2 >= 1 && v_size >= v_2] 19. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (?,1) && -2 + v_max_3 + v_size >= 0 && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && -1 + v_max_3 >= 0 && -2 + v_max_1 + v_max_3 >= 0 && -2 + v_i_0 + v_max_3 >= 0 && -1*v_i_0 + v_max_3 >= 0 && -4 + v_4 + v_max_3 >= 0 && -3 + v_2 + v_max_3 >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && v_i_0 = v_max_3] 20. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (?,1) && -2 + v_max_3 + v_size >= 0 && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && -1 + v_max_3 >= 0 && -2 + v_max_1 + v_max_3 >= 0 && -2 + v_i_0 + v_max_3 >= 0 && -1*v_i_0 + v_max_3 >= 0 && -4 + v_4 + v_max_3 >= 0 && -3 + v_2 + v_max_3 >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && -1 + v_max_3 >= v_i_0] 21. eval_heapsort_bb4_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-2 + v_size >= 0 (?,1) && -3 + v_i_0 + v_size >= 0 && -1 + -1*v_i_0 + v_size >= 0 && -5 + v_4 + v_size >= 0 && -4 + v_2 + v_size >= 0 && -1*v_2 + v_size >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0] 22. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (?,1) && -3 + v_max_3 + v_size >= 0 && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && -2 + v_max_3 >= 0 && -3 + v_max_1 + v_max_3 >= 0 && -3 + v_i_0 + v_max_3 >= 0 && -1 + -1*v_i_0 + v_max_3 >= 0 && -5 + v_4 + v_max_3 >= 0 && -4 + v_2 + v_max_3 >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && v_i_0 >= 1 && v_size >= v_i_0] 23. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (?,1) && -3 + v_max_3 + v_size >= 0 && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && -2 + v_max_3 >= 0 && -3 + v_max_1 + v_max_3 >= 0 && -3 + v_i_0 + v_max_3 >= 0 && -1 + -1*v_i_0 + v_max_3 >= 0 && -5 + v_4 + v_max_3 >= 0 && -4 + v_2 + v_max_3 >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && -1 + v_i_0 >= v_size] 24. eval_heapsort_14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_15(v_13,v_2,v_4,nondef_0,v_i_0,v_max_1,v_max_3,v_size) [-2 + v_size >= 0 (?,1) && -3 + v_i_0 + v_size >= 0 && -1 + -1*v_i_0 + v_size >= 0 && -5 + v_4 + v_size >= 0 && -4 + v_2 + v_size >= 0 && -1*v_2 + v_size >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0] 25. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_max_3,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (?,1) && -3 + v_max_3 + v_size >= 0 && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -1*v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && -2 + v_max_3 >= 0 && -3 + v_max_1 + v_max_3 >= 0 && -3 + v_i_0 + v_max_3 >= 0 && -1 + -1*v_i_0 + v_max_3 >= 0 && -5 + v_4 + v_max_3 >= 0 && -4 + v_2 + v_max_3 >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && v_max_3 >= 1 && v_size >= v_max_3] 26. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (?,1) && -3 + v_max_3 + v_size >= 0 && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -1*v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && -2 + v_max_3 >= 0 && -3 + v_max_1 + v_max_3 >= 0 && -3 + v_i_0 + v_max_3 >= 0 && -1 + -1*v_i_0 + v_max_3 >= 0 && -5 + v_4 + v_max_3 >= 0 && -4 + v_2 + v_max_3 >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && -1 + v_max_3 >= v_size] 27. eval_heapsort_15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_i_0,v_max_3,v_size) [-2 + v_size >= 0 (?,1) && -3 + v_i_0 + v_size >= 0 && -1 + -1*v_i_0 + v_size >= 0 && -5 + v_4 + v_size >= 0 && -4 + v_2 + v_size >= 0 && -1*v_2 + v_size >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && 0 >= v_8] 28. eval_heapsort_15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_2,v_max_3,v_size) [-2 + v_size >= 0 (?,1) && -3 + v_i_0 + v_size >= 0 && -1 + -1*v_i_0 + v_size >= 0 && -5 + v_4 + v_size >= 0 && -4 + v_2 + v_size >= 0 && -1*v_2 + v_size >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && -1 + v_8 >= 0] 29. eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (?,1) && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && v_size >= v_4] 30. eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb7_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-3 + v_size >= 0 (?,1) && -4 + v_max_1 + v_size >= 0 && -4 + v_i_0 + v_size >= 0 && -2 + -1*v_i_0 + v_size >= 0 && -6 + v_4 + v_size >= 0 && -1*v_4 + v_size >= 0 && -5 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && v_4 >= 1 && v_size >= v_4] 31. eval_heapsort_bb7_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-3 + v_size >= 0 (?,1) && -4 + v_max_1 + v_size >= 0 && -4 + v_i_0 + v_size >= 0 && -2 + -1*v_i_0 + v_size >= 0 && -6 + v_4 + v_size >= 0 && -1*v_4 + v_size >= 0 && -5 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0] 32. eval_heapsort_17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_18(nondef_1,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-3 + v_size >= 0 (?,1) && -4 + v_max_1 + v_size >= 0 && -4 + v_i_0 + v_size >= 0 && -2 + -1*v_i_0 + v_size >= 0 && -6 + v_4 + v_size >= 0 && -1*v_4 + v_size >= 0 && -5 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0] 33. eval_heapsort_18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1,v_size) [-3 + v_size >= 0 (?,1) && -4 + v_max_1 + v_size >= 0 && -4 + v_i_0 + v_size >= 0 && -2 + -1*v_i_0 + v_size >= 0 && -6 + v_4 + v_size >= 0 && -1*v_4 + v_size >= 0 && -5 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && 0 >= v_13] 34. eval_heapsort_18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_4,v_size) [-3 + v_size >= 0 (?,1) && -4 + v_max_1 + v_size >= 0 && -4 + v_i_0 + v_size >= 0 && -2 + -1*v_i_0 + v_size >= 0 && -6 + v_4 + v_size >= 0 && -1*v_4 + v_size >= 0 && -5 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && -1 + v_13 >= 0] Signature: {(eval_heapsort_0,8) ;(eval_heapsort_1,8) ;(eval_heapsort_14,8) ;(eval_heapsort_15,8) ;(eval_heapsort_17,8) ;(eval_heapsort_18,8) ;(eval_heapsort_2,8) ;(eval_heapsort_3,8) ;(eval_heapsort_4,8) ;(eval_heapsort_5,8) ;(eval_heapsort_6,8) ;(eval_heapsort_7,8) ;(eval_heapsort_8,8) ;(eval_heapsort_9,8) ;(eval_heapsort_bb0_in,8) ;(eval_heapsort_bb10_in,8) ;(eval_heapsort_bb11_in,8) ;(eval_heapsort_bb1_in,8) ;(eval_heapsort_bb2_in,8) ;(eval_heapsort_bb3_in,8) ;(eval_heapsort_bb4_in,8) ;(eval_heapsort_bb5_in,8) ;(eval_heapsort_bb6_in,8) ;(eval_heapsort_bb7_in,8) ;(eval_heapsort_bb8_in,8) ;(eval_heapsort_bb9_in,8) ;(eval_heapsort_start,8) ;(eval_heapsort_stop,8)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8},8->{9},9->{10},10->{11},11->{12,13},12->{14} ,13->{15,16},14->{},15->{17,29},16->{18},17->{19,20},18->{21},19->{14},20->{22,23},21->{24},22->{25,26} ,23->{14},24->{27,28},25->{12,13},26->{14},27->{17,29},28->{17,29},29->{30},30->{31},31->{32},32->{33,34} ,33->{19,20},34->{19,20}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths YES + Considered Problem: Rules: 0. eval_heapsort_start(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb0_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 1. eval_heapsort_bb0_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 2. eval_heapsort_0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 3. eval_heapsort_1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 4. eval_heapsort_2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 5. eval_heapsort_3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 6. eval_heapsort_4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 7. eval_heapsort_5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 8. eval_heapsort_6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 9. eval_heapsort_7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 10. eval_heapsort_8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 11. eval_heapsort_9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,1,v_max_1,v_max_3,v_size) True (1,1) 12. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= 0 && 0 >= v_size] (1,1) 13. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= 0 && -1 + v_size >= 0 && v_i_0 >= 1] (?,1) 14. eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_stop(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= 0] (1,1) 15. eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_i_0,v_max_3,v_size) [-1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -1 + v_i_0 >= 0 && -1 + 2*v_i_0 >= v_size] (?,1) 16. eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb3_in(v_13,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -1 + v_i_0 >= 0 && v_size >= 2*v_i_0] (?,1) 17. eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1,v_size) [-1 + v_size >= 0 (?,1) && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && -1 + v_4 >= v_size] 18. eval_heapsort_bb3_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb4_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-2 + v_size >= 0 (?,1) && -3 + v_i_0 + v_size >= 0 && -1 + -1*v_i_0 + v_size >= 0 && -5 + v_4 + v_size >= 0 && -4 + v_2 + v_size >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && v_2 >= 1 && v_size >= v_2] 19. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (1,1) && -2 + v_max_3 + v_size >= 0 && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && -1 + v_max_3 >= 0 && -2 + v_max_1 + v_max_3 >= 0 && -2 + v_i_0 + v_max_3 >= 0 && -1*v_i_0 + v_max_3 >= 0 && -4 + v_4 + v_max_3 >= 0 && -3 + v_2 + v_max_3 >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && v_i_0 = v_max_3] 20. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (?,1) && -2 + v_max_3 + v_size >= 0 && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && -1 + v_max_3 >= 0 && -2 + v_max_1 + v_max_3 >= 0 && -2 + v_i_0 + v_max_3 >= 0 && -1*v_i_0 + v_max_3 >= 0 && -4 + v_4 + v_max_3 >= 0 && -3 + v_2 + v_max_3 >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && -1 + v_max_3 >= v_i_0] 21. eval_heapsort_bb4_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-2 + v_size >= 0 (?,1) && -3 + v_i_0 + v_size >= 0 && -1 + -1*v_i_0 + v_size >= 0 && -5 + v_4 + v_size >= 0 && -4 + v_2 + v_size >= 0 && -1*v_2 + v_size >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0] 22. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (?,1) && -3 + v_max_3 + v_size >= 0 && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && -2 + v_max_3 >= 0 && -3 + v_max_1 + v_max_3 >= 0 && -3 + v_i_0 + v_max_3 >= 0 && -1 + -1*v_i_0 + v_max_3 >= 0 && -5 + v_4 + v_max_3 >= 0 && -4 + v_2 + v_max_3 >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && v_i_0 >= 1 && v_size >= v_i_0] 23. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (1,1) && -3 + v_max_3 + v_size >= 0 && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && -2 + v_max_3 >= 0 && -3 + v_max_1 + v_max_3 >= 0 && -3 + v_i_0 + v_max_3 >= 0 && -1 + -1*v_i_0 + v_max_3 >= 0 && -5 + v_4 + v_max_3 >= 0 && -4 + v_2 + v_max_3 >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && -1 + v_i_0 >= v_size] 24. eval_heapsort_14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_15(v_13,v_2,v_4,nondef_0,v_i_0,v_max_1,v_max_3,v_size) [-2 + v_size >= 0 (?,1) && -3 + v_i_0 + v_size >= 0 && -1 + -1*v_i_0 + v_size >= 0 && -5 + v_4 + v_size >= 0 && -4 + v_2 + v_size >= 0 && -1*v_2 + v_size >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0] 25. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_max_3,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (?,1) && -3 + v_max_3 + v_size >= 0 && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -1*v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && -2 + v_max_3 >= 0 && -3 + v_max_1 + v_max_3 >= 0 && -3 + v_i_0 + v_max_3 >= 0 && -1 + -1*v_i_0 + v_max_3 >= 0 && -5 + v_4 + v_max_3 >= 0 && -4 + v_2 + v_max_3 >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && v_max_3 >= 1 && v_size >= v_max_3] 26. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (1,1) && -3 + v_max_3 + v_size >= 0 && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -1*v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && -2 + v_max_3 >= 0 && -3 + v_max_1 + v_max_3 >= 0 && -3 + v_i_0 + v_max_3 >= 0 && -1 + -1*v_i_0 + v_max_3 >= 0 && -5 + v_4 + v_max_3 >= 0 && -4 + v_2 + v_max_3 >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && -1 + v_max_3 >= v_size] 27. eval_heapsort_15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_i_0,v_max_3,v_size) [-2 + v_size >= 0 (?,1) && -3 + v_i_0 + v_size >= 0 && -1 + -1*v_i_0 + v_size >= 0 && -5 + v_4 + v_size >= 0 && -4 + v_2 + v_size >= 0 && -1*v_2 + v_size >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && 0 >= v_8] 28. eval_heapsort_15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_2,v_max_3,v_size) [-2 + v_size >= 0 (?,1) && -3 + v_i_0 + v_size >= 0 && -1 + -1*v_i_0 + v_size >= 0 && -5 + v_4 + v_size >= 0 && -4 + v_2 + v_size >= 0 && -1*v_2 + v_size >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && -1 + v_8 >= 0] 29. eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (?,1) && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && v_size >= v_4] 30. eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb7_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-3 + v_size >= 0 (?,1) && -4 + v_max_1 + v_size >= 0 && -4 + v_i_0 + v_size >= 0 && -2 + -1*v_i_0 + v_size >= 0 && -6 + v_4 + v_size >= 0 && -1*v_4 + v_size >= 0 && -5 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && v_4 >= 1 && v_size >= v_4] 31. eval_heapsort_bb7_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-3 + v_size >= 0 (?,1) && -4 + v_max_1 + v_size >= 0 && -4 + v_i_0 + v_size >= 0 && -2 + -1*v_i_0 + v_size >= 0 && -6 + v_4 + v_size >= 0 && -1*v_4 + v_size >= 0 && -5 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0] 32. eval_heapsort_17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_18(nondef_1,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-3 + v_size >= 0 (?,1) && -4 + v_max_1 + v_size >= 0 && -4 + v_i_0 + v_size >= 0 && -2 + -1*v_i_0 + v_size >= 0 && -6 + v_4 + v_size >= 0 && -1*v_4 + v_size >= 0 && -5 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0] 33. eval_heapsort_18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1,v_size) [-3 + v_size >= 0 (?,1) && -4 + v_max_1 + v_size >= 0 && -4 + v_i_0 + v_size >= 0 && -2 + -1*v_i_0 + v_size >= 0 && -6 + v_4 + v_size >= 0 && -1*v_4 + v_size >= 0 && -5 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && 0 >= v_13] 34. eval_heapsort_18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_4,v_size) [-3 + v_size >= 0 (?,1) && -4 + v_max_1 + v_size >= 0 && -4 + v_i_0 + v_size >= 0 && -2 + -1*v_i_0 + v_size >= 0 && -6 + v_4 + v_size >= 0 && -1*v_4 + v_size >= 0 && -5 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && -1 + v_13 >= 0] Signature: {(eval_heapsort_0,8) ;(eval_heapsort_1,8) ;(eval_heapsort_14,8) ;(eval_heapsort_15,8) ;(eval_heapsort_17,8) ;(eval_heapsort_18,8) ;(eval_heapsort_2,8) ;(eval_heapsort_3,8) ;(eval_heapsort_4,8) ;(eval_heapsort_5,8) ;(eval_heapsort_6,8) ;(eval_heapsort_7,8) ;(eval_heapsort_8,8) ;(eval_heapsort_9,8) ;(eval_heapsort_bb0_in,8) ;(eval_heapsort_bb10_in,8) ;(eval_heapsort_bb11_in,8) ;(eval_heapsort_bb1_in,8) ;(eval_heapsort_bb2_in,8) ;(eval_heapsort_bb3_in,8) ;(eval_heapsort_bb4_in,8) ;(eval_heapsort_bb5_in,8) ;(eval_heapsort_bb6_in,8) ;(eval_heapsort_bb7_in,8) ;(eval_heapsort_bb8_in,8) ;(eval_heapsort_bb9_in,8) ;(eval_heapsort_start,8) ;(eval_heapsort_stop,8)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8},8->{9},9->{10},10->{11},11->{12,13},12->{14} ,13->{15,16},14->{},15->{17,29},16->{18},17->{19,20},18->{21},19->{14},20->{22,23},21->{24},22->{25,26} ,23->{14},24->{27,28},25->{12,13},26->{14},27->{17,29},28->{17,29},29->{30},30->{31},31->{32},32->{33,34} ,33->{19,20},34->{19,20}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(15,29),(25,12),(34,19)] * Step 3: Looptree YES + Considered Problem: Rules: 0. eval_heapsort_start(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb0_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 1. eval_heapsort_bb0_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 2. eval_heapsort_0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 3. eval_heapsort_1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 4. eval_heapsort_2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 5. eval_heapsort_3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 6. eval_heapsort_4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 7. eval_heapsort_5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 8. eval_heapsort_6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 9. eval_heapsort_7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 10. eval_heapsort_8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 11. eval_heapsort_9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,1,v_max_1,v_max_3,v_size) True (1,1) 12. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= 0 && 0 >= v_size] (1,1) 13. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= 0 && -1 + v_size >= 0 && v_i_0 >= 1] (?,1) 14. eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_stop(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= 0] (1,1) 15. eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_i_0,v_max_3,v_size) [-1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -1 + v_i_0 >= 0 && -1 + 2*v_i_0 >= v_size] (?,1) 16. eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb3_in(v_13,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -1 + v_i_0 >= 0 && v_size >= 2*v_i_0] (?,1) 17. eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1,v_size) [-1 + v_size >= 0 (?,1) && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && -1 + v_4 >= v_size] 18. eval_heapsort_bb3_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb4_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-2 + v_size >= 0 (?,1) && -3 + v_i_0 + v_size >= 0 && -1 + -1*v_i_0 + v_size >= 0 && -5 + v_4 + v_size >= 0 && -4 + v_2 + v_size >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && v_2 >= 1 && v_size >= v_2] 19. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (1,1) && -2 + v_max_3 + v_size >= 0 && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && -1 + v_max_3 >= 0 && -2 + v_max_1 + v_max_3 >= 0 && -2 + v_i_0 + v_max_3 >= 0 && -1*v_i_0 + v_max_3 >= 0 && -4 + v_4 + v_max_3 >= 0 && -3 + v_2 + v_max_3 >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && v_i_0 = v_max_3] 20. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (?,1) && -2 + v_max_3 + v_size >= 0 && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && -1 + v_max_3 >= 0 && -2 + v_max_1 + v_max_3 >= 0 && -2 + v_i_0 + v_max_3 >= 0 && -1*v_i_0 + v_max_3 >= 0 && -4 + v_4 + v_max_3 >= 0 && -3 + v_2 + v_max_3 >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && -1 + v_max_3 >= v_i_0] 21. eval_heapsort_bb4_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-2 + v_size >= 0 (?,1) && -3 + v_i_0 + v_size >= 0 && -1 + -1*v_i_0 + v_size >= 0 && -5 + v_4 + v_size >= 0 && -4 + v_2 + v_size >= 0 && -1*v_2 + v_size >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0] 22. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (?,1) && -3 + v_max_3 + v_size >= 0 && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && -2 + v_max_3 >= 0 && -3 + v_max_1 + v_max_3 >= 0 && -3 + v_i_0 + v_max_3 >= 0 && -1 + -1*v_i_0 + v_max_3 >= 0 && -5 + v_4 + v_max_3 >= 0 && -4 + v_2 + v_max_3 >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && v_i_0 >= 1 && v_size >= v_i_0] 23. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (1,1) && -3 + v_max_3 + v_size >= 0 && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && -2 + v_max_3 >= 0 && -3 + v_max_1 + v_max_3 >= 0 && -3 + v_i_0 + v_max_3 >= 0 && -1 + -1*v_i_0 + v_max_3 >= 0 && -5 + v_4 + v_max_3 >= 0 && -4 + v_2 + v_max_3 >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && -1 + v_i_0 >= v_size] 24. eval_heapsort_14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_15(v_13,v_2,v_4,nondef_0,v_i_0,v_max_1,v_max_3,v_size) [-2 + v_size >= 0 (?,1) && -3 + v_i_0 + v_size >= 0 && -1 + -1*v_i_0 + v_size >= 0 && -5 + v_4 + v_size >= 0 && -4 + v_2 + v_size >= 0 && -1*v_2 + v_size >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0] 25. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_max_3,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (?,1) && -3 + v_max_3 + v_size >= 0 && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -1*v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && -2 + v_max_3 >= 0 && -3 + v_max_1 + v_max_3 >= 0 && -3 + v_i_0 + v_max_3 >= 0 && -1 + -1*v_i_0 + v_max_3 >= 0 && -5 + v_4 + v_max_3 >= 0 && -4 + v_2 + v_max_3 >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && v_max_3 >= 1 && v_size >= v_max_3] 26. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (1,1) && -3 + v_max_3 + v_size >= 0 && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -1*v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && -2 + v_max_3 >= 0 && -3 + v_max_1 + v_max_3 >= 0 && -3 + v_i_0 + v_max_3 >= 0 && -1 + -1*v_i_0 + v_max_3 >= 0 && -5 + v_4 + v_max_3 >= 0 && -4 + v_2 + v_max_3 >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && -1 + v_max_3 >= v_size] 27. eval_heapsort_15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_i_0,v_max_3,v_size) [-2 + v_size >= 0 (?,1) && -3 + v_i_0 + v_size >= 0 && -1 + -1*v_i_0 + v_size >= 0 && -5 + v_4 + v_size >= 0 && -4 + v_2 + v_size >= 0 && -1*v_2 + v_size >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && 0 >= v_8] 28. eval_heapsort_15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_2,v_max_3,v_size) [-2 + v_size >= 0 (?,1) && -3 + v_i_0 + v_size >= 0 && -1 + -1*v_i_0 + v_size >= 0 && -5 + v_4 + v_size >= 0 && -4 + v_2 + v_size >= 0 && -1*v_2 + v_size >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && -1 + v_8 >= 0] 29. eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 (?,1) && -2 + v_max_1 + v_size >= 0 && -2 + v_i_0 + v_size >= 0 && -4 + v_4 + v_size >= 0 && -3 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && v_size >= v_4] 30. eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb7_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-3 + v_size >= 0 (?,1) && -4 + v_max_1 + v_size >= 0 && -4 + v_i_0 + v_size >= 0 && -2 + -1*v_i_0 + v_size >= 0 && -6 + v_4 + v_size >= 0 && -1*v_4 + v_size >= 0 && -5 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && v_4 >= 1 && v_size >= v_4] 31. eval_heapsort_bb7_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-3 + v_size >= 0 (?,1) && -4 + v_max_1 + v_size >= 0 && -4 + v_i_0 + v_size >= 0 && -2 + -1*v_i_0 + v_size >= 0 && -6 + v_4 + v_size >= 0 && -1*v_4 + v_size >= 0 && -5 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0] 32. eval_heapsort_17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_18(nondef_1,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-3 + v_size >= 0 (?,1) && -4 + v_max_1 + v_size >= 0 && -4 + v_i_0 + v_size >= 0 && -2 + -1*v_i_0 + v_size >= 0 && -6 + v_4 + v_size >= 0 && -1*v_4 + v_size >= 0 && -5 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0] 33. eval_heapsort_18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1,v_size) [-3 + v_size >= 0 (?,1) && -4 + v_max_1 + v_size >= 0 && -4 + v_i_0 + v_size >= 0 && -2 + -1*v_i_0 + v_size >= 0 && -6 + v_4 + v_size >= 0 && -1*v_4 + v_size >= 0 && -5 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && 0 >= v_13] 34. eval_heapsort_18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_4,v_size) [-3 + v_size >= 0 (?,1) && -4 + v_max_1 + v_size >= 0 && -4 + v_i_0 + v_size >= 0 && -2 + -1*v_i_0 + v_size >= 0 && -6 + v_4 + v_size >= 0 && -1*v_4 + v_size >= 0 && -5 + v_2 + v_size >= 0 && v_2 + -1*v_max_1 >= 0 && -1 + v_max_1 >= 0 && -2 + v_i_0 + v_max_1 >= 0 && -1*v_i_0 + v_max_1 >= 0 && -4 + v_4 + v_max_1 >= 0 && -3 + v_2 + v_max_1 >= 0 && -2 + v_4 + -1*v_i_0 >= 0 && -1 + v_2 + -1*v_i_0 >= 0 && -1 + v_i_0 >= 0 && -4 + v_4 + v_i_0 >= 0 && -3 + v_2 + v_i_0 >= 0 && -3 + v_4 >= 0 && -5 + v_2 + v_4 >= 0 && -2 + v_2 >= 0 && -1 + v_13 >= 0] Signature: {(eval_heapsort_0,8) ;(eval_heapsort_1,8) ;(eval_heapsort_14,8) ;(eval_heapsort_15,8) ;(eval_heapsort_17,8) ;(eval_heapsort_18,8) ;(eval_heapsort_2,8) ;(eval_heapsort_3,8) ;(eval_heapsort_4,8) ;(eval_heapsort_5,8) ;(eval_heapsort_6,8) ;(eval_heapsort_7,8) ;(eval_heapsort_8,8) ;(eval_heapsort_9,8) ;(eval_heapsort_bb0_in,8) ;(eval_heapsort_bb10_in,8) ;(eval_heapsort_bb11_in,8) ;(eval_heapsort_bb1_in,8) ;(eval_heapsort_bb2_in,8) ;(eval_heapsort_bb3_in,8) ;(eval_heapsort_bb4_in,8) ;(eval_heapsort_bb5_in,8) ;(eval_heapsort_bb6_in,8) ;(eval_heapsort_bb7_in,8) ;(eval_heapsort_bb8_in,8) ;(eval_heapsort_bb9_in,8) ;(eval_heapsort_start,8) ;(eval_heapsort_stop,8)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8},8->{9},9->{10},10->{11},11->{12,13},12->{14} ,13->{15,16},14->{},15->{17},16->{18},17->{19,20},18->{21},19->{14},20->{22,23},21->{24},22->{25,26} ,23->{14},24->{27,28},25->{13},26->{14},27->{17,29},28->{17,29},29->{30},30->{31},31->{32},32->{33,34} ,33->{19,20},34->{20}] + Applied Processor: Looptree + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34] | `- p:[13,25,22,20,17,15,27,24,21,18,16,28,33,32,31,30,29,34] c: [34] | `- p:[13,25,22,20,17,15,27,24,21,18,16,28,33,32,31,30,29] c: [33] | `- p:[13,25,22,20,17,15,27,24,21,18,16,28] c: [28] | `- p:[13,25,22,20,17,15,27,24,21,18,16] c: [27] | `- p:[13,25,22,20,17,15] c: [25] YES