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