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