Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f3
      0: f13 -> f14 : A'=0, [], cost: 1
      5: f14 -> f35 : A'=2, H'=1+H, M'=E, N'=F, O'=2, P'=G, Q_1'=2+H, R'=Q, S'=J, T'=K, U'=0, V'=0, W'=0, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, [ J>=1 ], cost: 1
     57: f14 -> f304 : A'=4, [ 0>=J ], cost: 1
      1: f167 -> f168 : B'=0, [], cost: 1
     32: f168 -> f176 : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F3'=1+F3, [ H3>=1 ], cost: 1
     42: f168 -> f222 : B'=4, [ 0>=H3 ], cost: 1
      2: f459 -> f460 : B'=0, [], cost: 1
     89: f460 -> f468 : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F3'=1+F3, [ H3>=1 ], cost: 1
     99: f460 -> f514 : B'=4, [ 0>=H3 ], cost: 1
      3: f3 -> f14 : A'=0, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=0, Q'=free_4, J'=free, K'=free_2, [], cost: 1
      4: f155 -> f35 : A'=2, H'=1+H, M'=E, N'=F, O'=2, P'=G, Q_1'=2+H, R'=Q, S'=J, T'=K, U'=0, V'=0, W'=0, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, [ L>=1 ], cost: 1
    116: f155 -> f666666 : E6'=0, F6'=0, [ 0>=L ], cost: 1
      7: f35 -> f42 : F1'=1, G1'=1, [ B1>=1 ], cost: 1
      8: f35 -> f42 : F1'=0, G1'=0, [ 0>=B1 ], cost: 1
      6: f26 -> f35 : O'=2, Q_1'=1+Q_1, X'=M, Y'=N, Z'=2, A1'=P, B1'=1+Q_1, C1'=R, D1'=S, E1'=T, [ S>=1 ], cost: 1
     16: f26 -> f81 : O'=4, [ 0>=S ], cost: 1
      9: f42 -> f155 : L'=1, H1'=1, [ F1>=1 ], cost: 1
     10: f42 -> f155 : L'=0, H1'=0, [ W>=1 && 0>=F1 ], cost: 1
     11: f42 -> f35 : O'=2, Q_1'=1+Q_1, X'=M, Y'=N, Z'=2, A1'=P, B1'=1+Q_1, C1'=R, D1'=S, E1'=T, Q1'=free_6, [ 0>=F1 && 0>=free_6 && 0>=W ], cost: 1
     12: f42 -> f35 : O'=2, Q_1'=1+Q_1, W'=1, X'=M, Y'=N, Z'=2, A1'=P, B1'=1+Q_1, C1'=R, D1'=S, E1'=T, Q1'=free_7, J1'=M, K1'=N, L1'=O, M1'=P, N1'=Q_1, O1'=R, P1'=S, Q1_1'=T, [ 0>=F1 && free_7>=1 && 0>=W ], cost: 1
     13: f63 -> f73 : X'=M, Y'=N, Z'=O, A1'=P, B1'=Q_1, C1'=R, D1'=S, E1'=T, F1'=1, R1'=1, [ Q_1>=1 ], cost: 1
     14: f63 -> f73 : X'=M, Y'=N, Z'=O, A1'=P, B1'=Q_1, C1'=R, D1'=S, E1'=T, F1'=0, R1'=0, [ 0>=Q_1 ], cost: 1
     15: f73 -> f155 : L'=1, H1'=1, [ F1>=1 ], cost: 1
     22: f73 -> f122 : K2'=M, L2'=N, M2'=O, N2'=P, O2'=Q_1, P2'=R, Q2_1'=S, R2'=T, [ 0>=F1 ], cost: 1
     17: f81 -> f155 : L'=0, O'=6, R'=-1+R, H1'=0, [ 0>=R && V>=1 ], cost: 1
     18: f81 -> f81 : O'=4, R'=-1+R, S1'=free_8, [ 0>=V && 0>=R && 0>=free_8 ], cost: 1
     19: f81 -> f81 : O'=4, R'=-1+R, V'=1, S1'=free_9, T1'=M, U1'=N, V1'=6, W1'=P, X1'=Q_1, Y1'=-1+R, Z1'=S, A2'=T, [ 0>=V && 0>=R && free_9>=1 ], cost: 1
     20: f81 -> f114 : O'=7, Q_1'=1, F1'=1, B2'=M, C2'=N, D2'=7, E2'=P, F2'=1, G2'=R, H2'=S, Q2'=T, J2'=1, [ 0>=R ], cost: 1
     21: f114 -> f155 : L'=1, H1'=1, [ F1>=1 ], cost: 1
     23: f114 -> f122 : K2'=M, L2'=N, M2'=O, N2'=P, O2'=Q_1, P2'=R, Q2_1'=S, R2'=T, [ 0>=F1 ], cost: 1
     24: f122 -> f129 : F1'=1, S2'=1, [ O2>=1 ], cost: 1
     25: f122 -> f129 : F1'=0, S2'=0, [ 0>=O2 ], cost: 1
     26: f129 -> f155 : L'=1, H1'=1, [ F1>=1 ], cost: 1
     27: f129 -> f138 : O'=9, S'=1, [ 0>=F1 ], cost: 1
     28: f138 -> f155 : L'=0, H1'=0, [ U>=1 ], cost: 1
     29: f138 -> f138 : O'=9, S'=1, T2'=free_10, [ 0>=free_10 && 0>=U ], cost: 1
     30: f138 -> f138 : O'=9, S'=1, U'=1, T2'=free_11, U2'=M, V2'=N, W2'=O, X2'=P, Y2'=Q_1, Z2'=R, A3'=S, B3'=T, [ free_11>=1 && 0>=U ], cost: 1
     31: f160 -> f168 : B'=A, C3'=E, D3'=F, E3'=G, F3'=H, G3'=Q, H3'=J, Q3'=K, J3'=0, K3'=0, L3'=0, [], cost: 1
     33: f176 -> f183 : F1'=1, G1'=1, [ B1>=1 ], cost: 1
     34: f176 -> f183 : F1'=0, G1'=0, [ 0>=B1 ], cost: 1
     37: f183 -> f176 : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F3'=1+F3, N3'=free_12, [ 0>=L3 && 0>=free_12 && 0>=F1 ], cost: 1
     38: f183 -> f176 : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F3'=1+F3, L3'=1, N3'=free_13, O3'=C3, P3'=D3, Q3_1'=B, R3'=E3, S3'=F3, T3'=G3, U3'=H3, V3'=Q3, [ 0>=L3 && free_13>=1 && 0>=F1 ], cost: 1
     35: f183 -> f296 : L'=1, M3'=1, [ F1>=1 ], cost: 1
     36: f183 -> f296 : L'=0, M3'=0, [ 0>=F1 && L3>=1 ], cost: 1
     87: f296 -> f460 : B'=A, C3'=E, D3'=F, E3'=G, F3'=H, G3'=Q, H3'=J, Q3'=K, J3'=0, K3'=0, L3'=0, [ L>=1 ], cost: 1
    117: f296 -> f666666 : E6'=0, F6'=0, [ 0>=L ], cost: 1
     39: f204 -> f214 : F1'=1, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, W3'=1, [ F3>=1 ], cost: 1
     40: f204 -> f214 : F1'=0, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, W3'=0, [ 0>=F3 ], cost: 1
     41: f214 -> f296 : L'=1, M3'=1, [ F1>=1 ], cost: 1
     48: f214 -> f263 : K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, [ 0>=F1 ], cost: 1
     43: f222 -> f296 : B'=6, L'=0, G3'=-1+G3, M3'=0, [ 0>=G3 && K3>=1 ], cost: 1
     44: f222 -> f222 : B'=4, G3'=-1+G3, X3'=free_14, [ 0>=K3 && 0>=free_14 && 0>=G3 ], cost: 1
     45: f222 -> f222 : B'=4, G3'=-1+G3, K3'=1, X3'=free_15, Y3'=C3, Z3'=D3, A4'=6, B4'=E3, C4'=F3, D4'=-1+G3, E4'=H3, F4'=Q3, [ 0>=K3 && free_15>=1 && 0>=G3 ], cost: 1
     46: f222 -> f255 : B'=7, F1'=1, B2'=C3, C2'=D3, D2'=7, E2'=E3, F2'=1, G2'=G3, H2'=H3, Q2'=Q3, J2'=1, F3'=1, [ 0>=G3 ], cost: 1
     47: f255 -> f296 : L'=1, M3'=1, [ F1>=1 ], cost: 1
     49: f255 -> f263 : K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, [ 0>=F1 ], cost: 1
     50: f263 -> f270 : F1'=1, S2'=1, [ O2>=1 ], cost: 1
     51: f263 -> f270 : F1'=0, S2'=0, [ 0>=O2 ], cost: 1
     52: f270 -> f296 : L'=1, M3'=1, [ F1>=1 ], cost: 1
     53: f270 -> f279 : B'=9, H3'=1, [ 0>=F1 ], cost: 1
     54: f279 -> f296 : L'=0, M3'=0, [ J3>=1 ], cost: 1
     55: f279 -> f279 : B'=9, H3'=1, G4'=free_16, [ 0>=free_16 && 0>=J3 ], cost: 1
     56: f279 -> f279 : B'=9, H3'=1, J3'=1, G4'=free_17, H4'=C3, Q4'=D3, J4'=B, K4'=E3, L4'=F3, M4'=G3, N4'=H3, O4'=Q3, [ free_17>=1 && 0>=J3 ], cost: 1
     58: f304 -> f304 : A'=4, Q'=-1+Q, [ 0>=Q ], cost: 1
     73: f304 -> f399 : A'=7, H'=1, B2'=E, C2'=F, D2'=7, E2'=G, F2'=1, G2'=Q, H2'=J, Q2'=K, P4'=J, Q4_1'=E, R4'=F, S4'=G, T4'=1, U4'=Q, V4'=K, W4'=7, Y4'=0, J5'=0, T5'=0, [ 0>=Q ], cost: 1
     59: f318 -> f327 : X'=Q4_1, Y'=R4, Z'=2, A1'=S4, B1'=1+T4, C1'=U4, D1'=P4, E1'=V4, T4'=1+T4, W4'=2, [ P4>=1 ], cost: 1
     69: f318 -> f373 : W4'=4, [ 0>=P4 ], cost: 1
     60: f327 -> f334 : F1'=1, G1'=1, [ B1>=1 ], cost: 1
     61: f327 -> f334 : F1'=0, G1'=0, [ 0>=B1 ], cost: 1
     64: f334 -> f327 : X'=Q4_1, Y'=R4, Z'=2, A1'=S4, B1'=1+T4, C1'=U4, D1'=P4, E1'=V4, T4'=1+T4, W4'=2, Z4'=free_18, [ 0>=F1 && 0>=Y4 && 0>=free_18 ], cost: 1
     65: f334 -> f327 : X'=Q4_1, Y'=R4, Z'=2, A1'=S4, B1'=1+T4, C1'=U4, D1'=P4, E1'=V4, T4'=1+T4, W4'=2, Y4'=1, Z4'=free_19, A5'=Q4_1, B5'=R4, C5'=W4, D5'=S4, E5'=T4, F5'=U4, G5'=P4, H5'=V4, [ 0>=F1 && 0>=Y4 && free_19>=1 ], cost: 1
     62: f334 -> f447 : L'=1, X4'=1, [ F1>=1 ], cost: 1
     63: f334 -> f447 : L'=0, X4'=0, [ Y4>=1 && 0>=F1 ], cost: 1
     88: f447 -> f460 : B'=A, C3'=E, D3'=F, E3'=G, F3'=H, G3'=Q, H3'=J, Q3'=K, J3'=0, K3'=0, L3'=0, [ L>=1 ], cost: 1
    118: f447 -> f666666 : E6'=0, F6'=0, [ 0>=L ], cost: 1
     66: f355 -> f365 : F1'=1, B2'=Q4_1, C2'=R4, D2'=W4, E2'=S4, F2'=T4, G2'=U4, H2'=P4, Q2'=V4, Q5'=1, [ T4>=1 ], cost: 1
     67: f355 -> f365 : F1'=0, B2'=Q4_1, C2'=R4, D2'=W4, E2'=S4, F2'=T4, G2'=U4, H2'=P4, Q2'=V4, Q5'=0, [ 0>=T4 ], cost: 1
     68: f365 -> f447 : L'=1, X4'=1, [ F1>=1 ], cost: 1
     78: f365 -> f414 : K2'=Q4_1, L2'=R4, M2'=W4, N2'=S4, O2'=T4, P2'=U4, Q2_1'=P4, R2'=V4, [ 0>=F1 ], cost: 1
     70: f373 -> f447 : L'=0, U4'=-1+U4, W4'=6, X4'=0, [ 0>=U4 && J5>=1 ], cost: 1
     71: f373 -> f373 : U4'=-1+U4, W4'=4, K5'=free_20, [ 0>=free_20 && 0>=U4 && 0>=J5 ], cost: 1
     72: f373 -> f373 : U4'=-1+U4, W4'=4, J5'=1, K5'=free_21, L5'=Q4_1, M5'=R4, N5'=6, O5'=S4, P5'=T4, Q5_1'=-1+U4, R5'=P4, S5'=V4, [ free_21>=1 && 0>=U4 && 0>=J5 ], cost: 1
     74: f373 -> f399 : B2'=Q4_1, C2'=R4, D2'=7, E2'=S4, F2'=1, G2'=U4, H2'=P4, Q2'=V4, T4'=1, W4'=7, [ 0>=U4 ], cost: 1
     75: f399 -> f406 : F1'=1, J2'=1, [ F2>=1 ], cost: 1
     76: f399 -> f406 : F1'=0, J2'=0, [ 0>=F2 ], cost: 1
     77: f406 -> f447 : L'=1, X4'=1, [ F1>=1 ], cost: 1
     79: f406 -> f414 : K2'=Q4_1, L2'=R4, M2'=W4, N2'=S4, O2'=T4, P2'=U4, Q2_1'=P4, R2'=V4, [ 0>=F1 ], cost: 1
     80: f414 -> f421 : F1'=1, S2'=1, [ O2>=1 ], cost: 1
     81: f414 -> f421 : F1'=0, S2'=0, [ 0>=O2 ], cost: 1
     82: f421 -> f447 : L'=1, X4'=1, [ F1>=1 ], cost: 1
     83: f421 -> f430 : P4'=1, W4'=9, [ 0>=F1 ], cost: 1
     84: f430 -> f447 : L'=0, X4'=0, [ T5>=1 ], cost: 1
     85: f430 -> f430 : P4'=1, W4'=9, U5'=free_22, [ 0>=T5 && 0>=free_22 ], cost: 1
     86: f430 -> f430 : P4'=1, W4'=9, T5'=1, U5'=free_23, V5'=Q4_1, W5'=R4, X5'=W4, Y5'=S4, Z5'=T4, A6'=U4, B6'=P4, C6'=V4, [ 0>=T5 && free_23>=1 ], cost: 1
     90: f468 -> f475 : F1'=1, G1'=1, [ B1>=1 ], cost: 1
     91: f468 -> f475 : F1'=0, G1'=0, [ 0>=B1 ], cost: 1
     94: f475 -> f468 : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F3'=1+F3, N3'=free_24, [ 0>=L3 && 0>=free_24 && 0>=F1 ], cost: 1
     95: f475 -> f468 : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F3'=1+F3, L3'=1, N3'=free_25, O3'=C3, P3'=D3, Q3_1'=B, R3'=E3, S3'=F3, T3'=G3, U3'=H3, V3'=Q3, [ 0>=L3 && free_25>=1 && 0>=F1 ], cost: 1
     92: f475 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
     93: f475 -> f588 : L'=0, D6'=0, [ 0>=F1 && L3>=1 ], cost: 1
    115: f588 -> f596 : A'=9, [ L>=1 ], cost: 1
    119: f588 -> f666666 : E6'=0, F6'=0, [ 0>=L ], cost: 1
     96: f496 -> f506 : F1'=1, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, W3'=1, [ F3>=1 ], cost: 1
     97: f496 -> f506 : F1'=0, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, W3'=0, [ 0>=F3 ], cost: 1
     98: f506 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
    105: f506 -> f555 : K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, [ 0>=F1 ], cost: 1
    100: f514 -> f588 : B'=6, L'=0, G3'=-1+G3, D6'=0, [ 0>=G3 && K3>=1 ], cost: 1
    101: f514 -> f514 : B'=4, G3'=-1+G3, X3'=free_26, [ 0>=K3 && 0>=free_26 && 0>=G3 ], cost: 1
    102: f514 -> f514 : B'=4, G3'=-1+G3, K3'=1, X3'=free_27, Y3'=C3, Z3'=D3, A4'=6, B4'=E3, C4'=F3, D4'=-1+G3, E4'=H3, F4'=Q3, [ 0>=K3 && free_27>=1 && 0>=G3 ], cost: 1
    103: f514 -> f547 : B'=7, F1'=1, B2'=C3, C2'=D3, D2'=7, E2'=E3, F2'=1, G2'=G3, H2'=H3, Q2'=Q3, J2'=1, F3'=1, [ 0>=G3 ], cost: 1
    104: f547 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
    106: f547 -> f555 : K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, [ 0>=F1 ], cost: 1
    107: f555 -> f562 : F1'=1, S2'=1, [ O2>=1 ], cost: 1
    108: f555 -> f562 : F1'=0, S2'=0, [ 0>=O2 ], cost: 1
    109: f562 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
    110: f562 -> f571 : B'=9, H3'=1, [ 0>=F1 ], cost: 1
    111: f571 -> f588 : L'=0, D6'=0, [ J3>=1 ], cost: 1
    112: f571 -> f571 : B'=9, H3'=1, G4'=free_28, [ 0>=free_28 && 0>=J3 ], cost: 1
    113: f571 -> f571 : B'=9, H3'=1, J3'=1, G4'=free_29, H4'=C3, Q4'=D3, J4'=B, K4'=E3, L4'=F3, M4'=G3, N4'=H3, O4'=Q3, [ free_29>=1 && 0>=J3 ], cost: 1
    114: f596 -> f596 : A'=9, J'=1, [], cost: 1


