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