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