Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f79 -> f81 : [ 0>=A ], cost: 1
     20: f79 -> f81 : [ A>=1 ], cost: 1
      3: f81 -> f65 : [ 0>=F ], cost: 1
     19: f81 -> f65 : [ F>=1 ], cost: 1
      1: f34 -> f34 : B'=-1+B, C'=free, [ B>=1 && 0>=free ], cost: 1
      2: f34 -> f44 : B'=-1+B, C'=free_2, D'=free_3, E'=free_1, [ 0>=free_3 && B>=1 && free_2>=1 ], cost: 1
     26: f34 -> f44 : B'=-1+B, C'=free_32, D'=free_33, E'=free_31, [ free_33>=1 && B>=1 && free_32>=1 ], cost: 1
     27: f34 -> f65 : G'=free_35, R'=0, V'=0, Z1'=free_34, A2'=free_35, [ 0>=B ], cost: 1
     24: f44 -> f34 : Y1'=C, [ 0>=E ], cost: 1
     25: f44 -> f34 : Y1'=C, [ E>=1 ], cost: 1
      4: f65 -> f75 : F'=free_5, G'=-1+G, H'=free_6, Q'=free_4, [ G>=1 && 0>=free_6 ], cost: 1
     22: f65 -> f75 : F'=free_27, G'=-1+G, H'=free_28, Q'=free_26, [ G>=1 && free_28>=1 ], cost: 1
     23: f65 -> f100 : R'=0, V'=0, P1'=free_30, W1'=free_29, X1'=free_30, [ 0>=G ], cost: 1
      5: f75 -> f79 : A'=free_7, [ 0>=Q ], cost: 1
     21: f75 -> f79 : A'=free_25, [ Q>=1 ], cost: 1
      6: f213 -> f213 : [], cost: 1
      7: f215 -> f218 : [], cost: 1
      9: f191 -> f213 : Q_1'=2, R'=0, S'=free_9, [ 0>=J && Q_1==2 ], cost: 1
     10: f191 -> f213 : R'=0, S'=free_10, T'=1, [ 1>=Q_1 && 0>=J ], cost: 1
     11: f191 -> f213 : R'=0, S'=free_11, T'=1, [ Q_1>=3 && 0>=J ], cost: 1
      8: f191 -> f191 : J'=-1+J, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, [ J>=1 ], cost: 1
     12: f132 -> f191 : J'=free_13, R'=0, V'=0, W'=free_12, X'=free_13, [ 0>=U ], cost: 1
     15: f132 -> f132 : R'=0, U'=-1+U, V'=0, J1'=free_14, K1'=free_15, [ U>=1 && 0>=free_14 ], cost: 1
     16: f132 -> f132 : R'=0, U'=-1+U, V'=0, Z'=free_16, D1'=0, J1'=free_18, K1'=free_19, L1'=free_17, M1'=free_17, N1'=0, O1'=0, [ U>=1 && free_18>=1 ], cost: 1
     13: f156 -> f132 : Q_1'=0, V'=0, Z'=Y, A1'=Y, B1'=0, C1'=D1, E1'=Y, F1'=0, G1'=Y, H1'=D1, [ Y>=1 ], cost: 1
     14: f156 -> f132 : V'=0, Z'=Y, Q1'=D1, [ 0>=Y ], cost: 1
     17: f100 -> f132 : R'=0, U'=free_21, V'=0, Q1_1'=free_20, R1'=free_21, [ 0>=P1 ], cost: 1
     18: f100 -> f100 : R'=0, V'=0, P1'=-1+P1, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, [ P1>=1 ], cost: 1
     28: f0 -> f34 : B'=free_36, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 ], cost: 1
     29: f0 -> f34 : B'=free_42, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f79 -> f81 : [ 0>=A ], cost: 1
     20: f79 -> f81 : [ A>=1 ], cost: 1
      3: f81 -> f65 : [ 0>=F ], cost: 1
     19: f81 -> f65 : [ F>=1 ], cost: 1
      1: f34 -> f34 : B'=-1+B, C'=free, [ B>=1 && 0>=free ], cost: 1
      2: f34 -> f44 : B'=-1+B, C'=free_2, D'=free_3, E'=free_1, [ 0>=free_3 && B>=1 && free_2>=1 ], cost: 1
     26: f34 -> f44 : B'=-1+B, C'=free_32, D'=free_33, E'=free_31, [ free_33>=1 && B>=1 && free_32>=1 ], cost: 1
     27: f34 -> f65 : G'=free_35, R'=0, V'=0, Z1'=free_34, A2'=free_35, [ 0>=B ], cost: 1
     24: f44 -> f34 : Y1'=C, [ 0>=E ], cost: 1
     25: f44 -> f34 : Y1'=C, [ E>=1 ], cost: 1
      4: f65 -> f75 : F'=free_5, G'=-1+G, H'=free_6, Q'=free_4, [ G>=1 && 0>=free_6 ], cost: 1
     22: f65 -> f75 : F'=free_27, G'=-1+G, H'=free_28, Q'=free_26, [ G>=1 && free_28>=1 ], cost: 1
     23: f65 -> f100 : R'=0, V'=0, P1'=free_30, W1'=free_29, X1'=free_30, [ 0>=G ], cost: 1
      5: f75 -> f79 : A'=free_7, [ 0>=Q ], cost: 1
     21: f75 -> f79 : A'=free_25, [ Q>=1 ], cost: 1
      6: f213 -> f213 : [], cost: 1
      9: f191 -> f213 : Q_1'=2, R'=0, S'=free_9, [ 0>=J && Q_1==2 ], cost: 1
     10: f191 -> f213 : R'=0, S'=free_10, T'=1, [ 1>=Q_1 && 0>=J ], cost: 1
     11: f191 -> f213 : R'=0, S'=free_11, T'=1, [ Q_1>=3 && 0>=J ], cost: 1
      8: f191 -> f191 : J'=-1+J, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, [ J>=1 ], cost: 1
     12: f132 -> f191 : J'=free_13, R'=0, V'=0, W'=free_12, X'=free_13, [ 0>=U ], cost: 1
     15: f132 -> f132 : R'=0, U'=-1+U, V'=0, J1'=free_14, K1'=free_15, [ U>=1 && 0>=free_14 ], cost: 1
     16: f132 -> f132 : R'=0, U'=-1+U, V'=0, Z'=free_16, D1'=0, J1'=free_18, K1'=free_19, L1'=free_17, M1'=free_17, N1'=0, O1'=0, [ U>=1 && free_18>=1 ], cost: 1
     17: f100 -> f132 : R'=0, U'=free_21, V'=0, Q1_1'=free_20, R1'=free_21, [ 0>=P1 ], cost: 1
     18: f100 -> f100 : R'=0, V'=0, P1'=-1+P1, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, [ P1>=1 ], cost: 1
     28: f0 -> f34 : B'=free_36, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 ], cost: 1
     29: f0 -> f34 : B'=free_42, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 ], cost: 1

