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