Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f3
      0: f15 -> f22 : A'=3, B'=0, [], cost: 1
      2: f22 -> f33 : A'=7, G'=free_4, Q'=-1+Q, [ 0>=Q && free_4>=1 ], cost: 1
      3: f22 -> f33 : A'=8, G'=free_5, Q'=-2+Q, [ 0>=Q && 0>=free_5 ], cost: 1
      6: f22 -> f53 : A'=11, F'=free_8, [ 0>=Q ], cost: 1
      1: f3 -> f22 : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [], cost: 1
      4: f33 -> f22 : A'=3, M'=free_6, [ 0>=L && 0>=free_6 ], cost: 1
      5: f33 -> f22 : A'=3, L'=1, M'=free_7, N'=F, O'=G, P'=A, Q_1'=B, R'=H, S'=Q, T'=J, [ 0>=L && free_7>=1 ], cost: 1
     92: f33 -> f666666 : Q3_1'=0, R3'=0, [ L>=1 ], cost: 1
     12: f53 -> f89 : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 ], cost: 1
     36: f53 -> f206 : A'=13, H'=0, M1'=F, N1'=G, O1'=13, P1'=B, Q1_1'=0, R1'=Q, S1'=J, K2'=13, L2'=B, M2'=Q, N2'=G, O2'=F, P2'=J, Q2_1'=0, [ 0>=F ], cost: 1
      7: f60 -> f67 : U'=3, V'=0, [], cost: 1
      8: f67 -> f67 : U'=3, W'=-1+W, X'=free_9, [ 0>=W && free_9>=1 ], cost: 1
      9: f67 -> f67 : U'=3, W'=-2+W, X'=free_10, [ 0>=W && 0>=free_10 ], cost: 1
     11: f67 -> f83 : U'=11, Z'=free_12, [ 0>=W ], cost: 1
     10: f128 -> f83 : U'=11, Z'=free_11, [ Y>=1 ], cost: 1
     24: f128 -> f149 : K1'=0, L1'=0, [ 0>=Y ], cost: 1
     13: f83 -> f89 : U'=12, A1'=1, C1'=Z, D1'=X, E1'=12, F1'=V, G1'=1, H1'=W, Q1'=B1, [ Z>=1 ], cost: 1
     18: f83 -> f113 : U'=13, Y'=0, A1'=0, M1'=Z, N1'=X, O1'=13, P1'=V, Q1_1'=0, R1'=W, S1'=B1, T1'=0, [ 0>=Z ], cost: 1
     14: f89 -> f96 : Y'=1, J1'=1, [ G1>=1 ], cost: 1
     15: f89 -> f96 : Y'=0, J1'=0, [ 0>=G1 ], cost: 1
     17: f96 -> f149 : K1'=0, L1'=0, [ 0>=Y ], cost: 1
     20: f96 -> f121 : U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, [ Y>=1 ], cost: 1
     16: f143 -> f149 : K1'=L1, [ Y>=1 ], cost: 1
     27: f143 -> f149 : K1'=0, L1'=0, [ 0>=Y ], cost: 1
     49: f149 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
     19: f113 -> f149 : K1'=0, L1'=0, [ 0>=Y ], cost: 1
     21: f113 -> f121 : U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, [ Y>=1 ], cost: 1
     22: f121 -> f128 : Y'=1, B2'=1, [ Y1>=1 ], cost: 1
     23: f121 -> f128 : Y'=0, B2'=0, [ 0>=Y1 ], cost: 1
     25: f133 -> f143 : Y'=1, C2'=Z, D2'=X, E2'=U, F2'=V, G2'=A1, H2'=W, Q2'=B1, J2'=1, [ A1>=1 ], cost: 1
     26: f133 -> f143 : Y'=0, C2'=Z, D2'=X, E2'=U, F2'=V, G2'=A1, H2'=W, Q2'=B1, J2'=0, [ 0>=A1 ], cost: 1
     28: f160 -> f167 : K2'=3, L2'=0, [], cost: 1
     29: f167 -> f167 : K2'=3, M2'=-1+M2, N2'=free_13, [ 0>=M2 && free_13>=1 ], cost: 1
     30: f167 -> f167 : K2'=3, M2'=-2+M2, N2'=free_14, [ 0>=M2 && 0>=free_14 ], cost: 1
     32: f167 -> f183 : K2'=11, O2'=free_16, [ 0>=M2 ], cost: 1
     31: f228 -> f183 : K2'=11, O2'=free_15, [ Y>=1 ], cost: 1
     45: f228 -> f249 : K1'=0, R2'=0, [ 0>=Y ], cost: 1
     33: f183 -> f196 : Y'=1, C1'=O2, D1'=N2, E1'=12, F1'=L2, G1'=1, H1'=M2, Q1'=P2, J1'=1, K2'=12, Q2_1'=1, [ O2>=1 ], cost: 1
     37: f183 -> f206 : M1'=O2, N1'=N2, O1'=13, P1'=L2, Q1_1'=0, R1'=M2, S1'=P2, K2'=13, Q2_1'=0, [ 0>=O2 ], cost: 1
     35: f196 -> f249 : K1'=0, R2'=0, [ 0>=Y ], cost: 1
     41: f196 -> f221 : U1'=O2, V1'=N2, W1'=K2, X1'=L2, Y1'=Q2_1, Z1'=M2, A2'=P2, [ Y>=1 ], cost: 1
     34: f243 -> f249 : K1'=R2, [ Y>=1 ], cost: 1
     48: f243 -> f249 : K1'=0, R2'=0, [ 0>=Y ], cost: 1
     50: f249 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
     38: f206 -> f213 : Y'=1, T1'=1, [ Q1_1>=1 ], cost: 1
     39: f206 -> f213 : Y'=0, T1'=0, [ 0>=Q1_1 ], cost: 1
     40: f213 -> f249 : K1'=0, R2'=0, [ 0>=Y ], cost: 1
     42: f213 -> f221 : U1'=O2, V1'=N2, W1'=K2, X1'=L2, Y1'=Q2_1, Z1'=M2, A2'=P2, [ Y>=1 ], cost: 1
     43: f221 -> f228 : Y'=1, B2'=1, [ Y1>=1 ], cost: 1
     44: f221 -> f228 : Y'=0, B2'=0, [ 0>=Y1 ], cost: 1
     46: f233 -> f243 : Y'=1, C2'=O2, D2'=N2, E2'=K2, F2'=L2, G2'=Q2_1, H2'=M2, Q2'=P2, J2'=1, [ Q2_1>=1 ], cost: 1
     47: f233 -> f243 : Y'=0, C2'=O2, D2'=N2, E2'=K2, F2'=L2, G2'=Q2_1, H2'=M2, Q2'=P2, J2'=0, [ 0>=Q2_1 ], cost: 1
     56: f281 -> f294 : Y'=1, C1'=S2, D1'=T2, E1'=12, F1'=V2, G1'=1, H1'=X2, Q1'=Y2, J1'=1, U2'=12, W2'=1, [ S2>=1 ], cost: 1
     59: f281 -> f311 : Y'=0, M1'=S2, N1'=T2, O1'=13, P1'=V2, Q1_1'=0, R1'=X2, S1'=Y2, T1'=0, U2'=13, W2'=0, [ 0>=S2 ], cost: 1
     51: f258 -> f265 : U2'=3, V2'=0, [], cost: 1
     55: f265 -> f281 : S2'=free_20, U2'=11, [ 0>=X2 ], cost: 1
     52: f265 -> f265 : T2'=free_17, U2'=3, X2'=-1+X2, [ 0>=X2 && free_17>=1 ], cost: 1
     53: f265 -> f265 : T2'=free_18, U2'=3, X2'=-2+X2, [ 0>=X2 && 0>=free_18 ], cost: 1
     54: f326 -> f281 : S2'=free_19, U2'=11, [ Y>=1 ], cost: 1
     65: f326 -> f347 : K1'=0, Z2'=0, [ 0>=Y ], cost: 1
     58: f294 -> f347 : K1'=0, Z2'=0, [ 0>=Y ], cost: 1
     61: f294 -> f319 : U1'=S2, V1'=T2, W1'=U2, X1'=V2, Y1'=W2, Z1'=X2, A2'=Y2, [ Y>=1 ], cost: 1
     57: f341 -> f347 : K1'=Z2, [ Y>=1 ], cost: 1
     68: f341 -> f347 : K1'=0, Z2'=0, [ 0>=Y ], cost: 1
     69: f347 -> f53 : A'=11, F'=free_21, A3'=free_22, [ 0>=free_22 && 0>=K && 0>=K1 ], cost: 1
     70: f347 -> f53 : A'=11, F'=free_23, K'=1, A3'=free_24, B3'=F, C3'=G, D3'=A, E3'=B, F3'=H, G3'=Q, H3'=J, [ free_24>=1 && 0>=K && 0>=K1 ], cost: 1
     93: f347 -> f666666 : Q3_1'=0, R3'=0, [ K>=1 && 0>=K1 ], cost: 1
     60: f311 -> f347 : K1'=0, Z2'=0, [ 0>=Y ], cost: 1
     62: f311 -> f319 : U1'=S2, V1'=T2, W1'=U2, X1'=V2, Y1'=W2, Z1'=X2, A2'=Y2, [ Y>=1 ], cost: 1
     63: f319 -> f326 : Y'=1, B2'=1, [ Y1>=1 ], cost: 1
     64: f319 -> f326 : Y'=0, B2'=0, [ 0>=Y1 ], cost: 1
     66: f331 -> f341 : Y'=1, C2'=S2, D2'=T2, E2'=U2, F2'=V2, G2'=W2, H2'=X2, Q2'=Y2, J2'=1, [ W2>=1 ], cost: 1
     67: f331 -> f341 : Y'=0, C2'=S2, D2'=T2, E2'=U2, F2'=V2, G2'=W2, H2'=X2, Q2'=Y2, J2'=0, [ 0>=W2 ], cost: 1
     71: f371 -> f378 : Q3'=3, J3'=0, [], cost: 1
     72: f378 -> f378 : Q3'=3, K3'=-1+K3, L3'=free_25, [ 0>=K3 && free_25>=1 ], cost: 1
     73: f378 -> f378 : Q3'=3, K3'=-2+K3, L3'=free_26, [ 0>=K3 && 0>=free_26 ], cost: 1
     76: f378 -> f394 : Q3'=11, M3'=free_29, [ 0>=K3 ], cost: 1
     74: f439 -> f394 : Q3'=11, M3'=free_27, [ Y>=1 ], cost: 1
     86: f439 -> f460 : K1'=0, P3'=0, [ 0>=Y ], cost: 1
     77: f394 -> f407 : Y'=1, C1'=M3, D1'=L3, E1'=12, F1'=J3, G1'=1, H1'=K3, Q1'=O3, J1'=1, Q3'=12, N3'=1, [ M3>=1 ], cost: 1
     80: f394 -> f424 : Y'=0, M1'=M3, N1'=L3, O1'=13, P1'=J3, Q1_1'=0, R1'=K3, S1'=O3, T1'=0, Q3'=13, N3'=0, [ 0>=M3 ], cost: 1
     75: f367 -> f394 : Q3'=11, J3'=B, K3'=Q, L3'=G, M3'=free_28, N3'=H, O3'=J, [], cost: 1
     79: f407 -> f460 : K1'=0, P3'=0, [ 0>=Y ], cost: 1
     82: f407 -> f432 : U1'=M3, V1'=L3, W1'=Q3, X1'=J3, Y1'=N3, Z1'=K3, A2'=O3, [ Y>=1 ], cost: 1
     78: f454 -> f460 : K1'=P3, [ Y>=1 ], cost: 1
     89: f454 -> f460 : K1'=0, P3'=0, [ 0>=Y ], cost: 1
     90: f460 -> f666666 : R3'=Q3_1, [ Q3_1>=2 && 0>=K1 ], cost: 1
     91: f460 -> f666666 : R3'=Q3_1, [ 0>=Q3_1 && 0>=K1 ], cost: 1
     81: f424 -> f460 : K1'=0, P3'=0, [ 0>=Y ], cost: 1
     83: f424 -> f432 : U1'=M3, V1'=L3, W1'=Q3, X1'=J3, Y1'=N3, Z1'=K3, A2'=O3, [ Y>=1 ], cost: 1
     84: f432 -> f439 : Y'=1, B2'=1, [ Y1>=1 ], cost: 1
     85: f432 -> f439 : Y'=0, B2'=0, [ 0>=Y1 ], cost: 1
     87: f444 -> f454 : Y'=1, C2'=M3, D2'=L3, E2'=Q3, F2'=J3, G2'=N3, H2'=K3, Q2'=O3, J2'=1, [ N3>=1 ], cost: 1
     88: f444 -> f454 : Y'=0, C2'=M3, D2'=L3, E2'=Q3, F2'=J3, G2'=N3, H2'=K3, Q2'=O3, J2'=0, [ 0>=N3 ], cost: 1


