%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM925+7 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:42:01 PM UTC 2026
% Result : Theorem 2.33s 0.86s
% Output : CNFRefutation 2.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 23
% Syntax : Number of formulae : 93 ( 34 unt; 9 def)
% Number of atoms : 194 ( 102 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 177 ( 76 ~; 74 |; 12 &)
% ( 14 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 13 ( 11 usr; 10 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 5 con; 0-4 aty)
% Number of variables : 59 ( 59 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f47,hypothesis,
! [B_1_1] : bit0(ti(int,B_1_1)) = bit0(B_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,hypothesis,
! [B_1_1] : bit1(ti(int,B_1_1)) = bit1(B_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,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') ).
fof(f100,axiom,
! [X_a] :
( linordered_idom(X_a)
=> ! [Xa,Ya] :
( plus_plus(X_a,hAPP(nat,X_a,power_power(X_a,Xa),number_number_of(nat,bit0(bit1(pls)))),hAPP(nat,X_a,power_power(X_a,Ya),number_number_of(nat,bit0(bit1(pls))))) = zero_zero(X_a)
<=> ( ti(X_a,Ya) = zero_zero(X_a)
& ti(X_a,Xa) = zero_zero(X_a) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f130,axiom,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f140,axiom,
! [K,L_1] :
( bit1(K) = bit1(L_1)
<=> ti(int,K) = ti(int,L_1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f153,axiom,
! [K] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),bit0(K)))
<=> hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),K)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f168,axiom,
! [K] :
( bit0(K) = pls
<=> ti(int,K) = pls ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f170,axiom,
bit0(pls) = pls,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f171,axiom,
pls = zero_zero(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f173,axiom,
! [K_1] : plus_plus(int,K_1,pls) = ti(int,K_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f190,axiom,
! [K_1] : bit1(K_1) = plus_plus(int,plus_plus(int,one_one(int),K_1),K_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1122,axiom,
linordered_idom(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1251,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') ).
fof(f1252,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(negated_conjecture,[status(cth)],[f1251]) ).
fof(f1365,plain,
! [X0] : bit0(ti(int,X0)) = bit0(X0),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f1367,plain,
! [X0] : bit1(ti(int,X0)) = bit1(X0),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f1461,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(cnf_transformation,[status(thm)],[f98]) ).
fof(f1463,plain,
! [X_a] :
( ! [Xa,Ya] :
( plus_plus(X_a,hAPP(nat,X_a,power_power(X_a,Xa),number_number_of(nat,bit0(bit1(pls)))),hAPP(nat,X_a,power_power(X_a,Ya),number_number_of(nat,bit0(bit1(pls))))) = zero_zero(X_a)
<=> ( ti(X_a,Ya) = zero_zero(X_a)
& ti(X_a,Xa) = zero_zero(X_a) ) )
| ~ linordered_idom(X_a) ),
inference(pre_NNF_transformation,[status(thm)],[f100]) ).
fof(f1464,plain,
! [X_a] :
( ! [Xa,Ya] :
( ( ti(X_a,Ya) != zero_zero(X_a)
| ti(X_a,Xa) != zero_zero(X_a)
| plus_plus(X_a,hAPP(nat,X_a,power_power(X_a,Xa),number_number_of(nat,bit0(bit1(pls)))),hAPP(nat,X_a,power_power(X_a,Ya),number_number_of(nat,bit0(bit1(pls))))) = zero_zero(X_a) )
& ( ( ti(X_a,Ya) = zero_zero(X_a)
& ti(X_a,Xa) = zero_zero(X_a) )
| plus_plus(X_a,hAPP(nat,X_a,power_power(X_a,Xa),number_number_of(nat,bit0(bit1(pls)))),hAPP(nat,X_a,power_power(X_a,Ya),number_number_of(nat,bit0(bit1(pls))))) != zero_zero(X_a) ) )
| ~ linordered_idom(X_a) ),
inference(NNF_transformation,[status(thm)],[f1463]) ).
fof(f1465,plain,
! [X_a] :
( ( ! [Xa,Ya] :
( ti(X_a,Ya) != zero_zero(X_a)
| ti(X_a,Xa) != zero_zero(X_a)
| plus_plus(X_a,hAPP(nat,X_a,power_power(X_a,Xa),number_number_of(nat,bit0(bit1(pls)))),hAPP(nat,X_a,power_power(X_a,Ya),number_number_of(nat,bit0(bit1(pls))))) = zero_zero(X_a) )
& ! [Xa,Ya] :
( ( ti(X_a,Ya) = zero_zero(X_a)
& ti(X_a,Xa) = zero_zero(X_a) )
| plus_plus(X_a,hAPP(nat,X_a,power_power(X_a,Xa),number_number_of(nat,bit0(bit1(pls)))),hAPP(nat,X_a,power_power(X_a,Ya),number_number_of(nat,bit0(bit1(pls))))) != zero_zero(X_a) ) )
| ~ linordered_idom(X_a) ),
inference(miniscoping,[status(thm)],[f1464]) ).
fof(f1466,plain,
! [X0,X1,X2] :
( ti(X0,X1) = zero_zero(X0)
| plus_plus(X0,hAPP(nat,X0,power_power(X0,X1),number_number_of(nat,bit0(bit1(pls)))),hAPP(nat,X0,power_power(X0,X2),number_number_of(nat,bit0(bit1(pls))))) != zero_zero(X0)
| ~ linordered_idom(X0) ),
inference(cnf_transformation,[status(thm)],[f1465]) ).
fof(f1529,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f1559,plain,
! [K,L_1] :
( ( ti(int,K) != ti(int,L_1)
| bit1(K) = bit1(L_1) )
& ( ti(int,K) = ti(int,L_1)
| bit1(K) != bit1(L_1) ) ),
inference(NNF_transformation,[status(thm)],[f140]) ).
fof(f1560,plain,
( ! [K,L_1] :
( ti(int,K) != ti(int,L_1)
| bit1(K) = bit1(L_1) )
& ! [K,L_1] :
( ti(int,K) = ti(int,L_1)
| bit1(K) != bit1(L_1) ) ),
inference(miniscoping,[status(thm)],[f1559]) ).
fof(f1561,plain,
! [X0,X1] :
( ti(int,X0) = ti(int,X1)
| bit1(X0) != bit1(X1) ),
inference(cnf_transformation,[status(thm)],[f1560]) ).
fof(f1605,plain,
! [K] :
( ( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),K))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),bit0(K))) )
& ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),K))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),bit0(K))) ) ),
inference(NNF_transformation,[status(thm)],[f153]) ).
fof(f1606,plain,
( ! [K] :
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),K))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),bit0(K))) )
& ! [K] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),K))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),bit0(K))) ) ),
inference(miniscoping,[status(thm)],[f1605]) ).
fof(f1608,plain,
! [X0] :
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),X0))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),bit0(X0))) ),
inference(cnf_transformation,[status(thm)],[f1606]) ).
fof(f1648,plain,
! [K] :
( ( ti(int,K) != pls
| bit0(K) = pls )
& ( ti(int,K) = pls
| bit0(K) != pls ) ),
inference(NNF_transformation,[status(thm)],[f168]) ).
fof(f1649,plain,
( ! [K] :
( ti(int,K) != pls
| bit0(K) = pls )
& ! [K] :
( ti(int,K) = pls
| bit0(K) != pls ) ),
inference(miniscoping,[status(thm)],[f1648]) ).
fof(f1650,plain,
! [X0] :
( ti(int,X0) = pls
| bit0(X0) != pls ),
inference(cnf_transformation,[status(thm)],[f1649]) ).
fof(f1651,plain,
! [X0] :
( ti(int,X0) != pls
| bit0(X0) = pls ),
inference(cnf_transformation,[status(thm)],[f1649]) ).
fof(f1656,plain,
bit0(pls) = pls,
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f1657,plain,
pls = zero_zero(int),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f1659,plain,
! [X0] : plus_plus(int,X0,pls) = ti(int,X0),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f1689,plain,
! [X0] : bit1(X0) = plus_plus(int,plus_plus(int,one_one(int),X0),X0),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f4406,plain,
linordered_idom(int),
inference(cnf_transformation,[status(thm)],[f1122]) ).
fof(f4535,plain,
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(cnf_transformation,[status(thm)],[f1252]) ).
fof(f4683,plain,
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)))) = pls,
inference(backward_demodulation,[status(thm)],[f1657,f4535]) ).
fof(f4691,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(forward_demodulation,[status(thm)],[f1657,f1461]) ).
fof(f4756,plain,
( ti(int,pls) = pls
| pls != pls ),
inference(paramodulation,[status(thm)],[f1656,f1650]) ).
fof(f4758,definition,
( sQ6_spl
<=> pls = pls ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f4760,plain,
( sQ6_spl
| pls != pls ),
inference(component_clause,[status(thm)],[f4758]) ).
fof(f4761,definition,
( sQ7_spl
<=> ti(int,pls) = pls ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f4764,plain,
( sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f4756,f4758,f4761]) ).
fof(f4765,plain,
( sQ6_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4760]) ).
fof(f4766,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f4765]) ).
fof(f5032,plain,
! [X0] : ti(int,ti(int,X0)) = ti(int,X0),
inference(resolution,[status(thm)],[f1561,f1367]) ).
fof(f5414,definition,
( sQ24_spl
<=> hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f5415,plain,
( ~ sQ24_spl
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)) ),
inference(component_clause,[status(thm)],[f5414]) ).
fof(f5919,plain,
( ~ sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5415,f1529]) ).
fof(f5920,plain,
~ sQ24_spl,
inference(contradiction_clause,[status(thm)],[f5919]) ).
fof(f6094,plain,
bit1(pls) = ti(int,plus_plus(int,one_one(int),pls)),
inference(paramodulation,[status(thm)],[f1659,f1689]) ).
fof(f6117,plain,
bit1(pls) = ti(int,ti(int,one_one(int))),
inference(forward_demodulation,[status(thm)],[f1659,f6094]) ).
fof(f6118,plain,
bit1(pls) = ti(int,one_one(int)),
inference(forward_demodulation,[status(thm)],[f5032,f6117]) ).
fof(f6159,plain,
bit0(bit1(pls)) = bit0(one_one(int)),
inference(paramodulation,[status(thm)],[f6118,f1365]) ).
fof(f6286,plain,
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(one_one(int)))) = pls,
inference(backward_demodulation,[status(thm)],[f6159,f4683]) ).
fof(f7234,plain,
! [X0,X1,X2] :
( ti(X0,X1) = zero_zero(X0)
| plus_plus(X0,hAPP(nat,X0,power_power(X0,X1),number_number_of(nat,bit0(one_one(int)))),hAPP(nat,X0,power_power(X0,X2),number_number_of(nat,bit0(bit1(pls))))) != zero_zero(X0)
| ~ linordered_idom(X0) ),
inference(forward_demodulation,[status(thm)],[f6159,f1466]) ).
fof(f7235,plain,
! [X0,X1,X2] :
( ti(X0,X1) = zero_zero(X0)
| plus_plus(X0,hAPP(nat,X0,power_power(X0,X1),number_number_of(nat,bit0(one_one(int)))),hAPP(nat,X0,power_power(X0,X2),number_number_of(nat,bit0(one_one(int))))) != zero_zero(X0)
| ~ linordered_idom(X0) ),
inference(forward_demodulation,[status(thm)],[f6159,f7234]) ).
fof(f7245,plain,
! [X0] :
( ti(int,X0) = zero_zero(int)
| plus_plus(int,hAPP(nat,int,power_power(int,X0),number_number_of(nat,bit0(one_one(int)))),pls) != zero_zero(int)
| ~ linordered_idom(int) ),
inference(paramodulation,[status(thm)],[f6286,f7235]) ).
fof(f7266,definition,
( sQ155_spl
<=> linordered_idom(int) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f7268,plain,
( sQ155_spl
| ~ linordered_idom(int) ),
inference(component_clause,[status(thm)],[f7266]) ).
fof(f7281,definition,
( sQ159_spl
<=> ti(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))) = zero_zero(int) ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f7282,plain,
( ~ sQ159_spl
| ti(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))) = zero_zero(int) ),
inference(component_clause,[status(thm)],[f7281]) ).
fof(f7283,plain,
( sQ159_spl
| ti(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))) != zero_zero(int) ),
inference(component_clause,[status(thm)],[f7281]) ).
fof(f7289,definition,
! [X0] :
( sQ161_spl
<=> ( ti(int,X0) = zero_zero(int)
| plus_plus(int,hAPP(nat,int,power_power(int,X0),number_number_of(nat,bit0(one_one(int)))),pls) != zero_zero(int) ) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f7290,plain,
! [X0] :
( ~ sQ161_spl
| ti(int,X0) = zero_zero(int)
| plus_plus(int,hAPP(nat,int,power_power(int,X0),number_number_of(nat,bit0(one_one(int)))),pls) != zero_zero(int) ),
inference(component_clause,[status(thm)],[f7289]) ).
fof(f7292,plain,
( sQ161_spl
| ~ sQ155_spl ),
inference(split_clause,[status(thm)],[f7245,f7266,f7289]) ).
fof(f7297,plain,
( sQ155_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7268,f4406]) ).
fof(f7298,plain,
sQ155_spl,
inference(contradiction_clause,[status(thm)],[f7297]) ).
fof(f7307,plain,
! [X0] :
( ~ sQ161_spl
| ti(int,X0) = zero_zero(int)
| ti(int,hAPP(nat,int,power_power(int,X0),number_number_of(nat,bit0(one_one(int))))) != zero_zero(int) ),
inference(forward_demodulation,[status(thm)],[f1659,f7290]) ).
fof(f7308,plain,
! [X0] :
( ~ sQ161_spl
| ti(int,X0) = zero_zero(int)
| ti(int,hAPP(nat,int,power_power(int,X0),number_number_of(nat,bit0(one_one(int))))) != pls ),
inference(forward_demodulation,[status(thm)],[f1657,f7307]) ).
fof(f7309,plain,
! [X0] :
( ~ sQ161_spl
| ti(int,X0) = pls
| ti(int,hAPP(nat,int,power_power(int,X0),number_number_of(nat,bit0(one_one(int))))) != pls ),
inference(forward_demodulation,[status(thm)],[f1657,f7308]) ).
fof(f7356,plain,
( ~ sQ159_spl
| ti(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))) = pls ),
inference(forward_demodulation,[status(thm)],[f1657,f7282]) ).
fof(f7385,plain,
( ~ sQ159_spl
| pls != pls
| bit0(plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))) = pls ),
inference(paramodulation,[status(thm)],[f7356,f1651]) ).
fof(f7403,definition,
( sQ172_spl
<=> bit0(plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))) = pls ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f7404,plain,
( ~ sQ172_spl
| bit0(plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))) = pls ),
inference(component_clause,[status(thm)],[f7403]) ).
fof(f7406,plain,
( ~ sQ159_spl
| ~ sQ6_spl
| sQ172_spl ),
inference(split_clause,[status(thm)],[f7385,f7403,f4758,f7281]) ).
fof(f7410,plain,
( sQ159_spl
| ti(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))) != pls ),
inference(forward_demodulation,[status(thm)],[f1657,f7283]) ).
fof(f7411,plain,
( ~ sQ161_spl
| ti(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))) = pls
| ti(int,pls) != pls ),
inference(paramodulation,[status(thm)],[f6286,f7309]) ).
fof(f7413,definition,
( sQ173_spl
<=> ti(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))) = pls ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f7414,plain,
( ~ sQ173_spl
| ti(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))) = pls ),
inference(component_clause,[status(thm)],[f7413]) ).
fof(f7416,plain,
( ~ sQ161_spl
| sQ173_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f7411,f4761,f7413,f7289]) ).
fof(f7417,plain,
( ~ sQ173_spl
| sQ159_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7414,f7410]) ).
fof(f7418,plain,
( ~ sQ173_spl
| sQ159_spl ),
inference(contradiction_clause,[status(thm)],[f7417]) ).
fof(f7781,plain,
( ~ sQ172_spl
| ~ 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))))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)) ),
inference(paramodulation,[status(thm)],[f7404,f1608]) ).
fof(f7808,definition,
( sQ228_spl
<=> 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)))) ),
introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition]) ).
fof(f7810,plain,
( sQ228_spl
| ~ 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(component_clause,[status(thm)],[f7808]) ).
fof(f7811,plain,
( ~ sQ172_spl
| ~ sQ228_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f7781,f5414,f7808,f7403]) ).
fof(f7827,plain,
( sQ228_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7810,f4691]) ).
fof(f7828,plain,
sQ228_spl,
inference(contradiction_clause,[status(thm)],[f7827]) ).
fof(f7829,plain,
$false,
inference(sat_refutation,[status(thm)],[f4764,f4766,f5920,f7292,f7298,f7406,f7416,f7418,f7811,f7828]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM925+7 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n008.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 03:18:55 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.24/0.50 % Drodi V4.1.1
% 2.33/0.86 % Refutation found
% 2.33/0.86 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.33/0.86 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.33/0.90 % Elapsed time: 0.519307 seconds
% 2.33/0.90 % CPU time: 2.971236 seconds
% 2.33/0.90 % Total memory used: 258.251 MB
% 2.33/0.90 % Net memory used: 256.195 MB
%------------------------------------------------------------------------------