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