Simplified the transitions:
  Start location: f3
      5: f14 -> f35 : A'=2, H'=1+H, M'=E, N'=F, O'=2, P'=G, Q_1'=2+H, R'=Q, S'=J, T'=K, U'=0, V'=0, W'=0, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, [ J>=1 ], cost: 1
     57: f14 -> f304 : A'=4, [ 0>=J ], cost: 1
     89: f460 -> f468 : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F3'=1+F3, [ H3>=1 ], cost: 1
     99: f460 -> f514 : B'=4, [ 0>=H3 ], cost: 1
      3: f3 -> f14 : A'=0, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=0, Q'=free_4, J'=free, K'=free_2, [], cost: 1
      4: f155 -> f35 : A'=2, H'=1+H, M'=E, N'=F, O'=2, P'=G, Q_1'=2+H, R'=Q, S'=J, T'=K, U'=0, V'=0, W'=0, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, [ L>=1 ], cost: 1
      7: f35 -> f42 : F1'=1, G1'=1, [ B1>=1 ], cost: 1
      8: f35 -> f42 : F1'=0, G1'=0, [ 0>=B1 ], cost: 1
      9: f42 -> f155 : L'=1, H1'=1, [ F1>=1 ], cost: 1
     10: f42 -> f155 : L'=0, H1'=0, [ W>=1 && 0>=F1 ], cost: 1
     11: f42 -> f35 : O'=2, Q_1'=1+Q_1, X'=M, Y'=N, Z'=2, A1'=P, B1'=1+Q_1, C1'=R, D1'=S, E1'=T, Q1'=free_6, [ 0>=F1 && 0>=free_6 && 0>=W ], cost: 1
     12: f42 -> f35 : O'=2, Q_1'=1+Q_1, W'=1, X'=M, Y'=N, Z'=2, A1'=P, B1'=1+Q_1, C1'=R, D1'=S, E1'=T, Q1'=free_7, J1'=M, K1'=N, L1'=O, M1'=P, N1'=Q_1, O1'=R, P1'=S, Q1_1'=T, [ 0>=F1 && free_7>=1 && 0>=W ], cost: 1
     58: f304 -> f304 : A'=4, Q'=-1+Q, [ 0>=Q ], cost: 1
     73: f304 -> f399 : A'=7, H'=1, B2'=E, C2'=F, D2'=7, E2'=G, F2'=1, G2'=Q, H2'=J, Q2'=K, P4'=J, Q4_1'=E, R4'=F, S4'=G, T4'=1, U4'=Q, V4'=K, W4'=7, Y4'=0, J5'=0, T5'=0, [ 0>=Q ], cost: 1
     88: f447 -> f460 : B'=A, C3'=E, D3'=F, E3'=G, F3'=H, G3'=Q, H3'=J, Q3'=K, J3'=0, K3'=0, L3'=0, [ L>=1 ], cost: 1
     75: f399 -> f406 : F1'=1, J2'=1, [ F2>=1 ], cost: 1
     76: f399 -> f406 : F1'=0, J2'=0, [ 0>=F2 ], cost: 1
     77: f406 -> f447 : L'=1, X4'=1, [ F1>=1 ], cost: 1
     79: f406 -> f414 : K2'=Q4_1, L2'=R4, M2'=W4, N2'=S4, O2'=T4, P2'=U4, Q2_1'=P4, R2'=V4, [ 0>=F1 ], cost: 1
     80: f414 -> f421 : F1'=1, S2'=1, [ O2>=1 ], cost: 1
     81: f414 -> f421 : F1'=0, S2'=0, [ 0>=O2 ], cost: 1
     82: f421 -> f447 : L'=1, X4'=1, [ F1>=1 ], cost: 1
     83: f421 -> f430 : P4'=1, W4'=9, [ 0>=F1 ], cost: 1
     84: f430 -> f447 : L'=0, X4'=0, [ T5>=1 ], cost: 1
     85: f430 -> f430 : P4'=1, W4'=9, U5'=free_22, [ 0>=T5 && 0>=free_22 ], cost: 1
     86: f430 -> f430 : P4'=1, W4'=9, T5'=1, U5'=free_23, V5'=Q4_1, W5'=R4, X5'=W4, Y5'=S4, Z5'=T4, A6'=U4, B6'=P4, C6'=V4, [ 0>=T5 && free_23>=1 ], cost: 1
     90: f468 -> f475 : F1'=1, G1'=1, [ B1>=1 ], cost: 1
     91: f468 -> f475 : F1'=0, G1'=0, [ 0>=B1 ], cost: 1
     94: f475 -> f468 : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F3'=1+F3, N3'=free_24, [ 0>=L3 && 0>=free_24 && 0>=F1 ], cost: 1
     95: f475 -> f468 : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F3'=1+F3, L3'=1, N3'=free_25, O3'=C3, P3'=D3, Q3_1'=B, R3'=E3, S3'=F3, T3'=G3, U3'=H3, V3'=Q3, [ 0>=L3 && free_25>=1 && 0>=F1 ], cost: 1
     92: f475 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
     93: f475 -> f588 : L'=0, D6'=0, [ 0>=F1 && L3>=1 ], cost: 1
    115: f588 -> f596 : A'=9, [ L>=1 ], cost: 1
    100: f514 -> f588 : B'=6, L'=0, G3'=-1+G3, D6'=0, [ 0>=G3 && K3>=1 ], cost: 1
    101: f514 -> f514 : B'=4, G3'=-1+G3, X3'=free_26, [ 0>=K3 && 0>=free_26 && 0>=G3 ], cost: 1
    102: f514 -> f514 : B'=4, G3'=-1+G3, K3'=1, X3'=free_27, Y3'=C3, Z3'=D3, A4'=6, B4'=E3, C4'=F3, D4'=-1+G3, E4'=H3, F4'=Q3, [ 0>=K3 && free_27>=1 && 0>=G3 ], cost: 1
    103: f514 -> f547 : B'=7, F1'=1, B2'=C3, C2'=D3, D2'=7, E2'=E3, F2'=1, G2'=G3, H2'=H3, Q2'=Q3, J2'=1, F3'=1, [ 0>=G3 ], cost: 1
    104: f547 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
    106: f547 -> f555 : K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, [ 0>=F1 ], cost: 1
    107: f555 -> f562 : F1'=1, S2'=1, [ O2>=1 ], cost: 1
    108: f555 -> f562 : F1'=0, S2'=0, [ 0>=O2 ], cost: 1
    109: f562 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
    110: f562 -> f571 : B'=9, H3'=1, [ 0>=F1 ], cost: 1
    111: f571 -> f588 : L'=0, D6'=0, [ J3>=1 ], cost: 1
    112: f571 -> f571 : B'=9, H3'=1, G4'=free_28, [ 0>=free_28 && 0>=J3 ], cost: 1
    113: f571 -> f571 : B'=9, H3'=1, J3'=1, G4'=free_29, H4'=C3, Q4'=D3, J4'=B, K4'=E3, L4'=F3, M4'=G3, N4'=H3, O4'=Q3, [ free_29>=1 && 0>=J3 ], cost: 1
    114: f596 -> f596 : A'=9, J'=1, [], cost: 1

