Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f21
      2: f13 -> f13 : A'=1+A, C'=K, J'=K, K'=free_19, P'=free_18, Q_1'=A, [ B>=1+A && A>=0 ], cost: 1
      0: f13 -> f20 : A'=D, B'=free_5, C'=free_7, E'=0, F'=free_8, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=C, M'=C, N'=C, O'=free_2, [ A>=B && A>=0 && free_8>=2 && 0>=1+C && free_2>=free_8 && D>=free_8 && E==0 ], cost: 1
      1: f13 -> f20 : A'=D, B'=free_14, C'=free_16, E'=0, F'=free_17, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=C, M'=C, N'=C, O'=free_11, [ A>=B && A>=0 && free_17>=2 && C>=1 && free_11>=free_17 && D>=free_17 && E==0 ], cost: 1
     17: f20 -> f20 : D'=-1+D, E'=1+E, F'=free_77, L'=free_75, M'=free_75, R'=free_76, Z'=N, A1'=free_74, B1'=1+E, C1'=-1+D, [ E>=0 && D>=0 && free_77>=2 && 0>=1+free_78 && 0>=1+free_75 && 0>=1+free_74 ], cost: 1
     18: f20 -> f20 : D'=-1+D, E'=1+E, F'=free_82, L'=free_80, M'=free_80, R'=free_81, Z'=N, A1'=free_79, B1'=1+E, C1'=-1+D, [ E>=0 && D>=0 && free_82>=2 && 0>=1+free_83 && 0>=1+free_80 && free_79>=1 ], cost: 1
     19: f20 -> f20 : D'=-1+D, E'=1+E, F'=free_87, L'=free_85, M'=free_85, R'=free_86, Z'=N, A1'=free_84, B1'=1+E, C1'=-1+D, [ E>=0 && D>=0 && free_87>=2 && 0>=1+free_88 && free_85>=1 && 0>=1+free_84 ], cost: 1
     20: f20 -> f20 : D'=-1+D, E'=1+E, F'=free_92, L'=free_90, M'=free_90, R'=free_91, Z'=N, A1'=free_89, B1'=1+E, C1'=-1+D, [ E>=0 && D>=0 && free_92>=2 && 0>=1+free_93 && free_90>=1 && free_89>=1 ], cost: 1
     21: f20 -> f20 : D'=-1+D, E'=1+E, F'=free_97, L'=free_95, M'=free_95, R'=free_96, Z'=N, A1'=free_94, B1'=1+E, C1'=-1+D, [ E>=0 && D>=0 && free_97>=2 && free_98>=1 && 0>=1+free_95 && 0>=1+free_94 ], cost: 1
     22: f20 -> f20 : D'=-1+D, E'=1+E, F'=free_102, L'=free_100, M'=free_100, R'=free_101, Z'=N, A1'=free_99, B1'=1+E, C1'=-1+D, [ E>=0 && D>=0 && free_102>=2 && free_103>=1 && 0>=1+free_100 && free_99>=1 ], cost: 1
     23: f20 -> f20 : D'=-1+D, E'=1+E, F'=free_107, L'=free_105, M'=free_105, R'=free_106, Z'=N, A1'=free_104, B1'=1+E, C1'=-1+D, [ E>=0 && D>=0 && free_107>=2 && free_108>=1 && free_105>=1 && 0>=1+free_104 ], cost: 1
     24: f20 -> f20 : D'=-1+D, E'=1+E, F'=free_112, L'=free_110, M'=free_110, R'=free_111, Z'=N, A1'=free_109, B1'=1+E, C1'=-1+D, [ E>=0 && D>=0 && free_112>=2 && free_113>=1 && free_110>=1 && free_109>=1 ], cost: 1
     15: f20 -> f11 : F'=free_72, M'=L, N'=L, X'=E, Y'=0, [ E>=0 && D>=0 && free_72>=2 && 0>=1+L && X==E && N==0 && Y==0 ], cost: 1
     16: f20 -> f11 : F'=free_73, M'=L, N'=L, X'=E, Y'=0, [ E>=0 && D>=0 && free_73>=2 && L>=1 && X==E && N==0 && Y==0 ], cost: 1
      3: f16 -> f20 : E'=1, F'=free_23, L'=free_21, M'=free_21, R'=free_22, S'=1+D, T'=free_20, U'=D, [ A>=0 && free_23>=2 && 0>=1+N && free_24>=free_23 && 0>=1+free_21 && E==1 ], cost: 1
      4: f16 -> f20 : E'=1, F'=free_28, L'=free_26, M'=free_26, R'=free_27, S'=1+D, T'=free_25, U'=D, [ A>=0 && free_28>=2 && 0>=1+N && free_29>=free_28 && free_26>=1 && E==1 ], cost: 1
      5: f16 -> f20 : E'=1, F'=free_33, L'=free_31, M'=free_31, R'=free_32, S'=1+D, T'=free_30, U'=D, [ A>=0 && free_33>=2 && N>=1 && free_34>=free_33 && 0>=1+free_31 && E==1 ], cost: 1
      6: f16 -> f20 : E'=1, F'=free_38, L'=free_36, M'=free_36, R'=free_37, S'=1+D, T'=free_35, U'=D, [ A>=0 && free_38>=2 && N>=1 && free_39>=free_38 && free_36>=1 && E==1 ], cost: 1
      7: f17 -> f20 : F'=free_43, L'=free_41, M'=free_41, V'=free_42, W'=free_40, [ U>=0 && free_43>=2 && 0>=1+N && 0>=1+free_41 && 0>=1+free_40 ], cost: 1
      8: f17 -> f20 : F'=free_47, L'=free_45, M'=free_45, V'=free_46, W'=free_44, [ U>=0 && free_47>=2 && 0>=1+N && 0>=1+free_45 && free_44>=1 ], cost: 1
      9: f17 -> f20 : F'=free_51, L'=free_49, M'=free_49, V'=free_50, W'=free_48, [ U>=0 && free_51>=2 && 0>=1+N && free_49>=1 && 0>=1+free_48 ], cost: 1
     10: f17 -> f20 : F'=free_55, L'=free_53, M'=free_53, V'=free_54, W'=free_52, [ U>=0 && free_55>=2 && 0>=1+N && free_53>=1 && free_52>=1 ], cost: 1
     11: f17 -> f20 : F'=free_59, L'=free_57, M'=free_57, V'=free_58, W'=free_56, [ U>=0 && free_59>=2 && N>=1 && 0>=1+free_57 && 0>=1+free_56 ], cost: 1
     12: f17 -> f20 : F'=free_63, L'=free_61, M'=free_61, V'=free_62, W'=free_60, [ U>=0 && free_63>=2 && N>=1 && 0>=1+free_61 && free_60>=1 ], cost: 1
     13: f17 -> f20 : F'=free_67, L'=free_65, M'=free_65, V'=free_66, W'=free_64, [ U>=0 && free_67>=2 && N>=1 && free_65>=1 && 0>=1+free_64 ], cost: 1
     14: f17 -> f20 : F'=free_71, L'=free_69, M'=free_69, V'=free_70, W'=free_68, [ U>=0 && free_71>=2 && N>=1 && free_69>=1 && free_68>=1 ], cost: 1
     61: f17 -> f11 : E'=1+X, F'=free_276, L'=free_274, M'=free_274, N'=L, R'=free_275, Y'=1, D1'=X, V1'=free_273, [ free_277>=2 && free_276>=2 && U>=0 && 0>=1+L && 0>=1+free_274 && N==0 && E==1 && Y==1 ], cost: 1
     62: f17 -> f11 : E'=1+X, F'=free_281, L'=free_279, M'=free_279, N'=L, R'=free_280, Y'=1, D1'=X, V1'=free_278, [ free_282>=2 && free_281>=2 && U>=0 && 0>=1+L && free_279>=1 && N==0 && E==1 && Y==1 ], cost: 1
     63: f17 -> f11 : E'=1+X, F'=free_286, L'=free_284, M'=free_284, N'=L, R'=free_285, Y'=1, D1'=X, V1'=free_283, [ free_287>=2 && free_286>=2 && U>=0 && L>=1 && 0>=1+free_284 && N==0 && E==1 && Y==1 ], cost: 1
     64: f17 -> f11 : E'=1+X, F'=free_291, L'=free_289, M'=free_289, N'=L, R'=free_290, Y'=1, D1'=X, V1'=free_288, [ free_292>=2 && free_291>=2 && U>=0 && L>=1 && free_289>=1 && N==0 && E==1 && Y==1 ], cost: 1
     33: f11 -> f11 : F'=free_149, L'=free_147, M'=free_147, R'=free_148, X'=-1+X, Y'=1+Y, G1'=N, H1'=free_146, Q1'=1+Y, J1'=-1+X, [ Y>=0 && X>=0 && free_149>=2 && 0>=1+free_150 && 0>=1+free_147 && 0>=1+free_146 ], cost: 1
     34: f11 -> f11 : F'=free_154, L'=free_152, M'=free_152, R'=free_153, X'=-1+X, Y'=1+Y, G1'=N, H1'=free_151, Q1'=1+Y, J1'=-1+X, [ Y>=0 && X>=0 && free_154>=2 && 0>=1+free_155 && 0>=1+free_152 && free_151>=1 ], cost: 1
     35: f11 -> f11 : F'=free_159, L'=free_157, M'=free_157, R'=free_158, X'=-1+X, Y'=1+Y, G1'=N, H1'=free_156, Q1'=1+Y, J1'=-1+X, [ Y>=0 && X>=0 && free_159>=2 && 0>=1+free_160 && free_157>=1 && 0>=1+free_156 ], cost: 1
     36: f11 -> f11 : F'=free_164, L'=free_162, M'=free_162, R'=free_163, X'=-1+X, Y'=1+Y, G1'=N, H1'=free_161, Q1'=1+Y, J1'=-1+X, [ Y>=0 && X>=0 && free_164>=2 && 0>=1+free_165 && free_162>=1 && free_161>=1 ], cost: 1
     37: f11 -> f11 : F'=free_169, L'=free_167, M'=free_167, R'=free_168, X'=-1+X, Y'=1+Y, G1'=N, H1'=free_166, Q1'=1+Y, J1'=-1+X, [ Y>=0 && X>=0 && free_169>=2 && free_170>=1 && 0>=1+free_167 && 0>=1+free_166 ], cost: 1
     38: f11 -> f11 : F'=free_174, L'=free_172, M'=free_172, R'=free_173, X'=-1+X, Y'=1+Y, G1'=N, H1'=free_171, Q1'=1+Y, J1'=-1+X, [ Y>=0 && X>=0 && free_174>=2 && free_175>=1 && 0>=1+free_172 && free_171>=1 ], cost: 1
     39: f11 -> f11 : F'=free_179, L'=free_177, M'=free_177, R'=free_178, X'=-1+X, Y'=1+Y, G1'=N, H1'=free_176, Q1'=1+Y, J1'=-1+X, [ Y>=0 && X>=0 && free_179>=2 && free_180>=1 && free_177>=1 && 0>=1+free_176 ], cost: 1
     40: f11 -> f11 : F'=free_184, L'=free_182, M'=free_182, R'=free_183, X'=-1+X, Y'=1+Y, G1'=N, H1'=free_181, Q1'=1+Y, J1'=-1+X, [ Y>=0 && X>=0 && free_184>=2 && free_185>=1 && free_182>=1 && free_181>=1 ], cost: 1
     70: f11 -> f5 : F'=free_333, M'=free_331, N'=free_332, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_334>=2 && free_333>=2 && X>=0 && Y>=0 && L>=1 && 0>=1+L && N==0 ], cost: 1
     71: f11 -> f5 : F'=free_337, M'=free_335, N'=free_336, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_338>=2 && free_337>=2 && X>=0 && Y>=0 && L>=1 && N==0 ], cost: 1
     72: f11 -> f5 : F'=free_341, M'=free_339, N'=free_340, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_342>=2 && free_341>=2 && X>=0 && Y>=0 && 0>=1+L && N==0 ], cost: 1
     73: f11 -> f5 : F'=free_345, M'=free_343, N'=free_344, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_346>=2 && free_345>=2 && X>=0 && Y>=0 && 0>=1+L && L>=1 && N==0 ], cost: 1
     25: f7 -> f11 : F'=free_117, L'=free_115, M'=free_115, E1'=free_116, F1'=free_114, [ D1>=0 && free_117>=2 && 0>=1+N && 0>=1+free_115 && 0>=1+free_114 ], cost: 1
     26: f7 -> f11 : F'=free_121, L'=free_119, M'=free_119, E1'=free_120, F1'=free_118, [ D1>=0 && free_121>=2 && 0>=1+N && 0>=1+free_119 && free_118>=1 ], cost: 1
     27: f7 -> f11 : F'=free_125, L'=free_123, M'=free_123, E1'=free_124, F1'=free_122, [ D1>=0 && free_125>=2 && 0>=1+N && free_123>=1 && 0>=1+free_122 ], cost: 1
     28: f7 -> f11 : F'=free_129, L'=free_127, M'=free_127, E1'=free_128, F1'=free_126, [ D1>=0 && free_129>=2 && 0>=1+N && free_127>=1 && free_126>=1 ], cost: 1
     29: f7 -> f11 : F'=free_133, L'=free_131, M'=free_131, E1'=free_132, F1'=free_130, [ D1>=0 && free_133>=2 && N>=1 && 0>=1+free_131 && 0>=1+free_130 ], cost: 1
     30: f7 -> f11 : F'=free_137, L'=free_135, M'=free_135, E1'=free_136, F1'=free_134, [ D1>=0 && free_137>=2 && N>=1 && 0>=1+free_135 && free_134>=1 ], cost: 1
     31: f7 -> f11 : F'=free_141, L'=free_139, M'=free_139, E1'=free_140, F1'=free_138, [ D1>=0 && free_141>=2 && N>=1 && free_139>=1 && 0>=1+free_138 ], cost: 1
     32: f7 -> f11 : F'=free_145, L'=free_143, M'=free_143, E1'=free_144, F1'=free_142, [ D1>=0 && free_145>=2 && N>=1 && free_143>=1 && free_142>=1 ], cost: 1
     66: f7 -> f5 : F'=free_317, M'=free_315, N'=free_316, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_318>=2 && free_317>=2 && D1>=0 && L>=1 && 0>=1+L && N==0 && Y==1 ], cost: 1
     67: f7 -> f5 : F'=free_321, M'=free_319, N'=free_320, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_322>=2 && free_321>=2 && D1>=0 && L>=1 && N==0 && Y==1 ], cost: 1
     68: f7 -> f5 : F'=free_325, M'=free_323, N'=free_324, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_326>=2 && free_325>=2 && D1>=0 && 0>=1+L && N==0 && Y==1 ], cost: 1
     69: f7 -> f5 : F'=free_329, M'=free_327, N'=free_328, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_330>=2 && free_329>=2 && D1>=0 && 0>=1+L && L>=1 && N==0 && Y==1 ], cost: 1
     41: f4 -> f5 : F'=free_187, L'=free_186, M1'=0, N1'=free_186, O1'=0, P1'=free_186, Q1_1'=K1, [ free_188>=1+K1 && L1>=0 && free_187>=2 && free_186>=1+free_188 && 0>=1+free_186 && M1==0 ], cost: 1
     42: f4 -> f5 : F'=free_190, L'=free_189, M1'=0, N1'=free_189, O1'=0, P1'=free_189, Q1_1'=K1, [ free_191>=1+K1 && L1>=0 && free_190>=2 && free_189>=1+free_191 && free_189>=1 && M1==0 ], cost: 1
     43: f4 -> f5 : F'=free_193, L'=free_192, M1'=0, N1'=free_192, O1'=0, P1'=free_192, Q1_1'=K1, [ free_194>=1+K1 && L1>=0 && free_193>=2 && free_194>=1+free_192 && 0>=1+free_192 && M1==0 ], cost: 1
     44: f4 -> f5 : F'=free_196, L'=free_195, M1'=0, N1'=free_195, O1'=0, P1'=free_195, Q1_1'=K1, [ free_197>=1+K1 && L1>=0 && free_196>=2 && free_197>=1+free_195 && free_195>=1 && M1==0 ], cost: 1
     45: f4 -> f5 : F'=free_199, L'=free_198, M1'=0, N1'=free_198, O1'=0, P1'=free_198, Q1_1'=K1, [ K1>=1+free_200 && L1>=0 && free_199>=2 && free_198>=1+free_200 && 0>=1+free_198 && M1==0 ], cost: 1
     46: f4 -> f5 : F'=free_202, L'=free_201, M1'=0, N1'=free_201, O1'=0, P1'=free_201, Q1_1'=K1, [ K1>=1+free_203 && L1>=0 && free_202>=2 && free_201>=1+free_203 && free_201>=1 && M1==0 ], cost: 1
     47: f4 -> f5 : F'=free_205, L'=free_204, M1'=0, N1'=free_204, O1'=0, P1'=free_204, Q1_1'=K1, [ K1>=1+free_206 && L1>=0 && free_205>=2 && free_206>=1+free_204 && 0>=1+free_204 && M1==0 ], cost: 1
     48: f4 -> f5 : F'=free_208, L'=free_207, M1'=0, N1'=free_207, O1'=0, P1'=free_207, Q1_1'=K1, [ K1>=1+free_209 && L1>=0 && free_208>=2 && free_209>=1+free_207 && free_207>=1 && M1==0 ], cost: 1
     49: f4 -> f22 : F'=free_218, H'=free_215, L'=free_217, K1'=free_213, M1'=free_210, N1'=free_211, O1'=free_214, P1'=free_216, Q1_1'=free_212, [ L1>=0 && 0>=1+free_217 && free_218>=2 && M1==K1 ], cost: 1
     50: f4 -> f22 : F'=free_227, H'=free_224, L'=free_226, K1'=free_222, M1'=free_219, N1'=free_220, O1'=free_223, P1'=free_225, Q1_1'=free_221, [ L1>=0 && free_226>=1 && free_227>=2 && M1==K1 ], cost: 1
     51: f5 -> f5 : F'=free_230, L'=free_228, R'=free_229, M1'=0, N1'=free_228, O1'=0, P1'=free_228, Q1_1'=K1, R1'=-1+R1, S1'=-1+R1, [ free_231>=1+K1 && R1>=0 && free_230>=2 && free_228>=1+free_231 && 0>=1+free_228 && M1==0 ], cost: 1
     52: f5 -> f5 : F'=free_234, L'=free_232, R'=free_233, M1'=0, N1'=free_232, O1'=0, P1'=free_232, Q1_1'=K1, R1'=-1+R1, S1'=-1+R1, [ free_235>=1+K1 && R1>=0 && free_234>=2 && free_232>=1+free_235 && free_232>=1 && M1==0 ], cost: 1
     53: f5 -> f5 : F'=free_238, L'=free_236, R'=free_237, M1'=0, N1'=free_236, O1'=0, P1'=free_236, Q1_1'=K1, R1'=-1+R1, S1'=-1+R1, [ free_239>=1+K1 && R1>=0 && free_238>=2 && free_239>=1+free_236 && 0>=1+free_236 && M1==0 ], cost: 1
     54: f5 -> f5 : F'=free_242, L'=free_240, R'=free_241, M1'=0, N1'=free_240, O1'=0, P1'=free_240, Q1_1'=K1, R1'=-1+R1, S1'=-1+R1, [ free_243>=1+K1 && R1>=0 && free_242>=2 && free_243>=1+free_240 && free_240>=1 && M1==0 ], cost: 1
     55: f5 -> f5 : F'=free_246, L'=free_244, R'=free_245, M1'=0, N1'=free_244, O1'=0, P1'=free_244, Q1_1'=K1, R1'=-1+R1, S1'=-1+R1, [ K1>=1+free_247 && R1>=0 && free_246>=2 && free_244>=1+free_247 && 0>=1+free_244 && M1==0 ], cost: 1
     56: f5 -> f5 : F'=free_250, L'=free_248, R'=free_249, M1'=0, N1'=free_248, O1'=0, P1'=free_248, Q1_1'=K1, R1'=-1+R1, S1'=-1+R1, [ K1>=1+free_251 && R1>=0 && free_250>=2 && free_248>=1+free_251 && free_248>=1 && M1==0 ], cost: 1
     57: f5 -> f5 : F'=free_254, L'=free_252, R'=free_253, M1'=0, N1'=free_252, O1'=0, P1'=free_252, Q1_1'=K1, R1'=-1+R1, S1'=-1+R1, [ K1>=1+free_255 && R1>=0 && free_254>=2 && free_255>=1+free_252 && 0>=1+free_252 && M1==0 ], cost: 1
     58: f5 -> f5 : F'=free_258, L'=free_256, R'=free_257, M1'=0, N1'=free_256, O1'=0, P1'=free_256, Q1_1'=K1, R1'=-1+R1, S1'=-1+R1, [ K1>=1+free_259 && R1>=0 && free_258>=2 && free_259>=1+free_256 && free_256>=1 && M1==0 ], cost: 1
     59: f5 -> f22 : F'=free_267, H'=free_264, K1'=free_260, M1'=free_265, N1'=free_266, O1'=free_261, P1'=free_263, Q1_1'=free_262, [ free_267>=2 && R1>=0 && M1==K1 ], cost: 1
     60: f21 -> f13 : A'=2, B'=free_270, C'=free_271, F'=free_270, Q'=free_271, J'=free_271, K'=free_268, T1'=free_272, U1'=free_269, [ free_270>=2 ], cost: 1
     65: f21 -> f22 : A'=free_301, B'=free_308, C'=free_295, F'=free_303, G'=free_306, H'=free_293, Q'=free_299, J'=free_297, K'=free_298, L'=0, M'=free_304, N'=free_309, K1'=free_300, M1'=free_294, N1'=free_296, O1'=free_302, P1'=free_307, Q1_1'=free_305, T1'=free_310, [ 0>=free_313 && 0>=free_314 && 0>=free_311 && 0>=free_303 && 0>=free_312 ], cost: 1


