1 include "logic/equality.ma".
3 (* Inclusion of: LAT070-1.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : LAT070-1 : TPTP v3.7.0. Released v2.6.0. *)
9 (* Domain : Lattice Theory (Ortholattices) *)
11 (* Problem : Given single axiom OL-23A, prove associativity *)
13 (* Version : [MRV03] (equality) axioms. *)
15 (* English : Given a single axiom OL-23A for ortholattices (OL) in terms of *)
17 (* the Sheffer Stroke, prove a Sheffer stroke form of associativity. *)
19 (* Refs : [MRV03] McCune et al. (2003), Sheffer Stroke Bases for Ortholatt *)
21 (* Source : [MRV03] *)
23 (* Names : OL-23A-associativity [MRV03] *)
25 (* Status : Unsatisfiable *)
27 (* Rating : 0.89 v3.4.0, 0.88 v3.3.0, 0.93 v3.1.0, 1.00 v2.7.0, 0.91 v2.6.0 *)
29 (* Syntax : Number of clauses : 2 ( 0 non-Horn; 2 unit; 1 RR) *)
31 (* Number of atoms : 2 ( 2 equality) *)
33 (* Maximal clause size : 1 ( 1 average) *)
35 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
37 (* Number of functors : 4 ( 3 constant; 0-2 arity) *)
39 (* Number of variables : 4 ( 1 singleton) *)
41 (* Maximal term depth : 7 ( 4 average) *)
45 (* -------------------------------------------------------------------------- *)
47 (* ----Single axiom OL-23A *)
49 (* ----Denial of Sheffer stroke associativity *)
50 ntheorem associativity:
51 (∀Univ:Type.∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.
55 ∀f:∀_:Univ.∀_:Univ.Univ.
56 ∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (f (f (f (f B A) (f A C)) D) (f A (f (f A (f (f B B) B)) C))) A.eq Univ (f a (f (f b c) (f b c))) (f c (f (f b a) (f b a))))
69 ntry (nassumption) ##;
72 (* -------------------------------------------------------------------------- *)