LP file converted from wpms_random/wpmax3sat/hi/file_rwpms_wcnf_L3_V100_C600_H100_0.wcnf of MAX-SAT Evaluation 2011 Benchmark

file_rwpms_wcnf_L3_V100_C600_H100_0.wcnf

c Weighted CNF
c from Selman's wff generator
p wcnf 100 600 3237
3237 2 5 30 0
3237 -68 -41 -22 0
3237 62 -58 9 0
3237 77 -70 42 0
3237 -94 -17 -26 0
3237 -72 84 2 0
3237 51 60 39 0
3237 83 90 -37 0
3237 92 -14 97 0
3237 -25 -7 51 0
3237 -54 48 14 0
3237 72 82 93 0
3237 -38 86 -15 0
3237 30 93 -73 0
3237 52 50 69 0
3237 33 86 93 0
3237 -79 12 5 0
3237 96 60 -93 0
3237 69 -65 87 0
3237 -3 42 -60 0
3237 17 77 10 0
3237 -2 -29 37 0
3237 -69 10 37 0
3237 -47 -9 17 0
3237 -91 -41 -86 0
3237 -79 -62 -53 0
3237 -21 -87 98 0
3237 2 29 58 0
3237 -70 54 10 0
3237 -13 -32 48 0
3237 75 -72 -94 0
3237 -97 81 65 0
3237 -42 -40 -52 0
3237 100 48 -13 0
3237 -17 46 -85 0
3237 -97 19 50 0
3237 69 42 90 0
3237 57 -76 67 0
3237 -68 -74 93 0
3237 33 -100 72 0
3237 96 -61 -33 0
3237 54 -20 -19 0
3237 70 9 30 0
3237 -82 -85 -78 0
3237 -100 98 60 0
3237 86 -10 85 0
3237 96 8 56 0
3237 -69 -20 17 0
3237 -1 37 -19 0
3237 -39 -11 -80 0
3237 22 -67 -4 0
3237 -43 -80 65 0
3237 5 -63 -34 0
3237 -55 61 26 0
3237 55 -77 48 0
3237 28 98 -95 0
3237 -89 46 -59 0
3237 68 -48 -15 0
3237 91 -23 -35 0
3237 -53 50 100 0
3237 12 23 43 0
3237 72 60 -84 0
3237 63 -26 53 0
3237 54 35 59 0
3237 -99 -58 11 0
3237 94 5 -62 0
3237 -67 3 22 0
3237 -2 80 -60 0
3237 -98 64 94 0
3237 -69 -11 58 0
3237 -18 87 -44 0
3237 -41 89 -77 0
3237 -96 -41 -73 0
3237 14 93 -47 0
3237 -7 -18 -70 0
3237 3 -15 -50 0
3237 -21 -35 -61 0
3237 -91 92 41 0
3237 -46 -60 -29 0
3237 51 72 -96 0
3237 83 -39 7 0
3237 -4 6 35 0
3237 65 -93 -23 0
3237 -40 -2 -28 0
3237 47 -44 -65 0
3237 35 -46 38 0
3237 -42 82 28 0
3237 7 10 -23 0
3237 97 54 -80 0
3237 17 -69 -81 0
3237 -46 26 19 0
3237 29 84 -69 0
3237 11 -40 22 0
3237 -36 8 -80 0
3237 -77 99 69 0
3237 -38 56 -74 0
3237 -98 -72 -61 0
3237 -66 87 -30 0
3237 -88 63 90 0
3237 -20 -99 18 0
3 36 94 83 0
10 86 48 -96 0
10 -36 -80 -59 0
7 47 -54 -37 0
4 40 67 75 0
10 -63 -15 84 0
10 58 12 -3 0
5 38 -5 33 0
9 -49 25 64 0
6 42 84 98 0
7 -17 74 -35 0
8 8 3 11 0
8 85 43 41 0
9 -34 -93 -35 0
6 29 20 -63 0
8 -46 -53 -48 0
3 -79 -60 -95 0
9 -25 -54 -42 0
9 76 5 -79 0
5 -90 -31 76 0
7 -27 -3 63 0
4 -66 -62 74 0
7 60 75 -97 0
3 -88 16 -73 0
10 -22 -16 -6 0
7 -8 -95 66 0
4 -86 -35 -9 0
5 -3 -55 -34 0
7 68 44 89 0
4 14 -30 -20 0
1 34 -92 -47 0
10 90 -95 -4 0
4 -52 -44 -96 0
1 -18 -43 -57 0
7 -72 81 -99 0
8 72 40 89 0
1 13 -34 43 0
7 -78 -34 -75 0
2 -41 -2 -17 0
10 -68 30 -48 0
2 -63 92 94 0
8 99 22 -71 0
7 73 -15 -87 0
9 21 28 73 0
6 -5 -93 -61 0
2 -6 -21 -72 0
6 36 70 4 0
9 60 83 55 0
10 -17 -51 -70 0
5 -20 93 87 0
3 61 50 65 0
7 14 -84 5 0
8 58 -50 98 0
10 55 13 -79 0
9 19 22 59 0
8 51 -63 -52 0
6 -52 9 -84 0
3 -71 -83 24 0
2 -97 -50 32 0
3 -41 -93 -55 0
7 -2 -49 19 0
3 54 -16 22 0
3 11 42 29 0
10 -54 -7 74 0
3 -20 22 40 0
10 31 -23 -87 0
7 -62 -31 67 0
4 -29 79 -80 0
6 -82 -67 -97 0
8 1 73 99 0
3 -78 77 43 0
8 -15 -88 50 0
6 -19 -99 96 0
9 -88 -38 76 0
7 -61 93 1 0
2 80 -11 24 0
1 -41 -90 37 0
3 8 -90 -6 0
10 -12 -75 -100 0
1 16 -19 84 0
7 -64 -58 28 0
3 -38 21 -92 0
7 -81 18 51 0
4 49 33 -13 0
3 40 -35 -89 0
6 -40 15 25 0
1 -69 40 24 0
9 -22 -95 -53 0
8 11 -29 5 0
3 -93 16 59 0
1 -48 79 25 0
4 -76 -14 -67 0
5 -34 -95 -75 0
4 -59 78 -84 0
4 88 -93 76 0
7 -57 -22 93 0
3 -9 -69 52 0
10 55 -3 -20 0
10 -84 47 -65 0
9 27 98 58 0
8 16 -1 52 0
3 -46 -90 -14 0
6 22 19 -85 0
4 -29 -32 20 0
1 59 25 -27 0
2 -46 42 -71 0
5 -43 -95 42 0
1 39 -13 -24 0
4 96 -83 3 0
5 -44 34 -25 0
1 42 -95 93 0
10 65 -36 37 0
8 11 -31 -41 0
8 6 -49 -77 0
4 9 -7 87 0
10 -85 19 31 0
3 -19 -95 58 0
5 83 11 80 0
8 -18 -51 82 0
1 47 68 51 0
7 -69 -85 -46 0
9 -21 80 -70 0
4 29 18 80 0
1 42 -59 75 0
3 67 100 1 0
8 -45 -1 86 0
7 66 -20 -27 0
5 -6 28 80 0
8 -10 -77 79 0
7 18 -66 -31 0
3 20 27 -64 0
6 52 -83 79 0
10 25 8 19 0
9 20 18 4 0
9 -84 80 -41 0
10 93 -7 65 0
1 93 51 95 0
3 36 -40 -54 0
1 -64 3 -10 0
4 89 -4 -38 0
8 -89 -62 -87 0
2 -70 -64 6 0
4 -98 -10 -77 0
5 -44 -18 -62 0
9 11 74 -86 0
8 28 91 -17 0
5 -69 -13 52 0
2 -12 75 -36 0
2 48 69 -9 0
3 -91 -32 -68 0
2 30 8 61 0
8 -34 -90 -17 0
1 12 -76 -67 0
6 38 11 -61 0
8 39 -10 -14 0
4 76 -16 100 0
3 -41 -95 -11 0
5 50 92 17 0
8 76 23 -69 0
10 -60 52 -64 0
2 -42 52 -56 0
1 -19 -9 -86 0
5 25 80 9 0
1 49 94 -45 0
9 69 75 -39 0
4 88 -82 27 0
1 19 -79 49 0
9 -65 78 16 0
6 95 -67 27 0
1 -26 -53 -16 0
3 -39 72 -38 0
4 -6 34 76 0
3 91 -2 6 0
7 -40 70 -91 0
9 8 -34 27 0
2 79 36 -83 0
4 -14 -7 -31 0
3 19 -51 70 0
3 48 -96 15 0
5 13 -70 -58 0
5 51 -71 -91 0
5 -31 -1 -98 0
2 -30 8 -9 0
6 -45 80 61 0
10 84 -29 -93 0
10 -96 -19 56 0
9 -77 83 42 0
3 33 -74 -40 0
4 -6 -18 -50 0
7 -89 60 -96 0
2 66 -96 82 0
5 63 58 -16 0
7 -37 64 32 0
7 -47 -10 -22 0
6 -63 65 -58 0
6 22 12 53 0
10 -37 -95 92 0
6 11 36 -87 0
5 -47 -57 -1 0
6 66 -16 -40 0
7 81 -96 97 0
7 -67 -35 23 0
9 -81 96 -58 0
9 -59 -84 -26 0
4 -35 17 -94 0
7 -60 -20 -63 0
10 85 -20 -96 0
7 -30 59 77 0
10 -55 85 99 0
3 -59 -78 67 0
1 -20 -12 -26 0
5 44 -52 -99 0
7 -20 -88 -35 0
3 11 30 -45 0
10 59 68 65 0
7 -31 39 -29 0
2 35 64 47 0
9 9 22 -94 0
9 4 29 98 0
6 36 96 -75 0
6 17 51 -33 0
10 -41 -40 18 0
1 -93 81 -41 0
2 -55 -27 87 0
7 60 10 19 0
6 -29 -26 -89 0
8 15 -11 35 0
7 -52 -91 87 0
1 50 -33 37 0
2 -59 -45 20 0
2 15 -9 55 0
7 98 85 37 0
9 38 -68 25 0
1 35 9 -72 0
6 -3 65 2 0
2 -94 53 85 0
8 94 8 -47 0
5 -63 -93 6 0
8 -22 61 -43 0
7 -75 -7 -27 0
8 -6 -80 23 0
9 2 -69 -52 0
1 28 55 69 0
5 -41 -64 -81 0
2 -45 31 -92 0
1 -41 13 57 0
1 -8 -4 -100 0
4 36 80 -48 0
10 25 54 53 0
9 -89 -82 39 0
9 -58 -94 14 0
5 65 64 45 0
9 -61 95 -85 0
10 -89 -61 26 0
7 -82 79 73 0
6 19 -25 75 0
5 77 -46 99 0
4 58 -31 9 0
2 15 -84 -76 0
6 75 58 -51 0
6 66 -37 -7 0
3 -76 -45 34 0
2 -89 -23 35 0
4 -12 79 -13 0
4 61 94 -47 0
8 -94 7 -2 0
5 88 -23 -14 0
1 -25 -85 -1 0
3 89 -93 -44 0
3 91 -41 -57 0
8 2 45 -5 0
10 -72 -32 -75 0
2 -65 78 55 0
8 -30 26 29 0
4 -36 -18 49 0
4 -91 -55 -45 0
9 48 30 -21 0
5 93 79 -50 0
7 83 74 12 0
9 -20 -82 56 0
4 -69 65 14 0
6 8 -51 -22 0
4 -22 45 -69 0
2 62 -43 -63 0
5 -90 37 51 0
10 -29 10 32 0
8 96 83 56 0
9 47 -93 94 0
4 67 -44 68 0
9 -11 41 85 0
4 80 33 -41 0
9 46 16 55 0
2 51 88 -96 0
6 69 -70 -20 0
2 -84 -10 11 0
5 99 -51 -48 0
3 -10 8 84 0
7 -67 58 12 0
5 -39 71 -83 0
5 29 -90 -91 0
10 -55 -11 -2 0
2 -3 -80 -52 0
5 -34 46 87 0
1 -33 18 -83 0
10 -19 -13 55 0
8 12 24 -26 0
4 81 -20 -78 0
9 -8 20 -11 0
3 -95 47 -76 0
1 -42 56 -11 0
8 10 25 4 0
6 33 -18 41 0
6 -76 -58 -47 0
1 45 46 8 0
8 19 -65 1 0
10 9 70 -38 0
10 -33 38 92 0
5 1 24 -100 0
8 8 -55 98 0
4 -61 93 85 0
4 74 30 15 0
2 -85 75 57 0
2 19 -49 29 0
5 -70 4 -94 0
7 -88 79 -60 0
3 18 12 -11 0
9 51 -7 -28 0
10 13 2 25 0
10 -81 -89 23 0
4 -41 43 -20 0
4 -81 -32 -70 0
9 -44 15 -99 0
6 -47 -35 83 0
8 90 57 -13 0
10 -71 87 73 0
6 51 -34 -1 0
6 -85 11 -91 0
4 -2 68 -54 0
4 -63 1 -44 0
9 29 -2 -75 0
4 32 -23 10 0
2 25 49 18 0
4 86 -7 -17 0
9 93 42 -61 0
2 -25 45 -93 0
2 -76 77 -88 0
8 93 33 100 0
2 -60 -33 -11 0
6 -37 -64 30 0
6 -89 24 90 0
5 46 -99 12 0
9 -84 -77 -53 0
7 -88 46 32 0
6 87 -60 -66 0
4 -63 46 90 0
4 -87 73 -11 0
9 -19 -89 -71 0
2 70 -61 3 0
4 -5 -46 84 0
9 36 -25 86 0
6 38 -64 -85 0
7 43 -80 78 0
7 -71 21 -11 0
1 -98 -27 -15 0
5 21 -33 -2 0
7 19 95 42 0
6 -92 -85 84 0
1 20 69 -54 0
10 99 38 -2 0
10 -90 40 -31 0
9 69 -66 83 0
3 -14 60 10 0
1 -30 -49 77 0
3 -60 -77 -56 0
1 -60 -78 -14 0
3 -79 37 -26 0
4 -86 -60 -53 0
9 -3 -86 31 0
4 -97 -30 -86 0
10 26 51 52 0
4 100 -19 56 0
8 -18 -65 62 0
8 -53 63 -3 0
1 -93 -39 -2 0
4 52 -16 -43 0
1 -23 -55 -3 0
5 81 -98 47 0
3 -60 21 68 0
3 35 -97 48 0
8 -29 26 54 0
1 -55 51 64 0
8 -39 -10 41 0
4 -90 -11 29 0
7 67 7 29 0
9 52 71 -28 0
9 -14 -96 7 0
3 -21 -91 -45 0
5 -69 65 -6 0
10 -30 89 85 0
3 -62 -54 98 0
4 -46 72 -35 0
9 88 69 -78 0
5 28 -99 19 0
5 -12 -26 29 0
1 23 47 85 0
5 -59 82 -14 0
7 -81 -21 -32 0
5 12 80 -60 0
3 -70 25 -81 0
1 30 -43 13 0
4 -58 22 -31 0
7 -34 -97 86 0
8 -25 -67 18 0
2 39 -67 -56 0
7 -86 95 -18 0
2 -47 67 3 0
2 42 71 -15 0
2 -66 60 36 0
4 -14 83 -98 0
5 -45 -88 -58 0
9 43 -33 -46 0
4 -51 -40 78 0
3 44 -34 82 0
3 40 -60 -11 0
1 53 50 -31 0
1 58 -67 -30 0
1 67 28 39 0
4 -91 -49 47 0
5 -87 15 84 0
1 71 -77 95 0
6 98 -49 -96 0
9 -27 -19 100 0
9 78 55 53 0
10 49 14 -42 0
4 -77 -81 42 0
10 -100 79 82 0
5 -68 -33 54 0
10 71 -76 -24 0
4 -49 12 -93 0
8 57 -2 100 0
1 27 -62 15 0
8 -90 -1 2 0
5 27 -73 -89 0
8 -1 22 98 0
9 -52 -58 20 0
2 -83 11 64 0
10 46 -22 32 0
10 -65 -5 -3 0
3 39 55 -97 0
3 -55 99 56 0
5 77 33 -52 0
1 72 75 -6 0
7 33 86 88 0
7 10 77 97 0
3 -5 68 -43 0
7 -1 -19 -24 0
7 36 32 28 0
4 25 68 -33 0
1 54 12 -47 0
2 94 -23 -28 0
4 -28 83 89 0
6 4 69 80 0
1 79 34 -82 0
3 82 1 96 0
6 89 -44 36 0
4 -86 -7 100 0
2 22 -62 3 0
1 -16 -71 -46 0
4 -81 -64 92 0
6 90 -82 -86 0
8 44 -83 72 0
4 -77 -78 -91 0
3 91 -94 54 0
2 28 72 -99 0
2 62 -38 -73 0
1 -12 7 53 0
3 13 27 -86 0
1 87 96 58 0
1 -76 -60 -19 0
5 66 -40 -4 0
4 -8 -98 73 0
5 -68 -94 -49 0
5 -18 85 -49 0
10 23 -100 40 0
2 8 -39 58 0
8 -78 85 42 0
7 73 -12 17 0
8 75 -83 100 0
1 4 81 -24 0
7 62 29 36 0
10 64 -18 97 0
5 28 -40 53 0
3 -60 -35 -1 0
10 84 62 -39 0
7 4 -66 90 0
9 53 -48 47 0
4 90 81 54 0
9 -60 85 49 0
9 -20 27 -69 0
7 19 -38 39 0

