bingham_h250.spec 31.3 KB
Newer Older
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
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
vars
x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44 x45 x46 x47 x48 x49 x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x60 x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74 x75 x76 x77 x78 x79 x80 x81 x82 x83 x84 x85 x86 x87 x88 x89 x90 x91 x92 x93 x94 x95 x96 x97 x98 x99 x100 x101 x102 x103 x104 x105 x106 x107 x108 x109 x110 x111 x112 x113 x114 x115 x116 x117 x118 x119 x120 x121 x122 x123 x124 x125 x126 x127 x128 x129 x130 x131 x132 x133 x134 x135 x136 x137 x138 x139 x140 x141 x142 x143 x144 x145 x146 x147 x148 x149 x150 x151 x152 x153 x154 x155 x156 x157 x158 x159 x160 x161 x162 x163 x164 x165 x166 x167 x168 x169 x170 x171 x172 x173 x174 x175 x176 x177 x178 x179 x180 x181 x182 x183 x184 x185 x186 x187 x188 x189 x190 x191 x192 x193 x194 x195 x196 x197 x198 x199 x200 x201 x202 x203 x204 x205 x206 x207 x208 x209 x210 x211 x212 x213 x214 x215 x216 x217 x218 x219 x220 x221 x222 x223 x224 x225 x226 x227 x228 x229 x230 x231 x232 x233 x234 x235 x236 x237 x238 x239 x240 x241 x242 x243 x244 x245 x246 x247 x248 x249 x250 x251 x252 