Simplified the transitions:
  Start location: f3
      2: f22 -> f33 : A'=7, G'=free_4, Q'=-1+Q, [ 0>=Q && free_4>=1 ], cost: 1
      3: f22 -> f33 : A'=8, G'=free_5, Q'=-2+Q, [ 0>=Q && 0>=free_5 ], cost: 1
      6: f22 -> f53 : A'=11, F'=free_8, [ 0>=Q ], cost: 1
      1: f3 -> f22 : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [], cost: 1
      4: f33 -> f22 : A'=3, M'=free_6, [ 0>=L && 0>=free_6 ], cost: 1
      5: f33 -> f22 : A'=3, L'=1, M'=free_7, N'=F, O'=G, P'=A, Q_1'=B, R'=H, S'=Q, T'=J, [ 0>=L && free_7>=1 ], cost: 1
     12: f53 -> f89 : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 ], cost: 1
     36: f53 -> f206 : A'=13, H'=0, M1'=F, N1'=G, O1'=13, P1'=B, Q1_1'=0, R1'=Q, S1'=J, K2'=13, L2'=B, M2'=Q, N2'=G, O2'=F, P2'=J, Q2_1'=0, [ 0>=F ], cost: 1
     10: f128 -> f83 : U'=11, Z'=free_11, [ Y>=1 ], cost: 1
     24: f128 -> f149 : K1'=0, L1'=0, [ 0>=Y ], cost: 1
     13: f83 -> f89 : U'=12, A1'=1, C1'=Z, D1'=X, E1'=12, F1'=V, G1'=1, H1'=W, Q1'=B1, [ Z>=1 ], cost: 1
     18: f83 -> f113 : U'=13, Y'=0, A1'=0, M1'=Z, N1'=X, O1'=13, P1'=V, Q1_1'=0, R1'=W, S1'=B1, T1'=0, [ 0>=Z ], cost: 1
     14: f89 -> f96 : Y'=1, J1'=1, [ G1>=1 ], cost: 1
     15: f89 -> f96 : Y'=0, J1'=0, [ 0>=G1 ], cost: 1
     17: f96 -> f149 : K1'=0, L1'=0, [ 0>=Y ], cost: 1
     20: f96 -> f121 : U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, [ Y>=1 ], cost: 1
     49: f149 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
     19: f113 -> f149 : K1'=0, L1'=0, [ 0>=Y ], cost: 1
     21: f113 -> f121 : U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, [ Y>=1 ], cost: 1
     22: f121 -> f128 : Y'=1, B2'=1, [ Y1>=1 ], cost: 1
     23: f121 -> f128 : Y'=0, B2'=0, [ 0>=Y1 ], cost: 1
     31: f228 -> f183 : K2'=11, O2'=free_15, [ Y>=1 ], cost: 1
     45: f228 -> f249 : K1'=0, R2'=0, [ 0>=Y ], cost: 1
     33: f183 -> f196 : Y'=1, C1'=O2, D1'=N2, E1'=12, F1'=L2, G1'=1, H1'=M2, Q1'=P2, J1'=1, K2'=12, Q2_1'=1, [ O2>=1 ], cost: 1
     37: f183 -> f206 : M1'=O2, N1'=N2, O1'=13, P1'=L2, Q1_1'=0, R1'=M2, S1'=P2, K2'=13, Q2_1'=0, [ 0>=O2 ], cost: 1
     35: f196 -> f249 : K1'=0, R2'=0, [ 0>=Y ], cost: 1
     41: f196 -> f221 : U1'=O2, V1'=N2, W1'=K2, X1'=L2, Y1'=Q2_1, Z1'=M2, A2'=P2, [ Y>=1 ], cost: 1
     50: f249 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
     38: f206 -> f213 : Y'=1, T1'=1, [ Q1_1>=1 ], cost: 1
     39: f206 -> f213 : Y'=0, T1'=0, [ 0>=Q1_1 ], cost: 1
     40: f213 -> f249 : K1'=0, R2'=0, [ 0>=Y ], cost: 1
     42: f213 -> f221 : U1'=O2, V1'=N2, W1'=K2, X1'=L2, Y1'=Q2_1, Z1'=M2, A2'=P2, [ Y>=1 ], cost: 1
     43: f221 -> f228 : Y'=1, B2'=1, [ Y1>=1 ], cost: 1
     44: f221 -> f228 : Y'=0, B2'=0, [ 0>=Y1 ], cost: 1
     56: f281 -> f294 : Y'=1, C1'=S2, D1'=T2, E1'=12, F1'=V2, G1'=1, H1'=X2, Q1'=Y2, J1'=1, U2'=12, W2'=1, [ S2>=1 ], cost: 1
     59: f281 -> f311 : Y'=0, M1'=S2, N1'=T2, O1'=13, P1'=V2, Q1_1'=0, R1'=X2, S1'=Y2, T1'=0, U2'=13, W2'=0, [ 0>=S2 ], cost: 1
     54: f326 -> f281 : S2'=free_19, U2'=11, [ Y>=1 ], cost: 1
     65: f326 -> f347 : K1'=0, Z2'=0, [ 0>=Y ], cost: 1
     58: f294 -> f347 : K1'=0, Z2'=0, [ 0>=Y ], cost: 1
     61: f294 -> f319 : U1'=S2, V1'=T2, W1'=U2, X1'=V2, Y1'=W2, Z1'=X2, A2'=Y2, [ Y>=1 ], cost: 1
     69: f347 -> f53 : A'=11, F'=free_21, A3'=free_22, [ 0>=free_22 && 0>=K && 0>=K1 ], cost: 1
     70: f347 -> f53 : A'=11, F'=free_23, K'=1, A3'=free_24, B3'=F, C3'=G, D3'=A, E3'=B, F3'=H, G3'=Q, H3'=J, [ free_24>=1 && 0>=K && 0>=K1 ], cost: 1
     60: f311 -> f347 : K1'=0, Z2'=0, [ 0>=Y ], cost: 1
     62: f311 -> f319 : U1'=S2, V1'=T2, W1'=U2, X1'=V2, Y1'=W2, Z1'=X2, A2'=Y2, [ Y>=1 ], cost: 1
     63: f319 -> f326 : Y'=1, B2'=1, [ Y1>=1 ], cost: 1
     64: f319 -> f326 : Y'=0, B2'=0, [ 0>=Y1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f3
     94: f22 -> f22 : A'=3, G'=free_4, Q'=-1+Q, M'=free_6, [ 0>=Q && free_4>=1 && 0>=L && 0>=free_6 ], cost: 2
     95: f22 -> f22 : A'=3, G'=free_4, Q'=-1+Q, L'=1, M'=free_7, N'=F, O'=free_4, P'=7, Q_1'=B, R'=H, S'=-1+Q, T'=J, [ 0>=Q && free_4>=1 && 0>=L && free_7>=1 ], cost: 2
     96: f22 -> f22 : A'=3, G'=free_5, Q'=-2+Q, M'=free_6, [ 0>=Q && 0>=free_5 && 0>=L && 0>=free_6 ], cost: 2
     97: f22 -> f22 : A'=3, G'=free_5, Q'=-2+Q, L'=1, M'=free_7, N'=F, O'=free_5, P'=8, Q_1'=B, R'=H, S'=-2+Q, T'=J, [ 0>=Q && 0>=free_5 && 0>=L && free_7>=1 ], cost: 2
      6: f22 -> f53 : A'=11, F'=free_8, [ 0>=Q ], cost: 1
      1: f3 -> f22 : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [], cost: 1
     12: f53 -> f89 : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 ], cost: 1
     36: f53 -> f206 : A'=13, H'=0, M1'=F, N1'=G, O1'=13, P1'=B, Q1_1'=0, R1'=Q, S1'=J, K2'=13, L2'=B, M2'=Q, N2'=G, O2'=F, P2'=J, Q2_1'=0, [ 0>=F ], cost: 1
     13: f83 -> f89 : U'=12, A1'=1, C1'=Z, D1'=X, E1'=12, F1'=V, G1'=1, H1'=W, Q1'=B1, [ Z>=1 ], cost: 1
    106: f83 -> f149 : U'=13, Y'=0, A1'=0, K1'=0, L1'=0, M1'=Z, N1'=X, O1'=13, P1'=V, Q1_1'=0, R1'=W, S1'=B1, T1'=0, [ 0>=Z && 0>=0 ], cost: 2
     99: f89 -> f149 : Y'=0, J1'=0, K1'=0, L1'=0, [ 0>=G1 && 0>=0 ], cost: 2
     98: f89 -> f121 : Y'=1, J1'=1, U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, [ G1>=1 && 1>=1 ], cost: 2
     49: f149 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
    104: f121 -> f83 : U'=11, Y'=1, Z'=free_11, B2'=1, [ Y1>=1 && 1>=1 ], cost: 2
    105: f121 -> f149 : Y'=0, K1'=0, L1'=0, B2'=0, [ 0>=Y1 && 0>=0 ], cost: 2
     37: f183 -> f206 : M1'=O2, N1'=N2, O1'=13, P1'=L2, Q1_1'=0, R1'=M2, S1'=P2, K2'=13, Q2_1'=0, [ 0>=O2 ], cost: 1
    111: f183 -> f221 : Y'=1, C1'=O2, D1'=N2, E1'=12, F1'=L2, G1'=1, H1'=M2, Q1'=P2, J1'=1, U1'=O2, V1'=N2, W1'=12, X1'=L2, Y1'=1, Z1'=M2, A2'=P2, K2'=12, Q2_1'=1, [ O2>=1 && 1>=1 ], cost: 2
     50: f249 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
    108: f206 -> f249 : Y'=0, K1'=0, T1'=0, R2'=0, [ 0>=Q1_1 && 0>=0 ], cost: 2
    107: f206 -> f221 : Y'=1, T1'=1, U1'=O2, V1'=N2, W1'=K2, X1'=L2, Y1'=Q2_1, Z1'=M2, A2'=P2, [ Q1_1>=1 && 1>=1 ], cost: 2
    109: f221 -> f183 : Y'=1, B2'=1, K2'=11, O2'=free_15, [ Y1>=1 && 1>=1 ], cost: 2
    110: f221 -> f249 : Y'=0, K1'=0, B2'=0, R2'=0, [ 0>=Y1 && 0>=0 ], cost: 2
    101: f281 -> f347 : Y'=0, K1'=0, M1'=S2, N1'=T2, O1'=13, P1'=V2, Q1_1'=0, R1'=X2, S1'=Y2, T1'=0, U2'=13, W2'=0, Z2'=0, [ 0>=S2 && 0>=0 ], cost: 2
    100: f281 -> f319 : Y'=1, C1'=S2, D1'=T2, E1'=12, F1'=V2, G1'=1, H1'=X2, Q1'=Y2, J1'=1, U1'=S2, V1'=T2, W1'=12, X1'=V2, Y1'=1, Z1'=X2, A2'=Y2, U2'=12, W2'=1, [ S2>=1 && 1>=1 ], cost: 2
     69: f347 -> f53 : A'=11, F'=free_21, A3'=free_22, [ 0>=free_22 && 0>=K && 0>=K1 ], cost: 1
     70: f347 -> f53 : A'=11, F'=free_23, K'=1, A3'=free_24, B3'=F, C3'=G, D3'=A, E3'=B, F3'=H, G3'=Q, H3'=J, [ free_24>=1 && 0>=K && 0>=K1 ], cost: 1
    102: f319 -> f281 : Y'=1, B2'=1, S2'=free_19, U2'=11, [ Y1>=1 && 1>=1 ], cost: 2
    103: f319 -> f347 : Y'=0, K1'=0, B2'=0, Z2'=0, [ 0>=Y1 && 0>=0 ], cost: 2

