%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM925+7 : 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 : n021.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:54 PM UTC 2026
% Result : Theorem 2.59s 2.17s
% Output : CNFRefutation 2.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 18
% Syntax : Number of formulae : 70 ( 67 unt; 0 def)
% Number of atoms : 76 ( 63 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 16 ( 10 ~; 4 |; 0 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 6 con; 0-4 aty)
% Number of variables : 46 ( 1 sgn 26 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_514_succ__Bit0,axiom,
! [X20] : succ(bit0(X20)) = bit1(X20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_514_succ__Bit0) ).
fof(fact_78_Bit0__def,axiom,
! [X20] : bit0(X20) = plus_plus(int,X20,X20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_Bit0__def) ).
fof(fact_777_diff__bin__simps_I2_J,axiom,
! [X20] : minus_minus(int,X20,min) = succ(X20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_777_diff__bin__simps_I2_J) ).
fof(fact_75_add__Pls__right,axiom,
! [X20] : plus_plus(int,X20,pls) = ti(int,X20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_add__Pls__right) ).
fof(fact_120_number__of__is__id,axiom,
! [X20] : number_number_of(int,X20) = ti(int,X20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_120_number__of__is__id) ).
fof(fact_37_one__is__num__one,axiom,
one_one(int) = number_number_of(int,bit1(pls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_one__is__num__one) ).
fof(fact_72_Bit0__Pls,axiom,
bit0(pls) = pls,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_Bit0__Pls) ).
fof(fact_76_add__Pls,axiom,
! [X20] : plus_plus(int,pls,X20) = ti(int,X20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_add__Pls) ).
fof(tsy_c_Int_Osucc_res,axiom,
! [X1] : ti(int,succ(X1)) = succ(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tsy_c_Int_Osucc_res) ).
fof(fact_29_nat__1__add__1,axiom,
plus_plus(nat,one_one(nat),one_one(nat)) = number_number_of(nat,bit0(bit1(pls))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_nat__1__add__1) ).
fof(fact_519_succ__def,axiom,
! [X20] : succ(X20) = plus_plus(int,X20,one_one(int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_519_succ__def) ).
fof(conj_0,conjecture,
hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,bit0(bit1(pls)))) != zero_zero(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(fact_47_zadd__commute,axiom,
! [X16,X8] : plus_plus(int,X16,X8) = plus_plus(int,X8,X16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_zadd__commute) ).
fof(fact_73_Pls__def,axiom,
pls = zero_zero(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_Pls__def) ).
fof(fact_0_n1pos,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_n1pos) ).
fof(fact_165_field__power__not__zero,axiom,
! [X2] :
( ring_11004092258visors(X2)
=> ! [X15,X31] :
( ti(X2,X31) != zero_zero(X2)
=> hAPP(nat,X2,power_power(X2,X31),X15) != zero_zero(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_165_field__power__not__zero) ).
fof(arity_Int_Oint___Rings_Oring__1__no__zero__divisors,axiom,
ring_11004092258visors(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Rings_Oring__1__no__zero__divisors) ).
fof(fact_32_rel__simps_I2_J,axiom,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_rel__simps_I2_J) ).
fof(c_0_18,plain,
! [X4194] : succ(bit0(X4194)) = bit1(X4194),
inference(variable_rename,[status(thm)],[fact_514_succ__Bit0]) ).
fof(c_0_19,plain,
! [X3004] : bit0(X3004) = plus_plus(int,X3004,X3004),
inference(variable_rename,[status(thm)],[fact_78_Bit0__def]) ).
fof(c_0_20,plain,
! [X4771] : minus_minus(int,X4771,min) = succ(X4771),
inference(variable_rename,[status(thm)],[fact_777_diff__bin__simps_I2_J]) ).
fof(c_0_21,plain,
! [X3000] : plus_plus(int,X3000,pls) = ti(int,X3000),
inference(variable_rename,[status(thm)],[fact_75_add__Pls__right]) ).
fof(c_0_22,plain,
! [X3076] : number_number_of(int,X3076) = ti(int,X3076),
inference(variable_rename,[status(thm)],[fact_120_number__of__is__id]) ).
cnf(c_0_23,plain,
one_one(int) = number_number_of(int,bit1(pls)),
inference(split_conjunct,[status(thm)],[fact_37_one__is__num__one]) ).
cnf(c_0_24,plain,
succ(bit0(X1)) = bit1(X1),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_25,plain,
bit0(X1) = plus_plus(int,X1,X1),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
cnf(c_0_26,plain,
minus_minus(int,X1,min) = succ(X1),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
cnf(c_0_27,plain,
bit0(pls) = pls,
inference(split_conjunct,[status(thm)],[fact_72_Bit0__Pls]) ).
fof(c_0_28,plain,
! [X3001] : plus_plus(int,pls,X3001) = ti(int,X3001),
inference(variable_rename,[status(thm)],[fact_76_add__Pls]) ).
cnf(c_0_29,plain,
plus_plus(int,X1,pls) = ti(int,X1),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_30,plain,
number_number_of(int,X1) = ti(int,X1),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
fof(c_0_31,plain,
! [X2834] : ti(int,succ(X2834)) = succ(X2834),
inference(variable_rename,[status(thm)],[tsy_c_Int_Osucc_res]) ).
cnf(c_0_32,plain,
one_one(int) = number_number_of(int,minus_minus(int,plus_plus(int,pls,pls),min)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_23,c_0_24]),c_0_25]),c_0_26]) ).
cnf(c_0_33,plain,
plus_plus(int,pls,pls) = pls,
inference(rw,[status(thm)],[c_0_27,c_0_25]) ).
cnf(c_0_34,plain,
plus_plus(int,pls,X1) = ti(int,X1),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
cnf(c_0_35,plain,
number_number_of(int,X1) = plus_plus(int,X1,pls),
inference(rw,[status(thm)],[c_0_29,c_0_30]) ).
cnf(c_0_36,plain,
ti(int,succ(X1)) = succ(X1),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
cnf(c_0_37,plain,
plus_plus(nat,one_one(nat),one_one(nat)) = number_number_of(nat,bit0(bit1(pls))),
inference(split_conjunct,[status(thm)],[fact_29_nat__1__add__1]) ).
cnf(c_0_38,plain,
number_number_of(int,minus_minus(int,pls,min)) = one_one(int),
inference(rw,[status(thm)],[c_0_32,c_0_33]) ).
cnf(c_0_39,plain,
plus_plus(int,X1,pls) = plus_plus(int,pls,X1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_34,c_0_30]),c_0_35]) ).
cnf(c_0_40,plain,
ti(int,minus_minus(int,X1,min)) = minus_minus(int,X1,min),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_36,c_0_26]),c_0_26]) ).
cnf(c_0_41,plain,
ti(int,X1) = plus_plus(int,X1,pls),
inference(rw,[status(thm)],[c_0_30,c_0_35]) ).
fof(c_0_42,plain,
! [X4202] : succ(X4202) = plus_plus(int,X4202,one_one(int)),
inference(variable_rename,[status(thm)],[fact_519_succ__def]) ).
fof(c_0_43,negated_conjecture,
hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,bit0(bit1(pls)))) = zero_zero(int),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[conj_0])]) ).
cnf(c_0_44,plain,
plus_plus(nat,one_one(nat),one_one(nat)) = number_number_of(nat,plus_plus(int,minus_minus(int,plus_plus(int,pls,pls),min),minus_minus(int,plus_plus(int,pls,pls),min))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_37,c_0_24]),c_0_25]),c_0_25]),c_0_26]),c_0_26]) ).
cnf(c_0_45,plain,
plus_plus(int,pls,minus_minus(int,pls,min)) = one_one(int),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_38,c_0_35]),c_0_39]) ).
cnf(c_0_46,plain,
plus_plus(int,pls,minus_minus(int,X1,min)) = minus_minus(int,X1,min),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_40,c_0_41]),c_0_39]) ).
cnf(c_0_47,plain,
succ(X1) = plus_plus(int,X1,one_one(int)),
inference(split_conjunct,[status(thm)],[c_0_42]) ).
cnf(c_0_48,negated_conjecture,
hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,bit0(bit1(pls)))) = zero_zero(int),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
cnf(c_0_49,plain,
number_number_of(nat,plus_plus(int,minus_minus(int,pls,min),minus_minus(int,pls,min))) = plus_plus(nat,one_one(nat),one_one(nat)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_44,c_0_33]),c_0_33]) ).
cnf(c_0_50,plain,
minus_minus(int,pls,min) = one_one(int),
inference(rw,[status(thm)],[c_0_45,c_0_46]) ).
cnf(c_0_51,plain,
minus_minus(int,X1,min) = plus_plus(int,X1,one_one(int)),
inference(rw,[status(thm)],[c_0_47,c_0_26]) ).
fof(c_0_52,plain,
! [X2965,X2966] : plus_plus(int,X2965,X2966) = plus_plus(int,X2966,X2965),
inference(variable_rename,[status(thm)],[fact_47_zadd__commute]) ).
cnf(c_0_53,negated_conjecture,
hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,plus_plus(int,minus_minus(int,plus_plus(int,pls,pls),min),minus_minus(int,plus_plus(int,pls,pls),min)))) = zero_zero(int),
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_24]),c_0_25]),c_0_25]),c_0_26]),c_0_26]) ).
cnf(c_0_54,plain,
number_number_of(nat,minus_minus(int,one_one(int),min)) = plus_plus(nat,one_one(nat),one_one(nat)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_49,c_0_50]),c_0_50]),c_0_51]) ).
cnf(c_0_55,plain,
pls = zero_zero(int),
inference(split_conjunct,[status(thm)],[fact_73_Pls__def]) ).
cnf(c_0_56,plain,
plus_plus(int,X1,X2) = plus_plus(int,X2,X1),
inference(split_conjunct,[status(thm)],[c_0_52]) ).
cnf(c_0_57,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n)))),
inference(split_conjunct,[status(thm)],[fact_0_n1pos]) ).
fof(c_0_58,plain,
! [X3172,X3173,X3174] :
( ~ ring_11004092258visors(X3172)
| ti(X3172,X3174) = zero_zero(X3172)
| hAPP(nat,X3172,power_power(X3172,X3174),X3173) != zero_zero(X3172) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_165_field__power__not__zero])])]) ).
cnf(c_0_59,negated_conjecture,
hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),plus_plus(nat,one_one(nat),one_one(nat))) = 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)],[c_0_53,c_0_33]),c_0_50]),c_0_33]),c_0_50]),c_0_51]),c_0_54]),c_0_55]) ).
cnf(c_0_60,plain,
plus_plus(int,one_one(int),X1) = minus_minus(int,X1,min),
inference(spm,[status(thm)],[c_0_51,c_0_56]) ).
cnf(c_0_61,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n)))),
inference(rw,[status(thm)],[c_0_57,c_0_55]) ).
cnf(c_0_62,plain,
( ti(X1,X2) = zero_zero(X1)
| ~ ring_11004092258visors(X1)
| hAPP(nat,X1,power_power(X1,X2),X3) != zero_zero(X1) ),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
cnf(c_0_63,negated_conjecture,
hAPP(nat,int,power_power(int,minus_minus(int,hAPP(nat,int,semiring_1_of_nat(int),n),min)),plus_plus(nat,one_one(nat),one_one(nat))) = pls,
inference(rw,[status(thm)],[c_0_59,c_0_60]) ).
cnf(c_0_64,plain,
ring_11004092258visors(int),
inference(split_conjunct,[status(thm)],[arity_Int_Oint___Rings_Oring__1__no__zero__divisors]) ).
fof(c_0_65,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)),
inference(fof_simplification,[status(thm)],[fact_32_rel__simps_I2_J]) ).
cnf(c_0_66,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),minus_minus(int,hAPP(nat,int,semiring_1_of_nat(int),n),min))),
inference(rw,[status(thm)],[c_0_61,c_0_60]) ).
cnf(c_0_67,negated_conjecture,
minus_minus(int,hAPP(nat,int,semiring_1_of_nat(int),n),min) = pls,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[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_62,c_0_63]),c_0_41]),c_0_55]),c_0_55]),c_0_64])]),c_0_56]),c_0_46]) ).
cnf(c_0_68,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)),
inference(split_conjunct,[status(thm)],[c_0_65]) ).
cnf(c_0_69,plain,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_66,c_0_67]),c_0_68]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : NUM925+7 : TPTP v9.2.1. Released v5.3.0.
% 0.00/0.11 % 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.15/0.32 % Computer : n021.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Tue May 5 01:19:25 EDT 2026
% 0.15/0.32 % CPUTime :
% 0.15/0.33 % start to proof: theBenchmark
% 2.59/2.17 % Version : CSE_E---1.7
% 2.59/2.17 % Problem : theBenchmark.p
% 2.59/2.17 % SZS status Theorem for theBenchmark.p
% 2.59/2.17 % SZS output start CNFRefutation
% See solution above
% 2.59/2.17 % Total time : 1.591s
%------------------------------------------------------------------------------