NO
* Step 1: UnsatRules NO
    + Considered Problem:
        Rules:
          0.  evalsipma91start(A,B,C,D)    -> evalsipma91entryin(A,B,C,D)           True                   (1,1)
          1.  evalsipma91entryin(A,B,C,D)  -> evalsipma91returnin(A,B,C,D)          [A >= 101]             (?,1)
          2.  evalsipma91entryin(A,B,C,D)  -> evalsipma91bb3in(1,A,C,D)             [100 >= A]             (?,1)
          3.  evalsipma91bb3in(A,B,C,D)    -> evalsipma91bb2in(A,B,C,D)             [100 >= B]             (?,1)
          4.  evalsipma91bb3in(A,B,C,D)    -> evalsipma91bb11in(A,B,C,D)            [B >= 101]             (?,1)
          5.  evalsipma91bb2in(A,B,C,D)    -> evalsipma91bb3in(1 + A,11 + B,C,D)    True                   (?,1)
          6.  evalsipma91bb11in(A,B,C,D)   -> evalsipma91bb5in(A,B,C,D)             [A >= 2]               (?,1)
          7.  evalsipma91bb11in(A,B,C,D)   -> evalsipma91returnin(A,B,C,D)          [1 >= A]               (?,1)
          8.  evalsipma91bb5in(A,B,C,D)    -> evalsipma91bb8in(A,B,-10 + B,-1 + A)  [110 >= B]             (?,1)
          9.  evalsipma91bb5in(A,B,C,D)    -> evalsipma91bb8in(A,B,-10 + B,-1 + A)  [1 >= A]               (?,1)
          10. evalsipma91bb5in(A,B,C,D)    -> evalsipma91bb8in(A,B,-10 + B,-1 + A)  [A >= 3]               (?,1)
          11. evalsipma91bb5in(A,B,C,D)    -> evalsipma91bb11in(-1 + A,-10 + B,C,D) [B >= 111 && A = 2]    (?,1)
          12. evalsipma91bb8in(A,B,C,D)    -> evalsipma91bb11in(D,1 + C,C,D)        [C >= 101]             (?,1)
          13. evalsipma91bb8in(A,B,C,D)    -> evalsipma91bb11in(D,11 + C,C,D)       [C >= 101 && 100 >= C] (?,1)
          14. evalsipma91bb8in(A,B,C,D)    -> evalsipma91bb11in(1 + D,1 + C,C,D)    [100 >= C && C >= 101] (?,1)
          15. evalsipma91bb8in(A,B,C,D)    -> evalsipma91bb11in(1 + D,11 + C,C,D)   [100 >= C]             (?,1)
          16. evalsipma91returnin(A,B,C,D) -> evalsipma91stop(A,B,C,D)              True                   (?,1)
        Signature:
          {(evalsipma91bb11in,4)
          ;(evalsipma91bb2in,4)
          ;(evalsipma91bb3in,4)
          ;(evalsipma91bb5in,4)
          ;(evalsipma91bb8in,4)
          ;(evalsipma91entryin,4)
          ;(evalsipma91returnin,4)
          ;(evalsipma91start,4)
          ;(evalsipma91stop,4)}
        Flow Graph:
          [0->{1,2},1->{16},2->{3,4},3->{5},4->{6,7},5->{3,4},6->{8,9,10,11},7->{16},8->{12,13,14,15},9->{12,13,14
          ,15},10->{12,13,14,15},11->{6,7},12->{6,7},13->{6,7},14->{6,7},15->{6,7},16->{}]
        
    + Applied Processor:
        UnsatRules
    + Details:
        Following transitions have unsatisfiable constraints and are removed:  [13,14]
