MAYBE
* Step 1: TrivialSCCs MAYBE
    + Considered Problem:
        Rules:
          0. f0(A,B,C,D,E,F,G)  -> f12(H,I,J,0,E,F,G)     True                                                                                              (1,1)
          1. f12(A,B,C,D,E,F,G) -> f12(A,B,C,1 + D,E,F,G) [D >= 0 && C >= 1 + D]                                                                            (?,1)
          2. f25(A,B,C,D,E,F,G) -> f25(A,B,C,D,E,1 + F,G) [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && E >= 1 + F] (?,1)
          3. f25(A,B,C,D,E,F,G) -> f34(A,B,C,D,E,F,G)     [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && F >= E]     (?,1)
          4. f12(A,B,C,D,E,F,G) -> f25(A,B,C,D,A,0,H)     [D >= 0 && D >= C]                                                                                (?,1)
        Signature:
          {(f0,7);(f12,7);(f25,7);(f34,7)}
        Flow Graph:
          [0->{1,4},1->{1,4},2->{2,3},3->{},4->{2,3}]
        
    + Applied Processor:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 2: AddSinks MAYBE
    + Considered Problem:
        Rules:
          0. f0(A,B,C,D,E,F,G)  -> f12(H,I,J,0,E,F,G)     True                                                                                              (1,1)
          1. f12(A,B,C,D,E,F,G) -> f12(A,B,C,1 + D,E,F,G) [D >= 0 && C >= 1 + D]                                                                            (?,1)
          2. f25(A,B,C,D,E,F,G) -> f25(A,B,C,D,E,1 + F,G) [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && E >= 1 + F] (?,1)
          3. f25(A,B,C,D,E,F,G) -> f34(A,B,C,D,E,F,G)     [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && F >= E]     (1,1)
          4. f12(A,B,C,D,E,F,G) -> f25(A,B,C,D,A,0,H)     [D >= 0 && D >= C]                                                                                (1,1)
        Signature:
          {(f0,7);(f12,7);(f25,7);(f34,7)}
        Flow Graph:
          [0->{1,4},1->{1,4},2->{2,3},3->{},4->{2,3}]
        
    + Applied Processor:
        AddSinks
    + Details:
        ()
* Step 3: LooptreeTransformer MAYBE
    + Considered Problem:
        Rules:
          0. f0(A,B,C,D,E,F,G)  -> f12(H,I,J,0,E,F,G)       True                                                                                              (1,1)
          1. f12(A,B,C,D,E,F,G) -> f12(A,B,C,1 + D,E,F,G)   [D >= 0 && C >= 1 + D]                                                                            (?,1)
          2. f25(A,B,C,D,E,F,G) -> f25(A,B,C,D,E,1 + F,G)   [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && E >= 1 + F] (?,1)
          3. f25(A,B,C,D,E,F,G) -> f34(A,B,C,D,E,F,G)       [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && F >= E]     (?,1)
          4. f12(A,B,C,D,E,F,G) -> f25(A,B,C,D,A,0,H)       [D >= 0 && D >= C]                                                                                (?,1)
          5. f25(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True                                                                                              (?,1)
        Signature:
          {(exitus616,7);(f0,7);(f12,7);(f25,7);(f34,7)}
        Flow Graph:
          [0->{1,4},1->{1,4},2->{2,3,5},3->{},4->{2,3,5},5->{}]
        
    + Applied Processor:
        LooptreeTransformer
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5]
          |
          +- p:[1] c: [1]
          |
          `- p:[2] c: [2]
* Step 4: SizeAbstraction MAYBE
    + Considered Problem:
        (Rules:
          0. f0(A,B,C,D,E,F,G)  -> f12(H,I,J,0,E,F,G)       True                                                                                              (1,1)
          1. f12(A,B,C,D,E,F,G) -> f12(A,B,C,1 + D,E,F,G)   [D >= 0 && C >= 1 + D]                                                                            (?,1)
          2. f25(A,B,C,D,E,F,G) -> f25(A,B,C,D,E,1 + F,G)   [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && E >= 1 + F] (?,1)
          3. f25(A,B,C,D,E,F,G) -> f34(A,B,C,D,E,F,G)       [F >= 0 && D + F >= 0 && A + -1*E >= 0 && -1*A + E >= 0 && D >= 0 && -1*C + D >= 0 && F >= E]     (?,1)
          4. f12(A,B,C,D,E,F,G) -> f25(A,B,C,D,A,0,H)       [D >= 0 && D >= C]                                                                                (?,1)
          5. f25(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True                                                                                              (?,1)
        Signature:
          {(exitus616,7);(f0,7);(f12,7);(f25,7);(f34,7)}
        Flow Graph:
          [0->{1,4},1->{1,4},2->{2,3,5},3->{},4->{2,3,5},5->{}]
        
        ,We construct a looptree:
          P: [0,1,2,3,4,5]
          |
          +- p:[1] c: [1]
          |
          `- p:[2] c: [2])
    + Applied Processor:
        SizeAbstraction UseCFG Minimize
    + Details:
        ()
* Step 5: FlowAbstraction MAYBE
    + Considered Problem:
        Program:
          Domain: [A,B,C,D,E,F,G,0.0,0.1]
           f0   ~>  f12         [A <= unknown, B <= unknown, C <= unknown, D <= 0*K, E <= E, F <= F, G <= G]
           f12  ~>  f12         [A <= A, B <= B, C <= C, D <= C, E <= E, F <= F, G <= G]
           f25  ~>  f25         [A <= A, B <= B, C <= C, D <= D, E <= E, F <= E, G <= G]
           f25  ~>  f34         [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G]
           f12  ~>  f25         [A <= A, B <= B, C <= C, D <= D, E <= A, F <= 0*K, G <= unknown]
           f25  ~>  exitus616   [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G]
          + Loop: [0.0 <= C + D]
               f12  ~>  f12   [A <= A, B <= B, C <= C, D <= C, E <= E, F <= F, G <= G]
          + Loop: [0.1 <= E + F]
               f25  ~>  f25   [A <= A, B <= B, C <= C, D <= D, E <= E, F <= E, G <= G]
    + Applied Processor:
        FlowAbstraction
    + Details:
        ()
* Step 6: Failure MAYBE
  + Considered Problem:
      Program:
        Domain: [tick,huge,K,A,B,C,D,E,F,G,0.0,0.1]
         f0   ~>  f12         [K ~=> D,huge ~=> A,huge ~=> B,huge ~=> C]
         f12  ~>  f12         [C ~=> D]
         f25  ~>  f25         [E ~=> F]
         f25  ~>  f34         []
         f12  ~>  f25         [A ~=> E,K ~=> F,huge ~=> G]
         f25  ~>  exitus616   []
        + Loop: [C ~+> 0.0,D ~+> 0.0]
             f12  ~>  f12   [C ~=> D]
        + Loop: [E ~+> 0.1,F ~+> 0.1]
             f25  ~>  f25   [E ~=> F]
  + Applied Processor:
      LareProcessor
  + Details:
      Unknown bound.
MAYBE