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