MAYBE
* Step 1: TrivialSCCs MAYBE
    + Considered Problem:
        Rules:
          0.  evalfstart(A,B,C,D,E)    -> evalfentryin(A,B,C,D,E)    True               (1,1)
          1.  evalfentryin(A,B,C,D,E)  -> evalfbb7in(B,B,0,D,E)      True               (?,1)
          2.  evalfbb7in(A,B,C,D,E)    -> evalfbbin(A,B,C,D,E)       [A >= 0 && C >= 0] (?,1)
          3.  evalfbb7in(A,B,C,D,E)    -> evalfreturnin(A,B,C,D,E)   [0 >= 1 + A]       (?,1)
          4.  evalfbb7in(A,B,C,D,E)    -> evalfreturnin(A,B,C,D,E)   [0 >= 1 + C]       (?,1)
          5.  evalfbbin(A,B,C,D,E)     -> evalfbb3in(A,B,C,C,E)      [0 >= 1 + F]       (?,1)
          6.  evalfbbin(A,B,C,D,E)     -> evalfbb3in(A,B,C,C,E)      [F >= 1]           (?,1)
          7.  evalfbbin(A,B,C,D,E)     -> evalfbb6in(A,B,C,A,C)      True               (?,1)
          8.  evalfbb3in(A,B,C,D,E)    -> evalfbb5in(A,B,C,D,E)      [D >= 1 + B]       (?,1)
          9.  evalfbb3in(A,B,C,D,E)    -> evalfbb4in(A,B,C,D,E)      [B >= D]           (?,1)
          10. evalfbb4in(A,B,C,D,E)    -> evalfbb2in(A,B,C,D,E)      [0 >= 1 + F]       (?,1)
          11. evalfbb4in(A,B,C,D,E)    -> evalfbb2in(A,B,C,D,E)      [F >= 1]           (?,1)
          12. evalfbb4in(A,B,C,D,E)    -> evalfbb5in(A,B,C,D,E)      True               (?,1)
          13. evalfbb2in(A,B,C,D,E)    -> evalfbb3in(A,B,C,1 + D,E)  True               (?,1)
          14. evalfbb5in(A,B,C,D,E)    -> evalfbb6in(A,B,C,-1 + A,D) True               (?,1)
          15. evalfbb6in(A,B,C,D,E)    -> evalfbb7in(D,B,-1 + E,D,E) True               (?,1)
          16. evalfreturnin(A,B,C,D,E) -> evalfstop(A,B,C,D,E)       True               (?,1)
        Signature:
          {(evalfbb2in,5)
          ;(evalfbb3in,5)
          ;(evalfbb4in,5)
          ;(evalfbb5in,5)
          ;(evalfbb6in,5)
          ;(evalfbb7in,5)
          ;(evalfbbin,5)
          ;(evalfentryin,5)
          ;(evalfreturnin,5)
          ;(evalfstart,5)
          ;(evalfstop,5)}
        Flow Graph:
          [0->{1},1->{2,3,4},2->{5,6,7},3->{16},4->{16},5->{8,9},6->{8,9},7->{15},8->{14},9->{10,11,12},10->{13}
          ,11->{13},12->{14},13->{8,9},14->{15},15->{2,3,4},16->{}]
        
    + Applied Processor:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 2: UnsatPaths MAYBE
    + Considered Problem:
        Rules:
          0.  evalfstart(A,B,C,D,E)    -> evalfentryin(A,B,C,D,E)    True               (1,1)
          1.  evalfentryin(A,B,C,D,E)  -> evalfbb7in(B,B,0,D,E)      True               (1,1)
          2.  evalfbb7in(A,B,C,D,E)    -> evalfbbin(A,B,C,D,E)       [A >= 0 && C >= 0] (?,1)
          3.  evalfbb7in(A,B,C,D,E)    -> evalfreturnin(A,B,C,D,E)   [0 >= 1 + A]       (1,1)
          4.  evalfbb7in(A,B,C,D,E)    -> evalfreturnin(A,B,C,D,E)   [0 >= 1 + C]       (1,1)
          5.  evalfbbin(A,B,C,D,E)     -> evalfbb3in(A,B,C,C,E)      [0 >= 1 + F]       (?,1)
          6.  evalfbbin(A,B,C,D,E)     -> evalfbb3in(A,B,C,C,E)      [F >= 1]           (?,1)
          7.  evalfbbin(A,B,C,D,E)     -> evalfbb6in(A,B,C,A,C)      True               (?,1)
          8.  evalfbb3in(A,B,C,D,E)    -> evalfbb5in(A,B,C,D,E)      [D >= 1 + B]       (?,1)
          9.  evalfbb3in(A,B,C,D,E)    -> evalfbb4in(A,B,C,D,E)      [B >= D]           (?,1)
          10. evalfbb4in(A,B,C,D,E)    -> evalfbb2in(A,B,C,D,E)      [0 >= 1 + F]       (?,1)
          11. evalfbb4in(A,B,C,D,E)    -> evalfbb2in(A,B,C,D,E)      [F >= 1]           (?,1)
          12. evalfbb4in(A,B,C,D,E)    -> evalfbb5in(A,B,C,D,E)      True               (?,1)
          13. evalfbb2in(A,B,C,D,E)    -> evalfbb3in(A,B,C,1 + D,E)  True               (?,1)
          14. evalfbb5in(A,B,C,D,E)    -> evalfbb6in(A,B,C,-1 + A,D) True               (?,1)
          15. evalfbb6in(A,B,C,D,E)    -> evalfbb7in(D,B,-1 + E,D,E) True               (?,1)
          16. evalfreturnin(A,B,C,D,E) -> evalfstop(A,B,C,D,E)       True               (1,1)
        Signature:
          {(evalfbb2in,5)
          ;(evalfbb3in,5)
          ;(evalfbb4in,5)
          ;(evalfbb5in,5)
          ;(evalfbb6in,5)
          ;(evalfbb7in,5)
          ;(evalfbbin,5)
          ;(evalfentryin,5)
          ;(evalfreturnin,5)
          ;(evalfstart,5)
          ;(evalfstop,5)}
        Flow Graph:
          [0->{1},1->{2,3,4},2->{5,6,7},3->{16},4->{16},5->{8,9},6->{8,9},7->{15},8->{14},9->{10,11,12},10->{13}
          ,11->{13},12->{14},13->{8,9},14->{15},15->{2,3,4},16->{}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(1,4)]
