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