% Here is an example that works much better (5 times better) with
% the old version of MACE (MACE 2.0).  The reason is that it is
% entirely relational.  We have to pay the overhead related to
% rewriting (data structures, etc), but no term rewriting occurs.
% (Boolean rewriting occurs, but that is precisely what MACE 2.0
% does so well.)
%
% This is the mutilated checkerboard problem from John McCarthy's
% 1964 Stanford AI memo "A Tough Nut for Proof Procedures".
%
% Of all the proofs I know about, this one comes closest to answersing
% the exact challenge put forth in the memo; that is, showing
% automatically that a set of first-order statements representing the
% 8x8 problem is unsatisfiable.
%
% (Of course, the real AI interest is in discovering the coloring
% argument, so most people focus on the 2n x 2n problem.)
%
% Running MACE with -n8 does not directly show that the
% set is unsatisfiable; it just shows there are no models of size 8;
% but that's all we're really interested in.  In other words, it
% would be fair to include
%   x = 0 | x = 1 | x = 2 | x = 3 | x = 4 | x = 5 | x = 6 | x = 7
% in McCarthy's set; then the MACE result would clearly be correct.
%
% If the board is
%
% (7,0) ... (7,7)
%   .         .
%   .         .
%   .         .
% (0,0) ... (0,7)
%
% G1(x,y) means that (x,y) and the space above are covered by a domino.
% G2(x,y) means that (x,y) and the space to the right are covered by a domino.
% G3(x,y) means that (x,y) and the space below are covered by a domino.
% G4(x,y) means that (x,y) and the space to the left are covered by a domino.
% G5(x,y) means that (x,y) is not allowed to be covered.
%
% S(x,y) is the successor relation for 0 ... 7.
% L(x,y) is the less-than relation for 0 ... 7.
%
% The numbers in comments are McCarthy's axiom numbers.
assign(domain_size, 8).
set(verbose).
formulas(theory).  % (formulas with explicit quantification)
% List the squares that are not allowed to be covered.
% This is unsatisfiable (it should give no models).
all x all y (G5(x,y) <-> (x=0 & y=0) | (x=7 & y=7)). % 11, 12
% Some test cases that are satisfiable:
%
% all x all y (G5(x,y) <-> (x=1 & y=1) | (x=1 & y=2) |
%                          (x=2 & y=2) | (x=3 & y=2) ).
%
% all x all y (G5(x,y) <-> (x=0 & y=1) | (x=7 & y=7)).
%
% all x all y ~G5(x,y).   % complete board -- 12988816 models
end_of_list.
clauses(theory).
% Dominoes don't stick out past the edges of the board.
~G3(0,y).  % 15
~G4(x,0).
~G1(7,y).
~G2(x,7).
S(0,1). S(1,2). S(2,3). S(3,4). S(4,5). S(5,6). S(6,7).  % 1
% To change the board size, update the preceding few clauses.
% The rest of the clauses don't depend on the size of the board.
~S(x,y) | L(x,y).  % 2
~L(x,y) | ~L(y,z) | L(x,z).   % 3a
~L(x,y) | ~L(y,z) | ~S(x,z).  % 3b
~L(x,y)  | x != y.  % 4
% = is built in, se we don't include McCarthy's axiom 5.
% Every square must satisfy a Gi.
G1(x,y) | G2(x,y) | G3(x,y) | G4(x,y) | G5(x,y).  % 6
% Every square satisfies at most one Gi.
~G1(x,y) | ~G2(x,y).  % 7
~G1(x,y) | ~G3(x,y).
~G1(x,y) | ~G4(x,y).
~G1(x,y) | ~G5(x,y).
~G2(x,y) | ~G3(x,y).  % 8
~G2(x,y) | ~G4(x,y).
~G2(x,y) | ~G5(x,y).
~G3(x,y) | ~G4(x,y).  % 9
~G3(x,y) | ~G5(x,y).
~G4(x,y) | ~G5(x,y).  % 10
% Relationships between Gis.
~S(x1,x2) | ~G1(x1,y) |  G3(x2,y).  % 13
~S(x1,x2) |  G1(x1,y) | ~G3(x2,y).
~S(y1,y2) | ~G2(x,y1) |  G4(x,y2).  % 14
~S(y1,y2) |  G2(x,y1) | ~G4(x,y2).
end_of_list.