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