Eliminating 1 self-loops for location f304
  Self-Loop 58 has unbounded runtime, resulting in the new transition 120.
  Removing the self-loops: 58.
Eliminating 2 self-loops for location f430
  Self-Loop 85 has unbounded runtime, resulting in the new transition 121.
  Removing the self-loops: 85 86.
Adding an epsilon transition (to model nonexecution of the loops): 123.
Eliminating 2 self-loops for location f514
  Self-Loop 101 has unbounded runtime, resulting in the new transition 124.
  Removing the self-loops: 101 102.
Adding an epsilon transition (to model nonexecution of the loops): 126.
Eliminating 2 self-loops for location f571
  Self-Loop 112 has unbounded runtime, resulting in the new transition 127.
  Removing the self-loops: 112 113.
Adding an epsilon transition (to model nonexecution of the loops): 129.
Eliminating 1 self-loops for location f596
  Self-Loop 114 has unbounded runtime, resulting in the new transition 130.
  Removing the self-loops: 114.

Removed all Self-loops using metering functions (where possible):
  Start location: f3
      5: f14 -> f35 : A'=2, H'=1+H, M'=E, N'=F, O'=2, P'=G, Q_1'=2+H, R'=Q, S'=J, T'=K, U'=0, V'=0, W'=0, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, [ J>=1 ], cost: 1
     57: f14 -> f304 : A'=4, [ 0>=J ], cost: 1
     89: f460 -> f468 : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F3'=1+F3, [ H3>=1 ], cost: 1
     99: f460 -> f514 : B'=4, [ 0>=H3 ], cost: 1
      3: f3 -> f14 : A'=0, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=0, Q'=free_4, J'=free, K'=free_2, [], cost: 1
      4: f155 -> f35 : A'=2, H'=1+H, M'=E, N'=F, O'=2, P'=G, Q_1'=2+H, R'=Q, S'=J, T'=K, U'=0, V'=0, W'=0, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, [ L>=1 ], cost: 1
      7: f35 -> f42 : F1'=1, G1'=1, [ B1>=1 ], cost: 1
      8: f35 -> f42 : F1'=0, G1'=0, [ 0>=B1 ], cost: 1
      9: f42 -> f155 : L'=1, H1'=1, [ F1>=1 ], cost: 1
     10: f42 -> f155 : L'=0, H1'=0, [ W>=1 && 0>=F1 ], cost: 1
     11: f42 -> f35 : O'=2, Q_1'=1+Q_1, X'=M, Y'=N, Z'=2, A1'=P, B1'=1+Q_1, C1'=R, D1'=S, E1'=T, Q1'=free_6, [ 0>=F1 && 0>=free_6 && 0>=W ], cost: 1
     12: f42 -> f35 : O'=2, Q_1'=1+Q_1, W'=1, X'=M, Y'=N, Z'=2, A1'=P, B1'=1+Q_1, C1'=R, D1'=S, E1'=T, Q1'=free_7, J1'=M, K1'=N, L1'=O, M1'=P, N1'=Q_1, O1'=R, P1'=S, Q1_1'=T, [ 0>=F1 && free_7>=1 && 0>=W ], cost: 1
    120: f304 -> [54] : [ 0>=Q ], cost: INF
     88: f447 -> f460 : B'=A, C3'=E, D3'=F, E3'=G, F3'=H, G3'=Q, H3'=J, Q3'=K, J3'=0, K3'=0, L3'=0, [ L>=1 ], cost: 1
     75: f399 -> f406 : F1'=1, J2'=1, [ F2>=1 ], cost: 1
     76: f399 -> f406 : F1'=0, J2'=0, [ 0>=F2 ], cost: 1
     77: f406 -> f447 : L'=1, X4'=1, [ F1>=1 ], cost: 1
     79: f406 -> f414 : K2'=Q4_1, L2'=R4, M2'=W4, N2'=S4, O2'=T4, P2'=U4, Q2_1'=P4, R2'=V4, [ 0>=F1 ], cost: 1
     80: f414 -> f421 : F1'=1, S2'=1, [ O2>=1 ], cost: 1
     81: f414 -> f421 : F1'=0, S2'=0, [ 0>=O2 ], cost: 1
     82: f421 -> f447 : L'=1, X4'=1, [ F1>=1 ], cost: 1
     83: f421 -> f430 : P4'=1, W4'=9, [ 0>=F1 ], cost: 1
    121: f430 -> [55] : [ 0>=T5 && 0>=free_22 ], cost: INF
    122: f430 -> [55] : P4'=1, W4'=9, T5'=1, U5'=free_23, V5'=Q4_1, W5'=R4, X5'=W4, Y5'=S4, Z5'=T4, A6'=U4, B6'=P4, C6'=V4, [ 0>=T5 && free_23>=1 ], cost: 1
    123: f430 -> [55] : [], cost: 0
     90: f468 -> f475 : F1'=1, G1'=1, [ B1>=1 ], cost: 1
     91: f468 -> f475 : F1'=0, G1'=0, [ 0>=B1 ], cost: 1
     94: f475 -> f468 : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F3'=1+F3, N3'=free_24, [ 0>=L3 && 0>=free_24 && 0>=F1 ], cost: 1
     95: f475 -> f468 : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F3'=1+F3, L3'=1, N3'=free_25, O3'=C3, P3'=D3, Q3_1'=B, R3'=E3, S3'=F3, T3'=G3, U3'=H3, V3'=Q3, [ 0>=L3 && free_25>=1 && 0>=F1 ], cost: 1
     92: f475 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
     93: f475 -> f588 : L'=0, D6'=0, [ 0>=F1 && L3>=1 ], cost: 1
    115: f588 -> f596 : A'=9, [ L>=1 ], cost: 1
    124: f514 -> [56] : [ 0>=K3 && 0>=free_26 && 0>=G3 ], cost: INF
    125: f514 -> [56] : B'=4, G3'=-1+G3, K3'=1, X3'=free_27, Y3'=C3, Z3'=D3, A4'=6, B4'=E3, C4'=F3, D4'=-1+G3, E4'=H3, F4'=Q3, [ 0>=K3 && free_27>=1 && 0>=G3 ], cost: 1
    126: f514 -> [56] : [], cost: 0
    104: f547 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
    106: f547 -> f555 : K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, [ 0>=F1 ], cost: 1
    107: f555 -> f562 : F1'=1, S2'=1, [ O2>=1 ], cost: 1
    108: f555 -> f562 : F1'=0, S2'=0, [ 0>=O2 ], cost: 1
    109: f562 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
    110: f562 -> f571 : B'=9, H3'=1, [ 0>=F1 ], cost: 1
    127: f571 -> [57] : [ 0>=free_28 && 0>=J3 ], cost: INF
    128: f571 -> [57] : B'=9, H3'=1, J3'=1, G4'=free_29, H4'=C3, Q4'=D3, J4'=B, K4'=E3, L4'=F3, M4'=G3, N4'=H3, O4'=Q3, [ free_29>=1 && 0>=J3 ], cost: 1
    129: f571 -> [57] : [], cost: 0
    130: f596 -> [58] : [], cost: INF
     73: [54] -> f399 : A'=7, H'=1, B2'=E, C2'=F, D2'=7, E2'=G, F2'=1, G2'=Q, H2'=J, Q2'=K, P4'=J, Q4_1'=E, R4'=F, S4'=G, T4'=1, U4'=Q, V4'=K, W4'=7, Y4'=0, J5'=0, T5'=0, [ 0>=Q ], cost: 1
     84: [55] -> f447 : L'=0, X4'=0, [ T5>=1 ], cost: 1
    100: [56] -> f588 : B'=6, L'=0, G3'=-1+G3, D6'=0, [ 0>=G3 && K3>=1 ], cost: 1
    103: [56] -> f547 : B'=7, F1'=1, B2'=C3, C2'=D3, D2'=7, E2'=E3, F2'=1, G2'=G3, H2'=H3, Q2'=Q3, J2'=1, F3'=1, [ 0>=G3 ], cost: 1
    111: [57] -> f588 : L'=0, D6'=0, [ J3>=1 ], cost: 1


