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