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