%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : NUM924+7 : 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 : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:51:00 PM UTC 2026
% Result : Theorem 4.96s 1.50s
% Output : CNFRefutation 5.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 22
% Syntax : Number of formulae : 76 ( 70 unt; 0 def)
% Number of atoms : 82 ( 65 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 15 ( 9 ~; 4 |; 0 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 8 con; 0-4 aty)
% Number of variables : 72 ( 2 sgn 42 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(tsy_c_Int_OBit1_res,hypothesis,
! [X4] : ti(int,bit1(X4)) = bit1(X4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tsy_c_Int_OBit1_res) ).
fof(fact_22_number__of__is__id,axiom,
! [X15] : number_number_of(int,X15) = ti(int,X15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_number__of__is__id) ).
fof(tsy_c_Int_OBit0_res,hypothesis,
! [X4] : ti(int,bit0(X4)) = bit0(X4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tsy_c_Int_OBit0_res) ).
fof(fact_132_Bit0__def,axiom,
! [X15] : bit0(X15) = hAPP(int,int,plus_plus(int,X15),X15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_132_Bit0__def) ).
fof(fact_139_mult__2,axiom,
! [X3] :
( number_ring(X3)
=> ! [X16] : hAPP(X3,X3,times_times(X3,number_number_of(X3,bit0(bit1(pls)))),X16) = hAPP(X3,X3,plus_plus(X3,X16),X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_mult__2) ).
fof(fact_141_mult__2__right,axiom,
! [X3] :
( number_ring(X3)
=> ! [X16] : hAPP(X3,X3,times_times(X3,X16),number_number_of(X3,bit0(bit1(pls)))) = hAPP(X3,X3,plus_plus(X3,X16),X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_mult__2__right) ).
fof(tsy_c_Int_OBit0_arg1,hypothesis,
! [X4] : bit0(ti(int,X4)) = bit0(X4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tsy_c_Int_OBit0_arg1) ).
fof(conj_0,conjecture,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int))),zero_zero(int))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(tsy_c_Int_OMin_res,axiom,
ti(int,min) = min,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tsy_c_Int_OMin_res) ).
fof(fact_111_one__is__num__one,axiom,
one_one(int) = number_number_of(int,bit1(pls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_111_one__is__num__one) ).
fof(fact_98_zadd__commute,axiom,
! [X16,X12] : hAPP(int,int,plus_plus(int,X16),X12) = hAPP(int,int,plus_plus(int,X12),X16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_zadd__commute) ).
fof(fact_63_mult__Bit0,axiom,
! [X15,X32] : hAPP(int,int,times_times(int,bit0(X15)),X32) = bit0(hAPP(int,int,times_times(int,X15),X32)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_mult__Bit0) ).
fof(arity_Int_Oint___Int_Onumber__ring,axiom,
number_ring(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Int_Onumber__ring) ).
fof(fact_129_add__Pls__right,axiom,
! [X15] : hAPP(int,int,plus_plus(int,X15),pls) = ti(int,X15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_129_add__Pls__right) ).
fof(fact_67_plus__numeral__code_I9_J,axiom,
! [X13,X12] : hAPP(int,int,plus_plus(int,number_number_of(int,X13)),number_number_of(int,X12)) = number_number_of(int,hAPP(int,int,plus_plus(int,X13),X12)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_plus__numeral__code_I9_J) ).
fof(fact_466__096s_A_094_A2_A_N_A_N1_A_061_As_A_094_A2_A_L_A1_096,axiom,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),number_number_of(int,min)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_466__096s_A_094_A2_A_N_A_N1_A_061_As_A_094_A2_A_L_A1_096) ).
fof(fact_162_add__Bit0__Bit1,axiom,
! [X15,X32] : hAPP(int,int,plus_plus(int,bit0(X15)),bit1(X32)) = bit1(hAPP(int,int,plus_plus(int,X15),X32)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_162_add__Bit0__Bit1) ).
fof(fact_23_zmult__commute,axiom,
! [X16,X12] : hAPP(int,int,times_times(int,X16),X12) = hAPP(int,int,times_times(int,X12),X16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_zmult__commute) ).
fof(fact_62_mult__Pls,axiom,
! [X12] : hAPP(int,int,times_times(int,pls),X12) = pls,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_mult__Pls) ).
fof(fact_3_t,axiom,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_t) ).
fof(fact_122_Pls__def,axiom,
pls = zero_zero(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_122_Pls__def) ).
fof(fact_2__096_I4_A_K_Am_A_L_A1_J_A_K_At_A_060_A_I4_A_K_Am_A_L_A1_J_A_K_A0_096,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2__096_I4_A_K_Am_A_L_A1_J_A_K_At_A_060_A_I4_A_K_Am_A_L_A1_J_A_K_A0_096) ).
fof(c_0_22,hypothesis,
! [X106] : ti(int,bit1(X106)) = bit1(X106),
inference(variable_rename,[status(thm)],[tsy_c_Int_OBit1_res]) ).
fof(c_0_23,plain,
! [X198] : number_number_of(int,X198) = ti(int,X198),
inference(variable_rename,[status(thm)],[fact_22_number__of__is__id]) ).
fof(c_0_24,hypothesis,
! [X104] : ti(int,bit0(X104)) = bit0(X104),
inference(variable_rename,[status(thm)],[tsy_c_Int_OBit0_res]) ).
cnf(c_0_25,hypothesis,
ti(int,bit1(X1)) = bit1(X1),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_26,plain,
number_number_of(int,X1) = ti(int,X1),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
fof(c_0_27,plain,
! [X144] : bit0(X144) = hAPP(int,int,plus_plus(int,X144),X144),
inference(variable_rename,[status(thm)],[fact_132_Bit0__def]) ).
fof(c_0_28,plain,
! [X1421,X1422] :
( hAPP(X1421,X1421,times_times(X1421,number_number_of(X1421,bit0(bit1(pls)))),X1422) = hAPP(X1421,X1421,plus_plus(X1421,X1422),X1422)
| ~ number_ring(X1421) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_139_mult__2])])])]) ).
cnf(c_0_29,hypothesis,
ti(int,bit0(X1)) = bit0(X1),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
fof(c_0_30,plain,
! [X1423,X1424] :
( hAPP(X1423,X1423,times_times(X1423,X1424),number_number_of(X1423,bit0(bit1(pls)))) = hAPP(X1423,X1423,plus_plus(X1423,X1424),X1424)
| ~ number_ring(X1423) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_141_mult__2__right])])])]) ).
fof(c_0_31,hypothesis,
! [X103] : bit0(ti(int,X103)) = bit0(X103),
inference(variable_rename,[status(thm)],[tsy_c_Int_OBit0_arg1]) ).
fof(c_0_32,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int))),zero_zero(int))),
inference(assume_negation,[status(cth)],[conj_0]) ).
cnf(c_0_33,plain,
ti(int,min) = min,
inference(split_conjunct,[status(thm)],[tsy_c_Int_OMin_res]) ).
cnf(c_0_34,plain,
one_one(int) = number_number_of(int,bit1(pls)),
inference(split_conjunct,[status(thm)],[fact_111_one__is__num__one]) ).
cnf(c_0_35,hypothesis,
number_number_of(int,bit1(X1)) = bit1(X1),
inference(rw,[status(thm)],[c_0_25,c_0_26]) ).
fof(c_0_36,plain,
! [X471,X472] : hAPP(int,int,plus_plus(int,X471),X472) = hAPP(int,int,plus_plus(int,X472),X471),
inference(variable_rename,[status(thm)],[fact_98_zadd__commute]) ).
fof(c_0_37,plain,
! [X118,X119] : hAPP(int,int,times_times(int,bit0(X118)),X119) = bit0(hAPP(int,int,times_times(int,X118),X119)),
inference(variable_rename,[status(thm)],[fact_63_mult__Bit0]) ).
cnf(c_0_38,plain,
bit0(X1) = hAPP(int,int,plus_plus(int,X1),X1),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_39,plain,
( ~ number_ring(X1)
| hAPP(X1,X1,times_times(X1,number_number_of(X1,bit0(bit1(pls)))),X2) = hAPP(X1,X1,plus_plus(X1,X2),X2) ),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
cnf(c_0_40,hypothesis,
number_number_of(int,bit0(X1)) = bit0(X1),
inference(rw,[status(thm)],[c_0_29,c_0_26]) ).
cnf(c_0_41,plain,
number_ring(int),
inference(split_conjunct,[status(thm)],[arity_Int_Oint___Int_Onumber__ring]) ).
fof(c_0_42,plain,
! [X211] : hAPP(int,int,plus_plus(int,X211),pls) = ti(int,X211),
inference(variable_rename,[status(thm)],[fact_129_add__Pls__right]) ).
fof(c_0_43,plain,
! [X573,X574] : hAPP(int,int,plus_plus(int,number_number_of(int,X573)),number_number_of(int,X574)) = number_number_of(int,hAPP(int,int,plus_plus(int,X573),X574)),
inference(variable_rename,[status(thm)],[fact_67_plus__numeral__code_I9_J]) ).
cnf(c_0_44,plain,
( ~ number_ring(X1)
| hAPP(X1,X1,times_times(X1,X2),number_number_of(X1,bit0(bit1(pls)))) = hAPP(X1,X1,plus_plus(X1,X2),X2) ),
inference(split_conjunct,[status(thm)],[c_0_30]) ).
cnf(c_0_45,hypothesis,
bit0(ti(int,X1)) = bit0(X1),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
fof(c_0_46,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int))),zero_zero(int))),
inference(fof_simplification,[status(thm)],[c_0_32]) ).
cnf(c_0_47,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),number_number_of(int,min)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)),
inference(split_conjunct,[status(thm)],[fact_466__096s_A_094_A2_A_N_A_N1_A_061_As_A_094_A2_A_L_A1_096]) ).
cnf(c_0_48,plain,
number_number_of(int,min) = min,
inference(rw,[status(thm)],[c_0_33,c_0_26]) ).
cnf(c_0_49,plain,
one_one(int) = bit1(pls),
inference(rw,[status(thm)],[c_0_34,c_0_35]) ).
cnf(c_0_50,plain,
hAPP(int,int,plus_plus(int,X1),X2) = hAPP(int,int,plus_plus(int,X2),X1),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
cnf(c_0_51,plain,
hAPP(int,int,times_times(int,bit0(X1)),X2) = bit0(hAPP(int,int,times_times(int,X1),X2)),
inference(split_conjunct,[status(thm)],[c_0_37]) ).
cnf(c_0_52,plain,
hAPP(int,int,times_times(int,bit0(bit1(pls))),X1) = bit0(X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38,c_0_39]),c_0_40]),c_0_41])]) ).
fof(c_0_53,plain,
! [X154,X155] : hAPP(int,int,plus_plus(int,bit0(X154)),bit1(X155)) = bit1(hAPP(int,int,plus_plus(int,X154),X155)),
inference(variable_rename,[status(thm)],[fact_162_add__Bit0__Bit1]) ).
cnf(c_0_54,plain,
hAPP(int,int,plus_plus(int,X1),pls) = ti(int,X1),
inference(split_conjunct,[status(thm)],[c_0_42]) ).
cnf(c_0_55,plain,
hAPP(int,int,plus_plus(int,number_number_of(int,X1)),number_number_of(int,X2)) = number_number_of(int,hAPP(int,int,plus_plus(int,X1),X2)),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
cnf(c_0_56,plain,
hAPP(int,int,times_times(int,X1),bit0(bit1(pls))) = bit0(X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38,c_0_44]),c_0_40]),c_0_41])]) ).
cnf(c_0_57,hypothesis,
bit0(number_number_of(int,X1)) = bit0(X1),
inference(rw,[status(thm)],[c_0_45,c_0_26]) ).
fof(c_0_58,plain,
! [X231,X232] : hAPP(int,int,times_times(int,X231),X232) = hAPP(int,int,times_times(int,X232),X231),
inference(variable_rename,[status(thm)],[fact_23_zmult__commute]) ).
fof(c_0_59,plain,
! [X260] : hAPP(int,int,times_times(int,pls),X260) = pls,
inference(variable_rename,[status(thm)],[fact_62_mult__Pls]) ).
fof(c_0_60,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int))),zero_zero(int))),
inference(fof_nnf,[status(thm)],[c_0_46]) ).
cnf(c_0_61,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t),
inference(split_conjunct,[status(thm)],[fact_3_t]) ).
cnf(c_0_62,plain,
hAPP(int,int,plus_plus(int,bit1(pls)),hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),min),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_47,c_0_48]),c_0_49]),c_0_50]) ).
cnf(c_0_63,plain,
hAPP(int,int,times_times(int,bit0(bit0(bit1(pls)))),X1) = bit0(bit0(X1)),
inference(spm,[status(thm)],[c_0_51,c_0_52]) ).
cnf(c_0_64,plain,
hAPP(int,int,plus_plus(int,bit0(X1)),bit1(X2)) = bit1(hAPP(int,int,plus_plus(int,X1),X2)),
inference(split_conjunct,[status(thm)],[c_0_53]) ).
cnf(c_0_65,plain,
hAPP(int,int,plus_plus(int,X1),pls) = number_number_of(int,X1),
inference(rw,[status(thm)],[c_0_54,c_0_26]) ).
cnf(c_0_66,plain,
number_number_of(int,hAPP(int,int,plus_plus(int,X1),X1)) = bit0(X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44,c_0_55]),c_0_40]),c_0_56]),c_0_57]),c_0_41])]) ).
cnf(c_0_67,plain,
hAPP(int,int,times_times(int,X1),X2) = hAPP(int,int,times_times(int,X2),X1),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
cnf(c_0_68,plain,
hAPP(int,int,times_times(int,pls),X1) = pls,
inference(split_conjunct,[status(thm)],[c_0_59]) ).
cnf(c_0_69,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int))),zero_zero(int))),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
cnf(c_0_70,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),min) = hAPP(int,int,times_times(int,t),bit1(hAPP(int,int,plus_plus(int,m),m))),
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_61,c_0_49]),c_0_50]),c_0_62]),c_0_40]),c_0_63]),c_0_38]),c_0_49]),c_0_64]),c_0_65]),c_0_66]),c_0_38]),c_0_67]) ).
cnf(c_0_71,plain,
pls = zero_zero(int),
inference(split_conjunct,[status(thm)],[fact_122_Pls__def]) ).
cnf(c_0_72,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(split_conjunct,[status(thm)],[fact_2__096_I4_A_K_Am_A_L_A1_J_A_K_At_A_060_A_I4_A_K_Am_A_L_A1_J_A_K_A0_096]) ).
cnf(c_0_73,plain,
hAPP(int,int,times_times(int,X1),pls) = pls,
inference(spm,[status(thm)],[c_0_68,c_0_67]) ).
cnf(c_0_74,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,t),bit1(hAPP(int,int,plus_plus(int,m),m)))),pls)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_69,c_0_49]),c_0_50]),c_0_62]),c_0_70]),c_0_71]) ).
cnf(c_0_75,plain,
$false,
inference(sr,[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_72,c_0_40]),c_0_63]),c_0_38]),c_0_49]),c_0_64]),c_0_65]),c_0_66]),c_0_38]),c_0_67]),c_0_40]),c_0_63]),c_0_38]),c_0_49]),c_0_64]),c_0_65]),c_0_66]),c_0_38]),c_0_71]),c_0_73]),c_0_74]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM924+7 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.59 % Computer : n011.cluster.edu
% 0.11/0.59 % Model : x86_64 x86_64
% 0.11/0.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.59 % Memory : 8046.5625MB
% 0.11/0.59 % OS : Linux 6.8.0-71-generic
% 0.11/0.59 % CPULimit : 300
% 0.11/0.59 % WCLimit : 300
% 0.11/0.59 % DateTime : Mon Sep 21 03:16:56 UTC 2026
% 0.11/0.59 % CPUTime :
% 0.11/0.59 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.17/0.64 Running first-order theorem proving
% 0.17/0.64 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
% 4.96/1.50 % Version: 3.5.1
% 4.96/1.50 % Preprocessing class: FMLMSMSMSSSNFFN.
% 4.96/1.50 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 4.96/1.50 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 4.96/1.50 % Starting new_bool_3 with 300s (1) cores
% 4.96/1.50 % Starting new_bool_1 with 300s (1) cores
% 4.96/1.50 % Starting sh5l with 300s (1) cores
% 4.96/1.50 % new_bool_3 with pid 846027 completed with status 0
% 4.96/1.50 % Result found by new_bool_3
% 4.96/1.50 % Preprocessing class: FMLMSMSMSSSNFFN.
% 4.96/1.50 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 4.96/1.50 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 4.96/1.50 % Starting new_bool_3 with 300s (1) cores
% 4.96/1.50 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 4.96/1.50 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 4.96/1.50 % Search class: FGHSM-FSLM32-DFFFFFNN
% 4.96/1.50 % Scheduled 13 strats onto 1 cores with 300 seconds (300 total)
% 4.96/1.50 % Starting SubtermCWHack with 28s (1) cores
% 4.96/1.50 % SubtermCWHack with pid 846061 completed with status 0
% 4.96/1.50 % Result found by SubtermCWHack
% 4.96/1.50 % Preprocessing class: FMLMSMSMSSSNFFN.
% 4.96/1.50 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 4.96/1.50 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 4.96/1.50 % Starting new_bool_3 with 300s (1) cores
% 4.96/1.50 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 4.96/1.50 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 4.96/1.50 % Search class: FGHSM-FSLM32-DFFFFFNN
% 4.96/1.50 % Scheduled 13 strats onto 1 cores with 300 seconds (300 total)
% 4.96/1.50 % Starting SubtermCWHack with 28s (1) cores
% 4.96/1.50 % Preprocessing time : 0.016 s
% 4.96/1.50
% 4.96/1.50 % Proof found!
% 4.96/1.50 % SZS status Theorem
% 4.96/1.50 % SZS output start CNFRefutation
% See solution above
% 5.72/1.50 % Parsed axioms : 1255
% 5.72/1.50 % Removed by relevancy pruning/SinE : 632
% 5.72/1.50 % Initial clauses : 987
% 5.72/1.50 % Removed in clause preprocessing : 71
% 5.72/1.50 % Initial clauses in saturation : 916
% 5.72/1.50 % Processed clauses : 9086
% 5.72/1.50 % ...of these trivial : 640
% 5.72/1.50 % ...subsumed : 6841
% 5.72/1.50 % ...remaining for further processing : 1604
% 5.72/1.50 % Other redundant clauses eliminated : 152
% 5.72/1.50 % Clauses deleted for lack of memory : 0
% 5.72/1.50 % Backward-subsumed : 141
% 5.72/1.50 % Backward-rewritten : 57
% 5.72/1.50 % Generated clauses : 57953
% 5.72/1.50 % ...of the previous two non-redundant : 51145
% 5.72/1.50 % ...aggressively subsumed : 0
% 5.72/1.50 % Contextual simplify-reflections : 2
% 5.72/1.50 % Paramodulations : 57761
% 5.72/1.50 % Factorizations : 14
% 5.72/1.50 % NegExts : 0
% 5.72/1.50 % Equation resolutions : 184
% 5.72/1.50 % Disequality decompositions : 0
% 5.72/1.50 % Total rewrite steps : 52234
% 5.72/1.50 % ...of those cached : 49510
% 5.72/1.50 % Propositional unsat checks : 0
% 5.72/1.50 % Propositional check models : 0
% 5.72/1.50 % Propositional check unsatisfiable : 0
% 5.72/1.50 % Propositional clauses : 0
% 5.72/1.50 % Propositional clauses after purity: 0
% 5.72/1.50 % Propositional unsat core size : 0
% 5.72/1.50 % Propositional preprocessing time : 0.000
% 5.72/1.50 % Propositional encoding time : 0.000
% 5.72/1.50 % Propositional solver time : 0.000
% 5.72/1.50 % Success case prop preproc time : 0.000
% 5.72/1.50 % Success case prop encoding time : 0.000
% 5.72/1.50 % Success case prop solver time : 0.000
% 5.72/1.50 % Current number of processed clauses : 1347
% 5.72/1.50 % Positive orientable unit clauses : 276
% 5.72/1.50 % Positive unorientable unit clauses: 13
% 5.72/1.50 % Negative unit clauses : 73
% 5.72/1.50 % Non-unit-clauses : 985
% 5.72/1.50 % Current number of unprocessed clauses: 42605
% 5.72/1.50 % ...number of literals in the above : 150286
% 5.72/1.50 % Current number of archived formulas : 0
% 5.72/1.50 % Current number of archived clauses : 198
% 5.72/1.50 % Clause-clause subsumption calls (NU) : 331151
% 5.72/1.50 % Rec. Clause-clause subsumption calls : 118063
% 5.72/1.50 % Non-unit clause-clause subsumptions : 4323
% 5.72/1.50 % Unit Clause-clause subsumption calls : 9590
% 5.72/1.50 % Rewrite failures with RHS unbound : 0
% 5.72/1.50 % BW rewrite match attempts : 16379
% 5.72/1.50 % BW rewrite match successes : 112
% 5.72/1.50 % Condensation attempts : 0
% 5.72/1.50 % Condensation successes : 0
% 5.72/1.50 % Termbank termtop insertions : 1565091
% 5.72/1.50 % Search garbage collected termcells : 15460
% 5.72/1.50
% 5.72/1.50 % -------------------------------------------------
% 5.72/1.50 % User time : 0.737 s
% 5.72/1.50 % System time : 0.030 s
% 5.72/1.50 % Total time : 0.767 s
% 5.72/1.50 % Maximum resident set size: 8120 pages
% 5.72/1.50
% 5.72/1.50 % -------------------------------------------------
% 5.72/1.50 % User time : 0.790 s
% 5.72/1.50 % System time : 0.037 s
% 5.72/1.50 % Total time : 0.827 s
% 5.72/1.50 % Maximum resident set size: 6400 pages
% 5.72/1.50 % E exiting
%------------------------------------------------------------------------------