WORST_CASE(?,O(n^1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  evalfstart(A,B)    -> evalfentryin(A,B)    True                 (1,1)
          1.  evalfentryin(A,B)  -> evalfbb3in(B,A)      True                 (?,1)
          2.  evalfbb3in(A,B)    -> evalfbbin(A,B)       [B >= 1 && 254 >= B] (?,1)
          3.  evalfbb3in(A,B)    -> evalfreturnin(A,B)   [0 >= B]             (?,1)
          4.  evalfbb3in(A,B)    -> evalfreturnin(A,B)   [B >= 255]           (?,1)
          5.  evalfbbin(A,B)     -> evalfbb1in(A,B)      [0 >= 1 + A]         (?,1)
          6.  evalfbbin(A,B)     -> evalfbb1in(A,B)      [A >= 1]             (?,1)
          7.  evalfbbin(A,B)     -> evalfbb2in(A,B)      [A = 0]              (?,1)
          8.  evalfbb1in(A,B)    -> evalfbb3in(A,1 + B)  True                 (?,1)
          9.  evalfbb2in(A,B)    -> evalfbb3in(A,-1 + B) True                 (?,1)
          10. evalfreturnin(A,B) -> evalfstop(A,B)       True                 (?,1)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [0->{1},1->{2,3,4},2->{5,6,7},3->{10},4->{10},5->{8},6->{8},7->{9},8->{2,3,4},9->{2,3,4},10->{}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (< 0,0,A>, A, .= 0) (< 0,0,B>,     B, .= 0) 
          (< 1,0,A>, B, .= 0) (< 1,0,B>,     A, .= 0) 
          (< 2,0,A>, A, .= 0) (< 2,0,B>,     B, .= 0) 
          (< 3,0,A>, A, .= 0) (< 3,0,B>,     B, .= 0) 
          (< 4,0,A>, A, .= 0) (< 4,0,B>,     B, .= 0) 
          (< 5,0,A>, A, .= 0) (< 5,0,B>,     B, .= 0) 
          (< 6,0,A>, A, .= 0) (< 6,0,B>,     B, .= 0) 
          (< 7,0,A>, A, .= 0) (< 7,0,B>,     B, .= 0) 
          (< 8,0,A>, A, .= 0) (< 8,0,B>, 1 + B, .+ 1) 
          (< 9,0,A>, A, .= 0) (< 9,0,B>, 1 + B, .+ 1) 
          (<10,0,A>, A, .= 0) (<10,0,B>,     B, .= 0) 
* Step 2: SizeboundsProc WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  evalfstart(A,B)    -> evalfentryin(A,B)    True                 (1,1)
          1.  evalfentryin(A,B)  -> evalfbb3in(B,A)      True                 (?,1)
          2.  evalfbb3in(A,B)    -> evalfbbin(A,B)       [B >= 1 && 254 >= B] (?,1)
          3.  evalfbb3in(A,B)    -> evalfreturnin(A,B)   [0 >= B]             (?,1)
          4.  evalfbb3in(A,B)    -> evalfreturnin(A,B)   [B >= 255]           (?,1)
          5.  evalfbbin(A,B)     -> evalfbb1in(A,B)      [0 >= 1 + A]         (?,1)
          6.  evalfbbin(A,B)     -> evalfbb1in(A,B)      [A >= 1]             (?,1)
          7.  evalfbbin(A,B)     -> evalfbb2in(A,B)      [A = 0]              (?,1)
          8.  evalfbb1in(A,B)    -> evalfbb3in(A,1 + B)  True                 (?,1)
          9.  evalfbb2in(A,B)    -> evalfbb3in(A,-1 + B) True                 (?,1)
          10. evalfreturnin(A,B) -> evalfstop(A,B)       True                 (?,1)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [0->{1},1->{2,3,4},2->{5,6,7},3->{10},4->{10},5->{8},6->{8},7->{9},8->{2,3,4},9->{2,3,4},10->{}]
        Sizebounds:
          (< 0,0,A>, ?) (< 0,0,B>, ?) 
          (< 1,0,A>, ?) (< 1,0,B>, ?) 
          (< 2,0,A>, ?) (< 2,0,B>, ?) 
          (< 3,0,A>, ?) (< 3,0,B>, ?) 
          (< 4,0,A>, ?) (< 4,0,B>, ?) 
          (< 5,0,A>, ?) (< 5,0,B>, ?) 
          (< 6,0,A>, ?) (< 6,0,B>, ?) 
          (< 7,0,A>, ?) (< 7,0,B>, ?) 
          (< 8,0,A>, ?) (< 8,0,B>, ?) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) 
          (<10,0,A>, ?) (<10,0,B>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (< 0,0,A>, A) (< 0,0,B>,       B) 
          (< 1,0,A>, B) (< 1,0,B>,       A) 
          (< 2,0,A>, B) (< 2,0,B>,     254) 
          (< 3,0,A>, B) (< 3,0,B>, 254 + A) 
          (< 4,0,A>, B) (< 4,0,B>, 254 + A) 
          (< 5,0,A>, B) (< 5,0,B>,     254) 
          (< 6,0,A>, B) (< 6,0,B>,     254) 
          (< 7,0,A>, B) (< 7,0,B>,     254) 
          (< 8,0,A>, B) (< 8,0,B>,     254) 
          (< 9,0,A>, B) (< 9,0,B>,     254) 
          (<10,0,A>, B) (<10,0,B>, 254 + A) 
* Step 3: LeafRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  evalfstart(A,B)    -> evalfentryin(A,B)    True                 (1,1)
          1.  evalfentryin(A,B)  -> evalfbb3in(B,A)      True                 (?,1)
          2.  evalfbb3in(A,B)    -> evalfbbin(A,B)       [B >= 1 && 254 >= B] (?,1)
          3.  evalfbb3in(A,B)    -> evalfreturnin(A,B)   [0 >= B]             (?,1)
          4.  evalfbb3in(A,B)    -> evalfreturnin(A,B)   [B >= 255]           (?,1)
          5.  evalfbbin(A,B)     -> evalfbb1in(A,B)      [0 >= 1 + A]         (?,1)
          6.  evalfbbin(A,B)     -> evalfbb1in(A,B)      [A >= 1]             (?,1)
          7.  evalfbbin(A,B)     -> evalfbb2in(A,B)      [A = 0]              (?,1)
          8.  evalfbb1in(A,B)    -> evalfbb3in(A,1 + B)  True                 (?,1)
          9.  evalfbb2in(A,B)    -> evalfbb3in(A,-1 + B) True                 (?,1)
          10. evalfreturnin(A,B) -> evalfstop(A,B)       True                 (?,1)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [0->{1},1->{2,3,4},2->{5,6,7},3->{10},4->{10},5->{8},6->{8},7->{9},8->{2,3,4},9->{2,3,4},10->{}]
        Sizebounds:
          (< 0,0,A>, A) (< 0,0,B>,       B) 
          (< 1,0,A>, B) (< 1,0,B>,       A) 
          (< 2,0,A>, B) (< 2,0,B>,     254) 
          (< 3,0,A>, B) (< 3,0,B>, 254 + A) 
          (< 4,0,A>, B) (< 4,0,B>, 254 + A) 
          (< 5,0,A>, B) (< 5,0,B>,     254) 
          (< 6,0,A>, B) (< 6,0,B>,     254) 
          (< 7,0,A>, B) (< 7,0,B>,     254) 
          (< 8,0,A>, B) (< 8,0,B>,     254) 
          (< 9,0,A>, B) (< 9,0,B>,     254) 
          (<10,0,A>, B) (<10,0,B>, 254 + A) 
    + Applied Processor:
        LeafRules
    + Details:
        The following transitions are estimated by its predecessors and are removed [3,4,10]
* Step 4: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. evalfstart(A,B)   -> evalfentryin(A,B)    True                 (1,1)
          1. evalfentryin(A,B) -> evalfbb3in(B,A)      True                 (?,1)
          2. evalfbb3in(A,B)   -> evalfbbin(A,B)       [B >= 1 && 254 >= B] (?,1)
          5. evalfbbin(A,B)    -> evalfbb1in(A,B)      [0 >= 1 + A]         (?,1)
          6. evalfbbin(A,B)    -> evalfbb1in(A,B)      [A >= 1]             (?,1)
          7. evalfbbin(A,B)    -> evalfbb2in(A,B)      [A = 0]              (?,1)
          8. evalfbb1in(A,B)   -> evalfbb3in(A,1 + B)  True                 (?,1)
          9. evalfbb2in(A,B)   -> evalfbb3in(A,-1 + B) True                 (?,1)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [0->{1},1->{2},2->{5,6,7},5->{8},6->{8},7->{9},8->{2},9->{2}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>,   B) 
          (<1,0,A>, B) (<1,0,B>,   A) 
          (<2,0,A>, B) (<2,0,B>, 254) 
          (<5,0,A>, B) (<5,0,B>, 254) 
          (<6,0,A>, B) (<6,0,B>, 254) 
          (<7,0,A>, B) (<7,0,B>, 254) 
          (<8,0,A>, B) (<8,0,B>, 254) 
          (<9,0,A>, B) (<9,0,B>, 254) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
            p(evalfbb1in) = 1
            p(evalfbb2in) = 1
            p(evalfbb3in) = 1
             p(evalfbbin) = 1
          p(evalfentryin) = 2
            p(evalfstart) = 2
        
        The following rules are strictly oriented:
                       True ==>                
          evalfentryin(A,B)   = 2              
                              > 1              
                              = evalfbb3in(B,A)
        
        
        The following rules are weakly oriented:
                        True ==>                     
             evalfstart(A,B)   = 2                   
                              >= 2                   
                               = evalfentryin(A,B)   
        
        [B >= 1 && 254 >= B] ==>                     
             evalfbb3in(A,B)   = 1                   
                              >= 1                   
                               = evalfbbin(A,B)      
        
                [0 >= 1 + A] ==>                     
              evalfbbin(A,B)   = 1                   
                              >= 1                   
                               = evalfbb1in(A,B)     
        
                    [A >= 1] ==>                     
              evalfbbin(A,B)   = 1                   
                              >= 1                   
                               = evalfbb1in(A,B)     
        
                     [A = 0] ==>                     
              evalfbbin(A,B)   = 1                   
                              >= 1                   
                               = evalfbb2in(A,B)     
        
                        True ==>                     
             evalfbb1in(A,B)   = 1                   
                              >= 1                   
                               = evalfbb3in(A,1 + B) 
        
                        True ==>                     
             evalfbb2in(A,B)   = 1                   
                              >= 1                   
                               = evalfbb3in(A,-1 + B)
        
        
* Step 5: ChainProcessor WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. evalfstart(A,B)   -> evalfentryin(A,B)    True                 (1,1)
          1. evalfentryin(A,B) -> evalfbb3in(B,A)      True                 (2,1)
          2. evalfbb3in(A,B)   -> evalfbbin(A,B)       [B >= 1 && 254 >= B] (?,1)
          5. evalfbbin(A,B)    -> evalfbb1in(A,B)      [0 >= 1 + A]         (?,1)
          6. evalfbbin(A,B)    -> evalfbb1in(A,B)      [A >= 1]             (?,1)
          7. evalfbbin(A,B)    -> evalfbb2in(A,B)      [A = 0]              (?,1)
          8. evalfbb1in(A,B)   -> evalfbb3in(A,1 + B)  True                 (?,1)
          9. evalfbb2in(A,B)   -> evalfbb3in(A,-1 + B) True                 (?,1)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [0->{1},1->{2},2->{5,6,7},5->{8},6->{8},7->{9},8->{2},9->{2}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>,   B) 
          (<1,0,A>, B) (<1,0,B>,   A) 
          (<2,0,A>, B) (<2,0,B>, 254) 
          (<5,0,A>, B) (<5,0,B>, 254) 
          (<6,0,A>, B) (<6,0,B>, 254) 
          (<7,0,A>, B) (<7,0,B>, 254) 
          (<8,0,A>, B) (<8,0,B>, 254) 
          (<9,0,A>, B) (<9,0,B>, 254) 
    + Applied Processor:
        ChainProcessor False [0,1,2,5,6,7,8,9]
    + Details:
        We chained rule 0 to obtain the rules [10] .
* Step 6: UnreachableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          1.  evalfentryin(A,B) -> evalfbb3in(B,A)      True                 (2,1)
          2.  evalfbb3in(A,B)   -> evalfbbin(A,B)       [B >= 1 && 254 >= B] (?,1)
          5.  evalfbbin(A,B)    -> evalfbb1in(A,B)      [0 >= 1 + A]         (?,1)
          6.  evalfbbin(A,B)    -> evalfbb1in(A,B)      [A >= 1]             (?,1)
          7.  evalfbbin(A,B)    -> evalfbb2in(A,B)      [A = 0]              (?,1)
          8.  evalfbb1in(A,B)   -> evalfbb3in(A,1 + B)  True                 (?,1)
          9.  evalfbb2in(A,B)   -> evalfbb3in(A,-1 + B) True                 (?,1)
          10. evalfstart(A,B)   -> evalfbb3in(B,A)      True                 (1,2)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [1->{2},2->{5,6,7},5->{8},6->{8},7->{9},8->{2},9->{2},10->{2}]
        Sizebounds:
          (< 1,0,A>, B) (< 1,0,B>,   A) 
          (< 2,0,A>, B) (< 2,0,B>, 254) 
          (< 5,0,A>, B) (< 5,0,B>, 254) 
          (< 6,0,A>, B) (< 6,0,B>, 254) 
          (< 7,0,A>, B) (< 7,0,B>, 254) 
          (< 8,0,A>, B) (< 8,0,B>, 254) 
          (< 9,0,A>, B) (< 9,0,B>, 254) 
          (<10,0,A>, B) (<10,0,B>,   A) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [1]
* Step 7: ChainProcessor WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          2.  evalfbb3in(A,B) -> evalfbbin(A,B)       [B >= 1 && 254 >= B] (?,1)
          5.  evalfbbin(A,B)  -> evalfbb1in(A,B)      [0 >= 1 + A]         (?,1)
          6.  evalfbbin(A,B)  -> evalfbb1in(A,B)      [A >= 1]             (?,1)
          7.  evalfbbin(A,B)  -> evalfbb2in(A,B)      [A = 0]              (?,1)
          8.  evalfbb1in(A,B) -> evalfbb3in(A,1 + B)  True                 (?,1)
          9.  evalfbb2in(A,B) -> evalfbb3in(A,-1 + B) True                 (?,1)
          10. evalfstart(A,B) -> evalfbb3in(B,A)      True                 (1,2)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [2->{5,6,7},5->{8},6->{8},7->{9},8->{2},9->{2},10->{2}]
        Sizebounds:
          (< 2,0,A>, B) (< 2,0,B>, 254) 
          (< 5,0,A>, B) (< 5,0,B>, 254) 
          (< 6,0,A>, B) (< 6,0,B>, 254) 
          (< 7,0,A>, B) (< 7,0,B>, 254) 
          (< 8,0,A>, B) (< 8,0,B>, 254) 
          (< 9,0,A>, B) (< 9,0,B>, 254) 
          (<10,0,A>, B) (<10,0,B>,   A) 
    + Applied Processor:
        ChainProcessor False [2,5,6,7,8,9,10]
    + Details:
        We chained rule 2 to obtain the rules [11,12,13] .
* Step 8: UnreachableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          5.  evalfbbin(A,B)  -> evalfbb1in(A,B)      [0 >= 1 + A]                       (?,1)
          6.  evalfbbin(A,B)  -> evalfbb1in(A,B)      [A >= 1]                           (?,1)
          7.  evalfbbin(A,B)  -> evalfbb2in(A,B)      [A = 0]                            (?,1)
          8.  evalfbb1in(A,B) -> evalfbb3in(A,1 + B)  True                               (?,1)
          9.  evalfbb2in(A,B) -> evalfbb3in(A,-1 + B) True                               (?,1)
          10. evalfstart(A,B) -> evalfbb3in(B,A)      True                               (1,2)
          11. evalfbb3in(A,B) -> evalfbb1in(A,B)      [B >= 1 && 254 >= B && 0 >= 1 + A] (?,2)
          12. evalfbb3in(A,B) -> evalfbb1in(A,B)      [B >= 1 && 254 >= B && A >= 1]     (?,2)
          13. evalfbb3in(A,B) -> evalfbb2in(A,B)      [B >= 1 && 254 >= B && A = 0]      (?,2)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [5->{8},6->{8},7->{9},8->{11,12,13},9->{11,12,13},10->{11,12,13},11->{8},12->{8},13->{9}]
        Sizebounds:
          (< 5,0,A>, B) (< 5,0,B>, 254) 
          (< 6,0,A>, B) (< 6,0,B>, 254) 
          (< 7,0,A>, B) (< 7,0,B>, 254) 
          (< 8,0,A>, B) (< 8,0,B>, 254) 
          (< 9,0,A>, B) (< 9,0,B>, 254) 
          (<10,0,A>, B) (<10,0,B>,   A) 
          (<11,0,A>, B) (<11,0,B>, 254) 
          (<12,0,A>, B) (<12,0,B>, 254) 
          (<13,0,A>, B) (<13,0,B>, 254) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [5,6,7]
* Step 9: ChainProcessor WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          8.  evalfbb1in(A,B) -> evalfbb3in(A,1 + B)  True                               (?,1)
          9.  evalfbb2in(A,B) -> evalfbb3in(A,-1 + B) True                               (?,1)
          10. evalfstart(A,B) -> evalfbb3in(B,A)      True                               (1,2)
          11. evalfbb3in(A,B) -> evalfbb1in(A,B)      [B >= 1 && 254 >= B && 0 >= 1 + A] (?,2)
          12. evalfbb3in(A,B) -> evalfbb1in(A,B)      [B >= 1 && 254 >= B && A >= 1]     (?,2)
          13. evalfbb3in(A,B) -> evalfbb2in(A,B)      [B >= 1 && 254 >= B && A = 0]      (?,2)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [8->{11,12,13},9->{11,12,13},10->{11,12,13},11->{8},12->{8},13->{9}]
        Sizebounds:
          (< 8,0,A>, B) (< 8,0,B>, 254) 
          (< 9,0,A>, B) (< 9,0,B>, 254) 
          (<10,0,A>, B) (<10,0,B>,   A) 
          (<11,0,A>, B) (<11,0,B>, 254) 
          (<12,0,A>, B) (<12,0,B>, 254) 
          (<13,0,A>, B) (<13,0,B>, 254) 
    + Applied Processor:
        ChainProcessor False [8,9,10,11,12,13]
    + Details:
        We chained rule 8 to obtain the rules [14,15,16] .
* Step 10: ChainProcessor WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          9.  evalfbb2in(A,B) -> evalfbb3in(A,-1 + B) True                                       (?,1)
          10. evalfstart(A,B) -> evalfbb3in(B,A)      True                                       (1,2)
          11. evalfbb3in(A,B) -> evalfbb1in(A,B)      [B >= 1 && 254 >= B && 0 >= 1 + A]         (?,2)
          12. evalfbb3in(A,B) -> evalfbb1in(A,B)      [B >= 1 && 254 >= B && A >= 1]             (?,2)
          13. evalfbb3in(A,B) -> evalfbb2in(A,B)      [B >= 1 && 254 >= B && A = 0]              (?,2)
          14. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && 0 >= 1 + A] (?,3)
          15. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && A >= 1]     (?,3)
          16. evalfbb1in(A,B) -> evalfbb2in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && A = 0]      (?,3)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [9->{11,12,13},10->{11,12,13},11->{14,15,16},12->{14,15,16},13->{9},14->{14,15,16},15->{14,15,16},16->{9}]
        Sizebounds:
          (< 9,0,A>, B) (< 9,0,B>, 254) 
          (<10,0,A>, B) (<10,0,B>,   A) 
          (<11,0,A>, B) (<11,0,B>, 254) 
          (<12,0,A>, B) (<12,0,B>, 254) 
          (<13,0,A>, B) (<13,0,B>, 254) 
          (<14,0,A>, B) (<14,0,B>, 254) 
          (<15,0,A>, B) (<15,0,B>, 254) 
          (<16,0,A>, B) (<16,0,B>, 254) 
    + Applied Processor:
        ChainProcessor False [9,10,11,12,13,14,15,16]
    + Details:
        We chained rule 9 to obtain the rules [17,18,19] .
