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