* Step 3: AddSinks MAYBE
    + Considered Problem:
        Rules:
          0.  evalfstart(A,B,C,D,E)    -> evalfentryin(A,B,C,D,E)    True               (1,1)
          1.  evalfentryin(A,B,C,D,E)  -> evalfbb7in(B,B,0,D,E)      True               (1,1)
          2.  evalfbb7in(A,B,C,D,E)    -> evalfbbin(A,B,C,D,E)       [A >= 0 && C >= 0] (?,1)
          3.  evalfbb7in(A,B,C,D,E)    -> evalfreturnin(A,B,C,D,E)   [0 >= 1 + A]       (1,1)
          4.  evalfbb7in(A,B,C,D,E)    -> evalfreturnin(A,B,C,D,E)   [0 >= 1 + C]       (1,1)
          5.  evalfbbin(A,B,C,D,E)     -> evalfbb3in(A,B,C,C,E)      [0 >= 1 + F]       (?,1)
          6.  evalfbbin(A,B,C,D,E)     -> evalfbb3in(A,B,C,C,E)      [F >= 1]           (?,1)
          7.  evalfbbin(A,B,C,D,E)     -> evalfbb6in(A,B,C,A,C)      True               (?,1)
          8.  evalfbb3in(A,B,C,D,E)    -> evalfbb5in(A,B,C,D,E)      [D >= 1 + B]       (?,1)
          9.  evalfbb3in(A,B,C,D,E)    -> evalfbb4in(A,B,C,D,E)      [B >= D]           (?,1)
          10. evalfbb4in(A,B,C,D,E)    -> evalfbb2in(A,B,C,D,E)      [0 >= 1 + F]       (?,1)
          11. evalfbb4in(A,B,C,D,E)    -> evalfbb2in(A,B,C,D,E)      [F >= 1]           (?,1)
          12. evalfbb4in(A,B,C,D,E)    -> evalfbb5in(A,B,C,D,E)      True               (?,1)
          13. evalfbb2in(A,B,C,D,E)    -> evalfbb3in(A,B,C,1 + D,E)  True               (?,1)
          14. evalfbb5in(A,B,C,D,E)    -> evalfbb6in(A,B,C,-1 + A,D) True               (?,1)
          15. evalfbb6in(A,B,C,D,E)    -> evalfbb7in(D,B,-1 + E,D,E) True               (?,1)
          16. evalfreturnin(A,B,C,D,E) -> evalfstop(A,B,C,D,E)       True               (1,1)
        Signature:
          {(evalfbb2in,5)
          ;(evalfbb3in,5)
          ;(evalfbb4in,5)
          ;(evalfbb5in,5)
          ;(evalfbb6in,5)
          ;(evalfbb7in,5)
          ;(evalfbbin,5)
          ;(evalfentryin,5)
          ;(evalfreturnin,5)
          ;(evalfstart,5)
          ;(evalfstop,5)}
        Flow Graph:
          [0->{1},1->{2,3},2->{5,6,7},3->{16},4->{16},5->{8,9},6->{8,9},7->{15},8->{14},9->{10,11,12},10->{13}
          ,11->{13},12->{14},13->{8,9},14->{15},15->{2,3,4},16->{}]
        
    + Applied Processor:
        AddSinks
    + Details:
        ()
