%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP195^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 : n011.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 124.65s 88.50s
% Output : Refutation 125.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP195^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.08/0.21 % Computer : n011.cluster.edu
% 0.08/0.21 % Model : x86_64 x86_64
% 0.08/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.21 % Memory : 8046.5625MB
% 0.08/0.21 % OS : Linux 6.8.0-71-generic
% 0.08/0.21 % CPULimit : 300
% 0.08/0.21 % WCLimit : 300
% 0.08/0.21 % DateTime : Tue Sep 29 20:10:31 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.64/0.51 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.39/0.79 % [INFO] Parsing done (272ms).
% 1.39/0.80 % [INFO] Running in sequential loop mode.
% 2.61/1.08 % [INFO] eprover registered as external prover.
% 2.61/1.09 % [INFO] Scanning for conjecture ...
% 3.09/1.24 % [INFO] Found a conjecture (or negated_conjecture) and 339 axioms. Running axiom selection ...
% 3.32/1.38 % [INFO] Axiom selection finished. Selected 338 axioms (removed 1 axioms).
% 4.10/1.58 % [INFO] Problem is higher-order (TPTP THF).
% 4.10/1.59 % [INFO] Type checking passed.
% 4.10/1.60 % [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 ...
% 124.65/88.49 % External prover 'e' found a proof!
% 124.65/88.49 % [INFO] Killing All external provers ...
% 124.65/88.49 % Time passed: 88193ms (effective reasoning time: 87694ms)
% 124.65/88.49 % 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)>
% 124.65/88.50 % Axioms used in derivation (338): fact_89_order_Otrans, tcon_Polynomial_Opoly___Rings_Oring__no__zero__divisors_48, fact_137_measure__induct__rule, tcon_HOL_Obool___Orderings_Oorder_25, fact_4_poly__0, fact_223_of__nat__eq__1__iff, tcon_Real_Oreal___Nat_Osemiring__char__0_33, fact_242_Suc__n__not__le__n, fact_23_reflect__poly__at__0__eq__0__iff, fact_171_order_Ostrict__iff__order, fact_178_le__less__linear, fact_211_Suc__le__mono, tcon_Polynomial_Opoly___Rings_Ocomm__semiring__0_50, tcon_Polynomial_Opoly___Rings_Ocomm__ring__1_54, fact_81_verit__la__disequality, fact_17_poly__eq__poly__eq__iff, fact_182_le__less__trans, fact_103_order_Ostrict__implies__not__eq, fact_110_dual__order_Oirrefl, tcon_Nat_Onat___Rings_Olinordered__nonzero__semiring_7, fact_239_verit__la__generic, fact_92_order__class_Oorder_Oeq__iff, fact_207_of__nat__eq__iff, tcon_Polynomial_Opoly___Rings_Osemiring__1_55, fact_240_full__nat__induct, fact_12_not__less__zero, tcon_Real_Oreal___Orderings_Olinorder_35, tcon_Real_Oreal___Orderings_Oord_42, fact_64_less__not__refl3, tcon_Nat_Onat___Orderings_Oorder_16, tcon_Real_Oreal___Orderings_Opreorder_34, fact_203_order__pderiv2, fact_73_conj__le__cong, tcon_Int_Oint___Groups_Ozero, fact_72_less__eq__nat_Osimps_I1_J, fact_125_less__asym, fact_238_Nat_Oex__has__greatest__nat, fact_50_verit__comp__simplify1_I3_J, fact_77_le__funI, fact_126_less__imp__neq, tcon_Real_Oreal___Fields_Ofield__char__0, fact_241_not__less__eq__eq, fact_199_poly__cutoff__1, tcon_Int_Oint___Nat_Oring__char__0, fact_3_assms, fact_228_variation__0_I1_J, fact_215_of__nat__0__eq__iff, fact_153_minf_I11_J, fact_204_cross__def, tcon_Polynomial_Opoly___Rings_Osemiring__no__zero__divisors_47, tcon_Polynomial_Opoly___Rings_Ocomm__semiring__1_49, fact_41_order__refl, tcon_HOL_Obool___Orderings_Oord_26, fact_104_not__less__iff__gr__or__eq, fact_245_le__Suc__eq, fact_175_not__le__imp__less, fact_43_minf_I6_J, fact_51_bot__nat__0_Oextremum, fact_161_gr0I, fact_13_gr__implies__not__zero, fact_11_gr__zeroI, fact_34_less__eq__real__def, fact_112_less__imp__triv, fact_160_not__gr0, fact_35_order__0I, tcon_fun___Orderings_Oord, fact_244_le__antisym, fact_19_rsquarefree__roots, fact_115_less__induct, fact_59_infinite__descent__measure, tcon_Nat_Onat___Orderings_Opreorder_12, fact_197_complete__interval, tcon_HOL_Obool___Orderings_Opreorder_23, tcon_Nat_Onat___Groups_Oone_19, fact_123_less__trans, tcon_Real_Oreal___Orderings_Oorder_40, tcon_Nat_Onat___Groups_Ozero_18, tcon_Real_Oreal___Conditionally__Complete__Lattices_Oconditionally__complete__linorder_27, fact_124_less__asym_H, fact_179_dense__le, tcon_Polynomial_Opoly___Orderings_Oorder_56, fact_202_order__pderiv, fact_192_order__le__less__subst1, fact_140_pinf_I1_J, fact_2__092_060open_0620_A_060_Apoly_Ap_Ax_A_092_060Longrightarrow_062_Asign__r__pos_Ap_Ax_092_060close_062, fact_117_less__imp__not__eq, fact_28_le__zero__eq, fact_1__092_060open_062sign__r__pos_Ap_Ax_A_092_060Longrightarrow_062_A0_A_060_Apoly_Ap_Ax_092_060close_062, tcon_Nat_Onat___Rings_Ocomm__semiring__1_9, fact_159_not__less0, fact_101_dual__order_Oantisym, fact_57_le__neq__implies__less, tcon_Nat_Onat___Orderings_Oord_17, fact_139_verit__comp__simplify1_I1_J, tcon_Int_Oint___Rings_Olinordered__idom_2, fact_133_order__less__subst2, fact_30_poly__shift__id, fact_96_order__trans, fact_181_less__le__trans, fact_52_le0, fact_14_zero__less__iff__neq__zero, tcon_Real_Oreal___Rings_Ocomm__ring__1_36, fact_217_of__nat__less__iff, fact_231_of__nat__le__0__iff, tcon_Int_Oint___Rings_Ocomm__ring__1, fact_119_ord__less__eq__trans, fact_131_gt__ex, fact_107_exists__least__iff, fact_247_le__trans, fact_68_bot__nat__0_Oextremum__uniqueI, fact_26_poly__shift__0, fact_16_zero__reorient, fact_76_le__funE, fact_65_less__not__refl2, fact_105_dual__order_Ostrict__trans, fact_235_of__nat__neq__0, tcon_Polynomial_Opoly___Orderings_Oord_58, fact_54_less__imp__le__nat, fact_18_cross__0, fact_180_dense__ge, tcon_Nat_Onat___Orderings_Ono__top_15, fact_162_order_Onot__eq__order__implies__strict, tcon_Real_Oreal___Orderings_Ono__top_38, fact_229_pderiv__1, fact_219_less__Suc0, tcon_Set_Oset___Orderings_Opreorder_20, tcon_Nat_Onat___Rings_Osemiring__no__zero__divisors_8, tcon_Int_Oint___Conditionally__Complete__Lattices_Oconditionally__complete__linorder, tcon_Polynomial_Opoly___Nat_Osemiring__char__0_51, fact_32_le__numeral__extra_I3_J, fact_22_poly__cutoff__0, fact_170_dual__order_Ostrict__trans1, fact_87_eq__refl, fact_208_lessI, fact_49_pinf_I6_J, fact_201_of__nat__0__less__iff, fact_122_less__linear, fact_10_field__lbound__gt__zero, fact_120_ord__eq__less__trans, fact_56_less__or__eq__imp__le, fact_148_minf_I2_J, tcon_Nat_Onat___Conditionally__Complete__Lattices_Oconditionally__complete__linorder_6, fact_53_nat__less__le, fact_71_le__0__eq, fact_61_infinite__descent, fact_143_pinf_I4_J, tcon_Int_Oint___Rings_Ocomm__semiring__1, fact_25_last__non__root__interval, fact_116_less__not__sym, fact_15_pderiv__0, fact_24_next__non__root__interval, tcon_Int_Oint___Orderings_Olinorder, fact_183_less__imp__le, fact_66_less__not__refl, tcon_Int_Oint___Orderings_Oorder_4, fact_95_order__class_Oorder_Oantisym, tcon_Nat_Onat___Rings_Ocomm__semiring__0_10, fact_158_less__zeroE, fact_138_measure__induct, fact_114_antisym__conv3, tcon_Polynomial_Opoly___Groups_Ozero_59, fact_99_dual__order_Otrans, fact_84_eq__iff, tcon_Nat_Onat___Orderings_Owellorder, fact_226_poly__1, fact_166_order_Ostrict__implies__order, fact_130_neqE, tcon_Real_Oreal___Rings_Osemiring__no__zero__divisors_29, fact_210_Suc__less__eq, fact_144_pinf_I5_J, tcon_Polynomial_Opoly___Orderings_Opreorder_52, tcon_Nat_Onat___Nat_Osemiring__char__0_11, fact_168_dense__ge__bounded, fact_185_antisym__conv1, fact_134_order__less__subst1, fact_167_dense__le__bounded, fact_243_nat__le__linear, tcon_Real_Oreal___Orderings_Odense__order, tcon_Polynomial_Opoly___Orderings_Olinorder_53, tcon_Real_Oreal___Orderings_Odense__linorder, fact_39_less__nat__zero__code, fact_127_dense, tcon_Polynomial_Opoly___Nat_Oring__char__0_57, tcon_Int_Oint___Rings_Osemiring__1, fact_33_zero__le, fact_198_rsquarefree__def, tcon_Polynomial_Opoly___Rings_Olinordered__idom, fact_40_bot__nat__0_Onot__eq__extremum, fact_90_le__cases3, tcon_Polynomial_Opoly___Rings_Olinordered__nonzero__semiring_46, fact_152_minf_I7_J, fact_7_poly__IVT__pos, fact_37_not__eq__pos__or__neg__iff__2, fact_38_neq0__conv, tcon_Real_Oreal___Rings_Oring__no__zero__divisors_30, fact_88_le__cases, fact_250_le__SucI, fact_113_less__imp__not__eq2, fact_75_le__funD, tcon_HOL_Obool___Orderings_Olinorder_24, fact_121_less__irrefl, fact_106_linorder__less__wlog, fact_195_leI, fact_8_poly__all__0__iff__0, tcon_Real_Oreal___Rings_Oidom_44, fact_225_coeff__0, fact_237_nat__induct__at__least, fact_190_order__less__le__subst1, tcon_Int_Oint___Orderings_Oord_5, tcon_Real_Oreal___Rings_Osemiring__1_37, fact_246_eq__imp__le, fact_214_of__nat__0, fact_93_ord__eq__le__trans, fact_176_less__le__not__le, fact_232_reflect__poly__reflect__poly, fact_187_not__less, fact_97_dual__order_Orefl, fact_27_order__root, fact_186_le__neq__trans, fact_31_complete__real, fact_48_pinf_I8_J, fact_141_pinf_I2_J, tcon_Set_Oset___Orderings_Oorder_21, fact_91_antisym__conv, tcon_Polynomial_Opoly___Groups_Oone_61, fact_251_le__SucE, fact_85_antisym, fact_221_of__nat__1, fact_154_infinite__descent0__measure, fact_100_dual__order_Oeq__iff, tcon_Int_Oint___Rings_Osemiring__no__zero__divisors, tcon_Real_Oreal___Rings_Olinordered__nonzero__semiring_28, fact_20_cross__no__root, tcon_Real_Oreal___Nat_Oring__char__0_41, fact_177_le__imp__less__or__eq, fact_42_minf_I8_J, fact_108_less__imp__not__less, tcon_fun___Orderings_Opreorder, tcon_Int_Oint___Rings_Ocomm__semiring__0, fact_45_Collect__mem__eq, fact_151_minf_I5_J, fact_209_Suc__mono, tcon_Real_Oreal___Fields_Olinordered__field, tcon_Int_Oint___Rings_Oring__no__zero__divisors, tcon_Nat_Onat___Orderings_Olinorder_13, fact_155_bot__nat__0_Oextremum__strict, fact_193_less__le, fact_111_linorder__cases, fact_63_less__irrefl__nat, fact_222_of__nat__1__eq__iff, fact_132_lt__ex, fact_196_leD, fact_83_ord__le__eq__subst, fact_224_less__one, tcon_Real_Oreal___Orderings_Ono__bot_39, fact_67_nat__neq__iff, fact_109_order_Ostrict__trans, fact_174_order_Ostrict__trans1, fact_236_transitive__stepwise__le, fact_55_le__eq__less__or__eq, fact_146_pinf_I11_J, fact_6_poly__IVT__neg, fact_98_linorder__wlog, fact_74_imp__le__cong, fact_169_dual__order_Ostrict__trans2, fact_62_nat__less__induct, tcon_Real_Oreal___Rings_Olinordered__idom_1, fact_184_antisym__conv2, fact_128_order_Oasym, tcon_Int_Oint___Nat_Osemiring__char__0, fact_191_order__le__less__subst2, fact_188_not__le, fact_5_not__gr__zero, fact_78_le__fun__def, fact_0_False, tcon_fun___Orderings_Oorder, fact_147_minf_I1_J, tcon_Set_Oset___Orderings_Oord_22, fact_230_order__1__eq__0, fact_233_One__nat__def, tcon_Int_Oint___Orderings_Ono__bot, tcon_Int_Oint___Orderings_Opreorder_3, fact_94_ord__le__eq__trans, fact_9_less__numeral__extra_I3_J, fact_60_linorder__neqE__nat, tcon_Int_Oint___Rings_Oidom, fact_220_zero__less__Suc, fact_129_neq__iff, tcon_Real_Oreal___Rings_Ocomm__semiring__0_32, tcon_Int_Oint___Orderings_Ono__top, fact_70_ex__least__nat__le, fact_58_less__mono__imp__le__mono, fact_79_order__subst1, fact_156_infinite__descent0, fact_249_le__refl, fact_142_pinf_I3_J, fact_194_le__less, fact_164_dual__order_Ostrict__iff__order, fact_189_order__less__le__subst2, tcon_Nat_Onat___Groups_Ocanonically__ordered__monoid__add, fact_216_of__nat__eq__0__iff, fact_165_dual__order_Oorder__iff__strict, fact_163_dual__order_Ostrict__implies__order, fact_212_pderiv__of__nat, fact_145_pinf_I7_J, fact_102_dual__order_Ostrict__implies__not__eq, fact_82_ord__eq__le__subst, fact_135_ord__less__eq__subst, fact_136_ord__eq__less__subst, tcon_Real_Oreal___Groups_Oone_45, fact_149_minf_I3_J, fact_173_order_Ostrict__trans2, fact_118_dual__order_Oasym, fact_69_bot__nat__0_Oextremum__unique, fact_172_order_Oorder__iff__strict, fact_29_reflect__poly__0, tcon_Real_Oreal___Groups_Ozero_43, fact_200_coeff__0__reflect__poly__0__iff, fact_36_not__eq__pos__or__neg__iff__1, tcon_Real_Oreal___Rings_Ocomm__semiring__1_31, fact_205_nat_Oinject, tcon_Int_Oint___Rings_Olinordered__nonzero__semiring, fact_21_is__zero__null, fact_150_minf_I4_J, tcon_Int_Oint___Groups_Oone, fact_248_Suc__le__D, fact_157_gr__implies__not0, tcon_Polynomial_Opoly___Rings_Oidom_60, fact_46_Collect__cong, fact_227_variation__0_I2_J, fact_44_mem__Collect__eq, fact_213_reflect__poly__1, tcon_Nat_Onat___Rings_Osemiring__1_14, fact_80_order__subst2, fact_86_linear, fact_206_old_Onat_Oinject, fact_234_less__fun__def, fact_218_of__nat__le__iff
% 124.65/88.50 % No. of inferences in proof: 745
% 124.65/88.50 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 88193 ms resp. 87694 ms w/o parsing
% 125.39/88.64 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 125.39/88.64 thf(real_type, type, real: $tType).
% 125.39/88.64 thf(nat_type, type, nat: $tType).
% 125.39/88.64 thf(int_type, type, int: $tType).
% 125.39/88.64 thf(linordered_idom_decl, type, linordered_idom: !> [TA: $tType]: $o).
% 125.39/88.64 thf(one_decl, type, one: !> [TA: $tType]: $o).
% 125.39/88.64 thf(idom_decl, type, idom: !> [TA: $tType]: $o).
% 125.39/88.64 thf(zero_decl, type, zero: !> [TA: $tType]: $o).
% 125.39/88.64 thf(ord_decl, type, ord: !> [TA: $tType]: $o).
% 125.39/88.64 thf(ring_char_0_decl, type, ring_char_0: !> [TA: $tType]: $o).
% 125.39/88.64 thf(order_decl, type, order: !> [TA: $tType]: $o).
% 125.39/88.64 thf(no_bot_decl, type, no_bot: !> [TA: $tType]: $o).
% 125.39/88.64 thf(no_top_decl, type, no_top: !> [TA: $tType]: $o).
% 125.39/88.64 thf(semiring_1_decl, type, semiring_1: !> [TA: $tType]: $o).
% 125.39/88.64 thf(comm_ring_1_decl, type, comm_ring_1: !> [TA: $tType]: $o).
% 125.39/88.64 thf(linorder_decl, type, linorder: !> [TA: $tType]: $o).
% 125.39/88.64 thf(preorder_decl, type, preorder: !> [TA: $tType]: $o).
% 125.39/88.64 thf(field_char_0_decl, type, field_char_0: !> [TA: $tType]: $o).
% 125.39/88.64 thf(semiring_char_0_decl, type, semiring_char_0: !> [TA: $tType]: $o).
% 125.39/88.64 thf(wellorder_decl, type, wellorder: !> [TA: $tType]: $o).
% 125.39/88.64 thf(dense_order_decl, type, dense_order: !> [TA: $tType]: $o).
% 125.39/88.64 thf(comm_semiring_0_decl, type, comm_semiring_0: !> [TA: $tType]: $o).
% 125.39/88.64 thf(comm_semiring_1_decl, type, comm_semiring_1: !> [TA: $tType]: $o).
% 125.39/88.64 thf(linordered_field_decl, type, linordered_field: !> [TA: $tType]: $o).
% 125.39/88.64 thf(dense_linorder_decl, type, dense_linorder: !> [TA: $tType]: $o).
% 125.39/88.64 thf(ring_n68954251visors_decl, type, ring_n68954251visors: !> [TA: $tType]: $o).
% 125.39/88.64 thf(semiri1193490041visors_decl, type, semiri1193490041visors: !> [TA: $tType]: $o).
% 125.39/88.64 thf(linord1659791738miring_decl, type, linord1659791738miring: !> [TA: $tType]: $o).
% 125.39/88.64 thf(canoni770627133id_add_decl, type, canoni770627133id_add: !> [TA: $tType]: $o).
% 125.39/88.64 thf(condit1037483654norder_decl, type, condit1037483654norder: !> [TA: $tType]: $o).
% 125.39/88.64 thf(one_one_decl, type, one_one: !> [TA: $tType]: TA).
% 125.39/88.64 thf(zero_zero_decl, type, zero_zero: !> [TA: $tType]: TA).
% 125.39/88.64 thf(suc_decl, type, suc: (nat > nat)).
% 125.39/88.64 thf(semiring_1_of_nat_decl, type, semiring_1_of_nat: !> [TA: $tType]: (nat > TA)).
% 125.39/88.64 thf(ord_less_decl, type, ord_less: !> [TA: $tType]: (TA > (TA > $o))).
% 125.39/88.64 thf(ord_less_eq_decl, type, ord_less_eq: !> [TA: $tType]: (TA > (TA > $o))).
% 125.39/88.64 thf(is_zero_decl, type, is_zero: !> [TA: $tType]: ((poly @ TA) > $o)).
% 125.39/88.64 thf(order2_decl, type, order2: !> [TA: $tType]: (TA > ((poly @ TA) > nat))).
% 125.39/88.64 thf(pderiv_decl, type, pderiv: !> [TA: $tType]: ((poly @ TA) > (poly @ TA))).
% 125.39/88.64 thf(poly2_decl, type, poly2: !> [TA: $tType]: ((poly @ TA) > (TA > TA))).
% 125.39/88.64 thf(coeff_decl, type, coeff: !> [TA: $tType]: ((poly @ TA) > (nat > TA))).
% 125.39/88.64 thf(poly_cutoff_decl, type, poly_cutoff: !> [TA: $tType]: (nat > ((poly @ TA) > (poly @ TA)))).
% 125.39/88.64 thf(poly_shift_decl, type, poly_shift: !> [TA: $tType]: (nat > ((poly @ TA) > (poly @ TA)))).
% 125.39/88.64 thf(reflect_poly_decl, type, reflect_poly: !> [TA: $tType]: ((poly @ TA) > (poly @ TA))).
% 125.39/88.64 thf(rsquarefree_decl, type, rsquarefree: !> [TA: $tType]: ((poly @ TA) > $o)).
% 125.39/88.64 thf(collect_decl, type, collect: !> [TA: $tType]: ((TA > $o) > (set @ TA))).
% 125.39/88.64 thf(sturm_424270202_cross_decl, type, sturm_424270202_cross: ((poly @ real) > (real > (real > int)))).
% 125.39/88.64 thf(sturm_1700286437_r_pos_decl, type, sturm_1700286437_r_pos: ((poly @ real) > (real > $o))).
% 125.39/88.64 thf(sturm_1771227917iation_decl, type, sturm_1771227917iation: (real > (real > int))).
% 125.39/88.64 thf(member_decl, type, member: !> [TA: $tType]: (TA > ((set @ TA) > $o))).
% 125.39/88.64 thf(p_decl, type, p: (poly @ real)).
% 125.39/88.64 thf(x_decl, type, x: real).
% 125.39/88.64 thf(sk1_decl, type, sk1: !> [TA: $tType]: ((TA > $o) > ((TA > $o) > TA))).
% 125.39/88.64 thf(sk2_decl, type, sk2: !> [TA: $tType,TB: $tType]: (TB > ((TA > TB) > (TA > (TA > TA))))).
% 125.39/88.64 thf(sk3_decl, type, sk3: !> [TA: $tType,TB: $tType]: (TB > ((TA > TB) > (TA > (TA > TA))))).
% 125.39/88.64 thf(sk4_decl, type, sk4: !> [TA: $tType]: (TA > (TA > (TA > $o)))).
% 125.39/88.64 thf(sk5_decl, type, sk5: !> [TA: $tType]: (TA > (TA > (TA > $o)))).
% 125.39/88.64 thf(sk6_decl, type, sk6: !> [TA: $tType]: (TA > (TA > (TA > $o)))).
% 125.39/88.64 thf(sk7_decl, type, sk7: !> [TA: $tType]: (TA > (TA > (TA > $o)))).
% 125.39/88.64 thf(sk1_def, definition, sk1 = (^ [TA: $tType]: (^ [A:(TA > $o),B:(TA > $o)]: (@+ [C:TA]: ~ ((B @ C) = (A @ C))))) ).
% 125.39/88.64 thf(sk2_def, definition, sk2 = (^ [TA: $tType,TB: $tType]: (^ [A:TB,B:(TA > TB),C:TA,D:TA]: (@+ [E:TA]: ~ (! [F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F))))))) ).
% 125.39/88.64 thf(sk3_def, definition, sk3 = (^ [TA: $tType,TB: $tType]: (^ [A:TB,B:(TA > TB),C:TA,D:TA]: (@+ [E:TA]: ~ ((ord_less_eq @ TA @ (sk2 @ TB @ TA @ A @ B @ C @ D) @ E) => (ord_less_eq @ TB @ (B @ (sk2 @ TB @ TA @ A @ B @ C @ D)) @ (B @ E)))))) ).
% 125.39/88.64 thf(190,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_less__nat__zero__code)).
% 125.39/88.64 thf(892,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 125.39/88.64 thf(219,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_155_bot__nat__0_Oextremum__strict)).
% 125.39/88.64 thf(1036,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 125.39/88.64 thf(335,axiom,(((ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)) => (sturm_1700286437_r_pos @ p @ x))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2__092_060open_0620_A_060_Apoly_Ap_Ax_A_092_060Longrightarrow_062_Asign__r__pos_Ap_Ax_092_060close_062)).
% 125.39/88.64 thf(1411,plain,(((ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)) => (sturm_1700286437_r_pos @ p @ x))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[335])).
% 125.39/88.64 thf(268,axiom,((! [A:(nat > nat),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less @ nat @ D @ E) => (ord_less @ nat @ (A @ D) @ (A @ E)))) => ((ord_less_eq @ nat @ B @ C) => (ord_less_eq @ nat @ (A @ B) @ (A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_less__mono__imp__le__mono)).
% 125.39/88.64 thf(1190,plain,((! [A:(nat > nat),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less @ nat @ D @ E) => (ord_less @ nat @ (A @ D) @ (A @ E)))) => ((ord_less_eq @ nat @ B @ C) => (ord_less_eq @ nat @ (A @ B) @ (A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[268])).
% 125.39/88.64 thf(56,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_dual__order_Orefl)).
% 125.39/88.64 thf(479,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 125.39/88.64 thf(4,axiom,((one @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Oone)).
% 125.39/88.64 thf(347,plain,((one @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 125.39/88.64 thf(280,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_48_pinf_I8_J)).
% 125.39/88.64 thf(1237,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)],[280])).
% 125.39/88.64 thf(196,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_5_not__gr__zero)).
% 125.39/88.64 thf(909,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)],[196])).
% 125.39/88.64 thf(66,axiom,((! [A:nat]: (ord_less_eq @ nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_249_le__refl)).
% 125.39/88.64 thf(518,plain,((! [A:nat]: (ord_less_eq @ nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 125.39/88.64 thf(51,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_77_le__funI)).
% 125.39/88.64 thf(468,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)],[51])).
% 125.39/88.64 thf(81,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_85_antisym)).
% 125.39/88.64 thf(555,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)],[81])).
% 125.39/88.64 thf(57,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_order__refl)).
% 125.39/88.64 thf(481,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 125.39/88.64 thf(6,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) | (ord_less_eq @ nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_243_nat__le__linear)).
% 125.39/88.64 thf(352,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) | (ord_less_eq @ nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 125.39/88.64 thf(94,axiom,((! [TA: $tType]: ((idom @ TA) => (idom @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Rings_Oidom_60)).
% 125.39/88.64 thf(582,plain,((! [TA: $tType]: ((idom @ TA) => (idom @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 125.39/88.64 thf(212,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_11_gr__zeroI)).
% 125.39/88.64 thf(1005,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)],[212])).
% 125.39/88.64 thf(299,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_187_not__less)).
% 125.39/88.64 thf(1290,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)],[299])).
% 125.39/88.64 thf(232,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_188_not__le)).
% 125.39/88.64 thf(1068,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)],[232])).
% 125.39/88.64 thf(209,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_dual__order_Ostrict__implies__not__eq)).
% 125.39/88.64 thf(994,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 125.39/88.64 thf(340,axiom,((! [A:nat]: ((ord_less_eq @ nat @ A @ (zero_zero @ nat)) = (A = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_bot__nat__0_Oextremum__unique)).
% 125.39/88.64 thf(1422,plain,((! [A:nat]: ((ord_less_eq @ nat @ A @ (zero_zero @ nat)) = (A = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[340])).
% 125.39/88.64 thf(101,axiom,((! [TA: $tType]: ((comm_semiring_1 @ TA) => (semiring_1 @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Rings_Osemiring__1_55)).
% 125.39/88.64 thf(597,plain,((! [TA: $tType]: ((comm_semiring_1 @ TA) => (semiring_1 @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 125.39/88.64 thf(272,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_144_pinf_I5_J)).
% 125.39/88.64 thf(1205,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)],[272])).
% 125.39/88.64 thf(43,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (order @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Orderings_Oorder_56)).
% 125.39/88.64 thf(449,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (order @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 125.39/88.64 thf(13,axiom,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((! [D:nat]: ((ord_less_eq @ nat @ (suc @ D) @ C) => (A @ D))) => (A @ C))) => (A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_240_full__nat__induct)).
% 125.39/88.64 thf(379,plain,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((! [D:nat]: ((ord_less_eq @ nat @ (suc @ D) @ C) => (A @ D))) => (A @ C))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 125.39/88.64 thf(292,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_125_less__asym)).
% 125.39/88.64 thf(1269,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)],[292])).
% 125.39/88.64 thf(183,axiom,((! [A:nat]: (ord_less @ nat @ (zero_zero @ nat) @ (suc @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_220_zero__less__Suc)).
% 125.39/88.64 thf(878,plain,((! [A:nat]: (ord_less @ nat @ (zero_zero @ nat) @ (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 125.39/88.64 thf(39,axiom,((! [TA: $tType]: (ord @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Oord_22)).
% 125.39/88.64 thf(440,plain,((! [TA: $tType]: (ord @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 125.39/88.64 thf(106,axiom,((linord1659791738miring @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Olinordered__nonzero__semiring)).
% 125.39/88.64 thf(607,plain,((linord1659791738miring @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 125.39/88.64 thf(306,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (~ (ord_less @ TA @ (zero_zero @ TA) @ (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_less__numeral__extra_I3_J)).
% 125.39/88.64 thf(1311,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (~ (ord_less @ TA @ (zero_zero @ TA) @ (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[306])).
% 125.39/88.64 thf(1312,plain,(! [TA:$tType] : ((~ (linord1659791738miring @ TA)) | (~ (ord_less @ TA @ (zero_zero @ TA) @ (zero_zero @ TA))))),inference(cnf,[status(esa)],[1311])).
% 125.39/88.64 thf(2605,plain,(! [TA:$tType] : (~ (($true)) | (~ (ord_less @ TA @ (zero_zero @ TA) @ (zero_zero @ TA))) | ((linord1659791738miring @ int) != (linord1659791738miring @ TA)))),inference(paramod_ordered,[status(thm)],[607,1312])).
% 125.39/88.64 thf(2606,plain,(! [TA:$tType] : ((~ (ord_less @ TA @ (zero_zero @ TA) @ (zero_zero @ TA))) | ((linord1659791738miring @ int) != (linord1659791738miring @ TA)))),inference(simp,[status(thm)],[2605])).
% 125.39/88.64 thf(2607,plain,((~ (ord_less @ int @ (zero_zero @ int) @ (zero_zero @ int)))),inference(pattern_uni,[status(thm)],[2606:[bind_type(TA,$thf(int))]])).
% 125.39/88.64 thf(78,axiom,((semiring_char_0 @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Nat_Osemiring__char__0)).
% 125.39/88.64 thf(550,plain,((semiring_char_0 @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 125.39/88.64 thf(261,axiom,(((ord_less @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) & (A != B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_nat__less__le)).
% 125.39/88.64 thf(1164,plain,(((ord_less @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) & ~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[261])).
% 125.39/88.64 thf(294,axiom,((! [A:nat,B:nat]: ((A != B) => ((~ (ord_less @ nat @ A @ B)) => (ord_less @ nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_60_linorder__neqE__nat)).
% 125.39/88.64 thf(1275,plain,((! [A:nat,B:nat]: ((~ (A = B)) => ((~ (ord_less @ nat @ A @ B)) => (ord_less @ nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[294])).
% 125.39/88.64 thf(53,axiom,((! [TA: $tType]: (((ring_char_0 @ TA) & (comm_ring_1 @ TA)) => (semiring_char_0 @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Nat_Osemiring__char__0_51)).
% 125.39/88.64 thf(472,plain,((! [TA: $tType]: (((ring_char_0 @ TA) & (comm_ring_1 @ TA)) => (semiring_char_0 @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 125.39/88.64 thf(279,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_191_order__le__less__subst2)).
% 125.39/88.64 thf(1233,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)],[279])).
% 125.39/88.64 thf(288,axiom,((! [TA: $tType]: ((semiring_char_0 @ TA) => (! [A:nat]: ((semiring_1_of_nat @ TA @ (suc @ A)) != (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_235_of__nat__neq__0)).
% 125.39/88.64 thf(1258,plain,((! [TA: $tType]: ((semiring_char_0 @ TA) => (! [A:nat]: ~ ((semiring_1_of_nat @ TA @ (suc @ A)) = (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[288])).
% 125.39/88.64 thf(1259,plain,(! [TA:$tType,A:nat] : ((~ (semiring_char_0 @ TA)) | (~ ((semiring_1_of_nat @ TA @ (suc @ A)) = (zero_zero @ TA))))),inference(cnf,[status(esa)],[1258])).
% 125.39/88.64 thf(1260,plain,(! [TA:$tType,A:nat] : (((semiring_1_of_nat @ TA @ (suc @ A)) != (zero_zero @ TA)) | (~ (semiring_char_0 @ TA)))),inference(lifteq,[status(thm)],[1259])).
% 125.39/88.64 thf(230,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_23_reflect__poly__at__0__eq__0__iff)).
% 125.39/88.64 thf(1063,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)],[230])).
% 125.39/88.64 thf(126,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_142_pinf_I3_J)).
% 125.39/88.64 thf(670,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)],[126])).
% 125.39/88.64 thf(161,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_179_dense__le)).
% 125.39/88.64 thf(814,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)],[161])).
% 125.39/88.64 thf(309,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_24_next__non__root__interval)).
% 125.39/88.64 thf(1327,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)],[309])).
% 125.39/88.64 thf(312,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ nat @ (suc @ A) @ (suc @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_209_Suc__mono)).
% 125.39/88.64 thf(1342,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ nat @ (suc @ A) @ (suc @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[312])).
% 125.39/88.64 thf(145,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_168_dense__ge__bounded)).
% 125.39/88.64 thf(747,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)],[145])).
% 125.39/88.64 thf(192,axiom,((! [TA: $tType]: ((field_char_0 @ TA) => (! [A:(poly @ TA),B:TA]: (((pderiv @ TA @ A) != (zero_zero @ (poly @ TA))) => (((order2 @ TA @ B @ A) != (zero_zero @ nat)) => ((order2 @ TA @ B @ A) = (suc @ (order2 @ TA @ B @ (pderiv @ TA @ A)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_order__pderiv)).
% 125.39/88.64 thf(898,plain,((! [TA: $tType]: ((field_char_0 @ TA) => (! [A:(poly @ TA),B:TA]: ((~ ((pderiv @ TA @ A) = (zero_zero @ (poly @ TA)))) => ((~ ((order2 @ TA @ B @ A) = (zero_zero @ nat))) => ((order2 @ TA @ B @ A) = (suc @ (order2 @ TA @ B @ (pderiv @ TA @ A)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 125.39/88.64 thf(154,axiom,((field_char_0 @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Fields_Ofield__char__0)).
% 125.39/88.64 thf(782,plain,((field_char_0 @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 125.39/88.64 thf(132,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_141_pinf_I2_J)).
% 125.39/88.64 thf(709,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)],[132])).
% 125.39/88.64 thf(29,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_49)).
% 125.39/88.64 thf(417,plain,((! [TA: $tType]: ((comm_semiring_1 @ TA) => (comm_semiring_1 @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 125.39/88.64 thf(1,conjecture,(((sturm_1700286437_r_pos @ p @ x) != (~ ((((poly2 @ real @ p @ x) = (zero_zero @ real)) => (sturm_1700286437_r_pos @ (pderiv @ real @ p) @ x)) & (((poly2 @ real @ p @ x) != (zero_zero @ real)) => (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 125.39/88.64 thf(2,negated_conjecture,((~ ((sturm_1700286437_r_pos @ p @ x) != (~ ((((poly2 @ real @ p @ x) = (zero_zero @ real)) => (sturm_1700286437_r_pos @ (pderiv @ real @ p) @ x)) & (((poly2 @ real @ p @ x) != (zero_zero @ real)) => (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)))))))),inference(neg_conjecture,[status(cth)],[1])).
% 125.39/88.64 thf(341,plain,((~ (~ ((sturm_1700286437_r_pos @ p @ x) = (~ ((((poly2 @ real @ p @ x) = (zero_zero @ real)) => (sturm_1700286437_r_pos @ (pderiv @ real @ p) @ x)) & ((~ ((poly2 @ real @ p @ x) = (zero_zero @ real))) => (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 125.39/88.64 thf(342,plain,(((sturm_1700286437_r_pos @ p @ x) = (~ ((((poly2 @ real @ p @ x) = (zero_zero @ real)) => (sturm_1700286437_r_pos @ (pderiv @ real @ p) @ x)) & ((~ ((poly2 @ real @ p @ x) = (zero_zero @ real))) => (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x))))))),inference(polarity_switch,[status(thm)],[341])).
% 125.39/88.64 thf(343,plain,(((sturm_1700286437_r_pos @ p @ x) = (~ ((((poly2 @ real @ p @ x) = (zero_zero @ real)) => (sturm_1700286437_r_pos @ (pderiv @ real @ p) @ x)) & ((~ ((poly2 @ real @ p @ x) = (zero_zero @ real))) => (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x))))))),inference(lifteq,[status(thm)],[342])).
% 125.39/88.64 thf(1426,plain,((sturm_1700286437_r_pos @ p @ x) | (~ (~ ((((poly2 @ real @ p @ x) = (zero_zero @ real)) => (sturm_1700286437_r_pos @ (pderiv @ real @ p) @ x)) & ((~ ((poly2 @ real @ p @ x) = (zero_zero @ real))) => (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x))))))),inference(bool_ext,[status(thm)],[343])).
% 125.39/88.64 thf(1439,plain,((((sturm_1700286437_r_pos @ p @ x) | ~ ((poly2 @ real @ p @ x) = (zero_zero @ real)) | (sturm_1700286437_r_pos @ (pderiv @ real @ p) @ x)) & ((sturm_1700286437_r_pos @ p @ x) | ((poly2 @ real @ p @ x) = (zero_zero @ real)) | (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x))))),inference(cnf,[status(esa)],[1426])).
% 125.39/88.64 thf(1441,plain,((sturm_1700286437_r_pos @ p @ x) | ((poly2 @ real @ p @ x) = (zero_zero @ real)) | (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x))),inference(cnfConj,[status(thm)],[1439])).
% 125.39/88.64 thf(1443,plain,(((poly2 @ real @ p @ x) = (zero_zero @ real)) | (sturm_1700286437_r_pos @ p @ x) | (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x))),inference(lifteq,[status(thm)],[1441])).
% 125.39/88.64 thf(156,axiom,(((poly2 @ real @ p @ x) != (zero_zero @ real))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_False)).
% 125.39/88.64 thf(786,plain,((~ ((poly2 @ real @ p @ x) = (zero_zero @ real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 125.39/88.64 thf(787,plain,((~ ((poly2 @ real @ p @ x) = (zero_zero @ real)))),inference(polarity_switch,[status(thm)],[786])).
% 125.39/88.64 thf(788,plain,(((poly2 @ real @ p @ x) != (zero_zero @ real))),inference(lifteq,[status(thm)],[787])).
% 125.39/88.64 thf(1975,plain,((sturm_1700286437_r_pos @ p @ x) | (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x))),inference(simplifyReflect,[status(thm)],[1443,788])).
% 125.39/88.64 thf(1979,plain,((ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)) | ((sturm_1700286437_r_pos @ p @ x) = (~ ((((poly2 @ real @ p @ x) = (zero_zero @ real)) => (($true))) & ((~ ((poly2 @ real @ p @ x) = (zero_zero @ real))) => (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)))))) | ((sturm_1700286437_r_pos @ (pderiv @ real @ p) @ x) != (sturm_1700286437_r_pos @ p @ x))),inference(paramod_ordered,[status(thm)],[1975,343])).
% 125.39/88.64 thf(1980,plain,((ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)) | ((sturm_1700286437_r_pos @ p @ x) = (~ ((~ ((poly2 @ real @ p @ x) = (zero_zero @ real))) => (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x))))) | ((sturm_1700286437_r_pos @ (pderiv @ real @ p) @ x) != (sturm_1700286437_r_pos @ p @ x))),inference(simp,[status(thm)],[1979])).
% 125.39/88.64 thf(1996,plain,((ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)) | ((sturm_1700286437_r_pos @ p @ x) = (~ ((~ ((poly2 @ real @ p @ x) = (zero_zero @ real))) => (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x))))) | ((pderiv @ real @ p) != p) | (x != x)),inference(simp,[status(thm)],[1980])).
% 125.39/88.64 thf(2010,plain,((ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)) | ((sturm_1700286437_r_pos @ p @ x) = (~ ((~ ((poly2 @ real @ p @ x) = (zero_zero @ real))) => (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x))))) | ((pderiv @ real @ p) != p)),inference(simp,[status(thm)],[1996])).
% 125.39/88.64 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_175_not__le__imp__less)).
% 125.39/88.64 thf(1386,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])).
% 125.39/88.64 thf(321,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_135_ord__less__eq__subst)).
% 125.39/88.64 thf(1366,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)],[321])).
% 125.39/88.64 thf(37,axiom,((condit1037483654norder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Conditionally__Complete__Lattices_Oconditionally__complete__linorder_6)).
% 125.39/88.64 thf(436,plain,((condit1037483654norder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 125.39/88.64 thf(286,axiom,((linordered_field @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Fields_Olinordered__field)).
% 125.39/88.64 thf(1254,plain,((linordered_field @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[286])).
% 125.39/88.64 thf(165,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_less__irrefl__nat)).
% 125.39/88.64 thf(827,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 125.39/88.64 thf(828,plain,((~ (? [A:nat]: (ord_less @ nat @ A @ A)))),inference(miniscope,[status(thm)],[827])).
% 125.39/88.64 thf(829,plain,(! [A:nat] : ((~ (ord_less @ nat @ A @ A)))),inference(cnf,[status(esa)],[828])).
% 125.39/88.64 thf(242,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_150_minf_I4_J)).
% 125.39/88.64 thf(1095,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)],[242])).
% 125.39/88.64 thf(15,axiom,((comm_ring_1 @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Ocomm__ring__1)).
% 125.39/88.64 thf(389,plain,((comm_ring_1 @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 125.39/88.64 thf(226,axiom,((semiri1193490041visors @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Osemiring__no__zero__divisors_29)).
% 125.39/88.64 thf(1055,plain,((semiri1193490041visors @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 125.39/88.64 thf(302,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_121_less__irrefl)).
% 125.39/88.64 thf(1298,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[302])).
% 125.39/88.64 thf(133,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_116_less__not__sym)).
% 125.39/88.64 thf(719,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)],[133])).
% 125.39/88.64 thf(290,axiom,((! [A:nat]: ((ord_less_eq @ nat @ A @ (zero_zero @ nat)) = (A = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_le__0__eq)).
% 125.39/88.64 thf(1264,plain,((! [A:nat]: ((ord_less_eq @ nat @ A @ (zero_zero @ nat)) = (A = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[290])).
% 125.39/88.64 thf(308,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_64_less__not__refl3)).
% 125.39/88.64 thf(1323,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[308])).
% 125.39/88.64 thf(307,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_140_pinf_I1_J)).
% 125.39/88.64 thf(1313,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)],[307])).
% 125.39/88.64 thf(8,axiom,((zero @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ozero_18)).
% 125.39/88.64 thf(357,plain,((zero @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 125.39/88.64 thf(228,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_163_dual__order_Ostrict__implies__order)).
% 125.39/88.64 thf(1059,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)],[228])).
% 125.39/88.64 thf(203,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_197_complete__interval)).
% 125.39/88.64 thf(949,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)],[203])).
% 125.39/88.64 thf(72,axiom,((linorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Olinorder_24)).
% 125.39/88.64 thf(542,plain,((linorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 125.39/88.64 thf(159,axiom,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((~ (A @ C)) => (? [D:nat]: ((ord_less @ nat @ D @ C) & ~ (A @ D))))) => (A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_infinite__descent)).
% 125.39/88.64 thf(802,plain,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((~ (A @ C)) => (? [D:nat]: ((ord_less @ nat @ D @ C) & ~ (A @ D))))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 125.39/88.64 thf(3,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)).
% 125.39/88.64 thf(344,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)],[3])).
% 125.39/88.64 thf(83,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_79_order__subst1)).
% 125.39/88.64 thf(559,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)],[83])).
% 125.39/88.64 thf(239,axiom,((! [A:nat]: (ord_less @ nat @ A @ (suc @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_208_lessI)).
% 125.39/88.64 thf(1087,plain,((! [A:nat]: (ord_less @ nat @ A @ (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 125.39/88.64 thf(314,axiom,((semiring_char_0 @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Nat_Osemiring__char__0_33)).
% 125.39/88.64 thf(1347,plain,((semiring_char_0 @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[314])).
% 125.39/88.64 thf(215,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_152_minf_I7_J)).
% 125.39/88.64 thf(1013,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)],[215])).
% 125.39/88.64 thf(319,axiom,((preorder @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Opreorder_34)).
% 125.39/88.64 thf(1362,plain,((preorder @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[319])).
% 125.39/88.64 thf(331,axiom,((zero @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Ozero_43)).
% 125.39/88.64 thf(1398,plain,((zero @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[331])).
% 125.39/88.64 thf(28,axiom,((! [TA: $tType]: (order @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Oorder_21)).
% 125.39/88.64 thf(415,plain,((! [TA: $tType]: (order @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 125.39/88.64 thf(416,plain,(! [TA:$tType] : ((order @ (set @ TA)))),inference(cnf,[status(esa)],[415])).
% 125.39/88.64 thf(147,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_195_leI)).
% 125.39/88.64 thf(756,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)],[147])).
% 125.39/88.64 thf(157,axiom,((! [TA: $tType]: ((field_char_0 @ TA) => ((rsquarefree @ TA) = (^ [A:(poly @ TA)]: ! [B:TA]: ~ (((poly2 @ TA @ A @ B) = (zero_zero @ TA)) & ((poly2 @ TA @ (pderiv @ TA @ A) @ B) = (zero_zero @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_rsquarefree__roots)).
% 125.39/88.64 thf(789,plain,((! [TA: $tType]: ((field_char_0 @ TA) => ((rsquarefree @ TA) = (^ [A:(poly @ TA)]: ! [B:TA]: ~ (((poly2 @ TA @ A @ B) = (zero_zero @ TA)) & ((poly2 @ TA @ (pderiv @ TA @ A) @ B) = (zero_zero @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 125.39/88.64 thf(99,axiom,((! [TA: $tType]: ((semiring_char_0 @ TA) => (! [A:nat,B:nat]: (((semiring_1_of_nat @ TA @ A) = (semiring_1_of_nat @ TA @ B)) = (A = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_of__nat__eq__iff)).
% 125.39/88.64 thf(591,plain,((! [TA: $tType]: ((semiring_char_0 @ TA) => (! [A:nat,B:nat]: (((semiring_1_of_nat @ TA @ A) = (semiring_1_of_nat @ TA @ B)) = (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 125.39/88.64 thf(247,axiom,((! [A:nat]: ((~ (ord_less @ nat @ (zero_zero @ nat) @ A)) = (A = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_160_not__gr0)).
% 125.39/88.64 thf(1109,plain,((! [A:nat]: ((~ (ord_less @ nat @ (zero_zero @ nat) @ A)) = (A = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[247])).
% 125.39/88.64 thf(310,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_6_poly__IVT__neg)).
% 125.39/88.64 thf(1334,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)],[310])).
% 125.39/88.64 thf(63,axiom,((semiri1193490041visors @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Osemiring__no__zero__divisors)).
% 125.39/88.64 thf(514,plain,((semiri1193490041visors @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 125.39/88.64 thf(353,plain,(! [B:nat,A:nat] : ((ord_less_eq @ nat @ A @ B) | (ord_less_eq @ nat @ B @ A))),inference(cnf,[status(esa)],[352])).
% 125.39/88.64 thf(298,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_199_poly__cutoff__1)).
% 125.39/88.64 thf(1283,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)],[298])).
% 125.39/88.64 thf(163,axiom,((! [TA: $tType]: ((zero @ TA) => ((poly_shift @ TA @ (zero_zero @ nat)) = (^ [A:(poly @ TA)]: (A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_poly__shift__id)).
% 125.39/88.64 thf(821,plain,((! [TA: $tType]: ((zero @ TA) => ((poly_shift @ TA @ (zero_zero @ nat)) = (^ [A:(poly @ TA)]: (A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 125.39/88.64 thf(338,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_196_leD)).
% 125.39/88.64 thf(1418,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)],[338])).
% 125.39/88.64 thf(112,axiom,((one @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Oone_19)).
% 125.39/88.64 thf(623,plain,((one @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 125.39/88.64 thf(88,axiom,((zero @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Ozero)).
% 125.39/88.64 thf(574,plain,((zero @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 125.39/88.64 thf(217,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_74_imp__le__cong)).
% 125.39/88.64 thf(1020,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)],[217])).
% 125.39/88.64 thf(5,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_80_order__subst2)).
% 125.39/88.64 thf(348,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)],[5])).
% 125.39/88.64 thf(323,axiom,((! [A:nat]: ((ord_less @ nat @ A @ (suc @ (zero_zero @ nat))) = (A = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_less__Suc0)).
% 125.39/88.64 thf(1377,plain,((! [A:nat]: ((ord_less @ nat @ A @ (suc @ (zero_zero @ nat))) = (A = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[323])).
% 125.39/88.64 thf(138,axiom,((linorder @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Olinorder_35)).
% 125.39/88.64 thf(734,plain,((linorder @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 125.39/88.64 thf(178,axiom,((order @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Oorder_40)).
% 125.39/88.64 thf(866,plain,((order @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 125.39/88.64 thf(252,axiom,((! [A:nat]: (ord_less_eq @ nat @ (zero_zero @ nat) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_less__eq__nat_Osimps_I1_J)).
% 125.39/88.64 thf(1119,plain,((! [A:nat]: (ord_less_eq @ nat @ (zero_zero @ nat) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[252])).
% 125.39/88.64 thf(20,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_50)).
% 125.39/88.64 thf(396,plain,((! [TA: $tType]: ((comm_semiring_0 @ TA) => (comm_semiring_0 @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 125.39/88.64 thf(210,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_120_ord__eq__less__trans)).
% 125.39/88.64 thf(998,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)],[210])).
% 125.39/88.64 thf(207,axiom,((! [TA: $tType]: ((zero @ TA) => (! [A:nat]: ((poly_shift @ TA @ A @ (zero_zero @ (poly @ TA))) = (zero_zero @ (poly @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_poly__shift__0)).
% 125.39/88.64 thf(988,plain,((! [TA: $tType]: ((zero @ TA) => (! [A:nat]: ((poly_shift @ TA @ A @ (zero_zero @ (poly @ TA))) = (zero_zero @ (poly @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 125.39/88.64 thf(71,axiom,((! [A:nat,B:nat,C:(nat > (nat > $o))]: ((ord_less_eq @ nat @ A @ B) => ((! [D:nat]: (C @ D @ D)) => ((! [D:nat,E:nat,F:nat]: ((C @ D @ E) => ((C @ E @ F) => (C @ D @ F)))) => ((! [D:nat]: (C @ D @ (suc @ D))) => (C @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_transitive__stepwise__le)).
% 125.39/88.64 thf(527,plain,((! [A:nat,B:nat,C:(nat > (nat > $o))]: ((ord_less_eq @ nat @ A @ B) => ((! [D:nat]: (C @ D @ D)) => ((! [D:nat,E:nat,F:nat]: ((C @ D @ E) => ((C @ E @ F) => (C @ D @ F)))) => ((! [D:nat]: (C @ D @ (suc @ D))) => (C @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 125.39/88.64 thf(276,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = ((ord_less @ TA @ B @ A) | (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_not__less__iff__gr__or__eq)).
% 125.39/88.64 thf(1215,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)],[276])).
% 125.39/88.64 thf(118,axiom,((! [TA: $tType]: ((semiring_1 @ TA) => ((semiring_1_of_nat @ TA @ (one_one @ nat)) = (one_one @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_221_of__nat__1)).
% 125.39/88.64 thf(634,plain,((! [TA: $tType]: ((semiring_1 @ TA) => ((semiring_1_of_nat @ TA @ (one_one @ nat)) = (one_one @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 125.39/88.64 thf(234,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_129_neq__iff)).
% 125.39/88.64 thf(1074,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)],[234])).
% 125.39/88.64 thf(129,axiom,((! [TA: $tType]: (! [A:(TA > nat),B:(TA > $o),C:TA]: ((! [D:TA]: (((A @ D) = (zero_zero @ nat)) => (B @ D))) => ((! [D:TA]: ((ord_less @ nat @ (zero_zero @ nat) @ (A @ D)) => ((~ (B @ D)) => (? [E:TA]: ((ord_less @ nat @ (A @ E) @ (A @ D)) & ~ (B @ E)))))) => (B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_154_infinite__descent0__measure)).
% 125.39/88.64 thf(678,plain,((! [TA: $tType]: (! [A:(TA > nat),B:(TA > $o),C:TA]: ((! [D:TA]: (((A @ D) = (zero_zero @ nat)) => (B @ D))) => ((! [D:TA]: ((ord_less @ nat @ (zero_zero @ nat) @ (A @ D)) => ((~ (B @ D)) => (? [E:TA]: ((ord_less @ nat @ (A @ E) @ (A @ D)) & ~ (B @ E)))))) => (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 125.39/88.64 thf(123,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_113_less__imp__not__eq2)).
% 125.39/88.64 thf(661,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 125.39/88.64 thf(74,axiom,((no_bot @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Ono__bot)).
% 125.39/88.64 thf(546,plain,((no_bot @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 125.39/88.64 thf(271,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_115_less__induct)).
% 125.39/88.64 thf(1199,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)],[271])).
% 125.39/88.64 thf(12,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_90_le__cases3)).
% 125.39/88.64 thf(364,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)],[12])).
% 125.39/88.64 thf(365,plain,(! [TA:$tType,C:TA,B:TA,A:TA] : (((~ (linorder @ TA) | (ord_less_eq @ TA @ A @ B) | (sk4 @ TA @ B @ A @ C)) & (~ (linorder @ TA) | (ord_less_eq @ TA @ B @ C) | (sk4 @ TA @ B @ A @ C)) & (~ (linorder @ TA) | ~ (sk4 @ TA @ B @ A @ C) | (ord_less_eq @ TA @ B @ A) | (sk5 @ TA @ A @ C @ B)) & (~ (linorder @ TA) | ~ (sk4 @ TA @ B @ A @ C) | (ord_less_eq @ TA @ A @ C) | (sk5 @ TA @ A @ C @ B)) & (~ (linorder @ TA) | ~ (sk4 @ TA @ B @ A @ C) | ~ (sk5 @ TA @ A @ C @ B) | (ord_less_eq @ TA @ A @ C) | (sk6 @ TA @ C @ B @ A)) & (~ (linorder @ TA) | ~ (sk4 @ TA @ B @ A @ C) | ~ (sk5 @ TA @ A @ C @ B) | (ord_less_eq @ TA @ C @ B) | (sk6 @ TA @ C @ B @ A)) & (~ (linorder @ TA) | ~ (sk4 @ TA @ B @ A @ C) | ~ (sk5 @ TA @ A @ C @ B) | ~ (sk6 @ TA @ C @ B @ A) | (ord_less_eq @ TA @ C @ B) | (sk7 @ TA @ B @ C @ A)) & (~ (linorder @ TA) | ~ (sk4 @ TA @ B @ A @ C) | ~ (sk5 @ TA @ A @ C @ B) | ~ (sk6 @ TA @ C @ B @ A) | (ord_less_eq @ TA @ B @ A) | (sk7 @ TA @ B @ C @ A)) & (~ (linorder @ TA) | ~ (sk4 @ TA @ B @ A @ C) | ~ (sk5 @ TA @ A @ C @ B) | ~ (sk6 @ TA @ C @ B @ A) | ~ (sk7 @ TA @ B @ C @ A) | (ord_less_eq @ TA @ B @ C) | (ord_less_eq @ TA @ C @ A)) & (~ (linorder @ TA) | ~ (sk4 @ TA @ B @ A @ C) | ~ (sk5 @ TA @ A @ C @ B) | ~ (sk6 @ TA @ C @ B @ A) | ~ (sk7 @ TA @ B @ C @ A) | (ord_less_eq @ TA @ B @ C) | (ord_less_eq @ TA @ A @ B)) & (~ (linorder @ TA) | ~ (sk4 @ TA @ B @ A @ C) | ~ (sk5 @ TA @ A @ C @ B) | ~ (sk6 @ TA @ C @ B @ A) | ~ (sk7 @ TA @ B @ C @ A) | (ord_less_eq @ TA @ C @ A) | (ord_less_eq @ TA @ C @ A)) & (~ (linorder @ TA) | ~ (sk4 @ TA @ B @ A @ C) | ~ (sk5 @ TA @ A @ C @ B) | ~ (sk6 @ TA @ C @ B @ A) | ~ (sk7 @ TA @ B @ C @ A) | (ord_less_eq @ TA @ C @ A) | (ord_less_eq @ TA @ A @ B))))),inference(cnf,[status(esa)],[364])).
% 125.39/88.64 thf(366,plain,(! [TA:$tType,C:TA,B:TA,A:TA] : ((~ (linorder @ TA)) | (~ (sk4 @ TA @ B @ A @ C)) | (~ (sk5 @ TA @ A @ C @ B)) | (~ (sk6 @ TA @ C @ B @ A)) | (~ (sk7 @ TA @ B @ C @ A)) | (ord_less_eq @ TA @ B @ C) | (ord_less_eq @ TA @ C @ A))),inference(cnfConj,[status(thm)],[365])).
% 125.39/88.64 thf(223,axiom,((! [A:nat]: ((ord_less_eq @ nat @ A @ (zero_zero @ nat)) => (A = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_bot__nat__0_Oextremum__uniqueI)).
% 125.39/88.64 thf(1047,plain,((! [A:nat]: ((ord_less_eq @ nat @ A @ (zero_zero @ nat)) => (A = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 125.39/88.64 thf(152,axiom,((comm_semiring_1 @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Ocomm__semiring__1_31)).
% 125.39/88.64 thf(778,plain,((comm_semiring_1 @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 125.39/88.64 thf(221,axiom,((! [TA: $tType]: ((semiring_char_0 @ TA) => (! [A:nat]: (((zero_zero @ TA) = (semiring_1_of_nat @ TA @ A)) = ((zero_zero @ nat) = A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_of__nat__0__eq__iff)).
% 125.39/88.64 thf(1042,plain,((! [TA: $tType]: ((semiring_char_0 @ TA) => (! [A:nat]: (((zero_zero @ TA) = (semiring_1_of_nat @ TA @ A)) = ((zero_zero @ nat) = A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 125.39/88.64 thf(287,axiom,((! [A:nat]: ((A != (zero_zero @ nat)) => (ord_less @ nat @ (zero_zero @ nat) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_161_gr0I)).
% 125.39/88.64 thf(1255,plain,((! [A:nat]: ((~ (A = (zero_zero @ nat))) => (ord_less @ nat @ (zero_zero @ nat) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[287])).
% 125.39/88.64 thf(177,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_117_less__imp__not__eq)).
% 125.39/88.64 thf(862,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 125.39/88.64 thf(116,axiom,((no_top @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Ono__top)).
% 125.39/88.64 thf(630,plain,((no_top @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 125.39/88.64 thf(34,axiom,((! [TA: $tType]: ((zero @ TA) => (zero @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Groups_Ozero_59)).
% 125.39/88.64 thf(429,plain,((! [TA: $tType]: ((zero @ TA) => (zero @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 125.39/88.64 thf(136,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_184_antisym__conv2)).
% 125.39/88.64 thf(729,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)],[136])).
% 125.39/88.64 thf(9,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_87_eq__refl)).
% 125.39/88.64 thf(358,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)],[9])).
% 125.39/88.64 thf(359,plain,(! [TA:$tType,B:TA,A:TA] : ((~ (preorder @ TA)) | (~ (A = B)) | (ord_less_eq @ TA @ A @ B))),inference(cnf,[status(esa)],[358])).
% 125.39/88.64 thf(360,plain,(! [TA:$tType,B:TA,A:TA] : ((A != B) | (~ (preorder @ TA)) | (ord_less_eq @ TA @ A @ B))),inference(lifteq,[status(thm)],[359])).
% 125.39/88.64 thf(361,plain,(! [TA:$tType,A:TA] : ((~ (preorder @ TA)) | (ord_less_eq @ TA @ A @ A))),inference(simp,[status(thm)],[360])).
% 125.39/88.64 thf(114,axiom,((! [TA: $tType]: ((comm_semiring_1 @ TA) => (one @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Groups_Oone_61)).
% 125.39/88.65 thf(625,plain,((! [TA: $tType]: ((comm_semiring_1 @ TA) => (one @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 125.39/88.65 thf(266,axiom,((! [TA: $tType,TB: $tType]: ((wellorder @ TB) => (! [A:(TA > TB),B:(TA > $o),C:TA]: ((! [D:TA]: ((! [E:TA]: ((ord_less @ TB @ (A @ E) @ (A @ D)) => (B @ E))) => (B @ D))) => (B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_137_measure__induct__rule)).
% 125.39/88.65 thf(1178,plain,((! [TA: $tType,TB: $tType]: ((wellorder @ TB) => (! [A:(TA > TB),B:(TA > $o),C:TA]: ((! [D:TA]: ((! [E:TA]: ((ord_less @ TB @ (A @ E) @ (A @ D)) => (B @ E))) => (B @ D))) => (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[266])).
% 125.39/88.65 thf(48,axiom,((! [TA: $tType]: (preorder @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Opreorder_20)).
% 125.39/88.65 thf(461,plain,((! [TA: $tType]: (preorder @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 125.39/88.65 thf(236,axiom,((! [A:real]: ((sturm_1771227917iation @ A @ (zero_zero @ real)) = (zero_zero @ int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_227_variation__0_I2_J)).
% 125.39/88.65 thf(1079,plain,((! [A:real]: ((sturm_1771227917iation @ A @ (zero_zero @ real)) = (zero_zero @ int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[236])).
% 125.39/88.65 thf(2343,plain,(! [TA:$tType,A:nat] : (((semiring_1_of_nat @ TA @ (suc @ A)) != (zero_zero @ TA)) | ~ (($true)) | ((semiring_char_0 @ int) != (semiring_char_0 @ TA)))),inference(paramod_ordered,[status(thm)],[550,1260])).
% 125.39/88.65 thf(2344,plain,(! [TA:$tType,A:nat] : (((semiring_1_of_nat @ TA @ (suc @ A)) != (zero_zero @ TA)) | ((semiring_char_0 @ int) != (semiring_char_0 @ TA)))),inference(simp,[status(thm)],[2343])).
% 125.39/88.65 thf(2345,plain,(! [A:nat] : (((semiring_1_of_nat @ int @ (suc @ A)) != (zero_zero @ int)))),inference(pattern_uni,[status(thm)],[2344:[bind_type(TA,$thf(int))]])).
% 125.39/88.65 thf(296,axiom,((idom @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Oidom_44)).
% 125.39/88.65 thf(1281,plain,((idom @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[296])).
% 125.39/88.65 thf(46,axiom,((comm_semiring_1 @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Ocomm__semiring__1_9)).
% 125.39/88.65 thf(456,plain,((comm_semiring_1 @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 125.39/88.65 thf(246,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_107_exists__least__iff)).
% 125.39/88.65 thf(1106,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)],[246])).
% 125.39/88.65 thf(172,axiom,((! [TA: $tType]: ((semiring_char_0 @ TA) => (! [A:nat]: (((semiring_1_of_nat @ TA @ A) = (zero_zero @ TA)) = (A = (zero_zero @ nat))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_216_of__nat__eq__0__iff)).
% 125.39/88.65 thf(847,plain,((! [TA: $tType]: ((semiring_char_0 @ TA) => (! [A:nat]: (((semiring_1_of_nat @ TA @ A) = (zero_zero @ TA)) = (A = (zero_zero @ nat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 125.39/88.65 thf(85,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_95_order__class_Oorder_Oantisym)).
% 125.39/88.65 thf(566,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)],[85])).
% 125.39/88.65 thf(301,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_verit__comp__simplify1_I1_J)).
% 125.39/88.65 thf(1296,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[301])).
% 125.39/88.65 thf(124,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_124_less__asym_H)).
% 125.39/88.65 thf(665,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)],[124])).
% 125.39/88.65 thf(68,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_86_linear)).
% 125.39/88.65 thf(522,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)],[68])).
% 125.39/88.65 thf(166,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_164_dual__order_Ostrict__iff__order)).
% 125.39/88.65 thf(830,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)],[166])).
% 125.39/88.65 thf(269,axiom,((! [A:nat]: ((A != (zero_zero @ nat)) = (ord_less @ nat @ (zero_zero @ nat) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_neq0__conv)).
% 125.39/88.65 thf(1195,plain,((! [A:nat]: ((~ (A = (zero_zero @ nat))) = (ord_less @ nat @ (zero_zero @ nat) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[269])).
% 125.39/88.65 thf(333,axiom,((one @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Oone_45)).
% 125.39/88.65 thf(1407,plain,((one @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[333])).
% 125.39/88.65 thf(79,axiom,((wellorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Owellorder)).
% 125.39/88.65 thf(551,plain,((wellorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 125.39/88.65 thf(254,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_13_gr__implies__not__zero)).
% 125.39/88.65 thf(1125,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)],[254])).
% 125.39/88.65 thf(1126,plain,(! [TA:$tType,B:TA,A:TA] : ((~ (canoni770627133id_add @ TA)) | (~ (ord_less @ TA @ A @ B)) | (~ (B = (zero_zero @ TA))))),inference(cnf,[status(esa)],[1125])).
% 125.39/88.65 thf(1127,plain,(! [TA:$tType,B:TA,A:TA] : ((B != (zero_zero @ TA)) | (~ (canoni770627133id_add @ TA)) | (~ (ord_less @ TA @ A @ B)))),inference(lifteq,[status(thm)],[1126])).
% 125.39/88.65 thf(1128,plain,(! [TA:$tType,A:TA] : ((~ (canoni770627133id_add @ TA)) | (~ (ord_less @ TA @ A @ (zero_zero @ TA))))),inference(simp,[status(thm)],[1127])).
% 125.39/88.65 thf(316,axiom,((! [TA: $tType]: ((semiring_1 @ TA) => ((semiring_1_of_nat @ TA @ (zero_zero @ nat)) = (zero_zero @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_214_of__nat__0)).
% 125.39/88.65 thf(1350,plain,((! [TA: $tType]: ((semiring_1 @ TA) => ((semiring_1_of_nat @ TA @ (zero_zero @ nat)) = (zero_zero @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[316])).
% 125.39/88.65 thf(240,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_133_order__less__subst2)).
% 125.39/88.65 thf(1089,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)],[240])).
% 125.39/88.65 thf(253,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (B != (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_157_gr__implies__not0)).
% 125.39/88.65 thf(1121,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (~ (B = (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[253])).
% 125.39/88.65 thf(24,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_98_linorder__wlog)).
% 125.39/88.65 thf(403,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)],[24])).
% 125.39/88.65 thf(14,axiom,((ord @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oord_26)).
% 125.39/88.65 thf(388,plain,((ord @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 125.39/88.65 thf(180,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_158_less__zeroE)).
% 125.39/88.65 thf(869,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 125.39/88.65 thf(108,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_82_ord__eq__le__subst)).
% 125.39/88.65 thf(610,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)],[108])).
% 125.39/88.65 thf(155,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_234_less__fun__def)).
% 125.39/88.65 thf(783,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)],[155])).
% 125.39/88.65 thf(143,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_17_poly__eq__poly__eq__iff)).
% 125.39/88.65 thf(742,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)],[143])).
% 125.39/88.65 thf(92,axiom,((semiring_1 @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Osemiring__1)).
% 125.39/88.65 thf(578,plain,((semiring_1 @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 125.39/88.65 thf(256,axiom,((sturm_424270202_cross = (^ [A:(poly @ real),B:real,C:real]: (sturm_1771227917iation @ (poly2 @ real @ A @ B) @ (poly2 @ real @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_204_cross__def)).
% 125.39/88.65 thf(1138,plain,(((sturm_424270202_cross) = (^ [A:(poly @ real),B:real,C:real]: (sturm_1771227917iation @ (poly2 @ real @ A @ B) @ (poly2 @ real @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[256])).
% 125.39/88.65 thf(7,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (! [A:nat,B:nat]: ((ord_less_eq @ TA @ (semiring_1_of_nat @ TA @ A) @ (semiring_1_of_nat @ TA @ B)) = (ord_less_eq @ nat @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_218_of__nat__le__iff)).
% 125.39/88.65 thf(354,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (! [A:nat,B:nat]: ((ord_less_eq @ TA @ (semiring_1_of_nat @ TA @ A) @ (semiring_1_of_nat @ TA @ B)) = (ord_less_eq @ nat @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 125.39/88.65 thf(355,plain,(! [TA:$tType,B:nat,A:nat] : ((~ (linord1659791738miring @ TA)) | ((ord_less_eq @ TA @ (semiring_1_of_nat @ TA @ A) @ (semiring_1_of_nat @ TA @ B)) = (ord_less_eq @ nat @ A @ B)))),inference(cnf,[status(esa)],[354])).
% 125.39/88.65 thf(356,plain,(! [TA:$tType,B:nat,A:nat] : (((ord_less_eq @ TA @ (semiring_1_of_nat @ TA @ A) @ (semiring_1_of_nat @ TA @ B)) = (ord_less_eq @ nat @ A @ B)) | (~ (linord1659791738miring @ TA)))),inference(lifteq,[status(thm)],[355])).
% 125.39/88.65 thf(175,axiom,(((sturm_1700286437_r_pos @ p @ x) => (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1__092_060open_062sign__r__pos_Ap_Ax_A_092_060Longrightarrow_062_A0_A_060_Apoly_Ap_Ax_092_060close_062)).
% 125.39/88.65 thf(857,plain,(((sturm_1700286437_r_pos @ p @ x) => (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 125.39/88.65 thf(330,axiom,((no_top @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Ono__top_38)).
% 125.39/88.65 thf(1397,plain,((no_top @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[330])).
% 125.39/88.65 thf(187,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_173_order_Ostrict__trans2)).
% 125.39/88.65 thf(884,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)],[187])).
% 125.39/88.65 thf(237,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_145_pinf_I7_J)).
% 125.39/88.65 thf(1082,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)],[237])).
% 125.39/88.65 thf(60,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (linordered_idom @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Rings_Olinordered__idom)).
% 125.39/88.65 thf(488,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (linordered_idom @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 125.39/88.65 thf(200,axiom,((p != (zero_zero @ (poly @ real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_assms)).
% 125.39/88.65 thf(933,plain,((~ (p = (zero_zero @ (poly @ real))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 125.39/88.65 thf(193,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_14_zero__less__iff__neq__zero)).
% 125.39/88.65 thf(901,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)],[193])).
% 125.39/88.65 thf(119,axiom,((! [A:nat,B:nat]: ((~ (ord_less_eq @ nat @ A @ B)) = (ord_less_eq @ nat @ (suc @ B) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_241_not__less__eq__eq)).
% 125.39/88.65 thf(637,plain,((! [A:nat,B:nat]: ((~ (ord_less_eq @ nat @ A @ B)) = (ord_less_eq @ nat @ (suc @ B) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 125.39/88.65 thf(273,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_not__less__zero)).
% 125.39/88.65 thf(1207,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[273])).
% 125.39/88.65 thf(220,axiom,((! [TA: $tType]: ((field_char_0 @ TA) => (! [A:(poly @ TA),B:TA,C:nat]: (((pderiv @ TA @ A) != (zero_zero @ (poly @ TA))) => (((order2 @ TA @ B @ A) != (zero_zero @ nat)) => (((order2 @ TA @ B @ (pderiv @ TA @ A)) = C) = ((order2 @ TA @ B @ A) = (suc @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_order__pderiv2)).
% 125.39/88.65 thf(1039,plain,((! [TA: $tType]: ((field_char_0 @ TA) => (! [A:(poly @ TA),B:TA,C:nat]: ((~ ((pderiv @ TA @ A) = (zero_zero @ (poly @ TA)))) => ((~ ((order2 @ TA @ B @ A) = (zero_zero @ nat))) => (((order2 @ TA @ B @ (pderiv @ TA @ A)) = C) = ((order2 @ TA @ B @ A) = (suc @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 125.39/88.65 thf(75,axiom,((comm_semiring_0 @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Ocomm__semiring__0_10)).
% 125.39/88.65 thf(547,plain,((comm_semiring_0 @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 125.39/88.65 thf(250,axiom,((! [A:real]: ((sturm_1771227917iation @ (zero_zero @ real) @ A) = (zero_zero @ int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_variation__0_I1_J)).
% 125.39/88.65 thf(1114,plain,((! [A:real]: ((sturm_1771227917iation @ (zero_zero @ real) @ A) = (zero_zero @ int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 125.39/88.65 thf(64,axiom,((semiring_char_0 @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Nat_Osemiring__char__0_11)).
% 125.39/88.65 thf(515,plain,((semiring_char_0 @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 125.39/88.65 thf(325,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_192_order__le__less__subst1)).
% 125.39/88.65 thf(1382,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)],[325])).
% 125.39/88.65 thf(134,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_25_last__non__root__interval)).
% 125.39/88.65 thf(721,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)],[134])).
% 125.39/88.65 thf(211,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ (suc @ B)) = (ord_less @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_210_Suc__less__eq)).
% 125.39/88.65 thf(1002,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ (suc @ B)) = (ord_less @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 125.39/88.65 thf(153,axiom,((! [A:nat]: ((ord_less @ nat @ A @ (one_one @ nat)) = (A = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_224_less__one)).
% 125.39/88.65 thf(779,plain,((! [A:nat]: ((ord_less @ nat @ A @ (one_one @ nat)) = (A = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 125.39/88.65 thf(111,axiom,((order @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oorder_25)).
% 125.39/88.65 thf(622,plain,((order @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 125.39/88.65 thf(169,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_22_poly__cutoff__0)).
% 125.39/88.65 thf(837,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)],[169])).
% 125.39/88.65 thf(243,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_49_pinf_I6_J)).
% 125.39/88.65 thf(1099,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)],[243])).
% 125.39/88.65 thf(206,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_114_antisym__conv3)).
% 125.39/88.65 thf(985,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)],[206])).
% 125.39/88.65 thf(224,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_174_order_Ostrict__trans1)).
% 125.39/88.65 thf(1050,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)],[224])).
% 125.39/88.65 thf(47,axiom,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_eq__imp__le)).
% 125.39/88.65 thf(457,plain,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 125.39/88.65 thf(86,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_92_order__class_Oorder_Oeq__iff)).
% 125.39/88.65 thf(569,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)],[86])).
% 125.39/88.65 thf(148,axiom,((linord1659791738miring @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Olinordered__nonzero__semiring_28)).
% 125.39/88.65 thf(758,plain,((linord1659791738miring @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 125.39/88.65 thf(2860,plain,(! [TA:$tType] : (~ (($true)) | (~ (ord_less @ TA @ (zero_zero @ TA) @ (zero_zero @ TA))) | ((linord1659791738miring @ real) != (linord1659791738miring @ TA)))),inference(paramod_ordered,[status(thm)],[758,1312])).
% 125.39/88.65 thf(2861,plain,(! [TA:$tType] : ((~ (ord_less @ TA @ (zero_zero @ TA) @ (zero_zero @ TA))) | ((linord1659791738miring @ real) != (linord1659791738miring @ TA)))),inference(simp,[status(thm)],[2860])).
% 125.39/88.65 thf(2862,plain,((~ (ord_less @ real @ (zero_zero @ real) @ (zero_zero @ real)))),inference(pattern_uni,[status(thm)],[2861:[bind_type(TA,$thf(real))]])).
% 125.39/88.65 thf(105,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (ord @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Orderings_Oord_58)).
% 125.39/88.65 thf(605,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (ord @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 125.39/88.65 thf(329,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_less__not__refl2)).
% 125.39/88.65 thf(1393,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[329])).
% 125.39/88.65 thf(158,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_147_minf_I1_J)).
% 125.39/88.65 thf(792,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)],[158])).
% 125.39/88.65 thf(282,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_143_pinf_I4_J)).
% 125.39/88.65 thf(1241,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)],[282])).
% 125.39/88.65 thf(150,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_122_less__linear)).
% 125.39/88.65 thf(765,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)],[150])).
% 125.39/88.65 thf(263,axiom,((! [A:nat]: (ord_less_eq @ nat @ (zero_zero @ nat) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_le0)).
% 125.39/88.65 thf(1170,plain,((! [A:nat]: (ord_less_eq @ nat @ (zero_zero @ nat) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[263])).
% 125.39/88.65 thf(21,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_57)).
% 125.39/88.65 thf(398,plain,((! [TA: $tType]: (((ring_char_0 @ TA) & (comm_ring_1 @ TA)) => (ring_char_0 @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 125.39/88.65 thf(127,axiom,((ord @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Oord_42)).
% 125.39/88.65 thf(674,plain,((ord @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 125.39/88.65 thf(97,axiom,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Opreorder)).
% 125.39/88.65 thf(586,plain,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 125.39/88.65 thf(189,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_119_ord__less__eq__trans)).
% 125.39/88.65 thf(888,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)],[189])).
% 125.39/88.65 thf(82,axiom,((no_top @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Ono__top_15)).
% 125.39/88.65 thf(558,plain,((no_top @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 125.39/88.65 thf(233,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_159_not__less0)).
% 125.39/88.65 thf(1071,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 125.39/88.65 thf(295,axiom,((! [TA: $tType]: (((comm_semiring_1 @ TA) & (semiri1193490041visors @ TA)) => ((pderiv @ TA @ (zero_zero @ (poly @ TA))) = (zero_zero @ (poly @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_pderiv__0)).
% 125.39/88.65 thf(1278,plain,((! [TA: $tType]: (((comm_semiring_1 @ TA) & (semiri1193490041visors @ TA)) => ((pderiv @ TA @ (zero_zero @ (poly @ TA))) = (zero_zero @ (poly @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[295])).
% 125.39/88.65 thf(26,axiom,((semiri1193490041visors @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Osemiring__no__zero__divisors_8)).
% 125.39/88.65 thf(412,plain,((semiri1193490041visors @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 125.39/88.65 thf(32,axiom,((order @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Oorder_4)).
% 125.39/88.65 thf(425,plain,((order @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 125.39/88.65 thf(245,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_36_not__eq__pos__or__neg__iff__1)).
% 125.39/88.65 thf(1103,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)],[245])).
% 125.39/88.65 thf(144,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_dual__order_Oirrefl)).
% 125.39/88.65 thf(745,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 125.39/88.65 thf(41,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ (suc @ B)) => ((~ (ord_less_eq @ nat @ A @ B)) => (A = (suc @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_251_le__SucE)).
% 125.39/88.65 thf(444,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ (suc @ B)) => ((~ (ord_less_eq @ nat @ A @ B)) => (A = (suc @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 125.39/88.65 thf(103,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_100_dual__order_Oeq__iff)).
% 125.39/88.65 thf(601,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)],[103])).
% 125.39/88.65 thf(285,axiom,((! [TA: $tType]: (((comm_semiring_1 @ TA) & (semiri1193490041visors @ TA)) => (! [A:nat]: ((pderiv @ TA @ (semiring_1_of_nat @ (poly @ TA) @ A)) = (zero_zero @ (poly @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_212_pderiv__of__nat)).
% 125.39/88.65 thf(1251,plain,((! [TA: $tType]: (((comm_semiring_1 @ TA) & (semiri1193490041visors @ TA)) => (! [A:nat]: ((pderiv @ TA @ (semiring_1_of_nat @ (poly @ TA) @ A)) = (zero_zero @ (poly @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[285])).
% 125.39/88.65 thf(109,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ B @ C) => (ord_less_eq @ nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_247_le__trans)).
% 125.39/88.65 thf(618,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ B @ C) => (ord_less_eq @ nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 125.39/88.65 thf(278,axiom,((! [A:(nat > $o),B:nat]: ((A @ B) => ((~ (A @ (zero_zero @ nat))) => (? [C:nat]: ((ord_less_eq @ nat @ C @ B) & ! [D:nat]: ((ord_less @ nat @ D @ C) => (~ (A @ D))) & (A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_ex__least__nat__le)).
% 125.39/88.65 thf(1219,plain,((! [A:(nat > $o),B:nat]: ((A @ B) => ((~ (A @ (zero_zero @ nat))) => (? [C:nat]: ((ord_less_eq @ nat @ C @ B) & ! [D:nat]: ((ord_less @ nat @ D @ C) => (~ (A @ D))) & (A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[278])).
% 125.39/88.65 thf(164,axiom,((! [TA: $tType]: ((zero @ TA) => (! [A:TA]: (((zero_zero @ TA) = A) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_zero__reorient)).
% 125.39/88.65 thf(824,plain,((! [TA: $tType]: ((zero @ TA) => (! [A:TA]: (((zero_zero @ TA) = A) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 125.39/88.65 thf(349,plain,(! [TA:$tType,TB:$tType,D:TB,C:(TA > TB),B:TA,A:TA] : (((~ (order @ TB) | ~ (order @ TA) | ~ (ord_less_eq @ TA @ A @ B) | ~ (ord_less_eq @ TB @ (C @ B) @ D) | (ord_less_eq @ TA @ (sk2 @ TB @ TA @ D @ (C) @ B @ A) @ (sk3 @ TB @ TA @ D @ (C) @ B @ A)) | (ord_less_eq @ TB @ (C @ A) @ D)) & (~ (order @ TB) | ~ (order @ TA) | ~ (ord_less_eq @ TA @ A @ B) | ~ (ord_less_eq @ TB @ (C @ B) @ D) | ~ (ord_less_eq @ TB @ (C @ (sk2 @ TB @ TA @ D @ (C) @ B @ A)) @ (C @ (sk3 @ TB @ TA @ D @ (C) @ B @ A))) | (ord_less_eq @ TB @ (C @ A) @ D))))),inference(cnf,[status(esa)],[348])).
% 125.39/88.65 thf(351,plain,(! [TA:$tType,TB:$tType,D:TB,C:(TA > TB),B:TA,A:TA] : ((~ (order @ TB)) | (~ (order @ TA)) | (~ (ord_less_eq @ TA @ A @ B)) | (~ (ord_less_eq @ TB @ (C @ B) @ D)) | (~ (ord_less_eq @ TB @ (C @ (sk2 @ TB @ TA @ D @ (C) @ B @ A)) @ (C @ (sk3 @ TB @ TA @ D @ (C) @ B @ A)))) | (ord_less_eq @ TB @ (C @ A) @ D))),inference(cnfConj,[status(thm)],[349])).
% 125.39/88.65 thf(1989,plain,(! [TA:$tType,D:$o,C:(TA > $o),B:TA,A:TA] : ((ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)) | (~ (order @ $o)) | (~ (order @ TA)) | (~ (ord_less_eq @ TA @ A @ B)) | (~ (ord_less_eq @ $o @ ($true) @ D)) | (~ (ord_less_eq @ $o @ (C @ (sk2 @ $o @ TA @ D @ (C) @ B @ A)) @ (C @ (sk3 @ $o @ TA @ D @ (C) @ B @ A)))) | (ord_less_eq @ $o @ (C @ A) @ D) | ((sturm_1700286437_r_pos @ p @ x) != (C @ B)))),inference(paramod_ordered,[status(thm)],[1975,351])).
% 125.39/88.65 thf(1997,plain,(! [TA:$tType,C:$o,B:TA,A:TA] : ((ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)) | (~ (order @ $o)) | (~ (order @ TA)) | (~ (ord_less_eq @ TA @ A @ B)) | (~ (ord_less_eq @ $o @ ($true) @ C)) | (~ (ord_less_eq @ $o @ (sturm_1700286437_r_pos @ p @ x) @ (sturm_1700286437_r_pos @ p @ x))) | (ord_less_eq @ $o @ (sturm_1700286437_r_pos @ p @ x) @ C))),inference(pre_uni,[status(thm)],[1989:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(^ [E:TA]: (sturm_1700286437_r_pos @ p @ x))),bind(D, $thf(D))]])).
% 125.39/88.65 thf(2011,plain,(! [TA:$tType,C:$o,B:TA,A:TA] : ((ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)) | (~ (order @ $o)) | (~ (order @ TA)) | (~ (ord_less_eq @ TA @ A @ B)) | (~ (ord_less_eq @ $o @ ($true) @ C)) | (~ (ord_less_eq @ $o @ (sturm_1700286437_r_pos @ p @ x) @ (sturm_1700286437_r_pos @ p @ x))) | (ord_less_eq @ $o @ (sturm_1700286437_r_pos @ p @ x) @ C))),inference(simp,[status(thm)],[1997])).
% 125.39/88.65 thf(2893,plain,(! [TA:$tType,C:$o,B:TA,A:TA] : ((ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)) | ~ (($true)) | (~ (order @ TA)) | (~ (ord_less_eq @ TA @ A @ B)) | (~ (ord_less_eq @ $o @ ($true) @ C)) | (~ (ord_less_eq @ $o @ (sturm_1700286437_r_pos @ p @ x) @ (sturm_1700286437_r_pos @ p @ x))) | (ord_less_eq @ $o @ (sturm_1700286437_r_pos @ p @ x) @ C))),inference(rewrite,[status(thm)],[2011,622])).
% 125.39/88.65 thf(2894,plain,(! [TA:$tType,C:$o,B:TA,A:TA] : ((ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)) | (~ (order @ TA)) | (~ (ord_less_eq @ TA @ A @ B)) | (~ (ord_less_eq @ $o @ ($true) @ C)) | (~ (ord_less_eq @ $o @ (sturm_1700286437_r_pos @ p @ x) @ (sturm_1700286437_r_pos @ p @ x))) | (ord_less_eq @ $o @ (sturm_1700286437_r_pos @ p @ x) @ C))),inference(simp,[status(thm)],[2893])).
% 125.39/88.65 thf(322,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_162_order_Onot__eq__order__implies__strict)).
% 125.39/88.65 thf(1374,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)],[322])).
% 125.39/88.65 thf(95,axiom,((order @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Oorder_16)).
% 125.39/88.65 thf(584,plain,((order @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 125.39/88.65 thf(194,axiom,((! [TA: $tType]: (((comm_semiring_1 @ TA) & (semiri1193490041visors @ TA)) => ((pderiv @ TA @ (one_one @ (poly @ TA))) = (zero_zero @ (poly @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_pderiv__1)).
% 125.39/88.65 thf(904,plain,((! [TA: $tType]: (((comm_semiring_1 @ TA) & (semiri1193490041visors @ TA)) => ((pderiv @ TA @ (one_one @ (poly @ TA))) = (zero_zero @ (poly @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 125.39/88.65 thf(23,axiom,((idom @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Oidom)).
% 125.39/88.65 thf(402,plain,((idom @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 125.39/88.65 thf(137,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_123_less__trans)).
% 125.39/88.65 thf(732,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)],[137])).
% 125.39/88.65 thf(327,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_128_order_Oasym)).
% 125.39/88.65 thf(1388,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)],[327])).
% 125.39/88.65 thf(93,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_78_le__fun__def)).
% 125.39/88.65 thf(579,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)],[93])).
% 125.39/88.65 thf(27,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (preorder @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Orderings_Opreorder_52)).
% 125.39/88.65 thf(413,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (preorder @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 125.39/88.65 thf(182,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_4_poly__0)).
% 125.39/88.65 thf(875,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)],[182])).
% 125.39/88.65 thf(91,axiom,((ord @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Oord_5)).
% 125.39/88.65 thf(577,plain,((ord @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 125.39/88.65 thf(17,axiom,((! [TA: $tType]: ((semiring_char_0 @ TA) => (! [A:nat]: (((semiring_1_of_nat @ TA @ A) = (one_one @ TA)) = (A = (one_one @ nat))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_223_of__nat__eq__1__iff)).
% 125.39/88.65 thf(391,plain,((! [TA: $tType]: ((semiring_char_0 @ TA) => (! [A:nat]: (((semiring_1_of_nat @ TA @ A) = (one_one @ TA)) = (A = (one_one @ nat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 125.39/88.65 thf(201,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_171_order_Ostrict__iff__order)).
% 125.39/88.65 thf(936,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)],[201])).
% 125.39/88.65 thf(87,axiom,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oorder)).
% 125.39/88.65 thf(572,plain,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 125.39/88.65 thf(293,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_126_less__imp__neq)).
% 125.39/88.65 thf(1271,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[293])).
% 125.39/88.65 thf(62,axiom,((! [A:(nat > $o),B:nat,C:nat]: ((A @ B) => ((! [D:nat]: ((A @ D) => (ord_less_eq @ nat @ D @ C))) => (? [D:nat]: ((A @ D) & ! [E:nat]: ((A @ E) => (ord_less_eq @ nat @ E @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_Nat_Oex__has__greatest__nat)).
% 125.39/88.65 thf(498,plain,((! [A:(nat > $o),B:nat,C:nat]: ((A @ B) => ((! [D:nat]: ((A @ D) => (ord_less_eq @ nat @ D @ C))) => (? [D:nat]: ((A @ D) & ! [E:nat]: ((A @ E) => (ord_less_eq @ nat @ E @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 125.39/88.65 thf(281,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_183_less__imp__le)).
% 125.39/88.65 thf(1239,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)],[281])).
% 125.39/88.65 thf(318,axiom,((! [TA: $tType,TB: $tType]: ((wellorder @ TB) => (! [A:(TA > TB),B:(TA > $o),C:TA]: ((! [D:TA]: ((! [E:TA]: ((ord_less @ TB @ (A @ E) @ (A @ D)) => (B @ E))) => (B @ D))) => (B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_measure__induct)).
% 125.39/88.65 thf(1356,plain,((! [TA: $tType,TB: $tType]: ((wellorder @ TB) => (! [A:(TA > TB),B:(TA > $o),C:TA]: ((! [D:TA]: ((! [E:TA]: ((ord_less @ TB @ (A @ E) @ (A @ D)) => (B @ E))) => (B @ D))) => (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[318])).
% 125.39/88.65 thf(350,plain,(! [TA:$tType,TB:$tType,D:TB,C:(TA > TB),B:TA,A:TA] : ((~ (order @ TB)) | (~ (order @ TA)) | (~ (ord_less_eq @ TA @ A @ B)) | (~ (ord_less_eq @ TB @ (C @ B) @ D)) | (ord_less_eq @ TA @ (sk2 @ TB @ TA @ D @ (C) @ B @ A) @ (sk3 @ TB @ TA @ D @ (C) @ B @ A)) | (ord_less_eq @ TB @ (C @ A) @ D))),inference(cnfConj,[status(thm)],[349])).
% 125.39/88.65 thf(104,axiom,((comm_semiring_1 @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Ocomm__semiring__1)).
% 125.39/88.65 thf(604,plain,((comm_semiring_1 @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 125.39/88.65 thf(274,axiom,((! [A:nat]: ((A != (zero_zero @ nat)) = (ord_less @ nat @ (zero_zero @ nat) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_bot__nat__0_Onot__eq__extremum)).
% 125.39/88.65 thf(1209,plain,((! [A:nat]: ((~ (A = (zero_zero @ nat))) = (ord_less @ nat @ (zero_zero @ nat) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[274])).
% 125.39/88.65 thf(334,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (! [A:nat]: ((ord_less @ TA @ (zero_zero @ TA) @ (semiring_1_of_nat @ TA @ A)) = (ord_less @ nat @ (zero_zero @ nat) @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_201_of__nat__0__less__iff)).
% 125.39/88.65 thf(1408,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (! [A:nat]: ((ord_less @ TA @ (zero_zero @ TA) @ (semiring_1_of_nat @ TA @ A)) = (ord_less @ nat @ (zero_zero @ nat) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[334])).
% 125.39/88.65 thf(297,axiom,((ring_n68954251visors @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Oring__no__zero__divisors_30)).
% 125.39/88.65 thf(1282,plain,((ring_n68954251visors @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[297])).
% 125.39/88.65 thf(251,axiom,(((ord_less_eq @ real) = (^ [A:real,B:real]: ((ord_less @ real @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_less__eq__real__def)).
% 125.39/88.65 thf(1117,plain,(((ord_less_eq @ real) = (^ [A:real,B:real]: ((ord_less @ real @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[251])).
% 125.39/88.65 thf(30,axiom,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_205_nat_Oinject)).
% 125.39/88.65 thf(419,plain,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 125.39/88.65 thf(140,axiom,((comm_ring_1 @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Ocomm__ring__1_36)).
% 125.39/88.65 thf(736,plain,((comm_ring_1 @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 125.39/88.65 thf(141,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less_eq @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_less__imp__le__nat)).
% 125.39/88.65 thf(737,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less_eq @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 125.39/88.65 thf(184,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_182_le__less__trans)).
% 125.39/88.65 thf(880,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)],[184])).
% 125.39/88.65 thf(102,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less_eq @ nat @ A @ (suc @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_250_le__SucI)).
% 125.39/88.65 thf(599,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less_eq @ nat @ A @ (suc @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 125.39/88.65 thf(10,axiom,((linorder @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Olinorder)).
% 125.39/88.65 thf(362,plain,((linorder @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 125.39/88.65 thf(44,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_84_eq__iff)).
% 125.39/88.65 thf(451,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)],[44])).
% 125.39/88.65 thf(55,axiom,((! [TA: $tType]: (((comm_semiring_0 @ TA) & (semiri1193490041visors @ TA)) => (semiri1193490041visors @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Rings_Osemiring__no__zero__divisors_47)).
% 125.39/88.65 thf(477,plain,((! [TA: $tType]: (((comm_semiring_0 @ TA) & (semiri1193490041visors @ TA)) => (semiri1193490041visors @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 125.39/88.65 thf(160,axiom,((! [TA: $tType]: ((zero @ TA) => ((is_zero @ TA) = (^ [A:(poly @ TA)]: (A = (zero_zero @ (poly @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_is__zero__null)).
% 125.39/88.65 thf(811,plain,((! [TA: $tType]: ((zero @ TA) => ((is_zero @ TA) = (^ [A:(poly @ TA)]: (A = (zero_zero @ (poly @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 125.39/88.65 thf(117,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)).
% 125.39/88.65 thf(631,plain,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ (B))) = (B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 125.39/88.65 thf(100,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ B @ A) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_244_le__antisym)).
% 125.39/88.65 thf(594,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 125.39/88.65 thf(110,axiom,((condit1037483654norder @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Conditionally__Complete__Lattices_Oconditionally__complete__linorder)).
% 125.39/88.65 thf(621,plain,((condit1037483654norder @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 125.39/88.65 thf(58,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_101_dual__order_Oantisym)).
% 125.39/88.65 thf(483,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)],[58])).
% 125.39/88.65 thf(67,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oord)).
% 125.39/88.65 thf(520,plain,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 125.39/88.65 thf(258,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_less__not__refl)).
% 125.39/88.65 thf(1149,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[258])).
% 125.39/88.65 thf(313,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_176_less__le__not__le)).
% 125.39/88.65 thf(1344,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)],[313])).
% 125.39/88.65 thf(300,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_50_verit__comp__simplify1_I3_J)).
% 125.39/88.65 thf(1293,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)],[300])).
% 125.39/88.65 thf(248,axiom,((comm_semiring_0 @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Ocomm__semiring__0_32)).
% 125.39/88.65 thf(1112,plain,((comm_semiring_0 @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[248])).
% 125.39/88.65 thf(367,plain,(! [TA:$tType,C:TA,B:TA,A:TA] : ((~ (linorder @ TA)) | (~ (sk4 @ TA @ B @ A @ C)) | (~ (sk5 @ TA @ A @ C @ B)) | (~ (sk6 @ TA @ C @ B @ A)) | (ord_less_eq @ TA @ B @ A) | (sk7 @ TA @ B @ C @ A))),inference(cnfConj,[status(thm)],[365])).
% 125.39/88.65 thf(80,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_81_verit__la__disequality)).
% 125.39/88.65 thf(552,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)],[80])).
% 125.39/88.65 thf(218,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_7_poly__IVT__pos)).
% 125.39/88.65 thf(1029,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)],[218])).
% 125.39/88.65 thf(191,axiom,((! [TA: $tType]: ((zero @ TA) => (! [A:(poly @ TA)]: (((coeff @ TA @ (reflect_poly @ TA @ A) @ (zero_zero @ nat)) = (zero_zero @ TA)) = (A = (zero_zero @ (poly @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_200_coeff__0__reflect__poly__0__iff)).
% 125.39/88.65 thf(895,plain,((! [TA: $tType]: ((zero @ TA) => (! [A:(poly @ TA)]: (((coeff @ TA @ (reflect_poly @ TA @ A) @ (zero_zero @ nat)) = (zero_zero @ TA)) = (A = (zero_zero @ (poly @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 125.39/88.65 thf(462,plain,(! [TA:$tType] : ((preorder @ (set @ TA)))),inference(cnf,[status(esa)],[461])).
% 125.39/88.65 thf(199,axiom,((no_bot @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Ono__bot_39)).
% 125.39/88.65 thf(932,plain,((no_bot @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 125.39/88.65 thf(229,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_108_less__imp__not__less)).
% 125.39/88.65 thf(1061,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)],[229])).
% 125.39/88.65 thf(197,axiom,((! [A:(nat > $o),B:nat]: ((A @ (zero_zero @ nat)) => ((! [C:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ C) => ((~ (A @ C)) => (? [D:nat]: ((ord_less @ nat @ D @ C) & ~ (A @ D)))))) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_156_infinite__descent0)).
% 125.39/88.65 thf(912,plain,((! [A:(nat > $o),B:nat]: ((A @ (zero_zero @ nat)) => ((! [C:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ C) => ((~ (A @ C)) => (? [D:nat]: ((ord_less @ nat @ D @ C) & ~ (A @ D)))))) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 125.39/88.65 thf(270,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_153_minf_I11_J)).
% 125.39/88.65 thf(1198,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[270])).
% 125.39/88.65 thf(283,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_172_order_Oorder__iff__strict)).
% 125.39/88.65 thf(1245,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)],[283])).
% 125.39/88.65 thf(231,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_151_minf_I5_J)).
% 125.39/88.65 thf(1066,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)],[231])).
% 125.39/88.65 thf(186,axiom,((dense_order @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Odense__order)).
% 125.39/88.65 thf(883,plain,((dense_order @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 125.39/88.65 thf(216,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_10_field__lbound__gt__zero)).
% 125.39/88.65 thf(1015,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)],[216])).
% 125.39/88.65 thf(18,axiom,((canoni770627133id_add @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocanonically__ordered__monoid__add)).
% 125.39/88.65 thf(394,plain,((canoni770627133id_add @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 125.39/88.65 thf(35,axiom,((ord @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Oord_17)).
% 125.39/88.65 thf(431,plain,((ord @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 125.39/88.65 thf(151,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_31_complete__real)).
% 125.39/88.65 thf(768,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)],[151])).
% 125.39/88.65 thf(265,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_118_dual__order_Oasym)).
% 125.39/88.65 thf(1176,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)],[265])).
% 125.39/88.65 thf(107,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (linorder @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Orderings_Olinorder_53)).
% 125.39/88.65 thf(608,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (linorder @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 125.39/88.65 thf(249,axiom,((dense_linorder @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Odense__linorder)).
% 125.39/88.65 thf(1113,plain,((dense_linorder @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[249])).
% 125.39/88.65 thf(84,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_239_verit__la__generic)).
% 125.39/88.65 thf(563,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)],[84])).
% 125.39/88.65 thf(336,axiom,((! [TA: $tType]: ((idom @ TA) => (! [A:TA]: ((order2 @ TA @ A @ (one_one @ (poly @ TA))) = (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_order__1__eq__0)).
% 125.39/88.65 thf(1413,plain,((! [TA: $tType]: ((idom @ TA) => (! [A:TA]: ((order2 @ TA @ A @ (one_one @ (poly @ TA))) = (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[336])).
% 125.39/88.65 thf(304,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_167_dense__le__bounded)).
% 125.39/88.65 thf(1304,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)],[304])).
% 125.39/88.65 thf(76,axiom,((comm_semiring_0 @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Ocomm__semiring__0)).
% 125.39/88.65 thf(548,plain,((comm_semiring_0 @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 125.39/88.65 thf(339,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_181_less__le__trans)).
% 125.39/88.65 thf(1420,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)],[339])).
% 125.39/88.65 thf(65,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_89_order_Otrans)).
% 125.39/88.65 thf(516,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)],[65])).
% 125.39/88.65 thf(202,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_148_minf_I2_J)).
% 125.39/88.65 thf(939,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)],[202])).
% 125.39/88.65 thf(61,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_83_ord__le__eq__subst)).
% 125.39/88.65 thf(490,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)],[61])).
% 125.39/88.65 thf(128,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_111_linorder__cases)).
% 125.39/88.65 thf(675,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)],[128])).
% 125.39/88.65 thf(33,axiom,((! [TA: $tType]: ((semiring_char_0 @ TA) => (! [A:nat]: (((one_one @ TA) = (semiring_1_of_nat @ TA @ A)) = (A = (one_one @ nat))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_222_of__nat__1__eq__iff)).
% 125.39/88.65 thf(426,plain,((! [TA: $tType]: ((semiring_char_0 @ TA) => (! [A:nat]: (((one_one @ TA) = (semiring_1_of_nat @ TA @ A)) = (A = (one_one @ nat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 125.39/88.65 thf(262,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_order_Ostrict__implies__not__eq)).
% 125.39/88.65 thf(1166,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[262])).
% 125.39/88.65 thf(70,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_76_le__funE)).
% 125.39/88.65 thf(525,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)],[70])).
% 125.39/88.65 thf(120,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_93_ord__eq__le__trans)).
% 125.39/88.65 thf(640,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)],[120])).
% 125.39/88.65 thf(181,axiom,((! [A:nat,B:nat]: ((A != B) = ((ord_less @ nat @ A @ B) | (ord_less @ nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_nat__neq__iff)).
% 125.39/88.65 thf(872,plain,((! [A:nat,B:nat]: ((~ (A = B)) = ((ord_less @ nat @ A @ B) | (ord_less @ nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 125.39/88.65 thf(142,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_194_le__less)).
% 125.39/88.65 thf(739,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)],[142])).
% 125.39/88.65 thf(291,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_42_minf_I8_J)).
% 125.39/88.65 thf(1267,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)],[291])).
% 125.39/88.65 thf(25,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)).
% 125.39/88.65 thf(409,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 125.39/88.65 thf(303,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_134_order__less__subst1)).
% 125.39/88.65 thf(1300,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)],[303])).
% 125.39/88.65 thf(441,plain,(! [TA:$tType] : ((ord @ (set @ TA)))),inference(cnf,[status(esa)],[440])).
% 125.39/88.65 thf(96,axiom,((linorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Olinorder_13)).
% 125.39/88.65 thf(585,plain,((linorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 125.39/88.65 thf(170,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_180_dense__ge)).
% 125.39/88.65 thf(840,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)],[170])).
% 125.39/88.65 thf(49,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_99_dual__order_Otrans)).
% 125.39/88.65 thf(463,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)],[49])).
% 125.39/88.65 thf(277,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_146_pinf_I11_J)).
% 125.39/88.65 thf(1218,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[277])).
% 125.39/88.65 thf(195,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_166_order_Ostrict__implies__order)).
% 125.39/88.65 thf(907,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)],[195])).
% 125.39/88.65 thf(52,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_88_le__cases)).
% 125.39/88.65 thf(470,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)],[52])).
% 125.39/88.65 thf(90,axiom,((ring_n68954251visors @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Oring__no__zero__divisors)).
% 125.39/88.65 thf(576,plain,((ring_n68954251visors @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 125.39/88.65 thf(317,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_8_poly__all__0__iff__0)).
% 125.39/88.65 thf(1353,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)],[317])).
% 125.39/88.65 thf(225,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_177_le__imp__less__or__eq)).
% 125.39/88.65 thf(1052,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)],[225])).
% 125.39/88.65 thf(213,axiom,(((ord_less_eq @ nat) = (^ [A:nat,B:nat]: ((ord_less @ nat @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_le__eq__less__or__eq)).
% 125.39/88.65 thf(1008,plain,(((ord_less_eq @ nat) = (^ [A:nat,B:nat]: ((ord_less @ nat @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 125.39/88.65 thf(176,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_165_dual__order_Oorder__iff__strict)).
% 125.39/88.65 thf(859,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)],[176])).
% 125.39/88.65 thf(208,axiom,((! [TA: $tType]: ((zero @ TA) => ((reflect_poly @ TA @ (zero_zero @ (poly @ TA))) = (zero_zero @ (poly @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_reflect__poly__0)).
% 125.39/88.65 thf(991,plain,((! [TA: $tType]: ((zero @ TA) => ((reflect_poly @ TA @ (zero_zero @ (poly @ TA))) = (zero_zero @ (poly @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 125.39/88.65 thf(204,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_149_minf_I3_J)).
% 125.39/88.65 thf(978,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)],[204])).
% 125.39/88.65 thf(257,axiom,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((! [D:nat]: ((ord_less @ nat @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_nat__less__induct)).
% 125.39/88.65 thf(1140,plain,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((! [D:nat]: ((ord_less @ nat @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[257])).
% 125.39/88.65 thf(50,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_91_antisym__conv)).
% 125.39/88.65 thf(465,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)],[50])).
% 125.39/88.65 thf(115,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_213_reflect__poly__1)).
% 125.39/88.65 thf(627,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)],[115])).
% 125.39/88.65 thf(238,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_130_neqE)).
% 125.39/88.65 thf(1084,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)],[238])).
% 125.39/88.65 thf(11,axiom,((ring_char_0 @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Nat_Oring__char__0)).
% 125.39/88.65 thf(363,plain,((ring_char_0 @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 125.39/88.65 thf(130,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => ((A != B) => (ord_less @ nat @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_le__neq__implies__less)).
% 125.39/88.65 thf(688,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => ((~ (A = B)) => (ord_less @ nat @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 125.39/88.65 thf(69,axiom,((linord1659791738miring @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Olinordered__nonzero__semiring_7)).
% 125.39/88.65 thf(524,plain,((linord1659791738miring @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 125.39/88.65 thf(149,axiom,((! [A:nat,B:nat]: (((ord_less @ nat @ A @ B) | (A = B)) => (ord_less_eq @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_less__or__eq__imp__le)).
% 125.39/88.65 thf(759,plain,((! [A:nat,B:nat]: (((ord_less @ nat @ A @ B) | (A = B)) => (ord_less_eq @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 125.39/88.65 thf(214,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_226_poly__1)).
% 125.39/88.65 thf(1010,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)],[214])).
% 125.39/88.65 thf(328,axiom,((! [TA: $tType]: ((zero @ TA) => (! [A:nat]: ((coeff @ TA @ (zero_zero @ (poly @ TA)) @ A) = (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_225_coeff__0)).
% 125.39/88.65 thf(1390,plain,((! [TA: $tType]: ((zero @ TA) => (! [A:nat]: ((coeff @ TA @ (zero_zero @ (poly @ TA)) @ A) = (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[328])).
% 125.39/88.65 thf(2340,plain,(! [TA:$tType,A:nat] : (((semiring_1_of_nat @ TA @ (suc @ A)) != (zero_zero @ TA)) | ~ (($true)) | ((semiring_char_0 @ nat) != (semiring_char_0 @ TA)))),inference(paramod_ordered,[status(thm)],[515,1260])).
% 125.39/88.65 thf(2341,plain,(! [TA:$tType,A:nat] : (((semiring_1_of_nat @ TA @ (suc @ A)) != (zero_zero @ TA)) | ((semiring_char_0 @ nat) != (semiring_char_0 @ TA)))),inference(simp,[status(thm)],[2340])).
% 125.39/88.65 thf(2342,plain,(! [A:nat] : (((semiring_1_of_nat @ nat @ (suc @ A)) != (zero_zero @ nat)))),inference(pattern_uni,[status(thm)],[2341:[bind_type(TA,$thf(nat))]])).
% 125.39/88.65 thf(368,plain,(! [TA:$tType,C:TA,B:TA,A:TA] : ((~ (linorder @ TA)) | (ord_less_eq @ TA @ A @ B) | (sk4 @ TA @ B @ A @ C))),inference(cnfConj,[status(thm)],[365])).
% 125.39/88.65 thf(171,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (! [A:nat,B:nat]: ((ord_less @ TA @ (semiring_1_of_nat @ TA @ A) @ (semiring_1_of_nat @ TA @ B)) = (ord_less @ nat @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_217_of__nat__less__iff)).
% 125.39/88.65 thf(844,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (! [A:nat,B:nat]: ((ord_less @ TA @ (semiring_1_of_nat @ TA @ A) @ (semiring_1_of_nat @ TA @ B)) = (ord_less @ nat @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 125.39/88.65 thf(1425,plain,((~ (sturm_1700286437_r_pos @ p @ x)) | (~ ((((poly2 @ real @ p @ x) = (zero_zero @ real)) => (sturm_1700286437_r_pos @ (pderiv @ real @ p) @ x)) & ((~ ((poly2 @ real @ p @ x) = (zero_zero @ real))) => (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)))))),inference(bool_ext,[status(thm)],[343])).
% 125.39/88.65 thf(1431,plain,(((~ (sturm_1700286437_r_pos @ p @ x) | ((poly2 @ real @ p @ x) = (zero_zero @ real)) | ~ ((poly2 @ real @ p @ x) = (zero_zero @ real))) & (~ (sturm_1700286437_r_pos @ p @ x) | ((poly2 @ real @ p @ x) = (zero_zero @ real)) | ~ (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x))) & (~ (sturm_1700286437_r_pos @ p @ x) | ~ (sturm_1700286437_r_pos @ (pderiv @ real @ p) @ x) | ~ ((poly2 @ real @ p @ x) = (zero_zero @ real))) & (~ (sturm_1700286437_r_pos @ p @ x) | ~ (sturm_1700286437_r_pos @ (pderiv @ real @ p) @ x) | ~ (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x))))),inference(cnf,[status(esa)],[1425])).
% 125.39/88.65 thf(1433,plain,((~ (sturm_1700286437_r_pos @ p @ x)) | ((poly2 @ real @ p @ x) = (zero_zero @ real)) | (~ (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)))),inference(cnfConj,[status(thm)],[1431])).
% 125.39/88.65 thf(1437,plain,(((poly2 @ real @ p @ x) = (zero_zero @ real)) | (~ (sturm_1700286437_r_pos @ p @ x)) | (~ (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)))),inference(lifteq,[status(thm)],[1433])).
% 125.39/88.65 thf(1646,plain,((~ (sturm_1700286437_r_pos @ p @ x)) | (~ (ord_less @ real @ (zero_zero @ real) @ (poly2 @ real @ p @ x)))),inference(simplifyReflect,[status(thm)],[1437,788])).
% 125.39/88.65 thf(98,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ (suc @ B)) = ((ord_less_eq @ nat @ A @ B) | (A = (suc @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_245_le__Suc__eq)).
% 125.39/88.65 thf(588,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ (suc @ B)) = ((ord_less_eq @ nat @ A @ B) | (A = (suc @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 125.39/88.65 thf(311,axiom,((condit1037483654norder @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Conditionally__Complete__Lattices_Oconditionally__complete__linorder_27)).
% 125.39/88.65 thf(1341,plain,((condit1037483654norder @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[311])).
% 125.39/88.65 thf(244,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_105_dual__order_Ostrict__trans)).
% 125.39/88.65 thf(1101,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)],[244])).
% 125.39/88.65 thf(16,axiom,((linordered_idom @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Olinordered__idom_2)).
% 125.39/88.65 thf(390,plain,((linordered_idom @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 125.39/88.65 thf(125,axiom,((! [TA: $tType]: ((idom @ TA) => ((rsquarefree @ TA) = (^ [A:(poly @ TA)]: ((A != (zero_zero @ (poly @ TA))) & ! [B:TA]: (((order2 @ TA @ B @ A) = (zero_zero @ nat)) | ((order2 @ TA @ B @ A) = (one_one @ nat))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_198_rsquarefree__def)).
% 125.39/88.65 thf(667,plain,((! [TA: $tType]: ((idom @ TA) => ((rsquarefree @ TA) = (^ [A:(poly @ TA)]: (~ (A = (zero_zero @ (poly @ TA))) & ! [B:TA]: (((order2 @ TA @ B @ A) = (zero_zero @ nat)) | ((order2 @ TA @ B @ A) = (one_one @ nat))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 125.39/88.65 thf(198,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_193_less__le)).
% 125.39/88.65 thf(929,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)],[198])).
% 125.39/88.65 thf(235,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: (ord_less_eq @ TA @ (zero_zero @ TA) @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_zero__le)).
% 125.39/88.65 thf(1077,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: (ord_less_eq @ TA @ (zero_zero @ TA) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 125.39/88.65 thf(275,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_185_antisym__conv1)).
% 125.39/88.65 thf(1212,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)],[275])).
% 125.39/88.65 thf(77,axiom,((preorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Opreorder_23)).
% 125.39/88.65 thf(549,plain,((preorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 125.39/88.65 thf(222,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (ord_less_eq @ TA @ (zero_zero @ TA) @ (zero_zero @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_le__numeral__extra_I3_J)).
% 125.39/88.65 thf(1045,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (ord_less_eq @ TA @ (zero_zero @ TA) @ (zero_zero @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 125.39/88.65 thf(260,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_186_le__neq__trans)).
% 125.39/88.65 thf(1161,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)],[260])).
% 125.39/88.65 thf(345,plain,(! [TA:$tType,B:(TA > $o),A:(TA > $o)] : ((~ ((A @ (sk1 @ TA @ (B) @ (A))) = (B @ (sk1 @ TA @ (B) @ (A))))) | ((collect @ TA @ (A)) = (collect @ TA @ (B))))),inference(cnf,[status(esa)],[344])).
% 125.39/88.65 thf(346,plain,(! [TA:$tType,B:(TA > $o),A:(TA > $o)] : (((A @ (sk1 @ TA @ (B) @ (A))) != (B @ (sk1 @ TA @ (B) @ (A)))) | ((collect @ TA @ (A)) = (collect @ TA @ (B))))),inference(lifteq,[status(thm)],[345])).
% 125.39/88.65 thf(305,axiom,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_gt__ex)).
% 125.39/88.65 thf(1309,plain,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[305])).
% 125.39/88.65 thf(315,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_109_order_Ostrict__trans)).
% 125.39/88.65 thf(1348,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)],[315])).
% 125.39/88.65 thf(146,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_189_order__less__le__subst2)).
% 125.39/88.65 thf(752,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)],[146])).
% 125.39/88.65 thf(42,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_96_order__trans)).
% 125.39/88.65 thf(447,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)],[42])).
% 125.39/88.65 thf(36,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_94_ord__le__eq__trans)).
% 125.39/88.65 thf(432,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)],[36])).
% 125.39/88.65 thf(167,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_43_minf_I6_J)).
% 125.39/88.65 thf(833,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)],[167])).
% 125.39/88.65 thf(168,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_112_less__imp__triv)).
% 125.39/88.65 thf(835,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)],[168])).
% 125.39/88.65 thf(162,axiom,((! [TA: $tType]: ((zero @ TA) => (! [A:(poly @ TA)]: (((coeff @ TA @ A @ (zero_zero @ nat)) != (zero_zero @ TA)) => ((reflect_poly @ TA @ (reflect_poly @ TA @ A)) = A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_reflect__poly__reflect__poly)).
% 125.39/88.65 thf(818,plain,((! [TA: $tType]: ((zero @ TA) => (! [A:(poly @ TA)]: ((~ ((coeff @ TA @ A @ (zero_zero @ nat)) = (zero_zero @ TA))) => ((reflect_poly @ TA @ (reflect_poly @ TA @ A)) = A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 125.39/88.65 thf(324,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_170_dual__order_Ostrict__trans1)).
% 125.39/88.65 thf(1380,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)],[324])).
% 125.39/88.65 thf(174,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (! [A:nat]: ((ord_less_eq @ TA @ (semiring_1_of_nat @ TA @ A) @ (zero_zero @ TA)) = (A = (zero_zero @ nat))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_of__nat__le__0__iff)).
% 125.39/88.65 thf(854,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (! [A:nat]: ((ord_less_eq @ TA @ (semiring_1_of_nat @ TA @ A) @ (zero_zero @ TA)) = (A = (zero_zero @ nat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 125.39/88.65 thf(179,axiom,(((one_one @ nat) = (suc @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_233_One__nat__def)).
% 125.39/88.65 thf(867,plain,(((one_one @ nat) = (suc @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 125.39/88.65 thf(139,axiom,((ring_char_0 @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Nat_Oring__char__0_41)).
% 125.39/88.65 thf(735,plain,((ring_char_0 @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 125.39/88.65 thf(31,axiom,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_old_Onat_Oinject)).
% 125.39/88.65 thf(422,plain,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 125.39/88.65 thf(284,axiom,((! [TA: $tType]: ((idom @ TA) => (! [A:(poly @ TA),B:TA]: (((poly2 @ TA @ A @ B) != (zero_zero @ TA)) => ((order2 @ TA @ B @ A) = (zero_zero @ nat))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_order__0I)).
% 125.39/88.65 thf(1248,plain,((! [TA: $tType]: ((idom @ TA) => (! [A:(poly @ TA),B:TA]: ((~ ((poly2 @ TA @ A @ B) = (zero_zero @ TA))) => ((order2 @ TA @ B @ A) = (zero_zero @ nat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[284])).
% 125.39/88.65 thf(320,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_37_not__eq__pos__or__neg__iff__2)).
% 125.39/88.65 thf(1363,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)],[320])).
% 125.39/88.65 thf(38,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ (suc @ A) @ B) => (? [C:nat]: (B = (suc @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_248_Suc__le__D)).
% 125.39/88.65 thf(437,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ (suc @ A) @ B) => (? [C:nat]: (B = (suc @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 125.39/88.65 thf(227,axiom,((! [TA: $tType]: ((idom @ TA) => (! [A:(poly @ TA),B:TA]: (((poly2 @ TA @ A @ B) = (zero_zero @ TA)) = ((A = (zero_zero @ (poly @ TA))) | ((order2 @ TA @ B @ A) != (zero_zero @ nat)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_order__root)).
% 125.39/88.65 thf(1056,plain,((! [TA: $tType]: ((idom @ TA) => (! [A:(poly @ TA),B:TA]: (((poly2 @ TA @ A @ B) = (zero_zero @ TA)) = ((A = (zero_zero @ (poly @ TA))) | ~ ((order2 @ TA @ B @ A) = (zero_zero @ nat)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 125.39/88.65 thf(22,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_54)).
% 125.39/88.65 thf(400,plain,((! [TA: $tType]: ((comm_ring_1 @ TA) => (comm_ring_1 @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 125.39/88.65 thf(264,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_127_dense)).
% 125.39/88.65 thf(1172,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)],[264])).
% 125.39/88.65 thf(54,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ (suc @ A) @ (suc @ B)) = (ord_less_eq @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_211_Suc__le__mono)).
% 125.39/88.65 thf(474,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ (suc @ A) @ (suc @ B)) = (ord_less_eq @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 125.39/88.65 thf(188,axiom,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_132_lt__ex)).
% 125.39/88.65 thf(886,plain,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 125.39/88.65 thf(135,axiom,((linordered_idom @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Olinordered__idom_1)).
% 125.39/88.65 thf(728,plain,((linordered_idom @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 125.39/88.65 thf(255,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_20_cross__no__root)).
% 125.39/88.65 thf(1129,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)],[255])).
% 125.39/88.65 thf(289,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_18_cross__0)).
% 125.39/88.65 thf(1261,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)],[289])).
% 125.39/88.65 thf(89,axiom,((preorder @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Opreorder_3)).
% 125.39/88.65 thf(575,plain,((preorder @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 125.39/88.65 thf(259,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_73_conj__le__cong)).
% 125.39/88.65 thf(1152,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)],[259])).
% 125.39/88.65 thf(121,axiom,((! [A:nat,B:nat,C:(nat > $o)]: ((ord_less_eq @ nat @ A @ B) => ((C @ A) => ((! [D:nat]: ((ord_less_eq @ nat @ A @ D) => ((C @ D) => (C @ (suc @ D))))) => (C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_237_nat__induct__at__least)).
% 125.39/88.65 thf(644,plain,((! [A:nat,B:nat,C:(nat > $o)]: ((ord_less_eq @ nat @ A @ B) => ((C @ A) => ((! [D:nat]: ((ord_less_eq @ nat @ A @ D) => ((C @ D) => (C @ (suc @ D))))) => (C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 125.39/88.65 thf(173,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_190_order__less__le__subst1)).
% 125.39/88.65 thf(850,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)],[173])).
% 125.39/88.65 thf(205,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_28_le__zero__eq)).
% 125.39/88.65 thf(982,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)],[205])).
% 125.39/88.65 thf(131,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_106_linorder__less__wlog)).
% 125.39/88.65 thf(691,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)],[131])).
% 125.39/88.65 thf(40,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (linord1659791738miring @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Rings_Olinordered__nonzero__semiring_46)).
% 125.39/88.65 thf(442,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (linord1659791738miring @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 125.39/88.65 thf(870,plain,((~ (? [A:nat]: (ord_less @ nat @ A @ (zero_zero @ nat))))),inference(miniscope,[status(thm)],[869])).
% 125.39/88.65 thf(871,plain,(! [A:nat] : ((~ (ord_less @ nat @ A @ (zero_zero @ nat))))),inference(cnf,[status(esa)],[870])).
% 125.39/88.65 thf(332,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_136_ord__eq__less__subst)).
% 125.39/88.65 thf(1399,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)],[332])).
% 125.39/88.65 thf(241,axiom,((! [A:nat]: (ord_less_eq @ nat @ (zero_zero @ nat) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_bot__nat__0_Oextremum)).
% 125.39/88.65 thf(1093,plain,((! [A:nat]: (ord_less_eq @ nat @ (zero_zero @ nat) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 125.39/88.65 thf(19,axiom,((preorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Opreorder_12)).
% 125.39/88.65 thf(395,plain,((preorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 125.39/88.65 thf(113,axiom,((semiring_1 @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Osemiring__1_14)).
% 125.39/88.65 thf(624,plain,((semiring_1 @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 125.39/88.65 thf(59,axiom,((! [TA: $tType]: ((idom @ TA) => (ring_n68954251visors @ (poly @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Polynomial_Opoly___Rings_Oring__no__zero__divisors_48)).
% 125.39/88.65 thf(486,plain,((! [TA: $tType]: ((idom @ TA) => (ring_n68954251visors @ (poly @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 125.39/88.65 thf(934,plain,((~ (p = (zero_zero @ (poly @ real))))),inference(polarity_switch,[status(thm)],[933])).
% 125.39/88.65 thf(935,plain,((p != (zero_zero @ (poly @ real)))),inference(lifteq,[status(thm)],[934])).
% 125.39/88.65 thf(267,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > nat),C:TA]: ((! [D:TA]: ((~ (A @ D)) => (? [E:TA]: ((ord_less @ nat @ (B @ E) @ (B @ D)) & ~ (A @ E))))) => (A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_infinite__descent__measure)).
% 125.39/88.65 thf(1184,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > nat),C:TA]: ((! [D:TA]: ((~ (A @ D)) => (? [E:TA]: ((ord_less @ nat @ (B @ E) @ (B @ D)) & ~ (A @ E))))) => (A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[267])).
% 125.39/88.65 thf(122,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_178_le__less__linear)).
% 125.39/88.65 thf(659,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)],[122])).
% 125.39/88.65 thf(73,axiom,((! [A:nat]: ~ (ord_less_eq @ nat @ (suc @ A) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_242_Suc__n__not__le__n)).
% 125.39/88.65 thf(543,plain,((! [A:nat]: ~ (ord_less_eq @ nat @ (suc @ A) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 125.39/88.65 thf(337,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_169_dual__order_Ostrict__trans2)).
% 125.39/88.65 thf(1416,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)],[337])).
% 125.39/88.65 thf(45,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_75_le__funD)).
% 125.39/88.65 thf(454,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)],[45])).
% 125.39/88.65 thf(185,axiom,((semiring_1 @ real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Osemiring__1_37)).
% 125.39/88.65 thf(882,plain,((semiring_1 @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 125.39/88.65 thf(3271,plain,(($false)),inference(e,[status(thm)],[892,1036,1411,1190,479,347,1237,909,518,468,555,481,352,582,1005,1290,1068,994,1422,597,1205,449,379,1269,878,440,2607,550,1164,1275,472,1233,1260,1063,670,814,1327,1342,747,898,782,709,417,2010,1386,1366,436,1254,829,1095,389,1055,1298,719,1264,1323,1313,357,1059,949,542,802,344,559,1087,1347,1013,1362,1398,416,756,789,591,1109,1334,514,353,1283,821,1418,623,574,1020,348,1377,734,866,1119,396,998,988,527,1975,1215,634,1074,678,661,546,1199,366,1311,1047,778,1042,1255,862,630,429,788,729,361,625,1178,461,1079,2345,1281,456,1106,847,566,1296,665,522,830,1195,1407,551,1128,1350,1089,1121,403,388,869,610,783,742,578,1138,356,857,1397,884,1082,488,933,901,637,1207,1039,547,1114,515,1382,721,1002,779,622,837,1099,985,1050,457,569,2862,605,1393,343,792,1241,765,1170,398,674,586,888,558,1071,1278,412,425,1103,745,444,601,1251,618,1219,824,2894,1374,584,904,402,732,1125,1388,579,413,875,577,391,936,572,1271,1312,498,1239,1258,1356,350,604,1209,1408,1282,1117,419,736,737,880,599,362,451,477,811,631,758,594,621,483,520,1149,1344,1293,1112,367,552,1029,895,462,932,1061,912,1198,1245,1066,883,1015,394,431,768,827,1176,608,1113,563,1413,1304,548,1420,516,939,490,675,426,1166,525,640,872,739,1267,409,1300,441,585,840,463,1218,907,470,576,1353,1052,1008,859,991,978,1140,465,627,1084,363,688,524,759,1010,1390,2342,368,844,1646,588,1341,1101,351,390,786,667,929,1077,1212,549,1045,1161,346,1309,1348,752,447,432,833,835,818,1380,854,867,735,422,1248,1363,341,358,437,1056,400,1172,474,886,415,728,1129,1261,575,1152,644,850,982,691,442,871,1399,607,1093,395,624,486,354,935,1184,659,543,1416,454,364,882])).
% 125.39/88.65 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 125.39/88.65 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------