YES(?,PRIMREC) * Step 1: UnsatRules MAYBE + Considered Problem: Rules: 0. evalrealheapsortstep1start(A,B,C) -> evalrealheapsortstep1entryin(A,B,C) True (1,1) 1. evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1bb6in(A,1,C) [A >= 3] (?,1) 2. evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [2 >= A] (?,1) 3. evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,B) [A >= 1 + B] (?,1) 4. evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [B >= A] (?,1) 5. evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [0 >= C] (?,1) 6. evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb4in(A,B,C) [C >= 1] (?,1) 7. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb2in(A,B,C) [1 + C = 0] (?,1) 8. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb2in(A,B,C) [C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] (?,1) 9. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb2in(A,B,C) [0 >= 2 + C && 0 >= D && 2*D >= 1 + C && 2 + C >= 2*D] (?,1) 10. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [1 + C = 0] (?,1) 11. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] (?,1) 12. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [0 >= 2 + C && 0 >= D && 2*D >= 1 + C && 2 + C >= 2*D] (?,1) 13. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1) [1 + C = 0] (?,1) 14. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [0 >= 1 && D >= 0 && 0 >= 2*D && 1 + 2*D >= 0 && 1 + C = 0] (?,1) 15. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [0 >= 1 && 0 >= D && 1 + C = 0 && 2*D >= 1 + C && 2 + C >= 2*D] (?,1) 16. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1) [0 >= 1 && D >= 0 && 0 >= 2*D && 1 + 2*D >= 0 && 1 + C = 0] (?,1) 17. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [0 >= 1 && E >= 0 && 0 >= 2*E && 1 + 2*E >= 0 && D >= 0 && 0 >= 2*D && 1 + 2*D >= 0 && 1 + C = 0] (?,1) 18. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [0 >= 1 && E >= 0 && 0 >= 2*E && 1 + 2*E >= 0 && 0 >= D && 1 + C = 0 && 2*D >= 1 + C && 2 + C >= 2*D] (?,1) 19. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1) [0 >= 1 && 0 >= D && 1 + C = 0 && 2*D >= 1 + C && 2 + C >= 2*D] (?,1) 20. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [0 >= 1 && 0 >= E && D >= 0 && 0 >= 2*D && 1 + 2*D >= 0 && 1 + C = 0 && 2*E >= 1 + C && 2 + C >= 2*E] (?,1) 21. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [0 >= 1 && 0 >= E && 0 >= D && 1 + C = 0 && 2*E >= 1 + C && 2 + C >= 2*E && 2*D >= 1 + C && 2 + C >= 2*D] (?,1) 22. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1) [0 >= 1 && D >= 0 && 0 >= 2*D && 1 + 2*D >= 0 && 1 + C = 0] (?,1) 23. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [0 >= 1 && E >= 0 && 0 >= 2*E && 1 + 2*E >= 0 && D >= 0 && 0 >= 2*D && 1 + 2*D >= 0 && 1 + C = 0] (?,1) 24. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [0 >= 1 && E >= 0 && 0 >= 2*E && 1 + 2*E >= 0 && 0 >= D && 1 + C = 0 && 2*D >= 1 + C && 2 + C >= 2*D] (?,1) 25. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1) [0 >= 1 && D >= 0 && 0 >= 2*D && 1 + 2*D >= 0 && E >= 0 && 0 >= 2*E && 1 + 2*E >= 0 && 1 + C = 0] (?,1) 26. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [C >= 0 (?,1) && E >= 0 && 1 + C >= 2*E && 2*E >= C && F >= 0 && 1 + C >= 2*F && 2*F >= C && D >= 0 && 1 + C >= 2*D && 2*D >= C] 27. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [C >= 0 (?,1) && E >= 0 && 1 + C >= 2*E && 2*E >= C && F >= 0 && 1 + C >= 2*F && 2*F >= C && 0 >= 2 + C && 0 >= D && 2*D >= 1 + C && 2 + C >= 2*D] 28. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1) [0 >= 1 && D >= 0 && 0 >= 2*D && 1 + 2*D >= 0 && 0 >= E && 1 + C = 0 && 2*E >= 1 + C && 2 + C >= 2*E] (?,1) 29. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [C >= 0 (?,1) && E >= 0 && 1 + C >= 2*E && 2*E >= C && 0 >= 2 + C && 0 >= F && D >= 0 && 1 + C >= 2*D && 2*D >= C && 2*F >= 1 + C && 2 + C >= 2*F] 30. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [C >= 0 (?,1) && E >= 0 && 1 + C >= 2*E && 2*E >= C && 0 >= 2 + C && 0 >= F && 0 >= D && 2*F >= 1 + C && 2 + C >= 2*F && 2*D >= 1 + C && 2 + C >= 2*D] 31. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1) [0 >= 1 && 0 >= D && 1 + C = 0 && 2*D >= 1 + C && 2 + C >= 2*D] (?,1) 32. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [0 >= 1 && 0 >= E && D >= 0 && 0 >= 2*D && 1 + 2*D >= 0 && 1 + C = 0 && 2*E >= 1 + C && 2 + C >= 2*E] (?,1) 33. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [0 >= 1 && 0 >= E && 0 >= D && 1 + C = 0 && 2*E >= 1 + C && 2 + C >= 2*E && 2*D >= 1 + C && 2 + C >= 2*D] (?,1) 34. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1) [0 >= 1 && 0 >= D && E >= 0 && 0 >= 2*E && 1 + 2*E >= 0 && 1 + C = 0 && 2*D >= 1 + C && 2 + C >= 2*D] (?,1) 35. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [0 >= 2 + C (?,1) && 0 >= E && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && D >= 0 && 1 + C >= 2*D && 2*D >= C && 2*E >= 1 + C && 2 + C >= 2*E] 36. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [0 >= 2 + C (?,1) && 0 >= E && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && 0 >= D && 2*E >= 1 + C && 2 + C >= 2*E && 2*D >= 1 + C && 2 + C >= 2*D] 37. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1) [0 >= 1 && 0 >= D && 0 >= E && 1 + C = 0 && 2*D >= 1 + C && 2 + C >= 2*D && 2*E >= 1 + C && 2 + C >= 2*E] (?,1) 38. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [0 >= 2 + C (?,1) && 0 >= E && 0 >= F && C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C && 2*E >= 1 + C && 2 + C >= 2*E && 2*F >= 1 + C && 2 + C >= 2*F] 39. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [0 >= 2 + C (?,1) && 0 >= E && 0 >= F && 0 >= D && 2*E >= 1 + C && 2 + C >= 2*E && 2*F >= 1 + C && 2 + C >= 2*F && 2*D >= 1 + C && 2 + C >= 2*D] 40. evalrealheapsortstep1bb5in(A,B,C) -> evalrealheapsortstep1bb6in(A,1 + B,C) True (?,1) 41. evalrealheapsortstep1returnin(A,B,C) -> evalrealheapsortstep1stop(A,B,C) True (?,1) Signature: {(evalrealheapsortstep1bb2in,3) ;(evalrealheapsortstep1bb3in,3) ;(evalrealheapsortstep1bb4in,3) ;(evalrealheapsortstep1bb5in,3) ;(evalrealheapsortstep1bb6in,3) ;(evalrealheapsortstep1entryin,3) ;(evalrealheapsortstep1returnin,3) ;(evalrealheapsortstep1start,3) ;(evalrealheapsortstep1stop,3)} Flow Graph: [0->{1,2},1->{3,4},2->{41},3->{5,6},4->{41},5->{40},6->{7,8,9,10,11,12},7->{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},8->{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},9->{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},10->{40},11->{40},12->{40},13->{5,6},14->{5,6},15->{5,6},16->{5,6},17->{5,6},18->{5,6},19->{5,6} ,20->{5,6},21->{5,6},22->{5,6},23->{5,6},24->{5,6},25->{5,6},26->{5,6},27->{5,6},28->{5,6},29->{5,6},30->{5 ,6},31->{5,6},32->{5,6},33->{5,6},34->{5,6},35->{5,6},36->{5,6},37->{5,6},38->{5,6},39->{5,6},40->{3,4} ,41->{}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [14 ,15 ,16 ,17 ,18 ,19 ,20 ,21 ,22 ,23 ,24 ,25 ,27 ,28 ,29 ,30 ,31 ,32 ,33 ,34 ,35 ,36 ,37 ,38] * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. evalrealheapsortstep1start(A,B,C) -> evalrealheapsortstep1entryin(A,B,C) True (1,1) 1. evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1bb6in(A,1,C) [A >= 3] (?,1) 2. evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [2 >= A] (?,1) 3. evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,B) [A >= 1 + B] (?,1) 4. evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [B >= A] (?,1) 5. evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [0 >= C] (?,1) 6. evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb4in(A,B,C) [C >= 1] (?,1) 7. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb2in(A,B,C) [1 + C = 0] (?,1) 8. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb2in(A,B,C) [C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] (?,1) 9. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb2in(A,B,C) [0 >= 2 + C && 0 >= D && 2*D >= 1 + C && 2 + C >= 2*D] (?,1) 10. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [1 + C = 0] (?,1) 11. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] (?,1) 12. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [0 >= 2 + C && 0 >= D && 2*D >= 1 + C && 2 + C >= 2*D] (?,1) 13. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1) [1 + C = 0] (?,1) 26. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [C >= 0 (?,1) && E >= 0 && 1 + C >= 2*E && 2*E >= C && F >= 0 && 1 + C >= 2*F && 2*F >= C && D >= 0 && 1 + C >= 2*D && 2*D >= C] 39. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [0 >= 2 + C (?,1) && 0 >= E && 0 >= F && 0 >= D && 2*E >= 1 + C && 2 + C >= 2*E && 2*F >= 1 + C && 2 + C >= 2*F && 2*D >= 1 + C && 2 + C >= 2*D] 40. evalrealheapsortstep1bb5in(A,B,C) -> evalrealheapsortstep1bb6in(A,1 + B,C) True (?,1) 41. evalrealheapsortstep1returnin(A,B,C) -> evalrealheapsortstep1stop(A,B,C) True (?,1) Signature: {(evalrealheapsortstep1bb2in,3) ;(evalrealheapsortstep1bb3in,3) ;(evalrealheapsortstep1bb4in,3) ;(evalrealheapsortstep1bb5in,3) ;(evalrealheapsortstep1bb6in,3) ;(evalrealheapsortstep1entryin,3) ;(evalrealheapsortstep1returnin,3) ;(evalrealheapsortstep1start,3) ;(evalrealheapsortstep1stop,3)} Flow Graph: [0->{1,2},1->{3,4},2->{41},3->{5,6},4->{41},5->{40},6->{7,8,9,10,11,12},7->{13,26,39},8->{13,26,39},9->{13 ,26,39},10->{40},11->{40},12->{40},13->{5,6},26->{5,6},39->{5,6},40->{3,4},41->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,4) ,(6,7) ,(6,9) ,(6,10) ,(6,12) ,(7,26) ,(7,39) ,(8,13) ,(8,39) ,(9,13) ,(9,26) ,(13,6) ,(39,6)] * Step 3: FromIts MAYBE + Considered Problem: Rules: 0. evalrealheapsortstep1start(A,B,C) -> evalrealheapsortstep1entryin(A,B,C) True (1,1) 1. evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1bb6in(A,1,C) [A >= 3] (?,1) 2. evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [2 >= A] (?,1) 3. evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,B) [A >= 1 + B] (?,1) 4. evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [B >= A] (?,1) 5. evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [0 >= C] (?,1) 6. evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb4in(A,B,C) [C >= 1] (?,1) 7. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb2in(A,B,C) [1 + C = 0] (?,1) 8. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb2in(A,B,C) [C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] (?,1) 9. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb2in(A,B,C) [0 >= 2 + C && 0 >= D && 2*D >= 1 + C && 2 + C >= 2*D] (?,1) 10. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [1 + C = 0] (?,1) 11. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] (?,1) 12. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [0 >= 2 + C && 0 >= D && 2*D >= 1 + C && 2 + C >= 2*D] (?,1) 13. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1) [1 + C = 0] (?,1) 26. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [C >= 0 (?,1) && E >= 0 && 1 + C >= 2*E && 2*E >= C && F >= 0 && 1 + C >= 2*F && 2*F >= C && D >= 0 && 1 + C >= 2*D && 2*D >= C] 39. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [0 >= 2 + C (?,1) && 0 >= E && 0 >= F && 0 >= D && 2*E >= 1 + C && 2 + C >= 2*E && 2*F >= 1 + C && 2 + C >= 2*F && 2*D >= 1 + C && 2 + C >= 2*D] 40. evalrealheapsortstep1bb5in(A,B,C) -> evalrealheapsortstep1bb6in(A,1 + B,C) True (?,1) 41. evalrealheapsortstep1returnin(A,B,C) -> evalrealheapsortstep1stop(A,B,C) True (?,1) Signature: {(evalrealheapsortstep1bb2in,3) ;(evalrealheapsortstep1bb3in,3) ;(evalrealheapsortstep1bb4in,3) ;(evalrealheapsortstep1bb5in,3) ;(evalrealheapsortstep1bb6in,3) ;(evalrealheapsortstep1entryin,3) ;(evalrealheapsortstep1returnin,3) ;(evalrealheapsortstep1start,3) ;(evalrealheapsortstep1stop,3)} Flow Graph: [0->{1,2},1->{3},2->{41},3->{5,6},4->{41},5->{40},6->{8,11},7->{13},8->{26},9->{39},10->{40},11->{40} ,12->{40},13->{5},26->{5,6},39->{5},40->{3,4},41->{}] + Applied Processor: FromIts + Details: () * Step 4: Unfold MAYBE + Considered Problem: Rules: evalrealheapsortstep1start(A,B,C) -> evalrealheapsortstep1entryin(A,B,C) True evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1bb6in(A,1,C) [A >= 3] evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [2 >= A] evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,B) [A >= 1 + B] evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [B >= A] evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [0 >= C] evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb4in(A,B,C) [C >= 1] evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb2in(A,B,C) [1 + C = 0] evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb2in(A,B,C) [C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb2in(A,B,C) [0 >= 2 + C && 0 >= D && 2*D >= 1 + C && 2 + C >= 2*D] evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [1 + C = 0] evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [0 >= 2 + C && 0 >= D && 2*D >= 1 + C && 2 + C >= 2*D] evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1) [1 + C = 0] evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C && F >= 0 && 1 + C >= 2*F && 2*F >= C && D >= 0 && 1 + C >= 2*D && 2*D >= C] evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [0 >= 2 + C && 0 >= E && 0 >= F && 0 >= D && 2*E >= 1 + C && 2 + C >= 2*E && 2*F >= 1 + C && 2 + C >= 2*F && 2*D >= 1 + C && 2 + C >= 2*D] evalrealheapsortstep1bb5in(A,B,C) -> evalrealheapsortstep1bb6in(A,1 + B,C) True evalrealheapsortstep1returnin(A,B,C) -> evalrealheapsortstep1stop(A,B,C) True Signature: {(evalrealheapsortstep1bb2in,3) ;(evalrealheapsortstep1bb3in,3) ;(evalrealheapsortstep1bb4in,3) ;(evalrealheapsortstep1bb5in,3) ;(evalrealheapsortstep1bb6in,3) ;(evalrealheapsortstep1entryin,3) ;(evalrealheapsortstep1returnin,3) ;(evalrealheapsortstep1start,3) ;(evalrealheapsortstep1stop,3)} Rule Graph: [0->{1,2},1->{3},2->{41},3->{5,6},4->{41},5->{40},6->{8,11},7->{13},8->{26},9->{39},10->{40},11->{40} ,12->{40},13->{5},26->{5,6},39->{5},40->{3,4},41->{}] + Applied Processor: Unfold + Details: () * Step 5: AddSinks MAYBE + Considered Problem: Rules: evalrealheapsortstep1start.0(A,B,C) -> evalrealheapsortstep1entryin.1(A,B,C) True evalrealheapsortstep1start.0(A,B,C) -> evalrealheapsortstep1entryin.2(A,B,C) True evalrealheapsortstep1entryin.1(A,B,C) -> evalrealheapsortstep1bb6in.3(A,1,C) [A >= 3] evalrealheapsortstep1entryin.2(A,B,C) -> evalrealheapsortstep1returnin.41(A,B,C) [2 >= A] evalrealheapsortstep1bb6in.3(A,B,C) -> evalrealheapsortstep1bb3in.5(A,B,B) [A >= 1 + B] evalrealheapsortstep1bb6in.3(A,B,C) -> evalrealheapsortstep1bb3in.6(A,B,B) [A >= 1 + B] evalrealheapsortstep1bb6in.4(A,B,C) -> evalrealheapsortstep1returnin.41(A,B,C) [B >= A] evalrealheapsortstep1bb3in.5(A,B,C) -> evalrealheapsortstep1bb5in.40(A,B,C) [0 >= C] evalrealheapsortstep1bb3in.6(A,B,C) -> evalrealheapsortstep1bb4in.8(A,B,C) [C >= 1] evalrealheapsortstep1bb3in.6(A,B,C) -> evalrealheapsortstep1bb4in.11(A,B,C) [C >= 1] evalrealheapsortstep1bb4in.7(A,B,C) -> evalrealheapsortstep1bb2in.13(A,B,C) [1 + C = 0] evalrealheapsortstep1bb4in.8(A,B,C) -> evalrealheapsortstep1bb2in.26(A,B,C) [C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] evalrealheapsortstep1bb4in.9(A,B,C) -> evalrealheapsortstep1bb2in.39(A,B,C) [0 >= 2 + C && 0 >= D && 2*D >= 1 + C && 2 + C >= 2*D] evalrealheapsortstep1bb4in.10(A,B,C) -> evalrealheapsortstep1bb5in.40(A,B,C) [1 + C = 0] evalrealheapsortstep1bb4in.11(A,B,C) -> evalrealheapsortstep1bb5in.40(A,B,C) [C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] evalrealheapsortstep1bb4in.12(A,B,C) -> evalrealheapsortstep1bb5in.40(A,B,C) [0 >= 2 + C && 0 >= D && 2*D >= 1 + C && 2 + C >= 2*D] evalrealheapsortstep1bb2in.13(A,B,C) -> evalrealheapsortstep1bb3in.5(A,B,-1) [1 + C = 0] evalrealheapsortstep1bb2in.26(A,B,C) -> evalrealheapsortstep1bb3in.5(A,B,-1 + D) [C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C && F >= 0 && 1 + C >= 2*F && 2*F >= C && D >= 0 && 1 + C >= 2*D && 2*D >= C] evalrealheapsortstep1bb2in.26(A,B,C) -> evalrealheapsortstep1bb3in.6(A,B,-1 + D) [C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C && F >= 0 && 1 + C >= 2*F && 2*F >= C && D >= 0 && 1 + C >= 2*D && 2*D >= C] evalrealheapsortstep1bb2in.39(A,B,C) -> evalrealheapsortstep1bb3in.5(A,B,-1 + D) [0 >= 2 + C && 0 >= E && 0 >= F && 0 >= D && 2*E >= 1 + C && 2 + C >= 2*E && 2*F >= 1 + C && 2 + C >= 2*F && 2*D >= 1 + C && 2 + C >= 2*D] evalrealheapsortstep1bb5in.40(A,B,C) -> evalrealheapsortstep1bb6in.3(A,1 + B,C) True evalrealheapsortstep1bb5in.40(A,B,C) -> evalrealheapsortstep1bb6in.4(A,1 + B,C) True evalrealheapsortstep1returnin.41(A,B,C) -> evalrealheapsortstep1stop.42(A,B,C) True Signature: {(evalrealheapsortstep1bb2in.13,3) ;(evalrealheapsortstep1bb2in.26,3) ;(evalrealheapsortstep1bb2in.39,3) ;(evalrealheapsortstep1bb3in.5,3) ;(evalrealheapsortstep1bb3in.6,3) ;(evalrealheapsortstep1bb4in.10,3) ;(evalrealheapsortstep1bb4in.11,3) ;(evalrealheapsortstep1bb4in.12,3) ;(evalrealheapsortstep1bb4in.7,3) ;(evalrealheapsortstep1bb4in.8,3) ;(evalrealheapsortstep1bb4in.9,3) ;(evalrealheapsortstep1bb5in.40,3) ;(evalrealheapsortstep1bb6in.3,3) ;(evalrealheapsortstep1bb6in.4,3) ;(evalrealheapsortstep1entryin.1,3) ;(evalrealheapsortstep1entryin.2,3) ;(evalrealheapsortstep1returnin.41,3) ;(evalrealheapsortstep1start.0,3) ;(evalrealheapsortstep1stop.42,3)} Rule Graph: [0->{2},1->{3},2->{4,5},3->{22},4->{7},5->{8,9},6->{22},7->{20,21},8->{11},9->{14},10->{16},11->{17,18} ,12->{19},13->{20,21},14->{20,21},15->{20,21},16->{7},17->{7},18->{8,9},19->{7},20->{4,5},21->{6},22->{}] + Applied Processor: AddSinks + Details: () * Step 6: Decompose MAYBE + Considered Problem: Rules: evalrealheapsortstep1start.0(A,B,C) -> evalrealheapsortstep1entryin.1(A,B,C) True evalrealheapsortstep1start.0(A,B,C) -> evalrealheapsortstep1entryin.2(A,B,C) True evalrealheapsortstep1entryin.1(A,B,C) -> evalrealheapsortstep1bb6in.3(A,1,C) [A >= 3] evalrealheapsortstep1entryin.2(A,B,C) -> evalrealheapsortstep1returnin.41(A,B,C) [2 >= A] evalrealheapsortstep1bb6in.3(A,B,C) -> evalrealheapsortstep1bb3in.5(A,B,B) [A >= 1 + B] evalrealheapsortstep1bb6in.3(A,B,C) -> evalrealheapsortstep1bb3in.6(A,B,B) [A >= 1 + B] evalrealheapsortstep1bb6in.4(A,B,C) -> evalrealheapsortstep1returnin.41(A,B,C) [B >= A] evalrealheapsortstep1bb3in.5(A,B,C) -> evalrealheapsortstep1bb5in.40(A,B,C) [0 >= C] evalrealheapsortstep1bb3in.6(A,B,C) -> evalrealheapsortstep1bb4in.8(A,B,C) [C >= 1] evalrealheapsortstep1bb3in.6(A,B,C) -> evalrealheapsortstep1bb4in.11(A,B,C) [C >= 1] evalrealheapsortstep1bb4in.7(A,B,C) -> evalrealheapsortstep1bb2in.13(A,B,C) [1 + C = 0] evalrealheapsortstep1bb4in.8(A,B,C) -> evalrealheapsortstep1bb2in.26(A,B,C) [C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] evalrealheapsortstep1bb4in.9(A,B,C) -> evalrealheapsortstep1bb2in.39(A,B,C) [0 >= 2 + C && 0 >= D && 2*D >= 1 + C && 2 + C >= 2*D] evalrealheapsortstep1bb4in.10(A,B,C) -> evalrealheapsortstep1bb5in.40(A,B,C) [1 + C = 0] evalrealheapsortstep1bb4in.11(A,B,C) -> evalrealheapsortstep1bb5in.40(A,B,C) [C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] evalrealheapsortstep1bb4in.12(A,B,C) -> evalrealheapsortstep1bb5in.40(A,B,C) [0 >= 2 + C && 0 >= D && 2*D >= 1 + C && 2 + C >= 2*D] evalrealheapsortstep1bb2in.13(A,B,C) -> evalrealheapsortstep1bb3in.5(A,B,-1) [1 + C = 0] evalrealheapsortstep1bb2in.26(A,B,C) -> evalrealheapsortstep1bb3in.5(A,B,-1 + D) [C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C && F >= 0 && 1 + C >= 2*F && 2*F >= C && D >= 0 && 1 + C >= 2*D && 2*D >= C] evalrealheapsortstep1bb2in.26(A,B,C) -> evalrealheapsortstep1bb3in.6(A,B,-1 + D) [C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C && F >= 0 && 1 + C >= 2*F && 2*F >= C && D >= 0 && 1 + C >= 2*D && 2*D >= C] evalrealheapsortstep1bb2in.39(A,B,C) -> evalrealheapsortstep1bb3in.5(A,B,-1 + D) [0 >= 2 + C && 0 >= E && 0 >= F && 0 >= D && 2*E >= 1 + C && 2 + C >= 2*E && 2*F >= 1 + C && 2 + C >= 2*F && 2*D >= 1 + C && 2 + C >= 2*D] evalrealheapsortstep1bb5in.40(A,B,C) -> evalrealheapsortstep1bb6in.3(A,1 + B,C) True evalrealheapsortstep1bb5in.40(A,B,C) -> evalrealheapsortstep1bb6in.4(A,1 + B,C) True evalrealheapsortstep1returnin.41(A,B,C) -> evalrealheapsortstep1stop.42(A,B,C) True evalrealheapsortstep1stop.42(A,B,C) -> exitus616(A,B,C) True evalrealheapsortstep1stop.42(A,B,C) -> exitus616(A,B,C) True evalrealheapsortstep1stop.42(A,B,C) -> exitus616(A,B,C) True evalrealheapsortstep1stop.42(A,B,C) -> exitus616(A,B,C) True evalrealheapsortstep1stop.42(A,B,C) -> exitus616(A,B,C) True evalrealheapsortstep1stop.42(A,B,C) -> exitus616(A,B,C) True Signature: {(evalrealheapsortstep1bb2in.13,3) ;(evalrealheapsortstep1bb2in.26,3) ;(evalrealheapsortstep1bb2in.39,3) ;(evalrealheapsortstep1bb3in.5,3) ;(evalrealheapsortstep1bb3in.6,3) ;(evalrealheapsortstep1bb4in.10,3) ;(evalrealheapsortstep1bb4in.11,3) ;(evalrealheapsortstep1bb4in.12,3) ;(evalrealheapsortstep1bb4in.7,3) ;(evalrealheapsortstep1bb4in.8,3) ;(evalrealheapsortstep1bb4in.9,3) ;(evalrealheapsortstep1bb5in.40,3) ;(evalrealheapsortstep1bb6in.3,3) ;(evalrealheapsortstep1bb6in.4,3) ;(evalrealheapsortstep1entryin.1,3) ;(evalrealheapsortstep1entryin.2,3) ;(evalrealheapsortstep1returnin.41,3) ;(evalrealheapsortstep1start.0,3) ;(evalrealheapsortstep1stop.42,3) ;(exitus616,3)} Rule Graph: [0->{2},1->{3},2->{4,5},3->{22},4->{7},5->{8,9},6->{22},7->{20,21},8->{11},9->{14},10->{16},11->{17,18} ,12->{19},13->{20,21},14->{20,21},15->{20,21},16->{7},17->{7},18->{8,9},19->{7},20->{4,5},21->{6},22->{23,24 ,25,26,27,28}] + 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] | `- p:[4,20,7,17,11,8,5,18,14,9] c: [4,5,7,9,14,17,20] | `- p:[8,18,11] c: [8,11,18] * Step 7: AbstractSize MAYBE + Considered Problem: (Rules: evalrealheapsortstep1start.0(A,B,C) -> evalrealheapsortstep1entryin.1(A,B,C) True evalrealheapsortstep1start.0(A,B,C) -> evalrealheapsortstep1entryin.2(A,B,C) True evalrealheapsortstep1entryin.1(A,B,C) -> evalrealheapsortstep1bb6in.3(A,1,C) [A >= 3] evalrealheapsortstep1entryin.2(A,B,C) -> evalrealheapsortstep1returnin.41(A,B,C) [2 >= A] evalrealheapsortstep1bb6in.3(A,B,C) -> evalrealheapsortstep1bb3in.5(A,B,B) [A >= 1 + B] evalrealheapsortstep1bb6in.3(A,B,C) -> evalrealheapsortstep1bb3in.6(A,B,B) [A >= 1 + B] evalrealheapsortstep1bb6in.4(A,B,C) -> evalrealheapsortstep1returnin.41(A,B,C) [B >= A] evalrealheapsortstep1bb3in.5(A,B,C) -> evalrealheapsortstep1bb5in.40(A,B,C) [0 >= C] evalrealheapsortstep1bb3in.6(A,B,C) -> evalrealheapsortstep1bb4in.8(A,B,C) [C >= 1] evalrealheapsortstep1bb3in.6(A,B,C) -> evalrealheapsortstep1bb4in.11(A,B,C) [C >= 1] evalrealheapsortstep1bb4in.7(A,B,C) -> evalrealheapsortstep1bb2in.13(A,B,C) [1 + C = 0] evalrealheapsortstep1bb4in.8(A,B,C) -> evalrealheapsortstep1bb2in.26(A,B,C) [C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] evalrealheapsortstep1bb4in.9(A,B,C) -> evalrealheapsortstep1bb2in.39(A,B,C) [0 >= 2 + C && 0 >= D && 2*D >= 1 + C && 2 + C >= 2*D] evalrealheapsortstep1bb4in.10(A,B,C) -> evalrealheapsortstep1bb5in.40(A,B,C) [1 + C = 0] evalrealheapsortstep1bb4in.11(A,B,C) -> evalrealheapsortstep1bb5in.40(A,B,C) [C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] evalrealheapsortstep1bb4in.12(A,B,C) -> evalrealheapsortstep1bb5in.40(A,B,C) [0 >= 2 + C && 0 >= D && 2*D >= 1 + C && 2 + C >= 2*D] evalrealheapsortstep1bb2in.13(A,B,C) -> evalrealheapsortstep1bb3in.5(A,B,-1) [1 + C = 0] evalrealheapsortstep1bb2in.26(A,B,C) -> evalrealheapsortstep1bb3in.5(A,B,-1 + D) [C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C && F >= 0 && 1 + C >= 2*F && 2*F >= C && D >= 0 && 1 + C >= 2*D && 2*D >= C] evalrealheapsortstep1bb2in.26(A,B,C) -> evalrealheapsortstep1bb3in.6(A,B,-1 + D) [C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C && F >= 0 && 1 + C >= 2*F && 2*F >= C && D >= 0 && 1 + C >= 2*D && 2*D >= C] evalrealheapsortstep1bb2in.39(A,B,C) -> evalrealheapsortstep1bb3in.5(A,B,-1 + D) [0 >= 2 + C && 0 >= E && 0 >= F && 0 >= D && 2*E >= 1 + C && 2 + C >= 2*E && 2*F >= 1 + C && 2 + C >= 2*F && 2*D >= 1 + C && 2 + C >= 2*D] evalrealheapsortstep1bb5in.40(A,B,C) -> evalrealheapsortstep1bb6in.3(A,1 + B,C) True evalrealheapsortstep1bb5in.40(A,B,C) -> evalrealheapsortstep1bb6in.4(A,1 + B,C) True evalrealheapsortstep1returnin.41(A,B,C) -> evalrealheapsortstep1stop.42(A,B,C) True evalrealheapsortstep1stop.42(A,B,C) -> exitus616(A,B,C) True evalrealheapsortstep1stop.42(A,B,C) -> exitus616(A,B,C) True evalrealheapsortstep1stop.42(A,B,C) -> exitus616(A,B,C) True evalrealheapsortstep1stop.42(A,B,C) -> exitus616(A,B,C) True evalrealheapsortstep1stop.42(A,B,C) -> exitus616(A,B,C) True evalrealheapsortstep1stop.42(A,B,C) -> exitus616(A,B,C) True Signature: {(evalrealheapsortstep1bb2in.13,3) ;(evalrealheapsortstep1bb2in.26,3) ;(evalrealheapsortstep1bb2in.39,3) ;(evalrealheapsortstep1bb3in.5,3) ;(evalrealheapsortstep1bb3in.6,3) ;(evalrealheapsortstep1bb4in.10,3) ;(evalrealheapsortstep1bb4in.11,3) ;(evalrealheapsortstep1bb4in.12,3) ;(evalrealheapsortstep1bb4in.7,3) ;(evalrealheapsortstep1bb4in.8,3) ;(evalrealheapsortstep1bb4in.9,3) ;(evalrealheapsortstep1bb5in.40,3) ;(evalrealheapsortstep1bb6in.3,3) ;(evalrealheapsortstep1bb6in.4,3) ;(evalrealheapsortstep1entryin.1,3) ;(evalrealheapsortstep1entryin.2,3) ;(evalrealheapsortstep1returnin.41,3) ;(evalrealheapsortstep1start.0,3) ;(evalrealheapsortstep1stop.42,3) ;(exitus616,3)} Rule Graph: [0->{2},1->{3},2->{4,5},3->{22},4->{7},5->{8,9},6->{22},7->{20,21},8->{11},9->{14},10->{16},11->{17,18} ,12->{19},13->{20,21},14->{20,21},15->{20,21},16->{7},17->{7},18->{8,9},19->{7},20->{4,5},21->{6},22->{23,24 ,25,26,27,28}] ,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] | `- p:[4,20,7,17,11,8,5,18,14,9] c: [4,5,7,9,14,17,20] | `- p:[8,18,11] c: [8,11,18]) + Applied Processor: AbstractSize Minimize + Details: () * Step 8: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,C,0.0,0.0.0] evalrealheapsortstep1start.0 ~> evalrealheapsortstep1entryin.1 [A <= A, B <= B, C <= C] evalrealheapsortstep1start.0 ~> evalrealheapsortstep1entryin.2 [A <= A, B <= B, C <= C] evalrealheapsortstep1entryin.1 ~> evalrealheapsortstep1bb6in.3 [A <= A, B <= K, C <= C] evalrealheapsortstep1entryin.2 ~> evalrealheapsortstep1returnin.41 [A <= A, B <= B, C <= C] evalrealheapsortstep1bb6in.3 ~> evalrealheapsortstep1bb3in.5 [A <= A, B <= B, C <= B] evalrealheapsortstep1bb6in.3 ~> evalrealheapsortstep1bb3in.6 [A <= A, B <= B, C <= B] evalrealheapsortstep1bb6in.4 ~> evalrealheapsortstep1returnin.41 [A <= A, B <= B, C <= C] evalrealheapsortstep1bb3in.5 ~> evalrealheapsortstep1bb5in.40 [A <= A, B <= B, C <= C] evalrealheapsortstep1bb3in.6 ~> evalrealheapsortstep1bb4in.8 [A <= A, B <= B, C <= C] evalrealheapsortstep1bb3in.6 ~> evalrealheapsortstep1bb4in.11 [A <= A, B <= B, C <= C] evalrealheapsortstep1bb4in.7 ~> evalrealheapsortstep1bb2in.13 [A <= A, B <= B, C <= C] evalrealheapsortstep1bb4in.8 ~> evalrealheapsortstep1bb2in.26 [A <= A, B <= B, C <= C] evalrealheapsortstep1bb4in.9 ~> evalrealheapsortstep1bb2in.39 [A <= A, B <= B, C <= C] evalrealheapsortstep1bb4in.10 ~> evalrealheapsortstep1bb5in.40 [A <= A, B <= B, C <= C] evalrealheapsortstep1bb4in.11 ~> evalrealheapsortstep1bb5in.40 [A <= A, B <= B, C <= C] evalrealheapsortstep1bb4in.12 ~> evalrealheapsortstep1bb5in.40 [A <= A, B <= B, C <= C] evalrealheapsortstep1bb2in.13 ~> evalrealheapsortstep1bb3in.5 [A <= A, B <= B, C <= K] evalrealheapsortstep1bb2in.26 ~> evalrealheapsortstep1bb3in.5 [A <= A, B <= B, C <= K + C] evalrealheapsortstep1bb2in.26 ~> evalrealheapsortstep1bb3in.6 [A <= A, B <= B, C <= K + C] evalrealheapsortstep1bb2in.39 ~> evalrealheapsortstep1bb3in.5 [A <= A, B <= B, C <= C] evalrealheapsortstep1bb5in.40 ~> evalrealheapsortstep1bb6in.3 [A <= A, B <= K + B, C <= C] evalrealheapsortstep1bb5in.40 ~> evalrealheapsortstep1bb6in.4 [A <= A, B <= K + B, C <= C] evalrealheapsortstep1returnin.41 ~> evalrealheapsortstep1stop.42 [A <= A, B <= B, C <= C] evalrealheapsortstep1stop.42 ~> exitus616 [A <= A, B <= B, C <= C] evalrealheapsortstep1stop.42 ~> exitus616 [A <= A, B <= B, C <= C] evalrealheapsortstep1stop.42 ~> exitus616 [A <= A, B <= B, C <= C] evalrealheapsortstep1stop.42 ~> exitus616 [A <= A, B <= B, C <= C] evalrealheapsortstep1stop.42 ~> exitus616 [A <= A, B <= B, C <= C] evalrealheapsortstep1stop.42 ~> exitus616 [A <= A, B <= B, C <= C] + Loop: [0.0 <= K + A + B] evalrealheapsortstep1bb6in.3 ~> evalrealheapsortstep1bb3in.5 [A <= A, B <= B, C <= B] evalrealheapsortstep1bb5in.40 ~> evalrealheapsortstep1bb6in.3 [A <= A, B <= K + B, C <= C] evalrealheapsortstep1bb3in.5 ~> evalrealheapsortstep1bb5in.40 [A <= A, B <= B, C <= C] evalrealheapsortstep1bb2in.26 ~> evalrealheapsortstep1bb3in.5 [A <= A, B <= B, C <= K + C] evalrealheapsortstep1bb4in.8 ~> evalrealheapsortstep1bb2in.26 [A <= A, B <= B, C <= C] evalrealheapsortstep1bb3in.6 ~> evalrealheapsortstep1bb4in.8 [A <= A, B <= B, C <= C] evalrealheapsortstep1bb6in.3 ~> evalrealheapsortstep1bb3in.6 [A <= A, B <= B, C <= B] evalrealheapsortstep1bb2in.26 ~> evalrealheapsortstep1bb3in.6 [A <= A, B <= B, C <= K + C] evalrealheapsortstep1bb4in.11 ~> evalrealheapsortstep1bb5in.40 [A <= A, B <= B, C <= C] evalrealheapsortstep1bb3in.6 ~> evalrealheapsortstep1bb4in.11 [A <= A, B <= B, C <= C] + Loop: [0.0.0 <= 2*C] evalrealheapsortstep1bb3in.6 ~> evalrealheapsortstep1bb4in.8 [A <= A, B <= B, C <= C] evalrealheapsortstep1bb2in.26 ~> evalrealheapsortstep1bb3in.6 [A <= A, B <= B, C <= K + C] evalrealheapsortstep1bb4in.8 ~> evalrealheapsortstep1bb2in.26 [A <= A, B <= B, C <= C] + Applied Processor: AbstractFlow + Details: () * Step 9: Lare MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,0.0,0.0.0] evalrealheapsortstep1start.0 ~> evalrealheapsortstep1entryin.1 [] evalrealheapsortstep1start.0 ~> evalrealheapsortstep1entryin.2 [] evalrealheapsortstep1entryin.1 ~> evalrealheapsortstep1bb6in.3 [K ~=> B] evalrealheapsortstep1entryin.2 ~> evalrealheapsortstep1returnin.41 [] evalrealheapsortstep1bb6in.3 ~> evalrealheapsortstep1bb3in.5 [B ~=> C] evalrealheapsortstep1bb6in.3 ~> evalrealheapsortstep1bb3in.6 [B ~=> C] evalrealheapsortstep1bb6in.4 ~> evalrealheapsortstep1returnin.41 [] evalrealheapsortstep1bb3in.5 ~> evalrealheapsortstep1bb5in.40 [] evalrealheapsortstep1bb3in.6 ~> evalrealheapsortstep1bb4in.8 [] evalrealheapsortstep1bb3in.6 ~> evalrealheapsortstep1bb4in.11 [] evalrealheapsortstep1bb4in.7 ~> evalrealheapsortstep1bb2in.13 [] evalrealheapsortstep1bb4in.8 ~> evalrealheapsortstep1bb2in.26 [] evalrealheapsortstep1bb4in.9 ~> evalrealheapsortstep1bb2in.39 [] evalrealheapsortstep1bb4in.10 ~> evalrealheapsortstep1bb5in.40 [] evalrealheapsortstep1bb4in.11 ~> evalrealheapsortstep1bb5in.40 [] evalrealheapsortstep1bb4in.12 ~> evalrealheapsortstep1bb5in.40 [] evalrealheapsortstep1bb2in.13 ~> evalrealheapsortstep1bb3in.5 [K ~=> C] evalrealheapsortstep1bb2in.26 ~> evalrealheapsortstep1bb3in.5 [C ~+> C,K ~+> C] evalrealheapsortstep1bb2in.26 ~> evalrealheapsortstep1bb3in.6 [C ~+> C,K ~+> C] evalrealheapsortstep1bb2in.39 ~> evalrealheapsortstep1bb3in.5 [] evalrealheapsortstep1bb5in.40 ~> evalrealheapsortstep1bb6in.3 [B ~+> B,K ~+> B] evalrealheapsortstep1bb5in.40 ~> evalrealheapsortstep1bb6in.4 [B ~+> B,K ~+> B] evalrealheapsortstep1returnin.41 ~> evalrealheapsortstep1stop.42 [] evalrealheapsortstep1stop.42 ~> exitus616 [] evalrealheapsortstep1stop.42 ~> exitus616 [] evalrealheapsortstep1stop.42 ~> exitus616 [] evalrealheapsortstep1stop.42 ~> exitus616 [] evalrealheapsortstep1stop.42 ~> exitus616 [] evalrealheapsortstep1stop.42 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] evalrealheapsortstep1bb6in.3 ~> evalrealheapsortstep1bb3in.5 [B ~=> C] evalrealheapsortstep1bb5in.40 ~> evalrealheapsortstep1bb6in.3 [B ~+> B,K ~+> B] evalrealheapsortstep1bb3in.5 ~> evalrealheapsortstep1bb5in.40 [] evalrealheapsortstep1bb2in.26 ~> evalrealheapsortstep1bb3in.5 [C ~+> C,K ~+> C] evalrealheapsortstep1bb4in.8 ~> evalrealheapsortstep1bb2in.26 [] evalrealheapsortstep1bb3in.6 ~> evalrealheapsortstep1bb4in.8 [] evalrealheapsortstep1bb6in.3 ~> evalrealheapsortstep1bb3in.6 [B ~=> C] evalrealheapsortstep1bb2in.26 ~> evalrealheapsortstep1bb3in.6 [C ~+> C,K ~+> C] evalrealheapsortstep1bb4in.11 ~> evalrealheapsortstep1bb5in.40 [] evalrealheapsortstep1bb3in.6 ~> evalrealheapsortstep1bb4in.11 [] + Loop: [C ~*> 0.0.0] evalrealheapsortstep1bb3in.6 ~> evalrealheapsortstep1bb4in.8 [] evalrealheapsortstep1bb2in.26 ~> evalrealheapsortstep1bb3in.6 [C ~+> C,K ~+> C] evalrealheapsortstep1bb4in.8 ~> evalrealheapsortstep1bb2in.26 [] + Applied Processor: Lare + Details: evalrealheapsortstep1start.0 ~> exitus616 [K ~=> C ,A ~+> 0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> C ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,A ~*> C ,A ~*> 0.0 ,A ~*> 0.0.0 ,A ~*> tick ,K ~*> B ,K ~*> C ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> C ,A ~^> 0.0.0 ,A ~^> tick ,K ~^> C ,K ~^> 0.0.0 ,K ~^> tick] evalrealheapsortstep1bb4in.10 ~> exitus616 [A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> C ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> C ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,A ~*> C ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> C ,B ~*> 0.0.0 ,B ~*> tick ,K ~*> B ,K ~*> C ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> C ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> C ,B ~^> 0.0.0 ,B ~^> tick ,K ~^> C ,K ~^> 0.0.0 ,K ~^> tick] evalrealheapsortstep1bb4in.12 ~> exitus616 [A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> C ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> C ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,A ~*> C ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> C ,B ~*> 0.0.0 ,B ~*> tick ,K ~*> B ,K ~*> C ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> C ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> C ,B ~^> 0.0.0 ,B ~^> tick ,K ~^> C ,K ~^> 0.0.0 ,K ~^> tick] evalrealheapsortstep1bb4in.7 ~> exitus616 [K ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> C ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> C ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,A ~*> C ,A ~*> 0.0 ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> C ,B ~*> 0.0 ,B ~*> 0.0.0 ,B ~*> tick ,K ~*> B ,K ~*> C ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> C ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> C ,B ~^> 0.0.0 ,B ~^> tick ,K ~^> C ,K ~^> 0.0.0 ,K ~^> tick] evalrealheapsortstep1bb4in.9 ~> exitus616 [A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> C ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> C ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,A ~*> C ,A ~*> 0.0 ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> C ,B ~*> 0.0 ,B ~*> 0.0.0 ,B ~*> tick ,K ~*> B ,K ~*> C ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> C ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> C ,B ~^> 0.0.0 ,B ~^> tick ,K ~^> C ,K ~^> 0.0.0 ,K ~^> tick] + evalrealheapsortstep1bb5in.40> [A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> C ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> C ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,A ~*> C ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> C ,B ~*> 0.0.0 ,B ~*> tick ,K ~*> B ,K ~*> C ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> C ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> C ,B ~^> 0.0.0 ,B ~^> tick ,K ~^> C ,K ~^> 0.0.0 ,K ~^> tick] evalrealheapsortstep1bb5in.40> [A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> C ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> C ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,A ~*> C ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> C ,B ~*> 0.0.0 ,B ~*> tick ,K ~*> B ,K ~*> C ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> C ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> C ,B ~^> 0.0.0 ,B ~^> tick ,K ~^> C ,K ~^> 0.0.0 ,K ~^> tick] evalrealheapsortstep1bb5in.40> [B ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> C ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> C ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,A ~*> C ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> C ,B ~*> 0.0.0 ,B ~*> tick ,K ~*> B ,K ~*> C ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> C ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> C ,B ~^> 0.0.0 ,B ~^> tick ,K ~^> C ,K ~^> 0.0.0 ,K ~^> tick] + evalrealheapsortstep1bb3in.6> [C ~+> C ,tick ~+> tick ,K ~+> C ,C ~*> C ,C ~*> 0.0.0 ,C ~*> tick ,K ~*> C] evalrealheapsortstep1bb2in.26> [C ~+> C ,tick ~+> tick ,K ~+> C ,C ~*> C ,C ~*> 0.0.0 ,C ~*> tick ,K ~*> C] YES(?,PRIMREC)