* Step 11: ChainProcessor WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          10. evalfstart(A,B) -> evalfbb3in(B,A)      True                                         (1,2)
          11. evalfbb3in(A,B) -> evalfbb1in(A,B)      [B >= 1 && 254 >= B && 0 >= 1 + A]           (?,2)
          12. evalfbb3in(A,B) -> evalfbb1in(A,B)      [B >= 1 && 254 >= B && A >= 1]               (?,2)
          13. evalfbb3in(A,B) -> evalfbb2in(A,B)      [B >= 1 && 254 >= B && A = 0]                (?,2)
          14. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && 0 >= 1 + A]   (?,3)
          15. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && A >= 1]       (?,3)
          16. evalfbb1in(A,B) -> evalfbb2in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && A = 0]        (?,3)
          17. evalfbb2in(A,B) -> evalfbb1in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && 0 >= 1 + A] (?,3)
          18. evalfbb2in(A,B) -> evalfbb1in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && A >= 1]     (?,3)
          19. evalfbb2in(A,B) -> evalfbb2in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && A = 0]      (?,3)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [10->{11,12,13},11->{14,15,16},12->{14,15,16},13->{17,18,19},14->{14,15,16},15->{14,15,16},16->{17,18,19}
          ,17->{14,15,16},18->{14,15,16},19->{17,18,19}]
        Sizebounds:
          (<10,0,A>, B) (<10,0,B>,   A) 
          (<11,0,A>, B) (<11,0,B>, 254) 
          (<12,0,A>, B) (<12,0,B>, 254) 
          (<13,0,A>, B) (<13,0,B>, 254) 
          (<14,0,A>, B) (<14,0,B>, 254) 
          (<15,0,A>, B) (<15,0,B>, 254) 
          (<16,0,A>, B) (<16,0,B>, 254) 
          (<17,0,A>, B) (<17,0,B>, 254) 
          (<18,0,A>, B) (<18,0,B>, 254) 
          (<19,0,A>, B) (<19,0,B>, 254) 
    + Applied Processor:
        ChainProcessor False [10,11,12,13,14,15,16,17,18,19]
    + Details:
        We chained rule 10 to obtain the rules [20,21,22] .
