:- ensure_loaded('../Transformations/to_cnf.pl').
:- use_module('../Basis/translations.pl').
:- use_module('../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).

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).
t6 :- test(~p v (q -> ~r)).
t7 :- test((p ^ ~q) v (p ^ r)).
t8 :- test((p v q) <-> ~r).
t9 :- test((p v q) ^ (~q v r)).
t10 :- test((p ^ q) v (~q ^ r)).