Applied simple chaining:
  Start location: f3
      5: f14 -> f35 : A'=2, H'=1+H, M'=E, N'=F, O'=2, P'=G, Q_1'=2+H, R'=Q, S'=J, T'=K, U'=0, V'=0, W'=0, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, [ J>=1 ], cost: 1
     57: f14 -> f399 : A'=7, H'=1, B2'=E, C2'=F, D2'=7, E2'=G, F2'=1, G2'=Q, H2'=J, Q2'=K, P4'=J, Q4_1'=E, R4'=F, S4'=G, T4'=1, U4'=Q, V4'=K, W4'=7, Y4'=0, J5'=0, T5'=0, [ 0>=J && 0>=Q && 0>=Q ], cost: INF
     89: f460 -> f468 : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F3'=1+F3, [ H3>=1 ], cost: 1
     99: f460 -> f514 : B'=4, [ 0>=H3 ], cost: 1
      3: f3 -> f14 : A'=0, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=0, Q'=free_4, J'=free, K'=free_2, [], cost: 1
      4: f155 -> f35 : A'=2, H'=1+H, M'=E, N'=F, O'=2, P'=G, Q_1'=2+H, R'=Q, S'=J, T'=K, U'=0, V'=0, W'=0, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, [ L>=1 ], cost: 1
      7: f35 -> f42 : F1'=1, G1'=1, [ B1>=1 ], cost: 1
      8: f35 -> f42 : F1'=0, G1'=0, [ 0>=B1 ], cost: 1
      9: f42 -> f155 : L'=1, H1'=1, [ F1>=1 ], cost: 1
     10: f42 -> f155 : L'=0, H1'=0, [ W>=1 && 0>=F1 ], cost: 1
     11: f42 -> f35 : O'=2, Q_1'=1+Q_1, X'=M, Y'=N, Z'=2, A1'=P, B1'=1+Q_1, C1'=R, D1'=S, E1'=T, Q1'=free_6, [ 0>=F1 && 0>=free_6 && 0>=W ], cost: 1
     12: f42 -> f35 : O'=2, Q_1'=1+Q_1, W'=1, X'=M, Y'=N, Z'=2, A1'=P, B1'=1+Q_1, C1'=R, D1'=S, E1'=T, Q1'=free_7, J1'=M, K1'=N, L1'=O, M1'=P, N1'=Q_1, O1'=R, P1'=S, Q1_1'=T, [ 0>=F1 && free_7>=1 && 0>=W ], cost: 1
     88: f447 -> f460 : B'=A, C3'=E, D3'=F, E3'=G, F3'=H, G3'=Q, H3'=J, Q3'=K, J3'=0, K3'=0, L3'=0, [ L>=1 ], cost: 1
     75: f399 -> f406 : F1'=1, J2'=1, [ F2>=1 ], cost: 1
     76: f399 -> f406 : F1'=0, J2'=0, [ 0>=F2 ], cost: 1
     77: f406 -> f447 : L'=1, X4'=1, [ F1>=1 ], cost: 1
     79: f406 -> f414 : K2'=Q4_1, L2'=R4, M2'=W4, N2'=S4, O2'=T4, P2'=U4, Q2_1'=P4, R2'=V4, [ 0>=F1 ], cost: 1
     80: f414 -> f421 : F1'=1, S2'=1, [ O2>=1 ], cost: 1
     81: f414 -> f421 : F1'=0, S2'=0, [ 0>=O2 ], cost: 1
     82: f421 -> f447 : L'=1, X4'=1, [ F1>=1 ], cost: 1
     83: f421 -> f430 : P4'=1, W4'=9, [ 0>=F1 ], cost: 1
    121: f430 -> [55] : [ 0>=T5 && 0>=free_22 ], cost: INF
    122: f430 -> [55] : P4'=1, W4'=9, T5'=1, U5'=free_23, V5'=Q4_1, W5'=R4, X5'=W4, Y5'=S4, Z5'=T4, A6'=U4, B6'=P4, C6'=V4, [ 0>=T5 && free_23>=1 ], cost: 1
    123: f430 -> [55] : [], cost: 0
     90: f468 -> f475 : F1'=1, G1'=1, [ B1>=1 ], cost: 1
     91: f468 -> f475 : F1'=0, G1'=0, [ 0>=B1 ], cost: 1
     94: f475 -> f468 : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F3'=1+F3, N3'=free_24, [ 0>=L3 && 0>=free_24 && 0>=F1 ], cost: 1
     95: f475 -> f468 : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F3'=1+F3, L3'=1, N3'=free_25, O3'=C3, P3'=D3, Q3_1'=B, R3'=E3, S3'=F3, T3'=G3, U3'=H3, V3'=Q3, [ 0>=L3 && free_25>=1 && 0>=F1 ], cost: 1
     92: f475 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
     93: f475 -> f588 : L'=0, D6'=0, [ 0>=F1 && L3>=1 ], cost: 1
    115: f588 -> [58] : A'=9, [ L>=1 ], cost: INF
    124: f514 -> [56] : [ 0>=K3 && 0>=free_26 && 0>=G3 ], cost: INF
    125: f514 -> [56] : B'=4, G3'=-1+G3, K3'=1, X3'=free_27, Y3'=C3, Z3'=D3, A4'=6, B4'=E3, C4'=F3, D4'=-1+G3, E4'=H3, F4'=Q3, [ 0>=K3 && free_27>=1 && 0>=G3 ], cost: 1
    126: f514 -> [56] : [], cost: 0
    104: f547 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
    106: f547 -> f555 : K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, [ 0>=F1 ], cost: 1
    107: f555 -> f562 : F1'=1, S2'=1, [ O2>=1 ], cost: 1
    108: f555 -> f562 : F1'=0, S2'=0, [ 0>=O2 ], cost: 1
    109: f562 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
    110: f562 -> f571 : B'=9, H3'=1, [ 0>=F1 ], cost: 1
    127: f571 -> [57] : [ 0>=free_28 && 0>=J3 ], cost: INF
    128: f571 -> [57] : B'=9, H3'=1, J3'=1, G4'=free_29, H4'=C3, Q4'=D3, J4'=B, K4'=E3, L4'=F3, M4'=G3, N4'=H3, O4'=Q3, [ free_29>=1 && 0>=J3 ], cost: 1
    129: f571 -> [57] : [], cost: 0
     84: [55] -> f447 : L'=0, X4'=0, [ T5>=1 ], cost: 1
    100: [56] -> f588 : B'=6, L'=0, G3'=-1+G3, D6'=0, [ 0>=G3 && K3>=1 ], cost: 1
    103: [56] -> f547 : B'=7, F1'=1, B2'=C3, C2'=D3, D2'=7, E2'=E3, F2'=1, G2'=G3, H2'=H3, Q2'=Q3, J2'=1, F3'=1, [ 0>=G3 ], cost: 1
    111: [57] -> f588 : L'=0, D6'=0, [ J3>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f3
    131: f3 -> f35 : A'=2, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, M'=free_5, N'=free_1, O'=2, P'=free_3, Q_1'=2, R'=free_4, S'=free, T'=free_2, U'=0, V'=0, W'=0, X'=free_5, Y'=free_1, Z'=2, A1'=free_3, B1'=2, C1'=free_4, D1'=free, E1'=free_2, [ free>=1 ], cost: 2
    132: f3 -> f399 : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 ], cost: INF
      4: f155 -> f35 : A'=2, H'=1+H, M'=E, N'=F, O'=2, P'=G, Q_1'=2+H, R'=Q, S'=J, T'=K, U'=0, V'=0, W'=0, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, [ L>=1 ], cost: 1
    133: f35 -> f155 : L'=1, F1'=1, G1'=1, H1'=1, [ B1>=1 && 1>=1 ], cost: 2
    134: f35 -> f155 : L'=0, F1'=0, G1'=0, H1'=0, [ 0>=B1 && W>=1 && 0>=0 ], cost: 2
    135: f35 -> f35 : O'=2, Q_1'=1+Q_1, X'=M, Y'=N, Z'=2, A1'=P, B1'=1+Q_1, C1'=R, D1'=S, E1'=T, F1'=0, G1'=0, Q1'=free_6, [ 0>=B1 && 0>=0 && 0>=free_6 && 0>=W ], cost: 2
    136: f35 -> f35 : O'=2, Q_1'=1+Q_1, W'=1, X'=M, Y'=N, Z'=2, A1'=P, B1'=1+Q_1, C1'=R, D1'=S, E1'=T, F1'=0, G1'=0, Q1'=free_7, J1'=M, K1'=N, L1'=O, M1'=P, N1'=Q_1, O1'=R, P1'=S, Q1_1'=T, [ 0>=B1 && 0>=0 && free_7>=1 && 0>=W ], cost: 2
    139: f447 -> f468 : B'=2, X'=E, Y'=F, Z'=2, A1'=G, B1'=1+H, C1'=Q, D1'=J, E1'=K, C3'=E, D3'=F, E3'=G, F3'=1+H, G3'=Q, H3'=J, Q3'=K, J3'=0, K3'=0, L3'=0, [ L>=1 && J>=1 ], cost: 2
    140: f447 -> f514 : B'=4, C3'=E, D3'=F, E3'=G, F3'=H, G3'=Q, H3'=J, Q3'=K, J3'=0, K3'=0, L3'=0, [ L>=1 && 0>=J ], cost: 2
    137: f399 -> f447 : L'=1, F1'=1, J2'=1, X4'=1, [ F2>=1 && 1>=1 ], cost: 2
    138: f399 -> f414 : F1'=0, J2'=0, K2'=Q4_1, L2'=R4, M2'=W4, N2'=S4, O2'=T4, P2'=U4, Q2_1'=P4, R2'=V4, [ 0>=F2 && 0>=0 ], cost: 2
    156: f414 -> f447 : L'=1, F1'=1, S2'=1, X4'=1, [ O2>=1 && 1>=1 ], cost: 2
    157: f414 -> f430 : F1'=0, S2'=0, P4'=1, W4'=9, [ 0>=O2 && 0>=0 ], cost: 2
    159: f430 -> f447 : L'=0, P4'=1, W4'=9, X4'=0, T5'=1, U5'=free_23, V5'=Q4_1, W5'=R4, X5'=W4, Y5'=S4, Z5'=T4, A6'=U4, B6'=P4, C6'=V4, [ 0>=T5 && free_23>=1 && 1>=1 ], cost: 2
    160: f430 -> f447 : L'=0, X4'=0, [ T5>=1 ], cost: 1
    158: f430 -> [60] : [ 0>=T5 && 0>=free_22 ], cost: INF
    142: f468 -> f468 : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F1'=0, G1'=0, F3'=1+F3, N3'=free_24, [ 0>=B1 && 0>=L3 && 0>=free_24 && 0>=0 ], cost: 2
    143: f468 -> f468 : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F1'=0, G1'=0, F3'=1+F3, L3'=1, N3'=free_25, O3'=C3, P3'=D3, Q3_1'=B, R3'=E3, S3'=F3, T3'=G3, U3'=H3, V3'=Q3, [ 0>=B1 && 0>=L3 && free_25>=1 && 0>=0 ], cost: 2
    141: f468 -> f588 : L'=1, F1'=1, G1'=1, D6'=1, [ B1>=1 && 1>=1 ], cost: 2
    144: f468 -> f588 : L'=0, F1'=0, G1'=0, D6'=0, [ 0>=B1 && 0>=0 && L3>=1 ], cost: 2
    115: f588 -> [58] : A'=9, [ L>=1 ], cost: INF
    147: f514 -> f588 : B'=6, L'=0, G3'=-2+G3, K3'=1, X3'=free_27, Y3'=C3, Z3'=D3, A4'=6, B4'=E3, C4'=F3, D4'=-1+G3, E4'=H3, F4'=Q3, D6'=0, [ 0>=K3 && free_27>=1 && 0>=G3 && 0>=-1+G3 && 1>=1 ], cost: 2
    149: f514 -> f588 : B'=6, L'=0, G3'=-1+G3, D6'=0, [ 0>=G3 && K3>=1 ], cost: 1
    146: f514 -> f547 : B'=7, F1'=1, B2'=C3, C2'=D3, D2'=7, E2'=E3, F2'=1, G2'=G3, H2'=H3, Q2'=Q3, J2'=1, F3'=1, [ 0>=K3 && 0>=free_26 && 0>=G3 && 0>=G3 ], cost: INF
    148: f514 -> f547 : B'=7, F1'=1, B2'=C3, C2'=D3, D2'=7, E2'=E3, F2'=1, G2'=-1+G3, H2'=H3, Q2'=Q3, J2'=1, F3'=1, G3'=-1+G3, K3'=1, X3'=free_27, Y3'=C3, Z3'=D3, A4'=6, B4'=E3, C4'=F3, D4'=-1+G3, E4'=H3, F4'=Q3, [ 0>=K3 && free_27>=1 && 0>=G3 && 0>=-1+G3 ], cost: 2
    150: f514 -> f547 : B'=7, F1'=1, B2'=C3, C2'=D3, D2'=7, E2'=E3, F2'=1, G2'=G3, H2'=H3, Q2'=Q3, J2'=1, F3'=1, [ 0>=G3 ], cost: 1
    145: f514 -> [59] : [ 0>=K3 && 0>=free_26 && 0>=G3 ], cost: INF
    104: f547 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
    151: f547 -> f562 : F1'=1, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, S2'=1, [ 0>=F1 && F3>=1 ], cost: 2
    152: f547 -> f562 : F1'=0, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, S2'=0, [ 0>=F1 && 0>=F3 ], cost: 2
    109: f562 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
    153: f562 -> [57] : B'=9, H3'=1, [ 0>=F1 && 0>=free_28 && 0>=J3 ], cost: INF
    154: f562 -> [57] : B'=9, H3'=1, J3'=1, G4'=free_29, H4'=C3, Q4'=D3, J4'=9, K4'=E3, L4'=F3, M4'=G3, N4'=1, O4'=Q3, [ 0>=F1 && free_29>=1 && 0>=J3 ], cost: 2
    155: f562 -> [57] : B'=9, H3'=1, [ 0>=F1 ], cost: 1
    111: [57] -> f588 : L'=0, D6'=0, [ J3>=1 ], cost: 1

