MAYBE
* Step 1: ArgumentFilter MAYBE
    + Considered Problem:
        Rules:
          0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,1 + B,1 + C,S,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)        [A >= 1 + B && C >= 0]                         (?,1)
          1. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f0(A,B,C,D,E,F,S,G,V,W,X,L,M,N,O,P,Q,R)                [U >= 1 + T && E >= 1 && F >= 0]               (?,1)
          2. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,M,0,W,X,K,M,N,V,S,E,Q,R)       [T >= U && E >= 0 && F >= 0 && H = 0]          (?,1)
          3. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f12(A,B,C,D,E,F,G,0,V,W,K,M,M,0,O,E,S,R)               [X >= T && E >= 0 && F >= 0 && N = 0 && H = 0] (?,1)
          4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1,-3 + C + T,S,0,U,A1,K,S,V,X,W,P,D,-2 + C) [C >= 2 && B >= A && Y >= Z]                   (?,1)
          5. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(17,1,0,S,E,F,G,H,I,J,K,V,M,N,O,P,Q,R)               True                                           (1,1)
        Signature:
          {(f0,18);(f12,18);(f5,18);(f6,18);(f9,18)}
        Flow Graph:
          [0->{0,4},1->{},2->{1,2,3},3->{},4->{1,2,3},5->{0,4}]
        
    + Applied Processor:
        ArgumentFilter [3,6,8,9,10,11,12,14,15,16,17]
    + Details:
        We remove following argument positions: [3,6,8,9,10,11,12,14,15,16,17].
* Step 2: UnsatPaths MAYBE
    + Considered Problem:
        Rules:
          0. f9(A,B,C,E,F,H,N) -> f9(A,1 + B,1 + C,E,F,H,N)  [A >= 1 + B && C >= 0]                         (?,1)
          1. f5(A,B,C,E,F,H,N) -> f0(A,B,C,E,F,G,N)          [U >= 1 + T && E >= 1 && F >= 0]               (?,1)
          2. f5(A,B,C,E,F,H,N) -> f5(A,B,C,1 + E,-1 + F,0,V) [T >= U && E >= 0 && F >= 0 && H = 0]          (?,1)
          3. f5(A,B,C,E,F,H,N) -> f12(A,B,C,E,F,0,0)         [X >= T && E >= 0 && F >= 0 && N = 0 && H = 0] (?,1)
          4. f9(A,B,C,E,F,H,N) -> f5(A,B,C,1,-3 + C + T,0,X) [C >= 2 && B >= A && Y >= Z]                   (?,1)
          5. f6(A,B,C,E,F,H,N) -> f9(17,1,0,E,F,H,N)         True                                           (1,1)
        Signature:
          {(f0,18);(f12,18);(f5,18);(f6,18);(f9,18)}
        Flow Graph:
          [0->{0,4},1->{},2->{1,2,3},3->{},4->{1,2,3},5->{0,4}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(5,4)]
