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