sidekick/tests/unsat/pb_real_30_0600_10_18.smt2

(set-info :smt-lib-version 2.6)
(set-logic QF_UFLRA)
(set-info :source |
MathSat group

|)
(set-info :category "random")
(set-info :status unsat)
(declare-fun f0_1 (Real) Real)
(declare-fun f0_2 (Real Real) Real)
(declare-fun f0_3 (Real Real Real) Real)
(declare-fun f0_4 (Real Real Real Real) Real)
(declare-fun f1_1 (Real) Real)
(declare-fun f1_2 (Real Real) Real)
(declare-fun f1_3 (Real Real Real) Real)
(declare-fun f1_4 (Real Real Real Real) Real)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
(declare-fun x2 () Real)
(declare-fun x3 () Real)
(declare-fun x4 () Real)
(declare-fun x5 () Real)
(declare-fun x6 () Real)
(declare-fun x7 () Real)
(declare-fun x8 () Real)
(declare-fun x9 () Real)
(declare-fun x10 () Real)
(declare-fun x11 () Real)
(declare-fun x12 () Real)
(declare-fun x13 () Real)
(declare-fun x14 () Real)
(declare-fun x15 () Real)
(declare-fun x16 () Real)
(declare-fun x17 () Real)
(declare-fun x18 () Real)
(declare-fun x19 () Real)
(declare-fun x20 () Real)
(declare-fun x21 () Real)
(declare-fun x22 () Real)
(declare-fun x23 () Real)
(declare-fun x24 () Real)
(declare-fun x25 () Real)
(declare-fun x26 () Real)
(declare-fun x27 () Real)
(declare-fun x28 () Real)
(declare-fun x29 () Real)
(declare-fun P0 () Bool)
(declare-fun P1 () Bool)
(declare-fun P2 () Bool)
(declare-fun P3 () Bool)
(declare-fun P4 () Bool)
(declare-fun P5 () Bool)
(declare-fun P6 () Bool)
(declare-fun P7 () Bool)
(declare-fun P8 () Bool)
(declare-fun P9 () Bool)
(declare-fun P10 () Bool)
(declare-fun P11 () Bool)
(declare-fun P12 () Bool)
(declare-fun P13 () Bool)
(declare-fun P14 () Bool)
(declare-fun P15 () Bool)
(declare-fun P16 () Bool)
(declare-fun P17 () Bool)
(declare-fun P18 () Bool)
(declare-fun P19 () Bool)
(declare-fun P20 () Bool)
(declare-fun P21 () Bool)
(declare-fun P22 () Bool)
(declare-fun P23 () Bool)
(declare-fun P24 () Bool)
(declare-fun P25 () Bool)
(declare-fun P26 () Bool)
(declare-fun P27 () Bool)
(declare-fun P28 () Bool)
(declare-fun P29 () Bool)
(assert (let ((?v_16 (f0_1 x10)) (?v_151 (+ (- (* 4 x20) (* 27 x8)) (* 24 x22))) (?v_76 (f1_2 x20 x26)) (?v_10 (f0_2 x10 x11)) (?v_64 (f1_2 x21 x7)) (?v_13 (f0_1 x1)) (?v_2 (f0_1 x24)) (?v_7 (f1_2 x2 x27)) (?v_1 (f1_2 x19 x10))) (let ((?v_282 (f1_1 ?v_151)) (?v_70 (+ (- (* 16 x25) (* 18 x1)) (* 9 x15))) (?v_36 (* 2 x25)) (?v_6 (f0_1 x2)) (?v_0 (f0_1 x19)) (?v_32 (f0_1 x13)) (?v_84 (f0_2 x16 x26)) (?v_63 (f1_1 x15)) (?v_17 (f0_2 x3 x24)) (?v_15 (- (- (* 8 x21) (* 19 ?v_2)) (* 24 ?v_10))) (?v_11 (* 5 x19)) (?v_139 (* 14 x13)) (?v_164 (f0_1 x6)) (?v_110 (f1_2 ?v_7 x2))) (let ((?v_147 (- (- (* 29 x1) (* 19 x7)) (* 12 ?v_17))) (?v_45 (f1_1 x12)) (?v_129 (f0_2 x7 x7)) (?v_149 (f0_1 x5)) (?v_26 (f1_2 x0 x23)) (?v_169 (* 27 x16)) (?v_21 (+ (- (* 16 x29) (* 6 x14)) (* 4 x2))) (?v_52 (f0_2 x22 x0))) (let ((?v_245 (f0_2 ?v_129 x17)) (?v_3 (f0_1 ?v_15)) (?v_322 (= x13 ?v_52))) (let ((?v_371 (< ?v_245 27)) (?v_313 (< x19 10)) (?v_20 (= (f1_2 x29 x2) x23)) (?v_50 (< x24 23)) (?v_192 (< x13 26)) (?v_96 (< ?v_52 10)) (?v_34 (< ?v_2 11)) (?v_319 (< x0 16)) (?v_235 (= x4 x18)) (?v_172 (< ?v_76 21)) (?v_18 (< ?v_10 4)) (?v_296 (< ?v_2 27)) (?v_87 (< x5 1)) (?v_232 (= x2 x6)) (?v_102 (< x27 14)) (?v_85 (< (- (- (* 7 x6) (* 26 x27)) (* 3 x16)) 25)) (?v_291 (= ?v_282 ?v_16)) (?v_186 (< x21 0)) (?v_193 (= ?v_84 x27)) (?v_287 (< x22 26)) (?v_106 (= ?v_21 ?v_3)) (?v_131 (< ?v_110 11)) (?v_128 (< ?v_0 7)) (?v_148 (< ?v_3 10)) (?v_104 (< ?v_70 4)) (?v_75 (= (f0_2 x21 x24) x25)) (?v_90 (< x20 12)) (?v_261 (< ?v_52 29)) (?v_350 (< ?v_16 0)) (?v_209 (= x21 x28)) (?v_74 (= x9 ?v_3)) (?v_244 (< (f1_2 x6 x20) 9)) (?v_321 (= ?v_10 x10)) (?v_339 (< ?v_64 23)) (?v_174 (< ?v_26 27)) (?v_160 (= x8 ?v_76)) (?v_328 (< x13 15)) (?v_222 (< ?v_0 10)) (?v_69 (< ?v_13 15)) (?v_196 (= ?v_2 x3)) (?v_171 (< ?v_17 29)) (?v_195 (< ?v_129 4)) (?v_40 (< ?v_164 19)) (?v_80 (< ?v_21 8)) (?v_295 (= ?v_64 ?v_282)) (?v_122 (< (+ (- ?v_36 (* 9 ?v_110)) (* 28 ?v_13)) 19)) (?v_92 (< ?v_0 28)) (?v_136 (< x22 1)) (?v_167 (= x1 x15)) (?v_229 (< ?v_164 21)) (?v_158 (< ?v_76 2)) (?v_103 (< ?v_2 4))) (let ((?v_31 (not ?v_87)) (?v_234 (not ?v_40)) (?v_278 (not ?v_186)) (?v_81 (not ?v_174)) (?v_30 (not P22)) (?v_293 (not ?v_192)) (?v_258 (not ?v_92)) (?v_41 (not ?v_18)) (?v_88 (not ?v_313)) (?v_279 (not ?v_148)) (?v_29 (not ?v_350)) (?v_301 (not P7)) (?v_117 (not P18)) (?v_271 (not ?v_50)) (?v_188 (not P12)) (?v_161 (not ?v_287)) (?v_48 (not ?v_34)) (?v_67 (not P10)) (?v_241 (not ?v_74)) (?v_51 (not P17)) (?v_253 (not P27)) (?v_200 (not ?v_261)) (?v_251 (not ?v_104)) (?v_263 (not P6)) (?v_227 (not P15)) (?v_201 (not ?v_339)) (?v_98 (not ?v_69)) (?v_306 (not P21)) (?v_156 (not ?v_296)) (?v_113 (not ?v_222)) (?v_82 (not ?v_160)) (?v_135 (not P24)) (?v_325 (not P23)) (?v_324 (not P11)) (?v_223 (not ?v_90)) (?v_108 (not ?v_96)) (?v_162 (not ?v_209)) (?v_170 (not ?v_102)) (?v_184 (not ?v_106)) (?v_284 (not ?v_122)) (?v_132 (not P13)) (?v_327 (not ?v_319)) (?v_146 (not P25)) (?v_289 (not ?v_196)) (?v_338 (not ?v_322)) (?v_159 (not P19)) (?v_220 (not ?v_128)) (?v_305 (not ?v_136)) (?v_272 (not ?v_229)) (?v_257 (not ?v_171)) (?v_329 (not ?v_172)) (?v_283 (not P5)) (?v_264 (not P28)) (?v_231 (not ?v_193)) (?v_368 (not ?v_75)) (?v_331 (not P8)) (?v_308 (not ?v_20)) (?v_275 (not P1)) (?v_269 (not P4)) (?v_285 (not P2)) (?v_292 (not ?v_371)) (?v_281 (not P20)) (?v_318 (not ?v_328)) (?v_300 (not P26)) (?v_286 (not P14)) (?v_353 (not ?v_167)) (?v_314 (not P0)) (?v_304 (not ?v_235)) (?v_310 (not ?v_195)) (?v_316 (not P3)) (?v_334 (not ?v_80)) (?v_359 (not ?v_295)) (?v_345 (not ?v_103)) (?v_367 (not ?v_232)) (?v_365 (not P29)) (?v_366 (not ?v_244)) (?v_28 (+ (* 19 x16) (* 9 x22) (* 12 x21)))) (let ((?v_9 (- (+ (* 2 ?v_28) (* 7 ?v_1)) (* 28 x27))) (?v_68 (+ (* 18 x7) (* 27 x19) (* 27 x24)))) (let ((?v_250 (= ?v_7 (- (+ (* 9 ?v_68) (* 2 x26)) (* 13 x13))))) (let ((?v_43 (not ?v_250)) (?v_56 (+ (- (* 7 x3) (* 8 x22)) x18))) (let ((?v_24 (< ?v_56 12)) (?v_191 (< (+ (* 6 (f0_2 (f0_2 x6 x19) (f0_1 ?v_9))) (* 10 ?v_2) (* 20 x27)) 4))) (let ((?v_218 (not ?v_191)) (?v_49 (not ?v_24)) (?v_138 (< ?v_28 17))) (let ((?v_95 (not ?v_138)) (?v_100 (- (+ (* 11 ?v_9) (* 8 ?v_147)) (* 11 x13))) (?v_178 (= (f1_2 (f0_1 (- (+ (* 14 x24) (* 11 x22)) (* 22 x16))) ?v_13) ?v_28))) (let ((?v_240 (not ?v_178)) (?v_183 (< (+ (* 6 x20) ?v_169 (* 6 x7)) 17))) (let ((?v_349 (not ?v_183)) (?v_4 (+ (- (* (- 1) x29) (* 10 x24)) (* 7 x1)))) (let ((?v_8 (+ (- (* (- 12) x27) (* 8 ?v_84)) (* 7 ?v_4)))) (let ((?v_249 (< ?v_8 27))) (let ((?v_134 (not ?v_249)) (?v_315 (< ?v_1 (- 10))) (?v_59 (< ?v_0 (- 2)))) (let ((?v_335 (not ?v_59)) (?v_78 (+ (* (- 17) x26) ?v_11 (* 17 x28))) (?v_14 (f0_2 (- (+ (* (- 5) x8) (* 26 x4)) (* 22 x26)) ?v_16))) (let ((?v_25 (+ (* 4 ?v_78) (* 24 ?v_14) (* 2 ?v_17)))) (let ((?v_224 (= ?v_25 ?v_9))) (let ((?v_97 (not ?v_224)) (?v_79 (- (+ (* (- 22) x6) (* 18 x22)) (* 19 x11)))) (let ((?v_107 (= ?v_3 ?v_79)) (?v_5 (< ?v_4 22)) (?v_208 (< ?v_6 (- 1))) (?v_47 (< ?v_6 (- 20))) (?v_114 (< (- (+ (* (- 22) x16) (* 9 x19)) ?v_139) 17))) (let ((?v_12 (not ?v_114)) (?v_46 (< ?v_8 9))) (let ((?v_101 (not ?v_46)) (?v_42 (< x18 (- 16)))) (let ((?v_185 (not ?v_42)) (?v_255 (< ?v_2 (- 3))) (?v_38 (- (+ (* (- 22) ?v_9) (* 15 ?v_10)) ?v_11))) (let ((?v_202 (= ?v_38 (f1_2 x16 x11))) (?v_35 (< (f0_1 x4) (- 20)))) (let ((?v_112 (not ?v_35)) (?v_124 (- (- (* (- 17) x28) (* 29 x27)) (* 5 x24)))) (let ((?v_332 (< ?v_124 29))) (let ((?v_145 (not ?v_332)) (?v_121 (< ?v_10 (- 26)))) (let ((?v_83 (not ?v_121)) (?v_99 (< ?v_13 (- 8))) (?v_19 (+ (- (* 3 ?v_14) (* 16 ?v_15)) (* 20 x25)))) (let ((?v_212 (< ?v_19 10))) (let ((?v_230 (not ?v_212)) (?v_77 (< ?v_16 (- 11))) (?v_55 (< ?v_16 (- 22))) (?v_33 (< x24 (- 19))) (?v_330 (< (+ (- (* (- 27) ?v_76) (* 14 ?v_64)) (* 8 x13)) 9))) (let ((?v_143 (not ?v_330)) (?v_22 (+ (- (* (- 24) x1) (* 6 x21)) (* 7 x2)))) (let ((?v_60 (= (f0_1 x11) ?v_22)) (?v_23 (+ (* (- 5) x18) (* 27 ?v_45) (* 26 ?v_63)))) (let ((?v_53 (< ?v_23 18)) (?v_73 (< ?v_19 (- 11))) (?v_58 (< x23 (- 13)))) (let ((?v_86 (not ?v_58)) (?v_61 (< x10 (- 13)))) (let ((?v_116 (not ?v_61)) (?v_177 (+ (- (* (- 15) x11) (* 29 x4)) (* 21 x27)))) (let ((?v_62 (= (+ (- (* 21 x26) ?v_169) (* 16 x4)) ?v_177)) (?v_111 (< ?v_10 (- 14)))) (let ((?v_242 (not ?v_111)) (?v_27 (< ?v_22 21)) (?v_57 (< ?v_23 7))) (let ((?v_44 (not ?v_57)) (?v_194 (< (f0_1 x0) (- 23)))) (let ((?v_299 (not ?v_194)) (?v_233 (< ?v_25 (- 9))) (?v_180 (< (+ (* (- 6) ?v_1) (* 21 ?v_14) ?v_26) 24)) (?v_91 (= ?v_282 ?v_19))) (let ((?v_214 (not ?v_91)) (?v_66 (< ?v_32 (- 18)))) (let ((?v_216 (not ?v_66)) (?v_37 (< ?v_8 (- 15)))) (let ((?v_123 (not ?v_37)) (?v_243 (< ?v_32 (- 17))) (?v_65 (< x22 (- 15))) (?v_274 (< x1 (- 29)))) (let ((?v_340 (not ?v_274)) (?v_39 (< ?v_52 (- 20)))) (let ((?v_126 (not ?v_39)) (?v_54 (< (- (+ (* (- 14) x6) (* 19 x29)) (* 13 x7)) (- 16))) (?v_71 (+ (* (- 19) x22) ?v_36 (* 6 x19)))) (let ((?v_115 (< (f1_2 x12 ?v_71) (- 16)))) (let ((?v_210 (not ?v_115)) (?v_190 (< ?v_38 (- 7)))) (let ((?v_360 (not ?v_190)) (?v_246 (= ?v_6 (+ (* (- 6) x25) (* 15 x16) (* 6 x9)))) (?v_155 (< x11 (- 25))) (?v_260 (< ?v_45 (- 10))) (?v_225 (not ?v_47)) (?v_94 (< x25 (- 19))) (?v_179 (< x12 (- 14))) (?v_153 (< (f1_2 ?v_14 (f1_1 (f0_2 x27 x25))) 11))) (let ((?v_72 (not ?v_153)) (?v_298 (not ?v_54)) (?v_369 (not ?v_55)) (?v_187 (< x0 (- 20)))) (let ((?v_333 (not ?v_187)) (?v_142 (+ (* 7 (f1_2 x19 x19)) (* 7 ?v_23) (* 21 ?v_56)))) (let ((?v_120 (= ?v_100 ?v_142))) (let ((?v_173 (not ?v_120)) (?v_226 (= ?v_0 ?v_25))) (let ((?v_204 (not ?v_226)) (?v_252 (not ?v_60)) (?v_176 (< x11 (- 7))) (?v_109 (- (- (* (- 19) x9) (* 20 ?v_63)) (* 3 x6)))) (let ((?v_219 (< ?v_109 2))) (let ((?v_137 (not ?v_219)) (?v_303 (not ?v_65)) (?v_217 (< ?v_68 (- 10))) (?v_133 (< ?v_70 (- 20)))) (let ((?v_93 (not ?v_133)) (?v_127 (< ?v_71 (- 3))) (?v_168 (= (+ (* (- 17) ?v_78) (* 23 ?v_17) (* 14 x0)) ?v_79)) (?v_290 (not ?v_73)) (?v_262 (< x27 (- 22)))) (let ((?v_89 (not ?v_262)) (?v_165 (< ?v_149 (- 5))) (?v_105 (< ?v_25 25)) (?v_150 (< ?v_78 (- 1))) (?v_207 (< ?v_45 (- 25))) (?v_189 (+ (- (* (- 29) x1) (* 5 ?v_84)) (* 19 ?v_16)))) (let ((?v_197 (= ?v_2 ?v_189))) (let ((?v_154 (not ?v_197)) (?v_265 (< ?v_0 (- 25))) (?v_163 (< (+ (* (- 9) x19) (* 17 x1) (* 15 x9)) (- 7)))) (let ((?v_302 (not ?v_163)) (?v_268 (not ?v_99)) (?v_198 (< ?v_100 (- 24))) (?v_125 (not ?v_105)) (?v_119 (< ?v_0 (- 10))) (?v_130 (not ?v_107)) (?v_140 (< ?v_109 (- 11))) (?v_206 (< (f0_2 ?v_15 ?v_76) (- 18))) (?v_118 (= x7 (- (+ (* (- 14) x22) (* 27 x21)) (* 15 x25)))) (?v_152 (< (+ (- (* (- 22) x5) (* 12 x12)) (* 27 x9)) (- 5)))) (let ((?v_141 (not ?v_152)) (?v_205 (not ?v_119)) (?v_199 (< ?v_124 24))) (let ((?v_336 (not ?v_199)) (?v_326 (< ?v_245 (- 14)))) (let ((?v_347 (not ?v_326)) (?v_144 (not ?v_62)) (?v_166 (= ?v_23 (+ ?v_139 (* 7 x9) (* 6 x18)))) (?v_181 (< ?v_22 (- 9))) (?v_221 (< ?v_142 (- 5))) (?v_157 (< ?v_26 (- 16))) (?v_294 (< ?v_147 (- 26))) (?v_211 (< ?v_149 (- 14)))) (let ((?v_358 (not ?v_211)) (?v_239 (not ?v_150)) (?v_355 (< ?v_151 (- 7)))) (let ((?v_323 (not ?v_355)) (?v_277 (not ?v_27)) (?v_247 (not ?v_157)) (?v_175 (not ?v_165)) (?v_270 (< ?v_38 (- 24)))) (let ((?v_215 (not ?v_270)) (?v_182 (< ?v_177 (- 15))) (?v_254 (not ?v_140)) (?v_267 (not ?v_181))) (let ((?v_248 (not ?v_182)) (?v_238 (< x18 (- 25)))) (let ((?v_237 (not ?v_238)) (?v_276 (not ?v_166)) (?v_228 (< x28 (- 23))) (?v_213 (= (f0_1 x28) ?v_189))) (let ((?v_307 (not ?v_213)) (?v_203 (not ?v_179)) (?v_309 (not ?v_168)) (?v_256 (< ?v_13 (- 23)))) (let ((?v_266 (not ?v_256)) (?v_344 (not ?v_53)) (?v_363 (not ?v_217)) (?v_236 (not ?v_77)) (?v_343 (not ?v_228)) (?v_342 (not ?v_233)) (?v_311 (not ?v_246)) (?v_259 (not ?v_94)) (?v_273 (not ?v_206)) (?v_357 (not ?v_255)) (?v_341 (not ?v_265)) (?v_372 (not ?v_176)) (?v_337 (not ?v_5)) (?v_288 (= x22 ?v_142)) (?v_280 (not ?v_33)) (?v_297 (not ?v_243)) (?v_312 (not ?v_260)) (?v_320 (not ?v_294)) (?v_356 (not ?v_155)) (?v_317 (= ?v_78 ?v_0)) (?v_351 (not ?v_198))) (let ((?v_348 (not ?v_288)) (?v_361 (not ?v_180)) (?v_362 (not ?v_208)) (?v_354 (not ?v_315)) (?v_352 (not ?v_221)) (?v_346 (not ?v_207)) (?v_370 (not ?v_202)) (?v_364 (not ?v_118))) (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 (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 (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 (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 (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 (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 (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 (or (or ?v_75 ?v_128) ?v_31) (or (or ?v_134 ?v_315) ?v_122)) (or (or ?v_335 ?v_34) ?v_97)) (or (or ?v_106 ?v_107) P8)) (or (or ?v_5 ?v_5) ?v_234)) (or (or ?v_20 ?v_278) ?v_81)) (or (or ?v_30 ?v_293) ?v_208)) (or (or ?v_47 ?v_12) P22)) (or (or ?v_43 ?v_101) ?v_185)) (or (or ?v_255 ?v_202) P19)) (or (or ?v_112 ?v_145) ?v_85)) (or (or ?v_83 ?v_258) ?v_41)) (or (or ?v_12 ?v_24) ?v_218)) (or (or ?v_99 ?v_230) ?v_77)) (or (or ?v_55 ?v_33) ?v_88)) (or (or ?v_171 ?v_143) ?v_18)) (or (or ?v_60 ?v_279) ?v_29)) (or (or ?v_53 ?v_73) ?v_86)) (or (or ?v_20 ?v_116) ?v_62)) (or (or ?v_242 ?v_80) ?v_27)) (or (or P16 ?v_44) ?v_49)) (or (or P8 ?v_299) ?v_301)) (or (or ?v_117 ?v_233) ?v_180)) (or (or P15 ?v_27) ?v_195)) (or (or ?v_214 ?v_95) ?v_216)) (or (or ?v_29 ?v_271) ?v_188)) (or (or ?v_123 ?v_30) ?v_31)) (or (or P22 ?v_31) ?v_90)) (or (or ?v_243 ?v_65) ?v_33)) (or (or ?v_161 ?v_48) ?v_340)) (or (or ?v_126 ?v_54) ?v_67)) (or (or ?v_103 ?v_102) ?v_35)) (or (or ?v_210 ?v_37) ?v_360)) (or (or ?v_241 ?v_39) ?v_246)) (or (or ?v_51 ?v_40) ?v_41)) (or (or ?v_37 ?v_42) ?v_43)) (or (or ?v_155 ?v_44) ?v_260)) (or (or P11 ?v_46) ?v_225)) (or (or ?v_48 ?v_94) P3)) (or (or ?v_179 ?v_253) ?v_49)) (or (or ?v_50 ?v_51) ?v_96)) (or (or ?v_72 ?v_53) ?v_298)) (or (or ?v_369 P23) ?v_200)) (or (or ?v_333 ?v_173) ?v_251)) (or (or ?v_57 ?v_69) ?v_58)) (or (or ?v_263 ?v_204) ?v_59)) (or (or ?v_252 P10) ?v_61)) (or (or ?v_227 ?v_62) ?v_176)) (or (or ?v_137 ?v_201) ?v_5)) (or (or ?v_303 ?v_66) ?v_67)) (or (or ?v_217 P26) ?v_98)) (or (or ?v_93 ?v_127) ?v_306)) (or (or ?v_72 ?v_73) ?v_74)) (or (or ?v_75 ?v_156) ?v_33)) (or (or ?v_113 ?v_82) ?v_58)) (or (or ?v_74 ?v_58) ?v_77)) (or (or ?v_135 ?v_168) ?v_325)) (or (or ?v_80 P1) ?v_324)) (or (or ?v_290 ?v_67) ?v_81)) (or (or P24 ?v_89) ?v_82)) (or (or ?v_165 ?v_83) ?v_37)) (or (or ?v_321 ?v_105) ?v_150)) (or (or ?v_193 P1) ?v_85)) (or (or ?v_86 ?v_244) ?v_87)) (or (or ?v_207 ?v_88) ?v_89)) (or (or ?v_90 ?v_167) ?v_91)) (or (or ?v_154 ?v_223) ?v_92)) (or (or ?v_265 ?v_93) ?v_302)) (or (or ?v_83 ?v_94) ?v_95)) (or (or ?v_108 ?v_97) ?v_82)) (or (or ?v_98 P23) ?v_162)) (or (or ?v_268 ?v_198) ?v_27)) (or (or P25 ?v_101) ?v_170)) (or (or ?v_103 ?v_104) ?v_125)) (or (or ?v_119 ?v_158) ?v_33)) (or (or ?v_99 P24) P7)) (or (or P5 P13) ?v_184)) (or (or ?v_53 ?v_130) ?v_108)) (or (or ?v_136 ?v_140) ?v_131)) (or (or ?v_58 ?v_111) ?v_112)) (or (or ?v_113 ?v_206) P5)) (or (or ?v_114 ?v_240) ?v_115)) (or (or ?v_80 ?v_116) ?v_103)) (or (or ?v_85 ?v_101) ?v_112)) (or (or ?v_117 ?v_118) ?v_65)) (or (or ?v_118 ?v_141) ?v_205)) (or (or ?v_120 ?v_12) ?v_121)) (or (or ?v_104 ?v_284) ?v_123)) (or (or ?v_336 ?v_125) ?v_132)) (or (or ?v_112 ?v_126) ?v_67)) (or (or ?v_127 ?v_74) ?v_128)) (or (or ?v_347 ?v_327) P0)) (or (or ?v_130 ?v_131) P9)) (or (or ?v_132 ?v_133) ?v_134)) (or (or ?v_135 ?v_144) P0)) (or (or ?v_136 ?v_81) ?v_137)) (or (or P15 P20) ?v_235)) (or (or ?v_146 ?v_138) ?v_166)) (or (or ?v_140 ?v_141) ?v_181)) (or (or ?v_221 ?v_232) ?v_96)) (or (or ?v_143 ?v_289) ?v_338)) (or (or P10 ?v_144) P23)) (or (or ?v_131 ?v_90) ?v_49)) (or (or ?v_145 ?v_146) ?v_157)) (or (or ?v_127 ?v_143) ?v_294)) (or (or ?v_77 ?v_148) ?v_89)) (or (or ?v_358 ?v_239) ?v_159)) (or (or ?v_220 ?v_323) ?v_144)) (or (or ?v_42 ?v_152) ?v_103)) (or (or ?v_277 ?v_153) P12)) (or (or ?v_93 ?v_154) ?v_155)) (or (or P7 ?v_98) ?v_103)) (or (or ?v_156 ?v_69) ?v_152)) (or (or P19 P22) ?v_65)) (or (or P14 ?v_5) ?v_247)) (or (or ?v_75 ?v_157) ?v_158)) (or (or ?v_159 ?v_160) ?v_305)) (or (or ?v_161 ?v_162) ?v_163)) (or (or ?v_272 ?v_29) ?v_96)) (or (or ?v_175 ?v_215) ?v_166)) (or (or ?v_167 ?v_172) ?v_168)) (or (or ?v_183 ?v_170) ?v_257)) (or (or (not P9) ?v_329) ?v_42)) (or (or ?v_173 ?v_174) ?v_175)) (or (or ?v_158 ?v_176) ?v_182)) (or (or ?v_254 ?v_283) ?v_178)) (or (or ?v_95 ?v_179) ?v_180)) (or (or ?v_267 ?v_248) ?v_161)) (or (or ?v_183 P20) ?v_67)) (or (or ?v_184 ?v_116) ?v_237)) (or (or P10 ?v_29) ?v_185)) (or (or ?v_91 ?v_83) ?v_27)) (or (or ?v_60 ?v_51) ?v_113)) (or (or ?v_132 ?v_39) ?v_60)) (or (or ?v_35 ?v_113) P8)) (or (or ?v_276 ?v_113) ?v_148)) (or (or ?v_157 ?v_186) ?v_125)) (or (or ?v_228 ?v_187) ?v_188)) (or (or ?v_307 ?v_264) ?v_190)) (or (or ?v_191 P7) ?v_171)) (or (or ?v_192 ?v_231) ?v_368)) (or (or ?v_331 ?v_194) P20)) (or (or ?v_195 ?v_35) ?v_196)) (or (or ?v_203 ?v_83) ?v_148)) (or (or ?v_44 P12) ?v_98)) (or (or ?v_308 ?v_197) ?v_198)) (or (or ?v_199 ?v_112) ?v_87)) (or (or ?v_309 ?v_141) ?v_67)) (or (or ?v_184 ?v_200) ?v_180)) (or (or ?v_201 ?v_50) P3)) (or (or ?v_275 ?v_182) ?v_185)) (or (or P1 ?v_42) ?v_202)) (or (or ?v_269 ?v_203) ?v_196)) (or (or ?v_57 ?v_204) ?v_205)) (or (or ?v_206 P25) ?v_127)) (or (or ?v_207 ?v_208) ?v_209)) (or (or ?v_210 ?v_266) ?v_211)) (or (or ?v_46 ?v_188) ?v_212)) (or (or ?v_165 ?v_103) ?v_213)) (or (or ?v_112 ?v_73) ?v_214)) (or (or ?v_175 ?v_44) ?v_215)) (or (or ?v_344 ?v_69) P18)) (or (or ?v_216 ?v_49) P3)) (or (or ?v_108 ?v_363) ?v_106)) (or (or ?v_200 ?v_179) ?v_218)) (or (or ?v_218 ?v_212) ?v_219)) (or (or ?v_201 ?v_58) ?v_220)) (or (or ?v_175 ?v_221) ?v_236)) (or (or ?v_222 ?v_223) ?v_224)) (or (or ?v_225 ?v_226) ?v_227)) (or (or ?v_132 ?v_343) ?v_229)) (or (or ?v_125 ?v_99) ?v_146)) (or (or ?v_41 ?v_69) P26)) (or (or ?v_55 ?v_106) ?v_230)) (or (or ?v_86 ?v_231) ?v_182)) (or (or ?v_232 P14) ?v_34)) (or (or ?v_117 ?v_342) ?v_114)) (or (or ?v_234 ?v_235) ?v_120)) (or (or ?v_236 ?v_175) ?v_127)) (or (or ?v_65 ?v_218) ?v_211)) (or (or ?v_57 ?v_165) ?v_46)) (or (or ?v_237 ?v_238) ?v_182)) (or (or ?v_47 ?v_37) ?v_176)) (or (or ?v_143 ?v_239) ?v_240)) (or (or ?v_241 ?v_194) ?v_117)) (or (or ?v_114 ?v_152) P22)) (or (or ?v_171 P29) ?v_168)) (or (or ?v_242 ?v_115) ?v_243)) (or (or ?v_285 ?v_244) P1)) (or (or ?v_292 ?v_153) ?v_181)) (or (or ?v_311 ?v_107) ?v_122)) (or (or ?v_170 ?v_247) ?v_259)) (or (or ?v_248 ?v_249) ?v_273)) (or (or ?v_250 ?v_133) P21)) (or (or ?v_195 P11) ?v_86)) (or (or P21 ?v_173) ?v_182)) (or (or ?v_242 ?v_251) ?v_77)) (or (or ?v_252 ?v_253) ?v_244)) (or (or ?v_41 P11) P21)) (or (or ?v_160 ?v_116) ?v_224)) (or (or ?v_198 ?v_254) ?v_92)) (or (or ?v_224 ?v_357) ?v_256)) (or (or P21 ?v_281) ?v_248)) (or (or ?v_247 ?v_72) ?v_257)) (or (or ?v_230 ?v_318) ?v_54)) (or (or ?v_258 ?v_27) ?v_259)) (or (or ?v_260 ?v_172) ?v_128)) (or (or ?v_154 ?v_261) ?v_262)) (or (or ?v_263 ?v_223) ?v_264)) (or (or ?v_220 ?v_186) ?v_135)) (or (or ?v_116 ?v_114) ?v_42)) (or (or ?v_159 P29) ?v_144)) (or (or ?v_341 ?v_214) ?v_156)) (or (or ?v_75 ?v_266) ?v_267)) (or (or ?v_233 ?v_173) ?v_241)) (or (or ?v_268 ?v_106) ?v_224)) (or (or ?v_260 ?v_152) ?v_269)) (or (or ?v_300 ?v_113) ?v_166)) (or (or ?v_270 P12) ?v_219)) (or (or ?v_91 ?v_286) ?v_193)) (or (or ?v_265 ?v_271) P2)) (or (or P29 ?v_103) ?v_372)) (or (or ?v_272 ?v_337) ?v_217)) (or (or ?v_135 ?v_58) ?v_181)) (or (or ?v_97 ?v_85) ?v_273)) (or (or ?v_288 ?v_241) ?v_202)) (or (or ?v_175 ?v_280) ?v_274)) (or (or ?v_41 ?v_163) ?v_231)) (or (or ?v_275 ?v_103) ?v_99)) (or (or ?v_126 ?v_152) ?v_252)) (or (or P25 ?v_157) ?v_264)) (or (or ?v_83 ?v_180) ?v_219)) (or (or ?v_113 ?v_67) ?v_276)) (or (or ?v_213 ?v_144) ?v_262)) (or (or ?v_118 ?v_256) ?v_353)) (or (or ?v_91 P19) ?v_51)) (or (or ?v_94 ?v_72) ?v_105)) (or (or ?v_277 ?v_278) P19)) (or (or ?v_218 ?v_29) ?v_236)) (or (or ?v_279 ?v_280) ?v_86)) (or (or ?v_115 ?v_266) ?v_273)) (or (or ?v_179 (not P16)) ?v_181)) (or (or ?v_281 P3) ?v_42)) (or (or ?v_75 ?v_107) ?v_43)) (or (or ?v_35 ?v_291) ?v_283)) (or (or ?v_258 ?v_284) ?v_77)) (or (or ?v_285 ?v_295) ?v_125)) (or (or ?v_186 ?v_108) ?v_134)) (or (or ?v_143 ?v_286) ?v_287)) (or (or ?v_60 ?v_288) P3)) (or (or ?v_289 ?v_89) P22)) (or (or ?v_290 P16) ?v_65)) (or (or ?v_291 ?v_297) ?v_127)) (or (or ?v_20 ?v_163) ?v_118)) (or (or ?v_141 ?v_292) ?v_293)) (or (or ?v_98 ?v_312) ?v_108)) (or (or ?v_320 ?v_246) ?v_191)) (or (or ?v_295 ?v_51) ?v_207)) (or (or ?v_215 ?v_61) ?v_72)) (or (or ?v_296 ?v_72) ?v_215)) (or (or ?v_349 ?v_297) ?v_314)) (or (or ?v_304 ?v_298) ?v_202)) (or (or ?v_146 ?v_125) ?v_29)) (or (or ?v_193 ?v_257) ?v_42)) (or (or ?v_112 ?v_273) ?v_50)) (or (or ?v_275 ?v_299) P8)) (or (or ?v_53 P17) ?v_300)) (or (or ?v_159 ?v_356) ?v_178)) (or (or ?v_97 ?v_98) P23)) (or (or ?v_278 ?v_161) ?v_41)) (or (or ?v_301 ?v_302) ?v_259)) (or (or ?v_263 ?v_249) ?v_264)) (or (or P2 ?v_69) ?v_303)) (or (or ?v_251 ?v_231) ?v_148)) (or (or ?v_304 ?v_67) ?v_305)) (or (or ?v_247 ?v_51) ?v_310)) (or (or ?v_306 ?v_204) ?v_90)) (or (or ?v_156 ?v_37) ?v_247)) (or (or P20 ?v_211) ?v_317)) (or (or ?v_131 ?v_307) ?v_256)) (or (or ?v_41 ?v_308) ?v_309)) (or (or ?v_148 ?v_108) ?v_133)) (or (or ?v_305 ?v_316) ?v_167)) (or (or ?v_305 P23) ?v_144)) (or (or ?v_334 ?v_66) ?v_207)) (or (or ?v_239 ?v_161) P23)) (or (or ?v_116 ?v_31) ?v_310)) (or (or ?v_237 ?v_24) ?v_235)) (or (or ?v_154 ?v_224) ?v_44)) (or (or ?v_86 ?v_292) ?v_260)) (or (or ?v_155 ?v_311) P17)) (or (or ?v_186 ?v_239) ?v_156)) (or (or ?v_312 P2) ?v_297)) (or (or ?v_210 ?v_285) ?v_351)) (or (or ?v_297 ?v_283) ?v_66)) (or (or ?v_111 ?v_115) ?v_313)) (or (or ?v_314 ?v_209) ?v_243)) (or (or ?v_315 ?v_180) ?v_308)) (or (or ?v_241 P27) ?v_316)) (or (or ?v_126 ?v_231) ?v_199)) (or (or ?v_192 ?v_101) ?v_258)) (or (or ?v_172 ?v_310) ?v_154)) (or (or ?v_298 ?v_161) ?v_106)) (or (or ?v_74 ?v_264) ?v_225)) (or (or ?v_348 ?v_263) P26)) (or (or ?v_118 ?v_317) ?v_318)) (or (or ?v_211 ?v_131) ?v_359)) (or (or P22 ?v_319) ?v_320)) (or (or ?v_271 ?v_66) P13)) (or (or ?v_153 ?v_93) ?v_241)) (or (or ?v_159 ?v_166) ?v_62)) (or (or ?v_102 ?v_256) ?v_321)) (or (or ?v_172 ?v_61) (not ?v_158))) (or (or ?v_50 ?v_153) (not ?v_131))) (or (or ?v_123 ?v_97) ?v_246)) (or (or ?v_50 ?v_118) ?v_322)) (or (or ?v_220 ?v_191) ?v_323)) (or (or ?v_324 ?v_171) ?v_244)) (or (or ?v_281 P14) ?v_257)) (or (or ?v_325 ?v_99) ?v_326)) (or (or ?v_271 ?v_319) P9)) (or (or ?v_201 ?v_254) ?v_165)) (or (or ?v_300 ?v_306) ?v_191)) (or (or ?v_224 ?v_361) ?v_197)) (or (or ?v_83 ?v_119) ?v_106)) (or (or ?v_272 ?v_327) ?v_168)) (or (or ?v_184 ?v_248) ?v_362)) (or (or ?v_328 P23) ?v_104)) (or (or ?v_201 ?v_102) ?v_345)) (or (or ?v_217 ?v_207) ?v_225)) (or (or ?v_329 ?v_159) P23)) (or (or ?v_330 ?v_188) ?v_24)) (or (or ?v_59 ?v_179) ?v_272)) (or (or ?v_187 ?v_291) ?v_237)) (or (or ?v_40 ?v_242) ?v_67)) (or (or ?v_211 ?v_331) ?v_354)) (or (or ?v_159 ?v_332) ?v_24)) (or (or P27 ?v_111) ?v_163)) (or (or ?v_154 ?v_324) P26)) (or (or ?v_150 ?v_166) ?v_190)) (or (or ?v_250 ?v_73) ?v_314)) (or (or P11 ?v_260) ?v_290)) (or (or ?v_190 ?v_264) ?v_299)) (or (or ?v_323 ?v_77) ?v_96)) (or (or ?v_29 ?v_212) P23)) (or (or ?v_352 ?v_206) P14)) (or (or P2 ?v_333) ?v_312)) (or (or ?v_242 ?v_167) ?v_224)) (or (or ?v_148 ?v_334) ?v_257)) (or (or ?v_309 ?v_335) ?v_191)) (or (or ?v_107 ?v_254) ?v_299)) (or (or ?v_219 ?v_62) ?v_336)) (or (or ?v_98 ?v_337) ?v_221)) (or (or ?v_157 ?v_161) P4)) (or (or ?v_335 ?v_281) ?v_232)) (or (or ?v_94 ?v_200) ?v_108)) (or (or P6 ?v_159) ?v_27)) (or (or ?v_338 ?v_101) ?v_339)) (or (or ?v_331 ?v_340) ?v_102)) (or (or ?v_49 ?v_255) ?v_249)) (or (or ?v_331 ?v_134) ?v_309)) (or (or ?v_238 ?v_131) ?v_341)) (or (or ?v_342 ?v_199) ?v_39)) (or (or ?v_47 P6) ?v_159)) (or (or ?v_5 ?v_240) ?v_343)) (or (or ?v_258 P9) ?v_60)) (or (or ?v_123 ?v_328) ?v_107)) (or (or ?v_233 ?v_333) ?v_92)) (or (or ?v_284 ?v_161) ?v_346)) (or (or ?v_250 P6) ?v_176)) (or (or ?v_180 ?v_59) ?v_303)) (or (or ?v_344 ?v_121) ?v_254)) (or (or ?v_273 ?v_191) ?v_222)) (or (or ?v_345 ?v_176) ?v_144)) (or (or ?v_83 ?v_346) ?v_306)) (or (or ?v_347 ?v_73) ?v_265)) (or (or ?v_348 ?v_48) (not ?v_291))) (or (or ?v_279 ?v_349) ?v_242)) (or (or ?v_135 ?v_279) P26)) (or (or ?v_331 ?v_104) ?v_152)) (or (or ?v_93 ?v_215) ?v_350)) (or (or ?v_47 ?v_254) ?v_43)) (or (or ?v_227 ?v_234) P29)) (or (or ?v_260 ?v_195) ?v_69)) (or (or ?v_279 ?v_229) ?v_351)) (or (or ?v_352 ?v_256) ?v_271)) (or (or ?v_126 ?v_353) ?v_193)) (or (or ?v_231 ?v_81) ?v_137)) (or (or ?v_87 P8) ?v_259)) (or (or ?v_75 ?v_333) ?v_24)) (or (or ?v_250 ?v_196) ?v_284)) (or (or ?v_267 ?v_278) P28)) (or (or ?v_187 ?v_193) ?v_304)) (or (or ?v_131 ?v_303) ?v_152)) (or (or ?v_337 ?v_300) ?v_228)) (or (or ?v_30 ?v_182) ?v_86)) (or (or ?v_213 ?v_344) ?v_206)) (or (or ?v_211 P21) ?v_231)) (or (or ?v_275 P10) ?v_353)) (or (or ?v_300 ?v_119) ?v_236)) (or (or ?v_261 ?v_258) ?v_354)) (or (or ?v_367 ?v_355) P27)) (or (or ?v_305 ?v_246) ?v_115)) (or (or ?v_300 ?v_345) ?v_18)) (or (or ?v_237 ?v_183) ?v_150)) (or (or ?v_29 ?v_167) P10)) (or (or ?v_192 ?v_332) ?v_348)) (or (or ?v_55 ?v_324) ?v_356)) (or (or ?v_50 ?v_65) ?v_199)) (or (or ?v_334 ?v_107) ?v_210)) (or (or ?v_60 ?v_211) ?v_143)) (or (or ?v_192 ?v_134) ?v_126)) (or (or ?v_186 ?v_251) ?v_27)) (or (or ?v_157 ?v_217) ?v_231)) (or (or ?v_304 ?v_273) P23)) (or (or P3 ?v_296) ?v_133)) (or (or ?v_351 ?v_357) ?v_180)) (or (or ?v_62 ?v_320) ?v_59)) (or (or ?v_356 ?v_264) ?v_27)) (or (or ?v_335 ?v_116) ?v_125)) (or (or ?v_89 ?v_93) ?v_343)) (or (or ?v_316 ?v_27) ?v_358)) (or (or ?v_294 ?v_340) ?v_315)) (or (or ?v_119 ?v_325) ?v_66)) (or (or ?v_359 ?v_288) ?v_154)) (or (or ?v_334 ?v_108) ?v_185)) (or (or ?v_302 ?v_67) ?v_244)) (or (or ?v_115 ?v_302) ?v_229)) (or (or ?v_96 ?v_111) ?v_325)) (or (or ?v_354 ?v_300) ?v_33)) (or (or ?v_303 ?v_250) ?v_205)) (or (or ?v_347 ?v_18) ?v_350)) (or (or ?v_252 ?v_115) ?v_72)) (or (or ?v_50 ?v_184) ?v_365)) (or (or ?v_101 ?v_160) ?v_358)) (or (or ?v_202 ?v_304) ?v_254)) (or (or ?v_29 ?v_329) ?v_279)) (or (or ?v_359 ?v_81) ?v_219)) (or (or ?v_312 ?v_128) ?v_249)) (or (or P12 ?v_90) ?v_148)) (or (or ?v_127 ?v_218) ?v_210)) (or (or ?v_360 ?v_353) ?v_246)) (or (or ?v_236 ?v_346) ?v_137)) (or (or ?v_131 ?v_216) ?v_297)) (or (or ?v_307 ?v_66) ?v_5)) (or (or ?v_216 ?v_248) ?v_108)) (or (or ?v_59 ?v_182) ?v_208)) (or (or ?v_263 ?v_238) ?v_90)) (or (or ?v_339 ?v_200) ?v_180)) (or (or ?v_356 ?v_316) ?v_310)) (or (or ?v_309 ?v_227) ?v_133)) (or (or ?v_138 ?v_361) ?v_214)) (or (or ?v_18 P6) ?v_83)) (or (or P17 ?v_240) ?v_207)) (or (or ?v_150 ?v_269) ?v_310)) (or (or ?v_140 ?v_232) ?v_80)) (or (or ?v_306 ?v_338) ?v_158)) (or (or ?v_132 ?v_224) ?v_87)) (or (or ?v_201 ?v_193) ?v_113)) (or (or ?v_331 ?v_161) ?v_235)) (or (or ?v_218 ?v_132) ?v_81)) (or (or ?v_254 ?v_212) ?v_226)) (or (or ?v_72 ?v_59) P7)) (or (or ?v_194 P16) ?v_143)) (or (or ?v_97 ?v_33) P24)) (or (or ?v_268 ?v_226) ?v_255)) (or (or ?v_95 ?v_357) ?v_249)) (or (or ?v_96 ?v_345) ?v_207)) (or (or ?v_161 ?v_65) ?v_103)) (or (or ?v_224 ?v_172) ?v_287)) (or (or ?v_343 ?v_132) ?v_362)) (or (or ?v_360 ?v_146) ?v_276)) (or (or ?v_304 ?v_333) ?v_173)) (or (or ?v_200 ?v_342) ?v_226)) (or (or ?v_144 ?v_18) ?v_363)) (or (or ?v_267 ?v_198) ?v_360)) (or (or ?v_305 ?v_59) ?v_137)) (or (or ?v_187 ?v_370) ?v_227)) (or (or ?v_356 ?v_290) ?v_230)) (or (or ?v_57 (not ?v_85)) P22)) (or (or P6 P13) P3)) (or (or ?v_131 ?v_58) ?v_240)) (or (or P5 ?v_336) ?v_335)) (or (or ?v_233 ?v_55) ?v_37)) (or (or ?v_356 P17) ?v_269)) (or (or ?v_300 ?v_123) ?v_305)) (or (or ?v_325 ?v_256) ?v_31)) (or (or ?v_191 ?v_180) ?v_75)) (or (or ?v_188 ?v_187) ?v_231)) (or (or ?v_61 ?v_277) ?v_192)) (or (or P28 ?v_357) ?v_207)) (or (or ?v_159 P26) ?v_233)) (or (or ?v_312 ?v_232) ?v_329)) (or (or ?v_310 ?v_311) ?v_111)) (or (or ?v_167 ?v_58) ?v_309)) (or (or ?v_157 ?v_292) ?v_75)) (or (or ?v_39 ?v_237) ?v_208)) (or (or ?v_364 ?v_193) ?v_267)) (or (or ?v_128 ?v_278) ?v_298)) (or (or ?v_146 ?v_197) ?v_171)) (or (or ?v_37 ?v_137) ?v_67)) (or (or ?v_305 ?v_92) ?v_359)) (or (or ?v_364 ?v_278) ?v_111)) (or (or ?v_95 ?v_114) ?v_224)) (or (or ?v_235 ?v_264) ?v_218)) (or (or ?v_334 ?v_353) ?v_313)) (or (or ?v_187 P3) ?v_366)) (or (or ?v_162 ?v_148) ?v_365)) (or (or ?v_331 P24) ?v_336)) (or (or ?v_319 P17) ?v_347)) (or (or ?v_58 ?v_246) ?v_132)) (or (or ?v_181 ?v_341) ?v_314)) (or (or ?v_148 P23) ?v_132)) (or (or ?v_277 ?v_184) ?v_224)) (or (or ?v_59 ?v_90) ?v_131)) (or (or ?v_49 ?v_310) ?v_359)) (or (or ?v_213 P26) ?v_240)) (or (or ?v_186 ?v_244) ?v_133)) (or (or ?v_39 ?v_240) ?v_106)) (or (or ?v_321 ?v_274) ?v_259)) (or (or ?v_299 ?v_326) ?v_285)) (or (or P26 ?v_339) ?v_12)) (or (or ?v_27 ?v_75) ?v_54)) (or (or ?v_128 ?v_131) ?v_328)) (or (or ?v_247 ?v_305) ?v_112)) (or (or ?v_256 P8) ?v_107)) (or (or ?v_338 ?v_308) ?v_108)) (or (or ?v_115 ?v_196) ?v_135)) (or (or ?v_69 ?v_254) ?v_81)) (or (or ?v_12 ?v_303) ?v_219)) (or (or ?v_256 ?v_366) ?v_231)) (or (or P6 ?v_211) ?v_254)) (or (or ?v_231 ?v_367) ?v_134)) (or (or P26 ?v_121) ?v_316)) (or (or ?v_202 ?v_306) ?v_103)) (or (or ?v_113 P18) ?v_368)) (or (or ?v_272 ?v_24) ?v_20)) (or (or ?v_154 ?v_92) ?v_335)) (or (or ?v_342 ?v_161) P2)) (or (or ?v_254 ?v_343) ?v_40)) (or (or ?v_117 ?v_183) ?v_57)) (or (or ?v_81 ?v_361) ?v_369)) (or (or ?v_312 ?v_332) ?v_171)) (or (or ?v_342 ?v_280) ?v_344)) (or (or ?v_263 ?v_257) ?v_155)) (or (or ?v_47 ?v_320) ?v_234)) (or (or ?v_206 ?v_370) ?v_180)) (or (or ?v_61 ?v_239) ?v_137)) (or (or ?v_24 P14) ?v_211)) (or (or ?v_69 ?v_66) ?v_35)) (or (or ?v_235 ?v_94) ?v_179)) (or (or ?v_199 ?v_150) ?v_351)) (or (or ?v_238 ?v_358) ?v_312)) (or (or ?v_241 ?v_320) ?v_197)) (or (or ?v_206 ?v_94) ?v_227)) (or (or ?v_299 ?v_250) (not ?v_321))) (or (or ?v_118 ?v_208) ?v_173)) (or (or ?v_47 ?v_117) ?v_60)) (or (or ?v_46 ?v_163) ?v_113)) (or (or ?v_280 ?v_226) ?v_44)) (or (or ?v_302 ?v_108) ?v_102)) (or (or P0 ?v_247) ?v_33)) (or (or ?v_55 ?v_135) ?v_231)) (or (or ?v_47 ?v_65) ?v_361)) (or (or ?v_205 ?v_329) ?v_231)) (or (or ?v_284 ?v_5) ?v_178)) (or (or ?v_59 P1) ?v_30)) (or (or ?v_338 ?v_242) ?v_65)) (or (or ?v_214 ?v_114) ?v_131)) (or (or ?v_43 ?v_255) ?v_344)) (or (or ?v_302 ?v_335) P25)) (or (or P6 ?v_153) ?v_296)) (or (or ?v_321 ?v_371) ?v_132)) (or (or ?v_93 ?v_368) ?v_275)) (or (or ?v_338 ?v_290) ?v_98)) (or (or ?v_285 ?v_272) P7)) (or (or ?v_29 ?v_182) ?v_349)) (or (or ?v_352 ?v_103) ?v_37)) (or (or ?v_41 ?v_274) ?v_307)) (or (or ?v_365 ?v_222) ?v_59)) (or (or ?v_360 ?v_33) ?v_247)) (or (or ?v_204 ?v_320) ?v_306)) (or (or ?v_35 ?v_69) ?v_259)) (or (or ?v_188 ?v_198) ?v_163)) (or (or ?v_255 ?v_113) ?v_291)) (or (or ?v_221 ?v_114) ?v_30)) (or (or ?v_372 ?v_244) ?v_254)) (or (or ?v_277 ?v_290) ?v_185)) (or (or ?v_179 ?v_165) ?v_261)) (or (or ?v_74 ?v_310) ?v_255)) (or (or ?v_359 ?v_30) ?v_322)) (or (or ?v_335 ?v_125) ?v_183)) (or (or ?v_148 ?v_206) ?v_136)) (or (or ?v_311 ?v_92) ?v_298)) (or (or P2 ?v_362) ?v_364)) (or (or ?v_342 ?v_153) ?v_247)) (or (or ?v_295 ?v_313) P19)) (or (or ?v_86 ?v_299) ?v_48)) (or (or P19 ?v_339) ?v_144)) (or (or ?v_244 ?v_201) ?v_259)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)