Eliminating 2 self-loops for location f35
  Removing the self-loops: 135 136.
Adding an epsilon transition (to model nonexecution of the loops): 163.
Eliminating 2 self-loops for location f468
  Removing the self-loops: 142 143.
Adding an epsilon transition (to model nonexecution of the loops): 166.

Removed all Self-loops using metering functions (where possible):
  Start location: f3
    131: f3 -> f35 : A'=2, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, M'=free_5, N'=free_1, O'=2, P'=free_3, Q_1'=2, R'=free_4, S'=free, T'=free_2, U'=0, V'=0, W'=0, X'=free_5, Y'=free_1, Z'=2, A1'=free_3, B1'=2, C1'=free_4, D1'=free, E1'=free_2, [ free>=1 ], cost: 2
    132: f3 -> f399 : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 ], cost: INF
      4: f155 -> f35 : A'=2, H'=1+H, M'=E, N'=F, O'=2, P'=G, Q_1'=2+H, R'=Q, S'=J, T'=K, U'=0, V'=0, W'=0, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, [ L>=1 ], cost: 1
    161: f35 -> [61] : O'=2, Q_1'=1+Q_1, X'=M, Y'=N, Z'=2, A1'=P, B1'=1+Q_1, C1'=R, D1'=S, E1'=T, F1'=0, G1'=0, Q1'=free_6, [ 0>=B1 && 0>=free_6 && 0>=W ], cost: 2
    162: f35 -> [61] : O'=2, Q_1'=1+Q_1, W'=1, X'=M, Y'=N, Z'=2, A1'=P, B1'=1+Q_1, C1'=R, D1'=S, E1'=T, F1'=0, G1'=0, Q1'=free_7, J1'=M, K1'=N, L1'=O, M1'=P, N1'=Q_1, O1'=R, P1'=S, Q1_1'=T, [ 0>=B1 && free_7>=1 && 0>=W ], cost: 2
    163: f35 -> [61] : [], cost: 0
    139: f447 -> f468 : B'=2, X'=E, Y'=F, Z'=2, A1'=G, B1'=1+H, C1'=Q, D1'=J, E1'=K, C3'=E, D3'=F, E3'=G, F3'=1+H, G3'=Q, H3'=J, Q3'=K, J3'=0, K3'=0, L3'=0, [ L>=1 && J>=1 ], cost: 2
    140: f447 -> f514 : B'=4, C3'=E, D3'=F, E3'=G, F3'=H, G3'=Q, H3'=J, Q3'=K, J3'=0, K3'=0, L3'=0, [ L>=1 && 0>=J ], cost: 2
    137: f399 -> f447 : L'=1, F1'=1, J2'=1, X4'=1, [ F2>=1 && 1>=1 ], cost: 2
    138: f399 -> f414 : F1'=0, J2'=0, K2'=Q4_1, L2'=R4, M2'=W4, N2'=S4, O2'=T4, P2'=U4, Q2_1'=P4, R2'=V4, [ 0>=F2 && 0>=0 ], cost: 2
    156: f414 -> f447 : L'=1, F1'=1, S2'=1, X4'=1, [ O2>=1 && 1>=1 ], cost: 2
    157: f414 -> f430 : F1'=0, S2'=0, P4'=1, W4'=9, [ 0>=O2 && 0>=0 ], cost: 2
    159: f430 -> f447 : L'=0, P4'=1, W4'=9, X4'=0, T5'=1, U5'=free_23, V5'=Q4_1, W5'=R4, X5'=W4, Y5'=S4, Z5'=T4, A6'=U4, B6'=P4, C6'=V4, [ 0>=T5 && free_23>=1 && 1>=1 ], cost: 2
    160: f430 -> f447 : L'=0, X4'=0, [ T5>=1 ], cost: 1
    158: f430 -> [60] : [ 0>=T5 && 0>=free_22 ], cost: INF
    164: f468 -> [62] : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F1'=0, G1'=0, F3'=1+F3, N3'=free_24, [ 0>=B1 && 0>=L3 && 0>=free_24 ], cost: 2
    165: f468 -> [62] : B'=2, X'=C3, Y'=D3, Z'=2, A1'=E3, B1'=1+F3, C1'=G3, D1'=H3, E1'=Q3, F1'=0, G1'=0, F3'=1+F3, L3'=1, N3'=free_25, O3'=C3, P3'=D3, Q3_1'=B, R3'=E3, S3'=F3, T3'=G3, U3'=H3, V3'=Q3, [ 0>=B1 && 0>=L3 && free_25>=1 ], cost: 2
    166: f468 -> [62] : [], cost: 0
    115: f588 -> [58] : A'=9, [ L>=1 ], cost: INF
    147: f514 -> f588 : B'=6, L'=0, G3'=-2+G3, K3'=1, X3'=free_27, Y3'=C3, Z3'=D3, A4'=6, B4'=E3, C4'=F3, D4'=-1+G3, E4'=H3, F4'=Q3, D6'=0, [ 0>=K3 && free_27>=1 && 0>=G3 && 0>=-1+G3 && 1>=1 ], cost: 2
    149: f514 -> f588 : B'=6, L'=0, G3'=-1+G3, D6'=0, [ 0>=G3 && K3>=1 ], cost: 1
    146: f514 -> f547 : B'=7, F1'=1, B2'=C3, C2'=D3, D2'=7, E2'=E3, F2'=1, G2'=G3, H2'=H3, Q2'=Q3, J2'=1, F3'=1, [ 0>=K3 && 0>=free_26 && 0>=G3 && 0>=G3 ], cost: INF
    148: f514 -> f547 : B'=7, F1'=1, B2'=C3, C2'=D3, D2'=7, E2'=E3, F2'=1, G2'=-1+G3, H2'=H3, Q2'=Q3, J2'=1, F3'=1, G3'=-1+G3, K3'=1, X3'=free_27, Y3'=C3, Z3'=D3, A4'=6, B4'=E3, C4'=F3, D4'=-1+G3, E4'=H3, F4'=Q3, [ 0>=K3 && free_27>=1 && 0>=G3 && 0>=-1+G3 ], cost: 2
    150: f514 -> f547 : B'=7, F1'=1, B2'=C3, C2'=D3, D2'=7, E2'=E3, F2'=1, G2'=G3, H2'=H3, Q2'=Q3, J2'=1, F3'=1, [ 0>=G3 ], cost: 1
    145: f514 -> [59] : [ 0>=K3 && 0>=free_26 && 0>=G3 ], cost: INF
    104: f547 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
    151: f547 -> f562 : F1'=1, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, S2'=1, [ 0>=F1 && F3>=1 ], cost: 2
    152: f547 -> f562 : F1'=0, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, S2'=0, [ 0>=F1 && 0>=F3 ], cost: 2
    109: f562 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
    153: f562 -> [57] : B'=9, H3'=1, [ 0>=F1 && 0>=free_28 && 0>=J3 ], cost: INF
    154: f562 -> [57] : B'=9, H3'=1, J3'=1, G4'=free_29, H4'=C3, Q4'=D3, J4'=9, K4'=E3, L4'=F3, M4'=G3, N4'=1, O4'=Q3, [ 0>=F1 && free_29>=1 && 0>=J3 ], cost: 2
    155: f562 -> [57] : B'=9, H3'=1, [ 0>=F1 ], cost: 1
    111: [57] -> f588 : L'=0, D6'=0, [ J3>=1 ], cost: 1
    133: [61] -> f155 : L'=1, F1'=1, G1'=1, H1'=1, [ B1>=1 && 1>=1 ], cost: 2
    134: [61] -> f155 : L'=0, F1'=0, G1'=0, H1'=0, [ 0>=B1 && W>=1 && 0>=0 ], cost: 2
    141: [62] -> f588 : L'=1, F1'=1, G1'=1, D6'=1, [ B1>=1 && 1>=1 ], cost: 2
    144: [62] -> f588 : L'=0, F1'=0, G1'=0, D6'=0, [ 0>=B1 && 0>=0 && L3>=1 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f3
    131: f3 -> f35 : A'=2, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, M'=free_5, N'=free_1, O'=2, P'=free_3, Q_1'=2, R'=free_4, S'=free, T'=free_2, U'=0, V'=0, W'=0, X'=free_5, Y'=free_1, Z'=2, A1'=free_3, B1'=2, C1'=free_4, D1'=free, E1'=free_2, [ free>=1 ], cost: 2
    167: f3 -> f447 : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    168: f3 -> [63] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 ], cost: INF
      4: f155 -> f35 : A'=2, H'=1+H, M'=E, N'=F, O'=2, P'=G, Q_1'=2+H, R'=Q, S'=J, T'=K, U'=0, V'=0, W'=0, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, [ L>=1 ], cost: 1
    169: f35 -> f155 : L'=1, O'=2, Q_1'=1+Q_1, X'=M, Y'=N, Z'=2, A1'=P, B1'=1+Q_1, C1'=R, D1'=S, E1'=T, F1'=1, G1'=1, H1'=1, Q1'=free_6, [ 0>=B1 && 0>=free_6 && 0>=W && 1+Q_1>=1 && 1>=1 ], cost: 4
    170: f35 -> f155 : L'=1, O'=2, Q_1'=1+Q_1, W'=1, X'=M, Y'=N, Z'=2, A1'=P, B1'=1+Q_1, C1'=R, D1'=S, E1'=T, F1'=1, G1'=1, H1'=1, Q1'=free_7, J1'=M, K1'=N, L1'=O, M1'=P, N1'=Q_1, O1'=R, P1'=S, Q1_1'=T, [ 0>=B1 && free_7>=1 && 0>=W && 1+Q_1>=1 && 1>=1 ], cost: 4
    171: f35 -> f155 : L'=0, O'=2, Q_1'=1+Q_1, W'=1, X'=M, Y'=N, Z'=2, A1'=P, B1'=1+Q_1, C1'=R, D1'=S, E1'=T, F1'=0, G1'=0, H1'=0, Q1'=free_7, J1'=M, K1'=N, L1'=O, M1'=P, N1'=Q_1, O1'=R, P1'=S, Q1_1'=T, [ 0>=B1 && free_7>=1 && 0>=W && 0>=1+Q_1 && 1>=1 && 0>=0 ], cost: 4
    172: f35 -> f155 : L'=1, F1'=1, G1'=1, H1'=1, [ B1>=1 && 1>=1 ], cost: 2
    173: f35 -> f155 : L'=0, F1'=0, G1'=0, H1'=0, [ 0>=B1 && W>=1 && 0>=0 ], cost: 2
    177: f447 -> f588 : B'=6, L'=0, C3'=E, D3'=F, E3'=G, F3'=H, G3'=-2+Q, H3'=J, Q3'=K, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=E, Z3'=F, A4'=6, B4'=G, C4'=H, D4'=-1+Q, E4'=J, F4'=K, D6'=0, [ L>=1 && 0>=J && 0>=0 && free_27>=1 && 0>=Q && 0>=-1+Q && 1>=1 ], cost: 4
    178: f447 -> f547 : B'=7, F1'=1, B2'=E, C2'=F, D2'=7, E2'=G, F2'=1, G2'=Q, H2'=J, Q2'=K, J2'=1, C3'=E, D3'=F, E3'=G, F3'=1, G3'=Q, H3'=J, Q3'=K, J3'=0, K3'=0, L3'=0, [ L>=1 && 0>=J && 0>=0 && 0>=free_26 && 0>=Q && 0>=Q ], cost: INF
    179: f447 -> f547 : B'=7, F1'=1, B2'=E, C2'=F, D2'=7, E2'=G, F2'=1, G2'=-1+Q, H2'=J, Q2'=K, J2'=1, C3'=E, D3'=F, E3'=G, F3'=1, G3'=-1+Q, H3'=J, Q3'=K, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=E, Z3'=F, A4'=6, B4'=G, C4'=H, D4'=-1+Q, E4'=J, F4'=K, [ L>=1 && 0>=J && 0>=0 && free_27>=1 && 0>=Q && 0>=-1+Q ], cost: 4
    180: f447 -> f547 : B'=7, F1'=1, B2'=E, C2'=F, D2'=7, E2'=G, F2'=1, G2'=Q, H2'=J, Q2'=K, J2'=1, C3'=E, D3'=F, E3'=G, F3'=1, G3'=Q, H3'=J, Q3'=K, J3'=0, K3'=0, L3'=0, [ L>=1 && 0>=J && 0>=Q ], cost: 3
    181: f447 -> [59] : B'=4, C3'=E, D3'=F, E3'=G, F3'=H, G3'=Q, H3'=J, Q3'=K, J3'=0, K3'=0, L3'=0, [ L>=1 && 0>=J && 0>=0 && 0>=free_26 && 0>=Q ], cost: INF
    174: f447 -> [62] : B'=2, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, F1'=0, G1'=0, C3'=E, D3'=F, E3'=G, F3'=2+H, G3'=Q, H3'=J, Q3'=K, J3'=0, K3'=0, L3'=0, N3'=free_24, [ L>=1 && J>=1 && 0>=1+H && 0>=0 && 0>=free_24 ], cost: 4
    175: f447 -> [62] : B'=2, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, F1'=0, G1'=0, C3'=E, D3'=F, E3'=G, F3'=2+H, G3'=Q, H3'=J, Q3'=K, J3'=0, K3'=0, L3'=1, N3'=free_25, O3'=E, P3'=F, Q3_1'=2, R3'=G, S3'=1+H, T3'=Q, U3'=J, V3'=K, [ L>=1 && J>=1 && 0>=1+H && 0>=0 && free_25>=1 ], cost: 4
    176: f447 -> [62] : B'=2, X'=E, Y'=F, Z'=2, A1'=G, B1'=1+H, C1'=Q, D1'=J, E1'=K, C3'=E, D3'=F, E3'=G, F3'=1+H, G3'=Q, H3'=J, Q3'=K, J3'=0, K3'=0, L3'=0, [ L>=1 && J>=1 ], cost: 2
    115: f588 -> [58] : A'=9, [ L>=1 ], cost: INF
    104: f547 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
    182: f547 -> f588 : L'=1, F1'=1, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, S2'=1, D6'=1, [ 0>=F1 && F3>=1 && 1>=1 ], cost: 3
    183: f547 -> [57] : B'=9, F1'=0, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, S2'=0, H3'=1, [ 0>=F1 && 0>=F3 && 0>=0 && 0>=free_28 && 0>=J3 ], cost: INF
    184: f547 -> [57] : B'=9, F1'=0, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, S2'=0, H3'=1, J3'=1, G4'=free_29, H4'=C3, Q4'=D3, J4'=9, K4'=E3, L4'=F3, M4'=G3, N4'=1, O4'=Q3, [ 0>=F1 && 0>=F3 && 0>=0 && free_29>=1 && 0>=J3 ], cost: 4
    185: f547 -> [57] : B'=9, F1'=0, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, S2'=0, H3'=1, [ 0>=F1 && 0>=F3 && 0>=0 ], cost: 3
    111: [57] -> f588 : L'=0, D6'=0, [ J3>=1 ], cost: 1
    141: [62] -> f588 : L'=1, F1'=1, G1'=1, D6'=1, [ B1>=1 && 1>=1 ], cost: 2
    144: [62] -> f588 : L'=0, F1'=0, G1'=0, D6'=0, [ 0>=B1 && 0>=0 && L3>=1 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f3
    131: f3 -> f35 : A'=2, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, M'=free_5, N'=free_1, O'=2, P'=free_3, Q_1'=2, R'=free_4, S'=free, T'=free_2, U'=0, V'=0, W'=0, X'=free_5, Y'=free_1, Z'=2, A1'=free_3, B1'=2, C1'=free_4, D1'=free, E1'=free_2, [ free>=1 ], cost: 2
    186: f3 -> f588 : A'=7, B'=6, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=0, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-2+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, D6'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 && 1>=1 ], cost: INF
    187: f3 -> f547 : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 && 0>=free_4 ], cost: INF
    188: f3 -> f547 : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=-1+free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-1+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 ], cost: INF
    189: f3 -> f547 : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=free_4 ], cost: INF
    190: f3 -> [59] : A'=7, B'=4, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 ], cost: INF
    168: f3 -> [63] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 ], cost: INF
    191: f3 -> [64] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    192: f3 -> [65] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    193: f3 -> [66] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    194: f35 -> f35 : A'=2, H'=1+H, L'=1, M'=E, N'=F, O'=2, P'=G, Q_1'=2+H, R'=Q, S'=J, T'=K, U'=0, V'=0, W'=0, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, F1'=1, G1'=1, H1'=1, Q1'=free_6, [ 0>=B1 && 0>=free_6 && 0>=W && 1+Q_1>=1 && 1>=1 && 1>=1 ], cost: 5
    195: f35 -> f35 : A'=2, H'=1+H, L'=1, M'=E, N'=F, O'=2, P'=G, Q_1'=2+H, R'=Q, S'=J, T'=K, U'=0, V'=0, W'=0, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, F1'=1, G1'=1, H1'=1, Q1'=free_7, J1'=M, K1'=N, L1'=O, M1'=P, N1'=Q_1, O1'=R, P1'=S, Q1_1'=T, [ 0>=B1 && free_7>=1 && 0>=W && 1+Q_1>=1 && 1>=1 && 1>=1 ], cost: 5
    196: f35 -> f35 : A'=2, H'=1+H, L'=1, M'=E, N'=F, O'=2, P'=G, Q_1'=2+H, R'=Q, S'=J, T'=K, U'=0, V'=0, W'=0, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, F1'=1, G1'=1, H1'=1, [ B1>=1 && 1>=1 && 1>=1 ], cost: 3
    115: f588 -> [58] : A'=9, [ L>=1 ], cost: INF
    104: f547 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
    182: f547 -> f588 : L'=1, F1'=1, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, S2'=1, D6'=1, [ 0>=F1 && F3>=1 && 1>=1 ], cost: 3
    198: f547 -> f588 : B'=9, L'=0, F1'=0, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, S2'=0, H3'=1, J3'=1, G4'=free_29, H4'=C3, Q4'=D3, J4'=9, K4'=E3, L4'=F3, M4'=G3, N4'=1, O4'=Q3, D6'=0, [ 0>=F1 && 0>=F3 && 0>=0 && free_29>=1 && 0>=J3 && 1>=1 ], cost: 5
    199: f547 -> f588 : B'=9, L'=0, F1'=0, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, S2'=0, H3'=1, D6'=0, [ 0>=F1 && 0>=F3 && 0>=0 && J3>=1 ], cost: 4
    197: f547 -> [67] : B'=9, F1'=0, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, S2'=0, H3'=1, [ 0>=F1 && 0>=F3 && 0>=0 && 0>=free_28 && 0>=J3 ], cost: INF