* Step 3: FromIts MAYBE
    + Considered Problem:
        Rules:
          0. f9(A,B,C,E,F,H,N) -> f9(A,1 + B,1 + C,E,F,H,N)  [A >= 1 + B && C >= 0]                         (?,1)
          1. f5(A,B,C,E,F,H,N) -> f0(A,B,C,E,F,G,N)          [U >= 1 + T && E >= 1 && F >= 0]               (?,1)
          2. f5(A,B,C,E,F,H,N) -> f5(A,B,C,1 + E,-1 + F,0,V) [T >= U && E >= 0 && F >= 0 && H = 0]          (?,1)
          3. f5(A,B,C,E,F,H,N) -> f12(A,B,C,E,F,0,0)         [X >= T && E >= 0 && F >= 0 && N = 0 && H = 0] (?,1)
          4. f9(A,B,C,E,F,H,N) -> f5(A,B,C,1,-3 + C + T,0,X) [C >= 2 && B >= A && Y >= Z]                   (?,1)
          5. f6(A,B,C,E,F,H,N) -> f9(17,1,0,E,F,H,N)         True                                           (1,1)
        Signature:
          {(f0,18);(f12,18);(f5,18);(f6,18);(f9,18)}
        Flow Graph:
          [0->{0,4},1->{},2->{1,2,3},3->{},4->{1,2,3},5->{0}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 4: Unfold MAYBE
    + Considered Problem:
        Rules:
          f9(A,B,C,E,F,H,N) -> f9(A,1 + B,1 + C,E,F,H,N)   [A >= 1 + B && C >= 0]
          f5(A,B,C,E,F,H,N) -> f0(A,B,C,E,F,G,N)           [U >= 1 + T && E >= 1 && F >= 0]
          f5(A,B,C,E,F,H,N) -> f5(A,B,C,1 + E,-1 + F,0,V)  [T >= U && E >= 0 && F >= 0 && H = 0]
          f5(A,B,C,E,F,H,N) -> f12(A,B,C,E,F,0,0)          [X >= T && E >= 0 && F >= 0 && N = 0 && H = 0]
          f9(A,B,C,E,F,H,N) -> f5(A,B,C,1,-3 + C + T,0,X)  [C >= 2 && B >= A && Y >= Z]
          f6(A,B,C,E,F,H,N) -> f9(17,1,0,E,F,H,N)          True
        Signature:
          {(f0,18);(f12,18);(f5,18);(f6,18);(f9,18)}
        Rule Graph:
          [0->{0,4},1->{},2->{1,2,3},3->{},4->{1,2,3},5->{0}]
    + Applied Processor:
        Unfold
    + Details:
        ()
* Step 5: AddSinks MAYBE
    + Considered Problem:
        Rules:
          f9.0(A,B,C,E,F,H,N) -> f9.0(A,1 + B,1 + C,E,F,H,N)   [A >= 1 + B && C >= 0]
          f9.0(A,B,C,E,F,H,N) -> f9.4(A,1 + B,1 + C,E,F,H,N)   [A >= 1 + B && C >= 0]
          f5.1(A,B,C,E,F,H,N) -> f0.6(A,B,C,E,F,G,N)           [U >= 1 + T && E >= 1 && F >= 0]
          f5.2(A,B,C,E,F,H,N) -> f5.1(A,B,C,1 + E,-1 + F,0,V)  [T >= U && E >= 0 && F >= 0 && H = 0]
          f5.2(A,B,C,E,F,H,N) -> f5.2(A,B,C,1 + E,-1 + F,0,V)  [T >= U && E >= 0 && F >= 0 && H = 0]
          f5.2(A,B,C,E,F,H,N) -> f5.3(A,B,C,1 + E,-1 + F,0,V)  [T >= U && E >= 0 && F >= 0 && H = 0]
          f5.3(A,B,C,E,F,H,N) -> f12.6(A,B,C,E,F,0,0)          [X >= T && E >= 0 && F >= 0 && N = 0 && H = 0]
          f9.4(A,B,C,E,F,H,N) -> f5.1(A,B,C,1,-3 + C + T,0,X)  [C >= 2 && B >= A && Y >= Z]
          f9.4(A,B,C,E,F,H,N) -> f5.2(A,B,C,1,-3 + C + T,0,X)  [C >= 2 && B >= A && Y >= Z]
          f9.4(A,B,C,E,F,H,N) -> f5.3(A,B,C,1,-3 + C + T,0,X)  [C >= 2 && B >= A && Y >= Z]
          f6.5(A,B,C,E,F,H,N) -> f9.0(17,1,0,E,F,H,N)          True
        Signature:
          {(f0.6,7);(f12.6,7);(f5.1,7);(f5.2,7);(f5.3,7);(f6.5,7);(f9.0,7);(f9.4,7)}
        Rule Graph:
          [0->{0,1},1->{7,8,9},2->{},3->{2},4->{3,4,5},5->{6},6->{},7->{2},8->{3,4,5},9->{6},10->{0,1}]
    + Applied Processor:
        AddSinks
    + Details:
        ()
* Step 6: Decompose MAYBE
    + Considered Problem:
        Rules:
          f9.0(A,B,C,E,F,H,N)  -> f9.0(A,1 + B,1 + C,E,F,H,N)   [A >= 1 + B && C >= 0]
          f9.0(A,B,C,E,F,H,N)  -> f9.4(A,1 + B,1 + C,E,F,H,N)   [A >= 1 + B && C >= 0]
          f5.1(A,B,C,E,F,H,N)  -> f0.6(A,B,C,E,F,G,N)           [U >= 1 + T && E >= 1 && F >= 0]
          f5.2(A,B,C,E,F,H,N)  -> f5.1(A,B,C,1 + E,-1 + F,0,V)  [T >= U && E >= 0 && F >= 0 && H = 0]
          f5.2(A,B,C,E,F,H,N)  -> f5.2(A,B,C,1 + E,-1 + F,0,V)  [T >= U && E >= 0 && F >= 0 && H = 0]
          f5.2(A,B,C,E,F,H,N)  -> f5.3(A,B,C,1 + E,-1 + F,0,V)  [T >= U && E >= 0 && F >= 0 && H = 0]
          f5.3(A,B,C,E,F,H,N)  -> f12.6(A,B,C,E,F,0,0)          [X >= T && E >= 0 && F >= 0 && N = 0 && H = 0]
          f9.4(A,B,C,E,F,H,N)  -> f5.1(A,B,C,1,-3 + C + T,0,X)  [C >= 2 && B >= A && Y >= Z]
          f9.4(A,B,C,E,F,H,N)  -> f5.2(A,B,C,1,-3 + C + T,0,X)  [C >= 2 && B >= A && Y >= Z]
          f9.4(A,B,C,E,F,H,N)  -> f5.3(A,B,C,1,-3 + C + T,0,X)  [C >= 2 && B >= A && Y >= Z]
          f6.5(A,B,C,E,F,H,N)  -> f9.0(17,1,0,E,F,H,N)          True
          f12.6(A,B,C,E,F,H,N) -> exitus616(A,B,C,E,F,H,N)      True
          f12.6(A,B,C,E,F,H,N) -> exitus616(A,B,C,E,F,H,N)      True
          f0.6(A,B,C,E,F,H,N)  -> exitus616(A,B,C,E,F,H,N)      True
          f0.6(A,B,C,E,F,H,N)  -> exitus616(A,B,C,E,F,H,N)      True
        Signature:
          {(exitus616,7);(f0.6,7);(f12.6,7);(f5.1,7);(f5.2,7);(f5.3,7);(f6.5,7);(f9.0,7);(f9.4,7)}
        Rule Graph:
          [0->{0,1},1->{7,8,9},2->{13,14},3->{2},4->{3,4,5},5->{6},6->{11,12},7->{2},8->{3,4,5},9->{6},10->{0,1}]
    + Applied Processor:
        Decompose Greedy
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14]
          |
          +- p:[0] c: [0]
          |
          `- p:[4] c: [4]
* Step 7: AbstractSize MAYBE
    + Considered Problem:
        (Rules:
          f9.0(A,B,C,E,F,H,N)  -> f9.0(A,1 + B,1 + C,E,F,H,N)   [A >= 1 + B && C >= 0]
          f9.0(A,B,C,E,F,H,N)  -> f9.4(A,1 + B,1 + C,E,F,H,N)   [A >= 1 + B && C >= 0]
          f5.1(A,B,C,E,F,H,N)  -> f0.6(A,B,C,E,F,G,N)           [U >= 1 + T && E >= 1 && F >= 0]
          f5.2(A,B,C,E,F,H,N)  -> f5.1(A,B,C,1 + E,-1 + F,0,V)  [T >= U && E >= 0 && F >= 0 && H = 0]
          f5.2(A,B,C,E,F,H,N)  -> f5.2(A,B,C,1 + E,-1 + F,0,V)  [T >= U && E >= 0 && F >= 0 && H = 0]
          f5.2(A,B,C,E,F,H,N)  -> f5.3(A,B,C,1 + E,-1 + F,0,V)  [T >= U && E >= 0 && F >= 0 && H = 0]
          f5.3(A,B,C,E,F,H,N)  -> f12.6(A,B,C,E,F,0,0)          [X >= T && E >= 0 && F >= 0 && N = 0 && H = 0]
          f9.4(A,B,C,E,F,H,N)  -> f5.1(A,B,C,1,-3 + C + T,0,X)  [C >= 2 && B >= A && Y >= Z]
          f9.4(A,B,C,E,F,H,N)  -> f5.2(A,B,C,1,-3 + C + T,0,X)  [C >= 2 && B >= A && Y >= Z]
          f9.4(A,B,C,E,F,H,N)  -> f5.3(A,B,C,1,-3 + C + T,0,X)  [C >= 2 && B >= A && Y >= Z]
          f6.5(A,B,C,E,F,H,N)  -> f9.0(17,1,0,E,F,H,N)          True
          f12.6(A,B,C,E,F,H,N) -> exitus616(A,B,C,E,F,H,N)      True
          f12.6(A,B,C,E,F,H,N) -> exitus616(A,B,C,E,F,H,N)      True
          f0.6(A,B,C,E,F,H,N)  -> exitus616(A,B,C,E,F,H,N)      True
          f0.6(A,B,C,E,F,H,N)  -> exitus616(A,B,C,E,F,H,N)      True
        Signature:
          {(exitus616,7);(f0.6,7);(f12.6,7);(f5.1,7);(f5.2,7);(f5.3,7);(f6.5,7);(f9.0,7);(f9.4,7)}
        Rule Graph:
          [0->{0,1},1->{7,8,9},2->{13,14},3->{2},4->{3,4,5},5->{6},6->{11,12},7->{2},8->{3,4,5},9->{6},10->{0,1}]
        ,We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14]
          |
          +- p:[0] c: [0]
          |
          `- p:[4] c: [4])
    + Applied Processor:
        AbstractSize Minimize
    + Details:
        ()
