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