atpg-ls/c6288.bench

# c6288

INPUT(1)
INPUT(18)
INPUT(35)
INPUT(52)
INPUT(69)
INPUT(86)
INPUT(103)
INPUT(120)
INPUT(137)
INPUT(154)
INPUT(171)
INPUT(188)
INPUT(205)
INPUT(222)
INPUT(239)
INPUT(256)
INPUT(273)
INPUT(290)
INPUT(307)
INPUT(324)
INPUT(341)
INPUT(358)
INPUT(375)
INPUT(392)
INPUT(409)
INPUT(426)
INPUT(443)
INPUT(460)
INPUT(477)
INPUT(494)
INPUT(511)
INPUT(528)

OUTPUT(545)
OUTPUT(1581)
OUTPUT(1901)
OUTPUT(2223)
OUTPUT(2548)
OUTPUT(2877)
OUTPUT(3211)
OUTPUT(3552)
OUTPUT(3895)
OUTPUT(4241)
OUTPUT(4591)
OUTPUT(4946)
OUTPUT(5308)
OUTPUT(5672)
OUTPUT(5971)
OUTPUT(6123)
OUTPUT(6150)
OUTPUT(6160)
OUTPUT(6170)
OUTPUT(6180)
OUTPUT(6190)
OUTPUT(6200)
OUTPUT(6210)
OUTPUT(6220)
OUTPUT(6230)
OUTPUT(6240)
OUTPUT(6250)
OUTPUT(6260)
OUTPUT(6270)
OUTPUT(6280)
OUTPUT(6287)
OUTPUT(6288)

