%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP205^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n026.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:07:10 AM UTC 2026
% Result : Theorem 39.14s 9.92s
% Output : Refutation 39.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP205^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.10/0.19 % Computer : n026.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Tue Sep 29 20:14:12 UTC 2026
% 0.10/0.19 % CPUTime :
% 0.10/0.19 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 1.07/0.80 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 2.43/1.24 % [INFO] Parsing done (438ms).
% 2.43/1.26 % [INFO] Running in sequential loop mode.
% 3.67/1.65 % [INFO] eprover registered as external prover.
% 3.67/1.66 % [INFO] Scanning for conjecture ...
% 4.11/1.81 % [INFO] Found a conjecture (or negated_conjecture) and 354 axioms. Running axiom selection ...
% 4.36/1.96 % [INFO] Axiom selection finished. Selected 254 axioms (removed 100 axioms).
% 5.02/2.19 % [INFO] Problem is higher-order (TPTP THF).
% 5.25/2.21 % [INFO] Type checking passed.
% 5.25/2.22 % [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 ...
% 39.14/9.91 % External prover 'e' found a proof!
% 39.14/9.92 % [INFO] Killing All external provers ...
% 39.14/9.92 % Time passed: 9576ms (effective reasoning time: 8653ms)
% 39.14/9.92 % 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)>
% 39.14/9.92 % Axioms used in derivation (254): fact_224_ord__eq__le__trans, fact_98_subset__eq, fact_158_bex__Un, fact_167_sup_Ocobounded2, fact_206_BVG__choice, fact_214_order__subst1, fact_255_prod__cases, fact_322_pred__subset__eq, fact_232_fst__swap, fact_11_Un__subset__iff, fact_157_ball__Un, fact_353_Choiceo_Oelims, fact_309_subset__CollectI, fact_251_old_Oprod_Oexhaust, fact_263_snd__eqD, fact_28_UnCI, fact_315_subrelI, fact_350_Composeo_Osimps_I3_J, fact_231_dual__order_Oantisym, fact_352_Composeo_Oelims, fact_108_sup__left__commute, fact_175_sup_Oabsorb1, fact_211_game_Odistinct_I45_J, fact_32_sup__apply, fact_247_prod_Ocollapse, fact_186_sup__ge1, fact_23_sup_Obounded__iff, fact_86_subset__refl, fact_301_sndOp__def, fact_216_ord__eq__le__subst, fact_201_prod__eq__iff, fact_217_ord__le__eq__subst, fact_35_sup_Oidem, fact_154_Un__commute, fact_215_order__subst2, fact_25_game_Oinject_I5_J, fact_280_exI__realizer, fact_119_sup_Oleft__commute, fact_210_game_Odistinct_I39_J, fact_254_prod__cases, fact_274_surjective__pairing, fact_219_antisym, fact_197_Un__least, fact_101_equalityE, fact_336_split__option__all, fact_31_union__or, fact_332_option_Ocollapse, fact_153_Un__left__absorb, fact_230_dual__order_Oeq__iff, fact_299_relChain__def, fact_205_usubstappp__loop__conv, fact_7_Compose_OIH_I2_J, fact_311_usubstappp_Osimps_I5_J, fact_335_combine__options__cases, fact_204_prod__eqI, fact_233_fst__swap, fact_287_Composeo_Osimps_I2_J, fact_176_sup__unique, fact_276_prod_Oexhaust__sel, fact_137_sup__assoc, fact_344_undefg__equiv, fact_75_set__eq__subset, fact_126_sup_Ocommute, fact_218_eq__iff, fact_46_sup__idem, fact_268_prod_Oswap__def, fact_305_Collect__subset, fact_283_usubstappp__compose, fact_286_Composeo__undef, fact_152_Un__left__commute, fact_300_sndOp__def, fact_107_in__mono, fact_190_inf__sup__ord_I4_J, fact_317_pred__equals__eq2, fact_338_option_Oinducts, fact_83_Collect__mono, fact_58_sup_Oright__idem, fact_185_sup__ge2, fact_195_Un__upper2, fact_342_option_Osel, fact_181_sup__mono, fact_193_Un__absorb2, fact_207_usubstappp__choice__conv, fact_102_subsetD, fact_74_Collect__mono__iff, fact_222_antisym__conv, fact_52_subsetI, fact_65_sup_Oleft__idem, fact_270_fst__pair, fact_226_order__class_Oorder_Oantisym, fact_170_sup_OboundedI, fact_0__092_060open_062U_A_092_060union_062_ABVG_A_Ithe_A_Isnd_A_Iusubstappp_A_092_060sigma_062_AU_A_092_060alpha_062_J_J_J_A_092_060union_062_ABVG_A_Ithe_A_Isnd_A_Iusubstappp_A_092_060sigma_062_A_Ifst_A_Iusubstappp_A_092_060sigma_062_AU_A_092_060alpha_062_J_J_A_092_060beta_062_J_J_J_A_092_060subseteq_062_Afst_A_Iusubstappp_A_092_060sigma_062_A_Ifst_A_Iusubstappp_A_092_060sigma_062_AU_A_092_060alpha_062_J_J_A_092_060beta_062_J_092_060close_062, fact_266_prod_Oswap__def, fact_306_Un__def, fact_178_sup_OorderE, fact_349_Composeo_Osimps_I1_J, fact_341_option_Odistinct_I1_J, fact_188_le__supE, fact_208_game_Oinject_I6_J, fact_174_sup_Oabsorb2, fact_292_sndI, fact_235_snd__swap, fact_64_sup__left__idem, fact_40_sup_Oidem, fact_307_sup__set__def, fact_329_option_Oinject, fact_132_sup__assoc, fact_172_sup__absorb2, fact_53_sup_Oright__idem, fact_334_option_Oexhaust__sel, fact_302_fstOp__def, fact_313_sup__Un__eq, fact_184_le__supI1, fact_77_set__eq__subset, fact_164_sup_OcoboundedI1, fact_120_sup__commute, fact_346_Loopo_Ocases, fact_80_subset__trans, fact_84_subset__refl, fact_182_sup_Omono, fact_257_surj__pair, fact_245_swap__simp, fact_312_usubstappp_Osimps_I6_J, fact_220_eq__refl, fact_59_sup__left__idem, fact_160_UnI1, fact_209_game_Oinject_I4_J, fact_150_inf__sup__aci_I8_J, fact_78_subset__trans, fact_331_not__None__eq, fact_179_le__iff__sup, fact_212_game_Odistinct_I37_J, fact_243_swap__simp, fact_49_subset__antisym, fact_41_sup__idem, fact_294_Loopo__undef, fact_347_Loopo_Osimps_I1_J, fact_259_fst__eqD, fact_242_prod_Oinject, fact_50_subsetI, fact_343_Composeo_Oinduct, fact_24_BVG__compose, fact_189_inf__sup__ord_I3_J, fact_89_subset__iff, fact_199_order__refl, fact_169_sup_Oorder__iff, fact_202_prod_Oexpand, fact_168_sup_Ocobounded1, fact_161_UnE, fact_198_Un__mono, fact_310_subset__Collect__iff, fact_173_sup__absorb1, fact_177_sup_OorderI, fact_5_usubst__taboos__mon, fact_95_equalityD1, fact_252_Pair__inject, fact_93_equalityD1, fact_165_sup_Oabsorb__iff2, fact_104_subsetD, fact_146_boolean__algebra__cancel_Osup1, fact_239_old_Oprod_Oinject, fact_148_inf__sup__aci_I6_J, fact_192_subset__UnE, fact_241_prod_Oinject, fact_339_option_Oexhaust, fact_278_conjI__realizer, fact_308_Collect__disj__eq, fact_319_pred__subset__eq2, fact_163_sup_OcoboundedI2, fact_17_le__sup__iff, fact_244_swap__simp, fact_324_prop__restrict, fact_114_sup_Oleft__commute, fact_92_equalityD2, fact_138_sup_Oassoc, fact_203_exE__realizer_H, fact_250_old_Oprod_Oexhaust, fact_96_subset__eq, fact_288_usubstappp__loop, fact_6_usubstappp__fst__mon, fact_293_Loopo_Osimps_I2_J, fact_229_dual__order_Otrans, fact_125_sup__commute, fact_240_old_Oprod_Oinject, fact_99_equalityE, fact_3_IHb, fact_249_old_Oprod_Oinducts, fact_337_split__option__ex, fact_71_usubstappp__det, fact_228_dual__order_Orefl, fact_304_less__eq__set__def, fact_213_BVG__loop, fact_87_subset__iff, fact_340_option_OdiscI, fact_272_snd__pair, fact_323_conj__subset__def, fact_149_inf__sup__aci_I7_J, fact_348_Choiceo_Osimps_I1_J, fact_156_Un__assoc, fact_221_order_Otrans, fact_191_subset__Un__eq, fact_166_sup_Oabsorb__iff1, fact_187_le__supI, fact_285_BNF__Greatest__Fixpoint_Osubst__Pair, fact_196_Un__upper1, fact_105_in__mono, fact_237_GreatestI2__order, fact_256_surj__pair, fact_180_sup__least, fact_145_boolean__algebra__cancel_Osup2, fact_183_le__supI2, fact_326_ssubst__Pair__rhs, fact_236_usubstappp__choice, fact_265_snd__conv, fact_2_IHa, fact_70_sup_Oleft__idem, fact_4_Compose_Oprems, fact_1_fact, fact_225_ord__le__eq__trans, fact_147_inf__sup__aci_I5_J, fact_159_UnI2, fact_200_option_Oexpand, fact_8_Compose_OIH_I1_J, fact_194_Un__absorb1, fact_248_old_Oprod_Oinducts, fact_47_subset__antisym, fact_303_usubstappp_Osimps_I4_J, fact_238_Greatest__equality, fact_143_sup_Oassoc, fact_351_Choiceo_Osimps_I3_J, fact_131_sup_Ocommute, fact_333_Composeo_Ocases, fact_261_fst__conv, fact_171_sup_OboundedE, fact_345_Loopo_Oinduct, fact_155_Un__absorb, fact_298_eq__fst__iff, fact_223_order__class_Oorder_Oeq__iff, fact_12_le__sup__iff, fact_281_Choiceo_Osimps_I2_J, fact_330_not__Some__eq, fact_227_order__trans, fact_18_sup_Obounded__iff, fact_151_not__union__or, fact_162_usubstappp__antimon, fact_296_fstI, fact_113_sup__left__commute, fact_290_eq__snd__iff, fact_90_equalityD2, fact_234_snd__swap, fact_282_Choiceo__undef, fact_328_Loopo_Oelims, fact_253_Pair__inject, fact_327_Collect__restrict
% 39.14/9.92 % No. of inferences in proof: 512
% 39.14/9.92 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 9576 ms resp. 8653 ms w/o parsing
% 39.89/10.12 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 39.89/10.12 thf(produc1418842292n_game_type, type, produc1418842292n_game: $tType).
% 39.89/10.12 thf(set_Pr1625152599n_game_type, type, set_Pr1625152599n_game: $tType).
% 39.89/10.12 thf(set_Pr166476775n_game_type, type, set_Pr166476775n_game: $tType).
% 39.89/10.12 thf(produc1016592119n_game_type, type, produc1016592119n_game: $tType).
% 39.89/10.12 thf(produc1078154247n_game_type, type, produc1078154247n_game: $tType).
% 39.89/10.12 thf(produc735959047riable_type, type, produc735959047riable: $tType).
% 39.89/10.12 thf(option_game_type, type, option_game: $tType).
% 39.89/10.12 thf(set_variable_type, type, set_variable: $tType).
% 39.89/10.12 thf(variable_type, type, variable: $tType).
% 39.89/10.12 thf(game_type, type, game: $tType).
% 39.89/10.12 thf(bNF_Ca1986151756riable_decl, type, bNF_Ca1986151756riable: (set_Pr1625152599n_game > ((option_game > set_variable) > $o))).
% 39.89/10.12 thf(bNF_fs984229733n_game_decl, type, bNF_fs984229733n_game: ((set_variable > (option_game > $o)) > ((option_game > (option_game > $o)) > (produc1078154247n_game > produc1078154247n_game)))).
% 39.89/10.12 thf(bNF_pi856525207n_game_decl, type, bNF_pi856525207n_game: ((set_variable > (option_game > $o)) > ((option_game > (option_game > $o)) > (set_variable > (option_game > option_game))))).
% 39.89/10.12 thf(bNF_pi1813424679n_game_decl, type, bNF_pi1813424679n_game: ((set_variable > (set_variable > $o)) > ((set_variable > (option_game > $o)) > (set_variable > (option_game > set_variable))))).
% 39.89/10.12 thf(bNF_sn1374695591n_game_decl, type, bNF_sn1374695591n_game: ((set_variable > (option_game > $o)) > ((option_game > (option_game > $o)) > (produc1078154247n_game > produc1016592119n_game)))).
% 39.89/10.12 thf(bNF_sn582998327n_game_decl, type, bNF_sn582998327n_game: ((set_variable > (set_variable > $o)) > ((set_variable > (option_game > $o)) > (produc1078154247n_game > produc1078154247n_game)))).
% 39.89/10.12 thf(sup_sup_variable_o_decl, type, sup_sup_variable_o: ((variable > $o) > ((variable > $o) > (variable > $o)))).
% 39.89/10.12 thf(sup_sup_o_decl, type, sup_sup_o: ($o > ($o > $o))).
% 39.89/10.12 thf(sup_sup_set_variable_decl, type, sup_sup_set_variable: (set_variable > (set_variable > set_variable))).
% 39.89/10.12 thf(none_game_decl, type, none_game: option_game).
% 39.89/10.12 thf(some_game_decl, type, some_game: (game > option_game)).
% 39.89/10.12 thf(the_game_decl, type, the_game: (option_game > game)).
% 39.89/10.12 thf(ord_le707292176game_o_decl, type, ord_le707292176game_o: ((option_game > (option_game > $o)) > ((option_game > (option_game > $o)) > $o))).
% 39.89/10.12 thf(ord_le1407353162able_o_decl, type, ord_le1407353162able_o: ((variable > $o) > ((variable > $o) > $o))).
% 39.89/10.12 thf(ord_le1780499447n_game_decl, type, ord_le1780499447n_game: (set_Pr1625152599n_game > (set_Pr1625152599n_game > $o))).
% 39.89/10.12 thf(ord_le282106107riable_decl, type, ord_le282106107riable: (set_variable > (set_variable > $o))).
% 39.89/10.12 thf(order_272405634riable_decl, type, order_272405634riable: ((set_variable > $o) > set_variable)).
% 39.89/10.12 thf(produc1111617711n_game_decl, type, produc1111617711n_game: (option_game > (option_game > produc1016592119n_game))).
% 39.89/10.12 thf(produc1140431679riable_decl, type, produc1140431679riable: (option_game > (set_variable > produc735959047riable))).
% 39.89/10.12 thf(produc1149443391n_game_decl, type, produc1149443391n_game: (set_variable > (option_game > produc1078154247n_game))).
% 39.89/10.12 thf(produc884810027riable_decl, type, produc884810027riable: (produc735959047riable > option_game)).
% 39.89/10.12 thf(produc893821739n_game_decl, type, produc893821739n_game: (produc1078154247n_game > set_variable)).
% 39.89/10.12 thf(produc284475501riable_decl, type, produc284475501riable: (produc735959047riable > set_variable)).
% 39.89/10.12 thf(produc293487213n_game_decl, type, produc293487213n_game: (produc1078154247n_game > option_game)).
% 39.89/10.12 thf(produc1696194127n_game_decl, type, produc1696194127n_game: (produc1016592119n_game > produc1016592119n_game)).
% 39.89/10.12 thf(produc345397471riable_decl, type, produc345397471riable: (produc735959047riable > produc1078154247n_game)).
% 39.89/10.12 thf(produc354409183n_game_decl, type, produc354409183n_game: (produc1078154247n_game > produc735959047riable)).
% 39.89/10.12 thf(collect_variable_decl, type, collect_variable: ((variable > $o) > set_variable)).
% 39.89/10.12 thf(static_BVG_decl, type, static_BVG: (game > set_variable)).
% 39.89/10.12 thf(choice_decl, type, choice: (game > (game > game))).
% 39.89/10.12 thf(compose_decl, type, compose: (game > (game > game))).
% 39.89/10.12 thf(loop_decl, type, loop: (game > game)).
% 39.89/10.12 thf(uSubst1484167963hoiceo_decl, type, uSubst1484167963hoiceo: (option_game > (option_game > option_game))).
% 39.89/10.12 thf(uSubst532817840mposeo_decl, type, uSubst532817840mposeo: (option_game > (option_game > option_game))).
% 39.89/10.12 thf(uSubst23177304_Loopo_decl, type, uSubst23177304_Loopo: (option_game > option_game)).
% 39.89/10.12 thf(uSubst516392814stappp_decl, type, uSubst516392814stappp: (produc1418842292n_game > (set_variable > (game > produc1078154247n_game)))).
% 39.89/10.12 thf(member191809696n_game_decl, type, member191809696n_game: (produc1016592119n_game > (set_Pr1625152599n_game > $o))).
% 39.89/10.12 thf(member_variable_decl, type, member_variable: (variable > (set_variable > $o))).
% 39.89/10.12 thf(ua_decl, type, ua: set_variable).
% 39.89/10.12 thf(alpha_decl, type, alpha: game).
% 39.89/10.12 thf(beta_decl, type, beta: game).
% 39.89/10.12 thf(sigma_decl, type, sigma: produc1418842292n_game).
% 39.89/10.12 thf(172,axiom,((! [A:set_variable,B:set_variable,C:set_variable,D:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ C @ D) => (ord_le282106107riable @ (sup_sup_set_variable @ A @ C) @ (sup_sup_set_variable @ B @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_182_sup_Omono)).
% 39.89/10.12 thf(892,plain,((! [A:set_variable,B:set_variable,C:set_variable,D:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ C @ D) => (ord_le282106107riable @ (sup_sup_set_variable @ A @ C) @ (sup_sup_set_variable @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 39.89/10.12 thf(216,axiom,((((=) @ set_variable) = (^ [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) & (ord_le282106107riable @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_223_order__class_Oorder_Oeq__iff)).
% 39.89/10.12 thf(1036,plain,((((=) @ set_variable) = (^ [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) & (ord_le282106107riable @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 39.89/10.12 thf(25,axiom,((! [A:option_game,B:option_game,C:option_game,D:option_game]: (((produc1111617711n_game @ A @ B) = (produc1111617711n_game @ C @ D)) => (~ ((A = C) => (B != D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_253_Pair__inject)).
% 39.89/10.12 thf(365,plain,((! [A:option_game,B:option_game,C:option_game,D:option_game]: (((produc1111617711n_game @ A @ B) = (produc1111617711n_game @ C @ D)) => (~ ((A = C) => (~ (B = D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 39.89/10.12 thf(234,axiom,((! [A:set_variable,B:set_variable,C:(variable > $o)]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ A @ (collect_variable @ (^ [D:variable]: ((member_variable @ D @ B) & (C @ D))))) = (! [D:variable]: ((member_variable @ D @ A) => (C @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_310_subset__Collect__iff)).
% 39.89/10.12 thf(1105,plain,((! [A:set_variable,B:set_variable,C:(variable > $o)]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ A @ (collect_variable @ (^ [D:variable]: ((member_variable @ D @ B) & (C @ D))))) = (! [D:variable]: ((member_variable @ D @ A) => (C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[234])).
% 39.89/10.12 thf(22,axiom,((! [A:set_variable,B:option_game,C:set_variable,D:option_game]: (((produc1149443391n_game @ A @ B) = (produc1149443391n_game @ C @ D)) => (~ ((A = C) => (B != D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_252_Pair__inject)).
% 39.89/10.12 thf(347,plain,((! [A:set_variable,B:option_game,C:set_variable,D:option_game]: (((produc1149443391n_game @ A @ B) = (produc1149443391n_game @ C @ D)) => (~ ((A = C) => (~ (B = D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 39.89/10.12 thf(159,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => (ord_le282106107riable @ A @ (sup_sup_set_variable @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_163_sup_OcoboundedI2)).
% 39.89/10.12 thf(846,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => (ord_le282106107riable @ A @ (sup_sup_set_variable @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 39.89/10.12 thf(66,axiom,((! [A:(variable > $o),B:(variable > $o)]: ((sup_sup_variable_o @ A @ (sup_sup_variable_o @ A @ B)) = (sup_sup_variable_o @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_65_sup_Oleft__idem)).
% 39.89/10.12 thf(518,plain,((! [A:(variable > $o),B:(variable > $o)]: ((sup_sup_variable_o @ A @ (sup_sup_variable_o @ A @ B)) = (sup_sup_variable_o @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 39.89/10.12 thf(135,axiom,((! [A:produc1078154247n_game]: ((produc884810027riable @ (produc354409183n_game @ A)) = (produc293487213n_game @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_233_fst__swap)).
% 39.89/10.12 thf(777,plain,((! [A:produc1078154247n_game]: ((produc884810027riable @ (produc354409183n_game @ A)) = (produc293487213n_game @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 39.89/10.12 thf(95,axiom,((! [A:set_variable,B:set_variable,C:produc1418842292n_game,D:game]: ((ord_le282106107riable @ A @ B) => (ord_le282106107riable @ (produc893821739n_game @ (uSubst516392814stappp @ C @ A @ D)) @ (produc893821739n_game @ (uSubst516392814stappp @ C @ B @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_6_usubstappp__fst__mon)).
% 39.89/10.12 thf(628,plain,((! [A:set_variable,B:set_variable,C:produc1418842292n_game,D:game]: ((ord_le282106107riable @ A @ B) => (ord_le282106107riable @ (produc893821739n_game @ (uSubst516392814stappp @ C @ A @ D)) @ (produc893821739n_game @ (uSubst516392814stappp @ C @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 39.89/10.12 thf(214,axiom,((! [A:(variable > $o),B:(variable > $o)]: ((! [C:variable]: ((A @ C) => (B @ C))) => (ord_le282106107riable @ (collect_variable @ A) @ (collect_variable @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_83_Collect__mono)).
% 39.89/10.12 thf(1031,plain,((! [A:(variable > $o),B:(variable > $o)]: ((! [C:variable]: ((A @ C) => (B @ C))) => (ord_le282106107riable @ (collect_variable @ (A)) @ (collect_variable @ (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 39.89/10.12 thf(166,axiom,((sup_sup_set_variable = (^ [A:set_variable,B:set_variable]: (sup_sup_set_variable @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_125_sup__commute)).
% 39.89/10.12 thf(873,plain,(((sup_sup_set_variable) = (^ [A:set_variable,B:set_variable]: (sup_sup_set_variable @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 39.89/10.12 thf(246,axiom,((((=) @ set_variable) = (^ [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) & (ord_le282106107riable @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_218_eq__iff)).
% 39.89/10.12 thf(1142,plain,((((=) @ set_variable) = (^ [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) & (ord_le282106107riable @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[246])).
% 39.89/10.12 thf(6,axiom,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ((A = B) => (ord_le1780499447n_game @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_90_equalityD2)).
% 39.89/10.12 thf(269,plain,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ((A = B) => (ord_le1780499447n_game @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 39.89/10.12 thf(86,axiom,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ B @ A) => (B = A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_231_dual__order_Oantisym)).
% 39.89/10.12 thf(597,plain,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ B @ A) => (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 39.89/10.12 thf(168,axiom,((! [A:produc1418842292n_game,B:set_variable,C:game]: (((produc293487213n_game @ (uSubst516392814stappp @ A @ B @ (loop @ C))) != none_game) => (((produc293487213n_game @ (uSubst516392814stappp @ A @ B @ C)) != none_game) & ((produc293487213n_game @ (uSubst516392814stappp @ A @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ C)) != none_game))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_205_usubstappp__loop__conv)).
% 39.89/10.12 thf(878,plain,((! [A:produc1418842292n_game,B:set_variable,C:game]: ((~ ((produc293487213n_game @ (uSubst516392814stappp @ A @ B @ (loop @ C))) = none_game)) => (~ ((produc293487213n_game @ (uSubst516392814stappp @ A @ B @ C)) = none_game) & ~ ((produc293487213n_game @ (uSubst516392814stappp @ A @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ C)) = none_game))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 39.89/10.12 thf(64,axiom,((! [A:produc1078154247n_game]: ~ (! [B:set_variable,C:option_game]: (A != (produc1149443391n_game @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_250_old_Oprod_Oexhaust)).
% 39.89/10.12 thf(511,plain,((! [A:produc1078154247n_game]: ~ (! [B:set_variable,C:option_game]: ~ (A = (produc1149443391n_game @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 39.89/10.12 thf(244,axiom,((! [A:set_variable,B:(variable > $o)]: (ord_le282106107riable @ (collect_variable @ (^ [C:variable]: ((member_variable @ C @ A) & (B @ C)))) @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_305_Collect__subset)).
% 39.89/10.12 thf(1137,plain,((! [A:set_variable,B:(variable > $o)]: (ord_le282106107riable @ (collect_variable @ (^ [C:variable]: ((member_variable @ C @ A) & (B @ C)))) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[244])).
% 39.89/10.12 thf(255,axiom,((ord_le282106107riable @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ ua @ (compose @ alpha @ beta))))) @ (sup_sup_set_variable @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)))) @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)) @ beta))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_fact)).
% 39.89/10.12 thf(1164,plain,((ord_le282106107riable @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ ua @ (compose @ alpha @ beta))))) @ (sup_sup_set_variable @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)))) @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)) @ beta))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[255])).
% 39.89/10.12 thf(53,axiom,((! [A:game]: ((uSubst532817840mposeo @ none_game @ (some_game @ A)) = none_game))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_350_Composeo_Osimps_I3_J)).
% 39.89/10.12 thf(472,plain,((! [A:game]: ((uSubst532817840mposeo @ none_game @ (some_game @ A)) = none_game))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 39.89/10.12 thf(177,axiom,((sup_sup_set_variable = (^ [A:set_variable,B:set_variable]: (collect_variable @ (sup_sup_variable_o @ (^ [C:variable]: (member_variable @ C @ A)) @ (^ [C:variable]: (member_variable @ C @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_307_sup__set__def)).
% 39.89/10.12 thf(913,plain,(((sup_sup_set_variable) = (^ [A:set_variable,B:set_variable]: (collect_variable @ (sup_sup_variable_o @ (^ [C:variable]: (member_variable @ C @ A)) @ (^ [C:variable]: (member_variable @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 39.89/10.12 thf(153,axiom,((! [A:variable,B:set_variable,C:set_variable]: ((member_variable @ A @ (sup_sup_set_variable @ B @ C)) => ((~ (member_variable @ A @ B)) => (member_variable @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_161_UnE)).
% 39.89/10.12 thf(829,plain,((! [A:variable,B:set_variable,C:set_variable]: ((member_variable @ A @ (sup_sup_set_variable @ B @ C)) => ((~ (member_variable @ A @ B)) => (member_variable @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 39.89/10.12 thf(174,axiom,((((=) @ set_variable) = (^ [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) & (ord_le282106107riable @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_77_set__eq__subset)).
% 39.89/10.12 thf(898,plain,((((=) @ set_variable) = (^ [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) & (ord_le282106107riable @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 39.89/10.12 thf(204,axiom,((! [A:(option_game > (set_variable > $o)),B:produc1078154247n_game]: ((A @ (produc293487213n_game @ B) @ (produc893821739n_game @ B)) => (~ (! [C:set_variable,D:option_game]: ~ (A @ D @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_203_exE__realizer_H)).
% 39.89/10.12 thf(1001,plain,((! [A:(option_game > (set_variable > $o)),B:produc1078154247n_game]: ((A @ (produc293487213n_game @ B) @ (produc893821739n_game @ B)) => (~ (! [C:set_variable,D:option_game]: ~ (A @ D @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 39.89/10.12 thf(157,axiom,((sup_sup_set_variable = (^ [A:set_variable,B:set_variable]: (sup_sup_set_variable @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_154_Un__commute)).
% 39.89/10.12 thf(841,plain,(((sup_sup_set_variable) = (^ [A:set_variable,B:set_variable]: (sup_sup_set_variable @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 39.89/10.12 thf(219,axiom,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ B @ A) => (A = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_49_subset__antisym)).
% 39.89/10.12 thf(1046,plain,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 39.89/10.12 thf(13,axiom,((((=) @ set_Pr1625152599n_game) = (^ [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ((ord_le1780499447n_game @ A @ B) & (ord_le1780499447n_game @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_75_set__eq__subset)).
% 39.89/10.12 thf(288,plain,((((=) @ set_Pr1625152599n_game) = (^ [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ((ord_le1780499447n_game @ A @ B) & (ord_le1780499447n_game @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 39.89/10.12 thf(76,axiom,((! [A:option_game,B:option_game,C:set_Pr1625152599n_game,D:option_game]: ((member191809696n_game @ (produc1111617711n_game @ A @ B) @ C) => ((D = B) => (member191809696n_game @ (produc1111617711n_game @ A @ D) @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_326_ssubst__Pair__rhs)).
% 39.89/10.12 thf(565,plain,((! [A:option_game,B:option_game,C:set_Pr1625152599n_game,D:option_game]: ((member191809696n_game @ (produc1111617711n_game @ A @ B) @ C) => ((D = B) => (member191809696n_game @ (produc1111617711n_game @ A @ D) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 39.89/10.12 thf(1,conjecture,((ord_le282106107riable @ (sup_sup_set_variable @ ua @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ ua @ (compose @ alpha @ beta)))))) @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)) @ beta)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 39.89/10.12 thf(2,negated_conjecture,((~ (ord_le282106107riable @ (sup_sup_set_variable @ ua @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ ua @ (compose @ alpha @ beta)))))) @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)) @ beta))))),inference(neg_conjecture,[status(cth)],[1])).
% 39.89/10.12 thf(257,plain,((~ (ord_le282106107riable @ (sup_sup_set_variable @ ua @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ ua @ (compose @ alpha @ beta)))))) @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)) @ beta))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 39.89/10.12 thf(27,axiom,((! [A:(produc1078154247n_game > $o),B:produc1078154247n_game]: ((! [C:set_variable,D:option_game]: (A @ (produc1149443391n_game @ C @ D))) => (A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_254_prod__cases)).
% 39.89/10.12 thf(389,plain,((! [A:(produc1078154247n_game > $o),B:produc1078154247n_game]: ((! [C:set_variable,D:option_game]: (A @ (produc1149443391n_game @ C @ D))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 39.89/10.12 thf(222,axiom,((ord_le282106107riable = (^ [A:set_variable,B:set_variable]: ! [C:variable]: ((member_variable @ C @ A) => (member_variable @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_98_subset__eq)).
% 39.89/10.12 thf(1055,plain,(((ord_le282106107riable) = (^ [A:set_variable,B:set_variable]: ! [C:variable]: ((member_variable @ C @ A) => (member_variable @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 39.89/10.12 thf(77,axiom,((produc345397471riable = (^ [A:produc735959047riable]: (produc1149443391n_game @ (produc284475501riable @ A) @ (produc884810027riable @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_266_prod_Oswap__def)).
% 39.89/10.12 thf(570,plain,(((produc345397471riable) = (^ [A:produc735959047riable]: (produc1149443391n_game @ (produc284475501riable @ A) @ (produc884810027riable @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 39.89/10.12 thf(138,axiom,((! [A:produc1078154247n_game]: ((produc1149443391n_game @ (produc893821739n_game @ A) @ (produc293487213n_game @ A)) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_247_prod_Ocollapse)).
% 39.89/10.12 thf(785,plain,((! [A:produc1078154247n_game]: ((produc1149443391n_game @ (produc893821739n_game @ A) @ (produc293487213n_game @ A)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 39.89/10.12 thf(143,axiom,((bNF_sn1374695591n_game = (^ [A:(set_variable > (option_game > $o)),B:(option_game > (option_game > $o)),C:produc1078154247n_game]: (produc1111617711n_game @ (bNF_pi856525207n_game @ A @ B @ (produc893821739n_game @ C) @ (produc293487213n_game @ C)) @ (produc293487213n_game @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_301_sndOp__def)).
% 39.89/10.12 thf(802,plain,(((bNF_sn1374695591n_game) = (^ [A:(set_variable > (option_game > $o)),B:(option_game > (option_game > $o)),C:produc1078154247n_game]: (produc1111617711n_game @ (bNF_pi856525207n_game @ A @ B @ (produc893821739n_game @ C) @ (produc293487213n_game @ C)) @ (produc293487213n_game @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 39.89/10.12 thf(23,axiom,((! [A:option_game,B:game]: ((A = (some_game @ B)) => (A != none_game)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_340_option_OdiscI)).
% 39.89/10.12 thf(357,plain,((! [A:option_game,B:game]: ((A = (some_game @ B)) => (~ (A = none_game))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 39.89/10.12 thf(49,axiom,((! [A:(variable > $o)]: ((sup_sup_variable_o @ A @ A) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_35_sup_Oidem)).
% 39.89/10.12 thf(460,plain,((! [A:(variable > $o)]: ((sup_sup_variable_o @ A @ A) = (A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 39.89/10.12 thf(83,axiom,((! [A:set_variable,B:set_variable]: ((! [C:variable]: ((member_variable @ C @ A) => (member_variable @ C @ B))) => (ord_le282106107riable @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_52_subsetI)).
% 39.89/10.12 thf(587,plain,((! [A:set_variable,B:set_variable]: ((! [C:variable]: ((member_variable @ C @ A) => (member_variable @ C @ B))) => (ord_le282106107riable @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 39.89/10.12 thf(156,axiom,((! [A:set_variable,B:set_variable]: ((sup_sup_set_variable @ A @ (sup_sup_set_variable @ A @ B)) = (sup_sup_set_variable @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_153_Un__left__absorb)).
% 39.89/10.12 thf(838,plain,((! [A:set_variable,B:set_variable]: ((sup_sup_set_variable @ A @ (sup_sup_set_variable @ A @ B)) = (sup_sup_set_variable @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 39.89/10.12 thf(179,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ (sup_sup_set_variable @ A @ B) @ C) => (~ ((ord_le282106107riable @ A @ C) => (~ (ord_le282106107riable @ B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_171_sup_OboundedE)).
% 39.89/10.12 thf(917,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ (sup_sup_set_variable @ A @ B) @ C) => (~ ((ord_le282106107riable @ A @ C) => (~ (ord_le282106107riable @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 39.89/10.12 thf(115,axiom,((ord_le282106107riable = (^ [A:set_variable,B:set_variable]: ((sup_sup_set_variable @ A @ B) = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_165_sup_Oabsorb__iff2)).
% 39.89/10.12 thf(702,plain,(((ord_le282106107riable) = (^ [A:set_variable,B:set_variable]: ((sup_sup_set_variable @ A @ B) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 39.89/10.12 thf(128,axiom,((! [A:set_variable,B:(variable > $o)]: (ord_le282106107riable @ (collect_variable @ (^ [C:variable]: ((member_variable @ C @ A) & (B @ C)))) @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_327_Collect__restrict)).
% 39.89/10.12 thf(751,plain,((! [A:set_variable,B:(variable > $o)]: (ord_le282106107riable @ (collect_variable @ (^ [C:variable]: ((member_variable @ C @ A) & (B @ C)))) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 39.89/10.12 thf(224,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((sup_sup_set_variable @ A @ (sup_sup_set_variable @ B @ C)) = (sup_sup_set_variable @ B @ (sup_sup_set_variable @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_149_inf__sup__aci_I7_J)).
% 39.89/10.12 thf(1059,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((sup_sup_set_variable @ A @ (sup_sup_set_variable @ B @ C)) = (sup_sup_set_variable @ B @ (sup_sup_set_variable @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 39.89/10.12 thf(242,axiom,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ B @ A) => (A = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_226_order__class_Oorder_Oantisym)).
% 39.89/10.12 thf(1132,plain,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 39.89/10.12 thf(248,axiom,((! [A:set_variable,B:set_variable]: (ord_le282106107riable @ A @ (sup_sup_set_variable @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_195_Un__upper2)).
% 39.89/10.12 thf(1147,plain,((! [A:set_variable,B:set_variable]: (ord_le282106107riable @ A @ (sup_sup_set_variable @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[248])).
% 39.89/10.12 thf(37,axiom,((! [A:set_variable,B:option_game,C:set_variable,D:option_game]: (((produc1149443391n_game @ A @ B) = (produc1149443391n_game @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_239_old_Oprod_Oinject)).
% 39.89/10.12 thf(421,plain,((! [A:set_variable,B:option_game,C:set_variable,D:option_game]: (((produc1149443391n_game @ A @ B) = (produc1149443391n_game @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 39.89/10.12 thf(237,axiom,((! [A:(variable > $o),B:(variable > $o)]: ((ord_le282106107riable @ (collect_variable @ A) @ (collect_variable @ B)) = (! [C:variable]: ((A @ C) => (B @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_74_Collect__mono__iff)).
% 39.89/10.12 thf(1115,plain,((! [A:(variable > $o),B:(variable > $o)]: ((ord_le282106107riable @ (collect_variable @ (A)) @ (collect_variable @ (B))) = (! [C:variable]: ((A @ C) => (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 39.89/10.12 thf(46,axiom,((! [A:(option_game > $o),B:option_game]: ((A @ none_game) => ((! [C:game]: (A @ (some_game @ C))) => (A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_338_option_Oinducts)).
% 39.89/10.12 thf(448,plain,((! [A:(option_game > $o),B:option_game]: ((A @ none_game) => ((! [C:game]: (A @ (some_game @ C))) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 39.89/10.12 thf(149,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((sup_sup_set_variable @ (sup_sup_set_variable @ A @ B) @ C) = (sup_sup_set_variable @ A @ (sup_sup_set_variable @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_143_sup_Oassoc)).
% 39.89/10.12 thf(817,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((sup_sup_set_variable @ (sup_sup_set_variable @ A @ B) @ C) = (sup_sup_set_variable @ A @ (sup_sup_set_variable @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 39.89/10.12 thf(176,axiom,((! [A:(set_variable > $o),B:set_variable,C:(option_game > $o),D:option_game]: ((A @ B) => ((C @ D) => ((A @ (produc893821739n_game @ (produc1149443391n_game @ B @ D))) & (C @ (produc293487213n_game @ (produc1149443391n_game @ B @ D)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_278_conjI__realizer)).
% 39.89/10.12 thf(902,plain,((! [A:(set_variable > $o),B:set_variable,C:(option_game > $o),D:option_game]: ((A @ B) => ((C @ D) => ((A @ (produc893821739n_game @ (produc1149443391n_game @ B @ D))) & (C @ (produc293487213n_game @ (produc1149443391n_game @ B @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 39.89/10.12 thf(193,axiom,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((sup_sup_set_variable @ A @ B) = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_194_Un__absorb1)).
% 39.89/10.12 thf(969,plain,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((sup_sup_set_variable @ A @ B) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 39.89/10.12 thf(89,axiom,((! [A:set_variable,B:set_variable,C:(variable > $o),D:(variable > $o)]: ((ord_le282106107riable @ A @ B) => ((! [E:variable]: ((member_variable @ E @ A) => ((C @ E) => (D @ E)))) => (ord_le282106107riable @ (collect_variable @ (^ [E:variable]: ((member_variable @ E @ A) & (C @ E)))) @ (collect_variable @ (^ [E:variable]: ((member_variable @ E @ B) & (D @ E))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_309_subset__CollectI)).
% 39.89/10.12 thf(606,plain,((! [A:set_variable,B:set_variable,C:(variable > $o),D:(variable > $o)]: ((ord_le282106107riable @ A @ B) => ((! [E:variable]: ((member_variable @ E @ A) => ((C @ E) => (D @ E)))) => (ord_le282106107riable @ (collect_variable @ (^ [E:variable]: ((member_variable @ E @ A) & (C @ E)))) @ (collect_variable @ (^ [E:variable]: ((member_variable @ E @ B) & (D @ E))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 39.89/10.12 thf(208,axiom,((! [A:produc1078154247n_game]: (A = (produc1149443391n_game @ (produc893821739n_game @ A) @ (produc293487213n_game @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_276_prod_Oexhaust__sel)).
% 39.89/10.12 thf(1013,plain,((! [A:produc1078154247n_game]: (A = (produc1149443391n_game @ (produc893821739n_game @ A) @ (produc293487213n_game @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 39.89/10.12 thf(11,axiom,((ord_le1780499447n_game = (^ [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ! [C:produc1016592119n_game]: ((member191809696n_game @ C @ A) => (member191809696n_game @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_87_subset__iff)).
% 39.89/10.12 thf(284,plain,(((ord_le1780499447n_game) = (^ [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ! [C:produc1016592119n_game]: ((member191809696n_game @ C @ A) => (member191809696n_game @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 39.89/10.12 thf(84,axiom,((! [A:produc1418842292n_game,B:set_variable,C:game]: ((uSubst516392814stappp @ A @ B @ (loop @ C)) = (produc1149443391n_game @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ (uSubst23177304_Loopo @ (produc293487213n_game @ (uSubst516392814stappp @ A @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_312_usubstappp_Osimps_I6_J)).
% 39.89/10.12 thf(591,plain,((! [A:produc1418842292n_game,B:set_variable,C:game]: ((uSubst516392814stappp @ A @ B @ (loop @ C)) = (produc1149443391n_game @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ (uSubst23177304_Loopo @ (produc293487213n_game @ (uSubst516392814stappp @ A @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 39.89/10.12 thf(235,axiom,((! [A:set_variable,B:set_variable]: ((sup_sup_set_variable @ (sup_sup_set_variable @ A @ B) @ B) = (sup_sup_set_variable @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_58_sup_Oright__idem)).
% 39.89/10.12 thf(1109,plain,((! [A:set_variable,B:set_variable]: ((sup_sup_set_variable @ (sup_sup_set_variable @ A @ B) @ B) = (sup_sup_set_variable @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 39.89/10.12 thf(54,axiom,((! [A:produc1078154247n_game]: ? [B:set_variable,C:option_game]: (A = (produc1149443391n_game @ B @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_256_surj__pair)).
% 39.89/10.12 thf(475,plain,((! [A:produc1078154247n_game]: ? [B:set_variable,C:option_game]: (A = (produc1149443391n_game @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 39.89/10.12 thf(181,axiom,((! [A:(set_variable > (set_variable > set_variable)),B:set_variable,C:set_variable]: ((! [D:set_variable,E:set_variable]: (ord_le282106107riable @ D @ (A @ D @ E))) => ((! [D:set_variable,E:set_variable]: (ord_le282106107riable @ E @ (A @ D @ E))) => ((! [D:set_variable,E:set_variable,F:set_variable]: ((ord_le282106107riable @ E @ D) => ((ord_le282106107riable @ F @ D) => (ord_le282106107riable @ (A @ E @ F) @ D)))) => ((sup_sup_set_variable @ B @ C) = (A @ B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_176_sup__unique)).
% 39.89/10.12 thf(924,plain,((! [A:(set_variable > (set_variable > set_variable)),B:set_variable,C:set_variable]: ((! [D:set_variable,E:set_variable]: (ord_le282106107riable @ D @ (A @ D @ E))) => ((! [D:set_variable,E:set_variable]: (ord_le282106107riable @ E @ (A @ D @ E))) => ((! [D:set_variable,E:set_variable,F:set_variable]: ((ord_le282106107riable @ E @ D) => ((ord_le282106107riable @ F @ D) => (ord_le282106107riable @ (A @ E @ F) @ D)))) => ((sup_sup_set_variable @ B @ C) = (A @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 39.89/10.12 thf(57,axiom,((! [A:(produc1078154247n_game > $o),B:produc1078154247n_game]: ((! [C:set_variable,D:option_game]: (A @ (produc1149443391n_game @ C @ D))) => (A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_248_old_Oprod_Oinducts)).
% 39.89/10.12 thf(485,plain,((! [A:(produc1078154247n_game > $o),B:produc1078154247n_game]: ((! [C:set_variable,D:option_game]: (A @ (produc1149443391n_game @ C @ D))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 39.89/10.12 thf(155,axiom,((! [A:set_variable,B:option_game,C:set_variable]: (((produc893821739n_game @ (produc1149443391n_game @ A @ B)) = C) => (A = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_259_fst__eqD)).
% 39.89/10.12 thf(834,plain,((! [A:set_variable,B:option_game,C:set_variable]: (((produc893821739n_game @ (produc1149443391n_game @ A @ B)) = C) => (A = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 39.89/10.12 thf(197,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((sup_sup_set_variable @ A @ (sup_sup_set_variable @ B @ C)) = (sup_sup_set_variable @ B @ (sup_sup_set_variable @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_152_Un__left__commute)).
% 39.89/10.12 thf(981,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((sup_sup_set_variable @ A @ (sup_sup_set_variable @ B @ C)) = (sup_sup_set_variable @ B @ (sup_sup_set_variable @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 39.89/10.12 thf(122,axiom,((! [A:set_variable,B:produc1078154247n_game]: ((A = (produc893821739n_game @ B)) = (? [C:option_game]: (B = (produc1149443391n_game @ A @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_298_eq__fst__iff)).
% 39.89/10.12 thf(734,plain,((! [A:set_variable,B:produc1078154247n_game]: ((A = (produc893821739n_game @ B)) = (? [C:option_game]: (B = (produc1149443391n_game @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 39.89/10.12 thf(188,axiom,((! [A:set_variable,B:set_variable]: (ord_le282106107riable @ A @ (sup_sup_set_variable @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_168_sup_Ocobounded1)).
% 39.89/10.12 thf(956,plain,((! [A:set_variable,B:set_variable]: (ord_le282106107riable @ A @ (sup_sup_set_variable @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 39.89/10.12 thf(101,axiom,((! [A:set_variable,B:set_variable,C:set_variable,D:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ C @ D) => (ord_le282106107riable @ (sup_sup_set_variable @ A @ C) @ (sup_sup_set_variable @ B @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_198_Un__mono)).
% 39.89/10.12 thf(660,plain,((! [A:set_variable,B:set_variable,C:set_variable,D:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ C @ D) => (ord_le282106107riable @ (sup_sup_set_variable @ A @ C) @ (sup_sup_set_variable @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 39.89/10.12 thf(199,axiom,((sup_sup_set_variable = (^ [A:set_variable,B:set_variable]: (sup_sup_set_variable @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_147_inf__sup__aci_I5_J)).
% 39.89/10.12 thf(988,plain,(((sup_sup_set_variable) = (^ [A:set_variable,B:set_variable]: (sup_sup_set_variable @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 39.89/10.12 thf(29,axiom,((! [A:(option_game > (option_game > $o)),B:option_game,C:option_game]: ((! [D:game,E:game]: (A @ (some_game @ D) @ (some_game @ E))) => ((! [D:option_game]: (A @ D @ none_game)) => ((! [D:game]: (A @ none_game @ (some_game @ D))) => (A @ B @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_343_Composeo_Oinduct)).
% 39.89/10.12 thf(397,plain,((! [A:(option_game > (option_game > $o)),B:option_game,C:option_game]: ((! [D:game,E:game]: (A @ (some_game @ D) @ (some_game @ E))) => ((! [D:option_game]: (A @ D @ none_game)) => ((! [D:game]: (A @ none_game @ (some_game @ D))) => (A @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 39.89/10.12 thf(110,axiom,((! [A:set_variable,B:set_variable]: ((A = (sup_sup_set_variable @ A @ B)) => (ord_le282106107riable @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_177_sup_OorderI)).
% 39.89/10.12 thf(687,plain,((! [A:set_variable,B:set_variable]: ((A = (sup_sup_set_variable @ A @ B)) => (ord_le282106107riable @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 39.89/10.12 thf(5,axiom,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ((! [C:produc1016592119n_game]: ((member191809696n_game @ C @ A) => (member191809696n_game @ C @ B))) => (ord_le1780499447n_game @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_50_subsetI)).
% 39.89/10.12 thf(265,plain,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ((! [C:produc1016592119n_game]: ((member191809696n_game @ C @ A) => (member191809696n_game @ C @ B))) => (ord_le1780499447n_game @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 39.89/10.12 thf(160,axiom,((! [A:produc1078154247n_game,B:set_variable,C:option_game]: ((A = (produc1149443391n_game @ B @ C)) => ((produc893821739n_game @ A) = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_296_fstI)).
% 39.89/10.12 thf(849,plain,((! [A:produc1078154247n_game,B:set_variable,C:option_game]: ((A = (produc1149443391n_game @ B @ C)) => ((produc893821739n_game @ A) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 39.89/10.12 thf(108,axiom,((! [A:produc1418842292n_game,B:set_variable,C:game,D:game]: (((produc293487213n_game @ (uSubst516392814stappp @ A @ B @ (choice @ C @ D))) != none_game) => (((produc293487213n_game @ (uSubst516392814stappp @ A @ B @ C)) != none_game) & ((produc293487213n_game @ (uSubst516392814stappp @ A @ B @ D)) != none_game))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_207_usubstappp__choice__conv)).
% 39.89/10.12 thf(678,plain,((! [A:produc1418842292n_game,B:set_variable,C:game,D:game]: ((~ ((produc293487213n_game @ (uSubst516392814stappp @ A @ B @ (choice @ C @ D))) = none_game)) => (~ ((produc293487213n_game @ (uSubst516392814stappp @ A @ B @ C)) = none_game) & ~ ((produc293487213n_game @ (uSubst516392814stappp @ A @ B @ D)) = none_game))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 39.89/10.12 thf(146,axiom,((! [A:set_variable,B:set_variable]: ((sup_sup_variable_o @ (^ [C:variable]: (member_variable @ C @ A)) @ (^ [C:variable]: (member_variable @ C @ B))) = (^ [C:variable]: (member_variable @ C @ (sup_sup_set_variable @ A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_313_sup__Un__eq)).
% 39.89/10.12 thf(810,plain,((! [A:set_variable,B:set_variable]: ((sup_sup_variable_o @ (^ [C:variable]: (member_variable @ C @ A)) @ (^ [C:variable]: (member_variable @ C @ B))) = (^ [C:variable]: (member_variable @ C @ (sup_sup_set_variable @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 39.89/10.12 thf(70,axiom,((sup_sup_variable_o = (^ [A:(variable > $o),B:(variable > $o),C:variable]: (sup_sup_o @ (A @ C) @ (B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_32_sup__apply)).
% 39.89/10.12 thf(546,plain,(((sup_sup_variable_o) = (^ [A:(variable > $o),B:(variable > $o),C:variable]: (sup_sup_o @ (A @ C) @ (B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 39.89/10.12 thf(141,axiom,((! [A:set_variable,B:set_variable,C:(set_variable > set_variable),D:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ (C @ B) @ D) => ((! [E:set_variable,F:set_variable]: ((ord_le282106107riable @ E @ F) => (ord_le282106107riable @ (C @ E) @ (C @ F)))) => (ord_le282106107riable @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_215_order__subst2)).
% 39.89/10.12 thf(793,plain,((! [A:set_variable,B:set_variable,C:(set_variable > set_variable),D:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ (C @ B) @ D) => ((! [E:set_variable,F:set_variable]: ((ord_le282106107riable @ E @ F) => (ord_le282106107riable @ (C @ E) @ (C @ F)))) => (ord_le282106107riable @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 39.89/10.12 thf(251,axiom,((! [A:produc735959047riable]: ((produc293487213n_game @ (produc345397471riable @ A)) = (produc884810027riable @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_235_snd__swap)).
% 39.89/10.12 thf(1153,plain,((! [A:produc735959047riable]: ((produc293487213n_game @ (produc345397471riable @ A)) = (produc884810027riable @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[251])).
% 39.89/10.12 thf(130,axiom,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((sup_sup_set_variable @ B @ A) = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_193_Un__absorb2)).
% 39.89/10.12 thf(761,plain,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((sup_sup_set_variable @ B @ A) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 39.89/10.12 thf(142,axiom,((! [A:variable,B:set_variable,C:set_variable]: (((~ (member_variable @ A @ B)) => (member_variable @ A @ C)) => (member_variable @ A @ (sup_sup_set_variable @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_28_UnCI)).
% 39.89/10.12 thf(798,plain,((! [A:variable,B:set_variable,C:set_variable]: (((~ (member_variable @ A @ B)) => (member_variable @ A @ C)) => (member_variable @ A @ (sup_sup_set_variable @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 39.89/10.12 thf(223,axiom,((! [A:set_variable,B:set_variable]: (ord_le282106107riable @ A @ (sup_sup_set_variable @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_186_sup__ge1)).
% 39.89/10.12 thf(1057,plain,((! [A:set_variable,B:set_variable]: (ord_le282106107riable @ A @ (sup_sup_set_variable @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 39.89/10.12 thf(16,axiom,((sup_sup_variable_o = (^ [A:(variable > $o),B:(variable > $o)]: (sup_sup_variable_o @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_120_sup__commute)).
% 39.89/10.12 thf(302,plain,(((sup_sup_variable_o) = (^ [A:(variable > $o),B:(variable > $o)]: (sup_sup_variable_o @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 39.89/10.12 thf(150,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((sup_sup_set_variable @ (sup_sup_set_variable @ A @ B) @ C) = (sup_sup_set_variable @ A @ (sup_sup_set_variable @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_156_Un__assoc)).
% 39.89/10.12 thf(820,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((sup_sup_set_variable @ (sup_sup_set_variable @ A @ B) @ C) = (sup_sup_set_variable @ A @ (sup_sup_set_variable @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 39.89/10.12 thf(38,axiom,((! [A:set_variable,B:option_game,C:set_variable,D:option_game]: (((produc1149443391n_game @ A @ B) = (produc1149443391n_game @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_241_prod_Oinject)).
% 39.89/10.12 thf(424,plain,((! [A:set_variable,B:option_game,C:set_variable,D:option_game]: (((produc1149443391n_game @ A @ B) = (produc1149443391n_game @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 39.89/10.12 thf(112,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ C @ B) => (ord_le282106107riable @ (sup_sup_set_variable @ A @ C) @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_170_sup_OboundedI)).
% 39.89/10.12 thf(693,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ C @ B) => (ord_le282106107riable @ (sup_sup_set_variable @ A @ C) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 39.89/10.12 thf(148,axiom,((! [A:set_variable,B:set_variable]: (ord_le282106107riable @ A @ (sup_sup_set_variable @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_189_inf__sup__ord_I3_J)).
% 39.89/10.12 thf(815,plain,((! [A:set_variable,B:set_variable]: (ord_le282106107riable @ A @ (sup_sup_set_variable @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 39.89/10.12 thf(8,axiom,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game,C:produc1016592119n_game]: ((ord_le1780499447n_game @ A @ B) => ((member191809696n_game @ C @ A) => (member191809696n_game @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_102_subsetD)).
% 39.89/10.12 thf(275,plain,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game,C:produc1016592119n_game]: ((ord_le1780499447n_game @ A @ B) => ((member191809696n_game @ C @ A) => (member191809696n_game @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 39.89/10.12 thf(139,axiom,((! [A:game,B:game]: ((uSubst532817840mposeo @ (some_game @ A) @ (some_game @ B)) = (some_game @ (compose @ A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_349_Composeo_Osimps_I1_J)).
% 39.89/10.12 thf(788,plain,((! [A:game,B:game]: ((uSubst532817840mposeo @ (some_game @ A) @ (some_game @ B)) = (some_game @ (compose @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 39.89/10.12 thf(93,axiom,((ord_le282106107riable @ (sup_sup_set_variable @ ua @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha))))) @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_IHa)).
% 39.89/10.12 thf(625,plain,((ord_le282106107riable @ (sup_sup_set_variable @ ua @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha))))) @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 39.89/10.12 thf(42,axiom,((! [A:set_variable,B:option_game]: ((produc354409183n_game @ (produc1149443391n_game @ A @ B)) = (produc1140431679riable @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_244_swap__simp)).
% 39.89/10.12 thf(435,plain,((! [A:set_variable,B:option_game]: ((produc354409183n_game @ (produc1149443391n_game @ A @ B)) = (produc1140431679riable @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 39.89/10.12 thf(103,axiom,((! [A:set_variable]: (ord_le282106107riable @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_199_order__refl)).
% 39.89/10.12 thf(665,plain,((! [A:set_variable]: (ord_le282106107riable @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 39.89/10.12 thf(253,axiom,((! [A:set_variable,B:set_variable,C:(variable > $o)]: ((? [D:variable]: ((member_variable @ D @ (sup_sup_set_variable @ A @ B)) & (C @ D))) = (? [D:variable]: ((member_variable @ D @ A) & (C @ D)) | ? [D:variable]: ((member_variable @ D @ B) & (C @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_158_bex__Un)).
% 39.89/10.12 thf(1159,plain,((! [A:set_variable,B:set_variable,C:(variable > $o)]: ((? [D:variable]: ((member_variable @ D @ (sup_sup_set_variable @ A @ B)) & (C @ D))) = (? [D:variable]: ((member_variable @ D @ A) & (C @ D)) | ? [D:variable]: ((member_variable @ D @ B) & (C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[253])).
% 39.89/10.12 thf(59,axiom,((! [A:option_game]: ((! [B:game]: (A != (some_game @ B))) => (A = none_game)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_346_Loopo_Ocases)).
% 39.89/10.12 thf(493,plain,((! [A:option_game]: ((! [B:game]: ~ (A = (some_game @ B))) => (A = none_game)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 39.89/10.12 thf(72,axiom,((! [A:game,B:game,C:game,D:game]: (((choice @ A @ B) = (choice @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_209_game_Oinject_I4_J)).
% 39.89/10.12 thf(551,plain,((! [A:game,B:game,C:game,D:game]: (((choice @ A @ B) = (choice @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 39.89/10.12 thf(118,axiom,((! [A:option_game,B:option_game,C:option_game]: (((uSubst532817840mposeo @ A @ B) = C) => ((! [D:game]: ((A = (some_game @ D)) => (! [E:game]: ((B = (some_game @ E)) => (C != (some_game @ (compose @ D @ E))))))) => (((B = none_game) => (C != none_game)) => (~ ((A = none_game) => ((? [D:game]: (B = (some_game @ D))) => (C != none_game))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_352_Composeo_Oelims)).
% 39.89/10.12 thf(710,plain,((! [A:option_game,B:option_game,C:option_game]: (((uSubst532817840mposeo @ A @ B) = C) => ((! [D:game]: ((A = (some_game @ D)) => (! [E:game]: ((B = (some_game @ E)) => (~ (C = (some_game @ (compose @ D @ E)))))))) => (((B = none_game) => (~ (C = none_game))) => (~ ((A = none_game) => ((? [D:game]: (B = (some_game @ D))) => (~ (C = none_game)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 39.89/10.12 thf(195,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ (sup_sup_set_variable @ A @ B) @ C) => (~ ((ord_le282106107riable @ A @ C) => (~ (ord_le282106107riable @ B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_188_le__supE)).
% 39.89/10.12 thf(974,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ (sup_sup_set_variable @ A @ B) @ C) => (~ ((ord_le282106107riable @ A @ C) => (~ (ord_le282106107riable @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 39.89/10.12 thf(185,axiom,((! [A:set_variable,B:option_game]: ((produc893821739n_game @ (produc1149443391n_game @ A @ B)) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_270_fst__pair)).
% 39.89/10.12 thf(948,plain,((! [A:set_variable,B:option_game]: ((produc893821739n_game @ (produc1149443391n_game @ A @ B)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 39.89/10.12 thf(239,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => ((B = C) => (ord_le282106107riable @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_225_ord__le__eq__trans)).
% 39.89/10.12 thf(1121,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => ((B = C) => (ord_le282106107riable @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 39.89/10.12 thf(165,axiom,((! [A:produc1418842292n_game,B:set_variable,C:game,D:set_variable]: (((produc293487213n_game @ (uSubst516392814stappp @ A @ B @ C)) != none_game) => (((produc293487213n_game @ (uSubst516392814stappp @ A @ D @ C)) != none_game) => ((produc293487213n_game @ (uSubst516392814stappp @ A @ B @ C)) = (produc293487213n_game @ (uSubst516392814stappp @ A @ D @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_71_usubstappp__det)).
% 39.89/10.12 thf(869,plain,((! [A:produc1418842292n_game,B:set_variable,C:game,D:set_variable]: ((~ ((produc293487213n_game @ (uSubst516392814stappp @ A @ B @ C)) = none_game)) => ((~ ((produc293487213n_game @ (uSubst516392814stappp @ A @ D @ C)) = none_game)) => ((produc293487213n_game @ (uSubst516392814stappp @ A @ B @ C)) = (produc293487213n_game @ (uSubst516392814stappp @ A @ D @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 39.89/10.12 thf(125,axiom,((! [A:set_variable]: ((sup_sup_set_variable @ A @ A) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_40_sup_Oidem)).
% 39.89/10.12 thf(742,plain,((! [A:set_variable]: ((sup_sup_set_variable @ A @ A) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 39.89/10.12 thf(80,axiom,((! [A:option_game,B:option_game]: (((uSubst532817840mposeo @ A @ B) = none_game) = ((A = none_game) | (B = none_game))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_286_Composeo__undef)).
% 39.89/10.12 thf(578,plain,((! [A:option_game,B:option_game]: (((uSubst532817840mposeo @ A @ B) = none_game) = ((A = none_game) | (B = none_game))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 39.89/10.12 thf(137,axiom,((ord_le282106107riable = (^ [A:set_variable,B:set_variable]: ((sup_sup_set_variable @ B @ A) = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_166_sup_Oabsorb__iff1)).
% 39.89/10.12 thf(783,plain,(((ord_le282106107riable) = (^ [A:set_variable,B:set_variable]: ((sup_sup_set_variable @ B @ A) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 39.89/10.12 thf(238,axiom,((! [A:set_variable,B:(variable > $o),C:(variable > $o)]: ((ord_le282106107riable @ A @ (collect_variable @ (^ [D:variable]: ((B @ D) & (C @ D))))) = ((ord_le282106107riable @ A @ (collect_variable @ B)) & (ord_le282106107riable @ A @ (collect_variable @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_323_conj__subset__def)).
% 39.89/10.12 thf(1118,plain,((! [A:set_variable,B:(variable > $o),C:(variable > $o)]: ((ord_le282106107riable @ A @ (collect_variable @ (^ [D:variable]: ((B @ D) & (C @ D))))) = ((ord_le282106107riable @ A @ (collect_variable @ (B))) & (ord_le282106107riable @ A @ (collect_variable @ (C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[238])).
% 39.89/10.12 thf(169,axiom,((! [A:set_variable,B:option_game]: ((produc293487213n_game @ (produc1149443391n_game @ A @ B)) = B))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_265_snd__conv)).
% 39.89/10.12 thf(884,plain,((! [A:set_variable,B:option_game]: ((produc293487213n_game @ (produc1149443391n_game @ A @ B)) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 39.89/10.12 thf(213,axiom,((! [A:set_variable,B:set_variable]: ((sup_sup_set_variable @ A @ (sup_sup_set_variable @ A @ B)) = (sup_sup_set_variable @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_150_inf__sup__aci_I8_J)).
% 39.89/10.12 thf(1028,plain,((! [A:set_variable,B:set_variable]: ((sup_sup_set_variable @ A @ (sup_sup_set_variable @ A @ B)) = (sup_sup_set_variable @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 39.89/10.12 thf(182,axiom,((! [A:variable,B:set_variable,C:set_variable]: ((member_variable @ A @ (sup_sup_set_variable @ B @ C)) = ((member_variable @ A @ B) | (member_variable @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_31_union__or)).
% 39.89/10.12 thf(933,plain,((! [A:variable,B:set_variable,C:set_variable]: ((member_variable @ A @ (sup_sup_set_variable @ B @ C)) = ((member_variable @ A @ B) | (member_variable @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 39.89/10.12 thf(105,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => (ord_le282106107riable @ A @ (sup_sup_set_variable @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_164_sup_OcoboundedI1)).
% 39.89/10.12 thf(669,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => (ord_le282106107riable @ A @ (sup_sup_set_variable @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 39.89/10.12 thf(209,axiom,((! [A:variable,B:set_variable,C:set_variable,D:(variable > $o)]: ((member_variable @ A @ B) => ((ord_le282106107riable @ B @ (collect_variable @ (^ [E:variable]: ((member_variable @ E @ C) & (D @ E))))) => (D @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_324_prop__restrict)).
% 39.89/10.12 thf(1016,plain,((! [A:variable,B:set_variable,C:set_variable,D:(variable > $o)]: ((member_variable @ A @ B) => ((ord_le282106107riable @ B @ (collect_variable @ (^ [E:variable]: ((member_variable @ E @ C) & (D @ E))))) => (D @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 39.89/10.12 thf(73,axiom,((! [A:produc1016592119n_game]: ? [B:option_game,C:option_game]: (A = (produc1111617711n_game @ B @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_257_surj__pair)).
% 39.89/10.12 thf(554,plain,((! [A:produc1016592119n_game]: ? [B:option_game,C:option_game]: (A = (produc1111617711n_game @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 39.89/10.12 thf(129,axiom,((! [A:set_variable,B:set_variable]: ((A = B) => (~ ((ord_le282106107riable @ A @ B) => (~ (ord_le282106107riable @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_101_equalityE)).
% 39.89/10.12 thf(753,plain,((! [A:set_variable,B:set_variable]: ((A = B) => (~ ((ord_le282106107riable @ A @ B) => (~ (ord_le282106107riable @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 39.89/10.12 thf(232,axiom,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((sup_sup_set_variable @ A @ B) = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_174_sup_Oabsorb2)).
% 39.89/10.12 thf(1099,plain,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((sup_sup_set_variable @ A @ B) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 39.89/10.12 thf(65,axiom,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ((ord_le707292176game_o @ (^ [C:option_game,D:option_game]: (member191809696n_game @ (produc1111617711n_game @ C @ D) @ A)) @ (^ [C:option_game,D:option_game]: (member191809696n_game @ (produc1111617711n_game @ C @ D) @ B))) = (ord_le1780499447n_game @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_319_pred__subset__eq2)).
% 39.89/10.12 thf(515,plain,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ((ord_le707292176game_o @ (^ [C:option_game,D:option_game]: (member191809696n_game @ (produc1111617711n_game @ C @ D) @ A)) @ (^ [C:option_game,D:option_game]: (member191809696n_game @ (produc1111617711n_game @ C @ D) @ B))) = (ord_le1780499447n_game @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 39.89/10.12 thf(48,axiom,((! [A:option_game]: ((! [B:game]: (A != (some_game @ B))) = (A = none_game)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_330_not__Some__eq)).
% 39.89/10.12 thf(457,plain,((! [A:option_game]: ((! [B:game]: ~ (A = (some_game @ B))) = (A = none_game)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 39.89/10.12 thf(198,axiom,((! [A:set_variable,B:set_variable,C:produc1418842292n_game,D:game]: ((ord_le282106107riable @ A @ B) => (((produc293487213n_game @ (uSubst516392814stappp @ C @ B @ D)) != none_game) => ((produc293487213n_game @ (uSubst516392814stappp @ C @ B @ D)) = (produc293487213n_game @ (uSubst516392814stappp @ C @ A @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_162_usubstappp__antimon)).
% 39.89/10.12 thf(984,plain,((! [A:set_variable,B:set_variable,C:produc1418842292n_game,D:game]: ((ord_le282106107riable @ A @ B) => ((~ ((produc293487213n_game @ (uSubst516392814stappp @ C @ B @ D)) = none_game)) => ((produc293487213n_game @ (uSubst516392814stappp @ C @ B @ D)) = (produc293487213n_game @ (uSubst516392814stappp @ C @ A @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 39.89/10.12 thf(119,axiom,((ord_le282106107riable = (^ [A:set_variable,B:set_variable]: (B = (sup_sup_set_variable @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_169_sup_Oorder__iff)).
% 39.89/10.12 thf(721,plain,(((ord_le282106107riable) = (^ [A:set_variable,B:set_variable]: (B = (sup_sup_set_variable @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 39.89/10.12 thf(61,axiom,((! [A:option_game]: ((uSubst532817840mposeo @ A @ none_game) = none_game))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_287_Composeo_Osimps_I2_J)).
% 39.89/10.12 thf(503,plain,((! [A:option_game]: ((uSubst532817840mposeo @ A @ none_game) = none_game))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 39.89/10.12 thf(97,axiom,((! [A:produc1078154247n_game]: ((produc284475501riable @ (produc354409183n_game @ A)) = (produc893821739n_game @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_234_snd__swap)).
% 39.89/10.12 thf(633,plain,((! [A:produc1078154247n_game]: ((produc284475501riable @ (produc354409183n_game @ A)) = (produc893821739n_game @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 39.89/10.12 thf(63,axiom,((! [A:(variable > $o),B:(variable > $o),C:(variable > $o)]: ((sup_sup_variable_o @ (sup_sup_variable_o @ A @ B) @ C) = (sup_sup_variable_o @ A @ (sup_sup_variable_o @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_138_sup_Oassoc)).
% 39.89/10.12 thf(508,plain,((! [A:(variable > $o),B:(variable > $o),C:(variable > $o)]: ((sup_sup_variable_o @ (sup_sup_variable_o @ A @ B) @ C) = (sup_sup_variable_o @ A @ (sup_sup_variable_o @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 39.89/10.12 thf(180,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((sup_sup_set_variable @ (sup_sup_set_variable @ A @ B) @ C) = (sup_sup_set_variable @ A @ (sup_sup_set_variable @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_137_sup__assoc)).
% 39.89/10.12 thf(921,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((sup_sup_set_variable @ (sup_sup_set_variable @ A @ B) @ C) = (sup_sup_set_variable @ A @ (sup_sup_set_variable @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 39.89/10.12 thf(215,axiom,((ord_le282106107riable @ (sup_sup_set_variable @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)) @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)) @ beta))))) @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)) @ beta)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_IHb)).
% 39.89/10.12 thf(1035,plain,((ord_le282106107riable @ (sup_sup_set_variable @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)) @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)) @ beta))))) @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)) @ beta)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 39.89/10.12 thf(228,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ (sup_sup_set_variable @ B @ C)) => (~ (! [D:set_variable]: ((ord_le282106107riable @ D @ B) => (! [E:set_variable]: ((ord_le282106107riable @ E @ C) => (A != (sup_sup_set_variable @ D @ E)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_192_subset__UnE)).
% 39.89/10.12 thf(1071,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ (sup_sup_set_variable @ B @ C)) => (~ (! [D:set_variable]: ((ord_le282106107riable @ D @ B) => (! [E:set_variable]: ((ord_le282106107riable @ E @ C) => (~ (A = (sup_sup_set_variable @ D @ E))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 39.89/10.12 thf(133,axiom,((! [A:game]: (ord_le282106107riable @ (static_BVG @ (loop @ A)) @ (static_BVG @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_213_BVG__loop)).
% 39.89/10.12 thf(773,plain,((! [A:game]: (ord_le282106107riable @ (static_BVG @ (loop @ A)) @ (static_BVG @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 39.89/10.12 thf(15,axiom,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ((! [C:option_game,D:option_game]: ((member191809696n_game @ (produc1111617711n_game @ C @ D) @ A) => (member191809696n_game @ (produc1111617711n_game @ C @ D) @ B))) => (ord_le1780499447n_game @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_315_subrelI)).
% 39.89/10.12 thf(298,plain,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ((! [C:option_game,D:option_game]: ((member191809696n_game @ (produc1111617711n_game @ C @ D) @ A) => (member191809696n_game @ (produc1111617711n_game @ C @ D) @ B))) => (ord_le1780499447n_game @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 39.89/10.12 thf(40,axiom,((((?) @ option_game) = (^ [A:(option_game > $o)]: ((A @ none_game) | ? [B:game]: (A @ (some_game @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_337_split__option__ex)).
% 39.89/10.12 thf(430,plain,((((?) @ option_game) = (^ [A:(option_game > $o)]: ((A @ none_game) | ? [B:game]: (A @ (some_game @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 39.89/10.12 thf(162,axiom,((! [A:produc1418842292n_game,B:set_variable,C:game,D:game]: ((uSubst516392814stappp @ A @ B @ (compose @ C @ D)) = (produc1149443391n_game @ (produc893821739n_game @ (uSubst516392814stappp @ A @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ D)) @ (uSubst532817840mposeo @ (produc293487213n_game @ (uSubst516392814stappp @ A @ B @ C)) @ (produc293487213n_game @ (uSubst516392814stappp @ A @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_311_usubstappp_Osimps_I5_J)).
% 39.89/10.12 thf(856,plain,((! [A:produc1418842292n_game,B:set_variable,C:game,D:game]: ((uSubst516392814stappp @ A @ B @ (compose @ C @ D)) = (produc1149443391n_game @ (produc893821739n_game @ (uSubst516392814stappp @ A @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ D)) @ (uSubst532817840mposeo @ (produc293487213n_game @ (uSubst516392814stappp @ A @ B @ C)) @ (produc293487213n_game @ (uSubst516392814stappp @ A @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 39.89/10.12 thf(126,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => (ord_le282106107riable @ A @ (sup_sup_set_variable @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_184_le__supI1)).
% 39.89/10.12 thf(745,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => (ord_le282106107riable @ A @ (sup_sup_set_variable @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 39.89/10.12 thf(45,axiom,((! [A:produc1016592119n_game]: ((! [B:game,C:game]: (A != (produc1111617711n_game @ (some_game @ B) @ (some_game @ C)))) => ((! [B:option_game]: (A != (produc1111617711n_game @ B @ none_game))) => (~ (! [B:game]: (A != (produc1111617711n_game @ none_game @ (some_game @ B))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_333_Composeo_Ocases)).
% 39.89/10.12 thf(444,plain,((! [A:produc1016592119n_game]: ((! [B:game,C:game]: ~ (A = (produc1111617711n_game @ (some_game @ B) @ (some_game @ C)))) => ((! [B:option_game]: ~ (A = (produc1111617711n_game @ B @ none_game))) => (~ (! [B:game]: ~ (A = (produc1111617711n_game @ none_game @ (some_game @ B))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 39.89/10.12 thf(26,axiom,((! [A:option_game,B:option_game]: (((uSubst23177304_Loopo @ A) = B) => ((! [C:game]: ((A = (some_game @ C)) => (B != (some_game @ (loop @ C))))) => (~ ((A = none_game) => (B != none_game))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_328_Loopo_Oelims)).
% 39.89/10.12 thf(375,plain,((! [A:option_game,B:option_game]: (((uSubst23177304_Loopo @ A) = B) => ((! [C:game]: ((A = (some_game @ C)) => (~ (B = (some_game @ (loop @ C)))))) => (~ ((A = none_game) => (~ (B = none_game)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 39.89/10.12 thf(243,axiom,((! [A:set_variable]: (ord_le282106107riable @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_228_dual__order_Orefl)).
% 39.89/10.12 thf(1135,plain,((! [A:set_variable]: (ord_le282106107riable @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[243])).
% 39.89/10.12 thf(34,axiom,((! [A:(variable > $o),B:(variable > $o),C:(variable > $o)]: ((ord_le1407353162able_o @ (sup_sup_variable_o @ A @ B) @ C) = ((ord_le1407353162able_o @ A @ C) & (ord_le1407353162able_o @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_18_sup_Obounded__iff)).
% 39.89/10.12 thf(412,plain,((! [A:(variable > $o),B:(variable > $o),C:(variable > $o)]: ((ord_le1407353162able_o @ (sup_sup_variable_o @ A @ B) @ (C)) = ((ord_le1407353162able_o @ (A) @ (C)) & (ord_le1407353162able_o @ (B) @ (C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 39.89/10.12 thf(82,axiom,((! [A:set_variable,B:set_variable,C:variable]: ((ord_le282106107riable @ A @ B) => ((member_variable @ C @ A) => (member_variable @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_104_subsetD)).
% 39.89/10.12 thf(584,plain,((! [A:set_variable,B:set_variable,C:variable]: ((ord_le282106107riable @ A @ B) => ((member_variable @ C @ A) => (member_variable @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 39.89/10.12 thf(75,axiom,((! [A:game,B:game]: (((loop @ A) = (loop @ B)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_208_game_Oinject_I6_J)).
% 39.89/10.12 thf(562,plain,((! [A:game,B:game]: (((loop @ A) = (loop @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 39.89/10.12 thf(206,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((sup_sup_set_variable @ A @ (sup_sup_set_variable @ B @ C)) = (sup_sup_set_variable @ B @ (sup_sup_set_variable @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_113_sup__left__commute)).
% 39.89/10.12 thf(1007,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((sup_sup_set_variable @ A @ (sup_sup_set_variable @ B @ C)) = (sup_sup_set_variable @ B @ (sup_sup_set_variable @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 39.89/10.12 thf(31,axiom,((! [A:option_game]: ((A != none_game) => (~ (! [B:game]: (A != (some_game @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_339_option_Oexhaust)).
% 39.89/10.12 thf(402,plain,((! [A:option_game]: ((~ (A = none_game)) => (~ (! [B:game]: ~ (A = (some_game @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 39.89/10.12 thf(121,axiom,((((=) @ set_variable) = (^ [A:set_variable,B:set_variable]: ((ord_le282106107riable @ B @ A) & (ord_le282106107riable @ A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_230_dual__order_Oeq__iff)).
% 39.89/10.12 thf(732,plain,((((=) @ set_variable) = (^ [A:set_variable,B:set_variable]: ((ord_le282106107riable @ B @ A) & (ord_le282106107riable @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 39.89/10.12 thf(158,axiom,((! [A:set_variable,B:set_variable]: ((ord_le1407353162able_o @ (^ [C:variable]: (member_variable @ C @ A)) @ (^ [C:variable]: (member_variable @ C @ B))) = (ord_le282106107riable @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_322_pred__subset__eq)).
% 39.89/10.12 thf(843,plain,((! [A:set_variable,B:set_variable]: ((ord_le1407353162able_o @ (^ [C:variable]: (member_variable @ C @ A)) @ (^ [C:variable]: (member_variable @ C @ B))) = (ord_le282106107riable @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 39.89/10.12 thf(12,axiom,((ord_le1780499447n_game = (^ [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ! [C:produc1016592119n_game]: ((member191809696n_game @ C @ A) => (member191809696n_game @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_96_subset__eq)).
% 39.89/10.12 thf(286,plain,(((ord_le1780499447n_game) = (^ [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ! [C:produc1016592119n_game]: ((member191809696n_game @ C @ A) => (member191809696n_game @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 39.89/10.12 thf(167,axiom,((! [A:produc1078154247n_game]: (A = (produc1149443391n_game @ (produc893821739n_game @ A) @ (produc293487213n_game @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_274_surjective__pairing)).
% 39.89/10.12 thf(875,plain,((! [A:produc1078154247n_game]: (A = (produc1149443391n_game @ (produc893821739n_game @ A) @ (produc293487213n_game @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 39.89/10.12 thf(189,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((sup_sup_set_variable @ A @ (sup_sup_set_variable @ B @ C)) = (sup_sup_set_variable @ B @ (sup_sup_set_variable @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_119_sup_Oleft__commute)).
% 39.89/10.12 thf(958,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((sup_sup_set_variable @ A @ (sup_sup_set_variable @ B @ C)) = (sup_sup_set_variable @ B @ (sup_sup_set_variable @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 39.89/10.12 thf(10,axiom,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ((ord_le1780499447n_game @ A @ B) => ((ord_le1780499447n_game @ B @ A) => (A = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_47_subset__antisym)).
% 39.89/10.12 thf(281,plain,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ((ord_le1780499447n_game @ A @ B) => ((ord_le1780499447n_game @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 39.89/10.12 thf(245,axiom,((! [A:variable,B:set_variable,C:set_variable]: ((member_variable @ A @ B) => (member_variable @ A @ (sup_sup_set_variable @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_160_UnI1)).
% 39.89/10.12 thf(1139,plain,((! [A:variable,B:set_variable,C:set_variable]: ((member_variable @ A @ B) => (member_variable @ A @ (sup_sup_set_variable @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[245])).
% 39.89/10.12 thf(183,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ B @ C) => (ord_le282106107riable @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_227_order__trans)).
% 39.89/10.12 thf(936,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ B @ C) => (ord_le282106107riable @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 39.89/10.12 thf(78,axiom,((! [A:(variable > $o)]: ((sup_sup_variable_o @ A @ A) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_41_sup__idem)).
% 39.89/10.12 thf(572,plain,((! [A:(variable > $o)]: ((sup_sup_variable_o @ A @ A) = (A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 39.89/10.12 thf(19,axiom,((! [A:option_game,B:option_game,C:option_game]: (((uSubst1484167963hoiceo @ A @ B) = C) => ((! [D:game]: ((A = (some_game @ D)) => (! [E:game]: ((B = (some_game @ E)) => (C != (some_game @ (choice @ D @ E))))))) => (((B = none_game) => (C != none_game)) => (~ ((A = none_game) => ((? [D:game]: (B = (some_game @ D))) => (C != none_game))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_353_Choiceo_Oelims)).
% 39.89/10.12 thf(313,plain,((! [A:option_game,B:option_game,C:option_game]: (((uSubst1484167963hoiceo @ A @ B) = C) => ((! [D:game]: ((A = (some_game @ D)) => (! [E:game]: ((B = (some_game @ E)) => (~ (C = (some_game @ (choice @ D @ E)))))))) => (((B = none_game) => (~ (C = none_game))) => (~ ((A = none_game) => ((? [D:game]: (B = (some_game @ D))) => (~ (C = none_game)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 39.89/10.12 thf(51,axiom,((! [A:(variable > $o),B:(variable > $o)]: ((sup_sup_variable_o @ A @ (sup_sup_variable_o @ A @ B)) = (sup_sup_variable_o @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_59_sup__left__idem)).
% 39.89/10.12 thf(466,plain,((! [A:(variable > $o),B:(variable > $o)]: ((sup_sup_variable_o @ A @ (sup_sup_variable_o @ A @ B)) = (sup_sup_variable_o @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 39.89/10.12 thf(231,axiom,((! [A:set_variable,B:(set_variable > set_variable),C:set_variable,D:set_variable]: ((A = (B @ C)) => ((ord_le282106107riable @ C @ D) => ((! [E:set_variable,F:set_variable]: ((ord_le282106107riable @ E @ F) => (ord_le282106107riable @ (B @ E) @ (B @ F)))) => (ord_le282106107riable @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_216_ord__eq__le__subst)).
% 39.89/10.12 thf(1090,plain,((! [A:set_variable,B:(set_variable > set_variable),C:set_variable,D:set_variable]: ((A = (B @ C)) => ((ord_le282106107riable @ C @ D) => ((! [E:set_variable,F:set_variable]: ((ord_le282106107riable @ E @ F) => (ord_le282106107riable @ (B @ E) @ (B @ F)))) => (ord_le282106107riable @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[231])).
% 39.89/10.12 thf(144,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ C @ B) => (ord_le282106107riable @ (sup_sup_set_variable @ A @ C) @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_197_Un__least)).
% 39.89/10.12 thf(804,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ C @ B) => (ord_le282106107riable @ (sup_sup_set_variable @ A @ C) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 39.89/10.12 thf(116,axiom,((! [A:set_variable]: (((produc293487213n_game @ (uSubst516392814stappp @ sigma @ A @ alpha)) != none_game) => (ord_le282106107riable @ (sup_sup_set_variable @ A @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ A @ alpha))))) @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ A @ alpha)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_8_Compose_OIH_I1_J)).
% 39.89/10.12 thf(704,plain,((! [A:set_variable]: ((~ ((produc293487213n_game @ (uSubst516392814stappp @ sigma @ A @ alpha)) = none_game)) => (ord_le282106107riable @ (sup_sup_set_variable @ A @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ A @ alpha))))) @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ A @ alpha)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 39.89/10.12 thf(106,axiom,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => (B = (sup_sup_set_variable @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_178_sup_OorderE)).
% 39.89/10.12 thf(672,plain,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => (B = (sup_sup_set_variable @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 39.89/10.12 thf(131,axiom,((! [A:set_variable,B:set_variable,C:set_variable,D:set_variable]: ((A = (sup_sup_set_variable @ B @ C)) => ((sup_sup_set_variable @ A @ D) = (sup_sup_set_variable @ B @ (sup_sup_set_variable @ C @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_146_boolean__algebra__cancel_Osup1)).
% 39.89/10.12 thf(764,plain,((! [A:set_variable,B:set_variable,C:set_variable,D:set_variable]: ((A = (sup_sup_set_variable @ B @ C)) => ((sup_sup_set_variable @ A @ D) = (sup_sup_set_variable @ B @ (sup_sup_set_variable @ C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 39.89/10.12 thf(154,axiom,((! [A:set_variable,B:option_game]: ((produc293487213n_game @ (produc1149443391n_game @ A @ B)) = B))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_272_snd__pair)).
% 39.89/10.12 thf(831,plain,((! [A:set_variable,B:option_game]: ((produc293487213n_game @ (produc1149443391n_game @ A @ B)) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 39.89/10.12 thf(24,axiom,((! [A:(variable > $o),B:(variable > $o),C:(variable > $o)]: ((sup_sup_variable_o @ A @ (sup_sup_variable_o @ B @ C)) = (sup_sup_variable_o @ B @ (sup_sup_variable_o @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_108_sup__left__commute)).
% 39.89/10.12 thf(362,plain,((! [A:(variable > $o),B:(variable > $o),C:(variable > $o)]: ((sup_sup_variable_o @ A @ (sup_sup_variable_o @ B @ C)) = (sup_sup_variable_o @ B @ (sup_sup_variable_o @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 39.89/10.12 thf(247,axiom,((! [A:produc1418842292n_game,B:set_variable,C:game]: ((uSubst516392814stappp @ A @ B @ (loop @ C)) = (produc1149443391n_game @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ (uSubst23177304_Loopo @ (produc293487213n_game @ (uSubst516392814stappp @ A @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_288_usubstappp__loop)).
% 39.89/10.12 thf(1144,plain,((! [A:produc1418842292n_game,B:set_variable,C:game]: ((uSubst516392814stappp @ A @ B @ (loop @ C)) = (produc1149443391n_game @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ (uSubst23177304_Loopo @ (produc293487213n_game @ (uSubst516392814stappp @ A @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[247])).
% 39.89/10.12 thf(123,axiom,((bNF_fs984229733n_game = (^ [A:(set_variable > (option_game > $o)),B:(option_game > (option_game > $o)),C:produc1078154247n_game]: (produc1149443391n_game @ (produc893821739n_game @ C) @ (bNF_pi856525207n_game @ A @ B @ (produc893821739n_game @ C) @ (produc293487213n_game @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_302_fstOp__def)).
% 39.89/10.12 thf(737,plain,(((bNF_fs984229733n_game) = (^ [A:(set_variable > (option_game > $o)),B:(option_game > (option_game > $o)),C:produc1078154247n_game]: (produc1149443391n_game @ (produc893821739n_game @ C) @ (bNF_pi856525207n_game @ A @ B @ (produc893821739n_game @ C) @ (produc293487213n_game @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 39.89/10.12 thf(218,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ C @ A) => (ord_le282106107riable @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_229_dual__order_Otrans)).
% 39.89/10.12 thf(1043,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ C @ A) => (ord_le282106107riable @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 39.89/10.12 thf(91,axiom,((! [A:set_variable,B:option_game,C:option_game]: (((produc293487213n_game @ (produc1149443391n_game @ A @ B)) = C) => (B = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_263_snd__eqD)).
% 39.89/10.12 thf(616,plain,((! [A:set_variable,B:option_game,C:option_game]: (((produc293487213n_game @ (produc1149443391n_game @ A @ B)) = C) => (B = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 39.89/10.12 thf(175,axiom,((produc354409183n_game = (^ [A:produc1078154247n_game]: (produc1140431679riable @ (produc293487213n_game @ A) @ (produc893821739n_game @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_268_prod_Oswap__def)).
% 39.89/10.12 thf(900,plain,(((produc354409183n_game) = (^ [A:produc1078154247n_game]: (produc1140431679riable @ (produc293487213n_game @ A) @ (produc893821739n_game @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 39.89/10.12 thf(32,axiom,((! [A:(variable > $o),B:(variable > $o)]: ((sup_sup_variable_o @ (sup_sup_variable_o @ A @ B) @ B) = (sup_sup_variable_o @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_53_sup_Oright__idem)).
% 39.89/10.12 thf(406,plain,((! [A:(variable > $o),B:(variable > $o)]: ((sup_sup_variable_o @ (sup_sup_variable_o @ A @ B) @ B) = (sup_sup_variable_o @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 39.89/10.12 thf(200,axiom,((! [A:set_variable,B:set_variable,C:variable]: ((ord_le282106107riable @ A @ B) => ((member_variable @ C @ A) => (member_variable @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_107_in__mono)).
% 39.89/10.12 thf(990,plain,((! [A:set_variable,B:set_variable,C:variable]: ((ord_le282106107riable @ A @ B) => ((member_variable @ C @ A) => (member_variable @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 39.89/10.12 thf(202,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ B @ C) => (ord_le282106107riable @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_80_subset__trans)).
% 39.89/10.12 thf(996,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ B @ C) => (ord_le282106107riable @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 39.89/10.12 thf(171,axiom,((! [A:(option_game > (set_variable > $o)),B:option_game,C:set_variable]: ((A @ B @ C) => (A @ (produc293487213n_game @ (produc1149443391n_game @ C @ B)) @ (produc893821739n_game @ (produc1149443391n_game @ C @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_280_exI__realizer)).
% 39.89/10.12 thf(890,plain,((! [A:(option_game > (set_variable > $o)),B:option_game,C:set_variable]: ((A @ B @ C) => (A @ (produc293487213n_game @ (produc1149443391n_game @ C @ B)) @ (produc893821739n_game @ (produc1149443391n_game @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 39.89/10.12 thf(230,axiom,((! [A:option_game,B:option_game]: (((A = none_game) = (B = none_game)) => (((A != none_game) => ((B != none_game) => ((the_game @ A) = (the_game @ B)))) => (A = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_200_option_Oexpand)).
% 39.89/10.12 thf(1080,plain,((! [A:option_game,B:option_game]: (((A = none_game) = (B = none_game)) => (((~ (A = none_game)) => ((~ (B = none_game)) => ((the_game @ A) = (the_game @ B)))) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 39.89/10.12 thf(96,axiom,((ord_le282106107riable = (^ [A:set_variable,B:set_variable]: ((sup_sup_set_variable @ A @ B) = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_191_subset__Un__eq)).
% 39.89/10.12 thf(631,plain,(((ord_le282106107riable) = (^ [A:set_variable,B:set_variable]: ((sup_sup_set_variable @ A @ B) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 39.89/10.12 thf(21,axiom,((((!) @ option_game) = (^ [A:(option_game > $o)]: ((A @ none_game) & ! [B:game]: (A @ (some_game @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_336_split__option__all)).
% 39.89/10.12 thf(345,plain,((((!) @ option_game) = (^ [A:(option_game > $o)]: ((A @ none_game) & ! [B:game]: (A @ (some_game @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 39.89/10.12 thf(85,axiom,((! [A:set_variable,B:option_game]: ((produc893821739n_game @ (produc1149443391n_game @ A @ B)) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_261_fst__conv)).
% 39.89/10.12 thf(594,plain,((! [A:set_variable,B:option_game]: ((produc893821739n_game @ (produc1149443391n_game @ A @ B)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 39.89/10.12 thf(254,axiom,((((=) @ produc1078154247n_game) = (^ [A:produc1078154247n_game,B:produc1078154247n_game]: (((produc893821739n_game @ A) = (produc893821739n_game @ B)) & ((produc293487213n_game @ A) = (produc293487213n_game @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_201_prod__eq__iff)).
% 39.89/10.12 thf(1162,plain,((((=) @ produc1078154247n_game) = (^ [A:produc1078154247n_game,B:produc1078154247n_game]: (((produc893821739n_game @ A) = (produc893821739n_game @ B)) & ((produc293487213n_game @ A) = (produc293487213n_game @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[254])).
% 39.89/10.12 thf(173,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ (sup_sup_set_variable @ A @ B) @ C) = ((ord_le282106107riable @ A @ C) & (ord_le282106107riable @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_17_le__sup__iff)).
% 39.89/10.12 thf(895,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ (sup_sup_set_variable @ A @ B) @ C) = ((ord_le282106107riable @ A @ C) & (ord_le282106107riable @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 39.89/10.12 thf(132,axiom,((! [A:set_variable,B:set_variable]: ((A = B) => (ord_le282106107riable @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_220_eq__refl)).
% 39.89/10.12 thf(769,plain,((! [A:set_variable,B:set_variable]: ((A = B) => (ord_le282106107riable @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 39.89/10.12 thf(211,axiom,((! [A:option_game,B:produc1078154247n_game]: ((A = (produc293487213n_game @ B)) = (? [C:set_variable]: (B = (produc1149443391n_game @ C @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_290_eq__snd__iff)).
% 39.89/10.12 thf(1022,plain,((! [A:option_game,B:produc1078154247n_game]: ((A = (produc293487213n_game @ B)) = (? [C:set_variable]: (B = (produc1149443391n_game @ C @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 39.89/10.12 thf(236,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ (sup_sup_set_variable @ A @ B) @ C) = ((ord_le282106107riable @ A @ C) & (ord_le282106107riable @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_11_Un__subset__iff)).
% 39.89/10.12 thf(1112,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ (sup_sup_set_variable @ A @ B) @ C) = ((ord_le282106107riable @ A @ C) & (ord_le282106107riable @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[236])).
% 39.89/10.12 thf(249,axiom,((! [A:produc1078154247n_game,B:produc1078154247n_game]: ((((produc893821739n_game @ A) = (produc893821739n_game @ B)) & ((produc293487213n_game @ A) = (produc293487213n_game @ B))) => (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_202_prod_Oexpand)).
% 39.89/10.12 thf(1149,plain,((! [A:produc1078154247n_game,B:produc1078154247n_game]: ((((produc893821739n_game @ A) = (produc893821739n_game @ B)) & ((produc293487213n_game @ A) = (produc293487213n_game @ B))) => (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[249])).
% 39.89/10.12 thf(191,axiom,((! [A:set_variable,B:set_variable]: ((sup_sup_set_variable @ A @ (sup_sup_set_variable @ A @ B)) = (sup_sup_set_variable @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_70_sup_Oleft__idem)).
% 39.89/10.12 thf(964,plain,((! [A:set_variable,B:set_variable]: ((sup_sup_set_variable @ A @ (sup_sup_set_variable @ A @ B)) = (sup_sup_set_variable @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 39.89/10.12 thf(94,axiom,((! [A:set_variable,B:produc1418842292n_game,C:game]: (ord_le282106107riable @ A @ (produc893821739n_game @ (uSubst516392814stappp @ B @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_usubst__taboos__mon)).
% 39.89/10.12 thf(626,plain,((! [A:set_variable,B:produc1418842292n_game,C:game]: (ord_le282106107riable @ A @ (produc893821739n_game @ (uSubst516392814stappp @ B @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 39.89/10.12 thf(178,axiom,((! [A:set_variable]: (ord_le282106107riable @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_86_subset__refl)).
% 39.89/10.12 thf(915,plain,((! [A:set_variable]: (ord_le282106107riable @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 39.89/10.12 thf(67,axiom,((! [A:option_game,B:(option_game > (option_game > $o)),C:option_game]: (((A = none_game) => (B @ A @ C)) => (((C = none_game) => (B @ A @ C)) => ((! [D:game,E:game]: ((A = (some_game @ D)) => ((C = (some_game @ E)) => (B @ A @ C)))) => (B @ A @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_335_combine__options__cases)).
% 39.89/10.12 thf(521,plain,((! [A:option_game,B:(option_game > (option_game > $o)),C:option_game]: (((A = none_game) => (B @ A @ C)) => (((C = none_game) => (B @ A @ C)) => ((! [D:game,E:game]: ((A = (some_game @ D)) => ((C = (some_game @ E)) => (B @ A @ C)))) => (B @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 39.89/10.12 thf(152,axiom,((bNF_sn582998327n_game = (^ [A:(set_variable > (set_variable > $o)),B:(set_variable > (option_game > $o)),C:produc1078154247n_game]: (produc1149443391n_game @ (bNF_pi1813424679n_game @ A @ B @ (produc893821739n_game @ C) @ (produc293487213n_game @ C)) @ (produc293487213n_game @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_300_sndOp__def)).
% 39.89/10.12 thf(827,plain,(((bNF_sn582998327n_game) = (^ [A:(set_variable > (set_variable > $o)),B:(set_variable > (option_game > $o)),C:produc1078154247n_game]: (produc1149443391n_game @ (bNF_pi1813424679n_game @ A @ B @ (produc893821739n_game @ C) @ (produc293487213n_game @ C)) @ (produc293487213n_game @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 39.89/10.12 thf(98,axiom,((! [A:game,B:game,C:game,D:game]: ((choice @ A @ B) != (compose @ C @ D)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_212_game_Odistinct_I37_J)).
% 39.89/10.12 thf(636,plain,((! [A:game,B:game,C:game,D:game]: ~ ((choice @ A @ B) = (compose @ C @ D)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 39.89/10.12 thf(9,axiom,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game,C:set_Pr1625152599n_game]: ((ord_le1780499447n_game @ A @ B) => ((ord_le1780499447n_game @ B @ C) => (ord_le1780499447n_game @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_78_subset__trans)).
% 39.89/10.12 thf(278,plain,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game,C:set_Pr1625152599n_game]: ((ord_le1780499447n_game @ A @ B) => ((ord_le1780499447n_game @ B @ C) => (ord_le1780499447n_game @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 39.89/10.12 thf(136,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ C @ B) => (ord_le282106107riable @ (sup_sup_set_variable @ A @ C) @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_187_le__supI)).
% 39.89/10.12 thf(780,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ C @ B) => (ord_le282106107riable @ (sup_sup_set_variable @ A @ C) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 39.89/10.12 thf(28,axiom,((! [A:game]: ((uSubst1484167963hoiceo @ none_game @ (some_game @ A)) = none_game))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_351_Choiceo_Osimps_I3_J)).
% 39.89/10.12 thf(394,plain,((! [A:game]: ((uSubst1484167963hoiceo @ none_game @ (some_game @ A)) = none_game))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 39.89/10.12 thf(233,axiom,((! [A:game]: ((the_game @ (some_game @ A)) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_342_option_Osel)).
% 39.89/10.12 thf(1102,plain,((! [A:game]: ((the_game @ (some_game @ A)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 39.89/10.12 thf(43,axiom,((! [A:option_game,B:option_game,C:option_game,D:option_game]: (((produc1111617711n_game @ A @ B) = (produc1111617711n_game @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_240_old_Oprod_Oinject)).
% 39.89/10.12 thf(438,plain,((! [A:option_game,B:option_game,C:option_game,D:option_game]: (((produc1111617711n_game @ A @ B) = (produc1111617711n_game @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 39.89/10.12 thf(184,axiom,((! [A:set_variable,B:set_variable,C:(set_variable > set_variable),D:set_variable]: ((ord_le282106107riable @ A @ B) => (((C @ B) = D) => ((! [E:set_variable,F:set_variable]: ((ord_le282106107riable @ E @ F) => (ord_le282106107riable @ (C @ E) @ (C @ F)))) => (ord_le282106107riable @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_217_ord__le__eq__subst)).
% 39.89/10.12 thf(939,plain,((! [A:set_variable,B:set_variable,C:(set_variable > set_variable),D:set_variable]: ((ord_le282106107riable @ A @ B) => (((C @ B) = D) => ((! [E:set_variable,F:set_variable]: ((ord_le282106107riable @ E @ F) => (ord_le282106107riable @ (C @ E) @ (C @ F)))) => (ord_le282106107riable @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 39.89/10.12 thf(20,axiom,((! [A:option_game,B:option_game]: ((produc1696194127n_game @ (produc1111617711n_game @ A @ B)) = (produc1111617711n_game @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_245_swap__simp)).
% 39.89/10.12 thf(342,plain,((! [A:option_game,B:option_game]: ((produc1696194127n_game @ (produc1111617711n_game @ A @ B)) = (produc1111617711n_game @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 39.89/10.12 thf(151,axiom,((! [A:game,B:game,C:game]: ((compose @ A @ B) != (loop @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_211_game_Odistinct_I45_J)).
% 39.89/10.12 thf(823,plain,((! [A:game,B:game,C:game]: ~ ((compose @ A @ B) = (loop @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 39.89/10.12 thf(220,axiom,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ B @ A) = (B = A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_222_antisym__conv)).
% 39.89/10.12 thf(1049,plain,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ B @ A) = (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 39.89/10.12 thf(58,axiom,((! [A:(variable > $o),B:(variable > $o),C:(variable > $o)]: ((sup_sup_variable_o @ (sup_sup_variable_o @ A @ B) @ C) = (sup_sup_variable_o @ A @ (sup_sup_variable_o @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_132_sup__assoc)).
% 39.89/10.12 thf(490,plain,((! [A:(variable > $o),B:(variable > $o),C:(variable > $o)]: ((sup_sup_variable_o @ (sup_sup_variable_o @ A @ B) @ C) = (sup_sup_variable_o @ A @ (sup_sup_variable_o @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 39.89/10.12 thf(107,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => (ord_le282106107riable @ A @ (sup_sup_set_variable @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_183_le__supI2)).
% 39.89/10.12 thf(675,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => (ord_le282106107riable @ A @ (sup_sup_set_variable @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 39.89/10.12 thf(102,axiom,((ord_le282106107riable = (^ [A:set_variable,B:set_variable]: ! [C:variable]: ((member_variable @ C @ A) => (member_variable @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_89_subset__iff)).
% 39.89/10.12 thf(663,plain,(((ord_le282106107riable) = (^ [A:set_variable,B:set_variable]: ! [C:variable]: ((member_variable @ C @ A) => (member_variable @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 39.89/10.12 thf(71,axiom,((! [A:option_game,B:option_game,C:option_game,D:option_game]: (((produc1111617711n_game @ A @ B) = (produc1111617711n_game @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_242_prod_Oinject)).
% 39.89/10.12 thf(548,plain,((! [A:option_game,B:option_game,C:option_game,D:option_game]: (((produc1111617711n_game @ A @ B) = (produc1111617711n_game @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 39.89/10.12 thf(74,axiom,((! [A:(produc1016592119n_game > $o),B:produc1016592119n_game]: ((! [C:option_game,D:option_game]: (A @ (produc1111617711n_game @ C @ D))) => (A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_255_prod__cases)).
% 39.89/10.12 thf(557,plain,((! [A:(produc1016592119n_game > $o),B:produc1016592119n_game]: ((! [C:option_game,D:option_game]: (A @ (produc1111617711n_game @ C @ D))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 39.89/10.12 thf(111,axiom,((! [A:produc1078154247n_game,B:produc1078154247n_game]: (((produc893821739n_game @ A) = (produc893821739n_game @ B)) => (((produc293487213n_game @ A) = (produc293487213n_game @ B)) => (A = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_204_prod__eqI)).
% 39.89/10.12 thf(690,plain,((! [A:produc1078154247n_game,B:produc1078154247n_game]: (((produc893821739n_game @ A) = (produc893821739n_game @ B)) => (((produc293487213n_game @ A) = (produc293487213n_game @ B)) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 39.89/10.12 thf(99,axiom,((! [A:set_variable,B:set_variable]: ((A = B) => (ord_le282106107riable @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_92_equalityD2)).
% 39.89/10.12 thf(640,plain,((! [A:set_variable,B:set_variable]: ((A = B) => (ord_le282106107riable @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 39.89/10.12 thf(212,axiom,(((produc293487213n_game @ (uSubst516392814stappp @ sigma @ ua @ (compose @ alpha @ beta))) != none_game)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4_Compose_Oprems)).
% 39.89/10.12 thf(1025,plain,((~ ((produc293487213n_game @ (uSubst516392814stappp @ sigma @ ua @ (compose @ alpha @ beta))) = none_game))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 39.89/10.12 thf(252,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ (sup_sup_set_variable @ A @ B) @ C) = ((ord_le282106107riable @ A @ C) & (ord_le282106107riable @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_23_sup_Obounded__iff)).
% 39.89/10.12 thf(1156,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ (sup_sup_set_variable @ A @ B) @ C) = ((ord_le282106107riable @ A @ C) & (ord_le282106107riable @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[252])).
% 39.89/10.12 thf(117,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ B @ C) => (ord_le282106107riable @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_221_order_Otrans)).
% 39.89/10.12 thf(707,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ B @ C) => (ord_le282106107riable @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 39.89/10.12 thf(170,axiom,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ B @ A) => (A = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_219_antisym)).
% 39.89/10.12 thf(887,plain,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 39.89/10.12 thf(187,axiom,((sup_sup_set_variable = (^ [A:set_variable,B:set_variable]: (collect_variable @ (^ [C:variable]: ((member_variable @ C @ A) | (member_variable @ C @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_306_Un__def)).
% 39.89/10.12 thf(954,plain,(((sup_sup_set_variable) = (^ [A:set_variable,B:set_variable]: (collect_variable @ (^ [C:variable]: ((member_variable @ C @ A) | (member_variable @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 39.89/10.12 thf(124,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ C @ B) => (ord_le282106107riable @ (sup_sup_set_variable @ A @ C) @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_180_sup__least)).
% 39.89/10.12 thf(739,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ C @ B) => (ord_le282106107riable @ (sup_sup_set_variable @ A @ C) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 39.89/10.12 thf(33,axiom,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: (((^ [C:option_game,D:option_game]: (member191809696n_game @ (produc1111617711n_game @ C @ D) @ A)) = (^ [C:option_game,D:option_game]: (member191809696n_game @ (produc1111617711n_game @ C @ D) @ B))) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_317_pred__equals__eq2)).
% 39.89/10.12 thf(409,plain,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: (((^ [C:option_game,D:option_game]: (member191809696n_game @ (produc1111617711n_game @ C @ D) @ A)) = (^ [C:option_game,D:option_game]: (member191809696n_game @ (produc1111617711n_game @ C @ D) @ B))) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 39.89/10.12 thf(201,axiom,((! [A:(variable > $o),B:(variable > $o)]: ((collect_variable @ (^ [C:variable]: ((A @ C) | (B @ C)))) = (sup_sup_set_variable @ (collect_variable @ A) @ (collect_variable @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_308_Collect__disj__eq)).
% 39.89/10.12 thf(993,plain,((! [A:(variable > $o),B:(variable > $o)]: ((collect_variable @ (^ [C:variable]: ((A @ C) | (B @ C)))) = (sup_sup_set_variable @ (collect_variable @ (A)) @ (collect_variable @ (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 39.89/10.12 thf(140,axiom,((sup_sup_set_variable = (^ [A:set_variable,B:set_variable]: (sup_sup_set_variable @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_131_sup_Ocommute)).
% 39.89/10.12 thf(791,plain,(((sup_sup_set_variable) = (^ [A:set_variable,B:set_variable]: (sup_sup_set_variable @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 39.89/10.12 thf(44,axiom,((! [A:(variable > $o),B:(variable > $o),C:(variable > $o)]: ((ord_le1407353162able_o @ (sup_sup_variable_o @ A @ B) @ C) = ((ord_le1407353162able_o @ A @ C) & (ord_le1407353162able_o @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_12_le__sup__iff)).
% 39.89/10.12 thf(441,plain,((! [A:(variable > $o),B:(variable > $o),C:(variable > $o)]: ((ord_le1407353162able_o @ (sup_sup_variable_o @ A @ B) @ (C)) = ((ord_le1407353162able_o @ (A) @ (C)) & (ord_le1407353162able_o @ (B) @ (C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 39.89/10.12 thf(217,axiom,((! [A:(set_variable > (option_game > $o)),B:set_variable,C:option_game,D:produc1078154247n_game]: ((A @ B @ C) => ((D = (produc1149443391n_game @ B @ C)) => (A @ (produc893821739n_game @ D) @ (produc293487213n_game @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_285_BNF__Greatest__Fixpoint_Osubst__Pair)).
% 39.89/10.12 thf(1038,plain,((! [A:(set_variable > (option_game > $o)),B:set_variable,C:option_game,D:produc1078154247n_game]: ((A @ B @ C) => ((D = (produc1149443391n_game @ B @ C)) => (A @ (produc893821739n_game @ D) @ (produc293487213n_game @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[217])).
% 39.89/10.12 thf(50,axiom,((! [A:option_game]: ((A != none_game) = (? [B:game]: (A = (some_game @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_344_undefg__equiv)).
% 39.89/10.12 thf(463,plain,((! [A:option_game]: ((~ (A = none_game)) = (? [B:game]: (A = (some_game @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 39.89/10.12 thf(186,axiom,((! [A:produc1418842292n_game,B:set_variable,C:game,D:game]: ((uSubst516392814stappp @ A @ B @ (choice @ C @ D)) = (produc1149443391n_game @ (sup_sup_set_variable @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ D))) @ (uSubst1484167963hoiceo @ (produc293487213n_game @ (uSubst516392814stappp @ A @ B @ C)) @ (produc293487213n_game @ (uSubst516392814stappp @ A @ B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_236_usubstappp__choice)).
% 39.89/10.12 thf(951,plain,((! [A:produc1418842292n_game,B:set_variable,C:game,D:game]: ((uSubst516392814stappp @ A @ B @ (choice @ C @ D)) = (produc1149443391n_game @ (sup_sup_set_variable @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ D))) @ (uSubst1484167963hoiceo @ (produc293487213n_game @ (uSubst516392814stappp @ A @ B @ C)) @ (produc293487213n_game @ (uSubst516392814stappp @ A @ B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 39.89/10.12 thf(87,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((sup_sup_set_variable @ (sup_sup_set_variable @ A @ B) @ C) = (sup_sup_set_variable @ A @ (sup_sup_set_variable @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_148_inf__sup__aci_I6_J)).
% 39.89/10.12 thf(600,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((sup_sup_set_variable @ (sup_sup_set_variable @ A @ B) @ C) = (sup_sup_set_variable @ A @ (sup_sup_set_variable @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 39.89/10.12 thf(221,axiom,((! [A:set_variable]: ((sup_sup_set_variable @ A @ A) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_155_Un__absorb)).
% 39.89/10.12 thf(1052,plain,((! [A:set_variable]: ((sup_sup_set_variable @ A @ A) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 39.89/10.12 thf(164,axiom,((! [A:set_variable,B:(set_variable > set_variable),C:set_variable,D:set_variable]: ((ord_le282106107riable @ A @ (B @ C)) => ((ord_le282106107riable @ C @ D) => ((! [E:set_variable,F:set_variable]: ((ord_le282106107riable @ E @ F) => (ord_le282106107riable @ (B @ E) @ (B @ F)))) => (ord_le282106107riable @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_214_order__subst1)).
% 39.89/10.12 thf(864,plain,((! [A:set_variable,B:(set_variable > set_variable),C:set_variable,D:set_variable]: ((ord_le282106107riable @ A @ (B @ C)) => ((ord_le282106107riable @ C @ D) => ((! [E:set_variable,F:set_variable]: ((ord_le282106107riable @ E @ F) => (ord_le282106107riable @ (B @ E) @ (B @ F)))) => (ord_le282106107riable @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 39.89/10.12 thf(196,axiom,((! [A:set_variable]: (((produc293487213n_game @ (uSubst516392814stappp @ sigma @ A @ beta)) != none_game) => (ord_le282106107riable @ (sup_sup_set_variable @ A @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ A @ beta))))) @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ A @ beta)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_7_Compose_OIH_I2_J)).
% 39.89/10.12 thf(978,plain,((! [A:set_variable]: ((~ ((produc293487213n_game @ (uSubst516392814stappp @ sigma @ A @ beta)) = none_game)) => (ord_le282106107riable @ (sup_sup_set_variable @ A @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ A @ beta))))) @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ A @ beta)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 39.89/10.12 thf(90,axiom,((! [A:produc1078154247n_game,B:set_variable,C:option_game]: ((A = (produc1149443391n_game @ B @ C)) => ((produc293487213n_game @ A) = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_292_sndI)).
% 39.89/10.12 thf(612,plain,((! [A:produc1078154247n_game,B:set_variable,C:option_game]: ((A = (produc1149443391n_game @ B @ C)) => ((produc293487213n_game @ A) = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 39.89/10.12 thf(60,axiom,((! [A:(option_game > $o),B:option_game]: ((! [C:game]: (A @ (some_game @ C))) => ((A @ none_game) => (A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_345_Loopo_Oinduct)).
% 39.89/10.12 thf(497,plain,((! [A:(option_game > $o),B:option_game]: ((! [C:game]: (A @ (some_game @ C))) => ((A @ none_game) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 39.89/10.12 thf(163,axiom,((! [A:set_variable,B:set_variable,C:set_variable]: ((A = B) => ((ord_le282106107riable @ B @ C) => (ord_le282106107riable @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_224_ord__eq__le__trans)).
% 39.89/10.12 thf(859,plain,((! [A:set_variable,B:set_variable,C:set_variable]: ((A = B) => ((ord_le282106107riable @ B @ C) => (ord_le282106107riable @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 39.89/10.12 thf(68,axiom,((! [A:game,B:game,C:game]: ((choice @ A @ B) != (loop @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_210_game_Odistinct_I39_J)).
% 39.89/10.12 thf(539,plain,((! [A:game,B:game,C:game]: ~ ((choice @ A @ B) = (loop @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 39.89/10.12 thf(56,axiom,((! [A:option_game,B:option_game]: (((uSubst1484167963hoiceo @ A @ B) = none_game) = ((A = none_game) | (B = none_game))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_282_Choiceo__undef)).
% 39.89/10.12 thf(482,plain,((! [A:option_game,B:option_game]: (((uSubst1484167963hoiceo @ A @ B) = none_game) = ((A = none_game) | (B = none_game))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 39.89/10.12 thf(81,axiom,((! [A:set_variable]: ((sup_sup_set_variable @ A @ A) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_46_sup__idem)).
% 39.89/10.12 thf(581,plain,((! [A:set_variable]: ((sup_sup_set_variable @ A @ A) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 39.89/10.12 thf(240,axiom,((! [A:option_game]: ((A != none_game) => ((some_game @ (the_game @ A)) = A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_332_option_Ocollapse)).
% 39.89/10.12 thf(1126,plain,((! [A:option_game]: ((~ (A = none_game)) => ((some_game @ (the_game @ A)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 39.89/10.12 thf(207,axiom,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((sup_sup_set_variable @ B @ A) = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_173_sup__absorb1)).
% 39.89/10.12 thf(1010,plain,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((sup_sup_set_variable @ B @ A) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 39.89/10.12 thf(114,axiom,((! [A:produc1418842292n_game,B:set_variable,C:game,D:game]: ((uSubst516392814stappp @ A @ B @ (choice @ C @ D)) = (produc1149443391n_game @ (sup_sup_set_variable @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ D))) @ (uSubst1484167963hoiceo @ (produc293487213n_game @ (uSubst516392814stappp @ A @ B @ C)) @ (produc293487213n_game @ (uSubst516392814stappp @ A @ B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_303_usubstappp_Osimps_I4_J)).
% 39.89/10.12 thf(699,plain,((! [A:produc1418842292n_game,B:set_variable,C:game,D:game]: ((uSubst516392814stappp @ A @ B @ (choice @ C @ D)) = (produc1149443391n_game @ (sup_sup_set_variable @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ D))) @ (uSubst1484167963hoiceo @ (produc293487213n_game @ (uSubst516392814stappp @ A @ B @ C)) @ (produc293487213n_game @ (uSubst516392814stappp @ A @ B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 39.89/10.12 thf(127,axiom,((! [A:produc1418842292n_game,B:set_variable,C:game,D:game]: ((uSubst516392814stappp @ A @ B @ (compose @ C @ D)) = (produc1149443391n_game @ (produc893821739n_game @ (uSubst516392814stappp @ A @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ D)) @ (uSubst532817840mposeo @ (produc293487213n_game @ (uSubst516392814stappp @ A @ B @ C)) @ (produc293487213n_game @ (uSubst516392814stappp @ A @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_283_usubstappp__compose)).
% 39.89/10.12 thf(748,plain,((! [A:produc1418842292n_game,B:set_variable,C:game,D:game]: ((uSubst516392814stappp @ A @ B @ (compose @ C @ D)) = (produc1149443391n_game @ (produc893821739n_game @ (uSubst516392814stappp @ A @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ D)) @ (uSubst532817840mposeo @ (produc293487213n_game @ (uSubst516392814stappp @ A @ B @ C)) @ (produc293487213n_game @ (uSubst516392814stappp @ A @ (produc893821739n_game @ (uSubst516392814stappp @ A @ B @ C)) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 39.89/10.12 thf(17,axiom,((! [A:(produc1016592119n_game > $o),B:produc1016592119n_game]: ((! [C:option_game,D:option_game]: (A @ (produc1111617711n_game @ C @ D))) => (A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_249_old_Oprod_Oinducts)).
% 39.89/10.12 thf(304,plain,((! [A:(produc1016592119n_game > $o),B:produc1016592119n_game]: ((! [C:option_game,D:option_game]: (A @ (produc1111617711n_game @ C @ D))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 39.89/10.12 thf(225,axiom,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((sup_sup_set_variable @ B @ A) = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_175_sup_Oabsorb1)).
% 39.89/10.12 thf(1062,plain,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((sup_sup_set_variable @ B @ A) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[225])).
% 39.89/10.12 thf(3,axiom,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ((A = B) => (ord_le1780499447n_game @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_93_equalityD1)).
% 39.89/10.12 thf(258,plain,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ((A = B) => (ord_le1780499447n_game @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 39.89/10.12 thf(36,axiom,((! [A:(variable > $o),B:(variable > $o),C:(variable > $o)]: ((sup_sup_variable_o @ A @ (sup_sup_variable_o @ B @ C)) = (sup_sup_variable_o @ B @ (sup_sup_variable_o @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_114_sup_Oleft__commute)).
% 39.89/10.12 thf(418,plain,((! [A:(variable > $o),B:(variable > $o),C:(variable > $o)]: ((sup_sup_variable_o @ A @ (sup_sup_variable_o @ B @ C)) = (sup_sup_variable_o @ B @ (sup_sup_variable_o @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 39.89/10.12 thf(190,axiom,((! [A:produc735959047riable]: ((produc893821739n_game @ (produc345397471riable @ A)) = (produc284475501riable @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_232_fst__swap)).
% 39.89/10.12 thf(961,plain,((! [A:produc735959047riable]: ((produc893821739n_game @ (produc345397471riable @ A)) = (produc284475501riable @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 39.89/10.12 thf(147,axiom,((! [A:set_variable,B:set_variable]: (ord_le282106107riable @ A @ (sup_sup_set_variable @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_167_sup_Ocobounded2)).
% 39.89/10.12 thf(813,plain,((! [A:set_variable,B:set_variable]: (ord_le282106107riable @ A @ (sup_sup_set_variable @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 39.89/10.12 thf(14,axiom,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ((A = B) => (~ ((ord_le1780499447n_game @ A @ B) => (~ (ord_le1780499447n_game @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_99_equalityE)).
% 39.89/10.12 thf(290,plain,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game]: ((A = B) => (~ ((ord_le1780499447n_game @ A @ B) => (~ (ord_le1780499447n_game @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 39.89/10.12 thf(104,axiom,((bNF_Ca1986151756riable = (^ [A:set_Pr1625152599n_game,B:(option_game > set_variable)]: ! [C:option_game,D:option_game]: ((member191809696n_game @ (produc1111617711n_game @ C @ D) @ A) => (ord_le282106107riable @ (B @ C) @ (B @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_299_relChain__def)).
% 39.89/10.12 thf(667,plain,(((bNF_Ca1986151756riable) = (^ [A:set_Pr1625152599n_game,B:(option_game > set_variable)]: ! [C:option_game,D:option_game]: ((member191809696n_game @ (produc1111617711n_game @ C @ D) @ A) => (ord_le282106107riable @ (B @ C) @ (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 39.89/10.12 thf(109,axiom,((! [A:set_variable,B:set_variable,C:(variable > $o)]: ((! [D:variable]: ((member_variable @ D @ (sup_sup_set_variable @ A @ B)) => (C @ D))) = (! [D:variable]: ((member_variable @ D @ A) => (C @ D)) & ! [D:variable]: ((member_variable @ D @ B) => (C @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_157_ball__Un)).
% 39.89/10.12 thf(684,plain,((! [A:set_variable,B:set_variable,C:(variable > $o)]: ((! [D:variable]: ((member_variable @ D @ (sup_sup_set_variable @ A @ B)) => (C @ D))) = (! [D:variable]: ((member_variable @ D @ A) => (C @ D)) & ! [D:variable]: ((member_variable @ D @ B) => (C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 39.89/10.12 thf(229,axiom,((! [A:variable,B:set_variable,C:set_variable]: ((~ (member_variable @ A @ (sup_sup_set_variable @ B @ C))) = (~ (member_variable @ A @ B) & ~ (member_variable @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_151_not__union__or)).
% 39.89/10.12 thf(1077,plain,((! [A:variable,B:set_variable,C:set_variable]: ((~ (member_variable @ A @ (sup_sup_set_variable @ B @ C))) = (~ (member_variable @ A @ B) & ~ (member_variable @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 39.89/10.12 thf(55,axiom,((! [A:produc1016592119n_game]: ~ (! [B:option_game,C:option_game]: (A != (produc1111617711n_game @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_251_old_Oprod_Oexhaust)).
% 39.89/10.12 thf(478,plain,((! [A:produc1016592119n_game]: ~ (! [B:option_game,C:option_game]: ~ (A = (produc1111617711n_game @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 39.89/10.12 thf(41,axiom,((! [A:game,B:game]: ((uSubst1484167963hoiceo @ (some_game @ A) @ (some_game @ B)) = (some_game @ (choice @ A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_348_Choiceo_Osimps_I1_J)).
% 39.89/10.12 thf(432,plain,((! [A:game,B:game]: ((uSubst1484167963hoiceo @ (some_game @ A) @ (some_game @ B)) = (some_game @ (choice @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 39.89/10.12 thf(192,axiom,((! [A:set_variable,B:set_variable]: (ord_le282106107riable @ A @ (sup_sup_set_variable @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_190_inf__sup__ord_I4_J)).
% 39.89/10.12 thf(967,plain,((! [A:set_variable,B:set_variable]: (ord_le282106107riable @ A @ (sup_sup_set_variable @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 39.89/10.12 thf(4,axiom,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game,C:produc1016592119n_game]: ((ord_le1780499447n_game @ A @ B) => ((member191809696n_game @ C @ A) => (member191809696n_game @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_105_in__mono)).
% 39.89/10.12 thf(262,plain,((! [A:set_Pr1625152599n_game,B:set_Pr1625152599n_game,C:produc1016592119n_game]: ((ord_le1780499447n_game @ A @ B) => ((member191809696n_game @ C @ A) => (member191809696n_game @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 39.89/10.12 thf(161,axiom,((! [A:set_variable,B:set_variable]: (ord_le282106107riable @ A @ (sup_sup_set_variable @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_185_sup__ge2)).
% 39.89/10.12 thf(854,plain,((! [A:set_variable,B:set_variable]: (ord_le282106107riable @ A @ (sup_sup_set_variable @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 39.89/10.12 thf(7,axiom,((! [A:set_Pr1625152599n_game]: (ord_le1780499447n_game @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_84_subset__refl)).
% 39.89/10.12 thf(273,plain,((! [A:set_Pr1625152599n_game]: (ord_le1780499447n_game @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 39.89/10.12 thf(88,axiom,((! [A:set_variable,B:set_variable]: ((sup_sup_set_variable @ A @ (sup_sup_set_variable @ A @ B)) = (sup_sup_set_variable @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_64_sup__left__idem)).
% 39.89/10.12 thf(603,plain,((! [A:set_variable,B:set_variable]: ((sup_sup_set_variable @ A @ (sup_sup_set_variable @ A @ B)) = (sup_sup_set_variable @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 39.89/10.12 thf(203,axiom,((! [A:set_variable,B:set_variable]: (ord_le282106107riable @ A @ (sup_sup_set_variable @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_196_Un__upper1)).
% 39.89/10.12 thf(999,plain,((! [A:set_variable,B:set_variable]: (ord_le282106107riable @ A @ (sup_sup_set_variable @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 39.89/10.12 thf(92,axiom,((! [A:set_variable,B:set_variable,C:set_variable,D:set_variable]: ((A = (sup_sup_set_variable @ B @ C)) => ((sup_sup_set_variable @ D @ A) = (sup_sup_set_variable @ B @ (sup_sup_set_variable @ D @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_145_boolean__algebra__cancel_Osup2)).
% 39.89/10.12 thf(620,plain,((! [A:set_variable,B:set_variable,C:set_variable,D:set_variable]: ((A = (sup_sup_set_variable @ B @ C)) => ((sup_sup_set_variable @ D @ A) = (sup_sup_set_variable @ B @ (sup_sup_set_variable @ D @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 39.89/10.12 thf(62,axiom,((sup_sup_variable_o = (^ [A:(variable > $o),B:(variable > $o)]: (sup_sup_variable_o @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_126_sup_Ocommute)).
% 39.89/10.12 thf(506,plain,(((sup_sup_variable_o) = (^ [A:(variable > $o),B:(variable > $o)]: (sup_sup_variable_o @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 39.89/10.12 thf(145,axiom,((! [A:option_game]: ((A != none_game) => (A = (some_game @ (the_game @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_334_option_Oexhaust__sel)).
% 39.89/10.12 thf(807,plain,((! [A:option_game]: ((~ (A = none_game)) => (A = (some_game @ (the_game @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 39.89/10.12 thf(30,axiom,(((uSubst23177304_Loopo @ none_game) = none_game)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_293_Loopo_Osimps_I2_J)).
% 39.89/10.12 thf(400,plain,(((uSubst23177304_Loopo @ none_game) = none_game)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 39.89/10.12 thf(226,axiom,((! [A:set_variable,B:set_variable]: ((A = B) => (ord_le282106107riable @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_95_equalityD1)).
% 39.89/10.12 thf(1065,plain,((! [A:set_variable,B:set_variable]: ((A = B) => (ord_le282106107riable @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 39.89/10.12 thf(113,axiom,((! [A:game,B:game,C:game,D:game]: (((compose @ A @ B) = (compose @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_25_game_Oinject_I5_J)).
% 39.89/10.12 thf(696,plain,((! [A:game,B:game,C:game,D:game]: (((compose @ A @ B) = (compose @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 39.89/10.12 thf(256,axiom,((! [A:game,B:game]: (ord_le282106107riable @ (static_BVG @ (choice @ A @ B)) @ (sup_sup_set_variable @ (static_BVG @ A) @ (static_BVG @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_206_BVG__choice)).
% 39.89/10.12 thf(1165,plain,((! [A:game,B:game]: (ord_le282106107riable @ (static_BVG @ (choice @ A @ B)) @ (sup_sup_set_variable @ (static_BVG @ A) @ (static_BVG @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[256])).
% 39.89/10.12 thf(35,axiom,((! [A:option_game]: (((uSubst23177304_Loopo @ A) = none_game) = (A = none_game)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_294_Loopo__undef)).
% 39.89/10.12 thf(415,plain,((! [A:option_game]: (((uSubst23177304_Loopo @ A) = none_game) = (A = none_game)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 39.89/10.12 thf(241,axiom,((! [A:variable,B:set_variable,C:set_variable]: ((member_variable @ A @ B) => (member_variable @ A @ (sup_sup_set_variable @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_159_UnI2)).
% 39.89/10.12 thf(1129,plain,((! [A:variable,B:set_variable,C:set_variable]: ((member_variable @ A @ B) => (member_variable @ A @ (sup_sup_set_variable @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 39.89/10.12 thf(79,axiom,((! [A:option_game,B:set_variable]: ((produc345397471riable @ (produc1140431679riable @ A @ B)) = (produc1149443391n_game @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_243_swap__simp)).
% 39.89/10.12 thf(575,plain,((! [A:option_game,B:set_variable]: ((produc345397471riable @ (produc1140431679riable @ A @ B)) = (produc1149443391n_game @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 39.89/10.12 thf(210,axiom,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((sup_sup_set_variable @ A @ B) = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_172_sup__absorb2)).
% 39.89/10.12 thf(1019,plain,((! [A:set_variable,B:set_variable]: ((ord_le282106107riable @ A @ B) => ((sup_sup_set_variable @ A @ B) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 39.89/10.12 thf(100,axiom,((! [A:(set_variable > $o),B:set_variable,C:(set_variable > $o)]: ((A @ B) => ((! [D:set_variable]: ((A @ D) => (ord_le282106107riable @ D @ B))) => ((! [D:set_variable]: ((A @ D) => ((! [E:set_variable]: ((A @ E) => (ord_le282106107riable @ E @ D))) => (C @ D)))) => (C @ (order_272405634riable @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_237_GreatestI2__order)).
% 39.89/10.12 thf(644,plain,((! [A:(set_variable > $o),B:set_variable,C:(set_variable > $o)]: ((A @ B) => ((! [D:set_variable]: ((A @ D) => (ord_le282106107riable @ D @ B))) => ((! [D:set_variable]: ((A @ D) => ((! [E:set_variable]: ((A @ E) => (ord_le282106107riable @ E @ D))) => (C @ D)))) => (C @ (order_272405634riable @ (A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 39.89/10.12 thf(120,axiom,((! [A:(set_variable > $o),B:set_variable]: ((A @ B) => ((! [C:set_variable]: ((A @ C) => (ord_le282106107riable @ C @ B))) => ((order_272405634riable @ A) = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_238_Greatest__equality)).
% 39.89/10.12 thf(723,plain,((! [A:(set_variable > $o),B:set_variable]: ((A @ B) => ((! [C:set_variable]: ((A @ C) => (ord_le282106107riable @ C @ B))) => ((order_272405634riable @ (A)) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 39.89/10.12 thf(205,axiom,((! [A:set_variable,B:set_variable,C:set_variable,D:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ C @ D) => (ord_le282106107riable @ (sup_sup_set_variable @ A @ C) @ (sup_sup_set_variable @ B @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_181_sup__mono)).
% 39.89/10.12 thf(1004,plain,((! [A:set_variable,B:set_variable,C:set_variable,D:set_variable]: ((ord_le282106107riable @ A @ B) => ((ord_le282106107riable @ C @ D) => (ord_le282106107riable @ (sup_sup_set_variable @ A @ C) @ (sup_sup_set_variable @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 39.89/10.12 thf(250,axiom,((ord_le282106107riable @ (sup_sup_set_variable @ (sup_sup_set_variable @ ua @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha))))) @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)) @ beta))))) @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)) @ beta)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0__092_060open_062U_A_092_060union_062_ABVG_A_Ithe_A_Isnd_A_Iusubstappp_A_092_060sigma_062_AU_A_092_060alpha_062_J_J_J_A_092_060union_062_ABVG_A_Ithe_A_Isnd_A_Iusubstappp_A_092_060sigma_062_A_Ifst_A_Iusubstappp_A_092_060sigma_062_AU_A_092_060alpha_062_J_J_A_092_060beta_062_J_J_J_A_092_060subseteq_062_Afst_A_Iusubstappp_A_092_060sigma_062_A_Ifst_A_Iusubstappp_A_092_060sigma_062_AU_A_092_060alpha_062_J_J_A_092_060beta_062_J_092_060close_062)).
% 39.89/10.12 thf(1152,plain,((ord_le282106107riable @ (sup_sup_set_variable @ (sup_sup_set_variable @ ua @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha))))) @ (static_BVG @ (the_game @ (produc293487213n_game @ (uSubst516392814stappp @ sigma @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)) @ beta))))) @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ (produc893821739n_game @ (uSubst516392814stappp @ sigma @ ua @ alpha)) @ beta)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 39.89/10.12 thf(39,axiom,((! [A:option_game]: ((A != none_game) = (? [B:game]: (A = (some_game @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_331_not__None__eq)).
% 39.89/10.12 thf(427,plain,((! [A:option_game]: ((~ (A = none_game)) = (? [B:game]: (A = (some_game @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 39.89/10.12 thf(52,axiom,((! [A:game]: ((uSubst23177304_Loopo @ (some_game @ A)) = (some_game @ (loop @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_347_Loopo_Osimps_I1_J)).
% 39.89/10.12 thf(469,plain,((! [A:game]: ((uSubst23177304_Loopo @ (some_game @ A)) = (some_game @ (loop @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 39.89/10.12 thf(18,axiom,((! [A:game]: (none_game != (some_game @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_341_option_Odistinct_I1_J)).
% 39.89/10.12 thf(309,plain,((! [A:game]: ~ (none_game = (some_game @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 39.89/10.12 thf(69,axiom,((! [A:game,B:game]: (((some_game @ A) = (some_game @ B)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_329_option_Oinject)).
% 39.89/10.12 thf(543,plain,((! [A:game,B:game]: (((some_game @ A) = (some_game @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 39.89/10.12 thf(134,axiom,((! [A:game,B:game]: (ord_le282106107riable @ (static_BVG @ (compose @ A @ B)) @ (sup_sup_set_variable @ (static_BVG @ A) @ (static_BVG @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_24_BVG__compose)).
% 39.89/10.12 thf(775,plain,((! [A:game,B:game]: (ord_le282106107riable @ (static_BVG @ (compose @ A @ B)) @ (sup_sup_set_variable @ (static_BVG @ A) @ (static_BVG @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 39.89/10.12 thf(194,axiom,((ord_le282106107riable = (^ [A:set_variable,B:set_variable]: ((sup_sup_set_variable @ A @ B) = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_179_le__iff__sup)).
% 39.89/10.12 thf(972,plain,(((ord_le282106107riable) = (^ [A:set_variable,B:set_variable]: ((sup_sup_set_variable @ A @ B) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 39.89/10.12 thf(47,axiom,((! [A:option_game]: ((uSubst1484167963hoiceo @ A @ none_game) = none_game))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_281_Choiceo_Osimps_I2_J)).
% 39.89/10.12 thf(454,plain,((! [A:option_game]: ((uSubst1484167963hoiceo @ A @ none_game) = none_game))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 39.89/10.12 thf(227,axiom,((ord_le282106107riable = (^ [A:set_variable,B:set_variable]: (ord_le1407353162able_o @ (^ [C:variable]: (member_variable @ C @ A)) @ (^ [C:variable]: (member_variable @ C @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_304_less__eq__set__def)).
% 39.89/10.12 thf(1069,plain,(((ord_le282106107riable) = (^ [A:set_variable,B:set_variable]: (ord_le1407353162able_o @ (^ [C:variable]: (member_variable @ C @ A)) @ (^ [C:variable]: (member_variable @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 39.89/10.12 thf(3901,plain,(($false)),inference(e,[status(thm)],[892,1036,365,1105,347,846,518,777,628,1031,873,1142,269,597,878,511,1137,1164,472,913,829,898,1001,841,1046,288,565,257,389,1055,570,785,802,357,460,587,838,917,702,751,1059,1132,1147,421,1115,448,817,902,969,606,1013,284,591,1109,475,924,485,834,981,734,956,660,988,397,687,265,849,678,810,546,793,1153,761,798,1057,302,820,424,693,815,275,788,625,435,665,1159,493,551,710,974,948,1121,869,742,578,783,1118,884,1028,933,669,1016,554,753,1099,515,457,984,721,503,633,508,921,1035,1071,773,298,430,856,745,444,375,1135,412,584,562,1007,402,732,843,286,875,958,281,1139,936,572,313,466,1090,804,704,672,764,831,362,1144,737,1043,616,900,406,990,996,890,1080,631,345,594,1162,895,769,1022,1112,1149,964,626,915,521,827,636,278,780,394,1102,438,939,342,823,1049,490,675,663,548,557,690,640,1025,1156,707,887,954,739,409,993,791,441,1038,463,951,600,1052,864,978,612,497,859,539,482,581,1126,1010,699,748,304,1062,258,418,961,813,290,667,684,1077,478,432,967,262,854,273,603,999,620,506,807,400,1065,696,1165,415,1129,575,1019,644,723,1004,1152,427,469,309,543,775,972,454,1069])).
% 39.89/10.12 % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 39.89/10.12 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------