NO * Step 1: UnsatPaths NO + 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) [A >= 1 + C] (?,1) 7. evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb7in(A,B,C,D,E) [C >= A] (?,1) 8. evalrealshellsortbb1in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,F,C) True (?,1) 9. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [B >= 1 + E] (?,1) 10. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb4in(A,B,C,D,E) [E >= B] (?,1) 11. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb2in(A,B,C,D,E) [F >= 1 + D] (?,1) 12. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [D >= F] (?,1) 13. evalrealshellsortbb2in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,D,-1*B + E) True (?,1) 14. evalrealshellsortbb5in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,1 + C,D,E) True (?,1) 15. evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,0,C,D,E) [B = 0] (?,1) 16. evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [B >= 1 && F >= 0 && B >= 2*F && 1 + 2*F >= B] (?,1) 17. evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [0 >= 1 + B && 0 >= F && 2*F >= B && 1 + B >= 2*F] (?,1) 18. evalrealshellsortreturnin(A,B,C,D,E) -> evalrealshellsortstop(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)} Flow Graph: [0->{1,2,3},1->{4,5},2->{4,5},3->{4,5},4->{6,7},5->{18},6->{8},7->{15,16,17},8->{9,10},9->{14},10->{11,12} ,11->{13},12->{14},13->{9,10},14->{6,7},15->{4,5},16->{4,5},17->{4,5},18->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,4),(3,4),(15,4),(17,4)] * Step 2: FromIts NO + 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) [A >= 1 + C] (?,1) 7. evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb7in(A,B,C,D,E) [C >= A] (?,1) 8. evalrealshellsortbb1in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,F,C) True (?,1) 9. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [B >= 1 + E] (?,1) 10. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb4in(A,B,C,D,E) [E >= B] (?,1) 11. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb2in(A,B,C,D,E) [F >= 1 + D] (?,1) 12. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [D >= F] (?,1) 13. evalrealshellsortbb2in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,D,-1*B + E) True (?,1) 14. evalrealshellsortbb5in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,1 + C,D,E) True (?,1) 15. evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,0,C,D,E) [B = 0] (?,1) 16. evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [B >= 1 && F >= 0 && B >= 2*F && 1 + 2*F >= B] (?,1) 17. evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [0 >= 1 + B && 0 >= F && 2*F >= B && 1 + B >= 2*F] (?,1) 18. evalrealshellsortreturnin(A,B,C,D,E) -> evalrealshellsortstop(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)} Flow Graph: [0->{1,2,3},1->{5},2->{4,5},3->{5},4->{6,7},5->{18},6->{8},7->{15,16,17},8->{9,10},9->{14},10->{11,12} ,11->{13},12->{14},13->{9,10},14->{6,7},15->{5},16->{4,5},17->{5},18->{}] + Applied Processor: FromIts + Details: () * Step 3: CloseWith NO + Considered Problem: Rules: evalrealshellsortstart(A,B,C,D,E) -> evalrealshellsortentryin(A,B,C,D,E) True evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,0,C,D,E) [A = 0] evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [A >= 1 && F >= 0 && A >= 2*F && 1 + 2*F >= A] evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [0 >= 1 + A && 0 >= F && 2*F >= A && 1 + A >= 2*F] evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,0,D,E) [B >= 1] evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortreturnin(A,B,C,D,E) [0 >= B] evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb1in(A,B,C,D,E) [A >= 1 + C] evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb7in(A,B,C,D,E) [C >= A] evalrealshellsortbb1in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,F,C) True evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [B >= 1 + E] evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb4in(A,B,C,D,E) [E >= B] evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb2in(A,B,C,D,E) [F >= 1 + D] evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [D >= F] evalrealshellsortbb2in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,D,-1*B + E) True evalrealshellsortbb5in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,1 + C,D,E) True evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,0,C,D,E) [B = 0] evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [B >= 1 && F >= 0 && B >= 2*F && 1 + 2*F >= B] evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [0 >= 1 + B && 0 >= F && 2*F >= B && 1 + B >= 2*F] evalrealshellsortreturnin(A,B,C,D,E) -> evalrealshellsortstop(A,B,C,D,E) True 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)} Rule Graph: [0->{1,2,3},1->{5},2->{4,5},3->{5},4->{6,7},5->{18},6->{8},7->{15,16,17},8->{9,10},9->{14},10->{11,12} ,11->{13},12->{14},13->{9,10},14->{6,7},15->{5},16->{4,5},17->{5},18->{}] + Applied Processor: CloseWith False + Details: () NO