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