* Step 2: UnsatPaths NO
    + Considered Problem:
        Rules:
          0.  evalsipma91start(A,B,C,D)    -> evalsipma91entryin(A,B,C,D)           True                (1,1)
          1.  evalsipma91entryin(A,B,C,D)  -> evalsipma91returnin(A,B,C,D)          [A >= 101]          (?,1)
          2.  evalsipma91entryin(A,B,C,D)  -> evalsipma91bb3in(1,A,C,D)             [100 >= A]          (?,1)
          3.  evalsipma91bb3in(A,B,C,D)    -> evalsipma91bb2in(A,B,C,D)             [100 >= B]          (?,1)
          4.  evalsipma91bb3in(A,B,C,D)    -> evalsipma91bb11in(A,B,C,D)            [B >= 101]          (?,1)
          5.  evalsipma91bb2in(A,B,C,D)    -> evalsipma91bb3in(1 + A,11 + B,C,D)    True                (?,1)
          6.  evalsipma91bb11in(A,B,C,D)   -> evalsipma91bb5in(A,B,C,D)             [A >= 2]            (?,1)
          7.  evalsipma91bb11in(A,B,C,D)   -> evalsipma91returnin(A,B,C,D)          [1 >= A]            (?,1)
          8.  evalsipma91bb5in(A,B,C,D)    -> evalsipma91bb8in(A,B,-10 + B,-1 + A)  [110 >= B]          (?,1)
          9.  evalsipma91bb5in(A,B,C,D)    -> evalsipma91bb8in(A,B,-10 + B,-1 + A)  [1 >= A]            (?,1)
          10. evalsipma91bb5in(A,B,C,D)    -> evalsipma91bb8in(A,B,-10 + B,-1 + A)  [A >= 3]            (?,1)
          11. evalsipma91bb5in(A,B,C,D)    -> evalsipma91bb11in(-1 + A,-10 + B,C,D) [B >= 111 && A = 2] (?,1)
          12. evalsipma91bb8in(A,B,C,D)    -> evalsipma91bb11in(D,1 + C,C,D)        [C >= 101]          (?,1)
          15. evalsipma91bb8in(A,B,C,D)    -> evalsipma91bb11in(1 + D,11 + C,C,D)   [100 >= C]          (?,1)
          16. evalsipma91returnin(A,B,C,D) -> evalsipma91stop(A,B,C,D)              True                (?,1)
        Signature:
          {(evalsipma91bb11in,4)
          ;(evalsipma91bb2in,4)
          ;(evalsipma91bb3in,4)
          ;(evalsipma91bb5in,4)
          ;(evalsipma91bb8in,4)
          ;(evalsipma91entryin,4)
          ;(evalsipma91returnin,4)
          ;(evalsipma91start,4)
          ;(evalsipma91stop,4)}
        Flow Graph:
          [0->{1,2},1->{16},2->{3,4},3->{5},4->{6,7},5->{3,4},6->{8,9,10,11},7->{16},8->{12,15},9->{12,15},10->{12
          ,15},11->{6,7},12->{6,7},15->{6,7},16->{}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(2,4),(6,9),(8,12),(11,6)]
