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