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