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