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