vars(X, [X]) :- atom(X).
vars(non(P), R) :- vars(P, R).
vars(imp(P, Q), R) :- vars(P, RP), vars(Q, RQ), union(RP, RQ, R).
vars(and(P, Q), R) :- vars(P, RP), vars(Q, RQ), union(RP, RQ, R).
vars(or(P, Q),  R) :- vars(P, RP), vars(Q, RQ), union(RP, RQ, R).

val(X, [(X, E) | _], E) :- !.
val(X, [_ | T], E) :- val(X, T, E).
bnon(0, 1) :- !.
bnon(1, 0) :- !.
bor(1, _, 1) :- !. bor(_, 1, 1) :- !. bor(0, 0, 0) :- !.
bimp(P, Q, R) :- bnon(P, NP), bor(NP, Q, R).
band(P, Q, R) :- bnon(P, NP), bnon(Q, NQ), bor(NP, NQ, NR), bnon(NR, R).

eval(X, L, R) :- val(X, L, R).
eval(non(P), L, R) :- eval(P, L, RP), bnon(RP, R).
eval(imp(P, Q), L, R) :- eval(P, L, RP), eval(Q, L, RQ), bimp(RP, RQ, R).
eval(and(P, Q), L, R) :- eval(P, L, RP), eval(Q, L, RQ), band(RP, RQ, R).
eval(or(P, Q),  L, R) :- eval(P, L, RP), eval(Q, L, RQ), bor(RP, RQ, R).

evals(_, [], []) :- !.
evals(P, [H | T], [HR | TR]) :-
    eval(P, H, HR),
    evals(P, T, TR).

cartesian_product([], _, [_], []) :- !.
cartesian_product([], L1, [_ | T2], R) :-
    cartesian_product(L1, L1, T2, R).
cartesian_product([H1 | T1], L1, [H2 | T2], [HR | TR]) :-
    append(H1, H2, HR),
    cartesian_product(T1, L1, [H2 | T2], TR).
cartesian_product(L1, L2, R) :-
    cartesian_product(L1, L1, L2, R).

repeat(L, 1, L) :- !.
repeat(L, N, Result) :-
    cartesian_product(L, [[0], [1]], TempResult),
    NewN is N - 1,
    repeat(TempResult, NewN, Result).
repeat(RepNumber, Result) :-
    repeat([[0], [1]], RepNumber, Result).

zip([], _, []) :- !.
zip(_, [], []) :- !.
zip([H1 | T1], [H2 | T2], [(H1, H2) | TR]) :-
    zip(T1, T2, TR).

ziplist(_, [], []) :- !.
ziplist(L, [H | T], [HR | TR]) :-
    zip(L, H, HR),
    ziplist(L, T, TR).

evs(Vars, Es) :-
    length(Vars, Length),
    repeat(Length, AllEvals),
    ziplist(Vars, AllEvals, Es).

all_evals(Form, Res) :-
    vars(Form, Vars),
    evs(Vars, AllEvals),
    evals(Form, AllEvals, Res).

all_eq_1([1]) :- !.
all_eq_1([1 | T]) :- all_eq_1(T).

taut(Form) :-
    all_evals(Form, Evals),
    all_eq_1(Evals).