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