File: normalized-bench1.pi.opb

package info (click to toggle)
sat4j 2.3.5-0.3
  • links: PTS
  • area: main
  • in suites: bookworm, bullseye, buster, sid, trixie
  • size: 90,260 kB
  • sloc: java: 50,309; xml: 1,491; lisp: 95; makefile: 36; sh: 35
file content (401 lines) | stat: -rw-r--r-- 127,434 bytes parent folder | download | duplicates (5)
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
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
* #variable= 4677 #constraint= 398
* converted from file: submitted/manquinho/logic-synthesis/bench1.pi.opb.bz2
min: +1*x1 +1*x2 +1*x3 +1*x4 +1*x5 +1*x6 +1*x7 +1*x8 +1*x9 +1*x10 +1*x11 +1*x12 +1*x13 +1*x14 +1*x15 +1*x16 +1*x17 +1*x18 +1*x19 +1*x20 +1*x21 +1*x22 +1*x23 +1*x24 +1*x25 +1*x26 +1*x27 +1*x28 +1*x29 +1*x30 +1*x31 +1*x32 +1*x33 +1*x34 +1*x35 +1*x36 +1*x37 +1*x38 +1*x39 +1*x40 +1*x41 +1*x42 +1*x43 +1*x44 +1*x45 +1*x46 +1*x47 +1*x48 +1*x49 +1*x50 +1*x51 +1*x52 +1*x53 +1*x54 +1*x55 +1*x56 +1*x57 +1*x58 +1*x59 +1*x60 +1*x61 +1*x62 +1*x63 +1*x64 +1*x65 +1*x66 +1*x67 +1*x68 +1*x69 +1*x70 +1*x71 +1*x72 +1*x73 +1*x74 +1*x75 +1*x76 +1*x77 +1*x78 +1*x79 +1*x80 +1*x81 +1*x82 +1*x83 +1*x84 +1*x85 +1*x86 +1*x87 +1*x88 +1*x89 +1*x90 +1*x91 +1*x92 +1*x93 +1*x94 +1*x95 +1*x96 +1*x97 +1*x98 +1*x99 +1*x100 +1*x101 +1*x102 +1*x103 +1*x104 +1*x105 +1*x106 +1*x107 +1*x108 +1*x109 +1*x110 +1*x111 +1*x112 +1*x113 +1*x114 +1*x115 +1*x116 +1*x117 +1*x118 +1*x119 +1*x120 +1*x121 +1*x122 +1*x123 +1*x124 +1*x125 +1*x126 +1*x127 +1*x128 +1*x129 +1*x130 +1*x131 +1*x132 +1*x133 +1*x134 +1*x135 +1*x136 +1*x137 +1*x138 +1*x139 +1*x140 +1*x141 +1*x142 +1*x143 +1*x144 +1*x145 +1*x146 +1*x147 +1*x148 +1*x149 +1*x150 +1*x151 +1*x152 +1*x153 +1*x154 +1*x155 +1*x156 +1*x157 +1*x158 +1*x159 +1*x160 +1*x161 +1*x162 +1*x163 +1*x164 +1*x165 +1*x166 +1*x167 +1*x168 +1*x169 +1*x170 +1*x171 +1*x172 +1*x173 +1*x174 +1*x175 +1*x176 +1*x177 +1*x178 +1*x179 +1*x180 +1*x181 +1*x182 +1*x183 +1*x184 +1*x185 +1*x186 +1*x187 +1*x188 +1*x189 +1*x190 +1*x191 +1*x192 +1*x193 +1*x194 +1*x195 +1*x196 +1*x197 +1*x198 +1*x199 +1*x200 +1*x201 +1*x202 +1*x203 +1*x204 +1*x205 +1*x206 +1*x207 +1*x208 +1*x209 +1*x210 +1*x211 +1*x212 +1*x213 +1*x214 +1*x215 +1*x216 +1*x217 +1*x218 +1*x219 +1*x220 +1*x221 +1*x222 +1*x223 +1*x224 +1*x225 +1*x226 +1*x227 +1*x228 +1*x229 +1*x230 +1*x231 +1*x232 +1*x233 +1*x234 +1*x235 +1*x236 +1*x237 +1*x238 +1*x239 +1*x240 +1*x241 +1*x242 +1*x243 +1*x244 +1*x245 +1*x246 +1*x247 +1*x248 +1*x249 +1*x250 +1*x251 +1*x252 +1*x253 +1*x254 +1*x255 +1*x256 +1*x257 +1*x258 +1*x259 +1*x260 +1*x261 +1*x262 +1*x263 +1*x264 +1*x265 +1*x266 +1*x267 +1*x268 +1*x269 +1*x270 +1*x271 +1*x272 +1*x273 +1*x274 +1*x275 +1*x276 +1*x277 +1*x278 +1*x279 +1*x280 +1*x281 +1*x282 +1*x283 +1*x284 +1*x285 +1*x286 +1*x287 +1*x288 +1*x289 +1*x290 +1*x291 +1*x292 +1*x293 +1*x294 +1*x295 +1*x296 +1*x297 +1*x298 +1*x299 +1*x300 +1*x301 +1*x302 +1*x303 +1*x304 +1*x305 +1*x306 +1*x307 +1*x308 +1*x309 +1*x310 +1*x311 +1*x312 +1*x313 +1*x314 +1*x315 +1*x316 +1*x317 +1*x318 +1*x319 +1*x320 +1*x321 +1*x322 +1*x323 +1*x324 +1*x325 +1*x326 +1*x327 +1*x328 +1*x329 +1*x330 +1*x331 +1*x332 +1*x333 +1*x334 +1*x335 +1*x336 +1*x337 +1*x338 +1*x339 +1*x340 +1*x341 +1*x342 +1*x343 +1*x344 +1*x345 +1*x346 +1*x347 +1*x348 +1*x349 +1*x350 +1*x351 +1*x352 +1*x353 +1*x354 +1*x355 +1*x356 +1*x357 +1*x358 +1*x359 +1*x360 +1*x361 +1*x362 +1*x363 +1*x364 +1*x365 +1*x366 +1*x367 +1*x368 +1*x369 +1*x370 +1*x371 +1*x372 +1*x373 +1*x374 +1*x375 +1*x376 +1*x377 +1*x378 +1*x379 +1*x380 +1*x381 +1*x382 +1*x383 +1*x384 +1*x385 +1*x386 +1*x387 +1*x388 +1*x389 +1*x390 +1*x391 +1*x392 +1*x393 +1*x394 +1*x395 +1*x396 +1*x397 +1*x398 +1*x399 +1*x400 +1*x401 +1*x402 +1*x403 +1*x404 +1*x405 +1*x406 +1*x407 +1*x408 +1*x409 +1*x410 +1*x411 +1*x412 +1*x413 +1*x414 +1*x415 +1*x416 +1*x417 +1*x418 +1*x419 +1*x420 +1*x421 +1*x422 +1*x423 +1*x424 +1*x425 +1*x426 +1*x427 +1*x428 +1*x429 +1*x430 +1*x431 +1*x432 +1*x433 +1*x434 +1*x435 +1*x436 +1*x437 +1*x438 +1*x439 +1*x440 +1*x441 +1*x442 +1*x443 +1*x444 +1*x445 +1*x446 +1*x447 +1*x448 +1*x449 +1*x450 +1*x451 +1*x452 +1*x453 +1*x454 +1*x455 +1*x456 +1*x457 +1*x458 +1*x459 +1*x460 +1*x461 +1*x462 +1*x463 +1*x464 +1*x465 +1*x466 +1*x467 +1*x468 +1*x469 +1*x470 +1*x471 +1*x472 +1*x473 +1*x474 +1*x475 +1*x476 +1*x477 +1*x478 +1*x479 +1*x480 +1*x481 +1*x482 +1*x483 +1*x484 +1*x485 +1*x486 +1*x487 +1*x488 +1*x489 +1*x490 +1*x491 +1*x492 +1*x493 +1*x494 +1*x495 +1*x496 +1*x497 +1*x498 +1*x499 +1*x500 +1*x501 +1*x502 +1*x503 +1*x504 +1*x505 +1*x506 +1*x507 +1*x508 +1*x509 +1*x510 +1*x511 +1*x512 +1*x513 +1*x514 +1*x515 +1*x516 +1*x517 +1*x518 +1*x519 +1*x520 +1*x521 +1*x522 +1*x523 +1*x524 +1*x525 +1*x526 +1*x527 +1*x528 +1*x529 +1*x530 +1*x531 +1*x532 +1*x533 +1*x534 +1*x535 +1*x536 +1*x537 +1*x538 +1*x539 +1*x540 +1*x541 +1*x542 +1*x543 +1*x544 +1*x545 +1*x546 +1*x547 +1*x548 +1*x549 +1*x550 +1*x551 +1*x552 +1*x553 +1*x554 +1*x555 +1*x556 +1*x557 +1*x558 +1*x559 +1*x560 +1*x561 +1*x562 +1*x563 +1*x564 +1*x565 +1*x566 +1*x567 +1*x568 +1*x569 +1*x570 +1*x571 +1*x572 +1*x573 +1*x574 +1*x575 +1*x576 +1*x577 +1*x578 +1*x579 +1*x580 +1*x581 +1*x582 +1*x583 +1*x584 +1*x585 +1*x586 +1*x587 +1*x588 +1*x589 +1*x590 +1*x591 +1*x592 +1*x593 +1*x594 +1*x595 +1*x596 +1*x597 +1*x598 +1*x599 +1*x600 +1*x601 +1*x602 +1*x603 +1*x604 +1*x605 +1*x606 +1*x607 +1*x608 +1*x609 +1*x610 +1*x611 +1*x612 +1*x613 +1*x614 +1*x615 +1*x616 +1*x617 +1*x618 +1*x619 +1*x620 +1*x621 +1*x622 +1*x623 +1*x624 +1*x625 +1*x626 +1*x627 +1*x628 +1*x629 +1*x630 +1*x631 +1*x632 +1*x633 +1*x634 +1*x635 +1*x636 +1*x637 +1*x638 +1*x639 +1*x640 +1*x641 +1*x642 +1*x643 +1*x644 +1*x645 +1*x646 +1*x647 +1*x648 +1*x649 +1*x650 +1*x651 +1*x652 +1*x653 +1*x654 +1*x655 +1*x656 +1*x657 +1*x658 +1*x659 +1*x660 +1*x661 +1*x662 +1*x663 +1*x664 +1*x665 +1*x666 +1*x667 +1*x668 +1*x669 +1*x670 +1*x671 +1*x672 +1*x673 +1*x674 +1*x675 +1*x676 +1*x677 +1*x678 +1*x679 +1*x680 +1*x681 +1*x682 +1*x683 +1*x684 +1*x685 +1*x686 +1*x687 +1*x688 +1*x689 +1*x690 +1*x691 +1*x692 +1*x693 +1*x694 +1*x695 +1*x696 +1*x697 +1*x698 +1*x699 +1*x700 +1*x701 +1*x702 +1*x703 +1*x704 +1*x705 +1*x706 +1*x707 +1*x708 +1*x709 +1*x710 +1*x711 +1*x712 +1*x713 +1*x714 +1*x715 +1*x716 +1*x717 +1*x718 +1*x719 +1*x720 +1*x721 +1*x722 +1*x723 +1*x724 +1*x725 +1*x726 +1*x727 +1*x728 +1*x729 +1*x730 +1*x731 +1*x732 +1*x733 +1*x734 +1*x735 +1*x736 +1*x737 +1*x738 +1*x739 +1*x740 +1*x741 +1*x742 +1*x743 +1*x744 +1*x745 +1*x746 +1*x747 +1*x748 +1*x749 +1*x750 +1*x751 +1*x752 +1*x753 +1*x754 +1*x755 +1*x756 +1*x757 +1*x758 +1*x759 +1*x760 +1*x761 +1*x762 +1*x763 +1*x764 +1*x765 +1*x766 +1*x767 +1*x768 +1*x769 +1*x770 +1*x771 +1*x772 +1*x773 +1*x774 +1*x775 +1*x776 +1*x777 +1*x778 +1*x779 +1*x780 +1*x781 +1*x782 +1*x783 +1*x784 +1*x785 +1*x786 +1*x787 +1*x788 +1*x789 +1*x790 +1*x791 +1*x792 +1*x793 +1*x794 +1*x795 +1*x796 +1*x797 +1*x798 +1*x799 +1*x800 +1*x801 +1*x802 +1*x803 +1*x804 +1*x805 +1*x806 +1*x807 +1*x808 +1*x809 +1*x810 +1*x811 +1*x812 +1*x813 +1*x814 +1*x815 +1*x816 +1*x817 +1*x818 +1*x819 +1*x820 +1*x821 +1*x822 +1*x823 +1*x824 +1*x825 +1*x826 +1*x827 +1*x828 +1*x829 +1*x830 +1*x831 +1*x832 +1*x833 +1*x834 +1*x835 +1*x836 +1*x837 +1*x838 +1*x839 +1*x840 +1*x841 +1*x842 +1*x843 +1*x844 +1*x845 +1*x846 +1*x847 +1*x848 +1*x849 +1*x850 +1*x851 +1*x852 +1*x853 +1*x854 +1*x855 +1*x856 +1*x857 +1*x858 +1*x859 +1*x860 +1*x861 +1*x862 +1*x863 +1*x864 +1*x865 +1*x866 +1*x867 +1*x868 +1*x869 +1*x870 +1*x871 +1*x872 +1*x873 +1*x874 +1*x875 +1*x876 +1*x877 +1*x878 +1*x879 +1*x880 +1*x881 +1*x882 +1*x883 +1*x884 +1*x885 +1*x886 +1*x887 +1*x888 +1*x889 +1*x890 +1*x891 +1*x892 +1*x893 +1*x894 +1*x895 +1*x896 +1*x897 +1*x898 +1*x899 +1*x900 +1*x901 +1*x902 +1*x903 +1*x904 +1*x905 +1*x906 +1*x907 +1*x908 +1*x909 +1*x910 +1*x911 +1*x912 +1*x913 +1*x914 +1*x915 +1*x916 +1*x917 +1*x918 +1*x919 +1*x920 +1*x921 +1*x922 +1*x923 +1*x924 +1*x925 +1*x926 +1*x927 +1*x928 +1*x929 +1*x930 +1*x931 +1*x932 +1*x933 +1*x934 +1*x935 +1*x936 +1*x937 +1*x938 +1*x939 +1*x940 +1*x941 +1*x942 +1*x943 +1*x944 +1*x945 +1*x946 +1*x947 +1*x948 +1*x949 +1*x950 +1*x951 +1*x952 +1*x953 +1*x954 +1*x955 +1*x956 +1*x957 +1*x958 +1*x959 +1*x960 +1*x961 +1*x962 +1*x963 +1*x964 +1*x965 +1*x966 +1*x967 +1*x968 +1*x969 +1*x970 +1*x971 +1*x972 +1*x973 +1*x974 +1*x975 +1*x976 +1*x977 +1*x978 +1*x979 +1*x980 +1*x981 +1*x982 +1*x983 +1*x984 +1*x985 +1*x986 +1*x987 +1*x988 +1*x989 +1*x990 +1*x991 +1*x992 +1*x993 +1*x994 +1*x995 +1*x996 +1*x997 +1*x998 +1*x999 +1*x1000 +1*x1001 +1*x1002 +1*x1003 +1*x1004 +1*x1005 +1*x1006 +1*x1007 +1*x1008 +1*x1009 +1*x1010 +1*x1011 +1*x1012 +1*x1013 +1*x1014 +1*x1015 +1*x1016 +1*x1017 +1*x1018 +1*x1019 +1*x1020 +1*x1021 +1*x1022 +1*x1023 +1*x1024 +1*x1025 +1*x1026 +1*x1027 +1*x1028 +1*x1029 +1*x1030 +1*x1031 +1*x1032 +1*x1033 +1*x1034 +1*x1035 +1*x1036 +1*x1037 +1*x1038 +1*x1039 +1*x1040 +1*x1041 +1*x1042 +1*x1043 +1*x1044 +1*x1045 +1*x1046 +1*x1047 +1*x1048 +1*x1049 +1*x1050 +1*x1051 +1*x1052 +1*x1053 +1*x1054 +1*x1055 +1*x1056 +1*x1057 +1*x1058 +1*x1059 +1*x1060 +1*x1061 +1*x1062 +1*x1063 +1*x1064 +1*x1065 +1*x1066 +1*x1067 +1*x1068 +1*x1069 +1*x1070 +1*x1071 +1*x1072 +1*x1073 +1*x1074 +1*x1075 +1*x1076 +1*x1077 +1*x1078 +1*x1079 +1*x1080 +1*x1081 +1*x1082 +1*x1083 +1*x1084 +1*x1085 +1*x1086 +1*x1087 +1*x1088 +1*x1089 +1*x1090 +1*x1091 +1*x1092 +1*x1093 +1*x1094 +1*x1095 +1*x1096 +1*x1097 +1*x1098 +1*x1099 +1*x1100 +1*x1101 +1*x1102 +1*x1103 +1*x1104 +1*x1105 +1*x1106 +1*x1107 +1*x1108 +1*x1109 +1*x1110 +1*x1111 +1*x1112 +1*x1113 +1*x1114 +1*x1115 +1*x1116 +1*x1117 +1*x1118 +1*x1119 +1*x1120 +1*x1121 +1*x1122 +1*x1123 +1*x1124 +1*x1125 +1*x1126 +1*x1127 +1*x1128 +1*x1129 +1*x1130 +1*x1131 +1*x1132 +1*x1133 +1*x1134 +1*x1135 +1*x1136 +1*x1137 +1*x1138 +1*x1139 +1*x1140 +1*x1141 +1*x1142 +1*x1143 +1*x1144 +1*x1145 +1*x1146 +1*x1147 +1*x1148 +1*x1149 +1*x1150 +1*x1151 +1*x1152 +1*x1153 +1*x1154 +1*x1155 +1*x1156 +1*x1157 +1*x1158 +1*x1159 +1*x1160 +1*x1161 +1*x1162 +1*x1163 +1*x1164 +1*x1165 +1*x1166 +1*x1167 +1*x1168 +1*x1169 +1*x1170 +1*x1171 +1*x1172 +1*x1173 +1*x1174 +1*x1175 +1*x1176 +1*x1177 +1*x1178 +1*x1179 +1*x1180 +1*x1181 +1*x1182 +1*x1183 +1*x1184 +1*x1185 +1*x1186 +1*x1187 +1*x1188 +1*x1189 +1*x1190 +1*x1191 +1*x1192 +1*x1193 +1*x1194 +1*x1195 +1*x1196 +1*x1197 +1*x1198 +1*x1199 +1*x1200 +1*x1201 +1*x1202 +1*x1203 +1*x1204 +1*x1205 +1*x1206 +1*x1207 +1*x1208 +1*x1209 +1*x1210 +1*x1211 +1*x1212 +1*x1213 +1*x1214 +1*x1215 +1*x1216 +1*x1217 +1*x1218 +1*x1219 +1*x1220 +1*x1221 +1*x1222 +1*x1223 +1*x1224 +1*x1225 +1*x1226 +1*x1227 +1*x1228 +1*x1229 +1*x1230 +1*x1231 +1*x1232 +1*x1233 +1*x1234 +1*x1235 +1*x1236 +1*x1237 +1*x1238 +1*x1239 +1*x1240 +1*x1241 +1*x1242 +1*x1243 +1*x1244 +1*x1245 +1*x1246 +1*x1247 +1*x1248 +1*x1249 +1*x1250 +1*x1251 +1*x1252 +1*x1253 +1*x1254 +1*x1255 +1*x1256 +1*x1257 +1*x1258 +1*x1259 +1*x1260 +1*x1261 +1*x1262 +1*x1263 +1*x1264 +1*x1265 +1*x1266 +1*x1267 +1*x1268 +1*x1269 +1*x1270 +1*x1271 +1*x1272 +1*x1273 +1*x1274 +1*x1275 +1*x1276 +1*x1277 +1*x1278 +1*x1279 +1*x1280 +1*x1281 +1*x1282 +1*x1283 +1*x1284 +1*x1285 +1*x1286 +1*x1287 +1*x1288 +1*x1289 +1*x1290 +1*x1291 +1*x1292 +1*x1293 +1*x1294 +1*x1295 +1*x1296 +1*x1297 +1*x1298 +1*x1299 +1*x1300 +1*x1301 +1*x1302 +1*x1303 +1*x1304 +1*x1305 +1*x1306 +1*x1307 +1*x1308 +1*x1309 +1*x1310 +1*x1311 +1*x1312 +1*x1313 +1*x1314 +1*x1315 +1*x1316 +1*x1317 +1*x1318 +1*x1319 +1*x1320 +1*x1321 +1*x1322 +1*x1323 +1*x1324 +1*x1325 +1*x1326 +1*x1327 +1*x1328 +1*x1329 +1*x1330 +1*x1331 +1*x1332 +1*x1333 +1*x1334 +1*x1335 +1*x1336 +1*x1337 +1*x1338 +1*x1339 +1*x1340 +1*x1341 +1*x1342 +1*x1343 +1*x1344 +1*x1345 +1*x1346 +1*x1347 +1*x1348 +1*x1349 +1*x1350 +1*x1351 +1*x1352 +1*x1353 +1*x1354 +1*x1355 +1*x1356 +1*x1357 +1*x1358 +1*x1359 +1*x1360 +1*x1361 +1*x1362 +1*x1363 +1*x1364 +1*x1365 +1*x1366 +1*x1367 +1*x1368 +1*x1369 +1*x1370 +1*x1371 +1*x1372 +1*x1373 +1*x1374 +1*x1375 +1*x1376 +1*x1377 +1*x1378 +1*x1379 +1*x1380 +1*x1381 +1*x1382 +1*x1383 +1*x1384 +1*x1385 +1*x1386 +1*x1387 +1*x1388 +1*x1389 +1*x1390 +1*x1391 +1*x1392 +1*x1393 +1*x1394 +1*x1395 +1*x1396 +1*x1397 +1*x1398 +1*x1399 +1*x1400 +1*x1401 +1*x1402 +1*x1403 +1*x1404 +1*x1405 +1*x1406 +1*x1407 +1*x1408 +1*x1409 +1*x1410 +1*x1411 +1*x1412 +1*x1413 +1*x1414 +1*x1415 +1*x1416 +1*x1417 +1*x1418 +1*x1419 +1*x1420 +1*x1421 +1*x1422 +1*x1423 +1*x1424 +1*x1425 +1*x1426 +1*x1427 +1*x1428 +1*x1429 +1*x1430 +1*x1431 +1*x1432 +1*x1433 +1*x1434 +1*x1435 +1*x1436 +1*x1437 +1*x1438 +1*x1439 +1*x1440 +1*x1441 +1*x1442 +1*x1443 +1*x1444 +1*x1445 +1*x1446 +1*x1447 +1*x1448 +1*x1449 +1*x1450 +1*x1451 +1*x1452 +1*x1453 +1*x1454 +1*x1455 +1*x1456 +1*x1457 +1*x1458 +1*x1459 +1*x1460 +1*x1461 +1*x1462 +1*x1463 +1*x1464 +1*x1465 +1*x1466 +1*x1467 +1*x1468 +1*x1469 +1*x1470 +1*x1471 +1*x1472 +1*x1473 +1*x1474 +1*x1475 +1*x1476 +1*x1477 +1*x1478 +1*x1479 +1*x1480 +1*x1481 +1*x1482 +1*x1483 +1*x1484 +1*x1485 +1*x1486 +1*x1487 +1*x1488 +1*x1489 +1*x1490 +1*x1491 +1*x1492 +1*x1493 +1*x1494 +1*x1495 +1*x1496 +1*x1497 +1*x1498 +1*x1499 +1*x1500 +1*x1501 +1*x1502 +1*x1503 +1*x1504 +1*x1505 +1*x1506 +1*x1507 +1*x1508 +1*x1509 +1*x1510 +1*x1511 +1*x1512 +1*x1513 +1*x1514 +1*x1515 +1*x1516 +1*x1517 +1*x1518 +1*x1519 +1*x1520 +1*x1521 +1*x1522 +1*x1523 +1*x1524 +1*x1525 +1*x1526 +1*x1527 +1*x1528 +1*x1529 +1*x1530 +1*x1531 +1*x1532 +1*x1533 +1*x1534 +1*x1535 +1*x1536 +1*x1537 +1*x1538 +1*x1539 +1*x1540 +1*x1541 +1*x1542 +1*x1543 +1*x1544 +1*x1545 +1*x1546 +1*x1547 +1*x1548 +1*x1549 +1*x1550 +1*x1551 +1*x1552 +1*x1553 +1*x1554 +1*x1555 +1*x1556 +1*x1557 +1*x1558 +1*x1559 +1*x1560 +1*x1561 +1*x1562 +1*x1563 +1*x1564 +1*x1565 +1*x1566 +1*x1567 +1*x1568 +1*x1569 +1*x1570 +1*x1571 +1*x1572 +1*x1573 +1*x1574 +1*x1575 +1*x1576 +1*x1577 +1*x1578 +1*x1579 +1*x1580 +1*x1581 +1*x1582 +1*x1583 +1*x1584 +1*x1585 +1*x1586 +1*x1587 +1*x1588 +1*x1589 +1*x1590 +1*x1591 +1*x1592 +1*x1593 +1*x1594 +1*x1595 +1*x1596 +1*x1597 +1*x1598 +1*x1599 +1*x1600 +1*x1601 +1*x1602 +1*x1603 +1*x1604 +1*x1605 +1*x1606 +1*x1607 +1*x1608 +1*x1609 +1*x1610 +1*x1611 +1*x1612 +1*x1613 +1*x1614 +1*x1615 +1*x1616 +1*x1617 +1*x1618 +1*x1619 +1*x1620 +1*x1621 +1*x1622 +1*x1623 +1*x1624 +1*x1625 +1*x1626 +1*x1627 +1*x1628 +1*x1629 +1*x1630 +1*x1631 +1*x1632 +1*x1633 +1*x1634 +1*x1635 +1*x1636 +1*x1637 +1*x1638 +1*x1639 +1*x1640 +1*x1641 +1*x1642 +1*x1643 +1*x1644 +1*x1645 +1*x1646 +1*x1647 +1*x1648 +1*x1649 +1*x1650 +1*x1651 +1*x1652 +1*x1653 +1*x1654 +1*x1655 +1*x1656 +1*x1657 +1*x1658 +1*x1659 +1*x1660 +1*x1661 +1*x1662 +1*x1663 +1*x1664 +1*x1665 +1*x1666 +1*x1667 +1*x1668 +1*x1669 +1*x1670 +1*x1671 +1*x1672 +1*x1673 +1*x1674 +1*x1675 +1*x1676 +1*x1677 +1*x1678 +1*x1679 +1*x1680 +1*x1681 +1*x1682 +1*x1683 +1*x1684 +1*x1685 +1*x1686 +1*x1687 +1*x1688 +1*x1689 +1*x1690 +1*x1691 +1*x1692 +1*x1693 +1*x1694 +1*x1695 +1*x1696 +1*x1697 +1*x1698 +1*x1699 +1*x1700 +1*x1701 +1*x1702 +1*x1703 +1*x1704 +1*x1705 +1*x1706 +1*x1707 +1*x1708 +1*x1709 +1*x1710 +1*x1711 +1*x1712 +1*x1713 +1*x1714 +1*x1715 +1*x1716 +1*x1717 +1*x1718 +1*x1719 +1*x1720 +1*x1721 +1*x1722 +1*x1723 +1*x1724 +1*x1725 +1*x1726 +1*x1727 +1*x1728 +1*x1729 +1*x1730 +1*x1731 +1*x1732 +1*x1733 +1*x1734 +1*x1735 +1*x1736 +1*x1737 +1*x1738 +1*x1739 +1*x1740 +1*x1741 +1*x1742 +1*x1743 +1*x1744 +1*x1745 +1*x1746 +1*x1747 +1*x1748 +1*x1749 +1*x1750 +1*x1751 +1*x1752 +1*x1753 +1*x1754 +1*x1755 +1*x1756 +1*x1757 +1*x1758 +1*x1759 +1*x1760 +1*x1761 +1*x1762 +1*x1763 +1*x1764 +1*x1765 +1*x1766 +1*x1767 +1*x1768 +1*x1769 +1*x1770 +1*x1771 +1*x1772 +1*x1773 +1*x1774 +1*x1775 +1*x1776 +1*x1777 +1*x1778 +1*x1779 +1*x1780 +1*x1781 +1*x1782 +1*x1783 +1*x1784 +1*x1785 +1*x1786 +1*x1787 +1*x1788 +1*x1789 +1*x1790 +1*x1791 +1*x1792 +1*x1793 +1*x1794 +1*x1795 +1*x1796 +1*x1797 +1*x1798 +1*x1799 +1*x1800 +1*x1801 +1*x1802 +1*x1803 +1*x1804 +1*x1805 +1*x1806 +1*x1807 +1*x1808 +1*x1809 +1*x1810 +1*x1811 +1*x1812 +1*x1813 +1*x1814 +1*x1815 +1*x1816 +1*x1817 +1*x1818 +1*x1819 +1*x1820 +1*x1821 +1*x1822 +1*x1823 +1*x1824 +1*x1825 +1*x1826 +1*x1827 +1*x1828 +1*x1829 +1*x1830 +1*x1831 +1*x1832 +1*x1833 +1*x1834 +1*x1835 +1*x1836 +1*x1837 +1*x1838 +1*x1839 +1*x1840 +1*x1841 +1*x1842 +1*x1843 +1*x1844 +1*x1845 +1*x1846 +1*x1847 +1*x1848 +1*x1849 +1*x1850 +1*x1851 +1*x1852 +1*x1853 +1*x1854 +1*x1855 +1*x1856 +1*x1857 +1*x1858 +1*x1859 +1*x1860 +1*x1861 +1*x1862 +1*x1863 +1*x1864 +1*x1865 +1*x1866 +1*x1867 +1*x1868 +1*x1869 +1*x1870 +1*x1871 +1*x1872 +1*x1873 +1*x1874 +1*x1875 +1*x1876 +1*x1877 +1*x1878 +1*x1879 +1*x1880 +1*x1881 +1*x1882 +1*x1883 +1*x1884 +1*x1885 +1*x1886 +1*x1887 +1*x1888 +1*x1889 +1*x1890 +1*x1891 +1*x1892 +1*x1893 +1*x1894 +1*x1895 +1*x1896 +1*x1897 +1*x1898 +1*x1899 +1*x1900 +1*x1901 +1*x1902 +1*x1903 +1*x1904 +1*x1905 +1*x1906 +1*x1907 +1*x1908 +1*x1909 +1*x1910 +1*x1911 +1*x1912 +1*x1913 +1*x1914 +1*x1915 +1*x1916 +1*x1917 +1*x1918 +1*x1919 +1*x1920 +1*x1921 +1*x1922 +1*x1923 +1*x1924 +1*x1925 +1*x1926 +1*x1927 +1*x1928 +1*x1929 +1*x1930 +1*x1931 +1*x1932 +1*x1933 +1*x1934 +1*x1935 +1*x1936 +1*x1937 +1*x1938 +1*x1939 +1*x1940 +1*x1941 +1*x1942 +1*x1943 +1*x1944 +1*x1945 +1*x1946 +1*x1947 +1*x1948 +1*x1949 +1*x1950 +1*x1951 +1*x1952 +1*x1953 +1*x1954 +1*x1955 +1*x1956 +1*x1957 +1*x1958 +1*x1959 +1*x1960 +1*x1961 +1*x1962 +1*x1963 +1*x1964 +1*x1965 +1*x1966 +1*x1967 +1*x1968 +1*x1969 +1*x1970 +1*x1971 +1*x1972 +1*x1973 +1*x1974 +1*x1975 +1*x1976 +1*x1977 +1*x1978 +1*x1979 +1*x1980 +1*x1981 +1*x1982 +1*x1983 +1*x1984 +1*x1985 +1*x1986 +1*x1987 +1*x1988 +1*x1989 +1*x1990 +1*x1991 +1*x1992 +1*x1993 +1*x1994 +1*x1995 +1*x1996 +1*x1997 +1*x1998 +1*x1999 +1*x2000 +1*x2001 +1*x2002 +1*x2003 +1*x2004 +1*x2005 +1*x2006 +1*x2007 +1*x2008 +1*x2009 +1*x2010 +1*x2011 +1*x2012 +1*x2013 +1*x2014 +1*x2015 +1*x2016 +1*x2017 +1*x2018 +1*x2019 +1*x2020 +1*x2021 +1*x2022 +1*x2023 +1*x2024 +1*x2025 +1*x2026 +1*x2027 +1*x2028 +1*x2029 +1*x2030 +1*x2031 +1*x2032 +1*x2033 +1*x2034 +1*x2035 +1*x2036 +1*x2037 +1*x2038 +1*x2039 +1*x2040 +1*x2041 +1*x2042 +1*x2043 +1*x2044 +1*x2045 +1*x2046 +1*x2047 +1*x2048 +1*x2049 +1*x2050 +1*x2051 +1*x2052 +1*x2053 +1*x2054 +1*x2055 +1*x2056 +1*x2057 +1*x2058 +1*x2059 +1*x2060 +1*x2061 +1*x2062 +1*x2063 +1*x2064 +1*x2065 +1*x2066 +1*x2067 +1*x2068 +1*x2069 +1*x2070 +1*x2071 +1*x2072 +1*x2073 +1*x2074 +1*x2075 +1*x2076 +1*x2077 +1*x2078 +1*x2079 +1*x2080 +1*x2081 +1*x2082 +1*x2083 +1*x2084 +1*x2085 +1*x2086 +1*x2087 +1*x2088 +1*x2089 +1*x2090 +1*x2091 +1*x2092 +1*x2093 +1*x2094 +1*x2095 +1*x2096 +1*x2097 +1*x2098 +1*x2099 +1*x2100 +1*x2101 +1*x2102 +1*x2103 +1*x2104 +1*x2105 +1*x2106 +1*x2107 +1*x2108 +1*x2109 +1*x2110 +1*x2111 +1*x2112 +1*x2113 +1*x2114 +1*x2115 +1*x2116 +1*x2117 +1*x2118 +1*x2119 +1*x2120 +1*x2121 +1*x2122 +1*x2123 +1*x2124 +1*x2125 +1*x2126 +1*x2127 +1*x2128 +1*x2129 +1*x2130 +1*x2131 +1*x2132 +1*x2133 +1*x2134 +1*x2135 +1*x2136 +1*x2137 +1*x2138 +1*x2139 +1*x2140 +1*x2141 +1*x2142 +1*x2143 +1*x2144 +1*x2145 +1*x2146 +1*x2147 +1*x2148 +1*x2149 +1*x2150 +1*x2151 +1*x2152 +1*x2153 +1*x2154 +1*x2155 +1*x2156 +1*x2157 +1*x2158 +1*x2159 +1*x2160 +1*x2161 +1*x2162 +1*x2163 +1*x2164 +1*x2165 +1*x2166 +1*x2167 +1*x2168 +1*x2169 +1*x2170 +1*x2171 +1*x2172 +1*x2173 +1*x2174 +1*x2175 +1*x2176 +1*x2177 +1*x2178 +1*x2179 +1*x2180 +1*x2181 +1*x2182 +1*x2183 +1*x2184 +1*x2185 +1*x2186 +1*x2187 +1*x2188 +1*x2189 +1*x2190 +1*x2191 +1*x2192 +1*x2193 +1*x2194 +1*x2195 +1*x2196 +1*x2197 +1*x2198 +1*x2199 +1*x2200 +1*x2201 +1*x2202 +1*x2203 +1*x2204 +1*x2205 +1*x2206 +1*x2207 +1*x2208 +1*x2209 +1*x2210 +1*x2211 +1*x2212 +1*x2213 +1*x2214 +1*x2215 +1*x2216 +1*x2217 +1*x2218 +1*x2219 +1*x2220 +1*x2221 +1*x2222 +1*x2223 +1*x2224 +1*x2225 +1*x2226 +1*x2227 +1*x2228 +1*x2229 +1*x2230 +1*x2231 +1*x2232 +1*x2233 +1*x2234 +1*x2235 +1*x2236 +1*x2237 +1*x2238 +1*x2239 +1*x2240 +1*x2241 +1*x2242 +1*x2243 +1*x2244 +1*x2245 +1*x2246 +1*x2247 +1*x2248 +1*x2249 +1*x2250 +1*x2251 +1*x2252 +1*x2253 +1*x2254 +1*x2255 +1*x2256 +1*x2257 +1*x2258 +1*x2259 +1*x2260 +1*x2261 +1*x2262 +1*x2263 +1*x2264 +1*x2265 +1*x2266 +1*x2267 +1*x2268 +1*x2269 +1*x2270 +1*x2271 +1*x2272 +1*x2273 +1*x2274 +1*x2275 +1*x2276 +1*x2277 +1*x2278 +1*x2279 +1*x2280 +1*x2281 +1*x2282 +1*x2283 +1*x2284 +1*x2285 +1*x2286 +1*x2287 +1*x2288 +1*x2289 +1*x2290 +1*x2291 +1*x2292 +1*x2293 +1*x2294 +1*x2295 +1*x2296 +1*x2297 +1*x2298 +1*x2299 +1*x2300 +1*x2301 +1*x2302 +1*x2303 +1*x2304 +1*x2305 +1*x2306 +1*x2307 +1*x2308 +1*x2309 +1*x2310 +1*x2311 +1*x2312 +1*x2313 +1*x2314 +1*x2315 +1*x2316 +1*x2317 +1*x2318 +1*x2319 +1*x2320 +1*x2321 +1*x2322 +1*x2323 +1*x2324 +1*x2325 +1*x2326 +1*x2327 +1*x2328 +1*x2329 +1*x2330 +1*x2331 +1*x2332 +1*x2333 +1*x2334 +1*x2335 +1*x2336 +1*x2337 +1*x2338 +1*x2339 +1*x2340 +1*x2341 +1*x2342 +1*x2343 +1*x2344 +1*x2345 +1*x2346 +1*x2347 +1*x2348 +1*x2349 +1*x2350 +1*x2351 +1*x2352 +1*x2353 +1*x2354 +1*x2355 +1*x2356 +1*x2357 +1*x2358 +1*x2359 +1*x2360 +1*x2361 +1*x2362 +1*x2363 +1*x2364 +1*x2365 +1*x2366 +1*x2367 +1*x2368 +1*x2369 +1*x2370 +1*x2371 +1*x2372 +1*x2373 +1*x2374 +1*x2375 +1*x2376 +1*x2377 +1*x2378 +1*x2379 +1*x2380 +1*x2381 +1*x2382 +1*x2383 +1*x2384 +1*x2385 +1*x2386 +1*x2387 +1*x2388 +1*x2389 +1*x2390 +1*x2391 +1*x2392 +1*x2393 +1*x2394 +1*x2395 +1*x2396 +1*x2397 +1*x2398 +1*x2399 +1*x2400 +1*x2401 +1*x2402 +1*x2403 +1*x2404 +1*x2405 +1*x2406 +1*x2407 +1*x2408 +1*x2409 +1*x2410 +1*x2411 +1*x2412 +1*x2413 +1*x2414 +1*x2415 +1*x2416 +1*x2417 +1*x2418 +1*x2419 +1*x2420 +1*x2421 +1*x2422 +1*x2423 +1*x2424 +1*x2425 +1*x2426 +1*x2427 +1*x2428 +1*x2429 +1*x2430 +1*x2431 +1*x2432 +1*x2433 +1*x2434 +1*x2435 +1*x2436 +1*x2437 +1*x2438 +1*x2439 +1*x2440 +1*x2441 +1*x2442 +1*x2443 +1*x2444 +1*x2445 +1*x2446 +1*x2447 +1*x2448 +1*x2449 +1*x2450 +1*x2451 +1*x2452 +1*x2453 +1*x2454 +1*x2455 +1*x2456 +1*x2457 +1*x2458 +1*x2459 +1*x2460 +1*x2461 +1*x2462 +1*x2463 +1*x2464 +1*x2465 +1*x2466 +1*x2467 +1*x2468 +1*x2469 +1*x2470 +1*x2471 +1*x2472 +1*x2473 +1*x2474 +1*x2475 +1*x2476 +1*x2477 +1*x2478 +1*x2479 +1*x2480 +1*x2481 +1*x2482 +1*x2483 +1*x2484 +1*x2485 +1*x2486 +1*x2487 +1*x2488 +1*x2489 +1*x2490 +1*x2491 +1*x2492 +1*x2493 +1*x2494 +1*x2495 +1*x2496 +1*x2497 +1*x2498 +1*x2499 +1*x2500 +1*x2501 +1*x2502 +1*x2503 +1*x2504 +1*x2505 +1*x2506 +1*x2507 +1*x2508 +1*x2509 +1*x2510 +1*x2511 +1*x2512 +1*x2513 +1*x2514 +1*x2515 +1*x2516 +1*x2517 +1*x2518 +1*x2519 +1*x2520 +1*x2521 +1*x2522 +1*x2523 +1*x2524 +1*x2525 +1*x2526 +1*x2527 +1*x2528 +1*x2529 +1*x2530 +1*x2531 +1*x2532 +1*x2533 +1*x2534 +1*x2535 +1*x2536 +1*x2537 +1*x2538 +1*x2539 +1*x2540 +1*x2541 +1*x2542 +1*x2543 +1*x2544 +1*x2545 +1*x2546 +1*x2547 +1*x2548 +1*x2549 +1*x2550 +1*x2551 +1*x2552 +1*x2553 +1*x2554 +1*x2555 +1*x2556 +1*x2557 +1*x2558 +1*x2559 +1*x2560 +1*x2561 +1*x2562 +1*x2563 +1*x2564 +1*x2565 +1*x2566 +1*x2567 +1*x2568 +1*x2569 +1*x2570 +1*x2571 +1*x2572 +1*x2573 +1*x2574 +1*x2575 +1*x2576 +1*x2577 +1*x2578 +1*x2579 +1*x2580 +1*x2581 +1*x2582 +1*x2583 +1*x2584 +1*x2585 +1*x2586 +1*x2587 +1*x2588 +1*x2589 +1*x2590 +1*x2591 +1*x2592 +1*x2593 +1*x2594 +1*x2595 +1*x2596 +1*x2597 +1*x2598 +1*x2599 +1*x2600 +1*x2601 +1*x2602 +1*x2603 +1*x2604 +1*x2605 +1*x2606 +1*x2607 +1*x2608 +1*x2609 +1*x2610 +1*x2611 +1*x2612 +1*x2613 +1*x2614 +1*x2615 +1*x2616 +1*x2617 +1*x2618 +1*x2619 +1*x2620 +1*x2621 +1*x2622 +1*x2623 +1*x2624 +1*x2625 +1*x2626 +1*x2627 +1*x2628 +1*x2629 +1*x2630 +1*x2631 +1*x2632 +1*x2633 +1*x2634 +1*x2635 +1*x2636 +1*x2637 +1*x2638 +1*x2639 +1*x2640 +1*x2641 +1*x2642 +1*x2643 +1*x2644 +1*x2645 +1*x2646 +1*x2647 +1*x2648 +1*x2649 +1*x2650 +1*x2651 +1*x2652 +1*x2653 +1*x2654 +1*x2655 +1*x2656 +1*x2657 +1*x2658 +1*x2659 +1*x2660 +1*x2661 +1*x2662 +1*x2663 +1*x2664 +1*x2665 +1*x2666 +1*x2667 +1*x2668 +1*x2669 +1*x2670 +1*x2671 +1*x2672 +1*x2673 +1*x2674 +1*x2675 +1*x2676 +1*x2677 +1*x2678 +1*x2679 +1*x2680 +1*x2681 +1*x2682 +1*x2683 +1*x2684 +1*x2685 +1*x2686 +1*x2687 +1*x2688 +1*x2689 +1*x2690 +1*x2691 +1*x2692 +1*x2693 +1*x2694 +1*x2695 +1*x2696 +1*x2697 +1*x2698 +1*x2699 +1*x2700 +1*x2701 +1*x2702 +1*x2703 +1*x2704 +1*x2705 +1*x2706 +1*x2707 +1*x2708 +1*x2709 +1*x2710 +1*x2711 +1*x2712 +1*x2713 +1*x2714 +1*x2715 +1*x2716 +1*x2717 +1*x2718 +1*x2719 +1*x2720 +1*x2721 +1*x2722 +1*x2723 +1*x2724 +1*x2725 +1*x2726 +1*x2727 +1*x2728 +1*x2729 +1*x2730 +1*x2731 +1*x2732 +1*x2733 +1*x2734 +1*x2735 +1*x2736 +1*x2737 +1*x2738 +1*x2739 +1*x2740 +1*x2741 +1*x2742 +1*x2743 +1*x2744 +1*x2745 +1*x2746 +1*x2747 +1*x2748 +1*x2749 +1*x2750 +1*x2751 +1*x2752 +1*x2753 +1*x2754 +1*x2755 +1*x2756 +1*x2757 +1*x2758 +1*x2759 +1*x2760 +1*x2761 +1*x2762 +1*x2763 +1*x2764 +1*x2765 +1*x2766 +1*x2767 +1*x2768 +1*x2769 +1*x2770 +1*x2771 +1*x2772 +1*x2773 +1*x2774 +1*x2775 +1*x2776 +1*x2777 +1*x2778 +1*x2779 +1*x2780 +1*x2781 +1*x2782 +1*x2783 +1*x2784 +1*x2785 +1*x2786 +1*x2787 +1*x2788 +1*x2789 +1*x2790 +1*x2791 +1*x2792 +1*x2793 +1*x2794 +1*x2795 +1*x2796 +1*x2797 +1*x2798 +1*x2799 +1*x2800 +1*x2801 +1*x2802 +1*x2803 +1*x2804 +1*x2805 +1*x2806 +1*x2807 +1*x2808 +1*x2809 +1*x2810 +1*x2811 +1*x2812 +1*x2813 +1*x2814 +1*x2815 +1*x2816 +1*x2817 +1*x2818 +1*x2819 +1*x2820 +1*x2821 +1*x2822 +1*x2823 +1*x2824 +1*x2825 +1*x2826 +1*x2827 +1*x2828 +1*x2829 +1*x2830 +1*x2831 +1*x2832 +1*x2833 +1*x2834 +1*x2835 +1*x2836 +1*x2837 +1*x2838 +1*x2839 +1*x2840 +1*x2841 +1*x2842 +1*x2843 +1*x2844 +1*x2845 +1*x2846 +1*x2847 +1*x2848 +1*x2849 +1*x2850 +1*x2851 +1*x2852 +1*x2853 +1*x2854 +1*x2855 +1*x2856 +1*x2857 +1*x2858 +1*x2859 +1*x2860 +1*x2861 +1*x2862 +1*x2863 +1*x2864 +1*x2865 +1*x2866 +1*x2867 +1*x2868 +1*x2869 +1*x2870 +1*x2871 +1*x2872 +1*x2873 +1*x2874 +1*x2875 +1*x2876 +1*x2877 +1*x2878 +1*x2879 +1*x2880 +1*x2881 +1*x2882 +1*x2883 +1*x2884 +1*x2885 +1*x2886 +1*x2887 +1*x2888 +1*x2889 +1*x2890 +1*x2891 +1*x2892 +1*x2893 +1*x2894 +1*x2895 +1*x2896 +1*x2897 +1*x2898 +1*x2899 +1*x2900 +1*x2901 +1*x2902 +1*x2903 +1*x2904 +1*x2905 +1*x2906 +1*x2907 +1*x2908 +1*x2909 +1*x2910 +1*x2911 +1*x2912 +1*x2913 +1*x2914 +1*x2915 +1*x2916 +1*x2917 +1*x2918 +1*x2919 +1*x2920 +1*x2921 +1*x2922 +1*x2923 +1*x2924 +1*x2925 +1*x2926 +1*x2927 +1*x2928 +1*x2929 +1*x2930 +1*x2931 +1*x2932 +1*x2933 +1*x2934 +1*x2935 +1*x2936 +1*x2937 +1*x2938 +1*x2939 +1*x2940 +1*x2941 +1*x2942 +1*x2943 +1*x2944 +1*x2945 +1*x2946 +1*x2947 +1*x2948 +1*x2949 +1*x2950 +1*x2951 +1*x2952 +1*x2953 +1*x2954 +1*x2955 +1*x2956 +1*x2957 +1*x2958 +1*x2959 +1*x2960 +1*x2961 +1*x2962 +1*x2963 +1*x2964 +1*x2965 +1*x2966 +1*x2967 +1*x2968 +1*x2969 +1*x2970 +1*x2971 +1*x2972 +1*x2973 +1*x2974 +1*x2975 +1*x2976 +1*x2977 +1*x2978 +1*x2979 +1*x2980 +1*x2981 +1*x2982 +1*x2983 +1*x2984 +1*x2985 +1*x2986 +1*x2987 +1*x2988 +1*x2989 +1*x2990 +1*x2991 +1*x2992 +1*x2993 +1*x2994 +1*x2995 +1*x2996 +1*x2997 +1*x2998 +1*x2999 +1*x3000 +1*x3001 +1*x3002 +1*x3003 +1*x3004 +1*x3005 +1*x3006 +1*x3007 +1*x3008 +1*x3009 +1*x3010 +1*x3011 +1*x3012 +1*x3013 +1*x3014 +1*x3015 +1*x3016 +1*x3017 +1*x3018 +1*x3019 +1*x3020 +1*x3021 +1*x3022 +1*x3023 +1*x3024 +1*x3025 +1*x3026 +1*x3027 +1*x3028 +1*x3029 +1*x3030 +1*x3031 +1*x3032 +1*x3033 +1*x3034 +1*x3035 +1*x3036 +1*x3037 +1*x3038 +1*x3039 +1*x3040 +1*x3041 +1*x3042 +1*x3043 +1*x3044 +1*x3045 +1*x3046 +1*x3047 +1*x3048 +1*x3049 +1*x3050 +1*x3051 +1*x3052 +1*x3053 +1*x3054 +1*x3055 +1*x3056 +1*x3057 +1*x3058 +1*x3059 +1*x3060 +1*x3061 +1*x3062 +1*x3063 +1*x3064 +1*x3065 +1*x3066 +1*x3067 +1*x3068 +1*x3069 +1*x3070 +1*x3071 +1*x3072 +1*x3073 +1*x3074 +1*x3075 +1*x3076 +1*x3077 +1*x3078 +1*x3079 +1*x3080 +1*x3081 +1*x3082 +1*x3083 +1*x3084 +1*x3085 +1*x3086 +1*x3087 +1*x3088 +1*x3089 +1*x3090 +1*x3091 +1*x3092 +1*x3093 +1*x3094 +1*x3095 +1*x3096 +1*x3097 +1*x3098 +1*x3099 +1*x3100 +1*x3101 +1*x3102 +1*x3103 +1*x3104 +1*x3105 +1*x3106 +1*x3107 +1*x3108 +1*x3109 +1*x3110 +1*x3111 +1*x3112 +1*x3113 +1*x3114 +1*x3115 +1*x3116 +1*x3117 +1*x3118 +1*x3119 +1*x3120 +1*x3121 +1*x3122 +1*x3123 +1*x3124 +1*x3125 +1*x3126 +1*x3127 +1*x3128 +1*x3129 +1*x3130 +1*x3131 +1*x3132 +1*x3133 +1*x3134 +1*x3135 +1*x3136 +1*x3137 +1*x3138 +1*x3139 +1*x3140 +1*x3141 +1*x3142 +1*x3143 +1*x3144 +1*x3145 +1*x3146 +1*x3147 +1*x3148 +1*x3149 +1*x3150 +1*x3151 +1*x3152 +1*x3153 +1*x3154 +1*x3155 +1*x3156 +1*x3157 +1*x3158 +1*x3159 +1*x3160 +1*x3161 +1*x3162 +1*x3163 +1*x3164 +1*x3165 +1*x3166 +1*x3167 +1*x3168 +1*x3169 +1*x3170 +1*x3171 +1*x3172 +1*x3173 +1*x3174 +1*x3175 +1*x3176 +1*x3177 +1*x3178 +1*x3179 +1*x3180 +1*x3181 +1*x3182 +1*x3183 +1*x3184 +1*x3185 +1*x3186 +1*x3187 +1*x3188 +1*x3189 +1*x3190 +1*x3191 +1*x3192 +1*x3193 +1*x3194 +1*x3195 +1*x3196 +1*x3197 +1*x3198 +1*x3199 +1*x3200 +1*x3201 +1*x3202 +1*x3203 +1*x3204 +1*x3205 +1*x3206 +1*x3207 +1*x3208 +1*x3209 +1*x3210 +1*x3211 +1*x3212 +1*x3213 +1*x3214 +1*x3215 +1*x3216 +1*x3217 +1*x3218 +1*x3219 +1*x3220 +1*x3221 +1*x3222 +1*x3223 +1*x3224 +1*x3225 +1*x3226 +1*x3227 +1*x3228 +1*x3229 +1*x3230 +1*x3231 +1*x3232 +1*x3233 +1*x3234 +1*x3235 +1*x3236 +1*x3237 +1*x3238 +1*x3239 +1*x3240 +1*x3241 +1*x3242 +1*x3243 +1*x3244 +1*x3245 +1*x3246 +1*x3247 +1*x3248 +1*x3249 +1*x3250 +1*x3251 +1*x3252 +1*x3253 +1*x3254 +1*x3255 +1*x3256 +1*x3257 +1*x3258 +1*x3259 +1*x3260 +1*x3261 +1*x3262 +1*x3263 +1*x3264 +1*x3265 +1*x3266 +1*x3267 +1*x3268 +1*x3269 +1*x3270 +1*x3271 +1*x3272 +1*x3273 +1*x3274 +1*x3275 +1*x3276 +1*x3277 +1*x3278 +1*x3279 +1*x3280 +1*x3281 +1*x3282 +1*x3283 +1*x3284 +1*x3285 +1*x3286 +1*x3287 +1*x3288 +1*x3289 +1*x3290 +1*x3291 +1*x3292 +1*x3293 +1*x3294 +1*x3295 +1*x3296 +1*x3297 +1*x3298 +1*x3299 +1*x3300 +1*x3301 +1*x3302 +1*x3303 +1*x3304 +1*x3305 +1*x3306 +1*x3307 +1*x3308 +1*x3309 +1*x3310 +1*x3311 +1*x3312 +1*x3313 +1*x3314 +1*x3315 +1*x3316 +1*x3317 +1*x3318 +1*x3319 +1*x3320 +1*x3321 +1*x3322 +1*x3323 +1*x3324 +1*x3325 +1*x3326 +1*x3327 +1*x3328 +1*x3329 +1*x3330 +1*x3331 +1*x3332 +1*x3333 +1*x3334 +1*x3335 +1*x3336 +1*x3337 +1*x3338 +1*x3339 +1*x3340 +1*x3341 +1*x3342 +1*x3343 +1*x3344 +1*x3345 +1*x3346 +1*x3347 +1*x3348 +1*x3349 +1*x3350 +1*x3351 +1*x3352 +1*x3353 +1*x3354 +1*x3355 +1*x3356 +1*x3357 +1*x3358 +1*x3359 +1*x3360 +1*x3361 +1*x3362 +1*x3363 +1*x3364 +1*x3365 +1*x3366 +1*x3367 +1*x3368 +1*x3369 +1*x3370 +1*x3371 +1*x3372 +1*x3373 +1*x3374 +1*x3375 +1*x3376 +1*x3377 +1*x3378 +1*x3379 +1*x3380 +1*x3381 +1*x3382 +1*x3383 +1*x3384 +1*x3385 +1*x3386 +1*x3387 +1*x3388 +1*x3389 +1*x3390 +1*x3391 +1*x3392 +1*x3393 +1*x3394 +1*x3395 +1*x3396 +1*x3397 +1*x3398 +1*x3399 +1*x3400 +1*x3401 +1*x3402 +1*x3403 +1*x3404 +1*x3405 +1*x3406 +1*x3407 +1*x3408 +1*x3409 +1*x3410 +1*x3411 +1*x3412 +1*x3413 +1*x3414 +1*x3415 +1*x3416 +1*x3417 +1*x3418 +1*x3419 +1*x3420 +1*x3421 +1*x3422 +1*x3423 +1*x3424 +1*x3425 +1*x3426 +1*x3427 +1*x3428 +1*x3429 +1*x3430 +1*x3431 +1*x3432 +1*x3433 +1*x3434 +1*x3435 +1*x3436 +1*x3437 +1*x3438 +1*x3439 +1*x3440 +1*x3441 +1*x3442 +1*x3443 +1*x3444 +1*x3445 +1*x3446 +1*x3447 +1*x3448 +1*x3449 +1*x3450 +1*x3451 +1*x3452 +1*x3453 +1*x3454 +1*x3455 +1*x3456 +1*x3457 +1*x3458 +1*x3459 +1*x3460 +1*x3461 +1*x3462 +1*x3463 +1*x3464 +1*x3465 +1*x3466 +1*x3467 +1*x3468 +1*x3469 +1*x3470 +1*x3471 +1*x3472 +1*x3473 +1*x3474 +1*x3475 +1*x3476 +1*x3477 +1*x3478 +1*x3479 +1*x3480 +1*x3481 +1*x3482 +1*x3483 +1*x3484 +1*x3485 +1*x3486 +1*x3487 +1*x3488 +1*x3489 +1*x3490 +1*x3491 +1*x3492 +1*x3493 +1*x3494 +1*x3495 +1*x3496 +1*x3497 +1*x3498 +1*x3499 +1*x3500 +1*x3501 +1*x3502 +1*x3503 +1*x3504 +1*x3505 +1*x3506 +1*x3507 +1*x3508 +1*x3509 +1*x3510 +1*x3511 +1*x3512 +1*x3513 +1*x3514 +1*x3515 +1*x3516 +1*x3517 +1*x3518 +1*x3519 +1*x3520 +1*x3521 +1*x3522 +1*x3523 +1*x3524 +1*x3525 +1*x3526 +1*x3527 +1*x3528 +1*x3529 +1*x3530 +1*x3531 +1*x3532 +1*x3533 +1*x3534 +1*x3535 +1*x3536 +1*x3537 +1*x3538 +1*x3539 +1*x3540 +1*x3541 +1*x3542 +1*x3543 +1*x3544 +1*x3545 +1*x3546 +1*x3547 +1*x3548 +1*x3549 +1*x3550 +1*x3551 +1*x3552 +1*x3553 +1*x3554 +1*x3555 +1*x3556 +1*x3557 +1*x3558 +1*x3559 +1*x3560 +1*x3561 +1*x3562 +1*x3563 +1*x3564 +1*x3565 +1*x3566 +1*x3567 +1*x3568 +1*x3569 +1*x3570 +1*x3571 +1*x3572 +1*x3573 +1*x3574 +1*x3575 +1*x3576 +1*x3577 +1*x3578 +1*x3579 +1*x3580 +1*x3581 +1*x3582 +1*x3583 +1*x3584 +1*x3585 +1*x3586 +1*x3587 +1*x3588 +1*x3589 +1*x3590 +1*x3591 +1*x3592 +1*x3593 +1*x3594 +1*x3595 +1*x3596 +1*x3597 +1*x3598 +1*x3599 +1*x3600 +1*x3601 +1*x3602 +1*x3603 +1*x3604 +1*x3605 +1*x3606 +1*x3607 +1*x3608 +1*x3609 +1*x3610 +1*x3611 +1*x3612 +1*x3613 +1*x3614 +1*x3615 +1*x3616 +1*x3617 +1*x3618 +1*x3619 +1*x3620 +1*x3621 +1*x3622 +1*x3623 +1*x3624 +1*x3625 +1*x3626 +1*x3627 +1*x3628 +1*x3629 +1*x3630 +1*x3631 +1*x3632 +1*x3633 +1*x3634 +1*x3635 +1*x3636 +1*x3637 +1*x3638 +1*x3639 +1*x3640 +1*x3641 +1*x3642 +1*x3643 +1*x3644 +1*x3645 +1*x3646 +1*x3647 +1*x3648 +1*x3649 +1*x3650 +1*x3651 +1*x3652 +1*x3653 +1*x3654 +1*x3655 +1*x3656 +1*x3657 +1*x3658 +1*x3659 +1*x3660 +1*x3661 +1*x3662 +1*x3663 +1*x3664 +1*x3665 +1*x3666 +1*x3667 +1*x3668 +1*x3669 +1*x3670 +1*x3671 +1*x3672 +1*x3673 +1*x3674 +1*x3675 +1*x3676 +1*x3677 +1*x3678 +1*x3679 +1*x3680 +1*x3681 +1*x3682 +1*x3683 +1*x3684 +1*x3685 +1*x3686 +1*x3687 +1*x3688 +1*x3689 +1*x3690 +1*x3691 +1*x3692 +1*x3693 +1*x3694 +1*x3695 +1*x3696 +1*x3697 +1*x3698 +1*x3699 +1*x3700 +1*x3701 +1*x3702 +1*x3703 +1*x3704 +1*x3705 +1*x3706 +1*x3707 +1*x3708 +1*x3709 +1*x3710 +1*x3711 +1*x3712 +1*x3713 +1*x3714 +1*x3715 +1*x3716 +1*x3717 +1*x3718 +1*x3719 +1*x3720 +1*x3721 +1*x3722 +1*x3723 +1*x3724 +1*x3725 +1*x3726 +1*x3727 +1*x3728 +1*x3729 +1*x3730 +1*x3731 +1*x3732 +1*x3733 +1*x3734 +1*x3735 +1*x3736 +1*x3737 +1*x3738 +1*x3739 +1*x3740 +1*x3741 +1*x3742 +1*x3743 +1*x3744 +1*x3745 +1*x3746 +1*x3747 +1*x3748 +1*x3749 +1*x3750 +1*x3751 +1*x3752 +1*x3753 +1*x3754 +1*x3755 +1*x3756 +1*x3757 +1*x3758 +1*x3759 +1*x3760 +1*x3761 +1*x3762 +1*x3763 +1*x3764 +1*x3765 +1*x3766 +1*x3767 +1*x3768 +1*x3769 +1*x3770 +1*x3771 +1*x3772 +1*x3773 +1*x3774 +1*x3775 +1*x3776 +1*x3777 +1*x3778 +1*x3779 +1*x3780 +1*x3781 +1*x3782 +1*x3783 +1*x3784 +1*x3785 +1*x3786 +1*x3787 +1*x3788 +1*x3789 +1*x3790 +1*x3791 +1*x3792 +1*x3793 +1*x3794 +1*x3795 +1*x3796 +1*x3797 +1*x3798 +1*x3799 +1*x3800 +1*x3801 +1*x3802 +1*x3803 +1*x3804 +1*x3805 +1*x3806 +1*x3807 +1*x3808 +1*x3809 +1*x3810 +1*x3811 +1*x3812 +1*x3813 +1*x3814 +1*x3815 +1*x3816 +1*x3817 +1*x3818 +1*x3819 +1*x3820 +1*x3821 +1*x3822 +1*x3823 +1*x3824 +1*x3825 +1*x3826 +1*x3827 +1*x3828 +1*x3829 +1*x3830 +1*x3831 +1*x3832 +1*x3833 +1*x3834 +1*x3835 +1*x3836 +1*x3837 +1*x3838 +1*x3839 +1*x3840 +1*x3841 +1*x3842 +1*x3843 +1*x3844 +1*x3845 +1*x3846 +1*x3847 +1*x3848 +1*x3849 +1*x3850 +1*x3851 +1*x3852 +1*x3853 +1*x3854 +1*x3855 +1*x3856 +1*x3857 +1*x3858 +1*x3859 +1*x3860 +1*x3861 +1*x3862 +1*x3863 +1*x3864 +1*x3865 +1*x3866 +1*x3867 +1*x3868 +1*x3869 +1*x3870 +1*x3871 +1*x3872 +1*x3873 +1*x3874 +1*x3875 +1*x3876 +1*x3877 +1*x3878 +1*x3879 +1*x3880 +1*x3881 +1*x3882 +1*x3883 +1*x3884 +1*x3885 +1*x3886 +1*x3887 +1*x3888 +1*x3889 +1*x3890 +1*x3891 +1*x3892 +1*x3893 +1*x3894 +1*x3895 +1*x3896 +1*x3897 +1*x3898 +1*x3899 +1*x3900 +1*x3901 +1*x3902 +1*x3903 +1*x3904 +1*x3905 +1*x3906 +1*x3907 +1*x3908 +1*x3909 +1*x3910 +1*x3911 +1*x3912 +1*x3913 +1*x3914 +1*x3915 +1*x3916 +1*x3917 +1*x3918 +1*x3919 +1*x3920 +1*x3921 +1*x3922 +1*x3923 +1*x3924 +1*x3925 +1*x3926 +1*x3927 +1*x3928 +1*x3929 +1*x3930 +1*x3931 +1*x3932 +1*x3933 +1*x3934 +1*x3935 +1*x3936 +1*x3937 +1*x3938 +1*x3939 +1*x3940 +1*x3941 +1*x3942 +1*x3943 +1*x3944 +1*x3945 +1*x3946 +1*x3947 +1*x3948 +1*x3949 +1*x3950 +1*x3951 +1*x3952 +1*x3953 +1*x3954 +1*x3955 +1*x3956 +1*x3957 +1*x3958 +1*x3959 +1*x3960 +1*x3961 +1*x3962 +1*x3963 +1*x3964 +1*x3965 +1*x3966 +1*x3967 +1*x3968 +1*x3969 +1*x3970 +1*x3971 +1*x3972 +1*x3973 +1*x3974 +1*x3975 +1*x3976 +1*x3977 +1*x3978 +1*x3979 +1*x3980 +1*x3981 +1*x3982 +1*x3983 +1*x3984 +1*x3985 +1*x3986 +1*x3987 +1*x3988 +1*x3989 +1*x3990 +1*x3991 +1*x3992 +1*x3993 +1*x3994 +1*x3995 +1*x3996 +1*x3997 +1*x3998 +1*x3999 +1*x4000 +1*x4001 +1*x4002 +1*x4003 +1*x4004 +1*x4005 +1*x4006 +1*x4007 +1*x4008 +1*x4009 +1*x4010 +1*x4011 +1*x4012 +1*x4013 +1*x4014 +1*x4015 +1*x4016 +1*x4017 +1*x4018 +1*x4019 +1*x4020 +1*x4021 +1*x4022 +1*x4023 +1*x4024 +1*x4025 +1*x4026 +1*x4027 +1*x4028 +1*x4029 +1*x4030 +1*x4031 +1*x4032 +1*x4033 +1*x4034 +1*x4035 +1*x4036 +1*x4037 +1*x4038 +1*x4039 +1*x4040 +1*x4041 +1*x4042 +1*x4043 +1*x4044 +1*x4045 +1*x4046 +1*x4047 +1*x4048 +1*x4049 +1*x4050 +1*x4051 +1*x4052 +1*x4053 +1*x4054 +1*x4055 +1*x4056 +1*x4057 +1*x4058 +1*x4059 +1*x4060 +1*x4061 +1*x4062 +1*x4063 +1*x4064 +1*x4065 +1*x4066 +1*x4067 +1*x4068 +1*x4069 +1*x4070 +1*x4071 +1*x4072 +1*x4073 +1*x4074 +1*x4075 +1*x4076 +1*x4077 +1*x4078 +1*x4079 +1*x4080 +1*x4081 +1*x4082 +1*x4083 +1*x4084 +1*x4085 +1*x4086 +1*x4087 +1*x4088 +1*x4089 +1*x4090 +1*x4091 +1*x4092 +1*x4093 +1*x4094 +1*x4095 +1*x4096 +1*x4097 +1*x4098 +1*x4099 +1*x4100 +1*x4101 +1*x4102 +1*x4103 +1*x4104 +1*x4105 +1*x4106 +1*x4107 +1*x4108 +1*x4109 +1*x4110 +1*x4111 +1*x4112 +1*x4113 +1*x4114 +1*x4115 +1*x4116 +1*x4117 +1*x4118 +1*x4119 +1*x4120 +1*x4121 +1*x4122 +1*x4123 +1*x4124 +1*x4125 +1*x4126 +1*x4127 +1*x4128 +1*x4129 +1*x4130 +1*x4131 +1*x4132 +1*x4133 +1*x4134 +1*x4135 +1*x4136 +1*x4137 +1*x4138 +1*x4139 +1*x4140 +1*x4141 +1*x4142 +1*x4143 +1*x4144 +1*x4145 +1*x4146 +1*x4147 +1*x4148 +1*x4149 +1*x4150 +1*x4151 +1*x4152 +1*x4153 +1*x4154 +1*x4155 +1*x4156 +1*x4157 +1*x4158 +1*x4159 +1*x4160 +1*x4161 +1*x4162 +1*x4163 +1*x4164 +1*x4165 +1*x4166 +1*x4167 +1*x4168 +1*x4169 +1*x4170 +1*x4171 +1*x4172 +1*x4173 +1*x4174 +1*x4175 +1*x4176 +1*x4177 +1*x4178 +1*x4179 +1*x4180 +1*x4181 +1*x4182 +1*x4183 +1*x4184 +1*x4185 +1*x4186 +1*x4187 +1*x4188 +1*x4189 +1*x4190 +1*x4191 +1*x4192 +1*x4193 +1*x4194 +1*x4195 +1*x4196 +1*x4197 +1*x4198 +1*x4199 +1*x4200 +1*x4201 +1*x4202 +1*x4203 +1*x4204 +1*x4205 +1*x4206 +1*x4207 +1*x4208 +1*x4209 +1*x4210 +1*x4211 +1*x4212 +1*x4213 +1*x4214 +1*x4215 +1*x4216 +1*x4217 +1*x4218 +1*x4219 +1*x4220 +1*x4221 +1*x4222 +1*x4223 +1*x4224 +1*x4225 +1*x4226 +1*x4227 +1*x4228 +1*x4229 +1*x4230 +1*x4231 +1*x4232 +1*x4233 +1*x4234 +1*x4235 +1*x4236 +1*x4237 +1*x4238 +1*x4239 +1*x4240 +1*x4241 +1*x4242 +1*x4243 +1*x4244 +1*x4245 +1*x4246 +1*x4247 +1*x4248 +1*x4249 +1*x4250 +1*x4251 +1*x4252 +1*x4253 +1*x4254 +1*x4255 +1*x4256 +1*x4257 +1*x4258 +1*x4259 +1*x4260 +1*x4261 +1*x4262 +1*x4263 +1*x4264 +1*x4265 +1*x4266 +1*x4267 +1*x4268 +1*x4269 +1*x4270 +1*x4271 +1*x4272 +1*x4273 +1*x4274 +1*x4275 +1*x4276 +1*x4277 +1*x4278 +1*x4279 +1*x4280 +1*x4281 +1*x4282 +1*x4283 +1*x4284 +1*x4285 +1*x4286 +1*x4287 +1*x4288 +1*x4289 +1*x4290 +1*x4291 +1*x4292 +1*x4293 +1*x4294 +1*x4295 +1*x4296 +1*x4297 +1*x4298 +1*x4299 +1*x4300 +1*x4301 +1*x4302 +1*x4303 +1*x4304 +1*x4305 +1*x4306 +1*x4307 +1*x4308 +1*x4309 +1*x4310 +1*x4311 +1*x4312 +1*x4313 +1*x4314 +1*x4315 +1*x4316 +1*x4317 +1*x4318 +1*x4319 +1*x4320 +1*x4321 +1*x4322 +1*x4323 +1*x4324 +1*x4325 +1*x4326 +1*x4327 +1*x4328 +1*x4329 +1*x4330 +1*x4331 +1*x4332 +1*x4333 +1*x4334 +1*x4335 +1*x4336 +1*x4337 +1*x4338 +1*x4339 +1*x4340 +1*x4341 +1*x4342 +1*x4343 +1*x4344 +1*x4345 +1*x4346 +1*x4347 +1*x4348 +1*x4349 +1*x4350 +1*x4351 +1*x4352 +1*x4353 +1*x4354 +1*x4355 +1*x4356 +1*x4357 +1*x4358 +1*x4359 +1*x4360 +1*x4361 +1*x4362 +1*x4363 +1*x4364 +1*x4365 +1*x4366 +1*x4367 +1*x4368 +1*x4369 +1*x4370 +1*x4371 +1*x4372 +1*x4373 +1*x4374 +1*x4375 +1*x4376 +1*x4377 +1*x4378 +1*x4379 +1*x4380 +1*x4381 +1*x4382 +1*x4383 +1*x4384 +1*x4385 +1*x4386 +1*x4387 +1*x4388 +1*x4389 +1*x4390 +1*x4391 +1*x4392 +1*x4393 +1*x4394 +1*x4395 +1*x4396 +1*x4397 +1*x4398 +1*x4399 +1*x4400 +1*x4401 +1*x4402 +1*x4403 +1*x4404 +1*x4405 +1*x4406 +1*x4407 +1*x4408 +1*x4409 +1*x4410 +1*x4411 +1*x4412 +1*x4413 +1*x4414 +1*x4415 +1*x4416 +1*x4417 +1*x4418 +1*x4419 +1*x4420 +1*x4421 +1*x4422 +1*x4423 +1*x4424 +1*x4425 +1*x4426 +1*x4427 +1*x4428 +1*x4429 +1*x4430 +1*x4431 +1*x4432 +1*x4433 +1*x4434 +1*x4435 +1*x4436 +1*x4437 +1*x4438 +1*x4439 +1*x4440 +1*x4441 +1*x4442 +1*x4443 +1*x4444 +1*x4445 +1*x4446 +1*x4447 +1*x4448 +1*x4449 +1*x4450 +1*x4451 +1*x4452 +1*x4453 +1*x4454 +1*x4455 +1*x4456 +1*x4457 +1*x4458 +1*x4459 +1*x4460 +1*x4461 +1*x4462 +1*x4463 +1*x4464 +1*x4465 +1*x4466 +1*x4467 +1*x4468 +1*x4469 +1*x4470 +1*x4471 +1*x4472 +1*x4473 +1*x4474 +1*x4475 +1*x4476 +1*x4477 +1*x4478 +1*x4479 +1*x4480 +1*x4481 +1*x4482 +1*x4483 +1*x4484 +1*x4485 +1*x4486 +1*x4487 +1*x4488 +1*x4489 +1*x4490 +1*x4491 +1*x4492 +1*x4493 +1*x4494 +1*x4495 +1*x4496 +1*x4497 +1*x4498 +1*x4499 +1*x4500 +1*x4501 +1*x4502 +1*x4503 +1*x4504 +1*x4505 +1*x4506 +1*x4507 +1*x4508 +1*x4509 +1*x4510 +1*x4511 +1*x4512 +1*x4513 +1*x4514 +1*x4515 +1*x4516 +1*x4517 +1*x4518 +1*x4519 +1*x4520 +1*x4521 +1*x4522 +1*x4523 +1*x4524 +1*x4525 +1*x4526 +1*x4527 +1*x4528 +1*x4529 +1*x4530 +1*x4531 +1*x4532 +1*x4533 +1*x4534 +1*x4535 +1*x4536 +1*x4537 +1*x4538 +1*x4539 +1*x4540 +1*x4541 +1*x4542 +1*x4543 +1*x4544 +1*x4545 +1*x4546 +1*x4547 +1*x4548 +1*x4549 +1*x4550 +1*x4551 +1*x4552 +1*x4553 +1*x4554 +1*x4555 +1*x4556 +1*x4557 +1*x4558 +1*x4559 +1*x4560 +1*x4561 +1*x4562 +1*x4563 +1*x4564 +1*x4565 +1*x4566 +1*x4567 +1*x4568 +1*x4569 +1*x4570 +1*x4571 +1*x4572 +1*x4573 +1*x4574 +1*x4575 +1*x4576 +1*x4577 +1*x4578 +1*x4579 +1*x4580 +1*x4581 +1*x4582 +1*x4583 +1*x4584 +1*x4585 +1*x4586 +1*x4587 +1*x4588 +1*x4589 +1*x4590 +1*x4591 +1*x4592 +1*x4593 +1*x4594 +1*x4595 +1*x4596 +1*x4597 +1*x4598 +1*x4599 +1*x4600 +1*x4601 +1*x4602 +1*x4603 +1*x4604 +1*x4605 +1*x4606 +1*x4607 +1*x4608 +1*x4609 +1*x4610 +1*x4611 +1*x4612 +1*x4613 +1*x4614 +1*x4615 +1*x4616 +1*x4617 +1*x4618 +1*x4619 +1*x4620 +1*x4621 +1*x4622 +1*x4623 +1*x4624 +1*x4625 +1*x4626 +1*x4627 +1*x4628 +1*x4629 +1*x4630 +1*x4631 +1*x4632 +1*x4633 +1*x4634 +1*x4635 +1*x4636 +1*x4637 +1*x4638 +1*x4639 +1*x4640 +1*x4641 +1*x4642 +1*x4643 +1*x4644 +1*x4645 +1*x4646 +1*x4647 +1*x4648 +1*x4649 +1*x4650 +1*x4651 +1*x4652 +1*x4653 +1*x4654 +1*x4655 +1*x4656 +1*x4657 +1*x4658 +1*x4659 +1*x4660 +1*x4661 +1*x4662 +1*x4663 +1*x4664 +1*x4665 +1*x4666 +1*x4667 +1*x4668 +1*x4669 +1*x4670 +1*x4671 +1*x4672 +1*x4673 +1*x4674 +1*x4675 +1*x4676 +1*x4677 ;
+1*x1 +1*x2 +1*x3 +1*x4 +1*x5 +1*x6 +1*x7 +1*x8 +1*x9 +1*x10 +1*x11 +1*x12 +1*x13 +1*x14 +1*x15 +1*x16 +1*x17 +1*x18 +1*x19 +1*x20 +1*x21 +1*x22 +1*x23 +1*x24 >= +1;
+1*x25 +1*x26 +1*x27 +1*x28 +1*x29 +1*x30 +1*x31 +1*x32 +1*x33 +1*x34 +1*x35 +1*x36 +1*x37 +1*x38 +1*x39 +1*x40 +1*x41 +1*x42 +1*x43 +1*x44 >= +1;
+1*x45 +1*x46 +1*x47 +1*x48 +1*x30 +1*x49 +1*x50 +1*x51 +1*x52 +1*x53 +1*x54 +1*x55 +1*x56 +1*x33 +1*x57 +1*x58 +1*x59 +1*x60 +1*x61 +1*x62 +1*x63 +1*x40 +1*x64 +1*x41 +1*x65 +1*x66 +1*x67 +1*x68 >= +1;
+1*x69 +1*x25 +1*x70 +1*x71 +1*x28 +1*x29 +1*x72 +1*x73 >= +1;
+1*x74 +1*x75 +1*x76 +1*x77 +1*x78 +1*x79 +1*x80 +1*x81 +1*x82 +1*x47 +1*x48 +1*x83 +1*x84 +1*x85 +1*x86 +1*x33 +1*x87 +1*x36 +1*x88 +1*x89 +1*x90 +1*x41 +1*x91 +1*x92 +1*x93 >= +1;
+1*x94 +1*x95 +1*x96 +1*x97 +1*x98 +1*x99 +1*x100 +1*x101 +1*x102 +1*x103 >= +1;
+1*x94 +1*x95 +1*x104 +1*x96 +1*x97 +1*x105 +1*x98 +1*x99 +1*x106 +1*x107 +1*x100 +1*x108 +1*x101 +1*x109 +1*x110 +1*x111 +1*x112 +1*x113 +1*x114 +1*x115 +1*x116 +1*x117 +1*x118 +1*x119 >= +1;
+1*x94 +1*x95 +1*x104 +1*x96 +1*x105 +1*x99 +1*x106 +1*x107 +1*x120 +1*x121 +1*x122 +1*x123 +1*x103 +1*x124 >= +1;
+1*x125 +1*x63 +1*x126 >= +1;
+1*x127 +1*x128 +1*x129 +1*x130 +1*x131 +1*x132 +1*x133 +1*x134 +1*x135 +1*x136 +1*x137 +1*x138 +1*x139 +1*x140 +1*x141 +1*x142 +1*x143 +1*x144 +1*x145 +1*x146 +1*x147 +1*x148 +1*x149 +1*x150 +1*x151 +1*x152 +1*x153 +1*x154 +1*x155 +1*x156 >= +1;
+1*x157 +1*x158 +1*x159 +1*x51 +1*x160 +1*x53 +1*x161 +1*x55 +1*x162 +1*x163 +1*x164 +1*x165 +1*x166 >= +1;
+1*x167 +1*x168 +1*x169 +1*x170 +1*x171 +1*x172 +1*x173 +1*x31 +1*x174 +1*x9 +1*x175 +1*x176 +1*x177 +1*x178 +1*x179 +1*x180 +1*x181 +1*x182 +1*x183 +1*x184 +1*x185 +1*x186 >= +1;
+1*x187 +1*x188 +1*x189 +1*x190 +1*x191 +1*x192 +1*x193 >= +1;
+1*x187 +1*x188 +1*x190 +1*x194 +1*x195 +1*x196 +1*x197 +1*x198 +1*x199 +1*x200 +1*x201 +1*x202 +1*x203 +1*x204 +1*x205 +1*x206 +1*x207 +1*x208 >= +1;
+1*x209 +1*x210 +1*x211 +1*x212 +1*x213 +1*x214 +1*x215 +1*x216 +1*x217 +1*x218 +1*x219 +1*x220 +1*x221 +1*x222 +1*x223 +1*x224 +1*x225 +1*x226 +1*x227 +1*x228 +1*x229 +1*x230 +1*x231 +1*x232 +1*x233 +1*x234 +1*x68 >= +1;
+1*x235 +1*x236 +1*x237 +1*x238 +1*x239 +1*x240 +1*x241 +1*x242 +1*x243 +1*x244 +1*x245 +1*x246 +1*x247 +1*x248 +1*x249 +1*x250 +1*x251 +1*x252 +1*x253 +1*x254 +1*x255 >= +1;
+1*x235 +1*x236 +1*x237 +1*x238 +1*x239 +1*x256 +1*x257 +1*x241 +1*x242 +1*x243 +1*x244 +1*x210 +1*x214 +1*x258 +1*x259 +1*x218 +1*x247 +1*x249 +1*x250 +1*x260 +1*x227 +1*x261 >= +1;
+1*x262 +1*x263 +1*x264 +1*x265 +1*x266 +1*x267 +1*x268 +1*x269 +1*x270 +1*x271 +1*x272 +1*x273 +1*x274 +1*x275 +1*x276 +1*x277 +1*x13 +1*x278 +1*x279 +1*x280 +1*x281 +1*x282 +1*x283 +1*x284 +1*x285 +1*x286 +1*x287 +1*x288 +1*x289 +1*x290 +1*x291 +1*x292 +1*x293 +1*x294 +1*x295 +1*x296 +1*x297 +1*x298 +1*x299 +1*x300 +1*x301 +1*x302 +1*x303 +1*x304 +1*x305 +1*x306 +1*x307 +1*x308 >= +1;
+1*x309 +1*x310 +1*x266 +1*x267 +1*x311 +1*x312 +1*x277 +1*x313 +1*x314 +1*x315 +1*x280 +1*x291 +1*x293 +1*x294 +1*x316 +1*x317 +1*x318 +1*x319 >= +1;
+1*x320 +1*x321 +1*x263 +1*x322 +1*x323 +1*x324 +1*x325 +1*x326 +1*x327 +1*x328 +1*x329 +1*x330 +1*x331 +1*x282 +1*x332 +1*x333 +1*x334 +1*x335 +1*x336 >= +1;
+1*x320 +1*x337 +1*x321 +1*x263 +1*x322 +1*x4 +1*x323 +1*x324 +1*x338 +1*x12 +1*x13 +1*x326 +1*x327 +1*x15 +1*x18 +1*x19 +1*x339 +1*x340 +1*x332 +1*x22 +1*x341 >= +1;
+1*x342 +1*x343 +1*x344 +1*x325 +1*x345 +1*x346 +1*x347 +1*x348 +1*x349 +1*x350 +1*x351 +1*x352 +1*x331 +1*x143 +1*x121 +1*x353 +1*x354 +1*x355 +1*x356 +1*x357 +1*x358 +1*x359 +1*x360 +1*x361 +1*x362 +1*x180 +1*x363 +1*x364 +1*x365 +1*x366 >= +1;
+1*x367 +1*x368 +1*x369 +1*x370 +1*x371 +1*x372 +1*x373 +1*x374 +1*x375 +1*x376 +1*x377 +1*x378 +1*x379 +1*x380 +1*x381 +1*x58 +1*x60 +1*x382 +1*x383 +1*x384 +1*x385 >= +1;
+1*x367 +1*x368 +1*x262 +1*x369 +1*x370 +1*x372 +1*x373 +1*x265 +1*x266 +1*x386 +1*x387 +1*x388 +1*x374 +1*x389 +1*x375 +1*x377 +1*x378 +1*x379 +1*x273 +1*x274 +1*x275 +1*x390 +1*x278 +1*x391 +1*x381 +1*x392 +1*x58 +1*x315 +1*x60 +1*x382 +1*x393 +1*x286 +1*x295 +1*x297 +1*x298 +1*x394 +1*x395 +1*x317 +1*x396 +1*x397 +1*x318 +1*x398 +1*x319 +1*x399 +1*x400 >= +1;
+1*x367 +1*x368 +1*x262 +1*x369 +1*x370 +1*x371 +1*x372 +1*x373 +1*x265 +1*x266 +1*x386 +1*x387 +1*x388 +1*x374 +1*x389 +1*x375 +1*x376 +1*x380 +1*x270 +1*x271 +1*x273 +1*x274 +1*x275 +1*x401 +1*x390 +1*x278 +1*x402 +1*x393 +1*x403 +1*x283 +1*x404 +1*x286 +1*x288 +1*x295 +1*x297 +1*x298 +1*x304 +1*x305 >= +1;
+1*x405 +1*x406 +1*x407 +1*x309 +1*x408 +1*x45 +1*x47 +1*x409 +1*x410 +1*x64 +1*x93 >= +1;
+1*x411 +1*x412 +1*x80 +1*x413 +1*x414 +1*x81 +1*x173 +1*x415 +1*x416 +1*x417 +1*x418 +1*x419 +1*x420 +1*x421 +1*x422 +1*x423 +1*x424 +1*x425 +1*x88 +1*x426 +1*x427 +1*x428 +1*x429 +1*x178 +1*x92 +1*x430 +1*x431 >= +1;
+1*x432 +1*x433 +1*x434 +1*x435 +1*x105 +1*x343 +1*x436 +1*x106 +1*x410 +1*x437 +1*x438 +1*x352 +1*x439 +1*x120 +1*x121 +1*x122 +1*x123 +1*x440 +1*x441 +1*x442 +1*x443 +1*x444 +1*x445 +1*x446 +1*x360 +1*x447 +1*x448 +1*x449 +1*x450 +1*x363 >= +1;
+1*x369 +1*x371 +1*x265 +1*x451 +1*x452 +1*x453 +1*x454 +1*x455 +1*x380 +1*x456 +1*x457 +1*x270 +1*x458 +1*x459 +1*x403 +1*x404 +1*x288 +1*x460 >= +1;
+1*x461 +1*x462 +1*x463 +1*x310 +1*x312 +1*x464 +1*x465 +1*x466 +1*x467 +1*x468 +1*x469 +1*x470 +1*x471 +1*x472 +1*x137 +1*x473 +1*x474 +1*x475 +1*x476 +1*x477 +1*x478 +1*x479 +1*x480 +1*x481 +1*x291 +1*x482 +1*x483 +1*x148 +1*x484 +1*x485 +1*x486 +1*x487 +1*x488 +1*x489 +1*x490 +1*x491 +1*x335 +1*x492 +1*x493 +1*x494 >= +1;
+1*x461 +1*x462 +1*x463 +1*x310 +1*x312 +1*x467 +1*x468 +1*x471 +1*x475 +1*x476 +1*x477 +1*x291 +1*x293 >= +1;
+1*x461 +1*x462 +1*x463 +1*x310 +1*x312 +1*x464 +1*x466 +1*x495 +1*x468 +1*x469 +1*x470 +1*x472 +1*x474 +1*x475 +1*x481 +1*x496 +1*x497 +1*x485 +1*x498 +1*x486 +1*x499 +1*x500 +1*x501 +1*x207 +1*x502 >= +1;
+1*x461 +1*x462 +1*x463 +1*x310 +1*x464 +1*x465 +1*x466 +1*x467 +1*x495 +1*x472 +1*x137 +1*x474 +1*x480 +1*x483 +1*x503 +1*x504 +1*x505 +1*x506 >= +1;
+1*x507 +1*x508 +1*x134 +1*x135 +1*x509 +1*x142 +1*x331 +1*x143 +1*x361 +1*x180 +1*x510 +1*x364 >= +1;
+1*x511 +1*x169 +1*x512 +1*x513 +1*x170 +1*x514 +1*x515 +1*x516 +1*x174 +1*x517 +1*x518 +1*x519 +1*x520 +1*x521 +1*x522 +1*x523 +1*x524 +1*x510 +1*x525 +1*x526 +1*x527 >= +1;
+1*x528 +1*x190 +1*x529 +1*x194 +1*x530 +1*x531 +1*x532 +1*x533 +1*x534 +1*x535 +1*x452 +1*x536 +1*x192 +1*x458 +1*x537 +1*x538 +1*x539 +1*x540 +1*x541 +1*x542 +1*x543 +1*x544 +1*x545 +1*x546 >= +1;
+1*x528 +1*x190 +1*x529 +1*x194 +1*x530 +1*x531 +1*x532 +1*x533 +1*x534 +1*x535 +1*x452 +1*x536 +1*x192 +1*x458 +1*x537 +1*x538 +1*x542 +1*x199 +1*x201 +1*x202 +1*x547 +1*x203 +1*x548 +1*x299 +1*x300 +1*x302 +1*x549 +1*x501 +1*x550 +1*x460 +1*x551 +1*x552 +1*x553 +1*x554 >= +1;
+1*x555 +1*x556 +1*x557 +1*x558 +1*x529 +1*x532 +1*x533 +1*x534 +1*x559 +1*x560 +1*x561 +1*x562 +1*x563 +1*x564 +1*x565 +1*x566 +1*x330 +1*x567 +1*x199 +1*x568 +1*x569 +1*x570 +1*x571 +1*x572 +1*x573 +1*x574 +1*x575 +1*x576 +1*x577 +1*x578 +1*x579 >= +1;
+1*x528 +1*x580 +1*x581 +1*x582 +1*x451 +1*x583 +1*x452 +1*x584 +1*x540 +1*x585 +1*x201 +1*x586 +1*x587 +1*x588 +1*x589 +1*x590 >= +1;
+1*x528 +1*x580 +1*x581 +1*x531 +1*x532 +1*x534 +1*x582 +1*x451 +1*x591 +1*x592 +1*x583 +1*x452 +1*x456 +1*x457 +1*x458 +1*x593 +1*x540 +1*x585 +1*x594 +1*x459 +1*x542 +1*x595 +1*x586 +1*x596 +1*x597 +1*x598 +1*x599 +1*x600 +1*x543 +1*x544 +1*x601 +1*x602 +1*x603 +1*x604 +1*x605 +1*x606 >= +1;
+1*x557 +1*x607 +1*x608 +1*x562 +1*x609 +1*x610 +1*x611 +1*x612 +1*x613 +1*x614 +1*x615 +1*x616 +1*x617 +1*x618 +1*x619 +1*x570 +1*x424 +1*x572 +1*x620 +1*x621 +1*x622 +1*x623 +1*x624 +1*x625 +1*x626 +1*x427 +1*x627 +1*x628 +1*x629 +1*x630 >= +1;
+1*x557 +1*x607 +1*x532 +1*x534 +1*x608 +1*x609 +1*x592 +1*x631 +1*x610 +1*x593 +1*x611 +1*x612 +1*x459 +1*x632 +1*x619 +1*x633 +1*x574 +1*x634 +1*x635 +1*x553 +1*x636 +1*x637 >= +1;
+1*x638 +1*x237 +1*x639 +1*x640 +1*x641 +1*x642 +1*x643 +1*x242 +1*x644 +1*x645 +1*x613 +1*x614 +1*x259 +1*x646 +1*x647 +1*x648 +1*x220 +1*x596 +1*x598 +1*x649 +1*x620 +1*x650 +1*x651 +1*x621 +1*x652 +1*x601 +1*x602 +1*x653 +1*x654 >= +1;
+1*x655 +1*x656 +1*x657 +1*x658 +1*x659 +1*x660 +1*x10 +1*x661 +1*x662 +1*x663 +1*x664 +1*x665 +1*x666 +1*x667 +1*x668 +1*x669 +1*x670 +1*x671 +1*x672 +1*x16 +1*x17 +1*x18 +1*x673 +1*x21 +1*x674 +1*x675 +1*x177 +1*x676 +1*x677 +1*x678 +1*x679 +1*x181 +1*x680 +1*x681 +1*x682 +1*x683 +1*x684 +1*x685 +1*x686 >= +1;
+1*x687 +1*x688 +1*x689 +1*x690 +1*x691 +1*x692 +1*x28 +1*x376 +1*x693 +1*x694 +1*x695 +1*x696 +1*x32 +1*x402 +1*x697 +1*x698 +1*x699 +1*x700 +1*x701 +1*x42 +1*x702 +1*x677 +1*x385 +1*x703 +1*x682 +1*x684 +1*x685 >= +1;
+1*x687 +1*x688 +1*x689 +1*x690 +1*x691 +1*x692 +1*x28 +1*x694 +1*x704 +1*x695 +1*x705 +1*x32 +1*x706 +1*x697 +1*x707 +1*x708 +1*x698 +1*x34 +1*x35 +1*x40 +1*x709 +1*x41 +1*x42 +1*x710 +1*x43 +1*x711 >= +1;
+1*x712 +1*x713 +1*x687 +1*x690 +1*x714 +1*x715 +1*x716 +1*x717 +1*x718 +1*x696 +1*x49 +1*x719 +1*x720 +1*x55 +1*x162 +1*x721 +1*x722 +1*x723 +1*x724 +1*x725 +1*x699 +1*x40 +1*x726 +1*x709 +1*x727 +1*x728 +1*x729 +1*x730 +1*x731 +1*x732 +1*x733 >= +1;
+1*x734 +1*x78 +1*x735 +1*x736 +1*x737 +1*x738 +1*x739 +1*x740 +1*x89 +1*x741 +1*x742 +1*x743 +1*x744 +1*x745 +1*x746 >= +1;
+1*x734 +1*x78 +1*x690 +1*x747 +1*x748 +1*x749 +1*x735 +1*x750 +1*x82 +1*x715 +1*x736 +1*x751 +1*x752 +1*x737 +1*x753 +1*x87 +1*x89 +1*x90 +1*x726 +1*x709 +1*x754 +1*x41 +1*x91 +1*x92 +1*x755 +1*x756 >= +1;
+1*x757 +1*x758 +1*x759 +1*x760 +1*x761 +1*x762 +1*x763 +1*x764 >= +1;
+1*x757 +1*x765 +1*x766 +1*x767 +1*x768 +1*x769 +1*x656 +1*x763 +1*x658 +1*x770 +1*x660 +1*x771 +1*x661 +1*x663 +1*x772 +1*x664 +1*x773 +1*x774 +1*x665 +1*x666 +1*x667 +1*x775 +1*x776 +1*x675 +1*x677 +1*x678 +1*x777 >= +1;
+1*x757 +1*x778 +1*x779 +1*x760 +1*x780 +1*x688 +1*x691 +1*x781 +1*x782 +1*x704 +1*x783 +1*x784 +1*x785 +1*x786 >= +1;
+1*x757 +1*x787 +1*x788 +1*x766 +1*x789 +1*x790 +1*x767 +1*x791 +1*x779 +1*x792 +1*x793 +1*x747 +1*x794 +1*x691 +1*x795 +1*x796 +1*x749 +1*x797 +1*x798 +1*x799 +1*x800 +1*x801 +1*x802 +1*x803 +1*x770 +1*x804 +1*x805 +1*x771 +1*x72 +1*x806 +1*x807 +1*x808 +1*x809 +1*x751 +1*x810 +1*x661 +1*x811 +1*x812 +1*x813 +1*x773 +1*x708 +1*x814 +1*x753 +1*x665 +1*x666 +1*x775 +1*x815 +1*x816 +1*x817 +1*x90 +1*x428 +1*x818 +1*x819 +1*x820 +1*x675 +1*x821 +1*x92 +1*x755 +1*x710 +1*x822 +1*x823 +1*x824 >= +1;
+1*x789 +1*x825 +1*x790 +1*x826 +1*x747 +1*x794 +1*x748 +1*x827 +1*x796 +1*x828 +1*x802 +1*x803 +1*x258 +1*x809 +1*x829 +1*x751 +1*x810 +1*x830 +1*x812 +1*x831 +1*x832 +1*x87 +1*x833 +1*x113 +1*x834 +1*x90 +1*x260 +1*x835 +1*x836 +1*x837 +1*x117 +1*x838 +1*x839 >= +1;
+1*x840 +1*x841 +1*x842 +1*x843 +1*x844 +1*x466 +1*x845 +1*x846 +1*x847 +1*x848 +1*x717 +1*x849 +1*x850 +1*x851 +1*x852 +1*x161 +1*x162 +1*x144 +1*x503 +1*x853 +1*x854 +1*x151 +1*x855 +1*x856 +1*x857 +1*x156 +1*x858 +1*x859 >= +1;
+1*x840 +1*x841 +1*x842 +1*x843 +1*x844 +1*x848 +1*x717 +1*x849 +1*x850 +1*x851 +1*x860 +1*x861 +1*x862 +1*x863 +1*x864 +1*x865 >= +1;
+1*x866 +1*x867 +1*x868 +1*x869 +1*x870 +1*x871 +1*x872 +1*x873 +1*x851 +1*x874 +1*x875 >= +1;
+1*x769 +1*x876 +1*x877 +1*x771 +1*x878 +1*x879 +1*x880 +1*x881 +1*x882 +1*x883 +1*x774 +1*x884 +1*x885 +1*x886 +1*x775 +1*x887 +1*x776 +1*x888 +1*x889 +1*x890 +1*x820 +1*x891 +1*x892 +1*x893 +1*x894 +1*x895 +1*x896 >= +1;
+1*x897 +1*x898 +1*x899 +1*x900 +1*x901 +1*x902 +1*x903 +1*x904 +1*x905 +1*x886 +1*x906 +1*x907 +1*x908 +1*x909 +1*x888 +1*x910 +1*x890 +1*x911 +1*x912 +1*x913 +1*x914 +1*x893 +1*x915 +1*x916 +1*x917 +1*x918 +1*x919 +1*x920 +1*x921 >= +1;
+1*x922 +1*x923 +1*x924 +1*x925 +1*x926 +1*x927 +1*x928 +1*x813 +1*x929 +1*x930 +1*x931 +1*x932 +1*x933 +1*x934 +1*x935 +1*x936 +1*x937 +1*x938 +1*x939 +1*x940 >= +1;
+1*x793 +1*x749 +1*x797 +1*x941 +1*x942 +1*x943 +1*x944 +1*x945 +1*x946 +1*x807 +1*x808 +1*x811 +1*x947 +1*x948 +1*x949 +1*x950 +1*x951 +1*x952 +1*x953 +1*x954 +1*x955 +1*x956 +1*x635 +1*x957 +1*x637 >= +1;
+1*x958 +1*x827 +1*x749 +1*x959 +1*x945 +1*x960 +1*x828 +1*x946 +1*x961 +1*x962 +1*x901 +1*x902 +1*x811 +1*x752 +1*x963 +1*x964 +1*x831 +1*x905 +1*x965 +1*x886 +1*x966 +1*x832 +1*x907 +1*x953 +1*x910 +1*x914 +1*x967 +1*x893 +1*x968 +1*x915 +1*x969 +1*x917 +1*x918 +1*x970 +1*x920 >= +1;
+1*x958 +1*x827 +1*x749 +1*x241 +1*x959 +1*x945 +1*x960 +1*x828 +1*x946 +1*x961 +1*x971 +1*x244 +1*x258 +1*x972 +1*x947 +1*x963 +1*x964 +1*x831 +1*x965 +1*x248 +1*x966 +1*x832 +1*x973 +1*x951 +1*x932 +1*x974 +1*x967 +1*x936 +1*x975 +1*x976 +1*x252 +1*x969 +1*x938 +1*x977 +1*x978 +1*x979 +1*x980 >= +1;
+1*x981 +1*x982 +1*x983 +1*x367 +1*x984 +1*x262 +1*x689 +1*x985 +1*x986 +1*x692 +1*x987 +1*x988 +1*x386 +1*x376 +1*x989 +1*x990 +1*x991 +1*x992 +1*x993 +1*x696 +1*x994 +1*x995 +1*x996 +1*x997 +1*x998 +1*x999 +1*x727 +1*x730 +1*x1000 +1*x1001 >= +1;
+1*x981 +1*x982 +1*x983 +1*x367 +1*x984 +1*x262 +1*x985 +1*x986 +1*x987 +1*x988 +1*x386 +1*x1002 +1*x1003 +1*x377 +1*x989 +1*x379 +1*x1004 +1*x990 +1*x991 +1*x992 +1*x390 +1*x994 +1*x996 +1*x1005 +1*x1006 +1*x997 +1*x382 +1*x1007 +1*x1008 +1*x396 +1*x398 +1*x998 +1*x1009 +1*x399 +1*x1010 +1*x400 +1*x1011 >= +1;
+1*x987 +1*x1012 +1*x1013 +1*x714 +1*x1014 +1*x1015 +1*x696 +1*x1016 +1*x1017 +1*x1018 >= +1;
+1*x987 +1*x1012 +1*x1013 +1*x988 +1*x386 +1*x714 +1*x1019 +1*x1020 +1*x718 +1*x1014 +1*x1015 +1*x271 +1*x849 +1*x1021 +1*x994 +1*x1022 +1*x1017 +1*x722 +1*x723 +1*x1023 +1*x1024 +1*x1025 +1*x1026 +1*x1007 +1*x1008 +1*x396 +1*x1027 +1*x1028 +1*x725 +1*x1029 +1*x1030 +1*x1031 +1*x1032 +1*x1033 >= +1;
+1*x762 +1*x1034 +1*x763 +1*x1035 +1*x1036 +1*x1037 +1*x1038 +1*x1039 +1*x1040 +1*x804 +1*x1041 +1*x1042 +1*x764 +1*x276 +1*x1043 +1*x1044 +1*x1045 +1*x1046 +1*x1047 +1*x1048 +1*x1049 +1*x1050 +1*x1051 +1*x1052 +1*x1053 +1*x1054 +1*x1055 +1*x1056 +1*x1057 +1*x1058 +1*x1059 +1*x1060 +1*x1061 +1*x1062 +1*x1063 +1*x1064 +1*x1065 +1*x1066 +1*x1067 +1*x1068 >= +1;
+1*x1069 +1*x1070 +1*x1071 +1*x1072 +1*x1073 +1*x1074 +1*x1075 +1*x1076 +1*x1077 +1*x1078 +1*x1079 +1*x1080 +1*x1081 +1*x1082 +1*x1083 +1*x1084 +1*x1085 +1*x307 +1*x1086 +1*x1087 +1*x1088 >= +1;
+1*x1089 +1*x1090 +1*x1091 +1*x1092 +1*x1093 +1*x1077 +1*x1094 +1*x1078 +1*x1095 +1*x1096 +1*x1097 +1*x1098 +1*x1099 +1*x1100 +1*x1101 +1*x1102 +1*x1103 +1*x1104 >= +1;
+1*x798 +1*x1002 +1*x1003 +1*x1105 +1*x377 +1*x1106 +1*x1004 +1*x1107 +1*x805 +1*x1108 +1*x1109 +1*x1110 +1*x1111 +1*x1112 +1*x1005 +1*x1113 +1*x1006 +1*x382 +1*x586 +1*x1114 +1*x1115 +1*x1116 +1*x1117 +1*x1007 +1*x1118 +1*x1119 +1*x1120 +1*x1009 +1*x1010 +1*x1011 >= +1;
+1*x1121 +1*x1122 +1*x1123 +1*x1124 +1*x1108 +1*x1111 +1*x1112 +1*x1113 +1*x1125 +1*x1126 >= +1;
+1*x1121 +1*x1122 +1*x1108 +1*x1127 +1*x1128 +1*x1129 +1*x1017 +1*x1130 +1*x1115 +1*x1024 +1*x1025 +1*x1117 +1*x1007 +1*x1118 +1*x1027 +1*x1028 +1*x1131 +1*x1132 +1*x1031 >= +1;
+1*x787 +1*x1133 +1*x788 +1*x767 +1*x1134 +1*x1135 +1*x1136 +1*x1137 +1*x1138 +1*x792 +1*x1139 +1*x1140 +1*x794 +1*x795 +1*x1141 +1*x796 +1*x1142 +1*x798 +1*x800 +1*x1143 +1*x1144 +1*x1145 +1*x1146 +1*x1147 +1*x1148 +1*x804 +1*x1106 +1*x805 +1*x806 +1*x1149 +1*x1150 +1*x610 +1*x810 +1*x1151 +1*x1152 +1*x1153 +1*x1154 +1*x1109 +1*x618 +1*x1155 +1*x1111 +1*x1005 +1*x1113 +1*x1006 +1*x1156 +1*x1049 +1*x708 +1*x1157 +1*x1050 +1*x423 +1*x1158 +1*x1159 +1*x1160 +1*x1161 +1*x1054 +1*x1162 +1*x1163 +1*x1164 +1*x1165 +1*x625 +1*x1166 +1*x427 +1*x1167 +1*x428 +1*x818 +1*x835 +1*x1062 +1*x1168 +1*x836 +1*x1064 +1*x1065 +1*x1066 +1*x1169 +1*x627 +1*x1170 +1*x1171 +1*x628 +1*x1172 +1*x1173 +1*x630 >= +1;
+1*x787 +1*x1133 +1*x788 +1*x767 +1*x1134 +1*x1135 +1*x1136 +1*x1137 +1*x1138 +1*x792 +1*x793 +1*x1139 +1*x1140 +1*x794 +1*x795 +1*x1141 +1*x796 +1*x797 +1*x1142 +1*x1143 +1*x1144 +1*x1145 +1*x1146 +1*x946 +1*x1174 +1*x1150 +1*x610 +1*x808 +1*x810 +1*x1175 +1*x1151 +1*x1176 +1*x1177 +1*x423 +1*x1158 +1*x1159 +1*x1160 +1*x1178 +1*x1179 +1*x954 >= +1;
+1*x1139 +1*x1140 +1*x1142 +1*x1180 +1*x1091 +1*x1181 +1*x1123 +1*x1124 +1*x1093 +1*x1095 +1*x1182 +1*x1111 +1*x1113 +1*x1183 +1*x1184 +1*x1096 +1*x1185 +1*x1186 +1*x1187 +1*x1100 +1*x1101 +1*x1102 +1*x1188 +1*x1009 +1*x1189 +1*x1190 +1*x1191 >= +1;
+1*x1192 +1*x1193 +1*x1194 +1*x991 +1*x1195 +1*x992 +1*x475 +1*x1196 +1*x1197 +1*x1198 +1*x1199 +1*x1200 +1*x1201 +1*x997 +1*x1047 +1*x1202 +1*x1048 +1*x1203 +1*x1204 +1*x477 +1*x479 +1*x1205 +1*x1206 +1*x1207 +1*x1208 +1*x486 +1*x1209 +1*x1210 +1*x1211 +1*x1212 +1*x1213 +1*x1214 +1*x1215 +1*x1216 +1*x1217 +1*x333 +1*x1218 +1*x1219 +1*x1220 +1*x1221 +1*x489 +1*x1222 +1*x1223 +1*x1224 +1*x493 +1*x1225 +1*x1226 >= +1;
+1*x1227 +1*x840 +1*x461 +1*x841 +1*x1228 +1*x1229 +1*x1230 +1*x1231 +1*x466 +1*x1232 +1*x846 +1*x847 +1*x495 +1*x1014 +1*x849 +1*x850 +1*x1233 +1*x851 +1*x1234 +1*x473 +1*x1235 +1*x1236 +1*x503 +1*x1237 +1*x151 +1*x857 >= +1;
+1*x1238 +1*x1239 +1*x1240 +1*x1241 +1*x1242 +1*x1243 +1*x1244 +1*x1245 +1*x1246 +1*x1247 +1*x326 +1*x1248 +1*x1249 +1*x1250 +1*x1251 +1*x1252 +1*x340 +1*x22 >= +1;
+1*x1228 +1*x1253 +1*x1254 +1*x1255 +1*x1256 +1*x850 +1*x509 +1*x473 +1*x142 +1*x478 +1*x479 +1*x1257 +1*x1258 +1*x1206 >= +1;
+1*x1227 +1*x1259 +1*x1260 +1*x841 +1*x1261 +1*x1262 +1*x1263 +1*x1264 +1*x1265 +1*x1232 +1*x847 +1*x1192 +1*x1266 +1*x1233 +1*x872 +1*x851 +1*x1267 +1*x1268 +1*x1218 +1*x976 +1*x1269 >= +1;
+1*x1270 +1*x1271 +1*x1272 +1*x1273 +1*x1274 +1*x1275 +1*x1040 +1*x539 +1*x540 +1*x541 +1*x1276 +1*x1277 +1*x1278 +1*x1279 +1*x1280 +1*x1281 +1*x1043 +1*x1282 +1*x1283 +1*x1284 +1*x544 +1*x545 +1*x569 +1*x1052 +1*x571 +1*x1285 +1*x1286 +1*x1287 +1*x1288 +1*x1289 +1*x1290 +1*x1291 +1*x1292 +1*x1293 +1*x1294 +1*x577 +1*x1295 >= +1;
+1*x1261 +1*x1296 +1*x1297 +1*x925 +1*x1265 +1*x1232 +1*x847 +1*x1127 +1*x1279 +1*x1298 +1*x1200 +1*x1299 +1*x1115 +1*x1300 +1*x1301 >= +1;
+1*x1134 +1*x1135 +1*x1302 +1*x1303 +1*x793 +1*x1304 +1*x1305 +1*x797 +1*x1143 +1*x608 +1*x943 +1*x1306 +1*x1307 +1*x1144 +1*x1195 +1*x610 +1*x593 +1*x808 +1*x1308 +1*x611 +1*x1109 +1*x618 +1*x1006 +1*x1309 +1*x1050 +1*x884 +1*x775 +1*x632 +1*x931 +1*x817 +1*x622 +1*x624 +1*x625 +1*x427 +1*x1167 +1*x1310 +1*x822 +1*x1311 +1*x1312 +1*x1313 >= +1;
+1*x1314 +1*x1315 +1*x1316 +1*x642 +1*x643 +1*x1317 +1*x1318 +1*x644 +1*x1319 +1*x621 +1*x1320 +1*x652 +1*x601 +1*x654 >= +1;
+1*x1321 +1*x1322 +1*x1323 +1*x1324 +1*x1325 +1*x1326 +1*x1327 +1*x1328 +1*x1329 +1*x1330 +1*x1331 +1*x1332 +1*x1333 +1*x1334 +1*x1335 +1*x1336 +1*x1337 +1*x1338 +1*x1339 +1*x1340 +1*x1341 +1*x1342 +1*x1343 +1*x1344 +1*x1345 +1*x1346 +1*x1347 +1*x1348 +1*x1349 >= +1;
+1*x1321 +1*x1322 +1*x1323 +1*x1324 +1*x1325 +1*x1326 +1*x1327 +1*x1328 +1*x1329 +1*x1330 +1*x1331 +1*x1332 +1*x1333 +1*x1334 +1*x1350 +1*x1351 +1*x1352 +1*x1335 +1*x1336 +1*x1353 +1*x1354 +1*x279 +1*x1355 +1*x1339 +1*x1340 +1*x1341 +1*x1342 +1*x1356 +1*x296 +1*x297 +1*x301 +1*x1357 +1*x1358 +1*x1359 +1*x1360 +1*x1361 +1*x1362 +1*x1363 +1*x1364 +1*x1365 +1*x1366 +1*x1367 +1*x303 +1*x1368 +1*x304 +1*x1369 +1*x1370 +1*x305 +1*x1371 +1*x1372 >= +1;
+1*x1373 +1*x1374 +1*x1375 +1*x1376 +1*x1377 +1*x1378 +1*x1379 +1*x1380 +1*x1381 +1*x1382 +1*x1383 +1*x1353 +1*x1384 +1*x1385 +1*x1386 +1*x279 +1*x1387 +1*x1388 +1*x1356 +1*x669 +1*x1389 +1*x1390 +1*x1391 +1*x296 +1*x1392 +1*x1357 +1*x1393 +1*x1394 +1*x1358 +1*x1359 +1*x1395 +1*x1360 +1*x1361 +1*x1362 +1*x1363 +1*x1364 +1*x1367 +1*x1396 +1*x1397 +1*x1398 +1*x1399 +1*x304 +1*x1369 +1*x1371 +1*x1400 >= +1;
+1*x1401 +1*x1402 +1*x1403 +1*x1404 +1*x1405 +1*x1406 +1*x1374 +1*x1407 +1*x1376 +1*x131 +1*x1408 +1*x1409 +1*x1410 +1*x1411 +1*x1412 +1*x98 +1*x1413 +1*x1414 +1*x1382 +1*x1384 +1*x1415 +1*x108 +1*x1416 +1*x1417 +1*x109 +1*x1418 +1*x1394 +1*x1419 +1*x1420 +1*x1421 +1*x1422 +1*x1423 +1*x1424 +1*x1425 +1*x1426 +1*x1427 +1*x1428 +1*x118 +1*x1429 >= +1;
+1*x1430 +1*x1431 +1*x1432 +1*x1433 +1*x26 +1*x1434 +1*x27 +1*x1435 +1*x29 +1*x1323 +1*x1436 +1*x1437 +1*x1438 +1*x1326 +1*x1439 +1*x30 +1*x1440 +1*x1441 +1*x1442 +1*x1443 +1*x1327 +1*x1329 +1*x1331 +1*x1444 +1*x1332 +1*x1333 +1*x1334 +1*x1445 +1*x32 +1*x1446 +1*x1337 +1*x1447 +1*x1448 +1*x1449 +1*x1338 +1*x1450 +1*x1451 +1*x1339 +1*x35 +1*x36 +1*x1452 +1*x1453 +1*x37 +1*x39 +1*x1344 +1*x1454 +1*x42 +1*x1345 +1*x43 +1*x1455 +1*x44 +1*x1349 >= +1;
+1*x1430 +1*x1431 +1*x1432 +1*x1433 +1*x26 +1*x1456 +1*x1435 +1*x29 +1*x374 +1*x1457 +1*x30 +1*x1440 +1*x1442 +1*x401 +1*x1446 +1*x1458 +1*x60 +1*x36 +1*x1459 +1*x1460 +1*x1461 >= +1;
+1*x1462 +1*x1463 +1*x1430 +1*x1464 +1*x1465 +1*x1466 +1*x1433 +1*x1467 +1*x1438 +1*x1326 +1*x46 +1*x48 +1*x1468 +1*x1469 +1*x1441 +1*x1470 +1*x1443 +1*x1332 +1*x720 +1*x1471 +1*x54 +1*x56 +1*x1472 +1*x1337 +1*x1448 +1*x1473 +1*x1474 +1*x1475 +1*x1476 +1*x1477 +1*x1452 +1*x1478 +1*x1479 >= +1;
+1*x1480 +1*x1481 +1*x71 +1*x77 +1*x1433 +1*x1482 +1*x1483 +1*x414 +1*x29 +1*x81 +1*x1484 +1*x1485 +1*x1486 +1*x83 +1*x1487 +1*x1442 +1*x1381 +1*x1382 +1*x1383 +1*x401 +1*x1488 +1*x1446 +1*x1387 +1*x1489 +1*x1490 +1*x1491 +1*x36 +1*x426 +1*x1492 +1*x1493 +1*x1459 +1*x1494 +1*x1460 +1*x1495 +1*x1461 +1*x1496 +1*x1497 +1*x1498 +1*x1499 >= +1;
+1*x1462 +1*x74 +1*x1401 +1*x1500 +1*x76 +1*x1501 +1*x1480 +1*x77 +1*x1466 +1*x1433 +1*x1403 +1*x1406 +1*x79 +1*x1483 +1*x1502 +1*x1409 +1*x1410 +1*x48 +1*x1484 +1*x83 +1*x1469 +1*x108 +1*x56 +1*x1448 +1*x1417 +1*x1503 +1*x1478 >= +1;
+1*x1504 +1*x1505 +1*x1506 +1*x1507 +1*x761 +1*x1508 +1*x1509 +1*x1510 +1*x1322 +1*x1511 +1*x1327 +1*x1330 +1*x1333 +1*x1512 +1*x1513 +1*x1514 +1*x1335 +1*x1336 +1*x1515 +1*x1516 +1*x1517 +1*x1518 +1*x1519 +1*x1347 +1*x1520 +1*x1521 >= +1;
+1*x1504 +1*x1505 +1*x1506 +1*x1507 +1*x761 +1*x1508 +1*x1522 +1*x1523 +1*x1524 +1*x1525 +1*x1322 +1*x1511 +1*x1526 +1*x1527 +1*x537 +1*x1327 +1*x1330 +1*x1333 +1*x1528 +1*x1529 +1*x1530 +1*x1531 +1*x1532 +1*x1515 +1*x1355 +1*x1533 +1*x1534 +1*x1535 +1*x1536 +1*x1537 >= +1;
+1*x1538 +1*x1511 +1*x1539 +1*x1540 +1*x1541 +1*x1514 +1*x1542 +1*x1543 +1*x1515 +1*x1544 +1*x1516 +1*x1545 +1*x1546 +1*x1547 +1*x1548 +1*x1518 +1*x1519 +1*x1549 +1*x1550 +1*x1551 +1*x1552 +1*x1553 +1*x1521 >= +1;
+1*x1538 +1*x1511 +1*x1539 +1*x1540 +1*x1554 +1*x1528 +1*x1542 +1*x1543 +1*x1515 +1*x1555 +1*x1533 +1*x1546 +1*x1556 +1*x1536 >= +1;
+1*x1557 +1*x1405 +1*x1558 +1*x1406 +1*x1559 +1*x1560 +1*x1561 +1*x1413 +1*x1562 +1*x1539 +1*x1563 +1*x1564 +1*x1565 +1*x1566 +1*x1567 +1*x1568 +1*x1569 +1*x1543 +1*x1544 +1*x1516 +1*x1570 +1*x1546 +1*x1519 +1*x1550 +1*x1552 +1*x1571 >= +1;
+1*x1500 +1*x1572 +1*x1573 +1*x826 +1*x1574 +1*x1558 +1*x1406 +1*x1559 +1*x1575 +1*x100 >= +1;
+1*x1500 +1*x1572 +1*x1573 +1*x1576 +1*x1501 +1*x1577 +1*x826 +1*x1574 +1*x79 +1*x257 +1*x1578 +1*x1579 +1*x1580 +1*x1581 +1*x1582 >= +1;
+1*x1583 +1*x1338 +1*x1584 +1*x1585 +1*x1586 +1*x1587 +1*x1588 +1*x1589 +1*x1590 +1*x1591 +1*x1592 +1*x1593 +1*x1594 +1*x1595 +1*x1596 +1*x1217 +1*x1597 +1*x1598 +1*x1599 +1*x1600 +1*x1601 +1*x1602 +1*x1603 +1*x1604 +1*x1605 +1*x1606 +1*x1607 +1*x1608 +1*x1609 +1*x1610 >= +1;
+1*x1583 +1*x1338 +1*x1584 +1*x1585 +1*x1586 +1*x1611 +1*x1587 +1*x1588 +1*x1589 +1*x1590 +1*x1343 +1*x1612 +1*x1344 +1*x1345 +1*x1601 +1*x1346 +1*x1613 +1*x1348 +1*x1614 +1*x1615 >= +1;
+1*x1583 +1*x1586 +1*x1611 +1*x1616 +1*x1617 >= +1;
+1*x1618 +1*x1619 +1*x1620 +1*x1621 +1*x1622 +1*x1623 +1*x1624 +1*x1625 +1*x1420 +1*x1421 +1*x1626 +1*x1627 +1*x1428 +1*x1628 +1*x1629 +1*x1630 >= +1;
+1*x1464 +1*x1631 +1*x1632 +1*x1633 +1*x1634 +1*x1635 +1*x1636 +1*x1637 +1*x1638 +1*x1639 +1*x1640 +1*x1641 +1*x1642 +1*x1643 +1*x1644 +1*x1472 +1*x1645 +1*x1646 +1*x1647 +1*x1648 >= +1;
+1*x1464 +1*x1631 +1*x1632 +1*x1633 +1*x1634 +1*x1635 +1*x1636 +1*x1637 +1*x1638 +1*x1639 +1*x1641 +1*x1642 +1*x1649 +1*x1443 +1*x1643 +1*x1644 +1*x1475 +1*x1650 +1*x1601 +1*x1604 +1*x1651 +1*x1652 >= +1;
+1*x1464 +1*x1631 +1*x1632 +1*x1633 +1*x1634 +1*x1636 +1*x1637 +1*x1640 +1*x1641 +1*x1642 +1*x1443 +1*x1471 +1*x1472 +1*x1473 +1*x1452 +1*x1345 +1*x1601 >= +1;
+1*x1653 +1*x1524 +1*x1654 +1*x1525 +1*x1655 +1*x1656 +1*x1657 +1*x1658 +1*x1659 +1*x1531 +1*x1660 +1*x1533 +1*x1661 +1*x1662 +1*x1663 +1*x1664 >= +1;
+1*x1665 +1*x1666 +1*x1667 +1*x1668 +1*x1669 +1*x1670 +1*x1671 +1*x1672 +1*x1673 +1*x1674 +1*x1675 +1*x1676 +1*x1641 +1*x1642 +1*x1677 +1*x1678 +1*x1679 +1*x1680 +1*x1681 +1*x1564 +1*x1682 +1*x1683 +1*x1684 +1*x1685 +1*x1686 +1*x1687 +1*x1688 +1*x1689 +1*x1570 +1*x1690 +1*x1691 +1*x1692 +1*x1693 +1*x1694 +1*x1695 +1*x500 +1*x1571 >= +1;
+1*x1696 +1*x1697 +1*x1698 +1*x1656 +1*x1699 +1*x1540 +1*x1700 +1*x1701 +1*x1659 +1*x1702 +1*x1703 +1*x1704 +1*x1705 +1*x1545 +1*x1661 +1*x1546 +1*x1549 +1*x1550 +1*x1706 +1*x1551 +1*x1707 +1*x1708 >= +1;
+1*x1655 +1*x1709 +1*x1710 +1*x1711 +1*x1712 +1*x1713 +1*x1714 +1*x1715 +1*x1716 +1*x1717 +1*x1718 +1*x1719 +1*x1720 +1*x1721 +1*x1722 +1*x1723 +1*x1724 +1*x1725 +1*x1726 +1*x1727 +1*x1728 +1*x1729 >= +1;
+1*x1730 +1*x1731 +1*x1668 +1*x1669 +1*x1633 +1*x1732 +1*x1670 +1*x1733 +1*x1638 +1*x1639 +1*x1734 +1*x1641 +1*x1642 +1*x1735 +1*x1710 +1*x1711 +1*x1712 +1*x1660 +1*x1682 +1*x1645 +1*x1646 +1*x1736 +1*x1648 >= +1;
+1*x1730 +1*x1731 +1*x1668 +1*x1669 +1*x1633 +1*x1732 +1*x1670 +1*x1733 +1*x1638 +1*x1639 +1*x213 +1*x214 +1*x1679 +1*x215 +1*x1737 +1*x1738 +1*x1739 +1*x1740 +1*x1741 +1*x1742 +1*x1743 >= +1;
+1*x1744 +1*x1745 +1*x1698 +1*x1746 +1*x1747 +1*x1748 +1*x1714 +1*x1661 +1*x1749 +1*x1750 +1*x1549 +1*x1726 +1*x1751 +1*x1752 +1*x1663 +1*x1753 +1*x1754 +1*x1755 >= +1;
+1*x1756 +1*x1757 +1*x1758 +1*x275 +1*x1759 +1*x1760 +1*x1761 +1*x280 +1*x281 +1*x284 +1*x285 +1*x1762 +1*x317 +1*x397 +1*x1763 +1*x1764 +1*x1765 +1*x1766 >= +1;
+1*x1767 +1*x1768 +1*x1407 +1*x1769 +1*x1770 +1*x1771 +1*x1376 +1*x1772 +1*x1773 +1*x1774 +1*x346 +1*x1775 +1*x1776 +1*x1777 +1*x347 +1*x349 +1*x1778 +1*x350 +1*x1416 +1*x1760 +1*x284 +1*x1387 +1*x1779 +1*x1762 +1*x1780 +1*x1781 +1*x1782 +1*x1783 +1*x1784 +1*x1763 +1*x1785 +1*x1786 >= +1;
+1*x1787 +1*x1788 +1*x1789 +1*x1790 +1*x1791 +1*x1792 +1*x1793 +1*x1794 +1*x1795 +1*x1796 +1*x381 +1*x1644 +1*x392 +1*x59 +1*x1458 +1*x1797 +1*x1798 +1*x60 +1*x61 +1*x1799 +1*x316 +1*x1026 +1*x1779 +1*x1800 +1*x1762 +1*x395 +1*x317 +1*x396 +1*x1780 +1*x1801 +1*x1802 +1*x1803 +1*x1804 +1*x1805 +1*x1027 +1*x725 +1*x1806 +1*x383 +1*x1784 +1*x1459 +1*x1763 +1*x1807 +1*x1461 +1*x1808 +1*x1764 +1*x1785 +1*x1809 +1*x1029 +1*x1810 +1*x1811 +1*x1812 >= +1;
+1*x1813 +1*x1814 +1*x1815 +1*x1816 +1*x1817 +1*x1818 +1*x1819 +1*x1820 +1*x1821 +1*x1822 +1*x1823 +1*x1772 +1*x1824 +1*x1825 +1*x1826 +1*x1827 +1*x1828 +1*x1829 +1*x1830 +1*x1791 +1*x1831 +1*x1832 +1*x1833 +1*x1834 +1*x1835 +1*x1836 +1*x1837 +1*x1838 +1*x1839 +1*x1840 +1*x1841 +1*x1842 +1*x1806 +1*x1782 +1*x1843 +1*x1844 +1*x1845 +1*x1846 +1*x1847 >= +1;
+1*x1813 +1*x1814 +1*x1815 +1*x1816 +1*x1817 +1*x1481 +1*x1819 +1*x1820 +1*x1821 +1*x1822 +1*x1483 +1*x412 +1*x413 +1*x1756 +1*x414 +1*x81 +1*x388 +1*x1848 +1*x1772 +1*x1824 +1*x1757 +1*x389 +1*x1825 +1*x1849 +1*x1826 +1*x1827 +1*x1831 +1*x1442 +1*x275 +1*x1850 +1*x1383 +1*x350 +1*x401 +1*x417 +1*x1832 +1*x278 +1*x1386 +1*x1387 +1*x1851 +1*x1852 +1*x1853 +1*x1854 +1*x1397 +1*x1398 +1*x1399 +1*x304 +1*x1369 >= +1;
+1*x1815 +1*x76 +1*x1855 +1*x1483 +1*x413 +1*x1856 +1*x81 +1*x1772 +1*x1824 +1*x1827 +1*x85 +1*x1791 +1*x349 +1*x350 +1*x1857 +1*x1797 +1*x1798 +1*x1839 +1*x1858 +1*x1579 +1*x1859 +1*x1860 +1*x1853 +1*x358 +1*x1861 +1*x1459 +1*x1494 +1*x1862 +1*x1863 +1*x429 +1*x1864 +1*x1865 +1*x362 +1*x1866 +1*x1867 +1*x1868 +1*x1869 +1*x1870 >= +1;
+1*x1815 +1*x76 +1*x1855 +1*x1871 +1*x1772 +1*x1824 +1*x1827 +1*x85 +1*x1791 +1*x1831 +1*x1773 +1*x1774 +1*x349 +1*x1778 +1*x1857 +1*x1832 +1*x1872 +1*x1873 +1*x1835 +1*x1797 +1*x1798 +1*x61 +1*x1839 +1*x1779 +1*x1800 +1*x1806 +1*x1782 +1*x1784 +1*x1874 +1*x1875 +1*x1876 +1*x1865 +1*x362 +1*x1846 +1*x1877 +1*x1878 >= +1;
+1*x1879 +1*x1880 +1*x1881 +1*x1882 +1*x1883 +1*x1884 +1*x1885 +1*x1886 +1*x1887 +1*x1888 +1*x1889 >= +1;
+1*x1890 +1*x1891 +1*x1892 +1*x1554 +1*x1893 +1*x1894 +1*x1555 +1*x1895 +1*x1393 +1*x1896 +1*x1897 +1*x1556 +1*x1898 +1*x1899 +1*x1900 +1*x1869 +1*x365 >= +1;
+1*x1901 +1*x1902 +1*x1903 +1*x1904 +1*x1905 +1*x1906 +1*x1907 +1*x1440 +1*x1830 +1*x378 +1*x1908 +1*x597 +1*x1460 +1*x1909 >= +1;
+1*x1901 +1*x1902 +1*x1903 +1*x1904 +1*x1910 +1*x1906 +1*x1907 +1*x1440 +1*x1830 +1*x378 +1*x1911 +1*x1912 +1*x1913 +1*x1914 +1*x1915 +1*x1916 +1*x1917 +1*x1918 +1*x1919 +1*x1110 +1*x1155 +1*x1920 +1*x1451 +1*x1838 +1*x382 +1*x1921 +1*x383 +1*x1922 +1*x1923 +1*x1924 +1*x1925 +1*x1926 +1*x1927 +1*x1928 +1*x1845 +1*x1929 +1*x384 +1*x1930 +1*x1931 +1*x1932 >= +1;
+1*x1933 +1*x1879 +1*x1934 +1*x1935 +1*x1915 +1*x1128 +1*x1936 +1*x1937 +1*x1928 +1*x1938 +1*x1939 +1*x1940 >= +1;
+1*x1818 +1*x1903 +1*x1941 +1*x1904 +1*x1823 +1*x1942 +1*x1943 +1*x1944 +1*x1487 +1*x1830 +1*x1893 +1*x1894 +1*x1945 +1*x1946 +1*x1947 +1*x1494 +1*x1862 +1*x1460 +1*x1556 +1*x1898 +1*x1899 +1*x1869 +1*x1948 >= +1;
+1*x1818 +1*x1903 +1*x1941 +1*x1904 +1*x1823 +1*x1949 +1*x1950 +1*x1942 +1*x1148 +1*x1487 +1*x1830 +1*x1913 +1*x1893 +1*x1951 +1*x1952 +1*x1953 +1*x1916 +1*x1954 +1*x1894 +1*x616 +1*x1153 +1*x1946 +1*x1919 +1*x1955 +1*x1155 +1*x1838 +1*x1956 +1*x1957 +1*x1958 +1*x1959 +1*x1960 +1*x1961 +1*x1163 +1*x1492 +1*x1556 +1*x1536 +1*x1962 +1*x1963 +1*x1964 +1*x1965 +1*x1845 +1*x1898 +1*x1899 +1*x1966 +1*x1066 +1*x1169 +1*x1171 +1*x1172 +1*x1967 +1*x1968 +1*x1969 +1*x630 >= +1;
+1*x1818 +1*x1903 +1*x1941 +1*x1904 +1*x1949 +1*x1950 +1*x1942 +1*x1943 +1*x1944 +1*x1830 +1*x1913 +1*x1833 +1*x1919 +1*x1955 +1*x1838 +1*x1970 +1*x1971 +1*x1972 >= +1;
+1*x1973 +1*x1974 +1*x1975 +1*x1976 +1*x471 +1*x1977 +1*x1978 +1*x477 +1*x1979 +1*x479 +1*x1980 +1*x1981 +1*x1982 +1*x1983 +1*x1984 +1*x1985 +1*x1986 +1*x1591 +1*x1593 +1*x1594 +1*x1595 +1*x1217 +1*x1597 +1*x1987 +1*x489 +1*x1988 +1*x1720 +1*x1989 +1*x1990 +1*x1226 >= +1;
+1*x1973 +1*x1974 +1*x1975 +1*x1976 +1*x471 +1*x1977 +1*x1978 +1*x477 +1*x1979 +1*x1991 +1*x1980 +1*x1992 +1*x1993 +1*x1982 +1*x1983 +1*x1994 +1*x1995 +1*x1996 +1*x1997 +1*x1998 +1*x1999 +1*x293 +1*x1852 +1*x2000 +1*x2001 +1*x2002 +1*x300 +1*x1985 +1*x1986 +1*x1591 +1*x1593 +1*x1594 +1*x1595 +1*x1217 +1*x1597 +1*x2003 +1*x2004 +1*x2005 +1*x1598 +1*x1599 +1*x1600 +1*x2006 +1*x1604 +1*x1605 +1*x1606 +1*x1608 +1*x2007 +1*x2008 +1*x1609 >= +1;
+1*x2009 +1*x462 +1*x2010 +1*x2011 +1*x463 +1*x2012 +1*x2013 +1*x1973 +1*x2014 +1*x1634 +1*x312 +1*x2015 +1*x2016 +1*x2017 +1*x2018 +1*x2019 +1*x1676 +1*x1789 +1*x1642 +1*x2020 +1*x2021 +1*x2022 +1*x1975 +1*x1976 +1*x471 +1*x2023 +1*x2024 +1*x1683 +1*x476 +1*x1978 +1*x477 +1*x1991 +1*x1982 +1*x1995 +1*x1996 +1*x1997 +1*x1998 +1*x1999 +1*x293 +1*x2025 +1*x2026 +1*x2027 +1*x2028 +1*x2029 +1*x1591 +1*x1875 +1*x2030 +1*x2003 +1*x2004 +1*x2005 +1*x2031 +1*x2006 +1*x1604 >= +1;
+1*x2032 +1*x2015 +1*x2033 +1*x2034 +1*x2017 +1*x2018 +1*x1411 +1*x2035 +1*x2019 +1*x1975 +1*x2036 +1*x1620 +1*x2023 +1*x2037 +1*x476 +1*x1978 +1*x478 +1*x479 +1*x2038 +1*x1591 +1*x2039 +1*x2040 +1*x2041 +1*x2042 +1*x2043 +1*x2044 +1*x490 +1*x2045 >= +1;
+1*x2032 +1*x2015 +1*x2033 +1*x2034 +1*x2017 +1*x2018 +1*x1411 +1*x2035 +1*x2019 +1*x2046 +1*x2022 +1*x1975 +1*x2047 +1*x2036 +1*x1832 +1*x2048 +1*x1872 +1*x1995 +1*x1996 +1*x2025 +1*x2049 +1*x2038 >= +1;
+1*x2050 +1*x2051 +1*x2052 +1*x1973 +1*x1636 +1*x2053 +1*x2054 +1*x2055 +1*x2056 +1*x2057 +1*x2058 +1*x1643 +1*x2059 +1*x2060 +1*x2061 +1*x1993 +1*x1716 +1*x1645 +1*x1909 +1*x1648 +1*x2062 >= +1;
+1*x2009 +1*x2050 +1*x2063 +1*x2012 +1*x2064 +1*x2065 +1*x1787 +1*x1789 +1*x2022 +1*x1797 +1*x2060 +1*x1839 +1*x1875 +1*x2066 >= +1;
+1*x1815 +1*x2064 +1*x2067 +1*x2065 +1*x2068 +1*x1871 +1*x1856 +1*x2069 +1*x2046 +1*x2022 +1*x1857 +1*x1832 +1*x1872 +1*x2070 +1*x2071 +1*x1995 +1*x2025 +1*x2049 +1*x2072 >= +1;
+1*x2010 +1*x2012 +1*x1667 +1*x1670 +1*x2073 +1*x2074 +1*x2075 +1*x1675 +1*x1676 +1*x2076 +1*x1642 +1*x2020 +1*x1678 +1*x2077 +1*x469 +1*x2078 +1*x2024 +1*x2079 +1*x1682 +1*x1683 +1*x1684 +1*x1685 +1*x496 +1*x1686 +1*x2080 +1*x1690 +1*x2028 +1*x2081 +1*x498 +1*x2082 +1*x1693 +1*x1694 +1*x1695 +1*x499 +1*x500 +1*x1938 +1*x2083 +1*x2084 +1*x1571 +1*x2085 +1*x1939 +1*x2086 >= +1;
+1*x2087 +1*x2088 +1*x2075 +1*x2089 +1*x2079 +1*x2090 >= +1;
+1*x2052 +1*x2091 +1*x2092 +1*x1905 +1*x1709 +1*x1952 +1*x2093 +1*x1711 +1*x2094 +1*x1981 +1*x1984 +1*x2095 +1*x2096 +1*x1713 +1*x2097 +1*x1937 +1*x1716 +1*x2098 +1*x2099 +1*x1965 +1*x1720 +1*x1721 +1*x1722 >= +1;
+1*x2100 +1*x2101 +1*x1949 +1*x1833 +1*x2102 +1*x2103 +1*x2104 +1*x1970 +1*x1963 +1*x1847 >= +1;
+1*x2100 +1*x2105 +1*x2101 +1*x2106 +1*x1949 +1*x1950 +1*x2107 +1*x2108 +1*x1833 +1*x2102 +1*x2109 +1*x2103 +1*x2110 +1*x2111 +1*x1970 +1*x1971 +1*x1972 +1*x2112 +1*x2113 >= +1;
+1*x639 +1*x643 +1*x2106 +1*x2088 +1*x2114 +1*x2115 +1*x242 +1*x2116 +1*x2117 +1*x2107 +1*x1734 +1*x645 +1*x2118 +1*x2108 +1*x614 +1*x2119 +1*x2120 +1*x2121 +1*x2110 +1*x2093 +1*x2122 +1*x2123 +1*x1735 +1*x650 +1*x2124 +1*x2125 +1*x2126 +1*x2127 +1*x2128 +1*x602 +1*x2129 +1*x653 +1*x654 +1*x2130 >= +1;
+1*x639 +1*x643 +1*x2106 +1*x2088 +1*x2114 +1*x2115 +1*x242 +1*x2116 +1*x2118 +1*x2108 +1*x614 +1*x2119 +1*x2131 +1*x2111 +1*x2132 +1*x1967 +1*x1868 +1*x2133 +1*x2134 +1*x2135 >= +1;
+1*x2136 +1*x1324 +1*x2137 +1*x1325 +1*x2138 +1*x2139 +1*x2140 +1*x2141 +1*x2142 +1*x2143 +1*x2144 +1*x2145 +1*x2146 >= +1;
+1*x1436 +1*x1437 +1*x1438 +1*x2147 +1*x694 +1*x2148 +1*x1331 +1*x704 +1*x2149 +1*x695 +1*x1444 +1*x1332 +1*x1333 +1*x1334 +1*x2150 +1*x2151 +1*x2152 +1*x2153 +1*x2154 +1*x2155 +1*x2156 +1*x697 +1*x707 +1*x2157 +1*x1449 +1*x2158 +1*x2159 +1*x2160 +1*x2161 +1*x2162 +1*x2163 +1*x1453 +1*x2164 +1*x700 +1*x2165 +1*x701 +1*x1479 +1*x2166 +1*x2167 +1*x2168 +1*x2169 >= +1;
+1*x2170 +1*x759 +1*x1507 +1*x761 +1*x2171 +1*x2172 +1*x1525 +1*x2173 +1*x2174 +1*x2175 +1*x2176 +1*x2177 +1*x2178 +1*x772 +1*x2179 +1*x2180 +1*x2181 +1*x2182 +1*x2183 +1*x2184 +1*x1517 +1*x1518 +1*x2185 +1*x2186 +1*x2187 +1*x2188 +1*x2189 +1*x2190 +1*x678 +1*x2191 +1*x2192 +1*x2193 +1*x1662 +1*x2194 +1*x1664 >= +1;
+1*x2170 +1*x759 +1*x760 +1*x2171 +1*x2172 +1*x2173 +1*x2174 +1*x2175 +1*x2176 +1*x2177 +1*x2195 +1*x2148 +1*x2196 +1*x2197 +1*x2179 +1*x2198 +1*x2181 +1*x2182 +1*x2183 +1*x2199 +1*x2165 +1*x2200 +1*x2201 +1*x2202 >= +1;
+1*x2177 +1*x2203 +1*x2204 +1*x2181 +1*x2182 +1*x2205 +1*x2183 +1*x2184 +1*x2206 +1*x2207 +1*x1517 +1*x2208 +1*x2186 +1*x2187 +1*x2188 +1*x2209 +1*x1692 +1*x2210 +1*x2189 +1*x2211 +1*x2212 +1*x2190 +1*x2213 +1*x2214 +1*x2215 +1*x2191 +1*x2192 +1*x2193 +1*x1662 +1*x2194 +1*x2216 +1*x2217 +1*x2218 +1*x2219 +1*x2220 +1*x2221 +1*x2222 +1*x2223 >= +1;
+1*x2224 +1*x1575 +1*x2225 +1*x2226 +1*x2227 +1*x2228 +1*x2210 +1*x2211 +1*x2229 +1*x2230 +1*x2190 +1*x2231 +1*x2191 +1*x2192 +1*x2232 >= +1;
+1*x2224 +1*x1575 +1*x2233 +1*x2226 +1*x1415 +1*x111 +1*x2234 +1*x2235 +1*x113 >= +1;
+1*x2236 +1*x2237 +1*x2238 +1*x2203 +1*x2239 +1*x2240 +1*x2241 +1*x2242 +1*x2208 +1*x2210 +1*x2243 +1*x2244 +1*x2245 >= +1;
+1*x2246 +1*x2247 +1*x1572 +1*x825 +1*x790 +1*x826 +1*x796 +1*x2248 +1*x2249 +1*x2250 +1*x803 +1*x2236 +1*x2238 +1*x831 +1*x2251 +1*x2252 +1*x260 >= +1;
+1*x2253 +1*x2254 >= +1;
+1*x2255 +1*x2256 +1*x2257 +1*x2258 +1*x2259 +1*x655 +1*x2260 +1*x2261 +1*x2262 +1*x2263 +1*x2264 +1*x2265 +1*x2266 +1*x2267 +1*x2268 +1*x2269 +1*x2270 +1*x2271 +1*x2272 +1*x2273 >= +1;
+1*x2274 +1*x2275 +1*x2276 +1*x2150 +1*x2151 +1*x2277 +1*x2164 +1*x2169 >= +1;
+1*x2278 +1*x2279 +1*x2280 +1*x870 +1*x871 +1*x873 +1*x2281 +1*x2282 +1*x874 >= +1;
+1*x2283 +1*x2170 +1*x2284 +1*x1653 +1*x2172 +1*x2285 +1*x2286 +1*x1525 +1*x2287 +1*x2288 +1*x1657 +1*x1659 +1*x2267 +1*x2178 +1*x2180 +1*x2289 +1*x2184 +1*x2186 +1*x2188 +1*x2290 +1*x2192 +1*x1662 +1*x1664 >= +1;
+1*x2283 +1*x2170 +1*x2284 +1*x1653 +1*x2172 +1*x2287 +1*x2291 +1*x1659 +1*x2196 +1*x2289 +1*x2292 +1*x1718 +1*x2201 >= +1;
+1*x2285 +1*x1671 +1*x2286 +1*x1657 +1*x1678 +1*x2293 +1*x2294 +1*x2295 +1*x2296 +1*x2297 +1*x1687 +1*x909 +1*x2298 +1*x1689 +1*x2299 +1*x2300 >= +1;
+1*x2291 +1*x2301 +1*x2302 +1*x929 +1*x2303 +1*x2304 +1*x2305 +1*x2306 +1*x933 +1*x934 +1*x2307 +1*x2292 +1*x1718 +1*x1719 +1*x2308 +1*x1720 +1*x1722 +1*x1723 +1*x937 +1*x1729 +1*x940 >= +1;
+1*x2309 +1*x1737 +1*x2241 +1*x2310 +1*x2242 +1*x2294 +1*x1739 +1*x2299 +1*x967 +1*x2211 +1*x2300 +1*x2311 +1*x231 +1*x920 +1*x2312 >= +1;
+1*x2248 +1*x2250 +1*x2313 +1*x2314 +1*x2116 +1*x2315 +1*x2225 +1*x2316 +1*x2317 +1*x2318 +1*x2131 +1*x963 +1*x831 +1*x966 +1*x832 +1*x2319 +1*x249 +1*x910 +1*x260 +1*x251 +1*x2320 +1*x838 >= +1;
+1*x2321 +1*x2322 +1*x2323 +1*x2324 +1*x2325 +1*x2140 +1*x2141 +1*x2326 +1*x2142 +1*x2143 +1*x2327 +1*x996 +1*x1197 +1*x1048 +1*x2328 +1*x2329 +1*x2330 +1*x2331 +1*x1060 +1*x2332 +1*x1061 +1*x2146 +1*x2333 +1*x2334 +1*x1065 +1*x1067 +1*x2335 +1*x2336 +1*x2337 +1*x2338 +1*x2339 +1*x2340 >= +1;
+1*x2341 +1*x2342 +1*x2343 +1*x2344 +1*x2345 +1*x2346 +1*x2347 +1*x2348 +1*x2349 +1*x1770 +1*x2350 +1*x2321 +1*x2322 +1*x2016 +1*x2019 +1*x2351 +1*x2352 +1*x1021 +1*x2353 +1*x2354 +1*x2355 +1*x2143 +1*x2356 +1*x2357 +1*x2358 +1*x2359 +1*x2360 +1*x2361 +1*x1340 +1*x497 +1*x1999 +1*x2328 +1*x1368 +1*x2362 +1*x2363 +1*x2364 +1*x2365 +1*x308 +1*x2366 +1*x2367 +1*x2368 +1*x2369 +1*x2370 >= +1;
+1*x2371 +1*x1828 +1*x338 +1*x2372 +1*x2373 +1*x2374 +1*x2375 +1*x2376 +1*x670 +1*x2377 +1*x1495 +1*x2378 +1*x2379 +1*x680 +1*x2335 +1*x2380 +1*x2381 >= +1;
+1*x2382 +1*x1816 +1*x2383 +1*x1819 +1*x1141 +1*x2384 +1*x2385 +1*x2386 +1*x1482 +1*x1823 +1*x2387 +1*x2371 +1*x1828 +1*x2388 +1*x1487 +1*x1829 +1*x2389 +1*x993 +1*x2390 +1*x806 +1*x1149 +1*x2391 +1*x417 +1*x2372 +1*x2374 +1*x1834 +1*x1945 +1*x2376 +1*x2392 +1*x2156 +1*x2393 +1*x2157 +1*x1837 +1*x1947 +1*x420 +1*x698 +1*x1841 +1*x1842 +1*x1495 +1*x1454 +1*x2378 +1*x2394 +1*x2379 +1*x703 +1*x2395 +1*x680 +1*x2335 +1*x2380 +1*x2381 +1*x2396 +1*x2397 >= +1;
+1*x2398 +1*x2171 +1*x2399 +1*x2172 +1*x2400 +1*x1038 +1*x1040 +1*x2175 +1*x2401 +1*x2402 +1*x2403 +1*x2323 +1*x2324 +1*x2177 +1*x2197 +1*x2198 +1*x1048 +1*x2404 +1*x1058 +1*x2331 +1*x1060 +1*x2185 +1*x2405 +1*x2406 +1*x2407 +1*x2200 +1*x2187 +1*x2188 +1*x2408 +1*x2409 +1*x2410 >= +1;
+1*x2411 +1*x2412 +1*x2413 +1*x1121 +1*x2237 +1*x2238 +1*x2414 +1*x2403 +1*x2415 +1*x1124 +1*x2324 +1*x2203 +1*x2416 +1*x2417 +1*x2240 +1*x2418 +1*x1112 +1*x1113 +1*x2198 +1*x2419 +1*x1025 +1*x2252 +1*x2420 +1*x2421 +1*x2243 +1*x1102 +1*x1010 +1*x1189 >= +1;
+1*x1133 +1*x2246 +1*x788 +1*x2382 +1*x1140 +1*x1141 +1*x796 +1*x2386 +1*x1941 +1*x1823 +1*x2422 +1*x1145 +1*x1146 +1*x1942 +1*x1943 +1*x1487 +1*x806 +1*x1149 +1*x2391 +1*x2423 +1*x1945 +1*x1946 +1*x2424 +1*x1947 +1*x2425 +1*x2426 +1*x954 +1*x2320 +1*x968 +1*x1948 +1*x2396 +1*x2427 >= +1;
+1*x1133 +1*x2246 +1*x788 +1*x2382 +1*x1140 +1*x1141 +1*x796 +1*x2386 +1*x1941 +1*x1823 +1*x2422 +1*x2428 +1*x1145 +1*x1146 +1*x1943 +1*x1148 +1*x2429 +1*x2430 +1*x1913 +1*x806 +1*x1149 +1*x1174 +1*x2423 +1*x2431 +1*x2432 +1*x2424 +1*x2418 +1*x2433 +1*x2419 +1*x2434 +1*x2426 +1*x1178 +1*x2435 +1*x1956 +1*x2436 +1*x2437 +1*x1963 +1*x2438 +1*x1964 +1*x1965 +1*x2439 +1*x2440 +1*x2441 +1*x2442 >= +1;
+1*x2246 +1*x2443 +1*x2413 +1*x1140 +1*x796 +1*x2233 +1*x1181 +1*x1146 +1*x2444 +1*x2445 +1*x2446 +1*x2417 +1*x1578 +1*x2447 +1*x2431 +1*x1093 +1*x1158 +1*x2448 +1*x2449 +1*x2450 +1*x2451 +1*x2452 +1*x2453 +1*x2454 +1*x2455 +1*x1582 >= +1;
+1*x2456 +1*x2457 +1*x2458 +1*x2459 +1*x1241 +1*x1242 +1*x1244 +1*x2460 +1*x1249 +1*x1250 +1*x2461 +1*x1196 +1*x1621 +1*x1201 +1*x1623 +1*x2462 +1*x2463 +1*x2464 >= +1;
+1*x2465 +1*x2466 +1*x2467 +1*x2468 +1*x2069 +1*x1020 +1*x2469 +1*x2470 +1*x2471 +1*x2472 +1*x1799 +1*x2473 +1*x1008 +1*x1801 +1*x2474 +1*x2475 +1*x2476 >= +1;
+1*x2477 +1*x2478 +1*x2479 +1*x2387 +1*x2480 +1*x2371 +1*x2388 +1*x2481 +1*x1149 +1*x2482 +1*x1834 +1*x2483 +1*x519 +1*x2392 +1*x2484 +1*x1837 +1*x2485 +1*x1842 +1*x2486 +1*x2487 +1*x2488 +1*x2489 +1*x2396 +1*x2397 >= +1;
+1*x2477 +1*x2490 +1*x2478 +1*x2479 +1*x2387 +1*x2480 +1*x2491 +1*x2492 +1*x2371 +1*x2388 +1*x2481 +1*x1149 +1*x2493 +1*x2282 +1*x1834 +1*x2494 +1*x1835 +1*x2495 +1*x2483 +1*x2496 +1*x2497 +1*x2498 +1*x2499 +1*x519 +1*x520 +1*x2392 +1*x2484 +1*x874 +1*x2500 +1*x1837 +1*x2485 +1*x1842 +1*x2501 +1*x2502 +1*x2503 +1*x1843 +1*x2504 +1*x2505 +1*x2487 +1*x2506 +1*x2507 +1*x2439 +1*x2508 +1*x999 +1*x2509 +1*x1846 +1*x2510 +1*x2489 +1*x2511 +1*x526 +1*x2512 +1*x2513 +1*x1847 +1*x527 >= +1;
+1*x2477 +1*x2490 +1*x2387 +1*x2480 +1*x2491 +1*x2492 +1*x2371 +1*x2388 +1*x2481 +1*x1149 +1*x2514 +1*x2515 +1*x2485 +1*x2501 +1*x2516 +1*x2517 +1*x2518 +1*x2519 >= +1;
+1*x2520 +1*x2521 +1*x2478 +1*x2522 +1*x2280 +1*x2523 +1*x2524 +1*x2525 +1*x2526 +1*x873 +1*x2527 +1*x2282 +1*x2482 +1*x2528 +1*x2529 +1*x2496 +1*x874 +1*x2530 +1*x2531 +1*x2532 +1*x2488 +1*x2533 +1*x2534 +1*x978 >= +1;
+1*x2520 +1*x2067 +1*x2523 +1*x2535 >= +1;
+1*x2284 +1*x2536 +1*x2399 +1*x2172 +1*x2286 +1*x2537 +1*x2538 +1*x2539 +1*x2402 +1*x2289 +1*x2540 +1*x2188 +1*x2541 >= +1;
+1*x2284 +1*x2536 +1*x2399 +1*x2172 +1*x2286 +1*x1273 +1*x2537 +1*x2538 +1*x2539 +1*x2402 +1*x2542 +1*x1276 +1*x2543 +1*x1277 +1*x1532 +1*x2544 +1*x2097 +1*x2545 +1*x544 +1*x545 +1*x2546 +1*x2099 +1*x2289 +1*x2540 +1*x2547 +1*x2548 +1*x2549 >= +1;
+1*x2284 +1*x2536 +1*x2399 +1*x2172 +1*x2286 +1*x2550 +1*x1273 +1*x2537 +1*x2538 +1*x2539 +1*x1040 +1*x2542 +1*x1276 +1*x2543 +1*x1277 +1*x1532 +1*x1281 +1*x2551 +1*x2295 +1*x2097 +1*x2545 +1*x544 +1*x545 +1*x2552 +1*x1290 +1*x2553 +1*x1292 +1*x1294 +1*x2554 +1*x1295 >= +1;
+1*x2555 +1*x2556 +1*x2557 +1*x2543 +1*x1277 +1*x2558 +1*x2544 +1*x2095 +1*x2097 +1*x2545 +1*x544 +1*x1119 +1*x2098 +1*x2546 +1*x2099 +1*x2547 +1*x2548 +1*x2559 +1*x604 +1*x606 >= +1;
+1*x2555 +1*x2556 +1*x2557 +1*x2543 +1*x1277 +1*x2560 +1*x2561 +1*x2095 +1*x2097 +1*x2545 +1*x544 +1*x2552 +1*x2553 +1*x1294 >= +1;
+1*x2562 +1*x2563 +1*x2564 +1*x2565 +1*x2566 +1*x2567 +1*x2568 +1*x2569 >= +1;
+1*x2570 +1*x2571 +1*x2572 +1*x2573 +1*x2574 +1*x2575 +1*x2576 +1*x2577 +1*x2578 +1*x2579 +1*x2580 +1*x2581 +1*x2582 +1*x8 +1*x2583 +1*x2584 +1*x2585 +1*x2586 +1*x2587 +1*x2588 +1*x2589 +1*x2590 +1*x2591 +1*x2592 +1*x2593 +1*x2594 +1*x2595 +1*x2596 +1*x2597 +1*x2598 +1*x2599 +1*x2600 +1*x2601 +1*x2602 +1*x2603 +1*x152 +1*x2604 +1*x2605 +1*x2606 +1*x2607 +1*x2608 +1*x2609 +1*x2610 +1*x2611 +1*x2612 +1*x2613 +1*x2614 >= +1;
+1*x2570 +1*x2571 +1*x2572 +1*x2574 +1*x2575 +1*x2576 +1*x311 +1*x2584 +1*x2586 +1*x1352 +1*x2590 +1*x2594 +1*x2609 +1*x2615 >= +1;
+1*x2570 +1*x2571 +1*x2572 +1*x2573 +1*x2574 +1*x2575 +1*x2576 +1*x311 +1*x2577 +1*x2578 +1*x2579 +1*x2580 +1*x2581 +1*x2582 +1*x8 +1*x2583 +1*x2584 +1*x2585 +1*x2616 +1*x277 +1*x1352 +1*x2587 +1*x2588 +1*x2589 +1*x2590 +1*x2591 +1*x2592 +1*x2595 +1*x2617 +1*x2618 +1*x2607 +1*x2608 +1*x2619 +1*x505 >= +1;
+1*x2562 +1*x2620 +1*x2621 +1*x2622 +1*x2573 +1*x2623 +1*x2566 +1*x2 +1*x2624 +1*x2625 +1*x2626 +1*x2568 +1*x2627 +1*x5 +1*x7 +1*x8 +1*x2628 +1*x2629 +1*x2630 +1*x11 +1*x2631 +1*x12 +1*x2632 +1*x2616 +1*x13 +1*x2588 +1*x279 +1*x2633 +1*x2634 +1*x2635 +1*x2636 +1*x2637 +1*x1389 +1*x2638 +1*x1391 +1*x1392 +1*x2639 +1*x2640 +1*x2641 +1*x2642 +1*x2643 +1*x2644 +1*x2645 +1*x1400 >= +1;
+1*x2621 +1*x2646 +1*x2647 +1*x2573 +1*x2648 +1*x104 +1*x2624 +1*x2578 +1*x2579 +1*x5 +1*x2649 +1*x1410 +1*x8 +1*x2583 +1*x2650 +1*x2632 +1*x2616 +1*x2651 +1*x2652 +1*x2653 +1*x2654 +1*x109 +1*x740 +1*x2638 +1*x1391 +1*x2655 +1*x2656 +1*x2597 +1*x2657 +1*x2658 +1*x2659 +1*x2660 +1*x2661 >= +1;
+1*x2621 +1*x2646 +1*x2647 +1*x2573 +1*x2648 +1*x104 +1*x2624 +1*x2578 +1*x2579 +1*x2662 +1*x2650 +1*x2630 +1*x2651 +1*x2663 +1*x2652 +1*x2653 +1*x353 +1*x2664 +1*x2596 +1*x2665 +1*x2666 +1*x2655 +1*x2656 +1*x2597 +1*x2657 +1*x146 +1*x2667 +1*x147 +1*x2601 +1*x2602 +1*x2603 +1*x152 +1*x2604 +1*x359 +1*x360 +1*x2668 +1*x2669 +1*x449 +1*x2670 +1*x2671 +1*x2672 >= +1;
+1*x2673 +1*x2674 +1*x27 +1*x2675 +1*x2676 +1*x2677 +1*x2678 +1*x2679 +1*x2680 +1*x375 +1*x2681 +1*x2682 +1*x2683 +1*x2684 +1*x2685 +1*x38 +1*x2686 +1*x2687 +1*x2688 +1*x2689 +1*x2690 +1*x2691 >= +1;
+1*x2673 +1*x2674 +1*x27 +1*x2677 +1*x2680 +1*x2683 +1*x2692 +1*x2693 +1*x2694 +1*x34 +1*x1365 +1*x2688 +1*x2695 +1*x2696 +1*x2697 >= +1;
+1*x74 +1*x2698 +1*x2699 +1*x2646 +1*x2700 +1*x2701 +1*x2648 +1*x78 +1*x2702 +1*x2649 +1*x1410 +1*x2662 +1*x2650 +1*x2703 +1*x740 +1*x2655 +1*x2704 +1*x2705 >= +1;
+1*x74 +1*x2698 +1*x2699 +1*x2646 +1*x78 +1*x2702 +1*x2662 +1*x84 +1*x2650 +1*x2703 +1*x2706 +1*x85 +1*x2663 +1*x91 >= +1;
+1*x74 +1*x2698 +1*x2699 +1*x2646 +1*x2700 +1*x2701 +1*x2648 +1*x2702 +1*x2662 +1*x84 +1*x2650 +1*x2703 +1*x2706 +1*x85 +1*x2707 +1*x2663 +1*x2655 +1*x359 +1*x2708 >= +1;
+1*x2623 +1*x2709 +1*x2710 +1*x2711 +1*x2712 +1*x2713 +1*x2630 +1*x2714 +1*x2715 +1*x2716 >= +1;
+1*x2623 +1*x2709 +1*x2566 +1*x2717 +1*x2627 +1*x2710 +1*x2711 +1*x2718 +1*x2712 +1*x2713 +1*x2719 +1*x2720 +1*x2721 +1*x2722 +1*x2723 +1*x2724 +1*x2725 +1*x2715 +1*x2637 +1*x2641 +1*x2726 +1*x2727 +1*x2728 +1*x2729 +1*x2730 +1*x2731 +1*x2732 +1*x2733 +1*x2734 >= +1;
+1*x2735 +1*x95 +1*x104 +1*x2736 +1*x97 +1*x2737 +1*x2654 +1*x109 +1*x2738 +1*x2739 >= +1;
+1*x2735 +1*x95 +1*x104 +1*x2736 +1*x97 +1*x2710 +1*x2712 +1*x2737 +1*x2630 +1*x2719 +1*x2740 +1*x2652 +1*x2722 +1*x2741 +1*x2724 +1*x2742 +1*x2657 +1*x2743 +1*x443 +1*x110 +1*x2667 +1*x2744 +1*x2601 +1*x2602 +1*x2603 +1*x360 +1*x2668 +1*x2669 +1*x449 +1*x2745 +1*x2746 +1*x2747 +1*x2670 +1*x2748 +1*x2749 +1*x2672 >= +1;
+1*x2750 +1*x2751 +1*x2752 +1*x2753 +1*x2683 +1*x2692 +1*x2754 +1*x2755 +1*x2686 >= +1;
+1*x2756 +1*x2754 +1*x2757 +1*x2758 +1*x2755 +1*x2759 +1*x2760 +1*x2761 +1*x2762 +1*x2763 +1*x2764 +1*x126 +1*x230 +1*x233 >= +1;
+1*x2765 +1*x2766 +1*x2767 +1*x2711 +1*x2768 +1*x2769 +1*x2770 +1*x2771 +1*x2713 +1*x2772 +1*x2773 +1*x2774 +1*x2723 +1*x2775 +1*x2725 +1*x2727 +1*x2731 >= +1;
+1*x2765 +1*x2766 +1*x2767 +1*x2776 +1*x2777 +1*x2768 +1*x2769 +1*x2770 +1*x2771 +1*x2772 +1*x2778 +1*x2779 +1*x2780 +1*x2773 +1*x2781 +1*x2774 >= +1;
+1*x2782 +1*x2577 +1*x2783 +1*x2580 +1*x2585 +1*x2784 +1*x2785 +1*x2587 +1*x2591 +1*x2592 +1*x2786 +1*x2595 +1*x2787 +1*x2597 +1*x150 +1*x2598 +1*x2601 +1*x152 +1*x2605 +1*x2607 +1*x2608 +1*x2788 +1*x2789 +1*x2610 +1*x2611 +1*x2790 +1*x2791 +1*x2792 +1*x2793 +1*x2613 >= +1;
+1*x2782 +1*x2577 +1*x2585 +1*x2784 +1*x2794 +1*x2786 +1*x2795 +1*x2787 +1*x2796 +1*x2597 +1*x2797 +1*x2798 +1*x2799 +1*x2800 +1*x2801 >= +1;
+1*x2802 +1*x2784 +1*x2652 +1*x140 +1*x2597 +1*x146 +1*x150 +1*x2601 +1*x152 >= +1;
+1*x2802 +1*x2803 +1*x2784 +1*x2804 +1*x2652 +1*x140 +1*x2655 +1*x2656 +1*x2805 +1*x145 +1*x146 +1*x2667 +1*x147 +1*x153 +1*x2806 +1*x2807 +1*x2808 +1*x2809 +1*x2810 +1*x2705 +1*x2811 >= +1;
+1*x2812 +1*x2813 +1*x2814 +1*x2815 +1*x2676 +1*x2816 +1*x2817 +1*x2818 +1*x2819 +1*x2820 +1*x2821 +1*x2682 +1*x2822 +1*x2823 +1*x2824 +1*x2825 +1*x2796 +1*x2826 +1*x2827 +1*x2828 +1*x2829 +1*x2830 +1*x1650 +1*x38 +1*x1590 +1*x39 +1*x2687 +1*x2689 +1*x2799 +1*x2800 +1*x2831 +1*x2832 +1*x2833 +1*x2834 +1*x2835 +1*x2836 >= +1;
+1*x2700 +1*x2837 +1*x2838 +1*x2839 +1*x2803 +1*x2840 +1*x2841 +1*x2704 +1*x164 +1*x253 +1*x2807 +1*x2842 >= +1;
+1*x2700 +1*x2701 +1*x2837 +1*x2838 +1*x2843 +1*x2839 +1*x2844 +1*x2845 +1*x2846 +1*x2847 +1*x2848 +1*x2849 >= +1;
+1*x2700 +1*x2701 +1*x2837 +1*x2844 +1*x2840 +1*x2845 +1*x2841 +1*x2850 +1*x2851 +1*x2852 >= +1;
+1*x2853 +1*x2854 +1*x2855 +1*x2856 +1*x2857 +1*x2858 +1*x2859 +1*x2860 +1*x2861 +1*x2862 +1*x2863 +1*x2864 +1*x2786 +1*x2865 +1*x2866 +1*x2829 +1*x2867 +1*x2789 +1*x2868 +1*x2869 +1*x2870 +1*x2871 >= +1;
+1*x2872 +1*x2873 +1*x2874 +1*x2859 +1*x2784 +1*x2860 +1*x2786 +1*x2865 +1*x2741 +1*x2875 +1*x2876 +1*x2877 +1*x2878 +1*x2598 +1*x2601 +1*x2605 +1*x2879 +1*x2788 +1*x2880 +1*x2881 +1*x2789 +1*x2882 +1*x2610 +1*x2611 +1*x2883 +1*x2884 +1*x2885 +1*x2886 +1*x2868 +1*x2790 +1*x2869 +1*x2870 +1*x2887 +1*x2888 +1*x2791 +1*x2792 +1*x2793 +1*x2889 >= +1;
+1*x2872 +1*x2873 +1*x2890 >= +1;
+1*x2891 +1*x2892 +1*x2857 +1*x2893 +1*x2894 +1*x2858 +1*x2859 +1*x2895 +1*x2712 +1*x2713 +1*x2896 +1*x567 +1*x2724 +1*x2725 +1*x2897 +1*x2898 +1*x2805 +1*x2899 +1*x2667 +1*x2900 +1*x2668 +1*x2901 +1*x2902 +1*x2903 +1*x2904 +1*x2905 +1*x2906 +1*x2907 +1*x2908 +1*x576 +1*x2909 +1*x2910 +1*x579 +1*x2911 >= +1;
+1*x2912 +1*x2735 +1*x2913 +1*x2872 +1*x2914 +1*x2891 +1*x2915 +1*x2892 +1*x2802 +1*x2859 +1*x2784 +1*x2712 +1*x2916 +1*x2860 +1*x2652 +1*x2741 +1*x2917 +1*x2738 +1*x2918 +1*x2919 +1*x2920 +1*x2921 +1*x2601 +1*x2879 +1*x2882 +1*x2869 +1*x2887 >= +1;
+1*x2912 +1*x2735 +1*x2913 +1*x2872 +1*x2914 +1*x2891 +1*x2915 +1*x2892 +1*x2802 +1*x2803 +1*x2859 +1*x2784 +1*x2712 +1*x2740 +1*x2652 +1*x2922 +1*x2795 +1*x2741 +1*x2724 +1*x2805 +1*x2667 +1*x2601 +1*x2668 +1*x2672 >= +1;
+1*x2923 +1*x2924 +1*x2856 +1*x2816 +1*x2925 +1*x2926 +1*x2927 +1*x2928 +1*x2929 +1*x2930 +1*x2931 +1*x2772 +1*x2932 +1*x2860 +1*x2862 +1*x2933 +1*x2829 +1*x2934 +1*x2867 +1*x2935 +1*x2936 +1*x2689 +1*x2690 >= +1;
+1*x2923 +1*x2937 +1*x2924 +1*x2856 +1*x2816 +1*x2929 +1*x2938 +1*x2930 +1*x2939 +1*x2829 +1*x2830 +1*x2940 +1*x2941 +1*x2942 >= +1;
+1*x2943 +1*x2944 +1*x2945 +1*x2946 +1*x2947 +1*x2766 +1*x2948 +1*x2949 +1*x2892 +1*x2950 +1*x2925 +1*x2927 +1*x2928 +1*x2895 +1*x2771 +1*x2713 +1*x2896 +1*x2931 +1*x2772 +1*x2932 +1*x2860 +1*x2951 +1*x2952 +1*x2953 +1*x2920 +1*x2954 +1*x2955 +1*x2956 +1*x2921 +1*x2867 +1*x2935 +1*x2716 +1*x2936 +1*x2957 >= +1;
+1*x2943 +1*x2944 +1*x2946 +1*x2947 +1*x2766 +1*x2948 +1*x2949 +1*x2892 +1*x2925 +1*x2958 +1*x2928 +1*x2895 +1*x2771 +1*x2713 +1*x2896 +1*x2931 +1*x2772 +1*x2860 +1*x2959 +1*x245 +1*x2773 +1*x2960 +1*x246 +1*x2774 +1*x2725 +1*x2961 +1*x2920 +1*x2954 +1*x2962 +1*x2921 +1*x952 +1*x2727 +1*x2963 +1*x975 >= +1;
+1*x2943 +1*x2944 +1*x2945 +1*x2946 +1*x2766 +1*x2948 +1*x2892 +1*x2925 +1*x2958 +1*x2927 +1*x2895 +1*x2771 +1*x2931 +1*x2772 +1*x2932 +1*x2860 +1*x2959 +1*x2964 +1*x2780 +1*x245 +1*x2773 +1*x2960 +1*x2781 +1*x246 +1*x2774 +1*x2965 +1*x2961 +1*x2966 +1*x2920 +1*x2967 +1*x2968 >= +1;
+1*x2581 +1*x2969 +1*x2678 +1*x2970 +1*x2971 +1*x2972 +1*x2631 +1*x2616 +1*x277 +1*x13 +1*x2973 +1*x2974 +1*x278 +1*x2975 +1*x286 +1*x294 +1*x298 +1*x2976 +1*x2977 +1*x2978 +1*x2979 +1*x318 +1*x2980 +1*x319 +1*x2981 +1*x2982 +1*x2983 +1*x2008 >= +1;
+1*x2984 +1*x2985 +1*x2575 +1*x2986 +1*x311 +1*x2578 +1*x2581 +1*x2969 +1*x2987 +1*x2582 +1*x2583 +1*x2988 +1*x2989 +1*x2990 +1*x2971 +1*x2616 +1*x277 +1*x2587 +1*x2589 +1*x2973 +1*x279 +1*x2991 +1*x2664 +1*x480 +1*x2992 +1*x287 +1*x2993 +1*x2994 +1*x294 +1*x2995 +1*x2996 +1*x2997 +1*x482 +1*x2998 +1*x2999 +1*x3000 +1*x1088 +1*x3001 +1*x3002 +1*x2370 >= +1;
+1*x3003 +1*x2647 +1*x2985 +1*x3004 +1*x2624 +1*x3005 +1*x2578 +1*x3006 +1*x2987 +1*x2583 +1*x344 +1*x2971 +1*x2616 +1*x2973 +1*x279 +1*x3007 +1*x2991 +1*x353 +1*x2664 +1*x2638 +1*x356 +1*x3008 +1*x2999 +1*x3009 +1*x3010 +1*x3000 >= +1;
+1*x3011 +1*x3012 +1*x370 +1*x3013 +1*x373 +1*x389 +1*x2675 +1*x2678 +1*x2970 +1*x2679 +1*x375 +1*x2972 +1*x2974 +1*x278 +1*x3014 +1*x391 +1*x392 +1*x286 +1*x298 +1*x2979 +1*x318 +1*x319 >= +1;
+1*x3015 +1*x3013 +1*x389 +1*x3016 +1*x3017 +1*x3018 +1*x3019 +1*x3020 +1*x3021 +1*x1863 +1*x3022 +1*x3023 +1*x3024 +1*x1867 >= +1;
+1*x3015 +1*x3013 +1*x3025 +1*x3026 +1*x389 +1*x1850 +1*x2972 +1*x2974 +1*x278 >= +1;
+1*x2702 +1*x3027 +1*x2662 +1*x3028 +1*x84 +1*x3018 +1*x3029 +1*x3030 +1*x3031 +1*x3032 +1*x3033 +1*x3034 >= +1;
+1*x3035 +1*x3036 +1*x2984 +1*x3037 +1*x3038 +1*x3039 +1*x2986 +1*x3040 +1*x3041 +1*x2874 +1*x3042 +1*x3043 +1*x3044 +1*x3045 +1*x3046 +1*x2754 +1*x2757 +1*x2758 +1*x2992 +1*x441 +1*x3047 +1*x2744 +1*x2599 +1*x445 +1*x3048 +1*x2761 +1*x2610 +1*x3049 +1*x3050 +1*x3051 +1*x2733 >= +1;
+1*x3035 +1*x3052 +1*x3036 +1*x2984 +1*x3053 +1*x3037 +1*x3038 +1*x3039 +1*x3054 +1*x3055 +1*x2986 +1*x3056 +1*x3057 +1*x3058 +1*x3041 +1*x3059 +1*x2988 +1*x1072 +1*x3060 +1*x1076 +1*x3061 +1*x3062 +1*x482 +1*x3063 >= +1;
+1*x3035 +1*x3052 +1*x3036 +1*x3037 +1*x3038 +1*x3039 +1*x3054 +1*x3055 +1*x3040 +1*x3064 +1*x3041 +1*x2874 +1*x1072 +1*x3060 +1*x1076 +1*x3042 +1*x3065 +1*x3066 +1*x3043 +1*x3044 +1*x3067 +1*x3068 +1*x2754 +1*x2757 +1*x3069 +1*x548 +1*x441 +1*x3070 +1*x2761 +1*x3050 +1*x3071 +1*x3072 +1*x3073 +1*x3074 +1*x3075 +1*x2086 >= +1;
+1*x3076 +1*x3077 +1*x2720 +1*x3078 +1*x2721 +1*x3079 +1*x3080 +1*x1059 +1*x626 +1*x1166 +1*x2728 +1*x2729 +1*x3081 +1*x3082 +1*x628 +1*x3083 +1*x3084 +1*x3085 >= +1;
+1*x3076 +1*x3077 +1*x2720 +1*x3078 +1*x2721 +1*x3086 +1*x3087 +1*x2637 +1*x3079 +1*x2641 +1*x3088 >= +1;
+1*x3037 +1*x3038 +1*x3089 +1*x3090 +1*x3056 +1*x3057 +1*x3041 +1*x3059 +1*x3091 +1*x3092 +1*x3093 +1*x3094 +1*x3061 +1*x3095 +1*x3096 +1*x1130 +1*x3062 +1*x3097 +1*x3098 +1*x3099 +1*x3100 +1*x3101 +1*x1028 +1*x3102 +1*x3063 +1*x3103 >= +1;
+1*x3104 +1*x1147 +1*x3105 +1*x615 +1*x3106 +1*x618 +1*x3107 +1*x3080 +1*x3108 +1*x626 +1*x1166 +1*x3109 +1*x3083 +1*x3110 +1*x3111 >= +1;
+1*x3112 +1*x3113 +1*x3114 +1*x3115 +1*x3095 +1*x3116 +1*x3096 +1*x3117 +1*x3047 +1*x442 +1*x3118 +1*x3119 +1*x3099 +1*x3120 +1*x3121 +1*x445 +1*x3122 +1*x446 +1*x3123 +1*x3124 +1*x3125 >= +1;
+1*x3126 +1*x3127 +1*x3128 +1*x3129 +1*x3130 +1*x3131 +1*x3132 +1*x3133 +1*x3134 +1*x3135 +1*x3136 +1*x3137 +1*x2864 +1*x2975 +1*x3138 +1*x3139 +1*x3140 +1*x3141 +1*x2595 +1*x3142 +1*x2977 +1*x2978 +1*x3143 +1*x3144 +1*x3145 +1*x3048 +1*x3146 +1*x3147 +1*x3148 +1*x3149 +1*x3150 +1*x3151 +1*x3152 +1*x2685 +1*x3153 +1*x2619 +1*x3154 +1*x3155 +1*x3156 +1*x3157 +1*x3158 +1*x3159 +1*x2942 +1*x3160 +1*x3161 >= +1;
+1*x3162 +1*x3163 +1*x3164 +1*x3165 +1*x3166 +1*x3132 +1*x3167 +1*x3168 +1*x3169 +1*x521 +1*x3170 +1*x3138 +1*x3141 +1*x3171 +1*x3172 +1*x2636 +1*x3173 +1*x3174 +1*x2640 +1*x3175 +1*x332 +1*x487 +1*x2042 +1*x1987 +1*x2806 +1*x3176 >= +1;
+1*x3173 +1*x3177 +1*x2999 +1*x3010 +1*x3178 >= +1;
+1*x3179 +1*x3180 +1*x3181 +1*x3128 +1*x3133 +1*x3182 +1*x3019 +1*x3183 +1*x3184 +1*x3185 +1*x3142 +1*x2684 +1*x3144 +1*x2685 +1*x3186 +1*x3187 +1*x3024 +1*x3188 +1*x3189 +1*x2691 >= +1;
+1*x3179 +1*x3190 +1*x3191 +1*x3181 +1*x3192 +1*x3128 +1*x3130 +1*x3193 +1*x3133 +1*x3135 +1*x3141 +1*x3194 +1*x3185 +1*x3195 +1*x3196 +1*x3143 +1*x3176 >= +1;
+1*x3197 +1*x3198 +1*x2840 +1*x3199 +1*x3200 +1*x3201 +1*x3202 +1*x3203 +1*x3204 +1*x3205 +1*x2851 +1*x3206 >= +1;
+1*x3197 +1*x3198 +1*x3207 +1*x3199 +1*x3200 +1*x3208 +1*x3185 +1*x3201 +1*x3202 +1*x3209 +1*x2070 +1*x3203 +1*x3204 +1*x3210 +1*x3211 +1*x524 +1*x3212 +1*x3213 +1*x3214 +1*x3215 +1*x3216 +1*x1864 +1*x3217 +1*x3218 +1*x3219 +1*x3220 +1*x3221 >= +1;
+1*x3197 +1*x3198 +1*x3207 +1*x2840 +1*x3201 +1*x3202 +1*x3209 +1*x2070 +1*x3177 +1*x2841 +1*x2851 +1*x3222 +1*x2852 +1*x3178 >= +1;
+1*x3223 +1*x3224 +1*x3036 +1*x3225 +1*x3226 +1*x3227 +1*x3040 +1*x2855 +1*x3228 +1*x3229 +1*x3129 +1*x3130 +1*x3131 +1*x2858 +1*x3134 +1*x3135 +1*x2939 +1*x3077 +1*x2865 +1*x3046 +1*x3138 +1*x2758 +1*x3230 +1*x3231 +1*x3080 +1*x2963 +1*x2728 +1*x3081 >= +1;
+1*x3035 +1*x3223 +1*x3036 +1*x3232 +1*x3053 +1*x3233 +1*x3234 +1*x2986 +1*x3058 +1*x3235 +1*x3236 +1*x470 +1*x3060 +1*x547 +1*x548 +1*x2997 +1*x482 >= +1;
+1*x3237 +1*x3225 +1*x3226 +1*x3238 +1*x3239 +1*x3227 +1*x3190 +1*x3040 +1*x580 +1*x531 +1*x3240 +1*x2937 +1*x2958 +1*x3241 +1*x3242 +1*x3192 +1*x3130 +1*x3243 +1*x3193 +1*x3244 +1*x2938 +1*x3135 +1*x3245 +1*x457 +1*x2939 +1*x585 +1*x594 +1*x3246 +1*x3247 +1*x3141 +1*x2961 +1*x3195 +1*x2758 +1*x3196 +1*x3248 +1*x3149 +1*x3214 +1*x2963 +1*x2764 >= +1;
+1*x3249 +1*x3237 +1*x3250 +1*x3251 +1*x3225 +1*x2943 +1*x2945 +1*x3252 +1*x557 +1*x3253 +1*x607 +1*x534 +1*x3254 +1*x608 +1*x3255 +1*x2950 +1*x2958 +1*x631 +1*x3256 +1*x3257 +1*x2964 +1*x3258 +1*x3259 +1*x612 +1*x3260 +1*x632 +1*x619 +1*x3261 +1*x634 +1*x636 +1*x3262 +1*x637 >= +1;
+1*x3253 +1*x2948 +1*x3198 +1*x3263 +1*x3243 +1*x3264 +1*x243 +1*x3265 +1*x3256 +1*x617 +1*x3266 +1*x2965 +1*x247 +1*x3200 +1*x3202 +1*x3204 +1*x3210 +1*x623 +1*x3212 +1*x3214 +1*x3215 +1*x3217 >= +1;
+1*x2565 +1*x3267 +1*x2567 +1*x2568 +1*x3268 +1*x3269 +1*x3270 +1*x3271 +1*x3272 +1*x3273 +1*x3274 +1*x3275 +1*x3276 +1*x3277 +1*x3278 +1*x3279 +1*x3280 +1*x2145 +1*x2146 +1*x3281 >= +1;
+1*x3282 +1*x3283 +1*x705 +1*x2693 +1*x2823 +1*x3276 +1*x3277 +1*x3278 +1*x3284 +1*x2694 +1*x34 +1*x3285 +1*x3286 +1*x3287 +1*x35 +1*x3288 +1*x3280 +1*x709 +1*x3289 +1*x3290 +1*x3291 +1*x3292 +1*x711 +1*x3293 >= +1;
+1*x3294 +1*x3295 +1*x719 +1*x3296 +1*x3297 +1*x3298 +1*x3299 +1*x3300 +1*x3301 +1*x3302 +1*x726 +1*x3303 +1*x3304 >= +1;
+1*x2699 +1*x3305 +1*x3306 +1*x734 +1*x748 +1*x3307 +1*x750 +1*x3308 +1*x2706 +1*x3309 +1*x3296 +1*x3310 +1*x3311 +1*x3298 +1*x3312 +1*x737 +1*x3313 +1*x3314 +1*x3301 +1*x3288 +1*x3302 +1*x726 +1*x3315 +1*x709 +1*x754 +1*x3304 +1*x3316 +1*x732 >= +1;
+1*x3317 +1*x3318 +1*x3319 +1*x3320 +1*x3321 +1*x3322 +1*x3323 +1*x3324 +1*x3325 +1*x3067 +1*x3326 +1*x2875 +1*x3327 +1*x3328 +1*x3329 +1*x2881 +1*x3330 >= +1;
+1*x3317 +1*x3318 +1*x3319 +1*x3320 +1*x3321 +1*x3322 +1*x3331 +1*x3332 +1*x3323 +1*x3324 +1*x3333 +1*x3334 +1*x3335 >= +1;
+1*x3336 +1*x765 +1*x766 +1*x3337 +1*x769 +1*x3338 +1*x3339 +1*x3340 >= +1;
+1*x3341 +1*x3331 +1*x3332 +1*x2737 +1*x3342 +1*x3343 +1*x2719 +1*x2740 +1*x3344 +1*x3345 +1*x3346 +1*x3347 +1*x3348 +1*x2669 +1*x2745 +1*x2747 +1*x2670 +1*x2672 >= +1;
+1*x3349 +1*x3350 +1*x3351 +1*x3352 +1*x3297 +1*x3353 +1*x3300 +1*x2759 +1*x3302 +1*x3303 +1*x2760 +1*x3354 +1*x3355 +1*x3356 +1*x3357 >= +1;
+1*x766 +1*x792 +1*x3358 +1*x2776 +1*x781 +1*x3359 +1*x801 +1*x2777 +1*x3360 +1*x807 +1*x808 +1*x1154 +1*x773 +1*x3361 +1*x783 +1*x1177 +1*x3362 +1*x3363 +1*x3364 +1*x3365 +1*x3366 >= +1;
+1*x748 +1*x827 +1*x3367 +1*x809 +1*x829 +1*x811 +1*x752 +1*x3368 >= +1;
+1*x3369 +1*x3370 +1*x3371 +1*x2787 +1*x3372 +1*x3373 +1*x3374 +1*x2611 +1*x3375 +1*x3376 +1*x3377 +1*x3378 +1*x2792 +1*x2613 >= +1;
+1*x3369 +1*x3379 +1*x860 +1*x3371 +1*x3380 +1*x2787 +1*x861 +1*x862 +1*x3373 +1*x3381 +1*x3374 +1*x3382 +1*x2611 +1*x3383 +1*x3384 +1*x3385 +1*x2798 +1*x3386 +1*x3387 +1*x3388 +1*x3389 +1*x3390 +1*x3391 +1*x3392 >= +1;
+1*x3393 +1*x3394 +1*x3395 +1*x3396 +1*x3379 +1*x3397 +1*x3344 +1*x3398 +1*x3399 +1*x3400 +1*x3380 +1*x3401 +1*x3402 +1*x3381 +1*x3403 +1*x3382 +1*x3354 +1*x3404 +1*x3405 +1*x3406 +1*x3407 >= +1;
+1*x3393 +1*x3394 +1*x3408 +1*x3409 +1*x3410 +1*x3398 +1*x3411 +1*x3412 >= +1;
+1*x3413 +1*x3414 +1*x3415 +1*x3416 +1*x3417 +1*x3418 +1*x3419 +1*x3420 +1*x3421 +1*x3283 +1*x3422 +1*x3423 +1*x3424 +1*x3425 +1*x3426 +1*x3427 +1*x3428 +1*x3280 +1*x3429 +1*x3430 +1*x3431 +1*x3432 >= +1;
+1*x3433 +1*x3434 +1*x3435 +1*x3436 +1*x3370 +1*x3437 +1*x3438 +1*x3439 +1*x3440 +1*x3441 +1*x3376 >= +1;
+1*x3442 +1*x3443 +1*x3444 +1*x3445 +1*x3446 +1*x3447 +1*x3448 +1*x3449 +1*x3406 >= +1;
+1*x3337 +1*x769 +1*x3450 +1*x3444 +1*x3451 +1*x3452 +1*x2866 +1*x3453 +1*x2919 >= +1;
+1*x3454 +1*x3418 +1*x3455 +1*x3456 +1*x3457 +1*x3419 +1*x2926 +1*x3458 +1*x3241 +1*x2928 +1*x3421 +1*x3245 +1*x3459 +1*x2862 +1*x3460 +1*x3461 +1*x3462 +1*x3259 +1*x926 +1*x3423 +1*x927 +1*x928 +1*x930 +1*x2933 +1*x2962 +1*x2824 +1*x3424 +1*x3463 +1*x2867 +1*x2935 +1*x3464 +1*x3465 +1*x3466 +1*x3467 +1*x3468 >= +1;
+1*x3454 +1*x3418 +1*x3455 +1*x3469 +1*x2926 +1*x3458 +1*x3241 +1*x3421 +1*x3245 +1*x2862 +1*x926 +1*x3423 +1*x927 +1*x930 +1*x2824 +1*x935 +1*x3470 +1*x3465 +1*x3471 +1*x2831 +1*x2833 +1*x590 >= +1;
+1*x3454 +1*x3418 +1*x3455 +1*x3469 +1*x3456 +1*x3457 +1*x3419 +1*x3421 +1*x3459 +1*x926 +1*x3423 +1*x927 +1*x928 +1*x3472 +1*x3473 >= +1;
+1*x3474 +1*x3475 +1*x3476 +1*x3458 +1*x3477 +1*x3478 +1*x971 +1*x3245 +1*x3350 +1*x3351 +1*x3479 +1*x3460 +1*x3480 +1*x930 +1*x2962 +1*x3481 +1*x935 +1*x936 +1*x3482 >= +1;
+1*x3483 +1*x3484 +1*x2947 +1*x3485 +1*x2949 +1*x3456 +1*x3419 +1*x3486 +1*x942 +1*x943 +1*x3487 +1*x944 +1*x2950 +1*x3488 +1*x945 +1*x2928 +1*x878 +1*x881 +1*x3460 +1*x3461 +1*x3462 +1*x3489 +1*x3259 +1*x3490 +1*x3491 +1*x3492 +1*x2952 +1*x2953 +1*x3493 +1*x2954 +1*x2962 +1*x2955 +1*x2956 +1*x2921 +1*x952 +1*x3494 +1*x936 +1*x975 +1*x3495 +1*x3496 +1*x3430 +1*x3497 +1*x939 +1*x3498 +1*x3499 +1*x3500 +1*x3501 >= +1;
+1*x3502 +1*x3503 +1*x3483 +1*x3504 +1*x3505 +1*x3506 +1*x2915 +1*x2949 +1*x3492 +1*x2953 >= +1;
+1*x3507 +1*x3508 +1*x3509 +1*x2976 +1*x2981 +1*x2982 >= +1;
+1*x3510 +1*x3507 +1*x3508 +1*x3511 +1*x3512 +1*x3513 +1*x3269 +1*x1039 +1*x3270 +1*x1041 +1*x3514 +1*x3509 +1*x3272 +1*x3273 +1*x3515 +1*x3516 +1*x1204 +1*x3517 +1*x3518 +1*x3519 +1*x2330 +1*x3520 +1*x1211 +1*x3521 +1*x3522 +1*x3523 +1*x3524 +1*x3525 +1*x3526 >= +1;
+1*x3527 +1*x3528 +1*x2989 +1*x3529 +1*x2990 +1*x3530 +1*x3509 +1*x3531 +1*x3532 +1*x2993 +1*x2995 +1*x3533 +1*x3534 +1*x2982 +1*x3535 >= +1;
+1*x3527 +1*x3528 +1*x2989 +1*x3529 +1*x2990 +1*x3530 +1*x3509 +1*x3272 +1*x3515 +1*x3531 +1*x3536 +1*x3537 +1*x3538 +1*x3539 +1*x3532 +1*x3540 +1*x3541 +1*x2991 +1*x1236 +1*x3542 +1*x3517 +1*x3328 +1*x3518 +1*x3519 +1*x3543 +1*x3348 +1*x3533 +1*x3544 +1*x3545 +1*x3546 +1*x2669 +1*x1030 +1*x2998 +1*x2362 +1*x3547 +1*x3548 +1*x3549 +1*x3550 +1*x3551 +1*x1032 +1*x1033 +1*x3552 >= +1;
+1*x3527 +1*x3528 +1*x2989 +1*x3529 +1*x2990 +1*x3530 +1*x3531 +1*x3536 +1*x3537 +1*x3538 +1*x3539 +1*x3532 +1*x3540 +1*x3541 +1*x2991 +1*x1236 +1*x3542 +1*x2993 +1*x2995 +1*x2996 +1*x2997 +1*x1030 +1*x2998 +1*x2362 +1*x1083 +1*x3534 +1*x3553 +1*x1087 +1*x3000 +1*x3554 +1*x3555 +1*x3556 +1*x2369 +1*x1088 +1*x3002 +1*x2370 >= +1;
+1*x3510 +1*x3557 +1*x3558 +1*x3559 +1*x3560 +1*x3561 +1*x2373 +1*x3562 +1*x3563 +1*x3516 +1*x3564 +1*x3565 >= +1;
+1*x3566 +1*x3560 +1*x3005 +1*x3567 +1*x3308 +1*x3568 +1*x3569 +1*x3345 +1*x3570 +1*x3571 +1*x3515 +1*x3346 +1*x2663 +1*x3536 +1*x3538 +1*x3539 +1*x3572 +1*x3519 +1*x3573 +1*x3574 +1*x2666 +1*x3543 +1*x3348 +1*x3575 +1*x3576 >= +1;
+1*x3577 +1*x3578 +1*x1013 +1*x3579 +1*x3092 +1*x1022 +1*x723 >= +1;
+1*x3580 +1*x3581 +1*x3582 +1*x3310 +1*x3583 +1*x3584 +1*x3585 +1*x3572 +1*x3586 +1*x3587 +1*x3588 +1*x1164 +1*x3589 +1*x754 +1*x3590 +1*x3591 >= +1;
+1*x3581 +1*x3592 +1*x3593 +1*x3582 +1*x3310 +1*x3583 +1*x3594 +1*x3595 +1*x3596 +1*x3586 +1*x3597 +1*x3587 +1*x3598 +1*x3599 +1*x3600 >= +1;
+1*x3580 +1*x3601 +1*x3581 +1*x3592 +1*x3593 +1*x3582 +1*x3310 +1*x3602 +1*x3572 +1*x3573 +1*x3574 +1*x3603 +1*x3586 +1*x3597 +1*x3587 +1*x3588 +1*x1164 +1*x3589 +1*x1165 +1*x3604 +1*x1167 +1*x818 +1*x754 +1*x3576 +1*x755 +1*x823 +1*x3605 +1*x3599 +1*x3606 +1*x3607 +1*x3608 >= +1;
+1*x3580 +1*x3601 +1*x3581 +1*x3592 +1*x3593 +1*x3582 +1*x3310 +1*x3602 +1*x3583 +1*x3594 +1*x3595 +1*x3584 +1*x3585 +1*x3609 +1*x3610 +1*x3572 +1*x3573 +1*x3574 +1*x3596 +1*x3605 +1*x3598 +1*x3590 +1*x3611 +1*x3612 +1*x3613 +1*x3614 +1*x3615 +1*x3616 +1*x3617 >= +1;
+1*x3618 +1*x3619 +1*x3620 +1*x3510 +1*x3621 +1*x1034 +1*x1035 +1*x3622 +1*x3623 +1*x3624 +1*x3625 +1*x1042 +1*x3514 +1*x3626 +1*x1075 +1*x3627 +1*x3628 +1*x3629 +1*x1082 +1*x3630 +1*x3631 +1*x3632 +1*x3565 +1*x3633 +1*x3634 +1*x3635 >= +1;
+1*x3618 +1*x3619 +1*x3620 +1*x3510 +1*x3636 +1*x3054 +1*x3621 +1*x3637 +1*x1034 +1*x1035 +1*x3622 +1*x3058 +1*x1037 +1*x3623 +1*x3624 +1*x3638 +1*x3639 +1*x1039 +1*x1041 +1*x3625 +1*x1042 +1*x3626 +1*x3628 +1*x3640 +1*x1282 +1*x3641 +1*x3246 +1*x1046 +1*x3629 +1*x3517 +1*x3519 +1*x1285 +1*x1287 +1*x3545 +1*x3630 +1*x3642 +1*x3631 +1*x1291 +1*x3643 +1*x1292 +1*x3632 +1*x3644 +1*x1293 +1*x3645 +1*x3646 >= +1;
+1*x3647 +1*x3336 +1*x3618 +1*x3648 +1*x3619 +1*x768 +1*x3620 +1*x3510 +1*x3649 +1*x1138 +1*x792 +1*x1035 +1*x3650 +1*x3558 +1*x3559 +1*x3651 +1*x3652 +1*x3653 +1*x3654 +1*x3655 +1*x3656 +1*x3580 +1*x3657 +1*x3639 +1*x1041 +1*x3658 +1*x3076 +1*x3078 +1*x2721 +1*x3659 +1*x3627 +1*x3602 +1*x3563 +1*x1046 +1*x776 +1*x3660 +1*x3079 +1*x1159 +1*x3661 +1*x1160 +1*x3662 +1*x3663 +1*x1059 +1*x1165 +1*x1166 +1*x2729 +1*x1067 +1*x1170 +1*x3082 +1*x628 >= +1;
+1*x3647 +1*x3336 +1*x3618 +1*x3648 +1*x3619 +1*x768 +1*x3620 +1*x3649 +1*x1138 +1*x792 +1*x3341 +1*x1035 +1*x3650 +1*x3651 +1*x3652 +1*x3653 +1*x3654 +1*x3655 +1*x3623 +1*x3664 +1*x3624 +1*x3656 +1*x3665 +1*x3658 +1*x3666 +1*x3076 +1*x3078 +1*x2721 +1*x3659 +1*x3627 +1*x3667 +1*x1176 +1*x3668 +1*x3660 +1*x3079 +1*x1159 +1*x3661 +1*x1160 +1*x3669 +1*x3670 +1*x3671 +1*x3088 +1*x1082 +1*x3672 +1*x3673 >= +1;
+1*x3647 +1*x3674 +1*x3675 +1*x3619 +1*x3676 +1*x3566 +1*x3341 +1*x3677 +1*x3650 +1*x3560 +1*x3678 +1*x3651 +1*x3679 +1*x3680 +1*x3332 +1*x3681 +1*x3682 +1*x3564 +1*x3683 >= +1;
+1*x3684 +1*x3625 +1*x3685 +1*x3472 +1*x3686 +1*x3687 +1*x3630 +1*x3688 +1*x3631 +1*x3689 +1*x3690 +1*x3691 +1*x3634 >= +1;
+1*x3692 +1*x3693 +1*x3089 +1*x3090 +1*x1122 +1*x3694 +1*x3695 +1*x3479 +1*x3685 +1*x3696 +1*x1129 +1*x1130 +1*x3697 +1*x1117 +1*x3698 +1*x3688 +1*x3248 +1*x1131 +1*x2763 +1*x3699 +1*x1125 +1*x3482 +1*x2764 +1*x1931 +1*x3700 +1*x3691 +1*x3701 >= +1;
+1*x3692 +1*x3693 +1*x3702 +1*x3703 +1*x3089 +1*x3090 +1*x3056 +1*x3057 +1*x3578 +1*x3679 +1*x1122 +1*x3694 +1*x3092 +1*x3685 +1*x3696 +1*x1129 +1*x1017 +1*x1130 +1*x3532 +1*x3704 +1*x3542 +1*x3705 +1*x1117 +1*x1118 +1*x3533 +1*x3698 +1*x3630 +1*x3642 +1*x1028 +1*x3688 +1*x3248 +1*x1131 +1*x3644 +1*x1132 +1*x3546 +1*x3706 +1*x3707 +1*x3645 +1*x3708 +1*x3551 >= +1;
+1*x3692 +1*x3693 +1*x3702 +1*x3703 +1*x3578 +1*x3679 +1*x3694 +1*x3695 +1*x3479 +1*x3532 +1*x3704 +1*x3542 +1*x3697 +1*x3709 +1*x3710 +1*x3706 +1*x3711 +1*x3712 +1*x3554 +1*x3555 +1*x3713 +1*x3714 +1*x3715 +1*x3716 >= +1;
+1*x3649 +1*x1137 +1*x1138 +1*x3640 +1*x3641 >= +1;
+1*x3416 +1*x3717 +1*x3718 +1*x3417 +1*x3719 +1*x3720 +1*x3721 +1*x3722 +1*x3723 +1*x3724 +1*x3725 +1*x3421 +1*x1266 +1*x2561 +1*x1309 +1*x3726 +1*x3727 +1*x3728 +1*x3729 +1*x3471 +1*x3730 +1*x3731 >= +1;
+1*x3732 +1*x3733 +1*x3734 +1*x3719 +1*x3735 +1*x3736 +1*x3737 +1*x3601 +1*x3720 +1*x3738 +1*x3739 +1*x3592 +1*x3740 +1*x3741 +1*x3742 +1*x3743 +1*x3744 +1*x3594 +1*x3745 +1*x3746 +1*x3603 +1*x3747 +1*x3748 +1*x3147 +1*x3749 +1*x3750 +1*x3751 >= +1;
+1*x3752 +1*x3753 +1*x3754 +1*x3755 +1*x3605 +1*x3756 +1*x3757 +1*x3614 +1*x3758 >= +1;
+1*x3759 +1*x3621 +1*x3760 +1*x3637 +1*x3761 +1*x3233 +1*x3762 +1*x3240 +1*x3763 +1*x3623 +1*x3764 +1*x3765 +1*x1272 +1*x3625 +1*x3514 +1*x3766 +1*x3767 +1*x3768 +1*x541 +1*x1276 +1*x3769 +1*x3628 +1*x3770 +1*x1282 +1*x3246 +1*x1283 +1*x3247 +1*x3629 +1*x3139 +1*x3140 +1*x1204 +1*x3196 +1*x3088 +1*x3771 +1*x1288 +1*x3772 +1*x1290 +1*x1291 +1*x3643 +1*x1292 +1*x3151 +1*x3773 +1*x3774 +1*x3775 +1*x3776 +1*x1219 +1*x3565 +1*x3777 +1*x3778 +1*x3779 +1*x3780 >= +1;
+1*x3232 +1*x3676 +1*x3053 +1*x3781 +1*x3703 +1*x3782 +1*x3783 +1*x3784 +1*x3057 +1*x3785 +1*x3235 +1*x3786 +1*x3787 +1*x3788 +1*x3789 +1*x3323 +1*x3790 +1*x3791 +1*x1235 +1*x3792 +1*x3793 +1*x3794 +1*x3541 +1*x2997 +1*x3795 +1*x488 +1*x2880 +1*x3796 +1*x3797 +1*x2881 +1*x3330 >= +1;
+1*x3675 +1*x3676 +1*x3798 +1*x3799 +1*x3783 +1*x3800 +1*x1090 +1*x3653 +1*x3624 +1*x3680 +1*x3343 +1*x899 +1*x3801 +1*x3802 +1*x3666 +1*x3791 +1*x3803 +1*x3804 +1*x3669 +1*x3805 +1*x3806 +1*x3672 +1*x3807 >= +1;
+1*x3808 +1*x3809 +1*x3762 +1*x3454 +1*x1305 +1*x3469 +1*x3684 +1*x3625 +1*x3462 +1*x3490 +1*x3472 >= +1;
+1*x3252 +1*x1303 +1*x1305 +1*x3486 +1*x1143 +1*x608 +1*x3255 +1*x2950 +1*x3738 +1*x3739 +1*x3360 +1*x1308 +1*x3462 +1*x3489 +1*x3258 +1*x3810 +1*x3811 +1*x3259 +1*x612 +1*x3106 +1*x618 +1*x3493 +1*x1309 +1*x2955 +1*x2956 +1*x3744 +1*x3660 +1*x3661 +1*x1160 +1*x619 +1*x3603 +1*x1167 +1*x1170 +1*x3082 +1*x628 +1*x3467 +1*x3812 +1*x2519 >= +1;
+1*x3813 +1*x2571 +1*x3814 +1*x3815 +1*x3816 +1*x3817 +1*x2574 +1*x2576 +1*x3818 +1*x3819 +1*x2580 +1*x3820 +1*x3821 +1*x3822 +1*x2582 +1*x2583 +1*x3823 +1*x1328 +1*x3824 +1*x3825 +1*x3826 +1*x1352 +1*x2588 +1*x2589 +1*x1336 +1*x3827 +1*x279 +1*x2617 +1*x3828 +1*x1341 +1*x3829 +1*x3830 +1*x3831 +1*x1361 +1*x3832 +1*x3833 +1*x3834 +1*x1368 +1*x3835 +1*x3836 +1*x3837 +1*x3838 >= +1;
+1*x3839 +1*x1431 +1*x3840 +1*x3841 +1*x3842 +1*x3843 +1*x2674 +1*x1434 +1*x27 +1*x3844 +1*x1457 +1*x2676 +1*x2679 +1*x3845 +1*x375 +1*x3846 +1*x3847 +1*x39 >= +1;
+1*x3839 +1*x1431 +1*x3840 +1*x3841 +1*x3842 +1*x3843 +1*x3848 +1*x3849 +1*x3850 +1*x2674 +1*x1434 +1*x3844 +1*x3851 +1*x3852 +1*x1456 +1*x2676 +1*x3853 +1*x1439 +1*x2677 +1*x2679 +1*x3854 +1*x3855 +1*x3856 +1*x3857 +1*x3858 +1*x3859 +1*x1441 +1*x3860 +1*x1329 +1*x3861 +1*x1444 +1*x1334 +1*x3862 +1*x2681 +1*x1337 +1*x1447 +1*x3863 +1*x1448 +1*x1449 +1*x3864 +1*x3865 +1*x3866 +1*x3867 +1*x2159 +1*x1452 +1*x3868 +1*x3869 +1*x3870 +1*x3871 +1*x3872 +1*x3873 +1*x3874 +1*x3875 +1*x3876 +1*x1479 +1*x3877 +1*x3878 +1*x3879 +1*x3880 +1*x2167 +1*x3881 +1*x3882 >= +1;
+1*x74 +1*x3883 +1*x3884 +1*x1501 +1*x2701 +1*x3885 +1*x1855 +1*x3886 +1*x3887 +1*x3888 +1*x1502 +1*x3889 +1*x1409 +1*x2649 +1*x1410 +1*x3890 +1*x3891 +1*x3892 +1*x2707 +1*x3893 +1*x3894 +1*x3895 +1*x3896 +1*x3897 +1*x1873 +1*x3898 +1*x3899 +1*x1581 +1*x3900 +1*x3901 +1*x1853 +1*x1399 >= +1;
+1*x3819 +1*x3820 +1*x3902 +1*x1336 +1*x3903 +1*x3904 +1*x3905 +1*x3829 +1*x3906 +1*x3830 +1*x3907 +1*x3832 +1*x3908 +1*x3909 +1*x3835 +1*x3910 +1*x3911 +1*x3837 +1*x3912 +1*x3913 +1*x3838 >= +1;
+1*x3914 +1*x3915 +1*x2717 +1*x3916 +1*x3917 +1*x2718 +1*x3918 +1*x3919 +1*x3920 +1*x1541 +1*x2722 +1*x2725 +1*x3921 +1*x1544 +1*x1545 +1*x3922 +1*x1550 +1*x1551 +1*x2731 +1*x2732 >= +1;
+1*x3914 +1*x3915 +1*x2717 +1*x3916 +1*x3917 +1*x2718 +1*x3923 +1*x1541 +1*x1514 +1*x2634 +1*x3924 +1*x3925 +1*x1545 +1*x3926 +1*x3927 +1*x2639 +1*x1363 +1*x3928 +1*x3929 +1*x2644 >= +1;
+1*x3849 +1*x3930 +1*x3931 +1*x1456 +1*x3854 +1*x3932 +1*x3933 +1*x3860 +1*x3934 +1*x3935 +1*x3936 +1*x3864 +1*x3866 +1*x3937 +1*x3938 +1*x2159 +1*x3939 +1*x3869 +1*x1923 +1*x3940 +1*x3873 +1*x1925 +1*x1927 +1*x3877 +1*x3878 +1*x3880 +1*x2167 +1*x3941 +1*x3881 +1*x3882 >= +1;
+1*x3942 +1*x3943 +1*x3932 +1*x3944 +1*x3945 +1*x3934 +1*x3946 +1*x3947 +1*x3864 +1*x3903 +1*x3948 +1*x3907 +1*x3939 +1*x3949 +1*x3950 +1*x3951 +1*x3952 +1*x3953 +1*x3954 +1*x3955 +1*x3956 >= +1;
+1*x3957 +1*x3884 +1*x1573 +1*x1501 +1*x1577 +1*x3958 +1*x3959 +1*x1574 +1*x3960 +1*x3961 +1*x3962 +1*x1559 +1*x3963 +1*x3942 +1*x3887 +1*x3943 +1*x3919 +1*x3964 +1*x3945 +1*x3896 +1*x3947 +1*x3965 +1*x3966 +1*x3967 +1*x3968 +1*x3969 +1*x3970 +1*x1568 +1*x3971 +1*x1417 +1*x3972 +1*x3973 +1*x3974 +1*x3921 +1*x3975 +1*x3976 +1*x3977 +1*x3978 +1*x3979 >= +1;
+1*x3814 +1*x3980 +1*x3981 +1*x3816 +1*x2783 +1*x2580 +1*x3982 +1*x3983 +1*x3984 +1*x3985 +1*x3835 +1*x3986 +1*x3987 +1*x3837 >= +1;
+1*x3988 +1*x3989 +1*x3990 +1*x3991 +1*x3992 +1*x3923 +1*x3993 +1*x1622 +1*x3994 +1*x1585 +1*x1623 +1*x3995 +1*x3996 +1*x3997 +1*x2635 +1*x3998 +1*x3999 +1*x3174 +1*x3926 +1*x4000 +1*x4001 +1*x3928 +1*x2640 +1*x2900 +1*x4002 +1*x1594 +1*x4003 +1*x4004 +1*x4005 +1*x4006 +1*x4007 +1*x4008 +1*x1988 +1*x4009 +1*x4010 >= +1;
+1*x3988 +1*x3990 +1*x3991 +1*x1622 +1*x1623 +1*x3995 +1*x3174 +1*x1630 >= +1;
+1*x3988 +1*x3989 +1*x3990 +1*x3991 +1*x3992 +1*x3923 +1*x3995 +1*x3996 +1*x3997 +1*x2635 +1*x3998 +1*x3999 +1*x3174 +1*x3926 +1*x4000 +1*x4001 +1*x3928 +1*x2640 +1*x4011 +1*x2645 >= +1;
+1*x3842 +1*x4012 +1*x4013 +1*x4014 +1*x4015 +1*x4016 +1*x3844 +1*x2815 +1*x2676 +1*x2816 +1*x3854 +1*x4017 +1*x4018 +1*x3845 +1*x4019 +1*x4020 +1*x3857 +1*x4021 +1*x4022 +1*x3863 +1*x4023 +1*x4024 +1*x4025 +1*x3847 +1*x4026 +1*x3186 +1*x4027 +1*x4028 +1*x4029 +1*x4030 +1*x2690 +1*x2691 >= +1;
+1*x3842 +1*x4031 +1*x4032 +1*x1434 +1*x4015 +1*x4016 +1*x3844 +1*x4033 +1*x2055 +1*x4034 +1*x3845 +1*x4035 +1*x4036 +1*x4037 +1*x3846 +1*x4038 +1*x1584 +1*x4024 +1*x4039 +1*x3847 >= +1;
+1*x4040 +1*x4041 +1*x1632 +1*x3981 +1*x4012 +1*x4042 +1*x1637 +1*x3982 +1*x1640 +1*x3857 +1*x4043 +1*x3858 +1*x2817 +1*x4022 +1*x4044 +1*x1472 +1*x3863 +1*x1473 +1*x1452 +1*x1345 >= +1;
+1*x4040 +1*x4041 +1*x1632 +1*x3981 +1*x4012 +1*x4014 +1*x4042 +1*x1637 +1*x3982 +1*x4045 +1*x4046 +1*x1638 +1*x1640 +1*x3857 +1*x4043 +1*x3858 +1*x2844 +1*x1649 +1*x2817 +1*x4022 +1*x4044 +1*x1472 +1*x3863 +1*x1473 +1*x4047 +1*x3864 +1*x3983 +1*x4048 +1*x4049 +1*x1452 +1*x4050 +1*x4051 +1*x2830 +1*x1650 +1*x2847 +1*x2848 +1*x1646 +1*x4052 +1*x4053 +1*x4054 +1*x4055 >= +1;
+1*x4056 +1*x3883 +1*x3884 +1*x4041 +1*x2701 +1*x4057 +1*x3888 +1*x4046 +1*x2844 +1*x4058 +1*x3896 +1*x4059 +1*x4060 +1*x2851 +1*x2852 >= +1;
+1*x4061 +1*x1696 +1*x4062 +1*x2893 +1*x1698 +1*x2895 +1*x4063 +1*x2917 +1*x4064 +1*x2920 +1*x2906 >= +1;
+1*x2916 +1*x4063 +1*x4065 +1*x1703 +1*x3970 +1*x4066 +1*x1567 +1*x1568 +1*x2917 +1*x2738 +1*x4064 +1*x3921 +1*x1704 +1*x2920 >= +1;
+1*x2916 +1*x4063 +1*x4065 +1*x1703 +1*x3970 +1*x4066 +1*x1567 +1*x1568 +1*x4067 +1*x4064 +1*x3921 +1*x1704 +1*x2918 +1*x4068 +1*x2125 +1*x1550 +1*x1706 +1*x1552 +1*x4069 >= +1;
+1*x4070 +1*x2944 +1*x2945 +1*x2946 +1*x4062 +1*x4071 +1*x4072 +1*x4073 +1*x2927 +1*x4074 +1*x4075 +1*x1744 +1*x4076 +1*x4077 +1*x1745 +1*x1698 +1*x1746 +1*x2895 +1*x2771 +1*x4078 +1*x2932 +1*x4079 +1*x2952 +1*x2953 +1*x4023 +1*x4080 +1*x4064 +1*x4025 +1*x4081 +1*x2920 +1*x2956 +1*x1750 +1*x4027 +1*x4029 +1*x2936 +1*x4082 +1*x1726 +1*x1752 +1*x1753 +1*x2957 +1*x1755 >= +1;
+1*x4083 +1*x3957 +1*x4084 +1*x4070 +1*x4085 +1*x3505 +1*x2946 +1*x3960 +1*x4086 +1*x3961 +1*x4087 +1*x4088 +1*x3943 +1*x4089 +1*x4090 +1*x4073 +1*x3964 +1*x4091 +1*x2932 +1*x3947 +1*x2953 +1*x3973 +1*x3974 +1*x4092 +1*x3953 >= +1;
+1*x4083 +1*x3957 +1*x4056 +1*x4093 +1*x3884 +1*x4084 +1*x4070 +1*x4085 +1*x3505 +1*x2946 +1*x1577 +1*x4086 +1*x3961 +1*x239 +1*x4087 +1*x4090 +1*x4094 +1*x3964 +1*x4077 +1*x1745 +1*x2916 +1*x4058 +1*x3896 +1*x3968 +1*x2120 +1*x3970 +1*x4066 +1*x1568 +1*x4067 +1*x3266 +1*x2965 +1*x247 +1*x3974 +1*x4064 +1*x3921 +1*x1704 +1*x3975 +1*x2918 +1*x2125 +1*x4095 +1*x2112 +1*x250 +1*x1552 +1*x4069 >= +1;
+1*x4096 +1*x4097 +1*x4098 +1*x4099 +1*x4100 +1*x4101 +1*x4102 +1*x4103 +1*x3850 +1*x4104 +1*x4105 +1*x1757 +1*x1758 +1*x4106 +1*x4107 +1*x4108 >= +1;
+1*x4109 +1*x4110 +1*x4111 +1*x3821 +1*x4112 +1*x2969 +1*x3822 +1*x2987 +1*x2582 +1*x4113 +1*x4114 +1*x4115 +1*x3827 +1*x2973 +1*x4116 +1*x4117 +1*x4118 +1*x3828 +1*x4119 +1*x2993 +1*x3833 +1*x1876 +1*x4120 +1*x4121 +1*x1877 +1*x4122 +1*x4123 +1*x4124 +1*x4125 +1*x4126 >= +1;
+1*x4127 +1*x4110 +1*x3006 +1*x4128 +1*x4129 +1*x3822 +1*x2987 +1*x2583 +1*x4130 +1*x4113 +1*x4131 +1*x4132 +1*x4114 +1*x1827 +1*x4133 +1*x4134 +1*x2036 +1*x4135 +1*x4136 +1*x4137 +1*x3897 +1*x2973 +1*x2048 +1*x1873 +1*x3898 +1*x4138 +1*x279 +1*x4139 +1*x4119 +1*x4140 +1*x4141 +1*x2638 +1*x1390 +1*x2049 +1*x4142 +1*x356 +1*x3008 +1*x3833 +1*x3834 +1*x1861 +1*x1399 +1*x3010 +1*x4143 +1*x4144 >= +1;
+1*x4145 +1*x4098 +1*x3840 +1*x4099 +1*x4146 +1*x3012 +1*x3013 +1*x3850 +1*x4147 +1*x1821 +1*x373 +1*x4148 +1*x4105 +1*x1457 +1*x1757 +1*x389 +1*x1790 +1*x1791 +1*x3014 +1*x392 +1*x3184 +1*x1808 >= +1;
+1*x4149 +1*x4150 +1*x3885 +1*x4151 +1*x1855 +1*x3887 +1*x3888 +1*x1856 +1*x4130 +1*x4113 +1*x4152 +1*x2703 +1*x85 +1*x3896 +1*x4153 +1*x4154 +1*x1864 >= +1;
+1*x4155 +1*x4156 +1*x4157 +1*x4158 +1*x4159 +1*x4160 +1*x4161 +1*x4162 +1*x4163 +1*x1922 +1*x4164 +1*x4165 +1*x4166 +1*x4167 +1*x1926 +1*x3152 +1*x4168 +1*x3773 +1*x4169 +1*x4170 +1*x3779 +1*x4171 +1*x4172 +1*x4173 +1*x4174 >= +1;
+1*x4175 +1*x4176 +1*x4177 +1*x1818 +1*x4178 +1*x4179 +1*x3963 +1*x1944 +1*x4180 +1*x4181 +1*x4182 +1*x1919 +1*x1838 +1*x3873 +1*x1925 +1*x4183 +1*x3976 >= +1;
+1*x4175 +1*x4184 +1*x4176 +1*x4177 +1*x1818 +1*x4185 +1*x3104 +1*x4179 +1*x3963 +1*x4186 +1*x4187 +1*x1950 +1*x1943 +1*x1944 +1*x4188 +1*x4180 +1*x4189 +1*x2779 +1*x1953 +1*x616 +1*x2432 +1*x1945 +1*x4181 +1*x4182 +1*x1919 +1*x4190 +1*x4191 +1*x4192 +1*x1947 +1*x3610 +1*x4193 +1*x3107 +1*x1972 +1*x1962 +1*x4194 +1*x4195 +1*x4196 +1*x3873 +1*x1925 +1*x4197 +1*x3880 +1*x3941 +1*x3749 +1*x3365 +1*x4198 >= +1;
+1*x4176 +1*x3958 +1*x4151 +1*x4178 +1*x3961 +1*x3963 +1*x4199 +1*x3887 +1*x4200 +1*x4201 +1*x4187 +1*x4202 +1*x3114 +1*x3945 +1*x4203 +1*x3896 +1*x4204 +1*x4137 +1*x3947 +1*x4138 +1*x3966 +1*x3096 +1*x4205 +1*x3972 +1*x4190 +1*x4191 +1*x3973 +1*x3974 +1*x3117 +1*x4206 +1*x4207 +1*x4208 +1*x4209 +1*x4183 +1*x3976 +1*x3123 +1*x4210 +1*x4211 +1*x4212 +1*x3977 +1*x4213 +1*x3979 +1*x4214 >= +1;
+1*x4097 +1*x4215 +1*x4102 +1*x4216 +1*x4217 +1*x4104 +1*x4218 +1*x4219 +1*x4105 +1*x1974 +1*x3990 +1*x4033 +1*x4220 +1*x3127 +1*x3131 +1*x3132 +1*x4221 +1*x1977 +1*x4222 +1*x4223 +1*x4224 +1*x4225 +1*x1979 +1*x4226 +1*x1993 +1*x4227 +1*x4228 +1*x3231 +1*x1986 +1*x4229 +1*x1987 +1*x4230 +1*x4231 >= +1;
+1*x4097 +1*x4215 +1*x4216 +1*x4217 +1*x4218 +1*x4219 +1*x4105 +1*x4232 +1*x1974 +1*x3990 +1*x4033 +1*x4220 +1*x3127 +1*x4233 +1*x4156 +1*x3132 +1*x4221 +1*x1977 +1*x4037 +1*x3137 +1*x4222 +1*x4224 +1*x1979 +1*x4226 +1*x1991 +1*x1993 +1*x2000 +1*x2001 +1*x2002 +1*x4234 +1*x1985 +1*x2978 +1*x4235 +1*x4236 +1*x1986 +1*x1594 +1*x1597 +1*x2980 +1*x4237 +1*x2005 +1*x4238 +1*x1599 +1*x1600 +1*x4239 +1*x4240 +1*x2006 +1*x4241 +1*x2008 +1*x1609 >= +1;
+1*x4097 +1*x4215 +1*x4102 +1*x4216 +1*x4217 +1*x4104 +1*x4218 +1*x4219 +1*x3990 +1*x4033 +1*x4233 +1*x4156 +1*x4221 +1*x4222 +1*x4223 +1*x4224 +1*x4225 +1*x4242 +1*x4235 +1*x4236 +1*x4243 >= +1;
+1*x4244 +1*x4217 +1*x4016 +1*x4148 +1*x4105 +1*x2054 +1*x4033 +1*x2055 +1*x4245 +1*x3845 +1*x2056 +1*x4037 +1*x3846 +1*x4038 +1*x3183 +1*x4246 +1*x3184 +1*x4247 +1*x4224 +1*x4024 +1*x4248 +1*x4039 +1*x4249 +1*x4225 +1*x4250 +1*x4226 +1*x3847 +1*x1840 +1*x4251 +1*x1842 +1*x4228 +1*x3187 +1*x4252 +1*x4230 +1*x3024 +1*x4253 +1*x4254 >= +1;
+1*x4244 +1*x4217 +1*x4016 +1*x4255 +1*x4148 +1*x4105 +1*x2054 +1*x4033 +1*x2055 +1*x4017 +1*x4245 +1*x3845 +1*x2056 +1*x4019 +1*x4020 +1*x4256 +1*x4257 +1*x2058 +1*x1643 +1*x4037 +1*x3846 +1*x4038 +1*x4222 +1*x4247 +1*x4224 +1*x4258 +1*x4024 +1*x4248 +1*x4039 +1*x4025 +1*x4250 +1*x4226 +1*x2061 +1*x3847 +1*x1840 +1*x1858 +1*x1991 +1*x1993 +1*x4259 +1*x2001 +1*x2002 +1*x4235 +1*x4236 +1*x4260 +1*x4261 +1*x4028 +1*x4212 +1*x4262 +1*x4237 +1*x4238 +1*x1599 +1*x1600 >= +1;
+1*x4057 +1*x2068 +1*x3888 +1*x1856 +1*x2535 +1*x4263 +1*x4264 +1*x4265 +1*x4266 +1*x4267 >= +1;
+1*x4219 +1*x4268 +1*x3229 +1*x4269 +1*x3131 +1*x4156 +1*x4270 +1*x3768 +1*x3770 +1*x4157 +1*x4271 +1*x4234 +1*x4272 +1*x545 +1*x1985 +1*x4273 +1*x3152 +1*x3773 +1*x4274 +1*x4275 +1*x4241 +1*x4276 +1*x3155 +1*x3157 +1*x2549 +1*x546 >= +1;
+1*x4277 +1*x4268 +1*x4269 +1*x4278 +1*x2076 +1*x3770 +1*x4279 +1*x4280 +1*x4281 +1*x4282 +1*x4283 +1*x2883 +1*x4284 +1*x4285 +1*x4286 >= +1;
+1*x4287 +1*x4288 +1*x4289 +1*x4290 +1*x4291 +1*x4292 +1*x4293 +1*x4139 +1*x4294 +1*x4295 +1*x4296 +1*x4297 >= +1;
+1*x4287 +1*x4288 +1*x4289 +1*x4290 +1*x4298 +1*x4295 +1*x4296 +1*x4272 +1*x4299 +1*x4300 +1*x2083 +1*x4301 >= +1;
+1*x4302 +1*x1732 +1*x4303 +1*x4089 +1*x4304 +1*x2122 +1*x4305 +1*x1735 +1*x4279 +1*x4280 +1*x4306 +1*x4283 +1*x4307 +1*x4308 +1*x4297 +1*x4309 +1*x2130 +1*x4310 >= +1;
+1*x4311 +1*x3267 +1*x4312 +1*x2137 +1*x4313 +1*x3270 +1*x4314 +1*x4315 +1*x4316 +1*x4317 +1*x4318 +1*x4319 +1*x4320 +1*x2199 +1*x2145 +1*x4321 +1*x4322 +1*x4323 >= +1;
+1*x3823 +1*x4324 +1*x4325 +1*x3827 +1*x4326 +1*x4327 +1*x4328 +1*x4117 +1*x4329 +1*x4330 +1*x4331 +1*x4332 +1*x4333 +1*x4334 +1*x2609 +1*x4335 +1*x4336 +1*x4121 +1*x4337 +1*x4338 +1*x2365 +1*x3836 +1*x4339 +1*x3377 +1*x4340 +1*x2612 +1*x4341 +1*x2216 +1*x4342 +1*x3378 +1*x2218 +1*x2220 +1*x2222 +1*x2613 +1*x4343 +1*x2614 >= +1;
+1*x3823 +1*x4324 +1*x4325 +1*x3827 +1*x4326 +1*x4327 +1*x4328 +1*x4117 +1*x4317 +1*x4318 +1*x4319 +1*x3830 +1*x4333 +1*x4334 +1*x2609 +1*x3304 +1*x4336 +1*x4121 +1*x4321 +1*x4340 +1*x4322 +1*x4323 +1*x4344 +1*x4345 +1*x4126 >= +1;
+1*x4313 +1*x4346 +1*x4347 +1*x4348 +1*x2266 +1*x4349 +1*x4350 +1*x4351 +1*x4316 +1*x4352 +1*x4353 +1*x4317 +1*x4320 +1*x4354 +1*x4322 +1*x4355 >= +1;
+1*x4356 +1*x4357 +1*x4358 +1*x4359 +1*x4360 +1*x3823 +1*x4361 +1*x4362 +1*x4363 +1*x4346 +1*x4348 +1*x4326 +1*x4364 +1*x4365 +1*x3312 +1*x4366 +1*x4349 +1*x1418 +1*x4328 +1*x4367 +1*x4317 +1*x3831 +1*x4368 +1*x4369 +1*x4332 +1*x4333 +1*x3304 +1*x4370 +1*x4371 +1*x4372 +1*x4373 +1*x4374 +1*x4375 +1*x4376 +1*x4377 +1*x4378 >= +1;
+1*x4379 +1*x4360 +1*x4380 +1*x3891 +1*x3892 +1*x3309 +1*x2707 +1*x4381 +1*x4348 +1*x4382 +1*x3894 +1*x3895 +1*x4326 +1*x4383 +1*x4384 +1*x3312 +1*x3313 +1*x3314 +1*x3301 +1*x4385 +1*x4386 +1*x4387 +1*x3304 +1*x4336 +1*x4355 >= +1;
+1*x4388 +1*x3320 +1*x4389 +1*x4390 +1*x3322 +1*x3902 +1*x4324 +1*x2204 +1*x2182 +1*x4318 +1*x3906 +1*x3830 +1*x4391 +1*x4392 +1*x4340 +1*x2215 +1*x4345 +1*x4393 +1*x4394 >= +1;
+1*x4395 +1*x3931 +1*x4396 +1*x4397 +1*x4398 +1*x3860 +1*x4399 +1*x4400 +1*x4401 +1*x3937 +1*x4402 +1*x4403 +1*x3361 +1*x4404 +1*x4405 +1*x3690 +1*x4406 +1*x3877 +1*x4407 +1*x4408 +1*x4409 >= +1;
+1*x4410 +1*x4411 +1*x801 +1*x4412 +1*x4413 +1*x4400 +1*x2423 +1*x4414 +1*x4415 +1*x3937 +1*x1947 +1*x4402 +1*x4403 +1*x3361 +1*x4416 +1*x4417 +1*x3362 +1*x4418 +1*x4419 +1*x4194 +1*x4406 +1*x3877 +1*x3363 +1*x3364 +1*x4082 +1*x4409 +1*x2427 +1*x2957 +1*x1755 >= +1;
+1*x4420 +1*x4421 +1*x4232 +1*x4314 +1*x4315 +1*x4036 +1*x4037 +1*x4422 +1*x4320 +1*x4423 >= +1;
+1*x2260 +1*x2261 +1*x4424 >= +1;
+1*x4361 +1*x4425 +1*x3410 +1*x4426 +1*x4365 +1*x4427 +1*x4332 +1*x3412 +1*x4428 +1*x4429 >= +1;
+1*x4430 +1*x4425 +1*x4431 +1*x4432 +1*x4433 +1*x4434 +1*x2281 +1*x4383 +1*x2529 +1*x4384 +1*x4435 +1*x4264 +1*x4368 +1*x4050 +1*x2848 +1*x4436 +1*x2849 +1*x4385 +1*x4437 +1*x3412 +1*x4054 >= +1;
+1*x4438 +1*x4390 +1*x2293 +1*x4439 +1*x2206 +1*x4339 >= +1;
+1*x4440 +1*x4441 +1*x4442 +1*x3450 +1*x4443 +1*x3453 >= +1;
+1*x4440 +1*x4441 +1*x4442 +1*x3450 +1*x4444 +1*x4445 +1*x3992 +1*x4446 +1*x1701 +1*x4447 +1*x4448 +1*x2265 +1*x4449 +1*x883 +1*x885 +1*x4068 +1*x4450 +1*x1706 +1*x892 +1*x4451 >= +1;
+1*x4452 +1*x4453 +1*x4454 +1*x2303 +1*x4455 +1*x4456 >= +1;
+1*x4452 +1*x4454 +1*x4457 +1*x3938 +1*x4458 +1*x4459 +1*x4460 +1*x4461 >= +1;
+1*x4462 +1*x3491 +1*x3492 +1*x4079 +1*x2952 +1*x2953 +1*x3493 +1*x2956 +1*x4463 +1*x4464 +1*x1750 +1*x4417 +1*x3362 +1*x4418 +1*x4419 +1*x3363 +1*x4082 +1*x4465 +1*x970 +1*x2427 +1*x2957 +1*x1755 +1*x4466 >= +1;
+1*x4084 +1*x3503 +1*x3505 +1*x3960 +1*x4467 +1*x4468 +1*x4432 +1*x4434 +1*x4383 +1*x4384 +1*x4067 +1*x2918 +1*x4469 >= +1;
+1*x4470 +1*x2349 +1*x3529 +1*x4471 +1*x3530 +1*x4472 +1*x4473 +1*x4474 +1*x4475 +1*x3544 +1*x3545 +1*x2362 +1*x4476 +1*x3547 +1*x3549 >= +1;
+1*x4477 +1*x4478 +1*x3558 +1*x4479 +1*x4480 +1*x4481 +1*x4482 +1*x3513 +1*x3639 +1*x4106 +1*x4483 +1*x4484 +1*x4485 +1*x3562 +1*x4486 +1*x4487 +1*x4488 +1*x4489 +1*x4490 +1*x4229 +1*x4007 +1*x4476 +1*x4491 +1*x4492 +1*x4371 +1*x4493 +1*x4373 +1*x4374 +1*x4494 +1*x4375 +1*x4495 >= +1;
+1*x4496 +1*x4497 +1*x4498 +1*x4499 +1*x4500 +1*x4501 +1*x4502 +1*x4115 +1*x4503 +1*x4327 +1*x4504 +1*x4026 +1*x4505 +1*x4506 +1*x4507 +1*x4331 +1*x4508 +1*x4509 +1*x4510 +1*x4511 +1*x4512 +1*x4513 +1*x4514 +1*x4121 +1*x4515 +1*x4516 +1*x4517 +1*x4337 +1*x4518 +1*x3711 +1*x4519 +1*x4520 +1*x4408 +1*x4521 +1*x4522 >= +1;
+1*x4523 +1*x4524 +1*x2383 +1*x4525 +1*x1819 +1*x4526 +1*x4527 +1*x2388 +1*x4528 +1*x2389 +1*x2393 +1*x4529 +1*x4530 +1*x1837 +1*x4251 +1*x1841 +1*x1842 >= +1;
+1*x4531 +1*x4532 +1*x4533 +1*x4534 +1*x4535 +1*x3899 +1*x4536 +1*x1851 +1*x4537 +1*x4265 +1*x4266 +1*x4538 +1*x2708 +1*x3598 +1*x4539 +1*x4540 +1*x3757 +1*x3612 +1*x4541 +1*x3614 +1*x4542 +1*x3615 +1*x4267 >= +1;
+1*x3648 +1*x3620 +1*x4478 +1*x4543 +1*x3650 +1*x3558 +1*x4544 +1*x3664 +1*x4545 +1*x4546 +1*x4547 +1*x3627 +1*x4548 +1*x3629 +1*x3672 +1*x3564 +1*x3633 +1*x4549 +1*x4550 +1*x4551 >= +1;
+1*x3648 +1*x3620 +1*x4478 +1*x4543 +1*x3650 +1*x4480 +1*x4544 +1*x3664 +1*x3665 +1*x4545 +1*x4546 +1*x4552 +1*x3658 +1*x4547 +1*x3659 +1*x3627 +1*x4553 +1*x2434 +1*x4554 +1*x3667 +1*x1176 +1*x4487 +1*x3670 +1*x3671 +1*x3672 +1*x4555 +1*x4556 +1*x4557 +1*x3673 >= +1;
+1*x4558 +1*x3695 +1*x4559 +1*x4503 +1*x4560 +1*x4561 +1*x4562 +1*x4506 +1*x4563 +1*x4564 +1*x3710 +1*x4507 +1*x4405 +1*x4331 +1*x4508 +1*x4565 +1*x4566 +1*x4511 +1*x3699 +1*x1125 +1*x4567 +1*x1126 +1*x4568 +1*x4517 +1*x3711 +1*x4569 +1*x4570 +1*x4519 +1*x4571 +1*x3691 +1*x4572 +1*x4550 +1*x4520 +1*x3634 +1*x4408 +1*x4521 +1*x2217 +1*x4573 >= +1;
+1*x4558 +1*x4574 +1*x4559 +1*x4560 +1*x4561 +1*x4575 +1*x4576 +1*x4566 +1*x4577 +1*x4570 >= +1;
+1*x4185 +1*x2422 +1*x4186 +1*x4544 +1*x3665 +1*x1174 +1*x4545 +1*x4546 +1*x4578 +1*x2391 +1*x2423 +1*x4579 +1*x2434 +1*x1176 +1*x4580 +1*x4403 +1*x4416 +1*x1177 +1*x2426 +1*x3670 +1*x1178 +1*x4555 +1*x4556 +1*x4557 +1*x3673 >= +1;
+1*x4581 +1*x4582 +1*x4202 +1*x4560 +1*x4583 +1*x3972 +1*x4572 >= +1;
+1*x4584 +1*x4585 +1*x4586 +1*x4587 +1*x4588 +1*x4589 +1*x4244 +1*x4217 +1*x4590 +1*x4591 +1*x4592 +1*x4016 +1*x4593 +1*x4421 +1*x4245 +1*x4020 +1*x4594 +1*x4256 +1*x4453 +1*x4595 +1*x4037 +1*x4038 +1*x2471 +1*x4596 +1*x4456 +1*x4259 +1*x2002 +1*x4597 >= +1;
+1*x4592 +1*x4593 +1*x4497 +1*x4598 +1*x4599 +1*x4020 +1*x4498 +1*x4501 +1*x4502 +1*x4600 +1*x4504 +1*x4026 +1*x3440 +1*x4601 +1*x4602 +1*x4510 +1*x4515 +1*x4522 +1*x4603 >= +1;
+1*x4585 +1*x4604 +1*x4524 +1*x2480 +1*x2388 +1*x4605 +1*x4606 +1*x4528 +1*x4578 +1*x4607 +1*x2482 +1*x2484 +1*x4530 +1*x1837 +1*x4249 +1*x2485 +1*x4251 +1*x1842 +1*x4602 +1*x4608 +1*x2486 +1*x4197 +1*x4515 +1*x4540 +1*x2396 >= +1;
+1*x2523 +1*x2535 +1*x4609 +1*x4433 +1*x2527 +1*x4264 +1*x4601 +1*x4265 +1*x4266 +1*x4610 +1*x4436 +1*x2126 +1*x4510 +1*x4611 +1*x2474 +1*x4612 +1*x4613 +1*x4214 +1*x4614 >= +1;
+1*x2537 +1*x4270 +1*x4615 +1*x3767 +1*x4616 +1*x3768 +1*x1276 +1*x4223 +1*x2551 +1*x4617 +1*x3771 +1*x4242 +1*x4618 +1*x3775 +1*x3776 >= +1;
+1*x4619 +1*x4441 +1*x4543 +1*x4620 +1*x4621 +1*x4544 +1*x3664 +1*x4622 +1*x4623 +1*x3801 +1*x4624 +1*x4484 +1*x4449 +1*x4554 +1*x4625 +1*x4626 +1*x3805 +1*x3670 +1*x3671 +1*x4627 +1*x4628 +1*x4629 +1*x4630 +1*x4631 +1*x3499 +1*x4495 >= +1;
+1*x4619 +1*x4441 +1*x4543 +1*x4622 +1*x4623 +1*x4484 +1*x4615 +1*x4616 +1*x4449 +1*x4617 >= +1;
+1*x4632 +1*x3799 +1*x4620 +1*x4633 +1*x3783 +1*x4634 +1*x3680 +1*x4635 +1*x3801 +1*x4636 +1*x4547 +1*x3791 +1*x4637 +1*x4638 +1*x4639 +1*x3804 +1*x3672 +1*x4640 +1*x3633 +1*x4641 +1*x4642 >= +1;
+1*x4632 +1*x4620 +1*x4633 +1*x4634 +1*x4635 +1*x4624 +1*x4547 +1*x4637 +1*x4639 >= +1;
+1*x4632 +1*x3799 +1*x4620 +1*x4633 +1*x3783 +1*x4643 +1*x4621 +1*x4635 +1*x3801 +1*x4636 +1*x4624 +1*x4638 +1*x4290 +1*x4644 +1*x4293 +1*x4294 +1*x3804 +1*x3805 +1*x4296 +1*x4628 +1*x4629 +1*x4437 +1*x4630 >= +1;
+1*x4632 +1*x3799 +1*x4620 +1*x4643 +1*x4621 +1*x4634 +1*x3680 +1*x4645 >= +1;
+1*x4646 +1*x4647 +1*x4648 +1*x4574 +1*x4649 +1*x4650 +1*x4651 +1*x3697 +1*x4306 +1*x4652 +1*x4653 +1*x4654 +1*x2547 +1*x4283 +1*x4307 +1*x4308 +1*x4655 +1*x4577 +1*x4656 +1*x4309 +1*x2130 >= +1;
+1*x4657 +1*x4658 +1*x4619 +1*x4604 +1*x3252 +1*x4185 +1*x4544 +1*x4606 +1*x4578 +1*x4659 +1*x3811 +1*x4462 +1*x4079 +1*x3493 +1*x2485 +1*x2956 +1*x4626 +1*x2426 +1*x4419 +1*x4197 +1*x4082 +1*x4465 +1*x4660 +1*x4661 +1*x2396 +1*x2427 +1*x4466 >= +1;
+1*x4657 +1*x4658 +1*x4619 +1*x4604 +1*x3252 +1*x4662 +1*x4663 +1*x4588 +1*x4185 +1*x4664 +1*x4621 +1*x4544 +1*x4623 +1*x4606 +1*x4665 +1*x4659 +1*x3811 +1*x4666 +1*x4462 +1*x4079 +1*x4191 +1*x3493 +1*x2485 +1*x2956 +1*x4580 +1*x4667 +1*x4668 +1*x4626 +1*x2426 +1*x3670 +1*x1178 +1*x4669 +1*x4627 +1*x4419 +1*x4628 +1*x4629 +1*x4670 +1*x4196 +1*x4671 +1*x2508 +1*x4082 +1*x4092 +1*x4460 +1*x2534 +1*x2440 +1*x3497 +1*x4672 +1*x4631 +1*x3499 +1*x2442 >= +1;
+1*x4657 +1*x4658 +1*x4619 +1*x4604 +1*x3252 +1*x4662 +1*x4663 +1*x4588 +1*x4185 +1*x4664 +1*x4621 +1*x4544 +1*x4647 +1*x4673 +1*x4578 +1*x4674 +1*x3739 +1*x4665 +1*x3257 +1*x4659 +1*x3811 +1*x4579 +1*x4580 +1*x4675 +1*x4667 +1*x4668 +1*x619 +1*x4626 +1*x2426 +1*x3670 +1*x1178 +1*x4676 +1*x3262 >= +1;