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