* Step 12: UnreachableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          11. evalfbb3in(A,B) -> evalfbb1in(A,B)      [B >= 1 && 254 >= B && 0 >= 1 + A]           (?,2)
          12. evalfbb3in(A,B) -> evalfbb1in(A,B)      [B >= 1 && 254 >= B && A >= 1]               (?,2)
          13. evalfbb3in(A,B) -> evalfbb2in(A,B)      [B >= 1 && 254 >= B && A = 0]                (?,2)
          14. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && 0 >= 1 + A]   (?,3)
          15. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && A >= 1]       (?,3)
          16. evalfbb1in(A,B) -> evalfbb2in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && A = 0]        (?,3)
          17. evalfbb2in(A,B) -> evalfbb1in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && 0 >= 1 + A] (?,3)
          18. evalfbb2in(A,B) -> evalfbb1in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && A >= 1]     (?,3)
          19. evalfbb2in(A,B) -> evalfbb2in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && A = 0]      (?,3)
          20. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && 0 >= 1 + B]           (1,4)
          21. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && B >= 1]               (1,4)
          22. evalfstart(A,B) -> evalfbb2in(B,A)      [A >= 1 && 254 >= A && B = 0]                (1,4)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [11->{14,15,16},12->{14,15,16},13->{17,18,19},14->{14,15,16},15->{14,15,16},16->{17,18,19},17->{14,15,16}
          ,18->{14,15,16},19->{17,18,19},20->{14,15,16},21->{14,15,16},22->{17,18,19}]
        Sizebounds:
          (<11,0,A>, B) (<11,0,B>, 254) 
          (<12,0,A>, B) (<12,0,B>, 254) 
          (<13,0,A>, B) (<13,0,B>, 254) 
          (<14,0,A>, B) (<14,0,B>, 254) 
          (<15,0,A>, B) (<15,0,B>, 254) 
          (<16,0,A>, B) (<16,0,B>, 254) 
          (<17,0,A>, B) (<17,0,B>, 254) 
          (<18,0,A>, B) (<18,0,B>, 254) 
          (<19,0,A>, B) (<19,0,B>, 254) 
          (<20,0,A>, B) (<20,0,B>, 254) 
          (<21,0,A>, B) (<21,0,B>, 254) 
          (<22,0,A>, B) (<22,0,B>, 254) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [11,12,13]
