WORST_CASE(?,O(n^1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  evalSimpleSingle2start(A,B,C,D)    -> evalSimpleSingle2entryin(A,B,C,D)       True         (1,1)
          1.  evalSimpleSingle2entryin(A,B,C,D)  -> evalSimpleSingle2bb4in(0,0,C,D)         True         (?,1)
          2.  evalSimpleSingle2bb4in(A,B,C,D)    -> evalSimpleSingle2bbin(A,B,C,D)          [0 >= 1 + E] (?,1)
          3.  evalSimpleSingle2bb4in(A,B,C,D)    -> evalSimpleSingle2bbin(A,B,C,D)          [E >= 1]     (?,1)
          4.  evalSimpleSingle2bb4in(A,B,C,D)    -> evalSimpleSingle2returnin(A,B,C,D)      True         (?,1)
          5.  evalSimpleSingle2bbin(A,B,C,D)     -> evalSimpleSingle2bb1in(A,B,C,D)         [C >= 1 + B] (?,1)
          6.  evalSimpleSingle2bbin(A,B,C,D)     -> evalSimpleSingle2bb2in(A,B,C,D)         [B >= C]     (?,1)
          7.  evalSimpleSingle2bb1in(A,B,C,D)    -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (?,1)
          8.  evalSimpleSingle2bb2in(A,B,C,D)    -> evalSimpleSingle2bb3in(A,B,C,D)         [D >= 1 + A] (?,1)
          9.  evalSimpleSingle2bb2in(A,B,C,D)    -> evalSimpleSingle2returnin(A,B,C,D)      [A >= D]     (?,1)
          10. evalSimpleSingle2bb3in(A,B,C,D)    -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (?,1)
          11. evalSimpleSingle2returnin(A,B,C,D) -> evalSimpleSingle2stop(A,B,C,D)          True         (?,1)
        Signature:
          {(evalSimpleSingle2bb1in,4)
          ;(evalSimpleSingle2bb2in,4)
          ;(evalSimpleSingle2bb3in,4)
          ;(evalSimpleSingle2bb4in,4)
          ;(evalSimpleSingle2bbin,4)
          ;(evalSimpleSingle2entryin,4)
          ;(evalSimpleSingle2returnin,4)
          ;(evalSimpleSingle2start,4)
          ;(evalSimpleSingle2stop,4)}
        Flow Graph:
          [0->{1},1->{2,3,4},2->{5,6},3->{5,6},4->{11},5->{7},6->{8,9},7->{2,3,4},8->{10},9->{11},10->{2,3,4}
          ,11->{}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (< 0,0,A>,     A, .= 0) (< 0,0,B>,     B, .= 0) (< 0,0,C>, C, .= 0) (< 0,0,D>, D, .= 0) 
          (< 1,0,A>,     0, .= 0) (< 1,0,B>,     0, .= 0) (< 1,0,C>, C, .= 0) (< 1,0,D>, D, .= 0) 
          (< 2,0,A>,     A, .= 0) (< 2,0,B>,     B, .= 0) (< 2,0,C>, C, .= 0) (< 2,0,D>, D, .= 0) 
          (< 3,0,A>,     A, .= 0) (< 3,0,B>,     B, .= 0) (< 3,0,C>, C, .= 0) (< 3,0,D>, D, .= 0) 
          (< 4,0,A>,     A, .= 0) (< 4,0,B>,     B, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>, D, .= 0) 
          (< 5,0,A>,     A, .= 0) (< 5,0,B>,     B, .= 0) (< 5,0,C>, C, .= 0) (< 5,0,D>, D, .= 0) 
          (< 6,0,A>,     A, .= 0) (< 6,0,B>,     B, .= 0) (< 6,0,C>, C, .= 0) (< 6,0,D>, D, .= 0) 
          (< 7,0,A>, 1 + A, .+ 1) (< 7,0,B>, 1 + B, .+ 1) (< 7,0,C>, C, .= 0) (< 7,0,D>, D, .= 0) 
          (< 8,0,A>,     A, .= 0) (< 8,0,B>,     B, .= 0) (< 8,0,C>, C, .= 0) (< 8,0,D>, D, .= 0) 
          (< 9,0,A>,     A, .= 0) (< 9,0,B>,     B, .= 0) (< 9,0,C>, C, .= 0) (< 9,0,D>, D, .= 0) 
          (<10,0,A>, 1 + A, .+ 1) (<10,0,B>, 1 + B, .+ 1) (<10,0,C>, C, .= 0) (<10,0,D>, D, .= 0) 
          (<11,0,A>,     A, .= 0) (<11,0,B>,     B, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, D, .= 0) 
* Step 2: SizeboundsProc WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  evalSimpleSingle2start(A,B,C,D)    -> evalSimpleSingle2entryin(A,B,C,D)       True         (1,1)
          1.  evalSimpleSingle2entryin(A,B,C,D)  -> evalSimpleSingle2bb4in(0,0,C,D)         True         (?,1)
          2.  evalSimpleSingle2bb4in(A,B,C,D)    -> evalSimpleSingle2bbin(A,B,C,D)          [0 >= 1 + E] (?,1)
          3.  evalSimpleSingle2bb4in(A,B,C,D)    -> evalSimpleSingle2bbin(A,B,C,D)          [E >= 1]     (?,1)
          4.  evalSimpleSingle2bb4in(A,B,C,D)    -> evalSimpleSingle2returnin(A,B,C,D)      True         (?,1)
          5.  evalSimpleSingle2bbin(A,B,C,D)     -> evalSimpleSingle2bb1in(A,B,C,D)         [C >= 1 + B] (?,1)
          6.  evalSimpleSingle2bbin(A,B,C,D)     -> evalSimpleSingle2bb2in(A,B,C,D)         [B >= C]     (?,1)
          7.  evalSimpleSingle2bb1in(A,B,C,D)    -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (?,1)
          8.  evalSimpleSingle2bb2in(A,B,C,D)    -> evalSimpleSingle2bb3in(A,B,C,D)         [D >= 1 + A] (?,1)
          9.  evalSimpleSingle2bb2in(A,B,C,D)    -> evalSimpleSingle2returnin(A,B,C,D)      [A >= D]     (?,1)
          10. evalSimpleSingle2bb3in(A,B,C,D)    -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (?,1)
          11. evalSimpleSingle2returnin(A,B,C,D) -> evalSimpleSingle2stop(A,B,C,D)          True         (?,1)
        Signature:
          {(evalSimpleSingle2bb1in,4)
          ;(evalSimpleSingle2bb2in,4)
          ;(evalSimpleSingle2bb3in,4)
          ;(evalSimpleSingle2bb4in,4)
          ;(evalSimpleSingle2bbin,4)
          ;(evalSimpleSingle2entryin,4)
          ;(evalSimpleSingle2returnin,4)
          ;(evalSimpleSingle2start,4)
          ;(evalSimpleSingle2stop,4)}
        Flow Graph:
          [0->{1},1->{2,3,4},2->{5,6},3->{5,6},4->{11},5->{7},6->{8,9},7->{2,3,4},8->{10},9->{11},10->{2,3,4}
          ,11->{}]
        Sizebounds:
          (< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?) 
          (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?) 
          (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) 
          (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) 
          (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) 
          (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) 
          (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) 
          (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) 
          (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) 
          (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) 
          (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) 
          (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) 
          (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) 
          (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) 
          (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, C) (< 4,0,D>, D) 
          (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) 
          (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) 
          (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) 
          (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, D) 
          (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) 
          (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, C) (<11,0,D>, D) 
* Step 3: LeafRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  evalSimpleSingle2start(A,B,C,D)    -> evalSimpleSingle2entryin(A,B,C,D)       True         (1,1)
          1.  evalSimpleSingle2entryin(A,B,C,D)  -> evalSimpleSingle2bb4in(0,0,C,D)         True         (?,1)
          2.  evalSimpleSingle2bb4in(A,B,C,D)    -> evalSimpleSingle2bbin(A,B,C,D)          [0 >= 1 + E] (?,1)
          3.  evalSimpleSingle2bb4in(A,B,C,D)    -> evalSimpleSingle2bbin(A,B,C,D)          [E >= 1]     (?,1)
          4.  evalSimpleSingle2bb4in(A,B,C,D)    -> evalSimpleSingle2returnin(A,B,C,D)      True         (?,1)
          5.  evalSimpleSingle2bbin(A,B,C,D)     -> evalSimpleSingle2bb1in(A,B,C,D)         [C >= 1 + B] (?,1)
          6.  evalSimpleSingle2bbin(A,B,C,D)     -> evalSimpleSingle2bb2in(A,B,C,D)         [B >= C]     (?,1)
          7.  evalSimpleSingle2bb1in(A,B,C,D)    -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (?,1)
          8.  evalSimpleSingle2bb2in(A,B,C,D)    -> evalSimpleSingle2bb3in(A,B,C,D)         [D >= 1 + A] (?,1)
          9.  evalSimpleSingle2bb2in(A,B,C,D)    -> evalSimpleSingle2returnin(A,B,C,D)      [A >= D]     (?,1)
          10. evalSimpleSingle2bb3in(A,B,C,D)    -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (?,1)
          11. evalSimpleSingle2returnin(A,B,C,D) -> evalSimpleSingle2stop(A,B,C,D)          True         (?,1)
        Signature:
          {(evalSimpleSingle2bb1in,4)
          ;(evalSimpleSingle2bb2in,4)
          ;(evalSimpleSingle2bb3in,4)
          ;(evalSimpleSingle2bb4in,4)
          ;(evalSimpleSingle2bbin,4)
          ;(evalSimpleSingle2entryin,4)
          ;(evalSimpleSingle2returnin,4)
          ;(evalSimpleSingle2start,4)
          ;(evalSimpleSingle2stop,4)}
        Flow Graph:
          [0->{1},1->{2,3,4},2->{5,6},3->{5,6},4->{11},5->{7},6->{8,9},7->{2,3,4},8->{10},9->{11},10->{2,3,4}
          ,11->{}]
        Sizebounds:
          (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) 
          (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) 
          (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) 
          (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) 
          (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, C) (< 4,0,D>, D) 
          (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) 
          (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) 
          (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) 
          (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, D) 
          (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) 
          (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, C) (<11,0,D>, D) 
    + Applied Processor:
        LeafRules
    + Details:
        The following transitions are estimated by its predecessors and are removed [4,9,11]
* Step 4: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  evalSimpleSingle2start(A,B,C,D)   -> evalSimpleSingle2entryin(A,B,C,D)       True         (1,1)
          1.  evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D)         True         (?,1)
          2.  evalSimpleSingle2bb4in(A,B,C,D)   -> evalSimpleSingle2bbin(A,B,C,D)          [0 >= 1 + E] (?,1)
          3.  evalSimpleSingle2bb4in(A,B,C,D)   -> evalSimpleSingle2bbin(A,B,C,D)          [E >= 1]     (?,1)
          5.  evalSimpleSingle2bbin(A,B,C,D)    -> evalSimpleSingle2bb1in(A,B,C,D)         [C >= 1 + B] (?,1)
          6.  evalSimpleSingle2bbin(A,B,C,D)    -> evalSimpleSingle2bb2in(A,B,C,D)         [B >= C]     (?,1)
          7.  evalSimpleSingle2bb1in(A,B,C,D)   -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (?,1)
          8.  evalSimpleSingle2bb2in(A,B,C,D)   -> evalSimpleSingle2bb3in(A,B,C,D)         [D >= 1 + A] (?,1)
          10. evalSimpleSingle2bb3in(A,B,C,D)   -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (?,1)
        Signature:
          {(evalSimpleSingle2bb1in,4)
          ;(evalSimpleSingle2bb2in,4)
          ;(evalSimpleSingle2bb3in,4)
          ;(evalSimpleSingle2bb4in,4)
          ;(evalSimpleSingle2bbin,4)
          ;(evalSimpleSingle2entryin,4)
          ;(evalSimpleSingle2returnin,4)
          ;(evalSimpleSingle2start,4)
          ;(evalSimpleSingle2stop,4)}
        Flow Graph:
          [0->{1},1->{2,3},2->{5,6},3->{5,6},5->{7},6->{8},7->{2,3},8->{10},10->{2,3}]
        Sizebounds:
          (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) 
          (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) 
          (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) 
          (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) 
          (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) 
          (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) 
          (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) 
          (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) 
          (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
            p(evalSimpleSingle2bb1in) = 1 + -1*x1 + x4
            p(evalSimpleSingle2bb2in) = 2 + -1*x1 + x4
            p(evalSimpleSingle2bb3in) = 1 + -1*x1 + x4
            p(evalSimpleSingle2bb4in) = 2 + -1*x1 + x4
             p(evalSimpleSingle2bbin) = 2 + -1*x1 + x4
          p(evalSimpleSingle2entryin) = 2 + x4        
            p(evalSimpleSingle2start) = 2 + x4        
        
        The following rules are strictly oriented:
                             [D >= 1 + A] ==>                                
          evalSimpleSingle2bb2in(A,B,C,D)   = 2 + -1*A + D                   
                                            > 1 + -1*A + D                   
                                            = evalSimpleSingle2bb3in(A,B,C,D)
        
        
        The following rules are weakly oriented:
                                       True ==>                                        
            evalSimpleSingle2start(A,B,C,D)   = 2 + D                                  
                                             >= 2 + D                                  
                                              = evalSimpleSingle2entryin(A,B,C,D)      
        
                                       True ==>                                        
          evalSimpleSingle2entryin(A,B,C,D)   = 2 + D                                  
                                             >= 2 + D                                  
                                              = evalSimpleSingle2bb4in(0,0,C,D)        
        
                               [0 >= 1 + E] ==>                                        
            evalSimpleSingle2bb4in(A,B,C,D)   = 2 + -1*A + D                           
                                             >= 2 + -1*A + D                           
                                              = evalSimpleSingle2bbin(A,B,C,D)         
        
                                   [E >= 1] ==>                                        
            evalSimpleSingle2bb4in(A,B,C,D)   = 2 + -1*A + D                           
                                             >= 2 + -1*A + D                           
                                              = evalSimpleSingle2bbin(A,B,C,D)         
        
                               [C >= 1 + B] ==>                                        
             evalSimpleSingle2bbin(A,B,C,D)   = 2 + -1*A + D                           
                                             >= 1 + -1*A + D                           
                                              = evalSimpleSingle2bb1in(A,B,C,D)        
        
                                   [B >= C] ==>                                        
             evalSimpleSingle2bbin(A,B,C,D)   = 2 + -1*A + D                           
                                             >= 2 + -1*A + D                           
                                              = evalSimpleSingle2bb2in(A,B,C,D)        
        
                                       True ==>                                        
            evalSimpleSingle2bb1in(A,B,C,D)   = 1 + -1*A + D                           
                                             >= 1 + -1*A + D                           
                                              = evalSimpleSingle2bb4in(1 + A,1 + B,C,D)
        
                                       True ==>                                        
            evalSimpleSingle2bb3in(A,B,C,D)   = 1 + -1*A + D                           
                                             >= 1 + -1*A + D                           
                                              = evalSimpleSingle2bb4in(1 + A,1 + B,C,D)
        
        
* Step 5: KnowledgePropagation WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  evalSimpleSingle2start(A,B,C,D)   -> evalSimpleSingle2entryin(A,B,C,D)       True         (1,1)    
          1.  evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D)         True         (?,1)    
          2.  evalSimpleSingle2bb4in(A,B,C,D)   -> evalSimpleSingle2bbin(A,B,C,D)          [0 >= 1 + E] (?,1)    
          3.  evalSimpleSingle2bb4in(A,B,C,D)   -> evalSimpleSingle2bbin(A,B,C,D)          [E >= 1]     (?,1)    
          5.  evalSimpleSingle2bbin(A,B,C,D)    -> evalSimpleSingle2bb1in(A,B,C,D)         [C >= 1 + B] (?,1)    
          6.  evalSimpleSingle2bbin(A,B,C,D)    -> evalSimpleSingle2bb2in(A,B,C,D)         [B >= C]     (?,1)    
          7.  evalSimpleSingle2bb1in(A,B,C,D)   -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (?,1)    
          8.  evalSimpleSingle2bb2in(A,B,C,D)   -> evalSimpleSingle2bb3in(A,B,C,D)         [D >= 1 + A] (2 + D,1)
          10. evalSimpleSingle2bb3in(A,B,C,D)   -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (?,1)    
        Signature:
          {(evalSimpleSingle2bb1in,4)
          ;(evalSimpleSingle2bb2in,4)
          ;(evalSimpleSingle2bb3in,4)
          ;(evalSimpleSingle2bb4in,4)
          ;(evalSimpleSingle2bbin,4)
          ;(evalSimpleSingle2entryin,4)
          ;(evalSimpleSingle2returnin,4)
          ;(evalSimpleSingle2start,4)
          ;(evalSimpleSingle2stop,4)}
        Flow Graph:
          [0->{1},1->{2,3},2->{5,6},3->{5,6},5->{7},6->{8},7->{2,3},8->{10},10->{2,3}]
        Sizebounds:
          (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) 
          (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) 
          (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) 
          (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) 
          (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) 
          (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) 
          (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) 
          (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) 
          (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 6: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  evalSimpleSingle2start(A,B,C,D)   -> evalSimpleSingle2entryin(A,B,C,D)       True         (1,1)    
          1.  evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D)         True         (1,1)    
          2.  evalSimpleSingle2bb4in(A,B,C,D)   -> evalSimpleSingle2bbin(A,B,C,D)          [0 >= 1 + E] (?,1)    
          3.  evalSimpleSingle2bb4in(A,B,C,D)   -> evalSimpleSingle2bbin(A,B,C,D)          [E >= 1]     (?,1)    
          5.  evalSimpleSingle2bbin(A,B,C,D)    -> evalSimpleSingle2bb1in(A,B,C,D)         [C >= 1 + B] (?,1)    
          6.  evalSimpleSingle2bbin(A,B,C,D)    -> evalSimpleSingle2bb2in(A,B,C,D)         [B >= C]     (?,1)    
          7.  evalSimpleSingle2bb1in(A,B,C,D)   -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (?,1)    
          8.  evalSimpleSingle2bb2in(A,B,C,D)   -> evalSimpleSingle2bb3in(A,B,C,D)         [D >= 1 + A] (2 + D,1)
          10. evalSimpleSingle2bb3in(A,B,C,D)   -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (2 + D,1)
        Signature:
          {(evalSimpleSingle2bb1in,4)
          ;(evalSimpleSingle2bb2in,4)
          ;(evalSimpleSingle2bb3in,4)
          ;(evalSimpleSingle2bb4in,4)
          ;(evalSimpleSingle2bbin,4)
          ;(evalSimpleSingle2entryin,4)
          ;(evalSimpleSingle2returnin,4)
          ;(evalSimpleSingle2start,4)
          ;(evalSimpleSingle2stop,4)}
        Flow Graph:
          [0->{1},1->{2,3},2->{5,6},3->{5,6},5->{7},6->{8},7->{2,3},8->{10},10->{2,3}]
        Sizebounds:
          (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) 
          (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) 
          (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) 
          (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) 
          (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) 
          (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) 
          (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) 
          (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) 
          (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
            p(evalSimpleSingle2bb1in) = 1 + -1*x2 + x3
            p(evalSimpleSingle2bb2in) = 1 + -1*x2 + x3
            p(evalSimpleSingle2bb3in) = 1 + -1*x2 + x3
            p(evalSimpleSingle2bb4in) = 2 + -1*x2 + x3
             p(evalSimpleSingle2bbin) = 2 + -1*x2 + x3
          p(evalSimpleSingle2entryin) = 2 + x3        
            p(evalSimpleSingle2start) = 2 + x3        
        
        The following rules are strictly oriented:
                            [C >= 1 + B] ==>                                
          evalSimpleSingle2bbin(A,B,C,D)   = 2 + -1*B + C                   
                                           > 1 + -1*B + C                   
                                           = evalSimpleSingle2bb1in(A,B,C,D)
        
        
        The following rules are weakly oriented:
                                       True ==>                                        
            evalSimpleSingle2start(A,B,C,D)   = 2 + C                                  
                                             >= 2 + C                                  
                                              = evalSimpleSingle2entryin(A,B,C,D)      
        
                                       True ==>                                        
          evalSimpleSingle2entryin(A,B,C,D)   = 2 + C                                  
                                             >= 2 + C                                  
                                              = evalSimpleSingle2bb4in(0,0,C,D)        
        
                               [0 >= 1 + E] ==>                                        
            evalSimpleSingle2bb4in(A,B,C,D)   = 2 + -1*B + C                           
                                             >= 2 + -1*B + C                           
                                              = evalSimpleSingle2bbin(A,B,C,D)         
        
                                   [E >= 1] ==>                                        
            evalSimpleSingle2bb4in(A,B,C,D)   = 2 + -1*B + C                           
                                             >= 2 + -1*B + C                           
                                              = evalSimpleSingle2bbin(A,B,C,D)         
        
                                   [B >= C] ==>                                        
             evalSimpleSingle2bbin(A,B,C,D)   = 2 + -1*B + C                           
                                             >= 1 + -1*B + C                           
                                              = evalSimpleSingle2bb2in(A,B,C,D)        
        
                                       True ==>                                        
            evalSimpleSingle2bb1in(A,B,C,D)   = 1 + -1*B + C                           
                                             >= 1 + -1*B + C                           
                                              = evalSimpleSingle2bb4in(1 + A,1 + B,C,D)
        
                               [D >= 1 + A] ==>                                        
            evalSimpleSingle2bb2in(A,B,C,D)   = 1 + -1*B + C                           
                                             >= 1 + -1*B + C                           
                                              = evalSimpleSingle2bb3in(A,B,C,D)        
        
                                       True ==>                                        
            evalSimpleSingle2bb3in(A,B,C,D)   = 1 + -1*B + C                           
                                             >= 1 + -1*B + C                           
                                              = evalSimpleSingle2bb4in(1 + A,1 + B,C,D)
        
        
* Step 7: KnowledgePropagation WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  evalSimpleSingle2start(A,B,C,D)   -> evalSimpleSingle2entryin(A,B,C,D)       True         (1,1)    
          1.  evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D)         True         (1,1)    
          2.  evalSimpleSingle2bb4in(A,B,C,D)   -> evalSimpleSingle2bbin(A,B,C,D)          [0 >= 1 + E] (?,1)    
          3.  evalSimpleSingle2bb4in(A,B,C,D)   -> evalSimpleSingle2bbin(A,B,C,D)          [E >= 1]     (?,1)    
          5.  evalSimpleSingle2bbin(A,B,C,D)    -> evalSimpleSingle2bb1in(A,B,C,D)         [C >= 1 + B] (2 + C,1)
          6.  evalSimpleSingle2bbin(A,B,C,D)    -> evalSimpleSingle2bb2in(A,B,C,D)         [B >= C]     (?,1)    
          7.  evalSimpleSingle2bb1in(A,B,C,D)   -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (?,1)    
          8.  evalSimpleSingle2bb2in(A,B,C,D)   -> evalSimpleSingle2bb3in(A,B,C,D)         [D >= 1 + A] (2 + D,1)
          10. evalSimpleSingle2bb3in(A,B,C,D)   -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (2 + D,1)
        Signature:
          {(evalSimpleSingle2bb1in,4)
          ;(evalSimpleSingle2bb2in,4)
          ;(evalSimpleSingle2bb3in,4)
          ;(evalSimpleSingle2bb4in,4)
          ;(evalSimpleSingle2bbin,4)
          ;(evalSimpleSingle2entryin,4)
          ;(evalSimpleSingle2returnin,4)
          ;(evalSimpleSingle2start,4)
          ;(evalSimpleSingle2stop,4)}
        Flow Graph:
          [0->{1},1->{2,3},2->{5,6},3->{5,6},5->{7},6->{8},7->{2,3},8->{10},10->{2,3}]
        Sizebounds:
          (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) 
          (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) 
          (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) 
          (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) 
          (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) 
          (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) 
          (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) 
          (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) 
          (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 8: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  evalSimpleSingle2start(A,B,C,D)   -> evalSimpleSingle2entryin(A,B,C,D)       True         (1,1)        
          1.  evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D)         True         (1,1)        
          2.  evalSimpleSingle2bb4in(A,B,C,D)   -> evalSimpleSingle2bbin(A,B,C,D)          [0 >= 1 + E] (?,1)        
          3.  evalSimpleSingle2bb4in(A,B,C,D)   -> evalSimpleSingle2bbin(A,B,C,D)          [E >= 1]     (5 + C + D,1)
          5.  evalSimpleSingle2bbin(A,B,C,D)    -> evalSimpleSingle2bb1in(A,B,C,D)         [C >= 1 + B] (2 + C,1)    
          6.  evalSimpleSingle2bbin(A,B,C,D)    -> evalSimpleSingle2bb2in(A,B,C,D)         [B >= C]     (?,1)        
          7.  evalSimpleSingle2bb1in(A,B,C,D)   -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (2 + C,1)    
          8.  evalSimpleSingle2bb2in(A,B,C,D)   -> evalSimpleSingle2bb3in(A,B,C,D)         [D >= 1 + A] (2 + D,1)    
          10. evalSimpleSingle2bb3in(A,B,C,D)   -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (2 + D,1)    
        Signature:
          {(evalSimpleSingle2bb1in,4)
          ;(evalSimpleSingle2bb2in,4)
          ;(evalSimpleSingle2bb3in,4)
          ;(evalSimpleSingle2bb4in,4)
          ;(evalSimpleSingle2bbin,4)
          ;(evalSimpleSingle2entryin,4)
          ;(evalSimpleSingle2returnin,4)
          ;(evalSimpleSingle2start,4)
          ;(evalSimpleSingle2stop,4)}
        Flow Graph:
          [0->{1},1->{2,3},2->{5,6},3->{5,6},5->{7},6->{8},7->{2,3},8->{10},10->{2,3}]
        Sizebounds:
          (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) 
          (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) 
          (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) 
          (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) 
          (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) 
          (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) 
          (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) 
          (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) 
          (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [2,7,5,3,10,6], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(evalSimpleSingle2bb1in) = 1
          p(evalSimpleSingle2bb2in) = 0
          p(evalSimpleSingle2bb3in) = 1
          p(evalSimpleSingle2bb4in) = 1
           p(evalSimpleSingle2bbin) = 1
        
        The following rules are strictly oriented:
                                [B >= C] ==>                                
          evalSimpleSingle2bbin(A,B,C,D)   = 1                              
                                           > 0                              
                                           = evalSimpleSingle2bb2in(A,B,C,D)
        
        
        The following rules are weakly oriented:
                             [0 >= 1 + E] ==>                                        
          evalSimpleSingle2bb4in(A,B,C,D)   = 1                                      
                                           >= 1                                      
                                            = evalSimpleSingle2bbin(A,B,C,D)         
        
                                 [E >= 1] ==>                                        
          evalSimpleSingle2bb4in(A,B,C,D)   = 1                                      
                                           >= 1                                      
                                            = evalSimpleSingle2bbin(A,B,C,D)         
        
                             [C >= 1 + B] ==>                                        
           evalSimpleSingle2bbin(A,B,C,D)   = 1                                      
                                           >= 1                                      
                                            = evalSimpleSingle2bb1in(A,B,C,D)        
        
                                     True ==>                                        
          evalSimpleSingle2bb1in(A,B,C,D)   = 1                                      
                                           >= 1                                      
                                            = evalSimpleSingle2bb4in(1 + A,1 + B,C,D)
        
                                     True ==>                                        
          evalSimpleSingle2bb3in(A,B,C,D)   = 1                                      
                                           >= 1                                      
                                            = evalSimpleSingle2bb4in(1 + A,1 + B,C,D)
        
        We use the following global sizebounds:
        (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) 
        (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) 
        (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) 
        (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) 
        (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) 
        (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) 
        (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) 
        (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) 
        (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) 
* Step 9: KnowledgePropagation WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  evalSimpleSingle2start(A,B,C,D)   -> evalSimpleSingle2entryin(A,B,C,D)       True         (1,1)        
          1.  evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D)         True         (1,1)        
          2.  evalSimpleSingle2bb4in(A,B,C,D)   -> evalSimpleSingle2bbin(A,B,C,D)          [0 >= 1 + E] (?,1)        
          3.  evalSimpleSingle2bb4in(A,B,C,D)   -> evalSimpleSingle2bbin(A,B,C,D)          [E >= 1]     (5 + C + D,1)
          5.  evalSimpleSingle2bbin(A,B,C,D)    -> evalSimpleSingle2bb1in(A,B,C,D)         [C >= 1 + B] (2 + C,1)    
          6.  evalSimpleSingle2bbin(A,B,C,D)    -> evalSimpleSingle2bb2in(A,B,C,D)         [B >= C]     (3 + D,1)    
          7.  evalSimpleSingle2bb1in(A,B,C,D)   -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (2 + C,1)    
          8.  evalSimpleSingle2bb2in(A,B,C,D)   -> evalSimpleSingle2bb3in(A,B,C,D)         [D >= 1 + A] (2 + D,1)    
          10. evalSimpleSingle2bb3in(A,B,C,D)   -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (2 + D,1)    
        Signature:
          {(evalSimpleSingle2bb1in,4)
          ;(evalSimpleSingle2bb2in,4)
          ;(evalSimpleSingle2bb3in,4)
          ;(evalSimpleSingle2bb4in,4)
          ;(evalSimpleSingle2bbin,4)
          ;(evalSimpleSingle2entryin,4)
          ;(evalSimpleSingle2returnin,4)
          ;(evalSimpleSingle2start,4)
          ;(evalSimpleSingle2stop,4)}
        Flow Graph:
          [0->{1},1->{2,3},2->{5,6},3->{5,6},5->{7},6->{8},7->{2,3},8->{10},10->{2,3}]
        Sizebounds:
          (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) 
          (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) 
          (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) 
          (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) 
          (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) 
          (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) 
          (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) 
          (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) 
          (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 10: LocalSizeboundsProc WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  evalSimpleSingle2start(A,B,C,D)   -> evalSimpleSingle2entryin(A,B,C,D)       True         (1,1)        
          1.  evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D)         True         (1,1)        
          2.  evalSimpleSingle2bb4in(A,B,C,D)   -> evalSimpleSingle2bbin(A,B,C,D)          [0 >= 1 + E] (5 + C + D,1)
          3.  evalSimpleSingle2bb4in(A,B,C,D)   -> evalSimpleSingle2bbin(A,B,C,D)          [E >= 1]     (5 + C + D,1)
          5.  evalSimpleSingle2bbin(A,B,C,D)    -> evalSimpleSingle2bb1in(A,B,C,D)         [C >= 1 + B] (2 + C,1)    
          6.  evalSimpleSingle2bbin(A,B,C,D)    -> evalSimpleSingle2bb2in(A,B,C,D)         [B >= C]     (3 + D,1)    
          7.  evalSimpleSingle2bb1in(A,B,C,D)   -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (2 + C,1)    
          8.  evalSimpleSingle2bb2in(A,B,C,D)   -> evalSimpleSingle2bb3in(A,B,C,D)         [D >= 1 + A] (2 + D,1)    
          10. evalSimpleSingle2bb3in(A,B,C,D)   -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (2 + D,1)    
        Signature:
          {(evalSimpleSingle2bb1in,4)
          ;(evalSimpleSingle2bb2in,4)
          ;(evalSimpleSingle2bb3in,4)
          ;(evalSimpleSingle2bb4in,4)
          ;(evalSimpleSingle2bbin,4)
          ;(evalSimpleSingle2entryin,4)
          ;(evalSimpleSingle2returnin,4)
          ;(evalSimpleSingle2start,4)
          ;(evalSimpleSingle2stop,4)}
        Flow Graph:
          [0->{1},1->{2,3},2->{5,6},3->{5,6},5->{7},6->{8},7->{2,3},8->{10},10->{2,3}]
        Sizebounds:
          (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) 
          (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) 
          (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) 
          (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) 
          (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) 
          (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) 
          (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) 
          (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) 
          (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) 
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        The problem is already solved.

WORST_CASE(?,O(n^1))