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