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