* Step 4: UnsatPaths MAYBE
    + Considered Problem:
        Rules:
          0.  evalfstart(A,B,C,D,E)    -> evalfentryin(A,B,C,D,E)    True               (1,1)
          1.  evalfentryin(A,B,C,D,E)  -> evalfbb7in(B,B,0,D,E)      True               (?,1)
          2.  evalfbb7in(A,B,C,D,E)    -> evalfbbin(A,B,C,D,E)       [A >= 0 && C >= 0] (?,1)
          3.  evalfbb7in(A,B,C,D,E)    -> evalfreturnin(A,B,C,D,E)   [0 >= 1 + A]       (?,1)
          4.  evalfbb7in(A,B,C,D,E)    -> evalfreturnin(A,B,C,D,E)   [0 >= 1 + C]       (?,1)
          5.  evalfbbin(A,B,C,D,E)     -> evalfbb3in(A,B,C,C,E)      [0 >= 1 + F]       (?,1)
          6.  evalfbbin(A,B,C,D,E)     -> evalfbb3in(A,B,C,C,E)      [F >= 1]           (?,1)
          7.  evalfbbin(A,B,C,D,E)     -> evalfbb6in(A,B,C,A,C)      True               (?,1)
          8.  evalfbb3in(A,B,C,D,E)    -> evalfbb5in(A,B,C,D,E)      [D >= 1 + B]       (?,1)
          9.  evalfbb3in(A,B,C,D,E)    -> evalfbb4in(A,B,C,D,E)      [B >= D]           (?,1)
          10. evalfbb4in(A,B,C,D,E)    -> evalfbb2in(A,B,C,D,E)      [0 >= 1 + F]       (?,1)
          11. evalfbb4in(A,B,C,D,E)    -> evalfbb2in(A,B,C,D,E)      [F >= 1]           (?,1)
          12. evalfbb4in(A,B,C,D,E)    -> evalfbb5in(A,B,C,D,E)      True               (?,1)
          13. evalfbb2in(A,B,C,D,E)    -> evalfbb3in(A,B,C,1 + D,E)  True               (?,1)
          14. evalfbb5in(A,B,C,D,E)    -> evalfbb6in(A,B,C,-1 + A,D) True               (?,1)
          15. evalfbb6in(A,B,C,D,E)    -> evalfbb7in(D,B,-1 + E,D,E) True               (?,1)
          16. evalfreturnin(A,B,C,D,E) -> evalfstop(A,B,C,D,E)       True               (?,1)
          17. evalfreturnin(A,B,C,D,E) -> exitus616(A,B,C,D,E)       True               (?,1)
        Signature:
          {(evalfbb2in,5)
          ;(evalfbb3in,5)
          ;(evalfbb4in,5)
          ;(evalfbb5in,5)
          ;(evalfbb6in,5)
          ;(evalfbb7in,5)
          ;(evalfbbin,5)
          ;(evalfentryin,5)
          ;(evalfreturnin,5)
          ;(evalfstart,5)
          ;(evalfstop,5)
          ;(exitus616,5)}
        Flow Graph:
          [0->{1},1->{2,3,4},2->{5,6,7},3->{16,17},4->{16,17},5->{8,9},6->{8,9},7->{15},8->{14},9->{10,11,12}
          ,10->{13},11->{13},12->{14},13->{8,9},14->{15},15->{2,3,4},16->{},17->{}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(1,4)]
