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