2 include "logic/equality.ma".
3 (* Inclusion of: BOO071-1.p *)
4 (* -------------------------------------------------------------------------- *)
5 (* File : BOO071-1 : TPTP v3.1.1. Released v2.6.0. *)
6 (* Domain : Boolean Algebra (Ternary) *)
7 (* Problem : Ternary Boolean Algebra Single axiom is complete, part 5 *)
8 (* Version : [MP96] (equality) axioms. *)
10 (* Refs : [McC98] McCune (1998), Email to G. Sutcliffe *)
11 (* : [MP96] McCune & Padmanabhan (1996), Automated Deduction in Eq *)
14 (* Status : Unsatisfiable *)
15 (* Rating : 0.00 v3.1.0, 0.11 v2.7.0, 0.00 v2.6.0 *)
16 (* Syntax : Number of clauses : 2 ( 0 non-Horn; 2 unit; 1 RR) *)
17 (* Number of atoms : 2 ( 2 equality) *)
18 (* Maximal clause size : 1 ( 1 average) *)
19 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
20 (* Number of functors : 4 ( 2 constant; 0-3 arity) *)
21 (* Number of variables : 7 ( 0 singleton) *)
22 (* Maximal term depth : 5 ( 2 average) *)
23 (* Comments : A UEQ part of BOO035-1 *)
24 (* -------------------------------------------------------------------------- *)
25 theorem prove_tba_axioms_5:
29 \forall inverse:\forall _:Univ.Univ.
30 \forall multiply:\forall _:Univ.\forall _:Univ.\forall _:Univ.Univ.
31 \forall H0:\forall A:Univ.\forall B:Univ.\forall C:Univ.\forall D:Univ.\forall E:Univ.\forall F:Univ.\forall G:Univ.eq Univ (multiply (multiply A (inverse A) B) (inverse (multiply (multiply C D E) F (multiply C D G))) (multiply D (multiply G F E) C)) B.eq Univ (multiply (inverse b) b a) a
34 autobatch paramodulation timeout=100;
38 (* -------------------------------------------------------------------------- *)