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

:- operators_for_external_representation.

%
%  test(+ExternalFormula)
%
test(ExternalFormula) :-
	from_external_to_printable(ExternalFormula, PrintableFormula),
	writeln(PrintableFormula),
	from_external_to_internal(ExternalFormula, Formula),
	cnf(Formula, CNFFormula),
	from_internal_to_printable(CNFFormula, PrintableCNFFormula),
	writeln(PrintableCNFFormula),
	cnf_to_clausal(CNFFormula, Clauses),
	write_clauses(Clauses).



t1 :- test(~((p -> q -> r) -> (p -> q) -> (p -> r))).
t2 :- test((p -> q) -> (r v p ) -> (r v q)).
t3 :- test((~p -> ~q) -> (p -> q)).
t4 :- test(~(p <-> q)).
t5 :- test((p -> q -> r) -> (p -> q) -> (p -> r)).