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