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