Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f26
      4: f29 -> f29 : B'=-1+B, E'=free_26, F'=C, G'=free_24, M'=free_25, N'=B, O'=A, [ A>=free_26 && A>=0 && B>=1 && free_26>=2 && 0>=1+free_27 && 0>=1+free_24 ], cost: 1
      5: f29 -> f29 : B'=-1+B, E'=free_30, F'=C, G'=free_28, M'=free_29, N'=B, O'=A, [ A>=free_30 && A>=0 && B>=1 && free_30>=2 && 0>=1+free_31 && free_28>=1 ], cost: 1
      6: f29 -> f29 : B'=-1+B, E'=free_34, F'=C, G'=free_32, M'=free_33, N'=B, O'=A, [ A>=free_34 && A>=0 && B>=1 && free_34>=2 && free_35>=1 && 0>=1+free_32 ], cost: 1
      7: f29 -> f29 : B'=-1+B, E'=free_38, F'=C, G'=free_36, M'=free_37, N'=B, O'=A, [ A>=free_38 && A>=0 && B>=1 && free_38>=2 && free_39>=1 && free_36>=1 ], cost: 1
      0: f29 -> f34 : D'=1, E'=free_3, F'=free_1, G'=0, H'=Q, J'=free_2, K'=1+Q, L'=free_4, M'=free, [ A>=0 && B>=1 && free_3>=2 && 0>=1+C && free_5>=free_3 && 0>=1+free_1 && D==1 ], cost: 1
      1: f29 -> f34 : D'=1, E'=free_9, F'=free_7, G'=0, H'=Q, J'=free_8, K'=1+Q, L'=free_10, M'=free_6, [ A>=0 && B>=1 && free_9>=2 && 0>=1+C && free_11>=free_9 && free_7>=1 && D==1 ], cost: 1
      2: f29 -> f34 : D'=1, E'=free_15, F'=free_13, G'=0, H'=Q, J'=free_14, K'=1+Q, L'=free_16, M'=free_12, [ A>=0 && B>=1 && free_15>=2 && C>=1 && free_17>=free_15 && 0>=1+free_13 && D==1 ], cost: 1
      3: f29 -> f34 : D'=1, E'=free_21, F'=free_19, G'=0, H'=Q, J'=free_20, K'=1+Q, L'=free_22, M'=free_18, [ A>=0 && B>=1 && free_21>=2 && C>=1 && free_23>=free_21 && free_19>=1 && D==1 ], cost: 1
    182: f29 -> f17 : B'=free_1267, C'=F, E'=free_1268, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1270>=free_1268 && 0>=free_1271 && free_1269>=2 && A>=free_1269 && 0>=free_1267 && A>=0 && free_1268>=2 && 0>=B && F>=1 && 0>=1+C && 0>=1+F ], cost: 1
    183: f29 -> f17 : B'=free_1272, C'=F, E'=free_1273, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1275>=free_1273 && 0>=free_1276 && free_1274>=2 && A>=free_1274 && 0>=free_1272 && A>=0 && free_1273>=2 && 0>=B && F>=1 && 0>=1+C ], cost: 1
    184: f29 -> f17 : B'=free_1277, C'=F, E'=free_1278, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1280>=free_1278 && 0>=free_1281 && free_1279>=2 && A>=free_1279 && 0>=free_1277 && A>=0 && free_1278>=2 && 0>=B && F>=1 && C>=1 && 0>=1+F ], cost: 1
    185: f29 -> f17 : B'=free_1282, C'=F, E'=free_1283, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1285>=free_1283 && 0>=free_1286 && free_1284>=2 && A>=free_1284 && 0>=free_1282 && A>=0 && free_1283>=2 && 0>=B && F>=1 && C>=1 ], cost: 1
    186: f29 -> f17 : B'=free_1287, C'=F, E'=free_1288, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1290>=free_1288 && 0>=free_1291 && free_1289>=2 && A>=free_1289 && 0>=free_1287 && A>=0 && free_1288>=2 && 0>=B && 0>=1+F && 0>=1+C ], cost: 1
    187: f29 -> f17 : B'=free_1292, C'=F, E'=free_1293, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1295>=free_1293 && 0>=free_1296 && free_1294>=2 && A>=free_1294 && 0>=free_1292 && A>=0 && free_1293>=2 && 0>=B && 0>=1+F && 0>=1+C && F>=1 ], cost: 1
    188: f29 -> f17 : B'=free_1297, C'=F, E'=free_1298, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1300>=free_1298 && 0>=free_1301 && free_1299>=2 && A>=free_1299 && 0>=free_1297 && A>=0 && free_1298>=2 && 0>=B && 0>=1+F && C>=1 ], cost: 1
    189: f29 -> f17 : B'=free_1302, C'=F, E'=free_1303, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1305>=free_1303 && 0>=free_1306 && free_1304>=2 && A>=free_1304 && 0>=free_1302 && A>=0 && free_1303>=2 && 0>=B && 0>=1+F && C>=1 && F>=1 ], cost: 1
     60: f34 -> f34 : D'=1+D, E'=free_295, F'=free_293, G'=0, Q'=-1+Q, J'=free_294, M'=free_296, E1'=C, F1'=free_292, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_295>=2 && 0>=1+free_297 && 0>=1+free_293 && 0>=1+free_292 ], cost: 1
     61: f34 -> f34 : D'=1+D, E'=free_301, F'=free_299, G'=0, Q'=-1+Q, J'=free_300, M'=free_302, E1'=C, F1'=free_298, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_301>=2 && 0>=1+free_303 && 0>=1+free_299 && free_298>=1 ], cost: 1
     62: f34 -> f34 : D'=1+D, E'=free_307, F'=free_305, G'=0, Q'=-1+Q, J'=free_306, M'=free_308, E1'=C, F1'=free_304, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_307>=2 && 0>=1+free_309 && free_305>=1 && 0>=1+free_304 ], cost: 1
     63: f34 -> f34 : D'=1+D, E'=free_313, F'=free_311, G'=0, Q'=-1+Q, J'=free_312, M'=free_314, E1'=C, F1'=free_310, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_313>=2 && 0>=1+free_315 && free_311>=1 && free_310>=1 ], cost: 1
     64: f34 -> f34 : D'=1+D, E'=free_319, F'=free_317, G'=0, Q'=-1+Q, J'=free_318, M'=free_320, E1'=C, F1'=free_316, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_319>=2 && free_321>=1 && 0>=1+free_317 && 0>=1+free_316 ], cost: 1
     65: f34 -> f34 : D'=1+D, E'=free_325, F'=free_323, G'=0, Q'=-1+Q, J'=free_324, M'=free_326, E1'=C, F1'=free_322, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_325>=2 && free_327>=1 && 0>=1+free_323 && free_322>=1 ], cost: 1
     66: f34 -> f34 : D'=1+D, E'=free_331, F'=free_329, G'=0, Q'=-1+Q, J'=free_330, M'=free_332, E1'=C, F1'=free_328, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_331>=2 && free_333>=1 && free_329>=1 && 0>=1+free_328 ], cost: 1
     67: f34 -> f34 : D'=1+D, E'=free_337, F'=free_335, G'=0, Q'=-1+Q, J'=free_336, M'=free_338, E1'=C, F1'=free_334, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_337>=2 && free_339>=1 && free_335>=1 && free_334>=1 ], cost: 1
     52: f34 -> f35 : B'=-1+B, E'=free_262, F'=free_260, G'=free_261, M'=free_263, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_262>=2 && 0>=1+C && 0>=1+free_261 && 0>=1+free_260 ], cost: 1
     53: f34 -> f35 : B'=-1+B, E'=free_266, F'=free_264, G'=free_265, M'=free_267, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_266>=2 && 0>=1+C && 0>=1+free_265 && free_264>=1 ], cost: 1
     54: f34 -> f35 : B'=-1+B, E'=free_270, F'=free_268, G'=free_269, M'=free_271, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_270>=2 && 0>=1+C && free_269>=1 && 0>=1+free_268 ], cost: 1
     55: f34 -> f35 : B'=-1+B, E'=free_274, F'=free_272, G'=free_273, M'=free_275, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_274>=2 && 0>=1+C && free_273>=1 && free_272>=1 ], cost: 1
     56: f34 -> f35 : B'=-1+B, E'=free_278, F'=free_276, G'=free_277, M'=free_279, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_278>=2 && C>=1 && 0>=1+free_277 && 0>=1+free_276 ], cost: 1
     57: f34 -> f35 : B'=-1+B, E'=free_282, F'=free_280, G'=free_281, M'=free_283, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_282>=2 && C>=1 && 0>=1+free_281 && free_280>=1 ], cost: 1
     58: f34 -> f35 : B'=-1+B, E'=free_286, F'=free_284, G'=free_285, M'=free_287, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_286>=2 && C>=1 && free_285>=1 && 0>=1+free_284 ], cost: 1
     59: f34 -> f35 : B'=-1+B, E'=free_290, F'=free_288, G'=free_289, M'=free_291, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_290>=2 && C>=1 && free_289>=1 && free_288>=1 ], cost: 1
    194: f34 -> f15 : B'=free_1323, C'=0, D'=1+G2, E'=free_1324, G'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1325>=1 && free_1326>=2 && free_1323>=1 && free_1324>=2 && F>=1 && Q>=0 && D>=0 && 0>=1+F && C==0 ], cost: 1
    195: f34 -> f15 : B'=free_1327, C'=0, D'=1+G2, E'=free_1328, G'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1329>=1 && free_1330>=2 && free_1327>=1 && free_1328>=2 && F>=1 && Q>=0 && D>=0 && C==0 ], cost: 1
    196: f34 -> f15 : B'=free_1331, C'=0, D'=1+G2, E'=free_1332, G'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1333>=1 && free_1334>=2 && free_1331>=1 && free_1332>=2 && 0>=1+F && Q>=0 && D>=0 && C==0 ], cost: 1
    197: f34 -> f15 : B'=free_1335, C'=0, D'=1+G2, E'=free_1336, G'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1337>=1 && free_1338>=2 && free_1335>=1 && free_1336>=2 && 0>=1+F && Q>=0 && D>=0 && F>=1 && C==0 ], cost: 1
     16: f30 -> f34 : D'=2, E'=free_83, F'=free_81, G'=0, Q'=-1+H, M'=free_82, R'=C, S'=free_84, T'=free_80, [ B>=1 && H>=0 && free_83>=2 && 0>=1+free_85 && 0>=1+free_81 && 0>=1+free_80 && 1+Q==H && D==2 ], cost: 1
     17: f30 -> f34 : D'=2, E'=free_89, F'=free_87, G'=0, Q'=-1+H, M'=free_88, R'=C, S'=free_90, T'=free_86, [ B>=1 && H>=0 && free_89>=2 && 0>=1+free_91 && 0>=1+free_87 && free_86>=1 && 1+Q==H && D==2 ], cost: 1
     18: f30 -> f34 : D'=2, E'=free_95, F'=free_93, G'=0, Q'=-1+H, M'=free_94, R'=C, S'=free_96, T'=free_92, [ B>=1 && H>=0 && free_95>=2 && 0>=1+free_97 && free_93>=1 && 0>=1+free_92 && 1+Q==H && D==2 ], cost: 1
     19: f30 -> f34 : D'=2, E'=free_101, F'=free_99, G'=0, Q'=-1+H, M'=free_100, R'=C, S'=free_102, T'=free_98, [ B>=1 && H>=0 && free_101>=2 && 0>=1+free_103 && free_99>=1 && free_98>=1 && 1+Q==H && D==2 ], cost: 1
     20: f30 -> f34 : D'=2, E'=free_107, F'=free_105, G'=0, Q'=-1+H, M'=free_106, R'=C, S'=free_108, T'=free_104, [ B>=1 && H>=0 && free_107>=2 && free_109>=1 && 0>=1+free_105 && 0>=1+free_104 && 1+Q==H && D==2 ], cost: 1
     21: f30 -> f34 : D'=2, E'=free_113, F'=free_111, G'=0, Q'=-1+H, M'=free_112, R'=C, S'=free_114, T'=free_110, [ B>=1 && H>=0 && free_113>=2 && free_115>=1 && 0>=1+free_111 && free_110>=1 && 1+Q==H && D==2 ], cost: 1
     22: f30 -> f34 : D'=2, E'=free_119, F'=free_117, G'=0, Q'=-1+H, M'=free_118, R'=C, S'=free_120, T'=free_116, [ B>=1 && H>=0 && free_119>=2 && free_121>=1 && free_117>=1 && 0>=1+free_116 && 1+Q==H && D==2 ], cost: 1
     23: f30 -> f34 : D'=2, E'=free_125, F'=free_123, G'=0, Q'=-1+H, M'=free_124, R'=C, S'=free_126, T'=free_122, [ B>=1 && H>=0 && free_125>=2 && free_127>=1 && free_123>=1 && free_122>=1 && 1+Q==H && D==2 ], cost: 1
      8: f30 -> f35 : B'=-1+B, D'=1, E'=free_43, F'=free_41, G'=free_42, Q'=H, M'=free_44, P'=B, Q_1'=free_40, [ B>=1 && Q>=0 && free_43>=2 && 0>=1+C && 0>=1+free_42 && 0>=1+free_41 && H==Q && D==1 ], cost: 1
      9: f30 -> f35 : B'=-1+B, D'=1, E'=free_48, F'=free_46, G'=free_47, Q'=H, M'=free_49, P'=B, Q_1'=free_45, [ B>=1 && Q>=0 && free_48>=2 && 0>=1+C && 0>=1+free_47 && free_46>=1 && H==Q && D==1 ], cost: 1
     10: f30 -> f35 : B'=-1+B, D'=1, E'=free_53, F'=free_51, G'=free_52, Q'=H, M'=free_54, P'=B, Q_1'=free_50, [ B>=1 && Q>=0 && free_53>=2 && 0>=1+C && free_52>=1 && 0>=1+free_51 && H==Q && D==1 ], cost: 1
     11: f30 -> f35 : B'=-1+B, D'=1, E'=free_58, F'=free_56, G'=free_57, Q'=H, M'=free_59, P'=B, Q_1'=free_55, [ B>=1 && Q>=0 && free_58>=2 && 0>=1+C && free_57>=1 && free_56>=1 && H==Q && D==1 ], cost: 1
     12: f30 -> f35 : B'=-1+B, D'=1, E'=free_63, F'=free_61, G'=free_62, Q'=H, M'=free_64, P'=B, Q_1'=free_60, [ B>=1 && Q>=0 && free_63>=2 && C>=1 && 0>=1+free_62 && 0>=1+free_61 && H==Q && D==1 ], cost: 1
     13: f30 -> f35 : B'=-1+B, D'=1, E'=free_68, F'=free_66, G'=free_67, Q'=H, M'=free_69, P'=B, Q_1'=free_65, [ B>=1 && Q>=0 && free_68>=2 && C>=1 && 0>=1+free_67 && free_66>=1 && H==Q && D==1 ], cost: 1
     14: f30 -> f35 : B'=-1+B, D'=1, E'=free_73, F'=free_71, G'=free_72, Q'=H, M'=free_74, P'=B, Q_1'=free_70, [ B>=1 && Q>=0 && free_73>=2 && C>=1 && free_72>=1 && 0>=1+free_71 && H==Q && D==1 ], cost: 1
     15: f30 -> f35 : B'=-1+B, D'=1, E'=free_78, F'=free_76, G'=free_77, Q'=H, M'=free_79, P'=B, Q_1'=free_75, [ B>=1 && Q>=0 && free_78>=2 && C>=1 && free_77>=1 && free_76>=1 && H==Q && D==1 ], cost: 1
    190: f30 -> f15 : B'=free_1307, C'=0, D'=1+G2, E'=free_1308, G'=0, H'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1307>=1 && free_1308>=2 && F>=1 && free_1309>=1 && free_1310>=2 && 0>=1+F && C==0 && H==0 && D==1 ], cost: 1
    191: f30 -> f15 : B'=free_1311, C'=0, D'=1+G2, E'=free_1312, G'=0, H'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1311>=1 && free_1312>=2 && F>=1 && free_1313>=1 && free_1314>=2 && C==0 && H==0 && D==1 ], cost: 1
    192: f30 -> f15 : B'=free_1315, C'=0, D'=1+G2, E'=free_1316, G'=0, H'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1315>=1 && free_1316>=2 && 0>=1+F && free_1317>=1 && free_1318>=2 && C==0 && H==0 && D==1 ], cost: 1
    193: f30 -> f15 : B'=free_1319, C'=0, D'=1+G2, E'=free_1320, G'=0, H'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1319>=1 && free_1320>=2 && 0>=1+F && free_1321>=1 && free_1322>=2 && F>=1 && C==0 && H==0 && D==1 ], cost: 1
     84: f35 -> f34 : D'=1+D, E'=free_423, F'=free_421, G'=0, Q'=-1+Q, J'=free_422, M'=free_424, Q1'=free_420, M1'=C, N1'=free_425, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_423>=2 && 0>=1+free_426 && 0>=1+free_425 && 0>=1+free_421 && 0>=1+free_420 ], cost: 1
     85: f35 -> f34 : D'=1+D, E'=free_430, F'=free_428, G'=0, Q'=-1+Q, J'=free_429, M'=free_431, Q1'=free_427, M1'=C, N1'=free_432, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_430>=2 && 0>=1+free_433 && 0>=1+free_432 && 0>=1+free_428 && free_427>=1 ], cost: 1
     86: f35 -> f34 : D'=1+D, E'=free_437, F'=free_435, G'=0, Q'=-1+Q, J'=free_436, M'=free_438, Q1'=free_434, M1'=C, N1'=free_439, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_437>=2 && 0>=1+free_440 && 0>=1+free_439 && free_435>=1 && 0>=1+free_434 ], cost: 1
     87: f35 -> f34 : D'=1+D, E'=free_444, F'=free_442, G'=0, Q'=-1+Q, J'=free_443, M'=free_445, Q1'=free_441, M1'=C, N1'=free_446, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_444>=2 && 0>=1+free_447 && 0>=1+free_446 && free_442>=1 && free_441>=1 ], cost: 1
     88: f35 -> f34 : D'=1+D, E'=free_451, F'=free_449, G'=0, Q'=-1+Q, J'=free_450, M'=free_452, Q1'=free_448, M1'=C, N1'=free_453, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_451>=2 && 0>=1+free_454 && free_453>=1 && 0>=1+free_449 && 0>=1+free_448 ], cost: 1
     89: f35 -> f34 : D'=1+D, E'=free_458, F'=free_456, G'=0, Q'=-1+Q, J'=free_457, M'=free_459, Q1'=free_455, M1'=C, N1'=free_460, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_458>=2 && 0>=1+free_461 && free_460>=1 && 0>=1+free_456 && free_455>=1 ], cost: 1
     90: f35 -> f34 : D'=1+D, E'=free_465, F'=free_463, G'=0, Q'=-1+Q, J'=free_464, M'=free_466, Q1'=free_462, M1'=C, N1'=free_467, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_465>=2 && 0>=1+free_468 && free_467>=1 && free_463>=1 && 0>=1+free_462 ], cost: 1
     91: f35 -> f34 : D'=1+D, E'=free_472, F'=free_470, G'=0, Q'=-1+Q, J'=free_471, M'=free_473, Q1'=free_469, M1'=C, N1'=free_474, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_472>=2 && 0>=1+free_475 && free_474>=1 && free_470>=1 && free_469>=1 ], cost: 1
     92: f35 -> f34 : D'=1+D, E'=free_479, F'=free_477, G'=0, Q'=-1+Q, J'=free_478, M'=free_480, Q1'=free_476, M1'=C, N1'=free_481, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_479>=2 && free_482>=1 && 0>=1+free_481 && 0>=1+free_477 && 0>=1+free_476 ], cost: 1
     93: f35 -> f34 : D'=1+D, E'=free_486, F'=free_484, G'=0, Q'=-1+Q, J'=free_485, M'=free_487, Q1'=free_483, M1'=C, N1'=free_488, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_486>=2 && free_489>=1 && 0>=1+free_488 && 0>=1+free_484 && free_483>=1 ], cost: 1
     94: f35 -> f34 : D'=1+D, E'=free_493, F'=free_491, G'=0, Q'=-1+Q, J'=free_492, M'=free_494, Q1'=free_490, M1'=C, N1'=free_495, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_493>=2 && free_496>=1 && 0>=1+free_495 && free_491>=1 && 0>=1+free_490 ], cost: 1
     95: f35 -> f34 : D'=1+D, E'=free_500, F'=free_498, G'=0, Q'=-1+Q, J'=free_499, M'=free_501, Q1'=free_497, M1'=C, N1'=free_502, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_500>=2 && free_503>=1 && 0>=1+free_502 && free_498>=1 && free_497>=1 ], cost: 1
     96: f35 -> f34 : D'=1+D, E'=free_507, F'=free_505, G'=0, Q'=-1+Q, J'=free_506, M'=free_508, Q1'=free_504, M1'=C, N1'=free_509, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_507>=2 && free_510>=1 && free_509>=1 && 0>=1+free_505 && 0>=1+free_504 ], cost: 1
     97: f35 -> f34 : D'=1+D, E'=free_514, F'=free_512, G'=0, Q'=-1+Q, J'=free_513, M'=free_515, Q1'=free_511, M1'=C, N1'=free_516, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_514>=2 && free_517>=1 && free_516>=1 && 0>=1+free_512 && free_511>=1 ], cost: 1
     98: f35 -> f34 : D'=1+D, E'=free_521, F'=free_519, G'=0, Q'=-1+Q, J'=free_520, M'=free_522, Q1'=free_518, M1'=C, N1'=free_523, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_521>=2 && free_524>=1 && free_523>=1 && free_519>=1 && 0>=1+free_518 ], cost: 1
     99: f35 -> f34 : D'=1+D, E'=free_528, F'=free_526, G'=0, Q'=-1+Q, J'=free_527, M'=free_529, Q1'=free_525, M1'=C, N1'=free_530, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_528>=2 && free_531>=1 && free_530>=1 && free_526>=1 && free_525>=1 ], cost: 1
     68: f35 -> f35 : B'=-1+B, E'=free_343, F'=free_341, G'=free_342, M'=free_344, Q1'=free_340, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_343>=2 && 0>=1+C && 0>=1+free_342 && 0>=1+free_340 && 0>=1+free_341 ], cost: 1
     69: f35 -> f35 : B'=-1+B, E'=free_348, F'=free_346, G'=free_347, M'=free_349, Q1'=free_345, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_348>=2 && 0>=1+C && 0>=1+free_347 && 0>=1+free_345 && free_346>=1 ], cost: 1
     70: f35 -> f35 : B'=-1+B, E'=free_353, F'=free_351, G'=free_352, M'=free_354, Q1'=free_350, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_353>=2 && 0>=1+C && 0>=1+free_352 && free_350>=1 && 0>=1+free_351 ], cost: 1
     71: f35 -> f35 : B'=-1+B, E'=free_358, F'=free_356, G'=free_357, M'=free_359, Q1'=free_355, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_358>=2 && 0>=1+C && 0>=1+free_357 && free_355>=1 && free_356>=1 ], cost: 1
     72: f35 -> f35 : B'=-1+B, E'=free_363, F'=free_361, G'=free_362, M'=free_364, Q1'=free_360, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_363>=2 && 0>=1+C && free_362>=1 && 0>=1+free_360 && 0>=1+free_361 ], cost: 1
     73: f35 -> f35 : B'=-1+B, E'=free_368, F'=free_366, G'=free_367, M'=free_369, Q1'=free_365, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_368>=2 && 0>=1+C && free_367>=1 && 0>=1+free_365 && free_366>=1 ], cost: 1
     74: f35 -> f35 : B'=-1+B, E'=free_373, F'=free_371, G'=free_372, M'=free_374, Q1'=free_370, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_373>=2 && 0>=1+C && free_372>=1 && free_370>=1 && 0>=1+free_371 ], cost: 1
     75: f35 -> f35 : B'=-1+B, E'=free_378, F'=free_376, G'=free_377, M'=free_379, Q1'=free_375, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_378>=2 && 0>=1+C && free_377>=1 && free_375>=1 && free_376>=1 ], cost: 1
     76: f35 -> f35 : B'=-1+B, E'=free_383, F'=free_381, G'=free_382, M'=free_384, Q1'=free_380, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_383>=2 && C>=1 && 0>=1+free_382 && 0>=1+free_380 && 0>=1+free_381 ], cost: 1
     77: f35 -> f35 : B'=-1+B, E'=free_388, F'=free_386, G'=free_387, M'=free_389, Q1'=free_385, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_388>=2 && C>=1 && 0>=1+free_387 && 0>=1+free_385 && free_386>=1 ], cost: 1
     78: f35 -> f35 : B'=-1+B, E'=free_393, F'=free_391, G'=free_392, M'=free_394, Q1'=free_390, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_393>=2 && C>=1 && 0>=1+free_392 && free_390>=1 && 0>=1+free_391 ], cost: 1
     79: f35 -> f35 : B'=-1+B, E'=free_398, F'=free_396, G'=free_397, M'=free_399, Q1'=free_395, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_398>=2 && C>=1 && 0>=1+free_397 && free_395>=1 && free_396>=1 ], cost: 1
     80: f35 -> f35 : B'=-1+B, E'=free_403, F'=free_401, G'=free_402, M'=free_404, Q1'=free_400, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_403>=2 && C>=1 && free_402>=1 && 0>=1+free_400 && 0>=1+free_401 ], cost: 1
     81: f35 -> f35 : B'=-1+B, E'=free_408, F'=free_406, G'=free_407, M'=free_409, Q1'=free_405, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_408>=2 && C>=1 && free_407>=1 && 0>=1+free_405 && free_406>=1 ], cost: 1
     82: f35 -> f35 : B'=-1+B, E'=free_413, F'=free_411, G'=free_412, M'=free_414, Q1'=free_410, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_413>=2 && C>=1 && free_412>=1 && free_410>=1 && 0>=1+free_411 ], cost: 1
     83: f35 -> f35 : B'=-1+B, E'=free_418, F'=free_416, G'=free_417, M'=free_419, Q1'=free_415, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_418>=2 && C>=1 && free_417>=1 && free_415>=1 && free_416>=1 ], cost: 1
     40: f31 -> f34 : E'=free_211, F'=free_209, G'=0, M'=free_210, Y'=free_212, Z'=free_208, [ B>=1 && H>=0 && free_211>=2 && 0>=1+C && 0>=1+free_209 && 0>=1+free_208 ], cost: 1
     41: f31 -> f34 : E'=free_216, F'=free_214, G'=0, M'=free_215, Y'=free_217, Z'=free_213, [ B>=1 && H>=0 && free_216>=2 && 0>=1+C && 0>=1+free_214 && free_213>=1 ], cost: 1
     42: f31 -> f34 : E'=free_221, F'=free_219, G'=0, M'=free_220, Y'=free_222, Z'=free_218, [ B>=1 && H>=0 && free_221>=2 && 0>=1+C && free_219>=1 && 0>=1+free_218 ], cost: 1
     43: f31 -> f34 : E'=free_226, F'=free_224, G'=0, M'=free_225, Y'=free_227, Z'=free_223, [ B>=1 && H>=0 && free_226>=2 && 0>=1+C && free_224>=1 && free_223>=1 ], cost: 1
     44: f31 -> f34 : E'=free_231, F'=free_229, G'=0, M'=free_230, Y'=free_232, Z'=free_228, [ B>=1 && H>=0 && free_231>=2 && C>=1 && 0>=1+free_229 && 0>=1+free_228 ], cost: 1
     45: f31 -> f34 : E'=free_236, F'=free_234, G'=0, M'=free_235, Y'=free_237, Z'=free_233, [ B>=1 && H>=0 && free_236>=2 && C>=1 && 0>=1+free_234 && free_233>=1 ], cost: 1
     46: f31 -> f34 : E'=free_241, F'=free_239, G'=0, M'=free_240, Y'=free_242, Z'=free_238, [ B>=1 && H>=0 && free_241>=2 && C>=1 && free_239>=1 && 0>=1+free_238 ], cost: 1
     47: f31 -> f34 : E'=free_246, F'=free_244, G'=0, M'=free_245, Y'=free_247, Z'=free_243, [ B>=1 && H>=0 && free_246>=2 && C>=1 && free_244>=1 && free_243>=1 ], cost: 1
     24: f31 -> f35 : B'=-1+B, D'=1, E'=free_131, F'=free_129, G'=free_130, Q'=H, M'=free_132, U'=free_128, V'=B, W'=J, X'=H, [ B>=1 && H>=0 && free_131>=2 && 0>=1+C && 0>=1+free_130 && 0>=1+free_128 && 0>=1+free_129 && Q==H && D==1 ], cost: 1
     25: f31 -> f35 : B'=-1+B, D'=1, E'=free_136, F'=free_134, G'=free_135, Q'=H, M'=free_137, U'=free_133, V'=B, W'=J, X'=H, [ B>=1 && H>=0 && free_136>=2 && 0>=1+C && 0>=1+free_135 && 0>=1+free_133 && free_134>=1 && Q==H && D==1 ], cost: 1
     26: f31 -> f35 : B'=-1+B, D'=1, E'=free_141, F'=free_139, G'=free_140, Q'=H, M'=free_142, U'=free_138, V'=B, W'=J, X'=H, [ B>=1 && H>=0 && free_141>=2 && 0>=1+C && 0>=1+free_140 && free_138>=1 && 0>=1+free_139 && Q==H && D==1 ], cost: 1
     27: f31 -> f35 : B'=-1+B, D'=1, E'=free_146, F'=free_144, G'=free_145, Q'=H, M'=free_147, U'=free_143, V'=B, W'=J, X'=H, [ B>=1 && H>=0 && free_146>=2 && 0>=1+C && 0>=1+free_145 && free_143>=1 && free_144>=1 && Q==H && D==1 ], cost: 1
     28: f31 -> f35 : B'=-1+B, D'=1, E'=free_151, F'=free_149, G'=free_150, Q'=H, M'=free_152, U'=free_148, V'=B, W'=J, X'=H, [ B>=1 && H>=0 && free_151>=2 && 0>=1+C && free_150>=1 && 0>=1+free_148 && 0>=1+free_149 && Q==H && D==1 ], cost: 1
     29: f31 -> f35 : B'=-1+B, D'=1, E'=free_156, F'=free_154, G'=free_155, Q'=H, M'=free_157, U'=free_153, V'=B, W'=J, X'=H, [ B>=1 && H>=0 && free_156>=2 && 0>=1+C && free_155>=1 && 0>=1+free_153 && free_154>=1 && Q==H && D==1 ], cost: 1
     30: f31 -> f35 : B'=-1+B, D'=1, E'=free_161, F'=free_159, G'=free_160, Q'=H, M'=free_162, U'=free_158, V'=B, W'=J, X'=H, [ B>=1 && H>=0 && free_161>=2 && 0>=1+C && free_160>=1 && free_158>=1 && 0>=1+free_159 && Q==H && D==1 ], cost: 1
     31: f31 -> f35 : B'=-1+B, D'=1, E'=free_166, F'=free_164, G'=free_165, Q'=H, M'=free_167, U'=free_163, V'=B, W'=J, X'=H, [ B>=1 && H>=0 && free_166>=2 && 0>=1+C && free_165>=1 && free_163>=1 && free_164>=1 && Q==H && D==1 ], cost: 1
     32: f31 -> f35 : B'=-1+B, D'=1, E'=free_171, F'=free_169, G'=free_170, Q'=H, M'=free_172, U'=free_168, V'=B, W'=J, X'=H, [ B>=1 && H>=0 && free_171>=2 && C>=1 && 0>=1+free_170 && 0>=1+free_168 && 0>=1+free_169 && Q==H && D==1 ], cost: 1
     33: f31 -> f35 : B'=-1+B, D'=1, E'=free_176, F'=free_174, G'=free_175, Q'=H, M'=free_177, U'=free_173, V'=B, W'=J, X'=H, [ B>=1 && H>=0 && free_176>=2 && C>=1 && 0>=1+free_175 && 0>=1+free_173 && free_174>=1 && Q==H && D==1 ], cost: 1
     34: f31 -> f35 : B'=-1+B, D'=1, E'=free_181, F'=free_179, G'=free_180, Q'=H, M'=free_182, U'=free_178, V'=B, W'=J, X'=H, [ B>=1 && H>=0 && free_181>=2 && C>=1 && 0>=1+free_180 && free_178>=1 && 0>=1+free_179 && Q==H && D==1 ], cost: 1
     35: f31 -> f35 : B'=-1+B, D'=1, E'=free_186, F'=free_184, G'=free_185, Q'=H, M'=free_187, U'=free_183, V'=B, W'=J, X'=H, [ B>=1 && H>=0 && free_186>=2 && C>=1 && 0>=1+free_185 && free_183>=1 && free_184>=1 && Q==H && D==1 ], cost: 1
     36: f31 -> f35 : B'=-1+B, D'=1, E'=free_191, F'=free_189, G'=free_190, Q'=H, M'=free_192, U'=free_188, V'=B, W'=J, X'=H, [ B>=1 && H>=0 && free_191>=2 && C>=1 && free_190>=1 && 0>=1+free_188 && 0>=1+free_189 && Q==H && D==1 ], cost: 1
     37: f31 -> f35 : B'=-1+B, D'=1, E'=free_196, F'=free_194, G'=free_195, Q'=H, M'=free_197, U'=free_193, V'=B, W'=J, X'=H, [ B>=1 && H>=0 && free_196>=2 && C>=1 && free_195>=1 && 0>=1+free_193 && free_194>=1 && Q==H && D==1 ], cost: 1
     38: f31 -> f35 : B'=-1+B, D'=1, E'=free_201, F'=free_199, G'=free_200, Q'=H, M'=free_202, U'=free_198, V'=B, W'=J, X'=H, [ B>=1 && H>=0 && free_201>=2 && C>=1 && free_200>=1 && free_198>=1 && 0>=1+free_199 && Q==H && D==1 ], cost: 1
     39: f31 -> f35 : B'=-1+B, D'=1, E'=free_206, F'=free_204, G'=free_205, Q'=H, M'=free_207, U'=free_203, V'=B, W'=J, X'=H, [ B>=1 && H>=0 && free_206>=2 && C>=1 && free_205>=1 && free_203>=1 && free_204>=1 && Q==H && D==1 ], cost: 1
     48: f32 -> f32 : B'=-1+B, E'=1, F'=C, G'=free_249, M'=free_248, A1'=B, B1'=C1, [ B>=1 && 0>=1+free_250 && 0>=1+free_249 ], cost: 1
     49: f32 -> f32 : B'=-1+B, E'=1, F'=C, G'=free_252, M'=free_251, A1'=B, B1'=C1, [ B>=1 && 0>=1+free_253 && free_252>=1 ], cost: 1
     50: f32 -> f32 : B'=-1+B, E'=1, F'=C, G'=free_255, M'=free_254, A1'=B, B1'=C1, [ B>=1 && free_256>=1 && 0>=1+free_255 ], cost: 1
     51: f32 -> f32 : B'=-1+B, E'=1, F'=C, G'=free_258, M'=free_257, A1'=B, B1'=C1, [ B>=1 && free_259>=1 && free_258>=1 ], cost: 1
    101: f1 -> f29 : A'=free_535, C'=R1, E'=free_538, F'=R1, Q1_1'=free_537, R1'=free_540, S1'=free_536, T1'=free_541, W1'=free_534, X1'=free_539, Y1'=free_542, [ A>=Q1_1 && A>=0 && free_535>=free_538 && free_538>=2 ], cost: 1
    100: f1 -> f1 : A'=1+A, R1'=S1, S1'=free_533, T1'=S1, U1'=free_532, V1'=A, [ Q1_1>=1+A && A>=0 ], cost: 1
    102: f11 -> f27 : B'=free_550, C'=free_544, E'=free_548, F'=free_544, G'=free_553, Y1'=free_545, Z1'=free_552, A2'=free_546, B2'=free_547, C2'=free_551, D2'=free_543, E2'=free_549, [ 0>=free_550 && free_548>=2 && 0>=1+free_544 && 0>=1+free_553 && Z1==A2 ], cost: 1
    103: f11 -> f27 : B'=free_561, C'=free_555, E'=free_559, F'=free_555, G'=free_564, Y1'=free_556, Z1'=free_563, A2'=free_557, B2'=free_558, C2'=free_562, D2'=free_554, E2'=free_560, [ 0>=free_561 && free_559>=2 && 0>=1+free_555 && free_564>=1 && Z1==A2 ], cost: 1
    104: f11 -> f27 : B'=free_572, C'=free_566, E'=free_570, F'=free_566, G'=free_575, Y1'=free_567, Z1'=free_574, A2'=free_568, B2'=free_569, C2'=free_573, D2'=free_565, E2'=free_571, [ 0>=free_572 && free_570>=2 && free_566>=1 && 0>=1+free_575 && Z1==A2 ], cost: 1
    105: f11 -> f27 : B'=free_583, C'=free_577, E'=free_581, F'=free_577, G'=free_586, Y1'=free_578, Z1'=free_585, A2'=free_579, B2'=free_580, C2'=free_584, D2'=free_576, E2'=free_582, [ 0>=free_583 && free_581>=2 && free_577>=1 && free_586>=1 && Z1==A2 ], cost: 1
    106: f12 -> f27 : B'=free_598, C'=free_588, E'=free_592, F'=free_594, G'=free_589, Y1'=free_593, Z1'=free_596, A2'=free_590, B2'=free_591, C2'=free_595, D2'=free_587, E2'=free_597, [ 0>=free_598 && free_592>=2 && 0>=1+free_589 && 0>=1+free_594 && 0>=1+free_597 && free_599>=1 && 0>=1+free_588 && Z1==A2 ], cost: 1
    107: f12 -> f27 : B'=free_611, C'=free_601, E'=free_605, F'=free_607, G'=free_602, Y1'=free_606, Z1'=free_609, A2'=free_603, B2'=free_604, C2'=free_608, D2'=free_600, E2'=free_610, [ 0>=free_611 && free_605>=2 && 0>=1+free_602 && 0>=1+free_607 && 0>=1+free_610 && free_612>=1 && free_601>=1 && Z1==A2 ], cost: 1
    108: f12 -> f27 : B'=free_624, C'=free_614, E'=free_618, F'=free_620, G'=free_615, Y1'=free_619, Z1'=free_622, A2'=free_616, B2'=free_617, C2'=free_621, D2'=free_613, E2'=free_623, [ 0>=free_624 && free_618>=2 && 0>=1+free_615 && 0>=1+free_620 && 0>=1+free_623 && 0>=1+free_625 && 0>=1+free_614 && Z1==A2 ], cost: 1
    109: f12 -> f27 : B'=free_637, C'=free_627, E'=free_631, F'=free_633, G'=free_628, Y1'=free_632, Z1'=free_635, A2'=free_629, B2'=free_630, C2'=free_634, D2'=free_626, E2'=free_636, [ 0>=free_637 && free_631>=2 && 0>=1+free_628 && 0>=1+free_633 && 0>=1+free_636 && 0>=1+free_638 && free_627>=1 && Z1==A2 ], cost: 1
    110: f12 -> f27 : B'=free_650, C'=free_640, E'=free_644, F'=free_646, G'=free_641, Y1'=free_645, Z1'=free_648, A2'=free_642, B2'=free_643, C2'=free_647, D2'=free_639, E2'=free_649, [ 0>=free_650 && free_644>=2 && 0>=1+free_641 && 0>=1+free_646 && free_649>=1 && free_651>=1 && 0>=1+free_640 && Z1==A2 ], cost: 1
    111: f12 -> f27 : B'=free_663, C'=free_653, E'=free_657, F'=free_659, G'=free_654, Y1'=free_658, Z1'=free_661, A2'=free_655, B2'=free_656, C2'=free_660, D2'=free_652, E2'=free_662, [ 0>=free_663 && free_657>=2 && 0>=1+free_654 && 0>=1+free_659 && free_662>=1 && free_664>=1 && free_653>=1 && Z1==A2 ], cost: 1
    112: f12 -> f27 : B'=free_676, C'=free_666, E'=free_670, F'=free_672, G'=free_667, Y1'=free_671, Z1'=free_674, A2'=free_668, B2'=free_669, C2'=free_673, D2'=free_665, E2'=free_675, [ 0>=free_676 && free_670>=2 && 0>=1+free_667 && 0>=1+free_672 && free_675>=1 && 0>=1+free_677 && 0>=1+free_666 && Z1==A2 ], cost: 1
    113: f12 -> f27 : B'=free_689, C'=free_679, E'=free_683, F'=free_685, G'=free_680, Y1'=free_684, Z1'=free_687, A2'=free_681, B2'=free_682, C2'=free_686, D2'=free_678, E2'=free_688, [ 0>=free_689 && free_683>=2 && 0>=1+free_680 && 0>=1+free_685 && free_688>=1 && 0>=1+free_690 && free_679>=1 && Z1==A2 ], cost: 1
    114: f12 -> f27 : B'=free_702, C'=free_692, E'=free_696, F'=free_698, G'=free_693, Y1'=free_697, Z1'=free_700, A2'=free_694, B2'=free_695, C2'=free_699, D2'=free_691, E2'=free_701, [ 0>=free_702 && free_696>=2 && 0>=1+free_693 && free_698>=1 && 0>=1+free_701 && free_703>=1 && 0>=1+free_692 && Z1==A2 ], cost: 1
    115: f12 -> f27 : B'=free_715, C'=free_705, E'=free_709, F'=free_711, G'=free_706, Y1'=free_710, Z1'=free_713, A2'=free_707, B2'=free_708, C2'=free_712, D2'=free_704, E2'=free_714, [ 0>=free_715 && free_709>=2 && 0>=1+free_706 && free_711>=1 && 0>=1+free_714 && free_716>=1 && free_705>=1 && Z1==A2 ], cost: 1
    116: f12 -> f27 : B'=free_728, C'=free_718, E'=free_722, F'=free_724, G'=free_719, Y1'=free_723, Z1'=free_726, A2'=free_720, B2'=free_721, C2'=free_725, D2'=free_717, E2'=free_727, [ 0>=free_728 && free_722>=2 && 0>=1+free_719 && free_724>=1 && 0>=1+free_727 && 0>=1+free_729 && 0>=1+free_718 && Z1==A2 ], cost: 1
    117: f12 -> f27 : B'=free_741, C'=free_731, E'=free_735, F'=free_737, G'=free_732, Y1'=free_736, Z1'=free_739, A2'=free_733, B2'=free_734, C2'=free_738, D2'=free_730, E2'=free_740, [ 0>=free_741 && free_735>=2 && 0>=1+free_732 && free_737>=1 && 0>=1+free_740 && 0>=1+free_742 && free_731>=1 && Z1==A2 ], cost: 1
    118: f12 -> f27 : B'=free_754, C'=free_744, E'=free_748, F'=free_750, G'=free_745, Y1'=free_749, Z1'=free_752, A2'=free_746, B2'=free_747, C2'=free_751, D2'=free_743, E2'=free_753, [ 0>=free_754 && free_748>=2 && 0>=1+free_745 && free_750>=1 && free_753>=1 && free_755>=1 && 0>=1+free_744 && Z1==A2 ], cost: 1
    119: f12 -> f27 : B'=free_767, C'=free_757, E'=free_761, F'=free_763, G'=free_758, Y1'=free_762, Z1'=free_765, A2'=free_759, B2'=free_760, C2'=free_764, D2'=free_756, E2'=free_766, [ 0>=free_767 && free_761>=2 && 0>=1+free_758 && free_763>=1 && free_766>=1 && free_768>=1 && free_757>=1 && Z1==A2 ], cost: 1
    120: f12 -> f27 : B'=free_780, C'=free_770, E'=free_774, F'=free_776, G'=free_771, Y1'=free_775, Z1'=free_778, A2'=free_772, B2'=free_773, C2'=free_777, D2'=free_769, E2'=free_779, [ 0>=free_780 && free_774>=2 && 0>=1+free_771 && free_776>=1 && free_779>=1 && 0>=1+free_781 && 0>=1+free_770 && Z1==A2 ], cost: 1
    121: f12 -> f27 : B'=free_793, C'=free_783, E'=free_787, F'=free_789, G'=free_784, Y1'=free_788, Z1'=free_791, A2'=free_785, B2'=free_786, C2'=free_790, D2'=free_782, E2'=free_792, [ 0>=free_793 && free_787>=2 && 0>=1+free_784 && free_789>=1 && free_792>=1 && 0>=1+free_794 && free_783>=1 && Z1==A2 ], cost: 1
    122: f12 -> f27 : B'=free_806, C'=free_796, E'=free_800, F'=free_802, G'=free_797, Y1'=free_801, Z1'=free_804, A2'=free_798, B2'=free_799, C2'=free_803, D2'=free_795, E2'=free_805, [ 0>=free_806 && free_800>=2 && free_797>=1 && 0>=1+free_802 && 0>=1+free_805 && free_807>=1 && 0>=1+free_796 && Z1==A2 ], cost: 1
    123: f12 -> f27 : B'=free_819, C'=free_809, E'=free_813, F'=free_815, G'=free_810, Y1'=free_814, Z1'=free_817, A2'=free_811, B2'=free_812, C2'=free_816, D2'=free_808, E2'=free_818, [ 0>=free_819 && free_813>=2 && free_810>=1 && 0>=1+free_815 && 0>=1+free_818 && free_820>=1 && free_809>=1 && Z1==A2 ], cost: 1
    124: f12 -> f27 : B'=free_832, C'=free_822, E'=free_826, F'=free_828, G'=free_823, Y1'=free_827, Z1'=free_830, A2'=free_824, B2'=free_825, C2'=free_829, D2'=free_821, E2'=free_831, [ 0>=free_832 && free_826>=2 && free_823>=1 && 0>=1+free_828 && 0>=1+free_831 && 0>=1+free_833 && 0>=1+free_822 && Z1==A2 ], cost: 1
    125: f12 -> f27 : B'=free_845, C'=free_835, E'=free_839, F'=free_841, G'=free_836, Y1'=free_840, Z1'=free_843, A2'=free_837, B2'=free_838, C2'=free_842, D2'=free_834, E2'=free_844, [ 0>=free_845 && free_839>=2 && free_836>=1 && 0>=1+free_841 && 0>=1+free_844 && 0>=1+free_846 && free_835>=1 && Z1==A2 ], cost: 1
    126: f12 -> f27 : B'=free_858, C'=free_848, E'=free_852, F'=free_854, G'=free_849, Y1'=free_853, Z1'=free_856, A2'=free_850, B2'=free_851, C2'=free_855, D2'=free_847, E2'=free_857, [ 0>=free_858 && free_852>=2 && free_849>=1 && 0>=1+free_854 && free_857>=1 && free_859>=1 && 0>=1+free_848 && Z1==A2 ], cost: 1
    127: f12 -> f27 : B'=free_871, C'=free_861, E'=free_865, F'=free_867, G'=free_862, Y1'=free_866, Z1'=free_869, A2'=free_863, B2'=free_864, C2'=free_868, D2'=free_860, E2'=free_870, [ 0>=free_871 && free_865>=2 && free_862>=1 && 0>=1+free_867 && free_870>=1 && free_872>=1 && free_861>=1 && Z1==A2 ], cost: 1
    128: f12 -> f27 : B'=free_884, C'=free_874, E'=free_878, F'=free_880, G'=free_875, Y1'=free_879, Z1'=free_882, A2'=free_876, B2'=free_877, C2'=free_881, D2'=free_873, E2'=free_883, [ 0>=free_884 && free_878>=2 && free_875>=1 && 0>=1+free_880 && free_883>=1 && 0>=1+free_885 && 0>=1+free_874 && Z1==A2 ], cost: 1
    129: f12 -> f27 : B'=free_897, C'=free_887, E'=free_891, F'=free_893, G'=free_888, Y1'=free_892, Z1'=free_895, A2'=free_889, B2'=free_890, C2'=free_894, D2'=free_886, E2'=free_896, [ 0>=free_897 && free_891>=2 && free_888>=1 && 0>=1+free_893 && free_896>=1 && 0>=1+free_898 && free_887>=1 && Z1==A2 ], cost: 1
    130: f12 -> f27 : B'=free_910, C'=free_900, E'=free_904, F'=free_906, G'=free_901, Y1'=free_905, Z1'=free_908, A2'=free_902, B2'=free_903, C2'=free_907, D2'=free_899, E2'=free_909, [ 0>=free_910 && free_904>=2 && free_901>=1 && free_906>=1 && 0>=1+free_909 && free_911>=1 && 0>=1+free_900 && Z1==A2 ], cost: 1
    131: f12 -> f27 : B'=free_923, C'=free_913, E'=free_917, F'=free_919, G'=free_914, Y1'=free_918, Z1'=free_921, A2'=free_915, B2'=free_916, C2'=free_920, D2'=free_912, E2'=free_922, [ 0>=free_923 && free_917>=2 && free_914>=1 && free_919>=1 && 0>=1+free_922 && free_924>=1 && free_913>=1 && Z1==A2 ], cost: 1
    132: f12 -> f27 : B'=free_936, C'=free_926, E'=free_930, F'=free_932, G'=free_927, Y1'=free_931, Z1'=free_934, A2'=free_928, B2'=free_929, C2'=free_933, D2'=free_925, E2'=free_935, [ 0>=free_936 && free_930>=2 && free_927>=1 && free_932>=1 && 0>=1+free_935 && 0>=1+free_937 && 0>=1+free_926 && Z1==A2 ], cost: 1
    133: f12 -> f27 : B'=free_949, C'=free_939, E'=free_943, F'=free_945, G'=free_940, Y1'=free_944, Z1'=free_947, A2'=free_941, B2'=free_942, C2'=free_946, D2'=free_938, E2'=free_948, [ 0>=free_949 && free_943>=2 && free_940>=1 && free_945>=1 && 0>=1+free_948 && 0>=1+free_950 && free_939>=1 && Z1==A2 ], cost: 1
    134: f12 -> f27 : B'=free_962, C'=free_952, E'=free_956, F'=free_958, G'=free_953, Y1'=free_957, Z1'=free_960, A2'=free_954, B2'=free_955, C2'=free_959, D2'=free_951, E2'=free_961, [ 0>=free_962 && free_956>=2 && free_953>=1 && free_958>=1 && free_961>=1 && free_963>=1 && 0>=1+free_952 && Z1==A2 ], cost: 1
    135: f12 -> f27 : B'=free_975, C'=free_965, E'=free_969, F'=free_971, G'=free_966, Y1'=free_970, Z1'=free_973, A2'=free_967, B2'=free_968, C2'=free_972, D2'=free_964, E2'=free_974, [ 0>=free_975 && free_969>=2 && free_966>=1 && free_971>=1 && free_974>=1 && free_976>=1 && free_965>=1 && Z1==A2 ], cost: 1
    136: f12 -> f27 : B'=free_988, C'=free_978, E'=free_982, F'=free_984, G'=free_979, Y1'=free_983, Z1'=free_986, A2'=free_980, B2'=free_981, C2'=free_985, D2'=free_977, E2'=free_987, [ 0>=free_988 && free_982>=2 && free_979>=1 && free_984>=1 && free_987>=1 && 0>=1+free_989 && 0>=1+free_978 && Z1==A2 ], cost: 1
    137: f12 -> f27 : B'=free_1001, C'=free_991, E'=free_995, F'=free_997, G'=free_992, Y1'=free_996, Z1'=free_999, A2'=free_993, B2'=free_994, C2'=free_998, D2'=free_990, E2'=free_1000, [ 0>=free_1001 && free_995>=2 && free_992>=1 && free_997>=1 && free_1000>=1 && 0>=1+free_1002 && free_991>=1 && Z1==A2 ], cost: 1
    146: f14 -> f27 : B'=free_1041, E'=free_1040, F'=free_1038, Y1'=free_1044, Z1'=free_1035, A2'=free_1043, B2'=free_1036, C2'=free_1039, D2'=free_1042, E2'=free_1037, [ F2>=0 && free_1040>=2 && 0>=1+free_1038 && free_1041>=1 && Z1==A2 ], cost: 1
    147: f14 -> f27 : B'=free_1051, E'=free_1050, F'=free_1048, Y1'=free_1054, Z1'=free_1045, A2'=free_1053, B2'=free_1046, C2'=free_1049, D2'=free_1052, E2'=free_1047, [ F2>=0 && free_1050>=2 && free_1048>=1 && free_1051>=1 && Z1==A2 ], cost: 1
    138: f14 -> f15 : B'=free_1004, C'=0, E'=free_1005, F'=free_1003, G'=0, Z1'=0, B2'=free_1003, C2'=0, D2'=free_1003, E2'=A2, [ free_1006>=1+A2 && F2>=0 && free_1005>=2 && free_1004>=1 && free_1003>=1+free_1006 && 0>=1+free_1003 && Z1==0 ], cost: 1
    139: f14 -> f15 : B'=free_1008, C'=0, E'=free_1009, F'=free_1007, G'=0, Z1'=0, B2'=free_1007, C2'=0, D2'=free_1007, E2'=A2, [ free_1010>=1+A2 && F2>=0 && free_1009>=2 && free_1008>=1 && free_1007>=1+free_1010 && free_1007>=1 && Z1==0 ], cost: 1
    140: f14 -> f15 : B'=free_1012, C'=0, E'=free_1013, F'=free_1011, G'=0, Z1'=0, B2'=free_1011, C2'=0, D2'=free_1011, E2'=A2, [ free_1014>=1+A2 && F2>=0 && free_1013>=2 && free_1012>=1 && free_1014>=1+free_1011 && 0>=1+free_1011 && Z1==0 ], cost: 1
    141: f14 -> f15 : B'=free_1016, C'=0, E'=free_1017, F'=free_1015, G'=0, Z1'=0, B2'=free_1015, C2'=0, D2'=free_1015, E2'=A2, [ free_1018>=1+A2 && F2>=0 && free_1017>=2 && free_1016>=1 && free_1018>=1+free_1015 && free_1015>=1 && Z1==0 ], cost: 1
    142: f14 -> f15 : B'=free_1020, C'=0, E'=free_1021, F'=free_1019, G'=0, Z1'=0, B2'=free_1019, C2'=0, D2'=free_1019, E2'=A2, [ A2>=1+free_1022 && F2>=0 && free_1021>=2 && free_1020>=1 && free_1019>=1+free_1022 && 0>=1+free_1019 && Z1==0 ], cost: 1
    143: f14 -> f15 : B'=free_1024, C'=0, E'=free_1025, F'=free_1023, G'=0, Z1'=0, B2'=free_1023, C2'=0, D2'=free_1023, E2'=A2, [ A2>=1+free_1026 && F2>=0 && free_1025>=2 && free_1024>=1 && free_1023>=1+free_1026 && free_1023>=1 && Z1==0 ], cost: 1
    144: f14 -> f15 : B'=free_1028, C'=0, E'=free_1029, F'=free_1027, G'=0, Z1'=0, B2'=free_1027, C2'=0, D2'=free_1027, E2'=A2, [ A2>=1+free_1030 && F2>=0 && free_1029>=2 && free_1028>=1 && free_1030>=1+free_1027 && 0>=1+free_1027 && Z1==0 ], cost: 1
    145: f14 -> f15 : B'=free_1032, C'=0, E'=free_1033, F'=free_1031, G'=0, Z1'=0, B2'=free_1031, C2'=0, D2'=free_1031, E2'=A2, [ A2>=1+free_1034 && F2>=0 && free_1033>=2 && free_1032>=1 && free_1034>=1+free_1031 && free_1031>=1 && Z1==0 ], cost: 1
    156: f15 -> f27 : B'=free_1101, E'=free_1100, F'=free_1098, Y1'=free_1104, Z1'=free_1095, A2'=free_1103, B2'=free_1096, C2'=free_1099, D2'=free_1102, E2'=free_1097, [ G2>=0 && free_1100>=2 && free_1101>=1 && 0>=1+free_1098 && 0>=1+free_1097 && Z1==A2 ], cost: 1
    157: f15 -> f27 : B'=free_1111, E'=free_1110, F'=free_1108, Y1'=free_1114, Z1'=free_1105, A2'=free_1113, B2'=free_1106, C2'=free_1109, D2'=free_1112, E2'=free_1107, [ G2>=0 && free_1110>=2 && free_1111>=1 && 0>=1+free_1108 && free_1107>=1 && Z1==A2 ], cost: 1
    158: f15 -> f27 : B'=free_1121, E'=free_1120, F'=free_1118, Y1'=free_1124, Z1'=free_1115, A2'=free_1123, B2'=free_1116, C2'=free_1119, D2'=free_1122, E2'=free_1117, [ G2>=0 && free_1120>=2 && free_1121>=1 && free_1118>=1 && 0>=1+free_1117 && Z1==A2 ], cost: 1
    159: f15 -> f27 : B'=free_1131, E'=free_1130, F'=free_1128, Y1'=free_1134, Z1'=free_1125, A2'=free_1133, B2'=free_1126, C2'=free_1129, D2'=free_1132, E2'=free_1127, [ G2>=0 && free_1130>=2 && free_1131>=1 && free_1128>=1 && free_1127>=1 && Z1==A2 ], cost: 1
    148: f15 -> f15 : B'=free_1056, C'=0, E'=free_1057, F'=free_1055, G'=0, J'=free_1058, Z1'=0, B2'=free_1055, C2'=0, D2'=free_1055, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ free_1059>=1+A2 && G2>=0 && free_1057>=2 && free_1056>=1 && free_1055>=1+free_1059 && 0>=1+free_1055 && Z1==0 ], cost: 1
    149: f15 -> f15 : B'=free_1061, C'=0, E'=free_1062, F'=free_1060, G'=0, J'=free_1063, Z1'=0, B2'=free_1060, C2'=0, D2'=free_1060, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ free_1064>=1+A2 && G2>=0 && free_1062>=2 && free_1061>=1 && free_1060>=1+free_1064 && free_1060>=1 && Z1==0 ], cost: 1
    150: f15 -> f15 : B'=free_1066, C'=0, E'=free_1067, F'=free_1065, G'=0, J'=free_1068, Z1'=0, B2'=free_1065, C2'=0, D2'=free_1065, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ free_1069>=1+A2 && G2>=0 && free_1067>=2 && free_1066>=1 && free_1069>=1+free_1065 && 0>=1+free_1065 && Z1==0 ], cost: 1
    151: f15 -> f15 : B'=free_1071, C'=0, E'=free_1072, F'=free_1070, G'=0, J'=free_1073, Z1'=0, B2'=free_1070, C2'=0, D2'=free_1070, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ free_1074>=1+A2 && G2>=0 && free_1072>=2 && free_1071>=1 && free_1074>=1+free_1070 && free_1070>=1 && Z1==0 ], cost: 1
    152: f15 -> f15 : B'=free_1076, C'=0, E'=free_1077, F'=free_1075, G'=0, J'=free_1078, Z1'=0, B2'=free_1075, C2'=0, D2'=free_1075, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ A2>=1+free_1079 && G2>=0 && free_1077>=2 && free_1076>=1 && free_1075>=1+free_1079 && 0>=1+free_1075 && Z1==0 ], cost: 1
    153: f15 -> f15 : B'=free_1081, C'=0, E'=free_1082, F'=free_1080, G'=0, J'=free_1083, Z1'=0, B2'=free_1080, C2'=0, D2'=free_1080, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ A2>=1+free_1084 && G2>=0 && free_1082>=2 && free_1081>=1 && free_1080>=1+free_1084 && free_1080>=1 && Z1==0 ], cost: 1
    154: f15 -> f15 : B'=free_1086, C'=0, E'=free_1087, F'=free_1085, G'=0, J'=free_1088, Z1'=0, B2'=free_1085, C2'=0, D2'=free_1085, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ A2>=1+free_1089 && G2>=0 && free_1087>=2 && free_1086>=1 && free_1089>=1+free_1085 && 0>=1+free_1085 && Z1==0 ], cost: 1
    155: f15 -> f15 : B'=free_1091, C'=0, E'=free_1092, F'=free_1090, G'=0, J'=free_1093, Z1'=0, B2'=free_1090, C2'=0, D2'=free_1090, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ A2>=1+free_1094 && G2>=0 && free_1092>=2 && free_1091>=1 && free_1094>=1+free_1090 && free_1090>=1 && Z1==0 ], cost: 1
    168: f16 -> f27 : B'=free_1173, C'=free_1168, E'=free_1172, Y1'=free_1176, Z1'=free_1175, A2'=free_1170, B2'=free_1171, C2'=free_1174, D2'=free_1167, E2'=free_1169, [ Q2>=0 && 0>=free_1173 && 0>=1+free_1168 && free_1172>=2 && Z1==A2 ], cost: 1
    169: f16 -> f27 : B'=free_1183, C'=free_1178, E'=free_1182, Y1'=free_1186, Z1'=free_1185, A2'=free_1180, B2'=free_1181, C2'=free_1184, D2'=free_1177, E2'=free_1179, [ Q2>=0 && 0>=free_1183 && free_1178>=1 && free_1182>=2 && Z1==A2 ], cost: 1
    160: f16 -> f17 : B'=free_1136, C'=free_1135, E'=free_1137, F'=free_1135, Z1'=0, B2'=free_1135, C2'=0, D2'=free_1135, E2'=A2, [ free_1138>=1+A2 && Q2>=0 && 0>=free_1136 && free_1137>=2 && free_1135>=1+free_1138 && 0>=1+free_1135 && Z1==0 ], cost: 1
    161: f16 -> f17 : B'=free_1140, C'=free_1139, E'=free_1141, F'=free_1139, Z1'=0, B2'=free_1139, C2'=0, D2'=free_1139, E2'=A2, [ free_1142>=1+A2 && Q2>=0 && 0>=free_1140 && free_1141>=2 && free_1139>=1+free_1142 && free_1139>=1 && Z1==0 ], cost: 1
    162: f16 -> f17 : B'=free_1144, C'=free_1143, E'=free_1145, F'=free_1143, Z1'=0, B2'=free_1143, C2'=0, D2'=free_1143, E2'=A2, [ free_1146>=1+A2 && Q2>=0 && 0>=free_1144 && free_1145>=2 && free_1146>=1+free_1143 && 0>=1+free_1143 && Z1==0 ], cost: 1
    163: f16 -> f17 : B'=free_1148, C'=free_1147, E'=free_1149, F'=free_1147, Z1'=0, B2'=free_1147, C2'=0, D2'=free_1147, E2'=A2, [ free_1150>=1+A2 && Q2>=0 && 0>=free_1148 && free_1149>=2 && free_1150>=1+free_1147 && free_1147>=1 && Z1==0 ], cost: 1
    164: f16 -> f17 : B'=free_1152, C'=free_1151, E'=free_1153, F'=free_1151, Z1'=0, B2'=free_1151, C2'=0, D2'=free_1151, E2'=A2, [ A2>=1+free_1154 && Q2>=0 && 0>=free_1152 && free_1153>=2 && free_1151>=1+free_1154 && 0>=1+free_1151 && Z1==0 ], cost: 1
    165: f16 -> f17 : B'=free_1156, C'=free_1155, E'=free_1157, F'=free_1155, Z1'=0, B2'=free_1155, C2'=0, D2'=free_1155, E2'=A2, [ A2>=1+free_1158 && Q2>=0 && 0>=free_1156 && free_1157>=2 && free_1155>=1+free_1158 && free_1155>=1 && Z1==0 ], cost: 1
    166: f16 -> f17 : B'=free_1160, C'=free_1159, E'=free_1161, F'=free_1159, Z1'=0, B2'=free_1159, C2'=0, D2'=free_1159, E2'=A2, [ A2>=1+free_1162 && Q2>=0 && 0>=free_1160 && free_1161>=2 && free_1162>=1+free_1159 && 0>=1+free_1159 && Z1==0 ], cost: 1
    167: f16 -> f17 : B'=free_1164, C'=free_1163, E'=free_1165, F'=free_1163, Z1'=0, B2'=free_1163, C2'=0, D2'=free_1163, E2'=A2, [ A2>=1+free_1166 && Q2>=0 && 0>=free_1164 && free_1165>=2 && free_1166>=1+free_1163 && free_1163>=1 && Z1==0 ], cost: 1
    178: f17 -> f27 : B'=free_1233, C'=free_1228, E'=free_1232, Y1'=free_1236, Z1'=free_1235, A2'=free_1230, B2'=free_1231, C2'=free_1234, D2'=free_1227, E2'=free_1229, [ J2>=0 && 0>=free_1233 && free_1232>=2 && 0>=1+free_1228 && 0>=1+free_1229 && Z1==A2 ], cost: 1
    179: f17 -> f27 : B'=free_1243, C'=free_1238, E'=free_1242, Y1'=free_1246, Z1'=free_1245, A2'=free_1240, B2'=free_1241, C2'=free_1244, D2'=free_1237, E2'=free_1239, [ J2>=0 && 0>=free_1243 && free_1242>=2 && 0>=1+free_1238 && free_1239>=1 && Z1==A2 ], cost: 1
    180: f17 -> f27 : B'=free_1253, C'=free_1248, E'=free_1252, Y1'=free_1256, Z1'=free_1255, A2'=free_1250, B2'=free_1251, C2'=free_1254, D2'=free_1247, E2'=free_1249, [ J2>=0 && 0>=free_1253 && free_1252>=2 && free_1248>=1 && 0>=1+free_1249 && Z1==A2 ], cost: 1
    181: f17 -> f27 : B'=free_1263, C'=free_1258, E'=free_1262, Y1'=free_1266, Z1'=free_1265, A2'=free_1260, B2'=free_1261, C2'=free_1264, D2'=free_1257, E2'=free_1259, [ J2>=0 && 0>=free_1263 && free_1262>=2 && free_1258>=1 && free_1259>=1 && Z1==A2 ], cost: 1
    170: f17 -> f17 : B'=free_1188, C'=free_1187, E'=free_1189, F'=free_1187, J'=free_1190, Z1'=0, B2'=free_1187, C2'=0, D2'=free_1187, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ free_1191>=1+A2 && J2>=0 && 0>=free_1188 && free_1189>=2 && free_1187>=1+free_1191 && 0>=1+free_1187 && Z1==0 ], cost: 1
    171: f17 -> f17 : B'=free_1193, C'=free_1192, E'=free_1194, F'=free_1192, J'=free_1195, Z1'=0, B2'=free_1192, C2'=0, D2'=free_1192, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ free_1196>=1+A2 && J2>=0 && 0>=free_1193 && free_1194>=2 && free_1192>=1+free_1196 && free_1192>=1 && Z1==0 ], cost: 1
    172: f17 -> f17 : B'=free_1198, C'=free_1197, E'=free_1199, F'=free_1197, J'=free_1200, Z1'=0, B2'=free_1197, C2'=0, D2'=free_1197, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ free_1201>=1+A2 && J2>=0 && 0>=free_1198 && free_1199>=2 && free_1201>=1+free_1197 && 0>=1+free_1197 && Z1==0 ], cost: 1
    173: f17 -> f17 : B'=free_1203, C'=free_1202, E'=free_1204, F'=free_1202, J'=free_1205, Z1'=0, B2'=free_1202, C2'=0, D2'=free_1202, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ free_1206>=1+A2 && J2>=0 && 0>=free_1203 && free_1204>=2 && free_1206>=1+free_1202 && free_1202>=1 && Z1==0 ], cost: 1
    174: f17 -> f17 : B'=free_1208, C'=free_1207, E'=free_1209, F'=free_1207, J'=free_1210, Z1'=0, B2'=free_1207, C2'=0, D2'=free_1207, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ A2>=1+free_1211 && J2>=0 && 0>=free_1208 && free_1209>=2 && free_1207>=1+free_1211 && 0>=1+free_1207 && Z1==0 ], cost: 1
    175: f17 -> f17 : B'=free_1213, C'=free_1212, E'=free_1214, F'=free_1212, J'=free_1215, Z1'=0, B2'=free_1212, C2'=0, D2'=free_1212, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ A2>=1+free_1216 && J2>=0 && 0>=free_1213 && free_1214>=2 && free_1212>=1+free_1216 && free_1212>=1 && Z1==0 ], cost: 1
    176: f17 -> f17 : B'=free_1218, C'=free_1217, E'=free_1219, F'=free_1217, J'=free_1220, Z1'=0, B2'=free_1217, C2'=0, D2'=free_1217, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ A2>=1+free_1221 && J2>=0 && 0>=free_1218 && free_1219>=2 && free_1221>=1+free_1217 && 0>=1+free_1217 && Z1==0 ], cost: 1
    177: f17 -> f17 : B'=free_1223, C'=free_1222, E'=free_1224, F'=free_1222, J'=free_1225, Z1'=0, B2'=free_1222, C2'=0, D2'=free_1222, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ A2>=1+free_1226 && J2>=0 && 0>=free_1223 && free_1224>=2 && free_1226>=1+free_1222 && free_1222>=1 && Z1==0 ], cost: 1
    199: f26 -> f32 : A'=free_1348, C'=S1, E'=1, F'=S1, M'=free_1345, Q1_1'=free_1347, R1'=free_1350, S1'=free_1346, T1'=free_1351, W1'=free_1344, X1'=free_1349, Y1'=free_1352, [], cost: 1
    198: f26 -> f1 : A'=2, E'=free_1342, M'=free_1340, Q1_1'=free_1342, R1'=free_1341, S1'=free_1343, T1'=free_1341, W1'=free_1341, M2'=free_1339, [ free_1342>=2 ], cost: 1
    200: f26 -> f27 : A'=free_1358, C'=0, E'=free_1360, F'=0, M'=free_1363, Q1_1'=free_1368, R1'=free_1356, S1'=free_1357, T1'=free_1367, W1'=free_1362, X1'=free_1361, Y1'=free_1366, Z1'=free_1353, A2'=free_1365, B2'=free_1354, C2'=free_1359, D2'=free_1364, E2'=free_1355, [ 0>=free_1360 && 0>=free_1370 && 0>=free_1371 && 0>=free_1369 ], cost: 1


