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