From 0841e0e7670901e866070194f6be8f4aba427c33 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 25 Jun 2023 15:39:28 -0400 Subject: [PATCH] add another bug repro --- tests/sat/Carpark2-ausgabe-8-reduced.smt2 | 3 + tests/sat/Carpark2-ausgabe-8.smt2 | 368 ++++++++++++++++++++++ 2 files changed, 371 insertions(+) create mode 100644 tests/sat/Carpark2-ausgabe-8-reduced.smt2 create mode 100644 tests/sat/Carpark2-ausgabe-8.smt2 diff --git a/tests/sat/Carpark2-ausgabe-8-reduced.smt2 b/tests/sat/Carpark2-ausgabe-8-reduced.smt2 new file mode 100644 index 00000000..8890d00f --- /dev/null +++ b/tests/sat/Carpark2-ausgabe-8-reduced.smt2 @@ -0,0 +1,3 @@ +(declare-fun _9 () Real) +(assert (= 0.0 (+ _9 1))) +(check-sat) diff --git a/tests/sat/Carpark2-ausgabe-8.smt2 b/tests/sat/Carpark2-ausgabe-8.smt2 new file mode 100644 index 00000000..f1b7c724 --- /dev/null +++ b/tests/sat/Carpark2-ausgabe-8.smt2 @@ -0,0 +1,368 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_LRA) +(set-info :source | +SAL benchmark suite. Created at SRI by Bruno Dutertre, John Rushby, Maria +Sorea, and Leonardo de Moura. Contact demoura@csl.sri.com for more +information. + +This benchmark was automatically translated into SMT-LIB format from +CVC format using CVC Lite +|) +(set-info :category "industrial") +(set-info :status sat) +(declare-fun x_0 () Bool) +(declare-fun x_1 () Bool) +(declare-fun x_2 () Bool) +(declare-fun x_3 () Bool) +(declare-fun x_4 () Bool) +(declare-fun x_5 () Bool) +(declare-fun x_6 () Bool) +(declare-fun x_7 () Bool) +(declare-fun x_8 () Bool) +(declare-fun x_9 () Real) +(declare-fun x_10 () Real) +(declare-fun x_11 () Bool) +(declare-fun x_12 () Real) +(declare-fun x_13 () Real) +(declare-fun x_14 () Real) +(declare-fun x_15 () Bool) +(declare-fun x_16 () Bool) +(declare-fun x_17 () Bool) +(declare-fun x_18 () Bool) +(declare-fun x_19 () Real) +(declare-fun x_20 () Bool) +(declare-fun x_21 () Real) +(declare-fun x_22 () Real) +(declare-fun x_23 () Bool) +(declare-fun x_24 () Bool) +(declare-fun x_25 () Bool) +(declare-fun x_26 () Real) +(declare-fun x_27 () Bool) +(declare-fun x_28 () Real) +(declare-fun x_29 () Real) +(declare-fun x_30 () Real) +(declare-fun x_31 () Bool) +(declare-fun x_32 () Bool) +(declare-fun x_33 () Bool) +(declare-fun x_34 () Real) +(declare-fun x_35 () Bool) +(declare-fun x_36 () Bool) +(declare-fun x_37 () Real) +(declare-fun x_38 () Real) +(declare-fun x_39 () Real) +(declare-fun x_40 () Bool) +(declare-fun x_41 () Real) +(declare-fun x_42 () Bool) +(declare-fun x_43 () Bool) +(declare-fun x_44 () Real) +(declare-fun x_45 () Bool) +(declare-fun x_46 () Real) +(declare-fun x_47 () Bool) +(declare-fun x_48 () Real) +(declare-fun x_49 () Bool) +(declare-fun x_50 () Real) +(declare-fun x_51 () Bool) +(declare-fun x_52 () Bool) +(declare-fun x_53 () Bool) +(declare-fun x_54 () Bool) +(declare-fun x_55 () Bool) +(declare-fun x_56 () Bool) +(declare-fun x_57 () Bool) +(declare-fun x_58 () Bool) +(declare-fun x_59 () Real) +(declare-fun x_60 () Real) +(declare-fun x_61 () Bool) +(declare-fun x_62 () Bool) +(declare-fun x_63 () Bool) +(declare-fun x_64 () Bool) +(declare-fun x_65 () Bool) +(declare-fun x_66 () Real) +(declare-fun x_67 () Real) +(declare-fun x_68 () Bool) +(declare-fun x_69 () Real) +(declare-fun x_70 () Real) +(declare-fun x_71 () Bool) +(declare-fun x_72 () Real) +(declare-fun x_73 () Bool) +(declare-fun x_74 () Real) +(declare-fun x_75 () Bool) +(declare-fun x_76 () Bool) +(declare-fun x_77 () Real) +(declare-fun x_78 () Real) +(declare-fun x_79 () Real) +(declare-fun x_80 () Bool) +(declare-fun x_81 () Real) +(declare-fun x_82 () Bool) +(declare-fun x_83 () Bool) +(declare-fun x_84 () Real) +(declare-fun x_85 () Bool) +(declare-fun x_86 () Real) +(declare-fun x_87 () Bool) +(declare-fun x_88 () Real) +(declare-fun x_89 () Bool) +(declare-fun x_90 () Real) +(declare-fun x_91 () Bool) +(declare-fun x_92 () Bool) +(declare-fun x_93 () Bool) +(declare-fun x_94 () Bool) +(declare-fun x_95 () Bool) +(declare-fun x_96 () Bool) +(declare-fun x_97 () Bool) +(declare-fun x_98 () Bool) +(declare-fun x_99 () Real) +(declare-fun x_100 () Real) +(declare-fun x_101 () Bool) +(declare-fun x_102 () Bool) +(declare-fun x_103 () Bool) +(declare-fun x_104 () Bool) +(declare-fun x_105 () Bool) +(declare-fun x_106 () Real) +(declare-fun x_107 () Real) +(declare-fun x_108 () Bool) +(declare-fun x_109 () Real) +(declare-fun x_110 () Real) +(declare-fun x_111 () Bool) +(declare-fun x_112 () Real) +(declare-fun x_113 () Bool) +(declare-fun x_114 () Real) +(declare-fun x_115 () Bool) +(declare-fun x_116 () Bool) +(declare-fun x_117 () Real) +(declare-fun x_118 () Real) +(declare-fun x_119 () Real) +(declare-fun x_120 () Bool) +(declare-fun x_121 () Real) +(declare-fun x_122 () Bool) +(declare-fun x_123 () Bool) +(declare-fun x_124 () Real) +(declare-fun x_125 () Bool) +(declare-fun x_126 () Real) +(declare-fun x_127 () Bool) +(declare-fun x_128 () Real) +(declare-fun x_129 () Bool) +(declare-fun x_130 () Real) +(declare-fun x_131 () Bool) +(declare-fun x_132 () Bool) +(declare-fun x_133 () Bool) +(declare-fun x_134 () Bool) +(declare-fun x_135 () Bool) +(declare-fun x_136 () Bool) +(declare-fun x_137 () Bool) +(declare-fun x_138 () Bool) +(declare-fun x_139 () Real) +(declare-fun x_140 () Real) +(declare-fun x_141 () Bool) +(declare-fun x_142 () Bool) +(declare-fun x_143 () Bool) +(declare-fun x_144 () Bool) +(declare-fun x_145 () Bool) +(declare-fun x_146 () Real) +(declare-fun x_147 () Real) +(declare-fun x_148 () Bool) +(declare-fun x_149 () Real) +(declare-fun x_150 () Real) +(declare-fun x_151 () Bool) +(declare-fun x_152 () Real) +(declare-fun x_153 () Bool) +(declare-fun x_154 () Real) +(declare-fun x_155 () Bool) +(declare-fun x_156 () Bool) +(declare-fun x_157 () Real) +(declare-fun x_158 () Real) +(declare-fun x_159 () Real) +(declare-fun x_160 () Bool) +(declare-fun x_161 () Real) +(declare-fun x_162 () Bool) +(declare-fun x_163 () Bool) +(declare-fun x_164 () Real) +(declare-fun x_165 () Bool) +(declare-fun x_166 () Real) +(declare-fun x_167 () Bool) +(declare-fun x_168 () Real) +(declare-fun x_169 () Bool) +(declare-fun x_170 () Real) +(declare-fun x_171 () Bool) +(declare-fun x_172 () Bool) +(declare-fun x_173 () Bool) +(declare-fun x_174 () Bool) +(declare-fun x_175 () Bool) +(declare-fun x_176 () Bool) +(declare-fun x_177 () Bool) +(declare-fun x_178 () Bool) +(declare-fun x_179 () Real) +(declare-fun x_180 () Real) +(declare-fun x_181 () Bool) +(declare-fun x_182 () Bool) +(declare-fun x_183 () Bool) +(declare-fun x_184 () Bool) +(declare-fun x_185 () Bool) +(declare-fun x_186 () Real) +(declare-fun x_187 () Real) +(declare-fun x_188 () Bool) +(declare-fun x_189 () Real) +(declare-fun x_190 () Real) +(declare-fun x_191 () Bool) +(declare-fun x_192 () Real) +(declare-fun x_193 () Bool) +(declare-fun x_194 () Real) +(declare-fun x_195 () Bool) +(declare-fun x_196 () Bool) +(declare-fun x_197 () Real) +(declare-fun x_198 () Real) +(declare-fun x_199 () Real) +(declare-fun x_200 () Bool) +(declare-fun x_201 () Real) +(declare-fun x_202 () Bool) +(declare-fun x_203 () Bool) +(declare-fun x_204 () Real) +(declare-fun x_205 () Bool) +(declare-fun x_206 () Real) +(declare-fun x_207 () Bool) +(declare-fun x_208 () Real) +(declare-fun x_209 () Bool) +(declare-fun x_210 () Real) +(declare-fun x_211 () Bool) +(declare-fun x_212 () Bool) +(declare-fun x_213 () Bool) +(declare-fun x_214 () Bool) +(declare-fun x_215 () Bool) +(declare-fun x_216 () Bool) +(declare-fun x_217 () Bool) +(declare-fun x_218 () Bool) +(declare-fun x_219 () Real) +(declare-fun x_220 () Real) +(declare-fun x_221 () Bool) +(declare-fun x_222 () Bool) +(declare-fun x_223 () Bool) +(declare-fun x_224 () Bool) +(declare-fun x_225 () Bool) +(declare-fun x_226 () Real) +(declare-fun x_227 () Real) +(declare-fun x_228 () Bool) +(declare-fun x_229 () Real) +(declare-fun x_230 () Real) +(declare-fun x_231 () Bool) +(declare-fun x_232 () Real) +(declare-fun x_233 () Bool) +(declare-fun x_234 () Real) +(declare-fun x_235 () Bool) +(declare-fun x_236 () Bool) +(declare-fun x_237 () Real) +(declare-fun x_238 () Real) +(declare-fun x_239 () Real) +(declare-fun x_240 () Bool) +(declare-fun x_241 () Real) +(declare-fun x_242 () Bool) +(declare-fun x_243 () Bool) +(declare-fun x_244 () Real) +(declare-fun x_245 () Bool) +(declare-fun x_246 () Real) +(declare-fun x_247 () Bool) +(declare-fun x_248 () Real) +(declare-fun x_249 () Bool) +(declare-fun x_250 () Real) +(declare-fun x_251 () Bool) +(declare-fun x_252 () Bool) +(declare-fun x_253 () Bool) +(declare-fun x_254 () Bool) +(declare-fun x_255 () Bool) +(declare-fun x_256 () Bool) +(declare-fun x_257 () Bool) +(declare-fun x_258 () Bool) +(declare-fun x_259 () Real) +(declare-fun x_260 () Real) +(declare-fun x_261 () Bool) +(declare-fun x_262 () Bool) +(declare-fun x_263 () Bool) +(declare-fun x_264 () Bool) +(declare-fun x_265 () Bool) +(declare-fun x_266 () Real) +(declare-fun x_267 () Real) +(declare-fun x_268 () Bool) +(declare-fun x_269 () Real) +(declare-fun x_270 () Real) +(declare-fun x_271 () Bool) +(declare-fun x_272 () Real) +(declare-fun x_273 () Bool) +(declare-fun x_274 () Real) +(declare-fun x_275 () Bool) +(declare-fun x_276 () Bool) +(declare-fun x_277 () Real) +(declare-fun x_278 () Real) +(declare-fun x_279 () Real) +(declare-fun x_280 () Bool) +(declare-fun x_281 () Real) +(declare-fun x_282 () Bool) +(declare-fun x_283 () Bool) +(declare-fun x_284 () Real) +(declare-fun x_285 () Bool) +(declare-fun x_286 () Real) +(declare-fun x_287 () Bool) +(declare-fun x_288 () Real) +(declare-fun x_289 () Bool) +(declare-fun x_290 () Real) +(declare-fun x_291 () Bool) +(declare-fun x_292 () Bool) +(declare-fun x_293 () Bool) +(declare-fun x_294 () Bool) +(declare-fun x_295 () Bool) +(declare-fun x_296 () Bool) +(declare-fun x_297 () Bool) +(declare-fun x_298 () Bool) +(declare-fun x_299 () Real) +(declare-fun x_300 () Real) +(declare-fun x_301 () Bool) +(declare-fun x_302 () Bool) +(declare-fun x_303 () Bool) +(declare-fun x_304 () Bool) +(declare-fun x_305 () Bool) +(declare-fun x_306 () Real) +(declare-fun x_307 () Real) +(declare-fun x_308 () Bool) +(declare-fun x_309 () Real) +(declare-fun x_310 () Real) +(declare-fun x_311 () Bool) +(declare-fun x_312 () Real) +(declare-fun x_313 () Bool) +(declare-fun x_314 () Real) +(declare-fun x_315 () Bool) +(declare-fun x_316 () Bool) +(declare-fun x_317 () Real) +(declare-fun x_318 () Real) +(declare-fun x_319 () Real) +(declare-fun x_320 () Bool) +(declare-fun x_321 () Real) +(declare-fun x_322 () Bool) +(declare-fun x_323 () Bool) +(declare-fun x_324 () Real) +(declare-fun x_325 () Bool) +(declare-fun x_326 () Real) +(declare-fun x_327 () Bool) +(declare-fun x_328 () Real) +(declare-fun x_329 () Bool) +(declare-fun x_330 () Real) +(declare-fun x_331 () Bool) +(declare-fun x_332 () Bool) +(declare-fun x_333 () Bool) +(declare-fun x_334 () Bool) +(declare-fun x_335 () Bool) +(declare-fun x_336 () Bool) +(declare-fun x_337 () Bool) +(declare-fun x_338 () Bool) +(declare-fun x_339 () Real) +(declare-fun x_340 () Real) +(declare-fun x_341 () Bool) +(declare-fun x_342 () Bool) +(declare-fun x_343 () Bool) +(declare-fun x_344 () Bool) +(declare-fun x_345 () Bool) +(declare-fun x_346 () Real) +(declare-fun x_347 () Real) +(declare-fun x_348 () Bool) +(declare-fun x_349 () Real) +(declare-fun x_350 () Real) +(declare-fun x_351 () Bool) +(declare-fun x_352 () Real) +(assert (let ((?v_25 (< x_288 x_300)) (?v_62 (<= x_278 x_277)) (?v_32 (< x_284 50)) (?v_34 (< x_284 20)) (?v_55 (= x_314 x_10))) (let ((?v_60 (and (= x_313 false) ?v_55)) (?v_31 (and x_315 x_316)) (?v_66 (= x_317 x_277)) (?v_65 (= x_318 x_278)) (?v_45 (not x_292))) (let ((?v_49 (and x_291 ?v_45)) (?v_51 (= x_319 x_279)) (?v_29 (and (= x_320 false) (= x_321 x_10))) (?v_19 (not x_275))) (let ((?v_24 (and ?v_19 x_276)) (?v_63 (not x_323))) (let ((?v_68 (and x_322 ?v_63)) (?v_18 (= x_324 x_284)) (?v_30 (and x_275 x_276)) (?v_69 (or x_282 x_283)) (?v_0 (not x_276))) (let ((?v_39 (or x_275 ?v_0)) (?v_43 (< x_284 10)) (?v_40 (<= x_284 0)) (?v_50 (and (= x_325 false) (= x_326 x_10))) (?v_47 (= x_327 false)) (?v_23 (= x_328 x_288)) (?v_48 (and (= x_329 false) (= x_330 x_10))) (?v_54 (not x_332))) (let ((?v_46 (and x_331 ?v_54)) (?v_41 (or ?v_19 ?v_0)) (?v_52 (not x_291))) (let ((?v_56 (or ?v_52 x_292)) (?v_8 (and (and (and (= x_333 false) (= x_334 x_5)) (= x_335 x_6)) (= x_336 x_7))) (?v_9 (= x_337 false)) (?v_64 (and (= x_338 false) (= x_339 x_10))) (?v_22 (= x_340 x_300)) (?v_67 (not x_282)) (?v_58 (not x_283))) (let ((?v_61 (and ?v_67 ?v_58)) (?v_26 (= x_341 false)) (?v_28 (not x_316))) (let ((?v_20 (and x_315 ?v_28)) (?v_2 (not x_343))) (let ((?v_4 (and x_342 ?v_2)) (?v_3 (not x_344))) (let ((?v_10 (and (and ?v_4 ?v_3) x_345)) (?v_5 (or x_342 x_343)) (?v_1 (not x_345)) (?v_6 (and x_342 x_343))) (let ((?v_11 (and (and ?v_6 x_344) ?v_1)) (?v_7 (or x_342 ?v_2)) (?v_13 (and (and ?v_4 x_344) ?v_1)) (?v_15 (and (and ?v_6 ?v_3) ?v_1))) (let ((?v_37 (or ?v_10 (and (or (or ?v_5 x_344) ?v_1) (or ?v_11 (and (or (or ?v_7 ?v_3) x_345) (or ?v_13 (and (or (or ?v_5 ?v_3) x_345) (or ?v_15 (and (and (and (and (or (or ?v_7 x_344) x_345) x_342) ?v_2) ?v_3) ?v_1))))))))) (?v_42 (not ?v_32)) (?v_70 (not ?v_62)) (?v_38 (not ?v_25)) (?v_21 (= x_341 true)) (?v_44 (not ?v_34)) (?v_96 (< x_248 x_260)) (?v_126 (<= x_238 x_237)) (?v_100 (< x_244 50)) (?v_102 (< x_244 20)) (?v_120 (= x_274 x_10))) (let ((?v_124 (and (= x_273 false) ?v_120)) (?v_129 (= x_277 x_237)) (?v_128 (= x_278 x_238)) (?v_113 (not x_252))) (let ((?v_116 (and x_251 ?v_113)) (?v_118 (= x_279 x_239)) (?v_98 (and (= x_280 false) (= x_281 x_10))) (?v_90 (not x_235))) (let ((?v_95 (and ?v_90 x_236)) (?v_131 (and x_282 ?v_58)) (?v_89 (= x_284 x_244)) (?v_99 (and x_235 x_236)) (?v_132 (or x_242 x_243)) (?v_71 (not x_236))) (let ((?v_107 (or x_235 ?v_71)) (?v_111 (< x_244 10)) (?v_108 (<= x_244 0)) (?v_117 (and (= x_285 false) (= x_286 x_10))) (?v_114 (= x_287 false)) (?v_94 (= x_288 x_248)) (?v_115 (and (= x_289 false) (= x_290 x_10))) (?v_109 (or ?v_90 ?v_71)) (?v_119 (not x_251))) (let ((?v_121 (or ?v_119 x_252)) (?v_79 (and (and (and (= x_293 false) (= x_294 x_5)) (= x_295 x_6)) (= x_296 x_7))) (?v_80 (= x_297 false)) (?v_127 (and (= x_298 false) (= x_299 x_10))) (?v_93 (= x_300 x_260)) (?v_130 (not x_242)) (?v_123 (not x_243))) (let ((?v_125 (and ?v_130 ?v_123)) (?v_97 (= x_301 false)) (?v_91 (and x_275 ?v_0)) (?v_73 (not x_303))) (let ((?v_75 (and x_302 ?v_73)) (?v_74 (not x_304))) (let ((?v_81 (and (and ?v_75 ?v_74) x_305)) (?v_76 (or x_302 x_303)) (?v_72 (not x_305)) (?v_77 (and x_302 x_303))) (let ((?v_82 (and (and ?v_77 x_304) ?v_72)) (?v_78 (or x_302 ?v_73)) (?v_84 (and (and ?v_75 x_304) ?v_72)) (?v_86 (and (and ?v_77 ?v_74) ?v_72))) (let ((?v_105 (or ?v_81 (and (or (or ?v_76 x_304) ?v_72) (or ?v_82 (and (or (or ?v_78 ?v_74) x_305) (or ?v_84 (and (or (or ?v_76 ?v_74) x_305) (or ?v_86 (and (and (and (and (or (or ?v_78 x_304) x_305) x_302) ?v_73) ?v_74) ?v_72))))))))) (?v_110 (not ?v_100)) (?v_133 (not ?v_126)) (?v_106 (not ?v_96)) (?v_92 (= x_301 true)) (?v_112 (not ?v_102)) (?v_159 (< x_208 x_220)) (?v_189 (<= x_198 x_197)) (?v_163 (< x_204 50)) (?v_165 (< x_204 20)) (?v_183 (= x_234 x_10))) (let ((?v_187 (and (= x_233 false) ?v_183)) (?v_192 (= x_237 x_197)) (?v_191 (= x_238 x_198)) (?v_176 (not x_212))) (let ((?v_179 (and x_211 ?v_176)) (?v_181 (= x_239 x_199)) (?v_161 (and (= x_240 false) (= x_241 x_10))) (?v_153 (not x_195))) (let ((?v_158 (and ?v_153 x_196)) (?v_194 (and x_242 ?v_123)) (?v_152 (= x_244 x_204)) (?v_162 (and x_195 x_196)) (?v_195 (or x_202 x_203)) (?v_134 (not x_196))) (let ((?v_170 (or x_195 ?v_134)) (?v_174 (< x_204 10)) (?v_171 (<= x_204 0)) (?v_180 (and (= x_245 false) (= x_246 x_10))) (?v_177 (= x_247 false)) (?v_157 (= x_248 x_208)) (?v_178 (and (= x_249 false) (= x_250 x_10))) (?v_172 (or ?v_153 ?v_134)) (?v_182 (not x_211))) (let ((?v_184 (or ?v_182 x_212)) (?v_142 (and (and (and (= x_253 false) (= x_254 x_5)) (= x_255 x_6)) (= x_256 x_7))) (?v_143 (= x_257 false)) (?v_190 (and (= x_258 false) (= x_259 x_10))) (?v_156 (= x_260 x_220)) (?v_193 (not x_202)) (?v_186 (not x_203))) (let ((?v_188 (and ?v_193 ?v_186)) (?v_160 (= x_261 false)) (?v_154 (and x_235 ?v_71)) (?v_136 (not x_263))) (let ((?v_138 (and x_262 ?v_136)) (?v_137 (not x_264))) (let ((?v_144 (and (and ?v_138 ?v_137) x_265)) (?v_139 (or x_262 x_263)) (?v_135 (not x_265)) (?v_140 (and x_262 x_263))) (let ((?v_145 (and (and ?v_140 x_264) ?v_135)) (?v_141 (or x_262 ?v_136)) (?v_147 (and (and ?v_138 x_264) ?v_135)) (?v_149 (and (and ?v_140 ?v_137) ?v_135))) (let ((?v_168 (or ?v_144 (and (or (or ?v_139 x_264) ?v_135) (or ?v_145 (and (or (or ?v_141 ?v_137) x_265) (or ?v_147 (and (or (or ?v_139 ?v_137) x_265) (or ?v_149 (and (and (and (and (or (or ?v_141 x_264) x_265) x_262) ?v_136) ?v_137) ?v_135))))))))) (?v_173 (not ?v_163)) (?v_196 (not ?v_189)) (?v_169 (not ?v_159)) (?v_155 (= x_261 true)) (?v_175 (not ?v_165)) (?v_222 (< x_168 x_180)) (?v_252 (<= x_158 x_157)) (?v_226 (< x_164 50)) (?v_228 (< x_164 20)) (?v_246 (= x_194 x_10))) (let ((?v_250 (and (= x_193 false) ?v_246)) (?v_255 (= x_197 x_157)) (?v_254 (= x_198 x_158)) (?v_239 (not x_172))) (let ((?v_242 (and x_171 ?v_239)) (?v_244 (= x_199 x_159)) (?v_224 (and (= x_200 false) (= x_201 x_10))) (?v_216 (not x_155))) (let ((?v_221 (and ?v_216 x_156)) (?v_257 (and x_202 ?v_186)) (?v_215 (= x_204 x_164)) (?v_225 (and x_155 x_156)) (?v_258 (or x_162 x_163)) (?v_197 (not x_156))) (let ((?v_233 (or x_155 ?v_197)) (?v_237 (< x_164 10)) (?v_234 (<= x_164 0)) (?v_243 (and (= x_205 false) (= x_206 x_10))) (?v_240 (= x_207 false)) (?v_220 (= x_208 x_168)) (?v_241 (and (= x_209 false) (= x_210 x_10))) (?v_235 (or ?v_216 ?v_197)) (?v_245 (not x_171))) (let ((?v_247 (or ?v_245 x_172)) (?v_205 (and (and (and (= x_213 false) (= x_214 x_5)) (= x_215 x_6)) (= x_216 x_7))) (?v_206 (= x_217 false)) (?v_253 (and (= x_218 false) (= x_219 x_10))) (?v_219 (= x_220 x_180)) (?v_256 (not x_162)) (?v_249 (not x_163))) (let ((?v_251 (and ?v_256 ?v_249)) (?v_223 (= x_221 false)) (?v_217 (and x_195 ?v_134)) (?v_199 (not x_223))) (let ((?v_201 (and x_222 ?v_199)) (?v_200 (not x_224))) (let ((?v_207 (and (and ?v_201 ?v_200) x_225)) (?v_202 (or x_222 x_223)) (?v_198 (not x_225)) (?v_203 (and x_222 x_223))) (let ((?v_208 (and (and ?v_203 x_224) ?v_198)) (?v_204 (or x_222 ?v_199)) (?v_210 (and (and ?v_201 x_224) ?v_198)) (?v_212 (and (and ?v_203 ?v_200) ?v_198))) (let ((?v_231 (or ?v_207 (and (or (or ?v_202 x_224) ?v_198) (or ?v_208 (and (or (or ?v_204 ?v_200) x_225) (or ?v_210 (and (or (or ?v_202 ?v_200) x_225) (or ?v_212 (and (and (and (and (or (or ?v_204 x_224) x_225) x_222) ?v_199) ?v_200) ?v_198))))))))) (?v_236 (not ?v_226)) (?v_259 (not ?v_252)) (?v_232 (not ?v_222)) (?v_218 (= x_221 true)) (?v_238 (not ?v_228)) (?v_285 (< x_128 x_140)) (?v_315 (<= x_118 x_117)) (?v_289 (< x_124 50)) (?v_291 (< x_124 20)) (?v_309 (= x_154 x_10))) (let ((?v_313 (and (= x_153 false) ?v_309)) (?v_318 (= x_157 x_117)) (?v_317 (= x_158 x_118)) (?v_302 (not x_132))) (let ((?v_305 (and x_131 ?v_302)) (?v_307 (= x_159 x_119)) (?v_287 (and (= x_160 false) (= x_161 x_10))) (?v_279 (not x_115))) (let ((?v_284 (and ?v_279 x_116)) (?v_320 (and x_162 ?v_249)) (?v_278 (= x_164 x_124)) (?v_288 (and x_115 x_116)) (?v_321 (or x_122 x_123)) (?v_260 (not x_116))) (let ((?v_296 (or x_115 ?v_260)) (?v_300 (< x_124 10)) (?v_297 (<= x_124 0)) (?v_306 (and (= x_165 false) (= x_166 x_10))) (?v_303 (= x_167 false)) (?v_283 (= x_168 x_128)) (?v_304 (and (= x_169 false) (= x_170 x_10))) (?v_298 (or ?v_279 ?v_260)) (?v_308 (not x_131))) (let ((?v_310 (or ?v_308 x_132)) (?v_268 (and (and (and (= x_173 false) (= x_174 x_5)) (= x_175 x_6)) (= x_176 x_7))) (?v_269 (= x_177 false)) (?v_316 (and (= x_178 false) (= x_179 x_10))) (?v_282 (= x_180 x_140)) (?v_319 (not x_122)) (?v_312 (not x_123))) (let ((?v_314 (and ?v_319 ?v_312)) (?v_286 (= x_181 false)) (?v_280 (and x_155 ?v_197)) (?v_262 (not x_183))) (let ((?v_264 (and x_182 ?v_262)) (?v_263 (not x_184))) (let ((?v_270 (and (and ?v_264 ?v_263) x_185)) (?v_265 (or x_182 x_183)) (?v_261 (not x_185)) (?v_266 (and x_182 x_183))) (let ((?v_271 (and (and ?v_266 x_184) ?v_261)) (?v_267 (or x_182 ?v_262)) (?v_273 (and (and ?v_264 x_184) ?v_261)) (?v_275 (and (and ?v_266 ?v_263) ?v_261))) (let ((?v_294 (or ?v_270 (and (or (or ?v_265 x_184) ?v_261) (or ?v_271 (and (or (or ?v_267 ?v_263) x_185) (or ?v_273 (and (or (or ?v_265 ?v_263) x_185) (or ?v_275 (and (and (and (and (or (or ?v_267 x_184) x_185) x_182) ?v_262) ?v_263) ?v_261))))))))) (?v_299 (not ?v_289)) (?v_322 (not ?v_315)) (?v_295 (not ?v_285)) (?v_281 (= x_181 true)) (?v_301 (not ?v_291)) (?v_348 (< x_88 x_100)) (?v_378 (<= x_78 x_77)) (?v_352 (< x_84 50)) (?v_354 (< x_84 20)) (?v_372 (= x_114 x_10))) (let ((?v_376 (and (= x_113 false) ?v_372)) (?v_381 (= x_117 x_77)) (?v_380 (= x_118 x_78)) (?v_365 (not x_92))) (let ((?v_368 (and x_91 ?v_365)) (?v_370 (= x_119 x_79)) (?v_350 (and (= x_120 false) (= x_121 x_10))) (?v_342 (not x_75))) (let ((?v_347 (and ?v_342 x_76)) (?v_383 (and x_122 ?v_312)) (?v_341 (= x_124 x_84)) (?v_351 (and x_75 x_76)) (?v_384 (or x_82 x_83)) (?v_323 (not x_76))) (let ((?v_359 (or x_75 ?v_323)) (?v_363 (< x_84 10)) (?v_360 (<= x_84 0)) (?v_369 (and (= x_125 false) (= x_126 x_10))) (?v_366 (= x_127 false)) (?v_346 (= x_128 x_88)) (?v_367 (and (= x_129 false) (= x_130 x_10))) (?v_361 (or ?v_342 ?v_323)) (?v_371 (not x_91))) (let ((?v_373 (or ?v_371 x_92)) (?v_331 (and (and (and (= x_133 false) (= x_134 x_5)) (= x_135 x_6)) (= x_136 x_7))) (?v_332 (= x_137 false)) (?v_379 (and (= x_138 false) (= x_139 x_10))) (?v_345 (= x_140 x_100)) (?v_382 (not x_82)) (?v_375 (not x_83))) (let ((?v_377 (and ?v_382 ?v_375)) (?v_349 (= x_141 false)) (?v_343 (and x_115 ?v_260)) (?v_325 (not x_143))) (let ((?v_327 (and x_142 ?v_325)) (?v_326 (not x_144))) (let ((?v_333 (and (and ?v_327 ?v_326) x_145)) (?v_328 (or x_142 x_143)) (?v_324 (not x_145)) (?v_329 (and x_142 x_143))) (let ((?v_334 (and (and ?v_329 x_144) ?v_324)) (?v_330 (or x_142 ?v_325)) (?v_336 (and (and ?v_327 x_144) ?v_324)) (?v_338 (and (and ?v_329 ?v_326) ?v_324))) (let ((?v_357 (or ?v_333 (and (or (or ?v_328 x_144) ?v_324) (or ?v_334 (and (or (or ?v_330 ?v_326) x_145) (or ?v_336 (and (or (or ?v_328 ?v_326) x_145) (or ?v_338 (and (and (and (and (or (or ?v_330 x_144) x_145) x_142) ?v_325) ?v_326) ?v_324))))))))) (?v_362 (not ?v_352)) (?v_385 (not ?v_378)) (?v_358 (not ?v_348)) (?v_344 (= x_141 true)) (?v_364 (not ?v_354)) (?v_411 (< x_48 x_60)) (?v_441 (<= x_38 x_37)) (?v_415 (< x_44 50)) (?v_417 (< x_44 20)) (?v_435 (= x_74 x_10))) (let ((?v_439 (and (= x_73 false) ?v_435)) (?v_444 (= x_77 x_37)) (?v_443 (= x_78 x_38)) (?v_428 (not x_52))) (let ((?v_431 (and x_51 ?v_428)) (?v_433 (= x_79 x_39)) (?v_413 (and (= x_80 false) (= x_81 x_10))) (?v_405 (not x_35))) (let ((?v_410 (and ?v_405 x_36)) (?v_446 (and x_82 ?v_375)) (?v_404 (= x_84 x_44)) (?v_414 (and x_35 x_36)) (?v_447 (or x_42 x_43)) (?v_386 (not x_36))) (let ((?v_422 (or x_35 ?v_386)) (?v_426 (< x_44 10)) (?v_423 (<= x_44 0)) (?v_432 (and (= x_85 false) (= x_86 x_10))) (?v_429 (= x_87 false)) (?v_409 (= x_88 x_48)) (?v_430 (and (= x_89 false) (= x_90 x_10))) (?v_424 (or ?v_405 ?v_386)) (?v_434 (not x_51))) (let ((?v_436 (or ?v_434 x_52)) (?v_394 (and (and (and (= x_93 false) (= x_94 x_5)) (= x_95 x_6)) (= x_96 x_7))) (?v_395 (= x_97 false)) (?v_442 (and (= x_98 false) (= x_99 x_10))) (?v_408 (= x_100 x_60)) (?v_445 (not x_42)) (?v_438 (not x_43))) (let ((?v_440 (and ?v_445 ?v_438)) (?v_412 (= x_101 false)) (?v_406 (and x_75 ?v_323)) (?v_388 (not x_103))) (let ((?v_390 (and x_102 ?v_388)) (?v_389 (not x_104))) (let ((?v_396 (and (and ?v_390 ?v_389) x_105)) (?v_391 (or x_102 x_103)) (?v_387 (not x_105)) (?v_392 (and x_102 x_103))) (let ((?v_397 (and (and ?v_392 x_104) ?v_387)) (?v_393 (or x_102 ?v_388)) (?v_399 (and (and ?v_390 x_104) ?v_387)) (?v_401 (and (and ?v_392 ?v_389) ?v_387))) (let ((?v_420 (or ?v_396 (and (or (or ?v_391 x_104) ?v_387) (or ?v_397 (and (or (or ?v_393 ?v_389) x_105) (or ?v_399 (and (or (or ?v_391 ?v_389) x_105) (or ?v_401 (and (and (and (and (or (or ?v_393 x_104) x_105) x_102) ?v_388) ?v_389) ?v_387))))))))) (?v_425 (not ?v_415)) (?v_448 (not ?v_441)) (?v_421 (not ?v_411)) (?v_407 (= x_101 true)) (?v_427 (not ?v_417)) (?v_474 (< x_13 x_14)) (?v_504 (<= x_29 x_30)) (?v_478 (< x_12 50)) (?v_480 (< x_12 20)) (?v_498 (= x_34 x_10))) (let ((?v_502 (and (= x_33 false) ?v_498)) (?v_507 (= x_37 x_30)) (?v_506 (= x_38 x_29)) (?v_492 (not x_24))) (let ((?v_495 (and x_23 ?v_492)) (?v_497 (= x_39 x_22)) (?v_476 (and (= x_40 false) (= x_41 x_10))) (?v_449 (not x_15))) (let ((?v_473 (and ?v_449 x_16)) (?v_509 (and x_42 ?v_438)) (?v_468 (= x_44 x_12)) (?v_477 (and x_15 x_16)) (?v_511 (or x_31 x_32)) (?v_450 (not x_16))) (let ((?v_485 (or x_15 ?v_450)) (?v_489 (< x_12 10)) (?v_486 (<= x_12 0)) (?v_496 (and (= x_45 false) (= x_46 x_10))) (?v_493 (= x_47 false)) (?v_472 (= x_48 x_13)) (?v_494 (and (= x_49 false) (= x_50 x_10))) (?v_487 (or ?v_449 ?v_450)) (?v_491 (not x_23))) (let ((?v_499 (or ?v_491 x_24)) (?v_458 (and (and (and (= x_53 false) (= x_54 x_5)) (= x_55 x_6)) (= x_56 x_7))) (?v_459 (= x_57 false)) (?v_505 (and (= x_58 false) (= x_59 x_10))) (?v_471 (= x_60 x_14)) (?v_508 (not x_31)) (?v_501 (not x_32))) (let ((?v_503 (and ?v_508 ?v_501)) (?v_475 (= x_61 false)) (?v_469 (and x_35 ?v_386)) (?v_452 (not x_63))) (let ((?v_454 (and x_62 ?v_452)) (?v_453 (not x_64))) (let ((?v_460 (and (and ?v_454 ?v_453) x_65)) (?v_455 (or x_62 x_63)) (?v_451 (not x_65)) (?v_456 (and x_62 x_63))) (let ((?v_461 (and (and ?v_456 x_64) ?v_451)) (?v_457 (or x_62 ?v_452)) (?v_463 (and (and ?v_454 x_64) ?v_451)) (?v_465 (and (and ?v_456 ?v_453) ?v_451))) (let ((?v_483 (or ?v_460 (and (or (or ?v_455 x_64) ?v_451) (or ?v_461 (and (or (or ?v_457 ?v_453) x_65) (or ?v_463 (and (or (or ?v_455 ?v_453) x_65) (or ?v_465 (and (and (and (and (or (or ?v_457 x_64) x_65) x_62) ?v_452) ?v_453) ?v_451))))))))) (?v_488 (not ?v_478)) (?v_512 (not ?v_504)) (?v_484 (not ?v_474)) (?v_470 (= x_61 true)) (?v_490 (not ?v_480)) (?v_510 (not x_20)) (?v_27 (not x_315)) (?v_12 (not x_342))) (let ((?v_14 (and ?v_12 ?v_2)) (?v_16 (and ?v_12 x_343))) (let ((?v_17 (ite ?v_10 4 (ite (and (and ?v_14 ?v_3) x_345) 4 (ite ?v_11 3 (ite (and (and ?v_16 x_344) ?v_1) 3 (ite ?v_13 2 (ite (and (and ?v_14 x_344) ?v_1) 2 (ite ?v_15 1 (ite (and (and ?v_16 ?v_3) ?v_1) 1 0))))))))) (?v_35 (not x_334)) (?v_33 (not x_336)) (?v_36 (not x_335)) (?v_57 (not x_313)) (?v_53 (not x_331)) (?v_59 (not x_322)) (?v_83 (not x_302))) (let ((?v_85 (and ?v_83 ?v_73)) (?v_87 (and ?v_83 x_303))) (let ((?v_88 (ite ?v_81 4 (ite (and (and ?v_85 ?v_74) x_305) 4 (ite ?v_82 3 (ite (and (and ?v_87 x_304) ?v_72) 3 (ite ?v_84 2 (ite (and (and ?v_85 x_304) ?v_72) 2 (ite ?v_86 1 (ite (and (and ?v_87 ?v_74) ?v_72) 1 0))))))))) (?v_103 (not x_294)) (?v_101 (not x_296)) (?v_104 (not x_295)) (?v_122 (not x_273)) (?v_146 (not x_262))) (let ((?v_148 (and ?v_146 ?v_136)) (?v_150 (and ?v_146 x_263))) (let ((?v_151 (ite ?v_144 4 (ite (and (and ?v_148 ?v_137) x_265) 4 (ite ?v_145 3 (ite (and (and ?v_150 x_264) ?v_135) 3 (ite ?v_147 2 (ite (and (and ?v_148 x_264) ?v_135) 2 (ite ?v_149 1 (ite (and (and ?v_150 ?v_137) ?v_135) 1 0))))))))) (?v_166 (not x_254)) (?v_164 (not x_256)) (?v_167 (not x_255)) (?v_185 (not x_233)) (?v_209 (not x_222))) (let ((?v_211 (and ?v_209 ?v_199)) (?v_213 (and ?v_209 x_223))) (let ((?v_214 (ite ?v_207 4 (ite (and (and ?v_211 ?v_200) x_225) 4 (ite ?v_208 3 (ite (and (and ?v_213 x_224) ?v_198) 3 (ite ?v_210 2 (ite (and (and ?v_211 x_224) ?v_198) 2 (ite ?v_212 1 (ite (and (and ?v_213 ?v_200) ?v_198) 1 0))))))))) (?v_229 (not x_214)) (?v_227 (not x_216)) (?v_230 (not x_215)) (?v_248 (not x_193)) (?v_272 (not x_182))) (let ((?v_274 (and ?v_272 ?v_262)) (?v_276 (and ?v_272 x_183))) (let ((?v_277 (ite ?v_270 4 (ite (and (and ?v_274 ?v_263) x_185) 4 (ite ?v_271 3 (ite (and (and ?v_276 x_184) ?v_261) 3 (ite ?v_273 2 (ite (and (and ?v_274 x_184) ?v_261) 2 (ite ?v_275 1 (ite (and (and ?v_276 ?v_263) ?v_261) 1 0))))))))) (?v_292 (not x_174)) (?v_290 (not x_176)) (?v_293 (not x_175)) (?v_311 (not x_153)) (?v_335 (not x_142))) (let ((?v_337 (and ?v_335 ?v_325)) (?v_339 (and ?v_335 x_143))) (let ((?v_340 (ite ?v_333 4 (ite (and (and ?v_337 ?v_326) x_145) 4 (ite ?v_334 3 (ite (and (and ?v_339 x_144) ?v_324) 3 (ite ?v_336 2 (ite (and (and ?v_337 x_144) ?v_324) 2 (ite ?v_338 1 (ite (and (and ?v_339 ?v_326) ?v_324) 1 0))))))))) (?v_355 (not x_134)) (?v_353 (not x_136)) (?v_356 (not x_135)) (?v_374 (not x_113)) (?v_398 (not x_102))) (let ((?v_400 (and ?v_398 ?v_388)) (?v_402 (and ?v_398 x_103))) (let ((?v_403 (ite ?v_396 4 (ite (and (and ?v_400 ?v_389) x_105) 4 (ite ?v_397 3 (ite (and (and ?v_402 x_104) ?v_387) 3 (ite ?v_399 2 (ite (and (and ?v_400 x_104) ?v_387) 2 (ite ?v_401 1 (ite (and (and ?v_402 ?v_389) ?v_387) 1 0))))))))) (?v_418 (not x_94)) (?v_416 (not x_96)) (?v_419 (not x_95)) (?v_437 (not x_73)) (?v_462 (not x_62))) (let ((?v_464 (and ?v_462 ?v_452)) (?v_466 (and ?v_462 x_63))) (let ((?v_467 (ite ?v_460 4 (ite (and (and ?v_464 ?v_453) x_65) 4 (ite ?v_461 3 (ite (and (and ?v_466 x_64) ?v_451) 3 (ite ?v_463 2 (ite (and (and ?v_464 x_64) ?v_451) 2 (ite ?v_465 1 (ite (and (and ?v_466 ?v_453) ?v_451) 1 0))))))))) (?v_481 (not x_54)) (?v_479 (not x_56)) (?v_482 (not x_55)) (?v_500 (not x_33)) (?v_516 (not x_2)) (?v_515 (not x_3)) (?v_514 (not x_4)) (?v_513 (not x_11))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not x_0) true) (not x_1)) (and (and (= x_2 x_5) (= x_3 x_6)) (= x_4 x_7))) (not x_8)) (= x_9 x_10)) ?v_513) true) (= x_12 0)) (= x_13 0)) (= x_14 0)) (and ?v_449 ?v_450)) (not x_17)) true) (not x_18)) (= x_19 x_10)) ?v_510) (= x_21 x_10)) (= x_22 0)) (and ?v_491 x_24)) (not x_25)) (= x_26 x_10)) (not x_27)) (= x_28 x_10)) (= x_29 0)) (= x_30 0)) (and x_31 ?v_501)) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (= x_346 0) ?v_19) ?v_0) x_338) ?v_20) x_320) (= x_321 x_339)) ?v_21) ?v_8) ?v_9) (= x_340 x_339)) ?v_18) ?v_23) (and (and (and (and (and (and (and (and (and (and (and (and (= x_346 1) x_275) ?v_0) ?v_37) ?v_27) x_316) ?v_8) ?v_26) ?v_29) ?v_9) (= x_328 (+ x_288 (* (ite (= ?v_17 4) 20 (ite (= ?v_17 3) 10 (ite (= ?v_17 2) 5 (ite (= ?v_17 1) 2 1)))) 10)))) ?v_22) ?v_18)) (and (and (and (and (and (and (and (and (and (and (and (= x_346 2) ?v_24) ?v_25) ?v_20) ?v_21) x_320) (= x_321 (- x_300 x_288))) ?v_8) ?v_9) ?v_22) ?v_18) ?v_23)) (and (and (and (and (and (and (and (and (and (and (and (= x_346 3) ?v_24) ?v_38) ?v_31) x_320) (= x_321 0)) x_337) ?v_8) ?v_26) (= x_324 (- x_288 x_300))) ?v_22) ?v_23)) (and (and (and (and (and (and (and (and (and (and (and (= x_346 4) ?v_30) ?v_40) ?v_27) ?v_28) ?v_8) ?v_26) ?v_29) ?v_9) (= x_328 0)) (= x_324 0)) (= x_340 0))) (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_346 5) ?v_30) ?v_42) ?v_31) x_333) ?v_35) x_335) ?v_33) ?v_26) ?v_29) ?v_9) (= x_324 (- x_284 50))) ?v_22) ?v_23)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_346 6) ?v_30) ?v_44) ?v_32) ?v_31) x_333) x_334) ?v_36) ?v_33) ?v_26) ?v_29) ?v_9) (= x_324 (- x_284 20))) ?v_22) ?v_23)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_346 7) ?v_30) (not ?v_43)) ?v_34) ?v_31) x_333) ?v_35) ?v_36) ?v_33) ?v_26) ?v_29) ?v_9) (= x_324 (- x_284 10))) ?v_22) ?v_23)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_346 8) (or (or x_275 x_276) (not x_338))) (or (or ?v_19 x_276) (not ?v_37))) (or ?v_39 ?v_38)) (or ?v_39 ?v_25)) (or ?v_41 (not ?v_40))) (or ?v_41 ?v_32)) (or (or ?v_41 ?v_34) ?v_42)) (or (or ?v_41 ?v_43) ?v_44)) ?v_26) ?v_8) ?v_29) ?v_9) (= x_315 x_275)) (= x_316 x_276)) ?v_22) ?v_18) ?v_23))) (or (or (or (or (and (and (and (and (and (and (and (and (= x_347 0) ?v_52) ?v_45) x_348) ?v_46) ?v_47) ?v_50) ?v_48) (= x_319 x_349)) (and (and (and (and (and (and (and (and (and (= x_347 1) ?v_49) ?v_57) ?v_55) ?v_46) x_325) (= x_326 x_279)) ?v_47) ?v_48) ?v_51)) (and (and (and (and (and (and (and (and (and (= x_347 2) ?v_49) x_313) ?v_53) x_332) x_329) (= x_330 x_314)) ?v_47) ?v_50) ?v_51)) (and (and (and (and (and (and (and (and (= x_347 3) ?v_52) x_292) ?v_53) ?v_54) x_327) ?v_50) ?v_48) ?v_51)) (and (and (and (and (and (and (and (and (and (and (= x_347 4) (or (or x_291 x_292) (not x_348))) (or (or ?v_56 x_313) (not ?v_55))) (or ?v_56 ?v_57)) (or x_291 ?v_45)) ?v_47) ?v_48) ?v_50) (= x_331 x_291)) (= x_332 x_292)) ?v_51))) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_350 0) x_282) ?v_58) x_285) x_351) ?v_59) ?v_63) ?v_64) ?v_60) (= x_318 x_352)) (= x_317 x_286)) (and (and (and (and (and (and (and (and (and (= x_350 1) ?v_61) ?v_70) ?v_59) x_323) x_338) (= x_339 (* (- x_278 x_277) 10))) ?v_60) ?v_65) ?v_66)) (and (and (and (and (and (and (and (and (= x_350 2) ?v_61) ?v_62) ?v_68) x_313) (= x_314 x_277)) ?v_64) ?v_65) ?v_66)) (and (and (and (and (and (and (and (and (and (= x_350 3) ?v_67) x_283) x_297) ?v_68) x_313) (= x_314 (+ x_278 10))) ?v_64) ?v_65) ?v_66)) (and (and (and (and (and (and (and (and (and (and (= x_350 4) (or (or (or ?v_67 x_283) (not x_285)) (not x_351))) (or ?v_69 ?v_62)) (or ?v_69 ?v_70)) (or (or x_282 ?v_58) (not x_297))) ?v_60) ?v_64) (= x_322 x_282)) (= x_323 x_283)) ?v_65) ?v_66))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (= x_306 0) ?v_90) ?v_71) x_298) ?v_91) x_280) (= x_281 x_299)) ?v_92) ?v_79) ?v_80) (= x_300 x_299)) ?v_89) ?v_94) (and (and (and (and (and (and (and (and (and (and (and (and (= x_306 1) x_235) ?v_71) ?v_105) ?v_19) x_276) ?v_79) ?v_97) ?v_98) ?v_80) (= x_288 (+ x_248 (* (ite (= ?v_88 4) 20 (ite (= ?v_88 3) 10 (ite (= ?v_88 2) 5 (ite (= ?v_88 1) 2 1)))) 10)))) ?v_93) ?v_89)) (and (and (and (and (and (and (and (and (and (and (and (= x_306 2) ?v_95) ?v_96) ?v_91) ?v_92) x_280) (= x_281 (- x_260 x_248))) ?v_79) ?v_80) ?v_93) ?v_89) ?v_94)) (and (and (and (and (and (and (and (and (and (and (and (= x_306 3) ?v_95) ?v_106) ?v_30) x_280) (= x_281 0)) x_297) ?v_79) ?v_97) (= x_284 (- x_248 x_260))) ?v_93) ?v_94)) (and (and (and (and (and (and (and (and (and (and (and (= x_306 4) ?v_99) ?v_108) ?v_19) ?v_0) ?v_79) ?v_97) ?v_98) ?v_80) (= x_288 0)) (= x_284 0)) (= x_300 0))) (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_306 5) ?v_99) ?v_110) ?v_30) x_293) ?v_103) x_295) ?v_101) ?v_97) ?v_98) ?v_80) (= x_284 (- x_244 50))) ?v_93) ?v_94)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_306 6) ?v_99) ?v_112) ?v_100) ?v_30) x_293) x_294) ?v_104) ?v_101) ?v_97) ?v_98) ?v_80) (= x_284 (- x_244 20))) ?v_93) ?v_94)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_306 7) ?v_99) (not ?v_111)) ?v_102) ?v_30) x_293) ?v_103) ?v_104) ?v_101) ?v_97) ?v_98) ?v_80) (= x_284 (- x_244 10))) ?v_93) ?v_94)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_306 8) (or (or x_235 x_236) (not x_298))) (or (or ?v_90 x_236) (not ?v_105))) (or ?v_107 ?v_106)) (or ?v_107 ?v_96)) (or ?v_109 (not ?v_108))) (or ?v_109 ?v_100)) (or (or ?v_109 ?v_102) ?v_110)) (or (or ?v_109 ?v_111) ?v_112)) ?v_97) ?v_79) ?v_98) ?v_80) (= x_275 x_235)) (= x_276 x_236)) ?v_93) ?v_89) ?v_94))) (or (or (or (or (and (and (and (and (and (and (and (and (= x_307 0) ?v_119) ?v_113) x_308) ?v_49) ?v_114) ?v_117) ?v_115) (= x_279 x_309)) (and (and (and (and (and (and (and (and (and (= x_307 1) ?v_116) ?v_122) ?v_120) ?v_49) x_285) (= x_286 x_239)) ?v_114) ?v_115) ?v_118)) (and (and (and (and (and (and (and (and (and (= x_307 2) ?v_116) x_273) ?v_52) x_292) x_289) (= x_290 x_274)) ?v_114) ?v_117) ?v_118)) (and (and (and (and (and (and (and (and (= x_307 3) ?v_119) x_252) ?v_52) ?v_45) x_287) ?v_117) ?v_115) ?v_118)) (and (and (and (and (and (and (and (and (and (and (= x_307 4) (or (or x_251 x_252) (not x_308))) (or (or ?v_121 x_273) (not ?v_120))) (or ?v_121 ?v_122)) (or x_251 ?v_113)) ?v_114) ?v_115) ?v_117) (= x_291 x_251)) (= x_292 x_252)) ?v_118))) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_310 0) x_242) ?v_123) x_245) x_311) ?v_67) ?v_58) ?v_127) ?v_124) (= x_278 x_312)) (= x_277 x_246)) (and (and (and (and (and (and (and (and (and (= x_310 1) ?v_125) ?v_133) ?v_67) x_283) x_298) (= x_299 (* (- x_238 x_237) 10))) ?v_124) ?v_128) ?v_129)) (and (and (and (and (and (and (and (and (= x_310 2) ?v_125) ?v_126) ?v_131) x_273) (= x_274 x_237)) ?v_127) ?v_128) ?v_129)) (and (and (and (and (and (and (and (and (and (= x_310 3) ?v_130) x_243) x_257) ?v_131) x_273) (= x_274 (+ x_238 10))) ?v_127) ?v_128) ?v_129)) (and (and (and (and (and (and (and (and (and (and (= x_310 4) (or (or (or ?v_130 x_243) (not x_245)) (not x_311))) (or ?v_132 ?v_126)) (or ?v_132 ?v_133)) (or (or x_242 ?v_123) (not x_257))) ?v_124) ?v_127) (= x_282 x_242)) (= x_283 x_243)) ?v_128) ?v_129))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (= x_266 0) ?v_153) ?v_134) x_258) ?v_154) x_240) (= x_241 x_259)) ?v_155) ?v_142) ?v_143) (= x_260 x_259)) ?v_152) ?v_157) (and (and (and (and (and (and (and (and (and (and (and (and (= x_266 1) x_195) ?v_134) ?v_168) ?v_90) x_236) ?v_142) ?v_160) ?v_161) ?v_143) (= x_248 (+ x_208 (* (ite (= ?v_151 4) 20 (ite (= ?v_151 3) 10 (ite (= ?v_151 2) 5 (ite (= ?v_151 1) 2 1)))) 10)))) ?v_156) ?v_152)) (and (and (and (and (and (and (and (and (and (and (and (= x_266 2) ?v_158) ?v_159) ?v_154) ?v_155) x_240) (= x_241 (- x_220 x_208))) ?v_142) ?v_143) ?v_156) ?v_152) ?v_157)) (and (and (and (and (and (and (and (and (and (and (and (= x_266 3) ?v_158) ?v_169) ?v_99) x_240) (= x_241 0)) x_257) ?v_142) ?v_160) (= x_244 (- x_208 x_220))) ?v_156) ?v_157)) (and (and (and (and (and (and (and (and (and (and (and (= x_266 4) ?v_162) ?v_171) ?v_90) ?v_71) ?v_142) ?v_160) ?v_161) ?v_143) (= x_248 0)) (= x_244 0)) (= x_260 0))) (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_266 5) ?v_162) ?v_173) ?v_99) x_253) ?v_166) x_255) ?v_164) ?v_160) ?v_161) ?v_143) (= x_244 (- x_204 50))) ?v_156) ?v_157)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_266 6) ?v_162) ?v_175) ?v_163) ?v_99) x_253) x_254) ?v_167) ?v_164) ?v_160) ?v_161) ?v_143) (= x_244 (- x_204 20))) ?v_156) ?v_157)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_266 7) ?v_162) (not ?v_174)) ?v_165) ?v_99) x_253) ?v_166) ?v_167) ?v_164) ?v_160) ?v_161) ?v_143) (= x_244 (- x_204 10))) ?v_156) ?v_157)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_266 8) (or (or x_195 x_196) (not x_258))) (or (or ?v_153 x_196) (not ?v_168))) (or ?v_170 ?v_169)) (or ?v_170 ?v_159)) (or ?v_172 (not ?v_171))) (or ?v_172 ?v_163)) (or (or ?v_172 ?v_165) ?v_173)) (or (or ?v_172 ?v_174) ?v_175)) ?v_160) ?v_142) ?v_161) ?v_143) (= x_235 x_195)) (= x_236 x_196)) ?v_156) ?v_152) ?v_157))) (or (or (or (or (and (and (and (and (and (and (and (and (= x_267 0) ?v_182) ?v_176) x_268) ?v_116) ?v_177) ?v_180) ?v_178) (= x_239 x_269)) (and (and (and (and (and (and (and (and (and (= x_267 1) ?v_179) ?v_185) ?v_183) ?v_116) x_245) (= x_246 x_199)) ?v_177) ?v_178) ?v_181)) (and (and (and (and (and (and (and (and (and (= x_267 2) ?v_179) x_233) ?v_119) x_252) x_249) (= x_250 x_234)) ?v_177) ?v_180) ?v_181)) (and (and (and (and (and (and (and (and (= x_267 3) ?v_182) x_212) ?v_119) ?v_113) x_247) ?v_180) ?v_178) ?v_181)) (and (and (and (and (and (and (and (and (and (and (= x_267 4) (or (or x_211 x_212) (not x_268))) (or (or ?v_184 x_233) (not ?v_183))) (or ?v_184 ?v_185)) (or x_211 ?v_176)) ?v_177) ?v_178) ?v_180) (= x_251 x_211)) (= x_252 x_212)) ?v_181))) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_270 0) x_202) ?v_186) x_205) x_271) ?v_130) ?v_123) ?v_190) ?v_187) (= x_238 x_272)) (= x_237 x_206)) (and (and (and (and (and (and (and (and (and (= x_270 1) ?v_188) ?v_196) ?v_130) x_243) x_258) (= x_259 (* (- x_198 x_197) 10))) ?v_187) ?v_191) ?v_192)) (and (and (and (and (and (and (and (and (= x_270 2) ?v_188) ?v_189) ?v_194) x_233) (= x_234 x_197)) ?v_190) ?v_191) ?v_192)) (and (and (and (and (and (and (and (and (and (= x_270 3) ?v_193) x_203) x_217) ?v_194) x_233) (= x_234 (+ x_198 10))) ?v_190) ?v_191) ?v_192)) (and (and (and (and (and (and (and (and (and (and (= x_270 4) (or (or (or ?v_193 x_203) (not x_205)) (not x_271))) (or ?v_195 ?v_189)) (or ?v_195 ?v_196)) (or (or x_202 ?v_186) (not x_217))) ?v_187) ?v_190) (= x_242 x_202)) (= x_243 x_203)) ?v_191) ?v_192))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (= x_226 0) ?v_216) ?v_197) x_218) ?v_217) x_200) (= x_201 x_219)) ?v_218) ?v_205) ?v_206) (= x_220 x_219)) ?v_215) ?v_220) (and (and (and (and (and (and (and (and (and (and (and (and (= x_226 1) x_155) ?v_197) ?v_231) ?v_153) x_196) ?v_205) ?v_223) ?v_224) ?v_206) (= x_208 (+ x_168 (* (ite (= ?v_214 4) 20 (ite (= ?v_214 3) 10 (ite (= ?v_214 2) 5 (ite (= ?v_214 1) 2 1)))) 10)))) ?v_219) ?v_215)) (and (and (and (and (and (and (and (and (and (and (and (= x_226 2) ?v_221) ?v_222) ?v_217) ?v_218) x_200) (= x_201 (- x_180 x_168))) ?v_205) ?v_206) ?v_219) ?v_215) ?v_220)) (and (and (and (and (and (and (and (and (and (and (and (= x_226 3) ?v_221) ?v_232) ?v_162) x_200) (= x_201 0)) x_217) ?v_205) ?v_223) (= x_204 (- x_168 x_180))) ?v_219) ?v_220)) (and (and (and (and (and (and (and (and (and (and (and (= x_226 4) ?v_225) ?v_234) ?v_153) ?v_134) ?v_205) ?v_223) ?v_224) ?v_206) (= x_208 0)) (= x_204 0)) (= x_220 0))) (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_226 5) ?v_225) ?v_236) ?v_162) x_213) ?v_229) x_215) ?v_227) ?v_223) ?v_224) ?v_206) (= x_204 (- x_164 50))) ?v_219) ?v_220)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_226 6) ?v_225) ?v_238) ?v_226) ?v_162) x_213) x_214) ?v_230) ?v_227) ?v_223) ?v_224) ?v_206) (= x_204 (- x_164 20))) ?v_219) ?v_220)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_226 7) ?v_225) (not ?v_237)) ?v_228) ?v_162) x_213) ?v_229) ?v_230) ?v_227) ?v_223) ?v_224) ?v_206) (= x_204 (- x_164 10))) ?v_219) ?v_220)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_226 8) (or (or x_155 x_156) (not x_218))) (or (or ?v_216 x_156) (not ?v_231))) (or ?v_233 ?v_232)) (or ?v_233 ?v_222)) (or ?v_235 (not ?v_234))) (or ?v_235 ?v_226)) (or (or ?v_235 ?v_228) ?v_236)) (or (or ?v_235 ?v_237) ?v_238)) ?v_223) ?v_205) ?v_224) ?v_206) (= x_195 x_155)) (= x_196 x_156)) ?v_219) ?v_215) ?v_220))) (or (or (or (or (and (and (and (and (and (and (and (and (= x_227 0) ?v_245) ?v_239) x_228) ?v_179) ?v_240) ?v_243) ?v_241) (= x_199 x_229)) (and (and (and (and (and (and (and (and (and (= x_227 1) ?v_242) ?v_248) ?v_246) ?v_179) x_205) (= x_206 x_159)) ?v_240) ?v_241) ?v_244)) (and (and (and (and (and (and (and (and (and (= x_227 2) ?v_242) x_193) ?v_182) x_212) x_209) (= x_210 x_194)) ?v_240) ?v_243) ?v_244)) (and (and (and (and (and (and (and (and (= x_227 3) ?v_245) x_172) ?v_182) ?v_176) x_207) ?v_243) ?v_241) ?v_244)) (and (and (and (and (and (and (and (and (and (and (= x_227 4) (or (or x_171 x_172) (not x_228))) (or (or ?v_247 x_193) (not ?v_246))) (or ?v_247 ?v_248)) (or x_171 ?v_239)) ?v_240) ?v_241) ?v_243) (= x_211 x_171)) (= x_212 x_172)) ?v_244))) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_230 0) x_162) ?v_249) x_165) x_231) ?v_193) ?v_186) ?v_253) ?v_250) (= x_198 x_232)) (= x_197 x_166)) (and (and (and (and (and (and (and (and (and (= x_230 1) ?v_251) ?v_259) ?v_193) x_203) x_218) (= x_219 (* (- x_158 x_157) 10))) ?v_250) ?v_254) ?v_255)) (and (and (and (and (and (and (and (and (= x_230 2) ?v_251) ?v_252) ?v_257) x_193) (= x_194 x_157)) ?v_253) ?v_254) ?v_255)) (and (and (and (and (and (and (and (and (and (= x_230 3) ?v_256) x_163) x_177) ?v_257) x_193) (= x_194 (+ x_158 10))) ?v_253) ?v_254) ?v_255)) (and (and (and (and (and (and (and (and (and (and (= x_230 4) (or (or (or ?v_256 x_163) (not x_165)) (not x_231))) (or ?v_258 ?v_252)) (or ?v_258 ?v_259)) (or (or x_162 ?v_249) (not x_177))) ?v_250) ?v_253) (= x_202 x_162)) (= x_203 x_163)) ?v_254) ?v_255))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (= x_186 0) ?v_279) ?v_260) x_178) ?v_280) x_160) (= x_161 x_179)) ?v_281) ?v_268) ?v_269) (= x_180 x_179)) ?v_278) ?v_283) (and (and (and (and (and (and (and (and (and (and (and (and (= x_186 1) x_115) ?v_260) ?v_294) ?v_216) x_156) ?v_268) ?v_286) ?v_287) ?v_269) (= x_168 (+ x_128 (* (ite (= ?v_277 4) 20 (ite (= ?v_277 3) 10 (ite (= ?v_277 2) 5 (ite (= ?v_277 1) 2 1)))) 10)))) ?v_282) ?v_278)) (and (and (and (and (and (and (and (and (and (and (and (= x_186 2) ?v_284) ?v_285) ?v_280) ?v_281) x_160) (= x_161 (- x_140 x_128))) ?v_268) ?v_269) ?v_282) ?v_278) ?v_283)) (and (and (and (and (and (and (and (and (and (and (and (= x_186 3) ?v_284) ?v_295) ?v_225) x_160) (= x_161 0)) x_177) ?v_268) ?v_286) (= x_164 (- x_128 x_140))) ?v_282) ?v_283)) (and (and (and (and (and (and (and (and (and (and (and (= x_186 4) ?v_288) ?v_297) ?v_216) ?v_197) ?v_268) ?v_286) ?v_287) ?v_269) (= x_168 0)) (= x_164 0)) (= x_180 0))) (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_186 5) ?v_288) ?v_299) ?v_225) x_173) ?v_292) x_175) ?v_290) ?v_286) ?v_287) ?v_269) (= x_164 (- x_124 50))) ?v_282) ?v_283)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_186 6) ?v_288) ?v_301) ?v_289) ?v_225) x_173) x_174) ?v_293) ?v_290) ?v_286) ?v_287) ?v_269) (= x_164 (- x_124 20))) ?v_282) ?v_283)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_186 7) ?v_288) (not ?v_300)) ?v_291) ?v_225) x_173) ?v_292) ?v_293) ?v_290) ?v_286) ?v_287) ?v_269) (= x_164 (- x_124 10))) ?v_282) ?v_283)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_186 8) (or (or x_115 x_116) (not x_178))) (or (or ?v_279 x_116) (not ?v_294))) (or ?v_296 ?v_295)) (or ?v_296 ?v_285)) (or ?v_298 (not ?v_297))) (or ?v_298 ?v_289)) (or (or ?v_298 ?v_291) ?v_299)) (or (or ?v_298 ?v_300) ?v_301)) ?v_286) ?v_268) ?v_287) ?v_269) (= x_155 x_115)) (= x_156 x_116)) ?v_282) ?v_278) ?v_283))) (or (or (or (or (and (and (and (and (and (and (and (and (= x_187 0) ?v_308) ?v_302) x_188) ?v_242) ?v_303) ?v_306) ?v_304) (= x_159 x_189)) (and (and (and (and (and (and (and (and (and (= x_187 1) ?v_305) ?v_311) ?v_309) ?v_242) x_165) (= x_166 x_119)) ?v_303) ?v_304) ?v_307)) (and (and (and (and (and (and (and (and (and (= x_187 2) ?v_305) x_153) ?v_245) x_172) x_169) (= x_170 x_154)) ?v_303) ?v_306) ?v_307)) (and (and (and (and (and (and (and (and (= x_187 3) ?v_308) x_132) ?v_245) ?v_239) x_167) ?v_306) ?v_304) ?v_307)) (and (and (and (and (and (and (and (and (and (and (= x_187 4) (or (or x_131 x_132) (not x_188))) (or (or ?v_310 x_153) (not ?v_309))) (or ?v_310 ?v_311)) (or x_131 ?v_302)) ?v_303) ?v_304) ?v_306) (= x_171 x_131)) (= x_172 x_132)) ?v_307))) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_190 0) x_122) ?v_312) x_125) x_191) ?v_256) ?v_249) ?v_316) ?v_313) (= x_158 x_192)) (= x_157 x_126)) (and (and (and (and (and (and (and (and (and (= x_190 1) ?v_314) ?v_322) ?v_256) x_163) x_178) (= x_179 (* (- x_118 x_117) 10))) ?v_313) ?v_317) ?v_318)) (and (and (and (and (and (and (and (and (= x_190 2) ?v_314) ?v_315) ?v_320) x_153) (= x_154 x_117)) ?v_316) ?v_317) ?v_318)) (and (and (and (and (and (and (and (and (and (= x_190 3) ?v_319) x_123) x_137) ?v_320) x_153) (= x_154 (+ x_118 10))) ?v_316) ?v_317) ?v_318)) (and (and (and (and (and (and (and (and (and (and (= x_190 4) (or (or (or ?v_319 x_123) (not x_125)) (not x_191))) (or ?v_321 ?v_315)) (or ?v_321 ?v_322)) (or (or x_122 ?v_312) (not x_137))) ?v_313) ?v_316) (= x_162 x_122)) (= x_163 x_123)) ?v_317) ?v_318))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (= x_146 0) ?v_342) ?v_323) x_138) ?v_343) x_120) (= x_121 x_139)) ?v_344) ?v_331) ?v_332) (= x_140 x_139)) ?v_341) ?v_346) (and (and (and (and (and (and (and (and (and (and (and (and (= x_146 1) x_75) ?v_323) ?v_357) ?v_279) x_116) ?v_331) ?v_349) ?v_350) ?v_332) (= x_128 (+ x_88 (* (ite (= ?v_340 4) 20 (ite (= ?v_340 3) 10 (ite (= ?v_340 2) 5 (ite (= ?v_340 1) 2 1)))) 10)))) ?v_345) ?v_341)) (and (and (and (and (and (and (and (and (and (and (and (= x_146 2) ?v_347) ?v_348) ?v_343) ?v_344) x_120) (= x_121 (- x_100 x_88))) ?v_331) ?v_332) ?v_345) ?v_341) ?v_346)) (and (and (and (and (and (and (and (and (and (and (and (= x_146 3) ?v_347) ?v_358) ?v_288) x_120) (= x_121 0)) x_137) ?v_331) ?v_349) (= x_124 (- x_88 x_100))) ?v_345) ?v_346)) (and (and (and (and (and (and (and (and (and (and (and (= x_146 4) ?v_351) ?v_360) ?v_279) ?v_260) ?v_331) ?v_349) ?v_350) ?v_332) (= x_128 0)) (= x_124 0)) (= x_140 0))) (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_146 5) ?v_351) ?v_362) ?v_288) x_133) ?v_355) x_135) ?v_353) ?v_349) ?v_350) ?v_332) (= x_124 (- x_84 50))) ?v_345) ?v_346)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_146 6) ?v_351) ?v_364) ?v_352) ?v_288) x_133) x_134) ?v_356) ?v_353) ?v_349) ?v_350) ?v_332) (= x_124 (- x_84 20))) ?v_345) ?v_346)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_146 7) ?v_351) (not ?v_363)) ?v_354) ?v_288) x_133) ?v_355) ?v_356) ?v_353) ?v_349) ?v_350) ?v_332) (= x_124 (- x_84 10))) ?v_345) ?v_346)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_146 8) (or (or x_75 x_76) (not x_138))) (or (or ?v_342 x_76) (not ?v_357))) (or ?v_359 ?v_358)) (or ?v_359 ?v_348)) (or ?v_361 (not ?v_360))) (or ?v_361 ?v_352)) (or (or ?v_361 ?v_354) ?v_362)) (or (or ?v_361 ?v_363) ?v_364)) ?v_349) ?v_331) ?v_350) ?v_332) (= x_115 x_75)) (= x_116 x_76)) ?v_345) ?v_341) ?v_346))) (or (or (or (or (and (and (and (and (and (and (and (and (= x_147 0) ?v_371) ?v_365) x_148) ?v_305) ?v_366) ?v_369) ?v_367) (= x_119 x_149)) (and (and (and (and (and (and (and (and (and (= x_147 1) ?v_368) ?v_374) ?v_372) ?v_305) x_125) (= x_126 x_79)) ?v_366) ?v_367) ?v_370)) (and (and (and (and (and (and (and (and (and (= x_147 2) ?v_368) x_113) ?v_308) x_132) x_129) (= x_130 x_114)) ?v_366) ?v_369) ?v_370)) (and (and (and (and (and (and (and (and (= x_147 3) ?v_371) x_92) ?v_308) ?v_302) x_127) ?v_369) ?v_367) ?v_370)) (and (and (and (and (and (and (and (and (and (and (= x_147 4) (or (or x_91 x_92) (not x_148))) (or (or ?v_373 x_113) (not ?v_372))) (or ?v_373 ?v_374)) (or x_91 ?v_365)) ?v_366) ?v_367) ?v_369) (= x_131 x_91)) (= x_132 x_92)) ?v_370))) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_150 0) x_82) ?v_375) x_85) x_151) ?v_319) ?v_312) ?v_379) ?v_376) (= x_118 x_152)) (= x_117 x_86)) (and (and (and (and (and (and (and (and (and (= x_150 1) ?v_377) ?v_385) ?v_319) x_123) x_138) (= x_139 (* (- x_78 x_77) 10))) ?v_376) ?v_380) ?v_381)) (and (and (and (and (and (and (and (and (= x_150 2) ?v_377) ?v_378) ?v_383) x_113) (= x_114 x_77)) ?v_379) ?v_380) ?v_381)) (and (and (and (and (and (and (and (and (and (= x_150 3) ?v_382) x_83) x_97) ?v_383) x_113) (= x_114 (+ x_78 10))) ?v_379) ?v_380) ?v_381)) (and (and (and (and (and (and (and (and (and (and (= x_150 4) (or (or (or ?v_382 x_83) (not x_85)) (not x_151))) (or ?v_384 ?v_378)) (or ?v_384 ?v_385)) (or (or x_82 ?v_375) (not x_97))) ?v_376) ?v_379) (= x_122 x_82)) (= x_123 x_83)) ?v_380) ?v_381))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (= x_106 0) ?v_405) ?v_386) x_98) ?v_406) x_80) (= x_81 x_99)) ?v_407) ?v_394) ?v_395) (= x_100 x_99)) ?v_404) ?v_409) (and (and (and (and (and (and (and (and (and (and (and (and (= x_106 1) x_35) ?v_386) ?v_420) ?v_342) x_76) ?v_394) ?v_412) ?v_413) ?v_395) (= x_88 (+ x_48 (* (ite (= ?v_403 4) 20 (ite (= ?v_403 3) 10 (ite (= ?v_403 2) 5 (ite (= ?v_403 1) 2 1)))) 10)))) ?v_408) ?v_404)) (and (and (and (and (and (and (and (and (and (and (and (= x_106 2) ?v_410) ?v_411) ?v_406) ?v_407) x_80) (= x_81 (- x_60 x_48))) ?v_394) ?v_395) ?v_408) ?v_404) ?v_409)) (and (and (and (and (and (and (and (and (and (and (and (= x_106 3) ?v_410) ?v_421) ?v_351) x_80) (= x_81 0)) x_97) ?v_394) ?v_412) (= x_84 (- x_48 x_60))) ?v_408) ?v_409)) (and (and (and (and (and (and (and (and (and (and (and (= x_106 4) ?v_414) ?v_423) ?v_342) ?v_323) ?v_394) ?v_412) ?v_413) ?v_395) (= x_88 0)) (= x_84 0)) (= x_100 0))) (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_106 5) ?v_414) ?v_425) ?v_351) x_93) ?v_418) x_95) ?v_416) ?v_412) ?v_413) ?v_395) (= x_84 (- x_44 50))) ?v_408) ?v_409)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_106 6) ?v_414) ?v_427) ?v_415) ?v_351) x_93) x_94) ?v_419) ?v_416) ?v_412) ?v_413) ?v_395) (= x_84 (- x_44 20))) ?v_408) ?v_409)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_106 7) ?v_414) (not ?v_426)) ?v_417) ?v_351) x_93) ?v_418) ?v_419) ?v_416) ?v_412) ?v_413) ?v_395) (= x_84 (- x_44 10))) ?v_408) ?v_409)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_106 8) (or (or x_35 x_36) (not x_98))) (or (or ?v_405 x_36) (not ?v_420))) (or ?v_422 ?v_421)) (or ?v_422 ?v_411)) (or ?v_424 (not ?v_423))) (or ?v_424 ?v_415)) (or (or ?v_424 ?v_417) ?v_425)) (or (or ?v_424 ?v_426) ?v_427)) ?v_412) ?v_394) ?v_413) ?v_395) (= x_75 x_35)) (= x_76 x_36)) ?v_408) ?v_404) ?v_409))) (or (or (or (or (and (and (and (and (and (and (and (and (= x_107 0) ?v_434) ?v_428) x_108) ?v_368) ?v_429) ?v_432) ?v_430) (= x_79 x_109)) (and (and (and (and (and (and (and (and (and (= x_107 1) ?v_431) ?v_437) ?v_435) ?v_368) x_85) (= x_86 x_39)) ?v_429) ?v_430) ?v_433)) (and (and (and (and (and (and (and (and (and (= x_107 2) ?v_431) x_73) ?v_371) x_92) x_89) (= x_90 x_74)) ?v_429) ?v_432) ?v_433)) (and (and (and (and (and (and (and (and (= x_107 3) ?v_434) x_52) ?v_371) ?v_365) x_87) ?v_432) ?v_430) ?v_433)) (and (and (and (and (and (and (and (and (and (and (= x_107 4) (or (or x_51 x_52) (not x_108))) (or (or ?v_436 x_73) (not ?v_435))) (or ?v_436 ?v_437)) (or x_51 ?v_428)) ?v_429) ?v_430) ?v_432) (= x_91 x_51)) (= x_92 x_52)) ?v_433))) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_110 0) x_42) ?v_438) x_45) x_111) ?v_382) ?v_375) ?v_442) ?v_439) (= x_78 x_112)) (= x_77 x_46)) (and (and (and (and (and (and (and (and (and (= x_110 1) ?v_440) ?v_448) ?v_382) x_83) x_98) (= x_99 (* (- x_38 x_37) 10))) ?v_439) ?v_443) ?v_444)) (and (and (and (and (and (and (and (and (= x_110 2) ?v_440) ?v_441) ?v_446) x_73) (= x_74 x_37)) ?v_442) ?v_443) ?v_444)) (and (and (and (and (and (and (and (and (and (= x_110 3) ?v_445) x_43) x_57) ?v_446) x_73) (= x_74 (+ x_38 10))) ?v_442) ?v_443) ?v_444)) (and (and (and (and (and (and (and (and (and (and (= x_110 4) (or (or (or ?v_445 x_43) (not x_45)) (not x_111))) (or ?v_447 ?v_441)) (or ?v_447 ?v_448)) (or (or x_42 ?v_438) (not x_57))) ?v_439) ?v_442) (= x_82 x_42)) (= x_83 x_43)) ?v_443) ?v_444))) (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (= x_66 0) ?v_449) ?v_450) x_58) ?v_469) x_40) (= x_41 x_59)) ?v_470) ?v_458) ?v_459) (= x_60 x_59)) ?v_468) ?v_472) (and (and (and (and (and (and (and (and (and (and (and (and (= x_66 1) x_15) ?v_450) ?v_483) ?v_405) x_36) ?v_458) ?v_475) ?v_476) ?v_459) (= x_48 (+ x_13 (* (ite (= ?v_467 4) 20 (ite (= ?v_467 3) 10 (ite (= ?v_467 2) 5 (ite (= ?v_467 1) 2 1)))) 10)))) ?v_471) ?v_468)) (and (and (and (and (and (and (and (and (and (and (and (= x_66 2) ?v_473) ?v_474) ?v_469) ?v_470) x_40) (= x_41 (- x_14 x_13))) ?v_458) ?v_459) ?v_471) ?v_468) ?v_472)) (and (and (and (and (and (and (and (and (and (and (and (= x_66 3) ?v_473) ?v_484) ?v_414) x_40) (= x_41 0)) x_57) ?v_458) ?v_475) (= x_44 (- x_13 x_14))) ?v_471) ?v_472)) (and (and (and (and (and (and (and (and (and (and (and (= x_66 4) ?v_477) ?v_486) ?v_405) ?v_386) ?v_458) ?v_475) ?v_476) ?v_459) (= x_48 0)) (= x_44 0)) (= x_60 0))) (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_66 5) ?v_477) ?v_488) ?v_414) x_53) ?v_481) x_55) ?v_479) ?v_475) ?v_476) ?v_459) (= x_44 (- x_12 50))) ?v_471) ?v_472)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_66 6) ?v_477) ?v_490) ?v_478) ?v_414) x_53) x_54) ?v_482) ?v_479) ?v_475) ?v_476) ?v_459) (= x_44 (- x_12 20))) ?v_471) ?v_472)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_66 7) ?v_477) (not ?v_489)) ?v_480) ?v_414) x_53) ?v_481) ?v_482) ?v_479) ?v_475) ?v_476) ?v_459) (= x_44 (- x_12 10))) ?v_471) ?v_472)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_66 8) (or (or x_15 x_16) (not x_58))) (or (or ?v_449 x_16) (not ?v_483))) (or ?v_485 ?v_484)) (or ?v_485 ?v_474)) (or ?v_487 (not ?v_486))) (or ?v_487 ?v_478)) (or (or ?v_487 ?v_480) ?v_488)) (or (or ?v_487 ?v_489) ?v_490)) ?v_475) ?v_458) ?v_476) ?v_459) (= x_35 x_15)) (= x_36 x_16)) ?v_471) ?v_468) ?v_472))) (or (or (or (or (and (and (and (and (and (and (and (and (= x_67 0) ?v_491) ?v_492) x_68) ?v_431) ?v_493) ?v_496) ?v_494) (= x_39 x_69)) (and (and (and (and (and (and (and (and (and (= x_67 1) ?v_495) ?v_500) ?v_498) ?v_431) x_45) (= x_46 x_22)) ?v_493) ?v_494) ?v_497)) (and (and (and (and (and (and (and (and (and (= x_67 2) ?v_495) x_33) ?v_434) x_52) x_49) (= x_50 x_34)) ?v_493) ?v_496) ?v_497)) (and (and (and (and (and (and (and (and (= x_67 3) ?v_491) x_24) ?v_434) ?v_428) x_47) ?v_496) ?v_494) ?v_497)) (and (and (and (and (and (and (and (and (and (and (= x_67 4) (or (or x_23 x_24) (not x_68))) (or (or ?v_499 x_33) (not ?v_498))) (or ?v_499 ?v_500)) (or x_23 ?v_492)) ?v_493) ?v_494) ?v_496) (= x_51 x_23)) (= x_52 x_24)) ?v_497))) (or (or (or (or (and (and (and (and (and (and (and (and (and (and (= x_70 0) x_31) ?v_501) x_20) x_71) ?v_445) ?v_438) ?v_505) ?v_502) (= x_38 x_72)) (= x_37 x_21)) (and (and (and (and (and (and (and (and (and (= x_70 1) ?v_503) ?v_512) ?v_445) x_43) x_58) (= x_59 (* (- x_29 x_30) 10))) ?v_502) ?v_506) ?v_507)) (and (and (and (and (and (and (and (and (= x_70 2) ?v_503) ?v_504) ?v_509) x_33) (= x_34 x_30)) ?v_505) ?v_506) ?v_507)) (and (and (and (and (and (and (and (and (and (= x_70 3) ?v_508) x_32) x_11) ?v_509) x_33) (= x_34 (+ x_29 10))) ?v_505) ?v_506) ?v_507)) (and (and (and (and (and (and (and (and (and (and (= x_70 4) (or (or (or ?v_508 x_32) ?v_510) (not x_71))) (or ?v_511 ?v_504)) (or ?v_511 ?v_512)) (or (or x_31 ?v_501) ?v_513)) ?v_502) ?v_505) (= x_42 x_31)) (= x_43 x_32)) ?v_506) ?v_507))) (or (or (or (or (or (or (or (or (and (and (and x_333 ?v_35) ?v_36) ?v_33) (and (and (and x_293 ?v_103) ?v_104) ?v_101)) (and (and (and x_253 ?v_166) ?v_167) ?v_164)) (and (and (and x_213 ?v_229) ?v_230) ?v_227)) (and (and (and x_173 ?v_292) ?v_293) ?v_290)) (and (and (and x_133 ?v_355) ?v_356) ?v_353)) (and (and (and x_93 ?v_418) ?v_419) ?v_416)) (and (and (and x_53 ?v_481) ?v_482) ?v_479)) (and (and (and x_1 ?v_516) ?v_515) ?v_514))) (or ?v_514 (and ?v_515 ?v_516))) (or (not x_7) (and (not x_6) (not x_5)))) (or ?v_492 ?v_491)) (or ?v_501 ?v_508)) (or ?v_438 ?v_445)) (or ?v_428 ?v_434)) (or ?v_479 (and ?v_482 ?v_481))) (or ?v_451 (and ?v_453 ?v_452))) (or ?v_375 ?v_382)) (or ?v_365 ?v_371)) (or ?v_416 (and ?v_419 ?v_418))) (or ?v_387 (and ?v_389 ?v_388))) (or ?v_312 ?v_319)) (or ?v_302 ?v_308)) (or ?v_353 (and ?v_356 ?v_355))) (or ?v_324 (and ?v_326 ?v_325))) (or ?v_249 ?v_256)) (or ?v_239 ?v_245)) (or ?v_290 (and ?v_293 ?v_292))) (or ?v_261 (and ?v_263 ?v_262))) (or ?v_186 ?v_193)) (or ?v_176 ?v_182)) (or ?v_227 (and ?v_230 ?v_229))) (or ?v_198 (and ?v_200 ?v_199))) (or ?v_123 ?v_130)) (or ?v_113 ?v_119)) (or ?v_164 (and ?v_167 ?v_166))) (or ?v_135 (and ?v_137 ?v_136))) (or ?v_58 ?v_67)) (or ?v_45 ?v_52)) (or ?v_101 (and ?v_104 ?v_103))) (or ?v_72 (and ?v_74 ?v_73))) (or ?v_63 ?v_59)) (or ?v_54 ?v_53)) (or ?v_33 (and ?v_36 ?v_35))) (or ?v_1 (and ?v_3 ?v_2)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(check-sat) +(exit)