Eliminating 1 self-loops for location f34
  Self-Loop 1 has the metering function: B, resulting in the new transition 30.
  Removing the self-loops: 1.
Eliminating 1 self-loops for location f213
  Self-Loop 6 has unbounded runtime, resulting in the new transition 31.
  Removing the self-loops: 6.
Eliminating 1 self-loops for location f191
  Self-Loop 8 has the metering function: J, resulting in the new transition 32.
  Removing the self-loops: 8.
Eliminating 2 self-loops for location f132
  Self-Loop 15 has the metering function: U, resulting in the new transition 33.
  Self-Loop 16 has the metering function: U, resulting in the new transition 34.
  Removing the self-loops: 15 16.
Eliminating 1 self-loops for location f100
  Self-Loop 18 has the metering function: P1, resulting in the new transition 35.
  Removing the self-loops: 18.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f79 -> f81 : [ 0>=A ], cost: 1
     20: f79 -> f81 : [ A>=1 ], cost: 1
      3: f81 -> f65 : [ 0>=F ], cost: 1
     19: f81 -> f65 : [ F>=1 ], cost: 1
     30: f34 -> [14] : B'=0, C'=free, [ B>=1 && 0>=free ], cost: B
     24: f44 -> f34 : Y1'=C, [ 0>=E ], cost: 1
     25: f44 -> f34 : Y1'=C, [ E>=1 ], cost: 1
      4: f65 -> f75 : F'=free_5, G'=-1+G, H'=free_6, Q'=free_4, [ G>=1 && 0>=free_6 ], cost: 1
     22: f65 -> f75 : F'=free_27, G'=-1+G, H'=free_28, Q'=free_26, [ G>=1 && free_28>=1 ], cost: 1
     23: f65 -> f100 : R'=0, V'=0, P1'=free_30, W1'=free_29, X1'=free_30, [ 0>=G ], cost: 1
      5: f75 -> f79 : A'=free_7, [ 0>=Q ], cost: 1
     21: f75 -> f79 : A'=free_25, [ Q>=1 ], cost: 1
     31: f213 -> [15] : [], cost: INF
     32: f191 -> [16] : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, [ J>=1 ], cost: J
     33: f132 -> [17] : R'=0, U'=0, V'=0, J1'=free_14, K1'=free_15, [ U>=1 && 0>=free_14 ], cost: U
     34: f132 -> [17] : R'=0, U'=0, V'=0, Z'=free_16, D1'=0, J1'=free_18, K1'=free_19, L1'=free_17, M1'=free_17, N1'=0, O1'=0, [ U>=1 && free_18>=1 ], cost: U
     35: f100 -> [18] : R'=0, V'=0, P1'=0, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, [ P1>=1 ], cost: P1
     28: f0 -> f34 : B'=free_36, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 ], cost: 1
     29: f0 -> f34 : B'=free_42, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 ], cost: 1
      2: [14] -> f44 : B'=-1+B, C'=free_2, D'=free_3, E'=free_1, [ 0>=free_3 && B>=1 && free_2>=1 ], cost: 1
     26: [14] -> f44 : B'=-1+B, C'=free_32, D'=free_33, E'=free_31, [ free_33>=1 && B>=1 && free_32>=1 ], cost: 1
     27: [14] -> f65 : G'=free_35, R'=0, V'=0, Z1'=free_34, A2'=free_35, [ 0>=B ], cost: 1
      9: [16] -> f213 : Q_1'=2, R'=0, S'=free_9, [ 0>=J && Q_1==2 ], cost: 1
     10: [16] -> f213 : R'=0, S'=free_10, T'=1, [ 1>=Q_1 && 0>=J ], cost: 1
     11: [16] -> f213 : R'=0, S'=free_11, T'=1, [ Q_1>=3 && 0>=J ], cost: 1
     12: [17] -> f191 : J'=free_13, R'=0, V'=0, W'=free_12, X'=free_13, [ 0>=U ], cost: 1
     17: [18] -> f132 : R'=0, U'=free_21, V'=0, Q1_1'=free_20, R1'=free_21, [ 0>=P1 ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f79 -> f81 : [ 0>=A ], cost: 1
     20: f79 -> f81 : [ A>=1 ], cost: 1
      3: f81 -> f65 : [ 0>=F ], cost: 1
     19: f81 -> f65 : [ F>=1 ], cost: 1
     30: f34 -> [14] : B'=0, C'=free, [ B>=1 && 0>=free ], cost: B
     24: f44 -> f34 : Y1'=C, [ 0>=E ], cost: 1
     25: f44 -> f34 : Y1'=C, [ E>=1 ], cost: 1
      4: f65 -> f75 : F'=free_5, G'=-1+G, H'=free_6, Q'=free_4, [ G>=1 && 0>=free_6 ], cost: 1
     22: f65 -> f75 : F'=free_27, G'=-1+G, H'=free_28, Q'=free_26, [ G>=1 && free_28>=1 ], cost: 1
     23: f65 -> f132 : R'=0, U'=free_21, V'=0, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, [ 0>=G && free_30>=1 && 0>=0 ], cost: 2+free_30
      5: f75 -> f79 : A'=free_7, [ 0>=Q ], cost: 1
     21: f75 -> f79 : A'=free_25, [ Q>=1 ], cost: 1
     31: f213 -> [15] : [], cost: INF
     33: f132 -> [17] : R'=0, U'=0, V'=0, J1'=free_14, K1'=free_15, [ U>=1 && 0>=free_14 ], cost: U
     34: f132 -> [17] : R'=0, U'=0, V'=0, Z'=free_16, D1'=0, J1'=free_18, K1'=free_19, L1'=free_17, M1'=free_17, N1'=0, O1'=0, [ U>=1 && free_18>=1 ], cost: U
     28: f0 -> f34 : B'=free_36, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 ], cost: 1
     29: f0 -> f34 : B'=free_42, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 ], cost: 1
      2: [14] -> f44 : B'=-1+B, C'=free_2, D'=free_3, E'=free_1, [ 0>=free_3 && B>=1 && free_2>=1 ], cost: 1
     26: [14] -> f44 : B'=-1+B, C'=free_32, D'=free_33, E'=free_31, [ free_33>=1 && B>=1 && free_32>=1 ], cost: 1
     27: [14] -> f65 : G'=free_35, R'=0, V'=0, Z1'=free_34, A2'=free_35, [ 0>=B ], cost: 1
      9: [16] -> f213 : Q_1'=2, R'=0, S'=free_9, [ 0>=J && Q_1==2 ], cost: 1
     10: [16] -> f213 : R'=0, S'=free_10, T'=1, [ 1>=Q_1 && 0>=J ], cost: 1
     11: [16] -> f213 : R'=0, S'=free_11, T'=1, [ Q_1>=3 && 0>=J ], cost: 1
     12: [17] -> [16] : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, R'=0, V'=0, W'=free_12, X'=free_13, [ 0>=U && free_13>=1 ], cost: 1+free_13


