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