Eliminating 4 self-loops for location f22
  Self-Loop 94 has unbounded runtime, resulting in the new transition 112.
  Self-Loop 96 has unbounded runtime, resulting in the new transition 114.
  Removing the self-loops: 94 95 96 97.
Adding an epsilon transition (to model nonexecution of the loops): 116.

Removed all Self-loops using metering functions (where possible):
  Start location: f3
    112: f22 -> [49] : [ 0>=Q && free_4>=1 && 0>=L && 0>=free_6 ], cost: INF
    113: f22 -> [49] : A'=3, G'=free_4, Q'=-1+Q, L'=1, M'=free_7, N'=F, O'=free_4, P'=7, Q_1'=B, R'=H, S'=-1+Q, T'=J, [ 0>=Q && free_4>=1 && 0>=L && free_7>=1 ], cost: 2
    114: f22 -> [49] : [ 0>=Q && 0>=free_5 && 0>=L && 0>=free_6 ], cost: INF
    115: f22 -> [49] : A'=3, G'=free_5, Q'=-2+Q, L'=1, M'=free_7, N'=F, O'=free_5, P'=8, Q_1'=B, R'=H, S'=-2+Q, T'=J, [ 0>=Q && 0>=free_5 && 0>=L && free_7>=1 ], cost: 2
    116: f22 -> [49] : [], cost: 0
      1: f3 -> f22 : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [], cost: 1
     12: f53 -> f89 : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 ], cost: 1
     36: f53 -> f206 : A'=13, H'=0, M1'=F, N1'=G, O1'=13, P1'=B, Q1_1'=0, R1'=Q, S1'=J, K2'=13, L2'=B, M2'=Q, N2'=G, O2'=F, P2'=J, Q2_1'=0, [ 0>=F ], cost: 1
     13: f83 -> f89 : U'=12, A1'=1, C1'=Z, D1'=X, E1'=12, F1'=V, G1'=1, H1'=W, Q1'=B1, [ Z>=1 ], cost: 1
    106: f83 -> f149 : U'=13, Y'=0, A1'=0, K1'=0, L1'=0, M1'=Z, N1'=X, O1'=13, P1'=V, Q1_1'=0, R1'=W, S1'=B1, T1'=0, [ 0>=Z && 0>=0 ], cost: 2
     99: f89 -> f149 : Y'=0, J1'=0, K1'=0, L1'=0, [ 0>=G1 && 0>=0 ], cost: 2
     98: f89 -> f121 : Y'=1, J1'=1, U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, [ G1>=1 && 1>=1 ], cost: 2
     49: f149 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
    104: f121 -> f83 : U'=11, Y'=1, Z'=free_11, B2'=1, [ Y1>=1 && 1>=1 ], cost: 2
    105: f121 -> f149 : Y'=0, K1'=0, L1'=0, B2'=0, [ 0>=Y1 && 0>=0 ], cost: 2
     37: f183 -> f206 : M1'=O2, N1'=N2, O1'=13, P1'=L2, Q1_1'=0, R1'=M2, S1'=P2, K2'=13, Q2_1'=0, [ 0>=O2 ], cost: 1
    111: f183 -> f221 : Y'=1, C1'=O2, D1'=N2, E1'=12, F1'=L2, G1'=1, H1'=M2, Q1'=P2, J1'=1, U1'=O2, V1'=N2, W1'=12, X1'=L2, Y1'=1, Z1'=M2, A2'=P2, K2'=12, Q2_1'=1, [ O2>=1 && 1>=1 ], cost: 2
     50: f249 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
    108: f206 -> f249 : Y'=0, K1'=0, T1'=0, R2'=0, [ 0>=Q1_1 && 0>=0 ], cost: 2
    107: f206 -> f221 : Y'=1, T1'=1, U1'=O2, V1'=N2, W1'=K2, X1'=L2, Y1'=Q2_1, Z1'=M2, A2'=P2, [ Q1_1>=1 && 1>=1 ], cost: 2
    109: f221 -> f183 : Y'=1, B2'=1, K2'=11, O2'=free_15, [ Y1>=1 && 1>=1 ], cost: 2
    110: f221 -> f249 : Y'=0, K1'=0, B2'=0, R2'=0, [ 0>=Y1 && 0>=0 ], cost: 2
    101: f281 -> f347 : Y'=0, K1'=0, M1'=S2, N1'=T2, O1'=13, P1'=V2, Q1_1'=0, R1'=X2, S1'=Y2, T1'=0, U2'=13, W2'=0, Z2'=0, [ 0>=S2 && 0>=0 ], cost: 2
    100: f281 -> f319 : Y'=1, C1'=S2, D1'=T2, E1'=12, F1'=V2, G1'=1, H1'=X2, Q1'=Y2, J1'=1, U1'=S2, V1'=T2, W1'=12, X1'=V2, Y1'=1, Z1'=X2, A2'=Y2, U2'=12, W2'=1, [ S2>=1 && 1>=1 ], cost: 2
     69: f347 -> f53 : A'=11, F'=free_21, A3'=free_22, [ 0>=free_22 && 0>=K && 0>=K1 ], cost: 1
     70: f347 -> f53 : A'=11, F'=free_23, K'=1, A3'=free_24, B3'=F, C3'=G, D3'=A, E3'=B, F3'=H, G3'=Q, H3'=J, [ free_24>=1 && 0>=K && 0>=K1 ], cost: 1
    102: f319 -> f281 : Y'=1, B2'=1, S2'=free_19, U2'=11, [ Y1>=1 && 1>=1 ], cost: 2
    103: f319 -> f347 : Y'=0, K1'=0, B2'=0, Z2'=0, [ 0>=Y1 && 0>=0 ], cost: 2
      6: [49] -> f53 : A'=11, F'=free_8, [ 0>=Q ], cost: 1


