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