MAYBE
* Step 1: ArgumentFilter MAYBE
    + Considered Problem:
        Rules:
          0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f1(A,1 + B,D,O,D,P,B,H,I,J,K,L,M,N) [-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) -> f4(P,Q,R,U,T,F,G,O,S,V,W,C,M,N)     [-2 + H >= 0 && -4 + B + H >= 0 && -2 + B >= 0 && B >= A && B >= 0 && Q >= O && O >= 2] (?,1)
          2. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f4(R,S,Q,V,U,F,G,P,T,W,Y,0,O,N)     [0 >= P && 0 >= X]                                                                      (1,1)
          3. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f1(P,2,R,Q,R,F,G,P,R,J,K,L,O,S)     [P >= 2]                                                                                (1,1)
          4. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f4(P,Q,R,U,T,F,G,1,S,V,W,D,O,N)     True                                                                                    (1,1)
        Signature:
          {(f1,14);(f3,14);(f4,14)}
        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]
    + Details:
        We remove following argument positions: [2,3,4,5,6,8,9,10,11,12,13].
* 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(P,Q,O)     [-2 + H >= 0 && -4 + B + H >= 0 && -2 + B >= 0 && B >= A && B >= 0 && Q >= O && O >= 2] (?,1)
          2. f3(A,B,H) -> f4(R,S,P)     [0 >= P && 0 >= X]                                                                      (1,1)
          3. f3(A,B,H) -> f1(P,2,P)     [P >= 2]                                                                                (1,1)
          4. f3(A,B,H) -> f4(P,Q,1)     True                                                                                    (1,1)
        Signature:
          {(f1,14);(f3,14);(f4,14)}
        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(P,Q,O)      [-2 + H >= 0
                                       && -4 + B + H >= 0
                                       && -2 + B >= 0
                                       && B >= A
                                       && B >= 0
                                       && Q >= O
                                       && O >= 2]
          f3(A,B,H) -> f4(R,S,P)      [0 >= P && 0 >= X]
          f3(A,B,H) -> f1(P,2,P)      [P >= 2]
          f3(A,B,H) -> f4(P,Q,1)      True
        Signature:
          {(f1,14);(f3,14);(f4,14)}
        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(P,Q,O)         [-2 + H >= 0
                                          && -4 + B + H >= 0
                                          && -2 + B >= 0
                                          && B >= A
                                          && B >= 0
                                          && Q >= O
                                          && O >= 2]
          f3(A,B,H) -> f4(R,S,P)         [0 >= P && 0 >= X]
          f3(A,B,H) -> f1(P,2,P)         [P >= 2]
          f3(A,B,H) -> f4(P,Q,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,14);(f3,14);(f4,14)}
        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(P,Q,O)         [-2 + H >= 0
                                          && -4 + B + H >= 0
                                          && -2 + B >= 0
                                          && B >= A
                                          && B >= 0
                                          && Q >= O
                                          && O >= 2]
          f3(A,B,H) -> f4(R,S,P)         [0 >= P && 0 >= X]
          f3(A,B,H) -> f1(P,2,P)         [P >= 2]
          f3(A,B,H) -> f4(P,Q,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,14);(f3,14);(f4,14)}
        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