MAYBE * Step 1: UnsatPaths MAYBE + 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_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 && v_i_0 >= 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_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_size] (?,1) 14. 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) [0 >= v_i_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_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) [v_size >= 2*v_i_0] (?,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_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 + 2*v_i_0 >= v_size] (?,1) 17. 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_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_2] (?,1) 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_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_2 >= v_size] (?,1) 19. 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) [v_2 >= 1 && v_size >= v_2] (?,1) 20. 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) True (?,1) 21. 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) True (?,1) 22. 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) [-1 + v_8 >= 0] (?,1) 23. 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) [0 >= v_8] (?,1) 24. 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) [v_size >= v_4] (?,1) 25. 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_4 >= v_size] (?,1) 26. 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_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_4] (?,1) 27. 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_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_4 >= v_size] (?,1) 28. 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) [v_4 >= 1 && v_size >= v_4] (?,1) 29. 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) True (?,1) 30. 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) True (?,1) 31. 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) [-1 + v_13 >= 0] (?,1) 32. 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) [0 >= v_13] (?,1) 33. 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_max_3 >= v_i_0] (?,1) 34. 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_i_0 >= v_max_3] (?,1) 35. 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) [v_i_0 = v_max_3] (?,1) 36. 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) [0 >= v_i_0] (?,1) 37. 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_i_0 >= v_size] (?,1) 38. 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) [v_i_0 >= 1 && v_size >= v_i_0] (?,1) 39. 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) [0 >= v_max_3] (?,1) 40. 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_max_3 >= v_size] (?,1) 41. 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) [v_max_3 >= 1 && v_size >= v_max_3] (?,1) 42. 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) True (?,1) 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,14},12->{15 ,16},13->{42},14->{42},15->{17,18,19},16->{24,25},17->{42},18->{42},19->{20},20->{21},21->{22,23},22->{24 ,25},23->{24,25},24->{26,27,28},25->{33,34,35},26->{42},27->{42},28->{29},29->{30},30->{31,32},31->{33,34 ,35},32->{33,34,35},33->{36,37,38},34->{36,37,38},35->{42},36->{42},37->{42},38->{39,40,41},39->{42} ,40->{42},41->{12,13,14},42->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(11,14),(15,18),(16,24),(24,27),(41,13),(41,14)] * Step 2: FromIts MAYBE + 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_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 && v_i_0 >= 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_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_size] (?,1) 14. 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) [0 >= v_i_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_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) [v_size >= 2*v_i_0] (?,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_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 + 2*v_i_0 >= v_size] (?,1) 17. 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_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_2] (?,1) 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_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_2 >= v_size] (?,1) 19. 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) [v_2 >= 1 && v_size >= v_2] (?,1) 20. 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) True (?,1) 21. 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) True (?,1) 22. 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) [-1 + v_8 >= 0] (?,1) 23. 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) [0 >= v_8] (?,1) 24. 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) [v_size >= v_4] (?,1) 25. 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_4 >= v_size] (?,1) 26. 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_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_4] (?,1) 27. 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_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_4 >= v_size] (?,1) 28. 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) [v_4 >= 1 && v_size >= v_4] (?,1) 29. 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) True (?,1) 30. 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) True (?,1) 31. 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) [-1 + v_13 >= 0] (?,1) 32. 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) [0 >= v_13] (?,1) 33. 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_max_3 >= v_i_0] (?,1) 34. 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_i_0 >= v_max_3] (?,1) 35. 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) [v_i_0 = v_max_3] (?,1) 36. 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) [0 >= v_i_0] (?,1) 37. 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_i_0 >= v_size] (?,1) 38. 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) [v_i_0 >= 1 && v_size >= v_i_0] (?,1) 39. 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) [0 >= v_max_3] (?,1) 40. 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_max_3 >= v_size] (?,1) 41. 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) [v_max_3 >= 1 && v_size >= v_max_3] (?,1) 42. 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) True (?,1) 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->{15,16} ,13->{42},14->{42},15->{17,19},16->{25},17->{42},18->{42},19->{20},20->{21},21->{22,23},22->{24,25},23->{24 ,25},24->{26,28},25->{33,34,35},26->{42},27->{42},28->{29},29->{30},30->{31,32},31->{33,34,35},32->{33,34 ,35},33->{36,37,38},34->{36,37,38},35->{42},36->{42},37->{42},38->{39,40,41},39->{42},40->{42},41->{12} ,42->{}] + Applied Processor: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: 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 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 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 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 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 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 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 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 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 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 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 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 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_size >= 0 && v_i_0 >= 1] 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) [0 >= v_size] 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) [0 >= v_i_0] 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) [v_size >= 2*v_i_0] 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 + 2*v_i_0 >= v_size] 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_bb11_in(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [0 >= v_2] 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_bb11_in(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_2 >= v_size] 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) [v_2 >= 1 && v_size >= v_2] 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) True 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) True 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) [-1 + v_8 >= 0] 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) [0 >= v_8] 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) [v_size >= v_4] 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_4 >= 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) -> eval_heapsort_bb11_in(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [0 >= v_4] 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_bb11_in(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_4 >= 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) -> eval_heapsort_bb7_in(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_4 >= 1 && v_size >= v_4] 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) True 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) True 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) [-1 + v_13 >= 0] 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) [0 >= v_13] 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_max_3 >= v_i_0] 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_i_0 >= v_max_3] 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) [v_i_0 = v_max_3] 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) [0 >= v_i_0] 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_i_0 >= 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) -> eval_heapsort_bb10_in(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_i_0 >= 1 && v_size >= v_i_0] 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) [0 >= v_max_3] 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_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) -> eval_heapsort_bb1_in(v_13,v_2,v_4 ,v_8,v_max_3,v_max_1,v_max_3 ,v_size) [v_max_3 >= 1 && v_size >= v_max_3] 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) True 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)} Rule 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->{15,16} ,13->{42},14->{42},15->{17,19},16->{25},17->{42},18->{42},19->{20},20->{21},21->{22,23},22->{24,25},23->{24 ,25},24->{26,28},25->{33,34,35},26->{42},27->{42},28->{29},29->{30},30->{31,32},31->{33,34,35},32->{33,34 ,35},33->{36,37,38},34->{36,37,38},35->{42},36->{42},37->{42},38->{39,40,41},39->{42},40->{42},41->{12} ,42->{}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: eval_heapsort_start.0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb0_in.1(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_bb0_in.1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_0.2(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_0.2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_1.3(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_1.3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_2.4(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_2.4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_3.5(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_3.5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_4.6(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_4.6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_5.7(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_5.7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_6.8(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_6.8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_7.9(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_7.9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_8.10(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_8.10(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_9.11(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_9.11(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in.12(v_13 ,v_2,v_4,v_8,1,v_max_1,v_max_3 ,v_size) True eval_heapsort_9.11(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in.13(v_13 ,v_2,v_4,v_8,1,v_max_1,v_max_3 ,v_size) True eval_heapsort_bb1_in.12(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb2_in.15(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_size >= 0 && v_i_0 >= 1] eval_heapsort_bb1_in.12(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb2_in.16(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_size >= 0 && v_i_0 >= 1] eval_heapsort_bb1_in.13(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [0 >= v_size] eval_heapsort_bb1_in.14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [0 >= v_i_0] eval_heapsort_bb2_in.15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb3_in.17(v_13 ,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_size >= 2*v_i_0] eval_heapsort_bb2_in.15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb3_in.19(v_13 ,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_size >= 2*v_i_0] eval_heapsort_bb2_in.16(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in.25(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 + 2*v_i_0 >= v_size] eval_heapsort_bb3_in.17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [0 >= v_2] eval_heapsort_bb3_in.18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_2 >= v_size] eval_heapsort_bb3_in.19(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb4_in.20(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_2 >= 1 && v_size >= v_2] eval_heapsort_bb4_in.20(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_14.21(v_13,v_2 ,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_14.21(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_15.22(v_13,v_2 ,v_4,nondef_0,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_14.21(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_15.23(v_13,v_2 ,v_4,nondef_0,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_15.22(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in.24(v_13 ,v_2,v_4,v_8,v_i_0,v_2,v_max_3 ,v_size) [-1 + v_8 >= 0] eval_heapsort_15.22(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in.25(v_13 ,v_2,v_4,v_8,v_i_0,v_2,v_max_3 ,v_size) [-1 + v_8 >= 0] eval_heapsort_15.23(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in.24(v_13 ,v_2,v_4,v_8,v_i_0,v_i_0,v_max_3 ,v_size) [0 >= v_8] eval_heapsort_15.23(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in.25(v_13 ,v_2,v_4,v_8,v_i_0,v_i_0,v_max_3 ,v_size) [0 >= v_8] eval_heapsort_bb5_in.24(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb6_in.26(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_size >= v_4] eval_heapsort_bb5_in.24(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb6_in.28(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_size >= v_4] eval_heapsort_bb5_in.25(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in.33(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1 ,v_size) [-1 + v_4 >= v_size] eval_heapsort_bb5_in.25(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in.34(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1 ,v_size) [-1 + v_4 >= v_size] eval_heapsort_bb5_in.25(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in.35(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1 ,v_size) [-1 + v_4 >= v_size] eval_heapsort_bb6_in.26(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [0 >= v_4] eval_heapsort_bb6_in.27(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_4 >= v_size] eval_heapsort_bb6_in.28(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb7_in.29(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_4 >= 1 && v_size >= v_4] eval_heapsort_bb7_in.29(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_17.30(v_13,v_2 ,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_17.30(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_18.31(nondef_1 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_17.30(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_18.32(nondef_1 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_18.31(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in.33(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_4 ,v_size) [-1 + v_13 >= 0] eval_heapsort_18.31(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in.34(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_4 ,v_size) [-1 + v_13 >= 0] eval_heapsort_18.31(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in.35(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_4 ,v_size) [-1 + v_13 >= 0] eval_heapsort_18.32(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in.33(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1 ,v_size) [0 >= v_13] eval_heapsort_18.32(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in.34(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1 ,v_size) [0 >= v_13] eval_heapsort_18.32(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in.35(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1 ,v_size) [0 >= v_13] eval_heapsort_bb8_in.33(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in.36(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_max_3 >= v_i_0] eval_heapsort_bb8_in.33(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in.37(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_max_3 >= v_i_0] eval_heapsort_bb8_in.33(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in.38(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_max_3 >= v_i_0] eval_heapsort_bb8_in.34(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in.36(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_i_0 >= v_max_3] eval_heapsort_bb8_in.34(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in.37(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_i_0 >= v_max_3] eval_heapsort_bb8_in.34(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in.38(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_i_0 >= v_max_3] eval_heapsort_bb8_in.35(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_i_0 = v_max_3] eval_heapsort_bb9_in.36(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [0 >= v_i_0] eval_heapsort_bb9_in.37(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_i_0 >= v_size] eval_heapsort_bb9_in.38(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb10_in.39(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_i_0 >= 1 && v_size >= v_i_0] eval_heapsort_bb9_in.38(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb10_in.40(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_i_0 >= 1 && v_size >= v_i_0] eval_heapsort_bb9_in.38(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb10_in.41(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_i_0 >= 1 && v_size >= v_i_0] eval_heapsort_bb10_in.39(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [0 >= v_max_3] eval_heapsort_bb10_in.40(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_max_3 >= v_size] eval_heapsort_bb10_in.41(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in.12(v_13 ,v_2,v_4,v_8,v_max_3,v_max_1,v_max_3 ,v_size) [v_max_3 >= 1 && v_size >= v_max_3] eval_heapsort_bb11_in.42(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_stop.43(v_13,v_2 ,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True Signature: {(eval_heapsort_0.2,8) ;(eval_heapsort_1.3,8) ;(eval_heapsort_14.21,8) ;(eval_heapsort_15.22,8) ;(eval_heapsort_15.23,8) ;(eval_heapsort_17.30,8) ;(eval_heapsort_18.31,8) ;(eval_heapsort_18.32,8) ;(eval_heapsort_2.4,8) ;(eval_heapsort_3.5,8) ;(eval_heapsort_4.6,8) ;(eval_heapsort_5.7,8) ;(eval_heapsort_6.8,8) ;(eval_heapsort_7.9,8) ;(eval_heapsort_8.10,8) ;(eval_heapsort_9.11,8) ;(eval_heapsort_bb0_in.1,8) ;(eval_heapsort_bb10_in.39,8) ;(eval_heapsort_bb10_in.40,8) ;(eval_heapsort_bb10_in.41,8) ;(eval_heapsort_bb11_in.42,8) ;(eval_heapsort_bb1_in.12,8) ;(eval_heapsort_bb1_in.13,8) ;(eval_heapsort_bb1_in.14,8) ;(eval_heapsort_bb2_in.15,8) ;(eval_heapsort_bb2_in.16,8) ;(eval_heapsort_bb3_in.17,8) ;(eval_heapsort_bb3_in.18,8) ;(eval_heapsort_bb3_in.19,8) ;(eval_heapsort_bb4_in.20,8) ;(eval_heapsort_bb5_in.24,8) ;(eval_heapsort_bb5_in.25,8) ;(eval_heapsort_bb6_in.26,8) ;(eval_heapsort_bb6_in.27,8) ;(eval_heapsort_bb6_in.28,8) ;(eval_heapsort_bb7_in.29,8) ;(eval_heapsort_bb8_in.33,8) ;(eval_heapsort_bb8_in.34,8) ;(eval_heapsort_bb8_in.35,8) ;(eval_heapsort_bb9_in.36,8) ;(eval_heapsort_bb9_in.37,8) ;(eval_heapsort_bb9_in.38,8) ;(eval_heapsort_start.0,8) ;(eval_heapsort_stop.43,8)} Rule Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8},8->{9},9->{10},10->{11,12},11->{13,14},12->{15} ,13->{17,18},14->{19},15->{62},16->{62},17->{20},18->{22},19->{32,33,34},20->{62},21->{62},22->{23},23->{24 ,25},24->{26,27},25->{28,29},26->{30,31},27->{32,33,34},28->{30,31},29->{32,33,34},30->{35},31->{37},32->{47 ,48,49},33->{50,51,52},34->{53},35->{62},36->{62},37->{38},38->{39,40},39->{41,42,43},40->{44,45,46},41->{47 ,48,49},42->{50,51,52},43->{53},44->{47,48,49},45->{50,51,52},46->{53},47->{54},48->{55},49->{56,57,58} ,50->{54},51->{55},52->{56,57,58},53->{62},54->{62},55->{62},56->{59},57->{60},58->{61},59->{62},60->{62} ,61->{13,14},62->{}] + Applied Processor: AddSinks + Details: () * Step 5: Failure MAYBE + Considered Problem: Rules: eval_heapsort_start.0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb0_in.1(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_bb0_in.1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_0.2(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_0.2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_1.3(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_1.3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_2.4(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_2.4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_3.5(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_3.5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_4.6(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_4.6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_5.7(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_5.7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_6.8(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_6.8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_7.9(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_7.9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_8.10(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_8.10(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_9.11(v_13,v_2,v_4 ,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_9.11(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in.12(v_13 ,v_2,v_4,v_8,1,v_max_1,v_max_3 ,v_size) True eval_heapsort_9.11(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in.13(v_13 ,v_2,v_4,v_8,1,v_max_1,v_max_3 ,v_size) True eval_heapsort_bb1_in.12(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb2_in.15(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_size >= 0 && v_i_0 >= 1] eval_heapsort_bb1_in.12(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb2_in.16(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_size >= 0 && v_i_0 >= 1] eval_heapsort_bb1_in.13(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [0 >= v_size] eval_heapsort_bb1_in.14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [0 >= v_i_0] eval_heapsort_bb2_in.15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb3_in.17(v_13 ,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_size >= 2*v_i_0] eval_heapsort_bb2_in.15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb3_in.19(v_13 ,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_size >= 2*v_i_0] eval_heapsort_bb2_in.16(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in.25(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 + 2*v_i_0 >= v_size] eval_heapsort_bb3_in.17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [0 >= v_2] eval_heapsort_bb3_in.18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_2 >= v_size] eval_heapsort_bb3_in.19(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb4_in.20(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_2 >= 1 && v_size >= v_2] eval_heapsort_bb4_in.20(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_14.21(v_13,v_2 ,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_14.21(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_15.22(v_13,v_2 ,v_4,nondef_0,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_14.21(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_15.23(v_13,v_2 ,v_4,nondef_0,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_15.22(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in.24(v_13 ,v_2,v_4,v_8,v_i_0,v_2,v_max_3 ,v_size) [-1 + v_8 >= 0] eval_heapsort_15.22(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in.25(v_13 ,v_2,v_4,v_8,v_i_0,v_2,v_max_3 ,v_size) [-1 + v_8 >= 0] eval_heapsort_15.23(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in.24(v_13 ,v_2,v_4,v_8,v_i_0,v_i_0,v_max_3 ,v_size) [0 >= v_8] eval_heapsort_15.23(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in.25(v_13 ,v_2,v_4,v_8,v_i_0,v_i_0,v_max_3 ,v_size) [0 >= v_8] eval_heapsort_bb5_in.24(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb6_in.26(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_size >= v_4] eval_heapsort_bb5_in.24(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb6_in.28(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_size >= v_4] eval_heapsort_bb5_in.25(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in.33(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1 ,v_size) [-1 + v_4 >= v_size] eval_heapsort_bb5_in.25(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in.34(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1 ,v_size) [-1 + v_4 >= v_size] eval_heapsort_bb5_in.25(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in.35(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1 ,v_size) [-1 + v_4 >= v_size] eval_heapsort_bb6_in.26(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [0 >= v_4] eval_heapsort_bb6_in.27(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_4 >= v_size] eval_heapsort_bb6_in.28(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb7_in.29(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_4 >= 1 && v_size >= v_4] eval_heapsort_bb7_in.29(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_17.30(v_13,v_2 ,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_17.30(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_18.31(nondef_1 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_17.30(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_18.32(nondef_1 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_18.31(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in.33(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_4 ,v_size) [-1 + v_13 >= 0] eval_heapsort_18.31(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in.34(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_4 ,v_size) [-1 + v_13 >= 0] eval_heapsort_18.31(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in.35(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_4 ,v_size) [-1 + v_13 >= 0] eval_heapsort_18.32(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in.33(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1 ,v_size) [0 >= v_13] eval_heapsort_18.32(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in.34(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1 ,v_size) [0 >= v_13] eval_heapsort_18.32(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in.35(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1 ,v_size) [0 >= v_13] eval_heapsort_bb8_in.33(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in.36(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_max_3 >= v_i_0] eval_heapsort_bb8_in.33(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in.37(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_max_3 >= v_i_0] eval_heapsort_bb8_in.33(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in.38(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_max_3 >= v_i_0] eval_heapsort_bb8_in.34(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in.36(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_i_0 >= v_max_3] eval_heapsort_bb8_in.34(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in.37(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_i_0 >= v_max_3] eval_heapsort_bb8_in.34(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in.38(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_i_0 >= v_max_3] eval_heapsort_bb8_in.35(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_i_0 = v_max_3] eval_heapsort_bb9_in.36(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [0 >= v_i_0] eval_heapsort_bb9_in.37(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_i_0 >= v_size] eval_heapsort_bb9_in.38(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb10_in.39(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_i_0 >= 1 && v_size >= v_i_0] eval_heapsort_bb9_in.38(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb10_in.40(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_i_0 >= 1 && v_size >= v_i_0] eval_heapsort_bb9_in.38(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb10_in.41(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [v_i_0 >= 1 && v_size >= v_i_0] eval_heapsort_bb10_in.39(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [0 >= v_max_3] eval_heapsort_bb10_in.40(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in.42(v_13 ,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) [-1 + v_max_3 >= v_size] eval_heapsort_bb10_in.41(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in.12(v_13 ,v_2,v_4,v_8,v_max_3,v_max_1,v_max_3 ,v_size) [v_max_3 >= 1 && v_size >= v_max_3] eval_heapsort_bb11_in.42(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_stop.43(v_13,v_2 ,v_4,v_8,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_stop.43(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> exitus616(v_13,v_2,v_4,v_8 ,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_stop.43(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> exitus616(v_13,v_2,v_4,v_8 ,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_stop.43(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> exitus616(v_13,v_2,v_4,v_8 ,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_stop.43(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> exitus616(v_13,v_2,v_4,v_8 ,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_stop.43(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> exitus616(v_13,v_2,v_4,v_8 ,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_stop.43(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> exitus616(v_13,v_2,v_4,v_8 ,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_stop.43(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> exitus616(v_13,v_2,v_4,v_8 ,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_stop.43(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> exitus616(v_13,v_2,v_4,v_8 ,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_stop.43(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> exitus616(v_13,v_2,v_4,v_8 ,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_stop.43(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> exitus616(v_13,v_2,v_4,v_8 ,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_stop.43(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> exitus616(v_13,v_2,v_4,v_8 ,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_stop.43(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> exitus616(v_13,v_2,v_4,v_8 ,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_stop.43(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> exitus616(v_13,v_2,v_4,v_8 ,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_stop.43(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> exitus616(v_13,v_2,v_4,v_8 ,v_i_0,v_max_1,v_max_3 ,v_size) True eval_heapsort_stop.43(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> exitus616(v_13,v_2,v_4,v_8 ,v_i_0,v_max_1,v_max_3 ,v_size) True Signature: {(eval_heapsort_0.2,8) ;(eval_heapsort_1.3,8) ;(eval_heapsort_14.21,8) ;(eval_heapsort_15.22,8) ;(eval_heapsort_15.23,8) ;(eval_heapsort_17.30,8) ;(eval_heapsort_18.31,8) ;(eval_heapsort_18.32,8) ;(eval_heapsort_2.4,8) ;(eval_heapsort_3.5,8) ;(eval_heapsort_4.6,8) ;(eval_heapsort_5.7,8) ;(eval_heapsort_6.8,8) ;(eval_heapsort_7.9,8) ;(eval_heapsort_8.10,8) ;(eval_heapsort_9.11,8) ;(eval_heapsort_bb0_in.1,8) ;(eval_heapsort_bb10_in.39,8) ;(eval_heapsort_bb10_in.40,8) ;(eval_heapsort_bb10_in.41,8) ;(eval_heapsort_bb11_in.42,8) ;(eval_heapsort_bb1_in.12,8) ;(eval_heapsort_bb1_in.13,8) ;(eval_heapsort_bb1_in.14,8) ;(eval_heapsort_bb2_in.15,8) ;(eval_heapsort_bb2_in.16,8) ;(eval_heapsort_bb3_in.17,8) ;(eval_heapsort_bb3_in.18,8) ;(eval_heapsort_bb3_in.19,8) ;(eval_heapsort_bb4_in.20,8) ;(eval_heapsort_bb5_in.24,8) ;(eval_heapsort_bb5_in.25,8) ;(eval_heapsort_bb6_in.26,8) ;(eval_heapsort_bb6_in.27,8) ;(eval_heapsort_bb6_in.28,8) ;(eval_heapsort_bb7_in.29,8) ;(eval_heapsort_bb8_in.33,8) ;(eval_heapsort_bb8_in.34,8) ;(eval_heapsort_bb8_in.35,8) ;(eval_heapsort_bb9_in.36,8) ;(eval_heapsort_bb9_in.37,8) ;(eval_heapsort_bb9_in.38,8) ;(eval_heapsort_start.0,8) ;(eval_heapsort_stop.43,8) ;(exitus616,8)} Rule Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8},8->{9},9->{10},10->{11,12},11->{13,14},12->{15} ,13->{17,18},14->{19},15->{62},16->{62},17->{20},18->{22},19->{32,33,34},20->{62},21->{62},22->{23},23->{24 ,25},24->{26,27},25->{28,29},26->{30,31},27->{32,33,34},28->{30,31},29->{32,33,34},30->{35},31->{37},32->{47 ,48,49},33->{50,51,52},34->{53},35->{62},36->{62},37->{38},38->{39,40},39->{41,42,43},40->{44,45,46},41->{47 ,48,49},42->{50,51,52},43->{53},44->{47,48,49},45->{50,51,52},46->{53},47->{54},48->{55},49->{56,57,58} ,50->{54},51->{55},52->{56,57,58},53->{62},54->{62},55->{62},56->{59},57->{60},58->{61},59->{62},60->{62} ,61->{13,14},62->{63,64,65,66,67,68,69,70,71,72,73,74,75,76,77}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77] | `- p:[13,61,58,49,32,19,14,27,24,23,22,18,29,25,41,39,38,37,31,26,28,44,40,52,33,42,45] c: [] MAYBE