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