%=======================================================================
%
%       Labeled (nondirected) graphs, with no isolated vertices.
%       Is enumerated by EIS A006129 (0,1,4,41,768,27449,1887284,...)
%
% See also:
%
% http://www.research.att.com/cgi-bin/access.cgi/as/njas/sequences/eisA.cgi?Anum=A006129
% http://arp.anu.edu.au/~jks/finder.html
%
%=======================================================================

sort {
        NODE
        cardinality = 2
}


function {
        e:        NODE,NODE -> bool { commutative }
        f:        NODE -> NODE { cut }
}


clause {
        e(x,x) -> FALSE.                % No loops.
%%      e(x,y) -> e(y,x).               % Non-directional, i.e. bidirectional edges. Already specified above.
        e(x,f(x)).                      % Every vertex connected at least one another vertex.
}

setting {
        verbosity stats: full
        stack: maximal
}


end