%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM924+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 : n006.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:58:52 PM UTC 2026
% Result : Theorem 10.62s 7.12s
% Output : CNFRefutation 10.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 15
% Syntax : Number of formulae : 53 ( 53 unt; 0 def)
% Number of atoms : 53 ( 45 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 3 ( 1 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 11 con; 0-4 aty)
% Number of variables : 34 ( 2 sgn 20 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_131_add__Pls,axiom,
! [X15] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),pls),X15) = ti(int,X15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_add__Pls) ).
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(fact_22_number__of__is__id,axiom,
! [X15] : hAPP(int,int,number_number_of(int),X15) = ti(int,X15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_number__of__is__id) ).
fof(fact_61_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_61_nat__1__add__1) ).
fof(fact_123_Pls__def,axiom,
pls = zero_zero(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_123_Pls__def) ).
fof(fact_1525_succ__Pls,axiom,
hAPP(int,int,succ,pls) = hAPP(int,int,bit1,pls),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1525_succ__Pls) ).
fof(fact_1528_succ__def,axiom,
! [X15] : hAPP(int,int,succ,X15) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X15),one_one(int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1528_succ__def) ).
fof(fact_1427_semiring__norm_I115_J,axiom,
hAPP(nat,nat,suc,hAPP(nat,nat,suc,zero_zero(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_1427_semiring__norm_I115_J) ).
fof(fact_1330_One__nat__def,axiom,
one_one(nat) = hAPP(nat,nat,suc,zero_zero(nat)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1330_One__nat__def) ).
fof(conj_0,conjecture,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int))),zero_zero(int))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(fact_99_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_99_zadd__commute) ).
fof(fact_23_zmult__commute,axiom,
! [X16,X12] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X16),X12) = hAPP(int,int,hAPP(int,fun(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,hAPP(int,fun(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,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),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),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_t) ).
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,hAPP(int,fun(int,int),times_times(int),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)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),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))),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_15,plain,
! [X14079] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),pls),X14079) = ti(int,X14079),
inference(variable_rename,[status(thm)],[fact_131_add__Pls]) ).
fof(c_0_16,plain,
! [X27419,X27420] : hAPP(X27419,X27419,combi(X27419),X27420) = ti(X27419,X27420),
inference(variable_rename,[status(thm)],[help_COMBI_1_1_U]) ).
fof(c_0_17,plain,
! [X13865] : hAPP(int,int,number_number_of(int),X13865) = ti(int,X13865),
inference(variable_rename,[status(thm)],[fact_22_number__of__is__id]) ).
cnf(c_0_18,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_61_nat__1__add__1]) ).
cnf(c_0_19,plain,
pls = zero_zero(int),
inference(split_conjunct,[status(thm)],[fact_123_Pls__def]) ).
cnf(c_0_20,plain,
hAPP(int,int,succ,pls) = hAPP(int,int,bit1,pls),
inference(split_conjunct,[status(thm)],[fact_1525_succ__Pls]) ).
fof(c_0_21,plain,
! [X17616] : hAPP(int,int,succ,X17616) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X17616),one_one(int)),
inference(variable_rename,[status(thm)],[fact_1528_succ__def]) ).
cnf(c_0_22,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),pls),X1) = ti(int,X1),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
cnf(c_0_23,plain,
hAPP(X1,X1,combi(X1),X2) = ti(X1,X2),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_24,plain,
hAPP(int,int,number_number_of(int),X1) = ti(int,X1),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_25,plain,
hAPP(nat,nat,suc,hAPP(nat,nat,suc,zero_zero(nat))) = hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))),
inference(split_conjunct,[status(thm)],[fact_1427_semiring__norm_I115_J]) ).
cnf(c_0_26,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_18,c_0_19]) ).
cnf(c_0_27,plain,
one_one(nat) = hAPP(nat,nat,suc,zero_zero(nat)),
inference(split_conjunct,[status(thm)],[fact_1330_One__nat__def]) ).
cnf(c_0_28,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_20,c_0_19]),c_0_19]) ).
cnf(c_0_29,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_21]) ).
cnf(c_0_30,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_22,c_0_23]) ).
cnf(c_0_31,plain,
hAPP(int,int,number_number_of(int),X1) = hAPP(int,int,combi(int),X1),
inference(rw,[status(thm)],[c_0_24,c_0_23]) ).
cnf(c_0_32,plain,
hAPP(nat,nat,hAPP(nat,fun(nat,nat),plus_plus(nat),one_one(nat)),one_one(nat)) = hAPP(nat,nat,suc,one_one(nat)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_25,c_0_19]),c_0_26]),c_0_27]) ).
cnf(c_0_33,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_28,c_0_29]) ).
cnf(c_0_34,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_30,c_0_31]),c_0_19]) ).
fof(c_0_35,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int))),zero_zero(int))),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[conj_0])]) ).
fof(c_0_36,plain,
! [X14024,X14025] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X14024),X14025) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X14025),X14024),
inference(variable_rename,[status(thm)],[fact_99_zadd__commute]) ).
fof(c_0_37,plain,
! [X13866,X13867] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X13866),X13867) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X13867),X13866),
inference(variable_rename,[status(thm)],[fact_23_zmult__commute]) ).
cnf(c_0_38,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_26,c_0_32]) ).
cnf(c_0_39,plain,
hAPP(int,int,bit1,zero_zero(int)) = hAPP(int,int,number_number_of(int),one_one(int)),
inference(rw,[status(thm)],[c_0_33,c_0_34]) ).
fof(c_0_40,plain,
! [X13945] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),pls),X13945) = pls,
inference(variable_rename,[status(thm)],[fact_62_mult__Pls]) ).
cnf(c_0_41,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int))),zero_zero(int))),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
cnf(c_0_42,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),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),
inference(split_conjunct,[status(thm)],[fact_3_t]) ).
cnf(c_0_43,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_36]) ).
cnf(c_0_44,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X1),X2) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X2),X1),
inference(split_conjunct,[status(thm)],[c_0_37]) ).
cnf(c_0_45,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_38,c_0_39]) ).
cnf(c_0_46,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),pls),X1) = pls,
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_47,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(nat,nat,suc,one_one(nat)))),one_one(int))),zero_zero(int))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_41,c_0_19]),c_0_26]),c_0_32]) ).
cnf(c_0_48,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),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)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),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))),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_49,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),t),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))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(nat,nat,suc,one_one(nat)))),
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_42,c_0_19]),c_0_39]),c_0_43]),c_0_44]),c_0_19]),c_0_39]),c_0_45]),c_0_43]) ).
cnf(c_0_50,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),zero_zero(int)),X1) = zero_zero(int),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_46,c_0_19]),c_0_19]) ).
cnf(c_0_51,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(nat,nat,suc,one_one(nat))))),zero_zero(int))),
inference(rw,[status(thm)],[c_0_47,c_0_43]) ).
cnf(c_0_52,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)],[c_0_48,c_0_19]),c_0_39]),c_0_43]),c_0_44]),c_0_49]),c_0_19]),c_0_39]),c_0_43]),c_0_44]),c_0_50]),c_0_51]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM924+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.13/0.32 % Computer : n006.cluster.edu
% 0.13/0.32 % Model : x86_64 x86_64
% 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.32 % Memory : 8042.1875MB
% 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.32 % CPULimit : 300
% 0.13/0.32 % WCLimit : 300
% 0.13/0.32 % DateTime : Tue May 5 01:17:46 EDT 2026
% 0.13/0.32 % CPUTime :
% 0.13/0.34 % start to proof: theBenchmark
% 10.62/7.12 % Version : CSE_E---1.7
% 10.62/7.12 % Problem : theBenchmark.p
% 10.62/7.12 % SZS status Theorem for theBenchmark.p
% 10.62/7.12 % SZS output start CNFRefutation
% See solution above
% 10.62/7.14 % Total time : 5.990s
%------------------------------------------------------------------------------