Hey PK, this is great! Your idea to use a proofGrid function to visualize which axioms are redundant to the proofs of particular theorems is one of the most innovative pieces of metamathematics that I've seen anyone attempt using FindEquationalProof! Kudos!
