NO
* Step 1: UnsatPaths NO
    + Considered Problem:
        Rules:
          0.  evalfstart(A,B)    -> evalfentryin(A,B)      True                   (1,1)
          1.  evalfentryin(A,B)  -> evalfbb3in(B,A)        [A >= 1 && B >= 1 + A] (?,1)
          2.  evalfbb3in(A,B)    -> evalfreturnin(A,B)     [0 >= A]               (?,1)
          3.  evalfbb3in(A,B)    -> evalfbb4in(A,B)        [A >= 1]               (?,1)
          4.  evalfbb4in(A,B)    -> evalfbbin(A,B)         [0 >= 1 + C]           (?,1)
          5.  evalfbb4in(A,B)    -> evalfbbin(A,B)         [C >= 1]               (?,1)
          6.  evalfbb4in(A,B)    -> evalfreturnin(A,B)     True                   (?,1)
          7.  evalfbbin(A,B)     -> evalfbb1in(A,B)        [B >= 1 + A]           (?,1)
          8.  evalfbbin(A,B)     -> evalfbb2in(A,B)        [A >= B]               (?,1)
          9.  evalfbb1in(A,B)    -> evalfbb3in(1 + A,B)    True                   (?,1)
          10. evalfbb2in(A,B)    -> evalfbb3in(A + -1*B,B) True                   (?,1)
          11. evalfreturnin(A,B) -> evalfstop(A,B)         True                   (?,1)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbb4in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [0->{1},1->{2,3},2->{11},3->{4,5,6},4->{7,8},5->{7,8},6->{11},7->{9},8->{10},9->{2,3},10->{2,3},11->{}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(1,2)]
* Step 2: FromIts NO
    + Considered Problem:
        Rules:
          0.  evalfstart(A,B)    -> evalfentryin(A,B)      True                   (1,1)
          1.  evalfentryin(A,B)  -> evalfbb3in(B,A)        [A >= 1 && B >= 1 + A] (?,1)
          2.  evalfbb3in(A,B)    -> evalfreturnin(A,B)     [0 >= A]               (?,1)
          3.  evalfbb3in(A,B)    -> evalfbb4in(A,B)        [A >= 1]               (?,1)
          4.  evalfbb4in(A,B)    -> evalfbbin(A,B)         [0 >= 1 + C]           (?,1)
          5.  evalfbb4in(A,B)    -> evalfbbin(A,B)         [C >= 1]               (?,1)
          6.  evalfbb4in(A,B)    -> evalfreturnin(A,B)     True                   (?,1)
          7.  evalfbbin(A,B)     -> evalfbb1in(A,B)        [B >= 1 + A]           (?,1)
          8.  evalfbbin(A,B)     -> evalfbb2in(A,B)        [A >= B]               (?,1)
          9.  evalfbb1in(A,B)    -> evalfbb3in(1 + A,B)    True                   (?,1)
          10. evalfbb2in(A,B)    -> evalfbb3in(A + -1*B,B) True                   (?,1)
          11. evalfreturnin(A,B) -> evalfstop(A,B)         True                   (?,1)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbb4in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [0->{1},1->{3},2->{11},3->{4,5,6},4->{7,8},5->{7,8},6->{11},7->{9},8->{10},9->{2,3},10->{2,3},11->{}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 3: CloseWith NO
    + Considered Problem:
        Rules:
          evalfstart(A,B)    -> evalfentryin(A,B)       True
          evalfentryin(A,B)  -> evalfbb3in(B,A)         [A >= 1 && B >= 1 + A]
          evalfbb3in(A,B)    -> evalfreturnin(A,B)      [0 >= A]
          evalfbb3in(A,B)    -> evalfbb4in(A,B)         [A >= 1]
          evalfbb4in(A,B)    -> evalfbbin(A,B)          [0 >= 1 + C]
          evalfbb4in(A,B)    -> evalfbbin(A,B)          [C >= 1]
          evalfbb4in(A,B)    -> evalfreturnin(A,B)      True
          evalfbbin(A,B)     -> evalfbb1in(A,B)         [B >= 1 + A]
          evalfbbin(A,B)     -> evalfbb2in(A,B)         [A >= B]
          evalfbb1in(A,B)    -> evalfbb3in(1 + A,B)     True
          evalfbb2in(A,B)    -> evalfbb3in(A + -1*B,B)  True
          evalfreturnin(A,B) -> evalfstop(A,B)          True
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbb4in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Rule Graph:
          [0->{1},1->{3},2->{11},3->{4,5,6},4->{7,8},5->{7,8},6->{11},7->{9},8->{10},9->{2,3},10->{2,3},11->{}]
    + Applied Processor:
        CloseWith False
    + Details:
        ()

NO