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