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