Simplified the transitions:
  Start location: f26
      4: f29 -> f29 : B'=-1+B, E'=free_26, F'=C, G'=free_24, M'=free_25, N'=B, O'=A, [ A>=free_26 && A>=0 && B>=1 && free_26>=2 && 0>=1+free_27 && 0>=1+free_24 ], cost: 1
      5: f29 -> f29 : B'=-1+B, E'=free_30, F'=C, G'=free_28, M'=free_29, N'=B, O'=A, [ A>=free_30 && A>=0 && B>=1 && free_30>=2 && 0>=1+free_31 && free_28>=1 ], cost: 1
      6: f29 -> f29 : B'=-1+B, E'=free_34, F'=C, G'=free_32, M'=free_33, N'=B, O'=A, [ A>=free_34 && A>=0 && B>=1 && free_34>=2 && free_35>=1 && 0>=1+free_32 ], cost: 1
      7: f29 -> f29 : B'=-1+B, E'=free_38, F'=C, G'=free_36, M'=free_37, N'=B, O'=A, [ A>=free_38 && A>=0 && B>=1 && free_38>=2 && free_39>=1 && free_36>=1 ], cost: 1
      0: f29 -> f34 : D'=1, E'=free_3, F'=free_1, G'=0, H'=Q, J'=free_2, K'=1+Q, L'=free_4, M'=free, [ A>=0 && B>=1 && free_3>=2 && 0>=1+C && free_5>=free_3 && 0>=1+free_1 && D==1 ], cost: 1
      1: f29 -> f34 : D'=1, E'=free_9, F'=free_7, G'=0, H'=Q, J'=free_8, K'=1+Q, L'=free_10, M'=free_6, [ A>=0 && B>=1 && free_9>=2 && 0>=1+C && free_11>=free_9 && free_7>=1 && D==1 ], cost: 1
      2: f29 -> f34 : D'=1, E'=free_15, F'=free_13, G'=0, H'=Q, J'=free_14, K'=1+Q, L'=free_16, M'=free_12, [ A>=0 && B>=1 && free_15>=2 && C>=1 && free_17>=free_15 && 0>=1+free_13 && D==1 ], cost: 1
      3: f29 -> f34 : D'=1, E'=free_21, F'=free_19, G'=0, H'=Q, J'=free_20, K'=1+Q, L'=free_22, M'=free_18, [ A>=0 && B>=1 && free_21>=2 && C>=1 && free_23>=free_21 && free_19>=1 && D==1 ], cost: 1
    182: f29 -> f17 : B'=free_1267, C'=F, E'=free_1268, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1270>=free_1268 && 0>=free_1271 && free_1269>=2 && A>=free_1269 && 0>=free_1267 && A>=0 && free_1268>=2 && 0>=B && F>=1 && 0>=1+C && 0>=1+F ], cost: 1
    183: f29 -> f17 : B'=free_1272, C'=F, E'=free_1273, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1275>=free_1273 && 0>=free_1276 && free_1274>=2 && A>=free_1274 && 0>=free_1272 && A>=0 && free_1273>=2 && 0>=B && F>=1 && 0>=1+C ], cost: 1
    184: f29 -> f17 : B'=free_1277, C'=F, E'=free_1278, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1280>=free_1278 && 0>=free_1281 && free_1279>=2 && A>=free_1279 && 0>=free_1277 && A>=0 && free_1278>=2 && 0>=B && F>=1 && C>=1 && 0>=1+F ], cost: 1
    185: f29 -> f17 : B'=free_1282, C'=F, E'=free_1283, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1285>=free_1283 && 0>=free_1286 && free_1284>=2 && A>=free_1284 && 0>=free_1282 && A>=0 && free_1283>=2 && 0>=B && F>=1 && C>=1 ], cost: 1
    186: f29 -> f17 : B'=free_1287, C'=F, E'=free_1288, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1290>=free_1288 && 0>=free_1291 && free_1289>=2 && A>=free_1289 && 0>=free_1287 && A>=0 && free_1288>=2 && 0>=B && 0>=1+F && 0>=1+C ], cost: 1
    187: f29 -> f17 : B'=free_1292, C'=F, E'=free_1293, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1295>=free_1293 && 0>=free_1296 && free_1294>=2 && A>=free_1294 && 0>=free_1292 && A>=0 && free_1293>=2 && 0>=B && 0>=1+F && 0>=1+C && F>=1 ], cost: 1
    188: f29 -> f17 : B'=free_1297, C'=F, E'=free_1298, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1300>=free_1298 && 0>=free_1301 && free_1299>=2 && A>=free_1299 && 0>=free_1297 && A>=0 && free_1298>=2 && 0>=B && 0>=1+F && C>=1 ], cost: 1
    189: f29 -> f17 : B'=free_1302, C'=F, E'=free_1303, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1305>=free_1303 && 0>=free_1306 && free_1304>=2 && A>=free_1304 && 0>=free_1302 && A>=0 && free_1303>=2 && 0>=B && 0>=1+F && C>=1 && F>=1 ], cost: 1
     60: f34 -> f34 : D'=1+D, E'=free_295, F'=free_293, G'=0, Q'=-1+Q, J'=free_294, M'=free_296, E1'=C, F1'=free_292, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_295>=2 && 0>=1+free_297 && 0>=1+free_293 && 0>=1+free_292 ], cost: 1
     61: f34 -> f34 : D'=1+D, E'=free_301, F'=free_299, G'=0, Q'=-1+Q, J'=free_300, M'=free_302, E1'=C, F1'=free_298, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_301>=2 && 0>=1+free_303 && 0>=1+free_299 && free_298>=1 ], cost: 1
     62: f34 -> f34 : D'=1+D, E'=free_307, F'=free_305, G'=0, Q'=-1+Q, J'=free_306, M'=free_308, E1'=C, F1'=free_304, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_307>=2 && 0>=1+free_309 && free_305>=1 && 0>=1+free_304 ], cost: 1
     63: f34 -> f34 : D'=1+D, E'=free_313, F'=free_311, G'=0, Q'=-1+Q, J'=free_312, M'=free_314, E1'=C, F1'=free_310, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_313>=2 && 0>=1+free_315 && free_311>=1 && free_310>=1 ], cost: 1
     64: f34 -> f34 : D'=1+D, E'=free_319, F'=free_317, G'=0, Q'=-1+Q, J'=free_318, M'=free_320, E1'=C, F1'=free_316, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_319>=2 && free_321>=1 && 0>=1+free_317 && 0>=1+free_316 ], cost: 1
     65: f34 -> f34 : D'=1+D, E'=free_325, F'=free_323, G'=0, Q'=-1+Q, J'=free_324, M'=free_326, E1'=C, F1'=free_322, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_325>=2 && free_327>=1 && 0>=1+free_323 && free_322>=1 ], cost: 1
     66: f34 -> f34 : D'=1+D, E'=free_331, F'=free_329, G'=0, Q'=-1+Q, J'=free_330, M'=free_332, E1'=C, F1'=free_328, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_331>=2 && free_333>=1 && free_329>=1 && 0>=1+free_328 ], cost: 1
     67: f34 -> f34 : D'=1+D, E'=free_337, F'=free_335, G'=0, Q'=-1+Q, J'=free_336, M'=free_338, E1'=C, F1'=free_334, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_337>=2 && free_339>=1 && free_335>=1 && free_334>=1 ], cost: 1
     52: f34 -> f35 : B'=-1+B, E'=free_262, F'=free_260, G'=free_261, M'=free_263, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_262>=2 && 0>=1+C && 0>=1+free_261 && 0>=1+free_260 ], cost: 1
     53: f34 -> f35 : B'=-1+B, E'=free_266, F'=free_264, G'=free_265, M'=free_267, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_266>=2 && 0>=1+C && 0>=1+free_265 && free_264>=1 ], cost: 1
     54: f34 -> f35 : B'=-1+B, E'=free_270, F'=free_268, G'=free_269, M'=free_271, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_270>=2 && 0>=1+C && free_269>=1 && 0>=1+free_268 ], cost: 1
     55: f34 -> f35 : B'=-1+B, E'=free_274, F'=free_272, G'=free_273, M'=free_275, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_274>=2 && 0>=1+C && free_273>=1 && free_272>=1 ], cost: 1
     56: f34 -> f35 : B'=-1+B, E'=free_278, F'=free_276, G'=free_277, M'=free_279, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_278>=2 && C>=1 && 0>=1+free_277 && 0>=1+free_276 ], cost: 1
     57: f34 -> f35 : B'=-1+B, E'=free_282, F'=free_280, G'=free_281, M'=free_283, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_282>=2 && C>=1 && 0>=1+free_281 && free_280>=1 ], cost: 1
     58: f34 -> f35 : B'=-1+B, E'=free_286, F'=free_284, G'=free_285, M'=free_287, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_286>=2 && C>=1 && free_285>=1 && 0>=1+free_284 ], cost: 1
     59: f34 -> f35 : B'=-1+B, E'=free_290, F'=free_288, G'=free_289, M'=free_291, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_290>=2 && C>=1 && free_289>=1 && free_288>=1 ], cost: 1
    194: f34 -> f15 : B'=free_1323, C'=0, D'=1+G2, E'=free_1324, G'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1325>=1 && free_1326>=2 && free_1323>=1 && free_1324>=2 && F>=1 && Q>=0 && D>=0 && 0>=1+F && C==0 ], cost: 1
    195: f34 -> f15 : B'=free_1327, C'=0, D'=1+G2, E'=free_1328, G'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1329>=1 && free_1330>=2 && free_1327>=1 && free_1328>=2 && F>=1 && Q>=0 && D>=0 && C==0 ], cost: 1
    196: f34 -> f15 : B'=free_1331, C'=0, D'=1+G2, E'=free_1332, G'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1333>=1 && free_1334>=2 && free_1331>=1 && free_1332>=2 && 0>=1+F && Q>=0 && D>=0 && C==0 ], cost: 1
    197: f34 -> f15 : B'=free_1335, C'=0, D'=1+G2, E'=free_1336, G'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1337>=1 && free_1338>=2 && free_1335>=1 && free_1336>=2 && 0>=1+F && Q>=0 && D>=0 && F>=1 && C==0 ], cost: 1
     84: f35 -> f34 : D'=1+D, E'=free_423, F'=free_421, G'=0, Q'=-1+Q, J'=free_422, M'=free_424, Q1'=free_420, M1'=C, N1'=free_425, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_423>=2 && 0>=1+free_426 && 0>=1+free_425 && 0>=1+free_421 && 0>=1+free_420 ], cost: 1
     85: f35 -> f34 : D'=1+D, E'=free_430, F'=free_428, G'=0, Q'=-1+Q, J'=free_429, M'=free_431, Q1'=free_427, M1'=C, N1'=free_432, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_430>=2 && 0>=1+free_433 && 0>=1+free_432 && 0>=1+free_428 && free_427>=1 ], cost: 1
     86: f35 -> f34 : D'=1+D, E'=free_437, F'=free_435, G'=0, Q'=-1+Q, J'=free_436, M'=free_438, Q1'=free_434, M1'=C, N1'=free_439, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_437>=2 && 0>=1+free_440 && 0>=1+free_439 && free_435>=1 && 0>=1+free_434 ], cost: 1
     87: f35 -> f34 : D'=1+D, E'=free_444, F'=free_442, G'=0, Q'=-1+Q, J'=free_443, M'=free_445, Q1'=free_441, M1'=C, N1'=free_446, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_444>=2 && 0>=1+free_447 && 0>=1+free_446 && free_442>=1 && free_441>=1 ], cost: 1
     88: f35 -> f34 : D'=1+D, E'=free_451, F'=free_449, G'=0, Q'=-1+Q, J'=free_450, M'=free_452, Q1'=free_448, M1'=C, N1'=free_453, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_451>=2 && 0>=1+free_454 && free_453>=1 && 0>=1+free_449 && 0>=1+free_448 ], cost: 1
     89: f35 -> f34 : D'=1+D, E'=free_458, F'=free_456, G'=0, Q'=-1+Q, J'=free_457, M'=free_459, Q1'=free_455, M1'=C, N1'=free_460, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_458>=2 && 0>=1+free_461 && free_460>=1 && 0>=1+free_456 && free_455>=1 ], cost: 1
     90: f35 -> f34 : D'=1+D, E'=free_465, F'=free_463, G'=0, Q'=-1+Q, J'=free_464, M'=free_466, Q1'=free_462, M1'=C, N1'=free_467, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_465>=2 && 0>=1+free_468 && free_467>=1 && free_463>=1 && 0>=1+free_462 ], cost: 1
     91: f35 -> f34 : D'=1+D, E'=free_472, F'=free_470, G'=0, Q'=-1+Q, J'=free_471, M'=free_473, Q1'=free_469, M1'=C, N1'=free_474, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_472>=2 && 0>=1+free_475 && free_474>=1 && free_470>=1 && free_469>=1 ], cost: 1
     92: f35 -> f34 : D'=1+D, E'=free_479, F'=free_477, G'=0, Q'=-1+Q, J'=free_478, M'=free_480, Q1'=free_476, M1'=C, N1'=free_481, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_479>=2 && free_482>=1 && 0>=1+free_481 && 0>=1+free_477 && 0>=1+free_476 ], cost: 1
     93: f35 -> f34 : D'=1+D, E'=free_486, F'=free_484, G'=0, Q'=-1+Q, J'=free_485, M'=free_487, Q1'=free_483, M1'=C, N1'=free_488, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_486>=2 && free_489>=1 && 0>=1+free_488 && 0>=1+free_484 && free_483>=1 ], cost: 1
     94: f35 -> f34 : D'=1+D, E'=free_493, F'=free_491, G'=0, Q'=-1+Q, J'=free_492, M'=free_494, Q1'=free_490, M1'=C, N1'=free_495, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_493>=2 && free_496>=1 && 0>=1+free_495 && free_491>=1 && 0>=1+free_490 ], cost: 1
     95: f35 -> f34 : D'=1+D, E'=free_500, F'=free_498, G'=0, Q'=-1+Q, J'=free_499, M'=free_501, Q1'=free_497, M1'=C, N1'=free_502, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_500>=2 && free_503>=1 && 0>=1+free_502 && free_498>=1 && free_497>=1 ], cost: 1
     96: f35 -> f34 : D'=1+D, E'=free_507, F'=free_505, G'=0, Q'=-1+Q, J'=free_506, M'=free_508, Q1'=free_504, M1'=C, N1'=free_509, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_507>=2 && free_510>=1 && free_509>=1 && 0>=1+free_505 && 0>=1+free_504 ], cost: 1
     97: f35 -> f34 : D'=1+D, E'=free_514, F'=free_512, G'=0, Q'=-1+Q, J'=free_513, M'=free_515, Q1'=free_511, M1'=C, N1'=free_516, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_514>=2 && free_517>=1 && free_516>=1 && 0>=1+free_512 && free_511>=1 ], cost: 1
     98: f35 -> f34 : D'=1+D, E'=free_521, F'=free_519, G'=0, Q'=-1+Q, J'=free_520, M'=free_522, Q1'=free_518, M1'=C, N1'=free_523, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_521>=2 && free_524>=1 && free_523>=1 && free_519>=1 && 0>=1+free_518 ], cost: 1
     99: f35 -> f34 : D'=1+D, E'=free_528, F'=free_526, G'=0, Q'=-1+Q, J'=free_527, M'=free_529, Q1'=free_525, M1'=C, N1'=free_530, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_528>=2 && free_531>=1 && free_530>=1 && free_526>=1 && free_525>=1 ], cost: 1
     68: f35 -> f35 : B'=-1+B, E'=free_343, F'=free_341, G'=free_342, M'=free_344, Q1'=free_340, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_343>=2 && 0>=1+C && 0>=1+free_342 && 0>=1+free_340 && 0>=1+free_341 ], cost: 1
     69: f35 -> f35 : B'=-1+B, E'=free_348, F'=free_346, G'=free_347, M'=free_349, Q1'=free_345, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_348>=2 && 0>=1+C && 0>=1+free_347 && 0>=1+free_345 && free_346>=1 ], cost: 1
     70: f35 -> f35 : B'=-1+B, E'=free_353, F'=free_351, G'=free_352, M'=free_354, Q1'=free_350, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_353>=2 && 0>=1+C && 0>=1+free_352 && free_350>=1 && 0>=1+free_351 ], cost: 1
     71: f35 -> f35 : B'=-1+B, E'=free_358, F'=free_356, G'=free_357, M'=free_359, Q1'=free_355, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_358>=2 && 0>=1+C && 0>=1+free_357 && free_355>=1 && free_356>=1 ], cost: 1
     72: f35 -> f35 : B'=-1+B, E'=free_363, F'=free_361, G'=free_362, M'=free_364, Q1'=free_360, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_363>=2 && 0>=1+C && free_362>=1 && 0>=1+free_360 && 0>=1+free_361 ], cost: 1
     73: f35 -> f35 : B'=-1+B, E'=free_368, F'=free_366, G'=free_367, M'=free_369, Q1'=free_365, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_368>=2 && 0>=1+C && free_367>=1 && 0>=1+free_365 && free_366>=1 ], cost: 1
     74: f35 -> f35 : B'=-1+B, E'=free_373, F'=free_371, G'=free_372, M'=free_374, Q1'=free_370, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_373>=2 && 0>=1+C && free_372>=1 && free_370>=1 && 0>=1+free_371 ], cost: 1
     75: f35 -> f35 : B'=-1+B, E'=free_378, F'=free_376, G'=free_377, M'=free_379, Q1'=free_375, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_378>=2 && 0>=1+C && free_377>=1 && free_375>=1 && free_376>=1 ], cost: 1
     76: f35 -> f35 : B'=-1+B, E'=free_383, F'=free_381, G'=free_382, M'=free_384, Q1'=free_380, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_383>=2 && C>=1 && 0>=1+free_382 && 0>=1+free_380 && 0>=1+free_381 ], cost: 1
     77: f35 -> f35 : B'=-1+B, E'=free_388, F'=free_386, G'=free_387, M'=free_389, Q1'=free_385, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_388>=2 && C>=1 && 0>=1+free_387 && 0>=1+free_385 && free_386>=1 ], cost: 1
     78: f35 -> f35 : B'=-1+B, E'=free_393, F'=free_391, G'=free_392, M'=free_394, Q1'=free_390, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_393>=2 && C>=1 && 0>=1+free_392 && free_390>=1 && 0>=1+free_391 ], cost: 1
     79: f35 -> f35 : B'=-1+B, E'=free_398, F'=free_396, G'=free_397, M'=free_399, Q1'=free_395, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_398>=2 && C>=1 && 0>=1+free_397 && free_395>=1 && free_396>=1 ], cost: 1
     80: f35 -> f35 : B'=-1+B, E'=free_403, F'=free_401, G'=free_402, M'=free_404, Q1'=free_400, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_403>=2 && C>=1 && free_402>=1 && 0>=1+free_400 && 0>=1+free_401 ], cost: 1
     81: f35 -> f35 : B'=-1+B, E'=free_408, F'=free_406, G'=free_407, M'=free_409, Q1'=free_405, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_408>=2 && C>=1 && free_407>=1 && 0>=1+free_405 && free_406>=1 ], cost: 1
     82: f35 -> f35 : B'=-1+B, E'=free_413, F'=free_411, G'=free_412, M'=free_414, Q1'=free_410, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_413>=2 && C>=1 && free_412>=1 && free_410>=1 && 0>=1+free_411 ], cost: 1
     83: f35 -> f35 : B'=-1+B, E'=free_418, F'=free_416, G'=free_417, M'=free_419, Q1'=free_415, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_418>=2 && C>=1 && free_417>=1 && free_415>=1 && free_416>=1 ], cost: 1
     48: f32 -> f32 : B'=-1+B, E'=1, F'=C, G'=free_249, M'=free_248, A1'=B, B1'=C1, [ B>=1 && 0>=1+free_250 && 0>=1+free_249 ], cost: 1
     49: f32 -> f32 : B'=-1+B, E'=1, F'=C, G'=free_252, M'=free_251, A1'=B, B1'=C1, [ B>=1 && 0>=1+free_253 && free_252>=1 ], cost: 1
     50: f32 -> f32 : B'=-1+B, E'=1, F'=C, G'=free_255, M'=free_254, A1'=B, B1'=C1, [ B>=1 && free_256>=1 && 0>=1+free_255 ], cost: 1
     51: f32 -> f32 : B'=-1+B, E'=1, F'=C, G'=free_258, M'=free_257, A1'=B, B1'=C1, [ B>=1 && free_259>=1 && free_258>=1 ], cost: 1
    101: f1 -> f29 : A'=free_535, C'=R1, E'=free_538, F'=R1, Q1_1'=free_537, R1'=free_540, S1'=free_536, T1'=free_541, W1'=free_534, X1'=free_539, Y1'=free_542, [ A>=Q1_1 && A>=0 && free_535>=free_538 && free_538>=2 ], cost: 1
    100: f1 -> f1 : A'=1+A, R1'=S1, S1'=free_533, T1'=S1, U1'=free_532, V1'=A, [ Q1_1>=1+A && A>=0 ], cost: 1
    148: f15 -> f15 : B'=free_1056, C'=0, E'=free_1057, F'=free_1055, G'=0, J'=free_1058, Z1'=0, B2'=free_1055, C2'=0, D2'=free_1055, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ free_1059>=1+A2 && G2>=0 && free_1057>=2 && free_1056>=1 && free_1055>=1+free_1059 && 0>=1+free_1055 && Z1==0 ], cost: 1
    149: f15 -> f15 : B'=free_1061, C'=0, E'=free_1062, F'=free_1060, G'=0, J'=free_1063, Z1'=0, B2'=free_1060, C2'=0, D2'=free_1060, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ free_1064>=1+A2 && G2>=0 && free_1062>=2 && free_1061>=1 && free_1060>=1+free_1064 && free_1060>=1 && Z1==0 ], cost: 1
    150: f15 -> f15 : B'=free_1066, C'=0, E'=free_1067, F'=free_1065, G'=0, J'=free_1068, Z1'=0, B2'=free_1065, C2'=0, D2'=free_1065, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ free_1069>=1+A2 && G2>=0 && free_1067>=2 && free_1066>=1 && free_1069>=1+free_1065 && 0>=1+free_1065 && Z1==0 ], cost: 1
    151: f15 -> f15 : B'=free_1071, C'=0, E'=free_1072, F'=free_1070, G'=0, J'=free_1073, Z1'=0, B2'=free_1070, C2'=0, D2'=free_1070, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ free_1074>=1+A2 && G2>=0 && free_1072>=2 && free_1071>=1 && free_1074>=1+free_1070 && free_1070>=1 && Z1==0 ], cost: 1
    152: f15 -> f15 : B'=free_1076, C'=0, E'=free_1077, F'=free_1075, G'=0, J'=free_1078, Z1'=0, B2'=free_1075, C2'=0, D2'=free_1075, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ A2>=1+free_1079 && G2>=0 && free_1077>=2 && free_1076>=1 && free_1075>=1+free_1079 && 0>=1+free_1075 && Z1==0 ], cost: 1
    153: f15 -> f15 : B'=free_1081, C'=0, E'=free_1082, F'=free_1080, G'=0, J'=free_1083, Z1'=0, B2'=free_1080, C2'=0, D2'=free_1080, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ A2>=1+free_1084 && G2>=0 && free_1082>=2 && free_1081>=1 && free_1080>=1+free_1084 && free_1080>=1 && Z1==0 ], cost: 1
    154: f15 -> f15 : B'=free_1086, C'=0, E'=free_1087, F'=free_1085, G'=0, J'=free_1088, Z1'=0, B2'=free_1085, C2'=0, D2'=free_1085, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ A2>=1+free_1089 && G2>=0 && free_1087>=2 && free_1086>=1 && free_1089>=1+free_1085 && 0>=1+free_1085 && Z1==0 ], cost: 1
    155: f15 -> f15 : B'=free_1091, C'=0, E'=free_1092, F'=free_1090, G'=0, J'=free_1093, Z1'=0, B2'=free_1090, C2'=0, D2'=free_1090, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ A2>=1+free_1094 && G2>=0 && free_1092>=2 && free_1091>=1 && free_1094>=1+free_1090 && free_1090>=1 && Z1==0 ], cost: 1
    170: f17 -> f17 : B'=free_1188, C'=free_1187, E'=free_1189, F'=free_1187, J'=free_1190, Z1'=0, B2'=free_1187, C2'=0, D2'=free_1187, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ free_1191>=1+A2 && J2>=0 && 0>=free_1188 && free_1189>=2 && free_1187>=1+free_1191 && 0>=1+free_1187 && Z1==0 ], cost: 1
    171: f17 -> f17 : B'=free_1193, C'=free_1192, E'=free_1194, F'=free_1192, J'=free_1195, Z1'=0, B2'=free_1192, C2'=0, D2'=free_1192, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ free_1196>=1+A2 && J2>=0 && 0>=free_1193 && free_1194>=2 && free_1192>=1+free_1196 && free_1192>=1 && Z1==0 ], cost: 1
    172: f17 -> f17 : B'=free_1198, C'=free_1197, E'=free_1199, F'=free_1197, J'=free_1200, Z1'=0, B2'=free_1197, C2'=0, D2'=free_1197, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ free_1201>=1+A2 && J2>=0 && 0>=free_1198 && free_1199>=2 && free_1201>=1+free_1197 && 0>=1+free_1197 && Z1==0 ], cost: 1
    173: f17 -> f17 : B'=free_1203, C'=free_1202, E'=free_1204, F'=free_1202, J'=free_1205, Z1'=0, B2'=free_1202, C2'=0, D2'=free_1202, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ free_1206>=1+A2 && J2>=0 && 0>=free_1203 && free_1204>=2 && free_1206>=1+free_1202 && free_1202>=1 && Z1==0 ], cost: 1
    174: f17 -> f17 : B'=free_1208, C'=free_1207, E'=free_1209, F'=free_1207, J'=free_1210, Z1'=0, B2'=free_1207, C2'=0, D2'=free_1207, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ A2>=1+free_1211 && J2>=0 && 0>=free_1208 && free_1209>=2 && free_1207>=1+free_1211 && 0>=1+free_1207 && Z1==0 ], cost: 1
    175: f17 -> f17 : B'=free_1213, C'=free_1212, E'=free_1214, F'=free_1212, J'=free_1215, Z1'=0, B2'=free_1212, C2'=0, D2'=free_1212, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ A2>=1+free_1216 && J2>=0 && 0>=free_1213 && free_1214>=2 && free_1212>=1+free_1216 && free_1212>=1 && Z1==0 ], cost: 1
    176: f17 -> f17 : B'=free_1218, C'=free_1217, E'=free_1219, F'=free_1217, J'=free_1220, Z1'=0, B2'=free_1217, C2'=0, D2'=free_1217, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ A2>=1+free_1221 && J2>=0 && 0>=free_1218 && free_1219>=2 && free_1221>=1+free_1217 && 0>=1+free_1217 && Z1==0 ], cost: 1
    177: f17 -> f17 : B'=free_1223, C'=free_1222, E'=free_1224, F'=free_1222, J'=free_1225, Z1'=0, B2'=free_1222, C2'=0, D2'=free_1222, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ A2>=1+free_1226 && J2>=0 && 0>=free_1223 && free_1224>=2 && free_1226>=1+free_1222 && free_1222>=1 && Z1==0 ], cost: 1
    199: f26 -> f32 : A'=free_1348, C'=S1, E'=1, F'=S1, M'=free_1345, Q1_1'=free_1347, R1'=free_1350, S1'=free_1346, T1'=free_1351, W1'=free_1344, X1'=free_1349, Y1'=free_1352, [], cost: 1
    198: f26 -> f1 : A'=2, E'=free_1342, M'=free_1340, Q1_1'=free_1342, R1'=free_1341, S1'=free_1343, T1'=free_1341, W1'=free_1341, M2'=free_1339, [ free_1342>=2 ], cost: 1

