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