% This file was generated by Isabelle (most likely Sledgehammer)
% 2017-03-10 17:56:15.847

% Explicit typings (4)
fof(gsy_c_HOL_Oundefined_001t__TPTP____Interpret__Oind, axiom,
    (gg_TPTP_ind(undefined_TPTP_ind(tPTP_ind)))).
fof(gsy_c_Scratch__tptp__translate__54683__16856_Obar__46p_Obnd__union, hypothesis,
    ((![B_1, B_2]: gg_TPTP_ind(scratc1953616460_union(B_1, B_2))))).
fof(gsy_c_fFalse, axiom,
    (gg_bool(fFalse))).
fof(gsy_c_fTrue, axiom,
    (gg_bool(fTrue))).

% Relevant facts (7)
fof(fact_equal__member__defn, axiom,
    ((![B, C]: ((gg_TPTP_ind(B) & gg_TPTP_ind(C)) => (B = C <=> (![D]: (gg_TPTP_ind(D) => (scratc424138589member(D, B) <=> scratc424138589member(D, C))))))))). % equal_member_defn
fof(fact_reflexivity__of__subset, axiom,
    ((![B]: scratc1705778757subset(B, B)))). % reflexivity_of_subset
fof(fact_subset__defn, axiom,
    ((![B, C]: (scratc1705778757subset(B, C) <=> (![D]: (gg_TPTP_ind(D) => (scratc424138589member(D, B) => scratc424138589member(D, C)))))))). % subset_defn
fof(fact_commutativity__of__union, axiom,
    ((![B, C]: scratc1953616460_union(B, C) = scratc1953616460_union(C, B)))). % commutativity_of_union
fof(fact_equal__defn, axiom,
    ((![B, C]: ((gg_TPTP_ind(B) & gg_TPTP_ind(C)) => (B = C <=> (scratc1705778757subset(B, C) & scratc1705778757subset(C, B))))))). % equal_defn
fof(fact_union__defn, axiom,
    ((![B, C, D2]: (scratc424138589member(D2, scratc1953616460_union(B, C)) <=> (scratc424138589member(D2, B) | scratc424138589member(D2, C)))))). % union_defn
fof(fact_subset__union, axiom,
    ((![B, C]: (gg_TPTP_ind(C) => (scratc1705778757subset(B, C) => scratc1953616460_union(B, C) = C))))). % subset_union

% Helper facts (2)
fof(help_pp_2_1_U, axiom,
    (pp(fTrue))).
fof(help_pp_1_1_U, axiom,
    ((~ pp(fFalse)))).

% Conjectures (1)
fof(conj_0, conjecture,
    ((![B2]: (gg_TPTP_ind(B2) => scratc1953616460_union(B2, B2) = B2)))).