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