]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/ng_TPTP/LAT059-1.ma
-ng implemented
[helm.git] / helm / software / matita / contribs / ng_TPTP / LAT059-1.ma
1 include "logic/equality.ma".
2
3 (* Inclusion of: LAT059-1.p *)
4
5 (* -------------------------------------------------------------------------- *)
6
7 (*  File     : LAT059-1 : TPTP v3.2.0. Released v2.5.0. *)
8
9 (*  Domain   : Lattice Theory (Ortholattices) *)
10
11 (*  Problem  : Ortholattice theory (equality) axioms *)
12
13 (*  Version  : [McC98b] (equality) axioms. *)
14
15 (*  English  :  *)
16
17 (*  Refs     : [McC98a] McCune (1998), Automatic Proofs and Counterexamples f *)
18
19 (*           : [McC98b] McCune (1998), Email to G. Sutcliffe *)
20
21 (*  Source   : [McC98b] *)
22
23 (*  Names    :  *)
24
25 (*  Status   : Satisfiable *)
26
27 (*  Rating   : 0.00 v3.2.0, 0.33 v3.1.0, 0.00 v2.5.0 *)
28
29 (*  Syntax   : Number of clauses     :   10 (   0 non-Horn;  10 unit;   0 RR) *)
30
31 (*             Number of atoms       :   10 (  10 equality) *)
32
33 (*             Maximal clause size   :    1 (   1 average) *)
34
35 (*             Number of predicates  :    1 (   0 propositional; 2-2 arity) *)
36
37 (*             Number of functors    :    5 (   2 constant; 0-2 arity) *)
38
39 (*             Number of variables   :   19 (   2 singleton) *)
40
41 (*             Maximal term depth    :    4 (   2 average) *)
42
43 (*  Comments :  *)
44
45 (* -------------------------------------------------------------------------- *)
46
47 (* ----Include Ortholattice theory (equality) axioms *)
48
49 (* Inclusion of: Axioms/LAT003-0.ax *)
50
51 (* -------------------------------------------------------------------------- *)
52
53 (*  File     : LAT003-0 : TPTP v3.2.0. Bugfixed v2.2.1. *)
54
55 (*  Domain   : Lattice Theory (Ortholattices) *)
56
57 (*  Axioms   : Ortholattice theory (equality) axioms *)
58
59 (*  Version  : [McC98b] (equality) axioms. *)
60
61 (*  English  :  *)
62
63 (*  Refs     : [McC98a] McCune (1998), Automatic Proofs and Counterexamples f *)
64
65 (*           : [McC98b] McCune (1998), Email to G. Sutcliffe *)
66
67 (*  Source   : [McC98b] *)
68
69 (*  Names    :  *)
70
71 (*  Status   :  *)
72
73 (*  Syntax   : Number of clauses    :   10 (   0 non-Horn;  10 unit;   0 RR) *)
74
75 (*             Number of literals   :   10 (  10 equality) *)
76
77 (*             Maximal clause size  :    1 (   1 average) *)
78
79 (*             Number of predicates :    1 (   0 propositional; 2-2 arity) *)
80
81 (*             Number of functors   :    5 (   2 constant; 0-2 arity) *)
82
83 (*             Number of variables  :   19 (   2 singleton) *)
84
85 (*             Maximal term depth   :    4 (   2 average) *)
86
87 (*  Comments :  *)
88
89 (*  Bugfixes : v2.2.1 - Added clauses top and bottom. *)
90
91 (* -------------------------------------------------------------------------- *)
92
93 (* ----Axioms for an Ortholattice: *)
94
95 (* -------------------------------------------------------------------------- *)
96
97 (* -------------------------------------------------------------------------- *)