* Step 13: UnsatPaths WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          14. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && 0 >= 1 + A]   (?,3)
          15. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && A >= 1]       (?,3)
          16. evalfbb1in(A,B) -> evalfbb2in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && A = 0]        (?,3)
          17. evalfbb2in(A,B) -> evalfbb1in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && 0 >= 1 + A] (?,3)
          18. evalfbb2in(A,B) -> evalfbb1in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && A >= 1]     (?,3)
          19. evalfbb2in(A,B) -> evalfbb2in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && A = 0]      (?,3)
          20. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && 0 >= 1 + B]           (1,4)
          21. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && B >= 1]               (1,4)
          22. evalfstart(A,B) -> evalfbb2in(B,A)      [A >= 1 && 254 >= A && B = 0]                (1,4)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [14->{14,15,16},15->{14,15,16},16->{17,18,19},17->{14,15,16},18->{14,15,16},19->{17,18,19},20->{14,15,16}
          ,21->{14,15,16},22->{17,18,19}]
        Sizebounds:
          (<14,0,A>, B) (<14,0,B>, 254) 
          (<15,0,A>, B) (<15,0,B>, 254) 
          (<16,0,A>, B) (<16,0,B>, 254) 
          (<17,0,A>, B) (<17,0,B>, 254) 
          (<18,0,A>, B) (<18,0,B>, 254) 
          (<19,0,A>, B) (<19,0,B>, 254) 
          (<20,0,A>, B) (<20,0,B>, 254) 
          (<21,0,A>, B) (<21,0,B>, 254) 
          (<22,0,A>, B) (<22,0,B>, 254) 
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(14,15)
                                                             ,(14,16)
                                                             ,(15,14)
                                                             ,(15,16)
                                                             ,(16,17)
                                                             ,(16,18)
                                                             ,(17,15)
                                                             ,(17,16)
                                                             ,(18,14)
                                                             ,(18,16)
                                                             ,(19,17)
                                                             ,(19,18)
                                                             ,(20,15)
                                                             ,(20,16)
                                                             ,(21,14)
                                                             ,(21,16)
                                                             ,(22,17)
                                                             ,(22,18)]
