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