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