* Step 14: UnreachableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          14. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && 0 >= 1 + A]   (?,3)
          15. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && A >= 1]       (?,3)
          16. evalfbb1in(A,B) -> evalfbb2in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && A = 0]        (?,3)
          17. evalfbb2in(A,B) -> evalfbb1in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && 0 >= 1 + A] (?,3)
          18. evalfbb2in(A,B) -> evalfbb1in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && A >= 1]     (?,3)
          19. evalfbb2in(A,B) -> evalfbb2in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && A = 0]      (?,3)
          20. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && 0 >= 1 + B]           (1,4)
          21. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && B >= 1]               (1,4)
          22. evalfstart(A,B) -> evalfbb2in(B,A)      [A >= 1 && 254 >= A && B = 0]                (1,4)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [14->{14},15->{15},16->{19},17->{14},18->{15},19->{19},20->{14},21->{15},22->{19}]
        Sizebounds:
          (<14,0,A>, B) (<14,0,B>, 254) 
          (<15,0,A>, B) (<15,0,B>, 254) 
          (<16,0,A>, B) (<16,0,B>, 254) 
          (<17,0,A>, B) (<17,0,B>, 254) 
          (<18,0,A>, B) (<18,0,B>, 254) 
          (<19,0,A>, B) (<19,0,B>, 254) 
          (<20,0,A>, B) (<20,0,B>, 254) 
          (<21,0,A>, B) (<21,0,B>, 254) 
          (<22,0,A>, B) (<22,0,B>, 254) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [16,17,18]
