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