%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP199^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 : n019.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 62.87s 20.36s
% Output : Refutation 61.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP199^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.08 % 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.21 % Computer : n019.cluster.edu
% 0.11/0.21 % Model : x86_64 x86_64
% 0.11/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.21 % Memory : 8046.5625MB
% 0.11/0.21 % OS : Linux 6.8.0-71-generic
% 0.11/0.22 % CPULimit : 300
% 0.11/0.22 % WCLimit : 300
% 0.11/0.22 % DateTime : Tue Sep 29 20:11:03 UTC 2026
% 0.11/0.22 % CPUTime :
% 0.11/0.22 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.05/0.80 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.37/1.24 % [INFO] Parsing done (433ms).
% 2.37/1.25 % [INFO] Running in sequential loop mode.
% 3.58/1.65 % [INFO] eprover registered as external prover.
% 3.58/1.65 % [INFO] Scanning for conjecture ...
% 4.03/1.83 % [INFO] Found a conjecture (or negated_conjecture) and 301 axioms. Running axiom selection ...
% 4.26/1.99 % [INFO] Axiom selection finished. Selected 300 axioms (removed 1 axioms).
% 5.78/2.31 % [INFO] Problem is higher-order (TPTP THF).
% 5.78/2.34 % [INFO] Type checking passed.
% 5.78/2.35 % [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 ...
% 62.87/20.32 % [WARNING] Translation of external proof obligation failed for some reason.
% 62.87/20.32 % [WARNING] java.util.NoSuchElementException: None.get: None.get
% 62.87/20.34 % External prover 'e' found a proof!
% 62.87/20.34 % [INFO] Killing All external provers ...
% 62.87/20.35 % Time passed: 19989ms (effective reasoning time: 19086ms)
% 62.87/20.35 % 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)>
% 62.87/20.35 % Axioms used in derivation (300): fact_69_Uvariation__sym__rel, tcon_fun___Orderings_Obot, fact_62_Un__absorb, fact_170_similar__selectlike__mem, fact_55_inf__sup__aci_I5_J, tcon_Set_Oset___Groups_Ouminus_15, fact_180_Vagree__sym__rel, tcon_Set_Oset___Orderings_Obot_14, fact_208_ComplD, fact_104_is__singleton__the__elem, fact_16_empty__iff, fact_50_sup__assoc, fact_13_empty__Collect__eq, fact_147_selectlike__union, fact_11_sup__bot_Oneutr__eq__iff, fact_151_option_Oexhaust, fact_3_Un__insert__right, fact_206_fun__Compl__def, fact_175_ospec, fact_44_sup__commute, fact_25_sup__apply, fact_247_compl__le__compl__iff, fact_222_Vagree__stateinterpol, fact_21_sup__left__idem, fact_40_insertI1, tcon_HOL_Obool___Lattices_Olattice_22, tcon_Set_Oset___Lattices_Olattice_13, tcon_Nat_Onat___Orderings_Opreorder_5, fact_66_UnI2, fact_42_sup__left__commute, fact_130_repv__access, fact_184_option_Osimps_I14_J, fact_155_combine__options__cases, fact_94_f2, tcon_Set_Oset___Orderings_Opreorder_12, fact_8_sup__eq__bot__iff, fact_242_inf__right__idem, fact_108_is__singletonI_H, fact_163_option_Osplit__sel, fact_179_Vagree__refl, fact_2_Un__insert__left, fact_201_equal__neg__zero, fact_243_IntI, fact_24_sup_Oidem, fact_90_union__or, fact_95_zero__reorient, fact_200_neg__equal__0__iff__equal, fact_131_these__empty, fact_127_these__not__empty__eq, fact_214_selectlike__equal__cond, tcon_HOL_Obool___Groups_Ouminus_24, tcon_HOL_Obool___Lattices_Oboolean__algebra_20, fact_117_usubstappt__det, tcon_Nat_Onat___Orderings_Obot_7, fact_187_solves__Vagree, fact_252_empty__subsetI, fact_27_singletonI, fact_129_repv__self, tcon_Nat_Onat___Lattices_Olattice_6, fact_87_variable_Oinject_I1_J, fact_126_these__empty__eq, fact_185_option_Oset__sel, fact_72_Uvariation__def, fact_33_mk__disjoint__insert, fact_205_equation__minus__iff, fact_128_variable_Osimps_I7_J, fact_20_sup_Oright__idem, fact_198_add_Oinverse__neutral, fact_204_minus__equation__iff, fact_246_neg__le__iff__le, fact_38_Set_Oset__insert, fact_89_variable_Oinject_I2_J, tcon_HOL_Obool___Lattices_Obounded__semilattice__sup__bot_17, fact_15_all__not__in__conv, fact_192_compl__eq__compl__iff, tcon_fun___Lattices_Obounded__semilattice__sup__bot, fact_239_inf_Oleft__idem, fact_31_equals0D, fact_141_not__None__eq, fact_110_is__singletonE, fact_39_insertI2, fact_199_neg__0__equal__iff__equal, fact_135_these__insert__Some, fact_133_repv__def__correct, fact_26_UnCI, fact_227_stateinterpol__diff, fact_253_subset__empty, fact_234_subsetI, fact_125_Uvariation__repv, fact_165_option_Osimps_I15_J, fact_43_sup_Oleft__commute, fact_137_repv__selectlike__other, fact_46_Collect__mem__eq, tcon_HOL_Obool___Lattices_Osemilattice__inf_19, fact_142_not__Some__eq, tcon_Real_Oreal___Orderings_Opreorder_27, fact_12_sup__bot_Oright__neutral, fact_5_sup__bot__left, fact_140_selectlike__self, fact_68_UnE, fact_132_these__insert__None, fact_51_sup_Oassoc, fact_230_coincidence__term, fact_63_Un__assoc, fact_101_variable_Oexhaust, fact_105_vaflow2, fact_93_bot__apply, tcon_HOL_Obool___Orderings_Obot_23, fact_229_nostatediff, fact_28_bot__set__def, fact_197_ComplI, fact_167_elem__set, fact_76_singleton__iff, tcon_fun___Lattices_Obounded__lattice_2, fact_158_Timeso_Oinduct, help_If_1_1_T, fact_10_sup__bot_Oleft__neutral, fact_109_is__singleton__def, fact_70_Uvariation__refl, tcon_Real_Oreal___Groups_Oordered__ab__group__add, fact_34_insert__commute, fact_1_Uvariation__empty, fact_61_Un__commute, fact_98_same__ODE__same__sol, tcon_fun___Lattices_Osemilattice__sup, fact_96_bot__fun__def, fact_115_variable_Osize__gen_I1_J, fact_7_bot__eq__sup__iff, fact_4_Un__empty, fact_249_inf_Obounded__iff, tcon_Set_Oset___Lattices_Osemilattice__sup_9, fact_216_Timeso_Oelims, fact_49_sup_Ocommute, fact_35_insert__eq__iff, fact_237_inf_Oidem, fact_186_option_Ocase__eq__if, fact_88_set__zero, fact_217_trm_Oinject_I6_J, fact_36_insert__absorb, fact_235_subset__antisym, fact_145_option_Ocollapse, fact_215_stateinterpol__insert, fact_6_sup__bot__right, tcon_fun___Lattices_Osemilattice__inf, fact_100_variable_Oinduct, tcon_Nat_Onat___Groups_Ozero, tcon_Real_Oreal___Lattices_Olattice_28, fact_64_ball__Un, fact_144_selectlike__compose, fact_57_inf__sup__aci_I7_J, fact_193_double__compl, fact_157_undeft__equiv, fact_223_stateinterpol__def, fact_181_Vagree__empty, fact_45_mem__Collect__eq, fact_81_singleton__Un__iff, fact_138_repv__selectlike__self, fact_103_Collect__empty__eq__bot, fact_112_l2r, fact_248_le__inf__iff, fact_78_Un__empty__right, fact_73_singleton__inject, fact_91_ball__insert, fact_188_Vagree__repv, fact_250_le__sup__iff, fact_233_order__refl, tcon_Real_Oreal___Groups_Ozero_30, fact_146_in__these__eq, fact_164_option_Osplit__sel__asm, fact_118_undeft__None, tcon_Set_Oset___Lattices_Obounded__semilattice__sup__bot_8, fact_194_uminus__apply, fact_168_Vagree__and, fact_190_neg__equal__iff__equal, fact_251_sup_Obounded__iff, tcon_Real_Oreal___Lattices_Osemilattice__inf_26, fact_75_doubleton__eq__iff, fact_224_usubstappt__times__conv, fact_74_insert__not__empty, fact_241_inf_Oright__idem, fact_245_le__zero__eq, fact_71_Uvariation__sym, fact_150_option_OdiscI, fact_107_a1, fact_92_the__elem__eq, fact_121_option_Oexpand, fact_154_split__option__all, fact_32_emptyE, fact_79_Un__empty__left, fact_60_Un__left__absorb, fact_196_Compl__iff, fact_47_Collect__cong, fact_207_double__complement, fact_41_insertE, fact_195_Compl__eq__Compl__iff, help_If_3_1_T, tcon_Nat_Onat___Lattices_Osemilattice__inf_4, fact_149_option_Osel, help_If_2_1_T, fact_111_vaflow1, fact_67_UnI1, fact_114_subdef, tcon_fun___Lattices_Oboolean__algebra, fact_30_equals0I, fact_82_Un__singleton__iff, fact_177_Vagree__def, fact_29_ex__in__conv, tcon_Set_Oset___Lattices_Obounded__lattice_1, tcon_Set_Oset___Lattices_Oboolean__algebra_11, fact_156_ODEo_Oinduct, fact_161_Differentialo_Oinduct, fact_159_Assigno_Oinduct, fact_134_variable_Osimps_I8_J, fact_176_Vagree__union, tcon_Real_Oreal___Groups_Ogroup__add, fact_173_option_Oset__intros, tcon_HOL_Obool___Orderings_Opreorder_21, fact_77_singletonD, fact_56_inf__sup__aci_I6_J, fact_86__092_060open_062_092_060forall_062x0_Ax1_Ax2_Ax3_Ax4_Ax5_O_A_I_092_060exists_062v6_O_AUvariation_Av6_A_Ix5_A0_J_A_123RVar_Ax4_M_ADVar_Ax4_125_A_092_060and_062_Aterm__sem_Ax3_Ax2_Av6_A_092_060noteq_062_Aterm__sem_Ax1_Ax0_Av6_J_A_061_A_IUvariation_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_A_Ix5_A0_J_A_123RVar_Ax4_M_ADVar_Ax4_125_A_092_060and_062_Aterm__sem_Ax3_Ax2_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_A_092_060noteq_062_Aterm__sem_Ax1_Ax0_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_J_092_060close_062, fact_136_repv__selectlike__other__converse, fact_14_Collect__empty__eq, fact_166_Vagree__repv__self, fact_236_inf__apply, fact_139_option_Oinject, fact_212_selectlike__equal__cocond__rule, fact_209_Timeso_Osimps_I2_J, fact_189_Timeso_Osimps_I3_J, fact_225_usubstappt_Osimps_I6_J, fact_17_insert__absorb2, fact_240_inf__left__idem, tcon_fun___Orderings_Opreorder, fact_174_option_Oset__cases, fact_172_Aterm__Some, fact_211_selectlike__equal__cocond__corule, fact_153_split__option__ex, fact_119_usubst__ode, fact_84__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062rr_O_A_092_060forall_062x0_Ax1_Ax2_Ax3_Ax4_Ax5_O_A_I_092_060exists_062v6_O_AUvariation_Av6_A_Ix5_A0_J_A_123RVar_Ax4_M_ADVar_Ax4_125_A_092_060and_062_Aterm__sem_Ax3_Ax2_Av6_A_092_060noteq_062_Aterm__sem_Ax1_Ax0_Av6_J_A_061_A_IUvariation_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_A_Ix5_A0_J_A_123RVar_Ax4_M_ADVar_Ax4_125_A_092_060and_062_Aterm__sem_Ax3_Ax2_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_A_092_060noteq_062_Aterm__sem_Ax1_Ax0_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_J_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062, fact_226_Timeso_Osimps_I1_J, fact_221_stateinterpol__empty, fact_218_stateinterpol__left, fact_52_boolean__algebra__cancel_Osup2, fact_22_sup_Oleft__idem, fact_113_IH, fact_148_option_Odistinct_I1_J, fact_191_add_Oinverse__inverse, fact_143_selectlike__empty, fact_18_insert__iff, fact_183_option_Osimps_I5_J, fact_182_option_Osimps_I4_J, fact_244_Int__iff, tcon_HOL_Obool___Lattices_Osemilattice__sup_18, tcon_Set_Oset___Groups_Ozero_16, fact_178_Vagree__sym, fact_162_option_Oexhaust__sel, fact_80_Uvariation__trans, tcon_Real_Oreal___Lattices_Osemilattice__sup_25, fact_97_not__union__or, tcon_Set_Oset___Lattices_Osemilattice__inf_10, fact_219_stateinterpol__right, tcon_Real_Oreal___Groups_Olinordered__ab__group__add, tcon_Real_Oreal___Groups_Ouminus_29, fact_210_Timeso__undef, fact_37_insert__ident, fact_203_Uvariation__Vagree, fact_228_stateinterpol__FVT, fact_83_insert__is__Un, fact_85_solves__Vagree__trans, fact_220_selectlike__co__selectlike, fact_202_neg__equal__zero, fact_120_variable_Osize__gen_I2_J, fact_169_set__empty__eq, tcon_Nat_Onat___Groups_Ocanonically__ordered__monoid__add, fact_99_variable_Odistinct_I1_J, fact_238_inf__idem, fact_231_coincidence__term__cor, fact_152_option_Oinducts, fact_59_Un__left__commute, fact_106_is__singletonI, tcon_fun___Groups_Ouminus, tcon_HOL_Obool___Lattices_Obounded__lattice, fact_65_bex__Un, fact_53_boolean__algebra__cancel_Osup1, fact_123_variable_Osize_I4_J, fact_122_variable_Osize_I3_J, fact_232_Vagree__statediff, fact_160_Differentialo_Ocases, fact_23_sup__idem, tcon_Nat_Onat___Lattices_Osemilattice__sup_3, fact_213_selectlike__equal__cocond, fact_116_usubst__term, fact_171_selectlike__Vagree, fact_9_sup__bot_Oeq__neutr__iff, fact_0_uv, fact_102_bot__empty__eq, fact_19_insertCI, tcon_fun___Lattices_Olattice, fact_54_sup__fun__def, fact_58_inf__sup__aci_I8_J, fact_124_Set_Ois__empty__def
% 62.87/20.35 % No. of inferences in proof: 604
% 62.87/20.36 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 19989 ms resp. 19086 ms w/o parsing
% 61.52/20.64 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.52/20.64 thf(denotational_interp_type, type, denotational_interp: $tType).
% 61.52/20.64 thf(variable_type, type, variable: $tType).
% 61.52/20.64 thf(game_type, type, game: $tType).
% 61.52/20.64 thf(char_type, type, char: $tType).
% 61.52/20.64 thf(trm_type, type, trm: $tType).
% 61.52/20.64 thf(fml_type, type, fml: $tType).
% 61.52/20.64 thf(real_type, type, real: $tType).
% 61.52/20.64 thf(nat_type, type, nat: $tType).
% 61.52/20.64 thf(bounded_lattice_decl, type, bounded_lattice: !> [TA: $tType]: $o).
% 61.52/20.64 thf(zero_decl, type, zero: !> [TA: $tType]: $o).
% 61.52/20.64 thf(uminus_decl, type, uminus: !> [TA: $tType]: $o).
% 61.52/20.64 thf(bot_decl, type, bot: !> [TA: $tType]: $o).
% 61.52/20.64 thf(group_add_decl, type, group_add: !> [TA: $tType]: $o).
% 61.52/20.64 thf(lattice_decl, type, lattice: !> [TA: $tType]: $o).
% 61.52/20.64 thf(preorder_decl, type, preorder: !> [TA: $tType]: $o).
% 61.52/20.64 thf(boolean_algebra_decl, type, boolean_algebra: !> [TA: $tType]: $o).
% 61.52/20.64 thf(semilattice_inf_decl, type, semilattice_inf: !> [TA: $tType]: $o).
% 61.52/20.64 thf(semilattice_sup_decl, type, semilattice_sup: !> [TA: $tType]: $o).
% 61.52/20.64 thf(ordered_ab_group_add_decl, type, ordered_ab_group_add: !> [TA: $tType]: $o).
% 61.52/20.64 thf(linord219039673up_add_decl, type, linord219039673up_add: !> [TA: $tType]: $o).
% 61.52/20.64 thf(bounde1808546759up_bot_decl, type, bounde1808546759up_bot: !> [TA: $tType]: $o).
% 61.52/20.64 thf(canoni770627133id_add_decl, type, canoni770627133id_add: !> [TA: $tType]: $o).
% 61.52/20.64 thf(statediff_decl, type, statediff: ((variable > real) > ((variable > real) > (set @ variable)))).
% 61.52/20.64 thf(stateinterpol_decl, type, stateinterpol: ((variable > real) > ((variable > real) > ((set @ variable) > (variable > real))))).
% 61.52/20.64 thf(denota1419872369iation_decl, type, denota1419872369iation: ((variable > real) > ((variable > real) > ((set @ variable) > $o)))).
% 61.52/20.64 thf(denotational_Vagree_decl, type, denotational_Vagree: ((variable > real) > ((variable > real) > ((set @ variable) > $o)))).
% 61.52/20.64 thf(denotational_repv_decl, type, denotational_repv: ((variable > real) > (variable > (real > (variable > real))))).
% 61.52/20.64 thf(denota1778088425es_ODE_decl, type, denota1778088425es_ODE: (denotational_interp > ((real > (variable > real)) > (char > (trm > $o))))).
% 61.52/20.64 thf(denota1863255036rm_sem_decl, type, denota1863255036rm_sem: (denotational_interp > (trm > ((variable > real) > real)))).
% 61.52/20.64 thf(uminus_uminus_decl, type, uminus_uminus: !> [TA: $tType]: (TA > TA)).
% 61.52/20.64 thf(zero_zero_decl, type, zero_zero: !> [TA: $tType]: TA).
% 61.52/20.64 thf(if_decl, type, if: !> [TA: $tType]: ($o > (TA > (TA > TA)))).
% 61.52/20.64 thf(inf_inf_decl, type, inf_inf: !> [TA: $tType]: (TA > (TA > TA))).
% 61.52/20.64 thf(sup_sup_decl, type, sup_sup: !> [TA: $tType]: (TA > (TA > TA))).
% 61.52/20.64 thf(size_size_decl, type, size_size: !> [TA: $tType]: (TA > nat)).
% 61.52/20.64 thf(none_decl, type, none: !> [TA: $tType]: (option @ TA)).
% 61.52/20.64 thf(some_decl, type, some: !> [TA: $tType]: (TA > (option @ TA))).
% 61.52/20.64 thf(case_option_decl, type, case_option: !> [TA: $tType,TB: $tType]: (TB > ((TA > TB) > ((option @ TA) > TB)))).
% 61.52/20.64 thf(set_option_decl, type, set_option: !> [TA: $tType]: ((option @ TA) > (set @ TA))).
% 61.52/20.64 thf(the_decl, type, the: !> [TA: $tType]: ((option @ TA) > TA)).
% 61.52/20.64 thf(these_decl, type, these: !> [TA: $tType]: ((set @ (option @ TA)) > (set @ TA))).
% 61.52/20.64 thf(bot_bot_decl, type, bot_bot: !> [TA: $tType]: TA).
% 61.52/20.64 thf(ord_less_eq_decl, type, ord_less_eq: !> [TA: $tType]: (TA > (TA > $o))).
% 61.52/20.64 thf(collect_decl, type, collect: !> [TA: $tType]: ((TA > $o) > (set @ TA))).
% 61.52/20.64 thf(insert_decl, type, insert: !> [TA: $tType]: (TA > ((set @ TA) > (set @ TA)))).
% 61.52/20.64 thf(is_empty_decl, type, is_empty: !> [TA: $tType]: ((set @ TA) > $o)).
% 61.52/20.64 thf(is_singleton_decl, type, is_singleton: !> [TA: $tType]: ((set @ TA) > $o)).
% 61.52/20.64 thf(the_elem_decl, type, the_elem: !> [TA: $tType]: ((set @ TA) > TA)).
% 61.52/20.64 thf(static_FVT_decl, type, static_FVT: (trm > (set @ variable))).
% 61.52/20.64 thf(static_selectlike_decl, type, static_selectlike: ((set @ (variable > real)) > ((variable > real) > ((set @ variable) > (set @ (variable > real)))))).
% 61.52/20.64 thf(times_decl, type, times: (trm > (trm > trm))).
% 61.52/20.64 thf(dVar_decl, type, dVar: (char > variable)).
% 61.52/20.64 thf(rVar_decl, type, rVar: (char > variable)).
% 61.52/20.64 thf(rec_variable_decl, type, rec_variable: !> [TA: $tType]: ((char > TA) > ((char > TA) > (variable > TA)))).
% 61.52/20.64 thf(size_variable_decl, type, size_variable: (variable > nat)).
% 61.52/20.64 thf(uSubst277968634Timeso_decl, type, uSubst277968634Timeso: ((option @ trm) > ((option @ trm) > (option @ trm)))).
% 61.52/20.64 thf(uSubst2091380086djoint_decl, type, uSubst2091380086djoint: ((product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))) > (denotational_interp > ((variable > real) > denotational_interp)))).
% 61.52/20.64 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))))).
% 61.52/20.64 thf(member_decl, type, member: !> [TA: $tType]: (TA > ((set @ TA) > $o))).
% 61.52/20.64 thf(f_decl, type, f: (real > (variable > real))).
% 61.52/20.64 thf(i_decl, type, i: denotational_interp).
% 61.52/20.64 thf(u_decl, type, u: (set @ variable)).
% 61.52/20.64 thf(omega_decl, type, omega: (variable > real)).
% 61.52/20.64 thf(sigma_decl, type, sigma: (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game)))))).
% 61.52/20.64 thf(theta_decl, type, theta: trm).
% 61.52/20.64 thf(rr_decl, type, rr: (trm > (denotational_interp > (trm > (denotational_interp > (char > ((real > (variable > real)) > (variable > real)))))))).
% 61.52/20.64 thf(x_decl, type, x: char).
% 61.52/20.64 thf(194,axiom,((denotational_Vagree = (^ [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_177_Vagree__def)).
% 61.52/20.64 thf(892,plain,(((denotational_Vagree) = (^ [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)],[194])).
% 61.52/20.64 thf(244,axiom,((! [A:denotational_interp,B:(real > (variable > real)),C:char,D:trm,E:real]: ((denota1778088425es_ODE @ A @ B @ C @ D) => (denotational_Vagree @ (B @ E) @ (B @ (zero_zero @ real)) @ (uminus_uminus @ (set @ variable) @ (insert @ variable @ (rVar @ C) @ (insert @ variable @ (dVar @ C) @ (bot_bot @ (set @ variable))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_solves__Vagree)).
% 61.52/20.64 thf(1036,plain,((! [A:denotational_interp,B:(real > (variable > real)),C:char,D:trm,E:real]: ((denota1778088425es_ODE @ A @ (B) @ C @ D) => (denotational_Vagree @ (B @ E) @ (B @ (zero_zero @ real)) @ (uminus_uminus @ (set @ variable) @ (insert @ variable @ (rVar @ C) @ (insert @ variable @ (dVar @ C) @ (bot_bot @ (set @ variable))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[244])).
% 61.52/20.64 thf(269,axiom,((group_add @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Ogroup__add)).
% 61.52/20.64 thf(1105,plain,((group_add @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[269])).
% 61.52/20.64 thf(242,axiom,((! [TA: $tType]: (! [A:(char > TA),B:(char > TA),C:char]: ((rec_variable @ TA @ A @ B @ (dVar @ C)) = (B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_variable_Osimps_I8_J)).
% 61.52/20.64 thf(1031,plain,((! [TA: $tType]: (! [A:(char > TA),B:(char > TA),C:char]: ((rec_variable @ TA @ (A) @ (B) @ (dVar @ C)) = (B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 61.52/20.64 thf(78,axiom,((! [TA: $tType]: ((semilattice_inf @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ (inf_inf @ TA @ B @ C)) = ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_248_le__inf__iff)).
% 61.52/20.64 thf(518,plain,((! [TA: $tType]: ((semilattice_inf @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ (inf_inf @ TA @ B @ C)) = ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 61.52/20.64 thf(59,axiom,((! [TA: $tType,TB: $tType]: ((semilattice_sup @ TA) => (semilattice_sup @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Lattices_Osemilattice__sup)).
% 61.52/20.64 thf(468,plain,((! [TA: $tType,TB: $tType]: ((semilattice_sup @ TA) => (semilattice_sup @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 61.52/20.64 thf(294,axiom,((! [TA: $tType]: (! [A:TA]: ((set_option @ TA @ (some @ TA @ A)) = (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_165_option_Osimps_I15_J)).
% 61.52/20.64 thf(1179,plain,((! [TA: $tType]: (! [A:TA]: ((set_option @ TA @ (some @ TA @ A)) = (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[294])).
% 61.52/20.64 thf(93,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_161_Differentialo_Oinduct)).
% 61.52/20.64 thf(555,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)],[93])).
% 61.52/20.64 thf(119,axiom,((! [A:(variable > real),B:(set @ variable),C:(set @ (variable > real)),D:(set @ (variable > real))]: ((! [E:(variable > real)]: ((denota1419872369iation @ E @ A @ (uminus_uminus @ (set @ variable) @ B)) => ((member @ (variable > real) @ E @ C) = (member @ (variable > real) @ E @ D)))) => ((static_selectlike @ C @ A @ B) = (static_selectlike @ D @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_212_selectlike__equal__cocond__rule)).
% 61.52/20.64 thf(666,plain,((! [A:(variable > real),B:(set @ variable),C:(set @ (variable > real)),D:(set @ (variable > real))]: ((! [E:(variable > real)]: ((denota1419872369iation @ (E) @ (A) @ (uminus_uminus @ (set @ variable) @ B)) => ((member @ (variable > real) @ (E) @ C) = (member @ (variable > real) @ (E) @ D)))) => ((static_selectlike @ C @ (A) @ B) = (static_selectlike @ D @ (A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 61.52/20.64 thf(64,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_226_Timeso_Osimps_I1_J)).
% 61.52/20.64 thf(481,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)],[64])).
% 61.52/20.64 thf(5,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_225_usubstappt_Osimps_I6_J)).
% 61.52/20.64 thf(308,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)],[5])).
% 61.52/20.64 thf(52,axiom,((! [TA: $tType,TB: $tType]: ((bounded_lattice @ TA) => (bounde1808546759up_bot @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Lattices_Obounded__semilattice__sup__bot)).
% 61.52/20.64 thf(449,plain,((! [TA: $tType,TB: $tType]: ((bounded_lattice @ TA) => (bounde1808546759up_bot @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 61.52/20.64 thf(282,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((member @ TA @ A @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_singletonD)).
% 61.52/20.64 thf(1142,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((member @ TA @ A @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[282])).
% 61.52/20.64 thf(75,axiom,((! [TA: $tType,TB: $tType]: ((uminus @ TA) => (uminus @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Groups_Ouminus)).
% 61.52/20.64 thf(511,plain,((! [TA: $tType,TB: $tType]: ((uminus @ TA) => (uminus @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 61.52/20.64 thf(122,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ (option @ TA))]: ((these @ TA @ (insert @ (option @ TA) @ (some @ TA @ A) @ B)) = (insert @ TA @ A @ (these @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_135_these__insert__Some)).
% 61.52/20.64 thf(677,plain,((! [TA: $tType]: (! [A:TA,B:(set @ (option @ TA))]: ((these @ TA @ (insert @ (option @ TA) @ (some @ TA @ A) @ B)) = (insert @ TA @ A @ (these @ TA @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 61.52/20.64 thf(183,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)) => ((~ (member @ TA @ A @ B)) => (member @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_UnE)).
% 61.52/20.64 thf(861,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)) => ((~ (member @ TA @ A @ B)) => (member @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 61.52/20.64 thf(292,axiom,((! [A:char]: ((size_size @ variable @ (rVar @ A)) = (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_122_variable_Osize_I3_J)).
% 61.52/20.64 thf(1173,plain,((! [A:char]: ((size_size @ variable @ (rVar @ A)) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[292])).
% 61.52/20.64 thf(258,axiom,((! [A:(set @ (variable > real)),B:(variable > real),C:(set @ variable),D:(set @ (variable > real))]: (((static_selectlike @ A @ B @ (uminus_uminus @ (set @ variable) @ C)) = (static_selectlike @ D @ B @ (uminus_uminus @ (set @ variable) @ C))) = (! [E:(variable > real)]: ((denota1419872369iation @ E @ B @ C) => ((member @ (variable > real) @ E @ A) = (member @ (variable > real) @ E @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_213_selectlike__equal__cocond)).
% 61.52/20.64 thf(1078,plain,((! [A:(set @ (variable > real)),B:(variable > real),C:(set @ variable),D:(set @ (variable > real))]: (((static_selectlike @ A @ (B) @ (uminus_uminus @ (set @ variable) @ C)) = (static_selectlike @ D @ (B) @ (uminus_uminus @ (set @ variable) @ C))) = (! [E:(variable > real)]: ((denota1419872369iation @ (E) @ (B) @ C) => ((member @ (variable > real) @ (E) @ A) = (member @ (variable > real) @ (E) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[258])).
% 61.52/20.64 thf(280,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: (((uminus_uminus @ (set @ TA) @ A) = (uminus_uminus @ (set @ TA) @ B)) = (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_195_Compl__eq__Compl__iff)).
% 61.52/20.64 thf(1137,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: (((uminus_uminus @ (set @ TA) @ A) = (uminus_uminus @ (set @ TA) @ B)) = (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[280])).
% 61.52/20.64 thf(290,axiom,((! [A:(real > (variable > real)),B:char,C:denotational_interp,D:trm,E:denotational_interp,F:trm]: ((! [G:(variable > real)]: ((denota1419872369iation @ G @ (A @ (zero_zero @ real)) @ (insert @ variable @ (rVar @ B) @ (insert @ variable @ (dVar @ B) @ (bot_bot @ (set @ variable))))) => ((denota1863255036rm_sem @ C @ D @ G) = (denota1863255036rm_sem @ E @ F @ G)))) => ((denota1778088425es_ODE @ C @ A @ B @ D) = (denota1778088425es_ODE @ E @ A @ B @ F))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_same__ODE__same__sol)).
% 61.52/20.64 thf(1164,plain,((! [A:(real > (variable > real)),B:char,C:denotational_interp,D:trm,E:denotational_interp,F:trm]: ((! [G:(variable > real)]: ((denota1419872369iation @ (G) @ (A @ (zero_zero @ real)) @ (insert @ variable @ (rVar @ B) @ (insert @ variable @ (dVar @ B) @ (bot_bot @ (set @ variable))))) => ((denota1863255036rm_sem @ C @ D @ (G)) = (denota1863255036rm_sem @ E @ F @ (G))))) => ((denota1778088425es_ODE @ C @ (A) @ B @ D) = (denota1778088425es_ODE @ E @ (A) @ B @ F))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[290])).
% 61.52/20.64 thf(253,axiom,((! [A:(real > (variable > real)),B:trm,C:real]: ((denota1778088425es_ODE @ i @ A @ x @ (the @ trm @ (uSubst95898992stappt @ sigma @ (sup_sup @ (set @ variable) @ u @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable))))) @ B))) => (denota1419872369iation @ (A @ C) @ (A @ (zero_zero @ real)) @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_111_vaflow1)).
% 61.52/20.64 thf(1063,plain,((! [A:(real > (variable > real)),B:trm,C:real]: ((denota1778088425es_ODE @ i @ (A) @ x @ (the @ trm @ (uSubst95898992stappt @ sigma @ (sup_sup @ (set @ variable) @ u @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable))))) @ B))) => (denota1419872369iation @ (A @ C) @ (A @ (zero_zero @ real)) @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[253])).
% 61.52/20.64 thf(17,axiom,((! [TA: $tType]: ((semilattice_inf @ TA) => (! [A:TA,B:TA]: ((inf_inf @ TA @ A @ (inf_inf @ TA @ A @ B)) = (inf_inf @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_239_inf_Oleft__idem)).
% 61.52/20.64 thf(340,plain,((! [TA: $tType]: ((semilattice_inf @ TA) => (! [A:TA,B:TA]: ((inf_inf @ TA @ A @ (inf_inf @ TA @ A @ B)) = (inf_inf @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 61.52/20.64 thf(265,axiom,((denotational_repv = (^ [A:(variable > real),B:variable,C:real,D:variable]: (if @ real @ (B = D) @ C @ (A @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_repv__def__correct)).
% 61.52/20.64 thf(1095,plain,(((denotational_repv) = (^ [A:(variable > real),B:variable,C:real,D:variable]: (if @ real @ (B = D) @ C @ (A @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[265])).
% 61.52/20.64 thf(300,axiom,((! [TA: $tType]: (! [A:(set @ (option @ TA))]: (((these @ TA @ A) != (bot_bot @ (set @ TA))) = ((A != (bot_bot @ (set @ (option @ TA)))) & (A != (insert @ (option @ TA) @ (none @ TA) @ (bot_bot @ (set @ (option @ TA)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_these__not__empty__eq)).
% 61.52/20.64 thf(1196,plain,((! [TA: $tType]: (! [A:(set @ (option @ TA))]: ((~ ((these @ TA @ A) = (bot_bot @ (set @ TA)))) = (~ (A = (bot_bot @ (set @ (option @ TA)))) & ~ (A = (insert @ (option @ TA) @ (none @ TA) @ (bot_bot @ (set @ (option @ TA)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[300])).
% 61.52/20.64 thf(231,axiom,((! [A:(variable > real),B:(variable > real)]: ((denota1419872369iation @ A @ B @ (bot_bot @ (set @ variable))) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_Uvariation__empty)).
% 61.52/20.64 thf(1001,plain,((! [A:(variable > real),B:(variable > real)]: ((denota1419872369iation @ (A) @ (B) @ (bot_bot @ (set @ variable))) = ((A) = (B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[231])).
% 61.52/20.64 thf(39,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_224_usubstappt__times__conv)).
% 61.52/20.64 thf(417,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)],[39])).
% 61.52/20.64 thf(47,axiom,((! [A:(variable > real),B:(variable > real)]: ((stateinterpol @ A @ B @ (statediff @ A @ B)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_227_stateinterpol__diff)).
% 61.52/20.64 thf(436,plain,((! [A:(variable > real),B:(variable > real)]: ((stateinterpol @ A @ B @ (statediff @ A @ B)) = (A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 61.52/20.64 thf(221,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((? [B:TA]: (member @ TA @ B @ A)) = (A != (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_ex__in__conv)).
% 61.52/20.64 thf(973,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((? [B:TA]: (member @ TA @ B @ A)) = (~ (A = (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 61.52/20.64 thf(191,axiom,((denota1419872369iation = (^ [A:(variable > real),B:(variable > real)]: (denota1419872369iation @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_Uvariation__sym)).
% 61.52/20.64 thf(885,plain,(((denota1419872369iation) = (^ [A:(variable > real),B:(variable > real)]: (denota1419872369iation @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 61.52/20.64 thf(97,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((A != (none @ TA)) => (member @ TA @ (the @ TA @ A) @ (set_option @ TA @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_185_option_Oset__sel)).
% 61.52/20.64 thf(570,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ((~ (A = (none @ TA))) => (member @ TA @ (the @ TA @ A) @ (set_option @ TA @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 61.52/20.64 thf(72,axiom,((bot @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Obot_7)).
% 61.52/20.64 thf(504,plain,((bot @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 61.52/20.64 thf(23,axiom,((semilattice_inf @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Lattices_Osemilattice__inf_4)).
% 61.52/20.64 thf(357,plain,((semilattice_inf @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 61.52/20.64 thf(252,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: (((~ (member @ TA @ A @ B)) => (member @ TA @ A @ C)) => (member @ TA @ A @ (sup_sup @ (set @ TA) @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_UnCI)).
% 61.52/20.64 thf(1059,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: (((~ (member @ TA @ A @ B)) => (member @ TA @ A @ C)) => (member @ TA @ A @ (sup_sup @ (set @ TA) @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[252])).
% 61.52/20.64 thf(213,axiom,((! [TA: $tType]: (lattice @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Lattices_Olattice_13)).
% 61.52/20.64 thf(949,plain,((! [TA: $tType]: (lattice @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 61.52/20.64 thf(88,axiom,((lattice @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Lattices_Olattice_6)).
% 61.52/20.64 thf(542,plain,((lattice @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 61.52/20.64 thf(131,axiom,((! [TA: $tType]: ((zero @ TA) => (! [A:TA]: (((zero_zero @ TA) = A) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_zero__reorient)).
% 61.52/20.64 thf(702,plain,((! [TA: $tType]: ((zero @ TA) => (! [A:TA]: (((zero_zero @ TA) = A) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 61.52/20.64 thf(148,axiom,((! [TA: $tType]: ((zero @ TA) => (zero @ (set @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Groups_Ozero_16)).
% 61.52/20.64 thf(751,plain,((! [TA: $tType]: ((zero @ TA) => (zero @ (set @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 61.52/20.64 thf(110,axiom,((! [A:char,B:char]: (((dVar @ A) = (dVar @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_variable_Oinject_I2_J)).
% 61.52/20.64 thf(638,plain,((! [A:char,B:char]: (((dVar @ A) = (dVar @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 61.52/20.64 thf(187,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_234_subsetI)).
% 61.52/20.64 thf(870,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)],[187])).
% 61.52/20.64 thf(220,axiom,((! [A:variable]: ((! [B:char]: (A != (rVar @ B))) => (~ (! [B:char]: (A != (dVar @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_variable_Oexhaust)).
% 61.52/20.64 thf(969,plain,((! [A:variable]: ((! [B:char]: ~ (A = (rVar @ B))) => (~ (! [B:char]: ~ (A = (dVar @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 61.52/20.64 thf(11,axiom,((! [TA: $tType]: (! [A:TA,B:(option @ TA)]: ((member @ TA @ A @ (set_option @ TA @ B)) => (B = (some @ TA @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_174_option_Oset__cases)).
% 61.52/20.64 thf(325,plain,((! [TA: $tType]: (! [A:TA,B:(option @ TA)]: ((member @ TA @ A @ (set_option @ TA @ B)) => (B = (some @ TA @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 61.52/20.64 thf(267,axiom,((! [TA: $tType]: ((lattice @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C)) = (sup_sup @ TA @ B @ (sup_sup @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_inf__sup__aci_I7_J)).
% 61.52/20.64 thf(1100,plain,((! [TA: $tType]: ((lattice @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C)) = (sup_sup @ TA @ B @ (sup_sup @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[267])).
% 61.52/20.64 thf(235,axiom,((stateinterpol = (^ [A:(variable > real),B:(variable > real),C:(set @ variable),D:variable]: (if @ real @ (member @ variable @ D @ C) @ (A @ D) @ (B @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_223_stateinterpol__def)).
% 61.52/20.64 thf(1013,plain,(((stateinterpol) = (^ [A:(variable > real),B:(variable > real),C:(set @ variable),D:variable]: (if @ real @ (member @ variable @ D @ C) @ (A @ D) @ (B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 61.52/20.64 thf(153,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ (bot_bot @ (set @ TA))) = (A = (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_253_subset__empty)).
% 61.52/20.64 thf(770,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ (bot_bot @ (set @ TA))) = (A = (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 61.52/20.64 thf(62,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_183_option_Osimps_I5_J)).
% 61.52/20.64 thf(475,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)],[62])).
% 61.52/20.64 thf(150,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((~ (member @ TA @ A @ B)) => ((~ (member @ TA @ A @ C)) => (((insert @ TA @ A @ B) = (insert @ TA @ A @ C)) = (B = C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_insert__ident)).
% 61.52/20.64 thf(756,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((~ (member @ TA @ A @ B)) => ((~ (member @ TA @ A @ C)) => (((insert @ TA @ A @ B) = (insert @ TA @ A @ C)) = (B = C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 61.52/20.64 thf(50,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((A != (none @ TA)) = (? [B:TA]: (A = (some @ TA @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_not__None__eq)).
% 61.52/20.64 thf(443,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ((~ (A = (none @ TA))) = (? [B:TA]: (A = (some @ TA @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 61.52/20.64 thf(285,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((sup_sup @ (set @ TA) @ (insert @ TA @ A @ B) @ C) = (insert @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_Un__insert__left)).
% 61.52/20.64 thf(1151,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((sup_sup @ (set @ TA) @ (insert @ TA @ A @ B) @ C) = (insert @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[285])).
% 61.52/20.64 thf(20,axiom,((! [TA: $tType,TB: $tType]: ((semilattice_inf @ TB) => ((inf_inf @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (inf_inf @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_inf__apply)).
% 61.52/20.64 thf(348,plain,((! [TA: $tType,TB: $tType]: ((semilattice_inf @ TB) => ((inf_inf @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (inf_inf @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 61.52/20.64 thf(219,axiom,((! [A:(variable > real),B:variable,C:real,D:(set @ (variable > real))]: ((member @ (variable > real) @ (denotational_repv @ A @ B @ C) @ (static_selectlike @ D @ A @ (insert @ variable @ B @ (bot_bot @ (set @ variable))))) = ((C = (A @ B)) & (member @ (variable > real) @ A @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_repv__selectlike__self)).
% 61.52/20.64 thf(966,plain,((! [A:(variable > real),B:variable,C:real,D:(set @ (variable > real))]: ((member @ (variable > real) @ (denotational_repv @ A @ B @ C) @ (static_selectlike @ D @ (A) @ (insert @ variable @ B @ (bot_bot @ (set @ variable))))) = ((C = (A @ B)) & (member @ (variable > real) @ (A) @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 61.52/20.64 thf(168,axiom,((zero @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Ozero_30)).
% 61.52/20.64 thf(821,plain,((zero @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 61.52/20.64 thf(271,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_69_Uvariation__sym__rel)).
% 61.52/20.64 thf(1109,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)],[271])).
% 61.52/20.64 thf(9,axiom,((! [TA: $tType]: (! [A:TA,B:(option @ TA)]: ((member @ TA @ A @ (set_option @ TA @ B)) = (B = (some @ TA @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_167_elem__set)).
% 61.52/20.64 thf(321,plain,((! [TA: $tType]: (! [A:TA,B:(option @ TA)]: ((member @ TA @ A @ (set_option @ TA @ B)) = (B = (some @ TA @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 61.52/20.64 thf(99,axiom,((! [TA: $tType]: (! [A:TA]: (member @ TA @ A @ (set_option @ TA @ (some @ TA @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_173_option_Oset__intros)).
% 61.52/20.64 thf(602,plain,((! [TA: $tType]: (! [A:TA]: (member @ TA @ A @ (set_option @ TA @ (some @ TA @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 61.52/20.64 thf(33,axiom,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA,B:TA]: ((A = (uminus_uminus @ TA @ B)) = (B = (uminus_uminus @ TA @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_205_equation__minus__iff)).
% 61.52/20.64 thf(397,plain,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA,B:TA]: ((A = (uminus_uminus @ TA @ B)) = (B = (uminus_uminus @ TA @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 61.52/20.64 thf(142,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o)]: ((! [D:TA]: ((member @ TA @ D @ (sup_sup @ (set @ TA) @ A @ B)) => (C @ D))) = (! [D:TA]: ((member @ TA @ D @ A) => (C @ D)) & ! [D:TA]: ((member @ TA @ D @ B) => (C @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_64_ball__Un)).
% 61.52/20.64 thf(734,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o)]: ((! [D:TA]: ((member @ TA @ D @ (sup_sup @ (set @ TA) @ A @ B)) => (C @ D))) = (! [D:TA]: ((member @ TA @ D @ A) => (C @ D)) & ! [D:TA]: ((member @ TA @ D @ B) => (C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 61.52/20.64 thf(185,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ (sup_sup @ TA @ A @ B) @ C) = ((ord_less_eq @ TA @ A @ C) & (ord_less_eq @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_251_sup_Obounded__iff)).
% 61.52/20.64 thf(866,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ (sup_sup @ TA @ A @ B) @ C) = ((ord_less_eq @ TA @ A @ C) & (ord_less_eq @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 61.52/20.64 thf(256,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => ((sup_sup @ TA) = (^ [A:TA,B:TA]: (sup_sup @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_sup_Ocommute)).
% 61.52/20.64 thf(1072,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => ((sup_sup @ TA) = (^ [A:TA,B:TA]: (sup_sup @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[256])).
% 61.52/20.64 thf(230,axiom,((! [A:trm,B:denotational_interp,C:trm,D:denotational_interp,E:char,F:(real > (variable > real))]: ((? [G:(variable > real)]: ((denota1419872369iation @ G @ (F @ (zero_zero @ real)) @ (insert @ variable @ (rVar @ E) @ (insert @ variable @ (dVar @ E) @ (bot_bot @ (set @ variable))))) & ((denota1863255036rm_sem @ D @ C @ G) != (denota1863255036rm_sem @ B @ A @ G)))) = ((denota1419872369iation @ (rr @ A @ B @ C @ D @ E @ F) @ (F @ (zero_zero @ real)) @ (insert @ variable @ (rVar @ E) @ (insert @ variable @ (dVar @ E) @ (bot_bot @ (set @ variable))))) & ((denota1863255036rm_sem @ D @ C @ (rr @ A @ B @ C @ D @ E @ F)) != (denota1863255036rm_sem @ B @ A @ (rr @ A @ B @ C @ D @ E @ F))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86__092_060open_062_092_060forall_062x0_Ax1_Ax2_Ax3_Ax4_Ax5_O_A_I_092_060exists_062v6_O_AUvariation_Av6_A_Ix5_A0_J_A_123RVar_Ax4_M_ADVar_Ax4_125_A_092_060and_062_Aterm__sem_Ax3_Ax2_Av6_A_092_060noteq_062_Aterm__sem_Ax1_Ax0_Av6_J_A_061_A_IUvariation_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_A_Ix5_A0_J_A_123RVar_Ax4_M_ADVar_Ax4_125_A_092_060and_062_Aterm__sem_Ax3_Ax2_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_A_092_060noteq_062_Aterm__sem_Ax1_Ax0_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_J_092_060close_062)).
% 61.52/20.64 thf(998,plain,((! [A:trm,B:denotational_interp,C:trm,D:denotational_interp,E:char,F:(real > (variable > real))]: ((? [G:(variable > real)]: ((denota1419872369iation @ (G) @ (F @ (zero_zero @ real)) @ (insert @ variable @ (rVar @ E) @ (insert @ variable @ (dVar @ E) @ (bot_bot @ (set @ variable))))) & ~ ((denota1863255036rm_sem @ D @ C @ (G)) = (denota1863255036rm_sem @ B @ A @ (G))))) = ((denota1419872369iation @ (rr @ A @ B @ C @ D @ E @ F) @ (F @ (zero_zero @ real)) @ (insert @ variable @ (rVar @ E) @ (insert @ variable @ (dVar @ E) @ (bot_bot @ (set @ variable))))) & ~ ((denota1863255036rm_sem @ D @ C @ (rr @ A @ B @ C @ D @ E @ F)) = (denota1863255036rm_sem @ B @ A @ (rr @ A @ B @ C @ D @ E @ F))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 61.52/20.64 thf(43,axiom,((preorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Opreorder_21)).
% 61.52/20.64 thf(428,plain,((preorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 61.52/20.64 thf(81,axiom,((bounde1808546759up_bot @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Lattices_Obounded__semilattice__sup__bot_17)).
% 61.52/20.64 thf(527,plain,((bounde1808546759up_bot @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 61.52/20.64 thf(4,axiom,((! [A:$o]: ((A = ($true)) | (A = ($false))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_3_1_T)).
% 61.52/20.64 thf(307,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 61.52/20.64 thf(48,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_153_split__option__ex)).
% 61.52/20.64 thf(439,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)],[48])).
% 61.52/20.64 thf(90,axiom,((! [TA: $tType]: ((semilattice_inf @ TA) => (! [A:TA]: ((inf_inf @ TA @ A @ A) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_237_inf_Oidem)).
% 61.52/20.64 thf(546,plain,((! [TA: $tType]: ((semilattice_inf @ TA) => (! [A:TA]: ((inf_inf @ TA @ A @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 61.52/20.64 thf(205,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ (uminus_uminus @ (set @ TA) @ B)) = (~ (member @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_196_Compl__iff)).
% 61.52/20.64 thf(925,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ (uminus_uminus @ (set @ TA) @ B)) = (~ (member @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 61.52/20.64 thf(301,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:TA,D:TA]: (((insert @ TA @ A @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) = (insert @ TA @ C @ (insert @ TA @ D @ (bot_bot @ (set @ TA))))) = (((A = C) & (B = D)) | ((A = D) & (B = C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_doubleton__eq__iff)).
% 61.52/20.64 thf(1199,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:TA,D:TA]: (((insert @ TA @ A @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) = (insert @ TA @ C @ (insert @ TA @ D @ (bot_bot @ (set @ TA))))) = (((A = C) & (B = D)) | ((A = D) & (B = C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[301])).
% 61.52/20.64 thf(164,axiom,((! [A:(variable > real),B:variable,C:real]: (denota1419872369iation @ A @ (denotational_repv @ A @ B @ C) @ (insert @ variable @ B @ (bot_bot @ (set @ variable)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_125_Uvariation__repv)).
% 61.52/20.64 thf(810,plain,((! [A:(variable > real),B:variable,C:real]: (denota1419872369iation @ (A) @ (denotational_repv @ A @ B @ C) @ (insert @ variable @ B @ (bot_bot @ (set @ variable)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 61.52/20.64 thf(27,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((A != (none @ TA)) => ((some @ TA @ (the @ TA @ A)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_145_option_Ocollapse)).
% 61.52/20.64 thf(366,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ((~ (A = (none @ TA))) => ((some @ TA @ (the @ TA @ A)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 61.52/20.64 thf(85,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((A != (none @ TA)) => (~ (! [B:TA]: (A != (some @ TA @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_151_option_Oexhaust)).
% 61.52/20.64 thf(534,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ((~ (A = (none @ TA))) => (~ (! [B:TA]: ~ (A = (some @ TA @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 61.52/20.64 thf(248,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ A) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_sup__idem)).
% 61.52/20.64 thf(1047,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[248])).
% 61.52/20.64 thf(161,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA]: (((~ (member @ TA @ A @ B)) => (A = C)) => (member @ TA @ A @ (insert @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_insertCI)).
% 61.52/20.64 thf(798,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA]: (((~ (member @ TA @ A @ B)) => (A = C)) => (member @ TA @ A @ (insert @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 61.52/20.64 thf(289,axiom,((semilattice_inf @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Lattices_Osemilattice__inf_26)).
% 61.52/20.64 thf(1163,plain,((semilattice_inf @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[289])).
% 61.52/20.64 thf(195,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(TA > $o)]: ((! [D:TA]: ((member @ TA @ D @ (insert @ TA @ A @ B)) => (C @ D))) = ((C @ A) & ! [D:TA]: ((member @ TA @ D @ B) => (C @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_ball__insert)).
% 61.52/20.64 thf(894,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(TA > $o)]: ((! [D:TA]: ((member @ TA @ D @ (insert @ TA @ A @ B)) => (C @ D))) = ((C @ A) & ! [D:TA]: ((member @ TA @ D @ B) => (C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 61.52/20.64 thf(146,axiom,((! [A:(variable > real),B:(variable > real)]: (denotational_Vagree @ A @ B @ (bot_bot @ (set @ variable))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_181_Vagree__empty)).
% 61.52/20.64 thf(746,plain,((! [A:(variable > real),B:(variable > real)]: (denotational_Vagree @ (A) @ (B) @ (bot_bot @ (set @ variable))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 61.52/20.64 thf(156,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: (member @ TA @ A @ (insert @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_insertI1)).
% 61.52/20.64 thf(778,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: (member @ TA @ A @ (insert @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 61.52/20.64 thf(246,axiom,((! [TA: $tType]: (semilattice_sup @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Lattices_Osemilattice__sup_9)).
% 61.52/20.64 thf(1042,plain,((! [TA: $tType]: (semilattice_sup @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[246])).
% 61.52/20.64 thf(94,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_159_Assigno_Oinduct)).
% 61.52/20.64 thf(561,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)],[94])).
% 61.52/20.64 thf(41,axiom,(((none @ trm) = (none @ trm))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_118_undeft__None)).
% 61.52/20.64 thf(424,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 61.52/20.64 thf(44,axiom,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA]: ((uminus_uminus @ TA @ (uminus_uminus @ TA @ A)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_191_add_Oinverse__inverse)).
% 61.52/20.64 thf(429,plain,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA]: ((uminus_uminus @ TA @ (uminus_uminus @ TA @ A)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 61.52/20.64 thf(158,axiom,((! [A:(variable > real),B:(variable > real),C:(set @ variable),D:trm,E:denotational_interp]: ((denota1419872369iation @ A @ B @ C) => (((inf_inf @ (set @ variable) @ (static_FVT @ D) @ C) = (bot_bot @ (set @ variable))) => ((denota1863255036rm_sem @ E @ D @ A) = (denota1863255036rm_sem @ E @ D @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_coincidence__term__cor)).
% 61.52/20.64 thf(788,plain,((! [A:(variable > real),B:(variable > real),C:(set @ variable),D:trm,E:denotational_interp]: ((denota1419872369iation @ (A) @ (B) @ C) => (((inf_inf @ (set @ variable) @ (static_FVT @ D) @ C) = (bot_bot @ (set @ variable))) => ((denota1863255036rm_sem @ E @ D @ (A)) = (denota1863255036rm_sem @ E @ D @ (B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 61.52/20.64 thf(166,axiom,((! [A:variable,B:(variable > real),C:(variable > real)]: ((~ (member @ variable @ A @ (statediff @ B @ C))) => ((B @ A) = (C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_nostatediff)).
% 61.52/20.64 thf(815,plain,((! [A:variable,B:(variable > real),C:(variable > real)]: ((~ (member @ variable @ A @ (statediff @ (B) @ (C)))) => ((B @ A) = (C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 61.52/20.64 thf(38,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_121_option_Oexpand)).
% 61.52/20.64 thf(407,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)],[38])).
% 61.52/20.64 thf(128,axiom,((! [A:(real > (variable > real)),B:trm,C:real]: ((denota1778088425es_ODE @ (uSubst2091380086djoint @ sigma @ i @ omega) @ A @ x @ B) => (denota1419872369iation @ (A @ C) @ (A @ (zero_zero @ real)) @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_105_vaflow2)).
% 61.52/20.64 thf(693,plain,((! [A:(real > (variable > real)),B:trm,C:real]: ((denota1778088425es_ODE @ (uSubst2091380086djoint @ sigma @ i @ (omega)) @ (A) @ x @ B) => (denota1419872369iation @ (A @ C) @ (A @ (zero_zero @ real)) @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 61.52/20.64 thf(107,axiom,((! [TA: $tType]: ((lattice @ TA) => ((sup_sup @ TA) = (^ [A:TA,B:TA]: (sup_sup @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_inf__sup__aci_I5_J)).
% 61.52/20.64 thf(630,plain,((! [TA: $tType]: ((lattice @ TA) => ((sup_sup @ TA) = (^ [A:TA,B:TA]: (sup_sup @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 61.52/20.64 thf(65,axiom,((! [A:(variable > real),B:(set @ variable)]: (denotational_Vagree @ A @ A @ B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_179_Vagree__refl)).
% 61.52/20.64 thf(484,plain,((! [A:(variable > real),B:(set @ variable)]: (denotational_Vagree @ (A) @ (A) @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 61.52/20.64 thf(105,axiom,((! [TA: $tType]: (semilattice_inf @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Lattices_Osemilattice__inf_10)).
% 61.52/20.64 thf(625,plain,((! [TA: $tType]: (semilattice_inf @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 61.52/20.64 thf(189,axiom,((! [A:(set @ (variable > real)),B:(variable > real),C:(set @ variable),D:(set @ variable)]: ((static_selectlike @ (static_selectlike @ A @ B @ C) @ B @ D) = (static_selectlike @ A @ B @ (sup_sup @ (set @ variable) @ C @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_144_selectlike__compose)).
% 61.52/20.65 thf(879,plain,((! [A:(set @ (variable > real)),B:(variable > real),C:(set @ variable),D:(set @ variable)]: ((static_selectlike @ (static_selectlike @ A @ (B) @ C) @ (B) @ D) = (static_selectlike @ A @ (B) @ (sup_sup @ (set @ variable) @ C @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 61.52/20.65 thf(46,axiom,((preorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Opreorder_5)).
% 61.52/20.65 thf(435,plain,((preorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 61.52/20.65 thf(173,axiom,((uminus @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Ouminus_29)).
% 61.52/20.65 thf(830,plain,((uminus @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 61.52/20.65 thf(193,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((uminus_uminus @ (set @ TA) @ (uminus_uminus @ (set @ TA) @ A)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_double__complement)).
% 61.52/20.65 thf(889,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((uminus_uminus @ (set @ TA) @ (uminus_uminus @ (set @ TA) @ A)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 61.52/20.65 thf(56,axiom,((semilattice_sup @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Lattices_Osemilattice__sup_18)).
% 61.52/20.65 thf(461,plain,((semilattice_sup @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 61.52/20.65 thf(240,axiom,((! [TA: $tType]: (bounde1808546759up_bot @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Lattices_Obounded__semilattice__sup__bot_8)).
% 61.52/20.65 thf(1027,plain,((! [TA: $tType]: (bounde1808546759up_bot @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 61.52/20.65 thf(277,axiom,((! [A:(variable > real),B:(variable > real),C:(set @ variable),D:(set @ variable)]: (((denotational_Vagree @ A @ B @ C) & (denotational_Vagree @ A @ B @ D)) = (denotational_Vagree @ A @ B @ (sup_sup @ (set @ variable) @ C @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_168_Vagree__and)).
% 61.52/20.65 thf(1128,plain,((! [A:(variable > real),B:(variable > real),C:(set @ variable),D:(set @ variable)]: (((denotational_Vagree @ (A) @ (B) @ C) & (denotational_Vagree @ (A) @ (B) @ D)) = (denotational_Vagree @ (A) @ (B) @ (sup_sup @ (set @ variable) @ C @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[277])).
% 61.52/20.65 thf(10,axiom,((boolean_algebra @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Lattices_Oboolean__algebra_20)).
% 61.52/20.65 thf(324,plain,((boolean_algebra @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 61.52/20.65 thf(270,axiom,((! [TA: $tType]: (! [A:(char > TA),B:(char > TA),C:char]: ((rec_variable @ TA @ A @ B @ (rVar @ C)) = (A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_128_variable_Osimps_I7_J)).
% 61.52/20.65 thf(1106,plain,((! [TA: $tType]: (! [A:(char > TA),B:(char > TA),C:char]: ((rec_variable @ TA @ (A) @ (B) @ (rVar @ C)) = (A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[270])).
% 61.52/20.65 thf(124,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: (((sup_sup @ (set @ TA) @ A @ B) = (insert @ TA @ C @ (bot_bot @ (set @ TA)))) = (((A = (bot_bot @ (set @ TA))) & (B = (insert @ TA @ C @ (bot_bot @ (set @ TA))))) | ((A = (insert @ TA @ C @ (bot_bot @ (set @ TA)))) & (B = (bot_bot @ (set @ TA)))) | ((A = (insert @ TA @ C @ (bot_bot @ (set @ TA)))) & (B = (insert @ TA @ C @ (bot_bot @ (set @ TA)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_Un__singleton__iff)).
% 61.52/20.65 thf(682,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: (((sup_sup @ (set @ TA) @ A @ B) = (insert @ TA @ C @ (bot_bot @ (set @ TA)))) = (((A = (bot_bot @ (set @ TA))) & (B = (insert @ TA @ C @ (bot_bot @ (set @ TA))))) | ((A = (insert @ TA @ C @ (bot_bot @ (set @ TA)))) & (B = (bot_bot @ (set @ TA)))) | ((A = (insert @ TA @ C @ (bot_bot @ (set @ TA)))) & (B = (insert @ TA @ C @ (bot_bot @ (set @ TA)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 61.52/20.65 thf(299,axiom,((preorder @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Opreorder_27)).
% 61.52/20.65 thf(1195,plain,((preorder @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[299])).
% 61.52/20.65 thf(188,axiom,((~ (! [A:(trm > (denotational_interp > (trm > (denotational_interp > (char > ((real > (variable > real)) > (variable > real)))))))]: ~ (! [B:trm,C:denotational_interp,D:trm,E:denotational_interp,F:char,G:(real > (variable > real))]: ((? [H:(variable > real)]: ((denota1419872369iation @ H @ (G @ (zero_zero @ real)) @ (insert @ variable @ (rVar @ F) @ (insert @ variable @ (dVar @ F) @ (bot_bot @ (set @ variable))))) & ((denota1863255036rm_sem @ E @ D @ H) != (denota1863255036rm_sem @ C @ B @ H)))) = ((denota1419872369iation @ (A @ B @ C @ D @ E @ F @ G) @ (G @ (zero_zero @ real)) @ (insert @ variable @ (rVar @ F) @ (insert @ variable @ (dVar @ F) @ (bot_bot @ (set @ variable))))) & ((denota1863255036rm_sem @ E @ D @ (A @ B @ C @ D @ E @ F @ G)) != (denota1863255036rm_sem @ C @ B @ (A @ B @ C @ D @ E @ F @ G))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062rr_O_A_092_060forall_062x0_Ax1_Ax2_Ax3_Ax4_Ax5_O_A_I_092_060exists_062v6_O_AUvariation_Av6_A_Ix5_A0_J_A_123RVar_Ax4_M_ADVar_Ax4_125_A_092_060and_062_Aterm__sem_Ax3_Ax2_Av6_A_092_060noteq_062_Aterm__sem_Ax1_Ax0_Av6_J_A_061_A_IUvariation_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_A_Ix5_A0_J_A_123RVar_Ax4_M_ADVar_Ax4_125_A_092_060and_062_Aterm__sem_Ax3_Ax2_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_A_092_060noteq_062_Aterm__sem_Ax1_Ax0_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_J_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062)).
% 61.52/20.65 thf(874,plain,((~ (! [A:(trm > (denotational_interp > (trm > (denotational_interp > (char > ((real > (variable > real)) > (variable > real)))))))]: ~ (! [B:trm,C:denotational_interp,D:trm,E:denotational_interp,F:char,G:(real > (variable > real))]: ((? [H:(variable > real)]: ((denota1419872369iation @ (H) @ (G @ (zero_zero @ real)) @ (insert @ variable @ (rVar @ F) @ (insert @ variable @ (dVar @ F) @ (bot_bot @ (set @ variable))))) & ~ ((denota1863255036rm_sem @ E @ D @ (H)) = (denota1863255036rm_sem @ C @ B @ (H))))) = ((denota1419872369iation @ (A @ B @ C @ D @ E @ F @ G) @ (G @ (zero_zero @ real)) @ (insert @ variable @ (rVar @ F) @ (insert @ variable @ (dVar @ F) @ (bot_bot @ (set @ variable))))) & ~ ((denota1863255036rm_sem @ E @ D @ (A @ B @ C @ D @ E @ F @ G)) = (denota1863255036rm_sem @ C @ B @ (A @ B @ C @ D @ E @ F @ G))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 61.52/20.65 thf(8,axiom,((! [A:(variable > real),B:(variable > real),C:(set @ variable),D:(set @ (variable > real))]: ((denotational_Vagree @ A @ B @ C) => ((static_selectlike @ D @ A @ C) = (static_selectlike @ D @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_171_selectlike__Vagree)).
% 61.52/20.65 thf(317,plain,((! [A:(variable > real),B:(variable > real),C:(set @ variable),D:(set @ (variable > real))]: ((denotational_Vagree @ (A) @ (B) @ C) => ((static_selectlike @ D @ (A) @ C) = (static_selectlike @ D @ (B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 61.52/20.65 thf(114,axiom,((! [TA: $tType]: ((insert @ TA) = (^ [A:TA]: (sup_sup @ (set @ TA) @ (insert @ TA @ A @ (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_insert__is__Un)).
% 61.52/20.65 thf(650,plain,((! [TA: $tType]: ((insert @ TA) = (^ [A:TA]: (sup_sup @ (set @ TA) @ (insert @ TA @ A @ (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 61.52/20.65 thf(272,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: (((sup_sup @ (set @ TA) @ A @ B) = (bot_bot @ (set @ TA))) = ((A = (bot_bot @ (set @ TA))) & (B = (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_Un__empty)).
% 61.52/20.65 thf(1111,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: (((sup_sup @ (set @ TA) @ A @ B) = (bot_bot @ (set @ TA))) = ((A = (bot_bot @ (set @ TA))) & (B = (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[272])).
% 61.52/20.65 thf(139,axiom,((! [TA: $tType]: (uminus @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Groups_Ouminus_15)).
% 61.52/20.65 thf(725,plain,((! [TA: $tType]: (uminus @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 61.52/20.65 thf(224,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((! [B:TA]: ~ (member @ TA @ B @ A)) = (A = (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_all__not__in__conv)).
% 61.52/20.65 thf(980,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((! [B:TA]: ~ (member @ TA @ B @ A)) = (A = (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 61.52/20.65 thf(186,axiom,((denota1419872369iation @ (f @ (zero_zero @ real)) @ omega @ (sup_sup @ (set @ variable) @ u @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_uv)).
% 61.52/20.65 thf(869,plain,((denota1419872369iation @ (f @ (zero_zero @ real)) @ (omega) @ (sup_sup @ (set @ variable) @ u @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 61.52/20.65 thf(227,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((A = (sup_sup @ TA @ B @ C)) => ((sup_sup @ TA @ D @ A) = (sup_sup @ TA @ B @ (sup_sup @ TA @ D @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_boolean__algebra__cancel_Osup2)).
% 61.52/20.65 thf(989,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((A = (sup_sup @ TA @ B @ C)) => ((sup_sup @ TA @ D @ A) = (sup_sup @ TA @ B @ (sup_sup @ TA @ D @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 61.52/20.65 thf(288,axiom,((! [TA: $tType]: (! [A:(TA > $o)]: (((collect @ TA @ A) = (bot_bot @ (set @ TA))) = (! [B:TA]: ~ (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_Collect__empty__eq)).
% 61.52/20.65 thf(1160,plain,((! [TA: $tType]: (! [A:(TA > $o)]: (((collect @ TA @ (A)) = (bot_bot @ (set @ TA))) = (! [B:TA]: ~ (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[288])).
% 61.52/20.65 thf(260,axiom,((! [TA: $tType]: (! [A:(set @ (option @ TA))]: ((these @ TA @ (insert @ (option @ TA) @ (none @ TA) @ A)) = (these @ TA @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_132_these__insert__None)).
% 61.52/20.65 thf(1082,plain,((! [TA: $tType]: (! [A:(set @ (option @ TA))]: ((these @ TA @ (insert @ (option @ TA) @ (none @ TA) @ A)) = (these @ TA @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[260])).
% 61.52/20.65 thf(16,axiom,((semilattice_sup @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Lattices_Osemilattice__sup_3)).
% 61.52/20.65 thf(339,plain,((semilattice_sup @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 61.52/20.65 thf(149,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ A) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_Un__absorb)).
% 61.52/20.65 thf(753,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ A) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 61.52/20.65 thf(295,axiom,((! [A:(set @ (variable > real)),B:(variable > real),C:(set @ variable)]: ((static_selectlike @ (uminus_uminus @ (set @ (variable > real)) @ (static_selectlike @ A @ B @ C)) @ B @ C) = (static_selectlike @ (uminus_uminus @ (set @ (variable > real)) @ A) @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_220_selectlike__co__selectlike)).
% 61.52/20.65 thf(1182,plain,((! [A:(set @ (variable > real)),B:(variable > real),C:(set @ variable)]: ((static_selectlike @ (uminus_uminus @ (set @ (variable > real)) @ (static_selectlike @ A @ (B) @ C)) @ (B) @ C) = (static_selectlike @ (uminus_uminus @ (set @ (variable > real)) @ A) @ (B) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[295])).
% 61.52/20.65 thf(86,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_233_order__refl)).
% 61.52/20.65 thf(537,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 61.52/20.65 thf(257,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((! [B:TA]: ~ (member @ TA @ B @ A)) => (A = (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_equals0I)).
% 61.52/20.65 thf(1075,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((! [B:TA]: ~ (member @ TA @ B @ A)) => (A = (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[257])).
% 61.52/20.65 thf(67,axiom,((! [A:(variable > real),B:(variable > real),C:(set @ variable)]: ((denotational_Vagree @ A @ B @ C) => (denotational_Vagree @ B @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_180_Vagree__sym__rel)).
% 61.52/20.65 thf(489,plain,((! [A:(variable > real),B:(variable > real),C:(set @ variable)]: ((denotational_Vagree @ (A) @ (B) @ C) => (denotational_Vagree @ (B) @ (A) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 61.52/20.65 thf(245,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (sup_sup @ (set @ TA) @ A @ B)) = (sup_sup @ (set @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_60_Un__left__absorb)).
% 61.52/20.65 thf(1039,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (sup_sup @ (set @ TA) @ A @ B)) = (sup_sup @ (set @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[245])).
% 61.52/20.65 thf(12,axiom,((! [TA: $tType,TB: $tType]: ((lattice @ TA) => (lattice @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Lattices_Olattice)).
% 61.52/20.65 thf(328,plain,((! [TA: $tType,TB: $tType]: ((lattice @ TA) => (lattice @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 61.52/20.65 thf(61,axiom,((! [A:(variable > real),B:(variable > real),C:trm,D:denotational_interp]: ((denotational_Vagree @ A @ B @ (static_FVT @ C)) => ((denota1863255036rm_sem @ D @ C @ A) = (denota1863255036rm_sem @ D @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_coincidence__term)).
% 61.52/20.65 thf(471,plain,((! [A:(variable > real),B:(variable > real),C:trm,D:denotational_interp]: ((denotational_Vagree @ (A) @ (B) @ (static_FVT @ C)) => ((denota1863255036rm_sem @ D @ C @ (A)) = (denota1863255036rm_sem @ D @ C @ (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 61.52/20.65 thf(104,axiom,((! [TA: $tType,TB: $tType]: ((semilattice_sup @ TB) => ((sup_sup @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (sup_sup @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_sup__apply)).
% 61.52/20.65 thf(622,plain,((! [TA: $tType,TB: $tType]: ((semilattice_sup @ TB) => ((sup_sup @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (sup_sup @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 61.52/20.65 thf(273,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ (bot_bot @ TA) @ A) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_sup__bot_Oleft__neutral)).
% 61.52/20.65 thf(1114,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ (bot_bot @ TA) @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[273])).
% 61.52/20.65 thf(113,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((sup_sup @ (set @ TA) @ (sup_sup @ (set @ TA) @ A @ B) @ C) = (sup_sup @ (set @ TA) @ A @ (sup_sup @ (set @ TA) @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_Un__assoc)).
% 61.52/20.65 thf(647,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((sup_sup @ (set @ TA) @ (sup_sup @ (set @ TA) @ A @ B) @ C) = (sup_sup @ (set @ TA) @ A @ (sup_sup @ (set @ TA) @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 61.52/20.65 thf(278,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ (sup_sup @ TA @ A @ B) @ C) = (sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_sup__assoc)).
% 61.52/20.65 thf(1131,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ (sup_sup @ TA @ A @ B) @ C) = (sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[278])).
% 61.52/20.65 thf(298,axiom,((! [A:char]: ((size_size @ variable @ (dVar @ A)) = (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_123_variable_Osize_I4_J)).
% 61.52/20.65 thf(1192,plain,((! [A:char]: ((size_size @ variable @ (dVar @ A)) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[298])).
% 61.52/20.65 thf(249,axiom,((! [TA: $tType]: ((linord219039673up_add @ TA) => (! [A:TA]: (((uminus_uminus @ TA @ A) = A) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_neg__equal__zero)).
% 61.52/20.65 thf(1050,plain,((! [TA: $tType]: ((linord219039673up_add @ TA) => (! [A:TA]: (((uminus_uminus @ TA @ A) = A) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[249])).
% 61.52/20.65 thf(200,axiom,((! [A:(variable > real),B:(variable > real),C:(set @ variable)]: ((denota1419872369iation @ A @ B @ (uminus_uminus @ (set @ variable) @ C)) = (denotational_Vagree @ A @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_Uvariation__Vagree)).
% 61.52/20.65 thf(911,plain,((! [A:(variable > real),B:(variable > real),C:(set @ variable)]: ((denota1419872369iation @ (A) @ (B) @ (uminus_uminus @ (set @ variable) @ C)) = (denotational_Vagree @ (A) @ (B) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 61.52/20.65 thf(29,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((! [B:TA]: (A != (some @ TA @ B))) = (A = (none @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_142_not__Some__eq)).
% 61.52/20.65 thf(371,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ((! [B:TA]: ~ (A = (some @ TA @ B))) = (A = (none @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 61.52/20.65 thf(18,axiom,((! [TA: $tType,TB: $tType]: ((semilattice_inf @ TA) => (semilattice_inf @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Lattices_Osemilattice__inf)).
% 61.52/20.65 thf(343,plain,((! [TA: $tType,TB: $tType]: ((semilattice_inf @ TA) => (semilattice_inf @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 61.52/20.65 thf(108,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ B) => (member @ TA @ A @ (sup_sup @ (set @ TA) @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_UnI2)).
% 61.52/20.65 thf(633,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ B) => (member @ TA @ A @ (sup_sup @ (set @ TA) @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 61.52/20.65 thf(74,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_154_split__option__all)).
% 61.52/20.65 thf(508,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)],[74])).
% 61.52/20.65 thf(6,axiom,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ B)) = (B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_mem__Collect__eq)).
% 61.52/20.65 thf(311,plain,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ (B))) = (B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 61.52/20.65 thf(203,axiom,((ordered_ab_group_add @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Oordered__ab__group__add)).
% 61.52/20.65 thf(921,plain,((ordered_ab_group_add @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 61.52/20.65 thf(291,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((sup_sup @ (set @ TA) @ (bot_bot @ (set @ TA)) @ A) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_Un__empty__left)).
% 61.52/20.65 thf(1170,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((sup_sup @ (set @ TA) @ (bot_bot @ (set @ TA)) @ A) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[291])).
% 61.52/20.65 thf(121,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (bot_bot @ (set @ TA))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_Un__empty__right)).
% 61.52/20.65 thf(674,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (bot_bot @ (set @ TA))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 61.52/20.65 thf(296,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:TA]: ((A = (bot_bot @ (set @ TA))) => (~ (member @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_equals0D)).
% 61.52/20.65 thf(1185,plain,((! [TA: $tType]: (! [A:(set @ TA),B:TA]: ((A = (bot_bot @ (set @ TA))) => (~ (member @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[296])).
% 61.52/20.65 thf(154,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ (sup_sup @ TA @ A @ B) @ C) = ((ord_less_eq @ TA @ A @ C) & (ord_less_eq @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_250_le__sup__iff)).
% 61.52/20.65 thf(773,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ (sup_sup @ TA @ A @ B) @ C) = ((ord_less_eq @ TA @ A @ C) & (ord_less_eq @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 61.52/20.65 thf(302,axiom,((! [TA: $tType]: (bot @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Obot_14)).
% 61.52/20.65 thf(1202,plain,((! [TA: $tType]: (bot @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[302])).
% 61.52/20.65 thf(159,axiom,((! [TA: $tType]: (! [A:(TA > $o)]: (((collect @ TA @ A) = (bot_bot @ (set @ TA))) = (A = (bot_bot @ (TA > $o))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_Collect__empty__eq__bot)).
% 61.52/20.65 thf(792,plain,((! [TA: $tType]: (! [A:(TA > $o)]: (((collect @ TA @ (A)) = (bot_bot @ (set @ TA))) = ((A) = (bot_bot @ (TA > $o))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 61.52/20.65 thf(118,axiom,((! [A:variable,B:variable,C:(variable > real),D:real,E:(set @ (variable > real))]: ((A != B) => ((member @ (variable > real) @ (denotational_repv @ C @ A @ D) @ E) = (member @ (variable > real) @ (denotational_repv @ C @ A @ D) @ (static_selectlike @ E @ C @ (insert @ variable @ B @ (bot_bot @ (set @ variable))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_136_repv__selectlike__other__converse)).
% 61.52/20.65 thf(662,plain,((! [A:variable,B:variable,C:(variable > real),D:real,E:(set @ (variable > real))]: ((~ (A = B)) => ((member @ (variable > real) @ (denotational_repv @ C @ A @ D) @ E) = (member @ (variable > real) @ (denotational_repv @ C @ A @ D) @ (static_selectlike @ E @ (C) @ (insert @ variable @ B @ (bot_bot @ (set @ variable))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 61.52/20.65 thf(136,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: (ord_less_eq @ (set @ TA) @ (bot_bot @ (set @ TA)) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_252_empty__subsetI)).
% 61.52/20.65 thf(718,plain,((! [TA: $tType]: (! [A:(set @ TA)]: (ord_less_eq @ (set @ TA) @ (bot_bot @ (set @ TA)) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 61.52/20.65 thf(199,axiom,((! [A:(variable > $o),B:variable]: ((! [C:char]: (A @ (rVar @ C))) => ((! [C:char]: (A @ (dVar @ C))) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_variable_Oinduct)).
% 61.52/20.65 thf(906,plain,((! [A:(variable > $o),B:variable]: ((! [C:char]: (A @ (rVar @ C))) => ((! [C:char]: (A @ (dVar @ C))) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 61.52/20.65 thf(42,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ (option @ TA))]: ((member @ TA @ A @ (these @ TA @ B)) = (member @ (option @ TA) @ (some @ TA @ A) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_146_in__these__eq)).
% 61.52/20.65 thf(425,plain,((! [TA: $tType]: (! [A:TA,B:(set @ (option @ TA))]: ((member @ TA @ A @ (these @ TA @ B)) = (member @ (option @ TA) @ (some @ TA @ A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 61.52/20.65 thf(76,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((A != (none @ TA)) => (A = (some @ TA @ (the @ TA @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_162_option_Oexhaust__sel)).
% 61.52/20.65 thf(513,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ((~ (A = (none @ TA))) => (A = (some @ TA @ (the @ TA @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 61.52/20.65 thf(268,axiom,((! [A:(variable > real),B:(set @ variable)]: (denota1419872369iation @ A @ A @ B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_Uvariation__refl)).
% 61.52/20.65 thf(1103,plain,((! [A:(variable > real),B:(set @ variable)]: (denota1419872369iation @ (A) @ (A) @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[268])).
% 61.52/20.65 thf(98,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_216_Timeso_Oelims)).
% 61.52/20.65 thf(573,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)],[98])).
% 61.52/20.65 thf(286,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((sup_sup @ TA @ A @ B) = (bot_bot @ TA)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_sup__bot_Oeq__neutr__iff)).
% 61.52/20.65 thf(1154,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((sup_sup @ TA @ A @ B) = (bot_bot @ TA)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[286])).
% 61.52/20.65 thf(40,axiom,((bot @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Obot_23)).
% 61.52/20.65 thf(423,plain,((bot @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 61.52/20.65 thf(233,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ (sup_sup @ TA @ A @ B) @ C) = (sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_sup_Oassoc)).
% 61.52/20.65 thf(1007,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ (sup_sup @ TA @ A @ B) @ C) = (sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 61.52/20.65 thf(35,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_156_ODEo_Oinduct)).
% 61.52/20.65 thf(402,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)],[35])).
% 61.52/20.65 thf(145,axiom,((! [A:(real > (variable > real)),B:(variable > real),C:(set @ variable),D:denotational_interp,E:char,F:trm,G:real]: ((denota1419872369iation @ (A @ (zero_zero @ real)) @ B @ C) => ((denota1778088425es_ODE @ D @ A @ E @ F) => (denota1419872369iation @ (A @ G) @ B @ (sup_sup @ (set @ variable) @ C @ (insert @ variable @ (rVar @ E) @ (insert @ variable @ (dVar @ E) @ (bot_bot @ (set @ variable)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_solves__Vagree__trans)).
% 61.52/20.65 thf(743,plain,((! [A:(real > (variable > real)),B:(variable > real),C:(set @ variable),D:denotational_interp,E:char,F:trm,G:real]: ((denota1419872369iation @ (A @ (zero_zero @ real)) @ (B) @ C) => ((denota1778088425es_ODE @ D @ (A) @ E @ F) => (denota1419872369iation @ (A @ G) @ (B) @ (sup_sup @ (set @ variable) @ C @ (insert @ variable @ (rVar @ E) @ (insert @ variable @ (dVar @ E) @ (bot_bot @ (set @ variable)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 61.52/20.65 thf(216,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((insert @ TA @ A @ B) != (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_insert__not__empty)).
% 61.52/20.65 thf(958,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ~ ((insert @ TA @ A @ B) = (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 61.52/20.65 thf(276,axiom,((! [A:variable,B:(set @ variable),C:(variable > real),D:(variable > real)]: ((~ (member @ variable @ A @ B)) => ((stateinterpol @ C @ D @ B @ A) = (D @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_stateinterpol__right)).
% 61.52/20.65 thf(1124,plain,((! [A:variable,B:(set @ variable),C:(variable > real),D:(variable > real)]: ((~ (member @ variable @ A @ B)) => ((stateinterpol @ (C) @ (D) @ B @ A) = (D @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[276])).
% 61.52/20.65 thf(171,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA]: ((member @ TA @ A @ B) => (member @ TA @ A @ (insert @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_insertI2)).
% 61.52/20.65 thf(826,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA]: ((member @ TA @ A @ B) => (member @ TA @ A @ (insert @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 61.52/20.65 thf(134,axiom,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_emptyE)).
% 61.52/20.65 thf(711,plain,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 61.52/20.65 thf(111,axiom,((! [A:(variable > real),B:variable,C:real]: ((denotational_Vagree @ A @ (denotational_repv @ A @ B @ C) @ (insert @ variable @ B @ (bot_bot @ (set @ variable)))) = (C = (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_166_Vagree__repv__self)).
% 61.52/20.65 thf(641,plain,((! [A:(variable > real),B:variable,C:real]: ((denotational_Vagree @ (A) @ (denotational_repv @ A @ B @ C) @ (insert @ variable @ B @ (bot_bot @ (set @ variable)))) = (C = (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 61.52/20.65 thf(31,axiom,((! [TA: $tType]: ((semilattice_inf @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ (inf_inf @ TA @ B @ C)) = ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_249_inf_Obounded__iff)).
% 61.52/20.65 thf(391,plain,((! [TA: $tType]: ((semilattice_inf @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ (inf_inf @ TA @ B @ C)) = ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 61.52/20.65 thf(209,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (sup_sup @ (set @ TA) @ B @ C)) = (sup_sup @ (set @ TA) @ B @ (sup_sup @ (set @ TA) @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_Un__left__commute)).
% 61.52/20.65 thf(936,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (sup_sup @ (set @ TA) @ B @ C)) = (sup_sup @ (set @ TA) @ B @ (sup_sup @ (set @ TA) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 61.52/20.65 thf(103,axiom,((! [TA: $tType]: (! [A:(option @ TA),B:(TA > $o),C:TA]: ((! [D:TA]: ((member @ TA @ D @ (set_option @ TA @ A)) => (B @ D))) => ((A = (some @ TA @ C)) => (B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_175_ospec)).
% 61.52/20.65 thf(611,plain,((! [TA: $tType]: (! [A:(option @ TA),B:(TA > $o),C:TA]: ((! [D:TA]: ((member @ TA @ D @ (set_option @ TA @ A)) => (B @ D))) => ((A = (some @ TA @ C)) => (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 61.52/20.65 thf(135,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => (~ (! [C:(set @ TA)]: ((B = (insert @ TA @ A @ C)) => (member @ TA @ A @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_Set_Oset__insert)).
% 61.52/20.65 thf(713,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => (~ (! [C:(set @ TA)]: ((B = (insert @ TA @ A @ C)) => (member @ TA @ A @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 61.52/20.65 thf(264,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((member @ TA @ A @ (insert @ TA @ B @ C)) => ((A != B) => (member @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_insertE)).
% 61.52/20.65 thf(1092,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((member @ TA @ A @ (insert @ TA @ B @ C)) => ((~ (A = B)) => (member @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[264])).
% 61.52/20.65 thf(14,axiom,((canoni770627133id_add @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocanonically__ordered__monoid__add)).
% 61.52/20.65 thf(335,plain,((canoni770627133id_add @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 61.52/20.65 thf(263,axiom,((! [TA: $tType]: (! [A:TA]: (member @ TA @ A @ (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_singletonI)).
% 61.52/20.65 thf(1090,plain,((! [TA: $tType]: (! [A:TA]: (member @ TA @ A @ (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[263])).
% 61.52/20.65 thf(162,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ (bot_bot @ TA)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_sup__bot__right)).
% 61.52/20.65 thf(804,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ (bot_bot @ TA)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 61.52/20.65 thf(120,axiom,((! [A:(variable > real),B:variable,C:real]: (denotational_Vagree @ A @ (denotational_repv @ A @ B @ C) @ (uminus_uminus @ (set @ variable) @ (insert @ variable @ B @ (bot_bot @ (set @ variable))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_Vagree__repv)).
% 61.52/20.65 thf(672,plain,((! [A:(variable > real),B:variable,C:real]: (denotational_Vagree @ (A) @ (denotational_repv @ A @ B @ C) @ (uminus_uminus @ (set @ variable) @ (insert @ variable @ B @ (bot_bot @ (set @ variable))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 61.52/20.65 thf(174,axiom,((denotational_repv = (^ [A:(variable > real),B:variable,C:real,D:variable]: (if @ real @ (B = D) @ C @ (A @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_130_repv__access)).
% 61.52/20.65 thf(831,plain,(((denotational_repv) = (^ [A:(variable > real),B:variable,C:real,D:variable]: (if @ real @ (B = D) @ C @ (A @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 61.52/20.65 thf(274,axiom,((! [TA: $tType]: ((bot_bot @ (set @ TA)) = (collect @ TA @ (bot_bot @ (TA > $o)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_bot__set__def)).
% 61.52/20.65 thf(1117,plain,((! [TA: $tType]: ((bot_bot @ (set @ TA)) = (collect @ TA @ (bot_bot @ (TA > $o)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[274])).
% 61.52/20.65 thf(143,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => ((sup_sup @ TA) = (^ [A:TA,B:TA]: (sup_sup @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_sup__commute)).
% 61.52/20.65 thf(737,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => ((sup_sup @ TA) = (^ [A:TA,B:TA]: (sup_sup @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 61.52/20.65 thf(1,conjecture,((denota1419872369iation @ (f @ (zero_zero @ real)) @ omega @ (sup_sup @ (set @ variable) @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable)))) @ u))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 61.52/20.65 thf(2,negated_conjecture,((~ (denota1419872369iation @ (f @ (zero_zero @ real)) @ omega @ (sup_sup @ (set @ variable) @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable)))) @ u)))),inference(neg_conjecture,[status(cth)],[1])).
% 61.52/20.65 thf(303,plain,((~ (denota1419872369iation @ (f @ (zero_zero @ real)) @ (omega) @ (sup_sup @ (set @ variable) @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable)))) @ u)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 61.52/20.65 thf(184,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)) = ((member @ TA @ A @ B) | (member @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_union__or)).
% 61.52/20.65 thf(863,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)) = ((member @ TA @ A @ B) | (member @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 61.52/20.65 thf(152,axiom,((! [A:(real > (variable > real)),B:char,C:denotational_interp,D:trm,E:denotational_interp,F:trm]: (((denota1419872369iation @ (rr @ F @ E @ D @ C @ B @ A) @ (A @ (zero_zero @ real)) @ (insert @ variable @ (rVar @ B) @ (insert @ variable @ (dVar @ B) @ (bot_bot @ (set @ variable))))) & ((denota1863255036rm_sem @ C @ D @ (rr @ F @ E @ D @ C @ B @ A)) != (denota1863255036rm_sem @ E @ F @ (rr @ F @ E @ D @ C @ B @ A)))) | ((denota1778088425es_ODE @ C @ A @ B @ D) = (denota1778088425es_ODE @ E @ A @ B @ F))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_f2)).
% 61.52/20.65 thf(764,plain,((! [A:(real > (variable > real)),B:char,C:denotational_interp,D:trm,E:denotational_interp,F:trm]: (((denota1419872369iation @ (rr @ F @ E @ D @ C @ B @ A) @ (A @ (zero_zero @ real)) @ (insert @ variable @ (rVar @ B) @ (insert @ variable @ (dVar @ B) @ (bot_bot @ (set @ variable))))) & ~ ((denota1863255036rm_sem @ C @ D @ (rr @ F @ E @ D @ C @ B @ A)) = (denota1863255036rm_sem @ E @ F @ (rr @ F @ E @ D @ C @ B @ A)))) | ((denota1778088425es_ODE @ C @ (A) @ B @ D) = (denota1778088425es_ODE @ E @ (A) @ B @ F))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 61.52/20.65 thf(223,axiom,((linord219039673up_add @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Olinordered__ab__group__add)).
% 61.52/20.65 thf(979,plain,((linord219039673up_add @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 61.52/20.65 thf(100,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_186_option_Ocase__eq__if)).
% 61.52/20.65 thf(604,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)],[100])).
% 61.52/20.65 thf(197,axiom,((! [TA: $tType]: ((is_empty @ TA) = (^ [A:(set @ TA)]: (A = (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_124_Set_Ois__empty__def)).
% 61.52/20.65 thf(900,plain,((! [TA: $tType]: ((is_empty @ TA) = (^ [A:(set @ TA)]: (A = (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 61.52/20.65 thf(37,axiom,((lattice @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Lattices_Olattice_22)).
% 61.52/20.65 thf(406,plain,((lattice @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 61.52/20.65 thf(26,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_117_usubstappt__det)).
% 61.52/20.65 thf(362,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)],[26])).
% 61.52/20.65 thf(53,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_182_option_Osimps_I4_J)).
% 61.52/20.65 thf(451,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)],[53])).
% 61.52/20.65 thf(96,axiom,((! [TA: $tType]: (! [A:TA]: ((the @ TA @ (some @ TA @ A)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_149_option_Osel)).
% 61.52/20.65 thf(567,plain,((! [TA: $tType]: (! [A:TA]: ((the @ TA @ (some @ TA @ A)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 61.52/20.65 thf(69,axiom,((! [TA: $tType]: ((boolean_algebra @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (uminus_uminus @ TA @ A) @ (uminus_uminus @ TA @ B)) = (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_247_compl__le__compl__iff)).
% 61.52/20.65 thf(494,plain,((! [TA: $tType]: ((boolean_algebra @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (uminus_uminus @ TA @ A) @ (uminus_uminus @ TA @ B)) = (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 61.52/20.65 thf(102,axiom,((! [TA: $tType,TB: $tType]: ((bot @ TA) => (bot @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Obot)).
% 61.52/20.65 thf(609,plain,((! [TA: $tType,TB: $tType]: ((bot @ TA) => (bot @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 61.52/20.65 thf(179,axiom,((! [TA: $tType]: ((these @ TA @ (bot_bot @ (set @ (option @ TA)))) = (bot_bot @ (set @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_these__empty)).
% 61.52/20.65 thf(848,plain,((! [TA: $tType]: ((these @ TA @ (bot_bot @ (set @ (option @ TA)))) = (bot_bot @ (set @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 61.52/20.65 thf(241,axiom,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_empty__iff)).
% 61.52/20.65 thf(1029,plain,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 61.52/20.65 thf(218,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ B) => (member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_UnI1)).
% 61.52/20.65 thf(964,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ B) => (member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 61.52/20.65 thf(13,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_152_option_Oinducts)).
% 61.52/20.65 thf(330,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)],[13])).
% 61.52/20.65 thf(19,axiom,((! [TA: $tType]: ((boolean_algebra @ TA) => (! [A:TA]: ((uminus_uminus @ TA @ (uminus_uminus @ TA @ A)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_double__compl)).
% 61.52/20.65 thf(345,plain,((! [TA: $tType]: ((boolean_algebra @ TA) => (! [A:TA]: ((uminus_uminus @ TA @ (uminus_uminus @ TA @ A)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 61.52/20.65 thf(182,axiom,((! [TA: $tType]: ((linord219039673up_add @ TA) => (! [A:TA]: ((A = (uminus_uminus @ TA @ A)) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_201_equal__neg__zero)).
% 61.52/20.65 thf(858,plain,((! [TA: $tType]: ((linord219039673up_add @ TA) => (! [A:TA]: ((A = (uminus_uminus @ TA @ A)) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 61.52/20.65 thf(92,axiom,((! [TA: $tType]: ((boolean_algebra @ TA) => (! [A:TA,B:TA]: (((uminus_uminus @ TA @ A) = (uminus_uminus @ TA @ B)) = (A = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_compl__eq__compl__iff)).
% 61.52/20.65 thf(552,plain,((! [TA: $tType]: ((boolean_algebra @ TA) => (! [A:TA,B:TA]: (((uminus_uminus @ TA @ A) = (uminus_uminus @ TA @ B)) = (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 61.52/20.65 thf(211,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((member @ TA @ A @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) = (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_singleton__iff)).
% 61.52/20.65 thf(943,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((member @ TA @ A @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) = (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 61.52/20.65 thf(238,axiom,((! [TA: $tType]: ((group_add @ TA) => ((uminus_uminus @ TA @ (zero_zero @ TA)) = (zero_zero @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_198_add_Oinverse__neutral)).
% 61.52/20.65 thf(1022,plain,((! [TA: $tType]: ((group_add @ TA) => ((uminus_uminus @ TA @ (zero_zero @ TA)) = (zero_zero @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[238])).
% 61.52/20.65 thf(57,axiom,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA,B:TA]: (((uminus_uminus @ TA @ A) = B) = ((uminus_uminus @ TA @ B) = A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_204_minus__equation__iff)).
% 61.52/20.65 thf(462,plain,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA,B:TA]: (((uminus_uminus @ TA @ A) = B) = ((uminus_uminus @ TA @ B) = A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 61.52/20.65 thf(208,axiom,((! [A:variable,B:trm,C:denotational_interp,D:(variable > real),E:(variable > real),F:(set @ variable)]: ((~ (member @ variable @ A @ (static_FVT @ B))) => ((denota1863255036rm_sem @ C @ B @ (stateinterpol @ D @ E @ F)) = (denota1863255036rm_sem @ C @ B @ (stateinterpol @ D @ E @ (insert @ variable @ A @ F))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_stateinterpol__FVT)).
% 61.52/20.65 thf(932,plain,((! [A:variable,B:trm,C:denotational_interp,D:(variable > real),E:(variable > real),F:(set @ variable)]: ((~ (member @ variable @ A @ (static_FVT @ B))) => ((denota1863255036rm_sem @ C @ B @ (stateinterpol @ D @ E @ F)) = (denota1863255036rm_sem @ C @ B @ (stateinterpol @ D @ E @ (insert @ variable @ A @ F))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 61.52/20.65 thf(225,axiom,((! [A:char,B:char]: (((rVar @ A) = (rVar @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_variable_Oinject_I1_J)).
% 61.52/20.65 thf(983,plain,((! [A:char,B:char]: (((rVar @ A) = (rVar @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[225])).
% 61.52/20.65 thf(247,axiom,((! [A:(variable > real),B:(variable > real),C:(set @ variable),D:(variable > real),E:(set @ variable)]: ((denota1419872369iation @ A @ B @ C) => ((denota1419872369iation @ B @ D @ E) => (denota1419872369iation @ A @ D @ (sup_sup @ (set @ variable) @ C @ E)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_Uvariation__trans)).
% 61.52/20.65 thf(1044,plain,((! [A:(variable > real),B:(variable > real),C:(set @ variable),D:(variable > real),E:(set @ variable)]: ((denota1419872369iation @ (A) @ (B) @ C) => ((denota1419872369iation @ (B) @ (D) @ E) => (denota1419872369iation @ (A) @ (D) @ (sup_sup @ (set @ variable) @ C @ E)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[247])).
% 61.52/20.65 thf(254,axiom,((! [A:char]: ((size_variable @ (rVar @ A)) = (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_115_variable_Osize__gen_I1_J)).
% 61.52/20.65 thf(1066,plain,((! [A:char]: ((size_variable @ (rVar @ A)) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[254])).
% 61.52/20.65 thf(157,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((A != (bot_bot @ (set @ TA))) => ((! [B:TA,C:TA]: ((member @ TA @ B @ A) => ((member @ TA @ C @ A) => (B = C)))) => (is_singleton @ TA @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_108_is__singletonI_H)).
% 61.52/20.65 thf(780,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((~ (A = (bot_bot @ (set @ TA)))) => ((! [B:TA,C:TA]: ((member @ TA @ B @ A) => ((member @ TA @ C @ A) => (B = C)))) => (is_singleton @ TA @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 61.52/20.65 thf(236,axiom,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:char,C:trm,D:denotational_interp,E:(real > (variable > real))]: (((uSubst95898992stappt @ A @ (insert @ variable @ (rVar @ B) @ (insert @ variable @ (dVar @ B) @ (bot_bot @ (set @ variable)))) @ C) != (none @ trm)) => ((denota1778088425es_ODE @ D @ E @ B @ (the @ trm @ (uSubst95898992stappt @ A @ (insert @ variable @ (rVar @ B) @ (insert @ variable @ (dVar @ B) @ (bot_bot @ (set @ variable)))) @ C))) = (denota1778088425es_ODE @ (uSubst2091380086djoint @ A @ D @ (E @ (zero_zero @ real))) @ E @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_usubst__ode)).
% 61.52/20.65 thf(1015,plain,((! [A:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),B:char,C:trm,D:denotational_interp,E:(real > (variable > real))]: ((~ ((uSubst95898992stappt @ A @ (insert @ variable @ (rVar @ B) @ (insert @ variable @ (dVar @ B) @ (bot_bot @ (set @ variable)))) @ C) = (none @ trm))) => ((denota1778088425es_ODE @ D @ (E) @ B @ (the @ trm @ (uSubst95898992stappt @ A @ (insert @ variable @ (rVar @ B) @ (insert @ variable @ (dVar @ B) @ (bot_bot @ (set @ variable)))) @ C))) = (denota1778088425es_ODE @ (uSubst2091380086djoint @ A @ D @ (E @ (zero_zero @ real))) @ (E) @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[236])).
% 61.52/20.65 thf(293,axiom,((! [A:(variable > real),B:(variable > real),C:(set @ variable),D:(set @ variable)]: ((denotational_Vagree @ A @ B @ C) => ((denotational_Vagree @ A @ B @ D) => (denotational_Vagree @ A @ B @ (sup_sup @ (set @ variable) @ C @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_176_Vagree__union)).
% 61.52/20.65 thf(1176,plain,((! [A:(variable > real),B:(variable > real),C:(set @ variable),D:(set @ variable)]: ((denotational_Vagree @ (A) @ (B) @ C) => ((denotational_Vagree @ (A) @ (B) @ D) => (denotational_Vagree @ (A) @ (B) @ (sup_sup @ (set @ variable) @ C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[293])).
% 61.52/20.65 thf(180,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((A = (sup_sup @ TA @ B @ C)) => ((sup_sup @ TA @ A @ D) = (sup_sup @ TA @ B @ (sup_sup @ TA @ C @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_boolean__algebra__cancel_Osup1)).
% 61.52/20.65 thf(851,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((A = (sup_sup @ TA @ B @ C)) => ((sup_sup @ TA @ A @ D) = (sup_sup @ TA @ B @ (sup_sup @ TA @ C @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 61.52/20.65 thf(73,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_164_option_Osplit__sel__asm)).
% 61.52/20.65 thf(505,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)],[73])).
% 61.52/20.65 thf(115,axiom,((! [A:(set @ (variable > real)),B:(variable > real)]: ((static_selectlike @ A @ B @ (bot_bot @ (set @ variable))) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_143_selectlike__empty)).
% 61.52/20.65 thf(653,plain,((! [A:(set @ (variable > real)),B:(variable > real)]: ((static_selectlike @ A @ (B) @ (bot_bot @ (set @ variable))) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 61.52/20.65 thf(204,axiom,((! [TA: $tType]: ((is_singleton @ TA) = (^ [A:(set @ TA)]: ? [B:TA]: (A = (insert @ TA @ B @ (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_109_is__singleton__def)).
% 61.52/20.65 thf(922,plain,((! [TA: $tType]: ((is_singleton @ TA) = (^ [A:(set @ TA)]: ? [B:TA]: (A = (insert @ TA @ B @ (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 61.52/20.65 thf(125,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C)) = (sup_sup @ TA @ B @ (sup_sup @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_42_sup__left__commute)).
% 61.52/20.65 thf(685,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C)) = (sup_sup @ TA @ B @ (sup_sup @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 61.52/20.65 thf(79,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_210_Timeso__undef)).
% 61.52/20.65 thf(521,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)],[79])).
% 61.52/20.65 thf(32,axiom,((! [A:trm]: ((uSubst277968634Timeso @ (some @ trm @ A) @ (none @ trm)) = (none @ trm)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_189_Timeso_Osimps_I3_J)).
% 61.52/20.65 thf(394,plain,((! [A:trm]: ((uSubst277968634Timeso @ (some @ trm @ A) @ (none @ trm)) = (none @ trm)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 61.52/20.65 thf(226,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (inf_inf @ (set @ TA) @ B @ C)) = ((member @ TA @ A @ B) & (member @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_244_Int__iff)).
% 61.52/20.65 thf(986,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (inf_inf @ (set @ TA) @ B @ C)) = ((member @ TA @ A @ B) & (member @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 61.52/20.65 thf(138,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((sup_sup @ TA @ A @ B) = (bot_bot @ TA)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_sup__eq__bot__iff)).
% 61.52/20.65 thf(722,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((sup_sup @ TA @ A @ B) = (bot_bot @ TA)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 61.52/20.65 thf(243,axiom,((! [TA: $tType]: (! [A:TA]: (is_singleton @ TA @ (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_106_is__singletonI)).
% 61.52/20.65 thf(1034,plain,((! [TA: $tType]: (! [A:TA]: (is_singleton @ TA @ (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[243])).
% 61.52/20.65 thf(83,axiom,((uminus @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Groups_Ouminus_24)).
% 61.52/20.65 thf(531,plain,((uminus @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 61.52/20.65 thf(30,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_155_combine__options__cases)).
% 61.52/20.65 thf(374,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)],[30])).
% 61.52/20.65 thf(279,axiom,((! [TA: $tType]: (! [A:(set @ (option @ TA))]: (((these @ TA @ A) = (bot_bot @ (set @ TA))) = ((A = (bot_bot @ (set @ (option @ TA)))) | (A = (insert @ (option @ TA) @ (none @ TA) @ (bot_bot @ (set @ (option @ TA)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_126_these__empty__eq)).
% 61.52/20.65 thf(1134,plain,((! [TA: $tType]: (! [A:(set @ (option @ TA))]: (((these @ TA @ A) = (bot_bot @ (set @ TA))) = ((A = (bot_bot @ (set @ (option @ TA)))) | (A = (insert @ (option @ TA) @ (none @ TA) @ (bot_bot @ (set @ (option @ TA)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[279])).
% 61.52/20.65 thf(165,axiom,((! [A:(variable > real),B:(variable > real)]: ((stateinterpol @ A @ B @ (bot_bot @ (set @ variable))) = B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_221_stateinterpol__empty)).
% 61.52/20.65 thf(812,plain,((! [A:(variable > real),B:(variable > real)]: ((stateinterpol @ A @ B @ (bot_bot @ (set @ variable))) = (B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 61.52/20.65 thf(259,axiom,((denota1778088425es_ODE @ (uSubst2091380086djoint @ sigma @ i @ omega) @ f @ x @ theta)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_a1)).
% 61.52/20.65 thf(1081,plain,((denota1778088425es_ODE @ (uSubst2091380086djoint @ sigma @ i @ (omega)) @ (f) @ x @ theta)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[259])).
% 61.52/20.65 thf(77,axiom,((! [TA: $tType,TB: $tType]: ((boolean_algebra @ TA) => (boolean_algebra @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Lattices_Oboolean__algebra)).
% 61.52/20.65 thf(516,plain,((! [TA: $tType,TB: $tType]: ((boolean_algebra @ TA) => (boolean_algebra @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 61.52/20.65 thf(210,axiom,((! [A:char,B:char]: ((rVar @ A) != (dVar @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_variable_Odistinct_I1_J)).
% 61.52/20.65 thf(939,plain,((! [A:char,B:char]: ~ ((rVar @ A) = (dVar @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 61.52/20.65 thf(283,axiom,((! [TA: $tType]: ((is_singleton @ TA) = (^ [A:(set @ TA)]: (A = (insert @ TA @ (the_elem @ TA @ A) @ (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_is__singleton__the__elem)).
% 61.52/20.65 thf(1145,plain,((! [TA: $tType]: ((is_singleton @ TA) = (^ [A:(set @ TA)]: (A = (insert @ TA @ (the_elem @ TA @ A) @ (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[283])).
% 61.52/20.65 thf(176,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ (bot_bot @ TA)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_sup__bot_Oright__neutral)).
% 61.52/20.65 thf(836,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ (bot_bot @ TA)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 61.52/20.65 thf(160,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((bot_bot @ TA) = (sup_sup @ TA @ A @ B)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_bot__eq__sup__iff)).
% 61.52/20.65 thf(795,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((bot_bot @ TA) = (sup_sup @ TA @ A @ B)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 61.52/20.65 thf(123,axiom,(((denota1778088425es_ODE @ i @ f @ x @ (the @ trm @ (uSubst95898992stappt @ sigma @ (sup_sup @ (set @ variable) @ u @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable))))) @ theta))) => (denota1778088425es_ODE @ (uSubst2091380086djoint @ sigma @ i @ omega) @ f @ x @ theta))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_112_l2r)).
% 61.52/20.65 thf(680,plain,(((denota1778088425es_ODE @ i @ (f) @ x @ (the @ trm @ (uSubst95898992stappt @ sigma @ (sup_sup @ (set @ variable) @ u @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable))))) @ theta))) => (denota1778088425es_ODE @ (uSubst2091380086djoint @ sigma @ i @ (omega)) @ (f) @ x @ theta))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 61.52/20.65 thf(55,axiom,((! [TA: $tType]: ((semilattice_inf @ TA) => (! [A:TA,B:TA]: ((inf_inf @ TA @ (inf_inf @ TA @ A @ B) @ B) = (inf_inf @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_242_inf__right__idem)).
% 61.52/20.65 thf(458,plain,((! [TA: $tType]: ((semilattice_inf @ TA) => (! [A:TA,B:TA]: ((inf_inf @ TA @ (inf_inf @ TA @ A @ B) @ B) = (inf_inf @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 61.52/20.65 thf(170,axiom,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_bot__apply)).
% 61.52/20.65 thf(823,plain,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 61.52/20.65 thf(155,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ (uminus_uminus @ (set @ TA) @ B)) => (~ (member @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_208_ComplD)).
% 61.52/20.65 thf(776,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ (uminus_uminus @ (set @ TA) @ B)) => (~ (member @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 61.52/20.65 thf(181,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ A @ B)) = (sup_sup @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_sup_Oleft__idem)).
% 61.52/20.65 thf(855,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ A @ B)) = (sup_sup @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 61.52/20.65 thf(239,axiom,((! [A:(variable > real),B:(variable > real),C:(set @ variable),D:variable]: (denotational_Vagree @ (stateinterpol @ A @ B @ C) @ (stateinterpol @ A @ B @ (insert @ variable @ D @ C)) @ (uminus_uminus @ (set @ variable) @ (insert @ variable @ D @ (bot_bot @ (set @ variable))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_stateinterpol__insert)).
% 61.52/20.65 thf(1025,plain,((! [A:(variable > real),B:(variable > real),C:(set @ variable),D:variable]: (denotational_Vagree @ (stateinterpol @ A @ B @ C) @ (stateinterpol @ A @ B @ (insert @ variable @ D @ C)) @ (uminus_uminus @ (set @ variable) @ (insert @ variable @ D @ (bot_bot @ (set @ variable))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 61.52/20.65 thf(132,axiom,((! [TA: $tType]: ((bot_bot @ (TA > $o)) = (^ [A:TA]: (member @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_bot__empty__eq)).
% 61.52/20.65 thf(705,plain,((! [TA: $tType]: ((bot_bot @ (TA > $o)) = (^ [A:TA]: (member @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 61.52/20.65 thf(192,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ B) => ((member @ TA @ A @ C) => (member @ TA @ A @ (inf_inf @ (set @ TA) @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_243_IntI)).
% 61.52/20.65 thf(887,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ B) => ((member @ TA @ A @ C) => (member @ TA @ A @ (inf_inf @ (set @ TA) @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 61.52/20.65 thf(215,axiom,((! [A:(variable > real),B:(variable > real),C:(set @ variable),D:(set @ (variable > real))]: ((denotational_Vagree @ A @ B @ C) => ((member @ (variable > real) @ A @ (static_selectlike @ D @ B @ C)) = (member @ (variable > real) @ A @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_170_similar__selectlike__mem)).
% 61.52/20.65 thf(954,plain,((! [A:(variable > real),B:(variable > real),C:(set @ variable),D:(set @ (variable > real))]: ((denotational_Vagree @ (A) @ (B) @ C) => ((member @ (variable > real) @ (A) @ (static_selectlike @ D @ (B) @ C)) = (member @ (variable > real) @ (A) @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 61.52/20.65 thf(228,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((~ (member @ TA @ A @ B)) => (member @ TA @ A @ (uminus_uminus @ (set @ TA) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_197_ComplI)).
% 61.52/20.65 thf(993,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((~ (member @ TA @ A @ B)) => (member @ TA @ A @ (uminus_uminus @ (set @ TA) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 61.52/20.65 thf(250,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => ((insert @ TA @ A @ B) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_insert__absorb)).
% 61.52/20.65 thf(1053,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => ((insert @ TA @ A @ B) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 61.52/20.65 thf(214,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: (((insert @ TA @ A @ (bot_bot @ (set @ TA))) = (sup_sup @ (set @ TA) @ B @ C)) = (((B = (bot_bot @ (set @ TA))) & (C = (insert @ TA @ A @ (bot_bot @ (set @ TA))))) | ((B = (insert @ TA @ A @ (bot_bot @ (set @ TA)))) & (C = (bot_bot @ (set @ TA)))) | ((B = (insert @ TA @ A @ (bot_bot @ (set @ TA)))) & (C = (insert @ TA @ A @ (bot_bot @ (set @ TA)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_singleton__Un__iff)).
% 61.52/20.65 thf(951,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: (((insert @ TA @ A @ (bot_bot @ (set @ TA))) = (sup_sup @ (set @ TA) @ B @ C)) = (((B = (bot_bot @ (set @ TA))) & (C = (insert @ TA @ A @ (bot_bot @ (set @ TA))))) | ((B = (insert @ TA @ A @ (bot_bot @ (set @ TA)))) & (C = (bot_bot @ (set @ TA)))) | ((B = (insert @ TA @ A @ (bot_bot @ (set @ TA)))) & (C = (insert @ TA @ A @ (bot_bot @ (set @ TA)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 61.52/20.65 thf(25,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)).
% 61.52/20.65 thf(359,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($false) @ A @ B) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 61.52/20.65 thf(261,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ A @ B)) = (sup_sup @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_sup__left__idem)).
% 61.52/20.65 thf(1085,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ A @ B)) = (sup_sup @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[261])).
% 61.52/20.65 thf(60,axiom,((semilattice_inf @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Lattices_Osemilattice__inf_19)).
% 61.52/20.65 thf(470,plain,((semilattice_inf @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 61.52/20.65 thf(15,axiom,((! [A:(option @ trm)]: ((A != (none @ trm)) = (? [B:trm]: (A = (some @ trm @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_157_undeft__equiv)).
% 61.52/20.65 thf(336,plain,((! [A:(option @ trm)]: ((~ (A = (none @ trm))) = (? [B:trm]: (A = (some @ trm @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 61.52/20.65 thf(116,axiom,((! [TA: $tType,TB: $tType]: ((semilattice_sup @ TB) => ((sup_sup @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (sup_sup @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_sup__fun__def)).
% 61.52/20.65 thf(656,plain,((! [TA: $tType,TB: $tType]: ((semilattice_sup @ TB) => ((sup_sup @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (sup_sup @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 61.52/20.65 thf(140,axiom,((! [A:(variable > real),B:(variable > real),C:(set @ variable),D:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),E:trm,F:denotational_interp]: ((denota1419872369iation @ A @ B @ C) => (((uSubst95898992stappt @ D @ C @ E) != (none @ trm)) => ((denota1863255036rm_sem @ F @ (the @ trm @ (uSubst95898992stappt @ D @ C @ E)) @ A) = (denota1863255036rm_sem @ (uSubst2091380086djoint @ D @ F @ B) @ E @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_116_usubst__term)).
% 61.52/20.65 thf(727,plain,((! [A:(variable > real),B:(variable > real),C:(set @ variable),D:(product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ trm)) @ (product_prod @ (char > (option @ fml)) @ (char > (option @ game))))),E:trm,F:denotational_interp]: ((denota1419872369iation @ (A) @ (B) @ C) => ((~ ((uSubst95898992stappt @ D @ C @ E) = (none @ trm))) => ((denota1863255036rm_sem @ F @ (the @ trm @ (uSubst95898992stappt @ D @ C @ E)) @ (A)) = (denota1863255036rm_sem @ (uSubst2091380086djoint @ D @ F @ (B)) @ E @ (A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 61.52/20.65 thf(281,axiom,((! [TA: $tType]: (preorder @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Opreorder_12)).
% 61.52/20.65 thf(1140,plain,((! [TA: $tType]: (preorder @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[281])).
% 61.52/20.65 thf(7,axiom,((! [TA: $tType]: (! [A:TA]: ((none @ TA) != (some @ TA @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_148_option_Odistinct_I1_J)).
% 61.52/20.65 thf(314,plain,((! [TA: $tType]: (! [A:TA]: ~ ((none @ TA) = (some @ TA @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 61.52/20.65 thf(51,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_Collect__mem__eq)).
% 61.52/20.65 thf(446,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 61.52/20.65 thf(70,axiom,((! [TA: $tType]: (! [A:(option @ TA),B:TA]: ((A = (some @ TA @ B)) => (A != (none @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_150_option_OdiscI)).
% 61.52/20.65 thf(497,plain,((! [TA: $tType]: (! [A:(option @ TA),B:TA]: ((A = (some @ TA @ B)) => (~ (A = (none @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 61.52/20.65 thf(178,axiom,((! [A:(variable > real)]: ((denota1419872369iation @ A @ (f @ (zero_zero @ real)) @ (sup_sup @ (set @ variable) @ u @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable)))))) => ((denota1863255036rm_sem @ i @ (the @ trm @ (uSubst95898992stappt @ sigma @ (sup_sup @ (set @ variable) @ u @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable))))) @ theta)) @ A) = (denota1863255036rm_sem @ (uSubst2091380086djoint @ sigma @ i @ (f @ (zero_zero @ real))) @ theta @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_113_IH)).
% 61.52/20.65 thf(845,plain,((! [A:(variable > real)]: ((denota1419872369iation @ (A) @ (f @ (zero_zero @ real)) @ (sup_sup @ (set @ variable) @ u @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable)))))) => ((denota1863255036rm_sem @ i @ (the @ trm @ (uSubst95898992stappt @ sigma @ (sup_sup @ (set @ variable) @ u @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable))))) @ theta)) @ (A)) = (denota1863255036rm_sem @ (uSubst2091380086djoint @ sigma @ i @ (f @ (zero_zero @ real))) @ theta @ (A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 61.52/20.65 thf(58,axiom,((! [A:(variable > real),B:variable]: ((denotational_repv @ A @ B @ (A @ B)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_129_repv__self)).
% 61.52/20.65 thf(465,plain,((! [A:(variable > real),B:variable]: ((denotational_repv @ A @ B @ (A @ B)) = (A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 61.52/20.65 thf(106,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ A) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_sup_Oidem)).
% 61.52/20.65 thf(627,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 61.52/20.65 thf(287,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((insert @ TA @ A @ (insert @ TA @ A @ B)) = (insert @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_insert__absorb2)).
% 61.52/20.65 thf(1157,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((insert @ TA @ A @ (insert @ TA @ A @ B)) = (insert @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[287])).
% 61.52/20.65 thf(80,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: (((some @ TA @ A) = (some @ TA @ B)) = (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_option_Oinject)).
% 61.52/20.65 thf(524,plain,((! [TA: $tType]: (! [A:TA,B:TA]: (((some @ TA @ A) = (some @ TA @ B)) = (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 61.52/20.65 thf(151,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => (? [C:(set @ TA)]: ((B = (insert @ TA @ A @ C)) & ~ (member @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_mk__disjoint__insert)).
% 61.52/20.65 thf(759,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => (? [C:(set @ TA)]: ((B = (insert @ TA @ A @ C)) & ~ (member @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 61.52/20.65 thf(297,axiom,((! [A:(set @ (variable > real)),B:(variable > real),C:(set @ variable),D:(set @ (variable > real))]: (((static_selectlike @ A @ B @ C) = (static_selectlike @ D @ B @ C)) = (! [E:(variable > real)]: ((denota1419872369iation @ E @ B @ (uminus_uminus @ (set @ variable) @ C)) => ((member @ (variable > real) @ E @ A) = (member @ (variable > real) @ E @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_214_selectlike__equal__cond)).
% 61.52/20.65 thf(1189,plain,((! [A:(set @ (variable > real)),B:(variable > real),C:(set @ variable),D:(set @ (variable > real))]: (((static_selectlike @ A @ (B) @ C) = (static_selectlike @ D @ (B) @ C)) = (! [E:(variable > real)]: ((denota1419872369iation @ (E) @ (B) @ (uminus_uminus @ (set @ variable) @ C)) => ((member @ (variable > real) @ (E) @ A) = (member @ (variable > real) @ (E) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[297])).
% 61.52/20.65 thf(234,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((is_singleton @ TA @ A) => (~ (! [B:TA]: (A != (insert @ TA @ B @ (bot_bot @ (set @ TA)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_is__singletonE)).
% 61.52/20.65 thf(1010,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((is_singleton @ TA @ A) => (~ (! [B:TA]: ~ (A = (insert @ TA @ B @ (bot_bot @ (set @ TA)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[234])).
% 61.52/20.65 thf(207,axiom,((lattice @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Lattices_Olattice_28)).
% 61.52/20.65 thf(931,plain,((lattice @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 61.52/20.65 thf(87,axiom,((! [TA: $tType]: ((semilattice_inf @ TA) => (! [A:TA,B:TA]: ((inf_inf @ TA @ A @ (inf_inf @ TA @ A @ B)) = (inf_inf @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_240_inf__left__idem)).
% 61.52/20.65 thf(539,plain,((! [TA: $tType]: ((semilattice_inf @ TA) => (! [A:TA,B:TA]: ((inf_inf @ TA @ A @ (inf_inf @ TA @ A @ B)) = (inf_inf @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 61.52/20.65 thf(222,axiom,((! [TA: $tType]: ((zero @ TA) => ((zero_zero @ (set @ TA)) = (insert @ TA @ (zero_zero @ TA) @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_set__zero)).
% 61.52/20.65 thf(976,plain,((! [TA: $tType]: ((zero @ TA) => ((zero_zero @ (set @ TA)) = (insert @ TA @ (zero_zero @ TA) @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 61.52/20.65 thf(126,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o)]: ((? [D:TA]: ((member @ TA @ D @ (sup_sup @ (set @ TA) @ A @ B)) & (C @ D))) = (? [D:TA]: ((member @ TA @ D @ A) & (C @ D)) | ? [D:TA]: ((member @ TA @ D @ B) & (C @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_bex__Un)).
% 61.52/20.65 thf(688,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o)]: ((? [D:TA]: ((member @ TA @ D @ (sup_sup @ (set @ TA) @ A @ B)) & (C @ D))) = (? [D:TA]: ((member @ TA @ D @ A) & (C @ D)) | ? [D:TA]: ((member @ TA @ D @ B) & (C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 61.52/20.65 thf(198,axiom,((! [A:char]: ((size_variable @ (dVar @ A)) = (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_120_variable_Osize__gen_I2_J)).
% 61.52/20.65 thf(903,plain,((! [A:char]: ((size_variable @ (dVar @ A)) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 61.52/20.65 thf(130,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((insert @ TA @ A @ (insert @ TA @ B @ C)) = (insert @ TA @ B @ (insert @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_insert__commute)).
% 61.52/20.65 thf(699,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((insert @ TA @ A @ (insert @ TA @ B @ C)) = (insert @ TA @ B @ (insert @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 61.52/20.65 thf(217,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: ((ord_less_eq @ TA @ A @ (zero_zero @ TA)) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_245_le__zero__eq)).
% 61.52/20.65 thf(961,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: ((ord_less_eq @ TA @ A @ (zero_zero @ TA)) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[217])).
% 61.52/20.65 thf(147,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((~ (member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C))) = (~ (member @ TA @ A @ B) & ~ (member @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_not__union__or)).
% 61.52/20.65 thf(748,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((~ (member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C))) = (~ (member @ TA @ A @ B) & ~ (member @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 61.52/20.65 thf(3,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_217_trm_Oinject_I6_J)).
% 61.52/20.65 thf(304,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)],[3])).
% 61.52/20.65 thf(212,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: (((insert @ TA @ A @ (bot_bot @ (set @ TA))) = (insert @ TA @ B @ (bot_bot @ (set @ TA)))) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_singleton__inject)).
% 61.52/20.65 thf(946,plain,((! [TA: $tType]: (! [A:TA,B:TA]: (((insert @ TA @ A @ (bot_bot @ (set @ TA))) = (insert @ TA @ B @ (bot_bot @ (set @ TA)))) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 61.52/20.65 thf(21,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_163_option_Osplit__sel)).
% 61.52/20.65 thf(351,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)],[21])).
% 61.52/20.65 thf(141,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:TA,C:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (insert @ TA @ B @ C)) = (insert @ TA @ B @ (sup_sup @ (set @ TA) @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_Un__insert__right)).
% 61.52/20.65 thf(731,plain,((! [TA: $tType]: (! [A:(set @ TA),B:TA,C:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (insert @ TA @ B @ C)) = (insert @ TA @ B @ (sup_sup @ (set @ TA) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 61.52/20.65 thf(229,axiom,((! [A:(variable > real),B:(set @ (variable > real)),C:(set @ variable)]: ((member @ (variable > real) @ A @ (static_selectlike @ B @ A @ C)) = (member @ (variable > real) @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_selectlike__self)).
% 61.52/20.65 thf(995,plain,((! [A:(variable > real),B:(set @ (variable > real)),C:(set @ variable)]: ((member @ (variable > real) @ (A) @ (static_selectlike @ B @ (A) @ C)) = (member @ (variable > real) @ (A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 61.52/20.65 thf(201,axiom,((! [A:variable,B:variable,C:(variable > real),D:real,E:(set @ (variable > real))]: ((A != B) => ((member @ (variable > real) @ (denotational_repv @ C @ A @ D) @ (static_selectlike @ E @ C @ (insert @ variable @ B @ (bot_bot @ (set @ variable))))) = (member @ (variable > real) @ (denotational_repv @ C @ A @ D) @ E))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_137_repv__selectlike__other)).
% 61.52/20.65 thf(914,plain,((! [A:variable,B:variable,C:(variable > real),D:real,E:(set @ (variable > real))]: ((~ (A = B)) => ((member @ (variable > real) @ (denotational_repv @ C @ A @ D) @ (static_selectlike @ E @ (C) @ (insert @ variable @ B @ (bot_bot @ (set @ variable))))) = (member @ (variable > real) @ (denotational_repv @ C @ A @ D) @ E))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 61.52/20.65 thf(63,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)).
% 61.52/20.65 thf(478,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($true) @ A @ B) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 61.52/20.65 thf(91,axiom,((! [TA: $tType,TB: $tType]: ((uminus @ TB) => ((uminus_uminus @ (TA > TB)) = (^ [A:(TA > TB),B:TA]: (uminus_uminus @ TB @ (A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_fun__Compl__def)).
% 61.52/20.65 thf(549,plain,((! [TA: $tType,TB: $tType]: ((uminus @ TB) => ((uminus_uminus @ (TA > TB)) = (^ [A:(TA > TB),B:TA]: (uminus_uminus @ TB @ (A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 61.52/20.65 thf(45,axiom,((! [TA: $tType,TB: $tType]: ((uminus @ TB) => ((uminus_uminus @ (TA > TB)) = (^ [A:(TA > TB),B:TA]: (uminus_uminus @ TB @ (A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_194_uminus__apply)).
% 61.52/20.65 thf(432,plain,((! [TA: $tType,TB: $tType]: ((uminus @ TB) => ((uminus_uminus @ (TA > TB)) = (^ [A:(TA > TB),B:TA]: (uminus_uminus @ TB @ (A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 61.52/20.65 thf(175,axiom,((! [A:(set @ (variable > real)),B:(set @ (variable > real)),C:(variable > real),D:(set @ variable)]: ((static_selectlike @ (sup_sup @ (set @ (variable > real)) @ A @ B) @ C @ D) = (sup_sup @ (set @ (variable > real)) @ (static_selectlike @ A @ C @ D) @ (static_selectlike @ B @ C @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_147_selectlike__union)).
% 61.52/20.65 thf(833,plain,((! [A:(set @ (variable > real)),B:(set @ (variable > real)),C:(variable > real),D:(set @ variable)]: ((static_selectlike @ (sup_sup @ (set @ (variable > real)) @ A @ B) @ (C) @ D) = (sup_sup @ (set @ (variable > real)) @ (static_selectlike @ A @ (C) @ D) @ (static_selectlike @ B @ (C) @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 61.52/20.65 thf(266,axiom,(((uSubst95898992stappt @ sigma @ (sup_sup @ (set @ variable) @ u @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable))))) @ theta) != (none @ trm))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_subdef)).
% 61.52/20.65 thf(1097,plain,((~ ((uSubst95898992stappt @ sigma @ (sup_sup @ (set @ variable) @ u @ (insert @ variable @ (rVar @ x) @ (insert @ variable @ (dVar @ x) @ (bot_bot @ (set @ variable))))) @ theta) = (none @ trm)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[266])).
% 61.52/20.65 thf(167,axiom,((! [TA: $tType]: (! [A:TA]: ((the_elem @ TA @ (insert @ TA @ A @ (bot_bot @ (set @ TA)))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_the__elem__eq)).
% 61.52/20.65 thf(818,plain,((! [TA: $tType]: (! [A:TA]: ((the_elem @ TA @ (insert @ TA @ A @ (bot_bot @ (set @ TA)))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 61.52/20.65 thf(36,axiom,(((some @ trm) = (some @ trm))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_172_Aterm__Some)).
% 61.52/20.65 thf(405,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 61.52/20.65 thf(284,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ (bot_bot @ TA) @ A) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_sup__bot__left)).
% 61.52/20.65 thf(1148,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ (bot_bot @ TA) @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[284])).
% 61.52/20.65 thf(95,axiom,((! [TA: $tType]: ((semilattice_inf @ TA) => (! [A:TA]: ((inf_inf @ TA @ A @ A) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_inf__idem)).
% 61.52/20.65 thf(564,plain,((! [TA: $tType]: ((semilattice_inf @ TA) => (! [A:TA]: ((inf_inf @ TA @ A @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 61.52/20.65 thf(202,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C)) = (sup_sup @ TA @ B @ (sup_sup @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_43_sup_Oleft__commute)).
% 61.52/20.65 thf(918,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C)) = (sup_sup @ TA @ B @ (sup_sup @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 61.52/20.65 thf(196,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((member @ TA @ A @ (insert @ TA @ B @ C)) = ((A = B) | (member @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_insert__iff)).
% 61.52/20.65 thf(897,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((member @ TA @ A @ (insert @ TA @ B @ C)) = ((A = B) | (member @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 61.52/20.65 thf(251,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: (((set_option @ TA @ A) = (bot_bot @ (set @ TA))) = (A = (none @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_169_set__empty__eq)).
% 61.52/20.65 thf(1056,plain,((! [TA: $tType]: (! [A:(option @ TA)]: (((set_option @ TA @ A) = (bot_bot @ (set @ TA))) = (A = (none @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[251])).
% 61.52/20.65 thf(34,axiom,((! [TA: $tType,TB: $tType]: ((bounded_lattice @ TA) => (bounded_lattice @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Lattices_Obounded__lattice_2)).
% 61.52/20.65 thf(400,plain,((! [TA: $tType,TB: $tType]: ((bounded_lattice @ TA) => (bounded_lattice @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 61.52/20.65 thf(172,axiom,((! [TA: $tType]: (bounded_lattice @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Lattices_Obounded__lattice_1)).
% 61.52/20.65 thf(828,plain,((! [TA: $tType]: (bounded_lattice @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 61.52/20.65 thf(109,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_235_subset__antisym)).
% 61.52/20.65 thf(635,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)],[109])).
% 61.52/20.65 thf(84,axiom,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Opreorder)).
% 61.52/20.65 thf(532,plain,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 61.52/20.65 thf(129,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((bot_bot @ TA) = (sup_sup @ TA @ A @ B)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_sup__bot_Oneutr__eq__iff)).
% 61.52/20.65 thf(696,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((bot_bot @ TA) = (sup_sup @ TA @ A @ B)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 61.52/20.65 thf(137,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_72_Uvariation__def)).
% 61.52/20.65 thf(720,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)],[137])).
% 61.52/20.65 thf(206,axiom,((! [TA: $tType]: ((set_option @ TA @ (none @ TA)) = (bot_bot @ (set @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_184_option_Osimps_I14_J)).
% 61.52/20.65 thf(928,plain,((! [TA: $tType]: ((set_option @ TA @ (none @ TA)) = (bot_bot @ (set @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 61.52/20.65 thf(24,axiom,((zero @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ozero)).
% 61.52/20.65 thf(358,plain,((zero @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 61.52/20.65 thf(163,axiom,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA]: (((zero_zero @ TA) = (uminus_uminus @ TA @ A)) = ((zero_zero @ TA) = A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_199_neg__0__equal__iff__equal)).
% 61.52/20.65 thf(807,plain,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA]: (((zero_zero @ TA) = (uminus_uminus @ TA @ A)) = ((zero_zero @ TA) = A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 61.52/20.65 thf(177,axiom,((! [A:(variable > real),B:(set @ variable),C:(set @ (variable > real)),D:(set @ (variable > real))]: ((! [E:(variable > real)]: ((denota1419872369iation @ E @ A @ B) => ((member @ (variable > real) @ E @ C) = (member @ (variable > real) @ E @ D)))) => ((static_selectlike @ C @ A @ (uminus_uminus @ (set @ variable) @ B)) = (static_selectlike @ D @ A @ (uminus_uminus @ (set @ variable) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_211_selectlike__equal__cocond__corule)).
% 61.52/20.65 thf(839,plain,((! [A:(variable > real),B:(set @ variable),C:(set @ (variable > real)),D:(set @ (variable > real))]: ((! [E:(variable > real)]: ((denota1419872369iation @ (E) @ (A) @ B) => ((member @ (variable > real) @ (E) @ C) = (member @ (variable > real) @ (E) @ D)))) => ((static_selectlike @ C @ (A) @ (uminus_uminus @ (set @ variable) @ B)) = (static_selectlike @ D @ (A) @ (uminus_uminus @ (set @ variable) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 61.52/20.65 thf(144,axiom,((! [TA: $tType]: (! [A:(TA > $o)]: (((bot_bot @ (set @ TA)) = (collect @ TA @ A)) = (! [B:TA]: ~ (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_empty__Collect__eq)).
% 61.52/20.65 thf(740,plain,((! [TA: $tType]: (! [A:(TA > $o)]: (((bot_bot @ (set @ TA)) = (collect @ TA @ (A))) = (! [B:TA]: ~ (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 61.52/20.65 thf(237,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA,D:(set @ TA)]: ((~ (member @ TA @ A @ B)) => ((~ (member @ TA @ C @ D)) => (((insert @ TA @ A @ B) = (insert @ TA @ C @ D)) = (((A = C) => (B = D)) & ((A != C) => (? [E:(set @ TA)]: ((B = (insert @ TA @ C @ E)) & ~ (member @ TA @ C @ E) & (D = (insert @ TA @ A @ E)) & ~ (member @ TA @ A @ E))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_insert__eq__iff)).
% 61.52/20.65 thf(1019,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA,D:(set @ TA)]: ((~ (member @ TA @ A @ B)) => ((~ (member @ TA @ C @ D)) => (((insert @ TA @ A @ B) = (insert @ TA @ C @ D)) = (((A = C) => (B = D)) & ((~ (A = C)) => (? [E:(set @ TA)]: ((B = (insert @ TA @ C @ E)) & ~ (member @ TA @ C @ E) & (D = (insert @ TA @ A @ E)) & ~ (member @ TA @ A @ E))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 61.52/20.65 thf(82,axiom,((! [A:(option @ trm)]: ((uSubst277968634Timeso @ (none @ trm) @ A) = (none @ trm)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_209_Timeso_Osimps_I2_J)).
% 61.52/20.65 thf(528,plain,((! [A:(option @ trm)]: ((uSubst277968634Timeso @ (none @ trm) @ A) = (none @ trm)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 61.52/20.65 thf(112,axiom,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_bot__fun__def)).
% 61.52/20.65 thf(644,plain,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 61.52/20.65 thf(169,axiom,((semilattice_sup @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Lattices_Osemilattice__sup_25)).
% 61.52/20.65 thf(822,plain,((semilattice_sup @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 61.52/20.65 thf(232,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA]: ((sup_sup @ TA @ (sup_sup @ TA @ A @ B) @ B) = (sup_sup @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_sup_Oright__idem)).
% 61.52/20.65 thf(1004,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA]: ((sup_sup @ TA @ (sup_sup @ TA @ A @ B) @ B) = (sup_sup @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 61.52/20.65 thf(127,axiom,((! [TA: $tType]: (boolean_algebra @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Lattices_Oboolean__algebra_11)).
% 61.52/20.65 thf(691,plain,((! [TA: $tType]: (boolean_algebra @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 61.52/20.65 thf(49,axiom,((bounded_lattice @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Lattices_Obounded__lattice)).
% 61.52/20.65 thf(442,plain,((bounded_lattice @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 61.52/20.65 thf(275,axiom,((! [A:variable,B:(set @ variable),C:(variable > real),D:(variable > real)]: ((member @ variable @ A @ B) => ((stateinterpol @ C @ D @ B @ A) = (C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_218_stateinterpol__left)).
% 61.52/20.65 thf(1120,plain,((! [A:variable,B:(set @ variable),C:(variable > real),D:(variable > real)]: ((member @ variable @ A @ B) => ((stateinterpol @ (C) @ (D) @ B @ A) = (C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[275])).
% 61.52/20.65 thf(71,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (uminus_uminus @ TA @ A) @ (uminus_uminus @ TA @ B)) = (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_neg__le__iff__le)).
% 61.52/20.65 thf(501,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (uminus_uminus @ TA @ A) @ (uminus_uminus @ TA @ B)) = (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 61.52/20.65 thf(28,axiom,((! [A:(variable > real),B:(variable > real),C:(set @ variable)]: (denotational_Vagree @ (stateinterpol @ A @ B @ C) @ A @ C))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_222_Vagree__stateinterpol)).
% 61.52/20.65 thf(369,plain,((! [A:(variable > real),B:(variable > real),C:(set @ variable)]: (denotational_Vagree @ (stateinterpol @ A @ B @ C) @ (A) @ C))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 61.52/20.65 thf(101,axiom,((denotational_Vagree = (^ [A:(variable > real),B:(variable > real)]: (denotational_Vagree @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_178_Vagree__sym)).
% 61.52/20.65 thf(607,plain,(((denotational_Vagree) = (^ [A:(variable > real),B:(variable > real)]: (denotational_Vagree @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 61.52/20.65 thf(66,axiom,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA,B:TA]: (((uminus_uminus @ TA @ A) = (uminus_uminus @ TA @ B)) = (A = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_neg__equal__iff__equal)).
% 61.52/20.65 thf(486,plain,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA,B:TA]: (((uminus_uminus @ TA @ A) = (uminus_uminus @ TA @ B)) = (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 61.52/20.65 thf(22,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_158_Timeso_Oinduct)).
% 61.52/20.65 thf(354,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)],[22])).
% 61.52/20.65 thf(117,axiom,((! [TA: $tType]: ((sup_sup @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (sup_sup @ (set @ TA) @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_Un__commute)).
% 61.52/20.65 thf(659,plain,((! [TA: $tType]: ((sup_sup @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (sup_sup @ (set @ TA) @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 61.52/20.65 thf(89,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_47_Collect__cong)).
% 61.52/20.65 thf(543,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)],[89])).
% 61.52/20.65 thf(133,axiom,((! [TA: $tType]: ((lattice @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ (sup_sup @ TA @ A @ B) @ C) = (sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_inf__sup__aci_I6_J)).
% 61.52/20.65 thf(708,plain,((! [TA: $tType]: ((lattice @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ (sup_sup @ TA @ A @ B) @ C) = (sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 61.52/20.65 thf(190,axiom,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA]: (((uminus_uminus @ TA @ A) = (zero_zero @ TA)) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_200_neg__equal__0__iff__equal)).
% 61.52/20.65 thf(882,plain,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA]: (((uminus_uminus @ TA @ A) = (zero_zero @ TA)) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 61.52/20.65 thf(68,axiom,((! [TA: $tType]: ((semilattice_inf @ TA) => (! [A:TA,B:TA]: ((inf_inf @ TA @ (inf_inf @ TA @ A @ B) @ B) = (inf_inf @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_241_inf_Oright__idem)).
% 61.52/20.65 thf(491,plain,((! [TA: $tType]: ((semilattice_inf @ TA) => (! [A:TA,B:TA]: ((inf_inf @ TA @ (inf_inf @ TA @ A @ B) @ B) = (inf_inf @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 61.52/20.65 thf(262,axiom,((! [A:(variable > real),B:(variable > real),C:(set @ variable)]: ((denotational_Vagree @ A @ B @ C) => (ord_less_eq @ (set @ variable) @ (statediff @ A @ B) @ (uminus_uminus @ (set @ variable) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_Vagree__statediff)).
% 61.52/20.65 thf(1088,plain,((! [A:(variable > real),B:(variable > real),C:(set @ variable)]: ((denotational_Vagree @ (A) @ (B) @ C) => (ord_less_eq @ (set @ variable) @ (statediff @ (A) @ (B)) @ (uminus_uminus @ (set @ variable) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[262])).
% 61.52/20.65 thf(54,axiom,((! [A:(option @ trm)]: ((! [B:trm]: (A != (some @ trm @ B))) => (A = (none @ trm))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_160_Differentialo_Ocases)).
% 61.52/20.65 thf(454,plain,((! [A:(option @ trm)]: ((! [B:trm]: ~ (A = (some @ trm @ B))) => (A = (none @ trm))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 61.52/20.65 thf(255,axiom,((! [TA: $tType]: ((lattice @ TA) => (! [A:TA,B:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ A @ B)) = (sup_sup @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_inf__sup__aci_I8_J)).
% 61.52/20.65 thf(1069,plain,((! [TA: $tType]: ((lattice @ TA) => (! [A:TA,B:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ A @ B)) = (sup_sup @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[255])).
% 61.52/20.65 thf(2975,plain,(($false)),inference(e,[status(thm)],[892,1036,1105,1031,518,468,1179,555,666,481,308,449,1142,511,677,861,1173,1078,1137,1164,1063,340,1095,1196,1001,417,436,973,885,570,504,357,1059,949,542,702,751,638,870,969,325,1100,1013,770,475,756,443,1151,348,966,821,1109,321,602,397,734,866,1072,998,428,527,307,439,546,925,1199,810,366,534,1047,798,1163,894,746,778,1042,561,424,429,788,815,407,693,630,484,625,879,435,830,889,461,1027,1128,324,1106,682,1195,874,317,650,1111,725,980,869,989,1160,1082,339,753,1182,537,1075,489,1039,328,471,622,1114,647,1131,1192,1050,911,371,343,633,508,311,921,1170,674,1185,773,1202,792,662,718,906,425,513,1103,573,1154,423,1007,402,743,958,1124,826,711,641,391,936,611,713,1092,335,1090,804,672,831,1117,737,303,863,764,979,604,900,406,362,451,567,494,609,848,1029,964,330,345,858,552,943,1022,462,932,983,1044,1066,780,1015,1176,851,505,653,922,685,521,394,986,722,1034,531,374,1134,812,1081,516,939,1145,836,795,680,458,823,776,855,1025,705,887,954,993,1053,951,359,1085,470,336,656,727,1140,314,446,497,845,465,627,1157,524,759,1189,1010,931,539,976,688,903,699,961,748,304,946,351,731,995,914,478,549,432,833,1097,818,405,1148,564,918,897,1056,400,828,635,532,696,720,928,358,807,839,740,1019,528,644,822,1004,691,442,1120,501,369,607,486,354,659,543,708,882,491,1088,454,1069])).
% 61.52/20.65 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.52/20.65 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------