Applied chaining over branches and pruning:
  Start location: f0
     45: f79 -> f65 : [ 0>=A && 0>=F ], cost: 2
     46: f79 -> f65 : [ 0>=A && F>=1 ], cost: 2
     47: f79 -> f65 : [ A>=1 && 0>=F ], cost: 2
     48: f79 -> f65 : [ A>=1 && F>=1 ], cost: 2
     38: f34 -> f65 : B'=0, C'=free, G'=free_35, R'=0, V'=0, Z1'=free_34, A2'=free_35, [ B>=1 && 0>=free && 0>=0 ], cost: 1+B
     36: f34 -> [19] : B'=0, C'=free, [ B>=1 && 0>=free ], cost: B
     37: f34 -> [20] : B'=0, C'=free, [ B>=1 && 0>=free ], cost: B
     39: f65 -> f79 : A'=free_7, F'=free_5, G'=-1+G, H'=free_6, Q'=free_4, [ G>=1 && 0>=free_6 && 0>=free_4 ], cost: 2
     40: f65 -> f79 : A'=free_25, F'=free_5, G'=-1+G, H'=free_6, Q'=free_4, [ G>=1 && 0>=free_6 && free_4>=1 ], cost: 2
     41: f65 -> f79 : A'=free_7, F'=free_27, G'=-1+G, H'=free_28, Q'=free_26, [ G>=1 && free_28>=1 && 0>=free_26 ], cost: 2
     42: f65 -> f79 : A'=free_25, F'=free_27, G'=-1+G, H'=free_28, Q'=free_26, [ G>=1 && free_28>=1 && free_26>=1 ], cost: 2
     43: f65 -> [17] : R'=0, U'=0, V'=0, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, [ 0>=G && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 ], cost: 2+free_30+free_21
     44: f65 -> [17] : R'=0, U'=0, V'=0, Z'=free_16, D1'=0, J1'=free_18, K1'=free_19, L1'=free_17, M1'=free_17, N1'=0, O1'=0, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, [ 0>=G && free_30>=1 && 0>=0 && free_21>=1 && free_18>=1 ], cost: 2+free_30+free_21
     31: f213 -> [15] : [], cost: INF
     28: f0 -> f34 : B'=free_36, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 ], cost: 1
     29: f0 -> f34 : B'=free_42, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 ], cost: 1
     49: [17] -> f213 : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, Q_1'=2, R'=0, S'=free_9, V'=0, W'=free_12, X'=free_13, [ 0>=U && free_13>=1 && 0>=0 && Q_1==2 ], cost: 2+free_13
     50: [17] -> f213 : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, R'=0, S'=free_10, T'=1, V'=0, W'=free_12, X'=free_13, [ 0>=U && free_13>=1 && 1>=Q_1 && 0>=0 ], cost: 2+free_13
     51: [17] -> f213 : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, R'=0, S'=free_11, T'=1, V'=0, W'=free_12, X'=free_13, [ 0>=U && free_13>=1 && Q_1>=3 && 0>=0 ], cost: 2+free_13


