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