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