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