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