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