Applied chaining over branches and pruning:
  Start location: f0
     58: f65 -> f65 : A'=free_7, F'=free_5, G'=-1+G, H'=free_6, Q'=free_4, [ G>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 4
     59: f65 -> f65 : A'=free_7, F'=free_5, G'=-1+G, H'=free_6, Q'=free_4, [ G>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && free_5>=1 ], cost: 4
     61: f65 -> f65 : A'=free_7, F'=free_5, G'=-1+G, H'=free_6, Q'=free_4, [ G>=1 && 0>=free_6 && 0>=free_4 && free_7>=1 && free_5>=1 ], cost: 4
     65: f65 -> f65 : A'=free_25, F'=free_5, G'=-1+G, H'=free_6, Q'=free_4, [ G>=1 && 0>=free_6 && free_4>=1 && free_25>=1 && free_5>=1 ], cost: 4
     67: f65 -> f65 : A'=free_7, F'=free_27, G'=-1+G, H'=free_28, Q'=free_26, [ G>=1 && free_28>=1 && 0>=free_26 && 0>=free_7 && free_27>=1 ], cost: 4
     74: f65 -> f213 : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, Q_1'=2, R'=0, S'=free_9, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, [ 0>=G && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && 0>=0 && Q_1==2 ], cost: 4+free_13+free_30+free_21
     75: f65 -> f213 : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, R'=0, S'=free_10, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, [ 0>=G && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && 1>=Q_1 && 0>=0 ], cost: 4+free_13+free_30+free_21
     76: f65 -> f213 : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, R'=0, S'=free_11, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, [ 0>=G && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && Q_1>=3 && 0>=0 ], cost: 4+free_13+free_30+free_21
     77: f65 -> f213 : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, Q_1'=2, R'=0, S'=free_9, U'=0, V'=0, W'=free_12, X'=free_13, Z'=free_16, D1'=0, J1'=free_18, K1'=free_19, L1'=free_17, M1'=free_17, N1'=0, O1'=0, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, [ 0>=G && free_30>=1 && 0>=0 && free_21>=1 && free_18>=1 && 0>=0 && free_13>=1 && 0>=0 && Q_1==2 ], cost: 4+free_13+free_30+free_21
     79: f65 -> f213 : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, R'=0, S'=free_11, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, Z'=free_16, D1'=0, J1'=free_18, K1'=free_19, L1'=free_17, M1'=free_17, N1'=0, O1'=0, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, [ 0>=G && free_30>=1 && 0>=0 && free_21>=1 && free_18>=1 && 0>=0 && free_13>=1 && Q_1>=3 && 0>=0 ], cost: 4+free_13+free_30+free_21
     31: f213 -> [15] : [], cost: INF
     52: f0 -> f65 : B'=0, C'=free, G'=free_35, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 ], cost: 2+free_36
     55: f0 -> f65 : B'=0, C'=free, G'=free_35, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free && 0>=0 ], cost: 2+free_42
     53: f0 -> [19] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free ], cost: 1+free_36
     56: f0 -> [19] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free ], cost: 1+free_42
     54: f0 -> [20] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free ], cost: 1+free_36
     57: f0 -> [20] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free ], cost: 1+free_42

