%
% Prover9 commands
%

clear(auto).

op(400,infix,[^,v,"->","=>",*]).
op(200,prefix,[~,-]).

lex([0,1,*,^,=>,->,v,~,-]).

assign(order,kbo).
set(lex_order_vars).

set(paramodulation).
set(para_units_only).
clear(back_demod).
set(hyper_resolution).

set(auto_denials).
set(restrict_denials).

% **************************************************************************
% Clauses for Section 4
% **************************************************************************

formulas(assumptions).

%
% Identities axiomatising lattices
%

(x v y) v z = x v (y v z)                 # label("(D1)").
(x ^ y) ^ z = x ^ (y ^ z)                 # label("(D2)").

x v y = y v x                             # label("(D3)").
x ^ y = y ^ x                             # label("(D4)").

x v (x ^ y) = x                           # label("(D5)").
x ^ (x v y) = x                           # label("(D6)").

%
% Identities and quasi-identities axiomatising BCK-algebras
%

(x => y) => ((y => z) => (x => z)) = 1    # label("(BCK1)").
1 => x = x                                # label("(BCK2)").
x => 1 = 1                                # label("(BCK3)").
x => y != 1 | y => x != 1 | x = y         # label("(BCK4)").

%
% Identities axiomatising partially ordered, commutative integral 
% residuated monoids (pocrims)
%
%    Note: These identities axiomatise pocrims when taken in
%    conjunction with the identities and quasi-identities axiomatising  
%    BCK-algebras given above.
%
x * 1 = x                                 # label("(M1)").
x * y = y * x                             # label("(M2)").
(x * y) * z = x * (y * z)                 # label("(M3)").
(x * y) => z = x => (y => z)              # label("(P)").

%
% Identities axiomatising commutative, integral residuated lattices
%
%    Note: These identities axiomatise commutative, integral residuated
%    lattices when taken in conjunction with the identities and 
%    quasi-identities axiomatising pocrims given above.
%
%    Note: This quasi-equational basis for commutative, integral 
%    residuated lattices axiomatises them as structures
%    <A; ^, v, *, =>, 1> with a lattice reduct <A; ^, v>,
%    a pocrim reduct <A; *, =>, 1>, such that (i) 1 is the greatest 
%    element with respect to the lattice partial ordering; and 
%    (ii) the lattice partial order and BCK-algebra partial orders 
%    coincide.
%

x ^ 1 = x                                 # label("(D10)").
x ^ ((x => y) => y) = x                   # label("(3.7)").
(x ^ y) => y = 1                          # label("(3.11)").

%
% Identities axiomatising FL_ew-algebras
%
%    Note: These identities axiomatise FL_ew-algebras
%    when taken in conjunction with the identities and 
%    quasi-identities axiomatising commutative, integral
%    residuated lattices given above.
%

x v 0 = x                                 # label("(D9)").

%
% Definitions mapping Nelson FL_ew-algebras to Nelson algebras
%

% Definition of -> (weak implication) in Nelson FL_ew-algebras
x -> y = x => (x => y)                    # label("(-> def)").

% Definition of ~ (strong negation) in Nelson FL_ew-algebras.
~x = x => 0                               # label("(~ def)").

% Definition of - (weak negation) in Nelson FL_ew-algebras
-x = x => (x => 0)                        # label("(- def)").

%
% Identities axiomatising Nelson FL_ew-algebras. 
%
%    Note: Nelson FL_algebras are 3-potent, distributive classical 
%    FL_ew-algebras satisfying the Nelson identity (N). 
%
%    Note: The identities expressing classicality and the Nelson identity
%    are expressed in terms of the definitions mapping Nelson FL_ew-algebras
%    into Nelson algebras.
%

x => (x => (x => y)) = x => (x => y)      # label("(E_2)"). % 3-potency

(x v y) ^ (x v z) = x v (y ^ z)           # label("(D7)").  % Distributivity
(x ^ y) v (x ^ z) = x ^ (y v z)           # label("(D8)").

~(~x) = x                                 # label("(DN)").  % Classicality

