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