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