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

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

% Result   : Theorem 73.50s 45.65s
% Output   : Refutation 74.58s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ITP193^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.09/0.20  % Computer : n014.cluster.edu
% 0.09/0.20  % Model    : x86_64 x86_64
% 0.09/0.20  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20  % Memory   : 8046.5625MB
% 0.09/0.20  % OS       : Linux 6.8.0-71-generic
% 0.09/0.20  % CPULimit : 300
% 0.09/0.20  % WCLimit  : 300
% 0.09/0.20  % DateTime : Tue Sep 29 20:09:44 UTC 2026
% 0.09/0.21  % CPUTime  : 
% 0.09/0.21  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.03/0.86  % [INFO] 	 Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ... 
% 2.66/1.37  % [INFO] 	 Parsing done (506ms). 
% 2.66/1.38  % [INFO] 	 Running in sequential loop mode. 
% 4.29/1.71  % [INFO] 	 eprover registered as external prover. 
% 4.29/1.72  % [INFO] 	 Scanning for conjecture ... 
% 4.63/1.86  % [INFO] 	 Found a conjecture (or negated_conjecture) and 351 axioms. Running axiom selection ... 
% 4.93/2.01  % [INFO] 	 Axiom selection finished. Selected 350 axioms (removed 1 axioms). 
% 7.08/2.43  % [INFO] 	 Problem is higher-order (TPTP THF). 
% 7.08/2.48  % [INFO] 	 Type checking passed. 
% 7.08/2.49  % [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 ... 
% 73.50/45.64  % External prover 'e' found a proof!
% 73.50/45.64  % [INFO] 	 Killing All external provers ... 
% 73.50/45.65  % Time passed: 45298ms (effective reasoning time: 44260ms)
% 73.50/45.65  % 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)>
% 73.50/45.65  % Axioms used in derivation (350): tcon_Polynomial_Opoly___Rings_Ocomm__semiring__0_57, fact_81_ord__eq__less__subst, tcon_Real_Oreal___Rings_Ocomm__semiring__0_38, fact_75_order__subst2, tcon_Set_Oset___Orderings_Oorder_23, fact_215_less__eq__int__code_I1_J, tcon_Real_Oreal___Orderings_Olinorder_41, tcon_Nat_Onat___Groups_Oone_20, tcon_Nat_Onat___Orderings_Oord_18, fact_27_not__eq__pos__or__neg__iff__2, fact_66_le__cases3, fact_41_dual__order_Ostrict__implies__order, fact_168_set__eq__subset, fact_107_dual__order_Oirrefl, tcon_Real_Oreal___Orderings_Oord_47, fact_188_minf_I11_J, fact_100_less__imp__not__eq, tcon_Real_Oreal___Groups_Oordered__comm__monoid__add_33, fact_25_finite, tcon_Nat_Onat___Rings_Ocomm__semiring__1_11, fact_231_sum_Oneutral__const, fact_181_pinf_I11_J, tcon_Real_Oreal___Conditionally__Complete__Lattices_Oconditionally__complete__linorder_30, fact_207_verit__la__generic, tcon_fun___Finite__Set_Ofinite, fact_148_psubsetI, fact_61_order__class_Oorder_Oantisym, fact_220_cindex__poly__def, tcon_Polynomial_Opoly___Orderings_Oord_64, fact_62_ord__le__eq__trans, fact_171_Collect__mono__iff, fact_166_Collect__mono, fact_239_sum__mono, fact_146_dual__order_Ostrict__trans2, tcon_Int_Oint___Groups_Ozero, fact_125_order__less__le__subst1, fact_36_order__refl, tcon_Real_Oreal___Rings_Ocomm__semiring__1_37, fact_9_finite__Collect__disjI, fact_28_not__eq__pos__or__neg__iff__1, fact_172_less__fun__def, tcon_Real_Oreal___Orderings_Oorder_45, fact_8_finite__Collect__conjI, fact_251_not__one__less__zero, fact_238_sum_Oneutral, fact_140_not__le__imp__less, tcon_Nat_Onat___Orderings_Olinorder_15, tcon_Int_Oint___Nat_Oring__char__0, fact_108_order_Ostrict__trans, fact_185_minf_I4_J, fact_189_conj__le__cong, fact_119_leD, fact_216_pred__subset__eq, tcon_fun___Orderings_Oord, fact_29_poly__eq__poly__eq__iff, fact_39_complete__interval, fact_86_gt__ex, fact_242_sum__nonneg, fact_139_less__le__not__le, fact_163_equalityD2, tcon_Polynomial_Opoly___Rings_Oidom, fact_116_ex__gt__or__lt, fact_15_less__numeral__extra_I3_J, fact_49_dense__le__bounded, tcon_Polynomial_Opoly___Rings_Ocomm__ring__1_61, fact_138_le__imp__less__or__eq, fact_194_psubset__subset__trans, fact_19_finite__psubset__induct, fact_7_assms_I4_J, fact_137_le__less__linear, tcon_Real_Oreal___Orderings_Ono__bot_44, fact_247_sum__strict__mono__ex1, fact_196_psubset__trans, fact_206_jump__poly0_I1_J, fact_213_finite__interval__int3, fact_155_poly__cutoff__0, fact_158_in__mono, tcon_Int_Oint___Groups_Oordered__comm__monoid__add, fact_117_complete__real, fact_123_order__le__less__subst1, fact_58_linorder__wlog, fact_245_sum__le__included, fact_59_dual__order_Orefl, fact_89_order_Oasym, fact_153_verit__comp__simplify1_I3_J, fact_94_less__trans, fact_55_dual__order_Oantisym, fact_85_lt__ex, fact_64_order__class_Oorder_Oeq__iff, fact_37_cross__no__root, fact_144_order_Ostrict__iff__order, fact_53_infinite__super, fact_240_sum_Oswap__restrict, fact_221_reflect__poly__1, tcon_Polynomial_Opoly___Groups_Oordered__comm__monoid__add_52, fact_115_dual__order_Ostrict__implies__not__eq, fact_68_le__cases, fact_241_sum__nonpos, fact_32_zero__less__iff__neq__zero, fact_2_assms_I3_J, tcon_Nat_Onat___Orderings_Oorder_17, fact_77_le__fun__def, tcon_Int_Oint___Rings_Ocomm__ring__1, tcon_Real_Oreal___Rings_Oidom_1, fact_205_reflect__poly__0, fact_227_less__numeral__extra_I1_J, fact_236_sum_Oswap, fact_208_predicate1D, tcon_Real_Oreal___Orderings_Opreorder_40, fact_200_less__set__def, fact_219_cindex__poly__cross, fact_246_sum__nonneg__eq__0__iff, fact_157_subset__antisym, fact_218_cindex__poly__0_I1_J, fact_170_less__eq__set__def, fact_82_ord__less__eq__subst, fact_63_ord__eq__le__trans, fact_179_pinf_I5_J, fact_52_finite__subset, fact_98_ord__less__eq__trans, fact_21_finite__has__maximal2, tcon_Real_Oreal___Nat_Oring__char__0_46, fact_133_le__less__trans, tcon_Real_Oreal___Rings_Oring__no__zero__divisors_34, fact_248_sum__nonneg__0, tcon_Int_Oint___Conditionally__Complete__Lattices_Oconditionally__complete__linorder, help_If_1_1_T, fact_83_order__less__subst1, fact_95_less__linear, fact_80_le__funD, tcon_Set_Oset___Finite__Set_Ofinite_22, tcon_Polynomial_Opoly___Orderings_Oorder_62, fact_76_order__subst1, fact_175_pinf_I1_J, fact_204_predicate1I, fact_198_psubsetE, fact_149_minf_I8_J, fact_12_poly__IVT__pos, fact_24_zero__reorient, fact_124_order__le__less__subst2, fact_159_subsetD, fact_16_le__zero__eq, tcon_HOL_Obool___Orderings_Oorder_28, tcon_Polynomial_Opoly___Nat_Oring__char__0_63, fact_224_le__numeral__extra_I4_J, fact_127_not__le, tcon_HOL_Obool___Finite__Set_Ofinite_27, tcon_Nat_Onat___Conditionally__Complete__Lattices_Oconditionally__complete__linorder_6, fact_191_subset__iff__psubset__eq, tcon_Nat_Onat___Orderings_Ono__top_16, fact_109_less__imp__not__less, tcon_Int_Oint___Rings_Olinordered__idom, tcon_Int_Oint___Orderings_Olinorder, fact_57_dual__order_Otrans, tcon_Int_Oint___Rings_Ocomm__semiring__1, fact_250_sum__pos2, fact_35_gr__zeroI, tcon_Int_Oint___Orderings_Oorder_4, tcon_Int_Oint___Rings_Ozero__less__one, fact_20_finite__has__minimal2, fact_190_imp__le__cong, tcon_Real_Oreal___Groups_Oone_49, fact_132_less__imp__le, fact_217_cindex__poly__0_I2_J, fact_101_less__not__sym, tcon_Nat_Onat___Orderings_Owellorder, fact_210_finite__interval__int1, fact_38_less__eq__real__def, fact_136_dense__le, fact_161_subset__eq, fact_165_subset__refl, tcon_Polynomial_Opoly___Rings_Ocomm__semiring__1_56, tcon_Nat_Onat___Groups_Oordered__comm__monoid__add_9, fact_180_pinf_I7_J, fact_244_sum_Ointer__filter, fact_84_order__less__subst2, fact_79_le__funE, tcon_Polynomial_Opoly___Rings_Oring__no__zero__divisors_53, fact_253_linorder__neqE__linordered__idom, fact_96_less__irrefl, fact_197_psubset__eq, tcon_Real_Oreal___Conditionally__Complete__Lattices_Olinear__continuum, fact_103_antisym__conv3, fact_122_less__le, tcon_Polynomial_Opoly___Groups_Oone_66, fact_56_dual__order_Oeq__iff, tcon_Int_Oint___Groups_Ocomm__monoid__add, tcon_Real_Oreal___Orderings_Ono__top_43, fact_6_not__gr__zero, fact_72_eq__iff, fact_1_assms_I2_J, fact_131_antisym__conv2, tcon_Polynomial_Opoly___Orderings_Opreorder_59, tcon_Real_Oreal___Orderings_Odense__order, fact_88_neq__iff, fact_150_minf_I6_J, fact_126_order__less__le__subst2, tcon_Real_Oreal___Orderings_Odense__linorder, fact_169_Collect__subset, fact_243_sum__mono__inv, tcon_Int_Oint___Rings_Oidom_2, fact_201_reflect__poly__at__0__eq__0__iff, fact_87_neqE, fact_167_subset__trans, fact_176_pinf_I2_J, tcon_Real_Oreal___Rings_Olinordered__idom_36, tcon_Set_Oset___Orderings_Oord_24, fact_73_ord__le__eq__subst, fact_183_minf_I2_J, fact_178_pinf_I4_J, fact_33_gr__implies__not__zero, fact_91_less__imp__neq, fact_234_sum__eq__1__iff, fact_214_less__int__code_I1_J, tcon_Polynomial_Opoly___Rings_Olinordered__nonzero__semiring_51, fact_78_le__funI, fact_11_poly__IVT__neg, help_If_3_1_T, fact_0__092_060open_062finite_A_123x_O_Apoly_Ap_Ax_A_061_A0_125_092_060close_062, fact_92_less__asym, help_If_2_1_T, tcon_Int_Oint___Orderings_Oord_5, fact_228_less__numeral__extra_I4_J, fact_71_antisym, fact_232_sum_Oinfinite, fact_118_field__lbound__gt__zero, tcon_Nat_Onat___Rings_Olinordered__nonzero__semiring_8, fact_230_sum_Odelta, fact_110_exists__least__iff, fact_17_zero__le, fact_104_less__imp__not__eq2, fact_74_ord__eq__le__subst, fact_93_less__asym_H, fact_249_sum__nonneg__leq__bound, tcon_Nat_Onat___Rings_Ozero__less__one_13, tcon_Polynomial_Opoly___Orderings_Olinorder_60, tcon_Real_Oreal___Rings_Ocomm__ring__1_42, fact_102_less__induct, tcon_Polynomial_Opoly___Groups_Oordered__cancel__comm__monoid__add_50, tcon_Polynomial_Opoly___Groups_Ocomm__monoid__add_54, fact_40_order_Onot__eq__order__implies__strict, fact_199_psubsetD, fact_193_subset__not__subset__eq, fact_112_dual__order_Ostrict__trans, tcon_Real_Oreal___Rings_Olinordered__nonzero__semiring_32, fact_252_zero__less__one, fact_18_le__numeral__extra_I3_J, fact_151_pinf_I8_J, fact_235_int__one__le__iff__zero__less, tcon_Int_Oint___Rings_Oring__no__zero__divisors, fact_113_not__less__iff__gr__or__eq, fact_99_dual__order_Oasym, fact_237_sum_Onot__neutral__contains__not__neutral, tcon_fun___Orderings_Opreorder, tcon_Int_Oint___Rings_Ocomm__semiring__0, fact_3_assms_I1_J, fact_186_minf_I5_J, tcon_Real_Oreal___Fields_Olinordered__field, fact_142_order_Ostrict__trans2, fact_226_one__reorient, fact_45_Collect__mem__eq, tcon_Real_Oreal___Groups_Ozero_48, fact_120_leI, tcon_HOL_Obool___Orderings_Opreorder_25, fact_90_dense, fact_187_minf_I7_J, fact_195_psubset__imp__subset, fact_135_dense__ge, fact_50_finite__Collect__subsets, fact_22_next__non__root__interval, fact_143_order_Oorder__iff__strict, fact_233_sum__eq__0__iff, tcon_HOL_Obool___Orderings_Olinorder_26, fact_111_linorder__less__wlog, fact_48_order_Ostrict__implies__order, fact_222_poly__1, fact_23_last__non__root__interval, fact_14_poly__all__0__iff__0, tcon_Polynomial_Opoly___Groups_Ozero_65, fact_130_antisym__conv1, fact_69_eq__refl, tcon_Int_Oint___Orderings_Ono__bot, fact_192_subset__psubset__trans, tcon_fun___Orderings_Oorder, fact_212_finite__interval__int4, tcon_Int_Oint___Orderings_Opreorder_3, fact_156_subsetI, fact_70_linear, fact_145_dual__order_Ostrict__trans1, fact_42_dual__order_Ostrict__iff__order, fact_4_False, fact_154_is__zero__null, fact_67_order_Otrans, fact_10_poly__roots__finite, tcon_Polynomial_Opoly___Rings_Olinordered__idom_55, tcon_Int_Oint___Orderings_Ono__top, fact_60_order__trans, fact_13_finite__code, fact_160_equalityE, tcon_Nat_Onat___Groups_Ocanonically__ordered__monoid__add, fact_229_sum_Odelta_H, fact_106_linorder__cases, fact_128_not__less, fact_174_verit__comp__simplify1_I1_J, fact_43_dual__order_Oorder__iff__strict, fact_54_rev__finite__subset, tcon_Set_Oset___Orderings_Opreorder_21, tcon_Int_Oint___Groups_Oordered__cancel__comm__monoid__add, fact_203_jump__poly0_I2_J, fact_211_finite__interval__int2, fact_34_not__less__zero, fact_162_equalityD1, fact_129_le__neq__trans, fact_141_order_Ostrict__trans1, fact_182_minf_I1_J, fact_184_minf_I3_J, fact_152_pinf_I6_J, fact_105_less__imp__triv, tcon_Int_Oint___Rings_Olinordered__nonzero__semiring, fact_177_pinf_I3_J, tcon_Real_Oreal___Groups_Oordered__cancel__comm__monoid__add_31, tcon_Int_Oint___Groups_Oone, fact_147_dense__ge__bounded, fact_114_order_Ostrict__implies__not__eq, tcon_Real_Oreal___Groups_Ocomm__monoid__add_35, fact_223_poly__cutoff__1, fact_65_antisym__conv, tcon_Nat_Onat___Rings_Ocomm__semiring__0_12, fact_5_poly__0, tcon_Nat_Onat___Groups_Oordered__cancel__comm__monoid__add_7, tcon_Nat_Onat___Groups_Ocomm__monoid__add_10, fact_134_less__le__trans, fact_46_Collect__cong, fact_209_rev__predicate1D, tcon_Nat_Onat___Orderings_Opreorder_14, tcon_Nat_Onat___Groups_Ozero_19, fact_26_finite__set__choice, fact_97_ord__eq__less__trans, fact_31_not__finite__existsD, fact_121_le__less, tcon_Polynomial_Opoly___Rings_Ozero__less__one_58, fact_51_cross__0, fact_173_verit__la__disequality, tcon_Real_Oreal___Rings_Ozero__less__one_39, fact_225_poly__sum, fact_202_jump__poly__not__root, fact_30_pigeonhole__infinite__rel, fact_44_mem__Collect__eq, tcon_HOL_Obool___Orderings_Oord_29, fact_164_subset__iff
% 73.50/45.65  % No. of inferences in proof: 704
% 73.50/45.65  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 45298 ms resp. 44260 ms w/o parsing
% 74.58/45.94  % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 74.58/45.94  thf(real_type, type, real: $tType).
% 74.58/45.94  thf(nat_type, type, nat: $tType).
% 74.58/45.94  thf(int_type, type, int: $tType).
% 74.58/45.94  thf(idom_decl, type, idom: !> [TA: $tType]: $o).
% 74.58/45.94  thf(one_decl, type, one: !> [TA: $tType]: $o).
% 74.58/45.94  thf(zero_decl, type, zero: !> [TA: $tType]: $o).
% 74.58/45.94  thf(ord_decl, type, ord: !> [TA: $tType]: $o).
% 74.58/45.94  thf(ring_char_0_decl, type, ring_char_0: !> [TA: $tType]: $o).
% 74.58/45.94  thf(order_decl, type, order: !> [TA: $tType]: $o).
% 74.58/45.94  thf(no_bot_decl, type, no_bot: !> [TA: $tType]: $o).
% 74.58/45.94  thf(no_top_decl, type, no_top: !> [TA: $tType]: $o).
% 74.58/45.94  thf(finite_finite_decl, type, finite_finite: !> [TA: $tType]: $o).
% 74.58/45.94  thf(comm_ring_1_decl, type, comm_ring_1: !> [TA: $tType]: $o).
% 74.58/45.94  thf(linorder_decl, type, linorder: !> [TA: $tType]: $o).
% 74.58/45.94  thf(preorder_decl, type, preorder: !> [TA: $tType]: $o).
% 74.58/45.94  thf(wellorder_decl, type, wellorder: !> [TA: $tType]: $o).
% 74.58/45.94  thf(zero_less_one_decl, type, zero_less_one: !> [TA: $tType]: $o).
% 74.58/45.94  thf(dense_order_decl, type, dense_order: !> [TA: $tType]: $o).
% 74.58/45.94  thf(comm_semiring_0_decl, type, comm_semiring_0: !> [TA: $tType]: $o).
% 74.58/45.94  thf(comm_semiring_1_decl, type, comm_semiring_1: !> [TA: $tType]: $o).
% 74.58/45.94  thf(linordered_idom_decl, type, linordered_idom: !> [TA: $tType]: $o).
% 74.58/45.94  thf(comm_monoid_add_decl, type, comm_monoid_add: !> [TA: $tType]: $o).
% 74.58/45.94  thf(linordered_field_decl, type, linordered_field: !> [TA: $tType]: $o).
% 74.58/45.94  thf(dense_linorder_decl, type, dense_linorder: !> [TA: $tType]: $o).
% 74.58/45.94  thf(ring_n68954251visors_decl, type, ring_n68954251visors: !> [TA: $tType]: $o).
% 74.58/45.94  thf(ordere216010020id_add_decl, type, ordere216010020id_add: !> [TA: $tType]: $o).
% 74.58/45.94  thf(linord1659791738miring_decl, type, linord1659791738miring: !> [TA: $tType]: $o).
% 74.58/45.94  thf(canoni770627133id_add_decl, type, canoni770627133id_add: !> [TA: $tType]: $o).
% 74.58/45.94  thf(ordere1818651114id_add_decl, type, ordere1818651114id_add: !> [TA: $tType]: $o).
% 74.58/45.94  thf(condit1656338222tinuum_decl, type, condit1656338222tinuum: !> [TA: $tType]: $o).
% 74.58/45.94  thf(condit1037483654norder_decl, type, condit1037483654norder: !> [TA: $tType]: $o).
% 74.58/45.94  thf(finite_finite2_decl, type, finite_finite2: !> [TA: $tType]: ((set @ TA) > $o)).
% 74.58/45.94  thf(one_one_decl, type, one_one: !> [TA: $tType]: TA).
% 74.58/45.94  thf(zero_zero_decl, type, zero_zero: !> [TA: $tType]: TA).
% 74.58/45.94  thf(groups1340683514dd_sum_decl, type, groups1340683514dd_sum: !> [TA: $tType,TB: $tType]: ((TB > TA) > ((set @ TB) > TA))).
% 74.58/45.94  thf(if_decl, type, if: !> [TA: $tType]: ($o > (TA > (TA > TA)))).
% 74.58/45.94  thf(ord_less_decl, type, ord_less: !> [TA: $tType]: (TA > (TA > $o))).
% 74.58/45.94  thf(ord_less_eq_decl, type, ord_less_eq: !> [TA: $tType]: (TA > (TA > $o))).
% 74.58/45.94  thf(is_zero_decl, type, is_zero: !> [TA: $tType]: ((poly @ TA) > $o)).
% 74.58/45.94  thf(poly2_decl, type, poly2: !> [TA: $tType]: ((poly @ TA) > (TA > TA))).
% 74.58/45.94  thf(poly_cutoff_decl, type, poly_cutoff: !> [TA: $tType]: (nat > ((poly @ TA) > (poly @ TA)))).
% 74.58/45.94  thf(reflect_poly_decl, type, reflect_poly: !> [TA: $tType]: ((poly @ TA) > (poly @ TA))).
% 74.58/45.94  thf(collect_decl, type, collect: !> [TA: $tType]: ((TA > $o) > (set @ TA))).
% 74.58/45.94  thf(sturm_1539314049x_poly_decl, type, sturm_1539314049x_poly: (real > (real > ((poly @ real) > ((poly @ real) > int))))).
% 74.58/45.94  thf(sturm_424270202_cross_decl, type, sturm_424270202_cross: ((poly @ real) > (real > (real > int)))).
% 74.58/45.94  thf(sturm_652470720p_poly_decl, type, sturm_652470720p_poly: ((poly @ real) > ((poly @ real) > (real > int)))).
% 74.58/45.94  thf(member_decl, type, member: !> [TA: $tType]: (TA > ((set @ TA) > $o))).
% 74.58/45.94  thf(a_decl, type, a: real).
% 74.58/45.94  thf(a2_decl, type, a2: real).
% 74.58/45.94  thf(b_decl, type, b: real).
% 74.58/45.94  thf(b2_decl, type, b2: real).
% 74.58/45.94  thf(p_decl, type, p: (poly @ real)).
% 74.58/45.94  thf(196,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_140_not__le__imp__less)).
% 74.58/45.94  thf(892,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)],[196])).
% 74.58/45.94  thf(237,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: ((ordere216010020id_add @ TB) => (! [A:(set @ TC),B:(set @ TA),C:(TA > TB),D:(TA > TC),E:(TC > TB)]: ((finite_finite2 @ TC @ A) => ((finite_finite2 @ TA @ B) => ((! [F:TA]: ((member @ TA @ F @ B) => (ord_less_eq @ TB @ (zero_zero @ TB) @ (C @ F)))) => ((! [F:TC]: ((member @ TC @ F @ A) => (? [G:TA]: ((member @ TA @ G @ B) & ((D @ G) = F) & (ord_less_eq @ TB @ (E @ F) @ (C @ G)))))) => (ord_less_eq @ TB @ (groups1340683514dd_sum @ TC @ TB @ E @ A) @ (groups1340683514dd_sum @ TA @ TB @ C @ B)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_245_sum__le__included)).
% 74.58/45.94  thf(1036,plain,((! [TA: $tType,TB: $tType,TC: $tType]: ((ordere216010020id_add @ TB) => (! [A:(set @ TC),B:(set @ TA),C:(TA > TB),D:(TA > TC),E:(TC > TB)]: ((finite_finite2 @ TC @ A) => ((finite_finite2 @ TA @ B) => ((! [F:TA]: ((member @ TA @ F @ B) => (ord_less_eq @ TB @ (zero_zero @ TB) @ (C @ F)))) => ((! [F:TC]: ((member @ TC @ F @ A) => (? [G:TA]: ((member @ TA @ G @ B) & ((D @ G) = F) & (ord_less_eq @ TB @ (E @ F) @ (C @ G)))))) => (ord_less_eq @ TB @ (groups1340683514dd_sum @ TC @ TB @ (E) @ A) @ (groups1340683514dd_sum @ TA @ TB @ (C) @ B)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 74.58/45.94  thf(125,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_61_order__class_Oorder_Oantisym)).
% 74.58/45.94  thf(629,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)],[125])).
% 74.58/45.94  thf(58,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_173_verit__la__disequality)).
% 74.58/45.94  thf(479,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)],[58])).
% 74.58/45.94  thf(327,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_123_order__le__less__subst1)).
% 74.58/45.94  thf(1315,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)],[327])).
% 74.58/45.94  thf(290,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_99_dual__order_Oasym)).
% 74.58/45.94  thf(1179,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)],[290])).
% 74.58/45.94  thf(167,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_178_pinf_I4_J)).
% 74.58/45.94  thf(777,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)],[167])).
% 74.58/45.94  thf(136,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_105_less__imp__triv)).
% 74.58/45.94  thf(666,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)],[136])).
% 74.58/45.94  thf(8,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_67_order_Otrans)).
% 74.58/45.94  thf(365,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)],[8])).
% 74.58/45.94  thf(294,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_order_Ostrict__implies__not__eq)).
% 74.58/45.94  thf(1190,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[294])).
% 74.58/45.94  thf(286,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_179_pinf_I5_J)).
% 74.58/45.94  thf(1168,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)],[286])).
% 74.58/45.94  thf(164,axiom,((! [TA: $tType]: (((ring_char_0 @ TA) & (comm_ring_1 @ TA) & (ring_n68954251visors @ TA)) => (! [A:(poly @ TA)]: ((! [B:TA]: ((poly2 @ TA @ A @ B) = (zero_zero @ TA))) = (A = (zero_zero @ (poly @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_poly__all__0__iff__0)).
% 74.58/45.94  thf(760,plain,((! [TA: $tType]: (((ring_char_0 @ TA) & (comm_ring_1 @ TA) & (ring_n68954251visors @ TA)) => (! [A:(poly @ TA)]: ((! [B:TA]: ((poly2 @ TA @ A @ B) = (zero_zero @ TA))) = (A = (zero_zero @ (poly @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 74.58/45.94  thf(253,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_193_subset__not__subset__eq)).
% 74.58/45.94  thf(1083,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)],[253])).
% 74.58/45.94  thf(53,axiom,((order @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oorder_28)).
% 74.58/45.94  thf(468,plain,((order @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 74.58/45.94  thf(216,axiom,((! [TA: $tType]: ((comm_semiring_0 @ TA) => (! [A:TA]: ((poly2 @ TA @ (zero_zero @ (poly @ TA)) @ A) = (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_poly__0)).
% 74.58/45.94  thf(977,plain,((! [TA: $tType]: ((comm_semiring_0 @ TA) => (! [A:TA]: ((poly2 @ TA @ (zero_zero @ (poly @ TA)) @ A) = (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 74.58/45.94  thf(77,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_74_ord__eq__le__subst)).
% 74.58/45.94  thf(523,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)],[77])).
% 74.58/45.94  thf(273,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_93_less__asym_H)).
% 74.58/45.94  thf(1142,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)],[273])).
% 74.58/45.94  thf(186,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_198_psubsetE)).
% 74.58/45.94  thf(861,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)],[186])).
% 74.58/45.94  thf(157,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_195_psubset__imp__subset)).
% 74.58/45.94  thf(730,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)],[157])).
% 74.58/45.94  thf(322,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_135_dense__ge)).
% 74.58/45.94  thf(1290,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)],[322])).
% 74.58/45.94  thf(297,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_106_linorder__cases)).
% 74.58/45.94  thf(1205,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)],[297])).
% 74.58/45.94  thf(50,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_66_le__cases3)).
% 74.58/45.94  thf(449,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)],[50])).
% 74.58/45.94  thf(46,axiom,((finite_finite @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Finite__Set_Ofinite_27)).
% 74.58/45.94  thf(440,plain,((finite_finite @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 74.58/45.94  thf(132,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_102_less__induct)).
% 74.58/45.94  thf(655,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)],[132])).
% 74.58/45.94  thf(117,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_62_ord__le__eq__trans)).
% 74.58/45.94  thf(614,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)],[117])).
% 74.58/45.94  thf(140,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) = (A != (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_zero__less__iff__neq__zero)).
% 74.58/45.94  thf(677,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) = (~ (A = (zero_zero @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 74.58/45.94  thf(251,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_137_le__less__linear)).
% 74.58/45.94  thf(1078,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)],[251])).
% 74.58/45.94  thf(18,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: (ord_less_eq @ (set @ TA) @ A @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_165_subset__refl)).
% 74.58/45.94  thf(384,plain,((! [TA: $tType]: (! [A:(set @ TA)]: (ord_less_eq @ (set @ TA) @ A @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 74.58/45.94  thf(88,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_71_antisym)).
% 74.58/45.94  thf(550,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)],[88])).
% 74.58/45.94  thf(68,axiom,((preorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Opreorder_25)).
% 74.58/45.94  thf(500,plain,((preorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 74.58/45.94  thf(152,axiom,((! [A:real,B:real,C:(poly @ real)]: ((ord_less @ real @ A @ B) => ((ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ C @ A)) => ((ord_less @ real @ (poly2 @ real @ C @ B) @ (zero_zero @ real)) => (? [D:real]: ((ord_less @ real @ A @ D) & (ord_less @ real @ D @ B) & ((poly2 @ real @ C @ D) = (zero_zero @ real))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_poly__IVT__neg)).
% 74.58/45.94  thf(715,plain,((! [A:real,B:real,C:(poly @ real)]: ((ord_less @ real @ A @ B) => ((ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ C @ A)) => ((ord_less @ real @ (poly2 @ real @ C @ B) @ (zero_zero @ real)) => (? [D:real]: ((ord_less @ real @ A @ D) & (ord_less @ real @ D @ B) & ((poly2 @ real @ C @ D) = (zero_zero @ real))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 74.58/45.94  thf(82,axiom,((ordere216010020id_add @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Oordered__comm__monoid__add_9)).
% 74.58/45.94  thf(538,plain,((ordere216010020id_add @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 74.58/45.94  thf(138,axiom,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TB) => (! [A:(set @ TA),B:TA,C:(TA > TB)]: ((finite_finite2 @ TA @ A) => ((member @ TA @ B @ A) => ((ord_less @ TB @ (zero_zero @ TB) @ (C @ B)) => ((! [D:TA]: ((member @ TA @ D @ A) => (ord_less_eq @ TB @ (zero_zero @ TB) @ (C @ D)))) => (ord_less @ TB @ (zero_zero @ TB) @ (groups1340683514dd_sum @ TA @ TB @ C @ A)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_250_sum__pos2)).
% 74.58/45.94  thf(670,plain,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TB) => (! [A:(set @ TA),B:TA,C:(TA > TB)]: ((finite_finite2 @ TA @ A) => ((member @ TA @ B @ A) => ((ord_less @ TB @ (zero_zero @ TB) @ (C @ B)) => ((! [D:TA]: ((member @ TA @ D @ A) => (ord_less_eq @ TB @ (zero_zero @ TB) @ (C @ D)))) => (ord_less @ TB @ (zero_zero @ TB) @ (groups1340683514dd_sum @ TA @ TB @ (C) @ A)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 74.58/45.94  thf(29,axiom,((ord @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oord_29)).
% 74.58/45.94  thf(404,plain,((ord @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 74.58/45.94  thf(296,axiom,((! [A:real,B:real,C:(poly @ real)]: ((ord_less @ real @ A @ B) => ((! [D:real]: (((ord_less @ real @ A @ D) & (ord_less @ real @ D @ B)) => ((poly2 @ real @ C @ D) != (zero_zero @ real)))) => ((sturm_424270202_cross @ C @ A @ B) = (zero_zero @ int)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_cross__no__root)).
% 74.58/45.94  thf(1196,plain,((! [A:real,B:real,C:(poly @ real)]: ((ord_less @ real @ A @ B) => ((! [D:real]: (((ord_less @ real @ A @ D) & (ord_less @ real @ D @ B)) => (~ ((poly2 @ real @ C @ D) = (zero_zero @ real))))) => ((sturm_424270202_cross @ C @ A @ B) = (zero_zero @ int)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[296])).
% 74.58/45.94  thf(150,axiom,((! [TA: $tType,TB: $tType]: ((canoni770627133id_add @ TB) => (! [A:(set @ TA),B:(TA > TB)]: ((finite_finite2 @ TA @ A) => (((groups1340683514dd_sum @ TA @ TB @ B @ A) = (zero_zero @ TB)) = (! [C:TA]: ((member @ TA @ C @ A) => ((B @ C) = (zero_zero @ TB)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_233_sum__eq__0__iff)).
% 74.58/45.94  thf(709,plain,((! [TA: $tType,TB: $tType]: ((canoni770627133id_add @ TB) => (! [A:(set @ TA),B:(TA > TB)]: ((finite_finite2 @ TA @ A) => (((groups1340683514dd_sum @ TA @ TB @ (B) @ A) = (zero_zero @ TB)) = (! [C:TA]: ((member @ TA @ C @ A) => ((B @ C) = (zero_zero @ TB)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 74.58/45.94  thf(34,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (ordere1818651114id_add @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Groups_Oordered__cancel__comm__monoid__add_50)).
% 74.58/45.94  thf(417,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (ordere1818651114id_add @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 74.58/45.94  thf(44,axiom,((! [TA: $tType]: ((finite_finite @ TA) => (finite_finite @ (set @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Finite__Set_Ofinite_22)).
% 74.58/45.94  thf(436,plain,((! [TA: $tType]: ((finite_finite @ TA) => (finite_finite @ (set @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 74.58/45.94  thf(303,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_82_ord__less__eq__subst)).
% 74.58/45.94  thf(1228,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)],[303])).
% 74.58/45.94  thf(193,axiom,((! [A:int,B:int]: (finite_finite2 @ int @ (collect @ int @ (^ [C:int]: ((ord_less @ int @ A @ C) & (ord_less_eq @ int @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_213_finite__interval__int3)).
% 74.58/45.94  thf(885,plain,((! [A:int,B:int]: (finite_finite2 @ int @ (collect @ int @ (^ [C:int]: ((ord_less @ int @ A @ C) & (ord_less_eq @ int @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 74.58/45.94  thf(239,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (ord_less_eq @ TA @ (zero_zero @ TA) @ (zero_zero @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_le__numeral__extra_I3_J)).
% 74.58/45.94  thf(1046,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (ord_less_eq @ TA @ (zero_zero @ TA) @ (zero_zero @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 74.58/45.94  thf(95,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_161_subset__eq)).
% 74.58/45.94  thf(565,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)],[95])).
% 74.58/45.94  thf(343,axiom,((! [TA: $tType]: ((linordered_field @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) => ((ord_less @ TA @ (zero_zero @ TA) @ B) => (? [C:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ C) & (ord_less @ TA @ C @ A) & (ord_less @ TA @ C @ B))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_118_field__lbound__gt__zero)).
% 74.58/45.94  thf(1366,plain,((! [TA: $tType]: ((linordered_field @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) => ((ord_less @ TA @ (zero_zero @ TA) @ B) => (? [C:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ C) & (ord_less @ TA @ C @ A) & (ord_less @ TA @ C @ B))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[343])).
% 74.58/45.94  thf(21,axiom,((linorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Olinorder_15)).
% 74.58/45.94  thf(389,plain,((linorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 74.58/45.94  thf(97,axiom,((comm_monoid_add @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocomm__monoid__add_10)).
% 74.58/45.94  thf(570,plain,((comm_monoid_add @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 74.58/45.94  thf(13,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_157_subset__antisym)).
% 74.58/45.94  thf(372,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)],[13])).
% 74.58/45.94  thf(314,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_177_pinf_I3_J)).
% 74.58/45.94  thf(1264,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)],[314])).
% 74.58/45.94  thf(329,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_131_antisym__conv2)).
% 74.58/45.94  thf(1323,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)],[329])).
% 74.58/45.94  thf(176,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_143_order_Oorder__iff__strict)).
% 74.58/45.94  thf(802,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)],[176])).
% 74.58/45.94  thf(244,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_43_dual__order_Oorder__iff__strict)).
% 74.58/45.94  thf(1059,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)],[244])).
% 74.58/45.94  thf(200,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_124_order__le__less__subst2)).
% 74.58/45.94  thf(902,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)],[200])).
% 74.58/45.94  thf(183,axiom,((one @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Oone_49)).
% 74.58/45.94  thf(853,plain,((one @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 74.58/45.94  thf(347,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_142_order_Ostrict__trans2)).
% 74.58/45.94  thf(1379,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)],[347])).
% 74.58/45.94  thf(276,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_120_leI)).
% 74.58/45.94  thf(1147,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)],[276])).
% 74.58/45.94  thf(230,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_89_order_Oasym)).
% 74.58/45.94  thf(1013,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)],[230])).
% 74.58/45.94  thf(192,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_90_dense)).
% 74.58/45.94  thf(881,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)],[192])).
% 74.58/45.94  thf(328,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_115_dual__order_Ostrict__implies__not__eq)).
% 74.58/45.94  thf(1319,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[328])).
% 74.58/45.94  thf(37,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (linord1659791738miring @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Rings_Olinordered__nonzero__semiring_51)).
% 74.58/45.94  thf(421,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (linord1659791738miring @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 74.58/45.94  thf(112,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_72_eq__iff)).
% 74.58/45.94  thf(606,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)],[112])).
% 74.58/45.94  thf(336,axiom,((! [TA: $tType]: ((zero @ TA) => (! [A:TA]: (((zero_zero @ TA) = A) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_zero__reorient)).
% 74.58/45.94  thf(1347,plain,((! [TA: $tType]: ((zero @ TA) => (! [A:TA]: (((zero_zero @ TA) = A) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[336])).
% 74.58/45.94  thf(48,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($true) @ A @ B) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_1_1_T)).
% 74.58/45.94  thf(443,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($true) @ A @ B) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 74.58/45.94  thf(74,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_65_antisym__conv)).
% 74.58/45.94  thf(514,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)],[74])).
% 74.58/45.94  thf(100,axiom,((ord @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Oord_5)).
% 74.58/45.94  thf(574,plain,((ord @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 74.58/45.94  thf(241,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_188_minf_I11_J)).
% 74.58/45.94  thf(1051,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 74.58/45.94  thf(62,axiom,((! [A:int,B:int]: ((ord_less_eq @ int @ A @ B) | (A = B) | (ord_less_eq @ int @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_verit__la__generic)).
% 74.58/45.94  thf(485,plain,((! [A:int,B:int]: ((ord_less_eq @ int @ A @ B) | (A = B) | (ord_less_eq @ int @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 74.58/45.94  thf(269,axiom,((! [TA: $tType]: ((zero_less_one @ TA) => (ord_less @ TA @ (zero_zero @ TA) @ (one_one @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_252_zero__less__one)).
% 74.58/45.94  thf(1136,plain,((! [TA: $tType]: ((zero_less_one @ TA) => (ord_less @ TA @ (zero_zero @ TA) @ (one_one @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[269])).
% 74.58/45.94  thf(278,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: ((comm_monoid_add @ TC) => (! [A:(set @ TB),B:(set @ TA),C:(TB > (TA > TC)),D:(TB > (TA > $o))]: ((finite_finite2 @ TB @ A) => ((finite_finite2 @ TA @ B) => ((groups1340683514dd_sum @ TB @ TC @ (^ [E:TB]: (groups1340683514dd_sum @ TA @ TC @ (C @ E) @ (collect @ TA @ (^ [F:TA]: ((member @ TA @ F @ B) & (D @ E @ F)))))) @ A) = (groups1340683514dd_sum @ TA @ TC @ (^ [E:TA]: (groups1340683514dd_sum @ TB @ TC @ (^ [F:TB]: (C @ F @ E)) @ (collect @ TB @ (^ [F:TB]: ((member @ TB @ F @ A) & (D @ F @ E)))))) @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_240_sum_Oswap__restrict)).
% 74.58/45.94  thf(1151,plain,((! [TA: $tType,TB: $tType,TC: $tType]: ((comm_monoid_add @ TC) => (! [A:(set @ TB),B:(set @ TA),C:(TB > (TA > TC)),D:(TB > (TA > $o))]: ((finite_finite2 @ TB @ A) => ((finite_finite2 @ TA @ B) => ((groups1340683514dd_sum @ TB @ TC @ (^ [E:TB]: (groups1340683514dd_sum @ TA @ TC @ (C @ E) @ (collect @ TA @ (^ [F:TA]: ((member @ TA @ F @ B) & (D @ E @ F)))))) @ A) = (groups1340683514dd_sum @ TA @ TC @ (^ [E:TA]: (groups1340683514dd_sum @ TB @ TC @ (^ [F:TB]: (C @ F @ E)) @ (collect @ TB @ (^ [F:TB]: ((member @ TB @ F @ A) & (D @ F @ E)))))) @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[278])).
% 74.58/45.94  thf(206,axiom,((! [TA: $tType,TB: $tType]: ((ordere1818651114id_add @ TB) => (! [A:(TA > TB),B:(set @ TA),C:(TA > TB),D:TA]: (((groups1340683514dd_sum @ TA @ TB @ A @ B) = (groups1340683514dd_sum @ TA @ TB @ C @ B)) => ((! [E:TA]: ((member @ TA @ E @ B) => (ord_less_eq @ TB @ (A @ E) @ (C @ E)))) => ((member @ TA @ D @ B) => ((finite_finite2 @ TA @ B) => ((A @ D) = (C @ D)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_243_sum__mono__inv)).
% 74.58/45.94  thf(937,plain,((! [TA: $tType,TB: $tType]: ((ordere1818651114id_add @ TB) => (! [A:(TA > TB),B:(set @ TA),C:(TA > TB),D:TA]: (((groups1340683514dd_sum @ TA @ TB @ (A) @ B) = (groups1340683514dd_sum @ TA @ TB @ (C) @ B)) => ((! [E:TA]: ((member @ TA @ E @ B) => (ord_less_eq @ TB @ (A @ E) @ (C @ E)))) => ((member @ TA @ D @ B) => ((finite_finite2 @ TA @ B) => ((A @ D) = (C @ D)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 74.58/45.94  thf(1,conjecture,((finite_finite2 @ real @ (collect @ real @ (^ [A:real]: (((poly2 @ real @ p @ A) = (zero_zero @ real)) & (ord_less @ real @ a @ A) & (ord_less @ real @ A @ b)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 74.58/45.94  thf(2,negated_conjecture,((~ (finite_finite2 @ real @ (collect @ real @ (^ [A:real]: (((poly2 @ real @ p @ A) = (zero_zero @ real)) & (ord_less @ real @ a @ A) & (ord_less @ real @ A @ b))))))),inference(neg_conjecture,[status(cth)],[1])).
% 74.58/45.94  thf(353,plain,((~ (finite_finite2 @ real @ (collect @ real @ (^ [A:real]: (((poly2 @ real @ p @ A) = (zero_zero @ real)) & (ord_less @ real @ a @ A) & (ord_less @ real @ A @ b))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 74.58/45.94  thf(213,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_less__imp__not__eq)).
% 74.58/45.94  thf(966,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 74.58/45.94  thf(346,axiom,((! [A:int,B:int]: (finite_finite2 @ int @ (collect @ int @ (^ [C:int]: ((ord_less_eq @ int @ A @ C) & (ord_less @ int @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_211_finite__interval__int2)).
% 74.58/45.94  thf(1377,plain,((! [A:int,B:int]: (finite_finite2 @ int @ (collect @ int @ (^ [C:int]: ((ord_less_eq @ int @ A @ C) & (ord_less @ int @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[346])).
% 74.58/45.94  thf(210,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_147_dense__ge__bounded)).
% 74.58/45.94  thf(956,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)],[210])).
% 74.58/45.94  thf(24,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (linorder @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Orderings_Olinorder_60)).
% 74.58/45.94  thf(396,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (linorder @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 74.58/45.94  thf(223,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_dual__order_Oirrefl)).
% 74.58/45.94  thf(998,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 74.58/45.94  thf(40,axiom,((condit1037483654norder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Conditionally__Complete__Lattices_Oconditionally__complete__linorder_6)).
% 74.58/45.94  thf(428,plain,((condit1037483654norder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 74.58/45.94  thf(261,axiom,((! [TA: $tType]: (! [A:(TA > $o)]: ((~ (finite_finite2 @ TA @ (collect @ TA @ A))) => (? [B:TA]: (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_not__finite__existsD)).
% 74.58/45.94  thf(1104,plain,((! [TA: $tType]: (! [A:(TA > $o)]: ((~ (finite_finite2 @ TA @ (collect @ TA @ (A)))) => (? [B:TA]: (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[261])).
% 74.58/45.94  thf(71,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_78_le__funI)).
% 74.58/45.94  thf(507,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)],[71])).
% 74.58/45.94  thf(250,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__neq)).
% 74.58/45.94  thf(1074,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 74.58/45.94  thf(73,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_209_rev__predicate1D)).
% 74.58/45.94  thf(512,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)],[73])).
% 74.58/45.94  thf(133,axiom,((ring_char_0 @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Nat_Oring__char__0_46)).
% 74.58/45.94  thf(661,plain,((ring_char_0 @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 74.58/45.94  thf(172,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_187_minf_I7_J)).
% 74.58/45.94  thf(793,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)],[172])).
% 74.58/45.94  thf(16,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_158_in__mono)).
% 74.58/45.94  thf(381,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)],[16])).
% 74.58/45.94  thf(247,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (ord_less @ TA @ (zero_zero @ TA) @ (one_one @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_227_less__numeral__extra_I1_J)).
% 74.58/45.94  thf(1067,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (ord_less @ TA @ (zero_zero @ TA) @ (one_one @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[247])).
% 74.58/45.94  thf(174,axiom,((! [TA: $tType]: ((finite_finite @ TA) => (! [A:(set @ TA)]: (finite_finite2 @ TA @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_finite)).
% 74.58/45.94  thf(798,plain,((! [TA: $tType]: ((finite_finite @ TA) => (! [A:(set @ TA)]: (finite_finite2 @ TA @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 74.58/45.94  thf(283,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_less__irrefl)).
% 74.58/45.94  thf(1163,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[283])).
% 74.58/45.94  thf(316,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_126_order__less__le__subst2)).
% 74.58/45.94  thf(1274,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)],[316])).
% 74.58/45.94  thf(350,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_141_order_Ostrict__trans1)).
% 74.58/45.94  thf(1387,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)],[350])).
% 74.58/45.94  thf(197,axiom,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_lt__ex)).
% 74.58/45.94  thf(894,plain,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 74.58/45.94  thf(311,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_gr__implies__not__zero)).
% 74.58/45.94  thf(1255,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = (zero_zero @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[311])).
% 74.58/45.94  thf(300,axiom,((! [A:real,B:real,C:(poly @ real)]: ((ord_less @ real @ A @ B) => ((ord_less @ real @ (poly2 @ real @ C @ A) @ (zero_zero @ real)) => ((ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ C @ B)) => (? [D:real]: ((ord_less @ real @ A @ D) & (ord_less @ real @ D @ B) & ((poly2 @ real @ C @ D) = (zero_zero @ real))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_poly__IVT__pos)).
% 74.58/45.94  thf(1217,plain,((! [A:real,B:real,C:(poly @ real)]: ((ord_less @ real @ A @ B) => ((ord_less @ real @ (poly2 @ real @ C @ A) @ (zero_zero @ real)) => ((ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ C @ B)) => (? [D:real]: ((ord_less @ real @ A @ D) & (ord_less @ real @ D @ B) & ((poly2 @ real @ C @ D) = (zero_zero @ real))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[300])).
% 74.58/45.94  thf(94,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_69_eq__refl)).
% 74.58/45.94  thf(561,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)],[94])).
% 74.58/45.94  thf(41,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_170_less__eq__set__def)).
% 74.58/45.94  thf(429,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)],[41])).
% 74.58/45.94  thf(170,axiom,((! [A:real,B:real,C:(poly @ real)]: ((sturm_1539314049x_poly @ A @ B @ C @ (zero_zero @ (poly @ real))) = (zero_zero @ int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_217_cindex__poly__0_I2_J)).
% 74.58/45.94  thf(788,plain,((! [A:real,B:real,C:(poly @ real)]: ((sturm_1539314049x_poly @ A @ B @ C @ (zero_zero @ (poly @ real))) = (zero_zero @ int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 74.58/45.94  thf(305,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((finite_finite2 @ TA @ B) => (finite_finite2 @ TA @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_finite__subset)).
% 74.58/45.94  thf(1238,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((finite_finite2 @ TA @ B) => (finite_finite2 @ TA @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[305])).
% 74.58/45.94  thf(202,axiom,((! [A:(set @ real)]: ((? [B:real]: (member @ real @ B @ A)) => ((? [B:real]: ! [C:real]: ((member @ real @ C @ A) => (ord_less_eq @ real @ C @ B))) => (? [B:real]: (! [C:real]: ((member @ real @ C @ A) => (ord_less_eq @ real @ C @ B)) & ! [C:real]: ((! [D:real]: ((member @ real @ D @ A) => (ord_less_eq @ real @ D @ C))) => (ord_less_eq @ real @ B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_117_complete__real)).
% 74.58/45.94  thf(916,plain,((! [A:(set @ real)]: ((? [B:real]: (member @ real @ B @ A)) => ((? [B:real]: ! [C:real]: ((member @ real @ C @ A) => (ord_less_eq @ real @ C @ B))) => (? [B:real]: (! [C:real]: ((member @ real @ C @ A) => (ord_less_eq @ real @ C @ B)) & ! [C:real]: ((! [D:real]: ((member @ real @ D @ A) => (ord_less_eq @ real @ D @ C))) => (ord_less_eq @ real @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 74.58/45.94  thf(61,axiom,((preorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Opreorder_14)).
% 74.58/45.94  thf(484,plain,((preorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 74.58/45.94  thf(5,axiom,((one @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Oone)).
% 74.58/45.94  thf(361,plain,((one @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 74.58/45.94  thf(122,axiom,((condit1037483654norder @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Conditionally__Complete__Lattices_Oconditionally__complete__linorder)).
% 74.58/45.94  thf(625,plain,((condit1037483654norder @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 74.58/45.94  thf(182,axiom,((preorder @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Opreorder_40)).
% 74.58/45.94  thf(852,plain,((preorder @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 74.58/45.94  thf(289,axiom,((condit1656338222tinuum @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Conditionally__Complete__Lattices_Olinear__continuum)).
% 74.58/45.94  thf(1178,plain,((condit1656338222tinuum @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[289])).
% 74.58/45.94  thf(195,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_le__imp__less__or__eq)).
% 74.58/45.94  thf(889,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)],[195])).
% 74.58/45.94  thf(282,axiom,((! [A:(poly @ real),B:real,C:(poly @ real)]: (((poly2 @ real @ A @ B) != (zero_zero @ real)) => ((sturm_652470720p_poly @ C @ A @ B) = (zero_zero @ int))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_jump__poly__not__root)).
% 74.58/45.94  thf(1159,plain,((! [A:(poly @ real),B:real,C:(poly @ real)]: ((~ ((poly2 @ real @ A @ B) = (zero_zero @ real))) => ((sturm_652470720p_poly @ C @ A @ B) = (zero_zero @ int))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[282])).
% 74.58/45.94  thf(65,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($false) @ A @ B) = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_2_1_T)).
% 74.58/45.94  thf(493,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($false) @ A @ B) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 74.58/45.94  thf(234,axiom,((no_bot @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Ono__bot_44)).
% 74.58/45.94  thf(1027,plain,((no_bot @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[234])).
% 74.58/45.94  thf(163,axiom,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TA) => (! [A:(set @ TB)]: ((groups1340683514dd_sum @ TB @ TA @ (^ [B:TB]: (zero_zero @ TA)) @ A) = (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_sum_Oneutral__const)).
% 74.58/45.94  thf(757,plain,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TA) => (! [A:(set @ TB)]: ((groups1340683514dd_sum @ TB @ TA @ (^ [B:TB]: (zero_zero @ TA)) @ A) = (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 74.58/45.94  thf(142,axiom,((! [A:int,B:int]: (finite_finite2 @ int @ (collect @ int @ (^ [C:int]: ((ord_less @ int @ A @ C) & (ord_less @ int @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_212_finite__interval__int4)).
% 74.58/45.94  thf(682,plain,((! [A:int,B:int]: (finite_finite2 @ int @ (collect @ int @ (^ [C:int]: ((ord_less @ int @ A @ C) & (ord_less @ int @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 74.58/45.94  thf(215,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: ((A != (zero_zero @ TA)) => (ord_less @ TA @ (zero_zero @ TA) @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_gr__zeroI)).
% 74.58/45.94  thf(974,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: ((~ (A = (zero_zero @ TA))) => (ord_less @ TA @ (zero_zero @ TA) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 74.58/45.94  thf(229,axiom,((idom @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Oidom_1)).
% 74.58/45.94  thf(1012,plain,((idom @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 74.58/45.94  thf(262,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_41_dual__order_Ostrict__implies__order)).
% 74.58/45.94  thf(1106,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)],[262])).
% 74.58/45.94  thf(312,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_153_verit__comp__simplify1_I3_J)).
% 74.58/45.94  thf(1259,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)],[312])).
% 74.58/45.94  thf(264,axiom,((finite_finite2 @ real @ (collect @ real @ (^ [A:real]: ((poly2 @ real @ p @ A) = (zero_zero @ real)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0__092_060open_062finite_A_123x_O_Apoly_Ap_Ax_A_061_A0_125_092_060close_062)).
% 74.58/45.94  thf(1111,plain,((finite_finite2 @ real @ (collect @ real @ (^ [A:real]: ((poly2 @ real @ p @ A) = (zero_zero @ real)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[264])).
% 74.58/45.94  thf(217,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_152_pinf_I6_J)).
% 74.58/45.94  thf(980,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)],[217])).
% 74.58/45.94  thf(258,axiom,((! [A:real,B:real,C:(poly @ real)]: ((! [D:real]: (((ord_less @ real @ A @ D) & (ord_less_eq @ real @ D @ B)) => ((poly2 @ real @ C @ D) != (zero_zero @ real)))) = (! [D:real]: (((ord_less @ real @ A @ D) & (ord_less_eq @ real @ D @ B)) => (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ C @ D))) | ! [D:real]: (((ord_less @ real @ A @ D) & (ord_less_eq @ real @ D @ B)) => (ord_less @ real @ (poly2 @ real @ C @ D) @ (zero_zero @ real))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_not__eq__pos__or__neg__iff__1)).
% 74.58/45.94  thf(1096,plain,((! [A:real,B:real,C:(poly @ real)]: ((! [D:real]: (((ord_less @ real @ A @ D) & (ord_less_eq @ real @ D @ B)) => (~ ((poly2 @ real @ C @ D) = (zero_zero @ real))))) = (! [D:real]: (((ord_less @ real @ A @ D) & (ord_less_eq @ real @ D @ B)) => (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ C @ D))) | ! [D:real]: (((ord_less @ real @ A @ D) & (ord_less_eq @ real @ D @ B)) => (ord_less @ real @ (poly2 @ real @ C @ D) @ (zero_zero @ real))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[258])).
% 74.58/45.94  thf(226,axiom,((! [A:real,B:real,C:(poly @ real)]: ((! [D:real]: (((ord_less_eq @ real @ A @ D) & (ord_less @ real @ D @ B)) => ((poly2 @ real @ C @ D) != (zero_zero @ real)))) = (! [D:real]: (((ord_less_eq @ real @ A @ D) & (ord_less @ real @ D @ B)) => (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ C @ D))) | ! [D:real]: (((ord_less_eq @ real @ A @ D) & (ord_less @ real @ D @ B)) => (ord_less @ real @ (poly2 @ real @ C @ D) @ (zero_zero @ real))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_not__eq__pos__or__neg__iff__2)).
% 74.58/45.94  thf(1006,plain,((! [A:real,B:real,C:(poly @ real)]: ((! [D:real]: (((ord_less_eq @ real @ A @ D) & (ord_less @ real @ D @ B)) => (~ ((poly2 @ real @ C @ D) = (zero_zero @ real))))) = (! [D:real]: (((ord_less_eq @ real @ A @ D) & (ord_less @ real @ D @ B)) => (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ C @ D))) | ! [D:real]: (((ord_less_eq @ real @ A @ D) & (ord_less @ real @ D @ B)) => (ord_less @ real @ (poly2 @ real @ C @ D) @ (zero_zero @ real))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 74.58/45.94  thf(270,axiom,((ord_less_eq @ int @ (zero_zero @ int) @ (zero_zero @ int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_less__eq__int__code_I1_J)).
% 74.58/45.94  thf(1138,plain,((ord_less_eq @ int @ (zero_zero @ int) @ (zero_zero @ int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[270])).
% 74.58/45.94  thf(189,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_132_less__imp__le)).
% 74.58/45.94  thf(869,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)],[189])).
% 74.58/45.94  thf(114,axiom,((ordere216010020id_add @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Oordered__comm__monoid__add)).
% 74.58/45.94  thf(610,plain,((ordere216010020id_add @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 74.58/45.94  thf(36,axiom,((order @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Oorder_4)).
% 74.58/45.94  thf(420,plain,((order @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 74.58/45.94  thf(340,axiom,((order @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Oorder_45)).
% 74.58/45.94  thf(1360,plain,((order @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[340])).
% 74.58/45.94  thf(337,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_196_psubset__trans)).
% 74.58/45.94  thf(1350,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)],[337])).
% 74.58/45.94  thf(76,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_76_order__subst1)).
% 74.58/45.94  thf(519,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)],[76])).
% 74.58/45.94  thf(103,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_60_order__trans)).
% 74.58/45.94  thf(578,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)],[103])).
% 74.58/45.94  thf(147,axiom,((! [A:(poly @ real),B:real]: ((sturm_652470720p_poly @ (zero_zero @ (poly @ real)) @ A @ B) = (zero_zero @ int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_jump__poly0_I1_J)).
% 74.58/45.94  thf(697,plain,((! [A:(poly @ real),B:real]: ((sturm_652470720p_poly @ (zero_zero @ (poly @ real)) @ A @ B) = (zero_zero @ int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 74.58/45.94  thf(255,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_83_order__less__subst1)).
% 74.58/45.94  thf(1089,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)],[255])).
% 74.58/45.94  thf(55,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (ord @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Orderings_Oord_64)).
% 74.58/45.94  thf(471,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (ord @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 74.58/45.94  thf(331,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_148_psubsetI)).
% 74.58/45.94  thf(1329,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)],[331])).
% 74.58/45.94  thf(235,axiom,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TA) => (! [A:(set @ TB),B:(TB > TA),C:TB]: ((finite_finite2 @ TB @ A) => ((! [D:TB]: ((member @ TB @ D @ A) => (ord_less_eq @ TA @ (zero_zero @ TA) @ (B @ D)))) => (((groups1340683514dd_sum @ TB @ TA @ B @ A) = (zero_zero @ TA)) => ((member @ TB @ C @ A) => ((B @ C) = (zero_zero @ TA)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_248_sum__nonneg__0)).
% 74.58/45.94  thf(1028,plain,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TA) => (! [A:(set @ TB),B:(TB > TA),C:TB]: ((finite_finite2 @ TB @ A) => ((! [D:TB]: ((member @ TB @ D @ A) => (ord_less_eq @ TA @ (zero_zero @ TA) @ (B @ D)))) => (((groups1340683514dd_sum @ TB @ TA @ (B) @ A) = (zero_zero @ TA)) => ((member @ TB @ C @ A) => ((B @ C) = (zero_zero @ TA)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 74.58/45.94  thf(63,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_167_subset__trans)).
% 74.58/45.94  thf(488,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)],[63])).
% 74.58/45.94  thf(341,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_129_le__neq__trans)).
% 74.58/45.94  thf(1361,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)],[341])).
% 74.58/45.94  thf(204,axiom,((! [TA: $tType]: (((ring_char_0 @ TA) & (comm_ring_1 @ TA) & (ring_n68954251visors @ TA)) => (! [A:(poly @ TA),B:(poly @ TA)]: (((poly2 @ TA @ A) = (poly2 @ TA @ B)) = (A = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_poly__eq__poly__eq__iff)).
% 74.58/45.94  thf(933,plain,((! [TA: $tType]: (((ring_char_0 @ TA) & (comm_ring_1 @ TA) & (ring_n68954251visors @ TA)) => (! [A:(poly @ TA),B:(poly @ TA)]: (((poly2 @ TA @ A) = (poly2 @ TA @ B)) = (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 74.58/45.94  thf(81,axiom,((! [A:$o]: ((A = ($true)) | (A = ($false))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_3_1_T)).
% 74.58/45.94  thf(537,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 74.58/45.94  thf(128,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_200_less__set__def)).
% 74.58/45.94  thf(637,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)],[128])).
% 74.58/45.94  thf(299,axiom,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TB) => (! [A:(set @ TA),B:(TA > TB),C:(TA > $o)]: ((finite_finite2 @ TA @ A) => ((groups1340683514dd_sum @ TA @ TB @ B @ (collect @ TA @ (^ [D:TA]: ((member @ TA @ D @ A) & (C @ D))))) = (groups1340683514dd_sum @ TA @ TB @ (^ [D:TA]: (if @ TB @ (C @ D) @ (B @ D) @ (zero_zero @ TB))) @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_244_sum_Ointer__filter)).
% 74.58/45.94  thf(1214,plain,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TB) => (! [A:(set @ TA),B:(TA > TB),C:(TA > $o)]: ((finite_finite2 @ TA @ A) => ((groups1340683514dd_sum @ TA @ TB @ (B) @ (collect @ TA @ (^ [D:TA]: ((member @ TA @ D @ A) & (C @ D))))) = (groups1340683514dd_sum @ TA @ TB @ (^ [D:TA]: (if @ TB @ (C @ D) @ (B @ D) @ (zero_zero @ TB))) @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[299])).
% 74.58/45.94  thf(106,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_57_dual__order_Otrans)).
% 74.58/45.94  thf(590,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)],[106])).
% 74.58/45.94  thf(214,axiom,((! [TA: $tType,TB: $tType]: ((ordere1818651114id_add @ TB) => (! [A:(set @ TA),B:(TA > TB),C:(TA > TB)]: ((finite_finite2 @ TA @ A) => ((! [D:TA]: ((member @ TA @ D @ A) => (ord_less_eq @ TB @ (B @ D) @ (C @ D)))) => ((? [D:TA]: ((member @ TA @ D @ A) & (ord_less @ TB @ (B @ D) @ (C @ D)))) => (ord_less @ TB @ (groups1340683514dd_sum @ TA @ TB @ B @ A) @ (groups1340683514dd_sum @ TA @ TB @ C @ A))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_247_sum__strict__mono__ex1)).
% 74.58/45.94  thf(970,plain,((! [TA: $tType,TB: $tType]: ((ordere1818651114id_add @ TB) => (! [A:(set @ TA),B:(TA > TB),C:(TA > TB)]: ((finite_finite2 @ TA @ A) => ((! [D:TA]: ((member @ TA @ D @ A) => (ord_less_eq @ TB @ (B @ D) @ (C @ D)))) => ((? [D:TA]: ((member @ TA @ D @ A) & (ord_less @ TB @ (B @ D) @ (C @ D)))) => (ord_less @ TB @ (groups1340683514dd_sum @ TA @ TB @ (B) @ A) @ (groups1340683514dd_sum @ TA @ TB @ (C) @ A))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 74.58/45.94  thf(280,axiom,(((ord_less_eq @ real) = (^ [A:real,B:real]: ((ord_less @ real @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_less__eq__real__def)).
% 74.58/45.94  thf(1155,plain,(((ord_less_eq @ real) = (^ [A:real,B:real]: ((ord_less @ real @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[280])).
% 74.58/45.94  thf(23,axiom,((! [TA: $tType]: ((one @ TA) => (! [A:TA]: (((one_one @ TA) = A) = (A = (one_one @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_226_one__reorient)).
% 74.58/45.94  thf(393,plain,((! [TA: $tType]: ((one @ TA) => (! [A:TA]: (((one_one @ TA) = A) = (A = (one_one @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 74.58/45.94  thf(309,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_88_neq__iff)).
% 74.58/45.94  thf(1249,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)],[309])).
% 74.58/45.94  thf(159,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_175_pinf_I1_J)).
% 74.58/45.94  thf(738,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)],[159])).
% 74.58/45.94  thf(267,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_169_Collect__subset)).
% 74.58/45.94  thf(1131,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)],[267])).
% 74.58/45.94  thf(111,axiom,((idom @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Oidom_2)).
% 74.58/45.94  thf(605,plain,((idom @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 74.58/45.94  thf(120,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_order__refl)).
% 74.58/45.94  thf(622,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 74.58/45.94  thf(180,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:((set @ TA) > $o)]: ((finite_finite2 @ TA @ A) => ((! [C:(set @ TA)]: ((finite_finite2 @ TA @ C) => ((! [D:(set @ TA)]: ((ord_less @ (set @ TA) @ D @ C) => (B @ D))) => (B @ C)))) => (B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_finite__psubset__induct)).
% 74.58/45.94  thf(837,plain,((! [TA: $tType]: (! [A:(set @ TA),B:((set @ TA) > $o)]: ((finite_finite2 @ TA @ A) => ((! [C:(set @ TA)]: ((finite_finite2 @ TA @ C) => ((! [D:(set @ TA)]: ((ord_less @ (set @ TA) @ D @ C) => (B @ D))) => (B @ C)))) => (B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 74.58/45.94  thf(259,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_122_less__le)).
% 74.58/45.94  thf(1099,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)],[259])).
% 74.58/45.94  thf(219,axiom,((zero @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Ozero_48)).
% 74.58/45.94  thf(985,plain,((zero @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 74.58/45.94  thf(333,axiom,((! [A:(poly @ real),B:real]: ((A != (zero_zero @ (poly @ real))) => (~ (! [C:real]: ((ord_less @ real @ B @ C) => (~ (! [D:real]: (((ord_less @ real @ B @ D) & (ord_less_eq @ real @ D @ C)) => ((poly2 @ real @ A @ D) != (zero_zero @ real))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_next__non__root__interval)).
% 74.58/45.94  thf(1333,plain,((! [A:(poly @ real),B:real]: ((~ (A = (zero_zero @ (poly @ real)))) => (~ (! [C:real]: ((ord_less @ real @ B @ C) => (~ (! [D:real]: (((ord_less @ real @ B @ D) & (ord_less_eq @ real @ D @ C)) => (~ ((poly2 @ real @ A @ D) = (zero_zero @ real)))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[333])).
% 74.58/45.94  thf(254,axiom,((! [A:real,B:real]: ((sturm_424270202_cross @ (zero_zero @ (poly @ real)) @ A @ B) = (zero_zero @ int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_cross__0)).
% 74.58/45.94  thf(1086,plain,((! [A:real,B:real]: ((sturm_424270202_cross @ (zero_zero @ (poly @ real)) @ A @ B) = (zero_zero @ int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[254])).
% 74.58/45.94  thf(307,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_166_Collect__mono)).
% 74.58/45.94  thf(1241,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)],[307])).
% 74.58/45.94  thf(4,axiom,((one @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Oone_20)).
% 74.58/45.94  thf(360,plain,((one @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 74.58/45.94  thf(177,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((finite_finite2 @ TA @ A) => ((ord_less_eq @ (set @ TA) @ B @ A) => (finite_finite2 @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_rev__finite__subset)).
% 74.58/45.94  thf(805,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((finite_finite2 @ TA @ A) => ((ord_less_eq @ (set @ TA) @ B @ A) => (finite_finite2 @ TA @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 74.58/45.94  thf(287,axiom,((! [A:(poly @ real),B:real]: ((A != (zero_zero @ (poly @ real))) => (~ (! [C:real]: ((ord_less @ real @ C @ B) => (~ (! [D:real]: (((ord_less_eq @ real @ C @ D) & (ord_less @ real @ D @ B)) => ((poly2 @ real @ A @ D) != (zero_zero @ real))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_last__non__root__interval)).
% 74.58/45.94  thf(1170,plain,((! [A:(poly @ real),B:real]: ((~ (A = (zero_zero @ (poly @ real)))) => (~ (! [C:real]: ((ord_less @ real @ C @ B) => (~ (! [D:real]: (((ord_less_eq @ real @ C @ D) & (ord_less @ real @ D @ B)) => (~ ((poly2 @ real @ A @ D) = (zero_zero @ real)))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[287])).
% 74.58/45.94  thf(285,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_181_pinf_I11_J)).
% 74.58/45.94  thf(1167,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[285])).
% 74.58/45.94  thf(209,axiom,((! [TA: $tType]: ((finite_finite @ TA) => ((finite_finite2 @ TA) = (^ [A:(set @ TA)]: (($true))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_finite__code)).
% 74.58/45.94  thf(953,plain,((! [TA: $tType]: ((finite_finite @ TA) => ((finite_finite2 @ TA) = (^ [A:(set @ TA)]: (($true))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 74.58/45.94  thf(166,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: (((finite_finite2 @ TA @ (collect @ TA @ A)) | (finite_finite2 @ TA @ (collect @ TA @ B))) => (finite_finite2 @ TA @ (collect @ TA @ (^ [C:TA]: ((A @ C) & (B @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_finite__Collect__conjI)).
% 74.58/45.94  thf(773,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: (((finite_finite2 @ TA @ (collect @ TA @ (A))) | (finite_finite2 @ TA @ (collect @ TA @ (B)))) => (finite_finite2 @ TA @ (collect @ TA @ (^ [C:TA]: ((A @ C) & (B @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 74.58/45.94  thf(134,axiom,((comm_semiring_0 @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Ocomm__semiring__0_38)).
% 74.58/45.94  thf(662,plain,((comm_semiring_0 @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 74.58/45.94  thf(203,axiom,((! [TA: $tType]: ((comm_semiring_1 @ TA) => (! [A:nat]: (((A = (zero_zero @ nat)) => ((poly_cutoff @ TA @ A @ (one_one @ (poly @ TA))) = (zero_zero @ (poly @ TA)))) & ((A != (zero_zero @ nat)) => ((poly_cutoff @ TA @ A @ (one_one @ (poly @ TA))) = (one_one @ (poly @ TA))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_223_poly__cutoff__1)).
% 74.58/45.94  thf(926,plain,((! [TA: $tType]: ((comm_semiring_1 @ TA) => (! [A:nat]: (((A = (zero_zero @ nat)) => ((poly_cutoff @ TA @ A @ (one_one @ (poly @ TA))) = (zero_zero @ (poly @ TA)))) & ((~ (A = (zero_zero @ nat))) => ((poly_cutoff @ TA @ A @ (one_one @ (poly @ TA))) = (one_one @ (poly @ TA))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 74.58/45.94  thf(320,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_119_leD)).
% 74.58/45.94  thf(1286,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)],[320])).
% 74.58/45.94  thf(25,axiom,((! [TA: $tType]: ((comm_semiring_1 @ TA) => (one @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Groups_Oone_66)).
% 74.58/45.94  thf(398,plain,((! [TA: $tType]: ((comm_semiring_1 @ TA) => (one @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 74.58/45.94  thf(92,axiom,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Opreorder)).
% 74.58/45.94  thf(558,plain,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 74.58/45.94  thf(249,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_130_antisym__conv1)).
% 74.58/45.94  thf(1071,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)],[249])).
% 74.58/45.94  thf(293,axiom,((! [TA: $tType]: ((zero @ TA) => ((is_zero @ TA) = (^ [A:(poly @ TA)]: (A = (zero_zero @ (poly @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_154_is__zero__null)).
% 74.58/45.94  thf(1187,plain,((! [TA: $tType]: ((zero @ TA) => ((is_zero @ TA) = (^ [A:(poly @ TA)]: (A = (zero_zero @ (poly @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[293])).
% 74.58/45.94  thf(139,axiom,((! [A:int]: ((ord_less_eq @ int @ (one_one @ int) @ A) = (ord_less @ int @ (zero_zero @ int) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_235_int__one__le__iff__zero__less)).
% 74.58/45.94  thf(674,plain,((! [A:int]: ((ord_less_eq @ int @ (one_one @ int) @ A) = (ord_less @ int @ (zero_zero @ int) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 74.58/45.94  thf(201,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_183_minf_I2_J)).
% 74.58/45.94  thf(906,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)],[201])).
% 74.58/45.94  thf(317,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_101_less__not__sym)).
% 74.58/45.94  thf(1278,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)],[317])).
% 74.58/45.94  thf(161,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_49_dense__le__bounded)).
% 74.58/45.94  thf(750,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)],[161])).
% 74.58/45.94  thf(118,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_56_dual__order_Oeq__iff)).
% 74.58/45.94  thf(618,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)],[118])).
% 74.58/45.94  thf(39,axiom,((! [TA: $tType]: ((comm_semiring_1 @ TA) => ((reflect_poly @ TA @ (one_one @ (poly @ TA))) = (one_one @ (poly @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_221_reflect__poly__1)).
% 74.58/45.94  thf(425,plain,((! [TA: $tType]: ((comm_semiring_1 @ TA) => ((reflect_poly @ TA @ (one_one @ (poly @ TA))) = (one_one @ (poly @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 74.58/45.94  thf(99,axiom,((ring_n68954251visors @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Oring__no__zero__divisors)).
% 74.58/45.94  thf(573,plain,((ring_n68954251visors @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 74.58/45.94  thf(345,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_191_subset__iff__psubset__eq)).
% 74.58/45.94  thf(1374,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)],[345])).
% 74.58/45.94  thf(14,axiom,((! [TA: $tType]: (ord @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Oord_24)).
% 74.58/45.94  thf(375,plain,((! [TA: $tType]: (ord @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 74.58/45.94  thf(279,axiom,((ord_less @ real @ a2 @ b2)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_assms_I2_J)).
% 74.58/45.94  thf(1154,plain,((ord_less @ real @ a2 @ b2)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[279])).
% 74.58/45.94  thf(38,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (preorder @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Orderings_Opreorder_59)).
% 74.58/45.94  thf(423,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (preorder @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 74.58/45.94  thf(146,axiom,((! [TA: $tType]: ((zero @ TA) => ((reflect_poly @ TA @ (zero_zero @ (poly @ TA))) = (zero_zero @ (poly @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_205_reflect__poly__0)).
% 74.58/45.94  thf(694,plain,((! [TA: $tType]: ((zero @ TA) => ((reflect_poly @ TA @ (zero_zero @ (poly @ TA))) = (zero_zero @ (poly @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 74.58/45.94  thf(28,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (ordere216010020id_add @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Groups_Oordered__comm__monoid__add_52)).
% 74.58/45.94  thf(402,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (ordere216010020id_add @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 74.58/45.94  thf(158,axiom,((! [TA: $tType,TB: $tType]: (! [A:(set @ TA),B:(set @ TB),C:(TA > (TB > $o))]: ((~ (finite_finite2 @ TA @ A)) => ((finite_finite2 @ TB @ B) => ((! [D:TA]: ((member @ TA @ D @ A) => (? [E:TB]: ((member @ TB @ E @ B) & (C @ D @ E))))) => (? [D:TB]: ((member @ TB @ D @ B) & ~ (finite_finite2 @ TA @ (collect @ TA @ (^ [E:TA]: ((member @ TA @ E @ A) & (C @ E @ D))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_pigeonhole__infinite__rel)).
% 74.58/45.94  thf(732,plain,((! [TA: $tType,TB: $tType]: (! [A:(set @ TA),B:(set @ TB),C:(TA > (TB > $o))]: ((~ (finite_finite2 @ TA @ A)) => ((finite_finite2 @ TB @ B) => ((! [D:TA]: ((member @ TA @ D @ A) => (? [E:TB]: ((member @ TB @ E @ B) & (C @ D @ E))))) => (? [D:TB]: ((member @ TB @ D @ B) & ~ (finite_finite2 @ TA @ (collect @ TA @ (^ [E:TA]: ((member @ TA @ E @ A) & (C @ E @ D))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 74.58/45.94  thf(351,axiom,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TA) => (! [A:(set @ TB),B:TB,C:(TB > TA)]: ((finite_finite2 @ TB @ A) => (((member @ TB @ B @ A) => ((groups1340683514dd_sum @ TB @ TA @ (^ [D:TB]: (if @ TA @ (B = D) @ (C @ D) @ (zero_zero @ TA))) @ A) = (C @ B))) & ((~ (member @ TB @ B @ A)) => ((groups1340683514dd_sum @ TB @ TA @ (^ [D:TB]: (if @ TA @ (B = D) @ (C @ D) @ (zero_zero @ TA))) @ A) = (zero_zero @ TA))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_sum_Odelta_H)).
% 74.58/45.94  thf(1389,plain,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TA) => (! [A:(set @ TB),B:TB,C:(TB > TA)]: ((finite_finite2 @ TB @ A) => (((member @ TB @ B @ A) => ((groups1340683514dd_sum @ TB @ TA @ (^ [D:TB]: (if @ TA @ (B = D) @ (C @ D) @ (zero_zero @ TA))) @ A) = (C @ B))) & ((~ (member @ TB @ B @ A)) => ((groups1340683514dd_sum @ TB @ TA @ (^ [D:TB]: (if @ TA @ (B = D) @ (C @ D) @ (zero_zero @ TA))) @ A) = (zero_zero @ TA))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[351])).
% 74.58/45.94  thf(86,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_216_pred__subset__eq)).
% 74.58/45.94  thf(545,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)],[86])).
% 74.58/45.94  thf(31,axiom,((zero_less_one @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Ozero__less__one)).
% 74.58/45.94  thf(413,plain,((zero_less_one @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 74.58/45.94  thf(271,axiom,((linordered_idom @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Olinordered__idom_36)).
% 74.58/45.94  thf(1139,plain,((linordered_idom @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[271])).
% 74.58/45.94  thf(205,axiom,((no_top @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Ono__top_43)).
% 74.58/45.94  thf(936,plain,((no_top @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 74.58/45.94  thf(344,axiom,((! [TA: $tType]: (((comm_ring_1 @ TA) & (ring_n68954251visors @ TA)) => (! [A:(poly @ TA)]: ((A != (zero_zero @ (poly @ TA))) => (finite_finite2 @ TA @ (collect @ TA @ (^ [B:TA]: ((poly2 @ TA @ A @ B) = (zero_zero @ TA)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_poly__roots__finite)).
% 74.58/45.94  thf(1371,plain,((! [TA: $tType]: (((comm_ring_1 @ TA) & (ring_n68954251visors @ TA)) => (! [A:(poly @ TA)]: ((~ (A = (zero_zero @ (poly @ TA)))) => (finite_finite2 @ TA @ (collect @ TA @ (^ [B:TA]: ((poly2 @ TA @ A @ B) = (zero_zero @ TA)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[344])).
% 74.58/45.94  thf(326,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_127_not__le)).
% 74.58/45.94  thf(1312,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)],[326])).
% 74.58/45.94  thf(115,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_159_subsetD)).
% 74.58/45.94  thf(611,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)],[115])).
% 74.58/45.94  thf(67,axiom,((! [TA: $tType]: ((comm_semiring_0 @ TA) => (comm_semiring_0 @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Rings_Ocomm__semiring__0_57)).
% 74.58/45.94  thf(498,plain,((! [TA: $tType]: ((comm_semiring_0 @ TA) => (comm_semiring_0 @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 74.58/45.94  thf(332,axiom,((ord_less @ real @ a @ a2)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_assms_I1_J)).
% 74.58/45.94  thf(1332,plain,((ord_less @ real @ a @ a2)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[332])).
% 74.58/45.94  thf(52,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_dual__order_Orefl)).
% 74.58/45.94  thf(466,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 74.58/45.94  thf(208,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:(set @ TA),B:TA]: ((finite_finite2 @ TA @ A) => ((member @ TA @ B @ A) => (? [C:TA]: ((member @ TA @ C @ A) & (ord_less_eq @ TA @ B @ C) & ! [D:TA]: ((member @ TA @ D @ A) => ((ord_less_eq @ TA @ C @ D) => (C = D))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_finite__has__maximal2)).
% 74.58/45.94  thf(947,plain,((! [TA: $tType]: ((order @ TA) => (! [A:(set @ TA),B:TA]: ((finite_finite2 @ TA @ A) => ((member @ TA @ B @ A) => (? [C:TA]: ((member @ TA @ C @ A) & (ord_less_eq @ TA @ B @ C) & ! [D:TA]: ((member @ TA @ D @ A) => ((ord_less_eq @ TA @ C @ D) => (C = D))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 74.58/45.94  thf(301,axiom,((ord @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Oord_47)).
% 74.58/45.94  thf(1224,plain,((ord @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[301])).
% 74.58/45.94  thf(84,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_162_equalityD1)).
% 74.58/45.94  thf(540,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)],[84])).
% 74.58/45.94  thf(295,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_149_minf_I8_J)).
% 74.58/45.94  thf(1194,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)],[295])).
% 74.58/45.94  thf(169,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_184_minf_I3_J)).
% 74.58/45.94  thf(784,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)],[169])).
% 74.58/45.94  thf(35,axiom,((linorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Olinorder_26)).
% 74.58/45.94  thf(419,plain,((linorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 74.58/45.94  thf(240,axiom,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ B)) = (B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_mem__Collect__eq)).
% 74.58/45.94  thf(1048,plain,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ (B))) = (B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 74.58/45.94  thf(15,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_75_order__subst2)).
% 74.58/45.94  thf(377,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)],[15])).
% 74.58/45.94  thf(6,axiom,((no_top @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Ono__top_16)).
% 74.58/45.94  thf(362,plain,((no_top @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 74.58/45.94  thf(274,axiom,((comm_ring_1 @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Ocomm__ring__1_42)).
% 74.58/45.94  thf(1144,plain,((comm_ring_1 @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[274])).
% 74.58/45.94  thf(72,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_64_order__class_Oorder_Oeq__iff)).
% 74.58/45.94  thf(509,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)],[72])).
% 74.58/45.94  thf(238,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_128_not__less)).
% 74.58/45.94  thf(1043,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)],[238])).
% 74.58/45.94  thf(43,axiom,((! [TA: $tType]: (order @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Oorder_23)).
% 74.58/45.94  thf(434,plain,((! [TA: $tType]: (order @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 74.58/45.94  thf(57,axiom,((! [TA: $tType]: ((idom @ TA) => (idom @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Rings_Oidom)).
% 74.58/45.94  thf(477,plain,((! [TA: $tType]: ((idom @ TA) => (idom @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 74.58/45.94  thf(20,axiom,((! [TA: $tType]: ((zero @ TA) => (zero @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Groups_Ozero_65)).
% 74.58/45.94  thf(387,plain,((! [TA: $tType]: ((zero @ TA) => (zero @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 74.58/45.94  thf(252,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_110_exists__least__iff)).
% 74.58/45.94  thf(1080,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)],[252])).
% 74.58/45.94  thf(79,axiom,((no_bot @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Ono__bot)).
% 74.58/45.94  thf(535,plain,((no_bot @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 74.58/45.94  thf(113,axiom,((comm_semiring_1 @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Ocomm__semiring__1)).
% 74.58/45.94  thf(609,plain,((comm_semiring_1 @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 74.58/45.94  thf(155,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (~ (ord_less @ TA @ (one_one @ TA) @ (one_one @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_less__numeral__extra_I4_J)).
% 74.58/45.94  thf(726,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (~ (ord_less @ TA @ (one_one @ TA) @ (one_one @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 74.58/45.94  thf(119,axiom,((linord1659791738miring @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Olinordered__nonzero__semiring)).
% 74.58/45.94  thf(621,plain,((linord1659791738miring @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 74.58/45.94  thf(60,axiom,((linord1659791738miring @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Olinordered__nonzero__semiring_8)).
% 74.58/45.94  thf(483,plain,((linord1659791738miring @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 74.58/45.94  thf(148,axiom,((! [TA: $tType,TB: $tType]: (! [A:(set @ TA),B:(TA > (TB > $o))]: ((finite_finite2 @ TA @ A) => ((! [C:TA]: ((member @ TA @ C @ A) => (? [D:TB]: (B @ C @ D)))) => (? [C:(TA > TB)]: ! [D:TA]: ((member @ TA @ D @ A) => (B @ D @ (C @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_finite__set__choice)).
% 74.58/45.94  thf(700,plain,((! [TA: $tType,TB: $tType]: (! [A:(set @ TA),B:(TA > (TB > $o))]: ((finite_finite2 @ TA @ A) => ((! [C:TA]: ((member @ TA @ C @ A) => (? [D:TB]: (B @ C @ D)))) => (? [C:(TA > TB)]: ! [D:TA]: ((member @ TA @ D @ A) => (B @ D @ (C @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 74.58/45.94  thf(123,axiom,((no_top @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Ono__top)).
% 74.58/45.94  thf(626,plain,((no_top @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 74.58/45.94  thf(335,axiom,((! [TA: $tType]: ((linordered_idom @ 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_253_linorder__neqE__linordered__idom)).
% 74.58/45.94  thf(1344,plain,((! [TA: $tType]: ((linordered_idom @ 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)],[335])).
% 74.58/45.94  thf(207,axiom,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TA) => (! [A:(set @ TB),B:(TB > TA)]: ((! [C:TB]: ((member @ TB @ C @ A) => (ord_less_eq @ TA @ (B @ C) @ (zero_zero @ TA)))) => (ord_less_eq @ TA @ (groups1340683514dd_sum @ TB @ TA @ B @ A) @ (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_241_sum__nonpos)).
% 74.58/45.94  thf(943,plain,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TA) => (! [A:(set @ TB),B:(TB > TA)]: ((! [C:TB]: ((member @ TB @ C @ A) => (ord_less_eq @ TA @ (B @ C) @ (zero_zero @ TA)))) => (ord_less_eq @ TA @ (groups1340683514dd_sum @ TB @ TA @ (B) @ A) @ (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 74.58/45.94  thf(137,axiom,((! [A:int,B:int]: (finite_finite2 @ int @ (collect @ int @ (^ [C:int]: ((ord_less_eq @ int @ A @ C) & (ord_less_eq @ int @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_210_finite__interval__int1)).
% 74.58/45.94  thf(668,plain,((! [A:int,B:int]: (finite_finite2 @ int @ (collect @ int @ (^ [C:int]: ((ord_less_eq @ int @ A @ C) & (ord_less_eq @ int @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 74.58/45.94  thf(265,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_111_linorder__less__wlog)).
% 74.58/45.94  thf(1112,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)],[265])).
% 74.58/45.94  thf(185,axiom,((! [A:(poly @ real),B:real]: ((sturm_652470720p_poly @ A @ (zero_zero @ (poly @ real)) @ B) = (zero_zero @ int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_jump__poly0_I2_J)).
% 74.58/45.94  thf(858,plain,((! [A:(poly @ real),B:real]: ((sturm_652470720p_poly @ A @ (zero_zero @ (poly @ real)) @ B) = (zero_zero @ int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 74.58/45.94  thf(9,axiom,((ordere1818651114id_add @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Oordered__cancel__comm__monoid__add_7)).
% 74.58/45.94  thf(367,plain,((ordere1818651114id_add @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 74.58/45.94  thf(277,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_186_minf_I5_J)).
% 74.58/45.94  thf(1149,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)],[277])).
% 74.58/45.94  thf(212,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_192_subset__psubset__trans)).
% 74.58/45.94  thf(964,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)],[212])).
% 74.58/45.94  thf(288,axiom,((linordered_field @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Fields_Olinordered__field)).
% 74.58/45.94  thf(1177,plain,((linordered_field @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[288])).
% 74.58/45.94  thf(348,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_84_order__less__subst2)).
% 74.58/45.94  thf(1381,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)],[348])).
% 74.58/45.94  thf(308,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_136_dense__le)).
% 74.58/45.94  thf(1245,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)],[308])).
% 74.58/45.94  thf(231,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_172_less__fun__def)).
% 74.58/45.94  thf(1015,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)],[231])).
% 74.58/45.94  thf(220,axiom,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TB) => (! [A:(set @ TA),B:(TA > TB)]: ((finite_finite2 @ TA @ A) => ((! [C:TA]: ((member @ TA @ C @ A) => (ord_less_eq @ TB @ (zero_zero @ TB) @ (B @ C)))) => (((groups1340683514dd_sum @ TA @ TB @ B @ A) = (zero_zero @ TB)) = (! [C:TA]: ((member @ TA @ C @ A) => ((B @ C) = (zero_zero @ TB))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_sum__nonneg__eq__0__iff)).
% 74.58/45.94  thf(986,plain,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TB) => (! [A:(set @ TA),B:(TA > TB)]: ((finite_finite2 @ TA @ A) => ((! [C:TA]: ((member @ TA @ C @ A) => (ord_less_eq @ TB @ (zero_zero @ TB) @ (B @ C)))) => (((groups1340683514dd_sum @ TA @ TB @ (B) @ A) = (zero_zero @ TB)) = (! [C:TA]: ((member @ TA @ C @ A) => ((B @ C) = (zero_zero @ TB))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 74.58/45.94  thf(224,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_185_minf_I4_J)).
% 74.58/45.94  thf(1000,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)],[224])).
% 74.58/45.94  thf(342,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (~ (ord_less @ TA @ (one_one @ TA) @ (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_251_not__one__less__zero)).
% 74.58/45.94  thf(1364,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (~ (ord_less @ TA @ (one_one @ TA) @ (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[342])).
% 74.58/45.94  thf(260,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_94_less__trans)).
% 74.58/45.94  thf(1102,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)],[260])).
% 74.58/45.94  thf(131,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_134_less__le__trans)).
% 74.58/45.94  thf(653,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)],[131])).
% 74.58/45.94  thf(246,axiom,((dense_linorder @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Odense__linorder)).
% 74.58/45.94  thf(1066,plain,((dense_linorder @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[246])).
% 74.58/45.94  thf(188,axiom,((ring_n68954251visors @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Oring__no__zero__divisors_34)).
% 74.58/45.94  thf(868,plain,((ring_n68954251visors @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 74.58/45.94  thf(70,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (zero_less_one @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Rings_Ozero__less__one_58)).
% 74.58/45.94  thf(505,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (zero_less_one @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 74.58/45.94  thf(45,axiom,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oorder)).
% 74.58/45.94  thf(438,plain,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 74.58/45.94  thf(56,axiom,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TB) => (! [A:(set @ TA),B:(TA > TB),C:(TA > TB)]: ((! [D:TA]: ((member @ TA @ D @ A) => (ord_less_eq @ TB @ (B @ D) @ (C @ D)))) => (ord_less_eq @ TB @ (groups1340683514dd_sum @ TA @ TB @ B @ A) @ (groups1340683514dd_sum @ TA @ TB @ C @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_239_sum__mono)).
% 74.58/45.94  thf(473,plain,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TB) => (! [A:(set @ TA),B:(TA > TB),C:(TA > TB)]: ((! [D:TA]: ((member @ TA @ D @ A) => (ord_less_eq @ TB @ (B @ D) @ (C @ D)))) => (ord_less_eq @ TB @ (groups1340683514dd_sum @ TA @ TB @ (B) @ A) @ (groups1340683514dd_sum @ TA @ TB @ (C) @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 74.58/45.94  thf(153,axiom,((ordere1818651114id_add @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Oordered__cancel__comm__monoid__add_31)).
% 74.58/45.94  thf(722,plain,((ordere1818651114id_add @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 74.58/45.94  thf(236,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__asym)).
% 74.58/45.94  thf(1034,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)],[236])).
% 74.58/45.94  thf(64,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_164_subset__iff)).
% 74.58/45.94  thf(490,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)],[64])).
% 74.58/45.94  thf(298,axiom,((! [A:real]: ((((ord_less @ real @ a @ A) & (ord_less_eq @ real @ A @ a2)) | ((ord_less_eq @ real @ b2 @ A) & (ord_less @ real @ A @ b))) => ((poly2 @ real @ p @ A) != (zero_zero @ real))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_assms_I4_J)).
% 74.58/45.94  thf(1208,plain,((! [A:real]: ((((ord_less @ real @ a @ A) & (ord_less_eq @ real @ A @ a2)) | ((ord_less_eq @ real @ b2 @ A) & (ord_less @ real @ A @ b))) => (~ ((poly2 @ real @ p @ A) = (zero_zero @ real)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[298])).
% 74.58/45.94  thf(78,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_204_predicate1I)).
% 74.58/45.94  thf(531,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)],[78])).
% 74.58/45.94  thf(334,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_97_ord__eq__less__trans)).
% 74.58/45.94  thf(1340,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)],[334])).
% 74.58/45.94  thf(89,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_55_dual__order_Oantisym)).
% 74.58/45.94  thf(553,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)],[89])).
% 74.58/45.94  thf(291,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_42_dual__order_Ostrict__iff__order)).
% 74.58/45.94  thf(1181,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)],[291])).
% 74.58/45.94  thf(179,axiom,((linord1659791738miring @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Olinordered__nonzero__semiring_32)).
% 74.58/45.94  thf(836,plain,((linord1659791738miring @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 74.58/45.94  thf(173,axiom,((! [TA: $tType]: ((comm_semiring_1 @ TA) => (! [A:TA]: ((poly2 @ TA @ (one_one @ (poly @ TA)) @ A) = (one_one @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_222_poly__1)).
% 74.58/45.94  thf(795,plain,((! [TA: $tType]: ((comm_semiring_1 @ TA) => (! [A:TA]: ((poly2 @ TA @ (one_one @ (poly @ TA)) @ A) = (one_one @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 74.58/45.94  thf(141,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_174_verit__comp__simplify1_I1_J)).
% 74.58/45.94  thf(680,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 74.58/45.94  thf(135,axiom,((! [A:real,B:real,C:(poly @ real)]: ((sturm_1539314049x_poly @ A @ B @ (zero_zero @ (poly @ real)) @ C) = (zero_zero @ int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_218_cindex__poly__0_I1_J)).
% 74.58/45.94  thf(663,plain,((! [A:real,B:real,C:(poly @ real)]: ((sturm_1539314049x_poly @ A @ B @ (zero_zero @ (poly @ real)) @ C) = (zero_zero @ int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 74.58/45.94  thf(87,axiom,((! [TA: $tType,TB: $tType]: (((finite_finite @ TB) & (finite_finite @ TA)) => (finite_finite @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Finite__Set_Ofinite)).
% 74.58/45.94  thf(548,plain,((! [TA: $tType,TB: $tType]: (((finite_finite @ TB) & (finite_finite @ TA)) => (finite_finite @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 74.58/45.94  thf(275,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_199_psubsetD)).
% 74.58/45.94  thf(1145,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)],[275])).
% 74.58/45.94  thf(232,axiom,((ordere216010020id_add @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Oordered__comm__monoid__add_33)).
% 74.58/45.94  thf(1018,plain,((ordere216010020id_add @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 74.58/45.94  thf(104,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_73_ord__le__eq__subst)).
% 74.58/45.94  thf(580,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)],[104])).
% 74.58/45.94  thf(129,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((finite_finite2 @ TA @ (collect @ TA @ (^ [C:TA]: ((A @ C) | (B @ C))))) = ((finite_finite2 @ TA @ (collect @ TA @ A)) & (finite_finite2 @ TA @ (collect @ TA @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_finite__Collect__disjI)).
% 74.58/45.94  thf(640,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((finite_finite2 @ TA @ (collect @ TA @ (^ [C:TA]: ((A @ C) | (B @ C))))) = ((finite_finite2 @ TA @ (collect @ TA @ (A))) & (finite_finite2 @ TA @ (collect @ TA @ (B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 74.58/45.94  thf(191,axiom,((! [A:int,B:int,C:$o,D:$o]: ((A = B) => (((ord_less_eq @ int @ (zero_zero @ int) @ B) => (C = D)) => (((ord_less_eq @ int @ (zero_zero @ int) @ A) & (C)) = ((ord_less_eq @ int @ (zero_zero @ int) @ B) & (D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_189_conj__le__cong)).
% 74.58/45.94  thf(872,plain,((! [A:int,B:int,C:$o,D:$o]: ((A = B) => (((ord_less_eq @ int @ (zero_zero @ int) @ B) => (C = D)) => (((ord_less_eq @ int @ (zero_zero @ int) @ A) & (C)) = ((ord_less_eq @ int @ (zero_zero @ int) @ B) & (D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 74.58/45.94  thf(149,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_98_ord__less__eq__trans)).
% 74.58/45.94  thf(705,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)],[149])).
% 74.58/45.94  thf(302,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_103_antisym__conv3)).
% 74.58/45.94  thf(1225,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)],[302])).
% 74.58/45.94  thf(194,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((~ (finite_finite2 @ TA @ A)) => (~ (finite_finite2 @ TA @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_infinite__super)).
% 74.58/45.94  thf(887,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((~ (finite_finite2 @ TA @ A)) => (~ (finite_finite2 @ TA @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 74.58/45.94  thf(32,axiom,((comm_monoid_add @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Ocomm__monoid__add)).
% 74.58/45.94  thf(414,plain,((comm_monoid_add @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 74.58/45.94  thf(310,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_95_less__linear)).
% 74.58/45.94  thf(1252,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)],[310])).
% 74.58/45.94  thf(151,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_87_neqE)).
% 74.58/45.94  thf(712,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)],[151])).
% 74.58/45.94  thf(91,axiom,((zero @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Ozero)).
% 74.58/45.94  thf(557,plain,((zero @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 74.58/45.94  thf(243,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:(set @ TA),B:TA]: ((finite_finite2 @ TA @ A) => ((member @ TA @ B @ A) => (? [C:TA]: ((member @ TA @ C @ A) & (ord_less_eq @ TA @ C @ B) & ! [D:TA]: ((member @ TA @ D @ A) => ((ord_less_eq @ TA @ D @ C) => (C = D))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_finite__has__minimal2)).
% 74.58/45.94  thf(1053,plain,((! [TA: $tType]: ((order @ TA) => (! [A:(set @ TA),B:TA]: ((finite_finite2 @ TA @ A) => ((member @ TA @ B @ A) => (? [C:TA]: ((member @ TA @ C @ A) & (ord_less_eq @ TA @ C @ B) & ! [D:TA]: ((member @ TA @ D @ A) => ((ord_less_eq @ TA @ D @ C) => (C = D))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[243])).
% 74.58/45.94  thf(324,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_171_Collect__mono__iff)).
% 74.58/45.94  thf(1300,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)],[324])).
% 74.58/45.94  thf(171,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_133_le__less__trans)).
% 74.58/45.94  thf(791,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)],[171])).
% 74.58/45.94  thf(47,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_208_predicate1D)).
% 74.58/45.94  thf(441,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)],[47])).
% 74.58/45.94  thf(12,axiom,((! [TA: $tType]: ((comm_semiring_1 @ TA) => (comm_semiring_1 @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Rings_Ocomm__semiring__1_56)).
% 74.58/45.94  thf(370,plain,((! [TA: $tType]: ((comm_semiring_1 @ TA) => (comm_semiring_1 @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 74.58/45.94  thf(313,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_112_dual__order_Ostrict__trans)).
% 74.58/45.94  thf(1262,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)],[313])).
% 74.58/45.94  thf(102,axiom,((! [TA: $tType]: ((idom @ TA) => (ring_n68954251visors @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Rings_Oring__no__zero__divisors_53)).
% 74.58/45.94  thf(576,plain,((! [TA: $tType]: ((idom @ TA) => (ring_n68954251visors @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 74.58/45.94  thf(266,axiom,((zero_less_one @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Ozero__less__one_39)).
% 74.58/45.94  thf(1130,plain,((zero_less_one @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[266])).
% 74.58/45.94  thf(130,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_176_pinf_I2_J)).
% 74.58/45.94  thf(643,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)],[130])).
% 74.58/45.94  thf(85,axiom,((wellorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Owellorder)).
% 74.58/45.94  thf(544,plain,((wellorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 74.58/45.94  thf(339,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_180_pinf_I7_J)).
% 74.58/45.94  thf(1358,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)],[339])).
% 74.58/45.94  thf(116,axiom,((zero_less_one @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Ozero__less__one_13)).
% 74.58/45.94  thf(613,plain,((zero_less_one @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 74.58/45.94  thf(319,axiom,((~ (ord_less @ int @ (zero_zero @ int) @ (zero_zero @ int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_214_less__int__code_I1_J)).
% 74.58/45.94  thf(1284,plain,((~ (ord_less @ int @ (zero_zero @ int) @ (zero_zero @ int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[319])).
% 74.58/45.94  thf(109,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_77_le__fun__def)).
% 74.58/45.94  thf(600,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)],[109])).
% 74.58/45.94  thf(242,axiom,((condit1037483654norder @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Conditionally__Complete__Lattices_Oconditionally__complete__linorder_30)).
% 74.58/45.94  thf(1052,plain,((condit1037483654norder @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 74.58/45.94  thf(306,axiom,((linorder @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Olinorder_41)).
% 74.58/45.94  thf(1240,plain,((linorder @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[306])).
% 74.58/45.94  thf(19,axiom,((canoni770627133id_add @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocanonically__ordered__monoid__add)).
% 74.58/45.94  thf(386,plain,((canoni770627133id_add @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 74.58/45.94  thf(257,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_150_minf_I6_J)).
% 74.58/45.94  thf(1094,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)],[257])).
% 74.58/45.94  thf(272,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_116_ex__gt__or__lt)).
% 74.58/45.94  thf(1140,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)],[272])).
% 74.58/45.94  thf(49,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_168_set__eq__subset)).
% 74.58/45.94  thf(446,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)],[49])).
% 74.58/45.94  thf(98,axiom,((! [TA: $tType]: (((ring_char_0 @ TA) & (comm_ring_1 @ TA)) => (ring_char_0 @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Nat_Oring__char__0_63)).
% 74.58/45.94  thf(571,plain,((! [TA: $tType]: (((ring_char_0 @ TA) & (comm_ring_1 @ TA)) => (ring_char_0 @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 74.58/45.94  thf(124,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (ord_less_eq @ TA @ (one_one @ TA) @ (one_one @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_224_le__numeral__extra_I4_J)).
% 74.58/45.94  thf(627,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (ord_less_eq @ TA @ (one_one @ TA) @ (one_one @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 74.58/45.94  thf(83,axiom,((order @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Oorder_17)).
% 74.58/45.94  thf(539,plain,((order @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 74.58/45.94  thf(59,axiom,((ordere1818651114id_add @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Oordered__cancel__comm__monoid__add)).
% 74.58/45.94  thf(482,plain,((ordere1818651114id_add @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 74.58/45.94  thf(281,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_194_psubset__subset__trans)).
% 74.58/45.94  thf(1157,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)],[281])).
% 74.58/45.94  thf(144,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: ((ord_less_eq @ TA @ A @ (zero_zero @ TA)) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_le__zero__eq)).
% 74.58/45.94  thf(688,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: ((ord_less_eq @ TA @ A @ (zero_zero @ TA)) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 74.58/45.94  thf(228,axiom,((sturm_1539314049x_poly = (^ [A:real,B:real,C:(poly @ real),D:(poly @ real)]: (groups1340683514dd_sum @ real @ int @ (sturm_652470720p_poly @ C @ D) @ (collect @ real @ (^ [E:real]: (((poly2 @ real @ D @ E) = (zero_zero @ real)) & (ord_less @ real @ A @ E) & (ord_less @ real @ E @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_220_cindex__poly__def)).
% 74.58/45.94  thf(1010,plain,(((sturm_1539314049x_poly) = (^ [A:real,B:real,C:(poly @ real),D:(poly @ real)]: (groups1340683514dd_sum @ real @ int @ (sturm_652470720p_poly @ C @ D) @ (collect @ real @ (^ [E:real]: (((poly2 @ real @ D @ E) = (zero_zero @ real)) & (ord_less @ real @ A @ E) & (ord_less @ real @ E @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 74.58/45.94  thf(263,axiom,((! [TA: $tType]: ((zero @ TA) => (! [A:nat]: ((poly_cutoff @ TA @ A @ (zero_zero @ (poly @ TA))) = (zero_zero @ (poly @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_155_poly__cutoff__0)).
% 74.58/45.94  thf(1108,plain,((! [TA: $tType]: ((zero @ TA) => (! [A:nat]: ((poly_cutoff @ TA @ A @ (zero_zero @ (poly @ TA))) = (zero_zero @ (poly @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[263])).
% 74.58/45.94  thf(7,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (order @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Orderings_Oorder_62)).
% 74.58/45.94  thf(363,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (order @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 74.58/45.94  thf(90,axiom,((comm_semiring_0 @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Ocomm__semiring__0_12)).
% 74.58/45.94  thf(556,plain,((comm_semiring_0 @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 74.58/45.94  thf(10,axiom,((linorder @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Olinorder)).
% 74.58/45.94  thf(368,plain,((linorder @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 74.58/45.94  thf(181,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_81_ord__eq__less__subst)).
% 74.58/45.94  thf(844,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)],[181])).
% 74.58/45.94  thf(330,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_Collect__mem__eq)).
% 74.58/45.94  thf(1326,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[330])).
% 74.58/45.94  thf(105,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oord)).
% 74.58/45.94  thf(588,plain,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 74.58/45.94  thf(75,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_68_le__cases)).
% 74.58/45.94  thf(517,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)],[75])).
% 74.58/45.94  thf(245,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_less__imp__not__eq2)).
% 74.58/45.94  thf(1062,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[245])).
% 74.58/45.94  thf(22,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: ((comm_monoid_add @ TC) => (! [A:(TB > (TA > TC)),B:(set @ TA),C:(set @ TB)]: ((groups1340683514dd_sum @ TB @ TC @ (^ [D:TB]: (groups1340683514dd_sum @ TA @ TC @ (A @ D) @ B)) @ C) = (groups1340683514dd_sum @ TA @ TC @ (^ [D:TA]: (groups1340683514dd_sum @ TB @ TC @ (^ [E:TB]: (A @ E @ D)) @ C)) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_sum_Oswap)).
% 74.58/45.94  thf(390,plain,((! [TA: $tType,TB: $tType,TC: $tType]: ((comm_monoid_add @ TC) => (! [A:(TB > (TA > TC)),B:(set @ TA),C:(set @ TB)]: ((groups1340683514dd_sum @ TB @ TC @ (^ [D:TB]: (groups1340683514dd_sum @ TA @ TC @ (A @ D) @ B)) @ C) = (groups1340683514dd_sum @ TA @ TC @ (^ [D:TA]: (groups1340683514dd_sum @ TB @ TC @ (^ [E:TB]: (A @ E @ D)) @ C)) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 74.58/45.94  thf(126,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_144_order_Ostrict__iff__order)).
% 74.58/45.94  thf(632,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)],[126])).
% 74.58/45.94  thf(27,axiom,((ord @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Oord_18)).
% 74.58/45.94  thf(401,plain,((ord @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 74.58/45.94  thf(168,axiom,((! [TA: $tType,TB: $tType]: ((comm_semiring_0 @ TB) => (! [A:(TA > (poly @ TB)),B:(set @ TA),C:TB]: ((poly2 @ TB @ (groups1340683514dd_sum @ TA @ (poly @ TB) @ A @ B) @ C) = (groups1340683514dd_sum @ TA @ TB @ (^ [D:TA]: (poly2 @ TB @ (A @ D) @ C)) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_225_poly__sum)).
% 74.58/45.94  thf(781,plain,((! [TA: $tType,TB: $tType]: ((comm_semiring_0 @ TB) => (! [A:(TA > (poly @ TB)),B:(set @ TA),C:TB]: ((poly2 @ TB @ (groups1340683514dd_sum @ TA @ (poly @ TB) @ (A) @ B) @ C) = (groups1340683514dd_sum @ TA @ TB @ (^ [D:TA]: (poly2 @ TB @ (A @ D) @ C)) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 74.58/45.94  thf(222,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_40_order_Onot__eq__order__implies__strict)).
% 74.58/45.94  thf(995,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)],[222])).
% 74.58/45.94  thf(211,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_197_psubset__eq)).
% 74.58/45.94  thf(961,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)],[211])).
% 74.58/45.94  thf(349,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_146_dual__order_Ostrict__trans2)).
% 74.58/45.94  thf(1385,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)],[349])).
% 74.58/45.94  thf(198,axiom,((p != (zero_zero @ (poly @ real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_False)).
% 74.58/45.94  thf(896,plain,((~ (p = (zero_zero @ (poly @ real))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 74.58/45.94  thf(160,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((finite_finite2 @ TA @ A) => (finite_finite2 @ (set @ TA) @ (collect @ (set @ TA) @ (^ [B:(set @ TA)]: (ord_less_eq @ (set @ TA) @ B @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_finite__Collect__subsets)).
% 74.58/45.94  thf(748,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((finite_finite2 @ TA @ A) => (finite_finite2 @ (set @ TA) @ (collect @ (set @ TA) @ (^ [B:(set @ TA)]: (ord_less_eq @ (set @ TA) @ B @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 74.58/45.94  thf(96,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_79_le__funE)).
% 74.58/45.94  thf(568,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)],[96])).
% 74.58/45.94  thf(323,axiom,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TA) => (! [A:(TB > TA),B:(set @ TB)]: (((groups1340683514dd_sum @ TB @ TA @ A @ B) != (zero_zero @ TA)) => (~ (! [C:TB]: ((member @ TB @ C @ B) => ((A @ C) = (zero_zero @ TA)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_237_sum_Onot__neutral__contains__not__neutral)).
% 74.58/45.94  thf(1294,plain,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TA) => (! [A:(TB > TA),B:(set @ TB)]: ((~ ((groups1340683514dd_sum @ TB @ TA @ (A) @ B) = (zero_zero @ TA))) => (~ (! [C:TB]: ((member @ TB @ C @ B) => ((A @ C) = (zero_zero @ TA)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[323])).
% 74.58/45.94  thf(165,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_182_minf_I1_J)).
% 74.58/45.94  thf(763,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)],[165])).
% 74.58/45.94  thf(17,axiom,((comm_ring_1 @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Ocomm__ring__1)).
% 74.58/45.94  thf(383,plain,((comm_ring_1 @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 74.58/45.94  thf(199,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > nat)]: ((finite_finite2 @ TA @ A) => (((groups1340683514dd_sum @ TA @ nat @ B @ A) = (one_one @ nat)) = (? [C:TA]: ((member @ TA @ C @ A) & ((B @ C) = (one_one @ nat)) & ! [D:TA]: ((member @ TA @ D @ A) => ((C != D) => ((B @ D) = (zero_zero @ nat))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_234_sum__eq__1__iff)).
% 74.58/45.94  thf(899,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > nat)]: ((finite_finite2 @ TA @ A) => (((groups1340683514dd_sum @ TA @ nat @ (B) @ A) = (one_one @ nat)) = (? [C:TA]: ((member @ TA @ C @ A) & ((B @ C) = (one_one @ nat)) & ! [D:TA]: ((member @ TA @ D @ A) => ((~ (C = D)) => ((B @ D) = (zero_zero @ nat))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 74.58/45.94  thf(143,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_125_order__less__le__subst1)).
% 74.58/45.94  thf(684,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)],[143])).
% 74.58/45.94  thf(80,axiom,((comm_semiring_0 @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Ocomm__semiring__0)).
% 74.58/45.94  thf(536,plain,((comm_semiring_0 @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 74.58/45.94  thf(175,axiom,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_gt__ex)).
% 74.58/45.94  thf(800,plain,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 74.58/45.94  thf(268,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: ((~ (ord_less @ TA @ (zero_zero @ TA) @ A)) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_not__gr__zero)).
% 74.58/45.94  thf(1133,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: ((~ (ord_less @ TA @ (zero_zero @ TA) @ A)) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[268])).
% 74.58/45.94  thf(318,axiom,((! [A:real,B:real,C:(poly @ real)]: ((ord_less @ real @ A @ B) => (((poly2 @ real @ C @ A) != (zero_zero @ real)) => (((poly2 @ real @ C @ B) != (zero_zero @ real)) => ((sturm_1539314049x_poly @ A @ B @ (one_one @ (poly @ real)) @ C) = (sturm_424270202_cross @ C @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_cindex__poly__cross)).
% 74.58/45.94  thf(1280,plain,((! [A:real,B:real,C:(poly @ real)]: ((ord_less @ real @ A @ B) => ((~ ((poly2 @ real @ C @ A) = (zero_zero @ real))) => ((~ ((poly2 @ real @ C @ B) = (zero_zero @ real))) => ((sturm_1539314049x_poly @ A @ B @ (one_one @ (poly @ real)) @ C) = (sturm_424270202_cross @ C @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[318])).
% 74.58/45.94  thf(42,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_80_le__funD)).
% 74.58/45.94  thf(432,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)],[42])).
% 74.58/45.94  thf(352,axiom,((ord_less @ real @ b2 @ b)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_assms_I3_J)).
% 74.58/45.94  thf(1395,plain,((ord_less @ real @ b2 @ b)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[352])).
% 74.58/45.94  thf(30,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_160_equalityE)).
% 74.58/45.94  thf(405,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)],[30])).
% 74.58/45.94  thf(187,axiom,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TA) => (! [A:(set @ TB),B:(TB > TA)]: ((~ (finite_finite2 @ TB @ A)) => ((groups1340683514dd_sum @ TB @ TA @ B @ A) = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_sum_Oinfinite)).
% 74.58/45.94  thf(865,plain,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TA) => (! [A:(set @ TB),B:(TB > TA)]: ((~ (finite_finite2 @ TB @ A)) => ((groups1340683514dd_sum @ TB @ TA @ (B) @ A) = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 74.58/45.94  thf(110,axiom,((! [TA: $tType]: (preorder @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Opreorder_21)).
% 74.58/45.94  thf(603,plain,((! [TA: $tType]: (preorder @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 74.58/45.94  thf(184,axiom,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TB) => (! [A:(set @ TA),B:(TA > TB)]: ((! [C:TA]: ((member @ TA @ C @ A) => (ord_less_eq @ TB @ (zero_zero @ TB) @ (B @ C)))) => (ord_less_eq @ TB @ (zero_zero @ TB) @ (groups1340683514dd_sum @ TA @ TB @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_242_sum__nonneg)).
% 74.58/45.94  thf(854,plain,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TB) => (! [A:(set @ TA),B:(TA > TB)]: ((! [C:TA]: ((member @ TA @ C @ A) => (ord_less_eq @ TB @ (zero_zero @ TB) @ (B @ C)))) => (ord_less_eq @ TB @ (zero_zero @ TB) @ (groups1340683514dd_sum @ TA @ TB @ (B) @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 74.58/45.94  thf(325,axiom,((! [A:int,B:int,C:$o,D:$o]: ((A = B) => (((ord_less_eq @ int @ (zero_zero @ int) @ B) => (C = D)) => (((ord_less_eq @ int @ (zero_zero @ int) @ A) => (C)) = ((ord_less_eq @ int @ (zero_zero @ int) @ B) => (D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_imp__le__cong)).
% 74.58/45.94  thf(1303,plain,((! [A:int,B:int,C:$o,D:$o]: ((A = B) => (((ord_less_eq @ int @ (zero_zero @ int) @ B) => (C = D)) => (((ord_less_eq @ int @ (zero_zero @ int) @ A) => (C)) = ((ord_less_eq @ int @ (zero_zero @ int) @ B) => (D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[325])).
% 74.58/45.94  thf(178,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_39_complete__interval)).
% 74.58/45.94  thf(807,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)],[178])).
% 74.58/45.94  thf(127,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_108_order_Ostrict__trans)).
% 74.58/45.94  thf(635,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)],[127])).
% 74.58/45.94  thf(284,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_109_less__imp__not__less)).
% 74.58/45.94  thf(1165,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)],[284])).
% 74.58/45.94  thf(33,axiom,((! [TA: $tType]: ((comm_monoid_add @ TA) => (comm_monoid_add @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Groups_Ocomm__monoid__add_54)).
% 74.58/45.94  thf(415,plain,((! [TA: $tType]: ((comm_monoid_add @ TA) => (comm_monoid_add @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 74.58/45.94  thf(321,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (~ (ord_less @ TA @ (zero_zero @ TA) @ (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_less__numeral__extra_I3_J)).
% 74.58/45.94  thf(1288,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (~ (ord_less @ TA @ (zero_zero @ TA) @ (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[321])).
% 74.58/45.94  thf(26,axiom,((linordered_idom @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Olinordered__idom)).
% 74.58/45.94  thf(400,plain,((linordered_idom @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 74.58/45.94  thf(156,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_not__less__zero)).
% 74.58/45.94  thf(728,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 74.58/45.94  thf(304,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_145_dual__order_Ostrict__trans1)).
% 74.58/45.94  thf(1236,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)],[304])).
% 74.58/45.94  thf(108,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_163_equalityD2)).
% 74.58/45.94  thf(596,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)],[108])).
% 74.58/45.94  thf(233,axiom,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TA) => (! [A:(set @ TB),B:(TB > TA),C:TA,D:TB]: ((finite_finite2 @ TB @ A) => ((! [E:TB]: ((member @ TB @ E @ A) => (ord_less_eq @ TA @ (zero_zero @ TA) @ (B @ E)))) => (((groups1340683514dd_sum @ TB @ TA @ B @ A) = C) => ((member @ TB @ D @ A) => (ord_less_eq @ TA @ (B @ D) @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_249_sum__nonneg__leq__bound)).
% 74.58/45.94  thf(1019,plain,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TA) => (! [A:(set @ TB),B:(TB > TA),C:TA,D:TB]: ((finite_finite2 @ TB @ A) => ((! [E:TB]: ((member @ TB @ E @ A) => (ord_less_eq @ TA @ (zero_zero @ TA) @ (B @ E)))) => (((groups1340683514dd_sum @ TB @ TA @ (B) @ A) = C) => ((member @ TB @ D @ A) => (ord_less_eq @ TA @ (B @ D) @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 74.58/45.94  thf(221,axiom,((! [TA: $tType]: ((comm_semiring_0 @ TA) => (! [A:(poly @ TA)]: (((poly2 @ TA @ (reflect_poly @ TA @ A) @ (zero_zero @ TA)) = (zero_zero @ TA)) = (A = (zero_zero @ (poly @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_201_reflect__poly__at__0__eq__0__iff)).
% 74.58/45.94  thf(992,plain,((! [TA: $tType]: ((comm_semiring_0 @ TA) => (! [A:(poly @ TA)]: (((poly2 @ TA @ (reflect_poly @ TA @ A) @ (zero_zero @ TA)) = (zero_zero @ TA)) = (A = (zero_zero @ (poly @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 74.58/45.94  thf(154,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_139_less__le__not__le)).
% 74.58/45.94  thf(723,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)],[154])).
% 74.58/45.94  thf(145,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) = (B @ C))) => ((collect @ TA @ A) = (collect @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_Collect__cong)).
% 74.58/45.94  thf(691,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)],[145])).
% 74.58/45.94  thf(190,axiom,((dense_order @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Odense__order)).
% 74.58/45.94  thf(871,plain,((dense_order @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 74.58/45.94  thf(69,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_156_subsetI)).
% 74.58/45.94  thf(501,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)],[69])).
% 74.58/45.94  thf(11,axiom,((ring_char_0 @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Nat_Oring__char__0)).
% 74.58/45.94  thf(369,plain,((ring_char_0 @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 74.58/45.94  thf(256,axiom,((comm_semiring_1 @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Ocomm__semiring__1_37)).
% 74.58/45.94  thf(1093,plain,((comm_semiring_1 @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[256])).
% 74.58/45.94  thf(121,axiom,((comm_semiring_1 @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Ocomm__semiring__1_11)).
% 74.58/45.94  thf(624,plain,((comm_semiring_1 @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 74.58/45.94  thf(338,axiom,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TA) => (! [A:(set @ TB),B:(TB > TA)]: ((! [C:TB]: ((member @ TB @ C @ A) => ((B @ C) = (zero_zero @ TA)))) => ((groups1340683514dd_sum @ TB @ TA @ B @ A) = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_sum_Oneutral)).
% 74.58/45.94  thf(1352,plain,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TA) => (! [A:(set @ TB),B:(TB > TA)]: ((! [C:TB]: ((member @ TB @ C @ A) => ((B @ C) = (zero_zero @ TA)))) => ((groups1340683514dd_sum @ TB @ TA @ (B) @ A) = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[338])).
% 74.58/45.94  thf(51,axiom,((! [TA: $tType]: ((comm_ring_1 @ TA) => (comm_ring_1 @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Rings_Ocomm__ring__1_61)).
% 74.58/45.94  thf(464,plain,((! [TA: $tType]: ((comm_ring_1 @ TA) => (comm_ring_1 @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 74.58/45.94  thf(315,axiom,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TA) => (! [A:(set @ TB),B:TB,C:(TB > TA)]: ((finite_finite2 @ TB @ A) => (((member @ TB @ B @ A) => ((groups1340683514dd_sum @ TB @ TA @ (^ [D:TB]: (if @ TA @ (D = B) @ (C @ D) @ (zero_zero @ TA))) @ A) = (C @ B))) & ((~ (member @ TB @ B @ A)) => ((groups1340683514dd_sum @ TB @ TA @ (^ [D:TB]: (if @ TA @ (D = B) @ (C @ D) @ (zero_zero @ TA))) @ A) = (zero_zero @ TA))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_sum_Odelta)).
% 74.58/45.94  thf(1268,plain,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TA) => (! [A:(set @ TB),B:TB,C:(TB > TA)]: ((finite_finite2 @ TB @ A) => (((member @ TB @ B @ A) => ((groups1340683514dd_sum @ TB @ TA @ (^ [D:TB]: (if @ TA @ (D = B) @ (C @ D) @ (zero_zero @ TA))) @ A) = (C @ B))) & ((~ (member @ TB @ B @ A)) => ((groups1340683514dd_sum @ TB @ TA @ (^ [D:TB]: (if @ TA @ (D = B) @ (C @ D) @ (zero_zero @ TA))) @ A) = (zero_zero @ TA))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[315])).
% 74.58/45.94  thf(101,axiom,((zero @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ozero_19)).
% 74.58/45.94  thf(575,plain,((zero @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 74.58/45.94  thf(218,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_121_le__less)).
% 74.58/45.94  thf(982,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)],[218])).
% 74.58/45.94  thf(225,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_48_order_Ostrict__implies__order)).
% 74.58/45.94  thf(1004,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)],[225])).
% 74.58/45.94  thf(54,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (linordered_idom @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Rings_Olinordered__idom_55)).
% 74.58/45.94  thf(469,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (linordered_idom @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 74.58/45.94  thf(3,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_58_linorder__wlog)).
% 74.58/45.94  thf(354,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)],[3])).
% 74.58/45.94  thf(227,axiom,((comm_monoid_add @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Ocomm__monoid__add_35)).
% 74.58/45.94  thf(1009,plain,((comm_monoid_add @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 74.58/45.94  thf(292,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_113_not__less__iff__gr__or__eq)).
% 74.58/45.94  thf(1184,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)],[292])).
% 74.58/45.94  thf(93,axiom,((preorder @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Opreorder_3)).
% 74.58/45.94  thf(560,plain,((preorder @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 74.58/45.94  thf(162,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_151_pinf_I8_J)).
% 74.58/45.94  thf(755,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)],[162])).
% 74.58/45.94  thf(107,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)).
% 74.58/45.94  thf(592,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)],[107])).
% 74.58/45.94  thf(66,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_70_linear)).
% 74.58/45.94  thf(496,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)],[66])).
% 74.58/45.94  thf(248,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: (ord_less_eq @ TA @ (zero_zero @ TA) @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_zero__le)).
% 74.58/45.94  thf(1069,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: (ord_less_eq @ TA @ (zero_zero @ TA) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[248])).
% 74.58/45.94  thf(1396,plain,(($false)),inference(e,[status(thm)],[892,1036,629,479,1315,1179,777,666,365,1190,1168,760,1083,468,977,523,1142,861,730,1290,1205,449,440,655,614,677,1078,384,550,500,715,538,670,404,1196,709,417,436,1228,885,1046,565,1366,389,570,372,1264,1323,802,1059,902,853,1379,1147,1013,881,1319,421,606,1347,443,514,574,1051,485,1136,1151,937,353,966,1377,956,396,998,428,1104,507,1074,512,661,793,381,1067,798,1163,1274,1387,894,1255,1217,561,429,788,1238,916,484,361,625,852,1178,889,1159,493,1027,757,682,974,1012,1106,1259,1111,980,1096,1006,1138,869,610,420,1360,1350,519,578,697,1089,471,1329,1028,488,1361,933,537,637,1214,590,970,1155,393,1249,738,1131,605,622,837,1099,985,1333,1086,1241,360,805,1170,1167,953,773,662,926,1286,398,558,1071,1187,674,906,1278,750,618,425,573,1374,375,1154,423,694,402,732,1389,545,413,1139,936,1371,1312,611,498,1332,466,947,1224,540,1194,784,419,1048,377,362,1144,509,1043,434,477,387,1080,535,609,726,621,483,700,626,1344,943,668,1112,858,367,1149,964,1177,1381,1245,1015,986,1000,1364,1102,653,1066,868,505,438,473,722,1034,490,1208,531,1340,553,1181,836,795,680,663,548,1145,1018,580,640,872,705,1225,887,414,1252,712,557,1053,1300,791,441,370,1262,576,1130,643,544,1358,613,1284,600,1052,1240,386,1094,1140,446,571,627,539,482,1157,688,1010,1108,363,556,368,844,1326,588,517,1062,390,632,401,781,995,961,1385,896,748,568,1294,763,383,899,684,536,800,1133,1280,432,1395,405,865,603,854,1303,807,635,1165,415,1288,400,728,1236,596,1019,992,723,691,871,501,369,1093,624,1352,464,1268,575,982,1004,469,354,1009,1184,560,755,592,496,1069])).
% 74.58/45.94  % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 74.58/45.94  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------