%--------------------------------------------------------------------------
% File     : LAT002-0 : TPTP v7.2.0. Released v1.0.0.
% Domain   : Lattice Theory
% Axioms   : Lattice theory axioms
% Version  : [MOW76] axioms :
%            Incomplete > Reduced & Augmented > Complete.
% English  :

% Refs     : [MOW76] McCharen et al. (1976), Problems and Experiments for a
%          : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr
% Source   : [MOW76]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of clauses    :   20 (   0 non-Horn;   8 unit;  12 RR)
%            Number of atoms      :   48 (   2 equality)
%            Maximal clause size  :    5 (   2 average)
%            Number of predicates :    3 (   0 propositional; 2-3 arity)
%            Number of functors   :    4 (   2 constant; 0-2 arity)
%            Number of variables  :   66 (   4 singleton)
%            Maximal term depth   :    2 (   1 average)
% SPC      : 

% Comments : These axioms are used in [Wos88] p.215, augmented by some
%            redundant axioms about 0 & 1.
%          : The original [MOW76] axioms have two extra redundant
%            modularity axioms.
%          : [OTTER] uses these too, augmented by some redundant axioms.
%          : The [MOW76] axiomatisation is missing the axioms that make
%            join and meet total functions.
%--------------------------------------------------------------------------
%----Union of n1 and x is equal to n1 :  (n1 v X) = n1
cnf(join_1_and_x,axiom,
    ( join(n1,X,n1) )).

%----Union of x with itself is equal to x :  (X v X) = X
cnf(join_x_and_x,axiom,
    ( join(X,X,X) )).

%----Union of n0 and x is equal to x :  (n0 v X) = X
cnf(join_0_and_x,axiom,
    ( join(n0,X,X) )).

%----Intersection of n0 and x is equal to n0 : (n0 ^ X) = n0
cnf(meet_0_and_x,axiom,
    ( meet(n0,X,n0) )).

%----Intersection of x and itself is equal to x : (X ^ X) = X
cnf(meet_x_and_x,axiom,
    ( meet(X,X,X) )).

%----Intersection of n1 and x is equal to itself : (n1 ^ X) = X
cnf(meet_1_and_x,axiom,
    ( meet(n1,X,X) )).

%----Intersection of x and y , is the same as meet of y and x.
%----  (X ^ Y) = (Y ^ X),
cnf(commutativity_of_meet,axiom,
    ( ~ meet(X,Y,Z)
    | meet(Y,X,Z) )).

%----Union of x and y is the same as join of y and x. (X v Y) = (Y v X),
cnf(commutativity_of_join,axiom,
    ( ~ join(X,Y,Z)
    | join(Y,X,Z) )).

%----Union of x with the meet of x and y is the same as x.
%----  X v (X ^ Y) = X
cnf(absorbtion1,axiom,
    ( ~ meet(X,Y,Z)
    | join(X,Z,X) )).

%----Intersection  of x with the join of x and y is the same as x.
%----  X ^ (X v Y) = X
cnf(absorbtion2,axiom,
    ( ~ join(X,Y,Z)
    | meet(X,Z,X) )).

%----The operation '^', meet ,is associative
%----  X ^ (Y ^ Z) = (X ^ Y) ^ Z
cnf(associativity_of_meet1,axiom,
    ( ~ meet(X,Y,Xy)
    | ~ meet(Y,Z,Yz)
    | ~ meet(X,Yz,Xyz)
    | meet(Xy,Z,Xyz) )).

cnf(associativity_of_meet2,axiom,
    ( ~ meet(X,Y,Xy)
    | ~ meet(Y,Z,Yz)
    | ~ meet(Xy,Z,Xyz)
    | meet(X,Yz,Xyz) )).

%----The operation 'v' is associative X v (Y v Z) = (X v Y) v Z
cnf(associativity_of_join1,axiom,
    ( ~ join(X,Y,Xy)
    | ~ join(Y,Z,Yz)
    | ~ join(X,Yz,Xyz)
    | join(Xy,Z,Xyz) )).

cnf(associativity_of_join2,axiom,
    ( ~ join(X,Y,Xy)
    | ~ join(Y,Z,Yz)
    | ~ join(Xy,Z,Xyz)
    | join(X,Yz,Xyz) )).

%----(X ^ Z) = X implies that (Z ^ (X v Y)) =  (X v (Y ^ Z)),
cnf(modularity1,axiom,
    ( ~ meet(X,Z,X)
    | ~ join(X,Y,X1)
    | ~ meet(Y,Z,Y1)
    | ~ meet(Z,X1,Z1)
    | join(X,Y1,Z1) )).

cnf(modularity2,axiom,
    ( ~ meet(X,Z,X)
    | ~ join(X,Y,X1)
    | ~ meet(Y,Z,Y1)
    | ~ join(X,Y1,Z1)
    | meet(Z,X1,Z1) )).

cnf(meet_total_function_1,axiom,
    ( meet(X,Y,meet_of(X,Y)) )).

cnf(meet_total_function_2,axiom,
    ( ~ meet(X,Y,Z1)
    | ~ meet(X,Y,Z2)
    | Z1 = Z2 )).

cnf(join_total_function_1,axiom,
    ( join(X,Y,join_of(X,Y)) )).

cnf(join_total_function_2,axiom,
    ( ~ join(X,Y,Z1)
    | ~ join(X,Y,Z2)
    | Z1 = Z2 )).

%--------------------------------------------------------------------------