Eliminating 4 self-loops for location f29
  Self-Loop 4 has the metering function: B, resulting in the new transition 201.
  Self-Loop 5 has the metering function: B, resulting in the new transition 202.
  Self-Loop 6 has the metering function: B, resulting in the new transition 203.
  Removing the self-loops: 4 5 6.

Removed all Self-loops using metering functions (where possible):
  Start location: f26
    201: f29 -> [15] : B'=0, E'=free_26, F'=C, G'=free_24, M'=free_25, N'=1, O'=A, [ A>=free_26 && A>=0 && B>=1 && free_26>=2 && 0>=1+free_24 ], cost: B
    202: f29 -> [15] : B'=0, E'=free_30, F'=C, G'=free_28, M'=free_29, N'=1, O'=A, [ A>=free_30 && A>=0 && B>=1 && free_30>=2 && free_28>=1 ], cost: B
    203: f29 -> [15] : B'=0, E'=free_34, F'=C, G'=free_32, M'=free_33, N'=1, O'=A, [ A>=free_34 && A>=0 && B>=1 && free_34>=2 && 0>=1+free_32 ], cost: B
     60: f34 -> f34 : D'=1+D, E'=free_295, F'=free_293, G'=0, Q'=-1+Q, J'=free_294, M'=free_296, E1'=C, F1'=free_292, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_295>=2 && 0>=1+free_297 && 0>=1+free_293 && 0>=1+free_292 ], cost: 1
     61: f34 -> f34 : D'=1+D, E'=free_301, F'=free_299, G'=0, Q'=-1+Q, J'=free_300, M'=free_302, E1'=C, F1'=free_298, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_301>=2 && 0>=1+free_303 && 0>=1+free_299 && free_298>=1 ], cost: 1
     62: f34 -> f34 : D'=1+D, E'=free_307, F'=free_305, G'=0, Q'=-1+Q, J'=free_306, M'=free_308, E1'=C, F1'=free_304, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_307>=2 && 0>=1+free_309 && free_305>=1 && 0>=1+free_304 ], cost: 1
     63: f34 -> f34 : D'=1+D, E'=free_313, F'=free_311, G'=0, Q'=-1+Q, J'=free_312, M'=free_314, E1'=C, F1'=free_310, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_313>=2 && 0>=1+free_315 && free_311>=1 && free_310>=1 ], cost: 1
     64: f34 -> f34 : D'=1+D, E'=free_319, F'=free_317, G'=0, Q'=-1+Q, J'=free_318, M'=free_320, E1'=C, F1'=free_316, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_319>=2 && free_321>=1 && 0>=1+free_317 && 0>=1+free_316 ], cost: 1
     65: f34 -> f34 : D'=1+D, E'=free_325, F'=free_323, G'=0, Q'=-1+Q, J'=free_324, M'=free_326, E1'=C, F1'=free_322, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_325>=2 && free_327>=1 && 0>=1+free_323 && free_322>=1 ], cost: 1
     66: f34 -> f34 : D'=1+D, E'=free_331, F'=free_329, G'=0, Q'=-1+Q, J'=free_330, M'=free_332, E1'=C, F1'=free_328, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_331>=2 && free_333>=1 && free_329>=1 && 0>=1+free_328 ], cost: 1
     67: f34 -> f34 : D'=1+D, E'=free_337, F'=free_335, G'=0, Q'=-1+Q, J'=free_336, M'=free_338, E1'=C, F1'=free_334, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_337>=2 && free_339>=1 && free_335>=1 && free_334>=1 ], cost: 1
     52: f34 -> f35 : B'=-1+B, E'=free_262, F'=free_260, G'=free_261, M'=free_263, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_262>=2 && 0>=1+C && 0>=1+free_261 && 0>=1+free_260 ], cost: 1
     53: f34 -> f35 : B'=-1+B, E'=free_266, F'=free_264, G'=free_265, M'=free_267, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_266>=2 && 0>=1+C && 0>=1+free_265 && free_264>=1 ], cost: 1
     54: f34 -> f35 : B'=-1+B, E'=free_270, F'=free_268, G'=free_269, M'=free_271, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_270>=2 && 0>=1+C && free_269>=1 && 0>=1+free_268 ], cost: 1
     55: f34 -> f35 : B'=-1+B, E'=free_274, F'=free_272, G'=free_273, M'=free_275, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_274>=2 && 0>=1+C && free_273>=1 && free_272>=1 ], cost: 1
     56: f34 -> f35 : B'=-1+B, E'=free_278, F'=free_276, G'=free_277, M'=free_279, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_278>=2 && C>=1 && 0>=1+free_277 && 0>=1+free_276 ], cost: 1
     57: f34 -> f35 : B'=-1+B, E'=free_282, F'=free_280, G'=free_281, M'=free_283, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_282>=2 && C>=1 && 0>=1+free_281 && free_280>=1 ], cost: 1
     58: f34 -> f35 : B'=-1+B, E'=free_286, F'=free_284, G'=free_285, M'=free_287, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_286>=2 && C>=1 && free_285>=1 && 0>=1+free_284 ], cost: 1
     59: f34 -> f35 : B'=-1+B, E'=free_290, F'=free_288, G'=free_289, M'=free_291, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_290>=2 && C>=1 && free_289>=1 && free_288>=1 ], cost: 1
    194: f34 -> f15 : B'=free_1323, C'=0, D'=1+G2, E'=free_1324, G'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1325>=1 && free_1326>=2 && free_1323>=1 && free_1324>=2 && F>=1 && Q>=0 && D>=0 && 0>=1+F && C==0 ], cost: 1
    195: f34 -> f15 : B'=free_1327, C'=0, D'=1+G2, E'=free_1328, G'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1329>=1 && free_1330>=2 && free_1327>=1 && free_1328>=2 && F>=1 && Q>=0 && D>=0 && C==0 ], cost: 1
    196: f34 -> f15 : B'=free_1331, C'=0, D'=1+G2, E'=free_1332, G'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1333>=1 && free_1334>=2 && free_1331>=1 && free_1332>=2 && 0>=1+F && Q>=0 && D>=0 && C==0 ], cost: 1
    197: f34 -> f15 : B'=free_1335, C'=0, D'=1+G2, E'=free_1336, G'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1337>=1 && free_1338>=2 && free_1335>=1 && free_1336>=2 && 0>=1+F && Q>=0 && D>=0 && F>=1 && C==0 ], cost: 1
     84: f35 -> f34 : D'=1+D, E'=free_423, F'=free_421, G'=0, Q'=-1+Q, J'=free_422, M'=free_424, Q1'=free_420, M1'=C, N1'=free_425, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_423>=2 && 0>=1+free_426 && 0>=1+free_425 && 0>=1+free_421 && 0>=1+free_420 ], cost: 1
     85: f35 -> f34 : D'=1+D, E'=free_430, F'=free_428, G'=0, Q'=-1+Q, J'=free_429, M'=free_431, Q1'=free_427, M1'=C, N1'=free_432, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_430>=2 && 0>=1+free_433 && 0>=1+free_432 && 0>=1+free_428 && free_427>=1 ], cost: 1
     86: f35 -> f34 : D'=1+D, E'=free_437, F'=free_435, G'=0, Q'=-1+Q, J'=free_436, M'=free_438, Q1'=free_434, M1'=C, N1'=free_439, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_437>=2 && 0>=1+free_440 && 0>=1+free_439 && free_435>=1 && 0>=1+free_434 ], cost: 1
     87: f35 -> f34 : D'=1+D, E'=free_444, F'=free_442, G'=0, Q'=-1+Q, J'=free_443, M'=free_445, Q1'=free_441, M1'=C, N1'=free_446, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_444>=2 && 0>=1+free_447 && 0>=1+free_446 && free_442>=1 && free_441>=1 ], cost: 1
     88: f35 -> f34 : D'=1+D, E'=free_451, F'=free_449, G'=0, Q'=-1+Q, J'=free_450, M'=free_452, Q1'=free_448, M1'=C, N1'=free_453, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_451>=2 && 0>=1+free_454 && free_453>=1 && 0>=1+free_449 && 0>=1+free_448 ], cost: 1
     89: f35 -> f34 : D'=1+D, E'=free_458, F'=free_456, G'=0, Q'=-1+Q, J'=free_457, M'=free_459, Q1'=free_455, M1'=C, N1'=free_460, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_458>=2 && 0>=1+free_461 && free_460>=1 && 0>=1+free_456 && free_455>=1 ], cost: 1
     90: f35 -> f34 : D'=1+D, E'=free_465, F'=free_463, G'=0, Q'=-1+Q, J'=free_464, M'=free_466, Q1'=free_462, M1'=C, N1'=free_467, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_465>=2 && 0>=1+free_468 && free_467>=1 && free_463>=1 && 0>=1+free_462 ], cost: 1
     91: f35 -> f34 : D'=1+D, E'=free_472, F'=free_470, G'=0, Q'=-1+Q, J'=free_471, M'=free_473, Q1'=free_469, M1'=C, N1'=free_474, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_472>=2 && 0>=1+free_475 && free_474>=1 && free_470>=1 && free_469>=1 ], cost: 1
     92: f35 -> f34 : D'=1+D, E'=free_479, F'=free_477, G'=0, Q'=-1+Q, J'=free_478, M'=free_480, Q1'=free_476, M1'=C, N1'=free_481, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_479>=2 && free_482>=1 && 0>=1+free_481 && 0>=1+free_477 && 0>=1+free_476 ], cost: 1
     93: f35 -> f34 : D'=1+D, E'=free_486, F'=free_484, G'=0, Q'=-1+Q, J'=free_485, M'=free_487, Q1'=free_483, M1'=C, N1'=free_488, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_486>=2 && free_489>=1 && 0>=1+free_488 && 0>=1+free_484 && free_483>=1 ], cost: 1
     94: f35 -> f34 : D'=1+D, E'=free_493, F'=free_491, G'=0, Q'=-1+Q, J'=free_492, M'=free_494, Q1'=free_490, M1'=C, N1'=free_495, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_493>=2 && free_496>=1 && 0>=1+free_495 && free_491>=1 && 0>=1+free_490 ], cost: 1
     95: f35 -> f34 : D'=1+D, E'=free_500, F'=free_498, G'=0, Q'=-1+Q, J'=free_499, M'=free_501, Q1'=free_497, M1'=C, N1'=free_502, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_500>=2 && free_503>=1 && 0>=1+free_502 && free_498>=1 && free_497>=1 ], cost: 1
     96: f35 -> f34 : D'=1+D, E'=free_507, F'=free_505, G'=0, Q'=-1+Q, J'=free_506, M'=free_508, Q1'=free_504, M1'=C, N1'=free_509, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_507>=2 && free_510>=1 && free_509>=1 && 0>=1+free_505 && 0>=1+free_504 ], cost: 1
     97: f35 -> f34 : D'=1+D, E'=free_514, F'=free_512, G'=0, Q'=-1+Q, J'=free_513, M'=free_515, Q1'=free_511, M1'=C, N1'=free_516, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_514>=2 && free_517>=1 && free_516>=1 && 0>=1+free_512 && free_511>=1 ], cost: 1
     98: f35 -> f34 : D'=1+D, E'=free_521, F'=free_519, G'=0, Q'=-1+Q, J'=free_520, M'=free_522, Q1'=free_518, M1'=C, N1'=free_523, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_521>=2 && free_524>=1 && free_523>=1 && free_519>=1 && 0>=1+free_518 ], cost: 1
     99: f35 -> f34 : D'=1+D, E'=free_528, F'=free_526, G'=0, Q'=-1+Q, J'=free_527, M'=free_529, Q1'=free_525, M1'=C, N1'=free_530, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_528>=2 && free_531>=1 && free_530>=1 && free_526>=1 && free_525>=1 ], cost: 1
     68: f35 -> f35 : B'=-1+B, E'=free_343, F'=free_341, G'=free_342, M'=free_344, Q1'=free_340, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_343>=2 && 0>=1+C && 0>=1+free_342 && 0>=1+free_340 && 0>=1+free_341 ], cost: 1
     69: f35 -> f35 : B'=-1+B, E'=free_348, F'=free_346, G'=free_347, M'=free_349, Q1'=free_345, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_348>=2 && 0>=1+C && 0>=1+free_347 && 0>=1+free_345 && free_346>=1 ], cost: 1
     70: f35 -> f35 : B'=-1+B, E'=free_353, F'=free_351, G'=free_352, M'=free_354, Q1'=free_350, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_353>=2 && 0>=1+C && 0>=1+free_352 && free_350>=1 && 0>=1+free_351 ], cost: 1
     71: f35 -> f35 : B'=-1+B, E'=free_358, F'=free_356, G'=free_357, M'=free_359, Q1'=free_355, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_358>=2 && 0>=1+C && 0>=1+free_357 && free_355>=1 && free_356>=1 ], cost: 1
     72: f35 -> f35 : B'=-1+B, E'=free_363, F'=free_361, G'=free_362, M'=free_364, Q1'=free_360, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_363>=2 && 0>=1+C && free_362>=1 && 0>=1+free_360 && 0>=1+free_361 ], cost: 1
     73: f35 -> f35 : B'=-1+B, E'=free_368, F'=free_366, G'=free_367, M'=free_369, Q1'=free_365, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_368>=2 && 0>=1+C && free_367>=1 && 0>=1+free_365 && free_366>=1 ], cost: 1
     74: f35 -> f35 : B'=-1+B, E'=free_373, F'=free_371, G'=free_372, M'=free_374, Q1'=free_370, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_373>=2 && 0>=1+C && free_372>=1 && free_370>=1 && 0>=1+free_371 ], cost: 1
     75: f35 -> f35 : B'=-1+B, E'=free_378, F'=free_376, G'=free_377, M'=free_379, Q1'=free_375, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_378>=2 && 0>=1+C && free_377>=1 && free_375>=1 && free_376>=1 ], cost: 1
     76: f35 -> f35 : B'=-1+B, E'=free_383, F'=free_381, G'=free_382, M'=free_384, Q1'=free_380, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_383>=2 && C>=1 && 0>=1+free_382 && 0>=1+free_380 && 0>=1+free_381 ], cost: 1
     77: f35 -> f35 : B'=-1+B, E'=free_388, F'=free_386, G'=free_387, M'=free_389, Q1'=free_385, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_388>=2 && C>=1 && 0>=1+free_387 && 0>=1+free_385 && free_386>=1 ], cost: 1
     78: f35 -> f35 : B'=-1+B, E'=free_393, F'=free_391, G'=free_392, M'=free_394, Q1'=free_390, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_393>=2 && C>=1 && 0>=1+free_392 && free_390>=1 && 0>=1+free_391 ], cost: 1
     79: f35 -> f35 : B'=-1+B, E'=free_398, F'=free_396, G'=free_397, M'=free_399, Q1'=free_395, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_398>=2 && C>=1 && 0>=1+free_397 && free_395>=1 && free_396>=1 ], cost: 1
     80: f35 -> f35 : B'=-1+B, E'=free_403, F'=free_401, G'=free_402, M'=free_404, Q1'=free_400, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_403>=2 && C>=1 && free_402>=1 && 0>=1+free_400 && 0>=1+free_401 ], cost: 1
     81: f35 -> f35 : B'=-1+B, E'=free_408, F'=free_406, G'=free_407, M'=free_409, Q1'=free_405, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_408>=2 && C>=1 && free_407>=1 && 0>=1+free_405 && free_406>=1 ], cost: 1
     82: f35 -> f35 : B'=-1+B, E'=free_413, F'=free_411, G'=free_412, M'=free_414, Q1'=free_410, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_413>=2 && C>=1 && free_412>=1 && free_410>=1 && 0>=1+free_411 ], cost: 1
     83: f35 -> f35 : B'=-1+B, E'=free_418, F'=free_416, G'=free_417, M'=free_419, Q1'=free_415, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_418>=2 && C>=1 && free_417>=1 && free_415>=1 && free_416>=1 ], cost: 1
     48: f32 -> f32 : B'=-1+B, E'=1, F'=C, G'=free_249, M'=free_248, A1'=B, B1'=C1, [ B>=1 && 0>=1+free_250 && 0>=1+free_249 ], cost: 1
     49: f32 -> f32 : B'=-1+B, E'=1, F'=C, G'=free_252, M'=free_251, A1'=B, B1'=C1, [ B>=1 && 0>=1+free_253 && free_252>=1 ], cost: 1
     50: f32 -> f32 : B'=-1+B, E'=1, F'=C, G'=free_255, M'=free_254, A1'=B, B1'=C1, [ B>=1 && free_256>=1 && 0>=1+free_255 ], cost: 1
     51: f32 -> f32 : B'=-1+B, E'=1, F'=C, G'=free_258, M'=free_257, A1'=B, B1'=C1, [ B>=1 && free_259>=1 && free_258>=1 ], cost: 1
    101: f1 -> f29 : A'=free_535, C'=R1, E'=free_538, F'=R1, Q1_1'=free_537, R1'=free_540, S1'=free_536, T1'=free_541, W1'=free_534, X1'=free_539, Y1'=free_542, [ A>=Q1_1 && A>=0 && free_535>=free_538 && free_538>=2 ], cost: 1
    100: f1 -> f1 : A'=1+A, R1'=S1, S1'=free_533, T1'=S1, U1'=free_532, V1'=A, [ Q1_1>=1+A && A>=0 ], cost: 1
    148: f15 -> f15 : B'=free_1056, C'=0, E'=free_1057, F'=free_1055, G'=0, J'=free_1058, Z1'=0, B2'=free_1055, C2'=0, D2'=free_1055, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ free_1059>=1+A2 && G2>=0 && free_1057>=2 && free_1056>=1 && free_1055>=1+free_1059 && 0>=1+free_1055 && Z1==0 ], cost: 1
    149: f15 -> f15 : B'=free_1061, C'=0, E'=free_1062, F'=free_1060, G'=0, J'=free_1063, Z1'=0, B2'=free_1060, C2'=0, D2'=free_1060, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ free_1064>=1+A2 && G2>=0 && free_1062>=2 && free_1061>=1 && free_1060>=1+free_1064 && free_1060>=1 && Z1==0 ], cost: 1
    150: f15 -> f15 : B'=free_1066, C'=0, E'=free_1067, F'=free_1065, G'=0, J'=free_1068, Z1'=0, B2'=free_1065, C2'=0, D2'=free_1065, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ free_1069>=1+A2 && G2>=0 && free_1067>=2 && free_1066>=1 && free_1069>=1+free_1065 && 0>=1+free_1065 && Z1==0 ], cost: 1
    151: f15 -> f15 : B'=free_1071, C'=0, E'=free_1072, F'=free_1070, G'=0, J'=free_1073, Z1'=0, B2'=free_1070, C2'=0, D2'=free_1070, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ free_1074>=1+A2 && G2>=0 && free_1072>=2 && free_1071>=1 && free_1074>=1+free_1070 && free_1070>=1 && Z1==0 ], cost: 1
    152: f15 -> f15 : B'=free_1076, C'=0, E'=free_1077, F'=free_1075, G'=0, J'=free_1078, Z1'=0, B2'=free_1075, C2'=0, D2'=free_1075, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ A2>=1+free_1079 && G2>=0 && free_1077>=2 && free_1076>=1 && free_1075>=1+free_1079 && 0>=1+free_1075 && Z1==0 ], cost: 1
    153: f15 -> f15 : B'=free_1081, C'=0, E'=free_1082, F'=free_1080, G'=0, J'=free_1083, Z1'=0, B2'=free_1080, C2'=0, D2'=free_1080, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ A2>=1+free_1084 && G2>=0 && free_1082>=2 && free_1081>=1 && free_1080>=1+free_1084 && free_1080>=1 && Z1==0 ], cost: 1
    154: f15 -> f15 : B'=free_1086, C'=0, E'=free_1087, F'=free_1085, G'=0, J'=free_1088, Z1'=0, B2'=free_1085, C2'=0, D2'=free_1085, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ A2>=1+free_1089 && G2>=0 && free_1087>=2 && free_1086>=1 && free_1089>=1+free_1085 && 0>=1+free_1085 && Z1==0 ], cost: 1
    155: f15 -> f15 : B'=free_1091, C'=0, E'=free_1092, F'=free_1090, G'=0, J'=free_1093, Z1'=0, B2'=free_1090, C2'=0, D2'=free_1090, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ A2>=1+free_1094 && G2>=0 && free_1092>=2 && free_1091>=1 && free_1094>=1+free_1090 && free_1090>=1 && Z1==0 ], cost: 1
    170: f17 -> f17 : B'=free_1188, C'=free_1187, E'=free_1189, F'=free_1187, J'=free_1190, Z1'=0, B2'=free_1187, C2'=0, D2'=free_1187, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ free_1191>=1+A2 && J2>=0 && 0>=free_1188 && free_1189>=2 && free_1187>=1+free_1191 && 0>=1+free_1187 && Z1==0 ], cost: 1
    171: f17 -> f17 : B'=free_1193, C'=free_1192, E'=free_1194, F'=free_1192, J'=free_1195, Z1'=0, B2'=free_1192, C2'=0, D2'=free_1192, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ free_1196>=1+A2 && J2>=0 && 0>=free_1193 && free_1194>=2 && free_1192>=1+free_1196 && free_1192>=1 && Z1==0 ], cost: 1
    172: f17 -> f17 : B'=free_1198, C'=free_1197, E'=free_1199, F'=free_1197, J'=free_1200, Z1'=0, B2'=free_1197, C2'=0, D2'=free_1197, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ free_1201>=1+A2 && J2>=0 && 0>=free_1198 && free_1199>=2 && free_1201>=1+free_1197 && 0>=1+free_1197 && Z1==0 ], cost: 1
    173: f17 -> f17 : B'=free_1203, C'=free_1202, E'=free_1204, F'=free_1202, J'=free_1205, Z1'=0, B2'=free_1202, C2'=0, D2'=free_1202, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ free_1206>=1+A2 && J2>=0 && 0>=free_1203 && free_1204>=2 && free_1206>=1+free_1202 && free_1202>=1 && Z1==0 ], cost: 1
    174: f17 -> f17 : B'=free_1208, C'=free_1207, E'=free_1209, F'=free_1207, J'=free_1210, Z1'=0, B2'=free_1207, C2'=0, D2'=free_1207, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ A2>=1+free_1211 && J2>=0 && 0>=free_1208 && free_1209>=2 && free_1207>=1+free_1211 && 0>=1+free_1207 && Z1==0 ], cost: 1
    175: f17 -> f17 : B'=free_1213, C'=free_1212, E'=free_1214, F'=free_1212, J'=free_1215, Z1'=0, B2'=free_1212, C2'=0, D2'=free_1212, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ A2>=1+free_1216 && J2>=0 && 0>=free_1213 && free_1214>=2 && free_1212>=1+free_1216 && free_1212>=1 && Z1==0 ], cost: 1
    176: f17 -> f17 : B'=free_1218, C'=free_1217, E'=free_1219, F'=free_1217, J'=free_1220, Z1'=0, B2'=free_1217, C2'=0, D2'=free_1217, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ A2>=1+free_1221 && J2>=0 && 0>=free_1218 && free_1219>=2 && free_1221>=1+free_1217 && 0>=1+free_1217 && Z1==0 ], cost: 1
    177: f17 -> f17 : B'=free_1223, C'=free_1222, E'=free_1224, F'=free_1222, J'=free_1225, Z1'=0, B2'=free_1222, C2'=0, D2'=free_1222, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ A2>=1+free_1226 && J2>=0 && 0>=free_1223 && free_1224>=2 && free_1226>=1+free_1222 && free_1222>=1 && Z1==0 ], cost: 1
    199: f26 -> f32 : A'=free_1348, C'=S1, E'=1, F'=S1, M'=free_1345, Q1_1'=free_1347, R1'=free_1350, S1'=free_1346, T1'=free_1351, W1'=free_1344, X1'=free_1349, Y1'=free_1352, [], cost: 1
    198: f26 -> f1 : A'=2, E'=free_1342, M'=free_1340, Q1_1'=free_1342, R1'=free_1341, S1'=free_1343, T1'=free_1341, W1'=free_1341, M2'=free_1339, [ free_1342>=2 ], cost: 1
      7: [15] -> f29 : B'=-1+B, E'=free_38, F'=C, G'=free_36, M'=free_37, N'=B, O'=A, [ A>=free_38 && A>=0 && B>=1 && free_38>=2 && free_39>=1 && free_36>=1 ], cost: 1
      0: [15] -> f34 : D'=1, E'=free_3, F'=free_1, G'=0, H'=Q, J'=free_2, K'=1+Q, L'=free_4, M'=free, [ A>=0 && B>=1 && free_3>=2 && 0>=1+C && free_5>=free_3 && 0>=1+free_1 && D==1 ], cost: 1
      1: [15] -> f34 : D'=1, E'=free_9, F'=free_7, G'=0, H'=Q, J'=free_8, K'=1+Q, L'=free_10, M'=free_6, [ A>=0 && B>=1 && free_9>=2 && 0>=1+C && free_11>=free_9 && free_7>=1 && D==1 ], cost: 1
      2: [15] -> f34 : D'=1, E'=free_15, F'=free_13, G'=0, H'=Q, J'=free_14, K'=1+Q, L'=free_16, M'=free_12, [ A>=0 && B>=1 && free_15>=2 && C>=1 && free_17>=free_15 && 0>=1+free_13 && D==1 ], cost: 1
      3: [15] -> f34 : D'=1, E'=free_21, F'=free_19, G'=0, H'=Q, J'=free_20, K'=1+Q, L'=free_22, M'=free_18, [ A>=0 && B>=1 && free_21>=2 && C>=1 && free_23>=free_21 && free_19>=1 && D==1 ], cost: 1
    182: [15] -> f17 : B'=free_1267, C'=F, E'=free_1268, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1270>=free_1268 && 0>=free_1271 && free_1269>=2 && A>=free_1269 && 0>=free_1267 && A>=0 && free_1268>=2 && 0>=B && F>=1 && 0>=1+C && 0>=1+F ], cost: 1
    183: [15] -> f17 : B'=free_1272, C'=F, E'=free_1273, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1275>=free_1273 && 0>=free_1276 && free_1274>=2 && A>=free_1274 && 0>=free_1272 && A>=0 && free_1273>=2 && 0>=B && F>=1 && 0>=1+C ], cost: 1
    184: [15] -> f17 : B'=free_1277, C'=F, E'=free_1278, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1280>=free_1278 && 0>=free_1281 && free_1279>=2 && A>=free_1279 && 0>=free_1277 && A>=0 && free_1278>=2 && 0>=B && F>=1 && C>=1 && 0>=1+F ], cost: 1
    185: [15] -> f17 : B'=free_1282, C'=F, E'=free_1283, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1285>=free_1283 && 0>=free_1286 && free_1284>=2 && A>=free_1284 && 0>=free_1282 && A>=0 && free_1283>=2 && 0>=B && F>=1 && C>=1 ], cost: 1
    186: [15] -> f17 : B'=free_1287, C'=F, E'=free_1288, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1290>=free_1288 && 0>=free_1291 && free_1289>=2 && A>=free_1289 && 0>=free_1287 && A>=0 && free_1288>=2 && 0>=B && 0>=1+F && 0>=1+C ], cost: 1
    187: [15] -> f17 : B'=free_1292, C'=F, E'=free_1293, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1295>=free_1293 && 0>=free_1296 && free_1294>=2 && A>=free_1294 && 0>=free_1292 && A>=0 && free_1293>=2 && 0>=B && 0>=1+F && 0>=1+C && F>=1 ], cost: 1
    188: [15] -> f17 : B'=free_1297, C'=F, E'=free_1298, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1300>=free_1298 && 0>=free_1301 && free_1299>=2 && A>=free_1299 && 0>=free_1297 && A>=0 && free_1298>=2 && 0>=B && 0>=1+F && C>=1 ], cost: 1
    189: [15] -> f17 : B'=free_1302, C'=F, E'=free_1303, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1305>=free_1303 && 0>=free_1306 && free_1304>=2 && A>=free_1304 && 0>=free_1302 && A>=0 && free_1303>=2 && 0>=B && 0>=1+F && C>=1 && F>=1 ], cost: 1