Eliminating 3 self-loops for location f35
  Removing the self-loops: 194 195 196.
Adding an epsilon transition (to model nonexecution of the loops): 203.

Removed all Self-loops using metering functions (where possible):
  Start location: f3
    131: f3 -> f35 : A'=2, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, M'=free_5, N'=free_1, O'=2, P'=free_3, Q_1'=2, R'=free_4, S'=free, T'=free_2, U'=0, V'=0, W'=0, X'=free_5, Y'=free_1, Z'=2, A1'=free_3, B1'=2, C1'=free_4, D1'=free, E1'=free_2, [ free>=1 ], cost: 2
    186: f3 -> f588 : A'=7, B'=6, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=0, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-2+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, D6'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 && 1>=1 ], cost: INF
    187: f3 -> f547 : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 && 0>=free_4 ], cost: INF
    188: f3 -> f547 : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=-1+free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-1+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 ], cost: INF
    189: f3 -> f547 : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=free_4 ], cost: INF
    190: f3 -> [59] : A'=7, B'=4, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 ], cost: INF
    168: f3 -> [63] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 ], cost: INF
    191: f3 -> [64] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    192: f3 -> [65] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    193: f3 -> [66] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    200: f35 -> [68] : A'=2, H'=1+H, L'=1, M'=E, N'=F, O'=2, P'=G, Q_1'=2+H, R'=Q, S'=J, T'=K, U'=0, V'=0, W'=0, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, F1'=1, G1'=1, H1'=1, Q1'=free_6, [ 0>=B1 && 0>=free_6 && 0>=W && 1+Q_1>=1 ], cost: 5
    201: f35 -> [68] : A'=2, H'=1+H, L'=1, M'=E, N'=F, O'=2, P'=G, Q_1'=2+H, R'=Q, S'=J, T'=K, U'=0, V'=0, W'=0, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, F1'=1, G1'=1, H1'=1, Q1'=free_7, J1'=M, K1'=N, L1'=O, M1'=P, N1'=Q_1, O1'=R, P1'=S, Q1_1'=T, [ 0>=B1 && free_7>=1 && 0>=W && 1+Q_1>=1 ], cost: 5
    202: f35 -> [68] : A'=2, H'=1+H, L'=1, M'=E, N'=F, O'=2, P'=G, Q_1'=2+H, R'=Q, S'=J, T'=K, U'=0, V'=0, W'=0, X'=E, Y'=F, Z'=2, A1'=G, B1'=2+H, C1'=Q, D1'=J, E1'=K, F1'=1, G1'=1, H1'=1, [ B1>=1 ], cost: 3
    203: f35 -> [68] : [], cost: 0
    115: f588 -> [58] : A'=9, [ L>=1 ], cost: INF
    104: f547 -> f588 : L'=1, D6'=1, [ F1>=1 ], cost: 1
    182: f547 -> f588 : L'=1, F1'=1, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, S2'=1, D6'=1, [ 0>=F1 && F3>=1 && 1>=1 ], cost: 3
    198: f547 -> f588 : B'=9, L'=0, F1'=0, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, S2'=0, H3'=1, J3'=1, G4'=free_29, H4'=C3, Q4'=D3, J4'=9, K4'=E3, L4'=F3, M4'=G3, N4'=1, O4'=Q3, D6'=0, [ 0>=F1 && 0>=F3 && 0>=0 && free_29>=1 && 0>=J3 && 1>=1 ], cost: 5
    199: f547 -> f588 : B'=9, L'=0, F1'=0, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, S2'=0, H3'=1, D6'=0, [ 0>=F1 && 0>=F3 && 0>=0 && J3>=1 ], cost: 4
    197: f547 -> [67] : B'=9, F1'=0, K2'=C3, L2'=D3, M2'=B, N2'=E3, O2'=F3, P2'=G3, Q2_1'=H3, R2'=Q3, S2'=0, H3'=1, [ 0>=F1 && 0>=F3 && 0>=0 && 0>=free_28 && 0>=J3 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f3
    186: f3 -> f588 : A'=7, B'=6, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=0, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-2+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, D6'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 && 1>=1 ], cost: INF
    206: f3 -> f588 : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, D6'=1, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 && 0>=free_4 && 1>=1 ], cost: INF
    211: f3 -> f588 : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=-1+free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-1+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, D6'=1, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 && 1>=1 ], cost: INF
    216: f3 -> f588 : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, D6'=1, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=free_4 && 1>=1 ], cost: INF
    190: f3 -> [59] : A'=7, B'=4, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 ], cost: INF
    168: f3 -> [63] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 ], cost: INF
    191: f3 -> [64] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    192: f3 -> [65] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    193: f3 -> [66] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    207: f3 -> [69] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 && 0>=free_4 ], cost: INF
    208: f3 -> [70] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 && 0>=free_4 ], cost: INF
    209: f3 -> [71] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 && 0>=free_4 ], cost: INF
    210: f3 -> [72] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 && 0>=free_4 ], cost: INF
    212: f3 -> [73] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=-1+free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-1+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 ], cost: INF
    213: f3 -> [74] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=-1+free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-1+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 ], cost: INF
    214: f3 -> [75] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=-1+free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-1+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 ], cost: INF
    215: f3 -> [76] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=-1+free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-1+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 ], cost: INF
    217: f3 -> [77] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=free_4 ], cost: INF
    218: f3 -> [78] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=free_4 ], cost: INF
    219: f3 -> [79] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=free_4 ], cost: INF
    220: f3 -> [80] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=free_4 ], cost: INF
    115: f588 -> [58] : A'=9, [ L>=1 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f3
    222: f3 -> [58] : A'=9, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, D6'=1, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    223: f3 -> [58] : A'=9, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=-1+free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-1+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, D6'=1, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 && 1>=1 && 1>=1 ], cost: INF
    224: f3 -> [58] : A'=9, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, D6'=1, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    190: f3 -> [59] : A'=7, B'=4, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 ], cost: INF
    168: f3 -> [63] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 ], cost: INF
    191: f3 -> [64] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    192: f3 -> [65] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    193: f3 -> [66] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    207: f3 -> [69] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 && 0>=free_4 ], cost: INF
    208: f3 -> [70] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 && 0>=free_4 ], cost: INF
    209: f3 -> [71] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 && 0>=free_4 ], cost: INF
    210: f3 -> [72] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 && 0>=free_4 ], cost: INF
    212: f3 -> [73] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=-1+free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-1+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 ], cost: INF
    213: f3 -> [74] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=-1+free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-1+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 ], cost: INF
    214: f3 -> [75] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=-1+free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-1+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 ], cost: INF
    215: f3 -> [76] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=-1+free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-1+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 ], cost: INF
    217: f3 -> [77] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=free_4 ], cost: INF
    218: f3 -> [78] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=free_4 ], cost: INF
    219: f3 -> [79] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=free_4 ], cost: INF
    220: f3 -> [80] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=free_4 ], cost: INF
    221: f3 -> [81] : A'=7, B'=6, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=0, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-2+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, D6'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 && 1>=1 ], cost: INF


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f3
    222: f3 -> [58] : A'=9, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, D6'=1, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    223: f3 -> [58] : A'=9, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=-1+free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-1+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, D6'=1, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 && 1>=1 && 1>=1 ], cost: INF
    224: f3 -> [58] : A'=9, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, D6'=1, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    190: f3 -> [59] : A'=7, B'=4, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 ], cost: INF
    168: f3 -> [63] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 ], cost: INF
    191: f3 -> [64] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    192: f3 -> [65] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    193: f3 -> [66] : A'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 ], cost: INF
    207: f3 -> [69] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 && 0>=free_4 ], cost: INF
    208: f3 -> [70] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 && 0>=free_4 ], cost: INF
    209: f3 -> [71] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 && 0>=free_4 ], cost: INF
    210: f3 -> [72] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 && 0>=free_4 ], cost: INF
    212: f3 -> [73] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=-1+free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-1+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 ], cost: INF
    213: f3 -> [74] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=-1+free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-1+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 ], cost: INF
    214: f3 -> [75] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=-1+free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-1+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 ], cost: INF
    215: f3 -> [76] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=-1+free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-1+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 ], cost: INF
    217: f3 -> [77] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=free_4 ], cost: INF
    218: f3 -> [78] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=free_4 ], cost: INF
    219: f3 -> [79] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=free_4 ], cost: INF
    220: f3 -> [80] : A'=7, B'=7, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=1, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=free_4, H3'=free, Q3'=free_2, J3'=0, K3'=0, L3'=0, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=free_4 ], cost: INF
    221: f3 -> [81] : A'=7, B'=6, C'=0, D'=0, E'=free_5, F'=free_1, G'=free_3, H'=1, Q'=free_4, J'=free, K'=free_2, L'=0, F1'=1, B2'=free_5, C2'=free_1, D2'=7, E2'=free_3, F2'=1, G2'=free_4, H2'=free, Q2'=free_2, J2'=1, C3'=free_5, D3'=free_1, E3'=free_3, F3'=1, G3'=-2+free_4, H3'=free, Q3'=free_2, J3'=0, K3'=1, L3'=0, X3'=free_27, Y3'=free_5, Z3'=free_1, A4'=6, B4'=free_3, C4'=1, D4'=-1+free_4, E4'=free, F4'=free_2, P4'=free, Q4_1'=free_5, R4'=free_1, S4'=free_3, T4'=1, U4'=free_4, V4'=free_2, W4'=7, X4'=1, Y4'=0, J5'=0, T5'=0, D6'=0, [ 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && free_27>=1 && 0>=free_4 && 0>=-1+free_4 && 1>=1 ], cost: INF


Computing complexity for remaining 21 transitions.

Found new complexity INF, because: INF sat.


The final runtime is determined by this resulting transition:
  Final Guard: 0>=free && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=1 && 1>=1 && 0>=free && 0>=0 && 0>=free_26 && 0>=free_4 && 0>=free_4 && 1>=1 && 1>=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,?)