%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR116+44 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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:15:33 PM UTC 2026
% Result : Theorem 131.53s 17.74s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR116+44 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.71 % Computer : n013.cluster.edu
% 0.18/0.71 % Model : x86_64 x86_64
% 0.18/0.71 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.71 % Memory : 8046.5625MB
% 0.18/0.71 % OS : Linux 6.8.0-71-generic
% 0.18/0.71 % CPULimit : 300
% 0.18/0.71 % WCLimit : 300
% 0.18/0.71 % DateTime : Mon Sep 21 15:09:07 UTC 2026
% 0.20/0.72 % CPUTime :
% 0.23/0.94 % Drodi V4.1.1
% 131.53/17.74 % Refutation found
% 131.53/17.74 % SZS status Theorem for theBenchmark: Theorem is valid
% 131.53/17.74 % SZS output start CNFRefutation for theBenchmark
% 131.53/17.74 fof(f10188,conjecture,(
% 131.53/17.74 (? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :( arg1(X3,X0)& arg2(X3,X4)& attr(X0,X1)& attr(X0,X2)& attr(X5,X6)& obj(X7,X0)& prop(X4,schwarz_1_1)& rslt(X7,X3)& sub(X1,familiename_1_1)& sub(X2,eigenname_1_1)& sub(X4,X8)& sub(X6,name_1_1)& subr(X3,rprs_0)& val(X1,mandela_0)& val(X2,nelson_0)& val(X6,s__374dafrika_0) ) )),
% 131.53/17.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.53/17.74 fof(f10189,negated_conjecture,(
% 131.53/17.74 ~((? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :( arg1(X3,X0)& arg2(X3,X4)& attr(X0,X1)& attr(X0,X2)& attr(X5,X6)& obj(X7,X0)& prop(X4,schwarz_1_1)& rslt(X7,X3)& sub(X1,familiename_1_1)& sub(X2,eigenname_1_1)& sub(X4,X8)& sub(X6,name_1_1)& subr(X3,rprs_0)& val(X1,mandela_0)& val(X2,nelson_0)& val(X6,s__374dafrika_0) ) ))),
% 131.53/17.74 inference(negated_conjecture,[status(cth)],[f10188])).
% 131.53/17.74 fof(f10190,hypothesis,(
% 131.53/17.74 ( sub(c16,montag__1_1)& prop(c23,schwarz_1_1)& sub(c23,c25)& pmod(c25,erst_1_1,staatpr__344sident_1_1)& obj(c27,c6)& rslt(c27,c42)& subs(c27,ernennen_1_2)& temp(c27,c16)& attch(c37,c23)& attr(c37,c38)& sub(c37,land_1_1)& sub(c38,name_1_1)& val(c38,s__374dafrika_0)& arg1(c42,c6)& arg2(c42,c23)& subr(c42,rprs_0)& attr(c6,c7)& attr(c6,c8)& sub(c6,mensch_1_1)& sub(c7,eigenname_1_1)& val(c7,nelson_0)& sub(c8,familiename_1_1)& val(c8,mandela_0)& assoc(staatpr__344sident_1_1,land_1_1)& sub(staatpr__344sident_1_1,pr__344sident_1_1)& sort(c16,ta)& card(c16,int1)& etype(c16,int0)& fact(c16,real)& gener(c16,sp)& quant(c16,one)& refer(c16,det)& varia(c16,con)& sort(montag__1_1,ta)& card(montag__1_1,int1)& etype(montag__1_1,int0)& fact(montag__1_1,real)& gener(montag__1_1,ge)& quant(montag__1_1,one)& refer(montag__1_1,refer_c)& varia(montag__1_1,varia_c)& sort(c23,d)& card(c23,int1)& etype(c23,int0)& fact(c23,real)& gener(c23,sp)& quant(c23,one)& refer(c23,det)& varia(c23,con)& sort(schwarz_1_1,tq)& sort(c25,d)& card(c25,int1)& etype(c25,int0)& fact(c25,real)& gener(c25,ge)& quant(c25,one)& refer(c25,refer_c)& varia(c25,varia_c)& sort(erst_1_1,oq)& card(erst_1_1,int1)& sort(staatpr__344sident_1_1,d)& card(staatpr__344sident_1_1,int1)& etype(staatpr__344sident_1_1,int0)& fact(staatpr__344sident_1_1,real)& gener(staatpr__344sident_1_1,ge)& quant(staatpr__344sident_1_1,one)& refer(staatpr__344sident_1_1,refer_c)& varia(staatpr__344sident_1_1,varia_c)& sort(c27,da)& fact(c27,real)& gener(c27,sp)& sort(c6,d)& card(c6,int1)& etype(c6,int0)& fact(c6,real)& gener(c6,sp)& quant(c6,one)& refer(c6,det)& varia(c6,con)& sort(c42,st)& fact(c42,real)& gener(c42,sp)& sort(ernennen_1_2,da)& fact(ernennen_1_2,real)& gener(ernennen_1_2,ge)& sort(c37,d)& sort(c37,io)& card(c37,int1)& etype(c37,int0)& fact(c37,real)& gener(c37,sp)& quant(c37,one)& refer(c37,det)& varia(c37,con)& sort(c38,na)& card(c38,int1)& etype(c38,int0)& fact(c38,real)& gener(c38,sp)& quant(c38,one)& refer(c38,indet)& varia(c38,varia_c)& sort(land_1_1,d)& sort(land_1_1,io)& card(land_1_1,int1)& etype(land_1_1,int0)& fact(land_1_1,real)& gener(land_1_1,ge)& quant(land_1_1,one)& refer(land_1_1,refer_c)& varia(land_1_1,varia_c)& sort(name_1_1,na)& card(name_1_1,int1)& etype(name_1_1,int0)& fact(name_1_1,real)& gener(name_1_1,ge)& quant(name_1_1,one)& refer(name_1_1,refer_c)& varia(name_1_1,varia_c)& sort(s__374dafrika_0,fe)& sort(rprs_0,st)& fact(rprs_0,real)& gener(rprs_0,gener_c)& sort(c7,na)& card(c7,int1)& etype(c7,int0)& fact(c7,real)& gener(c7,sp)& quant(c7,one)& refer(c7,indet)& varia(c7,varia_c)& sort(c8,na)& card(c8,int1)& etype(c8,int0)& fact(c8,real)& gener(c8,sp)& quant(c8,one)& refer(c8,indet)& varia(c8,varia_c)& sort(mensch_1_1,d)& card(mensch_1_1,int1)& etype(mensch_1_1,int0)& fact(mensch_1_1,real)& gener(mensch_1_1,ge)& quant(mensch_1_1,one)& refer(mensch_1_1,refer_c)& varia(mensch_1_1,varia_c)& sort(eigenname_1_1,na)& card(eigenname_1_1,int1)& etype(eigenname_1_1,int0)& fact(eigenname_1_1,real)& gener(eigenname_1_1,ge)& quant(eigenname_1_1,one)& refer(eigenname_1_1,refer_c)& varia(eigenname_1_1,varia_c)& sort(nelson_0,fe)& sort(familiename_1_1,na)& card(familiename_1_1,int1)& etype(familiename_1_1,int0)& fact(familiename_1_1,real)& gener(familiename_1_1,ge)& quant(familiename_1_1,one)& refer(familiename_1_1,refer_c)& varia(familiename_1_1,varia_c)& sort(mandela_0,fe)& sort(pr__344sident_1_1,d)& card(pr__344sident_1_1,int1)& etype(pr__344sident_1_1,int0)& fact(pr__344sident_1_1,real)& gener(pr__344sident_1_1,ge)& quant(pr__344sident_1_1,one)& refer(pr__344sident_1_1,refer_c)& varia(pr__344sident_1_1,varia_c) ) ),
% 131.53/17.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.53/17.74 fof(f20815,plain,(
% 131.53/17.74 (![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (((((((((((((((~arg1(X3,X0)|~arg2(X3,X4))|~attr(X0,X1))|~attr(X0,X2))|~attr(X5,X6))|~obj(X7,X0))|~prop(X4,schwarz_1_1))|~rslt(X7,X3))|~sub(X1,familiename_1_1))|~sub(X2,eigenname_1_1))|~sub(X4,X8))|~sub(X6,name_1_1))|~subr(X3,rprs_0))|~val(X1,mandela_0))|~val(X2,nelson_0))|~val(X6,s__374dafrika_0)))),
% 131.53/17.74 inference(pre_NNF_transformation,[status(thm)],[f10189])).
% 131.53/17.74 fof(f20816,plain,(
% 131.53/17.74 ![X6]: ((![X2]: ((![X1]: ((![X3]: (((![X4]: ((((![X7]: (((![X0]: (((((~arg1(X3,X0)|~arg2(X3,X4))|~attr(X0,X1))|~attr(X0,X2))|(![X5]: ~attr(X5,X6)))|~obj(X7,X0)))|~prop(X4,schwarz_1_1))|~rslt(X7,X3)))|~sub(X1,familiename_1_1))|~sub(X2,eigenname_1_1))|(![X8]: ~sub(X4,X8))))|~sub(X6,name_1_1))|~subr(X3,rprs_0)))|~val(X1,mandela_0)))|~val(X2,nelson_0)))|~val(X6,s__374dafrika_0))),
% 131.53/17.74 inference(miniscoping,[status(thm)],[f20815])).
% 131.53/17.74 fof(f20817,plain,(
% 131.53/17.74 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~arg1(X0,X1)|~arg2(X0,X2)|~attr(X1,X3)|~attr(X1,X4)|~attr(X5,X6)|~obj(X7,X1)|~prop(X2,schwarz_1_1)|~rslt(X7,X0)|~sub(X3,familiename_1_1)|~sub(X4,eigenname_1_1)|~sub(X2,X8)|~sub(X6,name_1_1)|~subr(X0,rprs_0)|~val(X3,mandela_0)|~val(X4,nelson_0)|~val(X6,s__374dafrika_0))),
% 131.53/17.74 inference(cnf_transformation,[status(thm)],[f20816])).
% 131.53/17.74 fof(f20819,plain,(
% 131.53/17.74 prop(c23,schwarz_1_1)),
% 131.53/17.74 inference(cnf_transformation,[status(thm)],[f10190])).
% 131.53/17.74 fof(f20820,plain,(
% 131.53/17.74 sub(c23,c25)),
% 131.53/17.74 inference(cnf_transformation,[status(thm)],[f10190])).
% 131.53/17.74 fof(f20822,plain,(
% 131.53/17.74 obj(c27,c6)),
% 131.53/17.74 inference(cnf_transformation,[status(thm)],[f10190])).
% 131.53/17.74 fof(f20823,plain,(
% 131.53/17.74 rslt(c27,c42)),
% 131.53/17.74 inference(cnf_transformation,[status(thm)],[f10190])).
% 131.53/17.74 fof(f20827,plain,(
% 131.53/17.74 attr(c37,c38)),
% 131.53/17.74 inference(cnf_transformation,[status(thm)],[f10190])).
% 131.53/17.74 fof(f20829,plain,(
% 131.53/17.74 sub(c38,name_1_1)),
% 131.53/17.74 inference(cnf_transformation,[status(thm)],[f10190])).
% 131.53/17.74 fof(f20830,plain,(
% 131.53/17.74 val(c38,s__374dafrika_0)),
% 131.53/17.74 inference(cnf_transformation,[status(thm)],[f10190])).
% 131.53/17.74 fof(f20831,plain,(
% 131.53/17.74 arg1(c42,c6)),
% 131.53/17.74 inference(cnf_transformation,[status(thm)],[f10190])).
% 131.53/17.74 fof(f20832,plain,(
% 131.53/17.74 arg2(c42,c23)),
% 131.53/17.74 inference(cnf_transformation,[status(thm)],[f10190])).
% 131.53/17.74 fof(f20833,plain,(
% 131.53/17.74 subr(c42,rprs_0)),
% 131.53/17.74 inference(cnf_transformation,[status(thm)],[f10190])).
% 131.53/17.74 fof(f20834,plain,(
% 131.53/17.74 attr(c6,c7)),
% 131.53/17.74 inference(cnf_transformation,[status(thm)],[f10190])).
% 131.53/17.74 fof(f20835,plain,(
% 131.53/17.74 attr(c6,c8)),
% 131.53/17.74 inference(cnf_transformation,[status(thm)],[f10190])).
% 131.53/17.74 fof(f20837,plain,(
% 131.53/17.74 sub(c7,eigenname_1_1)),
% 131.53/17.74 inference(cnf_transformation,[status(thm)],[f10190])).
% 131.53/17.74 fof(f20838,plain,(
% 131.53/17.74 val(c7,nelson_0)),
% 131.53/17.74 inference(cnf_transformation,[status(thm)],[f10190])).
% 131.53/17.74 fof(f20839,plain,(
% 131.53/17.74 sub(c8,familiename_1_1)),
% 131.53/17.74 inference(cnf_transformation,[status(thm)],[f10190])).
% 131.53/17.74 fof(f20840,plain,(
% 131.53/17.74 val(c8,mandela_0)),
% 131.53/17.74 inference(cnf_transformation,[status(thm)],[f10190])).
% 131.53/17.74 fof(f21028,plain,(
% 131.53/17.74 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~arg1(X0,X1)|~arg2(X0,X2)|~attr(X1,X3)|~attr(X1,X4)|~attr(X5,c38)|~obj(X6,X1)|~prop(X2,schwarz_1_1)|~rslt(X6,X0)|~sub(X3,familiename_1_1)|~sub(X4,eigenname_1_1)|~sub(X2,X7)|~sub(c38,name_1_1)|~subr(X0,rprs_0)|~val(X3,mandela_0)|~val(X4,nelson_0))),
% 131.53/17.74 inference(resolution,[status(thm)],[f20830,f20817])).
% 131.53/17.74 fof(f21045,plain,(
% 131.53/17.74 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~arg1(X0,X1)|~arg2(X0,X2)|~attr(X1,X3)|~attr(X1,X4)|~attr(X5,c38)|~obj(X6,X1)|~prop(X2,schwarz_1_1)|~rslt(X6,X0)|~sub(X3,familiename_1_1)|~sub(X4,eigenname_1_1)|~sub(X2,X7)|~subr(X0,rprs_0)|~val(X3,mandela_0)|~val(X4,nelson_0))),
% 131.53/17.74 inference(forward_subsumption_resolution,[status(thm)],[f21028,f20829])).
% 131.53/17.74 fof(f21048,plain,(
% 131.53/17.74 ![X0,X1,X2,X3,X4,X5,X6]: (~arg1(X0,X1)|~arg2(X0,X2)|~attr(X1,X3)|~attr(X1,c7)|~attr(X4,c38)|~obj(X5,X1)|~prop(X2,schwarz_1_1)|~rslt(X5,X0)|~sub(X3,familiename_1_1)|~sub(c7,eigenname_1_1)|~sub(X2,X6)|~subr(X0,rprs_0)|~val(X3,mandela_0))),
% 131.53/17.90 inference(resolution,[status(thm)],[f21045,f20838])).
% 131.53/17.90 fof(f21050,plain,(
% 131.53/17.90 ![X0,X1,X2,X3,X4,X5,X6]: (~arg1(X0,X1)|~arg2(X0,X2)|~attr(X1,X3)|~attr(X1,c7)|~attr(X4,c38)|~obj(X5,X1)|~prop(X2,schwarz_1_1)|~rslt(X5,X0)|~sub(X3,familiename_1_1)|~sub(X2,X6)|~subr(X0,rprs_0)|~val(X3,mandela_0))),
% 131.53/17.90 inference(forward_subsumption_resolution,[status(thm)],[f21048,f20837])).
% 131.53/17.90 fof(f21055,plain,(
% 131.53/17.90 ![X0,X1,X2,X3,X4,X5]: (~arg1(X0,X1)|~arg2(X0,X2)|~attr(X1,c8)|~attr(X1,c7)|~attr(X3,c38)|~obj(X4,X1)|~prop(X2,schwarz_1_1)|~rslt(X4,X0)|~sub(c8,familiename_1_1)|~sub(X2,X5)|~subr(X0,rprs_0))),
% 131.53/17.90 inference(resolution,[status(thm)],[f21050,f20840])).
% 131.53/17.90 fof(f21057,plain,(
% 131.53/17.90 ![X0,X1,X2,X3,X4,X5]: (~arg1(X0,X1)|~arg2(X0,X2)|~attr(X1,c8)|~attr(X1,c7)|~attr(X3,c38)|~obj(X4,X1)|~prop(X2,schwarz_1_1)|~rslt(X4,X0)|~sub(X2,X5)|~subr(X0,rprs_0))),
% 131.53/17.90 inference(forward_subsumption_resolution,[status(thm)],[f21055,f20839])).
% 131.53/17.90 fof(f21058,plain,(
% 131.53/17.90 ![X0,X1,X2,X3,X4]: (~arg1(c42,X0)|~arg2(c42,X1)|~attr(X0,c8)|~attr(X0,c7)|~attr(X2,c38)|~obj(X3,X0)|~prop(X1,schwarz_1_1)|~rslt(X3,c42)|~sub(X1,X4))),
% 131.53/17.90 inference(resolution,[status(thm)],[f21057,f20833])).
% 131.53/17.90 fof(f26248,plain,(
% 131.53/17.90 ![X0,X1,X2,X3]: (~arg1(c42,X0)|~arg2(c42,X1)|~attr(X0,c8)|~attr(X0,c7)|~attr(X2,c38)|~obj(c27,X0)|~prop(X1,schwarz_1_1)|~sub(X1,X3))),
% 131.53/17.90 inference(resolution,[status(thm)],[f20823,f21058])).
% 131.53/17.90 fof(f26391,plain,(
% 131.53/17.90 ![X0,X1,X2]: (~arg1(c42,X0)|~arg2(c42,X1)|~attr(X0,c8)|~attr(X0,c7)|~obj(c27,X0)|~prop(X1,schwarz_1_1)|~sub(X1,X2))),
% 131.53/17.90 inference(resolution,[status(thm)],[f20827,f26248])).
% 131.53/17.90 fof(f26535,plain,(
% 131.53/17.90 ![X0,X1]: (~arg1(c42,X0)|~attr(X0,c8)|~attr(X0,c7)|~obj(c27,X0)|~prop(c23,schwarz_1_1)|~sub(c23,X1))),
% 131.53/17.90 inference(resolution,[status(thm)],[f20832,f26391])).
% 131.53/17.90 fof(f26568,plain,(
% 131.53/17.90 ![X0,X1]: (~arg1(c42,X0)|~attr(X0,c8)|~attr(X0,c7)|~obj(c27,X0)|~sub(c23,X1))),
% 131.53/17.90 inference(forward_subsumption_resolution,[status(thm)],[f26535,f20819])).
% 131.53/17.90 fof(f26625,plain,(
% 131.53/17.90 ![X0]: (~arg1(c42,c6)|~attr(c6,c8)|~obj(c27,c6)|~sub(c23,X0))),
% 131.53/17.90 inference(resolution,[status(thm)],[f20834,f26568])).
% 131.53/17.90 fof(f26697,plain,(
% 131.53/17.90 ![X0]: (~attr(c6,c8)|~obj(c27,c6)|~sub(c23,X0))),
% 131.53/17.90 inference(forward_subsumption_resolution,[status(thm)],[f26625,f20831])).
% 131.53/17.90 fof(f26866,plain,(
% 131.53/17.90 ![X0]: (~obj(c27,c6)|~sub(c23,X0))),
% 131.53/17.90 inference(forward_subsumption_resolution,[status(thm)],[f26697,f20835])).
% 131.53/17.90 fof(f26867,plain,(
% 131.53/17.90 ![X0]: (~sub(c23,X0))),
% 131.53/17.90 inference(resolution,[status(thm)],[f26866,f20822])).
% 131.53/17.90 fof(f26869,plain,(
% 131.53/17.90 $false),
% 131.53/17.90 inference(backward_subsumption_resolution,[status(thm)],[f20820,f26867])).
% 131.53/17.90 % SZS output end CNFRefutation for theBenchmark.p
% 131.53/17.95 % Elapsed time: 17.210682 seconds
% 131.53/17.95 % CPU time: 133.733244 seconds
% 131.53/17.95 % Total memory used: 702.787 MB
% 131.53/17.95 % Net memory used: 682.461 MB
%------------------------------------------------------------------------------