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