Trying to load file: main.koat Initial Control flow graph problem: Start location: f2 0: f271 -> f281 : [ A>=1+B ], cost: 1 1: f271 -> f281 : [ B>=1+A ], cost: 1 71: f271 -> f223 : A'=-1+B, [ B1>=0 && B==A ], cost: 1 55: f271 -> f275 : A'=B, [ 0>=1+B1 && B==A ], cost: 1 57: f281 -> f290 : E'=free_52, T'=-1+A, X'=free_54, Y'=free_53, A1'=free_51, C1'=free_50, [ 29>=R ], cost: 1 58: f281 -> f290 : E'=free_57, T'=-1+A, X'=free_59, Y'=free_58, A1'=free_56, C1'=free_55, [ R>=31 ], cost: 1 59: f281 -> f290 : E'=free_62, R'=30, T'=-1+A, X'=free_64, Y'=free_63, A1'=free_61, C1'=free_60, [ R==30 ], cost: 1 2: f2 -> f7 : C'=0, D'=0, E'=0, [], cost: 1 3: f7 -> f16 : B'=1+G, D'=0, E'=0, Q'=0, [ F>=G && H>=G ], cost: 1 10: f7 -> f69 : B'=1+G, D'=0, E'=0, Q'=0, [ G>=1+H && F>=G ], cost: 1 111: f7 -> f136 : [ G>=1+F ], cost: 1 4: f16 -> f16 : A'=1+A, D'=free+D, J'=free, [ H>=A ], cost: 1 108: f16 -> f24 : [ 0>=1+D && A>=1+H ], cost: 1 109: f16 -> f24 : [ D>=1 && A>=1+H ], cost: 1 110: f16 -> f69 : D'=0, E'=0, Q'=0, [ A>=1+H && D==0 ], cost: 1 5: f24 -> f24 : A'=1+A, Q'=free_2*free_1+Q, [ H>=A ], cost: 1 106: f24 -> f42 : E'=-free_156, X'=free_158, Y'=-free_158*free_156-Q, M1'=free_157, N1'=free_156, O1'=free_156, [ free_158>=0 && A>=1+H ], cost: 1 107: f24 -> f42 : E'=free_159, X'=free_161, Y'=-Q+free_161*free_159, O1'=-free_159, P1'=free_160, Q1_1'=free_159, [ 0>=1+free_161 && A>=1+H ], cost: 1 6: f42 -> f45 : [ F>=K ], cost: 1 105: f42 -> f60 : [ K>=1+F ], cost: 1 7: f45 -> f45 : A'=1+A, Q'=free_3*free_4+Q, [ H>=A ], cost: 1 104: f45 -> f52 : X'=free_153, [ Q>=free_155*Y && free_155*Y+free_155>=1+Q && free_155>=free_153 && Q>=free_154*Y && free_154*Y+free_154>=1+Q && free_153>=free_154 && A>=1+H ], cost: 1 103: f52 -> f42 : K'=1+K, [ A>=1+H ], cost: 1 8: f52 -> f52 : A'=1+A, [ H>=A ], cost: 1 9: f60 -> f60 : A'=1+A, [ H>=A ], cost: 1 102: f60 -> f69 : D'=0, E'=0, Q'=0, [ A>=1+H ], cost: 1 11: f69 -> f72 : [ F>=1+G && H>=G ], cost: 1 12: f69 -> f72 : [ G>=1+F && H>=G ], cost: 1 20: f69 -> f130 : M'=C, N'=free_10, O'=free_11, P'=free_10+free_11, [ G>=1+H ], cost: 1 21: f69 -> f130 : F'=G, M'=C, N'=free_12, O'=free_13, P'=free_12+free_13, [ H>=F && G==F ], cost: 1 13: f72 -> f72 : A'=1+A, D'=free_5+D, L'=free_5, [ F>=A ], cost: 1 99: f72 -> f80 : [ 0>=1+D && A>=1+F ], cost: 1 100: f72 -> f80 : [ D>=1 && A>=1+F ], cost: 1 101: f72 -> f130 : D'=0, M'=C, N'=free_151, O'=free_152, P'=free_151+free_152, [ A>=1+F && D==0 ], cost: 1 14: f80 -> f80 : A'=1+A, Q'=Q+free_6*free_7, [ F>=A ], cost: 1 97: f80 -> f98 : E'=-free_145, X'=free_147, Y'=-Q-free_145*free_147, H1'=free_146, Q1'=free_145, J1'=free_145, [ free_147>=0 && A>=1+F ], cost: 1 98: f80 -> f98 : E'=free_148, X'=free_150, Y'=-Q+free_148*free_150, J1'=-free_148, K1'=free_149, L1'=free_148, [ 0>=1+free_150 && A>=1+F ], cost: 1 15: f98 -> f98 : A'=1+A, [ F>=A ], cost: 1 96: f98 -> f104 : [ A>=1+F ], cost: 1 16: f104 -> f107 : [ H>=K ], cost: 1 95: f104 -> f121 : [ K>=1+H ], cost: 1 17: f107 -> f107 : A'=1+A, Q'=Q+free_8*free_9, [ F>=A ], cost: 1 94: f107 -> f113 : [ A>=1+F ], cost: 1 93: f113 -> f104 : K'=1+K, [ A>=1+F ], cost: 1 18: f113 -> f113 : A'=1+A, [ F>=A ], cost: 1 19: f121 -> f121 : A'=1+A, [ F>=A ], cost: 1 92: f121 -> f130 : M'=C, N'=free_143, O'=free_144, P'=free_144+free_143, [ A>=1+F ], cost: 1 22: f130 -> f7 : C'=M, G'=1+G, [ M>=1+P ], cost: 1 23: f130 -> f7 : C'=P, G'=1+G, [ P>=M ], cost: 1 32: f136 -> f136 : B'=G, E'=free_16, G'=-1+G, [ G>=1 && G>=F ], cost: 1 24: f136 -> f141 : [ F>=1+G && 0>=1+E && G>=1 ], cost: 1 25: f136 -> f141 : [ F>=1+G && E>=1 && G>=1 ], cost: 1 30: f136 -> f164 : E'=0, [ G>=1 && F>=1+G && E==0 ], cost: 1 91: f136 -> f177 : [ 0>=G ], cost: 1 26: f141 -> f141 : K'=1+K, [ F>=K ], cost: 1 90: f141 -> f147 : [ K>=1+F ], cost: 1 27: f147 -> f150 : [ F>=K ], cost: 1 89: f147 -> f164 : [ K>=1+F ], cost: 1 28: f150 -> f150 : A'=1+A, Q'=Q+free_15*free_14, [ F>=A ], cost: 1 88: f150 -> f156 : [ A>=1+F ], cost: 1 87: f156 -> f147 : K'=1+K, [ A>=1+F ], cost: 1 29: f156 -> f156 : A'=1+A, [ F>=A ], cost: 1 86: f164 -> f136 : B'=G, E'=free_142, G'=-1+G, [ K>=1+F ], cost: 1 31: f164 -> f164 : K'=1+K, Q_1'=0, [ F>=K ], cost: 1 33: f177 -> f182 : B'=1+G, E'=free_17, [ G>=1 ], cost: 1 85: f177 -> f223 : [ 0>=G ], cost: 1 34: f182 -> f182 : K'=1+K, [ F>=K ], cost: 1 82: f182 -> f190 : E'=free_136, [ 0>=1+E && 1>=free_138*E && free_138+free_138*E>=2 && free_136>=free_138 && 1>=E*free_137 && E*free_137+free_137>=2 && free_137>=free_136 && K>=1+F ], cost: 1 83: f182 -> f190 : E'=free_139, [ E>=1 && 1>=free_141*E && free_141+free_141*E>=2 && free_139>=free_141 && 1>=E*free_140 && free_140+E*free_140>=2 && free_140>=free_139 && K>=1+F ], cost: 1 84: f182 -> f215 : E'=0, [ K>=1+F && E==0 ], cost: 1 35: f190 -> f193 : [ F>=K ], cost: 1 81: f190 -> f208 : [ K>=1+F ], cost: 1 36: f193 -> f193 : A'=1+A, Q'=Q+free_18*free_19, [ H>=A ], cost: 1 80: f193 -> f200 : X'=free_132, [ E*Q>=free_135*E*free_134 && free_135+free_135*E*free_134>=1+E*Q && free_135>=free_132 && E*Q>=E*free_133*free_134 && free_133+E*free_133*free_134>=1+E*Q && free_132>=free_133 && A>=1+H ], cost: 1 79: f200 -> f190 : K'=1+K, [ A>=1+H ], cost: 1 37: f200 -> f200 : A'=1+A, [ H>=A ], cost: 1 78: f208 -> f177 : G'=-1+G, [ K>=1+H ], cost: 1 38: f208 -> f208 : K'=1+K, [ H>=K ], cost: 1 77: f215 -> f177 : G'=-1+G, [ K>=1+H ], cost: 1 39: f215 -> f215 : K'=1+K, [ H>=K ], cost: 1 40: f223 -> f226 : [ A>=1 ], cost: 1 76: f223 -> f1 : [ 0>=A ], cost: 1 70: f226 -> f223 : A'=-1+A, [ R>=31 ], cost: 1 41: f226 -> f230 : S'=1, [ 30>=R ], cost: 1 42: f230 -> f241 : [ 0>=B ], cost: 1 43: f230 -> f241 : S'=0, T'=-1+B, U'=C-free_20, [ B>=1 ], cost: 1 44: f230 -> f238 : T'=-1+B, U'=free_21, V'=free_22, [ 0>=1+free_21 && B>=1 ], cost: 1 45: f230 -> f238 : T'=-1+B, U'=free_23, V'=free_24, [ free_23>=1 && B>=1 ], cost: 1 54: f241 -> f271 : S'=0, B1'=free_49, [ S==0 ], cost: 1 49: f241 -> f246 : Q'=1, W'=0, [ 0>=1+S ], cost: 1 50: f241 -> f246 : Q'=1, W'=0, [ S>=1 ], cost: 1 47: f238 -> f230 : B'=-1+B, [ 0>=1+V ], cost: 1 48: f238 -> f230 : B'=-1+B, [ V>=1 ], cost: 1 46: f238 -> f241 : [], cost: 1 74: f246 -> f271 : B1'=free_128, [ G>=1+A ], cost: 1 75: f246 -> f271 : X'=Q*free_131, Z'=-free_129+C, B1'=free_130, [ A>=G ], cost: 1 51: f246 -> f260 : E'=free_27, Q'=-free_28*Q*free_29, W'=free_25, X'=Q*free_29, Y'=free_26, Z'=free_30, [ 1>=free_28*free_35 && free_28+free_28*free_35>=2 && A>=G && 0>=1+free_30 && 1>=free_34*free_35 && free_34+free_34*free_35>=2 && free_26>=free_34 && 1>=free_35*free_32 && free_35*free_32+free_32>=2 && free_32>=free_26 && free_27>=free_27*free_35*free_33 && free_27*free_35*free_33+free_33>=1+free_27 && free_33>=free_25 && free_27>=free_27*free_31*free_35 && free_31+free_27*free_31*free_35>=1+free_27 && free_25>=free_31 ], cost: 1 52: f246 -> f260 : E'=free_38, Q'=-Q*free_39*free_40, W'=free_36, X'=Q*free_40, Y'=free_37, Z'=free_41, [ 1>=free_39*free_46 && free_39+free_39*free_46>=2 && A>=G && free_41>=1 && 1>=free_45*free_46 && free_45*free_46+free_45>=2 && free_37>=free_45 && 1>=free_46*free_43 && free_43+free_46*free_43>=2 && free_43>=free_37 && free_38>=free_44*free_38*free_46 && free_44+free_44*free_38*free_46>=1+free_38 && free_44>=free_36 && free_38>=free_38*free_42*free_46 && free_38*free_42*free_46+free_42>=1+free_38 && free_36>=free_42 ], cost: 1 73: f260 -> f246 : G'=1+G, [ K>=1+H ], cost: 1 53: f260 -> f260 : K'=1+K, A1'=free_47, B1'=free_48, [ H>=K ], cost: 1 72: f275 -> f223 : A'=-1+A, [ K>=1+F ], cost: 1 56: f275 -> f275 : K'=1+K, [ F>=K ], cost: 1 60: f290 -> f299 : Q'=1, W'=1, X'=free_65, D1'=free_66, E1'=free_66, [ X>=0 && A1*Y>=free_69*free_66*Y+X*free_69*Y && free_69+free_69*free_66*Y+X*free_69*Y>=1+A1*Y && free_69+C1^2>=B1^2+Y^2+free_68*C1 && free_68+B1^2+Y^2+free_68*C1>=1+free_69+C1^2 && free_68>=free_65 && A1*Y>=free_66*Y*free_67+X*Y*free_67 && free_66*Y*free_67+X*Y*free_67+free_67>=1+A1*Y && C1^2+free_67>=B1^2+Y^2+free_70*C1 && B1^2+Y^2+free_70+free_70*C1>=1+C1^2+free_67 && free_65>=free_70 ], cost: 1 61: f290 -> f299 : Q'=1, W'=1, X'=free_71, E1'=-free_72, F1'=free_72, [ 0>=1+X && free_75*free_72*Y+A1*Y>=X*free_75*Y && free_75+X*free_75*Y>=1+free_75*free_72*Y+A1*Y && free_75+C1^2>=B1^2+Y^2+C1*free_74 && B1^2+Y^2+C1*free_74+free_74>=1+free_75+C1^2 && free_74>=free_71 && free_72*Y*free_73+A1*Y>=X*Y*free_73 && X*Y*free_73+free_73>=1+free_72*Y*free_73+A1*Y && free_73+C1^2>=B1^2+Y^2+free_76*C1 && B1^2+Y^2+free_76+free_76*C1>=1+free_73+C1^2 && free_71>=free_76 ], cost: 1 69: f299 -> f226 : R'=1+R, [ K>=1+T ], cost: 1 62: f299 -> f315 : E'=free_82*free_79*W-free_80, G'=1+K, Q'=free_78, W'=free_85, X'=free_79*free_83*W+free_77, Y'=free_86, A1'=free_81, B1'=free_84, [ X>=free_84*free_82 && free_82+free_84*free_82>=1+X && Q*free_79*C1>=free_84*C1*free_80 && free_84*C1*free_80+free_80>=1+Q*free_79*C1 && X*C1>=free_84*C1*free_77 && free_84*C1*free_77+free_77>=1+X*C1 && Q*free_79>=free_84*free_83 && free_84*free_83+free_83>=1+Q*free_79 && Q*free_79>=free_84*free_91 && free_91+free_84*free_91>=1+Q*free_79 && free_91>=free_78 && Q*free_79>=free_84*free_94 && free_94+free_84*free_94>=1+Q*free_79 && free_78>=free_94 && free_87*Q*free_79>=free_87*free_84*free_90 && free_87*free_84*free_90+free_90>=1+free_87*Q*free_79 && free_90>=free_86 && free_87*Q*free_79>=free_87*free_84*free_93 && free_87*free_84*free_93+free_93>=1+free_87*Q*free_79 && free_86>=free_93 && T>=K && free_87*X>=free_87*free_84*free_95 && free_87*free_84*free_95+free_95>=1+free_87*X && free_95>=free_81 && free_87*X>=free_87*free_84*free_89 && free_89+free_87*free_84*free_89>=1+free_87*X && free_81>=free_89 && X>=free_84*free_92 && free_84*free_92+free_92>=1+X && free_92>=free_85 && X>=free_84*free_88 && free_88+free_84*free_88>=1+X && free_85>=free_88 ], cost: 1 63: f315 -> f315 : B1'=free_96, C1'=free_97, G1'=1+G1, [ F>=G1 ], cost: 1 66: f315 -> f332 : X'=E*W+A1*Q, B1'=0, C1'=-E*Q+A1*W, [ G1>=1+F ], cost: 1 67: f315 -> f332 : Q'=free_102, W'=free_101, X'=free_104+free_103, B1'=free_100, C1'=free_105-free_106, [ X*E>=free_113*free_104*X*E && free_104+free_113*free_104*X*E>=1+X*E && A1*Y>=free_113*A1*Y*free_103 && free_113*A1*Y*free_103+free_103>=1+A1*Y && A1*X>=free_113*A1*X*free_105 && free_113*A1*X*free_105+free_105>=1+A1*X && E*Y>=free_113*E*Y*free_106 && free_113*E*Y*free_106+free_106>=1+E*Y && 0>=1+free_113 && G1>=1+F && Y>=free_110*free_113*Y && free_110+free_110*free_113*Y>=1+Y && free_110>=free_102 && Y>=free_113*Y*free_112 && free_113*Y*free_112+free_112>=1+Y && free_102>=free_112 && 1>=free_113*free_109 && free_113*free_109+free_109>=2 && free_100>=free_109 && 1>=free_113*free_111 && free_111+free_113*free_111>=2 && free_111>=free_100 && X>=free_113*X*free_108 && free_108+free_113*X*free_108>=1+X && free_108>=free_101 && X>=free_113*free_107*X && free_107+free_113*free_107*X>=1+X && free_101>=free_107 ], cost: 1 68: f315 -> f332 : Q'=free_116, W'=free_115, X'=free_117+free_118, B1'=free_114, C1'=-free_120+free_119, [ X*E>=X*E*free_118*free_127 && X*E*free_118*free_127+free_118>=1+X*E && A1*Y>=A1*free_117*Y*free_127 && free_117+A1*free_117*Y*free_127>=1+A1*Y && A1*X>=A1*X*free_127*free_119 && A1*X*free_127*free_119+free_119>=1+A1*X && E*Y>=E*free_120*Y*free_127 && free_120+E*free_120*Y*free_127>=1+E*Y && free_127>=1 && G1>=1+F && Y>=free_124*Y*free_127 && free_124+free_124*Y*free_127>=1+Y && free_124>=free_116 && Y>=free_126*Y*free_127 && free_126+free_126*Y*free_127>=1+Y && free_116>=free_126 && 1>=free_123*free_127 && free_123+free_123*free_127>=2 && free_114>=free_123 && 1>=free_127*free_125 && free_125+free_127*free_125>=2 && free_125>=free_114 && X>=X*free_127*free_122 && X*free_127*free_122+free_122>=1+X && free_122>=free_115 && X>=X*free_121*free_127 && free_121+X*free_121*free_127>=1+X && free_115>=free_121 ], cost: 1 65: f332 -> f299 : K'=1+K, [ G1>=1+H ], cost: 1 64: f332 -> f332 : A1'=free_98, B1'=free_99, G1'=1+G1, [ H>=G1 ], cost: 1 Simplified the transitions: Start location: f2 0: f271 -> f281 : [ A>=1+B ], cost: 1 1: f271 -> f281 : [ B>=1+A ], cost: 1 71: f271 -> f223 : A'=-1+B, [ B1>=0 && B==A ], cost: 1 55: f271 -> f275 : A'=B, [ 0>=1+B1 && B==A ], cost: 1 57: f281 -> f290 : E'=free_52, T'=-1+A, X'=free_54, Y'=free_53, A1'=free_51, C1'=free_50, [ 29>=R ], cost: 1 58: f281 -> f290 : E'=free_57, T'=-1+A, X'=free_59, Y'=free_58, A1'=free_56, C1'=free_55, [ R>=31 ], cost: 1 59: f281 -> f290 : E'=free_62, R'=30, T'=-1+A, X'=free_64, Y'=free_63, A1'=free_61, C1'=free_60, [ R==30 ], cost: 1 2: f2 -> f7 : C'=0, D'=0, E'=0, [], cost: 1 3: f7 -> f16 : B'=1+G, D'=0, E'=0, Q'=0, [ F>=G && H>=G ], cost: 1 10: f7 -> f69 : B'=1+G, D'=0, E'=0, Q'=0, [ G>=1+H && F>=G ], cost: 1 111: f7 -> f136 : [ G>=1+F ], cost: 1 4: f16 -> f16 : A'=1+A, D'=free+D, J'=free, [ H>=A ], cost: 1 108: f16 -> f24 : [ 0>=1+D && A>=1+H ], cost: 1 109: f16 -> f24 : [ D>=1 && A>=1+H ], cost: 1 110: f16 -> f69 : D'=0, E'=0, Q'=0, [ A>=1+H && D==0 ], cost: 1 5: f24 -> f24 : A'=1+A, Q'=free_2*free_1+Q, [ H>=A ], cost: 1 106: f24 -> f42 : E'=-free_156, X'=free_158, Y'=-free_158*free_156-Q, M1'=free_157, N1'=free_156, O1'=free_156, [ free_158>=0 && A>=1+H ], cost: 1 107: f24 -> f42 : E'=free_159, X'=free_161, Y'=-Q+free_161*free_159, O1'=-free_159, P1'=free_160, Q1_1'=free_159, [ 0>=1+free_161 && A>=1+H ], cost: 1 6: f42 -> f45 : [ F>=K ], cost: 1 105: f42 -> f60 : [ K>=1+F ], cost: 1 7: f45 -> f45 : A'=1+A, Q'=free_3*free_4+Q, [ H>=A ], cost: 1 104: f45 -> f52 : X'=free_153, [ Q>=free_155*Y && free_155*Y+free_155>=1+Q && free_155>=free_153 && Q>=free_154*Y && free_154*Y+free_154>=1+Q && free_153>=free_154 && A>=1+H ], cost: 1 103: f52 -> f42 : K'=1+K, [ A>=1+H ], cost: 1 8: f52 -> f52 : A'=1+A, [ H>=A ], cost: 1 9: f60 -> f60 : A'=1+A, [ H>=A ], cost: 1 102: f60 -> f69 : D'=0, E'=0, Q'=0, [ A>=1+H ], cost: 1 11: f69 -> f72 : [ F>=1+G && H>=G ], cost: 1 12: f69 -> f72 : [ G>=1+F && H>=G ], cost: 1 20: f69 -> f130 : M'=C, N'=free_10, O'=free_11, P'=free_10+free_11, [ G>=1+H ], cost: 1 21: f69 -> f130 : F'=G, M'=C, N'=free_12, O'=free_13, P'=free_12+free_13, [ H>=F && G==F ], cost: 1 13: f72 -> f72 : A'=1+A, D'=free_5+D, L'=free_5, [ F>=A ], cost: 1 99: f72 -> f80 : [ 0>=1+D && A>=1+F ], cost: 1 100: f72 -> f80 : [ D>=1 && A>=1+F ], cost: 1 101: f72 -> f130 : D'=0, M'=C, N'=free_151, O'=free_152, P'=free_151+free_152, [ A>=1+F && D==0 ], cost: 1 14: f80 -> f80 : A'=1+A, Q'=Q+free_6*free_7, [ F>=A ], cost: 1 97: f80 -> f98 : E'=-free_145, X'=free_147, Y'=-Q-free_145*free_147, H1'=free_146, Q1'=free_145, J1'=free_145, [ free_147>=0 && A>=1+F ], cost: 1 98: f80 -> f98 : E'=free_148, X'=free_150, Y'=-Q+free_148*free_150, J1'=-free_148, K1'=free_149, L1'=free_148, [ 0>=1+free_150 && A>=1+F ], cost: 1 15: f98 -> f98 : A'=1+A, [ F>=A ], cost: 1 96: f98 -> f104 : [ A>=1+F ], cost: 1 16: f104 -> f107 : [ H>=K ], cost: 1 95: f104 -> f121 : [ K>=1+H ], cost: 1 17: f107 -> f107 : A'=1+A, Q'=Q+free_8*free_9, [ F>=A ], cost: 1 94: f107 -> f113 : [ A>=1+F ], cost: 1 93: f113 -> f104 : K'=1+K, [ A>=1+F ], cost: 1 18: f113 -> f113 : A'=1+A, [ F>=A ], cost: 1 19: f121 -> f121 : A'=1+A, [ F>=A ], cost: 1 92: f121 -> f130 : M'=C, N'=free_143, O'=free_144, P'=free_144+free_143, [ A>=1+F ], cost: 1 22: f130 -> f7 : C'=M, G'=1+G, [ M>=1+P ], cost: 1 23: f130 -> f7 : C'=P, G'=1+G, [ P>=M ], cost: 1 32: f136 -> f136 : B'=G, E'=free_16, G'=-1+G, [ G>=1 && G>=F ], cost: 1 24: f136 -> f141 : [ F>=1+G && 0>=1+E && G>=1 ], cost: 1 25: f136 -> f141 : [ F>=1+G && E>=1 && G>=1 ], cost: 1 30: f136 -> f164 : E'=0, [ G>=1 && F>=1+G && E==0 ], cost: 1 91: f136 -> f177 : [ 0>=G ], cost: 1 26: f141 -> f141 : K'=1+K, [ F>=K ], cost: 1 90: f141 -> f147 : [ K>=1+F ], cost: 1 27: f147 -> f150 : [ F>=K ], cost: 1 89: f147 -> f164 : [ K>=1+F ], cost: 1 28: f150 -> f150 : A'=1+A, Q'=Q+free_15*free_14, [ F>=A ], cost: 1 88: f150 -> f156 : [ A>=1+F ], cost: 1 87: f156 -> f147 : K'=1+K, [ A>=1+F ], cost: 1 29: f156 -> f156 : A'=1+A, [ F>=A ], cost: 1 86: f164 -> f136 : B'=G, E'=free_142, G'=-1+G, [ K>=1+F ], cost: 1 31: f164 -> f164 : K'=1+K, Q_1'=0, [ F>=K ], cost: 1 33: f177 -> f182 : B'=1+G, E'=free_17, [ G>=1 ], cost: 1 85: f177 -> f223 : [ 0>=G ], cost: 1 34: f182 -> f182 : K'=1+K, [ F>=K ], cost: 1 82: f182 -> f190 : E'=free_136, [ 0>=1+E && 1>=free_138*E && free_138+free_138*E>=2 && free_136>=free_138 && 1>=E*free_137 && E*free_137+free_137>=2 && free_137>=free_136 && K>=1+F ], cost: 1 83: f182 -> f190 : E'=free_139, [ E>=1 && 1>=free_141*E && free_141+free_141*E>=2 && free_139>=free_141 && 1>=E*free_140 && free_140+E*free_140>=2 && free_140>=free_139 && K>=1+F ], cost: 1 84: f182 -> f215 : E'=0, [ K>=1+F && E==0 ], cost: 1 35: f190 -> f193 : [ F>=K ], cost: 1 81: f190 -> f208 : [ K>=1+F ], cost: 1 36: f193 -> f193 : A'=1+A, Q'=Q+free_18*free_19, [ H>=A ], cost: 1 80: f193 -> f200 : X'=free_132, [ E*Q>=free_135*E*free_134 && free_135+free_135*E*free_134>=1+E*Q && free_135>=free_132 && E*Q>=E*free_133*free_134 && free_133+E*free_133*free_134>=1+E*Q && free_132>=free_133 && A>=1+H ], cost: 1 79: f200 -> f190 : K'=1+K, [ A>=1+H ], cost: 1 37: f200 -> f200 : A'=1+A, [ H>=A ], cost: 1 78: f208 -> f177 : G'=-1+G, [ K>=1+H ], cost: 1 38: f208 -> f208 : K'=1+K, [ H>=K ], cost: 1 77: f215 -> f177 : G'=-1+G, [ K>=1+H ], cost: 1 39: f215 -> f215 : K'=1+K, [ H>=K ], cost: 1 40: f223 -> f226 : [ A>=1 ], cost: 1 70: f226 -> f223 : A'=-1+A, [ R>=31 ], cost: 1 41: f226 -> f230 : S'=1, [ 30>=R ], cost: 1 42: f230 -> f241 : [ 0>=B ], cost: 1 43: f230 -> f241 : S'=0, T'=-1+B, U'=C-free_20, [ B>=1 ], cost: 1 44: f230 -> f238 : T'=-1+B, U'=free_21, V'=free_22, [ 0>=1+free_21 && B>=1 ], cost: 1 45: f230 -> f238 : T'=-1+B, U'=free_23, V'=free_24, [ free_23>=1 && B>=1 ], cost: 1 54: f241 -> f271 : S'=0, B1'=free_49, [ S==0 ], cost: 1 49: f241 -> f246 : Q'=1, W'=0, [ 0>=1+S ], cost: 1 50: f241 -> f246 : Q'=1, W'=0, [ S>=1 ], cost: 1 47: f238 -> f230 : B'=-1+B, [ 0>=1+V ], cost: 1 48: f238 -> f230 : B'=-1+B, [ V>=1 ], cost: 1 46: f238 -> f241 : [], cost: 1 74: f246 -> f271 : B1'=free_128, [ G>=1+A ], cost: 1 75: f246 -> f271 : X'=Q*free_131, Z'=-free_129+C, B1'=free_130, [ A>=G ], cost: 1 51: f246 -> f260 : E'=free_27, Q'=-free_28*Q*free_29, W'=free_25, X'=Q*free_29, Y'=free_26, Z'=free_30, [ 1>=free_28*free_35 && free_28+free_28*free_35>=2 && A>=G && 0>=1+free_30 && 1>=free_34*free_35 && free_34+free_34*free_35>=2 && free_26>=free_34 && 1>=free_35*free_32 && free_35*free_32+free_32>=2 && free_32>=free_26 && free_27>=free_27*free_35*free_33 && free_27*free_35*free_33+free_33>=1+free_27 && free_33>=free_25 && free_27>=free_27*free_31*free_35 && free_31+free_27*free_31*free_35>=1+free_27 && free_25>=free_31 ], cost: 1 52: f246 -> f260 : E'=free_38, Q'=-Q*free_39*free_40, W'=free_36, X'=Q*free_40, Y'=free_37, Z'=free_41, [ 1>=free_39*free_46 && free_39+free_39*free_46>=2 && A>=G && free_41>=1 && 1>=free_45*free_46 && free_45*free_46+free_45>=2 && free_37>=free_45 && 1>=free_46*free_43 && free_43+free_46*free_43>=2 && free_43>=free_37 && free_38>=free_44*free_38*free_46 && free_44+free_44*free_38*free_46>=1+free_38 && free_44>=free_36 && free_38>=free_38*free_42*free_46 && free_38*free_42*free_46+free_42>=1+free_38 && free_36>=free_42 ], cost: 1 73: f260 -> f246 : G'=1+G, [ K>=1+H ], cost: 1 53: f260 -> f260 : K'=1+K, A1'=free_47, B1'=free_48, [ H>=K ], cost: 1 72: f275 -> f223 : A'=-1+A, [ K>=1+F ], cost: 1 56: f275 -> f275 : K'=1+K, [ F>=K ], cost: 1 60: f290 -> f299 : Q'=1, W'=1, X'=free_65, D1'=free_66, E1'=free_66, [ X>=0 && A1*Y>=free_69*free_66*Y+X*free_69*Y && free_69+free_69*free_66*Y+X*free_69*Y>=1+A1*Y && free_69+C1^2>=B1^2+Y^2+free_68*C1 && free_68+B1^2+Y^2+free_68*C1>=1+free_69+C1^2 && free_68>=free_65 && A1*Y>=free_66*Y*free_67+X*Y*free_67 && free_66*Y*free_67+X*Y*free_67+free_67>=1+A1*Y && C1^2+free_67>=B1^2+Y^2+free_70*C1 && B1^2+Y^2+free_70+free_70*C1>=1+C1^2+free_67 && free_65>=free_70 ], cost: 1 61: f290 -> f299 : Q'=1, W'=1, X'=free_71, E1'=-free_72, F1'=free_72, [ 0>=1+X && free_75*free_72*Y+A1*Y>=X*free_75*Y && free_75+X*free_75*Y>=1+free_75*free_72*Y+A1*Y && free_75+C1^2>=B1^2+Y^2+C1*free_74 && B1^2+Y^2+C1*free_74+free_74>=1+free_75+C1^2 && free_74>=free_71 && free_72*Y*free_73+A1*Y>=X*Y*free_73 && X*Y*free_73+free_73>=1+free_72*Y*free_73+A1*Y && free_73+C1^2>=B1^2+Y^2+free_76*C1 && B1^2+Y^2+free_76+free_76*C1>=1+free_73+C1^2 && free_71>=free_76 ], cost: 1 69: f299 -> f226 : R'=1+R, [ K>=1+T ], cost: 1 62: f299 -> f315 : E'=free_82*free_79*W-free_80, G'=1+K, Q'=free_78, W'=free_85, X'=free_79*free_83*W+free_77, Y'=free_86, A1'=free_81, B1'=free_84, [ X>=free_84*free_82 && free_82+free_84*free_82>=1+X && Q*free_79*C1>=free_84*C1*free_80 && free_84*C1*free_80+free_80>=1+Q*free_79*C1 && X*C1>=free_84*C1*free_77 && free_84*C1*free_77+free_77>=1+X*C1 && Q*free_79>=free_84*free_83 && free_84*free_83+free_83>=1+Q*free_79 && Q*free_79>=free_84*free_91 && free_91+free_84*free_91>=1+Q*free_79 && free_91>=free_78 && Q*free_79>=free_84*free_94 && free_94+free_84*free_94>=1+Q*free_79 && free_78>=free_94 && free_87*Q*free_79>=free_87*free_84*free_90 && free_87*free_84*free_90+free_90>=1+free_87*Q*free_79 && free_90>=free_86 && free_87*Q*free_79>=free_87*free_84*free_93 && free_87*free_84*free_93+free_93>=1+free_87*Q*free_79 && free_86>=free_93 && T>=K && free_87*X>=free_87*free_84*free_95 && free_87*free_84*free_95+free_95>=1+free_87*X && free_95>=free_81 && free_87*X>=free_87*free_84*free_89 && free_89+free_87*free_84*free_89>=1+free_87*X && free_81>=free_89 && X>=free_84*free_92 && free_84*free_92+free_92>=1+X && free_92>=free_85 && X>=free_84*free_88 && free_88+free_84*free_88>=1+X && free_85>=free_88 ], cost: 1 63: f315 -> f315 : B1'=free_96, C1'=free_97, G1'=1+G1, [ F>=G1 ], cost: 1 66: f315 -> f332 : X'=E*W+A1*Q, B1'=0, C1'=-E*Q+A1*W, [ G1>=1+F ], cost: 1 67: f315 -> f332 : Q'=free_102, W'=free_101, X'=free_104+free_103, B1'=free_100, C1'=free_105-free_106, [ X*E>=free_113*free_104*X*E && free_104+free_113*free_104*X*E>=1+X*E && A1*Y>=free_113*A1*Y*free_103 && free_113*A1*Y*free_103+free_103>=1+A1*Y && A1*X>=free_113*A1*X*free_105 && free_113*A1*X*free_105+free_105>=1+A1*X && E*Y>=free_113*E*Y*free_106 && free_113*E*Y*free_106+free_106>=1+E*Y && 0>=1+free_113 && G1>=1+F && Y>=free_110*free_113*Y && free_110+free_110*free_113*Y>=1+Y && free_110>=free_102 && Y>=free_113*Y*free_112 && free_113*Y*free_112+free_112>=1+Y && free_102>=free_112 && 1>=free_113*free_109 && free_113*free_109+free_109>=2 && free_100>=free_109 && 1>=free_113*free_111 && free_111+free_113*free_111>=2 && free_111>=free_100 && X>=free_113*X*free_108 && free_108+free_113*X*free_108>=1+X && free_108>=free_101 && X>=free_113*free_107*X && free_107+free_113*free_107*X>=1+X && free_101>=free_107 ], cost: 1 68: f315 -> f332 : Q'=free_116, W'=free_115, X'=free_117+free_118, B1'=free_114, C1'=-free_120+free_119, [ X*E>=X*E*free_118*free_127 && X*E*free_118*free_127+free_118>=1+X*E && A1*Y>=A1*free_117*Y*free_127 && free_117+A1*free_117*Y*free_127>=1+A1*Y && A1*X>=A1*X*free_127*free_119 && A1*X*free_127*free_119+free_119>=1+A1*X && E*Y>=E*free_120*Y*free_127 && free_120+E*free_120*Y*free_127>=1+E*Y && free_127>=1 && G1>=1+F && Y>=free_124*Y*free_127 && free_124+free_124*Y*free_127>=1+Y && free_124>=free_116 && Y>=free_126*Y*free_127 && free_126+free_126*Y*free_127>=1+Y && free_116>=free_126 && 1>=free_123*free_127 && free_123+free_123*free_127>=2 && free_114>=free_123 && 1>=free_127*free_125 && free_125+free_127*free_125>=2 && free_125>=free_114 && X>=X*free_127*free_122 && X*free_127*free_122+free_122>=1+X && free_122>=free_115 && X>=X*free_121*free_127 && free_121+X*free_121*free_127>=1+X && free_115>=free_121 ], cost: 1 65: f332 -> f299 : K'=1+K, [ G1>=1+H ], cost: 1 64: f332 -> f332 : A1'=free_98, B1'=free_99, G1'=1+G1, [ H>=G1 ], cost: 1 Eliminating 1 self-loops for location f16 Self-Loop 4 has the metering function: 1+H-A, resulting in the new transition 112. Removing the self-loops: 4. Eliminating 1 self-loops for location f24 Self-Loop 5 has the metering function: 1+H-A, resulting in the new transition 113. Removing the self-loops: 5. Eliminating 1 self-loops for location f45 Self-Loop 7 has the metering function: 1+H-A, resulting in the new transition 114. Removing the self-loops: 7. Eliminating 1 self-loops for location f52 Self-Loop 8 has the metering function: 1+H-A, resulting in the new transition 115. Removing the self-loops: 8. Eliminating 1 self-loops for location f60 Self-Loop 9 has the metering function: 1+H-A, resulting in the new transition 116. Removing the self-loops: 9. Eliminating 1 self-loops for location f72 Self-Loop 13 has the metering function: 1+F-A, resulting in the new transition 117. Removing the self-loops: 13. Eliminating 1 self-loops for location f80 Self-Loop 14 has the metering function: 1+F-A, resulting in the new transition 118. Removing the self-loops: 14. Eliminating 1 self-loops for location f98 Self-Loop 15 has the metering function: 1+F-A, resulting in the new transition 119. Removing the self-loops: 15. Eliminating 1 self-loops for location f107 Self-Loop 17 has the metering function: 1+F-A, resulting in the new transition 120. Removing the self-loops: 17. Eliminating 1 self-loops for location f113 Self-Loop 18 has the metering function: 1+F-A, resulting in the new transition 121. Removing the self-loops: 18. Eliminating 1 self-loops for location f121 Self-Loop 19 has the metering function: 1+F-A, resulting in the new transition 122. Removing the self-loops: 19. Eliminating 1 self-loops for location f136 Removing the self-loops: 32. Adding an epsilon transition (to model nonexecution of the loops): 124. Eliminating 1 self-loops for location f141 Self-Loop 26 has the metering function: 1-K+F, resulting in the new transition 125. Removing the self-loops: 26. Eliminating 1 self-loops for location f150 Self-Loop 28 has the metering function: 1+F-A, resulting in the new transition 126. Removing the self-loops: 28. Eliminating 1 self-loops for location f156 Self-Loop 29 has the metering function: 1+F-A, resulting in the new transition 127. Removing the self-loops: 29. Eliminating 1 self-loops for location f164 Self-Loop 31 has the metering function: 1-K+F, resulting in the new transition 128. Removing the self-loops: 31. Eliminating 1 self-loops for location f182 Self-Loop 34 has the metering function: 1-K+F, resulting in the new transition 129. Removing the self-loops: 34. Eliminating 1 self-loops for location f193 Self-Loop 36 has the metering function: 1+H-A, resulting in the new transition 130. Removing the self-loops: 36. Eliminating 1 self-loops for location f200 Self-Loop 37 has the metering function: 1+H-A, resulting in the new transition 131. Removing the self-loops: 37. Eliminating 1 self-loops for location f208 Self-Loop 38 has the metering function: 1-K+H, resulting in the new transition 132. Removing the self-loops: 38. Eliminating 1 self-loops for location f215 Self-Loop 39 has the metering function: 1-K+H, resulting in the new transition 133. Removing the self-loops: 39. Eliminating 1 self-loops for location f260 Self-Loop 53 has the metering function: 1-K+H, resulting in the new transition 134. Removing the self-loops: 53. Eliminating 1 self-loops for location f275 Self-Loop 56 has the metering function: 1-K+F, resulting in the new transition 135. Removing the self-loops: 56. Eliminating 1 self-loops for location f315 Self-Loop 63 has the metering function: 1+F-G1, resulting in the new transition 136. Removing the self-loops: 63. Eliminating 1 self-loops for location f332 Self-Loop 64 has the metering function: 1+H-G1, resulting in the new transition 137. Removing the self-loops: 64. Removed all Self-loops using metering functions (where possible): Start location: f2 0: f271 -> f281 : [ A>=1+B ], cost: 1 1: f271 -> f281 : [ B>=1+A ], cost: 1 71: f271 -> f223 : A'=-1+B, [ B1>=0 && B==A ], cost: 1 55: f271 -> f275 : A'=B, [ 0>=1+B1 && B==A ], cost: 1 57: f281 -> f290 : E'=free_52, T'=-1+A, X'=free_54, Y'=free_53, A1'=free_51, C1'=free_50, [ 29>=R ], cost: 1 58: f281 -> f290 : E'=free_57, T'=-1+A, X'=free_59, Y'=free_58, A1'=free_56, C1'=free_55, [ R>=31 ], cost: 1 59: f281 -> f290 : E'=free_62, R'=30, T'=-1+A, X'=free_64, Y'=free_63, A1'=free_61, C1'=free_60, [ R==30 ], cost: 1 2: f2 -> f7 : C'=0, D'=0, E'=0, [], cost: 1 3: f7 -> f16 : B'=1+G, D'=0, E'=0, Q'=0, [ F>=G && H>=G ], cost: 1 10: f7 -> f69 : B'=1+G, D'=0, E'=0, Q'=0, [ G>=1+H && F>=G ], cost: 1 111: f7 -> f136 : [ G>=1+F ], cost: 1 112: f16 -> [45] : A'=1+H, D'=(1+H-A)*free+D, J'=free, [ H>=A ], cost: 1+H-A 113: f24 -> [46] : A'=1+H, Q'=Q+free_2*(1+H-A)*free_1, [ H>=A ], cost: 1+H-A 6: f42 -> f45 : [ F>=K ], cost: 1 105: f42 -> f60 : [ K>=1+F ], cost: 1 114: f45 -> [47] : A'=1+H, Q'=(1+H-A)*free_3*free_4+Q, [ H>=A ], cost: 1+H-A 115: f52 -> [48] : A'=1+H, [ H>=A ], cost: 1+H-A 116: f60 -> [49] : A'=1+H, [ H>=A ], cost: 1+H-A 11: f69 -> f72 : [ F>=1+G && H>=G ], cost: 1 12: f69 -> f72 : [ G>=1+F && H>=G ], cost: 1 20: f69 -> f130 : M'=C, N'=free_10, O'=free_11, P'=free_10+free_11, [ G>=1+H ], cost: 1 21: f69 -> f130 : F'=G, M'=C, N'=free_12, O'=free_13, P'=free_12+free_13, [ H>=F && G==F ], cost: 1 117: f72 -> [50] : A'=1+F, D'=free_5*(1+F-A)+D, L'=free_5, [ F>=A ], cost: 1+F-A 118: f80 -> [51] : A'=1+F, Q'=(1+F-A)*free_6*free_7+Q, [ F>=A ], cost: 1+F-A 119: f98 -> [52] : A'=1+F, [ F>=A ], cost: 1+F-A 16: f104 -> f107 : [ H>=K ], cost: 1 95: f104 -> f121 : [ K>=1+H ], cost: 1 120: f107 -> [53] : A'=1+F, Q'=free_8*(1+F-A)*free_9+Q, [ F>=A ], cost: 1+F-A 121: f113 -> [54] : A'=1+F, [ F>=A ], cost: 1+F-A 122: f121 -> [55] : A'=1+F, [ F>=A ], cost: 1+F-A 22: f130 -> f7 : C'=M, G'=1+G, [ M>=1+P ], cost: 1 23: f130 -> f7 : C'=P, G'=1+G, [ P>=M ], cost: 1 123: f136 -> [56] : B'=G, E'=free_16, G'=-1+G, [ G>=1 && G>=F ], cost: 1 124: f136 -> [56] : [], cost: 0 125: f141 -> [57] : K'=1+F, [ F>=K ], cost: 1-K+F 27: f147 -> f150 : [ F>=K ], cost: 1 89: f147 -> f164 : [ K>=1+F ], cost: 1 126: f150 -> [58] : A'=1+F, Q'=(1+F-A)*free_15*free_14+Q, [ F>=A ], cost: 1+F-A 127: f156 -> [59] : A'=1+F, [ F>=A ], cost: 1+F-A 128: f164 -> [60] : K'=1+F, Q_1'=0, [ F>=K ], cost: 1-K+F 33: f177 -> f182 : B'=1+G, E'=free_17, [ G>=1 ], cost: 1 85: f177 -> f223 : [ 0>=G ], cost: 1 129: f182 -> [61] : K'=1+F, [ F>=K ], cost: 1-K+F 35: f190 -> f193 : [ F>=K ], cost: 1 81: f190 -> f208 : [ K>=1+F ], cost: 1 130: f193 -> [62] : A'=1+H, Q'=Q+(1+H-A)*free_18*free_19, [ H>=A ], cost: 1+H-A 131: f200 -> [63] : A'=1+H, [ H>=A ], cost: 1+H-A 132: f208 -> [64] : K'=1+H, [ H>=K ], cost: 1-K+H 133: f215 -> [65] : K'=1+H, [ H>=K ], cost: 1-K+H 40: f223 -> f226 : [ A>=1 ], cost: 1 70: f226 -> f223 : A'=-1+A, [ R>=31 ], cost: 1 41: f226 -> f230 : S'=1, [ 30>=R ], cost: 1 42: f230 -> f241 : [ 0>=B ], cost: 1 43: f230 -> f241 : S'=0, T'=-1+B, U'=C-free_20, [ B>=1 ], cost: 1 44: f230 -> f238 : T'=-1+B, U'=free_21, V'=free_22, [ 0>=1+free_21 && B>=1 ], cost: 1 45: f230 -> f238 : T'=-1+B, U'=free_23, V'=free_24, [ free_23>=1 && B>=1 ], cost: 1 54: f241 -> f271 : S'=0, B1'=free_49, [ S==0 ], cost: 1 49: f241 -> f246 : Q'=1, W'=0, [ 0>=1+S ], cost: 1 50: f241 -> f246 : Q'=1, W'=0, [ S>=1 ], cost: 1 47: f238 -> f230 : B'=-1+B, [ 0>=1+V ], cost: 1 48: f238 -> f230 : B'=-1+B, [ V>=1 ], cost: 1 46: f238 -> f241 : [], cost: 1 74: f246 -> f271 : B1'=free_128, [ G>=1+A ], cost: 1 75: f246 -> f271 : X'=Q*free_131, Z'=-free_129+C, B1'=free_130, [ A>=G ], cost: 1 51: f246 -> f260 : E'=free_27, Q'=-free_28*Q*free_29, W'=free_25, X'=Q*free_29, Y'=free_26, Z'=free_30, [ 1>=free_28*free_35 && free_28+free_28*free_35>=2 && A>=G && 0>=1+free_30 && 1>=free_34*free_35 && free_34+free_34*free_35>=2 && free_26>=free_34 && 1>=free_35*free_32 && free_35*free_32+free_32>=2 && free_32>=free_26 && free_27>=free_27*free_35*free_33 && free_27*free_35*free_33+free_33>=1+free_27 && free_33>=free_25 && free_27>=free_27*free_31*free_35 && free_31+free_27*free_31*free_35>=1+free_27 && free_25>=free_31 ], cost: 1 52: f246 -> f260 : E'=free_38, Q'=-Q*free_39*free_40, W'=free_36, X'=Q*free_40, Y'=free_37, Z'=free_41, [ 1>=free_39*free_46 && free_39+free_39*free_46>=2 && A>=G && free_41>=1 && 1>=free_45*free_46 && free_45*free_46+free_45>=2 && free_37>=free_45 && 1>=free_46*free_43 && free_43+free_46*free_43>=2 && free_43>=free_37 && free_38>=free_44*free_38*free_46 && free_44+free_44*free_38*free_46>=1+free_38 && free_44>=free_36 && free_38>=free_38*free_42*free_46 && free_38*free_42*free_46+free_42>=1+free_38 && free_36>=free_42 ], cost: 1 134: f260 -> [66] : K'=1+H, A1'=free_47, B1'=free_48, [ H>=K ], cost: 1-K+H 135: f275 -> [67] : K'=1+F, [ F>=K ], cost: 1-K+F 60: f290 -> f299 : Q'=1, W'=1, X'=free_65, D1'=free_66, E1'=free_66, [ X>=0 && A1*Y>=free_69*free_66*Y+X*free_69*Y && free_69+free_69*free_66*Y+X*free_69*Y>=1+A1*Y && free_69+C1^2>=B1^2+Y^2+free_68*C1 && free_68+B1^2+Y^2+free_68*C1>=1+free_69+C1^2 && free_68>=free_65 && A1*Y>=free_66*Y*free_67+X*Y*free_67 && free_66*Y*free_67+X*Y*free_67+free_67>=1+A1*Y && C1^2+free_67>=B1^2+Y^2+free_70*C1 && B1^2+Y^2+free_70+free_70*C1>=1+C1^2+free_67 && free_65>=free_70 ], cost: 1 61: f290 -> f299 : Q'=1, W'=1, X'=free_71, E1'=-free_72, F1'=free_72, [ 0>=1+X && free_75*free_72*Y+A1*Y>=X*free_75*Y && free_75+X*free_75*Y>=1+free_75*free_72*Y+A1*Y && free_75+C1^2>=B1^2+Y^2+C1*free_74 && B1^2+Y^2+C1*free_74+free_74>=1+free_75+C1^2 && free_74>=free_71 && free_72*Y*free_73+A1*Y>=X*Y*free_73 && X*Y*free_73+free_73>=1+free_72*Y*free_73+A1*Y && free_73+C1^2>=B1^2+Y^2+free_76*C1 && B1^2+Y^2+free_76+free_76*C1>=1+free_73+C1^2 && free_71>=free_76 ], cost: 1 69: f299 -> f226 : R'=1+R, [ K>=1+T ], cost: 1 62: f299 -> f315 : E'=free_82*free_79*W-free_80, G'=1+K, Q'=free_78, W'=free_85, X'=free_79*free_83*W+free_77, Y'=free_86, A1'=free_81, B1'=free_84, [ X>=free_84*free_82 && free_82+free_84*free_82>=1+X && Q*free_79*C1>=free_84*C1*free_80 && free_84*C1*free_80+free_80>=1+Q*free_79*C1 && X*C1>=free_84*C1*free_77 && free_84*C1*free_77+free_77>=1+X*C1 && Q*free_79>=free_84*free_83 && free_84*free_83+free_83>=1+Q*free_79 && Q*free_79>=free_84*free_91 && free_91+free_84*free_91>=1+Q*free_79 && free_91>=free_78 && Q*free_79>=free_84*free_94 && free_94+free_84*free_94>=1+Q*free_79 && free_78>=free_94 && free_87*Q*free_79>=free_87*free_84*free_90 && free_87*free_84*free_90+free_90>=1+free_87*Q*free_79 && free_90>=free_86 && free_87*Q*free_79>=free_87*free_84*free_93 && free_87*free_84*free_93+free_93>=1+free_87*Q*free_79 && free_86>=free_93 && T>=K && free_87*X>=free_87*free_84*free_95 && free_87*free_84*free_95+free_95>=1+free_87*X && free_95>=free_81 && free_87*X>=free_87*free_84*free_89 && free_89+free_87*free_84*free_89>=1+free_87*X && free_81>=free_89 && X>=free_84*free_92 && free_84*free_92+free_92>=1+X && free_92>=free_85 && X>=free_84*free_88 && free_88+free_84*free_88>=1+X && free_85>=free_88 ], cost: 1 136: f315 -> [68] : B1'=free_96, C1'=free_97, G1'=1+F, [ F>=G1 ], cost: 1+F-G1 137: f332 -> [69] : A1'=free_98, B1'=free_99, G1'=1+H, [ H>=G1 ], cost: 1+H-G1 108: [45] -> f24 : [ 0>=1+D && A>=1+H ], cost: 1 109: [45] -> f24 : [ D>=1 && A>=1+H ], cost: 1 110: [45] -> f69 : D'=0, E'=0, Q'=0, [ A>=1+H && D==0 ], cost: 1 106: [46] -> f42 : E'=-free_156, X'=free_158, Y'=-free_158*free_156-Q, M1'=free_157, N1'=free_156, O1'=free_156, [ free_158>=0 && A>=1+H ], cost: 1 107: [46] -> f42 : E'=free_159, X'=free_161, Y'=-Q+free_161*free_159, O1'=-free_159, P1'=free_160, Q1_1'=free_159, [ 0>=1+free_161 && A>=1+H ], cost: 1 104: [47] -> f52 : X'=free_153, [ Q>=free_155*Y && free_155*Y+free_155>=1+Q && free_155>=free_153 && Q>=free_154*Y && free_154*Y+free_154>=1+Q && free_153>=free_154 && A>=1+H ], cost: 1 103: [48] -> f42 : K'=1+K, [ A>=1+H ], cost: 1 102: [49] -> f69 : D'=0, E'=0, Q'=0, [ A>=1+H ], cost: 1 99: [50] -> f80 : [ 0>=1+D && A>=1+F ], cost: 1 100: [50] -> f80 : [ D>=1 && A>=1+F ], cost: 1 101: [50] -> f130 : D'=0, M'=C, N'=free_151, O'=free_152, P'=free_151+free_152, [ A>=1+F && D==0 ], cost: 1 97: [51] -> f98 : E'=-free_145, X'=free_147, Y'=-Q-free_145*free_147, H1'=free_146, Q1'=free_145, J1'=free_145, [ free_147>=0 && A>=1+F ], cost: 1 98: [51] -> f98 : E'=free_148, X'=free_150, Y'=-Q+free_148*free_150, J1'=-free_148, K1'=free_149, L1'=free_148, [ 0>=1+free_150 && A>=1+F ], cost: 1 96: [52] -> f104 : [ A>=1+F ], cost: 1 94: [53] -> f113 : [ A>=1+F ], cost: 1 93: [54] -> f104 : K'=1+K, [ A>=1+F ], cost: 1 92: [55] -> f130 : M'=C, N'=free_143, O'=free_144, P'=free_144+free_143, [ A>=1+F ], cost: 1 24: [56] -> f141 : [ F>=1+G && 0>=1+E && G>=1 ], cost: 1 25: [56] -> f141 : [ F>=1+G && E>=1 && G>=1 ], cost: 1 30: [56] -> f164 : E'=0, [ G>=1 && F>=1+G && E==0 ], cost: 1 91: [56] -> f177 : [ 0>=G ], cost: 1 90: [57] -> f147 : [ K>=1+F ], cost: 1 88: [58] -> f156 : [ A>=1+F ], cost: 1 87: [59] -> f147 : K'=1+K, [ A>=1+F ], cost: 1 86: [60] -> f136 : B'=G, E'=free_142, G'=-1+G, [ K>=1+F ], cost: 1 82: [61] -> f190 : E'=free_136, [ 0>=1+E && 1>=free_138*E && free_138+free_138*E>=2 && free_136>=free_138 && 1>=E*free_137 && E*free_137+free_137>=2 && free_137>=free_136 && K>=1+F ], cost: 1 83: [61] -> f190 : E'=free_139, [ E>=1 && 1>=free_141*E && free_141+free_141*E>=2 && free_139>=free_141 && 1>=E*free_140 && free_140+E*free_140>=2 && free_140>=free_139 && K>=1+F ], cost: 1 84: [61] -> f215 : E'=0, [ K>=1+F && E==0 ], cost: 1 80: [62] -> f200 : X'=free_132, [ E*Q>=free_135*E*free_134 && free_135+free_135*E*free_134>=1+E*Q && free_135>=free_132 && E*Q>=E*free_133*free_134 && free_133+E*free_133*free_134>=1+E*Q && free_132>=free_133 && A>=1+H ], cost: 1 79: [63] -> f190 : K'=1+K, [ A>=1+H ], cost: 1 78: [64] -> f177 : G'=-1+G, [ K>=1+H ], cost: 1 77: [65] -> f177 : G'=-1+G, [ K>=1+H ], cost: 1 73: [66] -> f246 : G'=1+G, [ K>=1+H ], cost: 1 72: [67] -> f223 : A'=-1+A, [ K>=1+F ], cost: 1 66: [68] -> f332 : X'=E*W+A1*Q, B1'=0, C1'=-E*Q+A1*W, [ G1>=1+F ], cost: 1 67: [68] -> f332 : Q'=free_102, W'=free_101, X'=free_104+free_103, B1'=free_100, C1'=free_105-free_106, [ X*E>=free_113*free_104*X*E && free_104+free_113*free_104*X*E>=1+X*E && A1*Y>=free_113*A1*Y*free_103 && free_113*A1*Y*free_103+free_103>=1+A1*Y && A1*X>=free_113*A1*X*free_105 && free_113*A1*X*free_105+free_105>=1+A1*X && E*Y>=free_113*E*Y*free_106 && free_113*E*Y*free_106+free_106>=1+E*Y && 0>=1+free_113 && G1>=1+F && Y>=free_110*free_113*Y && free_110+free_110*free_113*Y>=1+Y && free_110>=free_102 && Y>=free_113*Y*free_112 && free_113*Y*free_112+free_112>=1+Y && free_102>=free_112 && 1>=free_113*free_109 && free_113*free_109+free_109>=2 && free_100>=free_109 && 1>=free_113*free_111 && free_111+free_113*free_111>=2 && free_111>=free_100 && X>=free_113*X*free_108 && free_108+free_113*X*free_108>=1+X && free_108>=free_101 && X>=free_113*free_107*X && free_107+free_113*free_107*X>=1+X && free_101>=free_107 ], cost: 1 68: [68] -> f332 : Q'=free_116, W'=free_115, X'=free_117+free_118, B1'=free_114, C1'=-free_120+free_119, [ X*E>=X*E*free_118*free_127 && X*E*free_118*free_127+free_118>=1+X*E && A1*Y>=A1*free_117*Y*free_127 && free_117+A1*free_117*Y*free_127>=1+A1*Y && A1*X>=A1*X*free_127*free_119 && A1*X*free_127*free_119+free_119>=1+A1*X && E*Y>=E*free_120*Y*free_127 && free_120+E*free_120*Y*free_127>=1+E*Y && free_127>=1 && G1>=1+F && Y>=free_124*Y*free_127 && free_124+free_124*Y*free_127>=1+Y && free_124>=free_116 && Y>=free_126*Y*free_127 && free_126+free_126*Y*free_127>=1+Y && free_116>=free_126 && 1>=free_123*free_127 && free_123+free_123*free_127>=2 && free_114>=free_123 && 1>=free_127*free_125 && free_125+free_127*free_125>=2 && free_125>=free_114 && X>=X*free_127*free_122 && X*free_127*free_122+free_122>=1+X && free_122>=free_115 && X>=X*free_121*free_127 && free_121+X*free_121*free_127>=1+X && free_115>=free_121 ], cost: 1 65: [69] -> f299 : K'=1+K, [ G1>=1+H ], cost: 1 Applied simple chaining: Start location: f2 0: f271 -> f281 : [ A>=1+B ], cost: 1 1: f271 -> f281 : [ B>=1+A ], cost: 1 71: f271 -> f223 : A'=-1+B, [ B1>=0 && B==A ], cost: 1 55: f271 -> f223 : A'=-1+B, K'=1+F, [ 0>=1+B1 && B==A && F>=K && 1+F>=1+F ], cost: 3-K+F 57: f281 -> f290 : E'=free_52, T'=-1+A, X'=free_54, Y'=free_53, A1'=free_51, C1'=free_50, [ 29>=R ], cost: 1 58: f281 -> f290 : E'=free_57, T'=-1+A, X'=free_59, Y'=free_58, A1'=free_56, C1'=free_55, [ R>=31 ], cost: 1 59: f281 -> f290 : E'=free_62, R'=30, T'=-1+A, X'=free_64, Y'=free_63, A1'=free_61, C1'=free_60, [ R==30 ], cost: 1 2: f2 -> f7 : C'=0, D'=0, E'=0, [], cost: 1 10: f7 -> f69 : B'=1+G, D'=0, E'=0, Q'=0, [ G>=1+H && F>=G ], cost: 1 111: f7 -> f136 : [ G>=1+F ], cost: 1 3: f7 -> [45] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A ], cost: 2+H-A 113: f24 -> [46] : A'=1+H, Q'=Q+free_2*(1+H-A)*free_1, [ H>=A ], cost: 1+H-A 6: f42 -> f52 : A'=1+H, Q'=(1+H-A)*free_3*free_4+Q, X'=free_153, [ F>=K && H>=A && (1+H-A)*free_3*free_4+Q>=free_155*Y && free_155*Y+free_155>=1+(1+H-A)*free_3*free_4+Q && free_155>=free_153 && (1+H-A)*free_3*free_4+Q>=free_154*Y && free_154*Y+free_154>=1+(1+H-A)*free_3*free_4+Q && free_153>=free_154 && 1+H>=1+H ], cost: 3+H-A 105: f42 -> f69 : A'=1+H, D'=0, E'=0, Q'=0, [ K>=1+F && H>=A && 1+H>=1+H ], cost: 3+H-A 115: f52 -> f42 : A'=1+H, K'=1+K, [ H>=A && 1+H>=1+H ], cost: 2+H-A 11: f69 -> f72 : [ F>=1+G && H>=G ], cost: 1 12: f69 -> f72 : [ G>=1+F && H>=G ], cost: 1 20: f69 -> f130 : M'=C, N'=free_10, O'=free_11, P'=free_10+free_11, [ G>=1+H ], cost: 1 21: f69 -> f130 : F'=G, M'=C, N'=free_12, O'=free_13, P'=free_12+free_13, [ H>=F && G==F ], cost: 1 117: f72 -> [50] : A'=1+F, D'=free_5*(1+F-A)+D, L'=free_5, [ F>=A ], cost: 1+F-A 118: f80 -> [51] : A'=1+F, Q'=(1+F-A)*free_6*free_7+Q, [ F>=A ], cost: 1+F-A 119: f98 -> f104 : A'=1+F, [ F>=A && 1+F>=1+F ], cost: 2+F-A 16: f104 -> f113 : A'=1+F, Q'=free_8*(1+F-A)*free_9+Q, [ H>=K && F>=A && 1+F>=1+F ], cost: 3+F-A 95: f104 -> f130 : A'=1+F, M'=C, N'=free_143, O'=free_144, P'=free_144+free_143, [ K>=1+H && F>=A && 1+F>=1+F ], cost: 3+F-A 121: f113 -> f104 : A'=1+F, K'=1+K, [ F>=A && 1+F>=1+F ], cost: 2+F-A 22: f130 -> f7 : C'=M, G'=1+G, [ M>=1+P ], cost: 1 23: f130 -> f7 : C'=P, G'=1+G, [ P>=M ], cost: 1 123: f136 -> [56] : B'=G, E'=free_16, G'=-1+G, [ G>=1 && G>=F ], cost: 1 124: f136 -> [56] : [], cost: 0 125: f141 -> f147 : K'=1+F, [ F>=K && 1+F>=1+F ], cost: 2-K+F 27: f147 -> f156 : A'=1+F, Q'=(1+F-A)*free_15*free_14+Q, [ F>=K && F>=A && 1+F>=1+F ], cost: 3+F-A 89: f147 -> f164 : [ K>=1+F ], cost: 1 127: f156 -> f147 : A'=1+F, K'=1+K, [ F>=A && 1+F>=1+F ], cost: 2+F-A 128: f164 -> f136 : B'=G, E'=free_142, G'=-1+G, K'=1+F, Q_1'=0, [ F>=K && 1+F>=1+F ], cost: 2-K+F 85: f177 -> f223 : [ 0>=G ], cost: 1 33: f177 -> [61] : B'=1+G, E'=free_17, K'=1+F, [ G>=1 && F>=K ], cost: 2-K+F 81: f190 -> f177 : G'=-1+G, K'=1+H, [ K>=1+F && H>=K && 1+H>=1+H ], cost: 3-K+H 35: f190 -> f200 : A'=1+H, Q'=Q+(1+H-A)*free_18*free_19, X'=free_132, [ F>=K && H>=A && E*(Q+(1+H-A)*free_18*free_19)>=free_135*E*free_134 && free_135+free_135*E*free_134>=1+E*(Q+(1+H-A)*free_18*free_19) && free_135>=free_132 && E*(Q+(1+H-A)*free_18*free_19)>=E*free_133*free_134 && free_133+E*free_133*free_134>=1+E*(Q+(1+H-A)*free_18*free_19) && free_132>=free_133 && 1+H>=1+H ], cost: 3+H-A 131: f200 -> f190 : A'=1+H, K'=1+K, [ H>=A && 1+H>=1+H ], cost: 2+H-A 40: f223 -> f226 : [ A>=1 ], cost: 1 70: f226 -> f223 : A'=-1+A, [ R>=31 ], cost: 1 41: f226 -> f230 : S'=1, [ 30>=R ], cost: 1 42: f230 -> f241 : [ 0>=B ], cost: 1 43: f230 -> f241 : S'=0, T'=-1+B, U'=C-free_20, [ B>=1 ], cost: 1 44: f230 -> f238 : T'=-1+B, U'=free_21, V'=free_22, [ 0>=1+free_21 && B>=1 ], cost: 1 45: f230 -> f238 : T'=-1+B, U'=free_23, V'=free_24, [ free_23>=1 && B>=1 ], cost: 1 54: f241 -> f271 : S'=0, B1'=free_49, [ S==0 ], cost: 1 49: f241 -> f246 : Q'=1, W'=0, [ 0>=1+S ], cost: 1 50: f241 -> f246 : Q'=1, W'=0, [ S>=1 ], cost: 1 47: f238 -> f230 : B'=-1+B, [ 0>=1+V ], cost: 1 48: f238 -> f230 : B'=-1+B, [ V>=1 ], cost: 1 46: f238 -> f241 : [], cost: 1 74: f246 -> f271 : B1'=free_128, [ G>=1+A ], cost: 1 75: f246 -> f271 : X'=Q*free_131, Z'=-free_129+C, B1'=free_130, [ A>=G ], cost: 1 51: f246 -> f260 : E'=free_27, Q'=-free_28*Q*free_29, W'=free_25, X'=Q*free_29, Y'=free_26, Z'=free_30, [ 1>=free_28*free_35 && free_28+free_28*free_35>=2 && A>=G && 0>=1+free_30 && 1>=free_34*free_35 && free_34+free_34*free_35>=2 && free_26>=free_34 && 1>=free_35*free_32 && free_35*free_32+free_32>=2 && free_32>=free_26 && free_27>=free_27*free_35*free_33 && free_27*free_35*free_33+free_33>=1+free_27 && free_33>=free_25 && free_27>=free_27*free_31*free_35 && free_31+free_27*free_31*free_35>=1+free_27 && free_25>=free_31 ], cost: 1 52: f246 -> f260 : E'=free_38, Q'=-Q*free_39*free_40, W'=free_36, X'=Q*free_40, Y'=free_37, Z'=free_41, [ 1>=free_39*free_46 && free_39+free_39*free_46>=2 && A>=G && free_41>=1 && 1>=free_45*free_46 && free_45*free_46+free_45>=2 && free_37>=free_45 && 1>=free_46*free_43 && free_43+free_46*free_43>=2 && free_43>=free_37 && free_38>=free_44*free_38*free_46 && free_44+free_44*free_38*free_46>=1+free_38 && free_44>=free_36 && free_38>=free_38*free_42*free_46 && free_38*free_42*free_46+free_42>=1+free_38 && free_36>=free_42 ], cost: 1 134: f260 -> f246 : G'=1+G, K'=1+H, A1'=free_47, B1'=free_48, [ H>=K && 1+H>=1+H ], cost: 2-K+H 60: f290 -> f299 : Q'=1, W'=1, X'=free_65, D1'=free_66, E1'=free_66, [ X>=0 && A1*Y>=free_69*free_66*Y+X*free_69*Y && free_69+free_69*free_66*Y+X*free_69*Y>=1+A1*Y && free_69+C1^2>=B1^2+Y^2+free_68*C1 && free_68+B1^2+Y^2+free_68*C1>=1+free_69+C1^2 && free_68>=free_65 && A1*Y>=free_66*Y*free_67+X*Y*free_67 && free_66*Y*free_67+X*Y*free_67+free_67>=1+A1*Y && C1^2+free_67>=B1^2+Y^2+free_70*C1 && B1^2+Y^2+free_70+free_70*C1>=1+C1^2+free_67 && free_65>=free_70 ], cost: 1 61: f290 -> f299 : Q'=1, W'=1, X'=free_71, E1'=-free_72, F1'=free_72, [ 0>=1+X && free_75*free_72*Y+A1*Y>=X*free_75*Y && free_75+X*free_75*Y>=1+free_75*free_72*Y+A1*Y && free_75+C1^2>=B1^2+Y^2+C1*free_74 && B1^2+Y^2+C1*free_74+free_74>=1+free_75+C1^2 && free_74>=free_71 && free_72*Y*free_73+A1*Y>=X*Y*free_73 && X*Y*free_73+free_73>=1+free_72*Y*free_73+A1*Y && free_73+C1^2>=B1^2+Y^2+free_76*C1 && B1^2+Y^2+free_76+free_76*C1>=1+free_73+C1^2 && free_71>=free_76 ], cost: 1 69: f299 -> f226 : R'=1+R, [ K>=1+T ], cost: 1 62: f299 -> [68] : E'=free_82*free_79*W-free_80, G'=1+K, Q'=free_78, W'=free_85, X'=free_79*free_83*W+free_77, Y'=free_86, A1'=free_81, B1'=free_96, C1'=free_97, G1'=1+F, [ X>=free_84*free_82 && free_82+free_84*free_82>=1+X && Q*free_79*C1>=free_84*C1*free_80 && free_84*C1*free_80+free_80>=1+Q*free_79*C1 && X*C1>=free_84*C1*free_77 && free_84*C1*free_77+free_77>=1+X*C1 && Q*free_79>=free_84*free_83 && free_84*free_83+free_83>=1+Q*free_79 && Q*free_79>=free_84*free_91 && free_91+free_84*free_91>=1+Q*free_79 && free_91>=free_78 && Q*free_79>=free_84*free_94 && free_94+free_84*free_94>=1+Q*free_79 && free_78>=free_94 && free_87*Q*free_79>=free_87*free_84*free_90 && free_87*free_84*free_90+free_90>=1+free_87*Q*free_79 && free_90>=free_86 && free_87*Q*free_79>=free_87*free_84*free_93 && free_87*free_84*free_93+free_93>=1+free_87*Q*free_79 && free_86>=free_93 && T>=K && free_87*X>=free_87*free_84*free_95 && free_87*free_84*free_95+free_95>=1+free_87*X && free_95>=free_81 && free_87*X>=free_87*free_84*free_89 && free_89+free_87*free_84*free_89>=1+free_87*X && free_81>=free_89 && X>=free_84*free_92 && free_84*free_92+free_92>=1+X && free_92>=free_85 && X>=free_84*free_88 && free_88+free_84*free_88>=1+X && free_85>=free_88 && F>=G1 ], cost: 2+F-G1 137: f332 -> f299 : K'=1+K, A1'=free_98, B1'=free_99, G1'=1+H, [ H>=G1 && 1+H>=1+H ], cost: 2+H-G1 108: [45] -> f24 : [ 0>=1+D && A>=1+H ], cost: 1 109: [45] -> f24 : [ D>=1 && A>=1+H ], cost: 1 110: [45] -> f69 : D'=0, E'=0, Q'=0, [ A>=1+H && D==0 ], cost: 1 106: [46] -> f42 : E'=-free_156, X'=free_158, Y'=-free_158*free_156-Q, M1'=free_157, N1'=free_156, O1'=free_156, [ free_158>=0 && A>=1+H ], cost: 1 107: [46] -> f42 : E'=free_159, X'=free_161, Y'=-Q+free_161*free_159, O1'=-free_159, P1'=free_160, Q1_1'=free_159, [ 0>=1+free_161 && A>=1+H ], cost: 1 99: [50] -> f80 : [ 0>=1+D && A>=1+F ], cost: 1 100: [50] -> f80 : [ D>=1 && A>=1+F ], cost: 1 101: [50] -> f130 : D'=0, M'=C, N'=free_151, O'=free_152, P'=free_151+free_152, [ A>=1+F && D==0 ], cost: 1 97: [51] -> f98 : E'=-free_145, X'=free_147, Y'=-Q-free_145*free_147, H1'=free_146, Q1'=free_145, J1'=free_145, [ free_147>=0 && A>=1+F ], cost: 1 98: [51] -> f98 : E'=free_148, X'=free_150, Y'=-Q+free_148*free_150, J1'=-free_148, K1'=free_149, L1'=free_148, [ 0>=1+free_150 && A>=1+F ], cost: 1 24: [56] -> f141 : [ F>=1+G && 0>=1+E && G>=1 ], cost: 1 25: [56] -> f141 : [ F>=1+G && E>=1 && G>=1 ], cost: 1 30: [56] -> f164 : E'=0, [ G>=1 && F>=1+G && E==0 ], cost: 1 91: [56] -> f177 : [ 0>=G ], cost: 1 84: [61] -> f177 : E'=0, G'=-1+G, K'=1+H, [ K>=1+F && E==0 && H>=K && 1+H>=1+H ], cost: 3-K+H 82: [61] -> f190 : E'=free_136, [ 0>=1+E && 1>=free_138*E && free_138+free_138*E>=2 && free_136>=free_138 && 1>=E*free_137 && E*free_137+free_137>=2 && free_137>=free_136 && K>=1+F ], cost: 1 83: [61] -> f190 : E'=free_139, [ E>=1 && 1>=free_141*E && free_141+free_141*E>=2 && free_139>=free_141 && 1>=E*free_140 && free_140+E*free_140>=2 && free_140>=free_139 && K>=1+F ], cost: 1 66: [68] -> f332 : X'=E*W+A1*Q, B1'=0, C1'=-E*Q+A1*W, [ G1>=1+F ], cost: 1 67: [68] -> f332 : Q'=free_102, W'=free_101, X'=free_104+free_103, B1'=free_100, C1'=free_105-free_106, [ X*E>=free_113*free_104*X*E && free_104+free_113*free_104*X*E>=1+X*E && A1*Y>=free_113*A1*Y*free_103 && free_113*A1*Y*free_103+free_103>=1+A1*Y && A1*X>=free_113*A1*X*free_105 && free_113*A1*X*free_105+free_105>=1+A1*X && E*Y>=free_113*E*Y*free_106 && free_113*E*Y*free_106+free_106>=1+E*Y && 0>=1+free_113 && G1>=1+F && Y>=free_110*free_113*Y && free_110+free_110*free_113*Y>=1+Y && free_110>=free_102 && Y>=free_113*Y*free_112 && free_113*Y*free_112+free_112>=1+Y && free_102>=free_112 && 1>=free_113*free_109 && free_113*free_109+free_109>=2 && free_100>=free_109 && 1>=free_113*free_111 && free_111+free_113*free_111>=2 && free_111>=free_100 && X>=free_113*X*free_108 && free_108+free_113*X*free_108>=1+X && free_108>=free_101 && X>=free_113*free_107*X && free_107+free_113*free_107*X>=1+X && free_101>=free_107 ], cost: 1 68: [68] -> f332 : Q'=free_116, W'=free_115, X'=free_117+free_118, B1'=free_114, C1'=-free_120+free_119, [ X*E>=X*E*free_118*free_127 && X*E*free_118*free_127+free_118>=1+X*E && A1*Y>=A1*free_117*Y*free_127 && free_117+A1*free_117*Y*free_127>=1+A1*Y && A1*X>=A1*X*free_127*free_119 && A1*X*free_127*free_119+free_119>=1+A1*X && E*Y>=E*free_120*Y*free_127 && free_120+E*free_120*Y*free_127>=1+E*Y && free_127>=1 && G1>=1+F && Y>=free_124*Y*free_127 && free_124+free_124*Y*free_127>=1+Y && free_124>=free_116 && Y>=free_126*Y*free_127 && free_126+free_126*Y*free_127>=1+Y && free_116>=free_126 && 1>=free_123*free_127 && free_123+free_123*free_127>=2 && free_114>=free_123 && 1>=free_127*free_125 && free_125+free_127*free_125>=2 && free_125>=free_114 && X>=X*free_127*free_122 && X*free_127*free_122+free_122>=1+X && free_122>=free_115 && X>=X*free_121*free_127 && free_121+X*free_121*free_127>=1+X && free_115>=free_121 ], cost: 1