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