prettify(File) :-
        read_clauses(File,Clauses),
%	             get_flag(variable_names, Mode),
%		     set_flag(variable_names, on),
	apply_to_conjuncts(Clauses,replace_variables,PrettyClauses),
%	             set_flag(variable_names, Mode),
	concatenate(File,'-pp',PrettyFile),
	write_clauses(PrettyFile,PrettyClauses).

replace_variables( Wff, Wff1 ) :-
	variables(Wff, V),
	length(V,N),
	new_variables(N,V1),
	substitution(Wff,Wff1,V,V1).
	
new_variables(0,[]):- !.
new_variables(1,['X']):- !.
new_variables(2,['X','Y']):- !.
new_variables(3,['X','Y','Z']):- !.
/*
new_variables(4,['W','X','Y','Z']):- !.
new_variables(5,['V','W','X','Y','Z']):- !.
new_variables(6,['U','V','W','X','Y','Z']):- !.
new_variables(7,['T','U','V','W','X','Y','Z']):- !.
new_variables(8,['S','T','U','V','W','X','Y','Z']):- !.
new_variables(9,['R','S','T','U','V','W','X','Y','Z']):- !.
new_variables(10,['Q','R','S','T','U','V','W','X','Y','Z']):- !.
new_variables(11,['P','Q','R','S','T','U','V','W','X','Y','Z']):- !.
new_variables(_,'i know: it is a hack, so here it ends!').
*/
new_variables(N,L) :-
	N > 3,
	new_variablesX(N,L).

new_variablesX(1,[V1]) :-
	new_variables(1,[V]),
	concatenate(V,1,V1).
new_variablesX(N,[VN|L1]) :-
	N > 1,
	new_variables(1,[V]),
	concatenate(V,N,VN),
	N1 is N - 1,
	new_variablesX(N1,L1).

substitution(Wff1,Wff2,V1,V2) :-
        var(Wff1) ->
	        exchange(Wff1,Wff2,V1,V2);
        atom(Wff1) ->
                Wff2 = Wff1;
        Wff1 = (A1 :- B1) ->
                substitution(A1,A2,V1,V2),
                substitution(B1,B2,V1,V2),
                Wff2 = (A2 :- B2);
        Wff1 = (A1 , B1) ->
                substitution(A1,A2,V1,V2),
                substitution(B1,B2,V1,V2),
                Wff2 = (A2 , B2);
        Wff1 = (A1 ; B1) ->
                substitution(A1,A2,V1,V2),
                substitution(B1,B2,V1,V2),
                Wff2 = (A2 ; B2);
        Wff1 = [A1|Args1] ->
	        substitution(A1,A2,V1,V2),
	        substitution(Args1,Args2,V1,V2),
		Wff2 = [A2|Args2];
        Wff1 =.. [F|Args1] ->
	        substitution(Args1,Args2,V1,V2),
		Wff2 =.. [F|Args2];
        %true ->
                error(substitution:'unknown term').

exchange(_X12,X1,[_X11],[X1]) :-
	_X11==_X12,!.
exchange(_X12,X1,[_X11|_],[X1|_]) :-
	_X11==_X12,!.
exchange(X1,X2,[_|R1],[_|R2]) :-
	exchange(X1,X2,R1,R2).

% ----------------------------------------------------------------------
% -- auxiliary predicates, 

idunion([], L, L).
idunion([Head|L1tail], L2, L3) :-
        idmember(Head, L2),
        !,
        idunion(L1tail, L2, L3).
idunion([Head|L1tail], L2, [Head|L3tail]) :-
        idunion(L1tail, L2, L3tail).

idmember(X1, [X2|_]    )  :- X1 == X2.
idmember(X1, [_,X2|_]  )  :- X1 == X2.
idmember(X1, [_,_,X2|_])  :- X1 == X2.
idmember(X , [_,_,_ |L])  :- idmember(X, L).