-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathcardinality_1_1_2048_dual.vnnlib
314 lines (312 loc) · 16.9 KB
/
cardinality_1_1_2048_dual.vnnlib
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
(declare-const X_0 Real)
(declare-const X_1 Real)
(declare-const X_2 Real)
(declare-const X_3 Real)
(declare-const X_4 Real)
(declare-const X_5 Real)
(declare-const X_6 Real)
(declare-const X_7 Real)
(declare-const X_8 Real)
(declare-const X_9 Real)
(declare-const X_10 Real)
(declare-const X_11 Real)
(declare-const X_12 Real)
(declare-const X_13 Real)
(declare-const X_14 Real)
(declare-const X_15 Real)
(declare-const X_16 Real)
(declare-const X_17 Real)
(declare-const X_18 Real)
(declare-const X_19 Real)
(declare-const X_20 Real)
(declare-const X_21 Real)
(declare-const X_22 Real)
(declare-const X_23 Real)
(declare-const X_24 Real)
(declare-const X_25 Real)
(declare-const X_26 Real)
(declare-const X_27 Real)
(declare-const X_28 Real)
(declare-const X_29 Real)
(declare-const X_30 Real)
(declare-const X_31 Real)
(declare-const X_32 Real)
(declare-const X_33 Real)
(declare-const X_34 Real)
(declare-const X_35 Real)
(declare-const X_36 Real)
(declare-const X_37 Real)
(declare-const X_38 Real)
(declare-const X_39 Real)
(declare-const X_40 Real)
(declare-const X_41 Real)
(declare-const X_42 Real)
(declare-const X_43 Real)
(declare-const X_44 Real)
(declare-const X_45 Real)
(declare-const X_46 Real)
(declare-const X_47 Real)
(declare-const X_48 Real)
(declare-const X_49 Real)
(declare-const X_50 Real)
(declare-const X_51 Real)
(declare-const X_52 Real)
(declare-const X_53 Real)
(declare-const X_54 Real)
(declare-const X_55 Real)
(declare-const X_56 Real)
(declare-const X_57 Real)
(declare-const X_58 Real)
(declare-const X_59 Real)
(declare-const X_60 Real)
(declare-const X_61 Real)
(declare-const X_62 Real)
(declare-const X_63 Real)
(declare-const X_64 Real)
(declare-const X_65 Real)
(declare-const X_66 Real)
(declare-const X_67 Real)
(declare-const X_68 Real)
(declare-const X_69 Real)
(declare-const X_70 Real)
(declare-const X_71 Real)
(declare-const X_72 Real)
(declare-const X_73 Real)
(declare-const X_74 Real)
(declare-const X_75 Real)
(declare-const X_76 Real)
(declare-const X_77 Real)
(declare-const X_78 Real)
(declare-const X_79 Real)
(declare-const X_80 Real)
(declare-const X_81 Real)
(declare-const X_82 Real)
(declare-const X_83 Real)
(declare-const X_84 Real)
(declare-const X_85 Real)
(declare-const X_86 Real)
(declare-const X_87 Real)
(declare-const X_88 Real)
(declare-const X_89 Real)
(declare-const X_90 Real)
(declare-const X_91 Real)
(declare-const X_92 Real)
(declare-const X_93 Real)
(declare-const X_94 Real)
(declare-const X_95 Real)
(declare-const X_96 Real)
(declare-const X_97 Real)
(declare-const X_98 Real)
(declare-const X_99 Real)
(declare-const X_100 Real)
(declare-const X_101 Real)
(declare-const X_102 Real)
(declare-const X_103 Real)
(declare-const X_104 Real)
(declare-const X_105 Real)
(declare-const X_106 Real)
(declare-const X_107 Real)
(declare-const X_108 Real)
(declare-const X_109 Real)
(declare-const X_110 Real)
(declare-const X_111 Real)
(declare-const X_112 Real)
(declare-const X_113 Real)
(declare-const X_114 Real)
(declare-const X_115 Real)
(declare-const X_116 Real)
(declare-const X_117 Real)
(declare-const X_118 Real)
(declare-const X_119 Real)
(declare-const X_120 Real)
(declare-const X_121 Real)
(declare-const X_122 Real)
(declare-const X_123 Real)
(declare-const X_124 Real)
(declare-const X_125 Real)
(declare-const X_126 Real)
(declare-const X_127 Real)
(declare-const X_128 Real)
(declare-const X_129 Real)
(declare-const X_130 Real)
(declare-const X_131 Real)
(declare-const X_132 Real)
(declare-const X_133 Real)
(declare-const X_134 Real)
(declare-const X_135 Real)
(declare-const X_136 Real)
(declare-const X_137 Real)
(declare-const X_138 Real)
(declare-const X_139 Real)
(declare-const X_140 Real)
(declare-const X_141 Real)
(declare-const X_142 Real)
(declare-const X_143 Real)
(declare-const X_144 Real)
(declare-const X_145 Real)
(declare-const X_146 Real)
(declare-const X_147 Real)
(declare-const X_148 Real)
(declare-const X_149 Real)
(declare-const X_150 Real)
(declare-const X_151 Real)
(declare-const X_152 Real)
(declare-const X_153 Real)
(declare-const X_154 Real)
(declare-const X_155 Real)
(declare-const X_156 Real)
(declare-const X_157 Real)
(declare-const X_158 Real)
(declare-const X_159 Real)
(declare-const X_160 Real)
(declare-const X_161 Real)
(declare-const X_162 Real)
(declare-const X_163 Real)
(declare-const X_164 Real)
(declare-const X_165 Real)
(declare-const X_166 Real)
(declare-const X_167 Real)
(declare-const X_168 Real)
(declare-const X_169 Real)
(declare-const X_170 Real)
(declare-const X_171 Real)
(declare-const X_172 Real)
(declare-const X_173 Real)
(declare-const X_174 Real)
(declare-const X_175 Real)
(declare-const X_176 Real)
(declare-const X_177 Real)
(declare-const X_178 Real)
(declare-const X_179 Real)
(declare-const X_180 Real)
(declare-const X_181 Real)
(declare-const X_182 Real)
(declare-const X_183 Real)
(declare-const X_184 Real)
(declare-const X_185 Real)
(declare-const X_186 Real)
(declare-const X_187 Real)
(declare-const X_188 Real)
(declare-const X_189 Real)
(declare-const X_190 Real)
(declare-const X_191 Real)
(declare-const X_192 Real)
(declare-const X_193 Real)
(declare-const X_194 Real)
(declare-const X_195 Real)
(declare-const X_196 Real)
(declare-const X_197 Real)
(declare-const X_198 Real)
(declare-const X_199 Real)
(declare-const X_200 Real)
(declare-const X_201 Real)
(declare-const X_202 Real)
(declare-const X_203 Real)
(declare-const X_204 Real)
(declare-const X_205 Real)
(declare-const X_206 Real)
(declare-const X_207 Real)
(declare-const X_208 Real)
(declare-const X_209 Real)
(declare-const X_210 Real)
(declare-const X_211 Real)
(declare-const X_212 Real)
(declare-const X_213 Real)
(declare-const X_214 Real)
(declare-const X_215 Real)
(declare-const X_216 Real)
(declare-const X_217 Real)
(declare-const X_218 Real)
(declare-const X_219 Real)
(declare-const X_220 Real)
(declare-const X_221 Real)
(declare-const X_222 Real)
(declare-const X_223 Real)
(declare-const X_224 Real)
(declare-const X_225 Real)
(declare-const X_226 Real)
(declare-const X_227 Real)
(declare-const X_228 Real)
(declare-const X_229 Real)
(declare-const X_230 Real)
(declare-const X_231 Real)
(declare-const X_232 Real)
(declare-const X_233 Real)
(declare-const X_234 Real)
(declare-const X_235 Real)
(declare-const X_236 Real)
(declare-const X_237 Real)
(declare-const X_238 Real)
(declare-const X_239 Real)
(declare-const X_240 Real)
(declare-const X_241 Real)
(declare-const X_242 Real)
(declare-const X_243 Real)
(declare-const X_244 Real)
(declare-const X_245 Real)
(declare-const X_246 Real)
(declare-const X_247 Real)
(declare-const X_248 Real)
(declare-const X_249 Real)
(declare-const X_250 Real)
(declare-const X_251 Real)
(declare-const X_252 Real)
(declare-const X_253 Real)
(declare-const X_254 Real)
(declare-const X_255 Real)
(declare-const X_256 Real)
(declare-const X_257 Real)
(declare-const X_258 Real)
(declare-const X_259 Real)
(declare-const X_260 Real)
(declare-const X_261 Real)
(declare-const X_262 Real)
(declare-const X_263 Real)
(declare-const X_264 Real)
(declare-const X_265 Real)
(declare-const X_266 Real)
(declare-const X_267 Real)
(declare-const X_268 Real)
(declare-const X_269 Real)
(declare-const X_270 Real)
(declare-const X_271 Real)
(declare-const X_272 Real)
(declare-const X_273 Real)
(declare-const X_274 Real)
(declare-const X_275 Real)
(declare-const X_276 Real)
(declare-const X_277 Real)
(declare-const X_278 Real)
(declare-const X_279 Real)
(declare-const X_280 Real)
(declare-const X_281 Real)
(declare-const X_282 Real)
(declare-const X_283 Real)
(declare-const X_284 Real)
(declare-const X_285 Real)
(declare-const X_286 Real)
(declare-const X_287 Real)
(declare-const X_288 Real)
(declare-const X_289 Real)
(declare-const X_290 Real)
(declare-const X_291 Real)
(declare-const X_292 Real)
(declare-const X_293 Real)
(declare-const X_294 Real)
(declare-const X_295 Real)
(declare-const X_296 Real)
(declare-const X_297 Real)
(declare-const X_298 Real)
(declare-const X_299 Real)
(declare-const X_300 Real)
(declare-const X_301 Real)
(declare-const X_302 Real)
(declare-const X_303 Real)
(declare-const X_304 Real)
(declare-const X_305 Real)
(declare-const X_306 Real)
(declare-const X_307 Real)
(declare-const Y_0 Real)
(assert (or
(and (>= X_0 0.0) (<= X_0 0.0) (>= X_1 0.0) (<= X_1 0.0) (>= X_2 0.0) (<= X_2 0.0) (>= X_3 0.0) (<= X_3 0.0) (>= X_4 1.0) (<= X_4 1.0) (>= X_5 0.0) (<= X_5 0.0) (>= X_6 1.0) (<= X_6 1.0) (>= X_7 0.0) (<= X_7 0.0) (>= X_8 0.0) (<= X_8 0.0) (>= X_9 0.0) (<= X_9 0.0) (>= X_10 0.0) (<= X_10 0.0) (>= X_11 0.0) (<= X_11 0.0) (>= X_12 0.0) (<= X_12 0.0) (>= X_13 0.0) (<= X_13 0.0) (>= X_14 0.0) (<= X_14 0.0) (>= X_15 0.0) (<= X_15 0.0) (>= X_16 0.0) (<= X_16 0.0) (>= X_17 0.0) (<= X_17 0.0) (>= X_18 0.0) (<= X_18 0.0) (>= X_19 0.0) (<= X_19 0.0) (>= X_20 0.0) (<= X_20 0.0) (>= X_21 0.0) (<= X_21 0.0) (>= X_22 0.0) (<= X_22 0.0) (>= X_23 0.0) (<= X_23 0.0) (>= X_24 0.0) (<= X_24 0.0) (>= X_25 0.0) (<= X_25 0.0) (>= X_26 0.0) (<= X_26 0.0) (>= X_27 0.0) (<= X_27 0.0) (>= X_28 0.0) (<= X_28 0.0) (>= X_29 0.0) (<= X_29 0.0) (>= X_30 0.0) (<= X_30 0.0) (>= X_31 0.0) (<= X_31 0.0) (>= X_32 0.0) (<= X_32 0.0) (>= X_33 0.0) (<= X_33 0.0) (>= X_34 0.0) (<= X_34 0.0) (>= X_35 0.0) (<= X_35 0.0) (>= X_36 0.0) (<= X_36 0.0) (>= X_37 0.0) (<= X_37 0.0) (>= X_38 0.0) (<= X_38 0.0) (>= X_39 0.0) (<= X_39 0.0) (>= X_40 0.0) (<= X_40 0.0) (>= X_41 0.0) (<= X_41 0.0) (>= X_42 0.0) (<= X_42 0.0) (>= X_43 0.0) (<= X_43 0.0) (>= X_44 0.0) (<= X_44 0.0) (>= X_45 0.0) (<= X_45 0.0) (>= X_46 0.0) (<= X_46 0.0) (>= X_47 0.0) (<= X_47 0.0) (>= X_48 1.0) (<= X_48 1.0) (>= X_49 0.0) (<= X_49 0.0) (>= X_50 0.0) (<= X_50 0.0) (>= X_51 0.0) (<= X_51 0.0) (>= X_52 0.0) (<= X_52 0.0) (>= X_53 1.0) (<= X_53 1.0) (>= X_54 0.2688847780227661) (<= X_54 0.2688847780227661) (>= X_55 1.0) (<= X_55 1.0) (>= X_56 0.0) (<= X_56 0.0) (>= X_57 0.0) (<= X_57 0.0) (>= X_58 0.0) (<= X_58 0.0) (>= X_59 0.0) (<= X_59 0.0) (>= X_60 0.0) (<= X_60 0.0) (>= X_61 0.0) (<= X_61 0.0) (>= X_62 0.0) (<= X_62 0.0) (>= X_63 0.0) (<= X_63 0.0) (>= X_64 0.0) (<= X_64 0.0) (>= X_65 0.0) (<= X_65 0.0) (>= X_66 0.0) (<= X_66 0.0) (>= X_67 0.0) (<= X_67 0.0) (>= X_68 0.0) (<= X_68 0.0) (>= X_69 0.0) (<= X_69 0.0) (>= X_70 0.0) (<= X_70 0.0) (>= X_71 0.0) (<= X_71 0.0) (>= X_72 0.0) (<= X_72 0.0) (>= X_73 0.0) (<= X_73 0.0) (>= X_74 0.0) (<= X_74 0.0) (>= X_75 0.0) (<= X_75 0.0) (>= X_76 0.0) (<= X_76 0.0) (>= X_77 0.0) (<= X_77 0.0) (>= X_78 0.0) (<= X_78 0.0) (>= X_79 0.0) (<= X_79 0.0) (>= X_80 0.0) (<= X_80 0.0) (>= X_81 0.0) (<= X_81 0.0) (>= X_82 0.0) (<= X_82 0.0) (>= X_83 0.0) (<= X_83 0.0) (>= X_84 0.0) (<= X_84 0.0) (>= X_85 0.0) (<= X_85 0.0) (>= X_86 0.0) (<= X_86 0.0) (>= X_87 0.0) (<= X_87 0.0) (>= X_88 0.0) (<= X_88 0.0) (>= X_89 0.0) (<= X_89 0.0) (>= X_90 0.0) (<= X_90 0.0) (>= X_91 0.0) (<= X_91 0.0) (>= X_92 0.0) (<= X_92 0.0) (>= X_93 0.0) (<= X_93 0.0) (>= X_94 0.0) (<= X_94 0.0) (>= X_95 0.0) (<= X_95 0.0) (>= X_96 0.0) (<= X_96 0.0) (>= X_97 0.0) (<= X_97 0.0) (>= X_98 0.0) (<= X_98 0.0) (>= X_99 0.0) (<= X_99 0.0) (>= X_100 0.0) (<= X_100 0.0) (>= X_101 0.0) (<= X_101 0.0) (>= X_102 0.0) (<= X_102 0.0) (>= X_103 0.0) (<= X_103 0.0) (>= X_104 0.0) (<= X_104 0.0) (>= X_105 0.0) (<= X_105 0.0) (>= X_106 0.0) (<= X_106 0.0) (>= X_107 0.0) (<= X_107 0.0) (>= X_108 0.0) (<= X_108 0.0) (>= X_109 0.0) (<= X_109 0.0) (>= X_110 0.0) (<= X_110 0.0) (>= X_111 0.0) (<= X_111 0.0) (>= X_112 0.0) (<= X_112 0.0) (>= X_113 0.0) (<= X_113 0.0) (>= X_114 0.0) (<= X_114 0.0) (>= X_115 0.0) (<= X_115 0.0) (>= X_116 0.0) (<= X_116 0.0) (>= X_117 0.0) (<= X_117 0.0) (>= X_118 0.0) (<= X_118 0.0) (>= X_119 0.0) (<= X_119 0.0) (>= X_120 0.0) (<= X_120 0.0) (>= X_121 0.0) (<= X_121 0.0) (>= X_122 0.0) (<= X_122 0.0) (>= X_123 0.0) (<= X_123 0.0) (>= X_124 0.0) (<= X_124 0.0) (>= X_125 0.0) (<= X_125 0.0) (>= X_126 1.0) (<= X_126 1.0) (>= X_127 0.0) (<= X_127 0.0) (>= X_128 0.0) (<= X_128 0.0) (>= X_129 0.0) (<= X_129 0.0) (>= X_130 0.0) (<= X_130 0.0) (>= X_131 0.0) (<= X_131 0.0) (>= X_132 1.0) (<= X_132 1.0) (>= X_133 0.0) (<= X_133 0.0) (>= X_134 0.0) (<= X_134 0.0) (>= X_135 0.0) (<= X_135 0.0) (>= X_136 0.0) (<= X_136 0.0) (>= X_137 0.0) (<= X_137 0.0) (>= X_138 0.0) (<= X_138 0.0) (>= X_139 0.0) (<= X_139 0.0) (>= X_140 0.0) (<= X_140 0.0) (>= X_141 0.0) (<= X_141 0.0) (>= X_142 0.0) (<= X_142 0.0) (>= X_143 0.0) (<= X_143 0.0) (>= X_144 0.0) (<= X_144 0.0) (>= X_145 0.0) (<= X_145 0.0) (>= X_146 0.0) (<= X_146 0.0) (>= X_147 0.0) (<= X_147 0.0) (>= X_148 0.0) (<= X_148 0.0) (>= X_149 0.0) (<= X_149 0.0) (>= X_150 0.0) (<= X_150 0.0) (>= X_151 0.0) (<= X_151 0.0) (>= X_152 0.0) (<= X_152 0.0) (>= X_153 0.0) (<= X_153 0.0) (>= X_154 0.0) (<= X_154 0.0) (>= X_155 0.0) (<= X_155 0.0) (>= X_156 0.0) (<= X_156 0.0) (>= X_157 0.0) (<= X_157 0.0) (>= X_158 1.0) (<= X_158 1.0) (>= X_159 0.0) (<= X_159 0.0) (>= X_160 1.0) (<= X_160 1.0) (>= X_161 0.0) (<= X_161 0.0) (>= X_162 0.0) (<= X_162 0.0) (>= X_163 0.0) (<= X_163 0.0) (>= X_164 0.0) (<= X_164 0.0) (>= X_165 0.0) (<= X_165 0.0) (>= X_166 0.0) (<= X_166 0.0) (>= X_167 0.0) (<= X_167 0.0) (>= X_168 0.0) (<= X_168 0.0) (>= X_169 0.0) (<= X_169 0.0) (>= X_170 0.0) (<= X_170 0.0) (>= X_171 0.0) (<= X_171 0.0) (>= X_172 0.0) (<= X_172 0.0) (>= X_173 0.0) (<= X_173 0.0) (>= X_174 0.0) (<= X_174 0.0) (>= X_175 0.0) (<= X_175 0.0) (>= X_176 0.0) (<= X_176 0.0) (>= X_177 0.0) (<= X_177 0.0) (>= X_178 0.0) (<= X_178 0.0) (>= X_179 0.0) (<= X_179 0.0) (>= X_180 0.0) (<= X_180 0.0) (>= X_181 0.0) (<= X_181 0.0) (>= X_182 0.0) (<= X_182 0.0) (>= X_183 0.0) (<= X_183 0.0) (>= X_184 0.0) (<= X_184 0.0) (>= X_185 0.0) (<= X_185 0.0) (>= X_186 0.0) (<= X_186 0.0) (>= X_187 0.0) (<= X_187 0.0) (>= X_188 0.0) (<= X_188 0.0) (>= X_189 0.0) (<= X_189 0.0) (>= X_190 0.0) (<= X_190 0.0) (>= X_191 0.0) (<= X_191 0.0) (>= X_192 0.0) (<= X_192 0.0) (>= X_193 0.0) (<= X_193 0.0) (>= X_194 0.0) (<= X_194 0.0) (>= X_195 0.0) (<= X_195 0.0) (>= X_196 0.0) (<= X_196 0.0) (>= X_197 0.0) (<= X_197 0.0) (>= X_198 0.0) (<= X_198 0.0) (>= X_199 0.0) (<= X_199 0.0) (>= X_200 0.0) (<= X_200 0.0) (>= X_201 0.0) (<= X_201 0.0) (>= X_202 1.0) (<= X_202 1.0) (>= X_203 0.0) (<= X_203 0.0) (>= X_204 0.0) (<= X_204 0.0) (>= X_205 0.0) (<= X_205 0.0) (>= X_206 0.0) (<= X_206 0.0) (>= X_207 0.0) (<= X_207 0.9999) (>= X_208 0.2688847780227661) (<= X_208 0.2688847780227661) (>= X_209 1.0) (<= X_209 1.0) (>= X_210 0.0) (<= X_210 0.0) (>= X_211 0.0) (<= X_211 0.0) (>= X_212 0.0) (<= X_212 0.0) (>= X_213 0.0) (<= X_213 0.0) (>= X_214 0.0) (<= X_214 0.0) (>= X_215 0.0) (<= X_215 0.0) (>= X_216 0.0) (<= X_216 0.0) (>= X_217 0.0) (<= X_217 0.0) (>= X_218 0.0) (<= X_218 0.0) (>= X_219 0.0) (<= X_219 0.0) (>= X_220 0.0) (<= X_220 0.0) (>= X_221 0.0) (<= X_221 0.0) (>= X_222 0.0) (<= X_222 0.0) (>= X_223 0.0) (<= X_223 0.0) (>= X_224 0.0) (<= X_224 0.0) (>= X_225 0.0) (<= X_225 0.0) (>= X_226 0.0) (<= X_226 0.0) (>= X_227 0.0) (<= X_227 0.0) (>= X_228 0.0) (<= X_228 0.0) (>= X_229 0.0) (<= X_229 0.0) (>= X_230 0.0) (<= X_230 0.0) (>= X_231 0.0) (<= X_231 0.0) (>= X_232 0.0) (<= X_232 0.0) (>= X_233 0.0) (<= X_233 0.0) (>= X_234 0.0) (<= X_234 0.0) (>= X_235 0.0) (<= X_235 0.0) (>= X_236 0.0) (<= X_236 0.0) (>= X_237 0.0) (<= X_237 0.0) (>= X_238 0.0) (<= X_238 0.0) (>= X_239 0.0) (<= X_239 0.0) (>= X_240 0.0) (<= X_240 0.0) (>= X_241 0.0) (<= X_241 0.0) (>= X_242 0.0) (<= X_242 0.0) (>= X_243 0.0) (<= X_243 0.0) (>= X_244 0.0) (<= X_244 0.0) (>= X_245 0.0) (<= X_245 0.0) (>= X_246 0.0) (<= X_246 0.0) (>= X_247 0.0) (<= X_247 0.0) (>= X_248 0.0) (<= X_248 0.0) (>= X_249 0.0) (<= X_249 0.0) (>= X_250 0.0) (<= X_250 0.0) (>= X_251 0.0) (<= X_251 0.0) (>= X_252 0.0) (<= X_252 0.0) (>= X_253 0.0) (<= X_253 0.0) (>= X_254 0.0) (<= X_254 0.0) (>= X_255 0.0) (<= X_255 0.0) (>= X_256 0.0) (<= X_256 0.0) (>= X_257 0.0) (<= X_257 0.0) (>= X_258 0.0) (<= X_258 0.0) (>= X_259 0.0) (<= X_259 0.0) (>= X_260 0.0) (<= X_260 0.0) (>= X_261 0.0) (<= X_261 0.0) (>= X_262 0.0) (<= X_262 0.0) (>= X_263 0.0) (<= X_263 0.0) (>= X_264 0.0) (<= X_264 0.0) (>= X_265 0.0) (<= X_265 0.0) (>= X_266 0.0) (<= X_266 0.0) (>= X_267 0.0) (<= X_267 0.0) (>= X_268 0.0) (<= X_268 0.0) (>= X_269 0.0) (<= X_269 0.0) (>= X_270 0.0) (<= X_270 0.0) (>= X_271 0.0) (<= X_271 0.0) (>= X_272 0.0) (<= X_272 0.0) (>= X_273 0.0) (<= X_273 0.0) (>= X_274 0.0) (<= X_274 0.0) (>= X_275 0.0) (<= X_275 0.0) (>= X_276 0.0) (<= X_276 0.0) (>= X_277 0.0) (<= X_277 0.0) (>= X_278 0.0) (<= X_278 0.0) (>= X_279 0.0) (<= X_279 0.0) (>= X_280 1.0) (<= X_280 1.0) (>= X_281 0.0) (<= X_281 0.0) (>= X_282 0.0) (<= X_282 0.0) (>= X_283 0.0) (<= X_283 0.0) (>= X_284 0.0) (<= X_284 0.0) (>= X_285 0.0) (<= X_285 0.0) (>= X_286 1.0) (<= X_286 1.0) (>= X_287 0.0) (<= X_287 0.0) (>= X_288 0.0) (<= X_288 0.0) (>= X_289 0.0) (<= X_289 0.0) (>= X_290 0.0) (<= X_290 0.0) (>= X_291 0.0) (<= X_291 0.0) (>= X_292 0.0) (<= X_292 0.0) (>= X_293 0.0) (<= X_293 0.0) (>= X_294 0.0) (<= X_294 0.0) (>= X_295 0.0) (<= X_295 0.0) (>= X_296 0.0) (<= X_296 0.0) (>= X_297 0.0) (<= X_297 0.0) (>= X_298 0.0) (<= X_298 0.0) (>= X_299 0.0) (<= X_299 0.0) (>= X_300 0.0) (<= X_300 0.0) (>= X_301 0.0) (<= X_301 0.0) (>= X_302 0.0) (<= X_302 0.0) (>= X_303 0.0) (<= X_303 0.0) (>= X_304 0.0) (<= X_304 0.0) (>= X_305 0.0) (<= X_305 0.0) (>= X_306 0.0) (<= X_306 0.0) (>= X_307 0.0) (<= X_307 0.0) (<= Y_0 -1e-5))
))