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