:- [prop_tableau].
:- [parser].

frm_dnf(Cs,NCs) :-
    stepDNF(Cs,Cs0),
    !,
    frm_dnf(Cs0,NCs).
frm_dnf(Cs,Cs).

:- frm_dnf([[p and (neg p)]],Cs), Cs=[[p,neg p]].

sat_file(File) :-
    input2formula(File,Formula),
    sat(Formula).

closed_branch(C) :-
    member(X, C),
    member(neg X, C).

sat(Formula) :-
    frm_dnf([[Formula]],DNF),
    member(C,DNF),
    \+ closed_branch(C).

:- sat((p imp (q imp r)) imp ((p imp q) imp (p imp r))).
:- \+ sat(p and neg p).