Trying to load file: main.koat Initial Control flow graph problem: Start location: f15 2: f7 -> f7 : A'=1+A, C'=N, M'=N, N'=free_22, W'=free_23, X'=A, Y'=T, [ B>=1+A && A>=0 ], cost: 1 0: f7 -> f14 : A'=E, B'=free_9, C'=free_4, F'=0, G'=D, H'=free_1, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=C, P'=C, Q_1'=D, R'=C, S'=T, U'=free_5, V'=free_6, [ A>=B && A>=0 && C>=1+D && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 ], cost: 1 1: f7 -> f14 : A'=E, B'=free_20, C'=free_15, F'=0, G'=D, H'=free_12, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=C, P'=C, Q_1'=D, R'=C, S'=T, U'=free_16, V'=free_17, [ A>=B && A>=0 && D>=1+C && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 ], cost: 1 15: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_93, O'=free_95, P'=free_95, Z'=free_92, H1'=R, Q1'=free_94, J1'=T, K1'=1+F, L1'=-1+E, [ free_96>=1+free_97 && free_96>=1+free_94 && F>=0 && E>=0 && free_95>=1+free_96 && free_93>=2 ], cost: 1 16: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_99, O'=free_101, P'=free_101, Z'=free_98, H1'=R, Q1'=free_100, J1'=T, K1'=1+F, L1'=-1+E, [ free_102>=1+free_103 && free_102>=1+free_100 && F>=0 && E>=0 && free_102>=1+free_101 && free_99>=2 ], cost: 1 17: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_105, O'=free_107, P'=free_107, Z'=free_104, H1'=R, Q1'=free_106, J1'=T, K1'=1+F, L1'=-1+E, [ free_108>=1+free_109 && free_106>=1+free_108 && F>=0 && E>=0 && free_107>=1+free_108 && free_105>=2 ], cost: 1 18: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_111, O'=free_113, P'=free_113, Z'=free_110, H1'=R, Q1'=free_112, J1'=T, K1'=1+F, L1'=-1+E, [ free_114>=1+free_115 && free_112>=1+free_114 && F>=0 && E>=0 && free_114>=1+free_113 && free_111>=2 ], cost: 1 19: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_117, O'=free_119, P'=free_119, Z'=free_116, H1'=R, Q1'=free_118, J1'=T, K1'=1+F, L1'=-1+E, [ free_121>=1+free_120 && free_120>=1+free_118 && F>=0 && E>=0 && free_119>=1+free_120 && free_117>=2 ], cost: 1 20: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_123, O'=free_125, P'=free_125, Z'=free_122, H1'=R, Q1'=free_124, J1'=T, K1'=1+F, L1'=-1+E, [ free_127>=1+free_126 && free_126>=1+free_124 && F>=0 && E>=0 && free_126>=1+free_125 && free_123>=2 ], cost: 1 21: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_129, O'=free_131, P'=free_131, Z'=free_128, H1'=R, Q1'=free_130, J1'=T, K1'=1+F, L1'=-1+E, [ free_133>=1+free_132 && free_130>=1+free_132 && F>=0 && E>=0 && free_131>=1+free_132 && free_129>=2 ], cost: 1 22: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_135, O'=free_137, P'=free_137, Z'=free_134, H1'=R, Q1'=free_136, J1'=T, K1'=1+F, L1'=-1+E, [ free_139>=1+free_138 && free_136>=1+free_138 && F>=0 && E>=0 && free_138>=1+free_137 && free_135>=2 ], cost: 1 47: f14 -> f5 : F'=1+R1, G'=D, H'=free_250, P'=free_253, Q_1'=free_249, R'=free_251, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_252, [ free_254>=2 && free_250>=2 && E>=0 && F>=0 && O>=1+D && D>=1+O && Q_1==R ], cost: 1 48: f14 -> f5 : F'=1+R1, G'=D, H'=free_256, P'=free_259, Q_1'=free_255, R'=free_257, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_258, [ free_260>=2 && free_256>=2 && E>=0 && F>=0 && O>=1+D && Q_1==R ], cost: 1 49: f14 -> f5 : F'=1+R1, G'=D, H'=free_262, P'=free_265, Q_1'=free_261, R'=free_263, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_264, [ free_266>=2 && free_262>=2 && E>=0 && F>=0 && D>=1+O && Q_1==R ], cost: 1 50: f14 -> f5 : F'=1+R1, G'=D, H'=free_268, P'=free_271, Q_1'=free_267, R'=free_269, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_270, [ free_272>=2 && free_268>=2 && E>=0 && F>=0 && D>=1+O && O>=1+D && Q_1==R ], cost: 1 3: f9 -> f14 : D'=Q_1, F'=1, G'=Q_1, H'=free_25, O'=free_28, P'=free_28, Z'=free_24, A1'=1+E, B1'=T, C1'=free_26, D1'=free_27, E1'=E, [ free_30>=1+R && A>=0 && free_25>=2 && free_28>=1+free_30 && free_29>=free_25 && F==1 ], cost: 1 4: f9 -> f14 : D'=Q_1, F'=1, G'=Q_1, H'=free_32, O'=free_35, P'=free_35, Z'=free_31, A1'=1+E, B1'=T, C1'=free_33, D1'=free_34, E1'=E, [ free_37>=1+R && A>=0 && free_32>=2 && free_37>=1+free_35 && free_36>=free_32 && F==1 ], cost: 1 5: f9 -> f14 : D'=Q_1, F'=1, G'=Q_1, H'=free_39, O'=free_42, P'=free_42, Z'=free_38, A1'=1+E, B1'=T, C1'=free_40, D1'=free_41, E1'=E, [ R>=1+free_44 && A>=0 && free_39>=2 && free_42>=1+free_44 && free_43>=free_39 && F==1 ], cost: 1 6: f9 -> f14 : D'=Q_1, F'=1, G'=Q_1, H'=free_46, O'=free_49, P'=free_49, Z'=free_45, A1'=1+E, B1'=T, C1'=free_47, D1'=free_48, E1'=E, [ R>=1+free_51 && A>=0 && free_46>=2 && free_51>=1+free_49 && free_50>=free_46 && F==1 ], cost: 1 7: f10 -> f14 : D'=Q_1, G'=Q_1, H'=free_53, O'=free_55, P'=free_55, F1'=free_52, G1'=free_54, [ free_56>=1+R && free_56>=1+free_54 && E1>=0 && free_55>=1+free_56 && free_53>=2 ], cost: 1 8: f10 -> f14 : D'=Q_1, G'=Q_1, H'=free_58, O'=free_60, P'=free_60, F1'=free_57, G1'=free_59, [ free_61>=1+R && free_61>=1+free_59 && E1>=0 && free_61>=1+free_60 && free_58>=2 ], cost: 1 9: f10 -> f14 : D'=Q_1, G'=Q_1, H'=free_63, O'=free_65, P'=free_65, F1'=free_62, G1'=free_64, [ free_66>=1+R && free_64>=1+free_66 && E1>=0 && free_65>=1+free_66 && free_63>=2 ], cost: 1 10: f10 -> f14 : D'=Q_1, G'=Q_1, H'=free_68, O'=free_70, P'=free_70, F1'=free_67, G1'=free_69, [ free_71>=1+R && free_69>=1+free_71 && E1>=0 && free_71>=1+free_70 && free_68>=2 ], cost: 1 11: f10 -> f14 : D'=Q_1, G'=Q_1, H'=free_73, O'=free_75, P'=free_75, F1'=free_72, G1'=free_74, [ R>=1+free_76 && free_76>=1+free_74 && E1>=0 && free_75>=1+free_76 && free_73>=2 ], cost: 1 12: f10 -> f14 : D'=Q_1, G'=Q_1, H'=free_78, O'=free_80, P'=free_80, F1'=free_77, G1'=free_79, [ R>=1+free_81 && free_81>=1+free_79 && E1>=0 && free_81>=1+free_80 && free_78>=2 ], cost: 1 13: f10 -> f14 : D'=Q_1, G'=Q_1, H'=free_83, O'=free_85, P'=free_85, F1'=free_82, G1'=free_84, [ R>=1+free_86 && free_84>=1+free_86 && E1>=0 && free_85>=1+free_86 && free_83>=2 ], cost: 1 14: f10 -> f14 : D'=Q_1, G'=Q_1, H'=free_88, O'=free_90, P'=free_90, F1'=free_87, G1'=free_89, [ R>=1+free_91 && free_89>=1+free_91 && E1>=0 && free_91>=1+free_90 && free_88>=2 ], cost: 1 43: f10 -> f5 : F'=1+R1, G'=D, H'=free_226, P'=free_229, Q_1'=free_225, R'=free_227, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, X1'=T, Y1'=T, Z1'=free_228, [ free_230>=2 && free_226>=2 && E1>=0 && O>=1+D && D>=1+O && Q_1==R && F==1 ], cost: 1 44: f10 -> f5 : F'=1+R1, G'=D, H'=free_232, P'=free_235, Q_1'=free_231, R'=free_233, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, X1'=T, Y1'=T, Z1'=free_234, [ free_236>=2 && free_232>=2 && E1>=0 && O>=1+D && Q_1==R && F==1 ], cost: 1 45: f10 -> f5 : F'=1+R1, G'=D, H'=free_238, P'=free_241, Q_1'=free_237, R'=free_239, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, X1'=T, Y1'=T, Z1'=free_240, [ free_242>=2 && free_238>=2 && E1>=0 && D>=1+O && Q_1==R && F==1 ], cost: 1 46: f10 -> f5 : F'=1+R1, G'=D, H'=free_244, P'=free_247, Q_1'=free_243, R'=free_245, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, X1'=T, Y1'=T, Z1'=free_246, [ free_248>=2 && free_244>=2 && E1>=0 && D>=1+O && O>=1+D && Q_1==R && F==1 ], cost: 1 23: f4 -> f5 : D'=O1, G'=O1, H'=free_140, O'=free_141, P1'=free_141, Q1_1'=M1, [ free_142>=1+M1 && N1>=0 && free_140>=2 && O1>=1+free_141 && free_141>=1+free_142 ], cost: 1 24: f4 -> f5 : D'=O1, G'=O1, H'=free_143, O'=free_144, P1'=free_144, Q1_1'=M1, [ free_145>=1+M1 && N1>=0 && free_143>=2 && O1>=1+free_144 && free_145>=1+free_144 ], cost: 1 25: f4 -> f5 : D'=O1, G'=O1, H'=free_146, O'=free_147, P1'=free_147, Q1_1'=M1, [ free_148>=1+M1 && N1>=0 && free_146>=2 && free_147>=1+O1 && free_147>=1+free_148 ], cost: 1 26: f4 -> f5 : D'=O1, G'=O1, H'=free_149, O'=free_150, P1'=free_150, Q1_1'=M1, [ free_151>=1+M1 && N1>=0 && free_149>=2 && free_150>=1+O1 && free_151>=1+free_150 ], cost: 1 27: f4 -> f5 : D'=O1, G'=O1, H'=free_152, O'=free_153, P1'=free_153, Q1_1'=M1, [ M1>=1+free_154 && N1>=0 && free_152>=2 && O1>=1+free_153 && free_153>=1+free_154 ], cost: 1 28: f4 -> f5 : D'=O1, G'=O1, H'=free_155, O'=free_156, P1'=free_156, Q1_1'=M1, [ M1>=1+free_157 && N1>=0 && free_155>=2 && O1>=1+free_156 && free_157>=1+free_156 ], cost: 1 29: f4 -> f5 : D'=O1, G'=O1, H'=free_158, O'=free_159, P1'=free_159, Q1_1'=M1, [ M1>=1+free_160 && N1>=0 && free_158>=2 && free_159>=1+O1 && free_159>=1+free_160 ], cost: 1 30: f4 -> f5 : D'=O1, G'=O1, H'=free_161, O'=free_162, P1'=free_162, Q1_1'=M1, [ M1>=1+free_163 && N1>=0 && free_161>=2 && free_162>=1+O1 && free_163>=1+free_162 ], cost: 1 31: f4 -> f16 : G'=free_165, H'=free_170, K'=free_164, O'=free_167, M1'=free_166, O1'=free_171, P1'=free_169, Q1_1'=free_168, [ N1>=0 && free_165>=1+free_167 && free_170>=2 && O1==M1 ], cost: 1 32: f4 -> f16 : G'=free_173, H'=free_178, K'=free_172, O'=free_175, M1'=free_174, O1'=free_179, P1'=free_177, Q1_1'=free_176, [ N1>=0 && free_175>=1+free_173 && free_178>=2 && O1==M1 ], cost: 1 33: f5 -> f5 : D'=O1, G'=O1, H'=free_181, O'=free_182, Z'=free_180, P1'=free_182, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ free_183>=1+M1 && R1>=0 && free_181>=2 && O1>=1+free_182 && free_182>=1+free_183 ], cost: 1 34: f5 -> f5 : D'=O1, G'=O1, H'=free_185, O'=free_186, Z'=free_184, P1'=free_186, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ free_187>=1+M1 && R1>=0 && free_185>=2 && O1>=1+free_186 && free_187>=1+free_186 ], cost: 1 35: f5 -> f5 : D'=O1, G'=O1, H'=free_189, O'=free_190, Z'=free_188, P1'=free_190, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ free_191>=1+M1 && R1>=0 && free_189>=2 && free_190>=1+O1 && free_190>=1+free_191 ], cost: 1 36: f5 -> f5 : D'=O1, G'=O1, H'=free_193, O'=free_194, Z'=free_192, P1'=free_194, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ free_195>=1+M1 && R1>=0 && free_193>=2 && free_194>=1+O1 && free_195>=1+free_194 ], cost: 1 37: f5 -> f5 : D'=O1, G'=O1, H'=free_197, O'=free_198, Z'=free_196, P1'=free_198, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ M1>=1+free_199 && R1>=0 && free_197>=2 && O1>=1+free_198 && free_198>=1+free_199 ], cost: 1 38: f5 -> f5 : D'=O1, G'=O1, H'=free_201, O'=free_202, Z'=free_200, P1'=free_202, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ M1>=1+free_203 && R1>=0 && free_201>=2 && O1>=1+free_202 && free_203>=1+free_202 ], cost: 1 39: f5 -> f5 : D'=O1, G'=O1, H'=free_205, O'=free_206, Z'=free_204, P1'=free_206, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ M1>=1+free_207 && R1>=0 && free_205>=2 && free_206>=1+O1 && free_206>=1+free_207 ], cost: 1 40: f5 -> f5 : D'=O1, G'=O1, H'=free_209, O'=free_210, Z'=free_208, P1'=free_210, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ M1>=1+free_211 && R1>=0 && free_209>=2 && free_210>=1+O1 && free_211>=1+free_210 ], cost: 1 41: f5 -> f16 : H'=free_213, K'=free_216, M1'=free_215, O1'=free_214, P1'=free_212, Q1_1'=free_217, [ free_213>=2 && R1>=0 && O1==M1 ], cost: 1 42: f15 -> f7 : A'=2, B'=free_221, C'=free_222, D'=free_219, G'=free_219, H'=free_221, Q'=free_219, L'=free_222, M'=free_222, N'=free_224, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 ], cost: 1 51: f15 -> f16 : A'=free_278, B'=free_280, C'=free_291, D'=U1, G'=U1, H'=free_274, Q'=free_286, J'=free_284, K'=free_277, L'=free_282, M'=free_283, N'=free_289, O'=U1, P'=free_275, Q_1'=free_281, R'=free_287, M1'=free_285, O1'=free_279, P1'=free_273, Q1_1'=free_290, U1'=free_276, V1'=free_288, [ 0>=free_294 && 0>=free_292 && 0>=free_274 && 0>=free_293 ], cost: 1 52: f15 -> f16 : A'=free_300, B'=free_302, C'=free_314, D'=N, G'=free_298, H'=1, Q'=free_308, J'=free_306, K'=free_299, L'=free_304, M'=free_305, N'=free_311, O'=free_297, P'=free_303, Q_1'=free_309, R'=free_295, M1'=free_313, O1'=free_307, P1'=free_301, Q1_1'=free_312, U1'=free_310, V1'=free_296, [ 0>=1 && free_298>=1+free_297 ], cost: 1 53: f15 -> f16 : A'=free_320, B'=free_322, C'=free_334, D'=N, G'=free_318, H'=1, Q'=free_328, J'=free_326, K'=free_319, L'=free_324, M'=free_325, N'=free_331, O'=free_317, P'=free_323, Q_1'=free_329, R'=free_315, M1'=free_333, O1'=free_327, P1'=free_321, Q1_1'=free_332, U1'=free_330, V1'=free_316, [ 0>=1 && free_317>=1+free_318 ], cost: 1 54: f15 -> f16 : A'=free_340, B'=free_342, C'=free_354, D'=N, G'=free_338, H'=1, Q'=free_348, J'=free_346, K'=free_339, L'=free_344, M'=free_345, N'=free_351, O'=free_337, P'=free_343, Q_1'=free_349, R'=free_335, M1'=free_353, O1'=free_347, P1'=free_341, Q1_1'=free_352, U1'=free_350, V1'=free_336, [ 0>=1 && free_338>=1+free_337 ], cost: 1 55: f15 -> f16 : A'=free_360, B'=free_362, C'=free_374, D'=N, G'=free_358, H'=1, Q'=free_368, J'=free_366, K'=free_359, L'=free_364, M'=free_365, N'=free_371, O'=free_357, P'=free_363, Q_1'=free_369, R'=free_355, M1'=free_373, O1'=free_367, P1'=free_361, Q1_1'=free_372, U1'=free_370, V1'=free_356, [ 0>=1 && free_357>=1+free_358 ], cost: 1 Removed unsatisfiable initial transitions: Start location: f15 2: f7 -> f7 : A'=1+A, C'=N, M'=N, N'=free_22, W'=free_23, X'=A, Y'=T, [ B>=1+A && A>=0 ], cost: 1 0: f7 -> f14 : A'=E, B'=free_9, C'=free_4, F'=0, G'=D, H'=free_1, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=C, P'=C, Q_1'=D, R'=C, S'=T, U'=free_5, V'=free_6, [ A>=B && A>=0 && C>=1+D && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 ], cost: 1 1: f7 -> f14 : A'=E, B'=free_20, C'=free_15, F'=0, G'=D, H'=free_12, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=C, P'=C, Q_1'=D, R'=C, S'=T, U'=free_16, V'=free_17, [ A>=B && A>=0 && D>=1+C && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 ], cost: 1 15: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_93, O'=free_95, P'=free_95, Z'=free_92, H1'=R, Q1'=free_94, J1'=T, K1'=1+F, L1'=-1+E, [ free_96>=1+free_97 && free_96>=1+free_94 && F>=0 && E>=0 && free_95>=1+free_96 && free_93>=2 ], cost: 1 16: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_99, O'=free_101, P'=free_101, Z'=free_98, H1'=R, Q1'=free_100, J1'=T, K1'=1+F, L1'=-1+E, [ free_102>=1+free_103 && free_102>=1+free_100 && F>=0 && E>=0 && free_102>=1+free_101 && free_99>=2 ], cost: 1 17: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_105, O'=free_107, P'=free_107, Z'=free_104, H1'=R, Q1'=free_106, J1'=T, K1'=1+F, L1'=-1+E, [ free_108>=1+free_109 && free_106>=1+free_108 && F>=0 && E>=0 && free_107>=1+free_108 && free_105>=2 ], cost: 1 18: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_111, O'=free_113, P'=free_113, Z'=free_110, H1'=R, Q1'=free_112, J1'=T, K1'=1+F, L1'=-1+E, [ free_114>=1+free_115 && free_112>=1+free_114 && F>=0 && E>=0 && free_114>=1+free_113 && free_111>=2 ], cost: 1 19: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_117, O'=free_119, P'=free_119, Z'=free_116, H1'=R, Q1'=free_118, J1'=T, K1'=1+F, L1'=-1+E, [ free_121>=1+free_120 && free_120>=1+free_118 && F>=0 && E>=0 && free_119>=1+free_120 && free_117>=2 ], cost: 1 20: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_123, O'=free_125, P'=free_125, Z'=free_122, H1'=R, Q1'=free_124, J1'=T, K1'=1+F, L1'=-1+E, [ free_127>=1+free_126 && free_126>=1+free_124 && F>=0 && E>=0 && free_126>=1+free_125 && free_123>=2 ], cost: 1 21: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_129, O'=free_131, P'=free_131, Z'=free_128, H1'=R, Q1'=free_130, J1'=T, K1'=1+F, L1'=-1+E, [ free_133>=1+free_132 && free_130>=1+free_132 && F>=0 && E>=0 && free_131>=1+free_132 && free_129>=2 ], cost: 1 22: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_135, O'=free_137, P'=free_137, Z'=free_134, H1'=R, Q1'=free_136, J1'=T, K1'=1+F, L1'=-1+E, [ free_139>=1+free_138 && free_136>=1+free_138 && F>=0 && E>=0 && free_138>=1+free_137 && free_135>=2 ], cost: 1 47: f14 -> f5 : F'=1+R1, G'=D, H'=free_250, P'=free_253, Q_1'=free_249, R'=free_251, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_252, [ free_254>=2 && free_250>=2 && E>=0 && F>=0 && O>=1+D && D>=1+O && Q_1==R ], cost: 1 48: f14 -> f5 : F'=1+R1, G'=D, H'=free_256, P'=free_259, Q_1'=free_255, R'=free_257, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_258, [ free_260>=2 && free_256>=2 && E>=0 && F>=0 && O>=1+D && Q_1==R ], cost: 1 49: f14 -> f5 : F'=1+R1, G'=D, H'=free_262, P'=free_265, Q_1'=free_261, R'=free_263, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_264, [ free_266>=2 && free_262>=2 && E>=0 && F>=0 && D>=1+O && Q_1==R ], cost: 1 50: f14 -> f5 : F'=1+R1, G'=D, H'=free_268, P'=free_271, Q_1'=free_267, R'=free_269, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_270, [ free_272>=2 && free_268>=2 && E>=0 && F>=0 && D>=1+O && O>=1+D && Q_1==R ], cost: 1 3: f9 -> f14 : D'=Q_1, F'=1, G'=Q_1, H'=free_25, O'=free_28, P'=free_28, Z'=free_24, A1'=1+E, B1'=T, C1'=free_26, D1'=free_27, E1'=E, [ free_30>=1+R && A>=0 && free_25>=2 && free_28>=1+free_30 && free_29>=free_25 && F==1 ], cost: 1 4: f9 -> f14 : D'=Q_1, F'=1, G'=Q_1, H'=free_32, O'=free_35, P'=free_35, Z'=free_31, A1'=1+E, B1'=T, C1'=free_33, D1'=free_34, E1'=E, [ free_37>=1+R && A>=0 && free_32>=2 && free_37>=1+free_35 && free_36>=free_32 && F==1 ], cost: 1 5: f9 -> f14 : D'=Q_1, F'=1, G'=Q_1, H'=free_39, O'=free_42, P'=free_42, Z'=free_38, A1'=1+E, B1'=T, C1'=free_40, D1'=free_41, E1'=E, [ R>=1+free_44 && A>=0 && free_39>=2 && free_42>=1+free_44 && free_43>=free_39 && F==1 ], cost: 1 6: f9 -> f14 : D'=Q_1, F'=1, G'=Q_1, H'=free_46, O'=free_49, P'=free_49, Z'=free_45, A1'=1+E, B1'=T, C1'=free_47, D1'=free_48, E1'=E, [ R>=1+free_51 && A>=0 && free_46>=2 && free_51>=1+free_49 && free_50>=free_46 && F==1 ], cost: 1 7: f10 -> f14 : D'=Q_1, G'=Q_1, H'=free_53, O'=free_55, P'=free_55, F1'=free_52, G1'=free_54, [ free_56>=1+R && free_56>=1+free_54 && E1>=0 && free_55>=1+free_56 && free_53>=2 ], cost: 1 8: f10 -> f14 : D'=Q_1, G'=Q_1, H'=free_58, O'=free_60, P'=free_60, F1'=free_57, G1'=free_59, [ free_61>=1+R && free_61>=1+free_59 && E1>=0 && free_61>=1+free_60 && free_58>=2 ], cost: 1 9: f10 -> f14 : D'=Q_1, G'=Q_1, H'=free_63, O'=free_65, P'=free_65, F1'=free_62, G1'=free_64, [ free_66>=1+R && free_64>=1+free_66 && E1>=0 && free_65>=1+free_66 && free_63>=2 ], cost: 1 10: f10 -> f14 : D'=Q_1, G'=Q_1, H'=free_68, O'=free_70, P'=free_70, F1'=free_67, G1'=free_69, [ free_71>=1+R && free_69>=1+free_71 && E1>=0 && free_71>=1+free_70 && free_68>=2 ], cost: 1 11: f10 -> f14 : D'=Q_1, G'=Q_1, H'=free_73, O'=free_75, P'=free_75, F1'=free_72, G1'=free_74, [ R>=1+free_76 && free_76>=1+free_74 && E1>=0 && free_75>=1+free_76 && free_73>=2 ], cost: 1 12: f10 -> f14 : D'=Q_1, G'=Q_1, H'=free_78, O'=free_80, P'=free_80, F1'=free_77, G1'=free_79, [ R>=1+free_81 && free_81>=1+free_79 && E1>=0 && free_81>=1+free_80 && free_78>=2 ], cost: 1 13: f10 -> f14 : D'=Q_1, G'=Q_1, H'=free_83, O'=free_85, P'=free_85, F1'=free_82, G1'=free_84, [ R>=1+free_86 && free_84>=1+free_86 && E1>=0 && free_85>=1+free_86 && free_83>=2 ], cost: 1 14: f10 -> f14 : D'=Q_1, G'=Q_1, H'=free_88, O'=free_90, P'=free_90, F1'=free_87, G1'=free_89, [ R>=1+free_91 && free_89>=1+free_91 && E1>=0 && free_91>=1+free_90 && free_88>=2 ], cost: 1 43: f10 -> f5 : F'=1+R1, G'=D, H'=free_226, P'=free_229, Q_1'=free_225, R'=free_227, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, X1'=T, Y1'=T, Z1'=free_228, [ free_230>=2 && free_226>=2 && E1>=0 && O>=1+D && D>=1+O && Q_1==R && F==1 ], cost: 1 44: f10 -> f5 : F'=1+R1, G'=D, H'=free_232, P'=free_235, Q_1'=free_231, R'=free_233, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, X1'=T, Y1'=T, Z1'=free_234, [ free_236>=2 && free_232>=2 && E1>=0 && O>=1+D && Q_1==R && F==1 ], cost: 1 45: f10 -> f5 : F'=1+R1, G'=D, H'=free_238, P'=free_241, Q_1'=free_237, R'=free_239, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, X1'=T, Y1'=T, Z1'=free_240, [ free_242>=2 && free_238>=2 && E1>=0 && D>=1+O && Q_1==R && F==1 ], cost: 1 46: f10 -> f5 : F'=1+R1, G'=D, H'=free_244, P'=free_247, Q_1'=free_243, R'=free_245, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, X1'=T, Y1'=T, Z1'=free_246, [ free_248>=2 && free_244>=2 && E1>=0 && D>=1+O && O>=1+D && Q_1==R && F==1 ], cost: 1 23: f4 -> f5 : D'=O1, G'=O1, H'=free_140, O'=free_141, P1'=free_141, Q1_1'=M1, [ free_142>=1+M1 && N1>=0 && free_140>=2 && O1>=1+free_141 && free_141>=1+free_142 ], cost: 1 24: f4 -> f5 : D'=O1, G'=O1, H'=free_143, O'=free_144, P1'=free_144, Q1_1'=M1, [ free_145>=1+M1 && N1>=0 && free_143>=2 && O1>=1+free_144 && free_145>=1+free_144 ], cost: 1 25: f4 -> f5 : D'=O1, G'=O1, H'=free_146, O'=free_147, P1'=free_147, Q1_1'=M1, [ free_148>=1+M1 && N1>=0 && free_146>=2 && free_147>=1+O1 && free_147>=1+free_148 ], cost: 1 26: f4 -> f5 : D'=O1, G'=O1, H'=free_149, O'=free_150, P1'=free_150, Q1_1'=M1, [ free_151>=1+M1 && N1>=0 && free_149>=2 && free_150>=1+O1 && free_151>=1+free_150 ], cost: 1 27: f4 -> f5 : D'=O1, G'=O1, H'=free_152, O'=free_153, P1'=free_153, Q1_1'=M1, [ M1>=1+free_154 && N1>=0 && free_152>=2 && O1>=1+free_153 && free_153>=1+free_154 ], cost: 1 28: f4 -> f5 : D'=O1, G'=O1, H'=free_155, O'=free_156, P1'=free_156, Q1_1'=M1, [ M1>=1+free_157 && N1>=0 && free_155>=2 && O1>=1+free_156 && free_157>=1+free_156 ], cost: 1 29: f4 -> f5 : D'=O1, G'=O1, H'=free_158, O'=free_159, P1'=free_159, Q1_1'=M1, [ M1>=1+free_160 && N1>=0 && free_158>=2 && free_159>=1+O1 && free_159>=1+free_160 ], cost: 1 30: f4 -> f5 : D'=O1, G'=O1, H'=free_161, O'=free_162, P1'=free_162, Q1_1'=M1, [ M1>=1+free_163 && N1>=0 && free_161>=2 && free_162>=1+O1 && free_163>=1+free_162 ], cost: 1 31: f4 -> f16 : G'=free_165, H'=free_170, K'=free_164, O'=free_167, M1'=free_166, O1'=free_171, P1'=free_169, Q1_1'=free_168, [ N1>=0 && free_165>=1+free_167 && free_170>=2 && O1==M1 ], cost: 1 32: f4 -> f16 : G'=free_173, H'=free_178, K'=free_172, O'=free_175, M1'=free_174, O1'=free_179, P1'=free_177, Q1_1'=free_176, [ N1>=0 && free_175>=1+free_173 && free_178>=2 && O1==M1 ], cost: 1 33: f5 -> f5 : D'=O1, G'=O1, H'=free_181, O'=free_182, Z'=free_180, P1'=free_182, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ free_183>=1+M1 && R1>=0 && free_181>=2 && O1>=1+free_182 && free_182>=1+free_183 ], cost: 1 34: f5 -> f5 : D'=O1, G'=O1, H'=free_185, O'=free_186, Z'=free_184, P1'=free_186, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ free_187>=1+M1 && R1>=0 && free_185>=2 && O1>=1+free_186 && free_187>=1+free_186 ], cost: 1 35: f5 -> f5 : D'=O1, G'=O1, H'=free_189, O'=free_190, Z'=free_188, P1'=free_190, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ free_191>=1+M1 && R1>=0 && free_189>=2 && free_190>=1+O1 && free_190>=1+free_191 ], cost: 1 36: f5 -> f5 : D'=O1, G'=O1, H'=free_193, O'=free_194, Z'=free_192, P1'=free_194, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ free_195>=1+M1 && R1>=0 && free_193>=2 && free_194>=1+O1 && free_195>=1+free_194 ], cost: 1 37: f5 -> f5 : D'=O1, G'=O1, H'=free_197, O'=free_198, Z'=free_196, P1'=free_198, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ M1>=1+free_199 && R1>=0 && free_197>=2 && O1>=1+free_198 && free_198>=1+free_199 ], cost: 1 38: f5 -> f5 : D'=O1, G'=O1, H'=free_201, O'=free_202, Z'=free_200, P1'=free_202, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ M1>=1+free_203 && R1>=0 && free_201>=2 && O1>=1+free_202 && free_203>=1+free_202 ], cost: 1 39: f5 -> f5 : D'=O1, G'=O1, H'=free_205, O'=free_206, Z'=free_204, P1'=free_206, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ M1>=1+free_207 && R1>=0 && free_205>=2 && free_206>=1+O1 && free_206>=1+free_207 ], cost: 1 40: f5 -> f5 : D'=O1, G'=O1, H'=free_209, O'=free_210, Z'=free_208, P1'=free_210, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ M1>=1+free_211 && R1>=0 && free_209>=2 && free_210>=1+O1 && free_211>=1+free_210 ], cost: 1 41: f5 -> f16 : H'=free_213, K'=free_216, M1'=free_215, O1'=free_214, P1'=free_212, Q1_1'=free_217, [ free_213>=2 && R1>=0 && O1==M1 ], cost: 1 42: f15 -> f7 : A'=2, B'=free_221, C'=free_222, D'=free_219, G'=free_219, H'=free_221, Q'=free_219, L'=free_222, M'=free_222, N'=free_224, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 ], cost: 1 51: f15 -> f16 : A'=free_278, B'=free_280, C'=free_291, D'=U1, G'=U1, H'=free_274, Q'=free_286, J'=free_284, K'=free_277, L'=free_282, M'=free_283, N'=free_289, O'=U1, P'=free_275, Q_1'=free_281, R'=free_287, M1'=free_285, O1'=free_279, P1'=free_273, Q1_1'=free_290, U1'=free_276, V1'=free_288, [ 0>=free_294 && 0>=free_292 && 0>=free_274 && 0>=free_293 ], cost: 1 Simplified the transitions: Start location: f15 2: f7 -> f7 : A'=1+A, C'=N, M'=N, N'=free_22, W'=free_23, X'=A, Y'=T, [ B>=1+A && A>=0 ], cost: 1 0: f7 -> f14 : A'=E, B'=free_9, C'=free_4, F'=0, G'=D, H'=free_1, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=C, P'=C, Q_1'=D, R'=C, S'=T, U'=free_5, V'=free_6, [ A>=B && A>=0 && C>=1+D && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 ], cost: 1 1: f7 -> f14 : A'=E, B'=free_20, C'=free_15, F'=0, G'=D, H'=free_12, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=C, P'=C, Q_1'=D, R'=C, S'=T, U'=free_16, V'=free_17, [ A>=B && A>=0 && D>=1+C && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 ], cost: 1 15: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_93, O'=free_95, P'=free_95, Z'=free_92, H1'=R, Q1'=free_94, J1'=T, K1'=1+F, L1'=-1+E, [ F>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1 16: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_99, O'=free_101, P'=free_101, Z'=free_98, H1'=R, Q1'=free_100, J1'=T, K1'=1+F, L1'=-1+E, [ F>=0 && E>=0 && free_99>=2 ], cost: 1 17: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_105, O'=free_107, P'=free_107, Z'=free_104, H1'=R, Q1'=free_106, J1'=T, K1'=1+F, L1'=-1+E, [ F>=0 && E>=0 && free_105>=2 ], cost: 1 18: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_111, O'=free_113, P'=free_113, Z'=free_110, H1'=R, Q1'=free_112, J1'=T, K1'=1+F, L1'=-1+E, [ F>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1 19: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_117, O'=free_119, P'=free_119, Z'=free_116, H1'=R, Q1'=free_118, J1'=T, K1'=1+F, L1'=-1+E, [ F>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1 20: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_123, O'=free_125, P'=free_125, Z'=free_122, H1'=R, Q1'=free_124, J1'=T, K1'=1+F, L1'=-1+E, [ F>=0 && E>=0 && free_123>=2 ], cost: 1 21: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_129, O'=free_131, P'=free_131, Z'=free_128, H1'=R, Q1'=free_130, J1'=T, K1'=1+F, L1'=-1+E, [ F>=0 && E>=0 && free_129>=2 ], cost: 1 22: f14 -> f14 : D'=Q_1, E'=-1+E, F'=1+F, G'=Q_1, H'=free_135, O'=free_137, P'=free_137, Z'=free_134, H1'=R, Q1'=free_136, J1'=T, K1'=1+F, L1'=-1+E, [ F>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1 47: f14 -> f5 : F'=1+R1, G'=D, H'=free_250, P'=free_253, Q_1'=free_249, R'=free_251, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_252, [ free_250>=2 && E>=0 && F>=0 && O>=1+D && D>=1+O && Q_1==R ], cost: 1 48: f14 -> f5 : F'=1+R1, G'=D, H'=free_256, P'=free_259, Q_1'=free_255, R'=free_257, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_258, [ free_256>=2 && E>=0 && F>=0 && O>=1+D && Q_1==R ], cost: 1 49: f14 -> f5 : F'=1+R1, G'=D, H'=free_262, P'=free_265, Q_1'=free_261, R'=free_263, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_264, [ free_262>=2 && E>=0 && F>=0 && D>=1+O && Q_1==R ], cost: 1 50: f14 -> f5 : F'=1+R1, G'=D, H'=free_268, P'=free_271, Q_1'=free_267, R'=free_269, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_270, [ free_268>=2 && E>=0 && F>=0 && D>=1+O && O>=1+D && Q_1==R ], cost: 1 33: f5 -> f5 : D'=O1, G'=O1, H'=free_181, O'=free_182, Z'=free_180, P1'=free_182, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ R1>=0 && free_181>=2 && O1>=1+free_182 && 1+M1<=-1+free_182 ], cost: 1 34: f5 -> f5 : D'=O1, G'=O1, H'=free_185, O'=free_186, Z'=free_184, P1'=free_186, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ R1>=0 && free_185>=2 && O1>=1+free_186 ], cost: 1 35: f5 -> f5 : D'=O1, G'=O1, H'=free_189, O'=free_190, Z'=free_188, P1'=free_190, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ R1>=0 && free_189>=2 && free_190>=1+O1 && 1+M1<=-1+free_190 ], cost: 1 36: f5 -> f5 : D'=O1, G'=O1, H'=free_193, O'=free_194, Z'=free_192, P1'=free_194, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ R1>=0 && free_193>=2 && free_194>=1+O1 ], cost: 1 37: f5 -> f5 : D'=O1, G'=O1, H'=free_197, O'=free_198, Z'=free_196, P1'=free_198, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ R1>=0 && free_197>=2 && O1>=1+free_198 ], cost: 1 38: f5 -> f5 : D'=O1, G'=O1, H'=free_201, O'=free_202, Z'=free_200, P1'=free_202, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ R1>=0 && free_201>=2 && O1>=1+free_202 && 1+free_202<=-1+M1 ], cost: 1 39: f5 -> f5 : D'=O1, G'=O1, H'=free_205, O'=free_206, Z'=free_204, P1'=free_206, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ R1>=0 && free_205>=2 && free_206>=1+O1 ], cost: 1 40: f5 -> f5 : D'=O1, G'=O1, H'=free_209, O'=free_210, Z'=free_208, P1'=free_210, Q1_1'=M1, R1'=-1+R1, S1'=T, T1'=-1+R1, [ R1>=0 && free_209>=2 && free_210>=1+O1 && 1+free_210<=-1+M1 ], cost: 1 42: f15 -> f7 : A'=2, B'=free_221, C'=free_222, D'=free_219, G'=free_219, H'=free_221, Q'=free_219, L'=free_222, M'=free_222, N'=free_224, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 ], cost: 1 Eliminating 1 self-loops for location f7 Self-Loop 2 has the metering function: B-A, resulting in the new transition 56. Removing the self-loops: 2. Eliminating 8 self-loops for location f14 Self-Loop 15 has the metering function: 1+E, resulting in the new transition 57. Self-Loop 16 has the metering function: 1+E, resulting in the new transition 58. Self-Loop 17 has the metering function: 1+E, resulting in the new transition 59. Self-Loop 18 has the metering function: 1+E, resulting in the new transition 60. Self-Loop 19 has the metering function: 1+E, resulting in the new transition 61. Self-Loop 20 has the metering function: 1+E, resulting in the new transition 62. Self-Loop 21 has the metering function: 1+E, resulting in the new transition 63. Self-Loop 22 has the metering function: 1+E, resulting in the new transition 64. Removing the self-loops: 15 16 17 18 19 20 21 22. Eliminating 8 self-loops for location f5 Self-Loop 33 has the metering function: 1+R1, resulting in the new transition 65. Self-Loop 34 has the metering function: 1+R1, resulting in the new transition 66. Self-Loop 35 has the metering function: 1+R1, resulting in the new transition 67. Self-Loop 36 has the metering function: 1+R1, resulting in the new transition 68. Self-Loop 37 has the metering function: 1+R1, resulting in the new transition 69. Self-Loop 38 has the metering function: 1+R1, resulting in the new transition 70. Self-Loop 39 has the metering function: 1+R1, resulting in the new transition 71. Self-Loop 40 has the metering function: 1+R1, resulting in the new transition 72. Removing the self-loops: 33 34 35 36 37 38 39 40. Removed all Self-loops using metering functions (where possible): Start location: f15 56: f7 -> [8] : A'=B, C'=free_22, M'=free_22, N'=free_22, W'=free_23, X'=-1+B, Y'=T, [ B>=1+A && A>=0 ], cost: B-A 57: f14 -> [9] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_93, O'=free_95, P'=free_95, Z'=free_92, H1'=R, Q1'=free_94, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E 58: f14 -> [9] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_99, O'=free_101, P'=free_101, Z'=free_98, H1'=R, Q1'=free_100, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_99>=2 ], cost: 1+E 59: f14 -> [9] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_105, O'=free_107, P'=free_107, Z'=free_104, H1'=R, Q1'=free_106, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_105>=2 ], cost: 1+E 60: f14 -> [9] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_111, O'=free_113, P'=free_113, Z'=free_110, H1'=R, Q1'=free_112, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E 61: f14 -> [9] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_117, O'=free_119, P'=free_119, Z'=free_116, H1'=R, Q1'=free_118, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E 62: f14 -> [9] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_123, O'=free_125, P'=free_125, Z'=free_122, H1'=R, Q1'=free_124, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_123>=2 ], cost: 1+E 63: f14 -> [9] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_129, O'=free_131, P'=free_131, Z'=free_128, H1'=R, Q1'=free_130, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_129>=2 ], cost: 1+E 64: f14 -> [9] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_135, O'=free_137, P'=free_137, Z'=free_134, H1'=R, Q1'=free_136, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E 65: f5 -> [10] : D'=O1, G'=O1, H'=free_181, O'=free_182, Z'=free_180, P1'=free_182, Q1_1'=M1, R1'=-1, S1'=T, T1'=-1, [ R1>=0 && free_181>=2 && O1>=1+free_182 && 1+M1<=-1+free_182 ], cost: 1+R1 66: f5 -> [10] : D'=O1, G'=O1, H'=free_185, O'=free_186, Z'=free_184, P1'=free_186, Q1_1'=M1, R1'=-1, S1'=T, T1'=-1, [ R1>=0 && free_185>=2 && O1>=1+free_186 ], cost: 1+R1 67: f5 -> [10] : D'=O1, G'=O1, H'=free_189, O'=free_190, Z'=free_188, P1'=free_190, Q1_1'=M1, R1'=-1, S1'=T, T1'=-1, [ R1>=0 && free_189>=2 && free_190>=1+O1 && 1+M1<=-1+free_190 ], cost: 1+R1 68: f5 -> [10] : D'=O1, G'=O1, H'=free_193, O'=free_194, Z'=free_192, P1'=free_194, Q1_1'=M1, R1'=-1, S1'=T, T1'=-1, [ R1>=0 && free_193>=2 && free_194>=1+O1 ], cost: 1+R1 69: f5 -> [10] : D'=O1, G'=O1, H'=free_197, O'=free_198, Z'=free_196, P1'=free_198, Q1_1'=M1, R1'=-1, S1'=T, T1'=-1, [ R1>=0 && free_197>=2 && O1>=1+free_198 ], cost: 1+R1 70: f5 -> [10] : D'=O1, G'=O1, H'=free_201, O'=free_202, Z'=free_200, P1'=free_202, Q1_1'=M1, R1'=-1, S1'=T, T1'=-1, [ R1>=0 && free_201>=2 && O1>=1+free_202 && 1+free_202<=-1+M1 ], cost: 1+R1 71: f5 -> [10] : D'=O1, G'=O1, H'=free_205, O'=free_206, Z'=free_204, P1'=free_206, Q1_1'=M1, R1'=-1, S1'=T, T1'=-1, [ R1>=0 && free_205>=2 && free_206>=1+O1 ], cost: 1+R1 72: f5 -> [10] : D'=O1, G'=O1, H'=free_209, O'=free_210, Z'=free_208, P1'=free_210, Q1_1'=M1, R1'=-1, S1'=T, T1'=-1, [ R1>=0 && free_209>=2 && free_210>=1+O1 && 1+free_210<=-1+M1 ], cost: 1+R1 42: f15 -> f7 : A'=2, B'=free_221, C'=free_222, D'=free_219, G'=free_219, H'=free_221, Q'=free_219, L'=free_222, M'=free_222, N'=free_224, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 ], cost: 1 0: [8] -> f14 : A'=E, B'=free_9, C'=free_4, F'=0, G'=D, H'=free_1, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=C, P'=C, Q_1'=D, R'=C, S'=T, U'=free_5, V'=free_6, [ A>=B && A>=0 && C>=1+D && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 ], cost: 1 1: [8] -> f14 : A'=E, B'=free_20, C'=free_15, F'=0, G'=D, H'=free_12, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=C, P'=C, Q_1'=D, R'=C, S'=T, U'=free_16, V'=free_17, [ A>=B && A>=0 && D>=1+C && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 ], cost: 1 47: [9] -> f5 : F'=1+R1, G'=D, H'=free_250, P'=free_253, Q_1'=free_249, R'=free_251, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_252, [ free_250>=2 && E>=0 && F>=0 && O>=1+D && D>=1+O && Q_1==R ], cost: 1 48: [9] -> f5 : F'=1+R1, G'=D, H'=free_256, P'=free_259, Q_1'=free_255, R'=free_257, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_258, [ free_256>=2 && E>=0 && F>=0 && O>=1+D && Q_1==R ], cost: 1 49: [9] -> f5 : F'=1+R1, G'=D, H'=free_262, P'=free_265, Q_1'=free_261, R'=free_263, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_264, [ free_262>=2 && E>=0 && F>=0 && D>=1+O && Q_1==R ], cost: 1 50: [9] -> f5 : F'=1+R1, G'=D, H'=free_268, P'=free_271, Q_1'=free_267, R'=free_269, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_270, [ free_268>=2 && E>=0 && F>=0 && D>=1+O && O>=1+D && Q_1==R ], cost: 1 Applied simple chaining: Start location: f15 57: f14 -> [9] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_93, O'=free_95, P'=free_95, Z'=free_92, H1'=R, Q1'=free_94, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E 58: f14 -> [9] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_99, O'=free_101, P'=free_101, Z'=free_98, H1'=R, Q1'=free_100, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_99>=2 ], cost: 1+E 59: f14 -> [9] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_105, O'=free_107, P'=free_107, Z'=free_104, H1'=R, Q1'=free_106, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_105>=2 ], cost: 1+E 60: f14 -> [9] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_111, O'=free_113, P'=free_113, Z'=free_110, H1'=R, Q1'=free_112, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E 61: f14 -> [9] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_117, O'=free_119, P'=free_119, Z'=free_116, H1'=R, Q1'=free_118, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E 62: f14 -> [9] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_123, O'=free_125, P'=free_125, Z'=free_122, H1'=R, Q1'=free_124, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_123>=2 ], cost: 1+E 63: f14 -> [9] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_129, O'=free_131, P'=free_131, Z'=free_128, H1'=R, Q1'=free_130, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_129>=2 ], cost: 1+E 64: f14 -> [9] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_135, O'=free_137, P'=free_137, Z'=free_134, H1'=R, Q1'=free_136, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E 65: f5 -> [10] : D'=O1, G'=O1, H'=free_181, O'=free_182, Z'=free_180, P1'=free_182, Q1_1'=M1, R1'=-1, S1'=T, T1'=-1, [ R1>=0 && free_181>=2 && O1>=1+free_182 && 1+M1<=-1+free_182 ], cost: 1+R1 66: f5 -> [10] : D'=O1, G'=O1, H'=free_185, O'=free_186, Z'=free_184, P1'=free_186, Q1_1'=M1, R1'=-1, S1'=T, T1'=-1, [ R1>=0 && free_185>=2 && O1>=1+free_186 ], cost: 1+R1 67: f5 -> [10] : D'=O1, G'=O1, H'=free_189, O'=free_190, Z'=free_188, P1'=free_190, Q1_1'=M1, R1'=-1, S1'=T, T1'=-1, [ R1>=0 && free_189>=2 && free_190>=1+O1 && 1+M1<=-1+free_190 ], cost: 1+R1 68: f5 -> [10] : D'=O1, G'=O1, H'=free_193, O'=free_194, Z'=free_192, P1'=free_194, Q1_1'=M1, R1'=-1, S1'=T, T1'=-1, [ R1>=0 && free_193>=2 && free_194>=1+O1 ], cost: 1+R1 69: f5 -> [10] : D'=O1, G'=O1, H'=free_197, O'=free_198, Z'=free_196, P1'=free_198, Q1_1'=M1, R1'=-1, S1'=T, T1'=-1, [ R1>=0 && free_197>=2 && O1>=1+free_198 ], cost: 1+R1 70: f5 -> [10] : D'=O1, G'=O1, H'=free_201, O'=free_202, Z'=free_200, P1'=free_202, Q1_1'=M1, R1'=-1, S1'=T, T1'=-1, [ R1>=0 && free_201>=2 && O1>=1+free_202 && 1+free_202<=-1+M1 ], cost: 1+R1 71: f5 -> [10] : D'=O1, G'=O1, H'=free_205, O'=free_206, Z'=free_204, P1'=free_206, Q1_1'=M1, R1'=-1, S1'=T, T1'=-1, [ R1>=0 && free_205>=2 && free_206>=1+O1 ], cost: 1+R1 72: f5 -> [10] : D'=O1, G'=O1, H'=free_209, O'=free_210, Z'=free_208, P1'=free_210, Q1_1'=M1, R1'=-1, S1'=T, T1'=-1, [ R1>=0 && free_209>=2 && free_210>=1+O1 && 1+free_210<=-1+M1 ], cost: 1+R1 42: f15 -> [8] : A'=free_221, B'=free_221, C'=free_22, D'=free_219, G'=free_219, H'=free_221, Q'=free_219, L'=free_222, M'=free_22, N'=free_22, W'=free_23, X'=-1+free_221, Y'=T, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 ], cost: -1+free_221 0: [8] -> f14 : A'=E, B'=free_9, C'=free_4, F'=0, G'=D, H'=free_1, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=C, P'=C, Q_1'=D, R'=C, S'=T, U'=free_5, V'=free_6, [ A>=B && A>=0 && C>=1+D && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 ], cost: 1 1: [8] -> f14 : A'=E, B'=free_20, C'=free_15, F'=0, G'=D, H'=free_12, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=C, P'=C, Q_1'=D, R'=C, S'=T, U'=free_16, V'=free_17, [ A>=B && A>=0 && D>=1+C && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 ], cost: 1 47: [9] -> f5 : F'=1+R1, G'=D, H'=free_250, P'=free_253, Q_1'=free_249, R'=free_251, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_252, [ free_250>=2 && E>=0 && F>=0 && O>=1+D && D>=1+O && Q_1==R ], cost: 1 48: [9] -> f5 : F'=1+R1, G'=D, H'=free_256, P'=free_259, Q_1'=free_255, R'=free_257, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_258, [ free_256>=2 && E>=0 && F>=0 && O>=1+D && Q_1==R ], cost: 1 49: [9] -> f5 : F'=1+R1, G'=D, H'=free_262, P'=free_265, Q_1'=free_261, R'=free_263, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_264, [ free_262>=2 && E>=0 && F>=0 && D>=1+O && Q_1==R ], cost: 1 50: [9] -> f5 : F'=1+R1, G'=D, H'=free_268, P'=free_271, Q_1'=free_267, R'=free_269, M1'=O, N1'=R1, O1'=D, P1'=O, Q1_1'=O, Y1'=T, Z1'=free_270, [ free_268>=2 && E>=0 && F>=0 && D>=1+O && O>=1+D && Q_1==R ], cost: 1 Applied chaining over branches and pruning: Start location: f15 75: f14 -> [11] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_93, O'=free_95, P'=free_95, Z'=free_92, H1'=R, Q1'=free_94, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E 76: f14 -> [12] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_93, O'=free_95, P'=free_95, Z'=free_92, H1'=R, Q1'=free_94, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E 77: f14 -> [13] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_93, O'=free_95, P'=free_95, Z'=free_92, H1'=R, Q1'=free_94, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E 78: f14 -> [14] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_93, O'=free_95, P'=free_95, Z'=free_92, H1'=R, Q1'=free_94, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E 79: f14 -> [15] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_99, O'=free_101, P'=free_101, Z'=free_98, H1'=R, Q1'=free_100, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_99>=2 ], cost: 1+E 80: f14 -> [16] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_99, O'=free_101, P'=free_101, Z'=free_98, H1'=R, Q1'=free_100, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_99>=2 ], cost: 1+E 81: f14 -> [17] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_99, O'=free_101, P'=free_101, Z'=free_98, H1'=R, Q1'=free_100, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_99>=2 ], cost: 1+E 82: f14 -> [18] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_99, O'=free_101, P'=free_101, Z'=free_98, H1'=R, Q1'=free_100, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_99>=2 ], cost: 1+E 83: f14 -> [19] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_105, O'=free_107, P'=free_107, Z'=free_104, H1'=R, Q1'=free_106, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_105>=2 ], cost: 1+E 84: f14 -> [20] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_105, O'=free_107, P'=free_107, Z'=free_104, H1'=R, Q1'=free_106, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_105>=2 ], cost: 1+E 85: f14 -> [21] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_105, O'=free_107, P'=free_107, Z'=free_104, H1'=R, Q1'=free_106, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_105>=2 ], cost: 1+E 86: f14 -> [22] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_105, O'=free_107, P'=free_107, Z'=free_104, H1'=R, Q1'=free_106, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_105>=2 ], cost: 1+E 87: f14 -> [23] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_111, O'=free_113, P'=free_113, Z'=free_110, H1'=R, Q1'=free_112, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E 88: f14 -> [24] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_111, O'=free_113, P'=free_113, Z'=free_110, H1'=R, Q1'=free_112, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E 89: f14 -> [25] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_111, O'=free_113, P'=free_113, Z'=free_110, H1'=R, Q1'=free_112, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E 90: f14 -> [26] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_111, O'=free_113, P'=free_113, Z'=free_110, H1'=R, Q1'=free_112, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E 91: f14 -> [27] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_117, O'=free_119, P'=free_119, Z'=free_116, H1'=R, Q1'=free_118, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E 92: f14 -> [28] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_117, O'=free_119, P'=free_119, Z'=free_116, H1'=R, Q1'=free_118, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E 93: f14 -> [29] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_117, O'=free_119, P'=free_119, Z'=free_116, H1'=R, Q1'=free_118, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E 94: f14 -> [30] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_117, O'=free_119, P'=free_119, Z'=free_116, H1'=R, Q1'=free_118, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E 95: f14 -> [31] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_123, O'=free_125, P'=free_125, Z'=free_122, H1'=R, Q1'=free_124, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_123>=2 ], cost: 1+E 96: f14 -> [32] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_123, O'=free_125, P'=free_125, Z'=free_122, H1'=R, Q1'=free_124, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_123>=2 ], cost: 1+E 97: f14 -> [33] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_123, O'=free_125, P'=free_125, Z'=free_122, H1'=R, Q1'=free_124, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_123>=2 ], cost: 1+E 98: f14 -> [34] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_123, O'=free_125, P'=free_125, Z'=free_122, H1'=R, Q1'=free_124, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_123>=2 ], cost: 1+E 99: f14 -> [35] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_129, O'=free_131, P'=free_131, Z'=free_128, H1'=R, Q1'=free_130, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_129>=2 ], cost: 1+E 100: f14 -> [36] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_129, O'=free_131, P'=free_131, Z'=free_128, H1'=R, Q1'=free_130, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_129>=2 ], cost: 1+E 101: f14 -> [37] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_129, O'=free_131, P'=free_131, Z'=free_128, H1'=R, Q1'=free_130, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_129>=2 ], cost: 1+E 102: f14 -> [38] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_129, O'=free_131, P'=free_131, Z'=free_128, H1'=R, Q1'=free_130, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_129>=2 ], cost: 1+E 103: f14 -> [39] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_135, O'=free_137, P'=free_137, Z'=free_134, H1'=R, Q1'=free_136, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E 104: f14 -> [40] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_135, O'=free_137, P'=free_137, Z'=free_134, H1'=R, Q1'=free_136, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E 105: f14 -> [41] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_135, O'=free_137, P'=free_137, Z'=free_134, H1'=R, Q1'=free_136, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E 106: f14 -> [42] : D'=Q_1, E'=-1, F'=1+E+F, G'=Q_1, H'=free_135, O'=free_137, P'=free_137, Z'=free_134, H1'=R, Q1'=free_136, J1'=T, K1'=1+E+F, L1'=-1, [ F>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E 73: f15 -> f14 : A'=E, B'=free_9, C'=free_4, D'=free_219, F'=0, G'=free_219, H'=free_1, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_22, P'=free_22, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 ], cost: free_221 74: f15 -> f14 : A'=E, B'=free_20, C'=free_15, D'=free_219, F'=0, G'=free_219, H'=free_12, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_22, P'=free_22, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 ], cost: free_221 Applied chaining over branches and pruning: Start location: f15 107: f15 -> [11] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_93, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_95, P'=free_95, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_92, H1'=free_22, Q1'=free_94, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E+free_221 139: f15 -> [11] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_93, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_95, P'=free_95, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_92, H1'=free_22, Q1'=free_94, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E+free_221 108: f15 -> [12] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_93, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_95, P'=free_95, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_92, H1'=free_22, Q1'=free_94, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E+free_221 140: f15 -> [12] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_93, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_95, P'=free_95, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_92, H1'=free_22, Q1'=free_94, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E+free_221 109: f15 -> [13] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_93, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_95, P'=free_95, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_92, H1'=free_22, Q1'=free_94, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E+free_221 141: f15 -> [13] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_93, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_95, P'=free_95, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_92, H1'=free_22, Q1'=free_94, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E+free_221 110: f15 -> [14] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_93, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_95, P'=free_95, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_92, H1'=free_22, Q1'=free_94, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E+free_221 142: f15 -> [14] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_93, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_95, P'=free_95, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_92, H1'=free_22, Q1'=free_94, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E+free_221 111: f15 -> [15] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_99, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_101, P'=free_101, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_98, H1'=free_22, Q1'=free_100, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_99>=2 ], cost: 1+E+free_221 143: f15 -> [15] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_99, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_101, P'=free_101, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_98, H1'=free_22, Q1'=free_100, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_99>=2 ], cost: 1+E+free_221 112: f15 -> [16] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_99, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_101, P'=free_101, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_98, H1'=free_22, Q1'=free_100, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_99>=2 ], cost: 1+E+free_221 144: f15 -> [16] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_99, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_101, P'=free_101, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_98, H1'=free_22, Q1'=free_100, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_99>=2 ], cost: 1+E+free_221 113: f15 -> [17] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_99, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_101, P'=free_101, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_98, H1'=free_22, Q1'=free_100, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_99>=2 ], cost: 1+E+free_221 145: f15 -> [17] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_99, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_101, P'=free_101, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_98, H1'=free_22, Q1'=free_100, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_99>=2 ], cost: 1+E+free_221 114: f15 -> [18] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_99, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_101, P'=free_101, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_98, H1'=free_22, Q1'=free_100, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_99>=2 ], cost: 1+E+free_221 146: f15 -> [18] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_99, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_101, P'=free_101, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_98, H1'=free_22, Q1'=free_100, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_99>=2 ], cost: 1+E+free_221 115: f15 -> [19] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_105, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_107, P'=free_107, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_104, H1'=free_22, Q1'=free_106, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_105>=2 ], cost: 1+E+free_221 147: f15 -> [19] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_105, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_107, P'=free_107, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_104, H1'=free_22, Q1'=free_106, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_105>=2 ], cost: 1+E+free_221 116: f15 -> [20] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_105, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_107, P'=free_107, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_104, H1'=free_22, Q1'=free_106, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_105>=2 ], cost: 1+E+free_221 148: f15 -> [20] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_105, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_107, P'=free_107, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_104, H1'=free_22, Q1'=free_106, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_105>=2 ], cost: 1+E+free_221 117: f15 -> [21] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_105, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_107, P'=free_107, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_104, H1'=free_22, Q1'=free_106, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_105>=2 ], cost: 1+E+free_221 149: f15 -> [21] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_105, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_107, P'=free_107, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_104, H1'=free_22, Q1'=free_106, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_105>=2 ], cost: 1+E+free_221 118: f15 -> [22] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_105, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_107, P'=free_107, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_104, H1'=free_22, Q1'=free_106, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_105>=2 ], cost: 1+E+free_221 150: f15 -> [22] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_105, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_107, P'=free_107, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_104, H1'=free_22, Q1'=free_106, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_105>=2 ], cost: 1+E+free_221 119: f15 -> [23] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_111, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_113, P'=free_113, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_110, H1'=free_22, Q1'=free_112, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E+free_221 151: f15 -> [23] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_111, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_113, P'=free_113, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_110, H1'=free_22, Q1'=free_112, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E+free_221 120: f15 -> [24] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_111, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_113, P'=free_113, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_110, H1'=free_22, Q1'=free_112, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E+free_221 152: f15 -> [24] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_111, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_113, P'=free_113, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_110, H1'=free_22, Q1'=free_112, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E+free_221 121: f15 -> [25] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_111, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_113, P'=free_113, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_110, H1'=free_22, Q1'=free_112, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E+free_221 153: f15 -> [25] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_111, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_113, P'=free_113, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_110, H1'=free_22, Q1'=free_112, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E+free_221 122: f15 -> [26] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_111, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_113, P'=free_113, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_110, H1'=free_22, Q1'=free_112, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E+free_221 154: f15 -> [26] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_111, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_113, P'=free_113, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_110, H1'=free_22, Q1'=free_112, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E+free_221 123: f15 -> [27] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_117, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_119, P'=free_119, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_116, H1'=free_22, Q1'=free_118, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E+free_221 155: f15 -> [27] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_117, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_119, P'=free_119, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_116, H1'=free_22, Q1'=free_118, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E+free_221 124: f15 -> [28] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_117, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_119, P'=free_119, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_116, H1'=free_22, Q1'=free_118, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E+free_221 156: f15 -> [28] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_117, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_119, P'=free_119, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_116, H1'=free_22, Q1'=free_118, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E+free_221 125: f15 -> [29] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_117, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_119, P'=free_119, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_116, H1'=free_22, Q1'=free_118, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E+free_221 157: f15 -> [29] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_117, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_119, P'=free_119, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_116, H1'=free_22, Q1'=free_118, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E+free_221 126: f15 -> [30] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_117, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_119, P'=free_119, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_116, H1'=free_22, Q1'=free_118, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E+free_221 158: f15 -> [30] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_117, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_119, P'=free_119, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_116, H1'=free_22, Q1'=free_118, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E+free_221 127: f15 -> [31] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_123, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_125, P'=free_125, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_122, H1'=free_22, Q1'=free_124, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_123>=2 ], cost: 1+E+free_221 159: f15 -> [31] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_123, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_125, P'=free_125, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_122, H1'=free_22, Q1'=free_124, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_123>=2 ], cost: 1+E+free_221 128: f15 -> [32] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_123, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_125, P'=free_125, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_122, H1'=free_22, Q1'=free_124, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_123>=2 ], cost: 1+E+free_221 160: f15 -> [32] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_123, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_125, P'=free_125, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_122, H1'=free_22, Q1'=free_124, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_123>=2 ], cost: 1+E+free_221 129: f15 -> [33] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_123, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_125, P'=free_125, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_122, H1'=free_22, Q1'=free_124, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_123>=2 ], cost: 1+E+free_221 161: f15 -> [33] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_123, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_125, P'=free_125, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_122, H1'=free_22, Q1'=free_124, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_123>=2 ], cost: 1+E+free_221 130: f15 -> [34] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_123, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_125, P'=free_125, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_122, H1'=free_22, Q1'=free_124, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_123>=2 ], cost: 1+E+free_221 162: f15 -> [34] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_123, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_125, P'=free_125, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_122, H1'=free_22, Q1'=free_124, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_123>=2 ], cost: 1+E+free_221 131: f15 -> [35] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_129, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_131, P'=free_131, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_128, H1'=free_22, Q1'=free_130, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_129>=2 ], cost: 1+E+free_221 163: f15 -> [35] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_129, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_131, P'=free_131, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_128, H1'=free_22, Q1'=free_130, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_129>=2 ], cost: 1+E+free_221 132: f15 -> [36] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_129, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_131, P'=free_131, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_128, H1'=free_22, Q1'=free_130, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_129>=2 ], cost: 1+E+free_221 164: f15 -> [36] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_129, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_131, P'=free_131, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_128, H1'=free_22, Q1'=free_130, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_129>=2 ], cost: 1+E+free_221 133: f15 -> [37] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_129, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_131, P'=free_131, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_128, H1'=free_22, Q1'=free_130, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_129>=2 ], cost: 1+E+free_221 165: f15 -> [37] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_129, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_131, P'=free_131, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_128, H1'=free_22, Q1'=free_130, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_129>=2 ], cost: 1+E+free_221 134: f15 -> [38] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_129, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_131, P'=free_131, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_128, H1'=free_22, Q1'=free_130, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_129>=2 ], cost: 1+E+free_221 166: f15 -> [38] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_129, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_131, P'=free_131, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_128, H1'=free_22, Q1'=free_130, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_129>=2 ], cost: 1+E+free_221 135: f15 -> [39] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_135, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_137, P'=free_137, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_134, H1'=free_22, Q1'=free_136, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E+free_221 167: f15 -> [39] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_135, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_137, P'=free_137, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_134, H1'=free_22, Q1'=free_136, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E+free_221 136: f15 -> [40] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_135, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_137, P'=free_137, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_134, H1'=free_22, Q1'=free_136, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E+free_221 168: f15 -> [40] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_135, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_137, P'=free_137, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_134, H1'=free_22, Q1'=free_136, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E+free_221 137: f15 -> [41] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_135, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_137, P'=free_137, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_134, H1'=free_22, Q1'=free_136, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E+free_221 169: f15 -> [41] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_135, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_137, P'=free_137, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_134, H1'=free_22, Q1'=free_136, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E+free_221 138: f15 -> [42] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_135, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_137, P'=free_137, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_134, H1'=free_22, Q1'=free_136, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E+free_221 170: f15 -> [42] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_135, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_137, P'=free_137, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_134, H1'=free_22, Q1'=free_136, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E+free_221 Final control flow graph problem, now checking costs for infinitely many models: Start location: f15 107: f15 -> [11] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_93, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_95, P'=free_95, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_92, H1'=free_22, Q1'=free_94, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E+free_221 139: f15 -> [11] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_93, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_95, P'=free_95, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_92, H1'=free_22, Q1'=free_94, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E+free_221 108: f15 -> [12] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_93, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_95, P'=free_95, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_92, H1'=free_22, Q1'=free_94, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E+free_221 140: f15 -> [12] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_93, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_95, P'=free_95, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_92, H1'=free_22, Q1'=free_94, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E+free_221 109: f15 -> [13] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_93, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_95, P'=free_95, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_92, H1'=free_22, Q1'=free_94, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E+free_221 141: f15 -> [13] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_93, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_95, P'=free_95, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_92, H1'=free_22, Q1'=free_94, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E+free_221 110: f15 -> [14] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_93, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_95, P'=free_95, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_92, H1'=free_22, Q1'=free_94, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E+free_221 142: f15 -> [14] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_93, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_95, P'=free_95, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_92, H1'=free_22, Q1'=free_94, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 ], cost: 1+E+free_221 111: f15 -> [15] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_99, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_101, P'=free_101, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_98, H1'=free_22, Q1'=free_100, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_99>=2 ], cost: 1+E+free_221 143: f15 -> [15] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_99, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_101, P'=free_101, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_98, H1'=free_22, Q1'=free_100, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_99>=2 ], cost: 1+E+free_221 112: f15 -> [16] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_99, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_101, P'=free_101, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_98, H1'=free_22, Q1'=free_100, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_99>=2 ], cost: 1+E+free_221 144: f15 -> [16] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_99, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_101, P'=free_101, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_98, H1'=free_22, Q1'=free_100, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_99>=2 ], cost: 1+E+free_221 113: f15 -> [17] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_99, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_101, P'=free_101, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_98, H1'=free_22, Q1'=free_100, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_99>=2 ], cost: 1+E+free_221 145: f15 -> [17] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_99, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_101, P'=free_101, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_98, H1'=free_22, Q1'=free_100, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_99>=2 ], cost: 1+E+free_221 114: f15 -> [18] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_99, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_101, P'=free_101, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_98, H1'=free_22, Q1'=free_100, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_99>=2 ], cost: 1+E+free_221 146: f15 -> [18] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_99, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_101, P'=free_101, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_98, H1'=free_22, Q1'=free_100, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_99>=2 ], cost: 1+E+free_221 115: f15 -> [19] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_105, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_107, P'=free_107, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_104, H1'=free_22, Q1'=free_106, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_105>=2 ], cost: 1+E+free_221 147: f15 -> [19] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_105, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_107, P'=free_107, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_104, H1'=free_22, Q1'=free_106, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_105>=2 ], cost: 1+E+free_221 116: f15 -> [20] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_105, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_107, P'=free_107, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_104, H1'=free_22, Q1'=free_106, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_105>=2 ], cost: 1+E+free_221 148: f15 -> [20] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_105, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_107, P'=free_107, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_104, H1'=free_22, Q1'=free_106, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_105>=2 ], cost: 1+E+free_221 117: f15 -> [21] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_105, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_107, P'=free_107, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_104, H1'=free_22, Q1'=free_106, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_105>=2 ], cost: 1+E+free_221 149: f15 -> [21] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_105, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_107, P'=free_107, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_104, H1'=free_22, Q1'=free_106, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_105>=2 ], cost: 1+E+free_221 118: f15 -> [22] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_105, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_107, P'=free_107, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_104, H1'=free_22, Q1'=free_106, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_105>=2 ], cost: 1+E+free_221 150: f15 -> [22] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_105, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_107, P'=free_107, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_104, H1'=free_22, Q1'=free_106, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_105>=2 ], cost: 1+E+free_221 119: f15 -> [23] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_111, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_113, P'=free_113, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_110, H1'=free_22, Q1'=free_112, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E+free_221 151: f15 -> [23] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_111, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_113, P'=free_113, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_110, H1'=free_22, Q1'=free_112, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E+free_221 120: f15 -> [24] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_111, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_113, P'=free_113, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_110, H1'=free_22, Q1'=free_112, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E+free_221 152: f15 -> [24] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_111, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_113, P'=free_113, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_110, H1'=free_22, Q1'=free_112, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E+free_221 121: f15 -> [25] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_111, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_113, P'=free_113, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_110, H1'=free_22, Q1'=free_112, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E+free_221 153: f15 -> [25] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_111, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_113, P'=free_113, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_110, H1'=free_22, Q1'=free_112, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E+free_221 122: f15 -> [26] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_111, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_113, P'=free_113, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_110, H1'=free_22, Q1'=free_112, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E+free_221 154: f15 -> [26] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_111, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_113, P'=free_113, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_110, H1'=free_22, Q1'=free_112, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_111>=2 && 1+free_113<=-1+free_112 ], cost: 1+E+free_221 123: f15 -> [27] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_117, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_119, P'=free_119, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_116, H1'=free_22, Q1'=free_118, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E+free_221 155: f15 -> [27] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_117, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_119, P'=free_119, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_116, H1'=free_22, Q1'=free_118, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E+free_221 124: f15 -> [28] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_117, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_119, P'=free_119, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_116, H1'=free_22, Q1'=free_118, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E+free_221 156: f15 -> [28] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_117, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_119, P'=free_119, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_116, H1'=free_22, Q1'=free_118, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E+free_221 125: f15 -> [29] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_117, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_119, P'=free_119, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_116, H1'=free_22, Q1'=free_118, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E+free_221 157: f15 -> [29] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_117, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_119, P'=free_119, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_116, H1'=free_22, Q1'=free_118, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E+free_221 126: f15 -> [30] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_117, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_119, P'=free_119, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_116, H1'=free_22, Q1'=free_118, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E+free_221 158: f15 -> [30] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_117, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_119, P'=free_119, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_116, H1'=free_22, Q1'=free_118, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_117>=2 && 1+free_118<=-1+free_119 ], cost: 1+E+free_221 127: f15 -> [31] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_123, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_125, P'=free_125, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_122, H1'=free_22, Q1'=free_124, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_123>=2 ], cost: 1+E+free_221 159: f15 -> [31] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_123, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_125, P'=free_125, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_122, H1'=free_22, Q1'=free_124, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_123>=2 ], cost: 1+E+free_221 128: f15 -> [32] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_123, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_125, P'=free_125, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_122, H1'=free_22, Q1'=free_124, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_123>=2 ], cost: 1+E+free_221 160: f15 -> [32] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_123, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_125, P'=free_125, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_122, H1'=free_22, Q1'=free_124, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_123>=2 ], cost: 1+E+free_221 129: f15 -> [33] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_123, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_125, P'=free_125, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_122, H1'=free_22, Q1'=free_124, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_123>=2 ], cost: 1+E+free_221 161: f15 -> [33] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_123, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_125, P'=free_125, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_122, H1'=free_22, Q1'=free_124, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_123>=2 ], cost: 1+E+free_221 130: f15 -> [34] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_123, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_125, P'=free_125, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_122, H1'=free_22, Q1'=free_124, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_123>=2 ], cost: 1+E+free_221 162: f15 -> [34] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_123, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_125, P'=free_125, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_122, H1'=free_22, Q1'=free_124, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_123>=2 ], cost: 1+E+free_221 131: f15 -> [35] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_129, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_131, P'=free_131, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_128, H1'=free_22, Q1'=free_130, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_129>=2 ], cost: 1+E+free_221 163: f15 -> [35] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_129, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_131, P'=free_131, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_128, H1'=free_22, Q1'=free_130, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_129>=2 ], cost: 1+E+free_221 132: f15 -> [36] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_129, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_131, P'=free_131, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_128, H1'=free_22, Q1'=free_130, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_129>=2 ], cost: 1+E+free_221 164: f15 -> [36] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_129, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_131, P'=free_131, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_128, H1'=free_22, Q1'=free_130, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_129>=2 ], cost: 1+E+free_221 133: f15 -> [37] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_129, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_131, P'=free_131, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_128, H1'=free_22, Q1'=free_130, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_129>=2 ], cost: 1+E+free_221 165: f15 -> [37] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_129, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_131, P'=free_131, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_128, H1'=free_22, Q1'=free_130, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_129>=2 ], cost: 1+E+free_221 134: f15 -> [38] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_129, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_131, P'=free_131, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_128, H1'=free_22, Q1'=free_130, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_129>=2 ], cost: 1+E+free_221 166: f15 -> [38] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_129, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_131, P'=free_131, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_128, H1'=free_22, Q1'=free_130, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_129>=2 ], cost: 1+E+free_221 135: f15 -> [39] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_135, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_137, P'=free_137, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_134, H1'=free_22, Q1'=free_136, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E+free_221 167: f15 -> [39] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_135, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_137, P'=free_137, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_134, H1'=free_22, Q1'=free_136, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E+free_221 136: f15 -> [40] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_135, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_137, P'=free_137, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_134, H1'=free_22, Q1'=free_136, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E+free_221 168: f15 -> [40] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_135, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_137, P'=free_137, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_134, H1'=free_22, Q1'=free_136, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E+free_221 137: f15 -> [41] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_135, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_137, P'=free_137, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_134, H1'=free_22, Q1'=free_136, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E+free_221 169: f15 -> [41] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_135, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_137, P'=free_137, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_134, H1'=free_22, Q1'=free_136, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E+free_221 138: f15 -> [42] : A'=E, B'=free_9, C'=free_4, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_135, Q'=free, J'=free_8, K'=free_10, L'=free_3, M'=free_7, N'=free_2, O'=free_137, P'=free_137, Q_1'=free_219, R'=free_22, S'=T, U'=free_5, V'=free_6, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_134, H1'=free_22, Q1'=free_136, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E+free_221 170: f15 -> [42] : A'=E, B'=free_20, C'=free_15, D'=free_219, E'=-1, F'=1+E, G'=free_219, H'=free_135, Q'=free_11, J'=free_19, K'=free_21, L'=free_14, M'=free_18, N'=free_13, O'=free_137, P'=free_137, Q_1'=free_219, R'=free_22, S'=T, U'=free_16, V'=free_17, W'=free_23, X'=-1+free_221, Y'=T, Z'=free_134, H1'=free_22, Q1'=free_136, J1'=T, K1'=1+E, L1'=-1, U1'=free_223, V1'=free_218, W1'=free_220, [ free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_219>=1+free_22 && free_12>=2 && free_16>=free_12 && E>=free_12 && F==0 && 0>=0 && E>=0 && free_135>=2 && 1+free_137<=-1+free_136 ], cost: 1+E+free_221 Computing complexity for remaining 64 transitions. Found configuration with infinitely models for cost: 1+E+free_221 and guard: free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95: free_22: Pos, free_95: Pos, E: Pos, free_219: Pos, free_93: Pos, F: Both, free_1: Const, free_94: Pos, free_221: Pos, free_5: Pos, where: free_22 > free_219 free_95 > free_94 Found new complexity INF, because: Found infinity configuration. The final runtime is determined by this resulting transition: Final Guard: free_221>=2 && free_221>=3 && 2>=0 && free_221>=free_221 && free_221>=0 && free_22>=1+free_219 && free_1>=2 && free_5>=free_1 && E>=free_1 && F==0 && 0>=0 && E>=0 && free_93>=2 && 1+free_94<=-1+free_95 Final Cost: 1+E+free_221 Obtained the following complexity w.r.t. the length of the input n: Complexity class: INF Complexity value: INF WORST_CASE(INF,?)