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