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