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