MAYBE
* Step 1: UnsatPaths MAYBE
    + Considered Problem:
        Rules:
          0. f0(A) -> f4(B)     True               (1,1)
          1. f4(A) -> f4(1 + A) [3 >= A && A >= 1] (?,1)
          2. f4(A) -> f4(1)     [0 >= A && 3 >= A] (?,1)
          3. f4(A) -> f12(A)    [A >= 4]           (?,1)
        Signature:
          {(f0,1);(f12,1);(f4,1)}
        Flow Graph:
          [0->{1,2,3},1->{1,2,3},2->{1,2,3},3->{}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(1,2),(2,2),(2,3)]
* Step 2: FromIts MAYBE
    + Considered Problem:
        Rules:
          0. f0(A) -> f4(B)     True               (1,1)
          1. f4(A) -> f4(1 + A) [3 >= A && A >= 1] (?,1)
          2. f4(A) -> f4(1)     [0 >= A && 3 >= A] (?,1)
          3. f4(A) -> f12(A)    [A >= 4]           (?,1)
        Signature:
          {(f0,1);(f12,1);(f4,1)}
        Flow Graph:
          [0->{1,2,3},1->{1,3},2->{1},3->{}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 3: Unfold MAYBE
    + Considered Problem:
        Rules:
          f0(A) -> f4(B)      True
          f4(A) -> f4(1 + A)  [3 >= A && A >= 1]
          f4(A) -> f4(1)      [0 >= A && 3 >= A]
          f4(A) -> f12(A)     [A >= 4]
        Signature:
          {(f0,1);(f12,1);(f4,1)}
        Rule Graph:
          [0->{1,2,3},1->{1,3},2->{1},3->{}]
    + Applied Processor:
        Unfold
    + Details:
        ()
* Step 4: AddSinks MAYBE
    + Considered Problem:
        Rules:
          f0.0(A) -> f4.1(B)      True
          f0.0(A) -> f4.2(B)      True
          f0.0(A) -> f4.3(B)      True
          f4.1(A) -> f4.1(1 + A)  [3 >= A && A >= 1]
          f4.1(A) -> f4.3(1 + A)  [3 >= A && A >= 1]
          f4.2(A) -> f4.1(1)      [0 >= A && 3 >= A]
          f4.3(A) -> f12.4(A)     [A >= 4]
        Signature:
          {(f0.0,1);(f12.4,1);(f4.1,1);(f4.2,1);(f4.3,1)}
        Rule Graph:
          [0->{3,4},1->{5},2->{6},3->{3,4},4->{6},5->{3,4},6->{}]
    + Applied Processor:
        AddSinks
    + Details:
        ()
* Step 5: Decompose MAYBE
    + Considered Problem:
        Rules:
          f0.0(A)  -> f4.1(B)       True
          f0.0(A)  -> f4.2(B)       True
          f0.0(A)  -> f4.3(B)       True
          f4.1(A)  -> f4.1(1 + A)   [3 >= A && A >= 1]
          f4.1(A)  -> f4.3(1 + A)   [3 >= A && A >= 1]
          f4.2(A)  -> f4.1(1)       [0 >= A && 3 >= A]
          f4.3(A)  -> f12.4(A)      [A >= 4]
          f12.4(A) -> exitus616(A)  True
          f12.4(A) -> exitus616(A)  True
          f12.4(A) -> exitus616(A)  True
        Signature:
          {(exitus616,1);(f0.0,1);(f12.4,1);(f4.1,1);(f4.2,1);(f4.3,1)}
        Rule Graph:
          [0->{3,4},1->{5},2->{6},3->{3,4},4->{6},5->{3,4},6->{7,8,9}]
    + Applied Processor:
        Decompose Greedy
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9]
          |
          `- p:[3] c: [3]
* Step 6: AbstractSize MAYBE
    + Considered Problem:
        (Rules:
          f0.0(A)  -> f4.1(B)       True
          f0.0(A)  -> f4.2(B)       True
          f0.0(A)  -> f4.3(B)       True
          f4.1(A)  -> f4.1(1 + A)   [3 >= A && A >= 1]
          f4.1(A)  -> f4.3(1 + A)   [3 >= A && A >= 1]
          f4.2(A)  -> f4.1(1)       [0 >= A && 3 >= A]
          f4.3(A)  -> f12.4(A)      [A >= 4]
          f12.4(A) -> exitus616(A)  True
          f12.4(A) -> exitus616(A)  True
          f12.4(A) -> exitus616(A)  True
        Signature:
          {(exitus616,1);(f0.0,1);(f12.4,1);(f4.1,1);(f4.2,1);(f4.3,1)}
        Rule Graph:
          [0->{3,4},1->{5},2->{6},3->{3,4},4->{6},5->{3,4},6->{7,8,9}]
        ,We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9]
          |
          `- p:[3] c: [3])
    + Applied Processor:
        AbstractSize Minimize
    + Details:
        ()
* Step 7: AbstractFlow MAYBE
    + Considered Problem:
        Program:
          Domain: [A,0.0]
           f0.0   ~>  f4.1        [A <= unknown]
           f0.0   ~>  f4.2        [A <= unknown]
           f0.0   ~>  f4.3        [A <= unknown]
           f4.1   ~>  f4.1        [A <= 4*K]
           f4.1   ~>  f4.3        [A <= 4*K]
           f4.2   ~>  f4.1        [A <= K]
           f4.3   ~>  f12.4       [A <= A]
           f12.4  ~>  exitus616   [A <= A]
           f12.4  ~>  exitus616   [A <= A]
           f12.4  ~>  exitus616   [A <= A]
          + Loop: [0.0 <= 3*K + A]
               f4.1  ~>  f4.1   [A <= 4*K]
    + Applied Processor:
        AbstractFlow
    + Details:
        ()
* Step 8: Failure MAYBE
  + Considered Problem:
      Program:
        Domain: [tick,huge,K,A,0.0]
         f0.0   ~>  f4.1        [huge ~=> A]
         f0.0   ~>  f4.2        [huge ~=> A]
         f0.0   ~>  f4.3        [huge ~=> A]
         f4.1   ~>  f4.1        [K ~=> A]
         f4.1   ~>  f4.3        [K ~=> A]
         f4.2   ~>  f4.1        [K ~=> A]
         f4.3   ~>  f12.4       []
         f12.4  ~>  exitus616   []
         f12.4  ~>  exitus616   []
         f12.4  ~>  exitus616   []
        + Loop: [A ~+> 0.0,K ~*> 0.0]
             f4.1  ~>  f4.1   [K ~=> A]
  + Applied Processor:
      Lare
  + Details:
      Unknown bound.
MAYBE