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