Applied chaining over branches and pruning:
  Start location: f3
    117: f3 -> [49] : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 ], cost: INF
    118: f3 -> [49] : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_4, H'=0, Q'=-1+free_2, J'=free_3, K'=0, L'=1, M'=free_7, N'=free, O'=free_4, P'=7, Q_1'=0, R'=0, S'=-1+free_2, T'=free_3, [ 0>=free_2 && free_4>=1 && 0>=0 && free_7>=1 ], cost: 3
    119: f3 -> [49] : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 ], cost: INF
    120: f3 -> [49] : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_5, H'=0, Q'=-2+free_2, J'=free_3, K'=0, L'=1, M'=free_7, N'=free, O'=free_5, P'=8, Q_1'=0, R'=0, S'=-2+free_2, T'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && free_7>=1 ], cost: 3
    121: f3 -> [49] : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [], cost: 1
     12: f53 -> f89 : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 ], cost: 1
     36: f53 -> f206 : A'=13, H'=0, M1'=F, N1'=G, O1'=13, P1'=B, Q1_1'=0, R1'=Q, S1'=J, K2'=13, L2'=B, M2'=Q, N2'=G, O2'=F, P2'=J, Q2_1'=0, [ 0>=F ], cost: 1
     13: f83 -> f89 : U'=12, A1'=1, C1'=Z, D1'=X, E1'=12, F1'=V, G1'=1, H1'=W, Q1'=B1, [ Z>=1 ], cost: 1
    106: f83 -> f149 : U'=13, Y'=0, A1'=0, K1'=0, L1'=0, M1'=Z, N1'=X, O1'=13, P1'=V, Q1_1'=0, R1'=W, S1'=B1, T1'=0, [ 0>=Z && 0>=0 ], cost: 2
    122: f89 -> f83 : U'=11, Y'=1, Z'=free_11, J1'=1, U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, B2'=1, [ G1>=1 && 1>=1 && A1>=1 && 1>=1 ], cost: 4
     99: f89 -> f149 : Y'=0, J1'=0, K1'=0, L1'=0, [ 0>=G1 && 0>=0 ], cost: 2
    123: f89 -> f149 : Y'=0, J1'=1, K1'=0, L1'=0, U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, B2'=0, [ G1>=1 && 1>=1 && 0>=A1 && 0>=0 ], cost: 4
     49: f149 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
     50: f249 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
    108: f206 -> f249 : Y'=0, K1'=0, T1'=0, R2'=0, [ 0>=Q1_1 && 0>=0 ], cost: 2
    107: f206 -> f221 : Y'=1, T1'=1, U1'=O2, V1'=N2, W1'=K2, X1'=L2, Y1'=Q2_1, Z1'=M2, A2'=P2, [ Q1_1>=1 && 1>=1 ], cost: 2
    110: f221 -> f249 : Y'=0, K1'=0, B2'=0, R2'=0, [ 0>=Y1 && 0>=0 ], cost: 2
    125: f221 -> f206 : Y'=1, M1'=free_15, N1'=N2, O1'=13, P1'=L2, Q1_1'=0, R1'=M2, S1'=P2, B2'=1, K2'=13, O2'=free_15, Q2_1'=0, [ Y1>=1 && 1>=1 && 0>=free_15 ], cost: 3
    126: f221 -> f221 : Y'=1, C1'=free_15, D1'=N2, E1'=12, F1'=L2, G1'=1, H1'=M2, Q1'=P2, J1'=1, U1'=free_15, V1'=N2, W1'=12, X1'=L2, Y1'=1, Z1'=M2, A2'=P2, B2'=1, K2'=12, O2'=free_15, Q2_1'=1, [ Y1>=1 && 1>=1 && free_15>=1 && 1>=1 ], cost: 4
    124: f281 -> f281 : Y'=1, C1'=S2, D1'=T2, E1'=12, F1'=V2, G1'=1, H1'=X2, Q1'=Y2, J1'=1, U1'=S2, V1'=T2, W1'=12, X1'=V2, Y1'=1, Z1'=X2, A2'=Y2, B2'=1, S2'=free_19, U2'=11, W2'=1, [ S2>=1 && 1>=1 && 1>=1 && 1>=1 ], cost: 4
    101: f281 -> f347 : Y'=0, K1'=0, M1'=S2, N1'=T2, O1'=13, P1'=V2, Q1_1'=0, R1'=X2, S1'=Y2, T1'=0, U2'=13, W2'=0, Z2'=0, [ 0>=S2 && 0>=0 ], cost: 2
     69: f347 -> f53 : A'=11, F'=free_21, A3'=free_22, [ 0>=free_22 && 0>=K && 0>=K1 ], cost: 1
     70: f347 -> f53 : A'=11, F'=free_23, K'=1, A3'=free_24, B3'=F, C3'=G, D3'=A, E3'=B, F3'=H, G3'=Q, H3'=J, [ free_24>=1 && 0>=K && 0>=K1 ], cost: 1
      6: [49] -> f53 : A'=11, F'=free_8, [ 0>=Q ], cost: 1

Eliminating 1 self-loops for location f221
  Self-Loop 126 has unbounded runtime, resulting in the new transition 127.
  Removing the self-loops: 126.
Eliminating 1 self-loops for location f281
  Removing the self-loops: 124.
Adding an epsilon transition (to model nonexecution of the loops): 129.