* Step 8: AbstractFlow MAYBE
    + Considered Problem:
        Program:
          Domain: [A,B,C,E,F,H,N,0.0,0.1]
           f9.0   ~>  f9.0        [A <= A, B <= A + B, C <= K + C, E <= E, F <= F, H <= H, N <= N]
           f9.0   ~>  f9.4        [A <= A, B <= A + B, C <= K + C, E <= E, F <= F, H <= H, N <= N]
           f5.1   ~>  f0.6        [A <= A, B <= B, C <= C, E <= E, F <= F, H <= unknown, N <= N]
           f5.2   ~>  f5.1        [A <= A, B <= B, C <= C, E <= K + E, F <= K + F, H <= 0*K, N <= unknown]
           f5.2   ~>  f5.2        [A <= A, B <= B, C <= C, E <= K + E, F <= K + F, H <= 0*K, N <= unknown]
           f5.2   ~>  f5.3        [A <= A, B <= B, C <= C, E <= K + E, F <= K + F, H <= 0*K, N <= unknown]
           f5.3   ~>  f12.6       [A <= A, B <= B, C <= C, E <= E, F <= F, H <= 0*K, N <= 0*K]
           f9.4   ~>  f5.1        [A <= A, B <= B, C <= C, E <= K, F <= unknown, H <= 0*K, N <= unknown]
           f9.4   ~>  f5.2        [A <= A, B <= B, C <= C, E <= K, F <= unknown, H <= 0*K, N <= unknown]
           f9.4   ~>  f5.3        [A <= A, B <= B, C <= C, E <= K, F <= unknown, H <= 0*K, N <= unknown]
           f6.5   ~>  f9.0        [A <= 17*K, B <= K, C <= 0*K, E <= E, F <= F, H <= H, N <= N]
           f12.6  ~>  exitus616   [A <= A, B <= B, C <= C, E <= E, F <= F, H <= H, N <= N]
           f12.6  ~>  exitus616   [A <= A, B <= B, C <= C, E <= E, F <= F, H <= H, N <= N]
           f0.6   ~>  exitus616   [A <= A, B <= B, C <= C, E <= E, F <= F, H <= H, N <= N]
           f0.6   ~>  exitus616   [A <= A, B <= B, C <= C, E <= E, F <= F, H <= H, N <= N]
          + Loop: [0.0 <= K + A + B]
               f9.0  ~>  f9.0   [A <= A, B <= A + B, C <= K + C, E <= E, F <= F, H <= H, N <= N]
          + Loop: [0.1 <= F]
               f5.2  ~>  f5.2   [A <= A, B <= B, C <= C, E <= K + E, F <= K + F, H <= 0*K, N <= unknown]
    + Applied Processor:
        AbstractFlow
    + Details:
        ()