Simplified the transitions:
  Start location: f21
      2: f13 -> f13 : A'=1+A, C'=K, J'=K, K'=free_19, P'=free_18, Q_1'=A, [ B>=1+A && A>=0 ], cost: 1
      0: f13 -> f20 : A'=D, B'=free_5, C'=free_7, E'=0, F'=free_8, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=C, M'=C, N'=C, O'=free_2, [ A>=B && A>=0 && free_8>=2 && 0>=1+C && free_2>=free_8 && D>=free_8 && E==0 ], cost: 1
      1: f13 -> f20 : A'=D, B'=free_14, C'=free_16, E'=0, F'=free_17, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=C, M'=C, N'=C, O'=free_11, [ A>=B && A>=0 && free_17>=2 && C>=1 && free_11>=free_17 && D>=free_17 && E==0 ], cost: 1
     17: f20 -> f20 : D'=-1+D, E'=1+E, F'=free_77, L'=free_75, M'=free_75, R'=free_76, Z'=N, A1'=free_74, B1'=1+E, C1'=-1+D, [ E>=0 && D>=0 && free_77>=2 && 0>=1+free_75 && 0>=1+free_74 ], cost: 1
     18: f20 -> f20 : D'=-1+D, E'=1+E, F'=free_82, L'=free_80, M'=free_80, R'=free_81, Z'=N, A1'=free_79, B1'=1+E, C1'=-1+D, [ E>=0 && D>=0 && free_82>=2 && 0>=1+free_80 && free_79>=1 ], cost: 1
     19: f20 -> f20 : D'=-1+D, E'=1+E, F'=free_87, L'=free_85, M'=free_85, R'=free_86, Z'=N, A1'=free_84, B1'=1+E, C1'=-1+D, [ E>=0 && D>=0 && free_87>=2 && free_85>=1 && 0>=1+free_84 ], cost: 1
     20: f20 -> f20 : D'=-1+D, E'=1+E, F'=free_92, L'=free_90, M'=free_90, R'=free_91, Z'=N, A1'=free_89, B1'=1+E, C1'=-1+D, [ E>=0 && D>=0 && free_92>=2 && free_90>=1 && free_89>=1 ], cost: 1
     21: f20 -> f20 : D'=-1+D, E'=1+E, F'=free_97, L'=free_95, M'=free_95, R'=free_96, Z'=N, A1'=free_94, B1'=1+E, C1'=-1+D, [ E>=0 && D>=0 && free_97>=2 && 0>=1+free_95 && 0>=1+free_94 ], cost: 1
     22: f20 -> f20 : D'=-1+D, E'=1+E, F'=free_102, L'=free_100, M'=free_100, R'=free_101, Z'=N, A1'=free_99, B1'=1+E, C1'=-1+D, [ E>=0 && D>=0 && free_102>=2 && 0>=1+free_100 && free_99>=1 ], cost: 1
     23: f20 -> f20 : D'=-1+D, E'=1+E, F'=free_107, L'=free_105, M'=free_105, R'=free_106, Z'=N, A1'=free_104, B1'=1+E, C1'=-1+D, [ E>=0 && D>=0 && free_107>=2 && free_105>=1 && 0>=1+free_104 ], cost: 1
     24: f20 -> f20 : D'=-1+D, E'=1+E, F'=free_112, L'=free_110, M'=free_110, R'=free_111, Z'=N, A1'=free_109, B1'=1+E, C1'=-1+D, [ E>=0 && D>=0 && free_112>=2 && free_110>=1 && free_109>=1 ], cost: 1
     15: f20 -> f11 : F'=free_72, M'=L, N'=L, X'=E, Y'=0, [ E>=0 && D>=0 && free_72>=2 && 0>=1+L && X==E && N==0 && Y==0 ], cost: 1
     16: f20 -> f11 : F'=free_73, M'=L, N'=L, X'=E, Y'=0, [ E>=0 && D>=0 && free_73>=2 && L>=1 && X==E && N==0 && Y==0 ], cost: 1
     33: f11 -> f11 : F'=free_149, L'=free_147, M'=free_147, R'=free_148, X'=-1+X, Y'=1+Y, G1'=N, H1'=free_146, Q1'=1+Y, J1'=-1+X, [ Y>=0 && X>=0 && free_149>=2 && 0>=1+free_147 && 0>=1+free_146 ], cost: 1
     34: f11 -> f11 : F'=free_154, L'=free_152, M'=free_152, R'=free_153, X'=-1+X, Y'=1+Y, G1'=N, H1'=free_151, Q1'=1+Y, J1'=-1+X, [ Y>=0 && X>=0 && free_154>=2 && 0>=1+free_152 && free_151>=1 ], cost: 1
     35: f11 -> f11 : F'=free_159, L'=free_157, M'=free_157, R'=free_158, X'=-1+X, Y'=1+Y, G1'=N, H1'=free_156, Q1'=1+Y, J1'=-1+X, [ Y>=0 && X>=0 && free_159>=2 && free_157>=1 && 0>=1+free_156 ], cost: 1
     36: f11 -> f11 : F'=free_164, L'=free_162, M'=free_162, R'=free_163, X'=-1+X, Y'=1+Y, G1'=N, H1'=free_161, Q1'=1+Y, J1'=-1+X, [ Y>=0 && X>=0 && free_164>=2 && free_162>=1 && free_161>=1 ], cost: 1
     37: f11 -> f11 : F'=free_169, L'=free_167, M'=free_167, R'=free_168, X'=-1+X, Y'=1+Y, G1'=N, H1'=free_166, Q1'=1+Y, J1'=-1+X, [ Y>=0 && X>=0 && free_169>=2 && 0>=1+free_167 && 0>=1+free_166 ], cost: 1
     38: f11 -> f11 : F'=free_174, L'=free_172, M'=free_172, R'=free_173, X'=-1+X, Y'=1+Y, G1'=N, H1'=free_171, Q1'=1+Y, J1'=-1+X, [ Y>=0 && X>=0 && free_174>=2 && 0>=1+free_172 && free_171>=1 ], cost: 1
     39: f11 -> f11 : F'=free_179, L'=free_177, M'=free_177, R'=free_178, X'=-1+X, Y'=1+Y, G1'=N, H1'=free_176, Q1'=1+Y, J1'=-1+X, [ Y>=0 && X>=0 && free_179>=2 && free_177>=1 && 0>=1+free_176 ], cost: 1
     40: f11 -> f11 : F'=free_184, L'=free_182, M'=free_182, R'=free_183, X'=-1+X, Y'=1+Y, G1'=N, H1'=free_181, Q1'=1+Y, J1'=-1+X, [ Y>=0 && X>=0 && free_184>=2 && free_182>=1 && free_181>=1 ], cost: 1
     70: f11 -> f5 : F'=free_333, M'=free_331, N'=free_332, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_334>=2 && free_333>=2 && X>=0 && Y>=0 && L>=1 && 0>=1+L && N==0 ], cost: 1
     71: f11 -> f5 : F'=free_337, M'=free_335, N'=free_336, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_338>=2 && free_337>=2 && X>=0 && Y>=0 && L>=1 && N==0 ], cost: 1
     72: f11 -> f5 : F'=free_341, M'=free_339, N'=free_340, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_342>=2 && free_341>=2 && X>=0 && Y>=0 && 0>=1+L && N==0 ], cost: 1
     73: f11 -> f5 : F'=free_345, M'=free_343, N'=free_344, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_346>=2 && free_345>=2 && X>=0 && Y>=0 && 0>=1+L && L>=1 && N==0 ], cost: 1
     51: f5 -> f5 : F'=free_230, L'=free_228, R'=free_229, M1'=0, N1'=free_228, O1'=0, P1'=free_228, Q1_1'=K1, R1'=-1+R1, S1'=-1+R1, [ R1>=0 && free_230>=2 && 0>=1+free_228 && M1==0 && 1+K1<=-1+free_228 ], cost: 1
     52: f5 -> f5 : F'=free_234, L'=free_232, R'=free_233, M1'=0, N1'=free_232, O1'=0, P1'=free_232, Q1_1'=K1, R1'=-1+R1, S1'=-1+R1, [ R1>=0 && free_234>=2 && free_232>=1 && M1==0 && 1+K1<=-1+free_232 ], cost: 1
     53: f5 -> f5 : F'=free_238, L'=free_236, R'=free_237, M1'=0, N1'=free_236, O1'=0, P1'=free_236, Q1_1'=K1, R1'=-1+R1, S1'=-1+R1, [ R1>=0 && free_238>=2 && 0>=1+free_236 && M1==0 ], cost: 1
     54: f5 -> f5 : F'=free_242, L'=free_240, R'=free_241, M1'=0, N1'=free_240, O1'=0, P1'=free_240, Q1_1'=K1, R1'=-1+R1, S1'=-1+R1, [ R1>=0 && free_242>=2 && free_240>=1 && M1==0 ], cost: 1
     55: f5 -> f5 : F'=free_246, L'=free_244, R'=free_245, M1'=0, N1'=free_244, O1'=0, P1'=free_244, Q1_1'=K1, R1'=-1+R1, S1'=-1+R1, [ R1>=0 && free_246>=2 && 0>=1+free_244 && M1==0 ], cost: 1
     56: f5 -> f5 : F'=free_250, L'=free_248, R'=free_249, M1'=0, N1'=free_248, O1'=0, P1'=free_248, Q1_1'=K1, R1'=-1+R1, S1'=-1+R1, [ K1>=1+free_251 && R1>=0 && free_250>=2 && free_248>=1+free_251 && free_248>=1 && M1==0 ], cost: 1
     57: f5 -> f5 : F'=free_254, L'=free_252, R'=free_253, M1'=0, N1'=free_252, O1'=0, P1'=free_252, Q1_1'=K1, R1'=-1+R1, S1'=-1+R1, [ K1>=1+free_255 && R1>=0 && free_254>=2 && free_255>=1+free_252 && 0>=1+free_252 && M1==0 ], cost: 1
     58: f5 -> f5 : F'=free_258, L'=free_256, R'=free_257, M1'=0, N1'=free_256, O1'=0, P1'=free_256, Q1_1'=K1, R1'=-1+R1, S1'=-1+R1, [ K1>=1+free_259 && R1>=0 && free_258>=2 && free_259>=1+free_256 && free_256>=1 && M1==0 ], cost: 1
     60: f21 -> f13 : A'=2, B'=free_270, C'=free_271, F'=free_270, Q'=free_271, J'=free_271, K'=free_268, T1'=free_272, U1'=free_269, [ free_270>=2 ], cost: 1

