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