Trying to load file: main.koat

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


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

Eliminating 1 self-loops for location f31
  Self-Loop 1 has the metering function: B, resulting in the new transition 31.
  Removing the self-loops: 1.
Eliminating 1 self-loops for location f237
  Self-Loop 6 has unbounded runtime, resulting in the new transition 32.
  Removing the self-loops: 6.
Eliminating 2 self-loops for location f211
  Self-Loop 8 has unbounded runtime, resulting in the new transition 33.
  Self-Loop 9 has the metering function: K, resulting in the new transition 34.
  Removing the self-loops: 8 9.
Eliminating 2 self-loops for location f144
  Self-Loop 14 has the metering function: U, resulting in the new transition 35.
  Self-Loop 15 has the metering function: U, resulting in the new transition 36.
  Removing the self-loops: 14 15.
Eliminating 1 self-loops for location f104
  Self-Loop 19 has unbounded runtime, resulting in the new transition 37.
  Removing the self-loops: 19.

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


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


Applied chaining over branches and pruning:
  Start location: f0
     45: f81 -> f67 : [ 0>=A && 0>=G ], cost: 2
     46: f81 -> f67 : [ 0>=A && G>=1 ], cost: 2
     47: f81 -> f67 : [ A>=1 && 0>=G ], cost: 2
     48: f81 -> f67 : [ A>=1 && G>=1 ], cost: 2
     40: f31 -> f67 : B'=0, C'=free, D'=free, H'=free_47, S'=0, V'=0, E2'=free_46, F2'=free_47, [ 0>=free && B>=1 && 0>=0 ], cost: 1+B
     38: f31 -> [19] : B'=0, C'=free, D'=free, [ 0>=free && B>=1 ], cost: B
     39: f31 -> [20] : B'=0, C'=free, D'=free, [ 0>=free && B>=1 ], cost: B
     41: f67 -> f81 : A'=free_7, G'=free_4, H'=-1+H, Q'=free_5, J'=free_6, [ H>=1 && 0>=free_5 && 0>=free_6 ], cost: 2
     42: f67 -> f81 : A'=free_38, G'=free_4, H'=-1+H, Q'=free_5, J'=free_6, [ H>=1 && 0>=free_5 && free_6>=1 ], cost: 2
     43: f67 -> f81 : A'=free_7, G'=free_39, H'=-1+H, Q'=free_40, J'=free_41, [ H>=1 && free_40>=1 && 0>=free_41 ], cost: 2
     44: f67 -> f81 : A'=free_38, G'=free_39, H'=-1+H, Q'=free_40, J'=free_41, [ H>=1 && free_40>=1 && free_41>=1 ], cost: 2
     24: f67 -> f144 : S'=0, U'=free_33, V'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 ], cost: INF
     56: f211 -> [15] : K'=0, L'=0, M'=free_10, N'=free_11, O'=0, P'=0, Q_1'=2, R'=free_10, S'=0, T'=free_12, [ K>=1 && free_11>=1 && 0>=0 ], cost: INF
     55: f211 -> [25] : [ K>=1 && 0>=free_9 ], cost: INF
     49: f144 -> f211 : K'=free_14, S'=0, U'=0, V'=0, W'=free_13, X'=free_14, K1'=free_15, L1'=free_15, M1'=free_16, [ U>=1 && 0>=free_15 && 0>=0 ], cost: 1+U
     52: f144 -> f211 : K'=free_14, S'=0, U'=0, V'=0, W'=free_13, X'=free_14, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, [ U>=1 && free_18>=1 && 0>=0 ], cost: 1+U
     50: f144 -> [21] : S'=0, U'=0, V'=0, K1'=free_15, L1'=free_15, M1'=free_16, [ U>=1 && 0>=free_15 ], cost: U
     51: f144 -> [22] : S'=0, U'=0, V'=0, K1'=free_15, L1'=free_15, M1'=free_16, [ U>=1 && 0>=free_15 ], cost: U
     53: f144 -> [23] : S'=0, U'=0, V'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, [ U>=1 && free_18>=1 ], cost: U
     54: f144 -> [24] : S'=0, U'=0, V'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, [ U>=1 && free_18>=1 ], cost: U
     29: f0 -> f31 : B'=free_49, S'=0, V'=0, Z'=0, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 ], cost: 1
     30: f0 -> f31 : B'=free_50, S'=0, V'=0, Z'=0, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
     63: f67 -> f67 : A'=free_7, G'=free_4, H'=-1+H, Q'=free_5, J'=free_6, [ H>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 ], cost: 4
     64: f67 -> f67 : A'=free_7, G'=free_4, H'=-1+H, Q'=free_5, J'=free_6, [ H>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && free_4>=1 ], cost: 4
     66: f67 -> f67 : A'=free_7, G'=free_4, H'=-1+H, Q'=free_5, J'=free_6, [ H>=1 && 0>=free_5 && 0>=free_6 && free_7>=1 && free_4>=1 ], cost: 4
     70: f67 -> f67 : A'=free_38, G'=free_4, H'=-1+H, Q'=free_5, J'=free_6, [ H>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 ], cost: 4
     72: f67 -> f67 : A'=free_7, G'=free_39, H'=-1+H, Q'=free_40, J'=free_41, [ H>=1 && free_40>=1 && 0>=free_41 && 0>=free_7 && free_39>=1 ], cost: 4
     79: f67 -> f211 : K'=free_14, S'=0, U'=0, V'=0, W'=free_13, X'=free_14, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 && 0>=0 ], cost: INF
     80: f67 -> f211 : K'=free_14, S'=0, U'=0, V'=0, W'=free_13, X'=free_14, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 && 0>=0 ], cost: INF
     81: f67 -> [21] : S'=0, U'=0, V'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
     82: f67 -> [22] : S'=0, U'=0, V'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
     83: f67 -> [23] : S'=0, U'=0, V'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
     84: f67 -> [24] : S'=0, U'=0, V'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
     56: f211 -> [15] : K'=0, L'=0, M'=free_10, N'=free_11, O'=0, P'=0, Q_1'=2, R'=free_10, S'=0, T'=free_12, [ K>=1 && free_11>=1 && 0>=0 ], cost: INF
     55: f211 -> [25] : [ K>=1 && 0>=free_9 ], cost: INF
     57: f0 -> f67 : B'=0, C'=free, D'=free, H'=free_47, S'=0, V'=0, Z'=0, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 ], cost: 2+free_49
     60: f0 -> f67 : B'=0, C'=free, D'=free, H'=free_47, S'=0, V'=0, Z'=0, E2'=free_46, F2'=free_47, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 && 0>=0 ], cost: 2+free_50
     58: f0 -> [19] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 ], cost: 1+free_49
     61: f0 -> [19] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 ], cost: 1+free_50
     59: f0 -> [20] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 ], cost: 1+free_49
     62: f0 -> [20] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 ], cost: 1+free_50

