Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f171 -> f172 : [ 0>=1+A ], cost: 1
      1: f171 -> f172 : [ A>=1 ], cost: 1
     32: f171 -> f165 : A'=0, B'=0, N1'=free_26, O1'=-1, [ A==0 ], cost: 1
     31: f172 -> f165 : B'=0, G'=0, N1'=free_25, O1'=-1, [ G==0 ], cost: 1
      7: f172 -> f173 : [ 0>=1+G ], cost: 1
      8: f172 -> f173 : [ G>=1 ], cost: 1
      2: f165 -> f185 : B'=7, C'=7, [ B==7 ], cost: 1
      3: f165 -> f170 : C'=B, D'=B, E'=0, [ 6>=B ], cost: 1
      4: f165 -> f170 : C'=B, D'=B, E'=0, [ B>=8 ], cost: 1
     27: f185 -> f195 : C'=free_20, B1'=0, G1'=1, [ E1>=1+F1 ], cost: 1
     28: f185 -> f195 : C'=free_21, B1'=0, F1'=0, G1'=1, [ F1>=E1 ], cost: 1
      5: f170 -> f171 : F'=E, [ 0>=1+E ], cost: 1
      6: f170 -> f171 : F'=E, [ E>=1 ], cost: 1
     29: f170 -> f185 : E'=0, F'=0, H1'=3, Q1'=2, J1'=C, K1'=free_22, L1'=free_23, M1'=1, [ E==0 ], cost: 1
      9: f173 -> f173 : [], cost: 1
     10: f203 -> f213 : C'=7, H'=free, Q'=free_2, J'=free_3, K'=L, M'=free_4, N'=free_1, O'=0, [ C==7 ], cost: 1
     13: f203 -> f130 : [ 6>=C ], cost: 1
     14: f203 -> f130 : [ C>=8 ], cost: 1
     11: f213 -> f226 : O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, [ O==0 ], cost: 1
     22: f213 -> f226 : P'=O, Q_1'=free_10, R'=free_11, S'=free_11, X'=O, Y'=free_9, Z'=O, [ 0>=1+O ], cost: 1
     23: f213 -> f226 : P'=O, Q_1'=free_13, R'=free_14, S'=free_14, X'=O, Y'=free_12, Z'=O, [ O>=1 ], cost: 1
     16: f226 -> f230 : T'=free_7, W'=S, [ 6>=S ], cost: 1
     17: f226 -> f230 : T'=free_8, W'=S, [ S>=8 ], cost: 1
     15: f226 -> f130 : S'=7, V'=1, W'=7, [ S==7 ], cost: 1
     12: f230 -> f130 : U'=T, [ T==U ], cost: 1
     18: f230 -> f130 : V'=1, [ T>=1+U ], cost: 1
     19: f230 -> f130 : V'=1, [ U>=1+T ], cost: 1
     39: f130 -> f236 : D2'=0, [ 0>=1+V ], cost: 1
     40: f130 -> f236 : D2'=0, [ V>=1 ], cost: 1
     36: f130 -> f147 : V'=0, W1'=free_30, X1'=free_31, Y1'=1, Z1'=0, [ 0>=V1 && V==0 ], cost: 1
     37: f130 -> f147 : V'=0, W1'=free_32, X1'=free_33, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, [ V1>=1 && V1>=1+A2 && V==0 ], cost: 1
     38: f130 -> f147 : V'=0, W1'=free_34, X1'=free_35, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, C2'=0, [ A2>=V1 && V1>=1 && V==0 ], cost: 1
     20: f236 -> f236 : [], cost: 1
     21: f238 -> f240 : [], cost: 1
     24: f195 -> f203 : A1'=B1, C1'=B1, [ 3>=C ], cost: 1
     25: f195 -> f203 : A1'=B1, C1'=B1, [ C>=5 ], cost: 1
     26: f195 -> f213 : C'=4, H'=free_15, Q'=free_17, J'=free_18, K'=L, M'=free_19, N'=free_16, O'=0, A1'=B1, C1'=B1, D1'=1, [ C==4 ], cost: 1
     30: f175 -> f165 : B'=0, N1'=free_24, O1'=-1, [], cost: 1
     33: f147 -> f165 : B'=0, N1'=free_27, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, [ 0>=P1 ], cost: 1
     34: f147 -> f165 : B'=0, N1'=free_28, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, [ P1>=2 ], cost: 1
     35: f147 -> f195 : C'=free_29, B1'=0, G1'=U1, P1'=1, Q1_1'=0, R1'=0, S1'=0, T1'=0, [ P1==1 ], cost: 1
     43: f116 -> f130 : E2'=0, M2'=8, [ E2==0 ], cost: 1
     41: f116 -> f116 : E2'=F2, F2'=-1+F2, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=G1, L2'=free_36, [ 0>=1+E2 ], cost: 1
     42: f116 -> f116 : E2'=F2, F2'=-1+F2, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=G1, L2'=free_37, [ E2>=1 ], cost: 1
     44: f85 -> f116 : G1'=U1, P1'=free_41, E2'=free_41, F2'=-1+free_41, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=L, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, [ free_41>=1 && N2==0 ], cost: 1
     45: f85 -> f116 : G1'=U1, P1'=free_47, E2'=free_47, F2'=-1+free_47, O2'=N2, P2'=free_44, Q2_1'=free_46, R2'=free_48, S2'=L, T2'=0, U2'=free_49, V2'=1, W2'=0, X2'=P1, Y2'=free_45, Z2'=0, A3'=1, [ free_47>=1 && 0>=1+N2 ], cost: 1
     46: f85 -> f116 : G1'=U1, P1'=free_53, E2'=free_53, F2'=-1+free_53, O2'=N2, P2'=free_50, Q2_1'=free_52, R2'=free_54, S2'=L, T2'=0, U2'=free_55, V2'=1, W2'=0, X2'=P1, Y2'=free_51, Z2'=0, A3'=1, [ free_53>=1 && N2>=1 ], cost: 1
     47: f0 -> f85 : C'=7, L'=free_56, V'=0, F1'=0, Q1_1'=0, U1'=free_60, A2'=0, M2'=9, N2'=0, B3'=free_56, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_65, K3'=free_65, L3'=free_65, M3'=free_70, N3'=free_59, O3'=free_64, P3'=free_69, Q3_1'=0, R3'=free_58, S3'=free_63, T3'=free_68, U3'=free_62, V3'=free_67, W3'=free_57, X3'=0, Y3'=0, Z3'=free_61, A4'=free_66, B4'=7, C4'=7, [ free_56>=1 && free_60>=1 ], cost: 1
     48: f0 -> f85 : C'=free_71, L'=free_72, V'=0, F1'=0, Q1_1'=0, U1'=free_78, A2'=0, M2'=9, N2'=0, B3'=free_72, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_84, K3'=free_84, L3'=free_84, M3'=free_90, N3'=free_76, O3'=free_82, P3'=free_88, Q3_1'=0, R3'=free_74, S3'=free_81, T3'=free_87, U3'=free_80, V3'=free_86, W3'=free_73, X3'=0, Y3'=0, Z3'=free_79, A4'=free_85, B4'=free_71, C4'=free_71, D4'=3, E4'=1, F4'=free_71, G4'=free_77, H4'=free_83, Q4'=free_89, J4'=free_75, K4'=1, [ 6>=free_71 && free_72>=1 && free_78>=1 ], cost: 1
     49: f0 -> f85 : C'=free_91, L'=free_92, V'=0, F1'=0, Q1_1'=0, U1'=free_98, A2'=0, M2'=9, N2'=0, B3'=free_92, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_104, K3'=free_104, L3'=free_104, M3'=free_110, N3'=free_96, O3'=free_102, P3'=free_108, Q3_1'=0, R3'=free_94, S3'=free_101, T3'=free_107, U3'=free_100, V3'=free_106, W3'=free_93, X3'=0, Y3'=0, Z3'=free_99, A4'=free_105, B4'=free_91, C4'=free_91, D4'=3, E4'=1, F4'=free_91, G4'=free_97, H4'=free_103, Q4'=free_109, J4'=free_95, K4'=1, [ free_91>=8 && free_92>=1 && free_98>=1 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f171 -> f172 : [ 0>=1+A ], cost: 1
      1: f171 -> f172 : [ A>=1 ], cost: 1
     32: f171 -> f165 : A'=0, B'=0, N1'=free_26, O1'=-1, [ A==0 ], cost: 1
     31: f172 -> f165 : B'=0, G'=0, N1'=free_25, O1'=-1, [ G==0 ], cost: 1
      7: f172 -> f173 : [ 0>=1+G ], cost: 1
      8: f172 -> f173 : [ G>=1 ], cost: 1
      2: f165 -> f185 : B'=7, C'=7, [ B==7 ], cost: 1
      3: f165 -> f170 : C'=B, D'=B, E'=0, [ 6>=B ], cost: 1
      4: f165 -> f170 : C'=B, D'=B, E'=0, [ B>=8 ], cost: 1
     27: f185 -> f195 : C'=free_20, B1'=0, G1'=1, [ E1>=1+F1 ], cost: 1
     28: f185 -> f195 : C'=free_21, B1'=0, F1'=0, G1'=1, [ F1>=E1 ], cost: 1
      5: f170 -> f171 : F'=E, [ 0>=1+E ], cost: 1
      6: f170 -> f171 : F'=E, [ E>=1 ], cost: 1
     29: f170 -> f185 : E'=0, F'=0, H1'=3, Q1'=2, J1'=C, K1'=free_22, L1'=free_23, M1'=1, [ E==0 ], cost: 1
      9: f173 -> f173 : [], cost: 1
     10: f203 -> f213 : C'=7, H'=free, Q'=free_2, J'=free_3, K'=L, M'=free_4, N'=free_1, O'=0, [ C==7 ], cost: 1
     13: f203 -> f130 : [ 6>=C ], cost: 1
     14: f203 -> f130 : [ C>=8 ], cost: 1
     11: f213 -> f226 : O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, [ O==0 ], cost: 1
     22: f213 -> f226 : P'=O, Q_1'=free_10, R'=free_11, S'=free_11, X'=O, Y'=free_9, Z'=O, [ 0>=1+O ], cost: 1
     23: f213 -> f226 : P'=O, Q_1'=free_13, R'=free_14, S'=free_14, X'=O, Y'=free_12, Z'=O, [ O>=1 ], cost: 1
     16: f226 -> f230 : T'=free_7, W'=S, [ 6>=S ], cost: 1
     17: f226 -> f230 : T'=free_8, W'=S, [ S>=8 ], cost: 1
     15: f226 -> f130 : S'=7, V'=1, W'=7, [ S==7 ], cost: 1
     12: f230 -> f130 : U'=T, [ T==U ], cost: 1
     18: f230 -> f130 : V'=1, [ T>=1+U ], cost: 1
     19: f230 -> f130 : V'=1, [ U>=1+T ], cost: 1
     39: f130 -> f236 : D2'=0, [ 0>=1+V ], cost: 1
     40: f130 -> f236 : D2'=0, [ V>=1 ], cost: 1
     36: f130 -> f147 : V'=0, W1'=free_30, X1'=free_31, Y1'=1, Z1'=0, [ 0>=V1 && V==0 ], cost: 1
     37: f130 -> f147 : V'=0, W1'=free_32, X1'=free_33, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, [ V1>=1 && V1>=1+A2 && V==0 ], cost: 1
     38: f130 -> f147 : V'=0, W1'=free_34, X1'=free_35, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, C2'=0, [ A2>=V1 && V1>=1 && V==0 ], cost: 1
     20: f236 -> f236 : [], cost: 1
     24: f195 -> f203 : A1'=B1, C1'=B1, [ 3>=C ], cost: 1
     25: f195 -> f203 : A1'=B1, C1'=B1, [ C>=5 ], cost: 1
     26: f195 -> f213 : C'=4, H'=free_15, Q'=free_17, J'=free_18, K'=L, M'=free_19, N'=free_16, O'=0, A1'=B1, C1'=B1, D1'=1, [ C==4 ], cost: 1
     33: f147 -> f165 : B'=0, N1'=free_27, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, [ 0>=P1 ], cost: 1
     34: f147 -> f165 : B'=0, N1'=free_28, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, [ P1>=2 ], cost: 1
     35: f147 -> f195 : C'=free_29, B1'=0, G1'=U1, P1'=1, Q1_1'=0, R1'=0, S1'=0, T1'=0, [ P1==1 ], cost: 1
     43: f116 -> f130 : E2'=0, M2'=8, [ E2==0 ], cost: 1
     41: f116 -> f116 : E2'=F2, F2'=-1+F2, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=G1, L2'=free_36, [ 0>=1+E2 ], cost: 1
     42: f116 -> f116 : E2'=F2, F2'=-1+F2, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=G1, L2'=free_37, [ E2>=1 ], cost: 1
     44: f85 -> f116 : G1'=U1, P1'=free_41, E2'=free_41, F2'=-1+free_41, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=L, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, [ free_41>=1 && N2==0 ], cost: 1
     45: f85 -> f116 : G1'=U1, P1'=free_47, E2'=free_47, F2'=-1+free_47, O2'=N2, P2'=free_44, Q2_1'=free_46, R2'=free_48, S2'=L, T2'=0, U2'=free_49, V2'=1, W2'=0, X2'=P1, Y2'=free_45, Z2'=0, A3'=1, [ free_47>=1 && 0>=1+N2 ], cost: 1
     46: f85 -> f116 : G1'=U1, P1'=free_53, E2'=free_53, F2'=-1+free_53, O2'=N2, P2'=free_50, Q2_1'=free_52, R2'=free_54, S2'=L, T2'=0, U2'=free_55, V2'=1, W2'=0, X2'=P1, Y2'=free_51, Z2'=0, A3'=1, [ free_53>=1 && N2>=1 ], cost: 1
     47: f0 -> f85 : C'=7, L'=free_56, V'=0, F1'=0, Q1_1'=0, U1'=free_60, A2'=0, M2'=9, N2'=0, B3'=free_56, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_65, K3'=free_65, L3'=free_65, M3'=free_70, N3'=free_59, O3'=free_64, P3'=free_69, Q3_1'=0, R3'=free_58, S3'=free_63, T3'=free_68, U3'=free_62, V3'=free_67, W3'=free_57, X3'=0, Y3'=0, Z3'=free_61, A4'=free_66, B4'=7, C4'=7, [ free_56>=1 && free_60>=1 ], cost: 1
     48: f0 -> f85 : C'=free_71, L'=free_72, V'=0, F1'=0, Q1_1'=0, U1'=free_78, A2'=0, M2'=9, N2'=0, B3'=free_72, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_84, K3'=free_84, L3'=free_84, M3'=free_90, N3'=free_76, O3'=free_82, P3'=free_88, Q3_1'=0, R3'=free_74, S3'=free_81, T3'=free_87, U3'=free_80, V3'=free_86, W3'=free_73, X3'=0, Y3'=0, Z3'=free_79, A4'=free_85, B4'=free_71, C4'=free_71, D4'=3, E4'=1, F4'=free_71, G4'=free_77, H4'=free_83, Q4'=free_89, J4'=free_75, K4'=1, [ 6>=free_71 && free_72>=1 && free_78>=1 ], cost: 1
     49: f0 -> f85 : C'=free_91, L'=free_92, V'=0, F1'=0, Q1_1'=0, U1'=free_98, A2'=0, M2'=9, N2'=0, B3'=free_92, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_104, K3'=free_104, L3'=free_104, M3'=free_110, N3'=free_96, O3'=free_102, P3'=free_108, Q3_1'=0, R3'=free_94, S3'=free_101, T3'=free_107, U3'=free_100, V3'=free_106, W3'=free_93, X3'=0, Y3'=0, Z3'=free_99, A4'=free_105, B4'=free_91, C4'=free_91, D4'=3, E4'=1, F4'=free_91, G4'=free_97, H4'=free_103, Q4'=free_109, J4'=free_95, K4'=1, [ free_91>=8 && free_92>=1 && free_98>=1 ], cost: 1

