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