%
% Prover9 commands
%

op(400,infix,[^,v,"=>",*]).

clear(auto).
set(hyper_resolution).

% **************************************************************************
% Clauses for Section 5 (logic) (based on file clsn2.pdf dated 2008-29-06)
% **************************************************************************

formulas(usable).

%
% Rule of inference (modus ponens) for FL_ew.
%

-P(x => y) | -P(x) | P(y) # label("MP").

end_of_list.

formulas(assumptions).

%
% Theses axiomatising FLew.
%
%    Note: These theses together with the rule of inference (MP) above 
%    axiomatise the deductive system H of Section 5 of Part II. By Lemma 5.4 
%    of Part II, the deductive system H is FL_ew.
%

P((x => y) => ((y => z) => (x => z)))       # label("(A1)").
P((x => (y => z)) => (y => (x => z)))       # label("(A2)").
P(x => (y => x))                            # label("(A3)").
P(x => (y => (x * y)))                      # label("(A4)").
P((x => (y => z)) => ((x * y) => z))        # label("(A5)").

P((x ^ y) => x)                             # label("(A6)").
P((x ^ y) => y)                             # label("(A7)").
P((x => y) => ((x => z) => (x => (y ^ z)))) # label("(A8)").

P(x => (x v y))                             # label("(A9)").
P(y => (x v y))                             # label("(A10)").
P((x => z) => ((y => z) => ((x v y) => z))) # label("(A11)").

P(1)                                        # label("(A12)").
P(0 => x)                                   # label("(A13)").

% Current problem (Lemma 5.1)

P(A => B).
P(B => A).
P(C => D).
P(D => C).

-P((A ^ C) => (B ^ D)) | -P((A v C) => (B v D)).

%-P((A ^ C) => (B ^ D)).
%-P((A v C) => (B v D)).

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

P((x => y) => ((y => z) => (x => z))).
P((x ^ y) => x).
P((x ^ y) => y).
P((x => y) => ((x => z) => (x => (y ^ z)))).
P(x => (x v y)).
P(x => (y v x)).
P((x => y) => ((z => y) => ((x v z) => y))).
P(A => B).
P(C => D).
P((x => y) => ((x ^ z) => y)).
P((x => y) => ((z ^ x) => y)).
P((B => x) => (A => x)).
P((D => x) => (C => x)).
P(A => (B v x)).
P((x => (B v y)) => ((A v x) => (B v y))).
P(C => (x v D)).
P((A ^ x) => B).
P(((A ^ x) => y) => ((A ^ x) => (B ^ y))).
P((x ^ C) => D).
P((A v C) => (B v D)).
P((A ^ C) => (B ^ D)).

end_of_list.
