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