file_rwpms_wcnf_L3_V100_C600_H100_0.wcnf.lp

MINIMIZE
+ 3 z101
+ 10 z102
+ 10 z103
+ 7 z104
+ 4 z105
+ 10 z106
+ 10 z107
+ 5 z108
+ 9 z109
+ 6 z110
+ 7 z111
+ 8 z112
+ 8 z113
+ 9 z114
+ 6 z115
+ 8 z116
+ 3 z117
+ 9 z118
+ 9 z119
+ 5 z120
+ 7 z121
+ 4 z122
+ 7 z123
+ 3 z124
+ 10 z125
+ 7 z126
+ 4 z127
+ 5 z128
+ 7 z129
+ 4 z130
+ 1 z131
+ 10 z132
+ 4 z133
+ 1 z134
+ 7 z135
+ 8 z136
+ 1 z137
+ 7 z138
+ 2 z139
+ 10 z140
+ 2 z141
+ 8 z142
+ 7 z143
+ 9 z144
+ 6 z145
+ 2 z146
+ 6 z147
+ 9 z148
+ 10 z149
+ 5 z150
+ 3 z151
+ 7 z152
+ 8 z153
+ 10 z154
+ 9 z155
+ 8 z156
+ 6 z157
+ 3 z158
+ 2 z159
+ 3 z160
+ 7 z161
+ 3 z162
+ 3 z163
+ 10 z164
+ 3 z165
+ 10 z166
+ 7 z167
+ 4 z168
+ 6 z169
+ 8 z170
+ 3 z171
+ 8 z172
+ 6 z173
+ 9 z174
+ 7 z175
+ 2 z176
+ 1 z177
+ 3 z178
+ 10 z179
+ 1 z180
+ 7 z181
+ 3 z182
+ 7 z183
+ 4 z184
+ 3 z185
+ 6 z186
+ 1 z187
+ 9 z188
+ 8 z189
+ 3 z190
+ 1 z191
+ 4 z192
+ 5 z193
+ 4 z194
+ 4 z195
+ 7 z196
+ 3 z197
+ 10 z198
+ 10 z199
+ 9 z200
+ 8 z201
+ 3 z202
+ 6 z203
+ 4 z204
+ 1 z205
+ 2 z206
+ 5 z207
+ 1 z208
+ 4 z209
+ 5 z210
+ 1 z211
+ 10 z212
+ 8 z213
+ 8 z214
+ 4 z215
+ 10 z216
+ 3 z217
+ 5 z218
+ 8 z219
+ 1 z220
+ 7 z221
+ 9 z222
+ 4 z223
+ 1 z224
+ 3 z225
+ 8 z226
+ 7 z227
+ 5 z228
+ 8 z229
+ 7 z230
+ 3 z231
+ 6 z232
+ 10 z233
+ 9 z234
+ 9 z235
+ 10 z236
+ 1 z237
+ 3 z238
+ 1 z239
+ 4 z240
+ 8 z241
+ 2 z242
+ 4 z243
+ 5 z244
+ 9 z245
+ 8 z246
+ 5 z247
+ 2 z248
+ 2 z249
+ 3 z250
+ 2 z251
+ 8 z252
+ 1 z253
+ 6 z254
+ 8 z255
+ 4 z256
+ 3 z257
+ 5 z258
+ 8 z259
+ 10 z260
+ 2 z261
+ 1 z262
+ 5 z263
+ 1 z264
+ 9 z265
+ 4 z266
+ 1 z267
+ 9 z268
+ 6 z269
+ 1 z270
+ 3 z271
+ 4 z272
+ 3 z273
+ 7 z274
+ 9 z275
+ 2 z276
+ 4 z277
+ 3 z278
+ 3 z279
+ 5 z280
+ 5 z281
+ 5 z282
+ 2 z283
+ 6 z284
+ 10 z285
+ 10 z286
+ 9 z287
+ 3 z288
+ 4 z289
+ 7 z290
+ 2 z291
+ 5 z292
+ 7 z293
+ 7 z294
+ 6 z295
+ 6 z296
+ 10 z297
+ 6 z298
+ 5 z299
+ 6 z300
+ 7 z301
+ 7 z302
+ 9 z303
+ 9 z304
+ 4 z305
+ 7 z306
+ 10 z307
+ 7 z308
+ 10 z309
+ 3 z310
+ 1 z311
+ 5 z312
+ 7 z313
+ 3 z314
+ 10 z315
+ 7 z316
+ 2 z317
+ 9 z318
+ 9 z319
+ 6 z320
+ 6 z321
+ 10 z322
+ 1 z323
+ 2 z324
+ 7 z325
+ 6 z326
+ 8 z327
+ 7 z328
+ 1 z329
+ 2 z330
+ 2 z331
+ 7 z332
+ 9 z333
+ 1 z334
+ 6 z335
+ 2 z336
+ 8 z337
+ 5 z338
+ 8 z339
+ 7 z340
+ 8 z341
+ 9 z342
+ 1 z343
+ 5 z344
+ 2 z345
+ 1 z346
+ 1 z347
+ 4 z348
+ 10 z349
+ 9 z350
+ 9 z351
+ 5 z352
+ 9 z353
+ 10 z354
+ 7 z355
+ 6 z356
+ 5 z357
+ 4 z358
+ 2 z359
+ 6 z360
+ 6 z361
+ 3 z362
+ 2 z363
+ 4 z364
+ 4 z365
+ 8 z366
+ 5 z367
+ 1 z368
+ 3 z369
+ 3 z370
+ 8 z371
+ 10 z372
+ 2 z373
+ 8 z374
+ 4 z375
+ 4 z376
+ 9 z377
+ 5 z378
+ 7 z379
+ 9 z380
+ 4 z381
+ 6 z382
+ 4 z383
+ 2 z384
+ 5 z385
+ 10 z386
+ 8 z387
+ 9 z388
+ 4 z389
+ 9 z390
+ 4 z391
+ 9 z392
+ 2 z393
+ 6 z394
+ 2 z395
+ 5 z396
+ 3 z397
+ 7 z398
+ 5 z399
+ 5 z400
+ 10 z401
+ 2 z402
+ 5 z403
+ 1 z404
+ 10 z405
+ 8 z406
+ 4 z407
+ 9 z408
+ 3 z409
+ 1 z410
+ 8 z411
+ 6 z412
+ 6 z413
+ 1 z414
+ 8 z415
+ 10 z416
+ 10 z417
+ 5 z418
+ 8 z419
+ 4 z420
+ 4 z421
+ 2 z422
+ 2 z423
+ 5 z424
+ 7 z425
+ 3 z426
+ 9 z427
+ 10 z428
+ 10 z429
+ 4 z430
+ 4 z431
+ 9 z432
+ 6 z433
+ 8 z434
+ 10 z435
+ 6 z436
+ 6 z437
+ 4 z438
+ 4 z439
+ 9 z440
+ 4 z441
+ 2 z442
+ 4 z443
+ 9 z444
+ 2 z445
+ 2 z446
+ 8 z447
+ 2 z448
+ 6 z449
+ 6 z450
+ 5 z451
+ 9 z452
+ 7 z453
+ 6 z454
+ 4 z455
+ 4 z456
+ 9 z457
+ 2 z458
+ 4 z459
+ 9 z460
+ 6 z461
+ 7 z462
+ 7 z463
+ 1 z464
+ 5 z465
+ 7 z466
+ 6 z467
+ 1 z468
+ 10 z469
+ 10 z470
+ 9 z471
+ 3 z472
+ 1 z473
+ 3 z474
+ 1 z475
+ 3 z476
+ 4 z477
+ 9 z478
+ 4 z479
+ 10 z480
+ 4 z481
+ 8 z482
+ 8 z483
+ 1 z484
+ 4 z485
+ 1 z486
+ 5 z487
+ 3 z488
+ 3 z489
+ 8 z490
+ 1 z491
+ 8 z492
+ 4 z493
+ 7 z494
+ 9 z495
+ 9 z496
+ 3 z497
+ 5 z498
+ 10 z499
+ 3 z500
+ 4 z501
+ 9 z502
+ 5 z503
+ 5 z504
+ 1 z505
+ 5 z506
+ 7 z507
+ 5 z508
+ 3 z509
+ 1 z510
+ 4 z511
+ 7 z512
+ 8 z513
+ 2 z514
+ 7 z515
+ 2 z516
+ 2 z517
+ 2 z518
+ 4 z519
+ 5 z520
+ 9 z521
+ 4 z522
+ 3 z523
+ 3 z524
+ 1 z525
+ 1 z526
+ 1 z527
+ 4 z528
+ 5 z529
+ 1 z530
+ 6 z531
+ 9 z532
+ 9 z533
+ 10 z534
+ 4 z535
+ 10 z536
+ 5 z537
+ 10 z538
+ 4 z539
+ 8 z540
+ 1 z541
+ 8 z542
+ 5 z543
+ 8 z544
+ 9 z545
+ 2 z546
+ 10 z547
+ 10 z548
+ 3 z549
+ 3 z550
+ 5 z551
+ 1 z552
+ 7 z553
+ 7 z554
+ 3 z555
+ 7 z556
+ 7 z557
+ 4 z558
+ 1 z559
+ 2 z560
+ 4 z561
+ 6 z562
+ 1 z563
+ 3 z564
+ 6 z565
+ 4 z566
+ 2 z567
+ 1 z568
+ 4 z569
+ 6 z570
+ 8 z571
+ 4 z572
+ 3 z573
+ 2 z574
+ 2 z575
+ 1 z576
+ 3 z577
+ 1 z578
+ 1 z579
+ 5 z580
+ 4 z581
+ 5 z582
+ 5 z583
+ 10 z584
+ 2 z585
+ 8 z586
+ 7 z587
+ 8 z588
+ 1 z589
+ 7 z590
+ 10 z591
+ 5 z592
+ 3 z593
+ 10 z594
+ 7 z595
+ 9 z596
+ 4 z597
+ 9 z598
+ 9 z599
+ 7 z600
SUBJECT TO
+ x2 + x5 + x30  >= 1
- x68 - x41 - x22  >= -2
+ x62 - x58 + x9  >= 0
+ x77 - x70 + x42  >= 0
- x94 - x17 - x26  >= -2
- x72 + x84 + x2  >= 0
+ x51 + x60 + x39  >= 1
+ x83 + x90 - x37  >= 0
+ x92 - x14 + x97  >= 0
- x25 - x7 + x51  >= -1
- x54 + x48 + x14  >= 0
+ x72 + x82 + x93  >= 1
- x38 + x86 - x15  >= -1
+ x30 + x93 - x73  >= 0
+ x52 + x50 + x69  >= 1
+ x33 + x86 + x93  >= 1
- x79 + x12 + x5  >= 0
+ x96 + x60 - x93  >= 0
+ x69 - x65 + x87  >= 0
- x3 + x42 - x60  >= -1
+ x17 + x77 + x10  >= 1
- x2 - x29 + x37  >= -1
- x69 + x10 + x37  >= 0
- x47 - x9 + x17  >= -1
- x91 - x41 - x86  >= -2
- x79 - x62 - x53  >= -2
- x21 - x87 + x98  >= -1
+ x2 + x29 + x58  >= 1
- x70 + x54 + x10  >= 0
- x13 - x32 + x48  >= -1
+ x75 - x72 - x94  >= -1
- x97 + x81 + x65  >= 0
- x42 - x40 - x52  >= -2
+ x100 + x48 - x13  >= 0
- x17 + x46 - x85  >= -1
- x97 + x19 + x50  >= 0
+ x69 + x42 + x90  >= 1
+ x57 - x76 + x67  >= 0
- x68 - x74 + x93  >= -1
+ x33 - x100 + x72  >= 0
+ x96 - x61 - x33  >= -1
+ x54 - x20 - x19  >= -1
+ x70 + x9 + x30  >= 1
- x82 - x85 - x78  >= -2
- x100 + x98 + x60  >= 0
+ x86 - x10 + x85  >= 0
+ x96 + x8 + x56  >= 1
- x69 - x20 + x17  >= -1
- x1 + x37 - x19  >= -1
- x39 - x11 - x80  >= -2
+ x22 - x67 - x4  >= -1
- x43 - x80 + x65  >= -1
+ x5 - x63 - x34  >= -1
- x55 + x61 + x26  >= 0
+ x55 - x77 + x48  >= 0
+ x28 + x98 - x95  >= 0
- x89 + x46 - x59  >= -1
+ x68 - x48 - x15  >= -1
+ x91 - x23 - x35  >= -1
- x53 + x50 + x100  >= 0
+ x12 + x23 + x43  >= 1
+ x72 + x60 - x84  >= 0
+ x63 - x26 + x53  >= 0
+ x54 + x35 + x59  >= 1
- x99 - x58 + x11  >= -1
+ x94 + x5 - x62  >= 0
- x67 + x3 + x22  >= 0
- x2 + x80 - x60  >= -1
- x98 + x64 + x94  >= 0
- x69 - x11 + x58  >= -1
- x18 + x87 - x44  >= -1
- x41 + x89 - x77  >= -1
- x96 - x41 - x73  >= -2
+ x14 + x93 - x47  >= 0
- x7 - x18 - x70  >= -2
+ x3 - x15 - x50  >= -1
- x21 - x35 - x61  >= -2
- x91 + x92 + x41  >= 0
- x46 - x60 - x29  >= -2
+ x51 + x72 - x96  >= 0
+ x83 - x39 + x7  >= 0
- x4 + x6 + x35  >= 0
+ x65 - x93 - x23  >= -1
- x40 - x2 - x28  >= -2
+ x47 - x44 - x65  >= -1
+ x35 - x46 + x38  >= 0
- x42 + x82 + x28  >= 0
+ x7 + x10 - x23  >= 0
+ x97 + x54 - x80  >= 0
+ x17 - x69 - x81  >= -1
- x46 + x26 + x19  >= 0
+ x29 + x84 - x69  >= 0
+ x11 - x40 + x22  >= 0
- x36 + x8 - x80  >= -1
- x77 + x99 + x69  >= 0
- x38 + x56 - x74  >= -1
- x98 - x72 - x61  >= -2
- x66 + x87 - x30  >= -1
- x88 + x63 + x90  >= 0
- x20 - x99 + x18  >= -1
+ x36 + x94 + x83 + z101 >= 1
+ x86 + x48 - x96 + z102 >= 0
- x36 - x80 - x59 + z103 >= -2
+ x47 - x54 - x37 + z104 >= -1
+ x40 + x67 + x75 + z105 >= 1
- x63 - x15 + x84 + z106 >= -1
+ x58 + x12 - x3 + z107 >= 0
+ x38 - x5 + x33 + z108 >= 0
- x49 + x25 + x64 + z109 >= 0
+ x42 + x84 + x98 + z110 >= 1
- x17 + x74 - x35 + z111 >= -1
+ x8 + x3 + x11 + z112 >= 1
+ x85 + x43 + x41 + z113 >= 1
- x34 - x93 - x35 + z114 >= -2
+ x29 + x20 - x63 + z115 >= 0
- x46 - x53 - x48 + z116 >= -2
- x79 - x60 - x95 + z117 >= -2
- x25 - x54 - x42 + z118 >= -2
+ x76 + x5 - x79 + z119 >= 0
- x90 - x31 + x76 + z120 >= -1
- x27 - x3 + x63 + z121 >= -1
- x66 - x62 + x74 + z122 >= -1
+ x60 + x75 - x97 + z123 >= 0
- x88 + x16 - x73 + z124 >= -1
- x22 - x16 - x6 + z125 >= -2
- x8 - x95 + x66 + z126 >= -1
- x86 - x35 - x9 + z127 >= -2
- x3 - x55 - x34 + z128 >= -2
+ x68 + x44 + x89 + z129 >= 1
+ x14 - x30 - x20 + z130 >= -1
+ x34 - x92 - x47 + z131 >= -1
+ x90 - x95 - x4 + z132 >= -1
- x52 - x44 - x96 + z133 >= -2
- x18 - x43 - x57 + z134 >= -2
- x72 + x81 - x99 + z135 >= -1
+ x72 + x40 + x89 + z136 >= 1
+ x13 - x34 + x43 + z137 >= 0
- x78 - x34 - x75 + z138 >= -2
- x41 - x2 - x17 + z139 >= -2
- x68 + x30 - x48 + z140 >= -1
- x63 + x92 + x94 + z141 >= 0
+ x99 + x22 - x71 + z142 >= 0
+ x73 - x15 - x87 + z143 >= -1
+ x21 + x28 + x73 + z144 >= 1
- x5 - x93 - x61 + z145 >= -2
- x6 - x21 - x72 + z146 >= -2
+ x36 + x70 + x4 + z147 >= 1
+ x60 + x83 + x55 + z148 >= 1
- x17 - x51 - x70 + z149 >= -2
- x20 + x93 + x87 + z150 >= 0
+ x61 + x50 + x65 + z151 >= 1
+ x14 - x84 + x5 + z152 >= 0
+ x58 - x50 + x98 + z153 >= 0
+ x55 + x13 - x79 + z154 >= 0
+ x19 + x22 + x59 + z155 >= 1
+ x51 - x63 - x52 + z156 >= -1
- x52 + x9 - x84 + z157 >= -1
- x71 - x83 + x24 + z158 >= -1
- x97 - x50 + x32 + z159 >= -1
- x41 - x93 - x55 + z160 >= -2
- x2 - x49 + x19 + z161 >= -1
+ x54 - x16 + x22 + z162 >= 0
+ x11 + x42 + x29 + z163 >= 1
- x54 - x7 + x74 + z164 >= -1
- x20 + x22 + x40 + z165 >= 0
+ x31 - x23 - x87 + z166 >= -1
- x62 - x31 + x67 + z167 >= -1
- x29 + x79 - x80 + z168 >= -1
- x82 - x67 - x97 + z169 >= -2
+ x1 + x73 + x99 + z170 >= 1
- x78 + x77 + x43 + z171 >= 0
- x15 - x88 + x50 + z172 >= -1
- x19 - x99 + x96 + z173 >= -1
- x88 - x38 + x76 + z174 >= -1
- x61 + x93 + x1 + z175 >= 0
+ x80 - x11 + x24 + z176 >= 0
- x41 - x90 + x37 + z177 >= -1
+ x8 - x90 - x6 + z178 >= -1
- x12 - x75 - x100 + z179 >= -2
+ x16 - x19 + x84 + z180 >= 0
- x64 - x58 + x28 + z181 >= -1
- x38 + x21 - x92 + z182 >= -1
- x81 + x18 + x51 + z183 >= 0
+ x49 + x33 - x13 + z184 >= 0
+ x40 - x35 - x89 + z185 >= -1
- x40 + x15 + x25 + z186 >= 0
- x69 + x40 + x24 + z187 >= 0
- x22 - x95 - x53 + z188 >= -2
+ x11 - x29 + x5 + z189 >= 0
- x93 + x16 + x59 + z190 >= 0
- x48 + x79 + x25 + z191 >= 0
- x76 - x14 - x67 + z192 >= -2
- x34 - x95 - x75 + z193 >= -2
- x59 + x78 - x84 + z194 >= -1
+ x88 - x93 + x76 + z195 >= 0
- x57 - x22 + x93 + z196 >= -1
- x9 - x69 + x52 + z197 >= -1
+ x55 - x3 - x20 + z198 >= -1
- x84 + x47 - x65 + z199 >= -1
+ x27 + x98 + x58 + z200 >= 1
+ x16 - x1 + x52 + z201 >= 0
- x46 - x90 - x14 + z202 >= -2
+ x22 + x19 - x85 + z203 >= 0
- x29 - x32 + x20 + z204 >= -1
+ x59 + x25 - x27 + z205 >= 0
- x46 + x42 - x71 + z206 >= -1
- x43 - x95 + x42 + z207 >= -1
+ x39 - x13 - x24 + z208 >= -1
+ x96 - x83 + x3 + z209 >= 0
- x44 + x34 - x25 + z210 >= -1
+ x42 - x95 + x93 + z211 >= 0
+ x65 - x36 + x37 + z212 >= 0
+ x11 - x31 - x41 + z213 >= -1
+ x6 - x49 - x77 + z214 >= -1
+ x9 - x7 + x87 + z215 >= 0
- x85 + x19 + x31 + z216 >= 0
- x19 - x95 + x58 + z217 >= -1
+ x83 + x11 + x80 + z218 >= 1
- x18 - x51 + x82 + z219 >= -1
+ x47 + x68 + x51 + z220 >= 1
- x69 - x85 - x46 + z221 >= -2
- x21 + x80 - x70 + z222 >= -1
+ x29 + x18 + x80 + z223 >= 1
+ x42 - x59 + x75 + z224 >= 0
+ x67 + x100 + x1 + z225 >= 1
- x45 - x1 + x86 + z226 >= -1
+ x66 - x20 - x27 + z227 >= -1
- x6 + x28 + x80 + z228 >= 0
- x10 - x77 + x79 + z229 >= -1
+ x18 - x66 - x31 + z230 >= -1
+ x20 + x27 - x64 + z231 >= 0
+ x52 - x83 + x79 + z232 >= 0
+ x25 + x8 + x19 + z233 >= 1
+ x20 + x18 + x4 + z234 >= 1
- x84 + x80 - x41 + z235 >= -1
+ x93 - x7 + x65 + z236 >= 0
+ x93 + x51 + x95 + z237 >= 1
+ x36 - x40 - x54 + z238 >= -1
- x64 + x3 - x10 + z239 >= -1
+ x89 - x4 - x38 + z240 >= -1
- x89 - x62 - x87 + z241 >= -2
- x70 - x64 + x6 + z242 >= -1
- x98 - x10 - x77 + z243 >= -2
- x44 - x18 - x62 + z244 >= -2
+ x11 + x74 - x86 + z245 >= 0
+ x28 + x91 - x17 + z246 >= 0
- x69 - x13 + x52 + z247 >= -1
- x12 + x75 - x36 + z248 >= -1
+ x48 + x69 - x9 + z249 >= 0
- x91 - x32 - x68 + z250 >= -2
+ x30 + x8 + x61 + z251 >= 1
- x34 - x90 - x17 + z252 >= -2
+ x12 - x76 - x67 + z253 >= -1
+ x38 + x11 - x61 + z254 >= 0
+ x39 - x10 - x14 + z255 >= -1
+ x76 - x16 + x100 + z256 >= 0
- x41 - x95 - x11 + z257 >= -2
+ x50 + x92 + x17 + z258 >= 1
+ x76 + x23 - x69 + z259 >= 0
- x60 + x52 - x64 + z260 >= -1
- x42 + x52 - x56 + z261 >= -1
- x19 - x9 - x86 + z262 >= -2
+ x25 + x80 + x9 + z263 >= 1
+ x49 + x94 - x45 + z264 >= 0
+ x69 + x75 - x39 + z265 >= 0
+ x88 - x82 + x27 + z266 >= 0
+ x19 - x79 + x49 + z267 >= 0
- x65 + x78 + x16 + z268 >= 0
+ x95 - x67 + x27 + z269 >= 0
- x26 - x53 - x16 + z270 >= -2
- x39 + x72 - x38 + z271 >= -1
- x6 + x34 + x76 + z272 >= 0
+ x91 - x2 + x6 + z273 >= 0
- x40 + x70 - x91 + z274 >= -1
+ x8 - x34 + x27 + z275 >= 0
+ x79 + x36 - x83 + z276 >= 0
- x14 - x7 - x31 + z277 >= -2
+ x19 - x51 + x70 + z278 >= 0
+ x48 - x96 + x15 + z279 >= 0
+ x13 - x70 - x58 + z280 >= -1
+ x51 - x71 - x91 + z281 >= -1
- x31 - x1 - x98 + z282 >= -2
- x30 + x8 - x9 + z283 >= -1
- x45 + x80 + x61 + z284 >= 0
+ x84 - x29 - x93 + z285 >= -1
- x96 - x19 + x56 + z286 >= -1
- x77 + x83 + x42 + z287 >= 0
+ x33 - x74 - x40 + z288 >= -1
- x6 - x18 - x50 + z289 >= -2
- x89 + x60 - x96 + z290 >= -1
+ x66 - x96 + x82 + z291 >= 0
+ x63 + x58 - x16 + z292 >= 0
- x37 + x64 + x32 + z293 >= 0
- x47 - x10 - x22 + z294 >= -2
- x63 + x65 - x58 + z295 >= -1
+ x22 + x12 + x53 + z296 >= 1
- x37 - x95 + x92 + z297 >= -1
+ x11 + x36 - x87 + z298 >= 0
- x47 - x57 - x1 + z299 >= -2
+ x66 - x16 - x40 + z300 >= -1
+ x81 - x96 + x97 + z301 >= 0
- x67 - x35 + x23 + z302 >= -1
- x81 + x96 - x58 + z303 >= -1
- x59 - x84 - x26 + z304 >= -2
- x35 + x17 - x94 + z305 >= -1
- x60 - x20 - x63 + z306 >= -2
+ x85 - x20 - x96 + z307 >= -1
- x30 + x59 + x77 + z308 >= 0
- x55 + x85 + x99 + z309 >= 0
- x59 - x78 + x67 + z310 >= -1
- x20 - x12 - x26 + z311 >= -2
+ x44 - x52 - x99 + z312 >= -1
- x20 - x88 - x35 + z313 >= -2
+ x11 + x30 - x45 + z314 >= 0
+ x59 + x68 + x65 + z315 >= 1
- x31 + x39 - x29 + z316 >= -1
+ x35 + x64 + x47 + z317 >= 1
+ x9 + x22 - x94 + z318 >= 0
+ x4 + x29 + x98 + z319 >= 1
+ x36 + x96 - x75 + z320 >= 0
+ x17 + x51 - x33 + z321 >= 0
- x41 - x40 + x18 + z322 >= -1
- x93 + x81 - x41 + z323 >= -1
- x55 - x27 + x87 + z324 >= -1
+ x60 + x10 + x19 + z325 >= 1
- x29 - x26 - x89 + z326 >= -2
+ x15 - x11 + x35 + z327 >= 0
- x52 - x91 + x87 + z328 >= -1
+ x50 - x33 + x37 + z329 >= 0
- x59 - x45 + x20 + z330 >= -1
+ x15 - x9 + x55 + z331 >= 0
+ x98 + x85 + x37 + z332 >= 1
+ x38 - x68 + x25 + z333 >= 0
+ x35 + x9 - x72 + z334 >= 0
- x3 + x65 + x2 + z335 >= 0
- x94 + x53 + x85 + z336 >= 0
+ x94 + x8 - x47 + z337 >= 0
- x63 - x93 + x6 + z338 >= -1
- x22 + x61 - x43 + z339 >= -1
- x75 - x7 - x27 + z340 >= -2
- x6 - x80 + x23 + z341 >= -1
+ x2 - x69 - x52 + z342 >= -1
+ x28 + x55 + x69 + z343 >= 1
- x41 - x64 - x81 + z344 >= -2
- x45 + x31 - x92 + z345 >= -1
- x41 + x13 + x57 + z346 >= 0
- x8 - x4 - x100 + z347 >= -2
+ x36 + x80 - x48 + z348 >= 0
+ x25 + x54 + x53 + z349 >= 1
- x89 - x82 + x39 + z350 >= -1
- x58 - x94 + x14 + z351 >= -1
+ x65 + x64 + x45 + z352 >= 1
- x61 + x95 - x85 + z353 >= -1
- x89 - x61 + x26 + z354 >= -1
- x82 + x79 + x73 + z355 >= 0
+ x19 - x25 + x75 + z356 >= 0
+ x77 - x46 + x99 + z357 >= 0
+ x58 - x31 + x9 + z358 >= 0
+ x15 - x84 - x76 + z359 >= -1
+ x75 + x58 - x51 + z360 >= 0
+ x66 - x37 - x7 + z361 >= -1
- x76 - x45 + x34 + z362 >= -1
- x89 - x23 + x35 + z363 >= -1
- x12 + x79 - x13 + z364 >= -1
+ x61 + x94 - x47 + z365 >= 0
- x94 + x7 - x2 + z366 >= -1
+ x88 - x23 - x14 + z367 >= -1
- x25 - x85 - x1 + z368 >= -2
+ x89 - x93 - x44 + z369 >= -1
+ x91 - x41 - x57 + z370 >= -1
+ x2 + x45 - x5 + z371 >= 0
- x72 - x32 - x75 + z372 >= -2
- x65 + x78 + x55 + z373 >= 0
- x30 + x26 + x29 + z374 >= 0
- x36 - x18 + x49 + z375 >= -1
- x91 - x55 - x45 + z376 >= -2
+ x48 + x30 - x21 + z377 >= 0
+ x93 + x79 - x50 + z378 >= 0
+ x83 + x74 + x12 + z379 >= 1
- x20 - x82 + x56 + z380 >= -1
- x69 + x65 + x14 + z381 >= 0
+ x8 - x51 - x22 + z382 >= -1
- x22 + x45 - x69 + z383 >= -1
+ x62 - x43 - x63 + z384 >= -1
- x90 + x37 + x51 + z385 >= 0
- x29 + x10 + x32 + z386 >= 0
+ x96 + x83 + x56 + z387 >= 1
+ x47 - x93 + x94 + z388 >= 0
+ x67 - x44 + x68 + z389 >= 0
- x11 + x41 + x85 + z390 >= 0
+ x80 + x33 - x41 + z391 >= 0
+ x46 + x16 + x55 + z392 >= 1
+ x51 + x88 - x96 + z393 >= 0
+ x69 - x70 - x20 + z394 >= -1
- x84 - x10 + x11 + z395 >= -1
+ x99 - x51 - x48 + z396 >= -1
- x10 + x8 + x84 + z397 >= 0
- x67 + x58 + x12 + z398 >= 0
- x39 + x71 - x83 + z399 >= -1
+ x29 - x90 - x91 + z400 >= -1
- x55 - x11 - x2 + z401 >= -2
- x3 - x80 - x52 + z402 >= -2
- x34 + x46 + x87 + z403 >= 0
- x33 + x18 - x83 + z404 >= -1
- x19 - x13 + x55 + z405 >= -1
+ x12 + x24 - x26 + z406 >= 0
+ x81 - x20 - x78 + z407 >= -1
- x8 + x20 - x11 + z408 >= -1
- x95 + x47 - x76 + z409 >= -1
- x42 + x56 - x11 + z410 >= -1
+ x10 + x25 + x4 + z411 >= 1
+ x33 - x18 + x41 + z412 >= 0
- x76 - x58 - x47 + z413 >= -2
+ x45 + x46 + x8 + z414 >= 1
+ x19 - x65 + x1 + z415 >= 0
+ x9 + x70 - x38 + z416 >= 0
- x33 + x38 + x92 + z417 >= 0
+ x1 + x24 - x100 + z418 >= 0
+ x8 - x55 + x98 + z419 >= 0
- x61 + x93 + x85 + z420 >= 0
+ x74 + x30 + x15 + z421 >= 1
- x85 + x75 + x57 + z422 >= 0
+ x19 - x49 + x29 + z423 >= 0
- x70 + x4 - x94 + z424 >= -1
- x88 + x79 - x60 + z425 >= -1
+ x18 + x12 - x11 + z426 >= 0
+ x51 - x7 - x28 + z427 >= -1
+ x13 + x2 + x25 + z428 >= 1
- x81 - x89 + x23 + z429 >= -1
- x41 + x43 - x20 + z430 >= -1
- x81 - x32 - x70 + z431 >= -2
- x44 + x15 - x99 + z432 >= -1
- x47 - x35 + x83 + z433 >= -1
+ x90 + x57 - x13 + z434 >= 0
- x71 + x87 + x73 + z435 >= 0
+ x51 - x34 - x1 + z436 >= -1
- x85 + x11 - x91 + z437 >= -1
- x2 + x68 - x54 + z438 >= -1
- x63 + x1 - x44 + z439 >= -1
+ x29 - x2 - x75 + z440 >= -1
+ x32 - x23 + x10 + z441 >= 0
+ x25 + x49 + x18 + z442 >= 1
+ x86 - x7 - x17 + z443 >= -1
+ x93 + x42 - x61 + z444 >= 0
- x25 + x45 - x93 + z445 >= -1
- x76 + x77 - x88 + z446 >= -1
+ x93 + x33 + x100 + z447 >= 1
- x60 - x33 - x11 + z448 >= -2
- x37 - x64 + x30 + z449 >= -1
- x89 + x24 + x90 + z450 >= 0
+ x46 - x99 + x12 + z451 >= 0
- x84 - x77 - x53 + z452 >= -2
- x88 + x46 + x32 + z453 >= 0
+ x87 - x60 - x66 + z454 >= -1
- x63 + x46 + x90 + z455 >= 0
- x87 + x73 - x11 + z456 >= -1
- x19 - x89 - x71 + z457 >= -2
+ x70 - x61 + x3 + z458 >= 0
- x5 - x46 + x84 + z459 >= -1
+ x36 - x25 + x86 + z460 >= 0
+ x38 - x64 - x85 + z461 >= -1
+ x43 - x80 + x78 + z462 >= 0
- x71 + x21 - x11 + z463 >= -1
- x98 - x27 - x15 + z464 >= -2
+ x21 - x33 - x2 + z465 >= -1
+ x19 + x95 + x42 + z466 >= 1
- x92 - x85 + x84 + z467 >= -1
+ x20 + x69 - x54 + z468 >= 0
+ x99 + x38 - x2 + z469 >= 0
- x90 + x40 - x31 + z470 >= -1
+ x69 - x66 + x83 + z471 >= 0
- x14 + x60 + x10 + z472 >= 0
- x30 - x49 + x77 + z473 >= -1
- x60 - x77 - x56 + z474 >= -2
- x60 - x78 - x14 + z475 >= -2
- x79 + x37 - x26 + z476 >= -1
- x86 - x60 - x53 + z477 >= -2
- x3 - x86 + x31 + z478 >= -1
- x97 - x30 - x86 + z479 >= -2
+ x26 + x51 + x52 + z480 >= 1
+ x100 - x19 + x56 + z481 >= 0
- x18 - x65 + x62 + z482 >= -1
- x53 + x63 - x3 + z483 >= -1
- x93 - x39 - x2 + z484 >= -2
+ x52 - x16 - x43 + z485 >= -1
- x23 - x55 - x3 + z486 >= -2
+ x81 - x98 + x47 + z487 >= 0
- x60 + x21 + x68 + z488 >= 0
+ x35 - x97 + x48 + z489 >= 0
- x29 + x26 + x54 + z490 >= 0
- x55 + x51 + x64 + z491 >= 0
- x39 - x10 + x41 + z492 >= -1
- x90 - x11 + x29 + z493 >= -1
+ x67 + x7 + x29 + z494 >= 1
+ x52 + x71 - x28 + z495 >= 0
- x14 - x96 + x7 + z496 >= -1
- x21 - x91 - x45 + z497 >= -2
- x69 + x65 - x6 + z498 >= -1
- x30 + x89 + x85 + z499 >= 0
- x62 - x54 + x98 + z500 >= -1
- x46 + x72 - x35 + z501 >= -1
+ x88 + x69 - x78 + z502 >= 0
+ x28 - x99 + x19 + z503 >= 0
- x12 - x26 + x29 + z504 >= -1
+ x23 + x47 + x85 + z505 >= 1
- x59 + x82 - x14 + z506 >= -1
- x81 - x21 - x32 + z507 >= -2
+ x12 + x80 - x60 + z508 >= 0
- x70 + x25 - x81 + z509 >= -1
+ x30 - x43 + x13 + z510 >= 0
- x58 + x22 - x31 + z511 >= -1
- x34 - x97 + x86 + z512 >= -1
- x25 - x67 + x18 + z513 >= -1
+ x39 - x67 - x56 + z514 >= -1
- x86 + x95 - x18 + z515 >= -1
- x47 + x67 + x3 + z516 >= 0
+ x42 + x71 - x15 + z517 >= 0
- x66 + x60 + x36 + z518 >= 0
- x14 + x83 - x98 + z519 >= -1
- x45 - x88 - x58 + z520 >= -2
+ x43 - x33 - x46 + z521 >= -1
- x51 - x40 + x78 + z522 >= -1
+ x44 - x34 + x82 + z523 >= 0
+ x40 - x60 - x11 + z524 >= -1
+ x53 + x50 - x31 + z525 >= 0
+ x58 - x67 - x30 + z526 >= -1
+ x67 + x28 + x39 + z527 >= 1
- x91 - x49 + x47 + z528 >= -1
- x87 + x15 + x84 + z529 >= 0
+ x71 - x77 + x95 + z530 >= 0
+ x98 - x49 - x96 + z531 >= -1
- x27 - x19 + x100 + z532 >= -1
+ x78 + x55 + x53 + z533 >= 1
+ x49 + x14 - x42 + z534 >= 0
- x77 - x81 + x42 + z535 >= -1
- x100 + x79 + x82 + z536 >= 0
- x68 - x33 + x54 + z537 >= -1
+ x71 - x76 - x24 + z538 >= -1
- x49 + x12 - x93 + z539 >= -1
+ x57 - x2 + x100 + z540 >= 0
+ x27 - x62 + x15 + z541 >= 0
- x90 - x1 + x2 + z542 >= -1
+ x27 - x73 - x89 + z543 >= -1
- x1 + x22 + x98 + z544 >= 0
- x52 - x58 + x20 + z545 >= -1
- x83 + x11 + x64 + z546 >= 0
+ x46 - x22 + x32 + z547 >= 0
- x65 - x5 - x3 + z548 >= -2
+ x39 + x55 - x97 + z549 >= 0
- x55 + x99 + x56 + z550 >= 0
+ x77 + x33 - x52 + z551 >= 0
+ x72 + x75 - x6 + z552 >= 0
+ x33 + x86 + x88 + z553 >= 1
+ x10 + x77 + x97 + z554 >= 1
- x5 + x68 - x43 + z555 >= -1
- x1 - x19 - x24 + z556 >= -2
+ x36 + x32 + x28 + z557 >= 1
+ x25 + x68 - x33 + z558 >= 0
+ x54 + x12 - x47 + z559 >= 0
+ x94 - x23 - x28 + z560 >= -1
- x28 + x83 + x89 + z561 >= 0
+ x4 + x69 + x80 + z562 >= 1
+ x79 + x34 - x82 + z563 >= 0
+ x82 + x1 + x96 + z564 >= 1
+ x89 - x44 + x36 + z565 >= 0
- x86 - x7 + x100 + z566 >= -1
+ x22 - x62 + x3 + z567 >= 0
- x16 - x71 - x46 + z568 >= -2
- x81 - x64 + x92 + z569 >= -1
+ x90 - x82 - x86 + z570 >= -1
+ x44 - x83 + x72 + z571 >= 0
- x77 - x78 - x91 + z572 >= -2
+ x91 - x94 + x54 + z573 >= 0
+ x28 + x72 - x99 + z574 >= 0
+ x62 - x38 - x73 + z575 >= -1
- x12 + x7 + x53 + z576 >= 0
+ x13 + x27 - x86 + z577 >= 0
+ x87 + x96 + x58 + z578 >= 1
- x76 - x60 - x19 + z579 >= -2
+ x66 - x40 - x4 + z580 >= -1
- x8 - x98 + x73 + z581 >= -1
- x68 - x94 - x49 + z582 >= -2
- x18 + x85 - x49 + z583 >= -1
+ x23 - x100 + x40 + z584 >= 0
+ x8 - x39 + x58 + z585 >= 0
- x78 + x85 + x42 + z586 >= 0
+ x73 - x12 + x17 + z587 >= 0
+ x75 - x83 + x100 + z588 >= 0
+ x4 + x81 - x24 + z589 >= 0
+ x62 + x29 + x36 + z590 >= 1
+ x64 - x18 + x97 + z591 >= 0
+ x28 - x40 + x53 + z592 >= 0
- x60 - x35 - x1 + z593 >= -2
+ x84 + x62 - x39 + z594 >= 0
+ x4 - x66 + x90 + z595 >= 0
+ x53 - x48 + x47 + z596 >= 0
+ x90 + x81 + x54 + z597 >= 1
- x60 + x85 + x49 + z598 >= 0
- x20 + x27 - x69 + z599 >= -1
+ x19 - x38 + x39 + z600 >= 0
BINARY
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
z101
z102
z103
z104
z105
z106
z107
z108
z109
z110
z111
z112
z113
z114
z115
z116
z117
z118
z119
z120
z121
z122
z123
z124
z125
z126
z127
z128
z129
z130
z131
z132
z133
z134
z135
z136
z137
z138
z139
z140
z141
z142
z143
z144
z145
z146
z147
z148
z149
z150
z151
z152
z153
z154
z155
z156
z157
z158
z159
z160
z161
z162
z163
z164
z165
z166
z167
z168
z169
z170
z171
z172
z173
z174
z175
z176
z177
z178
z179
z180
z181
z182
z183
z184
z185
z186
z187
z188
z189
z190
z191
z192
z193
z194
z195
z196
z197
z198
z199
z200
z201
z202
z203
z204
z205
z206
z207
z208
z209
z210
z211
z212
z213
z214
z215
z216
z217
z218
z219
z220
z221
z222
z223
z224
z225
z226
z227
z228
z229
z230
z231
z232
z233
z234
z235
z236
z237
z238
z239
z240
z241
z242
z243
z244
z245
z246
z247
z248
z249
z250
z251
z252
z253
z254
z255
z256
z257
z258
z259
z260
z261
z262
z263
z264
z265
z266
z267
z268
z269
z270
z271
z272
z273
z274
z275
z276
z277
z278
z279
z280
z281
z282
z283
z284
z285
z286
z287
z288
z289
z290
z291
z292
z293
z294
z295
z296
z297
z298
z299
z300
z301
z302
z303
z304
z305
z306
z307
z308
z309
z310
z311
z312
z313
z314
z315
z316
z317
z318
z319
z320
z321
z322
z323
z324
z325
z326
z327
z328
z329
z330
z331
z332
z333
z334
z335
z336
z337
z338
z339
z340
z341
z342
z343
z344
z345
z346
z347
z348
z349
z350
z351
z352
z353
z354
z355
z356
z357
z358
z359
z360
z361
z362
z363
z364
z365
z366
z367
z368
z369
z370
z371
z372
z373
z374
z375
z376
z377
z378
z379
z380
z381
z382
z383
z384
z385
z386
z387
z388
z389
z390
z391
z392
z393
z394
z395
z396
z397
z398
z399
z400
z401
z402
z403
z404
z405
z406
z407
z408
z409
z410
z411
z412
z413
z414
z415
z416
z417
z418
z419
z420
z421
z422
z423
z424
z425
z426
z427
z428
z429
z430
z431
z432
z433
z434
z435
z436
z437
z438
z439
z440
z441
z442
z443
z444
z445
z446
z447
z448
z449
z450
z451
z452
z453
z454
z455
z456
z457
z458
z459
z460
z461
z462
z463
z464
z465
z466
z467
z468
z469
z470
z471
z472
z473
z474
z475
z476
z477
z478
z479
z480
z481
z482
z483
z484
z485
z486
z487
z488
z489
z490
z491
z492
z493
z494
z495
z496
z497
z498
z499
z500
z501
z502
z503
z504
z505
z506
z507
z508
z509
z510
z511
z512
z513
z514
z515
z516
z517
z518
z519
z520
z521
z522
z523
z524
z525
z526
z527
z528
z529
z530
z531
z532
z533
z534
z535
z536
z537
z538
z539
z540
z541
z542
z543
z544
z545
z546
z547
z548
z549
z550
z551
z552
z553
z554
z555
z556
z557
z558
z559
z560
z561
z562
z563
z564
z565
z566
z567
z568
z569
z570
z571
z572
z573
z574
z575
z576
z577
z578
z579
z580
z581
z582
z583
z584
z585
z586
z587
z588
z589
z590
z591
z592
z593
z594
z595
z596
z597
z598
z599
z600
END

