c cnf generated by mark.reason.apps.PlgToDimacs written by Mark Chavira
c cnf generated on Wed Nov 17 12:34:35 PST 2004.
c
c Following is the map back to variable name:
c
c 1 X_1_101_input
c 2 X_4_104_input
c 3 X_7_107_input
c 4 X_10_110_input
c 5 X_13_113_input
c 6 X_16_116_input
c 7 X_19_119_input
c 8 X_22_122_input
c 9 X_25_125_input
c 10 X_28_128_input
c 11 X_31_131_input
c 12 X_34_134_input
c 13 X_37_137_input
c 14 X_40_140_input
c 15 X_43_143_input
c 16 X_46_146_input
c 17 X_49_210_input
c 18 X_53_214_input
c 19 X_56_217_input
c 20 X_60_221_input
c 21 X_63_224_input
c 22 X_66_227_input
c 23 X_69_234_input
c 24 X_72_237_input
c 25 X_76_469_input
c 26 X_79_472_input
c 27 X_82_475_input
c 28 X_85_478_input
c 29 X_88_898_input
c 30 X_91_900_input
c 31 X_94_902_input
c 32 X_99_952_input
c 33 X_104_953_input
c 34 X_190_149_internal
c 35 X_194_153_internal
c 36 X_197_156_internal
c 37 X_201_160_internal
c 38 X_206_165_internal
c 39 X_209_168_internal
c 40 X_212_171_internal
c 41 X_216_175_internal
c 42 X_220_179_internal
c 43 X_225_184_internal
c 44 X_229_188_internal
c 45 X_232_191_internal
c 46 X_235_194_internal
c 47 X_239_198_internal
c 48 X_243_202_internal
c 49 X_247_206_internal
c 50 X_251_231_internal
c 51 X_252_233_internal
c 52 X_253_241_internal
c 53 X_256_244_internal
c 54 X_263_517_internal
c 55 X_266_529_internal
c 56 X_269_541_internal
c 57 X_272_553_internal
c 58 X_275_859_internal
c 59 X_276_862_internal
c 60 X_277_907_internal
c 61 X_280_909_internal
c 62 X_290_918_internal
c 63 X_300_922_internal
c 64 X_306_930_internal
c 65 X_313_932_internal
c 66 X_319_938_internal
c 67 X_338_949_internal
c 68 X_534_1512_internal
c 69 X_535_1520_internal
c 70 X_536_1528_internal
c 71 X_537_1536_internal
c 72 X_538_1544_internal
c 73 X_539_1552_internal
c 74 X_540_1560_internal
c 75 X_541_1568_internal
c 76 X_542_1576_internal
c 77 X_543_1584_internal
c 78 X_544_1592_internal
c 79 X_545_1600_internal
c 80 X_546_1608_internal
c 81 X_547_1616_internal
c 82 X_548_1624_internal
c 83 X_549_1632_internal
c 84 X_550_50_internal
c 85 X_551_52_internal
c 86 X_552_56_internal
c 87 X_553_58_internal
c 88 X_554_62_internal
c 89 X_555_64_internal
c 90 X_574_318_internal
c 91 X_586_352_internal
c 92 X_592_369_internal
c 93 X_601_853_internal
c 94 X_602_856_internal
c 95 X_603_893_internal
c 96 X_608_954_internal
c 97 X_612_955_internal
c 98 X_643_1290_internal
c 99 X_655_1335_internal
c 100 X_682_1634_internal
c 101 X_685_1644_internal
c 102 X_724_1830_internal
c 103 X_886_1642_internal
c 104 X_887_1652_internal
c 105 X_888_1056_internal
c 106 X_889_1057_internal
c 107 X_890_1182_internal
c 108 X_891_1183_internal
c 109 X_892_1211_internal
c 110 X_893_1298_internal
c 111 X_894_1320_internal
c 112 X_895_1338_internal
c 113 X_896_1339_internal
c 114 X_897_457_internal
c 115 X_898_459_internal
c 116 X_899_482_internal
c 117 X_903_487_internal
c 118 X_907_492_internal
c 119 X_910_505_internal
c 120 X_913_1456_internal
c 121 X_914_1448_internal
c 122 X_915_1472_internal
c 123 X_916_1464_internal
c 124 X_917_1488_internal
c 125 X_918_1480_internal
c 126 X_919_1504_internal
c 127 X_920_1496_internal
c 128 X_921_956_internal
c 129 X_922_967_internal
c 130 X_923_978_internal
c 131 X_926_979_internal
c 132 X_938_1661_internal
c 133 X_942_1669_internal
c 134 X_946_1701_internal
c 135 X_950_1709_internal
c 136 X_954_1717_internal
c 137 X_958_1725_internal
c 138 X_968_1749_internal
c 139 X_972_1757_internal
c 140 X_976_1789_internal
c 141 X_980_1797_internal
c 142 X_984_1201_internal
c 143 X_988_1820_internal
c 144 X_989_1821_internal
c 145 X_990_1230_internal
c 146 X_991_1836_internal
c 147 X_992_1837_internal
c 148 X_993_1252_internal
c 149 X_997_1845_internal
c 150 X_1001_1853_internal
c 151 X_1002_1860_internal
c 152 X_1003_1861_internal
c 153 X_1004_1286_internal
c 154 X_1005_1876_internal
c 155 X_1006_1877_internal
c 156 X_1007_1308_internal
c 157 X_1008_1884_internal
c 158 X_1009_1885_internal
c 159 X_1054_297_internal
c 160 X_1055_298_internal
c 161 X_1063_361_internal
c 162 X_1064_362_internal
c 163 X_1067_404_internal
c 164 X_1068_405_internal
c 165 X_1119_1225_internal
c 166 X_1120_1226_internal
c 167 X_1121_1247_internal
c 168 X_1122_1248_internal
c 169 X_1128_1281_internal
c 170 X_1129_1282_internal
c 171 X_1130_1303_internal
c 172 X_1131_1304_internal
c 173 X_1132_1315_internal
c 174 X_1133_1316_internal
c 175 X_1148_998_internal
c 176 X_1149_988_internal
c 177 X_1150_268_internal
c 178 X_1151_1038_internal
c 179 X_1152_1048_internal
c 180 X_1153_1076_internal
c 181 X_1154_1066_internal
c 182 X_1155_1098_internal
c 183 X_1156_1120_internal
c 184 X_1157_1174_internal
c 185 X_1158_363_internal
c 186 X_1159_1210_internal
c 187 X_1160_373_internal
c 188 X_1161_1276_internal
c 189 X_1162_406_internal
c 190 X_1163_565_internal
c 191 X_1167_614_internal
c 192 X_1171_958_internal
c 193 X_1188_969_internal
c 194 X_1205_1660_internal
c 195 X_1206_984_internal
c 196 X_1207_1668_internal
c 197 X_1208_994_internal
c 198 X_1209_1700_internal
c 199 X_1210_1034_internal
c 200 X_1211_1708_internal
c 201 X_1212_1044_internal
c 202 X_1213_1716_internal
c 203 X_1214_1062_internal
c 204 X_1215_1724_internal
c 205 X_1216_1072_internal
c 206 X_1217_1732_internal
c 207 X_1218_1086_internal
c 208 X_1219_1740_internal
c 209 X_1220_1748_internal
c 210 X_1221_1104_internal
c 211 X_1222_1108_internal
c 212 X_1223_1756_internal
c 213 X_1224_1116_internal
c 214 X_1225_1788_internal
c 215 X_1226_1158_internal
c 216 X_1227_1162_internal
c 217 X_1228_1796_internal
c 218 X_1229_1170_internal
c 219 X_1230_1200_internal
c 220 X_1231_1203_internal
c 221 X_1232_1227_internal
c 222 X_1235_1249_internal
c 223 X_1238_1844_internal
c 224 X_1239_1260_internal
c 225 X_1240_1264_internal
c 226 X_1241_1852_internal
c 227 X_1242_1272_internal
c 228 X_1243_1283_internal
c 229 X_1246_1305_internal
c 230 X_1249_1317_internal
c 231 X_1264_269_internal
c 232 X_1267_372_internal
c 233 X_1309_983_internal
c 234 X_1310_993_internal
c 235 X_1311_1033_internal
c 236 X_1312_1043_internal
c 237 X_1313_1061_internal
c 238 X_1314_1071_internal
c 239 X_1315_1103_internal
c 240 X_1316_1115_internal
c 241 X_1317_1157_internal
c 242 X_1318_1169_internal
c 243 X_1319_1184_internal
c 244 X_1322_1202_internal
c 245 X_1327_1259_internal
c 246 X_1328_1271_internal
c 247 X_1334_1322_internal
c 248 X_1344_374_internal
c 249 X_1345_396_internal
c 250 X_1346_1321_internal
c 251 X_1348_1424_internal
c 252 X_1349_1416_internal
c 253 X_1350_1440_internal
c 254 X_1351_1432_internal
c 255 X_1352_985_internal
c 256 X_1355_995_internal
c 257 X_1358_1035_internal
c 258 X_1361_1045_internal
c 259 X_1364_1063_internal
c 260 X_1367_1073_internal
c 261 X_1370_1105_internal
c 262 X_1373_1117_internal
c 263 X_1376_1159_internal
c 264 X_1379_1171_internal
c 265 X_1383_1212_internal
c 266 X_1386_1231_internal
c 267 X_1387_1232_internal
c 268 X_1388_1253_internal
c 269 X_1389_1254_internal
c 270 X_1390_1261_internal
c 271 X_1393_1273_internal
c 272 X_1396_1287_internal
c 273 X_1397_1288_internal
c 274 X_1398_1309_internal
c 275 X_1399_1310_internal
c 276 X_1409_1192_internal
c 277 X_1412_397_internal
c 278 X_1413_1330_internal
c 279 X_1433_1233_internal
c 280 X_1434_1255_internal
c 281 X_1438_1289_internal
c 282 X_1439_1311_internal
c 283 X_1440_1381_internal
c 284 X_1443_257_internal
c 285 X_1444_999_internal
c 286 X_1445_260_internal
c 287 X_1446_989_internal
c 288 X_1447_272_internal
c 289 X_1448_1039_internal
c 290 X_1451_294_internal
c 291 X_1452_1049_internal
c 292 X_1453_305_internal
c 293 X_1454_1077_internal
c 294 X_1455_308_internal
c 295 X_1456_1067_internal
c 296 X_1457_333_internal
c 297 X_1458_1121_internal
c 298 X_1459_358_internal
c 299 X_1460_1175_internal
c 300 X_1461_1220_internal
c 301 X_1462_388_internal
c 302 X_1463_1277_internal
c 303 X_1464_398_internal
c 304 X_1468_1109_internal
c 305 X_1469_1110_internal
c 306 X_1470_1163_internal
c 307 X_1471_1164_internal
c 308 X_1472_1234_internal
c 309 X_1475_1265_internal
c 310 X_1476_1266_internal
c 311 X_1478_1822_internal
c 312 X_1481_1862_internal
c 313 X_1484_1865_internal
c 314 X_1487_258_internal
c 315 X_1488_261_internal
c 316 X_1489_273_internal
c 317 X_1490_1018_internal
c 318 X_1491_1008_internal
c 319 X_1492_295_internal
c 320 X_1493_306_internal
c 321 X_1494_309_internal
c 322 X_1495_334_internal
c 323 X_1496_359_internal
c 324 X_1498_389_internal
c 325 X_1499_1385_internal
c 326 X_1500_1111_internal
c 327 X_1501_1165_internal
c 328 X_1504_1267_internal
c 329 X_1510_1886_internal
c 330 X_1513_259_internal
c 331 X_1514_262_internal
c 332 X_1517_274_internal
c 333 X_1520_296_internal
c 334 X_1521_307_internal
c 335 X_1522_310_internal
c 336 X_1526_335_internal
c 337 X_1527_360_internal
c 338 X_1528_1242_internal
c 339 X_1529_390_internal
c 340 X_1530_1828_internal
c 341 X_1531_1868_internal
c 342 X_1532_1869_internal
c 343 X_1534_1373_internal
c 344 X_1537_1798_internal
c 345 X_1540_1825_internal
c 346 X_1546_265_internal
c 347 X_1554_314_internal
c 348 X_1557_336_internal
c 349 X_1561_407_internal
c 350 X_1567_1293_internal
c 351 X_1568_1294_internal
c 352 X_1569_1892_internal
c 353 X_1571_1777_internal
c 354 X_1576_1889_internal
c 355 X_1591_1377_internal
c 356 X_1593_1804_internal
c 357 X_1594_1237_internal
c 358 X_1595_1829_internal
c 359 X_1596_1295_internal
c 360 X_1635_1781_internal
c 361 X_1636_1238_internal
c 362 X_1638_1325_internal
c 363 X_1639_1893_internal
c 364 X_1671_391_internal
c 365 X_1672_1299_internal
c 366 X_1675_1676_internal
c 367 X_1677_1684_internal
c 368 X_1678_1081_internal
c 369 X_1679_1733_internal
c 370 X_1680_1093_internal
c 371 X_1681_1741_internal
c 372 X_1682_1765_internal
c 373 X_1683_1773_internal
c 374 X_1685_1239_internal
c 375 X_1688_1326_internal
c 376 X_1706_392_internal
c 377 X_1707_1360_internal
c 378 X_1708_1003_internal
c 379 X_1709_1677_internal
c 380 X_1710_1013_internal
c 381 X_1711_1685_internal
c 382 X_1712_1082_internal
c 383 X_1713_1094_internal
c 384 X_1720_1187_internal
c 385 X_1721_1805_internal
c 386 X_1723_1327_internal
c 387 X_1727_1901_internal
c 388 X_1728_1348_internal
c 389 X_1730_1909_internal
c 390 X_1740_377_internal
c 391 X_1741_1243_internal
c 392 X_1742_393_internal
c 393 X_1746_1004_internal
c 394 X_1747_1014_internal
c 395 X_1748_1083_internal
c 396 X_1751_1095_internal
c 397 X_1759_1188_internal
c 398 X_1761_1900_internal
c 399 X_1762_1344_internal
c 400 X_1763_1908_internal
c 401 X_1764_1356_internal
c 402 X_1768_1142_internal
c 403 X_1769_378_internal
c 404 X_1772_399_internal
c 405 X_1773_1331_internal
c 406 X_1774_1005_internal
c 407 X_1777_1015_internal
c 408 X_1783_1764_internal
c 409 X_1784_1126_internal
c 410 X_1785_1130_internal
c 411 X_1786_1772_internal
c 412 X_1787_1138_internal
c 413 X_1788_1189_internal
c 414 X_1791_1343_internal
c 415 X_1792_1355_internal
c 416 X_1795_324_internal
c 417 X_1796_1099_internal
c 418 X_1798_379_internal
c 419 X_1801_400_internal
c 420 X_1802_449_internal
c 421 X_1807_1087_internal
c 422 X_1808_1088_internal
c 423 X_1809_1125_internal
c 424 X_1810_1137_internal
c 425 X_1812_1345_internal
c 426 X_1815_1357_internal
c 427 X_1821_277_internal
c 428 X_1822_1019_internal
c 429 X_1823_280_internal
c 430 X_1824_1009_internal
c 431 X_1825_325_internal
c 432 X_1826_364_internal
c 433 X_1827_1193_internal
c 434 X_1830_401_internal
c 435 X_1837_1089_internal
c 436 X_1838_1127_internal
c 437 X_1841_1139_internal
c 438 X_1848_278_internal
c 439 X_1849_281_internal
c 440 X_1850_326_internal
c 441 X_1852_365_internal
c 442 X_1855_413_internal
c 443 X_1856_1361_internal
c 444 X_1857_1401_internal
c 445 X_1858_445_internal
c 446 X_1864_1349_internal
c 447 X_1865_1350_internal
c 448 X_1875_1689_internal
c 449 X_1878_279_internal
c 450 X_1879_282_internal
c 451 X_1882_346_internal
c 452 X_1883_1143_internal
c 453 X_1884_366_internal
c 454 X_1885_414_internal
c 455 X_1889_453_internal
c 456 X_1895_1131_internal
c 457 X_1896_1132_internal
c 458 X_1897_1351_internal
c 459 X_1898_1365_internal
c 460 X_1910_285_internal
c 461 X_1911_347_internal
c 462 X_1912_367_internal
c 463 X_1913_415_internal
c 464 X_1915_1393_internal
c 465 X_1919_556_internal
c 466 X_1920_1505_internal
c 467 X_1921_559_internal
c 468 X_1922_1497_internal
c 469 X_1923_1693_internal
c 470 X_1924_1133_internal
c 471 X_1933_1809_internal
c 472 X_1936_348_internal
c 473 X_1937_1369_internal
c 474 X_1938_1409_internal
c 475 X_1941_557_internal
c 476 X_1942_560_internal
c 477 X_1947_1378_internal
c 478 X_1961_1774_internal
c 479 X_1965_1910_internal
c 480 X_1968_1918_internal
c 481 X_1975_544_internal
c 482 X_1976_1489_internal
c 483 X_1977_547_internal
c 484 X_1978_1481_internal
c 485 X_1979_558_internal
c 486 X_1980_561_internal
c 487 X_1985_1813_internal
c 488 X_1987_1370_internal
c 489 X_1999_1368_internal
c 490 X_2000_417_internal
c 491 X_2002_1384_internal
c 492 X_2003_424_internal
c 493 X_2004_508_internal
c 494 X_2005_1441_internal
c 495 X_2006_511_internal
c 496 X_2007_1433_internal
c 497 X_2008_545_internal
c 498 X_2009_548_internal
c 499 X_2012_564_internal
c 500 X_2013_1692_internal
c 501 X_2014_1024_internal
c 502 X_2015_1780_internal
c 503 X_2016_1148_internal
c 504 X_2018_1916_internal
c 505 X_2019_1924_internal
c 506 X_2020_416_internal
c 507 X_2021_1376_internal
c 508 X_2022_421_internal
c 509 X_2023_423_internal
c 510 X_2024_509_internal
c 511 X_2025_512_internal
c 512 X_2026_546_internal
c 513 X_2027_549_internal
c 514 X_2030_719_internal
c 515 X_2036_1023_internal
c 516 X_2037_1147_internal
c 517 X_2038_418_internal
c 518 X_2039_420_internal
c 519 X_2040_425_internal
c 520 X_2041_510_internal
c 521 X_2042_513_internal
c 522 X_2047_552_internal
c 523 X_2052_1025_internal
c 524 X_2055_1149_internal
c 525 X_2060_419_internal
c 526 X_2061_422_internal
c 527 X_2062_441_internal
c 528 X_2067_516_internal
c 529 X_2068_725_internal
c 530 X_2076_1029_internal
c 531 X_2077_1153_internal
c 532 X_2078_433_internal
c 533 X_2081_437_internal
c 534 X_2086_663_internal
c 535 X_2104_731_internal
c 536 X_2119_746_internal
c 537 X_2129_756_internal
c 538 X_2143_770_internal
c 539 X_2214_532_internal
c 540 X_2215_1473_internal
c 541 X_2216_535_internal
c 542 X_2217_1465_internal
c 543 X_2222_495_internal
c 544 X_2223_1425_internal
c 545 X_2224_498_internal
c 546 X_2225_1417_internal
c 547 X_2226_520_internal
c 548 X_2227_1457_internal
c 549 X_2228_523_internal
c 550 X_2229_1449_internal
c 551 X_2230_533_internal
c 552 X_2231_536_internal
c 553 X_2232_496_internal
c 554 X_2233_499_internal
c 555 X_2234_521_internal
c 556 X_2235_524_internal
c 557 X_2236_534_internal
c 558 X_2237_537_internal
c 559 X_2240_497_internal
c 560 X_2241_500_internal
c 561 X_2244_522_internal
c 562 X_2245_525_internal
c 563 X_2250_540_internal
c 564 X_2253_503_internal
c 565 X_2256_528_internal
c 566 X_2257_669_internal
c 567 X_2263_569_internal
c 568 X_2266_588_internal
c 569 X_2269_618_internal
c 570 X_2272_639_internal
c 571 X_2279_867_internal
c 572 X_2340_675_internal
c 573 X_2353_688_internal
c 574 X_2361_696_internal
c 575 X_2375_710_internal
c 576 X_2384_73_internal
c 577 X_2385_572_internal
c 578 X_2386_573_internal
c 579 X_2426_621_internal
c 580 X_2427_622_internal
c 581 X_2537_776_internal
c 582 X_2540_780_internal
c 583 X_2543_784_internal
c 584 X_2546_788_internal
c 585 X_2549_812_internal
c 586 X_2552_832_internal
c 587 X_2555_836_internal
c 588 X_2558_1509_internal
c 589 X_2561_1517_internal
c 590 X_2564_1525_internal
c 591 X_2567_1533_internal
c 592 X_2570_1581_internal
c 593 X_2573_1621_internal
c 594 X_2576_1629_internal
c 595 X_2594_792_internal
c 596 X_2597_796_internal
c 597 X_2600_800_internal
c 598 X_2603_804_internal
c 599 X_2606_808_internal
c 600 X_2611_816_internal
c 601 X_2614_820_internal
c 602 X_2617_824_internal
c 603 X_2620_828_internal
c 604 X_2627_871_internal
c 605 X_2628_873_internal
c 606 X_2629_875_internal
c 607 X_2630_877_internal
c 608 X_2631_879_internal
c 609 X_2632_881_internal
c 610 X_2633_883_internal
c 611 X_2634_885_internal
c 612 X_2639_1541_internal
c 613 X_2642_1549_internal
c 614 X_2645_1557_internal
c 615 X_2648_1565_internal
c 616 X_2651_1573_internal
c 617 X_2655_1589_internal
c 618 X_2658_1597_internal
c 619 X_2661_1605_internal
c 620 X_2664_1613_internal
c 621 X_2669_1_internal
c 622 X_2670_1513_internal
c 623 X_2671_4_internal
c 624 X_2672_1521_internal
c 625 X_2673_7_internal
c 626 X_2674_1529_internal
c 627 X_2675_10_internal
c 628 X_2676_1537_internal
c 629 X_2682_28_internal
c 630 X_2683_1585_internal
c 631 X_2688_43_internal
c 632 X_2689_1625_internal
c 633 X_2690_46_internal
c 634 X_2691_1633_internal
c 635 X_2710_886_internal
c 636 X_2720_2_internal
c 637 X_2721_5_internal
c 638 X_2722_8_internal
c 639 X_2723_11_internal
c 640 X_2724_13_internal
c 641 X_2725_1545_internal
c 642 X_2726_16_internal
c 643 X_2727_1553_internal
c 644 X_2728_19_internal
c 645 X_2729_1561_internal
c 646 X_2730_22_internal
c 647 X_2731_1569_internal
c 648 X_2732_25_internal
c 649 X_2733_1577_internal
c 650 X_2734_29_internal
c 651 X_2735_31_internal
c 652 X_2736_1593_internal
c 653 X_2737_34_internal
c 654 X_2738_1601_internal
c 655 X_2739_37_internal
c 656 X_2740_1609_internal
c 657 X_2741_40_internal
c 658 X_2742_1617_internal
c 659 X_2743_44_internal
c 660 X_2744_47_internal
c 661 X_2745_857_internal
c 662 X_2746_860_internal
c 663 X_2747_863_internal
c 664 X_2750_865_internal
c 665 X_2753_3_output
c 666 X_2754_6_output
c 667 X_2755_9_output
c 668 X_2756_12_output
c 669 X_2757_14_internal
c 670 X_2758_17_internal
c 671 X_2759_20_internal
c 672 X_2760_23_internal
c 673 X_2761_26_internal
c 674 X_2762_30_output
c 675 X_2763_32_internal
c 676 X_2764_35_internal
c 677 X_2765_38_internal
c 678 X_2766_41_internal
c 679 X_2767_45_output
c 680 X_2768_48_output
c 681 X_2773_1913_internal
c 682 X_2776_1921_internal
c 683 X_2779_15_output
c 684 X_2780_18_output
c 685 X_2781_21_output
c 686 X_2782_24_output
c 687 X_2783_27_output
c 688 X_2784_33_output
c 689 X_2785_36_output
c 690 X_2786_39_output
c 691 X_2787_42_output
c 692 X_2788_887_internal
c 693 X_2789_462_internal
c 694 X_2800_74_internal
c 695 X_2807_1637_internal
c 696 X_2808_1917_internal
c 697 X_2809_1647_internal
c 698 X_2810_1925_internal
c 699 X_2811_75_output
c 700 X_2812_1020_internal
c 701 X_2815_1144_internal
c 702 X_2818_1386_internal
c 703 X_2821_1394_internal
c 704 X_2824_1402_internal
c 705 X_2827_1638_internal
c 706 X_2828_1648_internal
c 707 X_2829_1806_internal
c 708 X_2843_1639_internal
c 709 X_2846_1649_internal
c 710 X_2850_287_internal
c 711 X_2851_350_internal
c 712 X_2852_427_internal
c 713 X_2853_429_internal
c 714 X_2854_431_internal
c 715 X_2857_1028_internal
c 716 X_2858_1152_internal
c 717 X_2859_1392_internal
c 718 X_2860_1400_internal
c 719 X_2861_1408_internal
c 720 X_2862_1812_internal
c 721 X_2863_1216_internal
c 722 X_2866_286_internal
c 723 X_2867_349_internal
c 724 X_2868_426_internal
c 725 X_2869_428_internal
c 726 X_2870_430_internal
c 727 X_2871_67_internal
c 728 X_2872_1643_internal
c 729 X_2873_70_internal
c 730 X_2874_1653_internal
c 731 X_2875_1215_internal
c 732 X_2876_49_internal
c 733 X_2877_53_internal
c 734 X_2878_59_internal
c 735 X_2879_61_internal
c 736 X_2880_65_internal
c 737 X_2881_68_internal
c 738 X_2882_71_internal
c 739 X_2883_1217_internal
c 740 X_2886_51_output
c 741 X_2887_54_output
c 742 X_2888_60_output
c 743 X_2889_63_output
c 744 X_2890_66_output
c 745 X_2891_69_output
c 746 X_2892_72_output
c 747 X_2895_375_internal
c 748 X_2896_1221_internal
c 749 X_2897_376_internal
c 750 X_2898_55_internal
c 751 X_2899_57_output
c
p cnf 751 2053
-751 86 0
-751 750 0
-750 -749 -747 0
-750 -86 751 0
-749 -748 -265 0
-748 -739 0
-747 -739 -300 0
-746 -738 -729 0
-745 -737 -727 0
-744 89 0
-744 736 0
-743 88 0
-743 735 0
-742 87 0
-742 734 0
-741 85 0
-741 733 0
-740 84 0
-740 732 0
-739 -731 -721 0
-738 -730 -101 0
-737 -728 -100 0
-736 -726 -714 0
-736 -89 744 0
-735 -725 -713 0
-735 -88 743 0
-734 -724 -712 0
-734 -87 742 0
-733 -723 -711 0
-733 -85 741 0
-732 -722 -710 0
-732 -84 740 0
-731 -720 -471 0
-730 -709 0
-729 -709 -104 0
-728 -708 0
-727 -708 -103 0
-726 -719 -434 0
-725 -718 -392 0
-724 -717 -418 0
-723 -716 -524 0
-722 -715 -523 0
-721 -707 -487 0
-720 -707 0
-719 -704 0
-718 -703 0
-717 -702 0
-716 -701 0
-715 -700 0
-714 -704 -474 0
-713 -703 -444 0
-712 -702 -464 0
-711 -701 -531 0
-710 -700 -530 0
-709 -706 -697 0
-708 -705 -695 0
-707 26 0
-707 31 0
-707 693 0
-706 -698 -480 0
-705 -696 -479 0
-704 31 0
-704 115 0
-704 693 0
-703 28 0
-703 31 0
-703 693 0
-702 27 0
-702 31 0
-702 693 0
-701 25 0
-701 31 0
-701 693 0
-700 31 0
-700 114 0
-700 693 0
-699 -694 0
-699 -576 0
-698 -682 0
-697 -682 -505 0
-696 -681 0
-695 -681 -504 0
-694 32 0
-694 67 0
-694 571 0
-694 692 0
-693 -664 -663 0
-693 -115 -31 704 0
-693 -114 -31 700 0
-693 -31 -28 703 0
-693 -31 -27 702 0
-693 -31 -26 707 0
-693 -31 -25 701 0
-692 -571 -67 -32 694 0
-692 635 0
-692 663 0
-692 664 0
-691 -678 -657 0
-690 -677 -655 0
-689 -676 -653 0
-688 -675 -651 0
-687 -673 -648 0
-686 -672 -646 0
-685 -671 -644 0
-684 -670 -642 0
-683 -669 -640 0
-682 59 0
-682 662 0
-681 58 0
-681 661 0
-680 -660 -633 0
-679 -659 -631 0
-678 -658 -14 0
-677 -656 -13 0
-676 -654 -12 0
-675 -652 -11 0
-674 -650 -629 0
-673 -649 -9 0
-672 -647 -8 0
-671 -645 -7 0
-670 -643 -6 0
-669 -641 -5 0
-668 -639 -627 0
-667 -638 -625 0
-666 -637 -623 0
-665 -636 -621 0
-664 -663 -635 692 0
-664 585 0
-664 586 0
-664 587 0
-664 599 0
-664 600 0
-664 601 0
-664 602 0
-664 603 0
-663 581 0
-663 582 0
-663 583 0
-663 584 0
-663 595 0
-663 596 0
-663 597 0
-663 598 0
-662 -603 -602 -601 -600 -599 -587 -586 -585 0
-662 -59 682 0
-661 -598 -597 -596 -595 -584 -583 -582 -581 0
-661 -58 681 0
-660 -634 -16 0
-659 -632 -15 0
-658 -620 0
-657 -620 -81 0
-656 -619 0
-655 -619 -80 0
-654 -618 0
-653 -618 -79 0
-652 -617 0
-651 -617 -78 0
-650 -630 -10 0
-649 -616 0
-648 -616 -76 0
-647 -615 0
-646 -615 -75 0
-645 -614 0
-644 -614 -74 0
-643 -613 0
-642 -613 -73 0
-641 -612 0
-640 -612 -72 0
-639 -628 -4 0
-638 -626 -3 0
-637 -624 -2 0
-636 -622 -1 0
-635 604 0
-635 605 0
-635 606 0
-635 607 0
-635 608 0
-635 609 0
-635 610 0
-635 611 0
-634 -594 0
-633 -594 -83 0
-632 -593 0
-631 -593 -82 0
-630 -592 0
-629 -592 -77 0
-628 -591 0
-627 -591 -71 0
-626 -590 0
-625 -590 -70 0
-624 -589 0
-623 -589 -69 0
-622 -588 0
-621 -588 -68 0
-620 193 0
-620 537 0
-620 570 0
-620 573 0
-620 578 0
-619 193 0
-619 535 0
-619 570 0
-619 575 0
-619 578 0
-618 193 0
-618 536 0
-618 570 0
-618 574 0
-618 578 0
-617 193 0
-617 537 0
-617 570 0
-617 574 0
-617 578 0
-616 193 0
-616 537 0
-616 568 0
-616 573 0
-616 580 0
-615 192 0
-615 538 0
-615 568 0
-615 572 0
-615 580 0
-614 192 0
-614 535 0
-614 568 0
-614 575 0
-614 580 0
-613 192 0
-613 536 0
-613 568 0
-613 574 0
-613 580 0
-612 192 0
-612 537 0
-612 568 0
-612 574 0
-612 580 0
-611 -610 -609 -608 -607 -606 -605 -604 635 0
-611 -580 -577 -572 -535 -131 0
-610 -579 -578 -572 -535 -131 0
-609 -580 -578 -573 -535 -131 0
-608 -580 -578 -572 -536 -131 0
-607 -580 -578 -572 -537 -131 0
-606 -580 -578 -574 -535 -131 0
-605 -578 -572 -570 -535 -131 0
-604 -580 -572 -568 -535 -131 0
-603 -602 -601 -600 -599 -587 -586 -585 664 0
-603 -578 -573 -570 -537 -193 0
-602 -578 -575 -570 -535 -193 0
-601 -578 -574 -570 -536 -193 0
-600 -578 -574 -570 -537 -193 0
-599 -580 -573 -568 -537 -193 0
-598 -597 -596 -595 -584 -583 -582 -581 663 0
-598 -580 -572 -568 -538 -192 0
-597 -580 -575 -568 -535 -192 0
-596 -580 -574 -568 -536 -192 0
-595 -580 -574 -568 -537 -192 0
-594 193 0
-594 537 0
-594 568 0
-594 570 0
-594 575 0
-593 193 0
-593 538 0
-593 568 0
-593 570 0
-593 574 0
-592 193 0
-592 536 0
-592 568 0
-592 570 0
-592 575 0
-591 192 0
-591 535 0
-591 568 0
-591 570 0
-591 573 0
-590 192 0
-590 536 0
-590 568 0
-590 570 0
-590 572 0
-589 192 0
-589 537 0
-589 568 0
-589 570 0
-589 572 0
-588 192 0
-588 535 0
-588 568 0
-588 570 0
-588 574 0
-587 -575 -570 -568 -537 -193 0
-586 -574 -570 -568 -538 -193 0
-585 -575 -570 -568 -536 -193 0
-584 -573 -570 -568 -535 -192 0
-583 -572 -570 -568 -536 -192 0
-582 -572 -570 -568 -537 -192 0
-581 -574 -570 -568 -535 -192 0
-580 -575 -568 -535 -192 614 0
-580 -574 -568 -537 -192 612 0
-580 -574 -568 -536 -192 613 0
-580 -573 -568 -537 -193 616 0
-580 -572 -568 -538 -192 615 0
-580 117 0
-580 569 0
-579 191 0
-579 569 0
-578 -575 -570 -535 -193 619 0
-578 -574 -570 -537 -193 617 0
-578 -574 -570 -536 -193 618 0
-578 -573 -570 -537 -193 620 0
-578 116 0
-578 567 0
-577 190 0
-577 567 0
-576 65 0
-576 67 0
-576 571 0
-575 -570 -568 -537 -193 594 0
-575 -570 -568 -536 -193 592 0
-575 521 0
-575 558 0
-574 -570 -568 -538 -193 593 0
-574 -570 -568 -535 -192 588 0
-574 534 0
-574 558 0
-573 -570 -568 -535 -192 591 0
-573 521 0
-573 566 0
-572 -570 -568 -537 -192 589 0
-572 -570 -568 -536 -192 590 0
-572 534 0
-572 566 0
-571 -565 -564 -563 -528 -522 -499 -117 -116 0
-571 -67 -65 576 0
-570 117 0
-570 562 0
-569 -562 0
-569 -191 579 0
-569 -117 580 0
-568 116 0
-568 560 0
-567 -560 0
-567 -190 577 0
-567 -116 578 0
-566 -558 0
-566 -534 572 0
-566 -521 573 0
-565 -561 0
-564 -559 0
-563 -557 0
-562 -556 -549 0
-562 -117 570 0
-561 -555 -547 0
-560 -554 -545 0
-560 -116 568 0
-559 -553 -543 0
-558 -552 -541 0
-558 -534 574 0
-558 -521 575 0
-557 -551 -539 0
-556 -550 -54 0
-555 -548 -54 0
-554 -546 -118 0
-553 -544 -118 0
-552 -542 -55 0
-551 -540 -55 0
-550 -533 0
-549 -533 -121 0
-548 -533 0
-547 -533 -120 0
-546 -532 0
-545 -532 -252 0
-544 -532 0
-543 -532 -251 0
-542 -527 0
-541 -527 -123 0
-540 -527 0
-539 -527 -122 0
-538 486 0
-538 513 0
-537 513 0
-537 514 0
-536 486 0
-536 529 0
-535 514 0
-535 529 0
-534 -521 0
-533 -526 -62 0
-532 -525 -62 0
-531 -524 0
-530 -523 0
-529 -514 535 0
-529 -513 0
-529 -486 536 0
-528 -520 0
-527 -519 -62 0
-526 -518 -508 0
-525 -517 0
-524 -516 -503 0
-523 -515 -501 0
-522 -512 0
-521 -511 -495 0
-520 -510 -493 0
-519 -509 -492 0
-518 -507 -343 0
-517 -506 -490 0
-516 -502 -353 0
-515 -500 -448 0
-514 -513 537 0
-514 -486 0
-513 -498 -483 0
-513 -486 538 0
-512 -497 -481 0
-511 -496 -119 0
-510 -494 -119 0
-509 -491 -283 0
-508 -488 -355 0
-507 -488 0
-506 -489 -459 0
-505 -480 0
-504 -479 0
-503 -478 -360 0
-502 -478 0
-501 -469 -450 0
-500 -450 0
-499 -485 0
-498 -484 -56 0
-497 -482 -56 0
-496 -455 0
-495 -455 -254 0
-494 -455 0
-493 -455 -253 0
-492 -477 -325 0
-491 -477 0
-490 -473 -450 0
-489 -450 0
-488 -472 0
-487 -471 0
-486 -476 -467 0
-485 -475 -465 0
-484 -445 0
-483 -445 -125 0
-482 -445 0
-481 -445 -124 0
-480 94 0
-480 462 0
-479 93 0
-479 460 0
-478 -470 -457 0
-477 -463 0
-476 -468 -57 0
-475 -466 -57 0
-474 -434 0
-473 -459 0
-472 -461 -451 0
-471 -458 -447 0
-470 -456 -348 0
-469 -448 0
-468 -420 0
-467 -420 -127 0
-466 -420 0
-465 -420 -126 0
-464 -418 0
-463 -454 -442 0
-462 -453 0
-462 -94 480 0
-461 -452 -348 0
-460 -449 0
-460 -93 479 0
-459 -440 0
-458 -446 -349 0
-457 -436 -410 0
-456 -436 0
-455 -434 -62 0
-454 -443 -349 0
-453 -441 -432 0
-452 -437 0
-451 -437 -402 0
-450 -439 -429 0
-449 -438 -427 0
-448 -435 -422 0
-447 -425 -388 0
-446 -425 0
-445 -418 -62 0
-444 -392 0
-443 -426 0
-442 -426 -377 0
-441 -433 -243 0
-440 -431 -416 0
-439 -430 -231 0
-438 -428 -231 0
-437 -424 -412 0
-436 -423 -409 0
-435 -421 -90 0
-434 -419 -404 0
-433 -413 0
-432 -413 -276 0
-431 -417 -90 0
-430 -406 0
-429 -406 -318 0
-428 -407 0
-427 -407 -317 0
-426 -415 -401 0
-425 -414 -399 0
-424 -411 -331 0
-423 -408 -331 0
-422 -395 -207 0
-421 -395 0
-420 -392 -62 0
-419 -405 -247 0
-418 -403 -390 0
-417 -396 0
-416 -396 -182 0
-415 -400 -348 0
-414 -398 -348 0
-413 -397 -384 0
-412 -373 -347 0
-411 -347 0
-410 -348 0
-409 -372 -347 0
-408 -347 0
-407 -394 -380 0
-406 -393 -378 0
-405 -386 0
-404 -386 -278 0
-403 -391 -308 0
-402 -348 0
-401 -389 -335 0
-400 -335 0
-399 -387 -335 0
-398 -335 0
-397 -385 -344 0
-396 -383 -370 0
-395 -382 -368 0
-394 -381 -332 0
-393 -379 -332 0
-392 -376 -364 0
-391 -374 0
-390 -374 -338 0
-389 -348 0
-388 -349 0
-387 -348 0
-386 -375 -362 0
-385 -347 0
-384 -356 -347 0
-383 -371 -42 0
-382 -369 -42 0
-381 -346 0
-380 -367 -346 0
-379 -346 0
-378 -366 -346 0
-377 -349 0
-376 -365 -98 0
-375 -363 -329 0
-374 -361 -357 0
-373 -331 0
-372 -331 0
-371 -335 0
-370 -335 -208 0
-369 -335 0
-368 -335 -206 0
-367 -332 0
-366 -332 0
-365 -359 0
-364 -359 -110 0
-363 -354 0
-362 -354 -352 0
-361 -358 -311 0
-360 -353 0
-359 -351 -350 0
-358 -345 0
-357 -345 -340 0
-356 -344 0
-355 -343 0
-354 -339 0
-353 -337 0
-352 -329 0
-351 -342 -312 0
-350 -341 -313 0
-349 -333 0
-348 -336 0
-347 -334 0
-346 -330 0
-345 -328 -310 0
-344 -326 -305 0
-343 -327 -307 0
-342 -313 0
-341 -312 0
-340 -311 0
-339 -324 -301 0
-338 -308 0
-337 -323 -298 0
-336 -322 -296 0
-335 -321 -294 0
-334 -320 -292 0
-333 -319 -290 0
-332 -316 -288 0
-331 -315 -286 0
-330 -314 -284 0
-329 -303 0
-328 -309 -49 0
-327 -306 -91 0
-326 -304 -44 0
-325 -283 0
-324 -302 -49 0
-323 -299 -91 0
-322 -297 -44 0
-321 -295 -43 0
-320 -293 -43 0
-319 -291 -38 0
-318 -231 0
-317 -231 0
-316 -289 -38 0
-315 -287 -34 0
-314 -285 -34 0
-313 -281 -273 0
-312 -282 -275 0
-311 -280 -269 0
-310 -270 -225 0
-309 -270 0
-308 -279 -267 0
-307 -263 -216 0
-306 -263 0
-305 -261 -211 0
-304 -261 0
-303 -277 -249 0
-302 -271 0
-301 -271 -188 0
-300 -265 0
-299 -264 0
-298 -264 -184 0
-297 -262 0
-296 -262 -183 0
-295 -259 0
-294 -259 -181 0
-293 -260 0
-292 -260 -180 0
-291 -258 0
-290 -258 -179 0
-289 -257 0
-288 -257 -178 0
-287 -255 0
-286 -255 -176 0
-285 -256 0
-284 -256 -175 0
-283 -248 0
-282 -274 -45 0
-281 -272 -36 0
-280 -268 -44 0
-279 -266 -35 0
-278 -247 0
-277 -250 -37 0
-276 -243 0
-275 -229 -156 0
-274 -229 0
-273 -228 -153 0
-272 -228 0
-271 -246 -227 0
-270 -245 -224 0
-269 -222 -148 0
-268 -222 0
-267 -221 -145 0
-266 -221 0
-265 -244 -220 0
-264 -242 -218 0
-263 -241 -215 0
-262 -240 -213 0
-261 -239 -210 0
-260 -238 -205 0
-259 -237 -203 0
-258 -236 -201 0
-257 -235 -199 0
-256 -234 -197 0
-255 -233 -195 0
-254 -119 0
-253 -119 0
-252 -118 0
-251 -118 0
-250 -230 0
-249 -230 -111 0
-248 -232 -187 0
-247 -189 0
-246 -226 -42 0
-245 -223 -42 0
-244 -219 -34 0
-243 -185 0
-242 -217 -37 0
-241 -214 -37 0
-240 -212 -46 0
-239 -209 -46 0
-238 -204 -49 0
-237 -202 -49 0
-236 -200 -40 0
-235 -198 -40 0
-234 -196 -36 0
-233 -194 -36 0
-232 -186 -34 0
-231 -177 0
-230 -174 -173 0
-229 -172 -171 0
-228 -170 -169 0
-227 -150 -47 0
-226 -47 0
-225 -49 0
-224 -149 -47 0
-223 -47 0
-222 -168 -167 0
-221 -166 -165 0
-220 -142 -92 0
-219 -92 0
-218 -141 -47 0
-217 -47 0
-216 -91 0
-215 -140 -47 0
-214 -47 0
-213 -139 -45 0
-212 -45 0
-211 -44 0
-210 -138 -45 0
-209 -45 0
-208 -42 0
-207 -90 0
-206 -42 0
-205 -137 -48 0
-204 -48 0
-203 -136 -48 0
-202 -48 0
-201 -135 -39 0
-200 -39 0
-199 -134 -39 0
-198 -39 0
-197 -133 -35 0
-196 -35 0
-195 -132 -35 0
-194 -35 0
-193 -130 -129 0
-192 -130 -128 0
-191 -117 0
-190 -116 0
-189 -164 -163 0
-188 -49 0
-187 -109 -92 0
-186 -92 0
-185 -162 -161 0
-184 -91 0
-183 -44 0
-182 -90 0
-181 -43 0
-180 -43 0
-179 -38 0
-178 -38 0
-177 -160 -159 0
-176 -34 0
-175 -34 0
-174 -158 -40 0
-173 -157 -43 0
-172 -155 -43 0
-171 -154 -48 0
-170 -152 -39 0
-169 -151 -41 0
-168 -147 -102 0
-167 -146 -48 0
-166 -144 -38 0
-165 -143 -41 0
-164 -113 -46 0
-163 -112 -99 0
-162 -108 -42 0
-161 -107 -47 0
-160 -106 -37 0
-159 -105 -41 0
-158 -43 0
-157 -40 0
-156 -45 0
-155 -48 0
-154 -43 0
-153 -36 0
-152 -41 0
-151 -39 0
-150 -42 0
-149 -42 0
-148 -44 0
-147 -48 0
-146 -102 0
-145 -35 0
-144 -41 0
-143 -38 0
-142 -34 0
-141 -37 0
-140 -37 0
-139 -46 0
-138 -46 0
-137 -49 0
-136 -49 0
-135 -40 0
-134 -40 0
-133 -36 0
-132 -36 0
-131 32 0
-131 67 0
-131 95 0
-130 -95 -67 -32 0
-129 -95 -61 -33 -31 0
-128 -95 -60 -33 -31 0
-127 -57 0
-126 -57 0
-125 -56 0
-124 -56 0
-123 -55 0
-122 -55 0
-121 -54 0
-120 -54 0
-119 -96 -19 0
-118 -97 -17 0
-117 -96 -20 0
-116 -97 -18 0
-115 19 0
-115 96 0
-114 17 0
-114 97 0
-113 -99 0
-112 -46 0
-111 -37 0
-110 -98 0
-109 -34 0
-108 -47 0
-107 -42 0
-106 -41 0
-105 -37 0
-104 -101 0
-103 -100 0
-102 18 0
-102 52 0
-102 66 0
-101 33 0
-101 51 0
-100 33 0
-100 50 0
-99 20 0
-99 23 0
-99 66 0
-98 19 0
-98 23 0
-98 66 0
-97 -63 -53 0
-97 -17 114 0
-96 -63 -23 0
-96 -19 115 0
-95 -67 -32 131 0
-95 -24 -23 0
-94 -61 -33 0
-93 -60 -33 0
-92 17 0
-92 52 0
-92 66 0
-91 22 0
-91 66 0
-90 21 0
-90 66 0
-89 -64 -33 0
-88 -64 -33 0
-87 -64 -33 0
-86 -64 -33 0
-85 -64 -33 0
-84 -64 -33 0
-83 -16 0
-82 -15 0
-81 -14 0
-80 -13 0
-79 -12 0
-78 -11 0
-77 -10 0
-76 -9 0
-75 -8 0
-74 -7 0
-73 -6 0
-72 -5 0
-71 -4 0
-70 -3 0
-69 -2 0
-68 -1 0
-67 -33 0
-66 -52 -18 102 0
-66 -52 -17 92 0
-66 -33 0
-66 -23 -20 99 0
-66 -23 -19 98 0
-66 -22 91 0
-66 -21 90 0
-65 -32 0
-64 -32 0
-63 -31 0
-62 -31 0
-61 -30 0
-60 -29 0
-59 -33 0
-58 -33 0
-57 -28 0
-56 -27 0
-55 -26 0
-54 -25 0
-53 -24 0
-52 -24 0
-51 -33 101 0
-51 -30 -22 0
-50 -33 100 0
-50 -29 -21 0
-49 -16 0
-48 -15 0
-47 -14 0
-46 -13 0
-45 -12 0
-44 -11 0
-43 -10 0
-42 -9 0
-41 -8 0
-40 -7 0
-39 -6 0
-38 -5 0
-37 -4 0
-36 -3 0
-35 -2 0
-34 -1 0
1 34 0
1 68 0
1 636 0
2 35 0
2 69 0
2 637 0
3 36 0
3 70 0
3 638 0
4 37 0
4 71 0
4 639 0
5 38 0
5 72 0
5 669 0
6 39 0
6 73 0
6 670 0
7 40 0
7 74 0
7 671 0
8 41 0
8 75 0
8 672 0
9 42 0
9 76 0
9 673 0
10 43 0
10 77 0
10 650 0
11 44 0
11 78 0
11 675 0
12 45 0
12 79 0
12 676 0
13 46 0
13 80 0
13 677 0
14 47 0
14 81 0
14 678 0
15 48 0
15 82 0
15 659 0
16 49 0
16 83 0
16 660 0
17 118 0
18 116 0
19 119 0
20 117 0
21 50 0
22 51 0
23 95 0
23 96 0
24 52 0
24 53 0
24 95 0
25 54 0
26 55 0
27 56 0
28 57 0
29 50 0
29 60 0
30 51 0
30 61 0
31 62 0
31 63 0
31 128 0
31 129 0
32 64 0
32 65 0
32 130 0
33 58 0
33 59 0
33 66 0
33 67 0
33 84 0
33 85 0
33 86 0
33 87 0
33 88 0
33 89 0
33 93 0
33 94 0
33 128 0
33 129 0
34 109 0
34 142 0
34 175 0
34 176 0
34 232 0
34 244 0
34 314 0
34 315 0
35 145 0
35 194 0
35 195 0
35 196 0
35 197 0
35 279 0
36 132 0
36 133 0
36 153 0
36 233 0
36 234 0
36 281 0
37 105 0
37 111 0
37 140 0
37 141 0
37 160 0
37 241 0
37 242 0
37 277 0
38 143 0
38 166 0
38 178 0
38 179 0
38 316 0
38 319 0
39 151 0
39 170 0
39 198 0
39 199 0
39 200 0
39 201 0
40 134 0
40 135 0
40 157 0
40 174 0
40 235 0
40 236 0
41 106 0
41 144 0
41 152 0
41 159 0
41 165 0
41 169 0
42 107 0
42 149 0
42 150 0
42 162 0
42 206 0
42 208 0
42 245 0
42 246 0
42 382 0
42 383 0
43 154 0
43 158 0
43 172 0
43 173 0
43 180 0
43 181 0
43 320 0
43 321 0
44 148 0
44 183 0
44 211 0
44 280 0
44 322 0
44 326 0
45 156 0
45 209 0
45 210 0
45 212 0
45 213 0
45 282 0
46 112 0
46 138 0
46 139 0
46 164 0
46 239 0
46 240 0
47 108 0
47 161 0
47 214 0
47 215 0
47 217 0
47 218 0
47 223 0
47 224 0
47 226 0
47 227 0
48 147 0
48 155 0
48 167 0
48 171 0
48 202 0
48 203 0
48 204 0
48 205 0
49 136 0
49 137 0
49 188 0
49 225 0
49 237 0
49 238 0
49 324 0
49 328 0
53 97 0
54 120 0
54 121 0
54 555 0
54 556 0
55 122 0
55 123 0
55 551 0
55 552 0
56 124 0
56 125 0
56 497 0
56 498 0
57 126 0
57 127 0
57 475 0
57 476 0
60 93 0
60 128 0
61 94 0
61 129 0
62 420 0
62 445 0
62 455 0
62 527 0
62 532 0
62 533 0
63 96 0
63 97 0
64 84 0
64 85 0
64 86 0
64 87 0
64 88 0
64 89 0
67 130 0
68 621 0
69 623 0
70 625 0
71 627 0
72 640 0
73 642 0
74 644 0
75 646 0
76 648 0
77 629 0
78 651 0
79 653 0
80 655 0
81 657 0
82 631 0
83 633 0
90 182 0
90 207 0
90 431 0
90 435 0
91 184 0
91 216 0
91 323 0
91 327 0
92 186 0
92 187 0
92 219 0
92 220 0
95 128 0
95 129 0
95 130 0
96 117 0
96 119 0
97 116 0
97 118 0
98 110 0
98 376 0
99 113 0
99 163 0
100 103 0
100 737 0
101 104 0
101 738 0
102 146 0
102 168 0
103 727 0
104 729 0
105 159 0
106 160 0
107 161 0
108 162 0
109 187 0
110 364 0
111 249 0
112 163 0
113 164 0
116 190 0
116 571 0
117 191 0
117 571 0
118 251 0
118 252 0
118 553 0
118 554 0
119 253 0
119 254 0
119 510 0
119 511 0
120 547 0
121 549 0
122 539 0
123 541 0
124 481 0
125 483 0
126 465 0
127 467 0
128 192 0
129 193 0
130 192 0
130 193 0
131 604 0
131 605 0
131 606 0
131 607 0
131 608 0
131 609 0
131 610 0
131 611 0
132 195 0
133 197 0
134 199 0
135 201 0
136 203 0
137 205 0
138 210 0
139 213 0
140 215 0
141 218 0
142 220 0
143 165 0
144 166 0
145 267 0
146 167 0
147 168 0
148 269 0
149 224 0
150 227 0
151 169 0
152 170 0
153 273 0
154 171 0
155 172 0
156 275 0
157 173 0
158 174 0
159 177 0
160 177 0
161 185 0
162 185 0
163 189 0
164 189 0
165 221 0
166 221 0
167 222 0
168 222 0
169 228 0
170 228 0
171 229 0
172 229 0
173 230 0
174 230 0
175 284 0
176 286 0
177 231 0
178 288 0
179 290 0
180 292 0
181 294 0
182 416 0
183 296 0
184 298 0
185 243 0
186 232 0
187 248 0
188 301 0
189 247 0
192 581 0
192 582 0
192 583 0
192 584 0
192 595 0
192 596 0
192 597 0
192 598 0
193 585 0
193 586 0
193 587 0
193 599 0
193 600 0
193 601 0
193 602 0
193 603 0
194 233 0
195 255 0
196 234 0
197 256 0
198 235 0
199 257 0
200 236 0
201 258 0
202 237 0
203 259 0
204 238 0
205 260 0
206 368 0
207 422 0
208 370 0
209 239 0
210 261 0
211 305 0
212 240 0
213 262 0
214 241 0
215 263 0
216 307 0
217 242 0
218 264 0
219 244 0
220 265 0
221 266 0
221 267 0
222 268 0
222 269 0
223 245 0
224 270 0
225 310 0
226 246 0
227 271 0
228 272 0
228 273 0
229 274 0
229 275 0
230 249 0
230 250 0
231 317 0
231 318 0
231 438 0
231 439 0
232 248 0
233 255 0
234 256 0
235 257 0
236 258 0
237 259 0
238 260 0
239 261 0
240 262 0
241 263 0
242 264 0
243 276 0
243 441 0
244 265 0
245 270 0
246 271 0
247 278 0
247 419 0
248 283 0
249 303 0
250 277 0
251 543 0
252 545 0
253 493 0
254 495 0
255 286 0
255 287 0
256 284 0
256 285 0
257 288 0
257 289 0
258 290 0
258 291 0
259 294 0
259 295 0
260 292 0
260 293 0
261 304 0
261 305 0
262 296 0
262 297 0
263 306 0
263 307 0
264 298 0
264 299 0
265 300 0
265 749 0
266 279 0
267 308 0
268 280 0
269 311 0
270 309 0
270 310 0
271 301 0
271 302 0
272 281 0
273 313 0
274 282 0
275 312 0
276 432 0
277 303 0
278 404 0
279 308 0
280 311 0
281 313 0
282 312 0
283 325 0
283 509 0
284 330 0
285 314 0
286 331 0
287 315 0
288 332 0
289 316 0
290 333 0
291 319 0
292 334 0
293 320 0
294 335 0
295 321 0
296 336 0
297 322 0
298 337 0
299 323 0
300 747 0
301 339 0
302 324 0
303 329 0
304 326 0
305 344 0
306 327 0
307 343 0
308 338 0
308 403 0
309 328 0
310 345 0
311 340 0
311 361 0
312 341 0
312 351 0
313 342 0
313 350 0
314 330 0
315 331 0
316 332 0
317 427 0
318 429 0
319 333 0
320 334 0
321 335 0
322 336 0
323 337 0
324 339 0
325 492 0
326 344 0
327 343 0
328 345 0
329 352 0
329 375 0
330 346 0
331 372 0
331 373 0
331 423 0
331 424 0
332 366 0
332 367 0
332 393 0
332 394 0
333 349 0
334 347 0
335 368 0
335 369 0
335 370 0
335 371 0
335 398 0
335 399 0
335 400 0
335 401 0
336 348 0
337 353 0
338 390 0
339 354 0
340 357 0
341 350 0
342 351 0
343 355 0
343 518 0
344 356 0
344 397 0
345 357 0
345 358 0
346 378 0
346 379 0
346 380 0
346 381 0
347 384 0
347 385 0
347 408 0
347 409 0
347 411 0
347 412 0
348 387 0
348 389 0
348 402 0
348 410 0
348 414 0
348 415 0
348 461 0
348 470 0
349 377 0
349 388 0
349 454 0
349 458 0
350 359 0
351 359 0
352 362 0
353 360 0
353 516 0
354 362 0
354 363 0
355 508 0
356 384 0
357 374 0
358 361 0
359 364 0
359 365 0
360 503 0
361 374 0
362 386 0
363 375 0
364 392 0
365 376 0
366 378 0
367 380 0
368 395 0
369 382 0
370 396 0
371 383 0
372 409 0
373 412 0
374 390 0
374 391 0
375 386 0
376 392 0
377 442 0
378 406 0
379 393 0
380 407 0
381 394 0
382 395 0
383 396 0
384 413 0
385 397 0
386 404 0
386 405 0
387 399 0
388 447 0
389 401 0
390 418 0
391 403 0
392 420 0
392 444 0
392 725 0
393 406 0
394 407 0
395 421 0
395 422 0
396 416 0
396 417 0
397 413 0
398 414 0
399 425 0
400 415 0
401 426 0
402 451 0
403 418 0
404 434 0
405 419 0
406 429 0
406 430 0
407 427 0
407 428 0
408 423 0
409 436 0
410 457 0
411 424 0
412 437 0
413 432 0
413 433 0
414 425 0
415 426 0
416 440 0
417 431 0
418 445 0
418 464 0
418 724 0
419 434 0
420 465 0
420 466 0
420 467 0
420 468 0
421 435 0
422 448 0
423 436 0
424 437 0
425 446 0
425 447 0
426 442 0
426 443 0
427 449 0
428 438 0
429 450 0
430 439 0
431 440 0
432 453 0
433 441 0
434 455 0
434 474 0
434 726 0
435 448 0
436 456 0
436 457 0
437 451 0
437 452 0
438 449 0
439 450 0
440 459 0
441 453 0
442 463 0
443 454 0
444 713 0
445 481 0
445 482 0
445 483 0
445 484 0
446 458 0
447 471 0
448 469 0
448 515 0
449 460 0
450 489 0
450 490 0
450 500 0
450 501 0
451 472 0
452 461 0
453 462 0
454 463 0
455 493 0
455 494 0
455 495 0
455 496 0
456 470 0
457 478 0
458 471 0
459 473 0
459 506 0
461 472 0
463 477 0
464 712 0
465 485 0
466 475 0
467 486 0
468 476 0
469 501 0
470 478 0
471 487 0
471 731 0
472 488 0
473 490 0
474 714 0
475 485 0
476 486 0
477 491 0
477 492 0
478 502 0
478 503 0
479 504 0
479 705 0
480 505 0
480 706 0
481 512 0
482 497 0
483 513 0
484 498 0
485 499 0
486 514 0
487 721 0
488 507 0
488 508 0
489 506 0
490 517 0
491 509 0
492 519 0
493 520 0
494 510 0
495 521 0
496 511 0
497 512 0
498 513 0
499 571 0
500 515 0
501 523 0
502 516 0
503 524 0
504 695 0
505 697 0
506 517 0
507 518 0
508 526 0
509 519 0
510 520 0
511 521 0
512 522 0
513 529 0
515 523 0
516 524 0
517 525 0
518 526 0
519 527 0
520 528 0
521 534 0
522 571 0
523 530 0
523 722 0
524 531 0
524 723 0
525 532 0
526 533 0
527 539 0
527 540 0
527 541 0
527 542 0
528 571 0
530 710 0
531 711 0
532 543 0
532 544 0
532 545 0
532 546 0
533 547 0
533 548 0
533 549 0
533 550 0
535 581 0
535 584 0
535 597 0
535 602 0
535 604 0
535 605 0
535 606 0
535 609 0
535 610 0
535 611 0
536 583 0
536 585 0
536 596 0
536 601 0
536 608 0
537 582 0
537 587 0
537 595 0
537 599 0
537 600 0
537 603 0
537 607 0
538 586 0
538 598 0
539 557 0
540 551 0
541 558 0
542 552 0
543 559 0
544 553 0
545 560 0
546 554 0
547 561 0
548 555 0
549 562 0
550 556 0
551 557 0
552 558 0
553 559 0
554 560 0
555 561 0
556 562 0
557 563 0
558 566 0
559 564 0
560 567 0
561 565 0
562 569 0
563 571 0
564 571 0
565 571 0
568 581 0
568 582 0
568 583 0
568 584 0
568 585 0
568 586 0
568 587 0
568 595 0
568 596 0
568 597 0
568 598 0
568 599 0
568 604 0
570 581 0
570 582 0
570 583 0
570 584 0
570 585 0
570 586 0
570 587 0
570 600 0
570 601 0
570 602 0
570 603 0
570 605 0
572 582 0
572 583 0
572 598 0
572 604 0
572 605 0
572 607 0
572 608 0
572 610 0
572 611 0
573 584 0
573 599 0
573 603 0
573 609 0
574 581 0
574 586 0
574 595 0
574 596 0
574 600 0
574 601 0
574 606 0
575 585 0
575 587 0
575 597 0
575 602 0
576 694 699 0
577 611 0
578 600 0
578 601 0
578 602 0
578 603 0
578 605 0
578 606 0
578 607 0
578 608 0
578 609 0
578 610 0
579 610 0
580 595 0
580 596 0
580 597 0
580 598 0
580 599 0
580 604 0
580 606 0
580 607 0
580 608 0
580 609 0
580 611 0
581 661 0
582 661 0
583 661 0
584 661 0
585 662 0
586 662 0
587 662 0
588 621 0
588 622 0
589 623 0
589 624 0
590 625 0
590 626 0
591 627 0
591 628 0
592 629 0
592 630 0
593 631 0
593 632 0
594 633 0
594 634 0
595 661 0
596 661 0
597 661 0
598 661 0
599 662 0
600 662 0
601 662 0
602 662 0
603 662 0
612 640 0
612 641 0
613 642 0
613 643 0
614 644 0
614 645 0
615 646 0
615 647 0
616 648 0
616 649 0
617 651 0
617 652 0
618 653 0
618 654 0
619 655 0
619 656 0
620 657 0
620 658 0
621 665 0
622 636 0
623 666 0
624 637 0
625 667 0
626 638 0
627 668 0
628 639 0
629 674 0
630 650 0
631 679 0
632 659 0
633 680 0
634 660 0
636 665 0
637 666 0
638 667 0
639 668 0
640 683 0
641 669 0
642 684 0
643 670 0
644 685 0
645 671 0
646 686 0
647 672 0
648 687 0
649 673 0
650 674 0
651 688 0
652 675 0
653 689 0
654 676 0
655 690 0
656 677 0
657 691 0
658 678 0
659 679 0
660 680 0
663 693 0
664 693 0
669 683 0
670 684 0
671 685 0
672 686 0
673 687 0
675 688 0
676 689 0
677 690 0
678 691 0
681 695 0
681 696 0
682 697 0
682 698 0
695 708 0
696 705 0
697 709 0
698 706 0
700 710 0
700 715 0
701 711 0
701 716 0
702 712 0
702 717 0
703 713 0
703 718 0
704 714 0
704 719 0
705 708 0
706 709 0
707 720 0
707 721 0
708 727 0
708 728 0
709 729 0
709 730 0
710 732 0
711 733 0
712 734 0
713 735 0
714 736 0
715 722 0
716 723 0
717 724 0
718 725 0
719 726 0
720 731 0
721 739 0
722 732 0
723 733 0
724 734 0
725 735 0
726 736 0
727 745 0
728 737 0
729 746 0
730 738 0
731 739 0
737 745 0
738 746 0
739 747 0
739 748 0
747 750 0
748 749 0
749 750 0
%
0