%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR116+13 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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:09 PM UTC 2026
% Result : Theorem 69.64s 9.33s
% Output : CNFRefutation 69.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 19
% Syntax : Number of formulae : 98 ( 19 unt; 13 def)
% Number of atoms : 684 ( 0 equ)
% Maximal formula atoms : 222 ( 6 avg)
% Number of connectives : 890 ( 304 ~; 273 |; 297 &)
% ( 13 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 222 ( 10 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 38 ( 37 usr; 14 prp; 0-7 aty)
% Number of functors : 64 ( 64 usr; 59 con; 0-3 aty)
% Number of variables : 232 ( 202 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : member(X0,cons(X0,X1)),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f10188,conjecture,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( val(X6,s__374dafrika_0)
& val(X2,nelson_0)
& val(X1,mandela_0)
& subr(X3,rprs_0)
& sub(X6,name_1_1)
& sub(X4,X8)
& sub(X2,eigenname_1_1)
& sub(X1,familiename_1_1)
& obj(X7,X0)
& attr(X5,X6)
& attr(X0,X2)
& attr(X0,X1)
& arg2(X3,X4)
& arg1(X3,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10189,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( val(X6,s__374dafrika_0)
& val(X2,nelson_0)
& val(X1,mandela_0)
& subr(X3,rprs_0)
& sub(X6,name_1_1)
& sub(X4,X8)
& sub(X2,eigenname_1_1)
& sub(X1,familiename_1_1)
& obj(X7,X0)
& attr(X5,X6)
& attr(X0,X2)
& attr(X0,X1)
& arg2(X3,X4)
& arg1(X3,X0) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,hypothesis,
( varia(c636,varia_c)
& refer(c636,refer_c)
& quant(c636,quant_c)
& gener(c636,gener_c)
& fact(c636,real)
& etype(c636,etype_c)
& card(c636,card_c)
& sort(c636,ent)
& sort(ghana_0,fe)
& varia(c383,varia_c)
& refer(c383,indet)
& quant(c383,one)
& gener(c383,sp)
& fact(c383,real)
& etype(c383,int0)
& card(c383,int1)
& sort(c383,na)
& varia(c382,con)
& refer(c382,det)
& quant(c382,one)
& gener(c382,sp)
& fact(c382,real)
& etype(c382,int0)
& card(c382,int1)
& sort(c382,io)
& sort(c382,d)
& sort(rawling_0,fe)
& sort(jerry_0,fe)
& varia(c377,varia_c)
& refer(c377,indet)
& quant(c377,one)
& gener(c377,sp)
& fact(c377,real)
& etype(c377,int0)
& card(c377,int1)
& sort(c377,na)
& varia(c376,varia_c)
& refer(c376,indet)
& quant(c376,one)
& gener(c376,sp)
& fact(c376,real)
& etype(c376,int0)
& card(c376,int1)
& sort(c376,na)
& varia(c375,con)
& refer(c375,det)
& quant(c375,one)
& gener(c375,sp)
& fact(c375,real)
& etype(c375,int0)
& card(c375,int1)
& sort(c375,d)
& sort(s__374dafrika_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(c368,varia_c)
& refer(c368,indet)
& quant(c368,one)
& gener(c368,sp)
& fact(c368,real)
& etype(c368,int0)
& card(c368,int1)
& sort(c368,na)
& varia(c367,con)
& refer(c367,det)
& quant(c367,one)
& gener(c367,sp)
& fact(c367,real)
& etype(c367,int0)
& card(c367,int1)
& sort(c367,io)
& sort(c367,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(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(c362,varia_c)
& refer(c362,indet)
& quant(c362,one)
& gener(c362,sp)
& fact(c362,real)
& etype(c362,int0)
& card(c362,int1)
& sort(c362,na)
& varia(c361,varia_c)
& refer(c361,indet)
& quant(c361,one)
& gener(c361,sp)
& fact(c361,real)
& etype(c361,int0)
& card(c361,int1)
& sort(c361,na)
& varia(c360,con)
& refer(c360,det)
& quant(c360,one)
& gener(c360,sp)
& fact(c360,real)
& etype(c360,int0)
& card(c360,int1)
& sort(c360,d)
& 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)
& varia(c355,con)
& refer(c355,det)
& quant(c355,mult)
& gener(c355,sp)
& fact(c355,real)
& etype(c355,int1)
& card(c355,cons(x_constant,cons(int1,nil)))
& sort(c355,d)
& varia(c345,varia_c)
& refer(c345,refer_c)
& quant(c345,mult)
& gener(c345,gener_c)
& fact(c345,real)
& etype(c345,int1)
& card(c345,cons(x_constant,cons(int1,nil)))
& sort(c345,d)
& sort(ehemalig_1_1,tq)
& varia(c1,varia_c)
& refer(c1,refer_c)
& quant(c1,quant_c)
& gener(c1,gener_c)
& fact(c1,fact_c)
& etype(c1,etype_c)
& card(c1,card_c)
& sort(c1,ent)
& varia(traegerin_1_1,varia_c)
& refer(traegerin_1_1,refer_c)
& quant(traegerin_1_1,one)
& gener(traegerin_1_1,ge)
& fact(traegerin_1_1,real)
& etype(traegerin_1_1,int0)
& card(traegerin_1_1,int1)
& sort(traegerin_1_1,d)
& varia(auszeichnung_1_1,varia_c)
& refer(auszeichnung_1_1,refer_c)
& quant(auszeichnung_1_1,one)
& gener(auszeichnung_1_1,ge)
& fact(auszeichnung_1_1,real)
& etype(auszeichnung_1_1,int0)
& card(auszeichnung_1_1,int1)
& sort(auszeichnung_1_1,d)
& varia(auszeichnungstr__344ger_1_1,varia_c)
& refer(auszeichnungstr__344ger_1_1,refer_c)
& quant(auszeichnungstr__344ger_1_1,one)
& gener(auszeichnungstr__344ger_1_1,ge)
& fact(auszeichnungstr__344ger_1_1,real)
& etype(auszeichnungstr__344ger_1_1,int0)
& card(auszeichnungstr__344ger_1_1,int1)
& sort(auszeichnungstr__344ger_1_1,d)
& tupl_p7(c636,c345,c355,c360,c367,c375,c382)
& val(c383,ghana_0)
& sub(c383,name_1_1)
& sub(c382,land_1_1)
& attr(c382,c383)
& val(c377,rawling_0)
& sub(c377,familiename_1_1)
& val(c376,jerry_0)
& sub(c376,eigenname_1_1)
& sub(c375,mensch_1_1)
& attr(c375,c377)
& attr(c375,c376)
& val(c368,s__374dafrika_0)
& sub(c368,name_1_1)
& sub(c367,land_1_1)
& attr(c367,c368)
& val(c362,mandela_0)
& sub(c362,familiename_1_1)
& val(c361,nelson_0)
& sub(c361,eigenname_1_1)
& sub(c360,mensch_1_1)
& attr(c360,c362)
& attr(c360,c361)
& pred(c355,pr__344sident_1_1)
& pred(c345,c1)
& pmod(c1,ehemalig_1_1,auszeichnungstr__344ger_1_1)
& sub(auszeichnungstr__344ger_1_1,traegerin_1_1)
& assoc(auszeichnungstr__344ger_1_1,auszeichnung_1_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10191,plain,
! [X0,X1] : member(X0,cons(X0,X1)),
inference(cnf_transformation,[status(thm)],[f1]) ).
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] :
( arg1(sK50_skl(X0),X0)
| ~ sub(X1,X2)
| ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10694]) ).
fof(f10696,plain,
! [X0,X1,X2] :
( arg2(sK50_skl(X0),X0)
| ~ sub(X1,X2)
| ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10694]) ).
fof(f10697,plain,
! [X0,X1,X2] :
( subs(sK50_skl(X0),hei__337en_1_1)
| ~ sub(X1,X2)
| ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(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] :
( obj(sK51_skl(X0),X0)
| ~ sub(X1,X2)
| ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(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(sK53_skl(X2,X1,X0),X1)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10707]) ).
fof(f10709,plain,
! [X0,X1,X2] :
( arg2(sK53_skl(X2,X1,X0),X2)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10707]) ).
fof(f10713,plain,
! [X0,X1,X2] :
( subr(sK53_skl(X2,X1,X0),rprs_0)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10707]) ).
fof(f20815,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ val(X6,s__374dafrika_0)
| ~ val(X2,nelson_0)
| ~ val(X1,mandela_0)
| ~ subr(X3,rprs_0)
| ~ sub(X6,name_1_1)
| ~ sub(X4,X8)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ obj(X7,X0)
| ~ attr(X5,X6)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4)
| ~ arg1(X3,X0) ),
inference(pre_NNF_transformation,[status(thm)],[f10189]) ).
fof(f20816,plain,
! [X6] :
( ~ val(X6,s__374dafrika_0)
| ! [X2] :
( ~ val(X2,nelson_0)
| ! [X1] :
( ~ val(X1,mandela_0)
| ! [X3] :
( ~ subr(X3,rprs_0)
| ~ sub(X6,name_1_1)
| ! [X4] :
( ! [X8] : ~ sub(X4,X8)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ! [X0] :
( ! [X7] : ~ obj(X7,X0)
| ! [X5] : ~ attr(X5,X6)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4)
| ~ arg1(X3,X0) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f20815]) ).
fof(f20817,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ val(X6,s__374dafrika_0)
| ~ val(X4,nelson_0)
| ~ val(X3,mandela_0)
| ~ subr(X0,rprs_0)
| ~ sub(X6,name_1_1)
| ~ sub(X2,X8)
| ~ sub(X4,eigenname_1_1)
| ~ sub(X3,familiename_1_1)
| ~ obj(X7,X1)
| ~ attr(X5,X6)
| ~ attr(X1,X4)
| ~ attr(X1,X3)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f20816]) ).
fof(f20823,plain,
attr(c360,c361),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20824,plain,
attr(c360,c362),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20825,plain,
sub(c360,mensch_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20826,plain,
sub(c361,eigenname_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20827,plain,
val(c361,nelson_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20828,plain,
sub(c362,familiename_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20829,plain,
val(c362,mandela_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20830,plain,
attr(c367,c368),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20832,plain,
sub(c368,name_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20833,plain,
val(c368,s__374dafrika_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f21075,definition,
! [X0,X1,X2,X3,X4,X7,X8] :
( sQ0_spl
<=> ( ~ val(X4,nelson_0)
| ~ val(X3,mandela_0)
| ~ subr(X0,rprs_0)
| ~ sub(X2,X8)
| ~ sub(X4,eigenname_1_1)
| ~ sub(X3,familiename_1_1)
| ~ obj(X7,X1)
| ~ attr(X1,X4)
| ~ attr(X1,X3)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f21076,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ0_spl
| ~ val(X4,nelson_0)
| ~ val(X3,mandela_0)
| ~ subr(X0,rprs_0)
| ~ sub(X2,X6)
| ~ sub(X4,eigenname_1_1)
| ~ sub(X3,familiename_1_1)
| ~ obj(X5,X1)
| ~ attr(X1,X4)
| ~ attr(X1,X3)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(component_clause,[status(thm)],[f21075]) ).
fof(f21078,definition,
! [X5,X6] :
( sQ1_spl
<=> ( ~ val(X6,s__374dafrika_0)
| ~ sub(X6,name_1_1)
| ~ attr(X5,X6) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f21079,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ val(X1,s__374dafrika_0)
| ~ sub(X1,name_1_1)
| ~ attr(X0,X1) ),
inference(component_clause,[status(thm)],[f21078]) ).
fof(f21081,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f20817,f21075,f21078]) ).
fof(f21082,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ0_spl
| ~ val(c361,nelson_0)
| ~ val(X3,mandela_0)
| ~ subr(X0,rprs_0)
| ~ sub(X2,X5)
| ~ sub(X3,familiename_1_1)
| ~ obj(X4,X1)
| ~ attr(X1,c361)
| ~ attr(X1,X3)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(resolution,[status(thm)],[f20826,f21076]) ).
fof(f21084,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ2_spl
<=> ( ~ val(X3,mandela_0)
| ~ subr(X0,rprs_0)
| ~ sub(X2,X5)
| ~ sub(X3,familiename_1_1)
| ~ obj(X4,X1)
| ~ attr(X1,c361)
| ~ attr(X1,X3)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f21085,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ2_spl
| ~ val(X3,mandela_0)
| ~ subr(X0,rprs_0)
| ~ sub(X2,X5)
| ~ sub(X3,familiename_1_1)
| ~ obj(X4,X1)
| ~ attr(X1,c361)
| ~ attr(X1,X3)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(component_clause,[status(thm)],[f21084]) ).
fof(f21087,definition,
( sQ3_spl
<=> val(c361,nelson_0) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f21089,plain,
( sQ3_spl
| ~ val(c361,nelson_0) ),
inference(component_clause,[status(thm)],[f21087]) ).
fof(f21090,plain,
( ~ sQ0_spl
| ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f21082,f21084,f21087,f21075]) ).
fof(f21091,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21089,f20827]) ).
fof(f21092,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f21091]) ).
fof(f21097,plain,
! [X0] :
( ~ sQ1_spl
| ~ val(c368,s__374dafrika_0)
| ~ attr(X0,c368) ),
inference(resolution,[status(thm)],[f20832,f21079]) ).
fof(f21099,definition,
! [X0] :
( sQ4_spl
<=> ~ attr(X0,c368) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f21100,plain,
! [X0] :
( ~ sQ4_spl
| ~ attr(X0,c368) ),
inference(component_clause,[status(thm)],[f21099]) ).
fof(f21102,definition,
( sQ5_spl
<=> val(c368,s__374dafrika_0) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f21104,plain,
( sQ5_spl
| ~ val(c368,s__374dafrika_0) ),
inference(component_clause,[status(thm)],[f21102]) ).
fof(f21105,plain,
( ~ sQ1_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f21097,f21099,f21102,f21078]) ).
fof(f21106,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21104,f20833]) ).
fof(f21107,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f21106]) ).
fof(f21108,plain,
( ~ sQ4_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f20830,f21100]) ).
fof(f21109,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f21108]) ).
fof(f21121,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ2_spl
| ~ val(X5,mandela_0)
| ~ subr(X3,rprs_0)
| ~ sub(X4,X6)
| ~ sub(X5,familiename_1_1)
| ~ attr(X0,c361)
| ~ attr(X0,X5)
| ~ arg2(X3,X4)
| ~ arg1(X3,X0)
| ~ sub(X1,X2)
| ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[f10702,f21085]) ).
fof(f21122,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ2_spl
| ~ val(c362,mandela_0)
| ~ subr(X3,rprs_0)
| ~ sub(X4,X5)
| ~ attr(X0,c361)
| ~ attr(X0,c362)
| ~ arg2(X3,X4)
| ~ arg1(X3,X0)
| ~ sub(X1,X2)
| ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[f21121,f20828]) ).
fof(f21123,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ6_spl
<=> ( ~ subr(X3,rprs_0)
| ~ sub(X4,X5)
| ~ attr(X0,c361)
| ~ attr(X0,c362)
| ~ arg2(X3,X4)
| ~ arg1(X3,X0)
| ~ sub(X1,X2)
| ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f21124,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ6_spl
| ~ subr(X3,rprs_0)
| ~ sub(X4,X5)
| ~ attr(X0,c361)
| ~ attr(X0,c362)
| ~ arg2(X3,X4)
| ~ arg1(X3,X0)
| ~ sub(X1,X2)
| ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X0,X1) ),
inference(component_clause,[status(thm)],[f21123]) ).
fof(f21126,definition,
( sQ7_spl
<=> val(c362,mandela_0) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f21128,plain,
( sQ7_spl
| ~ val(c362,mandela_0) ),
inference(component_clause,[status(thm)],[f21126]) ).
fof(f21129,plain,
( ~ sQ2_spl
| ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f21122,f21123,f21126,f21084]) ).
fof(f21135,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ6_spl
| ~ subr(X2,rprs_0)
| ~ sub(X3,X4)
| ~ attr(c360,c361)
| ~ arg2(X2,X3)
| ~ arg1(X2,c360)
| ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c360,X0) ),
inference(resolution,[status(thm)],[f21124,f20824]) ).
fof(f21136,definition,
! [X0,X1] :
( sQ9_spl
<=> ( ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c360,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f21137,plain,
! [X0,X1] :
( ~ sQ9_spl
| ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c360,X0) ),
inference(component_clause,[status(thm)],[f21136]) ).
fof(f21139,definition,
! [X2,X3,X4] :
( sQ10_spl
<=> ( ~ subr(X2,rprs_0)
| ~ sub(X3,X4)
| ~ arg2(X2,X3)
| ~ arg1(X2,c360) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f21140,plain,
! [X0,X1,X2] :
( ~ sQ10_spl
| ~ subr(X0,rprs_0)
| ~ sub(X1,X2)
| ~ arg2(X0,X1)
| ~ arg1(X0,c360) ),
inference(component_clause,[status(thm)],[f21139]) ).
fof(f21142,definition,
( sQ11_spl
<=> attr(c360,c361) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f21144,plain,
( sQ11_spl
| ~ attr(c360,c361) ),
inference(component_clause,[status(thm)],[f21142]) ).
fof(f21145,plain,
( ~ sQ6_spl
| ~ sQ11_spl
| sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f21135,f21136,f21139,f21142,f21123]) ).
fof(f21146,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21128,f20829]) ).
fof(f21147,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f21146]) ).
fof(f21148,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21144,f20823]) ).
fof(f21149,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f21148]) ).
fof(f21151,plain,
! [X0] :
( ~ sQ9_spl
| ~ sub(X0,eigenname_1_1)
| ~ attr(c360,X0) ),
inference(resolution,[status(thm)],[f21137,f10191]) ).
fof(f21152,plain,
( ~ sQ9_spl
| ~ attr(c360,c361) ),
inference(resolution,[status(thm)],[f21151,f20826]) ).
fof(f21153,plain,
( ~ sQ9_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f21152,f21142,f21136]) ).
fof(f21158,definition,
! [X0,X1] :
( sQ12_spl
<=> ( ~ sub(X0,X1)
| ~ arg2(sK50_skl(c360),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f21159,plain,
! [X0,X1] :
( ~ sQ12_spl
| ~ sub(X0,X1)
| ~ arg2(sK50_skl(c360),X0) ),
inference(component_clause,[status(thm)],[f21158]) ).
fof(f21165,plain,
! [X0,X1,X2] :
( ~ sQ12_spl
| ~ sub(X1,X2)
| ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c360,X1)
| ~ sub(c360,X0) ),
inference(resolution,[status(thm)],[f21159,f10696]) ).
fof(f21166,definition,
! [X0] :
( sQ14_spl
<=> ~ sub(c360,X0) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f21167,plain,
! [X0] :
( ~ sQ14_spl
| ~ sub(c360,X0) ),
inference(component_clause,[status(thm)],[f21166]) ).
fof(f21169,plain,
( ~ sQ12_spl
| sQ9_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f21165,f21166,f21136,f21158]) ).
fof(f21170,plain,
( ~ sQ14_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f20825,f21167]) ).
fof(f21171,plain,
~ sQ14_spl,
inference(contradiction_clause,[status(thm)],[f21170]) ).
fof(f21484,plain,
! [X0,X1,X2,X3] :
( ~ sQ10_spl
| ~ subr(sK53_skl(X1,c360,X0),rprs_0)
| ~ sub(X2,X3)
| ~ arg2(sK53_skl(X1,c360,X0),X2)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X1)
| ~ arg1(X0,c360) ),
inference(resolution,[status(thm)],[f10708,f21140]) ).
fof(f21485,plain,
! [X0,X1,X2,X3] :
( ~ sQ10_spl
| ~ sub(X2,X3)
| ~ arg2(sK53_skl(X1,c360,X0),X2)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X1)
| ~ arg1(X0,c360) ),
inference(forward_subsumption_resolution,[status(thm)],[f21484,f10713]) ).
fof(f21486,plain,
! [X0,X1,X2] :
( ~ sQ10_spl
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X1)
| ~ arg1(X0,c360)
| ~ sub(X1,X2)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X1)
| ~ arg1(X0,c360) ),
inference(resolution,[status(thm)],[f21485,f10709]) ).
fof(f21487,plain,
! [X0,X1,X2] :
( ~ sQ10_spl
| ~ sub(X1,X2)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X1)
| ~ arg1(X0,c360) ),
inference(duplicate_literals_removal,[status(thm)],[f21486]) ).
fof(f21490,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ10_spl
| ~ sub(X3,X4)
| ~ member(X4,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X0,X3)
| ~ sub(X1,X2)
| ~ arg2(sK50_skl(X0),X1)
| ~ arg1(sK50_skl(X0),c360) ),
inference(resolution,[status(thm)],[f21487,f10697]) ).
fof(f21492,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ10_spl
| ~ sub(X4,X5)
| ~ member(X5,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c360,X4)
| ~ sub(X2,X3)
| ~ member(X3,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c360,X2)
| ~ sub(X0,X1)
| ~ arg2(sK50_skl(c360),X0) ),
inference(resolution,[status(thm)],[f21490,f10695]) ).
fof(f21493,plain,
( ~ sQ10_spl
| sQ9_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f21492,f21158,f21136,f21139]) ).
fof(f21494,plain,
$false,
inference(sat_refutation,[status(thm)],[f21081,f21090,f21092,f21105,f21107,f21109,f21129,f21145,f21147,f21149,f21153,f21169,f21171,f21493]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR116+13 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n020.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 15:09:18 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.22/0.49 % Drodi V4.1.1
% 69.64/9.33 % Refutation found
% 69.64/9.33 % SZS status Theorem for theBenchmark: Theorem is valid
% 69.64/9.33 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 45.54/9.51 % Elapsed time: 9.134185 seconds
% 45.54/9.51 % CPU time: 70.213372 seconds
% 45.54/9.51 % Total memory used: 579.038 MB
% 45.54/9.51 % Net memory used: 559.324 MB
%------------------------------------------------------------------------------