%--------------------------------------------------------------------------
% File     : GRP004-2 : TPTP v7.2.0. Bugfixed v1.2.0.
% Domain   : Group Theory (Lattice Ordered)
% Axioms   : Lattice ordered group (equality) axioms
% Version  : [Fuc94] (equality) axioms.
% English  :

% Refs     : [Fuc94] Fuchs (1994), The Application of Goal-Orientated Heuri
%          : [Sch95] Schulz (1995), Explanation Based Learning for Distribu
% Source   : [Sch95]
% Names    :

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

% Comments : Requires GRP004-0.ax
%--------------------------------------------------------------------------
%----Specification of the least upper bound and greatest lower bound
cnf(symmetry_of_glb,axiom,
    ( greatest_lower_bound(X,Y) = greatest_lower_bound(Y,X) )).

cnf(symmetry_of_lub,axiom,
    ( least_upper_bound(X,Y) = least_upper_bound(Y,X) )).

cnf(associativity_of_glb,axiom,
    ( greatest_lower_bound(X,greatest_lower_bound(Y,Z)) = greatest_lower_bound(greatest_lower_bound(X,Y),Z) )).

cnf(associativity_of_lub,axiom,
    ( least_upper_bound(X,least_upper_bound(Y,Z)) = least_upper_bound(least_upper_bound(X,Y),Z) )).

cnf(idempotence_of_lub,axiom,
    ( least_upper_bound(X,X) = X )).

cnf(idempotence_of_gld,axiom,
    ( greatest_lower_bound(X,X) = X )).

cnf(lub_absorbtion,axiom,
    ( least_upper_bound(X,greatest_lower_bound(X,Y)) = X )).

cnf(glb_absorbtion,axiom,
    ( greatest_lower_bound(X,least_upper_bound(X,Y)) = X )).

%----Monotony of multiply
cnf(monotony_lub1,axiom,
    ( multiply(X,least_upper_bound(Y,Z)) = least_upper_bound(multiply(X,Y),multiply(X,Z)) )).

cnf(monotony_glb1,axiom,
    ( multiply(X,greatest_lower_bound(Y,Z)) = greatest_lower_bound(multiply(X,Y),multiply(X,Z)) )).

cnf(monotony_lub2,axiom,
    ( multiply(least_upper_bound(Y,Z),X) = least_upper_bound(multiply(Y,X),multiply(Z,X)) )).

cnf(monotony_glb2,axiom,
    ( multiply(greatest_lower_bound(Y,Z),X) = greatest_lower_bound(multiply(Y,X),multiply(Z,X)) )).

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