CNF Problem Header Section

%--------------------------------------------------------------------------
% File     : GRP039-7 : TPTP v2.3.0. Bugfixed v1.0.1.
% Domain   : Group Theory (Subgroups)
% Problem  : Subgroups of index 2 are normal
% Version  : [MOW76] (equality) axioms : Augmented.
% English  : If O is a subgroup of G and there are exactly 2 cosets 
%            in G/O, then O is normal [that is, for all x in G and 
%            y in O, x*y*inverse(x) is back in O].

% Refs     : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% Source   : [MOW76]
% Names    : GP2 [MOW76]

% Status   : unsatisfiable
% Rating   : 0.44 v2.2.1, 0.44 v2.2.0, 0.67 v2.1.0, 0.89 v2.0.0
% Syntax   : Number of clauses    :   25 (   2 non-Horn;  13 unit;  12 RR)
%            Number of literals   :   43 (  28 equality)
%            Maximal clause size  :    4 (   1 average)
%            Number of predicates :    2 (   0 propositional; 1-2 arity)
%            Number of functors   :    8 (   5 constant; 0-2 arity)
%            Number of variables  :   38 (   0 singleton)
%            Maximal term depth   :    3 (   1 average)

% Comments : Used to define a subgroup of index two is a theorem which
%            says that {for all x, for all y, there exists a z such that
%            ... (some lines removed here for brevity)
% Bugfixes : v1.0.1 - Duplicate axioms multiply_inverse_left and
%            multiply_inverse_right removed.
%--------------------------------------------------------------------------