1 include "logic/equality.ma".
3 (* Inclusion of: GRP399-1.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : GRP399-1 : TPTP v3.7.0. Released v2.5.0. *)
9 (* Domain : Group Theory (Lattice Ordered) *)
11 (* Problem : Lattice ordered group (equality) axioms *)
13 (* Version : [Fuc94] (equality) axioms. *)
17 (* Refs : [Fuc94] Fuchs (1994), The Application of Goal-Orientated Heuri *)
19 (* : [Sch95] Schulz (1995), Explanation Based Learning for Distribu *)
21 (* Source : [Sch95] *)
25 (* Status : Satisfiable *)
27 (* Rating : 0.33 v2.5.0 *)
29 (* Syntax : Number of clauses : 15 ( 0 non-Horn; 15 unit; 0 RR) *)
31 (* Number of atoms : 15 ( 15 equality) *)
33 (* Maximal clause size : 1 ( 1 average) *)
35 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
37 (* Number of functors : 5 ( 1 constant; 0-2 arity) *)
39 (* Number of variables : 33 ( 2 singleton) *)
41 (* Maximal term depth : 3 ( 2 average) *)
45 (* -------------------------------------------------------------------------- *)
47 (* ----Include Group theory (equality) axioms *)
49 (* Inclusion of: Axioms/GRP004-0.ax *)
51 (* -------------------------------------------------------------------------- *)
53 (* File : GRP004-0 : TPTP v3.7.0. Released v1.0.0. *)
55 (* Domain : Group Theory *)
57 (* Axioms : Group theory (equality) axioms *)
59 (* Version : [MOW76] (equality) axioms : *)
61 (* Reduced > Complete. *)
65 (* Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a *)
67 (* : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr *)
75 (* Syntax : Number of clauses : 3 ( 0 non-Horn; 3 unit; 0 RR) *)
77 (* Number of atoms : 3 ( 3 equality) *)
79 (* Maximal clause size : 1 ( 1 average) *)
81 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
83 (* Number of functors : 3 ( 1 constant; 0-2 arity) *)
85 (* Number of variables : 5 ( 0 singleton) *)
87 (* Maximal term depth : 3 ( 2 average) *)
89 (* Comments : [MOW76] also contains redundant right_identity and *)
91 (* right_inverse axioms. *)
93 (* : These axioms are also used in [Wos88] p.186, also with *)
95 (* right_identity and right_inverse. *)
97 (* -------------------------------------------------------------------------- *)
99 (* ----For any x and y in the group x*y is also in the group. No clause *)
101 (* ----is needed here since this is an instance of reflexivity *)
103 (* ----There exists an identity element *)
105 (* ----For any x in the group, there exists an element y such that x*y = y*x *)
107 (* ----= identity. *)
109 (* ----The operation '*' is associative *)
111 (* -------------------------------------------------------------------------- *)
113 (* ----Include Lattice ordered group (equality) axioms *)
115 (* Inclusion of: Axioms/GRP004-2.ax *)
117 (* -------------------------------------------------------------------------- *)
119 (* File : GRP004-2 : TPTP v3.7.0. Bugfixed v1.2.0. *)
121 (* Domain : Group Theory (Lattice Ordered) *)
123 (* Axioms : Lattice ordered group (equality) axioms *)
125 (* Version : [Fuc94] (equality) axioms. *)
129 (* Refs : [Fuc94] Fuchs (1994), The Application of Goal-Orientated Heuri *)
131 (* : [Sch95] Schulz (1995), Explanation Based Learning for Distribu *)
133 (* Source : [Sch95] *)
139 (* Syntax : Number of clauses : 12 ( 0 non-Horn; 12 unit; 0 RR) *)
141 (* Number of atoms : 12 ( 12 equality) *)
143 (* Maximal clause size : 1 ( 1 average) *)
145 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
147 (* Number of functors : 3 ( 0 constant; 2-2 arity) *)
149 (* Number of variables : 28 ( 2 singleton) *)
151 (* Maximal term depth : 3 ( 2 average) *)
153 (* Comments : Requires GRP004-0.ax *)
155 (* -------------------------------------------------------------------------- *)
157 (* ----Specification of the least upper bound and greatest lower bound *)
159 (* ----Monotony of multiply *)
161 (* -------------------------------------------------------------------------- *)
163 (* -------------------------------------------------------------------------- *)