Here is a proof that a length 25 Sheffer equation named C6 (MOL-25A-785) implies modularity. This is a key step in proving that C6 is a short single axiom for modular ortholattices. This proof is 356 steps long! We found it using our method of proof sketches.
Here is a more comprehensive discussion.