Eliminating 1 self-loops for location f13
  Self-Loop 2 has the metering function: B-A, resulting in the new transition 74.
  Removing the self-loops: 2.
Eliminating 8 self-loops for location f20
  Self-Loop 17 has the metering function: 1+D, resulting in the new transition 75.
  Self-Loop 18 has the metering function: 1+D, resulting in the new transition 76.
  Self-Loop 19 has the metering function: 1+D, resulting in the new transition 77.
  Self-Loop 20 has the metering function: 1+D, resulting in the new transition 78.
  Self-Loop 21 has the metering function: 1+D, resulting in the new transition 79.
  Self-Loop 22 has the metering function: 1+D, resulting in the new transition 80.
  Self-Loop 23 has the metering function: 1+D, resulting in the new transition 81.
  Self-Loop 24 has the metering function: 1+D, resulting in the new transition 82.
  Removing the self-loops: 17 18 19 20 21 22 23 24.
Eliminating 8 self-loops for location f11
  Self-Loop 33 has the metering function: 1+X, resulting in the new transition 83.
  Self-Loop 34 has the metering function: 1+X, resulting in the new transition 84.
  Self-Loop 35 has the metering function: 1+X, resulting in the new transition 85.
  Self-Loop 36 has the metering function: 1+X, resulting in the new transition 86.
  Self-Loop 37 has the metering function: 1+X, resulting in the new transition 87.
  Self-Loop 38 has the metering function: 1+X, resulting in the new transition 88.
  Self-Loop 39 has the metering function: 1+X, resulting in the new transition 89.
  Self-Loop 40 has the metering function: 1+X, resulting in the new transition 90.
  Removing the self-loops: 33 34 35 36 37 38 39 40.
