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