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