#--------------------------------------------------------------------------
# File     : GRP175-3 : TPTP v2.1.0. Bugfixed v1.2.1.
# Domain   : Group Theory (Lattice Ordered)
# Problem  : Positivity is preserved under inner automorphisms
# Version  : [Fuc94] (equality) axioms.
#            Theorem formulation : Variant, and using different definitions 
#            for =<.
# English  : 

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

# Status   : unsatisfiable
# Rating   : 0.20 v2.1.0, 0.14 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   :    4 (   2 average)

# Comments : ORDERING LPO inverse > product > greatest_lower_bound >
#            least_upper_bound > identity > a > b
#          : tptp2X -f setheo:sign -t rm_equality:rstfp GRP175-3.p 
# Bugfixes : v1.2.1 - Duplicate axioms in GRP004-2.ax removed.
#--------------------------------------------------------------------------
# left_identity, axiom.
equal(multiply(identity, X), X) <- .

# left_inverse, axiom.
equal(multiply(inverse(X), X), identity) <- .

# associativity, axiom.
equal(multiply(multiply(X, Y), Z), multiply(X, multiply(Y, Z))) <- .

# symmetry_of_glb, axiom.
equal(greatest_lower_bound(X, Y), greatest_lower_bound(Y, X)) <- .

# symmetry_of_lub, axiom.
equal(least_upper_bound(X, Y), least_upper_bound(Y, X)) <- .

# associativity_of_glb, axiom.
equal(greatest_lower_bound(X, greatest_lower_bound(Y, Z)), greatest_lower_bound(greatest_lower_bound(X, Y), Z)) <- .

# associativity_of_lub, axiom.
equal(least_upper_bound(X, least_upper_bound(Y, Z)), least_upper_bound(least_upper_bound(X, Y), Z)) <- .

# idempotence_of_lub, axiom.
equal(least_upper_bound(X, X), X) <- .

# idempotence_of_gld, axiom.
equal(greatest_lower_bound(X, X), X) <- .

# lub_absorbtion, axiom.
equal(least_upper_bound(X, greatest_lower_bound(X, Y)), X) <- .

# glb_absorbtion, axiom.
equal(greatest_lower_bound(X, least_upper_bound(X, Y)), X) <- .

# monotony_lub1, axiom.
equal(multiply(X, least_upper_bound(Y, Z)), least_upper_bound(multiply(X, Y), multiply(X, Z))) <- .

# monotony_glb1, axiom.
equal(multiply(X, greatest_lower_bound(Y, Z)), greatest_lower_bound(multiply(X, Y), multiply(X, Z))) <- .

# monotony_lub2, axiom.
equal(multiply(least_upper_bound(Y, Z), X), least_upper_bound(multiply(Y, X), multiply(Z, X))) <- .

# monotony_glb2, axiom.
equal(multiply(greatest_lower_bound(Y, Z), X), greatest_lower_bound(multiply(Y, X), multiply(Z, X))) <- .

# p06c_1, hypothesis.
equal(least_upper_bound(identity, b), b) <- .

# prove_p06c, conjecture.
 <- equal(greatest_lower_bound(identity, multiply(inverse(a), multiply(b, a))), identity).

#--------------------------------------------------------------------------