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 250 1065 80 134 221 0 57 74 50 0 26 -154 210 0 -242 -239 31 0 126 143 -172 0 37 153 -125 0 -113 -79 -46 0 -208 -152 -32 0 18 -145 177 0 123 19 250 0 -35 -162 -226 0 -133 -32 -77 0 56 151 104 0 -25 -85 151 0 59 5 -62 0 131 -83 97 0 -103 126 -48 0 -131 -110 -141 0 -240 -221 -42 0 -182 231 -179 0 179 170 60 0 41 128 -178 0 -79 -187 91 0 -176 159 -7 0 142 -231 -160 0 47 -152 -117 0 159 218 19 0 -68 134 -11 0 -194 -28 -89 0 129 -137 118 0 236 4 -242 0 244 19 -135 0 87 172 -74 0 28 -23 -202 0 3 -102 84 0 -211 -125 -44 0 120 -222 172 0 195 -71 198 0 -192 195 49 0 -91 -64 122 0 214 144 136 0 161 -215 85 0 109 -164 140 0 -83 123 2 0 151 107 127 0 -33 244 204 0 31 -162 -14 0 185 -103 146 0 -131 242 -199 0 196 22 71 0 132 -76 96 0 -136 -24 9 0 132 -74 106 0 103 -28 -6 0 16 -106 -149 0 188 -59 18 0 -129 -30 -35 0 -141 60 -248 0 11 -189 172 0 144 5 187 0 235 28 172 0 14 190 96 0 -222 -217 -84 0 113 -224 109 0 115 -134 -104 0 164 -161 222 0 -152 -176 221 0 22 -195 -14 0 27 -200 -135 0 -175 -73 87 0 -139 159 2 0 126 -247 5 0 146 165 66 0 -28 -105 -241 0 -146 89 -2 0 13 -202 -158 0 49 -51 -225 0 -105 70 -109 0 -213 98 -42 0 -133 -156 44 0 135 -150 -58 0 -21 212 -35 0 190 120 28 0 235 -3 -196 0 231 -89 -110 0 -131 -108 147 0 -172 -170 22 0 -164 -105 -156 0 -39 -138 -199 0 188 -145 -244 0 -45 -49 -74 0 1 158 142 0 -59 -26 161 0 161 -5 200 0 14 -176 -7 0 -224 -18 47 0 -209 -118 -160 0 40 -6 -127 0 165 -227 139 0 38 141 -8 0 18 132 157 0 -82 50 -234 0 208 71 -219 0 -24 239 -167 0 -163 50 -23 0 104 -112 19 0 126 -8 -159 0 72 207 9 0 -230 -65 72 0 29 139 -134 0 -188 -163 91 0 -66 -49 23 0 162 229 171 0 -249 85 -76 0 -174 198 44 0 163 170 -112 0 -184 141 -150 0 -69 27 -151 0 244 -45 5 0 229 114 13 0 -43 250 189 0 -32 -52 -172 0 104 27 246 0 -174 9 86 0 243 56 -138 0 -24 120 225 0 -244 -56 144 0 -134 90 -128 0 171 -17 -152 0 -31 -188 34 0 144 -217 229 0 212 172 58 0 207 219 -134 0 -227 18 -244 0 -106 -54 127 0 -249 -116 -36 0 230 195 -137 0 -82 6 192 0 -192 -66 57 0 124 -48 134 0 70 -185 -221 0 -71 -142 -149 0 179 -10 203 0 -160 166 107 0 -47 -224 97 0 36 -45 -219 0 210 -220 -22 0 56 -106 -210 0 -50 135 -100 0 205 147 -174 0 86 112 193 0 -184 -77 -62 0 155 -240 94 0 -48 -47 204 0 97 -158 201 0 168 44 138 0 202 -31 82 0 3 140 7 0 166 -51 52 0 173 44 161 0 149 232 164 0 41 44 42 0 -140 -60 -167 0 -150 -71 -222 0 205 -112 213 0 -235 -133 9 0 -160 210 -145 0 -228 222 -12 0 66 -17 -238 0 -206 173 39 0 -195 -23 156 0 -53 81 34 0 -149 -10 -87 0 78 219 -221 0 242 -211 -111 0 -53 72 172 0 32 77 -174 0 181 173 215 0 -221 -160 87 0 -130 -216 -53 0 139 49 2 0 154 38 -103 0 33 -49 247 0 -21 41 201 0 92 -230 95 0 221 24 27 0 185 -68 155 0 45 203 -81 0 156 -24 2 0 -149 -77 -246 0 19 -129 245 0 97 96 92 0 33 -153 -214 0 75 -99 -240 0 93 105 -52 0 60 -116 -89 0 -80 7 -95 0 -182 -41 105 0 112 229 147 0 -77 -148 206 0 -88 46 169 0 176 180 86 0 222 -32 134 0 124 -40 15 0 122 -217 -78 0 183 248 -50 0 35 -27 214 0 27 159 -191 0 -227 126 243 0 -119 234 -29 0 76 11 228 0 -4 -154 -103 0 -25 236 -138 0 -192 65 100 0 246 180 -99 0 -4 201 186 0 -57 79 -210 0 138 70 -154 0 249 -227 57 0 214 -155 -48 0 -238 -182 -122 0 -229 -220 26 0 106 16 -141 0 2 -40 152 0 -176 -101 -217 0 145 150 -76 0 -214 -52 208 0 -60 95 -101 0 126 -105 182 0 89 171 -55 0 -207 233 25 0 -187 108 221 0 -235 192 158 0 61 151 231 0 -176 -152 220 0 -180 -170 36 0 -218 79 199 0 -245 238 -152 0 233 -184 -181 0 -246 149 201 0 156 -32 -38 0 78 3 16 0 -243 -110 161 0 -147 77 42 0 212 -223 188 0 117 -13 202 0 44 219 45 0 -42 201 215 0 103 -170 -118 0 -31 216 112 0 60 -167 -99 0 41 1 209 0 139 91 1 0 179 -149 14 0 185 -249 221 0 -132 26 -187 0 -222 -78 -144 0 -230 -50 33 0 73 -81 -228 0 92 61 -194 0 84 -238 -184 0 164 190 -48 0 249 99 -10 0 111 -151 243 0 -34 -79 179 0 136 -225 -22 0 40 -158 181 0 48 -213 -149 0 -219 -105 127 0 79 -226 192 0 42 -88 57 0 -54 197 -208 0 -34 -82 -135 0 159 106 -234 0 149 -146 151 0 -174 195 191 0 -31 62 45 0 161 80 -46 0 -170 -155 158 0 -105 117 234 0 119 -213 28 0 130 32 -170 0 29 -157 -159 0 -248 88 111 0 -238 148 -198 0 59 212 -180 0 -211 190 181 0 128 -88 164 0 244 159 -169 0 -187 52 -109 0 101 -82 -163 0 180 128 -163 0 118 -136 -58 0 113 166 -128 0 243 206 102 0 -191 98 -216 0 150 -143 102 0 -128 -36 131 0 22 -123 -227 0 -45 -98 -161 0 -200 128 24 0 -104 247 181 0 -27 134 115 0 -6 65 195 0 149 162 185 0 235 -7 249 0 -47 -25 93 0 -57 -6 233 0 -244 -167 -90 0 -25 47 -118 0 80 91 183 0 175 146 129 0 117 179 114 0 -126 94 192 0 172 56 -137 0 -215 -95 -84 0 -2 98 -79 0 238 232 -131 0 127 -207 75 0 158 -93 -162 0 38 -97 -21 0 -54 245 -41 0 -84 -113 -137 0 195 -90 173 0 125 65 187 0 -214 147 -165 0 -177 -71 152 0 122 38 138 0 -225 -196 191 0 -241 -90 163 0 -246 90 -168 0 -67 -250 -6 0 -244 87 -247 0 -232 -69 -194 0 -19 -207 248 0 203 129 213 0 56 105 35 0 21 -66 -88 0 -16 178 -250 0 117 118 171 0 -238 2 -183 0 236 -179 -77 0 22 11 -215 0 40 43 -89 0 -4 -118 56 0 -228 -219 -107 0 -133 -155 -157 0 107 197 -157 0 232 -95 -228 0 8 137 97 0 168 -39 -48 0 -3 82 121 0 -56 -146 243 0 147 199 141 0 -103 27 -161 0 28 8 -9 0 -41 -35 39 0 -208 -250 -224 0 -247 -109 -140 0 162 86 186 0 42 -64 34 0 8 179 100 0 124 -48 43 0 -38 -243 114 0 86 42 -182 0 47 -155 -31 0 -145 213 -97 0 37 -133 -235 0 -85 -18 224 0 -45 31 146 0 -194 -98 163 0 -142 72 79 0 -176 -103 -220 0 141 -17 -218 0 218 -9 -193 0 121 -179 92 0 -150 44 -91 0 66 208 -9 0 -236 8 -207 0 115 -90 -180 0 -51 74 -93 0 161 -6 38 0 -158 50 -27 0 107 71 151 0 -235 -138 112 0 -79 -246 -137 0 -165 48 -249 0 22 207 32 0 192 230 -187 0 -115 -28 98 0 -39 -20 -37 0 -168 106 222 0 -148 -79 227 0 -46 -68 79 0 193 -25 149 0 82 -39 109 0 43 131 -155 0 35 194 -41 0 -112 -169 -235 0 -61 -94 -169 0 -48 216 -207 0 207 -128 51 0 73 -177 -41 0 30 -50 -83 0 158 50 -77 0 -244 -57 176 0 -121 169 138 0 18 -102 -205 0 223 244 -192 0 38 -164 -231 0 76 -234 45 0 -12 -54 -177 0 -177 243 58 0 -24 25 16 0 -147 -117 -186 0 -116 57 159 0 168 -69 147 0 50 144 -115 0 -130 49 190 0 167 161 136 0 -28 154 -174 0 -29 232 51 0 -47 -125 -161 0 77 112 -234 0 -35 173 -159 0 -37 -52 -100 0 -191 -17 -144 0 -9 -240 94 0 106 -227 -188 0 -88 -27 -116 0 193 -233 -191 0 204 134 -196 0 -67 133 127 0 -236 -158 -3 0 -116 84 -23 0 121 22 -202 0 -240 17 -27 0 -73 181 35 0 -226 -76 -244 0 -225 114 -74 0 216 -175 167 0 -16 5 -87 0 -24 -50 22 0 -199 -216 102 0 -152 -78 167 0 114 -138 -245 0 -90 -181 238 0 -164 -155 156 0 -43 77 -11 0 -237 156 -52 0 -223 -168 113 0 -200 -37 207 0 -43 127 242 0 244 -104 -196 0 230 -236 -106 0 6 111 78 0 145 -27 62 0 -188 -5 -152 0 -49 -197 67 0 195 -182 -50 0 210 218 -49 0 63 230 152 0 150 -18 119 0 13 -246 -19 0 -144 -184 151 0 -132 -194 -82 0 -55 -43 -147 0 -70 67 -245 0 9 -130 -187 0 -247 103 110 0 11 178 37 0 -10 162 -60 0 -133 188 -44 0 69 -134 -40 0 181 158 -101 0 -134 -67 -75 0 -187 168 -93 0 223 207 149 0 -177 -153 157 0 215 -88 226 0 213 -12 98 0 218 118 -174 0 -22 86 205 0 193 -29 191 0 -168 211 185 0 174 239 74 0 -28 243 -122 0 -199 -75 -71 0 -191 187 -202 0 -228 203 -157 0 226 20 -171 0 -54 69 -188 0 -160 219 66 0 153 -62 246 0 -51 170 235 0 140 58 -100 0 -6 160 -209 0 -185 -244 197 0 60 -127 129 0 88 -31 241 0 153 -128 -130 0 143 -195 -146 0 80 73 -224 0 -93 -132 73 0 41 24 84 0 -104 -248 -200 0 220 -143 -83 0 95 73 43 0 15 -191 -246 0 -140 -203 205 0 -46 88 48 0 -134 -41 -190 0 -186 1 6 0 92 -84 -46 0 -18 61 -160 0 23 80 231 0 118 -208 -92 0 -240 109 249 0 -100 178 151 0 102 33 -133 0 -154 28 246 0 185 215 -29 0 24 11 -61 0 -90 107 75 0 -62 103 -121 0 111 -17 -153 0 -177 85 -215 0 -156 -135 247 0 -113 -247 110 0 -26 -49 214 0 -21 -103 -94 0 -174 135 -79 0 124 -245 -75 0 -124 73 -228 0 93 -34 14 0 -134 201 109 0 222 -48 203 0 240 -59 -36 0 46 53 69 0 238 -128 111 0 7 68 240 0 -184 16 161 0 -178 55 155 0 210 -164 -136 0 -104 -174 -49 0 -4 182 50 0 107 230 -109 0 114 43 229 0 -102 -215 -11 0 -158 97 122 0 -189 64 227 0 -81 -165 4 0 114 46 -162 0 -189 -165 133 0 147 60 221 0 64 -204 -95 0 65 -22 -66 0 186 -75 43 0 -15 105 -20 0 -21 -201 -231 0 21 33 -199 0 17 -138 160 0 79 -142 195 0 -226 -3 216 0 -167 -169 -220 0 142 181 221 0 -229 -62 -183 0 -10 222 29 0 65 69 -19 0 49 -230 -87 0 -207 17 -176 0 -222 -85 -33 0 41 -232 -148 0 86 1 59 0 22 80 -101 0 104 -55 243 0 1 204 -184 0 210 -149 139 0 -98 -54 76 0 -27 180 186 0 104 -141 89 0 -195 -171 -26 0 -35 163 -32 0 248 118 -53 0 180 -50 -141 0 -150 -30 -69 0 60 -71 160 0 -218 -233 26 0 248 -154 -163 0 -12 156 -236 0 -80 -171 192 0 137 218 138 0 -159 20 -69 0 -231 16 128 0 80 -78 10 0 -227 -59 202 0 236 -94 -78 0 209 -48 -150 0 -2 213 -183 0 -234 -186 77 0 -25 -226 115 0 -86 129 165 0 -43 -210 101 0 109 239 -47 0 41 102 89 0 174 119 -64 0 110 180 86 0 -78 135 48 0 12 -185 -23 0 210 -17 242 0 -136 57 206 0 -157 -205 229 0 -80 -56 206 0 -161 245 -216 0 75 12 208 0 152 -196 -148 0 -157 51 -198 0 -207 -122 -233 0 -193 160 212 0 101 -167 26 0 149 -135 -31 0 -39 149 226 0 -164 -241 -140 0 113 95 -47 0 88 -104 57 0 -198 60 -174 0 -152 -144 65 0 145 -44 -89 0 -172 -52 86 0 -108 213 193 0 -204 -22 164 0 44 152 162 0 206 -173 85 0 35 128 -77 0 -210 203 -165 0 -6 -71 11 0 187 242 -162 0 -140 55 112 0 249 134 196 0 -27 213 245 0 -180 121 -182 0 200 227 -122 0 -51 -215 25 0 -231 188 6 0 -218 -40 222 0 73 160 -206 0 134 -49 222 0 -225 210 -10 0 -122 102 -137 0 136 -245 -189 0 -193 29 -78 0 144 -166 -226 0 -160 -145 -95 0 119 -16 68 0 155 -29 91 0 12 -78 75 0 -16 -119 -23 0 -125 143 -88 0 186 -182 -247 0 -100 -91 167 0 237 195 130 0 -168 49 -224 0 -133 -164 -100 0 -202 69 94 0 86 171 120 0 -54 -97 248 0 38 77 79 0 219 149 -31 0 231 71 232 0 104 224 -106 0 181 24 -93 0 -165 134 142 0 -80 -31 -179 0 20 -176 234 0 -142 202 61 0 -157 215 -111 0 129 -218 49 0 130 -229 80 0 -217 -197 -199 0 38 125 -129 0 186 29 -128 0 212 -156 149 0 -59 55 -26 0 161 80 -149 0 -37 -68 -6 0 -77 -102 -156 0 136 110 88 0 82 178 -68 0 -59 226 11 0 89 121 109 0 -222 113 127 0 -60 -202 133 0 -160 -68 -179 0 -159 -233 219 0 211 28 -174 0 -94 -72 -220 0 -30 90 -126 0 87 144 57 0 -223 -51 18 0 -103 -18 -245 0 -15 -233 -26 0 228 -233 4 0 231 246 223 0 87 -33 91 0 -176 -27 -99 0 -125 -213 -221 0 63 174 157 0 146 9 62 0 -158 -133 155 0 -80 163 107 0 -166 208 -17 0 -60 -171 -138 0 32 -132 -173 0 215 -158 101 0 199 -235 1 0 -109 -78 -42 0 -90 -24 71 0 142 21 -189 0 -33 -78 96 0 -221 -145 -236 0 56 -58 -226 0 247 -23 -214 0 125 -141 224 0 2 237 165 0 98 90 -7 0 -232 -117 -14 0 147 210 -220 0 63 -151 109 0 124 216 -49 0 -150 -161 9 0 -113 -225 -186 0 73 -79 -108 0 11 2 -36 0 -182 -161 215 0 -149 99 -188 0 -227 -118 157 0 -61 66 167 0 53 -119 -108 0 88 -170 56 0 80 -49 103 0 198 183 -225 0 192 155 -34 0 215 -126 -11 0 218 51 168 0 -28 -182 117 0 -239 -147 5 0 -181 192 4 0 106 16 -202 0 115 56 215 0 -101 -106 -249 0 40 -225 93 0 -145 118 35 0 -224 188 -102 0 90 -169 245 0 121 53 -179 0 -65 60 140 0 250 -249 194 0 120 214 -221 0 -134 -187 -154 0 -58 -191 155 0 -241 20 209 0 -148 123 229 0 51 -138 -219 0 181 67 172 0 -62 -250 217 0 229 245 126 0 -225 9 205 0 131 -232 -28 0 -130 -139 43 0 -195 -198 71 0 160 -135 -101 0 60 -211 -139 0 20 -84 134 0 5 -25 -239 0 -153 103 134 0 -79 -195 -175 0 -61 39 122 0 -102 73 158 0 86 -124 -79 0 -10 74 89 0 183 126 68 0 -17 116 -87 0 213 -166 212 0 173 237 -204 0 237 -70 -200 0 199 -144 -121 0 -63 -17 41 0 -38 -117 -22 0 79 -160 -159 0 158 -147 -37 0 -103 -171 -143 0 -149 -249 159 0 45 -184 -181 0 -238 11 -77 0 -115 201 134 0 150 -160 -27 0 185 -32 211 0 157 15 -41 0 4 -69 233 0 -67 -80 226 0 56 -130 193 0 44 -107 106 0 -111 -107 -92 0 125 197 -241 0 133 93 35 0 141 -98 145 0 157 -223 173 0 -89 -87 -230 0 102 -113 -120 0 48 -102 239 0 -97 -100 129 0 -58 88 30 0 104 190 93 0 5 221 -193 0 20 -110 -14 0 -40 39 72 0 226 87 -91 0 12 171 -131 0 -185 -8 220 0 40 -152 142 0 26 199 -122 0 -100 92 238 0 132 -109 -226 0 -11 148 237 0 -12 66 -20 0 236 -145 -128 0 -8 91 -86 0 51 -162 42 0 -6 -183 -152 0 -111 174 243 0 -58 -62 -5 0 179 -177 87 0 -198 -223 -29 0 -243 -5 134 0 71 -107 220 0 -174 -45 107 0 175 -159 202 0 -128 120 96 0 -107 101 240 0 -65 -204 5 0 -51 -235 -157 0 -153 122 133 0 -41 164 -102 0 53 123 -47 0 78 182 98 0 133 110 -23 0 221 -241 -108 0 -109 -195 66 0 -157 -194 211 0 -97 -63 9 0 232 29 178 0 239 -39 -7 0 248 -1 -106 0 151 117 -190 0 -189 166 -238 0 -15 90 -162 0 -207 -82 -19 0 -124 -176 161 0 -225 140 238 0 89 -189 222 0 209 151 170 0 100 49 95 0 -29 135 -198 0 60 88 76 0 104 -90 -14 0 155 -124 -50 0 -87 -94 -190 0 -203 -241 -86 0 -87 240 37 0 238 -140 128 0 -151 -119 -167 0 91 -28 -5 0 232 161 -208 0 17 147 -127 0 -93 46 54 0 -14 -198 136 0 91 238 105 0 63 250 224 0 158 -85 -181 0 198 -230 36 0 -18 -213 -30 0 230 234 -165 0 147 -142 -183 0 154 69 -85 0 74 49 -202 0 -191 -66 115 0 147 198 241 0 -245 178 211 0 178 201 190 0 -233 -108 -91 0 -87 -156 -205 0 -208 23 -121 0 18 -79 229 0 -183 77 40 0 177 -218 171 0 -198 -90 -15 0 106 238 -58 0 72 -151 -38 0 -149 90 241 0 -19 210 69 0 250 -19 92 0 202 22 45 0 218 -147 -17 0 -170 95 13 0 12 -52 7 0 -83 241 96 0 230 -206 35 0 -141 -183 -6 0 81 108 46 0 -140 30 130 0 223 192 112 0 82 96 72 0 -225 -10 -219 0 -182 248 15 0 -56 -230 -62 0 -57 -98 -113 0 34 248 -75 0 141 88 204 0 15 -1 -118 0 61 -34 188 0 -44 -25 161 0 -135 226 -75 0 153 220 26 0 227 92 95 0 -52 181 105 0 -53 96 98 0 41 137 15 0 54 249 -64 0 174 -81 233 0 -90 -227 34 0 17 -19 -183 0 -154 -23 -72 0 11 192 165 0 -215 -195 100 0 -51 -1 -85 0 -12 -236 104 0 -29 -241 110 0 207 71 -192 0 -246 -37 60 0 244 49 85 0 250 -55 38 0 142 -209 -247 0 -29 -111 197 0 -180 138 75 0 -73 -75 -122 0 -209 152 -220 0 -3 -147 109 0 125 -178 124 0 -110 76 -153 0 -8 137 -57 0 44 -3 111 0 163 2 -13 0 -33 -126 -88 0 171 -58 60 0 56 -249 11 0 -71 -171 58 0 46 96 59 0 219 149 -186 0 42 225 -190 0 -226 -103 180 0 41 -35 -227 0 -155 11 5 0 -23 38 18 0 91 -135 47 0 -212 -211 -197 0 -198 238 -195 0 83 -240 -170 0 -208 -226 25 0 47 25 -4 0 -187 -16 -201 0 -44 104 -135 0 148 -110 -210 0 56 -155 139 0 -199 176 -97 0 -192 206 168 0 -40 132 -177 0 144 18 64 0 -16 -140 165 0 227 169 -220 0 -225 -63 194 0 -216 -245 163 0 -96 -62 -50 0 171 180 -24 0 130 -60 162 0 87 -108 95 0 -62 216 -45 0 7 204 -24 0 -190 33 -118 0 206 247 -12 0 -149 -183 2 0 44 -25 217 0 51 6 -28 0 -12 -3 173 0 80 171 -38 0 -236 -187 66 0 -239 225 53 0 30 -113 58 0 197 198 122 0 -160 -157 8 0 -80 -233 -145 0 -208 -138 226 0 -193 -63 -85 0 196 197 -76 0 -225 -180 -171 0 -1 -159 200 0 68 -86 -1 0 -71 -192 14 0 -109 -137 -210 0 98 176 162 0 -235 -98 247 0 47 61 -211 0 247 174 151 0 -23 188 -228 0 -215 -220 -105 0 -214 -223 49 0 86 -204 -102 0 -6 247 -129 0 -247 30 145 0 153 227 -237 0 208 66 198 0 -47 -112 58 0 -103 163 54 0 189 65 91 0 101 -192 -79 0 62 -156 247 0 -113 208 135 0 228 -209 205 0 -91 -129 -87 0 34 -63 67 0 43 -211 170 0 -63 82 -39 0 -240 229 103 0 216 101 -172 0 -178 -65 196 0 -8 220 55 0 8 72 105 0 190 -9 85 0 84 -168 -195 0 139 -147 -41 0 -179 149 -186 0 8 -84 17 0 219 69 -45 0 148 -194 -164 0 67 -88 -31 0 74 101 -70 0 -204 -91 229 0 6 -171 176 0 -46 -121 -230 0 93 -30 -16 0 44 -210 37 0 -8 -173 -211 0 94 -148 85 0 54 -243 -179 0 -211 -45 170 0 -162 212 -16 0 69 83 157 0 193 -162 -196 0 84 234 135 0 153 -227 132 0 -128 114 12 0 128 -131 -169 0 83 -102 149 0 170 -213 63 0 142 -127 55 0 72 -78 -121 0