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