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