Eliminating 5 self-loops for location f65
  Self-Loop 58 has the metering function: G, resulting in the new transition 80.
  Self-Loop 59 has the metering function: G, resulting in the new transition 81.
  Self-Loop 61 has the metering function: G, resulting in the new transition 82.
  Self-Loop 65 has the metering function: G, resulting in the new transition 83.
  Self-Loop 67 has the metering function: G, resulting in the new transition 84.
  Removing the self-loops: 58 59 61 65 67.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
     80: f65 -> [21] : A'=free_7, F'=free_5, G'=0, H'=free_6, Q'=free_4, [ G>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 4*G
     81: f65 -> [21] : A'=free_7, F'=free_5, G'=0, H'=free_6, Q'=free_4, [ G>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && free_5>=1 ], cost: 4*G
     82: f65 -> [21] : A'=free_7, F'=free_5, G'=0, H'=free_6, Q'=free_4, [ G>=1 && 0>=free_6 && 0>=free_4 && free_7>=1 && free_5>=1 ], cost: 4*G
     83: f65 -> [21] : A'=free_25, F'=free_5, G'=0, H'=free_6, Q'=free_4, [ G>=1 && 0>=free_6 && free_4>=1 && free_25>=1 && free_5>=1 ], cost: 4*G
     84: f65 -> [21] : A'=free_7, F'=free_27, G'=0, H'=free_28, Q'=free_26, [ G>=1 && free_28>=1 && 0>=free_26 && 0>=free_7 && free_27>=1 ], cost: 4*G
     31: f213 -> [15] : [], cost: INF
     52: f0 -> f65 : B'=0, C'=free, G'=free_35, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 ], cost: 2+free_36
     55: f0 -> f65 : B'=0, C'=free, G'=free_35, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free && 0>=0 ], cost: 2+free_42
     53: f0 -> [19] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free ], cost: 1+free_36
     56: f0 -> [19] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free ], cost: 1+free_42
     54: f0 -> [20] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free ], cost: 1+free_36
     57: f0 -> [20] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free ], cost: 1+free_42
     74: [21] -> f213 : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, Q_1'=2, R'=0, S'=free_9, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, [ 0>=G && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && 0>=0 && Q_1==2 ], cost: 4+free_13+free_30+free_21
     75: [21] -> f213 : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, R'=0, S'=free_10, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, [ 0>=G && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && 1>=Q_1 && 0>=0 ], cost: 4+free_13+free_30+free_21
     76: [21] -> f213 : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, R'=0, S'=free_11, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, [ 0>=G && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && Q_1>=3 && 0>=0 ], cost: 4+free_13+free_30+free_21
     77: [21] -> f213 : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, Q_1'=2, R'=0, S'=free_9, U'=0, V'=0, W'=free_12, X'=free_13, Z'=free_16, D1'=0, J1'=free_18, K1'=free_19, L1'=free_17, M1'=free_17, N1'=0, O1'=0, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, [ 0>=G && free_30>=1 && 0>=0 && free_21>=1 && free_18>=1 && 0>=0 && free_13>=1 && 0>=0 && Q_1==2 ], cost: 4+free_13+free_30+free_21
     79: [21] -> f213 : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, R'=0, S'=free_11, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, Z'=free_16, D1'=0, J1'=free_18, K1'=free_19, L1'=free_17, M1'=free_17, N1'=0, O1'=0, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, [ 0>=G && free_30>=1 && 0>=0 && free_21>=1 && free_18>=1 && 0>=0 && free_13>=1 && Q_1>=3 && 0>=0 ], cost: 4+free_13+free_30+free_21


