Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f155 -> f168 : A'=7, B'=7, [ A==7 ], cost: 1
      1: f155 -> f160 : B'=A, C'=A, D'=0, [ 6>=A ], cost: 1
      2: f155 -> f160 : B'=A, C'=A, D'=0, [ A>=8 ], cost: 1
     21: f168 -> f178 : B'=free_15, A1'=0, F1'=1, [ D1>=1+E1 ], cost: 1
     22: f168 -> f178 : B'=free_16, A1'=0, E1'=0, F1'=1, [ E1>=D1 ], cost: 1
     25: f160 -> f155 : A'=0, G'=D, H1'=free_18, Q1'=-1, [ D>=1 && 0>=F ], cost: 1
     26: f160 -> f155 : A'=0, G'=D, H1'=free_19, Q1'=-1, [ 0>=E && D>=1 && F>=1 ], cost: 1
     23: f160 -> f168 : G'=D, G1'=1, [ 0>=D ], cost: 1
      4: f160 -> f163 : G'=D, [ E>=1 && D>=1 && F>=1 ], cost: 1
      3: f163 -> f163 : [], cost: 1
      5: f186 -> f196 : B'=7, H'=free_2, Q'=free_4, J'=free, K'=L, M'=free_1, N'=free_3, O'=0, [ B==7 ], cost: 1
      8: f186 -> f120 : [ 6>=B ], cost: 1
      9: f186 -> f120 : [ B>=8 ], cost: 1
      6: f196 -> f209 : P'=O, Q_1'=free_5, R'=free_6, S'=free_6, [ 0>=O ], cost: 1
     17: f196 -> f209 : P'=O, Q_1'=free_9, R'=free_7, S'=free_7, W'=O, X'=free_8, Y'=O, [ O>=1 ], cost: 1
     11: f209 -> f213 : V'=S, [ 6>=S ], cost: 1
     12: f209 -> f213 : V'=S, [ S>=8 ], cost: 1
     10: f209 -> f120 : S'=7, U'=1, V'=7, [ S==7 ], cost: 1
      7: f213 -> f120 : T'=0, [ T==0 ], cost: 1
     13: f213 -> f120 : U'=1, [ 0>=1+T ], cost: 1
     14: f213 -> f120 : U'=1, [ T>=1 ], cost: 1
     33: f120 -> f219 : X1'=0, [ U>=1 ], cost: 1
     30: f120 -> f137 : Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 ], cost: 1
     31: f120 -> f137 : Q1_1'=free_25, R1'=free_26, S1'=1, T1'=0, U1'=1+U1, V1'=U1, [ P1>=1+U1 && 0>=U && P1>=1 ], cost: 1
     32: f120 -> f137 : Q1_1'=free_27, R1'=free_28, S1'=1, T1'=0, U1'=1+U1, V1'=U1, W1'=0, [ P1>=1 && 0>=U && U1>=P1 ], cost: 1
     15: f219 -> f219 : [], cost: 1
     16: f221 -> f223 : [], cost: 1
     18: f178 -> f186 : Z'=A1, B1'=A1, [ 3>=B ], cost: 1
     19: f178 -> f186 : Z'=A1, B1'=A1, [ B>=5 ], cost: 1
     20: f178 -> f196 : B'=4, H'=free_12, Q'=free_14, J'=free_10, K'=L, M'=free_11, N'=free_13, O'=0, Z'=A1, B1'=A1, C1'=1, [ B==4 ], cost: 1
     24: f165 -> f155 : A'=0, H1'=free_17, Q1'=-1, [], cost: 1
     27: f137 -> f155 : A'=0, H1'=free_20, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, [ 0>=J1 ], cost: 1
     28: f137 -> f155 : A'=0, H1'=free_21, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, [ J1>=2 ], cost: 1
     29: f137 -> f178 : B'=free_22, A1'=0, F1'=O1, J1'=1, K1'=0, L1'=0, M1'=0, N1'=0, [ J1==1 ], cost: 1
     35: f105 -> f120 : F2'=8, [ 0>=Y1 ], cost: 1
     34: f105 -> f105 : Y1'=-1+Y1, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=F1, E2'=free_29, [ Y1>=1 ], cost: 1
     36: f76 -> f105 : F1'=O1, J1'=free_30, Y1'=free_30, H2'=G2, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=L, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, [ free_30>=1 && 0>=G2 ], cost: 1
     37: f76 -> f105 : F1'=O1, J1'=free_36, Y1'=free_36, H2'=G2, Q2'=free_39, J2'=free_41, K2'=free_37, L2'=L, M2'=0, N2'=free_38, O2'=1, P2'=0, Q2_1'=J1, R2'=free_40, S2'=0, T2'=1, [ free_36>=1 && G2>=1 ], cost: 1
     38: f0 -> f76 : B'=7, L'=free_51, U'=0, E1'=0, K1'=0, O1'=free_56, U1'=0, F2'=9, G2'=0, U2'=free_51, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_46, D3'=free_46, E3'=free_46, F3'=free_50, G3'=free_55, H3'=free_44, Q3'=free_48, J3'=0, K3'=free_53, L3'=free_45, M3'=free_49, N3'=free_54, O3'=free_43, P3'=free_47, Q3_1'=0, R3'=0, S3'=free_52, T3'=free_42, U3'=7, V3'=7, [ free_51>=1 && free_56>=1 ], cost: 1
     39: f0 -> f76 : B'=free_62, L'=free_67, U'=0, E1'=0, K1'=0, O1'=free_72, U1'=0, F2'=9, G2'=0, U2'=free_67, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_61, D3'=free_61, E3'=free_61, F3'=free_66, G3'=free_71, H3'=free_59, Q3'=free_64, J3'=0, K3'=free_69, L3'=free_60, M3'=free_65, N3'=free_70, O3'=free_58, P3'=free_63, Q3_1'=0, R3'=0, S3'=free_68, T3'=free_57, U3'=free_62, V3'=free_62, W3'=1, [ 6>=free_62 && free_67>=1 && free_72>=1 ], cost: 1
     40: f0 -> f76 : B'=free_78, L'=free_83, U'=0, E1'=0, K1'=0, O1'=free_88, U1'=0, F2'=9, G2'=0, U2'=free_83, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_77, D3'=free_77, E3'=free_77, F3'=free_82, G3'=free_87, H3'=free_75, Q3'=free_80, J3'=0, K3'=free_85, L3'=free_76, M3'=free_81, N3'=free_86, O3'=free_74, P3'=free_79, Q3_1'=0, R3'=0, S3'=free_84, T3'=free_73, U3'=free_78, V3'=free_78, W3'=1, [ free_78>=8 && free_83>=1 && free_88>=1 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f155 -> f168 : A'=7, B'=7, [ A==7 ], cost: 1
      1: f155 -> f160 : B'=A, C'=A, D'=0, [ 6>=A ], cost: 1
      2: f155 -> f160 : B'=A, C'=A, D'=0, [ A>=8 ], cost: 1
     21: f168 -> f178 : B'=free_15, A1'=0, F1'=1, [ D1>=1+E1 ], cost: 1
     22: f168 -> f178 : B'=free_16, A1'=0, E1'=0, F1'=1, [ E1>=D1 ], cost: 1
     25: f160 -> f155 : A'=0, G'=D, H1'=free_18, Q1'=-1, [ D>=1 && 0>=F ], cost: 1
     26: f160 -> f155 : A'=0, G'=D, H1'=free_19, Q1'=-1, [ 0>=E && D>=1 && F>=1 ], cost: 1
     23: f160 -> f168 : G'=D, G1'=1, [ 0>=D ], cost: 1
      4: f160 -> f163 : G'=D, [ E>=1 && D>=1 && F>=1 ], cost: 1
      3: f163 -> f163 : [], cost: 1
      5: f186 -> f196 : B'=7, H'=free_2, Q'=free_4, J'=free, K'=L, M'=free_1, N'=free_3, O'=0, [ B==7 ], cost: 1
      8: f186 -> f120 : [ 6>=B ], cost: 1
      9: f186 -> f120 : [ B>=8 ], cost: 1
      6: f196 -> f209 : P'=O, Q_1'=free_5, R'=free_6, S'=free_6, [ 0>=O ], cost: 1
     17: f196 -> f209 : P'=O, Q_1'=free_9, R'=free_7, S'=free_7, W'=O, X'=free_8, Y'=O, [ O>=1 ], cost: 1
     11: f209 -> f213 : V'=S, [ 6>=S ], cost: 1
     12: f209 -> f213 : V'=S, [ S>=8 ], cost: 1
     10: f209 -> f120 : S'=7, U'=1, V'=7, [ S==7 ], cost: 1
      7: f213 -> f120 : T'=0, [ T==0 ], cost: 1
     13: f213 -> f120 : U'=1, [ 0>=1+T ], cost: 1
     14: f213 -> f120 : U'=1, [ T>=1 ], cost: 1
     33: f120 -> f219 : X1'=0, [ U>=1 ], cost: 1
     30: f120 -> f137 : Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 ], cost: 1
     31: f120 -> f137 : Q1_1'=free_25, R1'=free_26, S1'=1, T1'=0, U1'=1+U1, V1'=U1, [ P1>=1+U1 && 0>=U && P1>=1 ], cost: 1
     32: f120 -> f137 : Q1_1'=free_27, R1'=free_28, S1'=1, T1'=0, U1'=1+U1, V1'=U1, W1'=0, [ P1>=1 && 0>=U && U1>=P1 ], cost: 1
     15: f219 -> f219 : [], cost: 1
     18: f178 -> f186 : Z'=A1, B1'=A1, [ 3>=B ], cost: 1
     19: f178 -> f186 : Z'=A1, B1'=A1, [ B>=5 ], cost: 1
     20: f178 -> f196 : B'=4, H'=free_12, Q'=free_14, J'=free_10, K'=L, M'=free_11, N'=free_13, O'=0, Z'=A1, B1'=A1, C1'=1, [ B==4 ], cost: 1
     27: f137 -> f155 : A'=0, H1'=free_20, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, [ 0>=J1 ], cost: 1
     28: f137 -> f155 : A'=0, H1'=free_21, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, [ J1>=2 ], cost: 1
     29: f137 -> f178 : B'=free_22, A1'=0, F1'=O1, J1'=1, K1'=0, L1'=0, M1'=0, N1'=0, [ J1==1 ], cost: 1
     35: f105 -> f120 : F2'=8, [ 0>=Y1 ], cost: 1
     34: f105 -> f105 : Y1'=-1+Y1, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=F1, E2'=free_29, [ Y1>=1 ], cost: 1
     36: f76 -> f105 : F1'=O1, J1'=free_30, Y1'=free_30, H2'=G2, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=L, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, [ free_30>=1 && 0>=G2 ], cost: 1
     37: f76 -> f105 : F1'=O1, J1'=free_36, Y1'=free_36, H2'=G2, Q2'=free_39, J2'=free_41, K2'=free_37, L2'=L, M2'=0, N2'=free_38, O2'=1, P2'=0, Q2_1'=J1, R2'=free_40, S2'=0, T2'=1, [ free_36>=1 && G2>=1 ], cost: 1
     38: f0 -> f76 : B'=7, L'=free_51, U'=0, E1'=0, K1'=0, O1'=free_56, U1'=0, F2'=9, G2'=0, U2'=free_51, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_46, D3'=free_46, E3'=free_46, F3'=free_50, G3'=free_55, H3'=free_44, Q3'=free_48, J3'=0, K3'=free_53, L3'=free_45, M3'=free_49, N3'=free_54, O3'=free_43, P3'=free_47, Q3_1'=0, R3'=0, S3'=free_52, T3'=free_42, U3'=7, V3'=7, [ free_51>=1 && free_56>=1 ], cost: 1
     39: f0 -> f76 : B'=free_62, L'=free_67, U'=0, E1'=0, K1'=0, O1'=free_72, U1'=0, F2'=9, G2'=0, U2'=free_67, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_61, D3'=free_61, E3'=free_61, F3'=free_66, G3'=free_71, H3'=free_59, Q3'=free_64, J3'=0, K3'=free_69, L3'=free_60, M3'=free_65, N3'=free_70, O3'=free_58, P3'=free_63, Q3_1'=0, R3'=0, S3'=free_68, T3'=free_57, U3'=free_62, V3'=free_62, W3'=1, [ 6>=free_62 && free_67>=1 && free_72>=1 ], cost: 1
     40: f0 -> f76 : B'=free_78, L'=free_83, U'=0, E1'=0, K1'=0, O1'=free_88, U1'=0, F2'=9, G2'=0, U2'=free_83, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_77, D3'=free_77, E3'=free_77, F3'=free_82, G3'=free_87, H3'=free_75, Q3'=free_80, J3'=0, K3'=free_85, L3'=free_76, M3'=free_81, N3'=free_86, O3'=free_74, P3'=free_79, Q3_1'=0, R3'=0, S3'=free_84, T3'=free_73, U3'=free_78, V3'=free_78, W3'=1, [ free_78>=8 && free_83>=1 && free_88>=1 ], cost: 1

