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