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