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