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