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