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