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