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