Aborted due to lack of remaining time


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f26
    201: f29 -> [15] : B'=0, E'=free_26, F'=C, G'=free_24, M'=free_25, N'=1, O'=A, [ A>=free_26 && A>=0 && B>=1 && free_26>=2 && 0>=1+free_24 ], cost: B
    202: f29 -> [15] : B'=0, E'=free_30, F'=C, G'=free_28, M'=free_29, N'=1, O'=A, [ A>=free_30 && A>=0 && B>=1 && free_30>=2 && free_28>=1 ], cost: B
    203: f29 -> [15] : B'=0, E'=free_34, F'=C, G'=free_32, M'=free_33, N'=1, O'=A, [ A>=free_34 && A>=0 && B>=1 && free_34>=2 && 0>=1+free_32 ], cost: B
     60: f34 -> f34 : D'=1+D, E'=free_295, F'=free_293, G'=0, Q'=-1+Q, J'=free_294, M'=free_296, E1'=C, F1'=free_292, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_295>=2 && 0>=1+free_297 && 0>=1+free_293 && 0>=1+free_292 ], cost: 1
     61: f34 -> f34 : D'=1+D, E'=free_301, F'=free_299, G'=0, Q'=-1+Q, J'=free_300, M'=free_302, E1'=C, F1'=free_298, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_301>=2 && 0>=1+free_303 && 0>=1+free_299 && free_298>=1 ], cost: 1
     62: f34 -> f34 : D'=1+D, E'=free_307, F'=free_305, G'=0, Q'=-1+Q, J'=free_306, M'=free_308, E1'=C, F1'=free_304, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_307>=2 && 0>=1+free_309 && free_305>=1 && 0>=1+free_304 ], cost: 1
     63: f34 -> f34 : D'=1+D, E'=free_313, F'=free_311, G'=0, Q'=-1+Q, J'=free_312, M'=free_314, E1'=C, F1'=free_310, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_313>=2 && 0>=1+free_315 && free_311>=1 && free_310>=1 ], cost: 1
     64: f34 -> f34 : D'=1+D, E'=free_319, F'=free_317, G'=0, Q'=-1+Q, J'=free_318, M'=free_320, E1'=C, F1'=free_316, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_319>=2 && free_321>=1 && 0>=1+free_317 && 0>=1+free_316 ], cost: 1
     65: f34 -> f34 : D'=1+D, E'=free_325, F'=free_323, G'=0, Q'=-1+Q, J'=free_324, M'=free_326, E1'=C, F1'=free_322, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_325>=2 && free_327>=1 && 0>=1+free_323 && free_322>=1 ], cost: 1
     66: f34 -> f34 : D'=1+D, E'=free_331, F'=free_329, G'=0, Q'=-1+Q, J'=free_330, M'=free_332, E1'=C, F1'=free_328, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_331>=2 && free_333>=1 && free_329>=1 && 0>=1+free_328 ], cost: 1
     67: f34 -> f34 : D'=1+D, E'=free_337, F'=free_335, G'=0, Q'=-1+Q, J'=free_336, M'=free_338, E1'=C, F1'=free_334, G1'=1+D, H1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_337>=2 && free_339>=1 && free_335>=1 && free_334>=1 ], cost: 1
     52: f34 -> f35 : B'=-1+B, E'=free_262, F'=free_260, G'=free_261, M'=free_263, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_262>=2 && 0>=1+C && 0>=1+free_261 && 0>=1+free_260 ], cost: 1
     53: f34 -> f35 : B'=-1+B, E'=free_266, F'=free_264, G'=free_265, M'=free_267, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_266>=2 && 0>=1+C && 0>=1+free_265 && free_264>=1 ], cost: 1
     54: f34 -> f35 : B'=-1+B, E'=free_270, F'=free_268, G'=free_269, M'=free_271, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_270>=2 && 0>=1+C && free_269>=1 && 0>=1+free_268 ], cost: 1
     55: f34 -> f35 : B'=-1+B, E'=free_274, F'=free_272, G'=free_273, M'=free_275, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_274>=2 && 0>=1+C && free_273>=1 && free_272>=1 ], cost: 1
     56: f34 -> f35 : B'=-1+B, E'=free_278, F'=free_276, G'=free_277, M'=free_279, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_278>=2 && C>=1 && 0>=1+free_277 && 0>=1+free_276 ], cost: 1
     57: f34 -> f35 : B'=-1+B, E'=free_282, F'=free_280, G'=free_281, M'=free_283, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_282>=2 && C>=1 && 0>=1+free_281 && free_280>=1 ], cost: 1
     58: f34 -> f35 : B'=-1+B, E'=free_286, F'=free_284, G'=free_285, M'=free_287, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_286>=2 && C>=1 && free_285>=1 && 0>=1+free_284 ], cost: 1
     59: f34 -> f35 : B'=-1+B, E'=free_290, F'=free_288, G'=free_289, M'=free_291, D1'=B, [ D>=0 && B>=1 && Q>=0 && free_290>=2 && C>=1 && free_289>=1 && free_288>=1 ], cost: 1
    194: f34 -> f15 : B'=free_1323, C'=0, D'=1+G2, E'=free_1324, G'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1325>=1 && free_1326>=2 && free_1323>=1 && free_1324>=2 && F>=1 && Q>=0 && D>=0 && 0>=1+F && C==0 ], cost: 1
    195: f34 -> f15 : B'=free_1327, C'=0, D'=1+G2, E'=free_1328, G'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1329>=1 && free_1330>=2 && free_1327>=1 && free_1328>=2 && F>=1 && Q>=0 && D>=0 && C==0 ], cost: 1
    196: f34 -> f15 : B'=free_1331, C'=0, D'=1+G2, E'=free_1332, G'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1333>=1 && free_1334>=2 && free_1331>=1 && free_1332>=2 && 0>=1+F && Q>=0 && D>=0 && C==0 ], cost: 1
    197: f34 -> f15 : B'=free_1335, C'=0, D'=1+G2, E'=free_1336, G'=0, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, F2'=G2, [ free_1337>=1 && free_1338>=2 && free_1335>=1 && free_1336>=2 && 0>=1+F && Q>=0 && D>=0 && F>=1 && C==0 ], cost: 1
     84: f35 -> f34 : D'=1+D, E'=free_423, F'=free_421, G'=0, Q'=-1+Q, J'=free_422, M'=free_424, Q1'=free_420, M1'=C, N1'=free_425, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_423>=2 && 0>=1+free_426 && 0>=1+free_425 && 0>=1+free_421 && 0>=1+free_420 ], cost: 1
     85: f35 -> f34 : D'=1+D, E'=free_430, F'=free_428, G'=0, Q'=-1+Q, J'=free_429, M'=free_431, Q1'=free_427, M1'=C, N1'=free_432, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_430>=2 && 0>=1+free_433 && 0>=1+free_432 && 0>=1+free_428 && free_427>=1 ], cost: 1
     86: f35 -> f34 : D'=1+D, E'=free_437, F'=free_435, G'=0, Q'=-1+Q, J'=free_436, M'=free_438, Q1'=free_434, M1'=C, N1'=free_439, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_437>=2 && 0>=1+free_440 && 0>=1+free_439 && free_435>=1 && 0>=1+free_434 ], cost: 1
     87: f35 -> f34 : D'=1+D, E'=free_444, F'=free_442, G'=0, Q'=-1+Q, J'=free_443, M'=free_445, Q1'=free_441, M1'=C, N1'=free_446, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_444>=2 && 0>=1+free_447 && 0>=1+free_446 && free_442>=1 && free_441>=1 ], cost: 1
     88: f35 -> f34 : D'=1+D, E'=free_451, F'=free_449, G'=0, Q'=-1+Q, J'=free_450, M'=free_452, Q1'=free_448, M1'=C, N1'=free_453, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_451>=2 && 0>=1+free_454 && free_453>=1 && 0>=1+free_449 && 0>=1+free_448 ], cost: 1
     89: f35 -> f34 : D'=1+D, E'=free_458, F'=free_456, G'=0, Q'=-1+Q, J'=free_457, M'=free_459, Q1'=free_455, M1'=C, N1'=free_460, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_458>=2 && 0>=1+free_461 && free_460>=1 && 0>=1+free_456 && free_455>=1 ], cost: 1
     90: f35 -> f34 : D'=1+D, E'=free_465, F'=free_463, G'=0, Q'=-1+Q, J'=free_464, M'=free_466, Q1'=free_462, M1'=C, N1'=free_467, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_465>=2 && 0>=1+free_468 && free_467>=1 && free_463>=1 && 0>=1+free_462 ], cost: 1
     91: f35 -> f34 : D'=1+D, E'=free_472, F'=free_470, G'=0, Q'=-1+Q, J'=free_471, M'=free_473, Q1'=free_469, M1'=C, N1'=free_474, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_472>=2 && 0>=1+free_475 && free_474>=1 && free_470>=1 && free_469>=1 ], cost: 1
     92: f35 -> f34 : D'=1+D, E'=free_479, F'=free_477, G'=0, Q'=-1+Q, J'=free_478, M'=free_480, Q1'=free_476, M1'=C, N1'=free_481, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_479>=2 && free_482>=1 && 0>=1+free_481 && 0>=1+free_477 && 0>=1+free_476 ], cost: 1
     93: f35 -> f34 : D'=1+D, E'=free_486, F'=free_484, G'=0, Q'=-1+Q, J'=free_485, M'=free_487, Q1'=free_483, M1'=C, N1'=free_488, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_486>=2 && free_489>=1 && 0>=1+free_488 && 0>=1+free_484 && free_483>=1 ], cost: 1
     94: f35 -> f34 : D'=1+D, E'=free_493, F'=free_491, G'=0, Q'=-1+Q, J'=free_492, M'=free_494, Q1'=free_490, M1'=C, N1'=free_495, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_493>=2 && free_496>=1 && 0>=1+free_495 && free_491>=1 && 0>=1+free_490 ], cost: 1
     95: f35 -> f34 : D'=1+D, E'=free_500, F'=free_498, G'=0, Q'=-1+Q, J'=free_499, M'=free_501, Q1'=free_497, M1'=C, N1'=free_502, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_500>=2 && free_503>=1 && 0>=1+free_502 && free_498>=1 && free_497>=1 ], cost: 1
     96: f35 -> f34 : D'=1+D, E'=free_507, F'=free_505, G'=0, Q'=-1+Q, J'=free_506, M'=free_508, Q1'=free_504, M1'=C, N1'=free_509, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_507>=2 && free_510>=1 && free_509>=1 && 0>=1+free_505 && 0>=1+free_504 ], cost: 1
     97: f35 -> f34 : D'=1+D, E'=free_514, F'=free_512, G'=0, Q'=-1+Q, J'=free_513, M'=free_515, Q1'=free_511, M1'=C, N1'=free_516, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_514>=2 && free_517>=1 && free_516>=1 && 0>=1+free_512 && free_511>=1 ], cost: 1
     98: f35 -> f34 : D'=1+D, E'=free_521, F'=free_519, G'=0, Q'=-1+Q, J'=free_520, M'=free_522, Q1'=free_518, M1'=C, N1'=free_523, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_521>=2 && free_524>=1 && free_523>=1 && free_519>=1 && 0>=1+free_518 ], cost: 1
     99: f35 -> f34 : D'=1+D, E'=free_528, F'=free_526, G'=0, Q'=-1+Q, J'=free_527, M'=free_529, Q1'=free_525, M1'=C, N1'=free_530, O1'=1+D, P1'=-1+Q, [ D>=0 && B>=1 && Q>=0 && free_528>=2 && free_531>=1 && free_530>=1 && free_526>=1 && free_525>=1 ], cost: 1
     68: f35 -> f35 : B'=-1+B, E'=free_343, F'=free_341, G'=free_342, M'=free_344, Q1'=free_340, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_343>=2 && 0>=1+C && 0>=1+free_342 && 0>=1+free_340 && 0>=1+free_341 ], cost: 1
     69: f35 -> f35 : B'=-1+B, E'=free_348, F'=free_346, G'=free_347, M'=free_349, Q1'=free_345, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_348>=2 && 0>=1+C && 0>=1+free_347 && 0>=1+free_345 && free_346>=1 ], cost: 1
     70: f35 -> f35 : B'=-1+B, E'=free_353, F'=free_351, G'=free_352, M'=free_354, Q1'=free_350, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_353>=2 && 0>=1+C && 0>=1+free_352 && free_350>=1 && 0>=1+free_351 ], cost: 1
     71: f35 -> f35 : B'=-1+B, E'=free_358, F'=free_356, G'=free_357, M'=free_359, Q1'=free_355, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_358>=2 && 0>=1+C && 0>=1+free_357 && free_355>=1 && free_356>=1 ], cost: 1
     72: f35 -> f35 : B'=-1+B, E'=free_363, F'=free_361, G'=free_362, M'=free_364, Q1'=free_360, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_363>=2 && 0>=1+C && free_362>=1 && 0>=1+free_360 && 0>=1+free_361 ], cost: 1
     73: f35 -> f35 : B'=-1+B, E'=free_368, F'=free_366, G'=free_367, M'=free_369, Q1'=free_365, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_368>=2 && 0>=1+C && free_367>=1 && 0>=1+free_365 && free_366>=1 ], cost: 1
     74: f35 -> f35 : B'=-1+B, E'=free_373, F'=free_371, G'=free_372, M'=free_374, Q1'=free_370, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_373>=2 && 0>=1+C && free_372>=1 && free_370>=1 && 0>=1+free_371 ], cost: 1
     75: f35 -> f35 : B'=-1+B, E'=free_378, F'=free_376, G'=free_377, M'=free_379, Q1'=free_375, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_378>=2 && 0>=1+C && free_377>=1 && free_375>=1 && free_376>=1 ], cost: 1
     76: f35 -> f35 : B'=-1+B, E'=free_383, F'=free_381, G'=free_382, M'=free_384, Q1'=free_380, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_383>=2 && C>=1 && 0>=1+free_382 && 0>=1+free_380 && 0>=1+free_381 ], cost: 1
     77: f35 -> f35 : B'=-1+B, E'=free_388, F'=free_386, G'=free_387, M'=free_389, Q1'=free_385, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_388>=2 && C>=1 && 0>=1+free_387 && 0>=1+free_385 && free_386>=1 ], cost: 1
     78: f35 -> f35 : B'=-1+B, E'=free_393, F'=free_391, G'=free_392, M'=free_394, Q1'=free_390, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_393>=2 && C>=1 && 0>=1+free_392 && free_390>=1 && 0>=1+free_391 ], cost: 1
     79: f35 -> f35 : B'=-1+B, E'=free_398, F'=free_396, G'=free_397, M'=free_399, Q1'=free_395, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_398>=2 && C>=1 && 0>=1+free_397 && free_395>=1 && free_396>=1 ], cost: 1
     80: f35 -> f35 : B'=-1+B, E'=free_403, F'=free_401, G'=free_402, M'=free_404, Q1'=free_400, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_403>=2 && C>=1 && free_402>=1 && 0>=1+free_400 && 0>=1+free_401 ], cost: 1
     81: f35 -> f35 : B'=-1+B, E'=free_408, F'=free_406, G'=free_407, M'=free_409, Q1'=free_405, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_408>=2 && C>=1 && free_407>=1 && 0>=1+free_405 && free_406>=1 ], cost: 1
     82: f35 -> f35 : B'=-1+B, E'=free_413, F'=free_411, G'=free_412, M'=free_414, Q1'=free_410, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_413>=2 && C>=1 && free_412>=1 && free_410>=1 && 0>=1+free_411 ], cost: 1
     83: f35 -> f35 : B'=-1+B, E'=free_418, F'=free_416, G'=free_417, M'=free_419, Q1'=free_415, J1'=B, K1'=D, L1'=Q, [ D>=0 && B>=1 && Q>=0 && free_418>=2 && C>=1 && free_417>=1 && free_415>=1 && free_416>=1 ], cost: 1
     48: f32 -> f32 : B'=-1+B, E'=1, F'=C, G'=free_249, M'=free_248, A1'=B, B1'=C1, [ B>=1 && 0>=1+free_250 && 0>=1+free_249 ], cost: 1
     49: f32 -> f32 : B'=-1+B, E'=1, F'=C, G'=free_252, M'=free_251, A1'=B, B1'=C1, [ B>=1 && 0>=1+free_253 && free_252>=1 ], cost: 1
     50: f32 -> f32 : B'=-1+B, E'=1, F'=C, G'=free_255, M'=free_254, A1'=B, B1'=C1, [ B>=1 && free_256>=1 && 0>=1+free_255 ], cost: 1
     51: f32 -> f32 : B'=-1+B, E'=1, F'=C, G'=free_258, M'=free_257, A1'=B, B1'=C1, [ B>=1 && free_259>=1 && free_258>=1 ], cost: 1
    101: f1 -> f29 : A'=free_535, C'=R1, E'=free_538, F'=R1, Q1_1'=free_537, R1'=free_540, S1'=free_536, T1'=free_541, W1'=free_534, X1'=free_539, Y1'=free_542, [ A>=Q1_1 && A>=0 && free_535>=free_538 && free_538>=2 ], cost: 1
    100: f1 -> f1 : A'=1+A, R1'=S1, S1'=free_533, T1'=S1, U1'=free_532, V1'=A, [ Q1_1>=1+A && A>=0 ], cost: 1
    148: f15 -> f15 : B'=free_1056, C'=0, E'=free_1057, F'=free_1055, G'=0, J'=free_1058, Z1'=0, B2'=free_1055, C2'=0, D2'=free_1055, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ free_1059>=1+A2 && G2>=0 && free_1057>=2 && free_1056>=1 && free_1055>=1+free_1059 && 0>=1+free_1055 && Z1==0 ], cost: 1
    149: f15 -> f15 : B'=free_1061, C'=0, E'=free_1062, F'=free_1060, G'=0, J'=free_1063, Z1'=0, B2'=free_1060, C2'=0, D2'=free_1060, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ free_1064>=1+A2 && G2>=0 && free_1062>=2 && free_1061>=1 && free_1060>=1+free_1064 && free_1060>=1 && Z1==0 ], cost: 1
    150: f15 -> f15 : B'=free_1066, C'=0, E'=free_1067, F'=free_1065, G'=0, J'=free_1068, Z1'=0, B2'=free_1065, C2'=0, D2'=free_1065, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ free_1069>=1+A2 && G2>=0 && free_1067>=2 && free_1066>=1 && free_1069>=1+free_1065 && 0>=1+free_1065 && Z1==0 ], cost: 1
    151: f15 -> f15 : B'=free_1071, C'=0, E'=free_1072, F'=free_1070, G'=0, J'=free_1073, Z1'=0, B2'=free_1070, C2'=0, D2'=free_1070, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ free_1074>=1+A2 && G2>=0 && free_1072>=2 && free_1071>=1 && free_1074>=1+free_1070 && free_1070>=1 && Z1==0 ], cost: 1
    152: f15 -> f15 : B'=free_1076, C'=0, E'=free_1077, F'=free_1075, G'=0, J'=free_1078, Z1'=0, B2'=free_1075, C2'=0, D2'=free_1075, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ A2>=1+free_1079 && G2>=0 && free_1077>=2 && free_1076>=1 && free_1075>=1+free_1079 && 0>=1+free_1075 && Z1==0 ], cost: 1
    153: f15 -> f15 : B'=free_1081, C'=0, E'=free_1082, F'=free_1080, G'=0, J'=free_1083, Z1'=0, B2'=free_1080, C2'=0, D2'=free_1080, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ A2>=1+free_1084 && G2>=0 && free_1082>=2 && free_1081>=1 && free_1080>=1+free_1084 && free_1080>=1 && Z1==0 ], cost: 1
    154: f15 -> f15 : B'=free_1086, C'=0, E'=free_1087, F'=free_1085, G'=0, J'=free_1088, Z1'=0, B2'=free_1085, C2'=0, D2'=free_1085, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ A2>=1+free_1089 && G2>=0 && free_1087>=2 && free_1086>=1 && free_1089>=1+free_1085 && 0>=1+free_1085 && Z1==0 ], cost: 1
    155: f15 -> f15 : B'=free_1091, C'=0, E'=free_1092, F'=free_1090, G'=0, J'=free_1093, Z1'=0, B2'=free_1090, C2'=0, D2'=free_1090, E2'=A2, G2'=-1+G2, H2'=-1+G2, [ A2>=1+free_1094 && G2>=0 && free_1092>=2 && free_1091>=1 && free_1094>=1+free_1090 && free_1090>=1 && Z1==0 ], cost: 1
    170: f17 -> f17 : B'=free_1188, C'=free_1187, E'=free_1189, F'=free_1187, J'=free_1190, Z1'=0, B2'=free_1187, C2'=0, D2'=free_1187, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ free_1191>=1+A2 && J2>=0 && 0>=free_1188 && free_1189>=2 && free_1187>=1+free_1191 && 0>=1+free_1187 && Z1==0 ], cost: 1
    171: f17 -> f17 : B'=free_1193, C'=free_1192, E'=free_1194, F'=free_1192, J'=free_1195, Z1'=0, B2'=free_1192, C2'=0, D2'=free_1192, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ free_1196>=1+A2 && J2>=0 && 0>=free_1193 && free_1194>=2 && free_1192>=1+free_1196 && free_1192>=1 && Z1==0 ], cost: 1
    172: f17 -> f17 : B'=free_1198, C'=free_1197, E'=free_1199, F'=free_1197, J'=free_1200, Z1'=0, B2'=free_1197, C2'=0, D2'=free_1197, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ free_1201>=1+A2 && J2>=0 && 0>=free_1198 && free_1199>=2 && free_1201>=1+free_1197 && 0>=1+free_1197 && Z1==0 ], cost: 1
    173: f17 -> f17 : B'=free_1203, C'=free_1202, E'=free_1204, F'=free_1202, J'=free_1205, Z1'=0, B2'=free_1202, C2'=0, D2'=free_1202, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ free_1206>=1+A2 && J2>=0 && 0>=free_1203 && free_1204>=2 && free_1206>=1+free_1202 && free_1202>=1 && Z1==0 ], cost: 1
    174: f17 -> f17 : B'=free_1208, C'=free_1207, E'=free_1209, F'=free_1207, J'=free_1210, Z1'=0, B2'=free_1207, C2'=0, D2'=free_1207, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ A2>=1+free_1211 && J2>=0 && 0>=free_1208 && free_1209>=2 && free_1207>=1+free_1211 && 0>=1+free_1207 && Z1==0 ], cost: 1
    175: f17 -> f17 : B'=free_1213, C'=free_1212, E'=free_1214, F'=free_1212, J'=free_1215, Z1'=0, B2'=free_1212, C2'=0, D2'=free_1212, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ A2>=1+free_1216 && J2>=0 && 0>=free_1213 && free_1214>=2 && free_1212>=1+free_1216 && free_1212>=1 && Z1==0 ], cost: 1
    176: f17 -> f17 : B'=free_1218, C'=free_1217, E'=free_1219, F'=free_1217, J'=free_1220, Z1'=0, B2'=free_1217, C2'=0, D2'=free_1217, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ A2>=1+free_1221 && J2>=0 && 0>=free_1218 && free_1219>=2 && free_1221>=1+free_1217 && 0>=1+free_1217 && Z1==0 ], cost: 1
    177: f17 -> f17 : B'=free_1223, C'=free_1222, E'=free_1224, F'=free_1222, J'=free_1225, Z1'=0, B2'=free_1222, C2'=0, D2'=free_1222, E2'=A2, J2'=-1+J2, K2'=-1+J2, [ A2>=1+free_1226 && J2>=0 && 0>=free_1223 && free_1224>=2 && free_1226>=1+free_1222 && free_1222>=1 && Z1==0 ], cost: 1
    199: f26 -> f32 : A'=free_1348, C'=S1, E'=1, F'=S1, M'=free_1345, Q1_1'=free_1347, R1'=free_1350, S1'=free_1346, T1'=free_1351, W1'=free_1344, X1'=free_1349, Y1'=free_1352, [], cost: 1
    198: f26 -> f1 : A'=2, E'=free_1342, M'=free_1340, Q1_1'=free_1342, R1'=free_1341, S1'=free_1343, T1'=free_1341, W1'=free_1341, M2'=free_1339, [ free_1342>=2 ], cost: 1
      7: [15] -> f29 : B'=-1+B, E'=free_38, F'=C, G'=free_36, M'=free_37, N'=B, O'=A, [ A>=free_38 && A>=0 && B>=1 && free_38>=2 && free_39>=1 && free_36>=1 ], cost: 1
      0: [15] -> f34 : D'=1, E'=free_3, F'=free_1, G'=0, H'=Q, J'=free_2, K'=1+Q, L'=free_4, M'=free, [ A>=0 && B>=1 && free_3>=2 && 0>=1+C && free_5>=free_3 && 0>=1+free_1 && D==1 ], cost: 1
      1: [15] -> f34 : D'=1, E'=free_9, F'=free_7, G'=0, H'=Q, J'=free_8, K'=1+Q, L'=free_10, M'=free_6, [ A>=0 && B>=1 && free_9>=2 && 0>=1+C && free_11>=free_9 && free_7>=1 && D==1 ], cost: 1
      2: [15] -> f34 : D'=1, E'=free_15, F'=free_13, G'=0, H'=Q, J'=free_14, K'=1+Q, L'=free_16, M'=free_12, [ A>=0 && B>=1 && free_15>=2 && C>=1 && free_17>=free_15 && 0>=1+free_13 && D==1 ], cost: 1
      3: [15] -> f34 : D'=1, E'=free_21, F'=free_19, G'=0, H'=Q, J'=free_20, K'=1+Q, L'=free_22, M'=free_18, [ A>=0 && B>=1 && free_21>=2 && C>=1 && free_23>=free_21 && free_19>=1 && D==1 ], cost: 1
    182: [15] -> f17 : B'=free_1267, C'=F, E'=free_1268, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1270>=free_1268 && 0>=free_1271 && free_1269>=2 && A>=free_1269 && 0>=free_1267 && A>=0 && free_1268>=2 && 0>=B && F>=1 && 0>=1+C && 0>=1+F ], cost: 1
    183: [15] -> f17 : B'=free_1272, C'=F, E'=free_1273, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1275>=free_1273 && 0>=free_1276 && free_1274>=2 && A>=free_1274 && 0>=free_1272 && A>=0 && free_1273>=2 && 0>=B && F>=1 && 0>=1+C ], cost: 1
    184: [15] -> f17 : B'=free_1277, C'=F, E'=free_1278, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1280>=free_1278 && 0>=free_1281 && free_1279>=2 && A>=free_1279 && 0>=free_1277 && A>=0 && free_1278>=2 && 0>=B && F>=1 && C>=1 && 0>=1+F ], cost: 1
    185: [15] -> f17 : B'=free_1282, C'=F, E'=free_1283, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1285>=free_1283 && 0>=free_1286 && free_1284>=2 && A>=free_1284 && 0>=free_1282 && A>=0 && free_1283>=2 && 0>=B && F>=1 && C>=1 ], cost: 1
    186: [15] -> f17 : B'=free_1287, C'=F, E'=free_1288, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1290>=free_1288 && 0>=free_1291 && free_1289>=2 && A>=free_1289 && 0>=free_1287 && A>=0 && free_1288>=2 && 0>=B && 0>=1+F && 0>=1+C ], cost: 1
    187: [15] -> f17 : B'=free_1292, C'=F, E'=free_1293, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1295>=free_1293 && 0>=free_1296 && free_1294>=2 && A>=free_1294 && 0>=free_1292 && A>=0 && free_1293>=2 && 0>=B && 0>=1+F && 0>=1+C && F>=1 ], cost: 1
    188: [15] -> f17 : B'=free_1297, C'=F, E'=free_1298, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1300>=free_1298 && 0>=free_1301 && free_1299>=2 && A>=free_1299 && 0>=free_1297 && A>=0 && free_1298>=2 && 0>=B && 0>=1+F && C>=1 ], cost: 1
    189: [15] -> f17 : B'=free_1302, C'=F, E'=free_1303, Z1'=0, A2'=F, B2'=F, C2'=0, D2'=F, E2'=F, Q2'=J2, L2'=1+J2, [ free_1305>=free_1303 && 0>=free_1306 && free_1304>=2 && A>=free_1304 && 0>=free_1302 && A>=0 && free_1303>=2 && 0>=B && 0>=1+F && C>=1 && F>=1 ], cost: 1

