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