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