%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR116+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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 60.49s 8.37s
% Output : CNFRefutation 60.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 20
% Syntax : Number of formulae : 109 ( 24 unt; 14 def)
% Number of atoms : 828 ( 0 equ)
% Maximal formula atoms : 317 ( 7 avg)
% Number of connectives : 1057 ( 338 ~; 306 |; 396 &)
% ( 14 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 317 ( 10 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 43 ( 42 usr; 15 prp; 0-3 aty)
% Number of functors : 86 ( 86 usr; 81 con; 0-3 aty)
% Number of variables : 219 ( 189 !; 30 ?)
% 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(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(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,
( gener(equ_0,gener_c)
& fact(equ_0,real)
& sort(equ_0,st)
& gener(c55,sp)
& fact(c55,real)
& sort(c55,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(c52,con)
& refer(c52,det)
& quant(c52,one)
& gener(c52,sp)
& fact(c52,real)
& etype(c52,int0)
& card(c52,int1)
& sort(c52,ad)
& 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(c43,con)
& refer(c43,det)
& quant(c43,one)
& gener(c43,sp)
& fact(c43,real)
& etype(c43,int0)
& card(c43,int1)
& sort(c43,ad)
& varia(c31,varia_c)
& refer(c31,refer_c)
& quant(c31,quant_c)
& gener(c31,gener_c)
& fact(c31,real)
& etype(c31,etype_c)
& card(c31,card_c)
& sort(c31,ent)
& 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)
& varia(c199,con)
& refer(c199,det)
& quant(c199,one)
& gener(c199,sp)
& fact(c199,real)
& etype(c199,int0)
& card(c199,int1)
& sort(c199,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(c212,con)
& refer(c212,det)
& quant(c212,one)
& gener(c212,sp)
& fact(c212,real)
& etype(c212,int0)
& card(c212,int1)
& sort(c212,l)
& varia(c195,varia_c)
& refer(c195,indet)
& quant(c195,one)
& gener(c195,sp)
& fact(c195,real)
& etype(c195,int0)
& card(c195,int1)
& sort(c195,na)
& varia(c194,varia_c)
& refer(c194,indet)
& quant(c194,one)
& gener(c194,sp)
& fact(c194,real)
& etype(c194,int0)
& card(c194,int1)
& sort(c194,na)
& card(c16,int5)
& sort(c16,nu)
& varia(monat_1_1,varia_c)
& refer(monat_1_1,refer_c)
& quant(monat_1_1,quant_c)
& gener(monat_1_1,ge)
& fact(monat_1_1,real)
& etype(monat_1_1,etype_c)
& card(monat_1_1,card_c)
& sort(monat_1_1,ta)
& sort(monat_1_1,oa)
& sort(monat_1_1,me)
& sort(s__374dafrika_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(c188,varia_c)
& refer(c188,indet)
& quant(c188,one)
& gener(c188,sp)
& fact(c188,real)
& etype(c188,int0)
& card(c188,int1)
& sort(c188,na)
& varia(c193,con)
& refer(c193,det)
& quant(c193,one)
& gener(c193,sp)
& fact(c193,real)
& etype(c193,int0)
& card(c193,int1)
& sort(c193,d)
& varia(c187,con)
& refer(c187,det)
& quant(c187,one)
& gener(c187,sp)
& fact(c187,real)
& etype(c187,int0)
& card(c187,int1)
& sort(c187,io)
& sort(c187,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(c183,varia_c)
& refer(c183,refer_c)
& quant(c183,one)
& gener(c183,ge)
& fact(c183,real)
& etype(c183,int0)
& card(c183,int1)
& sort(c183,d)
& card(c15,int10)
& sort(c15,nu)
& varia(tag_1_1,varia_c)
& refer(tag_1_1,refer_c)
& quant(tag_1_1,quant_c)
& gener(tag_1_1,ge)
& fact(tag_1_1,real)
& etype(tag_1_1,etype_c)
& card(tag_1_1,card_c)
& sort(tag_1_1,ta)
& sort(tag_1_1,oa)
& sort(tag_1_1,me)
& varia(c19,varia_c)
& refer(c19,refer_c)
& quant(c19,quant_c)
& gener(c19,sp)
& fact(c19,real)
& etype(c19,etype_c)
& card(c19,card_c)
& sort(c19,ta)
& sort(c19,oa)
& sort(c19,me)
& varia(c18,varia_c)
& refer(c18,refer_c)
& quant(c18,quant_c)
& gener(c18,sp)
& fact(c18,real)
& etype(c18,etype_c)
& card(c18,card_c)
& sort(c18,ta)
& sort(c18,oa)
& sort(c18,me)
& varia(c17,con)
& refer(c17,det)
& quant(c17,one)
& gener(c17,sp)
& fact(c17,real)
& etype(c17,int0)
& card(c17,int1)
& sort(c17,t)
& sort(pretoria_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(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(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(c210,varia_c)
& refer(c210,indet)
& quant(c210,one)
& gener(c210,sp)
& fact(c210,real)
& etype(c210,int0)
& card(c210,int1)
& sort(c210,na)
& varia(c12,varia_c)
& refer(c12,indet)
& quant(c12,one)
& gener(c12,sp)
& fact(c12,real)
& etype(c12,int0)
& card(c12,int1)
& sort(c12,na)
& varia(c11,con)
& refer(c11,det)
& quant(c11,one)
& gener(c11,sp)
& fact(c11,real)
& etype(c11,int0)
& card(c11,int1)
& sort(c11,io)
& sort(c11,d)
& sub(hauptsstadt_1_1,stadt__1_1)
& subr(c55,equ_0)
& arg2(c55,c43)
& arg1(c55,c43)
& subs(c52,freude_1_1)
& prop(c52,ausgelassen_1_1)
& attch(c52,c43)
& temp(c43,c199)
& subs(c43,vereidigung_1_1)
& subs(c43,feier__1_1)
& prop(c43,afrikanisch__1_1)
& obj(c43,c193)
& equ(c43,c43)
& tupl(c31,c11,c17)
& in(c212,c11)
& val(c210,pretoria_0)
& sub(c210,name_1_1)
& sub(c199,dienstag__1_1)
& val(c195,mandela_0)
& sub(c195,familiename_1_1)
& val(c194,nelson_0)
& sub(c194,eigenname_1_1)
& sub(c193,c183)
& prop(c193,schwarz_1_1)
& loc(c193,c212)
& attr(c193,c195)
& attr(c193,c194)
& val(c19,c16)
& sub(c19,monat_1_1)
& val(c188,s__374dafrika_0)
& sub(c188,name_1_1)
& sub(c187,land_1_1)
& attr(c187,c188)
& attch(c187,c193)
& pmod(c183,erst_1_1,pr__344sident_1_1)
& val(c18,c15)
& sub(c18,tag_1_1)
& attr(c17,c19)
& attr(c17,c18)
& val(c12,pretoria_0)
& sub(c12,name_1_1)
& sub(c11,stadt__1_1)
& sub(c11,hauptsstadt_1_1)
& attr(c11,c210)
& attr(c11,c12) ),
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(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)
| ~ 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(f20828,plain,
pmod(c183,erst_1_1,pr__344sident_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20830,plain,
attr(c187,c188),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20832,plain,
sub(c188,name_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20833,plain,
val(c188,s__374dafrika_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20836,plain,
attr(c193,c194),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20837,plain,
attr(c193,c195),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20839,plain,
prop(c193,schwarz_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20840,plain,
sub(c193,c183),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20841,plain,
sub(c194,eigenname_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20842,plain,
val(c194,nelson_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20843,plain,
sub(c195,familiename_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20844,plain,
val(c195,mandela_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f21170,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(f21171,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)],[f21170]) ).
fof(f21173,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(f21174,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ val(X1,s__374dafrika_0)
| ~ sub(X1,name_1_1)
| ~ attr(X0,X1) ),
inference(component_clause,[status(thm)],[f21173]) ).
fof(f21176,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f20817,f21170,f21173]) ).
fof(f21178,definition,
! [X0] :
( sQ2_spl
<=> ( ~ sub(c193,X0)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f21179,plain,
! [X0] :
( ~ sQ2_spl
| ~ sub(c193,X0)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ),
inference(component_clause,[status(thm)],[f21178]) ).
fof(f21202,plain,
( ~ sQ2_spl
| ~ pmod(c183,erst_1_1,pr__344sident_1_1) ),
inference(resolution,[status(thm)],[f21179,f20840]) ).
fof(f21203,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21202,f20828]) ).
fof(f21204,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f21203]) ).
fof(f21207,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ0_spl
| ~ val(c194,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,c194)
| ~ attr(X2,X4)
| ~ arg2(X1,X3)
| ~ arg1(X1,X2)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ),
inference(resolution,[status(thm)],[f20841,f21171]) ).
fof(f21212,definition,
( sQ7_spl
<=> val(c194,nelson_0) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f21214,plain,
( sQ7_spl
| ~ val(c194,nelson_0) ),
inference(component_clause,[status(thm)],[f21212]) ).
fof(f21216,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ8_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,c194)
| ~ attr(X2,X4)
| ~ arg2(X1,X3)
| ~ arg1(X1,X2)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f21217,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ8_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,c194)
| ~ attr(X2,X4)
| ~ arg2(X1,X3)
| ~ arg1(X1,X2)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ),
inference(component_clause,[status(thm)],[f21216]) ).
fof(f21219,plain,
( ~ sQ0_spl
| ~ sQ7_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f21207,f21216,f21212,f21170]) ).
fof(f21220,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21214,f20842]) ).
fof(f21221,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f21220]) ).
fof(f21230,plain,
! [X0] :
( ~ sQ1_spl
| ~ sub(c188,name_1_1)
| ~ attr(X0,c188) ),
inference(resolution,[status(thm)],[f21174,f20833]) ).
fof(f21231,definition,
! [X0] :
( sQ9_spl
<=> ~ attr(X0,c188) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f21232,plain,
! [X0] :
( ~ sQ9_spl
| ~ attr(X0,c188) ),
inference(component_clause,[status(thm)],[f21231]) ).
fof(f21234,definition,
( sQ10_spl
<=> sub(c188,name_1_1) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f21236,plain,
( sQ10_spl
| ~ sub(c188,name_1_1) ),
inference(component_clause,[status(thm)],[f21234]) ).
fof(f21237,plain,
( ~ sQ1_spl
| ~ sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f21230,f21231,f21234,f21173]) ).
fof(f21238,plain,
( ~ sQ9_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f20830,f21232]) ).
fof(f21239,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f21238]) ).
fof(f21240,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21236,f20832]) ).
fof(f21241,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f21240]) ).
fof(f21244,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ8_spl
| ~ val(c195,mandela_0)
| ~ subr(X1,rprs_0)
| ~ sub(X3,X0)
| ~ prop(X3,schwarz_1_1)
| ~ obj(X4,X2)
| ~ attr(X2,c194)
| ~ attr(X2,c195)
| ~ arg2(X1,X3)
| ~ arg1(X1,X2)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ),
inference(resolution,[status(thm)],[f21217,f20843]) ).
fof(f21257,definition,
! [X0,X1,X2,X3,X4] :
( sQ14_spl
<=> ( ~ subr(X1,rprs_0)
| ~ sub(X3,X0)
| ~ prop(X3,schwarz_1_1)
| ~ obj(X4,X2)
| ~ attr(X2,c194)
| ~ attr(X2,c195)
| ~ arg2(X1,X3)
| ~ arg1(X1,X2)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f21258,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ14_spl
| ~ subr(X1,rprs_0)
| ~ sub(X3,X0)
| ~ prop(X3,schwarz_1_1)
| ~ obj(X4,X2)
| ~ attr(X2,c194)
| ~ attr(X2,c195)
| ~ arg2(X1,X3)
| ~ arg1(X1,X2)
| ~ pmod(X0,erst_1_1,pr__344sident_1_1) ),
inference(component_clause,[status(thm)],[f21257]) ).
fof(f21260,definition,
( sQ15_spl
<=> val(c195,mandela_0) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f21262,plain,
( sQ15_spl
| ~ val(c195,mandela_0) ),
inference(component_clause,[status(thm)],[f21260]) ).
fof(f21263,plain,
( ~ sQ8_spl
| ~ sQ15_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f21244,f21257,f21260,f21216]) ).
fof(f21270,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21262,f20844]) ).
fof(f21271,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f21270]) ).
fof(f21294,definition,
( sQ18_spl
<=> attr(c193,c194) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f21296,plain,
( sQ18_spl
| ~ attr(c193,c194) ),
inference(component_clause,[status(thm)],[f21294]) ).
fof(f21310,definition,
! [X0,X1] :
( sQ20_spl
<=> ( ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c193,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f21311,plain,
! [X0,X1] :
( ~ sQ20_spl
| ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c193,X0) ),
inference(component_clause,[status(thm)],[f21310]) ).
fof(f21326,plain,
! [X0,X1] :
( arg2(sK50_skl(X0),X0)
| ~ sub(X1,eigenname_1_1)
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[f10696,f10191]) ).
fof(f21327,plain,
! [X0] :
( arg2(sK50_skl(X0),X0)
| ~ attr(X0,c194) ),
inference(resolution,[status(thm)],[f21326,f20841]) ).
fof(f21328,plain,
arg2(sK50_skl(c193),c193),
inference(resolution,[status(thm)],[f21327,f20836]) ).
fof(f21352,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ14_spl
| ~ subr(X4,rprs_0)
| ~ sub(X5,X3)
| ~ prop(X5,schwarz_1_1)
| ~ attr(X0,c194)
| ~ attr(X0,c195)
| ~ arg2(X4,X5)
| ~ arg1(X4,X0)
| ~ pmod(X3,erst_1_1,pr__344sident_1_1)
| ~ 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,f21258]) ).
fof(f21356,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ14_spl
| ~ subr(X4,rprs_0)
| ~ sub(c193,X3)
| ~ attr(X0,c194)
| ~ attr(X0,c195)
| ~ arg2(X4,c193)
| ~ arg1(X4,X0)
| ~ pmod(X3,erst_1_1,pr__344sident_1_1)
| ~ 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)],[f21352,f20839]) ).
fof(f21359,definition,
! [X0,X1,X2,X4] :
( sQ26_spl
<=> ( ~ subr(X4,rprs_0)
| ~ attr(X0,c194)
| ~ attr(X0,c195)
| ~ arg2(X4,c193)
| ~ arg1(X4,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,[sQ26_spl])],[split_symbol_definition]) ).
fof(f21360,plain,
! [X0,X1,X2,X3] :
( ~ sQ26_spl
| ~ subr(X3,rprs_0)
| ~ attr(X0,c194)
| ~ attr(X0,c195)
| ~ arg2(X3,c193)
| ~ 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)],[f21359]) ).
fof(f21362,plain,
( ~ sQ14_spl
| sQ2_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f21356,f21359,f21178,f21257]) ).
fof(f21363,plain,
! [X0,X1,X2] :
( ~ sQ26_spl
| ~ subr(X2,rprs_0)
| ~ attr(c193,c194)
| ~ arg2(X2,c193)
| ~ arg1(X2,c193)
| ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c193,X0) ),
inference(resolution,[status(thm)],[f21360,f20837]) ).
fof(f21364,definition,
! [X2] :
( sQ27_spl
<=> ( ~ subr(X2,rprs_0)
| ~ arg2(X2,c193)
| ~ arg1(X2,c193) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f21365,plain,
! [X0] :
( ~ sQ27_spl
| ~ subr(X0,rprs_0)
| ~ arg2(X0,c193)
| ~ arg1(X0,c193) ),
inference(component_clause,[status(thm)],[f21364]) ).
fof(f21367,plain,
( ~ sQ26_spl
| ~ sQ18_spl
| sQ27_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f21363,f21310,f21364,f21294,f21359]) ).
fof(f21369,plain,
! [X0] :
( ~ sQ20_spl
| ~ sub(X0,eigenname_1_1)
| ~ attr(c193,X0) ),
inference(resolution,[status(thm)],[f21311,f10191]) ).
fof(f21370,plain,
( ~ sQ20_spl
| ~ attr(c193,c194) ),
inference(resolution,[status(thm)],[f21369,f20841]) ).
fof(f21371,plain,
( ~ sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21370,f20836]) ).
fof(f21372,plain,
~ sQ20_spl,
inference(contradiction_clause,[status(thm)],[f21371]) ).
fof(f21373,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21296,f20836]) ).
fof(f21374,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f21373]) ).
fof(f21430,definition,
( sQ35_spl
<=> arg2(sK50_skl(c193),c193) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f21432,plain,
( sQ35_spl
| ~ arg2(sK50_skl(c193),c193) ),
inference(component_clause,[status(thm)],[f21430]) ).
fof(f24442,plain,
! [X0,X1] :
( ~ sQ27_spl
| ~ subr(sK53_skl(X1,c193,X0),rprs_0)
| ~ arg2(sK53_skl(X1,c193,X0),c193)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X1)
| ~ arg1(X0,c193) ),
inference(resolution,[status(thm)],[f10708,f21365]) ).
fof(f24444,plain,
! [X0,X1] :
( ~ sQ27_spl
| ~ arg2(sK53_skl(X1,c193,X0),c193)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X1)
| ~ arg1(X0,c193) ),
inference(forward_subsumption_resolution,[status(thm)],[f24442,f10713]) ).
fof(f24450,plain,
! [X0] :
( ~ sQ27_spl
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,c193)
| ~ arg1(X0,c193)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,c193)
| ~ arg1(X0,c193) ),
inference(resolution,[status(thm)],[f24444,f10709]) ).
fof(f24451,plain,
! [X0] :
( ~ sQ27_spl
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,c193)
| ~ arg1(X0,c193) ),
inference(duplicate_literals_removal,[status(thm)],[f24450]) ).
fof(f24454,plain,
! [X0,X1,X2] :
( ~ sQ27_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),c193)
| ~ arg1(sK50_skl(X0),c193) ),
inference(resolution,[status(thm)],[f24451,f10697]) ).
fof(f24456,plain,
! [X0,X1,X2,X3] :
( ~ sQ27_spl
| ~ sub(X2,X3)
| ~ member(X3,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c193,X2)
| ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c193,X0)
| ~ arg2(sK50_skl(c193),c193) ),
inference(resolution,[status(thm)],[f24454,f10695]) ).
fof(f24457,plain,
( ~ sQ27_spl
| sQ20_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f24456,f21430,f21310,f21364]) ).
fof(f24458,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21432,f21328]) ).
fof(f24459,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f24458]) ).
fof(f24460,plain,
$false,
inference(sat_refutation,[status(thm)],[f21176,f21204,f21219,f21221,f21237,f21239,f21241,f21263,f21271,f21362,f21367,f21372,f21374,f24457,f24459]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR116+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.45 % Computer : n002.cluster.edu
% 0.17/0.45 % Model : x86_64 x86_64
% 0.17/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.45 % Memory : 8046.5625MB
% 0.17/0.45 % OS : Linux 6.8.0-71-generic
% 0.17/0.45 % CPULimit : 300
% 0.17/0.45 % WCLimit : 300
% 0.17/0.45 % DateTime : Mon Sep 21 15:12:33 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.42/0.67 % Drodi V4.1.1
% 60.49/8.37 % Refutation found
% 60.49/8.37 % SZS status Theorem for theBenchmark: Theorem is valid
% 60.49/8.37 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 56.05/8.48 % Elapsed time: 8.013297 seconds
% 56.05/8.48 % CPU time: 61.242695 seconds
% 56.05/8.48 % Total memory used: 542.950 MB
% 56.05/8.48 % Net memory used: 525.653 MB
%------------------------------------------------------------------------------