* Step 15: LocalSizeboundsProc WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          14. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && 0 >= 1 + A] (?,3)
          15. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && A >= 1]     (?,3)
          19. evalfbb2in(A,B) -> evalfbb2in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && A = 0]    (?,3)
          20. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && 0 >= 1 + B]         (1,4)
          21. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && B >= 1]             (1,4)
          22. evalfstart(A,B) -> evalfbb2in(B,A)      [A >= 1 && 254 >= A && B = 0]              (1,4)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [14->{14},15->{15},19->{19},20->{14},21->{15},22->{19}]
        Sizebounds:
          (<14,0,A>, B) (<14,0,B>, 254) 
          (<15,0,A>, B) (<15,0,B>, 254) 
          (<19,0,A>, B) (<19,0,B>, 254) 
          (<20,0,A>, B) (<20,0,B>, 254) 
          (<21,0,A>, B) (<21,0,B>, 254) 
          (<22,0,A>, B) (<22,0,B>, 254) 
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (<14,0,A>, A, .= 0) (<14,0,B>, 254, .= 254) 
          (<15,0,A>, A, .= 0) (<15,0,B>, 254, .= 254) 
          (<19,0,A>, A, .= 0) (<19,0,B>, 254, .= 254) 
          (<20,0,A>, B, .= 0) (<20,0,B>,   A,   .= 0) 
          (<21,0,A>, B, .= 0) (<21,0,B>,   A,   .= 0) 
          (<22,0,A>, B, .= 0) (<22,0,B>,   A,   .= 0) 
* Step 16: SizeboundsProc WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          14. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && 0 >= 1 + A] (?,3)
          15. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && A >= 1]     (?,3)
          19. evalfbb2in(A,B) -> evalfbb2in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && A = 0]    (?,3)
          20. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && 0 >= 1 + B]         (1,4)
          21. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && B >= 1]             (1,4)
          22. evalfstart(A,B) -> evalfbb2in(B,A)      [A >= 1 && 254 >= A && B = 0]              (1,4)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [14->{14},15->{15},19->{19},20->{14},21->{15},22->{19}]
        Sizebounds:
          (<14,0,A>, ?) (<14,0,B>, ?) 
          (<15,0,A>, ?) (<15,0,B>, ?) 
          (<19,0,A>, ?) (<19,0,B>, ?) 
          (<20,0,A>, ?) (<20,0,B>, ?) 
          (<21,0,A>, ?) (<21,0,B>, ?) 
          (<22,0,A>, ?) (<22,0,B>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (<14,0,A>, B) (<14,0,B>, 254) 
          (<15,0,A>, B) (<15,0,B>, 254) 
          (<19,0,A>, B) (<19,0,B>, 254) 
          (<20,0,A>, B) (<20,0,B>,   A) 
          (<21,0,A>, B) (<21,0,B>,   A) 
          (<22,0,A>, B) (<22,0,B>,   A) 
* Step 17: LocationConstraintsProc WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          14. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && 0 >= 1 + A] (?,3)
          15. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && A >= 1]     (?,3)
          19. evalfbb2in(A,B) -> evalfbb2in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && A = 0]    (?,3)
          20. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && 0 >= 1 + B]         (1,4)
          21. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && B >= 1]             (1,4)
          22. evalfstart(A,B) -> evalfbb2in(B,A)      [A >= 1 && 254 >= A && B = 0]              (1,4)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [14->{14},15->{15},19->{19},20->{14},21->{15},22->{19}]
        Sizebounds:
          (<14,0,A>, B) (<14,0,B>, 254) 
          (<15,0,A>, B) (<15,0,B>, 254) 
          (<19,0,A>, B) (<19,0,B>, 254) 
          (<20,0,A>, B) (<20,0,B>,   A) 
          (<21,0,A>, B) (<21,0,B>,   A) 
          (<22,0,A>, B) (<22,0,B>,   A) 
    + Applied Processor:
        LocationConstraintsProc
    + Details:
        We computed the location constraints  14 :  [B >= 1 && False] 15 :  [B >= 1 && False] 19 :  [B >= 1
                                                                                                     && False] 20 :  True 21 :  True 22 :  True .
