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