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