Spectra/snark-20120808r02/examples/RNG008-6+rm_eq_rstfp.kif

;--------------------------------------------------------------------------
; File     : RNG008-6 : TPTP v2.2.0. Released v1.0.0.
; Domain   : Ring Theory
; Problem  : Boolean rings are commutative
; Version  : [MOW76] axioms : Augmented.
; English  : Given a ring in which for all x, x * x = x, prove that for 
;            all x and y, x * y = y * x.

; Refs     : [MOW76] McCharen et al. (1976), Problems and Experiments for a
;          : [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   : [Ove90]
; Names    : CADE-11 Competition 3 [Ove90]
;          : THEOREM 3 [LM93]

; Status   : unsatisfiable
; Rating   : 0.67 v2.2.0, 0.71 v2.1.0, 0.75 v2.0.0
; Syntax   : Number of clauses    :   22 (   0 non-Horn;  11 unit;  13 RR)
;            Number of literals   :   55 (   2 equality)
;            Maximal clause size  :    5 (   2 average)
;            Number of predicates :    3 (   0 propositional; 2-3 arity)
;            Number of functors   :    7 (   4 constant; 0-2 arity)
;            Number of variables  :   74 (   2 singleton)
;            Maximal term depth   :    2 (   1 average)

; Comments : Supplies multiplication to identity as lemmas
;          : tptp2X -f kif -t rm_equality:rstfp RNG008-6.p 
;--------------------------------------------------------------------------
; additive_identity1, axiom.
(or (sum additive_identity ?A ?A))

; additive_identity2, axiom.
(or (sum ?A additive_identity ?A))

; closure_of_multiplication, axiom.
(or (product ?A ?B (multiply ?A ?B)))

; closure_of_addition, axiom.
(or (sum ?A ?B (add ?A ?B)))

; left_inverse, axiom.
(or (sum (additive_inverse ?A) ?A additive_identity))

; right_inverse, axiom.
(or (sum ?A (additive_inverse ?A) additive_identity))

; associativity_of_addition1, axiom.
(or (not (sum ?A ?B ?C))
    (not (sum ?B ?D ?E))
    (not (sum ?C ?D ?F))
    (sum ?A ?E ?F))

; associativity_of_addition2, axiom.
(or (not (sum ?A ?B ?C))
    (not (sum ?B ?D ?E))
    (not (sum ?A ?E ?F))
    (sum ?C ?D ?F))

; commutativity_of_addition, axiom.
(or (not (sum ?A ?B ?C))
    (sum ?B ?A ?C))

; associativity_of_multiplication1, axiom.
(or (not (product ?A ?B ?C))
    (not (product ?B ?D ?E))
    (not (product ?C ?D ?F))
    (product ?A ?E ?F))

; associativity_of_multiplication2, axiom.
(or (not (product ?A ?B ?C))
    (not (product ?B ?D ?E))
    (not (product ?A ?E ?F))
    (product ?C ?D ?F))

; distributivity1, axiom.
(or (not (product ?A ?B ?C))
    (not (product ?A ?D ?E))
    (not (sum ?B ?D ?F))
    (not (product ?A ?F ?G))
    (sum ?C ?E ?G))

; distributivity2, axiom.
(or (not (product ?A ?B ?C))
    (not (product ?A ?D ?E))
    (not (sum ?B ?D ?F))
    (not (sum ?C ?E ?G))
    (product ?A ?F ?G))

; distributivity3, axiom.
(or (not (product ?A ?B ?C))
    (not (product ?D ?B ?E))
    (not (sum ?A ?D ?F))
    (not (product ?F ?B ?G))
    (sum ?C ?E ?G))

; distributivity4, axiom.
(or (not (product ?A ?B ?C))
    (not (product ?D ?B ?E))
    (not (sum ?A ?D ?F))
    (not (sum ?C ?E ?G))
    (product ?F ?B ?G))

; addition_is_well_defined, axiom.
(or (not (sum ?A ?B ?C))
    (not (sum ?A ?B ?D))
    (= ?C ?D))

; multiplication_is_well_defined, axiom.
(or (not (product ?A ?B ?C))
    (not (product ?A ?B ?D))
    (= ?C ?D))

; x_times_identity_x_is_identity, axiom.
(or (product ?A additive_identity additive_identity))

; identity_times_x_is_identity, axiom.
(or (product additive_identity ?A additive_identity))

; x_squared_is_x, hypothesis.
(or (product ?A ?A ?A))

; a_times_b_is_c, hypothesis.
(or (product a b c))

; prove_b_times_a_is_c, conjecture.
(or (not (product b a c)))

;--------------------------------------------------------------------------