(x -> y) ^ (~y -> ~x) = x => y            # label("(N)").   % Nelson identity

%
% Identities which are known consequences of the theory of FL_ew-algebras
%
%    Note: The following identities are known to hold for BCK-algebras, and
%    hence hold for Nelson FL_ew-algebras.
%

(x => y) => ((z => x) => (z => y)) = 1    # label("(BCK1')").
x => ((x => y) => y) = 1                  # label("(BCK5)").
x => x = 1                                # label("(3.16)").
x => (y => x) = 1                         # label("(3.17)").
x => (y => z) = y => (x => z)             # label("(3.18)").

%
%    Note: The following identities are known to hold for commutative,
%    integral residuated lattices, and hence hold for Nelson FL_ew-algebras.
%

(x * y) v (x * z) = x * (y v z)           # label("(4.1)").
(x => y) ^ (x => z) = x => (y ^ z)        # label("(4.2)").
(x * (x => y)) v y = y                    # label("(4.3)").
(x => y) ^ (z => y) = (x v z) => y        # label("(4.4)").
((x => y) * z) => (x => (y * z)) = 1      # label("(4.5)").

end_of_list.

%
% Previous results
%

formulas(assumptions).

% Lemma 4.3

(x => y) ^ y = y                       # label("(3.13)"). % Lemma 4.3 (1)
(x v y) => y = x => y                  # label("(4.6)"). % Lemma 4.3 (2)
x -> (y => z) = y => (x -> z)          # label("(4.7)"). % Lemma 4.3 (3)
x ^ (~x => y) = x                      # label("(4.8)"). % Lemma 4.3 (4)

% Lemma 4.4

x -> ((y v x) -> z) = x -> z           # label("(4.9)"). % Lemma 4.4 (1)
x -> (~x v y) = x -> y                 # label("(4.10)"). % Lemma 4.4 (2)

x -> x = 1                             # label("(N2)"). % Lemma 4.5
(x -> y) ^ (x -> z) = x -> (y ^ z)     # label("(N5)"). % Lemma 4.6
(x -> y) ^ (~x v y) = ~x v y           # label("(N3)"). % Lemma 4.7
(x ^ y) -> z = x -> (y -> z)           # label("(N6)"). % Lemma 4.8
x ^ (~x v y) = x ^ (x -> y)            # label("(N4)"). % Lemma 4.9

end_of_list.

%
% Current problem (Lemma 4.11)
%

formulas(goals).

(x ^ ~x) ^ (y v ~y) = x ^ ~x           # label("(N1)"). % Lemma 4.11

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

