%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM926+8 : TPTP v9.2.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:59:08 PM UTC 2026
% Result : Theorem 42.92s 25.27s
% Output : CNFRefutation 43.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 25
% Syntax : Number of formulae : 94 ( 74 unt; 0 def)
% Number of atoms : 122 ( 86 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 55 ( 27 ~; 22 |; 0 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 17 con; 0-4 aty)
% Number of variables : 89 ( 7 sgn 39 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(tsy_c_hAPP_res,axiom,
! [X3,X1,X4,X5] : ti(X3,hAPP(X1,X3,X4,X5)) = hAPP(X1,X3,X4,X5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tsy_c_hAPP_res) ).
fof(help_COMBI_1_1_U,axiom,
! [X1,X228] : hAPP(X1,X1,combi(X1),X228) = ti(X1,X228),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBI_1_1_U) ).
fof(help_If_3_1_T,axiom,
! [X228] :
( ti(bool,X228) = fTrue
| ti(bool,X228) = fFalse ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_3_1_T) ).
fof(fact_127_add__Pls,axiom,
! [X19] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),pls),X19) = ti(int,X19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_add__Pls) ).
fof(fact_89_number__of__is__id,axiom,
! [X19] : hAPP(int,int,number_number_of(int),X19) = ti(int,X19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_number__of__is__id) ).
fof(fact_1506_not__neg__int,axiom,
! [X13] : ~ hBOOL(hAPP(int,bool,nat_neg,hAPP(nat,int,semiring_1_of_nat(int),X13))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1506_not__neg__int) ).
fof(fact_1590_succ__Pls,axiom,
hAPP(int,int,succ,pls) = hAPP(int,int,bit1,pls),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1590_succ__Pls) ).
fof(fact_206_Pls__def,axiom,
pls = zero_zero(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_Pls__def) ).
fof(fact_1593_succ__def,axiom,
! [X19] : hAPP(int,int,succ,X19) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X19),one_one(int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1593_succ__def) ).
fof(fact_37_nat__1__add__1,axiom,
hAPP(nat,nat,hAPP(nat,fun(nat,nat),plus_plus(nat),one_one(nat)),one_one(nat)) = hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_nat__1__add__1) ).
fof(fact_1344_Suc__eq__plus1,axiom,
! [X13] : hAPP(nat,nat,suc,X13) = hAPP(nat,nat,hAPP(nat,fun(nat,nat),plus_plus(nat),X13),one_one(nat)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1344_Suc__eq__plus1) ).
fof(help_fTrue_1_1_U,axiom,
hBOOL(fTrue),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fTrue_1_1_U) ).
fof(conj_0,conjecture,
? [X6,X7] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X6),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X7),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(fact_1316_transfer__int__nat__numerals_I2_J,axiom,
one_one(int) = hAPP(nat,int,semiring_1_of_nat(int),one_one(nat)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1316_transfer__int__nat__numerals_I2_J) ).
fof(fact_92_zadd__commute,axiom,
! [X16,X12] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X16),X12) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X12),X16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_zadd__commute) ).
fof(tsy_c_Groups_Oone__class_Oone_res,axiom,
! [X1] :
( one(X1)
=> ti(X1,one_one(X1)) = one_one(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tsy_c_Groups_Oone__class_Oone_res) ).
fof(fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,axiom,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))
=> ? [X6,X7] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X6),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X7),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
fof(fact_1290_transfer__int__nat__numerals_I1_J,axiom,
zero_zero(int) = hAPP(nat,int,semiring_1_of_nat(int),zero_zero(nat)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1290_transfer__int__nat__numerals_I1_J) ).
fof(fact_1568_xt1_I12_J,axiom,
! [X1] :
( order(X1)
=> ! [X8,X9] :
( ti(X1,X8) != ti(X1,X9)
=> ( hBOOL(hAPP(X1,bool,hAPP(X1,fun(X1,bool),ord_less_eq(X1),X9),X8))
=> hBOOL(hAPP(X1,bool,hAPP(X1,fun(X1,bool),ord_less(X1),X9),X8)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1568_xt1_I12_J) ).
fof(tsy_v_t_____res,axiom,
ti(int,t) = t,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tsy_v_t_____res) ).
fof(fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,axiom,
( t = one_one(int)
=> ? [X6,X7] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X6),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X7),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
fof(arity_Int_Oint___Groups_Oone,axiom,
one(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Groups_Oone) ).
fof(fact_1504_not__neg__0,axiom,
~ hBOOL(hAPP(int,bool,nat_neg,zero_zero(int))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1504_not__neg__0) ).
fof(fact_0_tpos,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_tpos) ).
fof(arity_Int_Oint___Orderings_Oorder,axiom,
order(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Orderings_Oorder) ).
fof(c_0_25,plain,
! [X13847,X13848,X13849,X13850] : ti(X13847,hAPP(X13848,X13847,X13849,X13850)) = hAPP(X13848,X13847,X13849,X13850),
inference(variable_rename,[status(thm)],[tsy_c_hAPP_res]) ).
fof(c_0_26,plain,
! [X27439,X27440] : hAPP(X27439,X27439,combi(X27439),X27440) = ti(X27439,X27440),
inference(variable_rename,[status(thm)],[help_COMBI_1_1_U]) ).
fof(c_0_27,plain,
! [X27421] :
( ti(bool,X27421) = fTrue
| ti(bool,X27421) = fFalse ),
inference(variable_rename,[status(thm)],[help_If_3_1_T]) ).
fof(c_0_28,plain,
! [X14131] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),pls),X14131) = ti(int,X14131),
inference(variable_rename,[status(thm)],[fact_127_add__Pls]) ).
fof(c_0_29,plain,
! [X14053] : hAPP(int,int,number_number_of(int),X14053) = ti(int,X14053),
inference(variable_rename,[status(thm)],[fact_89_number__of__is__id]) ).
fof(c_0_30,plain,
! [X13] : ~ hBOOL(hAPP(int,bool,nat_neg,hAPP(nat,int,semiring_1_of_nat(int),X13))),
inference(fof_simplification,[status(thm)],[fact_1506_not__neg__int]) ).
cnf(c_0_31,plain,
ti(X1,hAPP(X2,X1,X3,X4)) = hAPP(X2,X1,X3,X4),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
cnf(c_0_32,plain,
hAPP(X1,X1,combi(X1),X2) = ti(X1,X2),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
cnf(c_0_33,plain,
( ti(bool,X1) = fTrue
| ti(bool,X1) = fFalse ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_34,plain,
hAPP(int,int,succ,pls) = hAPP(int,int,bit1,pls),
inference(split_conjunct,[status(thm)],[fact_1590_succ__Pls]) ).
cnf(c_0_35,plain,
pls = zero_zero(int),
inference(split_conjunct,[status(thm)],[fact_206_Pls__def]) ).
fof(c_0_36,plain,
! [X17858] : hAPP(int,int,succ,X17858) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X17858),one_one(int)),
inference(variable_rename,[status(thm)],[fact_1593_succ__def]) ).
cnf(c_0_37,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),pls),X1) = ti(int,X1),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
cnf(c_0_38,plain,
hAPP(int,int,number_number_of(int),X1) = ti(int,X1),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
fof(c_0_39,plain,
! [X17609] : ~ hBOOL(hAPP(int,bool,nat_neg,hAPP(nat,int,semiring_1_of_nat(int),X17609))),
inference(variable_rename,[status(thm)],[c_0_30]) ).
cnf(c_0_40,plain,
hAPP(X1,X1,combi(X1),hAPP(X2,X1,X3,X4)) = hAPP(X2,X1,X3,X4),
inference(rw,[status(thm)],[c_0_31,c_0_32]) ).
cnf(c_0_41,plain,
( hAPP(bool,bool,combi(bool),X1) = fFalse
| hAPP(bool,bool,combi(bool),X1) = fTrue ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_33,c_0_32]),c_0_32]) ).
cnf(c_0_42,plain,
hAPP(nat,nat,hAPP(nat,fun(nat,nat),plus_plus(nat),one_one(nat)),one_one(nat)) = hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))),
inference(split_conjunct,[status(thm)],[fact_37_nat__1__add__1]) ).
fof(c_0_43,plain,
! [X17274] : hAPP(nat,nat,suc,X17274) = hAPP(nat,nat,hAPP(nat,fun(nat,nat),plus_plus(nat),X17274),one_one(nat)),
inference(variable_rename,[status(thm)],[fact_1344_Suc__eq__plus1]) ).
cnf(c_0_44,plain,
hAPP(int,int,succ,zero_zero(int)) = hAPP(int,int,bit1,zero_zero(int)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_34,c_0_35]),c_0_35]) ).
cnf(c_0_45,plain,
hAPP(int,int,succ,X1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X1),one_one(int)),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
cnf(c_0_46,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),pls),X1) = hAPP(int,int,combi(int),X1),
inference(rw,[status(thm)],[c_0_37,c_0_32]) ).
cnf(c_0_47,plain,
hAPP(int,int,number_number_of(int),X1) = hAPP(int,int,combi(int),X1),
inference(rw,[status(thm)],[c_0_38,c_0_32]) ).
cnf(c_0_48,plain,
~ hBOOL(hAPP(int,bool,nat_neg,hAPP(nat,int,semiring_1_of_nat(int),X1))),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_49,plain,
( hAPP(X1,bool,X2,X3) = fFalse
| fTrue = hAPP(X1,bool,X2,X3) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40,c_0_41]),c_0_40]) ).
cnf(c_0_50,plain,
hBOOL(fTrue),
inference(split_conjunct,[status(thm)],[help_fTrue_1_1_U]) ).
fof(c_0_51,negated_conjecture,
~ ? [X6,X7] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X6),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X7),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)),
inference(assume_negation,[status(cth)],[conj_0]) ).
cnf(c_0_52,plain,
hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,zero_zero(int)))) = hAPP(nat,nat,hAPP(nat,fun(nat,nat),plus_plus(nat),one_one(nat)),one_one(nat)),
inference(rw,[status(thm)],[c_0_42,c_0_35]) ).
cnf(c_0_53,plain,
hAPP(nat,nat,suc,X1) = hAPP(nat,nat,hAPP(nat,fun(nat,nat),plus_plus(nat),X1),one_one(nat)),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
cnf(c_0_54,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),zero_zero(int)),one_one(int)) = hAPP(int,int,bit1,zero_zero(int)),
inference(rw,[status(thm)],[c_0_44,c_0_45]) ).
cnf(c_0_55,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),zero_zero(int)),X1) = hAPP(int,int,number_number_of(int),X1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_46,c_0_47]),c_0_35]) ).
cnf(c_0_56,plain,
hAPP(int,bool,nat_neg,hAPP(nat,int,semiring_1_of_nat(int),X1)) = fFalse,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48,c_0_49]),c_0_50])]) ).
cnf(c_0_57,plain,
one_one(int) = hAPP(nat,int,semiring_1_of_nat(int),one_one(nat)),
inference(split_conjunct,[status(thm)],[fact_1316_transfer__int__nat__numerals_I2_J]) ).
fof(c_0_58,negated_conjecture,
! [X27477,X27478] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X27477),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X27478),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) != hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_51])]) ).
cnf(c_0_59,plain,
hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,zero_zero(int)))) = hAPP(nat,nat,suc,one_one(nat)),
inference(rw,[status(thm)],[c_0_52,c_0_53]) ).
cnf(c_0_60,plain,
hAPP(int,int,bit1,zero_zero(int)) = hAPP(int,int,number_number_of(int),one_one(int)),
inference(rw,[status(thm)],[c_0_54,c_0_55]) ).
fof(c_0_61,plain,
! [X14060,X14061] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X14060),X14061) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X14061),X14060),
inference(variable_rename,[status(thm)],[fact_92_zadd__commute]) ).
cnf(c_0_62,plain,
fFalse = hAPP(int,bool,nat_neg,one_one(int)),
inference(spm,[status(thm)],[c_0_56,c_0_57]) ).
fof(c_0_63,plain,
! [X13726] :
( ~ one(X13726)
| ti(X13726,one_one(X13726)) = one_one(X13726) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[tsy_c_Groups_Oone__class_Oone_res])]) ).
fof(c_0_64,plain,
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))
| hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),esk3_0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),esk4_0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06])])]) ).
cnf(c_0_65,negated_conjecture,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X2),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) != hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
cnf(c_0_66,plain,
hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,number_number_of(int),one_one(int)))) = hAPP(nat,nat,suc,one_one(nat)),
inference(rw,[status(thm)],[c_0_59,c_0_60]) ).
cnf(c_0_67,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X1),X2) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X2),X1),
inference(split_conjunct,[status(thm)],[c_0_61]) ).
cnf(c_0_68,plain,
hAPP(int,bool,nat_neg,hAPP(nat,int,semiring_1_of_nat(int),X1)) = hAPP(int,bool,nat_neg,one_one(int)),
inference(rw,[status(thm)],[c_0_56,c_0_62]) ).
cnf(c_0_69,plain,
zero_zero(int) = hAPP(nat,int,semiring_1_of_nat(int),zero_zero(nat)),
inference(split_conjunct,[status(thm)],[fact_1290_transfer__int__nat__numerals_I1_J]) ).
fof(c_0_70,plain,
! [X17790,X17791,X17792] :
( ~ order(X17790)
| ti(X17790,X17791) = ti(X17790,X17792)
| ~ hBOOL(hAPP(X17790,bool,hAPP(X17790,fun(X17790,bool),ord_less_eq(X17790),X17792),X17791))
| hBOOL(hAPP(X17790,bool,hAPP(X17790,fun(X17790,bool),ord_less(X17790),X17792),X17791)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_1568_xt1_I12_J])])]) ).
cnf(c_0_71,plain,
ti(int,t) = t,
inference(split_conjunct,[status(thm)],[tsy_v_t_____res]) ).
cnf(c_0_72,plain,
( ti(X1,one_one(X1)) = one_one(X1)
| ~ one(X1) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_73,plain,
( hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),esk3_0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),esk4_0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(split_conjunct,[status(thm)],[c_0_64]) ).
cnf(c_0_74,negated_conjecture,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(nat,nat,suc,one_one(nat)))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X2),hAPP(nat,nat,suc,one_one(nat)))) != hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,number_number_of(int),one_one(int)))))),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)],[c_0_65,c_0_35]),c_0_60]),c_0_66]),c_0_35]),c_0_60]),c_0_66]),c_0_35]),c_0_60]),c_0_67]) ).
cnf(c_0_75,plain,
hAPP(int,bool,nat_neg,one_one(int)) = hAPP(int,bool,nat_neg,zero_zero(int)),
inference(spm,[status(thm)],[c_0_68,c_0_69]) ).
fof(c_0_76,plain,
( t != one_one(int)
| hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),esk1_0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),esk2_0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06])])]) ).
cnf(c_0_77,plain,
( ti(X1,X2) = ti(X1,X3)
| hBOOL(hAPP(X1,bool,hAPP(X1,fun(X1,bool),ord_less(X1),X3),X2))
| ~ order(X1)
| ~ hBOOL(hAPP(X1,bool,hAPP(X1,fun(X1,bool),ord_less_eq(X1),X3),X2)) ),
inference(split_conjunct,[status(thm)],[c_0_70]) ).
cnf(c_0_78,plain,
hAPP(int,int,combi(int),t) = t,
inference(rw,[status(thm)],[c_0_71,c_0_32]) ).
cnf(c_0_79,plain,
( hAPP(X1,X1,combi(X1),one_one(X1)) = one_one(X1)
| ~ one(X1) ),
inference(rw,[status(thm)],[c_0_72,c_0_32]) ).
cnf(c_0_80,plain,
one(int),
inference(split_conjunct,[status(thm)],[arity_Int_Oint___Groups_Oone]) ).
cnf(c_0_81,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)),
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)],[c_0_73,c_0_35]),c_0_60]),c_0_66]),c_0_35]),c_0_60]),c_0_66]),c_0_35]),c_0_60]),c_0_67]),c_0_74]) ).
cnf(c_0_82,plain,
( hAPP(X1,bool,X2,X3) = hAPP(int,bool,nat_neg,zero_zero(int))
| fTrue = hAPP(X1,bool,X2,X3) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_49,c_0_62]),c_0_75]) ).
cnf(c_0_83,plain,
( hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),esk1_0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),esk2_0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))
| t != one_one(int) ),
inference(split_conjunct,[status(thm)],[c_0_76]) ).
fof(c_0_84,plain,
~ hBOOL(hAPP(int,bool,nat_neg,zero_zero(int))),
inference(fof_simplification,[status(thm)],[fact_1504_not__neg__0]) ).
cnf(c_0_85,plain,
( hAPP(X1,X1,combi(X1),X2) = hAPP(X1,X1,combi(X1),X3)
| hBOOL(hAPP(X1,bool,hAPP(X1,fun(X1,bool),ord_less(X1),X3),X2))
| ~ order(X1)
| ~ hBOOL(hAPP(X1,bool,hAPP(X1,fun(X1,bool),ord_less_eq(X1),X3),X2)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_77,c_0_32]),c_0_32]) ).
cnf(c_0_86,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t)),
inference(split_conjunct,[status(thm)],[fact_0_tpos]) ).
cnf(c_0_87,plain,
hAPP(int,int,number_number_of(int),t) = t,
inference(rw,[status(thm)],[c_0_78,c_0_47]) ).
cnf(c_0_88,plain,
hAPP(int,int,number_number_of(int),one_one(int)) = one_one(int),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_79,c_0_80]),c_0_47]) ).
cnf(c_0_89,plain,
hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t) = hAPP(int,bool,nat_neg,zero_zero(int)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_81,c_0_82]),c_0_50])]) ).
cnf(c_0_90,plain,
order(int),
inference(split_conjunct,[status(thm)],[arity_Int_Oint___Orderings_Oorder]) ).
cnf(c_0_91,plain,
t != one_one(int),
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)],[c_0_83,c_0_35]),c_0_60]),c_0_66]),c_0_35]),c_0_60]),c_0_66]),c_0_35]),c_0_60]),c_0_67]),c_0_74]) ).
cnf(c_0_92,plain,
~ hBOOL(hAPP(int,bool,nat_neg,zero_zero(int))),
inference(split_conjunct,[status(thm)],[c_0_84]) ).
cnf(c_0_93,plain,
$false,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[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(spm,[status(thm)],[c_0_85,c_0_86]),c_0_47]),c_0_87]),c_0_47]),c_0_88]),c_0_89]),c_0_90])]),c_0_91]),c_0_92]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM926+8 : TPTP v9.2.1. Released v5.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n003.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 01:19:11 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 42.92/25.27 % Version : CSE_E---1.7
% 42.92/25.27 % Problem : theBenchmark.p
% 42.92/25.27 % SZS status Theorem for theBenchmark.p
% 42.92/25.27 % SZS output start CNFRefutation
% See solution above
% 43.02/25.37 % Total time : 21.042s
%------------------------------------------------------------------------------