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