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