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