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