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