YES(?,POLY) * Step 1: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealheapsortstart(A,B,C,D) -> evalrealheapsortentryin(A,B,C,D) True (1,1) 1. evalrealheapsortentryin(A,B,C,D) -> evalrealheapsortreturnin(A,B,C,D) [2 >= A] (?,1) 2. evalrealheapsortentryin(A,B,C,D) -> evalrealheapsortbb6in(A,1,C,D) [A >= 3] (?,1) 3. evalrealheapsortreturnin(A,B,C,D) -> evalrealheapsortstop(A,B,C,D) True (?,1) 4. evalrealheapsortbb6in(A,B,C,D) -> evalrealheapsortbb3in(A,B,B,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && A >= 1 + B] (?,1) 5. evalrealheapsortbb3in(A,B,C,D) -> evalrealheapsortbb4in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] 6. evalrealheapsortbb3in(A,B,C,D) -> evalrealheapsortbb5in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && 0 >= C] 7. evalrealheapsortbb4in(A,B,C,D) -> evalrealheapsortbb5in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] 8. evalrealheapsortbb4in(A,B,C,D) -> evalrealheapsortbb2in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] 9. evalrealheapsortbb5in(A,B,C,D) -> evalrealheapsortbb6in(A,1 + B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] (?,1) 10. evalrealheapsortbb6in(A,B,C,D) -> evalrealheapsortbb7in(A,B,C,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && B >= A] (?,1) 11. evalrealheapsortbb2in(A,B,C,D) -> evalrealheapsortbb3in(A,B,-1 + E,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && G >= 0 && 1 + C >= 2*G && 2*G >= C && E >= 0 && 1 + C >= 2*E && 2*E >= C] 12. evalrealheapsortbb7in(A,B,C,D) -> evalrealheapsortbb18in(A,0,C,D) [-3 + B >= 0 && -6 + A + B >= 0 && -1*A + B >= 0 && -3 + A >= 0] (?,1) 13. evalrealheapsortbb18in(A,B,C,D) -> evalrealheapsortreturnin(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] (?,1) 14. evalrealheapsortbb18in(A,B,C,D) -> evalrealheapsortbb8in(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] (?,1) 15. evalrealheapsortbb8in(A,B,C,D) -> evalrealheapsortbb16in(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] (?,1) 16. evalrealheapsortbb16in(A,B,C,D) -> evalrealheapsortbb17in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 2 + B + 2*C >= A] (?,1) 17. evalrealheapsortbb16in(A,B,C,D) -> evalrealheapsortbb9in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] (?,1) 18. evalrealheapsortbb17in(A,B,C,D) -> evalrealheapsortbb18in(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] (?,1) 19. evalrealheapsortbb9in(A,B,C,D) -> evalrealheapsortbb10in(A,B,C,D) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] 20. evalrealheapsortbb9in(A,B,C,D) -> evalrealheapsortbb11in(A,B,C,D) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A = 3 + B + 2*C] 21. evalrealheapsortbb10in(A,B,C,D) -> evalrealheapsortbb12in(A,B,C,D) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 22. evalrealheapsortbb10in(A,B,C,D) -> evalrealheapsortbb11in(A,B,C,D) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 23. evalrealheapsortbb11in(A,B,C,D) -> evalrealheapsortbb13in(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 24. evalrealheapsortbb13in(A,B,C,D) -> evalrealheapsortbb16in(A,B,A,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 25. evalrealheapsortbb13in(A,B,C,D) -> evalrealheapsortbb14in(A,B,C,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 26. evalrealheapsortbb12in(A,B,C,D) -> evalrealheapsortbb13in(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 27. evalrealheapsortbb14in(A,B,C,D) -> evalrealheapsortbb16in(A,B,D,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] Signature: {(evalrealheapsortbb10in,4) ;(evalrealheapsortbb11in,4) ;(evalrealheapsortbb12in,4) ;(evalrealheapsortbb13in,4) ;(evalrealheapsortbb14in,4) ;(evalrealheapsortbb16in,4) ;(evalrealheapsortbb17in,4) ;(evalrealheapsortbb18in,4) ;(evalrealheapsortbb2in,4) ;(evalrealheapsortbb3in,4) ;(evalrealheapsortbb4in,4) ;(evalrealheapsortbb5in,4) ;(evalrealheapsortbb6in,4) ;(evalrealheapsortbb7in,4) ;(evalrealheapsortbb8in,4) ;(evalrealheapsortbb9in,4) ;(evalrealheapsortentryin,4) ;(evalrealheapsortreturnin,4) ;(evalrealheapsortstart,4) ;(evalrealheapsortstop,4)} Flow Graph: [0->{1,2},1->{3},2->{4,10},3->{},4->{5,6},5->{7,8},6->{9},7->{9},8->{11},9->{4,10},10->{12},11->{5,6} ,12->{13,14},13->{3},14->{15},15->{16,17},16->{18},17->{19,20},18->{13,14},19->{21,22},20->{23},21->{26} ,22->{23},23->{24,25},24->{16,17},25->{27},26->{24,25},27->{16,17}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,10),(4,6),(12,13),(24,17)] * Step 2: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealheapsortstart(A,B,C,D) -> evalrealheapsortentryin(A,B,C,D) True (1,1) 1. evalrealheapsortentryin(A,B,C,D) -> evalrealheapsortreturnin(A,B,C,D) [2 >= A] (?,1) 2. evalrealheapsortentryin(A,B,C,D) -> evalrealheapsortbb6in(A,1,C,D) [A >= 3] (?,1) 3. evalrealheapsortreturnin(A,B,C,D) -> evalrealheapsortstop(A,B,C,D) True (?,1) 4. evalrealheapsortbb6in(A,B,C,D) -> evalrealheapsortbb3in(A,B,B,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && A >= 1 + B] (?,1) 5. evalrealheapsortbb3in(A,B,C,D) -> evalrealheapsortbb4in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] 6. evalrealheapsortbb3in(A,B,C,D) -> evalrealheapsortbb5in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && 0 >= C] 7. evalrealheapsortbb4in(A,B,C,D) -> evalrealheapsortbb5in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] 8. evalrealheapsortbb4in(A,B,C,D) -> evalrealheapsortbb2in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] 9. evalrealheapsortbb5in(A,B,C,D) -> evalrealheapsortbb6in(A,1 + B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] (?,1) 10. evalrealheapsortbb6in(A,B,C,D) -> evalrealheapsortbb7in(A,B,C,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && B >= A] (?,1) 11. evalrealheapsortbb2in(A,B,C,D) -> evalrealheapsortbb3in(A,B,-1 + E,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && G >= 0 && 1 + C >= 2*G && 2*G >= C && E >= 0 && 1 + C >= 2*E && 2*E >= C] 12. evalrealheapsortbb7in(A,B,C,D) -> evalrealheapsortbb18in(A,0,C,D) [-3 + B >= 0 && -6 + A + B >= 0 && -1*A + B >= 0 && -3 + A >= 0] (?,1) 13. evalrealheapsortbb18in(A,B,C,D) -> evalrealheapsortreturnin(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] (?,1) 14. evalrealheapsortbb18in(A,B,C,D) -> evalrealheapsortbb8in(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] (?,1) 15. evalrealheapsortbb8in(A,B,C,D) -> evalrealheapsortbb16in(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] (?,1) 16. evalrealheapsortbb16in(A,B,C,D) -> evalrealheapsortbb17in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 2 + B + 2*C >= A] (?,1) 17. evalrealheapsortbb16in(A,B,C,D) -> evalrealheapsortbb9in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] (?,1) 18. evalrealheapsortbb17in(A,B,C,D) -> evalrealheapsortbb18in(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] (?,1) 19. evalrealheapsortbb9in(A,B,C,D) -> evalrealheapsortbb10in(A,B,C,D) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] 20. evalrealheapsortbb9in(A,B,C,D) -> evalrealheapsortbb11in(A,B,C,D) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A = 3 + B + 2*C] 21. evalrealheapsortbb10in(A,B,C,D) -> evalrealheapsortbb12in(A,B,C,D) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 22. evalrealheapsortbb10in(A,B,C,D) -> evalrealheapsortbb11in(A,B,C,D) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 23. evalrealheapsortbb11in(A,B,C,D) -> evalrealheapsortbb13in(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 24. evalrealheapsortbb13in(A,B,C,D) -> evalrealheapsortbb16in(A,B,A,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 25. evalrealheapsortbb13in(A,B,C,D) -> evalrealheapsortbb14in(A,B,C,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 26. evalrealheapsortbb12in(A,B,C,D) -> evalrealheapsortbb13in(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 27. evalrealheapsortbb14in(A,B,C,D) -> evalrealheapsortbb16in(A,B,D,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] Signature: {(evalrealheapsortbb10in,4) ;(evalrealheapsortbb11in,4) ;(evalrealheapsortbb12in,4) ;(evalrealheapsortbb13in,4) ;(evalrealheapsortbb14in,4) ;(evalrealheapsortbb16in,4) ;(evalrealheapsortbb17in,4) ;(evalrealheapsortbb18in,4) ;(evalrealheapsortbb2in,4) ;(evalrealheapsortbb3in,4) ;(evalrealheapsortbb4in,4) ;(evalrealheapsortbb5in,4) ;(evalrealheapsortbb6in,4) ;(evalrealheapsortbb7in,4) ;(evalrealheapsortbb8in,4) ;(evalrealheapsortbb9in,4) ;(evalrealheapsortentryin,4) ;(evalrealheapsortreturnin,4) ;(evalrealheapsortstart,4) ;(evalrealheapsortstop,4)} Flow Graph: [0->{1,2},1->{3},2->{4},3->{},4->{5},5->{7,8},6->{9},7->{9},8->{11},9->{4,10},10->{12},11->{5,6},12->{14} ,13->{3},14->{15},15->{16,17},16->{18},17->{19,20},18->{13,14},19->{21,22},20->{23},21->{26},22->{23} ,23->{24,25},24->{16},25->{27},26->{24,25},27->{16,17}] + Applied Processor: FromIts + Details: () * Step 3: Unfold WORST_CASE(?,POLY) + Considered Problem: Rules: evalrealheapsortstart(A,B,C,D) -> evalrealheapsortentryin(A,B,C,D) True evalrealheapsortentryin(A,B,C,D) -> evalrealheapsortreturnin(A,B,C,D) [2 >= A] evalrealheapsortentryin(A,B,C,D) -> evalrealheapsortbb6in(A,1,C,D) [A >= 3] evalrealheapsortreturnin(A,B,C,D) -> evalrealheapsortstop(A,B,C,D) True evalrealheapsortbb6in(A,B,C,D) -> evalrealheapsortbb3in(A,B,B,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && A >= 1 + B] evalrealheapsortbb3in(A,B,C,D) -> evalrealheapsortbb4in(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] evalrealheapsortbb3in(A,B,C,D) -> evalrealheapsortbb5in(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && 0 >= C] evalrealheapsortbb4in(A,B,C,D) -> evalrealheapsortbb5in(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb4in(A,B,C,D) -> evalrealheapsortbb2in(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb5in(A,B,C,D) -> evalrealheapsortbb6in(A,1 + B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb6in(A,B,C,D) -> evalrealheapsortbb7in(A,B,C,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && B >= A] evalrealheapsortbb2in(A,B,C,D) -> evalrealheapsortbb3in(A,B,-1 + E,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && G >= 0 && 1 + C >= 2*G && 2*G >= C && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb7in(A,B,C,D) -> evalrealheapsortbb18in(A,0,C,D) [-3 + B >= 0 && -6 + A + B >= 0 && -1*A + B >= 0 && -3 + A >= 0] evalrealheapsortbb18in(A,B,C,D) -> evalrealheapsortreturnin(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] evalrealheapsortbb18in(A,B,C,D) -> evalrealheapsortbb8in(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] evalrealheapsortbb8in(A,B,C,D) -> evalrealheapsortbb16in(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb16in(A,B,C,D) -> evalrealheapsortbb17in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 2 + B + 2*C >= A] evalrealheapsortbb16in(A,B,C,D) -> evalrealheapsortbb9in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] evalrealheapsortbb17in(A,B,C,D) -> evalrealheapsortbb18in(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb9in(A,B,C,D) -> evalrealheapsortbb10in(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] evalrealheapsortbb9in(A,B,C,D) -> evalrealheapsortbb11in(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A = 3 + B + 2*C] evalrealheapsortbb10in(A,B,C,D) -> evalrealheapsortbb12in(A,B,C,D) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb10in(A,B,C,D) -> evalrealheapsortbb11in(A,B,C,D) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb11in(A,B,C,D) -> evalrealheapsortbb13in(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb13in(A,B,C,D) -> evalrealheapsortbb16in(A,B,A,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb13in(A,B,C,D) -> evalrealheapsortbb14in(A,B,C,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb12in(A,B,C,D) -> evalrealheapsortbb13in(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb14in(A,B,C,D) -> evalrealheapsortbb16in(A,B,D,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] Signature: {(evalrealheapsortbb10in,4) ;(evalrealheapsortbb11in,4) ;(evalrealheapsortbb12in,4) ;(evalrealheapsortbb13in,4) ;(evalrealheapsortbb14in,4) ;(evalrealheapsortbb16in,4) ;(evalrealheapsortbb17in,4) ;(evalrealheapsortbb18in,4) ;(evalrealheapsortbb2in,4) ;(evalrealheapsortbb3in,4) ;(evalrealheapsortbb4in,4) ;(evalrealheapsortbb5in,4) ;(evalrealheapsortbb6in,4) ;(evalrealheapsortbb7in,4) ;(evalrealheapsortbb8in,4) ;(evalrealheapsortbb9in,4) ;(evalrealheapsortentryin,4) ;(evalrealheapsortreturnin,4) ;(evalrealheapsortstart,4) ;(evalrealheapsortstop,4)} Rule Graph: [0->{1,2},1->{3},2->{4},3->{},4->{5},5->{7,8},6->{9},7->{9},8->{11},9->{4,10},10->{12},11->{5,6},12->{14} ,13->{3},14->{15},15->{16,17},16->{18},17->{19,20},18->{13,14},19->{21,22},20->{23},21->{26},22->{23} ,23->{24,25},24->{16},25->{27},26->{24,25},27->{16,17}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: evalrealheapsortstart.0(A,B,C,D) -> evalrealheapsortentryin.1(A,B,C,D) True evalrealheapsortstart.0(A,B,C,D) -> evalrealheapsortentryin.2(A,B,C,D) True evalrealheapsortentryin.1(A,B,C,D) -> evalrealheapsortreturnin.3(A,B,C,D) [2 >= A] evalrealheapsortentryin.2(A,B,C,D) -> evalrealheapsortbb6in.4(A,1,C,D) [A >= 3] evalrealheapsortreturnin.3(A,B,C,D) -> evalrealheapsortstop.28(A,B,C,D) True evalrealheapsortbb6in.4(A,B,C,D) -> evalrealheapsortbb3in.5(A,B,B,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && A >= 1 + B] evalrealheapsortbb3in.5(A,B,C,D) -> evalrealheapsortbb4in.7(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] evalrealheapsortbb3in.5(A,B,C,D) -> evalrealheapsortbb4in.8(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] evalrealheapsortbb3in.6(A,B,C,D) -> evalrealheapsortbb5in.9(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && 0 >= C] evalrealheapsortbb4in.7(A,B,C,D) -> evalrealheapsortbb5in.9(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb4in.8(A,B,C,D) -> evalrealheapsortbb2in.11(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb5in.9(A,B,C,D) -> evalrealheapsortbb6in.4(A,1 + B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb5in.9(A,B,C,D) -> evalrealheapsortbb6in.10(A,1 + B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb6in.10(A,B,C,D) -> evalrealheapsortbb7in.12(A,B,C,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && B >= A] evalrealheapsortbb2in.11(A,B,C,D) -> evalrealheapsortbb3in.5(A,B,-1 + E,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && G >= 0 && 1 + C >= 2*G && 2*G >= C && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb2in.11(A,B,C,D) -> evalrealheapsortbb3in.6(A,B,-1 + E,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && G >= 0 && 1 + C >= 2*G && 2*G >= C && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb7in.12(A,B,C,D) -> evalrealheapsortbb18in.14(A,0,C,D) [-3 + B >= 0 && -6 + A + B >= 0 && -1*A + B >= 0 && -3 + A >= 0] evalrealheapsortbb18in.13(A,B,C,D) -> evalrealheapsortreturnin.3(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] evalrealheapsortbb18in.14(A,B,C,D) -> evalrealheapsortbb8in.15(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] evalrealheapsortbb8in.15(A,B,C,D) -> evalrealheapsortbb16in.16(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb8in.15(A,B,C,D) -> evalrealheapsortbb16in.17(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb16in.16(A,B,C,D) -> evalrealheapsortbb17in.18(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 2 + B + 2*C >= A] evalrealheapsortbb16in.17(A,B,C,D) -> evalrealheapsortbb9in.19(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] evalrealheapsortbb16in.17(A,B,C,D) -> evalrealheapsortbb9in.20(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] evalrealheapsortbb17in.18(A,B,C,D) -> evalrealheapsortbb18in.13(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb17in.18(A,B,C,D) -> evalrealheapsortbb18in.14(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb9in.19(A,B,C,D) -> evalrealheapsortbb10in.21(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] evalrealheapsortbb9in.19(A,B,C,D) -> evalrealheapsortbb10in.22(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] evalrealheapsortbb9in.20(A,B,C,D) -> evalrealheapsortbb11in.23(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A = 3 + B + 2*C] evalrealheapsortbb10in.21(A,B,C,D) -> evalrealheapsortbb12in.26(A,B,C,D) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb10in.22(A,B,C,D) -> evalrealheapsortbb11in.23(A,B,C,D) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb11in.23(A,B,C,D) -> evalrealheapsortbb13in.24(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb11in.23(A,B,C,D) -> evalrealheapsortbb13in.25(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb13in.24(A,B,C,D) -> evalrealheapsortbb16in.16(A,B,A,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb13in.25(A,B,C,D) -> evalrealheapsortbb14in.27(A,B,C,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb12in.26(A,B,C,D) -> evalrealheapsortbb13in.24(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb12in.26(A,B,C,D) -> evalrealheapsortbb13in.25(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb14in.27(A,B,C,D) -> evalrealheapsortbb16in.16(A,B,D,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb14in.27(A,B,C,D) -> evalrealheapsortbb16in.17(A,B,D,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] Signature: {(evalrealheapsortbb10in.21,4) ;(evalrealheapsortbb10in.22,4) ;(evalrealheapsortbb11in.23,4) ;(evalrealheapsortbb12in.26,4) ;(evalrealheapsortbb13in.24,4) ;(evalrealheapsortbb13in.25,4) ;(evalrealheapsortbb14in.27,4) ;(evalrealheapsortbb16in.16,4) ;(evalrealheapsortbb16in.17,4) ;(evalrealheapsortbb17in.18,4) ;(evalrealheapsortbb18in.13,4) ;(evalrealheapsortbb18in.14,4) ;(evalrealheapsortbb2in.11,4) ;(evalrealheapsortbb3in.5,4) ;(evalrealheapsortbb3in.6,4) ;(evalrealheapsortbb4in.7,4) ;(evalrealheapsortbb4in.8,4) ;(evalrealheapsortbb5in.9,4) ;(evalrealheapsortbb6in.10,4) ;(evalrealheapsortbb6in.4,4) ;(evalrealheapsortbb7in.12,4) ;(evalrealheapsortbb8in.15,4) ;(evalrealheapsortbb9in.19,4) ;(evalrealheapsortbb9in.20,4) ;(evalrealheapsortentryin.1,4) ;(evalrealheapsortentryin.2,4) ;(evalrealheapsortreturnin.3,4) ;(evalrealheapsortstart.0,4) ;(evalrealheapsortstop.28,4)} Rule Graph: [0->{2},1->{3},2->{4},3->{5},4->{},5->{6,7},6->{9},7->{10},8->{11,12},9->{11,12},10->{14,15},11->{5} ,12->{13},13->{16},14->{6,7},15->{8},16->{18},17->{4},18->{19,20},19->{21},20->{22,23},21->{24,25},22->{26 ,27},23->{28},24->{17},25->{18},26->{29},27->{30},28->{31,32},29->{35,36},30->{31,32},31->{33},32->{34} ,33->{21},34->{37,38},35->{33},36->{34},37->{21},38->{22,23}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: evalrealheapsortstart.0(A,B,C,D) -> evalrealheapsortentryin.1(A,B,C,D) True evalrealheapsortstart.0(A,B,C,D) -> evalrealheapsortentryin.2(A,B,C,D) True evalrealheapsortentryin.1(A,B,C,D) -> evalrealheapsortreturnin.3(A,B,C,D) [2 >= A] evalrealheapsortentryin.2(A,B,C,D) -> evalrealheapsortbb6in.4(A,1,C,D) [A >= 3] evalrealheapsortreturnin.3(A,B,C,D) -> evalrealheapsortstop.28(A,B,C,D) True evalrealheapsortbb6in.4(A,B,C,D) -> evalrealheapsortbb3in.5(A,B,B,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && A >= 1 + B] evalrealheapsortbb3in.5(A,B,C,D) -> evalrealheapsortbb4in.7(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] evalrealheapsortbb3in.5(A,B,C,D) -> evalrealheapsortbb4in.8(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] evalrealheapsortbb3in.6(A,B,C,D) -> evalrealheapsortbb5in.9(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && 0 >= C] evalrealheapsortbb4in.7(A,B,C,D) -> evalrealheapsortbb5in.9(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb4in.8(A,B,C,D) -> evalrealheapsortbb2in.11(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb5in.9(A,B,C,D) -> evalrealheapsortbb6in.4(A,1 + B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb5in.9(A,B,C,D) -> evalrealheapsortbb6in.10(A,1 + B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb6in.10(A,B,C,D) -> evalrealheapsortbb7in.12(A,B,C,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && B >= A] evalrealheapsortbb2in.11(A,B,C,D) -> evalrealheapsortbb3in.5(A,B,-1 + E,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && G >= 0 && 1 + C >= 2*G && 2*G >= C && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb2in.11(A,B,C,D) -> evalrealheapsortbb3in.6(A,B,-1 + E,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && G >= 0 && 1 + C >= 2*G && 2*G >= C && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb7in.12(A,B,C,D) -> evalrealheapsortbb18in.14(A,0,C,D) [-3 + B >= 0 && -6 + A + B >= 0 && -1*A + B >= 0 && -3 + A >= 0] evalrealheapsortbb18in.13(A,B,C,D) -> evalrealheapsortreturnin.3(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] evalrealheapsortbb18in.14(A,B,C,D) -> evalrealheapsortbb8in.15(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] evalrealheapsortbb8in.15(A,B,C,D) -> evalrealheapsortbb16in.16(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb8in.15(A,B,C,D) -> evalrealheapsortbb16in.17(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb16in.16(A,B,C,D) -> evalrealheapsortbb17in.18(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 2 + B + 2*C >= A] evalrealheapsortbb16in.17(A,B,C,D) -> evalrealheapsortbb9in.19(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] evalrealheapsortbb16in.17(A,B,C,D) -> evalrealheapsortbb9in.20(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] evalrealheapsortbb17in.18(A,B,C,D) -> evalrealheapsortbb18in.13(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb17in.18(A,B,C,D) -> evalrealheapsortbb18in.14(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb9in.19(A,B,C,D) -> evalrealheapsortbb10in.21(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] evalrealheapsortbb9in.19(A,B,C,D) -> evalrealheapsortbb10in.22(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] evalrealheapsortbb9in.20(A,B,C,D) -> evalrealheapsortbb11in.23(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A = 3 + B + 2*C] evalrealheapsortbb10in.21(A,B,C,D) -> evalrealheapsortbb12in.26(A,B,C,D) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb10in.22(A,B,C,D) -> evalrealheapsortbb11in.23(A,B,C,D) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb11in.23(A,B,C,D) -> evalrealheapsortbb13in.24(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb11in.23(A,B,C,D) -> evalrealheapsortbb13in.25(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb13in.24(A,B,C,D) -> evalrealheapsortbb16in.16(A,B,A,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb13in.25(A,B,C,D) -> evalrealheapsortbb14in.27(A,B,C,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb12in.26(A,B,C,D) -> evalrealheapsortbb13in.24(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb12in.26(A,B,C,D) -> evalrealheapsortbb13in.25(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb14in.27(A,B,C,D) -> evalrealheapsortbb16in.16(A,B,D,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb14in.27(A,B,C,D) -> evalrealheapsortbb16in.17(A,B,D,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstop.28(A,B,C,D) -> exitus616(A,B,C,D) True evalrealheapsortstop.28(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(evalrealheapsortbb10in.21,4) ;(evalrealheapsortbb10in.22,4) ;(evalrealheapsortbb11in.23,4) ;(evalrealheapsortbb12in.26,4) ;(evalrealheapsortbb13in.24,4) ;(evalrealheapsortbb13in.25,4) ;(evalrealheapsortbb14in.27,4) ;(evalrealheapsortbb16in.16,4) ;(evalrealheapsortbb16in.17,4) ;(evalrealheapsortbb17in.18,4) ;(evalrealheapsortbb18in.13,4) ;(evalrealheapsortbb18in.14,4) ;(evalrealheapsortbb2in.11,4) ;(evalrealheapsortbb3in.5,4) ;(evalrealheapsortbb3in.6,4) ;(evalrealheapsortbb4in.7,4) ;(evalrealheapsortbb4in.8,4) ;(evalrealheapsortbb5in.9,4) ;(evalrealheapsortbb6in.10,4) ;(evalrealheapsortbb6in.4,4) ;(evalrealheapsortbb7in.12,4) ;(evalrealheapsortbb8in.15,4) ;(evalrealheapsortbb9in.19,4) ;(evalrealheapsortbb9in.20,4) ;(evalrealheapsortentryin.1,4) ;(evalrealheapsortentryin.2,4) ;(evalrealheapsortreturnin.3,4) ;(evalrealheapsortstart.0,4) ;(evalrealheapsortstop.28,4) ;(exitus616,4)} Rule Graph: [0->{2},1->{3},2->{4},3->{5},4->{39,40},5->{6,7},6->{9},7->{10},8->{11,12},9->{11,12},10->{14,15},11->{5} ,12->{13},13->{16},14->{6,7},15->{8},16->{18},17->{4},18->{19,20},19->{21},20->{22,23},21->{24,25},22->{26 ,27},23->{28},24->{17},25->{18},26->{29},27->{30},28->{31,32},29->{35,36},30->{31,32},31->{33},32->{34} ,33->{21},34->{37,38},35->{33},36->{34},37->{21},38->{22,23}] + 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] | +- p:[5,11,8,15,10,7,14,9,6] c: [5,6,8,9,11,15] | | | `- p:[7,14,10] c: [7,10,14] | `- p:[18,25,21,19,33,31,28,23,20,38,34,32,30,27,22,36,29,26,35,37] c: [18,19,20,21,25,31,33,35,37] | `- p:[22,38,34,32,28,23,30,27,36,29,26] c: [22,23,26,27,28,29,30,32,34,36,38] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: evalrealheapsortstart.0(A,B,C,D) -> evalrealheapsortentryin.1(A,B,C,D) True evalrealheapsortstart.0(A,B,C,D) -> evalrealheapsortentryin.2(A,B,C,D) True evalrealheapsortentryin.1(A,B,C,D) -> evalrealheapsortreturnin.3(A,B,C,D) [2 >= A] evalrealheapsortentryin.2(A,B,C,D) -> evalrealheapsortbb6in.4(A,1,C,D) [A >= 3] evalrealheapsortreturnin.3(A,B,C,D) -> evalrealheapsortstop.28(A,B,C,D) True evalrealheapsortbb6in.4(A,B,C,D) -> evalrealheapsortbb3in.5(A,B,B,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && A >= 1 + B] evalrealheapsortbb3in.5(A,B,C,D) -> evalrealheapsortbb4in.7(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] evalrealheapsortbb3in.5(A,B,C,D) -> evalrealheapsortbb4in.8(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] evalrealheapsortbb3in.6(A,B,C,D) -> evalrealheapsortbb5in.9(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && 0 >= C] evalrealheapsortbb4in.7(A,B,C,D) -> evalrealheapsortbb5in.9(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb4in.8(A,B,C,D) -> evalrealheapsortbb2in.11(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb5in.9(A,B,C,D) -> evalrealheapsortbb6in.4(A,1 + B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb5in.9(A,B,C,D) -> evalrealheapsortbb6in.10(A,1 + B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb6in.10(A,B,C,D) -> evalrealheapsortbb7in.12(A,B,C,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && B >= A] evalrealheapsortbb2in.11(A,B,C,D) -> evalrealheapsortbb3in.5(A,B,-1 + E,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && G >= 0 && 1 + C >= 2*G && 2*G >= C && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb2in.11(A,B,C,D) -> evalrealheapsortbb3in.6(A,B,-1 + E,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && G >= 0 && 1 + C >= 2*G && 2*G >= C && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb7in.12(A,B,C,D) -> evalrealheapsortbb18in.14(A,0,C,D) [-3 + B >= 0 && -6 + A + B >= 0 && -1*A + B >= 0 && -3 + A >= 0] evalrealheapsortbb18in.13(A,B,C,D) -> evalrealheapsortreturnin.3(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] evalrealheapsortbb18in.14(A,B,C,D) -> evalrealheapsortbb8in.15(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] evalrealheapsortbb8in.15(A,B,C,D) -> evalrealheapsortbb16in.16(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb8in.15(A,B,C,D) -> evalrealheapsortbb16in.17(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb16in.16(A,B,C,D) -> evalrealheapsortbb17in.18(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 2 + B + 2*C >= A] evalrealheapsortbb16in.17(A,B,C,D) -> evalrealheapsortbb9in.19(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] evalrealheapsortbb16in.17(A,B,C,D) -> evalrealheapsortbb9in.20(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] evalrealheapsortbb17in.18(A,B,C,D) -> evalrealheapsortbb18in.13(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb17in.18(A,B,C,D) -> evalrealheapsortbb18in.14(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb9in.19(A,B,C,D) -> evalrealheapsortbb10in.21(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] evalrealheapsortbb9in.19(A,B,C,D) -> evalrealheapsortbb10in.22(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] evalrealheapsortbb9in.20(A,B,C,D) -> evalrealheapsortbb11in.23(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A = 3 + B + 2*C] evalrealheapsortbb10in.21(A,B,C,D) -> evalrealheapsortbb12in.26(A,B,C,D) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb10in.22(A,B,C,D) -> evalrealheapsortbb11in.23(A,B,C,D) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb11in.23(A,B,C,D) -> evalrealheapsortbb13in.24(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb11in.23(A,B,C,D) -> evalrealheapsortbb13in.25(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb13in.24(A,B,C,D) -> evalrealheapsortbb16in.16(A,B,A,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb13in.25(A,B,C,D) -> evalrealheapsortbb14in.27(A,B,C,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb12in.26(A,B,C,D) -> evalrealheapsortbb13in.24(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb12in.26(A,B,C,D) -> evalrealheapsortbb13in.25(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb14in.27(A,B,C,D) -> evalrealheapsortbb16in.16(A,B,D,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb14in.27(A,B,C,D) -> evalrealheapsortbb16in.17(A,B,D,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstop.28(A,B,C,D) -> exitus616(A,B,C,D) True evalrealheapsortstop.28(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(evalrealheapsortbb10in.21,4) ;(evalrealheapsortbb10in.22,4) ;(evalrealheapsortbb11in.23,4) ;(evalrealheapsortbb12in.26,4) ;(evalrealheapsortbb13in.24,4) ;(evalrealheapsortbb13in.25,4) ;(evalrealheapsortbb14in.27,4) ;(evalrealheapsortbb16in.16,4) ;(evalrealheapsortbb16in.17,4) ;(evalrealheapsortbb17in.18,4) ;(evalrealheapsortbb18in.13,4) ;(evalrealheapsortbb18in.14,4) ;(evalrealheapsortbb2in.11,4) ;(evalrealheapsortbb3in.5,4) ;(evalrealheapsortbb3in.6,4) ;(evalrealheapsortbb4in.7,4) ;(evalrealheapsortbb4in.8,4) ;(evalrealheapsortbb5in.9,4) ;(evalrealheapsortbb6in.10,4) ;(evalrealheapsortbb6in.4,4) ;(evalrealheapsortbb7in.12,4) ;(evalrealheapsortbb8in.15,4) ;(evalrealheapsortbb9in.19,4) ;(evalrealheapsortbb9in.20,4) ;(evalrealheapsortentryin.1,4) ;(evalrealheapsortentryin.2,4) ;(evalrealheapsortreturnin.3,4) ;(evalrealheapsortstart.0,4) ;(evalrealheapsortstop.28,4) ;(exitus616,4)} Rule Graph: [0->{2},1->{3},2->{4},3->{5},4->{39,40},5->{6,7},6->{9},7->{10},8->{11,12},9->{11,12},10->{14,15},11->{5} ,12->{13},13->{16},14->{6,7},15->{8},16->{18},17->{4},18->{19,20},19->{21},20->{22,23},21->{24,25},22->{26 ,27},23->{28},24->{17},25->{18},26->{29},27->{30},28->{31,32},29->{35,36},30->{31,32},31->{33},32->{34} ,33->{21},34->{37,38},35->{33},36->{34},37->{21},38->{22,23}] ,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] | +- p:[5,11,8,15,10,7,14,9,6] c: [5,6,8,9,11,15] | | | `- p:[7,14,10] c: [7,10,14] | `- p:[18,25,21,19,33,31,28,23,20,38,34,32,30,27,22,36,29,26,35,37] c: [18,19,20,21,25,31,33,35,37] | `- p:[22,38,34,32,28,23,30,27,36,29,26] c: [22,23,26,27,28,29,30,32,34,36,38]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.0.0,0.1,0.1.0] evalrealheapsortstart.0 ~> evalrealheapsortentryin.1 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstart.0 ~> evalrealheapsortentryin.2 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortentryin.1 ~> evalrealheapsortreturnin.3 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortentryin.2 ~> evalrealheapsortbb6in.4 [A <= A, B <= K, C <= C, D <= D] evalrealheapsortreturnin.3 ~> evalrealheapsortstop.28 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb6in.4 ~> evalrealheapsortbb3in.5 [A <= A, B <= B, C <= B, D <= D] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.7 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.8 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb3in.6 ~> evalrealheapsortbb5in.9 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb4in.7 ~> evalrealheapsortbb5in.9 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb4in.8 ~> evalrealheapsortbb2in.11 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb5in.9 ~> evalrealheapsortbb6in.4 [A <= A, B <= A, C <= C, D <= D] evalrealheapsortbb5in.9 ~> evalrealheapsortbb6in.10 [A <= A, B <= A, C <= C, D <= D] evalrealheapsortbb6in.10 ~> evalrealheapsortbb7in.12 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.5 [A <= A, B <= B, C <= A, D <= D] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.6 [A <= A, B <= B, C <= A, D <= D] evalrealheapsortbb7in.12 ~> evalrealheapsortbb18in.14 [A <= A, B <= 0*K, C <= C, D <= D] evalrealheapsortbb18in.13 ~> evalrealheapsortreturnin.3 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb18in.14 ~> evalrealheapsortbb8in.15 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb8in.15 ~> evalrealheapsortbb16in.16 [A <= A, B <= B, C <= 0*K, D <= D] evalrealheapsortbb8in.15 ~> evalrealheapsortbb16in.17 [A <= A, B <= B, C <= 0*K, D <= D] evalrealheapsortbb16in.16 ~> evalrealheapsortbb17in.18 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.19 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.20 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb17in.18 ~> evalrealheapsortbb18in.13 [A <= A, B <= A + B, C <= C, D <= D] evalrealheapsortbb17in.18 ~> evalrealheapsortbb18in.14 [A <= A, B <= A + B, C <= C, D <= D] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.21 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.22 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb9in.20 ~> evalrealheapsortbb11in.23 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb10in.21 ~> evalrealheapsortbb12in.26 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb10in.22 ~> evalrealheapsortbb11in.23 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.24 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.25 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb13in.24 ~> evalrealheapsortbb16in.16 [A <= A, B <= B, C <= A, D <= D] evalrealheapsortbb13in.25 ~> evalrealheapsortbb14in.27 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.24 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.25 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.16 [A <= A, B <= B, C <= D, D <= D] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.17 [A <= A, B <= B, C <= D, D <= D] evalrealheapsortstop.28 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstop.28 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= K + A + B] evalrealheapsortbb6in.4 ~> evalrealheapsortbb3in.5 [A <= A, B <= B, C <= B, D <= D] evalrealheapsortbb5in.9 ~> evalrealheapsortbb6in.4 [A <= A, B <= A, C <= C, D <= D] evalrealheapsortbb3in.6 ~> evalrealheapsortbb5in.9 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.6 [A <= A, B <= B, C <= A, D <= D] evalrealheapsortbb4in.8 ~> evalrealheapsortbb2in.11 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.8 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.5 [A <= A, B <= B, C <= A, D <= D] evalrealheapsortbb4in.7 ~> evalrealheapsortbb5in.9 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.7 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0.0 <= K + 4*C] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.8 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.5 [A <= A, B <= B, C <= A, D <= D] evalrealheapsortbb4in.8 ~> evalrealheapsortbb2in.11 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.1 <= K + A + B] evalrealheapsortbb18in.14 ~> evalrealheapsortbb8in.15 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb17in.18 ~> evalrealheapsortbb18in.14 [A <= A, B <= A + B, C <= C, D <= D] evalrealheapsortbb16in.16 ~> evalrealheapsortbb17in.18 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb8in.15 ~> evalrealheapsortbb16in.16 [A <= A, B <= B, C <= 0*K, D <= D] evalrealheapsortbb13in.24 ~> evalrealheapsortbb16in.16 [A <= A, B <= B, C <= A, D <= D] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.24 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb9in.20 ~> evalrealheapsortbb11in.23 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.20 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb8in.15 ~> evalrealheapsortbb16in.17 [A <= A, B <= B, C <= 0*K, D <= D] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.17 [A <= A, B <= B, C <= D, D <= D] evalrealheapsortbb13in.25 ~> evalrealheapsortbb14in.27 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.25 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb10in.22 ~> evalrealheapsortbb11in.23 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.22 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.19 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.25 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb10in.21 ~> evalrealheapsortbb12in.26 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.21 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.24 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.16 [A <= A, B <= B, C <= D, D <= D] + Loop: [0.1.0 <= 3*K + A + C] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.19 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.17 [A <= A, B <= B, C <= D, D <= D] evalrealheapsortbb13in.25 ~> evalrealheapsortbb14in.27 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.25 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb9in.20 ~> evalrealheapsortbb11in.23 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.20 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb10in.22 ~> evalrealheapsortbb11in.23 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.22 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.25 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb10in.21 ~> evalrealheapsortbb12in.26 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.21 [A <= A, B <= B, C <= C, D <= D] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,0.0,0.0.0,0.1,0.1.0] evalrealheapsortstart.0 ~> evalrealheapsortentryin.1 [] evalrealheapsortstart.0 ~> evalrealheapsortentryin.2 [] evalrealheapsortentryin.1 ~> evalrealheapsortreturnin.3 [] evalrealheapsortentryin.2 ~> evalrealheapsortbb6in.4 [K ~=> B] evalrealheapsortreturnin.3 ~> evalrealheapsortstop.28 [] evalrealheapsortbb6in.4 ~> evalrealheapsortbb3in.5 [B ~=> C] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.7 [] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.8 [] evalrealheapsortbb3in.6 ~> evalrealheapsortbb5in.9 [] evalrealheapsortbb4in.7 ~> evalrealheapsortbb5in.9 [] evalrealheapsortbb4in.8 ~> evalrealheapsortbb2in.11 [] evalrealheapsortbb5in.9 ~> evalrealheapsortbb6in.4 [A ~=> B] evalrealheapsortbb5in.9 ~> evalrealheapsortbb6in.10 [A ~=> B] evalrealheapsortbb6in.10 ~> evalrealheapsortbb7in.12 [] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.5 [A ~=> C] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.6 [A ~=> C] evalrealheapsortbb7in.12 ~> evalrealheapsortbb18in.14 [K ~=> B] evalrealheapsortbb18in.13 ~> evalrealheapsortreturnin.3 [] evalrealheapsortbb18in.14 ~> evalrealheapsortbb8in.15 [] evalrealheapsortbb8in.15 ~> evalrealheapsortbb16in.16 [K ~=> C] evalrealheapsortbb8in.15 ~> evalrealheapsortbb16in.17 [K ~=> C] evalrealheapsortbb16in.16 ~> evalrealheapsortbb17in.18 [] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.19 [] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.20 [] evalrealheapsortbb17in.18 ~> evalrealheapsortbb18in.13 [A ~+> B,B ~+> B] evalrealheapsortbb17in.18 ~> evalrealheapsortbb18in.14 [A ~+> B,B ~+> B] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.21 [] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.22 [] evalrealheapsortbb9in.20 ~> evalrealheapsortbb11in.23 [] evalrealheapsortbb10in.21 ~> evalrealheapsortbb12in.26 [] evalrealheapsortbb10in.22 ~> evalrealheapsortbb11in.23 [] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.24 [A ~+> D,C ~+> D] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.25 [A ~+> D,C ~+> D] evalrealheapsortbb13in.24 ~> evalrealheapsortbb16in.16 [A ~=> C] evalrealheapsortbb13in.25 ~> evalrealheapsortbb14in.27 [] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.24 [A ~+> D,C ~+> D] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.25 [A ~+> D,C ~+> D] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.16 [D ~=> C] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.17 [D ~=> C] evalrealheapsortstop.28 ~> exitus616 [] evalrealheapsortstop.28 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] evalrealheapsortbb6in.4 ~> evalrealheapsortbb3in.5 [B ~=> C] evalrealheapsortbb5in.9 ~> evalrealheapsortbb6in.4 [A ~=> B] evalrealheapsortbb3in.6 ~> evalrealheapsortbb5in.9 [] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.6 [A ~=> C] evalrealheapsortbb4in.8 ~> evalrealheapsortbb2in.11 [] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.8 [] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.5 [A ~=> C] evalrealheapsortbb4in.7 ~> evalrealheapsortbb5in.9 [] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.7 [] + Loop: [K ~+> 0.0.0,C ~*> 0.0.0] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.8 [] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.5 [A ~=> C] evalrealheapsortbb4in.8 ~> evalrealheapsortbb2in.11 [] + Loop: [A ~+> 0.1,B ~+> 0.1,K ~+> 0.1] evalrealheapsortbb18in.14 ~> evalrealheapsortbb8in.15 [] evalrealheapsortbb17in.18 ~> evalrealheapsortbb18in.14 [A ~+> B,B ~+> B] evalrealheapsortbb16in.16 ~> evalrealheapsortbb17in.18 [] evalrealheapsortbb8in.15 ~> evalrealheapsortbb16in.16 [K ~=> C] evalrealheapsortbb13in.24 ~> evalrealheapsortbb16in.16 [A ~=> C] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.24 [A ~+> D,C ~+> D] evalrealheapsortbb9in.20 ~> evalrealheapsortbb11in.23 [] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.20 [] evalrealheapsortbb8in.15 ~> evalrealheapsortbb16in.17 [K ~=> C] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.17 [D ~=> C] evalrealheapsortbb13in.25 ~> evalrealheapsortbb14in.27 [] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.25 [A ~+> D,C ~+> D] evalrealheapsortbb10in.22 ~> evalrealheapsortbb11in.23 [] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.22 [] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.19 [] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.25 [A ~+> D,C ~+> D] evalrealheapsortbb10in.21 ~> evalrealheapsortbb12in.26 [] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.21 [] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.24 [A ~+> D,C ~+> D] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.16 [D ~=> C] + Loop: [A ~+> 0.1.0,C ~+> 0.1.0,K ~*> 0.1.0] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.19 [] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.17 [D ~=> C] evalrealheapsortbb13in.25 ~> evalrealheapsortbb14in.27 [] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.25 [A ~+> D,C ~+> D] evalrealheapsortbb9in.20 ~> evalrealheapsortbb11in.23 [] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.20 [] evalrealheapsortbb10in.22 ~> evalrealheapsortbb11in.23 [] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.22 [] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.25 [A ~+> D,C ~+> D] evalrealheapsortbb10in.21 ~> evalrealheapsortbb12in.26 [] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.21 [] + Applied Processor: Lare + Details: evalrealheapsortstart.0 ~> exitus616 [A ~=> C ,D ~=> C ,K ~=> C ,A ~+> B ,A ~+> C ,A ~+> D ,A ~+> 0.0 ,A ~+> 0.1 ,A ~+> 0.1.0 ,A ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> tick ,A ~*> B ,A ~*> C ,A ~*> D ,A ~*> 0.0.0 ,A ~*> tick ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> tick] + evalrealheapsortbb5in.9> [A ~=> B ,A ~=> C ,B ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> 0.0.0 ,B ~*> tick ,K ~*> tick] + evalrealheapsortbb3in.5> [A ~=> C ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,C ~*> 0.0.0 ,C ~*> tick] evalrealheapsortbb2in.11> [A ~=> C ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,C ~*> 0.0.0 ,C ~*> tick] + evalrealheapsortbb17in.18> [A ~=> C ,D ~=> C ,K ~=> C ,A ~+> B ,A ~+> C ,A ~+> D ,A ~+> 0.1 ,A ~+> 0.1.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.1 ,B ~+> tick ,tick ~+> tick ,K ~+> C ,K ~+> D ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> tick ,A ~*> B ,A ~*> C ,A ~*> D ,A ~*> tick ,B ~*> B ,B ~*> tick ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> 0.1.0 ,K ~*> tick] + evalrealheapsortbb12in.26> [A ~+> C ,A ~+> D ,A ~+> 0.1.0 ,A ~+> tick ,C ~+> C ,C ~+> D ,C ~+> 0.1.0 ,C ~+> tick ,tick ~+> tick ,A ~*> C ,A ~*> D ,C ~*> C ,C ~*> D ,K ~*> C ,K ~*> D ,K ~*> 0.1.0 ,K ~*> tick] evalrealheapsortbb14in.27> [A ~+> C ,A ~+> D ,A ~+> 0.1.0 ,A ~+> tick ,C ~+> C ,C ~+> D ,C ~+> 0.1.0 ,C ~+> tick ,tick ~+> tick ,A ~*> C ,A ~*> D ,C ~*> C ,C ~*> D ,K ~*> C ,K ~*> D ,K ~*> 0.1.0 ,K ~*> tick] evalrealheapsortbb11in.23> [A ~+> C ,A ~+> D ,A ~+> 0.1.0 ,A ~+> tick ,C ~+> C ,C ~+> D ,C ~+> 0.1.0 ,C ~+> tick ,tick ~+> tick ,A ~*> C ,A ~*> D ,C ~*> C ,C ~*> D ,K ~*> C ,K ~*> D ,K ~*> 0.1.0 ,K ~*> tick] YES(?,POLY)