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