Trying to load file: main.koat Initial Control flow graph problem: Start location: f3 0: f1 -> f1 : B'=1+B, C'=D, D'=free_1, E'=D, F'=free, G'=B, H'=Q, [ A>=1+B && B>=0 ], cost: 1 53: f1 -> f7 : A'=free_418, B'=free_416, C'=free_412, D'=free_410, E'=free_417, K'=J, L'=E1, M'=0, N'=free_411, P'=O, Q_1'=free_414, R'=J, S'=free_414, C1'=J, F1'=free_420, S1'=free_408, T1'=free_415, U1'=free_413, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_419, A2'=free_409, [ free_421>=2 && W1>=free_421 && free_411>=2 && W1>=free_411 && O>=1+K && B>=A && B>=0 && W1>=0 && M==0 && J==K ], cost: 1 54: f1 -> f7 : A'=free_432, B'=free_430, C'=free_426, D'=free_424, E'=free_431, K'=J, L'=E1, M'=0, N'=free_425, P'=O, Q_1'=free_428, R'=J, S'=free_428, C1'=J, F1'=free_434, S1'=free_422, T1'=free_429, U1'=free_427, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_433, A2'=free_423, [ free_435>=2 && W1>=free_435 && free_425>=2 && W1>=free_425 && K>=1+O && B>=A && B>=0 && W1>=0 && M==0 && J==K ], cost: 1 55: f1 -> f4 : A'=free_448, B'=free_445, C'=free_440, D'=free_443, E'=free_438, J'=free_444, N'=free_439, P'=free_437, Q_1'=free_449, R'=free_442, C1'=free_447, F1'=free_441, S1'=free_436, T1'=free_450, U1'=free_446, [ free_451>=2 && W1>=free_451 && free_439>=2 && W1>=free_439 && B>=A && W1>=0 && B>=0 && O==J ], cost: 1 1: f5 -> f7 : L'=1+E1, M'=1, N'=free_7, O'=P, Q_1'=free_2, R'=J, S'=free_2, T'=free_4, U'=V, W'=Q, X'=K, Y'=free_6, Z'=free_3, A1'=free_5, B1'=free_8, C1'=J, D1'=E1, [ free_9>=1+free_10 && free_9>=1+J && free_9>=1+K && free_9>=1+free_8 && L>=0 && free_7>=2 && M==1 ], cost: 1 2: f5 -> f7 : L'=1+E1, M'=1, N'=free_16, O'=P, Q_1'=free_11, R'=J, S'=free_11, T'=free_13, U'=V, W'=Q, X'=K, Y'=free_15, Z'=free_12, A1'=free_14, B1'=free_17, C1'=J, D1'=E1, [ free_18>=1+free_19 && free_18>=1+J && free_18>=1+K && free_17>=1+free_18 && L>=0 && free_16>=2 && M==1 ], cost: 1 3: f5 -> f7 : L'=1+E1, M'=1, N'=free_25, O'=P, Q_1'=free_20, R'=J, S'=free_20, T'=free_22, U'=V, W'=Q, X'=K, Y'=free_24, Z'=free_21, A1'=free_23, B1'=free_26, C1'=J, D1'=E1, [ free_27>=1+free_28 && free_27>=1+J && K>=1+free_27 && free_27>=1+free_26 && L>=0 && free_25>=2 && M==1 ], cost: 1 4: f5 -> f7 : L'=1+E1, M'=1, N'=free_34, O'=P, Q_1'=free_29, R'=J, S'=free_29, T'=free_31, U'=V, W'=Q, X'=K, Y'=free_33, Z'=free_30, A1'=free_32, B1'=free_35, C1'=J, D1'=E1, [ free_36>=1+free_37 && free_36>=1+J && K>=1+free_36 && free_35>=1+free_36 && L>=0 && free_34>=2 && M==1 ], cost: 1 5: f5 -> f7 : L'=1+E1, M'=1, N'=free_43, O'=P, Q_1'=free_38, R'=J, S'=free_38, T'=free_40, U'=V, W'=Q, X'=K, Y'=free_42, Z'=free_39, A1'=free_41, B1'=free_44, C1'=J, D1'=E1, [ free_45>=1+free_46 && J>=1+free_45 && free_45>=1+K && free_45>=1+free_44 && L>=0 && free_43>=2 && M==1 ], cost: 1 6: f5 -> f7 : L'=1+E1, M'=1, N'=free_52, O'=P, Q_1'=free_47, R'=J, S'=free_47, T'=free_49, U'=V, W'=Q, X'=K, Y'=free_51, Z'=free_48, A1'=free_50, B1'=free_53, C1'=J, D1'=E1, [ free_54>=1+free_55 && J>=1+free_54 && free_54>=1+K && free_53>=1+free_54 && L>=0 && free_52>=2 && M==1 ], cost: 1 7: f5 -> f7 : L'=1+E1, M'=1, N'=free_61, O'=P, Q_1'=free_56, R'=J, S'=free_56, T'=free_58, U'=V, W'=Q, X'=K, Y'=free_60, Z'=free_57, A1'=free_59, B1'=free_62, C1'=J, D1'=E1, [ free_63>=1+free_64 && J>=1+free_63 && K>=1+free_63 && free_63>=1+free_62 && L>=0 && free_61>=2 && M==1 ], cost: 1 8: f5 -> f7 : L'=1+E1, M'=1, N'=free_70, O'=P, Q_1'=free_65, R'=J, S'=free_65, T'=free_67, U'=V, W'=Q, X'=K, Y'=free_69, Z'=free_66, A1'=free_68, B1'=free_71, C1'=J, D1'=E1, [ free_72>=1+free_73 && J>=1+free_72 && K>=1+free_72 && free_71>=1+free_72 && L>=0 && free_70>=2 && M==1 ], cost: 1 9: f5 -> f7 : L'=1+E1, M'=1, N'=free_79, O'=P, Q_1'=free_74, R'=J, S'=free_74, T'=free_76, U'=V, W'=Q, X'=K, Y'=free_78, Z'=free_75, A1'=free_77, B1'=free_80, C1'=J, D1'=E1, [ free_82>=1+free_81 && free_81>=1+J && free_81>=1+K && free_81>=1+free_80 && L>=0 && free_79>=2 && M==1 ], cost: 1 10: f5 -> f7 : L'=1+E1, M'=1, N'=free_88, O'=P, Q_1'=free_83, R'=J, S'=free_83, T'=free_85, U'=V, W'=Q, X'=K, Y'=free_87, Z'=free_84, A1'=free_86, B1'=free_89, C1'=J, D1'=E1, [ free_91>=1+free_90 && free_90>=1+J && free_90>=1+K && free_89>=1+free_90 && L>=0 && free_88>=2 && M==1 ], cost: 1 11: f5 -> f7 : L'=1+E1, M'=1, N'=free_97, O'=P, Q_1'=free_92, R'=J, S'=free_92, T'=free_94, U'=V, W'=Q, X'=K, Y'=free_96, Z'=free_93, A1'=free_95, B1'=free_98, C1'=J, D1'=E1, [ free_100>=1+free_99 && free_99>=1+J && K>=1+free_99 && free_99>=1+free_98 && L>=0 && free_97>=2 && M==1 ], cost: 1 12: f5 -> f7 : L'=1+E1, M'=1, N'=free_106, O'=P, Q_1'=free_101, R'=J, S'=free_101, T'=free_103, U'=V, W'=Q, X'=K, Y'=free_105, Z'=free_102, A1'=free_104, B1'=free_107, C1'=J, D1'=E1, [ free_109>=1+free_108 && free_108>=1+J && K>=1+free_108 && free_107>=1+free_108 && L>=0 && free_106>=2 && M==1 ], cost: 1 13: f5 -> f7 : L'=1+E1, M'=1, N'=free_115, O'=P, Q_1'=free_110, R'=J, S'=free_110, T'=free_112, U'=V, W'=Q, X'=K, Y'=free_114, Z'=free_111, A1'=free_113, B1'=free_116, C1'=J, D1'=E1, [ free_118>=1+free_117 && J>=1+free_117 && free_117>=1+K && free_117>=1+free_116 && L>=0 && free_115>=2 && M==1 ], cost: 1 14: f5 -> f7 : L'=1+E1, M'=1, N'=free_124, O'=P, Q_1'=free_119, R'=J, S'=free_119, T'=free_121, U'=V, W'=Q, X'=K, Y'=free_123, Z'=free_120, A1'=free_122, B1'=free_125, C1'=J, D1'=E1, [ free_127>=1+free_126 && J>=1+free_126 && free_126>=1+K && free_125>=1+free_126 && L>=0 && free_124>=2 && M==1 ], cost: 1 15: f5 -> f7 : L'=1+E1, M'=1, N'=free_133, O'=P, Q_1'=free_128, R'=J, S'=free_128, T'=free_130, U'=V, W'=Q, X'=K, Y'=free_132, Z'=free_129, A1'=free_131, B1'=free_134, C1'=J, D1'=E1, [ free_136>=1+free_135 && J>=1+free_135 && K>=1+free_135 && free_135>=1+free_134 && L>=0 && free_133>=2 && M==1 ], cost: 1 16: f5 -> f7 : L'=1+E1, M'=1, N'=free_142, O'=P, Q_1'=free_137, R'=J, S'=free_137, T'=free_139, U'=V, W'=Q, X'=K, Y'=free_141, Z'=free_138, A1'=free_140, B1'=free_143, C1'=J, D1'=E1, [ free_145>=1+free_144 && J>=1+free_144 && K>=1+free_144 && free_143>=1+free_144 && L>=0 && free_142>=2 && M==1 ], cost: 1 17: f5 -> f4 : J'=free_148, N'=free_153, O'=free_146, P'=free_150, Q_1'=free_147, R'=free_154, C1'=free_149, F1'=free_151, G1'=free_152, [ L>=0 && free_146>=1+free_152 && free_153>=2 && J==P ], cost: 1 18: f5 -> f4 : J'=free_157, N'=free_162, O'=free_155, P'=free_159, Q_1'=free_156, R'=free_163, C1'=free_158, F1'=free_160, G1'=free_161, [ L>=0 && free_161>=1+free_155 && free_162>=2 && J==P ], cost: 1 31: f7 -> f7 : M'=1+M, N'=free_243, O'=P, Q_1'=free_240, R'=J, S'=free_240, C1'=J, E1'=-1+E1, K1'=free_241, L1'=free_242, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_244>=1+free_245 && free_244>=1+J && free_244>=1+free_242 && free_244>=1+K && free_246>=0 && free_243>=2 && E1>=0 ], cost: 1 32: f7 -> f7 : M'=1+M, N'=free_250, O'=P, Q_1'=free_247, R'=J, S'=free_247, C1'=J, E1'=-1+E1, K1'=free_248, L1'=free_249, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_251>=1+free_252 && free_251>=1+J && free_251>=1+free_249 && K>=1+free_251 && free_253>=0 && free_250>=2 && E1>=0 ], cost: 1 33: f7 -> f7 : M'=1+M, N'=free_257, O'=P, Q_1'=free_254, R'=J, S'=free_254, C1'=J, E1'=-1+E1, K1'=free_255, L1'=free_256, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_258>=1+free_259 && free_258>=1+J && free_256>=1+free_258 && free_258>=1+K && free_260>=0 && free_257>=2 && E1>=0 ], cost: 1 34: f7 -> f7 : M'=1+M, N'=free_264, O'=P, Q_1'=free_261, R'=J, S'=free_261, C1'=J, E1'=-1+E1, K1'=free_262, L1'=free_263, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_265>=1+free_266 && free_265>=1+J && free_263>=1+free_265 && K>=1+free_265 && free_267>=0 && free_264>=2 && E1>=0 ], cost: 1 35: f7 -> f7 : M'=1+M, N'=free_271, O'=P, Q_1'=free_268, R'=J, S'=free_268, C1'=J, E1'=-1+E1, K1'=free_269, L1'=free_270, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_272>=1+free_273 && J>=1+free_272 && free_272>=1+free_270 && free_272>=1+K && free_274>=0 && free_271>=2 && E1>=0 ], cost: 1 36: f7 -> f7 : M'=1+M, N'=free_278, O'=P, Q_1'=free_275, R'=J, S'=free_275, C1'=J, E1'=-1+E1, K1'=free_276, L1'=free_277, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_279>=1+free_280 && J>=1+free_279 && free_279>=1+free_277 && K>=1+free_279 && free_281>=0 && free_278>=2 && E1>=0 ], cost: 1 37: f7 -> f7 : M'=1+M, N'=free_285, O'=P, Q_1'=free_282, R'=J, S'=free_282, C1'=J, E1'=-1+E1, K1'=free_283, L1'=free_284, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_286>=1+free_287 && J>=1+free_286 && free_284>=1+free_286 && free_286>=1+K && free_288>=0 && free_285>=2 && E1>=0 ], cost: 1 38: f7 -> f7 : M'=1+M, N'=free_292, O'=P, Q_1'=free_289, R'=J, S'=free_289, C1'=J, E1'=-1+E1, K1'=free_290, L1'=free_291, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_293>=1+free_294 && J>=1+free_293 && free_291>=1+free_293 && K>=1+free_293 && free_295>=0 && free_292>=2 && E1>=0 ], cost: 1 39: f7 -> f7 : M'=1+M, N'=free_299, O'=P, Q_1'=free_296, R'=J, S'=free_296, C1'=J, E1'=-1+E1, K1'=free_297, L1'=free_298, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_301>=1+free_300 && free_300>=1+J && free_300>=1+free_298 && free_300>=1+K && free_302>=0 && free_299>=2 && E1>=0 ], cost: 1 40: f7 -> f7 : M'=1+M, N'=free_306, O'=P, Q_1'=free_303, R'=J, S'=free_303, C1'=J, E1'=-1+E1, K1'=free_304, L1'=free_305, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_308>=1+free_307 && free_307>=1+J && free_307>=1+free_305 && K>=1+free_307 && free_309>=0 && free_306>=2 && E1>=0 ], cost: 1 41: f7 -> f7 : M'=1+M, N'=free_313, O'=P, Q_1'=free_310, R'=J, S'=free_310, C1'=J, E1'=-1+E1, K1'=free_311, L1'=free_312, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_315>=1+free_314 && free_314>=1+J && free_312>=1+free_314 && free_314>=1+K && free_316>=0 && free_313>=2 && E1>=0 ], cost: 1 42: f7 -> f7 : M'=1+M, N'=free_320, O'=P, Q_1'=free_317, R'=J, S'=free_317, C1'=J, E1'=-1+E1, K1'=free_318, L1'=free_319, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_322>=1+free_321 && free_321>=1+J && free_319>=1+free_321 && K>=1+free_321 && free_323>=0 && free_320>=2 && E1>=0 ], cost: 1 43: f7 -> f7 : M'=1+M, N'=free_327, O'=P, Q_1'=free_324, R'=J, S'=free_324, C1'=J, E1'=-1+E1, K1'=free_325, L1'=free_326, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_329>=1+free_328 && J>=1+free_328 && free_328>=1+free_326 && free_328>=1+K && free_330>=0 && free_327>=2 && E1>=0 ], cost: 1 44: f7 -> f7 : M'=1+M, N'=free_334, O'=P, Q_1'=free_331, R'=J, S'=free_331, C1'=J, E1'=-1+E1, K1'=free_332, L1'=free_333, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_336>=1+free_335 && J>=1+free_335 && free_335>=1+free_333 && K>=1+free_335 && free_337>=0 && free_334>=2 && E1>=0 ], cost: 1 45: f7 -> f7 : M'=1+M, N'=free_341, O'=P, Q_1'=free_338, R'=J, S'=free_338, C1'=J, E1'=-1+E1, K1'=free_339, L1'=free_340, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_343>=1+free_342 && J>=1+free_342 && free_340>=1+free_342 && free_342>=1+K && free_344>=0 && free_341>=2 && E1>=0 ], cost: 1 46: f7 -> f7 : M'=1+M, N'=free_348, O'=P, Q_1'=free_345, R'=J, S'=free_345, C1'=J, E1'=-1+E1, K1'=free_346, L1'=free_347, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_350>=1+free_349 && J>=1+free_349 && free_347>=1+free_349 && K>=1+free_349 && free_351>=0 && free_348>=2 && E1>=0 ], cost: 1 47: f7 -> f4 : J'=free_354, N'=free_359, O'=free_352, P'=free_356, Q_1'=free_353, R'=free_360, C1'=free_355, F1'=free_357, R1'=free_358, [ M>=0 && E1>=0 && free_359>=2 && free_352>=1+free_358 && free_352>=1+K && J==P ], cost: 1 48: f7 -> f4 : J'=free_363, N'=free_368, O'=free_361, P'=free_365, Q_1'=free_362, R'=free_369, C1'=free_364, F1'=free_366, R1'=free_367, [ M>=0 && E1>=0 && free_368>=2 && free_361>=1+free_367 && K>=1+free_361 && J==P ], cost: 1 49: f7 -> f4 : J'=free_372, N'=free_377, O'=free_370, P'=free_374, Q_1'=free_371, R'=free_378, C1'=free_373, F1'=free_375, R1'=free_376, [ M>=0 && E1>=0 && free_377>=2 && free_376>=1+free_370 && free_370>=1+K && J==P ], cost: 1 50: f7 -> f4 : J'=free_381, N'=free_386, O'=free_379, P'=free_383, Q_1'=free_380, R'=free_387, C1'=free_382, F1'=free_384, R1'=free_385, [ M>=0 && E1>=0 && free_386>=2 && free_385>=1+free_379 && K>=1+free_379 && J==P ], cost: 1 19: f6 -> f7 : N'=free_167, O'=P, Q_1'=free_164, R'=J, S'=free_164, C1'=J, H1'=free_165, Q1'=free_166, [ free_168>=1+K && free_168>=1+J && free_168>=1+free_166 && free_167>=2 && D1>=0 ], cost: 1 20: f6 -> f7 : N'=free_172, O'=P, Q_1'=free_169, R'=J, S'=free_169, C1'=J, H1'=free_170, Q1'=free_171, [ free_173>=1+K && free_173>=1+J && free_171>=1+free_173 && free_172>=2 && D1>=0 ], cost: 1 21: f6 -> f7 : N'=free_177, O'=P, Q_1'=free_174, R'=J, S'=free_174, C1'=J, H1'=free_175, Q1'=free_176, [ free_178>=1+K && J>=1+free_178 && free_178>=1+free_176 && free_177>=2 && D1>=0 ], cost: 1 22: f6 -> f7 : N'=free_182, O'=P, Q_1'=free_179, R'=J, S'=free_179, C1'=J, H1'=free_180, Q1'=free_181, [ free_183>=1+K && J>=1+free_183 && free_181>=1+free_183 && free_182>=2 && D1>=0 ], cost: 1 23: f6 -> f7 : N'=free_187, O'=P, Q_1'=free_184, R'=J, S'=free_184, C1'=J, H1'=free_185, Q1'=free_186, [ K>=1+free_188 && free_188>=1+J && free_188>=1+free_186 && free_187>=2 && D1>=0 ], cost: 1 24: f6 -> f7 : N'=free_192, O'=P, Q_1'=free_189, R'=J, S'=free_189, C1'=J, H1'=free_190, Q1'=free_191, [ K>=1+free_193 && free_193>=1+J && free_191>=1+free_193 && free_192>=2 && D1>=0 ], cost: 1 25: f6 -> f7 : N'=free_197, O'=P, Q_1'=free_194, R'=J, S'=free_194, C1'=J, H1'=free_195, Q1'=free_196, [ K>=1+free_198 && J>=1+free_198 && free_198>=1+free_196 && free_197>=2 && D1>=0 ], cost: 1 26: f6 -> f7 : N'=free_202, O'=P, Q_1'=free_199, R'=J, S'=free_199, C1'=J, H1'=free_200, Q1'=free_201, [ K>=1+free_203 && J>=1+free_203 && free_201>=1+free_203 && free_202>=2 && D1>=0 ], cost: 1 27: f6 -> f4 : J'=free_206, N'=free_211, O'=free_204, P'=free_208, Q_1'=free_205, R'=free_212, C1'=free_207, F1'=free_209, J1'=free_210, [ D1>=0 && free_211>=2 && free_204>=1+free_210 && free_204>=1+K && J==P ], cost: 1 28: f6 -> f4 : J'=free_215, N'=free_220, O'=free_213, P'=free_217, Q_1'=free_214, R'=free_221, C1'=free_216, F1'=free_218, J1'=free_219, [ D1>=0 && free_220>=2 && free_213>=1+free_219 && K>=1+free_213 && J==P ], cost: 1 29: f6 -> f4 : J'=free_224, N'=free_229, O'=free_222, P'=free_226, Q_1'=free_223, R'=free_230, C1'=free_225, F1'=free_227, J1'=free_228, [ D1>=0 && free_229>=2 && free_228>=1+free_222 && free_222>=1+K && J==P ], cost: 1 30: f6 -> f4 : J'=free_233, N'=free_238, O'=free_231, P'=free_235, Q_1'=free_232, R'=free_239, C1'=free_234, F1'=free_236, J1'=free_237, [ D1>=0 && free_238>=2 && free_237>=1+free_231 && K>=1+free_231 && J==P ], cost: 1 52: f3 -> f1 : A'=N, B'=2, C'=free_404, D'=free_405, E'=free_404, O'=free_407, S1'=free_407, U1'=free_404, V1'=free_406, [ N>=2 ], cost: 1 51: f3 -> f4 : A'=free_400, B'=free_397, C'=free_392, D'=free_395, E'=free_390, J'=free_396, N'=free_391, P'=free_389, Q_1'=free_401, R'=free_394, C1'=free_399, F1'=free_393, S1'=free_388, T1'=free_402, U1'=free_398, [ 0>=free_403 && 0>=N && 0>=free_391 ], cost: 1 56: f3 -> f4 : A'=free_463, B'=free_461, C'=free_456, D'=free_454, E'=free_462, J'=free_455, N'=1, O'=J, P'=free_464, Q_1'=free_459, R'=free_453, C1'=free_458, F1'=free_465, S1'=free_452, T1'=free_460, U1'=free_457, [ N==1 ], cost: 1 57: f3 -> f4 : A'=free_479, B'=free_476, C'=free_471, D'=free_474, E'=free_469, J'=free_475, N'=1, O'=free_470, P'=free_468, Q_1'=free_480, R'=free_473, S'=free_478, C1'=free_481, F1'=free_472, S1'=free_467, T1'=free_482, U1'=free_477, B2'=free_466, [ 0>=1 && free_470>=1+free_466 && N==1 ], cost: 1 58: f3 -> f4 : A'=free_496, B'=free_493, C'=free_488, D'=free_491, E'=free_486, J'=free_492, N'=1, O'=free_487, P'=free_485, Q_1'=free_497, R'=free_490, S'=free_495, C1'=free_498, F1'=free_489, S1'=free_484, T1'=free_499, U1'=free_494, B2'=free_483, [ 0>=1 && free_483>=1+free_487 && N==1 ], cost: 1 59: f3 -> f4 : A'=free_513, B'=free_510, C'=free_505, D'=free_508, E'=free_503, J'=free_509, N'=1, O'=free_504, P'=free_502, Q_1'=free_514, R'=free_507, S'=free_512, C1'=free_515, F1'=free_506, S1'=free_501, T1'=free_516, U1'=free_511, B2'=free_500, [ 0>=1 && free_504>=1+free_500 && N==1 ], cost: 1 60: f3 -> f4 : A'=free_530, B'=free_527, C'=free_522, D'=free_525, E'=free_520, J'=free_526, N'=1, O'=free_521, P'=free_519, Q_1'=free_531, R'=free_524, S'=free_529, C1'=free_532, F1'=free_523, S1'=free_518, T1'=free_533, U1'=free_528, B2'=free_517, [ 0>=1 && free_517>=1+free_521 && N==1 ], cost: 1 Removed unsatisfiable initial transitions: Start location: f3 0: f1 -> f1 : B'=1+B, C'=D, D'=free_1, E'=D, F'=free, G'=B, H'=Q, [ A>=1+B && B>=0 ], cost: 1 53: f1 -> f7 : A'=free_418, B'=free_416, C'=free_412, D'=free_410, E'=free_417, K'=J, L'=E1, M'=0, N'=free_411, P'=O, Q_1'=free_414, R'=J, S'=free_414, C1'=J, F1'=free_420, S1'=free_408, T1'=free_415, U1'=free_413, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_419, A2'=free_409, [ free_421>=2 && W1>=free_421 && free_411>=2 && W1>=free_411 && O>=1+K && B>=A && B>=0 && W1>=0 && M==0 && J==K ], cost: 1 54: f1 -> f7 : A'=free_432, B'=free_430, C'=free_426, D'=free_424, E'=free_431, K'=J, L'=E1, M'=0, N'=free_425, P'=O, Q_1'=free_428, R'=J, S'=free_428, C1'=J, F1'=free_434, S1'=free_422, T1'=free_429, U1'=free_427, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_433, A2'=free_423, [ free_435>=2 && W1>=free_435 && free_425>=2 && W1>=free_425 && K>=1+O && B>=A && B>=0 && W1>=0 && M==0 && J==K ], cost: 1 55: f1 -> f4 : A'=free_448, B'=free_445, C'=free_440, D'=free_443, E'=free_438, J'=free_444, N'=free_439, P'=free_437, Q_1'=free_449, R'=free_442, C1'=free_447, F1'=free_441, S1'=free_436, T1'=free_450, U1'=free_446, [ free_451>=2 && W1>=free_451 && free_439>=2 && W1>=free_439 && B>=A && W1>=0 && B>=0 && O==J ], cost: 1 1: f5 -> f7 : L'=1+E1, M'=1, N'=free_7, O'=P, Q_1'=free_2, R'=J, S'=free_2, T'=free_4, U'=V, W'=Q, X'=K, Y'=free_6, Z'=free_3, A1'=free_5, B1'=free_8, C1'=J, D1'=E1, [ free_9>=1+free_10 && free_9>=1+J && free_9>=1+K && free_9>=1+free_8 && L>=0 && free_7>=2 && M==1 ], cost: 1 2: f5 -> f7 : L'=1+E1, M'=1, N'=free_16, O'=P, Q_1'=free_11, R'=J, S'=free_11, T'=free_13, U'=V, W'=Q, X'=K, Y'=free_15, Z'=free_12, A1'=free_14, B1'=free_17, C1'=J, D1'=E1, [ free_18>=1+free_19 && free_18>=1+J && free_18>=1+K && free_17>=1+free_18 && L>=0 && free_16>=2 && M==1 ], cost: 1 3: f5 -> f7 : L'=1+E1, M'=1, N'=free_25, O'=P, Q_1'=free_20, R'=J, S'=free_20, T'=free_22, U'=V, W'=Q, X'=K, Y'=free_24, Z'=free_21, A1'=free_23, B1'=free_26, C1'=J, D1'=E1, [ free_27>=1+free_28 && free_27>=1+J && K>=1+free_27 && free_27>=1+free_26 && L>=0 && free_25>=2 && M==1 ], cost: 1 4: f5 -> f7 : L'=1+E1, M'=1, N'=free_34, O'=P, Q_1'=free_29, R'=J, S'=free_29, T'=free_31, U'=V, W'=Q, X'=K, Y'=free_33, Z'=free_30, A1'=free_32, B1'=free_35, C1'=J, D1'=E1, [ free_36>=1+free_37 && free_36>=1+J && K>=1+free_36 && free_35>=1+free_36 && L>=0 && free_34>=2 && M==1 ], cost: 1 5: f5 -> f7 : L'=1+E1, M'=1, N'=free_43, O'=P, Q_1'=free_38, R'=J, S'=free_38, T'=free_40, U'=V, W'=Q, X'=K, Y'=free_42, Z'=free_39, A1'=free_41, B1'=free_44, C1'=J, D1'=E1, [ free_45>=1+free_46 && J>=1+free_45 && free_45>=1+K && free_45>=1+free_44 && L>=0 && free_43>=2 && M==1 ], cost: 1 6: f5 -> f7 : L'=1+E1, M'=1, N'=free_52, O'=P, Q_1'=free_47, R'=J, S'=free_47, T'=free_49, U'=V, W'=Q, X'=K, Y'=free_51, Z'=free_48, A1'=free_50, B1'=free_53, C1'=J, D1'=E1, [ free_54>=1+free_55 && J>=1+free_54 && free_54>=1+K && free_53>=1+free_54 && L>=0 && free_52>=2 && M==1 ], cost: 1 7: f5 -> f7 : L'=1+E1, M'=1, N'=free_61, O'=P, Q_1'=free_56, R'=J, S'=free_56, T'=free_58, U'=V, W'=Q, X'=K, Y'=free_60, Z'=free_57, A1'=free_59, B1'=free_62, C1'=J, D1'=E1, [ free_63>=1+free_64 && J>=1+free_63 && K>=1+free_63 && free_63>=1+free_62 && L>=0 && free_61>=2 && M==1 ], cost: 1 8: f5 -> f7 : L'=1+E1, M'=1, N'=free_70, O'=P, Q_1'=free_65, R'=J, S'=free_65, T'=free_67, U'=V, W'=Q, X'=K, Y'=free_69, Z'=free_66, A1'=free_68, B1'=free_71, C1'=J, D1'=E1, [ free_72>=1+free_73 && J>=1+free_72 && K>=1+free_72 && free_71>=1+free_72 && L>=0 && free_70>=2 && M==1 ], cost: 1 9: f5 -> f7 : L'=1+E1, M'=1, N'=free_79, O'=P, Q_1'=free_74, R'=J, S'=free_74, T'=free_76, U'=V, W'=Q, X'=K, Y'=free_78, Z'=free_75, A1'=free_77, B1'=free_80, C1'=J, D1'=E1, [ free_82>=1+free_81 && free_81>=1+J && free_81>=1+K && free_81>=1+free_80 && L>=0 && free_79>=2 && M==1 ], cost: 1 10: f5 -> f7 : L'=1+E1, M'=1, N'=free_88, O'=P, Q_1'=free_83, R'=J, S'=free_83, T'=free_85, U'=V, W'=Q, X'=K, Y'=free_87, Z'=free_84, A1'=free_86, B1'=free_89, C1'=J, D1'=E1, [ free_91>=1+free_90 && free_90>=1+J && free_90>=1+K && free_89>=1+free_90 && L>=0 && free_88>=2 && M==1 ], cost: 1 11: f5 -> f7 : L'=1+E1, M'=1, N'=free_97, O'=P, Q_1'=free_92, R'=J, S'=free_92, T'=free_94, U'=V, W'=Q, X'=K, Y'=free_96, Z'=free_93, A1'=free_95, B1'=free_98, C1'=J, D1'=E1, [ free_100>=1+free_99 && free_99>=1+J && K>=1+free_99 && free_99>=1+free_98 && L>=0 && free_97>=2 && M==1 ], cost: 1 12: f5 -> f7 : L'=1+E1, M'=1, N'=free_106, O'=P, Q_1'=free_101, R'=J, S'=free_101, T'=free_103, U'=V, W'=Q, X'=K, Y'=free_105, Z'=free_102, A1'=free_104, B1'=free_107, C1'=J, D1'=E1, [ free_109>=1+free_108 && free_108>=1+J && K>=1+free_108 && free_107>=1+free_108 && L>=0 && free_106>=2 && M==1 ], cost: 1 13: f5 -> f7 : L'=1+E1, M'=1, N'=free_115, O'=P, Q_1'=free_110, R'=J, S'=free_110, T'=free_112, U'=V, W'=Q, X'=K, Y'=free_114, Z'=free_111, A1'=free_113, B1'=free_116, C1'=J, D1'=E1, [ free_118>=1+free_117 && J>=1+free_117 && free_117>=1+K && free_117>=1+free_116 && L>=0 && free_115>=2 && M==1 ], cost: 1 14: f5 -> f7 : L'=1+E1, M'=1, N'=free_124, O'=P, Q_1'=free_119, R'=J, S'=free_119, T'=free_121, U'=V, W'=Q, X'=K, Y'=free_123, Z'=free_120, A1'=free_122, B1'=free_125, C1'=J, D1'=E1, [ free_127>=1+free_126 && J>=1+free_126 && free_126>=1+K && free_125>=1+free_126 && L>=0 && free_124>=2 && M==1 ], cost: 1 15: f5 -> f7 : L'=1+E1, M'=1, N'=free_133, O'=P, Q_1'=free_128, R'=J, S'=free_128, T'=free_130, U'=V, W'=Q, X'=K, Y'=free_132, Z'=free_129, A1'=free_131, B1'=free_134, C1'=J, D1'=E1, [ free_136>=1+free_135 && J>=1+free_135 && K>=1+free_135 && free_135>=1+free_134 && L>=0 && free_133>=2 && M==1 ], cost: 1 16: f5 -> f7 : L'=1+E1, M'=1, N'=free_142, O'=P, Q_1'=free_137, R'=J, S'=free_137, T'=free_139, U'=V, W'=Q, X'=K, Y'=free_141, Z'=free_138, A1'=free_140, B1'=free_143, C1'=J, D1'=E1, [ free_145>=1+free_144 && J>=1+free_144 && K>=1+free_144 && free_143>=1+free_144 && L>=0 && free_142>=2 && M==1 ], cost: 1 17: f5 -> f4 : J'=free_148, N'=free_153, O'=free_146, P'=free_150, Q_1'=free_147, R'=free_154, C1'=free_149, F1'=free_151, G1'=free_152, [ L>=0 && free_146>=1+free_152 && free_153>=2 && J==P ], cost: 1 18: f5 -> f4 : J'=free_157, N'=free_162, O'=free_155, P'=free_159, Q_1'=free_156, R'=free_163, C1'=free_158, F1'=free_160, G1'=free_161, [ L>=0 && free_161>=1+free_155 && free_162>=2 && J==P ], cost: 1 31: f7 -> f7 : M'=1+M, N'=free_243, O'=P, Q_1'=free_240, R'=J, S'=free_240, C1'=J, E1'=-1+E1, K1'=free_241, L1'=free_242, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_244>=1+free_245 && free_244>=1+J && free_244>=1+free_242 && free_244>=1+K && free_246>=0 && free_243>=2 && E1>=0 ], cost: 1 32: f7 -> f7 : M'=1+M, N'=free_250, O'=P, Q_1'=free_247, R'=J, S'=free_247, C1'=J, E1'=-1+E1, K1'=free_248, L1'=free_249, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_251>=1+free_252 && free_251>=1+J && free_251>=1+free_249 && K>=1+free_251 && free_253>=0 && free_250>=2 && E1>=0 ], cost: 1 33: f7 -> f7 : M'=1+M, N'=free_257, O'=P, Q_1'=free_254, R'=J, S'=free_254, C1'=J, E1'=-1+E1, K1'=free_255, L1'=free_256, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_258>=1+free_259 && free_258>=1+J && free_256>=1+free_258 && free_258>=1+K && free_260>=0 && free_257>=2 && E1>=0 ], cost: 1 34: f7 -> f7 : M'=1+M, N'=free_264, O'=P, Q_1'=free_261, R'=J, S'=free_261, C1'=J, E1'=-1+E1, K1'=free_262, L1'=free_263, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_265>=1+free_266 && free_265>=1+J && free_263>=1+free_265 && K>=1+free_265 && free_267>=0 && free_264>=2 && E1>=0 ], cost: 1 35: f7 -> f7 : M'=1+M, N'=free_271, O'=P, Q_1'=free_268, R'=J, S'=free_268, C1'=J, E1'=-1+E1, K1'=free_269, L1'=free_270, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_272>=1+free_273 && J>=1+free_272 && free_272>=1+free_270 && free_272>=1+K && free_274>=0 && free_271>=2 && E1>=0 ], cost: 1 36: f7 -> f7 : M'=1+M, N'=free_278, O'=P, Q_1'=free_275, R'=J, S'=free_275, C1'=J, E1'=-1+E1, K1'=free_276, L1'=free_277, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_279>=1+free_280 && J>=1+free_279 && free_279>=1+free_277 && K>=1+free_279 && free_281>=0 && free_278>=2 && E1>=0 ], cost: 1 37: f7 -> f7 : M'=1+M, N'=free_285, O'=P, Q_1'=free_282, R'=J, S'=free_282, C1'=J, E1'=-1+E1, K1'=free_283, L1'=free_284, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_286>=1+free_287 && J>=1+free_286 && free_284>=1+free_286 && free_286>=1+K && free_288>=0 && free_285>=2 && E1>=0 ], cost: 1 38: f7 -> f7 : M'=1+M, N'=free_292, O'=P, Q_1'=free_289, R'=J, S'=free_289, C1'=J, E1'=-1+E1, K1'=free_290, L1'=free_291, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_293>=1+free_294 && J>=1+free_293 && free_291>=1+free_293 && K>=1+free_293 && free_295>=0 && free_292>=2 && E1>=0 ], cost: 1 39: f7 -> f7 : M'=1+M, N'=free_299, O'=P, Q_1'=free_296, R'=J, S'=free_296, C1'=J, E1'=-1+E1, K1'=free_297, L1'=free_298, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_301>=1+free_300 && free_300>=1+J && free_300>=1+free_298 && free_300>=1+K && free_302>=0 && free_299>=2 && E1>=0 ], cost: 1 40: f7 -> f7 : M'=1+M, N'=free_306, O'=P, Q_1'=free_303, R'=J, S'=free_303, C1'=J, E1'=-1+E1, K1'=free_304, L1'=free_305, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_308>=1+free_307 && free_307>=1+J && free_307>=1+free_305 && K>=1+free_307 && free_309>=0 && free_306>=2 && E1>=0 ], cost: 1 41: f7 -> f7 : M'=1+M, N'=free_313, O'=P, Q_1'=free_310, R'=J, S'=free_310, C1'=J, E1'=-1+E1, K1'=free_311, L1'=free_312, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_315>=1+free_314 && free_314>=1+J && free_312>=1+free_314 && free_314>=1+K && free_316>=0 && free_313>=2 && E1>=0 ], cost: 1 42: f7 -> f7 : M'=1+M, N'=free_320, O'=P, Q_1'=free_317, R'=J, S'=free_317, C1'=J, E1'=-1+E1, K1'=free_318, L1'=free_319, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_322>=1+free_321 && free_321>=1+J && free_319>=1+free_321 && K>=1+free_321 && free_323>=0 && free_320>=2 && E1>=0 ], cost: 1 43: f7 -> f7 : M'=1+M, N'=free_327, O'=P, Q_1'=free_324, R'=J, S'=free_324, C1'=J, E1'=-1+E1, K1'=free_325, L1'=free_326, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_329>=1+free_328 && J>=1+free_328 && free_328>=1+free_326 && free_328>=1+K && free_330>=0 && free_327>=2 && E1>=0 ], cost: 1 44: f7 -> f7 : M'=1+M, N'=free_334, O'=P, Q_1'=free_331, R'=J, S'=free_331, C1'=J, E1'=-1+E1, K1'=free_332, L1'=free_333, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_336>=1+free_335 && J>=1+free_335 && free_335>=1+free_333 && K>=1+free_335 && free_337>=0 && free_334>=2 && E1>=0 ], cost: 1 45: f7 -> f7 : M'=1+M, N'=free_341, O'=P, Q_1'=free_338, R'=J, S'=free_338, C1'=J, E1'=-1+E1, K1'=free_339, L1'=free_340, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_343>=1+free_342 && J>=1+free_342 && free_340>=1+free_342 && free_342>=1+K && free_344>=0 && free_341>=2 && E1>=0 ], cost: 1 46: f7 -> f7 : M'=1+M, N'=free_348, O'=P, Q_1'=free_345, R'=J, S'=free_345, C1'=J, E1'=-1+E1, K1'=free_346, L1'=free_347, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_350>=1+free_349 && J>=1+free_349 && free_347>=1+free_349 && K>=1+free_349 && free_351>=0 && free_348>=2 && E1>=0 ], cost: 1 47: f7 -> f4 : J'=free_354, N'=free_359, O'=free_352, P'=free_356, Q_1'=free_353, R'=free_360, C1'=free_355, F1'=free_357, R1'=free_358, [ M>=0 && E1>=0 && free_359>=2 && free_352>=1+free_358 && free_352>=1+K && J==P ], cost: 1 48: f7 -> f4 : J'=free_363, N'=free_368, O'=free_361, P'=free_365, Q_1'=free_362, R'=free_369, C1'=free_364, F1'=free_366, R1'=free_367, [ M>=0 && E1>=0 && free_368>=2 && free_361>=1+free_367 && K>=1+free_361 && J==P ], cost: 1 49: f7 -> f4 : J'=free_372, N'=free_377, O'=free_370, P'=free_374, Q_1'=free_371, R'=free_378, C1'=free_373, F1'=free_375, R1'=free_376, [ M>=0 && E1>=0 && free_377>=2 && free_376>=1+free_370 && free_370>=1+K && J==P ], cost: 1 50: f7 -> f4 : J'=free_381, N'=free_386, O'=free_379, P'=free_383, Q_1'=free_380, R'=free_387, C1'=free_382, F1'=free_384, R1'=free_385, [ M>=0 && E1>=0 && free_386>=2 && free_385>=1+free_379 && K>=1+free_379 && J==P ], cost: 1 19: f6 -> f7 : N'=free_167, O'=P, Q_1'=free_164, R'=J, S'=free_164, C1'=J, H1'=free_165, Q1'=free_166, [ free_168>=1+K && free_168>=1+J && free_168>=1+free_166 && free_167>=2 && D1>=0 ], cost: 1 20: f6 -> f7 : N'=free_172, O'=P, Q_1'=free_169, R'=J, S'=free_169, C1'=J, H1'=free_170, Q1'=free_171, [ free_173>=1+K && free_173>=1+J && free_171>=1+free_173 && free_172>=2 && D1>=0 ], cost: 1 21: f6 -> f7 : N'=free_177, O'=P, Q_1'=free_174, R'=J, S'=free_174, C1'=J, H1'=free_175, Q1'=free_176, [ free_178>=1+K && J>=1+free_178 && free_178>=1+free_176 && free_177>=2 && D1>=0 ], cost: 1 22: f6 -> f7 : N'=free_182, O'=P, Q_1'=free_179, R'=J, S'=free_179, C1'=J, H1'=free_180, Q1'=free_181, [ free_183>=1+K && J>=1+free_183 && free_181>=1+free_183 && free_182>=2 && D1>=0 ], cost: 1 23: f6 -> f7 : N'=free_187, O'=P, Q_1'=free_184, R'=J, S'=free_184, C1'=J, H1'=free_185, Q1'=free_186, [ K>=1+free_188 && free_188>=1+J && free_188>=1+free_186 && free_187>=2 && D1>=0 ], cost: 1 24: f6 -> f7 : N'=free_192, O'=P, Q_1'=free_189, R'=J, S'=free_189, C1'=J, H1'=free_190, Q1'=free_191, [ K>=1+free_193 && free_193>=1+J && free_191>=1+free_193 && free_192>=2 && D1>=0 ], cost: 1 25: f6 -> f7 : N'=free_197, O'=P, Q_1'=free_194, R'=J, S'=free_194, C1'=J, H1'=free_195, Q1'=free_196, [ K>=1+free_198 && J>=1+free_198 && free_198>=1+free_196 && free_197>=2 && D1>=0 ], cost: 1 26: f6 -> f7 : N'=free_202, O'=P, Q_1'=free_199, R'=J, S'=free_199, C1'=J, H1'=free_200, Q1'=free_201, [ K>=1+free_203 && J>=1+free_203 && free_201>=1+free_203 && free_202>=2 && D1>=0 ], cost: 1 27: f6 -> f4 : J'=free_206, N'=free_211, O'=free_204, P'=free_208, Q_1'=free_205, R'=free_212, C1'=free_207, F1'=free_209, J1'=free_210, [ D1>=0 && free_211>=2 && free_204>=1+free_210 && free_204>=1+K && J==P ], cost: 1 28: f6 -> f4 : J'=free_215, N'=free_220, O'=free_213, P'=free_217, Q_1'=free_214, R'=free_221, C1'=free_216, F1'=free_218, J1'=free_219, [ D1>=0 && free_220>=2 && free_213>=1+free_219 && K>=1+free_213 && J==P ], cost: 1 29: f6 -> f4 : J'=free_224, N'=free_229, O'=free_222, P'=free_226, Q_1'=free_223, R'=free_230, C1'=free_225, F1'=free_227, J1'=free_228, [ D1>=0 && free_229>=2 && free_228>=1+free_222 && free_222>=1+K && J==P ], cost: 1 30: f6 -> f4 : J'=free_233, N'=free_238, O'=free_231, P'=free_235, Q_1'=free_232, R'=free_239, C1'=free_234, F1'=free_236, J1'=free_237, [ D1>=0 && free_238>=2 && free_237>=1+free_231 && K>=1+free_231 && J==P ], cost: 1 52: f3 -> f1 : A'=N, B'=2, C'=free_404, D'=free_405, E'=free_404, O'=free_407, S1'=free_407, U1'=free_404, V1'=free_406, [ N>=2 ], cost: 1 51: f3 -> f4 : A'=free_400, B'=free_397, C'=free_392, D'=free_395, E'=free_390, J'=free_396, N'=free_391, P'=free_389, Q_1'=free_401, R'=free_394, C1'=free_399, F1'=free_393, S1'=free_388, T1'=free_402, U1'=free_398, [ 0>=free_403 && 0>=N && 0>=free_391 ], cost: 1 56: f3 -> f4 : A'=free_463, B'=free_461, C'=free_456, D'=free_454, E'=free_462, J'=free_455, N'=1, O'=J, P'=free_464, Q_1'=free_459, R'=free_453, C1'=free_458, F1'=free_465, S1'=free_452, T1'=free_460, U1'=free_457, [ N==1 ], cost: 1 Simplified the transitions: Start location: f3 0: f1 -> f1 : B'=1+B, C'=D, D'=free_1, E'=D, F'=free, G'=B, H'=Q, [ A>=1+B && B>=0 ], cost: 1 53: f1 -> f7 : A'=free_418, B'=free_416, C'=free_412, D'=free_410, E'=free_417, K'=J, L'=E1, M'=0, N'=free_411, P'=O, Q_1'=free_414, R'=J, S'=free_414, C1'=J, F1'=free_420, S1'=free_408, T1'=free_415, U1'=free_413, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_419, A2'=free_409, [ free_421>=2 && W1>=free_421 && free_411>=2 && W1>=free_411 && O>=1+K && B>=A && B>=0 && W1>=0 && M==0 && J==K ], cost: 1 54: f1 -> f7 : A'=free_432, B'=free_430, C'=free_426, D'=free_424, E'=free_431, K'=J, L'=E1, M'=0, N'=free_425, P'=O, Q_1'=free_428, R'=J, S'=free_428, C1'=J, F1'=free_434, S1'=free_422, T1'=free_429, U1'=free_427, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_433, A2'=free_423, [ free_435>=2 && W1>=free_435 && free_425>=2 && W1>=free_425 && K>=1+O && B>=A && B>=0 && W1>=0 && M==0 && J==K ], cost: 1 31: f7 -> f7 : M'=1+M, N'=free_243, O'=P, Q_1'=free_240, R'=J, S'=free_240, C1'=J, E1'=-1+E1, K1'=free_241, L1'=free_242, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_243>=2 && E1>=0 ], cost: 1 32: f7 -> f7 : M'=1+M, N'=free_250, O'=P, Q_1'=free_247, R'=J, S'=free_247, C1'=J, E1'=-1+E1, K1'=free_248, L1'=free_249, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_250>=2 && E1>=0 && 1+J<=-1+K && 1+free_249<=-1+K ], cost: 1 33: f7 -> f7 : M'=1+M, N'=free_257, O'=P, Q_1'=free_254, R'=J, S'=free_254, C1'=J, E1'=-1+E1, K1'=free_255, L1'=free_256, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_257>=2 && E1>=0 && 1+J<=-1+free_256 && 1+K<=-1+free_256 ], cost: 1 34: f7 -> f7 : M'=1+M, N'=free_264, O'=P, Q_1'=free_261, R'=J, S'=free_261, C1'=J, E1'=-1+E1, K1'=free_262, L1'=free_263, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_264>=2 && E1>=0 && 1+J<=-1+free_263 && 1+J<=-1+K ], cost: 1 35: f7 -> f7 : M'=1+M, N'=free_271, O'=P, Q_1'=free_268, R'=J, S'=free_268, C1'=J, E1'=-1+E1, K1'=free_269, L1'=free_270, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_271>=2 && E1>=0 && 1+free_270<=-1+J && 1+K<=-1+J ], cost: 1 36: f7 -> f7 : M'=1+M, N'=free_278, O'=P, Q_1'=free_275, R'=J, S'=free_275, C1'=J, E1'=-1+E1, K1'=free_276, L1'=free_277, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_278>=2 && E1>=0 && 1+free_277<=-1+J && 1+free_277<=-1+K ], cost: 1 37: f7 -> f7 : M'=1+M, N'=free_285, O'=P, Q_1'=free_282, R'=J, S'=free_282, C1'=J, E1'=-1+E1, K1'=free_283, L1'=free_284, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_285>=2 && E1>=0 && 1+K<=-1+J && 1+K<=-1+free_284 ], cost: 1 38: f7 -> f7 : M'=1+M, N'=free_292, O'=P, Q_1'=free_289, R'=J, S'=free_289, C1'=J, E1'=-1+E1, K1'=free_290, L1'=free_291, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_292>=2 && E1>=0 ], cost: 1 39: f7 -> f7 : M'=1+M, N'=free_299, O'=P, Q_1'=free_296, R'=J, S'=free_296, C1'=J, E1'=-1+E1, K1'=free_297, L1'=free_298, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_299>=2 && E1>=0 ], cost: 1 40: f7 -> f7 : M'=1+M, N'=free_306, O'=P, Q_1'=free_303, R'=J, S'=free_303, C1'=J, E1'=-1+E1, K1'=free_304, L1'=free_305, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_306>=2 && E1>=0 && 1+J<=-1+K && 1+free_305<=-1+K ], cost: 1 41: f7 -> f7 : M'=1+M, N'=free_313, O'=P, Q_1'=free_310, R'=J, S'=free_310, C1'=J, E1'=-1+E1, K1'=free_311, L1'=free_312, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_313>=2 && E1>=0 && 1+J<=-1+free_312 && 1+K<=-1+free_312 ], cost: 1 42: f7 -> f7 : M'=1+M, N'=free_320, O'=P, Q_1'=free_317, R'=J, S'=free_317, C1'=J, E1'=-1+E1, K1'=free_318, L1'=free_319, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_320>=2 && E1>=0 && 1+J<=-1+free_319 && 1+J<=-1+K ], cost: 1 43: f7 -> f7 : M'=1+M, N'=free_327, O'=P, Q_1'=free_324, R'=J, S'=free_324, C1'=J, E1'=-1+E1, K1'=free_325, L1'=free_326, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_327>=2 && E1>=0 && 1+free_326<=-1+J && 1+K<=-1+J ], cost: 1 44: f7 -> f7 : M'=1+M, N'=free_334, O'=P, Q_1'=free_331, R'=J, S'=free_331, C1'=J, E1'=-1+E1, K1'=free_332, L1'=free_333, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_334>=2 && E1>=0 && 1+free_333<=-1+J && 1+free_333<=-1+K ], cost: 1 45: f7 -> f7 : M'=1+M, N'=free_341, O'=P, Q_1'=free_338, R'=J, S'=free_338, C1'=J, E1'=-1+E1, K1'=free_339, L1'=free_340, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_341>=2 && E1>=0 && 1+K<=-1+J && 1+K<=-1+free_340 ], cost: 1 46: f7 -> f7 : M'=1+M, N'=free_348, O'=P, Q_1'=free_345, R'=J, S'=free_345, C1'=J, E1'=-1+E1, K1'=free_346, L1'=free_347, M1'=V, N1'=Q, O1'=K, P1'=1+M, Q1_1'=-1+E1, [ free_350>=1+free_349 && J>=1+free_349 && free_347>=1+free_349 && K>=1+free_349 && free_351>=0 && free_348>=2 && E1>=0 ], cost: 1 52: f3 -> f1 : A'=N, B'=2, C'=free_404, D'=free_405, E'=free_404, O'=free_407, S1'=free_407, U1'=free_404, V1'=free_406, [ N>=2 ], cost: 1 Eliminating 1 self-loops for location f1 Self-Loop 0 has the metering function: -B+A, resulting in the new transition 61. Removing the self-loops: 0. Eliminating 16 self-loops for location f7 Self-Loop 31 has the metering function: 1+E1, resulting in the new transition 62. Self-Loop 32 has the metering function: 1+E1, resulting in the new transition 63. Self-Loop 33 has the metering function: 1+E1, resulting in the new transition 64. Self-Loop 34 has the metering function: 1+E1, resulting in the new transition 65. Self-Loop 35 has the metering function: 1+E1, resulting in the new transition 66. Self-Loop 36 has the metering function: 1+E1, resulting in the new transition 67. Self-Loop 37 has the metering function: 1+E1, resulting in the new transition 68. Self-Loop 38 has the metering function: 1+E1, resulting in the new transition 69. Self-Loop 39 has the metering function: 1+E1, resulting in the new transition 70. Self-Loop 40 has the metering function: 1+E1, resulting in the new transition 71. Self-Loop 41 has the metering function: 1+E1, resulting in the new transition 72. Self-Loop 42 has the metering function: 1+E1, resulting in the new transition 73. Self-Loop 43 has the metering function: 1+E1, resulting in the new transition 74. Self-Loop 44 has the metering function: 1+E1, resulting in the new transition 75. Self-Loop 45 has the metering function: 1+E1, resulting in the new transition 76. Self-Loop 46 has the metering function: 1+E1, resulting in the new transition 77. Removing the self-loops: 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46. Removed all Self-loops using metering functions (where possible): Start location: f3 61: f1 -> [6] : B'=A, C'=free_1, D'=free_1, E'=free_1, F'=free, G'=-1+A, H'=Q, [ A>=1+B && B>=0 ], cost: -B+A 62: f7 -> [7] : M'=1+E1+M, N'=free_243, O'=P, Q_1'=free_240, R'=J, S'=free_240, C1'=J, E1'=-1, K1'=free_241, L1'=free_242, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_243>=2 && E1>=0 ], cost: 1+E1 63: f7 -> [7] : M'=1+E1+M, N'=free_250, O'=P, Q_1'=free_247, R'=J, S'=free_247, C1'=J, E1'=-1, K1'=free_248, L1'=free_249, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_250>=2 && E1>=0 && 1+J<=-1+K && 1+free_249<=-1+K ], cost: 1+E1 64: f7 -> [7] : M'=1+E1+M, N'=free_257, O'=P, Q_1'=free_254, R'=J, S'=free_254, C1'=J, E1'=-1, K1'=free_255, L1'=free_256, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_257>=2 && E1>=0 && 1+J<=-1+free_256 && 1+K<=-1+free_256 ], cost: 1+E1 65: f7 -> [7] : M'=1+E1+M, N'=free_264, O'=P, Q_1'=free_261, R'=J, S'=free_261, C1'=J, E1'=-1, K1'=free_262, L1'=free_263, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_264>=2 && E1>=0 && 1+J<=-1+free_263 && 1+J<=-1+K ], cost: 1+E1 66: f7 -> [7] : M'=1+E1+M, N'=free_271, O'=P, Q_1'=free_268, R'=J, S'=free_268, C1'=J, E1'=-1, K1'=free_269, L1'=free_270, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_271>=2 && E1>=0 && 1+free_270<=-1+J && 1+K<=-1+J ], cost: 1+E1 67: f7 -> [7] : M'=1+E1+M, N'=free_278, O'=P, Q_1'=free_275, R'=J, S'=free_275, C1'=J, E1'=-1, K1'=free_276, L1'=free_277, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_278>=2 && E1>=0 && 1+free_277<=-1+J && 1+free_277<=-1+K ], cost: 1+E1 68: f7 -> [7] : M'=1+E1+M, N'=free_285, O'=P, Q_1'=free_282, R'=J, S'=free_282, C1'=J, E1'=-1, K1'=free_283, L1'=free_284, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_285>=2 && E1>=0 && 1+K<=-1+J && 1+K<=-1+free_284 ], cost: 1+E1 69: f7 -> [7] : M'=1+E1+M, N'=free_292, O'=P, Q_1'=free_289, R'=J, S'=free_289, C1'=J, E1'=-1, K1'=free_290, L1'=free_291, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_292>=2 && E1>=0 ], cost: 1+E1 70: f7 -> [7] : M'=1+E1+M, N'=free_299, O'=P, Q_1'=free_296, R'=J, S'=free_296, C1'=J, E1'=-1, K1'=free_297, L1'=free_298, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_299>=2 && E1>=0 ], cost: 1+E1 71: f7 -> [7] : M'=1+E1+M, N'=free_306, O'=P, Q_1'=free_303, R'=J, S'=free_303, C1'=J, E1'=-1, K1'=free_304, L1'=free_305, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_306>=2 && E1>=0 && 1+J<=-1+K && 1+free_305<=-1+K ], cost: 1+E1 72: f7 -> [7] : M'=1+E1+M, N'=free_313, O'=P, Q_1'=free_310, R'=J, S'=free_310, C1'=J, E1'=-1, K1'=free_311, L1'=free_312, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_313>=2 && E1>=0 && 1+J<=-1+free_312 && 1+K<=-1+free_312 ], cost: 1+E1 73: f7 -> [7] : M'=1+E1+M, N'=free_320, O'=P, Q_1'=free_317, R'=J, S'=free_317, C1'=J, E1'=-1, K1'=free_318, L1'=free_319, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_320>=2 && E1>=0 && 1+J<=-1+free_319 && 1+J<=-1+K ], cost: 1+E1 74: f7 -> [7] : M'=1+E1+M, N'=free_327, O'=P, Q_1'=free_324, R'=J, S'=free_324, C1'=J, E1'=-1, K1'=free_325, L1'=free_326, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_327>=2 && E1>=0 && 1+free_326<=-1+J && 1+K<=-1+J ], cost: 1+E1 75: f7 -> [7] : M'=1+E1+M, N'=free_334, O'=P, Q_1'=free_331, R'=J, S'=free_331, C1'=J, E1'=-1, K1'=free_332, L1'=free_333, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_334>=2 && E1>=0 && 1+free_333<=-1+J && 1+free_333<=-1+K ], cost: 1+E1 76: f7 -> [7] : M'=1+E1+M, N'=free_341, O'=P, Q_1'=free_338, R'=J, S'=free_338, C1'=J, E1'=-1, K1'=free_339, L1'=free_340, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_341>=2 && E1>=0 && 1+K<=-1+J && 1+K<=-1+free_340 ], cost: 1+E1 77: f7 -> [7] : M'=1+E1+M, N'=free_348, O'=P, Q_1'=free_345, R'=J, S'=free_345, C1'=J, E1'=-1, K1'=free_346, L1'=free_347, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_348>=2 && E1>=0 ], cost: 1+E1 52: f3 -> f1 : A'=N, B'=2, C'=free_404, D'=free_405, E'=free_404, O'=free_407, S1'=free_407, U1'=free_404, V1'=free_406, [ N>=2 ], cost: 1 53: [6] -> f7 : A'=free_418, B'=free_416, C'=free_412, D'=free_410, E'=free_417, K'=J, L'=E1, M'=0, N'=free_411, P'=O, Q_1'=free_414, R'=J, S'=free_414, C1'=J, F1'=free_420, S1'=free_408, T1'=free_415, U1'=free_413, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_419, A2'=free_409, [ free_421>=2 && W1>=free_421 && free_411>=2 && W1>=free_411 && O>=1+K && B>=A && B>=0 && W1>=0 && M==0 && J==K ], cost: 1 54: [6] -> f7 : A'=free_432, B'=free_430, C'=free_426, D'=free_424, E'=free_431, K'=J, L'=E1, M'=0, N'=free_425, P'=O, Q_1'=free_428, R'=J, S'=free_428, C1'=J, F1'=free_434, S1'=free_422, T1'=free_429, U1'=free_427, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_433, A2'=free_423, [ free_435>=2 && W1>=free_435 && free_425>=2 && W1>=free_425 && K>=1+O && B>=A && B>=0 && W1>=0 && M==0 && J==K ], cost: 1 Applied simple chaining: Start location: f3 62: f7 -> [7] : M'=1+E1+M, N'=free_243, O'=P, Q_1'=free_240, R'=J, S'=free_240, C1'=J, E1'=-1, K1'=free_241, L1'=free_242, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_243>=2 && E1>=0 ], cost: 1+E1 63: f7 -> [7] : M'=1+E1+M, N'=free_250, O'=P, Q_1'=free_247, R'=J, S'=free_247, C1'=J, E1'=-1, K1'=free_248, L1'=free_249, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_250>=2 && E1>=0 && 1+J<=-1+K && 1+free_249<=-1+K ], cost: 1+E1 64: f7 -> [7] : M'=1+E1+M, N'=free_257, O'=P, Q_1'=free_254, R'=J, S'=free_254, C1'=J, E1'=-1, K1'=free_255, L1'=free_256, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_257>=2 && E1>=0 && 1+J<=-1+free_256 && 1+K<=-1+free_256 ], cost: 1+E1 65: f7 -> [7] : M'=1+E1+M, N'=free_264, O'=P, Q_1'=free_261, R'=J, S'=free_261, C1'=J, E1'=-1, K1'=free_262, L1'=free_263, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_264>=2 && E1>=0 && 1+J<=-1+free_263 && 1+J<=-1+K ], cost: 1+E1 66: f7 -> [7] : M'=1+E1+M, N'=free_271, O'=P, Q_1'=free_268, R'=J, S'=free_268, C1'=J, E1'=-1, K1'=free_269, L1'=free_270, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_271>=2 && E1>=0 && 1+free_270<=-1+J && 1+K<=-1+J ], cost: 1+E1 67: f7 -> [7] : M'=1+E1+M, N'=free_278, O'=P, Q_1'=free_275, R'=J, S'=free_275, C1'=J, E1'=-1, K1'=free_276, L1'=free_277, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_278>=2 && E1>=0 && 1+free_277<=-1+J && 1+free_277<=-1+K ], cost: 1+E1 68: f7 -> [7] : M'=1+E1+M, N'=free_285, O'=P, Q_1'=free_282, R'=J, S'=free_282, C1'=J, E1'=-1, K1'=free_283, L1'=free_284, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_285>=2 && E1>=0 && 1+K<=-1+J && 1+K<=-1+free_284 ], cost: 1+E1 69: f7 -> [7] : M'=1+E1+M, N'=free_292, O'=P, Q_1'=free_289, R'=J, S'=free_289, C1'=J, E1'=-1, K1'=free_290, L1'=free_291, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_292>=2 && E1>=0 ], cost: 1+E1 70: f7 -> [7] : M'=1+E1+M, N'=free_299, O'=P, Q_1'=free_296, R'=J, S'=free_296, C1'=J, E1'=-1, K1'=free_297, L1'=free_298, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_299>=2 && E1>=0 ], cost: 1+E1 71: f7 -> [7] : M'=1+E1+M, N'=free_306, O'=P, Q_1'=free_303, R'=J, S'=free_303, C1'=J, E1'=-1, K1'=free_304, L1'=free_305, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_306>=2 && E1>=0 && 1+J<=-1+K && 1+free_305<=-1+K ], cost: 1+E1 72: f7 -> [7] : M'=1+E1+M, N'=free_313, O'=P, Q_1'=free_310, R'=J, S'=free_310, C1'=J, E1'=-1, K1'=free_311, L1'=free_312, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_313>=2 && E1>=0 && 1+J<=-1+free_312 && 1+K<=-1+free_312 ], cost: 1+E1 73: f7 -> [7] : M'=1+E1+M, N'=free_320, O'=P, Q_1'=free_317, R'=J, S'=free_317, C1'=J, E1'=-1, K1'=free_318, L1'=free_319, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_320>=2 && E1>=0 && 1+J<=-1+free_319 && 1+J<=-1+K ], cost: 1+E1 74: f7 -> [7] : M'=1+E1+M, N'=free_327, O'=P, Q_1'=free_324, R'=J, S'=free_324, C1'=J, E1'=-1, K1'=free_325, L1'=free_326, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_327>=2 && E1>=0 && 1+free_326<=-1+J && 1+K<=-1+J ], cost: 1+E1 75: f7 -> [7] : M'=1+E1+M, N'=free_334, O'=P, Q_1'=free_331, R'=J, S'=free_331, C1'=J, E1'=-1, K1'=free_332, L1'=free_333, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_334>=2 && E1>=0 && 1+free_333<=-1+J && 1+free_333<=-1+K ], cost: 1+E1 76: f7 -> [7] : M'=1+E1+M, N'=free_341, O'=P, Q_1'=free_338, R'=J, S'=free_338, C1'=J, E1'=-1, K1'=free_339, L1'=free_340, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_341>=2 && E1>=0 && 1+K<=-1+J && 1+K<=-1+free_340 ], cost: 1+E1 77: f7 -> [7] : M'=1+E1+M, N'=free_348, O'=P, Q_1'=free_345, R'=J, S'=free_345, C1'=J, E1'=-1, K1'=free_346, L1'=free_347, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_348>=2 && E1>=0 ], cost: 1+E1 52: f3 -> [6] : A'=N, B'=N, C'=free_1, D'=free_1, E'=free_1, F'=free, G'=-1+N, H'=Q, O'=free_407, S1'=free_407, U1'=free_404, V1'=free_406, [ N>=2 && N>=3 && 2>=0 ], cost: -1+N 53: [6] -> f7 : A'=free_418, B'=free_416, C'=free_412, D'=free_410, E'=free_417, K'=J, L'=E1, M'=0, N'=free_411, P'=O, Q_1'=free_414, R'=J, S'=free_414, C1'=J, F1'=free_420, S1'=free_408, T1'=free_415, U1'=free_413, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_419, A2'=free_409, [ free_421>=2 && W1>=free_421 && free_411>=2 && W1>=free_411 && O>=1+K && B>=A && B>=0 && W1>=0 && M==0 && J==K ], cost: 1 54: [6] -> f7 : A'=free_432, B'=free_430, C'=free_426, D'=free_424, E'=free_431, K'=J, L'=E1, M'=0, N'=free_425, P'=O, Q_1'=free_428, R'=J, S'=free_428, C1'=J, F1'=free_434, S1'=free_422, T1'=free_429, U1'=free_427, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_433, A2'=free_423, [ free_435>=2 && W1>=free_435 && free_425>=2 && W1>=free_425 && K>=1+O && B>=A && B>=0 && W1>=0 && M==0 && J==K ], cost: 1 Applied chaining over branches and pruning: Start location: f3 63: f7 -> [7] : M'=1+E1+M, N'=free_250, O'=P, Q_1'=free_247, R'=J, S'=free_247, C1'=J, E1'=-1, K1'=free_248, L1'=free_249, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_250>=2 && E1>=0 && 1+J<=-1+K && 1+free_249<=-1+K ], cost: 1+E1 65: f7 -> [7] : M'=1+E1+M, N'=free_264, O'=P, Q_1'=free_261, R'=J, S'=free_261, C1'=J, E1'=-1, K1'=free_262, L1'=free_263, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_264>=2 && E1>=0 && 1+J<=-1+free_263 && 1+J<=-1+K ], cost: 1+E1 71: f7 -> [7] : M'=1+E1+M, N'=free_306, O'=P, Q_1'=free_303, R'=J, S'=free_303, C1'=J, E1'=-1, K1'=free_304, L1'=free_305, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_306>=2 && E1>=0 && 1+J<=-1+K && 1+free_305<=-1+K ], cost: 1+E1 72: f7 -> [7] : M'=1+E1+M, N'=free_313, O'=P, Q_1'=free_310, R'=J, S'=free_310, C1'=J, E1'=-1, K1'=free_311, L1'=free_312, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_313>=2 && E1>=0 && 1+J<=-1+free_312 && 1+K<=-1+free_312 ], cost: 1+E1 75: f7 -> [7] : M'=1+E1+M, N'=free_334, O'=P, Q_1'=free_331, R'=J, S'=free_331, C1'=J, E1'=-1, K1'=free_332, L1'=free_333, M1'=V, N1'=Q, O1'=K, P1'=1+E1+M, Q1_1'=-1, [ free_334>=2 && E1>=0 && 1+free_333<=-1+J && 1+free_333<=-1+K ], cost: 1+E1 78: f3 -> f7 : A'=free_418, B'=free_416, C'=free_412, D'=free_410, E'=free_417, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=0, N'=free_411, O'=free_407, P'=free_407, Q_1'=free_414, R'=J, S'=free_414, C1'=J, F1'=free_420, S1'=free_408, T1'=free_415, U1'=free_413, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_419, A2'=free_409, [ N>=2 && N>=3 && 2>=0 && free_421>=2 && W1>=free_421 && free_411>=2 && W1>=free_411 && free_407>=1+K && N>=N && N>=0 && W1>=0 && M==0 && J==K ], cost: N 79: f3 -> f7 : A'=free_432, B'=free_430, C'=free_426, D'=free_424, E'=free_431, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=0, N'=free_425, O'=free_407, P'=free_407, Q_1'=free_428, R'=J, S'=free_428, C1'=J, F1'=free_434, S1'=free_422, T1'=free_429, U1'=free_427, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_433, A2'=free_423, [ N>=2 && N>=3 && 2>=0 && free_435>=2 && W1>=free_435 && free_425>=2 && W1>=free_425 && K>=1+free_407 && N>=N && N>=0 && W1>=0 && M==0 && J==K ], cost: N Applied chaining over branches and pruning: Start location: f3 83: f3 -> [7] : A'=free_418, B'=free_416, C'=free_412, D'=free_410, E'=free_417, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=1+E1, N'=free_313, O'=free_407, P'=free_407, Q_1'=free_310, R'=J, S'=free_310, C1'=J, E1'=-1, F1'=free_420, K1'=free_311, L1'=free_312, M1'=V, N1'=Q, O1'=J, P1'=1+E1, Q1_1'=-1, S1'=free_408, T1'=free_415, U1'=free_413, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_419, A2'=free_409, [ N>=2 && N>=3 && 2>=0 && free_421>=2 && W1>=free_421 && free_411>=2 && W1>=free_411 && free_407>=1+K && N>=N && N>=0 && W1>=0 && M==0 && J==K && free_313>=2 && E1>=0 && 1+J<=-1+free_312 && 1+J<=-1+free_312 ], cost: 1+N+E1 84: f3 -> [7] : A'=free_418, B'=free_416, C'=free_412, D'=free_410, E'=free_417, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=1+E1, N'=free_334, O'=free_407, P'=free_407, Q_1'=free_331, R'=J, S'=free_331, C1'=J, E1'=-1, F1'=free_420, K1'=free_332, L1'=free_333, M1'=V, N1'=Q, O1'=J, P1'=1+E1, Q1_1'=-1, S1'=free_408, T1'=free_415, U1'=free_413, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_419, A2'=free_409, [ N>=2 && N>=3 && 2>=0 && free_421>=2 && W1>=free_421 && free_411>=2 && W1>=free_411 && free_407>=1+K && N>=N && N>=0 && W1>=0 && M==0 && J==K && free_334>=2 && E1>=0 && 1+free_333<=-1+J && 1+free_333<=-1+J ], cost: 1+N+E1 88: f3 -> [7] : A'=free_432, B'=free_430, C'=free_426, D'=free_424, E'=free_431, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=1+E1, N'=free_313, O'=free_407, P'=free_407, Q_1'=free_310, R'=J, S'=free_310, C1'=J, E1'=-1, F1'=free_434, K1'=free_311, L1'=free_312, M1'=V, N1'=Q, O1'=J, P1'=1+E1, Q1_1'=-1, S1'=free_422, T1'=free_429, U1'=free_427, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_433, A2'=free_423, [ N>=2 && N>=3 && 2>=0 && free_435>=2 && W1>=free_435 && free_425>=2 && W1>=free_425 && K>=1+free_407 && N>=N && N>=0 && W1>=0 && M==0 && J==K && free_313>=2 && E1>=0 && 1+J<=-1+free_312 && 1+J<=-1+free_312 ], cost: 1+N+E1 89: f3 -> [7] : A'=free_432, B'=free_430, C'=free_426, D'=free_424, E'=free_431, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=1+E1, N'=free_334, O'=free_407, P'=free_407, Q_1'=free_331, R'=J, S'=free_331, C1'=J, E1'=-1, F1'=free_434, K1'=free_332, L1'=free_333, M1'=V, N1'=Q, O1'=J, P1'=1+E1, Q1_1'=-1, S1'=free_422, T1'=free_429, U1'=free_427, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_433, A2'=free_423, [ N>=2 && N>=3 && 2>=0 && free_435>=2 && W1>=free_435 && free_425>=2 && W1>=free_425 && K>=1+free_407 && N>=N && N>=0 && W1>=0 && M==0 && J==K && free_334>=2 && E1>=0 && 1+free_333<=-1+J && 1+free_333<=-1+J ], cost: 1+N+E1 80: f3 -> [8] : A'=free_418, B'=free_416, C'=free_412, D'=free_410, E'=free_417, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=0, N'=free_411, O'=free_407, P'=free_407, Q_1'=free_414, R'=J, S'=free_414, C1'=J, F1'=free_420, S1'=free_408, T1'=free_415, U1'=free_413, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_419, A2'=free_409, [ N>=2 && N>=3 && 2>=0 && free_421>=2 && W1>=free_421 && free_411>=2 && W1>=free_411 && free_407>=1+K && N>=N && N>=0 && W1>=0 && M==0 && J==K ], cost: N 81: f3 -> [9] : A'=free_418, B'=free_416, C'=free_412, D'=free_410, E'=free_417, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=0, N'=free_411, O'=free_407, P'=free_407, Q_1'=free_414, R'=J, S'=free_414, C1'=J, F1'=free_420, S1'=free_408, T1'=free_415, U1'=free_413, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_419, A2'=free_409, [ N>=2 && N>=3 && 2>=0 && free_421>=2 && W1>=free_421 && free_411>=2 && W1>=free_411 && free_407>=1+K && N>=N && N>=0 && W1>=0 && M==0 && J==K ], cost: N 82: f3 -> [10] : A'=free_418, B'=free_416, C'=free_412, D'=free_410, E'=free_417, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=0, N'=free_411, O'=free_407, P'=free_407, Q_1'=free_414, R'=J, S'=free_414, C1'=J, F1'=free_420, S1'=free_408, T1'=free_415, U1'=free_413, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_419, A2'=free_409, [ N>=2 && N>=3 && 2>=0 && free_421>=2 && W1>=free_421 && free_411>=2 && W1>=free_411 && free_407>=1+K && N>=N && N>=0 && W1>=0 && M==0 && J==K ], cost: N 85: f3 -> [11] : A'=free_432, B'=free_430, C'=free_426, D'=free_424, E'=free_431, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=0, N'=free_425, O'=free_407, P'=free_407, Q_1'=free_428, R'=J, S'=free_428, C1'=J, F1'=free_434, S1'=free_422, T1'=free_429, U1'=free_427, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_433, A2'=free_423, [ N>=2 && N>=3 && 2>=0 && free_435>=2 && W1>=free_435 && free_425>=2 && W1>=free_425 && K>=1+free_407 && N>=N && N>=0 && W1>=0 && M==0 && J==K ], cost: N 86: f3 -> [12] : A'=free_432, B'=free_430, C'=free_426, D'=free_424, E'=free_431, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=0, N'=free_425, O'=free_407, P'=free_407, Q_1'=free_428, R'=J, S'=free_428, C1'=J, F1'=free_434, S1'=free_422, T1'=free_429, U1'=free_427, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_433, A2'=free_423, [ N>=2 && N>=3 && 2>=0 && free_435>=2 && W1>=free_435 && free_425>=2 && W1>=free_425 && K>=1+free_407 && N>=N && N>=0 && W1>=0 && M==0 && J==K ], cost: N 87: f3 -> [13] : A'=free_432, B'=free_430, C'=free_426, D'=free_424, E'=free_431, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=0, N'=free_425, O'=free_407, P'=free_407, Q_1'=free_428, R'=J, S'=free_428, C1'=J, F1'=free_434, S1'=free_422, T1'=free_429, U1'=free_427, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_433, A2'=free_423, [ N>=2 && N>=3 && 2>=0 && free_435>=2 && W1>=free_435 && free_425>=2 && W1>=free_425 && K>=1+free_407 && N>=N && N>=0 && W1>=0 && M==0 && J==K ], cost: N Final control flow graph problem, now checking costs for infinitely many models: Start location: f3 83: f3 -> [7] : A'=free_418, B'=free_416, C'=free_412, D'=free_410, E'=free_417, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=1+E1, N'=free_313, O'=free_407, P'=free_407, Q_1'=free_310, R'=J, S'=free_310, C1'=J, E1'=-1, F1'=free_420, K1'=free_311, L1'=free_312, M1'=V, N1'=Q, O1'=J, P1'=1+E1, Q1_1'=-1, S1'=free_408, T1'=free_415, U1'=free_413, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_419, A2'=free_409, [ N>=2 && N>=3 && 2>=0 && free_421>=2 && W1>=free_421 && free_411>=2 && W1>=free_411 && free_407>=1+K && N>=N && N>=0 && W1>=0 && M==0 && J==K && free_313>=2 && E1>=0 && 1+J<=-1+free_312 && 1+J<=-1+free_312 ], cost: 1+N+E1 84: f3 -> [7] : A'=free_418, B'=free_416, C'=free_412, D'=free_410, E'=free_417, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=1+E1, N'=free_334, O'=free_407, P'=free_407, Q_1'=free_331, R'=J, S'=free_331, C1'=J, E1'=-1, F1'=free_420, K1'=free_332, L1'=free_333, M1'=V, N1'=Q, O1'=J, P1'=1+E1, Q1_1'=-1, S1'=free_408, T1'=free_415, U1'=free_413, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_419, A2'=free_409, [ N>=2 && N>=3 && 2>=0 && free_421>=2 && W1>=free_421 && free_411>=2 && W1>=free_411 && free_407>=1+K && N>=N && N>=0 && W1>=0 && M==0 && J==K && free_334>=2 && E1>=0 && 1+free_333<=-1+J && 1+free_333<=-1+J ], cost: 1+N+E1 88: f3 -> [7] : A'=free_432, B'=free_430, C'=free_426, D'=free_424, E'=free_431, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=1+E1, N'=free_313, O'=free_407, P'=free_407, Q_1'=free_310, R'=J, S'=free_310, C1'=J, E1'=-1, F1'=free_434, K1'=free_311, L1'=free_312, M1'=V, N1'=Q, O1'=J, P1'=1+E1, Q1_1'=-1, S1'=free_422, T1'=free_429, U1'=free_427, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_433, A2'=free_423, [ N>=2 && N>=3 && 2>=0 && free_435>=2 && W1>=free_435 && free_425>=2 && W1>=free_425 && K>=1+free_407 && N>=N && N>=0 && W1>=0 && M==0 && J==K && free_313>=2 && E1>=0 && 1+J<=-1+free_312 && 1+J<=-1+free_312 ], cost: 1+N+E1 89: f3 -> [7] : A'=free_432, B'=free_430, C'=free_426, D'=free_424, E'=free_431, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=1+E1, N'=free_334, O'=free_407, P'=free_407, Q_1'=free_331, R'=J, S'=free_331, C1'=J, E1'=-1, F1'=free_434, K1'=free_332, L1'=free_333, M1'=V, N1'=Q, O1'=J, P1'=1+E1, Q1_1'=-1, S1'=free_422, T1'=free_429, U1'=free_427, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_433, A2'=free_423, [ N>=2 && N>=3 && 2>=0 && free_435>=2 && W1>=free_435 && free_425>=2 && W1>=free_425 && K>=1+free_407 && N>=N && N>=0 && W1>=0 && M==0 && J==K && free_334>=2 && E1>=0 && 1+free_333<=-1+J && 1+free_333<=-1+J ], cost: 1+N+E1 80: f3 -> [8] : A'=free_418, B'=free_416, C'=free_412, D'=free_410, E'=free_417, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=0, N'=free_411, O'=free_407, P'=free_407, Q_1'=free_414, R'=J, S'=free_414, C1'=J, F1'=free_420, S1'=free_408, T1'=free_415, U1'=free_413, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_419, A2'=free_409, [ N>=2 && N>=3 && 2>=0 && free_421>=2 && W1>=free_421 && free_411>=2 && W1>=free_411 && free_407>=1+K && N>=N && N>=0 && W1>=0 && M==0 && J==K ], cost: N 81: f3 -> [9] : A'=free_418, B'=free_416, C'=free_412, D'=free_410, E'=free_417, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=0, N'=free_411, O'=free_407, P'=free_407, Q_1'=free_414, R'=J, S'=free_414, C1'=J, F1'=free_420, S1'=free_408, T1'=free_415, U1'=free_413, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_419, A2'=free_409, [ N>=2 && N>=3 && 2>=0 && free_421>=2 && W1>=free_421 && free_411>=2 && W1>=free_411 && free_407>=1+K && N>=N && N>=0 && W1>=0 && M==0 && J==K ], cost: N 82: f3 -> [10] : A'=free_418, B'=free_416, C'=free_412, D'=free_410, E'=free_417, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=0, N'=free_411, O'=free_407, P'=free_407, Q_1'=free_414, R'=J, S'=free_414, C1'=J, F1'=free_420, S1'=free_408, T1'=free_415, U1'=free_413, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_419, A2'=free_409, [ N>=2 && N>=3 && 2>=0 && free_421>=2 && W1>=free_421 && free_411>=2 && W1>=free_411 && free_407>=1+K && N>=N && N>=0 && W1>=0 && M==0 && J==K ], cost: N 85: f3 -> [11] : A'=free_432, B'=free_430, C'=free_426, D'=free_424, E'=free_431, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=0, N'=free_425, O'=free_407, P'=free_407, Q_1'=free_428, R'=J, S'=free_428, C1'=J, F1'=free_434, S1'=free_422, T1'=free_429, U1'=free_427, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_433, A2'=free_423, [ N>=2 && N>=3 && 2>=0 && free_435>=2 && W1>=free_435 && free_425>=2 && W1>=free_425 && K>=1+free_407 && N>=N && N>=0 && W1>=0 && M==0 && J==K ], cost: N 86: f3 -> [12] : A'=free_432, B'=free_430, C'=free_426, D'=free_424, E'=free_431, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=0, N'=free_425, O'=free_407, P'=free_407, Q_1'=free_428, R'=J, S'=free_428, C1'=J, F1'=free_434, S1'=free_422, T1'=free_429, U1'=free_427, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_433, A2'=free_423, [ N>=2 && N>=3 && 2>=0 && free_435>=2 && W1>=free_435 && free_425>=2 && W1>=free_425 && K>=1+free_407 && N>=N && N>=0 && W1>=0 && M==0 && J==K ], cost: N 87: f3 -> [13] : A'=free_432, B'=free_430, C'=free_426, D'=free_424, E'=free_431, F'=free, G'=-1+N, H'=Q, K'=J, L'=E1, M'=0, N'=free_425, O'=free_407, P'=free_407, Q_1'=free_428, R'=J, S'=free_428, C1'=J, F1'=free_434, S1'=free_422, T1'=free_429, U1'=free_427, V1'=free_406, W1'=1+E1, X1'=V, Y1'=Q, Z1'=free_433, A2'=free_423, [ N>=2 && N>=3 && 2>=0 && free_435>=2 && W1>=free_435 && free_425>=2 && W1>=free_425 && K>=1+free_407 && N>=N && N>=0 && W1>=0 && M==0 && J==K ], cost: N Computing complexity for remaining 10 transitions. Found configuration with infinitely models for cost: 1+N+E1 and guard: N>=2 && N>=3 && 2>=0 && free_421>=2 && W1>=free_421 && free_411>=2 && W1>=free_411 && free_407>=1+K && N>=N && N>=0 && W1>=0 && M==0 && J==K && free_313>=2 && E1>=0 && 1+J<=-1+free_312 && 1+J<=-1+free_312: free_411: Const, K: Both, N: Pos, free_421: Const, E1: Pos, free_313: Pos, M: Both, J: Both, free_407: Pos, W1: Pos, free_312: Pos Found new complexity n^1, because: Found infinity configuration. The final runtime is determined by this resulting transition: Final Guard: N>=2 && N>=3 && 2>=0 && free_421>=2 && W1>=free_421 && free_411>=2 && W1>=free_411 && free_407>=1+K && N>=N && N>=0 && W1>=0 && M==0 && J==K && free_313>=2 && E1>=0 && 1+J<=-1+free_312 && 1+J<=-1+free_312 Final Cost: 1+N+E1 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),?)