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