YES * Step 1: TrivialSCCs YES + 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 YES + 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: Looptree YES + 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: Looptree + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16] | `- 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] YES