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