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