123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441 |
- c This Formular is generated by mcnf
- c
- c horn? no
- c forced? no
- c mixed sat? no
- c clause length = 3
- c
- p cnf 100 430
- -96 53 6 0
- -57 44 -58 0
- 58 3 61 0
- -39 72 -91 0
- 72 -35 84 0
- 24 50 -78 0
- -35 -86 -37 0
- 76 29 89 0
- -86 -72 80 0
- -71 -27 -45 0
- -79 80 -48 0
- -50 44 61 0
- -72 11 -61 0
- 69 32 67 0
- 59 79 48 0
- 1 -12 -84 0
- -24 17 -37 0
- -16 74 84 0
- 71 -3 -62 0
- 58 10 -49 0
- -8 -13 -93 0
- 84 -83 -77 0
- -92 -83 -52 0
- -5 -29 89 0
- -36 23 -50 0
- -66 34 75 0
- -19 8 -18 0
- 73 -19 66 0
- -10 -99 53 0
- -39 -100 -40 0
- 50 100 -24 0
- 26 -31 -75 0
- 93 -77 25 0
- 27 69 1 0
- -63 32 57 0
- 100 -65 22 0
- -82 99 76 0
- 15 12 -9 0
- -88 -55 -47 0
- -6 -41 10 0
- 85 91 -90 0
- 51 -96 -61 0
- -58 68 91 0
- -45 -94 -73 0
- -70 88 -93 0
- -5 34 -74 0
- 58 90 84 0
- -98 72 4 0
- -8 -83 -4 0
- 32 45 73 0
- -7 29 -55 0
- -69 -81 -84 0
- -89 -97 70 0
- 2 -92 -91 0
- -90 4 9 0
- 83 34 -62 0
- 32 84 -67 0
- -13 25 62 0
- -90 19 38 0
- -45 -12 13 0
- 86 -57 -74 0
- -33 26 72 0
- 64 53 33 0
- 71 25 -68 0
- 18 49 -3 0
- 71 88 32 0
- 33 -68 -52 0
- 13 -30 -45 0
- -95 26 4 0
- -53 -51 -57 0
- -30 -51 -46 0
- 88 28 48 0
- -31 -45 -43 0
- -55 84 -23 0
- 66 -99 -7 0
- 80 83 39 0
- -5 -31 -62 0
- 65 -100 38 0
- 5 -30 -11 0
- -84 -53 55 0
- 79 -53 89 0
- 51 82 64 0
- 6 97 33 0
- -69 9 38 0
- -36 21 -77 0
- -97 90 -4 0
- -18 -58 -63 0
- 15 75 -92 0
- -56 -86 4 0
- -17 -100 -61 0
- 45 -86 -62 0
- -30 -89 -26 0
- -86 85 -70 0
- -73 -87 72 0
- -17 -96 36 0
- 49 -34 -11 0
- 78 12 71 0
- -98 -89 -26 0
- 53 38 44 0
- -61 30 19 0
- 21 -56 42 0
- -12 43 35 0
- 23 43 -26 0
- 5 -63 28 0
- 71 -47 -89 0
- -63 -33 -38 0
- -6 -40 96 0
- -9 27 58 0
- 61 -98 77 0
- -78 -32 -88 0
- -63 37 -97 0
- -61 36 34 0
- 88 -32 -45 0
- -95 -48 -78 0
- -88 -33 -94 0
- 41 -62 5 0
- -31 -21 -70 0
- 82 64 23 0
- -5 -4 58 0
- 45 63 46 0
- 5 78 -6 0
- 44 45 -88 0
- 5 90 28 0
- -38 20 41 0
- -8 -47 78 0
- 97 -90 93 0
- -70 -42 -52 0
- 20 -59 -50 0
- 85 24 -84 0
- 40 -26 34 0
- 32 -75 7 0
- 30 47 82 0
- -24 60 -91 0
- -55 -70 39 0
- 20 -13 -58 0
- -68 66 -82 0
- 22 -89 34 0
- 44 -16 94 0
- 88 41 -9 0
- 51 -39 -9 0
- -83 43 65 0
- -52 -55 -96 0
- 19 1 -4 0
- -51 22 30 0
- -55 98 -88 0
- 63 -88 5 0
- 35 -3 93 0
- 19 7 -51 0
- 11 69 -6 0
- -89 83 -51 0
- 38 10 -44 0
- -80 72 -99 0
- -22 20 92 0
- -56 -52 79 0
- -15 -81 90 0
- -21 94 -46 0
- -60 -15 -53 0
- 43 -9 74 0
- 45 -36 -67 0
- 30 -12 -38 0
- -55 -98 88 0
- 82 -21 37 0
- -89 -22 32 0
- 77 100 47 0
- 1 -52 55 0
- 33 25 -29 0
- -42 5 -11 0
- 2 -27 -10 0
- -45 65 -66 0
- -35 8 40 0
- 20 -78 -34 0
- 38 39 63 0
- 37 -20 28 0
- -12 -98 -80 0
- 65 23 95 0
- 14 -32 19 0
- -5 -18 -55 0
- -68 3 91 0
- -11 61 41 0
- -78 1 -52 0
- 13 -18 -96 0
- 47 69 -93 0
- -72 -4 62 0
- 6 -9 71 0
- 75 77 9 0
- -90 -61 -30 0
- -60 38 -63 0
- -11 -10 -2 0
- -83 78 8 0
- -61 100 84 0
- 81 -16 -93 0
- -4 60 -22 0
- -64 -24 69 0
- -64 78 19 0
- -79 -91 -43 0
- -94 40 -83 0
- -70 52 -43 0
- 50 81 -78 0
- -60 -9 -51 0
- -22 59 72 0
- 32 -13 71 0
- 97 -69 -72 0
- -94 9 69 0
- -44 -88 23 0
- 76 -88 -60 0
- 79 -83 -93 0
- 68 94 60 0
- -28 -26 -27 0
- 11 41 33 0
- -11 95 -94 0
- -37 29 -66 0
- -54 -20 16 0
- 20 -78 60 0
- -27 -16 -55 0
- -92 62 56 0
- 59 57 -30 0
- -81 -96 75 0
- -30 8 -4 0
- -2 50 94 0
- -17 -100 6 0
- 73 -44 82 0
- 58 49 20 0
- -58 -73 15 0
- 40 64 -88 0
- -77 37 -96 0
- -8 -81 -24 0
- 13 -41 -40 0
- -40 -30 57 0
- -93 -30 82 0
- -77 39 38 0
- -52 28 26 0
- 67 -30 49 0
- 90 -1 50 0
- 65 48 70 0
- -48 -5 -72 0
- -31 27 20 0
- 65 -69 66 0
- -34 65 -28 0
- -23 75 -31 0
- -25 -69 64 0
- 88 84 -65 0
- 45 5 35 0
- -38 51 -73 0
- -48 57 -59 0
- 38 -75 49 0
- 39 -59 86 0
- 71 11 31 0
- -14 59 99 0
- 70 -72 90 0
- -8 -88 -14 0
- 57 27 42 0
- -69 100 19 0
- 46 19 99 0
- -78 75 95 0
- 6 -10 32 0
- 3 -22 -46 0
- -53 33 -75 0
- 12 77 98 0
- 34 -99 -77 0
- 73 -72 -89 0
- -24 93 76 0
- 45 -90 73 0
- -99 -73 80 0
- -98 17 -1 0
- 53 17 37 0
- -94 45 -20 0
- -9 -58 46 0
- -85 -76 -80 0
- -66 69 81 0
- -32 95 -41 0
- 95 -29 6 0
- 70 -7 -77 0
- 23 73 -29 0
- 66 -3 68 0
- 71 -1 5 0
- -73 -63 -69 0
- -98 -47 -73 0
- -28 -85 -34 0
- 56 -53 74 0
- 33 -70 42 0
- 76 53 73 0
- -10 28 -97 0
- -44 29 78 0
- -40 -84 -21 0
- 96 52 5 0
- -8 84 88 0
- 61 43 -34 0
- -88 -73 -36 0
- 13 -97 50 0
- -95 -55 84 0
- 14 94 100 0
- -37 6 -56 0
- -62 37 72 0
- 64 14 -26 0
- 46 41 40 0
- 44 -53 -20 0
- 57 -91 71 0
- -12 23 -58 0
- 13 -83 72 0
- -24 -41 -59 0
- 90 -13 52 0
- 74 13 -95 0
- 65 38 -77 0
- -81 -34 -79 0
- 71 -95 -14 0
- -28 -47 -96 0
- -84 -30 -65 0
- 33 -39 27 0
- -6 -42 -82 0
- -58 -64 48 0
- 54 -21 52 0
- -1 -83 38 0
- -54 94 50 0
- 29 -9 53 0
- 63 50 10 0
- -15 74 23 0
- 75 -22 -5 0
- -23 40 -59 0
- 84 -48 -70 0
- -82 20 11 0
- 94 44 4 0
- 39 -85 48 0
- -8 -19 -74 0
- -28 74 -41 0
- -58 -90 18 0
- 98 -74 91 0
- -27 -29 -86 0
- -8 80 -100 0
- 75 -73 -64 0
- 14 -27 63 0
- -77 -92 17 0
- -68 -20 36 0
- 35 -3 87 0
- -25 -58 -6 0
- 60 86 -1 0
- -65 -93 -87 0
- 89 -28 -100 0
- 32 16 -96 0
- -51 -74 37 0
- 31 22 94 0
- 26 -8 -2 0
- -92 77 -89 0
- -85 -32 86 0
- -59 -1 -9 0
- -4 88 91 0
- 6 -44 42 0
- -68 48 8 0
- 27 23 -41 0
- -47 -61 92 0
- 25 -59 -36 0
- -51 -61 -99 0
- 23 -35 2 0
- -39 19 -62 0
- -70 77 -24 0
- 10 -57 -39 0
- -1 23 55 0
- -53 -38 57 0
- -94 -7 -66 0
- 18 56 73 0
- -22 -27 61 0
- 55 -74 -56 0
- -30 -25 -7 0
- -34 73 -81 0
- -96 -45 22 0
- 72 -9 66 0
- 65 23 -12 0
- -90 61 -8 0
- -71 -81 -60 0
- 18 75 32 0
- 79 14 -27 0
- -83 10 18 0
- -78 18 -9 0
- 73 85 36 0
- 19 -54 91 0
- -68 73 -46 0
- 89 -1 100 0
- -54 -73 -47 0
- -18 -31 -45 0
- -68 81 35 0
- 91 -98 1 0
- 27 -80 18 0
- 55 40 85 0
- 61 -20 73 0
- 87 -41 16 0
- 49 89 43 0
- -68 -51 -14 0
- -98 32 39 0
- -25 -93 60 0
- 33 85 -72 0
- 93 54 -59 0
- -69 -72 34 0
- 82 55 -43 0
- 60 -63 -68 0
- 52 93 -50 0
- -94 -33 9 0
- -35 38 84 0
- 79 1 95 0
- -96 -81 -94 0
- -29 -52 -47 0
- 34 68 -20 0
- 55 54 25 0
- -78 100 -45 0
- -4 -16 46 0
- -52 -8 -97 0
- 84 -20 -39 0
- 91 -16 13 0
- 60 31 -34 0
- 69 7 70 0
- 60 56 54 0
- 62 66 41 0
- -38 -36 47 0
- 21 -3 -10 0
- 30 -26 -93 0
- 90 -29 8 0
- 80 -32 99 0
- -51 -92 58 0
- 3 -29 -12 0
- -56 -10 83 0
- 79 -12 -41 0
- 100 -14 -74 0
- -69 59 -54 0
- -68 -44 -9 0
- -70 26 -4 0
- 86 94 -98 0
- -1 13 -94 0
- 70 -1 -20 0
- 3 34 -5 0
- 5 83 1 0
- -94 20 8 0
- -72 47 -35 0
- %
- 0
|