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