path: root/test/regress/regress2/arith/miplib-pp08a-3000.smt2

; COMMAND-LINE: --miplib-trick
; EXPECT: unsat
(set-logic QF_LRA)
(set-info :source |
Relaxation of the Mixed-Integer Programming
optimization problem pp08a from the MIPLIB (http://miplib.zib.de/)
by Enric Rodriguez-Carbonell (erodri@lsi.upc.edu)
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun tmp75 () Real)
(declare-fun tmp74 () Real)
(declare-fun tmp73 () Real)
(declare-fun tmp72 () Real)
(declare-fun tmp71 () Real)
(declare-fun tmp70 () Real)
(declare-fun tmp69 () Real)
(declare-fun tmp68 () Real)
(declare-fun tmp67 () Real)
(declare-fun tmp66 () Real)
(declare-fun tmp65 () Real)
(declare-fun tmp64 () Real)
(declare-fun tmp63 () Real)
(declare-fun tmp62 () Real)
(declare-fun tmp61 () Real)
(declare-fun tmp60 () Real)
(declare-fun tmp59 () Real)
(declare-fun tmp58 () Real)
(declare-fun tmp57 () Real)
(declare-fun tmp56 () Real)
(declare-fun tmp55 () Real)
(declare-fun tmp54 () Real)
(declare-fun tmp53 () Real)
(declare-fun tmp52 () Real)
(declare-fun tmp51 () Real)
(declare-fun tmp50 () Real)
(declare-fun tmp49 () Real)
(declare-fun tmp48 () Real)
(declare-fun tmp47 () Real)
(declare-fun tmp46 () Real)
(declare-fun tmp45 () Real)
(declare-fun tmp44 () Real)
(declare-fun tmp43 () Real)
(declare-fun tmp42 () Real)
(declare-fun tmp41 () Real)
(declare-fun tmp40 () Real)
(declare-fun tmp39 () Real)
(declare-fun tmp38 () Real)
(declare-fun tmp37 () Real)
(declare-fun tmp36 () Real)
(declare-fun tmp35 () Real)
(declare-fun tmp34 () Real)
(declare-fun tmp33 () Real)
(declare-fun tmp32 () Real)
(declare-fun tmp31 () Real)
(declare-fun tmp30 () Real)
(declare-fun tmp29 () Real)
(declare-fun tmp28 () Real)
(declare-fun tmp27 () Real)
(declare-fun tmp26 () Real)
(declare-fun tmp25 () Real)
(declare-fun tmp24 () Real)
(declare-fun tmp23 () Real)
(declare-fun tmp22 () Real)
(declare-fun tmp21 () Real)
(declare-fun tmp20 () Real)
(declare-fun tmp19 () Real)
(declare-fun tmp18 () Real)
(declare-fun tmp17 () Real)
(declare-fun tmp16 () Real)
(declare-fun tmp15 () Real)
(declare-fun tmp14 () Real)
(declare-fun tmp13 () Real)
(declare-fun tmp12 () Real)
(declare-fun tmp11 () Real)
(declare-fun tmp10 () Real)
(declare-fun tmp9 () Real)
(declare-fun tmp8 () Real)
(declare-fun tmp7 () Real)
(declare-fun tmp6 () Real)
(declare-fun tmp5 () Real)
(declare-fun tmp4 () Real)
(declare-fun tmp3 () Real)
(declare-fun tmp2 () Real)
(declare-fun tmp1 () Real)
(declare-fun x113 () Real)
(declare-fun x114 () Real)
(declare-fun x115 () Real)
(declare-fun x116 () Real)
(declare-fun x117 () Real)
(declare-fun x118 () Real)
(declare-fun x119 () Real)
(declare-fun x120 () Real)
(declare-fun x121 () Real)
(declare-fun x122 () Real)
(declare-fun x123 () Real)
(declare-fun x124 () Real)
(declare-fun x125 () Real)
(declare-fun x126 () Real)
(declare-fun x127 () Real)
(declare-fun x128 () Real)
(declare-fun x129 () Real)
(declare-fun x130 () Real)
(declare-fun x131 () Real)
(declare-fun x132 () Real)
(declare-fun x133 () Real)
(declare-fun x134 () Real)
(declare-fun x135 () Real)
(declare-fun x136 () Real)
(declare-fun x137 () Real)
(declare-fun x138 () Real)
(declare-fun x139 () Real)
(declare-fun x140 () Real)
(declare-fun x141 () Real)
(declare-fun x142 () Real)
(declare-fun x143 () Real)
(declare-fun x144 () Real)
(declare-fun x145 () Real)
(declare-fun x146 () Real)
(declare-fun x147 () Real)
(declare-fun x148 () Real)
(declare-fun x149 () Real)
(declare-fun x150 () Real)
(declare-fun x151 () Real)
(declare-fun x152 () Real)
(declare-fun x153 () Real)
(declare-fun x154 () Real)
(declare-fun x155 () Real)
(declare-fun x156 () Real)
(declare-fun x157 () Real)
(declare-fun x158 () Real)
(declare-fun x159 () Real)
(declare-fun x160 () Real)
(declare-fun x161 () Real)
(declare-fun x162 () Real)
(declare-fun x163 () Real)
(declare-fun x164 () Real)
(declare-fun x165 () Real)
(declare-fun x166 () Real)
(declare-fun x167 () Real)
(declare-fun x168 () Real)
(declare-fun x169 () Real)
(declare-fun x170 () Real)
(declare-fun x171 () Real)
(declare-fun x172 () Real)
(declare-fun x173 () Real)
(declare-fun x174 () Real)
(declare-fun x175 () Real)
(declare-fun x176 () Real)
(declare-fun x112 () Real)
(declare-fun x111 () Real)
(declare-fun x110 () Real)
(declare-fun x109 () Real)
(declare-fun x108 () Real)
(declare-fun x107 () Real)
(declare-fun x106 () Real)
(declare-fun x105 () Real)
(declare-fun x104 () Real)
(declare-fun x103 () Real)
(declare-fun x102 () Real)
(declare-fun x101 () Real)
(declare-fun x100 () Real)
(declare-fun x99 () Real)
(declare-fun x98 () Real)
(declare-fun x97 () Real)
(declare-fun x96 () Real)
(declare-fun x95 () Real)
(declare-fun x94 () Real)
(declare-fun x93 () Real)
(declare-fun x92 () Real)
(declare-fun x91 () Real)
(declare-fun x90 () Real)
(declare-fun x89 () Real)
(declare-fun x88 () Real)
(declare-fun x87 () Real)
(declare-fun x86 () Real)
(declare-fun x85 () Real)
(declare-fun x84 () Real)
(declare-fun x83 () Real)
(declare-fun x82 () Real)
(declare-fun x81 () Real)
(declare-fun x80 () Real)
(declare-fun x79 () Real)
(declare-fun x78 () Real)
(declare-fun x77 () Real)
(declare-fun x76 () Real)
(declare-fun x75 () Real)
(declare-fun x74 () Real)
(declare-fun x73 () Real)
(declare-fun x72 () Real)
(declare-fun x71 () Real)
(declare-fun x70 () Real)
(declare-fun x69 () Real)
(declare-fun x68 () Real)
(declare-fun x67 () Real)
(declare-fun x66 () Real)
(declare-fun x65 () Real)
(declare-fun x64 () Real)
(declare-fun x63 () Real)
(declare-fun x62 () Real)
(declare-fun x61 () Real)
(declare-fun x60 () Real)
(declare-fun x59 () Real)
(declare-fun x58 () Real)
(declare-fun x57 () Real)
(declare-fun x56 () Real)
(declare-fun x55 () Real)
(declare-fun x54 () Real)
(declare-fun x53 () Real)
(declare-fun x52 () Real)
(declare-fun x51 () Real)
(declare-fun x50 () Real)
(declare-fun x49 () Real)
(declare-fun x48 () Real)
(declare-fun x47 () Real)
(declare-fun x46 () Real)
(declare-fun x45 () Real)
(declare-fun x44 () Real)
(declare-fun x43 () Real)
(declare-fun x42 () Real)
(declare-fun x41 () Real)
(declare-fun x40 () Real)
(declare-fun x39 () Real)
(declare-fun x38 () Real)
(declare-fun x37 () Real)
(declare-fun x36 () Real)
(declare-fun x35 () Real)
(declare-fun x34 () Real)
(declare-fun x33 () Real)
(declare-fun x32 () Real)
(declare-fun x31 () Real)
(declare-fun x30 () Real)
(declare-fun x29 () Real)
(declare-fun x28 () Real)
(declare-fun x27 () Real)
(declare-fun x26 () Real)
(declare-fun x25 () Real)
(declare-fun x24 () Real)
(declare-fun x23 () Real)
(declare-fun x22 () Real)
(declare-fun x21 () Real)
(declare-fun x20 () Real)
(declare-fun x19 () Real)
(declare-fun x18 () Real)
(declare-fun x17 () Real)
(declare-fun x16 () Real)
(declare-fun x15 () Real)
(declare-fun x14 () Real)
(declare-fun x13 () Real)
(declare-fun x12 () Real)
(declare-fun x11 () Real)
(declare-fun x10 () Real)
(declare-fun x9 () Real)
(declare-fun x8 () Real)
(declare-fun x7 () Real)
(declare-fun x6 () Real)
(declare-fun x5 () Real)
(declare-fun x4 () Real)
(declare-fun x3 () Real)
(declare-fun x2 () Real)
(declare-fun x1 () Real)
(declare-fun x177 () Bool)
(declare-fun x178 () Bool)
(declare-fun x179 () Bool)
(declare-fun x180 () Bool)
(declare-fun x181 () Bool)
(declare-fun x182 () Bool)
(declare-fun x183 () Bool)
(declare-fun x184 () Bool)
(declare-fun x185 () Bool)
(declare-fun x186 () Bool)
(declare-fun x187 () Bool)
(declare-fun x188 () Bool)
(declare-fun x189 () Bool)
(declare-fun x190 () Bool)
(declare-fun x191 () Bool)
(declare-fun x192 () Bool)
(declare-fun x193 () Bool)
(declare-fun x194 () Bool)
(declare-fun x195 () Bool)
(declare-fun x196 () Bool)
(declare-fun x197 () Bool)
(declare-fun x198 () Bool)
(declare-fun x199 () Bool)
(declare-fun x200 () Bool)
(declare-fun x201 () Bool)
(declare-fun x202 () Bool)
(declare-fun x203 () Bool)
(declare-fun x204 () Bool)
(declare-fun x205 () Bool)
(declare-fun x206 () Bool)
(declare-fun x207 () Bool)
(declare-fun x208 () Bool)
(declare-fun x209 () Bool)
(declare-fun x210 () Bool)
(declare-fun x211 () Bool)
(declare-fun x212 () Bool)
(declare-fun x213 () Bool)
(declare-fun x214 () Bool)
(declare-fun x215 () Bool)
(declare-fun x216 () Bool)
(declare-fun x217 () Bool)
(declare-fun x218 () Bool)
(declare-fun x219 () Bool)
(declare-fun x220 () Bool)
(declare-fun x221 () Bool)
(declare-fun x222 () Bool)
(declare-fun x223 () Bool)
(declare-fun x224 () Bool)
(declare-fun x225 () Bool)
(declare-fun x226 () Bool)
(declare-fun x227 () Bool)
(declare-fun x228 () Bool)
(declare-fun x229 () Bool)
(declare-fun x230 () Bool)
(declare-fun x231 () Bool)
(declare-fun x232 () Bool)
(declare-fun x233 () Bool)
(declare-fun x234 () Bool)
(declare-fun x235 () Bool)
(declare-fun x236 () Bool)
(declare-fun x237 () Bool)
(declare-fun x238 () Bool)
(declare-fun x239 () Bool)
(declare-fun x240 () Bool)
(assert (let ((?v_64 (* 1 x56)) (?v_65 (* 1 x55)) (?v_66 (* 1 x54)) (?v_67 (* 1 x53)) (?v_68 (* 1 x52)) (?v_69 (* 1 x51)) (?v_70 (* 1 x50)) (?v_71 (* 1 x49)) (?v_72 (* 1 x48)) (?v_73 (* 1 x47)) (?v_74 (* 1 x46)) (?v_75 (* 1 x45)) (?v_76 (* 1 x44)) (?v_77 (* 1 x43)) (?v_78 (* 1 x42)) (?v_79 (* 1 x41)) (?v_80 (* 1 x40)) (?v_81 (* 1 x39)) (?v_82 (* 1 x38)) (?v_83 (* 1 x37)) (?v_84 (* 1 x36)) (?v_85 (* 1 x35)) (?v_86 (* 1 x34)) (?v_87 (* 1 x33)) (?v_88 (* 1 x32)) (?v_89 (* 1 x31)) (?v_90 (* 1 x30)) (?v_91 (* 1 x29)) (?v_92 (* 1 x28)) (?v_93 (* 1 x27)) (?v_94 (* 1 x26)) (?v_95 (* 1 x25)) (?v_96 (* 1 x24)) (?v_97 (* 1 x23)) (?v_98 (* 1 x22)) (?v_99 (* 1 x21)) (?v_100 (* 1 x20)) (?v_101 (* 1 x19)) (?v_102 (* 1 x18)) (?v_103 (* 1 x17)) (?v_104 (* 1 x16)) (?v_105 (* 1 x15)) (?v_106 (* 1 x14)) (?v_107 (* 1 x13)) (?v_108 (* 1 x12)) (?v_109 (* 1 x11)) (?v_110 (* 1 x10)) (?v_111 (* 1 x9)) (?v_112 (* 1 x8)) (?v_113 (* 1 x7)) (?v_114 (* 1 x6)) (?v_115 (* 1 x5)) (?v_116 (* 1 x4)) (?v_117 (* 1 x3)) (?v_118 (* 1 x2)) (?v_119 (* 1 x1)) (?v_7 (* 1 x176)) (?v_15 (* 1 x175)) (?v_23 (* 1 x174)) (?v_31 (* 1 x173)) (?v_39 (* 1 x172)) (?v_47 (* 1 x171)) (?v_55 (* 1 x170)) (?v_63 (* 1 x169)) (?v_6 (* 1 x168)) (?v_14 (* 1 x167)) (?v_22 (* 1 x166)) (?v_30 (* 1 x165)) (?v_38 (* 1 x164)) (?v_46 (* 1 x163)) (?v_54 (* 1 x162)) (?v_62 (* 1 x161)) (?v_5 (* 1 x160)) (?v_13 (* 1 x159)) (?v_21 (* 1 x158)) (?v_29 (* 1 x157)) (?v_37 (* 1 x156)) (?v_45 (* 1 x155)) (?v_53 (* 1 x154)) (?v_61 (* 1 x153)) (?v_4 (* 1 x152)) (?v_12 (* 1 x151)) (?v_20 (* 1 x150)) (?v_28 (* 1 x149)) (?v_36 (* 1 x148)) (?v_44 (* 1 x147)) (?v_52 (* 1 x146)) (?v_60 (* 1 x145)) (?v_3 (* 1 x144)) (?v_11 (* 1 x143)) (?v_19 (* 1 x142)) (?v_27 (* 1 x141)) (?v_35 (* 1 x140)) (?v_43 (* 1 x139)) (?v_51 (* 1 x138)) (?v_59 (* 1 x137)) (?v_2 (* 1 x136)) (?v_10 (* 1 x135)) (?v_18 (* 1 x134)) (?v_26 (* 1 x133)) (?v_34 (* 1 x132)) (?v_42 (* 1 x131)) (?v_50 (* 1 x130)) (?v_58 (* 1 x129)) (?v_1 (* 1 x128)) (?v_9 (* 1 x127)) (?v_17 (* 1 x126)) (?v_25 (* 1 x125)) (?v_33 (* 1 x124)) (?v_41 (* 1 x123)) (?v_49 (* 1 x122)) (?v_57 (* 1 x121)) (?v_0 (* 1 x120)) (?v_8 (* 1 x119)) (?v_16 (* 1 x118)) (?v_24 (* 1 x117)) (?v_32 (* 1 x116)) (?v_40 (* 1 x115)) (?v_48 (* 1 x114)) (?v_56 (* 1 x113)) (?v_120 (not x207)) (?v_121 (not x208)) (?v_122 (not x209)) (?v_123 (and (not x210) true))) (let ((?v_126 (and ?v_122 ?v_123))) (let ((?v_131 (and ?v_121 ?v_126)) (?v_125 (and x210 true))) (let ((?v_127 (and ?v_122 ?v_125))) (let ((?v_133 (and ?v_121 ?v_127)) (?v_124 (= tmp75 400)) (?v_128 (and x209 ?v_123))) (let ((?v_134 (and ?v_121 ?v_128)) (?v_130 (and x209 ?v_125))) (let ((?v_135 (and ?v_121 ?v_130)) (?v_137 (and x208 ?v_126)) (?v_132 (= tmp75 300)) (?v_138 (and x208 ?v_127)) (?v_129 (= tmp75 700)) (?v_139 (and x208 ?v_128)) (?v_141 (and x208 ?v_130)) (?v_136 (= tmp75 1100)) (?v_140 (= tmp75 1000)) (?v_142 (not x216)) (?v_143 (not x215)) (?v_144 (not x214)) (?v_145 (not x213)) (?v_146 (not x212)) (?v_147 (and (not x211) true))) (let ((?v_150 (and ?v_146 ?v_147))) (let ((?v_155 (and ?v_145 ?v_150))) (let ((?v_164 (and ?v_144 ?v_155))) (let ((?v_181 (and ?v_143 ?v_164)) (?v_149 (and x211 true))) (let ((?v_151 (and ?v_146 ?v_149))) (let ((?v_156 (and ?v_145 ?v_151))) (let ((?v_165 (and ?v_144 ?v_156))) (let ((?v_182 (and ?v_143 ?v_165)) (?v_148 (= tmp74 400)) (?v_153 (and x212 ?v_147))) (let ((?v_157 (and ?v_145 ?v_153))) (let ((?v_166 (and ?v_144 ?v_157))) (let ((?v_183 (and ?v_143 ?v_166)) (?v_154 (and x212 ?v_149))) (let ((?v_158 (and ?v_145 ?v_154))) (let ((?v_167 (and ?v_144 ?v_158))) (let ((?v_184 (and ?v_143 ?v_167)) (?v_152 (= tmp74 800)) (?v_160 (and x213 ?v_150))) (let ((?v_168 (and ?v_144 ?v_160))) (let ((?v_185 (and ?v_143 ?v_168)) (?v_161 (and x213 ?v_151))) (let ((?v_169 (and ?v_144 ?v_161))) (let ((?v_186 (and ?v_143 ?v_169)) (?v_162 (and x213 ?v_153))) (let ((?v_170 (and ?v_144 ?v_162))) (let ((?v_187 (and ?v_143 ?v_170)) (?v_163 (and x213 ?v_154))) (let ((?v_171 (and ?v_144 ?v_163))) (let ((?v_188 (and ?v_143 ?v_171)) (?v_159 (= tmp74 1200)) (?v_173 (and x214 ?v_155))) (let ((?v_189 (and ?v_143 ?v_173)) (?v_174 (and x214 ?v_156))) (let ((?v_190 (and ?v_143 ?v_174)) (?v_175 (and x214 ?v_157))) (let ((?v_191 (and ?v_143 ?v_175)) (?v_176 (and x214 ?v_158))) (let ((?v_192 (and ?v_143 ?v_176)) (?v_177 (and x214 ?v_160))) (let ((?v_193 (and ?v_143 ?v_177)) (?v_178 (and x214 ?v_161))) (let ((?v_194 (and ?v_143 ?v_178)) (?v_179 (and x214 ?v_162))) (let ((?v_195 (and ?v_143 ?v_179)) (?v_180 (and x214 ?v_163))) (let ((?v_196 (and ?v_143 ?v_180)) (?v_172 (= tmp74 1600)) (?v_198 (and x215 ?v_164)) (?v_199 (and x215 ?v_165)) (?v_200 (and x215 ?v_166)) (?v_201 (and x215 ?v_167)) (?v_202 (and x215 ?v_168)) (?v_203 (and x215 ?v_169)) (?v_204 (and x215 ?v_170)) (?v_205 (and x215 ?v_171)) (?v_206 (and x215 ?v_173)) (?v_207 (and x215 ?v_174)) (?v_208 (and x215 ?v_175)) (?v_209 (and x215 ?v_176)) (?v_210 (and x215 ?v_177)) (?v_211 (and x215 ?v_178)) (?v_212 (and x215 ?v_179)) (?v_213 (and x215 ?v_180)) (?v_197 (= tmp74 2000)) (?v_214 (not x201)) (?v_215 (not x202)) (?v_216 (not x203)) (?v_217 (not x204)) (?v_218 (not x205)) (?v_219 (and (not x206) true))) (let ((?v_222 (and ?v_218 ?v_219))) (let ((?v_227 (and ?v_217 ?v_222))) (let ((?v_236 (and ?v_216 ?v_227))) (let ((?v_253 (and ?v_215 ?v_236)) (?v_221 (and x206 true))) (let ((?v_223 (and ?v_218 ?v_221))) (let ((?v_228 (and ?v_217 ?v_223))) (let ((?v_237 (and ?v_216 ?v_228))) (let ((?v_254 (and ?v_215 ?v_237)) (?v_220 (= tmp73 300)) (?v_225 (and x205 ?v_219))) (let ((?v_229 (and ?v_217 ?v_225))) (let ((?v_238 (and ?v_216 ?v_229))) (let ((?v_255 (and ?v_215 ?v_238)) (?v_226 (and x205 ?v_221))) (let ((?v_230 (and ?v_217 ?v_226))) (let ((?v_239 (and ?v_216 ?v_230))) (let ((?v_256 (and ?v_215 ?v_239)) (?v_224 (= tmp73 600)) (?v_232 (and x204 ?v_222))) (let ((?v_240 (and ?v_216 ?v_232))) (let ((?v_257 (and ?v_215 ?v_240)) (?v_233 (and x204 ?v_223))) (let ((?v_241 (and ?v_216 ?v_233))) (let ((?v_258 (and ?v_215 ?v_241)) (?v_234 (and x204 ?v_225))) (let ((?v_242 (and ?v_216 ?v_234))) (let ((?v_259 (and ?v_215 ?v_242)) (?v_235 (and x204 ?v_226))) (let ((?v_243 (and ?v_216 ?v_235))) (let ((?v_260 (and ?v_215 ?v_243)) (?v_231 (= tmp73 900)) (?v_245 (and x203 ?v_227))) (let ((?v_261 (and ?v_215 ?v_245)) (?v_246 (and x203 ?v_228))) (let ((?v_262 (and ?v_215 ?v_246)) (?v_247 (and x203 ?v_229))) (let ((?v_263 (and ?v_215 ?v_247)) (?v_248 (and x203 ?v_230))) (let ((?v_264 (and ?v_215 ?v_248)) (?v_249 (and x203 ?v_232))) (let ((?v_265 (and ?v_215 ?v_249)) (?v_250 (and x203 ?v_233))) (let ((?v_266 (and ?v_215 ?v_250)) (?v_251 (and x203 ?v_234))) (let ((?v_267 (and ?v_215 ?v_251)) (?v_252 (and x203 ?v_235))) (let ((?v_268 (and ?v_215 ?v_252)) (?v_244 (= tmp73 1200)) (?v_270 (and x202 ?v_236)) (?v_271 (and x202 ?v_237)) (?v_272 (and x202 ?v_238)) (?v_273 (and x202 ?v_239)) (?v_274 (and x202 ?v_240)) (?v_275 (and x202 ?v_241)) (?v_276 (and x202 ?v_242)) (?v_277 (and x202 ?v_243)) (?v_278 (and x202 ?v_245)) (?v_279 (and x202 ?v_246)) (?v_280 (and x202 ?v_247)) (?v_281 (and x202 ?v_248)) (?v_282 (and x202 ?v_249)) (?v_283 (and x202 ?v_250)) (?v_284 (and x202 ?v_251)) (?v_285 (and x202 ?v_252)) (?v_269 (= tmp73 1500)) (?v_286 (not x222)) (?v_287 (not x221)) (?v_288 (not x220)) (?v_289 (not x219)) (?v_290 (not x218)) (?v_291 (and (not x217) true))) (let ((?v_294 (and ?v_290 ?v_291))) (let ((?v_299 (and ?v_289 ?v_294))) (let ((?v_308 (and ?v_288 ?v_299))) (let ((?v_325 (and ?v_287 ?v_308)) (?v_293 (and x217 true))) (let ((?v_295 (and ?v_290 ?v_293))) (let ((?v_300 (and ?v_289 ?v_295))) (let ((?v_309 (and ?v_288 ?v_300))) (let ((?v_326 (and ?v_287 ?v_309)) (?v_292 (= tmp72 250)) (?v_297 (and x218 ?v_291))) (let ((?v_301 (and ?v_289 ?v_297))) (let ((?v_310 (and ?v_288 ?v_301))) (let ((?v_327 (and ?v_287 ?v_310)) (?v_298 (and x218 ?v_293))) (let ((?v_302 (and ?v_289 ?v_298))) (let ((?v_311 (and ?v_288 ?v_302))) (let ((?v_328 (and ?v_287 ?v_311)) (?v_296 (= tmp72 500)) (?v_304 (and x219 ?v_294))) (let ((?v_312 (and ?v_288 ?v_304))) (let ((?v_329 (and ?v_287 ?v_312)) (?v_305 (and x219 ?v_295))) (let ((?v_313 (and ?v_288 ?v_305))) (let ((?v_330 (and ?v_287 ?v_313)) (?v_306 (and x219 ?v_297))) (let ((?v_314 (and ?v_288 ?v_306))) (let ((?v_331 (and ?v_287 ?v_314)) (?v_307 (and x219 ?v_298))) (let ((?v_315 (and ?v_288 ?v_307))) (let ((?v_332 (and ?v_287 ?v_315)) (?v_303 (= tmp72 750)) (?v_317 (and x220 ?v_299))) (let ((?v_333 (and ?v_287 ?v_317)) (?v_318 (and x220 ?v_300))) (let ((?v_334 (and ?v_287 ?v_318)) (?v_319 (and x220 ?v_301))) (let ((?v_335 (and ?v_287 ?v_319)) (?v_320 (and x220 ?v_302))) (let ((?v_336 (and ?v_287 ?v_320)) (?v_321 (and x220 ?v_304))) (let ((?v_337 (and ?v_287 ?v_321)) (?v_322 (and x220 ?v_305))) (let ((?v_338 (and ?v_287 ?v_322)) (?v_323 (and x220 ?v_306))) (let ((?v_339 (and ?v_287 ?v_323)) (?v_324 (and x220 ?v_307))) (let ((?v_340 (and ?v_287 ?v_324)) (?v_316 (= tmp72 1000)) (?v_342 (and x221 ?v_308)) (?v_343 (and x221 ?v_309)) (?v_344 (and x221 ?v_310)) (?v_345 (and x221 ?v_311)) (?v_346 (and x221 ?v_312)) (?v_347 (and x221 ?v_313)) (?v_348 (and x221 ?v_314)) (?v_349 (and x221 ?v_315)) (?v_350 (and x221 ?v_317)) (?v_351 (and x221 ?v_318)) (?v_352 (and x221 ?v_319)) (?v_353 (and x221 ?v_320)) (?v_354 (and x221 ?v_321)) (?v_355 (and x221 ?v_322)) (?v_356 (and x221 ?v_323)) (?v_357 (and x221 ?v_324)) (?v_341 (= tmp72 1250)) (?v_358 (not x195)) (?v_359 (not x196)) (?v_360 (not x197)) (?v_361 (not x198)) (?v_362 (not x199)) (?v_363 (and (not x200) true))) (let ((?v_366 (and ?v_362 ?v_363))) (let ((?v_371 (and ?v_361 ?v_366))) (let ((?v_380 (and ?v_360 ?v_371))) (let ((?v_397 (and ?v_359 ?v_380)) (?v_365 (and x200 true))) (let ((?v_367 (and ?v_362 ?v_365))) (let ((?v_372 (and ?v_361 ?v_367))) (let ((?v_381 (and ?v_360 ?v_372))) (let ((?v_398 (and ?v_359 ?v_381)) (?v_364 (= tmp71 200)) (?v_369 (and x199 ?v_363))) (let ((?v_373 (and ?v_361 ?v_369))) (let ((?v_382 (and ?v_360 ?v_373))) (let ((?v_399 (and ?v_359 ?v_382)) (?v_370 (and x199 ?v_365))) (let ((?v_374 (and ?v_361 ?v_370))) (let ((?v_383 (and ?v_360 ?v_374))) (let ((?v_400 (and ?v_359 ?v_383)) (?v_368 (= tmp71 400)) (?v_376 (and x198 ?v_366))) (let ((?v_384 (and ?v_360 ?v_376))) (let ((?v_401 (and ?v_359 ?v_384)) (?v_377 (and x198 ?v_367))) (let ((?v_385 (and ?v_360 ?v_377))) (let ((?v_402 (and ?v_359 ?v_385)) (?v_378 (and x198 ?v_369))) (let ((?v_386 (and ?v_360 ?v_378))) (let ((?v_403 (and ?v_359 ?v_386)) (?v_379 (and x198 ?v_370))) (let ((?v_387 (and ?v_360 ?v_379))) (let ((?v_404 (and ?v_359 ?v_387)) (?v_375 (= tmp71 600)) (?v_389 (and x197 ?v_371))) (let ((?v_405 (and ?v_359 ?v_389)) (?v_390 (and x197 ?v_372))) (let ((?v_406 (and ?v_359 ?v_390)) (?v_391 (and x197 ?v_373))) (let ((?v_407 (and ?v_359 ?v_391)) (?v_392 (and x197 ?v_374))) (let ((?v_408 (and ?v_359 ?v_392)) (?v_393 (and x197 ?v_376))) (let ((?v_409 (and ?v_359 ?v_393)) (?v_394 (and x197 ?v_377))) (let ((?v_410 (and ?v_359 ?v_394)) (?v_395 (and x197 ?v_378))) (let ((?v_411 (and ?v_359 ?v_395)) (?v_396 (and x197 ?v_379))) (let ((?v_412 (and ?v_359 ?v_396)) (?v_388 (= tmp71 800)) (?v_414 (and x196 ?v_380)) (?v_415 (and x196 ?v_381)) (?v_416 (and x196 ?v_382)) (?v_417 (and x196 ?v_383)) (?v_418 (and x196 ?v_384)) (?v_419 (and x196 ?v_385)) (?v_420 (and x196 ?v_386)) (?v_421 (and x196 ?v_387)) (?v_422 (and x196 ?v_389)) (?v_423 (and x196 ?v_390)) (?v_424 (and x196 ?v_391)) (?v_425 (and x196 ?v_392)) (?v_426 (and x196 ?v_393)) (?v_427 (and x196 ?v_394)) (?v_428 (and x196 ?v_395)) (?v_429 (and x196 ?v_396)) (?v_413 (= tmp71 1000)) (?v_430 (not x228)) (?v_431 (not x227)) (?v_432 (not x226)) (?v_433 (not x225)) (?v_434 (not x224)) (?v_435 (and (not x223) true))) (let ((?v_438 (and ?v_434 ?v_435))) (let ((?v_444 (and ?v_433 ?v_438))) (let ((?v_454 (and ?v_432 ?v_444))) (let ((?v_472 (and ?v_431 ?v_454)) (?v_437 (and x223 true))) (let ((?v_440 (and ?v_434 ?v_437))) (let ((?v_445 (and ?v_433 ?v_440))) (let ((?v_455 (and ?v_432 ?v_445))) (let ((?v_473 (and ?v_431 ?v_455)) (?v_436 (= tmp70 250)) (?v_441 (and x224 ?v_435))) (let ((?v_446 (and ?v_433 ?v_441))) (let ((?v_456 (and ?v_432 ?v_446))) (let ((?v_474 (and ?v_431 ?v_456)) (?v_443 (and x224 ?v_437))) (let ((?v_447 (and ?v_433 ?v_443))) (let ((?v_457 (and ?v_432 ?v_447))) (let ((?v_475 (and ?v_431 ?v_457)) (?v_439 (= tmp70 500)) (?v_449 (and x225 ?v_438))) (let ((?v_458 (and ?v_432 ?v_449))) (let ((?v_476 (and ?v_431 ?v_458)) (?v_450 (and x225 ?v_440))) (let ((?v_459 (and ?v_432 ?v_450))) (let ((?v_477 (and ?v_431 ?v_459)) (?v_442 (= tmp70 750)) (?v_451 (and x225 ?v_441))) (let ((?v_460 (and ?v_432 ?v_451))) (let ((?v_478 (and ?v_431 ?v_460)) (?v_453 (and x225 ?v_443))) (let ((?v_461 (and ?v_432 ?v_453))) (let ((?v_479 (and ?v_431 ?v_461)) (?v_448 (= tmp70 1000)) (?v_463 (and x226 ?v_444))) (let ((?v_480 (and ?v_431 ?v_463)) (?v_464 (and x226 ?v_445))) (let ((?v_481 (and ?v_431 ?v_464)) (?v_465 (and x226 ?v_446))) (let ((?v_482 (and ?v_431 ?v_465)) (?v_466 (and x226 ?v_447))) (let ((?v_483 (and ?v_431 ?v_466)) (?v_467 (and x226 ?v_449))) (let ((?v_484 (and ?v_431 ?v_467)) (?v_468 (and x226 ?v_450))) (let ((?v_485 (and ?v_431 ?v_468)) (?v_452 (= tmp70 1250)) (?v_469 (and x226 ?v_451))) (let ((?v_486 (and ?v_431 ?v_469)) (?v_471 (and x226 ?v_453))) (let ((?v_487 (and ?v_431 ?v_471)) (?v_462 (= tmp70 1500)) (?v_489 (and x227 ?v_454)) (?v_490 (and x227 ?v_455)) (?v_491 (and x227 ?v_456)) (?v_492 (and x227 ?v_457)) (?v_493 (and x227 ?v_458)) (?v_494 (and x227 ?v_459)) (?v_495 (and x227 ?v_460)) (?v_496 (and x227 ?v_461)) (?v_497 (and x227 ?v_463)) (?v_498 (and x227 ?v_464)) (?v_499 (and x227 ?v_465)) (?v_500 (and x227 ?v_466)) (?v_501 (and x227 ?v_467)) (?v_502 (and x227 ?v_468)) (?v_470 (= tmp70 1750)) (?v_503 (and x227 ?v_469)) (?v_505 (and x227 ?v_471)) (?v_488 (= tmp70 2000)) (?v_504 (= tmp70 2250)) (?v_506 (not x189)) (?v_507 (not x190)) (?v_508 (not x191)) (?v_509 (not x192)) (?v_510 (not x193)) (?v_511 (and (not x194) true))) (let ((?v_514 (and ?v_510 ?v_511))) (let ((?v_519 (and ?v_509 ?v_514))) (let ((?v_528 (and ?v_508 ?v_519))) (let ((?v_545 (and ?v_507 ?v_528)) (?v_513 (and x194 true))) (let ((?v_515 (and ?v_510 ?v_513))) (let ((?v_520 (and ?v_509 ?v_515))) (let ((?v_529 (and ?v_508 ?v_520))) (let ((?v_546 (and ?v_507 ?v_529)) (?v_512 (= tmp69 200)) (?v_517 (and x193 ?v_511))) (let ((?v_521 (and ?v_509 ?v_517))) (let ((?v_530 (and ?v_508 ?v_521))) (let ((?v_547 (and ?v_507 ?v_530)) (?v_518 (and x193 ?v_513))) (let ((?v_522 (and ?v_509 ?v_518))) (let ((?v_531 (and ?v_508 ?v_522))) (let ((?v_548 (and ?v_507 ?v_531)) (?v_516 (= tmp69 400)) (?v_524 (and x192 ?v_514))) (let ((?v_532 (and ?v_508 ?v_524))) (let ((?v_549 (and ?v_507 ?v_532)) (?v_525 (and x192 ?v_515))) (let ((?v_533 (and ?v_508 ?v_525))) (let ((?v_550 (and ?v_507 ?v_533)) (?v_526 (and x192 ?v_517))) (let ((?v_534 (and ?v_508 ?v_526))) (let ((?v_551 (and ?v_507 ?v_534)) (?v_527 (and x192 ?v_518))) (let ((?v_535 (and ?v_508 ?v_527))) (let ((?v_552 (and ?v_507 ?v_535)) (?v_523 (= tmp69 600)) (?v_537 (and x191 ?v_519))) (let ((?v_553 (and ?v_507 ?v_537)) (?v_538 (and x191 ?v_520))) (let ((?v_554 (and ?v_507 ?v_538)) (?v_539 (and x191 ?v_521))) (let ((?v_555 (and ?v_507 ?v_539)) (?v_540 (and x191 ?v_522))) (let ((?v_556 (and ?v_507 ?v_540)) (?v_541 (and x191 ?v_524))) (let ((?v_557 (and ?v_507 ?v_541)) (?v_542 (and x191 ?v_525))) (let ((?v_558 (and ?v_507 ?v_542)) (?v_543 (and x191 ?v_526))) (let ((?v_559 (and ?v_507 ?v_543)) (?v_544 (and x191 ?v_527))) (let ((?v_560 (and ?v_507 ?v_544)) (?v_536 (= tmp69 800)) (?v_562 (and x190 ?v_528)) (?v_563 (and x190 ?v_529)) (?v_564 (and x190 ?v_530)) (?v_565 (and x190 ?v_531)) (?v_566 (and x190 ?v_532)) (?v_567 (and x190 ?v_533)) (?v_568 (and x190 ?v_534)) (?v_569 (and x190 ?v_535)) (?v_570 (and x190 ?v_537)) (?v_571 (and x190 ?v_538)) (?v_572 (and x190 ?v_539)) (?v_573 (and x190 ?v_540)) (?v_574 (and x190 ?v_541)) (?v_575 (and x190 ?v_542)) (?v_576 (and x190 ?v_543)) (?v_577 (and x190 ?v_544)) (?v_561 (= tmp69 1000)) (?v_578 (not x234)) (?v_579 (not x233)) (?v_580 (not x232)) (?v_581 (not x231)) (?v_582 (not x230)) (?v_583 (and (not x229) true))) (let ((?v_586 (and ?v_582 ?v_583))) (let ((?v_591 (and ?v_581 ?v_586))) (let ((?v_600 (and ?v_580 ?v_591))) (let ((?v_619 (and ?v_579 ?v_600)) (?v_585 (and x229 true))) (let ((?v_587 (and ?v_582 ?v_585))) (let ((?v_592 (and ?v_581 ?v_587))) (let ((?v_601 (and ?v_580 ?v_592))) (let ((?v_621 (and ?v_579 ?v_601)) (?v_584 (= tmp68 500)) (?v_589 (and x230 ?v_583))) (let ((?v_593 (and ?v_581 ?v_589))) (let ((?v_602 (and ?v_580 ?v_593))) (let ((?v_622 (and ?v_579 ?v_602)) (?v_590 (and x230 ?v_585))) (let ((?v_594 (and ?v_581 ?v_590))) (let ((?v_604 (and ?v_580 ?v_594))) (let ((?v_623 (and ?v_579 ?v_604)) (?v_588 (= tmp68 1000)) (?v_596 (and x231 ?v_586))) (let ((?v_605 (and ?v_580 ?v_596))) (let ((?v_624 (and ?v_579 ?v_605)) (?v_597 (and x231 ?v_587))) (let ((?v_606 (and ?v_580 ?v_597))) (let ((?v_625 (and ?v_579 ?v_606)) (?v_598 (and x231 ?v_589))) (let ((?v_608 (and ?v_580 ?v_598))) (let ((?v_626 (and ?v_579 ?v_608)) (?v_599 (and x231 ?v_590))) (let ((?v_609 (and ?v_580 ?v_599))) (let ((?v_627 (and ?v_579 ?v_609)) (?v_595 (= tmp68 1500)) (?v_610 (and x232 ?v_591))) (let ((?v_628 (and ?v_579 ?v_610)) (?v_611 (and x232 ?v_592))) (let ((?v_629 (and ?v_579 ?v_611)) (?v_612 (and x232 ?v_593))) (let ((?v_630 (and ?v_579 ?v_612)) (?v_613 (and x232 ?v_594))) (let ((?v_631 (and ?v_579 ?v_613)) (?v_615 (and x232 ?v_596))) (let ((?v_632 (and ?v_579 ?v_615)) (?v_616 (and x232 ?v_597))) (let ((?v_633 (and ?v_579 ?v_616)) (?v_617 (and x232 ?v_598))) (let ((?v_634 (and ?v_579 ?v_617)) (?v_618 (and x232 ?v_599))) (let ((?v_635 (and ?v_579 ?v_618)) (?v_637 (and x233 ?v_600)) (?v_620 (= tmp68 300)) (?v_638 (and x233 ?v_601)) (?v_603 (= tmp68 800)) (?v_639 (and x233 ?v_602)) (?v_641 (and x233 ?v_604)) (?v_607 (= tmp68 1300)) (?v_642 (and x233 ?v_605)) (?v_643 (and x233 ?v_606)) (?v_645 (and x233 ?v_608)) (?v_646 (and x233 ?v_609)) (?v_614 (= tmp68 1800)) (?v_647 (and x233 ?v_610)) (?v_648 (and x233 ?v_611)) (?v_649 (and x233 ?v_612)) (?v_650 (and x233 ?v_613)) (?v_652 (and x233 ?v_615)) (?v_653 (and x233 ?v_616)) (?v_654 (and x233 ?v_617)) (?v_655 (and x233 ?v_618)) (?v_636 (= tmp68 2300)) (?v_640 (= tmp68 1100)) (?v_644 (= tmp68 1600)) (?v_651 (= tmp68 2100)) (?v_656 (not x183)) (?v_657 (not x184)) (?v_658 (not x185)) (?v_659 (not x186)) (?v_660 (not x187)) (?v_661 (and (not x188) true))) (let ((?v_664 (and ?v_660 ?v_661))) (let ((?v_669 (and ?v_659 ?v_664))) (let ((?v_678 (and ?v_658 ?v_669))) (let ((?v_697 (and ?v_657 ?v_678)) (?v_663 (and x188 true))) (let ((?v_665 (and ?v_660 ?v_663))) (let ((?v_670 (and ?v_659 ?v_665))) (let ((?v_679 (and ?v_658 ?v_670))) (let ((?v_699 (and ?v_657 ?v_679)) (?v_662 (= tmp67 200)) (?v_667 (and x187 ?v_661))) (let ((?v_671 (and ?v_659 ?v_667))) (let ((?v_680 (and ?v_658 ?v_671))) (let ((?v_700 (and ?v_657 ?v_680)) (?v_668 (and x187 ?v_663))) (let ((?v_672 (and ?v_659 ?v_668))) (let ((?v_682 (and ?v_658 ?v_672))) (let ((?v_701 (and ?v_657 ?v_682)) (?v_666 (= tmp67 400)) (?v_674 (and x186 ?v_664))) (let ((?v_683 (and ?v_658 ?v_674))) (let ((?v_702 (and ?v_657 ?v_683)) (?v_675 (and x186 ?v_665))) (let ((?v_684 (and ?v_658 ?v_675))) (let ((?v_703 (and ?v_657 ?v_684)) (?v_676 (and x186 ?v_667))) (let ((?v_686 (and ?v_658 ?v_676))) (let ((?v_704 (and ?v_657 ?v_686)) (?v_677 (and x186 ?v_668))) (let ((?v_687 (and ?v_658 ?v_677))) (let ((?v_705 (and ?v_657 ?v_687)) (?v_673 (= tmp67 600)) (?v_688 (and x185 ?v_669))) (let ((?v_706 (and ?v_657 ?v_688)) (?v_689 (and x185 ?v_670))) (let ((?v_707 (and ?v_657 ?v_689)) (?v_690 (and x185 ?v_671))) (let ((?v_708 (and ?v_657 ?v_690)) (?v_691 (and x185 ?v_672))) (let ((?v_709 (and ?v_657 ?v_691)) (?v_693 (and x185 ?v_674))) (let ((?v_710 (and ?v_657 ?v_693)) (?v_694 (and x185 ?v_675))) (let ((?v_711 (and ?v_657 ?v_694)) (?v_695 (and x185 ?v_676))) (let ((?v_712 (and ?v_657 ?v_695)) (?v_696 (and x185 ?v_677))) (let ((?v_713 (and ?v_657 ?v_696)) (?v_723 (= tmp67 800)) (?v_715 (and x184 ?v_678)) (?v_698 (= tmp67 100)) (?v_716 (and x184 ?v_679)) (?v_681 (= tmp67 300)) (?v_717 (and x184 ?v_680)) (?v_718 (and x184 ?v_682)) (?v_685 (= tmp67 500)) (?v_719 (and x184 ?v_683)) (?v_720 (and x184 ?v_684)) (?v_721 (and x184 ?v_686)) (?v_722 (and x184 ?v_687)) (?v_692 (= tmp67 700)) (?v_724 (and x184 ?v_688)) (?v_725 (and x184 ?v_689)) (?v_726 (and x184 ?v_690)) (?v_727 (and x184 ?v_691)) (?v_728 (and x184 ?v_693)) (?v_729 (and x184 ?v_694)) (?v_730 (and x184 ?v_695)) (?v_731 (and x184 ?v_696)) (?v_714 (= tmp67 900)) (?v_732 (not x240)) (?v_733 (not x239)) (?v_734 (not x238)) (?v_735 (not x237)) (?v_736 (not x236)) (?v_737 (and (not x235) true))) (let ((?v_740 (and ?v_736 ?v_737))) (let ((?v_745 (and ?v_735 ?v_740))) (let ((?v_754 (and ?v_734 ?v_745))) (let ((?v_771 (and ?v_733 ?v_754)) (?v_739 (and x235 true))) (let ((?v_741 (and ?v_736 ?v_739))) (let ((?v_746 (and ?v_735 ?v_741))) (let ((?v_755 (and ?v_734 ?v_746))) (let ((?v_772 (and ?v_733 ?v_755)) (?v_738 (= tmp66 300)) (?v_743 (and x236 ?v_737))) (let ((?v_747 (and ?v_735 ?v_743))) (let ((?v_756 (and ?v_734 ?v_747))) (let ((?v_773 (and ?v_733 ?v_756)) (?v_744 (and x236 ?v_739))) (let ((?v_748 (and ?v_735 ?v_744))) (let ((?v_757 (and ?v_734 ?v_748))) (let ((?v_774 (and ?v_733 ?v_757)) (?v_742 (= tmp66 600)) (?v_750 (and x237 ?v_740))) (let ((?v_758 (and ?v_734 ?v_750))) (let ((?v_775 (and ?v_733 ?v_758)) (?v_751 (and x237 ?v_741))) (let ((?v_759 (and ?v_734 ?v_751))) (let ((?v_776 (and ?v_733 ?v_759)) (?v_752 (and x237 ?v_743))) (let ((?v_760 (and ?v_734 ?v_752))) (let ((?v_777 (and ?v_733 ?v_760)) (?v_753 (and x237 ?v_744))) (let ((?v_761 (and ?v_734 ?v_753))) (let ((?v_778 (and ?v_733 ?v_761)) (?v_749 (= tmp66 900)) (?v_763 (and x238 ?v_745))) (let ((?v_779 (and ?v_733 ?v_763)) (?v_764 (and x238 ?v_746))) (let ((?v_780 (and ?v_733 ?v_764)) (?v_765 (and x238 ?v_747))) (let ((?v_781 (and ?v_733 ?v_765)) (?v_766 (and x238 ?v_748))) (let ((?v_782 (and ?v_733 ?v_766)) (?v_767 (and x238 ?v_750))) (let ((?v_783 (and ?v_733 ?v_767)) (?v_768 (and x238 ?v_751))) (let ((?v_784 (and ?v_733 ?v_768)) (?v_769 (and x238 ?v_752))) (let ((?v_785 (and ?v_733 ?v_769)) (?v_770 (and x238 ?v_753))) (let ((?v_786 (and ?v_733 ?v_770)) (?v_762 (= tmp66 1200)) (?v_788 (and x239 ?v_754)) (?v_789 (and x239 ?v_755)) (?v_790 (and x239 ?v_756)) (?v_791 (and x239 ?v_757)) (?v_792 (and x239 ?v_758)) (?v_793 (and x239 ?v_759)) (?v_794 (and x239 ?v_760)) (?v_795 (and x239 ?v_761)) (?v_796 (and x239 ?v_763)) (?v_797 (and x239 ?v_764)) (?v_798 (and x239 ?v_765)) (?v_799 (and x239 ?v_766)) (?v_800 (and x239 ?v_767)) (?v_801 (and x239 ?v_768)) (?v_802 (and x239 ?v_769)) (?v_803 (and x239 ?v_770)) (?v_787 (= tmp66 1500)) (?v_804 (not x177)) (?v_805 (not x178)) (?v_806 (not x179)) (?v_807 (not x180)) (?v_808 (not x181)) (?v_809 (and (not x182) true))) (let ((?v_812 (and ?v_808 ?v_809))) (let ((?v_817 (and ?v_807 ?v_812))) (let ((?v_826 (and ?v_806 ?v_817))) (let ((?v_843 (and ?v_805 ?v_826)) (?v_811 (and x182 true))) (let ((?v_813 (and ?v_808 ?v_811))) (let ((?v_818 (and ?v_807 ?v_813))) (let ((?v_827 (and ?v_806 ?v_818))) (let ((?v_844 (and ?v_805 ?v_827)) (?v_810 (= tmp65 100)) (?v_815 (and x181 ?v_809))) (let ((?v_819 (and ?v_807 ?v_815))) (let ((?v_828 (and ?v_806 ?v_819))) (let ((?v_845 (and ?v_805 ?v_828)) (?v_816 (and x181 ?v_811))) (let ((?v_820 (and ?v_807 ?v_816))) (let ((?v_829 (and ?v_806 ?v_820))) (let ((?v_846 (and ?v_805 ?v_829)) (?v_814 (= tmp65 200)) (?v_822 (and x180 ?v_812))) (let ((?v_830 (and ?v_806 ?v_822))) (let ((?v_847 (and ?v_805 ?v_830)) (?v_823 (and x180 ?v_813))) (let ((?v_831 (and ?v_806 ?v_823))) (let ((?v_848 (and ?v_805 ?v_831)) (?v_824 (and x180 ?v_815))) (let ((?v_832 (and ?v_806 ?v_824))) (let ((?v_849 (and ?v_805 ?v_832)) (?v_825 (and x180 ?v_816))) (let ((?v_833 (and ?v_806 ?v_825))) (let ((?v_850 (and ?v_805 ?v_833)) (?v_821 (= tmp65 300)) (?v_835 (and x179 ?v_817))) (let ((?v_851 (and ?v_805 ?v_835)) (?v_836 (and x179 ?v_818))) (let ((?v_852 (and ?v_805 ?v_836)) (?v_837 (and x179 ?v_819))) (let ((?v_853 (and ?v_805 ?v_837)) (?v_838 (and x179 ?v_820))) (let ((?v_854 (and ?v_805 ?v_838)) (?v_839 (and x179 ?v_822))) (let ((?v_855 (and ?v_805 ?v_839)) (?v_840 (and x179 ?v_823))) (let ((?v_856 (and ?v_805 ?v_840)) (?v_841 (and x179 ?v_824))) (let ((?v_857 (and ?v_805 ?v_841)) (?v_842 (and x179 ?v_825))) (let ((?v_858 (and ?v_805 ?v_842)) (?v_834 (= tmp65 400)) (?v_860 (and x178 ?v_826)) (?v_861 (and x178 ?v_827)) (?v_862 (and x178 ?v_828)) (?v_863 (and x178 ?v_829)) (?v_864 (and x178 ?v_830)) (?v_865 (and x178 ?v_831)) (?v_866 (and x178 ?v_832)) (?v_867 (and x178 ?v_833)) (?v_868 (and x178 ?v_835)) (?v_869 (and x178 ?v_836)) (?v_870 (and x178 ?v_837)) (?v_871 (and x178 ?v_838)) (?v_872 (and x178 ?v_839)) (?v_873 (and x178 ?v_840)) (?v_874 (and x178 ?v_841)) (?v_875 (and x178 ?v_842)) (?v_859 (= tmp65 500))) (and (<= (+ (+ (* 1 tmp75) 0) (+ (* 1 tmp73) (+ (* 1 tmp71) (+ (* 1 tmp69) (+ (* 1 tmp67) (+ (* 1 tmp65) (+ (* 2 x112) (+ (* 2 x111) (+ (* 2 x110) (+ (* 2 x109) (+ (* 2 x108) (+ (* 2 x107) (+ (* 2 x106) (+ (* 2 x105) (+ (* 2 x104) (+ (* 2 x103) (+ (* 2 x102) (+ (* 2 x101) (+ (* 2 x100) (+ (* 2 x99) (+ (* 2 x98) (+ (* 2 x97) (+ (* 2 x96) (+ (* 2 x95) (+ (* 2 x94) (+ (* 2 x93) (+ (* 2 x92) (+ (* 2 x91) (+ (* 2 x90) (+ (* 2 x89) (+ (* 2 x88) (+ (* 2 x87) (+ (* 2 x86) (+ (* 2 x85) (+ (* 2 x84) (+ (* 2 x83) (+ (* 2 x82) (+ (* 2 x81) (+ (* 2 x80) (+ (* 2 x79) (+ (* 2 x78) (+ (* 2 x77) (+ (* 2 x76) (+ (* 2 x75) (+ (* 2 x74) (+ (* 2 x73) (+ (* 2 x72) (+ (* 2 x71) (+ (* 2 x70) (+ (* 2 x69) (+ (* 2 x68) (+ (* 2 x67) (+ (* 2 x66) (+ (* 2 x65) (+ (* 2 x64) (+ (* 2 x63) (+ (* 2 x62) (+ (* 2 x61) (+ (* 2 x60) (+ (* 2 x59) (+ (* 2 x58) (+ (* 2 x57) (+ ?v_64 (+ ?v_65 (+ ?v_66 (+ ?v_67 (+ ?v_68 (+ ?v_69 (+ ?v_70 (+ ?v_71 (+ ?v_72 (+ ?v_73 (+ ?v_74 (+ ?v_75 (+ ?v_76 (+ ?v_77 (+ ?v_78 (+ ?v_79 (+ ?v_80 (+ ?v_81 (+ ?v_82 (+ ?v_83 (+ ?v_84 (+ ?v_85 (+ ?v_86 (+ ?v_87 (+ ?v_88 (+ ?v_89 (+ ?v_90 (+ ?v_91 (+ ?v_92 (+ ?v_93 (+ ?v_94 (+ ?v_95 (+ ?v_96 (+ ?v_97 (+ ?v_98 (+ ?v_99 (+ ?v_100 (+ ?v_101 (+ ?v_102 (+ ?v_103 (+ ?v_104 (+ ?v_105 (+ ?v_106 (+ ?v_107 (+ ?v_108 (+ ?v_109 (+ ?v_110 (+ ?v_111 (+ ?v_112 (+ ?v_113 (+ ?v_114 (+ ?v_115 (+ ?v_116 (+ ?v_117 (+ ?v_118 (+ ?v_119 (+ (* 1 tmp66) (+ (* 1 tmp68) (+ (* 1 tmp70) (+ (* 1 tmp72) (+ (* 1 tmp74) 0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 3000) (<= (+ (+ (* 1 tmp64) 0) (+ ?v_7 0)) 0) (<= (+ (+ (* 1 tmp63) 0) (+ ?v_15 0)) 0) (<= (+ (+ (* 1 tmp62) 0) (+ ?v_23 0)) 0) (<= (+ (+ (* 1 tmp61) 0) (+ ?v_31 0)) 0) (<= (+ (+ (* 1 tmp60) 0) (+ ?v_39 0)) 0) (<= (+ (+ (* 1 tmp59) 0) (+ ?v_47 0)) 0) (<= (+ (+ (* 1 tmp58) 0) (+ ?v_55 0)) 0) (<= (+ (+ (* 1 tmp57) 0) (+ ?v_63 0)) 0) (<= (+ (+ (* 1 tmp56) 0) (+ ?v_6 0)) 0) (<= (+ (+ (* 1 tmp55) 0) (+ ?v_14 0)) 0) (<= (+ (+ (* 1 tmp54) 0) (+ ?v_22 0)) 0) (<= (+ (+ (* 1 tmp53) 0) (+ ?v_30 0)) 0) (<= (+ (+ (* 1 tmp52) 0) (+ ?v_38 0)) 0) (<= (+ (+ (* 1 tmp51) 0) (+ ?v_46 0)) 0) (<= (+ (+ (* 1 tmp50) 0) (+ ?v_54 0)) 0) (<= (+ (+ (* 1 tmp49) 0) (+ ?v_62 0)) 0) (<= (+ (+ (* 1 tmp48) 0) (+ ?v_5 0)) 0) (<= (+ (+ (* 1 tmp47) 0) (+ ?v_13 0)) 0) (<= (+ (+ (* 1 tmp46) 0) (+ ?v_21 0)) 0) (<= (+ (+ (* 1 tmp45) 0) (+ ?v_29 0)) 0) (<= (+ (+ (* 1 tmp44) 0) (+ ?v_37 0)) 0) (<= (+ (+ (* 1 tmp43) 0) (+ ?v_45 0)) 0) (<= (+ (+ (* 1 tmp42) 0) (+ ?v_53 0)) 0) (<= (+ (+ (* 1 tmp41) 0) (+ ?v_61 0)) 0) (<= (+ (+ (* 1 tmp40) 0) (+ ?v_4 0)) 0) (<= (+ (+ (* 1 tmp39) 0) (+ ?v_12 0)) 0) (<= (+ (+ (* 1 tmp38) 0) (+ ?v_20 0)) 0) (<= (+ (+ (* 1 tmp37) 0) (+ ?v_28 0)) 0) (<= (+ (+ (* 1 tmp36) 0) (+ ?v_36 0)) 0) (<= (+ (+ (* 1 tmp35) 0) (+ ?v_44 0)) 0) (<= (+ (+ (* 1 tmp34) 0) (+ ?v_52 0)) 0) (<= (+ (+ (* 1 tmp33) 0) (+ ?v_60 0)) 0) (<= (+ (+ (* 1 tmp32) 0) (+ ?v_3 0)) 0) (<= (+ (+ (* 1 tmp31) 0) (+ ?v_11 0)) 0) (<= (+ (+ (* 1 tmp30) 0) (+ ?v_19 0)) 0) (<= (+ (+ (* 1 tmp29) 0) (+ ?v_27 0)) 0) (<= (+ (+ (* 1 tmp28) 0) (+ ?v_35 0)) 0) (<= (+ (+ (* 1 tmp27) 0) (+ ?v_43 0)) 0) (<= (+ (+ (* 1 tmp26) 0) (+ ?v_51 0)) 0) (<= (+ (+ (* 1 tmp25) 0) (+ ?v_59 0)) 0) (<= (+ (+ (* 1 tmp24) 0) (+ ?v_2 0)) 0) (<= (+ (+ (* 1 tmp23) 0) (+ ?v_10 0)) 0) (<= (+ (+ (* 1 tmp22) 0) (+ ?v_18 0)) 0) (<= (+ (+ (* 1 tmp21) 0) (+ ?v_26 0)) 0) (<= (+ (+ (* 1 tmp20) 0) (+ ?v_34 0)) 0) (<= (+ (+ (* 1 tmp19) 0) (+ ?v_42 0)) 0) (<= (+ (+ (* 1 tmp18) 0) (+ ?v_50 0)) 0) (<= (+ (+ (* 1 tmp17) 0) (+ ?v_58 0)) 0) (<= (+ (+ (* 1 tmp16) 0) (+ ?v_1 0)) 0) (<= (+ (+ (* 1 tmp15) 0) (+ ?v_9 0)) 0) (<= (+ (+ (* 1 tmp14) 0) (+ ?v_17 0)) 0) (<= (+ (+ (* 1 tmp13) 0) (+ ?v_25 0)) 0) (<= (+ (+ (* 1 tmp12) 0) (+ ?v_33 0)) 0) (<= (+ (+ (* 1 tmp11) 0) (+ ?v_41 0)) 0) (<= (+ (+ (* 1 tmp10) 0) (+ ?v_49 0)) 0) (<= (+ (+ (* 1 tmp9) 0) (+ ?v_57 0)) 0) (<= (+ (+ (* 1 tmp8) 0) (+ ?v_0 0)) 0) (<= (+ (+ (* 1 tmp7) 0) (+ ?v_8 0)) 0) (<= (+ (+ (* 1 tmp6) 0) (+ ?v_16 0)) 0) (<= (+ (+ (* 1 tmp5) 0) (+ ?v_24 0)) 0) (<= (+ (+ (* 1 tmp4) 0) (+ ?v_32 0)) 0) (<= (+ (+ (* 1 tmp3) 0) (+ ?v_40 0)) 0) (<= (+ (+ (* 1 tmp2) 0) (+ ?v_48 0)) 0) (<= (+ (+ (* 1 tmp1) 0) (+ ?v_56 0)) 0) (<= (+ (+ (+ (+ (+ (+ (+ (+ 0 ?v_0) ?v_1) ?v_2) ?v_3) ?v_4) ?v_5) ?v_6) ?v_7) 500) (<= (+ (+ (+ (+ (+ (+ (+ (+ 0 ?v_8) ?v_9) ?v_10) ?v_11) ?v_12) ?v_13) ?v_14) ?v_15) 400) (<= (+ (+ (+ (+ (+ (+ (+ (+ 0 ?v_16) ?v_17) ?v_18) ?v_19) ?v_20) ?v_21) ?v_22) ?v_23) 400) (<= (+ (+ (+ (+ (+ (+ (+ (+ 0 ?v_24) ?v_25) ?v_26) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) 400) (<= (+ (+ (+ (+ (+ (+ (+ (+ 0 ?v_32) ?v_33) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) 400) (<= (+ (+ (+ (+ (+ (+ (+ (+ 0 ?v_40) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47) 350) (<= (+ (+ (+ (+ (+ (+ (+ (+ 0 ?v_48) ?v_49) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54) ?v_55) 350) (<= (+ (+ (+ (+ (+ (+ (+ (+ 0 ?v_56) ?v_57) ?v_58) ?v_59) ?v_60) ?v_61) ?v_62) ?v_63) 350) (= (+ (+ (+ 0 ?v_64) (* (- 1) x112)) ?v_7) 30) (= (+ (+ (+ (+ (+ 0 ?v_65) (* (- 1) x56)) (* (- 1) x111)) (* 1 x112)) ?v_15) 20) (= (+ (+ (+ (+ (+ 0 ?v_66) (* (- 1) x55)) (* (- 1) x110)) (* 1 x111)) ?v_23) 10) (= (+ (+ (+ (+ (+ 0 ?v_67) (* (- 1) x54)) (* (- 1) x109)) (* 1 x110)) ?v_31) 10) (= (+ (+ (+ (+ (+ 0 ?v_68) (* (- 1) x53)) (* (- 1) x108)) (* 1 x109)) ?v_39) 0) (= (+ (+ (+ (+ (+ 0 ?v_69) (* (- 1) x52)) (* (- 1) x107)) (* 1 x108)) ?v_47) 0) (= (+ (+ (+ (+ (+ 0 ?v_70) (* (- 1) x51)) (* (- 1) x106)) (* 1 x107)) ?v_55) 20) (= (+ (+ (+ 0 (* (- 1) x50)) (* 1 x106)) ?v_63) 10) (= (+ (+ (+ 0 ?v_71) (* (- 1) x105)) ?v_6) 40) (= (+ (+ (+ (+ (+ 0 ?v_72) (* (- 1) x49)) (* (- 1) x104)) (* 1 x105)) ?v_14) 40) (= (+ (+ (+ (+ (+ 0 ?v_73) (* (- 1) x48)) (* (- 1) x103)) (* 1 x104)) ?v_22) 60) (= (+ (+ (+ (+ (+ 0 ?v_74) (* (- 1) x47)) (* (- 1) x102)) (* 1 x103)) ?v_30) 20) (= (+ (+ (+ (+ (+ 0 ?v_75) (* (- 1) x46)) (* (- 1) x101)) (* 1 x102)) ?v_38) 10) (= (+ (+ (+ (+ (+ 0 ?v_76) (* (- 1) x45)) (* (- 1) x100)) (* 1 x101)) ?v_46) 50) (= (+ (+ (+ (+ (+ 0 ?v_77) (* (- 1) x44)) (* (- 1) x99)) (* 1 x100)) ?v_54) 20) (= (+ (+ (+ 0 (* (- 1) x43)) (* 1 x99)) ?v_62) 0) (= (+ (+ (+ 0 ?v_78) (* (- 1) x98)) ?v_5) 50) (= (+ (+ (+ (+ (+ 0 ?v_79) (* (- 1) x42)) (* (- 1) x97)) (* 1 x98)) ?v_13) 40) (= (+ (+ (+ (+ (+ 0 ?v_80) (* (- 1) x41)) (* (- 1) x96)) (* 1 x97)) ?v_21) 20) (= (+ (+ (+ (+ (+ 0 ?v_81) (* (- 1) x40)) (* (- 1) x95)) (* 1 x96)) ?v_29) 100) (= (+ (+ (+ (+ (+ 0 ?v_82) (* (- 1) x39)) (* (- 1) x94)) (* 1 x95)) ?v_37) 40) (= (+ (+ (+ (+ (+ 0 ?v_83) (* (- 1) x38)) (* (- 1) x93)) (* 1 x94)) ?v_45) 40) (= (+ (+ (+ (+ (+ 0 ?v_84) (* (- 1) x37)) (* (- 1) x92)) (* 1 x93)) ?v_53) 40) (= (+ (+ (+ 0 (* (- 1) x36)) (* 1 x92)) ?v_61) 70) (= (+ (+ (+ 0 ?v_85) (* (- 1) x91)) ?v_4) 10) (= (+ (+ (+ (+ (+ 0 ?v_86) (* (- 1) x35)) (* (- 1) x90)) (* 1 x91)) ?v_12) 20) (= (+ (+ (+ (+ (+ 0 ?v_87) (* (- 1) x34)) (* (- 1) x89)) (* 1 x90)) ?v_20) 10) (= (+ (+ (+ (+ (+ 0 ?v_88) (* (- 1) x33)) (* (- 1) x88)) (* 1 x89)) ?v_28) 10) (= (+ (+ (+ (+ (+ 0 ?v_89) (* (- 1) x32)) (* (- 1) x87)) (* 1 x88)) ?v_36) 40) (= (+ (+ (+ (+ (+ 0 ?v_90) (* (- 1) x31)) (* (- 1) x86)) (* 1 x87)) ?v_44) 20) (= (+ (+ (+ (+ (+ 0 ?v_91) (* (- 1) x30)) (* (- 1) x85)) (* 1 x86)) ?v_52) 0) (= (+ (+ (+ 0 (* (- 1) x29)) (* 1 x85)) ?v_60) 50) (= (+ (+ (+ 0 ?v_92) (* (- 1) x84)) ?v_3) 100) (= (+ (+ (+ (+ (+ 0 ?v_93) (* (- 1) x28)) (* (- 1) x83)) (* 1 x84)) ?v_11) 100) (= (+ (+ (+ (+ (+ 0 ?v_94) (* (- 1) x27)) (* (- 1) x82)) (* 1 x83)) ?v_19) 90) (= (+ (+ (+ (+ (+ 0 ?v_95) (* (- 1) x26)) (* (- 1) x81)) (* 1 x82)) ?v_27) 160) (= (+ (+ (+ (+ (+ 0 ?v_96) (* (- 1) x25)) (* (- 1) x80)) (* 1 x81)) ?v_35) 150) (= (+ (+ (+ (+ (+ 0 ?v_97) (* (- 1) x24)) (* (- 1) x79)) (* 1 x80)) ?v_43) 100) (= (+ (+ (+ (+ (+ 0 ?v_98) (* (- 1) x23)) (* (- 1) x78)) (* 1 x79)) ?v_51) 100) (= (+ (+ (+ 0 (* (- 1) x22)) (* 1 x78)) ?v_59) 0) (= (+ (+ (+ 0 ?v_99) (* (- 1) x77)) ?v_2) 160) (= (+ (+ (+ (+ (+ 0 ?v_100) (* (- 1) x21)) (* (- 1) x76)) (* 1 x77)) ?v_10) 90) (= (+ (+ (+ (+ (+ 0 ?v_101) (* (- 1) x20)) (* (- 1) x75)) (* 1 x76)) ?v_18) 80) (= (+ (+ (+ (+ (+ 0 ?v_102) (* (- 1) x19)) (* (- 1) x74)) (* 1 x75)) ?v_26) 40) (= (+ (+ (+ (+ (+ 0 ?v_103) (* (- 1) x18)) (* (- 1) x73)) (* 1 x74)) ?v_34) 100) (= (+ (+ (+ (+ (+ 0 ?v_104) (* (- 1) x17)) (* (- 1) x72)) (* 1 x73)) ?v_42) 0) (= (+ (+ (+ (+ (+ 0 ?v_105) (* (- 1) x16)) (* (- 1) x71)) (* 1 x72)) ?v_50) 50) (= (+ (+ (+ 0 (* (- 1) x15)) (* 1 x71)) ?v_58) 40) (= (+ (+ (+ 0 ?v_106) (* (- 1) x70)) ?v_1) 50) (= (+ (+ (+ (+ (+ 0 ?v_107) (* (- 1) x14)) (* (- 1) x69)) (* 1 x70)) ?v_9) 40) (= (+ (+ (+ (+ (+ 0 ?v_108) (* (- 1) x13)) (* (- 1) x68)) (* 1 x69)) ?v_17) 0) (= (+ (+ (+ (+ (+ 0 ?v_109) (* (- 1) x12)) (* (- 1) x67)) (* 1 x68)) ?v_25) 30) (= (+ (+ (+ (+ (+ 0 ?v_110) (* (- 1) x11)) (* (- 1) x66)) (* 1 x67)) ?v_33) 10) (= (+ (+ (+ (+ (+ 0 ?v_111) (* (- 1) x10)) (* (- 1) x65)) (* 1 x66)) ?v_41) 50) (= (+ (+ (+ (+ (+ 0 ?v_112) (* (- 1) x9)) (* (- 1) x64)) (* 1 x65)) ?v_49) 40) (= (+ (+ (+ 0 (* (- 1) x8)) (* 1 x64)) ?v_57) 20) (= (+ (+ (+ 0 ?v_113) (* (- 1) x63)) ?v_0) 100) (= (+ (+ (+ (+ (+ 0 ?v_114) (* (- 1) x7)) (* (- 1) x62)) (* 1 x63)) ?v_8) 0) (= (+ (+ (+ (+ (+ 0 ?v_115) (* (- 1) x6)) (* (- 1) x61)) (* 1 x62)) ?v_16) 80) (= (+ (+ (+ (+ (+ 0 ?v_116) (* (- 1) x5)) (* (- 1) x60)) (* 1 x61)) ?v_24) 20) (= (+ (+ (+ (+ (+ 0 ?v_117) (* (- 1) x4)) (* (- 1) x59)) (* 1 x60)) ?v_32) 100) (= (+ (+ (+ (+ (+ 0 ?v_118) (* (- 1) x3)) (* (- 1) x58)) (* 1 x59)) ?v_40) 50) (= (+ (+ (+ (+ (+ 0 ?v_119) (* (- 1) x2)) (* (- 1) x57)) (* 1 x58)) ?v_48) 70) (= (+ (+ (+ 0 (* (- 1) x1)) (* 1 x57)) ?v_56) 0) (>= x1 0) (>= x2 0) (>= x3 0) (>= x4 0) (>= x5 0) (>= x6 0) (>= x7 0) (>= x8 0) (>= x9 0) (>= x10 0) (>= x11 0) (>= x12 0) (>= x13 0) (>= x14 0) (>= x15 0) (>= x16 0) (>= x17 0) (>= x18 0) (>= x19 0) (>= x20 0) (>= x21 0) (>= x22 0) (>= x23 0) (>= x24 0) (>= x25 0) (>= x26 0) (>= x27 0) (>= x28 0) (>= x29 0) (>= x30 0) (>= x31 0) (>= x32 0) (>= x33 0) (>= x34 0) (>= x35 0) (>= x36 0) (>= x37 0) (>= x38 0) (>= x39 0) (>= x40 0) (>= x41 0) (>= x42 0) (>= x43 0) (>= x44 0) (>= x45 0) (>= x46 0) (>= x47 0) (>= x48 0) (>= x49 0) (>= x50 0) (>= x51 0) (>= x52 0) (>= x53 0) (>= x54 0) (>= x55 0) (>= x56 0) (>= x57 0) (>= x58 0) (>= x59 0) (>= x60 0) (>= x61 0) (>= x62 0) (>= x63 0) (>= x64 0) (>= x65 0) (>= x66 0) (>= x67 0) (>= x68 0) (>= x69 0) (>= x70 0) (>= x71 0) (>= x72 0) (>= x73 0) (>= x74 0) (>= x75 0) (>= x76 0) (>= x77 0) (>= x78 0) (>= x79 0) (>= x80 0) (>= x81 0) (>= x82 0) (>= x83 0) (>= x84 0) (>= x85 0) (>= x86 0) (>= x87 0) (>= x88 0) (>= x89 0) (>= x90 0) (>= x91 0) (>= x92 0) (>= x93 0) (>= x94 0) (>= x95 0) (>= x96 0) (>= x97 0) (>= x98 0) (>= x99 0) (>= x100 0) (>= x101 0) (>= x102 0) (>= x103 0) (>= x104 0) (>= x105 0) (>= x106 0) (>= x107 0) (>= x108 0) (>= x109 0) (>= x110 0) (>= x111 0) (>= x112 0) (>= x176 0) (>= x175 0) (>= x174 0) (>= x173 0) (>= x172 0) (>= x171 0) (>= x170 0) (>= x169 0) (>= x168 0) (>= x167 0) (>= x166 0) (>= x165 0) (>= x164 0) (>= x163 0) (>= x162 0) (>= x161 0) (>= x160 0) (>= x159 0) (>= x158 0) (>= x157 0) (>= x156 0) (>= x155 0) (>= x154 0) (>= x153 0) (>= x152 0) (>= x151 0) (>= x150 0) (>= x149 0) (>= x148 0) (>= x147 0) (>= x146 0) (>= x145 0) (>= x144 0) (>= x143 0) (>= x142 0) (>= x141 0) (>= x140 0) (>= x139 0) (>= x138 0) (>= x137 0) (>= x136 0) (>= x135 0) (>= x134 0) (>= x133 0) (>= x132 0) (>= x131 0) (>= x130 0) (>= x129 0) (>= x128 0) (>= x127 0) (>= x126 0) (>= x125 0) (>= x124 0) (>= x123 0) (>= x122 0) (>= x121 0) (>= x120 0) (>= x119 0) (>= x118 0) (>= x117 0) (>= x116 0) (>= x115 0) (>= x114 0) (>= x113 0) (=> (and ?v_120 ?v_131) (= tmp75 0)) (=> (and ?v_120 ?v_133) ?v_124) (=> (and ?v_120 ?v_134) ?v_124) (=> (and ?v_120 ?v_135) (= tmp75 800)) (=> (and ?v_120 ?v_137) ?v_132) (=> (and ?v_120 ?v_138) ?v_129) (=> (and ?v_120 ?v_139) ?v_129) (=> (and ?v_120 ?v_141) ?v_136) (=> (and x207 ?v_131) ?v_132) (=> (and x207 ?v_133) ?v_129) (=> (and x207 ?v_134) ?v_129) (=> (and x207 ?v_135) ?v_136) (=> (and x207 ?v_137) (= tmp75 600)) (=> (and x207 ?v_138) ?v_140) (=> (and x207 ?v_139) ?v_140) (=> (and x207 ?v_141) (= tmp75 1400)) (=> (and ?v_142 ?v_181) (= tmp74 0)) (=> (and ?v_142 ?v_182) ?v_148) (=> (and ?v_142 ?v_183) ?v_148) (=> (and ?v_142 ?v_184) ?v_152) (=> (and ?v_142 ?v_185) ?v_148) (=> (and ?v_142 ?v_186) ?v_152) (=> (and ?v_142 ?v_187) ?v_152) (=> (and ?v_142 ?v_188) ?v_159) (=> (and ?v_142 ?v_189) ?v_148) (=> (and ?v_142 ?v_190) ?v_152) (=> (and ?v_142 ?v_191) ?v_152) (=> (and ?v_142 ?v_192) ?v_159) (=> (and ?v_142 ?v_193) ?v_152) (=> (and ?v_142 ?v_194) ?v_159) (=> (and ?v_142 ?v_195) ?v_159) (=> (and ?v_142 ?v_196) ?v_172) (=> (and ?v_142 ?v_198) ?v_148) (=> (and ?v_142 ?v_199) ?v_152) (=> (and ?v_142 ?v_200) ?v_152) (=> (and ?v_142 ?v_201) ?v_159) (=> (and ?v_142 ?v_202) ?v_152) (=> (and ?v_142 ?v_203) ?v_159) (=> (and ?v_142 ?v_204) ?v_159) (=> (and ?v_142 ?v_205) ?v_172) (=> (and ?v_142 ?v_206) ?v_152) (=> (and ?v_142 ?v_207) ?v_159) (=> (and ?v_142 ?v_208) ?v_159) (=> (and ?v_142 ?v_209) ?v_172) (=> (and ?v_142 ?v_210) ?v_159) (=> (and ?v_142 ?v_211) ?v_172) (=> (and ?v_142 ?v_212) ?v_172) (=> (and ?v_142 ?v_213) ?v_197) (=> (and x216 ?v_181) ?v_148) (=> (and x216 ?v_182) ?v_152) (=> (and x216 ?v_183) ?v_152) (=> (and x216 ?v_184) ?v_159) (=> (and x216 ?v_185) ?v_152) (=> (and x216 ?v_186) ?v_159) (=> (and x216 ?v_187) ?v_159) (=> (and x216 ?v_188) ?v_172) (=> (and x216 ?v_189) ?v_152) (=> (and x216 ?v_190) ?v_159) (=> (and x216 ?v_191) ?v_159) (=> (and x216 ?v_192) ?v_172) (=> (and x216 ?v_193) ?v_159) (=> (and x216 ?v_194) ?v_172) (=> (and x216 ?v_195) ?v_172) (=> (and x216 ?v_196) ?v_197) (=> (and x216 ?v_198) ?v_152) (=> (and x216 ?v_199) ?v_159) (=> (and x216 ?v_200) ?v_159) (=> (and x216 ?v_201) ?v_172) (=> (and x216 ?v_202) ?v_159) (=> (and x216 ?v_203) ?v_172) (=> (and x216 ?v_204) ?v_172) (=> (and x216 ?v_205) ?v_197) (=> (and x216 ?v_206) ?v_159) (=> (and x216 ?v_207) ?v_172) (=> (and x216 ?v_208) ?v_172) (=> (and x216 ?v_209) ?v_197) (=> (and x216 ?v_210) ?v_172) (=> (and x216 ?v_211) ?v_197) (=> (and x216 ?v_212) ?v_197) (=> (and x216 ?v_213) (= tmp74 2400)) (=> (and ?v_214 ?v_253) (= tmp73 0)) (=> (and ?v_214 ?v_254) ?v_220) (=> (and ?v_214 ?v_255) ?v_220) (=> (and ?v_214 ?v_256) ?v_224) (=> (and ?v_214 ?v_257) ?v_220) (=> (and ?v_214 ?v_258) ?v_224) (=> (and ?v_214 ?v_259) ?v_224) (=> (and ?v_214 ?v_260) ?v_231) (=> (and ?v_214 ?v_261) ?v_220) (=> (and ?v_214 ?v_262) ?v_224) (=> (and ?v_214 ?v_263) ?v_224) (=> (and ?v_214 ?v_264) ?v_231) (=> (and ?v_214 ?v_265) ?v_224) (=> (and ?v_214 ?v_266) ?v_231) (=> (and ?v_214 ?v_267) ?v_231) (=> (and ?v_214 ?v_268) ?v_244) (=> (and ?v_214 ?v_270) ?v_220) (=> (and ?v_214 ?v_271) ?v_224) (=> (and ?v_214 ?v_272) ?v_224) (=> (and ?v_214 ?v_273) ?v_231) (=> (and ?v_214 ?v_274) ?v_224) (=> (and ?v_214 ?v_275) ?v_231) (=> (and ?v_214 ?v_276) ?v_231) (=> (and ?v_214 ?v_277) ?v_244) (=> (and ?v_214 ?v_278) ?v_224) (=> (and ?v_214 ?v_279) ?v_231) (=> (and ?v_214 ?v_280) ?v_231) (=> (and ?v_214 ?v_281) ?v_244) (=> (and ?v_214 ?v_282) ?v_231) (=> (and ?v_214 ?v_283) ?v_244) (=> (and ?v_214 ?v_284) ?v_244) (=> (and ?v_214 ?v_285) ?v_269) (=> (and x201 ?v_253) ?v_220) (=> (and x201 ?v_254) ?v_224) (=> (and x201 ?v_255) ?v_224) (=> (and x201 ?v_256) ?v_231) (=> (and x201 ?v_257) ?v_224) (=> (and x201 ?v_258) ?v_231) (=> (and x201 ?v_259) ?v_231) (=> (and x201 ?v_260) ?v_244) (=> (and x201 ?v_261) ?v_224) (=> (and x201 ?v_262) ?v_231) (=> (and x201 ?v_263) ?v_231) (=> (and x201 ?v_264) ?v_244) (=> (and x201 ?v_265) ?v_231) (=> (and x201 ?v_266) ?v_244) (=> (and x201 ?v_267) ?v_244) (=> (and x201 ?v_268) ?v_269) (=> (and x201 ?v_270) ?v_224) (=> (and x201 ?v_271) ?v_231) (=> (and x201 ?v_272) ?v_231) (=> (and x201 ?v_273) ?v_244) (=> (and x201 ?v_274) ?v_231) (=> (and x201 ?v_275) ?v_244) (=> (and x201 ?v_276) ?v_244) (=> (and x201 ?v_277) ?v_269) (=> (and x201 ?v_278) ?v_231) (=> (and x201 ?v_279) ?v_244) (=> (and x201 ?v_280) ?v_244) (=> (and x201 ?v_281) ?v_269) (=> (and x201 ?v_282) ?v_244) (=> (and x201 ?v_283) ?v_269) (=> (and x201 ?v_284) ?v_269) (=> (and x201 ?v_285) (= tmp73 1800)) (=> (and ?v_286 ?v_325) (= tmp72 0)) (=> (and ?v_286 ?v_326) ?v_292) (=> (and ?v_286 ?v_327) ?v_292) (=> (and ?v_286 ?v_328) ?v_296) (=> (and ?v_286 ?v_329) ?v_292) (=> (and ?v_286 ?v_330) ?v_296) (=> (and ?v_286 ?v_331) ?v_296) (=> (and ?v_286 ?v_332) ?v_303) (=> (and ?v_286 ?v_333) ?v_292) (=> (and ?v_286 ?v_334) ?v_296) (=> (and ?v_286 ?v_335) ?v_296) (=> (and ?v_286 ?v_336) ?v_303) (=> (and ?v_286 ?v_337) ?v_296) (=> (and ?v_286 ?v_338) ?v_303) (=> (and ?v_286 ?v_339) ?v_303) (=> (and ?v_286 ?v_340) ?v_316) (=> (and ?v_286 ?v_342) ?v_292) (=> (and ?v_286 ?v_343) ?v_296) (=> (and ?v_286 ?v_344) ?v_296) (=> (and ?v_286 ?v_345) ?v_303) (=> (and ?v_286 ?v_346) ?v_296) (=> (and ?v_286 ?v_347) ?v_303) (=> (and ?v_286 ?v_348) ?v_303) (=> (and ?v_286 ?v_349) ?v_316) (=> (and ?v_286 ?v_350) ?v_296) (=> (and ?v_286 ?v_351) ?v_303) (=> (and ?v_286 ?v_352) ?v_303) (=> (and ?v_286 ?v_353) ?v_316) (=> (and ?v_286 ?v_354) ?v_303) (=> (and ?v_286 ?v_355) ?v_316) (=> (and ?v_286 ?v_356) ?v_316) (=> (and ?v_286 ?v_357) ?v_341) (=> (and x222 ?v_325) ?v_292) (=> (and x222 ?v_326) ?v_296) (=> (and x222 ?v_327) ?v_296) (=> (and x222 ?v_328) ?v_303) (=> (and x222 ?v_329) ?v_296) (=> (and x222 ?v_330) ?v_303) (=> (and x222 ?v_331) ?v_303) (=> (and x222 ?v_332) ?v_316) (=> (and x222 ?v_333) ?v_296) (=> (and x222 ?v_334) ?v_303) (=> (and x222 ?v_335) ?v_303) (=> (and x222 ?v_336) ?v_316) (=> (and x222 ?v_337) ?v_303) (=> (and x222 ?v_338) ?v_316) (=> (and x222 ?v_339) ?v_316) (=> (and x222 ?v_340) ?v_341) (=> (and x222 ?v_342) ?v_296) (=> (and x222 ?v_343) ?v_303) (=> (and x222 ?v_344) ?v_303) (=> (and x222 ?v_345) ?v_316) (=> (and x222 ?v_346) ?v_303) (=> (and x222 ?v_347) ?v_316) (=> (and x222 ?v_348) ?v_316) (=> (and x222 ?v_349) ?v_341) (=> (and x222 ?v_350) ?v_303) (=> (and x222 ?v_351) ?v_316) (=> (and x222 ?v_352) ?v_316) (=> (and x222 ?v_353) ?v_341) (=> (and x222 ?v_354) ?v_316) (=> (and x222 ?v_355) ?v_341) (=> (and x222 ?v_356) ?v_341) (=> (and x222 ?v_357) (= tmp72 1500)) (=> (and ?v_358 ?v_397) (= tmp71 0)) (=> (and ?v_358 ?v_398) ?v_364) (=> (and ?v_358 ?v_399) ?v_364) (=> (and ?v_358 ?v_400) ?v_368) (=> (and ?v_358 ?v_401) ?v_364) (=> (and ?v_358 ?v_402) ?v_368) (=> (and ?v_358 ?v_403) ?v_368) (=> (and ?v_358 ?v_404) ?v_375) (=> (and ?v_358 ?v_405) ?v_364) (=> (and ?v_358 ?v_406) ?v_368) (=> (and ?v_358 ?v_407) ?v_368) (=> (and ?v_358 ?v_408) ?v_375) (=> (and ?v_358 ?v_409) ?v_368) (=> (and ?v_358 ?v_410) ?v_375) (=> (and ?v_358 ?v_411) ?v_375) (=> (and ?v_358 ?v_412) ?v_388) (=> (and ?v_358 ?v_414) ?v_364) (=> (and ?v_358 ?v_415) ?v_368) (=> (and ?v_358 ?v_416) ?v_368) (=> (and ?v_358 ?v_417) ?v_375) (=> (and ?v_358 ?v_418) ?v_368) (=> (and ?v_358 ?v_419) ?v_375) (=> (and ?v_358 ?v_420) ?v_375) (=> (and ?v_358 ?v_421) ?v_388) (=> (and ?v_358 ?v_422) ?v_368) (=> (and ?v_358 ?v_423) ?v_375) (=> (and ?v_358 ?v_424) ?v_375) (=> (and ?v_358 ?v_425) ?v_388) (=> (and ?v_358 ?v_426) ?v_375) (=> (and ?v_358 ?v_427) ?v_388) (=> (and ?v_358 ?v_428) ?v_388) (=> (and ?v_358 ?v_429) ?v_413) (=> (and x195 ?v_397) ?v_364) (=> (and x195 ?v_398) ?v_368) (=> (and x195 ?v_399) ?v_368) (=> (and x195 ?v_400) ?v_375) (=> (and x195 ?v_401) ?v_368) (=> (and x195 ?v_402) ?v_375) (=> (and x195 ?v_403) ?v_375) (=> (and x195 ?v_404) ?v_388) (=> (and x195 ?v_405) ?v_368) (=> (and x195 ?v_406) ?v_375) (=> (and x195 ?v_407) ?v_375) (=> (and x195 ?v_408) ?v_388) (=> (and x195 ?v_409) ?v_375) (=> (and x195 ?v_410) ?v_388) (=> (and x195 ?v_411) ?v_388) (=> (and x195 ?v_412) ?v_413) (=> (and x195 ?v_414) ?v_368) (=> (and x195 ?v_415) ?v_375) (=> (and x195 ?v_416) ?v_375) (=> (and x195 ?v_417) ?v_388) (=> (and x195 ?v_418) ?v_375) (=> (and x195 ?v_419) ?v_388) (=> (and x195 ?v_420) ?v_388) (=> (and x195 ?v_421) ?v_413) (=> (and x195 ?v_422) ?v_375) (=> (and x195 ?v_423) ?v_388) (=> (and x195 ?v_424) ?v_388) (=> (and x195 ?v_425) ?v_413) (=> (and x195 ?v_426) ?v_388) (=> (and x195 ?v_427) ?v_413) (=> (and x195 ?v_428) ?v_413) (=> (and x195 ?v_429) (= tmp71 1200)) (=> (and ?v_430 ?v_472) (= tmp70 0)) (=> (and ?v_430 ?v_473) ?v_436) (=> (and ?v_430 ?v_474) ?v_436) (=> (and ?v_430 ?v_475) ?v_439) (=> (and ?v_430 ?v_476) ?v_439) (=> (and ?v_430 ?v_477) ?v_442) (=> (and ?v_430 ?v_478) ?v_442) (=> (and ?v_430 ?v_479) ?v_448) (=> (and ?v_430 ?v_480) ?v_439) (=> (and ?v_430 ?v_481) ?v_442) (=> (and ?v_430 ?v_482) ?v_442) (=> (and ?v_430 ?v_483) ?v_448) (=> (and ?v_430 ?v_484) ?v_448) (=> (and ?v_430 ?v_485) ?v_452) (=> (and ?v_430 ?v_486) ?v_452) (=> (and ?v_430 ?v_487) ?v_462) (=> (and ?v_430 ?v_489) ?v_439) (=> (and ?v_430 ?v_490) ?v_442) (=> (and ?v_430 ?v_491) ?v_442) (=> (and ?v_430 ?v_492) ?v_448) (=> (and ?v_430 ?v_493) ?v_448) (=> (and ?v_430 ?v_494) ?v_452) (=> (and ?v_430 ?v_495) ?v_452) (=> (and ?v_430 ?v_496) ?v_462) (=> (and ?v_430 ?v_497) ?v_448) (=> (and ?v_430 ?v_498) ?v_452) (=> (and ?v_430 ?v_499) ?v_452) (=> (and ?v_430 ?v_500) ?v_462) (=> (and ?v_430 ?v_501) ?v_462) (=> (and ?v_430 ?v_502) ?v_470) (=> (and ?v_430 ?v_503) ?v_470) (=> (and ?v_430 ?v_505) ?v_488) (=> (and x228 ?v_472) ?v_439) (=> (and x228 ?v_473) ?v_442) (=> (and x228 ?v_474) ?v_442) (=> (and x228 ?v_475) ?v_448) (=> (and x228 ?v_476) ?v_448) (=> (and x228 ?v_477) ?v_452) (=> (and x228 ?v_478) ?v_452) (=> (and x228 ?v_479) ?v_462) (=> (and x228 ?v_480) ?v_448) (=> (and x228 ?v_481) ?v_452) (=> (and x228 ?v_482) ?v_452) (=> (and x228 ?v_483) ?v_462) (=> (and x228 ?v_484) ?v_462) (=> (and x228 ?v_485) ?v_470) (=> (and x228 ?v_486) ?v_470) (=> (and x228 ?v_487) ?v_488) (=> (and x228 ?v_489) ?v_448) (=> (and x228 ?v_490) ?v_452) (=> (and x228 ?v_491) ?v_452) (=> (and x228 ?v_492) ?v_462) (=> (and x228 ?v_493) ?v_462) (=> (and x228 ?v_494) ?v_470) (=> (and x228 ?v_495) ?v_470) (=> (and x228 ?v_496) ?v_488) (=> (and x228 ?v_497) ?v_462) (=> (and x228 ?v_498) ?v_470) (=> (and x228 ?v_499) ?v_470) (=> (and x228 ?v_500) ?v_488) (=> (and x228 ?v_501) ?v_488) (=> (and x228 ?v_502) ?v_504) (=> (and x228 ?v_503) ?v_504) (=> (and x228 ?v_505) (= tmp70 2500)) (=> (and ?v_506 ?v_545) (= tmp69 0)) (=> (and ?v_506 ?v_546) ?v_512) (=> (and ?v_506 ?v_547) ?v_512) (=> (and ?v_506 ?v_548) ?v_516) (=> (and ?v_506 ?v_549) ?v_512) (=> (and ?v_506 ?v_550) ?v_516) (=> (and ?v_506 ?v_551) ?v_516) (=> (and ?v_506 ?v_552) ?v_523) (=> (and ?v_506 ?v_553) ?v_512) (=> (and ?v_506 ?v_554) ?v_516) (=> (and ?v_506 ?v_555) ?v_516) (=> (and ?v_506 ?v_556) ?v_523) (=> (and ?v_506 ?v_557) ?v_516) (=> (and ?v_506 ?v_558) ?v_523) (=> (and ?v_506 ?v_559) ?v_523) (=> (and ?v_506 ?v_560) ?v_536) (=> (and ?v_506 ?v_562) ?v_512) (=> (and ?v_506 ?v_563) ?v_516) (=> (and ?v_506 ?v_564) ?v_516) (=> (and ?v_506 ?v_565) ?v_523) (=> (and ?v_506 ?v_566) ?v_516) (=> (and ?v_506 ?v_567) ?v_523) (=> (and ?v_506 ?v_568) ?v_523) (=> (and ?v_506 ?v_569) ?v_536) (=> (and ?v_506 ?v_570) ?v_516) (=> (and ?v_506 ?v_571) ?v_523) (=> (and ?v_506 ?v_572) ?v_523) (=> (and ?v_506 ?v_573) ?v_536) (=> (and ?v_506 ?v_574) ?v_523) (=> (and ?v_506 ?v_575) ?v_536) (=> (and ?v_506 ?v_576) ?v_536) (=> (and ?v_506 ?v_577) ?v_561) (=> (and x189 ?v_545) ?v_512) (=> (and x189 ?v_546) ?v_516) (=> (and x189 ?v_547) ?v_516) (=> (and x189 ?v_548) ?v_523) (=> (and x189 ?v_549) ?v_516) (=> (and x189 ?v_550) ?v_523) (=> (and x189 ?v_551) ?v_523) (=> (and x189 ?v_552) ?v_536) (=> (and x189 ?v_553) ?v_516) (=> (and x189 ?v_554) ?v_523) (=> (and x189 ?v_555) ?v_523) (=> (and x189 ?v_556) ?v_536) (=> (and x189 ?v_557) ?v_523) (=> (and x189 ?v_558) ?v_536) (=> (and x189 ?v_559) ?v_536) (=> (and x189 ?v_560) ?v_561) (=> (and x189 ?v_562) ?v_516) (=> (and x189 ?v_563) ?v_523) (=> (and x189 ?v_564) ?v_523) (=> (and x189 ?v_565) ?v_536) (=> (and x189 ?v_566) ?v_523) (=> (and x189 ?v_567) ?v_536) (=> (and x189 ?v_568) ?v_536) (=> (and x189 ?v_569) ?v_561) (=> (and x189 ?v_570) ?v_523) (=> (and x189 ?v_571) ?v_536) (=> (and x189 ?v_572) ?v_536) (=> (and x189 ?v_573) ?v_561) (=> (and x189 ?v_574) ?v_536) (=> (and x189 ?v_575) ?v_561) (=> (and x189 ?v_576) ?v_561) (=> (and x189 ?v_577) (= tmp69 1200)) (=> (and ?v_578 ?v_619) (= tmp68 0)) (=> (and ?v_578 ?v_621) ?v_584) (=> (and ?v_578 ?v_622) ?v_584) (=> (and ?v_578 ?v_623) ?v_588) (=> (and ?v_578 ?v_624) ?v_584) (=> (and ?v_578 ?v_625) ?v_588) (=> (and ?v_578 ?v_626) ?v_588) (=> (and ?v_578 ?v_627) ?v_595) (=> (and ?v_578 ?v_628) ?v_584) (=> (and ?v_578 ?v_629) ?v_588) (=> (and ?v_578 ?v_630) ?v_588) (=> (and ?v_578 ?v_631) ?v_595) (=> (and ?v_578 ?v_632) ?v_588) (=> (and ?v_578 ?v_633) ?v_595) (=> (and ?v_578 ?v_634) ?v_595) (=> (and ?v_578 ?v_635) (= tmp68 2000)) (=> (and ?v_578 ?v_637) ?v_620) (=> (and ?v_578 ?v_638) ?v_603) (=> (and ?v_578 ?v_639) ?v_603) (=> (and ?v_578 ?v_641) ?v_607) (=> (and ?v_578 ?v_642) ?v_603) (=> (and ?v_578 ?v_643) ?v_607) (=> (and ?v_578 ?v_645) ?v_607) (=> (and ?v_578 ?v_646) ?v_614) (=> (and ?v_578 ?v_647) ?v_603) (=> (and ?v_578 ?v_648) ?v_607) (=> (and ?v_578 ?v_649) ?v_607) (=> (and ?v_578 ?v_650) ?v_614) (=> (and ?v_578 ?v_652) ?v_607) (=> (and ?v_578 ?v_653) ?v_614) (=> (and ?v_578 ?v_654) ?v_614) (=> (and ?v_578 ?v_655) ?v_636) (=> (and x234 ?v_619) ?v_620) (=> (and x234 ?v_621) ?v_603) (=> (and x234 ?v_622) ?v_603) (=> (and x234 ?v_623) ?v_607) (=> (and x234 ?v_624) ?v_603) (=> (and x234 ?v_625) ?v_607) (=> (and x234 ?v_626) ?v_607) (=> (and x234 ?v_627) ?v_614) (=> (and x234 ?v_628) ?v_603) (=> (and x234 ?v_629) ?v_607) (=> (and x234 ?v_630) ?v_607) (=> (and x234 ?v_631) ?v_614) (=> (and x234 ?v_632) ?v_607) (=> (and x234 ?v_633) ?v_614) (=> (and x234 ?v_634) ?v_614) (=> (and x234 ?v_635) ?v_636) (=> (and x234 ?v_637) (= tmp68 600)) (=> (and x234 ?v_638) ?v_640) (=> (and x234 ?v_639) ?v_640) (=> (and x234 ?v_641) ?v_644) (=> (and x234 ?v_642) ?v_640) (=> (and x234 ?v_643) ?v_644) (=> (and x234 ?v_645) ?v_644) (=> (and x234 ?v_646) ?v_651) (=> (and x234 ?v_647) ?v_640) (=> (and x234 ?v_648) ?v_644) (=> (and x234 ?v_649) ?v_644) (=> (and x234 ?v_650) ?v_651) (=> (and x234 ?v_652) ?v_644) (=> (and x234 ?v_653) ?v_651) (=> (and x234 ?v_654) ?v_651) (=> (and x234 ?v_655) (= tmp68 2600)) (=> (and ?v_656 ?v_697) (= tmp67 0)) (=> (and ?v_656 ?v_699) ?v_662) (=> (and ?v_656 ?v_700) ?v_662) (=> (and ?v_656 ?v_701) ?v_666) (=> (and ?v_656 ?v_702) ?v_662) (=> (and ?v_656 ?v_703) ?v_666) (=> (and ?v_656 ?v_704) ?v_666) (=> (and ?v_656 ?v_705) ?v_673) (=> (and ?v_656 ?v_706) ?v_662) (=> (and ?v_656 ?v_707) ?v_666) (=> (and ?v_656 ?v_708) ?v_666) (=> (and ?v_656 ?v_709) ?v_673) (=> (and ?v_656 ?v_710) ?v_666) (=> (and ?v_656 ?v_711) ?v_673) (=> (and ?v_656 ?v_712) ?v_673) (=> (and ?v_656 ?v_713) ?v_723) (=> (and ?v_656 ?v_715) ?v_698) (=> (and ?v_656 ?v_716) ?v_681) (=> (and ?v_656 ?v_717) ?v_681) (=> (and ?v_656 ?v_718) ?v_685) (=> (and ?v_656 ?v_719) ?v_681) (=> (and ?v_656 ?v_720) ?v_685) (=> (and ?v_656 ?v_721) ?v_685) (=> (and ?v_656 ?v_722) ?v_692) (=> (and ?v_656 ?v_724) ?v_681) (=> (and ?v_656 ?v_725) ?v_685) (=> (and ?v_656 ?v_726) ?v_685) (=> (and ?v_656 ?v_727) ?v_692) (=> (and ?v_656 ?v_728) ?v_685) (=> (and ?v_656 ?v_729) ?v_692) (=> (and ?v_656 ?v_730) ?v_692) (=> (and ?v_656 ?v_731) ?v_714) (=> (and x183 ?v_697) ?v_698) (=> (and x183 ?v_699) ?v_681) (=> (and x183 ?v_700) ?v_681) (=> (and x183 ?v_701) ?v_685) (=> (and x183 ?v_702) ?v_681) (=> (and x183 ?v_703) ?v_685) (=> (and x183 ?v_704) ?v_685) (=> (and x183 ?v_705) ?v_692) (=> (and x183 ?v_706) ?v_681) (=> (and x183 ?v_707) ?v_685) (=> (and x183 ?v_708) ?v_685) (=> (and x183 ?v_709) ?v_692) (=> (and x183 ?v_710) ?v_685) (=> (and x183 ?v_711) ?v_692) (=> (and x183 ?v_712) ?v_692) (=> (and x183 ?v_713) ?v_714) (=> (and x183 ?v_715) ?v_662) (=> (and x183 ?v_716) ?v_666) (=> (and x183 ?v_717) ?v_666) (=> (and x183 ?v_718) ?v_673) (=> (and x183 ?v_719) ?v_666) (=> (and x183 ?v_720) ?v_673) (=> (and x183 ?v_721) ?v_673) (=> (and x183 ?v_722) ?v_723) (=> (and x183 ?v_724) ?v_666) (=> (and x183 ?v_725) ?v_673) (=> (and x183 ?v_726) ?v_673) (=> (and x183 ?v_727) ?v_723) (=> (and x183 ?v_728) ?v_673) (=> (and x183 ?v_729) ?v_723) (=> (and x183 ?v_730) ?v_723) (=> (and x183 ?v_731) (= tmp67 1000)) (=> (and ?v_732 ?v_771) (= tmp66 0)) (=> (and ?v_732 ?v_772) ?v_738) (=> (and ?v_732 ?v_773) ?v_738) (=> (and ?v_732 ?v_774) ?v_742) (=> (and ?v_732 ?v_775) ?v_738) (=> (and ?v_732 ?v_776) ?v_742) (=> (and ?v_732 ?v_777) ?v_742) (=> (and ?v_732 ?v_778) ?v_749) (=> (and ?v_732 ?v_779) ?v_738) (=> (and ?v_732 ?v_780) ?v_742) (=> (and ?v_732 ?v_781) ?v_742) (=> (and ?v_732 ?v_782) ?v_749) (=> (and ?v_732 ?v_783) ?v_742) (=> (and ?v_732 ?v_784) ?v_749) (=> (and ?v_732 ?v_785) ?v_749) (=> (and ?v_732 ?v_786) ?v_762) (=> (and ?v_732 ?v_788) ?v_738) (=> (and ?v_732 ?v_789) ?v_742) (=> (and ?v_732 ?v_790) ?v_742) (=> (and ?v_732 ?v_791) ?v_749) (=> (and ?v_732 ?v_792) ?v_742) (=> (and ?v_732 ?v_793) ?v_749) (=> (and ?v_732 ?v_794) ?v_749) (=> (and ?v_732 ?v_795) ?v_762) (=> (and ?v_732 ?v_796) ?v_742) (=> (and ?v_732 ?v_797) ?v_749) (=> (and ?v_732 ?v_798) ?v_749) (=> (and ?v_732 ?v_799) ?v_762) (=> (and ?v_732 ?v_800) ?v_749) (=> (and ?v_732 ?v_801) ?v_762) (=> (and ?v_732 ?v_802) ?v_762) (=> (and ?v_732 ?v_803) ?v_787) (=> (and x240 ?v_771) ?v_738) (=> (and x240 ?v_772) ?v_742) (=> (and x240 ?v_773) ?v_742) (=> (and x240 ?v_774) ?v_749) (=> (and x240 ?v_775) ?v_742) (=> (and x240 ?v_776) ?v_749) (=> (and x240 ?v_777) ?v_749) (=> (and x240 ?v_778) ?v_762) (=> (and x240 ?v_779) ?v_742) (=> (and x240 ?v_780) ?v_749) (=> (and x240 ?v_781) ?v_749) (=> (and x240 ?v_782) ?v_762) (=> (and x240 ?v_783) ?v_749) (=> (and x240 ?v_784) ?v_762) (=> (and x240 ?v_785) ?v_762) (=> (and x240 ?v_786) ?v_787) (=> (and x240 ?v_788) ?v_742) (=> (and x240 ?v_789) ?v_749) (=> (and x240 ?v_790) ?v_749) (=> (and x240 ?v_791) ?v_762) (=> (and x240 ?v_792) ?v_749) (=> (and x240 ?v_793) ?v_762) (=> (and x240 ?v_794) ?v_762) (=> (and x240 ?v_795) ?v_787) (=> (and x240 ?v_796) ?v_749) (=> (and x240 ?v_797) ?v_762) (=> (and x240 ?v_798) ?v_762) (=> (and x240 ?v_799) ?v_787) (=> (and x240 ?v_800) ?v_762) (=> (and x240 ?v_801) ?v_787) (=> (and x240 ?v_802) ?v_787) (=> (and x240 ?v_803) (= tmp66 1800)) (=> (and ?v_804 ?v_843) (= tmp65 0)) (=> (and ?v_804 ?v_844) ?v_810) (=> (and ?v_804 ?v_845) ?v_810) (=> (and ?v_804 ?v_846) ?v_814) (=> (and ?v_804 ?v_847) ?v_810) (=> (and ?v_804 ?v_848) ?v_814) (=> (and ?v_804 ?v_849) ?v_814) (=> (and ?v_804 ?v_850) ?v_821) (=> (and ?v_804 ?v_851) ?v_810) (=> (and ?v_804 ?v_852) ?v_814) (=> (and ?v_804 ?v_853) ?v_814) (=> (and ?v_804 ?v_854) ?v_821) (=> (and ?v_804 ?v_855) ?v_814) (=> (and ?v_804 ?v_856) ?v_821) (=> (and ?v_804 ?v_857) ?v_821) (=> (and ?v_804 ?v_858) ?v_834) (=> (and ?v_804 ?v_860) ?v_810) (=> (and ?v_804 ?v_861) ?v_814) (=> (and ?v_804 ?v_862) ?v_814) (=> (and ?v_804 ?v_863) ?v_821) (=> (and ?v_804 ?v_864) ?v_814) (=> (and ?v_804 ?v_865) ?v_821) (=> (and ?v_804 ?v_866) ?v_821) (=> (and ?v_804 ?v_867) ?v_834) (=> (and ?v_804 ?v_868) ?v_814) (=> (and ?v_804 ?v_869) ?v_821) (=> (and ?v_804 ?v_870) ?v_821) (=> (and ?v_804 ?v_871) ?v_834) (=> (and ?v_804 ?v_872) ?v_821) (=> (and ?v_804 ?v_873) ?v_834) (=> (and ?v_804 ?v_874) ?v_834) (=> (and ?v_804 ?v_875) ?v_859) (=> (and x177 ?v_843) ?v_810) (=> (and x177 ?v_844) ?v_814) (=> (and x177 ?v_845) ?v_814) (=> (and x177 ?v_846) ?v_821) (=> (and x177 ?v_847) ?v_814) (=> (and x177 ?v_848) ?v_821) (=> (and x177 ?v_849) ?v_821) (=> (and x177 ?v_850) ?v_834) (=> (and x177 ?v_851) ?v_814) (=> (and x177 ?v_852) ?v_821) (=> (and x177 ?v_853) ?v_821) (=> (and x177 ?v_854) ?v_834) (=> (and x177 ?v_855) ?v_821) (=> (and x177 ?v_856) ?v_834) (=> (and x177 ?v_857) ?v_834) (=> (and x177 ?v_858) ?v_859) (=> (and x177 ?v_860) ?v_814) (=> (and x177 ?v_861) ?v_821) (=> (and x177 ?v_862) ?v_821) (=> (and x177 ?v_863) ?v_834) (=> (and x177 ?v_864) ?v_821) (=> (and x177 ?v_865) ?v_834) (=> (and x177 ?v_866) ?v_834) (=> (and x177 ?v_867) ?v_859) (=> (and x177 ?v_868) ?v_821) (=> (and x177 ?v_869) ?v_834) (=> (and x177 ?v_870) ?v_834) (=> (and x177 ?v_871) ?v_859) (=> (and x177 ?v_872) ?v_834) (=> (and x177 ?v_873) ?v_859) (=> (and x177 ?v_874) ?v_859) (=> (and x177 ?v_875) (= tmp65 600)) (=> (and ?v_732 true) (= tmp64 0)) (=> (and x240 true) (= tmp64 (- 100))) (=> (and ?v_733 true) (= tmp63 0)) (=> (and x239 true) (= tmp63 (- 100))) (=> (and ?v_734 true) (= tmp62 0)) (=> (and x238 true) (= tmp62 (- 100))) (=> (and ?v_735 true) (= tmp61 0)) (=> (and x237 true) (= tmp61 (- 100))) (=> (and ?v_736 true) (= tmp60 0)) (=> (and x236 true) (= tmp60 (- 100))) (=> ?v_737 (= tmp59 0)) (=> ?v_739 (= tmp59 (- 100))) (=> (and ?v_578 true) (= tmp58 0)) (=> (and x234 true) (= tmp58 (- 100))) (=> (and ?v_579 true) (= tmp57 0)) (=> (and x233 true) (= tmp57 (- 100))) (=> (and ?v_580 true) (= tmp56 0)) (=> (and x232 true) (= tmp56 (- 240))) (=> (and ?v_581 true) (= tmp55 0)) (=> (and x231 true) (= tmp55 (- 240))) (=> (and ?v_582 true) (= tmp54 0)) (=> (and x230 true) (= tmp54 (- 240))) (=> ?v_583 (= tmp53 0)) (=> ?v_585 (= tmp53 (- 240))) (=> (and ?v_430 true) (= tmp52 0)) (=> (and x228 true) (= tmp52 (- 240))) (=> (and ?v_431 true) (= tmp51 0)) (=> (and x227 true) (= tmp51 (- 240))) (=> (and ?v_432 true) (= tmp50 0)) (=> (and x226 true) (= tmp50 (- 240))) (=> (and ?v_433 true) (= tmp49 0)) (=> (and x225 true) (= tmp49 (- 240))) (=> (and ?v_434 true) (= tmp48 0)) (=> (and x224 true) (= tmp48 (- 400))) (=> ?v_435 (= tmp47 0)) (=> ?v_437 (= tmp47 (- 400))) (=> (and ?v_286 true) (= tmp46 0)) (=> (and x222 true) (= tmp46 (- 400))) (=> (and ?v_287 true) (= tmp45 0)) (=> (and x221 true) (= tmp45 (- 400))) (=> (and ?v_288 true) (= tmp44 0)) (=> (and x220 true) (= tmp44 (- 400))) (=> (and ?v_289 true) (= tmp43 0)) (=> (and x219 true) (= tmp43 (- 350))) (=> (and ?v_290 true) (= tmp42 0)) (=> (and x218 true) (= tmp42 (- 350))) (=> ?v_291 (= tmp41 0)) (=> ?v_293 (= tmp41 (- 350))) (=> (and ?v_142 true) (= tmp40 0)) (=> (and x216 true) (= tmp40 (- 160))) (=> (and ?v_143 true) (= tmp39 0)) (=> (and x215 true) (= tmp39 (- 160))) (=> (and ?v_144 true) (= tmp38 0)) (=> (and x214 true) (= tmp38 (- 160))) (=> (and ?v_145 true) (= tmp37 0)) (=> (and x213 true) (= tmp37 (- 160))) (=> (and ?v_146 true) (= tmp36 0)) (=> (and x212 true) (= tmp36 (- 160))) (=> ?v_147 (= tmp35 0)) (=> ?v_149 (= tmp35 (- 160))) (=> ?v_123 (= tmp34 0)) (=> ?v_125 (= tmp34 (- 160))) (=> (and ?v_122 true) (= tmp33 0)) (=> (and x209 true) (= tmp33 (- 160))) (=> (and ?v_121 true) (= tmp32 0)) (=> (and x208 true) (= tmp32 (- 500))) (=> (and ?v_120 true) (= tmp31 0)) (=> (and x207 true) (= tmp31 (- 400))) (=> ?v_219 (= tmp30 0)) (=> ?v_221 (= tmp30 (- 400))) (=> (and ?v_218 true) (= tmp29 0)) (=> (and x205 true) (= tmp29 (- 400))) (=> (and ?v_217 true) (= tmp28 0)) (=> (and x204 true) (= tmp28 (- 400))) (=> (and ?v_216 true) (= tmp27 0)) (=> (and x203 true) (= tmp27 (- 350))) (=> (and ?v_215 true) (= tmp26 0)) (=> (and x202 true) (= tmp26 (- 350))) (=> (and ?v_214 true) (= tmp25 0)) (=> (and x201 true) (= tmp25 (- 350))) (=> ?v_363 (= tmp24 0)) (=> ?v_365 (= tmp24 (- 500))) (=> (and ?v_362 true) (= tmp23 0)) (=> (and x199 true) (= tmp23 (- 400))) (=> (and ?v_361 true) (= tmp22 0)) (=> (and x198 true) (= tmp22 (- 400))) (=> (and ?v_360 true) (= tmp21 0)) (=> (and x197 true) (= tmp21 (- 400))) (=> (and ?v_359 true) (= tmp20 0)) (=> (and x196 true) (= tmp20 (- 400))) (=> (and ?v_358 true) (= tmp19 0)) (=> (and x195 true) (= tmp19 (- 350))) (=> ?v_511 (= tmp18 0)) (=> ?v_513 (= tmp18 (- 350))) (=> (and ?v_510 true) (= tmp17 0)) (=> (and x193 true) (= tmp17 (- 350))) (=> (and ?v_509 true) (= tmp16 0)) (=> (and x192 true) (= tmp16 (- 240))) (=> (and ?v_508 true) (= tmp15 0)) (=> (and x191 true) (= tmp15 (- 240))) (=> (and ?v_507 true) (= tmp14 0)) (=> (and x190 true) (= tmp14 (- 240))) (=> (and ?v_506 true) (= tmp13 0)) (=> (and x189 true) (= tmp13 (- 240))) (=> ?v_661 (= tmp12 0)) (=> ?v_663 (= tmp12 (- 240))) (=> (and ?v_660 true) (= tmp11 0)) (=> (and x187 true) (= tmp11 (- 240))) (=> (and ?v_659 true) (= tmp10 0)) (=> (and x186 true) (= tmp10 (- 240))) (=> (and ?v_658 true) (= tmp9 0)) (=> (and x185 true) (= tmp9 (- 240))) (=> (and ?v_657 true) (= tmp8 0)) (=> (and x184 true) (= tmp8 (- 420))) (=> (and ?v_656 true) (= tmp7 0)) (=> (and x183 true) (= tmp7 (- 400))) (=> ?v_809 (= tmp6 0)) (=> ?v_811 (= tmp6 (- 400))) (=> (and ?v_808 true) (= tmp5 0)) (=> (and x181 true) (= tmp5 (- 400))) (=> (and ?v_807 true) (= tmp4 0)) (=> (and x180 true) (= tmp4 (- 400))) (=> (and ?v_806 true) (= tmp3 0)) (=> (and x179 true) (= tmp3 (- 350))) (=> (and ?v_805 true) (= tmp2 0)) (=> (and x178 true) (= tmp2 (- 350))) (=> (and ?v_804 true) (= tmp1 0)) (=> (and x177 true) (= tmp1 (- 350))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)