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