mirror of
https://github.com/RAIRLab/Spectra.git
synced 2024-11-24 18:06:32 -05:00
99 lines
3.2 KiB
Text
99 lines
3.2 KiB
Text
|
;--------------------------------------------------------------------------
|
||
|
|
; File : GRP002-1 : TPTP v2.2.0. Released v1.0.0.
|
||
|
|
; Domain : Group Theory
|
||
|
|
; Problem : Commutator equals identity in groups of order 3
|
||
|
|
; Version : [MOW76] axioms.
|
||
|
|
; 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 : [MOW76] McCharen et al. (1976), Problems and Experiments for a
|
||
|
|
; : [OMW76] Overbeek et al. (1976), Complexity and Related Enhance
|
||
|
|
; : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr
|
||
|
|
; : [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
|
||
|
|
; Source : [MOW76]
|
||
|
|
; Names : G6 [MOW76]
|
||
|
|
; : Theorem 1 [OMW76]
|
||
|
|
; : Test Problem 2 [Wos88]
|
||
|
|
; : Commutator Theorem [Wos88]
|
||
|
|
; : CADE-11 Competition 2 [Ove90]
|
||
|
|
; : THEOREM 2 [LM93]
|
||
|
|
; : commutator.ver1.in [ANL]
|
||
|
|
|
||
|
|
; Status : unsatisfiable
|
||
|
|
; Rating : 0.67 v2.2.0, 0.71 v2.1.0, 1.00 v2.0.0
|
||
|
|
; Syntax : Number of clauses : 16 ( 0 non-Horn; 11 unit; 11 RR)
|
||
|
|
; Number of literals : 26 ( 1 equality)
|
||
|
|
; Maximal clause size : 4 ( 1 average)
|
||
|
|
; Number of predicates : 2 ( 0 propositional; 2-3 arity)
|
||
|
|
; Number of functors : 10 ( 8 constant; 0-2 arity)
|
||
|
|
; Number of variables : 26 ( 0 singleton)
|
||
|
|
; Maximal term depth : 2 ( 1 average)
|
||
|
|
|
||
|
|
; Comments :
|
||
|
|
; : tptp2X -f kif -t rm_equality:rstfp GRP002-1.p
|
||
|
|
;--------------------------------------------------------------------------
|
||
|
|
; left_identity, axiom.
|
||
|
|
(or (product identity ?A ?A))
|
||
|
|
|
||
|
|
; right_identity, axiom.
|
||
|
|
(or (product ?A identity ?A))
|
||
|
|
|
||
|
|
; left_inverse, axiom.
|
||
|
|
(or (product (inverse ?A) ?A identity))
|
||
|
|
|
||
|
|
; right_inverse, axiom.
|
||
|
|
(or (product ?A (inverse ?A) identity))
|
||
|
|
|
||
|
|
; total_function1, axiom.
|
||
|
|
(or (product ?A ?B (multiply ?A ?B)))
|
||
|
|
|
||
|
|
; total_function2, axiom.
|
||
|
|
(or (not (product ?A ?B ?C))
|
||
|
|
(not (product ?A ?B ?D))
|
||
|
|
(= ?C ?D))
|
||
|
|
|
||
|
|
; associativity1, axiom.
|
||
|
|
(or (not (product ?A ?B ?C))
|
||
|
|
(not (product ?B ?D ?E))
|
||
|
|
(not (product ?C ?D ?F))
|
||
|
|
(product ?A ?E ?F))
|
||
|
|
|
||
|
|
; associativity2, axiom.
|
||
|
|
(or (not (product ?A ?B ?C))
|
||
|
|
(not (product ?B ?D ?E))
|
||
|
|
(not (product ?A ?E ?F))
|
||
|
|
(product ?C ?D ?F))
|
||
|
|
|
||
|
|
; x_cubed_is_identity_1, hypothesis.
|
||
|
|
(or (not (product ?A ?A ?B))
|
||
|
|
(product ?A ?B identity))
|
||
|
|
|
||
|
|
; x_cubed_is_identity_2, hypothesis.
|
||
|
|
(or (not (product ?A ?A ?B))
|
||
|
|
(product ?B ?A identity))
|
||
|
|
|
||
|
|
; a_times_b_is_c, conjecture.
|
||
|
|
(or (product a b c))
|
||
|
|
|
||
|
|
; c_times_inverse_a_is_d, conjecture.
|
||
|
|
(or (product c (inverse a) d))
|
||
|
|
|
||
|
|
; d_times_inverse_b_is_h, conjecture.
|
||
|
|
(or (product d (inverse b) h))
|
||
|
|
|
||
|
|
; h_times_b_is_j, conjecture.
|
||
|
|
(or (product h b j))
|
||
|
|
|
||
|
|
; j_times_inverse_h_is_k, conjecture.
|
||
|
|
(or (product j (inverse h) k))
|
||
|
|
|
||
|
|
; prove_k_times_inverse_b_is_e, conjecture.
|
||
|
|
(or (not (product k (inverse b) identity)))
|
||
|
|
|
||
|
|
;--------------------------------------------------------------------------
|