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