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