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: TrivialSCCs 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:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 3: AddSinks 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,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:
        AddSinks
    + Details:
        ()
* Step 4: LooptreeTransformer 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)
          5. f3(A,B,H) -> exitus616(A,B,H) True                                                                                    (1,1)
          6. f1(A,B,H) -> exitus616(A,B,H) True                                                                                    (?,1)
        Signature:
          {(exitus616,3);(f1,16);(f3,16);(f4,16)}
        Flow Graph:
          [0->{0,1,6},1->{},2->{},3->{0,1,6},4->{},5->{},6->{}]
        
    + Applied Processor:
        LooptreeTransformer
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6]
          |
          `- p:[0] c: [0]
* Step 5: SizeAbstraction 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)
          5. f3(A,B,H) -> exitus616(A,B,H) True                                                                                    (1,1)
          6. f1(A,B,H) -> exitus616(A,B,H) True                                                                                    (?,1)
        Signature:
          {(exitus616,3);(f1,16);(f3,16);(f4,16)}
        Flow Graph:
          [0->{0,1,6},1->{},2->{},3->{0,1,6},4->{},5->{},6->{}]
        
        ,We construct a looptree:
          P: [0,1,2,3,4,5,6]
          |
          `- p:[0] c: [0])
    + Applied Processor:
        SizeAbstraction UseCFG Minimize
    + Details:
        ()
* Step 6: FlowAbstraction 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]
           f3  ~>  exitus616   [A <= A, B <= B, H <= H]
           f1  ~>  exitus616   [A <= A, B <= B, H <= H]
          + Loop: [0.0 <= A + B]
               f1  ~>  f1   [A <= A, B <= A, H <= H]
    + Applied Processor:
        FlowAbstraction
    + 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]
         f3  ~>  exitus616   []
         f1  ~>  exitus616   []
        + Loop: [A ~+> 0.0,B ~+> 0.0]
             f1  ~>  f1   [A ~=> B]
  + Applied Processor:
      LareProcessor
  + Details:
      Unknown bound.
MAYBE