MAYBE
* Step 1: TrivialSCCs MAYBE
    + 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:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 2: UnsatPaths MAYBE
    + 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)        [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,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 3: AddSinks MAYBE
    + 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)        [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,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:
        AddSinks
    + Details:
        ()
* Step 4: UnsatPaths MAYBE
    + 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)
          19. 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->{18,19},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->{},19->{}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(1,4),(3,4),(15,4),(17,4)]
* Step 5: Failure MAYBE
  + 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)
        19. 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->{18,19},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->{},19->{}]
      
  + 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,18,19]
        |
        `- p:[4,16,7,14,9,8,6,13,11,10,12] c: [16]
           |
           `- p:[6,14,9,8,13,11,10,12] c: [6]
              |
              `- p:[10,13,11] c: []
MAYBE