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