%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR116+43 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:14:14 PM UTC 2026
% Result : Theorem 47.97s 11.66s
% Output : CNFRefutation 47.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 6
% Syntax : Number of formulae : 78 ( 14 unt; 0 def)
% Number of atoms : 741 ( 0 equ)
% Maximal formula atoms : 286 ( 9 avg)
% Number of connectives : 988 ( 325 ~; 290 |; 370 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 286 ( 14 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 30 ( 29 usr; 1 prp; 0-3 aty)
% Number of functors : 81 ( 81 usr; 74 con; 0-3 aty)
% Number of variables : 305 ( 265 !; 40 ?)
% Comments :
%------------------------------------------------------------------------------
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/sandbox2/benchmark/theBenchmark.p') ).
fof(f162,axiom,
! [X0,X1,X2] :
( ( subr(X0,sub_0)
& arg2(X0,X2)
& arg1(X0,X1) )
=> ? [X3,X4,X5] :
( subs(X3,bezeichnen_1_1)
& subr(X4,rprs_0)
& sub(X5,X2)
& obj(X3,X1)
& mcont(X3,X4)
& hsit(X0,X3)
& arg2(X4,X5)
& arg1(X4,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f163,axiom,
! [X0,X1] :
( sub(X0,X1)
=> ? [X2] :
( subr(X2,sub_0)
& arg2(X2,X1)
& arg1(X2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9161,axiom,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
file('/export/starexec/sandbox2/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/sandbox2/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(west__1_1,varia_c)
& refer(west__1_1,refer_c)
& quant(west__1_1,one)
& gener(west__1_1,ge)
& fact(west__1_1,real)
& etype(west__1_1,int0)
& card(west__1_1,int1)
& sort(west__1_1,io)
& sort(west__1_1,d)
& varia(sued_1_1,varia_c)
& refer(sued_1_1,refer_c)
& quant(sued_1_1,one)
& gener(sued_1_1,ge)
& fact(sued_1_1,real)
& etype(sued_1_1,int0)
& card(sued_1_1,int1)
& sort(sued_1_1,oa)
& varia(besuch_1_1,varia_c)
& refer(besuch_1_1,refer_c)
& quant(besuch_1_1,one)
& gener(besuch_1_1,ge)
& fact(besuch_1_1,real)
& etype(besuch_1_1,int0)
& card(besuch_1_1,int1)
& sort(besuch_1_1,as)
& sort(besuch_1_1,ad)
& 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(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(namibia_0,fe)
& sort(afrika_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(gebietsinstitution_1_1,varia_c)
& refer(gebietsinstitution_1_1,refer_c)
& quant(gebietsinstitution_1_1,one)
& gener(gebietsinstitution_1_1,ge)
& fact(gebietsinstitution_1_1,real)
& etype(gebietsinstitution_1_1,int0)
& card(gebietsinstitution_1_1,int1)
& sort(gebietsinstitution_1_1,io)
& sort(gebietsinstitution_1_1,d)
& varia(c56,varia_c)
& refer(c56,indet)
& quant(c56,one)
& gener(c56,sp)
& fact(c56,real)
& etype(c56,int0)
& card(c56,int1)
& sort(c56,na)
& gener(empfangen_1_1,ge)
& fact(empfangen_1_1,real)
& sort(empfangen_1_1,dn)
& varia(c55,con)
& refer(c55,det)
& quant(c55,one)
& gener(c55,sp)
& fact(c55,real)
& etype(c55,int0)
& card(c55,int1)
& sort(c55,io)
& sort(c55,d)
& gener(c53,sp)
& fact(c53,real)
& sort(c53,dn)
& 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(c6,varia_c)
& refer(c6,indet)
& quant(c6,one)
& gener(c6,sp)
& fact(c6,real)
& etype(c6,int0)
& card(c6,int1)
& sort(c6,na)
& varia(suedwest_1_1,varia_c)
& refer(suedwest_1_1,refer_c)
& quant(suedwest_1_1,one)
& gener(suedwest_1_1,ge)
& fact(suedwest_1_1,real)
& etype(suedwest_1_1,int0)
& card(suedwest_1_1,int1)
& sort(suedwest_1_1,io)
& sort(suedwest_1_1,d)
& sort(bundesdeutsch_1_1,tq)
& varia(staatgast_1_1,varia_c)
& refer(staatgast_1_1,refer_c)
& quant(staatgast_1_1,one)
& gener(staatgast_1_1,ge)
& fact(staatgast_1_1,real)
& etype(staatgast_1_1,int0)
& card(staatgast_1_1,int1)
& sort(staatgast_1_1,as)
& sort(staatgast_1_1,ad)
& card(erst_1_1,int1)
& sort(erst_1_1,oq)
& varia(c9,con)
& refer(c9,det)
& quant(c9,one)
& gener(c9,sp)
& fact(c9,real)
& etype(c9,int0)
& card(c9,int1)
& sort(c9,ta)
& gener(haben_1_1,ge)
& fact(haben_1_1,real)
& sort(haben_1_1,st)
& varia(c42,varia_c)
& refer(c42,refer_c)
& quant(c42,one)
& gener(c42,gener_c)
& fact(c42,real)
& etype(c42,int0)
& card(c42,int1)
& sort(c42,io)
& sort(c42,d)
& gener(c3,sp)
& fact(c3,real)
& sort(c3,st)
& varia(c32,varia_c)
& refer(c32,refer_c)
& quant(c32,one)
& gener(c32,ge)
& fact(c32,real)
& etype(c32,int0)
& card(c32,int1)
& sort(c32,as)
& sort(c32,ad)
& varia(c41,con)
& refer(c41,det)
& quant(c41,one)
& gener(c41,sp)
& fact(c41,real)
& etype(c41,int0)
& card(c41,int1)
& sort(c41,d)
& varia(c5,varia_c)
& refer(c5,det)
& quant(c5,one)
& gener(c5,sp)
& fact(c5,real)
& etype(c5,int0)
& card(c5,int1)
& sort(c5,o)
& 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)
& varia(c29,varia_c)
& refer(c29,det)
& quant(c29,one)
& gener(c29,sp)
& fact(c29,real)
& etype(c29,int0)
& card(c29,int1)
& sort(c29,as)
& sort(c29,ad)
& sort(s__374dafrikanisch_1_1,nq)
& varia(c21,varia_c)
& refer(c21,indet)
& quant(c21,one)
& gener(c21,sp)
& fact(c21,real)
& etype(c21,int0)
& card(c21,int1)
& sort(c21,na)
& varia(c20,varia_c)
& refer(c20,indet)
& quant(c20,one)
& gener(c20,sp)
& fact(c20,real)
& etype(c20,int0)
& card(c20,int1)
& sort(c20,na)
& varia(c19,con)
& refer(c19,det)
& quant(c19,one)
& gener(c19,sp)
& fact(c19,real)
& etype(c19,int0)
& card(c19,int1)
& sort(c19,d)
& varia(kolonie_1_1,varia_c)
& refer(kolonie_1_1,refer_c)
& quant(kolonie_1_1,one)
& gener(kolonie_1_1,ge)
& fact(kolonie_1_1,real)
& etype(kolonie_1_1,int0)
& card(kolonie_1_1,int1)
& sort(kolonie_1_1,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)
& sub(suedwest_1_1,west__1_1)
& assoc(suedwest_1_1,sued_1_1)
& subs(staatgast_1_1,besuch_1_1)
& assoc(staatgast_1_1,land_1_1)
& sub(pr__344sident_1_1,mensch_1_1)
& sub(c9,dienstag__1_1)
& val(c6,namibia_0)
& sub(c6,name_1_1)
& val(c56,afrika_0)
& sub(c56,name_1_1)
& sub(c55,gebietsinstitution_1_1)
& attr(c55,c56)
& subs(c53,empfangen_1_1)
& semrel(c53,c3)
& obj(c53,c55)
& sub(c5,land_1_1)
& attr(c5,c6)
& sub(c42,suedwest_1_1)
& sub(c41,c1)
& prop(c41,bundesdeutsch_1_1)
& pmod(c32,erst_1_1,staatgast_1_1)
& temp(c3,c9)
& subs(c3,haben_1_1)
& scar(c3,c5)
& obj(c3,c19)
& assoc(c3,c42)
& subs(c29,c32)
& obj(c29,c41)
& agt(c29,c5)
& val(c21,mandela_0)
& sub(c21,familiename_1_1)
& val(c20,nelson_0)
& sub(c20,eigenname_1_1)
& sub(c19,pr__344sident_1_1)
& purp(c19,c29)
& prop(c19,s__374dafrikanisch_1_1)
& attr(c19,c21)
& attr(c19,c20)
& pmod(c1,ehemalig_1_1,kolonie_1_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
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(X1,X2)
| ~ state_adjective_state_binding(X2,X0)
| in(sK49_skl(X0,X1),sK48_skl(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f10676]) ).
fof(f10678,plain,
! [X0,X1,X2] :
( ~ prop(X1,X2)
| ~ state_adjective_state_binding(X2,X0)
| 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(X2,X0),X2)
| ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10676]) ).
fof(f10715,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( subs(X3,bezeichnen_1_1)
& subr(X4,rprs_0)
& sub(X5,X2)
& obj(X3,X1)
& mcont(X3,X4)
& hsit(X0,X3)
& arg2(X4,X5)
& arg1(X4,X1) )
| ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(pre_NNF_transformation,[status(thm)],[f162]) ).
fof(f10716,plain,
! [X0,X1,X2] :
( ? [X3] :
( subs(X3,bezeichnen_1_1)
& ? [X4] :
( subr(X4,rprs_0)
& ? [X5] :
( sub(X5,X2)
& obj(X3,X1)
& mcont(X3,X4)
& hsit(X0,X3)
& arg2(X4,X5)
& arg1(X4,X1) ) ) )
| ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(miniscoping,[status(thm)],[f10715]) ).
fof(f10717,plain,
! [X0,X1,X2] :
( ( subs(sK54_skl(X2,X1,X0),bezeichnen_1_1)
& subr(sK55_skl(X2,X1,X0),rprs_0)
& sub(sK56_skl(X2,X1,X0),X2)
& obj(sK54_skl(X2,X1,X0),X1)
& mcont(sK54_skl(X2,X1,X0),sK55_skl(X2,X1,X0))
& hsit(X0,sK54_skl(X2,X1,X0))
& arg2(sK55_skl(X2,X1,X0),sK56_skl(X2,X1,X0))
& arg1(sK55_skl(X2,X1,X0),X1) )
| ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54_skl,sK55_skl,sK56_skl]),skolemize(X3,sK54_skl(X2,X1,X0)),skolemize(X4,sK55_skl(X2,X1,X0)),skolemize(X5,sK56_skl(X2,X1,X0))],[f10716]) ).
fof(f10718,plain,
! [X0,X1,X2] :
( ~ arg1(X0,X2)
| arg1(sK55_skl(X1,X2,X0),X2)
| ~ arg2(X0,X1)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[status(thm)],[f10717]) ).
fof(f10719,plain,
! [X0,X1,X2] :
( ~ arg1(X2,X1)
| ~ arg2(X2,X0)
| ~ subr(X2,sub_0)
| arg2(sK55_skl(X0,X1,X2),sK56_skl(X0,X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f10717]) ).
fof(f10723,plain,
! [X0,X1,X2] :
( sub(sK56_skl(X2,X1,X0),X2)
| ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10717]) ).
fof(f10724,plain,
! [X0,X1,X2] :
( ~ subr(X0,sub_0)
| ~ arg1(X0,X2)
| subr(sK55_skl(X1,X2,X0),rprs_0)
| ~ arg2(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10717]) ).
fof(f10726,plain,
! [X0,X1] :
( ? [X2] :
( subr(X2,sub_0)
& arg2(X2,X1)
& arg1(X2,X0) )
| ~ sub(X0,X1) ),
inference(pre_NNF_transformation,[status(thm)],[f163]) ).
fof(f10727,plain,
! [X0,X1] :
( ( subr(sK57_skl(X1,X0),sub_0)
& arg2(sK57_skl(X1,X0),X1)
& arg1(sK57_skl(X1,X0),X0) )
| ~ sub(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK57_skl]),skolemize(X2,sK57_skl(X1,X0))],[f10726]) ).
fof(f10728,plain,
! [X0,X1] :
( ~ sub(X1,X0)
| arg1(sK57_skl(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f10727]) ).
fof(f10729,plain,
! [X0,X1] :
( arg2(sK57_skl(X1,X0),X1)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10727]) ).
fof(f10730,plain,
! [X0,X1] :
( subr(sK57_skl(X1,X0),sub_0)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10727]) ).
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] :
( ~ in(X9,X0)
| ~ val(X7,mandela_0)
| ~ arg2(X6,X2)
| ~ obj(X8,X4)
| ~ subr(X6,rprs_0)
| ~ sub(X7,familiename_1_1)
| ~ attr(X4,X7)
| ~ sub(X1,name_1_1)
| ~ sub(X5,eigenname_1_1)
| ~ arg1(X6,X4)
| ~ val(X5,nelson_0)
| ~ attr(X4,X5)
| ~ val(X1,s__374dafrika_0)
| ~ sub(X2,X3)
| ~ attr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f20816]) ).
fof(f20819,plain,
attr(c19,c20),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20820,plain,
attr(c19,c21),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20821,plain,
prop(c19,s__374dafrikanisch_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20823,plain,
sub(c19,pr__344sident_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20824,plain,
sub(c20,eigenname_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20825,plain,
val(c20,nelson_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20826,plain,
sub(c21,familiename_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20827,plain,
val(c21,mandela_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20832,plain,
obj(c3,c19),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f21139,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ in(X8,X0)
| ~ val(X6,mandela_0)
| ~ arg2(X5,X2)
| ~ obj(X7,X4)
| ~ subr(X5,rprs_0)
| ~ sub(X6,familiename_1_1)
| ~ attr(X4,X6)
| ~ sub(X1,name_1_1)
| ~ sub(c20,eigenname_1_1)
| ~ arg1(X5,X4)
| ~ attr(X4,c20)
| ~ val(X1,s__374dafrika_0)
| ~ sub(X2,X3)
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[f20825,f20817]) ).
fof(f21140,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ val(X5,mandela_0)
| ~ in(X8,X7)
| ~ sub(X6,name_1_1)
| ~ arg1(X4,X1)
| ~ attr(X1,X5)
| ~ subr(X4,rprs_0)
| ~ attr(X7,X6)
| ~ val(X6,s__374dafrika_0)
| ~ sub(X5,familiename_1_1)
| ~ arg2(X4,X2)
| ~ attr(X1,c20)
| ~ sub(X2,X3)
| ~ obj(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f21139,f20824]) ).
fof(f21146,plain,
! [X0,X1,X2,X3] :
( ~ sub(X1,X0)
| subr(sK55_skl(X2,X3,sK57_skl(X0,X1)),rprs_0)
| ~ arg1(sK57_skl(X0,X1),X3)
| ~ arg2(sK57_skl(X0,X1),X2) ),
inference(resolution,[status(thm)],[f10730,f10724]) ).
fof(f21147,plain,
! [X0,X1,X2] :
( ~ sub(X1,X0)
| ~ sub(X1,X0)
| subr(sK55_skl(X0,X2,sK57_skl(X0,X1)),rprs_0)
| ~ arg1(sK57_skl(X0,X1),X2) ),
inference(resolution,[status(thm)],[f21146,f10729]) ).
fof(f21148,plain,
! [X0,X1,X2] :
( ~ arg1(sK57_skl(X1,X0),X2)
| subr(sK55_skl(X1,X2,sK57_skl(X1,X0)),rprs_0)
| ~ sub(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f21147]) ).
fof(f21149,plain,
! [X0,X1] :
( ~ sub(X0,X1)
| subr(sK55_skl(X1,X0,sK57_skl(X1,X0)),rprs_0)
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[f21148,f10728]) ).
fof(f21150,plain,
! [X0,X1] :
( ~ sub(X1,X0)
| subr(sK55_skl(X0,X1,sK57_skl(X0,X1)),rprs_0) ),
inference(duplicate_literals_removal,[status(thm)],[f21149]) ).
fof(f21151,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ obj(X9,X3)
| ~ val(X5,s__374dafrika_0)
| ~ in(X8,X6)
| ~ sub(X4,X7)
| ~ sub(X2,X1)
| ~ attr(X6,X5)
| ~ sub(X0,familiename_1_1)
| ~ sub(X5,name_1_1)
| ~ attr(X3,X0)
| ~ attr(X3,c20)
| ~ arg2(sK55_skl(X1,X2,sK57_skl(X1,X2)),X4)
| ~ arg1(sK55_skl(X1,X2,sK57_skl(X1,X2)),X3)
| ~ val(X0,mandela_0) ),
inference(resolution,[status(thm)],[f21150,f21140]) ).
fof(f21219,plain,
! [X0] :
( val(sK47_skl(s__374dafrika_0,X0),s__374dafrika_0)
| ~ prop(X0,s__374dafrikanisch_1_1) ),
inference(resolution,[status(thm)],[f10682,f19788]) ).
fof(f21258,plain,
val(sK47_skl(s__374dafrika_0,c19),s__374dafrika_0),
inference(resolution,[status(thm)],[f20821,f21219]) ).
fof(f21270,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ sub(sK47_skl(s__374dafrika_0,c19),name_1_1)
| ~ attr(X7,c20)
| ~ sub(X3,X2)
| ~ obj(X8,X7)
| ~ arg1(sK55_skl(X2,X3,sK57_skl(X2,X3)),X7)
| ~ sub(X5,familiename_1_1)
| ~ attr(X7,X5)
| ~ attr(X1,sK47_skl(s__374dafrika_0,c19))
| ~ sub(X4,X6)
| ~ val(X5,mandela_0)
| ~ arg2(sK55_skl(X2,X3,sK57_skl(X2,X3)),X4)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f21258,f21151]) ).
fof(f21272,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ prop(c19,X8)
| ~ state_adjective_state_binding(X8,s__374dafrika_0)
| ~ sub(sK47_skl(s__374dafrika_0,c19),name_1_1)
| ~ attr(X6,c20)
| ~ sub(X2,X1)
| ~ obj(X7,X6)
| ~ arg1(sK55_skl(X1,X2,sK57_skl(X1,X2)),X6)
| ~ sub(X4,familiename_1_1)
| ~ attr(X6,X4)
| ~ sub(X3,X5)
| ~ val(X4,mandela_0)
| ~ arg2(sK55_skl(X1,X2,sK57_skl(X1,X2)),X3)
| ~ in(X0,sK48_skl(s__374dafrika_0,c19)) ),
inference(resolution,[status(thm)],[f21270,f10678]) ).
fof(f21274,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ attr(X5,c20)
| ~ obj(X8,X5)
| ~ sub(X4,X7)
| ~ in(X6,sK48_skl(s__374dafrika_0,c19))
| ~ arg1(sK55_skl(X2,X1,sK57_skl(X2,X1)),X5)
| ~ attr(X5,X3)
| ~ sub(X3,familiename_1_1)
| ~ arg2(sK55_skl(X2,X1,sK57_skl(X2,X1)),X4)
| ~ val(X3,mandela_0)
| ~ state_adjective_state_binding(X0,s__374dafrika_0)
| ~ sub(X1,X2)
| ~ prop(c19,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f21272,f10681]) ).
fof(f21275,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ attr(X4,c20)
| ~ obj(X7,X4)
| ~ sub(X3,X6)
| ~ in(X5,sK48_skl(s__374dafrika_0,c19))
| ~ arg1(sK55_skl(X1,X0,sK57_skl(X1,X0)),X4)
| ~ attr(X4,X2)
| ~ sub(X2,familiename_1_1)
| ~ arg2(sK55_skl(X1,X0,sK57_skl(X1,X0)),X3)
| ~ val(X2,mandela_0)
| ~ sub(X0,X1)
| ~ prop(c19,s__374dafrikanisch_1_1) ),
inference(resolution,[status(thm)],[f21274,f19788]) ).
fof(f21276,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ in(X7,sK48_skl(s__374dafrika_0,c19))
| ~ obj(X6,X2)
| ~ sub(X4,X3)
| ~ arg2(sK55_skl(X3,X4,sK57_skl(X3,X4)),X0)
| ~ sub(X5,familiename_1_1)
| ~ val(X5,mandela_0)
| ~ attr(X2,X5)
| ~ arg1(sK55_skl(X3,X4,sK57_skl(X3,X4)),X2)
| ~ attr(X2,c20)
| ~ sub(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f21275,f20821]) ).
fof(f21281,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ attr(c19,X3)
| ~ obj(X6,c19)
| ~ arg1(sK55_skl(X5,X4,sK57_skl(X5,X4)),c19)
| ~ arg2(sK55_skl(X5,X4,sK57_skl(X5,X4)),X0)
| ~ val(X3,mandela_0)
| ~ sub(X4,X5)
| ~ sub(X3,familiename_1_1)
| ~ in(X2,sK48_skl(s__374dafrika_0,c19))
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[f21276,f20819]) ).
fof(f21284,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ arg1(sK57_skl(X4,c19),c19)
| ~ arg2(sK57_skl(X4,c19),X4)
| ~ subr(sK57_skl(X4,c19),sub_0)
| ~ attr(c19,X3)
| ~ obj(X5,c19)
| ~ arg2(sK55_skl(X4,c19,sK57_skl(X4,c19)),X0)
| ~ val(X3,mandela_0)
| ~ sub(c19,X4)
| ~ sub(X3,familiename_1_1)
| ~ in(X2,sK48_skl(s__374dafrika_0,c19))
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[f21281,f10718]) ).
fof(f21285,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ obj(X5,c19)
| ~ attr(c19,X1)
| ~ arg1(sK57_skl(X0,c19),c19)
| ~ val(X1,mandela_0)
| ~ in(X4,sK48_skl(s__374dafrika_0,c19))
| ~ arg2(sK55_skl(X0,c19,sK57_skl(X0,c19)),X2)
| ~ arg2(sK57_skl(X0,c19),X0)
| ~ sub(X2,X3)
| ~ sub(X1,familiename_1_1)
| ~ sub(c19,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f21284,f10730]) ).
fof(f21286,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ attr(c19,X0)
| ~ arg2(sK55_skl(X3,c19,sK57_skl(X3,c19)),X1)
| ~ in(X5,sK48_skl(s__374dafrika_0,c19))
| ~ sub(c19,X3)
| ~ obj(X4,c19)
| ~ sub(X0,familiename_1_1)
| ~ arg1(sK57_skl(X3,c19),c19)
| ~ sub(X1,X2)
| ~ val(X0,mandela_0) ),
inference(forward_subsumption_resolution,[status(thm)],[f21285,f10729]) ).
fof(f21287,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sub(c19,X4)
| ~ attr(c19,X0)
| ~ arg2(sK55_skl(X4,c19,sK57_skl(X4,c19)),X1)
| ~ in(X5,sK48_skl(s__374dafrika_0,c19))
| ~ sub(c19,X4)
| ~ obj(X3,c19)
| ~ sub(X0,familiename_1_1)
| ~ sub(X1,X2)
| ~ val(X0,mandela_0) ),
inference(resolution,[status(thm)],[f21286,f10728]) ).
fof(f21288,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sub(c19,X0)
| ~ obj(X5,c19)
| ~ in(X4,sK48_skl(s__374dafrika_0,c19))
| ~ sub(X1,X3)
| ~ attr(c19,X2)
| ~ val(X2,mandela_0)
| ~ sub(X2,familiename_1_1)
| ~ arg2(sK55_skl(X0,c19,sK57_skl(X0,c19)),X1) ),
inference(duplicate_literals_removal,[status(thm)],[f21287]) ).
fof(f21296,plain,
! [X0,X1,X2,X3,X4] :
( ~ sub(c19,X0)
| ~ obj(X4,c19)
| ~ in(X3,sK48_skl(s__374dafrika_0,c19))
| ~ sub(X1,X2)
| ~ attr(c19,c21)
| ~ sub(c21,familiename_1_1)
| ~ arg2(sK55_skl(X0,c19,sK57_skl(X0,c19)),X1) ),
inference(resolution,[status(thm)],[f21288,f20827]) ).
fof(f21297,plain,
! [X0,X1,X2,X3,X4] :
( ~ in(X4,sK48_skl(s__374dafrika_0,c19))
| ~ arg2(sK55_skl(X2,c19,sK57_skl(X2,c19)),X0)
| ~ obj(X3,c19)
| ~ attr(c19,c21)
| ~ sub(c19,X2)
| ~ sub(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f21296,f20826]) ).
fof(f21301,plain,
! [X0,X1,X2,X3,X4] :
( ~ in(X4,sK48_skl(s__374dafrika_0,c19))
| ~ sub(X1,X3)
| ~ sub(c19,X0)
| ~ obj(X2,c19)
| ~ arg2(sK55_skl(X0,c19,sK57_skl(X0,c19)),X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f21297,f20820]) ).
fof(f21302,plain,
! [X0,X1,X2,X3] :
( ~ arg1(sK57_skl(X1,c19),c19)
| ~ arg2(sK57_skl(X1,c19),X1)
| ~ subr(sK57_skl(X1,c19),sub_0)
| ~ in(X3,sK48_skl(s__374dafrika_0,c19))
| ~ sub(sK56_skl(X1,c19,sK57_skl(X1,c19)),X2)
| ~ sub(c19,X1)
| ~ obj(X0,c19) ),
inference(resolution,[status(thm)],[f21301,f10719]) ).
fof(f21303,plain,
! [X0,X1,X2,X3] :
( ~ in(X3,sK48_skl(s__374dafrika_0,c19))
| ~ sub(c19,X0)
| ~ sub(sK56_skl(X0,c19,sK57_skl(X0,c19)),X2)
| ~ obj(X1,c19)
| ~ arg1(sK57_skl(X0,c19),c19)
| ~ arg2(sK57_skl(X0,c19),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f21302,f10730]) ).
fof(f21309,plain,
! [X0,X1,X2,X3] :
( ~ in(X3,sK48_skl(s__374dafrika_0,c19))
| ~ sub(c19,X0)
| ~ sub(sK56_skl(X0,c19,sK57_skl(X0,c19)),X2)
| ~ obj(X1,c19)
| ~ arg1(sK57_skl(X0,c19),c19) ),
inference(forward_subsumption_resolution,[status(thm)],[f21303,f10729]) ).
fof(f21310,plain,
! [X0,X1,X2,X3] :
( ~ sub(c19,X1)
| ~ in(X3,sK48_skl(s__374dafrika_0,c19))
| ~ sub(c19,X1)
| ~ sub(sK56_skl(X1,c19,sK57_skl(X1,c19)),X2)
| ~ obj(X0,c19) ),
inference(resolution,[status(thm)],[f21309,f10728]) ).
fof(f21311,plain,
! [X0,X1,X2,X3] :
( ~ in(X3,sK48_skl(s__374dafrika_0,c19))
| ~ obj(X2,c19)
| ~ sub(c19,X0)
| ~ sub(sK56_skl(X0,c19,sK57_skl(X0,c19)),X1) ),
inference(duplicate_literals_removal,[status(thm)],[f21310]) ).
fof(f21312,plain,
! [X0,X1,X2,X3] :
( ~ obj(X3,c19)
| ~ prop(c19,X2)
| ~ sub(c19,X0)
| ~ state_adjective_state_binding(X2,s__374dafrika_0)
| ~ sub(sK56_skl(X0,c19,sK57_skl(X0,c19)),X1) ),
inference(resolution,[status(thm)],[f21311,f10677]) ).
fof(f21315,plain,
! [X0,X1,X2] :
( ~ obj(X2,c19)
| ~ prop(c19,s__374dafrikanisch_1_1)
| ~ sub(c19,X0)
| ~ sub(sK56_skl(X0,c19,sK57_skl(X0,c19)),X1) ),
inference(resolution,[status(thm)],[f21312,f19788]) ).
fof(f21316,plain,
! [X0,X1,X2] :
( ~ obj(X2,c19)
| ~ sub(sK56_skl(X0,c19,sK57_skl(X0,c19)),X1)
| ~ sub(c19,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f21315,f20821]) ).
fof(f21322,plain,
! [X0,X1] :
( ~ obj(X1,c19)
| ~ sub(sK56_skl(pr__344sident_1_1,c19,sK57_skl(pr__344sident_1_1,c19)),X0) ),
inference(resolution,[status(thm)],[f21316,f20823]) ).
fof(f21329,plain,
! [X0] :
( ~ arg2(sK57_skl(pr__344sident_1_1,c19),pr__344sident_1_1)
| ~ obj(X0,c19)
| ~ arg1(sK57_skl(pr__344sident_1_1,c19),c19)
| ~ subr(sK57_skl(pr__344sident_1_1,c19),sub_0) ),
inference(resolution,[status(thm)],[f21322,f10723]) ).
fof(f21450,plain,
! [X0] :
( ~ sub(c19,pr__344sident_1_1)
| ~ obj(X0,c19)
| ~ arg1(sK57_skl(pr__344sident_1_1,c19),c19)
| ~ subr(sK57_skl(pr__344sident_1_1,c19),sub_0) ),
inference(resolution,[status(thm)],[f21329,f10729]) ).
fof(f21451,plain,
! [X0] :
( ~ obj(X0,c19)
| ~ sub(c19,pr__344sident_1_1)
| ~ arg1(sK57_skl(pr__344sident_1_1,c19),c19) ),
inference(forward_subsumption_resolution,[status(thm)],[f21450,f10730]) ).
fof(f21452,plain,
! [X0] :
( ~ sub(c19,pr__344sident_1_1)
| ~ obj(X0,c19) ),
inference(forward_subsumption_resolution,[status(thm)],[f21451,f10728]) ).
fof(f21453,plain,
! [X0] : ~ obj(X0,c19),
inference(resolution,[status(thm)],[f21452,f20823]) ).
fof(f21460,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f20832,f21453]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : CSR116+43 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.05/5.48 % Computer : n012.cluster.edu
% 0.05/5.48 % Model : x86_64 x86_64
% 0.05/5.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/5.48 % Memory : 8046.5625MB
% 0.05/5.48 % OS : Linux 6.8.0-71-generic
% 0.05/5.49 % CPULimit : 300
% 0.05/5.49 % WCLimit : 300
% 0.05/5.49 % DateTime : Mon Sep 21 15:09:36 UTC 2026
% 0.05/5.49 % CPUTime :
% 0.07/5.55 % Drodi V4.1.1
% 47.97/11.66 % Refutation found
% 47.97/11.66 % SZS status Theorem for theBenchmark: Theorem is valid
% 47.97/11.66 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 32.15/11.73 % Elapsed time: 6.236230 seconds
% 32.15/11.73 % CPU time: 48.833968 seconds
% 32.15/11.73 % Total memory used: 634.405 MB
% 32.15/11.73 % Net memory used: 604.563 MB
%------------------------------------------------------------------------------