Eliminating 1 self-loops for location f173
  Self-Loop 9 has unbounded runtime, resulting in the new transition 50.
  Removing the self-loops: 9.
Eliminating 1 self-loops for location f236
  Self-Loop 20 has unbounded runtime, resulting in the new transition 51.
  Removing the self-loops: 20.
Eliminating 2 self-loops for location f116
  Removing the self-loops: 41 42.
Adding an epsilon transition (to model nonexecution of the loops): 54.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f171 -> f172 : [ 0>=1+A ], cost: 1
      1: f171 -> f172 : [ A>=1 ], cost: 1
     32: f171 -> f165 : A'=0, B'=0, N1'=free_26, O1'=-1, [ A==0 ], cost: 1
     31: f172 -> f165 : B'=0, G'=0, N1'=free_25, O1'=-1, [ G==0 ], cost: 1
      7: f172 -> f173 : [ 0>=1+G ], cost: 1
      8: f172 -> f173 : [ G>=1 ], cost: 1
      2: f165 -> f185 : B'=7, C'=7, [ B==7 ], cost: 1
      3: f165 -> f170 : C'=B, D'=B, E'=0, [ 6>=B ], cost: 1
      4: f165 -> f170 : C'=B, D'=B, E'=0, [ B>=8 ], cost: 1
     27: f185 -> f195 : C'=free_20, B1'=0, G1'=1, [ E1>=1+F1 ], cost: 1
     28: f185 -> f195 : C'=free_21, B1'=0, F1'=0, G1'=1, [ F1>=E1 ], cost: 1
      5: f170 -> f171 : F'=E, [ 0>=1+E ], cost: 1
      6: f170 -> f171 : F'=E, [ E>=1 ], cost: 1
     29: f170 -> f185 : E'=0, F'=0, H1'=3, Q1'=2, J1'=C, K1'=free_22, L1'=free_23, M1'=1, [ E==0 ], cost: 1
     50: f173 -> [20] : [], cost: INF
     10: f203 -> f213 : C'=7, H'=free, Q'=free_2, J'=free_3, K'=L, M'=free_4, N'=free_1, O'=0, [ C==7 ], cost: 1
     13: f203 -> f130 : [ 6>=C ], cost: 1
     14: f203 -> f130 : [ C>=8 ], cost: 1
     11: f213 -> f226 : O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, [ O==0 ], cost: 1
     22: f213 -> f226 : P'=O, Q_1'=free_10, R'=free_11, S'=free_11, X'=O, Y'=free_9, Z'=O, [ 0>=1+O ], cost: 1
     23: f213 -> f226 : P'=O, Q_1'=free_13, R'=free_14, S'=free_14, X'=O, Y'=free_12, Z'=O, [ O>=1 ], cost: 1
     16: f226 -> f230 : T'=free_7, W'=S, [ 6>=S ], cost: 1
     17: f226 -> f230 : T'=free_8, W'=S, [ S>=8 ], cost: 1
     15: f226 -> f130 : S'=7, V'=1, W'=7, [ S==7 ], cost: 1
     12: f230 -> f130 : U'=T, [ T==U ], cost: 1
     18: f230 -> f130 : V'=1, [ T>=1+U ], cost: 1
     19: f230 -> f130 : V'=1, [ U>=1+T ], cost: 1
     39: f130 -> f236 : D2'=0, [ 0>=1+V ], cost: 1
     40: f130 -> f236 : D2'=0, [ V>=1 ], cost: 1
     36: f130 -> f147 : V'=0, W1'=free_30, X1'=free_31, Y1'=1, Z1'=0, [ 0>=V1 && V==0 ], cost: 1
     37: f130 -> f147 : V'=0, W1'=free_32, X1'=free_33, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, [ V1>=1 && V1>=1+A2 && V==0 ], cost: 1
     38: f130 -> f147 : V'=0, W1'=free_34, X1'=free_35, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, C2'=0, [ A2>=V1 && V1>=1 && V==0 ], cost: 1
     51: f236 -> [21] : [], cost: INF
     24: f195 -> f203 : A1'=B1, C1'=B1, [ 3>=C ], cost: 1
     25: f195 -> f203 : A1'=B1, C1'=B1, [ C>=5 ], cost: 1
     26: f195 -> f213 : C'=4, H'=free_15, Q'=free_17, J'=free_18, K'=L, M'=free_19, N'=free_16, O'=0, A1'=B1, C1'=B1, D1'=1, [ C==4 ], cost: 1
     33: f147 -> f165 : B'=0, N1'=free_27, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, [ 0>=P1 ], cost: 1
     34: f147 -> f165 : B'=0, N1'=free_28, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, [ P1>=2 ], cost: 1
     35: f147 -> f195 : C'=free_29, B1'=0, G1'=U1, P1'=1, Q1_1'=0, R1'=0, S1'=0, T1'=0, [ P1==1 ], cost: 1
     52: f116 -> [22] : E2'=F2, F2'=-1+F2, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=G1, L2'=free_36, [ 0>=1+E2 ], cost: 1
     53: f116 -> [22] : E2'=F2, F2'=-1+F2, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=G1, L2'=free_37, [ E2>=1 ], cost: 1
     54: f116 -> [22] : [], cost: 0
     44: f85 -> f116 : G1'=U1, P1'=free_41, E2'=free_41, F2'=-1+free_41, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=L, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, [ free_41>=1 && N2==0 ], cost: 1
     45: f85 -> f116 : G1'=U1, P1'=free_47, E2'=free_47, F2'=-1+free_47, O2'=N2, P2'=free_44, Q2_1'=free_46, R2'=free_48, S2'=L, T2'=0, U2'=free_49, V2'=1, W2'=0, X2'=P1, Y2'=free_45, Z2'=0, A3'=1, [ free_47>=1 && 0>=1+N2 ], cost: 1
     46: f85 -> f116 : G1'=U1, P1'=free_53, E2'=free_53, F2'=-1+free_53, O2'=N2, P2'=free_50, Q2_1'=free_52, R2'=free_54, S2'=L, T2'=0, U2'=free_55, V2'=1, W2'=0, X2'=P1, Y2'=free_51, Z2'=0, A3'=1, [ free_53>=1 && N2>=1 ], cost: 1
     47: f0 -> f85 : C'=7, L'=free_56, V'=0, F1'=0, Q1_1'=0, U1'=free_60, A2'=0, M2'=9, N2'=0, B3'=free_56, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_65, K3'=free_65, L3'=free_65, M3'=free_70, N3'=free_59, O3'=free_64, P3'=free_69, Q3_1'=0, R3'=free_58, S3'=free_63, T3'=free_68, U3'=free_62, V3'=free_67, W3'=free_57, X3'=0, Y3'=0, Z3'=free_61, A4'=free_66, B4'=7, C4'=7, [ free_56>=1 && free_60>=1 ], cost: 1
     48: f0 -> f85 : C'=free_71, L'=free_72, V'=0, F1'=0, Q1_1'=0, U1'=free_78, A2'=0, M2'=9, N2'=0, B3'=free_72, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_84, K3'=free_84, L3'=free_84, M3'=free_90, N3'=free_76, O3'=free_82, P3'=free_88, Q3_1'=0, R3'=free_74, S3'=free_81, T3'=free_87, U3'=free_80, V3'=free_86, W3'=free_73, X3'=0, Y3'=0, Z3'=free_79, A4'=free_85, B4'=free_71, C4'=free_71, D4'=3, E4'=1, F4'=free_71, G4'=free_77, H4'=free_83, Q4'=free_89, J4'=free_75, K4'=1, [ 6>=free_71 && free_72>=1 && free_78>=1 ], cost: 1
     49: f0 -> f85 : C'=free_91, L'=free_92, V'=0, F1'=0, Q1_1'=0, U1'=free_98, A2'=0, M2'=9, N2'=0, B3'=free_92, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_104, K3'=free_104, L3'=free_104, M3'=free_110, N3'=free_96, O3'=free_102, P3'=free_108, Q3_1'=0, R3'=free_94, S3'=free_101, T3'=free_107, U3'=free_100, V3'=free_106, W3'=free_93, X3'=0, Y3'=0, Z3'=free_99, A4'=free_105, B4'=free_91, C4'=free_91, D4'=3, E4'=1, F4'=free_91, G4'=free_97, H4'=free_103, Q4'=free_109, J4'=free_95, K4'=1, [ free_91>=8 && free_92>=1 && free_98>=1 ], cost: 1
     43: [22] -> f130 : E2'=0, M2'=8, [ E2==0 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      2: f165 -> f185 : B'=7, C'=7, [ B==7 ], cost: 1
     72: f165 -> f185 : C'=B, D'=B, E'=0, F'=0, H1'=3, Q1'=2, J1'=B, K1'=free_22, L1'=free_23, M1'=1, [ 6>=B && 0==0 ], cost: 2
     73: f165 -> f185 : C'=B, D'=B, E'=0, F'=0, H1'=3, Q1'=2, J1'=B, K1'=free_22, L1'=free_23, M1'=1, [ B>=8 && 0==0 ], cost: 2
     27: f185 -> f195 : C'=free_20, B1'=0, G1'=1, [ E1>=1+F1 ], cost: 1
     28: f185 -> f195 : C'=free_21, B1'=0, F1'=0, G1'=1, [ F1>=E1 ], cost: 1
     78: f213 -> f230 : O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, T'=free_7, W'=free_6, [ O==0 && 6>=free_6 ], cost: 2
     79: f213 -> f230 : O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, T'=free_8, W'=free_6, [ O==0 && free_6>=8 ], cost: 2
     81: f213 -> f230 : P'=O, Q_1'=free_10, R'=free_11, S'=free_11, T'=free_7, W'=free_11, X'=O, Y'=free_9, Z'=O, [ 0>=1+O && 6>=free_11 ], cost: 2
     82: f213 -> f230 : P'=O, Q_1'=free_10, R'=free_11, S'=free_11, T'=free_8, W'=free_11, X'=O, Y'=free_9, Z'=O, [ 0>=1+O && free_11>=8 ], cost: 2
     85: f213 -> f230 : P'=O, Q_1'=free_13, R'=free_14, S'=free_14, T'=free_8, W'=free_14, X'=O, Y'=free_12, Z'=O, [ O>=1 && free_14>=8 ], cost: 2
     80: f213 -> f130 : O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=7, V'=1, W'=7, [ O==0 && free_6==7 ], cost: 2
     83: f213 -> f130 : P'=O, Q_1'=free_10, R'=free_11, S'=7, V'=1, W'=7, X'=O, Y'=free_9, Z'=O, [ 0>=1+O && free_11==7 ], cost: 2
     86: f213 -> f130 : P'=O, Q_1'=free_13, R'=free_14, S'=7, V'=1, W'=7, X'=O, Y'=free_12, Z'=O, [ O>=1 && free_14==7 ], cost: 2
     12: f230 -> f130 : U'=T, [ T==U ], cost: 1
     18: f230 -> f130 : V'=1, [ T>=1+U ], cost: 1
     19: f230 -> f130 : V'=1, [ U>=1+T ], cost: 1
     63: f130 -> f165 : B'=0, V'=0, N1'=free_27, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_30, X1'=free_31, Y1'=1, Z1'=0, [ 0>=V1 && V==0 && 0>=P1 ], cost: 2
     64: f130 -> f165 : B'=0, V'=0, N1'=free_28, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_30, X1'=free_31, Y1'=1, Z1'=0, [ 0>=V1 && V==0 && P1>=2 ], cost: 2
     66: f130 -> f165 : B'=0, V'=0, N1'=free_27, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_32, X1'=free_33, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, [ V1>=1 && V1>=1+A2 && V==0 && 0>=P1 ], cost: 2
     67: f130 -> f165 : B'=0, V'=0, N1'=free_28, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_32, X1'=free_33, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, [ V1>=1 && V1>=1+A2 && V==0 && P1>=2 ], cost: 2
     70: f130 -> f165 : B'=0, V'=0, N1'=free_28, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_34, X1'=free_35, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, C2'=0, [ A2>=V1 && V1>=1 && V==0 && P1>=2 ], cost: 2
     65: f130 -> f195 : C'=free_29, V'=0, B1'=0, G1'=U1, P1'=1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_30, X1'=free_31, Y1'=1, Z1'=0, [ 0>=V1 && V==0 && P1==1 ], cost: 2
     68: f130 -> f195 : C'=free_29, V'=0, B1'=0, G1'=U1, P1'=1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_32, X1'=free_33, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, [ V1>=1 && V1>=1+A2 && V==0 && P1==1 ], cost: 2
     71: f130 -> f195 : C'=free_29, V'=0, B1'=0, G1'=U1, P1'=1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_34, X1'=free_35, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, C2'=0, [ A2>=V1 && V1>=1 && V==0 && P1==1 ], cost: 2
     61: f130 -> [21] : D2'=0, [ 0>=1+V ], cost: INF
     62: f130 -> [21] : D2'=0, [ V>=1 ], cost: INF
     26: f195 -> f213 : C'=4, H'=free_15, Q'=free_17, J'=free_18, K'=L, M'=free_19, N'=free_16, O'=0, A1'=B1, C1'=B1, D1'=1, [ C==4 ], cost: 1
     75: f195 -> f213 : C'=7, H'=free, Q'=free_2, J'=free_3, K'=L, M'=free_4, N'=free_1, O'=0, A1'=B1, C1'=B1, [ C>=5 && C==7 ], cost: 2
     74: f195 -> f130 : A1'=B1, C1'=B1, [ 3>=C && 6>=C ], cost: 2
     76: f195 -> f130 : A1'=B1, C1'=B1, [ C>=5 && 6>=C ], cost: 2
     77: f195 -> f130 : A1'=B1, C1'=B1, [ C>=5 && C>=8 ], cost: 2
     58: f116 -> f130 : E2'=0, F2'=-1+F2, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=G1, L2'=free_36, M2'=8, [ 0>=1+E2 && F2==0 ], cost: 2
     59: f116 -> f130 : E2'=0, F2'=-1+F2, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=G1, L2'=free_37, M2'=8, [ E2>=1 && F2==0 ], cost: 2
     60: f116 -> f130 : E2'=0, M2'=8, [ E2==0 ], cost: 1
     55: f0 -> f116 : C'=7, L'=free_56, V'=0, F1'=0, G1'=free_60, P1'=free_41, Q1_1'=0, U1'=free_60, A2'=0, E2'=free_41, F2'=-1+free_41, M2'=9, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_56, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_56, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_65, K3'=free_65, L3'=free_65, M3'=free_70, N3'=free_59, O3'=free_64, P3'=free_69, Q3_1'=0, R3'=free_58, S3'=free_63, T3'=free_68, U3'=free_62, V3'=free_67, W3'=free_57, X3'=0, Y3'=0, Z3'=free_61, A4'=free_66, B4'=7, C4'=7, [ free_56>=1 && free_60>=1 && free_41>=1 && 0==0 ], cost: 2
     56: f0 -> f116 : C'=free_71, L'=free_72, V'=0, F1'=0, G1'=free_78, P1'=free_41, Q1_1'=0, U1'=free_78, A2'=0, E2'=free_41, F2'=-1+free_41, M2'=9, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_72, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_72, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_84, K3'=free_84, L3'=free_84, M3'=free_90, N3'=free_76, O3'=free_82, P3'=free_88, Q3_1'=0, R3'=free_74, S3'=free_81, T3'=free_87, U3'=free_80, V3'=free_86, W3'=free_73, X3'=0, Y3'=0, Z3'=free_79, A4'=free_85, B4'=free_71, C4'=free_71, D4'=3, E4'=1, F4'=free_71, G4'=free_77, H4'=free_83, Q4'=free_89, J4'=free_75, K4'=1, [ 6>=free_71 && free_72>=1 && free_78>=1 && free_41>=1 && 0==0 ], cost: 2
     57: f0 -> f116 : C'=free_91, L'=free_92, V'=0, F1'=0, G1'=free_98, P1'=free_41, Q1_1'=0, U1'=free_98, A2'=0, E2'=free_41, F2'=-1+free_41, M2'=9, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_92, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_92, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_104, K3'=free_104, L3'=free_104, M3'=free_110, N3'=free_96, O3'=free_102, P3'=free_108, Q3_1'=0, R3'=free_94, S3'=free_101, T3'=free_107, U3'=free_100, V3'=free_106, W3'=free_93, X3'=0, Y3'=0, Z3'=free_99, A4'=free_105, B4'=free_91, C4'=free_91, D4'=3, E4'=1, F4'=free_91, G4'=free_97, H4'=free_103, Q4'=free_109, J4'=free_95, K4'=1, [ free_91>=8 && free_92>=1 && free_98>=1 && free_41>=1 && 0==0 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
     27: f185 -> f195 : C'=free_20, B1'=0, G1'=1, [ E1>=1+F1 ], cost: 1
     28: f185 -> f195 : C'=free_21, B1'=0, F1'=0, G1'=1, [ F1>=E1 ], cost: 1
     12: f230 -> f130 : U'=T, [ T==U ], cost: 1
     18: f230 -> f130 : V'=1, [ T>=1+U ], cost: 1
     19: f230 -> f130 : V'=1, [ U>=1+T ], cost: 1
     90: f130 -> f185 : B'=0, C'=0, D'=0, E'=0, F'=0, V'=0, H1'=3, Q1'=2, J1'=0, K1'=free_22, L1'=free_23, M1'=1, N1'=free_27, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_30, X1'=free_31, Y1'=1, Z1'=0, [ 0>=V1 && V==0 && 0>=P1 && 6>=0 && 0==0 ], cost: 4
     91: f130 -> f185 : B'=0, C'=0, D'=0, E'=0, F'=0, V'=0, H1'=3, Q1'=2, J1'=0, K1'=free_22, L1'=free_23, M1'=1, N1'=free_28, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_30, X1'=free_31, Y1'=1, Z1'=0, [ 0>=V1 && V==0 && P1>=2 && 6>=0 && 0==0 ], cost: 4
     92: f130 -> f185 : B'=0, C'=0, D'=0, E'=0, F'=0, V'=0, H1'=3, Q1'=2, J1'=0, K1'=free_22, L1'=free_23, M1'=1, N1'=free_27, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_32, X1'=free_33, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, [ V1>=1 && V1>=1+A2 && V==0 && 0>=P1 && 6>=0 && 0==0 ], cost: 4
     93: f130 -> f185 : B'=0, C'=0, D'=0, E'=0, F'=0, V'=0, H1'=3, Q1'=2, J1'=0, K1'=free_22, L1'=free_23, M1'=1, N1'=free_28, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_32, X1'=free_33, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, [ V1>=1 && V1>=1+A2 && V==0 && P1>=2 && 6>=0 && 0==0 ], cost: 4
     94: f130 -> f185 : B'=0, C'=0, D'=0, E'=0, F'=0, V'=0, H1'=3, Q1'=2, J1'=0, K1'=free_22, L1'=free_23, M1'=1, N1'=free_28, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_34, X1'=free_35, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, C2'=0, [ A2>=V1 && V1>=1 && V==0 && P1>=2 && 6>=0 && 0==0 ], cost: 4
     65: f130 -> f195 : C'=free_29, V'=0, B1'=0, G1'=U1, P1'=1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_30, X1'=free_31, Y1'=1, Z1'=0, [ 0>=V1 && V==0 && P1==1 ], cost: 2
     68: f130 -> f195 : C'=free_29, V'=0, B1'=0, G1'=U1, P1'=1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_32, X1'=free_33, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, [ V1>=1 && V1>=1+A2 && V==0 && P1==1 ], cost: 2
     71: f130 -> f195 : C'=free_29, V'=0, B1'=0, G1'=U1, P1'=1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_34, X1'=free_35, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, C2'=0, [ A2>=V1 && V1>=1 && V==0 && P1==1 ], cost: 2
     61: f130 -> [21] : D2'=0, [ 0>=1+V ], cost: INF
     62: f130 -> [21] : D2'=0, [ V>=1 ], cost: INF
     95: f195 -> f230 : C'=4, H'=free_15, Q'=free_17, J'=free_18, K'=L, M'=free_19, N'=free_16, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, T'=free_7, W'=free_6, A1'=B1, C1'=B1, D1'=1, [ C==4 && 0==0 && 6>=free_6 ], cost: 3
     96: f195 -> f230 : C'=4, H'=free_15, Q'=free_17, J'=free_18, K'=L, M'=free_19, N'=free_16, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, T'=free_8, W'=free_6, A1'=B1, C1'=B1, D1'=1, [ C==4 && 0==0 && free_6>=8 ], cost: 3
     98: f195 -> f230 : C'=7, H'=free, Q'=free_2, J'=free_3, K'=L, M'=free_4, N'=free_1, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, T'=free_7, W'=free_6, A1'=B1, C1'=B1, [ C>=5 && C==7 && 0==0 && 6>=free_6 ], cost: 4
     99: f195 -> f230 : C'=7, H'=free, Q'=free_2, J'=free_3, K'=L, M'=free_4, N'=free_1, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, T'=free_8, W'=free_6, A1'=B1, C1'=B1, [ C>=5 && C==7 && 0==0 && free_6>=8 ], cost: 4
     74: f195 -> f130 : A1'=B1, C1'=B1, [ 3>=C && 6>=C ], cost: 2
     76: f195 -> f130 : A1'=B1, C1'=B1, [ C>=5 && 6>=C ], cost: 2
     77: f195 -> f130 : A1'=B1, C1'=B1, [ C>=5 && C>=8 ], cost: 2
     97: f195 -> f130 : C'=4, H'=free_15, Q'=free_17, J'=free_18, K'=L, M'=free_19, N'=free_16, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=7, V'=1, W'=7, A1'=B1, C1'=B1, D1'=1, [ C==4 && 0==0 && free_6==7 ], cost: 3
    100: f195 -> f130 : C'=7, H'=free, Q'=free_2, J'=free_3, K'=L, M'=free_4, N'=free_1, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=7, V'=1, W'=7, A1'=B1, C1'=B1, [ C>=5 && C==7 && 0==0 && free_6==7 ], cost: 4
     87: f0 -> f130 : C'=7, L'=free_56, V'=0, F1'=0, G1'=free_60, P1'=free_41, Q1_1'=0, U1'=free_60, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_60, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_56, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_56, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_65, K3'=free_65, L3'=free_65, M3'=free_70, N3'=free_59, O3'=free_64, P3'=free_69, Q3_1'=0, R3'=free_58, S3'=free_63, T3'=free_68, U3'=free_62, V3'=free_67, W3'=free_57, X3'=0, Y3'=0, Z3'=free_61, A4'=free_66, B4'=7, C4'=7, [ free_56>=1 && free_60>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 ], cost: 4
     88: f0 -> f130 : C'=free_71, L'=free_72, V'=0, F1'=0, G1'=free_78, P1'=free_41, Q1_1'=0, U1'=free_78, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_78, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_72, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_72, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_84, K3'=free_84, L3'=free_84, M3'=free_90, N3'=free_76, O3'=free_82, P3'=free_88, Q3_1'=0, R3'=free_74, S3'=free_81, T3'=free_87, U3'=free_80, V3'=free_86, W3'=free_73, X3'=0, Y3'=0, Z3'=free_79, A4'=free_85, B4'=free_71, C4'=free_71, D4'=3, E4'=1, F4'=free_71, G4'=free_77, H4'=free_83, Q4'=free_89, J4'=free_75, K4'=1, [ 6>=free_71 && free_72>=1 && free_78>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 ], cost: 4
     89: f0 -> f130 : C'=free_91, L'=free_92, V'=0, F1'=0, G1'=free_98, P1'=free_41, Q1_1'=0, U1'=free_98, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_98, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_92, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_92, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_104, K3'=free_104, L3'=free_104, M3'=free_110, N3'=free_96, O3'=free_102, P3'=free_108, Q3_1'=0, R3'=free_94, S3'=free_101, T3'=free_107, U3'=free_100, V3'=free_106, W3'=free_93, X3'=0, Y3'=0, Z3'=free_99, A4'=free_105, B4'=free_91, C4'=free_91, D4'=3, E4'=1, F4'=free_91, G4'=free_97, H4'=free_103, Q4'=free_109, J4'=free_95, K4'=1, [ free_91>=8 && free_92>=1 && free_98>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 ], cost: 4


Applied chaining over branches and pruning:
  Start location: f0
     65: f130 -> f195 : C'=free_29, V'=0, B1'=0, G1'=U1, P1'=1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_30, X1'=free_31, Y1'=1, Z1'=0, [ 0>=V1 && V==0 && P1==1 ], cost: 2
     68: f130 -> f195 : C'=free_29, V'=0, B1'=0, G1'=U1, P1'=1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_32, X1'=free_33, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, [ V1>=1 && V1>=1+A2 && V==0 && P1==1 ], cost: 2
    101: f130 -> f195 : B'=0, C'=free_20, D'=0, E'=0, F'=0, V'=0, B1'=0, G1'=1, H1'=3, Q1'=2, J1'=0, K1'=free_22, L1'=free_23, M1'=1, N1'=free_27, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_30, X1'=free_31, Y1'=1, Z1'=0, [ 0>=V1 && V==0 && 0>=P1 && 6>=0 && 0==0 && E1>=1+F1 ], cost: 5
    104: f130 -> f195 : B'=0, C'=free_21, D'=0, E'=0, F'=0, V'=0, B1'=0, F1'=0, G1'=1, H1'=3, Q1'=2, J1'=0, K1'=free_22, L1'=free_23, M1'=1, N1'=free_28, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_30, X1'=free_31, Y1'=1, Z1'=0, [ 0>=V1 && V==0 && P1>=2 && 6>=0 && 0==0 && F1>=E1 ], cost: 5
    105: f130 -> f195 : B'=0, C'=free_20, D'=0, E'=0, F'=0, V'=0, B1'=0, G1'=1, H1'=3, Q1'=2, J1'=0, K1'=free_22, L1'=free_23, M1'=1, N1'=free_27, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_32, X1'=free_33, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, [ V1>=1 && V1>=1+A2 && V==0 && 0>=P1 && 6>=0 && 0==0 && E1>=1+F1 ], cost: 5
     61: f130 -> [21] : D2'=0, [ 0>=1+V ], cost: INF
     62: f130 -> [21] : D2'=0, [ V>=1 ], cost: INF
     74: f195 -> f130 : A1'=B1, C1'=B1, [ 3>=C && 6>=C ], cost: 2
     76: f195 -> f130 : A1'=B1, C1'=B1, [ C>=5 && 6>=C ], cost: 2
     97: f195 -> f130 : C'=4, H'=free_15, Q'=free_17, J'=free_18, K'=L, M'=free_19, N'=free_16, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=7, V'=1, W'=7, A1'=B1, C1'=B1, D1'=1, [ C==4 && 0==0 && free_6==7 ], cost: 3
    113: f195 -> f130 : C'=4, H'=free_15, Q'=free_17, J'=free_18, K'=L, M'=free_19, N'=free_16, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, T'=free_7, V'=1, W'=free_6, A1'=B1, C1'=B1, D1'=1, [ C==4 && 0==0 && 6>=free_6 && U>=1+free_7 ], cost: 4
    114: f195 -> f130 : C'=4, H'=free_15, Q'=free_17, J'=free_18, K'=L, M'=free_19, N'=free_16, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, T'=free_8, U'=free_8, W'=free_6, A1'=B1, C1'=B1, D1'=1, [ C==4 && 0==0 && free_6>=8 && free_8==U ], cost: 4
     87: f0 -> f130 : C'=7, L'=free_56, V'=0, F1'=0, G1'=free_60, P1'=free_41, Q1_1'=0, U1'=free_60, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_60, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_56, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_56, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_65, K3'=free_65, L3'=free_65, M3'=free_70, N3'=free_59, O3'=free_64, P3'=free_69, Q3_1'=0, R3'=free_58, S3'=free_63, T3'=free_68, U3'=free_62, V3'=free_67, W3'=free_57, X3'=0, Y3'=0, Z3'=free_61, A4'=free_66, B4'=7, C4'=7, [ free_56>=1 && free_60>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 ], cost: 4
     88: f0 -> f130 : C'=free_71, L'=free_72, V'=0, F1'=0, G1'=free_78, P1'=free_41, Q1_1'=0, U1'=free_78, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_78, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_72, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_72, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_84, K3'=free_84, L3'=free_84, M3'=free_90, N3'=free_76, O3'=free_82, P3'=free_88, Q3_1'=0, R3'=free_74, S3'=free_81, T3'=free_87, U3'=free_80, V3'=free_86, W3'=free_73, X3'=0, Y3'=0, Z3'=free_79, A4'=free_85, B4'=free_71, C4'=free_71, D4'=3, E4'=1, F4'=free_71, G4'=free_77, H4'=free_83, Q4'=free_89, J4'=free_75, K4'=1, [ 6>=free_71 && free_72>=1 && free_78>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 ], cost: 4
     89: f0 -> f130 : C'=free_91, L'=free_92, V'=0, F1'=0, G1'=free_98, P1'=free_41, Q1_1'=0, U1'=free_98, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_98, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_92, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_92, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_104, K3'=free_104, L3'=free_104, M3'=free_110, N3'=free_96, O3'=free_102, P3'=free_108, Q3_1'=0, R3'=free_94, S3'=free_101, T3'=free_107, U3'=free_100, V3'=free_106, W3'=free_93, X3'=0, Y3'=0, Z3'=free_99, A4'=free_105, B4'=free_91, C4'=free_91, D4'=3, E4'=1, F4'=free_91, G4'=free_97, H4'=free_103, Q4'=free_109, J4'=free_95, K4'=1, [ free_91>=8 && free_92>=1 && free_98>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 ], cost: 4


Applied chaining over branches and pruning:
  Start location: f0
    123: f130 -> f130 : C'=free_29, V'=0, A1'=0, B1'=0, C1'=0, G1'=U1, P1'=1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_30, X1'=free_31, Y1'=1, Z1'=0, [ 0>=V1 && V==0 && P1==1 && 3>=free_29 && 6>=free_29 ], cost: 4
    124: f130 -> f130 : C'=free_29, V'=0, A1'=0, B1'=0, C1'=0, G1'=U1, P1'=1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_30, X1'=free_31, Y1'=1, Z1'=0, [ 0>=V1 && V==0 && P1==1 && free_29>=5 && 6>=free_29 ], cost: 4
    126: f130 -> f130 : C'=4, H'=free_15, Q'=free_17, J'=free_18, K'=L, M'=free_19, N'=free_16, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, T'=free_7, V'=1, W'=free_6, A1'=0, B1'=0, C1'=0, D1'=1, G1'=U1, P1'=1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_30, X1'=free_31, Y1'=1, Z1'=0, [ 0>=V1 && V==0 && P1==1 && free_29==4 && 0==0 && 6>=free_6 && U>=1+free_7 ], cost: 6
    130: f130 -> f130 : C'=4, H'=free_15, Q'=free_17, J'=free_18, K'=L, M'=free_19, N'=free_16, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=7, V'=1, W'=7, A1'=0, B1'=0, C1'=0, D1'=1, G1'=U1, P1'=1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_32, X1'=free_33, Y1'=1, Z1'=0, A2'=1+A2, B2'=A2, [ V1>=1 && V1>=1+A2 && V==0 && P1==1 && free_29==4 && 0==0 && free_6==7 ], cost: 5
    135: f130 -> f130 : B'=0, C'=4, D'=0, E'=0, F'=0, H'=free_15, Q'=free_17, J'=free_18, K'=L, M'=free_19, N'=free_16, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=7, V'=1, W'=7, A1'=0, B1'=0, C1'=0, D1'=1, G1'=1, H1'=3, Q1'=2, J1'=0, K1'=free_22, L1'=free_23, M1'=1, N1'=free_27, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_30, X1'=free_31, Y1'=1, Z1'=0, [ 0>=V1 && V==0 && 0>=P1 && 6>=0 && 0==0 && E1>=1+F1 && free_20==4 && 0==0 && free_6==7 ], cost: 8
     61: f130 -> [21] : D2'=0, [ 0>=1+V ], cost: INF
     62: f130 -> [21] : D2'=0, [ V>=1 ], cost: INF
     87: f0 -> f130 : C'=7, L'=free_56, V'=0, F1'=0, G1'=free_60, P1'=free_41, Q1_1'=0, U1'=free_60, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_60, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_56, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_56, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_65, K3'=free_65, L3'=free_65, M3'=free_70, N3'=free_59, O3'=free_64, P3'=free_69, Q3_1'=0, R3'=free_58, S3'=free_63, T3'=free_68, U3'=free_62, V3'=free_67, W3'=free_57, X3'=0, Y3'=0, Z3'=free_61, A4'=free_66, B4'=7, C4'=7, [ free_56>=1 && free_60>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 ], cost: 4
     88: f0 -> f130 : C'=free_71, L'=free_72, V'=0, F1'=0, G1'=free_78, P1'=free_41, Q1_1'=0, U1'=free_78, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_78, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_72, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_72, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_84, K3'=free_84, L3'=free_84, M3'=free_90, N3'=free_76, O3'=free_82, P3'=free_88, Q3_1'=0, R3'=free_74, S3'=free_81, T3'=free_87, U3'=free_80, V3'=free_86, W3'=free_73, X3'=0, Y3'=0, Z3'=free_79, A4'=free_85, B4'=free_71, C4'=free_71, D4'=3, E4'=1, F4'=free_71, G4'=free_77, H4'=free_83, Q4'=free_89, J4'=free_75, K4'=1, [ 6>=free_71 && free_72>=1 && free_78>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 ], cost: 4
     89: f0 -> f130 : C'=free_91, L'=free_92, V'=0, F1'=0, G1'=free_98, P1'=free_41, Q1_1'=0, U1'=free_98, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_98, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_92, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_92, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_104, K3'=free_104, L3'=free_104, M3'=free_110, N3'=free_96, O3'=free_102, P3'=free_108, Q3_1'=0, R3'=free_94, S3'=free_101, T3'=free_107, U3'=free_100, V3'=free_106, W3'=free_93, X3'=0, Y3'=0, Z3'=free_99, A4'=free_105, B4'=free_91, C4'=free_91, D4'=3, E4'=1, F4'=free_91, G4'=free_97, H4'=free_103, Q4'=free_109, J4'=free_95, K4'=1, [ free_91>=8 && free_92>=1 && free_98>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 ], cost: 4

Eliminating 5 self-loops for location f130
  Self-Loop 123 has unbounded runtime, resulting in the new transition 148.
  Self-Loop 124 has unbounded runtime, resulting in the new transition 149.
  Self-Loop 126 has the metering function: 1-V, resulting in the new transition 150.
  Self-Loop 130 has the metering function: -V, resulting in the new transition 151.
  Self-Loop 135 has the metering function: 1-V, resulting in the new transition 152.
  Removing the self-loops: 123 124 126 130 135.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
    148: f130 -> [23] : [ 0>=V1 && V==0 && P1==1 && 3>=free_29 ], cost: INF
    149: f130 -> [23] : [ 0>=V1 && V==0 && P1==1 && free_29>=5 && 6>=free_29 ], cost: INF
    150: f130 -> [23] : C'=4, H'=free_15, Q'=free_17, J'=free_18, K'=L, M'=free_19, N'=free_16, O'=0, P'=0, Q_1'=free_5, R'=free_6, S'=free_6, T'=free_7, V'=1, W'=free_6, A1'=0, B1'=0, C1'=0, D1'=1, G1'=U1, P1'=1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_30, X1'=free_31, Y1'=1, Z1'=0, [ 0>=V1 && V==0 && P1==1 && 6>=free_6 && U>=1+free_7 ], cost: 6-6*V
    151: f130 -> [23] : C'=4, H'=free_15, Q'=free_17, J'=free_18, K'=L, M'=free_19, N'=free_16, O'=0, P'=0, Q_1'=free_5, R'=7, S'=7, V'=1, W'=7, A1'=0, B1'=0, C1'=0, D1'=1, G1'=U1, P1'=1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_32, X1'=free_33, Y1'=1, Z1'=0, A2'=A2-V, B2'=-1+A2-V, [ V1>=1 && V1>=1+A2 && V==0 && P1==1 ], cost: -5*V
    152: f130 -> [23] : B'=0, C'=4, D'=0, E'=0, F'=0, H'=free_15, Q'=free_17, J'=free_18, K'=L, M'=free_19, N'=free_16, O'=0, P'=0, Q_1'=free_5, R'=7, S'=7, V'=1, W'=7, A1'=0, B1'=0, C1'=0, D1'=1, G1'=1, H1'=3, Q1'=2, J1'=0, K1'=free_22, L1'=free_23, M1'=1, N1'=free_27, O1'=-1, Q1_1'=0, R1'=0, S1'=0, T1'=0, W1'=free_30, X1'=free_31, Y1'=1, Z1'=0, [ 0>=V1 && V==0 && 0>=P1 && E1>=1+F1 ], cost: 8-8*V
     87: f0 -> f130 : C'=7, L'=free_56, V'=0, F1'=0, G1'=free_60, P1'=free_41, Q1_1'=0, U1'=free_60, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_60, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_56, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_56, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_65, K3'=free_65, L3'=free_65, M3'=free_70, N3'=free_59, O3'=free_64, P3'=free_69, Q3_1'=0, R3'=free_58, S3'=free_63, T3'=free_68, U3'=free_62, V3'=free_67, W3'=free_57, X3'=0, Y3'=0, Z3'=free_61, A4'=free_66, B4'=7, C4'=7, [ free_56>=1 && free_60>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 ], cost: 4
     88: f0 -> f130 : C'=free_71, L'=free_72, V'=0, F1'=0, G1'=free_78, P1'=free_41, Q1_1'=0, U1'=free_78, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_78, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_72, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_72, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_84, K3'=free_84, L3'=free_84, M3'=free_90, N3'=free_76, O3'=free_82, P3'=free_88, Q3_1'=0, R3'=free_74, S3'=free_81, T3'=free_87, U3'=free_80, V3'=free_86, W3'=free_73, X3'=0, Y3'=0, Z3'=free_79, A4'=free_85, B4'=free_71, C4'=free_71, D4'=3, E4'=1, F4'=free_71, G4'=free_77, H4'=free_83, Q4'=free_89, J4'=free_75, K4'=1, [ 6>=free_71 && free_72>=1 && free_78>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 ], cost: 4
     89: f0 -> f130 : C'=free_91, L'=free_92, V'=0, F1'=0, G1'=free_98, P1'=free_41, Q1_1'=0, U1'=free_98, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_98, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_92, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_92, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_104, K3'=free_104, L3'=free_104, M3'=free_110, N3'=free_96, O3'=free_102, P3'=free_108, Q3_1'=0, R3'=free_94, S3'=free_101, T3'=free_107, U3'=free_100, V3'=free_106, W3'=free_93, X3'=0, Y3'=0, Z3'=free_99, A4'=free_105, B4'=free_91, C4'=free_91, D4'=3, E4'=1, F4'=free_91, G4'=free_97, H4'=free_103, Q4'=free_109, J4'=free_95, K4'=1, [ free_91>=8 && free_92>=1 && free_98>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 ], cost: 4
     61: [23] -> [21] : D2'=0, [ 0>=1+V ], cost: INF
     62: [23] -> [21] : D2'=0, [ V>=1 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
    153: f0 -> [23] : C'=7, L'=free_56, V'=0, F1'=0, G1'=free_60, P1'=free_41, Q1_1'=0, U1'=free_60, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_60, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_56, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_56, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_65, K3'=free_65, L3'=free_65, M3'=free_70, N3'=free_59, O3'=free_64, P3'=free_69, Q3_1'=0, R3'=free_58, S3'=free_63, T3'=free_68, U3'=free_62, V3'=free_67, W3'=free_57, X3'=0, Y3'=0, Z3'=free_61, A4'=free_66, B4'=7, C4'=7, [ free_56>=1 && free_60>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && 3>=free_29 ], cost: INF
    154: f0 -> [23] : C'=7, L'=free_56, V'=0, F1'=0, G1'=free_60, P1'=free_41, Q1_1'=0, U1'=free_60, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_60, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_56, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_56, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_65, K3'=free_65, L3'=free_65, M3'=free_70, N3'=free_59, O3'=free_64, P3'=free_69, Q3_1'=0, R3'=free_58, S3'=free_63, T3'=free_68, U3'=free_62, V3'=free_67, W3'=free_57, X3'=0, Y3'=0, Z3'=free_61, A4'=free_66, B4'=7, C4'=7, [ free_56>=1 && free_60>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && free_29>=5 && 6>=free_29 ], cost: INF
    158: f0 -> [23] : C'=free_71, L'=free_72, V'=0, F1'=0, G1'=free_78, P1'=free_41, Q1_1'=0, U1'=free_78, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_78, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_72, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_72, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_84, K3'=free_84, L3'=free_84, M3'=free_90, N3'=free_76, O3'=free_82, P3'=free_88, Q3_1'=0, R3'=free_74, S3'=free_81, T3'=free_87, U3'=free_80, V3'=free_86, W3'=free_73, X3'=0, Y3'=0, Z3'=free_79, A4'=free_85, B4'=free_71, C4'=free_71, D4'=3, E4'=1, F4'=free_71, G4'=free_77, H4'=free_83, Q4'=free_89, J4'=free_75, K4'=1, [ 6>=free_71 && free_72>=1 && free_78>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && free_29>=5 && 6>=free_29 ], cost: INF
    161: f0 -> [23] : C'=free_91, L'=free_92, V'=0, F1'=0, G1'=free_98, P1'=free_41, Q1_1'=0, U1'=free_98, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_98, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_92, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_92, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_104, K3'=free_104, L3'=free_104, M3'=free_110, N3'=free_96, O3'=free_102, P3'=free_108, Q3_1'=0, R3'=free_94, S3'=free_101, T3'=free_107, U3'=free_100, V3'=free_106, W3'=free_93, X3'=0, Y3'=0, Z3'=free_99, A4'=free_105, B4'=free_91, C4'=free_91, D4'=3, E4'=1, F4'=free_91, G4'=free_97, H4'=free_103, Q4'=free_109, J4'=free_95, K4'=1, [ free_91>=8 && free_92>=1 && free_98>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && 3>=free_29 ], cost: INF
    162: f0 -> [23] : C'=free_91, L'=free_92, V'=0, F1'=0, G1'=free_98, P1'=free_41, Q1_1'=0, U1'=free_98, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_98, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_92, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_92, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_104, K3'=free_104, L3'=free_104, M3'=free_110, N3'=free_96, O3'=free_102, P3'=free_108, Q3_1'=0, R3'=free_94, S3'=free_101, T3'=free_107, U3'=free_100, V3'=free_106, W3'=free_93, X3'=0, Y3'=0, Z3'=free_99, A4'=free_105, B4'=free_91, C4'=free_91, D4'=3, E4'=1, F4'=free_91, G4'=free_97, H4'=free_103, Q4'=free_109, J4'=free_95, K4'=1, [ free_91>=8 && free_92>=1 && free_98>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && free_29>=5 && 6>=free_29 ], cost: INF
     61: [23] -> [21] : D2'=0, [ 0>=1+V ], cost: INF
     62: [23] -> [21] : D2'=0, [ V>=1 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
    165: f0 -> [24] : C'=7, L'=free_56, V'=0, F1'=0, G1'=free_60, P1'=free_41, Q1_1'=0, U1'=free_60, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_60, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_56, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_56, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_65, K3'=free_65, L3'=free_65, M3'=free_70, N3'=free_59, O3'=free_64, P3'=free_69, Q3_1'=0, R3'=free_58, S3'=free_63, T3'=free_68, U3'=free_62, V3'=free_67, W3'=free_57, X3'=0, Y3'=0, Z3'=free_61, A4'=free_66, B4'=7, C4'=7, [ free_56>=1 && free_60>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && 3>=free_29 ], cost: INF
    166: f0 -> [25] : C'=7, L'=free_56, V'=0, F1'=0, G1'=free_60, P1'=free_41, Q1_1'=0, U1'=free_60, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_60, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_56, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_56, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_65, K3'=free_65, L3'=free_65, M3'=free_70, N3'=free_59, O3'=free_64, P3'=free_69, Q3_1'=0, R3'=free_58, S3'=free_63, T3'=free_68, U3'=free_62, V3'=free_67, W3'=free_57, X3'=0, Y3'=0, Z3'=free_61, A4'=free_66, B4'=7, C4'=7, [ free_56>=1 && free_60>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && 3>=free_29 ], cost: INF
    167: f0 -> [26] : C'=7, L'=free_56, V'=0, F1'=0, G1'=free_60, P1'=free_41, Q1_1'=0, U1'=free_60, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_60, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_56, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_56, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_65, K3'=free_65, L3'=free_65, M3'=free_70, N3'=free_59, O3'=free_64, P3'=free_69, Q3_1'=0, R3'=free_58, S3'=free_63, T3'=free_68, U3'=free_62, V3'=free_67, W3'=free_57, X3'=0, Y3'=0, Z3'=free_61, A4'=free_66, B4'=7, C4'=7, [ free_56>=1 && free_60>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && free_29>=5 && 6>=free_29 ], cost: INF
    168: f0 -> [27] : C'=7, L'=free_56, V'=0, F1'=0, G1'=free_60, P1'=free_41, Q1_1'=0, U1'=free_60, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_60, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_56, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_56, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_65, K3'=free_65, L3'=free_65, M3'=free_70, N3'=free_59, O3'=free_64, P3'=free_69, Q3_1'=0, R3'=free_58, S3'=free_63, T3'=free_68, U3'=free_62, V3'=free_67, W3'=free_57, X3'=0, Y3'=0, Z3'=free_61, A4'=free_66, B4'=7, C4'=7, [ free_56>=1 && free_60>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && free_29>=5 && 6>=free_29 ], cost: INF
    169: f0 -> [28] : C'=free_71, L'=free_72, V'=0, F1'=0, G1'=free_78, P1'=free_41, Q1_1'=0, U1'=free_78, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_78, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_72, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_72, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_84, K3'=free_84, L3'=free_84, M3'=free_90, N3'=free_76, O3'=free_82, P3'=free_88, Q3_1'=0, R3'=free_74, S3'=free_81, T3'=free_87, U3'=free_80, V3'=free_86, W3'=free_73, X3'=0, Y3'=0, Z3'=free_79, A4'=free_85, B4'=free_71, C4'=free_71, D4'=3, E4'=1, F4'=free_71, G4'=free_77, H4'=free_83, Q4'=free_89, J4'=free_75, K4'=1, [ 6>=free_71 && free_72>=1 && free_78>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && free_29>=5 && 6>=free_29 ], cost: INF
    170: f0 -> [29] : C'=free_71, L'=free_72, V'=0, F1'=0, G1'=free_78, P1'=free_41, Q1_1'=0, U1'=free_78, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_78, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_72, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_72, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_84, K3'=free_84, L3'=free_84, M3'=free_90, N3'=free_76, O3'=free_82, P3'=free_88, Q3_1'=0, R3'=free_74, S3'=free_81, T3'=free_87, U3'=free_80, V3'=free_86, W3'=free_73, X3'=0, Y3'=0, Z3'=free_79, A4'=free_85, B4'=free_71, C4'=free_71, D4'=3, E4'=1, F4'=free_71, G4'=free_77, H4'=free_83, Q4'=free_89, J4'=free_75, K4'=1, [ 6>=free_71 && free_72>=1 && free_78>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && free_29>=5 && 6>=free_29 ], cost: INF
    171: f0 -> [30] : C'=free_91, L'=free_92, V'=0, F1'=0, G1'=free_98, P1'=free_41, Q1_1'=0, U1'=free_98, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_98, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_92, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_92, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_104, K3'=free_104, L3'=free_104, M3'=free_110, N3'=free_96, O3'=free_102, P3'=free_108, Q3_1'=0, R3'=free_94, S3'=free_101, T3'=free_107, U3'=free_100, V3'=free_106, W3'=free_93, X3'=0, Y3'=0, Z3'=free_99, A4'=free_105, B4'=free_91, C4'=free_91, D4'=3, E4'=1, F4'=free_91, G4'=free_97, H4'=free_103, Q4'=free_109, J4'=free_95, K4'=1, [ free_91>=8 && free_92>=1 && free_98>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && 3>=free_29 ], cost: INF
    172: f0 -> [31] : C'=free_91, L'=free_92, V'=0, F1'=0, G1'=free_98, P1'=free_41, Q1_1'=0, U1'=free_98, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_98, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_92, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_92, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_104, K3'=free_104, L3'=free_104, M3'=free_110, N3'=free_96, O3'=free_102, P3'=free_108, Q3_1'=0, R3'=free_94, S3'=free_101, T3'=free_107, U3'=free_100, V3'=free_106, W3'=free_93, X3'=0, Y3'=0, Z3'=free_99, A4'=free_105, B4'=free_91, C4'=free_91, D4'=3, E4'=1, F4'=free_91, G4'=free_97, H4'=free_103, Q4'=free_109, J4'=free_95, K4'=1, [ free_91>=8 && free_92>=1 && free_98>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && 3>=free_29 ], cost: INF
    173: f0 -> [32] : C'=free_91, L'=free_92, V'=0, F1'=0, G1'=free_98, P1'=free_41, Q1_1'=0, U1'=free_98, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_98, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_92, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_92, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_104, K3'=free_104, L3'=free_104, M3'=free_110, N3'=free_96, O3'=free_102, P3'=free_108, Q3_1'=0, R3'=free_94, S3'=free_101, T3'=free_107, U3'=free_100, V3'=free_106, W3'=free_93, X3'=0, Y3'=0, Z3'=free_99, A4'=free_105, B4'=free_91, C4'=free_91, D4'=3, E4'=1, F4'=free_91, G4'=free_97, H4'=free_103, Q4'=free_109, J4'=free_95, K4'=1, [ free_91>=8 && free_92>=1 && free_98>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && free_29>=5 && 6>=free_29 ], cost: INF
    174: f0 -> [33] : C'=free_91, L'=free_92, V'=0, F1'=0, G1'=free_98, P1'=free_41, Q1_1'=0, U1'=free_98, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_98, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_92, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_92, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_104, K3'=free_104, L3'=free_104, M3'=free_110, N3'=free_96, O3'=free_102, P3'=free_108, Q3_1'=0, R3'=free_94, S3'=free_101, T3'=free_107, U3'=free_100, V3'=free_106, W3'=free_93, X3'=0, Y3'=0, Z3'=free_99, A4'=free_105, B4'=free_91, C4'=free_91, D4'=3, E4'=1, F4'=free_91, G4'=free_97, H4'=free_103, Q4'=free_109, J4'=free_95, K4'=1, [ free_91>=8 && free_92>=1 && free_98>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && free_29>=5 && 6>=free_29 ], cost: INF


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
    165: f0 -> [24] : C'=7, L'=free_56, V'=0, F1'=0, G1'=free_60, P1'=free_41, Q1_1'=0, U1'=free_60, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_60, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_56, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_56, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_65, K3'=free_65, L3'=free_65, M3'=free_70, N3'=free_59, O3'=free_64, P3'=free_69, Q3_1'=0, R3'=free_58, S3'=free_63, T3'=free_68, U3'=free_62, V3'=free_67, W3'=free_57, X3'=0, Y3'=0, Z3'=free_61, A4'=free_66, B4'=7, C4'=7, [ free_56>=1 && free_60>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && 3>=free_29 ], cost: INF
    166: f0 -> [25] : C'=7, L'=free_56, V'=0, F1'=0, G1'=free_60, P1'=free_41, Q1_1'=0, U1'=free_60, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_60, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_56, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_56, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_65, K3'=free_65, L3'=free_65, M3'=free_70, N3'=free_59, O3'=free_64, P3'=free_69, Q3_1'=0, R3'=free_58, S3'=free_63, T3'=free_68, U3'=free_62, V3'=free_67, W3'=free_57, X3'=0, Y3'=0, Z3'=free_61, A4'=free_66, B4'=7, C4'=7, [ free_56>=1 && free_60>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && 3>=free_29 ], cost: INF
    167: f0 -> [26] : C'=7, L'=free_56, V'=0, F1'=0, G1'=free_60, P1'=free_41, Q1_1'=0, U1'=free_60, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_60, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_56, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_56, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_65, K3'=free_65, L3'=free_65, M3'=free_70, N3'=free_59, O3'=free_64, P3'=free_69, Q3_1'=0, R3'=free_58, S3'=free_63, T3'=free_68, U3'=free_62, V3'=free_67, W3'=free_57, X3'=0, Y3'=0, Z3'=free_61, A4'=free_66, B4'=7, C4'=7, [ free_56>=1 && free_60>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && free_29>=5 && 6>=free_29 ], cost: INF
    168: f0 -> [27] : C'=7, L'=free_56, V'=0, F1'=0, G1'=free_60, P1'=free_41, Q1_1'=0, U1'=free_60, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_60, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_56, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_56, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_65, K3'=free_65, L3'=free_65, M3'=free_70, N3'=free_59, O3'=free_64, P3'=free_69, Q3_1'=0, R3'=free_58, S3'=free_63, T3'=free_68, U3'=free_62, V3'=free_67, W3'=free_57, X3'=0, Y3'=0, Z3'=free_61, A4'=free_66, B4'=7, C4'=7, [ free_56>=1 && free_60>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && free_29>=5 && 6>=free_29 ], cost: INF
    169: f0 -> [28] : C'=free_71, L'=free_72, V'=0, F1'=0, G1'=free_78, P1'=free_41, Q1_1'=0, U1'=free_78, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_78, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_72, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_72, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_84, K3'=free_84, L3'=free_84, M3'=free_90, N3'=free_76, O3'=free_82, P3'=free_88, Q3_1'=0, R3'=free_74, S3'=free_81, T3'=free_87, U3'=free_80, V3'=free_86, W3'=free_73, X3'=0, Y3'=0, Z3'=free_79, A4'=free_85, B4'=free_71, C4'=free_71, D4'=3, E4'=1, F4'=free_71, G4'=free_77, H4'=free_83, Q4'=free_89, J4'=free_75, K4'=1, [ 6>=free_71 && free_72>=1 && free_78>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && free_29>=5 && 6>=free_29 ], cost: INF
    170: f0 -> [29] : C'=free_71, L'=free_72, V'=0, F1'=0, G1'=free_78, P1'=free_41, Q1_1'=0, U1'=free_78, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_78, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_72, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_72, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_84, K3'=free_84, L3'=free_84, M3'=free_90, N3'=free_76, O3'=free_82, P3'=free_88, Q3_1'=0, R3'=free_74, S3'=free_81, T3'=free_87, U3'=free_80, V3'=free_86, W3'=free_73, X3'=0, Y3'=0, Z3'=free_79, A4'=free_85, B4'=free_71, C4'=free_71, D4'=3, E4'=1, F4'=free_71, G4'=free_77, H4'=free_83, Q4'=free_89, J4'=free_75, K4'=1, [ 6>=free_71 && free_72>=1 && free_78>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && free_29>=5 && 6>=free_29 ], cost: INF
    171: f0 -> [30] : C'=free_91, L'=free_92, V'=0, F1'=0, G1'=free_98, P1'=free_41, Q1_1'=0, U1'=free_98, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_98, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_92, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_92, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_104, K3'=free_104, L3'=free_104, M3'=free_110, N3'=free_96, O3'=free_102, P3'=free_108, Q3_1'=0, R3'=free_94, S3'=free_101, T3'=free_107, U3'=free_100, V3'=free_106, W3'=free_93, X3'=0, Y3'=0, Z3'=free_99, A4'=free_105, B4'=free_91, C4'=free_91, D4'=3, E4'=1, F4'=free_91, G4'=free_97, H4'=free_103, Q4'=free_109, J4'=free_95, K4'=1, [ free_91>=8 && free_92>=1 && free_98>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && 3>=free_29 ], cost: INF
    172: f0 -> [31] : C'=free_91, L'=free_92, V'=0, F1'=0, G1'=free_98, P1'=free_41, Q1_1'=0, U1'=free_98, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_98, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_92, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_92, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_104, K3'=free_104, L3'=free_104, M3'=free_110, N3'=free_96, O3'=free_102, P3'=free_108, Q3_1'=0, R3'=free_94, S3'=free_101, T3'=free_107, U3'=free_100, V3'=free_106, W3'=free_93, X3'=0, Y3'=0, Z3'=free_99, A4'=free_105, B4'=free_91, C4'=free_91, D4'=3, E4'=1, F4'=free_91, G4'=free_97, H4'=free_103, Q4'=free_109, J4'=free_95, K4'=1, [ free_91>=8 && free_92>=1 && free_98>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && 3>=free_29 ], cost: INF
    173: f0 -> [32] : C'=free_91, L'=free_92, V'=0, F1'=0, G1'=free_98, P1'=free_41, Q1_1'=0, U1'=free_98, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_98, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_92, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_92, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_104, K3'=free_104, L3'=free_104, M3'=free_110, N3'=free_96, O3'=free_102, P3'=free_108, Q3_1'=0, R3'=free_94, S3'=free_101, T3'=free_107, U3'=free_100, V3'=free_106, W3'=free_93, X3'=0, Y3'=0, Z3'=free_99, A4'=free_105, B4'=free_91, C4'=free_91, D4'=3, E4'=1, F4'=free_91, G4'=free_97, H4'=free_103, Q4'=free_109, J4'=free_95, K4'=1, [ free_91>=8 && free_92>=1 && free_98>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && free_29>=5 && 6>=free_29 ], cost: INF
    174: f0 -> [33] : C'=free_91, L'=free_92, V'=0, F1'=0, G1'=free_98, P1'=free_41, Q1_1'=0, U1'=free_98, A2'=0, E2'=0, F2'=-2+free_41, G2'=0, H2'=6, Q2'=1, J2'=5, K2'=free_98, L2'=free_37, M2'=8, N2'=0, O2'=0, P2'=free_38, Q2_1'=free_40, R2'=free_42, S2'=free_92, T2'=0, U2'=free_43, V2'=1, W2'=0, X2'=P1, Y2'=free_39, Z2'=0, B3'=free_92, C3'=0, D3'=0, E3'=0, F3'=0, G3'=0, H3'=256, Q3'=0, J3'=free_104, K3'=free_104, L3'=free_104, M3'=free_110, N3'=free_96, O3'=free_102, P3'=free_108, Q3_1'=0, R3'=free_94, S3'=free_101, T3'=free_107, U3'=free_100, V3'=free_106, W3'=free_93, X3'=0, Y3'=0, Z3'=free_99, A4'=free_105, B4'=free_91, C4'=free_91, D4'=3, E4'=1, F4'=free_91, G4'=free_97, H4'=free_103, Q4'=free_109, J4'=free_95, K4'=1, [ free_91>=8 && free_92>=1 && free_98>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && free_29>=5 && 6>=free_29 ], cost: INF


Computing complexity for remaining 10 transitions.

Found new complexity INF, because: INF sat.


The final runtime is determined by this resulting transition:
  Final Guard: free_56>=1 && free_60>=1 && free_41>=1 && 0==0 && free_41>=1 && -1+free_41==0 && 0>=V1 && 0==0 && free_41==1 && 3>=free_29
  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,?)