WORST_CASE(?,O(1))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A,B,C,D,E,F,G)  -> f5(0,B,C,D,E,F,G)            True                     (1,1)
          1.  f5(A,B,C,D,E,F,G)  -> f5(1 + A,B,C,D,E,F,G)        [99 >= A]                (?,1)
          2.  f17(A,B,C,D,E,F,G) -> f17(A,B,C,D,E,F,G)           True                     (?,1)
          3.  f17(A,B,C,D,E,F,G) -> f17(A,1 + B,C,D,E,F,G)       [0 >= 1 + H]             (?,1)
          4.  f17(A,B,C,D,E,F,G) -> f17(A,1 + B,C,D,E,F,G)       True                     (?,1)
          5.  f32(A,B,C,D,E,F,G) -> f32(A,B,C,D,E,F,G)           True                     (?,1)
          6.  f32(A,B,C,D,E,F,G) -> f32(A,B,1 + C,D,E,F,G)       [0 >= 1 + H]             (?,1)
          7.  f32(A,B,C,D,E,F,G) -> f32(A,B,1 + C,D,E,F,G)       True                     (?,1)
          8.  f32(A,B,C,D,E,F,G) -> f13(A,B,C,C,C,F,G)           True                     (?,1)
          9.  f17(A,B,C,D,E,F,G) -> f32(A,B,B,B,E,B,H)           [0 >= 1 + I]             (?,1)
          10. f17(A,B,C,D,E,F,G) -> f32(A,B,B,B,E,B,H)           True                     (?,1)
          11. f17(A,B,C,D,E,F,G) -> f13(A,B,C,B,E,B,H)           True                     (?,1)
          12. f5(A,B,C,D,E,F,G)  -> f13(A,B,C,-2 + A,E,F,G)      [A >= 100]               (?,1)
          13. f5(A,B,C,D,E,F,G)  -> f17(A,-2 + A,C,-2 + A,E,F,G) [0 >= 1 + A && A >= 100] (?,1)
        Signature:
          {(f0,7);(f13,7);(f17,7);(f32,7);(f5,7)}
        Flow Graph:
          [0->{1,12,13},1->{1,12,13},2->{2,3,4,9,10,11},3->{2,3,4,9,10,11},4->{2,3,4,9,10,11},5->{5,6,7,8},6->{5,6,7
          ,8},7->{5,6,7,8},8->{},9->{5,6,7,8},10->{5,6,7,8},11->{},12->{},13->{2,3,4,9,10,11}]
        
    + Applied Processor:
        RestrictVarsProcessor
    + Details:
        We removed the arguments [D,E,F,G] .
* Step 2: UnsatRules WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A,B,C)  -> f5(0,B,C)       True                     (1,1)
          1.  f5(A,B,C)  -> f5(1 + A,B,C)   [99 >= A]                (?,1)
          2.  f17(A,B,C) -> f17(A,B,C)      True                     (?,1)
          3.  f17(A,B,C) -> f17(A,1 + B,C)  [0 >= 1 + H]             (?,1)
          4.  f17(A,B,C) -> f17(A,1 + B,C)  True                     (?,1)
          5.  f32(A,B,C) -> f32(A,B,C)      True                     (?,1)
          6.  f32(A,B,C) -> f32(A,B,1 + C)  [0 >= 1 + H]             (?,1)
          7.  f32(A,B,C) -> f32(A,B,1 + C)  True                     (?,1)
          8.  f32(A,B,C) -> f13(A,B,C)      True                     (?,1)
          9.  f17(A,B,C) -> f32(A,B,B)      [0 >= 1 + I]             (?,1)
          10. f17(A,B,C) -> f32(A,B,B)      True                     (?,1)
          11. f17(A,B,C) -> f13(A,B,C)      True                     (?,1)
          12. f5(A,B,C)  -> f13(A,B,C)      [A >= 100]               (?,1)
          13. f5(A,B,C)  -> f17(A,-2 + A,C) [0 >= 1 + A && A >= 100] (?,1)
        Signature:
          {(f0,3);(f13,3);(f17,3);(f32,3);(f5,3)}
        Flow Graph:
          [0->{1,12,13},1->{1,12,13},2->{2,3,4,9,10,11},3->{2,3,4,9,10,11},4->{2,3,4,9,10,11},5->{5,6,7,8},6->{5,6,7
          ,8},7->{5,6,7,8},8->{},9->{5,6,7,8},10->{5,6,7,8},11->{},12->{},13->{2,3,4,9,10,11}]
        
    + Applied Processor:
        UnsatRules
    + Details:
        The following transitions have unsatisfiable constraints and are removed:  [13]