Eliminating 1 self-loops for location f163
  Self-Loop 3 has unbounded runtime, resulting in the new transition 41.
  Removing the self-loops: 3.
Eliminating 1 self-loops for location f219
  Self-Loop 15 has unbounded runtime, resulting in the new transition 42.
  Removing the self-loops: 15.
Eliminating 1 self-loops for location f105
  Self-Loop 34 has the metering function: Y1, resulting in the new transition 43.
  Removing the self-loops: 34.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f155 -> f168 : A'=7, B'=7, [ A==7 ], cost: 1
      1: f155 -> f160 : B'=A, C'=A, D'=0, [ 6>=A ], cost: 1
      2: f155 -> f160 : B'=A, C'=A, D'=0, [ A>=8 ], cost: 1
     21: f168 -> f178 : B'=free_15, A1'=0, F1'=1, [ D1>=1+E1 ], cost: 1
     22: f168 -> f178 : B'=free_16, A1'=0, E1'=0, F1'=1, [ E1>=D1 ], cost: 1
     25: f160 -> f155 : A'=0, G'=D, H1'=free_18, Q1'=-1, [ D>=1 && 0>=F ], cost: 1
     26: f160 -> f155 : A'=0, G'=D, H1'=free_19, Q1'=-1, [ 0>=E && D>=1 && F>=1 ], cost: 1
     23: f160 -> f168 : G'=D, G1'=1, [ 0>=D ], cost: 1
      4: f160 -> f163 : G'=D, [ E>=1 && D>=1 && F>=1 ], cost: 1
     41: f163 -> [18] : [], cost: INF
      5: f186 -> f196 : B'=7, H'=free_2, Q'=free_4, J'=free, K'=L, M'=free_1, N'=free_3, O'=0, [ B==7 ], cost: 1
      8: f186 -> f120 : [ 6>=B ], cost: 1
      9: f186 -> f120 : [ B>=8 ], cost: 1
      6: f196 -> f209 : P'=O, Q_1'=free_5, R'=free_6, S'=free_6, [ 0>=O ], cost: 1
     17: f196 -> f209 : P'=O, Q_1'=free_9, R'=free_7, S'=free_7, W'=O, X'=free_8, Y'=O, [ O>=1 ], cost: 1
     11: f209 -> f213 : V'=S, [ 6>=S ], cost: 1
     12: f209 -> f213 : V'=S, [ S>=8 ], cost: 1
     10: f209 -> f120 : S'=7, U'=1, V'=7, [ S==7 ], cost: 1
      7: f213 -> f120 : T'=0, [ T==0 ], cost: 1
     13: f213 -> f120 : U'=1, [ 0>=1+T ], cost: 1
     14: f213 -> f120 : U'=1, [ T>=1 ], cost: 1
     33: f120 -> f219 : X1'=0, [ U>=1 ], cost: 1
     30: f120 -> f137 : Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 ], cost: 1
     31: f120 -> f137 : Q1_1'=free_25, R1'=free_26, S1'=1, T1'=0, U1'=1+U1, V1'=U1, [ P1>=1+U1 && 0>=U && P1>=1 ], cost: 1
     32: f120 -> f137 : Q1_1'=free_27, R1'=free_28, S1'=1, T1'=0, U1'=1+U1, V1'=U1, W1'=0, [ P1>=1 && 0>=U && U1>=P1 ], cost: 1
     42: f219 -> [19] : [], cost: INF
     18: f178 -> f186 : Z'=A1, B1'=A1, [ 3>=B ], cost: 1
     19: f178 -> f186 : Z'=A1, B1'=A1, [ B>=5 ], cost: 1
     20: f178 -> f196 : B'=4, H'=free_12, Q'=free_14, J'=free_10, K'=L, M'=free_11, N'=free_13, O'=0, Z'=A1, B1'=A1, C1'=1, [ B==4 ], cost: 1
     27: f137 -> f155 : A'=0, H1'=free_20, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, [ 0>=J1 ], cost: 1
     28: f137 -> f155 : A'=0, H1'=free_21, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, [ J1>=2 ], cost: 1
     29: f137 -> f178 : B'=free_22, A1'=0, F1'=O1, J1'=1, K1'=0, L1'=0, M1'=0, N1'=0, [ J1==1 ], cost: 1
     43: f105 -> [20] : Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=F1, E2'=free_29, [ Y1>=1 ], cost: Y1
     36: f76 -> f105 : F1'=O1, J1'=free_30, Y1'=free_30, H2'=G2, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=L, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, [ free_30>=1 && 0>=G2 ], cost: 1
     37: f76 -> f105 : F1'=O1, J1'=free_36, Y1'=free_36, H2'=G2, Q2'=free_39, J2'=free_41, K2'=free_37, L2'=L, M2'=0, N2'=free_38, O2'=1, P2'=0, Q2_1'=J1, R2'=free_40, S2'=0, T2'=1, [ free_36>=1 && G2>=1 ], cost: 1
     38: f0 -> f76 : B'=7, L'=free_51, U'=0, E1'=0, K1'=0, O1'=free_56, U1'=0, F2'=9, G2'=0, U2'=free_51, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_46, D3'=free_46, E3'=free_46, F3'=free_50, G3'=free_55, H3'=free_44, Q3'=free_48, J3'=0, K3'=free_53, L3'=free_45, M3'=free_49, N3'=free_54, O3'=free_43, P3'=free_47, Q3_1'=0, R3'=0, S3'=free_52, T3'=free_42, U3'=7, V3'=7, [ free_51>=1 && free_56>=1 ], cost: 1
     39: f0 -> f76 : B'=free_62, L'=free_67, U'=0, E1'=0, K1'=0, O1'=free_72, U1'=0, F2'=9, G2'=0, U2'=free_67, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_61, D3'=free_61, E3'=free_61, F3'=free_66, G3'=free_71, H3'=free_59, Q3'=free_64, J3'=0, K3'=free_69, L3'=free_60, M3'=free_65, N3'=free_70, O3'=free_58, P3'=free_63, Q3_1'=0, R3'=0, S3'=free_68, T3'=free_57, U3'=free_62, V3'=free_62, W3'=1, [ 6>=free_62 && free_67>=1 && free_72>=1 ], cost: 1
     40: f0 -> f76 : B'=free_78, L'=free_83, U'=0, E1'=0, K1'=0, O1'=free_88, U1'=0, F2'=9, G2'=0, U2'=free_83, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_77, D3'=free_77, E3'=free_77, F3'=free_82, G3'=free_87, H3'=free_75, Q3'=free_80, J3'=0, K3'=free_85, L3'=free_76, M3'=free_81, N3'=free_86, O3'=free_74, P3'=free_79, Q3_1'=0, R3'=0, S3'=free_84, T3'=free_73, U3'=free_78, V3'=free_78, W3'=1, [ free_78>=8 && free_83>=1 && free_88>=1 ], cost: 1
     35: [20] -> f120 : F2'=8, [ 0>=Y1 ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f155 -> f168 : A'=7, B'=7, [ A==7 ], cost: 1
      1: f155 -> f160 : B'=A, C'=A, D'=0, [ 6>=A ], cost: 1
      2: f155 -> f160 : B'=A, C'=A, D'=0, [ A>=8 ], cost: 1
     21: f168 -> f178 : B'=free_15, A1'=0, F1'=1, [ D1>=1+E1 ], cost: 1
     22: f168 -> f178 : B'=free_16, A1'=0, E1'=0, F1'=1, [ E1>=D1 ], cost: 1
     25: f160 -> f155 : A'=0, G'=D, H1'=free_18, Q1'=-1, [ D>=1 && 0>=F ], cost: 1
     26: f160 -> f155 : A'=0, G'=D, H1'=free_19, Q1'=-1, [ 0>=E && D>=1 && F>=1 ], cost: 1
     23: f160 -> f168 : G'=D, G1'=1, [ 0>=D ], cost: 1
      4: f160 -> [18] : G'=D, [ E>=1 && D>=1 && F>=1 ], cost: INF
      5: f186 -> f196 : B'=7, H'=free_2, Q'=free_4, J'=free, K'=L, M'=free_1, N'=free_3, O'=0, [ B==7 ], cost: 1
      8: f186 -> f120 : [ 6>=B ], cost: 1
      9: f186 -> f120 : [ B>=8 ], cost: 1
      6: f196 -> f209 : P'=O, Q_1'=free_5, R'=free_6, S'=free_6, [ 0>=O ], cost: 1
     17: f196 -> f209 : P'=O, Q_1'=free_9, R'=free_7, S'=free_7, W'=O, X'=free_8, Y'=O, [ O>=1 ], cost: 1
     11: f209 -> f213 : V'=S, [ 6>=S ], cost: 1
     12: f209 -> f213 : V'=S, [ S>=8 ], cost: 1
     10: f209 -> f120 : S'=7, U'=1, V'=7, [ S==7 ], cost: 1
      7: f213 -> f120 : T'=0, [ T==0 ], cost: 1
     13: f213 -> f120 : U'=1, [ 0>=1+T ], cost: 1
     14: f213 -> f120 : U'=1, [ T>=1 ], cost: 1
     30: f120 -> f137 : Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 ], cost: 1
     31: f120 -> f137 : Q1_1'=free_25, R1'=free_26, S1'=1, T1'=0, U1'=1+U1, V1'=U1, [ P1>=1+U1 && 0>=U && P1>=1 ], cost: 1
     32: f120 -> f137 : Q1_1'=free_27, R1'=free_28, S1'=1, T1'=0, U1'=1+U1, V1'=U1, W1'=0, [ P1>=1 && 0>=U && U1>=P1 ], cost: 1
     33: f120 -> [19] : X1'=0, [ U>=1 ], cost: INF
     18: f178 -> f186 : Z'=A1, B1'=A1, [ 3>=B ], cost: 1
     19: f178 -> f186 : Z'=A1, B1'=A1, [ B>=5 ], cost: 1
     20: f178 -> f196 : B'=4, H'=free_12, Q'=free_14, J'=free_10, K'=L, M'=free_11, N'=free_13, O'=0, Z'=A1, B1'=A1, C1'=1, [ B==4 ], cost: 1
     27: f137 -> f155 : A'=0, H1'=free_20, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, [ 0>=J1 ], cost: 1
     28: f137 -> f155 : A'=0, H1'=free_21, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, [ J1>=2 ], cost: 1
     29: f137 -> f178 : B'=free_22, A1'=0, F1'=O1, J1'=1, K1'=0, L1'=0, M1'=0, N1'=0, [ J1==1 ], cost: 1
     43: f105 -> f120 : Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=F1, E2'=free_29, F2'=8, [ Y1>=1 && 0>=0 ], cost: 1+Y1
     36: f76 -> f105 : F1'=O1, J1'=free_30, Y1'=free_30, H2'=G2, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=L, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, [ free_30>=1 && 0>=G2 ], cost: 1
     37: f76 -> f105 : F1'=O1, J1'=free_36, Y1'=free_36, H2'=G2, Q2'=free_39, J2'=free_41, K2'=free_37, L2'=L, M2'=0, N2'=free_38, O2'=1, P2'=0, Q2_1'=J1, R2'=free_40, S2'=0, T2'=1, [ free_36>=1 && G2>=1 ], cost: 1
     38: f0 -> f76 : B'=7, L'=free_51, U'=0, E1'=0, K1'=0, O1'=free_56, U1'=0, F2'=9, G2'=0, U2'=free_51, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_46, D3'=free_46, E3'=free_46, F3'=free_50, G3'=free_55, H3'=free_44, Q3'=free_48, J3'=0, K3'=free_53, L3'=free_45, M3'=free_49, N3'=free_54, O3'=free_43, P3'=free_47, Q3_1'=0, R3'=0, S3'=free_52, T3'=free_42, U3'=7, V3'=7, [ free_51>=1 && free_56>=1 ], cost: 1
     39: f0 -> f76 : B'=free_62, L'=free_67, U'=0, E1'=0, K1'=0, O1'=free_72, U1'=0, F2'=9, G2'=0, U2'=free_67, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_61, D3'=free_61, E3'=free_61, F3'=free_66, G3'=free_71, H3'=free_59, Q3'=free_64, J3'=0, K3'=free_69, L3'=free_60, M3'=free_65, N3'=free_70, O3'=free_58, P3'=free_63, Q3_1'=0, R3'=0, S3'=free_68, T3'=free_57, U3'=free_62, V3'=free_62, W3'=1, [ 6>=free_62 && free_67>=1 && free_72>=1 ], cost: 1
     40: f0 -> f76 : B'=free_78, L'=free_83, U'=0, E1'=0, K1'=0, O1'=free_88, U1'=0, F2'=9, G2'=0, U2'=free_83, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_77, D3'=free_77, E3'=free_77, F3'=free_82, G3'=free_87, H3'=free_75, Q3'=free_80, J3'=0, K3'=free_85, L3'=free_76, M3'=free_81, N3'=free_86, O3'=free_74, P3'=free_79, Q3_1'=0, R3'=0, S3'=free_84, T3'=free_73, U3'=free_78, V3'=free_78, W3'=1, [ free_78>=8 && free_83>=1 && free_88>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f155 -> f168 : A'=7, B'=7, [ A==7 ], cost: 1
     56: f155 -> f168 : B'=A, C'=A, D'=0, G'=0, G1'=1, [ 6>=A && 0>=0 ], cost: 2
     57: f155 -> f168 : B'=A, C'=A, D'=0, G'=0, G1'=1, [ A>=8 && 0>=0 ], cost: 2
     21: f168 -> f178 : B'=free_15, A1'=0, F1'=1, [ D1>=1+E1 ], cost: 1
     22: f168 -> f178 : B'=free_16, A1'=0, E1'=0, F1'=1, [ E1>=D1 ], cost: 1
     62: f196 -> f213 : P'=O, Q_1'=free_5, R'=free_6, S'=free_6, V'=free_6, [ 0>=O && 6>=free_6 ], cost: 2
     63: f196 -> f213 : P'=O, Q_1'=free_5, R'=free_6, S'=free_6, V'=free_6, [ 0>=O && free_6>=8 ], cost: 2
     65: f196 -> f213 : P'=O, Q_1'=free_9, R'=free_7, S'=free_7, V'=free_7, W'=O, X'=free_8, Y'=O, [ O>=1 && 6>=free_7 ], cost: 2
     66: f196 -> f213 : P'=O, Q_1'=free_9, R'=free_7, S'=free_7, V'=free_7, W'=O, X'=free_8, Y'=O, [ O>=1 && free_7>=8 ], cost: 2
     64: f196 -> f120 : P'=O, Q_1'=free_5, R'=free_6, S'=7, U'=1, V'=7, [ 0>=O && free_6==7 ], cost: 2
     67: f196 -> f120 : P'=O, Q_1'=free_9, R'=free_7, S'=7, U'=1, V'=7, W'=O, X'=free_8, Y'=O, [ O>=1 && free_7==7 ], cost: 2
      7: f213 -> f120 : T'=0, [ T==0 ], cost: 1
     13: f213 -> f120 : U'=1, [ 0>=1+T ], cost: 1
     14: f213 -> f120 : U'=1, [ T>=1 ], cost: 1
     47: f120 -> f155 : A'=0, H1'=free_20, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 && 0>=J1 ], cost: 2
     48: f120 -> f155 : A'=0, H1'=free_21, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 && J1>=2 ], cost: 2
     50: f120 -> f155 : A'=0, H1'=free_20, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_25, R1'=free_26, S1'=1, T1'=0, U1'=1+U1, V1'=U1, [ P1>=1+U1 && 0>=U && P1>=1 && 0>=J1 ], cost: 2
     51: f120 -> f155 : A'=0, H1'=free_21, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_25, R1'=free_26, S1'=1, T1'=0, U1'=1+U1, V1'=U1, [ P1>=1+U1 && 0>=U && P1>=1 && J1>=2 ], cost: 2
     54: f120 -> f155 : A'=0, H1'=free_21, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_27, R1'=free_28, S1'=1, T1'=0, U1'=1+U1, V1'=U1, W1'=0, [ P1>=1 && 0>=U && U1>=P1 && J1>=2 ], cost: 2
     49: f120 -> f178 : B'=free_22, A1'=0, F1'=O1, J1'=1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 && J1==1 ], cost: 2
     52: f120 -> f178 : B'=free_22, A1'=0, F1'=O1, J1'=1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_25, R1'=free_26, S1'=1, T1'=0, U1'=1+U1, V1'=U1, [ P1>=1+U1 && 0>=U && P1>=1 && J1==1 ], cost: 2
     55: f120 -> f178 : B'=free_22, A1'=0, F1'=O1, J1'=1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_27, R1'=free_28, S1'=1, T1'=0, U1'=1+U1, V1'=U1, W1'=0, [ P1>=1 && 0>=U && U1>=P1 && J1==1 ], cost: 2
     33: f120 -> [19] : X1'=0, [ U>=1 ], cost: INF
     20: f178 -> f196 : B'=4, H'=free_12, Q'=free_14, J'=free_10, K'=L, M'=free_11, N'=free_13, O'=0, Z'=A1, B1'=A1, C1'=1, [ B==4 ], cost: 1
     59: f178 -> f196 : B'=7, H'=free_2, Q'=free_4, J'=free, K'=L, M'=free_1, N'=free_3, O'=0, Z'=A1, B1'=A1, [ B>=5 && B==7 ], cost: 2
     58: f178 -> f120 : Z'=A1, B1'=A1, [ 3>=B && 6>=B ], cost: 2
     60: f178 -> f120 : Z'=A1, B1'=A1, [ B>=5 && 6>=B ], cost: 2
     61: f178 -> f120 : Z'=A1, B1'=A1, [ B>=5 && B>=8 ], cost: 2
     43: f105 -> f120 : Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=F1, E2'=free_29, F2'=8, [ Y1>=1 && 0>=0 ], cost: 1+Y1
     44: f0 -> f105 : B'=7, L'=free_51, U'=0, E1'=0, F1'=free_56, J1'=free_30, K1'=0, O1'=free_56, U1'=0, Y1'=free_30, F2'=9, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_51, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_51, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_46, D3'=free_46, E3'=free_46, F3'=free_50, G3'=free_55, H3'=free_44, Q3'=free_48, J3'=0, K3'=free_53, L3'=free_45, M3'=free_49, N3'=free_54, O3'=free_43, P3'=free_47, Q3_1'=0, R3'=0, S3'=free_52, T3'=free_42, U3'=7, V3'=7, [ free_51>=1 && free_56>=1 && free_30>=1 && 0>=0 ], cost: 2
     45: f0 -> f105 : B'=free_62, L'=free_67, U'=0, E1'=0, F1'=free_72, J1'=free_30, K1'=0, O1'=free_72, U1'=0, Y1'=free_30, F2'=9, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_67, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_67, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_61, D3'=free_61, E3'=free_61, F3'=free_66, G3'=free_71, H3'=free_59, Q3'=free_64, J3'=0, K3'=free_69, L3'=free_60, M3'=free_65, N3'=free_70, O3'=free_58, P3'=free_63, Q3_1'=0, R3'=0, S3'=free_68, T3'=free_57, U3'=free_62, V3'=free_62, W3'=1, [ 6>=free_62 && free_67>=1 && free_72>=1 && free_30>=1 && 0>=0 ], cost: 2
     46: f0 -> f105 : B'=free_78, L'=free_83, U'=0, E1'=0, F1'=free_88, J1'=free_30, K1'=0, O1'=free_88, U1'=0, Y1'=free_30, F2'=9, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_83, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_83, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_77, D3'=free_77, E3'=free_77, F3'=free_82, G3'=free_87, H3'=free_75, Q3'=free_80, J3'=0, K3'=free_85, L3'=free_76, M3'=free_81, N3'=free_86, O3'=free_74, P3'=free_79, Q3_1'=0, R3'=0, S3'=free_84, T3'=free_73, U3'=free_78, V3'=free_78, W3'=1, [ free_78>=8 && free_83>=1 && free_88>=1 && free_30>=1 && 0>=0 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
     21: f168 -> f178 : B'=free_15, A1'=0, F1'=1, [ D1>=1+E1 ], cost: 1
     22: f168 -> f178 : B'=free_16, A1'=0, E1'=0, F1'=1, [ E1>=D1 ], cost: 1
      7: f213 -> f120 : T'=0, [ T==0 ], cost: 1
     13: f213 -> f120 : U'=1, [ 0>=1+T ], cost: 1
     14: f213 -> f120 : U'=1, [ T>=1 ], cost: 1
     71: f120 -> f168 : A'=0, B'=0, C'=0, D'=0, G'=0, G1'=1, H1'=free_20, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 && 0>=J1 && 6>=0 && 0>=0 ], cost: 4
     72: f120 -> f168 : A'=0, B'=0, C'=0, D'=0, G'=0, G1'=1, H1'=free_21, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 && J1>=2 && 6>=0 && 0>=0 ], cost: 4
     73: f120 -> f168 : A'=0, B'=0, C'=0, D'=0, G'=0, G1'=1, H1'=free_20, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_25, R1'=free_26, S1'=1, T1'=0, U1'=1+U1, V1'=U1, [ P1>=1+U1 && 0>=U && P1>=1 && 0>=J1 && 6>=0 && 0>=0 ], cost: 4
     74: f120 -> f168 : A'=0, B'=0, C'=0, D'=0, G'=0, G1'=1, H1'=free_21, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_25, R1'=free_26, S1'=1, T1'=0, U1'=1+U1, V1'=U1, [ P1>=1+U1 && 0>=U && P1>=1 && J1>=2 && 6>=0 && 0>=0 ], cost: 4
     75: f120 -> f168 : A'=0, B'=0, C'=0, D'=0, G'=0, G1'=1, H1'=free_21, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_27, R1'=free_28, S1'=1, T1'=0, U1'=1+U1, V1'=U1, W1'=0, [ P1>=1 && 0>=U && U1>=P1 && J1>=2 && 6>=0 && 0>=0 ], cost: 4
     49: f120 -> f178 : B'=free_22, A1'=0, F1'=O1, J1'=1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 && J1==1 ], cost: 2
     52: f120 -> f178 : B'=free_22, A1'=0, F1'=O1, J1'=1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_25, R1'=free_26, S1'=1, T1'=0, U1'=1+U1, V1'=U1, [ P1>=1+U1 && 0>=U && P1>=1 && J1==1 ], cost: 2
     55: f120 -> f178 : B'=free_22, A1'=0, F1'=O1, J1'=1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_27, R1'=free_28, S1'=1, T1'=0, U1'=1+U1, V1'=U1, W1'=0, [ P1>=1 && 0>=U && U1>=P1 && J1==1 ], cost: 2
     33: f120 -> [19] : X1'=0, [ U>=1 ], cost: INF
     76: f178 -> f213 : B'=4, H'=free_12, Q'=free_14, J'=free_10, K'=L, M'=free_11, N'=free_13, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, V'=free_6, Z'=A1, B1'=A1, C1'=1, [ B==4 && 0>=0 && 6>=free_6 ], cost: 3
     77: f178 -> f213 : B'=4, H'=free_12, Q'=free_14, J'=free_10, K'=L, M'=free_11, N'=free_13, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, V'=free_6, Z'=A1, B1'=A1, C1'=1, [ B==4 && 0>=0 && free_6>=8 ], cost: 3
     79: f178 -> f213 : B'=7, H'=free_2, Q'=free_4, J'=free, K'=L, M'=free_1, N'=free_3, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, V'=free_6, Z'=A1, B1'=A1, [ B>=5 && B==7 && 0>=0 && 6>=free_6 ], cost: 4
     80: f178 -> f213 : B'=7, H'=free_2, Q'=free_4, J'=free, K'=L, M'=free_1, N'=free_3, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, V'=free_6, Z'=A1, B1'=A1, [ B>=5 && B==7 && 0>=0 && free_6>=8 ], cost: 4
     58: f178 -> f120 : Z'=A1, B1'=A1, [ 3>=B && 6>=B ], cost: 2
     60: f178 -> f120 : Z'=A1, B1'=A1, [ B>=5 && 6>=B ], cost: 2
     61: f178 -> f120 : Z'=A1, B1'=A1, [ B>=5 && B>=8 ], cost: 2
     78: f178 -> f120 : B'=4, H'=free_12, Q'=free_14, J'=free_10, K'=L, M'=free_11, N'=free_13, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=7, U'=1, V'=7, Z'=A1, B1'=A1, C1'=1, [ B==4 && 0>=0 && free_6==7 ], cost: 3
     81: f178 -> f120 : B'=7, H'=free_2, Q'=free_4, J'=free, K'=L, M'=free_1, N'=free_3, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=7, U'=1, V'=7, Z'=A1, B1'=A1, [ B>=5 && B==7 && 0>=0 && free_6==7 ], cost: 4
     68: f0 -> f120 : B'=7, L'=free_51, U'=0, E1'=0, F1'=free_56, J1'=free_30, K1'=0, O1'=free_56, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_56, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_51, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_51, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_46, D3'=free_46, E3'=free_46, F3'=free_50, G3'=free_55, H3'=free_44, Q3'=free_48, J3'=0, K3'=free_53, L3'=free_45, M3'=free_49, N3'=free_54, O3'=free_43, P3'=free_47, Q3_1'=0, R3'=0, S3'=free_52, T3'=free_42, U3'=7, V3'=7, [ free_51>=1 && free_56>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
     69: f0 -> f120 : B'=free_62, L'=free_67, U'=0, E1'=0, F1'=free_72, J1'=free_30, K1'=0, O1'=free_72, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_72, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_67, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_67, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_61, D3'=free_61, E3'=free_61, F3'=free_66, G3'=free_71, H3'=free_59, Q3'=free_64, J3'=0, K3'=free_69, L3'=free_60, M3'=free_65, N3'=free_70, O3'=free_58, P3'=free_63, Q3_1'=0, R3'=0, S3'=free_68, T3'=free_57, U3'=free_62, V3'=free_62, W3'=1, [ 6>=free_62 && free_67>=1 && free_72>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
     70: f0 -> f120 : B'=free_78, L'=free_83, U'=0, E1'=0, F1'=free_88, J1'=free_30, K1'=0, O1'=free_88, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_88, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_83, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_83, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_77, D3'=free_77, E3'=free_77, F3'=free_82, G3'=free_87, H3'=free_75, Q3'=free_80, J3'=0, K3'=free_85, L3'=free_76, M3'=free_81, N3'=free_86, O3'=free_74, P3'=free_79, Q3_1'=0, R3'=0, S3'=free_84, T3'=free_73, U3'=free_78, V3'=free_78, W3'=1, [ free_78>=8 && free_83>=1 && free_88>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30


Applied chaining over branches and pruning:
  Start location: f0
     49: f120 -> f178 : B'=free_22, A1'=0, F1'=O1, J1'=1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 && J1==1 ], cost: 2
     52: f120 -> f178 : B'=free_22, A1'=0, F1'=O1, J1'=1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_25, R1'=free_26, S1'=1, T1'=0, U1'=1+U1, V1'=U1, [ P1>=1+U1 && 0>=U && P1>=1 && J1==1 ], cost: 2
     82: f120 -> f178 : A'=0, B'=free_15, C'=0, D'=0, G'=0, A1'=0, F1'=1, G1'=1, H1'=free_20, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 && 0>=J1 && 6>=0 && 0>=0 && D1>=1+E1 ], cost: 5
     85: f120 -> f178 : A'=0, B'=free_16, C'=0, D'=0, G'=0, A1'=0, E1'=0, F1'=1, G1'=1, H1'=free_21, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 && J1>=2 && 6>=0 && 0>=0 && E1>=D1 ], cost: 5
     86: f120 -> f178 : A'=0, B'=free_15, C'=0, D'=0, G'=0, A1'=0, F1'=1, G1'=1, H1'=free_20, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_25, R1'=free_26, S1'=1, T1'=0, U1'=1+U1, V1'=U1, [ P1>=1+U1 && 0>=U && P1>=1 && 0>=J1 && 6>=0 && 0>=0 && D1>=1+E1 ], cost: 5
     33: f120 -> [19] : X1'=0, [ U>=1 ], cost: INF
     58: f178 -> f120 : Z'=A1, B1'=A1, [ 3>=B && 6>=B ], cost: 2
     60: f178 -> f120 : Z'=A1, B1'=A1, [ B>=5 && 6>=B ], cost: 2
     78: f178 -> f120 : B'=4, H'=free_12, Q'=free_14, J'=free_10, K'=L, M'=free_11, N'=free_13, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=7, U'=1, V'=7, Z'=A1, B1'=A1, C1'=1, [ B==4 && 0>=0 && free_6==7 ], cost: 3
     94: f178 -> f120 : B'=4, H'=free_12, Q'=free_14, J'=free_10, K'=L, M'=free_11, N'=free_13, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, U'=1, V'=free_6, Z'=A1, B1'=A1, C1'=1, [ B==4 && 0>=0 && 6>=free_6 && T>=1 ], cost: 4
     95: f178 -> f120 : B'=4, H'=free_12, Q'=free_14, J'=free_10, K'=L, M'=free_11, N'=free_13, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, T'=0, V'=free_6, Z'=A1, B1'=A1, C1'=1, [ B==4 && 0>=0 && free_6>=8 && T==0 ], cost: 4
     68: f0 -> f120 : B'=7, L'=free_51, U'=0, E1'=0, F1'=free_56, J1'=free_30, K1'=0, O1'=free_56, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_56, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_51, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_51, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_46, D3'=free_46, E3'=free_46, F3'=free_50, G3'=free_55, H3'=free_44, Q3'=free_48, J3'=0, K3'=free_53, L3'=free_45, M3'=free_49, N3'=free_54, O3'=free_43, P3'=free_47, Q3_1'=0, R3'=0, S3'=free_52, T3'=free_42, U3'=7, V3'=7, [ free_51>=1 && free_56>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
     69: f0 -> f120 : B'=free_62, L'=free_67, U'=0, E1'=0, F1'=free_72, J1'=free_30, K1'=0, O1'=free_72, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_72, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_67, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_67, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_61, D3'=free_61, E3'=free_61, F3'=free_66, G3'=free_71, H3'=free_59, Q3'=free_64, J3'=0, K3'=free_69, L3'=free_60, M3'=free_65, N3'=free_70, O3'=free_58, P3'=free_63, Q3_1'=0, R3'=0, S3'=free_68, T3'=free_57, U3'=free_62, V3'=free_62, W3'=1, [ 6>=free_62 && free_67>=1 && free_72>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
     70: f0 -> f120 : B'=free_78, L'=free_83, U'=0, E1'=0, F1'=free_88, J1'=free_30, K1'=0, O1'=free_88, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_88, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_83, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_83, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_77, D3'=free_77, E3'=free_77, F3'=free_82, G3'=free_87, H3'=free_75, Q3'=free_80, J3'=0, K3'=free_85, L3'=free_76, M3'=free_81, N3'=free_86, O3'=free_74, P3'=free_79, Q3_1'=0, R3'=0, S3'=free_84, T3'=free_73, U3'=free_78, V3'=free_78, W3'=1, [ free_78>=8 && free_83>=1 && free_88>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30


Applied chaining over branches and pruning:
  Start location: f0
    104: f120 -> f120 : B'=free_22, Z'=0, A1'=0, B1'=0, F1'=O1, J1'=1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 && J1==1 && 3>=free_22 && 6>=free_22 ], cost: 4
    105: f120 -> f120 : B'=free_22, Z'=0, A1'=0, B1'=0, F1'=O1, J1'=1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 && J1==1 && free_22>=5 && 6>=free_22 ], cost: 4
    107: f120 -> f120 : B'=4, H'=free_12, Q'=free_14, J'=free_10, K'=L, M'=free_11, N'=free_13, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, U'=1, V'=free_6, Z'=0, A1'=0, B1'=0, C1'=1, F1'=O1, J1'=1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 && J1==1 && free_22==4 && 0>=0 && 6>=free_6 && T>=1 ], cost: 6
    111: f120 -> f120 : B'=4, H'=free_12, Q'=free_14, J'=free_10, K'=L, M'=free_11, N'=free_13, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=7, U'=1, V'=7, Z'=0, A1'=0, B1'=0, C1'=1, F1'=O1, J1'=1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_25, R1'=free_26, S1'=1, T1'=0, U1'=1+U1, V1'=U1, [ P1>=1+U1 && 0>=U && P1>=1 && J1==1 && free_22==4 && 0>=0 && free_6==7 ], cost: 5
    116: f120 -> f120 : A'=0, B'=4, C'=0, D'=0, G'=0, H'=free_12, Q'=free_14, J'=free_10, K'=L, M'=free_11, N'=free_13, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=7, U'=1, V'=7, Z'=0, A1'=0, B1'=0, C1'=1, F1'=1, G1'=1, H1'=free_20, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 && 0>=J1 && 6>=0 && 0>=0 && D1>=1+E1 && free_15==4 && 0>=0 && free_6==7 ], cost: 8
     33: f120 -> [19] : X1'=0, [ U>=1 ], cost: INF
     68: f0 -> f120 : B'=7, L'=free_51, U'=0, E1'=0, F1'=free_56, J1'=free_30, K1'=0, O1'=free_56, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_56, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_51, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_51, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_46, D3'=free_46, E3'=free_46, F3'=free_50, G3'=free_55, H3'=free_44, Q3'=free_48, J3'=0, K3'=free_53, L3'=free_45, M3'=free_49, N3'=free_54, O3'=free_43, P3'=free_47, Q3_1'=0, R3'=0, S3'=free_52, T3'=free_42, U3'=7, V3'=7, [ free_51>=1 && free_56>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
     69: f0 -> f120 : B'=free_62, L'=free_67, U'=0, E1'=0, F1'=free_72, J1'=free_30, K1'=0, O1'=free_72, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_72, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_67, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_67, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_61, D3'=free_61, E3'=free_61, F3'=free_66, G3'=free_71, H3'=free_59, Q3'=free_64, J3'=0, K3'=free_69, L3'=free_60, M3'=free_65, N3'=free_70, O3'=free_58, P3'=free_63, Q3_1'=0, R3'=0, S3'=free_68, T3'=free_57, U3'=free_62, V3'=free_62, W3'=1, [ 6>=free_62 && free_67>=1 && free_72>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
     70: f0 -> f120 : B'=free_78, L'=free_83, U'=0, E1'=0, F1'=free_88, J1'=free_30, K1'=0, O1'=free_88, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_88, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_83, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_83, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_77, D3'=free_77, E3'=free_77, F3'=free_82, G3'=free_87, H3'=free_75, Q3'=free_80, J3'=0, K3'=free_85, L3'=free_76, M3'=free_81, N3'=free_86, O3'=free_74, P3'=free_79, Q3_1'=0, R3'=0, S3'=free_84, T3'=free_73, U3'=free_78, V3'=free_78, W3'=1, [ free_78>=8 && free_83>=1 && free_88>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30

Eliminating 5 self-loops for location f120
  Self-Loop 104 has unbounded runtime, resulting in the new transition 129.
  Self-Loop 105 has unbounded runtime, resulting in the new transition 130.
  Removing the self-loops: 104 105 107 111 116.
Adding an epsilon transition (to model nonexecution of the loops): 134.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
    129: f120 -> [21] : [ 0>=U && 0>=P1 && J1==1 && 3>=free_22 ], cost: INF
    130: f120 -> [21] : [ 0>=U && 0>=P1 && J1==1 && free_22>=5 && 6>=free_22 ], cost: INF
    131: f120 -> [21] : B'=4, H'=free_12, Q'=free_14, J'=free_10, K'=L, M'=free_11, N'=free_13, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, U'=1, V'=free_6, Z'=0, A1'=0, B1'=0, C1'=1, F1'=O1, J1'=1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 && J1==1 && 6>=free_6 && T>=1 ], cost: 6
    132: f120 -> [21] : B'=4, H'=free_12, Q'=free_14, J'=free_10, K'=L, M'=free_11, N'=free_13, O'=0, P'=0, Q_1'=free_5, R'=7, S'=7, U'=1, V'=7, Z'=0, A1'=0, B1'=0, C1'=1, F1'=O1, J1'=1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_25, R1'=free_26, S1'=1, T1'=0, U1'=1+U1, V1'=U1, [ P1>=1+U1 && 0>=U && P1>=1 && J1==1 ], cost: 5
    133: f120 -> [21] : A'=0, B'=4, C'=0, D'=0, G'=0, H'=free_12, Q'=free_14, J'=free_10, K'=L, M'=free_11, N'=free_13, O'=0, P'=0, Q_1'=free_5, R'=7, S'=7, U'=1, V'=7, Z'=0, A1'=0, B1'=0, C1'=1, F1'=1, G1'=1, H1'=free_20, Q1'=-1, K1'=0, L1'=0, M1'=0, N1'=0, Q1_1'=free_23, R1'=free_24, S1'=1, T1'=0, [ 0>=U && 0>=P1 && 0>=J1 && D1>=1+E1 ], cost: 8
    134: f120 -> [21] : [], cost: 0
     68: f0 -> f120 : B'=7, L'=free_51, U'=0, E1'=0, F1'=free_56, J1'=free_30, K1'=0, O1'=free_56, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_56, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_51, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_51, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_46, D3'=free_46, E3'=free_46, F3'=free_50, G3'=free_55, H3'=free_44, Q3'=free_48, J3'=0, K3'=free_53, L3'=free_45, M3'=free_49, N3'=free_54, O3'=free_43, P3'=free_47, Q3_1'=0, R3'=0, S3'=free_52, T3'=free_42, U3'=7, V3'=7, [ free_51>=1 && free_56>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
     69: f0 -> f120 : B'=free_62, L'=free_67, U'=0, E1'=0, F1'=free_72, J1'=free_30, K1'=0, O1'=free_72, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_72, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_67, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_67, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_61, D3'=free_61, E3'=free_61, F3'=free_66, G3'=free_71, H3'=free_59, Q3'=free_64, J3'=0, K3'=free_69, L3'=free_60, M3'=free_65, N3'=free_70, O3'=free_58, P3'=free_63, Q3_1'=0, R3'=0, S3'=free_68, T3'=free_57, U3'=free_62, V3'=free_62, W3'=1, [ 6>=free_62 && free_67>=1 && free_72>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
     70: f0 -> f120 : B'=free_78, L'=free_83, U'=0, E1'=0, F1'=free_88, J1'=free_30, K1'=0, O1'=free_88, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_88, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_83, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_83, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_77, D3'=free_77, E3'=free_77, F3'=free_82, G3'=free_87, H3'=free_75, Q3'=free_80, J3'=0, K3'=free_85, L3'=free_76, M3'=free_81, N3'=free_86, O3'=free_74, P3'=free_79, Q3_1'=0, R3'=0, S3'=free_84, T3'=free_73, U3'=free_78, V3'=free_78, W3'=1, [ free_78>=8 && free_83>=1 && free_88>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
     33: [21] -> [19] : X1'=0, [ U>=1 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
    136: f0 -> [21] : B'=7, L'=free_51, U'=0, E1'=0, F1'=free_56, J1'=free_30, K1'=0, O1'=free_56, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_56, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_51, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_51, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_46, D3'=free_46, E3'=free_46, F3'=free_50, G3'=free_55, H3'=free_44, Q3'=free_48, J3'=0, K3'=free_53, L3'=free_45, M3'=free_49, N3'=free_54, O3'=free_43, P3'=free_47, Q3_1'=0, R3'=0, S3'=free_52, T3'=free_42, U3'=7, V3'=7, [ free_51>=1 && free_56>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 && 0>=0 && 0>=P1 && free_30==1 && free_22>=5 && 6>=free_22 ], cost: INF
    140: f0 -> [21] : B'=7, L'=free_51, U'=0, E1'=0, F1'=free_56, J1'=free_30, K1'=0, O1'=free_56, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_56, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_51, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_51, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_46, D3'=free_46, E3'=free_46, F3'=free_50, G3'=free_55, H3'=free_44, Q3'=free_48, J3'=0, K3'=free_53, L3'=free_45, M3'=free_49, N3'=free_54, O3'=free_43, P3'=free_47, Q3_1'=0, R3'=0, S3'=free_52, T3'=free_42, U3'=7, V3'=7, [ free_51>=1 && free_56>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
    142: f0 -> [21] : B'=free_62, L'=free_67, U'=0, E1'=0, F1'=free_72, J1'=free_30, K1'=0, O1'=free_72, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_72, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_67, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_67, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_61, D3'=free_61, E3'=free_61, F3'=free_66, G3'=free_71, H3'=free_59, Q3'=free_64, J3'=0, K3'=free_69, L3'=free_60, M3'=free_65, N3'=free_70, O3'=free_58, P3'=free_63, Q3_1'=0, R3'=0, S3'=free_68, T3'=free_57, U3'=free_62, V3'=free_62, W3'=1, [ 6>=free_62 && free_67>=1 && free_72>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 && 0>=0 && 0>=P1 && free_30==1 && free_22>=5 && 6>=free_22 ], cost: INF
    146: f0 -> [21] : B'=free_62, L'=free_67, U'=0, E1'=0, F1'=free_72, J1'=free_30, K1'=0, O1'=free_72, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_72, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_67, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_67, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_61, D3'=free_61, E3'=free_61, F3'=free_66, G3'=free_71, H3'=free_59, Q3'=free_64, J3'=0, K3'=free_69, L3'=free_60, M3'=free_65, N3'=free_70, O3'=free_58, P3'=free_63, Q3_1'=0, R3'=0, S3'=free_68, T3'=free_57, U3'=free_62, V3'=free_62, W3'=1, [ 6>=free_62 && free_67>=1 && free_72>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
    152: f0 -> [21] : B'=free_78, L'=free_83, U'=0, E1'=0, F1'=free_88, J1'=free_30, K1'=0, O1'=free_88, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_88, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_83, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_83, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_77, D3'=free_77, E3'=free_77, F3'=free_82, G3'=free_87, H3'=free_75, Q3'=free_80, J3'=0, K3'=free_85, L3'=free_76, M3'=free_81, N3'=free_86, O3'=free_74, P3'=free_79, Q3_1'=0, R3'=0, S3'=free_84, T3'=free_73, U3'=free_78, V3'=free_78, W3'=1, [ free_78>=8 && free_83>=1 && free_88>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
    139: f0 -> [22] : B'=7, L'=free_51, U'=0, E1'=0, F1'=free_56, J1'=free_30, K1'=0, O1'=free_56, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_56, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_51, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_51, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_46, D3'=free_46, E3'=free_46, F3'=free_50, G3'=free_55, H3'=free_44, Q3'=free_48, J3'=0, K3'=free_53, L3'=free_45, M3'=free_49, N3'=free_54, O3'=free_43, P3'=free_47, Q3_1'=0, R3'=0, S3'=free_52, T3'=free_42, U3'=7, V3'=7, [ free_51>=1 && free_56>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
    145: f0 -> [23] : B'=free_62, L'=free_67, U'=0, E1'=0, F1'=free_72, J1'=free_30, K1'=0, O1'=free_72, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_72, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_67, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_67, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_61, D3'=free_61, E3'=free_61, F3'=free_66, G3'=free_71, H3'=free_59, Q3'=free_64, J3'=0, K3'=free_69, L3'=free_60, M3'=free_65, N3'=free_70, O3'=free_58, P3'=free_63, Q3_1'=0, R3'=0, S3'=free_68, T3'=free_57, U3'=free_62, V3'=free_62, W3'=1, [ 6>=free_62 && free_67>=1 && free_72>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
    151: f0 -> [24] : B'=free_78, L'=free_83, U'=0, E1'=0, F1'=free_88, J1'=free_30, K1'=0, O1'=free_88, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_88, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_83, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_83, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_77, D3'=free_77, E3'=free_77, F3'=free_82, G3'=free_87, H3'=free_75, Q3'=free_80, J3'=0, K3'=free_85, L3'=free_76, M3'=free_81, N3'=free_86, O3'=free_74, P3'=free_79, Q3_1'=0, R3'=0, S3'=free_84, T3'=free_73, U3'=free_78, V3'=free_78, W3'=1, [ free_78>=8 && free_83>=1 && free_88>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
     33: [21] -> [19] : X1'=0, [ U>=1 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
    139: f0 -> [22] : B'=7, L'=free_51, U'=0, E1'=0, F1'=free_56, J1'=free_30, K1'=0, O1'=free_56, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_56, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_51, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_51, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_46, D3'=free_46, E3'=free_46, F3'=free_50, G3'=free_55, H3'=free_44, Q3'=free_48, J3'=0, K3'=free_53, L3'=free_45, M3'=free_49, N3'=free_54, O3'=free_43, P3'=free_47, Q3_1'=0, R3'=0, S3'=free_52, T3'=free_42, U3'=7, V3'=7, [ free_51>=1 && free_56>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
    145: f0 -> [23] : B'=free_62, L'=free_67, U'=0, E1'=0, F1'=free_72, J1'=free_30, K1'=0, O1'=free_72, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_72, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_67, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_67, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_61, D3'=free_61, E3'=free_61, F3'=free_66, G3'=free_71, H3'=free_59, Q3'=free_64, J3'=0, K3'=free_69, L3'=free_60, M3'=free_65, N3'=free_70, O3'=free_58, P3'=free_63, Q3_1'=0, R3'=0, S3'=free_68, T3'=free_57, U3'=free_62, V3'=free_62, W3'=1, [ 6>=free_62 && free_67>=1 && free_72>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
    151: f0 -> [24] : B'=free_78, L'=free_83, U'=0, E1'=0, F1'=free_88, J1'=free_30, K1'=0, O1'=free_88, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_88, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_83, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_83, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_77, D3'=free_77, E3'=free_77, F3'=free_82, G3'=free_87, H3'=free_75, Q3'=free_80, J3'=0, K3'=free_85, L3'=free_76, M3'=free_81, N3'=free_86, O3'=free_74, P3'=free_79, Q3_1'=0, R3'=0, S3'=free_84, T3'=free_73, U3'=free_78, V3'=free_78, W3'=1, [ free_78>=8 && free_83>=1 && free_88>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
    153: f0 -> [25] : B'=7, L'=free_51, U'=0, E1'=0, F1'=free_56, J1'=free_30, K1'=0, O1'=free_56, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_56, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_51, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_51, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_46, D3'=free_46, E3'=free_46, F3'=free_50, G3'=free_55, H3'=free_44, Q3'=free_48, J3'=0, K3'=free_53, L3'=free_45, M3'=free_49, N3'=free_54, O3'=free_43, P3'=free_47, Q3_1'=0, R3'=0, S3'=free_52, T3'=free_42, U3'=7, V3'=7, [ free_51>=1 && free_56>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 && 0>=0 && 0>=P1 && free_30==1 && free_22>=5 && 6>=free_22 ], cost: INF
    154: f0 -> [26] : B'=7, L'=free_51, U'=0, E1'=0, F1'=free_56, J1'=free_30, K1'=0, O1'=free_56, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_56, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_51, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_51, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_46, D3'=free_46, E3'=free_46, F3'=free_50, G3'=free_55, H3'=free_44, Q3'=free_48, J3'=0, K3'=free_53, L3'=free_45, M3'=free_49, N3'=free_54, O3'=free_43, P3'=free_47, Q3_1'=0, R3'=0, S3'=free_52, T3'=free_42, U3'=7, V3'=7, [ free_51>=1 && free_56>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
    155: f0 -> [27] : B'=free_62, L'=free_67, U'=0, E1'=0, F1'=free_72, J1'=free_30, K1'=0, O1'=free_72, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_72, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_67, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_67, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_61, D3'=free_61, E3'=free_61, F3'=free_66, G3'=free_71, H3'=free_59, Q3'=free_64, J3'=0, K3'=free_69, L3'=free_60, M3'=free_65, N3'=free_70, O3'=free_58, P3'=free_63, Q3_1'=0, R3'=0, S3'=free_68, T3'=free_57, U3'=free_62, V3'=free_62, W3'=1, [ 6>=free_62 && free_67>=1 && free_72>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 && 0>=0 && 0>=P1 && free_30==1 && free_22>=5 && 6>=free_22 ], cost: INF
    156: f0 -> [28] : B'=free_62, L'=free_67, U'=0, E1'=0, F1'=free_72, J1'=free_30, K1'=0, O1'=free_72, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_72, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_67, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_67, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_61, D3'=free_61, E3'=free_61, F3'=free_66, G3'=free_71, H3'=free_59, Q3'=free_64, J3'=0, K3'=free_69, L3'=free_60, M3'=free_65, N3'=free_70, O3'=free_58, P3'=free_63, Q3_1'=0, R3'=0, S3'=free_68, T3'=free_57, U3'=free_62, V3'=free_62, W3'=1, [ 6>=free_62 && free_67>=1 && free_72>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
    157: f0 -> [29] : B'=free_78, L'=free_83, U'=0, E1'=0, F1'=free_88, J1'=free_30, K1'=0, O1'=free_88, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_88, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_83, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_83, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_77, D3'=free_77, E3'=free_77, F3'=free_82, G3'=free_87, H3'=free_75, Q3'=free_80, J3'=0, K3'=free_85, L3'=free_76, M3'=free_81, N3'=free_86, O3'=free_74, P3'=free_79, Q3_1'=0, R3'=0, S3'=free_84, T3'=free_73, U3'=free_78, V3'=free_78, W3'=1, [ free_78>=8 && free_83>=1 && free_88>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
    139: f0 -> [22] : B'=7, L'=free_51, U'=0, E1'=0, F1'=free_56, J1'=free_30, K1'=0, O1'=free_56, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_56, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_51, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_51, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_46, D3'=free_46, E3'=free_46, F3'=free_50, G3'=free_55, H3'=free_44, Q3'=free_48, J3'=0, K3'=free_53, L3'=free_45, M3'=free_49, N3'=free_54, O3'=free_43, P3'=free_47, Q3_1'=0, R3'=0, S3'=free_52, T3'=free_42, U3'=7, V3'=7, [ free_51>=1 && free_56>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
    145: f0 -> [23] : B'=free_62, L'=free_67, U'=0, E1'=0, F1'=free_72, J1'=free_30, K1'=0, O1'=free_72, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_72, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_67, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_67, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_61, D3'=free_61, E3'=free_61, F3'=free_66, G3'=free_71, H3'=free_59, Q3'=free_64, J3'=0, K3'=free_69, L3'=free_60, M3'=free_65, N3'=free_70, O3'=free_58, P3'=free_63, Q3_1'=0, R3'=0, S3'=free_68, T3'=free_57, U3'=free_62, V3'=free_62, W3'=1, [ 6>=free_62 && free_67>=1 && free_72>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
    151: f0 -> [24] : B'=free_78, L'=free_83, U'=0, E1'=0, F1'=free_88, J1'=free_30, K1'=0, O1'=free_88, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_88, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_83, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_83, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_77, D3'=free_77, E3'=free_77, F3'=free_82, G3'=free_87, H3'=free_75, Q3'=free_80, J3'=0, K3'=free_85, L3'=free_76, M3'=free_81, N3'=free_86, O3'=free_74, P3'=free_79, Q3_1'=0, R3'=0, S3'=free_84, T3'=free_73, U3'=free_78, V3'=free_78, W3'=1, [ free_78>=8 && free_83>=1 && free_88>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
    153: f0 -> [25] : B'=7, L'=free_51, U'=0, E1'=0, F1'=free_56, J1'=free_30, K1'=0, O1'=free_56, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_56, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_51, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_51, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_46, D3'=free_46, E3'=free_46, F3'=free_50, G3'=free_55, H3'=free_44, Q3'=free_48, J3'=0, K3'=free_53, L3'=free_45, M3'=free_49, N3'=free_54, O3'=free_43, P3'=free_47, Q3_1'=0, R3'=0, S3'=free_52, T3'=free_42, U3'=7, V3'=7, [ free_51>=1 && free_56>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 && 0>=0 && 0>=P1 && free_30==1 && free_22>=5 && 6>=free_22 ], cost: INF
    154: f0 -> [26] : B'=7, L'=free_51, U'=0, E1'=0, F1'=free_56, J1'=free_30, K1'=0, O1'=free_56, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_56, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_51, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_51, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_46, D3'=free_46, E3'=free_46, F3'=free_50, G3'=free_55, H3'=free_44, Q3'=free_48, J3'=0, K3'=free_53, L3'=free_45, M3'=free_49, N3'=free_54, O3'=free_43, P3'=free_47, Q3_1'=0, R3'=0, S3'=free_52, T3'=free_42, U3'=7, V3'=7, [ free_51>=1 && free_56>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
    155: f0 -> [27] : B'=free_62, L'=free_67, U'=0, E1'=0, F1'=free_72, J1'=free_30, K1'=0, O1'=free_72, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_72, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_67, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_67, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_61, D3'=free_61, E3'=free_61, F3'=free_66, G3'=free_71, H3'=free_59, Q3'=free_64, J3'=0, K3'=free_69, L3'=free_60, M3'=free_65, N3'=free_70, O3'=free_58, P3'=free_63, Q3_1'=0, R3'=0, S3'=free_68, T3'=free_57, U3'=free_62, V3'=free_62, W3'=1, [ 6>=free_62 && free_67>=1 && free_72>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 && 0>=0 && 0>=P1 && free_30==1 && free_22>=5 && 6>=free_22 ], cost: INF
    156: f0 -> [28] : B'=free_62, L'=free_67, U'=0, E1'=0, F1'=free_72, J1'=free_30, K1'=0, O1'=free_72, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_72, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_67, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_67, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_61, D3'=free_61, E3'=free_61, F3'=free_66, G3'=free_71, H3'=free_59, Q3'=free_64, J3'=0, K3'=free_69, L3'=free_60, M3'=free_65, N3'=free_70, O3'=free_58, P3'=free_63, Q3_1'=0, R3'=0, S3'=free_68, T3'=free_57, U3'=free_62, V3'=free_62, W3'=1, [ 6>=free_62 && free_67>=1 && free_72>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30
    157: f0 -> [29] : B'=free_78, L'=free_83, U'=0, E1'=0, F1'=free_88, J1'=free_30, K1'=0, O1'=free_88, U1'=0, Y1'=0, Z1'=0, A2'=6, B2'=1, C2'=5, D2'=free_88, E2'=free_29, F2'=8, G2'=0, H2'=0, Q2'=free_33, J2'=free_35, K2'=free_31, L2'=free_83, M2'=0, N2'=free_32, O2'=1, P2'=0, Q2_1'=J1, R2'=free_34, S2'=0, U2'=free_83, V2'=0, W2'=0, X2'=0, Y2'=0, Z2'=0, A3'=256, B3'=0, C3'=free_77, D3'=free_77, E3'=free_77, F3'=free_82, G3'=free_87, H3'=free_75, Q3'=free_80, J3'=0, K3'=free_85, L3'=free_76, M3'=free_81, N3'=free_86, O3'=free_74, P3'=free_79, Q3_1'=0, R3'=0, S3'=free_84, T3'=free_73, U3'=free_78, V3'=free_78, W3'=1, [ free_78>=8 && free_83>=1 && free_88>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0 ], cost: 3+free_30


Computing complexity for remaining 8 transitions.

  Found configuration with infinitely models for cost: 3+free_30
  and guard: free_51>=1 && free_56>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0:
  free_30: Pos, free_56: Pos, free_51: Pos

Found new complexity INF, because: Found infinity configuration.


The final runtime is determined by this resulting transition:
  Final Guard: free_51>=1 && free_56>=1 && free_30>=1 && 0>=0 && free_30>=1 && 0>=0
  Final Cost:  3+free_30

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

WORST_CASE(INF,?)