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