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