%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : ITP267_1 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 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 : Thu Sep 24 12:57:17 PM UTC 2026
% Result : Theorem 222.93s 35.73s
% Output : CNFRefutation 222.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 16
% Syntax : Number of formulae : 65 ( 45 unt; 0 typ; 0 def)
% Number of atoms : 88 ( 51 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 46 ( 23 ~; 21 |; 2 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 22 ( 4 avg)
% Number of types : 15 ( 14 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 40 ( 40 usr; 26 con; 0-3 aty)
% Number of variables : 63 ( 0 sgn 63 !; 0 ?; 63 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
fun_nat_fun_nat_bool: $tType ).
tff(decl_sort2,type,
fun_nat_bool: $tType ).
tff(decl_sort3,type,
fun_nat_fun_nat_nat: $tType ).
tff(decl_sort4,type,
nat: $tType ).
tff(decl_sort5,type,
num: $tType ).
tff(decl_sort6,type,
bool: $tType ).
tff(decl_sort7,type,
fun_nat_nat: $tType ).
tff(decl_sort8,type,
vEBT_VEBT: $tType ).
tff(decl_sort9,type,
option_nat: $tType ).
tff(decl_sort10,type,
list_VEBT_VEBT: $tType ).
tff(decl_sort11,type,
fun_num_nat: $tType ).
tff(decl_sort12,type,
fun_num_num: $tType ).
tff(decl_sort13,type,
fun_op7792301606653096457t_bool: $tType ).
tff(decl_sort14,type,
fun_option_nat_bool: $tType ).
tff(decl_1010,type,
one_one_nat: nat ).
tff(decl_1017,type,
plus_plus_nat: fun_nat_fun_nat_nat ).
tff(decl_1030,type,
times_times_nat: fun_nat_fun_nat_nat ).
tff(decl_1115,type,
if_nat: bool > fun_nat_fun_nat_nat ).
tff(decl_1157,type,
list_u1324408373059187874T_VEBT: ( vEBT_VEBT * ( nat * list_VEBT_VEBT ) ) > list_VEBT_VEBT ).
tff(decl_1176,type,
nth_VEBT_VEBT: ( nat * list_VEBT_VEBT ) > vEBT_VEBT ).
tff(decl_1204,type,
suc: fun_nat_nat ).
tff(decl_1271,type,
bit0: fun_num_num ).
tff(decl_1273,type,
one: num ).
tff(decl_1281,type,
numeral_numeral_nat: fun_num_nat ).
tff(decl_1287,type,
none_nat: option_nat ).
tff(decl_1301,type,
the_nat: option_nat > nat ).
tff(decl_1317,type,
ord_less_nat: fun_nat_fun_nat_bool ).
tff(decl_1338,type,
ord_less_eq_nat: fun_nat_fun_nat_bool ).
tff(decl_1383,type,
power_power_nat: fun_nat_fun_nat_nat ).
tff(decl_1467,type,
divide_divide_nat: fun_nat_fun_nat_nat ).
tff(decl_1478,type,
modulo_modulo_nat: fun_nat_fun_nat_nat ).
tff(decl_1614,type,
vEBT_VEBT_high: fun_nat_fun_nat_nat ).
tff(decl_1616,type,
vEBT_VEBT_low: fun_nat_fun_nat_nat ).
tff(decl_1627,type,
vEBT_vebt_delete: ( nat * vEBT_VEBT ) > vEBT_VEBT ).
tff(decl_1648,type,
vEBT_vebt_maxt: vEBT_VEBT > option_nat ).
tff(decl_1754,type,
aa_nat_bool: ( nat * fun_nat_bool ) > bool ).
tff(decl_1756,type,
aa_nat_nat: ( nat * fun_nat_nat ) > nat ).
tff(decl_1782,type,
aa_nat_fun_nat_bool: ( nat * fun_nat_fun_nat_bool ) > fun_nat_bool ).
tff(decl_1784,type,
aa_nat_fun_nat_nat: ( nat * fun_nat_fun_nat_nat ) > fun_nat_nat ).
tff(decl_1814,type,
aa_num_nat: ( num * fun_num_nat ) > nat ).
tff(decl_1815,type,
aa_num_num: ( num * fun_num_num ) > num ).
tff(decl_1830,type,
aa_option_nat_bool: ( option_nat * fun_option_nat_bool ) > bool ).
tff(decl_1832,type,
aa_opt7943525813896274546t_bool: ( option_nat * fun_op7792301606653096457t_bool ) > fun_option_nat_bool ).
tff(decl_2112,type,
fFalse: bool ).
tff(decl_2114,type,
fTrue: bool ).
tff(decl_2121,type,
fequal_nat: fun_nat_fun_nat_bool ).
tff(decl_2122,type,
fequal_option_nat: fun_op7792301606653096457t_bool ).
tff(decl_2138,type,
pp: bool > $o ).
tff(decl_2139,type,
deg: nat ).
tff(decl_2140,type,
lx: nat ).
tff(decl_2142,type,
ma: nat ).
tff(decl_2144,type,
na: nat ).
tff(decl_2145,type,
summary: vEBT_VEBT ).
tff(decl_2146,type,
summin: nat ).
tff(decl_2147,type,
treeList: list_VEBT_VEBT ).
tff(help_fFalse_1_1_U,axiom,
~ pp(fFalse),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
tff(help_If_3_1_If_001t__Product____Type__Oprod_It__Code____Numeral__Ointeger_Mt__Code____Numeral__Ointeger_J_T,axiom,
! [X19565: bool] :
( ( X19565 = fFalse )
| ( X19565 = fTrue ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_If_3_1_If_001t__Product____Type__Oprod_It__Code____Numeral__Ointeger_Mt__Code____Numeral__Ointeger_J_T) ).
tff(help_fequal_2_1_fequal_001t__Nat__Onat_T,axiom,
! [X2: nat,X10: nat] :
( pp(aa_nat_bool(aa_nat_fun_nat_bool(fequal_nat,X2),X10))
| ( X2 != X10 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fequal_2_1_fequal_001t__Nat__Onat_T) ).
tff(help_fequal_2_1_fequal_001t__Option__Ooption_It__Nat__Onat_J_T,axiom,
! [X19547: option_nat,X19548: option_nat] :
( pp(aa_option_nat_bool(aa_opt7943525813896274546t_bool(fequal_option_nat,X19547),X19548))
| ( X19547 != X19548 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fequal_2_1_fequal_001t__Option__Ooption_It__Nat__Onat_J_T) ).
tff(conj_0,conjecture,
( pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_eq_nat,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_nat_bool(aa_nat_fun_nat_bool(fequal_nat,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),ma)),aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_option_nat_bool(aa_opt7943525813896274546t_bool(fequal_option_nat,vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))),none_nat)),aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,deg),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))))),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))))),the_nat(vEBT_vebt_maxt(nth_VEBT_VEBT(list_u1324408373059187874T_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na),vEBT_vebt_delete(nth_VEBT_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)),aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_low,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na))),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))))))))),ma)))
& pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_nat,aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_nat_bool(aa_nat_fun_nat_bool(fequal_nat,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),ma)),aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_option_nat_bool(aa_opt7943525813896274546t_bool(fequal_option_nat,vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))),none_nat)),aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,deg),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))))),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))))),the_nat(vEBT_vebt_maxt(nth_VEBT_VEBT(list_u1324408373059187874T_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na),vEBT_vebt_delete(nth_VEBT_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)),aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_low,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na))),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))))))))),ma)),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),deg))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
tff(fact_1729_add_Ocommute,axiom,
! [X5: nat,X6: nat] : ( aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,X5),X6) = aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,X6),X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1729_add_Ocommute) ).
tff(fact_2280_low__def,axiom,
! [X2: nat,X7: nat] : ( aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_low,X2),X7) = aa_nat_nat(aa_nat_fun_nat_nat(modulo_modulo_nat,X2),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),X7)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2280_low__def) ).
tff(fact_4__092_060open_062summin_A_K_A2_A_094_An_A_L_Alx_A_061_Ama_092_060close_062,axiom,
aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx) = ma,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4__092_060open_062summin_A_K_A2_A_094_An_A_L_Alx_A_061_Ama_092_060close_062) ).
tff(fact_758_Suc__1,axiom,
aa_nat_nat(suc,one_one_nat) = aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_758_Suc__1) ).
tff(fact_10__C9_C,axiom,
aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,deg),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))) = na,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_10__C9_C) ).
tff(help_fTrue_1_1_U,axiom,
pp(fTrue),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fTrue_1_1_U) ).
tff(fact_8_True,axiom,
vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na))) = none_nat,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_8_True) ).
tff(fact_2579_mod__mult__self1,axiom,
! [X5: nat,X4779: nat,X6: nat] : ( aa_nat_nat(aa_nat_fun_nat_nat(modulo_modulo_nat,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,X5),aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,X4779),X6))),X6) = aa_nat_nat(aa_nat_fun_nat_nat(modulo_modulo_nat,X5),X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2579_mod__mult__self1) ).
tff(fact_0__C5_Ohyps_C_I8_J,axiom,
pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_nat,ma),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),deg))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0__C5_Ohyps_C_I8_J) ).
tff(fact_602_le__refl,axiom,
! [X7: nat] : pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_eq_nat,X7),X7)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_602_le__refl) ).
tff(help_If_1_1_If_001t__Nat__Onat_T,axiom,
! [X2: nat,X10: nat] : ( aa_nat_nat(aa_nat_fun_nat_nat(if_nat(fTrue),X2),X10) = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_If_1_1_If_001t__Nat__Onat_T) ).
tff(c_0_16,plain,
~ pp(fFalse),
inference(fof_simplification,[status(thm)],[help_fFalse_1_1_U]) ).
tff(c_0_17,plain,
! [X22092: bool] :
( ( X22092 = fFalse )
| ( X22092 = fTrue ) ),
inference(variable_rename,[status(thm)],[help_If_3_1_If_001t__Product____Type__Oprod_It__Code____Numeral__Ointeger_Mt__Code____Numeral__Ointeger_J_T]) ).
tff(c_0_18,plain,
~ pp(fFalse),
inference(fof_nnf,[status(thm)],[c_0_16]) ).
tcf(c_0_19,plain,
! [X211: bool] :
( ( X211 = fFalse )
| ( X211 = fTrue ) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
tcf(c_0_20,plain,
~ pp(fFalse),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
tcf(c_0_21,plain,
! [X217: bool,X211: bool] :
( ( X217 = X211 )
| ( X217 = fFalse )
| ( X211 = fFalse ) ),
inference(spm,[status(thm)],[c_0_19,c_0_19]) ).
tff(c_0_22,plain,
! [X2: nat,X10: nat] :
( pp(aa_nat_bool(aa_nat_fun_nat_bool(fequal_nat,X2),X10))
| ( X2 != X10 ) ),
inference(fof_simplification,[status(thm)],[help_fequal_2_1_fequal_001t__Nat__Onat_T]) ).
tff(c_0_23,plain,
! [X19547: option_nat,X19548: option_nat] :
( pp(aa_option_nat_bool(aa_opt7943525813896274546t_bool(fequal_option_nat,X19547),X19548))
| ( X19547 != X19548 ) ),
inference(fof_simplification,[status(thm)],[help_fequal_2_1_fequal_001t__Option__Ooption_It__Nat__Onat_J_T]) ).
tff(c_0_24,negated_conjecture,
~ ( pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_eq_nat,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_nat_bool(aa_nat_fun_nat_bool(fequal_nat,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),ma)),aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_option_nat_bool(aa_opt7943525813896274546t_bool(fequal_option_nat,vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))),none_nat)),aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,deg),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))))),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))))),the_nat(vEBT_vebt_maxt(nth_VEBT_VEBT(list_u1324408373059187874T_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na),vEBT_vebt_delete(nth_VEBT_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)),aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_low,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na))),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))))))))),ma)))
& pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_nat,aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_nat_bool(aa_nat_fun_nat_bool(fequal_nat,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),ma)),aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_option_nat_bool(aa_opt7943525813896274546t_bool(fequal_option_nat,vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))),none_nat)),aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,deg),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))))),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))))),the_nat(vEBT_vebt_maxt(nth_VEBT_VEBT(list_u1324408373059187874T_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na),vEBT_vebt_delete(nth_VEBT_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)),aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_low,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na))),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))))))))),ma)),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),deg))) ),
inference(assume_negation,[status(cth)],[conj_0]) ).
tff(c_0_25,plain,
! [X20430: nat,X20431: nat] : ( aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,X20430),X20431) = aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,X20431),X20430) ),
inference(variable_rename,[status(thm)],[fact_1729_add_Ocommute]) ).
tcf(c_0_26,plain,
! [X211: bool,X217: bool] :
( ~ pp(X217)
| ( X217 = X211 )
| ( X211 = fFalse ) ),
inference(spm,[status(thm)],[c_0_20,c_0_21]) ).
tff(c_0_27,plain,
! [X20981: nat,X20982: nat] :
( pp(aa_nat_bool(aa_nat_fun_nat_bool(fequal_nat,X20981),X20982))
| ( X20981 != X20982 ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_22])]) ).
tff(c_0_28,plain,
! [X20957: option_nat,X20958: option_nat] :
( pp(aa_option_nat_bool(aa_opt7943525813896274546t_bool(fequal_option_nat,X20957),X20958))
| ( X20957 != X20958 ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_23])]) ).
tff(c_0_29,plain,
! [X20685: nat,X20686: nat] : ( aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_low,X20685),X20686) = aa_nat_nat(aa_nat_fun_nat_nat(modulo_modulo_nat,X20685),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),X20686)) ),
inference(variable_rename,[status(thm)],[fact_2280_low__def]) ).
tff(c_0_30,negated_conjecture,
( ~ pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_eq_nat,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_nat_bool(aa_nat_fun_nat_bool(fequal_nat,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),ma)),aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_option_nat_bool(aa_opt7943525813896274546t_bool(fequal_option_nat,vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))),none_nat)),aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,deg),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))))),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))))),the_nat(vEBT_vebt_maxt(nth_VEBT_VEBT(list_u1324408373059187874T_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na),vEBT_vebt_delete(nth_VEBT_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)),aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_low,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na))),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))))))))),ma)))
| ~ pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_nat,aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_nat_bool(aa_nat_fun_nat_bool(fequal_nat,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),ma)),aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_option_nat_bool(aa_opt7943525813896274546t_bool(fequal_option_nat,vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))),none_nat)),aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,deg),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))))),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))))),the_nat(vEBT_vebt_maxt(nth_VEBT_VEBT(list_u1324408373059187874T_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na),vEBT_vebt_delete(nth_VEBT_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)),aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_low,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na))),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))))))))),ma)),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),deg))) ),
inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_24])]) ).
tcf(c_0_31,plain,
aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx) = ma,
inference(split_conjunct,[status(thm)],[fact_4__092_060open_062summin_A_K_A2_A_094_An_A_L_Alx_A_061_Ama_092_060close_062]) ).
tcf(c_0_32,plain,
! [X3: nat,X2: nat] : aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,X2),X3) = aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,X3),X2),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
tcf(c_0_33,plain,
aa_nat_nat(suc,one_one_nat) = aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one)),
inference(split_conjunct,[status(thm)],[fact_758_Suc__1]) ).
tcf(c_0_34,plain,
aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,deg),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))) = na,
inference(split_conjunct,[status(thm)],[fact_10__C9_C]) ).
tcf(c_0_35,plain,
! [X217: bool,X211: bool] :
( ~ pp(X211)
| ~ pp(X217)
| ( X211 = X217 ) ),
inference(spm,[status(thm)],[c_0_20,c_0_26]) ).
tcf(c_0_36,plain,
pp(fTrue),
inference(split_conjunct,[status(thm)],[help_fTrue_1_1_U]) ).
tcf(c_0_37,plain,
! [X2: nat,X3: nat] :
( ( X2 != X3 )
| pp(aa_nat_bool(aa_nat_fun_nat_bool(fequal_nat,X2),X3)) ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
tcf(c_0_38,plain,
vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na))) = none_nat,
inference(split_conjunct,[status(thm)],[fact_8_True]) ).
tcf(c_0_39,plain,
! [X1013: option_nat,X1027: option_nat] :
( ( X1013 != X1027 )
| pp(aa_option_nat_bool(aa_opt7943525813896274546t_bool(fequal_option_nat,X1013),X1027)) ),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
tff(c_0_40,plain,
! [X23791: nat,X23792: nat,X23793: nat] : ( aa_nat_nat(aa_nat_fun_nat_nat(modulo_modulo_nat,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,X23791),aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,X23792),X23793))),X23793) = aa_nat_nat(aa_nat_fun_nat_nat(modulo_modulo_nat,X23791),X23793) ),
inference(variable_rename,[status(thm)],[fact_2579_mod__mult__self1]) ).
tcf(c_0_41,plain,
! [X2: nat,X3: nat] : aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_low,X2),X3) = aa_nat_nat(aa_nat_fun_nat_nat(modulo_modulo_nat,X2),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),X3)),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
tcf(c_0_42,plain,
pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_nat,ma),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),deg))),
inference(split_conjunct,[status(thm)],[fact_0__C5_Ohyps_C_I8_J]) ).
tff(c_0_43,plain,
! [X20985: nat] : pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_eq_nat,X20985),X20985)),
inference(variable_rename,[status(thm)],[fact_602_le__refl]) ).
tcf(c_0_44,negated_conjecture,
( ~ pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_eq_nat,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_nat_bool(aa_nat_fun_nat_bool(fequal_nat,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),ma)),aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_option_nat_bool(aa_opt7943525813896274546t_bool(fequal_option_nat,vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))),none_nat)),aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,deg),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))))),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))))),the_nat(vEBT_vebt_maxt(nth_VEBT_VEBT(list_u1324408373059187874T_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na),vEBT_vebt_delete(nth_VEBT_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)),aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_low,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na))),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))))))))),ma)))
| ~ pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_nat,aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_nat_bool(aa_nat_fun_nat_bool(fequal_nat,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),ma)),aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_option_nat_bool(aa_opt7943525813896274546t_bool(fequal_option_nat,vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))),none_nat)),aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,deg),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))))),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))))),the_nat(vEBT_vebt_maxt(nth_VEBT_VEBT(list_u1324408373059187874T_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na),vEBT_vebt_delete(nth_VEBT_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)),aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_low,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na))),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),na))),lx)),na)))))))))),ma)),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),deg))) ),
inference(split_conjunct,[status(thm)],[c_0_30]) ).
tcf(c_0_45,plain,
aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,lx),aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_nat_nat(suc,one_one_nat)),na))) = ma,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_31,c_0_32]),c_0_33]) ).
tcf(c_0_46,plain,
aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,deg),aa_nat_nat(suc,one_one_nat)) = na,
inference(rw,[status(thm)],[c_0_34,c_0_33]) ).
tcf(c_0_47,plain,
! [X211: bool] :
( ~ pp(X211)
| ( fTrue = X211 ) ),
inference(spm,[status(thm)],[c_0_35,c_0_36]) ).
tcf(c_0_48,plain,
! [X2: nat] : pp(aa_nat_bool(aa_nat_fun_nat_bool(fequal_nat,X2),X2)),
inference(er,[status(thm)],[c_0_37]) ).
tcf(c_0_49,plain,
vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,summin),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_nat_nat(suc,one_one_nat)),na))),lx)),na))) = none_nat,
inference(rw,[status(thm)],[c_0_38,c_0_33]) ).
tcf(c_0_50,plain,
! [X1013: option_nat] : pp(aa_option_nat_bool(aa_opt7943525813896274546t_bool(fequal_option_nat,X1013),X1013)),
inference(er,[status(thm)],[c_0_39]) ).
tcf(c_0_51,plain,
! [X2: nat,X3: nat,X4: nat] : aa_nat_nat(aa_nat_fun_nat_nat(modulo_modulo_nat,aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,X2),aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,X3),X4))),X4) = aa_nat_nat(aa_nat_fun_nat_nat(modulo_modulo_nat,X2),X4),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
tcf(c_0_52,plain,
! [X2: nat,X3: nat] : aa_nat_nat(aa_nat_fun_nat_nat(modulo_modulo_nat,X2),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_nat_nat(suc,one_one_nat)),X3)) = aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_low,X2),X3),
inference(rw,[status(thm)],[c_0_41,c_0_33]) ).
tff(c_0_53,plain,
! [X20938: nat,X20939: nat] : ( aa_nat_nat(aa_nat_fun_nat_nat(if_nat(fTrue),X20938),X20939) = X20938 ),
inference(variable_rename,[status(thm)],[help_If_1_1_If_001t__Nat__Onat_T]) ).
tcf(c_0_54,plain,
pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_nat,ma),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_nat_nat(suc,one_one_nat)),deg))),
inference(rw,[status(thm)],[c_0_42,c_0_33]) ).
tcf(c_0_55,plain,
! [X2: nat] : pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_eq_nat,X2),X2)),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
tcf(c_0_56,negated_conjecture,
( ~ pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_eq_nat,ma),aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_nat_bool(aa_nat_fun_nat_bool(fequal_nat,ma),ma)),aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_option_nat_bool(aa_opt7943525813896274546t_bool(fequal_option_nat,vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,ma),na)))),none_nat)),ma),aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_nat_nat(suc,one_one_nat)),na)),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,ma),na)))))),the_nat(vEBT_vebt_maxt(nth_VEBT_VEBT(list_u1324408373059187874T_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,ma),na),vEBT_vebt_delete(nth_VEBT_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,ma),na)),aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_low,ma),na))),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,ma),na)))))))))),ma)))
| ~ pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_nat,aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_nat_bool(aa_nat_fun_nat_bool(fequal_nat,ma),ma)),aa_nat_nat(aa_nat_fun_nat_nat(if_nat(aa_option_nat_bool(aa_opt7943525813896274546t_bool(fequal_option_nat,vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,ma),na)))),none_nat)),ma),aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat,aa_nat_nat(aa_nat_fun_nat_nat(times_times_nat,aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_nat_nat(suc,one_one_nat)),na)),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,ma),na)))))),the_nat(vEBT_vebt_maxt(nth_VEBT_VEBT(list_u1324408373059187874T_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,ma),na),vEBT_vebt_delete(nth_VEBT_VEBT(treeList,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,ma),na)),aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_low,ma),na))),the_nat(vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,ma),na)))))))))),ma)),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_nat_nat(suc,one_one_nat)),deg))) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_44,c_0_32]),c_0_33]),c_0_45]),c_0_32]),c_0_33]),c_0_45]),c_0_32]),c_0_33]),c_0_45]),c_0_33]),c_0_33]),c_0_46]),c_0_32]),c_0_33]),c_0_45]),c_0_32]),c_0_33]),c_0_45]),c_0_32]),c_0_33]),c_0_45]),c_0_32]),c_0_33]),c_0_45]),c_0_32]),c_0_33]),c_0_45]),c_0_33]),c_0_32]),c_0_33]),c_0_45]),c_0_32]),c_0_33]),c_0_45]),c_0_32]),c_0_33]),c_0_45]),c_0_32]),c_0_33]),c_0_45]),c_0_33]),c_0_33]),c_0_46]),c_0_32]),c_0_33]),c_0_45]),c_0_32]),c_0_33]),c_0_45]),c_0_32]),c_0_33]),c_0_45]),c_0_32]),c_0_33]),c_0_45]),c_0_32]),c_0_33]),c_0_45]) ).
tcf(c_0_57,plain,
! [X2: nat] : aa_nat_bool(aa_nat_fun_nat_bool(fequal_nat,X2),X2) = fTrue,
inference(spm,[status(thm)],[c_0_47,c_0_48]) ).
tcf(c_0_58,plain,
vEBT_vebt_maxt(vEBT_vebt_delete(summary,aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_high,ma),na))) = none_nat,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_49,c_0_32]),c_0_45]) ).
tcf(c_0_59,plain,
! [X1013: option_nat] : aa_option_nat_bool(aa_opt7943525813896274546t_bool(fequal_option_nat,X1013),X1013) = fTrue,
inference(spm,[status(thm)],[c_0_47,c_0_50]) ).
tcf(c_0_60,plain,
aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_low,ma),na) = aa_nat_nat(aa_nat_fun_nat_nat(vEBT_VEBT_low,lx),na),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51,c_0_45]),c_0_52]),c_0_52]) ).
tcf(c_0_61,plain,
! [X3: nat,X2: nat] : aa_nat_nat(aa_nat_fun_nat_nat(if_nat(fTrue),X2),X3) = X2,
inference(split_conjunct,[status(thm)],[c_0_53]) ).
tcf(c_0_62,plain,
aa_nat_bool(aa_nat_fun_nat_bool(ord_less_nat,ma),aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat,aa_nat_nat(suc,one_one_nat)),deg)) = fTrue,
inference(spm,[status(thm)],[c_0_47,c_0_54]) ).
tcf(c_0_63,plain,
! [X2: nat] : aa_nat_bool(aa_nat_fun_nat_bool(ord_less_eq_nat,X2),X2) = fTrue,
inference(spm,[status(thm)],[c_0_47,c_0_55]) ).
cnf(c_0_64,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_56,c_0_57]),c_0_58]),c_0_59]),c_0_58]),c_0_60]),c_0_58]),c_0_61]),c_0_61]),c_0_62]),c_0_36]),c_0_57]),c_0_58]),c_0_59]),c_0_58]),c_0_60]),c_0_58]),c_0_61]),c_0_61]),c_0_63]),c_0_36])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP267_1 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.06 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.40 % Computer : n007.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Sun Sep 20 22:22:05 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.21/0.46 Running first-order theorem proving
% 0.21/0.46 Running: /export/starexec/sandbox2/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 222.93/35.73 % Version: 3.5.1
% 222.93/35.73 % Preprocessing class: FMLLSMLLSSSNFFN.
% 222.93/35.73 % Scheduled 4 strats onto 8 cores with 299 seconds (2392 total)
% 222.93/35.73 % Starting new_bool_3 with 897s (3) cores
% 222.93/35.73 % Starting new_bool_1 with 897s (3) cores
% 222.93/35.73 % Starting sh5l with 299s (1) cores
% 222.93/35.73 % Starting G-E--_301_C18_F1_URBAN_S5PRR_RG_S0Y with 299s (1) cores
% 222.93/35.73 % new_bool_1 with pid 3711298 completed with status 0
% 222.93/35.73 % Result found by new_bool_1
% 222.93/35.73 % Preprocessing class: FMLLSMLLSSSNFFN.
% 222.93/35.73 % Scheduled 4 strats onto 8 cores with 299 seconds (2392 total)
% 222.93/35.73 % Starting new_bool_3 with 897s (3) cores
% 222.93/35.73 % Starting new_bool_1 with 897s (3) cores
% 222.93/35.73 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 222.93/35.73 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 222.93/35.73 % Search class: FGHSM-SMLM32-DFFFFFNN
% 222.93/35.73 % Scheduled 13 strats onto 3 cores with 896 seconds (896 total)
% 222.93/35.73 % Starting SubtermCWHack with 81s (1) cores
% 222.93/35.73 % Starting new_bool_1 with 90s (1) cores
% 222.93/35.73 % Starting G-E--_008_C45_F1_PI_SE_Q4_CS_SP_S4SI with 68s (1) cores
% 222.93/35.73 % new_bool_1 with pid 3711302 completed with status 0
% 222.93/35.73 % Result found by new_bool_1
% 222.93/35.73 % Preprocessing class: FMLLSMLLSSSNFFN.
% 222.93/35.73 % Scheduled 4 strats onto 8 cores with 299 seconds (2392 total)
% 222.93/35.73 % Starting new_bool_3 with 897s (3) cores
% 222.93/35.73 % Starting new_bool_1 with 897s (3) cores
% 222.93/35.73 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 222.93/35.73 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 222.93/35.73 % Search class: FGHSM-SMLM32-DFFFFFNN
% 222.93/35.73 % Scheduled 13 strats onto 3 cores with 896 seconds (896 total)
% 222.93/35.73 % Starting SubtermCWHack with 81s (1) cores
% 222.93/35.73 % Starting new_bool_1 with 90s (1) cores
% 222.93/35.73 % Preprocessing time : 0.217 s
% 222.93/35.73 % Presaturation interreduction done
% 222.93/35.73
% 222.93/35.73 % Proof found!
% 222.93/35.73 % SZS status Theorem
% 222.93/35.73 % SZS output start CNFRefutation
% See solution above
% 222.93/35.73 % Parsed axioms : 13734
% 222.93/35.73 % Removed by relevancy pruning/SinE : 10192
% 222.93/35.73 % Initial clauses : 9275
% 222.93/35.73 % Removed in clause preprocessing : 1923
% 222.93/35.73 % Initial clauses in saturation : 7352
% 222.93/35.73 % Processed clauses : 47845
% 222.93/35.73 % ...of these trivial : 814
% 222.93/35.73 % ...subsumed : 30238
% 222.93/35.73 % ...remaining for further processing : 16792
% 222.93/35.73 % Other redundant clauses eliminated : 2973
% 222.93/35.73 % Clauses deleted for lack of memory : 0
% 222.93/35.73 % Backward-subsumed : 234
% 222.93/35.73 % Backward-rewritten : 1338
% 222.93/35.73 % Generated clauses : 488941
% 222.93/35.73 % ...of the previous two non-redundant : 455973
% 222.93/35.73 % ...aggressively subsumed : 0
% 222.93/35.73 % Contextual simplify-reflections : 252
% 222.93/35.73 % Paramodulations : 486471
% 222.93/35.73 % Factorizations : 78
% 222.93/35.73 % NegExts : 0
% 222.93/35.73 % Equation resolutions : 3089
% 222.93/35.73 % Disequality decompositions : 0
% 222.93/35.73 % Total rewrite steps : 204389
% 222.93/35.73 % ...of those cached : 188892
% 222.93/35.73 % Propositional unsat checks : 4
% 222.93/35.73 % Propositional check models : 2
% 222.93/35.73 % Propositional check unsatisfiable : 0
% 222.93/35.73 % Propositional clauses : 0
% 222.93/35.73 % Propositional clauses after purity: 0
% 222.93/35.73 % Propositional unsat core size : 0
% 222.93/35.73 % Propositional preprocessing time : 0.000
% 222.93/35.73 % Propositional encoding time : 0.976
% 222.93/35.73 % Propositional solver time : 0.352
% 222.93/35.73 % Success case prop preproc time : 0.000
% 222.93/35.73 % Success case prop encoding time : 0.000
% 222.93/35.73 % Success case prop solver time : 0.000
% 222.93/35.73 % Current number of processed clauses : 8959
% 222.93/35.73 % Positive orientable unit clauses : 1523
% 222.93/35.73 % Positive unorientable unit clauses: 41
% 222.93/35.73 % Negative unit clauses : 1924
% 222.93/35.73 % Non-unit-clauses : 5471
% 222.93/35.73 % Current number of unprocessed clauses: 415847
% 222.93/35.73 % ...number of literals in the above : 1589325
% 222.93/35.73 % Current number of archived formulas : 0
% 222.93/35.73 % Current number of archived clauses : 6579
% 222.93/35.73 % Clause-clause subsumption calls (NU) : 32925482
% 222.93/35.73 % Rec. Clause-clause subsumption calls : 3530010
% 222.93/35.73 % Non-unit clause-clause subsumptions : 10745
% 222.93/35.73 % Unit Clause-clause subsumption calls : 607117
% 222.93/35.73 % Rewrite failures with RHS unbound : 0
% 222.93/35.73 % BW rewrite match attempts : 29860
% 222.93/35.73 % BW rewrite match successes : 1534
% 222.93/35.73 % Condensation attempts : 0
% 222.93/35.73 % Condensation successes : 0
% 222.93/35.73 % Termbank termtop insertions : 17211473
% 222.93/35.73 % Search garbage collected termcells : 197884
% 222.93/35.73
% 222.93/35.73 % -------------------------------------------------
% 222.93/35.73 % User time : 32.271 s
% 222.93/35.73 % System time : 0.552 s
% 222.93/35.73 % Total time : 32.823 s
% 222.93/35.73 % Maximum resident set size: 55016 pages
% 222.93/35.73
% 222.93/35.73 % -------------------------------------------------
% 222.93/35.73 % User time : 95.094 s
% 222.93/35.73 % System time : 1.644 s
% 222.93/35.73 % Total time : 96.738 s
% 222.93/35.73 % Maximum resident set size: 33280 pages
% 222.93/35.73 % E exiting
%------------------------------------------------------------------------------