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