% benchmark parameters -N10 -p
% This is a problem about an ordering relation. See the e-mail below.
% Note that we don't use < as in the e-mail below, because
% < has a built-in meaning to MACE. We use << instead.
op(700, xfx, <<).
formula_list(usable).
all x exists y (x< -(y< (exists z (x<
% Date: Fri, 08 Jan 1999 15:27:29 +0100
% To: mccune@mcs.anl.gov
%
% Dear Prof. McCune,
%
% I found the following problem: the following 3 axioms for a relation <
% are given:
% 1. all x exists y: x < y
% 2. all x y: x < y => not y < x
% 3. all x y: x < y => exists z: x < z and z < y
%
% One has to find a finite model. It is surprising and not obvious, that a
% finite model exists, and it is not at all to find easily (at least for
% me, may be for you). Since I sometimes work with OTTER, I remembered
% MACE and tried to formulate and solve this problem with MACE, but
% unfortunately was able to do it.
% Is it possible to formulate and solve this problem with MACE and how?
%
% This problem was posed as an exercise in a very small german
% mathematical magazin by Dr. Waldmann, a former colleague of mine, who
% works now at another university. We both agree that the smallest model
% has seven elements.
%
% Sincerely yours
%
% Stefan Kauer