Removed all Self-loops using metering functions (where possible):
  Start location: f3
    117: f3 -> [49] : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 ], cost: INF
    118: f3 -> [49] : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_4, H'=0, Q'=-1+free_2, J'=free_3, K'=0, L'=1, M'=free_7, N'=free, O'=free_4, P'=7, Q_1'=0, R'=0, S'=-1+free_2, T'=free_3, [ 0>=free_2 && free_4>=1 && 0>=0 && free_7>=1 ], cost: 3
    119: f3 -> [49] : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 ], cost: INF
    120: f3 -> [49] : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_5, H'=0, Q'=-2+free_2, J'=free_3, K'=0, L'=1, M'=free_7, N'=free, O'=free_5, P'=8, Q_1'=0, R'=0, S'=-2+free_2, T'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && free_7>=1 ], cost: 3
    121: f3 -> [49] : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [], cost: 1
     12: f53 -> f89 : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 ], cost: 1
     36: f53 -> f206 : A'=13, H'=0, M1'=F, N1'=G, O1'=13, P1'=B, Q1_1'=0, R1'=Q, S1'=J, K2'=13, L2'=B, M2'=Q, N2'=G, O2'=F, P2'=J, Q2_1'=0, [ 0>=F ], cost: 1
     13: f83 -> f89 : U'=12, A1'=1, C1'=Z, D1'=X, E1'=12, F1'=V, G1'=1, H1'=W, Q1'=B1, [ Z>=1 ], cost: 1
    106: f83 -> f149 : U'=13, Y'=0, A1'=0, K1'=0, L1'=0, M1'=Z, N1'=X, O1'=13, P1'=V, Q1_1'=0, R1'=W, S1'=B1, T1'=0, [ 0>=Z && 0>=0 ], cost: 2
    122: f89 -> f83 : U'=11, Y'=1, Z'=free_11, J1'=1, U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, B2'=1, [ G1>=1 && 1>=1 && A1>=1 && 1>=1 ], cost: 4
     99: f89 -> f149 : Y'=0, J1'=0, K1'=0, L1'=0, [ 0>=G1 && 0>=0 ], cost: 2
    123: f89 -> f149 : Y'=0, J1'=1, K1'=0, L1'=0, U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, B2'=0, [ G1>=1 && 1>=1 && 0>=A1 && 0>=0 ], cost: 4
     49: f149 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
     50: f249 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
    108: f206 -> f249 : Y'=0, K1'=0, T1'=0, R2'=0, [ 0>=Q1_1 && 0>=0 ], cost: 2
    107: f206 -> f221 : Y'=1, T1'=1, U1'=O2, V1'=N2, W1'=K2, X1'=L2, Y1'=Q2_1, Z1'=M2, A2'=P2, [ Q1_1>=1 && 1>=1 ], cost: 2
    127: f221 -> [50] : [ Y1>=1 && free_15>=1 ], cost: INF
    128: f281 -> [51] : Y'=1, C1'=S2, D1'=T2, E1'=12, F1'=V2, G1'=1, H1'=X2, Q1'=Y2, J1'=1, U1'=S2, V1'=T2, W1'=12, X1'=V2, Y1'=1, Z1'=X2, A2'=Y2, B2'=1, S2'=free_19, U2'=11, W2'=1, [ S2>=1 ], cost: 4
    129: f281 -> [51] : [], cost: 0
     69: f347 -> f53 : A'=11, F'=free_21, A3'=free_22, [ 0>=free_22 && 0>=K && 0>=K1 ], cost: 1
     70: f347 -> f53 : A'=11, F'=free_23, K'=1, A3'=free_24, B3'=F, C3'=G, D3'=A, E3'=B, F3'=H, G3'=Q, H3'=J, [ free_24>=1 && 0>=K && 0>=K1 ], cost: 1
      6: [49] -> f53 : A'=11, F'=free_8, [ 0>=Q ], cost: 1
    110: [50] -> f249 : Y'=0, K1'=0, B2'=0, R2'=0, [ 0>=Y1 && 0>=0 ], cost: 2
    125: [50] -> f206 : Y'=1, M1'=free_15, N1'=N2, O1'=13, P1'=L2, Q1_1'=0, R1'=M2, S1'=P2, B2'=1, K2'=13, O2'=free_15, Q2_1'=0, [ Y1>=1 && 1>=1 && 0>=free_15 ], cost: 3
    101: [51] -> f347 : Y'=0, K1'=0, M1'=S2, N1'=T2, O1'=13, P1'=V2, Q1_1'=0, R1'=X2, S1'=Y2, T1'=0, U2'=13, W2'=0, Z2'=0, [ 0>=S2 && 0>=0 ], cost: 2


Applied simple chaining:
  Start location: f3
    117: f3 -> [49] : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 ], cost: INF
    118: f3 -> [49] : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_4, H'=0, Q'=-1+free_2, J'=free_3, K'=0, L'=1, M'=free_7, N'=free, O'=free_4, P'=7, Q_1'=0, R'=0, S'=-1+free_2, T'=free_3, [ 0>=free_2 && free_4>=1 && 0>=0 && free_7>=1 ], cost: 3
    119: f3 -> [49] : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 ], cost: INF
    120: f3 -> [49] : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_5, H'=0, Q'=-2+free_2, J'=free_3, K'=0, L'=1, M'=free_7, N'=free, O'=free_5, P'=8, Q_1'=0, R'=0, S'=-2+free_2, T'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && free_7>=1 ], cost: 3
    121: f3 -> [49] : A'=3, B'=0, C'=0, D'=0, E'=0, F'=free, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [], cost: 1
     12: f53 -> f89 : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 ], cost: 1
     36: f53 -> f206 : A'=13, H'=0, M1'=F, N1'=G, O1'=13, P1'=B, Q1_1'=0, R1'=Q, S1'=J, K2'=13, L2'=B, M2'=Q, N2'=G, O2'=F, P2'=J, Q2_1'=0, [ 0>=F ], cost: 1
     13: f83 -> f89 : U'=12, A1'=1, C1'=Z, D1'=X, E1'=12, F1'=V, G1'=1, H1'=W, Q1'=B1, [ Z>=1 ], cost: 1
    106: f83 -> f149 : U'=13, Y'=0, A1'=0, K1'=0, L1'=0, M1'=Z, N1'=X, O1'=13, P1'=V, Q1_1'=0, R1'=W, S1'=B1, T1'=0, [ 0>=Z && 0>=0 ], cost: 2
    122: f89 -> f83 : U'=11, Y'=1, Z'=free_11, J1'=1, U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, B2'=1, [ G1>=1 && 1>=1 && A1>=1 && 1>=1 ], cost: 4
     99: f89 -> f149 : Y'=0, J1'=0, K1'=0, L1'=0, [ 0>=G1 && 0>=0 ], cost: 2
    123: f89 -> f149 : Y'=0, J1'=1, K1'=0, L1'=0, U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, B2'=0, [ G1>=1 && 1>=1 && 0>=A1 && 0>=0 ], cost: 4
     49: f149 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
     50: f249 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
    108: f206 -> f249 : Y'=0, K1'=0, T1'=0, R2'=0, [ 0>=Q1_1 && 0>=0 ], cost: 2
    107: f206 -> [50] : Y'=1, T1'=1, U1'=O2, V1'=N2, W1'=K2, X1'=L2, Y1'=Q2_1, Z1'=M2, A2'=P2, [ Q1_1>=1 && 1>=1 && Q2_1>=1 && free_15>=1 ], cost: INF
    128: f281 -> [51] : Y'=1, C1'=S2, D1'=T2, E1'=12, F1'=V2, G1'=1, H1'=X2, Q1'=Y2, J1'=1, U1'=S2, V1'=T2, W1'=12, X1'=V2, Y1'=1, Z1'=X2, A2'=Y2, B2'=1, S2'=free_19, U2'=11, W2'=1, [ S2>=1 ], cost: 4
    129: f281 -> [51] : [], cost: 0
     69: f347 -> f53 : A'=11, F'=free_21, A3'=free_22, [ 0>=free_22 && 0>=K && 0>=K1 ], cost: 1
     70: f347 -> f53 : A'=11, F'=free_23, K'=1, A3'=free_24, B3'=F, C3'=G, D3'=A, E3'=B, F3'=H, G3'=Q, H3'=J, [ free_24>=1 && 0>=K && 0>=K1 ], cost: 1
      6: [49] -> f53 : A'=11, F'=free_8, [ 0>=Q ], cost: 1
    110: [50] -> f249 : Y'=0, K1'=0, B2'=0, R2'=0, [ 0>=Y1 && 0>=0 ], cost: 2
    125: [50] -> f206 : Y'=1, M1'=free_15, N1'=N2, O1'=13, P1'=L2, Q1_1'=0, R1'=M2, S1'=P2, B2'=1, K2'=13, O2'=free_15, Q2_1'=0, [ Y1>=1 && 1>=1 && 0>=free_15 ], cost: 3
    101: [51] -> f347 : Y'=0, K1'=0, M1'=S2, N1'=T2, O1'=13, P1'=V2, Q1_1'=0, R1'=X2, S1'=Y2, T1'=0, U2'=13, W2'=0, Z2'=0, [ 0>=S2 && 0>=0 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f3
    130: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 ], cost: INF
    131: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_4, H'=0, Q'=-1+free_2, J'=free_3, K'=0, L'=1, M'=free_7, N'=free, O'=free_4, P'=7, Q_1'=0, R'=0, S'=-1+free_2, T'=free_3, [ 0>=free_2 && free_4>=1 && 0>=0 && free_7>=1 && 0>=-1+free_2 ], cost: 4
    132: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 ], cost: INF
    133: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_5, H'=0, Q'=-2+free_2, J'=free_3, K'=0, L'=1, M'=free_7, N'=free, O'=free_5, P'=8, Q_1'=0, R'=0, S'=-2+free_2, T'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && free_7>=1 && 0>=-2+free_2 ], cost: 4
    134: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 ], cost: 2
     12: f53 -> f89 : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 ], cost: 1
     36: f53 -> f206 : A'=13, H'=0, M1'=F, N1'=G, O1'=13, P1'=B, Q1_1'=0, R1'=Q, S1'=J, K2'=13, L2'=B, M2'=Q, N2'=G, O2'=F, P2'=J, Q2_1'=0, [ 0>=F ], cost: 1
    135: f89 -> f89 : U'=12, Y'=1, Z'=free_11, A1'=1, C1'=free_11, D1'=X, E1'=12, F1'=V, G1'=1, H1'=W, Q1'=B1, J1'=1, U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, B2'=1, [ G1>=1 && 1>=1 && A1>=1 && 1>=1 && free_11>=1 ], cost: 5
     99: f89 -> f149 : Y'=0, J1'=0, K1'=0, L1'=0, [ 0>=G1 && 0>=0 ], cost: 2
    123: f89 -> f149 : Y'=0, J1'=1, K1'=0, L1'=0, U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, B2'=0, [ G1>=1 && 1>=1 && 0>=A1 && 0>=0 ], cost: 4
    136: f89 -> f149 : U'=13, Y'=0, Z'=free_11, A1'=0, J1'=1, K1'=0, L1'=0, M1'=free_11, N1'=X, O1'=13, P1'=V, Q1_1'=0, R1'=W, S1'=B1, T1'=0, U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, B2'=1, [ G1>=1 && 1>=1 && A1>=1 && 1>=1 && 0>=free_11 && 0>=0 ], cost: 6
     49: f149 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
     50: f249 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
    108: f206 -> f249 : Y'=0, K1'=0, T1'=0, R2'=0, [ 0>=Q1_1 && 0>=0 ], cost: 2
    139: f206 -> [52] : Y'=1, T1'=1, U1'=O2, V1'=N2, W1'=K2, X1'=L2, Y1'=Q2_1, Z1'=M2, A2'=P2, [ Q1_1>=1 && 1>=1 && Q2_1>=1 && free_15>=1 ], cost: INF
    140: f206 -> [53] : Y'=1, T1'=1, U1'=O2, V1'=N2, W1'=K2, X1'=L2, Y1'=Q2_1, Z1'=M2, A2'=P2, [ Q1_1>=1 && 1>=1 && Q2_1>=1 && free_15>=1 ], cost: INF
    137: f281 -> f347 : Y'=0, C1'=S2, D1'=T2, E1'=12, F1'=V2, G1'=1, H1'=X2, Q1'=Y2, J1'=1, K1'=0, M1'=free_19, N1'=T2, O1'=13, P1'=V2, Q1_1'=0, R1'=X2, S1'=Y2, T1'=0, U1'=S2, V1'=T2, W1'=12, X1'=V2, Y1'=1, Z1'=X2, A2'=Y2, B2'=1, S2'=free_19, U2'=13, W2'=0, Z2'=0, [ S2>=1 && 0>=free_19 && 0>=0 ], cost: 6
    138: f281 -> f347 : Y'=0, K1'=0, M1'=S2, N1'=T2, O1'=13, P1'=V2, Q1_1'=0, R1'=X2, S1'=Y2, T1'=0, U2'=13, W2'=0, Z2'=0, [ 0>=S2 && 0>=0 ], cost: 2
     69: f347 -> f53 : A'=11, F'=free_21, A3'=free_22, [ 0>=free_22 && 0>=K && 0>=K1 ], cost: 1
     70: f347 -> f53 : A'=11, F'=free_23, K'=1, A3'=free_24, B3'=F, C3'=G, D3'=A, E3'=B, F3'=H, G3'=Q, H3'=J, [ free_24>=1 && 0>=K && 0>=K1 ], cost: 1

