Formula Generator

number of variables

2

3

4

5

formula number

1

∀

x1

x1f(x1,x1)

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

g

is a pairing function and

f

is an interpretation function.