* Step 18: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          14. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && 0 >= 1 + A] (?,3)
          15. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && A >= 1]     (?,3)
          19. evalfbb2in(A,B) -> evalfbb2in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && A = 0]    (?,3)
          20. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && 0 >= 1 + B]         (1,4)
          21. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && B >= 1]             (1,4)
          22. evalfstart(A,B) -> evalfbb2in(B,A)      [A >= 1 && 254 >= A && B = 0]              (1,4)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [14->{14},15->{15},19->{19},20->{14},21->{15},22->{19}]
        Sizebounds:
          (<14,0,A>, B) (<14,0,B>, 254) 
          (<15,0,A>, B) (<15,0,B>, 254) 
          (<19,0,A>, B) (<19,0,B>, 254) 
          (<20,0,A>, B) (<20,0,B>,   A) 
          (<21,0,A>, B) (<21,0,B>,   A) 
          (<22,0,A>, B) (<22,0,B>,   A) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(evalfbb1in) = 0      
          p(evalfbb2in) = -1 + x2
          p(evalfstart) = -1 + x1
        
        The following rules are strictly oriented:
        [-1 + B >= 1 && 254 >= -1 + B && A = 0] ==>                     
                                evalfbb2in(A,B)   = -1 + B              
                                                  > -2 + B              
                                                  = evalfbb2in(A,-1 + B)
        
        
        The following rules are weakly oriented:
        [1 + B >= 1 && 254 >= 1 + B && 0 >= 1 + A] ==>                    
                                   evalfbb1in(A,B)   = 0                  
                                                    >= 0                  
                                                     = evalfbb1in(A,1 + B)
        
            [1 + B >= 1 && 254 >= 1 + B && A >= 1] ==>                    
                                   evalfbb1in(A,B)   = 0                  
                                                    >= 0                  
                                                     = evalfbb1in(A,1 + B)
        
                [A >= 1 && 254 >= A && 0 >= 1 + B] ==>                    
                                   evalfstart(A,B)   = -1 + A             
                                                    >= 0                  
                                                     = evalfbb1in(B,A)    
        
                    [A >= 1 && 254 >= A && B >= 1] ==>                    
                                   evalfstart(A,B)   = -1 + A             
                                                    >= 0                  
                                                     = evalfbb1in(B,A)    
        
                     [A >= 1 && 254 >= A && B = 0] ==>                    
                                   evalfstart(A,B)   = -1 + A             
                                                    >= -1 + A             
                                                     = evalfbb2in(B,A)    
        
        
* Step 19: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          14. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && 0 >= 1 + A] (?,3)    
          15. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && A >= 1]     (?,3)    
          19. evalfbb2in(A,B) -> evalfbb2in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && A = 0]    (1 + A,3)
          20. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && 0 >= 1 + B]         (1,4)    
          21. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && B >= 1]             (1,4)    
          22. evalfstart(A,B) -> evalfbb2in(B,A)      [A >= 1 && 254 >= A && B = 0]              (1,4)    
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [14->{14},15->{15},19->{19},20->{14},21->{15},22->{19}]
        Sizebounds:
          (<14,0,A>, B) (<14,0,B>, 254) 
          (<15,0,A>, B) (<15,0,B>, 254) 
          (<19,0,A>, B) (<19,0,B>, 254) 
          (<20,0,A>, B) (<20,0,B>,   A) 
          (<21,0,A>, B) (<21,0,B>,   A) 
          (<22,0,A>, B) (<22,0,B>,   A) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(evalfbb1in) = 254 + -1*x2
          p(evalfbb2in) = 0          
          p(evalfstart) = 253        
        
        The following rules are strictly oriented:
        [1 + B >= 1 && 254 >= 1 + B && A >= 1] ==>                    
                               evalfbb1in(A,B)   = 254 + -1*B         
                                                 > 253 + -1*B         
                                                 = evalfbb1in(A,1 + B)
        
                 [A >= 1 && 254 >= A && B = 0] ==>                    
                               evalfstart(A,B)   = 253                
                                                 > 0                  
                                                 = evalfbb2in(B,A)    
        
        
        The following rules are weakly oriented:
        [1 + B >= 1 && 254 >= 1 + B && 0 >= 1 + A] ==>                     
                                   evalfbb1in(A,B)   = 254 + -1*B          
                                                    >= 253 + -1*B          
                                                     = evalfbb1in(A,1 + B) 
        
           [-1 + B >= 1 && 254 >= -1 + B && A = 0] ==>                     
                                   evalfbb2in(A,B)   = 0                   
                                                    >= 0                   
                                                     = evalfbb2in(A,-1 + B)
        
                [A >= 1 && 254 >= A && 0 >= 1 + B] ==>                     
                                   evalfstart(A,B)   = 253                 
                                                    >= 254 + -1*A          
                                                     = evalfbb1in(B,A)     
        
                    [A >= 1 && 254 >= A && B >= 1] ==>                     
                                   evalfstart(A,B)   = 253                 
                                                    >= 254 + -1*A          
                                                     = evalfbb1in(B,A)     
        
        
