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