%=======================================================================
%
%       Labeled, boron trees counted by their leaves.
%       Is enumerated by EIS A001147 (1,1,3,15,105,945,10395,...)
%
% See also:
%
% http://www.research.att.com/cgi-bin/access.cgi/as/njas/sequences/eisA.cgi?Anum=A
%
%
% http://arp.anu.edu.au/~jks/finder.html
%
% See the following two papers from Peter J. Cameron:
% Orbits of permutation groups on unordered sets, IV: homogeneity and transitivity, J. London Math. Soc. (2) 27 (1983), 238-247.
% and
% Some treelike objects, Quart. J. Math. Oxford (2) 38 (1987), 155-183.
%
% On pages 240 & 241 of the former paper, we have five axioms:
%
% A1. If x|yz holds, then x, y, z are distinct.
% A2. If x|yz holds, then x|zy holds.
% A3. If x|yz and x|yw hold, then x|zw holds. (z and w distinct!)
% A4. for any distinct x, y, z, exactly one of x|yz, y|zx, z|xy holds.
% A5. for no four points a,b,c,d it is true that a|bc, b|cd, c|da, d|ab hold.
%
%=======================================================================

sort {
        LEAF
        cardinality = 7
}


function {
        b:        LEAF,LEAF,LEAF -> int.  % b(x,y,z)=1 means that leaf x bifurcates before y and z.
}


clause {
%% Make b actually a boolean function (obtaining only values 0 or 1):
        b(x,y,z) > 1 -> FALSE.
%% Axiom A1:
        b(x,x,y) = 0.
        b(x,y,y) = 0.
        b(x,y,x) = 0.
%% Axiom A2:
        b(x,y,z) -> b(x,z,y).           % The second and third arg commute.
%% Axiom A3:
        TRUE -> z=w; (2 > (b(x,y,z)+b(x,y,w))); b(x,z,w).
%% Axiom A4:
        TRUE -> x = y; y = z; x = z; (b(x,y,z) + b(y,z,x) + b(z,x,y) = 1).
%% Axiom A5:
        (4 = (b(x,y,z)+b(y,z,w)+b(z,w,x)+b(w,x,y))) -> FALSE.
}

setting {
        verbosity stats: full
        stack: maximal
}


end