:- ensure_loaded('../Evaluations/tableau.pl').
:- use_module('../Basis/translations.pl').
:- use_module('../Basis/external_operators.pl').

:- operators_for_external_representation.

%
%  test(+ExternalFormula)
%
test(ExternalFormula) :-
	from_external_to_internal(ExternalFormula, Formula),
	create_tableau(Formula, Tableau),
	write_tableau(Tableau).

t1 :- test(~(forall x: (p(x) -> q(x)) -> forall x: p(x) -> forall x: q(x))).

t2 :- test(~(forall x: p(x) -> forall y: p(y))).

t3 :- test(~(exists x: forall y: p(x,y) -> forall y: exists x: p(x,y))).

t4 :- test(~(forall x: (p(x) -> q) <-> exists x: p(x) -> q)).

t5 :- test(~(forall x: p(x) -> exists x: p(x))).

t6 :- test(~(exists x: exists y: p(x,y) -> exists y: exists x: p(y,x))).