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