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