Trying to load file: main.koat

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


Simplified the transitions:
  Start location: f0
      0: f81 -> f83 : [ 0>=A ], cost: 1
     20: f81 -> f83 : [ A>=1 ], cost: 1
      3: f83 -> f67 : [ 0>=G ], cost: 1
     19: f83 -> f67 : [ G>=1 ], cost: 1
      1: f31 -> f31 : B'=-1+B, C'=free, D'=free, [ 0>=free && B>=1 ], cost: 1
      2: f31 -> f42 : B'=-1+B, C'=free_3, D'=free_3, E'=free_1, F'=free_2, [ B>=1 && free_3>=1 && 0>=free_1 ], cost: 1
     26: f31 -> f42 : B'=-1+B, C'=free_42, D'=free_42, E'=free_40, F'=free_41, [ B>=1 && free_42>=1 && free_40>=1 ], cost: 1
     27: f31 -> f67 : H'=free_43, R'=0, U'=0, D2'=free_44, E2'=free_43, [ 0>=B ], cost: 1
     24: f42 -> f31 : C2'=D, [ 0>=F ], cost: 1
     25: f42 -> f31 : C2'=D, [ F>=1 ], cost: 1
      4: f67 -> f77 : G'=free_6, H'=-1+H, Q'=free_4, J'=free_5, [ H>=1 && 0>=free_4 ], cost: 1
     22: f67 -> f77 : G'=free_38, H'=-1+H, Q'=free_36, J'=free_37, [ H>=1 && free_36>=1 ], cost: 1
     23: f67 -> f104 : R'=0, U'=0, B2'=free_39, [ 0>=H ], cost: 1
      5: f77 -> f81 : A'=free_7, [ 0>=J ], cost: 1
     21: f77 -> f81 : A'=free_35, [ J>=1 ], cost: 1
      6: f235 -> f235 : [], cost: 1
      9: f211 -> f235 : R'=0, S'=free_9, [ 0>=K ], cost: 1
      8: f211 -> f211 : K'=-1+K, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, [ K>=1 ], cost: 1
     10: f144 -> f211 : K'=free_10, R'=0, U'=0, V'=free_11, W'=free_10, [ 0>=T ], cost: 1
     13: f144 -> f144 : R'=0, T'=-1+T, U'=0, J1'=free_13, K1'=free_13, L1'=free_12, [ T>=1 && 0>=free_13 ], cost: 1
     14: f144 -> f144 : R'=0, T'=-1+T, U'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, [ T>=1 && free_17>=1 ], cost: 1
     15: f144 -> f172 : R'=0, T'=-1+T, X'=0, Z'=free_20, D1'=free_21, J1'=free_22, K1'=free_22, L1'=free_19, M1'=free_18, N1'=free_18, O1'=0, P1'=free_21, Q1_1'=free_21, R1'=1, S1'=0, [ 0>=1+free_21 && T>=1 && free_22>=1 ], cost: 1
     16: f144 -> f172 : R'=0, T'=-1+T, X'=0, Z'=free_25, D1'=free_26, J1'=free_27, K1'=free_27, L1'=free_24, M1'=free_23, N1'=free_23, O1'=0, P1'=free_26, Q1_1'=free_26, R1'=1, S1'=0, [ free_26>=1 && T>=1 && free_27>=1 ], cost: 1
     11: f172 -> f144 : U'=0, Y'=0, Z'=X, A1'=X, B1'=0, C1'=D1, E1'=X, F1'=0, G1'=X, H1'=D1, [ X>=1 ], cost: 1
     12: f172 -> f144 : U'=0, Z'=X, Q1'=D1, [ 0>=X ], cost: 1
     17: f104 -> f144 : R'=0, T'=free_29, U'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, [ 0>=free_30 ], cost: 1
     18: f104 -> f104 : R'=0, U'=0, T1'=free_34, U1'=-1+free_34, X1'=free_31, Y1'=free_32, Z1'=free_33, A2'=free_31, [ free_34>=1 ], cost: 1
     28: f0 -> f31 : B'=free_45, R'=0, U'=0, Y'=0, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 ], cost: 1
     29: f0 -> f31 : B'=free_49, R'=0, U'=0, Y'=0, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 ], cost: 1

