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