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