NO
* Step 1: UnsatPaths NO
    + 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:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(1,4)]
* Step 2: FromIts NO
    + 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},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:
        FromIts
    + Details:
        ()
* Step 3: CloseWith NO
    + Considered Problem:
        Rules:
          evalfstart(A,B,C,D,E)    -> evalfentryin(A,B,C,D,E)     True
          evalfentryin(A,B,C,D,E)  -> evalfbb7in(B,B,0,D,E)       True
          evalfbb7in(A,B,C,D,E)    -> evalfbbin(A,B,C,D,E)        [A >= 0 && C >= 0]
          evalfbb7in(A,B,C,D,E)    -> evalfreturnin(A,B,C,D,E)    [0 >= 1 + A]
          evalfbb7in(A,B,C,D,E)    -> evalfreturnin(A,B,C,D,E)    [0 >= 1 + C]
          evalfbbin(A,B,C,D,E)     -> evalfbb3in(A,B,C,C,E)       [0 >= 1 + F]
          evalfbbin(A,B,C,D,E)     -> evalfbb3in(A,B,C,C,E)       [F >= 1]
          evalfbbin(A,B,C,D,E)     -> evalfbb6in(A,B,C,A,C)       True
          evalfbb3in(A,B,C,D,E)    -> evalfbb5in(A,B,C,D,E)       [D >= 1 + B]
          evalfbb3in(A,B,C,D,E)    -> evalfbb4in(A,B,C,D,E)       [B >= D]
          evalfbb4in(A,B,C,D,E)    -> evalfbb2in(A,B,C,D,E)       [0 >= 1 + F]
          evalfbb4in(A,B,C,D,E)    -> evalfbb2in(A,B,C,D,E)       [F >= 1]
          evalfbb4in(A,B,C,D,E)    -> evalfbb5in(A,B,C,D,E)       True
          evalfbb2in(A,B,C,D,E)    -> evalfbb3in(A,B,C,1 + D,E)   True
          evalfbb5in(A,B,C,D,E)    -> evalfbb6in(A,B,C,-1 + A,D)  True
          evalfbb6in(A,B,C,D,E)    -> evalfbb7in(D,B,-1 + E,D,E)  True
          evalfreturnin(A,B,C,D,E) -> evalfstop(A,B,C,D,E)        True
        Signature:
          {(evalfbb2in,5)
          ;(evalfbb3in,5)
          ;(evalfbb4in,5)
          ;(evalfbb5in,5)
          ;(evalfbb6in,5)
          ;(evalfbb7in,5)
          ;(evalfbbin,5)
          ;(evalfentryin,5)
          ;(evalfreturnin,5)
          ;(evalfstart,5)
          ;(evalfstop,5)}
        Rule 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:
        CloseWith False
    + Details:
        ()

NO