set(verbose).

formulas(theory).

all x (x != f(x)).
all x (x = f(f(x))).

all x all y all z (((x * y) * z) = (x * (y * z))).
all x (0 * x = x).
all x (x * 0 = x).
all x (x * inv(x) = 0).
all x (inv(x) * x = 0).

all x (x = f(x * f((inv(x) * f(x)) * f(inv(f(x)))))).

end_of_list.
