noconvergence.tmp.cnf

人工智能的一个重要方法

p cnf 3000 13500
1509 -336 -2107 0
973 -130 1157 0
444 1616 -1311 0
1413 179 -2500 0
-649 2351 1410 0
1061 42 1842 0
2956 548 820 0
2293 1745 330 0
2984 1996 -306 0
1714 -2572 -2464 0
373 -2518 820 0
-2933 -63 311 0
582 -1121 895 0
-1065 -2018 -852 0
2492 2344 587 0
-75 -663 -246 0
-1530 -1509 500 0
-979 -521 1572 0
2279 -2761 -2388 0
884 105 -2309 0
1128 972 -1675 0
-1539 -1285 2505 0
-1636 2235 77 0
1801 1499 770 0
-2762 2802 1148 0
329 382 20 0
289 -101 2279 0
-1762 -1189 -237 0
754 -2454 2932 0
-2829 1242 -1402 0
1782 -2530 2678 0
2021 -1165 -854 0
-1908 2328 227 0
122 1566 -2556 0
1015 -1242 1041 0
1233 -551 2037 0
-2718 -1094 46 0
679 -823 2400 0
2550 903 2191 0
907 1592 -1787 0
1910 128 1100 0
1648 2682 -1120 0
-185 -823 2512 0
2834 -2366 599 0
-2688 -156 304 0
-2270 843 1900 0
381 1515 -2972 0
-2908 -2992 -2156 0
-809 -677 1266 0
-1982 -1286 191 0
2053 1462 2480 0
1495 -2276 1021 0
-2607 1580 -2446 0
1039 -863 914 0
1816 -247 -20 0
-2563 -958 -206 0
2350 -10 1145 0
-291 -2472 -768 0
815 -1015 1542 0
2373 -1850 -191 0
-614 -974 1357 0
-853 238 -204 0
460 2423 813 0
1961 1730 651 0
218 721 -1457 0
-617 -1587 1086 0
-2121 -1837 -1944 0
-1494 -680 1612 0
-162 -1369 1402 0
-699 -1196 -328 0
-2080 81 -2339 0
-711 -1670 2716 0
-2065 -2019 2695 0
290 -1872 1432 0
1429 -2904 -1566 0
-1397 969 -1485 0
-1524 -947 -449 0
-2613 -516 2376 0
940 2602 2077 0
1503 1989 -2125 0
2953 2859 1973 0
1707 -845 515 0
-796 -2346 -779 0
1964 -1652 230 0
-2819 -343 784 0
2448 2479 1827 0
-1998 -2746 66 0
2698 -719 -894 0
1598 -59 2757 0
1951 -2218 2162 0
2719 -1141 -2371 0
-338 -377 -2592 0
-1192 2793 -756 0
-1749 -2177 499 0
-541 -931 -2811 0
2045 -1357 -168 0
626 -950 1066 0
2303 -2719 -1847 0
-2001 1637 1971 0
950 -1786 1017 0
219 1412 1653 0
-2447 -1337 -1819 0
1218 -1100 98 0
-1483 -2634 -1188 0
-154 2834 -672 0
-2316 183 -1239 0
-1147 -585 -1254 0
792 -419 -1579 0
-1866 1663 2010 0
1859 -2621 1864 0
-1166 1484 68 0
-2048 -2419 -2713 0
2337 4 -2465 0
2795 1092 2159 0
1834 -1878 2522 0
2050 1942 979 0
808 -1745 1241 0
-2821 554 -2776 0
10 -474 -1836 0
2354 46 2012 0
-1496 1961 -1107 0
-738 -1241 -1016 0
1352 1929 -2615 0
2825 603 -1951 0
-1131 503 1683 0
-1582 -584 -1602 0
-1824 364 -2643 0
1905 -689 2728 0
-656 2633 -1914 0
-433 -410 -101 0
-954 177 1537 0
1520 -1759 -267 0
-1598 -2291 -507 0
1195 -958 1241 0
874 -1656 -2385 0
-2527 -109 -1848 0
1144 1497 1339 0
2837 2065 -2605 0
621 2938 -2676 0
2656 2951 1015 0
1770 -5 -2472 0
2012 -2584 1060 0
-460 -1885 -1540 0
2829 1350 1685 0
2421 391 -365 0
144 -2163 -2569 0
1184 -1566 -2327 0
-854 765 -120 0
-1585 1930 2620 0
1907 -84 2260 0
-864 1054 -2025 0
2413 672 1577 0
2097 1029 -482 0
-2104 -1398 2316 0
1457 2044 -739 0
738 1883 717 0
2658 672 2820 0
-2304 -2560 1229 0
-331 2758 -572 0
-1067 1101 2587 0
-2718 1432 -1054 0
-2201 1581 1149 0
395 -1644 -1944 0
-1458 -1501 988 0
743 -1996 -1360 0
834 51 -860 0
2937 482 -436 0
-2812 604 2800 0
-2422 648 2746 0
359 1666 1185 0
-1127 208 1010 0
-1792 2687 2737 0
693 144 -697 0
838 -1147 2979 0
-880 -2054 473 0
698 -1955 -2557 0
-52 1888 534 0
939 -1425 648 0
1547 1877 -2917 0
1151 -793 -2959 0
-2639 2697 1071 0
371 -2162 987 0
-2382 811 2141 0
-2501 -2451 2787 0
2373 -212 -1845 0
-2242 -2810 -2515 0
374 494 -1670 0
2108 2918 124 0
-564 2981 -830 0
-2524 -1653 -169 0
1809 -2349 -2631 0
2671 -434 -664 0
-333 2233 2161 0
1966 2383 -1170 0
-2636 -2237 2831 0
235 1317 -284 0
-1488 499 184 0
1409 688 2988 0
1374 927 -2137 0
21 -2815 2220 0
-564 -2813 -1274 0
-581 -383 -450 0
683 -2285 939 0
2028 -2894 1049 0
611 1367 -2800 0
681 -2363 1768 0
751 2618 16 0
-1927 -2339 -1957 0
-1529 312 -1835 0
-2211 -323 -2444 0
-2530 -2506 1101 0
-1415 -2548 -524 0
-1981 780 -1556 0
950 -2386 763 0
1247 -2095 -1815 0
261 1470 -577 0
2168 -39 1966 0
-241 1355 337 0
-2860 -2556 2780 0
1058 -2404 -7 0
-191 -1526 219 0
135 -525 -112 0
1478 1665 -1142 0
1934 912 -1046 0
2400 255 2351 0
-1902 1912 312 0
1114 2730 -1541 0
572 -932 -424 0
-2025 -2683 -1326 0
-2025 -717 -1732 0
1127 -2563 353 0
-699 1721 -1570 0
-171 2154 2762 0
1312 -2377 2064 0
2356 1238 1691 0
604 1551 -264 0
-337 2723 2648 0
2444 1774 2448 0
-1655 -996 -1019 0
-2540 -2105 20 0
72 2578 -2410 0
2540 2553 1768 0
-831 2782 167 0
2602 -2426 1331 0
2413 -2396 1751 0
-686 -2502 -2860 0
2466 -1455 -317 0
1246 2326 2967 0
2578 2239 -467 0
-439 102 331 0
-883 84 -239 0
477 2725 194 0
-1974 794 -1904 0
-2019 2695 97 0
1079 -2949 1423 0
601 -2035 772 0
198 -556 -1169 0
-221 1308 -1373 0
-2749 -495 1690 0
2859 -697 -1026 0
1574 1593 2227 0
581 -1682 983 0
-1252 -2459 -2180 0
-2013 1294 269 0
2374 -1757 -198 0
-2302 -2896 -451 0
1633 1844 230 0
-1690 16 1702 0
-2579 1733 -2064 0
-2363 -1872 1736 0
393 -2221 2364 0
246 1018 1148 0
971 -857 1696 0
2540 -2416 589 0
-2121 2069 358 0
255 2385 120 0
2037 2385 2376 0
1026 1007 -1877 0
2771 -1137 -281 0
-2564 -1013 -1520 0
2295 1920 -2991 0
1355 2971 -430 0
-840 -1684 -1031 0
1679 1639 1010 0
-2809 -1912 -2114 0
2597 1965 1526 0
-561 -1320 -2092 0
2300 -936 -1411 0
-1408 -2233 -779 0
-646 -834 -1624 0
114 1225 -2118 0
-1870 2864 578 0
-2104 2244 -113 0
344 1525 533 0
43 -186 2584 0
-1634 1009 1659 0
698 2171 1613 0
1414 -546 -1791 0
-699 -627 -499 0
-447 1366 -1685 0
-1131 1752 -1895 0
-445 2052 1869 0
-1758 -519 145 0
-2085 -2971 -717 0
-1350 1567 32 0
-394 2458 1581 0
-2189 1913 -2132 0
531 -1843 618 0
-2973 -623 -1302 0
-577 -442 2954 0
1259 -2623 2262 0
-1931 995 -1546 0
1006 -2188 -402 0
1184 -2747 2560 0
29 346 1634 0
950 -1735 252 0
1527 869 2732 0
1337 -27 -2872 0
-848 50 -363 0
-23 -2573 -1881 0
2068 -2753 2679 0
-1795 961 -1377 0
2274 749 -2640 0
1534 -487 -2375 0
187 1004 1593 0
-312 -1253 200 0
-1082 1250 257 0
1761 -2327 -76 0
1514 -1123 -1480 0
2336 1120 1822 0
-880 1099 -1710 0
1745 -514 -1478 0
-2362 1275 2254 0
-947 -739 843 0
939 473 -383 0
-1327 -1891 2570 0
2933 699 989 0
-1442 -85 -1371 0
339 -765 -2668 0
-1114 2601 1720 0
-2406 773 2961 0
-1438 2364 2785 0
-2471 2706 1877 0
-435 -2166 -4 0
938 1866 -158 0
-2406 -1756 -1637 0
-30 -1422 -2316 0
-1528 1093 -511 0
-2287 -2783 2602 0
-1969 783 -1033 0
-1914 1368 -1596 0
2354 -626 -2607 0
2689 -1995 2855 0
1666 640 -265 0
-634 -2938 -1874 0
-2591 1097 2529 0
1537 2025 1511 0
-1931 2976 908 0
2855 -2172 -2309 0
-2766 2393 2672 0
-2335 1040 844 0
-118 -238 1847 0
734 1872 2710 0
-2981 -887 -121 0
-1856 -2887 -672 0
1743 1093 -713 0
1017 1082 2065 0
2447 319 -2457 0
-1284 -245 -395 0
42 1189 1474 0
1817 -1384 -2782 0
-1301 751 -1093 0
-2985 373 2708 0
-1443 -921 -1768 0
-2369 1071 -1993 0
-2778 1008 -2176 0
-1113 724 -368 0
1905 -395 2451 0
2184 -543 2746 0
-2226 1768 364 0
1452 2696 -137 0
593 1988 2974 0
-2013 -1201 222 0
1223 2015 -696 0
-374 -176 -1740 0
1061 -1645 -2339 0
-1838 2661 803 0
1464 -104 -1308 0
2927 2926 -1527 0
573 -2677 -1737 0
2340 -1005 1161 0
-1192 -2058 -2488 0
-992 -2751 2837 0
-2859 -379 -1805 0
-173 -331 -1255 0
1183 -47 1457 0
2738 998 397 0
907 -1274 -24 0
-2791 150 -194 0
2641 2456 1692 0
-541 -830 1661 0
-498 -1543 -2672 0
2049 -943 1632 0
2493 2243 -2409 0
-2330 437 1179 0
774 1760 -2871 0
1141 -1083 1696 0
905 2032 -989 0
-1065 -774 359 0
-194 2565 1737 0
-2471 -2120 2249 0
-2940 620 1495 0
2192 2275 -2842 0
-132 952 -158 0
2631 -1875 -1552 0
776 -531 2002 0
28 -1490 1951 0
2526 2929 -1391 0
277 2492 1325 0
-2309 1077 935 0
1816 1713 -1613 0
2455 923 -77 0
2235 -1251 -2842 0
-1360 104 -2411 0
-696 2163 -612 0
-1887 -2662 2569 0
-1005 2139 -69 0
-405 1656 2886 0
560 374 -455 0
-1296 2460 867 0
1897 2118 892 0
-2044 199 243 0
887 -2196 -1462 0
1240 2785 935 0
2197 2610 -2896 0
-2775 2734 -225 0
-2124 -2237 -740 0
452 -1911 -2864 0
337 832 1645 0
-438 833 1165 0
-373 -6 1400 0
-1658 1785 -384 0
2355 1474 -680 0
1043 553 -1289 0
2878 -2466 -2123 0
584 -1833 1463 0
-1832 20 -1886 0
2510 1812 -2028 0
-704 -2331 240 0
-1664 -1001 643 0
-1971 2271 -1435 0
-72 -2819 -458 0
-1045 -2039 -19 0
-2215 257 -2070 0
-2576 873 -1201 0
-1796 -1901 1092 0
-1755 -165 2758 0
-1005 2743 -1740 0
400 -553 -1992 0
2158 -922 1506 0
2237 -1368 2266 0
2615 -598 2013 0
2492 119 -1144 0
2792 -915 2099 0
1361 368 -2808 0
-978 -301 690 0
-2395 2455 867 0
1521 -369 260 0
223 -2381 -337 0
1568 647 -315 0
1381 -405 977 0
-2124 2596 -406 0
261 -1152 -815 0
1510 -2657 -1381 0
-2210 1701 -472 0
2577 -2842 379 0
-2453 -2950 1926 0
-1656 1665 -2849 0
-2100 -2382 -1687 0
-556 -1358 -2039 0
1503 1949 1702 0
-687 497 2870 0
2322 -919 2051 0
2480 -562 719 0
445 -597 1290 0
695 2432 -410 0
1649 -1117 1174 0
-2191 78 1305 0
2863 -450 -737 0
-2110 -1769 1043 0
327 1761 -1796 0
-1129 -399 1862 0
2956 2715 -2581 0
-215 2658 -462 0
-423 -594 2214 0
-1750 -1407 184 0
2536 2118 966 0
-2575 258 -2728 0
426 -2955 2008 0
-2072 2992 1839 0
-149 -1701 -146 0
-14 -2465 1943 0
289 -2115 2330 0
629 -1065 -2445 0
2389 -1120 240 0
-379 -185 -2532 0
-1310 477 1697 0
1293 2218 164 0
1310 1168 -2433 0
1641 2373 171 0
597 -1537 -4 0
-1630 1862 2477 0
2369 621 -380 0
-2925 -1070 -829 0
-2374 -1214 149 0
-2147 741 -2092 0
2657 -2481 -454 0
2843 -887 -1143 0
2218 1393 2343 0
739 -1234 -144 0
2991 904 -1595 0
2266 -701 1801 0
-1166 -1588 1536 0
1694 -629 -1342 0
112 1240 1005 0
682 2972 -796 0
-1314 2685 2399 0
2334 682 644 0
-2562 1230 138 0
2712 535 2945 0
-1215 2648 1653 0
1859 -2127 -1552 0
2951 388 1887 0
1224 -1947 1669 0
-1179 2647 2981 0
1784 2573 -2729 0
709 1296 1581 0
396 2715 -705 0
689 -1825 2569 0
-240 -1250 -169 0
1997 2841 506 0
-560 -2197 -485 0
1841 331 561 0
-915 -1404 1854 0
-1540 443 -1556 0
940 1837 1368 0
-1762 915 -375 0
694 -2047 -2023 0
792 -2940 2611 0
-1304 1835 1359 0
-1430 2135 1605 0
-1714 2418 392 0
-2074 -2897 -1796 0
2276 1652 -2436 0
1644 -480 -1632 0
1767 -2010 -697 0
-2726 1431 2015 0
1985 408 -612 0
-1596 -1342 2167 0
-2385 -2419 -884 0
486 -551 -1768 0
-2243 1050 1200 0
661 32 -2961 0
2691 1708 1679 0
-2340 2811 -1005 0
-1153 11 -2786 0
-2548 2511 1500 0
-1802 2771 2970 0
1855 -330 -1996 0
372 -2809 -2458 0
-2491 1989 1323 0
161 1257 -2796 0
2617 -1829 678 0
1630 -2514 -212 0
-2570 1042 -51 0
-2489 1285 391 0
1236 -157 -1185 0
-1428 -321 -371 0
-1899 1134 -1342 0
-1466 -2568 -1573 0
-1237 1405 -991 0
-159 2800 -1009 0
608 -2028 -1419 0
-1548 -165 1358 0
-1272 384 -1099 0
-1897 2206 647 0
-2911 1138 -89 0
-2750 2749 781 0
-144 -613 895 0
-1041 -1230 1199 0
-2632 -604 97 0
2839 -2171 794 0
95 -2470 2649 0
1974 41 -2444 0
-1706 786 -1556 0
881 1790 2829 0
-1320 -757 2894 0
-2216 2107 -763 0
-2100 -1945 -2029 0
-2733 -2175 -183 0
2347 2919 -2682 0
-1776 1309 979 0
1625 1466 2766 0
-1602 -1471 -1107 0
1435 -1559 -2064 0
-1319 -561 1425 0
1037 1358 1467 0
-796 1087 -2989 0
2494 308 -623 0
1279 -2114 -644 0
-1824 -2601 -2015 0
2158 -147 -2561 0
-790 -2357 -2918 0
11 -968 173 0
2657 412 -1474 0
-157 -2214 -582 0
744 2216 -2020 0
-2520 -2935 1624 0
-2743 -758 -872 0
-1770 -585 1418 0
677 1045 811 0
1492 -1965 -1621 0
199 -532 -728 0
-46 -1981 382 0
2414 -1212 402 0
1017 -1648 -1508 0
245 -802 -2566 0
-2912 -2025 71 0
-642 2103 -450 0
-2460 2428 386 0
2676 1268 -1168 0
-1692 -1734 -2900 0
-2529 2928 -2557 0
-2612 2315 452 0
1820 849 -2618 0
1742 -2253 485 0
1843 -1706 -2405 0
-784 1128 2468 0
-1369 -2189 95 0
2841 -2681 -136 0
-2325 -2754 2065 0
-2479 -1565 -55 0
-2756 -1713 -2876 0
2090 -905 -478 0
391 1013 -2342 0
-2159 1269 2404 0
-1698 1168 1019 0
-2631 1609 1929 0
-1731 -2335 2535 0
-2723 2804 30 0
-2413 -433 1049 0
28 2060 1838 0
1844 112 -2813 0
-2806 1221 2101 0
561 1217 2747 0
1863 2433 -1451 0
-2841 1 221 0
1519 -2259 318 0
-735 1289 -1957 0
2557 -2409 477 0
1135 -2655 504 0
1251 -1371 -1934 0
-1086 1281 1495 0
-1877 -2426 -517 0
-2242 2257 2383 0
1731 2956 606 0
2587 737 -966 0
470 -1762 1371 0
2875 92 -2865 0
-1311 2255 1898 0
1596 2395 -2574 0
-1516 -2487 -2237 0
-2500 2713 -1519 0
-1758 1858 -219 0
-2960 -2775 2317 0
-2627 155 -1757 0
1103 468 212 0
2288 -45 1139 0
1619 2663 -2105 0
2239 2197 -211 0
-2031 1427 2533 0
-1283 2810 2232 0
2176 2800 2414 0
2306 -2569 1610 0
-1889 179 -676 0
-1633 -543 -2025 0
-2084 2359 307 0
1149 -1045 2011 0
-862 2674 2737 0
-623 1554 -436 0
-1762 -543 -611 0
-2121 -1179 964 0
410 2765 1961 0
2721 -2473 2527 0
-2859 -600 -1977 0
1485 -1369 1560 0
-953 -1010 -1429 0
2474 -927 1591 0
-489 -117 -496 0
302 635 37 0
2164 -596 540 0
1121 1870 2847 0
-2947 2868 534 0
-27 1221 2793 0
739 -514 -806 0
2627 -478 1 0
-2868 1562 2279 0
-1273 -1121 1389 0
-1141 2406 2571 0
-1587 1566 2555 0
-1089 2017 1051 0
2889 -2111 170 0
-2917 -2594 -1865 0
1268 1420 -2044 0
2250 2006 -972 0
272 -498 -2740 0
1452 833 1136 0
1809 1722 2669 0
822 -1920 468 0
971 -1424 -137 0
-1033 2968 -2827 0
-1667 1563 -2580 0
-2743 -1689 -2633 0
-1025 2802 -2317 0
2093 607 2235 0
1117 -1943 1 0
1698 2543 -387 0
527 -2025 -655 0
1329 572 -1330 0
1598 543 1189 0
-2420 1262 -987 0
-2064 -111 -1032 0
-2822 -1732 1206 0
-2662 1684 2743 0
1995 -1333 -2454 0
2515 1643 -464 0
400 -138 1874 0
-1831 738 1526 0
-2063 1675 2392 0
1866 573 -32 0
-1421 1455 2098 0
2679 -213 -819 0
-872 -1937 -382 0
-1199 -396 -1182 0
2905 -1850 2692 0
1019 -2893 -1137 0
-361 2512 -2177 0
705 363 1864 0
1952 2434 1163 0
1811 -2629 2150 0
2998 -2359 -107 0
258 -2749 -35 0
-2785 -341 1336 0
-2459 -241 320 0