* Step 3: UnreachableRules NO
    + Considered Problem:
        Rules:
          0.  evalsipma91start(A,B,C,D)    -> evalsipma91entryin(A,B,C,D)           True                (1,1)
          1.  evalsipma91entryin(A,B,C,D)  -> evalsipma91returnin(A,B,C,D)          [A >= 101]          (?,1)
          2.  evalsipma91entryin(A,B,C,D)  -> evalsipma91bb3in(1,A,C,D)             [100 >= A]          (?,1)
          3.  evalsipma91bb3in(A,B,C,D)    -> evalsipma91bb2in(A,B,C,D)             [100 >= B]          (?,1)
          4.  evalsipma91bb3in(A,B,C,D)    -> evalsipma91bb11in(A,B,C,D)            [B >= 101]          (?,1)
          5.  evalsipma91bb2in(A,B,C,D)    -> evalsipma91bb3in(1 + A,11 + B,C,D)    True                (?,1)
          6.  evalsipma91bb11in(A,B,C,D)   -> evalsipma91bb5in(A,B,C,D)             [A >= 2]            (?,1)
          7.  evalsipma91bb11in(A,B,C,D)   -> evalsipma91returnin(A,B,C,D)          [1 >= A]            (?,1)
          8.  evalsipma91bb5in(A,B,C,D)    -> evalsipma91bb8in(A,B,-10 + B,-1 + A)  [110 >= B]          (?,1)
          9.  evalsipma91bb5in(A,B,C,D)    -> evalsipma91bb8in(A,B,-10 + B,-1 + A)  [1 >= A]            (?,1)
          10. evalsipma91bb5in(A,B,C,D)    -> evalsipma91bb8in(A,B,-10 + B,-1 + A)  [A >= 3]            (?,1)
          11. evalsipma91bb5in(A,B,C,D)    -> evalsipma91bb11in(-1 + A,-10 + B,C,D) [B >= 111 && A = 2] (?,1)
          12. evalsipma91bb8in(A,B,C,D)    -> evalsipma91bb11in(D,1 + C,C,D)        [C >= 101]          (?,1)
          15. evalsipma91bb8in(A,B,C,D)    -> evalsipma91bb11in(1 + D,11 + C,C,D)   [100 >= C]          (?,1)
          16. evalsipma91returnin(A,B,C,D) -> evalsipma91stop(A,B,C,D)              True                (?,1)
        Signature:
          {(evalsipma91bb11in,4)
          ;(evalsipma91bb2in,4)
          ;(evalsipma91bb3in,4)
          ;(evalsipma91bb5in,4)
          ;(evalsipma91bb8in,4)
          ;(evalsipma91entryin,4)
          ;(evalsipma91returnin,4)
          ;(evalsipma91start,4)
          ;(evalsipma91stop,4)}
        Flow Graph:
          [0->{1,2},1->{16},2->{3},3->{5},4->{6,7},5->{3,4},6->{8,10,11},7->{16},8->{15},9->{12,15},10->{12,15}
          ,11->{7},12->{6,7},15->{6,7},16->{}]
        
    + Applied Processor:
        UnreachableRules
    + Details:
        Following transitions are not reachable from the starting states and are revomed: [9]
