%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR116+41 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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:13 PM UTC 2026
% Result : Theorem 64.25s 8.92s
% Output : CNFRefutation 64.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 20
% Syntax : Number of formulae : 107 ( 25 unt; 15 def)
% Number of atoms : 722 ( 0 equ)
% Maximal formula atoms : 247 ( 6 avg)
% Number of connectives : 932 ( 317 ~; 286 |; 312 &)
% ( 15 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 247 ( 9 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 42 ( 41 usr; 16 prp; 0-3 aty)
% Number of functors : 70 ( 70 usr; 66 con; 0-3 aty)
% Number of variables : 197 ( 170 !; 27 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : member(X0,cons(X0,X1)),
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(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)
& prop(X4,schwarz_1_1)
& obj(X7,X0)
& attr(X5,X6)
& attr(X0,X2)
& attr(X0,X1)
& arg2(X3,X4)
& arg1(X3,X0)
& pmod(X8,erst_1_1,pr__344sident_1_1) ),
file('/export/starexec/sandbox/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)
& prop(X4,schwarz_1_1)
& obj(X7,X0)
& attr(X5,X6)
& attr(X0,X2)
& attr(X0,X1)
& arg2(X3,X4)
& arg1(X3,X0)
& pmod(X8,erst_1_1,pr__344sident_1_1) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,hypothesis,
( varia(mensch_1_1,varia_c)
& refer(mensch_1_1,refer_c)
& quant(mensch_1_1,quant_c)
& gener(mensch_1_1,gener_c)
& fact(mensch_1_1,real)
& etype(mensch_1_1,etype_c)
& card(mensch_1_1,card_c)
& sort(mensch_1_1,ent)
& 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)
& gener(equ_0,gener_c)
& fact(equ_0,real)
& sort(equ_0,st)
& gener(c23,sp)
& fact(c23,real)
& sort(c23,st)
& varia(freude_1_1,varia_c)
& refer(freude_1_1,refer_c)
& quant(freude_1_1,one)
& gener(freude_1_1,ge)
& fact(freude_1_1,real)
& etype(freude_1_1,int0)
& card(freude_1_1,int1)
& sort(freude_1_1,ad)
& sort(ausgelassen_1_1,ql)
& varia(c20,con)
& refer(c20,det)
& quant(c20,one)
& gener(c20,sp)
& fact(c20,real)
& etype(c20,int0)
& card(c20,int1)
& sort(c20,ad)
& sort(pretoria_0,fe)
& varia(hauptsstadt_1_1,varia_c)
& refer(hauptsstadt_1_1,refer_c)
& quant(hauptsstadt_1_1,one)
& gener(hauptsstadt_1_1,ge)
& fact(hauptsstadt_1_1,real)
& etype(hauptsstadt_1_1,int0)
& card(hauptsstadt_1_1,int1)
& sort(hauptsstadt_1_1,io)
& sort(hauptsstadt_1_1,d)
& varia(c178,varia_c)
& refer(c178,indet)
& quant(c178,one)
& gener(c178,sp)
& fact(c178,real)
& etype(c178,int0)
& card(c178,int1)
& sort(c178,na)
& varia(c177,con)
& refer(c177,det)
& quant(c177,one)
& gener(c177,sp)
& fact(c177,real)
& etype(c177,int0)
& card(c177,int1)
& sort(c177,io)
& sort(c177,d)
& varia(dienstag__1_1,varia_c)
& refer(dienstag__1_1,refer_c)
& quant(dienstag__1_1,one)
& gener(dienstag__1_1,ge)
& fact(dienstag__1_1,real)
& etype(dienstag__1_1,int0)
& card(dienstag__1_1,int1)
& sort(dienstag__1_1,ta)
& 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)
& sort(schwarz_1_1,tq)
& varia(c180,con)
& refer(c180,det)
& quant(c180,one)
& gener(c180,sp)
& fact(c180,real)
& etype(c180,int0)
& card(c180,int1)
& sort(c180,l)
& varia(c163,varia_c)
& refer(c163,indet)
& quant(c163,one)
& gener(c163,sp)
& fact(c163,real)
& etype(c163,int0)
& card(c163,int1)
& sort(c163,na)
& varia(c162,varia_c)
& refer(c162,indet)
& quant(c162,one)
& gener(c162,sp)
& fact(c162,real)
& etype(c162,int0)
& card(c162,int1)
& sort(c162,na)
& 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(c156,varia_c)
& refer(c156,indet)
& quant(c156,one)
& gener(c156,sp)
& fact(c156,real)
& etype(c156,int0)
& card(c156,int1)
& sort(c156,na)
& varia(c155,con)
& refer(c155,det)
& quant(c155,one)
& gener(c155,sp)
& fact(c155,real)
& etype(c155,int0)
& card(c155,int1)
& sort(c155,io)
& sort(c155,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)
& card(erst_1_1,int1)
& sort(erst_1_1,oq)
& varia(c151,varia_c)
& refer(c151,refer_c)
& quant(c151,one)
& gener(c151,ge)
& fact(c151,real)
& etype(c151,int0)
& card(c151,int1)
& sort(c151,d)
& varia(c167,con)
& refer(c167,det)
& quant(c167,one)
& gener(c167,sp)
& fact(c167,real)
& etype(c167,int0)
& card(c167,int1)
& sort(c167,ta)
& varia(vereidigung_1_1,varia_c)
& refer(vereidigung_1_1,refer_c)
& quant(vereidigung_1_1,one)
& gener(vereidigung_1_1,ge)
& fact(vereidigung_1_1,real)
& etype(vereidigung_1_1,int0)
& card(vereidigung_1_1,int1)
& sort(vereidigung_1_1,ad)
& varia(feier__1_1,varia_c)
& refer(feier__1_1,refer_c)
& quant(feier__1_1,one)
& gener(feier__1_1,ge)
& fact(feier__1_1,real)
& etype(feier__1_1,int0)
& card(feier__1_1,int1)
& sort(feier__1_1,ad)
& sort(afrikanisch__1_1,nq)
& varia(c161,con)
& refer(c161,det)
& quant(c161,one)
& gener(c161,sp)
& fact(c161,real)
& etype(c161,int0)
& card(c161,int1)
& sort(c161,d)
& varia(c11,varia_c)
& refer(c11,indet)
& quant(c11,one)
& gener(c11,sp)
& fact(c11,real)
& etype(c11,int0)
& card(c11,int1)
& sort(c11,ad)
& sub(pr__344sident_1_1,mensch_1_1)
& sub(hauptsstadt_1_1,stadt__1_1)
& subr(c23,equ_0)
& arg2(c23,c11)
& arg1(c23,c11)
& subs(c20,freude_1_1)
& prop(c20,ausgelassen_1_1)
& attch(c20,c11)
& in(c180,c177)
& val(c178,pretoria_0)
& sub(c178,name_1_1)
& sub(c177,hauptsstadt_1_1)
& attr(c177,c178)
& sub(c167,dienstag__1_1)
& val(c163,mandela_0)
& sub(c163,familiename_1_1)
& val(c162,nelson_0)
& sub(c162,eigenname_1_1)
& sub(c161,c151)
& prop(c161,schwarz_1_1)
& loc(c161,c180)
& attr(c161,c163)
& attr(c161,c162)
& val(c156,s__374dafrika_0)
& sub(c156,name_1_1)
& sub(c155,land_1_1)
& attr(c155,c156)
& attch(c155,c161)
& pmod(c151,erst_1_1,pr__344sident_1_1)
& temp(c11,c167)
& subs(c11,vereidigung_1_1)
& subs(c11,feier__1_1)
& prop(c11,afrikanisch__1_1)
& obj(c11,c161)
& equ(c11,c11) ),
file('/export/starexec/sandbox/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(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)
| ~ prop(X4,schwarz_1_1)
| ~ obj(X7,X0)
| ~ attr(X5,X6)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4)
| ~ arg1(X3,X0)
| ~ pmod(X8,erst_1_1,pr__344sident_1_1) ),
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)
| ~ prop(X4,schwarz_1_1)
| ! [X0] :
( ! [X7] : ~ obj(X7,X0)
| ! [X5] : ~ attr(X5,X6)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4)
| ~ arg1(X3,X0)
| ~ pmod(X8,erst_1_1,pr__344sident_1_1) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f20815]) ).
fof(f20817,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ val(X7,s__374dafrika_0)
| ~ val(X5,nelson_0)
| ~ val(X4,mandela_0)
| ~ subr(X1,rprs_0)
| ~ sub(X7,name_1_1)
| ~ sub(X3,X0)
| ~ sub(X5,eigenname_1_1)
| ~ sub(X4,familiename_1_1)
| ~ prop(X3,schwarz_1_1)
| ~ obj(X8,X2)
| ~ attr(X6,X7)
| ~ attr(X2,X5)
| ~ attr(X2,X4)
| ~ arg2(X1,X3)
| ~ arg1(X1,X2)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ),
inference(cnf_transformation,[status(thm)],[f20816]) ).
fof(f20819,plain,
obj(c11,c161),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20824,plain,
pmod(c151,erst_1_1,pr__344sident_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20826,plain,
attr(c155,c156),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20828,plain,
sub(c156,name_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20829,plain,
val(c156,s__374dafrika_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20830,plain,
attr(c161,c162),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20831,plain,
attr(c161,c163),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20833,plain,
prop(c161,schwarz_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20834,plain,
sub(c161,c151),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20835,plain,
sub(c162,eigenname_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20836,plain,
val(c162,nelson_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20837,plain,
sub(c163,familiename_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20838,plain,
val(c163,mandela_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f21100,definition,
! [X0,X1,X2,X3,X4,X5,X8] :
( sQ0_spl
<=> ( ~ val(X5,nelson_0)
| ~ val(X4,mandela_0)
| ~ subr(X1,rprs_0)
| ~ sub(X3,X0)
| ~ sub(X5,eigenname_1_1)
| ~ sub(X4,familiename_1_1)
| ~ prop(X3,schwarz_1_1)
| ~ obj(X8,X2)
| ~ attr(X2,X5)
| ~ attr(X2,X4)
| ~ arg2(X1,X3)
| ~ arg1(X1,X2)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f21101,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ0_spl
| ~ val(X5,nelson_0)
| ~ val(X4,mandela_0)
| ~ subr(X1,rprs_0)
| ~ sub(X3,X0)
| ~ sub(X5,eigenname_1_1)
| ~ sub(X4,familiename_1_1)
| ~ prop(X3,schwarz_1_1)
| ~ obj(X6,X2)
| ~ attr(X2,X5)
| ~ attr(X2,X4)
| ~ arg2(X1,X3)
| ~ arg1(X1,X2)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ),
inference(component_clause,[status(thm)],[f21100]) ).
fof(f21103,definition,
! [X6,X7] :
( sQ1_spl
<=> ( ~ val(X7,s__374dafrika_0)
| ~ sub(X7,name_1_1)
| ~ attr(X6,X7) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f21104,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ val(X1,s__374dafrika_0)
| ~ sub(X1,name_1_1)
| ~ attr(X0,X1) ),
inference(component_clause,[status(thm)],[f21103]) ).
fof(f21106,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f20817,f21100,f21103]) ).
fof(f21108,definition,
! [X0] :
( sQ2_spl
<=> ( ~ sub(c161,X0)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f21109,plain,
! [X0] :
( ~ sQ2_spl
| ~ sub(c161,X0)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ),
inference(component_clause,[status(thm)],[f21108]) ).
fof(f21131,plain,
( ~ sQ2_spl
| ~ pmod(c151,erst_1_1,pr__344sident_1_1) ),
inference(resolution,[status(thm)],[f20834,f21109]) ).
fof(f21133,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21131,f20824]) ).
fof(f21134,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f21133]) ).
fof(f21135,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ0_spl
| ~ val(c162,nelson_0)
| ~ val(X4,mandela_0)
| ~ subr(X1,rprs_0)
| ~ sub(X3,X0)
| ~ sub(X4,familiename_1_1)
| ~ prop(X3,schwarz_1_1)
| ~ obj(X5,X2)
| ~ attr(X2,c162)
| ~ attr(X2,X4)
| ~ arg2(X1,X3)
| ~ arg1(X1,X2)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ),
inference(resolution,[status(thm)],[f20835,f21101]) ).
fof(f21137,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ6_spl
<=> ( ~ val(X4,mandela_0)
| ~ subr(X1,rprs_0)
| ~ sub(X3,X0)
| ~ sub(X4,familiename_1_1)
| ~ prop(X3,schwarz_1_1)
| ~ obj(X5,X2)
| ~ attr(X2,c162)
| ~ attr(X2,X4)
| ~ arg2(X1,X3)
| ~ arg1(X1,X2)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f21138,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ6_spl
| ~ val(X4,mandela_0)
| ~ subr(X1,rprs_0)
| ~ sub(X3,X0)
| ~ sub(X4,familiename_1_1)
| ~ prop(X3,schwarz_1_1)
| ~ obj(X5,X2)
| ~ attr(X2,c162)
| ~ attr(X2,X4)
| ~ arg2(X1,X3)
| ~ arg1(X1,X2)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ),
inference(component_clause,[status(thm)],[f21137]) ).
fof(f21140,definition,
( sQ7_spl
<=> val(c162,nelson_0) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f21142,plain,
( sQ7_spl
| ~ val(c162,nelson_0) ),
inference(component_clause,[status(thm)],[f21140]) ).
fof(f21143,plain,
( ~ sQ0_spl
| ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f21135,f21137,f21140,f21100]) ).
fof(f21144,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21142,f20836]) ).
fof(f21145,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f21144]) ).
fof(f21153,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ6_spl
| ~ val(c163,mandela_0)
| ~ subr(X1,rprs_0)
| ~ sub(X3,X0)
| ~ prop(X3,schwarz_1_1)
| ~ obj(X4,X2)
| ~ attr(X2,c162)
| ~ attr(X2,c163)
| ~ arg2(X1,X3)
| ~ arg1(X1,X2)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ),
inference(resolution,[status(thm)],[f21138,f20837]) ).
fof(f21155,definition,
! [X0,X1,X2] :
( sQ8_spl
<=> ( ~ subr(X1,rprs_0)
| ~ sub(X2,X0)
| ~ prop(X2,schwarz_1_1)
| ~ arg2(X1,X2)
| ~ arg1(X1,c161)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f21156,plain,
! [X0,X1,X2] :
( ~ sQ8_spl
| ~ subr(X1,rprs_0)
| ~ sub(X2,X0)
| ~ prop(X2,schwarz_1_1)
| ~ arg2(X1,X2)
| ~ arg1(X1,c161)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ),
inference(component_clause,[status(thm)],[f21155]) ).
fof(f21169,definition,
! [X0,X1,X2,X3,X4] :
( sQ12_spl
<=> ( ~ subr(X1,rprs_0)
| ~ sub(X3,X0)
| ~ prop(X3,schwarz_1_1)
| ~ obj(X4,X2)
| ~ attr(X2,c162)
| ~ attr(X2,c163)
| ~ arg2(X1,X3)
| ~ arg1(X1,X2)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f21170,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ12_spl
| ~ subr(X1,rprs_0)
| ~ sub(X3,X0)
| ~ prop(X3,schwarz_1_1)
| ~ obj(X4,X2)
| ~ attr(X2,c162)
| ~ attr(X2,c163)
| ~ arg2(X1,X3)
| ~ arg1(X1,X2)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ),
inference(component_clause,[status(thm)],[f21169]) ).
fof(f21172,definition,
( sQ13_spl
<=> val(c163,mandela_0) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f21174,plain,
( sQ13_spl
| ~ val(c163,mandela_0) ),
inference(component_clause,[status(thm)],[f21172]) ).
fof(f21175,plain,
( ~ sQ6_spl
| ~ sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f21153,f21169,f21172,f21137]) ).
fof(f21180,plain,
! [X0] :
( ~ sQ1_spl
| ~ sub(c156,name_1_1)
| ~ attr(X0,c156) ),
inference(resolution,[status(thm)],[f21104,f20829]) ).
fof(f21181,definition,
! [X0] :
( sQ15_spl
<=> ~ attr(X0,c156) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f21182,plain,
! [X0] :
( ~ sQ15_spl
| ~ attr(X0,c156) ),
inference(component_clause,[status(thm)],[f21181]) ).
fof(f21184,definition,
( sQ16_spl
<=> sub(c156,name_1_1) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f21186,plain,
( sQ16_spl
| ~ sub(c156,name_1_1) ),
inference(component_clause,[status(thm)],[f21184]) ).
fof(f21187,plain,
( ~ sQ1_spl
| ~ sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f21180,f21181,f21184,f21103]) ).
fof(f21188,plain,
( ~ sQ15_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f20826,f21182]) ).
fof(f21189,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f21188]) ).
fof(f21190,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21186,f20828]) ).
fof(f21191,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f21190]) ).
fof(f21194,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21174,f20838]) ).
fof(f21195,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f21194]) ).
fof(f21214,plain,
! [X0,X1,X2] :
( ~ sQ12_spl
| ~ subr(X1,rprs_0)
| ~ sub(X2,X0)
| ~ prop(X2,schwarz_1_1)
| ~ attr(c161,c162)
| ~ attr(c161,c163)
| ~ arg2(X1,X2)
| ~ arg1(X1,c161)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ),
inference(resolution,[status(thm)],[f20819,f21170]) ).
fof(f21217,definition,
( sQ17_spl
<=> attr(c161,c163) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f21219,plain,
( sQ17_spl
| ~ attr(c161,c163) ),
inference(component_clause,[status(thm)],[f21217]) ).
fof(f21220,definition,
( sQ18_spl
<=> attr(c161,c162) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f21222,plain,
( sQ18_spl
| ~ attr(c161,c162) ),
inference(component_clause,[status(thm)],[f21220]) ).
fof(f21223,plain,
( ~ sQ12_spl
| ~ sQ18_spl
| ~ sQ17_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f21214,f21155,f21217,f21220,f21169]) ).
fof(f21238,definition,
! [X0,X1] :
( sQ20_spl
<=> ( ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c161,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f21239,plain,
! [X0,X1] :
( ~ sQ20_spl
| ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c161,X0) ),
inference(component_clause,[status(thm)],[f21238]) ).
fof(f21248,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21222,f20830]) ).
fof(f21249,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f21248]) ).
fof(f21252,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21219,f20831]) ).
fof(f21253,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f21252]) ).
fof(f21255,plain,
! [X0,X1] :
( arg2(sK50_skl(X0),X0)
| ~ sub(X1,eigenname_1_1)
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[f10696,f10191]) ).
fof(f21256,plain,
! [X0] :
( arg2(sK50_skl(X0),X0)
| ~ attr(X0,c162) ),
inference(resolution,[status(thm)],[f21255,f20835]) ).
fof(f21257,plain,
arg2(sK50_skl(c161),c161),
inference(resolution,[status(thm)],[f21256,f20830]) ).
fof(f22868,plain,
! [X0,X1,X2,X3] :
( ~ sQ8_spl
| ~ subr(sK53_skl(X1,c161,X0),rprs_0)
| ~ sub(X3,X2)
| ~ prop(X3,schwarz_1_1)
| ~ arg2(sK53_skl(X1,c161,X0),X3)
| ~ pmod(X2,erst_1_1,pr__344sident_1_1)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X1)
| ~ arg1(X0,c161) ),
inference(resolution,[status(thm)],[f10708,f21156]) ).
fof(f22869,plain,
! [X0,X1,X2,X3] :
( ~ sQ8_spl
| ~ sub(X3,X2)
| ~ prop(X3,schwarz_1_1)
| ~ arg2(sK53_skl(X1,c161,X0),X3)
| ~ pmod(X2,erst_1_1,pr__344sident_1_1)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X1)
| ~ arg1(X0,c161) ),
inference(forward_subsumption_resolution,[status(thm)],[f22868,f10713]) ).
fof(f22874,plain,
! [X0,X1,X2] :
( ~ sQ8_spl
| ~ sub(c161,X2)
| ~ arg2(sK53_skl(X1,c161,X0),c161)
| ~ pmod(X2,erst_1_1,pr__344sident_1_1)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X1)
| ~ arg1(X0,c161) ),
inference(resolution,[status(thm)],[f22869,f20833]) ).
fof(f22875,definition,
! [X0,X1] :
( sQ34_spl
<=> ( ~ arg2(sK53_skl(X1,c161,X0),c161)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X1)
| ~ arg1(X0,c161) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f22876,plain,
! [X0,X1] :
( ~ sQ34_spl
| ~ arg2(sK53_skl(X1,c161,X0),c161)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X1)
| ~ arg1(X0,c161) ),
inference(component_clause,[status(thm)],[f22875]) ).
fof(f22878,plain,
( ~ sQ8_spl
| sQ2_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f22874,f22875,f21108,f21155]) ).
fof(f22879,plain,
! [X0] :
( ~ sQ34_spl
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,c161)
| ~ arg1(X0,c161)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,c161)
| ~ arg1(X0,c161) ),
inference(resolution,[status(thm)],[f22876,f10709]) ).
fof(f22880,plain,
! [X0] :
( ~ sQ34_spl
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,c161)
| ~ arg1(X0,c161) ),
inference(duplicate_literals_removal,[status(thm)],[f22879]) ).
fof(f22883,plain,
! [X0,X1,X2] :
( ~ sQ34_spl
| ~ sub(X1,X2)
| ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X0,X1)
| ~ arg2(sK50_skl(X0),c161)
| ~ arg1(sK50_skl(X0),c161) ),
inference(resolution,[status(thm)],[f22880,f10697]) ).
fof(f22885,plain,
! [X0,X1,X2,X3] :
( ~ sQ34_spl
| ~ sub(X2,X3)
| ~ member(X3,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c161,X2)
| ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c161,X0)
| ~ arg2(sK50_skl(c161),c161) ),
inference(resolution,[status(thm)],[f22883,f10695]) ).
fof(f22886,definition,
( sQ35_spl
<=> arg2(sK50_skl(c161),c161) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f22888,plain,
( sQ35_spl
| ~ arg2(sK50_skl(c161),c161) ),
inference(component_clause,[status(thm)],[f22886]) ).
fof(f22889,plain,
( ~ sQ34_spl
| sQ20_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f22885,f22886,f21238,f22875]) ).
fof(f22896,plain,
! [X0] :
( ~ sQ20_spl
| ~ sub(X0,eigenname_1_1)
| ~ attr(c161,X0) ),
inference(resolution,[status(thm)],[f21239,f10191]) ).
fof(f22897,plain,
( ~ sQ20_spl
| ~ attr(c161,c162) ),
inference(resolution,[status(thm)],[f22896,f20835]) ).
fof(f22898,plain,
( ~ sQ20_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f22897,f21220,f21238]) ).
fof(f22899,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22888,f21257]) ).
fof(f22900,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f22899]) ).
fof(f22901,plain,
$false,
inference(sat_refutation,[status(thm)],[f21106,f21134,f21143,f21145,f21175,f21187,f21189,f21191,f21195,f21223,f21249,f21253,f22878,f22889,f22898,f22900]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR116+41 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n009.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 15:09:43 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.28/0.63 % Drodi V4.1.1
% 64.25/8.92 % Refutation found
% 64.25/8.92 % SZS status Theorem for theBenchmark: Theorem is valid
% 64.25/8.92 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.47/9.37 % Elapsed time: 8.901335 seconds
% 3.47/9.37 % CPU time: 66.151162 seconds
% 3.47/9.37 % Total memory used: 542.136 MB
% 3.47/9.37 % Net memory used: 521.217 MB
%------------------------------------------------------------------------------