Eliminating 8 self-loops for location f5
  Self-Loop 51 has the metering function: 1+R1, resulting in the new transition 91.
  Self-Loop 52 has the metering function: 1+R1, resulting in the new transition 92.
  Self-Loop 53 has the metering function: 1+R1, resulting in the new transition 93.
  Self-Loop 54 has the metering function: 1+R1, resulting in the new transition 94.
  Self-Loop 55 has the metering function: 1+R1, resulting in the new transition 95.
  Self-Loop 56 has the metering function: 1+R1, resulting in the new transition 96.
  Self-Loop 57 has the metering function: 1+R1, resulting in the new transition 97.
  Self-Loop 58 has the metering function: 1+R1, resulting in the new transition 98.
  Removing the self-loops: 51 52 53 54 55 56 57 58.

Removed all Self-loops using metering functions (where possible):
  Start location: f21
     74: f13 -> [10] : A'=B, C'=free_19, J'=free_19, K'=free_19, P'=free_18, Q_1'=-1+B, [ B>=1+A && A>=0 ], cost: B-A
     75: f20 -> [11] : D'=-1, E'=1+E+D, F'=free_77, L'=free_75, M'=free_75, R'=free_76, Z'=N, A1'=free_74, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_77>=2 && 0>=1+free_75 && 0>=1+free_74 ], cost: 1+D
     76: f20 -> [11] : D'=-1, E'=1+E+D, F'=free_82, L'=free_80, M'=free_80, R'=free_81, Z'=N, A1'=free_79, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_82>=2 && 0>=1+free_80 && free_79>=1 ], cost: 1+D
     77: f20 -> [11] : D'=-1, E'=1+E+D, F'=free_87, L'=free_85, M'=free_85, R'=free_86, Z'=N, A1'=free_84, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_87>=2 && free_85>=1 && 0>=1+free_84 ], cost: 1+D
     78: f20 -> [11] : D'=-1, E'=1+E+D, F'=free_92, L'=free_90, M'=free_90, R'=free_91, Z'=N, A1'=free_89, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_92>=2 && free_90>=1 && free_89>=1 ], cost: 1+D
     79: f20 -> [11] : D'=-1, E'=1+E+D, F'=free_97, L'=free_95, M'=free_95, R'=free_96, Z'=N, A1'=free_94, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_97>=2 && 0>=1+free_95 && 0>=1+free_94 ], cost: 1+D
     80: f20 -> [11] : D'=-1, E'=1+E+D, F'=free_102, L'=free_100, M'=free_100, R'=free_101, Z'=N, A1'=free_99, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_102>=2 && 0>=1+free_100 && free_99>=1 ], cost: 1+D
     81: f20 -> [11] : D'=-1, E'=1+E+D, F'=free_107, L'=free_105, M'=free_105, R'=free_106, Z'=N, A1'=free_104, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_107>=2 && free_105>=1 && 0>=1+free_104 ], cost: 1+D
     82: f20 -> [11] : D'=-1, E'=1+E+D, F'=free_112, L'=free_110, M'=free_110, R'=free_111, Z'=N, A1'=free_109, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_112>=2 && free_110>=1 && free_109>=1 ], cost: 1+D
     83: f11 -> [12] : F'=free_149, L'=free_147, M'=free_147, R'=free_148, X'=-1, Y'=1+X+Y, G1'=N, H1'=free_146, Q1'=1+X+Y, J1'=-1, [ Y>=0 && X>=0 && free_149>=2 && 0>=1+free_147 && 0>=1+free_146 ], cost: 1+X
     84: f11 -> [12] : F'=free_154, L'=free_152, M'=free_152, R'=free_153, X'=-1, Y'=1+X+Y, G1'=N, H1'=free_151, Q1'=1+X+Y, J1'=-1, [ Y>=0 && X>=0 && free_154>=2 && 0>=1+free_152 && free_151>=1 ], cost: 1+X
     85: f11 -> [12] : F'=free_159, L'=free_157, M'=free_157, R'=free_158, X'=-1, Y'=1+X+Y, G1'=N, H1'=free_156, Q1'=1+X+Y, J1'=-1, [ Y>=0 && X>=0 && free_159>=2 && free_157>=1 && 0>=1+free_156 ], cost: 1+X
     86: f11 -> [12] : F'=free_164, L'=free_162, M'=free_162, R'=free_163, X'=-1, Y'=1+X+Y, G1'=N, H1'=free_161, Q1'=1+X+Y, J1'=-1, [ Y>=0 && X>=0 && free_164>=2 && free_162>=1 && free_161>=1 ], cost: 1+X
     87: f11 -> [12] : F'=free_169, L'=free_167, M'=free_167, R'=free_168, X'=-1, Y'=1+X+Y, G1'=N, H1'=free_166, Q1'=1+X+Y, J1'=-1, [ Y>=0 && X>=0 && free_169>=2 && 0>=1+free_167 && 0>=1+free_166 ], cost: 1+X
     88: f11 -> [12] : F'=free_174, L'=free_172, M'=free_172, R'=free_173, X'=-1, Y'=1+X+Y, G1'=N, H1'=free_171, Q1'=1+X+Y, J1'=-1, [ Y>=0 && X>=0 && free_174>=2 && 0>=1+free_172 && free_171>=1 ], cost: 1+X
     89: f11 -> [12] : F'=free_179, L'=free_177, M'=free_177, R'=free_178, X'=-1, Y'=1+X+Y, G1'=N, H1'=free_176, Q1'=1+X+Y, J1'=-1, [ Y>=0 && X>=0 && free_179>=2 && free_177>=1 && 0>=1+free_176 ], cost: 1+X
     90: f11 -> [12] : F'=free_184, L'=free_182, M'=free_182, R'=free_183, X'=-1, Y'=1+X+Y, G1'=N, H1'=free_181, Q1'=1+X+Y, J1'=-1, [ Y>=0 && X>=0 && free_184>=2 && free_182>=1 && free_181>=1 ], cost: 1+X
     91: f5 -> [13] : F'=free_230, L'=free_228, R'=free_229, M1'=0, N1'=free_228, O1'=0, P1'=free_228, Q1_1'=K1, R1'=-1, S1'=-1, [ R1>=0 && free_230>=2 && 0>=1+free_228 && M1==0 && 1+K1<=-1+free_228 ], cost: 1+R1
     92: f5 -> [13] : F'=free_234, L'=free_232, R'=free_233, M1'=0, N1'=free_232, O1'=0, P1'=free_232, Q1_1'=K1, R1'=-1, S1'=-1, [ R1>=0 && free_234>=2 && free_232>=1 && M1==0 && 1+K1<=-1+free_232 ], cost: 1+R1
     93: f5 -> [13] : F'=free_238, L'=free_236, R'=free_237, M1'=0, N1'=free_236, O1'=0, P1'=free_236, Q1_1'=K1, R1'=-1, S1'=-1, [ R1>=0 && free_238>=2 && 0>=1+free_236 && M1==0 ], cost: 1+R1
     94: f5 -> [13] : F'=free_242, L'=free_240, R'=free_241, M1'=0, N1'=free_240, O1'=0, P1'=free_240, Q1_1'=K1, R1'=-1, S1'=-1, [ R1>=0 && free_242>=2 && free_240>=1 && M1==0 ], cost: 1+R1
     95: f5 -> [13] : F'=free_246, L'=free_244, R'=free_245, M1'=0, N1'=free_244, O1'=0, P1'=free_244, Q1_1'=K1, R1'=-1, S1'=-1, [ R1>=0 && free_246>=2 && 0>=1+free_244 && M1==0 ], cost: 1+R1
     96: f5 -> [13] : F'=free_250, L'=free_248, R'=free_249, M1'=0, N1'=free_248, O1'=0, P1'=free_248, Q1_1'=K1, R1'=-1, S1'=-1, [ R1>=0 && free_250>=2 && free_248>=1 && M1==0 ], cost: 1+R1
     97: f5 -> [13] : F'=free_254, L'=free_252, R'=free_253, M1'=0, N1'=free_252, O1'=0, P1'=free_252, Q1_1'=K1, R1'=-1, S1'=-1, [ R1>=0 && free_254>=2 && 0>=1+free_252 && M1==0 && 1+free_252<=-1+K1 ], cost: 1+R1
     98: f5 -> [13] : F'=free_258, L'=free_256, R'=free_257, M1'=0, N1'=free_256, O1'=0, P1'=free_256, Q1_1'=K1, R1'=-1, S1'=-1, [ R1>=0 && free_258>=2 && free_256>=1 && M1==0 && 1+free_256<=-1+K1 ], cost: 1+R1
     60: f21 -> f13 : A'=2, B'=free_270, C'=free_271, F'=free_270, Q'=free_271, J'=free_271, K'=free_268, T1'=free_272, U1'=free_269, [ free_270>=2 ], cost: 1
      0: [10] -> f20 : A'=D, B'=free_5, C'=free_7, E'=0, F'=free_8, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=C, M'=C, N'=C, O'=free_2, [ A>=B && A>=0 && free_8>=2 && 0>=1+C && free_2>=free_8 && D>=free_8 && E==0 ], cost: 1
      1: [10] -> f20 : A'=D, B'=free_14, C'=free_16, E'=0, F'=free_17, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=C, M'=C, N'=C, O'=free_11, [ A>=B && A>=0 && free_17>=2 && C>=1 && free_11>=free_17 && D>=free_17 && E==0 ], cost: 1
     15: [11] -> f11 : F'=free_72, M'=L, N'=L, X'=E, Y'=0, [ E>=0 && D>=0 && free_72>=2 && 0>=1+L && X==E && N==0 && Y==0 ], cost: 1
     16: [11] -> f11 : F'=free_73, M'=L, N'=L, X'=E, Y'=0, [ E>=0 && D>=0 && free_73>=2 && L>=1 && X==E && N==0 && Y==0 ], cost: 1
     70: [12] -> f5 : F'=free_333, M'=free_331, N'=free_332, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_334>=2 && free_333>=2 && X>=0 && Y>=0 && L>=1 && 0>=1+L && N==0 ], cost: 1
     71: [12] -> f5 : F'=free_337, M'=free_335, N'=free_336, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_338>=2 && free_337>=2 && X>=0 && Y>=0 && L>=1 && N==0 ], cost: 1
     72: [12] -> f5 : F'=free_341, M'=free_339, N'=free_340, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_342>=2 && free_341>=2 && X>=0 && Y>=0 && 0>=1+L && N==0 ], cost: 1
     73: [12] -> f5 : F'=free_345, M'=free_343, N'=free_344, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_346>=2 && free_345>=2 && X>=0 && Y>=0 && 0>=1+L && L>=1 && N==0 ], cost: 1


