Formatted a bit
Refactored a lot; added support for the universal quantifier and existential quantifier