Eliminating 1 self-loops for location f31
  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 f235
  Self-Loop 6 has unbounded runtime, resulting in the new transition 31.
  Removing the self-loops: 6.
Eliminating 1 self-loops for location f211
  Self-Loop 8 has the metering function: K, resulting in the new transition 32.
  Removing the self-loops: 8.
Eliminating 2 self-loops for location f144
  Self-Loop 13 has the metering function: T, resulting in the new transition 33.
  Self-Loop 14 has the metering function: T, resulting in the new transition 34.
  Removing the self-loops: 13 14.
Eliminating 1 self-loops for location f104
  Self-Loop 18 has unbounded runtime, resulting in the new transition 35.
  Removing the self-loops: 18.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f81 -> f83 : [ 0>=A ], cost: 1
     20: f81 -> f83 : [ A>=1 ], cost: 1
      3: f83 -> f67 : [ 0>=G ], cost: 1
     19: f83 -> f67 : [ G>=1 ], cost: 1
     30: f31 -> [14] : B'=0, C'=free, D'=free, [ 0>=free && B>=1 ], cost: B
     24: f42 -> f31 : C2'=D, [ 0>=F ], cost: 1
     25: f42 -> f31 : C2'=D, [ F>=1 ], cost: 1
      4: f67 -> f77 : G'=free_6, H'=-1+H, Q'=free_4, J'=free_5, [ H>=1 && 0>=free_4 ], cost: 1
     22: f67 -> f77 : G'=free_38, H'=-1+H, Q'=free_36, J'=free_37, [ H>=1 && free_36>=1 ], cost: 1
     23: f67 -> f104 : R'=0, U'=0, B2'=free_39, [ 0>=H ], cost: 1
      5: f77 -> f81 : A'=free_7, [ 0>=J ], cost: 1
     21: f77 -> f81 : A'=free_35, [ J>=1 ], cost: 1
     31: f235 -> [15] : [], cost: INF
     32: f211 -> [16] : K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, [ K>=1 ], cost: K
     33: f144 -> [17] : R'=0, T'=0, U'=0, J1'=free_13, K1'=free_13, L1'=free_12, [ T>=1 && 0>=free_13 ], cost: T
     34: f144 -> [17] : R'=0, T'=0, U'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, [ T>=1 && free_17>=1 ], cost: T
     11: f172 -> f144 : U'=0, Y'=0, Z'=X, A1'=X, B1'=0, C1'=D1, E1'=X, F1'=0, G1'=X, H1'=D1, [ X>=1 ], cost: 1
     12: f172 -> f144 : U'=0, Z'=X, Q1'=D1, [ 0>=X ], cost: 1
     35: f104 -> [18] : [ free_34>=1 ], cost: INF
     28: f0 -> f31 : B'=free_45, R'=0, U'=0, Y'=0, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 ], cost: 1
     29: f0 -> f31 : B'=free_49, R'=0, U'=0, Y'=0, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 ], cost: 1
      2: [14] -> f42 : B'=-1+B, C'=free_3, D'=free_3, E'=free_1, F'=free_2, [ B>=1 && free_3>=1 && 0>=free_1 ], cost: 1
     26: [14] -> f42 : B'=-1+B, C'=free_42, D'=free_42, E'=free_40, F'=free_41, [ B>=1 && free_42>=1 && free_40>=1 ], cost: 1
     27: [14] -> f67 : H'=free_43, R'=0, U'=0, D2'=free_44, E2'=free_43, [ 0>=B ], cost: 1
      9: [16] -> f235 : R'=0, S'=free_9, [ 0>=K ], cost: 1
     10: [17] -> f211 : K'=free_10, R'=0, U'=0, V'=free_11, W'=free_10, [ 0>=T ], cost: 1
     15: [17] -> f172 : R'=0, T'=-1+T, X'=0, Z'=free_20, D1'=free_21, J1'=free_22, K1'=free_22, L1'=free_19, M1'=free_18, N1'=free_18, O1'=0, P1'=free_21, Q1_1'=free_21, R1'=1, S1'=0, [ 0>=1+free_21 && T>=1 && free_22>=1 ], cost: 1
     16: [17] -> f172 : R'=0, T'=-1+T, X'=0, Z'=free_25, D1'=free_26, J1'=free_27, K1'=free_27, L1'=free_24, M1'=free_23, N1'=free_23, O1'=0, P1'=free_26, Q1_1'=free_26, R1'=1, S1'=0, [ free_26>=1 && T>=1 && free_27>=1 ], cost: 1
     17: [18] -> f144 : R'=0, T'=free_29, U'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, [ 0>=free_30 ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f81 -> f83 : [ 0>=A ], cost: 1
     20: f81 -> f83 : [ A>=1 ], cost: 1
      3: f83 -> f67 : [ 0>=G ], cost: 1
     19: f83 -> f67 : [ G>=1 ], cost: 1
     30: f31 -> [14] : B'=0, C'=free, D'=free, [ 0>=free && B>=1 ], cost: B
     24: f42 -> f31 : C2'=D, [ 0>=F ], cost: 1
     25: f42 -> f31 : C2'=D, [ F>=1 ], cost: 1
      4: f67 -> f77 : G'=free_6, H'=-1+H, Q'=free_4, J'=free_5, [ H>=1 && 0>=free_4 ], cost: 1
     22: f67 -> f77 : G'=free_38, H'=-1+H, Q'=free_36, J'=free_37, [ H>=1 && free_36>=1 ], cost: 1
     23: f67 -> f144 : R'=0, T'=free_29, U'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 ], cost: INF
      5: f77 -> f81 : A'=free_7, [ 0>=J ], cost: 1
     21: f77 -> f81 : A'=free_35, [ J>=1 ], cost: 1
     33: f144 -> [17] : R'=0, T'=0, U'=0, J1'=free_13, K1'=free_13, L1'=free_12, [ T>=1 && 0>=free_13 ], cost: T
     34: f144 -> [17] : R'=0, T'=0, U'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, [ T>=1 && free_17>=1 ], cost: T
     11: f172 -> f144 : U'=0, Y'=0, Z'=X, A1'=X, B1'=0, C1'=D1, E1'=X, F1'=0, G1'=X, H1'=D1, [ X>=1 ], cost: 1
     12: f172 -> f144 : U'=0, Z'=X, Q1'=D1, [ 0>=X ], cost: 1
     28: f0 -> f31 : B'=free_45, R'=0, U'=0, Y'=0, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 ], cost: 1
     29: f0 -> f31 : B'=free_49, R'=0, U'=0, Y'=0, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 ], cost: 1
      2: [14] -> f42 : B'=-1+B, C'=free_3, D'=free_3, E'=free_1, F'=free_2, [ B>=1 && free_3>=1 && 0>=free_1 ], cost: 1
     26: [14] -> f42 : B'=-1+B, C'=free_42, D'=free_42, E'=free_40, F'=free_41, [ B>=1 && free_42>=1 && free_40>=1 ], cost: 1
     27: [14] -> f67 : H'=free_43, R'=0, U'=0, D2'=free_44, E2'=free_43, [ 0>=B ], cost: 1
     15: [17] -> f172 : R'=0, T'=-1+T, X'=0, Z'=free_20, D1'=free_21, J1'=free_22, K1'=free_22, L1'=free_19, M1'=free_18, N1'=free_18, O1'=0, P1'=free_21, Q1_1'=free_21, R1'=1, S1'=0, [ 0>=1+free_21 && T>=1 && free_22>=1 ], cost: 1
     16: [17] -> f172 : R'=0, T'=-1+T, X'=0, Z'=free_25, D1'=free_26, J1'=free_27, K1'=free_27, L1'=free_24, M1'=free_23, N1'=free_23, O1'=0, P1'=free_26, Q1_1'=free_26, R1'=1, S1'=0, [ free_26>=1 && T>=1 && free_27>=1 ], cost: 1
     10: [17] -> [15] : K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, U'=0, V'=free_11, W'=free_10, [ 0>=T && free_10>=1 && 0>=0 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
     43: f81 -> f67 : [ 0>=A && 0>=G ], cost: 2
     44: f81 -> f67 : [ 0>=A && G>=1 ], cost: 2
     45: f81 -> f67 : [ A>=1 && 0>=G ], cost: 2
     46: f81 -> f67 : [ A>=1 && G>=1 ], cost: 2
     38: f31 -> f67 : B'=0, C'=free, D'=free, H'=free_43, R'=0, U'=0, D2'=free_44, E2'=free_43, [ 0>=free && B>=1 && 0>=0 ], cost: 1+B
     36: f31 -> [19] : B'=0, C'=free, D'=free, [ 0>=free && B>=1 ], cost: B
     37: f31 -> [20] : B'=0, C'=free, D'=free, [ 0>=free && B>=1 ], cost: B
     39: f67 -> f81 : A'=free_7, G'=free_6, H'=-1+H, Q'=free_4, J'=free_5, [ H>=1 && 0>=free_4 && 0>=free_5 ], cost: 2
     40: f67 -> f81 : A'=free_35, G'=free_6, H'=-1+H, Q'=free_4, J'=free_5, [ H>=1 && 0>=free_4 && free_5>=1 ], cost: 2
     41: f67 -> f81 : A'=free_7, G'=free_38, H'=-1+H, Q'=free_36, J'=free_37, [ H>=1 && free_36>=1 && 0>=free_37 ], cost: 2
     42: f67 -> f81 : A'=free_35, G'=free_38, H'=-1+H, Q'=free_36, J'=free_37, [ H>=1 && free_36>=1 && free_37>=1 ], cost: 2
     23: f67 -> f144 : R'=0, T'=free_29, U'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 ], cost: INF
     49: f144 -> [15] : K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, T'=0, U'=0, V'=free_11, W'=free_10, J1'=free_13, K1'=free_13, L1'=free_12, [ T>=1 && 0>=free_13 && 0>=0 && free_10>=1 && 0>=0 ], cost: INF
     52: f144 -> [15] : K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, T'=0, U'=0, V'=free_11, W'=free_10, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, [ T>=1 && free_17>=1 && 0>=0 && free_10>=1 && 0>=0 ], cost: INF
     47: f144 -> [21] : R'=0, T'=0, U'=0, J1'=free_13, K1'=free_13, L1'=free_12, [ T>=1 && 0>=free_13 ], cost: T
     48: f144 -> [22] : R'=0, T'=0, U'=0, J1'=free_13, K1'=free_13, L1'=free_12, [ T>=1 && 0>=free_13 ], cost: T
     50: f144 -> [23] : R'=0, T'=0, U'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, [ T>=1 && free_17>=1 ], cost: T
     51: f144 -> [24] : R'=0, T'=0, U'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, [ T>=1 && free_17>=1 ], cost: T
     28: f0 -> f31 : B'=free_45, R'=0, U'=0, Y'=0, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 ], cost: 1
     29: f0 -> f31 : B'=free_49, R'=0, U'=0, Y'=0, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
     59: f67 -> f67 : A'=free_7, G'=free_6, H'=-1+H, Q'=free_4, J'=free_5, [ H>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 ], cost: 4
     60: f67 -> f67 : A'=free_7, G'=free_6, H'=-1+H, Q'=free_4, J'=free_5, [ H>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && free_6>=1 ], cost: 4
     62: f67 -> f67 : A'=free_7, G'=free_6, H'=-1+H, Q'=free_4, J'=free_5, [ H>=1 && 0>=free_4 && 0>=free_5 && free_7>=1 && free_6>=1 ], cost: 4
     66: f67 -> f67 : A'=free_35, G'=free_6, H'=-1+H, Q'=free_4, J'=free_5, [ H>=1 && 0>=free_4 && free_5>=1 && free_35>=1 && free_6>=1 ], cost: 4
     68: f67 -> f67 : A'=free_7, G'=free_38, H'=-1+H, Q'=free_36, J'=free_37, [ H>=1 && free_36>=1 && 0>=free_37 && 0>=free_7 && free_38>=1 ], cost: 4
     75: f67 -> [15] : K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, T'=0, U'=0, V'=free_11, W'=free_10, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 && 0>=0 && free_10>=1 && 0>=0 ], cost: INF
     76: f67 -> [15] : K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, T'=0, U'=0, V'=free_11, W'=free_10, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 && 0>=0 && free_10>=1 && 0>=0 ], cost: INF
     77: f67 -> [21] : R'=0, T'=0, U'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
     78: f67 -> [22] : R'=0, T'=0, U'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
     79: f67 -> [23] : R'=0, T'=0, U'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
     80: f67 -> [24] : R'=0, T'=0, U'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
     53: f0 -> f67 : B'=0, C'=free, D'=free, H'=free_43, R'=0, U'=0, Y'=0, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 ], cost: 2+free_45
     56: f0 -> f67 : B'=0, C'=free, D'=free, H'=free_43, R'=0, U'=0, Y'=0, D2'=free_44, E2'=free_43, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 && 0>=0 ], cost: 2+free_49
     54: f0 -> [19] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 ], cost: 1+free_45
     57: f0 -> [19] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 ], cost: 1+free_49
     55: f0 -> [20] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 ], cost: 1+free_45
     58: f0 -> [20] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 ], cost: 1+free_49

