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