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