rules
x0 >= 1, x252 >= 1 -> x0'=x0-1, x252'=x252-1, x251'=x251+1, x1'=x1+1;
x1 >= 1, x252 >= 1 -> x1'=x1-1, x252'=x252-1, x251'=x251+1, x0'=x0+1;
x1 >= 1, x251 >= 1 -> x1'=x1-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x1 >= 1 -> x1'=x1-1, x2'=x2+1;
x2 >= 1, x251 >= 1 -> x2'=x2-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x2 >= 1 -> x2'=x2-1, x3'=x3+1;
x3 >= 1, x251 >= 1 -> x3'=x3-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x3 >= 1 -> x3'=x3-1, x4'=x4+1;
x4 >= 1, x251 >= 1 -> x4'=x4-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x4 >= 1 -> x4'=x4-1, x5'=x5+1;
x5 >= 1, x251 >= 1 -> x5'=x5-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x5 >= 1 -> x5'=x5-1, x6'=x6+1;
x6 >= 1, x251 >= 1 -> x6'=x6-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x6 >= 1 -> x6'=x6-1, x7'=x7+1;
x7 >= 1, x251 >= 1 -> x7'=x7-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x7 >= 1 -> x7'=x7-1, x8'=x8+1;
x8 >= 1, x251 >= 1 -> x8'=x8-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x8 >= 1 -> x8'=x8-1, x9'=x9+1;
x9 >= 1, x251 >= 1 -> x9'=x9-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x9 >= 1 -> x9'=x9-1, x10'=x10+1;
x10 >= 1, x251 >= 1 -> x10'=x10-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x10 >= 1 -> x10'=x10-1, x11'=x11+1;
x11 >= 1, x251 >= 1 -> x11'=x11-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x11 >= 1 -> x11'=x11-1, x12'=x12+1;
x12 >= 1, x251 >= 1 -> x12'=x12-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x12 >= 1 -> x12'=x12-1, x13'=x13+1;
x13 >= 1, x251 >= 1 -> x13'=x13-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x13 >= 1 -> x13'=x13-1, x14'=x14+1;
x14 >= 1, x251 >= 1 -> x14'=x14-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x14 >= 1 -> x14'=x14-1, x15'=x15+1;
x15 >= 1, x251 >= 1 -> x15'=x15-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x15 >= 1 -> x15'=x15-1, x16'=x16+1;
x16 >= 1, x251 >= 1 -> x16'=x16-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x16 >= 1 -> x16'=x16-1, x17'=x17+1;
x17 >= 1, x251 >= 1 -> x17'=x17-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x17 >= 1 -> x17'=x17-1, x18'=x18+1;
x18 >= 1, x251 >= 1 -> x18'=x18-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x18 >= 1 -> x18'=x18-1, x19'=x19+1;
x19 >= 1, x251 >= 1 -> x19'=x19-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x19 >= 1 -> x19'=x19-1, x20'=x20+1;
x20 >= 1, x251 >= 1 -> x20'=x20-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x20 >= 1 -> x20'=x20-1, x21'=x21+1;
x21 >= 1, x251 >= 1 -> x21'=x21-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x21 >= 1 -> x21'=x21-1, x22'=x22+1;
x22 >= 1, x251 >= 1 -> x22'=x22-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x22 >= 1 -> x22'=x22-1, x23'=x23+1;
x23 >= 1, x251 >= 1 -> x23'=x23-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x23 >= 1 -> x23'=x23-1, x24'=x24+1;
x24 >= 1, x251 >= 1 -> x24'=x24-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x24 >= 1 -> x24'=x24-1, x25'=x25+1;
x25 >= 1, x251 >= 1 -> x25'=x25-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x25 >= 1 -> x25'=x25-1, x26'=x26+1;
x26 >= 1, x251 >= 1 -> x26'=x26-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x26 >= 1 -> x26'=x26-1, x27'=x27+1;
x27 >= 1, x251 >= 1 -> x27'=x27-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x27 >= 1 -> x27'=x27-1, x28'=x28+1;
x28 >= 1, x251 >= 1 -> x28'=x28-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x28 >= 1 -> x28'=x28-1, x29'=x29+1;
x29 >= 1, x251 >= 1 -> x29'=x29-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x29 >= 1 -> x29'=x29-1, x30'=x30+1;
x30 >= 1, x251 >= 1 -> x30'=x30-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x30 >= 1 -> x30'=x30-1, x31'=x31+1;
x31 >= 1, x251 >= 1 -> x31'=x31-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x31 >= 1 -> x31'=x31-1, x32'=x32+1;
x32 >= 1, x251 >= 1 -> x32'=x32-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x32 >= 1 -> x32'=x32-1, x33'=x33+1;
x33 >= 1, x251 >= 1 -> x33'=x33-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x33 >= 1 -> x33'=x33-1, x34'=x34+1;
x34 >= 1, x251 >= 1 -> x34'=x34-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x34 >= 1 -> x34'=x34-1, x35'=x35+1;
x35 >= 1, x251 >= 1 -> x35'=x35-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x35 >= 1 -> x35'=x35-1, x36'=x36+1;
x36 >= 1, x251 >= 1 -> x36'=x36-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x36 >= 1 -> x36'=x36-1, x37'=x37+1;
x37 >= 1, x251 >= 1 -> x37'=x37-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x37 >= 1 -> x37'=x37-1, x38'=x38+1;
x38 >= 1, x251 >= 1 -> x38'=x38-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x38 >= 1 -> x38'=x38-1, x39'=x39+1;
x39 >= 1, x251 >= 1 -> x39'=x39-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x39 >= 1 -> x39'=x39-1, x40'=x40+1;
x40 >= 1, x251 >= 1 -> x40'=x40-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x40 >= 1 -> x40'=x40-1, x41'=x41+1;
x41 >= 1, x251 >= 1 -> x41'=x41-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x41 >= 1 -> x41'=x41-1, x42'=x42+1;
x42 >= 1, x251 >= 1 -> x42'=x42-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x42 >= 1 -> x42'=x42-1, x43'=x43+1;
x43 >= 1, x251 >= 1 -> x43'=x43-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x43 >= 1 -> x43'=x43-1, x44'=x44+1;
x44 >= 1, x251 >= 1 -> x44'=x44-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x44 >= 1 -> x44'=x44-1, x45'=x45+1;
x45 >= 1, x251 >= 1 -> x45'=x45-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x45 >= 1 -> x45'=x45-1, x46'=x46+1;
x46 >= 1, x251 >= 1 -> x46'=x46-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x46 >= 1 -> x46'=x46-1, x47'=x47+1;
x47 >= 1, x251 >= 1 -> x47'=x47-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x47 >= 1 -> x47'=x47-1, x48'=x48+1;
x48 >= 1, x251 >= 1 -> x48'=x48-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x48 >= 1 -> x48'=x48-1, x49'=x49+1;
x49 >= 1, x251 >= 1 -> x49'=x49-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x49 >= 1 -> x49'=x49-1, x50'=x50+1;
x50 >= 1, x251 >= 1 -> x50'=x50-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x50 >= 1 -> x50'=x50-1, x51'=x51+1;
x51 >= 1, x251 >= 1 -> x51'=x51-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x51 >= 1 -> x51'=x51-1, x52'=x52+1;
x52 >= 1, x251 >= 1 -> x52'=x52-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x52 >= 1 -> x52'=x52-1, x53'=x53+1;
x53 >= 1, x251 >= 1 -> x53'=x53-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x53 >= 1 -> x53'=x53-1, x54'=x54+1;
x54 >= 1, x251 >= 1 -> x54'=x54-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x54 >= 1 -> x54'=x54-1, x55'=x55+1;
x55 >= 1, x251 >= 1 -> x55'=x55-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x55 >= 1 -> x55'=x55-1, x56'=x56+1;
x56 >= 1, x251 >= 1 -> x56'=x56-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x56 >= 1 -> x56'=x56-1, x57'=x57+1;
x57 >= 1, x251 >= 1 -> x57'=x57-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x57 >= 1 -> x57'=x57-1, x58'=x58+1;
x58 >= 1, x251 >= 1 -> x58'=x58-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x58 >= 1 -> x58'=x58-1, x59'=x59+1;
x59 >= 1, x251 >= 1 -> x59'=x59-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x59 >= 1 -> x59'=x59-1, x60'=x60+1;
x60 >= 1, x251 >= 1 -> x60'=x60-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x60 >= 1 -> x60'=x60-1, x61'=x61+1;
x61 >= 1, x251 >= 1 -> x61'=x61-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x61 >= 1 -> x61'=x61-1, x62'=x62+1;
x62 >= 1, x251 >= 1 -> x62'=x62-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x62 >= 1 -> x62'=x62-1, x63'=x63+1;
x63 >= 1, x251 >= 1 -> x63'=x63-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x63 >= 1 -> x63'=x63-1, x64'=x64+1;
x64 >= 1, x251 >= 1 -> x64'=x64-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x64 >= 1 -> x64'=x64-1, x65'=x65+1;
x65 >= 1, x251 >= 1 -> x65'=x65-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x65 >= 1 -> x65'=x65-1, x66'=x66+1;
x66 >= 1, x251 >= 1 -> x66'=x66-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x66 >= 1 -> x66'=x66-1, x67'=x67+1;
x67 >= 1, x251 >= 1 -> x67'=x67-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x67 >= 1 -> x67'=x67-1, x68'=x68+1;
x68 >= 1, x251 >= 1 -> x68'=x68-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x68 >= 1 -> x68'=x68-1, x69'=x69+1;
x69 >= 1, x251 >= 1 -> x69'=x69-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x69 >= 1 -> x69'=x69-1, x70'=x70+1;
x70 >= 1, x251 >= 1 -> x70'=x70-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x70 >= 1 -> x70'=x70-1, x71'=x71+1;
x71 >= 1, x251 >= 1 -> x71'=x71-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x71 >= 1 -> x71'=x71-1, x72'=x72+1;
x72 >= 1, x251 >= 1 -> x72'=x72-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x72 >= 1 -> x72'=x72-1, x73'=x73+1;
x73 >= 1, x251 >= 1 -> x73'=x73-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x73 >= 1 -> x73'=x73-1, x74'=x74+1;
x74 >= 1, x251 >= 1 -> x74'=x74-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x74 >= 1 -> x74'=x74-1, x75'=x75+1;
x75 >= 1, x251 >= 1 -> x75'=x75-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x75 >= 1 -> x75'=x75-1, x76'=x76+1;
x76 >= 1, x251 >= 1 -> x76'=x76-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x76 >= 1 -> x76'=x76-1, x77'=x77+1;
x77 >= 1, x251 >= 1 -> x77'=x77-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x77 >= 1 -> x77'=x77-1, x78'=x78+1;
x78 >= 1, x251 >= 1 -> x78'=x78-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x78 >= 1 -> x78'=x78-1, x79'=x79+1;
x79 >= 1, x251 >= 1 -> x79'=x79-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x79 >= 1 -> x79'=x79-1, x80'=x80+1;
x80 >= 1, x251 >= 1 -> x80'=x80-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x80 >= 1 -> x80'=x80-1, x81'=x81+1;
x81 >= 1, x251 >= 1 -> x81'=x81-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x81 >= 1 -> x81'=x81-1, x82'=x82+1;
x82 >= 1, x251 >= 1 -> x82'=x82-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x82 >= 1 -> x82'=x82-1, x83'=x83+1;
x83 >= 1, x251 >= 1 -> x83'=x83-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x83 >= 1 -> x83'=x83-1, x84'=x84+1;
x84 >= 1, x251 >= 1 -> x84'=x84-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x84 >= 1 -> x84'=x84-1, x85'=x85+1;
x85 >= 1, x251 >= 1 -> x85'=x85-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x85 >= 1 -> x85'=x85-1, x86'=x86+1;
x86 >= 1, x251 >= 1 -> x86'=x86-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x86 >= 1 -> x86'=x86-1, x87'=x87+1;
x87 >= 1, x251 >= 1 -> x87'=x87-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x87 >= 1 -> x87'=x87-1, x88'=x88+1;
x88 >= 1, x251 >= 1 -> x88'=x88-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x88 >= 1 -> x88'=x88-1, x89'=x89+1;
x89 >= 1, x251 >= 1 -> x89'=x89-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x89 >= 1 -> x89'=x89-1, x90'=x90+1;
x90 >= 1, x251 >= 1 -> x90'=x90-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x90 >= 1 -> x90'=x90-1, x91'=x91+1;
x91 >= 1, x251 >= 1 -> x91'=x91-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x91 >= 1 -> x91'=x91-1, x92'=x92+1;
x92 >= 1, x251 >= 1 -> x92'=x92-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x92 >= 1 -> x92'=x92-1, x93'=x93+1;
x93 >= 1, x251 >= 1 -> x93'=x93-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x93 >= 1 -> x93'=x93-1, x94'=x94+1;
x94 >= 1, x251 >= 1 -> x94'=x94-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x94 >= 1 -> x94'=x94-1, x95'=x95+1;
x95 >= 1, x251 >= 1 -> x95'=x95-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x95 >= 1 -> x95'=x95-1, x96'=x96+1;
x96 >= 1, x251 >= 1 -> x96'=x96-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x96 >= 1 -> x96'=x96-1, x97'=x97+1;
x97 >= 1, x251 >= 1 -> x97'=x97-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x97 >= 1 -> x97'=x97-1, x98'=x98+1;
x98 >= 1, x251 >= 1 -> x98'=x98-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x98 >= 1 -> x98'=x98-1, x99'=x99+1;
x99 >= 1, x251 >= 1 -> x99'=x99-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x99 >= 1 -> x99'=x99-1, x100'=x100+1;
x100 >= 1, x251 >= 1 -> x100'=x100-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x100 >= 1 -> x100'=x100-1, x101'=x101+1;
x101 >= 1, x251 >= 1 -> x101'=x101-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x101 >= 1 -> x101'=x101-1, x102'=x102+1;
x102 >= 1, x251 >= 1 -> x102'=x102-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x102 >= 1 -> x102'=x102-1, x103'=x103+1;
x103 >= 1, x251 >= 1 -> x103'=x103-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x103 >= 1 -> x103'=x103-1, x104'=x104+1;
x104 >= 1, x251 >= 1 -> x104'=x104-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x104 >= 1 -> x104'=x104-1, x105'=x105+1;
x105 >= 1, x251 >= 1 -> x105'=x105-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x105 >= 1 -> x105'=x105-1, x106'=x106+1;
x106 >= 1, x251 >= 1 -> x106'=x106-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x106 >= 1 -> x106'=x106-1, x107'=x107+1;
x107 >= 1, x251 >= 1 -> x107'=x107-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x107 >= 1 -> x107'=x107-1, x108'=x108+1;
x108 >= 1, x251 >= 1 -> x108'=x108-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x108 >= 1 -> x108'=x108-1, x109'=x109+1;
x109 >= 1, x251 >= 1 -> x109'=x109-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x109 >= 1 -> x109'=x109-1, x110'=x110+1;
x110 >= 1, x251 >= 1 -> x110'=x110-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x110 >= 1 -> x110'=x110-1, x111'=x111+1;
x111 >= 1, x251 >= 1 -> x111'=x111-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x111 >= 1 -> x111'=x111-1, x112'=x112+1;
x112 >= 1, x251 >= 1 -> x112'=x112-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x112 >= 1 -> x112'=x112-1, x113'=x113+1;
x113 >= 1, x251 >= 1 -> x113'=x113-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x113 >= 1 -> x113'=x113-1, x114'=x114+1;
x114 >= 1, x251 >= 1 -> x114'=x114-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x114 >= 1 -> x114'=x114-1, x115'=x115+1;
x115 >= 1, x251 >= 1 -> x115'=x115-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x115 >= 1 -> x115'=x115-1, x116'=x116+1;
x116 >= 1, x251 >= 1 -> x116'=x116-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x116 >= 1 -> x116'=x116-1, x117'=x117+1;
x117 >= 1, x251 >= 1 -> x117'=x117-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x117 >= 1 -> x117'=x117-1, x118'=x118+1;
x118 >= 1, x251 >= 1 -> x118'=x118-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x118 >= 1 -> x118'=x118-1, x119'=x119+1;
x119 >= 1, x251 >= 1 -> x119'=x119-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x119 >= 1 -> x119'=x119-1, x120'=x120+1;
x120 >= 1, x251 >= 1 -> x120'=x120-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x120 >= 1 -> x120'=x120-1, x121'=x121+1;
x121 >= 1, x251 >= 1 -> x121'=x121-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x121 >= 1 -> x121'=x121-1, x122'=x122+1;
x122 >= 1, x251 >= 1 -> x122'=x122-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x122 >= 1 -> x122'=x122-1, x123'=x123+1;
x123 >= 1, x251 >= 1 -> x123'=x123-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x123 >= 1 -> x123'=x123-1, x124'=x124+1;
x124 >= 1, x251 >= 1 -> x124'=x124-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x124 >= 1 -> x124'=x124-1, x125'=x125+1;
x125 >= 1, x251 >= 1 -> x125'=x125-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x125 >= 1 -> x125'=x125-1, x126'=x126+1;
x126 >= 1, x251 >= 1 -> x126'=x126-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x126 >= 1 -> x126'=x126-1, x127'=x127+1;
x127 >= 1, x251 >= 1 -> x127'=x127-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x127 >= 1 -> x127'=x127-1, x128'=x128+1;
x128 >= 1, x251 >= 1 -> x128'=x128-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x128 >= 1 -> x128'=x128-1, x129'=x129+1;
x129 >= 1, x251 >= 1 -> x129'=x129-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x129 >= 1 -> x129'=x129-1, x130'=x130+1;
x130 >= 1, x251 >= 1 -> x130'=x130-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x130 >= 1 -> x130'=x130-1, x131'=x131+1;
x131 >= 1, x251 >= 1 -> x131'=x131-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x131 >= 1 -> x131'=x131-1, x132'=x132+1;
x132 >= 1, x251 >= 1 -> x132'=x132-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x132 >= 1 -> x132'=x132-1, x133'=x133+1;
x133 >= 1, x251 >= 1 -> x133'=x133-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x133 >= 1 -> x133'=x133-1, x134'=x134+1;
x134 >= 1, x251 >= 1 -> x134'=x134-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x134 >= 1 -> x134'=x134-1, x135'=x135+1;
x135 >= 1, x251 >= 1 -> x135'=x135-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x135 >= 1 -> x135'=x135-1, x136'=x136+1;
x136 >= 1, x251 >= 1 -> x136'=x136-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x136 >= 1 -> x136'=x136-1, x137'=x137+1;
x137 >= 1, x251 >= 1 -> x137'=x137-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x137 >= 1 -> x137'=x137-1, x138'=x138+1;
x138 >= 1, x251 >= 1 -> x138'=x138-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x138 >= 1 -> x138'=x138-1, x139'=x139+1;
x139 >= 1, x251 >= 1 -> x139'=x139-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x139 >= 1 -> x139'=x139-1, x140'=x140+1;
x140 >= 1, x251 >= 1 -> x140'=x140-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x140 >= 1 -> x140'=x140-1, x141'=x141+1;
x141 >= 1, x251 >= 1 -> x141'=x141-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x141 >= 1 -> x141'=x141-1, x142'=x142+1;
x142 >= 1, x251 >= 1 -> x142'=x142-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x142 >= 1 -> x142'=x142-1, x143'=x143+1;
x143 >= 1, x251 >= 1 -> x143'=x143-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x143 >= 1 -> x143'=x143-1, x144'=x144+1;
x144 >= 1, x251 >= 1 -> x144'=x144-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x144 >= 1 -> x144'=x144-1, x145'=x145+1;
x145 >= 1, x251 >= 1 -> x145'=x145-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x145 >= 1 -> x145'=x145-1, x146'=x146+1;
x146 >= 1, x251 >= 1 -> x146'=x146-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x146 >= 1 -> x146'=x146-1, x147'=x147+1;
x147 >= 1, x251 >= 1 -> x147'=x147-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x147 >= 1 -> x147'=x147-1, x148'=x148+1;
x148 >= 1, x251 >= 1 -> x148'=x148-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x148 >= 1 -> x148'=x148-1, x149'=x149+1;
x149 >= 1, x251 >= 1 -> x149'=x149-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x149 >= 1 -> x149'=x149-1, x150'=x150+1;
x150 >= 1, x251 >= 1 -> x150'=x150-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x150 >= 1 -> x150'=x150-1, x151'=x151+1;
x151 >= 1, x251 >= 1 -> x151'=x151-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x151 >= 1 -> x151'=x151-1, x152'=x152+1;
x152 >= 1, x251 >= 1 -> x152'=x152-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x152 >= 1 -> x152'=x152-1, x153'=x153+1;
x153 >= 1, x251 >= 1 -> x153'=x153-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x153 >= 1 -> x153'=x153-1, x154'=x154+1;
x154 >= 1, x251 >= 1 -> x154'=x154-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x154 >= 1 -> x154'=x154-1, x155'=x155+1;
x155 >= 1, x251 >= 1 -> x155'=x155-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x155 >= 1 -> x155'=x155-1, x156'=x156+1;
x156 >= 1, x251 >= 1 -> x156'=x156-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x156 >= 1 -> x156'=x156-1, x157'=x157+1;
x157 >= 1, x251 >= 1 -> x157'=x157-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x157 >= 1 -> x157'=x157-1, x158'=x158+1;
x158 >= 1, x251 >= 1 -> x158'=x158-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x158 >= 1 -> x158'=x158-1, x159'=x159+1;
x159 >= 1, x251 >= 1 -> x159'=x159-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x159 >= 1 -> x159'=x159-1, x160'=x160+1;
x160 >= 1, x251 >= 1 -> x160'=x160-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x160 >= 1 -> x160'=x160-1, x161'=x161+1;
x161 >= 1, x251 >= 1 -> x161'=x161-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x161 >= 1 -> x161'=x161-1, x162'=x162+1;
x162 >= 1, x251 >= 1 -> x162'=x162-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x162 >= 1 -> x162'=x162-1, x163'=x163+1;
x163 >= 1, x251 >= 1 -> x163'=x163-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x163 >= 1 -> x163'=x163-1, x164'=x164+1;
x164 >= 1, x251 >= 1 -> x164'=x164-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x164 >= 1 -> x164'=x164-1, x165'=x165+1;
x165 >= 1, x251 >= 1 -> x165'=x165-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x165 >= 1 -> x165'=x165-1, x166'=x166+1;
x166 >= 1, x251 >= 1 -> x166'=x166-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x166 >= 1 -> x166'=x166-1, x167'=x167+1;
x167 >= 1, x251 >= 1 -> x167'=x167-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x167 >= 1 -> x167'=x167-1, x168'=x168+1;
x168 >= 1, x251 >= 1 -> x168'=x168-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x168 >= 1 -> x168'=x168-1, x169'=x169+1;
x169 >= 1, x251 >= 1 -> x169'=x169-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x169 >= 1 -> x169'=x169-1, x170'=x170+1;
x170 >= 1, x251 >= 1 -> x170'=x170-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x170 >= 1 -> x170'=x170-1, x171'=x171+1;
x171 >= 1, x251 >= 1 -> x171'=x171-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x171 >= 1 -> x171'=x171-1, x172'=x172+1;
x172 >= 1, x251 >= 1 -> x172'=x172-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x172 >= 1 -> x172'=x172-1, x173'=x173+1;
x173 >= 1, x251 >= 1 -> x173'=x173-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x173 >= 1 -> x173'=x173-1, x174'=x174+1;
x174 >= 1, x251 >= 1 -> x174'=x174-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x174 >= 1 -> x174'=x174-1, x175'=x175+1;
x175 >= 1, x251 >= 1 -> x175'=x175-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x175 >= 1 -> x175'=x175-1, x176'=x176+1;
x176 >= 1, x251 >= 1 -> x176'=x176-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x176 >= 1 -> x176'=x176-1, x177'=x177+1;
x177 >= 1, x251 >= 1 -> x177'=x177-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x177 >= 1 -> x177'=x177-1, x178'=x178+1;
x178 >= 1, x251 >= 1 -> x178'=x178-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x178 >= 1 -> x178'=x178-1, x179'=x179+1;
x179 >= 1, x251 >= 1 -> x179'=x179-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x179 >= 1 -> x179'=x179-1, x180'=x180+1;
x180 >= 1, x251 >= 1 -> x180'=x180-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x180 >= 1 -> x180'=x180-1, x181'=x181+1;
x181 >= 1, x251 >= 1 -> x181'=x181-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x181 >= 1 -> x181'=x181-1, x182'=x182+1;
x182 >= 1, x251 >= 1 -> x182'=x182-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x182 >= 1 -> x182'=x182-1, x183'=x183+1;
x183 >= 1, x251 >= 1 -> x183'=x183-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x183 >= 1 -> x183'=x183-1, x184'=x184+1;
x184 >= 1, x251 >= 1 -> x184'=x184-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x184 >= 1 -> x184'=x184-1, x185'=x185+1;
x185 >= 1, x251 >= 1 -> x185'=x185-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x185 >= 1 -> x185'=x185-1, x186'=x186+1;
x186 >= 1, x251 >= 1 -> x186'=x186-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x186 >= 1 -> x186'=x186-1, x187'=x187+1;
x187 >= 1, x251 >= 1 -> x187'=x187-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x187 >= 1 -> x187'=x187-1, x188'=x188+1;
x188 >= 1, x251 >= 1 -> x188'=x188-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x188 >= 1 -> x188'=x188-1, x189'=x189+1;
x189 >= 1, x251 >= 1 -> x189'=x189-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x189 >= 1 -> x189'=x189-1, x190'=x190+1;
x190 >= 1, x251 >= 1 -> x190'=x190-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x190 >= 1 -> x190'=x190-1, x191'=x191+1;
x191 >= 1, x251 >= 1 -> x191'=x191-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x191 >= 1 -> x191'=x191-1, x192'=x192+1;
x192 >= 1, x251 >= 1 -> x192'=x192-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x192 >= 1 -> x192'=x192-1, x193'=x193+1;
x193 >= 1, x251 >= 1 -> x193'=x193-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x193 >= 1 -> x193'=x193-1, x194'=x194+1;
x194 >= 1, x251 >= 1 -> x194'=x194-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x194 >= 1 -> x194'=x194-1, x195'=x195+1;
x195 >= 1, x251 >= 1 -> x195'=x195-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x195 >= 1 -> x195'=x195-1, x196'=x196+1;
x196 >= 1, x251 >= 1 -> x196'=x196-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x196 >= 1 -> x196'=x196-1, x197'=x197+1;
x197 >= 1, x251 >= 1 -> x197'=x197-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x197 >= 1 -> x197'=x197-1, x198'=x198+1;
x198 >= 1, x251 >= 1 -> x198'=x198-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x198 >= 1 -> x198'=x198-1, x199'=x199+1;
x199 >= 1, x251 >= 1 -> x199'=x199-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x199 >= 1 -> x199'=x199-1, x200'=x200+1;
x200 >= 1, x251 >= 1 -> x200'=x200-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x200 >= 1 -> x200'=x200-1, x201'=x201+1;
x201 >= 1, x251 >= 1 -> x201'=x201-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x201 >= 1 -> x201'=x201-1, x202'=x202+1;
x202 >= 1, x251 >= 1 -> x202'=x202-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x202 >= 1 -> x202'=x202-1, x203'=x203+1;
x203 >= 1, x251 >= 1 -> x203'=x203-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x203 >= 1 -> x203'=x203-1, x204'=x204+1;
x204 >= 1, x251 >= 1 -> x204'=x204-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x204 >= 1 -> x204'=x204-1, x205'=x205+1;
x205 >= 1, x251 >= 1 -> x205'=x205-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x205 >= 1 -> x205'=x205-1, x206'=x206+1;
x206 >= 1, x251 >= 1 -> x206'=x206-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x206 >= 1 -> x206'=x206-1, x207'=x207+1;
x207 >= 1, x251 >= 1 -> x207'=x207-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x207 >= 1 -> x207'=x207-1, x208'=x208+1;
x208 >= 1, x251 >= 1 -> x208'=x208-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x208 >= 1 -> x208'=x208-1, x209'=x209+1;
x209 >= 1, x251 >= 1 -> x209'=x209-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x209 >= 1 -> x209'=x209-1, x210'=x210+1;
x210 >= 1, x251 >= 1 -> x210'=x210-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x210 >= 1 -> x210'=x210-1, x211'=x211+1;
x211 >= 1, x251 >= 1 -> x211'=x211-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x211 >= 1 -> x211'=x211-1, x212'=x212+1;
x212 >= 1, x251 >= 1 -> x212'=x212-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x212 >= 1 -> x212'=x212-1, x213'=x213+1;
x213 >= 1, x251 >= 1 -> x213'=x213-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x213 >= 1 -> x213'=x213-1, x214'=x214+1;
x214 >= 1, x251 >= 1 -> x214'=x214-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x214 >= 1 -> x214'=x214-1, x215'=x215+1;
x215 >= 1, x251 >= 1 -> x215'=x215-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x215 >= 1 -> x215'=x215-1, x216'=x216+1;
x216 >= 1, x251 >= 1 -> x216'=x216-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x216 >= 1 -> x216'=x216-1, x217'=x217+1;
x217 >= 1, x251 >= 1 -> x217'=x217-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x217 >= 1 -> x217'=x217-1, x218'=x218+1;
x218 >= 1, x251 >= 1 -> x218'=x218-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x218 >= 1 -> x218'=x218-1, x219'=x219+1;
x219 >= 1, x251 >= 1 -> x219'=x219-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x219 >= 1 -> x219'=x219-1, x220'=x220+1;
x220 >= 1, x251 >= 1 -> x220'=x220-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x220 >= 1 -> x220'=x220-1, x221'=x221+1;
x221 >= 1, x251 >= 1 -> x221'=x221-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x221 >= 1 -> x221'=x221-1, x222'=x222+1;
x222 >= 1, x251 >= 1 -> x222'=x222-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x222 >= 1 -> x222'=x222-1, x223'=x223+1;
x223 >= 1, x251 >= 1 -> x223'=x223-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x223 >= 1 -> x223'=x223-1, x224'=x224+1;
x224 >= 1, x251 >= 1 -> x224'=x224-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x224 >= 1 -> x224'=x224-1, x225'=x225+1;
x225 >= 1, x251 >= 1 -> x225'=x225-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x225 >= 1 -> x225'=x225-1, x226'=x226+1;
x226 >= 1, x251 >= 1 -> x226'=x226-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x226 >= 1 -> x226'=x226-1, x227'=x227+1;
x227 >= 1, x251 >= 1 -> x227'=x227-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x227 >= 1 -> x227'=x227-1, x228'=x228+1;
x228 >= 1, x251 >= 1 -> x228'=x228-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x228 >= 1 -> x228'=x228-1, x229'=x229+1;
x229 >= 1, x251 >= 1 -> x229'=x229-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x229 >= 1 -> x229'=x229-1, x230'=x230+1;
x230 >= 1, x251 >= 1 -> x230'=x230-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x230 >= 1 -> x230'=x230-1, x231'=x231+1;
x231 >= 1, x251 >= 1 -> x231'=x231-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x231 >= 1 -> x231'=x231-1, x232'=x232+1;
x232 >= 1, x251 >= 1 -> x232'=x232-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x232 >= 1 -> x232'=x232-1, x233'=x233+1;
x233 >= 1, x251 >= 1 -> x233'=x233-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x233 >= 1 -> x233'=x233-1, x234'=x234+1;
x234 >= 1, x251 >= 1 -> x234'=x234-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x234 >= 1 -> x234'=x234-1, x235'=x235+1;
x235 >= 1, x251 >= 1 -> x235'=x235-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x235 >= 1 -> x235'=x235-1, x236'=x236+1;
x236 >= 1, x251 >= 1 -> x236'=x236-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x236 >= 1 -> x236'=x236-1, x237'=x237+1;
x237 >= 1, x251 >= 1 -> x237'=x237-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x237 >= 1 -> x237'=x237-1, x238'=x238+1;
x238 >= 1, x251 >= 1 -> x238'=x238-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x238 >= 1 -> x238'=x238-1, x239'=x239+1;
x239 >= 1, x251 >= 1 -> x239'=x239-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x239 >= 1 -> x239'=x239-1, x240'=x240+1;
x240 >= 1, x251 >= 1 -> x240'=x240-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x240 >= 1 -> x240'=x240-1, x241'=x241+1;
x241 >= 1, x251 >= 1 -> x241'=x241-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x241 >= 1 -> x241'=x241-1, x242'=x242+1;
x242 >= 1, x251 >= 1 -> x242'=x242-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x242 >= 1 -> x242'=x242-1, x243'=x243+1;
x243 >= 1, x251 >= 1 -> x243'=x243-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x243 >= 1 -> x243'=x243-1, x244'=x244+1;
x244 >= 1, x251 >= 1 -> x244'=x244-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x244 >= 1 -> x244'=x244-1, x245'=x245+1;
x245 >= 1, x251 >= 1 -> x245'=x245-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x245 >= 1 -> x245'=x245-1, x246'=x246+1;
x246 >= 1, x251 >= 1 -> x246'=x246-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x246 >= 1 -> x246'=x246-1, x247'=x247+1;
x247 >= 1, x251 >= 1 -> x247'=x247-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x247 >= 1 -> x247'=x247-1, x248'=x248+1;
x248 >= 1, x251 >= 1 -> x248'=x248-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x248 >= 1 -> x248'=x248-1, x249'=x249+1;
x249 >= 1, x251 >= 1 -> x249'=x249-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;
x249 >= 1 -> x249'=x249-1, x250'=x250+1;
x250 >= 1, x251 >= 1 -> x250'=x250-1, x251'=x251-1, x0'=x0+1, x252'=x252+1;

