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