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