%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM924+7 : TPTP v9.2.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n017.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 14.66s 9.13s
% Output : CNFRefutation 14.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 15
% Syntax : Number of formulae : 53 ( 53 unt; 0 def)
% Number of atoms : 53 ( 43 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 15 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 7 con; 0-4 aty)
% Number of variables : 46 ( 1 sgn 28 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_132_Bit0__def,axiom,
! [X15] : bit0(X15) = hAPP(int,int,plus_plus(int,X15),X15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_132_Bit0__def) ).
fof(fact_161_add__Bit1__Bit0,axiom,
! [X15,X32] : hAPP(int,int,plus_plus(int,bit1(X15)),bit0(X32)) = bit1(hAPP(int,int,plus_plus(int,X15),X32)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_161_add__Bit1__Bit0) ).
fof(fact_130_add__Pls,axiom,
! [X15] : hAPP(int,int,plus_plus(int,pls),X15) = ti(int,X15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_130_add__Pls) ).
fof(fact_22_number__of__is__id,axiom,
! [X15] : number_number_of(int,X15) = ti(int,X15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_22_number__of__is__id) ).
fof(tsy_c_Int_OBit1_res,hypothesis,
! [X4] : ti(int,bit1(X4)) = bit1(X4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_c_Int_OBit1_res) ).
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/sandbox2/benchmark/theBenchmark.p',fact_3_t) ).
fof(fact_96_zadd__assoc,axiom,
! [X19,X20,X21] : hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,X19),X20)),X21) = hAPP(int,int,plus_plus(int,X19),hAPP(int,int,plus_plus(int,X20),X21)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_96_zadd__assoc) ).
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/sandbox2/benchmark/theBenchmark.p',fact_23_zmult__commute) ).
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/sandbox2/benchmark/theBenchmark.p',fact_98_zadd__commute) ).
fof(fact_61_nat__1__add__1,axiom,
hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = number_number_of(nat,bit0(bit1(pls))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_61_nat__1__add__1) ).
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/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(fact_751__096sum2sq_A_Is_M_A1_J_A_061_A_I4_A_K_Am_A_L_A1_J_A_K_At_096,axiom,
twoSqu1929807760sum2sq(product_Pair(int,int,s,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/sandbox2/benchmark/theBenchmark.p',fact_751__096sum2sq_A_Is_M_A1_J_A_061_A_I4_A_K_Am_A_L_A1_J_A_K_At_096) ).
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/sandbox2/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(fact_62_mult__Pls,axiom,
! [X12] : hAPP(int,int,times_times(int,pls),X12) = pls,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_62_mult__Pls) ).
fof(fact_122_Pls__def,axiom,
pls = zero_zero(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_122_Pls__def) ).
fof(c_0_15,plain,
! [X3323] : bit0(X3323) = hAPP(int,int,plus_plus(int,X3323),X3323),
inference(variable_rename,[status(thm)],[fact_132_Bit0__def]) ).
fof(c_0_16,plain,
! [X3374,X3375] : hAPP(int,int,plus_plus(int,bit1(X3374)),bit0(X3375)) = bit1(hAPP(int,int,plus_plus(int,X3374),X3375)),
inference(variable_rename,[status(thm)],[fact_161_add__Bit1__Bit0]) ).
fof(c_0_17,plain,
! [X3320] : hAPP(int,int,plus_plus(int,pls),X3320) = ti(int,X3320),
inference(variable_rename,[status(thm)],[fact_130_add__Pls]) ).
fof(c_0_18,plain,
! [X3111] : number_number_of(int,X3111) = ti(int,X3111),
inference(variable_rename,[status(thm)],[fact_22_number__of__is__id]) ).
fof(c_0_19,hypothesis,
! [X3019] : ti(int,bit1(X3019)) = bit1(X3019),
inference(variable_rename,[status(thm)],[tsy_c_Int_OBit1_res]) ).
cnf(c_0_20,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_21,plain,
bit0(X1) = hAPP(int,int,plus_plus(int,X1),X1),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
fof(c_0_22,plain,
! [X3259,X3260,X3261] : hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,X3259),X3260)),X3261) = hAPP(int,int,plus_plus(int,X3259),hAPP(int,int,plus_plus(int,X3260),X3261)),
inference(variable_rename,[status(thm)],[fact_96_zadd__assoc]) ).
cnf(c_0_23,plain,
hAPP(int,int,plus_plus(int,bit1(X1)),bit0(X2)) = bit1(hAPP(int,int,plus_plus(int,X1),X2)),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_24,plain,
hAPP(int,int,plus_plus(int,pls),X1) = ti(int,X1),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_25,plain,
number_number_of(int,X1) = ti(int,X1),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_26,hypothesis,
ti(int,bit1(X1)) = bit1(X1),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
fof(c_0_27,plain,
! [X3112,X3113] : hAPP(int,int,times_times(int,X3112),X3113) = hAPP(int,int,times_times(int,X3113),X3112),
inference(variable_rename,[status(thm)],[fact_23_zmult__commute]) ).
fof(c_0_28,plain,
! [X3265,X3266] : hAPP(int,int,plus_plus(int,X3265),X3266) = hAPP(int,int,plus_plus(int,X3266),X3265),
inference(variable_rename,[status(thm)],[fact_98_zadd__commute]) ).
cnf(c_0_29,plain,
hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = number_number_of(nat,bit0(bit1(pls))),
inference(split_conjunct,[status(thm)],[fact_61_nat__1__add__1]) ).
fof(c_0_30,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)],[inference(assume_negation,[status(cth)],[conj_0])]) ).
cnf(c_0_31,plain,
twoSqu1929807760sum2sq(product_Pair(int,int,s,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_751__096sum2sq_A_Is_M_A1_J_A_061_A_I4_A_K_Am_A_L_A1_J_A_K_At_096]) ).
cnf(c_0_32,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),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,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))),hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))),m)),one_one(int))),t),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_20,c_0_21]),c_0_21]),c_0_21]) ).
cnf(c_0_33,plain,
hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,X1),X2)),X3) = hAPP(int,int,plus_plus(int,X1),hAPP(int,int,plus_plus(int,X2),X3)),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_34,plain,
hAPP(int,int,plus_plus(int,bit1(X1)),hAPP(int,int,plus_plus(int,X2),X2)) = bit1(hAPP(int,int,plus_plus(int,X1),X2)),
inference(rw,[status(thm)],[c_0_23,c_0_21]) ).
cnf(c_0_35,plain,
hAPP(int,int,plus_plus(int,pls),X1) = number_number_of(int,X1),
inference(rw,[status(thm)],[c_0_24,c_0_25]) ).
cnf(c_0_36,hypothesis,
number_number_of(int,bit1(X1)) = bit1(X1),
inference(rw,[status(thm)],[c_0_26,c_0_25]) ).
cnf(c_0_37,plain,
hAPP(int,int,times_times(int,X1),X2) = hAPP(int,int,times_times(int,X2),X1),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_38,plain,
hAPP(int,int,plus_plus(int,X1),X2) = hAPP(int,int,plus_plus(int,X2),X1),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
cnf(c_0_39,plain,
hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))),
inference(rw,[status(thm)],[c_0_29,c_0_21]) ).
cnf(c_0_40,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_30]) ).
cnf(c_0_41,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_42,plain,
twoSqu1929807760sum2sq(product_Pair(int,int,s,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,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))),hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))),m)),one_one(int))),t),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_31,c_0_21]),c_0_21]) ).
cnf(c_0_43,plain,
hAPP(int,int,times_times(int,t),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),number_number_of(int,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(bit1(pls))))))) = hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),hAPP(nat,nat,plus_plus(nat,one_one(nat)),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)],[inference(rw,[status(thm)],[c_0_32,c_0_33]),c_0_34]),c_0_35]),c_0_36]),c_0_37]),c_0_38]),c_0_37]),c_0_39]),c_0_38]) ).
fof(c_0_44,plain,
! [X3191] : hAPP(int,int,times_times(int,pls),X3191) = pls,
inference(variable_rename,[status(thm)],[fact_62_mult__Pls]) ).
cnf(c_0_45,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,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))),one_one(int))),zero_zero(int))),
inference(rw,[status(thm)],[c_0_40,c_0_21]) ).
cnf(c_0_46,plain,
pls = zero_zero(int),
inference(split_conjunct,[status(thm)],[fact_122_Pls__def]) ).
cnf(c_0_47,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,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))),hAPP(int,int,plus_plus(int,bit1(pls)),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,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))),hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_41,c_0_21]),c_0_21]),c_0_21]),c_0_21]) ).
cnf(c_0_48,plain,
hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)))) = twoSqu1929807760sum2sq(product_Pair(int,int,s,one_one(int))),
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_33]),c_0_34]),c_0_35]),c_0_36]),c_0_37]),c_0_38]),c_0_37]),c_0_43]) ).
cnf(c_0_49,plain,
hAPP(int,int,times_times(int,pls),X1) = pls,
inference(split_conjunct,[status(thm)],[c_0_44]) ).
cnf(c_0_50,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),hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)))),one_one(int))),pls)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_45,c_0_39]),c_0_46]) ).
cnf(c_0_51,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),twoSqu1929807760sum2sq(product_Pair(int,int,s,one_one(int)))),pls)),
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_47,c_0_33]),c_0_34]),c_0_35]),c_0_36]),c_0_37]),c_0_38]),c_0_37]),c_0_43]),c_0_48]),c_0_33]),c_0_34]),c_0_35]),c_0_36]),c_0_37]),c_0_38]),c_0_46]),c_0_37]),c_0_49]) ).
cnf(c_0_52,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_50,c_0_38]),c_0_48]),c_0_51])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : NUM924+7 : TPTP v9.2.1. Released v5.3.0.
% 0.00/0.11 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.32 % Computer : n017.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Tue May 5 01:16:28 EDT 2026
% 0.14/0.32 % CPUTime :
% 0.14/0.33 % start to proof: theBenchmark
% 14.66/9.13 % Version : CSE_E---1.7
% 14.66/9.13 % Problem : theBenchmark.p
% 14.66/9.13 % SZS status Theorem for theBenchmark.p
% 14.66/9.13 % SZS output start CNFRefutation
% See solution above
% 14.66/9.18 % Total time : 6.616s
%------------------------------------------------------------------------------