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