* Step 3: UnreachableRules WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A,B,C)  -> f5(0,B,C)      True         (1,1)
          1.  f5(A,B,C)  -> f5(1 + A,B,C)  [99 >= A]    (?,1)
          2.  f17(A,B,C) -> f17(A,B,C)     True         (?,1)
          3.  f17(A,B,C) -> f17(A,1 + B,C) [0 >= 1 + H] (?,1)
          4.  f17(A,B,C) -> f17(A,1 + B,C) True         (?,1)
          5.  f32(A,B,C) -> f32(A,B,C)     True         (?,1)
          6.  f32(A,B,C) -> f32(A,B,1 + C) [0 >= 1 + H] (?,1)
          7.  f32(A,B,C) -> f32(A,B,1 + C) True         (?,1)
          8.  f32(A,B,C) -> f13(A,B,C)     True         (?,1)
          9.  f17(A,B,C) -> f32(A,B,B)     [0 >= 1 + I] (?,1)
          10. f17(A,B,C) -> f32(A,B,B)     True         (?,1)
          11. f17(A,B,C) -> f13(A,B,C)     True         (?,1)
          12. f5(A,B,C)  -> f13(A,B,C)     [A >= 100]   (?,1)
        Signature:
          {(f0,3);(f13,3);(f17,3);(f32,3);(f5,3)}
        Flow Graph:
          [0->{1,12},1->{1,12},2->{2,3,4,9,10,11},3->{2,3,4,9,10,11},4->{2,3,4,9,10,11},5->{5,6,7,8},6->{5,6,7,8}
          ,7->{5,6,7,8},8->{},9->{5,6,7,8},10->{5,6,7,8},11->{},12->{}]
        
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [2
                                                                                              ,3
                                                                                              ,4
                                                                                              ,5
                                                                                              ,6
                                                                                              ,7
                                                                                              ,8
                                                                                              ,9
                                                                                              ,10
                                                                                              ,11]
