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