This is only a partial result (probably due to a timeout), trying to find max complexity

Removed transitions with const cost
  Start location: f26
    201: f29 -> [15] : B'=0, E'=free_26, F'=C, G'=free_24, M'=free_25, N'=1, O'=A, [ A>=free_26 && A>=0 && B>=1 && free_26>=2 && 0>=1+free_24 ], cost: B
    202: f29 -> [15] : B'=0, E'=free_30, F'=C, G'=free_28, M'=free_29, N'=1, O'=A, [ A>=free_30 && A>=0 && B>=1 && free_30>=2 && free_28>=1 ], cost: B
    203: f29 -> [15] : B'=0, E'=free_34, F'=C, G'=free_32, M'=free_33, N'=1, O'=A, [ A>=free_34 && A>=0 && B>=1 && free_34>=2 && 0>=1+free_32 ], cost: B
    101: f1 -> f29 : A'=free_535, C'=R1, E'=free_538, F'=R1, Q1_1'=free_537, R1'=free_540, S1'=free_536, T1'=free_541, W1'=free_534, X1'=free_539, Y1'=free_542, [ A>=Q1_1 && A>=0 && free_535>=free_538 && free_538>=2 ], cost: 1
    198: f26 -> f1 : A'=2, E'=free_1342, M'=free_1340, Q1_1'=free_1342, R1'=free_1341, S1'=free_1343, T1'=free_1341, W1'=free_1341, M2'=free_1339, [ free_1342>=2 ], cost: 1

