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