* Step 20: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          14. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && 0 >= 1 + A] (?,3)    
          15. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && A >= 1]     (253,3)  
          19. evalfbb2in(A,B) -> evalfbb2in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && A = 0]    (1 + A,3)
          20. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && 0 >= 1 + B]         (1,4)    
          21. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && B >= 1]             (1,4)    
          22. evalfstart(A,B) -> evalfbb2in(B,A)      [A >= 1 && 254 >= A && B = 0]              (1,4)    
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [14->{14},15->{15},19->{19},20->{14},21->{15},22->{19}]
        Sizebounds:
          (<14,0,A>, B) (<14,0,B>, 254) 
          (<15,0,A>, B) (<15,0,B>, 254) 
          (<19,0,A>, B) (<19,0,B>, 254) 
          (<20,0,A>, B) (<20,0,B>,   A) 
          (<21,0,A>, B) (<21,0,B>,   A) 
          (<22,0,A>, B) (<22,0,B>,   A) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(evalfbb1in) = 254 + -1*x2
          p(evalfbb2in) = 0          
          p(evalfstart) = 253        
        
        The following rules are strictly oriented:
        [1 + B >= 1 && 254 >= 1 + B && 0 >= 1 + A] ==>                    
                                   evalfbb1in(A,B)   = 254 + -1*B         
                                                     > 253 + -1*B         
                                                     = evalfbb1in(A,1 + B)
        
            [1 + B >= 1 && 254 >= 1 + B && A >= 1] ==>                    
                                   evalfbb1in(A,B)   = 254 + -1*B         
                                                     > 253 + -1*B         
                                                     = evalfbb1in(A,1 + B)
        
                     [A >= 1 && 254 >= A && B = 0] ==>                    
                                   evalfstart(A,B)   = 253                
                                                     > 0                  
                                                     = evalfbb2in(B,A)    
        
        
        The following rules are weakly oriented:
        [-1 + B >= 1 && 254 >= -1 + B && A = 0] ==>                     
                                evalfbb2in(A,B)   = 0                   
                                                 >= 0                   
                                                  = evalfbb2in(A,-1 + B)
        
             [A >= 1 && 254 >= A && 0 >= 1 + B] ==>                     
                                evalfstart(A,B)   = 253                 
                                                 >= 254 + -1*A          
                                                  = evalfbb1in(B,A)     
        
                 [A >= 1 && 254 >= A && B >= 1] ==>                     
                                evalfstart(A,B)   = 253                 
                                                 >= 254 + -1*A          
                                                  = evalfbb1in(B,A)     
        
        
* Step 21: LoopRecurrenceProcessor WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          14. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && 0 >= 1 + A] (253,3)  
          15. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && A >= 1]     (253,3)  
          19. evalfbb2in(A,B) -> evalfbb2in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && A = 0]    (1 + A,3)
          20. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && 0 >= 1 + B]         (1,4)    
          21. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && B >= 1]             (1,4)    
          22. evalfstart(A,B) -> evalfbb2in(B,A)      [A >= 1 && 254 >= A && B = 0]              (1,4)    
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [14->{14},15->{15},19->{19},20->{14},21->{15},22->{19}]
        Sizebounds:
          (<14,0,A>, B) (<14,0,B>, 254) 
          (<15,0,A>, B) (<15,0,B>, 254) 
          (<19,0,A>, B) (<19,0,B>, 254) 
          (<20,0,A>, B) (<20,0,B>,   A) 
          (<21,0,A>, B) (<21,0,B>,   A) 
          (<22,0,A>, B) (<22,0,B>,   A) 
    + Applied Processor:
        LoopRecurrenceProcessor [19]
    + Details:
        Applying the recurrence pattern linear * f to the expression B yields the solution B .
* Step 22: UnsatPaths WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          14. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && 0 >= 1 + A] (253,3)
          15. evalfbb1in(A,B) -> evalfbb1in(A,1 + B)  [1 + B >= 1 && 254 >= 1 + B && A >= 1]     (253,3)
          19. evalfbb2in(A,B) -> evalfbb2in(A,-1 + B) [-1 + B >= 1 && 254 >= -1 + B && A = 0]    (A,3)  
          20. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && 0 >= 1 + B]         (1,4)  
          21. evalfstart(A,B) -> evalfbb1in(B,A)      [A >= 1 && 254 >= A && B >= 1]             (1,4)  
          22. evalfstart(A,B) -> evalfbb2in(B,A)      [A >= 1 && 254 >= A && B = 0]              (1,4)  
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [14->{14},15->{15},19->{19},20->{14},21->{15},22->{19}]
        Sizebounds:
          (<14,0,A>, B) (<14,0,B>, 254) 
          (<15,0,A>, B) (<15,0,B>, 254) 
          (<19,0,A>, B) (<19,0,B>, 254) 
          (<20,0,A>, B) (<20,0,B>,   A) 
          (<21,0,A>, B) (<21,0,B>,   A) 
          (<22,0,A>, B) (<22,0,B>,   A) 
    + Applied Processor:
        UnsatPaths
    + Details:
        The problem is already solved.

WORST_CASE(?,O(n^1))