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