We show the first 3083 equational first-order formulas with up to five variables. This is done according to an enumeration procedure that assures going through all such formulas, which are in Skolemized form. The function is a pairing function and is an interpretation function.
Wolfram Demonstrations Project
Published: March 7 2011