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