1 include "logic/equality.ma".
3 (* Inclusion of: LAT054-1.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : LAT054-1 : TPTP v3.7.0. Released v2.5.0. *)
9 (* Domain : Lattice Theory *)
11 (* Problem : Countermodel for Megill equation for ortholattices *)
13 (* Version : [McC88] (equality) axioms. *)
17 (* Refs : [McC88] McCune (1988), Challenge Equality Problems in Lattice *)
19 (* : [Meg00] Megill & Pavicic (2000), Equations and State and Latti *)
21 (* : [RW01] Rose & Wilkinson (2001), Application of Model Search *)
23 (* : [EF+02] Ernst et al. (2002), More First-order Test Problems in *)
27 (* Names : sem-rw-2.in [RW01] *)
29 (* : ol-rw2 [EF+02] *)
31 (* Status : Satisfiable *)
33 (* Rating : 0.33 v3.2.0, 0.67 v3.1.0, 0.33 v2.6.0, 0.67 v2.5.0 *)
35 (* Syntax : Number of clauses : 14 ( 0 non-Horn; 14 unit; 1 RR) *)
37 (* Number of atoms : 14 ( 14 equality) *)
39 (* Maximal clause size : 1 ( 1 average) *)
41 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
43 (* Number of functors : 7 ( 4 constant; 0-2 arity) *)
45 (* Number of variables : 23 ( 2 singleton) *)
47 (* Maximal term depth : 10 ( 3 average) *)
51 (* -------------------------------------------------------------------------- *)
53 (* ----Include lattice axioms *)
55 (* Inclusion of: Axioms/LAT001-0.ax *)
57 (* -------------------------------------------------------------------------- *)
59 (* File : LAT001-0 : TPTP v3.7.0. Released v1.0.0. *)
61 (* Domain : Lattice Theory *)
63 (* Axioms : Lattice theory (equality) axioms *)
65 (* Version : [McC88] (equality) axioms. *)
69 (* Refs : [Bum65] Bumcroft (1965), Proceedings of the Glasgow Mathematic *)
71 (* : [McC88] McCune (1988), Challenge Equality Problems in Lattice *)
73 (* : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr *)
75 (* Source : [McC88] *)
81 (* Syntax : Number of clauses : 8 ( 0 non-Horn; 8 unit; 0 RR) *)
83 (* Number of atoms : 8 ( 8 equality) *)
85 (* Maximal clause size : 1 ( 1 average) *)
87 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
89 (* Number of functors : 2 ( 0 constant; 2-2 arity) *)
91 (* Number of variables : 16 ( 2 singleton) *)
93 (* Maximal term depth : 3 ( 2 average) *)
97 (* -------------------------------------------------------------------------- *)
99 (* ----The following 8 clauses characterise lattices *)
101 (* -------------------------------------------------------------------------- *)
103 (* -------------------------------------------------------------------------- *)
105 (* ----Compatibility (6) *)
107 (* ----Invertability (5) *)
109 (* ----Denial of equation in question *)
111 (∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
114 ∀complement:∀_:Univ.Univ.
115 ∀join:∀_:Univ.∀_:Univ.Univ.
116 ∀meet:∀_:Univ.∀_:Univ.Univ.
119 ∀H0:∀X:Univ.eq Univ (complement (complement X)) X.
120 ∀H1:∀X:Univ.eq Univ (meet (complement X) X) n0.
121 ∀H2:∀X:Univ.eq Univ (join (complement X) X) n1.
122 ∀H3:∀X:Univ.∀Y:Univ.eq Univ (complement (meet X Y)) (join (complement X) (complement Y)).
123 ∀H4:∀X:Univ.∀Y:Univ.eq Univ (complement (join X Y)) (meet (complement X) (complement Y)).
124 ∀H5:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (join (join X Y) Z) (join X (join Y Z)).
125 ∀H6:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet (meet X Y) Z) (meet X (meet Y Z)).
126 ∀H7:∀X:Univ.∀Y:Univ.eq Univ (join X Y) (join Y X).
127 ∀H8:∀X:Univ.∀Y:Univ.eq Univ (meet X Y) (meet Y X).
128 ∀H9:∀X:Univ.∀Y:Univ.eq Univ (join X (meet X Y)) X.
129 ∀H10:∀X:Univ.∀Y:Univ.eq Univ (meet X (join X Y)) X.
130 ∀H11:∀X:Univ.eq Univ (join X X) X.
131 ∀H12:∀X:Univ.eq Univ (meet X X) X.eq Univ (join a (meet (complement b) (join (complement a) (meet (complement b) (join a (meet (complement b) (complement a))))))) (join a (meet (complement b) (join (complement a) (meet (complement b) (join a (meet (complement b) (join (complement a) (meet (complement b) a)))))))))
157 nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12 ##;
158 ntry (nassumption) ##;
161 (* -------------------------------------------------------------------------- *)