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

%------------------------------------------------------------------------------
% File     : Leo-III---1.8.0
% Problem  : ITP234^1 : TPTP v9.3.1. Bugfixed v9.2.1.
% Transfm  : none
% Format   : tptp:raw
% Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox2/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:20 AM UTC 2026

% Result   : Theorem 20.02s 5.43s
% Output   : Refutation 20.45s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ITP234^1 : TPTP v9.3.1. Bugfixed v9.2.1.
% 0.00/0.08  % Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.10/0.20  % Computer : n007.cluster.edu
% 0.10/0.20  % Model    : x86_64 x86_64
% 0.10/0.20  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20  % Memory   : 8046.5625MB
% 0.10/0.20  % OS       : Linux 6.8.0-71-generic
% 0.10/0.21  % CPULimit : 300
% 0.10/0.21  % WCLimit  : 300
% 0.10/0.21  % DateTime : Tue Sep 29 20:23:26 UTC 2026
% 0.10/0.21  % CPUTime  : 
% 0.10/0.21  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.65/0.51  % [INFO] 	 Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ... 
% 4.99/1.59  % [INFO] 	 Parsing done (1076ms). 
% 5.44/1.61  % [INFO] 	 Running in sequential loop mode. 
% 6.45/1.97  % [INFO] 	 eprover registered as external prover. 
% 6.45/1.98  % [INFO] 	 Scanning for conjecture ... 
% 8.14/2.47  % [INFO] 	 Found a conjecture (or negated_conjecture) and 8149 axioms. Running axiom selection ... 
% 9.32/2.78  % [INFO] 	 Axiom selection finished. Selected 152 axioms (removed 7997 axioms). 
% 9.93/2.95  % [INFO] 	 Problem is higher-order (TPTP THF). 
% 9.93/2.97  % [INFO] 	 Type checking passed. 
% 9.93/2.98  % [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 ... 
% 20.02/5.42  % External prover 'e' found a proof!
% 20.02/5.42  % [INFO] 	 Killing All external provers ... 
% 20.02/5.42  % Time passed: 5125ms (effective reasoning time: 3808ms)
% 20.02/5.42  % 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)>
% 20.02/5.43  % Axioms used in derivation (152): fact_469_ord__less__eq__subst, fact_1565_max_Oabsorb3, fact_940_add__right__imp__eq, fact_33__C163_C, fact_479_ord__eq__less__subst, fact_292_nth__mem, fact_173_trans__less__add1, fact_30_abcdef, fact_513_order_Ostrict__implies__not__eq, fact_176_not__add__less1, fact_174_add__less__mono1, fact_465_order__less__irrefl, fact_262_nth__equalityI, fact_445_order__less__subst2, fact_583_nat__less__induct, fact_517_dual__order_Ostrict__trans, fact_1019_add__less__imp__less__left, fact_1507_max__add__distrib__right, fact_535_dual__order_Oirrefl, fact_586_less__not__refl2, fact_1819_replicate__length__same, fact_2_bit__split__inv, fact_933_add_Oleft__commute, fact_1512_minf_I7_J, fact_1573_max__less__iff__conj, fact_587_less__not__refl, fact_892_add__less__cancel__left, fact_3_tc, fact_1707_length__replicate, fact_172_trans__less__add2, fact_561_order_Oasym, fact_437_order__less__imp__triv, fact_7_list__update__id, fact_1413_verit__comp__simplify1_I1_J, fact_1468_mi__eq__ma__no__ch, fact_1540_pinf_I5_J, fact_1628_max_Ostrict__coboundedI2, fact_175_not__add__less2, fact_15_nsprop, fact_565_less__imp__neq, fact_271_all__set__conv__all__nth, fact_27_both__member__options__equiv__member, fact_1006_add__mono__thms__linordered__field_I1_J, fact_283_in__set__conv__nth, fact_585_less__not__refl3, fact_1569_max_Oabsorb4, fact_489_order__less__trans, fact_1022_add__less__imp__less__right, fact_1640_max_Ostrict__boundedE, fact_575_nth__list__update, fact_1465__C10_C, fact_94_nat__add__left__cancel__less, fact_582_infinite__descent, fact_1000_add__mono__thms__linordered__field_I5_J, fact_120_Ex__list__of__length, fact_18_list__update__swap, fact_1632_max_Ostrict__coboundedI1, fact_509_dual__order_Ostrict__implies__not__eq, fact_108_set__swap, fact_425_order__less__imp__not__eq2, fact_421_order__less__imp__not__less, fact_1510_nat__add__max__right, fact_533_exists__least__iff, fact_24_not__min__Null__member, fact_256_list__eq__iff__nth__eq, fact_21_in__children__def, fact_1509_nat__add__max__left, fact_17_False, fact_501_order__less__asym, fact_1524_minf_I3_J, fact_1636_max_Ostrict__order__iff, fact_937_add__left__imp__eq, fact_1556_pinf_I1_J, fact_11__C162_C, fact_570_gt__ex, fact_917_group__cancel_Oadd2, fact_1532_minf_I1_J, fact_578_list__update__same__conv, fact_847_add__right__cancel, fact_218_length__induct, fact_543_linorder__cases, fact_32__C0_C, fact_57__C3_C, fact_178_add__lessD1, fact_1548_pinf_I3_J, fact_553_ord__less__eq__trans, fact_4__C161_C, fact_1013_add__strict__left__mono, fact_905_ab__semigroup__add__class_Oadd__ac_I1_J, fact_1544_pinf_I4_J, fact_23__C12_C, fact_1016_add__strict__right__mono, fact_177_add__less__mono, fact_171_less__add__eq__less, fact_455_order__less__subst1, fact_929_add_Ocommute, fact_913_group__cancel_Oadd1, fact_844_add__left__cancel, fact_1673_intind, fact_505_linorder__neqE, fact_1504_max__add__distrib__left, fact_921_add_Oassoc, fact_28_valid__member__both__member__options, fact_1520_minf_I4_J, fact_529_linorder__less__wlog, fact_539_dual__order_Oasym, fact_557_ord__eq__less__trans, fact_433_linorder__less__linear, fact_128_size__neq__size__imp__neq, fact_551_less__induct, fact_29__C5_C, fact_1466_deg__deg__n, fact_1009_add__strict__mono, fact_14_list__update__overwrite, fact_1552_pinf_I2_J, fact_497_linorder__neq__iff, fact_547_antisym__conv3, fact_1_insprop, fact_895_add__less__cancel__right, fact_105_nth__list__update__eq, fact_581_linorder__neqE__nat, fact_1588_VEBT__internal_OminNull_Osimps_I5_J, fact_1816_replicate__eqI, fact_1536_pinf_I7_J, fact_16__C11_C, fact_1516_minf_I5_J, fact_429_order__less__imp__not__eq, fact_1528_minf_I2_J, fact_25_min__Null__member, fact_0_True, fact_525_order_Ostrict__trans, fact_1744_nth__replicate, fact_123_neq__if__length__neq, fact_286_list__ball__nth, fact_909_add__mono__thms__linordered__semiring_I4_J, fact_588_nat__neq__iff, fact_34_mimaxrel, fact_259_Skolem__list__nth, fact_10_nth__list__update__neq, fact_441_order__less__not__sym, fact_277_all__nth__imp__all__set, fact_584_less__irrefl__nat, fact_1644_less__max__iff__disj, fact_268_set__update__subsetI, fact_26__C1_C, fact_96_length__list__update, fact_1003_add__mono__thms__linordered__field_I2_J, fact_418_set__update__memI, fact_224_subset__code_I1_J, fact_493_order__less__asym_H, fact_521_not__less__iff__gr__or__eq, fact_53_inthall
% 20.02/5.43  % No. of inferences in proof: 308
% 20.02/5.43  % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 5125 ms resp. 3808 ms w/o parsing
% 20.45/5.59  % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.45/5.59  thf(set_Pr1542805901266377927at_nat_type, type, set_Pr1542805901266377927at_nat: $tType).
% 20.45/5.59  thf(produc4471711990508489141at_nat_type, type, produc4471711990508489141at_nat: $tType).
% 20.45/5.59  thf(produc6392793444374437607at_nat_type, type, produc6392793444374437607at_nat: $tType).
% 20.45/5.59  thf(list_P8469869581646625389at_nat_type, type, list_P8469869581646625389at_nat: $tType).
% 20.45/5.59  thf(set_Pr8693737435421807431at_nat_type, type, set_Pr8693737435421807431at_nat: $tType).
% 20.45/5.59  thf(set_Pr1916528119006554503T_VEBT_type, type, set_Pr1916528119006554503T_VEBT: $tType).
% 20.45/5.59  thf(produc859450856879609959at_nat_type, type, produc859450856879609959at_nat: $tType).
% 20.45/5.59  thf(produc9211091688327510695T_VEBT_type, type, produc9211091688327510695T_VEBT: $tType).
% 20.45/5.59  thf(set_Pr3451248702717554689st_nat_type, type, set_Pr3451248702717554689st_nat: $tType).
% 20.45/5.59  thf(set_Pr765067013931698361st_int_type, type, set_Pr765067013931698361st_int: $tType).
% 20.45/5.59  thf(list_P7413028617227757229T_VEBT_type, type, list_P7413028617227757229T_VEBT: $tType).
% 20.45/5.59  thf(set_Pr6192946355708809607T_VEBT_type, type, set_Pr6192946355708809607T_VEBT: $tType).
% 20.45/5.59  thf(produc7248412053542808358at_nat_type, type, produc7248412053542808358at_nat: $tType).
% 20.45/5.59  thf(produc1828647624359046049st_nat_type, type, produc1828647624359046049st_nat: $tType).
% 20.45/5.59  thf(produc1186641810826059865st_int_type, type, produc1186641810826059865st_int: $tType).
% 20.45/5.59  thf(list_P7037539587688870467BT_nat_type, type, list_P7037539587688870467BT_nat: $tType).
% 20.45/5.59  thf(list_P4547456442757143711BT_int_type, type, list_P4547456442757143711BT_int: $tType).
% 20.45/5.59  thf(list_P5647936690300460905T_VEBT_type, type, list_P5647936690300460905T_VEBT: $tType).
% 20.45/5.59  thf(list_P7524865323317820941T_VEBT_type, type, list_P7524865323317820941T_VEBT: $tType).
% 20.45/5.59  thf(produc8243902056947475879T_VEBT_type, type, produc8243902056947475879T_VEBT: $tType).
% 20.45/5.59  thf(set_Pr7556676689462069481BT_nat_type, type, set_Pr7556676689462069481BT_nat: $tType).
% 20.45/5.59  thf(option4927543243414619207at_nat_type, type, option4927543243414619207at_nat: $tType).
% 20.45/5.59  thf(filter1242075044329608583at_nat_type, type, filter1242075044329608583at_nat: $tType).
% 20.45/5.59  thf(list_P6011104703257516679at_nat_type, type, list_P6011104703257516679at_nat: $tType).
% 20.45/5.59  thf(list_P3521021558325789923at_int_type, type, list_P3521021558325789923at_int: $tType).
% 20.45/5.59  thf(list_P8198026277950538467nt_nat_type, type, list_P8198026277950538467nt_nat: $tType).
% 20.45/5.59  thf(list_P5707943133018811711nt_int_type, type, list_P5707943133018811711nt_int: $tType).
% 20.45/5.59  thf(produc9072475918466114483BT_nat_type, type, produc9072475918466114483BT_nat: $tType).
% 20.45/5.59  thf(produc4894624898956917775BT_int_type, type, produc4894624898956917775BT_int: $tType).
% 20.45/5.59  thf(produc8025551001238799321T_VEBT_type, type, produc8025551001238799321T_VEBT: $tType).
% 20.45/5.59  thf(produc1531783533982839933T_VEBT_type, type, produc1531783533982839933T_VEBT: $tType).
% 20.45/5.59  thf(set_Pr1261947904930325089at_nat_type, type, set_Pr1261947904930325089at_nat: $tType).
% 20.45/5.59  thf(set_Pr958786334691620121nt_int_type, type, set_Pr958786334691620121nt_int: $tType).
% 20.45/5.59  thf(set_list_VEBT_VEBT_type, type, set_list_VEBT_VEBT: $tType).
% 20.45/5.59  thf(set_li5464603477888414924d_enat_type, type, set_li5464603477888414924d_enat: $tType).
% 20.45/5.59  thf(set_se7270636423289371942d_enat_type, type, set_se7270636423289371942d_enat: $tType).
% 20.45/5.59  thf(product_prod_nat_nat_type, type, product_prod_nat_nat: $tType).
% 20.45/5.59  thf(product_prod_nat_int_type, type, product_prod_nat_int: $tType).
% 20.45/5.59  thf(product_prod_int_nat_type, type, product_prod_int_nat: $tType).
% 20.45/5.59  thf(product_prod_int_int_type, type, product_prod_int_int: $tType).
% 20.45/5.59  thf(set_list_complex_type, type, set_list_complex: $tType).
% 20.45/5.59  thf(set_set_complex_type, type, set_set_complex: $tType).
% 20.45/5.59  thf(option_VEBT_VEBT_type, type, option_VEBT_VEBT: $tType).
% 20.45/5.59  thf(option_set_nat_type, type, option_set_nat: $tType).
% 20.45/5.59  thf(option_Extended_enat_type, type, option_Extended_enat: $tType).
% 20.45/5.59  thf(list_VEBT_VEBT_type, type, list_VEBT_VEBT: $tType).
% 20.45/5.59  thf(set_list_nat_type, type, set_list_nat: $tType).
% 20.45/5.59  thf(set_list_int_type, type, set_list_int: $tType).
% 20.45/5.59  thf(list_set_nat_type, type, list_set_nat: $tType).
% 20.45/5.59  thf(set_VEBT_VEBT_type, type, set_VEBT_VEBT: $tType).
% 20.45/5.59  thf(set_set_nat_type, type, set_set_nat: $tType).
% 20.45/5.59  thf(set_set_int_type, type, set_set_int: $tType).
% 20.45/5.59  thf(list_Extended_enat_type, type, list_Extended_enat: $tType).
% 20.45/5.59  thf(set_Product_unit_type, type, set_Product_unit: $tType).
% 20.45/5.59  thf(set_Extended_enat_type, type, set_Extended_enat: $tType).
% 20.45/5.59  thf(list_complex_type, type, list_complex: $tType).
% 20.45/5.59  thf(set_complex_type, type, set_complex: $tType).
% 20.45/5.59  thf(option_real_type, type, option_real: $tType).
% 20.45/5.59  thf(filter_real_type, type, filter_real: $tType).
% 20.45/5.59  thf(option_num_type, type, option_num: $tType).
% 20.45/5.59  thf(option_nat_type, type, option_nat: $tType).
% 20.45/5.59  thf(option_int_type, type, option_int: $tType).
% 20.45/5.59  thf(filter_nat_type, type, filter_nat: $tType).
% 20.45/5.59  thf(set_char_type, type, set_char: $tType).
% 20.45/5.59  thf(list_real_type, type, list_real: $tType).
% 20.45/5.59  thf(set_real_type, type, set_real: $tType).
% 20.45/5.59  thf(list_num_type, type, list_num: $tType).
% 20.45/5.59  thf(list_nat_type, type, list_nat: $tType).
% 20.45/5.59  thf(list_int_type, type, list_int: $tType).
% 20.45/5.59  thf(vEBT_VEBT_type, type, vEBT_VEBT: $tType).
% 20.45/5.59  thf(set_num_type, type, set_num: $tType).
% 20.45/5.59  thf(set_nat_type, type, set_nat: $tType).
% 20.45/5.59  thf(set_int_type, type, set_int: $tType).
% 20.45/5.59  thf(extended_enat_type, type, extended_enat: $tType).
% 20.45/5.59  thf(complex_type, type, complex: $tType).
% 20.45/5.59  thf(char_type, type, char: $tType).
% 20.45/5.59  thf(real_type, type, real: $tType).
% 20.45/5.59  thf(num_type, type, num: $tType).
% 20.45/5.59  thf(nat_type, type, nat: $tType).
% 20.45/5.59  thf(int_type, type, int: $tType).
% 20.45/5.59  thf(plus_plus_nat_decl, type, plus_plus_nat: (nat > (nat > nat))).
% 20.45/5.59  thf(if_VEBT_VEBT_decl, type, if_VEBT_VEBT: ($o > (vEBT_VEBT > (vEBT_VEBT > vEBT_VEBT)))).
% 20.45/5.59  thf(set_VEBT_VEBT2_decl, type, set_VEBT_VEBT2: (list_VEBT_VEBT > set_VEBT_VEBT)).
% 20.45/5.59  thf(list_u1324408373059187874T_VEBT_decl, type, list_u1324408373059187874T_VEBT: (list_VEBT_VEBT > (nat > (vEBT_VEBT > list_VEBT_VEBT)))).
% 20.45/5.59  thf(nth_VEBT_VEBT_decl, type, nth_VEBT_VEBT: (list_VEBT_VEBT > (nat > vEBT_VEBT))).
% 20.45/5.59  thf(replicate_VEBT_VEBT_decl, type, replicate_VEBT_VEBT: (nat > (vEBT_VEBT > list_VEBT_VEBT))).
% 20.45/5.59  thf(size_s6755466524823107622T_VEBT_decl, type, size_s6755466524823107622T_VEBT: (list_VEBT_VEBT > nat)).
% 20.45/5.59  thf(some_P7363390416028606310at_nat_decl, type, some_P7363390416028606310at_nat: (product_prod_nat_nat > option4927543243414619207at_nat)).
% 20.45/5.59  thf(ord_less_nat_decl, type, ord_less_nat: (nat > (nat > $o))).
% 20.45/5.59  thf(ord_le4337996190870823476T_VEBT_decl, type, ord_le4337996190870823476T_VEBT: (set_VEBT_VEBT > (set_VEBT_VEBT > $o))).
% 20.45/5.59  thf(ord_max_nat_decl, type, ord_max_nat: (nat > (nat > nat))).
% 20.45/5.59  thf(product_Pair_nat_nat_decl, type, product_Pair_nat_nat: (nat > (nat > product_prod_nat_nat))).
% 20.45/5.59  thf(vEBT_Node_decl, type, vEBT_Node: (option4927543243414619207at_nat > (nat > (list_VEBT_VEBT > (vEBT_VEBT > vEBT_VEBT))))).
% 20.45/5.59  thf(vEBT_V8194947554948674370ptions_decl, type, vEBT_V8194947554948674370ptions: (vEBT_VEBT > (nat > $o))).
% 20.45/5.59  thf(vEBT_VEBT_high_decl, type, vEBT_VEBT_high: (nat > (nat > nat))).
% 20.45/5.59  thf(vEBT_V5917875025757280293ildren_decl, type, vEBT_V5917875025757280293ildren: (nat > (list_VEBT_VEBT > (nat > $o)))).
% 20.45/5.59  thf(vEBT_VEBT_low_decl, type, vEBT_VEBT_low: (nat > (nat > nat))).
% 20.45/5.59  thf(vEBT_invar_vebt_decl, type, vEBT_invar_vebt: (vEBT_VEBT > (nat > $o))).
% 20.45/5.59  thf(vEBT_vebt_insert_decl, type, vEBT_vebt_insert: (vEBT_VEBT > (nat > vEBT_VEBT))).
% 20.45/5.59  thf(vEBT_VEBT_bit_concat_decl, type, vEBT_VEBT_bit_concat: (nat > (nat > (nat > nat)))).
% 20.45/5.59  thf(vEBT_VEBT_minNull_decl, type, vEBT_VEBT_minNull: (vEBT_VEBT > $o)).
% 20.45/5.59  thf(vEBT_vebt_member_decl, type, vEBT_vebt_member: (vEBT_VEBT > (nat > $o))).
% 20.45/5.59  thf(member_VEBT_VEBT_decl, type, member_VEBT_VEBT: (vEBT_VEBT > (set_VEBT_VEBT > $o))).
% 20.45/5.59  thf(deg_decl, type, deg: nat).
% 20.45/5.59  thf(i_decl, type, i: nat).
% 20.45/5.59  thf(m_decl, type, m: nat).
% 20.45/5.59  thf(ma_decl, type, ma: nat).
% 20.45/5.59  thf(mi_decl, type, mi: nat).
% 20.45/5.59  thf(na_decl, type, na: nat).
% 20.45/5.59  thf(summary_decl, type, summary: vEBT_VEBT).
% 20.45/5.59  thf(treeList_decl, type, treeList: list_VEBT_VEBT).
% 20.45/5.59  thf(xa_decl, type, xa: nat).
% 20.45/5.59  thf(117,axiom,((! [A:list_VEBT_VEBT,B:(vEBT_VEBT > $o),C:vEBT_VEBT]: ((! [D:nat]: ((ord_less_nat @ D @ (size_s6755466524823107622T_VEBT @ A)) => (B @ (nth_VEBT_VEBT @ A @ D)))) => ((member_VEBT_VEBT @ C @ (set_VEBT_VEBT2 @ A)) => (B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_277_all__nth__imp__all__set)).
% 20.45/5.59  thf(606,plain,((! [A:list_VEBT_VEBT,B:(vEBT_VEBT > $o),C:vEBT_VEBT]: ((! [D:nat]: ((ord_less_nat @ D @ (size_s6755466524823107622T_VEBT @ A)) => (B @ (nth_VEBT_VEBT @ A @ D)))) => ((member_VEBT_VEBT @ C @ (set_VEBT_VEBT2 @ A)) => (B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 20.45/5.59  thf(23,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_586_less__not__refl2)).
% 20.45/5.59  thf(237,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 20.45/5.59  thf(73,axiom,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ (plus_plus_nat @ A @ B) @ C) = (plus_plus_nat @ A @ (plus_plus_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_905_ab__semigroup__add__class_Oadd__ac_I1_J)).
% 20.45/5.59  thf(444,plain,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ (plus_plus_nat @ A @ B) @ C) = (plus_plus_nat @ A @ (plus_plus_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 20.45/5.59  thf(122,axiom,((! [A:vEBT_VEBT,B:list_VEBT_VEBT]: ((member_VEBT_VEBT @ A @ (set_VEBT_VEBT2 @ B)) = (? [C:nat]: ((ord_less_nat @ C @ (size_s6755466524823107622T_VEBT @ B)) & ((nth_VEBT_VEBT @ B @ C) = A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_283_in__set__conv__nth)).
% 20.45/5.59  thf(629,plain,((! [A:vEBT_VEBT,B:list_VEBT_VEBT]: ((member_VEBT_VEBT @ A @ (set_VEBT_VEBT2 @ B)) = (? [C:nat]: ((ord_less_nat @ C @ (size_s6755466524823107622T_VEBT @ B)) & ((nth_VEBT_VEBT @ B @ C) = A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 20.45/5.59  thf(49,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ A @ (ord_max_nat @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1628_max_Ostrict__coboundedI2)).
% 20.45/5.59  thf(347,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ A @ (ord_max_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 20.45/5.59  thf(80,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ (ord_max_nat @ B @ C)) = ((ord_less_nat @ A @ B) | (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1644_less__max__iff__disj)).
% 20.45/5.59  thf(468,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ (ord_max_nat @ B @ C)) = ((ord_less_nat @ A @ B) | (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 20.45/5.59  thf(22,axiom,((! [A:nat,B:nat,C:nat]: (((plus_plus_nat @ A @ B) = (plus_plus_nat @ A @ C)) = (B = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_844_add__left__cancel)).
% 20.45/5.59  thf(234,plain,((! [A:nat,B:nat,C:nat]: (((plus_plus_nat @ A @ B) = (plus_plus_nat @ A @ C)) = (B = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 20.45/5.59  thf(131,axiom,((! [A:list_VEBT_VEBT,B:(vEBT_VEBT > $o),C:nat]: ((! [D:vEBT_VEBT]: ((member_VEBT_VEBT @ D @ (set_VEBT_VEBT2 @ A)) => (B @ D))) => ((ord_less_nat @ C @ (size_s6755466524823107622T_VEBT @ A)) => (B @ (nth_VEBT_VEBT @ A @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_53_inthall)).
% 20.45/5.59  thf(666,plain,((! [A:list_VEBT_VEBT,B:(vEBT_VEBT > $o),C:nat]: ((! [D:vEBT_VEBT]: ((member_VEBT_VEBT @ D @ (set_VEBT_VEBT2 @ A)) => (B @ D))) => ((ord_less_nat @ C @ (size_s6755466524823107622T_VEBT @ A)) => (B @ (nth_VEBT_VEBT @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 20.45/5.59  thf(65,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B) | (ord_less_nat @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_433_linorder__less__linear)).
% 20.45/5.59  thf(408,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)],[65])).
% 20.45/5.59  thf(18,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/sandbox2/benchmark/theBenchmark.p',fact_479_ord__eq__less__subst)).
% 20.45/5.59  thf(217,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)],[18])).
% 20.45/5.59  thf(75,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((A != B) => (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_543_linorder__cases)).
% 20.45/5.59  thf(449,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)],[75])).
% 20.45/5.59  thf(27,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (ord_max_nat @ A @ B) @ C) => (~ ((ord_less_nat @ A @ C) => (~ (ord_less_nat @ B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1640_max_Ostrict__boundedE)).
% 20.45/5.59  thf(247,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (ord_max_nat @ A @ B) @ C) => (~ ((ord_less_nat @ A @ C) => (~ (ord_less_nat @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 20.45/5.59  thf(94,axiom,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((! [D:nat]: ((ord_less_nat @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_551_less__induct)).
% 20.45/5.59  thf(523,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)],[94])).
% 20.45/5.59  thf(109,axiom,((! [A:list_VEBT_VEBT,B:set_VEBT_VEBT]: ((ord_le4337996190870823476T_VEBT @ (set_VEBT_VEBT2 @ A) @ B) = (! [C:vEBT_VEBT]: ((member_VEBT_VEBT @ C @ (set_VEBT_VEBT2 @ A)) => (member_VEBT_VEBT @ C @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_224_subset__code_I1_J)).
% 20.45/5.59  thf(582,plain,((! [A:list_VEBT_VEBT,B:set_VEBT_VEBT]: ((ord_le4337996190870823476T_VEBT @ (set_VEBT_VEBT2 @ A) @ B) = (! [C:vEBT_VEBT]: ((member_VEBT_VEBT @ C @ (set_VEBT_VEBT2 @ A)) => (member_VEBT_VEBT @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 20.45/5.59  thf(58,axiom,((! [A:nat,B:nat,C:nat,D:nat]: (((A = B) & (ord_less_nat @ C @ D)) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1003_add__mono__thms__linordered__field_I2_J)).
% 20.45/5.59  thf(385,plain,((! [A:nat,B:nat,C:nat,D:nat]: (((A = B) & (ord_less_nat @ C @ D)) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 20.45/5.59  thf(102,axiom,((! [A:nat,B:list_VEBT_VEBT,C:vEBT_VEBT]: ((ord_less_nat @ A @ (size_s6755466524823107622T_VEBT @ B)) => (((list_u1324408373059187874T_VEBT @ B @ A @ C) = B) = ((nth_VEBT_VEBT @ B @ A) = C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_578_list__update__same__conv)).
% 20.45/5.59  thf(550,plain,((! [A:nat,B:list_VEBT_VEBT,C:vEBT_VEBT]: ((ord_less_nat @ A @ (size_s6755466524823107622T_VEBT @ B)) => (((list_u1324408373059187874T_VEBT @ B @ A @ C) = B) = ((nth_VEBT_VEBT @ B @ A) = C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 20.45/5.59  thf(64,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (C != A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1524_minf_I3_J)).
% 20.45/5.59  thf(404,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (C = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 20.45/5.59  thf(70,axiom,((! [A:nat,B:nat,C:nat,D:nat]: (((ord_less_nat @ A @ B) & (ord_less_nat @ C @ D)) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1000_add__mono__thms__linordered__field_I5_J)).
% 20.45/5.59  thf(436,plain,((! [A:nat,B:nat,C:nat,D:nat]: (((ord_less_nat @ A @ B) & (ord_less_nat @ C @ D)) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 20.45/5.59  thf(127,axiom,((! [A:nat,B:nat,C:nat,D:list_VEBT_VEBT,E:vEBT_VEBT]: ((vEBT_invar_vebt @ (vEBT_Node @ (some_P7363390416028606310at_nat @ (product_Pair_nat_nat @ A @ B)) @ C @ D @ E) @ C) => ((A = B) => (! [F:vEBT_VEBT]: ((member_VEBT_VEBT @ F @ (set_VEBT_VEBT2 @ D)) => (~ (? [G:nat]: (vEBT_V8194947554948674370ptions @ F @ G)))) & ~ (? [F:nat]: (vEBT_V8194947554948674370ptions @ E @ F))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1468_mi__eq__ma__no__ch)).
% 20.45/5.59  thf(651,plain,((! [A:nat,B:nat,C:nat,D:list_VEBT_VEBT,E:vEBT_VEBT]: ((vEBT_invar_vebt @ (vEBT_Node @ (some_P7363390416028606310at_nat @ (product_Pair_nat_nat @ A @ B)) @ C @ D @ E) @ C) => ((A = B) => (! [F:vEBT_VEBT]: ((member_VEBT_VEBT @ F @ (set_VEBT_VEBT2 @ D)) => (~ (? [G:nat]: (vEBT_V8194947554948674370ptions @ F @ G)))) & ~ (? [F:nat]: (vEBT_V8194947554948674370ptions @ E @ F))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 20.45/5.59  thf(59,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/sandbox2/benchmark/theBenchmark.p',fact_455_order__less__subst1)).
% 20.45/5.59  thf(389,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)],[59])).
% 20.45/5.59  thf(148,axiom,((vEBT_invar_vebt @ (if_VEBT_VEBT @ (vEBT_VEBT_minNull @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na))) @ (vEBT_vebt_insert @ summary @ (vEBT_VEBT_high @ mi @ na)) @ summary) @ m)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_23__C12_C)).
% 20.45/5.59  thf(724,plain,((vEBT_invar_vebt @ (if_VEBT_VEBT @ (vEBT_VEBT_minNull @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na))) @ (vEBT_vebt_insert @ summary @ (vEBT_VEBT_high @ mi @ na)) @ summary) @ m)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 20.45/5.59  thf(106,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_nat @ A @ B) => (((plus_plus_nat @ C @ B) = (plus_plus_nat @ A @ D)) => (ord_less_nat @ C @ D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_171_less__add__eq__less)).
% 20.45/5.59  thf(570,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_nat @ A @ B) => (((plus_plus_nat @ C @ B) = (plus_plus_nat @ A @ D)) => (ord_less_nat @ C @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 20.45/5.59  thf(146,axiom,((i = (vEBT_VEBT_high @ mi @ na))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_True)).
% 20.45/5.59  thf(719,plain,((i = (vEBT_VEBT_high @ mi @ na))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 20.45/5.59  thf(48,axiom,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ A @ (ord_max_nat @ B @ C)) = (ord_max_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1510_nat__add__max__right)).
% 20.45/5.59  thf(344,plain,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ A @ (ord_max_nat @ B @ C)) = (ord_max_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 20.45/5.59  thf(99,axiom,((! [A:nat,B:nat]: ((A != B) = ((ord_less_nat @ A @ B) | (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_588_nat__neq__iff)).
% 20.45/5.59  thf(542,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)],[99])).
% 20.45/5.59  thf(3,axiom,((! [A:nat,B:nat,C:nat]: (((plus_plus_nat @ A @ B) = (plus_plus_nat @ A @ C)) => (B = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_937_add__left__imp__eq)).
% 20.45/5.59  thf(157,plain,((! [A:nat,B:nat,C:nat]: (((plus_plus_nat @ A @ B) = (plus_plus_nat @ A @ C)) => (B = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 20.45/5.59  thf(83,axiom,((! [A:nat,B:nat,C:nat]: (((plus_plus_nat @ A @ B) = (plus_plus_nat @ C @ B)) => (A = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_940_add__right__imp__eq)).
% 20.45/5.59  thf(485,plain,((! [A:nat,B:nat,C:nat]: (((plus_plus_nat @ A @ B) = (plus_plus_nat @ C @ B)) => (A = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 20.45/5.59  thf(107,axiom,((! [A:nat,B:nat,C:(vEBT_VEBT > $o),D:vEBT_VEBT]: ((ord_less_nat @ A @ B) => ((C @ D) => (C @ (nth_VEBT_VEBT @ (replicate_VEBT_VEBT @ B @ D) @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1673_intind)).
% 20.45/5.59  thf(574,plain,((! [A:nat,B:nat,C:(vEBT_VEBT > $o),D:vEBT_VEBT]: ((ord_less_nat @ A @ B) => ((C @ D) => (C @ (nth_VEBT_VEBT @ (replicate_VEBT_VEBT @ B @ D) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 20.45/5.59  thf(51,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((B = C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_553_ord__less__eq__trans)).
% 20.45/5.59  thf(353,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)],[51])).
% 20.45/5.59  thf(153,axiom,((! [A:list_VEBT_VEBT,B:nat,C:vEBT_VEBT,D:vEBT_VEBT]: ((list_u1324408373059187874T_VEBT @ (list_u1324408373059187874T_VEBT @ A @ B @ C) @ B @ D) = (list_u1324408373059187874T_VEBT @ A @ B @ D)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_14_list__update__overwrite)).
% 20.45/5.59  thf(734,plain,((! [A:list_VEBT_VEBT,B:nat,C:vEBT_VEBT,D:vEBT_VEBT]: ((list_u1324408373059187874T_VEBT @ (list_u1324408373059187874T_VEBT @ A @ B @ C) @ B @ D) = (list_u1324408373059187874T_VEBT @ A @ B @ D)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 20.45/5.59  thf(61,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/sandbox2/benchmark/theBenchmark.p',fact_517_dual__order_Ostrict__trans)).
% 20.45/5.59  thf(396,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)],[61])).
% 20.45/5.59  thf(66,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_501_order__less__asym)).
% 20.45/5.59  thf(411,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 20.45/5.59  thf(25,axiom,((((?) @ nat) = (^ [A:(nat > $o)]: ? [B:nat]: ((A @ B) & ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_533_exists__least__iff)).
% 20.45/5.59  thf(243,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)],[25])).
% 20.45/5.59  thf(32,axiom,((! [A:nat,B:(nat > (vEBT_VEBT > $o))]: ((! [C:nat]: ((ord_less_nat @ C @ A) => (? [D:vEBT_VEBT]: (B @ C @ D)))) = (? [C:list_VEBT_VEBT]: (((size_s6755466524823107622T_VEBT @ C) = A) & ! [D:nat]: ((ord_less_nat @ D @ A) => (B @ D @ (nth_VEBT_VEBT @ C @ D)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_259_Skolem__list__nth)).
% 20.45/5.59  thf(265,plain,((! [A:nat,B:(nat > (vEBT_VEBT > $o))]: ((! [C:nat]: ((ord_less_nat @ C @ A) => (? [D:vEBT_VEBT]: (B @ C @ D)))) = (? [C:list_VEBT_VEBT]: (((size_s6755466524823107622T_VEBT @ C) = A) & ! [D:nat]: ((ord_less_nat @ D @ A) => (B @ D @ (nth_VEBT_VEBT @ C @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 20.45/5.59  thf(90,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_174_add__less__mono1)).
% 20.45/5.59  thf(507,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 20.45/5.59  thf(44,axiom,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o),D:(nat > $o)]: ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => ((A @ F) = (B @ F)))) => ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => ((C @ F) = (D @ F)))) => (? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => (((A @ F) & (C @ F)) = ((B @ F) & (D @ F))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1556_pinf_I1_J)).
% 20.45/5.59  thf(307,plain,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o),D:(nat > $o)]: ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => ((A @ F) = (B @ F)))) => ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => ((C @ F) = (D @ F)))) => (? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => (((A @ F) & (C @ F)) = ((B @ F) & (D @ F))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 20.45/5.59  thf(38,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (ord_less_nat @ C @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1516_minf_I5_J)).
% 20.45/5.59  thf(292,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (ord_less_nat @ C @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 20.45/5.59  thf(76,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/sandbox2/benchmark/theBenchmark.p',fact_445_order__less__subst2)).
% 20.45/5.59  thf(452,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)],[76])).
% 20.45/5.59  thf(129,axiom,((! [A:list_VEBT_VEBT,B:list_VEBT_VEBT]: (((size_s6755466524823107622T_VEBT @ A) != (size_s6755466524823107622T_VEBT @ B)) => (A != B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_128_size__neq__size__imp__neq)).
% 20.45/5.59  thf(661,plain,((! [A:list_VEBT_VEBT,B:list_VEBT_VEBT]: ((~ ((size_s6755466524823107622T_VEBT @ A) = (size_s6755466524823107622T_VEBT @ B))) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 20.45/5.59  thf(42,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_421_order__less__imp__not__less)).
% 20.45/5.59  thf(302,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 20.45/5.59  thf(31,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((A = (plus_plus_nat @ B @ C)) => ((plus_plus_nat @ D @ A) = (plus_plus_nat @ B @ (plus_plus_nat @ D @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_917_group__cancel_Oadd2)).
% 20.45/5.59  thf(260,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((A = (plus_plus_nat @ B @ C)) => ((plus_plus_nat @ D @ A) = (plus_plus_nat @ B @ (plus_plus_nat @ D @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 20.45/5.59  thf(114,axiom,((~ (vEBT_V8194947554948674370ptions @ summary @ i))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_33__C163_C)).
% 20.45/5.59  thf(598,plain,((~ (vEBT_V8194947554948674370ptions @ summary @ i))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 20.45/5.59  thf(105,axiom,((! [A:(list_VEBT_VEBT > $o),B:list_VEBT_VEBT]: ((! [C:list_VEBT_VEBT]: ((! [D:list_VEBT_VEBT]: ((ord_less_nat @ (size_s6755466524823107622T_VEBT @ D) @ (size_s6755466524823107622T_VEBT @ C)) => (A @ D))) => (A @ C))) => (A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_218_length__induct)).
% 20.45/5.59  thf(561,plain,((! [A:(list_VEBT_VEBT > $o),B:list_VEBT_VEBT]: ((! [C:list_VEBT_VEBT]: ((! [D:list_VEBT_VEBT]: ((ord_less_nat @ (size_s6755466524823107622T_VEBT @ D) @ (size_s6755466524823107622T_VEBT @ C)) => (A @ D))) => (A @ C))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 20.45/5.59  thf(40,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_441_order__less__not__sym)).
% 20.45/5.59  thf(297,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 20.45/5.59  thf(68,axiom,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((! [D:nat]: ((ord_less_nat @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_583_nat__less__induct)).
% 20.45/5.59  thf(424,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)],[68])).
% 20.45/5.59  thf(35,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ C @ D) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1009_add__strict__mono)).
% 20.45/5.59  thf(275,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ C @ D) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 20.45/5.59  thf(5,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (C != A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1548_pinf_I3_J)).
% 20.45/5.59  thf(165,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (~ (C = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 20.45/5.59  thf(151,axiom,(((nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na) @ (vEBT_vebt_insert @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)) @ (vEBT_VEBT_low @ mi @ na))) @ (vEBT_VEBT_high @ mi @ na)) = (vEBT_vebt_insert @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)) @ (vEBT_VEBT_low @ mi @ na)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_insprop)).
% 20.45/5.59  thf(729,plain,(((nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na) @ (vEBT_vebt_insert @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)) @ (vEBT_VEBT_low @ mi @ na))) @ (vEBT_VEBT_high @ mi @ na)) = (vEBT_vebt_insert @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)) @ (vEBT_VEBT_low @ mi @ na)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 20.45/5.59  thf(20,axiom,((plus_plus_nat = (^ [A:nat,B:nat]: (plus_plus_nat @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_929_add_Ocommute)).
% 20.45/5.59  thf(229,plain,(((plus_plus_nat) = (^ [A:nat,B:nat]: (plus_plus_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 20.45/5.59  thf(13,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_584_less__irrefl__nat)).
% 20.45/5.59  thf(197,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 20.45/5.59  thf(53,axiom,((! [A:nat,B:nat]: ((A != B) => ((~ (ord_less_nat @ A @ B)) => (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_581_linorder__neqE__nat)).
% 20.45/5.59  thf(361,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)],[53])).
% 20.45/5.59  thf(130,axiom,((vEBT_invar_vebt @ summary @ m)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_26__C1_C)).
% 20.45/5.59  thf(665,plain,((vEBT_invar_vebt @ summary @ m)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 20.45/5.59  thf(78,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ C @ D) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_177_add__less__mono)).
% 20.45/5.59  thf(461,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ C @ D) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 20.45/5.59  thf(85,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_513_order_Ostrict__implies__not__eq)).
% 20.45/5.59  thf(493,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 20.45/5.59  thf(135,axiom,((! [A:nat]: ? [B:list_VEBT_VEBT]: ((size_s6755466524823107622T_VEBT @ B) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_120_Ex__list__of__length)).
% 20.45/5.59  thf(682,plain,((! [A:nat]: ? [B:list_VEBT_VEBT]: ((size_s6755466524823107622T_VEBT @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 20.45/5.59  thf(143,axiom,((! [A:list_VEBT_VEBT,B:nat,C:vEBT_VEBT]: ((size_s6755466524823107622T_VEBT @ (list_u1324408373059187874T_VEBT @ A @ B @ C)) = (size_s6755466524823107622T_VEBT @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_96_length__list__update)).
% 20.45/5.59  thf(710,plain,((! [A:list_VEBT_VEBT,B:nat,C:vEBT_VEBT]: ((size_s6755466524823107622T_VEBT @ (list_u1324408373059187874T_VEBT @ A @ B @ C)) = (size_s6755466524823107622T_VEBT @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 20.45/5.59  thf(138,axiom,(((mi = ma) => (! [A:vEBT_VEBT]: ((member_VEBT_VEBT @ A @ (set_VEBT_VEBT2 @ treeList)) => (~ (? [B:nat]: (vEBT_V8194947554948674370ptions @ A @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_29__C5_C)).
% 20.45/5.59  thf(697,plain,(((mi = ma) => (! [A:vEBT_VEBT]: ((member_VEBT_VEBT @ A @ (set_VEBT_VEBT2 @ treeList)) => (~ (? [B:nat]: (vEBT_V8194947554948674370ptions @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 20.45/5.59  thf(149,axiom,(((vEBT_vebt_insert @ (vEBT_Node @ (some_P7363390416028606310at_nat @ (product_Pair_nat_nat @ mi @ ma)) @ deg @ treeList @ summary) @ xa) = (vEBT_Node @ (some_P7363390416028606310at_nat @ (product_Pair_nat_nat @ xa @ (ord_max_nat @ mi @ ma))) @ deg @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na) @ (vEBT_vebt_insert @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)) @ (vEBT_VEBT_low @ mi @ na))) @ (if_VEBT_VEBT @ (vEBT_VEBT_minNull @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na))) @ (vEBT_vebt_insert @ summary @ (vEBT_VEBT_high @ mi @ na)) @ summary)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1465__C10_C)).
% 20.45/5.59  thf(725,plain,(((vEBT_vebt_insert @ (vEBT_Node @ (some_P7363390416028606310at_nat @ (product_Pair_nat_nat @ mi @ ma)) @ deg @ treeList @ summary) @ xa) = (vEBT_Node @ (some_P7363390416028606310at_nat @ (product_Pair_nat_nat @ xa @ (ord_max_nat @ mi @ ma))) @ deg @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na) @ (vEBT_vebt_insert @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)) @ (vEBT_VEBT_low @ mi @ na))) @ (if_VEBT_VEBT @ (vEBT_VEBT_minNull @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na))) @ (vEBT_vebt_insert @ summary @ (vEBT_VEBT_high @ mi @ na)) @ summary)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 20.45/5.59  thf(10,axiom,((! [A:nat,B:nat]: ((A != B) => ((~ (ord_less_nat @ A @ B)) => (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_505_linorder__neqE)).
% 20.45/5.59  thf(188,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)],[10])).
% 20.45/5.59  thf(6,axiom,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((~ (A @ C)) => (? [D:nat]: ((ord_less_nat @ D @ C) & ~ (A @ D))))) => (A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_582_infinite__descent)).
% 20.45/5.59  thf(169,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)],[6])).
% 20.45/5.59  thf(112,axiom,((! [A:list_VEBT_VEBT,B:(vEBT_VEBT > $o)]: ((! [C:vEBT_VEBT]: ((member_VEBT_VEBT @ C @ (set_VEBT_VEBT2 @ A)) => (B @ C))) = (! [C:nat]: ((ord_less_nat @ C @ (size_s6755466524823107622T_VEBT @ A)) => (B @ (nth_VEBT_VEBT @ A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_271_all__set__conv__all__nth)).
% 20.45/5.59  thf(593,plain,((! [A:list_VEBT_VEBT,B:(vEBT_VEBT > $o)]: ((! [C:vEBT_VEBT]: ((member_VEBT_VEBT @ C @ (set_VEBT_VEBT2 @ A)) => (B @ C))) = (! [C:nat]: ((ord_less_nat @ C @ (size_s6755466524823107622T_VEBT @ A)) => (B @ (nth_VEBT_VEBT @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 20.45/5.59  thf(81,axiom,((! [A:nat,B:nat,C:nat]: ((A = B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_557_ord__eq__less__trans)).
% 20.45/5.59  thf(471,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)],[81])).
% 20.45/5.59  thf(103,axiom,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ A @ (plus_plus_nat @ B @ C)) = (plus_plus_nat @ B @ (plus_plus_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_933_add_Oleft__commute)).
% 20.45/5.59  thf(554,plain,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ A @ (plus_plus_nat @ B @ C)) = (plus_plus_nat @ B @ (plus_plus_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 20.45/5.59  thf(97,axiom,((! [A:nat,B:nat]: ~ (ord_less_nat @ (plus_plus_nat @ A @ B) @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_176_not__add__less1)).
% 20.45/5.59  thf(537,plain,((! [A:nat,B:nat]: ~ (ord_less_nat @ (plus_plus_nat @ A @ B) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 20.45/5.59  thf(82,axiom,((! [A:nat,B:list_VEBT_VEBT,C:nat,D:vEBT_VEBT]: ((ord_less_nat @ A @ (size_s6755466524823107622T_VEBT @ B)) => (((A = C) => ((nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ B @ A @ D) @ C) = D)) & ((A != C) => ((nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ B @ A @ D) @ C) = (nth_VEBT_VEBT @ B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_575_nth__list__update)).
% 20.45/5.59  thf(476,plain,((! [A:nat,B:list_VEBT_VEBT,C:nat,D:vEBT_VEBT]: ((ord_less_nat @ A @ (size_s6755466524823107622T_VEBT @ B)) => (((A = C) => ((nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ B @ A @ D) @ C) = D)) & ((~ (A = C)) => ((nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ B @ A @ D) @ C) = (nth_VEBT_VEBT @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 20.45/5.59  thf(111,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ A @ (plus_plus_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_173_trans__less__add1)).
% 20.45/5.59  thf(590,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ A @ (plus_plus_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 20.45/5.59  thf(134,axiom,((! [A:product_prod_nat_nat,B:nat,C:list_VEBT_VEBT,D:vEBT_VEBT]: ~ (vEBT_VEBT_minNull @ (vEBT_Node @ (some_P7363390416028606310at_nat @ A) @ B @ C @ D)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1588_VEBT__internal_OminNull_Osimps_I5_J)).
% 20.45/5.59  thf(679,plain,((! [A:product_prod_nat_nat,B:nat,C:list_VEBT_VEBT,D:vEBT_VEBT]: ~ (vEBT_VEBT_minNull @ (vEBT_Node @ (some_P7363390416028606310at_nat @ A) @ B @ C @ D)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 20.45/5.59  thf(16,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/sandbox2/benchmark/theBenchmark.p',fact_489_order__less__trans)).
% 20.45/5.59  thf(212,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)],[16])).
% 20.45/5.59  thf(77,axiom,((! [A:nat,B:nat,C:vEBT_VEBT]: ((ord_less_nat @ A @ B) => ((nth_VEBT_VEBT @ (replicate_VEBT_VEBT @ B @ C) @ A) = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1744_nth__replicate)).
% 20.45/5.59  thf(457,plain,((! [A:nat,B:nat,C:vEBT_VEBT]: ((ord_less_nat @ A @ B) => ((nth_VEBT_VEBT @ (replicate_VEBT_VEBT @ B @ C) @ A) = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 20.45/5.59  thf(147,axiom,(((~ (vEBT_VEBT_minNull @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)))) => (summary = (vEBT_vebt_insert @ summary @ (vEBT_VEBT_high @ mi @ na))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_15_nsprop)).
% 20.45/5.59  thf(721,plain,(((~ (vEBT_VEBT_minNull @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)))) => (summary = (vEBT_vebt_insert @ summary @ (vEBT_VEBT_high @ mi @ na))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 20.45/5.59  thf(56,axiom,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o),D:(nat > $o)]: ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => ((A @ F) = (B @ F)))) => ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => ((C @ F) = (D @ F)))) => (? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => (((A @ F) & (C @ F)) = ((B @ F) & (D @ F))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1532_minf_I1_J)).
% 20.45/5.59  thf(371,plain,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o),D:(nat > $o)]: ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => ((A @ F) = (B @ F)))) => ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => ((C @ F) = (D @ F)))) => (? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => (((A @ F) & (C @ F)) = ((B @ F) & (D @ F))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 20.45/5.59  thf(11,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ A @ (ord_max_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1632_max_Ostrict__coboundedI1)).
% 20.45/5.59  thf(191,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ A @ (ord_max_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 20.45/5.59  thf(37,axiom,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o),D:(nat > $o)]: ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => ((A @ F) = (B @ F)))) => ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => ((C @ F) = (D @ F)))) => (? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => (((A @ F) | (C @ F)) = ((B @ F) | (D @ F))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1528_minf_I2_J)).
% 20.45/5.59  thf(281,plain,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o),D:(nat > $o)]: ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => ((A @ F) = (B @ F)))) => ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => ((C @ F) = (D @ F)))) => (? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => (((A @ F) | (C @ F)) = ((B @ F) | (D @ F))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 20.45/5.59  thf(100,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (ord_max_nat @ A @ B) @ C) = ((ord_less_nat @ A @ C) & (ord_less_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1573_max__less__iff__conj)).
% 20.45/5.59  thf(545,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (ord_max_nat @ A @ B) @ C) = ((ord_less_nat @ A @ C) & (ord_less_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 20.45/5.59  thf(67,axiom,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o),D:(nat > $o)]: ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => ((A @ F) = (B @ F)))) => ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => ((C @ F) = (D @ F)))) => (? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => (((A @ F) | (C @ F)) = ((B @ F) | (D @ F))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1552_pinf_I2_J)).
% 20.45/5.59  thf(413,plain,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o),D:(nat > $o)]: ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => ((A @ F) = (B @ F)))) => ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => ((C @ F) = (D @ F)))) => (? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => (((A @ F) | (C @ F)) = ((B @ F) | (D @ F))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 20.45/5.59  thf(57,axiom,((! [A:nat,B:nat,C:$o]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ A) => (C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_437_order__less__imp__triv)).
% 20.45/5.59  thf(382,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)],[57])).
% 20.45/5.59  thf(144,axiom,((~ (? [A:nat]: (vEBT_vebt_member @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)) @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4__C161_C)).
% 20.45/5.59  thf(713,plain,((~ (? [A:nat]: (vEBT_vebt_member @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 20.45/5.59  thf(140,axiom,((vEBT_VEBT_minNull @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_tc)).
% 20.45/5.59  thf(704,plain,((vEBT_VEBT_minNull @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 20.45/5.59  thf(50,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1016_add__strict__right__mono)).
% 20.45/5.59  thf(350,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 20.45/5.59  thf(98,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ C) => (ord_less_nat @ A @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_178_add__lessD1)).
% 20.45/5.59  thf(540,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ C) => (ord_less_nat @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 20.45/5.59  thf(26,axiom,((! [A:nat]: ? [B:nat]: (ord_less_nat @ A @ B))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_570_gt__ex)).
% 20.45/5.59  thf(245,plain,((! [A:nat]: ? [B:nat]: (ord_less_nat @ A @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 20.45/5.59  thf(126,axiom,((! [A:vEBT_VEBT]: ((member_VEBT_VEBT @ A @ (set_VEBT_VEBT2 @ treeList)) => (vEBT_invar_vebt @ A @ na)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_32__C0_C)).
% 20.45/5.59  thf(649,plain,((! [A:vEBT_VEBT]: ((member_VEBT_VEBT @ A @ (set_VEBT_VEBT2 @ treeList)) => (vEBT_invar_vebt @ A @ na)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 20.45/5.59  thf(154,axiom,((! [A:nat,B:nat,C:list_VEBT_VEBT,D:vEBT_VEBT]: ((A != B) => ((nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ C @ A @ D) @ B) = (nth_VEBT_VEBT @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_10_nth__list__update__neq)).
% 20.45/5.59  thf(737,plain,((! [A:nat,B:nat,C:list_VEBT_VEBT,D:vEBT_VEBT]: ((~ (A = B)) => ((nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ C @ A @ D) @ B) = (nth_VEBT_VEBT @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 20.45/5.59  thf(45,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/sandbox2/benchmark/theBenchmark.p',fact_529_linorder__less__wlog)).
% 20.45/5.59  thf(318,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)],[45])).
% 20.45/5.59  thf(96,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1536_pinf_I7_J)).
% 20.45/5.59  thf(535,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 20.45/5.59  thf(28,axiom,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ A @ (ord_max_nat @ B @ C)) = (ord_max_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1507_max__add__distrib__right)).
% 20.45/5.59  thf(251,plain,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ A @ (ord_max_nat @ B @ C)) = (ord_max_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 20.45/5.59  thf(121,axiom,((! [A:list_VEBT_VEBT,B:set_VEBT_VEBT,C:vEBT_VEBT,D:nat]: ((ord_le4337996190870823476T_VEBT @ (set_VEBT_VEBT2 @ A) @ B) => ((member_VEBT_VEBT @ C @ B) => (ord_le4337996190870823476T_VEBT @ (set_VEBT_VEBT2 @ (list_u1324408373059187874T_VEBT @ A @ D @ C)) @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_268_set__update__subsetI)).
% 20.45/5.59  thf(626,plain,((! [A:list_VEBT_VEBT,B:set_VEBT_VEBT,C:vEBT_VEBT,D:nat]: ((ord_le4337996190870823476T_VEBT @ (set_VEBT_VEBT2 @ A) @ B) => ((member_VEBT_VEBT @ C @ B) => (ord_le4337996190870823476T_VEBT @ (set_VEBT_VEBT2 @ (list_u1324408373059187874T_VEBT @ A @ D @ C)) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 20.45/5.59  thf(1,conjecture,(((nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na) @ (vEBT_vebt_insert @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)) @ (vEBT_VEBT_low @ mi @ na))) @ i) = (vEBT_vebt_insert @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)) @ (vEBT_VEBT_low @ mi @ na)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 20.45/5.59  thf(2,negated_conjecture,((~ ((nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na) @ (vEBT_vebt_insert @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)) @ (vEBT_VEBT_low @ mi @ na))) @ i) = (vEBT_vebt_insert @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)) @ (vEBT_VEBT_low @ mi @ na))))),inference(neg_conjecture,[status(cth)],[1])).
% 20.45/5.59  thf(155,plain,((~ ((nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na) @ (vEBT_vebt_insert @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)) @ (vEBT_VEBT_low @ mi @ na))) @ i) = (vEBT_vebt_insert @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)) @ (vEBT_VEBT_low @ mi @ na))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 20.45/5.59  thf(139,axiom,((! [A:nat,B:nat,C:list_VEBT_VEBT,D:vEBT_VEBT,E:vEBT_VEBT]: ((A != B) => ((list_u1324408373059187874T_VEBT @ (list_u1324408373059187874T_VEBT @ C @ A @ D) @ B @ E) = (list_u1324408373059187874T_VEBT @ (list_u1324408373059187874T_VEBT @ C @ B @ E) @ A @ D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_18_list__update__swap)).
% 20.45/5.59  thf(700,plain,((! [A:nat,B:nat,C:list_VEBT_VEBT,D:vEBT_VEBT,E:vEBT_VEBT]: ((~ (A = B)) => ((list_u1324408373059187874T_VEBT @ (list_u1324408373059187874T_VEBT @ C @ A @ D) @ B @ E) = (list_u1324408373059187874T_VEBT @ (list_u1324408373059187874T_VEBT @ C @ B @ E) @ A @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 20.45/5.59  thf(93,axiom,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ (ord_max_nat @ A @ B) @ C) = (ord_max_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1509_nat__add__max__left)).
% 20.45/5.59  thf(520,plain,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ (ord_max_nat @ A @ B) @ C) = (ord_max_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 20.45/5.59  thf(136,axiom,((! [A:list_VEBT_VEBT,B:vEBT_VEBT]: ((! [C:vEBT_VEBT]: ((member_VEBT_VEBT @ C @ (set_VEBT_VEBT2 @ A)) => (C = B))) => ((replicate_VEBT_VEBT @ (size_s6755466524823107622T_VEBT @ A) @ B) = A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1819_replicate__length__same)).
% 20.45/5.59  thf(685,plain,((! [A:list_VEBT_VEBT,B:vEBT_VEBT]: ((! [C:vEBT_VEBT]: ((member_VEBT_VEBT @ C @ (set_VEBT_VEBT2 @ A)) => (C = B))) => ((replicate_VEBT_VEBT @ (size_s6755466524823107622T_VEBT @ A) @ B) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 20.45/5.59  thf(62,axiom,((ord_less_nat = (^ [A:nat,B:nat]: ((B = (ord_max_nat @ B @ A)) & (B != A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1636_max_Ostrict__order__iff)).
% 20.45/5.59  thf(399,plain,(((ord_less_nat) = (^ [A:nat,B:nat]: ((B = (ord_max_nat @ B @ A)) & ~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 20.45/5.59  thf(124,axiom,((! [A:nat,B:list_VEBT_VEBT,C:nat]: ((ord_less_nat @ A @ (size_s6755466524823107622T_VEBT @ B)) => ((ord_less_nat @ C @ (size_s6755466524823107622T_VEBT @ B)) => ((set_VEBT_VEBT2 @ (list_u1324408373059187874T_VEBT @ (list_u1324408373059187874T_VEBT @ B @ A @ (nth_VEBT_VEBT @ B @ C)) @ C @ (nth_VEBT_VEBT @ B @ A))) = (set_VEBT_VEBT2 @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_108_set__swap)).
% 20.45/5.59  thf(636,plain,((! [A:nat,B:list_VEBT_VEBT,C:nat]: ((ord_less_nat @ A @ (size_s6755466524823107622T_VEBT @ B)) => ((ord_less_nat @ C @ (size_s6755466524823107622T_VEBT @ B)) => ((set_VEBT_VEBT2 @ (list_u1324408373059187874T_VEBT @ (list_u1324408373059187874T_VEBT @ B @ A @ (nth_VEBT_VEBT @ B @ C)) @ C @ (nth_VEBT_VEBT @ B @ A))) = (set_VEBT_VEBT2 @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 20.45/5.59  thf(36,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => ((ord_max_nat @ B @ A) = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1565_max_Oabsorb3)).
% 20.45/5.59  thf(278,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => ((ord_max_nat @ B @ A) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 20.45/5.59  thf(60,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_561_order_Oasym)).
% 20.45/5.59  thf(394,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 20.45/5.59  thf(41,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/sandbox2/benchmark/theBenchmark.p',fact_525_order_Ostrict__trans)).
% 20.45/5.59  thf(299,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)],[41])).
% 20.45/5.59  thf(19,axiom,((! [A:nat,B:vEBT_VEBT]: ((size_s6755466524823107622T_VEBT @ (replicate_VEBT_VEBT @ A @ B)) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1707_length__replicate)).
% 20.45/5.59  thf(226,plain,((! [A:nat,B:vEBT_VEBT]: ((size_s6755466524823107622T_VEBT @ (replicate_VEBT_VEBT @ A @ B)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 20.45/5.59  thf(24,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_539_dual__order_Oasym)).
% 20.45/5.59  thf(241,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 20.45/5.59  thf(89,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) => (ord_less_nat @ B @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1019_add__less__imp__less__left)).
% 20.45/5.59  thf(505,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) => (ord_less_nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 20.45/5.59  thf(71,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ A @ (plus_plus_nat @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_172_trans__less__add2)).
% 20.45/5.59  thf(438,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ A @ (plus_plus_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 20.45/5.59  thf(84,axiom,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ (plus_plus_nat @ A @ B) @ C) = (plus_plus_nat @ A @ (plus_plus_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_921_add_Oassoc)).
% 20.45/5.59  thf(490,plain,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ (plus_plus_nat @ A @ B) @ C) = (plus_plus_nat @ A @ (plus_plus_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 20.45/5.59  thf(4,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_nat @ B @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_892_add__less__cancel__left)).
% 20.45/5.59  thf(162,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 20.45/5.59  thf(101,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (~ (ord_less_nat @ C @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1540_pinf_I5_J)).
% 20.45/5.59  thf(548,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (~ (ord_less_nat @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 20.45/5.59  thf(12,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => ((ord_max_nat @ A @ B) = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1569_max_Oabsorb4)).
% 20.45/5.59  thf(194,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => ((ord_max_nat @ A @ B) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 20.45/5.59  thf(119,axiom,((! [A:nat,B:list_VEBT_VEBT,C:(vEBT_VEBT > $o)]: ((ord_less_nat @ A @ (size_s6755466524823107622T_VEBT @ B)) => ((! [D:vEBT_VEBT]: ((member_VEBT_VEBT @ D @ (set_VEBT_VEBT2 @ B)) => (C @ D))) => (C @ (nth_VEBT_VEBT @ B @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_286_list__ball__nth)).
% 20.45/5.59  thf(617,plain,((! [A:nat,B:list_VEBT_VEBT,C:(vEBT_VEBT > $o)]: ((ord_less_nat @ A @ (size_s6755466524823107622T_VEBT @ B)) => ((! [D:vEBT_VEBT]: ((member_VEBT_VEBT @ D @ (set_VEBT_VEBT2 @ B)) => (C @ D))) => (C @ (nth_VEBT_VEBT @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 20.45/5.59  thf(92,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_509_dual__order_Ostrict__implies__not__eq)).
% 20.45/5.59  thf(516,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 20.45/5.59  thf(104,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_429_order__less__imp__not__eq)).
% 20.45/5.59  thf(557,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 20.45/5.59  thf(108,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_493_order__less__asym_H)).
% 20.45/5.59  thf(580,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 20.45/5.59  thf(125,axiom,((! [A:list_VEBT_VEBT,B:nat,C:vEBT_VEBT]: (((size_s6755466524823107622T_VEBT @ A) = B) => ((! [D:vEBT_VEBT]: ((member_VEBT_VEBT @ D @ (set_VEBT_VEBT2 @ A)) => (D = C))) => (A = (replicate_VEBT_VEBT @ B @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1816_replicate__eqI)).
% 20.45/5.59  thf(640,plain,((! [A:list_VEBT_VEBT,B:nat,C:vEBT_VEBT]: (((size_s6755466524823107622T_VEBT @ A) = B) => ((! [D:vEBT_VEBT]: ((member_VEBT_VEBT @ D @ (set_VEBT_VEBT2 @ A)) => (D = C))) => (A = (replicate_VEBT_VEBT @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 20.45/5.59  thf(141,axiom,((vEBT_V5917875025757280293ildren = (^ [A:nat,B:list_VEBT_VEBT,C:nat]: (vEBT_V8194947554948674370ptions @ (nth_VEBT_VEBT @ B @ (vEBT_VEBT_high @ C @ A)) @ (vEBT_VEBT_low @ C @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_21_in__children__def)).
% 20.45/5.59  thf(705,plain,(((vEBT_V5917875025757280293ildren) = (^ [A:nat,B:list_VEBT_VEBT,C:nat]: (vEBT_V8194947554948674370ptions @ (nth_VEBT_VEBT @ B @ (vEBT_VEBT_high @ C @ A)) @ (vEBT_VEBT_low @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 20.45/5.59  thf(142,axiom,((! [A:nat,B:nat]: ((vEBT_VEBT_bit_concat @ (vEBT_VEBT_high @ A @ B) @ (vEBT_VEBT_low @ A @ B) @ B) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_bit__split__inv)).
% 20.45/5.59  thf(707,plain,((! [A:nat,B:nat]: ((vEBT_VEBT_bit_concat @ (vEBT_VEBT_high @ A @ B) @ (vEBT_VEBT_low @ A @ B) @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 20.45/5.59  thf(132,axiom,((! [A:option4927543243414619207at_nat,B:nat,C:list_VEBT_VEBT,D:vEBT_VEBT,E:nat]: ((vEBT_invar_vebt @ (vEBT_Node @ A @ B @ C @ D) @ E) => (B = E)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1466_deg__deg__n)).
% 20.45/5.59  thf(673,plain,((! [A:option4927543243414619207at_nat,B:nat,C:list_VEBT_VEBT,D:vEBT_VEBT,E:nat]: ((vEBT_invar_vebt @ (vEBT_Node @ A @ B @ C @ D) @ E) => (B = E)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 20.45/5.59  thf(8,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (C != A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1544_pinf_I4_J)).
% 20.45/5.59  thf(182,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (~ (C = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 20.45/5.59  thf(72,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((~ (ord_less_nat @ B @ A)) = (B = A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_547_antisym__conv3)).
% 20.45/5.59  thf(441,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)],[72])).
% 20.45/5.59  thf(110,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((A = (plus_plus_nat @ B @ C)) => ((plus_plus_nat @ A @ D) = (plus_plus_nat @ B @ (plus_plus_nat @ C @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_913_group__cancel_Oadd1)).
% 20.45/5.59  thf(585,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((A = (plus_plus_nat @ B @ C)) => ((plus_plus_nat @ A @ D) = (plus_plus_nat @ B @ (plus_plus_nat @ C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 20.45/5.59  thf(88,axiom,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ (ord_max_nat @ A @ B) @ C) = (ord_max_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1504_max__add__distrib__left)).
% 20.45/5.59  thf(502,plain,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ (ord_max_nat @ A @ B) @ C) = (ord_max_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 20.45/5.59  thf(118,axiom,((! [A:list_VEBT_VEBT,B:list_VEBT_VEBT]: (((size_s6755466524823107622T_VEBT @ A) != (size_s6755466524823107622T_VEBT @ B)) => (A != B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_123_neq__if__length__neq)).
% 20.45/5.59  thf(613,plain,((! [A:list_VEBT_VEBT,B:list_VEBT_VEBT]: ((~ ((size_s6755466524823107622T_VEBT @ A) = (size_s6755466524823107622T_VEBT @ B))) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 20.45/5.59  thf(115,axiom,((! [A:vEBT_VEBT,B:nat,C:nat]: ((vEBT_invar_vebt @ A @ B) => ((vEBT_V8194947554948674370ptions @ A @ C) => (vEBT_vebt_member @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_28_valid__member__both__member__options)).
% 20.45/5.59  thf(600,plain,((! [A:vEBT_VEBT,B:nat,C:nat]: ((vEBT_invar_vebt @ A @ B) => ((vEBT_V8194947554948674370ptions @ A @ C) => (vEBT_vebt_member @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 20.45/5.59  thf(150,axiom,((! [A:vEBT_VEBT]: ((member_VEBT_VEBT @ A @ (set_VEBT_VEBT2 @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na) @ (vEBT_vebt_insert @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)) @ (vEBT_VEBT_low @ mi @ na))))) => (vEBT_invar_vebt @ A @ na)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_16__C11_C)).
% 20.45/5.59  thf(727,plain,((! [A:vEBT_VEBT]: ((member_VEBT_VEBT @ A @ (set_VEBT_VEBT2 @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na) @ (vEBT_vebt_insert @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)) @ (vEBT_VEBT_low @ mi @ na))))) => (vEBT_invar_vebt @ A @ na)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 20.45/5.59  thf(86,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (C != A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1520_minf_I4_J)).
% 20.45/5.59  thf(497,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (C = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 20.45/5.59  thf(21,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ (plus_plus_nat @ C @ A) @ (plus_plus_nat @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1013_add__strict__left__mono)).
% 20.45/5.59  thf(231,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ (plus_plus_nat @ C @ A) @ (plus_plus_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 20.45/5.59  thf(15,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/sandbox2/benchmark/theBenchmark.p',fact_469_ord__less__eq__subst)).
% 20.45/5.59  thf(203,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)],[15])).
% 20.45/5.59  thf(55,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_465_order__less__irrefl)).
% 20.45/5.59  thf(368,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 20.45/5.59  thf(43,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_nat @ B @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_94_nat__add__left__cancel__less)).
% 20.45/5.59  thf(304,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 20.45/5.59  thf(30,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ C @ B)) => (ord_less_nat @ A @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1022_add__less__imp__less__right)).
% 20.45/5.59  thf(258,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ C @ B)) => (ord_less_nat @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 20.45/5.59  thf(9,axiom,((~ (ord_less_nat @ mi @ xa))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_17_False)).
% 20.45/5.59  thf(186,plain,((~ (ord_less_nat @ mi @ xa))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 20.45/5.59  thf(123,axiom,((! [A:vEBT_VEBT,B:nat,C:nat]: ((vEBT_invar_vebt @ A @ B) => ((vEBT_V8194947554948674370ptions @ A @ C) = (vEBT_vebt_member @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_27_both__member__options__equiv__member)).
% 20.45/5.59  thf(632,plain,((! [A:vEBT_VEBT,B:nat,C:nat]: ((vEBT_invar_vebt @ A @ B) => ((vEBT_V8194947554948674370ptions @ A @ C) = (vEBT_vebt_member @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 20.45/5.59  thf(63,axiom,((! [A:nat,B:nat]: ~ (ord_less_nat @ (plus_plus_nat @ A @ B) @ B))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_175_not__add__less2)).
% 20.45/5.59  thf(401,plain,((! [A:nat,B:nat]: ~ (ord_less_nat @ (plus_plus_nat @ A @ B) @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 20.45/5.59  thf(152,axiom,((~ (? [A:nat]: (vEBT_V8194947554948674370ptions @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)) @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_11__C162_C)).
% 20.45/5.59  thf(731,plain,((~ (? [A:nat]: (vEBT_V8194947554948674370ptions @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ mi @ na)) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 20.45/5.59  thf(34,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) = ((ord_less_nat @ B @ A) | (A = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_521_not__less__iff__gr__or__eq)).
% 20.45/5.59  thf(272,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)],[34])).
% 20.45/5.59  thf(145,axiom,((! [A:list_VEBT_VEBT,B:nat]: ((list_u1324408373059187874T_VEBT @ A @ B @ (nth_VEBT_VEBT @ A @ B)) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_7_list__update__id)).
% 20.45/5.59  thf(716,plain,((! [A:list_VEBT_VEBT,B:nat]: ((list_u1324408373059187874T_VEBT @ A @ B @ (nth_VEBT_VEBT @ A @ B)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 20.45/5.60  thf(69,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1413_verit__comp__simplify1_I1_J)).
% 20.45/5.60  thf(433,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 20.45/5.60  thf(91,axiom,((! [A:list_VEBT_VEBT,B:list_VEBT_VEBT]: (((size_s6755466524823107622T_VEBT @ A) = (size_s6755466524823107622T_VEBT @ B)) => ((! [C:nat]: ((ord_less_nat @ C @ (size_s6755466524823107622T_VEBT @ A)) => ((nth_VEBT_VEBT @ A @ C) = (nth_VEBT_VEBT @ B @ C)))) => (A = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_262_nth__equalityI)).
% 20.45/5.60  thf(510,plain,((! [A:list_VEBT_VEBT,B:list_VEBT_VEBT]: (((size_s6755466524823107622T_VEBT @ A) = (size_s6755466524823107622T_VEBT @ B)) => ((! [C:nat]: ((ord_less_nat @ C @ (size_s6755466524823107622T_VEBT @ A)) => ((nth_VEBT_VEBT @ A @ C) = (nth_VEBT_VEBT @ B @ C)))) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 20.45/5.60  thf(74,axiom,((((=) @ list_VEBT_VEBT) = (^ [A:list_VEBT_VEBT,B:list_VEBT_VEBT]: (((size_s6755466524823107622T_VEBT @ A) = (size_s6755466524823107622T_VEBT @ B)) & ! [C:nat]: ((ord_less_nat @ C @ (size_s6755466524823107622T_VEBT @ A)) => ((nth_VEBT_VEBT @ A @ C) = (nth_VEBT_VEBT @ B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_256_list__eq__iff__nth__eq)).
% 20.45/5.60  thf(447,plain,((((=) @ list_VEBT_VEBT) = (^ [A:list_VEBT_VEBT,B:list_VEBT_VEBT]: (((size_s6755466524823107622T_VEBT @ A) = (size_s6755466524823107622T_VEBT @ B)) & ! [C:nat]: ((ord_less_nat @ C @ (size_s6755466524823107622T_VEBT @ A)) => ((nth_VEBT_VEBT @ A @ C) = (nth_VEBT_VEBT @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 20.45/5.60  thf(116,axiom,((! [A:vEBT_VEBT,B:nat]: ((vEBT_VEBT_minNull @ A) => (~ (vEBT_vebt_member @ A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_25_min__Null__member)).
% 20.45/5.60  thf(603,plain,((! [A:vEBT_VEBT,B:nat]: ((vEBT_VEBT_minNull @ A) => (~ (vEBT_vebt_member @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 20.45/5.60  thf(39,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ C @ B)) = (ord_less_nat @ A @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_895_add__less__cancel__right)).
% 20.45/5.60  thf(294,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ C @ B)) = (ord_less_nat @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 20.45/5.60  thf(47,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_587_less__not__refl)).
% 20.45/5.60  thf(341,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 20.45/5.60  thf(33,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_565_less__imp__neq)).
% 20.45/5.60  thf(268,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 20.45/5.60  thf(52,axiom,((! [A:nat,B:nat,C:nat]: (((plus_plus_nat @ A @ B) = (plus_plus_nat @ C @ B)) = (A = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_847_add__right__cancel)).
% 20.45/5.60  thf(358,plain,((! [A:nat,B:nat,C:nat]: (((plus_plus_nat @ A @ B) = (plus_plus_nat @ C @ B)) = (A = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 20.45/5.60  thf(95,axiom,((! [A:nat,B:nat]: ((A != B) = ((ord_less_nat @ A @ B) | (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_497_linorder__neq__iff)).
% 20.45/5.60  thf(532,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)],[95])).
% 20.45/5.60  thf(120,axiom,((! [A:vEBT_VEBT]: ((~ (vEBT_VEBT_minNull @ A)) => (? [B:nat]: (vEBT_V8194947554948674370ptions @ A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_24_not__min__Null__member)).
% 20.45/5.60  thf(624,plain,((! [A:vEBT_VEBT]: ((~ (vEBT_VEBT_minNull @ A)) => (? [B:nat]: (vEBT_V8194947554948674370ptions @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 20.45/5.60  thf(79,axiom,((! [A:nat,B:nat,C:nat,D:nat]: (((ord_less_nat @ A @ B) & (C = D)) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1006_add__mono__thms__linordered__field_I1_J)).
% 20.45/5.60  thf(464,plain,((! [A:nat,B:nat,C:nat,D:nat]: (((ord_less_nat @ A @ B) & (C = D)) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 20.45/5.60  thf(113,axiom,((deg = (plus_plus_nat @ na @ m))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_57__C3_C)).
% 20.45/5.60  thf(596,plain,((deg = (plus_plus_nat @ na @ m))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 20.45/5.60  thf(14,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_535_dual__order_Oirrefl)).
% 20.45/5.60  thf(200,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 20.45/5.60  thf(7,axiom,((! [A:nat,B:list_VEBT_VEBT,C:vEBT_VEBT]: ((ord_less_nat @ A @ (size_s6755466524823107622T_VEBT @ B)) => ((nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ B @ A @ C) @ A) = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_105_nth__list__update__eq)).
% 20.45/5.60  thf(178,plain,((! [A:nat,B:list_VEBT_VEBT,C:vEBT_VEBT]: ((ord_less_nat @ A @ (size_s6755466524823107622T_VEBT @ B)) => ((nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ B @ A @ C) @ A) = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 20.45/5.60  thf(137,axiom,(((xa != mi) & (xa != ma))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_34_mimaxrel)).
% 20.45/5.60  thf(691,plain,((~ (xa = mi) & ~ (xa = ma))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 20.45/5.60  thf(87,axiom,((ord_less_nat @ xa @ mi)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_30_abcdef)).
% 20.45/5.60  thf(501,plain,((ord_less_nat @ xa @ mi)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 20.45/5.60  thf(29,axiom,((! [A:nat,B:nat,C:nat,D:nat]: (((A = B) & (C = D)) => ((plus_plus_nat @ A @ C) = (plus_plus_nat @ B @ D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_909_add__mono__thms__linordered__semiring_I4_J)).
% 20.45/5.60  thf(254,plain,((! [A:nat,B:nat,C:nat,D:nat]: (((A = B) & (C = D)) => ((plus_plus_nat @ A @ C) = (plus_plus_nat @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 20.45/5.60  thf(46,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_425_order__less__imp__not__eq2)).
% 20.45/5.60  thf(337,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 20.45/5.60  thf(128,axiom,((! [A:nat,B:list_VEBT_VEBT]: ((ord_less_nat @ A @ (size_s6755466524823107622T_VEBT @ B)) => (member_VEBT_VEBT @ (nth_VEBT_VEBT @ B @ A) @ (set_VEBT_VEBT2 @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_292_nth__mem)).
% 20.45/5.60  thf(659,plain,((! [A:nat,B:list_VEBT_VEBT]: ((ord_less_nat @ A @ (size_s6755466524823107622T_VEBT @ B)) => (member_VEBT_VEBT @ (nth_VEBT_VEBT @ B @ A) @ (set_VEBT_VEBT2 @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 20.45/5.60  thf(17,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1512_minf_I7_J)).
% 20.45/5.60  thf(215,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 20.45/5.60  thf(133,axiom,((! [A:nat,B:list_VEBT_VEBT,C:vEBT_VEBT]: ((ord_less_nat @ A @ (size_s6755466524823107622T_VEBT @ B)) => (member_VEBT_VEBT @ C @ (set_VEBT_VEBT2 @ (list_u1324408373059187874T_VEBT @ B @ A @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_418_set__update__memI)).
% 20.45/5.60  thf(676,plain,((! [A:nat,B:list_VEBT_VEBT,C:vEBT_VEBT]: ((ord_less_nat @ A @ (size_s6755466524823107622T_VEBT @ B)) => (member_VEBT_VEBT @ C @ (set_VEBT_VEBT2 @ (list_u1324408373059187874T_VEBT @ B @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 20.45/5.60  thf(54,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_585_less__not__refl3)).
% 20.45/5.60  thf(364,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 20.45/5.60  thf(765,plain,(($false)),inference(e,[status(thm)],[606,237,444,629,347,468,234,666,408,217,449,247,523,582,385,550,404,436,651,389,724,570,719,344,542,157,485,574,353,734,396,411,243,265,507,307,292,452,661,302,260,598,561,297,424,275,165,729,229,197,361,665,461,493,682,710,697,725,188,169,593,471,554,537,476,590,679,212,457,721,371,191,281,545,413,382,713,704,350,540,245,649,737,318,535,251,626,155,700,520,685,399,636,278,394,299,226,241,505,438,490,162,548,194,617,516,557,580,640,705,707,673,182,441,585,502,613,600,727,497,231,203,368,304,258,186,632,401,731,272,716,433,510,447,603,294,341,268,358,532,624,464,596,200,178,691,501,254,337,659,215,676,364])).
% 20.45/5.60  % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.45/5.60  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------