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