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