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