:- ensure_loaded('../Transformations/to_clauses.pl').
:- ensure_loaded('../Transformations/skolemize.pl').
:- use_module('../Basis/translations.pl').
:- use_module('../Basis/external_operators.pl').
:- ensure_loaded('../Transformations/to_prenex_form').

:- operators_for_external_representation.

%
%  test(+ExternalFormula)
%
test(ExternalFormula) :-
	from_external_to_printable(ExternalFormula, PrintableFormula),
	writeln(PrintableFormula),
	from_external_to_internal(ExternalFormula, Formula),
	prenex(Formula, PrenexFormula),
	from_internal_to_printable(PrenexFormula, PrintablePrenexFormula),
	writeln(PrintablePrenexFormula),
	skolemize(PrenexFormula, SkolemFormula),
	from_internal_to_printable(SkolemFormula, PrintableSkolemFormula),
	writeln(PrintableSkolemFormula),
	clauses(SkolemFormula, Clauses),
	write_clauses(Clauses).


t1 :- test(forall x: (p(x) -> q(x)) -> forall x: p(x) -> forall x: q(x)).
t2 :- test(exists x: forall y: p(x,y) -> forall y: exists x: p(x, y)).
t3 :- test(forall x: forall y: (p(x,y) -> p(y,x)) ^
	   forall x: forall y: forall z: (p(x,y) ^ p(y,z) -> p(x,z)) ^
	   forall x: exists y: p(x,y) ^
	   ~forall x: p(x,x)).