%--------------------------------------------------------------------------
% File     : GRP190-2 : TPTP v2.1.0. Bugfixed v1.2.1.
% Domain   : Group Theory (Lattice Ordered)
% Problem  : Something useful for estimations
% Version  : [Fuc94] (equality) axioms.
%            Theorem formulation : Using a dual definition of =<.
% English  : 

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

% Status   : unsatisfiable
% Rating   : 0.20 v2.1.0, 0.29 v2.0.0
% Syntax   : Number of clauses    :   17 (   0 non-Horn;  17 unit;   2 RR)
%            Number of literals   :   17 (  17 equality)
%            Maximal clause size  :    1 (   1 average)
%            Number of predicates :    1 (   0 propositional; 2-2 arity)
%            Number of functors   :    7 (   3 constant; 0-2 arity)
%            Number of variables  :   33 (   2 singleton)
%            Maximal term depth   :    3 (   2 average)

% Comments : ORDERING LPO inverse > product > greatest_lower_bound >
%            least_upper_bound > identity > a > b
%          : ORDERING LPO greatest_lower_bound > least_upper_bound > 
%            inverse > product > identity > a > b
%          : tptp2X -f tptp -t rm_equality:rstfp GRP190-2.p 
% Bugfixes : v1.2.1 - Duplicate axioms in GRP004-2.ax removed.
%--------------------------------------------------------------------------
input_clause(left_identity,axiom,
    [++ equal(multiply(identity, X), X)]).

input_clause(left_inverse,axiom,
    [++ equal(multiply(inverse(X), X), identity)]).

input_clause(associativity,axiom,
    [++ equal(multiply(multiply(X, Y), Z), multiply(X, multiply(Y, Z)))]).

input_clause(symmetry_of_glb,axiom,
    [++ equal(greatest_lower_bound(X, Y), greatest_lower_bound(Y, X))]).

input_clause(symmetry_of_lub,axiom,
    [++ equal(least_upper_bound(X, Y), least_upper_bound(Y, X))]).

input_clause(associativity_of_glb,axiom,
    [++ equal(greatest_lower_bound(X, greatest_lower_bound(Y, Z)), greatest_lower_bound(greatest_lower_bound(X, Y), Z))]).

input_clause(associativity_of_lub,axiom,
    [++ equal(least_upper_bound(X, least_upper_bound(Y, Z)), least_upper_bound(least_upper_bound(X, Y), Z))]).

input_clause(idempotence_of_lub,axiom,
    [++ equal(least_upper_bound(X, X), X)]).

input_clause(idempotence_of_gld,axiom,
    [++ equal(greatest_lower_bound(X, X), X)]).

input_clause(lub_absorbtion,axiom,
    [++ equal(least_upper_bound(X, greatest_lower_bound(X, Y)), X)]).

input_clause(glb_absorbtion,axiom,
    [++ equal(greatest_lower_bound(X, least_upper_bound(X, Y)), X)]).

input_clause(monotony_lub1,axiom,
    [++ equal(multiply(X, least_upper_bound(Y, Z)), least_upper_bound(multiply(X, Y), multiply(X, Z)))]).

input_clause(monotony_glb1,axiom,
    [++ equal(multiply(X, greatest_lower_bound(Y, Z)), greatest_lower_bound(multiply(X, Y), multiply(X, Z)))]).

input_clause(monotony_lub2,axiom,
    [++ equal(multiply(least_upper_bound(Y, Z), X), least_upper_bound(multiply(Y, X), multiply(Z, X)))]).

input_clause(monotony_glb2,axiom,
    [++ equal(multiply(greatest_lower_bound(Y, Z), X), greatest_lower_bound(multiply(Y, X), multiply(Z, X)))]).

input_clause(p39c_1,hypothesis,
    [++ equal(least_upper_bound(a, b), a)]).

input_clause(prove_p39c,conjecture,
    [-- equal(greatest_lower_bound(inverse(a), inverse(b)), inverse(a))]).
%--------------------------------------------------------------------------