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