%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP194^1 : 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 : n007.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 17.99s 5.15s
% Output : Refutation 18.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP194^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.09/0.22 % Computer : n007.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.22 % CPULimit : 300
% 0.09/0.22 % WCLimit : 300
% 0.09/0.22 % DateTime : Tue Sep 29 20:08:11 UTC 2026
% 0.09/0.22 % CPUTime :
% 0.09/0.22 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.00/0.84 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.87/1.20 % [INFO] Parsing done (351ms).
% 2.15/1.21 % [INFO] Running in sequential loop mode.
% 3.08/1.59 % [INFO] eprover registered as external prover.
% 3.34/1.60 % [INFO] Scanning for conjecture ...
% 3.53/1.73 % [INFO] Found a conjecture (or negated_conjecture) and 350 axioms. Running axiom selection ...
% 3.71/1.86 % [INFO] Axiom selection finished. Selected 282 axioms (removed 68 axioms).
% 4.50/2.07 % [INFO] Problem is higher-order (TPTP THF).
% 4.50/2.09 % [INFO] Type checking passed.
% 4.50/2.10 % [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 ...
% 17.99/5.14 % External prover 'e' found a proof!
% 17.99/5.14 % [INFO] Killing All external provers ...
% 17.99/5.14 % Time passed: 4779ms (effective reasoning time: 3925ms)
% 17.99/5.14 % 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)>
% 17.99/5.15 % Axioms used in derivation (282): fact_311_order_Ostrict__trans, fact_52_min_Oleft__commute, fact_199_nat__descend__induct, fact_96_min_Omono, fact_129_not__eq__pos__or__neg__iff__2, fact_320_not__less__iff__gr__or__eq, fact_160_le__trans, fact_226_le__cases, fact_35_min_Oleft__idem, fact_258_ord__less__eq__subst, fact_223_le__cases3, fact_244_order__subst2, fact_181_gr__implies__not0, fact_94_le__numeral__extra_I3_J, fact_183_not__less0, fact_13_poly__all__0__iff__0, fact_323_order_Ostrict__implies__not__eq, fact_270_gt__ex, fact_283_less__asym_H, fact_174_less__irrefl__nat, fact_203_dual__order_Oeq__iff, fact_2__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062lb1_O_A_092_060forall_062x_O_Apoly_Ap_Ax_A_061_A0_A_092_060longrightarrow_062_Alb1_A_060_Ax_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062, fact_10_poly__IVT__neg, fact_45_min_Ostrict__boundedE, fact_268_lt__ex, fact_72_order__root, fact_214_ord__le__eq__trans, fact_296_less__imp__not__eq, fact_9_not__gr__zero, fact_1_lb__def, fact_191_order__refl, fact_221_antisym__conv, fact_98_min_OorderE, fact_3_assms, fact_19_field__lbound__gt__zero, fact_234_eq__iff, fact_224_order_Otrans, fact_116_min_Oabsorb__iff1, fact_229_eq__refl, fact_165_less__mono__imp__le__mono, fact_288_less__irrefl, fact_225_order_Otrans, fact_31_min__less__iff__conj, fact_186_less__eq__nat_Osimps_I1_J, fact_300_less__induct, fact_259_ord__less__eq__subst, fact_168_le__eq__less__or__eq, fact_188_ex__least__nat__le, fact_29_poly__eq__poly__eq__iff, fact_304_less__imp__not__eq2, fact_313_less__imp__not__less, fact_281_less__asym, fact_172_infinite__descent, fact_205_dual__order_Otrans, fact_278_less__imp__neq, fact_15_less__numeral__extra_I3_J, fact_200_dual__order_Oantisym, fact_243_ord__eq__le__subst, fact_280_less__asym, fact_202_dual__order_Oeq__iff, fact_47_min__less__iff__disj, fact_286_less__linear, fact_159_le__refl, fact_69_poly__shift__0, fact_331_le__less, fact_134_sgn__greater, fact_106_min_OboundedE, fact_264_order__less__subst2, fact_63_reflect__poly__at__0__eq__0__iff, fact_124_min__le__iff__disj, fact_265_order__less__subst2, fact_322_order_Ostrict__implies__not__eq, fact_303_less__imp__not__eq2, fact_95_less__eq__real__def, fact_23_zero__less__iff__neq__zero, fact_321_not__less__iff__gr__or__eq, fact_213_order__class_Oorder_Oantisym, fact_201_dual__order_Oantisym, fact_62_next__non__root__interval, fact_17_less__numeral__extra_I3_J, fact_30_poly__eq__poly__eq__iff, fact_169_less__imp__le__nat, fact_58_poly__cutoff__0, fact_114_min_Ocobounded2, fact_251_order__subst1, fact_173_nat__less__induct, fact_137_sgn__less, fact_219_order__class_Oorder_Oeq__iff, fact_110_min_Oorder__iff, fact_104_min_Oabsorb2, fact_227_le__cases, fact_206_linorder__wlog, fact_241_ord__eq__le__subst, fact_290_ord__eq__less__trans, fact_277_dense, fact_269_gt__ex, fact_329_leI, fact_231_linear, fact_145_sgn__eq__0__iff, fact_73_order__root, fact_146_sgn__eq__0__iff, fact_275_order_Oasym, fact_218_order__class_Oorder_Oeq__iff, fact_256_ord__less__eq__subst, fact_209_dual__order_Orefl, fact_24_zero__reorient, fact_252_ord__eq__less__subst, fact_343_order__less__le__subst1, fact_328_leI, fact_261_order__less__subst1, fact_262_order__less__subst1, fact_217_ord__eq__le__trans, fact_338_order__le__less__subst2, fact_80_le__zero__eq, fact_192_order__refl, fact_237_ord__le__eq__subst, fact_176_less__not__refl2, fact_49_is__zero__null, fact_318_dual__order_Ostrict__trans, fact_215_ord__le__eq__trans, fact_235_eq__iff, fact_43_min_Ostrict__order__iff, fact_56_min_Oassoc, fact_327_leD, fact_167_less__or__eq__imp__le, fact_333_less__le, fact_162_le__antisym, fact_335_order__le__less__subst1, fact_289_less__irrefl, fact_228_eq__refl, fact_175_less__not__refl3, fact_236_ord__le__eq__subst, fact_233_antisym, fact_319_dual__order_Ostrict__trans, fact_245_order__subst2, fact_185_gr0I, fact_246_order__subst2, fact_195_min__absorb2, fact_120_min_OcoboundedI1, fact_139_sgn__0, fact_127_order__0I, fact_28_zero__reorient, fact_301_antisym__conv3, fact_179_bot__nat__0_Oextremum__strict, fact_240_ord__eq__le__subst, fact_337_order__le__less__subst1, fact_184_not__gr0, fact_276_order_Oasym, fact_142_sgn__zero, fact_267_order__less__subst2, fact_344_order__less__le__subst1, fact_190_bot__nat__0_Oextremum__uniqueI, fact_324_dual__order_Ostrict__implies__not__eq, fact_131_sgn__le__0__iff, fact_25_zero__reorient, fact_163_nat__le__linear, fact_291_ord__eq__less__trans, fact_154_neq0__conv, fact_292_ord__less__eq__trans, fact_247_order__subst2, fact_79__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062lb2_O_A_092_060forall_062x_092_060le_062lb2_O_Asgn_A_Ipoly_Ap_Ax_J_A_061_Asgn__neg__inf_Ap_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062, fact_0_lb1, fact_156_bot__nat__0_Onot__eq__extremum, fact_68_lb2, fact_33_min_Oidem, fact_315_exists__least__iff, fact_309_dual__order_Oirrefl, fact_255_ord__eq__less__subst, fact_171_linorder__neqE__nat, fact_216_ord__eq__le__trans, fact_238_ord__le__eq__subst, fact_308_linorder__cases, fact_295_dual__order_Oasym, fact_317_linorder__less__wlog, fact_193_min__absorb1, fact_210_order__trans, fact_100_min_OorderI, fact_39_min_Ostrict__coboundedI2, fact_342_order__less__le__subst1, fact_75_divide__poly__main__0, fact_88_that, fact_285_less__trans, fact_310_dual__order_Oirrefl, fact_11_poly__IVT__pos, fact_293_ord__less__eq__trans, fact_170_nat__less__le, fact_279_less__imp__neq, fact_102_min_Oabsorb1, fact_204_dual__order_Otrans, fact_263_order__less__subst1, fact_112_min_Ocobounded1, fact_126_order__0I, fact_287_less__linear, fact_180_infinite__descent0, fact_41_min_Ostrict__coboundedI1, fact_81_min_Obounded__iff, fact_197_min__def, fact_118_min_Oabsorb__iff2, fact_341_order__le__less__subst2, fact_260_order__less__subst1, fact_242_ord__eq__le__subst, fact_220_antisym__conv, fact_178_nat__neq__iff, fact_153_bot__nat__0_Oextremum, fact_207_linorder__wlog, fact_254_ord__eq__less__subst, fact_130_zero__le__sgn__iff, fact_274_neq__iff, fact_18_less__numeral__extra_I3_J, fact_138_root__ub, fact_89_complete__real, fact_284_less__trans, fact_108_min_OboundedI, fact_20_gr__zeroI, fact_257_ord__less__eq__subst, fact_189_bot__nat__0_Oextremum__unique, fact_135_sgn__less, fact_305_less__imp__triv, fact_208_dual__order_Orefl, fact_273_neq__iff, fact_271_neqE, fact_161_eq__imp__le, fact_336_order__le__less__subst1, fact_14_poly__all__0__iff__0, fact_249_order__subst1, fact_140_sgn__0, fact_307_linorder__cases, fact_332_less__le, fact_91_le__numeral__extra_I3_J, fact_21_not__less__zero, fact_272_neqE, fact_90_zero__le, fact_166_le__neq__implies__less, fact_143_sgn__sgn, fact_144_linorder__neqE__linordered__idom, fact_339_order__le__less__subst2, fact_334_order__le__less__subst1, fact_340_order__le__less__subst2, fact_212_order__class_Oorder_Oantisym, fact_316_linorder__less__wlog, fact_306_less__imp__triv, fact_232_antisym, fact_211_order__trans, fact_22_gr__implies__not__zero, fact_298_less__not__sym, fact_148_sgn__0__0, fact_151_sgn__zero__iff, fact_326_leD, fact_177_less__not__refl, fact_230_linear, fact_302_antisym__conv3, fact_325_dual__order_Ostrict__implies__not__eq, fact_239_ord__le__eq__subst, fact_132_sgn__greater, fact_266_order__less__subst2, fact_297_less__imp__not__eq, fact_314_less__imp__not__less, fact_330_le__less, fact_253_ord__eq__less__subst, fact_83_reflect__poly__0, fact_222_le__cases3, fact_182_less__zeroE, fact_26_zero__reorient, fact_8_poly__0, fact_54_min_Ocommute, fact_299_less__not__sym, fact_37_min_Oright__idem, fact_294_dual__order_Oasym, fact_250_order__subst1, fact_155_less__nat__zero__code, fact_187_le__0__eq, fact_78_not__eq__pos__or__neg__iff__1, fact_312_order_Ostrict__trans, fact_122_min_OcoboundedI2, fact_164_Nat_Oex__has__greatest__nat, fact_93_le__numeral__extra_I3_J, fact_61_last__non__root__interval, fact_152_le0, fact_248_order__subst1, fact_149_sgn__0__0, fact_282_less__asym_H, fact_6_poly__0
% 17.99/5.15 % No. of inferences in proof: 568
% 17.99/5.15 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 4779 ms resp. 3925 ms w/o parsing
% 18.74/5.36 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.74/5.36 thf(poly_poly_poly_real_type, type, poly_poly_poly_real: $tType).
% 18.74/5.36 thf(poly_poly_real_type, type, poly_poly_real: $tType).
% 18.74/5.36 thf(poly_poly_nat_type, type, poly_poly_nat: $tType).
% 18.74/5.36 thf(poly_real_type, type, poly_real: $tType).
% 18.74/5.36 thf(poly_nat_type, type, poly_nat: $tType).
% 18.74/5.36 thf(set_real_type, type, set_real: $tType).
% 18.74/5.36 thf(real_type, type, real: $tType).
% 18.74/5.36 thf(nat_type, type, nat: $tType).
% 18.74/5.36 thf(sgn_sgn_poly_real_decl, type, sgn_sgn_poly_real: (poly_real > poly_real)).
% 18.74/5.36 thf(sgn_sgn_real_decl, type, sgn_sgn_real: (real > real)).
% 18.74/5.36 thf(zero_zero_nat_decl, type, zero_zero_nat: nat).
% 18.74/5.36 thf(zero_z1423781445y_real_decl, type, zero_z1423781445y_real: poly_poly_real).
% 18.74/5.36 thf(zero_zero_poly_real_decl, type, zero_zero_poly_real: poly_real).
% 18.74/5.36 thf(zero_zero_real_decl, type, zero_zero_real: real).
% 18.74/5.36 thf(if_real_decl, type, if_real: ($o > (real > (real > real)))).
% 18.74/5.36 thf(ord_less_nat_decl, type, ord_less_nat: (nat > (nat > $o))).
% 18.74/5.36 thf(ord_less_poly_real_decl, type, ord_less_poly_real: (poly_real > (poly_real > $o))).
% 18.74/5.36 thf(ord_less_real_decl, type, ord_less_real: (real > (real > $o))).
% 18.74/5.36 thf(ord_less_eq_nat_decl, type, ord_less_eq_nat: (nat > (nat > $o))).
% 18.74/5.36 thf(ord_le1180086932y_real_decl, type, ord_le1180086932y_real: (poly_real > (poly_real > $o))).
% 18.74/5.36 thf(ord_less_eq_real_decl, type, ord_less_eq_real: (real > (real > $o))).
% 18.74/5.36 thf(ord_min_real_decl, type, ord_min_real: (real > (real > real))).
% 18.74/5.36 thf(divide1561404011n_real_decl, type, divide1561404011n_real: (real > (poly_real > (poly_real > (poly_real > (nat > (nat > poly_real))))))).
% 18.74/5.36 thf(is_zero_real_decl, type, is_zero_real: (poly_real > $o)).
% 18.74/5.36 thf(order_poly_real_decl, type, order_poly_real: (poly_real > (poly_poly_real > nat))).
% 18.74/5.36 thf(order_real_decl, type, order_real: (real > (poly_real > nat))).
% 18.74/5.36 thf(poly_poly_real2_decl, type, poly_poly_real2: (poly_poly_real > (poly_real > poly_real))).
% 18.74/5.36 thf(poly_real2_decl, type, poly_real2: (poly_real > (real > real))).
% 18.74/5.36 thf(poly_cutoff_real_decl, type, poly_cutoff_real: (nat > (poly_real > poly_real))).
% 18.74/5.36 thf(poly_shift_real_decl, type, poly_shift_real: (nat > (poly_real > poly_real))).
% 18.74/5.36 thf(reflect_poly_real_decl, type, reflect_poly_real: (poly_real > poly_real)).
% 18.74/5.36 thf(sturm_1076696862f_real_decl, type, sturm_1076696862f_real: (poly_real > real)).
% 18.74/5.36 thf(sturm_1308388506f_real_decl, type, sturm_1308388506f_real: (poly_real > real)).
% 18.74/5.36 thf(member_real_decl, type, member_real: (real > (set_real > $o))).
% 18.74/5.36 thf(lb1_decl, type, lb1: real).
% 18.74/5.36 thf(lb2_decl, type, lb2: real).
% 18.74/5.36 thf(lb_decl, type, lb: real).
% 18.74/5.36 thf(p_decl, type, p: poly_real).
% 18.74/5.36 thf(thesis_decl, type, thesis: $o).
% 18.74/5.36 thf(203,axiom,((! [A:real,B:(real > real),C:real,D:real]: ((ord_less_real @ A @ (B @ C)) => ((ord_less_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_real @ (B @ E) @ (B @ F)))) => (ord_less_real @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_260_order__less__subst1)).
% 18.74/5.36 thf(1105,plain,((! [A:real,B:(real > real),C:real,D:real]: ((ord_less_real @ A @ (B @ C)) => ((ord_less_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_real @ (B @ E) @ (B @ F)))) => (ord_less_real @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 18.74/5.36 thf(237,axiom,((! [A:real]: ((ord_less_real @ zero_zero_real @ (sgn_sgn_real @ A)) = (ord_less_real @ zero_zero_real @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_sgn__greater)).
% 18.74/5.36 thf(1237,plain,((! [A:real]: ((ord_less_real @ zero_zero_real @ (sgn_sgn_real @ A)) = (ord_less_real @ zero_zero_real @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 18.74/5.36 thf(151,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_233_antisym)).
% 18.74/5.36 thf(893,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)],[151])).
% 18.74/5.36 thf(53,axiom,((((?) @ nat) = (^ [A:(nat > $o)]: ? [B:nat]: ((A @ B) & ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_315_exists__least__iff)).
% 18.74/5.36 thf(468,plain,((((?) @ nat) = (^ [A:(nat > $o)]: ? [B:nat]: ((A @ B) & ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 18.74/5.36 thf(204,axiom,((ord_less_eq_real = (^ [A:real,B:real]: ((ord_less_real @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_330_le__less)).
% 18.74/5.36 thf(1110,plain,(((ord_less_eq_real) = (^ [A:real,B:real]: ((ord_less_real @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 18.74/5.36 thf(156,axiom,((ord_less_nat = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (A != B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_170_nat__less__le)).
% 18.74/5.36 thf(909,plain,(((ord_less_nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & ~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 18.74/5.36 thf(100,axiom,((! [A:real,B:real]: ((A = B) => (ord_less_eq_real @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_eq__refl)).
% 18.74/5.36 thf(628,plain,((! [A:real,B:real]: ((A = B) => (ord_less_eq_real @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 18.74/5.36 thf(189,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_173_nat__less__induct)).
% 18.74/5.36 thf(1031,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)],[189])).
% 18.74/5.36 thf(38,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_299_less__not__sym)).
% 18.74/5.36 thf(408,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 18.74/5.36 thf(232,axiom,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (~ (ord_less_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_313_less__imp__not__less)).
% 18.74/5.36 thf(1211,plain,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (~ (ord_less_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 18.74/5.36 thf(89,axiom,((! [A:poly_real]: (((sgn_sgn_poly_real @ A) = zero_zero_poly_real) = (A = zero_zero_poly_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_146_sgn__eq__0__iff)).
% 18.74/5.36 thf(582,plain,((! [A:poly_real]: (((sgn_sgn_poly_real @ A) = zero_zero_poly_real) = (A = zero_zero_poly_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 18.74/5.36 thf(251,axiom,((! [A:real,B:real]: ((~ (ord_less_real @ A @ B)) => ((A != B) => (ord_less_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_307_linorder__cases)).
% 18.74/5.36 thf(1290,plain,((! [A:real,B:real]: ((~ (ord_less_real @ A @ B)) => ((~ (A = B)) => (ord_less_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[251])).
% 18.74/5.36 thf(9,axiom,((! [A:poly_real]: ((ord_less_poly_real @ (sgn_sgn_poly_real @ A) @ zero_zero_poly_real) = (ord_less_poly_real @ A @ zero_zero_poly_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_135_sgn__less)).
% 18.74/5.36 thf(308,plain,((! [A:poly_real]: ((ord_less_poly_real @ (sgn_sgn_poly_real @ A) @ zero_zero_poly_real) = (ord_less_poly_real @ A @ zero_zero_poly_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 18.74/5.36 thf(223,axiom,((lb = (ord_min_real @ lb1 @ lb2))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_lb__def)).
% 18.74/5.36 thf(1173,plain,((lb = (ord_min_real @ lb1 @ lb2))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 18.74/5.36 thf(73,axiom,((! [A:nat]: ((poly_cutoff_real @ A @ zero_zero_poly_real) = zero_zero_poly_real))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_poly__cutoff__0)).
% 18.74/5.36 thf(533,plain,((! [A:nat]: ((poly_cutoff_real @ A @ zero_zero_poly_real) = zero_zero_poly_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 18.74/5.36 thf(158,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_160_le__trans)).
% 18.74/5.36 thf(913,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)],[158])).
% 18.74/5.36 thf(269,axiom,((! [A:real,B:real,C:poly_real]: ((! [D:real]: (((ord_less_real @ A @ D) & (ord_less_eq_real @ D @ B)) => ((poly_real2 @ C @ D) != zero_zero_real))) = (! [D:real]: (((ord_less_real @ A @ D) & (ord_less_eq_real @ D @ B)) => (ord_less_real @ zero_zero_real @ (poly_real2 @ C @ D))) | ! [D:real]: (((ord_less_real @ A @ D) & (ord_less_eq_real @ D @ B)) => (ord_less_real @ (poly_real2 @ C @ D) @ zero_zero_real)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_not__eq__pos__or__neg__iff__1)).
% 18.74/5.36 thf(1354,plain,((! [A:real,B:real,C:poly_real]: ((! [D:real]: (((ord_less_real @ A @ D) & (ord_less_eq_real @ D @ B)) => (~ ((poly_real2 @ C @ D) = zero_zero_real)))) = (! [D:real]: (((ord_less_real @ A @ D) & (ord_less_eq_real @ D @ B)) => (ord_less_real @ zero_zero_real @ (poly_real2 @ C @ D))) | ! [D:real]: (((ord_less_real @ A @ D) & (ord_less_eq_real @ D @ B)) => (ord_less_real @ (poly_real2 @ C @ D) @ zero_zero_real)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[269])).
% 18.74/5.36 thf(140,axiom,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_eq_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_239_ord__le__eq__subst)).
% 18.74/5.36 thf(829,plain,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_eq_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 18.74/5.36 thf(210,axiom,((! [A:real]: ((poly_real2 @ zero_zero_poly_real @ A) = zero_zero_real))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_poly__0)).
% 18.74/5.36 thf(1127,plain,((! [A:real]: ((poly_real2 @ zero_zero_poly_real @ A) = zero_zero_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 18.74/5.36 thf(45,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_225_order_Otrans)).
% 18.74/5.36 thf(436,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)],[45])).
% 18.74/5.36 thf(244,axiom,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (~ (ord_less_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_298_less__not__sym)).
% 18.74/5.36 thf(1265,plain,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (~ (ord_less_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[244])).
% 18.74/5.36 thf(236,axiom,((! [A:nat,B:(real > nat),C:real,D:real]: ((A = (B @ C)) => ((ord_less_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_253_ord__eq__less__subst)).
% 18.74/5.36 thf(1228,plain,((! [A:nat,B:(real > nat),C:real,D:real]: ((A = (B @ C)) => ((ord_less_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[236])).
% 18.74/5.36 thf(241,axiom,((! [A:real]: ((zero_zero_real = A) = (A = zero_zero_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_zero__reorient)).
% 18.74/5.36 thf(1254,plain,((! [A:real]: ((zero_zero_real = A) = (A = zero_zero_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 18.74/5.36 thf(117,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((A != B) => (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_308_linorder__cases)).
% 18.74/5.36 thf(719,plain,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((~ (A = B)) => (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 18.74/5.36 thf(63,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) = (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_221_antisym__conv)).
% 18.74/5.36 thf(504,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) = (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 18.74/5.36 thf(141,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_295_dual__order_Oasym)).
% 18.74/5.36 thf(838,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 18.74/5.36 thf(21,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_163_nat__le__linear)).
% 18.74/5.36 thf(344,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)],[21])).
% 18.74/5.36 thf(26,axiom,((! [A:real,B:real,C:real]: ((ord_min_real @ A @ (ord_min_real @ B @ C)) = (ord_min_real @ B @ (ord_min_real @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_min_Oleft__commute)).
% 18.74/5.36 thf(357,plain,((! [A:real,B:real,C:real]: ((ord_min_real @ A @ (ord_min_real @ B @ C)) = (ord_min_real @ B @ (ord_min_real @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 18.74/5.36 thf(77,axiom,((! [A:real,B:real,C:real,D:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ C @ D) => (ord_less_eq_real @ (ord_min_real @ A @ C) @ (ord_min_real @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_min_Omono)).
% 18.74/5.36 thf(542,plain,((! [A:real,B:real,C:real,D:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ C @ D) => (ord_less_eq_real @ (ord_min_real @ A @ C) @ (ord_min_real @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 18.74/5.36 thf(195,axiom,((! [A:real]: ~ (ord_less_real @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_309_dual__order_Oirrefl)).
% 18.74/5.36 thf(1055,plain,((! [A:real]: ~ (ord_less_real @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 18.74/5.36 thf(119,axiom,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => (ord_less_eq_real @ (ord_min_real @ C @ A) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_122_min_OcoboundedI2)).
% 18.74/5.36 thf(724,plain,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => (ord_less_eq_real @ (ord_min_real @ C @ A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 18.74/5.36 thf(258,axiom,((! [A:real,B:(nat > real),C:nat,D:nat]: ((ord_less_eq_real @ A @ (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_real @ (B @ E) @ (B @ F)))) => (ord_less_real @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_335_order__le__less__subst1)).
% 18.74/5.36 thf(1313,plain,((! [A:real,B:(nat > real),C:nat,D:nat]: ((ord_less_eq_real @ A @ (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_real @ (B @ E) @ (B @ F)))) => (ord_less_real @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[258])).
% 18.74/5.36 thf(247,axiom,((! [A:real,B:real]: ((ord_less_real @ A @ B) | (A = B) | (ord_less_real @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_286_less__linear)).
% 18.74/5.36 thf(1279,plain,((! [A:real,B:real]: ((ord_less_real @ A @ B) | (A = B) | (ord_less_real @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[247])).
% 18.74/5.36 thf(138,axiom,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ C @ A) => (ord_less_eq_real @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_204_dual__order_Otrans)).
% 18.74/5.36 thf(817,plain,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ C @ A) => (ord_less_eq_real @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 18.74/5.36 thf(275,axiom,((! [A:real,B:(nat > real),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_real @ (B @ E) @ (B @ F)))) => (ord_less_real @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_254_ord__eq__less__subst)).
% 18.74/5.36 thf(1379,plain,((! [A:real,B:(nat > real),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_real @ (B @ E) @ (B @ F)))) => (ord_less_real @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[275])).
% 18.74/5.36 thf(239,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => (~ (ord_less_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_326_leD)).
% 18.74/5.36 thf(1247,plain,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => (~ (ord_less_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 18.74/5.36 thf(267,axiom,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (~ (ord_less_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_294_dual__order_Oasym)).
% 18.74/5.36 thf(1347,plain,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (~ (ord_less_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[267])).
% 18.74/5.36 thf(128,axiom,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less_nat @ D @ E) => (A @ D @ E))) => ((! [D:nat]: (A @ D @ D)) => ((! [D:nat,E:nat]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_317_linorder__less__wlog)).
% 18.74/5.36 thf(770,plain,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less_nat @ D @ E) => (A @ D @ E))) => ((! [D:nat]: (A @ D @ D)) => ((! [D:nat,E:nat]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 18.74/5.36 thf(271,axiom,((! [A:real]: ((! [B:real]: (((poly_real2 @ p @ B) = zero_zero_real) => (ord_less_real @ A @ B))) => ((! [B:real]: ((ord_less_eq_real @ B @ A) => ((sgn_sgn_real @ (poly_real2 @ p @ B)) = (sturm_1076696862f_real @ p)))) => (thesis))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_that)).
% 18.74/5.36 thf(1362,plain,((! [A:real]: ((! [B:real]: (((poly_real2 @ p @ B) = zero_zero_real) => (ord_less_real @ A @ B))) => ((! [B:real]: ((ord_less_eq_real @ B @ A) => ((sgn_sgn_real @ (poly_real2 @ p @ B)) = (sturm_1076696862f_real @ p)))) => (thesis))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[271])).
% 18.74/5.36 thf(56,axiom,((! [A:poly_real]: (((sgn_sgn_poly_real @ A) = zero_zero_poly_real) = (A = zero_zero_poly_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_149_sgn__0__0)).
% 18.74/5.36 thf(475,plain,((! [A:poly_real]: (((sgn_sgn_poly_real @ A) = zero_zero_poly_real) = (A = zero_zero_poly_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 18.74/5.36 thf(129,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_279_less__imp__neq)).
% 18.74/5.36 thf(789,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 18.74/5.36 thf(32,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_188_ex__least__nat__le)).
% 18.74/5.36 thf(376,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)],[32])).
% 18.74/5.36 thf(59,axiom,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_259_ord__less__eq__subst)).
% 18.74/5.36 thf(485,plain,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 18.74/5.36 thf(23,axiom,((! [A:nat]: ((zero_zero_nat = A) = (A = zero_zero_nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_zero__reorient)).
% 18.74/5.36 thf(348,plain,((! [A:nat]: ((zero_zero_nat = A) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 18.74/5.36 thf(226,axiom,((! [A:poly_real,B:real]: (((poly_real2 @ A @ B) = zero_zero_real) = ((A = zero_zero_poly_real) | ((order_real @ B @ A) != zero_zero_nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_order__root)).
% 18.74/5.36 thf(1183,plain,((! [A:poly_real,B:real]: (((poly_real2 @ A @ B) = zero_zero_real) = ((A = zero_zero_poly_real) | ~ ((order_real @ B @ A) = zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 18.74/5.36 thf(154,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_281_less__asym)).
% 18.74/5.36 thf(905,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 18.74/5.36 thf(190,axiom,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) => (A = zero_zero_nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_bot__nat__0_Oextremum__uniqueI)).
% 18.74/5.36 thf(1040,plain,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) => (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 18.74/5.36 thf(13,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_178_nat__neq__iff)).
% 18.74/5.36 thf(321,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)],[13])).
% 18.74/5.36 thf(102,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_min_real @ B @ A) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_195_min__absorb2)).
% 18.74/5.36 thf(634,plain,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_min_real @ B @ A) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 18.74/5.36 thf(4,axiom,((! [A:poly_poly_real]: ((zero_z1423781445y_real = A) = (A = zero_z1423781445y_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_zero__reorient)).
% 18.74/5.36 thf(293,plain,((! [A:poly_poly_real]: ((zero_z1423781445y_real = A) = (A = zero_z1423781445y_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 18.74/5.36 thf(50,axiom,((! [A:poly_real]: ((zero_zero_poly_real = A) = (A = zero_zero_poly_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_zero__reorient)).
% 18.74/5.36 thf(453,plain,((! [A:poly_real]: ((zero_zero_poly_real = A) = (A = zero_zero_poly_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 18.74/5.36 thf(208,axiom,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ B) => (ord_less_real @ (ord_min_real @ C @ A) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_min_Ostrict__coboundedI2)).
% 18.74/5.36 thf(1119,plain,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ B) => (ord_less_real @ (ord_min_real @ C @ A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 18.74/5.36 thf(107,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_162_le__antisym)).
% 18.74/5.36 thf(660,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)],[107])).
% 18.74/5.36 thf(64,axiom,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_247_order__subst2)).
% 18.74/5.36 thf(507,plain,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 18.74/5.36 thf(70,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) | (ord_less_eq_real @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_linear)).
% 18.74/5.36 thf(527,plain,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) | (ord_less_eq_real @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 18.74/5.36 thf(112,axiom,((! [A:nat]: ((A != zero_zero_nat) = (ord_less_nat @ zero_zero_nat @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_156_bot__nat__0_Onot__eq__extremum)).
% 18.74/5.36 thf(678,plain,((! [A:nat]: ((~ (A = zero_zero_nat)) = (ord_less_nat @ zero_zero_nat @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 18.74/5.36 thf(71,axiom,((ord_min_real = (^ [A:real,B:real]: (if_real @ (ord_less_eq_real @ A @ B) @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_197_min__def)).
% 18.74/5.36 thf(529,plain,(((ord_min_real) = (^ [A:real,B:real]: (if_real @ (ord_less_eq_real @ A @ B) @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 18.74/5.36 thf(130,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_213_order__class_Oorder_Oantisym)).
% 18.74/5.36 thf(793,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)],[130])).
% 18.74/5.36 thf(230,axiom,((! [A:nat,B:nat,C:(nat > real),D:real]: ((ord_less_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_real @ (C @ E) @ (C @ F)))) => (ord_less_real @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_258_ord__less__eq__subst)).
% 18.74/5.36 thf(1199,plain,((! [A:nat,B:nat,C:(nat > real),D:real]: ((ord_less_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_real @ (C @ E) @ (C @ F)))) => (ord_less_real @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 18.74/5.36 thf(29,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ A) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_212_order__class_Oorder_Oantisym)).
% 18.74/5.36 thf(366,plain,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 18.74/5.36 thf(197,axiom,((! [A:poly_real,B:real]: (((poly_real2 @ A @ B) != zero_zero_real) => ((order_real @ B @ A) = zero_zero_nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_126_order__0I)).
% 18.74/5.36 thf(1067,plain,((! [A:poly_real,B:real]: ((~ ((poly_real2 @ A @ B) = zero_zero_real)) => ((order_real @ B @ A) = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 18.74/5.36 thf(65,axiom,((! [A:real,B:real,C:real]: ((A = B) => ((ord_less_eq_real @ B @ C) => (ord_less_eq_real @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_216_ord__eq__le__trans)).
% 18.74/5.36 thf(512,plain,((! [A:real,B:real,C:real]: ((A = B) => ((ord_less_eq_real @ B @ C) => (ord_less_eq_real @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 18.74/5.36 thf(166,axiom,((ord_less_eq_nat = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_331_le__less)).
% 18.74/5.36 thf(942,plain,(((ord_less_eq_nat) = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 18.74/5.36 thf(46,axiom,((! [A:nat,B:nat,C:nat]: ((A = B) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_217_ord__eq__le__trans)).
% 18.74/5.36 thf(439,plain,((! [A:nat,B:nat,C:nat]: ((A = B) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 18.74/5.36 thf(192,axiom,((! [A:poly_real,B:poly_real,C:nat,D:nat]: ((divide1561404011n_real @ zero_zero_real @ zero_zero_poly_real @ A @ B @ C @ D) = zero_zero_poly_real))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_divide__poly__main__0)).
% 18.74/5.36 thf(1047,plain,((! [A:poly_real,B:poly_real,C:nat,D:nat]: ((divide1561404011n_real @ zero_zero_real @ zero_zero_poly_real @ A @ B @ C @ D) = zero_zero_poly_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 18.74/5.36 thf(132,axiom,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((B = C) => (ord_less_eq_real @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_214_ord__le__eq__trans)).
% 18.74/5.36 thf(798,plain,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((B = C) => (ord_less_eq_real @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 18.74/5.36 thf(219,axiom,((ord_less_real = (^ [A:real,B:real]: ((A = (ord_min_real @ A @ B)) & (A != B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_43_min_Ostrict__order__iff)).
% 18.74/5.36 thf(1163,plain,(((ord_less_real) = (^ [A:real,B:real]: ((A = (ord_min_real @ A @ B)) & ~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 18.74/5.36 thf(17,axiom,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_less__eq__nat_Osimps_I1_J)).
% 18.74/5.36 thf(334,plain,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 18.74/5.36 thf(7,axiom,((! [A:poly_real]: ((ord_less_poly_real @ zero_zero_poly_real @ (sgn_sgn_poly_real @ A)) = (ord_less_poly_real @ zero_zero_poly_real @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_132_sgn__greater)).
% 18.74/5.36 thf(302,plain,((! [A:poly_real]: ((ord_less_poly_real @ zero_zero_poly_real @ (sgn_sgn_poly_real @ A)) = (ord_less_poly_real @ zero_zero_poly_real @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 18.74/5.36 thf(144,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_274_neq__iff)).
% 18.74/5.36 thf(862,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)],[144])).
% 18.74/5.36 thf(139,axiom,((! [A:nat,B:(real > nat),C:real,D:real]: ((A = (B @ C)) => ((ord_less_eq_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_241_ord__eq__le__subst)).
% 18.74/5.36 thf(820,plain,((! [A:nat,B:(real > nat),C:real,D:real]: ((A = (B @ C)) => ((ord_less_eq_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 18.74/5.36 thf(81,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_166_le__neq__implies__less)).
% 18.74/5.36 thf(561,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)],[81])).
% 18.74/5.36 thf(121,axiom,((! [A:real,B:real]: ((A = (ord_min_real @ A @ B)) => (ord_less_eq_real @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_min_OorderI)).
% 18.74/5.36 thf(729,plain,((! [A:real,B:real]: ((A = (ord_min_real @ A @ B)) => (ord_less_eq_real @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 18.74/5.36 thf(159,axiom,((! [A:real,B:real,C:(real > nat),D:nat]: ((ord_less_eq_real @ A @ B) => ((ord_less_nat @ (C @ B) @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_339_order__le__less__subst2)).
% 18.74/5.36 thf(916,plain,((! [A:real,B:real,C:(real > nat),D:nat]: ((ord_less_eq_real @ A @ B) => ((ord_less_nat @ (C @ B) @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 18.74/5.36 thf(99,axiom,((! [A:real]: ((sgn_sgn_real @ (sgn_sgn_real @ A)) = (sgn_sgn_real @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_143_sgn__sgn)).
% 18.74/5.36 thf(625,plain,((! [A:real]: ((sgn_sgn_real @ (sgn_sgn_real @ A)) = (sgn_sgn_real @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 18.74/5.36 thf(68,axiom,((! [A:nat]: ((poly_shift_real @ A @ zero_zero_poly_real) = zero_zero_poly_real))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_poly__shift__0)).
% 18.74/5.36 thf(522,plain,((! [A:nat]: ((poly_shift_real @ A @ zero_zero_poly_real) = zero_zero_poly_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 18.74/5.36 thf(217,axiom,(((sgn_sgn_real @ zero_zero_real) = zero_zero_real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_sgn__0)).
% 18.74/5.36 thf(1159,plain,(((sgn_sgn_real @ zero_zero_real) = zero_zero_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[217])).
% 18.74/5.36 thf(51,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_300_less__induct)).
% 18.74/5.36 thf(456,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)],[51])).
% 18.74/5.36 thf(14,axiom,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_nat @ A @ (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_344_order__less__le__subst1)).
% 18.74/5.36 thf(324,plain,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_nat @ A @ (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 18.74/5.36 thf(184,axiom,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ C) => (ord_less_eq_real @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_210_order__trans)).
% 18.74/5.36 thf(1012,plain,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ C) => (ord_less_eq_real @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 18.74/5.36 thf(1,conjecture,((! [A:real]: (((poly_real2 @ p @ A) != zero_zero_real) | (ord_less_real @ lb @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 18.74/5.36 thf(2,negated_conjecture,((~ (! [A:real]: (((poly_real2 @ p @ A) != zero_zero_real) | (ord_less_real @ lb @ A))))),inference(neg_conjecture,[status(cth)],[1])).
% 18.74/5.36 thf(285,plain,((~ (! [A:real]: (~ ((poly_real2 @ p @ A) = zero_zero_real) | (ord_less_real @ lb @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 18.74/5.36 thf(15,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) => (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_201_dual__order_Oantisym)).
% 18.74/5.36 thf(329,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) => (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 18.74/5.36 thf(225,axiom,((! [A:real,B:real,C:real]: ((A = B) => ((ord_less_real @ B @ C) => (ord_less_real @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_290_ord__eq__less__trans)).
% 18.74/5.36 thf(1178,plain,((! [A:real,B:real,C:real]: ((A = B) => ((ord_less_real @ B @ C) => (ord_less_real @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[225])).
% 18.74/5.36 thf(253,axiom,((! [A:real,B:real,C:(real > real),D:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_real @ (C @ B) @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_real @ (C @ E) @ (C @ F)))) => (ord_less_real @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_338_order__le__less__subst2)).
% 18.74/5.36 thf(1296,plain,((! [A:real,B:real,C:(real > real),D:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_real @ (C @ B) @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_real @ (C @ E) @ (C @ F)))) => (ord_less_real @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[253])).
% 18.74/5.36 thf(109,axiom,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_153_bot__nat__0_Oextremum)).
% 18.74/5.36 thf(665,plain,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 18.74/5.36 thf(199,axiom,((! [A:real,B:(nat > real),C:nat,D:nat]: ((ord_less_real @ A @ (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_real @ (B @ E) @ (B @ F)))) => (ord_less_real @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_343_order__less__le__subst1)).
% 18.74/5.36 thf(1089,plain,((! [A:real,B:(nat > real),C:nat,D:nat]: ((ord_less_real @ A @ (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_real @ (B @ E) @ (B @ F)))) => (ord_less_real @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 18.74/5.36 thf(246,axiom,((! [A:real,B:real,C:(real > real),D:real]: ((ord_less_real @ A @ B) => (((C @ B) = D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_real @ (C @ E) @ (C @ F)))) => (ord_less_real @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_256_ord__less__eq__subst)).
% 18.74/5.36 thf(1270,plain,((! [A:real,B:real,C:(real > real),D:real]: ((ord_less_real @ A @ B) => (((C @ B) = D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_real @ (C @ E) @ (C @ F)))) => (ord_less_real @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[246])).
% 18.74/5.36 thf(186,axiom,((! [A:real,B:(real > real),C:real,D:real]: ((A = (B @ C)) => ((ord_less_eq_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_real @ (B @ E) @ (B @ F)))) => (ord_less_eq_real @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_240_ord__eq__le__subst)).
% 18.74/5.36 thf(1017,plain,((! [A:real,B:(real > real),C:real,D:real]: ((A = (B @ C)) => ((ord_less_eq_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_real @ (B @ E) @ (B @ F)))) => (ord_less_eq_real @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 18.74/5.36 thf(261,axiom,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (? [C:real]: ((ord_less_real @ A @ C) & (ord_less_real @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_277_dense)).
% 18.74/5.36 thf(1328,plain,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (? [C:real]: ((ord_less_real @ A @ C) & (ord_less_real @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[261])).
% 18.74/5.36 thf(61,axiom,((! [A:nat]: ((A != zero_zero_nat) = (ord_less_nat @ zero_zero_nat @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_154_neq0__conv)).
% 18.74/5.36 thf(499,plain,((! [A:nat]: ((~ (A = zero_zero_nat)) = (ord_less_nat @ zero_zero_nat @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 18.74/5.36 thf(178,axiom,((((=) @ real) = (^ [A:real,B:real]: ((ord_less_eq_real @ A @ B) & (ord_less_eq_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_218_order__class_Oorder_Oeq__iff)).
% 18.74/5.36 thf(989,plain,((((=) @ real) = (^ [A:real,B:real]: ((ord_less_eq_real @ A @ B) & (ord_less_eq_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 18.74/5.36 thf(143,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((B = C) => (ord_less_eq_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_ord__le__eq__trans)).
% 18.74/5.36 thf(857,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((B = C) => (ord_less_eq_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 18.74/5.36 thf(175,axiom,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ B @ A) & (ord_less_eq_nat @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_dual__order_Oeq__iff)).
% 18.74/5.36 thf(980,plain,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ B @ A) & (ord_less_eq_nat @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 18.74/5.36 thf(36,axiom,((ord_less_eq_real = (^ [A:real,B:real]: ((ord_min_real @ B @ A) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_118_min_Oabsorb__iff2)).
% 18.74/5.36 thf(403,plain,(((ord_less_eq_real) = (^ [A:real,B:real]: ((ord_min_real @ B @ A) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 18.74/5.36 thf(19,axiom,((! [A:real]: (ord_less_eq_real @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_208_dual__order_Orefl)).
% 18.74/5.36 thf(339,plain,((! [A:real]: (ord_less_eq_real @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 18.74/5.36 thf(75,axiom,(((reflect_poly_real @ zero_zero_poly_real) = zero_zero_poly_real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_reflect__poly__0)).
% 18.74/5.36 thf(537,plain,(((reflect_poly_real @ zero_zero_poly_real) = zero_zero_poly_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 18.74/5.36 thf(103,axiom,((! [A:nat]: ((A != zero_zero_nat) => (ord_less_nat @ zero_zero_nat @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_185_gr0I)).
% 18.74/5.36 thf(637,plain,((! [A:nat]: ((~ (A = zero_zero_nat)) => (ord_less_nat @ zero_zero_nat @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 18.74/5.36 thf(173,axiom,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_341_order__le__less__subst2)).
% 18.74/5.36 thf(970,plain,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 18.74/5.36 thf(284,axiom,((! [A:real,B:real,C:poly_real]: ((ord_less_real @ A @ B) => ((ord_less_real @ zero_zero_real @ (poly_real2 @ C @ A)) => ((ord_less_real @ (poly_real2 @ C @ B) @ zero_zero_real) => (? [D:real]: ((ord_less_real @ A @ D) & (ord_less_real @ D @ B) & ((poly_real2 @ C @ D) = zero_zero_real)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_poly__IVT__neg)).
% 18.74/5.36 thf(1419,plain,((! [A:real,B:real,C:poly_real]: ((ord_less_real @ A @ B) => ((ord_less_real @ zero_zero_real @ (poly_real2 @ C @ A)) => ((ord_less_real @ (poly_real2 @ C @ B) @ zero_zero_real) => (? [D:real]: ((ord_less_real @ A @ D) & (ord_less_real @ D @ B) & ((poly_real2 @ C @ D) = zero_zero_real)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[284])).
% 18.74/5.36 thf(206,axiom,(((sgn_sgn_real @ zero_zero_real) = zero_zero_real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_142_sgn__zero)).
% 18.74/5.36 thf(1114,plain,(((sgn_sgn_real @ zero_zero_real) = zero_zero_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 18.74/5.36 thf(177,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_323_order_Ostrict__implies__not__eq)).
% 18.74/5.36 thf(985,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 18.74/5.36 thf(240,axiom,((! [A:real,B:real,C:(real > real),D:real]: ((ord_less_real @ A @ B) => ((ord_less_real @ (C @ B) @ D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_real @ (C @ E) @ (C @ F)))) => (ord_less_real @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_264_order__less__subst2)).
% 18.74/5.36 thf(1249,plain,((! [A:real,B:real,C:(real > real),D:real]: ((ord_less_real @ A @ B) => ((ord_less_real @ (C @ B) @ D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_real @ (C @ E) @ (C @ F)))) => (ord_less_real @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 18.74/5.36 thf(193,axiom,((! [A:real]: ((ord_less_eq_real @ A @ lb2) => ((sgn_sgn_real @ (poly_real2 @ p @ A)) = (sturm_1076696862f_real @ p))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_lb2)).
% 18.74/5.36 thf(1050,plain,((! [A:real]: ((ord_less_eq_real @ A @ lb2) => ((sgn_sgn_real @ (poly_real2 @ p @ A)) = (sturm_1076696862f_real @ p))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 18.74/5.36 thf(157,axiom,((ord_less_eq_nat = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_168_le__eq__less__or__eq)).
% 18.74/5.36 thf(911,plain,(((ord_less_eq_nat) = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 18.74/5.36 thf(183,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_89_complete__real)).
% 18.74/5.36 thf(1002,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)],[183])).
% 18.74/5.36 thf(84,axiom,((! [A:real,B:real]: (ord_less_eq_real @ (ord_min_real @ A @ B) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_112_min_Ocobounded1)).
% 18.74/5.36 thf(569,plain,((! [A:real,B:real]: (ord_less_eq_real @ (ord_min_real @ A @ B) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 18.74/5.36 thf(106,axiom,((! [A:nat,B:(nat > $o),C:nat]: ((! [D:nat]: ((ord_less_nat @ A @ D) => (B @ D))) => ((! [D:nat]: ((ord_less_eq_nat @ D @ A) => ((! [E:nat]: ((ord_less_nat @ D @ E) => (B @ E))) => (B @ D)))) => (B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_199_nat__descend__induct)).
% 18.74/5.36 thf(647,plain,((! [A:nat,B:(nat > $o),C:nat]: ((! [D:nat]: ((ord_less_nat @ A @ D) => (B @ D))) => ((! [D:nat]: ((ord_less_eq_nat @ D @ A) => ((! [E:nat]: ((ord_less_nat @ D @ E) => (B @ E))) => (B @ D)))) => (B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 18.74/5.36 thf(243,axiom,((! [A:real]: ? [B:real]: (ord_less_real @ A @ B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_269_gt__ex)).
% 18.74/5.36 thf(1263,plain,((! [A:real]: ? [B:real]: (ord_less_real @ A @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[243])).
% 18.74/5.36 thf(181,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ zero_zero_nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_not__less__zero)).
% 18.74/5.36 thf(997,plain,((! [A:nat]: ~ (ord_less_nat @ A @ zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 18.74/5.36 thf(93,axiom,((! [A:real,B:real]: (ord_less_eq_real @ (ord_min_real @ A @ B) @ B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_min_Ocobounded2)).
% 18.74/5.36 thf(605,plain,((! [A:real,B:real]: (ord_less_eq_real @ (ord_min_real @ A @ B) @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 18.74/5.36 thf(277,axiom,((! [A:real]: ((ord_less_real @ (sgn_sgn_real @ A) @ zero_zero_real) = (ord_less_real @ A @ zero_zero_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_137_sgn__less)).
% 18.74/5.36 thf(1393,plain,((! [A:real]: ((ord_less_real @ (sgn_sgn_real @ A) @ zero_zero_real) = (ord_less_real @ A @ zero_zero_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[277])).
% 18.74/5.36 thf(259,axiom,((! [A:poly_real]: ((A != zero_zero_poly_real) => (~ (! [B:real]: ((! [C:real]: (((poly_real2 @ A @ C) = zero_zero_real) => (ord_less_real @ C @ B))) => (~ (! [C:real]: ((ord_less_eq_real @ B @ C) => ((sgn_sgn_real @ (poly_real2 @ A @ C)) = (sturm_1308388506f_real @ A))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_root__ub)).
% 18.74/5.36 thf(1318,plain,((! [A:poly_real]: ((~ (A = zero_zero_poly_real)) => (~ (! [B:real]: ((! [C:real]: (((poly_real2 @ A @ C) = zero_zero_real) => (ord_less_real @ C @ B))) => (~ (! [C:real]: ((ord_less_eq_real @ B @ C) => ((sgn_sgn_real @ (poly_real2 @ A @ C)) = (sturm_1308388506f_real @ A))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[259])).
% 18.74/5.36 thf(27,axiom,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) = (A = zero_zero_nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_le__zero__eq)).
% 18.74/5.36 thf(360,plain,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 18.74/5.36 thf(10,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => (A = (ord_min_real @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_min_OorderE)).
% 18.74/5.36 thf(311,plain,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => (A = (ord_min_real @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 18.74/5.36 thf(160,axiom,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_nat @ A @ (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_263_order__less__subst1)).
% 18.74/5.36 thf(921,plain,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_nat @ A @ (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 18.74/5.36 thf(127,axiom,((! [A:nat,B:nat,C:nat]: ((A = B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_291_ord__eq__less__trans)).
% 18.74/5.36 thf(765,plain,((! [A:nat,B:nat,C:nat]: ((A = B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 18.74/5.36 thf(222,axiom,((! [A:real]: ((ord_less_eq_real @ zero_zero_real @ (sgn_sgn_real @ A)) = (ord_less_eq_real @ zero_zero_real @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_130_zero__le__sgn__iff)).
% 18.74/5.36 thf(1170,plain,((! [A:real]: ((ord_less_eq_real @ zero_zero_real @ (sgn_sgn_real @ A)) = (ord_less_eq_real @ zero_zero_real @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 18.74/5.36 thf(35,axiom,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_eq_nat @ A @ (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_337_order__le__less__subst1)).
% 18.74/5.36 thf(398,plain,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_eq_nat @ A @ (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 18.74/5.36 thf(170,axiom,((! [A:nat,B:nat,C:(nat > real),D:real]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_real @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_real @ (C @ E) @ (C @ F)))) => (ord_less_eq_real @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_order__subst2)).
% 18.74/5.36 thf(953,plain,((! [A:nat,B:nat,C:(nat > real),D:real]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_real @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_real @ (C @ E) @ (C @ F)))) => (ord_less_eq_real @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 18.74/5.36 thf(149,axiom,((~ (ord_less_nat @ zero_zero_nat @ zero_zero_nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_less__numeral__extra_I3_J)).
% 18.74/5.36 thf(888,plain,((~ (ord_less_nat @ zero_zero_nat @ zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 18.74/5.36 thf(161,axiom,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ (ord_min_real @ A @ B) @ C) = ((ord_less_eq_real @ A @ C) | (ord_less_eq_real @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_124_min__le__iff__disj)).
% 18.74/5.36 thf(926,plain,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ (ord_min_real @ A @ B) @ C) = ((ord_less_eq_real @ A @ C) | (ord_less_eq_real @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 18.74/5.36 thf(187,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_171_linorder__neqE__nat)).
% 18.74/5.36 thf(1026,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)],[187])).
% 18.74/5.36 thf(221,axiom,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ B) => ((ord_less_real @ B @ C) => (ord_less_real @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_311_order_Ostrict__trans)).
% 18.74/5.36 thf(1167,plain,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ B) => ((ord_less_real @ B @ C) => (ord_less_real @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 18.74/5.36 thf(212,axiom,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_324_dual__order_Ostrict__implies__not__eq)).
% 18.74/5.36 thf(1135,plain,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 18.74/5.36 thf(97,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_209_dual__order_Orefl)).
% 18.74/5.36 thf(618,plain,((! [A:nat]: (ord_less_eq_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 18.74/5.36 thf(214,axiom,((! [A:real,B:real]: ((~ (ord_less_real @ A @ B)) => ((~ (ord_less_real @ B @ A)) = (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_301_antisym__conv3)).
% 18.74/5.36 thf(1146,plain,((! [A:real,B:real]: ((~ (ord_less_real @ A @ B)) => ((~ (ord_less_real @ B @ A)) = (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 18.74/5.36 thf(254,axiom,((! [A:real,B:real]: ((A != B) => ((~ (ord_less_real @ A @ B)) => (ord_less_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_144_linorder__neqE__linordered__idom)).
% 18.74/5.36 thf(1301,plain,((! [A:real,B:real]: ((~ (A = B)) => ((~ (ord_less_real @ A @ B)) => (ord_less_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[254])).
% 18.74/5.36 thf(86,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_177_less__not__refl)).
% 18.74/5.36 thf(573,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 18.74/5.36 thf(5,axiom,((! [A:poly_real]: ((poly_poly_real2 @ zero_z1423781445y_real @ A) = zero_zero_poly_real))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_poly__0)).
% 18.74/5.36 thf(296,plain,((! [A:poly_real]: ((poly_poly_real2 @ zero_z1423781445y_real @ A) = zero_zero_poly_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 18.74/5.36 thf(47,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ A) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_antisym)).
% 18.74/5.36 thf(444,plain,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 18.74/5.36 thf(273,axiom,((! [A:real]: ? [B:real]: (ord_less_real @ B @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_268_lt__ex)).
% 18.74/5.36 thf(1374,plain,((! [A:real]: ? [B:real]: (ord_less_real @ B @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[273])).
% 18.74/5.36 thf(174,axiom,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_267_order__less__subst2)).
% 18.74/5.36 thf(975,plain,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 18.74/5.36 thf(115,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_172_infinite__descent)).
% 18.74/5.36 thf(694,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)],[115])).
% 18.74/5.36 thf(122,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_312_order_Ostrict__trans)).
% 18.74/5.36 thf(732,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 18.74/5.36 thf(276,axiom,((! [A:nat,B:(real > nat),C:real,D:real]: ((ord_less_nat @ A @ (B @ C)) => ((ord_less_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_262_order__less__subst1)).
% 18.74/5.36 thf(1388,plain,((! [A:nat,B:(real > nat),C:real,D:real]: ((ord_less_nat @ A @ (B @ C)) => ((ord_less_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[276])).
% 18.74/5.36 thf(88,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ zero_zero_nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_179_bot__nat__0_Oextremum__strict)).
% 18.74/5.36 thf(579,plain,((! [A:nat]: ~ (ord_less_nat @ A @ zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 18.74/5.36 thf(78,axiom,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_161_eq__imp__le)).
% 18.74/5.36 thf(545,plain,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 18.74/5.36 thf(40,axiom,((! [A:real,B:(nat > real),C:nat,D:nat]: ((ord_less_eq_real @ A @ (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_real @ (B @ E) @ (B @ F)))) => (ord_less_eq_real @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_249_order__subst1)).
% 18.74/5.36 thf(413,plain,((! [A:real,B:(nat > real),C:nat,D:nat]: ((ord_less_eq_real @ A @ (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_real @ (B @ E) @ (B @ F)))) => (ord_less_eq_real @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 18.74/5.36 thf(171,axiom,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_255_ord__eq__less__subst)).
% 18.74/5.36 thf(958,plain,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 18.74/5.36 thf(280,axiom,((~ (! [A:real]: ~ (! [B:real]: ((ord_less_eq_real @ B @ A) => ((sgn_sgn_real @ (poly_real2 @ p @ B)) = (sturm_1076696862f_real @ p))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062lb2_O_A_092_060forall_062x_092_060le_062lb2_O_Asgn_A_Ipoly_Ap_Ax_J_A_061_Asgn__neg__inf_Ap_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062)).
% 18.74/5.36 thf(1403,plain,((~ (! [A:real]: ~ (! [B:real]: ((ord_less_eq_real @ B @ A) => ((sgn_sgn_real @ (poly_real2 @ p @ B)) = (sturm_1076696862f_real @ p))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[280])).
% 18.74/5.36 thf(213,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)) => ((poly_real2 @ A @ D) != zero_zero_real)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_next__non__root__interval)).
% 18.74/5.36 thf(1139,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)) => (~ ((poly_real2 @ A @ D) = zero_zero_real))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 18.74/5.36 thf(272,axiom,((! [A:poly_real]: ((! [B:real]: ((poly_real2 @ A @ B) = zero_zero_real)) = (A = zero_zero_poly_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_poly__all__0__iff__0)).
% 18.74/5.36 thf(1371,plain,((! [A:poly_real]: ((! [B:real]: ((poly_real2 @ A @ B) = zero_zero_real)) = (A = zero_zero_poly_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[272])).
% 18.74/5.36 thf(95,axiom,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_235_eq__iff)).
% 18.74/5.36 thf(611,plain,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 18.74/5.36 thf(196,axiom,((! [A:real,B:real,C:(real > nat),D:nat]: ((ord_less_real @ A @ B) => (((C @ B) = D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_257_ord__less__eq__subst)).
% 18.74/5.36 thf(1058,plain,((! [A:real,B:real,C:(real > nat),D:nat]: ((ord_less_real @ A @ B) => (((C @ B) = D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 18.74/5.36 thf(262,axiom,((p != zero_zero_poly_real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_assms)).
% 18.74/5.36 thf(1332,plain,((~ (p = zero_zero_poly_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[262])).
% 18.74/5.36 thf(168,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_min_real @ A @ B) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_min_Oabsorb1)).
% 18.74/5.36 thf(947,plain,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_min_real @ A @ B) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 18.74/5.36 thf(111,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_167_less__or__eq__imp__le)).
% 18.74/5.36 thf(672,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)],[111])).
% 18.74/5.36 thf(229,axiom,((! [A:nat,B:nat,C:(nat > real),D:real]: ((ord_less_eq_nat @ A @ B) => ((ord_less_real @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_real @ (C @ E) @ (C @ F)))) => (ord_less_real @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_340_order__le__less__subst2)).
% 18.74/5.36 thf(1194,plain,((! [A:nat,B:nat,C:(nat > real),D:real]: ((ord_less_eq_nat @ A @ B) => ((ord_less_real @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_real @ (C @ E) @ (C @ F)))) => (ord_less_real @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 18.74/5.36 thf(248,axiom,((! [A:real]: (((sgn_sgn_real @ A) = zero_zero_real) = (A = zero_zero_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_151_sgn__zero__iff)).
% 18.74/5.36 thf(1282,plain,((! [A:real]: (((sgn_sgn_real @ A) = zero_zero_real) = (A = zero_zero_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[248])).
% 18.74/5.36 thf(268,axiom,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ B) => ((B = C) => (ord_less_real @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_292_ord__less__eq__trans)).
% 18.74/5.36 thf(1349,plain,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ B) => ((B = C) => (ord_less_real @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[268])).
% 18.74/5.36 thf(83,axiom,((! [A:real]: (ord_less_eq_real @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_191_order__refl)).
% 18.74/5.36 thf(567,plain,((! [A:real]: (ord_less_eq_real @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 18.74/5.36 thf(12,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_min_real @ B @ A) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_min_Oabsorb2)).
% 18.74/5.36 thf(318,plain,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_min_real @ B @ A) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 18.74/5.36 thf(209,axiom,((! [A:nat,B:(real > nat),C:real,D:real]: ((ord_less_eq_nat @ A @ (B @ C)) => ((ord_less_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_336_order__le__less__subst1)).
% 18.74/5.36 thf(1122,plain,((! [A:nat,B:(real > nat),C:real,D:real]: ((ord_less_eq_nat @ A @ (B @ C)) => ((ord_less_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 18.74/5.36 thf(274,axiom,((! [A:real,B:real,C:poly_real]: ((! [D:real]: (((ord_less_eq_real @ A @ D) & (ord_less_real @ D @ B)) => ((poly_real2 @ C @ D) != zero_zero_real))) = (! [D:real]: (((ord_less_eq_real @ A @ D) & (ord_less_real @ D @ B)) => (ord_less_real @ zero_zero_real @ (poly_real2 @ C @ D))) | ! [D:real]: (((ord_less_eq_real @ A @ D) & (ord_less_real @ D @ B)) => (ord_less_real @ (poly_real2 @ C @ D) @ zero_zero_real)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_129_not__eq__pos__or__neg__iff__2)).
% 18.74/5.36 thf(1376,plain,((! [A:real,B:real,C:poly_real]: ((! [D:real]: (((ord_less_eq_real @ A @ D) & (ord_less_real @ D @ B)) => (~ ((poly_real2 @ C @ D) = zero_zero_real)))) = (! [D:real]: (((ord_less_eq_real @ A @ D) & (ord_less_real @ D @ B)) => (ord_less_real @ zero_zero_real @ (poly_real2 @ C @ D))) | ! [D:real]: (((ord_less_eq_real @ A @ D) & (ord_less_real @ D @ B)) => (ord_less_real @ (poly_real2 @ C @ D) @ zero_zero_real)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[274])).
% 18.74/5.36 thf(224,axiom,((! [A:real,B:real,C:real]: ((ord_less_real @ (ord_min_real @ A @ B) @ C) = ((ord_less_real @ A @ C) | (ord_less_real @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_min__less__iff__disj)).
% 18.74/5.36 thf(1175,plain,((! [A:real,B:real,C:real]: ((ord_less_real @ (ord_min_real @ A @ B) @ C) = ((ord_less_real @ A @ C) | (ord_less_real @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 18.74/5.36 thf(113,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != zero_zero_nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_181_gr__implies__not0)).
% 18.74/5.36 thf(681,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 18.74/5.36 thf(281,axiom,((! [A:nat,B:nat,C:(nat > real),D:real]: ((ord_less_nat @ A @ B) => ((ord_less_real @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_real @ (C @ E) @ (C @ F)))) => (ord_less_real @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_266_order__less__subst2)).
% 18.74/5.36 thf(1408,plain,((! [A:nat,B:nat,C:(nat > real),D:real]: ((ord_less_nat @ A @ B) => ((ord_less_real @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_real @ (C @ E) @ (C @ F)))) => (ord_less_real @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[281])).
% 18.74/5.36 thf(146,axiom,((! [A:real,B:real]: ((ord_min_real @ A @ (ord_min_real @ A @ B)) = (ord_min_real @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_min_Oleft__idem)).
% 18.74/5.36 thf(880,plain,((! [A:real,B:real]: ((ord_min_real @ A @ (ord_min_real @ A @ B)) = (ord_min_real @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 18.74/5.36 thf(191,axiom,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_eq__refl)).
% 18.74/5.36 thf(1043,plain,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 18.74/5.36 thf(150,axiom,((! [A:nat]: ((A != zero_zero_nat) => (ord_less_nat @ zero_zero_nat @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_gr__zeroI)).
% 18.74/5.36 thf(890,plain,((! [A:nat]: ((~ (A = zero_zero_nat)) => (ord_less_nat @ zero_zero_nat @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 18.74/5.36 thf(135,axiom,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_zero__le)).
% 18.74/5.36 thf(811,plain,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 18.74/5.36 thf(60,axiom,((! [A:real,B:real,C:(real > real),D:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ (C @ B) @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_real @ (C @ E) @ (C @ F)))) => (ord_less_eq_real @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_244_order__subst2)).
% 18.74/5.36 thf(494,plain,((! [A:real,B:real,C:(real > real),D:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ (C @ B) @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_real @ (C @ E) @ (C @ F)))) => (ord_less_eq_real @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 18.74/5.36 thf(80,axiom,((! [A:real,B:(nat > real),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_real @ (B @ E) @ (B @ F)))) => (ord_less_eq_real @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_242_ord__eq__le__subst)).
% 18.74/5.36 thf(552,plain,((! [A:real,B:(nat > real),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_real @ (B @ E) @ (B @ F)))) => (ord_less_eq_real @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 18.74/5.36 thf(137,axiom,((ord_le1180086932y_real @ zero_zero_poly_real @ zero_zero_poly_real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_le__numeral__extra_I3_J)).
% 18.74/5.36 thf(816,plain,((ord_le1180086932y_real @ zero_zero_poly_real @ zero_zero_poly_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 18.74/5.36 thf(91,axiom,((! [A:real,B:real,C:(real > real),D:real]: ((ord_less_eq_real @ A @ B) => (((C @ B) = D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_real @ (C @ E) @ (C @ F)))) => (ord_less_eq_real @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_ord__le__eq__subst)).
% 18.74/5.36 thf(594,plain,((! [A:real,B:real,C:(real > real),D:real]: ((ord_less_eq_real @ A @ B) => (((C @ B) = D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_real @ (C @ E) @ (C @ F)))) => (ord_less_eq_real @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 18.74/5.36 thf(67,axiom,((is_zero_real = (^ [A:poly_real]: (A = zero_zero_poly_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_is__zero__null)).
% 18.74/5.36 thf(520,plain,(((is_zero_real) = (^ [A:poly_real]: (A = zero_zero_poly_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 18.74/5.36 thf(260,axiom,((! [A:real,B:real]: ((A != B) => ((~ (ord_less_real @ A @ B)) => (ord_less_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_271_neqE)).
% 18.74/5.36 thf(1325,plain,((! [A:real,B:real]: ((~ (A = B)) => ((~ (ord_less_real @ A @ B)) => (ord_less_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[260])).
% 18.74/5.36 thf(188,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_231_linear)).
% 18.74/5.36 thf(1029,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)],[188])).
% 18.74/5.36 thf(215,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)) => ((poly_real2 @ A @ D) != zero_zero_real)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_last__non__root__interval)).
% 18.74/5.36 thf(1149,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)) => (~ ((poly_real2 @ A @ D) = zero_zero_real))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 18.74/5.36 thf(266,axiom,((! [A:poly_real]: (((poly_real2 @ (reflect_poly_real @ A) @ zero_zero_real) = zero_zero_real) = (A = zero_zero_poly_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_reflect__poly__at__0__eq__0__iff)).
% 18.74/5.36 thf(1344,plain,((! [A:poly_real]: (((poly_real2 @ (reflect_poly_real @ A) @ zero_zero_real) = zero_zero_real) = (A = zero_zero_poly_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[266])).
% 18.74/5.36 thf(252,axiom,((! [A:real]: (((sgn_sgn_real @ A) = zero_zero_real) = (A = zero_zero_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_145_sgn__eq__0__iff)).
% 18.74/5.36 thf(1293,plain,((! [A:real]: (((sgn_sgn_real @ A) = zero_zero_real) = (A = zero_zero_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[252])).
% 18.74/5.36 thf(163,axiom,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) = (A = zero_zero_nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_189_bot__nat__0_Oextremum__unique)).
% 18.74/5.36 thf(932,plain,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 18.74/5.36 thf(205,axiom,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (~ (ord_less_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_280_less__asym)).
% 18.74/5.36 thf(1112,plain,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (~ (ord_less_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 18.74/5.36 thf(126,axiom,((! [A:(real > (real > $o)),B:real,C:real]: ((! [D:real,E:real]: ((ord_less_eq_real @ D @ E) => (A @ D @ E))) => ((! [D:real,E:real]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_linorder__wlog)).
% 18.74/5.36 thf(758,plain,((! [A:(real > (real > $o)),B:real,C:real]: ((! [D:real,E:real]: ((ord_less_eq_real @ D @ E) => (A @ D @ E))) => ((! [D:real,E:real]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 18.74/5.36 thf(264,axiom,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (~ (ord_less_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_282_less__asym_H)).
% 18.74/5.36 thf(1339,plain,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (~ (ord_less_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[264])).
% 18.74/5.36 thf(114,axiom,((! [A:real,B:real,C:(real > nat),D:nat]: ((ord_less_eq_real @ A @ B) => (((C @ B) = D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_237_ord__le__eq__subst)).
% 18.74/5.36 thf(685,plain,((! [A:real,B:real,C:(real > nat),D:nat]: ((ord_less_eq_real @ A @ B) => (((C @ B) = D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 18.74/5.36 thf(278,axiom,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_278_less__imp__neq)).
% 18.74/5.36 thf(1396,plain,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[278])).
% 18.74/5.36 thf(233,axiom,((! [A:real,B:real]: ((A != B) = ((ord_less_real @ A @ B) | (ord_less_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_273_neq__iff)).
% 18.74/5.36 thf(1213,plain,((! [A:real,B:real]: ((~ (A = B)) = ((ord_less_real @ A @ B) | (ord_less_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 18.74/5.36 thf(147,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_310_dual__order_Oirrefl)).
% 18.74/5.36 thf(883,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 18.74/5.36 thf(185,axiom,((! [A:nat]: ? [B:nat]: (ord_less_nat @ A @ B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_270_gt__ex)).
% 18.74/5.36 thf(1015,plain,((! [A:nat]: ? [B:nat]: (ord_less_nat @ A @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 18.74/5.36 thf(182,axiom,(((sgn_sgn_poly_real @ zero_zero_poly_real) = zero_zero_poly_real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_sgn__0)).
% 18.74/5.36 thf(1000,plain,(((sgn_sgn_poly_real @ zero_zero_poly_real) = zero_zero_poly_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 18.74/5.36 thf(6,axiom,((! [A:poly_poly_real,B:poly_poly_real]: (((poly_poly_real2 @ A) = (poly_poly_real2 @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_poly__eq__poly__eq__iff)).
% 18.74/5.36 thf(299,plain,((! [A:poly_poly_real,B:poly_poly_real]: (((poly_poly_real2 @ A) = (poly_poly_real2 @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 18.74/5.36 thf(202,axiom,((! [A:real]: ((ord_less_eq_real @ (sgn_sgn_real @ A) @ zero_zero_real) = (ord_less_eq_real @ A @ zero_zero_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_sgn__le__0__iff)).
% 18.74/5.36 thf(1102,plain,((! [A:real]: ((ord_less_eq_real @ (sgn_sgn_real @ A) @ zero_zero_real) = (ord_less_eq_real @ A @ zero_zero_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 18.74/5.36 thf(43,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => (ord_less_eq_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_329_leI)).
% 18.74/5.36 thf(431,plain,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => (ord_less_eq_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 18.74/5.36 thf(118,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_159_le__refl)).
% 18.74/5.36 thf(722,plain,((! [A:nat]: (ord_less_eq_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 18.74/5.36 thf(255,axiom,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ (ord_min_real @ B @ C)) => (~ ((ord_less_real @ A @ B) => (~ (ord_less_real @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_min_Ostrict__boundedE)).
% 18.74/5.36 thf(1304,plain,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ (ord_min_real @ B @ C)) => (~ ((ord_less_real @ A @ B) => (~ (ord_less_real @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[255])).
% 18.74/5.36 thf(231,axiom,((! [A:real]: (((poly_real2 @ p @ A) = zero_zero_real) => (ord_less_real @ lb1 @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_lb1)).
% 18.74/5.36 thf(1208,plain,((! [A:real]: (((poly_real2 @ p @ A) = zero_zero_real) => (ord_less_real @ lb1 @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[231])).
% 18.74/5.36 thf(108,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_276_order_Oasym)).
% 18.74/5.36 thf(663,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 18.74/5.36 thf(31,axiom,((! [A:real,B:real]: ((~ (ord_less_eq_real @ A @ B)) => (ord_less_eq_real @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_226_le__cases)).
% 18.74/5.36 thf(374,plain,((! [A:real,B:real]: ((~ (ord_less_eq_real @ A @ B)) => (ord_less_eq_real @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 18.74/5.36 thf(165,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_289_less__irrefl)).
% 18.74/5.36 thf(939,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 18.74/5.36 thf(282,axiom,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_322_order_Ostrict__implies__not__eq)).
% 18.74/5.36 thf(1413,plain,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[282])).
% 18.74/5.36 thf(55,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_314_less__imp__not__less)).
% 18.74/5.36 thf(473,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 18.74/5.36 thf(72,axiom,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_152_le0)).
% 18.74/5.36 thf(531,plain,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 18.74/5.36 thf(167,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) = ((ord_less_nat @ B @ A) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_321_not__less__iff__gr__or__eq)).
% 18.74/5.36 thf(944,plain,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) = ((ord_less_nat @ B @ A) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 18.74/5.36 thf(69,axiom,((ord_min_real = (^ [A:real,B:real]: (ord_min_real @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_min_Ocommute)).
% 18.74/5.36 thf(525,plain,(((ord_min_real) = (^ [A:real,B:real]: (ord_min_real @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 18.74/5.36 thf(104,axiom,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ (ord_min_real @ B @ C)) => (~ ((ord_less_eq_real @ A @ B) => (~ (ord_less_eq_real @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_106_min_OboundedE)).
% 18.74/5.36 thf(640,plain,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ (ord_min_real @ B @ C)) => (~ ((ord_less_eq_real @ A @ B) => (~ (ord_less_eq_real @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 18.74/5.36 thf(198,axiom,((! [A:(real > (real > $o)),B:real,C:real]: ((! [D:real,E:real]: ((ord_less_real @ D @ E) => (A @ D @ E))) => ((! [D:real]: (A @ D @ D)) => ((! [D:real,E:real]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_316_linorder__less__wlog)).
% 18.74/5.36 thf(1070,plain,((! [A:(real > (real > $o)),B:real,C:real]: ((! [D:real,E:real]: ((ord_less_real @ D @ E) => (A @ D @ E))) => ((! [D:real]: (A @ D @ D)) => ((! [D:real,E:real]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 18.74/5.36 thf(216,axiom,((! [A:real]: (((sgn_sgn_real @ A) = zero_zero_real) = (A = zero_zero_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_148_sgn__0__0)).
% 18.74/5.36 thf(1156,plain,((! [A:real]: (((sgn_sgn_real @ A) = zero_zero_real) = (A = zero_zero_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 18.74/5.36 thf(245,axiom,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ B) => (ord_less_real @ (ord_min_real @ A @ C) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_min_Ostrict__coboundedI1)).
% 18.74/5.36 thf(1267,plain,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ B) => (ord_less_real @ (ord_min_real @ A @ C) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[245])).
% 18.74/5.36 thf(180,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != zero_zero_nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_gr__implies__not__zero)).
% 18.74/5.36 thf(993,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 18.74/5.36 thf(235,axiom,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ (ord_min_real @ B @ C)) = ((ord_less_real @ A @ B) & (ord_less_real @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_min__less__iff__conj)).
% 18.74/5.36 thf(1225,plain,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ (ord_min_real @ B @ C)) = ((ord_less_real @ A @ B) & (ord_less_real @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 18.74/5.36 thf(279,axiom,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ B) => ((ord_less_real @ B @ C) => (ord_less_real @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_284_less__trans)).
% 18.74/5.36 thf(1400,plain,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ B) => ((ord_less_real @ B @ C) => (ord_less_real @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[279])).
% 18.74/5.36 thf(194,axiom,((ord_less_real = (^ [A:real,B:real]: ((ord_less_eq_real @ A @ B) & (A != B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_332_less__le)).
% 18.74/5.36 thf(1053,plain,(((ord_less_real) = (^ [A:real,B:real]: ((ord_less_eq_real @ A @ B) & ~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 18.74/5.36 thf(227,axiom,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ B) => ((ord_less_real @ C @ A) => (ord_less_real @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_318_dual__order_Ostrict__trans)).
% 18.74/5.36 thf(1186,plain,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ B) => ((ord_less_real @ C @ A) => (ord_less_real @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 18.74/5.36 thf(90,axiom,((! [A:nat,B:nat,C:(nat > real),D:real]: ((ord_less_eq_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_real @ (C @ E) @ (C @ F)))) => (ord_less_eq_real @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_ord__le__eq__subst)).
% 18.74/5.36 thf(585,plain,((! [A:nat,B:nat,C:(nat > real),D:real]: ((ord_less_eq_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_real @ (C @ E) @ (C @ F)))) => (ord_less_eq_real @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 18.74/5.36 thf(62,axiom,((ord_less_eq_real = (^ [A:real,B:real]: (A = (ord_min_real @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_min_Oorder__iff)).
% 18.74/5.36 thf(502,plain,(((ord_less_eq_real) = (^ [A:real,B:real]: (A = (ord_min_real @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 18.74/5.36 thf(142,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_180_infinite__descent0)).
% 18.74/5.36 thf(840,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)],[142])).
% 18.74/5.36 thf(134,axiom,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ A @ C) => (ord_less_eq_real @ A @ (ord_min_real @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_108_min_OboundedI)).
% 18.74/5.36 thf(808,plain,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ A @ C) => (ord_less_eq_real @ A @ (ord_min_real @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 18.74/5.36 thf(211,axiom,((! [A:real,B:(nat > real),C:nat,D:nat]: ((ord_less_real @ A @ (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_real @ (B @ E) @ (B @ F)))) => (ord_less_real @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_261_order__less__subst1)).
% 18.74/5.36 thf(1130,plain,((! [A:real,B:(nat > real),C:nat,D:nat]: ((ord_less_real @ A @ (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_real @ (B @ E) @ (B @ F)))) => (ord_less_real @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 18.74/5.36 thf(249,axiom,((! [A:real,B:real,C:$o]: ((ord_less_real @ A @ B) => ((ord_less_real @ B @ A) => (C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_305_less__imp__triv)).
% 18.74/5.36 thf(1285,plain,((! [A:real,B:real,C:$o]: ((ord_less_real @ A @ B) => ((ord_less_real @ B @ A) => (C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[249])).
% 18.74/5.36 thf(155,axiom,((ord_less_eq_real = (^ [A:real,B:real]: ((ord_min_real @ A @ B) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_116_min_Oabsorb__iff1)).
% 18.74/5.36 thf(907,plain,(((ord_less_eq_real) = (^ [A:real,B:real]: ((ord_min_real @ A @ B) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 18.74/5.36 thf(54,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_211_order__trans)).
% 18.74/5.36 thf(470,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)],[54])).
% 18.74/5.36 thf(87,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((~ (ord_less_nat @ B @ A)) = (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_302_antisym__conv3)).
% 18.74/5.36 thf(576,plain,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((~ (ord_less_nat @ B @ A)) = (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 18.74/5.36 thf(18,axiom,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ C) => (ord_less_eq_real @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_224_order_Otrans)).
% 18.74/5.36 thf(336,plain,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ C) => (ord_less_eq_real @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 18.74/5.36 thf(242,axiom,((! [A:real,B:real]: ((ord_less_real @ zero_zero_real @ A) => ((ord_less_real @ zero_zero_real @ B) => (? [C:real]: ((ord_less_real @ zero_zero_real @ C) & (ord_less_real @ C @ A) & (ord_less_real @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_field__lbound__gt__zero)).
% 18.74/5.36 thf(1257,plain,((! [A:real,B:real]: ((ord_less_real @ zero_zero_real @ A) => ((ord_less_real @ zero_zero_real @ B) => (? [C:real]: ((ord_less_real @ zero_zero_real @ C) & (ord_less_real @ C @ A) & (ord_less_real @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 18.74/5.36 thf(116,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_164_Nat_Oex__has__greatest__nat)).
% 18.74/5.36 thf(703,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)],[116])).
% 18.74/5.36 thf(96,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_165_less__mono__imp__le__mono)).
% 18.74/5.36 thf(613,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)],[96])).
% 18.74/5.36 thf(120,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_283_less__asym_H)).
% 18.74/5.36 thf(727,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 18.74/5.36 thf(200,axiom,((! [A:real,B:real]: ((~ (ord_less_real @ A @ B)) = ((ord_less_real @ B @ A) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_320_not__less__iff__gr__or__eq)).
% 18.74/5.36 thf(1094,plain,((! [A:real,B:real]: ((~ (ord_less_real @ A @ B)) = ((ord_less_real @ B @ A) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 18.74/5.36 thf(11,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_175_less__not__refl3)).
% 18.74/5.36 thf(314,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 18.74/5.36 thf(85,axiom,((((=) @ real) = (^ [A:real,B:real]: ((ord_less_eq_real @ B @ A) & (ord_less_eq_real @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_dual__order_Oeq__iff)).
% 18.74/5.36 thf(571,plain,((((=) @ real) = (^ [A:real,B:real]: ((ord_less_eq_real @ B @ A) & (ord_less_eq_real @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 18.74/5.36 thf(238,axiom,((! [A:real,B:real,C:poly_real]: ((ord_less_real @ A @ B) => ((ord_less_real @ (poly_real2 @ C @ A) @ zero_zero_real) => ((ord_less_real @ zero_zero_real @ (poly_real2 @ C @ B)) => (? [D:real]: ((ord_less_real @ A @ D) & (ord_less_real @ D @ B) & ((poly_real2 @ C @ D) = zero_zero_real)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_poly__IVT__pos)).
% 18.74/5.36 thf(1240,plain,((! [A:real,B:real,C:poly_real]: ((ord_less_real @ A @ B) => ((ord_less_real @ (poly_real2 @ C @ A) @ zero_zero_real) => ((ord_less_real @ zero_zero_real @ (poly_real2 @ C @ B)) => (? [D:real]: ((ord_less_real @ A @ D) & (ord_less_real @ D @ B) & ((poly_real2 @ C @ D) = zero_zero_real)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[238])).
% 18.74/5.36 thf(179,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_327_leD)).
% 18.74/5.36 thf(991,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 18.74/5.36 thf(52,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ A) = (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_220_antisym__conv)).
% 18.74/5.36 thf(465,plain,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ A) = (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 18.74/5.36 thf(49,axiom,((! [A:real]: ((ord_min_real @ A @ A) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_min_Oidem)).
% 18.74/5.36 thf(450,plain,((! [A:real]: ((ord_min_real @ A @ A) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 18.74/5.36 thf(28,axiom,((! [A:nat]: ((~ (ord_less_nat @ zero_zero_nat @ A)) = (A = zero_zero_nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_184_not__gr0)).
% 18.74/5.36 thf(363,plain,((! [A:nat]: ((~ (ord_less_nat @ zero_zero_nat @ A)) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 18.74/5.36 thf(76,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ zero_zero_nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_155_less__nat__zero__code)).
% 18.74/5.36 thf(539,plain,((! [A:nat]: ~ (ord_less_nat @ A @ zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 18.74/5.36 thf(58,axiom,((! [A:poly_poly_real,B:poly_real]: (((poly_poly_real2 @ A @ B) != zero_zero_poly_real) => ((order_poly_real @ B @ A) = zero_zero_nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_order__0I)).
% 18.74/5.36 thf(482,plain,((! [A:poly_poly_real,B:poly_real]: ((~ ((poly_poly_real2 @ A @ B) = zero_zero_poly_real)) => ((order_poly_real @ B @ A) = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 18.74/5.36 thf(153,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_169_less__imp__le__nat)).
% 18.74/5.36 thf(903,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 18.74/5.36 thf(234,axiom,((! [A:real,B:(real > real),C:real,D:real]: ((A = (B @ C)) => ((ord_less_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_real @ (B @ E) @ (B @ F)))) => (ord_less_real @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_252_ord__eq__less__subst)).
% 18.74/5.36 thf(1216,plain,((! [A:real,B:(real > real),C:real,D:real]: ((A = (B @ C)) => ((ord_less_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_real @ (B @ E) @ (B @ F)))) => (ord_less_real @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[234])).
% 18.74/5.36 thf(228,axiom,((~ (! [A:real]: ~ (! [B:real]: (((poly_real2 @ p @ B) = zero_zero_real) => (ord_less_real @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062lb1_O_A_092_060forall_062x_O_Apoly_Ap_Ax_A_061_A0_A_092_060longrightarrow_062_Alb1_A_060_Ax_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062)).
% 18.74/5.36 thf(1189,plain,((~ (! [A:real]: ~ (! [B:real]: (((poly_real2 @ p @ B) = zero_zero_real) => (ord_less_real @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 18.74/5.36 thf(136,axiom,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ (ord_min_real @ B @ C)) = ((ord_less_eq_real @ A @ B) & (ord_less_eq_real @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_min_Obounded__iff)).
% 18.74/5.36 thf(813,plain,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ (ord_min_real @ B @ C)) = ((ord_less_eq_real @ A @ B) & (ord_less_eq_real @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 18.74/5.36 thf(66,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ zero_zero_nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_less__zeroE)).
% 18.74/5.36 thf(517,plain,((! [A:nat]: ~ (ord_less_nat @ A @ zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 18.74/5.36 thf(24,axiom,((! [A:real,B:real]: ((ord_min_real @ (ord_min_real @ A @ B) @ B) = (ord_min_real @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_min_Oright__idem)).
% 18.74/5.36 thf(351,plain,((! [A:real,B:real]: ((ord_min_real @ (ord_min_real @ A @ B) @ B) = (ord_min_real @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 18.74/5.36 thf(33,axiom,((! [A:nat,B:(real > nat),C:real,D:real]: ((ord_less_eq_nat @ A @ (B @ C)) => ((ord_less_eq_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_250_order__subst1)).
% 18.74/5.36 thf(390,plain,((! [A:nat,B:(real > nat),C:real,D:real]: ((ord_less_eq_nat @ A @ (B @ C)) => ((ord_less_eq_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 18.74/5.36 thf(101,axiom,((~ (ord_less_poly_real @ zero_zero_poly_real @ zero_zero_poly_real))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_less__numeral__extra_I3_J)).
% 18.74/5.36 thf(632,plain,((~ (ord_less_poly_real @ zero_zero_poly_real @ zero_zero_poly_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 18.74/5.36 thf(41,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_176_less__not__refl2)).
% 18.74/5.36 thf(418,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 18.74/5.36 thf(265,axiom,((! [A:real]: ~ (ord_less_real @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_288_less__irrefl)).
% 18.74/5.36 thf(1341,plain,((! [A:real]: ~ (ord_less_real @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[265])).
% 18.74/5.36 thf(152,axiom,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less_eq_nat @ D @ E) => (A @ D @ E))) => ((! [D:nat,E:nat]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_linorder__wlog)).
% 18.74/5.36 thf(896,plain,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less_eq_nat @ D @ E) => (A @ D @ E))) => ((! [D:nat,E:nat]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 18.74/5.36 thf(3,axiom,((! [A:poly_poly_real]: ((! [B:poly_real]: ((poly_poly_real2 @ A @ B) = zero_zero_poly_real)) = (A = zero_z1423781445y_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_poly__all__0__iff__0)).
% 18.74/5.36 thf(290,plain,((! [A:poly_poly_real]: ((! [B:poly_real]: ((poly_poly_real2 @ A @ B) = zero_zero_poly_real)) = (A = zero_z1423781445y_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 18.74/5.36 thf(44,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_272_neqE)).
% 18.74/5.36 thf(433,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)],[44])).
% 18.74/5.36 thf(110,axiom,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_eq_nat @ A @ (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_251_order__subst1)).
% 18.74/5.36 thf(667,plain,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_eq_nat @ A @ (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 18.74/5.36 thf(162,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ A) => (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_200_dual__order_Oantisym)).
% 18.74/5.36 thf(929,plain,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ A) => (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 18.74/5.36 thf(256,axiom,((ord_less_eq_real @ zero_zero_real @ zero_zero_real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_le__numeral__extra_I3_J)).
% 18.74/5.36 thf(1308,plain,((ord_less_eq_real @ zero_zero_real @ zero_zero_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[256])).
% 18.74/5.36 thf(57,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_325_dual__order_Ostrict__implies__not__eq)).
% 18.74/5.36 thf(478,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 18.74/5.36 thf(79,axiom,((! [A:nat]: ((ord_less_nat @ zero_zero_nat @ A) = (A != zero_zero_nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_zero__less__iff__neq__zero)).
% 18.74/5.36 thf(549,plain,((! [A:nat]: ((ord_less_nat @ zero_zero_nat @ A) = (~ (A = zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 18.74/5.36 thf(74,axiom,((ord_less_eq_nat @ zero_zero_nat @ zero_zero_nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_le__numeral__extra_I3_J)).
% 18.74/5.36 thf(536,plain,((ord_less_eq_nat @ zero_zero_nat @ zero_zero_nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 18.74/5.36 thf(218,axiom,((ord_less_eq_real = (^ [A:real,B:real]: ((ord_less_real @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_less__eq__real__def)).
% 18.74/5.36 thf(1161,plain,(((ord_less_eq_real) = (^ [A:real,B:real]: ((ord_less_real @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 18.74/5.36 thf(22,axiom,((ord_less_nat = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (A != B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_333_less__le)).
% 18.74/5.36 thf(346,plain,(((ord_less_nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & ~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 18.74/5.36 thf(257,axiom,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_303_less__imp__not__eq2)).
% 18.74/5.36 thf(1309,plain,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[257])).
% 18.74/5.36 thf(207,axiom,((! [A:poly_real,B:poly_real]: (((poly_real2 @ A) = (poly_real2 @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_poly__eq__poly__eq__iff)).
% 18.74/5.36 thf(1116,plain,((! [A:poly_real,B:poly_real]: (((poly_real2 @ A) = (poly_real2 @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 18.74/5.36 thf(98,axiom,((! [A:nat,B:(real > nat),C:real,D:real]: ((ord_less_nat @ A @ (B @ C)) => ((ord_less_eq_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_342_order__less__le__subst1)).
% 18.74/5.36 thf(620,plain,((! [A:nat,B:(real > nat),C:real,D:real]: ((ord_less_nat @ A @ (B @ C)) => ((ord_less_eq_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 18.74/5.36 thf(48,axiom,((! [A:real,B:real,C:real]: ((ord_min_real @ (ord_min_real @ A @ B) @ C) = (ord_min_real @ A @ (ord_min_real @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_min_Oassoc)).
% 18.74/5.36 thf(447,plain,((! [A:real,B:real,C:real]: ((ord_min_real @ (ord_min_real @ A @ B) @ C) = (ord_min_real @ A @ (ord_min_real @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 18.74/5.36 thf(37,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_174_less__irrefl__nat)).
% 18.74/5.36 thf(405,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 18.74/5.36 thf(42,axiom,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_243_ord__eq__le__subst)).
% 18.74/5.36 thf(422,plain,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 18.74/5.36 thf(145,axiom,((! [A:nat,B:nat,C:nat]: (((ord_less_eq_nat @ A @ B) => (~ (ord_less_eq_nat @ B @ C))) => (((ord_less_eq_nat @ B @ A) => (~ (ord_less_eq_nat @ A @ C))) => (((ord_less_eq_nat @ A @ C) => (~ (ord_less_eq_nat @ C @ B))) => (((ord_less_eq_nat @ C @ B) => (~ (ord_less_eq_nat @ B @ A))) => (((ord_less_eq_nat @ B @ C) => (~ (ord_less_eq_nat @ C @ A))) => (~ ((ord_less_eq_nat @ C @ A) => (~ (ord_less_eq_nat @ A @ B))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_223_le__cases3)).
% 18.74/5.36 thf(865,plain,((! [A:nat,B:nat,C:nat]: (((ord_less_eq_nat @ A @ B) => (~ (ord_less_eq_nat @ B @ C))) => (((ord_less_eq_nat @ B @ A) => (~ (ord_less_eq_nat @ A @ C))) => (((ord_less_eq_nat @ A @ C) => (~ (ord_less_eq_nat @ C @ B))) => (((ord_less_eq_nat @ C @ B) => (~ (ord_less_eq_nat @ B @ A))) => (((ord_less_eq_nat @ B @ C) => (~ (ord_less_eq_nat @ C @ A))) => (~ ((ord_less_eq_nat @ C @ A) => (~ (ord_less_eq_nat @ A @ B))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 18.74/5.36 thf(92,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_order__refl)).
% 18.74/5.36 thf(603,plain,((! [A:nat]: (ord_less_eq_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 18.74/5.36 thf(123,axiom,((! [A:real,B:real,C:(real > nat),D:nat]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_nat @ (C @ B) @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_245_order__subst2)).
% 18.74/5.36 thf(735,plain,((! [A:real,B:real,C:(real > nat),D:nat]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_nat @ (C @ B) @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 18.74/5.36 thf(39,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B) | (ord_less_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_287_less__linear)).
% 18.74/5.36 thf(410,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B) | (ord_less_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 18.74/5.36 thf(172,axiom,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => (ord_less_eq_real @ (ord_min_real @ A @ C) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_120_min_OcoboundedI1)).
% 18.74/5.36 thf(967,plain,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => (ord_less_eq_real @ (ord_min_real @ A @ C) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 18.74/5.36 thf(169,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_285_less__trans)).
% 18.74/5.36 thf(950,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 18.74/5.36 thf(201,axiom,((! [A:real,B:real,C:(real > nat),D:nat]: ((ord_less_real @ A @ B) => ((ord_less_nat @ (C @ B) @ D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_265_order__less__subst2)).
% 18.74/5.36 thf(1097,plain,((! [A:real,B:real,C:(real > nat),D:nat]: ((ord_less_real @ A @ B) => ((ord_less_nat @ (C @ B) @ D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 18.74/5.36 thf(82,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_min_real @ A @ B) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_min__absorb1)).
% 18.74/5.36 thf(564,plain,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_min_real @ A @ B) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 18.74/5.36 thf(8,axiom,((! [A:poly_poly_real,B:poly_real]: (((poly_poly_real2 @ A @ B) = zero_zero_poly_real) = ((A = zero_z1423781445y_real) | ((order_poly_real @ B @ A) != zero_zero_nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_order__root)).
% 18.74/5.36 thf(305,plain,((! [A:poly_poly_real,B:poly_real]: (((poly_poly_real2 @ A @ B) = zero_zero_poly_real) = ((A = zero_z1423781445y_real) | ~ ((order_poly_real @ B @ A) = zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 18.74/5.36 thf(20,axiom,((! [A:nat,B:nat,C:$o]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ A) => (C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_306_less__imp__triv)).
% 18.74/5.36 thf(341,plain,((! [A:nat,B:nat,C:$o]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ A) => (C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 18.74/5.36 thf(263,axiom,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_296_less__imp__not__eq)).
% 18.74/5.36 thf(1335,plain,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[263])).
% 18.74/5.36 thf(250,axiom,((~ (ord_less_real @ zero_zero_real @ zero_zero_real))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_less__numeral__extra_I3_J)).
% 18.74/5.36 thf(1288,plain,((~ (ord_less_real @ zero_zero_real @ zero_zero_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 18.74/5.36 thf(220,axiom,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (~ (ord_less_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_275_order_Oasym)).
% 18.74/5.36 thf(1165,plain,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (~ (ord_less_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 18.74/5.36 thf(131,axiom,((((=) @ real) = (^ [A:real,B:real]: ((ord_less_eq_real @ A @ B) & (ord_less_eq_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_234_eq__iff)).
% 18.74/5.36 thf(796,plain,((((=) @ real) = (^ [A:real,B:real]: ((ord_less_eq_real @ A @ B) & (ord_less_eq_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 18.74/5.36 thf(148,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_227_le__cases)).
% 18.74/5.36 thf(886,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)],[148])).
% 18.74/5.36 thf(34,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ A) => (ord_less_eq_nat @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_205_dual__order_Otrans)).
% 18.74/5.36 thf(395,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ A) => (ord_less_eq_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 18.74/5.36 thf(124,axiom,((! [A:real,B:real,C:real]: (((ord_less_eq_real @ A @ B) => (~ (ord_less_eq_real @ B @ C))) => (((ord_less_eq_real @ B @ A) => (~ (ord_less_eq_real @ A @ C))) => (((ord_less_eq_real @ A @ C) => (~ (ord_less_eq_real @ C @ B))) => (((ord_less_eq_real @ C @ B) => (~ (ord_less_eq_real @ B @ A))) => (((ord_less_eq_real @ B @ C) => (~ (ord_less_eq_real @ C @ A))) => (~ ((ord_less_eq_real @ C @ A) => (~ (ord_less_eq_real @ A @ B))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_222_le__cases3)).
% 18.74/5.36 thf(740,plain,((! [A:real,B:real,C:real]: (((ord_less_eq_real @ A @ B) => (~ (ord_less_eq_real @ B @ C))) => (((ord_less_eq_real @ B @ A) => (~ (ord_less_eq_real @ A @ C))) => (((ord_less_eq_real @ A @ C) => (~ (ord_less_eq_real @ C @ B))) => (((ord_less_eq_real @ C @ B) => (~ (ord_less_eq_real @ B @ A))) => (((ord_less_eq_real @ B @ C) => (~ (ord_less_eq_real @ C @ A))) => (~ ((ord_less_eq_real @ C @ A) => (~ (ord_less_eq_real @ A @ B))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 18.74/5.36 thf(16,axiom,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_order__class_Oorder_Oeq__iff)).
% 18.74/5.36 thf(332,plain,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 18.74/5.36 thf(105,axiom,((! [A:nat]: ((~ (ord_less_nat @ zero_zero_nat @ A)) = (A = zero_zero_nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_not__gr__zero)).
% 18.74/5.36 thf(644,plain,((! [A:nat]: ((~ (ord_less_nat @ zero_zero_nat @ A)) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 18.74/5.36 thf(270,axiom,((! [A:real,B:(real > real),C:real,D:real]: ((ord_less_eq_real @ A @ (B @ C)) => ((ord_less_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_real @ (B @ E) @ (B @ F)))) => (ord_less_real @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_334_order__le__less__subst1)).
% 18.74/5.36 thf(1357,plain,((! [A:real,B:(real > real),C:real,D:real]: ((ord_less_eq_real @ A @ (B @ C)) => ((ord_less_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_real @ E @ F) => (ord_less_real @ (B @ E) @ (B @ F)))) => (ord_less_real @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[270])).
% 18.74/5.36 thf(176,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ C @ A) => (ord_less_nat @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_319_dual__order_Ostrict__trans)).
% 18.74/5.36 thf(982,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ C @ A) => (ord_less_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 18.74/5.36 thf(30,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((B = C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_293_ord__less__eq__trans)).
% 18.74/5.36 thf(369,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((B = C) => (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 18.74/5.36 thf(94,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_304_less__imp__not__eq2)).
% 18.74/5.36 thf(607,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 18.74/5.36 thf(133,axiom,((! [A:real,B:(real > real),C:real,D:real]: ((ord_less_eq_real @ A @ (B @ C)) => ((ord_less_eq_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_real @ (B @ E) @ (B @ F)))) => (ord_less_eq_real @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_248_order__subst1)).
% 18.74/5.36 thf(803,plain,((! [A:real,B:(real > real),C:real,D:real]: ((ord_less_eq_real @ A @ (B @ C)) => ((ord_less_eq_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_real @ (B @ E) @ (B @ F)))) => (ord_less_eq_real @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 18.74/5.36 thf(25,axiom,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) = (A = zero_zero_nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_le__0__eq)).
% 18.74/5.36 thf(354,plain,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 18.74/5.36 thf(164,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_297_less__imp__not__eq)).
% 18.74/5.36 thf(935,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 18.74/5.36 thf(125,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ zero_zero_nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_183_not__less0)).
% 18.74/5.36 thf(755,plain,((! [A:nat]: ~ (ord_less_nat @ A @ zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 18.74/5.36 thf(283,axiom,((! [A:real,B:real]: ((~ (ord_less_real @ A @ B)) => (ord_less_eq_real @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_328_leI)).
% 18.74/5.36 thf(1417,plain,((! [A:real,B:real]: ((~ (ord_less_real @ A @ B)) => (ord_less_eq_real @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[283])).
% 18.74/5.36 thf(1547,plain,(($false)),inference(e,[status(thm)],[1105,1237,893,468,1110,909,628,1031,408,1211,582,1290,308,1173,533,913,1354,829,1127,436,1265,1228,1254,719,504,838,344,357,542,1055,724,1313,1279,817,1379,1247,1347,770,1362,475,789,376,485,348,1183,905,1040,321,634,293,453,1119,660,507,527,678,529,793,1199,366,1067,512,942,439,1047,798,1163,334,302,862,820,561,729,916,625,522,1159,456,324,1012,285,329,1178,1296,665,1089,1270,1017,1328,499,989,857,980,403,339,537,637,970,1419,1114,985,1249,1050,911,1002,569,647,1263,997,605,1393,1318,360,311,921,765,1170,398,953,888,926,1026,1167,1135,618,1146,1301,573,296,444,1374,975,694,732,1388,579,545,413,958,1403,1139,1371,611,1058,1332,947,672,1194,1282,1349,567,318,1122,1376,1175,681,1408,880,1043,890,811,494,552,816,594,520,1325,1029,1149,1344,1293,932,1112,758,1339,685,1396,1213,883,1015,1000,299,1102,431,722,1304,1208,663,374,939,1413,473,531,944,525,640,1070,1156,1267,993,1225,1400,1053,1186,585,502,840,808,1130,1285,907,470,576,336,1257,703,613,727,1094,314,571,1240,991,465,450,363,539,482,903,1216,1189,813,517,351,390,632,418,1341,896,290,433,667,929,1308,478,549,536,1161,346,1309,1116,620,447,405,422,865,603,735,410,967,950,1097,564,305,341,1335,1288,1165,796,886,395,740,332,644,1357,982,369,607,803,354,935,755,1417])).
% 18.74/5.36 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.74/5.36 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------