YES(?,POLY) * Step 1: TrivialSCCs WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealshellsortstart(A,B,C,D,E) -> evalrealshellsortentryin(A,B,C,D,E) True (1,1) 1. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,0,C,D,E) [A = 0] (?,1) 2. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [A >= 1 && F >= 0 && A >= 2*F && 1 + 2*F >= A] (?,1) 3. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [0 >= 1 + A && 0 >= F && 2*F >= A && 1 + A >= 2*F] (?,1) 4. evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,0,D,E) [B >= 1] (?,1) 5. evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortreturnin(A,B,C,D,E) [0 >= B] (?,1) 6. evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb1in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && A >= 1 + C] (?,1) 7. evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb7in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && C >= A] (?,1) 8. evalrealshellsortbb1in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,F,C) [-1 + A + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 9. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + E] 10. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb4in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= B] 11. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb2in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && F >= 1 + D] 12. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && D >= F] 13. evalrealshellsortbb2in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,D,-1*B + E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] 14. evalrealshellsortbb5in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,1 + C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 15. evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1*A + C >= 0 && -1 + B >= 0 && B >= 1 && F >= 0 && B >= 2*F && 1 + 2*F >= B] (?,1) 16. evalrealshellsortreturnin(A,B,C,D,E) -> evalrealshellsortstop(A,B,C,D,E) [-1*B >= 0] (?,1) Signature: {(evalrealshellsortbb1in,5) ;(evalrealshellsortbb2in,5) ;(evalrealshellsortbb3in,5) ;(evalrealshellsortbb4in,5) ;(evalrealshellsortbb5in,5) ;(evalrealshellsortbb6in,5) ;(evalrealshellsortbb7in,5) ;(evalrealshellsortbb8in,5) ;(evalrealshellsortentryin,5) ;(evalrealshellsortreturnin,5) ;(evalrealshellsortstart,5) ;(evalrealshellsortstop,5)} Flow Graph: [0->{1,2,3},1->{4,5},2->{4,5},3->{4,5},4->{6,7},5->{16},6->{8},7->{15},8->{9,10},9->{14},10->{11,12} ,11->{13},12->{14},13->{9,10},14->{6,7},15->{4,5},16->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealshellsortstart(A,B,C,D,E) -> evalrealshellsortentryin(A,B,C,D,E) True (1,1) 1. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,0,C,D,E) [A = 0] (1,1) 2. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [A >= 1 && F >= 0 && A >= 2*F && 1 + 2*F >= A] (1,1) 3. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [0 >= 1 + A && 0 >= F && 2*F >= A && 1 + A >= 2*F] (1,1) 4. evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,0,D,E) [B >= 1] (?,1) 5. evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortreturnin(A,B,C,D,E) [0 >= B] (1,1) 6. evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb1in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && A >= 1 + C] (?,1) 7. evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb7in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && C >= A] (?,1) 8. evalrealshellsortbb1in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,F,C) [-1 + A + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 9. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + E] 10. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb4in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= B] 11. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb2in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && F >= 1 + D] 12. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && D >= F] 13. evalrealshellsortbb2in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,D,-1*B + E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] 14. evalrealshellsortbb5in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,1 + C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 15. evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1*A + C >= 0 && -1 + B >= 0 && B >= 1 && F >= 0 && B >= 2*F && 1 + 2*F >= B] (?,1) 16. evalrealshellsortreturnin(A,B,C,D,E) -> evalrealshellsortstop(A,B,C,D,E) [-1*B >= 0] (1,1) Signature: {(evalrealshellsortbb1in,5) ;(evalrealshellsortbb2in,5) ;(evalrealshellsortbb3in,5) ;(evalrealshellsortbb4in,5) ;(evalrealshellsortbb5in,5) ;(evalrealshellsortbb6in,5) ;(evalrealshellsortbb7in,5) ;(evalrealshellsortbb8in,5) ;(evalrealshellsortentryin,5) ;(evalrealshellsortreturnin,5) ;(evalrealshellsortstart,5) ;(evalrealshellsortstop,5)} Flow Graph: [0->{1,2,3},1->{4,5},2->{4,5},3->{4,5},4->{6,7},5->{16},6->{8},7->{15},8->{9,10},9->{14},10->{11,12} ,11->{13},12->{14},13->{9,10},14->{6,7},15->{4,5},16->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,4),(3,4)] * Step 3: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealshellsortstart(A,B,C,D,E) -> evalrealshellsortentryin(A,B,C,D,E) True (1,1) 1. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,0,C,D,E) [A = 0] (1,1) 2. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [A >= 1 && F >= 0 && A >= 2*F && 1 + 2*F >= A] (1,1) 3. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [0 >= 1 + A && 0 >= F && 2*F >= A && 1 + A >= 2*F] (1,1) 4. evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,0,D,E) [B >= 1] (?,1) 5. evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortreturnin(A,B,C,D,E) [0 >= B] (1,1) 6. evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb1in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && A >= 1 + C] (?,1) 7. evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb7in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && C >= A] (?,1) 8. evalrealshellsortbb1in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,F,C) [-1 + A + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 9. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + E] 10. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb4in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= B] 11. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb2in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && F >= 1 + D] 12. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && D >= F] 13. evalrealshellsortbb2in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,D,-1*B + E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] 14. evalrealshellsortbb5in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,1 + C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 15. evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1*A + C >= 0 && -1 + B >= 0 && B >= 1 && F >= 0 && B >= 2*F && 1 + 2*F >= B] (?,1) 16. evalrealshellsortreturnin(A,B,C,D,E) -> evalrealshellsortstop(A,B,C,D,E) [-1*B >= 0] (1,1) Signature: {(evalrealshellsortbb1in,5) ;(evalrealshellsortbb2in,5) ;(evalrealshellsortbb3in,5) ;(evalrealshellsortbb4in,5) ;(evalrealshellsortbb5in,5) ;(evalrealshellsortbb6in,5) ;(evalrealshellsortbb7in,5) ;(evalrealshellsortbb8in,5) ;(evalrealshellsortentryin,5) ;(evalrealshellsortreturnin,5) ;(evalrealshellsortstart,5) ;(evalrealshellsortstop,5)} Flow Graph: [0->{1,2,3},1->{5},2->{4,5},3->{5},4->{6,7},5->{16},6->{8},7->{15},8->{9,10},9->{14},10->{11,12},11->{13} ,12->{14},13->{9,10},14->{6,7},15->{4,5},16->{}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealshellsortstart(A,B,C,D,E) -> evalrealshellsortentryin(A,B,C,D,E) True (1,1) 1. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,0,C,D,E) [A = 0] (?,1) 2. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [A >= 1 && F >= 0 && A >= 2*F && 1 + 2*F >= A] (?,1) 3. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [0 >= 1 + A && 0 >= F && 2*F >= A && 1 + A >= 2*F] (?,1) 4. evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,0,D,E) [B >= 1] (?,1) 5. evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortreturnin(A,B,C,D,E) [0 >= B] (?,1) 6. evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb1in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && A >= 1 + C] (?,1) 7. evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb7in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && C >= A] (?,1) 8. evalrealshellsortbb1in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,F,C) [-1 + A + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 9. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + E] 10. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb4in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= B] 11. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb2in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && F >= 1 + D] 12. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && D >= F] 13. evalrealshellsortbb2in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,D,-1*B + E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] 14. evalrealshellsortbb5in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,1 + C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 15. evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1*A + C >= 0 && -1 + B >= 0 && B >= 1 && F >= 0 && B >= 2*F && 1 + 2*F >= B] (?,1) 16. evalrealshellsortreturnin(A,B,C,D,E) -> evalrealshellsortstop(A,B,C,D,E) [-1*B >= 0] (?,1) 17. evalrealshellsortreturnin(A,B,C,D,E) -> exitus616(A,B,C,D,E) True (?,1) Signature: {(evalrealshellsortbb1in,5) ;(evalrealshellsortbb2in,5) ;(evalrealshellsortbb3in,5) ;(evalrealshellsortbb4in,5) ;(evalrealshellsortbb5in,5) ;(evalrealshellsortbb6in,5) ;(evalrealshellsortbb7in,5) ;(evalrealshellsortbb8in,5) ;(evalrealshellsortentryin,5) ;(evalrealshellsortreturnin,5) ;(evalrealshellsortstart,5) ;(evalrealshellsortstop,5) ;(exitus616,5)} Flow Graph: [0->{1,2,3},1->{4,5},2->{4,5},3->{4,5},4->{6,7},5->{16,17},6->{8},7->{15},8->{9,10},9->{14},10->{11,12} ,11->{13},12->{14},13->{9,10},14->{6,7},15->{4,5},16->{},17->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,4),(3,4)] * Step 5: LooptreeTransformer WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealshellsortstart(A,B,C,D,E) -> evalrealshellsortentryin(A,B,C,D,E) True (1,1) 1. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,0,C,D,E) [A = 0] (?,1) 2. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [A >= 1 && F >= 0 && A >= 2*F && 1 + 2*F >= A] (?,1) 3. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [0 >= 1 + A && 0 >= F && 2*F >= A && 1 + A >= 2*F] (?,1) 4. evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,0,D,E) [B >= 1] (?,1) 5. evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortreturnin(A,B,C,D,E) [0 >= B] (?,1) 6. evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb1in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && A >= 1 + C] (?,1) 7. evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb7in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && C >= A] (?,1) 8. evalrealshellsortbb1in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,F,C) [-1 + A + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 9. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + E] 10. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb4in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= B] 11. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb2in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && F >= 1 + D] 12. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && D >= F] 13. evalrealshellsortbb2in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,D,-1*B + E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] 14. evalrealshellsortbb5in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,1 + C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 15. evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1*A + C >= 0 && -1 + B >= 0 && B >= 1 && F >= 0 && B >= 2*F && 1 + 2*F >= B] (?,1) 16. evalrealshellsortreturnin(A,B,C,D,E) -> evalrealshellsortstop(A,B,C,D,E) [-1*B >= 0] (?,1) 17. evalrealshellsortreturnin(A,B,C,D,E) -> exitus616(A,B,C,D,E) True (?,1) Signature: {(evalrealshellsortbb1in,5) ;(evalrealshellsortbb2in,5) ;(evalrealshellsortbb3in,5) ;(evalrealshellsortbb4in,5) ;(evalrealshellsortbb5in,5) ;(evalrealshellsortbb6in,5) ;(evalrealshellsortbb7in,5) ;(evalrealshellsortbb8in,5) ;(evalrealshellsortentryin,5) ;(evalrealshellsortreturnin,5) ;(evalrealshellsortstart,5) ;(evalrealshellsortstop,5) ;(exitus616,5)} Flow Graph: [0->{1,2,3},1->{5},2->{4,5},3->{5},4->{6,7},5->{16,17},6->{8},7->{15},8->{9,10},9->{14},10->{11,12} ,11->{13},12->{14},13->{9,10},14->{6,7},15->{4,5},16->{},17->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17] | `- p:[4,15,7,14,9,8,6,13,11,10,12] c: [15] | `- p:[6,14,9,8,13,11,10,12] c: [14] | `- p:[10,13,11] c: [13] * Step 6: SizeAbstraction WORST_CASE(?,POLY) + Considered Problem: (Rules: 0. evalrealshellsortstart(A,B,C,D,E) -> evalrealshellsortentryin(A,B,C,D,E) True (1,1) 1. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,0,C,D,E) [A = 0] (?,1) 2. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [A >= 1 && F >= 0 && A >= 2*F && 1 + 2*F >= A] (?,1) 3. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [0 >= 1 + A && 0 >= F && 2*F >= A && 1 + A >= 2*F] (?,1) 4. evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,0,D,E) [B >= 1] (?,1) 5. evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortreturnin(A,B,C,D,E) [0 >= B] (?,1) 6. evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb1in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && A >= 1 + C] (?,1) 7. evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb7in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && C >= A] (?,1) 8. evalrealshellsortbb1in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,F,C) [-1 + A + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 9. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + E] 10. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb4in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= B] 11. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb2in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && F >= 1 + D] 12. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && D >= F] 13. evalrealshellsortbb2in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,D,-1*B + E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] 14. evalrealshellsortbb5in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,1 + C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 15. evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1*A + C >= 0 && -1 + B >= 0 && B >= 1 && F >= 0 && B >= 2*F && 1 + 2*F >= B] (?,1) 16. evalrealshellsortreturnin(A,B,C,D,E) -> evalrealshellsortstop(A,B,C,D,E) [-1*B >= 0] (?,1) 17. evalrealshellsortreturnin(A,B,C,D,E) -> exitus616(A,B,C,D,E) True (?,1) Signature: {(evalrealshellsortbb1in,5) ;(evalrealshellsortbb2in,5) ;(evalrealshellsortbb3in,5) ;(evalrealshellsortbb4in,5) ;(evalrealshellsortbb5in,5) ;(evalrealshellsortbb6in,5) ;(evalrealshellsortbb7in,5) ;(evalrealshellsortbb8in,5) ;(evalrealshellsortentryin,5) ;(evalrealshellsortreturnin,5) ;(evalrealshellsortstart,5) ;(evalrealshellsortstop,5) ;(exitus616,5)} Flow Graph: [0->{1,2,3},1->{5},2->{4,5},3->{5},4->{6,7},5->{16,17},6->{8},7->{15},8->{9,10},9->{14},10->{11,12} ,11->{13},12->{14},13->{9,10},14->{6,7},15->{4,5},16->{},17->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17] | `- p:[4,15,7,14,9,8,6,13,11,10,12] c: [15] | `- p:[6,14,9,8,13,11,10,12] c: [14] | `- p:[10,13,11] c: [13]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,E,0.0,0.0.0,0.0.0.0] evalrealshellsortstart ~> evalrealshellsortentryin [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortentryin ~> evalrealshellsortbb8in [A <= A, B <= 0*K, C <= C, D <= D, E <= E] evalrealshellsortentryin ~> evalrealshellsortbb8in [A <= A, B <= A, C <= C, D <= D, E <= E] evalrealshellsortentryin ~> evalrealshellsortbb8in [A <= A, B <= A, C <= C, D <= D, E <= E] evalrealshellsortbb8in ~> evalrealshellsortbb6in [A <= A, B <= B, C <= 0*K, D <= D, E <= E] evalrealshellsortbb8in ~> evalrealshellsortreturnin [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb6in ~> evalrealshellsortbb1in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb6in ~> evalrealshellsortbb7in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb1in ~> evalrealshellsortbb3in [A <= A, B <= B, C <= C, D <= unknown, E <= C] evalrealshellsortbb3in ~> evalrealshellsortbb5in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb3in ~> evalrealshellsortbb4in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb4in ~> evalrealshellsortbb2in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb4in ~> evalrealshellsortbb5in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb2in ~> evalrealshellsortbb3in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb5in ~> evalrealshellsortbb6in [A <= A, B <= B, C <= A, D <= D, E <= E] evalrealshellsortbb7in ~> evalrealshellsortbb8in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortreturnin ~> evalrealshellsortstop [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortreturnin ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E] + Loop: [0.0 <= K + 2*B] evalrealshellsortbb8in ~> evalrealshellsortbb6in [A <= A, B <= B, C <= 0*K, D <= D, E <= E] evalrealshellsortbb7in ~> evalrealshellsortbb8in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb6in ~> evalrealshellsortbb7in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb5in ~> evalrealshellsortbb6in [A <= A, B <= B, C <= A, D <= D, E <= E] evalrealshellsortbb3in ~> evalrealshellsortbb5in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb1in ~> evalrealshellsortbb3in [A <= A, B <= B, C <= C, D <= unknown, E <= C] evalrealshellsortbb6in ~> evalrealshellsortbb1in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb2in ~> evalrealshellsortbb3in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb4in ~> evalrealshellsortbb2in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb3in ~> evalrealshellsortbb4in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb4in ~> evalrealshellsortbb5in [A <= A, B <= B, C <= C, D <= D, E <= E] + Loop: [0.0.0 <= A + C] evalrealshellsortbb6in ~> evalrealshellsortbb1in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb5in ~> evalrealshellsortbb6in [A <= A, B <= B, C <= A, D <= D, E <= E] evalrealshellsortbb3in ~> evalrealshellsortbb5in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb1in ~> evalrealshellsortbb3in [A <= A, B <= B, C <= C, D <= unknown, E <= C] evalrealshellsortbb2in ~> evalrealshellsortbb3in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb4in ~> evalrealshellsortbb2in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb3in ~> evalrealshellsortbb4in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb4in ~> evalrealshellsortbb5in [A <= A, B <= B, C <= C, D <= D, E <= E] + Loop: [0.0.0.0 <= K + B + E] evalrealshellsortbb3in ~> evalrealshellsortbb4in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb2in ~> evalrealshellsortbb3in [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb4in ~> evalrealshellsortbb2in [A <= A, B <= B, C <= C, D <= D, E <= E] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,0.0,0.0.0,0.0.0.0] evalrealshellsortstart ~> evalrealshellsortentryin [] evalrealshellsortentryin ~> evalrealshellsortbb8in [K ~=> B] evalrealshellsortentryin ~> evalrealshellsortbb8in [A ~=> B] evalrealshellsortentryin ~> evalrealshellsortbb8in [A ~=> B] evalrealshellsortbb8in ~> evalrealshellsortbb6in [K ~=> C] evalrealshellsortbb8in ~> evalrealshellsortreturnin [] evalrealshellsortbb6in ~> evalrealshellsortbb1in [] evalrealshellsortbb6in ~> evalrealshellsortbb7in [] evalrealshellsortbb1in ~> evalrealshellsortbb3in [C ~=> E,huge ~=> D] evalrealshellsortbb3in ~> evalrealshellsortbb5in [] evalrealshellsortbb3in ~> evalrealshellsortbb4in [] evalrealshellsortbb4in ~> evalrealshellsortbb2in [] evalrealshellsortbb4in ~> evalrealshellsortbb5in [] evalrealshellsortbb2in ~> evalrealshellsortbb3in [] evalrealshellsortbb5in ~> evalrealshellsortbb6in [A ~=> C] evalrealshellsortbb7in ~> evalrealshellsortbb8in [] evalrealshellsortreturnin ~> evalrealshellsortstop [] evalrealshellsortreturnin ~> exitus616 [] + Loop: [K ~+> 0.0,B ~*> 0.0] evalrealshellsortbb8in ~> evalrealshellsortbb6in [K ~=> C] evalrealshellsortbb7in ~> evalrealshellsortbb8in [] evalrealshellsortbb6in ~> evalrealshellsortbb7in [] evalrealshellsortbb5in ~> evalrealshellsortbb6in [A ~=> C] evalrealshellsortbb3in ~> evalrealshellsortbb5in [] evalrealshellsortbb1in ~> evalrealshellsortbb3in [C ~=> E,huge ~=> D] evalrealshellsortbb6in ~> evalrealshellsortbb1in [] evalrealshellsortbb2in ~> evalrealshellsortbb3in [] evalrealshellsortbb4in ~> evalrealshellsortbb2in [] evalrealshellsortbb3in ~> evalrealshellsortbb4in [] evalrealshellsortbb4in ~> evalrealshellsortbb5in [] + Loop: [A ~+> 0.0.0,C ~+> 0.0.0] evalrealshellsortbb6in ~> evalrealshellsortbb1in [] evalrealshellsortbb5in ~> evalrealshellsortbb6in [A ~=> C] evalrealshellsortbb3in ~> evalrealshellsortbb5in [] evalrealshellsortbb1in ~> evalrealshellsortbb3in [C ~=> E,huge ~=> D] evalrealshellsortbb2in ~> evalrealshellsortbb3in [] evalrealshellsortbb4in ~> evalrealshellsortbb2in [] evalrealshellsortbb3in ~> evalrealshellsortbb4in [] evalrealshellsortbb4in ~> evalrealshellsortbb5in [] + Loop: [B ~+> 0.0.0.0,E ~+> 0.0.0.0,K ~+> 0.0.0.0] evalrealshellsortbb3in ~> evalrealshellsortbb4in [] evalrealshellsortbb2in ~> evalrealshellsortbb3in [] evalrealshellsortbb4in ~> evalrealshellsortbb2in [] + Applied Processor: LareProcessor + Details: evalrealshellsortstart ~> exitus616 [A ~=> B ,A ~=> C ,A ~=> E ,K ~=> B ,K ~=> C ,K ~=> E ,huge ~=> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> tick ,A ~*> 0.0 ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> tick ,K ~*> 0.0 ,K ~*> 0.0.0.0 ,K ~*> tick] evalrealshellsortstart ~> evalrealshellsortstop [A ~=> B ,A ~=> C ,A ~=> E ,K ~=> B ,K ~=> C ,K ~=> E ,huge ~=> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> tick ,A ~*> 0.0 ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> tick ,K ~*> 0.0 ,K ~*> 0.0.0.0 ,K ~*> tick] + evalrealshellsortbb8in> [A ~=> C ,A ~=> E ,K ~=> C ,K ~=> E ,huge ~=> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> tick ,B ~+> 0.0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> tick ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> 0.0 ,B ~*> tick ,K ~*> 0.0.0.0 ,K ~*> tick] + evalrealshellsortbb6in> [A ~=> C ,A ~=> E ,C ~=> E ,huge ~=> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> tick ,B ~+> 0.0.0.0 ,B ~+> tick ,C ~+> 0.0.0 ,C ~+> 0.0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0 ,K ~+> tick ,A ~*> tick ,B ~*> tick ,C ~*> tick ,K ~*> tick] + evalrealshellsortbb4in> [B ~+> 0.0.0.0 ,B ~+> tick ,E ~+> 0.0.0.0 ,E ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0 ,K ~+> tick] evalrealshellsortbb3in> [B ~+> 0.0.0.0 ,B ~+> tick ,E ~+> 0.0.0.0 ,E ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0 ,K ~+> tick] YES(?,POLY)