The main purpose of this project is to take a look to the beginning of
the mathematical universe of all possible first-order axiom systems.
To achieve that, it is necessary to enumerate all of them using two
pairing functions and automatic theorem proving.