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