Eliminating 1 self-loops for location f89
  Self-Loop 135 has unbounded runtime, resulting in the new transition 141.
  Removing the self-loops: 135.

Removed all Self-loops using metering functions (where possible):
  Start location: f3
    130: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 ], cost: INF
    131: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_4, H'=0, Q'=-1+free_2, J'=free_3, K'=0, L'=1, M'=free_7, N'=free, O'=free_4, P'=7, Q_1'=0, R'=0, S'=-1+free_2, T'=free_3, [ 0>=free_2 && free_4>=1 && 0>=0 && free_7>=1 && 0>=-1+free_2 ], cost: 4
    132: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 ], cost: INF
    133: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_5, H'=0, Q'=-2+free_2, J'=free_3, K'=0, L'=1, M'=free_7, N'=free, O'=free_5, P'=8, Q_1'=0, R'=0, S'=-2+free_2, T'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && free_7>=1 && 0>=-2+free_2 ], cost: 4
    134: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 ], cost: 2
     12: f53 -> f89 : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 ], cost: 1
     36: f53 -> f206 : A'=13, H'=0, M1'=F, N1'=G, O1'=13, P1'=B, Q1_1'=0, R1'=Q, S1'=J, K2'=13, L2'=B, M2'=Q, N2'=G, O2'=F, P2'=J, Q2_1'=0, [ 0>=F ], cost: 1
    141: f89 -> [54] : [ G1>=1 && A1>=1 && free_11>=1 ], cost: INF
     49: f149 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
     50: f249 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
    108: f206 -> f249 : Y'=0, K1'=0, T1'=0, R2'=0, [ 0>=Q1_1 && 0>=0 ], cost: 2
    139: f206 -> [52] : Y'=1, T1'=1, U1'=O2, V1'=N2, W1'=K2, X1'=L2, Y1'=Q2_1, Z1'=M2, A2'=P2, [ Q1_1>=1 && 1>=1 && Q2_1>=1 && free_15>=1 ], cost: INF
    140: f206 -> [53] : Y'=1, T1'=1, U1'=O2, V1'=N2, W1'=K2, X1'=L2, Y1'=Q2_1, Z1'=M2, A2'=P2, [ Q1_1>=1 && 1>=1 && Q2_1>=1 && free_15>=1 ], cost: INF
    137: f281 -> f347 : Y'=0, C1'=S2, D1'=T2, E1'=12, F1'=V2, G1'=1, H1'=X2, Q1'=Y2, J1'=1, K1'=0, M1'=free_19, N1'=T2, O1'=13, P1'=V2, Q1_1'=0, R1'=X2, S1'=Y2, T1'=0, U1'=S2, V1'=T2, W1'=12, X1'=V2, Y1'=1, Z1'=X2, A2'=Y2, B2'=1, S2'=free_19, U2'=13, W2'=0, Z2'=0, [ S2>=1 && 0>=free_19 && 0>=0 ], cost: 6
    138: f281 -> f347 : Y'=0, K1'=0, M1'=S2, N1'=T2, O1'=13, P1'=V2, Q1_1'=0, R1'=X2, S1'=Y2, T1'=0, U2'=13, W2'=0, Z2'=0, [ 0>=S2 && 0>=0 ], cost: 2
     69: f347 -> f53 : A'=11, F'=free_21, A3'=free_22, [ 0>=free_22 && 0>=K && 0>=K1 ], cost: 1
     70: f347 -> f53 : A'=11, F'=free_23, K'=1, A3'=free_24, B3'=F, C3'=G, D3'=A, E3'=B, F3'=H, G3'=Q, H3'=J, [ free_24>=1 && 0>=K && 0>=K1 ], cost: 1
     99: [54] -> f149 : Y'=0, J1'=0, K1'=0, L1'=0, [ 0>=G1 && 0>=0 ], cost: 2
    123: [54] -> f149 : Y'=0, J1'=1, K1'=0, L1'=0, U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, B2'=0, [ G1>=1 && 1>=1 && 0>=A1 && 0>=0 ], cost: 4
    136: [54] -> f149 : U'=13, Y'=0, Z'=free_11, A1'=0, J1'=1, K1'=0, L1'=0, M1'=free_11, N1'=X, O1'=13, P1'=V, Q1_1'=0, R1'=W, S1'=B1, T1'=0, U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, B2'=1, [ G1>=1 && 1>=1 && A1>=1 && 1>=1 && 0>=free_11 && 0>=0 ], cost: 6


Applied simple chaining:
  Start location: f3
    130: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 ], cost: INF
    131: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_4, H'=0, Q'=-1+free_2, J'=free_3, K'=0, L'=1, M'=free_7, N'=free, O'=free_4, P'=7, Q_1'=0, R'=0, S'=-1+free_2, T'=free_3, [ 0>=free_2 && free_4>=1 && 0>=0 && free_7>=1 && 0>=-1+free_2 ], cost: 4
    132: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 ], cost: INF
    133: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_5, H'=0, Q'=-2+free_2, J'=free_3, K'=0, L'=1, M'=free_7, N'=free, O'=free_5, P'=8, Q_1'=0, R'=0, S'=-2+free_2, T'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && free_7>=1 && 0>=-2+free_2 ], cost: 4
    134: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 ], cost: 2
     36: f53 -> f206 : A'=13, H'=0, M1'=F, N1'=G, O1'=13, P1'=B, Q1_1'=0, R1'=Q, S1'=J, K2'=13, L2'=B, M2'=Q, N2'=G, O2'=F, P2'=J, Q2_1'=0, [ 0>=F ], cost: 1
     12: f53 -> [54] : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
     49: f149 -> f281 : S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=K1 ], cost: 1
    108: f206 -> f281 : Y'=0, K1'=0, T1'=0, R2'=0, S2'=F, T2'=G, U2'=A, V2'=B, W2'=H, X2'=Q, Y2'=J, [ 0>=Q1_1 && 0>=0 && 0>=0 ], cost: 3
    139: f206 -> [52] : Y'=1, T1'=1, U1'=O2, V1'=N2, W1'=K2, X1'=L2, Y1'=Q2_1, Z1'=M2, A2'=P2, [ Q1_1>=1 && 1>=1 && Q2_1>=1 && free_15>=1 ], cost: INF
    140: f206 -> [53] : Y'=1, T1'=1, U1'=O2, V1'=N2, W1'=K2, X1'=L2, Y1'=Q2_1, Z1'=M2, A2'=P2, [ Q1_1>=1 && 1>=1 && Q2_1>=1 && free_15>=1 ], cost: INF
    137: f281 -> f347 : Y'=0, C1'=S2, D1'=T2, E1'=12, F1'=V2, G1'=1, H1'=X2, Q1'=Y2, J1'=1, K1'=0, M1'=free_19, N1'=T2, O1'=13, P1'=V2, Q1_1'=0, R1'=X2, S1'=Y2, T1'=0, U1'=S2, V1'=T2, W1'=12, X1'=V2, Y1'=1, Z1'=X2, A2'=Y2, B2'=1, S2'=free_19, U2'=13, W2'=0, Z2'=0, [ S2>=1 && 0>=free_19 && 0>=0 ], cost: 6
    138: f281 -> f347 : Y'=0, K1'=0, M1'=S2, N1'=T2, O1'=13, P1'=V2, Q1_1'=0, R1'=X2, S1'=Y2, T1'=0, U2'=13, W2'=0, Z2'=0, [ 0>=S2 && 0>=0 ], cost: 2
     69: f347 -> f53 : A'=11, F'=free_21, A3'=free_22, [ 0>=free_22 && 0>=K && 0>=K1 ], cost: 1
     70: f347 -> f53 : A'=11, F'=free_23, K'=1, A3'=free_24, B3'=F, C3'=G, D3'=A, E3'=B, F3'=H, G3'=Q, H3'=J, [ free_24>=1 && 0>=K && 0>=K1 ], cost: 1
     99: [54] -> f149 : Y'=0, J1'=0, K1'=0, L1'=0, [ 0>=G1 && 0>=0 ], cost: 2
    123: [54] -> f149 : Y'=0, J1'=1, K1'=0, L1'=0, U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, B2'=0, [ G1>=1 && 1>=1 && 0>=A1 && 0>=0 ], cost: 4
    136: [54] -> f149 : U'=13, Y'=0, Z'=free_11, A1'=0, J1'=1, K1'=0, L1'=0, M1'=free_11, N1'=X, O1'=13, P1'=V, Q1_1'=0, R1'=W, S1'=B1, T1'=0, U1'=Z, V1'=X, W1'=U, X1'=V, Y1'=A1, Z1'=W, A2'=B1, B2'=1, [ G1>=1 && 1>=1 && A1>=1 && 1>=1 && 0>=free_11 && 0>=0 ], cost: 6


