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