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