NO
* Step 1: FromIts NO
    + Considered Problem:
        Rules:
          0.  evalfstart(A,B,C,D)    -> evalfentryin(A,B,C,D)       True         (1,1)
          1.  evalfentryin(A,B,C,D)  -> evalfbb6in(0,B,C,D)         True         (?,1)
          2.  evalfbb6in(A,B,C,D)    -> evalfbbin(A,B,C,D)          [B >= 1 + A] (?,1)
          3.  evalfbb6in(A,B,C,D)    -> evalfreturnin(A,B,C,D)      [A >= B]     (?,1)
          4.  evalfbbin(A,B,C,D)     -> evalfbb2in(A,B,0,1 + A)     True         (?,1)
          5.  evalfbb2in(A,B,C,D)    -> evalfbb4in(A,B,C,D)         [D >= B]     (?,1)
          6.  evalfbb2in(A,B,C,D)    -> evalfbb3in(A,B,C,D)         [B >= 1 + D] (?,1)
          7.  evalfbb3in(A,B,C,D)    -> evalfbb1in(A,B,C,D)         [0 >= 1 + E] (?,1)
          8.  evalfbb3in(A,B,C,D)    -> evalfbb1in(A,B,C,D)         [E >= 1]     (?,1)
          9.  evalfbb3in(A,B,C,D)    -> evalfbb4in(A,B,C,D)         True         (?,1)
          10. evalfbb1in(A,B,C,D)    -> evalfbb2in(A,B,1 + C,1 + D) True         (?,1)
          11. evalfbb4in(A,B,C,D)    -> evalfbb6in(-1 + D,B,C,D)    [C >= 1]     (?,1)
          12. evalfbb4in(A,B,C,D)    -> evalfbb6in(D,B,C,D)         [0 >= C]     (?,1)
          13. evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D)          True         (?,1)
        Signature:
          {(evalfbb1in,4)
          ;(evalfbb2in,4)
          ;(evalfbb3in,4)
          ;(evalfbb4in,4)
          ;(evalfbb6in,4)
          ;(evalfbbin,4)
          ;(evalfentryin,4)
          ;(evalfreturnin,4)
          ;(evalfstart,4)
          ;(evalfstop,4)}
        Flow Graph:
          [0->{1},1->{2,3},2->{4},3->{13},4->{5,6},5->{11,12},6->{7,8,9},7->{10},8->{10},9->{11,12},10->{5,6},11->{2
          ,3},12->{2,3},13->{}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 2: CloseWith NO
    + Considered Problem:
        Rules:
          evalfstart(A,B,C,D)    -> evalfentryin(A,B,C,D)        True
          evalfentryin(A,B,C,D)  -> evalfbb6in(0,B,C,D)          True
          evalfbb6in(A,B,C,D)    -> evalfbbin(A,B,C,D)           [B >= 1 + A]
          evalfbb6in(A,B,C,D)    -> evalfreturnin(A,B,C,D)       [A >= B]
          evalfbbin(A,B,C,D)     -> evalfbb2in(A,B,0,1 + A)      True
          evalfbb2in(A,B,C,D)    -> evalfbb4in(A,B,C,D)          [D >= B]
          evalfbb2in(A,B,C,D)    -> evalfbb3in(A,B,C,D)          [B >= 1 + D]
          evalfbb3in(A,B,C,D)    -> evalfbb1in(A,B,C,D)          [0 >= 1 + E]
          evalfbb3in(A,B,C,D)    -> evalfbb1in(A,B,C,D)          [E >= 1]
          evalfbb3in(A,B,C,D)    -> evalfbb4in(A,B,C,D)          True
          evalfbb1in(A,B,C,D)    -> evalfbb2in(A,B,1 + C,1 + D)  True
          evalfbb4in(A,B,C,D)    -> evalfbb6in(-1 + D,B,C,D)     [C >= 1]
          evalfbb4in(A,B,C,D)    -> evalfbb6in(D,B,C,D)          [0 >= C]
          evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D)           True
        Signature:
          {(evalfbb1in,4)
          ;(evalfbb2in,4)
          ;(evalfbb3in,4)
          ;(evalfbb4in,4)
          ;(evalfbb6in,4)
          ;(evalfbbin,4)
          ;(evalfentryin,4)
          ;(evalfreturnin,4)
          ;(evalfstart,4)
          ;(evalfstop,4)}
        Rule Graph:
          [0->{1},1->{2,3},2->{4},3->{13},4->{5,6},5->{11,12},6->{7,8,9},7->{10},8->{10},9->{11,12},10->{5,6},11->{2
          ,3},12->{2,3},13->{}]
    + Applied Processor:
        CloseWith False
    + Details:
        ()

NO