%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP144^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:06:56 AM UTC 2026
% Result : Theorem 15.33s 5.32s
% Output : Refutation 16.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ITP144^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.11 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.22/0.31 % Computer : n002.cluster.edu
% 0.22/0.31 % Model : x86_64 x86_64
% 0.22/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/0.31 % Memory : 8046.5625MB
% 0.22/0.31 % OS : Linux 6.8.0-71-generic
% 0.22/0.31 % CPULimit : 300
% 0.22/0.31 % WCLimit : 300
% 0.22/0.31 % DateTime : Tue Sep 29 20:02:37 UTC 2026
% 0.22/0.31 % CPUTime :
% 0.22/0.31 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.46/1.14 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.58/1.53 % [INFO] Parsing done (386ms).
% 2.58/1.55 % [INFO] Running in sequential loop mode.
% 3.38/1.99 % [INFO] eprover registered as external prover.
% 3.38/2.00 % [INFO] Scanning for conjecture ...
% 3.88/2.18 % [INFO] Found a conjecture (or negated_conjecture) and 111 axioms. Running axiom selection ...
% 4.18/2.34 % [INFO] Axiom selection finished. Selected 111 axioms (removed 0 axioms).
% 4.71/2.57 % [INFO] Problem is higher-order (TPTP THF).
% 4.93/2.60 % [INFO] Type checking passed.
% 4.93/2.61 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 15.33/5.32 % External prover 'e' found a proof!
% 15.33/5.32 % [INFO] Killing All external provers ...
% 15.33/5.32 % Time passed: 4827ms (effective reasoning time: 3763ms)
% 15.33/5.32 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 15.33/5.32 % Axioms used in derivation (111): fact_109_remove__def, conj_0, fact_11_some__eq__ex, fact_22_some__in__eq, fact_51_singleton__conv2, fact_79_rev__image__eqI, fact_7_verit__sko__forall_H_H, fact_19_verit__sko__ex__indirect2, fact_105_DiffD1, fact_3_verit__sko__ex_H, fact_91_Diff__iff, fact_29_Collect__mem__eq, fact_75_empty__is__image, fact_86_inj__singleton, fact_57_Set_Oset__insert, fact_4_verit__sko__forall, fact_40_UNIV__I, fact_53_insert__eq__iff, fact_66_singletonD, fact_55_insert__ident, fact_27_empty__iff, fact_95_insert__Diff1, fact_15_someI, fact_101_insert__Diff, fact_37_Collect__empty__eq__bot, fact_61_top__empty__eq, fact_72_the__elem__eq, fact_76_image__empty, fact_74_image__is__empty, fact_94_Diff__cancel, fact_98_Diff__UNIV, fact_68_Collect__conv__if2, fact_30_bot__set__def, fact_97_insert__Diff__single, fact_64_doubleton__eq__iff, fact_100_Diff__insert2, fact_92_Diff__empty, fact_70_is__singletonE, fact_90_DiffI, fact_93_empty__Diff, fact_43_UNIV__witness, fact_8_someI__ex, fact_78_imageI, fact_26_all__not__in__conv, fact_0_some__equality, fact_81_inv__into__into, fact_71_is__singleton__the__elem, fact_21_Nitpick_OEps__psimp, fact_35_empty__def, fact_59_insertI1, fact_33_equals0I, fact_108_insert__Diff__if, fact_62_singleton__inject, fact_38_bot__empty__eq, fact_104_DiffE, fact_13_tfl__some, fact_85_bij__betw__empty1, fact_73_image__eqI, fact_9_someI2__ex, fact_18_some1__equality, fact_6_verit__sko__forall_H, fact_42_UNIV__eq__I, fact_2_some__sym__eq__trivial, fact_46_is__singletonI, fact_87_inj__img__insertE, fact_25_Collect__empty__eq, fact_60_insertE, fact_39_is__singletonI_H, fact_17_verit__sko__forall__indirect, fact_24_empty__Collect__eq, fact_48_insertCI, fact_20_verit__sko__ex__indirect, fact_80_Compr__image__eq, fact_56_insert__compr, fact_54_insert__absorb, fact_14_Eps__cong, fact_103_in__image__insert__iff, fact_65_singleton__iff, fact_31_emptyE, fact_47_insert__iff, fact_23_exE__some, fact_99_Diff__insert__absorb, fact_67_Collect__conv__if, fact_107_set__diff__eq, fact_28_mem__Collect__eq, fact_16_verit__sko__forall__indirect2, fact_10_someI2__bex, fact_63_insert__not__empty, fact_49_singletonI, fact_102_Diff__insert, fact_77_imageE, fact_88_inj__image__mem__iff, fact_1_some__eq__trivial, fact_36_Set_Ois__empty__def, fact_69_is__singleton__def, fact_5_someI2, fact_32_equals0D, fact_50_singleton__conv, fact_106_DiffD2, fact_83_image__constant__conv, fact_41_Collect__const, fact_44_empty__not__UNIV, fact_89_inj__on__insert, fact_52_mk__disjoint__insert, fact_34_ex__in__conv, fact_82_image__constant, fact_58_insertI2, fact_96_Diff__insert0, fact_12_some__eq__imp, fact_84_bij__betw__empty2, fact_45_iso__tuple__UNIV__I
% 15.33/5.32 % No. of inferences in proof: 226
% 15.33/5.32 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 4827 ms resp. 3763 ms w/o parsing
% 16.10/5.55 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.10/5.55 thf(set_set_b_type, type, set_set_b: $tType).
% 16.10/5.55 thf(set_b_type, type, set_b: $tType).
% 16.10/5.55 thf(b_type, type, b: $tType).
% 16.10/5.55 thf(a_type, type, a: $tType).
% 16.10/5.55 thf(bij_betw_b_b_decl, type, bij_betw_b_b: ((b > b) > (set_b > (set_b > $o)))).
% 16.10/5.55 thf(inj_on_b_set_b_decl, type, inj_on_b_set_b: ((b > set_b) > (set_b > $o))).
% 16.10/5.55 thf(inj_on_b_b_decl, type, inj_on_b_b: ((b > b) > (set_b > $o))).
% 16.10/5.55 thf(minus_minus_set_b_decl, type, minus_minus_set_b: (set_b > (set_b > set_b))).
% 16.10/5.55 thf(hilbert_Eps_b_decl, type, hilbert_Eps_b: ((b > $o) > b)).
% 16.10/5.55 thf(hilbert_inv_into_b_b_decl, type, hilbert_inv_into_b_b: (set_b > ((b > b) > (b > b)))).
% 16.10/5.55 thf(bot_bot_b_o_decl, type, bot_bot_b_o: (b > $o)).
% 16.10/5.55 thf(bot_bot_set_b_decl, type, bot_bot_set_b: set_b).
% 16.10/5.55 thf(top_top_b_o_decl, type, top_top_b_o: (b > $o)).
% 16.10/5.55 thf(top_top_set_b_decl, type, top_top_set_b: set_b).
% 16.10/5.55 thf(collect_b_decl, type, collect_b: ((b > $o) > set_b)).
% 16.10/5.55 thf(image_set_b_set_b_decl, type, image_set_b_set_b: ((set_b > set_b) > (set_set_b > set_set_b))).
% 16.10/5.55 thf(image_b_b_decl, type, image_b_b: ((b > b) > (set_b > set_b))).
% 16.10/5.55 thf(insert_b_decl, type, insert_b: (b > (set_b > set_b))).
% 16.10/5.55 thf(is_empty_b_decl, type, is_empty_b: (set_b > $o)).
% 16.10/5.55 thf(is_singleton_b_decl, type, is_singleton_b: (set_b > $o)).
% 16.10/5.55 thf(remove_b_decl, type, remove_b: (b > (set_b > set_b))).
% 16.10/5.55 thf(the_elem_b_decl, type, the_elem_b: (set_b > b)).
% 16.10/5.55 thf(member_set_b_decl, type, member_set_b: (set_b > (set_set_b > $o))).
% 16.10/5.55 thf(member_b_decl, type, member_b: (b > (set_b > $o))).
% 16.10/5.55 thf(p_decl, type, p: (a > $o)).
% 16.10/5.55 thf(q_decl, type, q: (a > (b > $o))).
% 16.10/5.55 thf(108,axiom,((! [A:(b > $o),B:b,C:(b > $o)]: ((A @ B) => ((! [D:b]: ((A @ D) => (C @ D))) => (C @ (hilbert_Eps_b @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_someI2)).
% 16.10/5.55 thf(519,plain,((! [A:(b > $o),B:b,C:(b > $o)]: ((A @ B) => ((! [D:b]: ((A @ D) => (C @ D))) => (C @ (hilbert_Eps_b @ (A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 16.10/5.55 thf(111,axiom,((! [A:(b > $o),B:b]: ((A @ B) => (A @ (hilbert_Eps_b @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_tfl__some)).
% 16.10/5.55 thf(541,plain,((! [A:(b > $o),B:b]: ((A @ B) => (A @ (hilbert_Eps_b @ (A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 16.10/5.55 thf(7,axiom,((is_singleton_b = (^ [A:set_b]: (A = (insert_b @ (the_elem_b @ A) @ bot_bot_set_b))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_is__singleton__the__elem)).
% 16.10/5.55 thf(138,plain,(((is_singleton_b) = (^ [A:set_b]: (A = (insert_b @ (the_elem_b @ A) @ bot_bot_set_b))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 16.10/5.55 thf(64,axiom,((! [A:b,B:set_b]: ((member_b @ A @ B) => ((insert_b @ A @ (minus_minus_set_b @ B @ (insert_b @ A @ bot_bot_set_b))) = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_insert__Diff)).
% 16.10/5.55 thf(347,plain,((! [A:b,B:set_b]: ((member_b @ A @ B) => ((insert_b @ A @ (minus_minus_set_b @ B @ (insert_b @ A @ bot_bot_set_b))) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 16.10/5.55 thf(60,axiom,((! [A:b,B:set_b,C:b]: ((member_b @ A @ B) => ((image_b_b @ (^ [D:b]: (C)) @ B) = (insert_b @ C @ bot_bot_set_b))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_image__constant)).
% 16.10/5.55 thf(333,plain,((! [A:b,B:set_b,C:b]: ((member_b @ A @ B) => ((image_b_b @ (^ [D:b]: (C)) @ B) = (insert_b @ C @ bot_bot_set_b))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 16.10/5.55 thf(101,axiom,((! [A:(b > $o),B:b]: ((A @ B) => ((! [C:b]: ((A @ C) => (C = B))) => ((hilbert_Eps_b @ A) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_some__equality)).
% 16.10/5.55 thf(481,plain,((! [A:(b > $o),B:b]: ((A @ B) => ((! [C:b]: ((A @ C) => (C = B))) => ((hilbert_Eps_b @ (A)) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 16.10/5.55 thf(46,axiom,((! [A:(b > $o),B:b]: (((A @ B) => ((collect_b @ (^ [C:b]: ((B = C) & (A @ C)))) = (insert_b @ B @ bot_bot_set_b))) & ((~ (A @ B)) => ((collect_b @ (^ [C:b]: ((B = C) & (A @ C)))) = bot_bot_set_b))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_Collect__conv__if2)).
% 16.10/5.55 thf(276,plain,((! [A:(b > $o),B:b]: (((A @ B) => ((collect_b @ (^ [C:b]: ((B = C) & (A @ C)))) = (insert_b @ B @ bot_bot_set_b))) & ((~ (A @ B)) => ((collect_b @ (^ [C:b]: ((B = C) & (A @ C)))) = bot_bot_set_b))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 16.10/5.55 thf(75,axiom,((! [A:(b > b),B:set_b]: ((bij_betw_b_b @ A @ B @ bot_bot_set_b) => (B = bot_bot_set_b)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_bij__betw__empty2)).
% 16.10/5.55 thf(379,plain,((! [A:(b > b),B:set_b]: ((bij_betw_b_b @ (A) @ B @ bot_bot_set_b) => (B = bot_bot_set_b)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 16.10/5.55 thf(77,axiom,((bot_bot_set_b = (collect_b @ (^ [A:b]: (($false)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_empty__def)).
% 16.10/5.55 thf(384,plain,((bot_bot_set_b = (collect_b @ (^ [A:b]: (($false)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 16.10/5.55 thf(110,axiom,((! [A:(b > $o),B:b,C:b]: ((A @ B) => ((~ (A @ C)) => (((hilbert_Eps_b @ A) = C) => ((hilbert_Eps_b @ A) = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_Nitpick_OEps__psimp)).
% 16.10/5.55 thf(533,plain,((! [A:(b > $o),B:b,C:b]: ((A @ B) => ((~ (A @ C)) => (((hilbert_Eps_b @ (A)) = C) => ((hilbert_Eps_b @ (A)) = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 16.10/5.55 thf(105,axiom,((! [A:b,B:(b > $o),C:(b > $o)]: ((A = (hilbert_Eps_b @ B)) => ((! [D:b]: ((B @ D) = (C @ D))) => ((? [D:b]: (C @ D)) = (B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_verit__sko__ex__indirect2)).
% 16.10/5.55 thf(500,plain,((! [A:b,B:(b > $o),C:(b > $o)]: ((A = (hilbert_Eps_b @ (B))) => ((! [D:b]: ((B @ D) = (C @ D))) => ((? [D:b]: (C @ D)) = (B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 16.10/5.55 thf(62,axiom,((! [A:b,B:set_b,C:set_b]: ((member_b @ A @ (minus_minus_set_b @ B @ C)) => (~ ((member_b @ A @ B) => (member_b @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_DiffE)).
% 16.10/5.55 thf(340,plain,((! [A:b,B:set_b,C:set_b]: ((member_b @ A @ (minus_minus_set_b @ B @ C)) => (~ ((member_b @ A @ B) => (member_b @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 16.10/5.55 thf(79,axiom,((! [A:b]: (member_b @ A @ (insert_b @ A @ bot_bot_set_b)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_singletonI)).
% 16.10/5.55 thf(389,plain,((! [A:b]: (member_b @ A @ (insert_b @ A @ bot_bot_set_b)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 16.10/5.55 thf(73,axiom,((! [A:set_b,B:b]: ((A = bot_bot_set_b) => (~ (member_b @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_equals0D)).
% 16.10/5.55 thf(372,plain,((! [A:set_b,B:b]: ((A = bot_bot_set_b) => (~ (member_b @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 16.10/5.55 thf(63,axiom,((! [A:b,B:set_b,C:set_b]: ((member_b @ A @ (minus_minus_set_b @ B @ C)) => (member_b @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_105_DiffD1)).
% 16.10/5.55 thf(344,plain,((! [A:b,B:set_b,C:set_b]: ((member_b @ A @ (minus_minus_set_b @ B @ C)) => (member_b @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 16.10/5.55 thf(68,axiom,((! [A:set_b]: ((! [B:b]: ~ (member_b @ B @ A)) => (A = bot_bot_set_b)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_equals0I)).
% 16.10/5.55 thf(357,plain,((! [A:set_b]: ((! [B:b]: ~ (member_b @ B @ A)) => (A = bot_bot_set_b)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 16.10/5.55 thf(13,axiom,((! [A:b,B:b]: (((insert_b @ A @ bot_bot_set_b) = (insert_b @ B @ bot_bot_set_b)) => (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_singleton__inject)).
% 16.10/5.55 thf(157,plain,((! [A:b,B:b]: (((insert_b @ A @ bot_bot_set_b) = (insert_b @ B @ bot_bot_set_b)) => (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 16.10/5.55 thf(22,axiom,((! [A:set_b]: ((minus_minus_set_b @ A @ bot_bot_set_b) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_Diff__empty)).
% 16.10/5.55 thf(189,plain,((! [A:set_b]: ((minus_minus_set_b @ A @ bot_bot_set_b) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 16.10/5.55 thf(47,axiom,((remove_b = (^ [A:b,B:set_b]: (minus_minus_set_b @ B @ (insert_b @ A @ bot_bot_set_b))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_109_remove__def)).
% 16.10/5.55 thf(284,plain,(((remove_b) = (^ [A:b,B:set_b]: (minus_minus_set_b @ B @ (insert_b @ A @ bot_bot_set_b))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 16.10/5.55 thf(57,axiom,((! [A:b,B:set_b,C:set_b]: ((~ (member_b @ A @ B)) => ((minus_minus_set_b @ B @ (insert_b @ A @ C)) = (minus_minus_set_b @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_Diff__insert0)).
% 16.10/5.55 thf(325,plain,((! [A:b,B:set_b,C:set_b]: ((~ (member_b @ A @ B)) => ((minus_minus_set_b @ B @ (insert_b @ A @ C)) = (minus_minus_set_b @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 16.10/5.55 thf(56,axiom,((! [A:set_b,B:b]: (((A = bot_bot_set_b) => ((image_b_b @ (^ [C:b]: (B)) @ A) = bot_bot_set_b)) & ((A != bot_bot_set_b) => ((image_b_b @ (^ [C:b]: (B)) @ A) = (insert_b @ B @ bot_bot_set_b)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_image__constant__conv)).
% 16.10/5.55 thf(316,plain,((! [A:set_b,B:b]: (((A = bot_bot_set_b) => ((image_b_b @ (^ [C:b]: (B)) @ A) = bot_bot_set_b)) & ((~ (A = bot_bot_set_b)) => ((image_b_b @ (^ [C:b]: (B)) @ A) = (insert_b @ B @ bot_bot_set_b)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 16.10/5.55 thf(103,axiom,((! [A:b,B:b,C:(b > $o)]: ((A = B) => (((hilbert_Eps_b @ C) = B) = ((hilbert_Eps_b @ C) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_verit__sko__forall_H_H)).
% 16.10/5.55 thf(492,plain,((! [A:b,B:b,C:(b > $o)]: ((A = B) => (((hilbert_Eps_b @ (C)) = B) = ((hilbert_Eps_b @ (C)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 16.10/5.55 thf(4,axiom,((! [A:(b > b),B:set_b,C:b,D:set_b]: ((inj_on_b_b @ A @ B) => ((~ (member_b @ C @ D)) => (((insert_b @ C @ D) = (image_b_b @ A @ B)) => (~ (! [E:b,F:set_b]: ((~ (member_b @ E @ F)) => ((B = (insert_b @ E @ F)) => ((C = (A @ E)) => (D != (image_b_b @ A @ F)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_inj__img__insertE)).
% 16.10/5.55 thf(121,plain,((! [A:(b > b),B:set_b,C:b,D:set_b]: ((inj_on_b_b @ (A) @ B) => ((~ (member_b @ C @ D)) => (((insert_b @ C @ D) = (image_b_b @ (A) @ B)) => (~ (! [E:b,F:set_b]: ((~ (member_b @ E @ F)) => ((B = (insert_b @ E @ F)) => ((C = (A @ E)) => (~ (D = (image_b_b @ (A) @ F))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 16.10/5.55 thf(66,axiom,((! [A:b,B:(b > b),C:set_b]: ((member_b @ A @ (image_b_b @ B @ C)) => (member_b @ (hilbert_inv_into_b_b @ C @ B @ A) @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_inv__into__into)).
% 16.10/5.55 thf(353,plain,((! [A:b,B:(b > b),C:set_b]: ((member_b @ A @ (image_b_b @ (B) @ C)) => (member_b @ (hilbert_inv_into_b_b @ C @ (B) @ A) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 16.10/5.55 thf(28,axiom,((! [A:b,B:set_b,C:b,D:set_b]: ((~ (member_b @ A @ B)) => ((~ (member_b @ C @ D)) => (((insert_b @ A @ B) = (insert_b @ C @ D)) = (((A = C) => (B = D)) & ((A != C) => (? [E:set_b]: ((B = (insert_b @ C @ E)) & ~ (member_b @ C @ E) & (D = (insert_b @ A @ E)) & ~ (member_b @ A @ E)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_insert__eq__iff)).
% 16.10/5.55 thf(211,plain,((! [A:b,B:set_b,C:b,D:set_b]: ((~ (member_b @ A @ B)) => ((~ (member_b @ C @ D)) => (((insert_b @ A @ B) = (insert_b @ C @ D)) = (((A = C) => (B = D)) & ((~ (A = C)) => (? [E:set_b]: ((B = (insert_b @ C @ E)) & ~ (member_b @ C @ E) & (D = (insert_b @ A @ E)) & ~ (member_b @ A @ E)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 16.10/5.55 thf(40,axiom,((! [A:b,B:set_b]: ((member_b @ A @ B) => (~ (! [C:set_b]: ((B = (insert_b @ A @ C)) => (member_b @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_Set_Oset__insert)).
% 16.10/5.55 thf(253,plain,((! [A:b,B:set_b]: ((member_b @ A @ B) => (~ (! [C:set_b]: ((B = (insert_b @ A @ C)) => (member_b @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 16.10/5.55 thf(49,axiom,((! [A:b,B:set_b]: ((~ (member_b @ A @ B)) => ((minus_minus_set_b @ (insert_b @ A @ B) @ (insert_b @ A @ bot_bot_set_b)) = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_Diff__insert__absorb)).
% 16.10/5.55 thf(293,plain,((! [A:b,B:set_b]: ((~ (member_b @ A @ B)) => ((minus_minus_set_b @ (insert_b @ A @ B) @ (insert_b @ A @ bot_bot_set_b)) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 16.10/5.55 thf(5,axiom,((! [A:b,B:b,C:b,D:b]: (((insert_b @ A @ (insert_b @ B @ bot_bot_set_b)) = (insert_b @ C @ (insert_b @ D @ bot_bot_set_b))) = (((A = C) & (B = D)) | ((A = D) & (B = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_64_doubleton__eq__iff)).
% 16.10/5.55 thf(132,plain,((! [A:b,B:b,C:b,D:b]: (((insert_b @ A @ (insert_b @ B @ bot_bot_set_b)) = (insert_b @ C @ (insert_b @ D @ bot_bot_set_b))) = (((A = C) & (B = D)) | ((A = D) & (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 16.10/5.55 thf(37,axiom,((! [A:b,B:set_b,C:set_b]: ((member_b @ A @ (minus_minus_set_b @ B @ C)) => (~ (member_b @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_106_DiffD2)).
% 16.10/5.55 thf(243,plain,((! [A:b,B:set_b,C:set_b]: ((member_b @ A @ (minus_minus_set_b @ B @ C)) => (~ (member_b @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 16.10/5.55 thf(44,axiom,((! [A:set_b]: ((minus_minus_set_b @ A @ A) = bot_bot_set_b))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_Diff__cancel)).
% 16.10/5.55 thf(265,plain,((! [A:set_b]: ((minus_minus_set_b @ A @ A) = bot_bot_set_b))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 16.10/5.55 thf(109,axiom,((! [A:(b > $o),B:$o]: (((A @ (hilbert_Eps_b @ (^ [C:b]: ~ (A @ C)))) = B) => ((! [C:b]: (A @ C)) = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_verit__sko__forall_H)).
% 16.10/5.55 thf(529,plain,((! [A:(b > $o),B:$o]: (((A @ (hilbert_Eps_b @ (^ [C:b]: ~ (A @ C)))) = B) => ((! [C:b]: (A @ C)) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 16.10/5.55 thf(25,axiom,((! [A:b,B:set_b,C:set_b]: ((member_b @ A @ (minus_minus_set_b @ B @ C)) = ((member_b @ A @ B) & ~ (member_b @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_Diff__iff)).
% 16.10/5.55 thf(201,plain,((! [A:b,B:set_b,C:set_b]: ((member_b @ A @ (minus_minus_set_b @ B @ C)) = ((member_b @ A @ B) & ~ (member_b @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 16.10/5.55 thf(34,axiom,((! [A:b,B:set_b,C:set_b]: ((member_b @ A @ B) => ((~ (member_b @ A @ C)) => (member_b @ A @ (minus_minus_set_b @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_DiffI)).
% 16.10/5.55 thf(233,plain,((! [A:b,B:set_b,C:set_b]: ((member_b @ A @ B) => ((~ (member_b @ A @ C)) => (member_b @ A @ (minus_minus_set_b @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 16.10/5.55 thf(96,axiom,((((!) @ b) = (^ [A:(b > $o)]: (A @ (hilbert_Eps_b @ (^ [B:b]: ~ (A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_verit__sko__forall)).
% 16.10/5.55 thf(452,plain,((((!) @ b) = (^ [A:(b > $o)]: (A @ (hilbert_Eps_b @ (^ [B:b]: ~ (A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 16.10/5.55 thf(42,axiom,((! [A:b]: (is_singleton_b @ (insert_b @ A @ bot_bot_set_b)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_is__singletonI)).
% 16.10/5.55 thf(260,plain,((! [A:b]: (is_singleton_b @ (insert_b @ A @ bot_bot_set_b)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 16.10/5.55 thf(14,axiom,((insert_b = (^ [A:b,B:set_b]: (collect_b @ (^ [C:b]: ((C = A) | (member_b @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_insert__compr)).
% 16.10/5.55 thf(160,plain,(((insert_b) = (^ [A:b,B:set_b]: (collect_b @ (^ [C:b]: ((C = A) | (member_b @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 16.10/5.55 thf(16,axiom,((! [A:b,B:set_b,C:(b > b)]: ((member_b @ A @ B) => (member_b @ (C @ A) @ (image_b_b @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_imageI)).
% 16.10/5.55 thf(165,plain,((! [A:b,B:set_b,C:(b > b)]: ((member_b @ A @ B) => (member_b @ (C @ A) @ (image_b_b @ (C) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 16.10/5.55 thf(23,axiom,((! [A:b,B:set_b,C:b]: (((~ (member_b @ A @ B)) => (A = C)) => (member_b @ A @ (insert_b @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_48_insertCI)).
% 16.10/5.55 thf(192,plain,((! [A:b,B:set_b,C:b]: (((~ (member_b @ A @ B)) => (A = C)) => (member_b @ A @ (insert_b @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 16.10/5.55 thf(84,axiom,((! [A:b,B:b]: ((member_b @ A @ (insert_b @ B @ bot_bot_set_b)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_singleton__iff)).
% 16.10/5.55 thf(407,plain,((! [A:b,B:b]: ((member_b @ A @ (insert_b @ B @ bot_bot_set_b)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 16.10/5.55 thf(69,axiom,((! [A:b]: ~ (member_b @ A @ bot_bot_set_b))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_empty__iff)).
% 16.10/5.55 thf(361,plain,((! [A:b]: ~ (member_b @ A @ bot_bot_set_b))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 16.10/5.55 thf(58,axiom,((bot_bot_set_b = (collect_b @ bot_bot_b_o))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_bot__set__def)).
% 16.10/5.55 thf(329,plain,((bot_bot_set_b = (collect_b @ (bot_bot_b_o)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 16.10/5.55 thf(32,axiom,((! [A:b,B:(b > b),C:set_b]: ((member_b @ A @ (image_b_b @ B @ C)) => (~ (! [D:b]: ((A = (B @ D)) => (~ (member_b @ D @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_imageE)).
% 16.10/5.55 thf(225,plain,((! [A:b,B:(b > b),C:set_b]: ((member_b @ A @ (image_b_b @ (B) @ C)) => (~ (! [D:b]: ((A = (B @ D)) => (~ (member_b @ D @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 16.10/5.55 thf(100,axiom,((! [A:b,B:(b > $o),C:(b > $o)]: ((A = (hilbert_Eps_b @ (^ [D:b]: ~ (B @ D)))) => ((! [D:b]: ((B @ D) = (C @ D))) => ((! [D:b]: (C @ D)) = (B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_verit__sko__forall__indirect2)).
% 16.10/5.55 thf(476,plain,((! [A:b,B:(b > $o),C:(b > $o)]: ((A = (hilbert_Eps_b @ (^ [D:b]: ~ (B @ D)))) => ((! [D:b]: ((B @ D) = (C @ D))) => ((! [D:b]: (C @ D)) = (B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 16.10/5.55 thf(113,axiom,((! [A:(b > $o),B:b]: ((? [C:b]: ((A @ C) & ! [D:b]: ((A @ D) => (D = C)))) => ((A @ B) => ((hilbert_Eps_b @ A) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_some1__equality)).
% 16.10/5.55 thf(547,plain,((! [A:(b > $o),B:b]: ((? [C:b]: ((A @ C) & ! [D:b]: ((A @ D) => (D = C)))) => ((A @ B) => ((hilbert_Eps_b @ (A)) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 16.10/5.55 thf(81,axiom,((! [A:set_b]: ((A != bot_bot_set_b) => ((! [B:b,C:b]: ((member_b @ B @ A) => ((member_b @ C @ A) => (B = C)))) => (is_singleton_b @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_is__singletonI_H)).
% 16.10/5.55 thf(393,plain,((! [A:set_b]: ((~ (A = bot_bot_set_b)) => ((! [B:b,C:b]: ((member_b @ B @ A) => ((member_b @ C @ A) => (B = C)))) => (is_singleton_b @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 16.10/5.55 thf(107,axiom,((! [A:(b > $o),B:$o]: (((A @ (hilbert_Eps_b @ A)) = B) => ((? [C:b]: (A @ C)) = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_verit__sko__ex_H)).
% 16.10/5.55 thf(515,plain,((! [A:(b > $o),B:$o]: (((A @ (hilbert_Eps_b @ (A))) = B) => ((? [C:b]: (A @ C)) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 16.10/5.55 thf(89,axiom,((! [A:a]: ((p @ A) => (? [B:b]: (q @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 16.10/5.55 thf(425,plain,((! [A:a]: ((p @ A) => (? [B:b]: (q @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 16.10/5.55 thf(50,axiom,((! [A:set_b,B:b,C:set_b]: ((minus_minus_set_b @ A @ (insert_b @ B @ C)) = (minus_minus_set_b @ (minus_minus_set_b @ A @ (insert_b @ B @ bot_bot_set_b)) @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_Diff__insert2)).
% 16.10/5.55 thf(296,plain,((! [A:set_b,B:b,C:set_b]: ((minus_minus_set_b @ A @ (insert_b @ B @ C)) = (minus_minus_set_b @ (minus_minus_set_b @ A @ (insert_b @ B @ bot_bot_set_b)) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 16.10/5.55 thf(95,axiom,((! [A:(b > $o),B:b,C:b]: (((hilbert_Eps_b @ A) = B) => ((A @ C) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_some__eq__imp)).
% 16.10/5.55 thf(444,plain,((! [A:(b > $o),B:b,C:b]: (((hilbert_Eps_b @ (A)) = B) => ((A @ C) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 16.10/5.55 thf(11,axiom,((! [A:b,B:set_b,C:b,D:(b > b)]: ((member_b @ A @ B) => ((C = (D @ A)) => (member_b @ C @ (image_b_b @ D @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_rev__image__eqI)).
% 16.10/5.55 thf(149,plain,((! [A:b,B:set_b,C:b,D:(b > b)]: ((member_b @ A @ B) => ((C = (D @ A)) => (member_b @ C @ (image_b_b @ (D) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 16.10/5.55 thf(82,axiom,((! [A:(b > b),B:set_b]: ((bij_betw_b_b @ A @ bot_bot_set_b @ B) => (B = bot_bot_set_b)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_bij__betw__empty1)).
% 16.10/5.55 thf(402,plain,((! [A:(b > b),B:set_b]: ((bij_betw_b_b @ (A) @ bot_bot_set_b @ B) => (B = bot_bot_set_b)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 16.10/5.55 thf(48,axiom,((! [A:$o]: (((A) => ((collect_b @ (^ [B:b]: (A))) = top_top_set_b)) & ((~ (A)) => ((collect_b @ (^ [B:b]: (A))) = bot_bot_set_b))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_Collect__const)).
% 16.10/5.55 thf(286,plain,((! [A:$o]: (((A) => ((collect_b @ (^ [B:b]: (A))) = top_top_set_b)) & ((~ (A)) => ((collect_b @ (^ [B:b]: (A))) = bot_bot_set_b))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 16.10/5.55 thf(3,axiom,((! [A:b]: ((the_elem_b @ (insert_b @ A @ bot_bot_set_b)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_the__elem__eq)).
% 16.10/5.55 thf(118,plain,((! [A:b]: ((the_elem_b @ (insert_b @ A @ bot_bot_set_b)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 16.10/5.55 thf(26,axiom,((! [A:b,B:set_b]: ((member_b @ A @ B) => (? [C:set_b]: ((B = (insert_b @ A @ C)) & ~ (member_b @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_mk__disjoint__insert)).
% 16.10/5.55 thf(204,plain,((! [A:b,B:set_b]: ((member_b @ A @ B) => (? [C:set_b]: ((B = (insert_b @ A @ C)) & ~ (member_b @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 16.10/5.55 thf(86,axiom,((is_empty_b = (^ [A:set_b]: (A = bot_bot_set_b)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_Set_Ois__empty__def)).
% 16.10/5.55 thf(413,plain,(((is_empty_b) = (^ [A:set_b]: (A = bot_bot_set_b)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 16.10/5.55 thf(80,axiom,((bot_bot_b_o = (^ [A:b]: (member_b @ A @ bot_bot_set_b)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_bot__empty__eq)).
% 16.10/5.55 thf(391,plain,(((bot_bot_b_o) = (^ [A:b]: (member_b @ A @ bot_bot_set_b)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 16.10/5.55 thf(76,axiom,((! [A:b]: (member_b @ A @ top_top_set_b))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_UNIV__I)).
% 16.10/5.55 thf(382,plain,((! [A:b]: (member_b @ A @ top_top_set_b))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 16.10/5.55 thf(55,axiom,((! [A:b,B:set_b,C:b]: ((member_b @ A @ B) => (member_b @ A @ (insert_b @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_insertI2)).
% 16.10/5.55 thf(313,plain,((! [A:b,B:set_b,C:b]: ((member_b @ A @ B) => (member_b @ A @ (insert_b @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 16.10/5.55 thf(35,axiom,((! [A:(b > b),B:set_b,C:(b > $o)]: ((collect_b @ (^ [D:b]: ((member_b @ D @ (image_b_b @ A @ B)) & (C @ D)))) = (image_b_b @ A @ (collect_b @ (^ [D:b]: ((member_b @ D @ B) & (C @ (A @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_Compr__image__eq)).
% 16.10/5.55 thf(236,plain,((! [A:(b > b),B:set_b,C:(b > $o)]: ((collect_b @ (^ [D:b]: ((member_b @ D @ (image_b_b @ A @ B)) & (C @ D)))) = (image_b_b @ (A) @ (collect_b @ (^ [D:b]: ((member_b @ D @ B) & (C @ (A @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 16.10/5.55 thf(65,axiom,((! [A:set_b]: ((? [B:b]: (member_b @ B @ A)) = (A != bot_bot_set_b)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_ex__in__conv)).
% 16.10/5.55 thf(350,plain,((! [A:set_b]: ((? [B:b]: (member_b @ B @ A)) = (~ (A = bot_bot_set_b))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 16.10/5.55 thf(74,axiom,((! [A:set_b]: (inj_on_b_set_b @ (^ [B:b]: (insert_b @ B @ bot_bot_set_b)) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_inj__singleton)).
% 16.10/5.55 thf(377,plain,((! [A:set_b]: (inj_on_b_set_b @ (^ [B:b]: (insert_b @ B @ bot_bot_set_b)) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 16.10/5.55 thf(33,axiom,((! [A:(b > b),B:b,C:set_b]: ((inj_on_b_b @ A @ (insert_b @ B @ C)) = ((inj_on_b_b @ A @ C) & ~ (member_b @ (A @ B) @ (image_b_b @ A @ (minus_minus_set_b @ C @ (insert_b @ B @ bot_bot_set_b)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_inj__on__insert)).
% 16.10/5.55 thf(230,plain,((! [A:(b > b),B:b,C:set_b]: ((inj_on_b_b @ (A) @ (insert_b @ B @ C)) = ((inj_on_b_b @ (A) @ C) & ~ (member_b @ (A @ B) @ (image_b_b @ (A) @ (minus_minus_set_b @ C @ (insert_b @ B @ bot_bot_set_b)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 16.10/5.55 thf(38,axiom,((! [A:b,B:(b > b),C:b,D:set_b]: ((A = (B @ C)) => ((member_b @ C @ D) => (member_b @ A @ (image_b_b @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_image__eqI)).
% 16.10/5.55 thf(245,plain,((! [A:b,B:(b > b),C:b,D:set_b]: ((A = (B @ C)) => ((member_b @ C @ D) => (member_b @ A @ (image_b_b @ (B) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 16.10/5.55 thf(92,axiom,((! [A:b]: ((hilbert_Eps_b @ ((=) @ b @ A)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_some__sym__eq__trivial)).
% 16.10/5.55 thf(434,plain,((! [A:b]: ((hilbert_Eps_b @ ((=) @ b @ A)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 16.10/5.55 thf(52,axiom,((! [A:b,B:b,C:set_b]: ((member_b @ A @ (insert_b @ B @ C)) = ((A = B) | (member_b @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_insert__iff)).
% 16.10/5.55 thf(303,plain,((! [A:b,B:b,C:set_b]: ((member_b @ A @ (insert_b @ B @ C)) = ((A = B) | (member_b @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 16.10/5.55 thf(71,axiom,((top_top_b_o = (^ [A:b]: (member_b @ A @ top_top_set_b)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_top__empty__eq)).
% 16.10/5.55 thf(367,plain,(((top_top_b_o) = (^ [A:b]: (member_b @ A @ top_top_set_b)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 16.10/5.55 thf(8,axiom,((! [A:set_b]: ((minus_minus_set_b @ bot_bot_set_b @ A) = bot_bot_set_b))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_empty__Diff)).
% 16.10/5.55 thf(140,plain,((! [A:set_b]: ((minus_minus_set_b @ bot_bot_set_b @ A) = bot_bot_set_b))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 16.10/5.55 thf(24,axiom,((! [A:set_b]: ((minus_minus_set_b @ A @ top_top_set_b) = bot_bot_set_b))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_Diff__UNIV)).
% 16.10/5.55 thf(198,plain,((! [A:set_b]: ((minus_minus_set_b @ A @ top_top_set_b) = bot_bot_set_b))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 16.10/5.55 thf(53,axiom,((! [A:(b > b),B:set_b]: ((bot_bot_set_b = (image_b_b @ A @ B)) = (B = bot_bot_set_b)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_empty__is__image)).
% 16.10/5.55 thf(306,plain,((! [A:(b > b),B:set_b]: ((bot_bot_set_b = (image_b_b @ (A) @ B)) = (B = bot_bot_set_b)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 16.10/5.55 thf(6,axiom,((! [A:(b > $o)]: ((bot_bot_set_b = (collect_b @ A)) = (! [B:b]: ~ (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_empty__Collect__eq)).
% 16.10/5.55 thf(135,plain,((! [A:(b > $o)]: ((bot_bot_set_b = (collect_b @ (A))) = (! [B:b]: ~ (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 16.10/5.55 thf(51,axiom,((! [A:b,B:set_b,C:set_b]: ((~ (member_b @ A @ B)) => ((~ (member_b @ A @ C)) => (((insert_b @ A @ B) = (insert_b @ A @ C)) = (B = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_insert__ident)).
% 16.10/5.55 thf(299,plain,((! [A:b,B:set_b,C:set_b]: ((~ (member_b @ A @ B)) => ((~ (member_b @ A @ C)) => (((insert_b @ A @ B) = (insert_b @ A @ C)) = (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 16.10/5.55 thf(106,axiom,((! [A:(b > $o),B:(b > $o)]: ((? [C:b]: (A @ C)) => ((! [C:b]: ((A @ C) => (B @ C))) => (B @ (hilbert_Eps_b @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_someI2__ex)).
% 16.10/5.55 thf(505,plain,((! [A:(b > $o),B:(b > $o)]: ((? [C:b]: (A @ C)) => ((! [C:b]: ((A @ C) => (B @ C))) => (B @ (hilbert_Eps_b @ (A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 16.10/5.55 thf(91,axiom,((! [A:(b > $o),B:(b > $o)]: ((! [C:b]: ((A @ C) = (B @ C))) => ((hilbert_Eps_b @ A) = (hilbert_Eps_b @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_Eps__cong)).
% 16.10/5.55 thf(431,plain,((! [A:(b > $o),B:(b > $o)]: ((! [C:b]: ((A @ C) = (B @ C))) => ((hilbert_Eps_b @ (A)) = (hilbert_Eps_b @ (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 16.10/5.55 thf(99,axiom,((! [A:set_b]: ((member_b @ (hilbert_Eps_b @ (^ [B:b]: (member_b @ B @ A))) @ A) = (A != bot_bot_set_b)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_some__in__eq)).
% 16.10/5.55 thf(473,plain,((! [A:set_b]: ((member_b @ (hilbert_Eps_b @ (^ [B:b]: (member_b @ B @ A))) @ A) = (~ (A = bot_bot_set_b))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 16.10/5.55 thf(102,axiom,((! [A:(b > $o)]: ((? [B:b]: (A @ B)) => (A @ (hilbert_Eps_b @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_someI__ex)).
% 16.10/5.55 thf(490,plain,((! [A:(b > $o)]: ((? [B:b]: (A @ B)) => (A @ (hilbert_Eps_b @ (A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 16.10/5.55 thf(15,axiom,((! [A:(b > $o)]: (((collect_b @ A) = bot_bot_set_b) = (! [B:b]: ~ (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_Collect__empty__eq)).
% 16.10/5.55 thf(162,plain,((! [A:(b > $o)]: (((collect_b @ (A)) = bot_bot_set_b) = (! [B:b]: ~ (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 16.10/5.55 thf(27,axiom,((minus_minus_set_b = (^ [A:set_b,B:set_b]: (collect_b @ (^ [C:b]: ((member_b @ C @ A) & ~ (member_b @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_set__diff__eq)).
% 16.10/5.55 thf(209,plain,(((minus_minus_set_b) = (^ [A:set_b,B:set_b]: (collect_b @ (^ [C:b]: ((member_b @ C @ A) & ~ (member_b @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 16.10/5.55 thf(67,axiom,((! [A:b]: (member_b @ A @ top_top_set_b))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_iso__tuple__UNIV__I)).
% 16.10/5.55 thf(355,plain,((! [A:b]: (member_b @ A @ top_top_set_b))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 16.10/5.55 thf(59,axiom,((is_singleton_b = (^ [A:set_b]: ? [B:b]: (A = (insert_b @ B @ bot_bot_set_b))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_is__singleton__def)).
% 16.10/5.55 thf(331,plain,(((is_singleton_b) = (^ [A:set_b]: ? [B:b]: (A = (insert_b @ B @ bot_bot_set_b))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 16.10/5.55 thf(94,axiom,((! [A:b]: ((hilbert_Eps_b @ (^ [B:b]: (B = A))) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_some__eq__trivial)).
% 16.10/5.55 thf(441,plain,((! [A:b]: ((hilbert_Eps_b @ (^ [B:b]: (B = A))) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 16.10/5.55 thf(112,axiom,((! [A:(b > $o)]: ((A @ (hilbert_Eps_b @ A)) = (? [B:b]: (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_some__eq__ex)).
% 16.10/5.55 thf(544,plain,((! [A:(b > $o)]: ((A @ (hilbert_Eps_b @ (A))) = (? [B:b]: (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 16.10/5.55 thf(12,axiom,((! [A:set_b,B:b,C:set_b]: ((minus_minus_set_b @ A @ (insert_b @ B @ C)) = (minus_minus_set_b @ (minus_minus_set_b @ A @ C) @ (insert_b @ B @ bot_bot_set_b))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_Diff__insert)).
% 16.10/5.55 thf(154,plain,((! [A:set_b,B:b,C:set_b]: ((minus_minus_set_b @ A @ (insert_b @ B @ C)) = (minus_minus_set_b @ (minus_minus_set_b @ A @ C) @ (insert_b @ B @ bot_bot_set_b))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 16.10/5.55 thf(19,axiom,((! [A:b,B:set_b,C:set_b]: (((member_b @ A @ B) => ((minus_minus_set_b @ (insert_b @ A @ C) @ B) = (minus_minus_set_b @ C @ B))) & ((~ (member_b @ A @ B)) => ((minus_minus_set_b @ (insert_b @ A @ C) @ B) = (insert_b @ A @ (minus_minus_set_b @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_108_insert__Diff__if)).
% 16.10/5.55 thf(175,plain,((! [A:b,B:set_b,C:set_b]: (((member_b @ A @ B) => ((minus_minus_set_b @ (insert_b @ A @ C) @ B) = (minus_minus_set_b @ C @ B))) & ((~ (member_b @ A @ B)) => ((minus_minus_set_b @ (insert_b @ A @ C) @ B) = (insert_b @ A @ (minus_minus_set_b @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 16.10/5.55 thf(78,axiom,((! [A:set_b]: ((! [B:b]: ~ (member_b @ B @ A)) = (A = bot_bot_set_b)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_all__not__in__conv)).
% 16.10/5.55 thf(386,plain,((! [A:set_b]: ((! [B:b]: ~ (member_b @ B @ A)) = (A = bot_bot_set_b)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 16.10/5.55 thf(9,axiom,((! [A:(b > b)]: ((image_b_b @ A @ bot_bot_set_b) = bot_bot_set_b))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_image__empty)).
% 16.10/5.55 thf(143,plain,((! [A:(b > b)]: ((image_b_b @ (A) @ bot_bot_set_b) = bot_bot_set_b))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 16.10/5.55 thf(104,axiom,((! [A:(b > $o),B:b]: ((A @ B) => (A @ (hilbert_Eps_b @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_someI)).
% 16.10/5.55 thf(497,plain,((! [A:(b > $o),B:b]: ((A @ B) => (A @ (hilbert_Eps_b @ (A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 16.10/5.55 thf(30,axiom,((! [A:b,B:set_b]: ((insert_b @ A @ B) != bot_bot_set_b))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_insert__not__empty)).
% 16.10/5.55 thf(218,plain,((! [A:b,B:set_b]: ~ ((insert_b @ A @ B) = bot_bot_set_b))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 16.10/5.55 thf(39,axiom,((! [A:set_b]: ((collect_b @ (^ [B:b]: (member_b @ B @ A))) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_Collect__mem__eq)).
% 16.10/5.55 thf(250,plain,((! [A:set_b]: ((collect_b @ (^ [B:b]: (member_b @ B @ A))) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 16.10/5.55 thf(98,axiom,((! [A:(b > $o),B:b]: ((? [C:b]: (A @ C)) => ((B = (hilbert_Eps_b @ A)) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_exE__some)).
% 16.10/5.55 thf(465,plain,((! [A:(b > $o),B:b]: ((? [C:b]: (A @ C)) => ((B = (hilbert_Eps_b @ (A))) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 16.10/5.55 thf(41,axiom,((! [A:b,B:set_b]: (member_b @ A @ (insert_b @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_insertI1)).
% 16.10/5.55 thf(258,plain,((! [A:b,B:set_b]: (member_b @ A @ (insert_b @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 16.10/5.55 thf(21,axiom,((! [A:b,B:b,C:set_b]: ((member_b @ A @ (insert_b @ B @ C)) => ((A != B) => (member_b @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_60_insertE)).
% 16.10/5.55 thf(186,plain,((! [A:b,B:b,C:set_b]: ((member_b @ A @ (insert_b @ B @ C)) => ((~ (A = B)) => (member_b @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 16.10/5.55 thf(1,conjecture,((! [A:a]: (~ (p @ A) | (q @ A @ (hilbert_Eps_b @ (q @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1)).
% 16.10/5.55 thf(2,negated_conjecture,((~ (! [A:a]: (~ (p @ A) | (q @ A @ (hilbert_Eps_b @ (q @ A))))))),inference(neg_conjecture,[status(cth)],[1])).
% 16.10/5.55 thf(114,plain,((~ (! [A:a]: (~ (p @ A) | (q @ A @ (hilbert_Eps_b @ (q @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 16.10/5.55 thf(18,axiom,((! [A:b,B:set_b,C:set_b]: ((member_b @ A @ B) => ((minus_minus_set_b @ (insert_b @ A @ C) @ B) = (minus_minus_set_b @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_insert__Diff1)).
% 16.10/5.55 thf(171,plain,((! [A:b,B:set_b,C:set_b]: ((member_b @ A @ B) => ((minus_minus_set_b @ (insert_b @ A @ C) @ B) = (minus_minus_set_b @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 16.10/5.55 thf(85,axiom,((! [A:set_b]: ((! [B:b]: (member_b @ B @ A)) => (top_top_set_b = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_42_UNIV__eq__I)).
% 16.10/5.55 thf(410,plain,((! [A:set_b]: ((! [B:b]: (member_b @ B @ A)) => (top_top_set_b = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 16.10/5.55 thf(10,axiom,((! [A:b,B:set_b]: ((member_b @ A @ B) => ((insert_b @ A @ B) = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_insert__absorb)).
% 16.10/5.55 thf(146,plain,((! [A:b,B:set_b]: ((member_b @ A @ B) => ((insert_b @ A @ B) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 16.10/5.55 thf(83,axiom,((? [A:b]: (member_b @ A @ top_top_set_b))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_43_UNIV__witness)).
% 16.10/5.55 thf(405,plain,((? [A:b]: (member_b @ A @ top_top_set_b))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 16.10/5.55 thf(20,axiom,((! [A:b,B:set_b]: ((insert_b @ A @ (minus_minus_set_b @ B @ (insert_b @ A @ bot_bot_set_b))) = (insert_b @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_insert__Diff__single)).
% 16.10/5.55 thf(183,plain,((! [A:b,B:set_b]: ((insert_b @ A @ (minus_minus_set_b @ B @ (insert_b @ A @ bot_bot_set_b))) = (insert_b @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 16.10/5.55 thf(88,axiom,((bot_bot_set_b != top_top_set_b)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_empty__not__UNIV)).
% 16.10/5.55 thf(422,plain,((~ (bot_bot_set_b = top_top_set_b))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 16.10/5.55 thf(17,axiom,((! [A:(b > $o)]: (((collect_b @ A) = bot_bot_set_b) = (A = bot_bot_b_o)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_Collect__empty__eq__bot)).
% 16.10/5.55 thf(168,plain,((! [A:(b > $o)]: (((collect_b @ (A)) = bot_bot_set_b) = ((A) = (bot_bot_b_o))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 16.10/5.55 thf(43,axiom,((! [A:b]: ((collect_b @ (^ [B:b]: (B = A))) = (insert_b @ A @ bot_bot_set_b)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_singleton__conv)).
% 16.10/5.55 thf(262,plain,((! [A:b]: ((collect_b @ (^ [B:b]: (B = A))) = (insert_b @ A @ bot_bot_set_b)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 16.10/5.55 thf(36,axiom,((! [A:(b > b),B:b,C:set_b]: ((inj_on_b_b @ A @ top_top_set_b) => ((member_b @ (A @ B) @ (image_b_b @ A @ C)) = (member_b @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_inj__image__mem__iff)).
% 16.10/5.55 thf(239,plain,((! [A:(b > b),B:b,C:set_b]: ((inj_on_b_b @ (A) @ top_top_set_b) => ((member_b @ (A @ B) @ (image_b_b @ (A) @ C)) = (member_b @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 16.10/5.55 thf(45,axiom,((! [A:(b > $o),B:b]: (((A @ B) => ((collect_b @ (^ [C:b]: ((C = B) & (A @ C)))) = (insert_b @ B @ bot_bot_set_b))) & ((~ (A @ B)) => ((collect_b @ (^ [C:b]: ((C = B) & (A @ C)))) = bot_bot_set_b))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_Collect__conv__if)).
% 16.10/5.55 thf(268,plain,((! [A:(b > $o),B:b]: (((A @ B) => ((collect_b @ (^ [C:b]: ((C = B) & (A @ C)))) = (insert_b @ B @ bot_bot_set_b))) & ((~ (A @ B)) => ((collect_b @ (^ [C:b]: ((C = B) & (A @ C)))) = bot_bot_set_b))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 16.10/5.55 thf(93,axiom,((! [A:b,B:(b > $o)]: ((A = (hilbert_Eps_b @ B)) => ((? [C:b]: (B @ C)) = (B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_verit__sko__ex__indirect)).
% 16.10/5.55 thf(437,plain,((! [A:b,B:(b > $o)]: ((A = (hilbert_Eps_b @ (B))) => ((? [C:b]: (B @ C)) = (B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 16.10/5.55 thf(87,axiom,((! [A:set_set_b,B:b,C:set_b]: ((! [D:set_b]: ((member_set_b @ D @ A) => (~ (member_b @ B @ D)))) => ((member_set_b @ C @ (image_set_b_set_b @ (insert_b @ B) @ A)) = ((member_b @ B @ C) & (member_set_b @ (minus_minus_set_b @ C @ (insert_b @ B @ bot_bot_set_b)) @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_in__image__insert__iff)).
% 16.10/5.55 thf(415,plain,((! [A:set_set_b,B:b,C:set_b]: ((! [D:set_b]: ((member_set_b @ D @ A) => (~ (member_b @ B @ D)))) => ((member_set_b @ C @ (image_set_b_set_b @ (insert_b @ B) @ A)) = ((member_b @ B @ C) & (member_set_b @ (minus_minus_set_b @ C @ (insert_b @ B @ bot_bot_set_b)) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 16.10/5.55 thf(90,axiom,((! [A:b,B:(b > $o)]: ((A = (hilbert_Eps_b @ (^ [C:b]: ~ (B @ C)))) => ((! [C:b]: (B @ C)) = (B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_verit__sko__forall__indirect)).
% 16.10/5.55 thf(427,plain,((! [A:b,B:(b > $o)]: ((A = (hilbert_Eps_b @ (^ [C:b]: ~ (B @ C)))) => ((! [C:b]: (B @ C)) = (B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 16.10/5.55 thf(72,axiom,((! [A:b]: ~ (member_b @ A @ bot_bot_set_b))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_emptyE)).
% 16.10/5.55 thf(369,plain,((! [A:b]: ~ (member_b @ A @ bot_bot_set_b))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 16.10/5.55 thf(61,axiom,((! [A:(b > b),B:set_b]: (((image_b_b @ A @ B) = bot_bot_set_b) = (B = bot_bot_set_b)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_image__is__empty)).
% 16.10/5.55 thf(337,plain,((! [A:(b > b),B:set_b]: (((image_b_b @ (A) @ B) = bot_bot_set_b) = (B = bot_bot_set_b)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 16.10/5.55 thf(54,axiom,((! [A:set_b]: ((is_singleton_b @ A) => (~ (! [B:b]: (A != (insert_b @ B @ bot_bot_set_b))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_is__singletonE)).
% 16.10/5.55 thf(309,plain,((! [A:set_b]: ((is_singleton_b @ A) => (~ (! [B:b]: ~ (A = (insert_b @ B @ bot_bot_set_b))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 16.10/5.55 thf(29,axiom,((! [A:b,B:(b > $o)]: ((member_b @ A @ (collect_b @ B)) = (B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_mem__Collect__eq)).
% 16.10/5.55 thf(215,plain,((! [A:b,B:(b > $o)]: ((member_b @ A @ (collect_b @ (B))) = (B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 16.10/5.55 thf(31,axiom,((! [A:b]: ((collect_b @ ((=) @ b @ A)) = (insert_b @ A @ bot_bot_set_b)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_singleton__conv2)).
% 16.10/5.55 thf(222,plain,((! [A:b]: ((collect_b @ ((=) @ b @ A)) = (insert_b @ A @ bot_bot_set_b)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 16.10/5.55 thf(97,axiom,((! [A:set_b,B:(b > $o),C:(b > $o)]: ((? [D:b]: ((member_b @ D @ A) & (B @ D))) => ((! [D:b]: (((member_b @ D @ A) & (B @ D)) => (C @ D))) => (C @ (hilbert_Eps_b @ (^ [D:b]: ((member_b @ D @ A) & (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_someI2__bex)).
% 16.10/5.55 thf(454,plain,((! [A:set_b,B:(b > $o),C:(b > $o)]: ((? [D:b]: ((member_b @ D @ A) & (B @ D))) => ((! [D:b]: (((member_b @ D @ A) & (B @ D)) => (C @ D))) => (C @ (hilbert_Eps_b @ (^ [D:b]: ((member_b @ D @ A) & (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 16.10/5.55 thf(70,axiom,((! [A:b,B:b]: ((member_b @ A @ (insert_b @ B @ bot_bot_set_b)) => (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_singletonD)).
% 16.10/5.55 thf(364,plain,((! [A:b,B:b]: ((member_b @ A @ (insert_b @ B @ bot_bot_set_b)) => (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 16.10/5.55 thf(578,plain,(($false)),inference(e,[status(thm)],[519,541,138,347,333,481,276,379,384,533,500,340,389,372,344,357,157,189,284,325,316,492,121,353,211,253,293,132,243,265,529,201,233,452,260,160,165,192,407,361,329,225,476,547,393,515,425,296,444,149,402,286,118,204,413,391,382,313,236,350,377,230,245,434,303,367,140,198,306,135,299,505,431,473,490,162,209,355,331,441,544,154,175,386,143,497,218,250,465,258,186,114,171,410,146,405,183,422,168,262,239,268,437,415,427,369,337,309,215,222,454,364])).
% 16.10/5.55 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.10/5.55 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------