% benchmark parameters -n4 -m1000

% How many ordered semigroups are there?
% Note that we use the built-in relation <,
% which orders the members of the domain.

op(400, xfx, *).

formula_list(usable).

all x y z ((x*y)*z = x* (y*z)).    % associativity

all x y z (x*y < x*z -> y < z).    % first order axiom

all x y z (y*x < z*x -> y < z).    % second order axiom

end_of_list.

