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