;-------------------------------------------------------------------------- ; File : GRP002-3 : TPTP v2.2.0. Released v1.0.0. ; Domain : Group Theory ; Problem : Commutator equals identity in groups of order 3 ; Version : [Ove90] (equality) axioms : Incomplete. ; English : In a group, if (for all x) the cube of x is the identity ; (i.e. a group of order 3), then the equation [[x,y],y]= ; identity holds, where [x,y] is the product of x, y, the ; inverse of x and the inverse of y (i.e. the commutator ; of x and y). ; Refs : [Ove90] Overbeek (1990), ATP competition announced at CADE-10 ; : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal ; : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11 ; : [Zha93] Zhang (1993), Automated Proofs of Equality Problems in ; Source : [Ove90] ; Names : CADE-11 Competition Eq-1 [Ove90] ; : THEOREM EQ-1 [LM93] ; : PROBLEM 1 [Zha93] ; : comm.in [OTTER] ; Status : unsatisfiable ; Rating : 0.33 v2.2.0, 0.43 v2.1.0, 0.25 v2.0.0 ; Syntax : Number of clauses : 6 ( 0 non-Horn; 6 unit; 1 RR) ; Number of literals : 6 ( 6 equality) ; Maximal clause size : 1 ( 1 average) ; Number of predicates : 1 ( 0 propositional; 2-2 arity) ; Number of functors : 6 ( 3 constant; 0-2 arity) ; Number of variables : 8 ( 0 singleton) ; Maximal term depth : 5 ( 2 average) ; Comments : Uses an explicit formulation of the commutator. ; : tptp2X -f kif -t rm_equality:rstfp GRP002-3.p ;-------------------------------------------------------------------------- ; left_identity, axiom. (or (= (multiply identity ?A) ?A)) ; left_inverse, axiom. (or (= (multiply (inverse ?A) ?A) identity)) ; associativity, axiom. (or (= (multiply (multiply ?A ?B) ?C) (multiply ?A (multiply ?B ?C)))) ; commutator, axiom. (or (= (commutator ?A ?B) (multiply ?A (multiply ?B (multiply (inverse ?A) (inverse ?B)))))) ; x_cubed_is_identity, hypothesis. (or (= (multiply ?A (multiply ?A ?A)) identity)) ; prove_commutator, conjecture. (or (/= (commutator (commutator a b) b) identity)) ;--------------------------------------------------------------------------