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