output-of-akmaxsat.txt

% time akmaxsat file_rwpms_wcnf_L3_V100_C600_H100_0.wcnf
o 158
o 157
o 156
o 154
o 151
o 145
o 138
o 136
o 133
o 132
o 128
o 121
o 120
o 117
o 115
o 112
o 111
o 109
o 105
o 103
o 100
o 99
o 98
o 96
o 95
o 94
o 93
o 90
o 89
o 88
o 87
o 85
o 84
o 83
o 82
o 81
o 80
o 79
o 78
o 77
o 75
o 74
o 73
o 70
o 68
o 67
o 64
o 62
o 61
o 58
o 57
o 56
o 53
o 52
o 46
o 44
o 43
o 42
o 41
o 40
o 38
o 37
o 35
o 34
o 32
o 31
o 30
o 29
o 28
c 9341 branches 9074 propagates
c total generalized unit propagation = 27568, success = 33.20%
s OPTIMUM FOUND
c Optimal Solution = 28
v 2 5 30 68 -41 -22 -58 9 -62 -70 42 -77 -94 26 -17 72 -84 -39 51 -60 37 83 90 -14 92 -97 -25 -7 -54 -48 -82 -93 38 -15 -86 73 50 52 -69 33 79 12 -96 -65 -87 3 10 29 -47 -91 53 21 98 -32 -13 75 81 -40 -100 85 -46 19 76 57 -67 -74 -61 -20 -78 8 56 1 -80 -11 4 -43 63 -34 55 -95 28 -89 59 35 -23 -99 64 44 -18 6 36 -66 -88 49 -31 -27 -16 -71 -24 -45

real	0m11.419s
user	0m11.085s
sys	0m0.032s