* Step 4: LocalSizeboundsProc WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A,B,C) -> f5(0,B,C)     True       (1,1)
          1.  f5(A,B,C) -> f5(1 + A,B,C) [99 >= A]  (?,1)
          12. f5(A,B,C) -> f13(A,B,C)    [A >= 100] (?,1)
        Signature:
          {(f0,3);(f13,3);(f17,3);(f32,3);(f5,3)}
        Flow Graph:
          [0->{1,12},1->{1,12},12->{}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (< 0,0,A>,     0, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,C>, C, .= 0) 
          (< 1,0,A>, 1 + A, .+ 1) (< 1,0,B>, B, .= 0) (< 1,0,C>, C, .= 0) 
          (<12,0,A>,     A, .= 0) (<12,0,B>, B, .= 0) (<12,0,C>, C, .= 0) 
* Step 5: SizeboundsProc WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A,B,C) -> f5(0,B,C)     True       (1,1)
          1.  f5(A,B,C) -> f5(1 + A,B,C) [99 >= A]  (?,1)
          12. f5(A,B,C) -> f13(A,B,C)    [A >= 100] (?,1)
        Signature:
          {(f0,3);(f13,3);(f17,3);(f32,3);(f5,3)}
        Flow Graph:
          [0->{1,12},1->{1,12},12->{}]
        Sizebounds:
          (< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) 
          (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) 
          (<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (< 0,0,A>,   0) (< 0,0,B>, B) (< 0,0,C>, C) 
          (< 1,0,A>, 100) (< 1,0,B>, B) (< 1,0,C>, C) 
          (<12,0,A>, 100) (<12,0,B>, B) (<12,0,C>, C) 
* Step 6: UnsatPaths WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A,B,C) -> f5(0,B,C)     True       (1,1)
          1.  f5(A,B,C) -> f5(1 + A,B,C) [99 >= A]  (?,1)
          12. f5(A,B,C) -> f13(A,B,C)    [A >= 100] (?,1)
        Signature:
          {(f0,3);(f13,3);(f17,3);(f32,3);(f5,3)}
        Flow Graph:
          [0->{1,12},1->{1,12},12->{}]
        Sizebounds:
          (< 0,0,A>,   0) (< 0,0,B>, B) (< 0,0,C>, C) 
          (< 1,0,A>, 100) (< 1,0,B>, B) (< 1,0,C>, C) 
          (<12,0,A>, 100) (<12,0,B>, B) (<12,0,C>, C) 
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(0,12)]
* Step 7: LeafRules WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A,B,C) -> f5(0,B,C)     True       (1,1)
          1.  f5(A,B,C) -> f5(1 + A,B,C) [99 >= A]  (?,1)
          12. f5(A,B,C) -> f13(A,B,C)    [A >= 100] (?,1)
        Signature:
          {(f0,3);(f13,3);(f17,3);(f32,3);(f5,3)}
        Flow Graph:
          [0->{1},1->{1,12},12->{}]
        Sizebounds:
          (< 0,0,A>,   0) (< 0,0,B>, B) (< 0,0,C>, C) 
          (< 1,0,A>, 100) (< 1,0,B>, B) (< 1,0,C>, C) 
          (<12,0,A>, 100) (<12,0,B>, B) (<12,0,C>, C) 
    + Applied Processor:
        LeafRules
    + Details:
        The following transitions are estimated by its predecessors and are removed [12]
* Step 8: PolyRank WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0. f0(A,B,C) -> f5(0,B,C)     True      (1,1)
          1. f5(A,B,C) -> f5(1 + A,B,C) [99 >= A] (?,1)
        Signature:
          {(f0,3);(f13,3);(f17,3);(f32,3);(f5,3)}
        Flow Graph:
          [0->{1},1->{1}]
        Sizebounds:
          (<0,0,A>,   0) (<0,0,B>, B) (<0,0,C>, C) 
          (<1,0,A>, 100) (<1,0,B>, B) (<1,0,C>, C) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(f0) = 100        
          p(f5) = 100 + -1*x1
        
        The following rules are strictly oriented:
          [99 >= A] ==>              
          f5(A,B,C)   = 100 + -1*A   
                      > 99 + -1*A    
                      = f5(1 + A,B,C)
        
        
        The following rules are weakly oriented:
               True ==>          
          f0(A,B,C)   = 100      
                     >= 100      
                      = f5(0,B,C)
        
        
* Step 9: KnowledgePropagation WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0. f0(A,B,C) -> f5(0,B,C)     True      (1,1)  
          1. f5(A,B,C) -> f5(1 + A,B,C) [99 >= A] (100,1)
        Signature:
          {(f0,3);(f13,3);(f17,3);(f32,3);(f5,3)}
        Flow Graph:
          [0->{1},1->{1}]
        Sizebounds:
          (<0,0,A>,   0) (<0,0,B>, B) (<0,0,C>, C) 
          (<1,0,A>, 100) (<1,0,B>, B) (<1,0,C>, C) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        The problem is already solved.

WORST_CASE(?,O(1))