1 include "logic/equality.ma".
3 (* Inclusion of: LAT063-1.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : LAT063-1 : TPTP v3.7.0. Released v2.5.0. *)
9 (* Domain : Lattice Theory *)
11 (* Problem : E62 does not necessarily hold in ortholattices *)
13 (* Version : [EF+02] axioms. *)
17 (* Refs : [EF+02] Ernst et al. (2002), More First-order Test Problems in *)
19 (* Source : [EF+02] *)
21 (* Names : ol-e62 [EF+02] *)
23 (* Status : Satisfiable *)
25 (* Rating : 0.33 v3.2.0, 0.67 v3.1.0, 0.33 v2.6.0, 0.67 v2.5.0 *)
27 (* Syntax : Number of clauses : 12 ( 0 non-Horn; 12 unit; 1 RR) *)
29 (* Number of atoms : 12 ( 12 equality) *)
31 (* Maximal clause size : 1 ( 1 average) *)
33 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
35 (* Number of functors : 7 ( 4 constant; 0-2 arity) *)
37 (* Number of variables : 20 ( 2 singleton) *)
39 (* Maximal term depth : 6 ( 2 average) *)
43 (* -------------------------------------------------------------------------- *)
45 (* ----Include lattice axioms *)
47 (* Inclusion of: Axioms/LAT001-0.ax *)
49 (* -------------------------------------------------------------------------- *)
51 (* File : LAT001-0 : TPTP v3.7.0. Released v1.0.0. *)
53 (* Domain : Lattice Theory *)
55 (* Axioms : Lattice theory (equality) axioms *)
57 (* Version : [McC88] (equality) axioms. *)
61 (* Refs : [Bum65] Bumcroft (1965), Proceedings of the Glasgow Mathematic *)
63 (* : [McC88] McCune (1988), Challenge Equality Problems in Lattice *)
65 (* : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr *)
67 (* Source : [McC88] *)
73 (* Syntax : Number of clauses : 8 ( 0 non-Horn; 8 unit; 0 RR) *)
75 (* Number of atoms : 8 ( 8 equality) *)
77 (* Maximal clause size : 1 ( 1 average) *)
79 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
81 (* Number of functors : 2 ( 0 constant; 2-2 arity) *)
83 (* Number of variables : 16 ( 2 singleton) *)
85 (* Maximal term depth : 3 ( 2 average) *)
89 (* -------------------------------------------------------------------------- *)
91 (* ----The following 8 clauses characterise lattices *)
93 (* -------------------------------------------------------------------------- *)
95 (* -------------------------------------------------------------------------- *)
97 (* ----Ortholattice axioms *)
99 (* ----Denial of E62 *)
101 (∀Univ:Type.∀A:Univ.∀B:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.
104 ∀complement:∀_:Univ.Univ.
105 ∀join:∀_:Univ.∀_:Univ.Univ.
106 ∀meet:∀_:Univ.∀_:Univ.Univ.
109 ∀H0:∀A:Univ.∀B:Univ.eq Univ (meet A B) (complement (join (complement A) (complement B))).
110 ∀H1:∀A:Univ.eq Univ (meet (complement A) A) n0.
111 ∀H2:∀A:Univ.eq Univ (join (complement A) A) n1.
112 ∀H3:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (join (join X Y) Z) (join X (join Y Z)).
113 ∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet (meet X Y) Z) (meet X (meet Y Z)).
114 ∀H5:∀X:Univ.∀Y:Univ.eq Univ (join X Y) (join Y X).
115 ∀H6:∀X:Univ.∀Y:Univ.eq Univ (meet X Y) (meet Y X).
116 ∀H7:∀X:Univ.∀Y:Univ.eq Univ (join X (meet X Y)) X.
117 ∀H8:∀X:Univ.∀Y:Univ.eq Univ (meet X (join X Y)) X.
118 ∀H9:∀X:Univ.eq Univ (join X X) X.
119 ∀H10:∀X:Univ.eq Univ (meet X X) X.eq Univ (meet a (join b (meet a (join (complement a) (meet a b))))) (meet a (join (complement a) (meet a b))))
145 nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10 ##;
146 ntry (nassumption) ##;
149 (* -------------------------------------------------------------------------- *)