%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR116+5 : 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 : n003.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 115.47s 15.15s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR116+5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n003.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 15:11:46 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.14/0.48 % Drodi V4.1.1
% 115.47/15.15 % Refutation found
% 115.47/15.15 % SZS status Theorem for theBenchmark: Theorem is valid
% 115.47/15.15 % SZS output start CNFRefutation for theBenchmark
% 115.47/15.15 fof(f158,axiom,(
% 115.47/15.15 (! [X0,X1,X2,X3] :( ( tupl(X1,X2,X3)& sub(X0,eigenname_1_1)& val(X0,X1) )=> val(X0,X2) ) )),
% 115.47/15.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 115.47/15.15 fof(f10188,conjecture,(
% 115.47/15.15 (? [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)& 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) ) )),
% 115.47/15.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 115.47/15.15 fof(f10189,negated_conjecture,(
% 115.47/15.15 ~((? [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)& 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) ) ))),
% 115.47/15.15 inference(negated_conjecture,[status(cth)],[f10188])).
% 115.47/15.15 fof(f10190,hypothesis,(
% 115.47/15.15 ( agt(c15,c3)& obj(c15,c345)& rslt(c15,c394)& subs(c15,erkl__344ren_1_4)& attr(c345,c346)& attr(c345,c348)& sub(c345,mensch_1_1)& sub(c346,eigenname_1_1)& val(c346,c347)& tupl(c347,nelson_0,rolihlahla_0)& sub(c348,familiename_1_1)& val(c348,mandela_0)& prop(c381,c382)& sub(c381,pr__344sident_1_1)& modp(c382,amtlich_1_1,c1)& attch(c391,c381)& attr(c391,c392)& sub(c391,republik__1_1)& sub(c392,name_1_1)& val(c392,s__374dafrika_0)& arg1(c394,c345)& arg2(c394,c381)& subr(c394,rprs_0)& sub(republik__1_1,land_1_1)& chsp2(w__344hlen_1_2,c1)& sort(c15,da)& fact(c15,real)& gener(c15,sp)& sort(c3,d)& card(c3,int1)& etype(c3,int0)& fact(c3,real)& gener(c3,sp)& quant(c3,one)& refer(c3,det)& varia(c3,varia_c)& sort(c345,d)& card(c345,int1)& etype(c345,int0)& fact(c345,real)& gener(c345,sp)& quant(c345,one)& refer(c345,det)& varia(c345,con)& sort(c394,st)& fact(c394,real)& gener(c394,sp)& sort(erkl__344ren_1_4,da)& fact(erkl__344ren_1_4,real)& gener(erkl__344ren_1_4,ge)& sort(c346,na)& card(c346,int1)& etype(c346,int0)& fact(c346,real)& gener(c346,sp)& quant(c346,one)& refer(c346,indet)& varia(c346,varia_c)& sort(c348,na)& card(c348,int1)& etype(c348,int0)& fact(c348,real)& gener(c348,sp)& quant(c348,one)& refer(c348,indet)& varia(c348,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(c347,fe)& sort(nelson_0,fe)& sort(rolihlahla_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(c381,d)& card(c381,int1)& etype(c381,int0)& fact(c381,real)& gener(c381,sp)& quant(c381,one)& refer(c381,det)& varia(c381,con)& sort(c382,tq)& 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)& sort(amtlich_1_1,tq)& sort(c1,tq)& sort(c391,d)& sort(c391,io)& card(c391,int1)& etype(c391,int0)& fact(c391,real)& gener(c391,sp)& quant(c391,one)& refer(c391,det)& varia(c391,con)& sort(c392,na)& card(c392,int1)& etype(c392,int0)& fact(c392,real)& gener(c392,sp)& quant(c392,one)& refer(c392,indet)& varia(c392,varia_c)& sort(republik__1_1,d)& sort(republik__1_1,io)& card(republik__1_1,int1)& etype(republik__1_1,int0)& fact(republik__1_1,real)& gener(republik__1_1,ge)& quant(republik__1_1,one)& refer(republik__1_1,refer_c)& varia(republik__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(land_1_1,ent)& card(land_1_1,card_c)& etype(land_1_1,etype_c)& fact(land_1_1,real)& gener(land_1_1,gener_c)& quant(land_1_1,quant_c)& refer(land_1_1,refer_c)& varia(land_1_1,varia_c)& sort(w__344hlen_1_2,da)& fact(w__344hlen_1_2,real)& gener(w__344hlen_1_2,ge) ) ),
% 115.47/15.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 115.47/15.16 fof(f10689,plain,(
% 115.47/15.16 ![X0,X1,X2,X3]: (((~tupl(X1,X2,X3)|~sub(X0,eigenname_1_1))|~val(X0,X1))|val(X0,X2))),
% 115.47/15.16 inference(pre_NNF_transformation,[status(thm)],[f158])).
% 115.47/15.16 fof(f10690,plain,(
% 115.47/15.16 ![X0,X2]: ((![X1]: (((![X3]: ~tupl(X1,X2,X3))|~sub(X0,eigenname_1_1))|~val(X0,X1)))|val(X0,X2))),
% 115.47/15.16 inference(miniscoping,[status(thm)],[f10689])).
% 115.47/15.16 fof(f10691,plain,(
% 115.47/15.16 ![X0,X1,X2,X3]: (~tupl(X0,X1,X2)|~sub(X3,eigenname_1_1)|~val(X3,X0)|val(X3,X1))),
% 115.47/15.16 inference(cnf_transformation,[status(thm)],[f10690])).
% 115.47/15.16 fof(f20815,plain,(
% 115.47/15.16 (![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))|~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)))),
% 115.47/15.16 inference(pre_NNF_transformation,[status(thm)],[f10189])).
% 115.47/15.16 fof(f20816,plain,(
% 115.47/15.16 ![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)))|~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))),
% 115.47/15.16 inference(miniscoping,[status(thm)],[f20815])).
% 115.47/15.16 fof(f20817,plain,(
% 115.47/15.16 ![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)|~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))),
% 115.47/15.16 inference(cnf_transformation,[status(thm)],[f20816])).
% 115.47/15.16 fof(f20819,plain,(
% 115.47/15.16 obj(c15,c345)),
% 115.47/15.16 inference(cnf_transformation,[status(thm)],[f10190])).
% 115.47/15.16 fof(f20820,plain,(
% 115.47/15.16 rslt(c15,c394)),
% 115.47/15.16 inference(cnf_transformation,[status(thm)],[f10190])).
% 115.47/15.16 fof(f20822,plain,(
% 115.47/15.16 attr(c345,c346)),
% 115.47/15.16 inference(cnf_transformation,[status(thm)],[f10190])).
% 115.47/15.16 fof(f20823,plain,(
% 115.47/15.16 attr(c345,c348)),
% 115.47/15.16 inference(cnf_transformation,[status(thm)],[f10190])).
% 115.47/15.16 fof(f20825,plain,(
% 115.47/15.16 sub(c346,eigenname_1_1)),
% 115.47/15.16 inference(cnf_transformation,[status(thm)],[f10190])).
% 115.47/15.16 fof(f20826,plain,(
% 115.47/15.16 val(c346,c347)),
% 115.47/15.16 inference(cnf_transformation,[status(thm)],[f10190])).
% 115.47/15.16 fof(f20827,plain,(
% 115.47/15.16 tupl(c347,nelson_0,rolihlahla_0)),
% 115.47/15.16 inference(cnf_transformation,[status(thm)],[f10190])).
% 115.47/15.16 fof(f20828,plain,(
% 115.47/15.16 sub(c348,familiename_1_1)),
% 115.47/15.16 inference(cnf_transformation,[status(thm)],[f10190])).
% 115.47/15.16 fof(f20829,plain,(
% 115.47/15.16 val(c348,mandela_0)),
% 115.47/15.16 inference(cnf_transformation,[status(thm)],[f10190])).
% 115.47/15.16 fof(f20831,plain,(
% 115.47/15.16 sub(c381,pr__344sident_1_1)),
% 115.47/15.16 inference(cnf_transformation,[status(thm)],[f10190])).
% 115.47/15.16 fof(f20834,plain,(
% 115.47/15.16 attr(c391,c392)),
% 115.47/15.16 inference(cnf_transformation,[status(thm)],[f10190])).
% 115.47/15.16 fof(f20836,plain,(
% 115.47/15.16 sub(c392,name_1_1)),
% 115.47/15.16 inference(cnf_transformation,[status(thm)],[f10190])).
% 115.47/15.16 fof(f20837,plain,(
% 115.47/15.16 val(c392,s__374dafrika_0)),
% 115.47/15.16 inference(cnf_transformation,[status(thm)],[f10190])).
% 115.47/15.16 fof(f20838,plain,(
% 115.47/15.16 arg1(c394,c345)),
% 115.47/15.16 inference(cnf_transformation,[status(thm)],[f10190])).
% 115.47/15.16 fof(f20839,plain,(
% 115.47/15.16 arg2(c394,c381)),
% 115.47/15.16 inference(cnf_transformation,[status(thm)],[f10190])).
% 115.47/15.16 fof(f20840,plain,(
% 115.47/15.16 subr(c394,rprs_0)),
% 115.47/15.16 inference(cnf_transformation,[status(thm)],[f10190])).
% 115.47/15.16 fof(f21017,plain,(
% 115.47/15.16 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~arg1(X0,X1)|~arg2(X0,X2)|~attr(X1,c348)|~attr(X1,X3)|~attr(X4,X5)|~obj(X6,X1)|~rslt(X6,X0)|~sub(c348,familiename_1_1)|~sub(X3,eigenname_1_1)|~sub(X2,X7)|~sub(X5,name_1_1)|~subr(X0,rprs_0)|~val(X3,nelson_0)|~val(X5,s__374dafrika_0))),
% 115.47/15.16 inference(resolution,[status(thm)],[f20829,f20817])).
% 86.87/15.29 fof(f21028,plain,(
% 86.87/15.29 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~arg1(X0,X1)|~arg2(X0,X2)|~attr(X1,c348)|~attr(X1,X3)|~attr(X4,X5)|~obj(X6,X1)|~rslt(X6,X0)|~sub(X3,eigenname_1_1)|~sub(X2,X7)|~sub(X5,name_1_1)|~subr(X0,rprs_0)|~val(X3,nelson_0)|~val(X5,s__374dafrika_0))),
% 86.87/15.29 inference(forward_subsumption_resolution,[status(thm)],[f21017,f20828])).
% 86.87/15.29 fof(f21029,plain,(
% 86.87/15.29 ![X0,X1,X2,X3,X4,X5,X6]: (~arg1(X0,X1)|~arg2(X0,X2)|~attr(X1,c348)|~attr(X1,X3)|~attr(X4,c392)|~obj(X5,X1)|~rslt(X5,X0)|~sub(X3,eigenname_1_1)|~sub(X2,X6)|~sub(c392,name_1_1)|~subr(X0,rprs_0)|~val(X3,nelson_0))),
% 86.87/15.29 inference(resolution,[status(thm)],[f21028,f20837])).
% 86.87/15.29 fof(f21031,plain,(
% 86.87/15.29 ![X0,X1,X2,X3,X4,X5,X6]: (~arg1(X0,X1)|~arg2(X0,X2)|~attr(X1,c348)|~attr(X1,X3)|~attr(X4,c392)|~obj(X5,X1)|~rslt(X5,X0)|~sub(X3,eigenname_1_1)|~sub(X2,X6)|~subr(X0,rprs_0)|~val(X3,nelson_0))),
% 86.87/15.29 inference(forward_subsumption_resolution,[status(thm)],[f21029,f20836])).
% 86.87/15.29 fof(f21039,plain,(
% 86.87/15.29 ![X0,X1,X2,X3,X4,X5]: (~arg1(c394,X0)|~arg2(c394,X1)|~attr(X0,c348)|~attr(X0,X2)|~attr(X3,c392)|~obj(X4,X0)|~rslt(X4,c394)|~sub(X2,eigenname_1_1)|~sub(X1,X5)|~val(X2,nelson_0))),
% 86.87/15.29 inference(resolution,[status(thm)],[f21031,f20840])).
% 86.87/15.29 fof(f21205,plain,(
% 86.87/15.29 ![X0]: (~sub(X0,eigenname_1_1)|~val(X0,c347)|val(X0,nelson_0))),
% 86.87/15.29 inference(resolution,[status(thm)],[f10691,f20827])).
% 86.87/15.29 fof(f26157,plain,(
% 86.87/15.29 ![X0,X1,X2,X3]: (~arg1(c394,c345)|~arg2(c394,X0)|~attr(c345,c348)|~attr(X1,c392)|~obj(X2,c345)|~rslt(X2,c394)|~sub(c346,eigenname_1_1)|~sub(X0,X3)|~val(c346,nelson_0))),
% 86.87/15.29 inference(resolution,[status(thm)],[f20822,f21039])).
% 86.87/15.29 fof(f26189,plain,(
% 86.87/15.29 ![X0,X1,X2,X3]: (~arg1(c394,c345)|~arg2(c394,X0)|~attr(c345,c348)|~attr(X1,c392)|~obj(X2,c345)|~rslt(X2,c394)|~sub(X0,X3)|~val(c346,nelson_0))),
% 86.87/15.29 inference(forward_subsumption_resolution,[status(thm)],[f26157,f20825])).
% 86.87/15.29 fof(f26303,plain,(
% 86.87/15.29 ~sub(c346,eigenname_1_1)|val(c346,nelson_0)),
% 86.87/15.29 inference(resolution,[status(thm)],[f20826,f21205])).
% 86.87/15.29 fof(f26307,plain,(
% 86.87/15.29 val(c346,nelson_0)),
% 86.87/15.29 inference(forward_subsumption_resolution,[status(thm)],[f26303,f20825])).
% 86.87/15.29 fof(f26316,plain,(
% 86.87/15.29 ![X0,X1,X2,X3]: (~arg1(c394,c345)|~arg2(c394,X0)|~attr(X1,c392)|~obj(X2,c345)|~rslt(X2,c394)|~sub(X0,X3)|~val(c346,nelson_0))),
% 86.87/15.29 inference(forward_subsumption_resolution,[status(thm)],[f26189,f20823])).
% 86.87/15.29 fof(f26317,plain,(
% 86.87/15.29 ![X0,X1,X2]: (~arg1(c394,c345)|~arg2(c394,X0)|~attr(X1,c392)|~obj(c15,c345)|~sub(X0,X2)|~val(c346,nelson_0))),
% 86.87/15.29 inference(resolution,[status(thm)],[f26316,f20820])).
% 86.87/15.29 fof(f26320,plain,(
% 86.87/15.29 ![X0,X1,X2]: (~arg1(c394,c345)|~arg2(c394,X0)|~attr(X1,c392)|~sub(X0,X2)|~val(c346,nelson_0))),
% 86.87/15.29 inference(forward_subsumption_resolution,[status(thm)],[f26317,f20819])).
% 86.87/15.29 fof(f26393,plain,(
% 86.87/15.29 ![X0,X1,X2]: (~arg1(c394,c345)|~arg2(c394,X0)|~attr(X1,c392)|~sub(X0,X2))),
% 86.87/15.29 inference(forward_subsumption_resolution,[status(thm)],[f26320,f26307])).
% 86.87/15.29 fof(f26515,plain,(
% 86.87/15.29 ![X0,X1,X2]: (~arg2(c394,X0)|~attr(X1,c392)|~sub(X0,X2))),
% 86.87/15.29 inference(backward_subsumption_resolution,[status(thm)],[f26393,f20838])).
% 86.87/15.29 fof(f26531,plain,(
% 86.87/15.29 ![X0,X1]: (~arg2(c394,X0)|~sub(X0,X1))),
% 86.87/15.29 inference(resolution,[status(thm)],[f26515,f20834])).
% 86.87/15.29 fof(f26548,plain,(
% 86.87/15.29 ![X0]: (~sub(c381,X0))),
% 86.87/15.29 inference(resolution,[status(thm)],[f20839,f26531])).
% 86.87/15.29 fof(f26576,plain,(
% 86.87/15.29 $false),
% 86.87/15.29 inference(backward_subsumption_resolution,[status(thm)],[f20831,f26548])).
% 86.87/15.29 % SZS output end CNFRefutation for theBenchmark.p
% 30.77/15.37 % Elapsed time: 15.006730 seconds
% 30.77/15.37 % CPU time: 116.399042 seconds
% 30.77/15.37 % Total memory used: 646.383 MB
% 30.77/15.37 % Net memory used: 631.147 MB
%------------------------------------------------------------------------------