NO * Step 1: UnsatPaths NO + 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: UnreachableRules NO + 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: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [14,18,27] * Step 3: FromIts NO + 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) 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) 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) 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},15->{17,19},16->{25},17->{42},19->{20},20->{21},21->{22,23},22->{24,25},23->{24,25},24->{26,28} ,25->{33,34,35},26->{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 4: CloseWith NO + 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_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_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_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},15->{17,19},16->{25},17->{42},19->{20},20->{21},21->{22,23},22->{24,25},23->{24,25},24->{26,28} ,25->{33,34,35},26->{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: CloseWith False + Details: () NO