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