* Step 5: Failure MAYBE
  + Considered Problem:
      Rules:
        0.  evalfstart(A,B,C,D,E)    -> evalfentryin(A,B,C,D,E)    True               (1,1)
        1.  evalfentryin(A,B,C,D,E)  -> evalfbb7in(B,B,0,D,E)      True               (?,1)
        2.  evalfbb7in(A,B,C,D,E)    -> evalfbbin(A,B,C,D,E)       [A >= 0 && C >= 0] (?,1)
        3.  evalfbb7in(A,B,C,D,E)    -> evalfreturnin(A,B,C,D,E)   [0 >= 1 + A]       (?,1)
        4.  evalfbb7in(A,B,C,D,E)    -> evalfreturnin(A,B,C,D,E)   [0 >= 1 + C]       (?,1)
        5.  evalfbbin(A,B,C,D,E)     -> evalfbb3in(A,B,C,C,E)      [0 >= 1 + F]       (?,1)
        6.  evalfbbin(A,B,C,D,E)     -> evalfbb3in(A,B,C,C,E)      [F >= 1]           (?,1)
        7.  evalfbbin(A,B,C,D,E)     -> evalfbb6in(A,B,C,A,C)      True               (?,1)
        8.  evalfbb3in(A,B,C,D,E)    -> evalfbb5in(A,B,C,D,E)      [D >= 1 + B]       (?,1)
        9.  evalfbb3in(A,B,C,D,E)    -> evalfbb4in(A,B,C,D,E)      [B >= D]           (?,1)
        10. evalfbb4in(A,B,C,D,E)    -> evalfbb2in(A,B,C,D,E)      [0 >= 1 + F]       (?,1)
        11. evalfbb4in(A,B,C,D,E)    -> evalfbb2in(A,B,C,D,E)      [F >= 1]           (?,1)
        12. evalfbb4in(A,B,C,D,E)    -> evalfbb5in(A,B,C,D,E)      True               (?,1)
        13. evalfbb2in(A,B,C,D,E)    -> evalfbb3in(A,B,C,1 + D,E)  True               (?,1)
        14. evalfbb5in(A,B,C,D,E)    -> evalfbb6in(A,B,C,-1 + A,D) True               (?,1)
        15. evalfbb6in(A,B,C,D,E)    -> evalfbb7in(D,B,-1 + E,D,E) True               (?,1)
        16. evalfreturnin(A,B,C,D,E) -> evalfstop(A,B,C,D,E)       True               (?,1)
        17. evalfreturnin(A,B,C,D,E) -> exitus616(A,B,C,D,E)       True               (?,1)
      Signature:
        {(evalfbb2in,5)
        ;(evalfbb3in,5)
        ;(evalfbb4in,5)
        ;(evalfbb5in,5)
        ;(evalfbb6in,5)
        ;(evalfbb7in,5)
        ;(evalfbbin,5)
        ;(evalfentryin,5)
        ;(evalfreturnin,5)
        ;(evalfstart,5)
        ;(evalfstop,5)
        ;(exitus616,5)}
      Flow Graph:
        [0->{1},1->{2,3},2->{5,6,7},3->{16,17},4->{16,17},5->{8,9},6->{8,9},7->{15},8->{14},9->{10,11,12},10->{13}
        ,11->{13},12->{14},13->{8,9},14->{15},15->{2,3,4},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:[2,15,7,14,8,5,6,13,10,9,11,12] c: []
MAYBE