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