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