Applied chaining over branches and pruning:
  Start location: f3
    130: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 ], cost: INF
    131: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_4, H'=0, Q'=-1+free_2, J'=free_3, K'=0, L'=1, M'=free_7, N'=free, O'=free_4, P'=7, Q_1'=0, R'=0, S'=-1+free_2, T'=free_3, [ 0>=free_2 && free_4>=1 && 0>=0 && free_7>=1 && 0>=-1+free_2 ], cost: 4
    132: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 ], cost: INF
    133: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_5, H'=0, Q'=-2+free_2, J'=free_3, K'=0, L'=1, M'=free_7, N'=free, O'=free_5, P'=8, Q_1'=0, R'=0, S'=-2+free_2, T'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && free_7>=1 && 0>=-2+free_2 ], cost: 4
    134: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 ], cost: 2
    142: f53 -> f281 : A'=13, H'=0, Y'=0, K1'=0, M1'=F, N1'=G, O1'=13, P1'=B, Q1_1'=0, R1'=Q, S1'=J, T1'=0, K2'=13, L2'=B, M2'=Q, N2'=G, O2'=F, P2'=J, Q2_1'=0, R2'=0, S2'=F, T2'=G, U2'=13, V2'=B, W2'=0, X2'=Q, Y2'=J, [ 0>=F && 0>=0 && 0>=0 && 0>=0 ], cost: 4
    143: f53 -> [55] : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    144: f53 -> [56] : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    145: f53 -> [57] : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    146: f281 -> f53 : A'=11, F'=free_21, Y'=0, C1'=S2, D1'=T2, E1'=12, F1'=V2, G1'=1, H1'=X2, Q1'=Y2, J1'=1, K1'=0, M1'=free_19, N1'=T2, O1'=13, P1'=V2, Q1_1'=0, R1'=X2, S1'=Y2, T1'=0, U1'=S2, V1'=T2, W1'=12, X1'=V2, Y1'=1, Z1'=X2, A2'=Y2, B2'=1, S2'=free_19, U2'=13, W2'=0, Z2'=0, A3'=free_22, [ S2>=1 && 0>=free_19 && 0>=0 && 0>=free_22 && 0>=K && 0>=0 ], cost: 7
    147: f281 -> f53 : A'=11, F'=free_23, K'=1, Y'=0, C1'=S2, D1'=T2, E1'=12, F1'=V2, G1'=1, H1'=X2, Q1'=Y2, J1'=1, K1'=0, M1'=free_19, N1'=T2, O1'=13, P1'=V2, Q1_1'=0, R1'=X2, S1'=Y2, T1'=0, U1'=S2, V1'=T2, W1'=12, X1'=V2, Y1'=1, Z1'=X2, A2'=Y2, B2'=1, S2'=free_19, U2'=13, W2'=0, Z2'=0, A3'=free_24, B3'=F, C3'=G, D3'=A, E3'=B, F3'=H, G3'=Q, H3'=J, [ S2>=1 && 0>=free_19 && 0>=0 && free_24>=1 && 0>=K && 0>=0 ], cost: 7
    148: f281 -> f53 : A'=11, F'=free_21, Y'=0, K1'=0, M1'=S2, N1'=T2, O1'=13, P1'=V2, Q1_1'=0, R1'=X2, S1'=Y2, T1'=0, U2'=13, W2'=0, Z2'=0, A3'=free_22, [ 0>=S2 && 0>=0 && 0>=free_22 && 0>=K && 0>=0 ], cost: 3
    149: f281 -> f53 : A'=11, F'=free_23, K'=1, Y'=0, K1'=0, M1'=S2, N1'=T2, O1'=13, P1'=V2, Q1_1'=0, R1'=X2, S1'=Y2, T1'=0, U2'=13, W2'=0, Z2'=0, A3'=free_24, B3'=F, C3'=G, D3'=A, E3'=B, F3'=H, G3'=Q, H3'=J, [ 0>=S2 && 0>=0 && free_24>=1 && 0>=K && 0>=0 ], cost: 3


Applied chaining over branches and pruning:
  Start location: f3
    130: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 ], cost: INF
    131: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_4, H'=0, Q'=-1+free_2, J'=free_3, K'=0, L'=1, M'=free_7, N'=free, O'=free_4, P'=7, Q_1'=0, R'=0, S'=-1+free_2, T'=free_3, [ 0>=free_2 && free_4>=1 && 0>=0 && free_7>=1 && 0>=-1+free_2 ], cost: 4
    132: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 ], cost: INF
    133: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_5, H'=0, Q'=-2+free_2, J'=free_3, K'=0, L'=1, M'=free_7, N'=free, O'=free_5, P'=8, Q_1'=0, R'=0, S'=-2+free_2, T'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && free_7>=1 && 0>=-2+free_2 ], cost: 4
    134: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 ], cost: 2
    150: f53 -> f53 : A'=11, F'=free_21, H'=0, Y'=0, K1'=0, M1'=F, N1'=G, O1'=13, P1'=B, Q1_1'=0, R1'=Q, S1'=J, T1'=0, K2'=13, L2'=B, M2'=Q, N2'=G, O2'=F, P2'=J, Q2_1'=0, R2'=0, S2'=F, T2'=G, U2'=13, V2'=B, W2'=0, X2'=Q, Y2'=J, Z2'=0, A3'=free_22, [ 0>=F && 0>=0 && 0>=0 && 0>=0 && 0>=F && 0>=0 && 0>=free_22 && 0>=K && 0>=0 ], cost: 7
    151: f53 -> f53 : A'=11, F'=free_23, H'=0, K'=1, Y'=0, K1'=0, M1'=F, N1'=G, O1'=13, P1'=B, Q1_1'=0, R1'=Q, S1'=J, T1'=0, K2'=13, L2'=B, M2'=Q, N2'=G, O2'=F, P2'=J, Q2_1'=0, R2'=0, S2'=F, T2'=G, U2'=13, V2'=B, W2'=0, X2'=Q, Y2'=J, Z2'=0, A3'=free_24, B3'=F, C3'=G, D3'=13, E3'=B, F3'=0, G3'=Q, H3'=J, [ 0>=F && 0>=0 && 0>=0 && 0>=0 && 0>=F && 0>=0 && free_24>=1 && 0>=K && 0>=0 ], cost: 7
    143: f53 -> [55] : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    144: f53 -> [56] : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    145: f53 -> [57] : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF

Eliminating 2 self-loops for location f53
  Removing the self-loops: 150 151.
Adding an epsilon transition (to model nonexecution of the loops): 154.

