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