Eliminating 5 self-loops for location f67
  Self-Loop 59 has the metering function: H, resulting in the new transition 81.
  Self-Loop 60 has the metering function: H, resulting in the new transition 82.
  Self-Loop 62 has the metering function: H, resulting in the new transition 83.
  Self-Loop 66 has the metering function: H, resulting in the new transition 84.
  Self-Loop 68 has the metering function: H, resulting in the new transition 85.
  Removing the self-loops: 59 60 62 66 68.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
     81: f67 -> [25] : A'=free_7, G'=free_6, H'=0, Q'=free_4, J'=free_5, [ H>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 ], cost: 4*H
     82: f67 -> [25] : A'=free_7, G'=free_6, H'=0, Q'=free_4, J'=free_5, [ H>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && free_6>=1 ], cost: 4*H
     83: f67 -> [25] : A'=free_7, G'=free_6, H'=0, Q'=free_4, J'=free_5, [ H>=1 && 0>=free_4 && 0>=free_5 && free_7>=1 && free_6>=1 ], cost: 4*H
     84: f67 -> [25] : A'=free_35, G'=free_6, H'=0, Q'=free_4, J'=free_5, [ H>=1 && 0>=free_4 && free_5>=1 && free_35>=1 && free_6>=1 ], cost: 4*H
     85: f67 -> [25] : A'=free_7, G'=free_38, H'=0, Q'=free_36, J'=free_37, [ H>=1 && free_36>=1 && 0>=free_37 && 0>=free_7 && free_38>=1 ], cost: 4*H
     53: f0 -> f67 : B'=0, C'=free, D'=free, H'=free_43, R'=0, U'=0, Y'=0, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 ], cost: 2+free_45
     56: f0 -> f67 : B'=0, C'=free, D'=free, H'=free_43, R'=0, U'=0, Y'=0, D2'=free_44, E2'=free_43, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 && 0>=0 ], cost: 2+free_49
     54: f0 -> [19] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 ], cost: 1+free_45
     57: f0 -> [19] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 ], cost: 1+free_49
     55: f0 -> [20] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 ], cost: 1+free_45
     58: f0 -> [20] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 ], cost: 1+free_49
     75: [25] -> [15] : K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, T'=0, U'=0, V'=free_11, W'=free_10, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 && 0>=0 && free_10>=1 && 0>=0 ], cost: INF
     76: [25] -> [15] : K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, T'=0, U'=0, V'=free_11, W'=free_10, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 && 0>=0 && free_10>=1 && 0>=0 ], cost: INF
     77: [25] -> [21] : R'=0, T'=0, U'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
     78: [25] -> [22] : R'=0, T'=0, U'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
     79: [25] -> [23] : R'=0, T'=0, U'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
     80: [25] -> [24] : R'=0, T'=0, U'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
     54: f0 -> [19] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 ], cost: 1+free_45
     57: f0 -> [19] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 ], cost: 1+free_49
     55: f0 -> [20] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 ], cost: 1+free_45
     58: f0 -> [20] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 ], cost: 1+free_49
     86: f0 -> [25] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, U'=0, Y'=0, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 ], cost: 2+free_45+4*free_43
     87: f0 -> [25] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, U'=0, Y'=0, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && free_6>=1 ], cost: 2+free_45+4*free_43
     89: f0 -> [25] : A'=free_35, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, U'=0, Y'=0, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && free_5>=1 && free_35>=1 && free_6>=1 ], cost: 2+free_45+4*free_43
     90: f0 -> [25] : A'=free_7, B'=0, C'=free, D'=free, G'=free_38, H'=0, Q'=free_36, J'=free_37, R'=0, U'=0, Y'=0, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && free_36>=1 && 0>=free_37 && 0>=free_7 && free_38>=1 ], cost: 2+free_45+4*free_43
     91: f0 -> [25] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, U'=0, Y'=0, D2'=free_44, E2'=free_43, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 ], cost: 2+free_49+4*free_43
     75: [25] -> [15] : K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, T'=0, U'=0, V'=free_11, W'=free_10, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 && 0>=0 && free_10>=1 && 0>=0 ], cost: INF
     76: [25] -> [15] : K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, T'=0, U'=0, V'=free_11, W'=free_10, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 && 0>=0 && free_10>=1 && 0>=0 ], cost: INF
     77: [25] -> [21] : R'=0, T'=0, U'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
     78: [25] -> [22] : R'=0, T'=0, U'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
     79: [25] -> [23] : R'=0, T'=0, U'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
     80: [25] -> [24] : R'=0, T'=0, U'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, [ 0>=H && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
     96: f0 -> [15] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, T'=0, U'=0, V'=free_11, W'=free_10, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 && 0>=0 && free_10>=1 && 0>=0 ], cost: INF
     97: f0 -> [15] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, T'=0, U'=0, V'=free_11, W'=free_10, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 && 0>=0 && free_10>=1 && 0>=0 ], cost: INF
    103: f0 -> [15] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, T'=0, U'=0, V'=free_11, W'=free_10, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 && 0>=0 && free_10>=1 && 0>=0 ], cost: INF
    108: f0 -> [15] : A'=free_35, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, T'=0, U'=0, V'=free_11, W'=free_10, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && free_5>=1 && free_35>=1 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 && 0>=0 && free_10>=1 && 0>=0 ], cost: INF
    109: f0 -> [15] : A'=free_35, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, T'=0, U'=0, V'=free_11, W'=free_10, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && free_5>=1 && free_35>=1 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 && 0>=0 && free_10>=1 && 0>=0 ], cost: INF
     54: f0 -> [19] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 ], cost: 1+free_45
     57: f0 -> [19] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 ], cost: 1+free_49
     55: f0 -> [20] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 ], cost: 1+free_45
     58: f0 -> [20] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 ], cost: 1+free_49
     98: f0 -> [21] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
    104: f0 -> [21] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
    110: f0 -> [21] : A'=free_35, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && free_5>=1 && free_35>=1 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
    116: f0 -> [21] : A'=free_7, B'=0, C'=free, D'=free, G'=free_38, H'=0, Q'=free_36, J'=free_37, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && free_36>=1 && 0>=free_37 && 0>=free_7 && free_38>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
    122: f0 -> [21] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
     99: f0 -> [22] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
    105: f0 -> [22] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
    111: f0 -> [22] : A'=free_35, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && free_5>=1 && free_35>=1 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
    117: f0 -> [22] : A'=free_7, B'=0, C'=free, D'=free, G'=free_38, H'=0, Q'=free_36, J'=free_37, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && free_36>=1 && 0>=free_37 && 0>=free_7 && free_38>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
    123: f0 -> [22] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
    100: f0 -> [23] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
    106: f0 -> [23] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
    112: f0 -> [23] : A'=free_35, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && free_5>=1 && free_35>=1 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
    118: f0 -> [23] : A'=free_7, B'=0, C'=free, D'=free, G'=free_38, H'=0, Q'=free_36, J'=free_37, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && free_36>=1 && 0>=free_37 && 0>=free_7 && free_38>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
    124: f0 -> [23] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
    101: f0 -> [24] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
    107: f0 -> [24] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
    113: f0 -> [24] : A'=free_35, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && free_5>=1 && free_35>=1 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
    119: f0 -> [24] : A'=free_7, B'=0, C'=free, D'=free, G'=free_38, H'=0, Q'=free_36, J'=free_37, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && free_36>=1 && 0>=free_37 && 0>=free_7 && free_38>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
    125: f0 -> [24] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
     96: f0 -> [15] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, T'=0, U'=0, V'=free_11, W'=free_10, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 && 0>=0 && free_10>=1 && 0>=0 ], cost: INF
     97: f0 -> [15] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, T'=0, U'=0, V'=free_11, W'=free_10, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 && 0>=0 && free_10>=1 && 0>=0 ], cost: INF
    103: f0 -> [15] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, T'=0, U'=0, V'=free_11, W'=free_10, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 && 0>=0 && free_10>=1 && 0>=0 ], cost: INF
    108: f0 -> [15] : A'=free_35, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, T'=0, U'=0, V'=free_11, W'=free_10, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && free_5>=1 && free_35>=1 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 && 0>=0 && free_10>=1 && 0>=0 ], cost: INF
    109: f0 -> [15] : A'=free_35, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, K'=0, L'=0, M'=free_8, N'=0, O'=0, P'=2, Q_1'=free_8, R'=0, S'=free_9, T'=0, U'=0, V'=free_11, W'=free_10, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && free_5>=1 && free_35>=1 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 && 0>=0 && free_10>=1 && 0>=0 ], cost: INF
     54: f0 -> [19] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 ], cost: 1+free_45
     57: f0 -> [19] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 ], cost: 1+free_49
     55: f0 -> [20] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 ], cost: 1+free_45
     58: f0 -> [20] : B'=0, C'=free, D'=free, R'=0, U'=0, Y'=0, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 ], cost: 1+free_49
     98: f0 -> [21] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
    104: f0 -> [21] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
    110: f0 -> [21] : A'=free_35, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && free_5>=1 && free_35>=1 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
    116: f0 -> [21] : A'=free_7, B'=0, C'=free, D'=free, G'=free_38, H'=0, Q'=free_36, J'=free_37, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && free_36>=1 && 0>=free_37 && 0>=free_7 && free_38>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
    122: f0 -> [21] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
     99: f0 -> [22] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
    105: f0 -> [22] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
    111: f0 -> [22] : A'=free_35, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && free_5>=1 && free_35>=1 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
    117: f0 -> [22] : A'=free_7, B'=0, C'=free, D'=free, G'=free_38, H'=0, Q'=free_36, J'=free_37, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && free_36>=1 && 0>=free_37 && 0>=free_7 && free_38>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
    123: f0 -> [22] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, J1'=free_13, K1'=free_13, L1'=free_12, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 ], cost: INF
    100: f0 -> [23] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
    106: f0 -> [23] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
    112: f0 -> [23] : A'=free_35, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && free_5>=1 && free_35>=1 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
    118: f0 -> [23] : A'=free_7, B'=0, C'=free, D'=free, G'=free_38, H'=0, Q'=free_36, J'=free_37, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && free_36>=1 && 0>=free_37 && 0>=free_7 && free_38>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
    124: f0 -> [23] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
    101: f0 -> [24] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
    107: f0 -> [24] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
    113: f0 -> [24] : A'=free_35, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && free_5>=1 && free_35>=1 && free_6>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
    119: f0 -> [24] : A'=free_7, B'=0, C'=free, D'=free, G'=free_38, H'=0, Q'=free_36, J'=free_37, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_46, G2'=0, H2'=free_45, [ 0>=free_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && free_36>=1 && 0>=free_37 && 0>=free_7 && free_38>=1 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF
    125: f0 -> [24] : A'=free_7, B'=0, C'=free, D'=free, G'=free_6, H'=0, Q'=free_4, J'=free_5, R'=0, T'=0, U'=0, Y'=0, Z'=free_15, D1'=0, J1'=free_17, K1'=free_17, L1'=free_14, M1'=free_16, N1'=free_16, O1'=0, P1'=0, Q1_1'=0, T1'=free_30, U1'=free_30, V1'=free_28, W1'=free_29, B2'=free_39, D2'=free_44, E2'=free_43, F2'=free_50, G2'=0, H2'=free_49, Q2'=free_47, J2'=free_48, K2'=0, [ free_50>=1 && 0>=free && free_49>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && free_17>=1 ], cost: INF


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_46 && 0>=free && free_45>=1 && 0>=0 && free_43>=1 && 0>=free_4 && 0>=free_5 && 0>=free_7 && 0>=free_6 && 0>=0 && free_34>=1 && 0>=free_30 && free_29>=1 && 0>=free_13 && 0>=0 && free_10>=1 && 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,?)