clocksynchro_9clocks.main_invar.base.smt2

(set-info :smt-lib-version 2.6)
(set-logic QF_LRA)
(set-info :source | Clock Synchronization. Bruno Dutertre (bruno@csl.sri.com) |)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x_0 () Real)
(declare-fun x_1 () Real)
(declare-fun x_2 () Real)
(declare-fun x_3 () Real)
(declare-fun x_4 () Real)
(declare-fun x_5 () Real)
(declare-fun x_6 () Real)
(declare-fun x_7 () Real)
(declare-fun x_8 () Real)
(declare-fun x_9 () Real)
(declare-fun x_10 () Real)
(declare-fun x_11 () Real)
(declare-fun x_12 () Real)
(declare-fun x_13 () Real)
(declare-fun x_14 () Real)
(declare-fun x_15 () Real)
(declare-fun x_16 () Real)
(declare-fun x_17 () Real)
(declare-fun x_18 () Real)
(declare-fun x_19 () Real)
(declare-fun x_20 () Real)
(declare-fun x_21 () Real)
(declare-fun x_22 () Real)
(declare-fun x_23 () Real)
(declare-fun x_24 () Real)
(declare-fun x_25 () Real)
(declare-fun x_26 () Real)
(declare-fun x_27 () Real)
(declare-fun x_28 () Real)
(declare-fun x_29 () Real)
(declare-fun x_30 () Real)
(declare-fun x_31 () Real)
(declare-fun x_32 () Real)
(declare-fun x_33 () Real)
(declare-fun x_34 () Real)
(declare-fun x_35 () Real)
(declare-fun x_36 () Real)
(declare-fun x_37 () Real)
(declare-fun x_38 () Real)
(declare-fun x_39 () Real)
(declare-fun x_40 () Real)
(declare-fun x_41 () Real)
(declare-fun x_42 () Real)
(declare-fun x_43 () Real)
(declare-fun x_44 () Real)
(declare-fun x_45 () Real)
(declare-fun x_46 () Real)
(declare-fun x_47 () Real)
(declare-fun x_48 () Real)
(declare-fun x_49 () Real)
(declare-fun x_50 () Real)
(declare-fun x_51 () Real)
(declare-fun x_52 () Real)
(declare-fun x_53 () Real)
(declare-fun x_54 () Real)
(declare-fun x_55 () Real)
(declare-fun x_56 () Real)
(declare-fun x_57 () Real)
(declare-fun x_58 () Real)
(declare-fun x_59 () Real)
(declare-fun x_60 () Real)
(declare-fun x_61 () Real)
(declare-fun x_62 () Real)
(declare-fun x_63 () Real)
(declare-fun x_64 () Real)
(declare-fun x_65 () Real)
(declare-fun x_66 () Real)
(declare-fun x_67 () Real)
(declare-fun x_68 () Real)
(declare-fun x_69 () Real)
(declare-fun x_70 () Real)
(declare-fun x_71 () Real)
(declare-fun x_72 () Real)
(declare-fun x_73 () Real)
(declare-fun x_74 () Real)
(declare-fun x_75 () Real)
(declare-fun x_76 () Real)
(declare-fun x_77 () Real)
(declare-fun x_78 () Real)
(declare-fun x_79 () Real)
(declare-fun x_80 () Real)
(declare-fun x_81 () Real)
(declare-fun x_82 () Real)
(declare-fun x_83 () Real)
(declare-fun x_84 () Real)
(declare-fun x_85 () Real)
(declare-fun x_86 () Real)
(declare-fun x_87 () Real)
(declare-fun x_88 () Real)
(declare-fun x_89 () Real)
(declare-fun x_90 () Real)
(declare-fun x_91 () Real)
(declare-fun x_92 () Real)
(declare-fun x_93 () Real)
(declare-fun x_94 () Real)
(declare-fun x_95 () Real)
(declare-fun x_96 () Real)
(declare-fun x_97 () Real)
(declare-fun x_98 () Real)
(declare-fun x_99 () Real)
(declare-fun x_100 () Real)
(declare-fun x_101 () Real)
(declare-fun x_102 () Real)
(declare-fun x_103 () Real)
(declare-fun x_104 () Real)
(declare-fun x_105 () Real)
(declare-fun x_106 () Real)
(declare-fun x_107 () Real)
(declare-fun x_108 () Real)
(declare-fun x_109 () Real)
(declare-fun x_110 () Real)
(declare-fun x_111 () Real)
(declare-fun x_112 () Real)
(declare-fun x_113 () Real)
(declare-fun x_114 () Real)
(declare-fun x_115 () Real)
(declare-fun x_116 () Real)
(declare-fun x_117 () Real)
(declare-fun x_118 () Real)
(declare-fun x_119 () Real)
(declare-fun x_120 () Real)
(declare-fun x_121 () Real)
(declare-fun x_122 () Real)
(declare-fun x_123 () Real)
(declare-fun x_124 () Real)
(declare-fun x_125 () Real)
(declare-fun x_126 () Real)
(declare-fun x_127 () Real)
(declare-fun x_128 () Real)
(declare-fun x_129 () Real)
(declare-fun x_130 () Real)
(declare-fun x_131 () Real)
(declare-fun x_132 () Real)
(declare-fun x_133 () Real)
(declare-fun x_134 () Real)
(declare-fun x_135 () Real)
(declare-fun x_136 () Real)
(declare-fun x_137 () Real)
(declare-fun x_138 () Real)
(declare-fun x_139 () Real)
(declare-fun x_140 () Real)
(declare-fun x_141 () Real)
(declare-fun x_142 () Real)
(declare-fun x_143 () Real)
(declare-fun x_144 () Real)
(declare-fun x_145 () Real)
(declare-fun x_146 () Real)
(declare-fun x_147 () Real)
(declare-fun x_148 () Real)
(declare-fun x_149 () Real)
(declare-fun x_150 () Real)
(declare-fun x_151 () Real)
(declare-fun x_152 () Real)
(declare-fun x_153 () Real)
(declare-fun x_154 () Real)
(declare-fun x_155 () Real)
(declare-fun x_156 () Real)
(declare-fun x_157 () Real)
(declare-fun x_158 () Real)
(declare-fun x_159 () Real)
(declare-fun x_160 () Real)
(declare-fun x_161 () Real)
(declare-fun x_162 () Real)
(declare-fun x_163 () Real)
(declare-fun x_164 () Real)
(declare-fun x_165 () Real)
(declare-fun x_166 () Real)
(declare-fun x_167 () Real)
(declare-fun x_168 () Real)
(declare-fun x_169 () Real)
(declare-fun x_170 () Real)
(declare-fun x_171 () Real)
(declare-fun x_172 () Real)
(declare-fun x_173 () Real)
(declare-fun x_174 () Real)
(declare-fun x_175 () Real)
(declare-fun x_176 () Real)
(declare-fun x_177 () Real)
(declare-fun x_178 () Real)
(declare-fun x_179 () Real)
(declare-fun x_180 () Real)
(assert (let ((?v_62 (= x_68 x_9)) (?v_75 (= x_69 x_1)) (?v_13 (= x_70 x_2)) (?v_20 (= x_71 x_3)) (?v_27 (= x_72 x_4)) (?v_34 (= x_73 x_5)) (?v_41 (= x_74 x_6)) (?v_48 (= x_75 x_7)) (?v_55 (= x_76 x_8)) (?v_132 (= x_12 x_21))) (let ((?v_123 (not ?v_132)) (?v_122 (+ (+ x_21 x_10) x_11))) (let ((?v_178 (= x_12 ?v_122)) (?v_135 (= x_13 x_21))) (let ((?v_124 (not ?v_135)) (?v_182 (= x_13 ?v_122)) (?v_138 (= x_14 x_21))) (let ((?v_125 (not ?v_138)) (?v_186 (= x_14 ?v_122)) (?v_141 (= x_15 x_21))) (let ((?v_126 (not ?v_141)) (?v_190 (= x_15 ?v_122)) (?v_144 (= x_16 x_21))) (let ((?v_127 (not ?v_144)) (?v_194 (= x_16 ?v_122)) (?v_147 (= x_17 x_21))) (let ((?v_128 (not ?v_147)) (?v_198 (= x_17 ?v_122)) (?v_150 (= x_18 x_21))) (let ((?v_129 (not ?v_150)) (?v_202 (= x_18 ?v_122)) (?v_153 (= x_19 x_21))) (let ((?v_130 (not ?v_153)) (?v_206 (= x_19 ?v_122)) (?v_156 (= x_20 x_21))) (let ((?v_131 (not ?v_156)) (?v_210 (= x_20 ?v_122)) (?v_177 (not (<= x_61 x_21))) (?v_181 (not (<= x_62 x_21))) (?v_185 (not (<= x_63 x_21))) (?v_189 (not (<= x_64 x_21))) (?v_193 (not (<= x_65 x_21))) (?v_197 (not (<= x_66 x_21))) (?v_201 (not (<= x_67 x_21))) (?v_205 (not (<= x_58 x_21))) (?v_209 (not (<= x_60 x_21)))) (let ((?v_213 (or ?v_177 ?v_178)) (?v_216 (or ?v_181 ?v_182)) (?v_219 (or ?v_185 ?v_186)) (?v_222 (or ?v_189 ?v_190)) (?v_225 (or ?v_193 ?v_194)) (?v_228 (or ?v_197 ?v_198)) (?v_231 (or ?v_201 ?v_202)) (?v_234 (or ?v_205 ?v_206)) (?v_237 (or ?v_209 ?v_210)) (?v_5 (= x_49 0)) (?v_14 (= x_50 0)) (?v_21 (= x_51 0)) (?v_28 (= x_52 0)) (?v_35 (= x_53 0)) (?v_42 (= x_54 0)) (?v_49 (= x_55 0)) (?v_56 (= x_56 0)) (?v_63 (= x_57 0)) (?v_4 (= x_12 x_10)) (?v_15 (= x_13 x_10)) (?v_22 (= x_14 x_10)) (?v_29 (= x_15 x_10)) (?v_36 (= x_16 x_10)) (?v_43 (= x_17 x_10)) (?v_50 (= x_18 x_10)) (?v_57 (= x_19 x_10)) (?v_64 (= x_20 x_10)) (?v_76 (= x_61 1)) (?v_16 (= x_62 1)) (?v_23 (= x_63 1)) (?v_30 (= x_64 1)) (?v_37 (= x_65 1)) (?v_44 (= x_66 1)) (?v_51 (= x_67 1)) (?v_58 (= x_58 1)) (?v_65 (= x_60 1)) (?v_10 (= x_25 0)) (?v_17 (= x_28 0)) (?v_24 (= x_31 0)) (?v_31 (= x_34 0)) (?v_38 (= x_37 0)) (?v_45 (= x_40 0)) (?v_52 (= x_43 0)) (?v_59 (= x_46 0)) (?v_66 (= x_24 0)) (?v_9 (= x_26 0)) (?v_18 (= x_29 0)) (?v_25 (= x_32 0)) (?v_32 (= x_35 0)) (?v_39 (= x_38 0)) (?v_46 (= x_41 0)) (?v_53 (= x_44 0)) (?v_60 (= x_47 0)) (?v_67 (= x_23 0)) (?v_11 (= x_27 0)) (?v_19 (= x_30 0)) (?v_26 (= x_33 0)) (?v_33 (= x_36 0)) (?v_40 (= x_39 0)) (?v_47 (= x_42 0)) (?v_54 (= x_45 0)) (?v_61 (= x_48 0)) (?v_68 (= x_22 0)) (?v_6 (= 1 x_10)) (?v_3 (+ 1 1))) (let ((?v_8 (= x_61 ?v_3)) (?v_7 (= (+ x_10 x_11) 1))) (let ((?v_12 (and (not ?v_6) (not ?v_7))) (?v_74 (= x_62 ?v_3)) (?v_78 (= x_63 ?v_3)) (?v_80 (= x_64 ?v_3)) (?v_82 (= x_65 ?v_3)) (?v_84 (= x_66 ?v_3)) (?v_86 (= x_67 ?v_3)) (?v_88 (= x_58 ?v_3)) (?v_90 (= x_60 ?v_3)) (?v_109 (+ x_0 x_10))) (let ((?v_110 (<= x_12 ?v_109)) (?v_111 (<= x_13 ?v_109)) (?v_112 (<= x_14 ?v_109)) (?v_113 (<= x_15 ?v_109)) (?v_114 (<= x_16 ?v_109)) (?v_115 (<= x_17 ?v_109)) (?v_116 (<= x_18 ?v_109)) (?v_117 (<= x_19 ?v_109)) (?v_118 (<= x_20 ?v_109)) (?v_251 (not (<= (- ?v_109 x_179) 1))) (?v_252 (not (>= (- ?v_109 x_180) 1))) (?v_258 (- 1 1))) (let ((?v_253 (not (<= ?v_258 x_178))) (?v_257 (= x_10 ?v_109))) (let ((?v_256 (not ?v_257)) (?v_254 (+ (+ ?v_109 x_10) x_11))) (let ((?v_285 (= x_10 ?v_254))) (let ((?v_255 (and (or ?v_256 (not (>= (+ ?v_109 x_11) 1))) (not ?v_285))) (?v_284 (not (>= ?v_109 1)))) (let ((?v_272 (and ?v_257 ?v_284)) (?v_273 (< x_0 0)) (?v_289 (or ?v_284 ?v_285)) (?v_290 (- 0 x_1))) (let ((?v_286 (* ?v_290 1000)) (?v_301 (- 0 x_9))) (let ((?v_287 (* ?v_301 1000)) (?v_302 (+ 0 x_11))) (let ((?v_303 (and ?v_285 (not (= ?v_302 0)))) (?v_304 (- 0 0)) (?v_2 (* x_49 2)) (?v_69 (- ?v_3 1)) (?v_71 (+ ?v_3 1)) (?v_72 (+ ?v_302 1)) (?v_73 (+ (+ x_10 x_10) x_11)) (?v_70 (* x_50 2)) (?v_77 (* x_51 2)) (?v_79 (* x_52 2)) (?v_81 (* x_53 2)) (?v_83 (* x_54 2)) (?v_85 (* x_55 2)) (?v_87 (* x_56 2)) (?v_89 (* x_57 2)) (?v_91 (- x_61 x_59)) (?v_92 (- x_62 x_59)) (?v_93 (- x_63 x_59)) (?v_94 (- x_64 x_59)) (?v_95 (- x_65 x_59)) (?v_96 (- x_66 x_59)) (?v_97 (- x_67 x_59)) (?v_98 (- x_58 x_59)) (?v_99 (- x_60 x_59)) (?v_100 (+ x_61 x_59)) (?v_101 (+ x_62 x_59)) (?v_102 (+ x_63 x_59)) (?v_103 (+ x_64 x_59)) (?v_104 (+ x_65 x_59)) (?v_105 (+ x_66 x_59)) (?v_106 (+ x_67 x_59)) (?v_107 (+ x_58 x_59)) (?v_108 (+ x_60 x_59)) (?v_119 (- x_21 x_179)) (?v_120 (- x_21 x_180)) (?v_121 (+ x_21 x_11)) (?v_133 (- x_69 x_169)) (?v_134 (- x_61 x_160)) (?v_136 (- x_70 x_170)) (?v_137 (- x_62 x_161)) (?v_139 (- x_71 x_171)) (?v_140 (- x_63 x_162)) (?v_142 (- x_72 x_172)) (?v_143 (- x_64 x_163)) (?v_145 (- x_73 x_173)) (?v_146 (- x_65 x_164)) (?v_148 (- x_74 x_174)) (?v_149 (- x_66 x_165)) (?v_151 (- x_75 x_175)) (?v_152 (- x_67 x_166)) (?v_154 (- x_76 x_176)) (?v_155 (- x_58 x_167)) (?v_157 (- x_68 x_177)) (?v_158 (- x_60 x_168)) (?v_159 (- x_69 x_27)) (?v_160 (- x_61 x_21)) (?v_161 (- x_70 x_30)) (?v_162 (- x_62 x_21)) (?v_163 (- x_71 x_33)) (?v_164 (- x_63 x_21)) (?v_165 (- x_72 x_36)) (?v_166 (- x_64 x_21)) (?v_167 (- x_73 x_39)) (?v_168 (- x_65 x_21)) (?v_169 (- x_74 x_42)) (?v_170 (- x_66 x_21)) (?v_171 (- x_75 x_45)) (?v_172 (- x_67 x_21)) (?v_173 (- x_76 x_48)) (?v_174 (- x_58 x_21)) (?v_175 (- x_68 x_22)) (?v_176 (- x_60 x_21)) (?v_214 (- x_27 x_169))) (let ((?v_179 (* ?v_214 1000)) (?v_180 (* (- x_27 x_177) 1000)) (?v_183 (* (- x_30 x_169) 1000)) (?v_184 (* (- x_30 x_177) 1000)) (?v_187 (* (- x_33 x_169) 1000)) (?v_188 (* (- x_33 x_177) 1000)) (?v_191 (* (- x_36 x_169) 1000)) (?v_192 (* (- x_36 x_177) 1000)) (?v_195 (* (- x_39 x_169) 1000)) (?v_196 (* (- x_39 x_177) 1000)) (?v_199 (* (- x_42 x_169) 1000)) (?v_200 (* (- x_42 x_177) 1000)) (?v_203 (* (- x_45 x_169) 1000)) (?v_204 (* (- x_45 x_177) 1000)) (?v_207 (* (- x_48 x_169) 1000)) (?v_208 (* (- x_48 x_177) 1000)) (?v_211 (* (- x_22 x_169) 1000)) (?v_238 (- x_22 x_177))) (let ((?v_212 (* ?v_238 1000)) (?v_215 (- x_21 x_160)) (?v_217 (- x_30 x_170)) (?v_218 (- x_21 x_161)) (?v_220 (- x_33 x_171)) (?v_221 (- x_21 x_162)) (?v_223 (- x_36 x_172)) (?v_224 (- x_21 x_163)) (?v_226 (- x_39 x_173)) (?v_227 (- x_21 x_164)) (?v_229 (- x_42 x_174)) (?v_230 (- x_21 x_165)) (?v_232 (- x_45 x_175)) (?v_233 (- x_21 x_166)) (?v_235 (- x_48 x_176)) (?v_236 (- x_21 x_167)) (?v_239 (- x_21 x_168)) (?v_240 (- x_26 x_27)) (?v_242 (- x_29 x_30)) (?v_244 (- x_32 x_33)) (?v_245 (- x_35 x_36)) (?v_246 (- x_38 x_39)) (?v_247 (- x_41 x_42)) (?v_248 (- x_44 x_45)) (?v_249 (- x_47 x_48)) (?v_250 (- x_23 x_22)) (?v_259 (- x_1 x_1)) (?v_261 (- x_2 x_2)) (?v_263 (- x_3 x_3)) (?v_264 (- x_4 x_4)) (?v_265 (- x_5 x_5)) (?v_266 (- x_6 x_6)) (?v_267 (- x_7 x_7)) (?v_268 (- x_8 x_8)) (?v_269 (- x_9 x_9)) (?v_270 (- x_1 0)) (?v_271 (- 1 ?v_109)) (?v_275 (- x_2 0)) (?v_277 (- x_3 0)) (?v_278 (- x_4 0)) (?v_279 (- x_5 0)) (?v_280 (- x_6 0)) (?v_281 (- x_7 0)) (?v_282 (- x_8 0)) (?v_283 (- x_9 0)) (?v_291 (- ?v_109 1)) (?v_293 (- 0 x_2)) (?v_295 (- 0 x_3)) (?v_296 (- 0 x_4)) (?v_297 (- 0 x_5)) (?v_298 (- 0 x_6)) (?v_299 (- 0 x_7)) (?v_300 (- 0 x_8)) (?v_0 (+ x_0 (/ 999 1000))) (?v_1 (+ x_0 (/ 1001 1000))) (?v_241 (* (* x_11 999) (/ 1 1000))) (?v_243 (* (* x_11 1001) (/ 1 1000))) (?v_260 (* (* ?v_258 999) (/ 1 1000))) (?v_262 (* (* ?v_258 1001) (/ 1 1000)))) (let ((?v_274 (* (* ?v_271 999) (/ 1 1000))) (?v_276 (* (* ?v_271 1001) (/ 1 1000))) (?v_288 (and ?v_289 (or (not (>= (+ (+ (* (* (+ (+ (+ 1 (* ?v_286 (/ 1 999))) 1) (* ?v_287 (/ 1 999))) 1) (/ 1 2)) x_59) (/ 3001 1998)) 0)) (> (- (- (* (* (+ (+ (+ 1 (* ?v_286 (/ 1 1001))) 1) (* ?v_287 (/ 1 1001))) 1) (/ 1 2)) x_59) (/ 1 2)) 0)))) (?v_292 (* (* ?v_291 999) (/ 1 1000))) (?v_294 (* (* ?v_291 1001) (/ 1 1000))) (?v_305 (and ?v_285 (or (not (<= ?v_241 ?v_304)) (not (<= ?v_304 ?v_243)))))) (and (and (and (and (and (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_10 0)) (not (<= x_11 0))) (not (<= x_59 0))) (not (< x_178 (+ x_59 (* (* (+ (* (* x_11 1) (/ 1 2)) 1) 1001) (/ 1 999)))))) (< x_179 (- (* (* (- (- x_11 x_178) 1) 999) (/ 1 2)) 1))) (not (< x_179 (* (* (+ (+ (+ x_10 x_59) x_178) (/ 1501 1000)) 1001) (/ 1 999))))) (not (<= x_180 0))) (<= x_180 (- x_10 (+ (+ x_59 (* (* (+ x_11 2) 1001) (/ 1 999))) (/ 1 2))))) (= x_0 0)) (<= ?v_0 x_1)) (<= x_1 ?v_1)) (<= ?v_0 x_2)) (<= x_2 ?v_1)) (<= ?v_0 x_3)) (<= x_3 ?v_1)) (<= ?v_0 x_4)) (<= x_4 ?v_1)) (<= ?v_0 x_5)) (<= x_5 ?v_1)) (<= ?v_0 x_6)) (<= x_6 ?v_1)) (<= ?v_0 x_7)) (<= x_7 ?v_1)) (<= ?v_0 x_8)) (<= x_8 ?v_1)) (<= ?v_0 x_9)) (<= x_9 ?v_1)) (or (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (< x_0 x_1) (< x_0 x_2)) (< x_0 x_3)) (< x_0 x_4)) (< x_0 x_5)) (< x_0 x_6)) (< x_0 x_7)) (< x_0 x_8)) (< x_0 x_9)) (< x_0 x_77)) (<= x_77 x_1)) (<= x_77 x_2)) (<= x_77 x_3)) (<= x_77 x_4)) (<= x_77 x_5)) (<= x_77 x_6)) (<= x_77 x_7)) (<= x_77 x_8)) (<= x_77 x_9)) (or (or (or (or (or (or (or (or (= x_77 x_1) (= x_77 x_2)) (= x_77 x_3)) (= x_77 x_4)) (= x_77 x_5)) (= x_77 x_6)) (= x_77 x_7)) (= x_77 x_8)) (= x_77 x_9))) ?v_75) ?v_13) ?v_20) ?v_27) ?v_34) ?v_41) ?v_48) ?v_55) ?v_62) ?v_5) ?v_14) ?v_21) ?v_28) ?v_35) ?v_42) ?v_49) ?v_56) ?v_63) ?v_4) ?v_15) ?v_22) ?v_29) ?v_36) ?v_43) ?v_50) ?v_57) ?v_64) ?v_76) ?v_16) ?v_23) ?v_30) ?v_37) ?v_44) ?v_51) ?v_58) ?v_65) ?v_10) ?v_17) ?v_24) ?v_31) ?v_38) ?v_45) ?v_52) ?v_59) ?v_66) ?v_9) ?v_18) ?v_25) ?v_32) ?v_39) ?v_46) ?v_53) ?v_60) ?v_67) ?v_11) ?v_19) ?v_26) ?v_33) ?v_40) ?v_47) ?v_54) ?v_61) ?v_68) (= x_78 1)) (= x_79 1)) (= x_80 1)) (= x_81 1)) (= x_82 1)) (= x_83 1)) (= x_84 1)) (= x_85 1)) (= x_86 1)) (= x_87 1)) (= x_88 1)) (= x_89 1)) (= x_90 1)) (= x_91 1)) (= x_92 1)) (= x_93 1)) (= x_94 1)) (= x_95 1)) (= x_96 1)) (= x_97 1)) (= x_98 1)) (= x_99 1)) (= x_100 1)) (= x_101 1)) (= x_102 1)) (= x_103 1)) (= x_104 1)) (= x_105 1)) (= x_106 1)) (= x_107 1)) (= x_108 1)) (= x_109 1)) (= x_110 1)) (= x_111 1)) (= x_112 1)) (= x_113 1)) (= x_114 1)) (= x_115 1)) (= x_116 1)) (= x_117 1)) (= x_118 1)) (= x_119 1)) (= x_120 1)) (= x_121 1)) (= x_122 1)) (= x_123 1)) (= x_124 1)) (= x_125 1)) (= x_126 1)) (= x_127 1)) (= x_128 1)) (= x_129 1)) (= x_130 1)) (= x_131 1)) (= x_132 1)) (= x_133 1)) (= x_134 1)) (= x_135 1)) (= x_136 1)) (= x_137 1)) (= x_138 1)) (= x_139 1)) (= x_140 1)) (= x_141 1)) (= x_142 1)) (= x_143 1)) (= x_144 1)) (= x_145 1)) (= x_146 1)) (= x_147 1)) (= x_148 1)) (= x_149 1)) (= x_150 1)) (= x_151 1)) (= x_152 1)) (= x_153 1)) (= x_154 1)) (= x_155 1)) (= x_156 1)) (= x_157 1)) (= x_158 1)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (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 (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_1) (<= ?v_0 x_69)) (<= x_69 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_69 ?v_2)) (<= ?v_2 ?v_71)) ?v_8) ?v_4) (and (and (and ?v_7 (= x_61 ?v_72)) (= x_12 ?v_73)) ?v_5)) (and (and (and ?v_12 ?v_8) ?v_5) ?v_4))) (or (or (and (and (and ?v_6 (= x_27 x_0)) ?v_9) ?v_10) (and (and (and ?v_7 (= x_26 x_0)) (= x_25 (- x_61 1))) ?v_11)) (and (and (and ?v_12 ?v_11) ?v_9) ?v_10))) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47) ?v_48) ?v_49) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54) ?v_55) ?v_56) ?v_57) ?v_58) ?v_59) ?v_60) ?v_61) ?v_62) ?v_63) ?v_64) ?v_65) ?v_66) ?v_67) ?v_68) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_2) (<= ?v_0 x_70)) (<= x_70 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_69 ?v_70)) (<= ?v_70 ?v_71)) ?v_74) ?v_15) (and (and (and ?v_7 (= x_62 ?v_72)) (= x_13 ?v_73)) ?v_14)) (and (and (and ?v_12 ?v_74) ?v_14) ?v_15))) (or (or (and (and (and ?v_6 (= x_30 x_0)) ?v_18) ?v_17) (and (and (and ?v_7 (= x_29 x_0)) (= x_28 (- x_62 1))) ?v_19)) (and (and (and ?v_12 ?v_19) ?v_18) ?v_17))) ?v_75) ?v_5) ?v_4) ?v_76) ?v_10) ?v_9) ?v_11) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47) ?v_48) ?v_49) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54) ?v_55) ?v_56) ?v_57) ?v_58) ?v_59) ?v_60) ?v_61) ?v_62) ?v_63) ?v_64) ?v_65) ?v_66) ?v_67) ?v_68)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_3) (<= ?v_0 x_71)) (<= x_71 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_69 ?v_77)) (<= ?v_77 ?v_71)) ?v_78) ?v_22) (and (and (and ?v_7 (= x_63 ?v_72)) (= x_14 ?v_73)) ?v_21)) (and (and (and ?v_12 ?v_78) ?v_21) ?v_22))) (or (or (and (and (and ?v_6 (= x_33 x_0)) ?v_25) ?v_24) (and (and (and ?v_7 (= x_32 x_0)) (= x_31 (- x_63 1))) ?v_26)) (and (and (and ?v_12 ?v_26) ?v_25) ?v_24))) ?v_75) ?v_5) ?v_4) ?v_76) ?v_10) ?v_9) ?v_11) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47) ?v_48) ?v_49) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54) ?v_55) ?v_56) ?v_57) ?v_58) ?v_59) ?v_60) ?v_61) ?v_62) ?v_63) ?v_64) ?v_65) ?v_66) ?v_67) ?v_68)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_4) (<= ?v_0 x_72)) (<= x_72 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_69 ?v_79)) (<= ?v_79 ?v_71)) ?v_80) ?v_29) (and (and (and ?v_7 (= x_64 ?v_72)) (= x_15 ?v_73)) ?v_28)) (and (and (and ?v_12 ?v_80) ?v_28) ?v_29))) (or (or (and (and (and ?v_6 (= x_36 x_0)) ?v_32) ?v_31) (and (and (and ?v_7 (= x_35 x_0)) (= x_34 (- x_64 1))) ?v_33)) (and (and (and ?v_12 ?v_33) ?v_32) ?v_31))) ?v_75) ?v_5) ?v_4) ?v_76) ?v_10) ?v_9) ?v_11) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47) ?v_48) ?v_49) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54) ?v_55) ?v_56) ?v_57) ?v_58) ?v_59) ?v_60) ?v_61) ?v_62) ?v_63) ?v_64) ?v_65) ?v_66) ?v_67) ?v_68)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_5) (<= ?v_0 x_73)) (<= x_73 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_69 ?v_81)) (<= ?v_81 ?v_71)) ?v_82) ?v_36) (and (and (and ?v_7 (= x_65 ?v_72)) (= x_16 ?v_73)) ?v_35)) (and (and (and ?v_12 ?v_82) ?v_35) ?v_36))) (or (or (and (and (and ?v_6 (= x_39 x_0)) ?v_39) ?v_38) (and (and (and ?v_7 (= x_38 x_0)) (= x_37 (- x_65 1))) ?v_40)) (and (and (and ?v_12 ?v_40) ?v_39) ?v_38))) ?v_75) ?v_5) ?v_4) ?v_76) ?v_10) ?v_9) ?v_11) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47) ?v_48) ?v_49) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54) ?v_55) ?v_56) ?v_57) ?v_58) ?v_59) ?v_60) ?v_61) ?v_62) ?v_63) ?v_64) ?v_65) ?v_66) ?v_67) ?v_68)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_6) (<= ?v_0 x_74)) (<= x_74 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_69 ?v_83)) (<= ?v_83 ?v_71)) ?v_84) ?v_43) (and (and (and ?v_7 (= x_66 ?v_72)) (= x_17 ?v_73)) ?v_42)) (and (and (and ?v_12 ?v_84) ?v_42) ?v_43))) (or (or (and (and (and ?v_6 (= x_42 x_0)) ?v_46) ?v_45) (and (and (and ?v_7 (= x_41 x_0)) (= x_40 (- x_66 1))) ?v_47)) (and (and (and ?v_12 ?v_47) ?v_46) ?v_45))) ?v_75) ?v_5) ?v_4) ?v_76) ?v_10) ?v_9) ?v_11) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40) ?v_48) ?v_49) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54) ?v_55) ?v_56) ?v_57) ?v_58) ?v_59) ?v_60) ?v_61) ?v_62) ?v_63) ?v_64) ?v_65) ?v_66) ?v_67) ?v_68)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_7) (<= ?v_0 x_75)) (<= x_75 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_69 ?v_85)) (<= ?v_85 ?v_71)) ?v_86) ?v_50) (and (and (and ?v_7 (= x_67 ?v_72)) (= x_18 ?v_73)) ?v_49)) (and (and (and ?v_12 ?v_86) ?v_49) ?v_50))) (or (or (and (and (and ?v_6 (= x_45 x_0)) ?v_53) ?v_52) (and (and (and ?v_7 (= x_44 x_0)) (= x_43 (- x_67 1))) ?v_54)) (and (and (and ?v_12 ?v_54) ?v_53) ?v_52))) ?v_75) ?v_5) ?v_4) ?v_76) ?v_10) ?v_9) ?v_11) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47) ?v_55) ?v_56) ?v_57) ?v_58) ?v_59) ?v_60) ?v_61) ?v_62) ?v_63) ?v_64) ?v_65) ?v_66) ?v_67) ?v_68)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_8) (<= ?v_0 x_76)) (<= x_76 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_69 ?v_87)) (<= ?v_87 ?v_71)) ?v_88) ?v_57) (and (and (and ?v_7 (= x_58 ?v_72)) (= x_19 ?v_73)) ?v_56)) (and (and (and ?v_12 ?v_88) ?v_56) ?v_57))) (or (or (and (and (and ?v_6 (= x_48 x_0)) ?v_60) ?v_59) (and (and (and ?v_7 (= x_47 x_0)) (= x_46 (- x_58 1))) ?v_61)) (and (and (and ?v_12 ?v_61) ?v_60) ?v_59))) ?v_75) ?v_5) ?v_4) ?v_76) ?v_10) ?v_9) ?v_11) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47) ?v_48) ?v_49) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54) ?v_62) ?v_63) ?v_64) ?v_65) ?v_66) ?v_67) ?v_68)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_9) (<= ?v_0 x_68)) (<= x_68 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_69 ?v_89)) (<= ?v_89 ?v_71)) ?v_90) ?v_64) (and (and (and ?v_7 (= x_60 ?v_72)) (= x_20 ?v_73)) ?v_63)) (and (and (and ?v_12 ?v_90) ?v_63) ?v_64))) (or (or (and (and (and ?v_6 (= x_22 x_0)) ?v_67) ?v_66) (and (and (and ?v_7 (= x_23 x_0)) (= x_24 (- x_60 1))) ?v_68)) (and (and (and ?v_12 ?v_68) ?v_67) ?v_66))) ?v_75) ?v_5) ?v_4) ?v_76) ?v_10) ?v_9) ?v_11) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47) ?v_48) ?v_49) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54) ?v_55) ?v_56) ?v_57) ?v_58) ?v_59) ?v_60) ?v_61)) (<= ?v_91 x_78)) (<= ?v_91 x_87)) (<= ?v_91 x_96)) (<= ?v_91 x_105)) (<= ?v_91 x_114)) (<= ?v_91 x_123)) (<= ?v_91 x_132)) (<= ?v_91 x_141)) (<= ?v_91 x_150)) (<= ?v_92 x_79)) (<= ?v_92 x_88)) (<= ?v_92 x_97)) (<= ?v_92 x_106)) (<= ?v_92 x_115)) (<= ?v_92 x_124)) (<= ?v_92 x_133)) (<= ?v_92 x_142)) (<= ?v_92 x_151)) (<= ?v_93 x_80)) (<= ?v_93 x_89)) (<= ?v_93 x_98)) (<= ?v_93 x_107)) (<= ?v_93 x_116)) (<= ?v_93 x_125)) (<= ?v_93 x_134)) (<= ?v_93 x_143)) (<= ?v_93 x_152)) (<= ?v_94 x_81)) (<= ?v_94 x_90)) (<= ?v_94 x_99)) (<= ?v_94 x_108)) (<= ?v_94 x_117)) (<= ?v_94 x_126)) (<= ?v_94 x_135)) (<= ?v_94 x_144)) (<= ?v_94 x_153)) (<= ?v_95 x_82)) (<= ?v_95 x_91)) (<= ?v_95 x_100)) (<= ?v_95 x_109)) (<= ?v_95 x_118)) (<= ?v_95 x_127)) (<= ?v_95 x_136)) (<= ?v_95 x_145)) (<= ?v_95 x_154)) (<= ?v_96 x_83)) (<= ?v_96 x_92)) (<= ?v_96 x_101)) (<= ?v_96 x_110)) (<= ?v_96 x_119)) (<= ?v_96 x_128)) (<= ?v_96 x_137)) (<= ?v_96 x_146)) (<= ?v_96 x_155)) (<= ?v_97 x_84)) (<= ?v_97 x_93)) (<= ?v_97 x_102)) (<= ?v_97 x_111)) (<= ?v_97 x_120)) (<= ?v_97 x_129)) (<= ?v_97 x_138)) (<= ?v_97 x_147)) (<= ?v_97 x_156)) (<= ?v_98 x_85)) (<= ?v_98 x_94)) (<= ?v_98 x_103)) (<= ?v_98 x_112)) (<= ?v_98 x_121)) (<= ?v_98 x_130)) (<= ?v_98 x_139)) (<= ?v_98 x_148)) (<= ?v_98 x_157)) (<= ?v_99 x_86)) (<= ?v_99 x_95)) (<= ?v_99 x_104)) (<= ?v_99 x_113)) (<= ?v_99 x_122)) (<= ?v_99 x_131)) (<= ?v_99 x_140)) (<= ?v_99 x_149)) (<= ?v_99 x_158)) (<= x_78 ?v_100)) (<= x_87 ?v_100)) (<= x_96 ?v_100)) (<= x_105 ?v_100)) (<= x_114 ?v_100)) (<= x_123 ?v_100)) (<= x_132 ?v_100)) (<= x_141 ?v_100)) (<= x_150 ?v_100)) (<= x_79 ?v_101)) (<= x_88 ?v_101)) (<= x_97 ?v_101)) (<= x_106 ?v_101)) (<= x_115 ?v_101)) (<= x_124 ?v_101)) (<= x_133 ?v_101)) (<= x_142 ?v_101)) (<= x_151 ?v_101)) (<= x_80 ?v_102)) (<= x_89 ?v_102)) (<= x_98 ?v_102)) (<= x_107 ?v_102)) (<= x_116 ?v_102)) (<= x_125 ?v_102)) (<= x_134 ?v_102)) (<= x_143 ?v_102)) (<= x_152 ?v_102)) (<= x_81 ?v_103)) (<= x_90 ?v_103)) (<= x_99 ?v_103)) (<= x_108 ?v_103)) (<= x_117 ?v_103)) (<= x_126 ?v_103)) (<= x_135 ?v_103)) (<= x_144 ?v_103)) (<= x_153 ?v_103)) (<= x_82 ?v_104)) (<= x_91 ?v_104)) (<= x_100 ?v_104)) (<= x_109 ?v_104)) (<= x_118 ?v_104)) (<= x_127 ?v_104)) (<= x_136 ?v_104)) (<= x_145 ?v_104)) (<= x_154 ?v_104)) (<= x_83 ?v_105)) (<= x_92 ?v_105)) (<= x_101 ?v_105)) (<= x_110 ?v_105)) (<= x_119 ?v_105)) (<= x_128 ?v_105)) (<= x_137 ?v_105)) (<= x_146 ?v_105)) (<= x_155 ?v_105)) (<= x_84 ?v_106)) (<= x_93 ?v_106)) (<= x_102 ?v_106)) (<= x_111 ?v_106)) (<= x_120 ?v_106)) (<= x_129 ?v_106)) (<= x_138 ?v_106)) (<= x_147 ?v_106)) (<= x_156 ?v_106)) (<= x_85 ?v_107)) (<= x_94 ?v_107)) (<= x_103 ?v_107)) (<= x_112 ?v_107)) (<= x_121 ?v_107)) (<= x_130 ?v_107)) (<= x_139 ?v_107)) (<= x_148 ?v_107)) (<= x_157 ?v_107)) (<= x_86 ?v_108)) (<= x_95 ?v_108)) (<= x_104 ?v_108)) (<= x_113 ?v_108)) (<= x_122 ?v_108)) (<= x_131 ?v_108)) (<= x_140 ?v_108)) (<= x_149 ?v_108)) (<= x_158 ?v_108)) (= x_77 x_0)))) (or (and (and (and (and (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 ?v_110) (not ?v_111)) (not ?v_112)) (not ?v_113)) (not ?v_114)) (not ?v_115)) (not ?v_116)) (not ?v_117)) (not ?v_118)) (= x_159 x_77)) (= x_160 x_61)) (= x_161 x_62)) (= x_162 x_63)) (= x_163 x_64)) (= x_164 x_65)) (= x_165 x_66)) (= x_166 x_67)) (= x_167 x_58)) (= x_168 x_60)) (= x_169 x_69)) (= x_170 x_70)) (= x_171 x_71)) (= x_172 x_72)) (= x_173 x_73)) (= x_174 x_74)) (= x_175 x_75)) (= x_176 x_76)) (= x_177 x_68)) (= x_21 ?v_254)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (or (or ?v_110 ?v_111) ?v_112) ?v_113) ?v_114) ?v_115) ?v_116) ?v_117) ?v_118) (= x_21 ?v_109)) (= x_159 x_0)) (= x_169 x_1)) (= x_170 x_2)) (= x_171 x_3)) (= x_172 x_4)) (= x_173 x_5)) (= x_174 x_6)) (= x_175 x_7)) (= x_176 x_8)) (= x_177 x_9)) (= x_160 1)) (= x_161 1)) (= x_162 1)) (= x_163 1)) (= x_164 1)) (= x_165 1)) (= x_166 1)) (= x_167 1)) (= x_168 1)))) (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (not (<= ?v_119 x_160)) (not (<= ?v_119 x_161))) (not (<= ?v_119 x_162))) (not (<= ?v_119 x_163))) (not (<= ?v_119 x_164))) (not (<= ?v_119 x_165))) (not (<= ?v_119 x_166))) (not (<= ?v_119 x_167))) (not (<= ?v_119 x_168))) (not (<= x_160 ?v_120))) (not (<= x_161 ?v_120))) (not (<= x_162 ?v_120))) (not (<= x_163 ?v_120))) (not (<= x_164 ?v_120))) (not (<= x_165 ?v_120))) (not (<= x_166 ?v_120))) (not (<= x_167 ?v_120))) (not (<= x_168 ?v_120))) (not (<= (- x_160 x_160) x_178))) (not (<= (- x_161 x_160) x_178))) (not (<= (- x_162 x_160) x_178))) (not (<= (- x_163 x_160) x_178))) (not (<= (- x_164 x_160) x_178))) (not (<= (- x_165 x_160) x_178))) (not (<= (- x_166 x_160) x_178))) (not (<= (- x_167 x_160) x_178))) (not (<= (- x_168 x_160) x_178))) (not (<= (- x_160 x_161) x_178))) (not (<= (- x_161 x_161) x_178))) (not (<= (- x_162 x_161) x_178))) (not (<= (- x_163 x_161) x_178))) (not (<= (- x_164 x_161) x_178))) (not (<= (- x_165 x_161) x_178))) (not (<= (- x_166 x_161) x_178))) (not (<= (- x_167 x_161) x_178))) (not (<= (- x_168 x_161) x_178))) (not (<= (- x_160 x_162) x_178))) (not (<= (- x_161 x_162) x_178))) (not (<= (- x_162 x_162) x_178))) (not (<= (- x_163 x_162) x_178))) (not (<= (- x_164 x_162) x_178))) (not (<= (- x_165 x_162) x_178))) (not (<= (- x_166 x_162) x_178))) (not (<= (- x_167 x_162) x_178))) (not (<= (- x_168 x_162) x_178))) (not (<= (- x_160 x_163) x_178))) (not (<= (- x_161 x_163) x_178))) (not (<= (- x_162 x_163) x_178))) (not (<= (- x_163 x_163) x_178))) (not (<= (- x_164 x_163) x_178))) (not (<= (- x_165 x_163) x_178))) (not (<= (- x_166 x_163) x_178))) (not (<= (- x_167 x_163) x_178))) (not (<= (- x_168 x_163) x_178))) (not (<= (- x_160 x_164) x_178))) (not (<= (- x_161 x_164) x_178))) (not (<= (- x_162 x_164) x_178))) (not (<= (- x_163 x_164) x_178))) (not (<= (- x_164 x_164) x_178))) (not (<= (- x_165 x_164) x_178))) (not (<= (- x_166 x_164) x_178))) (not (<= (- x_167 x_164) x_178))) (not (<= (- x_168 x_164) x_178))) (not (<= (- x_160 x_165) x_178))) (not (<= (- x_161 x_165) x_178))) (not (<= (- x_162 x_165) x_178))) (not (<= (- x_163 x_165) x_178))) (not (<= (- x_164 x_165) x_178))) (not (<= (- x_165 x_165) x_178))) (not (<= (- x_166 x_165) x_178))) (not (<= (- x_167 x_165) x_178))) (not (<= (- x_168 x_165) x_178))) (not (<= (- x_160 x_166) x_178))) (not (<= (- x_161 x_166) x_178))) (not (<= (- x_162 x_166) x_178))) (not (<= (- x_163 x_166) x_178))) (not (<= (- x_164 x_166) x_178))) (not (<= (- x_165 x_166) x_178))) (not (<= (- x_166 x_166) x_178))) (not (<= (- x_167 x_166) x_178))) (not (<= (- x_168 x_166) x_178))) (not (<= (- x_160 x_167) x_178))) (not (<= (- x_161 x_167) x_178))) (not (<= (- x_162 x_167) x_178))) (not (<= (- x_163 x_167) x_178))) (not (<= (- x_164 x_167) x_178))) (not (<= (- x_165 x_167) x_178))) (not (<= (- x_166 x_167) x_178))) (not (<= (- x_167 x_167) x_178))) (not (<= (- x_168 x_167) x_178))) (not (<= (- x_160 x_168) x_178))) (not (<= (- x_161 x_168) x_178))) (not (<= (- x_162 x_168) x_178))) (not (<= (- x_163 x_168) x_178))) (not (<= (- x_164 x_168) x_178))) (not (<= (- x_165 x_168) x_178))) (not (<= (- x_166 x_168) x_178))) (not (<= (- x_167 x_168) x_178))) (not (<= (- x_168 x_168) x_178))) (and (or ?v_123 (not (<= x_61 ?v_121))) (not ?v_178))) (and (or ?v_124 (not (<= x_62 ?v_121))) (not ?v_182))) (and (or ?v_125 (not (<= x_63 ?v_121))) (not ?v_186))) (and (or ?v_126 (not (<= x_64 ?v_121))) (not ?v_190))) (and (or ?v_127 (not (<= x_65 ?v_121))) (not ?v_194))) (and (or ?v_128 (not (<= x_66 ?v_121))) (not ?v_198))) (and (or ?v_129 (not (<= x_67 ?v_121))) (not ?v_202))) (and (or ?v_130 (not (<= x_58 ?v_121))) (not ?v_206))) (and (or ?v_131 (not (<= x_60 ?v_121))) (not ?v_210))) (and (and (and (and (and (and (and (and ?v_123 ?v_124) ?v_125) ?v_126) ?v_127) ?v_128) ?v_129) ?v_130) ?v_131)) (and ?v_132 (or (not (<= (* (* ?v_134 999) (/ 1 1000)) ?v_133)) (not (<= ?v_133 (* (* ?v_134 1001) (/ 1 1000))))))) (and ?v_135 (or (not (<= (* (* ?v_137 999) (/ 1 1000)) ?v_136)) (not (<= ?v_136 (* (* ?v_137 1001) (/ 1 1000))))))) (and ?v_138 (or (not (<= (* (* ?v_140 999) (/ 1 1000)) ?v_139)) (not (<= ?v_139 (* (* ?v_140 1001) (/ 1 1000))))))) (and ?v_141 (or (not (<= (* (* ?v_143 999) (/ 1 1000)) ?v_142)) (not (<= ?v_142 (* (* ?v_143 1001) (/ 1 1000))))))) (and ?v_144 (or (not (<= (* (* ?v_146 999) (/ 1 1000)) ?v_145)) (not (<= ?v_145 (* (* ?v_146 1001) (/ 1 1000))))))) (and ?v_147 (or (not (<= (* (* ?v_149 999) (/ 1 1000)) ?v_148)) (not (<= ?v_148 (* (* ?v_149 1001) (/ 1 1000))))))) (and ?v_150 (or (not (<= (* (* ?v_152 999) (/ 1 1000)) ?v_151)) (not (<= ?v_151 (* (* ?v_152 1001) (/ 1 1000))))))) (and ?v_153 (or (not (<= (* (* ?v_155 999) (/ 1 1000)) ?v_154)) (not (<= ?v_154 (* (* ?v_155 1001) (/ 1 1000))))))) (and ?v_156 (or (not (<= (* (* ?v_158 999) (/ 1 1000)) ?v_157)) (not (<= ?v_157 (* (* ?v_158 1001) (/ 1 1000))))))) (and (and ?v_132 ?v_177) (or (or (< x_77 x_27) (not (<= (* (* ?v_160 999) (/ 1 1000)) ?v_159))) (not (<= ?v_159 (* (* ?v_160 1001) (/ 1 1000))))))) (and (and ?v_135 ?v_181) (or (or (< x_77 x_30) (not (<= (* (* ?v_162 999) (/ 1 1000)) ?v_161))) (not (<= ?v_161 (* (* ?v_162 1001) (/ 1 1000))))))) (and (and ?v_138 ?v_185) (or (or (< x_77 x_33) (not (<= (* (* ?v_164 999) (/ 1 1000)) ?v_163))) (not (<= ?v_163 (* (* ?v_164 1001) (/ 1 1000))))))) (and (and ?v_141 ?v_189) (or (or (< x_77 x_36) (not (<= (* (* ?v_166 999) (/ 1 1000)) ?v_165))) (not (<= ?v_165 (* (* ?v_166 1001) (/ 1 1000))))))) (and (and ?v_144 ?v_193) (or (or (< x_77 x_39) (not (<= (* (* ?v_168 999) (/ 1 1000)) ?v_167))) (not (<= ?v_167 (* (* ?v_168 1001) (/ 1 1000))))))) (and (and ?v_147 ?v_197) (or (or (< x_77 x_42) (not (<= (* (* ?v_170 999) (/ 1 1000)) ?v_169))) (not (<= ?v_169 (* (* ?v_170 1001) (/ 1 1000))))))) (and (and ?v_150 ?v_201) (or (or (< x_77 x_45) (not (<= (* (* ?v_172 999) (/ 1 1000)) ?v_171))) (not (<= ?v_171 (* (* ?v_172 1001) (/ 1 1000))))))) (and (and ?v_153 ?v_205) (or (or (< x_77 x_48) (not (<= (* (* ?v_174 999) (/ 1 1000)) ?v_173))) (not (<= ?v_173 (* (* ?v_174 1001) (/ 1 1000))))))) (and (and ?v_156 ?v_209) (or (or (< x_77 x_22) (not (<= (* (* ?v_176 999) (/ 1 1000)) ?v_175))) (not (<= ?v_175 (* (* ?v_176 1001) (/ 1 1000))))))) (and ?v_213 (or (not (<= x_49 (+ (+ (* (* (+ (+ (+ x_160 (* ?v_179 (/ 1 999))) x_168) (* ?v_180 (/ 1 999))) 1) (/ 1 2)) x_59) (/ 3001 1998)))) (< x_49 (- (- (* (* (+ (+ (+ x_160 (* ?v_179 (/ 1 1001))) x_168) (* ?v_180 (/ 1 1001))) 1) (/ 1 2)) x_59) (/ 1 2)))))) (and ?v_216 (or (not (<= x_50 (+ (+ (* (* (+ (+ (+ x_160 (* ?v_183 (/ 1 999))) x_168) (* ?v_184 (/ 1 999))) 1) (/ 1 2)) x_59) (/ 3001 1998)))) (< x_50 (- (- (* (* (+ (+ (+ x_160 (* ?v_183 (/ 1 1001))) x_168) (* ?v_184 (/ 1 1001))) 1) (/ 1 2)) x_59) (/ 1 2)))))) (and ?v_219 (or (not (<= x_51 (+ (+ (* (* (+ (+ (+ x_160 (* ?v_187 (/ 1 999))) x_168) (* ?v_188 (/ 1 999))) 1) (/ 1 2)) x_59) (/ 3001 1998)))) (< x_51 (- (- (* (* (+ (+ (+ x_160 (* ?v_187 (/ 1 1001))) x_168) (* ?v_188 (/ 1 1001))) 1) (/ 1 2)) x_59) (/ 1 2)))))) (and ?v_222 (or (not (<= x_52 (+ (+ (* (* (+ (+ (+ x_160 (* ?v_191 (/ 1 999))) x_168) (* ?v_192 (/ 1 999))) 1) (/ 1 2)) x_59) (/ 3001 1998)))) (< x_52 (- (- (* (* (+ (+ (+ x_160 (* ?v_191 (/ 1 1001))) x_168) (* ?v_192 (/ 1 1001))) 1) (/ 1 2)) x_59) (/ 1 2)))))) (and ?v_225 (or (not (<= x_53 (+ (+ (* (* (+ (+ (+ x_160 (* ?v_195 (/ 1 999))) x_168) (* ?v_196 (/ 1 999))) 1) (/ 1 2)) x_59) (/ 3001 1998)))) (< x_53 (- (- (* (* (+ (+ (+ x_160 (* ?v_195 (/ 1 1001))) x_168) (* ?v_196 (/ 1 1001))) 1) (/ 1 2)) x_59) (/ 1 2)))))) (and ?v_228 (or (not (<= x_54 (+ (+ (* (* (+ (+ (+ x_160 (* ?v_199 (/ 1 999))) x_168) (* ?v_200 (/ 1 999))) 1) (/ 1 2)) x_59) (/ 3001 1998)))) (< x_54 (- (- (* (* (+ (+ (+ x_160 (* ?v_199 (/ 1 1001))) x_168) (* ?v_200 (/ 1 1001))) 1) (/ 1 2)) x_59) (/ 1 2)))))) (and ?v_231 (or (not (<= x_55 (+ (+ (* (* (+ (+ (+ x_160 (* ?v_203 (/ 1 999))) x_168) (* ?v_204 (/ 1 999))) 1) (/ 1 2)) x_59) (/ 3001 1998)))) (< x_55 (- (- (* (* (+ (+ (+ x_160 (* ?v_203 (/ 1 1001))) x_168) (* ?v_204 (/ 1 1001))) 1) (/ 1 2)) x_59) (/ 1 2)))))) (and ?v_234 (or (not (<= x_56 (+ (+ (* (* (+ (+ (+ x_160 (* ?v_207 (/ 1 999))) x_168) (* ?v_208 (/ 1 999))) 1) (/ 1 2)) x_59) (/ 3001 1998)))) (< x_56 (- (- (* (* (+ (+ (+ x_160 (* ?v_207 (/ 1 1001))) x_168) (* ?v_208 (/ 1 1001))) 1) (/ 1 2)) x_59) (/ 1 2)))))) (and ?v_237 (or (not (<= x_57 (+ (+ (* (* (+ (+ (+ x_160 (* ?v_211 (/ 1 999))) x_168) (* ?v_212 (/ 1 999))) 1) (/ 1 2)) x_59) (/ 3001 1998)))) (< x_57 (- (- (* (* (+ (+ (+ x_160 (* ?v_211 (/ 1 1001))) x_168) (* ?v_212 (/ 1 1001))) 1) (/ 1 2)) x_59) (/ 1 2)))))) (and ?v_213 (or (not (<= (* (* ?v_215 999) (/ 1 1000)) ?v_214)) (not (<= ?v_214 (* (* ?v_215 1001) (/ 1 1000))))))) (and ?v_216 (or (not (<= (* (* ?v_218 999) (/ 1 1000)) ?v_217)) (not (<= ?v_217 (* (* ?v_218 1001) (/ 1 1000))))))) (and ?v_219 (or (not (<= (* (* ?v_221 999) (/ 1 1000)) ?v_220)) (not (<= ?v_220 (* (* ?v_221 1001) (/ 1 1000))))))) (and ?v_222 (or (not (<= (* (* ?v_224 999) (/ 1 1000)) ?v_223)) (not (<= ?v_223 (* (* ?v_224 1001) (/ 1 1000))))))) (and ?v_225 (or (not (<= (* (* ?v_227 999) (/ 1 1000)) ?v_226)) (not (<= ?v_226 (* (* ?v_227 1001) (/ 1 1000))))))) (and ?v_228 (or (not (<= (* (* ?v_230 999) (/ 1 1000)) ?v_229)) (not (<= ?v_229 (* (* ?v_230 1001) (/ 1 1000))))))) (and ?v_231 (or (not (<= (* (* ?v_233 999) (/ 1 1000)) ?v_232)) (not (<= ?v_232 (* (* ?v_233 1001) (/ 1 1000))))))) (and ?v_234 (or (not (<= (* (* ?v_236 999) (/ 1 1000)) ?v_235)) (not (<= ?v_235 (* (* ?v_236 1001) (/ 1 1000))))))) (and ?v_237 (or (not (<= (* (* ?v_239 999) (/ 1 1000)) ?v_238)) (not (<= ?v_238 (* (* ?v_239 1001) (/ 1 1000))))))) (and ?v_178 (not (= x_25 (+ x_49 x_11))))) (and ?v_182 (not (= x_28 (+ x_50 x_11))))) (and ?v_186 (not (= x_31 (+ x_51 x_11))))) (and ?v_190 (not (= x_34 (+ x_52 x_11))))) (and ?v_194 (not (= x_37 (+ x_53 x_11))))) (and ?v_198 (not (= x_40 (+ x_54 x_11))))) (and ?v_202 (not (= x_43 (+ x_55 x_11))))) (and ?v_206 (not (= x_46 (+ x_56 x_11))))) (and ?v_210 (not (= x_24 (+ x_57 x_11))))) (and ?v_178 (or (not (<= ?v_241 ?v_240)) (not (<= ?v_240 ?v_243))))) (and ?v_182 (or (not (<= ?v_241 ?v_242)) (not (<= ?v_242 ?v_243))))) (and ?v_186 (or (not (<= ?v_241 ?v_244)) (not (<= ?v_244 ?v_243))))) (and ?v_190 (or (not (<= ?v_241 ?v_245)) (not (<= ?v_245 ?v_243))))) (and ?v_194 (or (not (<= ?v_241 ?v_246)) (not (<= ?v_246 ?v_243))))) (and ?v_198 (or (not (<= ?v_241 ?v_247)) (not (<= ?v_247 ?v_243))))) (and ?v_202 (or (not (<= ?v_241 ?v_248)) (not (<= ?v_248 ?v_243))))) (and ?v_206 (or (not (<= ?v_241 ?v_249)) (not (<= ?v_249 ?v_243))))) (and ?v_210 (or (not (<= ?v_241 ?v_250)) (not (<= ?v_250 ?v_243))))) ?v_251) ?v_251) ?v_251) ?v_251) ?v_251) ?v_251) ?v_251) ?v_251) ?v_251) ?v_252) ?v_252) ?v_252) ?v_252) ?v_252) ?v_252) ?v_252) ?v_252) ?v_252) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_253) ?v_255) ?v_255) ?v_255) ?v_255) ?v_255) ?v_255) ?v_255) ?v_255) ?v_255) (and (and (and (and (and (and (and (and ?v_256 ?v_256) ?v_256) ?v_256) ?v_256) ?v_256) ?v_256) ?v_256) ?v_256)) (and ?v_257 (or (not (<= ?v_260 ?v_259)) (not (<= ?v_259 ?v_262))))) (and ?v_257 (or (not (<= ?v_260 ?v_261)) (not (<= ?v_261 ?v_262))))) (and ?v_257 (or (not (<= ?v_260 ?v_263)) (not (<= ?v_263 ?v_262))))) (and ?v_257 (or (not (<= ?v_260 ?v_264)) (not (<= ?v_264 ?v_262))))) (and ?v_257 (or (not (<= ?v_260 ?v_265)) (not (<= ?v_265 ?v_262))))) (and ?v_257 (or (not (<= ?v_260 ?v_266)) (not (<= ?v_266 ?v_262))))) (and ?v_257 (or (not (<= ?v_260 ?v_267)) (not (<= ?v_267 ?v_262))))) (and ?v_257 (or (not (<= ?v_260 ?v_268)) (not (<= ?v_268 ?v_262))))) (and ?v_257 (or (not (<= ?v_260 ?v_269)) (not (<= ?v_269 ?v_262))))) (and ?v_272 (or (or ?v_273 (not (<= ?v_274 ?v_270))) (not (<= ?v_270 ?v_276))))) (and ?v_272 (or (or ?v_273 (not (<= ?v_274 ?v_275))) (not (<= ?v_275 ?v_276))))) (and ?v_272 (or (or ?v_273 (not (<= ?v_274 ?v_277))) (not (<= ?v_277 ?v_276))))) (and ?v_272 (or (or ?v_273 (not (<= ?v_274 ?v_278))) (not (<= ?v_278 ?v_276))))) (and ?v_272 (or (or ?v_273 (not (<= ?v_274 ?v_279))) (not (<= ?v_279 ?v_276))))) (and ?v_272 (or (or ?v_273 (not (<= ?v_274 ?v_280))) (not (<= ?v_280 ?v_276))))) (and ?v_272 (or (or ?v_273 (not (<= ?v_274 ?v_281))) (not (<= ?v_281 ?v_276))))) (and ?v_272 (or (or ?v_273 (not (<= ?v_274 ?v_282))) (not (<= ?v_282 ?v_276))))) (and ?v_272 (or (or ?v_273 (not (<= ?v_274 ?v_283))) (not (<= ?v_283 ?v_276))))) ?v_288) ?v_288) ?v_288) ?v_288) ?v_288) ?v_288) ?v_288) ?v_288) ?v_288) (and ?v_289 (or (not (<= ?v_292 ?v_290)) (not (<= ?v_290 ?v_294))))) (and ?v_289 (or (not (<= ?v_292 ?v_293)) (not (<= ?v_293 ?v_294))))) (and ?v_289 (or (not (<= ?v_292 ?v_295)) (not (<= ?v_295 ?v_294))))) (and ?v_289 (or (not (<= ?v_292 ?v_296)) (not (<= ?v_296 ?v_294))))) (and ?v_289 (or (not (<= ?v_292 ?v_297)) (not (<= ?v_297 ?v_294))))) (and ?v_289 (or (not (<= ?v_292 ?v_298)) (not (<= ?v_298 ?v_294))))) (and ?v_289 (or (not (<= ?v_292 ?v_299)) (not (<= ?v_299 ?v_294))))) (and ?v_289 (or (not (<= ?v_292 ?v_300)) (not (<= ?v_300 ?v_294))))) (and ?v_289 (or (not (<= ?v_292 ?v_301)) (not (<= ?v_301 ?v_294))))) ?v_303) ?v_303) ?v_303) ?v_303) ?v_303) ?v_303) ?v_303) ?v_303) ?v_303) ?v_305) ?v_305) ?v_305) ?v_305) ?v_305) ?v_305) ?v_305) ?v_305) ?v_305)))))))))))))))))))))))))))))
(check-sat)
(exit)