%=======================================================================
%
%       Labeled, complete bipartite graphs.
%       Is enumerated by EIS A000225 (0,1,3,7,15,31,63,127,...)
%       (Except that with these axiomatizations we get no
%        solution for cardinality = 2).
%
% See also:
%
% http://mathworld.wolfram.com/CompleteBipartiteGraph.html
% http://www.research.att.com/cgi-bin/access.cgi/as/njas/sequences/eisA.cgi?Anum=A000225
% This shows the reason: [seq(add(binomial(n,i),i=1..n-1)/2,n=2..10)];
%
% http://arp.anu.edu.au/~jks/finder.html
%
%=======================================================================

sort {
        NODE
        cardinality = 5
}


function {
        p:        int -> bool { print: none } %% Just the parity.
        e:        NODE,NODE -> int { commutative } %% Edge-relation: 0 = no edge, 1 = there is an edge.
        g:        NODE,NODE -> NODE { cut } %% Skolem-function for obtaining the third vertex.
}


clause {
        p(0).
        p(2).
        p(1) -> FALSE.
        p(3) -> FALSE.
        e(x,x) -> FALSE.                % No loops.
        e(x,y) > 1 -> FALSE.            % We allow only the values 0 & 1 for e.
%% If x & y are not connected, then there is a third node z with edge to both:
        e(x,y) = 0 -> e(x,g(x,y)).
        e(x,y) = 0 -> e(y,g(x,y)).
%% If x & y are connected, then there is a third node z with an edge to
%% either one, BUT not both:
        e(x,y) -> (1 = (e(x,g(x,y)) + e(y,g(x,y)))).
%% If there is a third vertex which is not connected to NEITHER x nor y,
%% or which is connected to BOTH, then x and y are not connected:
        p(e(x,z) + e(y,z)) -> e(x,y) = 0.
%% No 3-cliques (this one should not be needed!)
%%      e(x,y)+e(y,z)+e(x,z) > 2 -> FALSE.
%% Stipulate that the third node is indeed distinct from both x and y:
        g(x,y) = x -> FALSE.
        g(x,y) = y -> FALSE.
}

setting {
        verbosity stats: full
        stack: maximal
}


end