input_clause(assoc_plus,conjecture,
	     [--distinct(plus(X,plus(Y,Z)),plus(plus(X,Y),Z))]).
input_clause(comm_plus,conjecture,
	     [--distinct(plus(X,Y),plus(Y,X))]).
input_clause(plus_zero,conjecture,
	     [--distinct(plus(X,zero),X)]).
input_clause(homo_1,conjecture,
	     [--distinct(crypt(plus(X,Y),Z),plus(crypt(X,Z),crypt(Y,Z)))]).

input_clause(non_refl,axiom,
	     [--distinct(X,X)]).
%input_clause(distinct_a,axiom,
%	     [--distinct(a,a)]).
%input_clause(distinct_plus,axiom,
%	     [++distinct(X1,X2), ++distinct(Y1,Y2),
%	     --distinct(plus(X1,Y1),plus(X2,Y2))]).