1 include "logic/equality.ma".
3 (* Inclusion of: LAT050-1.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : LAT050-1 : TPTP v3.7.0. Released v2.5.0. *)
9 (* Domain : Lattice Theory *)
11 (* Problem : Orthomodular lattice is not modular lattice *)
13 (* Version : [McC88] (equality) axioms. *)
17 (* Refs : [McC88] McCune (1988), Challenge Equality Problems in Lattice *)
19 (* : [RW01] Rose & Wilkinson (2001), Application of Model Search *)
21 (* : [EF+02] Ernst et al. (2002), More First-order Test Problems in *)
25 (* Names : mace-f.in [RW01] *)
27 (* : oml-mod [EF+02] *)
29 (* Status : Satisfiable *)
31 (* Rating : 0.33 v3.2.0, 0.67 v3.1.0, 0.33 v2.6.0, 0.67 v2.5.0 *)
33 (* Syntax : Number of clauses : 15 ( 0 non-Horn; 15 unit; 1 RR) *)
35 (* Number of atoms : 15 ( 15 equality) *)
37 (* Maximal clause size : 1 ( 1 average) *)
39 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
41 (* Number of functors : 8 ( 5 constant; 0-2 arity) *)
43 (* Number of variables : 25 ( 2 singleton) *)
45 (* Maximal term depth : 4 ( 2 average) *)
47 (* Comments : This is well known, but it is a good test problem for finite *)
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 (* ----Orthomodular law (8) *)
111 (* ----Denial of modular law: *)
112 ntheorem prove_modular_law:
113 (∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
117 ∀complement:∀_:Univ.Univ.
118 ∀join:∀_:Univ.∀_:Univ.Univ.
119 ∀meet:∀_:Univ.∀_:Univ.Univ.
122 ∀H0:∀X:Univ.∀Y:Univ.eq Univ (join X (meet (complement X) (join X Y))) (join X Y).
123 ∀H1:∀X:Univ.eq Univ (complement (complement X)) X.
124 ∀H2:∀X:Univ.eq Univ (meet (complement X) X) n0.
125 ∀H3:∀X:Univ.eq Univ (join (complement X) X) n1.
126 ∀H4:∀X:Univ.∀Y:Univ.eq Univ (complement (meet X Y)) (join (complement X) (complement Y)).
127 ∀H5:∀X:Univ.∀Y:Univ.eq Univ (complement (join X Y)) (meet (complement X) (complement Y)).
128 ∀H6:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (join (join X Y) Z) (join X (join Y Z)).
129 ∀H7:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet (meet X Y) Z) (meet X (meet Y Z)).
130 ∀H8:∀X:Univ.∀Y:Univ.eq Univ (join X Y) (join Y X).
131 ∀H9:∀X:Univ.∀Y:Univ.eq Univ (meet X Y) (meet Y X).
132 ∀H10:∀X:Univ.∀Y:Univ.eq Univ (join X (meet X Y)) X.
133 ∀H11:∀X:Univ.∀Y:Univ.eq Univ (meet X (join X Y)) X.
134 ∀H12:∀X:Univ.eq Univ (join X X) X.
135 ∀H13:∀X:Univ.eq Univ (meet X X) X.eq Univ (join a (meet b (join a c))) (meet (join a b) (join a c)))
163 nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13 ##;
164 ntry (nassumption) ##;
167 (* -------------------------------------------------------------------------- *)