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