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