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

%------------------------------------------------------------------------------
% File     : Leo-III---1.8.0
% Problem  : ITP033^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 : n001.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Wed Sep 30 08:06:29 AM UTC 2026

% Result   : Theorem 46.78s 26.48s
% Output   : Refutation 47.90s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ITP033^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.10/0.23  % Computer : n001.cluster.edu
% 0.10/0.23  % Model    : x86_64 x86_64
% 0.10/0.23  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.23  % Memory   : 8046.5625MB
% 0.10/0.23  % OS       : Linux 6.8.0-71-generic
% 0.10/0.23  % CPULimit : 300
% 0.10/0.23  % WCLimit  : 300
% 0.10/0.23  % DateTime : Tue Sep 29 19:44:58 UTC 2026
% 0.10/0.23  % CPUTime  : 
% 0.10/0.23  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.99/0.80  % [INFO] 	 Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ... 
% 2.24/1.21  % [INFO] 	 Parsing done (403ms). 
% 2.24/1.22  % [INFO] 	 Running in sequential loop mode. 
% 3.47/1.60  % [INFO] 	 eprover registered as external prover. 
% 3.47/1.61  % [INFO] 	 Scanning for conjecture ... 
% 3.64/1.76  % [INFO] 	 Found a conjecture (or negated_conjecture) and 279 axioms. Running axiom selection ... 
% 4.20/1.91  % [INFO] 	 Axiom selection finished. Selected 263 axioms (removed 16 axioms). 
% 5.13/2.24  % [INFO] 	 Problem is higher-order (TPTP THF). 
% 5.13/2.27  % [INFO] 	 Type checking passed. 
% 5.13/2.28  % [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 ... 
% 46.78/26.47  % External prover 'e' found a proof!
% 46.78/26.47  % [INFO] 	 Killing All external provers ... 
% 46.78/26.47  % Time passed: 26102ms (effective reasoning time: 25241ms)
% 46.78/26.47  % 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)>
% 46.78/26.48  % Axioms used in derivation (263): fact_158_dual__order_Ostrict__iff__order, tcon_fun___Orderings_Obot, fact_145_le__imp__less__or__eq, fact_34_subsetI, fact_52_ord__eq__le__subst, fact_73_ord__less__eq__subst, fact_26_binsert_Osimps_I2_J, fact_88_ord__eq__less__trans, fact_193_pinf_I1_J, fact_170_pinf_I6_J, fact_224_case__prod__app, fact_242_rev__predicate2D, fact_3_sortLemmaL, fact_32_subset__empty, fact_53_ord__le__eq__subst, fact_9_memb__spec, fact_37_all__not__in__conv, fact_92_less__not__sym, fact_226_bot__empty__eq2, fact_187_psubset__eq, tcon_HOL_Obool___Orderings_Olinorder_11, fact_43_le__funE, fact_38_empty__iff, fact_189_less__eq__set__def, fact_184_subset__not__subset__eq, fact_55_antisym, fact_195_pinf_I3_J, fact_12_sorted__distinct, fact_148_order_Ostrict__trans1, fact_248_case__prodE2, fact_197_pinf_I5_J, tcon_Int_Oint___Orderings_Oorder_2, fact_230_ssubst__Pair__rhs, fact_117_equalityD2, fact_220_subset__CollectI, fact_104_not__less__iff__gr__or__eq, fact_240_eq__subset, fact_250_cond__case__prod__eta, fact_0_t2nTip, fact_190_verit__la__disequality, fact_232_mem__case__prodI2, fact_8_sortedTree_Osimps_I1_J, fact_18_Tree_Oexhaust, fact_15_binsert_Osimps_I1_J, fact_152_dual__order_Ostrict__trans1, fact_130_order__le__less__subst1, tcon_fun___Orderings_Oord, fact_103_dual__order_Ostrict__trans, fact_244_case__prodE, fact_109_equals0D, fact_77_gt__ex, fact_141_less__le__trans, fact_185_psubset__subset__trans, tcon_Set_Oset___Orderings_Obot_8, fact_17_Tree_Oinduct, fact_1_s, fact_96_less__imp__triv, fact_202_minf_I3_J, fact_160_order_Onot__eq__order__implies__strict, fact_115_subset__eq, fact_132_order__less__le__subst1, fact_127_leI, fact_68_linorder__wlog, fact_172_complete__interval, fact_154_dense__ge__bounded, fact_39_bot__apply, fact_2_res, fact_40_order__refl, fact_50_order__subst1, fact_210_Collect__empty__eq__bot, fact_234_case__prodI, fact_13__092_060open_062Tip_A_092_060noteq_062_ATip_A_092_060and_062_AsortedTree_Ah_ATip_A_092_060longrightarrow_062_AsortedTree_Ah_A_Iwrm_Ah_ATip_J_092_060close_062, fact_87_less__irrefl, fact_200_minf_I1_J, fact_41_bot__set__def, fact_182_subset__iff__psubset__eq, fact_49_le__fun__def, fact_181_not__psubset__empty, fact_119_subset__refl, fact_58_le__cases, fact_156_order_Ostrict__implies__order, fact_106_dual__order_Ostrict__implies__not__eq, fact_140_le__less__trans, fact_110_equals0I, fact_192_verit__comp__simplify1_I1_J, fact_231_case__prod__conv, fact_254_prod_Odisc__eq__case, tcon_Int_Oint___Orderings_Opreorder_1, fact_46_Collect__mem__eq, fact_90_dual__order_Oasym, fact_23_remove_Osimps_I1_J, fact_228_pred__subset__eq2, fact_251_less__by__empty, fact_19_rm__set, fact_174_psubsetI, fact_75_order__less__subst2, fact_78_neqE, fact_85_less__trans, fact_121_subset__trans, fact_207_prop__restrict, fact_213_less__set__def, fact_95_less__imp__not__eq2, fact_139_less__imp__le, fact_35_empty__Collect__eq, fact_208_Collect__restrict, fact_235_case__prodI2, fact_63_ord__eq__le__trans, fact_105_order_Ostrict__implies__not__eq, fact_81_dense, tcon_Int_Oint___Conditionally__Complete__Lattices_Oconditionally__complete__linorder, fact_124_empty__def, fact_188_psubsetE, fact_255_inv__image__def, fact_241_predicate2D, fact_209_bot__empty__eq, fact_118_subset__iff, fact_67_dual__order_Orefl, fact_138_antisym__conv2, fact_83_less__asym, fact_44_le__funI, fact_11_h2, fact_107_bot__fun__def, fact_133_order__less__le__subst2, fact_70_dual__order_Oeq__iff, fact_125_Collect__subset, tcon_Set_Oset___Orderings_Oorder_6, fact_21_wrm__set1, tcon_Int_Oint___Orderings_Olinorder, fact_129_less__le, fact_5_Tree_Oinject, fact_31_empty__subsetI, tcon_HOL_Obool___Orderings_Oorder_12, fact_237_mem__case__prodI, fact_97_linorder__cases, fact_82_less__imp__neq, fact_36_Collect__empty__eq, fact_144_le__less__linear, fact_99_order_Ostrict__trans, tcon_Set_Oset___Orderings_Oord_7, fact_14_Tree_Odistinct_I1_J, fact_146_less__le__not__le, fact_91_less__imp__not__eq, fact_45_mem__Collect__eq, tcon_HOL_Obool___Orderings_Opreorder_10, fact_27_setOf_Osimps_I1_J, fact_243_case__prodD, fact_147_not__le__imp__less, fact_33_subset__antisym, fact_169_pinf_I8_J, fact_175_less__fun__def, fact_219_subset__Collect__iff, fact_171_verit__comp__simplify1_I3_J, fact_225_case__prod__Pair__iden, fact_196_pinf_I4_J, fact_7_h1, fact_222_remove_Osimps_I2_J, fact_89_ord__less__eq__trans, fact_217_psubsetD, fact_194_pinf_I2_J, fact_42_le__funD, fact_113_subsetD, fact_168_minf_I6_J, fact_203_minf_I4_J, fact_143_dense__le, fact_47_Collect__cong, fact_79_neq__iff, fact_150_order_Oorder__iff__strict, fact_236_case__prodI2_H, fact_80_order_Oasym, fact_84_less__asym_H, fact_214_rev__predicate1D, fact_102_linorder__less__wlog, fact_20_rm_Osimps, tcon_HOL_Obool___Orderings_Obot_14, fact_114_equalityE, fact_206_minf_I11_J, fact_167_minf_I8_J, fact_229_pred__equals__eq2, fact_60_le__cases3, fact_216_psubset__trans, fact_252_relChain__def, fact_94_antisym__conv3, fact_191_ex__gt__or__lt, tcon_HOL_Obool___Orderings_Oord_13, fact_25_Tree_Osimps_I5_J, tcon_fun___Orderings_Opreorder, fact_212_predicate1I, fact_51_order__subst2, fact_30_Tree_Ocase__distrib, fact_126_leD, fact_249_case__prod__eta, fact_61_antisym__conv, fact_122_set__eq__subset, fact_149_order_Ostrict__trans2, fact_4_sortLemmaR, fact_98_dual__order_Oirrefl, fact_247_prod_Ocase__distrib, fact_215_predicate1D, fact_6_binsert__sorted, fact_221_conj__subset__def, fact_116_equalityD1, fact_201_minf_I2_J, fact_120_Collect__mono, fact_159_dual__order_Ostrict__implies__order, fact_65_order__class_Oorder_Oantisym, fact_245_case__prodD_H, fact_10_sorted__distinct__pred__def, fact_101_exists__least__iff, fact_62_order__class_Oorder_Oeq__iff, fact_151_order_Ostrict__iff__order, fact_142_dense__ge, fact_123_Collect__mono__iff, tcon_fun___Orderings_Oorder, fact_198_pinf_I7_J, fact_100_less__imp__not__less, fact_108_emptyE, tcon_Int_Oint___Orderings_Ono__bot, fact_155_dense__le__bounded, fact_22_sortedTree_Osimps_I2_J, fact_28_Tree_Osimps_I6_J, fact_183_subset__psubset__trans, fact_153_dual__order_Ostrict__trans2, fact_71_dual__order_Oantisym, fact_72_ord__eq__less__subst, fact_86_less__linear, fact_131_order__le__less__subst2, fact_205_minf_I7_J, fact_246_case__prodE_H, fact_253_split__part, fact_134_not__le, fact_239_predicate2D__conj, tcon_Int_Oint___Orderings_Ono__top, fact_74_order__less__subst1, fact_128_le__less, fact_166_subset__emptyI, fact_199_pinf_I11_J, fact_29_Tree_Osimps_I7_J, fact_136_le__neq__trans, fact_59_order_Otrans, fact_24_Tree_Osimps_I4_J, fact_76_lt__ex, tcon_Set_Oset___Orderings_Opreorder_5, fact_54_eq__iff, fact_66_order__trans, fact_233_predicate2I, fact_186_psubset__imp__subset, fact_157_dual__order_Oorder__iff__strict, fact_137_antisym__conv1, fact_56_linear, tcon_Int_Oint___Orderings_Oord_3, fact_223_wrmrm__decomp, fact_16_wrm_Osimps, fact_57_eq__refl, fact_111_ex__in__conv, fact_64_ord__le__eq__trans, fact_112_in__mono, fact_93_less__induct, fact_69_dual__order_Otrans, fact_238_Collect__case__prod__mono, fact_135_not__less, fact_204_minf_I5_J, fact_227_subrelI, fact_218_pred__subset__eq
% 46.78/26.48  % No. of inferences in proof: 530
% 46.78/26.48  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 26102 ms resp. 25241 ms w/o parsing
% 47.90/26.73  % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 47.90/26.73  thf(int_type, type, int: $tType).
% 47.90/26.73  thf(a_type, type, a: $tType).
% 47.90/26.73  thf(bot_decl, type, bot: !> [TA: $tType]: $o).
% 47.90/26.73  thf(ord_decl, type, ord: !> [TA: $tType]: $o).
% 47.90/26.73  thf(order_decl, type, order: !> [TA: $tType]: $o).
% 47.90/26.73  thf(no_bot_decl, type, no_bot: !> [TA: $tType]: $o).
% 47.90/26.73  thf(no_top_decl, type, no_top: !> [TA: $tType]: $o).
% 47.90/26.73  thf(linorder_decl, type, linorder: !> [TA: $tType]: $o).
% 47.90/26.73  thf(preorder_decl, type, preorder: !> [TA: $tType]: $o).
% 47.90/26.73  thf(wellorder_decl, type, wellorder: !> [TA: $tType]: $o).
% 47.90/26.73  thf(dense_order_decl, type, dense_order: !> [TA: $tType]: $o).
% 47.90/26.73  thf(dense_linorder_decl, type, dense_linorder: !> [TA: $tType]: $o).
% 47.90/26.73  thf(condit1656338222tinuum_decl, type, condit1656338222tinuum: !> [TA: $tType]: $o).
% 47.90/26.73  thf(condit1037483654norder_decl, type, condit1037483654norder: !> [TA: $tType]: $o).
% 47.90/26.73  thf(bNF_Ca1785829860lChain_decl, type, bNF_Ca1785829860lChain: !> [TA: $tType,TB: $tType]: ((set @ (product_prod @ TB @ TB)) > ((TB > TA) > $o))).
% 47.90/26.73  thf(binary210054475elle_T_decl, type, binary210054475elle_T: !> [TA: $tType]: ((binary1291135688e_Tree @ TA) > (TA > ((binary1291135688e_Tree @ TA) > (binary1291135688e_Tree @ TA))))).
% 47.90/26.73  thf(binary1746293266le_Tip_decl, type, binary1746293266le_Tip: !> [TA: $tType]: (binary1291135688e_Tree @ TA)).
% 47.90/26.73  thf(binary536355927e_Tree_decl, type, binary536355927e_Tree: !> [TA: $tType,TB: $tType]: (TB > (((binary1291135688e_Tree @ TA) > (TA > ((binary1291135688e_Tree @ TA) > TB))) > ((binary1291135688e_Tree @ TA) > TB)))).
% 47.90/26.73  thf(binary1929596613c_Tree_decl, type, binary1929596613c_Tree: !> [TA: $tType,TB: $tType]: (TB > (((binary1291135688e_Tree @ TA) > (TA > ((binary1291135688e_Tree @ TA) > (TB > (TB > TB))))) > ((binary1291135688e_Tree @ TA) > TB)))).
% 47.90/26.73  thf(binary1830089824insert_decl, type, binary1830089824insert: !> [TA: $tType]: ((TA > int) > (TA > ((binary1291135688e_Tree @ TA) > (binary1291135688e_Tree @ TA))))).
% 47.90/26.73  thf(binary827270440e_memb_decl, type, binary827270440e_memb: !> [TA: $tType]: ((TA > int) > (TA > ((binary1291135688e_Tree @ TA) > $o)))).
% 47.90/26.73  thf(binary997842527remove_decl, type, binary997842527remove: !> [TA: $tType]: ((TA > int) > (TA > ((binary1291135688e_Tree @ TA) > (binary1291135688e_Tree @ TA))))).
% 47.90/26.73  thf(binary576689334lle_rm_decl, type, binary576689334lle_rm: !> [TA: $tType]: ((TA > int) > ((binary1291135688e_Tree @ TA) > TA))).
% 47.90/26.73  thf(binary1653327646_setOf_decl, type, binary1653327646_setOf: !> [TA: $tType]: ((binary1291135688e_Tree @ TA) > (set @ TA))).
% 47.90/26.73  thf(binary1610619414edTree_decl, type, binary1610619414edTree: !> [TA: $tType]: ((TA > int) > ((binary1291135688e_Tree @ TA) > $o))).
% 47.90/26.73  thf(binary231205461t_pred_decl, type, binary231205461t_pred: !> [TA: $tType]: ((TA > int) > (TA > (TA > ((binary1291135688e_Tree @ TA) > $o))))).
% 47.90/26.73  thf(binary213313527le_wrm_decl, type, binary213313527le_wrm: !> [TA: $tType]: ((TA > int) > ((binary1291135688e_Tree @ TA) > (binary1291135688e_Tree @ TA)))).
% 47.90/26.73  thf(binary1271298290_wrmrm_decl, type, binary1271298290_wrmrm: !> [TA: $tType]: ((TA > int) > ((binary1291135688e_Tree @ TA) > (product_prod @ (binary1291135688e_Tree @ TA) @ TA)))).
% 47.90/26.73  thf(bot_bot_decl, type, bot_bot: !> [TA: $tType]: TA).
% 47.90/26.73  thf(ord_less_decl, type, ord_less: !> [TA: $tType]: (TA > (TA > $o))).
% 47.90/26.73  thf(ord_less_eq_decl, type, ord_less_eq: !> [TA: $tType]: (TA > (TA > $o))).
% 47.90/26.73  thf(product_Pair_decl, type, product_Pair: !> [TA: $tType,TB: $tType]: (TB > (TA > (product_prod @ TB @ TA)))).
% 47.90/26.73  thf(product_case_prod_decl, type, product_case_prod: !> [TA: $tType,TB: $tType,TC: $tType]: ((TC > (TB > TA)) > ((product_prod @ TC @ TB) > TA))).
% 47.90/26.73  thf(inv_image_decl, type, inv_image: !> [TA: $tType,TB: $tType]: ((set @ (product_prod @ TB @ TB)) > ((TA > TB) > (set @ (product_prod @ TA @ TA))))).
% 47.90/26.73  thf(collect_decl, type, collect: !> [TA: $tType]: ((TA > $o) > (set @ TA))).
% 47.90/26.73  thf(member_decl, type, member: !> [TA: $tType]: (TA > ((set @ TA) > $o))).
% 47.90/26.73  thf(h_decl, type, h: (a > int)).
% 47.90/26.73  thf(t1_decl, type, t1: (binary1291135688e_Tree @ a)).
% 47.90/26.73  thf(t2_decl, type, t2: (binary1291135688e_Tree @ a)).
% 47.90/26.73  thf(x_decl, type, x: a).
% 47.90/26.73  thf(27,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:TC,B:(TB > (TA > (set @ TC))),C:TB,D:TA]: ((member @ TC @ A @ (B @ C @ D)) => (member @ TC @ A @ (product_case_prod @ TB @ TA @ (set @ TC) @ B @ (product_Pair @ TB @ TA @ C @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_237_mem__case__prodI)).
% 47.90/26.73  thf(365,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:TC,B:(TB > (TA > (set @ TC))),C:TB,D:TA]: ((member @ TC @ A @ (B @ C @ D)) => (member @ TC @ A @ (product_case_prod @ TB @ TA @ (set @ TC) @ (B) @ (product_Pair @ TB @ TA @ C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 47.90/26.73  thf(254,axiom,((! [TA: $tType]: (! [A:(TA > int),B:(binary1291135688e_Tree @ TA),C:TA,D:(binary1291135688e_Tree @ TA)]: ((binary1610619414edTree @ TA @ A @ (binary210054475elle_T @ TA @ B @ C @ D)) => (binary1610619414edTree @ TA @ A @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_sortLemmaR)).
% 47.90/26.73  thf(1105,plain,((! [TA: $tType]: (! [A:(TA > int),B:(binary1291135688e_Tree @ TA),C:TA,D:(binary1291135688e_Tree @ TA)]: ((binary1610619414edTree @ TA @ (A) @ (binary210054475elle_T @ TA @ B @ C @ D)) => (binary1610619414edTree @ TA @ (A) @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[254])).
% 47.90/26.73  thf(62,axiom,((order @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oorder_12)).
% 47.90/26.73  thf(468,plain,((order @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 47.90/26.73  thf(256,axiom,((((t2 != (binary1746293266le_Tip @ a)) & (binary1610619414edTree @ a @ h @ t2)) => (binary1610619414edTree @ a @ h @ (binary213313527le_wrm @ a @ h @ t2)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_h2)).
% 47.90/26.73  thf(1110,plain,(((~ (t2 = (binary1746293266le_Tip @ a)) & (binary1610619414edTree @ a @ (h) @ t2)) => (binary1610619414edTree @ a @ (h) @ (binary213313527le_wrm @ a @ (h) @ t2)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[256])).
% 47.90/26.73  thf(185,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA),D:(TA > $o)]: ((member @ TA @ A @ B) => ((ord_less_eq @ (set @ TA) @ B @ (collect @ TA @ (^ [E:TA]: ((member @ TA @ E @ C) & (D @ E))))) => (D @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_prop__restrict)).
% 47.90/26.73  thf(909,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA),D:(TA > $o)]: ((member @ TA @ A @ B) => ((ord_less_eq @ (set @ TA) @ B @ (collect @ TA @ (^ [E:TA]: ((member @ TA @ E @ C) & (D @ E))))) => (D @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 47.90/26.73  thf(112,axiom,((! [TA: $tType,TB: $tType]: (! [A:$o,B:(TA > (TB > $o))]: ((product_case_prod @ TA @ TB @ $o @ (^ [C:TA,D:TB]: ((A) & (B @ C @ D)))) = (^ [C:(product_prod @ TA @ TB)]: ((A) & (product_case_prod @ TA @ TB @ $o @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_253_split__part)).
% 47.90/26.73  thf(628,plain,((! [TA: $tType,TB: $tType]: (! [A:$o,B:(TA > (TB > $o))]: ((product_case_prod @ TA @ TB @ $o @ (^ [C:TA,D:TB]: ((A) & (B @ C @ D)))) = (^ [C:(product_prod @ TA @ TB)]: ((A) & (product_case_prod @ TA @ TB @ $o @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 47.90/26.73  thf(99,axiom,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ B @ A) & (ord_less_eq @ TA @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_dual__order_Oeq__iff)).
% 47.90/26.73  thf(582,plain,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ B @ A) & (ord_less_eq @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 47.90/26.73  thf(216,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_leI)).
% 47.90/26.73  thf(1005,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 47.90/26.73  thf(127,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > $o),B:(TA > $o),C:(TA > $o),D:(TA > $o)]: ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => ((A @ F) = (B @ F)))) => ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => ((C @ F) = (D @ F)))) => (? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => (((A @ F) & (C @ F)) = ((B @ F) & (D @ F))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_pinf_I1_J)).
% 47.90/26.73  thf(683,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > $o),B:(TA > $o),C:(TA > $o),D:(TA > $o)]: ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => ((A @ F) = (B @ F)))) => ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => ((C @ F) = (D @ F)))) => (? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => (((A @ F) & (C @ F)) = ((B @ F) & (D @ F))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 47.90/26.73  thf(5,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TC > (TA > TB)),B:TC,C:TA]: ((product_case_prod @ TC @ TA @ TB @ A @ (product_Pair @ TC @ TA @ B @ C)) = (A @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_case__prod__conv)).
% 47.90/26.73  thf(276,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TC > (TA > TB)),B:TC,C:TA]: ((product_case_prod @ TC @ TA @ TB @ (A) @ (product_Pair @ TC @ TA @ B @ C)) = (A @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 47.90/26.73  thf(14,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_less__imp__not__less)).
% 47.90/26.73  thf(308,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 47.90/26.73  thf(240,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_109_equals0D)).
% 47.90/26.73  thf(1073,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)],[240])).
% 47.90/26.73  thf(54,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_dual__order_Oirrefl)).
% 47.90/26.73  thf(440,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 47.90/26.73  thf(84,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:TA]: ? [B:TB]: ! [C:TB]: ((ord_less @ TB @ B @ C) => (A = A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_199_pinf_I11_J)).
% 47.90/26.73  thf(533,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 47.90/26.73  thf(90,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => ((ord_less_eq @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB)]: ! [C:TA]: (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_le__fun__def)).
% 47.90/26.73  thf(550,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => ((ord_less_eq @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB)]: ! [C:TA]: (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 47.90/26.73  thf(76,axiom,((! [TA: $tType]: (! [A:(TA > (TA > $o))]: (ord_less_eq @ (TA > (TA > $o)) @ ((=) @ TA) @ (^ [B:TA,C:TA]: ((A @ B @ C) | (B = C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_240_eq__subset)).
% 47.90/26.73  thf(500,plain,((! [TA: $tType]: (! [A:(TA > (TA > $o))]: (ord_less_eq @ (TA > (TA > $o)) @ ((=) @ TA) @ (^ [B:TA,C:TA]: ((A @ B @ C) | (B = C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 47.90/26.73  thf(154,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) => (B @ C))) => (ord_less_eq @ (set @ TA) @ (collect @ TA @ A) @ (collect @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_120_Collect__mono)).
% 47.90/26.73  thf(797,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) => (B @ C))) => (ord_less_eq @ (set @ TA) @ (collect @ TA @ (A)) @ (collect @ TA @ (B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 47.90/26.73  thf(135,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) => (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_le__cases)).
% 47.90/26.73  thf(715,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) => (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 47.90/26.73  thf(158,axiom,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_gt__ex)).
% 47.90/26.73  thf(814,plain,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 47.90/26.73  thf(198,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_112_in__mono)).
% 47.90/26.73  thf(945,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 47.90/26.73  thf(86,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((A = B) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_eq__refl)).
% 47.90/26.73  thf(538,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((A = B) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 47.90/26.73  thf(145,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_149_order_Ostrict__trans2)).
% 47.90/26.73  thf(747,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 47.90/26.73  thf(187,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_37_all__not__in__conv)).
% 47.90/26.73  thf(913,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)],[187])).
% 47.90/26.73  thf(40,axiom,((! [TA: $tType]: ((bot_bot @ (set @ TA)) = (collect @ TA @ (^ [A:TA]: (($false))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_124_empty__def)).
% 47.90/26.73  thf(404,plain,((! [TA: $tType]: ((bot_bot @ (set @ TA)) = (collect @ TA @ (^ [A:TA]: (($false))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 47.90/26.73  thf(181,axiom,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_108_emptyE)).
% 47.90/26.73  thf(898,plain,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 47.90/26.73  thf(11,axiom,((! [TA: $tType]: (preorder @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Opreorder_5)).
% 47.90/26.73  thf(301,plain,((! [TA: $tType]: (preorder @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 47.90/26.73  thf(95,axiom,((! [TA: $tType,TB: $tType]: ((bot_bot @ (TA > (TB > $o))) = (^ [A:TA,B:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ A @ B) @ (bot_bot @ (set @ (product_prod @ TA @ TB)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_226_bot__empty__eq2)).
% 47.90/26.73  thf(570,plain,((! [TA: $tType,TB: $tType]: ((bot_bot @ (TA > (TB > $o))) = (^ [A:TA,B:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ A @ B) @ (bot_bot @ (set @ (product_prod @ TA @ TB)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 47.90/26.73  thf(137,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TB > $o)),B:(TA > (TB > $o))]: ((ord_less_eq @ (TA > (TB > $o)) @ A @ B) => (ord_less_eq @ (set @ (product_prod @ TA @ TB)) @ (collect @ (product_prod @ TA @ TB) @ (product_case_prod @ TA @ TB @ $o @ A)) @ (collect @ (product_prod @ TA @ TB) @ (product_case_prod @ TA @ TB @ $o @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_Collect__case__prod__mono)).
% 47.90/26.73  thf(719,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TB > $o)),B:(TA > (TB > $o))]: ((ord_less_eq @ (TA > (TB > $o)) @ (A) @ (B)) => (ord_less_eq @ (set @ (product_prod @ TA @ TB)) @ (collect @ (product_prod @ TA @ TB) @ (product_case_prod @ TA @ TB @ $o @ A)) @ (collect @ (product_prod @ TA @ TB) @ (product_case_prod @ TA @ TB @ $o @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 47.90/26.73  thf(78,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:TA]: ? [B:TB]: ! [C:TB]: ((ord_less @ TB @ C @ B) => (A = A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_minf_I11_J)).
% 47.90/26.73  thf(504,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 47.90/26.73  thf(147,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less_eq @ TB @ A @ (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_130_order__le__less__subst1)).
% 47.90/26.73  thf(751,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less_eq @ TB @ A @ (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 47.90/26.73  thf(20,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TB > (TC > (TA > $o))),B:(product_prod @ TB @ TC),C:TA]: ((product_case_prod @ TB @ TC @ (TA > $o) @ A @ B @ C) => (~ (! [D:TB,E:TC]: ((B = (product_Pair @ TB @ TC @ D @ E)) => (~ (A @ D @ E @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_case__prodE_H)).
% 47.90/26.73  thf(344,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TB > (TC > (TA > $o))),B:(product_prod @ TB @ TC),C:TA]: ((product_case_prod @ TB @ TC @ (TA > $o) @ (A) @ B @ C) => (~ (! [D:TB,E:TC]: ((B = (product_Pair @ TB @ TC @ D @ E)) => (~ (A @ D @ E @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 47.90/26.73  thf(236,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (B != A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_158_dual__order_Ostrict__iff__order)).
% 47.90/26.73  thf(1059,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[236])).
% 47.90/26.73  thf(87,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_dual__order_Oasym)).
% 47.90/26.73  thf(542,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 47.90/26.73  thf(246,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((ord_less @ (set @ TA) @ A @ B) => ((ord_less @ (set @ TA) @ B @ C) => (ord_less @ (set @ TA) @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_216_psubset__trans)).
% 47.90/26.73  thf(1087,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((ord_less @ (set @ TA) @ A @ B) => ((ord_less @ (set @ TA) @ B @ C) => (ord_less @ (set @ TA) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[246])).
% 47.90/26.73  thf(47,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB),C:TA]: ((ord_less_eq @ (TA > TB) @ A @ B) => (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_42_le__funD)).
% 47.90/26.73  thf(421,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB),C:TA]: ((ord_less_eq @ (TA > TB) @ (A) @ (B)) => (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 47.90/26.73  thf(206,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((ord_less @ (set @ TA) @ A @ B) => ((ord_less_eq @ (set @ TA) @ B @ C) => (ord_less @ (set @ TA) @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_185_psubset__subset__trans)).
% 47.90/26.73  thf(969,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((ord_less @ (set @ TA) @ A @ B) => ((ord_less_eq @ (set @ TA) @ B @ C) => (ord_less @ (set @ TA) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 47.90/26.73  thf(45,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_210_Collect__empty__eq__bot)).
% 47.90/26.73  thf(416,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)],[45])).
% 47.90/26.73  thf(258,axiom,((! [TA: $tType]: ((binary231205461t_pred @ TA) = (^ [A:(TA > int),B:TA,C:TA,D:(binary1291135688e_Tree @ TA)]: (((binary1610619414edTree @ TA @ A @ D) & (member @ TA @ B @ (binary1653327646_setOf @ TA @ D)) & (member @ TA @ C @ (binary1653327646_setOf @ TA @ D)) & ((A @ B) = (A @ C))) => (B = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_sorted__distinct__pred__def)).
% 47.90/26.73  thf(1115,plain,((! [TA: $tType]: ((binary231205461t_pred @ TA) = (^ [A:(TA > int),B:TA,C:TA,D:(binary1291135688e_Tree @ TA)]: (((binary1610619414edTree @ TA @ A @ D) & (member @ TA @ B @ (binary1653327646_setOf @ TA @ D)) & (member @ TA @ C @ (binary1653327646_setOf @ TA @ D)) & ((A @ B) = (A @ C))) => (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[258])).
% 47.90/26.73  thf(9,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > $o),B:(TA > $o),C:(TA > $o),D:(TA > $o)]: ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => ((A @ F) = (B @ F)))) => ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => ((C @ F) = (D @ F)))) => (? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => (((A @ F) | (C @ F)) = ((B @ F) | (D @ F))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_194_pinf_I2_J)).
% 47.90/26.73  thf(289,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > $o),B:(TA > $o),C:(TA > $o),D:(TA > $o)]: ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => ((A @ F) = (B @ F)))) => ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => ((C @ F) = (D @ F)))) => (? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => (((A @ F) | (C @ F)) = ((B @ F) | (D @ F))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 47.90/26.73  thf(72,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TA > $o)),B:TB,C:TA]: ((A @ B @ C) => (product_case_prod @ TB @ TA @ $o @ A @ (product_Pair @ TB @ TA @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_234_case__prodI)).
% 47.90/26.73  thf(492,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TA > $o)),B:TB,C:TA]: ((A @ B @ C) => (product_case_prod @ TB @ TA @ $o @ (A) @ (product_Pair @ TB @ TA @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 47.90/26.73  thf(228,axiom,((! [TA: $tType]: ((binary1653327646_setOf @ TA @ (binary1746293266le_Tip @ TA)) = (bot_bot @ (set @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_setOf_Osimps_I1_J)).
% 47.90/26.73  thf(1040,plain,((! [TA: $tType]: ((binary1653327646_setOf @ TA @ (binary1746293266le_Tip @ TA)) = (bot_bot @ (set @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 47.90/26.73  thf(221,axiom,((! [TA: $tType,TB: $tType]: (! [A:TA,B:((binary1291135688e_Tree @ TB) > (TB > ((binary1291135688e_Tree @ TB) > TA)))]: ((binary536355927e_Tree @ TA @ TB @ A @ B @ (binary1746293266le_Tip @ TB)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_Tree_Osimps_I4_J)).
% 47.90/26.73  thf(1020,plain,((! [TA: $tType,TB: $tType]: (! [A:TA,B:((binary1291135688e_Tree @ TB) > (TB > ((binary1291135688e_Tree @ TB) > TA)))]: ((binary536355927e_Tree @ TA @ TB @ A @ (B) @ (binary1746293266le_Tip @ TB)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 47.90/26.73  thf(157,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((A = B) => (~ ((ord_less_eq @ (set @ TA) @ A @ B) => (~ (ord_less_eq @ (set @ TA) @ B @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_equalityE)).
% 47.90/26.73  thf(806,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((A = B) => (~ ((ord_less_eq @ (set @ TA) @ A @ B) => (~ (ord_less_eq @ (set @ TA) @ B @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 47.90/26.73  thf(22,axiom,((! [TA: $tType]: ((bot_bot @ (set @ TA)) = (collect @ TA @ (bot_bot @ (TA > $o)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_bot__set__def)).
% 47.90/26.73  thf(353,plain,((! [TA: $tType]: ((bot_bot @ (set @ TA)) = (collect @ TA @ (bot_bot @ (TA > $o)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 47.90/26.73  thf(68,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((A != B) => ((~ (ord_less @ TA @ A @ B)) => (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_neqE)).
% 47.90/26.73  thf(480,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (A = B)) => ((~ (ord_less @ TA @ A @ B)) => (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 47.90/26.73  thf(176,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((A != B) => ((ord_less_eq @ TA @ A @ B) => (ord_less @ TA @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_160_order_Onot__eq__order__implies__strict)).
% 47.90/26.73  thf(877,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((~ (A = B)) => ((ord_less_eq @ TA @ A @ B) => (ord_less @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 47.90/26.73  thf(201,axiom,((! [TA: $tType,TB: $tType]: (! [A:TB,B:((binary1291135688e_Tree @ TA) > (TA > ((binary1291135688e_Tree @ TA) > (TB > (TB > TB))))),C:(binary1291135688e_Tree @ TA),D:TA,E:(binary1291135688e_Tree @ TA)]: ((binary1929596613c_Tree @ TB @ TA @ A @ B @ (binary210054475elle_T @ TA @ C @ D @ E)) = (B @ C @ D @ E @ (binary1929596613c_Tree @ TB @ TA @ A @ B @ C) @ (binary1929596613c_Tree @ TB @ TA @ A @ B @ E)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_Tree_Osimps_I7_J)).
% 47.90/26.73  thf(956,plain,((! [TA: $tType,TB: $tType]: (! [A:TB,B:((binary1291135688e_Tree @ TA) > (TA > ((binary1291135688e_Tree @ TA) > (TB > (TB > TB))))),C:(binary1291135688e_Tree @ TA),D:TA,E:(binary1291135688e_Tree @ TA)]: ((binary1929596613c_Tree @ TB @ TA @ A @ (B) @ (binary210054475elle_T @ TA @ C @ D @ E)) = (B @ C @ D @ E @ (binary1929596613c_Tree @ TB @ TA @ A @ (B) @ C) @ (binary1929596613c_Tree @ TB @ TA @ A @ (B) @ E)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 47.90/26.73  thf(121,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(product_prod @ TC @ TB),B:(TC > (TB > (TA > $o))),C:TA]: ((! [D:TC,E:TB]: (((product_Pair @ TC @ TB @ D @ E) = A) => (B @ D @ E @ C))) => (product_case_prod @ TC @ TB @ (TA > $o) @ B @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_case__prodI2_H)).
% 47.90/26.73  thf(660,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(product_prod @ TC @ TB),B:(TC > (TB > (TA > $o))),C:TA]: ((! [D:TC,E:TB]: (((product_Pair @ TC @ TB @ D @ E) = A) => (B @ D @ E @ C))) => (product_case_prod @ TC @ TB @ (TA > $o) @ (B) @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 47.90/26.73  thf(82,axiom,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_eq__iff)).
% 47.90/26.73  thf(527,plain,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 47.90/26.73  thf(105,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TA > $o)),B:(product_prod @ TB @ TA)]: ((product_case_prod @ TB @ TA @ $o @ A @ B) => (~ (! [C:TB,D:TA]: ((B = (product_Pair @ TB @ TA @ C @ D)) => (~ (A @ C @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_244_case__prodE)).
% 47.90/26.73  thf(602,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TA > $o)),B:(product_prod @ TB @ TA)]: ((product_case_prod @ TB @ TA @ $o @ (A) @ B) => (~ (! [C:TB,D:TA]: ((B = (product_Pair @ TB @ TA @ C @ D)) => (~ (A @ C @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 47.90/26.73  thf(211,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((A != B) => (ord_less @ TA @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_136_le__neq__trans)).
% 47.90/26.73  thf(981,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((~ (A = B)) => (ord_less @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 47.90/26.73  thf(43,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_less__trans)).
% 47.90/26.73  thf(411,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 47.90/26.73  thf(214,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ A @ B) | (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_145_le__imp__less__or__eq)).
% 47.90/26.73  thf(988,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ A @ B) | (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 47.90/26.73  thf(253,axiom,((binary1610619414edTree @ a @ h @ (binary210054475elle_T @ a @ t1 @ x @ t2))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_s)).
% 47.90/26.73  thf(1104,plain,((binary1610619414edTree @ a @ (h) @ (binary210054475elle_T @ a @ t1 @ x @ t2))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[253])).
% 47.90/26.73  thf(168,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((ord_less_eq @ (set @ TA) @ A @ (collect @ TA @ (^ [D:TA]: ((member @ TA @ D @ B) & (C @ D))))) = (! [D:TA]: ((member @ TA @ D @ A) => (C @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_subset__Collect__iff)).
% 47.90/26.73  thf(849,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((ord_less_eq @ (set @ TA) @ A @ (collect @ TA @ (^ [D:TA]: ((member @ TA @ D @ B) & (C @ D))))) = (! [D:TA]: ((member @ TA @ D @ A) => (C @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 47.90/26.73  thf(59,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > $o),B:(TA > $o),C:(TA > $o),D:(TA > $o)]: ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => ((A @ F) = (B @ F)))) => ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => ((C @ F) = (D @ F)))) => (? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => (((A @ F) | (C @ F)) = ((B @ F) | (D @ F))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_201_minf_I2_J)).
% 47.90/26.73  thf(452,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > $o),B:(TA > $o),C:(TA > $o),D:(TA > $o)]: ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => ((A @ F) = (B @ F)))) => ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => ((C @ F) = (D @ F)))) => (? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => (((A @ F) | (C @ F)) = ((B @ F) | (D @ F))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 47.90/26.73  thf(190,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_128_le__less)).
% 47.90/26.73  thf(920,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 47.90/26.73  thf(192,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_32_subset__empty)).
% 47.90/26.73  thf(925,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)],[192])).
% 47.90/26.73  thf(150,axiom,((! [TA: $tType]: ((condit1037483654norder @ TA) => (! [A:TA,B:TA,C:(TA > $o)]: ((ord_less @ TA @ A @ B) => ((C @ A) => ((~ (C @ B)) => (? [D:TA]: ((ord_less_eq @ TA @ A @ D) & (ord_less_eq @ TA @ D @ B) & ! [E:TA]: (((ord_less_eq @ TA @ A @ E) & (ord_less @ TA @ E @ D)) => (C @ E)) & ! [E:TA]: ((! [F:TA]: (((ord_less_eq @ TA @ A @ F) & (ord_less @ TA @ F @ E)) => (C @ F))) => (ord_less_eq @ TA @ E @ D))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_172_complete__interval)).
% 47.90/26.73  thf(761,plain,((! [TA: $tType]: ((condit1037483654norder @ TA) => (! [A:TA,B:TA,C:(TA > $o)]: ((ord_less @ TA @ A @ B) => ((C @ A) => ((~ (C @ B)) => (? [D:TA]: ((ord_less_eq @ TA @ A @ D) & (ord_less_eq @ TA @ D @ B) & ! [E:TA]: (((ord_less_eq @ TA @ A @ E) & (ord_less @ TA @ E @ D)) => (C @ E)) & ! [E:TA]: ((! [F:TA]: (((ord_less_eq @ TA @ A @ F) & (ord_less @ TA @ F @ E)) => (C @ F))) => (ord_less_eq @ TA @ E @ D))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 47.90/26.73  thf(85,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) => (B @ C))) => (ord_less_eq @ (TA > $o) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_212_predicate1I)).
% 47.90/26.73  thf(534,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) => (B @ C))) => (ord_less_eq @ (TA > $o) @ (A) @ (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 47.90/26.73  thf(231,axiom,((! [TA: $tType]: ((wellorder @ TA) => (((?) @ TA) = (^ [A:(TA > $o)]: ? [B:TA]: ((A @ B) & ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (A @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_exists__least__iff)).
% 47.90/26.73  thf(1047,plain,((! [TA: $tType]: ((wellorder @ TA) => (((?) @ TA) = (^ [A:(TA > $o)]: ? [B:TA]: ((A @ B) & ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (A @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[231])).
% 47.90/26.73  thf(81,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA,C:TA]: (((ord_less_eq @ TA @ A @ B) => (~ (ord_less_eq @ TA @ B @ C))) => (((ord_less_eq @ TA @ B @ A) => (~ (ord_less_eq @ TA @ A @ C))) => (((ord_less_eq @ TA @ A @ C) => (~ (ord_less_eq @ TA @ C @ B))) => (((ord_less_eq @ TA @ C @ B) => (~ (ord_less_eq @ TA @ B @ A))) => (((ord_less_eq @ TA @ B @ C) => (~ (ord_less_eq @ TA @ C @ A))) => (~ ((ord_less_eq @ TA @ C @ A) => (~ (ord_less_eq @ TA @ A @ B))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_60_le__cases3)).
% 47.90/26.73  thf(512,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA,C:TA]: (((ord_less_eq @ TA @ A @ B) => (~ (ord_less_eq @ TA @ B @ C))) => (((ord_less_eq @ TA @ B @ A) => (~ (ord_less_eq @ TA @ A @ C))) => (((ord_less_eq @ TA @ A @ C) => (~ (ord_less_eq @ TA @ C @ B))) => (((ord_less_eq @ TA @ C @ B) => (~ (ord_less_eq @ TA @ B @ A))) => (((ord_less_eq @ TA @ B @ C) => (~ (ord_less_eq @ TA @ C @ A))) => (~ ((ord_less_eq @ TA @ C @ A) => (~ (ord_less_eq @ TA @ A @ B))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 47.90/26.73  thf(197,axiom,((! [TA: $tType]: ((ord_less_eq @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: ! [C:TA]: ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_118_subset__iff)).
% 47.90/26.73  thf(942,plain,((! [TA: $tType]: ((ord_less_eq @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: ! [C:TA]: ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 47.90/26.73  thf(162,axiom,((! [TA: $tType]: (! [A:(TA > int),B:TA,C:TA,D:(binary1291135688e_Tree @ TA),E:(binary1291135688e_Tree @ TA)]: (((ord_less @ int @ (A @ B) @ (A @ C)) => ((binary997842527remove @ TA @ A @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = (binary210054475elle_T @ TA @ (binary997842527remove @ TA @ A @ B @ D) @ C @ E))) & ((~ (ord_less @ int @ (A @ B) @ (A @ C))) => (((ord_less @ int @ (A @ C) @ (A @ B)) => ((binary997842527remove @ TA @ A @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = (binary210054475elle_T @ TA @ D @ C @ (binary997842527remove @ TA @ A @ B @ E)))) & ((~ (ord_less @ int @ (A @ C) @ (A @ B))) => (((D = (binary1746293266le_Tip @ TA)) => ((binary997842527remove @ TA @ A @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = E)) & ((D != (binary1746293266le_Tip @ TA)) => ((binary997842527remove @ TA @ A @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = (product_case_prod @ (binary1291135688e_Tree @ TA) @ TA @ (binary1291135688e_Tree @ TA) @ (^ [F:(binary1291135688e_Tree @ TA),G:TA]: (binary210054475elle_T @ TA @ F @ G @ E)) @ (binary1271298290_wrmrm @ TA @ A @ D)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_222_remove_Osimps_I2_J)).
% 47.90/26.73  thf(825,plain,((! [TA: $tType]: (! [A:(TA > int),B:TA,C:TA,D:(binary1291135688e_Tree @ TA),E:(binary1291135688e_Tree @ TA)]: (((ord_less @ int @ (A @ B) @ (A @ C)) => ((binary997842527remove @ TA @ (A) @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = (binary210054475elle_T @ TA @ (binary997842527remove @ TA @ (A) @ B @ D) @ C @ E))) & ((~ (ord_less @ int @ (A @ B) @ (A @ C))) => (((ord_less @ int @ (A @ C) @ (A @ B)) => ((binary997842527remove @ TA @ (A) @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = (binary210054475elle_T @ TA @ D @ C @ (binary997842527remove @ TA @ (A) @ B @ E)))) & ((~ (ord_less @ int @ (A @ C) @ (A @ B))) => (((D = (binary1746293266le_Tip @ TA)) => ((binary997842527remove @ TA @ (A) @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = E)) & ((~ (D = (binary1746293266le_Tip @ TA))) => ((binary997842527remove @ TA @ (A) @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = (product_case_prod @ (binary1291135688e_Tree @ TA) @ TA @ (binary1291135688e_Tree @ TA) @ (^ [F:(binary1291135688e_Tree @ TA),G:TA]: (binary210054475elle_T @ TA @ F @ G @ E)) @ (binary1271298290_wrmrm @ TA @ (A) @ D)))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 47.90/26.73  thf(104,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (C != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_195_pinf_I3_J)).
% 47.90/26.73  thf(598,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (~ (C = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 47.90/26.73  thf(160,axiom,((! [TA: $tType]: (bot @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Obot_8)).
% 47.90/26.73  thf(820,plain,((! [TA: $tType]: (bot @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 47.90/26.73  thf(4,axiom,((linorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Olinorder_11)).
% 47.90/26.73  thf(275,plain,((linorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 47.90/26.73  thf(261,axiom,((! [TA: $tType]: (! [A:(TA > int),B:(binary1291135688e_Tree @ TA),C:TA,D:(binary1291135688e_Tree @ TA)]: ((binary1610619414edTree @ TA @ A @ (binary210054475elle_T @ TA @ B @ C @ D)) => (binary1610619414edTree @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_sortLemmaL)).
% 47.90/26.73  thf(1123,plain,((! [TA: $tType]: (! [A:(TA > int),B:(binary1291135688e_Tree @ TA),C:TA,D:(binary1291135688e_Tree @ TA)]: ((binary1610619414edTree @ TA @ (A) @ (binary210054475elle_T @ TA @ B @ C @ D)) => (binary1610619414edTree @ TA @ (A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[261])).
% 47.90/26.73  thf(21,axiom,((! [TA: $tType,TB: $tType]: (! [A:TA,B:TB,C:(set @ (product_prod @ TA @ TB)),D:TB]: ((member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ A @ B) @ C) => ((D = B) => (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ A @ D) @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_ssubst__Pair__rhs)).
% 47.90/26.73  thf(349,plain,((! [TA: $tType,TB: $tType]: (! [A:TA,B:TB,C:(set @ (product_prod @ TA @ TB)),D:TB]: ((member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ A @ B) @ C) => ((D = B) => (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ A @ D) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 47.90/26.73  thf(41,axiom,((! [TA: $tType,TB: $tType]: ((bot @ TA) => (bot @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Obot)).
% 47.90/26.73  thf(407,plain,((! [TA: $tType,TB: $tType]: ((bot @ TA) => (bot @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 47.90/26.73  thf(128,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less_eq @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_linorder__wlog)).
% 47.90/26.73  thf(693,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less_eq @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 47.90/26.73  thf(188,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_148_order_Ostrict__trans1)).
% 47.90/26.73  thf(916,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 47.90/26.73  thf(225,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_169_pinf_I8_J)).
% 47.90/26.73  thf(1032,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[225])).
% 47.90/26.73  thf(122,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_antisym)).
% 47.90/26.73  thf(665,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 47.90/26.73  thf(242,axiom,((! [TA: $tType]: ((ord_less @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) & ~ (ord_less_eq @ (set @ TA) @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_184_subset__not__subset__eq)).
% 47.90/26.73  thf(1079,plain,((! [TA: $tType]: ((ord_less @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) & ~ (ord_less_eq @ (set @ TA) @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 47.90/26.73  thf(149,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_order__le__less__subst2)).
% 47.90/26.73  thf(757,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 47.90/26.73  thf(263,axiom,((t2 != (binary1746293266le_Tip @ a))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_t2nTip)).
% 47.90/26.73  thf(1128,plain,((~ (t2 = (binary1746293266le_Tip @ a)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[263])).
% 47.90/26.73  thf(165,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_113_subsetD)).
% 47.90/26.73  thf(842,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 47.90/26.73  thf(208,axiom,((! [TA: $tType]: (! [A:(TA > int),B:TA,C:TA,D:(binary1291135688e_Tree @ TA)]: (binary231205461t_pred @ TA @ A @ B @ C @ D)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_sorted__distinct)).
% 47.90/26.73  thf(974,plain,((! [TA: $tType]: (! [A:(TA > int),B:TA,C:TA,D:(binary1291135688e_Tree @ TA)]: (binary231205461t_pred @ TA @ (A) @ B @ C @ D)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 47.90/26.73  thf(167,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((! [B:TA]: ~ (member @ TA @ B @ A)) => (ord_less_eq @ (set @ TA) @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_166_subset__emptyI)).
% 47.90/26.73  thf(847,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((! [B:TA]: ~ (member @ TA @ B @ A)) => (ord_less_eq @ (set @ TA) @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 47.90/26.73  thf(94,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less @ TB @ A @ (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_order__less__subst1)).
% 47.90/26.73  thf(566,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less @ TB @ A @ (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 47.90/26.73  thf(169,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_153_dual__order_Ostrict__trans2)).
% 47.90/26.73  thf(852,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 47.90/26.73  thf(52,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_less__irrefl)).
% 47.90/26.73  thf(435,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 47.90/26.73  thf(143,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((ord_less_eq @ (set @ TA) @ B @ C) => (ord_less_eq @ (set @ TA) @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_121_subset__trans)).
% 47.90/26.73  thf(742,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((ord_less_eq @ (set @ TA) @ B @ C) => (ord_less_eq @ (set @ TA) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 47.90/26.73  thf(247,axiom,((! [TA: $tType]: ((dense_order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (? [C:TA]: ((ord_less @ TA @ A @ C) & (ord_less @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_dense)).
% 47.90/26.73  thf(1089,plain,((! [TA: $tType]: ((dense_order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (? [C:TA]: ((ord_less @ TA @ A @ C) & (ord_less @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[247])).
% 47.90/26.73  thf(175,axiom,((! [TA: $tType]: ((preorder @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (ord_less_eq @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_146_less__le__not__le)).
% 47.90/26.73  thf(874,plain,((! [TA: $tType]: ((preorder @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (ord_less_eq @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 47.90/26.73  thf(108,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((~ (ord_less @ TA @ B @ A)) = (B = A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_antisym__conv3)).
% 47.90/26.73  thf(615,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((~ (ord_less @ TA @ B @ A)) = (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 47.90/26.73  thf(139,axiom,((! [TA: $tType]: (! [A:(TA > int),B:TA]: ((binary997842527remove @ TA @ A @ B @ (binary1746293266le_Tip @ TA)) = (binary1746293266le_Tip @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_remove_Osimps_I1_J)).
% 47.90/26.73  thf(725,plain,((! [TA: $tType]: (! [A:(TA > int),B:TA]: ((binary997842527remove @ TA @ (A) @ B @ (binary1746293266le_Tip @ TA)) = (binary1746293266le_Tip @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 47.90/26.73  thf(23,axiom,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Opreorder)).
% 47.90/26.73  thf(356,plain,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 47.90/26.73  thf(101,axiom,((preorder @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Opreorder_1)).
% 47.90/26.73  thf(593,plain,((preorder @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 47.90/26.73  thf(259,axiom,((! [TA: $tType]: (! [A:(TA > int),B:(binary1291135688e_Tree @ TA),C:TA]: ((binary1610619414edTree @ TA @ A @ B) => (binary1610619414edTree @ TA @ A @ (binary1830089824insert @ TA @ A @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_binsert__sorted)).
% 47.90/26.73  thf(1118,plain,((! [TA: $tType]: (! [A:(TA > int),B:(binary1291135688e_Tree @ TA),C:TA]: ((binary1610619414edTree @ TA @ (A) @ B) => (binary1610619414edTree @ TA @ (A) @ (binary1830089824insert @ TA @ (A) @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[259])).
% 47.90/26.73  thf(171,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (A != B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_151_order_Ostrict__iff__order)).
% 47.90/26.73  thf(857,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 47.90/26.73  thf(64,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (B = A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_dual__order_Oantisym)).
% 47.90/26.73  thf(471,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 47.90/26.73  thf(178,axiom,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:(TA > int),C:(binary1291135688e_Tree @ TA),D:TA]: (((A = (binary1746293266le_Tip @ TA)) => ((binary213313527le_wrm @ TA @ B @ (binary210054475elle_T @ TA @ C @ D @ A)) = C)) & ((A != (binary1746293266le_Tip @ TA)) => ((binary213313527le_wrm @ TA @ B @ (binary210054475elle_T @ TA @ C @ D @ A)) = (binary210054475elle_T @ TA @ C @ D @ (binary213313527le_wrm @ TA @ B @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_wrm_Osimps)).
% 47.90/26.73  thf(884,plain,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:(TA > int),C:(binary1291135688e_Tree @ TA),D:TA]: (((A = (binary1746293266le_Tip @ TA)) => ((binary213313527le_wrm @ TA @ (B) @ (binary210054475elle_T @ TA @ C @ D @ A)) = C)) & ((~ (A = (binary1746293266le_Tip @ TA))) => ((binary213313527le_wrm @ TA @ (B) @ (binary210054475elle_T @ TA @ C @ D @ A)) = (binary210054475elle_T @ TA @ C @ D @ (binary213313527le_wrm @ TA @ (B) @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 47.90/26.73  thf(243,axiom,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_empty__iff)).
% 47.90/26.73  thf(1082,plain,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[243])).
% 47.90/26.73  thf(115,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((A = B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_ord__eq__le__trans)).
% 47.90/26.73  thf(637,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((A = B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 47.90/26.73  thf(219,axiom,((! [TA: $tType]: ((condit1656338222tinuum @ TA) => (! [A:TA]: ? [B:TA]: ((ord_less @ TA @ A @ B) | (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_191_ex__gt__or__lt)).
% 47.90/26.73  thf(1016,plain,((! [TA: $tType]: ((condit1656338222tinuum @ TA) => (! [A:TA]: ? [B:TA]: ((ord_less @ TA @ A @ B) | (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 47.90/26.73  thf(126,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((A = B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_ord__eq__less__trans)).
% 47.90/26.73  thf(679,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((A = B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 47.90/26.73  thf(89,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((A != B) => (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_linorder__cases)).
% 47.90/26.73  thf(547,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((~ (A = B)) => (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 47.90/26.73  thf(132,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ A) => (ord_less_eq @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_dual__order_Otrans)).
% 47.90/26.73  thf(706,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ A) => (ord_less_eq @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 47.90/26.73  thf(213,axiom,((! [TA: $tType]: ((ord_less_eq @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: ((ord_less @ (set @ TA) @ A @ B) | (A = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_subset__iff__psubset__eq)).
% 47.90/26.73  thf(985,plain,((! [TA: $tType]: ((ord_less_eq @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: ((ord_less @ (set @ TA) @ A @ B) | (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 47.90/26.73  thf(142,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_34_subsetI)).
% 47.90/26.73  thf(738,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)],[142])).
% 47.90/26.73  thf(232,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (~ (ord_less_eq @ TA @ C @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_170_pinf_I6_J)).
% 47.90/26.73  thf(1050,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (~ (ord_less_eq @ TA @ C @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 47.90/26.73  thf(138,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((A = B) => (ord_less_eq @ (set @ TA) @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_117_equalityD2)).
% 47.90/26.73  thf(721,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((A = B) => (ord_less_eq @ (set @ TA) @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 47.90/26.73  thf(30,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_less__asym)).
% 47.90/26.73  thf(371,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 47.90/26.73  thf(264,axiom,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:(TA > int)]: (((A != (binary1746293266le_Tip @ TA)) & (binary1610619414edTree @ TA @ B @ A)) => (member @ TA @ (binary576689334lle_rm @ TA @ B @ A) @ (binary1653327646_setOf @ TA @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_rm__set)).
% 47.90/26.73  thf(1131,plain,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:(TA > int)]: ((~ (A = (binary1746293266le_Tip @ TA)) & (binary1610619414edTree @ TA @ (B) @ A)) => (member @ TA @ (binary576689334lle_rm @ TA @ (B) @ A) @ (binary1653327646_setOf @ TA @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[264])).
% 47.90/26.73  thf(119,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less_eq @ TB @ A @ (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less_eq @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_order__subst1)).
% 47.90/26.73  thf(654,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less_eq @ TB @ A @ (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less_eq @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 47.90/26.73  thf(212,axiom,((no_bot @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Ono__bot)).
% 47.90/26.73  thf(984,plain,((no_bot @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 47.90/26.73  thf(186,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_152_dual__order_Ostrict__trans1)).
% 47.90/26.73  thf(911,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 47.90/26.73  thf(152,axiom,((! [TA: $tType]: ((ord_less_eq @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (ord_less_eq @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_189_less__eq__set__def)).
% 47.90/26.73  thf(792,plain,((! [TA: $tType]: ((ord_less_eq @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (ord_less_eq @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 47.90/26.73  thf(1,conjecture,((binary1610619414edTree @ a @ h @ t1)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 47.90/26.73  thf(2,negated_conjecture,((~ (binary1610619414edTree @ a @ h @ t1))),inference(neg_conjecture,[status(cth)],[1])).
% 47.90/26.73  thf(266,plain,((~ (binary1610619414edTree @ a @ (h) @ t1))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 47.90/26.73  thf(25,axiom,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: ((product_case_prod @ TA @ TB @ (TC > TD)) = (^ [A:(TA > (TB > (TC > TD))),B:(product_prod @ TA @ TB),C:TC]: (product_case_prod @ TA @ TB @ TD @ (^ [D:TA,E:TB]: (A @ D @ E @ C)) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_224_case__prod__app)).
% 47.90/26.73  thf(360,plain,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: ((product_case_prod @ TA @ TB @ (TC > TD)) = (^ [A:(TA > (TB > (TC > TD))),B:(product_prod @ TA @ TB),C:TC]: (product_case_prod @ TA @ TB @ TD @ (^ [D:TA,E:TB]: (A @ D @ E @ C)) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 47.90/26.73  thf(80,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (C != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_minf_I4_J)).
% 47.90/26.73  thf(508,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (C = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 47.90/26.73  thf(16,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (C != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_196_pinf_I4_J)).
% 47.90/26.73  thf(311,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (~ (C = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 47.90/26.73  thf(234,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) | (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_144_le__less__linear)).
% 47.90/26.73  thf(1054,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) | (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[234])).
% 47.90/26.73  thf(93,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((A = (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_ord__eq__less__subst)).
% 47.90/26.73  thf(558,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((A = (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 47.90/26.73  thf(223,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (A != B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_129_less__le)).
% 47.90/26.73  thf(1026,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 47.90/26.73  thf(83,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((A = B) | ~ (ord_less_eq @ TA @ A @ B) | ~ (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_verit__la__disequality)).
% 47.90/26.73  thf(530,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((A = B) | ~ (ord_less_eq @ TA @ A @ B) | ~ (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 47.90/26.73  thf(245,axiom,((condit1037483654norder @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Conditionally__Complete__Lattices_Oconditionally__complete__linorder)).
% 47.90/26.73  thf(1086,plain,((condit1037483654norder @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[245])).
% 47.90/26.73  thf(196,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less @ TB @ A @ (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_132_order__less__le__subst1)).
% 47.90/26.73  thf(938,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less @ TB @ A @ (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 47.90/26.73  thf(184,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_33_subset__antisym)).
% 47.90/26.73  thf(906,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)],[184])).
% 47.90/26.73  thf(109,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((A != B) = ((ord_less @ TA @ A @ B) | (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_neq__iff)).
% 47.90/26.73  thf(618,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (A = B)) = ((ord_less @ TA @ A @ B) | (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 47.90/26.73  thf(50,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_order_Otrans)).
% 47.90/26.73  thf(430,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 47.90/26.73  thf(252,axiom,(((((binary1746293266le_Tip @ a) != (binary1746293266le_Tip @ a)) & (binary1610619414edTree @ a @ h @ (binary1746293266le_Tip @ a))) => (binary1610619414edTree @ a @ h @ (binary213313527le_wrm @ a @ h @ (binary1746293266le_Tip @ a))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13__092_060open_062Tip_A_092_060noteq_062_ATip_A_092_060and_062_AsortedTree_Ah_ATip_A_092_060longrightarrow_062_AsortedTree_Ah_A_Iwrm_Ah_ATip_J_092_060close_062)).
% 47.90/26.73  thf(1103,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[252])).
% 47.90/26.73  thf(6,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((B = C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_ord__less__eq__trans)).
% 47.90/26.73  thf(279,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((B = C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 47.90/26.73  thf(96,axiom,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_bot__apply)).
% 47.90/26.73  thf(573,plain,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 47.90/26.73  thf(32,axiom,((! [TA: $tType,TB: $tType]: (! [A:(product_prod @ TA @ TB)]: (product_case_prod @ TA @ TB @ $o @ (^ [B:TA,C:TB]: (($true))) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_254_prod_Odisc__eq__case)).
% 47.90/26.73  thf(375,plain,((! [TA: $tType,TB: $tType]: (! [A:(product_prod @ TA @ TB)]: (product_case_prod @ TA @ TB @ $o @ (^ [B:TA,C:TB]: (($true))) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 47.90/26.73  thf(183,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ~ (ord_less @ (set @ TA) @ A @ (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_181_not__psubset__empty)).
% 47.90/26.73  thf(904,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ~ (ord_less @ (set @ TA) @ A @ (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 47.90/26.73  thf(48,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_105_order_Ostrict__implies__not__eq)).
% 47.90/26.73  thf(423,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 47.90/26.73  thf(217,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less @ (set @ TA) @ A @ B) => (~ ((ord_less_eq @ (set @ TA) @ A @ B) => (ord_less_eq @ (set @ TA) @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_psubsetE)).
% 47.90/26.73  thf(1007,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less @ (set @ TA) @ A @ B) => (~ ((ord_less_eq @ (set @ TA) @ A @ B) => (ord_less_eq @ (set @ TA) @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[217])).
% 47.90/26.73  thf(39,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (ord_less @ TA @ C @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_204_minf_I5_J)).
% 47.90/26.73  thf(402,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (ord_less @ TA @ C @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 47.90/26.73  thf(262,axiom,((! [TA: $tType]: (! [A:(TA > int),B:(binary1291135688e_Tree @ TA),C:TA]: ((binary1610619414edTree @ TA @ A @ B) => ((binary827270440e_memb @ TA @ A @ C @ B) = (member @ TA @ C @ (binary1653327646_setOf @ TA @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_memb__spec)).
% 47.90/26.73  thf(1125,plain,((! [TA: $tType]: (! [A:(TA > int),B:(binary1291135688e_Tree @ TA),C:TA]: ((binary1610619414edTree @ TA @ (A) @ B) => ((binary827270440e_memb @ TA @ (A) @ C @ B) = (member @ TA @ C @ (binary1653327646_setOf @ TA @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[262])).
% 47.90/26.73  thf(8,axiom,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_bot__fun__def)).
% 47.90/26.73  thf(286,plain,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 47.90/26.73  thf(44,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_35_empty__Collect__eq)).
% 47.90/26.73  thf(413,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)],[44])).
% 47.90/26.73  thf(116,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)).
% 47.90/26.73  thf(641,plain,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ (B))) = (B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 47.90/26.73  thf(35,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_order__less__subst2)).
% 47.90/26.73  thf(391,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 47.90/26.73  thf(75,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_verit__comp__simplify1_I1_J)).
% 47.90/26.73  thf(498,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 47.90/26.73  thf(255,axiom,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:(TA > int)]: (((A != (binary1746293266le_Tip @ TA)) & (binary1610619414edTree @ TA @ B @ A)) => (ord_less_eq @ (set @ TA) @ (binary1653327646_setOf @ TA @ (binary213313527le_wrm @ TA @ B @ A)) @ (binary1653327646_setOf @ TA @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_wrm__set1)).
% 47.90/26.73  thf(1107,plain,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:(TA > int)]: ((~ (A = (binary1746293266le_Tip @ TA)) & (binary1610619414edTree @ TA @ (B) @ A)) => (ord_less_eq @ (set @ TA) @ (binary1653327646_setOf @ TA @ (binary213313527le_wrm @ TA @ (B) @ A)) @ (binary1653327646_setOf @ TA @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[255])).
% 47.90/26.73  thf(131,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_dual__order_Ostrict__trans)).
% 47.90/26.73  thf(704,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 47.90/26.73  thf(199,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((ord_less_eq @ (set @ TA) @ (collect @ TA @ A) @ (collect @ TA @ B)) = (! [C:TA]: ((A @ C) => (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_123_Collect__mono__iff)).
% 47.90/26.73  thf(947,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((ord_less_eq @ (set @ TA) @ (collect @ TA @ (A)) @ (collect @ TA @ (B))) = (! [C:TA]: ((A @ C) => (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 47.90/26.73  thf(56,axiom,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oorder)).
% 47.90/26.73  thf(445,plain,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 47.90/26.73  thf(195,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_less__le__trans)).
% 47.90/26.73  thf(936,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 47.90/26.73  thf(210,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: (ord_less_eq @ (set @ TA) @ A @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_subset__refl)).
% 47.90/26.73  thf(979,plain,((! [TA: $tType]: (! [A:(set @ TA)]: (ord_less_eq @ (set @ TA) @ A @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 47.90/26.73  thf(182,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((A = B) => (ord_less_eq @ (set @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_116_equalityD1)).
% 47.90/26.73  thf(900,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((A = B) => (ord_less_eq @ (set @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 47.90/26.73  thf(33,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > $o),B:(TA > $o),C:(TA > $o),D:(TA > $o)]: ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => ((A @ F) = (B @ F)))) => ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => ((C @ F) = (D @ F)))) => (? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => (((A @ F) & (C @ F)) = ((B @ F) & (D @ F))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_200_minf_I1_J)).
% 47.90/26.73  thf(377,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > $o),B:(TA > $o),C:(TA > $o),D:(TA > $o)]: ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => ((A @ F) = (B @ F)))) => ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => ((C @ F) = (D @ F)))) => (? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => (((A @ F) & (C @ F)) = ((B @ F) & (D @ F))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 47.90/26.73  thf(58,axiom,((bot @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Obot_14)).
% 47.90/26.73  thf(451,plain,((bot @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 47.90/26.73  thf(12,axiom,((linorder @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Olinorder)).
% 47.90/26.73  thf(303,plain,((linorder @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 47.90/26.73  thf(218,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o),D:(TA > $o)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((! [E:TA]: ((member @ TA @ E @ A) => ((C @ E) => (D @ E)))) => (ord_less_eq @ (set @ TA) @ (collect @ TA @ (^ [E:TA]: ((member @ TA @ E @ A) & (C @ E)))) @ (collect @ TA @ (^ [E:TA]: ((member @ TA @ E @ B) & (D @ E)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_220_subset__CollectI)).
% 47.90/26.73  thf(1011,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o),D:(TA > $o)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((! [E:TA]: ((member @ TA @ E @ A) => ((C @ E) => (D @ E)))) => (ord_less_eq @ (set @ TA) @ (collect @ TA @ (^ [E:TA]: ((member @ TA @ E @ A) & (C @ E)))) @ (collect @ TA @ (^ [E:TA]: ((member @ TA @ E @ B) & (D @ E)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 47.90/26.73  thf(46,axiom,((! [TA: $tType]: (order @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Oorder_6)).
% 47.90/26.73  thf(419,plain,((! [TA: $tType]: (order @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 47.90/26.73  thf(177,axiom,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA]: ((! [C:TA]: ((ord_less @ TA @ A @ C) => (ord_less_eq @ TA @ B @ C))) => (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_142_dense__ge)).
% 47.90/26.73  thf(880,plain,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA]: ((! [C:TA]: ((ord_less @ TA @ A @ C) => (ord_less_eq @ TA @ B @ C))) => (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 47.90/26.73  thf(229,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (ord_less_eq @ TA @ C @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_168_minf_I6_J)).
% 47.90/26.73  thf(1043,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (ord_less_eq @ TA @ C @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 47.90/26.73  thf(66,axiom,((ord @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oord_13)).
% 47.90/26.73  thf(477,plain,((ord @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 47.90/26.73  thf(34,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => ((ord_less_eq @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less_eq @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_order__subst2)).
% 47.90/26.73  thf(387,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => ((ord_less_eq @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less_eq @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 47.90/26.73  thf(73,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:$o]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ A) => (C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_less__imp__triv)).
% 47.90/26.73  thf(494,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:$o]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ A) => (C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 47.90/26.73  thf(113,axiom,((! [TA: $tType]: (! [A:(set @ (product_prod @ TA @ TA)),B:(set @ (product_prod @ TA @ TA))]: ((A = (bot_bot @ (set @ (product_prod @ TA @ TA)))) => (ord_less_eq @ (set @ (product_prod @ TA @ TA)) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_251_less__by__empty)).
% 47.90/26.73  thf(631,plain,((! [TA: $tType]: (! [A:(set @ (product_prod @ TA @ TA)),B:(set @ (product_prod @ TA @ TA))]: ((A = (bot_bot @ (set @ (product_prod @ TA @ TA)))) => (ord_less_eq @ (set @ (product_prod @ TA @ TA)) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 47.90/26.73  thf(28,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_order_Ostrict__trans)).
% 47.90/26.73  thf(367,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 47.90/26.73  thf(159,axiom,((! [TA: $tType,TB: $tType]: (! [A:(set @ (product_prod @ TA @ TB)),B:(set @ (product_prod @ TA @ TB))]: ((! [C:TA,D:TB]: ((member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ A) => (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ B))) => (ord_less_eq @ (set @ (product_prod @ TA @ TB)) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_227_subrelI)).
% 47.90/26.73  thf(816,plain,((! [TA: $tType,TB: $tType]: (! [A:(set @ (product_prod @ TA @ TB)),B:(set @ (product_prod @ TA @ TB))]: ((! [C:TA,D:TB]: ((member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ A) => (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ B))) => (ord_less_eq @ (set @ (product_prod @ TA @ TB)) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 47.90/26.73  thf(18,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA]: (A @ D @ D)) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_linorder__less__wlog)).
% 47.90/26.73  thf(323,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA]: (A @ D @ D)) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 47.90/26.73  thf(102,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_198_pinf_I7_J)).
% 47.90/26.73  thf(594,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 47.90/26.73  thf(110,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)).
% 47.90/26.73  thf(621,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 47.90/26.73  thf(69,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)).
% 47.90/26.73  thf(483,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)],[69])).
% 47.90/26.73  thf(204,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > $o),C:(TA > $o)]: ((ord_less_eq @ (set @ TA) @ A @ (collect @ TA @ (^ [D:TA]: ((B @ D) & (C @ D))))) = ((ord_less_eq @ (set @ TA) @ A @ (collect @ TA @ B)) & (ord_less_eq @ (set @ TA) @ A @ (collect @ TA @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_221_conj__subset__def)).
% 47.90/26.73  thf(964,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > $o),C:(TA > $o)]: ((ord_less_eq @ (set @ TA) @ A @ (collect @ TA @ (^ [D:TA]: ((B @ D) & (C @ D))))) = ((ord_less_eq @ (set @ TA) @ A @ (collect @ TA @ (B))) & (ord_less_eq @ (set @ TA) @ A @ (collect @ TA @ (C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 47.90/26.73  thf(123,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(product_prod @ TA @ TB),B:TC,C:(TA > (TB > (set @ TC)))]: ((! [D:TA,E:TB]: ((A = (product_Pair @ TA @ TB @ D @ E)) => (member @ TC @ B @ (C @ D @ E)))) => (member @ TC @ B @ (product_case_prod @ TA @ TB @ (set @ TC) @ C @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_mem__case__prodI2)).
% 47.90/26.73  thf(668,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(product_prod @ TA @ TB),B:TC,C:(TA > (TB > (set @ TC)))]: ((! [D:TA,E:TB]: ((A = (product_Pair @ TA @ TB @ D @ E)) => (member @ TC @ B @ (C @ D @ E)))) => (member @ TC @ B @ (product_case_prod @ TA @ TB @ (set @ TC) @ (C) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 47.90/26.73  thf(60,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_order__class_Oorder_Oantisym)).
% 47.90/26.73  thf(462,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 47.90/26.73  thf(224,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B))) = (ord_less_eq @ (set @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_218_pred__subset__eq)).
% 47.90/26.73  thf(1029,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B))) = (ord_less_eq @ (set @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 47.90/26.73  thf(180,axiom,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:(TA > int)]: ((A != (binary1746293266le_Tip @ TA)) => ((binary1271298290_wrmrm @ TA @ B @ A) = (product_Pair @ (binary1291135688e_Tree @ TA) @ TA @ (binary213313527le_wrm @ TA @ B @ A) @ (binary576689334lle_rm @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_223_wrmrm__decomp)).
% 47.90/26.73  thf(895,plain,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:(TA > int)]: ((~ (A = (binary1746293266le_Tip @ TA))) => ((binary1271298290_wrmrm @ TA @ (B) @ A) = (product_Pair @ (binary1291135688e_Tree @ TA) @ TA @ (binary213313527le_wrm @ TA @ (B) @ A) @ (binary576689334lle_rm @ TA @ (B) @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 47.90/26.73  thf(37,axiom,((ord @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Oord_3)).
% 47.90/26.73  thf(399,plain,((ord @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 47.90/26.73  thf(202,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_167_minf_I8_J)).
% 47.90/26.73  thf(959,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 47.90/26.73  thf(173,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) = (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_171_verit__comp__simplify1_I3_J)).
% 47.90/26.73  thf(868,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) = (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 47.90/26.73  thf(257,axiom,(((binary213313527le_wrm @ a @ h @ (binary210054475elle_T @ a @ t1 @ x @ t2)) = (binary210054475elle_T @ a @ t1 @ x @ (binary213313527le_wrm @ a @ h @ t2)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_res)).
% 47.90/26.73  thf(1113,plain,(((binary213313527le_wrm @ a @ (h) @ (binary210054475elle_T @ a @ t1 @ x @ t2)) = (binary210054475elle_T @ a @ t1 @ x @ (binary213313527le_wrm @ a @ (h) @ t2)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[257])).
% 47.90/26.73  thf(10,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_order__trans)).
% 47.90/26.73  thf(299,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 47.90/26.73  thf(3,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => (((C @ B) = D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_ord__less__eq__subst)).
% 47.90/26.73  thf(267,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => (((C @ B) = D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 47.90/26.73  thf(79,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B) | (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_less__linear)).
% 47.90/26.73  thf(505,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B) | (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 47.90/26.73  thf(120,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_dual__order_Orefl)).
% 47.90/26.73  thf(658,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 47.90/26.73  thf(226,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((~ (ord_less @ TA @ A @ B)) = (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_antisym__conv2)).
% 47.90/26.73  thf(1034,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((~ (ord_less @ TA @ A @ B)) = (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 47.90/26.73  thf(71,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB),C:TA]: ((ord_less_eq @ (TA > TB) @ A @ B) => (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_43_le__funE)).
% 47.90/26.73  thf(490,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB),C:TA]: ((ord_less_eq @ (TA > TB) @ (A) @ (B)) => (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 47.90/26.73  thf(153,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_126_leD)).
% 47.90/26.73  thf(795,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 47.90/26.73  thf(265,axiom,((! [TA: $tType]: (! [A:(TA > int),B:(binary1291135688e_Tree @ TA),C:TA,D:(binary1291135688e_Tree @ TA)]: ((binary1610619414edTree @ TA @ A @ (binary210054475elle_T @ TA @ B @ C @ D)) = ((binary1610619414edTree @ TA @ A @ B) & ! [E:TA]: ((member @ TA @ E @ (binary1653327646_setOf @ TA @ B)) => (ord_less @ int @ (A @ E) @ (A @ C))) & ! [E:TA]: ((member @ TA @ E @ (binary1653327646_setOf @ TA @ D)) => (ord_less @ int @ (A @ C) @ (A @ E))) & (binary1610619414edTree @ TA @ A @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_sortedTree_Osimps_I2_J)).
% 47.90/26.73  thf(1134,plain,((! [TA: $tType]: (! [A:(TA > int),B:(binary1291135688e_Tree @ TA),C:TA,D:(binary1291135688e_Tree @ TA)]: ((binary1610619414edTree @ TA @ (A) @ (binary210054475elle_T @ TA @ B @ C @ D)) = ((binary1610619414edTree @ TA @ (A) @ B) & ! [E:TA]: ((member @ TA @ E @ (binary1653327646_setOf @ TA @ B)) => (ord_less @ int @ (A @ E) @ (A @ C))) & ! [E:TA]: ((member @ TA @ E @ (binary1653327646_setOf @ TA @ D)) => (ord_less @ int @ (A @ C) @ (A @ E))) & (binary1610619414edTree @ TA @ (A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[265])).
% 47.90/26.73  thf(146,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > $o)]: (ord_less_eq @ (set @ TA) @ (collect @ TA @ (^ [C:TA]: ((member @ TA @ C @ A) & (B @ C)))) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_125_Collect__subset)).
% 47.90/26.73  thf(749,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > $o)]: (ord_less_eq @ (set @ TA) @ (collect @ TA @ (^ [C:TA]: ((member @ TA @ C @ A) & (B @ C)))) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 47.90/26.73  thf(220,axiom,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_lt__ex)).
% 47.90/26.73  thf(1018,plain,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 47.90/26.73  thf(91,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:((product_prod @ TA @ TB) > TC)]: ((product_case_prod @ TA @ TB @ TC @ (^ [B:TA,C:TB]: (A @ (product_Pair @ TA @ TB @ B @ C)))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_249_case__prod__eta)).
% 47.90/26.73  thf(553,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:((product_prod @ TA @ TB) > TC)]: ((product_case_prod @ TA @ TB @ TC @ (^ [B:TA,C:TB]: (A @ (product_Pair @ TA @ TB @ B @ C)))) = (A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 47.90/26.73  thf(163,axiom,((! [TA: $tType]: ((ord_less_eq @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: ! [C:TA]: ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_115_subset__eq)).
% 47.90/26.73  thf(836,plain,((! [TA: $tType]: ((ord_less_eq @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: ! [C:TA]: ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 47.90/26.73  thf(134,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_36_Collect__empty__eq)).
% 47.90/26.73  thf(712,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)],[134])).
% 47.90/26.73  thf(98,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_order__refl)).
% 47.90/26.73  thf(580,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 47.90/26.73  thf(239,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_135_not__less)).
% 47.90/26.73  thf(1070,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 47.90/26.73  thf(207,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => ((ord_less @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB)]: ((ord_less_eq @ (TA > TB) @ A @ B) & ~ (ord_less_eq @ (TA > TB) @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_175_less__fun__def)).
% 47.90/26.73  thf(971,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => ((ord_less @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB)]: ((ord_less_eq @ (TA > TB) @ A @ B) & ~ (ord_less_eq @ (TA > TB) @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 47.90/26.73  thf(42,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_less__not__sym)).
% 47.90/26.73  thf(409,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 47.90/26.73  thf(15,axiom,((preorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Opreorder_10)).
% 47.90/26.73  thf(310,plain,((preorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 47.90/26.73  thf(124,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TB > TC),B:TB,C:((binary1291135688e_Tree @ TA) > (TA > ((binary1291135688e_Tree @ TA) > TB))),D:(binary1291135688e_Tree @ TA)]: ((A @ (binary536355927e_Tree @ TB @ TA @ B @ C @ D)) = (binary536355927e_Tree @ TC @ TA @ (A @ B) @ (^ [E:(binary1291135688e_Tree @ TA),F:TA,G:(binary1291135688e_Tree @ TA)]: (A @ (C @ E @ F @ G))) @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_Tree_Ocase__distrib)).
% 47.90/26.73  thf(673,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TB > TC),B:TB,C:((binary1291135688e_Tree @ TA) > (TA > ((binary1291135688e_Tree @ TA) > TB))),D:(binary1291135688e_Tree @ TA)]: ((A @ (binary536355927e_Tree @ TB @ TA @ B @ (C) @ D)) = (binary536355927e_Tree @ TC @ TA @ (A @ B) @ (^ [E:(binary1291135688e_Tree @ TA),F:TA,G:(binary1291135688e_Tree @ TA)]: (A @ (C @ E @ F @ G))) @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 47.90/26.73  thf(100,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((A = (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less_eq @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_ord__eq__le__subst)).
% 47.90/26.73  thf(585,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((A = (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less_eq @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 47.90/26.73  thf(136,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (~ (ord_less @ TA @ C @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_197_pinf_I5_J)).
% 47.90/26.73  thf(717,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (~ (ord_less @ TA @ C @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 47.90/26.73  thf(77,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_205_minf_I7_J)).
% 47.90/26.73  thf(502,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 47.90/26.73  thf(97,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TA > $o)),B:(TB > (TA > $o)),C:$o,D:TB,E:TA]: (((ord_less_eq @ (TB > (TA > $o)) @ A @ B) & (C)) => ((C) & ((A @ D @ E) => (B @ D @ E))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_239_predicate2D__conj)).
% 47.90/26.73  thf(576,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TA > $o)),B:(TB > (TA > $o)),C:$o,D:TB,E:TA]: (((ord_less_eq @ (TB > (TA > $o)) @ (A) @ (B)) & (C)) => ((C) & ((A @ D @ E) => (B @ D @ E))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 47.90/26.73  thf(88,axiom,((! [TA: $tType,TB: $tType]: ((inv_image @ TA @ TB) = (^ [A:(set @ (product_prod @ TA @ TA)),B:(TB > TA)]: (collect @ (product_prod @ TB @ TB) @ (product_case_prod @ TB @ TB @ $o @ (^ [C:TB,D:TB]: (member @ (product_prod @ TA @ TA) @ (product_Pair @ TA @ TA @ (B @ C) @ (B @ D)) @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_255_inv__image__def)).
% 47.90/26.73  thf(544,plain,((! [TA: $tType,TB: $tType]: ((inv_image @ TA @ TB) = (^ [A:(set @ (product_prod @ TA @ TA)),B:(TB > TA)]: (collect @ (product_prod @ TB @ TB) @ (product_case_prod @ TB @ TB @ $o @ (^ [C:TB,D:TB]: (member @ (product_prod @ TA @ TA) @ (product_Pair @ TA @ TA @ (B @ C) @ (B @ D)) @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 47.90/26.73  thf(144,axiom,((! [TA: $tType]: (! [A:(TA > int),B:TA]: ((binary1830089824insert @ TA @ A @ B @ (binary1746293266le_Tip @ TA)) = (binary210054475elle_T @ TA @ (binary1746293266le_Tip @ TA) @ B @ (binary1746293266le_Tip @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_binsert_Osimps_I1_J)).
% 47.90/26.73  thf(744,plain,((! [TA: $tType]: (! [A:(TA > int),B:TA]: ((binary1830089824insert @ TA @ (A) @ B @ (binary1746293266le_Tip @ TA)) = (binary210054475elle_T @ TA @ (binary1746293266le_Tip @ TA) @ B @ (binary1746293266le_Tip @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 47.90/26.73  thf(130,axiom,((order @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Oorder_2)).
% 47.90/26.73  thf(703,plain,((order @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 47.90/26.73  thf(222,axiom,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA)]: ((A != (binary1746293266le_Tip @ TA)) => (~ (! [B:(binary1291135688e_Tree @ TA),C:TA,D:(binary1291135688e_Tree @ TA)]: (A != (binary210054475elle_T @ TA @ B @ C @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_Tree_Oexhaust)).
% 47.90/26.73  thf(1023,plain,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA)]: ((~ (A = (binary1746293266le_Tip @ TA))) => (~ (! [B:(binary1291135688e_Tree @ TA),C:TA,D:(binary1291135688e_Tree @ TA)]: ~ (A = (binary210054475elle_T @ TA @ B @ C @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 47.90/26.73  thf(233,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) => (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_147_not__le__imp__less)).
% 47.90/26.73  thf(1052,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) => (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 47.90/26.73  thf(249,axiom,((! [TA: $tType]: ((ord_less @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) & (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_psubset__eq)).
% 47.90/26.73  thf(1094,plain,((! [TA: $tType]: ((ord_less @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) & ~ (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[249])).
% 47.90/26.73  thf(107,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) = (B = A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_antisym__conv)).
% 47.90/26.73  thf(612,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) = (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 47.90/26.73  thf(215,axiom,((! [TA: $tType]: (! [A:((binary1291135688e_Tree @ TA) > $o),B:(binary1291135688e_Tree @ TA)]: ((A @ (binary1746293266le_Tip @ TA)) => ((! [C:(binary1291135688e_Tree @ TA),D:TA,E:(binary1291135688e_Tree @ TA)]: ((A @ C) => ((A @ E) => (A @ (binary210054475elle_T @ TA @ C @ D @ E))))) => (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_Tree_Oinduct)).
% 47.90/26.73  thf(991,plain,((! [TA: $tType]: (! [A:((binary1291135688e_Tree @ TA) > $o),B:(binary1291135688e_Tree @ TA)]: ((A @ (binary1746293266le_Tip @ TA)) => ((! [C:(binary1291135688e_Tree @ TA),D:TA,E:(binary1291135688e_Tree @ TA)]: ((A @ C) => ((A @ E) => (A @ (binary210054475elle_T @ TA @ C @ D @ E))))) => (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 47.90/26.73  thf(61,axiom,((! [TA: $tType,TB: $tType]: (! [A:(product_prod @ TA @ TB)]: ((product_case_prod @ TA @ TB @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB) @ A) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_225_case__prod__Pair__iden)).
% 47.90/26.73  thf(465,plain,((! [TA: $tType,TB: $tType]: (! [A:(product_prod @ TA @ TB)]: ((product_case_prod @ TA @ TB @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB) @ A) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 47.90/26.73  thf(244,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_less__imp__le)).
% 47.90/26.73  thf(1084,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[244])).
% 47.90/26.73  thf(194,axiom,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((! [D:TA]: ((ord_less @ TA @ A @ D) => ((ord_less @ TA @ D @ B) => (ord_less_eq @ TA @ C @ D)))) => (ord_less_eq @ TA @ C @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_154_dense__ge__bounded)).
% 47.90/26.73  thf(931,plain,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((! [D:TA]: ((ord_less @ TA @ A @ D) => ((ord_less @ TA @ D @ B) => (ord_less_eq @ TA @ C @ D)))) => (ord_less_eq @ TA @ C @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 47.90/26.73  thf(209,axiom,((! [TA: $tType]: (((=) @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) & (ord_less_eq @ (set @ TA) @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_122_set__eq__subset)).
% 47.90/26.73  thf(976,plain,((! [TA: $tType]: (((=) @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) & (ord_less_eq @ (set @ TA) @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 47.90/26.73  thf(179,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less_eq @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_order__less__le__subst2)).
% 47.90/26.73  thf(891,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less_eq @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 47.90/26.73  thf(166,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_111_ex__in__conv)).
% 47.90/26.73  thf(844,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)],[166])).
% 47.90/26.73  thf(26,axiom,((! [TA: $tType]: (ord @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Oord_7)).
% 47.90/26.73  thf(363,plain,((! [TA: $tType]: (ord @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 47.90/26.73  thf(92,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) | (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_linear)).
% 47.90/26.73  thf(556,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) | (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 47.90/26.73  thf(129,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_106_dual__order_Ostrict__implies__not__eq)).
% 47.90/26.73  thf(699,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 47.90/26.73  thf(203,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (B = A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_157_dual__order_Oorder__iff__strict)).
% 47.90/26.73  thf(961,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 47.90/26.73  thf(13,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_less__imp__not__eq)).
% 47.90/26.73  thf(304,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 47.90/26.73  thf(237,axiom,((! [TA: $tType,TB: $tType]: (! [A:TB,B:((binary1291135688e_Tree @ TA) > (TA > ((binary1291135688e_Tree @ TA) > TB))),C:(binary1291135688e_Tree @ TA),D:TA,E:(binary1291135688e_Tree @ TA)]: ((binary536355927e_Tree @ TB @ TA @ A @ B @ (binary210054475elle_T @ TA @ C @ D @ E)) = (B @ C @ D @ E))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_Tree_Osimps_I5_J)).
% 47.90/26.73  thf(1062,plain,((! [TA: $tType,TB: $tType]: (! [A:TB,B:((binary1291135688e_Tree @ TA) > (TA > ((binary1291135688e_Tree @ TA) > TB))),C:(binary1291135688e_Tree @ TA),D:TA,E:(binary1291135688e_Tree @ TA)]: ((binary536355927e_Tree @ TB @ TA @ A @ (B) @ (binary210054475elle_T @ TA @ C @ D @ E)) = (B @ C @ D @ E))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 47.90/26.73  thf(251,axiom,((! [TA: $tType]: (! [A:(TA > int)]: (binary1610619414edTree @ TA @ A @ (binary1746293266le_Tip @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_sortedTree_Osimps_I1_J)).
% 47.90/26.73  thf(1101,plain,((! [TA: $tType]: (! [A:(TA > int)]: (binary1610619414edTree @ TA @ (A) @ (binary1746293266le_Tip @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[251])).
% 47.90/26.73  thf(118,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TA > $o)),B:TB,C:TA,D:(TB > (TA > $o))]: ((A @ B @ C) => ((ord_less_eq @ (TB > (TA > $o)) @ A @ D) => (D @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_242_rev__predicate2D)).
% 47.90/26.73  thf(652,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TA > $o)),B:TB,C:TA,D:(TB > (TA > $o))]: ((A @ B @ C) => ((ord_less_eq @ (TB > (TA > $o)) @ (A) @ (D)) => (D @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 47.90/26.73  thf(141,axiom,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:(TA > int),C:(binary1291135688e_Tree @ TA),D:TA]: (((A = (binary1746293266le_Tip @ TA)) => ((binary576689334lle_rm @ TA @ B @ (binary210054475elle_T @ TA @ C @ D @ A)) = D)) & ((A != (binary1746293266le_Tip @ TA)) => ((binary576689334lle_rm @ TA @ B @ (binary210054475elle_T @ TA @ C @ D @ A)) = (binary576689334lle_rm @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_rm_Osimps)).
% 47.90/26.73  thf(731,plain,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:(TA > int),C:(binary1291135688e_Tree @ TA),D:TA]: (((A = (binary1746293266le_Tip @ TA)) => ((binary576689334lle_rm @ TA @ (B) @ (binary210054475elle_T @ TA @ C @ D @ A)) = D)) & ((~ (A = (binary1746293266le_Tip @ TA))) => ((binary576689334lle_rm @ TA @ (B) @ (binary210054475elle_T @ TA @ C @ D @ A)) = (binary576689334lle_rm @ TA @ (B) @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 47.90/26.73  thf(230,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less @ (set @ TA) @ A @ B) => (ord_less_eq @ (set @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_psubset__imp__subset)).
% 47.90/26.73  thf(1045,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less @ (set @ TA) @ A @ B) => (ord_less_eq @ (set @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 47.90/26.73  thf(241,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: ((ord_less @ (set @ TA) @ A @ B) => ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_217_psubsetD)).
% 47.90/26.73  thf(1077,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: ((ord_less @ (set @ TA) @ A @ B) => ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 47.90/26.73  thf(67,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((A @ B) => ((ord_less_eq @ (TA > $o) @ A @ C) => (C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_214_rev__predicate1D)).
% 47.90/26.73  thf(478,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((A @ B) => ((ord_less_eq @ (TA > $o) @ (A) @ (C)) => (C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 47.90/26.73  thf(57,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((B = C) => (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_64_ord__le__eq__trans)).
% 47.90/26.73  thf(447,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((B = C) => (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 47.90/26.73  thf(17,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => (((C @ B) = D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less_eq @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_ord__le__eq__subst)).
% 47.90/26.73  thf(315,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => (((C @ B) = D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less_eq @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 47.90/26.73  thf(51,axiom,((! [TA: $tType,TB: $tType]: (! [A:(set @ (product_prod @ TA @ TB)),B:(set @ (product_prod @ TA @ TB))]: (((^ [C:TA,D:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ A)) = (^ [C:TA,D:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ B))) = (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_pred__equals__eq2)).
% 47.90/26.73  thf(432,plain,((! [TA: $tType,TB: $tType]: (! [A:(set @ (product_prod @ TA @ TB)),B:(set @ (product_prod @ TA @ TB))]: (((^ [C:TA,D:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ A)) = (^ [C:TA,D:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ B))) = (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 47.90/26.73  thf(205,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((ord_less @ (set @ TA) @ B @ C) => (ord_less @ (set @ TA) @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_183_subset__psubset__trans)).
% 47.90/26.73  thf(967,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((ord_less @ (set @ TA) @ B @ C) => (ord_less @ (set @ TA) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 47.90/26.73  thf(170,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((ord_less_eq @ TA @ A @ B) = (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_137_antisym__conv1)).
% 47.90/26.73  thf(854,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((ord_less_eq @ TA @ A @ B) = (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 47.90/26.73  thf(151,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: (ord_less_eq @ (set @ TA) @ (bot_bot @ (set @ TA)) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_empty__subsetI)).
% 47.90/26.73  thf(790,plain,((! [TA: $tType]: (! [A:(set @ TA)]: (ord_less_eq @ (set @ TA) @ (bot_bot @ (set @ TA)) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 47.90/26.73  thf(31,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_less__asym_H)).
% 47.90/26.73  thf(373,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 47.90/26.73  thf(200,axiom,((! [TA: $tType]: ((wellorder @ TA) => (! [A:(TA > $o),B:TA]: ((! [C:TA]: ((! [D:TA]: ((ord_less @ TA @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_less__induct)).
% 47.90/26.73  thf(950,plain,((! [TA: $tType]: ((wellorder @ TA) => (! [A:(TA > $o),B:TA]: ((! [C:TA]: ((! [D:TA]: ((ord_less @ TA @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 47.90/26.73  thf(250,axiom,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA]: ((! [C:TA]: ((ord_less @ TA @ C @ A) => (ord_less_eq @ TA @ C @ B))) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_143_dense__le)).
% 47.90/26.73  thf(1097,plain,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA]: ((! [C:TA]: ((ord_less @ TA @ C @ A) => (ord_less_eq @ TA @ C @ B))) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 47.90/26.73  thf(19,axiom,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (! [A:(TD > TC),B:(TA > (TB > TD)),C:(product_prod @ TA @ TB)]: ((A @ (product_case_prod @ TA @ TB @ TD @ B @ C)) = (product_case_prod @ TA @ TB @ TC @ (^ [D:TA,E:TB]: (A @ (B @ D @ E))) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_247_prod_Ocase__distrib)).
% 47.90/26.73  thf(341,plain,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (! [A:(TD > TC),B:(TA > (TB > TD)),C:(product_prod @ TA @ TB)]: ((A @ (product_case_prod @ TA @ TB @ TD @ (B) @ C)) = (product_case_prod @ TA @ TB @ TC @ (^ [D:TA,E:TB]: (A @ (B @ D @ E))) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 47.90/26.73  thf(24,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_order_Oasym)).
% 47.90/26.73  thf(358,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 47.90/26.73  thf(53,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = ((ord_less @ TA @ B @ A) | (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_not__less__iff__gr__or__eq)).
% 47.90/26.73  thf(437,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = ((ord_less @ TA @ B @ A) | (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 47.90/26.73  thf(65,axiom,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_order__class_Oorder_Oeq__iff)).
% 47.90/26.73  thf(474,plain,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 47.90/26.73  thf(235,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_150_order_Oorder__iff__strict)).
% 47.90/26.73  thf(1056,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 47.90/26.73  thf(38,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB)]: ((! [C:TA]: (ord_less_eq @ TB @ (A @ C) @ (B @ C))) => (ord_less_eq @ (TA > TB) @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_le__funI)).
% 47.90/26.73  thf(400,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB)]: ((! [C:TA]: (ord_less_eq @ TB @ (A @ C) @ (B @ C))) => (ord_less_eq @ (TA > TB) @ (A) @ (B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 47.90/26.73  thf(114,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o),C:TA]: ((ord_less_eq @ (TA > $o) @ A @ B) => ((A @ C) => (B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_predicate1D)).
% 47.90/26.73  thf(635,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o),C:TA]: ((ord_less_eq @ (TA > $o) @ (A) @ (B)) => ((A @ C) => (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 47.90/26.73  thf(238,axiom,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((! [D:TA]: ((ord_less @ TA @ A @ D) => ((ord_less @ TA @ D @ B) => (ord_less_eq @ TA @ D @ C)))) => (ord_less_eq @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_155_dense__le__bounded)).
% 47.90/26.73  thf(1065,plain,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((! [D:TA]: ((ord_less @ TA @ A @ D) => ((ord_less @ TA @ D @ B) => (ord_less_eq @ TA @ D @ C)))) => (ord_less_eq @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[238])).
% 47.90/26.73  thf(7,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => ((bNF_Ca1785829860lChain @ TA @ TB) = (^ [A:(set @ (product_prod @ TA @ TA)),B:(TA > TB)]: ! [C:TA,D:TA]: ((member @ (product_prod @ TA @ TA) @ (product_Pair @ TA @ TA @ C @ D) @ A) => (ord_less_eq @ TB @ (B @ C) @ (B @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_252_relChain__def)).
% 47.90/26.73  thf(283,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => ((bNF_Ca1785829860lChain @ TA @ TB) = (^ [A:(set @ (product_prod @ TA @ TA)),B:(TA > TB)]: ! [C:TA,D:TA]: ((member @ (product_prod @ TA @ TA) @ (product_Pair @ TA @ TA @ C @ D) @ A) => (ord_less_eq @ TB @ (B @ C) @ (B @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 47.90/26.73  thf(193,axiom,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:TA,C:(binary1291135688e_Tree @ TA),D:(binary1291135688e_Tree @ TA),E:TA,F:(binary1291135688e_Tree @ TA)]: (((binary210054475elle_T @ TA @ A @ B @ C) = (binary210054475elle_T @ TA @ D @ E @ F)) = ((A = D) & (B = E) & (C = F)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_Tree_Oinject)).
% 47.90/26.73  thf(928,plain,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:TA,C:(binary1291135688e_Tree @ TA),D:(binary1291135688e_Tree @ TA),E:TA,F:(binary1291135688e_Tree @ TA)]: (((binary210054475elle_T @ TA @ A @ B @ C) = (binary210054475elle_T @ TA @ D @ E @ F)) = ((A = D) & (B = E) & (C = F)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 47.90/26.73  thf(189,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > $o)]: (ord_less_eq @ (set @ TA) @ (collect @ TA @ (^ [C:TA]: ((member @ TA @ C @ A) & (B @ C)))) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_208_Collect__restrict)).
% 47.90/26.73  thf(918,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > $o)]: (ord_less_eq @ (set @ TA) @ (collect @ TA @ (^ [C:TA]: ((member @ TA @ C @ A) & (B @ C)))) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 47.90/26.73  thf(155,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_156_order_Ostrict__implies__order)).
% 47.90/26.73  thf(801,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 47.90/26.73  thf(140,axiom,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:TA,C:(binary1291135688e_Tree @ TA)]: ((binary1746293266le_Tip @ TA) != (binary210054475elle_T @ TA @ A @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_Tree_Odistinct_I1_J)).
% 47.90/26.73  thf(728,plain,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:TA,C:(binary1291135688e_Tree @ TA)]: ~ ((binary1746293266le_Tip @ TA) = (binary210054475elle_T @ TA @ A @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 47.90/26.73  thf(49,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TA > (TB > TC)),B:((product_prod @ TA @ TB) > TC)]: ((! [C:TA,D:TB]: ((A @ C @ D) = (B @ (product_Pair @ TA @ TB @ C @ D)))) => ((product_case_prod @ TA @ TB @ TC @ A) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_250_cond__case__prod__eta)).
% 47.90/26.73  thf(427,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TA > (TB > TC)),B:((product_prod @ TA @ TB) > TC)]: ((! [C:TA,D:TB]: ((A @ C @ D) = (B @ (product_Pair @ TA @ TB @ C @ D)))) => ((product_case_prod @ TA @ TB @ TC @ A) = (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 47.90/26.73  thf(172,axiom,((! [TA: $tType]: (! [A:(TA > int),B:TA,C:TA,D:(binary1291135688e_Tree @ TA),E:(binary1291135688e_Tree @ TA)]: (((ord_less @ int @ (A @ B) @ (A @ C)) => ((binary1830089824insert @ TA @ A @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = (binary210054475elle_T @ TA @ (binary1830089824insert @ TA @ A @ B @ D) @ C @ E))) & ((~ (ord_less @ int @ (A @ B) @ (A @ C))) => (((ord_less @ int @ (A @ C) @ (A @ B)) => ((binary1830089824insert @ TA @ A @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = (binary210054475elle_T @ TA @ D @ C @ (binary1830089824insert @ TA @ A @ B @ E)))) & ((~ (ord_less @ int @ (A @ C) @ (A @ B))) => ((binary1830089824insert @ TA @ A @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = (binary210054475elle_T @ TA @ D @ B @ E))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_binsert_Osimps_I2_J)).
% 47.90/26.73  thf(860,plain,((! [TA: $tType]: (! [A:(TA > int),B:TA,C:TA,D:(binary1291135688e_Tree @ TA),E:(binary1291135688e_Tree @ TA)]: (((ord_less @ int @ (A @ B) @ (A @ C)) => ((binary1830089824insert @ TA @ (A) @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = (binary210054475elle_T @ TA @ (binary1830089824insert @ TA @ (A) @ B @ D) @ C @ E))) & ((~ (ord_less @ int @ (A @ B) @ (A @ C))) => (((ord_less @ int @ (A @ C) @ (A @ B)) => ((binary1830089824insert @ TA @ (A) @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = (binary210054475elle_T @ TA @ D @ C @ (binary1830089824insert @ TA @ (A) @ B @ E)))) & ((~ (ord_less @ int @ (A @ C) @ (A @ B))) => ((binary1830089824insert @ TA @ (A) @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = (binary210054475elle_T @ TA @ D @ B @ E))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 47.90/26.73  thf(103,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TB > (TC > (TA > $o))),B:TB,C:TC,D:TA]: ((product_case_prod @ TB @ TC @ (TA > $o) @ A @ (product_Pair @ TB @ TC @ B @ C) @ D) => (A @ B @ C @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_245_case__prodD_H)).
% 47.90/26.73  thf(596,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TB > (TC > (TA > $o))),B:TB,C:TC,D:TA]: ((product_case_prod @ TB @ TC @ (TA > $o) @ (A) @ (product_Pair @ TB @ TC @ B @ C) @ D) => (A @ B @ C @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 47.90/26.73  thf(117,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TB > $o),B:(TC > (TA > TB)),C:(product_prod @ TC @ TA)]: ((A @ (product_case_prod @ TC @ TA @ TB @ B @ C)) => (~ (! [D:TC,E:TA]: ((C = (product_Pair @ TC @ TA @ D @ E)) => (~ (A @ (B @ D @ E)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_248_case__prodE2)).
% 47.90/26.73  thf(644,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TB > $o),B:(TC > (TA > TB)),C:(product_prod @ TC @ TA)]: ((A @ (product_case_prod @ TC @ TA @ TB @ (B) @ C)) => (~ (! [D:TC,E:TA]: ((C = (product_Pair @ TC @ TA @ D @ E)) => (~ (A @ (B @ D @ E)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 47.90/26.73  thf(161,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((A != B) => (ord_less @ (set @ TA) @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_174_psubsetI)).
% 47.90/26.73  thf(822,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((~ (A = B)) => (ord_less @ (set @ TA) @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 47.90/26.73  thf(55,axiom,((! [TA: $tType,TB: $tType]: (! [A:(set @ (product_prod @ TA @ TB)),B:(set @ (product_prod @ TA @ TB))]: ((ord_less_eq @ (TA > (TB > $o)) @ (^ [C:TA,D:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ A)) @ (^ [C:TA,D:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ B))) = (ord_less_eq @ (set @ (product_prod @ TA @ TB)) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_pred__subset__eq2)).
% 47.90/26.73  thf(442,plain,((! [TA: $tType,TB: $tType]: (! [A:(set @ (product_prod @ TA @ TB)),B:(set @ (product_prod @ TA @ TB))]: ((ord_less_eq @ (TA > (TB > $o)) @ (^ [C:TA,D:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ A)) @ (^ [C:TA,D:TB]: (member @ (product_prod @ TA @ TB) @ (product_Pair @ TA @ TB @ C @ D) @ B))) = (ord_less_eq @ (set @ (product_prod @ TA @ TB)) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 47.90/26.73  thf(174,axiom,((! [TA: $tType]: ((ord_less @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (ord_less @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_213_less__set__def)).
% 47.90/26.73  thf(871,plain,((! [TA: $tType]: ((ord_less @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (ord_less @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 47.90/26.73  thf(260,axiom,((((t1 != (binary1746293266le_Tip @ a)) & (binary1610619414edTree @ a @ h @ t1)) => (binary1610619414edTree @ a @ h @ (binary213313527le_wrm @ a @ h @ t1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_h1)).
% 47.90/26.73  thf(1120,plain,(((~ (t1 = (binary1746293266le_Tip @ a)) & (binary1610619414edTree @ a @ (h) @ t1)) => (binary1610619414edTree @ a @ (h) @ (binary213313527le_wrm @ a @ (h) @ t1)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[260])).
% 47.90/26.73  thf(248,axiom,((no_top @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Ono__top)).
% 47.90/26.73  thf(1093,plain,((no_top @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[248])).
% 47.90/26.73  thf(36,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (C != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_minf_I3_J)).
% 47.90/26.73  thf(395,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (C = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 47.90/26.73  thf(111,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_less__imp__not__eq2)).
% 47.90/26.73  thf(624,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 47.90/26.73  thf(164,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_110_equals0I)).
% 47.90/26.73  thf(839,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)],[164])).
% 47.90/26.73  thf(29,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oord)).
% 47.90/26.73  thf(369,plain,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 47.90/26.73  thf(106,axiom,((! [TA: $tType,TB: $tType]: (! [A:(product_prod @ TA @ TB),B:(TA > (TB > $o))]: ((! [C:TA,D:TB]: ((A = (product_Pair @ TA @ TB @ C @ D)) => (B @ C @ D))) => (product_case_prod @ TA @ TB @ $o @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_235_case__prodI2)).
% 47.90/26.73  thf(607,plain,((! [TA: $tType,TB: $tType]: (! [A:(product_prod @ TA @ TB),B:(TA > (TB > $o))]: ((! [C:TA,D:TB]: ((A = (product_Pair @ TA @ TB @ C @ D)) => (B @ C @ D))) => (product_case_prod @ TA @ TB @ $o @ (B) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 47.90/26.73  thf(70,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TB > $o)),B:(TA > (TB > $o))]: ((! [C:TA,D:TB]: ((A @ C @ D) => (B @ C @ D))) => (ord_less_eq @ (TA > (TB > $o)) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_233_predicate2I)).
% 47.90/26.73  thf(486,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TB > $o)),B:(TA > (TB > $o))]: ((! [C:TA,D:TB]: ((A @ C @ D) => (B @ C @ D))) => (ord_less_eq @ (TA > (TB > $o)) @ (A) @ (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 47.90/26.73  thf(156,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) = (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_not__le)).
% 47.90/26.73  thf(803,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) = (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 47.90/26.73  thf(63,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TA > $o)),B:TB,C:TA]: ((product_case_prod @ TB @ TA @ $o @ A @ (product_Pair @ TB @ TA @ B @ C)) => (A @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_243_case__prodD)).
% 47.90/26.73  thf(469,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TA > $o)),B:TB,C:TA]: ((product_case_prod @ TB @ TA @ $o @ (A) @ (product_Pair @ TB @ TA @ B @ C)) => (A @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 47.90/26.73  thf(191,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_le__less__trans)).
% 47.90/26.73  thf(923,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 47.90/26.73  thf(227,axiom,((! [TA: $tType,TB: $tType]: (! [A:TA,B:((binary1291135688e_Tree @ TB) > (TB > ((binary1291135688e_Tree @ TB) > (TA > (TA > TA)))))]: ((binary1929596613c_Tree @ TA @ TB @ A @ B @ (binary1746293266le_Tip @ TB)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_Tree_Osimps_I6_J)).
% 47.90/26.73  thf(1037,plain,((! [TA: $tType,TB: $tType]: (! [A:TA,B:((binary1291135688e_Tree @ TB) > (TB > ((binary1291135688e_Tree @ TB) > (TA > (TA > TA)))))]: ((binary1929596613c_Tree @ TA @ TB @ A @ (B) @ (binary1746293266le_Tip @ TB)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 47.90/26.73  thf(74,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TA > $o)),B:(TB > (TA > $o)),C:TB,D:TA]: ((ord_less_eq @ (TB > (TA > $o)) @ A @ B) => ((A @ C @ D) => (B @ C @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_241_predicate2D)).
% 47.90/26.73  thf(496,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TA > $o)),B:(TB > (TA > $o)),C:TB,D:TA]: ((ord_less_eq @ (TB > (TA > $o)) @ (A) @ (B)) => ((A @ C @ D) => (B @ C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 47.90/26.73  thf(133,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_less__imp__neq)).
% 47.90/26.73  thf(708,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 47.90/26.73  thf(148,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_159_dual__order_Ostrict__implies__order)).
% 47.90/26.73  thf(755,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 47.90/26.73  thf(125,axiom,((! [TA: $tType]: ((bot_bot @ (TA > $o)) = (^ [A:TA]: (member @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_209_bot__empty__eq)).
% 47.90/26.73  thf(676,plain,((! [TA: $tType]: ((bot_bot @ (TA > $o)) = (^ [A:TA]: (member @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 47.90/26.73  thf(1137,plain,(($false)),inference(e,[status(thm)],[365,1105,468,1110,909,628,582,1005,683,276,308,1073,440,533,550,500,797,715,814,945,538,747,913,404,898,301,570,719,504,751,344,1059,542,1087,421,969,416,1115,289,492,1040,1020,806,353,480,877,956,660,527,602,981,411,988,1104,849,452,920,925,761,534,1047,512,942,825,598,820,275,1123,349,407,693,916,1032,665,1079,757,1128,842,974,847,566,852,435,742,1089,874,615,725,356,593,1118,857,471,884,1082,637,1016,679,547,706,985,738,1050,721,371,1131,654,984,911,792,266,360,508,311,1054,558,1026,530,1086,938,906,618,430,1103,279,573,375,904,423,1007,402,1125,286,413,641,391,498,1107,704,947,445,936,979,900,377,451,303,1011,419,880,1043,477,387,494,631,367,816,323,594,621,483,964,668,462,1029,895,399,959,868,1113,299,267,505,658,1034,490,795,1134,749,1018,553,836,712,580,1070,971,409,310,673,585,717,502,576,544,744,703,1023,1052,1094,612,991,465,1084,931,976,891,844,363,556,699,961,304,1062,1101,652,731,1045,1077,478,447,315,432,967,854,790,373,950,1097,341,358,437,474,1056,400,635,1065,283,928,918,801,728,427,860,596,644,822,442,871,1120,1093,395,624,839,369,607,486,803,469,923,1037,496,708,755,676])).
% 47.90/26.73  % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 47.90/26.73  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------