Leo-III---1.8.0.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Leo-III---1.8.0
% Problem  : ITP200^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39

% Computer : n006.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:09 AM UTC 2026

% Result   : Theorem 276.13s 240.28s
% Output   : Refutation 277.20s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : ITP200^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.07  % Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.11/0.20  % Computer : n006.cluster.edu
% 0.11/0.20  % Model    : x86_64 x86_64
% 0.11/0.20  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.20  % Memory   : 8046.5625MB
% 0.11/0.20  % OS       : Linux 6.8.0-71-generic
% 0.11/0.21  % CPULimit : 300
% 0.11/0.21  % WCLimit  : 300
% 0.11/0.21  % DateTime : Tue Sep 29 20:10:39 UTC 2026
% 0.11/0.21  % CPUTime  : 
% 0.11/0.21  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.90/0.78  % [INFO] 	 Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ... 
% 2.45/1.22  % [INFO] 	 Parsing done (437ms). 
% 2.45/1.23  % [INFO] 	 Running in sequential loop mode. 
% 3.91/1.65  % [INFO] 	 eprover registered as external prover. 
% 3.91/1.65  % [INFO] 	 Scanning for conjecture ... 
% 4.38/1.83  % [INFO] 	 Found a conjecture (or negated_conjecture) and 278 axioms. Running axiom selection ... 
% 4.64/1.99  % [INFO] 	 Axiom selection finished. Selected 239 axioms (removed 39 axioms). 
% 6.03/2.33  % [INFO] 	 Problem is higher-order (TPTP THF). 
% 6.03/2.37  % [INFO] 	 Type checking passed. 
% 6.03/2.37  % [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 ... 
% 276.13/240.27  % External prover 'e' found a proof!
% 276.13/240.28  % [INFO] 	 Killing All external provers ... 
% 276.13/240.28  % Time passed: 239926ms (effective reasoning time: 239036ms)
% 276.13/240.28  % 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)>
% 276.13/240.28  % Axioms used in derivation (239): fact_69_equalityD2, fact_100_option_Oinducts, fact_110_Differentialo_Oelims, fact_128_Testo_Oinduct, fact_132_accp__subset__induct, fact_175_ODEo_Ocases, fact_134_usubstappf__geq, fact_163_pred__subset__eq2, fact_24_fml_Oinject_I2_J, fact_122_Geqo_Osimps_I1_J, fact_185_in__lex__prod, fact_230_Assigno_Osimps_I2_J, fact_174_disjE__realizer2, fact_66_Collect__mono, fact_76_Uvariation__refl, fact_195_usubstappt_Osimps_I2_J, fact_143_option_Oexpand, fact_127_undeff__equiv, fact_246_UNIV__witness, fact_119_Geqo_Oelims, fact_194_trm_Odistinct_I1_J, fact_187_trm_Oinject_I1_J, fact_93_predicate1D, fact_206_trm_Odistinct_I23_J, fact_213_trm_Oinduct, fact_131_accp__subset, fact_251_top__empty__eq2, fact_208_trm_Odistinct_I27_J, fact_173_Pluso_Opelims, fact_10_Differentialo__undef, fact_252_top__empty__eq, fact_205_trm_Odistinct_I15_J, fact_210_trm_Odistinct_I35_J, fact_113_Timeso_Osimps_I3_J, fact_211_trm_Odistinct_I33_J, fact_193_trm_Odistinct_I11_J, fact_248_ODEo_Oelims, fact_21_Geqo__undef, fact_214_trm_Oexhaust, fact_245_UNIV__eq__I, fact_75_Uvariation__sym__rel, fact_90_predicate1I, fact_189_trm_Odistinct_I19_J, fact_16_usubstappf__antimon, fact_4_usubstappt__det, fact_129_Testo_Ocases, fact_184_usubstappt_Opsimps_I2_J, fact_138_rev__predicate2D, fact_74_in__mono, fact_87_usubstappt_Osimps_I7_J, fact_50_le__cases, fact_108_undeft__equiv, fact_105_Differentialo_Ocases, fact_159_ssubst__Pair__rhs, fact_101_option_Oexhaust, fact_126_Existso_Oinduct, fact_67_subset__refl, tcon_HOL_Obool___Orderings_Olinorder, fact_8_usubstappt__antimon, fact_83_prop__restrict, fact_232_Assigno_Opelims, fact_3_undeft__None, fact_197_usubstappt_Ocases, fact_169_option_Ocase__eq__if, fact_22_trm_Oinject_I6_J, fact_158_subrelI, fact_172_Timeso_Opelims, fact_176_Assigno_Ocases, fact_191_trm_Odistinct_I7_J, fact_137_predicate2D, fact_207_trm_Odistinct_I29_J, fact_231_Assigno_Oelims, fact_28_trm_Odistinct_I37_J, fact_200_trm_Oinject_I4_J, fact_115_Pluso_Osimps_I1_J, fact_168_case__optionE, fact_237_ODEo__undef, fact_190_trm_Odistinct_I21_J, fact_79_pred__subset__eq, fact_19_usubstappt_Osimps_I6_J, fact_150_accp_Oinducts, fact_228_Assigno__undef, fact_52_linear, fact_235_Assigno_Osimps_I1_J, fact_171_option_Osplit__sel__asm, fact_146_accp_Ocases, fact_142_Loopo_Ocases, fact_2_Geq_Oprems_I1_J, fact_227_relInvImage__def, fact_202_trm_Odistinct_I3_J, fact_164_option_Osimps_I5_J, fact_203_trm_Odistinct_I5_J, fact_221_game_Oinject_I3_J, fact_32_less__eq__set__def, help_If_1_1_T, fact_160_pred__equals__eq2, fact_14_Timeso__undef, fact_86_Timeso_Oelims, fact_192_trm_Odistinct_I9_J, fact_63_Collect__mono__iff, fact_6_usubstappt__plus__conv, fact_238_top__apply, fact_112_trm_Odistinct_I39_J, fact_140_undefg__equiv, fact_95_Aterm__Some, fact_1_usubstappf__geq__conv, fact_180_usubstappt_Opsimps_I7_J, fact_162_option_Osimps_I4_J, fact_236_relInvImage__UNIV__relImage, fact_116_Timeso_Osimps_I1_J, fact_199_Testo__undef, tcon_Set_Oset___Orderings_Oorder__top_1, fact_92_not__None__eq, fact_182_usubstappt_Opsimps_I5_J, fact_243_top_Oextremum__uniqueI, fact_166_option_Odisc__eq__case_I2_J, fact_167_Timeso_Ocases, fact_17_usubstappf__det, fact_154_eq__subset, tcon_HOL_Obool___Orderings_Otop_9, fact_156_Diamondo_Ocases, fact_26_subsetI, fact_117_usubstappt__differential__conv, fact_15_Geqo_Osimps_I2_J, fact_106_Assigno_Oinduct, fact_196_usubstappt_Osimps_I1_J, fact_70_equalityD1, fact_241_top__greatest, fact_188_trm_Odistinct_I17_J, fact_114_Pluso_Osimps_I3_J, fact_198_Testo_Osimps_I2_J, fact_216_usubstappt_Opsimps_I3_J, fact_23_trm_Oinject_I5_J, fact_65_subset__trans, fact_183_usubstappt_Opsimps_I1_J, fact_157_option_Osplit__sel, fact_250_game_Oinject_I8_J, fact_247_ODEo_Osimps_I2_J, fact_201_trm_Oinject_I3_J, fact_177_Composeo_Ocases, fact_155_Geqo_Opelims, help_If_3_1_T, help_If_2_1_T, fact_0_vaouter, fact_78_Uvariation__def, fact_107_Timeso_Oinduct, fact_234_game_Odistinct_I15_J, fact_148_accp_Ointros, fact_223_Testo_Osimps_I1_J, tcon_fun___Orderings_Otop, fact_25_Uvariation__mon, fact_242_top_Oextremum__unique, fact_30_Uvariation__univ, fact_89_trm_Oinject_I7_J, fact_209_trm_Odistinct_I25_J, fact_81_subset__CollectI, fact_109_ODEo_Oinduct, fact_85_Pluso_Oelims, fact_13_Pluso__undef, fact_133_usubstappf__geqr, fact_149_accp__induct, fact_170_predicate2D__conj, fact_218_usubstappt_Osimps_I3_J, fact_12_Timeso_Osimps_I2_J, fact_48_le__cases3, fact_104_Differentialo_Oinduct, fact_9_Differentialo_Osimps_I2_J, tcon_Set_Oset___Orderings_Otop_4, fact_220_Testo_Oelims, fact_82_Collect__restrict, fact_97_combine__options__cases, fact_253_top__set__def, fact_212_trm_Odistinct_I31_J, fact_94_rev__predicate1D, fact_145_option_Oexhaust__sel, fact_204_trm_Odistinct_I13_J, fact_45_Collect__mem__eq, fact_165_option_Odisc__eq__case_I1_J, fact_27_subset__antisym, tcon_fun___Orderings_Oorder__top, fact_80_subset__Collect__iff, fact_141_Loopo_Oinduct, fact_120_Differentialo_Opelims, fact_152_not__accp__down, fact_222_image2__eqI, fact_125_Diamondo_Oinduct, fact_11_Pluso_Osimps_I2_J, fact_144_option_Osel, fact_233_game_Oinject_I2_J, tcon_HOL_Obool___Orderings_Oorder__top_6, fact_239_UNIV__I, fact_225_relImage__def, fact_186_trm_Oinject_I2_J, fact_229_relInvImage__mono, fact_102_option_OdiscI, fact_217_term__sem_Oinduct, fact_244_UNIV__def, fact_88_option_Oinject, fact_7_usubstappt__times__conv, fact_139_Composeo_Oinduct, fact_181_usubstappt_Opsimps_I6_J, fact_136_option_Ocollapse, fact_103_option_Odistinct_I1_J, fact_151_accp__downward, fact_118_Geqo_Osimps_I3_J, fact_240_subset__UNIV, fact_224_Testo_Opelims, fact_130_Ando_Oinduct, fact_31_Collect__subset, fact_18_usubstappt_Osimps_I5_J, fact_72_equalityE, fact_121_Powp__mono, fact_20_usubstappf_Osimps_I2_J, fact_84_conj__subset__def, fact_71_subset__eq, fact_111_trm_Odistinct_I41_J, fact_161_option_Ocase__distrib, fact_249_ODEo_Opelims, fact_153_accp__induct__rule, fact_178_Existso_Ocases, fact_5_Geq_Oprems_I2_J, fact_36_linorder__wlog, fact_98_split__option__all, fact_215_term__sem_Ocases, fact_99_split__option__ex, fact_179_Ando_Ocases, fact_68_subset__iff, fact_135_predicate2I, fact_147_accp_Osimps, fact_254_game_Odistinct_I35_J, fact_91_not__Some__eq, fact_46_Collect__cong, fact_73_subsetD, fact_64_set__eq__subset, fact_44_mem__Collect__eq, fact_96_Differentialo_Osimps_I1_J, fact_219_image2__def, fact_226_relImage__mono, fact_77_Uvariation__sym
% 276.13/240.28  % No. of inferences in proof: 482
% 276.13/240.28  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 239926 ms resp. 239036 ms w/o parsing
% 277.20/240.55  % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 277.20/240.55  thf(denotational_interp_type, type, denotational_interp: $tType).
% 277.20/240.55  thf(variable_type, type, variable: $tType).
% 277.20/240.55  thf(game_type, type, game: $tType).
% 277.20/240.55  thf(char_type, type, char: $tType).
% 277.20/240.55  thf(trm_type, type, trm: $tType).
% 277.20/240.55  thf(fml_type, type, fml: $tType).
% 277.20/240.55  thf(real_type, type, real: $tType).
% 277.20/240.55  thf(top_decl, type, top: !> [TA: $tType]: $o).
% 277.20/240.55  thf(linorder_decl, type, linorder: !> [TA: $tType]: $o).
% 277.20/240.55  thf(order_top_decl, type, order_top: !> [TA: $tType]: $o).
% 277.20/240.55  thf(bNF_Greatest_image2_decl, type, bNF_Greatest_image2: !> [TA: $tType,TB: $tType,TC: $tType]: ((set @ TC) > ((TC > TB) > ((TC > TA) > (set @ (product_prod @ TB @ TA)))))).
% 277.20/240.55  thf(bNF_Gr1317331620lImage_decl, type, bNF_Gr1317331620lImage: !> [TA: $tType,TB: $tType]: ((set @ (product_prod @ TB @ TB)) > ((TB > TA) > (set @ (product_prod @ TA @ TA))))).
% 277.20/240.55  thf(bNF_Gr2107612801vImage_decl, type, bNF_Gr2107612801vImage: !> [TA: $tType,TB: $tType]: ((set @ TB) > ((set @ (product_prod @ TA @ TA)) > ((TB > TA) > (set @ (product_prod @ TB @ TB)))))).
% 277.20/240.55  thf(denota1419872369iation_decl, type, denota1419872369iation: ((variable > real) > ((variable > real) > ((set @ variable) > $o)))).
% 277.20/240.55  thf(if_decl, type, if: !> [TA: $tType]: ($o > (TA > (TA > TA)))).
% 277.20/240.55  thf(none_decl, type, none: !> [TA: $tType]: (option @ TA)).
% 277.20/240.55  thf(some_decl, type, some: !> [TA: $tType]: (TA > (option @ TA))).
% 277.20/240.55  thf(case_option_decl, type, case_option: !> [TA: $tType,TB: $tType]: (TB > ((TA > TB) > ((option @ TA) > TB)))).
% 277.20/240.55  thf(the_decl, type, the: !> [TA: $tType]: ((option @ TA) > TA)).
% 277.20/240.55  thf(ord_less_eq_decl, type, ord_less_eq: !> [TA: $tType]: (TA > (TA > $o))).
% 277.20/240.55  thf(top_top_decl, type, top_top: !> [TA: $tType]: TA).
% 277.20/240.55  thf(product_Pair_decl, type, product_Pair: !> [TA: $tType,TB: $tType]: (TB > (TA > (product_prod @ TB @ TA)))).
% 277.20/240.55  thf(powp_decl, type, powp: !> [TA: $tType]: ((TA > $o) > ((set @ TA) > $o))).
% 277.20/240.55  thf(collect_decl, type, collect: !> [TA: $tType]: ((TA > $o) > (set @ TA))).
% 277.20/240.55  thf(geq_decl, type, geq: (trm > (trm > fml))).
% 277.20/240.55  thf(assign_decl, type, assign: (variable > (trm > game))).
% 277.20/240.55  thf(ode_decl, type, ode: (char > (trm > game))).
% 277.20/240.55  thf(test_decl, type, test: (fml > game)).
% 277.20/240.55  thf(const_decl, type, const: (char > trm)).
% 277.20/240.55  thf(differential_decl, type, differential: (trm > trm)).
% 277.20/240.55  thf(func_decl, type, func: (char > (trm > trm))).
% 277.20/240.55  thf(number_decl, type, number: (real > trm)).
% 277.20/240.55  thf(plus_decl, type, plus: (trm > (trm > trm))).
% 277.20/240.55  thf(times_decl, type, times: (trm > (trm > trm))).
% 277.20/240.55  thf(var_decl, type, var: (variable > trm)).
% 277.20/240.55  thf(uSubst1326326671ssigno_decl, type, uSubst1326326671ssigno: (variable > ((option @ trm) > (option @ game)))).
% 277.20/240.55  thf(uSubst1741596714no_rel_decl, type, uSubst1741596714no_rel: ((product_prod @ variable @ (option @ trm)) > ((product_prod @ variable @ (option @ trm)) > $o))).
% 277.20/240.55  thf(uSubst259074819ntialo_decl, type, uSubst259074819ntialo: ((option @ trm) > (option @ trm))).
% 277.20/240.55  thf(uSubst99643830lo_rel_decl, type, uSubst99643830lo_rel: ((option @ trm) > ((option @ trm) > $o))).
% 277.20/240.55  thf(uSubst1556497037e_Geqo_decl, type, uSubst1556497037e_Geqo: ((option @ trm) > ((option @ trm) > (option @ fml)))).
% 277.20/240.55  thf(uSubst864323244qo_rel_decl, type, uSubst864323244qo_rel: ((product_prod @ (option @ trm) @ (option @ trm)) > ((product_prod @ (option @ trm) @ (option @ trm)) > $o))).
% 277.20/240.55  thf(uSubst1083227664e_ODEo_decl, type, uSubst1083227664e_ODEo: (char > ((option @ trm) > (option @ game)))).
% 277.20/240.55  thf(uSubst2007600873Eo_rel_decl, type, uSubst2007600873Eo_rel: ((product_prod @ char @ (option @ trm)) > ((product_prod @ char @ (option @ trm)) > $o))).
% 277.20/240.55  thf(uSubst1112714340_Pluso_decl, type, uSubst1112714340_Pluso: ((option @ trm) > ((option @ trm) > (option @ trm)))).
% 277.20/240.55  thf(uSubst270600597so_rel_decl, type, uSubst270600597so_rel: ((product_prod @ (option @ trm) @ (option @ trm)) > ((product_prod @ (option @ trm) @ (option @ trm)) > $o))).
% 277.20/240.55  thf(uSubst190403692_Testo_decl, type, uSubst190403692_Testo: ((option @ fml) > (option @ game))).
% 277.20/240.55  thf(uSubst533687181to_rel_decl, type, uSubst533687181to_rel: ((option @ fml) > ((option @ fml) > $o))).
% 277.20/240.55  thf(uSubst277968634Timeso_decl, type, uSubst277968634Timeso: ((option @ trm) > ((option @ trm) > (option @ trm)))).
% 277.20/240.55  thf(uSubst1377811071so_rel_decl, type, uSubst1377811071so_rel: ((product_prod @ (option @ trm) @ (option @ trm)) > ((product_prod @ (option @ trm) @ (option @ trm)) > $o))).
% 277.20/240.55  thf(uSubst1138577137pconst_decl, type, uSubst1138577137pconst: ((product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) > ((set @ variable) > (char > (option @ trm))))).
% 277.20/240.55  thf(uSubst95898978stappf_decl, type, uSubst95898978stappf: ((product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) > ((set @ variable) > (fml > (option @ fml))))).
% 277.20/240.55  thf(uSubst95898992stappt_decl, type, uSubst95898992stappt: ((product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) > ((set @ variable) > (trm > (option @ trm))))).
% 277.20/240.55  thf(uSubst2096773001pt_rel_decl, type, uSubst2096773001pt_rel: ((product_prod @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm)) > ((product_prod @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm)) > $o))).
% 277.20/240.55  thf(accp_decl, type, accp: !> [TA: $tType]: ((TA > (TA > $o)) > (TA > $o))).
% 277.20/240.55  thf(lex_prod_decl, type, lex_prod: !> [TA: $tType,TB: $tType]: ((set @ (product_prod @ TB @ TB)) > ((set @ (product_prod @ TA @ TA)) > (set @ (product_prod @ (product_prod @ TB @ TA) @ (product_prod @ TB @ TA)))))).
% 277.20/240.55  thf(member_decl, type, member: !> [TA: $tType]: (TA > ((set @ TA) > $o))).
% 277.20/240.55  thf(u_decl, type, u: (set @ variable)).
% 277.20/240.55  thf(ua_decl, type, ua: (set @ variable)).
% 277.20/240.55  thf(eta_decl, type, eta: trm).
% 277.20/240.55  thf(nu_decl, type, nu: (variable > real)).
% 277.20/240.55  thf(nu2_decl, type, nu2: (variable > real)).
% 277.20/240.55  thf(omega_decl, type, omega: (variable > real)).
% 277.20/240.55  thf(omega2_decl, type, omega2: (variable > real)).
% 277.20/240.55  thf(sigma_decl, type, sigma: (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game)))))).
% 277.20/240.55  thf(theta_decl, type, theta: trm).
% 277.20/240.55  thf(67,axiom,((! [TA: $tType,TB: $tType]: (! [A:TB,B:TA,C:TB,D:TA,E:(set @ (product_prod @ TB @ TB)),F:(set @ (product_prod @ TA @ TA))]: ((member @ (product_prod @ (product_prod @ TB @ TA) @ (product_prod @ TB @ TA)) @ (product_Pair @ (product_prod @ TB @ TA) @ (product_prod @ TB @ TA) @ (product_Pair @ TB @ TA @ A @ B) @ (product_Pair @ TB @ TA @ C @ D)) @ (lex_prod @ TB @ TA @ E @ F)) = ((member @ (product_prod @ TB @ TB) @ (product_Pair @ TB @ TB @ A @ C) @ E) | ((A = C) & (member @ (product_prod @ TA @ TA) @ (product_Pair @ TA @ TA @ B @ D) @ F))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_185_in__lex__prod)).
% 277.20/240.55  thf(468,plain,((! [TA: $tType,TB: $tType]: (! [A:TB,B:TA,C:TB,D:TA,E:(set @ (product_prod @ TB @ TB)),F:(set @ (product_prod @ TA @ TA))]: ((member @ (product_prod @ (product_prod @ TB @ TA) @ (product_prod @ TB @ TA)) @ (product_Pair @ (product_prod @ TB @ TA) @ (product_prod @ TB @ TA) @ (product_Pair @ TB @ TA @ A @ B) @ (product_Pair @ TB @ TA @ C @ D)) @ (lex_prod @ TB @ TA @ E @ F)) = ((member @ (product_prod @ TB @ TB) @ (product_Pair @ TB @ TB @ A @ C) @ E) | ((A = C) & (member @ (product_prod @ TA @ TA) @ (product_Pair @ TA @ TA @ B @ D) @ F))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 277.20/240.55  thf(72,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o),D:(TA > $o)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((! [E:TA]: ((member @ TA @ E @ A) => ((C @ E) => (D @ E)))) => (ord_less_eq @ (set @ TA) @ (collect @ TA @ (^ [E:TA]: ((member @ TA @ E @ A) & (C @ E)))) @ (collect @ TA @ (^ [E:TA]: ((member @ TA @ E @ B) & (D @ E)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_subset__CollectI)).
% 277.20/240.55  thf(481,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o),D:(TA > $o)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((! [E:TA]: ((member @ TA @ E @ A) => ((C @ E) => (D @ E)))) => (ord_less_eq @ (set @ TA) @ (collect @ TA @ (^ [E:TA]: ((member @ TA @ E @ A) & (C @ E)))) @ (collect @ TA @ (^ [E:TA]: ((member @ TA @ E @ B) & (D @ E)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 277.20/240.55  thf(126,axiom,((! [A:char,B:trm]: ((const @ A) != (differential @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_trm_Odistinct_I29_J)).
% 277.20/240.55  thf(666,plain,((! [A:char,B:trm]: ~ ((const @ A) = (differential @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 277.20/240.55  thf(211,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm]: (((uSubst95898992stappt @ A @ B @ (differential @ C)) != (none @ trm)) => ((uSubst95898992stappt @ A @ (collect @ variable @ (^ [D:variable]: (($true)))) @ C) != (none @ trm))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_117_usubstappt__differential__conv)).
% 277.20/240.55  thf(1295,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm]: ((~ ((uSubst95898992stappt @ A @ B @ (differential @ C)) = (none @ trm))) => (~ ((uSubst95898992stappt @ A @ (collect @ variable @ (^ [D:variable]: (($true)))) @ C) = (none @ trm)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 277.20/240.55  thf(49,axiom,((denota1419872369iation = (^ [A:(variable > real),B:(variable > real),C:(set @ variable)]: ! [D:variable]: ((~ (member @ variable @ D @ C)) => ((A @ D) = (B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_Uvariation__def)).
% 277.20/240.55  thf(408,plain,(((denota1419872369iation) = (^ [A:(variable > real),B:(variable > real),C:(set @ variable)]: ! [D:variable]: ((~ (member @ variable @ D @ C)) => ((A @ D) = (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 277.20/240.55  thf(142,axiom,((! [A:(option @ trm),B:(option @ trm),C:(option @ fml)]: (((uSubst1556497037e_Geqo @ A @ B) = C) => ((! [D:trm]: ((A = (some @ trm @ D)) => (! [E:trm]: ((B = (some @ trm @ E)) => (C != (some @ fml @ (geq @ D @ E))))))) => (((A = (none @ trm)) => (C != (none @ fml))) => (~ ((? [D:trm]: (A = (some @ trm @ D))) => ((B = (none @ trm)) => (C != (none @ fml)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_Geqo_Oelims)).
% 277.20/240.55  thf(762,plain,((! [A:(option @ trm),B:(option @ trm),C:(option @ fml)]: (((uSubst1556497037e_Geqo @ A @ B) = C) => ((! [D:trm]: ((A = (some @ trm @ D)) => (! [E:trm]: ((B = (some @ trm @ E)) => (~ (C = (some @ fml @ (geq @ D @ E)))))))) => (((A = (none @ trm)) => (~ (C = (none @ fml)))) => (~ ((? [D:trm]: (A = (some @ trm @ D))) => ((B = (none @ trm)) => (~ (C = (none @ fml))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 277.20/240.55  thf(233,axiom,((! [A:(option @ trm),B:(option @ trm),C:(option @ trm)]: (((uSubst277968634Timeso @ A @ B) = C) => ((! [D:trm]: ((A = (some @ trm @ D)) => (! [E:trm]: ((B = (some @ trm @ E)) => (C != (some @ trm @ (times @ D @ E))))))) => (((A = (none @ trm)) => (C != (none @ trm))) => (~ ((? [D:trm]: (A = (some @ trm @ D))) => ((B = (none @ trm)) => (C != (none @ trm)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_Timeso_Oelims)).
% 277.20/240.55  thf(1401,plain,((! [A:(option @ trm),B:(option @ trm),C:(option @ trm)]: (((uSubst277968634Timeso @ A @ B) = C) => ((! [D:trm]: ((A = (some @ trm @ D)) => (! [E:trm]: ((B = (some @ trm @ E)) => (~ (C = (some @ trm @ (times @ D @ E)))))))) => (((A = (none @ trm)) => (~ (C = (none @ trm)))) => (~ ((? [D:trm]: (A = (some @ trm @ D))) => ((B = (none @ trm)) => (~ (C = (none @ trm))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 277.20/240.55  thf(191,axiom,((! [A:(product_prod @ variable @ (option @ fml))]: ((! [B:variable,C:fml]: (A != (product_Pair @ variable @ (option @ fml) @ B @ (some @ fml @ C)))) => (~ (! [B:variable]: (A != (product_Pair @ variable @ (option @ fml) @ B @ (none @ fml)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_178_Existso_Ocases)).
% 277.20/240.55  thf(1173,plain,((! [A:(product_prod @ variable @ (option @ fml))]: ((! [B:variable,C:fml]: ~ (A = (product_Pair @ variable @ (option @ fml) @ B @ (some @ fml @ C)))) => (~ (! [B:variable]: ~ (A = (product_Pair @ variable @ (option @ fml) @ B @ (none @ fml)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 277.20/240.55  thf(42,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) = (B @ C))) => ((collect @ TA @ A) = (collect @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_Collect__cong)).
% 277.20/240.55  thf(384,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) = (B @ C))) => ((collect @ TA @ (A)) = (collect @ TA @ (B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 277.20/240.55  thf(213,axiom,((! [A:variable,B:(option @ trm),C:(option @ game)]: (((uSubst1326326671ssigno @ A @ B) = C) => ((! [D:trm]: ((B = (some @ trm @ D)) => (C != (some @ game @ (assign @ A @ D))))) => (~ ((B = (none @ trm)) => (C != (none @ game)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_Assigno_Oelims)).
% 277.20/240.55  thf(1327,plain,((! [A:variable,B:(option @ trm),C:(option @ game)]: (((uSubst1326326671ssigno @ A @ B) = C) => ((! [D:trm]: ((B = (some @ trm @ D)) => (~ (C = (some @ game @ (assign @ A @ D)))))) => (~ ((B = (none @ trm)) => (~ (C = (none @ game))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 277.20/240.55  thf(218,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: ((uSubst95898992stappt @ A @ B @ (plus @ C @ D)) = (uSubst1112714340_Pluso @ (uSubst95898992stappt @ A @ B @ C) @ (uSubst95898992stappt @ A @ B @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_usubstappt_Osimps_I5_J)).
% 277.20/240.55  thf(1354,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: ((uSubst95898992stappt @ A @ B @ (plus @ C @ D)) = (uSubst1112714340_Pluso @ (uSubst95898992stappt @ A @ B @ C) @ (uSubst95898992stappt @ A @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 277.20/240.55  thf(127,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:TC,B:(TA > TC),C:TA,D:TB,E:(TA > TB),F:(set @ TA)]: ((A = (B @ C)) => ((D = (E @ C)) => ((member @ TA @ C @ F) => (member @ (product_prod @ TC @ TB) @ (product_Pair @ TC @ TB @ A @ D) @ (bNF_Greatest_image2 @ TA @ TC @ TB @ F @ B @ E)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_222_image2__eqI)).
% 277.20/240.55  thf(670,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:TC,B:(TA > TC),C:TA,D:TB,E:(TA > TB),F:(set @ TA)]: ((A = (B @ C)) => ((D = (E @ C)) => ((member @ TA @ C @ F) => (member @ (product_prod @ TC @ TB) @ (product_Pair @ TC @ TB @ A @ D) @ (bNF_Greatest_image2 @ TA @ TC @ TB @ F @ (B) @ (E))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 277.20/240.55  thf(48,axiom,((! [TA: $tType]: (! [A:(TA > (TA > $o)),B:TA]: ((~ (accp @ TA @ A @ B)) => (~ (! [C:TA]: ((A @ C @ B) => (accp @ TA @ A @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_152_not__accp__down)).
% 277.20/240.55  thf(404,plain,((! [TA: $tType]: (! [A:(TA > (TA > $o)),B:TA]: ((~ (accp @ TA @ (A) @ B)) => (~ (! [C:TA]: ((A @ C @ B) => (accp @ TA @ (A) @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 277.20/240.55  thf(154,axiom,((! [A:(set @ variable),B:(set @ variable),C:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),D:fml]: ((ord_less_eq @ (set @ variable) @ A @ B) => (((uSubst95898978stappf @ C @ B @ D) != (none @ fml)) => ((uSubst95898978stappf @ C @ B @ D) = (uSubst95898978stappf @ C @ A @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_usubstappf__antimon)).
% 277.20/240.55  thf(898,plain,((! [A:(set @ variable),B:(set @ variable),C:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),D:fml]: ((ord_less_eq @ (set @ variable) @ A @ B) => ((~ ((uSubst95898978stappf @ C @ B @ D) = (none @ fml))) => ((uSubst95898978stappf @ C @ B @ D) = (uSubst95898978stappf @ C @ A @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 277.20/240.55  thf(239,axiom,((! [A:(product_prod @ (option @ fml) @ (option @ fml))]: ((! [B:fml,C:fml]: (A != (product_Pair @ (option @ fml) @ (option @ fml) @ (some @ fml @ B) @ (some @ fml @ C)))) => ((! [B:(option @ fml)]: (A != (product_Pair @ (option @ fml) @ (option @ fml) @ (none @ fml) @ B))) => (~ (! [B:fml]: (A != (product_Pair @ (option @ fml) @ (option @ fml) @ (some @ fml @ B) @ (none @ fml))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_179_Ando_Ocases)).
% 277.20/240.55  thf(1441,plain,((! [A:(product_prod @ (option @ fml) @ (option @ fml))]: ((! [B:fml,C:fml]: ~ (A = (product_Pair @ (option @ fml) @ (option @ fml) @ (some @ fml @ B) @ (some @ fml @ C)))) => ((! [B:(option @ fml)]: ~ (A = (product_Pair @ (option @ fml) @ (option @ fml) @ (none @ fml) @ B))) => (~ (! [B:fml]: ~ (A = (product_Pair @ (option @ fml) @ (option @ fml) @ (some @ fml @ B) @ (none @ fml))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 277.20/240.55  thf(13,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) | (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_linear)).
% 277.20/240.55  thf(288,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) | (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 277.20/240.55  thf(19,axiom,((! [TA: $tType]: (order_top @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Oorder__top_1)).
% 277.20/240.55  thf(301,plain,((! [TA: $tType]: (order_top @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 277.20/240.55  thf(6,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((! [B:TA]: (member @ TA @ B @ A)) => ((top_top @ (set @ TA)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_245_UNIV__eq__I)).
% 277.20/240.55  thf(257,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((! [B:TA]: (member @ TA @ B @ A)) => ((top_top @ (set @ TA)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 277.20/240.55  thf(212,axiom,((! [A:char,B:(option @ trm),C:(option @ game)]: (((uSubst1083227664e_ODEo @ A @ B) = C) => ((accp @ (product_prod @ char @ (option @ trm)) @ uSubst2007600873Eo_rel @ (product_Pair @ char @ (option @ trm) @ A @ B)) => ((! [D:trm]: ((B = (some @ trm @ D)) => ((C = (some @ game @ (ode @ A @ D))) => (~ (accp @ (product_prod @ char @ (option @ trm)) @ uSubst2007600873Eo_rel @ (product_Pair @ char @ (option @ trm) @ A @ (some @ trm @ D))))))) => (~ ((B = (none @ trm)) => ((C = (none @ game)) => (~ (accp @ (product_prod @ char @ (option @ trm)) @ uSubst2007600873Eo_rel @ (product_Pair @ char @ (option @ trm) @ A @ (none @ trm)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_249_ODEo_Opelims)).
% 277.20/240.55  thf(1298,plain,((! [A:char,B:(option @ trm),C:(option @ game)]: (((uSubst1083227664e_ODEo @ A @ B) = C) => ((accp @ (product_prod @ char @ (option @ trm)) @ (uSubst2007600873Eo_rel) @ (product_Pair @ char @ (option @ trm) @ A @ B)) => ((! [D:trm]: ((B = (some @ trm @ D)) => ((C = (some @ game @ (ode @ A @ D))) => (~ (accp @ (product_prod @ char @ (option @ trm)) @ (uSubst2007600873Eo_rel) @ (product_Pair @ char @ (option @ trm) @ A @ (some @ trm @ D))))))) => (~ ((B = (none @ trm)) => ((C = (none @ game)) => (~ (accp @ (product_prod @ char @ (option @ trm)) @ (uSubst2007600873Eo_rel) @ (product_Pair @ char @ (option @ trm) @ A @ (none @ trm)))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 277.20/240.55  thf(39,axiom,((! [A:variable,B:char,C:trm]: ((var @ A) != (func @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_trm_Odistinct_I5_J)).
% 277.20/240.55  thf(372,plain,((! [A:variable,B:char,C:trm]: ~ ((var @ A) = (func @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 277.20/240.55  thf(77,axiom,((! [TA: $tType]: ((ord_less_eq @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (ord_less_eq @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_less__eq__set__def)).
% 277.20/240.55  thf(504,plain,((! [TA: $tType]: ((ord_less_eq @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (ord_less_eq @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 277.20/240.55  thf(202,axiom,((! [A:(option @ trm)]: ((A != (none @ trm)) = (? [B:trm]: (A = (some @ trm @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_108_undeft__equiv)).
% 277.20/240.55  thf(1264,plain,((! [A:(option @ trm)]: ((~ (A = (none @ trm))) = (? [B:trm]: (A = (some @ trm @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 277.20/240.55  thf(155,axiom,((! [A:variable,B:(option @ trm)]: (((uSubst1326326671ssigno @ A @ B) = (none @ game)) = (B = (none @ trm))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_Assigno__undef)).
% 277.20/240.55  thf(902,plain,((! [A:variable,B:(option @ trm)]: (((uSubst1326326671ssigno @ A @ B) = (none @ game)) = (B = (none @ trm))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 277.20/240.55  thf(118,axiom,((! [A:trm,B:trm,C:trm,D:trm]: (((plus @ A @ B) = (plus @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_trm_Oinject_I5_J)).
% 277.20/240.55  thf(638,plain,((! [A:trm,B:trm,C:trm,D:trm]: (((plus @ A @ B) = (plus @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 277.20/240.55  thf(106,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((ord_less_eq @ (TA > $o) @ A @ B) => (ord_less_eq @ ((set @ TA) > $o) @ (powp @ TA @ A) @ (powp @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_121_Powp__mono)).
% 277.20/240.55  thf(606,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((ord_less_eq @ (TA > $o) @ (A) @ (B)) => (ord_less_eq @ ((set @ TA) > $o) @ (powp @ TA @ A) @ (powp @ TA @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 277.20/240.55  thf(232,axiom,((! [A:trm]: ((uSubst259074819ntialo @ (some @ trm @ A)) = (some @ trm @ (differential @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_Differentialo_Osimps_I1_J)).
% 277.20/240.55  thf(1398,plain,((! [A:trm]: ((uSubst259074819ntialo @ (some @ trm @ A)) = (some @ trm @ (differential @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 277.20/240.55  thf(60,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > $o)]: (ord_less_eq @ (set @ TA) @ (collect @ TA @ (^ [C:TA]: ((member @ TA @ C @ A) & (B @ C)))) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_Collect__subset)).
% 277.20/240.55  thf(448,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > $o)]: (ord_less_eq @ (set @ TA) @ (collect @ TA @ (^ [C:TA]: ((member @ TA @ C @ A) & (B @ C)))) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 277.20/240.55  thf(25,axiom,((! [A:(variable > real),B:(variable > real),C:(set @ variable)]: ((denota1419872369iation @ A @ B @ C) => (denota1419872369iation @ B @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_Uvariation__sym__rel)).
% 277.20/240.55  thf(316,plain,((! [A:(variable > real),B:(variable > real),C:(set @ variable)]: ((denota1419872369iation @ (A) @ (B) @ C) => (denota1419872369iation @ (B) @ (A) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 277.20/240.55  thf(235,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: (((uSubst95898992stappt @ A @ B @ (plus @ C @ D)) != (none @ trm)) => (((uSubst95898992stappt @ A @ B @ C) != (none @ trm)) & ((uSubst95898992stappt @ A @ B @ D) != (none @ trm)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_usubstappt__plus__conv)).
% 277.20/240.55  thf(1415,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: ((~ ((uSubst95898992stappt @ A @ B @ (plus @ C @ D)) = (none @ trm))) => (~ ((uSubst95898992stappt @ A @ B @ C) = (none @ trm)) & ~ ((uSubst95898992stappt @ A @ B @ D) = (none @ trm)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 277.20/240.55  thf(70,axiom,((denota1419872369iation = (^ [A:(variable > real),B:(variable > real)]: (denota1419872369iation @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_Uvariation__sym)).
% 277.20/240.55  thf(475,plain,(((denota1419872369iation) = (^ [A:(variable > real),B:(variable > real)]: (denota1419872369iation @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 277.20/240.55  thf(40,axiom,((! [A:trm,B:trm,C:trm,D:trm]: ((plus @ A @ B) != (times @ C @ D)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_trm_Odistinct_I37_J)).
% 277.20/240.55  thf(376,plain,((! [A:trm,B:trm,C:trm,D:trm]: ~ ((plus @ A @ B) = (times @ C @ D)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 277.20/240.55  thf(112,axiom,((linorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Olinorder)).
% 277.20/240.55  thf(623,plain,((linorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 277.20/240.55  thf(149,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((A != (none @ TA)) => (A = (some @ TA @ (the @ TA @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_145_option_Oexhaust__sel)).
% 277.20/240.55  thf(834,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ((~ (A = (none @ TA))) => (A = (some @ TA @ (the @ TA @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 277.20/240.55  thf(207,axiom,((! [A:(variable > ((option @ trm) > $o)),B:variable,C:(option @ trm)]: ((! [D:variable,E:trm]: (A @ D @ (some @ trm @ E))) => ((! [D:variable]: (A @ D @ (none @ trm))) => (A @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_106_Assigno_Oinduct)).
% 277.20/240.55  thf(1283,plain,((! [A:(variable > ((option @ trm) > $o)),B:variable,C:(option @ trm)]: ((! [D:variable,E:trm]: (A @ D @ (some @ trm @ E))) => ((! [D:variable]: (A @ D @ (none @ trm))) => (A @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 277.20/240.55  thf(156,axiom,((! [A:((option @ game) > ((option @ fml) > $o)),B:(option @ game),C:(option @ fml)]: ((! [D:game,E:fml]: (A @ (some @ game @ D) @ (some @ fml @ E))) => ((! [D:(option @ fml)]: (A @ (none @ game) @ D)) => ((! [D:game]: (A @ (some @ game @ D) @ (none @ fml))) => (A @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_125_Diamondo_Oinduct)).
% 277.20/240.55  thf(905,plain,((! [A:((option @ game) > ((option @ fml) > $o)),B:(option @ game),C:(option @ fml)]: ((! [D:game,E:fml]: (A @ (some @ game @ D) @ (some @ fml @ E))) => ((! [D:(option @ fml)]: (A @ (none @ game) @ D)) => ((! [D:game]: (A @ (some @ game @ D) @ (none @ fml))) => (A @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 277.20/240.55  thf(241,axiom,((! [TA: $tType]: (! [A:$o,B:(TA > $o),C:(option @ TA)]: ((case_option @ $o @ TA @ A @ B @ C) => (((C = (none @ TA)) => (~ (A))) => (~ (! [D:TA]: ((C = (some @ TA @ D)) => (~ (B @ D)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_168_case__optionE)).
% 277.20/240.55  thf(1447,plain,((! [TA: $tType]: (! [A:$o,B:(TA > $o),C:(option @ TA)]: ((case_option @ $o @ TA @ A @ (B) @ C) => (((C = (none @ TA)) => (~ (A))) => (~ (! [D:TA]: ((C = (some @ TA @ D)) => (~ (B @ D)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 277.20/240.55  thf(62,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B))) = (ord_less_eq @ (set @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_pred__subset__eq)).
% 277.20/240.55  thf(453,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B))) = (ord_less_eq @ (set @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 277.20/240.55  thf(231,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:fml,D:(set @ variable)]: (((uSubst95898978stappf @ A @ B @ C) != (none @ fml)) => (((uSubst95898978stappf @ A @ D @ C) != (none @ fml)) => ((uSubst95898978stappf @ A @ B @ C) = (uSubst95898978stappf @ A @ D @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_usubstappf__det)).
% 277.20/240.55  thf(1394,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:fml,D:(set @ variable)]: ((~ ((uSubst95898978stappf @ A @ B @ C) = (none @ fml))) => ((~ ((uSubst95898978stappf @ A @ D @ C) = (none @ fml))) => ((uSubst95898978stappf @ A @ B @ C) = (uSubst95898978stappf @ A @ D @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[231])).
% 277.20/240.55  thf(217,axiom,(((uSubst95898978stappf @ sigma @ ua @ (geq @ theta @ eta)) != (none @ fml))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_Geq_Oprems_I1_J)).
% 277.20/240.55  thf(1351,plain,((~ ((uSubst95898978stappf @ sigma @ ua @ (geq @ theta @ eta)) = (none @ fml)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[217])).
% 277.20/240.55  thf(173,axiom,((! [A:variable,B:(option @ trm),C:(option @ game)]: (((uSubst1326326671ssigno @ A @ B) = C) => ((accp @ (product_prod @ variable @ (option @ trm)) @ uSubst1741596714no_rel @ (product_Pair @ variable @ (option @ trm) @ A @ B)) => ((! [D:trm]: ((B = (some @ trm @ D)) => ((C = (some @ game @ (assign @ A @ D))) => (~ (accp @ (product_prod @ variable @ (option @ trm)) @ uSubst1741596714no_rel @ (product_Pair @ variable @ (option @ trm) @ A @ (some @ trm @ D))))))) => (~ ((B = (none @ trm)) => ((C = (none @ game)) => (~ (accp @ (product_prod @ variable @ (option @ trm)) @ uSubst1741596714no_rel @ (product_Pair @ variable @ (option @ trm) @ A @ (none @ trm)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_Assigno_Opelims)).
% 277.20/240.55  thf(998,plain,((! [A:variable,B:(option @ trm),C:(option @ game)]: (((uSubst1326326671ssigno @ A @ B) = C) => ((accp @ (product_prod @ variable @ (option @ trm)) @ (uSubst1741596714no_rel) @ (product_Pair @ variable @ (option @ trm) @ A @ B)) => ((! [D:trm]: ((B = (some @ trm @ D)) => ((C = (some @ game @ (assign @ A @ D))) => (~ (accp @ (product_prod @ variable @ (option @ trm)) @ (uSubst1741596714no_rel) @ (product_Pair @ variable @ (option @ trm) @ A @ (some @ trm @ D))))))) => (~ ((B = (none @ trm)) => ((C = (none @ game)) => (~ (accp @ (product_prod @ variable @ (option @ trm)) @ (uSubst1741596714no_rel) @ (product_Pair @ variable @ (option @ trm) @ A @ (none @ trm)))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 277.20/240.55  thf(53,axiom,((! [TA: $tType,TB: $tType]: (! [A:TA,B:TB,C:(set @ (product_prod @ TA @ TB)),D:TB]: ((member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ A @ B) @ C) => ((D = B) => (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ A @ D) @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_159_ssubst__Pair__rhs)).
% 277.20/240.55  thf(428,plain,((! [TA: $tType,TB: $tType]: (! [A:TA,B:TB,C:(set @ (product_prod @ TA @ TB)),D:TB]: ((member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ A @ B) @ C) => ((D = B) => (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ A @ D) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 277.20/240.55  thf(197,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((A != (none @ TA)) => ((some @ TA @ (the @ TA @ A)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_136_option_Ocollapse)).
% 277.20/240.55  thf(1242,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ((~ (A = (none @ TA))) => ((some @ TA @ (the @ TA @ A)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 277.20/240.55  thf(78,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > $o)]: (ord_less_eq @ (set @ TA) @ (collect @ TA @ (^ [C:TA]: ((member @ TA @ C @ A) & (B @ C)))) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_Collect__restrict)).
% 277.20/240.55  thf(507,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > $o)]: (ord_less_eq @ (set @ TA) @ (collect @ TA @ (^ [C:TA]: ((member @ TA @ C @ A) & (B @ C)))) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 277.20/240.55  thf(83,axiom,((! [A:variable,B:trm,C:trm]: ((var @ A) != (times @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_trm_Odistinct_I9_J)).
% 277.20/240.55  thf(527,plain,((! [A:variable,B:trm,C:trm]: ~ ((var @ A) = (times @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 277.20/240.55  thf(104,axiom,((! [A:(variable > real),B:(set @ variable)]: (denota1419872369iation @ A @ A @ B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_Uvariation__refl)).
% 277.20/240.55  thf(602,plain,((! [A:(variable > real),B:(set @ variable)]: (denota1419872369iation @ (A) @ (A) @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 277.20/240.55  thf(171,axiom,((! [A:(option @ trm),B:(option @ trm)]: (((uSubst259074819ntialo @ A) = B) => ((! [C:trm]: ((A = (some @ trm @ C)) => (B != (some @ trm @ (differential @ C))))) => (~ ((A = (none @ trm)) => (B != (none @ trm)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_Differentialo_Oelims)).
% 277.20/240.55  thf(981,plain,((! [A:(option @ trm),B:(option @ trm)]: (((uSubst259074819ntialo @ A) = B) => ((! [C:trm]: ((A = (some @ trm @ C)) => (~ (B = (some @ trm @ (differential @ C)))))) => (~ ((A = (none @ trm)) => (~ (B = (none @ trm))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 277.20/240.55  thf(46,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) => (B @ C))) => (ord_less_eq @ (TA > $o) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_predicate1I)).
% 277.20/240.55  thf(397,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) => (B @ C))) => (ord_less_eq @ (TA > $o) @ (A) @ (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 277.20/240.55  thf(131,axiom,((! [A:variable,B:trm]: ((var @ A) != (differential @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_trm_Odistinct_I11_J)).
% 277.20/240.55  thf(687,plain,((! [A:variable,B:trm]: ~ ((var @ A) = (differential @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 277.20/240.55  thf(225,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: (((uSubst95898978stappf @ A @ B @ (geq @ C @ D)) != (none @ fml)) => ((uSubst95898978stappf @ A @ B @ (geq @ C @ D)) = (some @ fml @ (geq @ (the @ trm @ (uSubst95898992stappt @ A @ B @ C)) @ (the @ trm @ (uSubst95898992stappt @ A @ B @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_usubstappf__geqr)).
% 277.20/240.55  thf(1377,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: ((~ ((uSubst95898978stappf @ A @ B @ (geq @ C @ D)) = (none @ fml))) => ((uSubst95898978stappf @ A @ B @ (geq @ C @ D)) = (some @ fml @ (geq @ (the @ trm @ (uSubst95898992stappt @ A @ B @ C)) @ (the @ trm @ (uSubst95898992stappt @ A @ B @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[225])).
% 277.20/240.55  thf(10,axiom,((! [TA: $tType]: (? [A:TA]: (member @ TA @ A @ (top_top @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_UNIV__witness)).
% 277.20/240.55  thf(280,plain,((! [TA: $tType]: (? [A:TA]: (member @ TA @ A @ (top_top @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 277.20/240.55  thf(22,axiom,((! [A:char,B:trm,C:trm]: ((func @ A @ B) != (differential @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_210_trm_Odistinct_I35_J)).
% 277.20/240.55  thf(307,plain,((! [A:char,B:trm,C:trm]: ~ ((func @ A @ B) = (differential @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 277.20/240.55  thf(15,axiom,((! [TA: $tType]: ((top_top @ (TA > $o)) = (^ [A:TA]: (member @ TA @ A @ (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_252_top__empty__eq)).
% 277.20/240.55  thf(292,plain,((! [TA: $tType]: ((top_top @ (TA > $o)) = (^ [A:TA]: (member @ TA @ A @ (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 277.20/240.55  thf(4,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less_eq @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_linorder__wlog)).
% 277.20/240.55  thf(248,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less_eq @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 277.20/240.55  thf(41,axiom,((! [A:trm]: ((! [B:variable]: (A != (var @ B))) => ((! [B:real]: (A != (number @ B))) => ((! [B:char]: (A != (const @ B))) => ((! [B:char,C:trm]: (A != (func @ B @ C))) => ((! [B:trm,C:trm]: (A != (plus @ B @ C))) => ((! [B:trm,C:trm]: (A != (times @ B @ C))) => (~ (! [B:trm]: (A != (differential @ B)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_214_trm_Oexhaust)).
% 277.20/240.55  thf(380,plain,((! [A:trm]: ((! [B:variable]: ~ (A = (var @ B))) => ((! [B:real]: ~ (A = (number @ B))) => ((! [B:char]: ~ (A = (const @ B))) => ((! [B:char,C:trm]: ~ (A = (func @ B @ C))) => ((! [B:trm,C:trm]: ~ (A = (plus @ B @ C))) => ((! [B:trm,C:trm]: ~ (A = (times @ B @ C))) => (~ (! [B:trm]: ~ (A = (differential @ B)))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 277.20/240.55  thf(238,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm]: ((accp @ (product_prod @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm)) @ uSubst2096773001pt_rel @ (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ A @ (product_Pair @ (set @ variable) @ trm @ B @ (differential @ C)))) => ((uSubst95898992stappt @ A @ B @ (differential @ C)) = (uSubst259074819ntialo @ (uSubst95898992stappt @ A @ (collect @ variable @ (^ [D:variable]: (($true)))) @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_180_usubstappt_Opsimps_I7_J)).
% 277.20/240.55  thf(1438,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm]: ((accp @ (product_prod @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm)) @ (uSubst2096773001pt_rel) @ (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ A @ (product_Pair @ (set @ variable) @ trm @ B @ (differential @ C)))) => ((uSubst95898992stappt @ A @ B @ (differential @ C)) = (uSubst259074819ntialo @ (uSubst95898992stappt @ A @ (collect @ variable @ (^ [D:variable]: (($true)))) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[238])).
% 277.20/240.55  thf(229,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > $o),B:TB,C:(TA > TB),D:(option @ TA)]: ((A @ (case_option @ TB @ TA @ B @ C @ D)) = (((D = (none @ TA)) => (A @ B)) & ((D = (some @ TA @ (the @ TA @ D))) => (A @ (C @ (the @ TA @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_157_option_Osplit__sel)).
% 277.20/240.55  thf(1387,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > $o),B:TB,C:(TA > TB),D:(option @ TA)]: ((A @ (case_option @ TB @ TA @ B @ (C) @ D)) = (((D = (none @ TA)) => (A @ B)) & ((D = (some @ TA @ (the @ TA @ D))) => (A @ (C @ (the @ TA @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 277.20/240.55  thf(137,axiom,((! [TA: $tType]: (! [A:TA]: ((none @ TA) != (some @ TA @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_option_Odistinct_I1_J)).
% 277.20/240.55  thf(746,plain,((! [TA: $tType]: (! [A:TA]: ~ ((none @ TA) = (some @ TA @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 277.20/240.55  thf(199,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm]: ((uSubst95898992stappt @ A @ B @ (differential @ C)) = (uSubst259074819ntialo @ (uSubst95898992stappt @ A @ (collect @ variable @ (^ [D:variable]: (($true)))) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_usubstappt_Osimps_I7_J)).
% 277.20/240.55  thf(1255,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm]: ((uSubst95898992stappt @ A @ B @ (differential @ C)) = (uSubst259074819ntialo @ (uSubst95898992stappt @ A @ (collect @ variable @ (^ [D:variable]: (($true)))) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 277.20/240.55  thf(103,axiom,((! [A:variable,B:char]: ((var @ A) != (const @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_trm_Odistinct_I3_J)).
% 277.20/240.55  thf(598,plain,((! [A:variable,B:char]: ~ ((var @ A) = (const @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 277.20/240.55  thf(94,axiom,((! [TA: $tType,TB: $tType]: (! [A:(set @ (product_prod @ TB @ TB)),B:(set @ (product_prod @ TB @ TB)),C:(set @ TA),D:(TA > TB)]: ((ord_less_eq @ (set @ (product_prod @ TB @ TB)) @ A @ B) => (ord_less_eq @ (set @ (product_prod @ TA @ TA)) @ (bNF_Gr2107612801vImage @ TA @ TB @ C @ A @ D) @ (bNF_Gr2107612801vImage @ TA @ TB @ C @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_relInvImage__mono)).
% 277.20/240.55  thf(561,plain,((! [TA: $tType,TB: $tType]: (! [A:(set @ (product_prod @ TB @ TB)),B:(set @ (product_prod @ TB @ TB)),C:(set @ TA),D:(TA > TB)]: ((ord_less_eq @ (set @ (product_prod @ TB @ TB)) @ A @ B) => (ord_less_eq @ (set @ (product_prod @ TA @ TA)) @ (bNF_Gr2107612801vImage @ TA @ TB @ C @ A @ (D)) @ (bNF_Gr2107612801vImage @ TA @ TB @ C @ B @ (D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 277.20/240.55  thf(17,axiom,((! [TA: $tType,TB: $tType]: ((order_top @ TA) => (order_top @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oorder__top)).
% 277.20/240.55  thf(297,plain,((! [TA: $tType,TB: $tType]: ((order_top @ TA) => (order_top @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 277.20/240.55  thf(135,axiom,((! [A:(option @ fml),B:(option @ game)]: (((uSubst190403692_Testo @ A) = B) => ((! [C:fml]: ((A = (some @ fml @ C)) => (B != (some @ game @ (test @ C))))) => (~ ((A = (none @ fml)) => (B != (none @ game)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_220_Testo_Oelims)).
% 277.20/240.55  thf(729,plain,((! [A:(option @ fml),B:(option @ game)]: (((uSubst190403692_Testo @ A) = B) => ((! [C:fml]: ((A = (some @ fml @ C)) => (~ (B = (some @ game @ (test @ C)))))) => (~ ((A = (none @ fml)) => (~ (B = (none @ game))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 277.20/240.55  thf(7,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA,C:TA]: (((ord_less_eq @ TA @ A @ B) => (~ (ord_less_eq @ TA @ B @ C))) => (((ord_less_eq @ TA @ B @ A) => (~ (ord_less_eq @ TA @ A @ C))) => (((ord_less_eq @ TA @ A @ C) => (~ (ord_less_eq @ TA @ C @ B))) => (((ord_less_eq @ TA @ C @ B) => (~ (ord_less_eq @ TA @ B @ A))) => (((ord_less_eq @ TA @ B @ C) => (~ (ord_less_eq @ TA @ C @ A))) => (~ ((ord_less_eq @ TA @ C @ A) => (~ (ord_less_eq @ TA @ A @ B))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_48_le__cases3)).
% 277.20/240.55  thf(260,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA,C:TA]: (((ord_less_eq @ TA @ A @ B) => (~ (ord_less_eq @ TA @ B @ C))) => (((ord_less_eq @ TA @ B @ A) => (~ (ord_less_eq @ TA @ A @ C))) => (((ord_less_eq @ TA @ A @ C) => (~ (ord_less_eq @ TA @ C @ B))) => (((ord_less_eq @ TA @ C @ B) => (~ (ord_less_eq @ TA @ B @ A))) => (((ord_less_eq @ TA @ B @ C) => (~ (ord_less_eq @ TA @ C @ A))) => (~ ((ord_less_eq @ TA @ C @ A) => (~ (ord_less_eq @ TA @ A @ B))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 277.20/240.55  thf(35,axiom,((top @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Otop_9)).
% 277.20/240.55  thf(349,plain,((top @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 277.20/240.55  thf(133,axiom,((! [A:(trm > $o),B:trm]: ((! [C:variable]: (A @ (var @ C))) => ((! [C:real]: (A @ (number @ C))) => ((! [C:char]: (A @ (const @ C))) => ((! [C:char,D:trm]: ((A @ D) => (A @ (func @ C @ D)))) => ((! [C:trm,D:trm]: ((A @ C) => ((A @ D) => (A @ (plus @ C @ D))))) => ((! [C:trm,D:trm]: ((A @ C) => ((A @ D) => (A @ (times @ C @ D))))) => ((! [C:trm]: ((A @ C) => (A @ (differential @ C)))) => (A @ B)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_213_trm_Oinduct)).
% 277.20/240.55  thf(693,plain,((! [A:(trm > $o),B:trm]: ((! [C:variable]: (A @ (var @ C))) => ((! [C:real]: (A @ (number @ C))) => ((! [C:char]: (A @ (const @ C))) => ((! [C:char,D:trm]: ((A @ D) => (A @ (func @ C @ D)))) => ((! [C:trm,D:trm]: ((A @ C) => ((A @ D) => (A @ (plus @ C @ D))))) => ((! [C:trm,D:trm]: ((A @ C) => ((A @ D) => (A @ (times @ C @ D))))) => ((! [C:trm]: ((A @ C) => (A @ (differential @ C)))) => (A @ B)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 277.20/240.55  thf(115,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((ord_less_eq @ (set @ TA) @ B @ A) => (A = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_subset__antisym)).
% 277.20/240.55  thf(630,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((ord_less_eq @ (set @ TA) @ B @ A) => (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 277.20/240.55  thf(8,axiom,((! [TA: $tType,TB: $tType]: ((top @ TB) => ((top_top @ (TA > TB)) = (^ [A:TA]: (top_top @ TB)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_top__apply)).
% 277.20/240.55  thf(275,plain,((! [TA: $tType,TB: $tType]: ((top @ TB) => ((top_top @ (TA > TB)) = (^ [A:TA]: (top_top @ TB)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 277.20/240.55  thf(223,axiom,((! [A:(option @ fml)]: ((! [B:fml]: (A != (some @ fml @ B))) => (A = (none @ fml))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_129_Testo_Ocases)).
% 277.20/240.55  thf(1370,plain,((! [A:(option @ fml)]: ((! [B:fml]: ~ (A = (some @ fml @ B))) => (A = (none @ fml))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 277.20/240.55  thf(147,axiom,((denota1419872369iation @ nu2 @ omega2 @ ua)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_Geq_Oprems_I2_J)).
% 277.20/240.55  thf(830,plain,((denota1419872369iation @ (nu2) @ (omega2) @ ua)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 277.20/240.55  thf(174,axiom,((! [A:(option @ trm),B:(option @ trm),C:(option @ trm)]: (((uSubst277968634Timeso @ A @ B) = C) => ((accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ uSubst1377811071so_rel @ (product_Pair @ (option @ trm) @ (option @ trm) @ A @ B)) => ((! [D:trm]: ((A = (some @ trm @ D)) => (! [E:trm]: ((B = (some @ trm @ E)) => ((C = (some @ trm @ (times @ D @ E))) => (~ (accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ uSubst1377811071so_rel @ (product_Pair @ (option @ trm) @ (option @ trm) @ (some @ trm @ D) @ (some @ trm @ E))))))))) => (((A = (none @ trm)) => ((C = (none @ trm)) => (~ (accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ uSubst1377811071so_rel @ (product_Pair @ (option @ trm) @ (option @ trm) @ (none @ trm) @ B))))) => (~ (! [D:trm]: ((A = (some @ trm @ D)) => ((B = (none @ trm)) => ((C = (none @ trm)) => (~ (accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ uSubst1377811071so_rel @ (product_Pair @ (option @ trm) @ (option @ trm) @ (some @ trm @ D) @ (none @ trm))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_172_Timeso_Opelims)).
% 277.20/240.55  thf(1027,plain,((! [A:(option @ trm),B:(option @ trm),C:(option @ trm)]: (((uSubst277968634Timeso @ A @ B) = C) => ((accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ (uSubst1377811071so_rel) @ (product_Pair @ (option @ trm) @ (option @ trm) @ A @ B)) => ((! [D:trm]: ((A = (some @ trm @ D)) => (! [E:trm]: ((B = (some @ trm @ E)) => ((C = (some @ trm @ (times @ D @ E))) => (~ (accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ (uSubst1377811071so_rel) @ (product_Pair @ (option @ trm) @ (option @ trm) @ (some @ trm @ D) @ (some @ trm @ E))))))))) => (((A = (none @ trm)) => ((C = (none @ trm)) => (~ (accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ (uSubst1377811071so_rel) @ (product_Pair @ (option @ trm) @ (option @ trm) @ (none @ trm) @ B))))) => (~ (! [D:trm]: ((A = (some @ trm @ D)) => ((B = (none @ trm)) => ((C = (none @ trm)) => (~ (accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ (uSubst1377811071so_rel) @ (product_Pair @ (option @ trm) @ (option @ trm) @ (some @ trm @ D) @ (none @ trm))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 277.20/240.55  thf(90,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TB > TC),B:TB,C:(TA > TB),D:(option @ TA)]: ((A @ (case_option @ TB @ TA @ B @ C @ D)) = (case_option @ TC @ TA @ (A @ B) @ (^ [E:TA]: (A @ (C @ E))) @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_161_option_Ocase__distrib)).
% 277.20/240.55  thf(551,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TB > TC),B:TB,C:(TA > TB),D:(option @ TA)]: ((A @ (case_option @ TB @ TA @ B @ (C) @ D)) = (case_option @ TC @ TA @ (A @ B) @ (^ [E:TA]: (A @ (C @ E))) @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 277.20/240.55  thf(169,axiom,((! [A:(product_prod @ (option @ trm) @ (option @ trm))]: ((! [B:trm,C:trm]: (A != (product_Pair @ (option @ trm) @ (option @ trm) @ (some @ trm @ B) @ (some @ trm @ C)))) => ((! [B:(option @ trm)]: (A != (product_Pair @ (option @ trm) @ (option @ trm) @ (none @ trm) @ B))) => (~ (! [B:trm]: (A != (product_Pair @ (option @ trm) @ (option @ trm) @ (some @ trm @ B) @ (none @ trm))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_167_Timeso_Ocases)).
% 277.20/240.55  thf(974,plain,((! [A:(product_prod @ (option @ trm) @ (option @ trm))]: ((! [B:trm,C:trm]: ~ (A = (product_Pair @ (option @ trm) @ (option @ trm) @ (some @ trm @ B) @ (some @ trm @ C)))) => ((! [B:(option @ trm)]: ~ (A = (product_Pair @ (option @ trm) @ (option @ trm) @ (none @ trm) @ B))) => (~ (! [B:trm]: ~ (A = (product_Pair @ (option @ trm) @ (option @ trm) @ (some @ trm @ B) @ (none @ trm))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 277.20/240.55  thf(63,axiom,((! [A:char,B:trm,C:char,D:trm]: (((func @ A @ B) = (func @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_200_trm_Oinject_I4_J)).
% 277.20/240.55  thf(456,plain,((! [A:char,B:trm,C:char,D:trm]: (((func @ A @ B) = (func @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 277.20/240.55  thf(152,axiom,((! [A:((option @ fml) > $o),B:(option @ fml)]: ((! [C:fml]: (A @ (some @ fml @ C))) => ((A @ (none @ fml)) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_128_Testo_Oinduct)).
% 277.20/240.55  thf(842,plain,((! [A:((option @ fml) > $o),B:(option @ fml)]: ((! [C:fml]: (A @ (some @ fml @ C))) => ((A @ (none @ fml)) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 277.20/240.55  thf(12,axiom,((! [TA: $tType]: ((order_top @ TA) => (! [A:TA]: ((ord_less_eq @ TA @ (top_top @ TA) @ A) = (A = (top_top @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_242_top_Oextremum__unique)).
% 277.20/240.55  thf(285,plain,((! [TA: $tType]: ((order_top @ TA) => (! [A:TA]: ((ord_less_eq @ TA @ (top_top @ TA) @ A) = (A = (top_top @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 277.20/240.55  thf(183,axiom,((! [TA: $tType]: (! [A:((option @ TA) > $o),B:(option @ TA)]: ((A @ (none @ TA)) => ((! [C:TA]: (A @ (some @ TA @ C))) => (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_option_Oinducts)).
% 277.20/240.55  thf(1106,plain,((! [TA: $tType]: (! [A:((option @ TA) > $o),B:(option @ TA)]: ((A @ (none @ TA)) => ((! [C:TA]: (A @ (some @ TA @ C))) => (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 277.20/240.55  thf(100,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: (((some @ TA @ A) = (some @ TA @ B)) = (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_option_Oinject)).
% 277.20/240.55  thf(578,plain,((! [TA: $tType]: (! [A:TA,B:TA]: (((some @ TA @ A) = (some @ TA @ B)) = (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 277.20/240.55  thf(122,axiom,((! [TA: $tType,TB: $tType]: (! [A:(set @ (product_prod @ TA @ TA)),B:(TA > TB)]: (ord_less_eq @ (set @ (product_prod @ TA @ TA)) @ A @ (bNF_Gr2107612801vImage @ TA @ TB @ (top_top @ (set @ TA)) @ (bNF_Gr1317331620lImage @ TA @ TB @ A @ B) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_relInvImage__UNIV__relImage)).
% 277.20/240.55  thf(650,plain,((! [TA: $tType,TB: $tType]: (! [A:(set @ (product_prod @ TA @ TA)),B:(TA > TB)]: (ord_less_eq @ (set @ (product_prod @ TA @ TA)) @ A @ (bNF_Gr2107612801vImage @ TA @ TB @ (top_top @ (set @ TA)) @ (bNF_Gr1317331620lImage @ TA @ TB @ A @ (B)) @ (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 277.20/240.55  thf(109,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TA > $o)),B:TB,C:TA,D:(TB > (TA > $o))]: ((A @ B @ C) => ((ord_less_eq @ (TB > (TA > $o)) @ A @ D) => (D @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_rev__predicate2D)).
% 277.20/240.55  thf(615,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TA > $o)),B:TB,C:TA,D:(TB > (TA > $o))]: ((A @ B @ C) => ((ord_less_eq @ (TB > (TA > $o)) @ (A) @ (D)) => (D @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 277.20/240.55  thf(184,axiom,((! [A:((option @ trm) > ((option @ trm) > $o)),B:(option @ trm),C:(option @ trm)]: ((! [D:trm,E:trm]: (A @ (some @ trm @ D) @ (some @ trm @ E))) => ((! [D:(option @ trm)]: (A @ (none @ trm) @ D)) => ((! [D:trm]: (A @ (some @ trm @ D) @ (none @ trm))) => (A @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_Timeso_Oinduct)).
% 277.20/240.55  thf(1111,plain,((! [A:((option @ trm) > ((option @ trm) > $o)),B:(option @ trm),C:(option @ trm)]: ((! [D:trm,E:trm]: (A @ (some @ trm @ D) @ (some @ trm @ E))) => ((! [D:(option @ trm)]: (A @ (none @ trm) @ D)) => ((! [D:trm]: (A @ (some @ trm @ D) @ (none @ trm))) => (A @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 277.20/240.55  thf(134,axiom,((! [A:real,B:trm,C:trm]: ((number @ A) != (times @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_189_trm_Odistinct_I19_J)).
% 277.20/240.55  thf(725,plain,((! [A:real,B:trm,C:trm]: ~ ((number @ A) = (times @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 277.20/240.55  thf(180,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: ((accp @ (product_prod @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm)) @ uSubst2096773001pt_rel @ (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ A @ (product_Pair @ (set @ variable) @ trm @ B @ (plus @ C @ D)))) => ((uSubst95898992stappt @ A @ B @ (plus @ C @ D)) = (uSubst1112714340_Pluso @ (uSubst95898992stappt @ A @ B @ C) @ (uSubst95898992stappt @ A @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_usubstappt_Opsimps_I5_J)).
% 277.20/240.55  thf(1096,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: ((accp @ (product_prod @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm)) @ (uSubst2096773001pt_rel) @ (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ A @ (product_Pair @ (set @ variable) @ trm @ B @ (plus @ C @ D)))) => ((uSubst95898992stappt @ A @ B @ (plus @ C @ D)) = (uSubst1112714340_Pluso @ (uSubst95898992stappt @ A @ B @ C) @ (uSubst95898992stappt @ A @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 277.20/240.55  thf(188,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((A != (none @ TA)) => (~ (! [B:TA]: (A != (some @ TA @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_option_Oexhaust)).
% 277.20/240.55  thf(1138,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ((~ (A = (none @ TA))) => (~ (! [B:TA]: ~ (A = (some @ TA @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 277.20/240.55  thf(186,axiom,((! [TA: $tType,TB: $tType]: (! [A:(option @ TB),B:((option @ TB) > ((option @ TA) > $o)),C:(option @ TA)]: (((A = (none @ TB)) => (B @ A @ C)) => (((C = (none @ TA)) => (B @ A @ C)) => ((! [D:TB,E:TA]: ((A = (some @ TB @ D)) => ((C = (some @ TA @ E)) => (B @ A @ C)))) => (B @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_combine__options__cases)).
% 277.20/240.55  thf(1118,plain,((! [TA: $tType,TB: $tType]: (! [A:(option @ TB),B:((option @ TB) > ((option @ TA) > $o)),C:(option @ TA)]: (((A = (none @ TB)) => (B @ A @ C)) => (((C = (none @ TA)) => (B @ A @ C)) => ((! [D:TB,E:TA]: ((A = (some @ TB @ D)) => ((C = (some @ TA @ E)) => (B @ A @ C)))) => (B @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 277.20/240.55  thf(220,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: ((uSubst95898978stappf @ A @ B @ (geq @ C @ D)) = (uSubst1556497037e_Geqo @ (uSubst95898992stappt @ A @ B @ C) @ (uSubst95898992stappt @ A @ B @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_usubstappf_Osimps_I2_J)).
% 277.20/240.55  thf(1361,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: ((uSubst95898978stappf @ A @ B @ (geq @ C @ D)) = (uSubst1556497037e_Geqo @ (uSubst95898992stappt @ A @ B @ C) @ (uSubst95898992stappt @ A @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 277.20/240.55  thf(210,axiom,((! [A:char]: ((uSubst1083227664e_ODEo @ A @ (none @ trm)) = (none @ game)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_247_ODEo_Osimps_I2_J)).
% 277.20/240.55  thf(1292,plain,((! [A:char]: ((uSubst1083227664e_ODEo @ A @ (none @ trm)) = (none @ game)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 277.20/240.55  thf(91,axiom,((! [A:char,B:trm,C:trm,D:trm]: ((func @ A @ B) != (times @ C @ D)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_211_trm_Odistinct_I33_J)).
% 277.20/240.55  thf(554,plain,((! [A:char,B:trm,C:trm,D:trm]: ~ ((func @ A @ B) = (times @ C @ D)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 277.20/240.55  thf(237,axiom,((! [A:char,B:(option @ trm),C:(option @ game)]: (((uSubst1083227664e_ODEo @ A @ B) = C) => ((! [D:trm]: ((B = (some @ trm @ D)) => (C != (some @ game @ (ode @ A @ D))))) => (~ ((B = (none @ trm)) => (C != (none @ game)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_248_ODEo_Oelims)).
% 277.20/240.55  thf(1424,plain,((! [A:char,B:(option @ trm),C:(option @ game)]: (((uSubst1083227664e_ODEo @ A @ B) = C) => ((! [D:trm]: ((B = (some @ trm @ D)) => (~ (C = (some @ game @ (ode @ A @ D)))))) => (~ ((B = (none @ trm)) => (~ (C = (none @ game))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 277.20/240.55  thf(168,axiom,((! [A:(product_prod @ (option @ game) @ (option @ game))]: ((! [B:game,C:game]: (A != (product_Pair @ (option @ game) @ (option @ game) @ (some @ game @ B) @ (some @ game @ C)))) => ((! [B:(option @ game)]: (A != (product_Pair @ (option @ game) @ (option @ game) @ B @ (none @ game)))) => (~ (! [B:game]: (A != (product_Pair @ (option @ game) @ (option @ game) @ (none @ game) @ (some @ game @ B))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_177_Composeo_Ocases)).
% 277.20/240.55  thf(970,plain,((! [A:(product_prod @ (option @ game) @ (option @ game))]: ((! [B:game,C:game]: ~ (A = (product_Pair @ (option @ game) @ (option @ game) @ (some @ game @ B) @ (some @ game @ C)))) => ((! [B:(option @ game)]: ~ (A = (product_Pair @ (option @ game) @ (option @ game) @ B @ (none @ game)))) => (~ (! [B:game]: ~ (A = (product_Pair @ (option @ game) @ (option @ game) @ (none @ game) @ (some @ game @ B))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 277.20/240.55  thf(29,axiom,((! [TA: $tType]: (! [A:(TA > (TA > $o)),B:TA]: ((! [C:TA]: ((A @ C @ B) => (accp @ TA @ A @ C))) => (accp @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_148_accp_Ointros)).
% 277.20/240.55  thf(328,plain,((! [TA: $tType]: (! [A:(TA > (TA > $o)),B:TA]: ((! [C:TA]: ((A @ C @ B) => (accp @ TA @ (A) @ C))) => (accp @ TA @ (A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 277.20/240.55  thf(68,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_in__mono)).
% 277.20/240.55  thf(471,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 277.20/240.55  thf(150,axiom,(((uSubst259074819ntialo @ (none @ trm)) = (none @ trm))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_Differentialo_Osimps_I2_J)).
% 277.20/240.55  thf(837,plain,(((uSubst259074819ntialo @ (none @ trm)) = (none @ trm))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 277.20/240.55  thf(121,axiom,((! [TA: $tType,TB: $tType]: ((bNF_Gr1317331620lImage @ TA @ TB) = (^ [A:(set @ (product_prod @ TA @ TA)),B:(TA > TB)]: (collect @ (product_prod @ TB @ TB) @ (^ [C:(product_prod @ TB @ TB)]: ? [D:TA,E:TA]: ((C = (product_Pair @ TB @ TB @ (B @ D) @ (B @ E))) & (member @ (product_prod @ TA @ TA) @ (product_Pair @ TA @ TA @ D @ E) @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_225_relImage__def)).
% 277.20/240.55  thf(647,plain,((! [TA: $tType,TB: $tType]: ((bNF_Gr1317331620lImage @ TA @ TB) = (^ [A:(set @ (product_prod @ TA @ TA)),B:(TA > TB)]: (collect @ (product_prod @ TB @ TB) @ (^ [C:(product_prod @ TB @ TB)]: ? [D:TA,E:TA]: ((C = (product_Pair @ TB @ TB @ (B @ D) @ (B @ E))) & (member @ (product_prod @ TA @ TA) @ (product_Pair @ TA @ TA @ D @ E) @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 277.20/240.55  thf(181,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/sandbox/benchmark/theBenchmark.p',fact_139_Composeo_Oinduct)).
% 277.20/240.55  thf(1099,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)],[181])).
% 277.20/240.55  thf(196,axiom,((! [A:(option @ trm),B:(option @ trm),C:(option @ fml)]: (((uSubst1556497037e_Geqo @ A @ B) = C) => ((accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ uSubst864323244qo_rel @ (product_Pair @ (option @ trm) @ (option @ trm) @ A @ B)) => ((! [D:trm]: ((A = (some @ trm @ D)) => (! [E:trm]: ((B = (some @ trm @ E)) => ((C = (some @ fml @ (geq @ D @ E))) => (~ (accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ uSubst864323244qo_rel @ (product_Pair @ (option @ trm) @ (option @ trm) @ (some @ trm @ D) @ (some @ trm @ E))))))))) => (((A = (none @ trm)) => ((C = (none @ fml)) => (~ (accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ uSubst864323244qo_rel @ (product_Pair @ (option @ trm) @ (option @ trm) @ (none @ trm) @ B))))) => (~ (! [D:trm]: ((A = (some @ trm @ D)) => ((B = (none @ trm)) => ((C = (none @ fml)) => (~ (accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ uSubst864323244qo_rel @ (product_Pair @ (option @ trm) @ (option @ trm) @ (some @ trm @ D) @ (none @ trm))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_155_Geqo_Opelims)).
% 277.20/240.55  thf(1192,plain,((! [A:(option @ trm),B:(option @ trm),C:(option @ fml)]: (((uSubst1556497037e_Geqo @ A @ B) = C) => ((accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ (uSubst864323244qo_rel) @ (product_Pair @ (option @ trm) @ (option @ trm) @ A @ B)) => ((! [D:trm]: ((A = (some @ trm @ D)) => (! [E:trm]: ((B = (some @ trm @ E)) => ((C = (some @ fml @ (geq @ D @ E))) => (~ (accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ (uSubst864323244qo_rel) @ (product_Pair @ (option @ trm) @ (option @ trm) @ (some @ trm @ D) @ (some @ trm @ E))))))))) => (((A = (none @ trm)) => ((C = (none @ fml)) => (~ (accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ (uSubst864323244qo_rel) @ (product_Pair @ (option @ trm) @ (option @ trm) @ (none @ trm) @ B))))) => (~ (! [D:trm]: ((A = (some @ trm @ D)) => ((B = (none @ trm)) => ((C = (none @ fml)) => (~ (accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ (uSubst864323244qo_rel) @ (product_Pair @ (option @ trm) @ (option @ trm) @ (some @ trm @ D) @ (none @ trm))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 277.20/240.55  thf(45,axiom,((! [A:char,B:trm,C:trm]: ((const @ A) != (plus @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_209_trm_Odistinct_I25_J)).
% 277.20/240.55  thf(393,plain,((! [A:char,B:trm,C:trm]: ~ ((const @ A) = (plus @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 277.20/240.55  thf(185,axiom,((! [A:(option @ trm)]: ((! [B:trm]: (A != (some @ trm @ B))) => (A = (none @ trm))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_105_Differentialo_Ocases)).
% 277.20/240.55  thf(1114,plain,((! [A:(option @ trm)]: ((! [B:trm]: ~ (A = (some @ trm @ B))) => (A = (none @ trm))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 277.20/240.55  thf(116,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: ((bNF_Greatest_image2 @ TA @ TC @ TB) = (^ [A:(set @ TA),B:(TA > TC),C:(TA > TB)]: (collect @ (product_prod @ TC @ TB) @ (^ [D:(product_prod @ TC @ TB)]: ? [E:TA]: ((D = (product_Pair @ TC @ TB @ (B @ E) @ (C @ E))) & (member @ TA @ E @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_image2__def)).
% 277.20/240.55  thf(633,plain,((! [TA: $tType,TB: $tType,TC: $tType]: ((bNF_Greatest_image2 @ TA @ TC @ TB) = (^ [A:(set @ TA),B:(TA > TC),C:(TA > TB)]: (collect @ (product_prod @ TC @ TB) @ (^ [D:(product_prod @ TC @ TB)]: ? [E:TA]: ((D = (product_Pair @ TC @ TB @ (B @ E) @ (C @ E))) & (member @ TA @ E @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 277.20/240.55  thf(23,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA),D:(TA > $o)]: ((member @ TA @ A @ B) => ((ord_less_eq @ (set @ TA) @ B @ (collect @ TA @ (^ [E:TA]: ((member @ TA @ E @ C) & (D @ E))))) => (D @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_prop__restrict)).
% 277.20/240.55  thf(311,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA),D:(TA > $o)]: ((member @ TA @ A @ B) => ((ord_less_eq @ (set @ TA) @ B @ (collect @ TA @ (^ [E:TA]: ((member @ TA @ E @ C) & (D @ E))))) => (D @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 277.20/240.55  thf(208,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((A = (none @ TA)) = (case_option @ $o @ TA @ ($true) @ (^ [B:TA]: (($false))) @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_165_option_Odisc__eq__case_I1_J)).
% 277.20/240.55  thf(1286,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ((A = (none @ TA)) = (case_option @ $o @ TA @ ($true) @ (^ [B:TA]: (($false))) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 277.20/240.55  thf(92,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TA > $o)),B:(TB > (TA > $o)),C:TB,D:TA]: ((ord_less_eq @ (TB > (TA > $o)) @ A @ B) => ((A @ C @ D) => (B @ C @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_137_predicate2D)).
% 277.20/240.55  thf(558,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TA > $o)),B:(TB > (TA > $o)),C:TB,D:TA]: ((ord_less_eq @ (TB > (TA > $o)) @ (A) @ (B)) => ((A @ C @ D) => (B @ C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 277.20/240.55  thf(128,axiom,((! [TA: $tType]: (! [A:(TA > (TA > $o)),B:TA,C:(TA > $o)]: ((accp @ TA @ A @ B) => ((! [D:TA]: ((accp @ TA @ A @ D) => ((! [E:TA]: ((A @ E @ D) => (C @ E))) => (C @ D)))) => (C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_153_accp__induct__rule)).
% 277.20/240.55  thf(674,plain,((! [TA: $tType]: (! [A:(TA > (TA > $o)),B:TA,C:(TA > $o)]: ((accp @ TA @ (A) @ B) => ((! [D:TA]: ((accp @ TA @ (A) @ D) => ((! [E:TA]: ((A @ E @ D) => (C @ E))) => (C @ D)))) => (C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 277.20/240.55  thf(144,axiom,((! [A:(option @ fml),B:(option @ game)]: (((uSubst190403692_Testo @ A) = B) => ((accp @ (option @ fml) @ uSubst533687181to_rel @ A) => ((! [C:fml]: ((A = (some @ fml @ C)) => ((B = (some @ game @ (test @ C))) => (~ (accp @ (option @ fml) @ uSubst533687181to_rel @ (some @ fml @ C)))))) => (~ ((A = (none @ fml)) => ((B = (none @ game)) => (~ (accp @ (option @ fml) @ uSubst533687181to_rel @ (none @ fml))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_224_Testo_Opelims)).
% 277.20/240.55  thf(794,plain,((! [A:(option @ fml),B:(option @ game)]: (((uSubst190403692_Testo @ A) = B) => ((accp @ (option @ fml) @ (uSubst533687181to_rel) @ A) => ((! [C:fml]: ((A = (some @ fml @ C)) => ((B = (some @ game @ (test @ C))) => (~ (accp @ (option @ fml) @ (uSubst533687181to_rel) @ (some @ fml @ C)))))) => (~ ((A = (none @ fml)) => ((B = (none @ game)) => (~ (accp @ (option @ fml) @ (uSubst533687181to_rel) @ (none @ fml))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 277.20/240.55  thf(162,axiom,((! [TA: $tType]: (((?) @ (option @ TA)) = (^ [A:((option @ TA) > $o)]: ((A @ (none @ TA)) | ? [B:TA]: (A @ (some @ TA @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_split__option__ex)).
% 277.20/240.55  thf(926,plain,((! [TA: $tType]: (((?) @ (option @ TA)) = (^ [A:((option @ TA) > $o)]: ((A @ (none @ TA)) | ? [B:TA]: (A @ (some @ TA @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 277.20/240.55  thf(187,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:variable]: ((accp @ (product_prod @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm)) @ uSubst2096773001pt_rel @ (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ A @ (product_Pair @ (set @ variable) @ trm @ B @ (var @ C)))) => ((uSubst95898992stappt @ A @ B @ (var @ C)) = (some @ trm @ (var @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_183_usubstappt_Opsimps_I1_J)).
% 277.20/240.55  thf(1135,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:variable]: ((accp @ (product_prod @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm)) @ (uSubst2096773001pt_rel) @ (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ A @ (product_Pair @ (set @ variable) @ trm @ B @ (var @ C)))) => ((uSubst95898992stappt @ A @ B @ (var @ C)) = (some @ trm @ (var @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 277.20/240.55  thf(146,axiom,((! [A:((option @ trm) > $o),B:(option @ trm)]: ((! [C:trm]: (A @ (some @ trm @ C))) => ((A @ (none @ trm)) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_Differentialo_Oinduct)).
% 277.20/240.55  thf(824,plain,((! [A:((option @ trm) > $o),B:(option @ trm)]: ((! [C:trm]: (A @ (some @ trm @ C))) => ((A @ (none @ trm)) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 277.20/240.55  thf(224,axiom,((! [A:trm]: ((uSubst1556497037e_Geqo @ (some @ trm @ A) @ (none @ trm)) = (none @ fml)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_118_Geqo_Osimps_I3_J)).
% 277.20/240.55  thf(1374,plain,((! [A:trm]: ((uSubst1556497037e_Geqo @ (some @ trm @ A) @ (none @ trm)) = (none @ fml)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 277.20/240.55  thf(136,axiom,((! [TA: $tType,TB: $tType]: ((case_option @ TA @ TB) = (^ [A:TA,B:(TB > TA),C:(option @ TB)]: (if @ TA @ (C = (none @ TB)) @ A @ (B @ (the @ TB @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_169_option_Ocase__eq__if)).
% 277.20/240.55  thf(743,plain,((! [TA: $tType,TB: $tType]: ((case_option @ TA @ TB) = (^ [A:TA,B:(TB > TA),C:(option @ TB)]: (if @ TA @ (C = (none @ TB)) @ A @ (B @ (the @ TB @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 277.20/240.55  thf(164,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:char]: ((accp @ (product_prod @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm)) @ uSubst2096773001pt_rel @ (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ A @ (product_Pair @ (set @ variable) @ trm @ B @ (const @ C)))) => ((uSubst95898992stappt @ A @ B @ (const @ C)) = (uSubst1138577137pconst @ A @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_216_usubstappt_Opsimps_I3_J)).
% 277.20/240.55  thf(958,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:char]: ((accp @ (product_prod @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm)) @ (uSubst2096773001pt_rel) @ (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ A @ (product_Pair @ (set @ variable) @ trm @ B @ (const @ C)))) => ((uSubst95898992stappt @ A @ B @ (const @ C)) = (uSubst1138577137pconst @ A @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 277.20/240.55  thf(88,axiom,((! [TA: $tType]: ((top_top @ (set @ TA)) = (collect @ TA @ (^ [A:TA]: (($true))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_244_UNIV__def)).
% 277.20/240.55  thf(545,plain,((! [TA: $tType]: ((top_top @ (set @ TA)) = (collect @ TA @ (^ [A:TA]: (($true))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 277.20/240.55  thf(51,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > (TA > $o)),C:TA,D:(TA > $o)]: ((ord_less_eq @ (TA > $o) @ A @ (accp @ TA @ B)) => ((! [E:TA,F:TA]: ((A @ E) => ((B @ F @ E) => (A @ F)))) => ((A @ C) => ((! [E:TA]: ((A @ E) => ((! [F:TA]: ((B @ F @ E) => (D @ F))) => (D @ E)))) => (D @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_132_accp__subset__induct)).
% 277.20/240.55  thf(413,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > (TA > $o)),C:TA,D:(TA > $o)]: ((ord_less_eq @ (TA > $o) @ (A) @ (accp @ TA @ B)) => ((! [E:TA,F:TA]: ((A @ E) => ((B @ F @ E) => (A @ F)))) => ((A @ C) => ((! [E:TA]: ((A @ E) => ((! [F:TA]: ((B @ F @ E) => (D @ F))) => (D @ E)))) => (D @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 277.20/240.55  thf(119,axiom,((! [A:variable,B:variable]: (((var @ A) = (var @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_trm_Oinject_I1_J)).
% 277.20/240.55  thf(641,plain,((! [A:variable,B:variable]: (((var @ A) = (var @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 277.20/240.55  thf(58,axiom,((! [TA: $tType]: (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((accp @ TA @ A @ B) => ((A @ C @ B) => (accp @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_151_accp__downward)).
% 277.20/240.55  thf(445,plain,((! [TA: $tType]: (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((accp @ TA @ (A) @ B) => ((A @ C @ B) => (accp @ TA @ (A) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 277.20/240.55  thf(98,axiom,((! [TA: $tType,TB: $tType]: ((bNF_Gr2107612801vImage @ TA @ TB) = (^ [A:(set @ TA),B:(set @ (product_prod @ TB @ TB)),C:(TA > TB)]: (collect @ (product_prod @ TA @ TA) @ (^ [D:(product_prod @ TA @ TA)]: ? [E:TA,F:TA]: ((D = (product_Pair @ TA @ TA @ E @ F)) & (member @ TA @ E @ A) & (member @ TA @ F @ A) & (member @ (product_prod @ TB @ TB) @ (product_Pair @ TB @ TB @ (C @ E) @ (C @ F)) @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_227_relInvImage__def)).
% 277.20/240.55  thf(572,plain,((! [TA: $tType,TB: $tType]: ((bNF_Gr2107612801vImage @ TA @ TB) = (^ [A:(set @ TA),B:(set @ (product_prod @ TB @ TB)),C:(TA > TB)]: (collect @ (product_prod @ TA @ TA) @ (^ [D:(product_prod @ TA @ TA)]: ? [E:TA,F:TA]: ((D = (product_Pair @ TA @ TA @ E @ F)) & (member @ TA @ E @ A) & (member @ TA @ F @ A) & (member @ (product_prod @ TB @ TB) @ (product_Pair @ TB @ TB @ (C @ E) @ (C @ F)) @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 277.20/240.55  thf(24,axiom,((! [TA: $tType,TB: $tType]: ((top_top @ (TA > (TB > $o))) = (^ [A:TA,B:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ A @ B) @ (top_top @ (set @ (product_prod @ TA @ TB)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_251_top__empty__eq2)).
% 277.20/240.55  thf(313,plain,((! [TA: $tType,TB: $tType]: ((top_top @ (TA > (TB > $o))) = (^ [A:TA,B:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ A @ B) @ (top_top @ (set @ (product_prod @ TA @ TB)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 277.20/240.55  thf(204,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: (((uSubst95898978stappf @ A @ B @ (geq @ C @ D)) != (none @ fml)) => (((uSubst95898992stappt @ A @ B @ C) != (none @ trm)) & ((uSubst95898992stappt @ A @ B @ D) != (none @ trm)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_usubstappf__geq__conv)).
% 277.20/240.55  thf(1271,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: ((~ ((uSubst95898978stappf @ A @ B @ (geq @ C @ D)) = (none @ fml))) => (~ ((uSubst95898992stappt @ A @ B @ C) = (none @ trm)) & ~ ((uSubst95898992stappt @ A @ B @ D) = (none @ trm)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 277.20/240.55  thf(108,axiom,((! [A:fml,B:char,C:trm]: ((test @ A) != (ode @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_254_game_Odistinct_I35_J)).
% 277.20/240.55  thf(611,plain,((! [A:fml,B:char,C:trm]: ~ ((test @ A) = (ode @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 277.20/240.55  thf(31,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((ord_less_eq @ (set @ TA) @ A @ (collect @ TA @ (^ [D:TA]: ((member @ TA @ D @ B) & (C @ D))))) = (! [D:TA]: ((member @ TA @ D @ A) => (C @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_subset__Collect__iff)).
% 277.20/240.55  thf(335,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((ord_less_eq @ (set @ TA) @ A @ (collect @ TA @ (^ [D:TA]: ((member @ TA @ D @ B) & (C @ D))))) = (! [D:TA]: ((member @ TA @ D @ A) => (C @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 277.20/240.55  thf(178,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((! [B:TA]: (A != (some @ TA @ B))) = (A = (none @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_not__Some__eq)).
% 277.20/240.55  thf(1090,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ((! [B:TA]: ~ (A = (some @ TA @ B))) = (A = (none @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 277.20/240.55  thf(200,axiom,((! [A:variable,B:trm]: ((uSubst1326326671ssigno @ A @ (some @ trm @ B)) = (some @ game @ (assign @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_235_Assigno_Osimps_I1_J)).
% 277.20/240.55  thf(1258,plain,((! [A:variable,B:trm]: ((uSubst1326326671ssigno @ A @ (some @ trm @ B)) = (some @ game @ (assign @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 277.20/240.55  thf(36,axiom,((! [TA: $tType,TB: $tType]: (! [A:$o,B:(TA > $o),C:(option @ TA),D:(TB > $o),E:TB,F:(TA > TB)]: ((case_option @ $o @ TA @ A @ B @ C) => (((A) => (D @ E)) => ((! [G:TA]: ((B @ G) => (D @ (F @ G)))) => (D @ (case_option @ TB @ TA @ E @ F @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_174_disjE__realizer2)).
% 277.20/240.55  thf(350,plain,((! [TA: $tType,TB: $tType]: (! [A:$o,B:(TA > $o),C:(option @ TA),D:(TB > $o),E:TB,F:(TA > TB)]: ((case_option @ $o @ TA @ A @ (B) @ C) => (((A) => (D @ E)) => ((! [G:TA]: ((B @ G) => (D @ (F @ G)))) => (D @ (case_option @ TB @ TA @ E @ (F) @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 277.20/240.55  thf(105,axiom,((! [TA: $tType]: (! [A:(TA > (TA > $o)),B:(TA > (TA > $o))]: ((ord_less_eq @ (TA > (TA > $o)) @ A @ B) => (ord_less_eq @ (TA > $o) @ (accp @ TA @ B) @ (accp @ TA @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_accp__subset)).
% 277.20/240.55  thf(604,plain,((! [TA: $tType]: (! [A:(TA > (TA > $o)),B:(TA > (TA > $o))]: ((ord_less_eq @ (TA > (TA > $o)) @ (A) @ (B)) => (ord_less_eq @ (TA > $o) @ (accp @ TA @ B) @ (accp @ TA @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 277.20/240.55  thf(148,axiom,((! [A:variable]: ((uSubst1326326671ssigno @ A @ (none @ trm)) = (none @ game)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_Assigno_Osimps_I2_J)).
% 277.20/240.55  thf(831,plain,((! [A:variable]: ((uSubst1326326671ssigno @ A @ (none @ trm)) = (none @ game)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 277.20/240.55  thf(129,axiom,((! [TA: $tType]: ((ord_less_eq @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: ! [C:TA]: ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_subset__iff)).
% 277.20/240.55  thf(681,plain,((! [TA: $tType]: ((ord_less_eq @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: ! [C:TA]: ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 277.20/240.55  thf(96,axiom,((! [A:variable,B:real]: ((var @ A) != (number @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_194_trm_Odistinct_I1_J)).
% 277.20/240.55  thf(567,plain,((! [A:variable,B:real]: ~ ((var @ A) = (number @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 277.20/240.55  thf(190,axiom,((! [A:(option @ trm),B:(option @ trm),C:(option @ trm)]: (((uSubst1112714340_Pluso @ A @ B) = C) => ((! [D:trm]: ((A = (some @ trm @ D)) => (! [E:trm]: ((B = (some @ trm @ E)) => (C != (some @ trm @ (plus @ D @ E))))))) => (((A = (none @ trm)) => (C != (none @ trm))) => (~ ((? [D:trm]: (A = (some @ trm @ D))) => ((B = (none @ trm)) => (C != (none @ trm)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_Pluso_Oelims)).
% 277.20/240.55  thf(1144,plain,((! [A:(option @ trm),B:(option @ trm),C:(option @ trm)]: (((uSubst1112714340_Pluso @ A @ B) = C) => ((! [D:trm]: ((A = (some @ trm @ D)) => (! [E:trm]: ((B = (some @ trm @ E)) => (~ (C = (some @ trm @ (plus @ D @ E)))))))) => (((A = (none @ trm)) => (~ (C = (none @ trm)))) => (~ ((? [D:trm]: (A = (some @ trm @ D))) => ((B = (none @ trm)) => (~ (C = (none @ trm))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 277.20/240.55  thf(3,axiom,((! [TA: $tType]: ((order_top @ TA) => (! [A:TA]: ((ord_less_eq @ TA @ (top_top @ TA) @ A) => (A = (top_top @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_243_top_Oextremum__uniqueI)).
% 277.20/240.55  thf(245,plain,((! [TA: $tType]: ((order_top @ TA) => (! [A:TA]: ((ord_less_eq @ TA @ (top_top @ TA) @ A) => (A = (top_top @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 277.20/240.55  thf(26,axiom,((! [A:char,B:trm,C:trm,D:trm]: ((func @ A @ B) != (plus @ C @ D)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_212_trm_Odistinct_I31_J)).
% 277.20/240.55  thf(318,plain,((! [A:char,B:trm,C:trm,D:trm]: ~ ((func @ A @ B) = (plus @ C @ D)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 277.20/240.55  thf(20,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: (ord_less_eq @ (set @ TA) @ A @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_subset__refl)).
% 277.20/240.55  thf(303,plain,((! [TA: $tType]: (! [A:(set @ TA)]: (ord_less_eq @ (set @ TA) @ A @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 277.20/240.55  thf(79,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((A = B) => (~ ((ord_less_eq @ (set @ TA) @ A @ B) => (~ (ord_less_eq @ (set @ TA) @ B @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_equalityE)).
% 277.20/240.55  thf(509,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((A = B) => (~ ((ord_less_eq @ (set @ TA) @ A @ B) => (~ (ord_less_eq @ (set @ TA) @ B @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 277.20/240.55  thf(55,axiom,((! [A:real,B:char]: ((number @ A) != (const @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_204_trm_Odistinct_I13_J)).
% 277.20/240.55  thf(434,plain,((! [A:real,B:char]: ~ ((number @ A) = (const @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 277.20/240.55  thf(71,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((! [C:TA]: ((member @ TA @ C @ A) => (member @ TA @ C @ B))) => (ord_less_eq @ (set @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_subsetI)).
% 277.20/240.55  thf(477,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((! [C:TA]: ((member @ TA @ C @ A) => (member @ TA @ C @ B))) => (ord_less_eq @ (set @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 277.20/240.55  thf(43,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > $o),C:(TA > $o)]: ((ord_less_eq @ (set @ TA) @ A @ (collect @ TA @ (^ [D:TA]: ((B @ D) & (C @ D))))) = ((ord_less_eq @ (set @ TA) @ A @ (collect @ TA @ B)) & (ord_less_eq @ (set @ TA) @ A @ (collect @ TA @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_conj__subset__def)).
% 277.20/240.55  thf(387,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > $o),C:(TA > $o)]: ((ord_less_eq @ (set @ TA) @ A @ (collect @ TA @ (^ [D:TA]: ((B @ D) & (C @ D))))) = ((ord_less_eq @ (set @ TA) @ A @ (collect @ TA @ (B))) & (ord_less_eq @ (set @ TA) @ A @ (collect @ TA @ (C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 277.20/240.55  thf(75,axiom,((! [TA: $tType]: (! [A:(TA > (TA > $o)),B:TA,C:(TA > $o)]: ((accp @ TA @ A @ B) => ((! [D:TA]: ((accp @ TA @ A @ D) => ((! [E:TA]: ((A @ E @ D) => (C @ E))) => (C @ D)))) => (C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_149_accp__induct)).
% 277.20/240.55  thf(494,plain,((! [TA: $tType]: (! [A:(TA > (TA > $o)),B:TA,C:(TA > $o)]: ((accp @ TA @ (A) @ B) => ((! [D:TA]: ((accp @ TA @ (A) @ D) => ((! [E:TA]: ((A @ E @ D) => (C @ E))) => (C @ D)))) => (C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 277.20/240.55  thf(34,axiom,((! [A:real,B:trm]: ((number @ A) != (differential @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_trm_Odistinct_I21_J)).
% 277.20/240.55  thf(345,plain,((! [A:real,B:trm]: ~ ((number @ A) = (differential @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 277.20/240.55  thf(85,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TA > $o)),B:(TB > (TA > $o)),C:$o,D:TB,E:TA]: (((ord_less_eq @ (TB > (TA > $o)) @ A @ B) & (C)) => ((C) & ((A @ D @ E) => (B @ D @ E))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_170_predicate2D__conj)).
% 277.20/240.55  thf(535,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TA > $o)),B:(TB > (TA > $o)),C:$o,D:TB,E:TA]: (((ord_less_eq @ (TB > (TA > $o)) @ (A) @ (B)) & (C)) => ((C) & ((A @ D @ E) => (B @ D @ E))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 277.20/240.55  thf(166,axiom,((! [A:(option @ trm),B:(option @ trm)]: (((uSubst1556497037e_Geqo @ A @ B) = (none @ fml)) = ((A = (none @ trm)) | (B = (none @ trm)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_Geqo__undef)).
% 277.20/240.55  thf(964,plain,((! [A:(option @ trm),B:(option @ trm)]: (((uSubst1556497037e_Geqo @ A @ B) = (none @ fml)) = ((A = (none @ trm)) | (B = (none @ trm)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 277.20/240.55  thf(215,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:(set @ variable)]: (((uSubst95898992stappt @ A @ B @ C) != (none @ trm)) => (((uSubst95898992stappt @ A @ D @ C) != (none @ trm)) => ((uSubst95898992stappt @ A @ B @ C) = (uSubst95898992stappt @ A @ D @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_usubstappt__det)).
% 277.20/240.55  thf(1344,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:(set @ variable)]: ((~ ((uSubst95898992stappt @ A @ B @ C) = (none @ trm))) => ((~ ((uSubst95898992stappt @ A @ D @ C) = (none @ trm))) => ((uSubst95898992stappt @ A @ B @ C) = (uSubst95898992stappt @ A @ D @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 277.20/240.55  thf(65,axiom,((! [A:fml,B:fml]: (((test @ A) = (test @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_221_game_Oinject_I3_J)).
% 277.20/240.55  thf(462,plain,((! [A:fml,B:fml]: (((test @ A) = (test @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 277.20/240.55  thf(153,axiom,((! [A:(option @ trm),B:(option @ trm),C:(option @ trm)]: (((uSubst1112714340_Pluso @ A @ B) = C) => ((accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ uSubst270600597so_rel @ (product_Pair @ (option @ trm) @ (option @ trm) @ A @ B)) => ((! [D:trm]: ((A = (some @ trm @ D)) => (! [E:trm]: ((B = (some @ trm @ E)) => ((C = (some @ trm @ (plus @ D @ E))) => (~ (accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ uSubst270600597so_rel @ (product_Pair @ (option @ trm) @ (option @ trm) @ (some @ trm @ D) @ (some @ trm @ E))))))))) => (((A = (none @ trm)) => ((C = (none @ trm)) => (~ (accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ uSubst270600597so_rel @ (product_Pair @ (option @ trm) @ (option @ trm) @ (none @ trm) @ B))))) => (~ (! [D:trm]: ((A = (some @ trm @ D)) => ((B = (none @ trm)) => ((C = (none @ trm)) => (~ (accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ uSubst270600597so_rel @ (product_Pair @ (option @ trm) @ (option @ trm) @ (some @ trm @ D) @ (none @ trm))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_173_Pluso_Opelims)).
% 277.20/240.55  thf(848,plain,((! [A:(option @ trm),B:(option @ trm),C:(option @ trm)]: (((uSubst1112714340_Pluso @ A @ B) = C) => ((accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ (uSubst270600597so_rel) @ (product_Pair @ (option @ trm) @ (option @ trm) @ A @ B)) => ((! [D:trm]: ((A = (some @ trm @ D)) => (! [E:trm]: ((B = (some @ trm @ E)) => ((C = (some @ trm @ (plus @ D @ E))) => (~ (accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ (uSubst270600597so_rel) @ (product_Pair @ (option @ trm) @ (option @ trm) @ (some @ trm @ D) @ (some @ trm @ E))))))))) => (((A = (none @ trm)) => ((C = (none @ trm)) => (~ (accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ (uSubst270600597so_rel) @ (product_Pair @ (option @ trm) @ (option @ trm) @ (none @ trm) @ B))))) => (~ (! [D:trm]: ((A = (some @ trm @ D)) => ((B = (none @ trm)) => ((C = (none @ trm)) => (~ (accp @ (product_prod @ (option @ trm) @ (option @ trm)) @ (uSubst270600597so_rel) @ (product_Pair @ (option @ trm) @ (option @ trm) @ (some @ trm @ D) @ (none @ trm))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 277.20/240.55  thf(81,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((A = B) => (ord_less_eq @ (set @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_equalityD1)).
% 277.20/240.55  thf(520,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((A = B) => (ord_less_eq @ (set @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 277.20/240.55  thf(114,axiom,((! [A:char,B:trm,C:trm]: ((const @ A) != (times @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_208_trm_Odistinct_I27_J)).
% 277.20/240.55  thf(626,plain,((! [A:char,B:trm,C:trm]: ~ ((const @ A) = (times @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 277.20/240.55  thf(159,axiom,((! [A:(option @ trm),B:(option @ trm)]: (((uSubst1112714340_Pluso @ A @ B) = (none @ trm)) = ((A = (none @ trm)) | (B = (none @ trm)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_Pluso__undef)).
% 277.20/240.55  thf(915,plain,((! [A:(option @ trm),B:(option @ trm)]: (((uSubst1112714340_Pluso @ A @ B) = (none @ trm)) = ((A = (none @ trm)) | (B = (none @ trm)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 277.20/240.55  thf(192,axiom,((! [A:(variable > ((option @ fml) > $o)),B:variable,C:(option @ fml)]: ((! [D:variable,E:fml]: (A @ D @ (some @ fml @ E))) => ((! [D:variable]: (A @ D @ (none @ fml))) => (A @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_126_Existso_Oinduct)).
% 277.20/240.55  thf(1177,plain,((! [A:(variable > ((option @ fml) > $o)),B:variable,C:(option @ fml)]: ((! [D:variable,E:fml]: (A @ D @ (some @ fml @ E))) => ((! [D:variable]: (A @ D @ (none @ fml))) => (A @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 277.20/240.55  thf(227,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:real]: ((accp @ (product_prod @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm)) @ uSubst2096773001pt_rel @ (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ A @ (product_Pair @ (set @ variable) @ trm @ B @ (number @ C)))) => ((uSubst95898992stappt @ A @ B @ (number @ C)) = (some @ trm @ (number @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_184_usubstappt_Opsimps_I2_J)).
% 277.20/240.55  thf(1381,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:real]: ((accp @ (product_prod @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm)) @ (uSubst2096773001pt_rel) @ (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ A @ (product_Pair @ (set @ variable) @ trm @ B @ (number @ C)))) => ((uSubst95898992stappt @ A @ B @ (number @ C)) = (some @ trm @ (number @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 277.20/240.55  thf(158,axiom,((! [A:(option @ fml)]: (((uSubst190403692_Testo @ A) = (none @ game)) = (A = (none @ fml))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_199_Testo__undef)).
% 277.20/240.55  thf(912,plain,((! [A:(option @ fml)]: (((uSubst190403692_Testo @ A) = (none @ game)) = (A = (none @ fml))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 277.20/240.55  thf(107,axiom,((! [TA: $tType]: (((=) @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) & (ord_less_eq @ (set @ TA) @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_64_set__eq__subset)).
% 277.20/240.55  thf(608,plain,((! [TA: $tType]: (((=) @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) & (ord_less_eq @ (set @ TA) @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 277.20/240.55  thf(95,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TB > $o)),B:(TA > (TB > $o))]: ((! [C:TA,D:TB]: ((A @ C @ D) => (B @ C @ D))) => (ord_less_eq @ (TA > (TB > $o)) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_135_predicate2I)).
% 277.20/240.55  thf(563,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TB > $o)),B:(TA > (TB > $o))]: ((! [C:TA,D:TB]: ((A @ C @ D) => (B @ C @ D))) => (ord_less_eq @ (TA > (TB > $o)) @ (A) @ (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 277.20/240.55  thf(18,axiom,((! [TA: $tType]: ((order_top @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ (top_top @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_241_top__greatest)).
% 277.20/240.55  thf(299,plain,((! [TA: $tType]: ((order_top @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ (top_top @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 277.20/240.55  thf(221,axiom,((! [A:trm]: ((uSubst1112714340_Pluso @ (some @ trm @ A) @ (none @ trm)) = (none @ trm)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_Pluso_Osimps_I3_J)).
% 277.20/240.55  thf(1364,plain,((! [A:trm]: ((uSubst1112714340_Pluso @ (some @ trm @ A) @ (none @ trm)) = (none @ trm)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 277.20/240.55  thf(182,axiom,((! [A:(product_prod @ denotational_interp @ trm)]: ((! [B:denotational_interp,C:variable]: (A != (product_Pair @ denotational_interp @ trm @ B @ (var @ C)))) => ((! [B:denotational_interp,C:real]: (A != (product_Pair @ denotational_interp @ trm @ B @ (number @ C)))) => ((! [B:denotational_interp,C:char]: (A != (product_Pair @ denotational_interp @ trm @ B @ (const @ C)))) => ((! [B:denotational_interp,C:char,D:trm]: (A != (product_Pair @ denotational_interp @ trm @ B @ (func @ C @ D)))) => ((! [B:denotational_interp,C:trm,D:trm]: (A != (product_Pair @ denotational_interp @ trm @ B @ (plus @ C @ D)))) => ((! [B:denotational_interp,C:trm,D:trm]: (A != (product_Pair @ denotational_interp @ trm @ B @ (times @ C @ D)))) => (~ (! [B:denotational_interp,C:trm]: (A != (product_Pair @ denotational_interp @ trm @ B @ (differential @ C))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_term__sem_Ocases)).
% 277.20/240.55  thf(1102,plain,((! [A:(product_prod @ denotational_interp @ trm)]: ((! [B:denotational_interp,C:variable]: ~ (A = (product_Pair @ denotational_interp @ trm @ B @ (var @ C)))) => ((! [B:denotational_interp,C:real]: ~ (A = (product_Pair @ denotational_interp @ trm @ B @ (number @ C)))) => ((! [B:denotational_interp,C:char]: ~ (A = (product_Pair @ denotational_interp @ trm @ B @ (const @ C)))) => ((! [B:denotational_interp,C:char,D:trm]: ~ (A = (product_Pair @ denotational_interp @ trm @ B @ (func @ C @ D)))) => ((! [B:denotational_interp,C:trm,D:trm]: ~ (A = (product_Pair @ denotational_interp @ trm @ B @ (plus @ C @ D)))) => ((! [B:denotational_interp,C:trm,D:trm]: ~ (A = (product_Pair @ denotational_interp @ trm @ B @ (times @ C @ D)))) => (~ (! [B:denotational_interp,C:trm]: ~ (A = (product_Pair @ denotational_interp @ trm @ B @ (differential @ C))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 277.20/240.55  thf(56,axiom,((! [A:real,B:char,C:trm]: ((number @ A) != (func @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_205_trm_Odistinct_I15_J)).
% 277.20/240.55  thf(438,plain,((! [A:real,B:char,C:trm]: ~ ((number @ A) = (func @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 277.20/240.55  thf(161,axiom,((! [A:(set @ variable),B:(set @ variable),C:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),D:trm]: ((ord_less_eq @ (set @ variable) @ A @ B) => (((uSubst95898992stappt @ C @ B @ D) != (none @ trm)) => ((uSubst95898992stappt @ C @ B @ D) = (uSubst95898992stappt @ C @ A @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_usubstappt__antimon)).
% 277.20/240.55  thf(922,plain,((! [A:(set @ variable),B:(set @ variable),C:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),D:trm]: ((ord_less_eq @ (set @ variable) @ A @ B) => ((~ ((uSubst95898992stappt @ C @ B @ D) = (none @ trm))) => ((uSubst95898992stappt @ C @ B @ D) = (uSubst95898992stappt @ C @ A @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 277.20/240.55  thf(117,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o),C:TA]: ((ord_less_eq @ (TA > $o) @ A @ B) => ((A @ C) => (B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_predicate1D)).
% 277.20/240.55  thf(636,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o),C:TA]: ((ord_less_eq @ (TA > $o) @ (A) @ (B)) => ((A @ C) => (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 277.20/240.55  thf(198,axiom,((! [TA: $tType]: (! [A:(option @ TA),B:(option @ TA)]: (((A = (none @ TA)) = (B = (none @ TA))) => (((A != (none @ TA)) => ((B != (none @ TA)) => ((the @ TA @ A) = (the @ TA @ B)))) => (A = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_143_option_Oexpand)).
% 277.20/240.55  thf(1245,plain,((! [TA: $tType]: (! [A:(option @ TA),B:(option @ TA)]: (((A = (none @ TA)) = (B = (none @ TA))) => (((~ (A = (none @ TA))) => ((~ (B = (none @ TA))) => ((the @ TA @ A) = (the @ TA @ B)))) => (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 277.20/240.55  thf(9,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) => (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_le__cases)).
% 277.20/240.55  thf(278,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) => (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 277.20/240.55  thf(240,axiom,(((uSubst190403692_Testo @ (none @ fml)) = (none @ game))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_198_Testo_Osimps_I2_J)).
% 277.20/240.55  thf(1445,plain,(((uSubst190403692_Testo @ (none @ fml)) = (none @ game))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 277.20/240.55  thf(69,axiom,((! [A:(variable > real),B:(variable > real)]: (denota1419872369iation @ A @ B @ (collect @ variable @ (^ [C:variable]: (($true))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_Uvariation__univ)).
% 277.20/240.55  thf(473,plain,((! [A:(variable > real),B:(variable > real)]: (denota1419872369iation @ (A) @ (B) @ (collect @ variable @ (^ [C:variable]: (($true))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 277.20/240.55  thf(74,axiom,((! [A:char,B:char,C:trm]: ((const @ A) != (func @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_trm_Odistinct_I23_J)).
% 277.20/240.55  thf(490,plain,((! [A:char,B:char,C:trm]: ~ ((const @ A) = (func @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 277.20/240.55  thf(52,axiom,((! [TA: $tType]: (top @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Otop_4)).
% 277.20/240.55  thf(426,plain,((! [TA: $tType]: (top @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 277.20/240.55  thf(84,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((A = B) => (ord_less_eq @ (set @ TA) @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_equalityD2)).
% 277.20/240.55  thf(531,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((A = B) => (ord_less_eq @ (set @ TA) @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 277.20/240.55  thf(89,axiom,((! [TA: $tType,TB: $tType]: (! [A:(set @ (product_prod @ TA @ TB)),B:(set @ (product_prod @ TA @ TB))]: ((ord_less_eq @ (TA > (TB > $o)) @ (^ [C:TA,D:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ A)) @ (^ [C:TA,D:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ B))) = (ord_less_eq @ (set @ (product_prod @ TA @ TB)) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_163_pred__subset__eq2)).
% 277.20/240.55  thf(548,plain,((! [TA: $tType,TB: $tType]: (! [A:(set @ (product_prod @ TA @ TB)),B:(set @ (product_prod @ TA @ TB))]: ((ord_less_eq @ (TA > (TB > $o)) @ (^ [C:TA,D:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ A)) @ (^ [C:TA,D:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ B))) = (ord_less_eq @ (set @ (product_prod @ TA @ TB)) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 277.20/240.55  thf(205,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > $o),B:TB,C:(TA > TB),D:(option @ TA)]: ((A @ (case_option @ TB @ TA @ B @ C @ D)) = (~ (((D = (none @ TA)) & ~ (A @ B)) | ((D = (some @ TA @ (the @ TA @ D))) & ~ (A @ (C @ (the @ TA @ D)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_171_option_Osplit__sel__asm)).
% 277.20/240.55  thf(1277,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > $o),B:TB,C:(TA > TB),D:(option @ TA)]: ((A @ (case_option @ TB @ TA @ B @ (C) @ D)) = (~ (((D = (none @ TA)) & ~ (A @ B)) | ((D = (some @ TA @ (the @ TA @ D))) & ~ (A @ (C @ (the @ TA @ D)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 277.20/240.55  thf(110,axiom,((! [A:fml]: ((uSubst190403692_Testo @ (some @ fml @ A)) = (some @ game @ (test @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_223_Testo_Osimps_I1_J)).
% 277.20/240.55  thf(617,plain,((! [A:fml]: ((uSubst190403692_Testo @ (some @ fml @ A)) = (some @ game @ (test @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 277.20/240.55  thf(33,axiom,((! [A:variable,B:trm,C:variable,D:trm]: (((assign @ A @ B) = (assign @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_233_game_Oinject_I2_J)).
% 277.20/240.55  thf(342,plain,((! [A:variable,B:trm,C:variable,D:trm]: (((assign @ A @ B) = (assign @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 277.20/240.55  thf(145,axiom,(((none @ trm) = (none @ trm))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_undeft__None)).
% 277.20/240.55  thf(823,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 277.20/240.55  thf(176,axiom,((! [TA: $tType]: (((!) @ (option @ TA)) = (^ [A:((option @ TA) > $o)]: ((A @ (none @ TA)) & ! [B:TA]: (A @ (some @ TA @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_split__option__all)).
% 277.20/240.55  thf(1081,plain,((! [TA: $tType]: (((!) @ (option @ TA)) = (^ [A:((option @ TA) > $o)]: ((A @ (none @ TA)) & ! [B:TA]: (A @ (some @ TA @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 277.20/240.55  thf(138,axiom,((! [A:trm,B:trm]: ((uSubst1112714340_Pluso @ (some @ trm @ A) @ (some @ trm @ B)) = (some @ trm @ (plus @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_115_Pluso_Osimps_I1_J)).
% 277.20/240.55  thf(749,plain,((! [A:trm,B:trm]: ((uSubst1112714340_Pluso @ (some @ trm @ A) @ (some @ trm @ B)) = (some @ trm @ (plus @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 277.20/240.55  thf(16,axiom,((! [TA: $tType]: (! [A:TA]: (member @ TA @ A @ (top_top @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_239_UNIV__I)).
% 277.20/240.55  thf(295,plain,((! [TA: $tType]: (! [A:TA]: (member @ TA @ A @ (top_top @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 277.20/240.55  thf(11,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_Collect__mem__eq)).
% 277.20/240.55  thf(282,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 277.20/240.55  thf(203,axiom,((! [A:(product_prod @ variable @ (option @ trm))]: ((! [B:variable,C:trm]: (A != (product_Pair @ variable @ (option @ trm) @ B @ (some @ trm @ C)))) => (~ (! [B:variable]: (A != (product_Pair @ variable @ (option @ trm) @ B @ (none @ trm)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_176_Assigno_Ocases)).
% 277.20/240.55  thf(1267,plain,((! [A:(product_prod @ variable @ (option @ trm))]: ((! [B:variable,C:trm]: ~ (A = (product_Pair @ variable @ (option @ trm) @ B @ (some @ trm @ C)))) => (~ (! [B:variable]: ~ (A = (product_Pair @ variable @ (option @ trm) @ B @ (none @ trm)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 277.20/240.55  thf(143,axiom,((! [A:(option @ trm)]: (((uSubst259074819ntialo @ A) = (none @ trm)) = (A = (none @ trm))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_Differentialo__undef)).
% 277.20/240.55  thf(791,plain,((! [A:(option @ trm)]: (((uSubst259074819ntialo @ A) = (none @ trm)) = (A = (none @ trm))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 277.20/240.55  thf(194,axiom,((! [A:(option @ fml)]: ((A != (none @ fml)) = (? [B:fml]: (A = (some @ fml @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_undeff__equiv)).
% 277.20/240.55  thf(1186,plain,((! [A:(option @ fml)]: ((~ (A = (none @ fml))) = (? [B:fml]: (A = (some @ fml @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 277.20/240.55  thf(32,axiom,((! [TA: $tType,TB: $tType]: (! [A:(set @ (product_prod @ TA @ TB)),B:(set @ (product_prod @ TA @ TB))]: ((! [C:TA,D:TB]: ((member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ A) => (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ B))) => (ord_less_eq @ (set @ (product_prod @ TA @ TB)) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_158_subrelI)).
% 277.20/240.55  thf(338,plain,((! [TA: $tType,TB: $tType]: (! [A:(set @ (product_prod @ TA @ TB)),B:(set @ (product_prod @ TA @ TB))]: ((! [C:TA,D:TB]: ((member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ A) => (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ B))) => (ord_less_eq @ (set @ (product_prod @ TA @ TB)) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 277.20/240.55  thf(189,axiom,((! [A:(option @ trm),B:(option @ trm)]: (((uSubst277968634Timeso @ A @ B) = (none @ trm)) = ((A = (none @ trm)) | (B = (none @ trm)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_Timeso__undef)).
% 277.20/240.55  thf(1141,plain,((! [A:(option @ trm),B:(option @ trm)]: (((uSubst277968634Timeso @ A @ B) = (none @ trm)) = ((A = (none @ trm)) | (B = (none @ trm)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 277.20/240.55  thf(124,axiom,((! [TA: $tType]: (! [A:(TA > (TA > $o)),B:TA,C:(TA > $o)]: ((accp @ TA @ A @ B) => ((! [D:TA]: ((! [E:TA]: ((A @ E @ D) => (accp @ TA @ A @ E))) => ((! [E:TA]: ((A @ E @ D) => (C @ E))) => (C @ D)))) => (C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_150_accp_Oinducts)).
% 277.20/240.55  thf(656,plain,((! [TA: $tType]: (! [A:(TA > (TA > $o)),B:TA,C:(TA > $o)]: ((accp @ TA @ (A) @ B) => ((! [D:TA]: ((! [E:TA]: ((A @ E @ D) => (accp @ TA @ (A) @ E))) => ((! [E:TA]: ((A @ E @ D) => (C @ E))) => (C @ D)))) => (C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 277.20/240.55  thf(170,axiom,((! [A:(option @ game)]: ((A != (none @ game)) = (? [B:game]: (A = (some @ game @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_undefg__equiv)).
% 277.20/240.55  thf(978,plain,((! [A:(option @ game)]: ((~ (A = (none @ game))) = (? [B:game]: (A = (some @ game @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 277.20/240.55  thf(97,axiom,((! [A:$o]: ((A = ($true)) | (A = ($false))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_3_1_T)).
% 277.20/240.55  thf(571,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 277.20/240.55  thf(102,axiom,((! [A:char,B:char]: (((const @ A) = (const @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_201_trm_Oinject_I3_J)).
% 277.20/240.55  thf(595,plain,((! [A:char,B:char]: (((const @ A) = (const @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 277.20/240.55  thf(193,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: (((uSubst95898992stappt @ A @ B @ (times @ C @ D)) != (none @ trm)) => (((uSubst95898992stappt @ A @ B @ C) != (none @ trm)) & ((uSubst95898992stappt @ A @ B @ D) != (none @ trm)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_usubstappt__times__conv)).
% 277.20/240.55  thf(1180,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: ((~ ((uSubst95898992stappt @ A @ B @ (times @ C @ D)) = (none @ trm))) => (~ ((uSubst95898992stappt @ A @ B @ C) = (none @ trm)) & ~ ((uSubst95898992stappt @ A @ B @ D) = (none @ trm)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 277.20/240.55  thf(86,axiom,((! [A:trm,B:trm,C:trm]: ((plus @ A @ B) != (differential @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_112_trm_Odistinct_I39_J)).
% 277.20/240.55  thf(539,plain,((! [A:trm,B:trm,C:trm]: ~ ((plus @ A @ B) = (differential @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 277.20/240.55  thf(234,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: ((uSubst95898992stappt @ A @ B @ (times @ C @ D)) = (uSubst277968634Timeso @ (uSubst95898992stappt @ A @ B @ C) @ (uSubst95898992stappt @ A @ B @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_usubstappt_Osimps_I6_J)).
% 277.20/240.55  thf(1412,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: ((uSubst95898992stappt @ A @ B @ (times @ C @ D)) = (uSubst277968634Timeso @ (uSubst95898992stappt @ A @ B @ C) @ (uSubst95898992stappt @ A @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[234])).
% 277.20/240.55  thf(141,axiom,((! [A:(option @ trm)]: ((uSubst1556497037e_Geqo @ (none @ trm) @ A) = (none @ fml)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_Geqo_Osimps_I2_J)).
% 277.20/240.55  thf(759,plain,((! [A:(option @ trm)]: ((uSubst1556497037e_Geqo @ (none @ trm) @ A) = (none @ fml)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 277.20/240.55  thf(195,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((A != (none @ TA)) = (? [B:TA]: (A = (some @ TA @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_not__None__eq)).
% 277.20/240.55  thf(1189,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ((~ (A = (none @ TA))) = (? [B:TA]: (A = (some @ TA @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 277.20/240.55  thf(230,axiom,((! [A:(option @ game)]: ((! [B:game]: (A != (some @ game @ B))) => (A = (none @ game))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_142_Loopo_Ocases)).
% 277.20/240.55  thf(1390,plain,((! [A:(option @ game)]: ((! [B:game]: ~ (A = (some @ game @ B))) => (A = (none @ game))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 277.20/240.55  thf(236,axiom,((! [A:trm,B:trm]: ((uSubst277968634Timeso @ (some @ trm @ A) @ (some @ trm @ B)) = (some @ trm @ (times @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_116_Timeso_Osimps_I1_J)).
% 277.20/240.55  thf(1421,plain,((! [A:trm,B:trm]: ((uSubst277968634Timeso @ (some @ trm @ A) @ (some @ trm @ B)) = (some @ trm @ (times @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[236])).
% 277.20/240.55  thf(66,axiom,((! [TA: $tType]: (! [A:TA]: ((the @ TA @ (some @ TA @ A)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_144_option_Osel)).
% 277.20/240.55  thf(465,plain,((! [TA: $tType]: (! [A:TA]: ((the @ TA @ (some @ TA @ A)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 277.20/240.55  thf(61,axiom,((! [A:real,B:real]: (((number @ A) = (number @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_trm_Oinject_I2_J)).
% 277.20/240.55  thf(450,plain,((! [A:real,B:real]: (((number @ A) = (number @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 277.20/240.55  thf(177,axiom,((! [A:((option @ game) > $o),B:(option @ game)]: ((! [C:game]: (A @ (some @ game @ C))) => ((A @ (none @ game)) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_Loopo_Oinduct)).
% 277.20/240.55  thf(1084,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)],[177])).
% 277.20/240.55  thf(82,axiom,((! [TA: $tType]: ((ord_less_eq @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: ! [C:TA]: ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_subset__eq)).
% 277.20/240.55  thf(524,plain,((! [TA: $tType]: ((ord_less_eq @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: ! [C:TA]: ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 277.20/240.55  thf(101,axiom,((! [A:(denotational_interp > (trm > $o)),B:denotational_interp,C:trm]: ((! [D:denotational_interp,E:variable]: (A @ D @ (var @ E))) => ((! [D:denotational_interp,E:real]: (A @ D @ (number @ E))) => ((! [D:denotational_interp,E:char]: (A @ D @ (const @ E))) => ((! [D:denotational_interp,E:char,F:trm]: ((A @ D @ F) => (A @ D @ (func @ E @ F)))) => ((! [D:denotational_interp,E:trm]: ((A @ D @ E) => (! [F:trm]: ((A @ D @ F) => (A @ D @ (plus @ E @ F)))))) => ((! [D:denotational_interp,E:trm]: ((A @ D @ E) => (! [F:trm]: ((A @ D @ F) => (A @ D @ (times @ E @ F)))))) => ((! [D:denotational_interp,E:trm]: (((? [F:char]: (member @ char @ F @ (collect @ char @ (^ [G:char]: (($true)))))) => (A @ D @ E)) => (A @ D @ (differential @ E)))) => (A @ B @ C)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_217_term__sem_Oinduct)).
% 277.20/240.55  thf(581,plain,((! [A:(denotational_interp > (trm > $o)),B:denotational_interp,C:trm]: ((! [D:denotational_interp,E:variable]: (A @ D @ (var @ E))) => ((! [D:denotational_interp,E:real]: (A @ D @ (number @ E))) => ((! [D:denotational_interp,E:char]: (A @ D @ (const @ E))) => ((! [D:denotational_interp,E:char,F:trm]: ((A @ D @ F) => (A @ D @ (func @ E @ F)))) => ((! [D:denotational_interp,E:trm]: ((A @ D @ E) => (! [F:trm]: ((A @ D @ F) => (A @ D @ (plus @ E @ F)))))) => ((! [D:denotational_interp,E:trm]: ((A @ D @ E) => (! [F:trm]: ((A @ D @ F) => (A @ D @ (times @ E @ F)))))) => ((! [D:denotational_interp,E:trm]: (((? [F:char]: (member @ char @ F @ (collect @ char @ (^ [G:char]: (($true)))))) => (A @ D @ E)) => (A @ D @ (differential @ E)))) => (A @ B @ C)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 277.20/240.55  thf(209,axiom,((! [A:(option @ trm)]: ((uSubst277968634Timeso @ (none @ trm) @ A) = (none @ trm)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_Timeso_Osimps_I2_J)).
% 277.20/240.55  thf(1289,plain,((! [A:(option @ trm)]: ((uSubst277968634Timeso @ (none @ trm) @ A) = (none @ trm)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 277.20/240.55  thf(38,axiom,((! [A:real,B:trm,C:trm]: ((number @ A) != (plus @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_trm_Odistinct_I17_J)).
% 277.20/240.55  thf(368,plain,((! [A:real,B:trm,C:trm]: ~ ((number @ A) = (plus @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 277.20/240.55  thf(165,axiom,((! [A:trm,B:trm]: ((uSubst1556497037e_Geqo @ (some @ trm @ A) @ (some @ trm @ B)) = (some @ fml @ (geq @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_122_Geqo_Osimps_I1_J)).
% 277.20/240.55  thf(961,plain,((! [A:trm,B:trm]: ((uSubst1556497037e_Geqo @ (some @ trm @ A) @ (some @ trm @ B)) = (some @ fml @ (geq @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 277.20/240.55  thf(80,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($false) @ A @ B) = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_2_1_T)).
% 277.20/240.55  thf(517,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($false) @ A @ B) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 277.20/240.55  thf(214,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:variable]: ((uSubst95898992stappt @ A @ B @ (var @ C)) = (some @ trm @ (var @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_196_usubstappt_Osimps_I1_J)).
% 277.20/240.55  thf(1341,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:variable]: ((uSubst95898992stappt @ A @ B @ (var @ C)) = (some @ trm @ (var @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 277.20/240.55  thf(123,axiom,((! [A:variable,B:trm,C:trm]: ((var @ A) != (plus @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_191_trm_Odistinct_I7_J)).
% 277.20/240.55  thf(652,plain,((! [A:variable,B:trm,C:trm]: ~ ((var @ A) = (plus @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 277.20/240.55  thf(44,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((ord_less_eq @ (set @ TA) @ (collect @ TA @ A) @ (collect @ TA @ B)) = (! [C:TA]: ((A @ C) => (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_Collect__mono__iff)).
% 277.20/240.55  thf(390,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((ord_less_eq @ (set @ TA) @ (collect @ TA @ (A)) @ (collect @ TA @ (B))) = (! [C:TA]: ((A @ C) => (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 277.20/240.55  thf(47,axiom,((! [TA: $tType,TB: $tType]: (! [A:TB,B:(TA > TB),C:TA]: ((case_option @ TB @ TA @ A @ B @ (some @ TA @ C)) = (B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_164_option_Osimps_I5_J)).
% 277.20/240.55  thf(401,plain,((! [TA: $tType,TB: $tType]: (! [A:TB,B:(TA > TB),C:TA]: ((case_option @ TB @ TA @ A @ (B) @ (some @ TA @ C)) = (B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 277.20/240.55  thf(172,axiom,((! [A:(char > ((option @ trm) > $o)),B:char,C:(option @ trm)]: ((! [D:char,E:trm]: (A @ D @ (some @ trm @ E))) => ((! [D:char]: (A @ D @ (none @ trm))) => (A @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_109_ODEo_Oinduct)).
% 277.20/240.55  thf(995,plain,((! [A:(char > ((option @ trm) > $o)),B:char,C:(option @ trm)]: ((! [D:char,E:trm]: (A @ D @ (some @ trm @ E))) => ((! [D:char]: (A @ D @ (none @ trm))) => (A @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 277.20/240.55  thf(14,axiom,((! [TA: $tType,TB: $tType]: ((top @ TA) => (top @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Otop)).
% 277.20/240.55  thf(290,plain,((! [TA: $tType,TB: $tType]: ((top @ TA) => (top @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 277.20/240.55  thf(163,axiom,((! [A:(option @ trm),B:(option @ trm)]: (((uSubst259074819ntialo @ A) = B) => ((accp @ (option @ trm) @ uSubst99643830lo_rel @ A) => ((! [C:trm]: ((A = (some @ trm @ C)) => ((B = (some @ trm @ (differential @ C))) => (~ (accp @ (option @ trm) @ uSubst99643830lo_rel @ (some @ trm @ C)))))) => (~ ((A = (none @ trm)) => ((B = (none @ trm)) => (~ (accp @ (option @ trm) @ uSubst99643830lo_rel @ (none @ trm))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_120_Differentialo_Opelims)).
% 277.20/240.55  thf(929,plain,((! [A:(option @ trm),B:(option @ trm)]: (((uSubst259074819ntialo @ A) = B) => ((accp @ (option @ trm) @ (uSubst99643830lo_rel) @ A) => ((! [C:trm]: ((A = (some @ trm @ C)) => ((B = (some @ trm @ (differential @ C))) => (~ (accp @ (option @ trm) @ (uSubst99643830lo_rel) @ (some @ trm @ C)))))) => (~ ((A = (none @ trm)) => ((B = (none @ trm)) => (~ (accp @ (option @ trm) @ (uSubst99643830lo_rel) @ (none @ trm))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 277.20/240.55  thf(175,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: (((uSubst95898992stappt @ A @ B @ C) != (none @ trm)) => (((uSubst95898992stappt @ A @ B @ D) != (none @ trm)) => ((uSubst95898978stappf @ A @ B @ (geq @ C @ D)) = (some @ fml @ (geq @ (the @ trm @ (uSubst95898992stappt @ A @ B @ C)) @ (the @ trm @ (uSubst95898992stappt @ A @ B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_usubstappf__geq)).
% 277.20/240.55  thf(1077,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: ((~ ((uSubst95898992stappt @ A @ B @ C) = (none @ trm))) => ((~ ((uSubst95898992stappt @ A @ B @ D) = (none @ trm))) => ((uSubst95898978stappf @ A @ B @ (geq @ C @ D)) = (some @ fml @ (geq @ (the @ trm @ (uSubst95898992stappt @ A @ B @ C)) @ (the @ trm @ (uSubst95898992stappt @ A @ B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 277.20/240.55  thf(130,axiom,((! [A:trm,B:trm,C:trm,D:trm]: (((times @ A @ B) = (times @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_trm_Oinject_I6_J)).
% 277.20/240.55  thf(684,plain,((! [A:trm,B:trm,C:trm,D:trm]: (((times @ A @ B) = (times @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 277.20/240.55  thf(216,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((A != (none @ TA)) = (case_option @ $o @ TA @ ($false) @ (^ [B:TA]: (($true))) @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_166_option_Odisc__eq__case_I2_J)).
% 277.20/240.55  thf(1348,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ((~ (A = (none @ TA))) = (case_option @ $o @ TA @ ($false) @ (^ [B:TA]: (($true))) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 277.20/240.55  thf(111,axiom,((! [A:(set @ variable),B:(set @ variable),C:(variable > real),D:(variable > real)]: ((ord_less_eq @ (set @ variable) @ A @ B) => ((denota1419872369iation @ C @ D @ A) => (denota1419872369iation @ C @ D @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_Uvariation__mon)).
% 277.20/240.55  thf(620,plain,((! [A:(set @ variable),B:(set @ variable),C:(variable > real),D:(variable > real)]: ((ord_less_eq @ (set @ variable) @ A @ B) => ((denota1419872369iation @ (C) @ (D) @ A) => (denota1419872369iation @ (C) @ (D) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 277.20/240.55  thf(139,axiom,((! [A:(option @ trm)]: ((uSubst1112714340_Pluso @ (none @ trm) @ A) = (none @ trm)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_Pluso_Osimps_I2_J)).
% 277.20/240.55  thf(752,plain,((! [A:(option @ trm)]: ((uSubst1112714340_Pluso @ (none @ trm) @ A) = (none @ trm)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 277.20/240.55  thf(59,axiom,((order_top @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oorder__top_6)).
% 277.20/240.55  thf(447,plain,((order_top @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 277.20/240.55  thf(206,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: ((accp @ (product_prod @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm)) @ uSubst2096773001pt_rel @ (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ A @ (product_Pair @ (set @ variable) @ trm @ B @ (times @ C @ D)))) => ((uSubst95898992stappt @ A @ B @ (times @ C @ D)) = (uSubst277968634Timeso @ (uSubst95898992stappt @ A @ B @ C) @ (uSubst95898992stappt @ A @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_181_usubstappt_Opsimps_I6_J)).
% 277.20/240.55  thf(1280,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:trm,D:trm]: ((accp @ (product_prod @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm)) @ (uSubst2096773001pt_rel) @ (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ A @ (product_Pair @ (set @ variable) @ trm @ B @ (times @ C @ D)))) => ((uSubst95898992stappt @ A @ B @ (times @ C @ D)) = (uSubst277968634Timeso @ (uSubst95898992stappt @ A @ B @ C) @ (uSubst95898992stappt @ A @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 277.20/240.55  thf(54,axiom,((! [TA: $tType]: (! [A:(TA > (TA > $o))]: (ord_less_eq @ (TA > (TA > $o)) @ ((=) @ TA) @ (^ [B:TA,C:TA]: ((A @ B @ C) | (B = C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_154_eq__subset)).
% 277.20/240.55  thf(432,plain,((! [TA: $tType]: (! [A:(TA > (TA > $o))]: (ord_less_eq @ (TA > (TA > $o)) @ ((=) @ TA) @ (^ [B:TA,C:TA]: ((A @ B @ C) | (B = C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 277.20/240.55  thf(226,axiom,(((some @ trm) = (some @ trm))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_Aterm__Some)).
% 277.20/240.55  thf(1380,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 277.20/240.55  thf(50,axiom,((! [TA: $tType]: ((accp @ TA) = (^ [A:(TA > (TA > $o)),B:TA]: ? [C:TA]: ((B = C) & ! [D:TA]: ((A @ D @ C) => (accp @ TA @ A @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_147_accp_Osimps)).
% 277.20/240.55  thf(410,plain,((! [TA: $tType]: ((accp @ TA) = (^ [A:(TA > (TA > $o)),B:TA]: ? [C:TA]: ((B = C) & ! [D:TA]: ((A @ D @ C) => (accp @ TA @ A @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 277.20/240.55  thf(167,axiom,((! [TA: $tType,TB: $tType]: (! [A:TA,B:(TB > TA)]: ((case_option @ TA @ TB @ A @ B @ (none @ TB)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_162_option_Osimps_I4_J)).
% 277.20/240.55  thf(967,plain,((! [TA: $tType,TB: $tType]: (! [A:TA,B:(TB > TA)]: ((case_option @ TA @ TB @ A @ (B) @ (none @ TB)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 277.20/240.55  thf(21,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: (ord_less_eq @ (set @ TA) @ A @ (top_top @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_240_subset__UNIV)).
% 277.20/240.55  thf(305,plain,((! [TA: $tType]: (! [A:(set @ TA)]: (ord_less_eq @ (set @ TA) @ A @ (top_top @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 277.20/240.55  thf(28,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((A @ B) => ((ord_less_eq @ (TA > $o) @ A @ C) => (C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_rev__predicate1D)).
% 277.20/240.55  thf(326,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((A @ B) => ((ord_less_eq @ (TA > $o) @ (A) @ (C)) => (C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 277.20/240.55  thf(1,conjecture,(((uSubst95898992stappt @ sigma @ ua @ theta) != (none @ trm))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 277.20/240.55  thf(2,negated_conjecture,((~ ((uSubst95898992stappt @ sigma @ ua @ theta) != (none @ trm)))),inference(neg_conjecture,[status(cth)],[1])).
% 277.20/240.55  thf(242,plain,((~ (~ ((uSubst95898992stappt @ sigma @ ua @ theta) = (none @ trm))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 277.20/240.55  thf(160,axiom,((! [A:(product_prod @ (option @ game) @ (option @ fml))]: ((! [B:game,C:fml]: (A != (product_Pair @ (option @ game) @ (option @ fml) @ (some @ game @ B) @ (some @ fml @ C)))) => ((! [B:(option @ fml)]: (A != (product_Pair @ (option @ game) @ (option @ fml) @ (none @ game) @ B))) => (~ (! [B:game]: (A != (product_Pair @ (option @ game) @ (option @ fml) @ (some @ game @ B) @ (none @ fml))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_156_Diamondo_Ocases)).
% 277.20/240.55  thf(918,plain,((! [A:(product_prod @ (option @ game) @ (option @ fml))]: ((! [B:game,C:fml]: ~ (A = (product_Pair @ (option @ game) @ (option @ fml) @ (some @ game @ B) @ (some @ fml @ C)))) => ((! [B:(option @ fml)]: ~ (A = (product_Pair @ (option @ game) @ (option @ fml) @ (none @ game) @ B))) => (~ (! [B:game]: ~ (A = (product_Pair @ (option @ game) @ (option @ fml) @ (some @ game @ B) @ (none @ fml))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 277.20/240.55  thf(125,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((ord_less_eq @ (set @ TA) @ B @ C) => (ord_less_eq @ (set @ TA) @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_subset__trans)).
% 277.20/240.55  thf(664,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((ord_less_eq @ (set @ TA) @ B @ C) => (ord_less_eq @ (set @ TA) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 277.20/240.55  thf(30,axiom,((! [TA: $tType]: ((top_top @ (set @ TA)) = (collect @ TA @ (top_top @ (TA > $o)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_253_top__set__def)).
% 277.20/240.55  thf(332,plain,((! [TA: $tType]: ((top_top @ (set @ TA)) = (collect @ TA @ (top_top @ (TA > $o)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 277.20/240.55  thf(201,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:real]: ((uSubst95898992stappt @ A @ B @ (number @ C)) = (some @ trm @ (number @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_195_usubstappt_Osimps_I2_J)).
% 277.20/240.55  thf(1261,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:real]: ((uSubst95898992stappt @ A @ B @ (number @ C)) = (some @ trm @ (number @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 277.20/240.55  thf(99,axiom,((! [A:char,B:trm,C:char,D:trm]: (((ode @ A @ B) = (ode @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_250_game_Oinject_I8_J)).
% 277.20/240.55  thf(575,plain,((! [A:char,B:trm,C:char,D:trm]: (((ode @ A @ B) = (ode @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 277.20/240.55  thf(228,axiom,((! [A:((option @ fml) > ((option @ fml) > $o)),B:(option @ fml),C:(option @ fml)]: ((! [D:fml,E:fml]: (A @ (some @ fml @ D) @ (some @ fml @ E))) => ((! [D:(option @ fml)]: (A @ (none @ fml) @ D)) => ((! [D:fml]: (A @ (some @ fml @ D) @ (none @ fml))) => (A @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_130_Ando_Oinduct)).
% 277.20/240.55  thf(1384,plain,((! [A:((option @ fml) > ((option @ fml) > $o)),B:(option @ fml),C:(option @ fml)]: ((! [D:fml,E:fml]: (A @ (some @ fml @ D) @ (some @ fml @ E))) => ((! [D:(option @ fml)]: (A @ (none @ fml) @ D)) => ((! [D:fml]: (A @ (some @ fml @ D) @ (none @ fml))) => (A @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 277.20/240.55  thf(120,axiom,((! [A:trm,B:trm]: (((differential @ A) = (differential @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_trm_Oinject_I7_J)).
% 277.20/240.55  thf(644,plain,((! [A:trm,B:trm]: (((differential @ A) = (differential @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 277.20/240.55  thf(157,axiom,((! [A:(product_prod @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm))]: ((! [B:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),C:(set @ variable),D:variable]: (A != (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ B @ (product_Pair @ (set @ variable) @ trm @ C @ (var @ D))))) => ((! [B:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),C:(set @ variable),D:real]: (A != (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ B @ (product_Pair @ (set @ variable) @ trm @ C @ (number @ D))))) => ((! [B:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),C:(set @ variable),D:char]: (A != (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ B @ (product_Pair @ (set @ variable) @ trm @ C @ (const @ D))))) => ((! [B:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),C:(set @ variable),D:char,E:trm]: (A != (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ B @ (product_Pair @ (set @ variable) @ trm @ C @ (func @ D @ E))))) => ((! [B:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),C:(set @ variable),D:trm,E:trm]: (A != (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ B @ (product_Pair @ (set @ variable) @ trm @ C @ (plus @ D @ E))))) => ((! [B:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),C:(set @ variable),D:trm,E:trm]: (A != (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ B @ (product_Pair @ (set @ variable) @ trm @ C @ (times @ D @ E))))) => (~ (! [B:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),C:(set @ variable),D:trm]: (A != (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ B @ (product_Pair @ (set @ variable) @ trm @ C @ (differential @ D)))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_197_usubstappt_Ocases)).
% 277.20/240.55  thf(908,plain,((! [A:(product_prod @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm))]: ((! [B:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),C:(set @ variable),D:variable]: ~ (A = (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ B @ (product_Pair @ (set @ variable) @ trm @ C @ (var @ D))))) => ((! [B:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),C:(set @ variable),D:real]: ~ (A = (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ B @ (product_Pair @ (set @ variable) @ trm @ C @ (number @ D))))) => ((! [B:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),C:(set @ variable),D:char]: ~ (A = (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ B @ (product_Pair @ (set @ variable) @ trm @ C @ (const @ D))))) => ((! [B:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),C:(set @ variable),D:char,E:trm]: ~ (A = (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ B @ (product_Pair @ (set @ variable) @ trm @ C @ (func @ D @ E))))) => ((! [B:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),C:(set @ variable),D:trm,E:trm]: ~ (A = (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ B @ (product_Pair @ (set @ variable) @ trm @ C @ (plus @ D @ E))))) => ((! [B:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),C:(set @ variable),D:trm,E:trm]: ~ (A = (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ B @ (product_Pair @ (set @ variable) @ trm @ C @ (times @ D @ E))))) => (~ (! [B:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),C:(set @ variable),D:trm]: ~ (A = (product_Pair @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) @ (product_prod @ (set @ variable) @ trm) @ B @ (product_Pair @ (set @ variable) @ trm @ C @ (differential @ D)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 277.20/240.55  thf(132,axiom,((! [TA: $tType,TB: $tType]: (! [A:(set @ (product_prod @ TA @ TA)),B:(set @ (product_prod @ TA @ TA)),C:(TA > TB)]: ((ord_less_eq @ (set @ (product_prod @ TA @ TA)) @ A @ B) => (ord_less_eq @ (set @ (product_prod @ TB @ TB)) @ (bNF_Gr1317331620lImage @ TA @ TB @ A @ C) @ (bNF_Gr1317331620lImage @ TA @ TB @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_226_relImage__mono)).
% 277.20/240.55  thf(691,plain,((! [TA: $tType,TB: $tType]: (! [A:(set @ (product_prod @ TA @ TA)),B:(set @ (product_prod @ TA @ TA)),C:(TA > TB)]: ((ord_less_eq @ (set @ (product_prod @ TA @ TA)) @ A @ B) => (ord_less_eq @ (set @ (product_prod @ TB @ TB)) @ (bNF_Gr1317331620lImage @ TA @ TB @ A @ (C)) @ (bNF_Gr1317331620lImage @ TA @ TB @ B @ (C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 277.20/240.55  thf(57,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($true) @ A @ B) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_1_1_T)).
% 277.20/240.55  thf(442,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($true) @ A @ B) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 277.20/240.55  thf(76,axiom,((! [TA: $tType,TB: $tType]: (! [A:(set @ (product_prod @ TA @ TB)),B:(set @ (product_prod @ TA @ TB))]: (((^ [C:TA,D:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ A)) = (^ [C:TA,D:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ B))) = (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_160_pred__equals__eq2)).
% 277.20/240.55  thf(501,plain,((! [TA: $tType,TB: $tType]: (! [A:(set @ (product_prod @ TA @ TB)),B:(set @ (product_prod @ TA @ TB))]: (((^ [C:TA,D:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ A)) = (^ [C:TA,D:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ B))) = (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 277.20/240.55  thf(179,axiom,((! [A:trm]: ((uSubst277968634Timeso @ (some @ trm @ A) @ (none @ trm)) = (none @ trm)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_113_Timeso_Osimps_I3_J)).
% 277.20/240.55  thf(1093,plain,((! [A:trm]: ((uSubst277968634Timeso @ (some @ trm @ A) @ (none @ trm)) = (none @ trm)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 277.20/240.55  thf(113,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_subsetD)).
% 277.20/240.55  thf(624,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 277.20/240.55  thf(151,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:char]: ((uSubst95898992stappt @ A @ B @ (const @ C)) = (uSubst1138577137pconst @ A @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_218_usubstappt_Osimps_I3_J)).
% 277.20/240.55  thf(839,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:(set @ variable),C:char]: ((uSubst95898992stappt @ A @ B @ (const @ C)) = (uSubst1138577137pconst @ A @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 277.20/240.55  thf(219,axiom,((! [A:(product_prod @ char @ (option @ trm))]: ((! [B:char,C:trm]: (A != (product_Pair @ char @ (option @ trm) @ B @ (some @ trm @ C)))) => (~ (! [B:char]: (A != (product_Pair @ char @ (option @ trm) @ B @ (none @ trm)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_175_ODEo_Ocases)).
% 277.20/240.55  thf(1357,plain,((! [A:(product_prod @ char @ (option @ trm))]: ((! [B:char,C:trm]: ~ (A = (product_Pair @ char @ (option @ trm) @ B @ (some @ trm @ C)))) => (~ (! [B:char]: ~ (A = (product_Pair @ char @ (option @ trm) @ B @ (none @ trm)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 277.20/240.55  thf(64,axiom,((! [A:trm,B:trm,C:trm,D:trm]: (((geq @ A @ B) = (geq @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_fml_Oinject_I2_J)).
% 277.20/240.55  thf(459,plain,((! [A:trm,B:trm,C:trm,D:trm]: (((geq @ A @ B) = (geq @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 277.20/240.55  thf(5,axiom,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ B)) = (B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_mem__Collect__eq)).
% 277.20/240.55  thf(254,plain,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ (B))) = (B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 277.20/240.55  thf(27,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) => (B @ C))) => (ord_less_eq @ (set @ TA) @ (collect @ TA @ A) @ (collect @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_Collect__mono)).
% 277.20/240.55  thf(322,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) => (B @ C))) => (ord_less_eq @ (set @ TA) @ (collect @ TA @ (A)) @ (collect @ TA @ (B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 277.20/240.55  thf(73,axiom,((! [A:trm,B:trm,C:trm]: ((times @ A @ B) != (differential @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_111_trm_Odistinct_I41_J)).
% 277.20/240.55  thf(486,plain,((! [A:trm,B:trm,C:trm]: ~ ((times @ A @ B) = (differential @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 277.20/240.55  thf(222,axiom,((! [A:char,B:(option @ trm)]: (((uSubst1083227664e_ODEo @ A @ B) = (none @ game)) = (B = (none @ trm))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_237_ODEo__undef)).
% 277.20/240.55  thf(1367,plain,((! [A:char,B:(option @ trm)]: (((uSubst1083227664e_ODEo @ A @ B) = (none @ game)) = (B = (none @ trm))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 277.20/240.55  thf(87,axiom,((! [TA: $tType]: (! [A:(TA > (TA > $o)),B:TA]: ((accp @ TA @ A @ B) => (! [C:TA]: ((A @ C @ B) => (accp @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_146_accp_Ocases)).
% 277.20/240.55  thf(543,plain,((! [TA: $tType]: (! [A:(TA > (TA > $o)),B:TA]: ((accp @ TA @ (A) @ B) => (! [C:TA]: ((A @ C @ B) => (accp @ TA @ (A) @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 277.20/240.55  thf(93,axiom,((denota1419872369iation @ nu @ omega @ u)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_vaouter)).
% 277.20/240.55  thf(560,plain,((denota1419872369iation @ (nu) @ (omega) @ u)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 277.20/240.55  thf(140,axiom,((! [TA: $tType]: (! [A:(option @ TA),B:TA]: ((A = (some @ TA @ B)) => (A != (none @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_option_OdiscI)).
% 277.20/240.55  thf(755,plain,((! [TA: $tType]: (! [A:(option @ TA),B:TA]: ((A = (some @ TA @ B)) => (~ (A = (none @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 277.20/240.55  thf(37,axiom,((! [A:variable,B:trm,C:fml]: ((assign @ A @ B) != (test @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_234_game_Odistinct_I15_J)).
% 277.20/240.55  thf(364,plain,((! [A:variable,B:trm,C:fml]: ~ ((assign @ A @ B) = (test @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 277.20/240.55  thf(1456,plain,(($false)),inference(e,[status(thm)],[468,481,666,1295,408,762,1401,1173,384,1327,1354,670,404,898,1441,288,301,257,1298,372,504,1264,902,638,606,1398,448,316,1415,475,376,623,834,1283,905,1447,453,1394,1351,998,428,1242,507,527,602,981,397,687,1377,280,307,292,248,380,1438,1387,746,1255,598,561,297,729,260,349,693,630,275,1370,830,1027,551,974,456,842,285,1106,578,650,615,1111,725,1096,1138,1118,1361,1292,554,1424,970,328,471,837,647,1099,1192,393,1114,633,311,1286,558,674,794,926,1135,824,1374,743,958,545,413,641,445,572,313,1271,611,335,1090,1258,350,604,831,681,567,1144,245,318,303,509,434,477,387,494,345,535,964,1344,462,848,520,626,915,1177,1381,912,608,563,299,1364,1102,438,922,636,1245,278,1445,473,490,426,531,548,1277,617,342,823,1081,749,295,282,1267,791,1186,338,1141,656,978,571,595,1180,539,1412,759,1189,1390,1421,465,450,1084,524,581,1289,368,961,517,1341,652,390,401,995,290,929,1077,684,1348,620,752,447,1280,432,1380,410,967,305,326,242,918,664,332,1261,575,1384,644,908,691,442,501,1093,624,839,1357,459,254,322,486,1367,543,560,755,364])).
% 277.20/240.55  % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 277.20/240.55  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------