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