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