CNF Problem Clauses Section

%--------------------------------------------------------------------------
%----Redundant two axioms
input_clause(right_identity,axiom,
    [++equal(multiply(X,identity),X)]).

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

    

%----Denial of theorem
input_clause(b_in_O2,hypothesis,
    [++subgroup_member(b)]).

input_clause(b_times_a_inverse_is_c,hypothesis,
    [++equal(multiply(b,inverse(a)),c)]).

input_clause(a_times_c_is_d,hypothesis,
    [++equal(multiply(a,c),d)]).

input_clause(prove_d_in_O2,conjecture,
    [--subgroup_member(d)]).
%--------------------------------------------------------------------------