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