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