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