x v x = x.
(x ^ y) => x = 1.
(x * x) => y = x -> y.
(x * y) => (x => (y => z)) = (x * y) -> z.
~ x => 0 = x.
x => ((y ^ (x => z)) => z) = 1.
x => (y -> z) = y => (x => (y => z)).
x => (y => (x => z)) = y => (x -> z).
x => (y => (z => u)) = z => (x => (y => u)).
~ x ^ (y => 0) = (x v y) => 0.
(x v y) => x = y => x.
(x ^ y) -> z = y -> (x -> z).
x -> y = x -> ((z => x) -> y).
x -> ((y => x) -> z) = x -> z.
x ^ (y v ~ x) = x ^ (x -> y).
x ^ ~ x = x ^ (x -> 0).
x ^ (x -> 0) = x ^ ~ x.
x v y = x v (x v y).
x v (x v y) = x v y.
x ^ (y => 0) = (~ x v y) => 0.
(~ x v y) => 0 = x ^ (y => 0).
(x => (y ^ z)) => (x => y) = 1.
(x -> y) ^ y = y.
x v ((y -> x) ^ z) = (y -> x) ^ (x v z).
(x v y) => (y => x) = (x v y) -> x.
(x v y) ^ (x v z) = x v (y ^ (x v z)).
x v (y ^ (x v z)) = (x v y) ^ (x v z).
x ^ (1 => ((y ^ (x => z)) => z)) = x.
x -> y = (x v z) -> (x -> y).
(x v y) -> (x -> z) = x -> z.
x -> (y -> z) = y -> (x -> z).
1 = x => ((x => (y ^ z)) => y).
x => ((x => (y ^ z)) => y) = 1.
x -> ((y * (y => x)) -> z) = (y * (y => x)) -> z.
~ x ^ ~ y = (x v y) => 0.
(x v y) => 0 = ~ x ^ ~ y.
~ x ^ ~ y = ~ (x v y).
x ^ ~ y = ~ (~ x v y).
~ (~ x v y) = x ^ ~ y.
(x ^ ~ y) => 0 = ~ x v y.
(~ x v y) => (x ^ (y => 0)) = (~ x v y) -> 0.
(x v y) -> x = y => ((x v y) => x).
x => ((y v x) => y) = (y v x) -> y.
x ^ ((y ^ (x => z)) => z) = x.
x ^ (((y v x) => z) => z) = x.
x ^ (1 => (((y v x) => (z ^ u)) => z)) = x.
x => (x => y) = (y v x) -> y.
(x v y) -> x = y -> x.
(x * y) -> z = x => (y => (x => (y => z))).
x => (y => (x => (y => z))) = (x * y) -> z.
x => (y => ((z ^ (y => (x => u))) => u)) = 1.
x => (y => (~ z v u)) = (z ^ ~ u) => (x => (y => 0)).
(x ^ ~ y) => (z => (u => 0)) = z => (u => (~ x v y)).
x v (y ^ (z -> x)) = (z -> x) ^ (x v y).
x v (y ^ (x v z)) = x v (y ^ z).
x v (y ^ (y -> x)) = x v (y ^ ~ y).
x ^ (((y v x) => (z ^ u)) => z) = x.
x => (x => (y -> z)) = (x * y) -> z.
(x * y) -> z = x -> (y -> z).
(x -> y) ^ (y v x) = y v (x ^ ~ x).
x -> (y -> ((y => x) -> z)) = (y * (y => x)) -> z.
x ^ (((~ y v x) -> 0) => y) = x.
x => (((~ (x => y) v z) -> 0) => (z => y)) = 1.
x => (((y v ~ (x => z)) -> 0) => (y => z)) = 1.
x => (y => (((y v ~ (x => z)) -> 0) => z)) = 1.
x => (y => (((y v ~ ~ x) -> 0) => 0)) = 1.
x => (y => (((y v x) -> 0) => 0)) = 1.
x => (y => ~ ((y v x) -> 0)) = 1.
(x * (x => y)) -> z = x -> (y -> ((x => y) -> z)).
x -> (y -> ((x => y) -> z)) = (x * (x => y)) -> z.
x -> (y -> z) = (x * (x => y)) -> z.
(x * (x => y)) -> z = x -> (y -> z).
(x * (x -> y)) -> z = x -> ((x => y) -> z).
x -> (y -> z) = x -> ((x => y) -> z).
x -> ((x => y) -> z) = x -> (y -> z).
(x * (x -> y)) -> z = x -> (y -> z).
x -> (y -> z) = x -> ((x -> y) -> z).
x -> ((x -> y) -> z) = x -> (y -> z).
(x v y) -> (((x v y) -> x) -> z) = x -> z.
(x v y) -> ((y -> x) -> z) = x -> z.
((x -> y) ^ (y v x)) -> z = y -> z.
(x v (y ^ ~ y)) -> z = x -> z.
(x ^ ~ x) => (y => ~ (y -> 0)) = 1.
(x ^ ~ y) => (z => ~ u) = z => (u => (~ x v y)).
x => ((x -> 0) => (~ y v y)) = 1.
x => ((x -> 0) => (y v ~ y)) = 1.
(x ^ y) => ((x -> (y -> 0)) => (z v ~ z)) = 1.
((x -> 0) ^ x) => (1 => (y v ~ y)) = 1.
(x ^ (x -> 0)) => (1 => (y v ~ y)) = 1.
(x ^ ~ x) => (1 => (y v ~ y)) = 1.
(x ^ ~ x) => (y v ~ y) = 1.
(x ^ ~ x) ^ (1 => (y v ~ y)) = x ^ ~ x.

end_of_list.