Removed all Self-loops using metering functions (where possible):
  Start location: f3
    130: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 ], cost: INF
    131: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_4, H'=0, Q'=-1+free_2, J'=free_3, K'=0, L'=1, M'=free_7, N'=free, O'=free_4, P'=7, Q_1'=0, R'=0, S'=-1+free_2, T'=free_3, [ 0>=free_2 && free_4>=1 && 0>=0 && free_7>=1 && 0>=-1+free_2 ], cost: 4
    132: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 ], cost: INF
    133: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_5, H'=0, Q'=-2+free_2, J'=free_3, K'=0, L'=1, M'=free_7, N'=free, O'=free_5, P'=8, Q_1'=0, R'=0, S'=-2+free_2, T'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && free_7>=1 && 0>=-2+free_2 ], cost: 4
    134: f3 -> f53 : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 ], cost: 2
    152: f53 -> [58] : A'=11, F'=free_21, H'=0, Y'=0, K1'=0, M1'=F, N1'=G, O1'=13, P1'=B, Q1_1'=0, R1'=Q, S1'=J, T1'=0, K2'=13, L2'=B, M2'=Q, N2'=G, O2'=F, P2'=J, Q2_1'=0, R2'=0, S2'=F, T2'=G, U2'=13, V2'=B, W2'=0, X2'=Q, Y2'=J, Z2'=0, A3'=free_22, [ 0>=F && 0>=free_22 && 0>=K ], cost: 7
    153: f53 -> [58] : A'=11, F'=free_23, H'=0, K'=1, Y'=0, K1'=0, M1'=F, N1'=G, O1'=13, P1'=B, Q1_1'=0, R1'=Q, S1'=J, T1'=0, K2'=13, L2'=B, M2'=Q, N2'=G, O2'=F, P2'=J, Q2_1'=0, R2'=0, S2'=F, T2'=G, U2'=13, V2'=B, W2'=0, X2'=Q, Y2'=J, Z2'=0, A3'=free_24, B3'=F, C3'=G, D3'=13, E3'=B, F3'=0, G3'=Q, H3'=J, [ 0>=F && free_24>=1 && 0>=K ], cost: 7
    154: f53 -> [58] : [], cost: 0
    143: [58] -> [55] : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    144: [58] -> [56] : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    145: [58] -> [57] : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f3
    155: f3 -> [58] : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_21, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, Y'=0, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_22, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && 0>=free_22 && 0>=0 ], cost: INF
    156: f3 -> [58] : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_23, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=1, L'=0, Y'=0, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_24, B3'=free_8, C3'=free_1, D3'=13, E3'=0, F3'=0, G3'=free_2, H3'=free_3, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && free_24>=1 && 0>=0 ], cost: INF
    161: f3 -> [58] : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_21, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, Y'=0, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_22, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && 0>=free_22 && 0>=0 ], cost: INF
    162: f3 -> [58] : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_23, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=1, L'=0, Y'=0, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_24, B3'=free_8, C3'=free_1, D3'=13, E3'=0, F3'=0, G3'=free_2, H3'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && free_24>=1 && 0>=0 ], cost: INF
    163: f3 -> [58] : A'=11, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=0, Q'=free_2, J'=free_3, K'=0, L'=0, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 ], cost: INF
    143: [58] -> [55] : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    144: [58] -> [56] : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    145: [58] -> [57] : A'=12, H'=1, U'=12, V'=B, W'=Q, X'=G, Z'=F, A1'=1, B1'=J, C1'=F, D1'=G, E1'=12, F1'=B, G1'=1, H1'=Q, Q1'=J, [ F>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f3
    170: f3 -> [55] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_21, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=0, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_21, A1'=1, B1'=free_3, C1'=free_21, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_22, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && 0>=free_22 && 0>=0 && free_21>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    173: f3 -> [55] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_23, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=1, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_23, A1'=1, B1'=free_3, C1'=free_23, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_24, B3'=free_8, C3'=free_1, D3'=13, E3'=0, F3'=0, G3'=free_2, H3'=free_3, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && free_24>=1 && 0>=0 && free_23>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    176: f3 -> [55] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_21, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=0, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_21, A1'=1, B1'=free_3, C1'=free_21, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_22, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && 0>=free_22 && 0>=0 && free_21>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    179: f3 -> [55] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_23, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=1, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_23, A1'=1, B1'=free_3, C1'=free_23, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_24, B3'=free_8, C3'=free_1, D3'=13, E3'=0, F3'=0, G3'=free_2, H3'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && free_24>=1 && 0>=0 && free_23>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    182: f3 -> [55] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=0, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Z'=free_8, A1'=1, B1'=free_3, C1'=free_8, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && free_8>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    171: f3 -> [56] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_21, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=0, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_21, A1'=1, B1'=free_3, C1'=free_21, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_22, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && 0>=free_22 && 0>=0 && free_21>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    174: f3 -> [56] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_23, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=1, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_23, A1'=1, B1'=free_3, C1'=free_23, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_24, B3'=free_8, C3'=free_1, D3'=13, E3'=0, F3'=0, G3'=free_2, H3'=free_3, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && free_24>=1 && 0>=0 && free_23>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    177: f3 -> [56] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_21, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=0, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_21, A1'=1, B1'=free_3, C1'=free_21, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_22, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && 0>=free_22 && 0>=0 && free_21>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    180: f3 -> [56] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_23, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=1, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_23, A1'=1, B1'=free_3, C1'=free_23, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_24, B3'=free_8, C3'=free_1, D3'=13, E3'=0, F3'=0, G3'=free_2, H3'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && free_24>=1 && 0>=0 && free_23>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    183: f3 -> [56] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=0, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Z'=free_8, A1'=1, B1'=free_3, C1'=free_8, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && free_8>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    172: f3 -> [57] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_21, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=0, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_21, A1'=1, B1'=free_3, C1'=free_21, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_22, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && 0>=free_22 && 0>=0 && free_21>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    175: f3 -> [57] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_23, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=1, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_23, A1'=1, B1'=free_3, C1'=free_23, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_24, B3'=free_8, C3'=free_1, D3'=13, E3'=0, F3'=0, G3'=free_2, H3'=free_3, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && free_24>=1 && 0>=0 && free_23>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    178: f3 -> [57] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_21, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=0, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_21, A1'=1, B1'=free_3, C1'=free_21, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_22, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && 0>=free_22 && 0>=0 && free_21>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    181: f3 -> [57] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_23, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=1, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_23, A1'=1, B1'=free_3, C1'=free_23, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_24, B3'=free_8, C3'=free_1, D3'=13, E3'=0, F3'=0, G3'=free_2, H3'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && free_24>=1 && 0>=0 && free_23>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    184: f3 -> [57] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=0, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Z'=free_8, A1'=1, B1'=free_3, C1'=free_8, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && free_8>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f3
    170: f3 -> [55] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_21, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=0, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_21, A1'=1, B1'=free_3, C1'=free_21, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_22, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && 0>=free_22 && 0>=0 && free_21>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    173: f3 -> [55] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_23, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=1, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_23, A1'=1, B1'=free_3, C1'=free_23, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_24, B3'=free_8, C3'=free_1, D3'=13, E3'=0, F3'=0, G3'=free_2, H3'=free_3, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && free_24>=1 && 0>=0 && free_23>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    176: f3 -> [55] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_21, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=0, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_21, A1'=1, B1'=free_3, C1'=free_21, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_22, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && 0>=free_22 && 0>=0 && free_21>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    179: f3 -> [55] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_23, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=1, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_23, A1'=1, B1'=free_3, C1'=free_23, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_24, B3'=free_8, C3'=free_1, D3'=13, E3'=0, F3'=0, G3'=free_2, H3'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && free_24>=1 && 0>=0 && free_23>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    182: f3 -> [55] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=0, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Z'=free_8, A1'=1, B1'=free_3, C1'=free_8, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && free_8>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    171: f3 -> [56] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_21, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=0, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_21, A1'=1, B1'=free_3, C1'=free_21, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_22, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && 0>=free_22 && 0>=0 && free_21>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    174: f3 -> [56] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_23, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=1, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_23, A1'=1, B1'=free_3, C1'=free_23, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_24, B3'=free_8, C3'=free_1, D3'=13, E3'=0, F3'=0, G3'=free_2, H3'=free_3, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && free_24>=1 && 0>=0 && free_23>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    177: f3 -> [56] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_21, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=0, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_21, A1'=1, B1'=free_3, C1'=free_21, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_22, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && 0>=free_22 && 0>=0 && free_21>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    180: f3 -> [56] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_23, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=1, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_23, A1'=1, B1'=free_3, C1'=free_23, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_24, B3'=free_8, C3'=free_1, D3'=13, E3'=0, F3'=0, G3'=free_2, H3'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && free_24>=1 && 0>=0 && free_23>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    183: f3 -> [56] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=0, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Z'=free_8, A1'=1, B1'=free_3, C1'=free_8, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && free_8>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    172: f3 -> [57] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_21, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=0, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_21, A1'=1, B1'=free_3, C1'=free_21, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_22, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && 0>=free_22 && 0>=0 && free_21>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    175: f3 -> [57] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_23, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=1, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_23, A1'=1, B1'=free_3, C1'=free_23, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_24, B3'=free_8, C3'=free_1, D3'=13, E3'=0, F3'=0, G3'=free_2, H3'=free_3, [ 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && free_24>=1 && 0>=0 && free_23>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    178: f3 -> [57] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_21, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=0, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_21, A1'=1, B1'=free_3, C1'=free_21, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_22, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && 0>=free_22 && 0>=0 && free_21>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    181: f3 -> [57] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_23, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=1, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Y'=0, Z'=free_23, A1'=1, B1'=free_3, C1'=free_23, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, K1'=0, M1'=free_8, N1'=free_1, O1'=13, P1'=0, Q1_1'=0, R1'=free_2, S1'=free_3, T1'=0, K2'=13, L2'=0, M2'=free_2, N2'=free_1, O2'=free_8, P2'=free_3, Q2_1'=0, R2'=0, S2'=free_8, T2'=free_1, U2'=13, V2'=0, W2'=0, X2'=free_2, Y2'=free_3, Z2'=0, A3'=free_24, B3'=free_8, C3'=free_1, D3'=13, E3'=0, F3'=0, G3'=free_2, H3'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && free_24>=1 && 0>=0 && free_23>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF
    184: f3 -> [57] : A'=12, B'=0, C'=0, D'=0, E'=0, F'=free_8, G'=free_1, H'=1, Q'=free_2, J'=free_3, K'=0, L'=0, U'=12, V'=0, W'=free_2, X'=free_1, Z'=free_8, A1'=1, B1'=free_3, C1'=free_8, D1'=free_1, E1'=12, F1'=0, G1'=1, H1'=free_2, Q1'=free_3, [ 0>=free_2 && 0>=free_5 && 0>=0 && 0>=free_6 && 0>=free_2 && free_8>=1 && 1>=1 && 1>=1 && free_11>=1 ], cost: INF


Computing complexity for remaining 15 transitions.

Found new complexity INF, because: INF sat.


The final runtime is determined by this resulting transition:
  Final Guard: 0>=free_2 && free_4>=1 && 0>=0 && 0>=free_6 && 0>=free_2 && 0>=free_8 && 0>=free_22 && 0>=0 && free_21>=1 && 1>=1 && 1>=1 && free_11>=1
  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,?)