Applied chaining over branches and pruning:
  Start location: f0
     53: f0 -> [19] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free ], cost: 1+free_36
     56: f0 -> [19] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free ], cost: 1+free_42
     54: f0 -> [20] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free ], cost: 1+free_36
     57: f0 -> [20] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free ], cost: 1+free_42
     85: f0 -> [21] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 2+free_36+4*free_35
     86: f0 -> [21] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && free_5>=1 ], cost: 2+free_36+4*free_35
     88: f0 -> [21] : A'=free_25, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && free_4>=1 && free_25>=1 && free_5>=1 ], cost: 2+free_36+4*free_35
     89: f0 -> [21] : A'=free_7, B'=0, C'=free, F'=free_27, G'=0, H'=free_28, Q'=free_26, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && free_28>=1 && 0>=free_26 && 0>=free_7 && free_27>=1 ], cost: 2+free_36+4*free_35
     90: f0 -> [21] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 2+free_42+4*free_35
     95: [21] -> [15] : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, Q_1'=2, R'=0, S'=free_9, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, [ 0>=G && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && 0>=0 && Q_1==2 ], cost: INF
     96: [21] -> [15] : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, R'=0, S'=free_10, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, [ 0>=G && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && 1>=Q_1 && 0>=0 ], cost: INF
     97: [21] -> [15] : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, R'=0, S'=free_11, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, [ 0>=G && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && Q_1>=3 && 0>=0 ], cost: INF
     98: [21] -> [15] : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, Q_1'=2, R'=0, S'=free_9, U'=0, V'=0, W'=free_12, X'=free_13, Z'=free_16, D1'=0, J1'=free_18, K1'=free_19, L1'=free_17, M1'=free_17, N1'=0, O1'=0, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, [ 0>=G && free_30>=1 && 0>=0 && free_21>=1 && free_18>=1 && 0>=0 && free_13>=1 && 0>=0 && Q_1==2 ], cost: INF
     99: [21] -> [15] : J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, R'=0, S'=free_11, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, Z'=free_16, D1'=0, J1'=free_18, K1'=free_19, L1'=free_17, M1'=free_17, N1'=0, O1'=0, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, [ 0>=G && free_30>=1 && 0>=0 && free_21>=1 && free_18>=1 && 0>=0 && free_13>=1 && Q_1>=3 && 0>=0 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
    101: f0 -> [15] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, Q_1'=0, R'=0, S'=free_10, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 && 0>=0 && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && 1>=0 && 0>=0 ], cost: INF
    106: f0 -> [15] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, Q_1'=0, R'=0, S'=free_10, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && free_5>=1 && 0>=0 && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && 1>=0 && 0>=0 ], cost: INF
    111: f0 -> [15] : A'=free_25, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, Q_1'=0, R'=0, S'=free_10, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && free_4>=1 && free_25>=1 && free_5>=1 && 0>=0 && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && 1>=0 && 0>=0 ], cost: INF
    116: f0 -> [15] : A'=free_7, B'=0, C'=free, F'=free_27, G'=0, H'=free_28, Q'=free_26, J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, Q_1'=0, R'=0, S'=free_10, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && free_28>=1 && 0>=free_26 && 0>=free_7 && free_27>=1 && 0>=0 && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && 1>=0 && 0>=0 ], cost: INF
    121: f0 -> [15] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, Q_1'=0, R'=0, S'=free_10, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 && 0>=0 && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && 1>=0 && 0>=0 ], cost: INF
     53: f0 -> [19] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free ], cost: 1+free_36
     56: f0 -> [19] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free ], cost: 1+free_42
     54: f0 -> [20] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free ], cost: 1+free_36
     57: f0 -> [20] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free ], cost: 1+free_42
    100: f0 -> [22] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 2+free_36+4*free_35
    102: f0 -> [23] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 2+free_36+4*free_35
    103: f0 -> [24] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 2+free_36+4*free_35
    104: f0 -> [25] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 2+free_36+4*free_35
    105: f0 -> [26] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && free_5>=1 ], cost: 2+free_36+4*free_35
    107: f0 -> [27] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && free_5>=1 ], cost: 2+free_36+4*free_35
    108: f0 -> [28] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && free_5>=1 ], cost: 2+free_36+4*free_35
    109: f0 -> [29] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && free_5>=1 ], cost: 2+free_36+4*free_35
    110: f0 -> [30] : A'=free_25, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && free_4>=1 && free_25>=1 && free_5>=1 ], cost: 2+free_36+4*free_35
    112: f0 -> [31] : A'=free_25, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && free_4>=1 && free_25>=1 && free_5>=1 ], cost: 2+free_36+4*free_35
    113: f0 -> [32] : A'=free_25, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && free_4>=1 && free_25>=1 && free_5>=1 ], cost: 2+free_36+4*free_35
    114: f0 -> [33] : A'=free_25, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && free_4>=1 && free_25>=1 && free_5>=1 ], cost: 2+free_36+4*free_35
    115: f0 -> [34] : A'=free_7, B'=0, C'=free, F'=free_27, G'=0, H'=free_28, Q'=free_26, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && free_28>=1 && 0>=free_26 && 0>=free_7 && free_27>=1 ], cost: 2+free_36+4*free_35
    117: f0 -> [35] : A'=free_7, B'=0, C'=free, F'=free_27, G'=0, H'=free_28, Q'=free_26, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && free_28>=1 && 0>=free_26 && 0>=free_7 && free_27>=1 ], cost: 2+free_36+4*free_35
    118: f0 -> [36] : A'=free_7, B'=0, C'=free, F'=free_27, G'=0, H'=free_28, Q'=free_26, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && free_28>=1 && 0>=free_26 && 0>=free_7 && free_27>=1 ], cost: 2+free_36+4*free_35
    119: f0 -> [37] : A'=free_7, B'=0, C'=free, F'=free_27, G'=0, H'=free_28, Q'=free_26, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && free_28>=1 && 0>=free_26 && 0>=free_7 && free_27>=1 ], cost: 2+free_36+4*free_35
    120: f0 -> [38] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 2+free_42+4*free_35
    122: f0 -> [39] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 2+free_42+4*free_35
    123: f0 -> [40] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 2+free_42+4*free_35
    124: f0 -> [41] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 2+free_42+4*free_35


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
    101: f0 -> [15] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, Q_1'=0, R'=0, S'=free_10, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 && 0>=0 && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && 1>=0 && 0>=0 ], cost: INF
    106: f0 -> [15] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, Q_1'=0, R'=0, S'=free_10, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && free_5>=1 && 0>=0 && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && 1>=0 && 0>=0 ], cost: INF
    111: f0 -> [15] : A'=free_25, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, Q_1'=0, R'=0, S'=free_10, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && free_4>=1 && free_25>=1 && free_5>=1 && 0>=0 && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && 1>=0 && 0>=0 ], cost: INF
    116: f0 -> [15] : A'=free_7, B'=0, C'=free, F'=free_27, G'=0, H'=free_28, Q'=free_26, J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, Q_1'=0, R'=0, S'=free_10, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && free_28>=1 && 0>=free_26 && 0>=free_7 && free_27>=1 && 0>=0 && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && 1>=0 && 0>=0 ], cost: INF
    121: f0 -> [15] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, J'=0, K'=1, L'=0, M'=free_8, N'=0, O'=0, P'=free_8, Q_1'=0, R'=0, S'=free_10, T'=1, U'=0, V'=0, W'=free_12, X'=free_13, J1'=free_14, K1'=free_15, P1'=0, Q1_1'=free_20, R1'=free_21, S1'=free_23, T1'=free_24, U1'=free_22, V1'=free_23, W1'=free_29, X1'=free_30, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 && 0>=0 && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && 1>=0 && 0>=0 ], cost: INF
     53: f0 -> [19] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free ], cost: 1+free_36
     56: f0 -> [19] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free ], cost: 1+free_42
     54: f0 -> [20] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free ], cost: 1+free_36
     57: f0 -> [20] : B'=0, C'=free, K'=0, Q_1'=0, R'=0, T'=0, V'=0, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free ], cost: 1+free_42
    100: f0 -> [22] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 2+free_36+4*free_35
    102: f0 -> [23] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 2+free_36+4*free_35
    103: f0 -> [24] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 2+free_36+4*free_35
    104: f0 -> [25] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 2+free_36+4*free_35
    105: f0 -> [26] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && free_5>=1 ], cost: 2+free_36+4*free_35
    107: f0 -> [27] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && free_5>=1 ], cost: 2+free_36+4*free_35
    108: f0 -> [28] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && free_5>=1 ], cost: 2+free_36+4*free_35
    109: f0 -> [29] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && free_5>=1 ], cost: 2+free_36+4*free_35
    110: f0 -> [30] : A'=free_25, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && free_4>=1 && free_25>=1 && free_5>=1 ], cost: 2+free_36+4*free_35
    112: f0 -> [31] : A'=free_25, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && free_4>=1 && free_25>=1 && free_5>=1 ], cost: 2+free_36+4*free_35
    113: f0 -> [32] : A'=free_25, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && free_4>=1 && free_25>=1 && free_5>=1 ], cost: 2+free_36+4*free_35
    114: f0 -> [33] : A'=free_25, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && free_4>=1 && free_25>=1 && free_5>=1 ], cost: 2+free_36+4*free_35
    115: f0 -> [34] : A'=free_7, B'=0, C'=free, F'=free_27, G'=0, H'=free_28, Q'=free_26, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && free_28>=1 && 0>=free_26 && 0>=free_7 && free_27>=1 ], cost: 2+free_36+4*free_35
    117: f0 -> [35] : A'=free_7, B'=0, C'=free, F'=free_27, G'=0, H'=free_28, Q'=free_26, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && free_28>=1 && 0>=free_26 && 0>=free_7 && free_27>=1 ], cost: 2+free_36+4*free_35
    118: f0 -> [36] : A'=free_7, B'=0, C'=free, F'=free_27, G'=0, H'=free_28, Q'=free_26, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && free_28>=1 && 0>=free_26 && 0>=free_7 && free_27>=1 ], cost: 2+free_36+4*free_35
    119: f0 -> [37] : A'=free_7, B'=0, C'=free, F'=free_27, G'=0, H'=free_28, Q'=free_26, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_37, E2'=free_38, F2'=0, G2'=free_36, [ 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && free_28>=1 && 0>=free_26 && 0>=free_7 && free_27>=1 ], cost: 2+free_36+4*free_35
    120: f0 -> [38] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 2+free_42+4*free_35
    122: f0 -> [39] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 2+free_42+4*free_35
    123: f0 -> [40] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 2+free_42+4*free_35
    124: f0 -> [41] : A'=free_7, B'=0, C'=free, F'=free_5, G'=0, H'=free_6, Q'=free_4, K'=0, Q_1'=0, R'=0, T'=0, V'=0, Z1'=free_34, A2'=free_35, B2'=0, C2'=0, D2'=free_41, E2'=free_43, F2'=0, G2'=free_42, H2'=free_39, Q2'=free_40, J2'=0, [ free_43>=1 && free_42>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 ], cost: 2+free_42+4*free_35


Computing complexity for remaining 29 transitions.

Found new complexity INF, because: INF sat.


The final runtime is determined by this resulting transition:
  Final Guard: 0>=free_38 && free_36>=1 && 0>=free && 0>=0 && free_35>=1 && 0>=free_6 && 0>=free_4 && 0>=free_7 && 0>=free_5 && 0>=0 && free_30>=1 && 0>=0 && free_21>=1 && 0>=free_14 && 0>=0 && free_13>=1 && 1>=0 && 0>=0
  Final Cost:  INF

Obtained the following complexity w.r.t. the length of the input n:
  Complexity class: INF
  Complexity value: INF

WORST_CASE(INF,?)