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