init
x0 >= 1, x1 = 0, x2 = 0, x3 = 0, x4 = 0, x5 = 0, x6 = 0, x7 = 0, x8 = 0, x9 = 0, x10 = 0, x11 = 0, x12 = 0, x13 = 0, x14 = 0, x15 = 0, x16 = 0, x17 = 0, x18 = 0, x19 = 0, x20 = 0, x21 = 0, x22 = 0, x23 = 0, x24 = 0, x25 = 0, x26 = 0, x27 = 0, x28 = 0, x29 = 0, x30 = 0, x31 = 0, x32 = 0, x33 = 0, x34 = 0, x35 = 0, x36 = 0, x37 = 0, x38 = 0, x39 = 0, x40 = 0, x41 = 0, x42 = 0, x43 = 0, x44 = 0, x45 = 0, x46 = 0, x47 = 0, x48 = 0, x49 = 0, x50 = 0, x51 = 0, x52 = 0, x53 = 0, x54 = 0, x55 = 0, x56 = 0, x57 = 0, x58 = 0, x59 = 0, x60 = 0, x61 = 0, x62 = 0, x63 = 0, x64 = 0, x65 = 0, x66 = 0, x67 = 0, x68 = 0, x69 = 0, x70 = 0, x71 = 0, x72 = 0, x73 = 0, x74 = 0, x75 = 0, x76 = 0, x77 = 0, x78 = 0, x79 = 0, x80 = 0, x81 = 0, x82 = 0, x83 = 0, x84 = 0, x85 = 0, x86 = 0, x87 = 0, x88 = 0, x89 = 0, x90 = 0, x91 = 0, x92 = 0, x93 = 0, x94 = 0, x95 = 0, x96 = 0, x97 = 0, x98 = 0, x99 = 0, x100 = 0, x101 = 0, x102 = 0, x103 = 0, x104 = 0, x105 = 0, x106 = 0, x107 = 0, x108 = 0, x109 = 0, x110 = 0, x111 = 0, x112 = 0, x113 = 0, x114 = 0, x115 = 0, x116 = 0, x117 = 0, x118 = 0, x119 = 0, x120 = 0, x121 = 0, x122 = 0, x123 = 0, x124 = 0, x125 = 0, x126 = 0, x127 = 0, x128 = 0, x129 = 0, x130 = 0, x131 = 0, x132 = 0, x133 = 0, x134 = 0, x135 = 0, x136 = 0, x137 = 0, x138 = 0, x139 = 0, x140 = 0, x141 = 0, x142 = 0, x143 = 0, x144 = 0, x145 = 0, x146 = 0, x147 = 0, x148 = 0, x149 = 0, x150 = 0, x151 = 0, x152 = 0, x153 = 0, x154 = 0, x155 = 0, x156 = 0, x157 = 0, x158 = 0, x159 = 0, x160 = 0, x161 = 0, x162 = 0, x163 = 0, x164 = 0, x165 = 0, x166 = 0, x167 = 0, x168 = 0, x169 = 0, x170 = 0, x171 = 0, x172 = 0, x173 = 0, x174 = 0, x175 = 0, x176 = 0, x177 = 0, x178 = 0, x179 = 0, x180 = 0, x181 = 0, x182 = 0, x183 = 0, x184 = 0, x185 = 0, x186 = 0, x187 = 0, x188 = 0, x189 = 0, x190 = 0, x191 = 0, x192 = 0, x193 = 0, x194 = 0, x195 = 0, x196 = 0, x197 = 0, x198 = 0, x199 = 0, x200 = 0, x201 = 0, x202 = 0, x203 = 0, x204 = 0, x205 = 0, x206 = 0, x207 = 0, x208 = 0, x209 = 0, x210 = 0, x211 = 0, x212 = 0, x213 = 0, x214 = 0, x215 = 0, x216 = 0, x217 = 0, x218 = 0, x219 = 0, x220 = 0, x221 = 0, x222 = 0, x223 = 0, x224 = 0, x225 = 0, x226 = 0, x227 = 0, x228 = 0, x229 = 0, x230 = 0, x231 = 0, x232 = 0, x233 = 0, x234 = 0, x235 = 0, x236 = 0, x237 = 0, x238 = 0, x239 = 0, x240 = 0, x241 = 0, x242 = 0, x243 = 0, x244 = 0, x245 = 0, x246 = 0, x247 = 0, x248 = 0, x249 = 0, x250 = 0, x251 = 0, x252 = 1

target
x250 >= 2