Satisfy a larger 3-SAT instance (250 variables)

Instance

• Provenance: TfP dogfood fixture — deterministically generated random 3-SAT with a planted satisfying assignment (generator generateCnf in the TfP repository, seed 303, 250 variables, 1065 clauses). Not a research benchmark; satisfiability is guaranteed by construction.
• SHA-256 of the CNF text below: 7548d44a36d06d93496d91f8bf9fa938669129ecec7ae472003717011c7b743a — the same bytes are bound as the Contract's instance reference input.

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