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