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