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