Performed chaining from the start location:
  Start location: f26
    201: f29 -> [15] : B'=0, E'=free_26, F'=C, G'=free_24, M'=free_25, N'=1, O'=A, [ A>=free_26 && A>=0 && B>=1 && free_26>=2 && 0>=1+free_24 ], cost: B
    202: f29 -> [15] : B'=0, E'=free_30, F'=C, G'=free_28, M'=free_29, N'=1, O'=A, [ A>=free_30 && A>=0 && B>=1 && free_30>=2 && free_28>=1 ], cost: B
    203: f29 -> [15] : B'=0, E'=free_34, F'=C, G'=free_32, M'=free_33, N'=1, O'=A, [ A>=free_34 && A>=0 && B>=1 && free_34>=2 && 0>=1+free_32 ], cost: B
    204: f26 -> f29 : A'=free_535, C'=free_1341, E'=free_538, F'=free_1341, M'=free_1340, Q1_1'=free_537, R1'=free_540, S1'=free_536, T1'=free_541, W1'=free_534, X1'=free_539, Y1'=free_542, M2'=free_1339, [ free_1342>=2 && 2>=free_1342 && 2>=0 && free_535>=free_538 && free_538>=2 ], cost: 2

Performed chaining from the start location:
  Start location: f26
    205: f26 -> [15] : A'=free_535, B'=0, C'=free_1341, E'=free_26, F'=free_1341, G'=free_24, M'=free_25, N'=1, O'=free_535, Q1_1'=free_537, R1'=free_540, S1'=free_536, T1'=free_541, W1'=free_534, X1'=free_539, Y1'=free_542, M2'=free_1339, [ free_1342>=2 && 2>=free_1342 && 2>=0 && free_535>=free_538 && free_538>=2 && free_535>=free_26 && free_535>=0 && B>=1 && free_26>=2 && 0>=1+free_24 ], cost: 2+B
    206: f26 -> [15] : A'=free_535, B'=0, C'=free_1341, E'=free_30, F'=free_1341, G'=free_28, M'=free_29, N'=1, O'=free_535, Q1_1'=free_537, R1'=free_540, S1'=free_536, T1'=free_541, W1'=free_534, X1'=free_539, Y1'=free_542, M2'=free_1339, [ free_1342>=2 && 2>=free_1342 && 2>=0 && free_535>=free_538 && free_538>=2 && free_535>=free_30 && free_535>=0 && B>=1 && free_30>=2 && free_28>=1 ], cost: 2+B
    207: f26 -> [15] : A'=free_535, B'=0, C'=free_1341, E'=free_34, F'=free_1341, G'=free_32, M'=free_33, N'=1, O'=free_535, Q1_1'=free_537, R1'=free_540, S1'=free_536, T1'=free_541, W1'=free_534, X1'=free_539, Y1'=free_542, M2'=free_1339, [ free_1342>=2 && 2>=free_1342 && 2>=0 && free_535>=free_538 && free_538>=2 && free_535>=free_34 && free_535>=0 && B>=1 && free_34>=2 && 0>=1+free_32 ], cost: 2+B

  Found configuration with infinitely models for cost: 2+B
  and guard: free_1342>=2 && 2>=free_1342 && 2>=0 && free_535>=free_538 && free_538>=2 && free_535>=free_26 && free_535>=0 && B>=1 && free_26>=2 && 0>=1+free_24:
  free_535: Pos, B: Pos, free_538: Pos, free_1342: Const, free_26: Pos, free_24: Neg, where: free_535 > free_538 free_535 > free_26

Found new complexity n^1, because: Found infinity configuration.

Performed chaining from the start location:
  Start location: f26
    <empty>


The final runtime is determined by this resulting transition:
  Final Guard: free_1342>=2 && 2>=free_1342 && 2>=0 && free_535>=free_538 && free_538>=2 && free_535>=free_26 && free_535>=0 && B>=1 && free_26>=2 && 0>=1+free_24
  Final Cost:  2+B

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

WORST_CASE(Omega(n^1),?)