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