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