123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656 |
- 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 150 645
- -31 59 -92 0
- -90 97 89 0
- 117 142 45 0
- 23 58 112 0
- 52 -45 5 0
- 88 -111 124 0
- -141 -37 105 0
- -85 -103 -19 0
- -10 138 144 0
- 15 -77 99 0
- 85 -48 -139 0
- 66 -67 -123 0
- 47 80 62 0
- -1 70 14 0
- -49 56 115 0
- 26 10 121 0
- 101 133 -113 0
- -33 -50 -39 0
- -120 -116 17 0
- -22 8 113 0
- 60 30 -47 0
- 77 146 -97 0
- 149 -101 -37 0
- -13 79 1 0
- 17 45 20 0
- -62 -80 104 0
- 20 119 -14 0
- -57 139 112 0
- -77 46 4 0
- 136 59 -87 0
- 63 123 65 0
- -84 8 97 0
- -50 34 -21 0
- -70 111 -100 0
- -133 -60 78 0
- 50 93 128 0
- -149 -92 24 0
- 5 -134 102 0
- 122 46 -128 0
- -62 26 40 0
- 52 -63 -103 0
- 45 128 -51 0
- -136 -78 -118 0
- -105 -74 140 0
- -62 56 58 0
- 111 -95 -133 0
- 23 -18 89 0
- 59 70 89 0
- -120 111 -115 0
- 142 105 14 0
- -120 -16 -1 0
- 64 102 -141 0
- -13 -84 146 0
- -143 80 113 0
- -65 -31 110 0
- -135 49 -31 0
- -110 64 -61 0
- 26 79 -20 0
- -23 -22 -60 0
- -141 -43 129 0
- -115 -106 -107 0
- 105 51 -21 0
- -101 26 15 0
- 101 69 66 0
- -108 -44 87 0
- -145 -110 -14 0
- 59 6 80 0
- -25 -32 31 0
- -96 147 141 0
- -63 -94 122 0
- -144 47 -43 0
- -4 -60 3 0
- -101 8 -41 0
- 56 98 115 0
- 82 -115 108 0
- -82 106 -92 0
- -121 -55 -2 0
- 131 89 -143 0
- -139 126 -93 0
- 117 103 109 0
- 119 87 -28 0
- 3 30 -133 0
- -140 133 -60 0
- 128 -143 -105 0
- 65 -63 -79 0
- -95 106 -21 0
- 51 18 -110 0
- 5 -12 -95 0
- -44 122 91 0
- 124 -107 -99 0
- 137 75 41 0
- 87 -98 -74 0
- -8 135 -107 0
- -50 -92 -71 0
- -27 -64 69 0
- -61 -104 124 0
- -7 -47 -118 0
- -26 100 -82 0
- 82 -101 73 0
- 115 -118 76 0
- 82 -4 -145 0
- 76 111 -2 0
- 141 67 -44 0
- -53 -130 -46 0
- 137 -97 105 0
- -103 -62 50 0
- 53 -41 116 0
- 149 -74 -72 0
- 138 48 -99 0
- -21 9 27 0
- 22 -24 68 0
- 76 -24 74 0
- -47 -78 -81 0
- 88 -108 -125 0
- -117 -12 -6 0
- 149 -8 99 0
- 99 5 93 0
- -31 92 98 0
- 38 148 26 0
- 8 -2 29 0
- 89 144 -23 0
- 106 8 49 0
- 61 92 -17 0
- 60 150 -111 0
- -79 36 6 0
- 30 -23 -42 0
- 22 -90 -99 0
- 139 31 41 0
- 90 113 -43 0
- 27 -112 32 0
- -82 -13 -94 0
- 19 -34 -88 0
- -35 24 81 0
- -50 108 -70 0
- -43 -146 128 0
- 27 -149 123 0
- -43 -126 93 0
- -56 -14 98 0
- -6 -150 122 0
- -22 125 -1 0
- 30 -97 -136 0
- 60 -13 55 0
- 77 49 -47 0
- 38 -41 -146 0
- 15 -138 -51 0
- -2 17 66 0
- -66 -78 50 0
- 4 7 -91 0
- 46 -69 -16 0
- 118 -92 -119 0
- 138 -108 -123 0
- -91 -11 -69 0
- -32 134 5 0
- -98 -79 103 0
- 95 -88 -122 0
- -19 -94 -36 0
- 132 -88 -141 0
- 48 -109 -105 0
- 87 -29 67 0
- 70 -86 -124 0
- 119 18 22 0
- -135 141 107 0
- 97 -88 141 0
- -39 -76 -101 0
- -141 -35 29 0
- 43 45 -65 0
- 34 -43 40 0
- 106 21 -63 0
- 45 86 -149 0
- 86 -56 -103 0
- -57 127 -60 0
- -139 72 -33 0
- -104 26 18 0
- 5 122 -88 0
- -143 -108 -21 0
- 91 -26 -80 0
- 144 -120 31 0
- -130 72 -61 0
- -149 35 -68 0
- 51 -31 48 0
- -25 67 42 0
- -64 -61 -143 0
- 131 66 32 0
- 138 -62 -97 0
- 144 -49 -16 0
- -58 -146 -59 0
- -123 -14 -36 0
- -75 -89 -38 0
- -18 118 12 0
- -100 16 58 0
- 107 114 -23 0
- 140 -35 -137 0
- 147 74 35 0
- -134 48 132 0
- 4 -113 19 0
- -90 35 -39 0
- 85 40 -136 0
- 17 -62 -59 0
- 66 79 -137 0
- 51 -78 112 0
- 144 78 -74 0
- -134 125 -13 0
- 104 -64 -139 0
- -101 -30 -12 0
- 88 127 13 0
- 89 39 -79 0
- -136 54 -93 0
- 75 -127 52 0
- 147 90 -45 0
- -95 115 -98 0
- 108 -102 -31 0
- -4 -101 6 0
- -84 -24 -5 0
- 1 -84 -82 0
- -17 -36 -73 0
- -106 -100 39 0
- -89 -138 103 0
- -122 17 74 0
- 118 2 93 0
- -9 64 71 0
- 18 -133 -12 0
- 58 135 11 0
- -122 -85 -135 0
- -66 -88 -115 0
- 48 -43 55 0
- 58 -117 128 0
- -84 99 -46 0
- 57 101 -91 0
- 69 -125 -23 0
- -7 -37 -61 0
- 139 109 -110 0
- 100 21 -41 0
- -90 138 88 0
- 13 -148 46 0
- -53 113 77 0
- 96 33 -26 0
- -50 147 118 0
- 87 120 141 0
- -47 -76 -13 0
- 132 -25 -81 0
- 126 -83 8 0
- 100 -38 -52 0
- 71 -63 -52 0
- -76 133 41 0
- -57 37 -138 0
- -91 -107 119 0
- -42 -132 76 0
- -30 -22 60 0
- -17 92 -66 0
- -11 73 -115 0
- -110 128 95 0
- 102 112 -21 0
- -35 100 -2 0
- 118 57 51 0
- 111 21 140 0
- 63 128 5 0
- 47 8 -36 0
- 47 70 -55 0
- 8 131 1 0
- 125 32 -114 0
- -113 -28 145 0
- -17 -92 104 0
- 131 47 115 0
- -37 40 59 0
- 70 -29 101 0
- 24 41 -29 0
- 87 -28 54 0
- 101 -92 -76 0
- 123 -8 -26 0
- 101 22 108 0
- -53 -79 -77 0
- -44 34 114 0
- 127 -25 -17 0
- 38 -62 -145 0
- -142 -44 118 0
- 135 -149 102 0
- -148 123 82 0
- 36 -46 -30 0
- 40 136 -30 0
- -131 -40 -17 0
- 122 123 111 0
- 122 -31 -12 0
- -59 -28 127 0
- -57 120 -60 0
- 59 -134 -148 0
- -37 -55 -110 0
- 37 99 24 0
- -129 -60 -42 0
- -30 -55 -91 0
- 48 -49 78 0
- -32 10 65 0
- 133 -43 -140 0
- 21 70 51 0
- -34 -55 -104 0
- -68 -41 -143 0
- 6 -117 -126 0
- -112 -90 -25 0
- -92 116 35 0
- -42 61 -114 0
- -90 -102 -148 0
- 48 103 51 0
- 6 -134 97 0
- 147 27 7 0
- 91 61 -94 0
- 12 -146 81 0
- -93 -125 130 0
- -150 5 136 0
- -137 32 -96 0
- 26 -3 -120 0
- -69 77 28 0
- 21 -129 35 0
- -13 132 -22 0
- -94 -48 38 0
- -113 114 -28 0
- 30 89 36 0
- -112 37 -18 0
- 33 62 -126 0
- 147 113 41 0
- 35 -12 -114 0
- 21 122 -73 0
- -96 -141 126 0
- -107 20 -86 0
- -76 -71 -67 0
- -117 139 127 0
- -65 -72 42 0
- 77 73 61 0
- 76 142 -67 0
- 115 -150 61 0
- -147 83 4 0
- -43 77 -126 0
- 5 141 26 0
- 111 -117 -53 0
- -18 -92 -127 0
- -93 -120 25 0
- -150 136 114 0
- -79 -74 19 0
- 15 -99 26 0
- 45 143 95 0
- -114 -14 -37 0
- -24 -110 115 0
- 16 -13 -108 0
- -93 132 45 0
- 123 -93 -13 0
- 134 77 97 0
- -149 -88 -15 0
- -147 -91 -113 0
- -51 68 -61 0
- -114 8 52 0
- -59 91 5 0
- 78 92 76 0
- -38 -107 138 0
- -43 148 -128 0
- -101 -42 138 0
- -135 -25 -93 0
- -50 31 37 0
- -1 -109 -10 0
- 55 -143 -88 0
- -119 79 -13 0
- 109 -140 -4 0
- 146 29 137 0
- -86 -5 -16 0
- -35 -48 -108 0
- -94 49 15 0
- -86 113 -9 0
- 46 9 17 0
- -91 127 25 0
- 72 -107 -64 0
- -116 -23 42 0
- 1 66 9 0
- 147 -51 30 0
- 34 -24 -48 0
- -75 -51 76 0
- 132 46 27 0
- -70 27 -71 0
- -100 33 126 0
- -51 -79 82 0
- -68 60 112 0
- 146 30 -88 0
- -28 123 141 0
- 25 -1 -59 0
- -59 -31 32 0
- 52 46 -78 0
- -55 35 6 0
- -106 85 -32 0
- 122 58 83 0
- 134 -117 94 0
- -32 9 118 0
- -85 78 -41 0
- 148 -26 31 0
- 111 -94 122 0
- 106 -107 -146 0
- -121 -3 -112 0
- -95 -46 -61 0
- -82 133 -6 0
- -27 121 70 0
- 28 119 -150 0
- -126 -138 -124 0
- -71 21 -131 0
- -111 88 -97 0
- 93 76 -79 0
- 56 -101 -61 0
- -26 100 -66 0
- 84 -107 14 0
- -29 48 106 0
- 84 -107 81 0
- 103 -25 -106 0
- 92 -105 28 0
- 150 -38 -21 0
- -32 -131 6 0
- 143 40 -126 0
- 79 4 119 0
- -113 -110 -3 0
- 55 -116 -145 0
- 32 -10 77 0
- 57 140 -73 0
- -127 142 -128 0
- -144 -138 105 0
- -103 -32 37 0
- -44 139 26 0
- -4 -83 -13 0
- 50 92 -68 0
- -24 30 80 0
- -49 -129 90 0
- -100 -120 35 0
- 148 93 -142 0
- 86 -69 -48 0
- 96 -120 -114 0
- 83 -146 119 0
- -68 31 -15 0
- 12 3 48 0
- 110 -98 -136 0
- 92 46 -52 0
- 46 3 145 0
- 59 92 -106 0
- -28 55 -114 0
- -142 18 74 0
- -59 117 -71 0
- -109 -68 144 0
- -28 140 110 0
- 94 91 -58 0
- -33 -8 135 0
- 131 43 -127 0
- 42 112 -66 0
- 54 -93 137 0
- 17 -19 141 0
- 41 108 -15 0
- 34 -46 42 0
- 9 138 7 0
- 72 -77 -14 0
- -109 105 108 0
- -106 -70 142 0
- 119 -127 101 0
- 55 146 35 0
- -132 143 134 0
- 84 -9 28 0
- 75 64 125 0
- 122 2 46 0
- 119 -66 -29 0
- 61 -108 -92 0
- -116 -37 -1 0
- 49 3 22 0
- -92 -41 57 0
- 20 -82 -134 0
- -147 145 68 0
- -80 -4 -57 0
- 39 45 137 0
- 116 -10 96 0
- 90 16 140 0
- -34 -60 -68 0
- 122 77 -109 0
- -13 -46 149 0
- 56 -72 77 0
- 60 -33 89 0
- 122 -140 62 0
- -146 -64 -136 0
- 59 -105 -39 0
- 124 10 67 0
- 123 -70 -42 0
- -64 -90 -137 0
- 34 -125 -141 0
- 13 137 -37 0
- -47 18 150 0
- 123 -41 79 0
- -12 -16 -137 0
- 77 25 91 0
- 150 -57 5 0
- 28 -4 -67 0
- -37 -90 -25 0
- -13 -115 -142 0
- 115 -40 6 0
- -73 -107 106 0
- 126 20 67 0
- 26 84 -124 0
- 27 62 42 0
- 150 -25 45 0
- 54 -1 -108 0
- -72 -55 120 0
- -23 123 -100 0
- -73 49 -61 0
- 119 66 145 0
- -15 -124 74 0
- 72 55 57 0
- 58 67 -126 0
- 7 -135 -47 0
- 37 -68 -29 0
- 105 95 72 0
- -31 138 109 0
- 90 -88 -68 0
- -63 101 114 0
- -72 -55 130 0
- -48 40 5 0
- -24 98 -59 0
- 134 124 -25 0
- -31 101 -71 0
- 57 -132 -143 0
- -96 -130 119 0
- -21 -123 134 0
- 18 -88 142 0
- -12 19 132 0
- 20 -70 -24 0
- 91 52 85 0
- -95 -23 -7 0
- -97 120 49 0
- -120 -23 57 0
- 142 -124 -140 0
- 120 -76 -147 0
- -89 79 -22 0
- -57 105 -93 0
- 143 -13 -127 0
- -119 -105 54 0
- 54 -89 -115 0
- 49 83 29 0
- -45 85 141 0
- 92 -33 47 0
- 149 51 -115 0
- 92 -62 23 0
- 6 -11 -99 0
- 70 -125 -61 0
- -94 -54 134 0
- -150 120 -116 0
- 49 113 -35 0
- 88 25 -7 0
- 13 128 63 0
- 24 -132 78 0
- 74 -122 19 0
- 14 135 4 0
- 45 143 -48 0
- 138 -41 -84 0
- 74 -137 104 0
- 51 -69 -47 0
- -110 121 117 0
- 136 -63 15 0
- 139 101 83 0
- -44 -75 32 0
- -72 127 95 0
- 101 -6 23 0
- 90 -104 -136 0
- 18 -78 -47 0
- 93 5 88 0
- 146 126 -128 0
- 48 -50 -146 0
- -119 -43 38 0
- -80 -127 -111 0
- -67 -88 4 0
- -102 -94 141 0
- 41 -21 -65 0
- -26 -4 38 0
- 60 -89 -32 0
- -102 -20 52 0
- -119 78 -114 0
- -29 113 105 0
- -93 45 69 0
- -52 -85 120 0
- -47 72 73 0
- -119 -146 126 0
- -17 -133 10 0
- -37 -19 -72 0
- -136 -50 -31 0
- -7 -30 -72 0
- -127 97 93 0
- 149 45 -30 0
- -36 53 -124 0
- -55 -143 23 0
- 85 104 35 0
- 104 -9 -109 0
- -94 -110 31 0
- 79 -4 -99 0
- 25 -16 99 0
- -51 35 149 0
- 98 145 40 0
- 43 -135 -110 0
- 120 -37 82 0
- -25 114 59 0
- 18 -61 -44 0
- -47 -94 -79 0
- 87 -42 104 0
- 124 85 99 0
- 98 28 2 0
- 16 18 73 0
- 144 82 12 0
- -42 104 53 0
- 58 124 -102 0
- 45 -127 -134 0
- -58 149 2 0
- 48 -52 -117 0
- -70 15 -89 0
- -139 67 -63 0
- 46 118 69 0
- 13 71 -51 0
- 50 97 -10 0
- -1 76 148 0
- -28 -36 -74 0
- -31 22 -114 0
- 1 -63 -47 0
- 10 -126 44 0
- -2 -143 125 0
- -5 109 57 0
- 76 79 -54 0
- 16 -29 -17 0
- 10 -89 69 0
- -102 -109 -53 0
- 97 112 -94 0
- -36 115 -70 0
- 44 -20 126 0
- 3 -92 -144 0
- 132 96 59 0
- -19 -118 127 0
- 104 -6 -131 0
- -121 138 -5 0
- -2 -51 29 0
- 97 -103 -118 0
- -20 -6 -106 0
- -12 -72 81 0
- -127 66 14 0
- -68 15 -111 0
- -119 -106 35 0
- 75 -132 -28 0
- 106 -139 67 0
- 62 -107 -77 0
- -136 -4 -103 0
- 29 68 69 0
- -85 -79 -11 0
- 108 -64 -126 0
- -36 -11 64 0
- 50 71 -4 0
- %
- 0
|