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