%
%  Test program for symbolic model checking.
%
:- load_files(sym).
user:file_search_path(common,'../common').
:- ensure_loaded(common(io)).
:- ensure_loaded(common(cnf)).
:- ensure_loaded(common(intext)).

test(F) :-
  write_formula(F), nl,
  to_internal(F, FI),
  symbolic_tableau(FI).

t1 :- test(# <> p v <> # ~ p).
t2 :- test(~ (# <> p v <> # ~ p)).