545 = AND(1, 273)
546 = AND(1, 290)
549 = AND(1, 307)
552 = AND(1, 324)
555 = AND(1, 341)
558 = AND(1, 358)
561 = AND(1, 375)
564 = AND(1, 392)
567 = AND(1, 409)
570 = AND(1, 426)
573 = AND(1, 443)
576 = AND(1, 460)
579 = AND(1, 477)
582 = AND(1, 494)
585 = AND(1, 511)
588 = AND(1, 528)
591 = AND(18, 273)
594 = AND(18, 290)
597 = AND(18, 307)
600 = AND(18, 324)
603 = AND(18, 341)
606 = AND(18, 358)
609 = AND(18, 375)
612 = AND(18, 392)
615 = AND(18, 409)
618 = AND(18, 426)
621 = AND(18, 443)
624 = AND(18, 460)
627 = AND(18, 477)
630 = AND(18, 494)
633 = AND(18, 511)
636 = AND(18, 528)
639 = AND(35, 273)
642 = AND(35, 290)
645 = AND(35, 307)
648 = AND(35, 324)
651 = AND(35, 341)
654 = AND(35, 358)
657 = AND(35, 375)
660 = AND(35, 392)
663 = AND(35, 409)
666 = AND(35, 426)
669 = AND(35, 443)
672 = AND(35, 460)
675 = AND(35, 477)
678 = AND(35, 494)
681 = AND(35, 511)
684 = AND(35, 528)
687 = AND(52, 273)
690 = AND(52, 290)
693 = AND(52, 307)
696 = AND(52, 324)
699 = AND(52, 341)
702 = AND(52, 358)
705 = AND(52, 375)
708 = AND(52, 392)
711 = AND(52, 409)
714 = AND(52, 426)
717 = AND(52, 443)
720 = AND(52, 460)
723 = AND(52, 477)
726 = AND(52, 494)
729 = AND(52, 511)
732 = AND(52, 528)
735 = AND(69, 273)
738 = AND(69, 290)
741 = AND(69, 307)
744 = AND(69, 324)
747 = AND(69, 341)
750 = AND(69, 358)
753 = AND(69, 375)
756 = AND(69, 392)
759 = AND(69, 409)
762 = AND(69, 426)
765 = AND(69, 443)
768 = AND(69, 460)
771 = AND(69, 477)
774 = AND(69, 494)
777 = AND(69, 511)
780 = AND(69, 528)
783 = AND(86, 273)
786 = AND(86, 290)
789 = AND(86, 307)
792 = AND(86, 324)
795 = AND(86, 341)
798 = AND(86, 358)
801 = AND(86, 375)
804 = AND(86, 392)
807 = AND(86, 409)
810 = AND(86, 426)
813 = AND(86, 443)
816 = AND(86, 460)
819 = AND(86, 477)
822 = AND(86, 494)
825 = AND(86, 511)
828 = AND(86, 528)
831 = AND(103, 273)
834 = AND(103, 290)
837 = AND(103, 307)
840 = AND(103, 324)
843 = AND(103, 341)
846 = AND(103, 358)
849 = AND(103, 375)
852 = AND(103, 392)
855 = AND(103, 409)
858 = AND(103, 426)
861 = AND(103, 443)
864 = AND(103, 460)
867 = AND(103, 477)
870 = AND(103, 494)
873 = AND(103, 511)
876 = AND(103, 528)
879 = AND(120, 273)
882 = AND(120, 290)
885 = AND(120, 307)
888 = AND(120, 324)
891 = AND(120, 341)
894 = AND(120, 358)
897 = AND(120, 375)
900 = AND(120, 392)
903 = AND(120, 409)
906 = AND(120, 426)
909 = AND(120, 443)
912 = AND(120, 460)
915 = AND(120, 477)
918 = AND(120, 494)
921 = AND(120, 511)
924 = AND(120, 528)
927 = AND(137, 273)
930 = AND(137, 290)
933 = AND(137, 307)
936 = AND(137, 324)
939 = AND(137, 341)
942 = AND(137, 358)
945 = AND(137, 375)
948 = AND(137, 392)
951 = AND(137, 409)
954 = AND(137, 426)
957 = AND(137, 443)
960 = AND(137, 460)
963 = AND(137, 477)
966 = AND(137, 494)
969 = AND(137, 511)
972 = AND(137, 528)
975 = AND(154, 273)
978 = AND(154, 290)
981 = AND(154, 307)
984 = AND(154, 324)
987 = AND(154, 341)
990 = AND(154, 358)
993 = AND(154, 375)
996 = AND(154, 392)
999 = AND(154, 409)
1002 = AND(154, 426)
1005 = AND(154, 443)
1008 = AND(154, 460)
1011 = AND(154, 477)
1014 = AND(154, 494)
1017 = AND(154, 511)
1020 = AND(154, 528)
1023 = AND(171, 273)
1026 = AND(171, 290)
1029 = AND(171, 307)
1032 = AND(171, 324)
1035 = AND(171, 341)
1038 = AND(171, 358)
1041 = AND(171, 375)
1044 = AND(171, 392)
1047 = AND(171, 409)
1050 = AND(171, 426)
1053 = AND(171, 443)
1056 = AND(171, 460)
1059 = AND(171, 477)
1062 = AND(171, 494)
1065 = AND(171, 511)
1068 = AND(171, 528)
1071 = AND(188, 273)
1074 = AND(188, 290)
1077 = AND(188, 307)
1080 = AND(188, 324)
1083 = AND(188, 341)
1086 = AND(188, 358)
1089 = AND(188, 375)
1092 = AND(188, 392)
1095 = AND(188, 409)
1098 = AND(188, 426)
1101 = AND(188, 443)
1104 = AND(188, 460)
1107 = AND(188, 477)
1110 = AND(188, 494)
1113 = AND(188, 511)
1116 = AND(188, 528)
1119 = AND(205, 273)
1122 = AND(205, 290)
1125 = AND(205, 307)
1128 = AND(205, 324)
1131 = AND(205, 341)
1134 = AND(205, 358)
1137 = AND(205, 375)
1140 = AND(205, 392)
1143 = AND(205, 409)
1146 = AND(205, 426)
1149 = AND(205, 443)
1152 = AND(205, 460)
1155 = AND(205, 477)
1158 = AND(205, 494)
1161 = AND(205, 511)
1164 = AND(205, 528)
1167 = AND(222, 273)
1170 = AND(222, 290)
1173 = AND(222, 307)
1176 = AND(222, 324)
1179 = AND(222, 341)
1182 = AND(222, 358)
1185 = AND(222, 375)
1188 = AND(222, 392)
1191 = AND(222, 409)
1194 = AND(222, 426)
1197 = AND(222, 443)
1200 = AND(222, 460)
1203 = AND(222, 477)
1206 = AND(222, 494)
1209 = AND(222, 511)
1212 = AND(222, 528)
1215 = AND(239, 273)
1218 = AND(239, 290)
1221 = AND(239, 307)
1224 = AND(239, 324)
1227 = AND(239, 341)
1230 = AND(239, 358)
1233 = AND(239, 375)
1236 = AND(239, 392)
1239 = AND(239, 409)
1242 = AND(239, 426)
1245 = AND(239, 443)
1248 = AND(239, 460)
1251 = AND(239, 477)
1254 = AND(239, 494)
1257 = AND(239, 511)
1260 = AND(239, 528)
1263 = AND(256, 273)
1266 = AND(256, 290)
1269 = AND(256, 307)
1272 = AND(256, 324)
1275 = AND(256, 341)
1278 = AND(256, 358)
1281 = AND(256, 375)
1284 = AND(256, 392)
1287 = AND(256, 409)
1290 = AND(256, 426)
1293 = AND(256, 443)
1296 = AND(256, 460)
1299 = AND(256, 477)
1302 = AND(256, 494)
1305 = AND(256, 511)
1308 = AND(256, 528)
1311 = NOT(591)
1315 = NOT(639)
1319 = NOT(687)
1323 = NOT(735)
1327 = NOT(783)
1331 = NOT(831)
1335 = NOT(879)
1339 = NOT(927)
1343 = NOT(975)
1347 = NOT(1023)
1351 = NOT(1071)
1355 = NOT(1119)
1359 = NOT(1167)
1363 = NOT(1215)
1367 = NOT(1263)
1371 = NOR(591, 1311)
1372 = NOT(1311)
1373 = NOR(639, 1315)
1374 = NOT(1315)
1375 = NOR(687, 1319)
1376 = NOT(1319)
1377 = NOR(735, 1323)
1378 = NOT(1323)
1379 = NOR(783, 1327)
1380 = NOT(1327)
1381 = NOR(831, 1331)
1382 = NOT(1331)
1383 = NOR(879, 1335)
1384 = NOT(1335)
1385 = NOR(927, 1339)
1386 = NOT(1339)
1387 = NOR(975, 1343)
1388 = NOT(1343)
1389 = NOR(1023, 1347)
1390 = NOT(1347)
1391 = NOR(1071, 1351)
1392 = NOT(1351)
1393 = NOR(1119, 1355)
1394 = NOT(1355)
1395 = NOR(1167, 1359)
1396 = NOT(1359)
1397 = NOR(1215, 1363)
1398 = NOT(1363)
1399 = NOR(1263, 1367)
1400 = NOT(1367)
1401 = NOR(1371, 1372)
1404 = NOR(1373, 1374)
1407 = NOR(1375, 1376)
1410 = NOR(1377, 1378)
1413 = NOR(1379, 1380)
1416 = NOR(1381, 1382)
1419 = NOR(1383, 1384)
1422 = NOR(1385, 1386)
1425 = NOR(1387, 1388)
1428 = NOR(1389, 1390)
1431 = NOR(1391, 1392)
1434 = NOR(1393, 1394)
1437 = NOR(1395, 1396)
1440 = NOR(1397, 1398)
1443 = NOR(1399, 1400)
1446 = NOR(1401, 546)
1450 = NOR(1404, 594)
1454 = NOR(1407, 642)
1458 = NOR(1410, 690)
1462 = NOR(1413, 738)
1466 = NOR(1416, 786)
1470 = NOR(1419, 834)
1474 = NOR(1422, 882)
1478 = NOR(1425, 930)
1482 = NOR(1428, 978)
1486 = NOR(1431, 1026)
1490 = NOR(1434, 1074)
1494 = NOR(1437, 1122)
1498 = NOR(1440, 1170)
1502 = NOR(1443, 1218)
1506 = NOR(1401, 1446)
1507 = NOR(1446, 546)
1508 = NOR(1311, 1446)
1511 = NOR(1404, 1450)
1512 = NOR(1450, 594)
1513 = NOR(1315, 1450)
1516 = NOR(1407, 1454)
1517 = NOR(1454, 642)
1518 = NOR(1319, 1454)
1521 = NOR(1410, 1458)
1522 = NOR(1458, 690)
1523 = NOR(1323, 1458)
1526 = NOR(1413, 1462)
1527 = NOR(1462, 738)
1528 = NOR(1327, 1462)
1531 = NOR(1416, 1466)
1532 = NOR(1466, 786)
1533 = NOR(1331, 1466)
1536 = NOR(1419, 1470)
1537 = NOR(1470, 834)
1538 = NOR(1335, 1470)
1541 = NOR(1422, 1474)
1542 = NOR(1474, 882)
1543 = NOR(1339, 1474)
1546 = NOR(1425, 1478)
1547 = NOR(1478, 930)
1548 = NOR(1343, 1478)
1551 = NOR(1428, 1482)
1552 = NOR(1482, 978)
1553 = NOR(1347, 1482)
1556 = NOR(1431, 1486)
1557 = NOR(1486, 1026)
1558 = NOR(1351, 1486)
1561 = NOR(1434, 1490)
1562 = NOR(1490, 1074)
1563 = NOR(1355, 1490)
1566 = NOR(1437, 1494)
1567 = NOR(1494, 1122)
1568 = NOR(1359, 1494)
1571 = NOR(1440, 1498)
1572 = NOR(1498, 1170)
1573 = NOR(1363, 1498)
1576 = NOR(1443, 1502)
1577 = NOR(1502, 1218)
1578 = NOR(1367, 1502)
1581 = NOR(1506, 1507)
1582 = NOR(1511, 1512)
1585 = NOR(1516, 1517)
1588 = NOR(1521, 1522)
1591 = NOR(1526, 1527)
1594 = NOR(1531, 1532)
1597 = NOR(1536, 1537)
1600 = NOR(1541, 1542)
1603 = NOR(1546, 1547)
1606 = NOR(1551, 1552)
1609 = NOR(1556, 1557)
1612 = NOR(1561, 1562)
1615 = NOR(1566, 1567)
1618 = NOR(1571, 1572)
1621 = NOR(1576, 1577)
1624 = NOR(1266, 1578)
1628 = NOR(1582, 1508)
1632 = NOR(1585, 1513)
1636 = NOR(1588, 1518)
1640 = NOR(1591, 1523)
1644 = NOR(1594, 1528)
1648 = NOR(1597, 1533)
1652 = NOR(1600, 1538)
1656 = NOR(1603, 1543)
1660 = NOR(1606, 1548)
1664 = NOR(1609, 1553)
1668 = NOR(1612, 1558)
1672 = NOR(1615, 1563)
1676 = NOR(1618, 1568)
1680 = NOR(1621, 1573)
1684 = NOR(1266, 1624)
1685 = NOR(1624, 1578)
1686 = NOR(1582, 1628)
1687 = NOR(1628, 1508)
1688 = NOR(1585, 1632)
1689 = NOR(1632, 1513)
1690 = NOR(1588, 1636)
1691 = NOR(1636, 1518)
1692 = NOR(1591, 1640)
1693 = NOR(1640, 1523)
1694 = NOR(1594, 1644)
1695 = NOR(1644, 1528)
1696 = NOR(1597, 1648)
1697 = NOR(1648, 1533)
1698 = NOR(1600, 1652)
1699 = NOR(1652, 1538)
1700 = NOR(1603, 1656)
1701 = NOR(1656, 1543)
1702 = NOR(1606, 1660)
1703 = NOR(1660, 1548)
1704 = NOR(1609, 1664)
1705 = NOR(1664, 1553)
1706 = NOR(1612, 1668)
1707 = NOR(1668, 1558)
1708 = NOR(1615, 1672)
1709 = NOR(1672, 1563)
1710 = NOR(1618, 1676)
1711 = NOR(1676, 1568)
1712 = NOR(1621, 1680)
1713 = NOR(1680, 1573)
1714 = NOR(1684, 1685)
1717 = NOR(1686, 1687)
1720 = NOR(1688, 1689)
1723 = NOR(1690, 1691)
1726 = NOR(1692, 1693)
1729 = NOR(1694, 1695)
1732 = NOR(1696, 1697)
1735 = NOR(1698, 1699)
1738 = NOR(1700, 1701)
1741 = NOR(1702, 1703)
1744 = NOR(1704, 1705)
1747 = NOR(1706, 1707)
1750 = NOR(1708, 1709)
1753 = NOR(1710, 1711)
1756 = NOR(1712, 1713)
1759 = NOR(1714, 1221)
1763 = NOR(1717, 549)
1767 = NOR(1720, 597)
1771 = NOR(1723, 645)
1775 = NOR(1726, 693)
1779 = NOR(1729, 741)
1783 = NOR(1732, 789)
1787 = NOR(1735, 837)
1791 = NOR(1738, 885)
1795 = NOR(1741, 933)
1799 = NOR(1744, 981)
1803 = NOR(1747, 1029)
1807 = NOR(1750, 1077)
1811 = NOR(1753, 1125)
1815 = NOR(1756, 1173)
1819 = NOR(1714, 1759)
1820 = NOR(1759, 1221)
1821 = NOR(1624, 1759)
1824 = NOR(1717, 1763)
1825 = NOR(1763, 549)
1826 = NOR(1628, 1763)
1829 = NOR(1720, 1767)
1830 = NOR(1767, 597)
1831 = NOR(1632, 1767)
1834 = NOR(1723, 1771)
1835 = NOR(1771, 645)
1836 = NOR(1636, 1771)
1839 = NOR(1726, 1775)
1840 = NOR(1775, 693)
1841 = NOR(1640, 1775)
1844 = NOR(1729, 1779)
1845 = NOR(1779, 741)
1846 = NOR(1644, 1779)
1849 = NOR(1732, 1783)
1850 = NOR(1783, 789)
1851 = NOR(1648, 1783)
1854 = NOR(1735, 1787)
1855 = NOR(1787, 837)
1856 = NOR(1652, 1787)
1859 = NOR(1738, 1791)
1860 = NOR(1791, 885)
1861 = NOR(1656, 1791)
1864 = NOR(1741, 1795)
1865 = NOR(1795, 933)
1866 = NOR(1660, 1795)
1869 = NOR(1744, 1799)
1870 = NOR(1799, 981)
1871 = NOR(1664, 1799)
1874 = NOR(1747, 1803)
1875 = NOR(1803, 1029)
1876 = NOR(1668, 1803)
1879 = NOR(1750, 1807)
1880 = NOR(1807, 1077)
1881 = NOR(1672, 1807)
1884 = NOR(1753, 1811)
1885 = NOR(1811, 1125)
1886 = NOR(1676, 1811)
1889 = NOR(1756, 1815)
1890 = NOR(1815, 1173)
1891 = NOR(1680, 1815)
1894 = NOR(1819, 1820)
1897 = NOR(1269, 1821)
1901 = NOR(1824, 1825)
1902 = NOR(1829, 1830)
1905 = NOR(1834, 1835)
1908 = NOR(1839, 1840)
1911 = NOR(1844, 1845)
1914 = NOR(1849, 1850)
1917 = NOR(1854, 1855)
1920 = NOR(1859, 1860)
1923 = NOR(1864, 1865)
1926 = NOR(1869, 1870)
1929 = NOR(1874, 1875)
1932 = NOR(1879, 1880)
1935 = NOR(1884, 1885)
1938 = NOR(1889, 1890)
1941 = NOR(1894, 1891)
1945 = NOR(1269, 1897)
1946 = NOR(1897, 1821)
1947 = NOR(1902, 1826)
1951 = NOR(1905, 1831)
1955 = NOR(1908, 1836)
1959 = NOR(1911, 1841)
1963 = NOR(1914, 1846)
1967 = NOR(1917, 1851)
1971 = NOR(1920, 1856)
1975 = NOR(1923, 1861)
1979 = NOR(1926, 1866)
1983 = NOR(1929, 1871)
1987 = NOR(1932, 1876)
1991 = NOR(1935, 1881)
1995 = NOR(1938, 1886)
1999 = NOR(1894, 1941)
2000 = NOR(1941, 1891)
2001 = NOR(1945, 1946)
2004 = NOR(1902, 1947)
2005 = NOR(1947, 1826)
2006 = NOR(1905, 1951)
2007 = NOR(1951, 1831)
2008 = NOR(1908, 1955)
2009 = NOR(1955, 1836)
2010 = NOR(1911, 1959)
2011 = NOR(1959, 1841)
2012 = NOR(1914, 1963)
2013 = NOR(1963, 1846)
2014 = NOR(1917, 1967)
2015 = NOR(1967, 1851)
2016 = NOR(1920, 1971)
2017 = NOR(1971, 1856)
2018 = NOR(1923, 1975)
2019 = NOR(1975, 1861)
2020 = NOR(1926, 1979)
2021 = NOR(1979, 1866)
2022 = NOR(1929, 1983)
2023 = NOR(1983, 1871)
2024 = NOR(1932, 1987)
2025 = NOR(1987, 1876)
2026 = NOR(1935, 1991)
2027 = NOR(1991, 1881)
2028 = NOR(1938, 1995)
2029 = NOR(1995, 1886)
2030 = NOR(1999, 2000)
2033 = NOR(2001, 1224)
2037 = NOR(2004, 2005)
2040 = NOR(2006, 2007)
2043 = NOR(2008, 2009)
2046 = NOR(2010, 2011)
2049 = NOR(2012, 2013)
2052 = NOR(2014, 2015)
2055 = NOR(2016, 2017)
2058 = NOR(2018, 2019)
2061 = NOR(2020, 2021)
2064 = NOR(2022, 2023)
2067 = NOR(2024, 2025)
2070 = NOR(2026, 2027)
2073 = NOR(2028, 2029)
2076 = NOR(2030, 1176)
2080 = NOR(2001, 2033)
2081 = NOR(2033, 1224)
2082 = NOR(1897, 2033)
2085 = NOR(2037, 552)
2089 = NOR(2040, 600)
2093 = NOR(2043, 648)
2097 = NOR(2046, 696)
2101 = NOR(2049, 744)
2105 = NOR(2052, 792)
2109 = NOR(2055, 840)
2113 = NOR(2058, 888)
2117 = NOR(2061, 936)
2121 = NOR(2064, 984)
2125 = NOR(2067, 1032)
2129 = NOR(2070, 1080)
2133 = NOR(2073, 1128)
2137 = NOR(2030, 2076)
2138 = NOR(2076, 1176)
2139 = NOR(1941, 2076)
2142 = NOR(2080, 2081)
2145 = NOR(1272, 2082)
2149 = NOR(2037, 2085)
2150 = NOR(2085, 552)
2151 = NOR(1947, 2085)
2154 = NOR(2040, 2089)
2155 = NOR(2089, 600)
2156 = NOR(1951, 2089)
2159 = NOR(2043, 2093)
2160 = NOR(2093, 648)
2161 = NOR(1955, 2093)
2164 = NOR(2046, 2097)
2165 = NOR(2097, 696)
2166 = NOR(1959, 2097)
2169 = NOR(2049, 2101)
2170 = NOR(2101, 744)
2171 = NOR(1963, 2101)
2174 = NOR(2052, 2105)
2175 = NOR(2105, 792)
2176 = NOR(1967, 2105)
2179 = NOR(2055, 2109)
2180 = NOR(2109, 840)
2181 = NOR(1971, 2109)
2184 = NOR(2058, 2113)
2185 = NOR(2113, 888)
2186 = NOR(1975, 2113)
2189 = NOR(2061, 2117)
2190 = NOR(2117, 936)
2191 = NOR(1979, 2117)
2194 = NOR(2064, 2121)
2195 = NOR(2121, 984)
2196 = NOR(1983, 2121)
2199 = NOR(2067, 2125)
2200 = NOR(2125, 1032)
2201 = NOR(1987, 2125)
2204 = NOR(2070, 2129)
2205 = NOR(2129, 1080)
2206 = NOR(1991, 2129)
2209 = NOR(2073, 2133)
2210 = NOR(2133, 1128)
2211 = NOR(1995, 2133)
2214 = NOR(2137, 2138)
2217 = NOR(2142, 2139)
2221 = NOR(1272, 2145)
2222 = NOR(2145, 2082)
2223 = NOR(2149, 2150)
2224 = NOR(2154, 2155)
2227 = NOR(2159, 2160)
2230 = NOR(2164, 2165)
2233 = NOR(2169, 2170)
2236 = NOR(2174, 2175)
2239 = NOR(2179, 2180)
2242 = NOR(2184, 2185)
2245 = NOR(2189, 2190)
2248 = NOR(2194, 2195)
2251 = NOR(2199, 2200)
2254 = NOR(2204, 2205)
2257 = NOR(2209, 2210)
2260 = NOR(2214, 2211)
2264 = NOR(2142, 2217)
2265 = NOR(2217, 2139)
2266 = NOR(2221, 2222)
2269 = NOR(2224, 2151)
2273 = NOR(2227, 2156)
2277 = NOR(2230, 2161)
2281 = NOR(2233, 2166)
2285 = NOR(2236, 2171)
2289 = NOR(2239, 2176)
2293 = NOR(2242, 2181)
2297 = NOR(2245, 2186)
2301 = NOR(2248, 2191)
2305 = NOR(2251, 2196)
2309 = NOR(2254, 2201)
2313 = NOR(2257, 2206)
2317 = NOR(2214, 2260)
2318 = NOR(2260, 2211)
2319 = NOR(2264, 2265)
2322 = NOR(2266, 1227)
2326 = NOR(2224, 2269)
2327 = NOR(2269, 2151)
2328 = NOR(2227, 2273)
2329 = NOR(2273, 2156)
2330 = NOR(2230, 2277)
2331 = NOR(2277, 2161)
2332 = NOR(2233, 2281)
2333 = NOR(2281, 2166)
2334 = NOR(2236, 2285)
2335 = NOR(2285, 2171)
2336 = NOR(2239, 2289)
2337 = NOR(2289, 2176)
2338 = NOR(2242, 2293)
2339 = NOR(2293, 2181)
2340 = NOR(2245, 2297)
2341 = NOR(2297, 2186)
2342 = NOR(2248, 2301)
2343 = NOR(2301, 2191)
2344 = NOR(2251, 2305)
2345 = NOR(2305, 2196)
2346 = NOR(2254, 2309)
2347 = NOR(2309, 2201)
2348 = NOR(2257, 2313)
2349 = NOR(2313, 2206)
2350 = NOR(2317, 2318)
2353 = NOR(2319, 1179)
2357 = NOR(2266, 2322)
2358 = NOR(2322, 1227)
2359 = NOR(2145, 2322)
2362 = NOR(2326, 2327)
2365 = NOR(2328, 2329)
2368 = NOR(2330, 2331)
2371 = NOR(2332, 2333)
2374 = NOR(2334, 2335)
2377 = NOR(2336, 2337)
2380 = NOR(2338, 2339)
2383 = NOR(2340, 2341)
2386 = NOR(2342, 2343)
2389 = NOR(2344, 2345)
2392 = NOR(2346, 2347)
2395 = NOR(2348, 2349)
2398 = NOR(2350, 1131)
2402 = NOR(2319, 2353)
2403 = NOR(2353, 1179)
2404 = NOR(2217, 2353)
2407 = NOR(2357, 2358)
2410 = NOR(1275, 2359)
2414 = NOR(2362, 555)
2418 = NOR(2365, 603)
2422 = NOR(2368, 651)
2426 = NOR(2371, 699)
2430 = NOR(2374, 747)
2434 = NOR(2377, 795)
2438 = NOR(2380, 843)
2442 = NOR(2383, 891)
2446 = NOR(2386, 939)
2450 = NOR(2389, 987)
2454 = NOR(2392, 1035)
2458 = NOR(2395, 1083)
2462 = NOR(2350, 2398)
2463 = NOR(2398, 1131)
2464 = NOR(2260, 2398)
2467 = NOR(2402, 2403)
2470 = NOR(2407, 2404)
2474 = NOR(1275, 2410)
2475 = NOR(2410, 2359)
2476 = NOR(2362, 2414)
2477 = NOR(2414, 555)
2478 = NOR(2269, 2414)
2481 = NOR(2365, 2418)
2482 = NOR(2418, 603)
2483 = NOR(2273, 2418)
2486 = NOR(2368, 2422)
2487 = NOR(2422, 651)
2488 = NOR(2277, 2422)
2491 = NOR(2371, 2426)
2492 = NOR(2426, 699)
2493 = NOR(2281, 2426)
2496 = NOR(2374, 2430)
2497 = NOR(2430, 747)
2498 = NOR(2285, 2430)
2501 = NOR(2377, 2434)
2502 = NOR(2434, 795)
2503 = NOR(2289, 2434)
2506 = NOR(2380, 2438)
2507 = NOR(2438, 843)
2508 = NOR(2293, 2438)
2511 = NOR(2383, 2442)
2512 = NOR(2442, 891)
2513 = NOR(2297, 2442)
2516 = NOR(2386, 2446)
2517 = NOR(2446, 939)
2518 = NOR(2301, 2446)
2521 = NOR(2389, 2450)
2522 = NOR(2450, 987)
2523 = NOR(2305, 2450)
2526 = NOR(2392, 2454)
2527 = NOR(2454, 1035)
2528 = NOR(2309, 2454)
2531 = NOR(2395, 2458)
2532 = NOR(2458, 1083)
2533 = NOR(2313, 2458)
2536 = NOR(2462, 2463)
2539 = NOR(2467, 2464)
2543 = NOR(2407, 2470)
2544 = NOR(2470, 2404)
2545 = NOR(2474, 2475)
2548 = NOR(2476, 2477)
2549 = NOR(2481, 2482)
2552 = NOR(2486, 2487)
2555 = NOR(2491, 2492)
2558 = NOR(2496, 2497)
2561 = NOR(2501, 2502)
2564 = NOR(2506, 2507)
2567 = NOR(2511, 2512)
2570 = NOR(2516, 2517)
2573 = NOR(2521, 2522)
2576 = NOR(2526, 2527)
2579 = NOR(2531, 2532)
2582 = NOR(2536, 2533)
2586 = NOR(2467, 2539)
2587 = NOR(2539, 2464)
2588 = NOR(2543, 2544)
2591 = NOR(2545, 1230)
2595 = NOR(2549, 2478)
2599 = NOR(2552, 2483)
2603 = NOR(2555, 2488)
2607 = NOR(2558, 2493)
2611 = NOR(2561, 2498)
2615 = NOR(2564, 2503)
2619 = NOR(2567, 2508)
2623 = NOR(2570, 2513)
2627 = NOR(2573, 2518)
2631 = NOR(2576, 2523)
2635 = NOR(2579, 2528)
2639 = NOR(2536, 2582)
2640 = NOR(2582, 2533)
2641 = NOR(2586, 2587)
2644 = NOR(2588, 1182)
2648 = NOR(2545, 2591)
2649 = NOR(2591, 1230)
2650 = NOR(2410, 2591)
2653 = NOR(2549, 2595)
2654 = NOR(2595, 2478)
2655 = NOR(2552, 2599)
2656 = NOR(2599, 2483)
2657 = NOR(2555, 2603)
2658 = NOR(2603, 2488)
2659 = NOR(2558, 2607)
2660 = NOR(2607, 2493)
2661 = NOR(2561, 2611)
2662 = NOR(2611, 2498)
2663 = NOR(2564, 2615)
2664 = NOR(2615, 2503)
2665 = NOR(2567, 2619)
2666 = NOR(2619, 2508)
2667 = NOR(2570, 2623)
2668 = NOR(2623, 2513)
2669 = NOR(2573, 2627)
2670 = NOR(2627, 2518)
2671 = NOR(2576, 2631)
2672 = NOR(2631, 2523)
2673 = NOR(2579, 2635)
2674 = NOR(2635, 2528)
2675 = NOR(2639, 2640)
2678 = NOR(2641, 1134)
2682 = NOR(2588, 2644)
2683 = NOR(2644, 1182)
2684 = NOR(2470, 2644)
2687 = NOR(2648, 2649)
2690 = NOR(1278, 2650)
2694 = NOR(2653, 2654)
2697 = NOR(2655, 2656)
2700 = NOR(2657, 2658)
2703 = NOR(2659, 2660)
2706 = NOR(2661, 2662)
2709 = NOR(2663, 2664)
2712 = NOR(2665, 2666)
2715 = NOR(2667, 2668)
2718 = NOR(2669, 2670)
2721 = NOR(2671, 2672)
2724 = NOR(2673, 2674)
2727 = NOR(2675, 1086)
2731 = NOR(2641, 2678)
2732 = NOR(2678, 1134)
2733 = NOR(2539, 2678)
2736 = NOR(2682, 2683)
2739 = NOR(2687, 2684)
2743 = NOR(1278, 2690)
2744 = NOR(2690, 2650)
2745 = NOR(2694, 558)
2749 = NOR(2697, 606)
2753 = NOR(2700, 654)
2757 = NOR(2703, 702)
2761 = NOR(2706, 750)
2765 = NOR(2709, 798)
2769 = NOR(2712, 846)
2773 = NOR(2715, 894)
2777 = NOR(2718, 942)
2781 = NOR(2721, 990)
2785 = NOR(2724, 1038)
2789 = NOR(2675, 2727)
2790 = NOR(2727, 1086)
2791 = NOR(2582, 2727)
2794 = NOR(2731, 2732)
2797 = NOR(2736, 2733)
2801 = NOR(2687, 2739)
2802 = NOR(2739, 2684)
2803 = NOR(2743, 2744)
2806 = NOR(2694, 2745)
2807 = NOR(2745, 558)
2808 = NOR(2595, 2745)
2811 = NOR(2697, 2749)
2812 = NOR(2749, 606)
2813 = NOR(2599, 2749)
2816 = NOR(2700, 2753)
2817 = NOR(2753, 654)
2818 = NOR(2603, 2753)
2821 = NOR(2703, 2757)
2822 = NOR(2757, 702)
2823 = NOR(2607, 2757)
2826 = NOR(2706, 2761)
2827 = NOR(2761, 750)
2828 = NOR(2611, 2761)
2831 = NOR(2709, 2765)
2832 = NOR(2765, 798)
2833 = NOR(2615, 2765)
2836 = NOR(2712, 2769)
2837 = NOR(2769, 846)
2838 = NOR(2619, 2769)
2841 = NOR(2715, 2773)
2842 = NOR(2773, 894)
2843 = NOR(2623, 2773)
2846 = NOR(2718, 2777)
2847 = NOR(2777, 942)
2848 = NOR(2627, 2777)
2851 = NOR(2721, 2781)
2852 = NOR(2781, 990)
2853 = NOR(2631, 2781)
2856 = NOR(2724, 2785)
2857 = NOR(2785, 1038)
2858 = NOR(2635, 2785)
2861 = NOR(2789, 2790)
2864 = NOR(2794, 2791)
2868 = NOR(2736, 2797)
2869 = NOR(2797, 2733)
2870 = NOR(2801, 2802)
2873 = NOR(2803, 1233)
2877 = NOR(2806, 2807)
2878 = NOR(2811, 2812)
2881 = NOR(2816, 2817)
2884 = NOR(2821, 2822)
2887 = NOR(2826, 2827)
2890 = NOR(2831, 2832)
2893 = NOR(2836, 2837)
2896 = NOR(2841, 2842)
2899 = NOR(2846, 2847)
2902 = NOR(2851, 2852)
2905 = NOR(2856, 2857)
2908 = NOR(2861, 2858)
2912 = NOR(2794, 2864)
2913 = NOR(2864, 2791)
2914 = NOR(2868, 2869)
2917 = NOR(2870, 1185)
2921 = NOR(2803, 2873)
2922 = NOR(2873, 1233)
2923 = NOR(2690, 2873)
2926 = NOR(2878, 2808)
2930 = NOR(2881, 2813)
2934 = NOR(2884, 2818)
2938 = NOR(2887, 2823)
2942 = NOR(2890, 2828)
2946 = NOR(2893, 2833)
2950 = NOR(2896, 2838)
2954 = NOR(2899, 2843)
2958 = NOR(2902, 2848)
2962 = NOR(2905, 2853)
2966 = NOR(2861, 2908)
2967 = NOR(2908, 2858)
2968 = NOR(2912, 2913)
2971 = NOR(2914, 1137)
2975 = NOR(2870, 2917)
2976 = NOR(2917, 1185)
2977 = NOR(2739, 2917)
2980 = NOR(2921, 2922)
2983 = NOR(1281, 2923)
2987 = NOR(2878, 2926)
2988 = NOR(2926, 2808)
2989 = NOR(2881, 2930)
2990 = NOR(2930, 2813)
2991 = NOR(2884, 2934)
2992 = NOR(2934, 2818)
2993 = NOR(2887, 2938)
2994 = NOR(2938, 2823)
2995 = NOR(2890, 2942)
2996 = NOR(2942, 2828)
2997 = NOR(2893, 2946)
2998 = NOR(2946, 2833)
2999 = NOR(2896, 2950)
3000 = NOR(2950, 2838)
3001 = NOR(2899, 2954)
3002 = NOR(2954, 2843)
3003 = NOR(2902, 2958)
3004 = NOR(2958, 2848)
3005 = NOR(2905, 2962)
3006 = NOR(2962, 2853)
3007 = NOR(2966, 2967)
3010 = NOR(2968, 1089)
3014 = NOR(2914, 2971)
3015 = NOR(2971, 1137)
3016 = NOR(2797, 2971)
3019 = NOR(2975, 2976)
3022 = NOR(2980, 2977)
3026 = NOR(1281, 2983)
3027 = NOR(2983, 2923)
3028 = NOR(2987, 2988)
3031 = NOR(2989, 2990)
3034 = NOR(2991, 2992)
3037 = NOR(2993, 2994)
3040 = NOR(2995, 2996)
3043 = NOR(2997, 2998)
3046 = NOR(2999, 3000)
3049 = NOR(3001, 3002)
3052 = NOR(3003, 3004)
3055 = NOR(3005, 3006)
3058 = NOR(3007, 1041)
3062 = NOR(2968, 3010)
3063 = NOR(3010, 1089)
3064 = NOR(2864, 3010)
3067 = NOR(3014, 3015)
3070 = NOR(3019, 3016)
3074 = NOR(2980, 3022)
3075 = NOR(3022, 2977)
3076 = NOR(3026, 3027)
3079 = NOR(3028, 561)
3083 = NOR(3031, 609)
3087 = NOR(3034, 657)
3091 = NOR(3037, 705)
3095 = NOR(3040, 753)
3099 = NOR(3043, 801)
3103 = NOR(3046, 849)
3107 = NOR(3049, 897)
3111 = NOR(3052, 945)
3115 = NOR(3055, 993)
3119 = NOR(3007, 3058)
3120 = NOR(3058, 1041)
3121 = NOR(2908, 3058)
3124 = NOR(3062, 3063)
3127 = NOR(3067, 3064)
3131 = NOR(3019, 3070)
3132 = NOR(3070, 3016)
3133 = NOR(3074, 3075)
3136 = NOR(3076, 1236)
3140 = NOR(3028, 3079)
3141 = NOR(3079, 561)
3142 = NOR(2926, 3079)
3145 = NOR(3031, 3083)
3146 = NOR(3083, 609)
3147 = NOR(2930, 3083)
3150 = NOR(3034, 3087)
3151 = NOR(3087, 657)
3152 = NOR(2934, 3087)
3155 = NOR(3037, 3091)
3156 = NOR(3091, 705)
3157 = NOR(2938, 3091)
3160 = NOR(3040, 3095)
3161 = NOR(3095, 753)
3162 = NOR(2942, 3095)
3165 = NOR(3043, 3099)
3166 = NOR(3099, 801)
3167 = NOR(2946, 3099)
3170 = NOR(3046, 3103)
3171 = NOR(3103, 849)
3172 = NOR(2950, 3103)
3175 = NOR(3049, 3107)
3176 = NOR(3107, 897)
3177 = NOR(2954, 3107)
3180 = NOR(3052, 3111)
3181 = NOR(3111, 945)
3182 = NOR(2958, 3111)
3185 = NOR(3055, 3115)
3186 = NOR(3115, 993)
3187 = NOR(2962, 3115)
3190 = NOR(3119, 3120)
3193 = NOR(3124, 3121)
3197 = NOR(3067, 3127)
3198 = NOR(3127, 3064)
3199 = NOR(3131, 3132)
3202 = NOR(3133, 1188)
3206 = NOR(3076, 3136)
3207 = NOR(3136, 1236)
3208 = NOR(2983, 3136)
3211 = NOR(3140, 3141)
3212 = NOR(3145, 3146)
3215 = NOR(3150, 3151)
3218 = NOR(3155, 3156)
3221 = NOR(3160, 3161)
3224 = NOR(3165, 3166)
3227 = NOR(3170, 3171)
3230 = NOR(3175, 3176)
3233 = NOR(3180, 3181)
3236 = NOR(3185, 3186)
3239 = NOR(3190, 3187)
3243 = NOR(3124, 3193)
3244 = NOR(3193, 3121)
3245 = NOR(3197, 3198)
3248 = NOR(3199, 1140)
3252 = NOR(3133, 3202)
3253 = NOR(3202, 1188)
3254 = NOR(3022, 3202)
3257 = NOR(3206, 3207)
3260 = NOR(1284, 3208)
3264 = NOR(3212, 3142)
3268 = NOR(3215, 3147)
3272 = NOR(3218, 3152)
3276 = NOR(3221, 3157)
3280 = NOR(3224, 3162)
3284 = NOR(3227, 3167)
3288 = NOR(3230, 3172)
3292 = NOR(3233, 3177)
3296 = NOR(3236, 3182)
3300 = NOR(3190, 3239)
3301 = NOR(3239, 3187)
3302 = NOR(3243, 3244)
3305 = NOR(3245, 1092)
3309 = NOR(3199, 3248)
3310 = NOR(3248, 1140)
3311 = NOR(3070, 3248)
3314 = NOR(3252, 3253)
3317 = NOR(3257, 3254)
3321 = NOR(1284, 3260)
3322 = NOR(3260, 3208)
3323 = NOR(3212, 3264)
3324 = NOR(3264, 3142)
3325 = NOR(3215, 3268)
3326 = NOR(3268, 3147)
3327 = NOR(3218, 3272)
3328 = NOR(3272, 3152)
3329 = NOR(3221, 3276)
3330 = NOR(3276, 3157)
3331 = NOR(3224, 3280)
3332 = NOR(3280, 3162)
3333 = NOR(3227, 3284)
3334 = NOR(3284, 3167)
3335 = NOR(3230, 3288)
3336 = NOR(3288, 3172)
3337 = NOR(3233, 3292)
3338 = NOR(3292, 3177)
3339 = NOR(3236, 3296)
3340 = NOR(3296, 3182)
3341 = NOR(3300, 3301)
3344 = NOR(3302, 1044)
3348 = NOR(3245, 3305)
3349 = NOR(3305, 1092)
3350 = NOR(3127, 3305)
3353 = NOR(3309, 3310)
3356 = NOR(3314, 3311)
3360 = NOR(3257, 3317)
3361 = NOR(3317, 3254)
3362 = NOR(3321, 3322)
3365 = NOR(3323, 3324)
3368 = NOR(3325, 3326)
3371 = NOR(3327, 3328)
3374 = NOR(3329, 3330)
3377 = NOR(3331, 3332)
3380 = NOR(3333, 3334)
3383 = NOR(3335, 3336)
3386 = NOR(3337, 3338)
3389 = NOR(3339, 3340)
3392 = NOR(3341, 996)
3396 = NOR(3302, 3344)
3397 = NOR(3344, 1044)
3398 = NOR(3193, 3344)
3401 = NOR(3348, 3349)
3404 = NOR(3353, 3350)
3408 = NOR(3314, 3356)
3409 = NOR(3356, 3311)
3410 = NOR(3360, 3361)
3413 = NOR(3362, 1239)
3417 = NOR(3365, 564)
3421 = NOR(3368, 612)
3425 = NOR(3371, 660)
3429 = NOR(3374, 708)
3433 = NOR(3377, 756)
3437 = NOR(3380, 804)
3441 = NOR(3383, 852)
3445 = NOR(3386, 900)
3449 = NOR(3389, 948)
3453 = NOR(3341, 3392)
3454 = NOR(3392, 996)
3455 = NOR(3239, 3392)
3458 = NOR(3396, 3397)
3461 = NOR(3401, 3398)
3465 = NOR(3353, 3404)
3466 = NOR(3404, 3350)
3467 = NOR(3408, 3409)
3470 = NOR(3410, 1191)
3474 = NOR(3362, 3413)
3475 = NOR(3413, 1239)
3476 = NOR(3260, 3413)
3479 = NOR(3365, 3417)
3480 = NOR(3417, 564)
3481 = NOR(3264, 3417)
3484 = NOR(3368, 3421)
3485 = NOR(3421, 612)
3486 = NOR(3268, 3421)
3489 = NOR(3371, 3425)
3490 = NOR(3425, 660)
3491 = NOR(3272, 3425)
3494 = NOR(3374, 3429)
3495 = NOR(3429, 708)
3496 = NOR(3276, 3429)
3499 = NOR(3377, 3433)
3500 = NOR(3433, 756)
3501 = NOR(3280, 3433)
3504 = NOR(3380, 3437)
3505 = NOR(3437, 804)
3506 = NOR(3284, 3437)
3509 = NOR(3383, 3441)
3510 = NOR(3441, 852)
3511 = NOR(3288, 3441)
3514 = NOR(3386, 3445)
3515 = NOR(3445, 900)
3516 = NOR(3292, 3445)
3519 = NOR(3389, 3449)
3520 = NOR(3449, 948)
3521 = NOR(3296, 3449)
3524 = NOR(3453, 3454)
3527 = NOR(3458, 3455)
3531 = NOR(3401, 3461)
3532 = NOR(3461, 3398)
3533 = NOR(3465, 3466)
3536 = NOR(3467, 1143)
3540 = NOR(3410, 3470)
3541 = NOR(3470, 1191)
3542 = NOR(3317, 3470)
3545 = NOR(3474, 3475)
3548 = NOR(1287, 3476)
3552 = NOR(3479, 3480)
3553 = NOR(3484, 3485)
3556 = NOR(3489, 3490)
3559 = NOR(3494, 3495)
3562 = NOR(3499, 3500)
3565 = NOR(3504, 3505)
3568 = NOR(3509, 3510)
3571 = NOR(3514, 3515)
3574 = NOR(3519, 3520)
3577 = NOR(3524, 3521)
3581 = NOR(3458, 3527)
3582 = NOR(3527, 3455)
3583 = NOR(3531, 3532)
3586 = NOR(3533, 1095)
3590 = NOR(3467, 3536)
3591 = NOR(3536, 1143)
3592 = NOR(3356, 3536)
3595 = NOR(3540, 3541)
3598 = NOR(3545, 3542)
3602 = NOR(1287, 3548)
3603 = NOR(3548, 3476)
3604 = NOR(3553, 3481)
3608 = NOR(3556, 3486)
3612 = NOR(3559, 3491)
3616 = NOR(3562, 3496)
3620 = NOR(3565, 3501)
3624 = NOR(3568, 3506)
3628 = NOR(3571, 3511)
3632 = NOR(3574, 3516)
3636 = NOR(3524, 3577)
3637 = NOR(3577, 3521)
3638 = NOR(3581, 3582)
3641 = NOR(3583, 1047)
3645 = NOR(3533, 3586)
3646 = NOR(3586, 1095)
3647 = NOR(3404, 3586)
3650 = NOR(3590, 3591)
3653 = NOR(3595, 3592)
3657 = NOR(3545, 3598)
3658 = NOR(3598, 3542)
3659 = NOR(3602, 3603)
3662 = NOR(3553, 3604)
3663 = NOR(3604, 3481)
3664 = NOR(3556, 3608)
3665 = NOR(3608, 3486)
3666 = NOR(3559, 3612)
3667 = NOR(3612, 3491)
3668 = NOR(3562, 3616)
3669 = NOR(3616, 3496)
3670 = NOR(3565, 3620)
3671 = NOR(3620, 3501)
3672 = NOR(3568, 3624)
3673 = NOR(3624, 3506)
3674 = NOR(3571, 3628)
3675 = NOR(3628, 3511)
3676 = NOR(3574, 3632)
3677 = NOR(3632, 3516)
3678 = NOR(3636, 3637)
3681 = NOR(3638, 999)
3685 = NOR(3583, 3641)
3686 = NOR(3641, 1047)
3687 = NOR(3461, 3641)
3690 = NOR(3645, 3646)
3693 = NOR(3650, 3647)
3697 = NOR(3595, 3653)
3698 = NOR(3653, 3592)
3699 = NOR(3657, 3658)
3702 = NOR(3659, 1242)
3706 = NOR(3662, 3663)
3709 = NOR(3664, 3665)
3712 = NOR(3666, 3667)
3715 = NOR(3668, 3669)
3718 = NOR(3670, 3671)
3721 = NOR(3672, 3673)
3724 = NOR(3674, 3675)
3727 = NOR(3676, 3677)
3730 = NOR(3678, 951)
3734 = NOR(3638, 3681)
3735 = NOR(3681, 999)
3736 = NOR(3527, 3681)
3739 = NOR(3685, 3686)
3742 = NOR(3690, 3687)
3746 = NOR(3650, 3693)
3747 = NOR(3693, 3647)
3748 = NOR(3697, 3698)
3751 = NOR(3699, 1194)
3755 = NOR(3659, 3702)
3756 = NOR(3702, 1242)
3757 = NOR(3548, 3702)
3760 = NOR(3706, 567)
3764 = NOR(3709, 615)
3768 = NOR(3712, 663)
3772 = NOR(3715, 711)
3776 = NOR(3718, 759)
3780 = NOR(3721, 807)
3784 = NOR(3724, 855)
3788 = NOR(3727, 903)
3792 = NOR(3678, 3730)
3793 = NOR(3730, 951)
3794 = NOR(3577, 3730)
3797 = NOR(3734, 3735)
3800 = NOR(3739, 3736)
3804 = NOR(3690, 3742)
3805 = NOR(3742, 3687)
3806 = NOR(3746, 3747)
3809 = NOR(3748, 1146)
3813 = NOR(3699, 3751)
3814 = NOR(3751, 1194)
3815 = NOR(3598, 3751)
3818 = NOR(3755, 3756)
3821 = NOR(1290, 3757)
3825 = NOR(3706, 3760)
3826 = NOR(3760, 567)
3827 = NOR(3604, 3760)
3830 = NOR(3709, 3764)
3831 = NOR(3764, 615)
3832 = NOR(3608, 3764)
3835 = NOR(3712, 3768)
3836 = NOR(3768, 663)
3837 = NOR(3612, 3768)
3840 = NOR(3715, 3772)
3841 = NOR(3772, 711)
3842 = NOR(3616, 3772)
3845 = NOR(3718, 3776)
3846 = NOR(3776, 759)
3847 = NOR(3620, 3776)
3850 = NOR(3721, 3780)
3851 = NOR(3780, 807)
3852 = NOR(3624, 3780)
3855 = NOR(3724, 3784)
3856 = NOR(3784, 855)
3857 = NOR(3628, 3784)
3860 = NOR(3727, 3788)
3861 = NOR(3788, 903)
3862 = NOR(3632, 3788)
3865 = NOR(3792, 3793)
3868 = NOR(3797, 3794)
3872 = NOR(3739, 3800)
3873 = NOR(3800, 3736)
3874 = NOR(3804, 3805)
3877 = NOR(3806, 1098)
3881 = NOR(3748, 3809)
3882 = NOR(3809, 1146)
3883 = NOR(3653, 3809)
3886 = NOR(3813, 3814)
3889 = NOR(3818, 3815)
3893 = NOR(1290, 3821)
3894 = NOR(3821, 3757)
3895 = NOR(3825, 3826)
3896 = NOR(3830, 3831)
3899 = NOR(3835, 3836)
3902 = NOR(3840, 3841)
3905 = NOR(3845, 3846)
3908 = NOR(3850, 3851)
3911 = NOR(3855, 3856)
3914 = NOR(3860, 3861)
3917 = NOR(3865, 3862)
3921 = NOR(3797, 3868)
3922 = NOR(3868, 3794)
3923 = NOR(3872, 3873)
3926 = NOR(3874, 1050)
3930 = NOR(3806, 3877)
3931 = NOR(3877, 1098)
3932 = NOR(3693, 3877)
3935 = NOR(3881, 3882)
3938 = NOR(3886, 3883)
3942 = NOR(3818, 3889)
3943 = NOR(3889, 3815)
3944 = NOR(3893, 3894)
3947 = NOR(3896, 3827)
3951 = NOR(3899, 3832)
3955 = NOR(3902, 3837)
3959 = NOR(3905, 3842)
3963 = NOR(3908, 3847)
3967 = NOR(3911, 3852)
3971 = NOR(3914, 3857)
3975 = NOR(3865, 3917)
3976 = NOR(3917, 3862)
3977 = NOR(3921, 3922)
3980 = NOR(3923, 1002)
3984 = NOR(3874, 3926)
3985 = NOR(3926, 1050)
3986 = NOR(3742, 3926)
3989 = NOR(3930, 3931)
3992 = NOR(3935, 3932)
3996 = NOR(3886, 3938)
3997 = NOR(3938, 3883)
3998 = NOR(3942, 3943)
4001 = NOR(3944, 1245)
4005 = NOR(3896, 3947)
4006 = NOR(3947, 3827)
4007 = NOR(3899, 3951)
4008 = NOR(3951, 3832)
4009 = NOR(3902, 3955)
4010 = NOR(3955, 3837)
4011 = NOR(3905, 3959)
4012 = NOR(3959, 3842)
4013 = NOR(3908, 3963)
4014 = NOR(3963, 3847)
4015 = NOR(3911, 3967)
4016 = NOR(3967, 3852)
4017 = NOR(3914, 3971)
4018 = NOR(3971, 3857)
4019 = NOR(3975, 3976)
4022 = NOR(3977, 954)
4026 = NOR(3923, 3980)
4027 = NOR(3980, 1002)
4028 = NOR(3800, 3980)
4031 = NOR(3984, 3985)
4034 = NOR(3989, 3986)
4038 = NOR(3935, 3992)
4039 = NOR(3992, 3932)
4040 = NOR(3996, 3997)
4043 = NOR(3998, 1197)
4047 = NOR(3944, 4001)
4048 = NOR(4001, 1245)
4049 = NOR(3821, 4001)
4052 = NOR(4005, 4006)
4055 = NOR(4007, 4008)
4058 = NOR(4009, 4010)
4061 = NOR(4011, 4012)
4064 = NOR(4013, 4014)
4067 = NOR(4015, 4016)
4070 = NOR(4017, 4018)
4073 = NOR(4019, 906)
4077 = NOR(3977, 4022)
4078 = NOR(4022, 954)
4079 = NOR(3868, 4022)
4082 = NOR(4026, 4027)
4085 = NOR(4031, 4028)
4089 = NOR(3989, 4034)
4090 = NOR(4034, 3986)
4091 = NOR(4038, 4039)
4094 = NOR(4040, 1149)
4098 = NOR(3998, 4043)
4099 = NOR(4043, 1197)
4100 = NOR(3889, 4043)
4103 = NOR(4047, 4048)
4106 = NOR(1293, 4049)
4110 = NOR(4052, 570)
4114 = NOR(4055, 618)
4118 = NOR(4058, 666)
4122 = NOR(4061, 714)
4126 = NOR(4064, 762)
4130 = NOR(4067, 810)
4134 = NOR(4070, 858)
4138 = NOR(4019, 4073)
4139 = NOR(4073, 906)
4140 = NOR(3917, 4073)
4143 = NOR(4077, 4078)
4146 = NOR(4082, 4079)
4150 = NOR(4031, 4085)
4151 = NOR(4085, 4028)
4152 = NOR(4089, 4090)
4155 = NOR(4091, 1101)
4159 = NOR(4040, 4094)
4160 = NOR(4094, 1149)
4161 = NOR(3938, 4094)
4164 = NOR(4098, 4099)
4167 = NOR(4103, 4100)
4171 = NOR(1293, 4106)
4172 = NOR(4106, 4049)
4173 = NOR(4052, 4110)
4174 = NOR(4110, 570)
4175 = NOR(3947, 4110)
4178 = NOR(4055, 4114)
4179 = NOR(4114, 618)
4180 = NOR(3951, 4114)
4183 = NOR(4058, 4118)
4184 = NOR(4118, 666)
4185 = NOR(3955, 4118)
4188 = NOR(4061, 4122)
4189 = NOR(4122, 714)
4190 = NOR(3959, 4122)
4193 = NOR(4064, 4126)
4194 = NOR(4126, 762)
4195 = NOR(3963, 4126)
4198 = NOR(4067, 4130)
4199 = NOR(4130, 810)
4200 = NOR(3967, 4130)
4203 = NOR(4070, 4134)
4204 = NOR(4134, 858)
4205 = NOR(3971, 4134)
4208 = NOR(4138, 4139)
4211 = NOR(4143, 4140)
4215 = NOR(4082, 4146)
4216 = NOR(4146, 4079)
4217 = NOR(4150, 4151)
4220 = NOR(4152, 1053)
4224 = NOR(4091, 4155)
4225 = NOR(4155, 1101)
4226 = NOR(3992, 4155)
4229 = NOR(4159, 4160)
4232 = NOR(4164, 4161)
4236 = NOR(4103, 4167)
4237 = NOR(4167, 4100)
4238 = NOR(4171, 4172)
4241 = NOR(4173, 4174)
4242 = NOR(4178, 4179)
4245 = NOR(4183, 4184)
4248 = NOR(4188, 4189)
4251 = NOR(4193, 4194)
4254 = NOR(4198, 4199)
4257 = NOR(4203, 4204)
4260 = NOR(4208, 4205)
4264 = NOR(4143, 4211)
4265 = NOR(4211, 4140)
4266 = NOR(4215, 4216)
4269 = NOR(4217, 1005)
4273 = NOR(4152, 4220)
4274 = NOR(4220, 1053)
4275 = NOR(4034, 4220)
4278 = NOR(4224, 4225)
4281 = NOR(4229, 4226)
4285 = NOR(4164, 4232)
4286 = NOR(4232, 4161)
4287 = NOR(4236, 4237)
4290 = NOR(4238, 1248)
4294 = NOR(4242, 4175)
4298 = NOR(4245, 4180)
4302 = NOR(4248, 4185)
4306 = NOR(4251, 4190)
4310 = NOR(4254, 4195)
4314 = NOR(4257, 4200)
4318 = NOR(4208, 4260)
4319 = NOR(4260, 4205)
4320 = NOR(4264, 4265)
4323 = NOR(4266, 957)
4327 = NOR(4217, 4269)
4328 = NOR(4269, 1005)
4329 = NOR(4085, 4269)
4332 = NOR(4273, 4274)
4335 = NOR(4278, 4275)
4339 = NOR(4229, 4281)
4340 = NOR(4281, 4226)
4341 = NOR(4285, 4286)
4344 = NOR(4287, 1200)
4348 = NOR(4238, 4290)
4349 = NOR(4290, 1248)
4350 = NOR(4106, 4290)
4353 = NOR(4242, 4294)
4354 = NOR(4294, 4175)
4355 = NOR(4245, 4298)
4356 = NOR(4298, 4180)
4357 = NOR(4248, 4302)
4358 = NOR(4302, 4185)
4359 = NOR(4251, 4306)
4360 = NOR(4306, 4190)
4361 = NOR(4254, 4310)
4362 = NOR(4310, 4195)
4363 = NOR(4257, 4314)
4364 = NOR(4314, 4200)
4365 = NOR(4318, 4319)
4368 = NOR(4320, 909)
4372 = NOR(4266, 4323)
4373 = NOR(4323, 957)
4374 = NOR(4146, 4323)
4377 = NOR(4327, 4328)
4380 = NOR(4332, 4329)
4384 = NOR(4278, 4335)
4385 = NOR(4335, 4275)
4386 = NOR(4339, 4340)
4389 = NOR(4341, 1152)
4393 = NOR(4287, 4344)
4394 = NOR(4344, 1200)
4395 = NOR(4167, 4344)
4398 = NOR(4348, 4349)
4401 = NOR(1296, 4350)
4405 = NOR(4353, 4354)
4408 = NOR(4355, 4356)
4411 = NOR(4357, 4358)
4414 = NOR(4359, 4360)
4417 = NOR(4361, 4362)
4420 = NOR(4363, 4364)
4423 = NOR(4365, 861)
4427 = NOR(4320, 4368)
4428 = NOR(4368, 909)
4429 = NOR(4211, 4368)
4432 = NOR(4372, 4373)
4435 = NOR(4377, 4374)
4439 = NOR(4332, 4380)
4440 = NOR(4380, 4329)
4441 = NOR(4384, 4385)
4444 = NOR(4386, 1104)
4448 = NOR(4341, 4389)
4449 = NOR(4389, 1152)
4450 = NOR(4232, 4389)
4453 = NOR(4393, 4394)
4456 = NOR(4398, 4395)
4460 = NOR(1296, 4401)
4461 = NOR(4401, 4350)
4462 = NOR(4405, 573)
4466 = NOR(4408, 621)
4470 = NOR(4411, 669)
4474 = NOR(4414, 717)
4478 = NOR(4417, 765)
4482 = NOR(4420, 813)
4486 = NOR(4365, 4423)
4487 = NOR(4423, 861)
4488 = NOR(4260, 4423)
4491 = NOR(4427, 4428)
4494 = NOR(4432, 4429)
4498 = NOR(4377, 4435)
4499 = NOR(4435, 4374)
4500 = NOR(4439, 4440)
4503 = NOR(4441, 1056)
4507 = NOR(4386, 4444)
4508 = NOR(4444, 1104)
4509 = NOR(4281, 4444)
4512 = NOR(4448, 4449)
4515 = NOR(4453, 4450)
4519 = NOR(4398, 4456)
4520 = NOR(4456, 4395)
4521 = NOR(4460, 4461)
4524 = NOR(4405, 4462)
4525 = NOR(4462, 573)
4526 = NOR(4294, 4462)
4529 = NOR(4408, 4466)
4530 = NOR(4466, 621)
4531 = NOR(4298, 4466)
4534 = NOR(4411, 4470)
4535 = NOR(4470, 669)
4536 = NOR(4302, 4470)
4539 = NOR(4414, 4474)
4540 = NOR(4474, 717)
4541 = NOR(4306, 4474)
4544 = NOR(4417, 4478)
4545 = NOR(4478, 765)
4546 = NOR(4310, 4478)
4549 = NOR(4420, 4482)
4550 = NOR(4482, 813)
4551 = NOR(4314, 4482)
4554 = NOR(4486, 4487)
4557 = NOR(4491, 4488)
4561 = NOR(4432, 4494)
4562 = NOR(4494, 4429)
4563 = NOR(4498, 4499)
4566 = NOR(4500, 1008)
4570 = NOR(4441, 4503)
4571 = NOR(4503, 1056)
4572 = NOR(4335, 4503)
4575 = NOR(4507, 4508)
4578 = NOR(4512, 4509)
4582 = NOR(4453, 4515)
4583 = NOR(4515, 4450)
4584 = NOR(4519, 4520)
4587 = NOR(4521, 1251)
4591 = NOR(4524, 4525)
4592 = NOR(4529, 4530)
4595 = NOR(4534, 4535)
4598 = NOR(4539, 4540)
4601 = NOR(4544, 4545)
4604 = NOR(4549, 4550)
4607 = NOR(4554, 4551)
4611 = NOR(4491, 4557)
4612 = NOR(4557, 4488)
4613 = NOR(4561, 4562)
4616 = NOR(4563, 960)
4620 = NOR(4500, 4566)
4621 = NOR(4566, 1008)
4622 = NOR(4380, 4566)
4625 = NOR(4570, 4571)
4628 = NOR(4575, 4572)
4632 = NOR(4512, 4578)
4633 = NOR(4578, 4509)
4634 = NOR(4582, 4583)
4637 = NOR(4584, 1203)
4641 = NOR(4521, 4587)
4642 = NOR(4587, 1251)
4643 = NOR(4401, 4587)
4646 = NOR(4592, 4526)
4650 = NOR(4595, 4531)
4654 = NOR(4598, 4536)
4658 = NOR(4601, 4541)
4662 = NOR(4604, 4546)
4666 = NOR(4554, 4607)
4667 = NOR(4607, 4551)
4668 = NOR(4611, 4612)
4671 = NOR(4613, 912)
4675 = NOR(4563, 4616)
4676 = NOR(4616, 960)
4677 = NOR(4435, 4616)
4680 = NOR(4620, 4621)
4683 = NOR(4625, 4622)
4687 = NOR(4575, 4628)
4688 = NOR(4628, 4572)
4689 = NOR(4632, 4633)
4692 = NOR(4634, 1155)
4696 = NOR(4584, 4637)
4697 = NOR(4637, 1203)
4698 = NOR(4456, 4637)
4701 = NOR(4641, 4642)
4704 = NOR(1299, 4643)
4708 = NOR(4592, 4646)
4709 = NOR(4646, 4526)
4710 = NOR(4595, 4650)
4711 = NOR(4650, 4531)
4712 = NOR(4598, 4654)
4713 = NOR(4654, 4536)
4714 = NOR(4601, 4658)
4715 = NOR(4658, 4541)
4716 = NOR(4604, 4662)
4717 = NOR(4662, 4546)
4718 = NOR(4666, 4667)
4721 = NOR(4668, 864)
4725 = NOR(4613, 4671)
4726 = NOR(4671, 912)
4727 = NOR(4494, 4671)
4730 = NOR(4675, 4676)
4733 = NOR(4680, 4677)
4737 = NOR(4625, 4683)
4738 = NOR(4683, 4622)
4739 = NOR(4687, 4688)
4742 = NOR(4689, 1107)
4746 = NOR(4634, 4692)
4747 = NOR(4692, 1155)
4748 = NOR(4515, 4692)
4751 = NOR(4696, 4697)
4754 = NOR(4701, 4698)
4758 = NOR(1299, 4704)
4759 = NOR(4704, 4643)
4760 = NOR(4708, 4709)
4763 = NOR(4710, 4711)
4766 = NOR(4712, 4713)
4769 = NOR(4714, 4715)
4772 = NOR(4716, 4717)
4775 = NOR(4718, 816)
4779 = NOR(4668, 4721)
4780 = NOR(4721, 864)
4781 = NOR(4557, 4721)
4784 = NOR(4725, 4726)
4787 = NOR(4730, 4727)
4791 = NOR(4680, 4733)
4792 = NOR(4733, 4677)
4793 = NOR(4737, 4738)
4796 = NOR(4739, 1059)
4800 = NOR(4689, 4742)
4801 = NOR(4742, 1107)
4802 = NOR(4578, 4742)
4805 = NOR(4746, 4747)
4808 = NOR(4751, 4748)
4812 = NOR(4701, 4754)
4813 = NOR(4754, 4698)
4814 = NOR(4758, 4759)
4817 = NOR(4760, 576)
4821 = NOR(4763, 624)
4825 = NOR(4766, 672)
4829 = NOR(4769, 720)
4833 = NOR(4772, 768)
4837 = NOR(4718, 4775)
4838 = NOR(4775, 816)
4839 = NOR(4607, 4775)
4842 = NOR(4779, 4780)
4845 = NOR(4784, 4781)
4849 = NOR(4730, 4787)
4850 = NOR(4787, 4727)
4851 = NOR(4791, 4792)
4854 = NOR(4793, 1011)
4858 = NOR(4739, 4796)
4859 = NOR(4796, 1059)
4860 = NOR(4628, 4796)
4863 = NOR(4800, 4801)
4866 = NOR(4805, 4802)
4870 = NOR(4751, 4808)
4871 = NOR(4808, 4748)
4872 = NOR(4812, 4813)
4875 = NOR(4814, 1254)
4879 = NOR(4760, 4817)
4880 = NOR(4817, 576)
4881 = NOR(4646, 4817)
4884 = NOR(4763, 4821)
4885 = NOR(4821, 624)
4886 = NOR(4650, 4821)
4889 = NOR(4766, 4825)
4890 = NOR(4825, 672)
4891 = NOR(4654, 4825)
4894 = NOR(4769, 4829)
4895 = NOR(4829, 720)
4896 = NOR(4658, 4829)
4899 = NOR(4772, 4833)
4900 = NOR(4833, 768)
4901 = NOR(4662, 4833)
4904 = NOR(4837, 4838)
4907 = NOR(4842, 4839)
4911 = NOR(4784, 4845)
4912 = NOR(4845, 4781)
4913 = NOR(4849, 4850)
4916 = NOR(4851, 963)
4920 = NOR(4793, 4854)
4921 = NOR(4854, 1011)
4922 = NOR(4683, 4854)
4925 = NOR(4858, 4859)
4928 = NOR(4863, 4860)
4932 = NOR(4805, 4866)
4933 = NOR(4866, 4802)
4934 = NOR(4870, 4871)
4937 = NOR(4872, 1206)
4941 = NOR(4814, 4875)
4942 = NOR(4875, 1254)
4943 = NOR(4704, 4875)
4946 = NOR(4879, 4880)
4947 = NOR(4884, 4885)
4950 = NOR(4889, 4890)
4953 = NOR(4894, 4895)
4956 = NOR(4899, 4900)
4959 = NOR(4904, 4901)
4963 = NOR(4842, 4907)
4964 = NOR(4907, 4839)
4965 = NOR(4911, 4912)
4968 = NOR(4913, 915)
4972 = NOR(4851, 4916)
4973 = NOR(4916, 963)
4974 = NOR(4733, 4916)
4977 = NOR(4920, 4921)
4980 = NOR(4925, 4922)
4984 = NOR(4863, 4928)
4985 = NOR(4928, 4860)
4986 = NOR(4932, 4933)
4989 = NOR(4934, 1158)
4993 = NOR(4872, 4937)
4994 = NOR(4937, 1206)
4995 = NOR(4754, 4937)
4998 = NOR(4941, 4942)
5001 = NOR(1302, 4943)
5005 = NOR(4947, 4881)
5009 = NOR(4950, 4886)
5013 = NOR(4953, 4891)
5017 = NOR(4956, 4896)
5021 = NOR(4904, 4959)
5022 = NOR(4959, 4901)
5023 = NOR(4963, 4964)
5026 = NOR(4965, 867)
5030 = NOR(4913, 4968)
5031 = NOR(4968, 915)
5032 = NOR(4787, 4968)
5035 = NOR(4972, 4973)
5038 = NOR(4977, 4974)
5042 = NOR(4925, 4980)
5043 = NOR(4980, 4922)
5044 = NOR(4984, 4985)
5047 = NOR(4986, 1110)
5051 = NOR(4934, 4989)
5052 = NOR(4989, 1158)
5053 = NOR(4808, 4989)
5056 = NOR(4993, 4994)
5059 = NOR(4998, 4995)
5063 = NOR(1302, 5001)
5064 = NOR(5001, 4943)
5065 = NOR(4947, 5005)
5066 = NOR(5005, 4881)
5067 = NOR(4950, 5009)
5068 = NOR(5009, 4886)
5069 = NOR(4953, 5013)
5070 = NOR(5013, 4891)
5071 = NOR(4956, 5017)
5072 = NOR(5017, 4896)
5073 = NOR(5021, 5022)
5076 = NOR(5023, 819)
5080 = NOR(4965, 5026)
5081 = NOR(5026, 867)
5082 = NOR(4845, 5026)
5085 = NOR(5030, 5031)
5088 = NOR(5035, 5032)
5092 = NOR(4977, 5038)
5093 = NOR(5038, 4974)
5094 = NOR(5042, 5043)
5097 = NOR(5044, 1062)
5101 = NOR(4986, 5047)
5102 = NOR(5047, 1110)
5103 = NOR(4866, 5047)
5106 = NOR(5051, 5052)
5109 = NOR(5056, 5053)
5113 = NOR(4998, 5059)
5114 = NOR(5059, 4995)
5115 = NOR(5063, 5064)
5118 = NOR(5065, 5066)
5121 = NOR(5067, 5068)
5124 = NOR(5069, 5070)
5127 = NOR(5071, 5072)
5130 = NOR(5073, 771)
5134 = NOR(5023, 5076)
5135 = NOR(5076, 819)
5136 = NOR(4907, 5076)
5139 = NOR(5080, 5081)
5142 = NOR(5085, 5082)
5146 = NOR(5035, 5088)
5147 = NOR(5088, 5032)
5148 = NOR(5092, 5093)
5151 = NOR(5094, 1014)
5155 = NOR(5044, 5097)
5156 = NOR(5097, 1062)
5157 = NOR(4928, 5097)
5160 = NOR(5101, 5102)
5163 = NOR(5106, 5103)
5167 = NOR(5056, 5109)
5168 = NOR(5109, 5053)
5169 = NOR(5113, 5114)
5172 = NOR(5115, 1257)
5176 = NOR(5118, 579)
5180 = NOR(5121, 627)
5184 = NOR(5124, 675)
5188 = NOR(5127, 723)
5192 = NOR(5073, 5130)
5193 = NOR(5130, 771)
5194 = NOR(4959, 5130)
5197 = NOR(5134, 5135)
5200 = NOR(5139, 5136)
5204 = NOR(5085, 5142)
5205 = NOR(5142, 5082)
5206 = NOR(5146, 5147)
5209 = NOR(5148, 966)
5213 = NOR(5094, 5151)
5214 = NOR(5151, 1014)
5215 = NOR(4980, 5151)
5218 = NOR(5155, 5156)
5221 = NOR(5160, 5157)
5225 = NOR(5106, 5163)
5226 = NOR(5163, 5103)
5227 = NOR(5167, 5168)
5230 = NOR(5169, 1209)
5234 = NOR(5115, 5172)
5235 = NOR(5172, 1257)
5236 = NOR(5001, 5172)
5239 = NOR(5118, 5176)
5240 = NOR(5176, 579)
5241 = NOR(5005, 5176)
5244 = NOR(5121, 5180)
5245 = NOR(5180, 627)
5246 = NOR(5009, 5180)
5249 = NOR(5124, 5184)
5250 = NOR(5184, 675)
5251 = NOR(5013, 5184)
5254 = NOR(5127, 5188)
5255 = NOR(5188, 723)
5256 = NOR(5017, 5188)
5259 = NOR(5192, 5193)
5262 = NOR(5197, 5194)
5266 = NOR(5139, 5200)
5267 = NOR(5200, 5136)
5268 = NOR(5204, 5205)
5271 = NOR(5206, 918)
5275 = NOR(5148, 5209)
5276 = NOR(5209, 966)
5277 = NOR(5038, 5209)
5280 = NOR(5213, 5214)
5283 = NOR(5218, 5215)
5287 = NOR(5160, 5221)
5288 = NOR(5221, 5157)
5289 = NOR(5225, 5226)
5292 = NOR(5227, 1161)
5296 = NOR(5169, 5230)
5297 = NOR(5230, 1209)
5298 = NOR(5059, 5230)
5301 = NOR(5234, 5235)
5304 = NOR(1305, 5236)
5308 = NOR(5239, 5240)
5309 = NOR(5244, 5245)
5312 = NOR(5249, 5250)
5315 = NOR(5254, 5255)
5318 = NOR(5259, 5256)
5322 = NOR(5197, 5262)
5323 = NOR(5262, 5194)
5324 = NOR(5266, 5267)
5327 = NOR(5268, 870)
5331 = NOR(5206, 5271)
5332 = NOR(5271, 918)
5333 = NOR(5088, 5271)
5336 = NOR(5275, 5276)
5339 = NOR(5280, 5277)
5343 = NOR(5218, 5283)
5344 = NOR(5283, 5215)
5345 = NOR(5287, 5288)
5348 = NOR(5289, 1113)
5352 = NOR(5227, 5292)
5353 = NOR(5292, 1161)
5354 = NOR(5109, 5292)
5357 = NOR(5296, 5297)
5360 = NOR(5301, 5298)
5364 = NOR(1305, 5304)
5365 = NOR(5304, 5236)
5366 = NOR(5309, 5241)
5370 = NOR(5312, 5246)
5374 = NOR(5315, 5251)
5378 = NOR(5259, 5318)
5379 = NOR(5318, 5256)
5380 = NOR(5322, 5323)
5383 = NOR(5324, 822)
5387 = NOR(5268, 5327)
5388 = NOR(5327, 870)
5389 = NOR(5142, 5327)
5392 = NOR(5331, 5332)
5395 = NOR(5336, 5333)
5399 = NOR(5280, 5339)
5400 = NOR(5339, 5277)
5401 = NOR(5343, 5344)
5404 = NOR(5345, 1065)
5408 = NOR(5289, 5348)
5409 = NOR(5348, 1113)
5410 = NOR(5163, 5348)
5413 = NOR(5352, 5353)
5416 = NOR(5357, 5354)
5420 = NOR(5301, 5360)
5421 = NOR(5360, 5298)
5422 = NOR(5364, 5365)
5425 = NOR(5309, 5366)
5426 = NOR(5366, 5241)
5427 = NOR(5312, 5370)
5428 = NOR(5370, 5246)
5429 = NOR(5315, 5374)
5430 = NOR(5374, 5251)
5431 = NOR(5378, 5379)
5434 = NOR(5380, 774)
5438 = NOR(5324, 5383)
5439 = NOR(5383, 822)
5440 = NOR(5200, 5383)
5443 = NOR(5387, 5388)
5446 = NOR(5392, 5389)
5450 = NOR(5336, 5395)
5451 = NOR(5395, 5333)
5452 = NOR(5399, 5400)
5455 = NOR(5401, 1017)
5459 = NOR(5345, 5404)
5460 = NOR(5404, 1065)
5461 = NOR(5221, 5404)
5464 = NOR(5408, 5409)
5467 = NOR(5413, 5410)
5471 = NOR(5357, 5416)
5472 = NOR(5416, 5354)
5473 = NOR(5420, 5421)
5476 = NOR(5422, 1260)
5480 = NOR(5425, 5426)
5483 = NOR(5427, 5428)
5486 = NOR(5429, 5430)
5489 = NOR(5431, 726)
5493 = NOR(5380, 5434)
5494 = NOR(5434, 774)
5495 = NOR(5262, 5434)
5498 = NOR(5438, 5439)
5501 = NOR(5443, 5440)
5505 = NOR(5392, 5446)
5506 = NOR(5446, 5389)
5507 = NOR(5450, 5451)
5510 = NOR(5452, 969)
5514 = NOR(5401, 5455)
5515 = NOR(5455, 1017)
5516 = NOR(5283, 5455)
5519 = NOR(5459, 5460)
5522 = NOR(5464, 5461)
5526 = NOR(5413, 5467)
5527 = NOR(5467, 5410)
5528 = NOR(5471, 5472)
5531 = NOR(5473, 1212)
5535 = NOR(5422, 5476)
5536 = NOR(5476, 1260)
5537 = NOR(5304, 5476)
5540 = NOR(5480, 582)
5544 = NOR(5483, 630)
5548 = NOR(5486, 678)
5552 = NOR(5431, 5489)
5553 = NOR(5489, 726)
5554 = NOR(5318, 5489)
5557 = NOR(5493, 5494)
5560 = NOR(5498, 5495)
5564 = NOR(5443, 5501)
5565 = NOR(5501, 5440)
5566 = NOR(5505, 5506)
5569 = NOR(5507, 921)
5573 = NOR(5452, 5510)
5574 = NOR(5510, 969)
5575 = NOR(5339, 5510)
5578 = NOR(5514, 5515)
5581 = NOR(5519, 5516)
5585 = NOR(5464, 5522)
5586 = NOR(5522, 5461)
5587 = NOR(5526, 5527)
5590 = NOR(5528, 1164)
5594 = NOR(5473, 5531)
5595 = NOR(5531, 1212)
5596 = NOR(5360, 5531)
5599 = NOR(5535, 5536)
5602 = NOR(1308, 5537)
5606 = NOR(5480, 5540)
5607 = NOR(5540, 582)
5608 = NOR(5366, 5540)
5611 = NOR(5483, 5544)
5612 = NOR(5544, 630)
5613 = NOR(5370, 5544)
5616 = NOR(5486, 5548)
5617 = NOR(5548, 678)
5618 = NOR(5374, 5548)
5621 = NOR(5552, 5553)
5624 = NOR(5557, 5554)
5628 = NOR(5498, 5560)
5629 = NOR(5560, 5495)
5630 = NOR(5564, 5565)
5633 = NOR(5566, 873)
5637 = NOR(5507, 5569)
5638 = NOR(5569, 921)
5639 = NOR(5395, 5569)
5642 = NOR(5573, 5574)
5645 = NOR(5578, 5575)
5649 = NOR(5519, 5581)
5650 = NOR(5581, 5516)
5651 = NOR(5585, 5586)
5654 = NOR(5587, 1116)
5658 = NOR(5528, 5590)
5659 = NOR(5590, 1164)
5660 = NOR(5416, 5590)
5663 = NOR(5594, 5595)
5666 = NOR(5599, 5596)
5670 = NOR(1308, 5602)
5671 = NOR(5602, 5537)
5672 = NOR(5606, 5607)
5673 = NOR(5611, 5612)
5676 = NOR(5616, 5617)
5679 = NOR(5621, 5618)
5683 = NOR(5557, 5624)
5684 = NOR(5624, 5554)
5685 = NOR(5628, 5629)
5688 = NOR(5630, 825)
5692 = NOR(5566, 5633)
5693 = NOR(5633, 873)
5694 = NOR(5446, 5633)
5697 = NOR(5637, 5638)
5700 = NOR(5642, 5639)
5704 = NOR(5578, 5645)
5705 = NOR(5645, 5575)
5706 = NOR(5649, 5650)
5709 = NOR(5651, 1068)
5713 = NOR(5587, 5654)
5714 = NOR(5654, 1116)
5715 = NOR(5467, 5654)
5718 = NOR(5658, 5659)
5721 = NOR(5663, 5660)
5725 = NOR(5599, 5666)
5726 = NOR(5666, 5596)
5727 = NOR(5670, 5671)
5730 = NOR(5673, 5608)
5734 = NOR(5676, 5613)
5738 = NOR(5621, 5679)
5739 = NOR(5679, 5618)
5740 = NOR(5683, 5684)
5743 = NOR(5685, 777)
5747 = NOR(5630, 5688)
5748 = NOR(5688, 825)
5749 = NOR(5501, 5688)
5752 = NOR(5692, 5693)
5755 = NOR(5697, 5694)
5759 = NOR(5642, 5700)
5760 = NOR(5700, 5639)
5761 = NOR(5704, 5705)
5764 = NOR(5706, 1020)
5768 = NOR(5651, 5709)
5769 = NOR(5709, 1068)
5770 = NOR(5522, 5709)
5773 = NOR(5713, 5714)
5776 = NOR(5718, 5715)
5780 = NOR(5663, 5721)
5781 = NOR(5721, 5660)
5782 = NOR(5725, 5726)
5785 = NOR(5673, 5730)
5786 = NOR(5730, 5608)
5787 = NOR(5676, 5734)
5788 = NOR(5734, 5613)
5789 = NOR(5738, 5739)
5792 = NOR(5740, 729)
5796 = NOR(5685, 5743)
5797 = NOR(5743, 777)
5798 = NOR(5560, 5743)
5801 = NOR(5747, 5748)
5804 = NOR(5752, 5749)
5808 = NOR(5697, 5755)
5809 = NOR(5755, 5694)
5810 = NOR(5759, 5760)
5813 = NOR(5761, 972)
5817 = NOR(5706, 5764)
5818 = NOR(5764, 1020)
5819 = NOR(5581, 5764)
5822 = NOR(5768, 5769)
5825 = NOR(5773, 5770)
5829 = NOR(5718, 5776)
5830 = NOR(5776, 5715)
5831 = NOR(5780, 5781)
5834 = NOR(5785, 5786)
5837 = NOR(5787, 5788)
5840 = NOR(5789, 681)
5844 = NOR(5740, 5792)
5845 = NOR(5792, 729)
5846 = NOR(5624, 5792)
5849 = NOR(5796, 5797)
5852 = NOR(5801, 5798)
5856 = NOR(5752, 5804)
5857 = NOR(5804, 5749)
5858 = NOR(5808, 5809)
5861 = NOR(5810, 924)
5865 = NOR(5761, 5813)
5866 = NOR(5813, 972)
5867 = NOR(5645, 5813)
5870 = NOR(5817, 5818)
5873 = NOR(5822, 5819)
5877 = NOR(5773, 5825)
5878 = NOR(5825, 5770)
5879 = NOR(5829, 5830)
5882 = NOR(5834, 585)
5886 = NOR(5837, 633)
5890 = NOR(5789, 5840)
5891 = NOR(5840, 681)
5892 = NOR(5679, 5840)
5895 = NOR(5844, 5845)
5898 = NOR(5849, 5846)
5902 = NOR(5801, 5852)
5903 = NOR(5852, 5798)
5904 = NOR(5856, 5857)
5907 = NOR(5858, 876)
5911 = NOR(5810, 5861)
5912 = NOR(5861, 924)
5913 = NOR(5700, 5861)
5916 = NOR(5865, 5866)
5919 = NOR(5870, 5867)
5923 = NOR(5822, 5873)
5924 = NOR(5873, 5819)
5925 = NOR(5877, 5878)
5928 = NOR(5834, 5882)
5929 = NOR(5882, 585)
5930 = NOR(5730, 5882)
5933 = NOR(5837, 5886)
5934 = NOR(5886, 633)
5935 = NOR(5734, 5886)
5938 = NOR(5890, 5891)
5941 = NOR(5895, 5892)
5945 = NOR(5849, 5898)
5946 = NOR(5898, 5846)
5947 = NOR(5902, 5903)
5950 = NOR(5904, 828)
5954 = NOR(5858, 5907)
5955 = NOR(5907, 876)
5956 = NOR(5755, 5907)
5959 = NOR(5911, 5912)
5962 = NOR(5916, 5913)
5966 = NOR(5870, 5919)
5967 = NOR(5919, 5867)
5968 = NOR(5923, 5924)
5971 = NOR(5928, 5929)
5972 = NOR(5933, 5934)
5975 = NOR(5938, 5935)
5979 = NOR(5895, 5941)
5980 = NOR(5941, 5892)
5981 = NOR(5945, 5946)
5984 = NOR(5947, 780)
5988 = NOR(5904, 5950)
5989 = NOR(5950, 828)
5990 = NOR(5804, 5950)
5993 = NOR(5954, 5955)
5996 = NOR(5959, 5956)
6000 = NOR(5916, 5962)
6001 = NOR(5962, 5913)
6002 = NOR(5966, 5967)
6005 = NOR(5972, 5930)
6009 = NOR(5938, 5975)
6010 = NOR(5975, 5935)
6011 = NOR(5979, 5980)
6014 = NOR(5981, 732)
6018 = NOR(5947, 5984)
6019 = NOR(5984, 780)
6020 = NOR(5852, 5984)
6023 = NOR(5988, 5989)
6026 = NOR(5993, 5990)
6030 = NOR(5959, 5996)
6031 = NOR(5996, 5956)
6032 = NOR(6000, 6001)
6035 = NOR(5972, 6005)
6036 = NOR(6005, 5930)
6037 = NOR(6009, 6010)
6040 = NOR(6011, 684)
6044 = NOR(5981, 6014)
6045 = NOR(6014, 732)
6046 = NOR(5898, 6014)
6049 = NOR(6018, 6019)
6052 = NOR(6023, 6020)
6056 = NOR(5993, 6026)
6057 = NOR(6026, 5990)
6058 = NOR(6030, 6031)
6061 = NOR(6035, 6036)
6064 = NOR(6037, 636)
6068 = NOR(6011, 6040)
6069 = NOR(6040, 684)
6070 = NOR(5941, 6040)
6073 = NOR(6044, 6045)
6076 = NOR(6049, 6046)
6080 = NOR(6023, 6052)
6081 = NOR(6052, 6020)
6082 = NOR(6056, 6057)
6085 = NOR(6061, 588)
6089 = NOR(6037, 6064)
6090 = NOR(6064, 636)
6091 = NOR(5975, 6064)
6094 = NOR(6068, 6069)
6097 = NOR(6073, 6070)
6101 = NOR(6049, 6076)
6102 = NOR(6076, 6046)
6103 = NOR(6080, 6081)
6106 = NOR(6061, 6085)
6107 = NOR(6085, 588)
6108 = NOR(6005, 6085)
6111 = NOR(6089, 6090)
6114 = NOR(6094, 6091)
6118 = NOR(6073, 6097)
6119 = NOR(6097, 6070)
6120 = NOR(6101, 6102)
6123 = NOR(6106, 6107)
6124 = NOR(6111, 6108)
6128 = NOR(6094, 6114)
6129 = NOR(6114, 6091)
6130 = NOR(6118, 6119)
6133 = NOR(6111, 6124)
6134 = NOR(6124, 6108)
6135 = NOR(6128, 6129)
6138 = NOR(6133, 6134)
6141 = NOT(6138)
6145 = NOR(6138, 6141)
6146 = NOT(6141)
6147 = NOR(6124, 6141)
6150 = NOR(6145, 6146)
6151 = NOR(6135, 6147)
6155 = NOR(6135, 6151)
6156 = NOR(6151, 6147)
6157 = NOR(6114, 6151)
6160 = NOR(6155, 6156)
6161 = NOR(6130, 6157)
6165 = NOR(6130, 6161)
6166 = NOR(6161, 6157)
6167 = NOR(6097, 6161)
6170 = NOR(6165, 6166)
6171 = NOR(6120, 6167)
6175 = NOR(6120, 6171)
6176 = NOR(6171, 6167)
6177 = NOR(6076, 6171)
6180 = NOR(6175, 6176)
6181 = NOR(6103, 6177)
6185 = NOR(6103, 6181)
6186 = NOR(6181, 6177)
6187 = NOR(6052, 6181)
6190 = NOR(6185, 6186)
6191 = NOR(6082, 6187)
6195 = NOR(6082, 6191)
6196 = NOR(6191, 6187)
6197 = NOR(6026, 6191)
6200 = NOR(6195, 6196)
6201 = NOR(6058, 6197)
6205 = NOR(6058, 6201)
6206 = NOR(6201, 6197)
6207 = NOR(5996, 6201)
6210 = NOR(6205, 6206)
6211 = NOR(6032, 6207)
6215 = NOR(6032, 6211)
6216 = NOR(6211, 6207)
6217 = NOR(5962, 6211)
6220 = NOR(6215, 6216)
6221 = NOR(6002, 6217)
6225 = NOR(6002, 6221)
6226 = NOR(6221, 6217)
6227 = NOR(5919, 6221)
6230 = NOR(6225, 6226)
6231 = NOR(5968, 6227)
6235 = NOR(5968, 6231)
6236 = NOR(6231, 6227)
6237 = NOR(5873, 6231)
6240 = NOR(6235, 6236)
6241 = NOR(5925, 6237)
6245 = NOR(5925, 6241)
6246 = NOR(6241, 6237)
6247 = NOR(5825, 6241)
6250 = NOR(6245, 6246)
6251 = NOR(5879, 6247)
6255 = NOR(5879, 6251)
6256 = NOR(6251, 6247)
6257 = NOR(5776, 6251)
6260 = NOR(6255, 6256)
6261 = NOR(5831, 6257)
6265 = NOR(5831, 6261)
6266 = NOR(6261, 6257)
6267 = NOR(5721, 6261)
6270 = NOR(6265, 6266)
6271 = NOR(5782, 6267)
6275 = NOR(5782, 6271)
6276 = NOR(6271, 6267)
6277 = NOR(5666, 6271)
6280 = NOR(6275, 6276)
6281 = NOR(5727, 6277)
6285 = NOR(5727, 6281)
6286 = NOR(6281, 6277)
6287 = NOR(5602, 6281)
6288 = NOR(6285, 6286)