Applied simple chaining:
  Start location: f21
     75: f20 -> [11] : D'=-1, E'=1+E+D, F'=free_77, L'=free_75, M'=free_75, R'=free_76, Z'=N, A1'=free_74, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_77>=2 && 0>=1+free_75 && 0>=1+free_74 ], cost: 1+D
     76: f20 -> [11] : D'=-1, E'=1+E+D, F'=free_82, L'=free_80, M'=free_80, R'=free_81, Z'=N, A1'=free_79, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_82>=2 && 0>=1+free_80 && free_79>=1 ], cost: 1+D
     77: f20 -> [11] : D'=-1, E'=1+E+D, F'=free_87, L'=free_85, M'=free_85, R'=free_86, Z'=N, A1'=free_84, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_87>=2 && free_85>=1 && 0>=1+free_84 ], cost: 1+D
     78: f20 -> [11] : D'=-1, E'=1+E+D, F'=free_92, L'=free_90, M'=free_90, R'=free_91, Z'=N, A1'=free_89, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_92>=2 && free_90>=1 && free_89>=1 ], cost: 1+D
     79: f20 -> [11] : D'=-1, E'=1+E+D, F'=free_97, L'=free_95, M'=free_95, R'=free_96, Z'=N, A1'=free_94, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_97>=2 && 0>=1+free_95 && 0>=1+free_94 ], cost: 1+D
     80: f20 -> [11] : D'=-1, E'=1+E+D, F'=free_102, L'=free_100, M'=free_100, R'=free_101, Z'=N, A1'=free_99, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_102>=2 && 0>=1+free_100 && free_99>=1 ], cost: 1+D
     81: f20 -> [11] : D'=-1, E'=1+E+D, F'=free_107, L'=free_105, M'=free_105, R'=free_106, Z'=N, A1'=free_104, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_107>=2 && free_105>=1 && 0>=1+free_104 ], cost: 1+D
     82: f20 -> [11] : D'=-1, E'=1+E+D, F'=free_112, L'=free_110, M'=free_110, R'=free_111, Z'=N, A1'=free_109, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_112>=2 && free_110>=1 && free_109>=1 ], cost: 1+D
     83: f11 -> [12] : F'=free_149, L'=free_147, M'=free_147, R'=free_148, X'=-1, Y'=1+X+Y, G1'=N, H1'=free_146, Q1'=1+X+Y, J1'=-1, [ Y>=0 && X>=0 && free_149>=2 && 0>=1+free_147 && 0>=1+free_146 ], cost: 1+X
     84: f11 -> [12] : F'=free_154, L'=free_152, M'=free_152, R'=free_153, X'=-1, Y'=1+X+Y, G1'=N, H1'=free_151, Q1'=1+X+Y, J1'=-1, [ Y>=0 && X>=0 && free_154>=2 && 0>=1+free_152 && free_151>=1 ], cost: 1+X
     85: f11 -> [12] : F'=free_159, L'=free_157, M'=free_157, R'=free_158, X'=-1, Y'=1+X+Y, G1'=N, H1'=free_156, Q1'=1+X+Y, J1'=-1, [ Y>=0 && X>=0 && free_159>=2 && free_157>=1 && 0>=1+free_156 ], cost: 1+X
     86: f11 -> [12] : F'=free_164, L'=free_162, M'=free_162, R'=free_163, X'=-1, Y'=1+X+Y, G1'=N, H1'=free_161, Q1'=1+X+Y, J1'=-1, [ Y>=0 && X>=0 && free_164>=2 && free_162>=1 && free_161>=1 ], cost: 1+X
     87: f11 -> [12] : F'=free_169, L'=free_167, M'=free_167, R'=free_168, X'=-1, Y'=1+X+Y, G1'=N, H1'=free_166, Q1'=1+X+Y, J1'=-1, [ Y>=0 && X>=0 && free_169>=2 && 0>=1+free_167 && 0>=1+free_166 ], cost: 1+X
     88: f11 -> [12] : F'=free_174, L'=free_172, M'=free_172, R'=free_173, X'=-1, Y'=1+X+Y, G1'=N, H1'=free_171, Q1'=1+X+Y, J1'=-1, [ Y>=0 && X>=0 && free_174>=2 && 0>=1+free_172 && free_171>=1 ], cost: 1+X
     89: f11 -> [12] : F'=free_179, L'=free_177, M'=free_177, R'=free_178, X'=-1, Y'=1+X+Y, G1'=N, H1'=free_176, Q1'=1+X+Y, J1'=-1, [ Y>=0 && X>=0 && free_179>=2 && free_177>=1 && 0>=1+free_176 ], cost: 1+X
     90: f11 -> [12] : F'=free_184, L'=free_182, M'=free_182, R'=free_183, X'=-1, Y'=1+X+Y, G1'=N, H1'=free_181, Q1'=1+X+Y, J1'=-1, [ Y>=0 && X>=0 && free_184>=2 && free_182>=1 && free_181>=1 ], cost: 1+X
     91: f5 -> [13] : F'=free_230, L'=free_228, R'=free_229, M1'=0, N1'=free_228, O1'=0, P1'=free_228, Q1_1'=K1, R1'=-1, S1'=-1, [ R1>=0 && free_230>=2 && 0>=1+free_228 && M1==0 && 1+K1<=-1+free_228 ], cost: 1+R1
     92: f5 -> [13] : F'=free_234, L'=free_232, R'=free_233, M1'=0, N1'=free_232, O1'=0, P1'=free_232, Q1_1'=K1, R1'=-1, S1'=-1, [ R1>=0 && free_234>=2 && free_232>=1 && M1==0 && 1+K1<=-1+free_232 ], cost: 1+R1
     93: f5 -> [13] : F'=free_238, L'=free_236, R'=free_237, M1'=0, N1'=free_236, O1'=0, P1'=free_236, Q1_1'=K1, R1'=-1, S1'=-1, [ R1>=0 && free_238>=2 && 0>=1+free_236 && M1==0 ], cost: 1+R1
     94: f5 -> [13] : F'=free_242, L'=free_240, R'=free_241, M1'=0, N1'=free_240, O1'=0, P1'=free_240, Q1_1'=K1, R1'=-1, S1'=-1, [ R1>=0 && free_242>=2 && free_240>=1 && M1==0 ], cost: 1+R1
     95: f5 -> [13] : F'=free_246, L'=free_244, R'=free_245, M1'=0, N1'=free_244, O1'=0, P1'=free_244, Q1_1'=K1, R1'=-1, S1'=-1, [ R1>=0 && free_246>=2 && 0>=1+free_244 && M1==0 ], cost: 1+R1
     96: f5 -> [13] : F'=free_250, L'=free_248, R'=free_249, M1'=0, N1'=free_248, O1'=0, P1'=free_248, Q1_1'=K1, R1'=-1, S1'=-1, [ R1>=0 && free_250>=2 && free_248>=1 && M1==0 ], cost: 1+R1
     97: f5 -> [13] : F'=free_254, L'=free_252, R'=free_253, M1'=0, N1'=free_252, O1'=0, P1'=free_252, Q1_1'=K1, R1'=-1, S1'=-1, [ R1>=0 && free_254>=2 && 0>=1+free_252 && M1==0 && 1+free_252<=-1+K1 ], cost: 1+R1
     98: f5 -> [13] : F'=free_258, L'=free_256, R'=free_257, M1'=0, N1'=free_256, O1'=0, P1'=free_256, Q1_1'=K1, R1'=-1, S1'=-1, [ R1>=0 && free_258>=2 && free_256>=1 && M1==0 && 1+free_256<=-1+K1 ], cost: 1+R1
     60: f21 -> [10] : A'=free_270, B'=free_270, C'=free_19, F'=free_270, Q'=free_271, J'=free_19, K'=free_19, P'=free_18, Q_1'=-1+free_270, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 ], cost: -1+free_270
      0: [10] -> f20 : A'=D, B'=free_5, C'=free_7, E'=0, F'=free_8, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=C, M'=C, N'=C, O'=free_2, [ A>=B && A>=0 && free_8>=2 && 0>=1+C && free_2>=free_8 && D>=free_8 && E==0 ], cost: 1
      1: [10] -> f20 : A'=D, B'=free_14, C'=free_16, E'=0, F'=free_17, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=C, M'=C, N'=C, O'=free_11, [ A>=B && A>=0 && free_17>=2 && C>=1 && free_11>=free_17 && D>=free_17 && E==0 ], cost: 1
     15: [11] -> f11 : F'=free_72, M'=L, N'=L, X'=E, Y'=0, [ E>=0 && D>=0 && free_72>=2 && 0>=1+L && X==E && N==0 && Y==0 ], cost: 1
     16: [11] -> f11 : F'=free_73, M'=L, N'=L, X'=E, Y'=0, [ E>=0 && D>=0 && free_73>=2 && L>=1 && X==E && N==0 && Y==0 ], cost: 1
     70: [12] -> f5 : F'=free_333, M'=free_331, N'=free_332, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_334>=2 && free_333>=2 && X>=0 && Y>=0 && L>=1 && 0>=1+L && N==0 ], cost: 1
     71: [12] -> f5 : F'=free_337, M'=free_335, N'=free_336, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_338>=2 && free_337>=2 && X>=0 && Y>=0 && L>=1 && N==0 ], cost: 1
     72: [12] -> f5 : F'=free_341, M'=free_339, N'=free_340, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_342>=2 && free_341>=2 && X>=0 && Y>=0 && 0>=1+L && N==0 ], cost: 1
     73: [12] -> f5 : F'=free_345, M'=free_343, N'=free_344, Y'=1+R1, K1'=L, L1'=R1, M1'=0, N1'=L, O1'=0, P1'=L, Q1_1'=L, [ free_346>=2 && free_345>=2 && X>=0 && Y>=0 && 0>=1+L && L>=1 && N==0 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f21
    101: f20 -> [14] : D'=-1, E'=1+E+D, F'=free_77, L'=free_75, M'=free_75, R'=free_76, Z'=N, A1'=free_74, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_77>=2 && 0>=1+free_75 && 0>=1+free_74 ], cost: 1+D
    102: f20 -> [15] : D'=-1, E'=1+E+D, F'=free_77, L'=free_75, M'=free_75, R'=free_76, Z'=N, A1'=free_74, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_77>=2 && 0>=1+free_75 && 0>=1+free_74 ], cost: 1+D
    103: f20 -> [16] : D'=-1, E'=1+E+D, F'=free_82, L'=free_80, M'=free_80, R'=free_81, Z'=N, A1'=free_79, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_82>=2 && 0>=1+free_80 && free_79>=1 ], cost: 1+D
    104: f20 -> [17] : D'=-1, E'=1+E+D, F'=free_82, L'=free_80, M'=free_80, R'=free_81, Z'=N, A1'=free_79, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_82>=2 && 0>=1+free_80 && free_79>=1 ], cost: 1+D
    105: f20 -> [18] : D'=-1, E'=1+E+D, F'=free_87, L'=free_85, M'=free_85, R'=free_86, Z'=N, A1'=free_84, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_87>=2 && free_85>=1 && 0>=1+free_84 ], cost: 1+D
    106: f20 -> [19] : D'=-1, E'=1+E+D, F'=free_87, L'=free_85, M'=free_85, R'=free_86, Z'=N, A1'=free_84, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_87>=2 && free_85>=1 && 0>=1+free_84 ], cost: 1+D
    107: f20 -> [20] : D'=-1, E'=1+E+D, F'=free_92, L'=free_90, M'=free_90, R'=free_91, Z'=N, A1'=free_89, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_92>=2 && free_90>=1 && free_89>=1 ], cost: 1+D
    108: f20 -> [21] : D'=-1, E'=1+E+D, F'=free_92, L'=free_90, M'=free_90, R'=free_91, Z'=N, A1'=free_89, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_92>=2 && free_90>=1 && free_89>=1 ], cost: 1+D
    109: f20 -> [22] : D'=-1, E'=1+E+D, F'=free_97, L'=free_95, M'=free_95, R'=free_96, Z'=N, A1'=free_94, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_97>=2 && 0>=1+free_95 && 0>=1+free_94 ], cost: 1+D
    110: f20 -> [23] : D'=-1, E'=1+E+D, F'=free_97, L'=free_95, M'=free_95, R'=free_96, Z'=N, A1'=free_94, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_97>=2 && 0>=1+free_95 && 0>=1+free_94 ], cost: 1+D
    111: f20 -> [24] : D'=-1, E'=1+E+D, F'=free_102, L'=free_100, M'=free_100, R'=free_101, Z'=N, A1'=free_99, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_102>=2 && 0>=1+free_100 && free_99>=1 ], cost: 1+D
    112: f20 -> [25] : D'=-1, E'=1+E+D, F'=free_102, L'=free_100, M'=free_100, R'=free_101, Z'=N, A1'=free_99, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_102>=2 && 0>=1+free_100 && free_99>=1 ], cost: 1+D
    113: f20 -> [26] : D'=-1, E'=1+E+D, F'=free_107, L'=free_105, M'=free_105, R'=free_106, Z'=N, A1'=free_104, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_107>=2 && free_105>=1 && 0>=1+free_104 ], cost: 1+D
    114: f20 -> [27] : D'=-1, E'=1+E+D, F'=free_107, L'=free_105, M'=free_105, R'=free_106, Z'=N, A1'=free_104, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_107>=2 && free_105>=1 && 0>=1+free_104 ], cost: 1+D
    115: f20 -> [28] : D'=-1, E'=1+E+D, F'=free_112, L'=free_110, M'=free_110, R'=free_111, Z'=N, A1'=free_109, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_112>=2 && free_110>=1 && free_109>=1 ], cost: 1+D
    116: f20 -> [29] : D'=-1, E'=1+E+D, F'=free_112, L'=free_110, M'=free_110, R'=free_111, Z'=N, A1'=free_109, B1'=1+E+D, C1'=-1, [ E>=0 && D>=0 && free_112>=2 && free_110>=1 && free_109>=1 ], cost: 1+D
     99: f21 -> f20 : A'=D, B'=free_5, C'=free_7, E'=0, F'=free_8, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_19, M'=free_19, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 ], cost: free_270
    100: f21 -> f20 : A'=D, B'=free_14, C'=free_16, E'=0, F'=free_17, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_19, M'=free_19, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 ], cost: free_270