* Step 4: FromIts NO
    + Considered Problem:
        Rules:
          0.  evalsipma91start(A,B,C,D)    -> evalsipma91entryin(A,B,C,D)           True                (1,1)
          1.  evalsipma91entryin(A,B,C,D)  -> evalsipma91returnin(A,B,C,D)          [A >= 101]          (?,1)
          2.  evalsipma91entryin(A,B,C,D)  -> evalsipma91bb3in(1,A,C,D)             [100 >= A]          (?,1)
          3.  evalsipma91bb3in(A,B,C,D)    -> evalsipma91bb2in(A,B,C,D)             [100 >= B]          (?,1)
          4.  evalsipma91bb3in(A,B,C,D)    -> evalsipma91bb11in(A,B,C,D)            [B >= 101]          (?,1)
          5.  evalsipma91bb2in(A,B,C,D)    -> evalsipma91bb3in(1 + A,11 + B,C,D)    True                (?,1)
          6.  evalsipma91bb11in(A,B,C,D)   -> evalsipma91bb5in(A,B,C,D)             [A >= 2]            (?,1)
          7.  evalsipma91bb11in(A,B,C,D)   -> evalsipma91returnin(A,B,C,D)          [1 >= A]            (?,1)
          8.  evalsipma91bb5in(A,B,C,D)    -> evalsipma91bb8in(A,B,-10 + B,-1 + A)  [110 >= B]          (?,1)
          10. evalsipma91bb5in(A,B,C,D)    -> evalsipma91bb8in(A,B,-10 + B,-1 + A)  [A >= 3]            (?,1)
          11. evalsipma91bb5in(A,B,C,D)    -> evalsipma91bb11in(-1 + A,-10 + B,C,D) [B >= 111 && A = 2] (?,1)
          12. evalsipma91bb8in(A,B,C,D)    -> evalsipma91bb11in(D,1 + C,C,D)        [C >= 101]          (?,1)
          15. evalsipma91bb8in(A,B,C,D)    -> evalsipma91bb11in(1 + D,11 + C,C,D)   [100 >= C]          (?,1)
          16. evalsipma91returnin(A,B,C,D) -> evalsipma91stop(A,B,C,D)              True                (?,1)
        Signature:
          {(evalsipma91bb11in,4)
          ;(evalsipma91bb2in,4)
          ;(evalsipma91bb3in,4)
          ;(evalsipma91bb5in,4)
          ;(evalsipma91bb8in,4)
          ;(evalsipma91entryin,4)
          ;(evalsipma91returnin,4)
          ;(evalsipma91start,4)
          ;(evalsipma91stop,4)}
        Flow Graph:
          [0->{1,2},1->{16},2->{3},3->{5},4->{6,7},5->{3,4},6->{8,10,11},7->{16},8->{15},10->{12,15},11->{7},12->{6
          ,7},15->{6,7},16->{}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 5: CloseWith NO
    + Considered Problem:
        Rules:
          evalsipma91start(A,B,C,D)    -> evalsipma91entryin(A,B,C,D)             True
          evalsipma91entryin(A,B,C,D)  -> evalsipma91returnin(A,B,C,D)            [A >= 101]
          evalsipma91entryin(A,B,C,D)  -> evalsipma91bb3in(1,A,C,D)               [100 >= A]
          evalsipma91bb3in(A,B,C,D)    -> evalsipma91bb2in(A,B,C,D)               [100 >= B]
          evalsipma91bb3in(A,B,C,D)    -> evalsipma91bb11in(A,B,C,D)              [B >= 101]
          evalsipma91bb2in(A,B,C,D)    -> evalsipma91bb3in(1 + A,11 + B,C,D)      True
          evalsipma91bb11in(A,B,C,D)   -> evalsipma91bb5in(A,B,C,D)               [A >= 2]
          evalsipma91bb11in(A,B,C,D)   -> evalsipma91returnin(A,B,C,D)            [1 >= A]
          evalsipma91bb5in(A,B,C,D)    -> evalsipma91bb8in(A,B,-10 + B,-1 + A)    [110 >= B]
          evalsipma91bb5in(A,B,C,D)    -> evalsipma91bb8in(A,B,-10 + B,-1 + A)    [A >= 3]
          evalsipma91bb5in(A,B,C,D)    -> evalsipma91bb11in(-1 + A,-10 + B,C,D)   [B >= 111 && A = 2]
          evalsipma91bb8in(A,B,C,D)    -> evalsipma91bb11in(D,1 + C,C,D)          [C >= 101]
          evalsipma91bb8in(A,B,C,D)    -> evalsipma91bb11in(1 + D,11 + C,C,D)     [100 >= C]
          evalsipma91returnin(A,B,C,D) -> evalsipma91stop(A,B,C,D)                True
        Signature:
          {(evalsipma91bb11in,4)
          ;(evalsipma91bb2in,4)
          ;(evalsipma91bb3in,4)
          ;(evalsipma91bb5in,4)
          ;(evalsipma91bb8in,4)
          ;(evalsipma91entryin,4)
          ;(evalsipma91returnin,4)
          ;(evalsipma91start,4)
          ;(evalsipma91stop,4)}
        Rule Graph:
          [0->{1,2},1->{16},2->{3},3->{5},4->{6,7},5->{3,4},6->{8,10,11},7->{16},8->{15},10->{12,15},11->{7},12->{6
          ,7},15->{6,7},16->{}]
    + Applied Processor:
        CloseWith False
    + Details:
        ()

NO