%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR116+29 : TPTP v9.3.1. Released v4.0.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 12:14:11 PM UTC 2026
% Result : Theorem 70.28s 9.38s
% Output : CNFRefutation 68.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 21
% Syntax : Number of formulae : 116 ( 18 unt; 13 def)
% Number of atoms : 929 ( 0 equ)
% Maximal formula atoms : 370 ( 8 avg)
% Number of connectives : 1182 ( 369 ~; 328 |; 468 &)
% ( 13 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 370 ( 11 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 42 ( 41 usr; 14 prp; 0-12 aty)
% Number of functors : 88 ( 88 usr; 80 con; 0-3 aty)
% Number of variables : 291 ( 250 !; 41 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : member(X0,cons(X0,X1)),
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(f160,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,stehen_1_b)
& scar(X3,X2)
& obj(X3,X2)
& mcont(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(macht_1_2,varia_c)
& refer(macht_1_2,refer_c)
& quant(macht_1_2,one)
& gener(macht_1_2,ge)
& fact(macht_1_2,real)
& etype(macht_1_2,int0)
& card(macht_1_2,int1)
& sort(macht_1_2,io)
& sort(macht_1_2,d)
& varia(b__374rgschaft_1_1,varia_c)
& refer(b__374rgschaft_1_1,refer_c)
& quant(b__374rgschaft_1_1,one)
& gener(b__374rgschaft_1_1,ge)
& fact(b__374rgschaft_1_1,real)
& etype(b__374rgschaft_1_1,int0)
& card(b__374rgschaft_1_1,int1)
& sort(b__374rgschaft_1_1,io)
& varia(c9590,varia_c)
& refer(c9590,refer_c)
& quant(c9590,quant_c)
& gener(c9590,gener_c)
& fact(c9590,real)
& etype(c9590,etype_c)
& card(c9590,card_c)
& sort(c9590,ent)
& sort(russland_0,fe)
& varia(c9519,varia_c)
& refer(c9519,indet)
& quant(c9519,one)
& gener(c9519,sp)
& fact(c9519,real)
& etype(c9519,int0)
& card(c9519,int1)
& sort(c9519,na)
& varia(c9518,con)
& refer(c9518,det)
& quant(c9518,one)
& gener(c9518,sp)
& fact(c9518,real)
& etype(c9518,int0)
& card(c9518,int1)
& sort(c9518,io)
& sort(c9518,d)
& sort(portugal_0,fe)
& varia(c9506,varia_c)
& refer(c9506,indet)
& quant(c9506,one)
& gener(c9506,sp)
& fact(c9506,real)
& etype(c9506,int0)
& card(c9506,int1)
& sort(c9506,na)
& varia(c9505,con)
& refer(c9505,det)
& quant(c9505,one)
& gener(c9505,sp)
& fact(c9505,real)
& etype(c9505,int0)
& card(c9505,int1)
& sort(c9505,io)
& sort(c9505,d)
& sort(usa_0,fe)
& varia(c9501,varia_c)
& refer(c9501,indet)
& quant(c9501,one)
& gener(c9501,sp)
& fact(c9501,real)
& etype(c9501,int0)
& card(c9501,int1)
& sort(c9501,na)
& varia(c9500,con)
& refer(c9500,det)
& quant(c9500,one)
& gener(c9500,sp)
& fact(c9500,real)
& etype(c9500,int0)
& card(c9500,int1)
& sort(c9500,io)
& sort(c9500,d)
& varia(garantiemacht_1_2,varia_c)
& refer(garantiemacht_1_2,refer_c)
& quant(garantiemacht_1_2,one)
& gener(garantiemacht_1_2,ge)
& fact(garantiemacht_1_2,real)
& etype(garantiemacht_1_2,int0)
& card(garantiemacht_1_2,int1)
& sort(garantiemacht_1_2,io)
& sort(garantiemacht_1_2,d)
& varia(c9495,con)
& refer(c9495,det)
& quant(c9495,nfquant)
& gener(c9495,sp)
& fact(c9495,real)
& etype(c9495,int1)
& card(c9495,int3)
& sort(c9495,io)
& sort(c9495,d)
& sort(mugabe_0,fe)
& sort(robert_0,fe)
& varia(c9490,varia_c)
& refer(c9490,indet)
& quant(c9490,one)
& gener(c9490,sp)
& fact(c9490,real)
& etype(c9490,int0)
& card(c9490,int1)
& sort(c9490,na)
& varia(c9489,varia_c)
& refer(c9489,indet)
& quant(c9489,one)
& gener(c9489,sp)
& fact(c9489,real)
& etype(c9489,int0)
& card(c9489,int1)
& sort(c9489,na)
& varia(c9488,con)
& refer(c9488,det)
& quant(c9488,one)
& gener(c9488,sp)
& fact(c9488,real)
& etype(c9488,int0)
& card(c9488,int1)
& sort(c9488,d)
& sort(simbabwe_0,fe)
& 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(c9485,varia_c)
& refer(c9485,indet)
& quant(c9485,one)
& gener(c9485,sp)
& fact(c9485,real)
& etype(c9485,int0)
& card(c9485,int1)
& sort(c9485,na)
& varia(c9484,con)
& refer(c9484,det)
& quant(c9484,one)
& gener(c9484,sp)
& fact(c9484,real)
& etype(c9484,int0)
& card(c9484,int1)
& sort(c9484,io)
& sort(c9484,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(c9475,varia_c)
& refer(c9475,indet)
& quant(c9475,one)
& gener(c9475,sp)
& fact(c9475,real)
& etype(c9475,int0)
& card(c9475,int1)
& sort(c9475,na)
& varia(c9474,varia_c)
& refer(c9474,indet)
& quant(c9474,one)
& gener(c9474,sp)
& fact(c9474,real)
& etype(c9474,int0)
& card(c9474,int1)
& sort(c9474,na)
& varia(c9473,con)
& refer(c9473,det)
& quant(c9473,one)
& gener(c9473,sp)
& fact(c9473,real)
& etype(c9473,int0)
& card(c9473,int1)
& sort(c9473,d)
& varia(druck_1_1,varia_c)
& refer(druck_1_1,refer_c)
& quant(druck_1_1,one)
& gener(druck_1_1,ge)
& fact(druck_1_1,real)
& etype(druck_1_1,int0)
& card(druck_1_1,int1)
& sort(druck_1_1,oa)
& varia(c9464,varia_c)
& refer(c9464,det)
& quant(c9464,one)
& gener(c9464,sp)
& fact(c9464,real)
& etype(c9464,int0)
& card(c9464,int1)
& sort(c9464,oa)
& varia(meuterer_1_1,varia_c)
& refer(meuterer_1_1,refer_c)
& quant(meuterer_1_1,one)
& gener(meuterer_1_1,ge)
& fact(meuterer_1_1,real)
& etype(meuterer_1_1,int0)
& card(meuterer_1_1,int1)
& sort(meuterer_1_1,d)
& varia(c9458,varia_c)
& refer(c9458,indet)
& quant(c9458,mult)
& gener(c9458,gener_c)
& fact(c9458,real)
& etype(c9458,int1)
& card(c9458,cons(x_constant,cons(int1,nil)))
& sort(c9458,d)
& sort(unita_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(einrichtung_1_2,varia_c)
& refer(einrichtung_1_2,refer_c)
& quant(einrichtung_1_2,quant_c)
& gener(einrichtung_1_2,ge)
& fact(einrichtung_1_2,real)
& etype(einrichtung_1_2,int1)
& card(einrichtung_1_2,card_c)
& sort(einrichtung_1_2,io)
& sort(einrichtung_1_2,d)
& varia(c9457,varia_c)
& refer(c9457,indet)
& quant(c9457,one)
& gener(c9457,sp)
& fact(c9457,real)
& etype(c9457,int0)
& card(c9457,int1)
& sort(c9457,na)
& varia(c9456,con)
& refer(c9456,det)
& quant(c9456,one)
& gener(c9456,sp)
& fact(c9456,real)
& etype(c9456,int1)
& card(c9456,int1)
& sort(c9456,io)
& sort(c9456,d)
& varia(regierung_1_1,varia_c)
& refer(regierung_1_1,refer_c)
& quant(regierung_1_1,quant_c)
& gener(regierung_1_1,ge)
& fact(regierung_1_1,real)
& etype(regierung_1_1,int1)
& card(regierung_1_1,card_c)
& sort(regierung_1_1,io)
& sort(regierung_1_1,d)
& sort(angolanisch_1_1,nq)
& varia(c9448,con)
& refer(c9448,det)
& quant(c9448,one)
& gener(c9448,sp)
& fact(c9448,real)
& etype(c9448,int1)
& card(c9448,int1)
& sort(c9448,io)
& sort(c9448,d)
& varia(verfechter_1_1,varia_c)
& refer(verfechter_1_1,refer_c)
& quant(verfechter_1_1,one)
& gener(verfechter_1_1,ge)
& fact(verfechter_1_1,real)
& etype(verfechter_1_1,int0)
& card(verfechter_1_1,int1)
& sort(verfechter_1_1,io)
& sort(verfechter_1_1,d)
& varia(c9443,varia_c)
& refer(c9443,indet)
& quant(c9443,mult)
& gener(c9443,sp)
& fact(c9443,real)
& etype(c9443,int1)
& card(c9443,cons(x_constant,cons(int1,nil)))
& sort(c9443,io)
& sort(c9443,d)
& varia(abkommen_1_1,varia_c)
& refer(abkommen_1_1,refer_c)
& quant(abkommen_1_1,one)
& gener(abkommen_1_1,ge)
& fact(abkommen_1_1,real)
& etype(abkommen_1_1,int0)
& card(abkommen_1_1,int1)
& sort(abkommen_1_1,io)
& sort(abkommen_1_1,d)
& varia(c9434,con)
& refer(c9434,det)
& quant(c9434,one)
& gener(c9434,sp)
& fact(c9434,real)
& etype(c9434,int0)
& card(c9434,int1)
& sort(c9434,io)
& sort(c9434,d)
& sub(garantiemacht_1_2,macht_1_2)
& assoc(garantiemacht_1_2,b__374rgschaft_1_1)
& tupl_p12(c9590,c9434,c9443,c9456,c9458,c9464,c9488,c9484,c9495,c9500,c9505,c9518)
& val(c9519,russland_0)
& sub(c9519,name_1_1)
& sub(c9518,land_1_1)
& attr(c9518,c9519)
& val(c9506,portugal_0)
& sub(c9506,name_1_1)
& sub(c9505,land_1_1)
& attr(c9505,c9506)
& val(c9501,usa_0)
& sub(c9501,name_1_1)
& sub(c9500,land_1_1)
& attr(c9500,c9501)
& pred(c9495,garantiemacht_1_2)
& val(c9490,mugabe_0)
& sub(c9490,familiename_1_1)
& val(c9489,robert_0)
& sub(c9489,eigenname_1_1)
& sub(c9488,pr__344sident_1_1)
& attr(c9488,c9490)
& attr(c9488,c9489)
& val(c9485,simbabwe_0)
& sub(c9485,name_1_1)
& sub(c9484,land_1_1)
& attr(c9484,c9485)
& val(c9475,mandela_0)
& sub(c9475,familiename_1_1)
& val(c9474,nelson_0)
& sub(c9474,eigenname_1_1)
& sub(c9473,pr__344sident_1_1)
& prop(c9473,s__374dafrikanisch_1_1)
& attr(c9473,c9475)
& attr(c9473,c9474)
& attr(c9473,c9464)
& sub(c9464,druck_1_1)
& pred(c9458,meuterer_1_1)
& val(c9457,unita_0)
& sub(c9457,name_1_1)
& sub(c9456,einrichtung_1_2)
& attr(c9456,c9457)
& sub(c9448,regierung_1_1)
& prop(c9448,angolanisch_1_1)
& attch(c9448,c9443)
& pred(c9443,verfechter_1_1)
& sub(c9434,abkommen_1_1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10191,plain,
! [X0,X1] : member(X0,cons(X0,X1)),
inference(cnf_transformation,[status(thm)],[f1]) ).
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] :
( ~ state_adjective_state_binding(X2,X0)
| ~ prop(X1,X2)
| attr(sK48_skl(X0,X1),sK47_skl(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f10676]) ).
fof(f10681,plain,
! [X0,X1,X2] :
( sub(sK47_skl(X2,X0),name_1_1)
| ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10676]) ).
fof(f10682,plain,
! [X0,X1,X2] :
( val(sK47_skl(X1,X2),X1)
| ~ prop(X2,X0)
| ~ state_adjective_state_binding(X0,X1) ),
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] :
( ~ sub(X2,X1)
| ~ attr(X0,X2)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| arg1(sK50_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f10694]) ).
fof(f10696,plain,
! [X0,X1,X2] :
( ~ attr(X0,X1)
| ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X1,X2)
| arg2(sK50_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f10694]) ).
fof(f10697,plain,
! [X0,X1,X2] :
( subs(sK50_skl(X2),hei__337en_1_1)
| ~ attr(X2,X0)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10694]) ).
fof(f10698,plain,
! [X0,X1,X2] :
( ? [X3] :
( subs(X3,stehen_1_b)
& scar(X3,X2)
& obj(X3,X2)
& mcont(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)],[f160]) ).
fof(f10699,plain,
! [X2] :
( ? [X3] :
( subs(X3,stehen_1_b)
& scar(X3,X2)
& obj(X3,X2)
& mcont(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)],[f10698]) ).
fof(f10700,plain,
! [X2] :
( ( subs(sK51_skl(X2),stehen_1_b)
& scar(sK51_skl(X2),X2)
& obj(sK51_skl(X2),X2)
& mcont(sK51_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,[sK51_skl]),skolemize(X3,sK51_skl(X2))],[f10699]) ).
fof(f10702,plain,
! [X0,X1,X2] :
( ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X2,X0)
| obj(sK51_skl(X2),X2)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10700]) ).
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(X2,X1)
| ~ arg2(X2,X0)
| ~ subs(X2,hei__337en_1_1)
| arg1(sK53_skl(X0,X1,X2),X1) ),
inference(cnf_transformation,[status(thm)],[f10707]) ).
fof(f10709,plain,
! [X0,X1,X2] :
( ~ arg1(X2,X1)
| ~ arg2(X2,X0)
| ~ subs(X2,hei__337en_1_1)
| arg2(sK53_skl(X0,X1,X2),X0) ),
inference(cnf_transformation,[status(thm)],[f10707]) ).
fof(f10713,plain,
! [X0,X1,X2] :
( ~ subs(X0,hei__337en_1_1)
| subr(sK53_skl(X2,X1,X0),rprs_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
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(f20830,plain,
attr(c9473,c9474),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20831,plain,
attr(c9473,c9475),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20832,plain,
prop(c9473,s__374dafrikanisch_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20833,plain,
sub(c9473,pr__344sident_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20834,plain,
sub(c9474,eigenname_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20835,plain,
val(c9474,nelson_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20836,plain,
sub(c9475,familiename_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20837,plain,
val(c9475,mandela_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f21223,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(f21224,plain,
! [X0,X1,X2] :
( ~ sQ0_spl
| ~ in(X2,X1)
| ~ sub(X0,name_1_1)
| ~ attr(X1,X0)
| ~ val(X0,s__374dafrika_0) ),
inference(component_clause,[status(thm)],[f21223]) ).
fof(f21226,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(f21227,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ1_spl
| ~ val(X1,mandela_0)
| ~ attr(X3,X1)
| ~ sub(X0,eigenname_1_1)
| ~ sub(X5,X6)
| ~ subr(X2,rprs_0)
| ~ attr(X3,X0)
| ~ arg2(X2,X5)
| ~ obj(X4,X3)
| ~ arg1(X2,X3)
| ~ sub(X1,familiename_1_1)
| ~ val(X0,nelson_0) ),
inference(component_clause,[status(thm)],[f21226]) ).
fof(f21229,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f20817,f21223,f21226]) ).
fof(f23044,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ state_adjective_state_binding(X1,s__374dafrika_0)
| ~ in(X3,X2)
| ~ attr(X2,sK47_skl(s__374dafrika_0,X0))
| ~ sub(sK47_skl(s__374dafrika_0,X0),name_1_1)
| ~ prop(X0,X1) ),
inference(resolution,[status(thm)],[f10682,f21224]) ).
fof(f24320,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ state_adjective_state_binding(X3,s__374dafrika_0)
| ~ prop(X1,X3)
| ~ in(X2,X0)
| ~ attr(X0,sK47_skl(s__374dafrika_0,X1)) ),
inference(backward_subsumption_resolution,[status(thm)],[f23044,f10681]) ).
fof(f25300,plain,
! [X0] :
( attr(sK48_skl(s__374dafrika_0,X0),sK47_skl(s__374dafrika_0,X0))
| ~ prop(X0,s__374dafrikanisch_1_1) ),
inference(resolution,[status(thm)],[f10678,f19788]) ).
fof(f25301,plain,
! [X0,X1,X2] :
( ~ sQ0_spl
| ~ prop(X2,s__374dafrikanisch_1_1)
| ~ prop(X2,X0)
| ~ in(X1,sK48_skl(s__374dafrika_0,X2))
| ~ state_adjective_state_binding(X0,s__374dafrika_0) ),
inference(resolution,[status(thm)],[f25300,f24320]) ).
fof(f25303,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ prop(X1,s__374dafrikanisch_1_1)
| ~ prop(X1,s__374dafrikanisch_1_1)
| ~ in(X0,sK48_skl(s__374dafrika_0,X1)) ),
inference(resolution,[status(thm)],[f25301,f19788]) ).
fof(f25304,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)],[f25303]) ).
fof(f25305,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ state_adjective_state_binding(X1,s__374dafrika_0)
| ~ prop(X0,X1)
| ~ prop(X0,s__374dafrikanisch_1_1) ),
inference(resolution,[status(thm)],[f25304,f10677]) ).
fof(f25308,plain,
! [X0] :
( ~ sQ0_spl
| ~ prop(X0,s__374dafrikanisch_1_1)
| ~ prop(X0,s__374dafrikanisch_1_1) ),
inference(resolution,[status(thm)],[f25305,f19788]) ).
fof(f25309,plain,
! [X0] :
( ~ sQ0_spl
| ~ prop(X0,s__374dafrikanisch_1_1) ),
inference(duplicate_literals_removal,[status(thm)],[f25308]) ).
fof(f25310,plain,
( ~ sQ0_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f20832,f25309]) ).
fof(f25316,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f25310]) ).
fof(f25317,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ sQ1_spl
| ~ sub(X3,eigenname_1_1)
| ~ sub(X6,X8)
| ~ val(X2,mandela_0)
| ~ sub(X2,familiename_1_1)
| ~ arg1(X0,X5)
| ~ obj(X7,X1)
| ~ arg2(sK53_skl(X4,X5,X0),X6)
| ~ arg2(X0,X4)
| ~ val(X3,nelson_0)
| ~ arg1(sK53_skl(X4,X5,X0),X1)
| ~ attr(X1,X3)
| ~ attr(X1,X2)
| ~ subs(X0,hei__337en_1_1) ),
inference(resolution,[status(thm)],[f21227,f10713]) ).
fof(f25320,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ sQ1_spl
| ~ arg1(X0,X1)
| ~ arg2(X0,X4)
| ~ subs(X0,hei__337en_1_1)
| ~ sub(X3,eigenname_1_1)
| ~ sub(X5,X7)
| ~ val(X2,mandela_0)
| ~ sub(X2,familiename_1_1)
| ~ arg1(X0,X1)
| ~ obj(X6,X1)
| ~ arg2(sK53_skl(X4,X1,X0),X5)
| ~ arg2(X0,X4)
| ~ val(X3,nelson_0)
| ~ attr(X1,X3)
| ~ attr(X1,X2)
| ~ subs(X0,hei__337en_1_1) ),
inference(resolution,[status(thm)],[f25317,f10708]) ).
fof(f25321,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ sQ1_spl
| ~ arg2(sK53_skl(X7,X2,X6),X4)
| ~ arg2(X6,X7)
| ~ sub(X3,eigenname_1_1)
| ~ arg1(X6,X2)
| ~ subs(X6,hei__337en_1_1)
| ~ sub(X4,X5)
| ~ attr(X2,X0)
| ~ sub(X0,familiename_1_1)
| ~ attr(X2,X3)
| ~ val(X3,nelson_0)
| ~ obj(X1,X2)
| ~ val(X0,mandela_0) ),
inference(duplicate_literals_removal,[status(thm)],[f25320]) ).
fof(f25322,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ1_spl
| ~ arg1(X6,X2)
| ~ arg2(X6,X4)
| ~ subs(X6,hei__337en_1_1)
| ~ arg2(X6,X4)
| ~ sub(X3,eigenname_1_1)
| ~ arg1(X6,X2)
| ~ subs(X6,hei__337en_1_1)
| ~ sub(X4,X5)
| ~ attr(X2,X0)
| ~ sub(X0,familiename_1_1)
| ~ attr(X2,X3)
| ~ val(X3,nelson_0)
| ~ obj(X1,X2)
| ~ val(X0,mandela_0) ),
inference(resolution,[status(thm)],[f25321,f10709]) ).
fof(f25323,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ1_spl
| ~ sub(X6,eigenname_1_1)
| ~ subs(X2,hei__337en_1_1)
| ~ attr(X3,X6)
| ~ val(X6,nelson_0)
| ~ obj(X5,X3)
| ~ sub(X4,familiename_1_1)
| ~ val(X4,mandela_0)
| ~ arg2(X2,X0)
| ~ attr(X3,X4)
| ~ arg1(X2,X3)
| ~ sub(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f25322]) ).
fof(f25326,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ1_spl
| ~ sub(c9474,eigenname_1_1)
| ~ subs(X2,hei__337en_1_1)
| ~ attr(X3,c9474)
| ~ obj(X5,X3)
| ~ sub(X4,familiename_1_1)
| ~ val(X4,mandela_0)
| ~ arg2(X2,X0)
| ~ attr(X3,X4)
| ~ arg1(X2,X3)
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[f25323,f20835]) ).
fof(f25327,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ89_spl
<=> ( ~ subs(X2,hei__337en_1_1)
| ~ attr(X3,c9474)
| ~ obj(X5,X3)
| ~ sub(X4,familiename_1_1)
| ~ val(X4,mandela_0)
| ~ arg2(X2,X0)
| ~ attr(X3,X4)
| ~ arg1(X2,X3)
| ~ sub(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f25328,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ89_spl
| ~ arg1(X5,X2)
| ~ attr(X2,c9474)
| ~ sub(X3,familiename_1_1)
| ~ subs(X5,hei__337en_1_1)
| ~ arg2(X5,X0)
| ~ val(X3,mandela_0)
| ~ obj(X4,X2)
| ~ attr(X2,X3)
| ~ sub(X0,X1) ),
inference(component_clause,[status(thm)],[f25327]) ).
fof(f25330,definition,
( sQ90_spl
<=> sub(c9474,eigenname_1_1) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f25332,plain,
( sQ90_spl
| ~ sub(c9474,eigenname_1_1) ),
inference(component_clause,[status(thm)],[f25330]) ).
fof(f25333,plain,
( ~ sQ1_spl
| ~ sQ90_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f25326,f25327,f25330,f21226]) ).
fof(f25334,plain,
( sQ90_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25332,f20834]) ).
fof(f25335,plain,
sQ90_spl,
inference(contradiction_clause,[status(thm)],[f25334]) ).
fof(f25338,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ89_spl
| ~ arg1(X4,c9473)
| ~ sub(X2,familiename_1_1)
| ~ subs(X4,hei__337en_1_1)
| ~ arg2(X4,X0)
| ~ val(X2,mandela_0)
| ~ obj(X3,c9473)
| ~ attr(c9473,X2)
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[f25328,f20830]) ).
fof(f25339,definition,
! [X0,X1,X4] :
( sQ91_spl
<=> ( ~ arg1(X4,c9473)
| ~ subs(X4,hei__337en_1_1)
| ~ arg2(X4,X0)
| ~ sub(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f25340,plain,
! [X0,X1,X2] :
( ~ sQ91_spl
| ~ sub(X1,X2)
| ~ arg1(X0,c9473)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X1) ),
inference(component_clause,[status(thm)],[f25339]) ).
fof(f25342,definition,
! [X2] :
( sQ92_spl
<=> ( ~ sub(X2,familiename_1_1)
| ~ val(X2,mandela_0)
| ~ attr(c9473,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f25343,plain,
! [X0] :
( ~ sQ92_spl
| ~ attr(c9473,X0)
| ~ sub(X0,familiename_1_1)
| ~ val(X0,mandela_0) ),
inference(component_clause,[status(thm)],[f25342]) ).
fof(f25345,definition,
! [X3] :
( sQ93_spl
<=> ~ obj(X3,c9473) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f25346,plain,
! [X0] :
( ~ sQ93_spl
| ~ obj(X0,c9473) ),
inference(component_clause,[status(thm)],[f25345]) ).
fof(f25348,plain,
( ~ sQ89_spl
| sQ93_spl
| sQ92_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f25338,f25339,f25342,f25345,f25327]) ).
fof(f25672,plain,
! [X0,X1] :
( ~ sQ93_spl
| ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c9473,X0) ),
inference(resolution,[status(thm)],[f25346,f10702]) ).
fof(f25724,plain,
( ~ sQ92_spl
| ~ attr(c9473,c9475)
| ~ sub(c9475,familiename_1_1) ),
inference(resolution,[status(thm)],[f25343,f20837]) ).
fof(f25725,definition,
( sQ102_spl
<=> sub(c9475,familiename_1_1) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f25727,plain,
( sQ102_spl
| ~ sub(c9475,familiename_1_1) ),
inference(component_clause,[status(thm)],[f25725]) ).
fof(f25728,definition,
( sQ103_spl
<=> attr(c9473,c9475) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f25730,plain,
( sQ103_spl
| ~ attr(c9473,c9475) ),
inference(component_clause,[status(thm)],[f25728]) ).
fof(f25731,plain,
( ~ sQ92_spl
| ~ sQ103_spl
| ~ sQ102_spl ),
inference(split_clause,[status(thm)],[f25724,f25725,f25728,f25342]) ).
fof(f25732,plain,
( sQ102_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25727,f20836]) ).
fof(f25733,plain,
sQ102_spl,
inference(contradiction_clause,[status(thm)],[f25732]) ).
fof(f25734,plain,
( sQ103_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25730,f20831]) ).
fof(f25735,plain,
sQ103_spl,
inference(contradiction_clause,[status(thm)],[f25734]) ).
fof(f26066,plain,
! [X0] :
( ~ sQ93_spl
| ~ sub(X0,eigenname_1_1)
| ~ attr(c9473,X0) ),
inference(resolution,[status(thm)],[f25672,f10191]) ).
fof(f26068,plain,
( ~ sQ93_spl
| ~ sub(c9474,eigenname_1_1) ),
inference(resolution,[status(thm)],[f26066,f20830]) ).
fof(f26071,plain,
( ~ sQ93_spl
| ~ sQ90_spl ),
inference(split_clause,[status(thm)],[f26068,f25330,f25345]) ).
fof(f26094,definition,
! [X2] :
( sQ107_spl
<=> ~ sub(c9473,X2) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f26095,plain,
! [X0] :
( ~ sQ107_spl
| ~ sub(c9473,X0) ),
inference(component_clause,[status(thm)],[f26094]) ).
fof(f26108,plain,
( ~ sQ107_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f20833,f26095]) ).
fof(f26123,plain,
~ sQ107_spl,
inference(contradiction_clause,[status(thm)],[f26108]) ).
fof(f26137,plain,
! [X0,X1,X2,X3] :
( ~ sQ91_spl
| ~ sub(X3,X2)
| ~ attr(c9473,X3)
| ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1)
| ~ subs(sK50_skl(c9473),hei__337en_1_1)
| ~ arg2(sK50_skl(c9473),X0) ),
inference(resolution,[status(thm)],[f25340,f10695]) ).
fof(f26140,definition,
! [X0,X1] :
( sQ113_spl
<=> ( ~ sub(X0,X1)
| ~ arg2(sK50_skl(c9473),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f26141,plain,
! [X0,X1] :
( ~ sQ113_spl
| ~ sub(X0,X1)
| ~ arg2(sK50_skl(c9473),X0) ),
inference(component_clause,[status(thm)],[f26140]) ).
fof(f26143,definition,
( sQ114_spl
<=> subs(sK50_skl(c9473),hei__337en_1_1) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f26145,plain,
( sQ114_spl
| ~ subs(sK50_skl(c9473),hei__337en_1_1) ),
inference(component_clause,[status(thm)],[f26143]) ).
fof(f26146,definition,
! [X2,X3] :
( sQ115_spl
<=> ( ~ sub(X3,X2)
| ~ attr(c9473,X3)
| ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))) ) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f26147,plain,
! [X0,X1] :
( ~ sQ115_spl
| ~ sub(X1,X0)
| ~ attr(c9473,X1)
| ~ member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))) ),
inference(component_clause,[status(thm)],[f26146]) ).
fof(f26149,plain,
( ~ sQ91_spl
| sQ115_spl
| ~ sQ114_spl
| sQ113_spl ),
inference(split_clause,[status(thm)],[f26137,f26140,f26143,f26146,f25339]) ).
fof(f26175,plain,
! [X0] :
( ~ sQ115_spl
| ~ sub(X0,eigenname_1_1)
| ~ attr(c9473,X0) ),
inference(resolution,[status(thm)],[f26147,f10191]) ).
fof(f26177,plain,
( ~ sQ115_spl
| ~ sub(c9474,eigenname_1_1) ),
inference(resolution,[status(thm)],[f26175,f20830]) ).
fof(f26180,plain,
( ~ sQ115_spl
| ~ sQ90_spl ),
inference(split_clause,[status(thm)],[f26177,f25330,f26146]) ).
fof(f26301,plain,
! [X0,X1] :
( sQ114_spl
| ~ attr(c9473,X0)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[f26145,f10697]) ).
fof(f26304,plain,
( sQ114_spl
| sQ115_spl ),
inference(split_clause,[status(thm)],[f26301,f26146,f26143]) ).
fof(f26415,plain,
! [X0,X1,X2] :
( ~ sQ113_spl
| ~ attr(c9473,X1)
| ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X1,X2)
| ~ sub(c9473,X0) ),
inference(resolution,[status(thm)],[f26141,f10696]) ).
fof(f26416,plain,
( ~ sQ113_spl
| sQ115_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f26415,f26094,f26146,f26140]) ).
fof(f26417,plain,
$false,
inference(sat_refutation,[status(thm)],[f21229,f25316,f25333,f25335,f25348,f25731,f25733,f25735,f26071,f26123,f26149,f26180,f26304,f26416]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR116+29 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n008.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 15:10:11 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.12/0.42 % Drodi V4.1.1
% 70.28/9.38 % Refutation found
% 70.28/9.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 70.28/9.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 68.72/9.49 % Elapsed time: 9.113918 seconds
% 68.72/9.49 % CPU time: 71.185351 seconds
% 68.72/9.49 % Total memory used: 616.940 MB
% 68.72/9.49 % Net memory used: 588.940 MB
%------------------------------------------------------------------------------