Computer-assisted proof of Havel's conjecture on spanning trees of hypercubes for dimension five

Ivan Havel in 1984 published a conjecture claiming that an arbitrary tree of maximum degree at most three on 2ⁿ vertices is a spanning tree of the 𝑛-dimensional hypercube iff its bipartition classes are of the same size. Four decades have passed and the problem is still open; the statement has been verified with computer assistance for 𝑛 ≤ 4 while for larger dimensions its validity is known only for several special cases. This dataset provides a machine-verifiable proof of the validity of Havel's conjecture for dimension 𝑛 = 5 . The submitted files contain the following:
computed_solution – a file containing the proof of Havel's conjecture for dimension 5
program.zip – an archive containing the program used to compute this solution, along with its documentation, including a function that receives a tree on 2⁵ vertices satisfying the assumptions of the conjecture in graphwiz format and outputs the desired embedding