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