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