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