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