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