%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : NUM925_4 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n010.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 01:51:02 PM UTC 2026
% Result : Theorem 0.17s 11.50s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 17
% Syntax : Number of formulae : 71 ( 42 unt; 0 typ; 0 def)
% Number of atoms : 113 ( 79 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 81 ( 39 ~; 27 |; 7 &)
% ( 5 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 14 ( 13 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 17 con; 0-2 aty)
% Number of variables : 77 ( 0 sgn 75 !; 2 ?; 77 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
int: $tType ).
tff(decl_sort2,type,
fun_int_int: $tType ).
tff(decl_sort3,type,
fun_int_bool: $tType ).
tff(decl_sort4,type,
fun_nat_nat: $tType ).
tff(decl_sort5,type,
fun_nat_bool: $tType ).
tff(decl_sort6,type,
nat: $tType ).
tff(decl_sort7,type,
fun_int_fun_int_bool: $tType ).
tff(decl_sort8,type,
fun_int_nat: $tType ).
tff(decl_sort9,type,
bool: $tType ).
tff(decl_sort10,type,
fun_int_fun_int_int: $tType ).
tff(decl_sort11,type,
fun_nat_int: $tType ).
tff(decl_sort12,type,
fun_nat_fun_nat_bool: $tType ).
tff(decl_sort13,type,
fun_int_fun_nat_int: $tType ).
tff(decl_299,type,
one_one_int: int ).
tff(decl_306,type,
plus_plus_int: fun_int_fun_int_int ).
tff(decl_317,type,
times_times_int: fun_int_fun_int_int ).
tff(decl_328,type,
zero_zero_int: int ).
tff(decl_329,type,
zero_zero_nat: nat ).
tff(decl_351,type,
bit0: fun_int_int ).
tff(decl_352,type,
bit1: fun_int_int ).
tff(decl_354,type,
pls: int ).
tff(decl_363,type,
number_number_of_int: fun_int_int ).
tff(decl_364,type,
number_number_of_nat: fun_int_nat ).
tff(decl_392,type,
suc: fun_nat_nat ).
tff(decl_398,type,
semiri1621563631at_int: fun_nat_int ).
tff(decl_424,type,
ord_less_int: fun_int_fun_int_bool ).
tff(decl_425,type,
ord_less_nat: fun_nat_fun_nat_bool ).
tff(decl_433,type,
ord_less_eq_int: fun_int_fun_int_bool ).
tff(decl_446,type,
power_power_int: fun_int_fun_nat_int ).
tff(decl_607,type,
hAPP_int_bool: ( int * fun_int_bool ) > bool ).
tff(decl_608,type,
hAPP_int_int: ( int * fun_int_int ) > int ).
tff(decl_609,type,
hAPP_int_nat: ( int * fun_int_nat ) > nat ).
tff(decl_614,type,
hAPP_i1948725293t_bool: ( int * fun_int_fun_int_bool ) > fun_int_bool ).
tff(decl_615,type,
hAPP_int_fun_int_int: ( int * fun_int_fun_int_int ) > fun_int_int ).
tff(decl_624,type,
hAPP_int_fun_nat_int: ( int * fun_int_fun_nat_int ) > fun_nat_int ).
tff(decl_648,type,
hAPP_nat_bool: ( nat * fun_nat_bool ) > bool ).
tff(decl_649,type,
hAPP_nat_int: ( nat * fun_nat_int ) > int ).
tff(decl_650,type,
hAPP_nat_nat: ( nat * fun_nat_nat ) > nat ).
tff(decl_656,type,
hAPP_n1699378549t_bool: ( nat * fun_nat_fun_nat_bool ) > fun_nat_bool ).
tff(decl_1085,type,
hBOOL: bool > $o ).
tff(decl_1095,type,
n: nat ).
tff(decl_1108,type,
esk3_1: int > nat ).
tff(decl_1113,type,
esk8_2: ( int * int ) > nat ).
tff(fact_158_zadd__0,axiom,
! [X28: int] : ( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,zero_zero_int),X28) = X28 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_158_zadd__0) ).
tff(fact_738_zle__iff__zadd,axiom,
! [X44: int,X63: int] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X44),X63))
<=> ? [X314: nat] : ( X63 = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,X44),hAPP_nat_int(semiri1621563631at_int,X314)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_738_zle__iff__zadd) ).
tff(fact_206_number__of__int,axiom,
! [X118: nat] : ( hAPP_int_int(number_number_of_int,hAPP_nat_int(semiri1621563631at_int,X118)) = hAPP_nat_int(semiri1621563631at_int,X118) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_number__of__int) ).
tff(fact_103_int__int__eq,axiom,
! [X56: nat,X29: nat] :
( ( hAPP_nat_int(semiri1621563631at_int,X56) = hAPP_nat_int(semiri1621563631at_int,X29) )
<=> ( X56 = X29 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_int__int__eq) ).
tff(fact_718_of__nat__0__le__iff,axiom,
! [X743: nat] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_nat_int(semiri1621563631at_int,X743))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_718_of__nat__0__le__iff) ).
tff(fact_87_eq__number__of,axiom,
! [X42: int,X43: int] :
( ( hAPP_int_int(number_number_of_int,X42) = hAPP_int_int(number_number_of_int,X43) )
<=> ( X42 = X43 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_eq__number__of) ).
tff(fact_3103_int__Suc0__eq__1,axiom,
hAPP_nat_int(semiri1621563631at_int,hAPP_nat_nat(suc,zero_zero_nat)) = one_one_int,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3103_int__Suc0__eq__1) ).
tff(fact_473_zero__less__imp__eq__int,axiom,
! [X32: int] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X32))
=> ? [X314: nat] :
( ( X32 = hAPP_nat_int(semiri1621563631at_int,X314) )
& hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),X314)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_473_zero__less__imp__eq__int) ).
tff(fact_3105_int__Suc,axiom,
! [X26: nat] : ( hAPP_nat_int(semiri1621563631at_int,hAPP_nat_nat(suc,X26)) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,X26)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3105_int__Suc) ).
tff(fact_770_int__one__le__iff__zero__less,axiom,
! [X63: int] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),X63))
<=> hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X63)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_770_int__one__le__iff__zero__less) ).
tff(fact_51_semiring__norm_I110_J,axiom,
one_one_int = hAPP_int_int(number_number_of_int,hAPP_int_int(bit1,pls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_semiring__norm_I110_J) ).
tff(fact_151_Pls__def,axiom,
pls = zero_zero_int,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_151_Pls__def) ).
tff(fact_347_field__power__not__zero,axiom,
! [X213: nat,X217: int] :
( ( X217 != zero_zero_int )
=> ( hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X217),X213) != zero_zero_int ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_347_field__power__not__zero) ).
tff(fact_1907_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J,axiom,
! [X3126: int] : ( hAPP_int_int(hAPP_int_fun_int_int(times_times_int,X3126),X3126) = hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X3126),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1907_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J) ).
tff(conj_0,conjecture,
hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))) != zero_zero_int,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
tff(fact_71_int__eq__0__conv,axiom,
! [X29: nat] :
( ( hAPP_nat_int(semiri1621563631at_int,X29) = zero_zero_int )
<=> ( X29 = zero_zero_nat ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_int__eq__0__conv) ).
tff(fact_276_less__not__refl,axiom,
! [X27: nat] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X27),X27)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_276_less__not__refl) ).
tff(c_0_17,plain,
! [X8322: int] : ( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,zero_zero_int),X8322) = X8322 ),
inference(variable_rename,[status(thm)],[fact_158_zadd__0]) ).
tff(c_0_18,plain,
! [X8197: int,X8198: int,X8200: int,X8201: int,X8202: nat] :
( ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X8200),X8201))
| ( X8201 != hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,X8200),hAPP_nat_int(semiri1621563631at_int,X8202)) ) )
& ( ( X8198 = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,X8197),hAPP_nat_int(semiri1621563631at_int,esk8_2(X8197,X8198))) )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X8197),X8198)) ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_738_zle__iff__zadd])])])])])]) ).
tff(c_0_19,plain,
! [X8155: nat] : ( hAPP_int_int(number_number_of_int,hAPP_nat_int(semiri1621563631at_int,X8155)) = hAPP_nat_int(semiri1621563631at_int,X8155) ),
inference(variable_rename,[status(thm)],[fact_206_number__of__int]) ).
tff(c_0_20,plain,
! [X8152: nat,X8153: nat] :
( ( ( hAPP_nat_int(semiri1621563631at_int,X8152) = hAPP_nat_int(semiri1621563631at_int,X8153) )
| ( X8152 != X8153 ) )
& ( ( X8152 = X8153 )
| ( hAPP_nat_int(semiri1621563631at_int,X8152) != hAPP_nat_int(semiri1621563631at_int,X8153) ) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_103_int__int__eq])])]) ).
tcf(c_0_21,plain,
! [X5: int] : hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,zero_zero_int),X5) = X5,
inference(split_conjunct,[status(thm)],[c_0_17]) ).
tcf(c_0_22,plain,
! [X5: int,X6: int] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X5),X6))
| ( X6 = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,X5),hAPP_nat_int(semiri1621563631at_int,esk8_2(X5,X6))) ) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
tff(c_0_23,plain,
! [X8181: nat] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_nat_int(semiri1621563631at_int,X8181))),
inference(variable_rename,[status(thm)],[fact_718_of__nat__0__le__iff]) ).
tff(c_0_24,plain,
! [X8945: int,X8946: int] :
( ( ( hAPP_int_int(number_number_of_int,X8945) = hAPP_int_int(number_number_of_int,X8946) )
| ( X8945 != X8946 ) )
& ( ( X8945 = X8946 )
| ( hAPP_int_int(number_number_of_int,X8945) != hAPP_int_int(number_number_of_int,X8946) ) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_87_eq__number__of])])]) ).
tcf(c_0_25,plain,
! [X26: nat] : hAPP_int_int(number_number_of_int,hAPP_nat_int(semiri1621563631at_int,X26)) = hAPP_nat_int(semiri1621563631at_int,X26),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
tcf(c_0_26,plain,
hAPP_nat_int(semiri1621563631at_int,hAPP_nat_nat(suc,zero_zero_nat)) = one_one_int,
inference(split_conjunct,[status(thm)],[fact_3103_int__Suc0__eq__1]) ).
tcf(c_0_27,plain,
! [X26: nat,X27: nat] :
( ( hAPP_nat_int(semiri1621563631at_int,X26) != hAPP_nat_int(semiri1621563631at_int,X27) )
| ( X26 = X27 ) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
tcf(c_0_28,plain,
! [X5: int] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),X5))
| ( hAPP_nat_int(semiri1621563631at_int,esk8_2(zero_zero_int,X5)) = X5 ) ),
inference(spm,[status(thm)],[c_0_21,c_0_22]) ).
tcf(c_0_29,plain,
! [X26: nat] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_nat_int(semiri1621563631at_int,X26))),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
tff(c_0_30,plain,
! [X8177: int] :
( ( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X8177))
| ( X8177 = hAPP_nat_int(semiri1621563631at_int,esk3_1(X8177)) ) )
& ( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X8177))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),esk3_1(X8177))) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_473_zero__less__imp__eq__int])])])])]) ).
tff(c_0_31,plain,
! [X8233: nat] : ( hAPP_nat_int(semiri1621563631at_int,hAPP_nat_nat(suc,X8233)) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,X8233)) ),
inference(variable_rename,[status(thm)],[fact_3105_int__Suc]) ).
tff(c_0_32,plain,
! [X8253: int] :
( ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),X8253))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X8253)) )
& ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X8253))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),X8253)) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_770_int__one__le__iff__zero__less])])]) ).
tcf(c_0_33,plain,
! [X5: int,X6: int,X26: nat] :
( ( X5 != hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,X6),hAPP_nat_int(semiri1621563631at_int,X26)) )
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X6),X5)) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
tcf(c_0_34,plain,
! [X5: int,X6: int] :
( ( hAPP_int_int(number_number_of_int,X5) != hAPP_int_int(number_number_of_int,X6) )
| ( X5 = X6 ) ),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
tcf(c_0_35,plain,
hAPP_int_int(number_number_of_int,one_one_int) = one_one_int,
inference(spm,[status(thm)],[c_0_25,c_0_26]) ).
tcf(c_0_36,plain,
one_one_int = hAPP_int_int(number_number_of_int,hAPP_int_int(bit1,pls)),
inference(split_conjunct,[status(thm)],[fact_51_semiring__norm_I110_J]) ).
tcf(c_0_37,plain,
pls = zero_zero_int,
inference(split_conjunct,[status(thm)],[fact_151_Pls__def]) ).
tcf(c_0_38,plain,
! [X26: nat] : esk8_2(zero_zero_int,hAPP_nat_int(semiri1621563631at_int,X26)) = X26,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_27,c_0_28])]),c_0_29])]) ).
tcf(c_0_39,plain,
! [X5: int] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X5))
| ( X5 = hAPP_nat_int(semiri1621563631at_int,esk3_1(X5)) ) ),
inference(split_conjunct,[status(thm)],[c_0_30]) ).
tcf(c_0_40,plain,
! [X26: nat] : hAPP_nat_int(semiri1621563631at_int,hAPP_nat_nat(suc,X26)) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,X26)),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
tcf(c_0_41,plain,
! [X5: int] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),X5))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X5)) ),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
tcf(c_0_42,plain,
! [X5: int,X26: nat] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X5),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,X5),hAPP_nat_int(semiri1621563631at_int,X26)))),
inference(er,[status(thm)],[c_0_33]) ).
tff(c_0_43,plain,
! [X213: nat,X217: int] :
( ( X217 != zero_zero_int )
=> ( hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X217),X213) != zero_zero_int ) ),
inference(fof_simplification,[status(thm)],[fact_347_field__power__not__zero]) ).
tff(c_0_44,plain,
! [X8108: int] : ( hAPP_int_int(hAPP_int_fun_int_int(times_times_int,X8108),X8108) = hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X8108),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))) ),
inference(variable_rename,[status(thm)],[fact_1907_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J]) ).
tcf(c_0_45,plain,
! [X5: int] :
( ( hAPP_int_int(number_number_of_int,X5) != one_one_int )
| ( X5 = one_one_int ) ),
inference(spm,[status(thm)],[c_0_34,c_0_35]) ).
tcf(c_0_46,plain,
hAPP_int_int(number_number_of_int,hAPP_int_int(bit1,zero_zero_int)) = one_one_int,
inference(rw,[status(thm)],[c_0_36,c_0_37]) ).
tff(c_0_47,negated_conjecture,
~ ( ( hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))) != zero_zero_int ) ),
inference(assume_negation,[status(cth)],[conj_0]) ).
tcf(c_0_48,plain,
! [X5: int] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X5))
| ( esk8_2(zero_zero_int,X5) = esk3_1(X5) ) ),
inference(spm,[status(thm)],[c_0_38,c_0_39]) ).
tcf(c_0_49,plain,
! [X26: nat] : esk8_2(zero_zero_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,X26))) = hAPP_nat_nat(suc,X26),
inference(spm,[status(thm)],[c_0_38,c_0_40]) ).
tcf(c_0_50,plain,
! [X26: nat] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,X26)))),
inference(spm,[status(thm)],[c_0_41,c_0_42]) ).
tff(c_0_51,plain,
! [X8151: nat] :
( ( ( hAPP_nat_int(semiri1621563631at_int,X8151) = zero_zero_int )
| ( X8151 != zero_zero_nat ) )
& ( ( X8151 = zero_zero_nat )
| ( hAPP_nat_int(semiri1621563631at_int,X8151) != zero_zero_int ) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_71_int__eq__0__conv])])]) ).
tff(c_0_52,plain,
! [X27: nat] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X27),X27)),
inference(fof_simplification,[status(thm)],[fact_276_less__not__refl]) ).
tff(c_0_53,plain,
! [X8013: nat,X8014: int] :
( ( hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X8014),X8013) != zero_zero_int )
| ( X8014 = zero_zero_int ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_43])])]) ).
tcf(c_0_54,plain,
! [X5: int] : hAPP_int_int(hAPP_int_fun_int_int(times_times_int,X5),X5) = hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X5),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
tcf(c_0_55,plain,
hAPP_int_int(bit1,zero_zero_int) = one_one_int,
inference(spm,[status(thm)],[c_0_45,c_0_46]) ).
tff(c_0_56,negated_conjecture,
hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))) = zero_zero_int,
inference(fof_simplification,[status(thm)],[c_0_47]) ).
tcf(c_0_57,plain,
! [X5: int] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X5))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),esk3_1(X5))) ),
inference(split_conjunct,[status(thm)],[c_0_30]) ).
tcf(c_0_58,plain,
! [X26: nat] : esk3_1(hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,X26))) = hAPP_nat_nat(suc,X26),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48,c_0_49]),c_0_50])]) ).
tcf(c_0_59,plain,
! [X26: nat] :
( ( hAPP_nat_int(semiri1621563631at_int,X26) != zero_zero_int )
| ( X26 = zero_zero_nat ) ),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
tff(c_0_60,plain,
! [X8762: nat] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X8762),X8762)),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_52])]) ).
tcf(c_0_61,plain,
! [X5: int,X26: nat] :
( ( hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X5),X26) != zero_zero_int )
| ( X5 = zero_zero_int ) ),
inference(split_conjunct,[status(thm)],[c_0_53]) ).
tcf(c_0_62,plain,
! [X5: int] : hAPP_int_int(hAPP_int_fun_int_int(times_times_int,X5),X5) = hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X5),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,one_one_int))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_54,c_0_37]),c_0_55]) ).
tcf(c_0_63,negated_conjecture,
hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))) = zero_zero_int,
inference(split_conjunct,[status(thm)],[c_0_56]) ).
tcf(c_0_64,plain,
! [X26: nat] : hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),hAPP_nat_nat(suc,X26))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57,c_0_58]),c_0_50])]) ).
tcf(c_0_65,plain,
! [X26: nat] :
( ( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,X26)) != zero_zero_int )
| ( hAPP_nat_nat(suc,X26) = zero_zero_nat ) ),
inference(spm,[status(thm)],[c_0_59,c_0_40]) ).
tcf(c_0_66,plain,
! [X26: nat] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X26),X26)),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
tcf(c_0_67,plain,
! [X5: int] :
( ( hAPP_int_int(hAPP_int_fun_int_int(times_times_int,X5),X5) != zero_zero_int )
| ( X5 = zero_zero_int ) ),
inference(spm,[status(thm)],[c_0_61,c_0_62]) ).
tcf(c_0_68,negated_conjecture,
hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n))) = zero_zero_int,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_63,c_0_37]),c_0_55]),c_0_62]) ).
tcf(c_0_69,plain,
! [X26: nat] : hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,X26)) != zero_zero_int,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_64,c_0_65]),c_0_66]) ).
cnf(c_0_70,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_67,c_0_68]),c_0_69]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM925_4 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/10.60 % Computer : n010.cluster.edu
% 0.10/10.60 % Model : x86_64 x86_64
% 0.10/10.60 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.60 % Memory : 8046.5625MB
% 0.10/10.60 % OS : Linux 6.8.0-71-generic
% 0.10/10.60 % CPULimit : 300
% 0.10/10.60 % WCLimit : 300
% 0.10/10.60 % DateTime : Mon Sep 21 03:17:55 UTC 2026
% 0.10/10.60 % CPUTime :
% 0.10/10.60 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/10.64 Running first-order theorem proving
% 0.10/10.65 Running: /export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p
% 0.17/11.50 % Version: 3.5.1
% 0.17/11.50 % Preprocessing class: FMLLSMLLSSSNFFN.
% 0.17/11.50 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.17/11.50 % Starting new_bool_3 with 900s (3) cores
% 0.17/11.50 % Starting new_bool_1 with 900s (3) cores
% 0.17/11.50 % Starting sh5l with 300s (1) cores
% 0.17/11.50 % Starting G-E--_301_C18_F1_URBAN_S5PRR_RG_S0Y with 300s (1) cores
% 0.17/11.50 % G-E--_301_C18_F1_URBAN_S5PRR_RG_S0Y with pid 4116309 completed with status 0
% 0.17/11.50 % Result found by G-E--_301_C18_F1_URBAN_S5PRR_RG_S0Y
% 0.17/11.50 % Preprocessing class: FMLLSMLLSSSNFFN.
% 0.17/11.50 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.17/11.50 % Starting new_bool_3 with 900s (3) cores
% 0.17/11.50 % Starting new_bool_1 with 900s (3) cores
% 0.17/11.50 % Starting sh5l with 300s (1) cores
% 0.17/11.50 % Starting G-E--_301_C18_F1_URBAN_S5PRR_RG_S0Y with 300s (1) cores
% 0.17/11.50 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.17/11.50 % SinE strategy is gf120_h_gu_RUU_F100_L00500
% 0.17/11.50 % Search class: FGHSM-FSLM31-DFFFFFNN
% 0.17/11.50 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.17/11.50 % Starting SubtermCWHack with 28s (1) cores
% 0.17/11.50 % SubtermCWHack with pid 4116310 completed with status 0
% 0.17/11.50 % Result found by SubtermCWHack
% 0.17/11.50 % Preprocessing class: FMLLSMLLSSSNFFN.
% 0.17/11.50 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.17/11.50 % Starting new_bool_3 with 900s (3) cores
% 0.17/11.50 % Starting new_bool_1 with 900s (3) cores
% 0.17/11.50 % Starting sh5l with 300s (1) cores
% 0.17/11.50 % Starting G-E--_301_C18_F1_URBAN_S5PRR_RG_S0Y with 300s (1) cores
% 0.17/11.50 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.17/11.50 % SinE strategy is gf120_h_gu_RUU_F100_L00500
% 0.17/11.50 % Search class: FGHSM-FSLM31-DFFFFFNN
% 0.17/11.50 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.17/11.50 % Starting SubtermCWHack with 28s (1) cores
% 0.17/11.50 % Preprocessing time : 0.018 s
% 0.17/11.50
% 0.17/11.50 % Proof found!
% 0.17/11.50 % SZS status Theorem
% 0.17/11.50 % SZS output start CNFRefutation
% See solution above
% 0.17/11.51 % Parsed axioms : 7028
% 0.17/11.51 % Removed by relevancy pruning/SinE : 6527
% 0.17/11.51 % Initial clauses : 716
% 0.17/11.51 % Removed in clause preprocessing : 68
% 0.17/11.51 % Initial clauses in saturation : 648
% 0.17/11.51 % Processed clauses : 2310
% 0.17/11.51 % ...of these trivial : 121
% 0.17/11.51 % ...subsumed : 1573
% 0.17/11.51 % ...remaining for further processing : 616
% 0.17/11.51 % Other redundant clauses eliminated : 114
% 0.17/11.51 % Clauses deleted for lack of memory : 0
% 0.17/11.51 % Backward-subsumed : 20
% 0.17/11.51 % Backward-rewritten : 22
% 0.17/11.51 % Generated clauses : 6442
% 0.17/11.51 % ...of the previous two non-redundant : 4965
% 0.17/11.51 % ...aggressively subsumed : 0
% 0.17/11.51 % Contextual simplify-reflections : 2
% 0.17/11.51 % Paramodulations : 6318
% 0.17/11.51 % Factorizations : 6
% 0.17/11.51 % NegExts : 0
% 0.17/11.51 % Equation resolutions : 121
% 0.17/11.51 % Disequality decompositions : 0
% 0.17/11.51 % Total rewrite steps : 3288
% 0.17/11.51 % ...of those cached : 3022
% 0.17/11.51 % Propositional unsat checks : 0
% 0.17/11.51 % Propositional check models : 0
% 0.17/11.51 % Propositional check unsatisfiable : 0
% 0.17/11.51 % Propositional clauses : 0
% 0.17/11.51 % Propositional clauses after purity: 0
% 0.17/11.51 % Propositional unsat core size : 0
% 0.17/11.51 % Propositional preprocessing time : 0.000
% 0.17/11.51 % Propositional encoding time : 0.000
% 0.17/11.51 % Propositional solver time : 0.000
% 0.17/11.51 % Success case prop preproc time : 0.000
% 0.17/11.51 % Success case prop encoding time : 0.000
% 0.17/11.51 % Success case prop solver time : 0.000
% 0.17/11.51 % Current number of processed clauses : 528
% 0.17/11.51 % Positive orientable unit clauses : 148
% 0.17/11.51 % Positive unorientable unit clauses: 6
% 0.17/11.51 % Negative unit clauses : 110
% 0.17/11.51 % Non-unit-clauses : 264
% 0.17/11.51 % Current number of unprocessed clauses: 3235
% 0.17/11.51 % ...number of literals in the above : 7224
% 0.17/11.51 % Current number of archived formulas : 0
% 0.17/11.51 % Current number of archived clauses : 42
% 0.17/11.51 % Clause-clause subsumption calls (NU) : 8868
% 0.17/11.51 % Rec. Clause-clause subsumption calls : 8247
% 0.17/11.51 % Non-unit clause-clause subsumptions : 478
% 0.17/11.51 % Unit Clause-clause subsumption calls : 1353
% 0.17/11.51 % Rewrite failures with RHS unbound : 0
% 0.17/11.51 % BW rewrite match attempts : 1231
% 0.17/11.51 % BW rewrite match successes : 34
% 0.17/11.51 % Condensation attempts : 0
% 0.17/11.51 % Condensation successes : 0
% 0.17/11.51 % Termbank termtop insertions : 258235
% 0.17/11.51 % Search garbage collected termcells : 66443
% 0.17/11.51
% 0.17/11.51 % -------------------------------------------------
% 0.17/11.51 % User time : 0.280 s
% 0.17/11.51 % System time : 0.046 s
% 0.17/11.51 % Total time : 0.326 s
% 0.17/11.51 % Maximum resident set size: 18760 pages
% 0.17/11.51
% 0.17/11.51 % -------------------------------------------------
% 0.17/11.51 % User time : 0.764 s
% 0.17/11.51 % System time : 0.079 s
% 0.17/11.51 % Total time : 0.843 s
% 0.17/11.51 % Maximum resident set size: 17664 pages
% 0.17/11.51 % E exiting
%------------------------------------------------------------------------------