%--------------------------------------------------------------------------
% File     : GRP002-1 : TPTP v2.1.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.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 tptp -t rm_equality:rstfp GRP002-1.p 
%--------------------------------------------------------------------------
input_clause(left_identity,axiom,
    [++ product(identity, X, X)]).

input_clause(right_identity,axiom,
    [++ product(X, identity, X)]).

input_clause(left_inverse,axiom,
    [++ product(inverse(X), X, identity)]).

input_clause(right_inverse,axiom,
    [++ product(X, inverse(X), identity)]).

input_clause(total_function1,axiom,
    [++ product(X, Y, multiply(X, Y))]).

input_clause(total_function2,axiom,
    [-- product(X, Y, Z),
     -- product(X, Y, W),
     ++ equal(Z, W)]).

input_clause(associativity1,axiom,
    [-- product(X, Y, U),
     -- product(Y, Z, V),
     -- product(U, Z, W),
     ++ product(X, V, W)]).

input_clause(associativity2,axiom,
    [-- product(X, Y, U),
     -- product(Y, Z, V),
     -- product(X, V, W),
     ++ product(U, Z, W)]).

input_clause(x_cubed_is_identity_1,hypothesis,
    [-- product(X, X, Y),
     ++ product(X, Y, identity)]).

input_clause(x_cubed_is_identity_2,hypothesis,
    [-- product(X, X, Y),
     ++ product(Y, X, identity)]).

input_clause(a_times_b_is_c,conjecture,
    [++ product(a, b, c)]).

input_clause(c_times_inverse_a_is_d,conjecture,
    [++ product(c, inverse(a), d)]).

input_clause(d_times_inverse_b_is_h,conjecture,
    [++ product(d, inverse(b), h)]).

input_clause(h_times_b_is_j,conjecture,
    [++ product(h, b, j)]).

input_clause(j_times_inverse_h_is_k,conjecture,
    [++ product(j, inverse(h), k)]).

input_clause(prove_k_times_inverse_b_is_e,conjecture,
    [-- product(k, inverse(b), identity)]).
%--------------------------------------------------------------------------