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