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