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