* Step 9: Failure MAYBE
  + Considered Problem:
      Program:
        Domain: [tick,huge,K,A,B,C,E,F,H,N,0.0,0.1]
         f9.0   ~>  f9.0        [A ~+> B,B ~+> B,C ~+> C,K ~+> C]
         f9.0   ~>  f9.4        [A ~+> B,B ~+> B,C ~+> C,K ~+> C]
         f5.1   ~>  f0.6        [huge ~=> H]
         f5.2   ~>  f5.1        [K ~=> H,huge ~=> N,E ~+> E,F ~+> F,K ~+> E,K ~+> F]
         f5.2   ~>  f5.2        [K ~=> H,huge ~=> N,E ~+> E,F ~+> F,K ~+> E,K ~+> F]
         f5.2   ~>  f5.3        [K ~=> H,huge ~=> N,E ~+> E,F ~+> F,K ~+> E,K ~+> F]
         f5.3   ~>  f12.6       [K ~=> H,K ~=> N]
         f9.4   ~>  f5.1        [K ~=> E,K ~=> H,huge ~=> F,huge ~=> N]
         f9.4   ~>  f5.2        [K ~=> E,K ~=> H,huge ~=> F,huge ~=> N]
         f9.4   ~>  f5.3        [K ~=> E,K ~=> H,huge ~=> F,huge ~=> N]
         f6.5   ~>  f9.0        [K ~=> A,K ~=> B,K ~=> C]
         f12.6  ~>  exitus616   []
         f12.6  ~>  exitus616   []
         f0.6   ~>  exitus616   []
         f0.6   ~>  exitus616   []
        + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0]
             f9.0  ~>  f9.0   [A ~+> B,B ~+> B,C ~+> C,K ~+> C]
        + Loop: [F ~=> 0.1]
             f5.2  ~>  f5.2   [K ~=> H,huge ~=> N,E ~+> E,F ~+> F,K ~+> E,K ~+> F]
  + Applied Processor:
      Lare
  + Details:
      Unknown bound.
MAYBE