WORST_CASE(?,O(1))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0. f0(A,B,C)  -> f9(0,D,0)      True      (1,1)
          1. f9(A,B,C)  -> f9(A,B,1 + C)  [49 >= C] (?,1)
          2. f17(A,B,C) -> f17(1 + A,B,C) [49 >= A] (?,1)
          3. f17(A,B,C) -> f24(A,B,C)     [A >= 50] (?,1)
          4. f9(A,B,C)  -> f17(0,B,C)     [C >= 50] (?,1)
        Signature:
          {(f0,3);(f17,3);(f24,3);(f9,3)}
        Flow Graph:
          [0->{1,4},1->{1,4},2->{2,3},3->{},4->{2,3}]
        
    + Applied Processor:
        RestrictVarsProcessor
    + Details:
        We removed the arguments [B] .
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0. f0(A,C)  -> f9(0,0)      True      (1,1)
          1. f9(A,C)  -> f9(A,1 + C)  [49 >= C] (?,1)
          2. f17(A,C) -> f17(1 + A,C) [49 >= A] (?,1)
          3. f17(A,C) -> f24(A,C)     [A >= 50] (?,1)
          4. f9(A,C)  -> f17(0,C)     [C >= 50] (?,1)
        Signature:
          {(f0,2);(f17,2);(f24,2);(f9,2)}
        Flow Graph:
          [0->{1,4},1->{1,4},2->{2,3},3->{},4->{2,3}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (<0,0,A>,     0, .= 0) (<0,0,C>,     0, .= 0) 
          (<1,0,A>,     A, .= 0) (<1,0,C>, 1 + C, .+ 1) 
          (<2,0,A>, 1 + A, .+ 1) (<2,0,C>,     C, .= 0) 
          (<3,0,A>,     A, .= 0) (<3,0,C>,     C, .= 0) 
          (<4,0,A>,     0, .= 0) (<4,0,C>,     C, .= 0) 
* Step 3: SizeboundsProc WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0. f0(A,C)  -> f9(0,0)      True      (1,1)
          1. f9(A,C)  -> f9(A,1 + C)  [49 >= C] (?,1)
          2. f17(A,C) -> f17(1 + A,C) [49 >= A] (?,1)
          3. f17(A,C) -> f24(A,C)     [A >= 50] (?,1)
          4. f9(A,C)  -> f17(0,C)     [C >= 50] (?,1)
        Signature:
          {(f0,2);(f17,2);(f24,2);(f9,2)}
        Flow Graph:
          [0->{1,4},1->{1,4},2->{2,3},3->{},4->{2,3}]
        Sizebounds:
          (<0,0,A>, ?) (<0,0,C>, ?) 
          (<1,0,A>, ?) (<1,0,C>, ?) 
          (<2,0,A>, ?) (<2,0,C>, ?) 
          (<3,0,A>, ?) (<3,0,C>, ?) 
          (<4,0,A>, ?) (<4,0,C>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (<0,0,A>,  0) (<0,0,C>,  0) 
          (<1,0,A>,  0) (<1,0,C>, 50) 
          (<2,0,A>, 50) (<2,0,C>, 50) 
          (<3,0,A>, 50) (<3,0,C>, 50) 
          (<4,0,A>,  0) (<4,0,C>, 50) 
* Step 4: UnsatPaths WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0. f0(A,C)  -> f9(0,0)      True      (1,1)
          1. f9(A,C)  -> f9(A,1 + C)  [49 >= C] (?,1)
          2. f17(A,C) -> f17(1 + A,C) [49 >= A] (?,1)
          3. f17(A,C) -> f24(A,C)     [A >= 50] (?,1)
          4. f9(A,C)  -> f17(0,C)     [C >= 50] (?,1)
        Signature:
          {(f0,2);(f17,2);(f24,2);(f9,2)}
        Flow Graph:
          [0->{1,4},1->{1,4},2->{2,3},3->{},4->{2,3}]
        Sizebounds:
          (<0,0,A>,  0) (<0,0,C>,  0) 
          (<1,0,A>,  0) (<1,0,C>, 50) 
          (<2,0,A>, 50) (<2,0,C>, 50) 
          (<3,0,A>, 50) (<3,0,C>, 50) 
          (<4,0,A>,  0) (<4,0,C>, 50) 
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(0,4),(4,3)]
* Step 5: LeafRules WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0. f0(A,C)  -> f9(0,0)      True      (1,1)
          1. f9(A,C)  -> f9(A,1 + C)  [49 >= C] (?,1)
          2. f17(A,C) -> f17(1 + A,C) [49 >= A] (?,1)
          3. f17(A,C) -> f24(A,C)     [A >= 50] (?,1)
          4. f9(A,C)  -> f17(0,C)     [C >= 50] (?,1)
        Signature:
          {(f0,2);(f17,2);(f24,2);(f9,2)}
        Flow Graph:
          [0->{1},1->{1,4},2->{2,3},3->{},4->{2}]
        Sizebounds:
          (<0,0,A>,  0) (<0,0,C>,  0) 
          (<1,0,A>,  0) (<1,0,C>, 50) 
          (<2,0,A>, 50) (<2,0,C>, 50) 
          (<3,0,A>, 50) (<3,0,C>, 50) 
          (<4,0,A>,  0) (<4,0,C>, 50) 
    + Applied Processor:
        LeafRules
    + Details:
        The following transitions are estimated by its predecessors and are removed [3]
* Step 6: PolyRank WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0. f0(A,C)  -> f9(0,0)      True      (1,1)
          1. f9(A,C)  -> f9(A,1 + C)  [49 >= C] (?,1)
          2. f17(A,C) -> f17(1 + A,C) [49 >= A] (?,1)
          4. f9(A,C)  -> f17(0,C)     [C >= 50] (?,1)
        Signature:
          {(f0,2);(f17,2);(f24,2);(f9,2)}
        Flow Graph:
          [0->{1},1->{1,4},2->{2},4->{2}]
        Sizebounds:
          (<0,0,A>,  0) (<0,0,C>,  0) 
          (<1,0,A>,  0) (<1,0,C>, 50) 
          (<2,0,A>, 50) (<2,0,C>, 50) 
          (<4,0,A>,  0) (<4,0,C>, 50) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
           p(f0) = 1
          p(f17) = 0
           p(f9) = 1
        
        The following rules are strictly oriented:
        [C >= 50] ==>         
          f9(A,C)   = 1       
                    > 0       
                    = f17(0,C)
        
        
        The following rules are weakly oriented:
              True ==>             
           f0(A,C)   = 1           
                    >= 1           
                     = f9(0,0)     
        
         [49 >= C] ==>             
           f9(A,C)   = 1           
                    >= 1           
                     = f9(A,1 + C) 
        
         [49 >= A] ==>             
          f17(A,C)   = 0           
                    >= 0           
                     = f17(1 + A,C)
        
        
* Step 7: PolyRank WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0. f0(A,C)  -> f9(0,0)      True      (1,1)
          1. f9(A,C)  -> f9(A,1 + C)  [49 >= C] (?,1)
          2. f17(A,C) -> f17(1 + A,C) [49 >= A] (?,1)
          4. f9(A,C)  -> f17(0,C)     [C >= 50] (1,1)
        Signature:
          {(f0,2);(f17,2);(f24,2);(f9,2)}
        Flow Graph:
          [0->{1},1->{1,4},2->{2},4->{2}]
        Sizebounds:
          (<0,0,A>,  0) (<0,0,C>,  0) 
          (<1,0,A>,  0) (<1,0,C>, 50) 
          (<2,0,A>, 50) (<2,0,C>, 50) 
          (<4,0,A>,  0) (<4,0,C>, 50) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
           p(f0) = 50        
          p(f17) = 50 + -1*x1
           p(f9) = 50        
        
        The following rules are strictly oriented:
         [49 >= A] ==>             
          f17(A,C)   = 50 + -1*A   
                     > 49 + -1*A   
                     = f17(1 + A,C)
        
        
        The following rules are weakly oriented:
             True ==>            
          f0(A,C)   = 50         
                   >= 50         
                    = f9(0,0)    
        
        [49 >= C] ==>            
          f9(A,C)   = 50         
                   >= 50         
                    = f9(A,1 + C)
        
        [C >= 50] ==>            
          f9(A,C)   = 50         
                   >= 50         
                    = f17(0,C)   
        
        
* Step 8: PolyRank WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0. f0(A,C)  -> f9(0,0)      True      (1,1) 
          1. f9(A,C)  -> f9(A,1 + C)  [49 >= C] (?,1) 
          2. f17(A,C) -> f17(1 + A,C) [49 >= A] (50,1)
          4. f9(A,C)  -> f17(0,C)     [C >= 50] (1,1) 
        Signature:
          {(f0,2);(f17,2);(f24,2);(f9,2)}
        Flow Graph:
          [0->{1},1->{1,4},2->{2},4->{2}]
        Sizebounds:
          (<0,0,A>,  0) (<0,0,C>,  0) 
          (<1,0,A>,  0) (<1,0,C>, 50) 
          (<2,0,A>, 50) (<2,0,C>, 50) 
          (<4,0,A>,  0) (<4,0,C>, 50) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
           p(f0) = 50        
          p(f17) = -1*x2     
           p(f9) = 50 + -1*x2
        
        The following rules are strictly oriented:
        [49 >= C] ==>            
          f9(A,C)   = 50 + -1*C  
                    > 49 + -1*C  
                    = f9(A,1 + C)
        
        
        The following rules are weakly oriented:
              True ==>             
           f0(A,C)   = 50          
                    >= 50          
                     = f9(0,0)     
        
         [49 >= A] ==>             
          f17(A,C)   = -1*C        
                    >= -1*C        
                     = f17(1 + A,C)
        
         [C >= 50] ==>             
           f9(A,C)   = 50 + -1*C   
                    >= -1*C        
                     = f17(0,C)    
        
        
* Step 9: KnowledgePropagation WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0. f0(A,C)  -> f9(0,0)      True      (1,1) 
          1. f9(A,C)  -> f9(A,1 + C)  [49 >= C] (50,1)
          2. f17(A,C) -> f17(1 + A,C) [49 >= A] (50,1)
          4. f9(A,C)  -> f17(0,C)     [C >= 50] (1,1) 
        Signature:
          {(f0,2);(f17,2);(f24,2);(f9,2)}
        Flow Graph:
          [0->{1},1->{1,4},2->{2},4->{2}]
        Sizebounds:
          (<0,0,A>,  0) (<0,0,C>,  0) 
          (<1,0,A>,  0) (<1,0,C>, 50) 
          (<2,0,A>, 50) (<2,0,C>, 50) 
          (<4,0,A>,  0) (<4,0,C>, 50) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        The problem is already solved.

WORST_CASE(?,O(1))