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