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 200 860 55 -2 159 0 -35 92 68 0 67 -90 8 0 -71 -154 70 0 -90 -60 6 0 -145 48 64 0 -118 86 138 0 5 145 116 0 -88 98 173 0 28 -135 -146 0 -96 -54 186 0 -5 74 -123 0 168 64 -144 0 101 -163 -69 0 -159 -148 -48 0 42 75 -11 0 -64 -39 41 0 -185 149 162 0 -98 132 -1 0 -79 164 68 0 83 -108 -122 0 60 -198 -195 0 -199 168 -124 0 -198 -193 86 0 -118 -38 -54 0 -32 -46 -28 0 -110 198 -161 0 79 95 111 0 156 53 -198 0 -132 -168 -194 0 -105 -184 -4 0 95 -47 140 0 -199 29 -131 0 -115 187 39 0 69 -160 56 0 20 -50 -192 0 -164 -77 -176 0 139 130 -155 0 56 152 -172 0 182 -133 -160 0 45 14 -154 0 -164 -1 -11 0 66 -42 -71 0 -5 168 -61 0 -175 43 57 0 -38 -124 -66 0 -126 123 102 0 -79 -128 -47 0 -58 -151 -126 0 43 102 -30 0 151 74 -33 0 118 -190 -114 0 24 -5 104 0 -30 -11 -2 0 -142 171 29 0 -79 20 138 0 103 -153 -192 0 193 196 123 0 -147 96 86 0 -75 -192 184 0 -168 -41 -73 0 108 54 62 0 -18 -62 29 0 15 104 191 0 114 126 -33 0 151 -198 -36 0 -132 -11 -41 0 26 127 -172 0 -150 -81 34 0 182 -94 11 0 10 -141 -38 0 31 95 151 0 -181 -113 188 0 -83 118 -134 0 1 41 -8 0 51 -64 -139 0 -29 139 197 0 40 -191 -197 0 81 -26 -82 0 -129 -142 180 0 135 3 98 0 -176 119 -145 0 57 -137 145 0 18 45 114 0 38 -188 -197 0 -52 -59 151 0 156 108 159 0 -54 -137 -193 0 -87 -8 1 0 55 -145 -46 0 -200 -14 -28 0 -191 118 -67 0 -6 71 84 0 -154 -156 -82 0 13 10 132 0 28 60 107 0 14 -200 187 0 -28 -155 -75 0 186 106 99 0 -55 -72 -64 0 -81 158 -184 0 56 -26 -193 0 -46 134 96 0 -64 29 153 0 16 -151 83 0 -2 17 -170 0 -179 -59 -8 0 113 147 47 0 57 130 120 0 -20 -107 -166 0 116 -187 -120 0 67 -150 182 0 187 34 28 0 123 -99 -24 0 57 127 22 0 124 145 -193 0 -166 -96 114 0 29 -155 -68 0 -151 -109 -8 0 -90 7 42 0 -117 -152 16 0 -73 -160 -140 0 20 -135 63 0 198 -142 -159 0 -120 -5 -115 0 32 -31 95 0 91 -12 -49 0 139 -17 90 0 51 -102 -22 0 118 -26 141 0 176 18 87 0 159 -155 37 0 162 -124 -50 0 -131 -176 -56 0 89 -101 -188 0 -85 -108 192 0 196 -137 -10 0 -66 -105 119 0 -69 86 18 0 87 -126 103 0 49 39 -143 0 -96 5 -57 0 101 102 105 0 61 86 -146 0 -81 -97 110 0 -18 19 -103 0 -81 154 -117 0 138 -159 56 0 101 -38 -158 0 -30 -197 65 0 -3 -197 -53 0 -17 -38 -64 0 -87 -113 82 0 -13 -55 96 0 139 131 -9 0 37 -73 -184 0 200 -194 -178 0 186 -13 65 0 125 -167 -73 0 32 77 -105 0 27 116 47 0 -150 4 -19 0 -80 -53 -159 0 164 44 80 0 -10 -95 -93 0 -90 -160 88 0 -161 119 -96 0 125 126 -15 0 195 33 177 0 -91 -79 134 0 156 83 -27 0 134 -179 -115 0 192 -82 -86 0 -140 159 188 0 157 -123 -136 0 -158 -62 11 0 181 38 -8 0 -55 58 47 0 96 -4 169 0 141 -77 124 0 4 -124 -92 0 44 -88 32 0 16 -38 157 0 -74 -25 43 0 -97 -22 -167 0 -176 112 88 0 34 108 115 0 -100 -128 -169 0 36 -179 -13 0 122 31 -179 0 -86 -179 79 0 -56 2 6 0 -182 -186 -23 0 -140 184 106 0 110 184 71 0 -56 -157 52 0 33 -185 -21 0 -134 137 91 0 -85 -26 23 0 -31 -87 -68 0 175 -30 97 0 45 197 -11 0 171 -169 -101 0 -101 -9 -14 0 7 -29 77 0 -15 -104 82 0 -137 174 42 0 112 10 -44 0 200 172 -177 0 4 -101 -5 0 132 189 -39 0 58 -36 -142 0 175 -94 190 0 -187 -106 -33 0 -139 122 27 0 -78 -133 190 0 83 -4 -125 0 -5 77 -200 0 56 81 -11 0 13 -183 49 0 40 -3 -183 0 119 1 132 0 -150 30 110 0 54 -79 -85 0 192 179 111 0 91 58 -39 0 -2 7 -158 0 167 -199 13 0 -81 1 115 0 94 56 60 0 41 187 135 0 -36 -62 29 0 -177 161 78 0 -25 117 26 0 20 -177 146 0 156 21 29 0 -114 -136 -150 0 20 106 -105 0 -122 118 -58 0 -37 -76 117 0 25 111 118 0 143 115 154 0 -36 -76 188 0 -81 95 199 0 -78 79 131 0 91 -86 -195 0 -27 -82 -110 0 62 -9 42 0 -130 -30 -109 0 -184 45 29 0 -198 -129 -175 0 189 -164 -195 0 -64 5 -177 0 121 -183 -155 0 180 95 166 0 97 -6 133 0 -184 187 -33 0 -146 149 180 0 47 174 -16 0 122 -182 22 0 92 -86 35 0 -94 -141 -19 0 102 -64 -52 0 -114 32 79 0 56 154 64 0 -105 -133 139 0 -172 -50 -36 0 -93 -77 18 0 -49 -71 34 0 9 -54 20 0 124 -35 -193 0 -158 -146 -199 0 -148 -29 50 0 168 -22 78 0 67 157 130 0 -146 152 95 0 88 -172 -15 0 -59 113 -179 0 -116 46 -173 0 -69 -113 -78 0 58 145 152 0 171 44 -34 0 114 -121 -163 0 -139 44 87 0 -200 4 -86 0 55 146 -48 0 26 199 -163 0 44 -169 92 0 120 129 135 0 13 59 28 0 -89 -110 176 0 56 142 3 0 189 45 25 0 -171 -170 145 0 -131 187 -63 0 -188 -173 -28 0 -166 -164 85 0 26 171 -131 0 66 -22 -150 0 14 57 -111 0 194 -2 167 0 165 130 40 0 136 -124 192 0 -46 40 -64 0 118 -63 48 0 -22 -131 64 0 -64 -116 158 0 -125 -101 -179 0 158 11 192 0 13 -123 104 0 -122 -173 -171 0 -13 -25 39 0 26 -53 104 0 -157 -127 80 0 190 160 -8 0 -134 -142 130 0 27 -139 116 0 -68 -134 96 0 -41 95 -190 0 6 -33 -98 0 -172 -59 -58 0 -192 189 123 0 151 121 -166 0 110 134 198 0 -37 60 -74 0 -51 -45 59 0 93 137 10 0 47 194 184 0 -115 149 9 0 154 84 -123 0 27 -68 -40 0 -106 68 -122 0 -178 -130 -159 0 37 -57 -147 0 108 -123 77 0 26 177 -161 0 -50 168 4 0 137 60 -16 0 94 -57 -14 0 -33 10 105 0 -4 -66 31 0 -100 -181 -60 0 190 -89 3 0 -163 -78 -80 0 158 150 192 0 -116 62 98 0 39 126 -10 0 40 20 51 0 -65 -188 112 0 -127 -120 177 0 150 97 -98 0 77 -81 49 0 48 19 -98 0 132 126 109 0 70 -196 -192 0 -83 -64 -70 0 -104 188 -192 0 -31 121 189 0 -50 -150 174 0 30 -62 -39 0 194 -191 -17 0 -175 74 -116 0 -137 -56 -109 0 -174 -32 76 0 191 21 129 0 -183 35 -27 0 127 72 70 0 -31 175 -151 0 -66 73 -165 0 -9 12 175 0 -174 24 -51 0 197 -148 20 0 -162 -20 -32 0 44 -25 4 0 -164 -174 36 0 155 84 -100 0 -153 -81 69 0 30 108 78 0 -193 64 61 0 21 -36 -200 0 133 -128 194 0 153 86 -157 0 -81 -88 11 0 195 -142 -94 0 82 159 -1 0 -191 -148 102 0 61 -133 -120 0 -121 -35 65 0 162 188 156 0 20 124 54 0 194 -196 -17 0 130 41 49 0 -178 -119 -91 0 -71 -99 -62 0 -145 65 9 0 158 65 94 0 182 -85 -19 0 -57 120 -21 0 -53 99 -31 0 69 -168 -37 0 154 -89 171 0 -137 -123 100 0 58 -9 -161 0 11 -8 -88 0 13 190 78 0 -155 20 97 0 141 -4 -160 0 82 18 120 0 -31 -107 83 0 -29 160 192 0 114 163 -78 0 48 28 -149 0 119 -149 126 0 -115 -22 127 0 -200 168 34 0 -50 -187 5 0 73 45 -121 0 130 171 -137 0 76 -124 148 0 -77 -120 -55 0 -152 161 -115 0 -49 -160 157 0 157 -110 -180 0 -19 39 113 0 -54 118 153 0 -35 -179 -24 0 61 -184 70 0 25 109 -160 0 -194 -20 162 0 139 -40 -120 0 -155 -182 126 0 -89 191 -45 0 -8 33 -106 0 90 -30 -126 0 -54 -74 151 0 121 120 79 0 -107 -186 200 0 147 -151 39 0 158 8 105 0 -195 113 114 0 -43 7 198 0 -130 -159 80 0 -135 -56 174 0 -49 -65 -99 0 -193 144 -71 0 -184 132 164 0 -75 -183 176 0 -178 46 140 0 -43 68 112 0 -100 -12 4 0 127 101 24 0 107 -157 -59 0 -166 89 15 0 153 82 -101 0 -125 123 133 0 21 -19 151 0 -121 16 188 0 -149 -62 187 0 198 -120 -108 0 -20 108 -53 0 -2 -57 164 0 -185 22 -88 0 71 -150 46 0 -83 111 -133 0 -121 -28 24 0 119 -182 117 0 155 118 38 0 26 161 -188 0 85 100 12 0 -133 -10 48 0 -17 -102 -8 0 -149 -138 -59 0 25 5 -109 0 -114 -161 -26 0 -145 110 -125 0 18 83 -9 0 167 -164 -130 0 175 -176 -113 0 9 102 -150 0 149 -171 -36 0 180 -185 -188 0 -172 -163 109 0 172 88 -130 0 63 177 -68 0 -46 -174 -30 0 98 -114 -116 0 -65 90 -77 0 -190 -59 -78 0 -39 176 -130 0 -101 118 106 0 -63 133 154 0 -93 82 163 0 160 -46 108 0 -189 -4 195 0 -51 -11 184 0 -197 -3 -151 0 -23 74 -50 0 -34 3 -150 0 -160 -28 118 0 21 -197 -37 0 -23 149 -181 0 -140 -122 36 0 94 140 -81 0 157 -41 147 0 -101 16 89 0 116 42 190 0 58 -154 -11 0 172 36 -56 0 -173 -35 -177 0 12 -10 186 0 -141 -63 47 0 20 -17 -14 0 146 -82 192 0 -139 106 105 0 85 -36 -22 0 -76 77 -31 0 -183 27 -6 0 -153 2 -197 0 -14 142 37 0 -130 141 97 0 -121 88 -109 0 -141 -192 -142 0 62 141 199 0 189 98 145 0 -86 145 -142 0 -16 -17 40 0 -39 109 42 0 -178 -118 170 0 -180 -164 -151 0 124 75 109 0 18 -73 -22 0 -108 35 -99 0 -178 -193 72 0 -200 149 -11 0 115 196 -73 0 29 -79 -2 0 -40 -43 33 0 -92 -169 40 0 10 115 157 0 18 180 24 0 21 31 162 0 20 120 -141 0 -100 149 -140 0 -121 -130 -105 0 158 -174 157 0 69 7 2 0 -112 7 -40 0 64 -12 71 0 150 -45 15 0 -188 -143 -183 0 -184 -60 165 0 -85 63 -58 0 -96 89 133 0 52 41 101 0 76 83 27 0 -17 -10 77 0 33 80 -90 0 -12 100 5 0 -1 -119 137 0 186 -61 -114 0 -29 -135 -150 0 134 150 24 0 -139 -52 -128 0 -38 197 113 0 -6 84 158 0 59 124 -12 0 -152 -163 -77 0 -4 124 -168 0 125 105 161 0 135 83 142 0 -169 61 -161 0 -108 -21 -152 0 100 -200 -61 0 -32 56 -31 0 -52 -27 -192 0 -30 88 -54 0 -180 -174 -144 0 -68 -58 139 0 55 -158 124 0 -194 -2 -44 0 179 25 -49 0 155 -195 90 0 -37 -193 104 0 -45 176 -186 0 185 54 -138 0 190 18 -157 0 154 -4 166 0 -90 -139 84 0 22 -159 180 0 144 -111 -95 0 -13 -128 -150 0 -142 -119 -4 0 199 51 -44 0 87 65 116 0 107 16 153 0 134 109 -18 0 83 -20 102 0 191 126 -114 0 -192 -95 22 0 -150 68 109 0 193 2 -113 0 193 168 -11 0 158 44 64 0 29 -70 -165 0 144 126 193 0 -56 20 -62 0 -159 -23 -114 0 -107 -75 10 0 41 174 -157 0 -132 168 59 0 185 75 -106 0 -193 -2 158 0 73 78 149 0 -170 89 68 0 -60 -25 59 0 -4 -133 -153 0 44 172 -198 0 75 150 47 0 -117 -2 183 0 -76 -188 101 0 -12 109 -183 0 -160 62 133 0 -126 -137 -159 0 66 76 -193 0 124 136 108 0 75 83 -121 0 -18 -6 200 0 -159 88 -199 0 108 -125 34 0 -21 -97 -30 0 141 196 183 0 -200 70 -35 0 61 178 -85 0 17 -3 69 0 -145 123 138 0 75 192 -54 0 -86 53 -176 0 118 -113 172 0 147 188 -69 0 -57 -183 -94 0 -52 31 -136 0 -12 173 41 0 -181 11 -5 0 19 -160 164 0 -58 31 -184 0 95 -77 172 0 19 -194 -32 0 -152 -160 -135 0 133 130 107 0 98 75 -113 0 -23 -121 -13 0 52 169 -188 0 -8 -180 127 0 -91 -70 -169 0 -79 -64 59 0 -127 -168 -4 0 -134 13 -124 0 88 104 132 0 53 -137 -138 0 6 13 -166 0 -148 131 79 0 106 -4 -52 0 -181 12 52 0 -180 78 -35 0 -20 -104 -182 0 -97 116 -117 0 14 173 -190 0 14 182 -125 0 -164 -73 -29 0 -167 -9 -31 0 135 90 -113 0 37 -78 -153 0 140 157 136 0 15 -185 102 0 171 150 99 0 -199 34 181 0 92 -121 123 0 -198 -86 23 0 163 166 30 0 156 -179 162 0 -146 179 -94 0 172 181 98 0 -161 -22 130 0 28 -119 46 0 70 -139 33 0 -92 138 191 0 163 -36 61 0 105 90 107 0 -115 -100 -181 0 14 26 102 0 58 -149 31 0 -128 -97 130 0 -73 62 149 0 42 -11 120 0 186 183 -102 0 181 -87 108 0 107 62 139 0 96 -122 158 0 -64 -142 65 0 -60 150 17 0 120 17 132 0 70 -135 -127 0 104 -67 -98 0 -115 -174 -140 0 13 -16 53 0 75 -97 -106 0 -71 193 70 0 173 -105 108 0 69 80 -192 0 -113 -72 -164 0 -54 -176 -37 0 -94 53 -154 0 -4 23 58 0 -129 -162 -103 0 68 82 -34 0 172 101 110 0 -168 -154 -143 0 -75 120 -15 0 155 159 69 0 20 -145 -120 0 187 -147 -67 0 -187 123 -80 0 -122 118 -115 0 -43 5 -102 0 150 -82 -125 0 -36 120 47 0 -28 -2 -124 0 102 -52 -85 0 160 -31 139 0 -42 -92 82 0 -66 197 -135 0 114 127 151 0 5 -136 -133 0 -23 -112 151 0 162 -15 -185 0 -59 -46 142 0 143 -73 -166 0 -174 114 134 0 -28 -25 -197 0 71 -148 -184 0 -200 50 -11 0 -181 185 -41 0 145 -51 65 0 -163 -185 92 0 -129 34 26 0 77 89 -67 0 55 -10 -93 0 -47 -100 -21 0 177 140 -163 0 -146 -28 159 0 188 -16 -136 0 162 157 -174 0 25 99 28 0 -23 186 144 0 110 -200 70 0 116 158 -25 0 -15 174 -84 0 -116 52 34 0 147 -119 29 0 134 14 82 0 14 197 11 0 165 62 196 0 184 -165 -75 0 60 -55 -91 0 171 79 8 0 -105 -96 -87 0 -138 -98 195 0 156 -129 -8 0 2 6 -169 0 87 -65 193 0 184 -23 -171 0 -4 75 -2 0 41 -163 76 0 -162 195 -28 0 44 174 -187 0 111 -51 127 0 -185 -124 -140 0 134 162 -109 0 31 -171 -97 0 -181 -145 157 0 -72 -90 -75 0 63 -155 120 0 148 74 3 0 158 -113 183 0 -38 -152 28 0 18 -191 98 0 88 51 -22 0 48 200 -35 0 62 14 30 0 -128 105 153 0 163 116 63 0 -127 -95 -102 0 -110 -149 152 0 61 -59 21 0 91 -30 193 0 -115 148 6 0 -28 134 108 0 82 -192 -157 0 41 196 -13 0 -149 176 -145 0 32 -134 78 0 -51 139 18 0 -167 -150 91 0 78 24 -22 0 -6 -34 -82 0 -81 6 -35 0 42 93 -84 0 159 -17 100 0 76 -18 -106 0 3 114 -24 0 186 -145 4 0 165 144 -139 0 198 162 -6 0 179 -86 164 0 75 186 98 0 56 194 -99 0 39 83 86 0 3 77 -180 0 99 186 -43 0 -67 42 -15 0 192 -85 -9 0 -105 20 -37 0 73 64 184 0 11 176 192 0 -170 123 -90 0 -94 -50 66 0 57 20 -66 0 -1 -83 190 0 -190 -146 42 0 -29 -168 20 0 -99 -46 128 0 11 5 63 0 -3 98 155 0 59 71 36 0 197 -80 -2 0 95 97 -199 0 -66 -72 152 0 -1 -151 147 0 45 -2 -100 0 -114 -99 31 0 69 10 -125 0 -15 97 57 0 -16 -25 154 0 191 -25 -99 0 41 -18 98 0 99 1 22 0 8 82 -150 0 68 64 -200 0 119 -17 -4 0 -16 146 126 0 -125 -115 -59 0 -200 146 8 0 -124 78 -119 0 -102 17 160 0 -13 -49 12 0 196 87 143 0 -180 -33 26 0 -42 105 113 0 104 129 28 0 -129 -46 110 0 % 0