:- op(700,xfy,eqv).
:- op(650,xfy,imp).
:- op(600,xfy,or).
:- op(550,xfy,and).
:- op(500,fy,not).
false(f) :- !.
false(not t) :- !.
false(P eqv Q) :- false((P imp Q) and (Q imp P)).
false(P imp Q) :- false(Q or not P).
false(P or Q) :- false(P), false(Q).
false(P and Q) :- (false(P) ; false(Q)).
false(not not P) :- false(P).
false(not(P eqv Q)) :- false(not(P imp Q) or not(Q imp P)).
false(not(P imp Q)) :- false(not(Q or not P)).
false(not(P or Q)) :- false(not P and not Q).
false(not(P and Q)) :- false(not P or not Q).

theorem(T) :- (false(T), write('false'),!;write('true')),nl.