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

WORST_CASE(?,O(n^1))