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