Maximize
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 + x253 + x254 + x255 + x256
 + x257 + x258 + x259 + x260 + x261 + x262 + x263 + x264
 + x265 + x266 + x267 + x268 + x269 + x270 + x271 + x272
 + x273 + x274 + x275 + x276 + x277 + x278 + x279 + x280
 + x281 + x282 + x283 + x284 + x285 + x286 + x287 + x288
 + x289 + x290 + x291 + x292 + x293 + x294 + x295 + x296
 + x297 + x298 + x299 + x300
subject to
c1: x1 + x4 + x278 + x108 <= 1
c2: x1 + x11 + x65 + x72 + x14 + x95 + x221 <= 1
c3: x1 + x13 + x132 + x187 + x50 <= 1
c4: x1 + x15 + x238 + x74 + x118 + x172 <= 1
c5: x1 + x19 + x278 + x282 + x80 <= 1
c6: x1 + x20 + x69 + x238 + x202 + x208 <= 1
c7: x1 + x21 + x238 + x69 + x203 + x122 <= 1
c8: x1 + x22 + x69 + x216 + x74 + x233 <= 1
c9: x1 + x23 + x132 + x187 + x243 + x199 <= 1
c10: x1 + x34 + x278 + x282 + x203 <= 1
c11: x1 + x36 + x132 + x69 + x187 <= 1
c12: x1 + x41 + x238 + x278 + x69 + x73 <= 1
c13: x1 + x44 + x187 + x243 + x289 <= 1
c14: x1 + x47 + x132 + x50 + x41 <= 1
c15: x1 + x49 + x282 + x34 + x243 <= 1
c16: x1 + x53 + x132 + x69 + x72 + x14 <= 1
c17: x1 + x55 + x238 + x202 + x72 + x82 + x80 <= 1
c18: x1 + x62 + x86 + x69 + x282 + x74 + x157 <= 1
c19: x1 + x63 + x238 + x278 + x253 + x73 <= 1
c20: x1 + x68 + x216 + x53 + x233 + x195 <= 1
c21: x1 + x76 + x65 + x203 + x23 <= 1
c22: x1 + x77 + x132 + x187 + x69 + x41 <= 1
c23: x1 + x84 + x238 + x278 + x203 <= 1
c24: x1 + x87 + x132 + x65 + x118 + x243 <= 1
c25: x1 + x91 + x238 + x278 + x23 + x203 <= 1
c26: x1 + x92 + x238 + x86 + x202 + x108 <= 1
c27: x1 + x94 + x278 + x50 + x65 + x203 <= 1
c28: x1 + x97 + x132 + x187 + x69 + x77 <= 1
c29: x1 + x98 + x34 + x99 + x201 <= 1
c30: x1 + x100 + x238 + x69 + x74 + x224 <= 1
c31: x1 + x105 + x132 + x65 + x243 + x279 <= 1
c32: x1 + x106 + x278 + x238 + x69 + x243 + x73 <= 1
c33: x1 + x114 + x257 + x23 + x243 <= 1
c34: x1 + x115 + x278 + x50 + x203 <= 1
c35: x1 + x117 + x187 + x86 + x50 + x94 <= 1
c36: x1 + x119 + x34 + x53 + x14 + x221 <= 1
c37: x1 + x120 + x238 + x278 + x69 + x213 <= 1
c38: x1 + x124 + x132 + x187 + x157 <= 1
c39: x1 + x127 + x99 + x14 + x201 + x55 <= 1
c40: x1 + x130 + x132 + x257 + x95 <= 1
c41: x1 + x131 + x216 + x50 + x224 <= 1
c42: x1 + x135 + x132 + x187 + x41 + x69 <= 1
c43: x1 + x138 + x216 + x82 <= 1
c44: x1 + x143 + x238 + x72 + x118 + x69 + x243 <= 1
c45: x1 + x144 + x34 + x41 + x47 + x108 <= 1
c46: x1 + x146 + x282 + x74 + x86 + x62 + x204 <= 1
c47: x1 + x151 + x216 + x74 + x69 + x41 <= 1
c48: x1 + x165 + x132 + x187 + x23 + x243 <= 1
c49: x1 + x166 + x282 + x72 + x80 + x82 <= 1
c50: x1 + x169 + x132 + x187 + x14 <= 1
c51: x1 + x171 + x238 + x86 + x69 + x14 <= 1
c52: x1 + x175 + x278 + x34 + x108 <= 1
c53: x1 + x185 + x282 + x34 <= 1
c54: x1 + x188 + x238 + x203 + x122 <= 1
c55: x1 + x193 + x132 + x53 + x263 <= 1
c56: x1 + x196 + x132 + x257 + x72 + x243 <= 1
c57: x1 + x200 + x278 + x50 + x157 <= 1
c58: x1 + x212 + x278 + x282 + x203 + x69 <= 1
c59: x1 + x214 + x65 + x132 + x14 + x279 <= 1
c60: x1 + x218 + x238 + x278 + x65 + x203 + x172 <= 1
c61: x1 + x219 + x74 + x289 + x224 <= 1
c62: x1 + x220 + x216 + x74 + x253 <= 1
c63: x1 + x235 + x127 + x23 + x185 <= 1
c64: x1 + x240 + x282 + x65 + x82 + x72 <= 1
c65: x1 + x250 + x202 + x238 + x169 <= 1
c66: x1 + x259 + x99 + x114 + x41 <= 1
c67: x1 + x260 + x132 + x118 + x50 + x72 + x65 <= 1
c68: x1 + x266 + x202 + x118 + x130 + x106 <= 1
c69: x1 + x269 + x143 + x233 + x62 + x14 + x55 <= 1
c70: x1 + x270 + x11 + x169 + x14 + x172 <= 1
c71: x1 + x274 + x282 + x80 <= 1
c72: x1 + x280 + x132 + x289 <= 1
c73: x1 + x286 + x216 + x53 + x68 <= 1
c74: x1 + x287 + x34 + x282 + x263 <= 1
c75: x1 + x288 + x278 + x238 + x69 + x224 + x243 <= 1
c76: x1 + x291 + x127 + x95 <= 1
c77: x1 + x294 + x216 + x53 + x69 + x100 + x224 <= 1
c78: x1 + x296 + x99 + x53 + x157 <= 1
c79: x2 + x6 + x64 + x295 + x141 + x238 + x169 <= 1
c80: x2 + x8 + x112 + x284 + x203 + x212 <= 1
c81: x2 + x14 + x66 + x112 + x186 + x134 + x132 <= 1
c82: x2 + x18 + x241 + x85 + x148 + x216 <= 1
c83: x2 + x19 + x265 + x66 + x80 <= 1
c84: x2 + x20 + x64 + x60 + x241 + x238 <= 1
c85: x2 + x22 + x284 + x265 + x202 + x80 <= 1
c86: x2 + x25 + x112 + x66 + x186 + x278 <= 1
c87: x2 + x31 + x8 + x112 + x186 + x134 + x157 <= 1
c88: x2 + x36 + x64 + x155 + x85 + x154 <= 1
c89: x2 + x41 + x241 + x121 + x132 + x294 <= 1
c90: x2 + x42 + x60 + x265 + x295 + x80 + x238 <= 1
c91: x2 + x43 + x154 + x150 + x141 <= 1
c92: x2 + x44 + x284 + x253 + x217 <= 1
c93: x2 + x48 + x155 + x154 + x150 <= 1
c94: x2 + x51 + x183 + x265 + x132 + x243 <= 1
c95: x2 + x52 + x60 + x241 + x121 + x65 <= 1
c96: x2 + x53 + x112 + x186 + x134 + x278 + x157 <= 1
c97: x2 + x58 + x64 + x112 + x241 + x238 <= 1
c98: x2 + x59 + x60 + x143 + x69 + x238 + x42 <= 1
c99: x2 + x63 + x66 + x85 + x132 <= 1
c100: x2 + x68 + x183 + x112 + x195 + x172 <= 1
c101: x2 + x76 + x148 + x150 + x203 <= 1
c102: x2 + x77 + x284 + x253 <= 1
c103: x2 + x81 + x148 + x85 + x241 + x216 <= 1
c104: x2 + x93 + x8 + x186 + x212 + x31 <= 1
c105: x2 + x94 + x66 + x155 + x60 + x278 + x203 <= 1
c106: x2 + x97 + x64 + x148 + x241 + x238 + x196 <= 1
c107: x2 + x98 + x66 + x60 + x203 <= 1
c108: x2 + x103 + x8 + x112 + x31 + x238 <= 1
c109: x2 + x109 + x284 + x202 <= 1
c110: x2 + x110 + x186 + x66 + x93 + x80 <= 1
c111: x2 + x118 + x183 + x155 + x134 + x132 <= 1
c112: x2 + x122 + x64 + x241 + x158 + x237 <= 1
c113: x2 + x123 + x64 + x85 + x203 + x290 <= 1
c114: x2 + x126 + x8 + x168 <= 1
c115: x2 + x131 + x8 + x186 + x134 + x138 <= 1
c116: x2 + x135 + x284 + x265 <= 1
c117: x2 + x139 + x64 + x6 + x233 + x97 <= 1
c118: x2 + x146 + x284 + x6 + x294 <= 1
c119: x2 + x159 + x8 + x65 + x31 + x238 <= 1
c120: x2 + x162 + x183 + x168 + x276 <= 1
c121: x2 + x164 + x64 + x154 + x278 + x238 <= 1
c122: x2 + x165 + x284 + x265 <= 1
c123: x2 + x166 + x8 + x155 + x134 + x14 <= 1
c124: x2 + x174 + x66 + x186 + x112 + x134 + x132 <= 1
c125: x2 + x175 + x295 + x64 + x154 + x150 + x36 <= 1
c126: x2 + x176 + x284 + x8 + x112 + x157 <= 1
c127: x2 + x177 + x66 + x121 + x132 + x146 <= 1
c128: x2 + x182 + x183 + x112 + x241 + x278 + x238 <= 1
c129: x2 + x184 + x148 + x85 + x64 + x216 <= 1
c130: x2 + x185 + x186 + x66 + x233 <= 1
c131: x2 + x192 + x85 + x66 + x155 + x18 <= 1
c132: x2 + x193 + x265 + x183 + x202 <= 1
c133: x2 + x204 + x64 + x241 + x216 + x172 <= 1
c134: x2 + x206 + x295 + x6 + x141 <= 1
c135: x2 + x209 + x8 + x202 + x243 <= 1
c136: x2 + x215 + x148 + x143 <= 1
c137: x2 + x218 + x85 + x154 + x64 + x155 <= 1
c138: x2 + x221 + x112 + x183 + x118 + x134 <= 1
c139: x2 + x224 + x148 + x265 + x184 <= 1
c140: x2 + x225 + x295 + x154 + x81 <= 1
c141: x2 + x226 + x112 + x65 + x203 + x14 <= 1
c142: x2 + x240 + x295 + x150 + x103 + x31 <= 1
c143: x2 + x244 + x186 + x66 + x14 + x138 <= 1
c144: x2 + x255 + x8 + x93 <= 1
c145: x2 + x263 + x284 + x8 + x112 + x212 <= 1
c146: x2 + x270 + x284 + x6 + x93 <= 1
c147: x2 + x280 + x265 + x224 + x51 <= 1
c148: x2 + x285 + x85 + x64 + x184 + x203 <= 1
c149: x2 + x291 + x148 + x241 + x81 + x238 <= 1
c150: x2 + x297 + x284 + x202 <= 1
c151: x2 + x298 + x186 + x66 + x93 + x278 <= 1
c152: x3 + x6 + x12 + x230 + x194 + x8 <= 1
c153: x3 + x15 + x12 + x194 + x108 + x175 <= 1
c154: x3 + x22 + x210 + x116 + x140 + x233 <= 1
c155: x3 + x23 + x12 + x248 + x61 + x8 + x202 <= 1
c156: x3 + x24 + x230 + x210 + x248 + x278 <= 1
c157: x3 + x30 + x46 + x210 + x284 + x6 <= 1
c158: x3 + x34 + x12 + x230 + x148 + x261 <= 1
c159: x3 + x36 + x248 + x140 + x210 + x62 <= 1
c160: x3 + x37 + x178 + x154 + x202 + x175 <= 1
c161: x3 + x40 + x194 + x127 + x92 <= 1
c162: x3 + x56 + x230 + x67 + x118 <= 1
c163: x3 + x58 + x86 + x140 + x60 <= 1
c164: x3 + x63 + x258 + x61 + x127 + x36 <= 1
c165: x3 + x65 + x46 + x198 + x210 + x6 <= 1
c166: x3 + x78 + x173 + x116 + x282 + x8 <= 1
c167: x3 + x79 + x173 + x108 <= 1
c168: x3 + x80 + x12 + x194 + x230 + x148 <= 1
c169: x3 + x88 + x12 + x34 + x37 + x278 <= 1
c170: x3 + x89 + x46 + x116 + x140 + x23 <= 1
c171: x3 + x96 + x178 + x194 + x300 + x116 <= 1
c172: x3 + x98 + x12 + x86 + x202 <= 1
c173: x3 + x103 + x173 + x116 + x282 + x148 <= 1
c174: x3 + x106 + x230 + x12 + x248 + x148 + x202 <= 1
c175: x3 + x123 + x230 + x12 + x194 <= 1
c176: x3 + x125 + x178 + x154 <= 1
c177: x3 + x126 + x46 + x78 + x282 + x8 <= 1
c178: x3 + x129 + x230 + x12 + x194 + x6 + x278 <= 1
c179: x3 + x147 + x173 + x198 <= 1
c180: x3 + x153 + x198 + x210 + x92 <= 1
c181: x3 + x156 + x12 + x265 + x23 + x80 <= 1
c182: x3 + x157 + x178 + x194 + x284 + x8 <= 1
c183: x3 + x161 + x248 + x12 + x8 <= 1
c184: x3 + x165 + x300 + x34 + x6 <= 1
c185: x3 + x172 + x173 + x248 + x140 <= 1
c186: x3 + x186 + x230 + x12 + x248 + x80 + x8 <= 1
c187: x3 + x193 + x12 + x248 + x61 + x186 <= 1
c188: x3 + x215 + x12 + x248 + x148 + x80 <= 1
c189: x3 + x216 + x46 + x78 + x126 <= 1
c190: x3 + x263 + x46 + x210 + x284 + x8 <= 1
c191: x3 + x269 + x178 + x194 + x116 + x129 <= 1
c192: x3 + x271 + x46 + x258 + x127 + x129 <= 1
c193: x3 + x273 + x230 + x284 + x8 <= 1
c194: x3 + x285 + x230 + x178 + x116 + x261 <= 1
c195: x3 + x290 + x300 + x12 <= 1
c196: x3 + x297 + x194 + x230 + x178 + x284 <= 1
c197: x4 + x14 + x173 + x186 <= 1
c198: x4 + x15 + x16 + x108 + x186 <= 1
c199: x4 + x31 + x242 + x114 + x186 <= 1
c200: x4 + x39 + x242 + x114 <= 1
c201: x4 + x54 + x90 + x211 <= 1
c202: x4 + x62 + x16 + x64 + x108 <= 1
c203: x4 + x68 + x168 + x183 + x272 <= 1
c204: x4 + x73 + x242 + x173 + x168 + x186 + x31 + x197 <= 1
c205: x4 + x87 + x295 + x168 <= 1
c206: x4 + x93 + x242 + x39 + x230 <= 1
c207: x4 + x120 + x16 + x15 <= 1
c208: x4 + x135 + x90 + x230 + x186 <= 1
c209: x4 + x151 + x152 <= 1
c210: x4 + x158 + x16 + x64 + x272 <= 1
c211: x4 + x172 + x183 + x241 + x278 <= 1
c212: x4 + x206 + x16 + x15 <= 1
c213: x4 + x214 + x16 + x230 + x186 <= 1
c214: x4 + x217 + x242 + x152 <= 1
c215: x4 + x253 + x114 + x39 <= 1
c216: x4 + x262 + x90 + x272 <= 1
c217: x4 + x264 + x39 + x253 + x64 <= 1
c218: x4 + x266 + x183 + x68 + x272 + x54 <= 1
c219: x5 + x7 + x113 + x210 + x248 <= 1
c220: x5 + x12 + x275 + x289 + x72 <= 1
c221: x5 + x13 + x113 + x178 + x150 + x96 <= 1
c222: x5 + x22 + x82 + x118 + x243 + x202 <= 1
c223: x5 + x30 + x229 + x47 + x55 <= 1
c224: x5 + x31 + x275 + x289 + x41 <= 1
c225: x5 + x34 + x229 + x275 + x187 + x289 + x41 <= 1
c226: x5 + x37 + x275 + x121 + x12 <= 1
c227: x5 + x39 + x229 + x194 + x265 <= 1
c228: x5 + x40 + x229 + x90 + x194 <= 1
c229: x5 + x42 + x229 + x47 + x158 <= 1
c230: x5 + x43 + x72 + x150 <= 1
c231: x5 + x45 + x47 + x164 + x55 <= 1
c232: x5 + x49 + x275 + x289 + x34 <= 1
c233: x5 + x61 + x47 + x248 <= 1
c234: x5 + x63 + x113 + x82 + x55 <= 1
c235: x5 + x69 + x229 + x187 + x41 + x110 <= 1
c236: x5 + x98 + x229 + x90 + x34 <= 1
c237: x5 + x106 + x113 + x248 <= 1
c238: x5 + x108 + x229 + x187 + x289 + x265 + x34 + x41 <= 1
c239: x5 + x115 + x82 + x178 + x55 <= 1
c240: x5 + x120 + x275 + x121 <= 1
c241: x5 + x125 + x113 + x178 <= 1
c242: x5 + x131 + x113 + x34 + x96 <= 1
c243: x5 + x135 + x113 + x178 <= 1
c244: x5 + x137 + x113 + x164 + x265 <= 1
c245: x5 + x157 + x113 + x248 + x186 <= 1
c246: x5 + x159 + x229 + x275 + x72 <= 1
c247: x5 + x162 + x275 + x229 + x187 <= 1
c248: x5 + x163 + x229 + x47 + x158 <= 1
c249: x5 + x166 + x113 + x82 <= 1
c250: x5 + x185 + x113 + x82 + x118 <= 1
c251: x5 + x192 + x229 + x69 + x72 + x202 <= 1
c252: x5 + x195 + x187 + x210 + x108 <= 1
c253: x5 + x200 + x113 + x210 <= 1
c254: x5 + x211 + x275 + x121 <= 1
c255: x5 + x220 + x113 + x210 + x7 <= 1
c256: x5 + x227 + x187 + x289 <= 1
c257: x5 + x231 + x211 + x121 + x265 <= 1
c258: x5 + x250 + x187 + x69 <= 1
c259: x5 + x276 + x275 + x229 + x41 <= 1
c260: x6 + x13 + x113 + x71 + x96 <= 1
c261: x6 + x17 + x234 + x29 + x194 + x151 <= 1
c262: x6 + x18 + x189 + x207 + x141 <= 1
c263: x6 + x31 + x234 + x249 + x99 + x242 <= 1
c264: x6 + x33 + x234 + x198 + x242 <= 1
c265: x6 + x41 + x189 + x29 + x61 <= 1
c266: x6 + x45 + x300 + x127 <= 1
c267: x6 + x49 + x17 <= 1
c268: x6 + x54 + x234 + x249 + x284 + x210 <= 1
c269: x6 + x55 + x17 + x113 + x29 <= 1
c270: x6 + x62 + x17 + x78 + x169 <= 1
c271: x6 + x66 + x17 + x169 + x238 <= 1
c272: x6 + x73 + x207 + x189 + x242 + x278 <= 1
c273: x6 + x82 + x17 + x113 + x169 + x238 <= 1
c274: x6 + x84 + x207 + x249 + x99 <= 1
c275: x6 + x87 + x207 + x300 + x82 + x96 <= 1
c276: x6 + x88 + x17 + x46 + x65 + x129 <= 1
c277: x6 + x91 + x189 + x207 + x212 + x278 <= 1
c278: x6 + x105 + x17 + x113 + x169 + x238 <= 1
c279: x6 + x107 + x189 + x113 + x73 <= 1
c280: x6 + x120 + x143 + x198 <= 1
c281: x6 + x136 + x295 + x141 + x66 <= 1
c282: x6 + x144 + x17 + x194 + x65 + x129 <= 1
c283: x6 + x149 + x46 + x78 + x93 <= 1
c284: x6 + x152 + x249 + x207 + x300 <= 1
c285: x6 + x156 + x234 + x207 + x12 + x278 <= 1
c286: x6 + x157 + x234 + x99 + x198 + x242 <= 1
c287: x6 + x158 + x198 + x210 + x270 <= 1
c288: x6 + x162 + x113 + x295 + x64 <= 1
c289: x6 + x176 + x17 + x78 + x283 <= 1
c290: x6 + x181 + x249 + x295 + x66 + x169 <= 1
c291: x6 + x188 + x189 + x113 + x73 <= 1
c292: x6 + x195 + x99 + x143 + x284 + x71 <= 1
c293: x6 + x200 + x189 + x78 + x210 + x278 <= 1
c294: x6 + x208 + x189 + x141 + x12 <= 1
c295: x6 + x211 + x46 + x127 + x277 <= 1
c296: x6 + x213 + x17 + x46 <= 1
c297: x6 + x218 + x234 + x249 + x300 <= 1
c298: x6 + x219 + x17 + x224 + x78 + x210 <= 1
c299: x6 + x235 + x141 + x194 + x195 + x206 <= 1
c300: x6 + x239 + x61 + x198 + x65 <= 1
c301: x6 + x245 + x234 + x29 + x194 <= 1
c302: x6 + x246 + x234 + x233 + x288 <= 1
c303: x6 + x261 + x152 + x230 + x12 <= 1
c304: x6 + x267 + x46 + x127 <= 1
c305: x6 + x268 + x189 + x295 + x12 <= 1
c306: x6 + x279 + x99 + x230 + x284 <= 1
c307: x6 + x286 + x17 + x189 + x242 + x278 <= 1
c308: x7 + x11 + x275 + x128 + x85 <= 1
c309: x7 + x13 + x11 + x86 + x60 <= 1
c310: x7 + x18 + x85 + x154 + x241 + x216 <= 1
c311: x7 + x20 + x275 + x60 + x94 <= 1
c312: x7 + x22 + x257 + x201 + x173 + x60 <= 1
c313: x7 + x27 + x86 + x92 + x241 + x198 <= 1
c314: x7 + x30 + x201 <= 1
c315: x7 + x31 + x275 + x222 <= 1
c316: x7 + x43 + x201 + x11 <= 1
c317: x7 + x44 + x275 + x276 + x94 <= 1
c318: x7 + x45 + x128 + x11 + x300 + x80 <= 1
c319: x7 + x65 + x85 + x11 + x241 <= 1
c320: x7 + x68 + x248 + x212 <= 1
c321: x7 + x77 + x249 + x152 + x132 + x131 <= 1
c322: x7 + x79 + x275 + x128 + x164 + x80 <= 1
c323: x7 + x87 + x85 + x128 + x300 <= 1
c324: x7 + x88 + x257 + x201 + x147 <= 1
c325: x7 + x97 + x257 + x113 + x222 + x217 <= 1
c326: x7 + x99 + x275 + x85 + x198 + x109 <= 1
c327: x7 + x138 + x201 + x154 <= 1
c328: x7 + x148 + x275 + x85 + x11 + x216 <= 1
c329: x7 + x158 + x128 + x248 + x210 <= 1
c330: x7 + x165 + x257 + x113 + x152 + x132 <= 1
c331: x7 + x181 + x128 + x11 + x210 <= 1
c332: x7 + x185 + x86 + x11 <= 1
c333: x7 + x190 + x128 + x275 <= 1
c334: x7 + x191 + x173 + x212 + x222 + x195 <= 1
c335: x7 + x199 + x257 + x173 + x147 + x132 <= 1
c336: x7 + x202 + x86 + x92 <= 1
c337: x7 + x203 + x85 + x128 + x275 <= 1
c338: x7 + x209 + x257 + x249 <= 1
c339: x7 + x213 + x128 + x248 + x113 <= 1
c340: x7 + x225 + x154 + x241 + x191 + x132 <= 1
c341: x7 + x237 + x27 + x241 <= 1
c342: x7 + x245 + x86 + x92 + x164 <= 1
c343: x7 + x273 + x92 + x27 + x241 + x198 <= 1
c344: x8 + x9 + x10 + x74 + x111 + x212 <= 1
c345: x8 + x15 + x228 + x16 + x157 + x238 <= 1
c346: x8 + x20 + x228 + x16 + x258 + x178 + x202 <= 1
c347: x8 + x27 + x10 + x9 + x114 <= 1
c348: x8 + x28 + x10 + x9 + x187 <= 1
c349: x8 + x29 + x229 + x112 + x134 + x201 + x88 <= 1
c350: x8 + x32 + x10 + x102 + x282 + x212 <= 1
c351: x8 + x35 + x167 + x140 + x114 <= 1
c352: x8 + x55 + x167 + x140 + x78 <= 1
c353: x8 + x56 + x102 + x230 + x279 <= 1
c354: x8 + x83 + x116 + x282 <= 1
c355: x8 + x84 + x74 + x229 + x86 + x265 + x238 <= 1
c356: x8 + x91 + x228 + x112 + x23 + x189 + x212 <= 1
c357: x8 + x92 + x10 + x130 + x86 + x265 <= 1
c358: x8 + x101 + x227 + x74 + x189 + x157 <= 1
c359: x8 + x106 + x10 + x74 + x282 + x86 <= 1
c360: x8 + x133 + x9 + x229 + x187 + x112 <= 1
c361: x8 + x141 + x10 + x134 + x154 + x169 <= 1
c362: x8 + x147 + x167 + x187 + x275 <= 1
c363: x8 + x150 + x10 + x155 + x74 + x282 + x86 <= 1
c364: x8 + x160 + x167 + x140 + x93 + x154 <= 1
c365: x8 + x162 + x9 + x229 + x187 <= 1
c366: x8 + x164 + x16 + x282 + x15 + x88 <= 1
c367: x8 + x171 + x229 + x187 + x112 + x86 <= 1
c368: x8 + x181 + x10 + x155 + x187 + x169 + x154 <= 1
c369: x8 + x196 + x228 + x114 + x275 <= 1
c370: x8 + x197 + x10 + x168 + x186 + x150 + x214 <= 1
c371: x8 + x199 + x227 + x12 + x80 <= 1
c372: x8 + x205 + x227 + x9 + x112 <= 1
c373: x8 + x206 + x234 + x29 + x194 + x300 + x6 <= 1
c374: x8 + x211 + x101 + x155 + x140 + x189 <= 1
c375: x8 + x215 + x167 + x116 + x27 + x150 <= 1
c376: x8 + x218 + x10 + x114 + x275 <= 1
c377: x8 + x224 + x74 + x23 + x300 <= 1
c378: x8 + x246 + x16 + x230 + x12 + x186 <= 1
c379: x8 + x264 + x228 + x201 + x140 + x78 <= 1
c380: x8 + x266 + x9 + x74 + x169 + x140 <= 1
c381: x8 + x267 + x46 + x116 + x166 <= 1
c382: x8 + x291 + x229 + x114 + x275 <= 1
c383: x9 + x11 + x142 + x90 + x148 <= 1
c384: x9 + x14 + x253 + x227 + x187 <= 1
c385: x9 + x26 + x142 + x47 + x257 <= 1
c386: x9 + x37 + x10 + x74 + x111 <= 1
c387: x9 + x41 + x254 + x69 + x128 + x140 <= 1
c388: x9 + x54 + x10 + x72 + x74 <= 1
c389: x9 + x57 + x207 + x69 + x132 <= 1
c390: x9 + x58 + x142 + x11 + x111 <= 1
c391: x9 + x60 + x10 + x289 + x72 + x74 <= 1
c392: x9 + x64 + x100 + x227 + x253 + x187 + x154 <= 1
c393: x9 + x71 + x248 + x37 + x148 + x202 <= 1
c394: x9 + x78 + x142 + x229 + x90 <= 1
c395: x9 + x80 + x142 + x229 + x118 + x74 <= 1
c396: x9 + x89 + x184 + x72 + x27 <= 1
c397: x9 + x99 + x10 + x289 + x114 <= 1
c398: x9 + x107 + x10 + x37 <= 1
c399: x9 + x119 + x100 + x266 <= 1
c400: x9 + x120 + x184 + x295 + x128 + x11 <= 1
c401: x9 + x124 + x10 + x72 + x74 <= 1
c402: x9 + x131 + x227 + x289 <= 1
c403: x9 + x138 + x142 + x229 + x69 + x187 <= 1
c404: x9 + x156 + x142 + x203 + x278 <= 1
c405: x9 + x157 + x100 + x207 + x69 + x114 + x252 <= 1
c406: x9 + x158 + x10 + x64 + x60 <= 1
c407: x9 + x159 + x100 + x229 + x72 <= 1
c408: x9 + x164 + x142 + x47 + x74 <= 1
c409: x9 + x180 + x10 + x90 + x289 + x60 <= 1
c410: x9 + x185 + x142 + x69 + x118 + x202 <= 1
c411: x9 + x188 + x99 <= 1
c412: x9 + x196 + x47 + x257 + x132 <= 1
c413: x9 + x198 + x142 + x118 + x74 <= 1
c414: x9 + x219 + x284 + x289 + x187 <= 1
c415: x9 + x221 + x47 + x253 + x229 <= 1
c416: x9 + x226 + x257 + x47 <= 1
c417: x9 + x245 + x254 + x90 + x148 <= 1
c418: x9 + x247 + x227 + x64 <= 1
c419: x9 + x250 + x248 + x158 + x202 <= 1
c420: x9 + x260 + x227 + x37 + x111 <= 1
c421: x9 + x263 + x254 + x64 + x148 <= 1
c422: x9 + x265 + x142 + x257 + x266 + x74 <= 1
c423: x9 + x268 + x142 + x148 + x80 <= 1
c424: x9 + x270 + x10 + x295 + x99 + x169 <= 1
c425: x9 + x281 + x289 + x72 <= 1
c426: x9 + x287 + x253 + x100 + x229 <= 1
c427: x9 + x293 + x184 + x72 <= 1
c428: x9 + x294 + x254 + x69 + x41 + x132 <= 1
c429: x9 + x297 + x64 + x295 + x11 + x162 <= 1
c430: x9 + x300 + x142 + x257 + x74 <= 1
c431: x10 + x12 + x50 + x183 + x134 + x155 + x278 <= 1
c432: x10 + x18 + x95 + x85 + x127 + x155 <= 1
c433: x10 + x23 + x121 + x242 + x269 <= 1
c434: x10 + x33 + x85 + x121 + x275 + x132 <= 1
c435: x10 + x36 + x50 + x85 + x155 + x64 <= 1
c436: x10 + x45 + x183 + x258 + x127 + x269 <= 1
c437: x10 + x46 + x95 + x50 + x183 + x132 <= 1
c438: x10 + x49 + x121 + x241 + x282 + x191 <= 1
c439: x10 + x51 + x50 + x183 + x37 <= 1
c440: x10 + x52 + x82 + x258 + x241 + x282 + x269 <= 1
c441: x10 + x61 + x134 + x72 + x65 + x154 <= 1
c442: x10 + x68 + x95 + x168 + x130 + x183 <= 1
c443: x10 + x73 + x50 + x85 + x113 + x132 <= 1
c444: x10 + x78 + x95 + x183 + x46 + x82 <= 1
c445: x10 + x79 + x95 + x50 + x141 + x132 <= 1
c446: x10 + x88 + x51 + x92 + x37 <= 1
c447: x10 + x89 + x230 + x132 <= 1
c448: x10 + x110 + x95 + x102 + x72 <= 1
c449: x10 + x122 + x95 + x168 + x183 <= 1
c450: x10 + x125 + x51 + x289 + x148 <= 1
c451: x10 + x137 + x50 + x85 + x36 + x64 <= 1
c452: x10 + x147 + x50 + x253 + x73 + x111 <= 1
c453: x10 + x152 + x230 + x85 + x12 + x148 <= 1
c454: x10 + x170 + x102 + x90 + x289 + x132 <= 1
c455: x10 + x172 + x168 + x121 + x60 <= 1
c456: x10 + x174 + x32 + x230 + x134 + x186 <= 1
c457: x10 + x177 + x130 + x36 + x127 <= 1
c458: x10 + x179 + x46 + x258 + x148 <= 1
c459: x10 + x192 + x155 + x85 + x12 + x72 <= 1
c460: x10 + x195 + x183 + x46 + x258 <= 1
c461: x10 + x209 + x50 + x46 + x72 <= 1
c462: x10 + x213 + x51 + x177 <= 1
c463: x10 + x215 + x130 + x152 + x12 + x148 <= 1
c464: x10 + x221 + x95 + x183 + x253 + x82 <= 1
c465: x10 + x223 + x95 + x183 + x127 <= 1
c466: x10 + x226 + x36 + x127 + x37 <= 1
c467: x10 + x231 + x242 + x121 + x186 <= 1
c468: x10 + x235 + x242 + x23 + x278 <= 1
c469: x10 + x240 + x61 + x258 + x282 + x72 <= 1
c470: x10 + x244 + x141 + x241 + x110 <= 1
c471: x10 + x245 + x86 + x92 + x186 <= 1
c472: x10 + x247 + x95 + x86 <= 1
c473: x10 + x263 + x102 + x64 + x148 <= 1
c474: x10 + x268 + x61 + x23 + x212 + x223 <= 1
c475: x10 + x271 + x95 + x155 + x183 + x127 <= 1
c476: x10 + x272 + x168 + x183 + x99 <= 1
c477: x10 + x283 + x155 + x295 + x60 + x86 <= 1
c478: x10 + x298 + x50 + x158 <= 1
c479: x11 + x12 + x16 + x108 + x288 + x230 <= 1
c480: x11 + x25 + x39 + x242 <= 1
c481: x11 + x32 + x39 + x173 <= 1
c482: x11 + x35 + x39 + x194 + x211 <= 1
c483: x11 + x36 + x16 + x142 + x85 <= 1
c484: x11 + x38 + x108 + x194 + x12 <= 1
c485: x11 + x41 + x232 + x276 + x128 + x275 <= 1
c486: x11 + x42 + x232 + x16 <= 1
c487: x11 + x54 + x216 + x113 + x266 <= 1
c488: x11 + x91 + x232 + x288 <= 1
c489: x11 + x104 + x232 + x128 <= 1
c490: x11 + x106 + x216 + x169 + x64 + x113 + x148 <= 1
c491: x11 + x109 + x276 + x168 + x288 <= 1
c492: x11 + x117 + x232 + x95 + x230 + x64 <= 1
c493: x11 + x123 + x16 + x242 + x230 + x64 <= 1
c494: x11 + x129 + x201 + x60 + x72 + x172 + x218 <= 1
c495: x11 + x133 + x216 + x90 + x272 <= 1
c496: x11 + x141 + x39 + x194 + x267 <= 1
c497: x11 + x146 + x35 + x284 + x36 <= 1
c498: x11 + x147 + x173 + x201 + x14 <= 1
c499: x11 + x155 + x108 + x194 + x211 <= 1
c500: x11 + x156 + x142 + x16 <= 1
c501: x11 + x157 + x276 + x95 + x189 + x271 <= 1
c502: x11 + x158 + x184 + x216 + x64 <= 1
c503: x11 + x160 + x142 + x85 <= 1
c504: x11 + x171 + x39 + x173 + x201 <= 1
c505: x11 + x188 + x108 + x194 + x155 <= 1
c506: x11 + x209 + x184 + x216 + x90 <= 1
c507: x11 + x213 + x142 + x25 <= 1
c508: x11 + x225 + x39 + x35 + x242 + x230 <= 1
c509: x11 + x231 + x39 + x211 <= 1
c510: x11 + x237 + x168 + x276 + x95 <= 1
c511: x11 + x244 + x39 + x194 + x141 <= 1
c512: x11 + x252 + x142 + x181 + x242 <= 1
c513: x11 + x260 + x16 + x284 + x270 <= 1
c514: x11 + x273 + x117 + x169 + x64 <= 1
c515: x11 + x294 + x39 + x41 + x276 + x241 <= 1
c516: x11 + x296 + x232 + x41 + x271 <= 1
c517: x11 + x298 + x181 + x201 + x72 <= 1
c518: x12 + x13 + x236 + x227 + x288 <= 1
c519: x12 + x14 + x167 + x17 + x52 <= 1
c520: x12 + x35 + x236 + x167 + x17 + x154 <= 1
c521: x12 + x41 + x53 + x34 + x277 + x265 <= 1
c522: x12 + x62 + x53 + x143 + x248 + x71 <= 1
c523: x12 + x64 + x261 + x34 + x16 + x230 <= 1
c524: x12 + x70 + x167 + x236 + x222 <= 1
c525: x12 + x90 + x17 + x100 + x61 + x194 <= 1
c526: x12 + x97 + x234 + x112 + x217 + x227 <= 1
c527: x12 + x104 + x143 + x15 + x186 <= 1
c528: x12 + x115 + x53 + x17 + x224 + x85 <= 1
c529: x12 + x133 + x261 + x243 + x134 + x183 <= 1
c530: x12 + x137 + x236 + x50 + x266 + x85 <= 1
c531: x12 + x139 + x234 + x34 + x6 <= 1
c532: x12 + x149 + x143 + x248 + x265 <= 1
c533: x12 + x160 + x167 + x243 + x202 + x106 + x8 <= 1
c534: x12 + x164 + x236 + x275 + x222 <= 1
c535: x12 + x168 + x143 + x227 + x85 + x72 + x192 <= 1
c536: x12 + x170 + x234 + x207 + x112 <= 1
c537: x12 + x171 + x53 + x17 + x14 <= 1
c538: x12 + x172 + x234 + x207 + x121 <= 1
c539: x12 + x174 + x143 + x243 + x156 <= 1
c540: x12 + x176 + x167 + x17 + x216 + x194 <= 1
c541: x12 + x221 + x53 + x15 + x134 <= 1
c542: x12 + x226 + x34 + x37 + x52 <= 1
c543: x12 + x231 + x17 + x100 + x154 <= 1
c544: x12 + x239 + x236 + x248 + x23 + x202 <= 1
c545: x12 + x252 + x254 + x152 + x134 + x230 <= 1
c546: x12 + x259 + x167 + x236 + x275 <= 1
c547: x12 + x274 + x234 + x112 + x70 <= 1
c548: x12 + x280 + x224 + x17 + x289 + x265 <= 1
c549: x12 + x283 + x234 + x295 + x86 <= 1
c550: x12 + x287 + x53 + x34 + x100 + x139 <= 1
c551: x12 + x294 + x224 + x53 + x121 + x100 + x85 <= 1
c552: x12 + x298 + x224 + x50 + x254 + x300 <= 1
c553: x12 + x299 + x236 + x248 + x50 + x265 <= 1
c554: x13 + x15 + x144 + x94 + x276 <= 1
c555: x13 + x18 + x178 + x203 + x148 <= 1
c556: x13 + x22 + x81 + x173 + x50 + x148 <= 1
c557: x13 + x25 + x47 + x34 + x95 + x148 <= 1
c558: x13 + x30 + x47 + x15 + x25 <= 1
c559: x13 + x46 + x94 + x112 + x50 <= 1
c560: x13 + x51 + x92 + x136 + x96 <= 1
c561: x13 + x62 + x178 + x108 + x187 <= 1
c562: x13 + x72 + x144 + x258 + x227 <= 1
c563: x13 + x74 + x47 + x173 + x203 + x60 + x148 <= 1
c564: x13 + x83 + x81 + x86 <= 1
c565: x13 + x87 + x144 + x94 + x168 <= 1
c566: x13 + x106 + x92 + x86 + x112 <= 1
c567: x13 + x133 + x81 + x92 + x86 <= 1
c568: x13 + x134 + x178 + x113 + x203 <= 1
c569: x13 + x138 + x94 + x187 + x50 + x1 <= 1
c570: x13 + x147 + x236 + x187 + x50 <= 1
c571: x13 + x180 + x94 + x60 + x86 + x168 <= 1
c572: x13 + x181 + x94 + x187 <= 1
c573: x13 + x186 + x108 + x173 + x92 <= 1
c574: x13 + x216 + x81 + x22 + x50 + x148 <= 1
c575: x13 + x225 + x81 + x132 + x280 <= 1
c576: x13 + x244 + x178 + x94 + x187 <= 1
c577: x13 + x246 + x108 + x288 + x186 + x50 + x12 <= 1
c578: x13 + x251 + x46 + x258 + x227 <= 1
c579: x13 + x252 + x47 + x236 + x50 <= 1
c580: x13 + x255 + x144 + x108 <= 1
c581: x13 + x263 + x144 + x34 + x108 + x1 <= 1
c582: x13 + x265 + x51 + x34 + x187 + x87 <= 1
c583: x13 + x269 + x144 + x258 + x87 <= 1
c584: x13 + x294 + x144 + x34 + x1 <= 1
c585: x13 + x298 + x96 + x181 <= 1
c586: x13 + x299 + x22 + x173 + x50 <= 1
c587: x14 + x24 + x292 + x196 + x244 <= 1
c588: x14 + x26 + x249 + x201 + x89 <= 1
c589: x14 + x38 + x167 + x173 + x238 <= 1
c590: x14 + x44 + x233 + x249 + x253 + x94 + x187 <= 1
c591: x14 + x54 + x292 + x69 + x72 <= 1
c592: x14 + x57 + x66 + x211 + x155 + x34 <= 1
c593: x14 + x59 + x285 + x69 + x238 + x2 <= 1
c594: x14 + x61 + x279 + x117 + x65 + x214 <= 1
c595: x14 + x67 + x66 + x117 + x136 <= 1
c596: x14 + x78 + x292 + x69 + x173 + x202 <= 1
c597: x14 + x83 + x232 + x69 + x132 <= 1
c598: x14 + x87 + x232 + x293 <= 1
c599: x14 + x104 + x232 + x233 + x69 <= 1
c600: x14 + x115 + x292 + x53 + x121 + x203 + x221 <= 1
c601: x14 + x120 + x143 + x248 + x52 + x265 <= 1
c602: x14 + x125 + x232 + x69 + x220 <= 1
c603: x14 + x126 + x232 + x233 + x249 + x288 <= 1
c604: x14 + x146 + x66 + x155 + x95 + x86 <= 1
c605: x14 + x148 + x67 + x127 + x173 <= 1
c606: x14 + x150 + x67 + x216 + x78 <= 1
c607: x14 + x156 + x143 + x196 + x241 + x244 <= 1
c608: x14 + x164 + x285 + x232 + x69 + x220 <= 1
c609: x14 + x180 + x167 + x17 + x57 <= 1
c610: x14 + x213 + x66 + x67 + x230 <= 1
c611: x14 + x217 + x279 + x127 <= 1
c612: x14 + x225 + x285 + x248 + x230 <= 1
c613: x14 + x240 + x67 + x127 <= 1
c614: x14 + x263 + x279 + x66 + x117 <= 1
c615: x14 + x272 + x66 + x17 + x238 <= 1
c616: x14 + x283 + x67 + x66 <= 1
c617: x14 + x287 + x53 + x143 + x1 <= 1
c618: x14 + x298 + x67 + x66 + x230 <= 1
c619: x14 + x299 + x233 + x65 + x270 <= 1
c620: x15 + x19 + x118 + x198 + x141 <= 1
c621: x15 + x22 + x228 + x53 + x202 <= 1
c622: x15 + x42 + x77 + x127 + x59 + x154 <= 1
c623: x15 + x43 + x228 + x264 + x141 <= 1
c624: x15 + x50 + x118 + x210 + x22 <= 1
c625: x15 + x57 + x101 + x144 <= 1
c626: x15 + x66 + x101 + x264 + x198 <= 1
c627: x15 + x71 + x118 + x210 <= 1
c628: x15 + x78 + x228 + x182 + x264 <= 1
c629: x15 + x85 + x289 + x16 + x198 + x96 <= 1
c630: x15 + x89 + x191 + x282 + x74 <= 1
c631: x15 + x97 + x222 + x191 + x238 + x172 <= 1
c632: x15 + x105 + x182 + x238 <= 1
c633: x15 + x110 + x228 + x182 + x53 <= 1
c634: x15 + x117 + x118 + x144 + x1 <= 1
c635: x15 + x123 + x243 + x143 + x22 <= 1
c636: x15 + x129 + x228 + x144 + x194 + x141 <= 1
c637: x15 + x138 + x71 + x264 + x66 + x134 <= 1
c638: x15 + x148 + x228 + x194 + x127 <= 1
c639: x15 + x171 + x77 + x293 + x274 <= 1
c640: x15 + x193 + x228 + x53 + x202 <= 1
c641: x15 + x199 + x207 + x53 + x157 <= 1
c642: x15 + x208 + x282 + x243 + x1 <= 1
c643: x15 + x209 + x101 + x144 + x276 <= 1
c644: x15 + x216 + x47 + x74 + x267 + x148 <= 1
c645: x15 + x223 + x210 + x47 <= 1
c646: x15 + x225 + x207 + x16 + x272 + x293 <= 1
c647: x15 + x237 + x228 + x194 + x129 <= 1
c648: x15 + x241 + x261 + x191 <= 1
c649: x15 + x254 + x118 + x175 + x117 + x202 <= 1
c650: x15 + x291 + x101 + x144 <= 1
c651: x15 + x294 + x222 + x264 + x172 <= 1
c652: x16 + x25 + x228 + x178 + x82 + x113 <= 1
c653: x16 + x27 + x116 + x167 + x142 + x238 <= 1
c654: x16 + x28 + x261 + x27 + x69 <= 1
c655: x16 + x32 + x178 + x261 + x230 <= 1
c656: x16 + x52 + x116 + x167 + x34 + x202 <= 1
c657: x16 + x53 + x292 + x207 + x242 + x186 + x157 <= 1
c658: x16 + x57 + x163 + x236 + x238 <= 1
c659: x16 + x65 + x233 + x249 + x236 <= 1
c660: x16 + x71 + x232 + x233 + x64 <= 1
c661: x16 + x72 + x260 + x282 + x258 + x227 <= 1
c662: x16 + x84 + x116 + x281 + x230 <= 1
c663: x16 + x95 + x116 + x130 + x178 + x202 <= 1
c664: x16 + x97 + x232 + x233 + x69 <= 1
c665: x16 + x107 + x167 + x284 + x113 <= 1
c666: x16 + x111 + x232 + x163 + x288 + x230 <= 1
c667: x16 + x122 + x62 + x169 + x64 <= 1
c668: x16 + x132 + x145 + x258 + x20 + x214 <= 1
c669: x16 + x137 + x232 + x64 + x71 <= 1
c670: x16 + x139 + x233 + x53 + x97 <= 1
c671: x16 + x146 + x62 + x282 + x248 <= 1
c672: x16 + x149 + x130 + x178 <= 1
c673: x16 + x150 + x116 + x167 + x27 + x8 <= 1
c674: x16 + x159 + x62 + x36 + x130 + x198 <= 1
c675: x16 + x171 + x292 + x270 + x69 <= 1
c676: x16 + x182 + x228 + x36 + x20 <= 1
c677: x16 + x185 + x142 + x233 + x108 + x186 <= 1
c678: x16 + x195 + x228 + x178 + x62 + x69 + x157 <= 1
c679: x16 + x197 + x116 + x167 + x142 <= 1
c680: x16 + x220 + x261 + x289 + x96 + x34 <= 1
c681: x16 + x221 + x82 + x130 + x95 <= 1
c682: x16 + x223 + x116 + x260 + x95 <= 1
c683: x16 + x247 + x116 + x178 + x95 + x202 <= 1
c684: x16 + x256 + x32 + x282 + x157 <= 1
c685: x16 + x265 + x228 + x62 + x248 + x36 <= 1
c686: x16 + x283 + x158 + x228 <= 1
c687: x16 + x286 + x232 + x164 <= 1
c688: x16 + x287 + x284 + x113 + x270 <= 1
c689: x17 + x19 + x184 + x128 <= 1
c690: x17 + x21 + x29 + x151 + x81 + x234 + x85 <= 1
c691: x17 + x25 + x128 + x115 + x61 <= 1
c692: x17 + x26 + x151 + x194 + x62 <= 1
c693: x17 + x30 + x184 + x46 + x210 + x95 <= 1
c694: x17 + x32 + x101 + x277 + x151 + x66 <= 1
c695: x17 + x37 + x29 + x184 + x178 + x95 <= 1
c696: x17 + x40 + x151 + x92 + x194 + x216 <= 1
c697: x17 + x44 + x101 + x90 <= 1
c698: x17 + x58 + x93 + x100 + x140 + x154 <= 1
c699: x17 + x59 + x102 + x224 + x238 <= 1
c700: x17 + x60 + x102 + x140 + x289 + x90 <= 1
c701: x17 + x68 + x234 + x52 + x272 <= 1
c702: x17 + x74 + x204 + x224 + x191 + x216 + x172 <= 1
c703: x17 + x110 + x93 + x101 + x66 + x140 <= 1
c704: x17 + x111 + x93 + x232 + x289 <= 1
c705: x17 + x123 + x189 + x224 + x243 + x134 + x12 <= 1
c706: x17 + x124 + x81 + x35 <= 1
c707: x17 + x126 + x46 + x82 + x115 <= 1
c708: x17 + x132 + x253 + x81 + x191 + x154 <= 1
c709: x17 + x153 + x93 + x128 + x210 + x92 <= 1
c710: x17 + x168 + x204 + x35 + x140 <= 1
c711: x17 + x185 + x46 + x82 <= 1
c712: x17 + x187 + x277 + x243 + x128 <= 1
c713: x17 + x192 + x60 + x65 <= 1
c714: x17 + x214 + x222 + x251 <= 1
c715: x17 + x221 + x184 + x82 + x46 + x65 + x95 <= 1
c716: x17 + x228 + x29 + x81 + x37 <= 1
c717: x17 + x241 + x204 + x167 + x251 <= 1
c718: x17 + x248 + x204 + x128 + x140 + x172 <= 1
c719: x17 + x252 + x29 + x236 <= 1
c720: x17 + x255 + x82 + x144 + x184 <= 1
c721: x17 + x262 + x234 + x194 + x92 <= 1
c722: x17 + x263 + x102 + x210 + x132 <= 1
c723: x17 + x270 + x102 + x210 + x113 + x132 <= 1
c724: x17 + x271 + x169 + x224 + x134 <= 1
c725: x18 + x22 + x114 + x207 + x69 <= 1
c726: x18 + x24 + x292 + x162 + x278 <= 1
c727: x18 + x30 + x155 + x182 + x53 + x278 <= 1
c728: x18 + x38 + x207 + x53 + x278 <= 1
c729: x18 + x51 + x114 + x207 <= 1
c730: x18 + x65 + x114 + x182 + x241 <= 1
c731: x18 + x68 + x217 + x277 + x195 + x53 <= 1
c732: x18 + x73 + x93 + x207 + x278 + x6 <= 1
c733: x18 + x86 + x73 + x189 + x69 <= 1
c734: x18 + x112 + x118 + x141 + x238 + x2 <= 1
c735: x18 + x115 + x73 + x93 + x278 <= 1
c736: x18 + x120 + x114 + x207 + x69 <= 1
c737: x18 + x129 + x203 + x66 + x178 <= 1
c738: x18 + x132 + x73 + x253 + x180 + x10 <= 1
c739: x18 + x160 + x169 + x66 + x238 <= 1
c740: x18 + x164 + x73 + x169 + x238 <= 1
c741: x18 + x170 + x114 + x207 + x69 <= 1
c742: x18 + x184 + x203 + x178 + x148 <= 1
c743: x18 + x185 + x118 + x155 + x127 + x182 <= 1
c744: x18 + x188 + x73 + x189 + x6 <= 1
c745: x18 + x191 + x51 + x93 + x154 <= 1
c746: x18 + x213 + x51 + x296 <= 1
c747: x18 + x218 + x114 + x253 + x10 <= 1
c748: x18 + x227 + x217 + x112 <= 1
c749: x18 + x237 + x73 + x207 + x132 <= 1
c750: x18 + x244 + x292 + x141 + x241 <= 1
c751: x18 + x262 + x155 + x292 + x65 + x278 <= 1
c752: x19 + x25 + x275 + x73 + x278 <= 1
c753: x19 + x28 + x99 + x275 + x187 <= 1
c754: x19 + x30 + x39 + x25 <= 1
c755: x19 + x44 + x233 + x131 + x1 <= 1
c756: x19 + x51 + x39 + x264 <= 1
c757: x19 + x62 + x99 + x73 + x169 + x1 <= 1
c758: x19 + x84 + x99 + x155 + x230 + x278 <= 1
c759: x19 + x92 + x282 + x80 + x28 <= 1
c760: x19 + x95 + x275 + x233 + x66 <= 1
c761: x19 + x109 + x300 + x282 + x206 <= 1
c762: x19 + x117 + x118 + x254 + x155 + x230 + x202 <= 1
c763: x19 + x159 + x99 + x275 + x198 + x169 <= 1
c764: x19 + x162 + x300 + x187 <= 1
c765: x19 + x171 + x39 + x233 <= 1
c766: x19 + x173 + x39 + x118 <= 1
c767: x19 + x193 + x118 + x233 + x1 <= 1
c768: x19 + x216 + x131 + x184 + x2 <= 1
c769: x19 + x227 + x300 + x80 + x282 <= 1
c770: x19 + x231 + x39 + x131 + x230 <= 1
c771: x19 + x289 + x99 + x275 + x187 + x198 <= 1
c772: x20 + x27 + x145 + x100 + x64 + x50 <= 1
c773: x20 + x29 + x67 + x275 <= 1
c774: x20 + x35 + x284 + x143 + x99 <= 1
c775: x20 + x39 + x29 + x269 + x178 <= 1
c776: x20 + x51 + x279 + x191 + x132 <= 1
c777: x20 + x61 + x279 + x284 + x68 <= 1
c778: x20 + x65 + x279 + x94 + x105 + x1 <= 1
c779: x20 + x71 + x60 + x121 <= 1
c780: x20 + x92 + x295 + x130 + x127 <= 1
c781: x20 + x95 + x183 + x29 + x189 + x202 <= 1
c782: x20 + x96 + x60 + x94 + x178 <= 1
c783: x20 + x102 + x67 + x60 + x289 <= 1
c784: x20 + x110 + x102 + x36 + x207 <= 1
c785: x20 + x147 + x279 + x61 + x68 <= 1
c786: x20 + x153 + x67 <= 1
c787: x20 + x154 + x295 + x189 + x127 <= 1
c788: x20 + x159 + x94 + x145 + x60 + x275 <= 1
c789: x20 + x185 + x183 + x258 + x289 <= 1
c790: x20 + x193 + x183 + x99 + x127 <= 1
c791: x20 + x196 + x67 + x208 + x132 <= 1
c792: x20 + x218 + x228 + x275 + x8 <= 1
c793: x20 + x240 + x295 + x189 + x127 <= 1
c794: x20 + x260 + x279 + x284 + x214 + x69 <= 1
c795: x20 + x267 + x260 + x100 + x214 + x65 <= 1
c796: x20 + x272 + x183 + x102 + x289 <= 1
c797: x20 + x282 + x29 + x269 <= 1
c798: x20 + x286 + x183 + x99 + x182 <= 1
c799: x20 + x288 + x279 + x61 + x238 <= 1
c800: x20 + x294 + x196 + x145 + x132 <= 1
c801: x21 + x22 + x152 + x116 + x29 <= 1
c802: x21 + x23 + x114 + x242 + x81 + x185 <= 1
c803: x21 + x45 + x151 + x232 <= 1
c804: x21 + x47 + x229 + x142 + x238 <= 1
c805: x21 + x61 + x23 + x47 + x203 + x238 <= 1
c806: x21 + x65 + x229 + x181 + x114 <= 1
c807: x21 + x66 + x161 + x183 + x102 + x238 <= 1
c808: x21 + x77 + x152 + x253 + x132 <= 1
c809: x21 + x86 + x229 + x285 + x114 + x81 <= 1
c810: x21 + x95 + x77 + x253 + x132 + x1 <= 1
c811: x21 + x106 + x152 + x113 + x218 <= 1
c812: x21 + x112 + x229 + x234 + x241 + x260 <= 1
c813: x21 + x118 + x229 + x142 + x183 + x81 + x238 <= 1
c814: x21 + x127 + x23 + x112 + x113 <= 1
c815: x21 + x135 + x118 + x183 + x132 <= 1
c816: x21 + x147 + x23 + x152 + x253 + x132 <= 1
c817: x21 + x193 + x23 + x242 + x248 <= 1
c818: x21 + x194 + x229 + x234 + x242 + x207 <= 1
c819: x21 + x195 + x23 + x112 <= 1
c820: x21 + x198 + x285 + x203 + x232 <= 1
c821: x21 + x225 + x285 + x116 + x81 <= 1
c822: x21 + x227 + x152 + x253 <= 1
c823: x21 + x231 + x285 + x116 + x225 <= 1
c824: x21 + x289 + x229 + x114 + x232 <= 1
c825: x21 + x292 + x229 + x142 + x181 + x242 <= 1
c826: x21 + x294 + x151 + x112 + x241 + x85 <= 1
c827: x22 + x32 + x211 + x212 <= 1
c828: x22 + x36 + x257 + x82 + x142 + x115 <= 1
c829: x22 + x48 + x243 + x82 + x114 + x65 <= 1
c830: x22 + x70 + x201 + x74 + x60 <= 1
c831: x22 + x86 + x201 + x243 + x228 + x140 <= 1
c832: x22 + x93 + x212 + x284 + x2 <= 1
c833: x22 + x94 + x212 + x203 + x168 + x2 <= 1
c834: x22 + x95 + x257 + x212 + x82 + x1 <= 1
c835: x22 + x96 + x257 + x234 <= 1
c836: x22 + x97 + x257 + x143 + x29 + x265 <= 1
c837: x22 + x107 + x279 + x284 + x69 <= 1
c838: x22 + x126 + x32 + x282 + x148 <= 1
c839: x22 + x131 + x257 + x152 + x7 <= 1
c840: x22 + x153 + x211 + x210 + x140 <= 1
c841: x22 + x162 + x211 + x131 + x5 <= 1
c842: x22 + x163 + x175 + x284 + x202 <= 1
c843: x22 + x177 + x201 + x236 <= 1
c844: x22 + x179 + x279 + x284 <= 1
c845: x22 + x185 + x233 + x118 + x142 + x69 <= 1
c846: x22 + x188 + x152 + x233 + x246 + x216 <= 1
c847: x22 + x192 + x279 + x284 + x69 <= 1
c848: x22 + x195 + x210 + x284 <= 1
c849: x22 + x205 + x175 + x168 <= 1
c850: x22 + x213 + x116 + x94 + x142 + x233 <= 1
c851: x22 + x240 + x210 + x116 + x152 + x233 <= 1
c852: x22 + x241 + x201 + x60 + x86 + x7 <= 1
c853: x22 + x244 + x143 + x94 + x86 + x241 <= 1
c854: x22 + x271 + x257 + x96 <= 1
c855: x22 + x273 + x212 + x284 + x82 <= 1
c856: x22 + x283 + x60 + x143 + x86 + x69 <= 1
c857: x22 + x288 + x211 + x265 <= 1
c858: x22 + x296 + x93 + x18 <= 1
c859: x23 + x26 + x257 + x46 <= 1
c860: x23 + x27 + x261 + x46 + x116 + x241 <= 1
c861: x23 + x31 + x41 + x261 + x212 <= 1
c862: x23 + x35 + x257 + x108 + x300 + x140 <= 1
c863: x23 + x48 + x41 + x108 + x238 <= 1
c864: x23 + x52 + x47 + x121 + x60 + x203 <= 1
c865: x23 + x54 + x80 + x211 + x265 <= 1
c866: x23 + x55 + x41 + x121 + x47 <= 1
c867: x23 + x66 + x257 + x67 + x47 + x74 + x60 <= 1
c868: x23 + x68 + x144 + x211 + x108 + x152 <= 1
c869: x23 + x79 + x258 + x275 + x143 + x97 <= 1
c870: x23 + x88 + x41 + x74 + x108 <= 1
c871: x23 + x92 + x41 + x199 + x88 + x241 <= 1
c872: x23 + x94 + x224 + x277 + x265 <= 1
c873: x23 + x96 + x257 + x300 + x74 + x66 <= 1
c874: x23 + x98 + x91 + x27 + x203 <= 1
c875: x23 + x119 + x121 + x242 + x275 <= 1
c876: x23 + x123 + x224 + x243 + x189 + x12 <= 1
c877: x23 + x124 + x224 + x243 + x1 <= 1
c878: x23 + x126 + x46 + x258 + x207 <= 1
c879: x23 + x129 + x257 + x46 + x228 + x88 <= 1
c880: x23 + x131 + x184 + x224 + x211 <= 1
c881: x23 + x138 + x80 + x60 + x129 + x278 + x66 <= 1
c882: x23 + x139 + x261 + x67 + x81 + x132 <= 1
c883: x23 + x146 + x121 + x35 + x207 <= 1
c884: x23 + x155 + x248 + x253 + x187 + x275 <= 1
c885: x23 + x210 + x91 + x47 + x27 + x108 <= 1
c886: x23 + x221 + x121 + x47 + x203 <= 1
c887: x23 + x225 + x184 + x46 + x210 + x132 <= 1
c888: x23 + x252 + x114 + x236 + x156 + x207 <= 1
c889: x23 + x260 + x277 + x46 + x258 <= 1
c890: x23 + x280 + x224 + x238 + x265 <= 1
c891: x23 + x283 + x31 <= 1
c892: x23 + x287 + x300 + x97 + x12 <= 1
c893: x23 + x298 + x224 + x300 + x74 <= 1
c894: x24 + x28 + x249 + x234 + x132 <= 1
c895: x24 + x29 + x285 + x229 + x81 <= 1
c896: x24 + x34 + x249 + x229 + x90 + x60 <= 1
c897: x24 + x41 + x77 + x167 + x216 + x152 <= 1
c898: x24 + x43 + x77 + x216 <= 1
c899: x24 + x61 + x249 + x77 + x90 <= 1
c900: x24 + x71 + x210 + x248 + x230 + x278 <= 1
c901: x24 + x74 + x229 + x249 + x60 <= 1
c902: x24 + x82 + x196 + x138 <= 1
c903: x24 + x86 + x285 + x229 + x60 <= 1
c904: x24 + x97 + x136 + x196 + x132 <= 1
c905: x24 + x111 + x285 + x229 + x90 + x261 + x230 <= 1
c906: x24 + x131 + x167 + x77 + x216 + x152 <= 1
c907: x24 + x144 + x285 + x90 + x111 + x230 <= 1
c908: x24 + x159 + x167 + x152 <= 1
c909: x24 + x164 + x285 + x261 + x81 <= 1
c910: x24 + x168 + x249 + x210 + x230 <= 1
c911: x24 + x169 + x77 + x249 + x152 + x132 <= 1
c912: x24 + x179 + x196 + x138 <= 1
c913: x24 + x224 + x136 + x278 <= 1
c914: x24 + x227 + x279 + x144 + x230 <= 1
c915: x24 + x259 + x167 + x41 <= 1
c916: x24 + x274 + x285 + x90 + x111 + x144 <= 1
c917: x24 + x286 + x229 + x34 <= 1
c918: x24 + x294 + x196 + x292 <= 1
c919: x24 + x296 + x77 + x167 + x41 <= 1
c920: x25 + x27 + x166 + x142 + x82 <= 1
c921: x25 + x31 + x37 + x181 + x73 + x242 <= 1
c922: x25 + x43 + x161 + x234 + x278 <= 1
c923: x25 + x49 + x217 + x227 + x289 <= 1
c924: x25 + x52 + x84 + x217 + x180 <= 1
c925: x25 + x55 + x281 + x217 <= 1
c926: x25 + x56 + x78 + x142 <= 1
c927: x25 + x58 + x31 + x37 + x181 <= 1
c928: x25 + x71 + x161 + x115 + x278 <= 1
c929: x25 + x74 + x161 + x142 + x115 <= 1
c930: x25 + x83 + x186 + x73 + x86 <= 1
c931: x25 + x87 + x128 + x187 + x34 <= 1
c932: x25 + x91 + x39 + x118 + x112 <= 1
c933: x25 + x100 + x84 + x61 + x74 <= 1
c934: x25 + x110 + x178 + x129 + x228 + x17 <= 1
c935: x25 + x131 + x281 + x217 + x289 <= 1
c936: x25 + x135 + x166 + x113 <= 1
c937: x25 + x154 + x167 + x78 + x187 + x17 <= 1
c938: x25 + x163 + x281 + x292 + x115 <= 1
c939: x25 + x192 + x186 + x242 + x66 <= 1
c940: x25 + x223 + x31 + x47 + x61 <= 1
c941: x25 + x247 + x161 + x86 <= 1
c942: x25 + x261 + x39 + x178 + x115 <= 1
c943: x25 + x288 + x178 + x39 + x91 <= 1
c944: x26 + x27 + x150 + x284 + x91 <= 1
c945: x26 + x30 + x42 + x47 <= 1
c946: x26 + x31 + x103 + x295 + x150 <= 1
c947: x26 + x35 + x158 + x254 <= 1
c948: x26 + x44 + x276 + x114 + x31 + x275 <= 1
c949: x26 + x71 + x42 + x293 <= 1
c950: x26 + x82 + x295 + x130 + x257 + x95 <= 1
c951: x26 + x104 + x295 + x151 <= 1
c952: x26 + x133 + x103 + x183 <= 1
c953: x26 + x152 + x130 + x151 <= 1
c954: x26 + x154 + x201 + x150 <= 1
c955: x26 + x162 + x276 + x183 + x95 <= 1
c956: x26 + x175 + x295 + x150 + x154 + x278 <= 1
c957: x26 + x180 + x194 + x175 + x211 <= 1
c958: x26 + x189 + x103 + x295 + x150 <= 1
c959: x26 + x212 + x276 + x189 + x242 <= 1
c960: x26 + x216 + x158 + x150 <= 1
c961: x26 + x227 + x103 + x46 + x95 <= 1
c962: x26 + x235 + x130 + x194 <= 1
c963: x26 + x236 + x201 + x249 <= 1
c964: x26 + x263 + x42 + x293 <= 1
c965: x26 + x285 + x276 + x183 + x133 <= 1
c966: x27 + x30 + x145 + x229 + x53 + x46 <= 1
c967: x27 + x35 + x282 + x166 + x8 <= 1
c968: x27 + x45 + x215 + x150 + x278 + x10 <= 1
c969: x27 + x61 + x64 + x186 + x184 <= 1
c970: x27 + x73 + x282 + x248 + x50 + x278 <= 1
c971: x27 + x88 + x134 + x166 + x61 + x8 <= 1
c972: x27 + x96 + x116 + x300 + x23 <= 1
c973: x27 + x109 + x215 + x134 + x261 <= 1
c974: x27 + x124 + x215 + x229 + x108 <= 1
c975: x27 + x125 + x142 + x186 <= 1
c976: x27 + x126 + x141 + x249 + x46 + x241 <= 1
c977: x27 + x127 + x64 + x184 + x61 <= 1
c978: x27 + x129 + x116 + x167 + x300 <= 1
c979: x27 + x163 + x141 + x47 + x134 + x50 <= 1
c980: x27 + x165 + x224 + x300 + x23 <= 1
c981: x27 + x174 + x150 + x282 + x50 + x10 <= 1
c982: x27 + x205 + x100 + x72 + x46 <= 1
c983: x27 + x219 + x224 + x210 + x50 <= 1
c984: x27 + x231 + x116 + x64 + x100 + x241 <= 1
c985: x27 + x234 + x203 + x249 + x284 + x28 <= 1
c986: x27 + x247 + x116 + x64 + x272 + x16 <= 1
c987: x27 + x283 + x142 + x229 + x234 <= 1
c988: x27 + x292 + x98 + x203 <= 1
c989: x28 + x36 + x63 + x187 + x284 <= 1
c990: x28 + x41 + x264 + x187 <= 1
c991: x28 + x44 + x80 + x194 + x284 <= 1
c992: x28 + x46 + x222 + x249 + x65 <= 1
c993: x28 + x58 + x63 + x36 + x132 <= 1
c994: x28 + x60 + x173 + x72 + x203 + x69 <= 1
c995: x28 + x66 + x63 + x85 + x275 + x132 <= 1
c996: x28 + x79 + x63 + x99 + x187 + x275 <= 1
c997: x28 + x86 + x63 + x222 + x187 <= 1
c998: x28 + x91 + x118 + x36 <= 1
c999: x28 + x94 + x270 + x275 <= 1
c1000: x28 + x105 + x41 + x152 + x132 <= 1
c1001: x28 + x146 + x264 + x284 <= 1
c1002: x28 + x150 + x277 + x223 + x284 <= 1
c1003: x28 + x156 + x63 + x58 + x132 <= 1
c1004: x28 + x162 + x193 + x187 + x242 <= 1
c1005: x28 + x170 + x222 + x86 <= 1
c1006: x28 + x189 + x80 + x60 + x72 <= 1
c1007: x28 + x213 + x63 + x222 <= 1
c1008: x28 + x231 + x118 + x242 <= 1
c1009: x28 + x237 + x63 + x36 + x284 <= 1
c1010: x29 + x31 + x266 + x201 + x37 <= 1
c1011: x29 + x33 + x256 + x282 <= 1
c1012: x29 + x47 + x295 + x257 + x206 + x95 <= 1
c1013: x29 + x52 + x266 + x37 + x189 + x202 <= 1
c1014: x29 + x64 + x151 + x232 + x285 <= 1
c1015: x29 + x77 + x269 + x295 <= 1
c1016: x29 + x98 + x257 + x201 + x88 + x129 <= 1
c1017: x29 + x108 + x254 + x140 + x300 + x41 + x152 <= 1
c1018: x29 + x109 + x276 + x282 + x205 <= 1
c1019: x29 + x138 + x266 + x201 + x186 + x134 + x8 <= 1
c1020: x29 + x148 + x245 + x254 + x113 + x152 <= 1
c1021: x29 + x150 + x151 + x232 + x64 <= 1
c1022: x29 + x155 + x266 + x178 + x134 + x8 <= 1
c1023: x29 + x156 + x228 + x140 <= 1
c1024: x29 + x163 + x281 + x41 + x226 <= 1
c1025: x29 + x164 + x269 + x55 + x143 <= 1
c1026: x29 + x174 + x269 + x39 + x55 <= 1
c1027: x29 + x190 + x194 + x116 + x148 <= 1
c1028: x29 + x207 + x256 + x151 + x194 <= 1
c1029: x29 + x215 + x67 + x266 + x164 <= 1
c1030: x29 + x216 + x224 + x295 + x184 + x95 <= 1
c1031: x29 + x250 + x183 + x265 + x202 <= 1
c1032: x29 + x260 + x201 + x112 + x228 <= 1
c1033: x29 + x273 + x112 + x300 + x8 <= 1
c1034: x29 + x277 + x269 + x39 + x229 <= 1
c1035: x29 + x290 + x232 + x64 + x164 <= 1
c1036: x29 + x296 + x77 + x269 <= 1
c1037: x29 + x297 + x77 + x295 + x216 + x95 <= 1
c1038: x30 + x33 + x210 + x246 + x6 <= 1
c1039: x30 + x36 + x62 + x228 + x244 <= 1
c1040: x30 + x66 + x243 + x201 + x183 <= 1
c1041: x30 + x87 + x157 + x112 + x284 <= 1
c1042: x30 + x89 + x191 + x184 <= 1
c1043: x30 + x111 + x182 + x146 + x155 <= 1
c1044: x30 + x123 + x42 + x243 + x15 <= 1
c1045: x30 + x126 + x62 + x53 + x17 <= 1
c1046: x30 + x127 + x42 + x243 + x15 <= 1
c1047: x30 + x152 + x254 + x232 <= 1
c1048: x30 + x161 + x145 + x53 <= 1
c1049: x30 + x164 + x285 + x232 + x278 <= 1
c1050: x30 + x169 + x62 + x155 + x19 <= 1
c1051: x30 + x172 + x157 + x53 + x112 + x278 <= 1
c1052: x30 + x180 + x184 + x210 + x17 <= 1
c1053: x30 + x185 + x182 + x191 + x36 <= 1
c1054: x30 + x294 + x42 + x112 <= 1
c1055: x31 + x35 + x204 + x167 <= 1
c1056: x31 + x56 + x204 + x118 + x224 <= 1
c1057: x31 + x59 + x103 + x173 + x222 + x116 + x238 <= 1
c1058: x31 + x77 + x99 + x167 + x114 + x41 <= 1
c1059: x31 + x91 + x212 + x256 <= 1
c1060: x31 + x110 + x93 + x120 + x65 <= 1
c1061: x31 + x137 + x141 + x194 + x271 <= 1
c1062: x31 + x160 + x204 + x243 + x167 <= 1
c1063: x31 + x162 + x196 + x276 + x211 + x275 <= 1
c1064: x31 + x165 + x204 + x167 + x243 <= 1
c1065: x31 + x171 + x181 + x201 + x58 <= 1
c1066: x31 + x180 + x93 + x73 + x186 <= 1
c1067: x31 + x184 + x103 + x173 + x59 + x282 <= 1
c1068: x31 + x195 + x103 + x173 + x222 <= 1
c1069: x31 + x213 + x160 + x238 <= 1
c1070: x31 + x226 + x93 + x194 + x65 <= 1
c1071: x31 + x237 + x254 + x73 + x168 + x282 <= 1
c1072: x31 + x277 + x103 + x173 + x195 <= 1
c1073: x31 + x285 + x204 + x266 + x116 <= 1
c1074: x31 + x290 + x295 + x141 + x275 <= 1
c1075: x31 + x294 + x196 + x276 + x116 <= 1
c1076: x32 + x37 + x101 + x151 + x17 <= 1
c1077: x32 + x41 + x128 + x178 + x48 <= 1
c1078: x32 + x52 + x84 + x217 + x141 <= 1
c1079: x32 + x53 + x101 + x157 + x248 <= 1
c1080: x32 + x56 + x102 + x90 + x230 <= 1
c1081: x32 + x68 + x245 + x212 + x189 <= 1
c1082: x32 + x73 + x102 + x37 + x10 <= 1
c1083: x32 + x76 + x39 + x230 <= 1
c1084: x32 + x77 + x101 + x80 + x211 <= 1
c1085: x32 + x78 + x80 + x282 + x8 <= 1
c1086: x32 + x81 + x102 + x151 + x37 + x17 <= 1
c1087: x32 + x87 + x101 + x128 + x157 + x248 <= 1
c1088: x32 + x100 + x84 + x102 + x211 <= 1
c1089: x32 + x112 + x212 + x217 + x157 + x211 <= 1
c1090: x32 + x114 + x80 + x186 + x102 + x8 <= 1
c1091: x32 + x120 + x101 + x128 + x90 <= 1
c1092: x32 + x127 + x166 + x37 <= 1
c1093: x32 + x133 + x128 + x215 <= 1
c1094: x32 + x143 + x78 + x184 + x56 <= 1
c1095: x32 + x192 + x134 + x224 + x17 <= 1
c1096: x32 + x200 + x101 + x90 + x128 <= 1
c1097: x32 + x210 + x256 + x78 <= 1
c1098: x32 + x225 + x39 + x178 + x230 <= 1
c1099: x32 + x237 + x73 + x254 + x282 <= 1
c1100: x32 + x250 + x39 + x210 + x225 <= 1
c1101: x32 + x255 + x248 + x8 <= 1
c1102: x32 + x266 + x134 + x178 + x225 + x184 <= 1
c1103: x32 + x273 + x173 + x212 + x261 <= 1
c1104: x32 + x285 + x151 + x90 <= 1
c1105: x32 + x290 + x78 + x90 <= 1
c1106: x32 + x291 + x101 + x157 + x53 <= 1
c1107: x33 + x61 + x117 + x214 + x65 <= 1
c1108: x33 + x69 + x136 + x208 + x282 <= 1
c1109: x33 + x79 + x214 + x69 + x132 <= 1
c1110: x33 + x104 + x208 + x196 <= 1
c1111: x33 + x106 + x121 + x288 <= 1
c1112: x33 + x111 + x117 + x144 <= 1
c1113: x33 + x112 + x136 + x85 + x65 + x132 <= 1
c1114: x33 + x128 + x121 + x85 + x140 <= 1
c1115: x33 + x135 + x196 + x275 + x132 <= 1
c1116: x33 + x156 + x196 + x135 + x132 <= 1
c1117: x33 + x173 + x175 + x140 <= 1
c1118: x33 + x177 + x208 + x132 <= 1
c1119: x33 + x260 + x267 + x214 + x65 <= 1
c1120: x33 + x261 + x121 + x173 + x132 <= 1
c1121: x33 + x271 + x196 <= 1
c1122: x33 + x280 + x246 + x69 <= 1
c1123: x33 + x295 + x136 + x128 <= 1
c1124: x33 + x300 + x175 + x85 + x234 + x140 <= 1
c1125: x34 + x39 + x51 + x177 + x98 <= 1
c1126: x34 + x43 + x220 + x5 <= 1
c1127: x34 + x46 + x220 + x119 <= 1
c1128: x34 + x58 + x57 + x134 + x66 <= 1
c1129: x34 + x59 + x245 + x60 <= 1
c1130: x34 + x80 + x101 + x286 + x211 <= 1
c1131: x34 + x83 + x142 + x87 + x187 + x25 <= 1
c1132: x34 + x85 + x99 + x198 + x289 + x96 <= 1
c1133: x34 + x105 + x113 + x64 + x60 + x148 <= 1
c1134: x34 + x107 + x113 + x167 + x177 <= 1
c1135: x34 + x109 + x258 + x99 + x261 <= 1
c1136: x34 + x111 + x47 + x144 + x37 + x123 <= 1
c1137: x34 + x120 + x101 + x198 + x119 + x275 <= 1
c1138: x34 + x125 + x51 + x289 + x148 <= 1
c1139: x34 + x141 + x208 + x64 + x95 <= 1
c1140: x34 + x180 + x57 + x167 + x14 <= 1
c1141: x34 + x188 + x281 + x300 + x85 <= 1
c1142: x34 + x205 + x198 + x289 <= 1
c1143: x34 + x207 + x51 + x57 <= 1
c1144: x34 + x209 + x264 + x101 + x249 <= 1
c1145: x34 + x215 + x57 + x243 + x167 <= 1
c1146: x34 + x219 + x249 + x289 + x187 <= 1
c1147: x34 + x231 + x64 + x131 + x39 + x230 <= 1
c1148: x34 + x242 + x201 + x99 + x229 + x249 + x234 + x39 + x207 <= 1
c1149: x34 + x244 + x113 + x167 + x128 <= 1
c1150: x34 + x254 + x113 + x175 + x64 + x148 <= 1
c1151: x34 + x262 + x258 + x201 + x289 <= 1
c1152: x34 + x268 + x51 + x80 + x148 <= 1
c1153: x34 + x271 + x51 + x264 + x41 <= 1
c1154: x34 + x272 + x243 + x289 + x66 <= 1
c1155: x34 + x288 + x101 + x198 + x234 <= 1
c1156: x35 + x52 + x158 + x269 + x114 + x140 <= 1
c1157: x35 + x58 + x181 + x154 + x156 <= 1
c1158: x35 + x65 + x147 + x236 + x23 <= 1
c1159: x35 + x68 + x147 + x166 + x143 <= 1
c1160: x35 + x69 + x203 + x212 + x167 + x284 <= 1
c1161: x35 + x75 + x158 + x109 + x202 <= 1
c1162: x35 + x90 + x75 + x254 <= 1
c1163: x35 + x95 + x204 + x157 + x282 <= 1
c1164: x35 + x112 + x257 + x147 + x217 + x113 <= 1
c1165: x35 + x126 + x168 + x242 + x17 <= 1
c1166: x35 + x127 + x204 + x300 <= 1
c1167: x35 + x131 + x158 + x52 + x202 <= 1
c1168: x35 + x164 + x158 + x269 + x52 <= 1
c1169: x35 + x176 + x181 + x157 + x8 <= 1
c1170: x35 + x185 + x292 + x113 + x284 <= 1
c1171: x35 + x193 + x121 + x269 + x242 + x23 <= 1
c1172: x35 + x200 + x158 + x114 <= 1
c1173: x35 + x219 + x121 + x194 + x292 <= 1
c1174: x35 + x226 + x257 + x36 + x140 <= 1
c1175: x35 + x247 + x257 + x108 + x300 <= 1
c1176: x35 + x250 + x158 + x202 <= 1
c1177: x35 + x266 + x257 + x147 + x113 + x112 <= 1
c1178: x35 + x281 + x124 + x217 + x131 <= 1
c1179: x35 + x285 + x257 + x113 + x266 <= 1
c1180: x35 + x289 + x99 + x108 + x194 + x284 <= 1
c1181: x36 + x57 + x151 + x295 + x144 + x275 <= 1
c1182: x36 + x67 + x62 + x257 + x265 <= 1
c1183: x36 + x80 + x182 + x118 + x142 + x132 <= 1
c1184: x36 + x87 + x130 + x82 + x118 + x295 + x144 <= 1
c1185: x36 + x106 + x130 + x228 + x121 <= 1
c1186: x36 + x114 + x220 + x257 + x228 <= 1
c1187: x36 + x120 + x137 + x295 + x50 + x265 <= 1
c1188: x36 + x133 + x276 + x229 <= 1
c1189: x36 + x136 + x63 + x228 <= 1
c1190: x36 + x166 + x257 + x82 + x142 <= 1
c1191: x36 + x171 + x198 + x187 + x275 <= 1
c1192: x36 + x172 + x137 + x64 + x127 + x10 <= 1
c1193: x36 + x184 + x63 + x82 + x295 + x144 <= 1
c1194: x36 + x186 + x191 + x245 + x10 <= 1
c1195: x36 + x190 + x137 + x187 + x284 + x265 <= 1
c1196: x36 + x217 + x130 + x220 + x257 <= 1
c1197: x36 + x234 + x257 + x142 + x210 + x132 <= 1
c1198: x36 + x242 + x276 + x67 + x229 + x275 <= 1
c1199: x36 + x254 + x82 + x115 + x118 <= 1
c1200: x36 + x256 + x82 + x258 + x118 + x87 <= 1
c1201: x36 + x261 + x63 + x136 + x295 <= 1
c1202: x36 + x262 + x136 + x85 + x155 <= 1
c1203: x36 + x269 + x62 + x177 + x248 + x140 <= 1
c1204: x36 + x272 + x257 + x64 + x115 <= 1
c1205: x36 + x273 + x63 + x82 + x295 <= 1
c1206: x36 + x296 + x130 + x64 <= 1
c1207: x37 + x42 + x103 + x105 <= 1
c1208: x37 + x62 + x169 + x92 + x88 + x17 <= 1
c1209: x37 + x69 + x103 + x42 + x249 + x127 <= 1
c1210: x37 + x84 + x103 + x105 <= 1
c1211: x37 + x85 + x179 + x154 + x175 <= 1
c1212: x37 + x86 + x101 + x74 + x62 + x151 <= 1
c1213: x37 + x97 + x103 + x227 <= 1
c1214: x37 + x126 + x178 + x88 + x62 + x3 <= 1
c1215: x37 + x133 + x103 + x183 <= 1
c1216: x37 + x136 + x183 + x51 + x228 <= 1
c1217: x37 + x137 + x74 + x169 + x266 <= 1
c1218: x37 + x146 + x51 + x182 <= 1
c1219: x37 + x147 + x73 + x169 + x275 + x10 <= 1
c1220: x37 + x153 + x103 + x227 <= 1
c1221: x37 + x157 + x181 + x101 + x296 <= 1
c1222: x37 + x162 + x84 + x151 <= 1
c1223: x37 + x174 + x42 + x121 <= 1
c1224: x37 + x180 + x73 + x175 + x86 <= 1
c1225: x37 + x193 + x183 + x74 + x189 <= 1
c1226: x37 + x200 + x73 + x62 + x69 <= 1
c1227: x37 + x203 + x42 + x47 + x121 <= 1
c1228: x37 + x219 + x103 + x84 + x249 <= 1
c1229: x37 + x225 + x47 + x248 <= 1
c1230: x37 + x269 + x183 + x182 + x127 <= 1
c1231: x37 + x280 + x147 + x101 <= 1
c1232: x37 + x286 + x183 + x182 + x201 <= 1
c1233: x37 + x298 + x181 + x151 <= 1
c1234: x38 + x45 + x160 + x204 + x258 + x278 <= 1
c1235: x38 + x46 + x53 + x228 <= 1
c1236: x38 + x47 + x55 + x204 + x45 <= 1
c1237: x38 + x52 + x173 + x167 + x47 <= 1
c1238: x38 + x62 + x55 + x204 + x45 <= 1
c1239: x38 + x77 + x55 + x167 <= 1
c1240: x38 + x81 + x173 + x238 + x228 + x242 <= 1
c1241: x38 + x102 + x55 + x238 <= 1
c1242: x38 + x105 + x243 + x238 <= 1
c1243: x38 + x106 + x160 + x243 + x167 + x238 <= 1
c1244: x38 + x162 + x55 + x77 <= 1
c1245: x38 + x171 + x53 + x173 + x14 <= 1
c1246: x38 + x224 + x204 + x243 + x173 <= 1
c1247: x38 + x235 + x204 + x224 + x278 <= 1
c1248: x38 + x245 + x45 + x204 + x258 <= 1
c1249: x38 + x291 + x53 + x62 <= 1
c1250: x39 + x50 + x253 + x104 + x229 <= 1
c1251: x39 + x65 + x233 + x93 + x214 + x269 <= 1
c1252: x39 + x107 + x203 + x201 + x34 <= 1
c1253: x39 + x127 + x267 + x194 + x245 <= 1
c1254: x39 + x130 + x178 + x98 + x203 <= 1
c1255: x39 + x132 + x253 + x218 + x249 <= 1
c1256: x39 + x135 + x233 + x293 <= 1
c1257: x39 + x137 + x251 + x253 <= 1
c1258: x39 + x138 + x161 + x99 + x234 <= 1
c1259: x39 + x149 + x264 + x214 <= 1
c1260: x39 + x153 + x233 + x93 + x210 <= 1
c1261: x39 + x179 + x218 + x91 <= 1
c1262: x39 + x180 + x253 + x233 + x174 <= 1
c1263: x39 + x189 + x276 + x41 + x229 + x114 <= 1
c1264: x39 + x192 + x267 + x250 <= 1
c1265: x39 + x213 + x222 + x51 <= 1
c1266: x39 + x224 + x264 + x51 <= 1
c1267: x39 + x246 + x161 + x222 <= 1
c1268: x39 + x268 + x51 + x225 <= 1
c1269: x39 + x283 + x118 + x229 <= 1
c1270: x39 + x284 + x253 + x264 + x249 <= 1
c1271: x40 + x51 + x195 + x191 + x63 + x228 <= 1
c1272: x40 + x52 + x158 + x248 <= 1
c1273: x40 + x53 + x158 + x233 + x216 <= 1
c1274: x40 + x57 + x227 + x189 <= 1
c1275: x40 + x68 + x212 + x195 + x233 <= 1
c1276: x40 + x72 + x82 + x257 + x212 <= 1
c1277: x40 + x77 + x158 + x216 <= 1
c1278: x40 + x85 + x117 + x96 + x99 <= 1
c1279: x40 + x134 + x251 + x169 + x17 <= 1
c1280: x40 + x171 + x90 + x233 <= 1
c1281: x40 + x175 + x251 + x90 <= 1
c1282: x40 + x201 + x82 + x72 + x257 <= 1
c1283: x40 + x203 + x72 + x82 + x212 <= 1
c1284: x40 + x261 + x191 + x212 <= 1
c1285: x40 + x278 + x195 + x212 <= 1
c1286: x41 + x42 + x103 + x232 + x105 <= 1
c1287: x41 + x62 + x92 + x55 + x88 <= 1
c1288: x41 + x70 + x199 + x53 + x132 <= 1
c1289: x41 + x81 + x92 + x216 + x241 + x151 <= 1
c1290: x41 + x84 + x103 + x199 + x53 <= 1
c1291: x41 + x91 + x232 + x47 + x179 <= 1
c1292: x41 + x96 + x220 + x74 + x216 <= 1
c1293: x41 + x111 + x163 + x232 + x74 + x229 + x47 <= 1
c1294: x41 + x134 + x163 + x229 + x47 + x50 <= 1
c1295: x41 + x153 + x103 + x233 + x140 <= 1
c1296: x41 + x164 + x70 + x199 + x12 <= 1
c1297: x41 + x166 + x70 + x61 + x201 <= 1
c1298: x41 + x168 + x276 + x73 + x31 <= 1
c1299: x41 + x172 + x92 + x55 + x216 + x1 <= 1
c1300: x41 + x177 + x73 + x229 + x234 + x50 <= 1
c1301: x41 + x182 + x103 + x187 + x167 <= 1
c1302: x41 + x185 + x276 + x233 + x2 <= 1
c1303: x41 + x204 + x220 + x42 <= 1
c1304: x41 + x206 + x300 + x74 <= 1
c1305: x41 + x213 + x163 + x238 + x47 <= 1
c1306: x41 + x215 + x108 + x299 + x189 + x278 + x12 <= 1
c1307: x41 + x217 + x264 + x281 <= 1
c1308: x41 + x219 + x103 + x238 + x84 <= 1
c1309: x41 + x228 + x70 + x53 <= 1
c1310: x41 + x240 + x103 + x167 + x69 <= 1
c1311: x41 + x255 + x70 + x289 <= 1
c1312: x41 + x291 + x103 + x163 + x232 + x69 <= 1
c1313: x42 + x49 + x253 + x154 <= 1
c1314: x42 + x50 + x93 + x158 <= 1
c1315: x42 + x63 + x253 + x195 + x143 + x2 <= 1
c1316: x42 + x72 + x293 + x60 + x238 + x143 + x241 <= 1
c1317: x42 + x82 + x253 + x134 + x174 <= 1
c1318: x42 + x85 + x198 + x154 + x241 + x15 <= 1
c1319: x42 + x108 + x59 + x71 + x15 <= 1
c1320: x42 + x122 + x158 + x77 + x2 <= 1
c1321: x42 + x125 + x93 + x154 <= 1
c1322: x42 + x135 + x60 + x293 <= 1
c1323: x42 + x140 + x279 + x243 + x204 <= 1
c1324: x42 + x151 + x165 + x203 + x85 <= 1
c1325: x42 + x156 + x243 + x82 + x174 + x134 <= 1
c1326: x42 + x159 + x198 + x264 <= 1
c1327: x42 + x173 + x59 + x103 + x238 + x69 <= 1
c1328: x42 + x177 + x93 + x108 + x140 <= 1
c1329: x42 + x188 + x122 + x194 + x238 + x203 <= 1
c1330: x42 + x226 + x198 + x173 + x203 <= 1
c1331: x42 + x234 + x198 + x121 + x241 + x85 <= 1
c1332: x42 + x273 + x103 + x295 + x63 <= 1
c1333: x42 + x280 + x232 + x125 + x69 <= 1
c1334: x42 + x300 + x71 + x264 + x294 <= 1
c1335: x43 + x58 + x100 + x72 + x154 + x93 <= 1
c1336: x43 + x62 + x122 + x141 <= 1
c1337: x43 + x67 + x100 + x216 <= 1
c1338: x43 + x73 + x236 + x244 <= 1
c1339: x43 + x75 + x150 + x154 + x278 <= 1
c1340: x43 + x87 + x236 + x154 + x202 <= 1
c1341: x43 + x97 + x75 + x264 <= 1
c1342: x43 + x99 + x161 + x72 <= 1
c1343: x43 + x116 + x122 <= 1
c1344: x43 + x134 + x221 + x141 + x2 <= 1
c1345: x43 + x139 + x100 + x67 <= 1
c1346: x43 + x151 + x150 + x67 + x216 <= 1
c1347: x43 + x164 + x236 + x154 + x87 <= 1
c1348: x43 + x184 + x67 + x216 <= 1
c1349: x43 + x200 + x286 + x62 <= 1
c1350: x43 + x240 + x150 + x67 <= 1
c1351: x43 + x273 + x154 + x141 <= 1
c1352: x43 + x281 + x116 + x282 + x300 + x34 <= 1
c1353: x43 + x296 + x150 + x99 <= 1
c1354: x43 + x298 + x67 + x151 <= 1
c1355: x44 + x51 + x279 + x243 <= 1
c1356: x44 + x55 + x276 + x101 <= 1
c1357: x44 + x58 + x181 + x154 <= 1
c1358: x44 + x61 + x279 + x147 + x84 <= 1
c1359: x44 + x68 + x279 + x147 + x217 <= 1
c1360: x44 + x71 + x253 + x147 + x233 <= 1
c1361: x44 + x74 + x267 + x61 + x68 <= 1
c1362: x44 + x81 + x196 + x80 + x114 + x275 <= 1
c1363: x44 + x116 + x197 + x267 + x194 <= 1
c1364: x44 + x121 + x94 + x253 + x275 <= 1
c1365: x44 + x130 + x243 + x121 <= 1
c1366: x44 + x138 + x94 + x196 + x187 + x1 + x14 <= 1
c1367: x44 + x170 + x90 + x289 + x284 <= 1
c1368: x44 + x180 + x94 + x253 + x114 <= 1
c1369: x44 + x218 + x220 + x253 + x217 <= 1
c1370: x44 + x226 + x230 + x281 + x249 <= 1
c1371: x44 + x268 + x220 <= 1
c1372: x45 + x48 + x178 + x128 <= 1
c1373: x45 + x51 + x183 + x195 + x103 <= 1
c1374: x45 + x52 + x208 + x269 + x164 <= 1
c1375: x45 + x58 + x64 + x150 + x232 <= 1
c1376: x45 + x65 + x110 + x215 + x10 <= 1
c1377: x45 + x72 + x160 + x64 + x144 <= 1
c1378: x45 + x90 + x118 + x91 <= 1
c1379: x45 + x93 + x160 + x128 + x80 <= 1
c1380: x45 + x114 + x252 + x148 <= 1
c1381: x45 + x139 + x47 + x90 <= 1
c1382: x45 + x163 + x150 + x232 + x103 <= 1
c1383: x45 + x169 + x178 + x258 + x204 <= 1
c1384: x45 + x188 + x160 + x93 <= 1
c1385: x45 + x216 + x208 + x64 + x151 <= 1
c1386: x45 + x239 + x178 + x169 <= 1
c1387: x45 + x244 + x128 + x178 <= 1
c1388: x45 + x271 + x183 + x258 + x127 + x10 <= 1
c1389: x45 + x284 + x208 + x245 + x6 <= 1
c1390: x45 + x290 + x183 + x195 <= 1
c1391: x45 + x291 + x118 + x232 <= 1
c1392: x45 + x295 + x128 + x80 + x11 <= 1
c1393: x45 + x297 + x178 + x91 + x284 <= 1
c1394: x46 + x56 + x279 + x277 + x198 <= 1
c1395: x46 + x69 + x270 + x122 + x284 <= 1
c1396: x46 + x73 + x145 + x186 + x115 + x50 <= 1
c1397: x46 + x77 + x129 + x141 + x249 + x132 <= 1
c1398: x46 + x117 + x145 + x183 + x229 + x50 <= 1
c1399: x46 + x118 + x279 + x260 + x229 + x65 <= 1
c1400: x46 + x120 + x183 + x195 + x112 <= 1
c1401: x46 + x128 + x270 + x210 + x211 + x140 <= 1
c1402: x46 + x131 + x78 + x227 + x282 + x8 <= 1
c1403: x46 + x135 + x222 + x183 + x195 <= 1
c1404: x46 + x137 + x251 + x260 + x241 <= 1
c1405: x46 + x139 + x279 + x257 + x132 <= 1
c1406: x46 + x163 + x94 + x279 + x103 <= 1
c1407: x46 + x172 + x251 + x222 + x183 + x112 + x195 <= 1
c1408: x46 + x226 + x222 + x257 + x249 + x112 <= 1
c1409: x46 + x231 + x251 + x257 + x279 <= 1
c1410: x46 + x234 + x78 + x210 + x227 + x93 + x8 <= 1
c1411: x46 + x250 + x88 + x267 + x225 <= 1
c1412: x46 + x259 + x82 + x241 <= 1
c1413: x46 + x265 + x122 + x78 + x183 + x10 <= 1
c1414: x46 + x268 + x122 + x78 + x10 <= 1
c1415: x46 + x269 + x129 + x285 + x116 + x3 <= 1
c1416: x46 + x273 + x117 <= 1
c1417: x46 + x287 + x270 + x284 <= 1
c1418: x46 + x296 + x221 + x53 <= 1
c1419: x47 + x68 + x223 + x267 + x61 <= 1
c1420: x47 + x86 + x117 + x252 + x50 <= 1
c1421: x47 + x107 + x60 + x238 + x66 + x203 <= 1
c1422: x47 + x124 + x248 + x157 + x128 + x9 <= 1
c1423: x47 + x133 + x230 + x111 + x229 + x90 <= 1
c1424: x47 + x145 + x223 + x210 <= 1
c1425: x47 + x162 + x176 + x279 <= 1
c1426: x47 + x170 + x260 + x248 <= 1
c1427: x47 + x175 + x117 + x254 + x230 <= 1
c1428: x47 + x177 + x236 + x248 + x50 <= 1
c1429: x47 + x200 + x158 + x210 + x128 <= 1
c1430: x47 + x207 + x236 + x288 <= 1
c1431: x47 + x209 + x158 + x117 + x229 + x50 <= 1
c1432: x47 + x235 + x196 + x257 + x141 <= 1
c1433: x47 + x259 + x236 + x248 + x238 <= 1
c1434: x47 + x271 + x158 + x196 <= 1
c1435: x47 + x286 + x142 + x252 + x148 <= 1
c1436: x47 + x296 + x176 + x288 <= 1
c1437: x48 + x51 + x100 + x154 <= 1
c1438: x48 + x70 + x236 + x78 <= 1
c1439: x48 + x77 + x253 + x100 + x154 <= 1
c1440: x48 + x105 + x243 + x238 + x65 <= 1
c1441: x48 + x116 + x223 + x100 + x260 <= 1
c1442: x48 + x145 + x223 + x210 + x114 <= 1
c1443: x48 + x157 + x236 + x238 <= 1
c1444: x48 + x169 + x70 + x155 <= 1
c1445: x48 + x170 + x145 + x114 <= 1
c1446: x48 + x180 + x223 + x210 + x114 <= 1
c1447: x48 + x182 + x155 + x105 + x65 <= 1
c1448: x48 + x185 + x292 + x155 <= 1
c1449: x48 + x213 + x145 <= 1
c1450: x48 + x232 + x253 + x70 + x210 <= 1
c1451: x48 + x240 + x178 + x150 + x116 <= 1
c1452: x48 + x241 + x292 + x157 + x128 <= 1
c1453: x48 + x263 + x243 + x282 <= 1
c1454: x48 + x275 + x236 + x114 + x23 <= 1
c1455: x48 + x297 + x178 + x82 <= 1
c1456: x49 + x64 + x256 + x227 <= 1
c1457: x49 + x68 + x147 + x143 + x233 <= 1
c1458: x49 + x83 + x186 + x147 <= 1
c1459: x49 + x101 + x150 + x116 + x148 <= 1
c1460: x49 + x118 + x191 + x186 + x233 <= 1
c1461: x49 + x127 + x243 + x118 + x1 <= 1
c1462: x49 + x157 + x206 + x282 + x241 <= 1
c1463: x49 + x164 + x285 + x64 + x232 <= 1
c1464: x49 + x182 + x191 + x118 <= 1
c1465: x49 + x267 + x116 + x148 <= 1
c1466: x50 + x63 + x199 + x113 + x85 + x132 <= 1
c1467: x50 + x66 + x161 + x183 + x300 <= 1
c1468: x50 + x89 + x113 + x216 + x63 <= 1
c1469: x50 + x90 + x98 + x103 + x249 <= 1
c1470: x50 + x97 + x79 + x176 + x113 <= 1
c1471: x50 + x123 + x199 + x187 + x183 <= 1
c1472: x50 + x142 + x236 + x79 + x187 + x265 <= 1
c1473: x50 + x146 + x236 + x111 <= 1
c1474: x50 + x149 + x158 + x155 + x248 <= 1
c1475: x50 + x164 + x199 + x236 + x137 + x265 + x12 <= 1
c1476: x50 + x196 + x104 + x208 + x148 <= 1
c1477: x50 + x220 + x161 + x138 + x145 <= 1
c1478: x50 + x231 + x100 + x252 + x12 <= 1
c1479: x50 + x232 + x104 + x224 <= 1
c1480: x50 + x269 + x246 + x161 + x39 <= 1
c1481: x50 + x272 + x266 + x104 + x295 <= 1
c1482: x50 + x277 + x94 + x196 + x187 <= 1
c1483: x50 + x297 + x115 + x224 <= 1
c1484: x51 + x53 + x293 + x257 + x71 <= 1
c1485: x51 + x67 + x136 + x100 + x266 <= 1
c1486: x51 + x104 + x57 + x187 + x183 <= 1
c1487: x51 + x110 + x168 + x173 + x140 <= 1
c1488: x51 + x119 + x161 + x248 + x279 <= 1
c1489: x51 + x159 + x92 + x80 + x19 <= 1
c1490: x51 + x166 + x191 + x182 + x53 <= 1
c1491: x51 + x171 + x270 + x57 + x299 <= 1
c1492: x51 + x218 + x270 + x243 + x257 + x132 <= 1
c1493: x51 + x221 + x222 + x195 + x173 + x183 <= 1
c1494: x51 + x237 + x270 + x299 <= 1
c1495: x51 + x273 + x92 + x173 <= 1
c1496: x51 + x281 + x168 + x41 <= 1
c1497: x51 + x285 + x92 + x93 <= 1
c1498: x51 + x287 + x270 <= 1
c1499: x52 + x70 + x60 + x158 + x116 <= 1
c1500: x52 + x93 + x214 + x131 <= 1
c1501: x52 + x96 + x214 + x131 + x189 <= 1
c1502: x52 + x99 + x270 + x198 <= 1
c1503: x52 + x105 + x122 + x158 <= 1
c1504: x52 + x128 + x270 + x121 + x140 <= 1
c1505: x52 + x159 + x60 + x229 + x65 <= 1
c1506: x52 + x162 + x84 + x141 <= 1
c1507: x52 + x185 + x223 + x82 + x114 <= 1
c1508: x52 + x191 + x208 + x282 + x141 <= 1
c1509: x52 + x206 + x214 + x282 + x226 <= 1
c1510: x52 + x207 + x84 + x217 + x203 <= 1
c1511: x52 + x210 + x122 + x270 + x158 + x116 <= 1
c1512: x52 + x218 + x60 + x217 + x203 + x2 <= 1
c1513: x52 + x259 + x167 + x99 + x114 + x241 <= 1
c1514: x52 + x262 + x258 + x34 <= 1
c1515: x53 + x58 + x60 + x190 + x171 <= 1
c1516: x53 + x65 + x129 + x154 + x72 + x134 + x132 <= 1
c1517: x53 + x89 + x115 + x14 <= 1
c1518: x53 + x91 + x115 + x203 + x278 + x1 <= 1
c1519: x53 + x113 + x292 + x186 + x147 + x152 <= 1
c1520: x53 + x136 + x199 + x100 + x224 + x85 <= 1
c1521: x53 + x137 + x119 + x172 + x65 + x46 <= 1
c1522: x53 + x150 + x215 + x203 + x278 + x2 <= 1
c1523: x53 + x159 + x100 + x145 + x229 + x275 <= 1
c1524: x53 + x162 + x193 + x166 + x242 <= 1
c1525: x53 + x200 + x293 + x263 <= 1
c1526: x53 + x218 + x129 + x60 + x72 + x172 + x203 + x65 <= 1
c1527: x53 + x223 + x193 + x115 + x242 <= 1
c1528: x53 + x245 + x193 + x186 + x134 <= 1
c1529: x53 + x273 + x154 + x72 <= 1
c1530: x53 + x297 + x113 + x216 + x154 <= 1
c1531: x54 + x79 + x109 + x74 <= 1
c1532: x54 + x82 + x98 + x74 <= 1
c1533: x54 + x93 + x230 + x80 + x284 <= 1
c1534: x54 + x102 + x267 + x110 <= 1
c1535: x54 + x105 + x216 + x158 <= 1
c1536: x54 + x131 + x102 + x272 + x216 + x158 <= 1
c1537: x54 + x151 + x102 + x216 + x131 <= 1
c1538: x54 + x157 + x292 + x98 <= 1
c1539: x54 + x171 + x292 + x229 + x183 <= 1
c1540: x54 + x192 + x98 + x74 + x229 <= 1
c1541: x54 + x225 + x80 + x230 + x102 <= 1
c1542: x54 + x245 + x110 + x267 <= 1
c1543: x54 + x246 + x230 + x210 + x6 <= 1
c1544: x54 + x252 + x230 + x131 <= 1
c1545: x54 + x260 + x266 + x211 + x11 <= 1
c1546: x54 + x282 + x246 + x69 <= 1
c1547: x55 + x56 + x143 + x78 + x62 <= 1
c1548: x55 + x60 + x178 + x155 + x62 <= 1
c1549: x55 + x68 + x167 + x202 + x95 <= 1
c1550: x55 + x73 + x276 + x238 + x202 + x229 <= 1
c1551: x55 + x75 + x276 + x78 + x229 + x202 <= 1
c1552: x55 + x110 + x178 + x80 + x202 <= 1
c1553: x55 + x112 + x92 + x88 + x62 <= 1
c1554: x55 + x137 + x276 + x238 <= 1
c1555: x55 + x149 + x88 + x178 + x155 <= 1
c1556: x55 + x151 + x92 + x101 + x62 + x17 <= 1
c1557: x55 + x152 + x246 + x230 + x210 + x6 <= 1
c1558: x55 + x158 + x250 + x210 + x5 <= 1
c1559: x55 + x193 + x250 + x210 <= 1
c1560: x55 + x206 + x246 + x210 + x6 + x8 <= 1
c1561: x55 + x215 + x143 + x63 <= 1
c1562: x55 + x223 + x75 + x158 <= 1
c1563: x55 + x225 + x174 + x230 + x82 <= 1
c1564: x55 + x228 + x178 + x88 + x62 + x17 <= 1
c1565: x55 + x232 + x276 + x233 + x115 <= 1
c1566: x55 + x244 + x143 + x99 + x73 + x62 <= 1
c1567: x55 + x262 + x92 + x112 <= 1
c1568: x55 + x271 + x174 + x127 <= 1
c1569: x55 + x287 + x143 + x113 + x23 <= 1
c1570: x56 + x60 + x67 + x102 <= 1
c1571: x56 + x64 + x122 + x78 + x62 <= 1
c1572: x56 + x65 + x198 + x62 + x118 + x279 <= 1
c1573: x56 + x72 + x212 + x102 <= 1
c1574: x56 + x86 + x198 + x277 + x279 + x62 <= 1
c1575: x56 + x113 + x122 + x64 <= 1
c1576: x56 + x134 + x264 + x224 + x184 <= 1
c1577: x56 + x141 + x142 + x198 + x118 + x279 + x62 <= 1
c1578: x56 + x150 + x67 + x102 <= 1
c1579: x56 + x152 + x122 + x113 <= 1
c1580: x56 + x195 + x212 + x62 <= 1
c1581: x56 + x223 + x212 + x31 <= 1
c1582: x56 + x244 + x67 + x224 <= 1
c1583: x57 + x61 + x129 + x194 + x278 + x17 <= 1
c1584: x57 + x84 + x243 + x270 <= 1
c1585: x57 + x89 + x144 + x194 + x15 <= 1
c1586: x57 + x95 + x222 + x167 + x238 + x17 <= 1
c1587: x57 + x97 + x222 + x187 + x112 <= 1
c1588: x57 + x110 + x236 + x129 + x17 <= 1
c1589: x57 + x115 + x179 <= 1
c1590: x57 + x150 + x246 + x186 + x295 + x278 <= 1
c1591: x57 + x166 + x66 + x155 + x134 + x14 <= 1
c1592: x57 + x173 + x222 + x167 + x238 <= 1
c1593: x57 + x208 + x243 + x270 + x69 + x132 <= 1
c1594: x57 + x214 + x222 + x155 + x183 <= 1
c1595: x57 + x224 + x243 + x277 + x238 + x173 + x69 <= 1
c1596: x57 + x226 + x222 + x187 + x112 <= 1
c1597: x57 + x248 + x236 + x101 + x238 + x17 <= 1
c1598: x57 + x266 + x163 + x236 <= 1
c1599: x57 + x274 + x243 + x295 <= 1
c1600: x57 + x298 + x270 + x248 + x14 <= 1
c1601: x58 + x59 + x111 + x227 + x154 <= 1
c1602: x58 + x80 + x124 + x108 + x93 <= 1
c1603: x58 + x82 + x212 + x111 <= 1
c1604: x58 + x88 + x181 + x142 <= 1
c1605: x58 + x121 + x100 + x140 <= 1
c1606: x58 + x125 + x181 + x142 + x156 <= 1
c1607: x58 + x139 + x100 + x64 + x34 <= 1
c1608: x58 + x153 + x227 + x264 + x66 <= 1
c1609: x58 + x184 + x59 + x224 + x2 + x31 <= 1
c1610: x58 + x206 + x72 + x184 <= 1
c1611: x58 + x225 + x250 + x88 <= 1
c1612: x58 + x226 + x140 + x80 + x93 <= 1
c1613: x58 + x262 + x201 + x154 <= 1
c1614: x58 + x271 + x283 + x17 <= 1
c1615: x59 + x61 + x288 + x293 + x238 + x14 <= 1
c1616: x59 + x62 + x130 + x178 + x228 + x257 <= 1
c1617: x59 + x110 + x235 + x228 + x141 <= 1
c1618: x59 + x138 + x130 + x266 + x116 <= 1
c1619: x59 + x142 + x288 + x178 + x108 <= 1
c1620: x59 + x151 + x130 + x285 <= 1
c1621: x59 + x152 + x130 + x116 <= 1
c1622: x59 + x158 + x130 + x116 + x202 + x228 <= 1
c1623: x59 + x170 + x222 + x102 <= 1
c1624: x59 + x185 + x130 + x235 + x127 <= 1
c1625: x59 + x192 + x143 + x293 + x60 <= 1
c1626: x59 + x207 + x272 + x143 + x293 + x15 <= 1
c1627: x59 + x214 + x130 <= 1
c1628: x59 + x231 + x71 + x143 + x257 <= 1
c1629: x59 + x261 + x111 + x285 + x192 <= 1
c1630: x59 + x263 + x288 + x293 + x14 <= 1
c1631: x59 + x270 + x71 + x257 <= 1
c1632: x59 + x274 + x276 + x285 <= 1
c1633: x59 + x294 + x222 + x116 + x31 <= 1
c1634: x59 + x299 + x108 + x142 + x173 + x257 <= 1
c1635: x60 + x61 + x176 + x87 <= 1
c1636: x60 + x73 + x168 + x86 + x143 + x180 <= 1
c1637: x60 + x101 + x251 + x67 + x74 + x257 <= 1
c1638: x60 + x123 + x94 + x168 + x87 <= 1
c1639: x60 + x126 + x168 + x216 + x87 <= 1
c1640: x60 + x136 + x94 + x96 + x66 + x155 <= 1
c1641: x60 + x141 + x94 + x145 + x217 <= 1
c1642: x60 + x157 + x160 + x74 + x87 <= 1
c1643: x60 + x169 + x160 + x121 + x201 + x66 + x140 <= 1
c1644: x60 + x179 + x168 + x105 + x113 <= 1
c1645: x60 + x193 + x247 + x269 <= 1
c1646: x60 + x202 + x243 + x160 + x265 + x238 <= 1
c1647: x60 + x225 + x251 + x102 + x295 <= 1
c1648: x60 + x239 + x129 + x178 + x285 <= 1
c1649: x60 + x260 + x168 + x203 + x72 + x201 <= 1
c1650: x60 + x264 + x64 + x172 <= 1
c1651: x61 + x86 + x117 + x63 + x180 <= 1
c1652: x61 + x103 + x122 + x194 + x238 <= 1
c1653: x61 + x104 + x258 + x77 + x127 <= 1
c1654: x61 + x111 + x212 + x147 + x8 + x10 <= 1
c1655: x61 + x124 + x117 + x129 + x65 <= 1
c1656: x61 + x131 + x176 + x282 + x8 <= 1
c1657: x61 + x138 + x198 + x70 <= 1
c1658: x61 + x172 + x124 + x128 + x248 + x17 <= 1
c1659: x61 + x205 + x212 + x198 <= 1
c1660: x61 + x225 + x254 + x117 + x47 <= 1
c1661: x61 + x243 + x84 + x124 <= 1
c1662: x61 + x247 + x186 + x64 + x248 + x27 <= 1
c1663: x61 + x273 + x212 + x198 <= 1
c1664: x61 + x287 + x100 + x64 + x12 <= 1
c1665: x61 + x291 + x254 + x154 <= 1
c1666: x61 + x298 + x212 + x186 + x248 + x278 <= 1
c1667: x61 + x299 + x267 + x214 + x65 <= 1
c1668: x62 + x68 + x196 + x195 + x277 <= 1
c1669: x62 + x85 + x212 + x198 + x155 + x203 <= 1
c1670: x62 + x107 + x92 + x279 <= 1
c1671: x62 + x121 + x253 + x195 + x71 <= 1
c1672: x62 + x125 + x253 + x73 <= 1
c1673: x62 + x190 + x146 + x36 <= 1
c1674: x62 + x209 + x130 + x140 + x257 <= 1
c1675: x62 + x211 + x92 + x196 + x101 <= 1
c1676: x62 + x219 + x187 + x233 + x195 + x210 <= 1
c1677: x62 + x241 + x92 + x88 + x196 <= 1
c1678: x62 + x255 + x146 + x86 <= 1
c1679: x62 + x260 + x178 + x169 + x16 <= 1
c1680: x62 + x268 + x78 + x108 + x142 <= 1
c1681: x62 + x280 + x125 + x178 + x142 + x69 <= 1
c1682: x63 + x75 + x144 + x258 + x275 + x228 <= 1
c1683: x63 + x111 + x253 + x144 + x82 <= 1
c1684: x63 + x120 + x181 + x295 + x278 <= 1
c1685: x63 + x125 + x181 + x199 + x214 <= 1
c1686: x63 + x153 + x99 <= 1
c1687: x63 + x154 + x181 + x187 + x169 + x295 <= 1
c1688: x63 + x158 + x79 + x50 <= 1
c1689: x63 + x179 + x191 + x261 + x132 <= 1
c1690: x63 + x185 + x222 + x191 <= 1
c1691: x63 + x190 + x136 + x216 <= 1
c1692: x63 + x196 + x181 + x187 <= 1
c1693: x63 + x201 + x181 + x66 + x169 <= 1
c1694: x63 + x219 + x187 + x195 + x284 <= 1
c1695: x63 + x240 + x181 + x295 <= 1
c1696: x63 + x246 + x281 + x265 <= 1
c1697: x63 + x269 + x213 + x66 <= 1
c1698: x63 + x296 + x181 + x261 <= 1
c1699: x64 + x74 + x106 + x163 + x253 + x238 <= 1
c1700: x64 + x84 + x100 + x230 + x102 + x238 <= 1
c1701: x64 + x88 + x97 + x136 + x112 <= 1
c1702: x64 + x129 + x197 + x203 <= 1
c1703: x64 + x133 + x161 + x187 <= 1
c1704: x64 + x179 + x175 + x218 + x85 + x230 + x133 <= 1
c1705: x64 + x181 + x106 + x169 + x148 + x10 <= 1
c1706: x64 + x195 + x100 + x235 + x78 + x228 <= 1
c1707: x64 + x199 + x227 + x187 + x100 <= 1
c1708: x64 + x200 + x254 + x129 + x230 <= 1
c1709: x64 + x210 + x256 + x161 + x78 <= 1
c1710: x64 + x220 + x204 + x145 + x285 <= 1
c1711: x64 + x222 + x256 + x272 + x108 <= 1
c1712: x64 + x259 + x97 + x238 + x241 <= 1
c1713: x64 + x260 + x220 + x227 + x112 <= 1
c1714: x64 + x271 + x144 + x130 + x129 <= 1
c1715: x64 + x279 + x197 + x227 <= 1
c1716: x65 + x79 + x182 + x118 + x238 <= 1
c1717: x65 + x89 + x106 + x181 + x10 <= 1
c1718: x65 + x92 + x292 + x194 + x262 <= 1
c1719: x65 + x104 + x120 + x114 <= 1
c1720: x65 + x135 + x236 + x233 + x118 <= 1
c1721: x65 + x174 + x124 + x243 + x132 <= 1
c1722: x65 + x190 + x233 + x249 <= 1
c1723: x65 + x199 + x92 + x243 + x88 + x8 + x23 <= 1
c1724: x65 + x227 + x198 + x85 + x154 <= 1
c1725: x65 + x235 + x281 + x194 + x282 <= 1
c1726: x65 + x246 + x117 + x33 <= 1
c1727: x65 + x261 + x215 + x267 + x110 <= 1
c1728: x65 + x272 + x119 + x210 <= 1
c1729: x65 + x286 + x182 + x72 + x238 + x16 <= 1
c1730: x66 + x84 + x94 + x215 + x203 + x278 <= 1
c1731: x66 + x92 + x96 + x117 + x136 <= 1
c1732: x66 + x108 + x289 + x186 + x86 + x185 <= 1
c1733: x66 + x122 + x213 + x294 + x269 <= 1
c1734: x66 + x128 + x96 + x300 + x178 <= 1
c1735: x66 + x130 + x98 + x177 <= 1
c1736: x66 + x139 + x289 + x67 + x132 <= 1
c1737: x66 + x147 + x71 + x117 <= 1
c1738: x66 + x163 + x67 + x213 + x230 + x47 <= 1
c1739: x66 + x172 + x96 + x92 + x128 + x173 <= 1
c1740: x66 + x188 + x300 + x233 + x108 <= 1
c1741: x66 + x191 + x146 + x121 + x132 <= 1
c1742: x66 + x194 + x289 + x67 + x283 <= 1
c1743: x66 + x199 + x289 + x67 + x265 + x132 <= 1
c1744: x66 + x225 + x174 + x253 + x134 + x132 + x2 <= 1
c1745: x66 + x232 + x98 + x249 + x203 + x74 <= 1
c1746: x66 + x260 + x178 + x191 <= 1
c1747: x66 + x267 + x92 + x169 + x108 <= 1
c1748: x66 + x297 + x198 + x178 <= 1
c1749: x67 + x82 + x83 + x224 + x216 <= 1
c1750: x67 + x97 + x197 + x191 + x241 <= 1
c1751: x67 + x129 + x197 + x265 + x194 <= 1
c1752: x67 + x140 + x160 + x144 + x191 <= 1
c1753: x67 + x145 + x252 + x100 <= 1
c1754: x67 + x172 + x251 + x266 + x74 <= 1
c1755: x67 + x181 + x150 + x240 + x214 <= 1
c1756: x67 + x188 + x250 + x160 <= 1
c1757: x67 + x202 + x81 + x208 + x151 <= 1
c1758: x67 + x237 + x276 + x78 <= 1
c1759: x67 + x246 + x208 + x216 <= 1
c1760: x67 + x284 + x208 + x266 + x202 <= 1
c1761: x67 + x297 + x97 + x132 <= 1
c1762: x67 + x299 + x208 <= 1
c1763: x68 + x87 + x168 + x164 + x130 <= 1
c1764: x68 + x100 + x168 + x183 <= 1
c1765: x68 + x104 + x143 + x213 + x233 <= 1
c1766: x68 + x139 + x233 + x234 <= 1
c1767: x68 + x174 + x277 + x168 <= 1
c1768: x68 + x185 + x233 + x248 + x183 <= 1
c1769: x68 + x198 + x212 + x147 + x7 <= 1
c1770: x68 + x203 + x167 + x212 + x284 + x35 <= 1
c1771: x68 + x207 + x212 + x217 + x112 + x203 + x35 <= 1
c1772: x68 + x208 + x147 + x196 + x20 <= 1
c1773: x68 + x209 + x217 + x234 <= 1
c1774: x68 + x218 + x167 + x144 + x152 <= 1
c1775: x68 + x226 + x281 + x198 <= 1
c1776: x68 + x228 + x212 + x245 + x189 <= 1
c1777: x68 + x259 + x167 + x202 + x95 <= 1
c1778: x68 + x290 + x167 + x147 <= 1
c1779: x69 + x76 + x249 + x143 <= 1
c1780: x69 + x88 + x165 + x288 + x229 + x279 <= 1
c1781: x69 + x129 + x258 + x285 + x178 + x228 <= 1
c1782: x69 + x144 + x292 + x72 + x281 + x194 <= 1
c1783: x69 + x152 + x165 + x167 + x77 <= 1
c1784: x69 + x160 + x167 + x106 + x243 + x238 + x202 <= 1
c1785: x69 + x162 + x292 + x187 + x229 <= 1
c1786: x69 + x172 + x270 + x157 + x128 <= 1
c1787: x69 + x174 + x120 + x143 <= 1
c1788: x69 + x190 + x212 + x187 + x157 + x233 + x62 <= 1
c1789: x69 + x199 + x250 + x136 + x88 <= 1
c1790: x69 + x223 + x120 + x114 <= 1
c1791: x69 + x230 + x167 + x106 + x152 <= 1
c1792: x69 + x263 + x165 + x243 + x288 + x279 + x132 + x1 <= 1
c1793: x69 + x290 + x167 + x243 + x78 + x140 <= 1
c1794: x69 + x298 + x254 + x270 <= 1
c1795: x70 + x79 + x236 + x167 <= 1
c1796: x70 + x100 + x252 + x112 + x12 <= 1
c1797: x70 + x101 + x197 + x236 + x227 <= 1
c1798: x70 + x117 + x167 + x230 <= 1
c1799: x70 + x123 + x166 + x253 <= 1
c1800: x70 + x133 + x161 + x12 <= 1
c1801: x70 + x137 + x236 + x164 + x266 + x260 <= 1
c1802: x70 + x196 + x138 + x116 <= 1
c1803: x70 + x237 + x236 + x167 + x78 <= 1
c1804: x70 + x243 + x289 + x274 + x12 <= 1
c1805: x70 + x245 + x289 + x60 <= 1
c1806: x70 + x250 + x286 <= 1
c1807: x70 + x279 + x161 + x210 <= 1
c1808: x70 + x285 + x236 + x252 <= 1
c1809: x71 + x73 + x98 + x99 + x143 <= 1
c1810: x71 + x84 + x99 + x138 + x230 + x278 <= 1
c1811: x71 + x122 + x113 + x270 + x284 + x210 <= 1
c1812: x71 + x145 + x204 + x160 + x64 <= 1
c1813: x71 + x155 + x96 + x99 + x117 <= 1
c1814: x71 + x156 + x204 + x278 <= 1
c1815: x71 + x159 + x99 + x117 <= 1
c1816: x71 + x163 + x134 + x253 + x278 + x66 <= 1
c1817: x71 + x171 + x293 + x233 + x16 + x53 <= 1
c1818: x71 + x199 + x113 + x137 + x53 <= 1
c1819: x71 + x208 + x283 + x155 + x12 <= 1
c1820: x71 + x209 + x264 + x117 + x230 + x202 <= 1
c1821: x71 + x212 + x161 + x248 + x278 <= 1
c1822: x71 + x235 + x96 + x161 <= 1
c1823: x71 + x239 + x270 + x284 + x264 <= 1
c1824: x71 + x251 + x300 + x204 <= 1
c1825: x71 + x259 + x99 + x161 + x248 <= 1
c1826: x71 + x266 + x204 + x251 <= 1
c1827: x71 + x268 + x137 + x12 <= 1
c1828: x72 + x76 + x182 + x203 + x155 + x65 <= 1
c1829: x72 + x77 + x221 + x99 + x1 <= 1
c1830: x72 + x86 + x175 + x150 + x168 <= 1
c1831: x72 + x101 + x292 + x222 + x275 + x155 <= 1
c1832: x72 + x112 + x221 + x211 + x212 + x203 <= 1
c1833: x72 + x136 + x85 + x184 + x132 + x65 <= 1
c1834: x72 + x149 + x258 + x289 + x93 <= 1
c1835: x72 + x153 + x99 + x227 <= 1
c1836: x72 + x210 + x293 + x184 + x211 <= 1
c1837: x72 + x237 + x254 + x154 + x282 + x241 <= 1
c1838: x72 + x250 + x293 + x85 + x238 <= 1
c1839: x72 + x252 + x134 + x289 + x112 + x12 <= 1
c1840: x72 + x255 + x292 + x229 <= 1
c1841: x72 + x269 + x182 + x241 + x65 <= 1
c1842: x72 + x277 + x150 + x74 + x86 + x289 <= 1
c1843: x72 + x283 + x124 + x229 + x27 <= 1
c1844: x73 + x79 + x106 + x99 + x143 <= 1
c1845: x73 + x82 + x175 + x113 + x254 <= 1
c1846: x73 + x100 + x175 + x113 + x85 + x168 <= 1
c1847: x73 + x104 + x186 + x197 + x131 <= 1
c1848: x73 + x110 + x186 + x102 + x207 + x236 <= 1
c1849: x73 + x127 + x177 + x98 <= 1
c1850: x73 + x138 + x83 + x186 <= 1
c1851: x73 + x149 + x111 + x258 + x93 <= 1
c1852: x73 + x165 + x102 + x207 + x132 <= 1
c1853: x73 + x190 + x186 + x173 <= 1
c1854: x73 + x194 + x175 + x234 + x85 + x93 <= 1
c1855: x73 + x223 + x242 + x99 + x10 <= 1
c1856: x73 + x265 + x165 + x86 + x229 + x238 <= 1
c1857: x73 + x272 + x234 + x295 + x102 + x238 <= 1
c1858: x73 + x279 + x83 + x147 + x132 <= 1
c1859: x73 + x285 + x276 + x229 + x275 <= 1
c1860: x73 + x297 + x113 + x295 + x82 <= 1
c1861: x74 + x125 + x276 + x229 + x232 <= 1
c1862: x74 + x130 + x109 + x189 <= 1
c1863: x74 + x152 + x109 + x300 + x257 <= 1
c1864: x74 + x179 + x115 + x142 + x22 <= 1
c1865: x74 + x180 + x124 + x217 + x84 <= 1
c1866: x74 + x182 + x146 + x251 <= 1
c1867: x74 + x194 + x300 + x96 + x216 <= 1
c1868: x74 + x208 + x182 + x155 <= 1
c1869: x74 + x210 + x276 + x182 + x15 <= 1
c1870: x74 + x222 + x220 + x217 + x253 + x238 <= 1
c1871: x74 + x242 + x193 + x118 + x115 <= 1
c1872: x74 + x250 + x146 + x220 + x1 <= 1
c1873: x74 + x252 + x242 + x118 + x142 <= 1
c1874: x74 + x261 + x109 + x267 + x152 <= 1
c1875: x74 + x270 + x124 + x84 + x1 <= 1
c1876: x74 + x290 + x300 + x115 + x183 <= 1
c1877: x74 + x291 + x300 + x118 + x148 + x82 <= 1
c1878: x75 + x86 + x91 + x256 <= 1
c1879: x75 + x124 + x256 + x229 <= 1
c1880: x75 + x125 + x91 + x256 <= 1
c1881: x75 + x128 + x90 + x184 + x144 <= 1
c1882: x75 + x132 + x109 + x90 + x261 <= 1
c1883: x75 + x138 + x256 + x142 + x229 <= 1
c1884: x75 + x168 + x109 + x276 + x144 <= 1
c1885: x75 + x195 + x276 + x233 <= 1
c1886: x75 + x198 + x97 + x275 + x132 <= 1
c1887: x75 + x209 + x90 + x184 + x144 <= 1
c1888: x75 + x215 + x109 + x267 + x261 <= 1
c1889: x75 + x220 + x154 + x125 <= 1
c1890: x75 + x243 + x91 + x278 <= 1
c1891: x75 + x257 + x293 <= 1
c1892: x76 + x105 + x150 + x158 + x155 <= 1
c1893: x76 + x117 + x254 + x136 + x155 + x158 <= 1
c1894: x76 + x121 + x253 + x194 <= 1
c1895: x76 + x125 + x181 + x220 <= 1
c1896: x76 + x141 + x249 + x257 <= 1
c1897: x76 + x180 + x143 + x253 <= 1
c1898: x76 + x267 + x257 + x141 <= 1
c1899: x76 + x283 + x143 + x23 <= 1
c1900: x77 + x84 + x221 + x212 + x211 <= 1
c1901: x77 + x98 + x249 + x90 + x127 <= 1
c1902: x77 + x109 + x114 + x120 <= 1
c1903: x77 + x121 + x170 + x169 + x132 <= 1
c1904: x77 + x126 + x249 + x258 + x289 <= 1
c1905: x77 + x136 + x167 + x216 + x24 <= 1
c1906: x77 + x149 + x114 + x126 + x289 <= 1
c1907: x77 + x184 + x221 + x211 + x212 + x72 <= 1
c1908: x77 + x188 + x122 + x167 + x152 <= 1
c1909: x77 + x197 + x80 + x129 <= 1
c1910: x77 + x214 + x90 + x284 + x230 <= 1
c1911: x77 + x215 + x162 + x84 <= 1
c1912: x77 + x267 + x187 + x169 + x141 <= 1
c1913: x77 + x300 + x249 + x187 + x284 <= 1
c1914: x78 + x85 + x96 + x116 + x294 <= 1
c1915: x78 + x87 + x94 + x96 + x216 <= 1
c1916: x78 + x92 + x276 + x234 + x210 <= 1
c1917: x78 + x98 + x177 + x201 + x229 <= 1
c1918: x78 + x129 + x80 + x92 + x265 + x3 <= 1
c1919: x78 + x171 + x94 + x292 + x187 + x229 <= 1
c1920: x78 + x175 + x224 + x295 + x184 + x264 <= 1
c1921: x78 + x180 + x94 + x143 + x265 + x14 <= 1
c1922: x78 + x188 + x176 + x167 + x216 <= 1
c1923: x78 + x261 + x96 + x116 + x173 + x3 <= 1
c1924: x78 + x269 + x177 + x93 + x140 <= 1
c1925: x78 + x272 + x176 + x216 + x295 <= 1
c1926: x78 + x284 + x176 + x150 + x167 + x8 <= 1
c1927: x79 + x82 + x178 + x80 + x113 + x148 <= 1
c1928: x79 + x84 + x103 + x207 <= 1
c1929: x79 + x96 + x170 + x178 + x99 + x207 <= 1
c1930: x79 + x125 + x80 + x113 + x178 + x148 <= 1
c1931: x79 + x126 + x258 + x178 + x207 + x82 <= 1
c1932: x79 + x183 + x106 + x118 + x238 + x74 <= 1
c1933: x79 + x189 + x103 + x207 + x132 + x69 <= 1
c1934: x79 + x204 + x128 + x167 + x173 <= 1
c1935: x79 + x212 + x187 + x236 + x167 <= 1
c1936: x79 + x229 + x187 + x128 + x275 <= 1
c1937: x79 + x244 + x176 + x187 + x167 + x99 <= 1
c1938: x79 + x254 + x113 + x96 + x128 <= 1
c1939: x79 + x279 + x204 + x118 <= 1
c1940: x80 + x94 + x242 + x217 + x277 <= 1
c1941: x80 + x104 + x186 + x114 <= 1
c1942: x80 + x122 + x217 + x113 + x284 <= 1
c1943: x80 + x141 + x166 + x282 + x142 <= 1
c1944: x80 + x147 + x186 + x292 + x113 <= 1
c1945: x80 + x169 + x81 + x92 + x164 + x238 <= 1
c1946: x80 + x172 + x92 + x124 + x234 <= 1
c1947: x80 + x223 + x81 + x114 + x242 + x23 <= 1
c1948: x80 + x233 + x186 + x102 + x118 + x236 <= 1
c1949: x80 + x235 + x196 + x242 <= 1
c1950: x80 + x247 + x186 + x92 + x108 <= 1
c1951: x80 + x259 + x114 + x275 + x236 <= 1
c1952: x81 + x99 + x274 + x114 + x285 <= 1
c1953: x81 + x100 + x119 + x275 <= 1
c1954: x81 + x111 + x146 + x155 + x182 <= 1
c1955: x81 + x113 + x177 + x146 + x216 + x50 <= 1
c1956: x81 + x125 + x162 + x113 <= 1
c1957: x81 + x130 + x177 + x213 + x151 <= 1
c1958: x81 + x170 + x293 + x114 + x241 <= 1
c1959: x81 + x179 + x218 + x113 + x154 + x85 + x132 <= 1
c1960: x81 + x205 + x196 <= 1
c1961: x81 + x209 + x205 + x216 <= 1
c1962: x81 + x217 + x119 + x242 + x234 <= 1
c1963: x81 + x248 + x83 + x124 <= 1
c1964: x81 + x254 + x111 + x154 + x155 <= 1
c1965: x81 + x260 + x116 + x118 + x21 <= 1
c1966: x81 + x267 + x119 + x223 + x100 <= 1
c1967: x82 + x101 + x134 + x196 + x72 <= 1
c1968: x82 + x112 + x193 + x134 + x118 + x183 <= 1
c1969: x82 + x147 + x221 + x83 + x253 + x216 <= 1
c1970: x82 + x173 + x201 + x134 + x203 + x72 <= 1
c1971: x82 + x190 + x227 + x95 + x65 <= 1
c1972: x82 + x208 + x175 + x243 + x202 + x1 <= 1
c1973: x82 + x218 + x201 + x203 + x173 + x72 <= 1
c1974: x82 + x226 + x256 + x203 + x282 <= 1
c1975: x82 + x272 + x293 + x115 + x257 <= 1
c1976: x83 + x137 + x224 + x232 + x271 <= 1
c1977: x83 + x149 + x193 + x248 <= 1
c1978: x83 + x160 + x204 + x87 <= 1
c1979: x83 + x169 + x186 + x160 + x8 <= 1
c1980: x83 + x182 + x251 + x187 + x142 + x183 <= 1
c1981: x83 + x211 + x186 + x138 + x8 + x14 <= 1
c1982: x83 + x241 + x204 + x116 + x282 <= 1
c1983: x83 + x246 + x186 + x8 <= 1
c1984: x83 + x247 + x116 <= 1
c1985: x83 + x250 + x187 + x193 + x248 + x183 <= 1
c1986: x83 + x257 + x246 + x67 <= 1
c1987: x83 + x273 + x204 + x241 <= 1
c1988: x84 + x87 + x94 + x215 <= 1
c1989: x84 + x89 + x249 + x127 <= 1
c1990: x84 + x95 + x94 + x103 + x116 <= 1
c1991: x84 + x98 + x249 + x103 + x127 <= 1
c1992: x84 + x135 + x155 + x230 <= 1
c1993: x84 + x165 + x102 + x151 + x207 <= 1
c1994: x84 + x174 + x243 + x124 <= 1
c1995: x84 + x181 + x249 + x94 + x229 <= 1
c1996: x84 + x216 + x286 + x229 + x53 <= 1
c1997: x84 + x235 + x165 + x203 + x1 <= 1
c1998: x84 + x269 + x116 + x52 <= 1
c1999: x84 + x271 + x276 + x95 <= 1
c2000: x85 + x88 + x120 + x109 + x34 <= 1
c2001: x85 + x105 + x157 + x143 + x113 + x238 <= 1
c2002: x85 + x124 + x168 + x224 + x17 <= 1
c2003: x85 + x126 + x117 + x168 + x87 <= 1
c2004: x85 + x138 + x116 + x266 + x142 <= 1
c2005: x85 + x141 + x145 + x275 + x270 + x132 <= 1
c2006: x85 + x144 + x275 + x292 + x128 <= 1
c2007: x85 + x149 + x93 + x115 + x50 + x73 <= 1
c2008: x85 + x162 + x275 + x292 + x155 + x53 <= 1
c2009: x85 + x229 + x275 + x128 + x292 <= 1
c2010: x85 + x268 + x275 + x137 + x10 + x12 <= 1
c2011: x86 + x110 + x186 + x245 + x10 <= 1
c2012: x86 + x120 + x150 + x92 + x282 <= 1
c2013: x86 + x128 + x204 + x146 + x241 <= 1
c2014: x86 + x139 + x94 + x168 + x171 <= 1
c2015: x86 + x166 + x91 + x289 + x1 <= 1
c2016: x86 + x192 + x186 + x277 + x168 + x12 <= 1
c2017: x86 + x195 + x288 + x245 <= 1
c2018: x86 + x210 + x91 + x108 + x256 <= 1
c2019: x86 + x221 + x288 + x195 + x1 <= 1
c2020: x86 + x251 + x204 + x146 + x241 <= 1
c2021: x86 + x268 + x106 + x201 <= 1
c2022: x86 + x269 + x91 + x288 + x1 <= 1
c2023: x86 + x280 + x106 + x238 + x1 + x69 <= 1
c2024: x86 + x291 + x161 + x247 <= 1
c2025: x86 + x298 + x186 + x201 + x14 + x61 <= 1
c2026: x87 + x97 + x176 + x187 + x112 <= 1
c2027: x87 + x129 + x204 + x258 + x300 <= 1
c2028: x87 + x158 + x164 + x160 + x128 <= 1
c2029: x87 + x159 + x204 <= 1
c2030: x87 + x166 + x123 <= 1
c2031: x87 + x175 + x204 + x243 + x118 + x202 + x1 <= 1
c2032: x87 + x193 + x232 + x118 + x112 + x132 <= 1
c2033: x87 + x222 + x97 + x187 + x265 <= 1
c2034: x87 + x227 + x97 + x187 + x300 + x112 <= 1
c2035: x87 + x244 + x176 + x187 <= 1
c2036: x87 + x254 + x94 + x96 + x117 <= 1
c2037: x87 + x259 + x97 + x1 <= 1
c2038: x87 + x263 + x97 + x112 + x132 <= 1
c2039: x87 + x289 + x187 + x284 + x265 <= 1
c2040: x88 + x94 + x167 + x114 + x150 + x181 <= 1
c2041: x88 + x145 + x200 + x114 <= 1
c2042: x88 + x162 + x292 + x278 + x155 <= 1
c2043: x88 + x216 + x286 + x126 + x229 <= 1
c2044: x88 + x236 + x201 + x147 <= 1
c2045: x88 + x295 + x109 + x278 + x120 <= 1
c2046: x88 + x297 + x97 + x134 + x29 <= 1
c2047: x89 + x110 + x249 + x229 + x65 <= 1
c2048: x89 + x133 + x282 <= 1
c2049: x89 + x143 + x249 + x14 <= 1
c2050: x89 + x153 + x140 + x3 <= 1
c2051: x89 + x157 + x113 + x172 + x143 + x53 <= 1
c2052: x89 + x169 + x249 + x201 + x181 <= 1
c2053: x89 + x185 + x249 + x191 <= 1
c2054: x89 + x192 + x234 + x229 <= 1
c2055: x89 + x263 + x181 + x229 <= 1
c2056: x89 + x285 + x116 + x113 <= 1
c2057: x90 + x95 + x103 + x184 + x127 + x148 <= 1
c2058: x90 + x137 + x240 + x127 + x10 <= 1
c2059: x90 + x145 + x103 + x170 + x132 <= 1
c2060: x90 + x155 + x111 + x140 + x211 <= 1
c2061: x90 + x173 + x186 + x184 + x128 + x32 <= 1
c2062: x90 + x193 + x240 + x233 <= 1
c2063: x90 + x203 + x91 + x284 <= 1
c2064: x90 + x207 + x91 + x278 + x203 <= 1
c2065: x90 + x213 + x284 + x151 <= 1
c2066: x90 + x228 + x91 + x75 <= 1
c2067: x90 + x237 + x207 + x203 + x194 <= 1
c2068: x90 + x250 + x293 + x211 <= 1
c2069: x90 + x271 + x262 + x155 + x194 <= 1
c2070: x90 + x282 + x274 + x148 + x194 <= 1
c2071: x90 + x283 + x118 + x142 + x229 <= 1
c2072: x90 + x297 + x91 + x284 + x11 + x45 <= 1
c2073: x91 + x101 + x116 + x189 + x150 + x8 <= 1
c2074: x91 + x104 + x232 + x114 <= 1
c2075: x91 + x122 + x116 + x238 <= 1
c2076: x91 + x133 + x178 + x243 + x8 <= 1
c2077: x91 + x162 + x166 + x8 <= 1
c2078: x91 + x169 + x108 + x256 <= 1
c2079: x91 + x172 + x118 + x218 + x238 + x1 <= 1
c2080: x91 + x183 + x122 + x238 <= 1
c2081: x91 + x200 + x232 + x278 + x112 + x210 <= 1
c2082: x91 + x219 + x284 + x289 <= 1
c2083: x91 + x235 + x115 + x278 + x203 + x1 <= 1
c2084: x91 + x244 + x288 + x178 + x39 <= 1
c2085: x91 + x248 + x212 + x278 + x23 <= 1
c2086: x91 + x273 + x256 + x284 + x212 <= 1
c2087: x91 + x277 + x243 + x218 + x238 <= 1
c2088: x91 + x279 + x98 + x118 + x1 <= 1
c2089: x91 + x300 + x108 + x178 + x288 <= 1
c2090: x92 + x98 + x249 + x127 + x129 + x27 <= 1
c2091: x92 + x115 + x93 + x186 + x233 <= 1
c2092: x92 + x126 + x197 + x243 + x167 + x8 <= 1
c2093: x92 + x162 + x276 + x106 <= 1
c2094: x92 + x180 + x93 + x186 + x233 + x210 <= 1
c2095: x92 + x218 + x93 + x186 + x167 + x8 <= 1
c2096: x92 + x222 + x108 + x265 + x238 + x86 <= 1
c2097: x92 + x248 + x292 + x128 + x173 + x186 <= 1
c2098: x92 + x254 + x93 + x108 + x128 <= 1
c2099: x92 + x290 + x164 + x127 <= 1
c2100: x92 + x293 + x262 + x115 <= 1
c2101: x93 + x116 + x131 + x233 + x158 <= 1
c2102: x93 + x119 + x242 + x284 + x234 <= 1
c2103: x93 + x127 + x177 + x201 + x39 <= 1
c2104: x93 + x139 + x177 + x242 + x234 <= 1
c2105: x93 + x142 + x187 + x111 + x230 <= 1
c2106: x93 + x193 + x245 + x186 + x167 <= 1
c2107: x93 + x199 + x188 + x250 + x85 <= 1
c2108: x93 + x200 + x258 + x278 + x73 <= 1
c2109: x93 + x216 + x177 + x131 + x167 + x78 <= 1
c2110: x93 + x235 + x242 + x278 + x115 <= 1
c2111: x93 + x279 + x119 + x284 + x210 + x46 <= 1
c2112: x93 + x291 + x154 + x175 + x127 <= 1
c2113: x94 + x100 + x121 + x224 + x265 <= 1
c2114: x94 + x107 + x121 + x242 + x66 <= 1
c2115: x94 + x125 + x123 + x253 <= 1
c2116: x94 + x140 + x103 + x266 + x116 <= 1
c2117: x94 + x164 + x121 + x275 + x292 + x142 <= 1
c2118: x94 + x195 + x281 + x217 + x141 <= 1
c2119: x94 + x207 + x96 + x178 + x155 <= 1
c2120: x94 + x247 + x105 + x60 <= 1
c2121: x94 + x252 + x181 + x292 + x242 + x142 <= 1
c2122: x94 + x274 + x276 + x114 + x285 <= 1
c2123: x95 + x156 + x103 + x132 <= 1
c2124: x95 + x163 + x239 + x202 <= 1
c2125: x95 + x182 + x146 + x155 + x127 + x30 <= 1
c2126: x95 + x188 + x206 + x275 <= 1
c2127: x95 + x193 + x122 + x227 + x247 <= 1
c2128: x95 + x199 + x224 + x184 + x85 <= 1
c2129: x95 + x234 + x206 + x184 + x295 + x210 <= 1
c2130: x95 + x278 + x224 + x204 + x168 + x282 <= 1
c2131: x95 + x293 + x232 + x233 + x210 <= 1
c2132: x96 + x106 + x253 + x238 + x74 <= 1
c2133: x96 + x151 + x294 + x213 + x284 + x6 <= 1
c2134: x96 + x157 + x198 + x178 + x113 + x16 <= 1
c2135: x96 + x184 + x178 + x113 + x128 <= 1
c2136: x96 + x185 + x233 + x16 <= 1
c2137: x96 + x226 + x198 + x281 + x34 <= 1
c2138: x96 + x240 + x294 + x178 + x116 + x300 <= 1
c2139: x96 + x256 + x161 + x194 <= 1
c2140: x96 + x272 + x116 + x131 + x289 + x34 <= 1
c2141: x96 + x283 + x106 <= 1
c2142: x96 + x288 + x198 + x178 + x113 + x16 <= 1
c2143: x97 + x121 + x191 + x232 + x222 <= 1
c2144: x97 + x124 + x217 + x239 <= 1
c2145: x97 + x141 + x134 + x196 + x132 + x2 <= 1
c2146: x97 + x147 + x196 + x187 + x275 + x132 <= 1
c2147: x97 + x151 + x258 + x241 <= 1
c2148: x97 + x156 + x287 + x196 + x143 <= 1
c2149: x97 + x169 + x134 + x251 + x172 <= 1
c2150: x97 + x180 + x287 + x143 + x156 <= 1
c2151: x97 + x192 + x198 + x264 + x227 <= 1
c2152: x97 + x200 + x258 + x241 + x300 <= 1
c2153: x97 + x203 + x217 + x134 + x112 + x113 + x53 <= 1
c2154: x97 + x255 + x257 <= 1
c2155: x97 + x262 + x258 + x222 <= 1
c2156: x97 + x268 + x275 + x148 + x12 <= 1
c2157: x97 + x269 + x187 + x198 + x264 <= 1
c2158: x98 + x128 + x224 + x204 + x178 + x184 <= 1
c2159: x98 + x154 + x201 + x129 + x127 <= 1
c2160: x98 + x158 + x130 + x202 + x229 <= 1
c2161: x98 + x164 + x154 + x220 <= 1
c2162: x98 + x188 + x154 + x77 <= 1
c2163: x98 + x195 + x103 + x129 <= 1
c2164: x98 + x223 + x201 + x249 + x99 + x127 <= 1
c2165: x98 + x246 + x201 + x203 + x39 <= 1
c2166: x98 + x258 + x249 + x201 + x118 + x127 <= 1
c2167: x98 + x270 + x177 + x2 + x51 <= 1
c2168: x99 + x104 + x266 + x272 + x295 <= 1
c2169: x99 + x112 + x176 + x272 + x207 <= 1
c2170: x99 + x116 + x206 + x138 <= 1
c2171: x99 + x160 + x191 + x186 + x138 <= 1
c2172: x99 + x164 + x176 + x272 <= 1
c2173: x99 + x174 + x109 + x143 + x168 <= 1
c2174: x99 + x224 + x244 + x178 + x285 <= 1
c2175: x99 + x226 + x206 + x187 + x41 <= 1
c2176: x99 + x298 + x182 + x201 + x127 <= 1
c2177: x100 + x135 + x140 + x231 + x46 <= 1
c2178: x100 + x146 + x294 + x264 <= 1
c2179: x100 + x156 + x287 + x9 <= 1
c2180: x100 + x158 + x102 + x114 + x140 + x207 <= 1
c2181: x100 + x169 + x154 + x266 + x113 + x216 <= 1
c2182: x100 + x190 + x146 + x136 + x216 <= 1
c2183: x100 + x204 + x245 + x157 + x228 <= 1
c2184: x100 + x285 + x114 + x252 + x145 + x94 <= 1
c2185: x100 + x288 + x211 + x265 + x121 + x224 <= 1
c2186: x101 + x121 + x119 + x120 + x198 + x275 <= 1
c2187: x101 + x136 + x119 + x196 <= 1
c2188: x101 + x145 + x181 + x196 + x67 <= 1
c2189: x101 + x149 + x147 + x212 <= 1
c2190: x101 + x176 + x296 + x150 + x181 <= 1
c2191: x101 + x179 + x134 + x196 <= 1
c2192: x101 + x182 + x280 + x238 <= 1
c2193: x101 + x195 + x276 + x196 <= 1
c2194: x101 + x260 + x276 + x211 + x288 <= 1
c2195: x101 + x284 + x176 + x150 + x8 <= 1
c2196: x101 + x295 + x176 + x251 + x150 <= 1
c2197: x102 + x106 + x114 + x202 + x148 <= 1
c2198: x102 + x108 + x233 + x131 + x186 + x64 <= 1
c2199: x102 + x120 + x110 + x238 <= 1
c2200: x102 + x155 + x166 + x282 + x8 <= 1
c2201: x102 + x176 + x131 + x272 + x216 <= 1
c2202: x102 + x194 + x161 + x211 + x8 <= 1
c2203: x102 + x220 + x161 + x166 <= 1
c2204: x102 + x232 + x233 + x118 + x210 <= 1
c2205: x102 + x242 + x225 + x230 + x66 + x80 <= 1
c2206: x102 + x257 + x165 + x166 + x113 <= 1
c2207: x102 + x259 + x236 + x114 + x202 + x80 <= 1
c2208: x102 + x264 + x281 + x230 <= 1
c2209: x102 + x273 + x212 + x8 + x32 <= 1
c2210: x102 + x292 + x281 + x148 + x194 <= 1
c2211: x103 + x119 + x208 + x266 <= 1
c2212: x103 + x131 + x189 + x227 + x8 <= 1
c2213: x103 + x142 + x205 + x233 + x183 <= 1
c2214: x103 + x191 + x170 + x233 <= 1
c2215: x103 + x192 + x227 + x279 <= 1
c2216: x103 + x228 + x189 + x131 + x116 + x8 <= 1
c2217: x103 + x251 + x249 + x187 + x295 + x222 <= 1
c2218: x103 + x257 + x173 + x140 + x228 + x51 <= 1
c2219: x103 + x259 + x291 + x238 + x41 <= 1
c2220: x103 + x260 + x163 + x266 + x112 + x50 <= 1
c2221: x103 + x261 + x189 + x183 + x132 <= 1
c2222: x103 + x288 + x163 + x232 + x50 <= 1
c2223: x104 + x144 + x253 + x184 <= 1
c2224: x104 + x189 + x299 + x183 + x12 <= 1
c2225: x104 + x202 + x253 + x114 + x229 <= 1
c2226: x104 + x234 + x151 + x295 <= 1
c2227: x104 + x261 + x258 + x148 <= 1
c2228: x104 + x284 + x213 + x120 + x143 + x69 <= 1
c2229: x104 + x285 + x258 + x151 + x144 + x69 <= 1
c2230: x104 + x290 + x266 + x295 + x12 <= 1
c2231: x105 + x111 + x146 + x155 + x182 <= 1
c2232: x105 + x112 + x201 + x262 <= 1
c2233: x105 + x133 + x111 + x285 <= 1
c2234: x105 + x137 + x152 + x113 + x169 <= 1
c2235: x105 + x151 + x177 + x155 + x216 <= 1
c2236: x105 + x184 + x137 + x113 + x64 + x85 <= 1
c2237: x105 + x202 + x243 + x238 + x1 + x15 <= 1
c2238: x105 + x227 + x111 + x247 <= 1
c2239: x105 + x254 + x152 + x113 + x148 + x169 <= 1
c2240: x105 + x300 + x152 + x227 + x85 <= 1
c2241: x106 + x127 + x130 + x243 + x189 + x183 + x228 <= 1
c2242: x106 + x134 + x152 + x252 + x230 + x12 <= 1
c2243: x106 + x141 + x280 + x118 + x238 <= 1
c2244: x106 + x149 + x130 + x266 + x12 <= 1
c2245: x106 + x225 + x286 + x253 + x278 <= 1
c2246: x106 + x277 + x243 + x238 + x218 <= 1
c2247: x106 + x287 + x276 + x282 <= 1
c2248: x106 + x300 + x152 + x134 + x12 <= 1
c2249: x107 + x116 + x152 + x272 <= 1
c2250: x107 + x117 + x152 + x242 <= 1
c2251: x107 + x143 + x174 + x177 + x113 <= 1
c2252: x107 + x155 + x187 + x117 + x183 <= 1
c2253: x107 + x185 + x177 + x242 + x34 + x66 <= 1
c2254: x107 + x190 + x187 + x284 + x69 <= 1
c2255: x107 + x229 + x201 + x242 + x177 + x34 + x39 <= 1
c2256: x107 + x243 + x174 + x189 + x69 <= 1
c2257: x107 + x245 + x152 + x113 + x167 <= 1
c2258: x107 + x269 + x152 + x174 + x10 <= 1
c2259: x108 + x135 + x296 + x230 <= 1
c2260: x108 + x136 + x186 + x233 + x288 <= 1
c2261: x108 + x153 + x215 + x128 + x41 <= 1
c2262: x108 + x154 + x299 + x175 + x278 + x12 <= 1
c2263: x108 + x167 + x215 + x128 + x34 + x41 <= 1
c2264: x108 + x190 + x173 + x128 + x186 <= 1
c2265: x108 + x193 + x265 + x187 + x23 <= 1
c2266: x108 + x213 + x296 + x238 + x230 + x47 <= 1
c2267: x108 + x217 + x211 + x299 <= 1
c2268: x108 + x220 + x213 + x238 + x222 <= 1
c2269: x108 + x225 + x178 + x154 + x187 <= 1
c2270: x108 + x251 + x124 + x187 <= 1
c2271: x108 + x264 + x217 + x187 + x195 + x284 <= 1
c2272: x109 + x113 + x198 + x168 + x143 + x85 <= 1
c2273: x109 + x122 + x215 + x152 + x167 + x77 <= 1
c2274: x109 + x139 + x215 + x282 + x34 <= 1
c2275: x109 + x149 + x130 + x215 <= 1
c2276: x109 + x196 + x276 + x205 <= 1
c2277: x109 + x204 + x276 + x168 + x282 <= 1
c2278: x109 + x211 + x275 + x276 + x196 <= 1
c2279: x109 + x228 + x130 + x144 <= 1
c2280: x109 + x234 + x206 + x295 + x257 + x29 <= 1
c2281: x109 + x236 + x130 + x202 <= 1
c2282: x109 + x264 + x198 + x19 <= 1
c2283: x109 + x298 + x158 + x2 <= 1
c2284: x110 + x119 + x221 + x51 + x53 <= 1
c2285: x110 + x125 + x178 + x148 + x142 + x80 <= 1
c2286: x110 + x126 + x178 + x249 + x207 <= 1
c2287: x110 + x138 + x173 + x186 + x142 <= 1
c2288: x110 + x158 + x283 + x140 + x228 <= 1
c2289: x110 + x164 + x221 + x238 + x2 <= 1
c2290: x110 + x184 + x173 + x221 + x72 <= 1
c2291: x110 + x195 + x173 + x221 + x51 + x53 <= 1
c2292: x110 + x262 + x229 + x36 <= 1
c2293: x111 + x114 + x163 + x236 + x218 <= 1
c2294: x111 + x151 + x147 + x37 <= 1
c2295: x111 + x172 + x176 + x218 <= 1
c2296: x111 + x224 + x123 + x17 <= 1
c2297: x111 + x234 + x274 + x295 + x81 <= 1
c2298: x111 + x238 + x244 + x236 + x288 <= 1
c2299: x111 + x256 + x274 + x114 <= 1
c2300: x111 + x257 + x146 + x74 <= 1
c2301: x111 + x284 + x163 + x253 <= 1
c2302: x111 + x292 + x274 + x144 + x24 <= 1
c2303: x112 + x145 + x294 + x186 + x210 + x132 <= 1
c2304: x112 + x179 + x294 + x284 + x39 <= 1
c2305: x112 + x213 + x294 + x120 + x284 <= 1
c2306: x112 + x224 + x294 + x213 + x300 <= 1
c2307: x112 + x235 + x157 + x241 + x278 + x172 <= 1
c2308: x112 + x237 + x163 + x203 + x284 <= 1
c2309: x112 + x270 + x147 + x113 + x292 <= 1
c2310: x113 + x123 + x166 + x134 <= 1
c2311: x113 + x182 + x198 + x146 + x118 + x132 <= 1
c2312: x113 + x208 + x147 + x175 + x132 <= 1
c2313: x113 + x240 + x150 + x178 + x116 + x96 <= 1
c2314: x113 + x241 + x165 + x137 + x238 + x85 <= 1
c2315: x113 + x277 + x165 + x265 + x238 + x23 <= 1
c2316: x113 + x279 + x165 + x150 + x217 + x277 + x284 <= 1
c2317: x113 + x290 + x123 + x203 + x167 <= 1
c2318: x113 + x291 + x154 + x266 <= 1
c2319: x113 + x299 + x265 + x248 + x257 <= 1
c2320: x114 + x117 + x196 + x221 + x1 <= 1
c2321: x114 + x138 + x274 + x186 + x80 <= 1
c2322: x114 + x159 + x275 + x236 + x167 <= 1
c2323: x114 + x175 + x243 + x140 + x167 <= 1
c2324: x114 + x219 + x276 + x210 <= 1
c2325: x114 + x261 + x181 + x243 + x167 + x31 <= 1
c2326: x114 + x267 + x232 + x102 <= 1
c2327: x114 + x281 + x276 + x157 <= 1
c2328: x115 + x137 + x128 + x276 + x232 <= 1
c2329: x115 + x138 + x161 + x278 + x142 + x50 <= 1
c2330: x115 + x140 + x144 + x128 + x17 + x85 <= 1
c2331: x115 + x146 + x121 + x128 <= 1
c2332: x115 + x152 + x233 + x232 + x55 <= 1
c2333: x115 + x159 + x278 + x140 + x204 <= 1
c2334: x115 + x164 + x121 + x128 + x232 <= 1
c2335: x115 + x269 + x161 + x144 <= 1
c2336: x115 + x274 + x161 + x144 <= 1
c2337: x115 + x279 + x161 + x144 + x142 <= 1
c2338: x116 + x121 + x170 + x178 <= 1
c2339: x116 + x181 + x240 + x150 + x167 + x31 <= 1
c2340: x116 + x208 + x206 + x189 + x52 <= 1
c2341: x116 + x244 + x231 + x223 <= 1
c2342: x116 + x255 + x130 + x213 <= 1
c2343: x116 + x275 + x206 + x222 + x95 <= 1
c2344: x116 + x278 + x275 + x230 + x285 + x99 <= 1
c2345: x116 + x298 + x181 + x270 <= 1
c2346: x116 + x299 + x173 + x282 + x142 + x22 <= 1
c2347: x117 + x131 + x214 + x145 + x229 <= 1
c2348: x117 + x150 + x246 + x50 <= 1
c2349: x117 + x162 + x246 <= 1
c2350: x117 + x164 + x286 + x168 + x99 <= 1
c2351: x117 + x178 + x124 + x129 <= 1
c2352: x117 + x185 + x242 + x118 + x202 <= 1
c2353: x117 + x205 + x168 + x183 + x175 <= 1
c2354: x118 + x120 + x258 + x143 + x69 <= 1
c2355: x118 + x133 + x252 + x134 + x230 <= 1
c2356: x118 + x136 + x233 + x186 <= 1
c2357: x118 + x153 + x130 + x198 <= 1
c2358: x118 + x206 + x173 + x183 + x74 <= 1
c2359: x118 + x247 + x236 + x272 + x202 <= 1
c2360: x118 + x261 + x258 + x148 + x3 + x46 <= 1
c2361: x118 + x274 + x243 + x130 + x295 <= 1
c2362: x118 + x281 + x280 + x141 <= 1
c2363: x119 + x143 + x258 + x275 + x248 + x120 <= 1
c2364: x119 + x144 + x161 + x275 + x248 <= 1
c2365: x119 + x178 + x197 + x198 <= 1
c2366: x119 + x186 + x197 + x242 <= 1
c2367: x119 + x192 + x196 + x242 + x143 <= 1
c2368: x119 + x232 + x286 <= 1
c2369: x119 + x244 + x196 + x143 + x14 <= 1
c2370: x119 + x245 + x286 + x34 + x53 <= 1
c2371: x119 + x289 + x258 + x275 + x245 + x34 <= 1
c2372: x120 + x134 + x265 + x137 + x184 <= 1
c2373: x120 + x173 + x128 + x121 + x52 <= 1
c2374: x120 + x190 + x265 + x194 + x137 + x284 <= 1
c2375: x120 + x210 + x294 + x284 + x6 <= 1
c2376: x120 + x225 + x265 + x295 + x184 <= 1
c2377: x120 + x247 + x248 + x9 <= 1
c2378: x120 + x263 + x174 + x282 + x69 <= 1
c2379: x120 + x299 + x265 + x248 + x183 + x50 <= 1
c2380: x121 + x129 + x201 + x265 + x228 <= 1
c2381: x121 + x163 + x253 + x221 + x232 + x47 <= 1
c2382: x121 + x171 + x296 + x173 + x53 <= 1
c2383: x121 + x188 + x160 + x66 + x85 <= 1
c2384: x121 + x192 + x168 + x198 + x242 <= 1
c2385: x121 + x200 + x128 + x232 + x47 <= 1
c2386: x121 + x205 + x128 + x186 <= 1
c2387: x121 + x246 + x170 + x201 + x234 <= 1
c2388: x122 + x157 + x227 + x237 + x95 <= 1
c2389: x122 + x170 + x227 + x247 <= 1
c2390: x122 + x175 + x168 + x180 <= 1
c2391: x122 + x209 + x249 + x46 <= 1
c2392: x122 + x211 + x203 + x217 <= 1
c2393: x122 + x220 + x203 + x217 + x238 + x113 <= 1
c2394: x122 + x223 + x249 + x284 + x210 <= 1
c2395: x122 + x255 + x294 + x213 + x116 <= 1
c2396: x122 + x258 + x249 + x241 + x46 <= 1
c2397: x123 + x130 + x215 + x243 + x189 + x12 <= 1
c2398: x123 + x149 + x215 + x130 + x12 <= 1
c2399: x123 + x163 + x253 + x134 + x47 + x50 <= 1
c2400: x123 + x181 + x199 + x243 + x187 <= 1
c2401: x123 + x191 + x166 + x233 + x253 <= 1
c2402: x123 + x196 + x243 + x181 + x187 + x242 <= 1
c2403: x123 + x213 + x189 + x130 + x224 <= 1
c2404: x123 + x227 + x199 + x187 + x64 <= 1
c2405: x123 + x235 + x203 + x130 + x194 <= 1
c2406: x123 + x245 + x191 <= 1
c2407: x123 + x262 + x293 + x85 <= 1
c2408: x123 + x275 + x253 + x187 + x233 + x94 <= 1
c2409: x124 + x143 + x283 + x23 <= 1
c2410: x124 + x201 + x239 + x276 <= 1
c2411: x124 + x213 + x128 + x248 + x17 <= 1
c2412: x124 + x232 + x293 <= 1
c2413: x124 + x245 + x157 + x234 + x276 <= 1
c2414: x124 + x267 + x215 + x65 <= 1
c2415: x124 + x273 + x217 + x157 <= 1
c2416: x124 + x285 + x283 + x229 <= 1
c2417: x125 + x161 + x280 + x142 <= 1
c2418: x125 + x172 + x207 + x69 <= 1
c2419: x125 + x191 + x280 + x178 <= 1
c2420: x125 + x217 + x253 + x220 + x14 <= 1
c2421: x125 + x228 + x253 + x191 + x63 <= 1
c2422: x125 + x239 + x162 + x276 <= 1
c2423: x125 + x298 + x181 + x186 + x10 <= 1
c2424: x126 + x142 + x197 + x168 + x242 <= 1
c2425: x126 + x182 + x286 + x142 <= 1
c2426: x126 + x189 + x243 + x242 + x17 <= 1
c2427: x126 + x199 + x243 + x289 <= 1
c2428: x126 + x222 + x249 + x168 <= 1
c2429: x126 + x252 + x286 + x148 + x282 + x142 <= 1
c2430: x126 + x256 + x197 + x142 <= 1
c2431: x126 + x270 + x243 + x233 + x2 <= 1
c2432: x127 + x138 + x154 + x129 + x201 + x61 <= 1
c2433: x127 + x171 + x173 + x174 + x39 <= 1
c2434: x127 + x180 + x265 + x211 + x194 + x39 <= 1
c2435: x127 + x200 + x212 + x189 + x6 <= 1
c2436: x127 + x208 + x154 + x155 + x189 <= 1
c2437: x127 + x244 + x182 + x228 + x30 + x36 <= 1
c2438: x127 + x248 + x154 + x155 + x36 + x64 <= 1
c2439: x128 + x161 + x280 + x248 <= 1
c2440: x128 + x196 + x158 + x241 + x276 <= 1
c2441: x128 + x227 + x158 + x210 + x93 <= 1
c2442: x128 + x235 + x203 + x161 + x115 <= 1
c2443: x128 + x259 + x295 + x275 + x80 <= 1
c2444: x128 + x264 + x187 + x295 <= 1
c2445: x128 + x266 + x215 + x204 <= 1
c2446: x128 + x281 + x280 + x69 <= 1
c2447: x128 + x285 + x203 + x275 + x232 <= 1
c2448: x129 + x135 + x231 + x230 <= 1
c2449: x129 + x153 + x237 + x67 <= 1
c2450: x129 + x162 + x239 + x141 + x6 <= 1
c2451: x129 + x185 + x271 + x258 + x289 <= 1
c2452: x129 + x196 + x271 + x134 + x141 <= 1
c2453: x129 + x288 + x249 + x230 + x178 + x204 <= 1
c2454: x129 + x299 + x271 + x257 <= 1
c2455: x130 + x147 + x198 + x173 + x132 + x66 <= 1
c2456: x130 + x176 + x177 <= 1
c2457: x130 + x179 + x148 + x140 + x74 <= 1
c2458: x130 + x193 + x209 + x144 <= 1
c2459: x130 + x225 + x243 + x265 + x295 + x66 <= 1
c2460: x130 + x252 + x236 + x202 + x12 <= 1
c2461: x130 + x292 + x147 + x152 <= 1
c2462: x131 + x143 + x249 + x233 <= 1
c2463: x131 + x146 + x177 + x176 + x155 + x216 + x2 <= 1
c2464: x131 + x154 + x214 + x231 + x282 <= 1
c2465: x131 + x174 + x177 + x134 + x289 + x132 <= 1
c2466: x131 + x199 + x214 + x132 + x1 <= 1
c2467: x131 + x262 + x154 + x155 <= 1
c2468: x131 + x276 + x199 + x162 <= 1
c2469: x132 + x211 + x253 + x265 + x180 + x184 <= 1
c2470: x132 + x286 + x253 + x183 <= 1
c2471: x132 + x291 + x294 + x241 + x254 + x41 <= 1
c2472: x132 + x296 + x249 + x258 + x241 + x46 <= 1
c2473: x133 + x156 + x243 + x134 + x12 <= 1
c2474: x133 + x169 + x187 + x198 + x178 <= 1
c2475: x133 + x212 + x187 + x198 + x178 <= 1
c2476: x133 + x224 + x198 + x243 + x178 <= 1
c2477: x133 + x241 + x156 + x252 + x11 <= 1
c2478: x133 + x296 + x230 + x261 + x64 <= 1
c2479: x134 + x139 + x215 + x261 + x12 + x34 <= 1
c2480: x134 + x145 + x215 + x203 + x27 + x53 <= 1
c2481: x134 + x185 + x249 + x242 + x34 + x66 <= 1
c2482: x134 + x247 + x242 + x186 + x193 + x118 <= 1
c2483: x134 + x293 + x173 + x201 + x14 + x72 <= 1
c2484: x135 + x184 + x265 + x266 + x113 <= 1
c2485: x135 + x217 + x187 + x195 + x284 + x108 <= 1
c2486: x135 + x220 + x166 + x289 + x1 + x41 <= 1
c2487: x135 + x246 + x236 + x233 + x186 <= 1
c2488: x135 + x283 + x187 + x183 + x155 <= 1
c2489: x136 + x157 + x207 + x278 + x194 + x242 + x6 <= 1
c2490: x136 + x198 + x158 + x155 <= 1
c2491: x136 + x231 + x295 + x186 + x64 <= 1
c2492: x137 + x146 + x236 + x275 <= 1
c2493: x137 + x173 + x172 + x238 + x224 + x74 <= 1
c2494: x137 + x185 + x271 + x276 <= 1
c2495: x137 + x188 + x287 + x236 <= 1
c2496: x137 + x263 + x165 + x275 <= 1
c2497: x137 + x298 + x172 + x238 + x224 + x74 <= 1
c2498: x137 + x300 + x240 + x152 <= 1
c2499: x138 + x189 + x278 + x154 + x242 + x134 <= 1
c2500: x138 + x197 + x191 + x186 + x173 <= 1
c2501: x138 + x227 + x197 + x256 <= 1
c2502: x138 + x280 + x191 <= 1
c2503: x139 + x151 + x234 + x177 + x81 <= 1
c2504: x139 + x180 + x287 + x168 <= 1
c2505: x139 + x191 + x233 + x53 + x97 <= 1
c2506: x139 + x192 + x234 + x284 + x242 <= 1
c2507: x139 + x260 + x234 + x284 + x46 <= 1
c2508: x139 + x268 + x171 + x12 + x86 <= 1
c2509: x140 + x166 + x158 + x233 + x102 <= 1
c2510: x140 + x246 + x152 + x233 + x210 + x22 <= 1
c2511: x140 + x253 + x160 + x278 + x154 <= 1
c2512: x140 + x258 + x160 + x278 + x204 <= 1
c2513: x140 + x273 + x152 + x169 <= 1
c2514: x140 + x297 + x233 + x210 + x3 <= 1
c2515: x141 + x213 + x150 + x163 + x94 <= 1
c2516: x141 + x246 + x280 + x150 <= 1
c2517: x141 + x250 + x187 + x292 <= 1
c2518: x141 + x256 + x207 + x249 + x169 <= 1
c2519: x141 + x289 + x271 + x166 + x134 <= 1
c2520: x142 + x163 + x230 + x278 + x203 + x238 + x69 <= 1
c2521: x142 + x176 + x181 + x187 + x167 <= 1
c2522: x142 + x223 + x265 + x183 <= 1
c2523: x142 + x241 + x197 + x148 + x167 + x116 <= 1
c2524: x142 + x243 + x160 + x187 + x265 + x87 <= 1
c2525: x143 + x162 + x215 + x2 + x53 <= 1
c2526: x143 + x220 + x147 + x166 + x253 + x14 <= 1
c2527: x143 + x221 + x147 + x233 + x253 + x275 <= 1
c2528: x143 + x237 + x168 + x227 + x72 <= 1
c2529: x143 + x274 + x148 + x12 + x15 <= 1
c2530: x143 + x281 + x168 + x249 + x94 <= 1
c2531: x143 + x298 + x172 + x238 + x248 + x14 <= 1
c2532: x144 + x169 + x160 + x258 + x269 + x45 <= 1
c2533: x144 + x172 + x294 + x227 <= 1
c2534: x144 + x207 + x291 + x275 <= 1
c2535: x144 + x226 + x230 + x194 + x281 <= 1
c2536: x144 + x231 + x295 + x211 <= 1
c2537: x144 + x293 + x168 + x72 + x85 <= 1
c2538: x145 + x172 + x294 + x30 + x53 + x112 <= 1
c2539: x145 + x187 + x160 + x243 <= 1
c2540: x145 + x281 + x217 + x94 + x141 <= 1
c2541: x145 + x282 + x214 + x258 + x16 + x20 <= 1
c2542: x145 + x299 + x214 + x183 <= 1
c2543: x146 + x167 + x251 + x182 + x241 <= 1
c2544: x146 + x201 + x177 + x236 + x248 <= 1
c2545: x146 + x230 + x264 + x284 <= 1
c2546: x146 + x256 + x182 + x284 + x16 + x36 <= 1
c2547: x146 + x289 + x177 + x201 + x66 <= 1
c2548: x147 + x189 + x212 + x278 + x23 + x61 <= 1
c2549: x147 + x197 + x186 + x236 + x167 <= 1
c2550: x147 + x215 + x152 + x167 <= 1
c2551: x147 + x231 + x186 + x169 + x10 <= 1
c2552: x147 + x249 + x151 + x152 <= 1
c2553: x147 + x271 + x166 + x253 <= 1
c2554: x147 + x272 + x212 + x236 <= 1
c2555: x147 + x282 + x166 + x271 <= 1
c2556: x148 + x153 + x215 + x282 + x3 <= 1
c2557: x148 + x187 + x277 + x265 + x289 + x34 <= 1
c2558: x148 + x233 + x152 + x216 + x300 + x74 <= 1
c2559: x148 + x250 + x286 + x215 <= 1
c2560: x148 + x287 + x263 + x282 + x34 + x46 <= 1
c2561: x148 + x294 + x254 + x291 + x300 + x241 <= 1
c2562: x149 + x164 + x158 + x16 + x130 <= 1
c2563: x149 + x238 + x265 + x248 + x16 <= 1
c2564: x149 + x278 + x212 + x155 + x248 <= 1
c2565: x149 + x300 + x258 + x178 <= 1
c2566: x150 + x156 + x181 + x154 + x278 <= 1
c2567: x150 + x191 + x197 + x232 <= 1
c2568: x150 + x194 + x216 + x226 + x29 <= 1
c2569: x150 + x199 + x214 + x181 + x8 <= 1
c2570: x150 + x259 + x295 + x154 + x64 <= 1
c2571: x150 + x274 + x295 + x186 + x57 <= 1
c2572: x151 + x154 + x160 + x202 <= 1
c2573: x151 + x170 + x234 + x284 + x241 + x112 <= 1
c2574: x151 + x205 + x258 + x155 <= 1
c2575: x151 + x206 + x160 + x234 + x284 <= 1
c2576: x151 + x264 + x294 + x202 + x284 <= 1
c2577: x151 + x268 + x295 + x206 + x275 <= 1
c2578: x152 + x164 + x261 + x215 + x12 + x41 <= 1
c2579: x152 + x199 + x257 + x7 + x113 + x131 + x132 <= 1
c2580: x152 + x222 + x217 + x257 + x7 + x113 <= 1
c2581: x152 + x237 + x254 + x270 + x132 <= 1
c2582: x152 + x250 + x165 + x217 <= 1
c2583: x152 + x256 + x165 + x207 + x151 <= 1
c2584: x152 + x283 + x6 + x12 <= 1
c2585: x153 + x157 + x211 + x128 <= 1
c2586: x153 + x176 + x157 + x215 + x282 <= 1
c2587: x153 + x219 + x233 + x210 <= 1
c2588: x153 + x223 + x210 <= 1
c2589: x154 + x170 + x266 + x178 + x225 <= 1
c2590: x154 + x174 + x156 + x12 + x134 <= 1
c2591: x154 + x205 + x216 + x188 + x155 <= 1
c2592: x154 + x219 + x295 + x187 + x225 <= 1
c2593: x154 + x283 + x208 + x155 + x12 <= 1
c2594: x155 + x270 + x181 + x254 + x292 + x94 <= 1
c2595: x155 + x277 + x211 + x266 + x57 <= 1
c2596: x155 + x288 + x262 + x278 + x34 <= 1
c2597: x155 + x299 + x214 + x183 + x189 + x271 <= 1
c2598: x156 + x161 + x234 + x203 + x278 + x142 <= 1
c2599: x156 + x164 + x265 + x236 + x12 + x16 <= 1
c2600: x156 + x197 + x265 + x228 + x243 <= 1
c2601: x156 + x219 + x164 + x9 + x154 <= 1
c2602: x156 + x258 + x265 + x277 + x23 <= 1
c2603: x156 + x270 + x287 + x9 + x14 <= 1
c2604: x157 + x208 + x211 + x189 + x6 <= 1
c2605: x157 + x216 + x195 + x194 + x253 + x100 <= 1
c2606: x157 + x239 + x181 + x236 <= 1
c2607: x157 + x261 + x212 + x178 + x32 <= 1
c2608: x158 + x165 + x209 + x233 + x2 <= 1
c2609: x158 + x174 + x202 + x2 + x109 <= 1
c2610: x158 + x179 + x294 + x196 <= 1
c2611: x158 + x183 + x251 + x248 <= 1
c2612: x158 + x208 + x196 + x283 <= 1
c2613: x158 + x240 + x166 + x198 <= 1
c2614: x159 + x184 + x234 + x31 <= 1
c2615: x159 + x189 + x286 + x278 + x80 <= 1
c2616: x159 + x195 + x264 + x42 + x71 <= 1
c2617: x159 + x213 + x278 + x238 <= 1
c2618: x159 + x282 + x278 + x286 + x65 <= 1
c2619: x160 + x195 + x278 + x243 + x69 <= 1
c2620: x160 + x198 + x234 + x187 + x210 + x142 <= 1
c2621: x160 + x242 + x186 + x278 + x64 <= 1
c2622: x160 + x263 + x287 + x284 <= 1
c2623: x161 + x167 + x212 + x203 + x8 <= 1
c2624: x161 + x168 + x212 + x203 + x278 <= 1
c2625: x161 + x205 + x212 + x168 + x8 <= 1
c2626: x161 + x260 + x203 + x278 + x168 <= 1
c2627: x161 + x261 + x212 + x167 <= 1
c2628: x161 + x277 + x168 + x187 + x86 <= 1
c2629: x162 + x163 + x239 + x284 <= 1
c2630: x162 + x186 + x295 + x211 + x266 + x31 <= 1
c2631: x162 + x283 + x295 + x278 + x6 <= 1
c2632: x162 + x293 + x196 + x211 + x92 <= 1
c2633: x163 + x165 + x203 + x238 + x27 + x69 <= 1
c2634: x163 + x190 + x232 + x29 + x95 <= 1
c2635: x163 + x214 + x230 + x226 + x229 <= 1
c2636: x163 + x225 + x230 + x278 + x288 + x106 <= 1
c2637: x163 + x272 + x236 + x238 + x202 + x16 <= 1
c2638: x163 + x298 + x230 + x238 + x278 + x66 <= 1
c2639: x164 + x294 + x290 + x266 + x12 <= 1
c2640: x165 + x189 + x203 + x207 + x23 <= 1
c2641: x165 + x195 + x217 + x277 + x187 + x284 <= 1
c2642: x165 + x196 + x257 + x238 + x243 + x1 <= 1
c2643: x165 + x215 + x203 + x189 + x150 <= 1
c2644: x165 + x252 + x207 + x23 + x152 <= 1
c2645: x166 + x177 + x216 + x2 + x41 <= 1
c2646: x166 + x230 + x240 + x14 <= 1
c2647: x166 + x261 + x267 + x230 + x116 <= 1
c2648: x166 + x262 + x193 <= 1
c2649: x166 + x268 + x201 + x61 + x86 <= 1
c2650: x167 + x255 + x243 + x8 <= 1
c2651: x167 + x260 + x251 + x241 <= 1
c2652: x168 + x188 + x287 + x113 <= 1
c2653: x168 + x219 + x171 + x187 + x17 <= 1
c2654: x168 + x252 + x212 + x186 + x242 <= 1
c2655: x168 + x271 + x214 + x183 + x10 + x130 <= 1
c2656: x168 + x291 + x254 + x175 + x113 <= 1
c2657: x169 + x199 + x181 + x187 + x8 <= 1
c2658: x169 + x235 + x224 + x204 + x172 + x1 <= 1
c2659: x169 + x280 + x178 + x224 + x17 <= 1
c2660: x170 + x216 + x191 + x233 <= 1
c2661: x170 + x239 + x178 + x284 <= 1
c2662: x170 + x251 + x227 + x260 + x103 + x112 <= 1
c2663: x170 + x277 + x260 + x266 + x284 <= 1
c2664: x171 + x184 + x173 + x199 <= 1
c2665: x171 + x194 + x292 + x274 <= 1
c2666: x171 + x241 + x183 + x292 + x229 + x112 <= 1
c2667: x171 + x253 + x183 + x238 + x229 <= 1
c2668: x171 + x258 + x183 + x201 + x241 <= 1
c2669: x171 + x298 + x181 + x201 + x11 <= 1
c2670: x172 + x175 + x218 + x173 + x224 + x118 <= 1
c2671: x172 + x189 + x264 + x207 + x140 <= 1
c2672: x172 + x236 + x203 + x218 + x201 + x129 <= 1
c2673: x172 + x263 + x251 + x17 + x46 <= 1
c2674: x173 + x182 + x212 + x191 + x228 <= 1
c2675: x173 + x223 + x183 + x201 + x82 <= 1
c2676: x173 + x229 + x183 + x292 + x221 + x130 <= 1
c2677: x173 + x245 + x254 + x32 + x90 + x148 <= 1
c2678: x173 + x276 + x183 + x201 + x182 + x74 <= 1
c2679: x174 + x232 + x180 + x233 + x253 <= 1
c2680: x174 + x266 + x186 + x277 + x12 + x50 <= 1
c2681: x174 + x285 + x177 + x269 <= 1
c2682: x175 + x235 + x183 + x224 + x278 + x78 <= 1
c2683: x175 + x241 + x291 + x254 + x300 + x82 + x148 <= 1
c2684: x175 + x286 + x211 + x34 <= 1
c2685: x175 + x292 + x178 + x194 + x284 <= 1
c2686: x176 + x240 + x295 + x181 + x150 <= 1
c2687: x176 + x241 + x244 + x216 + x2 <= 1
c2688: x176 + x253 + x218 + x187 + x275 + x155 <= 1
c2689: x177 + x212 + x217 + x242 <= 1
c2690: x177 + x218 + x228 + x201 + x248 <= 1
c2691: x177 + x231 + x242 + x10 + x121 <= 1
c2692: x177 + x237 + x228 + x36 <= 1
c2693: x178 + x196 + x257 + x228 + x300 + x82 <= 1
c2694: x178 + x227 + x234 + x260 + x288 <= 1
c2695: x178 + x233 + x240 + x212 + x195 + x69 <= 1
c2696: x178 + x259 + x194 + x80 <= 1
c2697: x178 + x274 + x234 + x194 + x80 <= 1
c2698: x179 + x194 + x230 + x284 + x39 <= 1
c2699: x179 + x199 + x41 + x132 <= 1
c2700: x179 + x212 + x191 + x261 + x74 <= 1
c2701: x179 + x247 + x191 + x10 <= 1
c2702: x179 + x285 + x261 + x230 + x24 <= 1
c2703: x179 + x287 + x230 + x284 <= 1
c2704: x180 + x228 + x265 + x257 <= 1
c2705: x180 + x229 + x265 + x232 + x253 + x74 <= 1
c2706: x180 + x244 + x186 + x10 + x73 + x86 <= 1
c2707: x180 + x261 + x289 + x229 + x34 + x90 <= 1
c2708: x180 + x278 + x186 + x210 + x93 <= 1
c2709: x181 + x198 + x240 + x210 + x65 <= 1
c2710: x181 + x211 + x295 + x186 + x210 + x128 <= 1
c2711: x181 + x217 + x211 + x35 + x157 <= 1
c2712: x181 + x221 + x240 + x10 + x65 + x72 <= 1
c2713: x181 + x222 + x214 + x63 <= 1
c2714: x181 + x293 + x201 + x211 + x196 + x72 <= 1
c2715: x182 + x205 + x183 + x276 <= 1
c2716: x182 + x211 + x286 + x276 + x201 <= 1
c2717: x182 + x214 + x251 + x264 <= 1
c2718: x182 + x288 + x238 + x244 + x276 <= 1
c2719: x183 + x230 + x214 + x261 + x229 <= 1
c2720: x183 + x237 + x206 + x241 + x2 <= 1
c2721: x183 + x255 + x257 + x243 + x278 <= 1
c2722: x184 + x226 + x203 + x282 + x65 + x82 <= 1
c2723: x184 + x242 + x186 + x212 + x31 + x173 <= 1
c2724: x184 + x289 + x265 + x224 + x199 + x67 <= 1
c2725: x185 + x197 + x186 + x191 <= 1
c2726: x185 + x200 + x258 + x69 + x127 + x129 <= 1
c2727: x185 + x227 + x197 + x242 + x16 <= 1
c2728: x185 + x264 + x249 + x222 <= 1
c2729: x186 + x260 + x214 + x264 <= 1
c2730: x186 + x268 + x295 + x10 + x12 + x86 <= 1
c2731: x186 + x269 + x295 + x246 + x50 <= 1
c2732: x186 + x291 + x207 + x15 + x53 + x157 <= 1
c2733: x187 + x191 + x295 + x249 + x210 <= 1
c2734: x187 + x209 + x249 + x234 + x233 <= 1
c2735: x187 + x297 + x295 + x210 + x230 + x64 <= 1
c2736: x188 + x192 + x224 + x300 + x85 <= 1
c2737: x188 + x204 + x216 + x224 + x300 <= 1
c2738: x188 + x217 + x203 + x238 + x250 <= 1
c2739: x189 + x292 + x202 + x203 + x69 + x72 <= 1
c2740: x190 + x208 + x216 + x69 + x136 + x157 <= 1
c2741: x190 + x264 + x249 + x284 + x187 <= 1
c2742: x191 + x296 + x249 + x238 + x241 <= 1
c2743: x191 + x298 + x238 + x224 + x74 + x172 <= 1
c2744: x192 + x226 + x198 + x65 <= 1
c2745: x192 + x232 + x267 + x66 + x74 <= 1
c2746: x192 + x263 + x279 + x229 + x69 <= 1
c2747: x193 + x207 + x234 + x242 + x21 <= 1
c2748: x193 + x219 + x233 + x210 + x74 <= 1
c2749: x193 + x283 + x234 + x12 <= 1
c2750: x194 + x220 + x245 + x238 + x228 <= 1
c2751: x194 + x221 + x195 + x216 + x253 <= 1
c2752: x194 + x280 + x265 + x281 + x289 <= 1
c2753: x195 + x270 + x243 + x233 + x1 + x69 <= 1
c2754: x195 + x272 + x243 + x216 + x78 <= 1
c2755: x195 + x299 + x270 + x233 <= 1
c2756: x196 + x210 + x294 + x257 + x132 <= 1
c2757: x197 + x206 + x214 + x4 + x16 <= 1
c2758: x197 + x253 + x265 + x228 + x194 <= 1
c2759: x197 + x257 + x265 + x228 + x243 <= 1
c2760: x197 + x273 + x265 + x8 + x92 <= 1
c2761: x198 + x246 + x281 + x234 + x288 <= 1
c2762: x198 + x290 + x279 + x243 + x92 <= 1
c2763: x199 + x200 + x241 + x64 + x88 <= 1
c2764: x199 + x203 + x236 + x207 + x23 <= 1
c2765: x199 + x209 + x243 + x257 <= 1
c2766: x200 + x244 + x241 + x62 <= 1
c2767: x200 + x259 + x241 + x64 + x97 <= 1
c2768: x200 + x273 + x212 + x284 + x91 + x112 <= 1
c2769: x201 + x215 + x286 + x229 + x34 <= 1
c2770: x201 + x256 + x249 + x207 + x258 + x169 <= 1
c2771: x201 + x290 + x286 + x183 <= 1
c2772: x202 + x224 + x254 + x294 + x12 + x148 <= 1
c2773: x202 + x267 + x204 + x230 + x116 <= 1
c2774: x202 + x295 + x265 + x238 + x243 + x224 + x2 <= 1
c2775: x203 + x271 + x232 + x47 <= 1
c2776: x203 + x291 + x207 + x275 + x53 <= 1
c2777: x204 + x231 + x251 + x279 <= 1
c2778: x204 + x233 + x249 + x243 + x288 + x178 <= 1
c2779: x204 + x292 + x251 + x248 <= 1
c2780: x205 + x236 + x265 + x212 + x248 <= 1
c2781: x206 + x209 + x234 + x257 <= 1
c2782: x206 + x254 + x237 + x282 + x241 + x15 <= 1
c2783: x207 + x214 + x234 + x229 + x39 <= 1
c2784: x207 + x220 + x217 + x36 <= 1
c2785: x207 + x276 + x237 + x15 + x157 <= 1
c2786: x208 + x221 + x211 + x253 <= 1
c2787: x208 + x236 + x246 + x238 + x57 <= 1
c2788: x209 + x256 + x249 + x229 <= 1
c2789: x209 + x261 + x229 + x230 + x34 + x90 <= 1
c2790: x209 + x278 + x286 + x34 <= 1
c2791: x210 + x275 + x263 + x211 + x8 <= 1
c2792: x211 + x251 + x295 + x266 <= 1
c2793: x211 + x300 + x277 + x224 + x6 <= 1
c2794: x212 + x246 + x222 + x265 + x236 <= 1
c2795: x212 + x289 + x240 + x252 + x72 <= 1
c2796: x213 + x216 + x294 + x224 + x1 + x69 <= 1
c2797: x213 + x263 + x284 + x46 + x69 + x120 <= 1
c2798: x214 + x232 + x267 + x271 <= 1
c2799: x214 + x243 + x279 + x1 + x65 + x132 <= 1
c2800: x214 + x247 + x10 + x61 + x186 <= 1
c2801: x214 + x268 + x10 + x61 + x186 <= 1
c2802: x215 + x228 + x248 + x8 + x157 <= 1
c2803: x215 + x287 + x229 + x34 + x53 <= 1
c2804: x216 + x293 + x272 + x14 <= 1
c2805: x217 + x241 + x273 + x284 + x112 + x157 <= 1
c2806: x217 + x260 + x277 + x279 + x284 <= 1
c2807: x217 + x286 + x238 + x250 <= 1
c2808: x218 + x235 + x224 + x278 + x1 + x172 + x175 <= 1
c2809: x218 + x297 + x220 + x224 <= 1
c2810: x218 + x299 + x270 + x248 + x257 + x51 <= 1
c2811: x219 + x237 + x276 + x78 <= 1
c2812: x221 + x251 + x222 + x238 + x253 + x17 <= 1
c2813: x222 + x230 + x249 + x295 + x238 <= 1
c2814: x222 + x244 + x236 + x238 + x167 <= 1
c2815: x222 + x274 + x295 + x12 <= 1
c2816: x223 + x263 + x288 + x260 + x69 <= 1
c2817: x223 + x295 + x249 + x31 + x99 <= 1
c2818: x224 + x258 + x265 + x277 + x23 <= 1
c2819: x225 + x244 + x285 + x231 + x116 <= 1
c2820: x226 + x233 + x249 + x14 + x44 + x187 <= 1
c2821: x226 + x259 + x291 + x41 <= 1
c2822: x227 + x271 + x258 + x282 + x46 + x185 <= 1
c2823: x227 + x290 + x279 + x64 <= 1
c2824: x228 + x249 + x258 + x16 + x69 + x178 <= 1
c2825: x228 + x272 + x248 + x238 + x257 + x64 <= 1
c2826: x229 + x272 + x262 + x295 + x234 + x36 <= 1
c2827: x231 + x283 + x285 <= 1
c2828: x232 + x262 + x271 + x17 + x55 <= 1
c2829: x233 + x280 + x246 + x69 <= 1
c2830: x234 + x265 + x246 + x281 + x288 <= 1
c2831: x234 + x290 + x274 + x295 + x12 <= 1
c2832: x236 + x245 + x287 <= 1
c2833: x236 + x277 + x249 + x266 + x50 <= 1
c2834: x237 + x246 + x282 + x203 <= 1
c2835: x237 + x266 + x282 + x31 <= 1
c2836: x238 + x268 + x296 + x108 <= 1
c2837: x239 + x250 + x248 + x202 <= 1
c2838: x239 + x254 + x270 + x169 + x181 <= 1
c2839: x239 + x262 + x270 + x65 <= 1
c2840: x239 + x271 + x262 <= 1
c2841: x239 + x291 + x254 + x61 <= 1
c2842: x240 + x254 + x294 + x31 + x41 <= 1
c2843: x240 + x285 + x252 + x258 + x69 <= 1
c2844: x240 + x286 + x252 + x282 + x72 <= 1
c2845: x242 + x257 + x247 + x248 + x64 <= 1
c2846: x243 + x246 + x265 + x288 + x12 + x121 <= 1
c2847: x245 + x261 + x267 + x6 + x152 <= 1
c2848: x246 + x262 + x278 + x288 + x234 <= 1
c2849: x247 + x270 + x248 + x9 + x257 <= 1
c2850: x247 + x281 + x9 + x118 + x300 <= 1
c2851: x248 + x252 + x258 + x282 + x148 <= 1
c2852: x249 + x294 + x284 + x6 + x151 <= 1
c2853: x250 + x281 + x265 + x292 + x148 <= 1
c2854: x253 + x291 + x275 + x81 + x114 + x229 <= 1
c2855: x254 + x255 + x270 + x93 <= 1
c2856: x254 + x275 + x291 + x41 + x81 + x132 <= 1
c2857: x254 + x280 + x294 + x12 + x224 <= 1
c2858: x255 + x276 + x294 + x2 + x41 <= 1
c2859: x258 + x293 + x16 + x72 + x82 <= 1
c2860: x259 + x298 + x12 + x248 <= 1
c2861: x261 + x281 + x16 + x25 + x34 + x289 <= 1
c2862: x265 + x285 + x2 + x14 + x94 + x164 <= 1
c2863: x267 + x273 + x8 + x46 + x141 <= 1
c2864: x267 + x274 + x15 + x77 <= 1
c2865: x267 + x294 + x6 + x66 <= 1
c2866: x270 + x279 + x284 + x6 + x46 + x93 + x210 <= 1
c2867: x272 + x297 + x295 + x11 + x64 + x210 <= 1
c2868: x273 + x280 + x287 + x51 <= 1
c2869: x274 + x298 + x12 + x143 + x186 <= 1
c2870: x275 + x288 + x278 + x12 + x34 + x155 + x207 <= 1
c2871: x277 + x296 + x18 + x53 <= 1
c2872: x278 + x279 + x1 + x65 + x94 <= 1
c2873: x279 + x291 + x1 + x62 + x69 + x86 <= 1
c2874: x280 + x290 + x2 + x69 + x294 <= 1
c2875: x282 + x296 + x287 + x1 <= 1
c2876: x283 + x286 + x6 + x17 + x278 <= 1
c2877: x284 + x290 + x2 + x68 + x195 <= 1
c2878: x287 + x295 + x9 + x64 <= 1
c2879: x291 + x299 + x41 + x61 <= 1
END