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