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