Applied chaining over branches and pruning:
  Start location: f21
    117: f21 -> [14] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_77, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_75, M'=free_75, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_76, Z'=free_19, A1'=free_74, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_77>=2 && 0>=1+free_75 && 0>=1+free_74 ], cost: 1+free_270+D
    133: f21 -> [14] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_77, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_75, M'=free_75, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_76, Z'=free_19, A1'=free_74, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_77>=2 && 0>=1+free_75 && 0>=1+free_74 ], cost: 1+free_270+D
    118: f21 -> [15] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_77, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_75, M'=free_75, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_76, Z'=free_19, A1'=free_74, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_77>=2 && 0>=1+free_75 && 0>=1+free_74 ], cost: 1+free_270+D
    134: f21 -> [15] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_77, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_75, M'=free_75, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_76, Z'=free_19, A1'=free_74, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_77>=2 && 0>=1+free_75 && 0>=1+free_74 ], cost: 1+free_270+D
    119: f21 -> [16] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_82, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_80, M'=free_80, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_81, Z'=free_19, A1'=free_79, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_82>=2 && 0>=1+free_80 && free_79>=1 ], cost: 1+free_270+D
    135: f21 -> [16] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_82, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_80, M'=free_80, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_81, Z'=free_19, A1'=free_79, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_82>=2 && 0>=1+free_80 && free_79>=1 ], cost: 1+free_270+D
    120: f21 -> [17] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_82, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_80, M'=free_80, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_81, Z'=free_19, A1'=free_79, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_82>=2 && 0>=1+free_80 && free_79>=1 ], cost: 1+free_270+D
    136: f21 -> [17] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_82, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_80, M'=free_80, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_81, Z'=free_19, A1'=free_79, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_82>=2 && 0>=1+free_80 && free_79>=1 ], cost: 1+free_270+D
    121: f21 -> [18] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_87, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_85, M'=free_85, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_86, Z'=free_19, A1'=free_84, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_87>=2 && free_85>=1 && 0>=1+free_84 ], cost: 1+free_270+D
    137: f21 -> [18] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_87, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_85, M'=free_85, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_86, Z'=free_19, A1'=free_84, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_87>=2 && free_85>=1 && 0>=1+free_84 ], cost: 1+free_270+D
    122: f21 -> [19] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_87, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_85, M'=free_85, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_86, Z'=free_19, A1'=free_84, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_87>=2 && free_85>=1 && 0>=1+free_84 ], cost: 1+free_270+D
    138: f21 -> [19] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_87, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_85, M'=free_85, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_86, Z'=free_19, A1'=free_84, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_87>=2 && free_85>=1 && 0>=1+free_84 ], cost: 1+free_270+D
    123: f21 -> [20] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_92, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_90, M'=free_90, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_91, Z'=free_19, A1'=free_89, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_92>=2 && free_90>=1 && free_89>=1 ], cost: 1+free_270+D
    139: f21 -> [20] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_92, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_90, M'=free_90, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_91, Z'=free_19, A1'=free_89, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_92>=2 && free_90>=1 && free_89>=1 ], cost: 1+free_270+D
    124: f21 -> [21] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_92, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_90, M'=free_90, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_91, Z'=free_19, A1'=free_89, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_92>=2 && free_90>=1 && free_89>=1 ], cost: 1+free_270+D
    140: f21 -> [21] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_92, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_90, M'=free_90, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_91, Z'=free_19, A1'=free_89, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_92>=2 && free_90>=1 && free_89>=1 ], cost: 1+free_270+D
    125: f21 -> [22] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_97, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_95, M'=free_95, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_96, Z'=free_19, A1'=free_94, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_97>=2 && 0>=1+free_95 && 0>=1+free_94 ], cost: 1+free_270+D
    141: f21 -> [22] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_97, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_95, M'=free_95, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_96, Z'=free_19, A1'=free_94, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_97>=2 && 0>=1+free_95 && 0>=1+free_94 ], cost: 1+free_270+D
    126: f21 -> [23] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_97, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_95, M'=free_95, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_96, Z'=free_19, A1'=free_94, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_97>=2 && 0>=1+free_95 && 0>=1+free_94 ], cost: 1+free_270+D
    142: f21 -> [23] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_97, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_95, M'=free_95, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_96, Z'=free_19, A1'=free_94, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_97>=2 && 0>=1+free_95 && 0>=1+free_94 ], cost: 1+free_270+D
    127: f21 -> [24] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_102, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_100, M'=free_100, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_101, Z'=free_19, A1'=free_99, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_102>=2 && 0>=1+free_100 && free_99>=1 ], cost: 1+free_270+D
    143: f21 -> [24] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_102, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_100, M'=free_100, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_101, Z'=free_19, A1'=free_99, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_102>=2 && 0>=1+free_100 && free_99>=1 ], cost: 1+free_270+D
    128: f21 -> [25] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_102, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_100, M'=free_100, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_101, Z'=free_19, A1'=free_99, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_102>=2 && 0>=1+free_100 && free_99>=1 ], cost: 1+free_270+D
    144: f21 -> [25] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_102, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_100, M'=free_100, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_101, Z'=free_19, A1'=free_99, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_102>=2 && 0>=1+free_100 && free_99>=1 ], cost: 1+free_270+D
    129: f21 -> [26] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_107, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_105, M'=free_105, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_106, Z'=free_19, A1'=free_104, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_107>=2 && free_105>=1 && 0>=1+free_104 ], cost: 1+free_270+D
    145: f21 -> [26] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_107, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_105, M'=free_105, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_106, Z'=free_19, A1'=free_104, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_107>=2 && free_105>=1 && 0>=1+free_104 ], cost: 1+free_270+D
    130: f21 -> [27] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_107, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_105, M'=free_105, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_106, Z'=free_19, A1'=free_104, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_107>=2 && free_105>=1 && 0>=1+free_104 ], cost: 1+free_270+D
    146: f21 -> [27] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_107, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_105, M'=free_105, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_106, Z'=free_19, A1'=free_104, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_107>=2 && free_105>=1 && 0>=1+free_104 ], cost: 1+free_270+D
    131: f21 -> [28] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_112, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_110, M'=free_110, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_111, Z'=free_19, A1'=free_109, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_112>=2 && free_110>=1 && free_109>=1 ], cost: 1+free_270+D
    147: f21 -> [28] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_112, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_110, M'=free_110, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_111, Z'=free_19, A1'=free_109, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_112>=2 && free_110>=1 && free_109>=1 ], cost: 1+free_270+D
    132: f21 -> [29] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_112, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_110, M'=free_110, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_111, Z'=free_19, A1'=free_109, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_112>=2 && free_110>=1 && free_109>=1 ], cost: 1+free_270+D
    148: f21 -> [29] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_112, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_110, M'=free_110, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_111, Z'=free_19, A1'=free_109, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_112>=2 && free_110>=1 && free_109>=1 ], cost: 1+free_270+D


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f21
    117: f21 -> [14] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_77, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_75, M'=free_75, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_76, Z'=free_19, A1'=free_74, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_77>=2 && 0>=1+free_75 && 0>=1+free_74 ], cost: 1+free_270+D
    133: f21 -> [14] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_77, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_75, M'=free_75, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_76, Z'=free_19, A1'=free_74, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_77>=2 && 0>=1+free_75 && 0>=1+free_74 ], cost: 1+free_270+D
    118: f21 -> [15] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_77, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_75, M'=free_75, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_76, Z'=free_19, A1'=free_74, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_77>=2 && 0>=1+free_75 && 0>=1+free_74 ], cost: 1+free_270+D
    134: f21 -> [15] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_77, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_75, M'=free_75, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_76, Z'=free_19, A1'=free_74, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_77>=2 && 0>=1+free_75 && 0>=1+free_74 ], cost: 1+free_270+D
    119: f21 -> [16] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_82, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_80, M'=free_80, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_81, Z'=free_19, A1'=free_79, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_82>=2 && 0>=1+free_80 && free_79>=1 ], cost: 1+free_270+D
    135: f21 -> [16] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_82, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_80, M'=free_80, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_81, Z'=free_19, A1'=free_79, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_82>=2 && 0>=1+free_80 && free_79>=1 ], cost: 1+free_270+D
    120: f21 -> [17] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_82, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_80, M'=free_80, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_81, Z'=free_19, A1'=free_79, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_82>=2 && 0>=1+free_80 && free_79>=1 ], cost: 1+free_270+D
    136: f21 -> [17] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_82, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_80, M'=free_80, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_81, Z'=free_19, A1'=free_79, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_82>=2 && 0>=1+free_80 && free_79>=1 ], cost: 1+free_270+D
    121: f21 -> [18] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_87, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_85, M'=free_85, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_86, Z'=free_19, A1'=free_84, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_87>=2 && free_85>=1 && 0>=1+free_84 ], cost: 1+free_270+D
    137: f21 -> [18] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_87, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_85, M'=free_85, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_86, Z'=free_19, A1'=free_84, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_87>=2 && free_85>=1 && 0>=1+free_84 ], cost: 1+free_270+D
    122: f21 -> [19] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_87, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_85, M'=free_85, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_86, Z'=free_19, A1'=free_84, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_87>=2 && free_85>=1 && 0>=1+free_84 ], cost: 1+free_270+D
    138: f21 -> [19] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_87, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_85, M'=free_85, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_86, Z'=free_19, A1'=free_84, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_87>=2 && free_85>=1 && 0>=1+free_84 ], cost: 1+free_270+D
    123: f21 -> [20] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_92, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_90, M'=free_90, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_91, Z'=free_19, A1'=free_89, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_92>=2 && free_90>=1 && free_89>=1 ], cost: 1+free_270+D
    139: f21 -> [20] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_92, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_90, M'=free_90, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_91, Z'=free_19, A1'=free_89, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_92>=2 && free_90>=1 && free_89>=1 ], cost: 1+free_270+D
    124: f21 -> [21] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_92, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_90, M'=free_90, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_91, Z'=free_19, A1'=free_89, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_92>=2 && free_90>=1 && free_89>=1 ], cost: 1+free_270+D
    140: f21 -> [21] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_92, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_90, M'=free_90, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_91, Z'=free_19, A1'=free_89, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_92>=2 && free_90>=1 && free_89>=1 ], cost: 1+free_270+D
    125: f21 -> [22] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_97, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_95, M'=free_95, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_96, Z'=free_19, A1'=free_94, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_97>=2 && 0>=1+free_95 && 0>=1+free_94 ], cost: 1+free_270+D
    141: f21 -> [22] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_97, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_95, M'=free_95, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_96, Z'=free_19, A1'=free_94, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_97>=2 && 0>=1+free_95 && 0>=1+free_94 ], cost: 1+free_270+D
    126: f21 -> [23] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_97, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_95, M'=free_95, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_96, Z'=free_19, A1'=free_94, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_97>=2 && 0>=1+free_95 && 0>=1+free_94 ], cost: 1+free_270+D
    142: f21 -> [23] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_97, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_95, M'=free_95, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_96, Z'=free_19, A1'=free_94, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_97>=2 && 0>=1+free_95 && 0>=1+free_94 ], cost: 1+free_270+D
    127: f21 -> [24] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_102, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_100, M'=free_100, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_101, Z'=free_19, A1'=free_99, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_102>=2 && 0>=1+free_100 && free_99>=1 ], cost: 1+free_270+D
    143: f21 -> [24] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_102, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_100, M'=free_100, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_101, Z'=free_19, A1'=free_99, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_102>=2 && 0>=1+free_100 && free_99>=1 ], cost: 1+free_270+D
    128: f21 -> [25] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_102, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_100, M'=free_100, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_101, Z'=free_19, A1'=free_99, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_102>=2 && 0>=1+free_100 && free_99>=1 ], cost: 1+free_270+D
    144: f21 -> [25] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_102, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_100, M'=free_100, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_101, Z'=free_19, A1'=free_99, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_102>=2 && 0>=1+free_100 && free_99>=1 ], cost: 1+free_270+D
    129: f21 -> [26] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_107, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_105, M'=free_105, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_106, Z'=free_19, A1'=free_104, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_107>=2 && free_105>=1 && 0>=1+free_104 ], cost: 1+free_270+D
    145: f21 -> [26] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_107, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_105, M'=free_105, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_106, Z'=free_19, A1'=free_104, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_107>=2 && free_105>=1 && 0>=1+free_104 ], cost: 1+free_270+D
    130: f21 -> [27] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_107, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_105, M'=free_105, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_106, Z'=free_19, A1'=free_104, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_107>=2 && free_105>=1 && 0>=1+free_104 ], cost: 1+free_270+D
    146: f21 -> [27] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_107, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_105, M'=free_105, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_106, Z'=free_19, A1'=free_104, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_107>=2 && free_105>=1 && 0>=1+free_104 ], cost: 1+free_270+D
    131: f21 -> [28] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_112, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_110, M'=free_110, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_111, Z'=free_19, A1'=free_109, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_112>=2 && free_110>=1 && free_109>=1 ], cost: 1+free_270+D
    147: f21 -> [28] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_112, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_110, M'=free_110, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_111, Z'=free_19, A1'=free_109, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_112>=2 && free_110>=1 && free_109>=1 ], cost: 1+free_270+D
    132: f21 -> [29] : A'=D, B'=free_5, C'=free_7, D'=-1, E'=1+D, F'=free_112, G'=free_1, H'=free_4, Q'=free_6, J'=free, K'=free_3, L'=free_110, M'=free_110, N'=free_19, O'=free_2, P'=free_18, Q_1'=-1+free_270, R'=free_111, Z'=free_19, A1'=free_109, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_112>=2 && free_110>=1 && free_109>=1 ], cost: 1+free_270+D
    148: f21 -> [29] : A'=D, B'=free_14, C'=free_16, D'=-1, E'=1+D, F'=free_112, G'=free_10, H'=free_13, Q'=free_15, J'=free_9, K'=free_12, L'=free_110, M'=free_110, N'=free_19, O'=free_11, P'=free_18, Q_1'=-1+free_270, R'=free_111, Z'=free_19, A1'=free_109, B1'=1+D, C1'=-1, T1'=free_272, U1'=free_269, [ free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_17>=2 && free_19>=1 && free_11>=free_17 && D>=free_17 && E==0 && 0>=0 && D>=0 && free_112>=2 && free_110>=1 && free_109>=1 ], cost: 1+free_270+D


Computing complexity for remaining 32 transitions.

  Found configuration with infinitely models for cost: 1+free_270+D
  and guard: free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_77>=2 && 0>=1+free_75 && 0>=1+free_74:
  free_19: Neg, E: Both, free_270: Pos, free_77: Pos, free_74: Neg, free_8: Const, free_2: Pos, free_75: Neg, D: Pos

Found new complexity INF, because: Found infinity configuration.


The final runtime is determined by this resulting transition:
  Final Guard: free_270>=2 && free_270>=3 && 2>=0 && free_270>=free_270 && free_270>=0 && free_8>=2 && 0>=1+free_19 && free_2>=free_8 && D>=free_8 && E==0 && 0>=0 && D>=0 && free_77>=2 && 0>=1+free_75 && 0>=1+free_74
  Final Cost:  1+free_270+D

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

WORST_CASE(INF,?)