Created a tactic that solves large spider diagram MFOLE formulae.
Migrated all MFOLE proofs to the new SMT tactic.