Eliminating 5 self-loops for location f67
  Self-Loop 63 has the metering function: H, resulting in the new transition 85.
  Self-Loop 64 has the metering function: H, resulting in the new transition 86.
  Self-Loop 66 has the metering function: H, resulting in the new transition 87.
  Self-Loop 70 has the metering function: H, resulting in the new transition 88.
  Self-Loop 72 has the metering function: H, resulting in the new transition 89.
  Removing the self-loops: 63 64 66 70 72.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
     85: f67 -> [26] : A'=free_7, G'=free_4, H'=0, Q'=free_5, J'=free_6, [ H>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 ], cost: 4*H
     86: f67 -> [26] : A'=free_7, G'=free_4, H'=0, Q'=free_5, J'=free_6, [ H>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && free_4>=1 ], cost: 4*H
     87: f67 -> [26] : A'=free_7, G'=free_4, H'=0, Q'=free_5, J'=free_6, [ H>=1 && 0>=free_5 && 0>=free_6 && free_7>=1 && free_4>=1 ], cost: 4*H
     88: f67 -> [26] : A'=free_38, G'=free_4, H'=0, Q'=free_5, J'=free_6, [ H>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 ], cost: 4*H
     89: f67 -> [26] : A'=free_7, G'=free_39, H'=0, Q'=free_40, J'=free_41, [ H>=1 && free_40>=1 && 0>=free_41 && 0>=free_7 && free_39>=1 ], cost: 4*H
     56: f211 -> [15] : K'=0, L'=0, M'=free_10, N'=free_11, O'=0, P'=0, Q_1'=2, R'=free_10, S'=0, T'=free_12, [ K>=1 && free_11>=1 && 0>=0 ], cost: INF
     55: f211 -> [25] : [ K>=1 && 0>=free_9 ], cost: INF
     57: f0 -> f67 : B'=0, C'=free, D'=free, H'=free_47, S'=0, V'=0, Z'=0, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 ], cost: 2+free_49
     60: f0 -> f67 : B'=0, C'=free, D'=free, H'=free_47, S'=0, V'=0, Z'=0, E2'=free_46, F2'=free_47, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 && 0>=0 ], cost: 2+free_50
     58: f0 -> [19] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 ], cost: 1+free_49
     61: f0 -> [19] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 ], cost: 1+free_50
     59: f0 -> [20] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 ], cost: 1+free_49
     62: f0 -> [20] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 ], cost: 1+free_50
     79: [26] -> f211 : K'=free_14, S'=0, U'=0, V'=0, W'=free_13, X'=free_14, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 && 0>=0 ], cost: INF
     80: [26] -> f211 : K'=free_14, S'=0, U'=0, V'=0, W'=free_13, X'=free_14, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 && 0>=0 ], cost: INF
     81: [26] -> [21] : S'=0, U'=0, V'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
     82: [26] -> [22] : S'=0, U'=0, V'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
     83: [26] -> [23] : S'=0, U'=0, V'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
     84: [26] -> [24] : S'=0, U'=0, V'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
     58: f0 -> [19] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 ], cost: 1+free_49
     61: f0 -> [19] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 ], cost: 1+free_50
     59: f0 -> [20] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 ], cost: 1+free_49
     62: f0 -> [20] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 ], cost: 1+free_50
     90: f0 -> [26] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, V'=0, Z'=0, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 ], cost: 2+4*free_47+free_49
     91: f0 -> [26] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, V'=0, Z'=0, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && free_4>=1 ], cost: 2+4*free_47+free_49
     93: f0 -> [26] : A'=free_38, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, V'=0, Z'=0, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 ], cost: 2+4*free_47+free_49
     94: f0 -> [26] : A'=free_7, B'=0, C'=free, D'=free, G'=free_39, H'=0, Q'=free_40, J'=free_41, S'=0, V'=0, Z'=0, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && free_40>=1 && 0>=free_41 && 0>=free_7 && free_39>=1 ], cost: 2+4*free_47+free_49
     95: f0 -> [26] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, V'=0, Z'=0, E2'=free_46, F2'=free_47, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 ], cost: 2+free_50+4*free_47
    100: [26] -> [15] : K'=0, L'=0, M'=free_10, N'=free_11, O'=0, P'=0, Q_1'=2, R'=free_10, S'=0, T'=free_12, U'=0, V'=0, W'=free_13, X'=free_14, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 && 0>=0 && free_14>=1 && free_11>=1 && 0>=0 ], cost: INF
    102: [26] -> [15] : K'=0, L'=0, M'=free_10, N'=free_11, O'=0, P'=0, Q_1'=2, R'=free_10, S'=0, T'=free_12, U'=0, V'=0, W'=free_13, X'=free_14, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 && 0>=0 && free_14>=1 && free_11>=1 && 0>=0 ], cost: INF
     81: [26] -> [21] : S'=0, U'=0, V'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
     82: [26] -> [22] : S'=0, U'=0, V'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
     83: [26] -> [23] : S'=0, U'=0, V'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
     84: [26] -> [24] : S'=0, U'=0, V'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    101: [26] -> [25] : K'=free_14, S'=0, U'=0, V'=0, W'=free_13, X'=free_14, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 && 0>=0 && free_14>=1 && 0>=free_9 ], cost: INF
    103: [26] -> [25] : K'=free_14, S'=0, U'=0, V'=0, W'=free_13, X'=free_14, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, [ 0>=H && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 && 0>=0 && free_14>=1 && 0>=free_9 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
    104: f0 -> [15] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=0, L'=0, M'=free_10, N'=free_11, O'=0, P'=0, Q_1'=2, R'=free_10, S'=0, T'=free_12, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 && 0>=0 && free_14>=1 && free_11>=1 && 0>=0 ], cost: INF
    105: f0 -> [15] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=0, L'=0, M'=free_10, N'=free_11, O'=0, P'=0, Q_1'=2, R'=free_10, S'=0, T'=free_12, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 && 0>=0 && free_14>=1 && free_11>=1 && 0>=0 ], cost: INF
    113: f0 -> [15] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=0, L'=0, M'=free_10, N'=free_11, O'=0, P'=0, Q_1'=2, R'=free_10, S'=0, T'=free_12, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 && 0>=0 && free_14>=1 && free_11>=1 && 0>=0 ], cost: INF
    120: f0 -> [15] : A'=free_38, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=0, L'=0, M'=free_10, N'=free_11, O'=0, P'=0, Q_1'=2, R'=free_10, S'=0, T'=free_12, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 && 0>=0 && free_14>=1 && free_11>=1 && 0>=0 ], cost: INF
    121: f0 -> [15] : A'=free_38, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=0, L'=0, M'=free_10, N'=free_11, O'=0, P'=0, Q_1'=2, R'=free_10, S'=0, T'=free_12, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 && 0>=0 && free_14>=1 && free_11>=1 && 0>=0 ], cost: INF
     58: f0 -> [19] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 ], cost: 1+free_49
     61: f0 -> [19] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 ], cost: 1+free_50
     59: f0 -> [20] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 ], cost: 1+free_49
     62: f0 -> [20] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 ], cost: 1+free_50
    106: f0 -> [21] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    114: f0 -> [21] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    122: f0 -> [21] : A'=free_38, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    130: f0 -> [21] : A'=free_7, B'=0, C'=free, D'=free, G'=free_39, H'=0, Q'=free_40, J'=free_41, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && free_40>=1 && 0>=free_41 && 0>=free_7 && free_39>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    138: f0 -> [21] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    107: f0 -> [22] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    115: f0 -> [22] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    123: f0 -> [22] : A'=free_38, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    131: f0 -> [22] : A'=free_7, B'=0, C'=free, D'=free, G'=free_39, H'=0, Q'=free_40, J'=free_41, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && free_40>=1 && 0>=free_41 && 0>=free_7 && free_39>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    139: f0 -> [22] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    108: f0 -> [23] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    116: f0 -> [23] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    124: f0 -> [23] : A'=free_38, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    132: f0 -> [23] : A'=free_7, B'=0, C'=free, D'=free, G'=free_39, H'=0, Q'=free_40, J'=free_41, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && free_40>=1 && 0>=free_41 && 0>=free_7 && free_39>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    140: f0 -> [23] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    109: f0 -> [24] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    117: f0 -> [24] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    125: f0 -> [24] : A'=free_38, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    133: f0 -> [24] : A'=free_7, B'=0, C'=free, D'=free, G'=free_39, H'=0, Q'=free_40, J'=free_41, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && free_40>=1 && 0>=free_41 && 0>=free_7 && free_39>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    141: f0 -> [24] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    110: f0 -> [25] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=free_14, S'=0, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 && 0>=0 && free_14>=1 && 0>=free_9 ], cost: INF
    111: f0 -> [25] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=free_14, S'=0, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 && 0>=0 && free_14>=1 && 0>=free_9 ], cost: INF
    119: f0 -> [25] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=free_14, S'=0, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 && 0>=0 && free_14>=1 && 0>=free_9 ], cost: INF
    126: f0 -> [25] : A'=free_38, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=free_14, S'=0, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 && 0>=0 && free_14>=1 && 0>=free_9 ], cost: INF
    127: f0 -> [25] : A'=free_38, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=free_14, S'=0, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 && 0>=0 && free_14>=1 && 0>=free_9 ], cost: INF


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
    104: f0 -> [15] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=0, L'=0, M'=free_10, N'=free_11, O'=0, P'=0, Q_1'=2, R'=free_10, S'=0, T'=free_12, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 && 0>=0 && free_14>=1 && free_11>=1 && 0>=0 ], cost: INF
    105: f0 -> [15] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=0, L'=0, M'=free_10, N'=free_11, O'=0, P'=0, Q_1'=2, R'=free_10, S'=0, T'=free_12, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 && 0>=0 && free_14>=1 && free_11>=1 && 0>=0 ], cost: INF
    113: f0 -> [15] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=0, L'=0, M'=free_10, N'=free_11, O'=0, P'=0, Q_1'=2, R'=free_10, S'=0, T'=free_12, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 && 0>=0 && free_14>=1 && free_11>=1 && 0>=0 ], cost: INF
    120: f0 -> [15] : A'=free_38, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=0, L'=0, M'=free_10, N'=free_11, O'=0, P'=0, Q_1'=2, R'=free_10, S'=0, T'=free_12, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 && 0>=0 && free_14>=1 && free_11>=1 && 0>=0 ], cost: INF
    121: f0 -> [15] : A'=free_38, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=0, L'=0, M'=free_10, N'=free_11, O'=0, P'=0, Q_1'=2, R'=free_10, S'=0, T'=free_12, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 && 0>=0 && free_14>=1 && free_11>=1 && 0>=0 ], cost: INF
     58: f0 -> [19] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 ], cost: 1+free_49
     61: f0 -> [19] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 ], cost: 1+free_50
     59: f0 -> [20] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 ], cost: 1+free_49
     62: f0 -> [20] : B'=0, C'=free, D'=free, S'=0, V'=0, Z'=0, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 ], cost: 1+free_50
    106: f0 -> [21] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    114: f0 -> [21] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    122: f0 -> [21] : A'=free_38, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    130: f0 -> [21] : A'=free_7, B'=0, C'=free, D'=free, G'=free_39, H'=0, Q'=free_40, J'=free_41, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && free_40>=1 && 0>=free_41 && 0>=free_7 && free_39>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    138: f0 -> [21] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    107: f0 -> [22] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    115: f0 -> [22] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    123: f0 -> [22] : A'=free_38, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    131: f0 -> [22] : A'=free_7, B'=0, C'=free, D'=free, G'=free_39, H'=0, Q'=free_40, J'=free_41, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && free_40>=1 && 0>=free_41 && 0>=free_7 && free_39>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    139: f0 -> [22] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 ], cost: INF
    108: f0 -> [23] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    116: f0 -> [23] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    124: f0 -> [23] : A'=free_38, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    132: f0 -> [23] : A'=free_7, B'=0, C'=free, D'=free, G'=free_39, H'=0, Q'=free_40, J'=free_41, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && free_40>=1 && 0>=free_41 && 0>=free_7 && free_39>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    140: f0 -> [23] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    109: f0 -> [24] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    117: f0 -> [24] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    125: f0 -> [24] : A'=free_38, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    133: f0 -> [24] : A'=free_7, B'=0, C'=free, D'=free, G'=free_39, H'=0, Q'=free_40, J'=free_41, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && free_40>=1 && 0>=free_41 && 0>=free_7 && free_39>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    141: f0 -> [24] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, S'=0, U'=0, V'=0, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_51, H2'=0, Q2'=free_50, J2'=free_52, K2'=free_53, L2'=0, [ free_51>=1 && 0>=free && free_50>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 ], cost: INF
    110: f0 -> [25] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=free_14, S'=0, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 && 0>=0 && free_14>=1 && 0>=free_9 ], cost: INF
    111: f0 -> [25] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=free_14, S'=0, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 && 0>=0 && free_14>=1 && 0>=free_9 ], cost: INF
    119: f0 -> [25] : A'=free_7, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=free_14, S'=0, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 && 0>=0 && free_14>=1 && 0>=free_9 ], cost: INF
    126: f0 -> [25] : A'=free_38, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=free_14, S'=0, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, K1'=free_15, L1'=free_15, M1'=free_16, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 && 0>=0 && free_14>=1 && 0>=free_9 ], cost: INF
    127: f0 -> [25] : A'=free_38, B'=0, C'=free, D'=free, G'=free_4, H'=0, Q'=free_5, J'=free_6, K'=free_14, S'=0, U'=0, V'=0, W'=free_13, X'=free_14, Z'=0, A1'=free_20, E1'=0, K1'=free_18, L1'=free_18, M1'=free_19, N1'=free_17, O1'=free_17, P1'=0, Q1_1'=0, R1'=0, U1'=free_31, V1'=free_31, W1'=free_32, X1'=free_33, C2'=free_42, E2'=free_46, F2'=free_47, G2'=free_48, H2'=0, Q2'=free_49, [ 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && free_6>=1 && free_38>=1 && free_4>=1 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && free_18>=1 && 0>=0 && free_14>=1 && 0>=free_9 ], cost: INF


Computing complexity for remaining 34 transitions.

Found new complexity INF, because: INF sat.


The final runtime is determined by this resulting transition:
  Final Guard: 0>=free_48 && 0>=free && free_49>=1 && 0>=0 && free_47>=1 && 0>=free_5 && 0>=free_6 && 0>=free_7 && 0>=free_4 && 0>=0 && free_35>=1 && 0>=free_31 && free_33>=1 && 0>=free_15 && 0>=0 && free_14>=1 && free_11>=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,?)