%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR116+10 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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 12:14:08 PM UTC 2026
% Result : Theorem 80.26s 10.57s
% Output : CNFRefutation 71.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 23
% Syntax : Number of formulae : 129 ( 23 unt; 14 def)
% Number of atoms : 904 ( 0 equ)
% Maximal formula atoms : 367 ( 7 avg)
% Number of connectives : 1116 ( 341 ~; 298 |; 458 &)
% ( 14 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 367 ( 10 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 44 ( 43 usr; 15 prp; 0-12 aty)
% Number of functors : 94 ( 94 usr; 86 con; 0-3 aty)
% Number of variables : 275 ( 235 !; 40 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : member(X0,cons(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X0,X1] :
( fact(X0,X1)
=> has_fact_leq(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f95,axiom,
! [X0,X1] :
( ( loc(X1,X0)
& has_fact_leq(X1,real) )
=> ? [X2] :
( subs(X2,geben_1_1)
& obj(X2,X1)
& loc(X2,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f155,axiom,
! [X0,X1,X2] :
( ( state_adjective_state_binding(X1,X2)
& prop(X0,X1) )
=> ? [X3,X4,X5] :
( val(X4,X2)
& sub(X4,name_1_1)
& sub(X3,land_1_1)
& loc(X0,X5)
& attr(X3,X4)
& in(X5,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f159,axiom,
! [X0,X1,X2] :
( ( sub(X0,X1)
& member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
& attr(X2,X0) )
=> ? [X3] :
( subs(X3,hei__337en_1_1)
& arg2(X3,X2)
& arg1(X3,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f161,axiom,
! [X0,X1,X2] :
( ( subs(X0,hei__337en_1_1)
& arg2(X0,X2)
& arg1(X0,X1) )
=> ? [X3,X4] :
( subs(X3,bezeichnen_1_1)
& subr(X4,rprs_0)
& obj(X3,X1)
& mcont(X3,X4)
& hsit(X0,X3)
& arg2(X4,X2)
& arg1(X4,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9161,axiom,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10188,conjecture,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( val(X7,s__374dafrika_0)
& val(X2,nelson_0)
& val(X1,mandela_0)
& subr(X3,rprs_0)
& sub(X7,name_1_1)
& sub(X4,X9)
& sub(X2,eigenname_1_1)
& sub(X1,familiename_1_1)
& obj(X8,X0)
& attr(X6,X7)
& attr(X0,X2)
& attr(X0,X1)
& arg2(X3,X4)
& arg1(X3,X0)
& in(X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10189,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( val(X7,s__374dafrika_0)
& val(X2,nelson_0)
& val(X1,mandela_0)
& subr(X3,rprs_0)
& sub(X7,name_1_1)
& sub(X4,X9)
& sub(X2,eigenname_1_1)
& sub(X1,familiename_1_1)
& obj(X8,X0)
& attr(X6,X7)
& attr(X0,X2)
& attr(X0,X1)
& arg2(X3,X4)
& arg1(X3,X0)
& in(X5,X6) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,hypothesis,
( varia(sekret__344r_1_1,varia_c)
& refer(sekret__344r_1_1,refer_c)
& quant(sekret__344r_1_1,one)
& gener(sekret__344r_1_1,ge)
& fact(sekret__344r_1_1,real)
& etype(sekret__344r_1_1,int0)
& card(sekret__344r_1_1,int1)
& sort(sekret__344r_1_1,d)
& sort(allgemein_1_1,tq)
& varia(c28553,varia_c)
& refer(c28553,refer_c)
& quant(c28553,quant_c)
& gener(c28553,gener_c)
& fact(c28553,real)
& etype(c28553,etype_c)
& card(c28553,card_c)
& sort(c28553,ent)
& sort(lesotho_0,fe)
& varia(c28535,varia_c)
& refer(c28535,indet)
& quant(c28535,one)
& gener(c28535,sp)
& fact(c28535,real)
& etype(c28535,int0)
& card(c28535,int1)
& sort(c28535,na)
& varia(c28534,con)
& refer(c28534,det)
& quant(c28534,one)
& gener(c28534,sp)
& fact(c28534,real)
& etype(c28534,int0)
& card(c28534,int1)
& sort(c28534,io)
& sort(c28534,d)
& varia(krise_1_1,varia_c)
& refer(krise_1_1,refer_c)
& quant(krise_1_1,one)
& gener(krise_1_1,ge)
& fact(krise_1_1,real)
& etype(krise_1_1,int0)
& card(krise_1_1,int1)
& sort(krise_1_1,ad)
& varia(c28514,con)
& refer(c28514,det)
& quant(c28514,one)
& gener(c28514,sp)
& fact(c28514,real)
& etype(c28514,int0)
& card(c28514,int1)
& sort(c28514,ad)
& varia(stunde_1_1,varia_c)
& refer(stunde_1_1,refer_c)
& quant(stunde_1_1,quant_c)
& gener(stunde_1_1,ge)
& fact(stunde_1_1,real)
& etype(stunde_1_1,etype_c)
& card(stunde_1_1,card_c)
& sort(stunde_1_1,ta)
& sort(stunde_1_1,oa)
& sort(stunde_1_1,me)
& card(c28504,int6)
& sort(c28504,nu)
& varia(c28511,varia_c)
& refer(c28511,refer_c)
& quant(c28511,quant_c)
& gener(c28511,gener_c)
& fact(c28511,real)
& etype(c28511,etype_c)
& card(c28511,card_c)
& sort(c28511,ta)
& sort(c28511,m)
& sort(pretoria_0,fe)
& varia(stadt__1_1,varia_c)
& refer(stadt__1_1,refer_c)
& quant(stadt__1_1,one)
& gener(stadt__1_1,ge)
& fact(stadt__1_1,real)
& etype(stadt__1_1,int0)
& card(stadt__1_1,int1)
& sort(stadt__1_1,io)
& sort(stadt__1_1,d)
& varia(c28503,varia_c)
& refer(c28503,indet)
& quant(c28503,one)
& gener(c28503,sp)
& fact(c28503,real)
& etype(c28503,int0)
& card(c28503,int1)
& sort(c28503,na)
& varia(c28502,con)
& refer(c28502,det)
& quant(c28502,one)
& gener(c28502,sp)
& fact(c28502,real)
& etype(c28502,int0)
& card(c28502,int1)
& sort(c28502,io)
& sort(c28502,d)
& sort(mugabe_0,fe)
& varia(c28497,varia_c)
& refer(c28497,indet)
& quant(c28497,one)
& gener(c28497,sp)
& fact(c28497,real)
& etype(c28497,int0)
& card(c28497,int1)
& sort(c28497,na)
& varia(c28496,con)
& refer(c28496,det)
& quant(c28496,one)
& gener(c28496,sp)
& fact(c28496,real)
& etype(c28496,int0)
& card(c28496,int1)
& sort(c28496,d)
& sort(ahmed_0,fe)
& sort(salim_0,fe)
& sort(c28489,fe)
& varia(mensch_1_1,varia_c)
& refer(mensch_1_1,refer_c)
& quant(mensch_1_1,one)
& gener(mensch_1_1,ge)
& fact(mensch_1_1,real)
& etype(mensch_1_1,int0)
& card(mensch_1_1,int1)
& sort(mensch_1_1,d)
& varia(c28490,varia_c)
& refer(c28490,indet)
& quant(c28490,one)
& gener(c28490,sp)
& fact(c28490,real)
& etype(c28490,int0)
& card(c28490,int1)
& sort(c28490,na)
& varia(c28488,varia_c)
& refer(c28488,indet)
& quant(c28488,one)
& gener(c28488,sp)
& fact(c28488,real)
& etype(c28488,int0)
& card(c28488,int1)
& sort(c28488,na)
& varia(c28487,con)
& refer(c28487,det)
& quant(c28487,one)
& gener(c28487,sp)
& fact(c28487,real)
& etype(c28487,int0)
& card(c28487,int1)
& sort(c28487,d)
& varia(einheit_1_1,varia_c)
& refer(einheit_1_1,refer_c)
& quant(einheit_1_1,one)
& gener(einheit_1_1,ge)
& fact(einheit_1_1,real)
& etype(einheit_1_1,int0)
& card(einheit_1_1,int1)
& sort(einheit_1_1,oa)
& sort(einheit_1_1,io)
& sort(afrikanisch__1_1,nq)
& varia(c28477,varia_c)
& refer(c28477,refer_c)
& quant(c28477,one)
& gener(c28477,gener_c)
& fact(c28477,real)
& etype(c28477,int0)
& card(c28477,int1)
& sort(c28477,oa)
& sort(c28477,io)
& varia(organisation_1_1,varia_c)
& refer(organisation_1_1,refer_c)
& quant(organisation_1_1,quant_c)
& gener(organisation_1_1,ge)
& fact(organisation_1_1,real)
& etype(organisation_1_1,int1)
& card(organisation_1_1,card_c)
& sort(organisation_1_1,io)
& sort(organisation_1_1,d)
& varia(c28473,con)
& refer(c28473,det)
& quant(c28473,one)
& gener(c28473,sp)
& fact(c28473,real)
& etype(c28473,int1)
& card(c28473,int1)
& sort(c28473,io)
& sort(c28473,d)
& varia(generalsekretaer_1_1,varia_c)
& refer(generalsekretaer_1_1,refer_c)
& quant(generalsekretaer_1_1,one)
& gener(generalsekretaer_1_1,ge)
& fact(generalsekretaer_1_1,real)
& etype(generalsekretaer_1_1,int0)
& card(generalsekretaer_1_1,int1)
& sort(generalsekretaer_1_1,d)
& varia(c28468,con)
& refer(c28468,det)
& quant(c28468,one)
& gener(c28468,sp)
& fact(c28468,real)
& etype(c28468,int0)
& card(c28468,int1)
& sort(c28468,d)
& varia(masire_1_1,varia_c)
& refer(masire_1_1,refer_c)
& quant(masire_1_1,one)
& gener(masire_1_1,ge)
& fact(masire_1_1,real)
& etype(masire_1_1,int0)
& card(masire_1_1,int1)
& sort(masire_1_1,o)
& varia(c28460,varia_c)
& refer(c28460,refer_c)
& quant(c28460,one)
& gener(c28460,gener_c)
& fact(c28460,real)
& etype(c28460,int0)
& card(c28460,int1)
& sort(c28460,o)
& varia(quett_1_1,varia_c)
& refer(quett_1_1,refer_c)
& quant(quett_1_1,one)
& gener(quett_1_1,ge)
& fact(quett_1_1,real)
& etype(quett_1_1,int0)
& card(quett_1_1,int1)
& sort(quett_1_1,o)
& varia(c28459,varia_c)
& refer(c28459,refer_c)
& quant(c28459,one)
& gener(c28459,gener_c)
& fact(c28459,real)
& etype(c28459,int0)
& card(c28459,int1)
& sort(c28459,o)
& sort(botswana_0,fe)
& varia(name_1_1,varia_c)
& refer(name_1_1,refer_c)
& quant(name_1_1,one)
& gener(name_1_1,ge)
& fact(name_1_1,real)
& etype(name_1_1,int0)
& card(name_1_1,int1)
& sort(name_1_1,na)
& varia(land_1_1,varia_c)
& refer(land_1_1,refer_c)
& quant(land_1_1,one)
& gener(land_1_1,ge)
& fact(land_1_1,real)
& etype(land_1_1,int0)
& card(land_1_1,int1)
& sort(land_1_1,io)
& sort(land_1_1,d)
& varia(c28458,varia_c)
& refer(c28458,indet)
& quant(c28458,one)
& gener(c28458,sp)
& fact(c28458,real)
& etype(c28458,int0)
& card(c28458,int1)
& sort(c28458,na)
& varia(c28457,con)
& refer(c28457,det)
& quant(c28457,one)
& gener(c28457,sp)
& fact(c28457,real)
& etype(c28457,int0)
& card(c28457,int1)
& sort(c28457,io)
& sort(c28457,d)
& sort(mandela_0,fe)
& varia(familiename_1_1,varia_c)
& refer(familiename_1_1,refer_c)
& quant(familiename_1_1,one)
& gener(familiename_1_1,ge)
& fact(familiename_1_1,real)
& etype(familiename_1_1,int0)
& card(familiename_1_1,int1)
& sort(familiename_1_1,na)
& sort(nelson_0,fe)
& varia(eigenname_1_1,varia_c)
& refer(eigenname_1_1,refer_c)
& quant(eigenname_1_1,one)
& gener(eigenname_1_1,ge)
& fact(eigenname_1_1,real)
& etype(eigenname_1_1,int0)
& card(eigenname_1_1,int1)
& sort(eigenname_1_1,na)
& varia(pr__344sident_1_1,varia_c)
& refer(pr__344sident_1_1,refer_c)
& quant(pr__344sident_1_1,one)
& gener(pr__344sident_1_1,ge)
& fact(pr__344sident_1_1,real)
& etype(pr__344sident_1_1,int0)
& card(pr__344sident_1_1,int1)
& sort(pr__344sident_1_1,d)
& sort(s__374dafrikanisch_1_1,nq)
& varia(c28446,varia_c)
& refer(c28446,indet)
& quant(c28446,one)
& gener(c28446,sp)
& fact(c28446,real)
& etype(c28446,int0)
& card(c28446,int1)
& sort(c28446,na)
& varia(c28445,varia_c)
& refer(c28445,indet)
& quant(c28445,one)
& gener(c28445,sp)
& fact(c28445,real)
& etype(c28445,int0)
& card(c28445,int1)
& sort(c28445,na)
& varia(c28444,con)
& refer(c28444,det)
& quant(c28444,one)
& gener(c28444,sp)
& fact(c28444,real)
& etype(c28444,int0)
& card(c28444,int1)
& sort(c28444,d)
& sub(generalsekretaer_1_1,sekret__344r_1_1)
& assoc(generalsekretaer_1_1,allgemein_1_1)
& tupl_p12(c28553,c28444,c28457,c28459,c28460,c28468,c28487,c28496,c28502,c28511,c28514,c28534)
& val(c28535,lesotho_0)
& sub(c28535,name_1_1)
& sub(c28534,land_1_1)
& attr(c28534,c28535)
& subs(c28514,krise_1_1)
& quant_p3(c28511,c28504,stunde_1_1)
& val(c28503,pretoria_0)
& sub(c28503,name_1_1)
& sub(c28502,stadt__1_1)
& attr(c28502,c28503)
& val(c28497,mugabe_0)
& sub(c28497,familiename_1_1)
& sub(c28496,mensch_1_1)
& attr(c28496,c28497)
& val(c28490,salim_0)
& sub(c28490,familiename_1_1)
& tupl(c28489,salim_0,ahmed_0)
& val(c28488,c28489)
& sub(c28488,eigenname_1_1)
& sub(c28487,mensch_1_1)
& attr(c28487,c28490)
& attr(c28487,c28488)
& sub(c28477,einheit_1_1)
& prop(c28477,afrikanisch__1_1)
& attch(c28477,c28473)
& sub(c28473,organisation_1_1)
& attch(c28473,c28468)
& sub(c28468,generalsekretaer_1_1)
& sub(c28460,masire_1_1)
& sub(c28459,quett_1_1)
& val(c28458,botswana_0)
& sub(c28458,name_1_1)
& sub(c28457,land_1_1)
& attr(c28457,c28458)
& val(c28446,mandela_0)
& sub(c28446,familiename_1_1)
& val(c28445,nelson_0)
& sub(c28445,eigenname_1_1)
& sub(c28444,pr__344sident_1_1)
& prop(c28444,s__374dafrikanisch_1_1)
& attr(c28444,c28446)
& attr(c28444,c28445) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10191,plain,
! [X0,X1] : member(X0,cons(X0,X1)),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f10209,plain,
! [X0,X1] :
( has_fact_leq(X0,X1)
| ~ fact(X0,X1) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f10210,plain,
! [X0,X1] :
( ~ fact(X0,X1)
| has_fact_leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10209]) ).
fof(f10363,plain,
! [X0,X1] :
( ? [X2] :
( subs(X2,geben_1_1)
& obj(X2,X1)
& loc(X2,X0) )
| ~ loc(X1,X0)
| ~ has_fact_leq(X1,real) ),
inference(pre_NNF_transformation,[status(thm)],[f95]) ).
fof(f10364,plain,
! [X0,X1] :
( ( subs(sK2_skl(X1,X0),geben_1_1)
& obj(sK2_skl(X1,X0),X1)
& loc(sK2_skl(X1,X0),X0) )
| ~ loc(X1,X0)
| ~ has_fact_leq(X1,real) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X2,sK2_skl(X1,X0))],[f10363]) ).
fof(f10366,plain,
! [X0,X1] :
( ~ loc(X0,X1)
| ~ has_fact_leq(X0,real)
| obj(sK2_skl(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f10364]) ).
fof(f10674,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( val(X4,X2)
& sub(X4,name_1_1)
& sub(X3,land_1_1)
& loc(X0,X5)
& attr(X3,X4)
& in(X5,X3) )
| ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1) ),
inference(pre_NNF_transformation,[status(thm)],[f155]) ).
fof(f10675,plain,
! [X0,X2] :
( ? [X4] :
( val(X4,X2)
& sub(X4,name_1_1)
& ? [X3] :
( sub(X3,land_1_1)
& ? [X5] :
( loc(X0,X5)
& attr(X3,X4)
& in(X5,X3) ) ) )
| ! [X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1) ) ),
inference(miniscoping,[status(thm)],[f10674]) ).
fof(f10676,plain,
! [X0,X2] :
( ( val(sK47_skl(X2,X0),X2)
& sub(sK47_skl(X2,X0),name_1_1)
& sub(sK48_skl(X2,X0),land_1_1)
& loc(X0,sK49_skl(X2,X0))
& attr(sK48_skl(X2,X0),sK47_skl(X2,X0))
& in(sK49_skl(X2,X0),sK48_skl(X2,X0)) )
| ! [X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl]),skolemize(X4,sK47_skl(X2,X0)),skolemize(X3,sK48_skl(X2,X0)),skolemize(X5,sK49_skl(X2,X0))],[f10675]) ).
fof(f10677,plain,
! [X0,X1,X2] :
( ~ prop(X2,X0)
| in(sK49_skl(X1,X2),sK48_skl(X1,X2))
| ~ state_adjective_state_binding(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10676]) ).
fof(f10678,plain,
! [X0,X1,X2] :
( ~ prop(X2,X0)
| attr(sK48_skl(X1,X2),sK47_skl(X1,X2))
| ~ state_adjective_state_binding(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10676]) ).
fof(f10679,plain,
! [X0,X1,X2] :
( ~ state_adjective_state_binding(X2,X1)
| ~ prop(X0,X2)
| loc(X0,sK49_skl(X1,X0)) ),
inference(cnf_transformation,[status(thm)],[f10676]) ).
fof(f10681,plain,
! [X0,X1,X2] :
( ~ state_adjective_state_binding(X2,X0)
| ~ prop(X1,X2)
| sub(sK47_skl(X0,X1),name_1_1) ),
inference(cnf_transformation,[status(thm)],[f10676]) ).
fof(f10682,plain,
! [X0,X1,X2] :
( ~ state_adjective_state_binding(X2,X0)
| ~ prop(X1,X2)
| val(sK47_skl(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f10676]) ).
fof(f10692,plain,
! [X0,X1,X2] :
( ? [X3] :
( subs(X3,hei__337en_1_1)
& arg2(X3,X2)
& arg1(X3,X2) )
| ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X2,X0) ),
inference(pre_NNF_transformation,[status(thm)],[f159]) ).
fof(f10693,plain,
! [X2] :
( ? [X3] :
( subs(X3,hei__337en_1_1)
& arg2(X3,X2)
& arg1(X3,X2) )
| ! [X0,X1] :
( ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X2,X0) ) ),
inference(miniscoping,[status(thm)],[f10692]) ).
fof(f10694,plain,
! [X2] :
( ( subs(sK50_skl(X2),hei__337en_1_1)
& arg2(sK50_skl(X2),X2)
& arg1(sK50_skl(X2),X2) )
| ! [X0,X1] :
( ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X2,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50_skl]),skolemize(X3,sK50_skl(X2))],[f10693]) ).
fof(f10695,plain,
! [X0,X1,X2] :
( ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X1,X2)
| arg1(sK50_skl(X0),X0)
| ~ attr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10694]) ).
fof(f10696,plain,
! [X0,X1,X2] :
( ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X1,X2)
| arg2(sK50_skl(X0),X0)
| ~ attr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10694]) ).
fof(f10697,plain,
! [X0,X1,X2] :
( ~ attr(X0,X2)
| ~ sub(X2,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| subs(sK50_skl(X0),hei__337en_1_1) ),
inference(cnf_transformation,[status(thm)],[f10694]) ).
fof(f10705,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( subs(X3,bezeichnen_1_1)
& subr(X4,rprs_0)
& obj(X3,X1)
& mcont(X3,X4)
& hsit(X0,X3)
& arg2(X4,X2)
& arg1(X4,X1) )
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(pre_NNF_transformation,[status(thm)],[f161]) ).
fof(f10706,plain,
! [X0,X1,X2] :
( ? [X3] :
( subs(X3,bezeichnen_1_1)
& ? [X4] :
( subr(X4,rprs_0)
& obj(X3,X1)
& mcont(X3,X4)
& hsit(X0,X3)
& arg2(X4,X2)
& arg1(X4,X1) ) )
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(miniscoping,[status(thm)],[f10705]) ).
fof(f10707,plain,
! [X0,X1,X2] :
( ( subs(sK52_skl(X2,X1,X0),bezeichnen_1_1)
& subr(sK53_skl(X2,X1,X0),rprs_0)
& obj(sK52_skl(X2,X1,X0),X1)
& mcont(sK52_skl(X2,X1,X0),sK53_skl(X2,X1,X0))
& hsit(X0,sK52_skl(X2,X1,X0))
& arg2(sK53_skl(X2,X1,X0),X2)
& arg1(sK53_skl(X2,X1,X0),X1) )
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52_skl,sK53_skl]),skolemize(X3,sK52_skl(X2,X1,X0)),skolemize(X4,sK53_skl(X2,X1,X0))],[f10706]) ).
fof(f10708,plain,
! [X0,X1,X2] :
( arg1(sK53_skl(X1,X2,X0),X2)
| ~ subs(X0,hei__337en_1_1)
| ~ arg1(X0,X2)
| ~ arg2(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10707]) ).
fof(f10709,plain,
! [X0,X1,X2] :
( ~ subs(X0,hei__337en_1_1)
| arg2(sK53_skl(X1,X2,X0),X1)
| ~ arg1(X0,X2)
| ~ arg2(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10707]) ).
fof(f10713,plain,
! [X0,X1,X2] :
( ~ arg2(X0,X2)
| subr(sK53_skl(X2,X1,X0),rprs_0)
| ~ arg1(X0,X1)
| ~ subs(X0,hei__337en_1_1) ),
inference(cnf_transformation,[status(thm)],[f10707]) ).
fof(f19788,plain,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
inference(cnf_transformation,[status(thm)],[f9161]) ).
fof(f20815,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ val(X7,s__374dafrika_0)
| ~ val(X2,nelson_0)
| ~ val(X1,mandela_0)
| ~ subr(X3,rprs_0)
| ~ sub(X7,name_1_1)
| ~ sub(X4,X9)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ obj(X8,X0)
| ~ attr(X6,X7)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4)
| ~ arg1(X3,X0)
| ~ in(X5,X6) ),
inference(pre_NNF_transformation,[status(thm)],[f10189]) ).
fof(f20816,plain,
! [X7] :
( ~ val(X7,s__374dafrika_0)
| ! [X2] :
( ~ val(X2,nelson_0)
| ! [X1] :
( ~ val(X1,mandela_0)
| ! [X3] :
( ~ subr(X3,rprs_0)
| ~ sub(X7,name_1_1)
| ! [X4] :
( ! [X9] : ~ sub(X4,X9)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ! [X0] :
( ! [X8] : ~ obj(X8,X0)
| ! [X6] :
( ~ attr(X6,X7)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4)
| ~ arg1(X3,X0)
| ! [X5] : ~ in(X5,X6) ) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f20815]) ).
fof(f20817,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ val(X7,s__374dafrika_0)
| ~ val(X6,nelson_0)
| ~ val(X5,mandela_0)
| ~ subr(X2,rprs_0)
| ~ sub(X7,name_1_1)
| ~ sub(X4,X9)
| ~ sub(X6,eigenname_1_1)
| ~ sub(X5,familiename_1_1)
| ~ obj(X8,X3)
| ~ attr(X1,X7)
| ~ attr(X3,X6)
| ~ attr(X3,X5)
| ~ arg2(X2,X4)
| ~ arg1(X2,X3)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f20816]) ).
fof(f20818,plain,
attr(c28444,c28445),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20819,plain,
attr(c28444,c28446),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20820,plain,
prop(c28444,s__374dafrikanisch_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20821,plain,
sub(c28444,pr__344sident_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20822,plain,
sub(c28445,eigenname_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20823,plain,
val(c28445,nelson_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20824,plain,
sub(c28446,familiename_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20825,plain,
val(c28446,mandela_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20866,plain,
fact(c28444,real),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f21061,plain,
fact(mensch_1_1,real),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f21220,definition,
! [X0,X1,X7] :
( sQ0_spl
<=> ( ~ val(X7,s__374dafrika_0)
| ~ sub(X7,name_1_1)
| ~ attr(X1,X7)
| ~ in(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f21221,plain,
! [X0,X1,X2] :
( ~ sQ0_spl
| ~ sub(X2,name_1_1)
| ~ attr(X1,X2)
| ~ val(X2,s__374dafrika_0)
| ~ in(X0,X1) ),
inference(component_clause,[status(thm)],[f21220]) ).
fof(f21223,definition,
! [X2,X3,X4,X5,X6,X8,X9] :
( sQ1_spl
<=> ( ~ val(X6,nelson_0)
| ~ val(X5,mandela_0)
| ~ subr(X2,rprs_0)
| ~ sub(X4,X9)
| ~ sub(X6,eigenname_1_1)
| ~ sub(X5,familiename_1_1)
| ~ obj(X8,X3)
| ~ attr(X3,X6)
| ~ attr(X3,X5)
| ~ arg2(X2,X4)
| ~ arg1(X2,X3) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f21224,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ1_spl
| ~ sub(X5,eigenname_1_1)
| ~ subr(X3,rprs_0)
| ~ obj(X6,X4)
| ~ arg2(X3,X1)
| ~ attr(X4,X0)
| ~ val(X0,mandela_0)
| ~ val(X5,nelson_0)
| ~ attr(X4,X5)
| ~ arg1(X3,X4)
| ~ sub(X1,X2)
| ~ sub(X0,familiename_1_1) ),
inference(component_clause,[status(thm)],[f21223]) ).
fof(f21226,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f20817,f21220,f21223]) ).
fof(f22141,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ attr(X2,sK47_skl(s__374dafrika_0,X3))
| ~ sub(sK47_skl(s__374dafrika_0,X3),name_1_1)
| ~ prop(X3,X0)
| ~ in(X1,X2)
| ~ state_adjective_state_binding(X0,s__374dafrika_0) ),
inference(resolution,[status(thm)],[f10682,f21221]) ).
fof(f22146,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ in(X3,X1)
| ~ prop(X2,X0)
| ~ attr(X1,sK47_skl(s__374dafrika_0,X2))
| ~ state_adjective_state_binding(X0,s__374dafrika_0) ),
inference(backward_subsumption_resolution,[status(thm)],[f22141,f10681]) ).
fof(f22751,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ prop(X3,X0)
| ~ prop(X3,X1)
| ~ in(X2,sK48_skl(s__374dafrika_0,X3))
| ~ state_adjective_state_binding(X1,s__374dafrika_0)
| ~ state_adjective_state_binding(X0,s__374dafrika_0) ),
inference(resolution,[status(thm)],[f10678,f22146]) ).
fof(f22752,plain,
! [X0,X1,X2] :
( ~ sQ0_spl
| ~ prop(X0,X1)
| ~ in(X2,sK48_skl(s__374dafrika_0,X0))
| ~ state_adjective_state_binding(X1,s__374dafrika_0)
| ~ prop(X0,s__374dafrikanisch_1_1) ),
inference(resolution,[status(thm)],[f22751,f19788]) ).
fof(f22753,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ prop(X0,s__374dafrikanisch_1_1)
| ~ in(X1,sK48_skl(s__374dafrika_0,X0))
| ~ prop(X0,s__374dafrikanisch_1_1) ),
inference(resolution,[status(thm)],[f22752,f19788]) ).
fof(f22754,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ in(X1,sK48_skl(s__374dafrika_0,X0))
| ~ prop(X0,s__374dafrikanisch_1_1) ),
inference(duplicate_literals_removal,[status(thm)],[f22753]) ).
fof(f22755,plain,
! [X0] :
( ~ sQ0_spl
| ~ in(X0,sK48_skl(s__374dafrika_0,c28444)) ),
inference(resolution,[status(thm)],[f22754,f20820]) ).
fof(f22757,plain,
! [X0] :
( ~ sQ0_spl
| ~ prop(c28444,X0)
| ~ state_adjective_state_binding(X0,s__374dafrika_0) ),
inference(resolution,[status(thm)],[f22755,f10677]) ).
fof(f22761,plain,
( ~ sQ0_spl
| ~ prop(c28444,s__374dafrikanisch_1_1) ),
inference(resolution,[status(thm)],[f22757,f19788]) ).
fof(f22762,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22761,f20820]) ).
fof(f22763,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f22762]) ).
fof(f22765,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ1_spl
| ~ sub(X4,eigenname_1_1)
| ~ subr(X2,rprs_0)
| ~ obj(X5,X3)
| ~ arg2(X2,X0)
| ~ attr(X3,c28446)
| ~ val(X4,nelson_0)
| ~ attr(X3,X4)
| ~ arg1(X2,X3)
| ~ sub(X0,X1)
| ~ sub(c28446,familiename_1_1) ),
inference(resolution,[status(thm)],[f21224,f20825]) ).
fof(f22768,definition,
( sQ2_spl
<=> sub(c28446,familiename_1_1) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f22770,plain,
( sQ2_spl
| ~ sub(c28446,familiename_1_1) ),
inference(component_clause,[status(thm)],[f22768]) ).
fof(f22771,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ3_spl
<=> ( ~ sub(X4,eigenname_1_1)
| ~ subr(X2,rprs_0)
| ~ obj(X5,X3)
| ~ arg2(X2,X0)
| ~ attr(X3,c28446)
| ~ val(X4,nelson_0)
| ~ attr(X3,X4)
| ~ arg1(X2,X3)
| ~ sub(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f22772,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ3_spl
| ~ sub(X4,X5)
| ~ arg1(X0,X1)
| ~ sub(X2,eigenname_1_1)
| ~ arg2(X0,X4)
| ~ obj(X3,X1)
| ~ val(X2,nelson_0)
| ~ attr(X1,c28446)
| ~ attr(X1,X2)
| ~ subr(X0,rprs_0) ),
inference(component_clause,[status(thm)],[f22771]) ).
fof(f22774,plain,
( ~ sQ1_spl
| sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f22765,f22768,f22771,f21223]) ).
fof(f22775,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22770,f20824]) ).
fof(f22776,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f22775]) ).
fof(f22777,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ3_spl
| ~ sub(X3,X4)
| ~ arg1(X0,c28444)
| ~ sub(X1,eigenname_1_1)
| ~ arg2(X0,X3)
| ~ obj(X2,c28444)
| ~ val(X1,nelson_0)
| ~ attr(c28444,X1)
| ~ subr(X0,rprs_0) ),
inference(resolution,[status(thm)],[f22772,f20819]) ).
fof(f22778,definition,
! [X0,X3,X4] :
( sQ4_spl
<=> ( ~ sub(X3,X4)
| ~ arg1(X0,c28444)
| ~ arg2(X0,X3)
| ~ subr(X0,rprs_0) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f22779,plain,
! [X0,X1,X2] :
( ~ sQ4_spl
| ~ arg1(X0,c28444)
| ~ sub(X1,X2)
| ~ subr(X0,rprs_0)
| ~ arg2(X0,X1) ),
inference(component_clause,[status(thm)],[f22778]) ).
fof(f22781,definition,
! [X1] :
( sQ5_spl
<=> ( ~ sub(X1,eigenname_1_1)
| ~ val(X1,nelson_0)
| ~ attr(c28444,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f22782,plain,
! [X0] :
( ~ sQ5_spl
| ~ attr(c28444,X0)
| ~ val(X0,nelson_0)
| ~ sub(X0,eigenname_1_1) ),
inference(component_clause,[status(thm)],[f22781]) ).
fof(f22784,definition,
! [X2] :
( sQ6_spl
<=> ~ obj(X2,c28444) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f22785,plain,
! [X0] :
( ~ sQ6_spl
| ~ obj(X0,c28444) ),
inference(component_clause,[status(thm)],[f22784]) ).
fof(f22787,plain,
( ~ sQ3_spl
| sQ6_spl
| sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f22777,f22778,f22781,f22784,f22771]) ).
fof(f23063,plain,
! [X0] :
( ~ sQ6_spl
| ~ loc(c28444,X0)
| ~ has_fact_leq(c28444,real) ),
inference(resolution,[status(thm)],[f22785,f10366]) ).
fof(f23067,definition,
( sQ7_spl
<=> has_fact_leq(c28444,real) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f23069,plain,
( sQ7_spl
| ~ has_fact_leq(c28444,real) ),
inference(component_clause,[status(thm)],[f23067]) ).
fof(f23070,definition,
! [X0] :
( sQ8_spl
<=> ~ loc(c28444,X0) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f23071,plain,
! [X0] :
( ~ sQ8_spl
| ~ loc(c28444,X0) ),
inference(component_clause,[status(thm)],[f23070]) ).
fof(f23073,plain,
( ~ sQ6_spl
| sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f23063,f23067,f23070,f22784]) ).
fof(f23081,plain,
! [X0,X1] :
( ~ sQ8_spl
| ~ prop(c28444,X0)
| ~ state_adjective_state_binding(X0,X1) ),
inference(resolution,[status(thm)],[f23071,f10679]) ).
fof(f23100,plain,
( ~ sQ5_spl
| ~ attr(c28444,c28445)
| ~ sub(c28445,eigenname_1_1) ),
inference(resolution,[status(thm)],[f22782,f20823]) ).
fof(f23101,definition,
( sQ13_spl
<=> sub(c28445,eigenname_1_1) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f23103,plain,
( sQ13_spl
| ~ sub(c28445,eigenname_1_1) ),
inference(component_clause,[status(thm)],[f23101]) ).
fof(f23104,definition,
( sQ14_spl
<=> attr(c28444,c28445) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f23106,plain,
( sQ14_spl
| ~ attr(c28444,c28445) ),
inference(component_clause,[status(thm)],[f23104]) ).
fof(f23107,plain,
( ~ sQ5_spl
| ~ sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f23100,f23101,f23104,f22781]) ).
fof(f23108,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23106,f20818]) ).
fof(f23109,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f23108]) ).
fof(f23110,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23103,f20822]) ).
fof(f23111,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f23110]) ).
fof(f23112,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ4_spl
| ~ arg1(sK53_skl(X1,X2,X0),c28444)
| ~ arg1(X0,X2)
| ~ sub(X3,X4)
| ~ arg2(X0,X1)
| ~ arg2(sK53_skl(X1,X2,X0),X3)
| ~ subs(X0,hei__337en_1_1) ),
inference(resolution,[status(thm)],[f22779,f10713]) ).
fof(f23117,plain,
( sQ7_spl
| ~ fact(c28444,real) ),
inference(resolution,[status(thm)],[f23069,f10210]) ).
fof(f23119,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23117,f20866]) ).
fof(f23120,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f23119]) ).
fof(f25369,definition,
! [X2] :
( sQ323_spl
<=> ~ sub(c28444,X2) ),
introduced(definition,[new_symbols(definition,[sQ323_spl])],[split_symbol_definition]) ).
fof(f25370,plain,
! [X0] :
( ~ sQ323_spl
| ~ sub(c28444,X0) ),
inference(component_clause,[status(thm)],[f25369]) ).
fof(f25398,plain,
( ~ sQ8_spl
| ~ prop(c28444,s__374dafrikanisch_1_1) ),
inference(resolution,[status(thm)],[f23081,f19788]) ).
fof(f25399,plain,
( ~ sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25398,f20820]) ).
fof(f25400,plain,
~ sQ8_spl,
inference(contradiction_clause,[status(thm)],[f25399]) ).
fof(f25402,plain,
( ~ sQ323_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f20821,f25370]) ).
fof(f25524,plain,
~ sQ323_spl,
inference(contradiction_clause,[status(thm)],[f25402]) ).
fof(f25996,plain,
! [X0,X1,X2,X3] :
( ~ sQ4_spl
| ~ arg1(sK53_skl(X1,X2,X0),c28444)
| ~ arg1(X0,X2)
| ~ sub(X1,X3)
| ~ arg2(X0,X1)
| ~ subs(X0,hei__337en_1_1)
| ~ subs(X0,hei__337en_1_1)
| ~ arg1(X0,X2)
| ~ arg2(X0,X1) ),
inference(resolution,[status(thm)],[f10709,f23112]) ).
fof(f25999,plain,
! [X0,X1,X2,X3] :
( ~ sQ4_spl
| ~ arg1(sK53_skl(X2,X1,X0),c28444)
| ~ arg2(X0,X2)
| ~ subs(X0,hei__337en_1_1)
| ~ sub(X2,X3)
| ~ arg1(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f25996]) ).
fof(f26075,plain,
! [X0,X1,X2] :
( ~ sQ4_spl
| ~ subs(X0,hei__337en_1_1)
| ~ arg1(X0,c28444)
| ~ arg2(X0,X1)
| ~ arg2(X0,X1)
| ~ subs(X0,hei__337en_1_1)
| ~ sub(X1,X2)
| ~ arg1(X0,c28444) ),
inference(resolution,[status(thm)],[f25999,f10708]) ).
fof(f26076,plain,
! [X0,X1,X2] :
( ~ sQ4_spl
| ~ sub(X1,X2)
| ~ arg1(X0,c28444)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f26075]) ).
fof(f26224,definition,
( sQ420_spl
<=> has_fact_leq(mensch_1_1,real) ),
introduced(definition,[new_symbols(definition,[sQ420_spl])],[split_symbol_definition]) ).
fof(f26226,plain,
( sQ420_spl
| ~ has_fact_leq(mensch_1_1,real) ),
inference(component_clause,[status(thm)],[f26224]) ).
fof(f26242,plain,
( sQ420_spl
| ~ fact(mensch_1_1,real) ),
inference(resolution,[status(thm)],[f26226,f10210]) ).
fof(f26244,plain,
( sQ420_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f26242,f21061]) ).
fof(f26245,plain,
sQ420_spl,
inference(contradiction_clause,[status(thm)],[f26244]) ).
fof(f26258,plain,
! [X0,X1,X2,X3] :
( ~ sQ4_spl
| ~ member(X3,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X2,X3)
| ~ attr(X0,X2)
| ~ sub(X0,X1)
| ~ arg1(sK50_skl(X0),c28444)
| ~ subs(sK50_skl(X0),hei__337en_1_1) ),
inference(resolution,[status(thm)],[f26076,f10696]) ).
fof(f26261,plain,
! [X0,X1,X2,X3] :
( ~ sQ4_spl
| ~ sub(X3,X0)
| ~ arg1(sK50_skl(X1),c28444)
| ~ attr(X1,X3)
| ~ sub(X1,X2)
| ~ member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f26258,f10697]) ).
fof(f26262,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ4_spl
| ~ member(X4,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X3,X4)
| ~ attr(c28444,X3)
| ~ sub(X2,X0)
| ~ attr(c28444,X2)
| ~ sub(c28444,X1)
| ~ member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))) ),
inference(resolution,[status(thm)],[f26261,f10695]) ).
fof(f26263,definition,
! [X0,X2] :
( sQ423_spl
<=> ( ~ sub(X2,X0)
| ~ attr(c28444,X2)
| ~ member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))) ) ),
introduced(definition,[new_symbols(definition,[sQ423_spl])],[split_symbol_definition]) ).
fof(f26264,plain,
! [X0,X1] :
( ~ sQ423_spl
| ~ attr(c28444,X1)
| ~ sub(X1,X0)
| ~ member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))) ),
inference(component_clause,[status(thm)],[f26263]) ).
fof(f26266,plain,
( ~ sQ4_spl
| sQ323_spl
| sQ423_spl ),
inference(split_clause,[status(thm)],[f26262,f26263,f25369,f22778]) ).
fof(f26268,plain,
! [X0] :
( ~ sQ423_spl
| ~ sub(X0,eigenname_1_1)
| ~ attr(c28444,X0) ),
inference(resolution,[status(thm)],[f26264,f10191]) ).
fof(f26269,plain,
( ~ sQ423_spl
| ~ sub(c28445,eigenname_1_1) ),
inference(resolution,[status(thm)],[f26268,f20818]) ).
fof(f26272,plain,
( ~ sQ423_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f26269,f23101,f26263]) ).
fof(f26273,plain,
$false,
inference(sat_refutation,[status(thm)],[f21226,f22763,f22774,f22776,f22787,f23073,f23107,f23109,f23111,f23120,f25400,f25524,f26245,f26266,f26272]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : CSR116+10 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Mon Sep 21 15:08:07 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 80.26/10.57 % Refutation found
% 80.26/10.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 80.26/10.57 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 71.51/10.69 % Elapsed time: 10.378857 seconds
% 71.51/10.69 % CPU time: 81.272394 seconds
% 71.51/10.69 % Total memory used: 646.805 MB
% 71.51/10.69 % Net memory used: 614.704 MB
%------------------------------------------------------------------------------