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