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