%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR116+42 : 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 : n001.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 72.34s 9.89s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR116+42 : 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.19/0.48 % Computer : n001.cluster.edu
% 0.19/0.48 % Model : x86_64 x86_64
% 0.19/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.48 % Memory : 8046.5625MB
% 0.19/0.48 % OS : Linux 6.8.0-71-generic
% 0.19/0.48 % CPULimit : 300
% 0.19/0.48 % WCLimit : 300
% 0.19/0.48 % DateTime : Mon Sep 21 15:15:15 UTC 2026
% 0.19/0.49 % CPUTime :
% 0.33/0.71 % Drodi V4.1.1
% 72.34/9.89 % Refutation found
% 72.34/9.89 % SZS status Theorem for theBenchmark: Theorem is valid
% 72.34/9.89 % SZS output start CNFRefutation for theBenchmark
% 72.34/9.89 fof(f1,axiom,(
% 72.34/9.89 (! [X0,X1] : member(X0,cons(X0,X1)) )),
% 72.34/9.89 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.34/9.89 fof(f159,axiom,(
% 72.34/9.89 (! [X0,X1,X2] :( ( attr(X2,X0)& member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))& sub(X0,X1) )=> (? [X3] :( arg1(X3,X2)& arg2(X3,X2)& subs(X3,hei__337en_1_1) ) )) )),
% 72.34/9.89 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.34/9.89 fof(f160,axiom,(
% 72.34/9.89 (! [X0,X1,X2] :( ( attr(X2,X0)& member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))& sub(X0,X1) )=> (? [X3] :( mcont(X3,X2)& obj(X3,X2)& scar(X3,X2)& subs(X3,stehen_1_b) ) )) )),
% 72.34/9.89 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.34/9.89 fof(f161,axiom,(
% 72.34/9.89 (! [X0,X1,X2] :( ( arg1(X0,X1)& arg2(X0,X2)& subs(X0,hei__337en_1_1) )=> (? [X3,X4] :( arg1(X4,X1)& arg2(X4,X2)& hsit(X0,X3)& mcont(X3,X4)& obj(X3,X1)& subr(X4,rprs_0)& subs(X3,bezeichnen_1_1) ) )) )),
% 72.34/9.89 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.34/9.89 fof(f10188,conjecture,(
% 72.34/9.89 (? [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)& 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) ) )),
% 72.34/9.89 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.34/9.89 fof(f10189,negated_conjecture,(
% 72.34/9.89 ~((? [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)& 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) ) ))),
% 72.34/9.89 inference(negated_conjecture,[status(cth)],[f10188])).
% 72.34/9.89 fof(f10190,hypothesis,(
% 72.34/9.89 ( attr(c294,c295)& attr(c294,c296)& attr(c294,c301)& sub(c294,mensch_1_1)& sub(c295,eigenname_1_1)& val(c295,nelson_0)& sub(c296,familiename_1_1)& val(c296,mandela_0)& sub(c301,familiename_1_1)& val(c301,mandela_0)& sub(c303,pr__344sident_1_1)& attch(c313,c303)& attr(c313,c314)& sub(c313,land_1_1)& sub(c314,name_1_1)& val(c314,s__374dafrika_0)& name(c324,zukunft_in_w__374rde_und_vertrauen_0)& pred(c330,landesleute_1_1)& sub(c332,gehaltsangabe_1_1)& tupl_p7(c459,c294,c294,c303,c324,c330,c332)& assoc(landesleute_1_1,land_2_1)& sub(landesleute_1_1,leute_1_1)& sort(c294,d)& card(c294,int1)& etype(c294,int0)& fact(c294,real)& gener(c294,sp)& quant(c294,one)& refer(c294,det)& varia(c294,con)& sort(c295,na)& card(c295,int1)& etype(c295,int0)& fact(c295,real)& gener(c295,sp)& quant(c295,one)& refer(c295,indet)& varia(c295,varia_c)& sort(c296,na)& card(c296,int1)& etype(c296,int0)& fact(c296,real)& gener(c296,sp)& quant(c296,one)& refer(c296,indet)& varia(c296,varia_c)& sort(c301,na)& card(c301,int1)& etype(c301,int0)& fact(c301,real)& gener(c301,sp)& quant(c301,one)& refer(c301,indet)& varia(c301,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(c303,d)& card(c303,int1)& etype(c303,int0)& fact(c303,real)& gener(c303,sp)& quant(c303,one)& refer(c303,det)& varia(c303,con)& 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(c313,d)& sort(c313,io)& card(c313,int1)& etype(c313,int0)& fact(c313,real)& gener(c313,sp)& quant(c313,one)& refer(c313,det)& varia(c313,con)& sort(c314,na)& card(c314,int1)& etype(c314,int0)& fact(c314,real)& gener(c314,sp)& quant(c314,one)& refer(c314,indet)& varia(c314,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(c324,o)& card(c324,int1)& etype(c324,int0)& fact(c324,real)& gener(c324,gener_c)& quant(c324,one)& refer(c324,refer_c)& varia(c324,varia_c)& sort(zukunft_in_w__374rde_und_vertrauen_0,fe)& sort(c330,d)& card(c330,cons(x_constant,cons(int1,nil)))& etype(c330,int1)& fact(c330,real)& gener(c330,gener_c)& quant(c330,all)& refer(c330,det)& varia(c330,con)& sort(landesleute_1_1,d)& card(landesleute_1_1,int1)& etype(landesleute_1_1,int0)& fact(landesleute_1_1,real)& gener(landesleute_1_1,ge)& quant(landesleute_1_1,one)& refer(landesleute_1_1,refer_c)& varia(landesleute_1_1,varia_c)& sort(c332,d)& sort(c332,io)& card(c332,int1)& etype(c332,int0)& fact(c332,real)& gener(c332,gener_c)& quant(c332,one)& refer(c332,refer_c)& varia(c332,varia_c)& sort(gehaltsangabe_1_1,d)& sort(gehaltsangabe_1_1,io)& card(gehaltsangabe_1_1,int1)& etype(gehaltsangabe_1_1,int0)& fact(gehaltsangabe_1_1,real)& gener(gehaltsangabe_1_1,ge)& quant(gehaltsangabe_1_1,one)& refer(gehaltsangabe_1_1,refer_c)& varia(gehaltsangabe_1_1,varia_c)& sort(c459,ent)& card(c459,card_c)& etype(c459,etype_c)& fact(c459,real)& gener(c459,gener_c)& quant(c459,quant_c)& refer(c459,refer_c)& varia(c459,varia_c)& sort(land_2_1,d)& card(land_2_1,int1)& etype(land_2_1,int0)& fact(land_2_1,real)& gener(land_2_1,ge)& quant(land_2_1,one)& refer(land_2_1,refer_c)& varia(land_2_1,varia_c)& sort(leute_1_1,d)& card(leute_1_1,int1)& etype(leute_1_1,int0)& fact(leute_1_1,real)& gener(leute_1_1,ge)& quant(leute_1_1,one)& refer(leute_1_1,refer_c)& varia(leute_1_1,varia_c) ) ),
% 72.34/9.89 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.34/9.89 fof(f10191,plain,(
% 72.34/9.89 ![X0,X1]: (member(X0,cons(X0,X1)))),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f1])).
% 72.34/9.89 fof(f10692,plain,(
% 72.34/9.89 ![X0,X1,X2]: (((~attr(X2,X0)|~member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))))|~sub(X0,X1))|(?[X3]: ((arg1(X3,X2)&arg2(X3,X2))&subs(X3,hei__337en_1_1))))),
% 72.34/9.89 inference(pre_NNF_transformation,[status(thm)],[f159])).
% 72.34/9.89 fof(f10693,plain,(
% 72.34/9.89 ![X2]: ((![X0,X1]: ((~attr(X2,X0)|~member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))))|~sub(X0,X1)))|(?[X3]: ((arg1(X3,X2)&arg2(X3,X2))&subs(X3,hei__337en_1_1))))),
% 72.34/9.89 inference(miniscoping,[status(thm)],[f10692])).
% 72.34/9.89 fof(f10694,plain,(
% 72.34/9.89 ![X2]: ((![X0,X1]: ((~attr(X2,X0)|~member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))))|~sub(X0,X1)))|((arg1(sK50_skl(X2),X2)&arg2(sK50_skl(X2),X2))&subs(sK50_skl(X2),hei__337en_1_1)))),
% 72.34/9.89 inference(skolemize,[status(esa),new_symbols(skolem,[sK50_skl]),skolemize(X3,sK50_skl(X2))],[f10693])).
% 72.34/9.89 fof(f10695,plain,(
% 72.34/9.89 ![X0,X1,X2]: (~attr(X0,X1)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X1,X2)|arg1(sK50_skl(X0),X0))),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f10694])).
% 72.34/9.89 fof(f10696,plain,(
% 72.34/9.89 ![X0,X1,X2]: (~attr(X0,X1)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X1,X2)|arg2(sK50_skl(X0),X0))),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f10694])).
% 72.34/9.89 fof(f10697,plain,(
% 72.34/9.89 ![X0,X1,X2]: (~attr(X0,X1)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X1,X2)|subs(sK50_skl(X0),hei__337en_1_1))),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f10694])).
% 72.34/9.89 fof(f10698,plain,(
% 72.34/9.89 ![X0,X1,X2]: (((~attr(X2,X0)|~member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))))|~sub(X0,X1))|(?[X3]: (((mcont(X3,X2)&obj(X3,X2))&scar(X3,X2))&subs(X3,stehen_1_b))))),
% 72.34/9.89 inference(pre_NNF_transformation,[status(thm)],[f160])).
% 72.34/9.89 fof(f10699,plain,(
% 72.34/9.89 ![X2]: ((![X0,X1]: ((~attr(X2,X0)|~member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))))|~sub(X0,X1)))|(?[X3]: (((mcont(X3,X2)&obj(X3,X2))&scar(X3,X2))&subs(X3,stehen_1_b))))),
% 72.34/9.89 inference(miniscoping,[status(thm)],[f10698])).
% 72.34/9.89 fof(f10700,plain,(
% 72.34/9.89 ![X2]: ((![X0,X1]: ((~attr(X2,X0)|~member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))))|~sub(X0,X1)))|(((mcont(sK51_skl(X2),X2)&obj(sK51_skl(X2),X2))&scar(sK51_skl(X2),X2))&subs(sK51_skl(X2),stehen_1_b)))),
% 72.34/9.89 inference(skolemize,[status(esa),new_symbols(skolem,[sK51_skl]),skolemize(X3,sK51_skl(X2))],[f10699])).
% 72.34/9.89 fof(f10702,plain,(
% 72.34/9.89 ![X0,X1,X2]: (~attr(X0,X1)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X1,X2)|obj(sK51_skl(X0),X0))),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f10700])).
% 72.34/9.89 fof(f10705,plain,(
% 72.34/9.89 ![X0,X1,X2]: (((~arg1(X0,X1)|~arg2(X0,X2))|~subs(X0,hei__337en_1_1))|(?[X3,X4]: ((((((arg1(X4,X1)&arg2(X4,X2))&hsit(X0,X3))&mcont(X3,X4))&obj(X3,X1))&subr(X4,rprs_0))&subs(X3,bezeichnen_1_1))))),
% 72.34/9.89 inference(pre_NNF_transformation,[status(thm)],[f161])).
% 72.34/9.89 fof(f10706,plain,(
% 72.34/9.89 ![X0,X1,X2]: (((~arg1(X0,X1)|~arg2(X0,X2))|~subs(X0,hei__337en_1_1))|(?[X3]: ((?[X4]: (((((arg1(X4,X1)&arg2(X4,X2))&hsit(X0,X3))&mcont(X3,X4))&obj(X3,X1))&subr(X4,rprs_0)))&subs(X3,bezeichnen_1_1))))),
% 72.34/9.89 inference(miniscoping,[status(thm)],[f10705])).
% 72.34/9.89 fof(f10707,plain,(
% 72.34/9.89 ![X0,X1,X2]: (((~arg1(X0,X1)|~arg2(X0,X2))|~subs(X0,hei__337en_1_1))|((((((arg1(sK53_skl(X2,X1,X0),X1)&arg2(sK53_skl(X2,X1,X0),X2))&hsit(X0,sK52_skl(X2,X1,X0)))&mcont(sK52_skl(X2,X1,X0),sK53_skl(X2,X1,X0)))&obj(sK52_skl(X2,X1,X0),X1))&subr(sK53_skl(X2,X1,X0),rprs_0))&subs(sK52_skl(X2,X1,X0),bezeichnen_1_1)))),
% 72.34/9.89 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])).
% 72.34/9.89 fof(f10708,plain,(
% 72.34/9.89 ![X0,X1,X2]: (~arg1(X0,X1)|~arg2(X0,X2)|~subs(X0,hei__337en_1_1)|arg1(sK53_skl(X2,X1,X0),X1))),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f10707])).
% 72.34/9.89 fof(f10709,plain,(
% 72.34/9.89 ![X0,X1,X2]: (~arg1(X0,X1)|~arg2(X0,X2)|~subs(X0,hei__337en_1_1)|arg2(sK53_skl(X2,X1,X0),X2))),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f10707])).
% 72.34/9.89 fof(f10713,plain,(
% 72.34/9.89 ![X0,X1,X2]: (~arg1(X0,X1)|~arg2(X0,X2)|~subs(X0,hei__337en_1_1)|subr(sK53_skl(X2,X1,X0),rprs_0))),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f10707])).
% 72.34/9.89 fof(f20815,plain,(
% 72.34/9.89 (![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))|~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)))),
% 72.34/9.89 inference(pre_NNF_transformation,[status(thm)],[f10189])).
% 72.34/9.89 fof(f20816,plain,(
% 72.34/9.89 ![X6]: ((![X2]: ((![X1]: ((![X3]: (((![X4]: ((((![X0]: (((((~arg1(X3,X0)|~arg2(X3,X4))|~attr(X0,X1))|~attr(X0,X2))|(![X5]: ~attr(X5,X6)))|(![X7]: ~obj(X7,X0))))|~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))),
% 72.34/9.89 inference(miniscoping,[status(thm)],[f20815])).
% 72.34/9.89 fof(f20817,plain,(
% 72.34/9.89 ![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)|~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))),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f20816])).
% 72.34/9.89 fof(f20818,plain,(
% 72.34/9.89 attr(c294,c295)),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f10190])).
% 72.34/9.89 fof(f20819,plain,(
% 72.34/9.89 attr(c294,c296)),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f10190])).
% 72.34/9.89 fof(f20821,plain,(
% 72.34/9.89 sub(c294,mensch_1_1)),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f10190])).
% 72.34/9.89 fof(f20822,plain,(
% 72.34/9.89 sub(c295,eigenname_1_1)),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f10190])).
% 72.34/9.89 fof(f20823,plain,(
% 72.34/9.89 val(c295,nelson_0)),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f10190])).
% 72.34/9.89 fof(f20824,plain,(
% 72.34/9.89 sub(c296,familiename_1_1)),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f10190])).
% 72.34/9.89 fof(f20825,plain,(
% 72.34/9.89 val(c296,mandela_0)),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f10190])).
% 72.34/9.89 fof(f20830,plain,(
% 72.34/9.89 attr(c313,c314)),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f10190])).
% 72.34/9.89 fof(f20832,plain,(
% 72.34/9.89 sub(c314,name_1_1)),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f10190])).
% 72.34/9.89 fof(f20833,plain,(
% 72.34/9.89 val(c314,s__374dafrika_0)),
% 72.34/9.89 inference(cnf_transformation,[status(thm)],[f10190])).
% 72.34/9.89 fof(f21051,definition,(
% 72.34/9.89 ![X0,X1,X2,X3,X4,X7,X8]: (sQ0_spl <=> (~arg1(X0,X1)|~arg2(X0,X2)|~attr(X1,X3)|~attr(X1,X4)|~obj(X7,X1)|~sub(X3,familiename_1_1)|~sub(X4,eigenname_1_1)|~sub(X2,X8)|~subr(X0,rprs_0)|~val(X3,mandela_0)|~val(X4,nelson_0)))),
% 72.34/9.89 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 72.34/9.89 fof(f21052,plain,(
% 72.34/9.89 ![X0,X1,X2,X3,X4,X5,X6]: (~arg1(X0,X1)|~arg2(X0,X2)|~attr(X1,X3)|~attr(X1,X4)|~obj(X5,X1)|~sub(X3,familiename_1_1)|~sub(X4,eigenname_1_1)|~sub(X2,X6)|~subr(X0,rprs_0)|~val(X3,mandela_0)|~val(X4,nelson_0)|~sQ0_spl)),
% 72.34/9.89 inference(component_clause,[status(thm)],[f21051])).
% 72.34/9.89 fof(f21054,definition,(
% 72.34/9.89 ![X5,X6]: (sQ1_spl <=> (~attr(X5,X6)|~sub(X6,name_1_1)|~val(X6,s__374dafrika_0)))),
% 72.34/9.89 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 72.34/9.89 fof(f21055,plain,(
% 72.34/9.89 ![X0,X1]: (~attr(X0,X1)|~sub(X1,name_1_1)|~val(X1,s__374dafrika_0)|~sQ1_spl)),
% 72.34/9.89 inference(component_clause,[status(thm)],[f21054])).
% 72.34/9.89 fof(f21057,plain,(
% 72.34/9.89 sQ0_spl|sQ1_spl),
% 72.34/9.89 inference(split_clause,[status(thm)],[f20817,f21051,f21054])).
% 72.34/9.89 fof(f21063,definition,(
% 72.34/9.89 sQ3_spl <=> (val(c295,nelson_0))),
% 72.34/9.89 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 72.34/9.89 fof(f21065,plain,(
% 72.34/9.89 ~val(c295,nelson_0)|sQ3_spl),
% 72.34/9.89 inference(component_clause,[status(thm)],[f21063])).
% 72.34/9.89 fof(f21067,plain,(
% 72.34/9.89 $false|sQ3_spl),
% 72.34/9.89 inference(forward_subsumption_resolution,[status(thm)],[f21065,f20823])).
% 72.34/9.89 fof(f21068,plain,(
% 72.34/9.89 sQ3_spl),
% 72.34/9.89 inference(contradiction_clause,[status(thm)],[f21067])).
% 72.34/9.89 fof(f21072,plain,(
% 72.34/9.89 ![X0]: (~attr(X0,c314)|~val(c314,s__374dafrika_0)|~sQ1_spl)),
% 72.34/9.89 inference(resolution,[status(thm)],[f21055,f20832])).
% 72.34/9.89 fof(f21073,definition,(
% 72.34/9.89 ![X0]: (sQ4_spl <=> (~attr(X0,c314)))),
% 72.34/9.89 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 72.34/9.89 fof(f21074,plain,(
% 72.34/9.89 ![X0]: (~attr(X0,c314)|~sQ4_spl)),
% 72.34/9.89 inference(component_clause,[status(thm)],[f21073])).
% 72.34/9.89 fof(f21076,definition,(
% 72.34/9.89 sQ5_spl <=> (val(c314,s__374dafrika_0))),
% 72.34/9.89 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 72.34/9.89 fof(f21078,plain,(
% 72.34/9.89 ~val(c314,s__374dafrika_0)|sQ5_spl),
% 72.34/9.89 inference(component_clause,[status(thm)],[f21076])).
% 72.34/9.89 fof(f21079,plain,(
% 72.34/9.89 sQ4_spl|~sQ5_spl|~sQ1_spl),
% 72.34/9.89 inference(split_clause,[status(thm)],[f21072,f21073,f21076,f21054])).
% 72.34/9.89 fof(f21080,plain,(
% 72.34/9.89 $false|sQ5_spl),
% 72.34/9.89 inference(forward_subsumption_resolution,[status(thm)],[f21078,f20833])).
% 72.34/9.89 fof(f21081,plain,(
% 72.34/9.89 sQ5_spl),
% 72.34/9.89 inference(contradiction_clause,[status(thm)],[f21080])).
% 72.34/9.89 fof(f21082,plain,(
% 72.34/9.89 $false|~sQ4_spl),
% 72.34/9.89 inference(backward_subsumption_resolution,[status(thm)],[f20830,f21074])).
% 72.34/9.89 fof(f21083,plain,(
% 72.34/9.89 ~sQ4_spl),
% 72.34/9.89 inference(contradiction_clause,[status(thm)],[f21082])).
% 72.34/9.89 fof(f21091,plain,(
% 72.34/9.89 ![X0,X1,X2,X3,X4]: (~attr(X0,X1)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X1,X2)|~arg1(sK50_skl(X0),X3)|~arg2(sK50_skl(X0),X4)|subr(sK53_skl(X4,X3,sK50_skl(X0)),rprs_0))),
% 72.34/9.89 inference(resolution,[status(thm)],[f10697,f10713])).
% 72.34/9.89 fof(f21092,plain,(
% 72.34/9.89 ![X0,X1,X2,X3,X4,X5]: (~attr(X0,X1)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X1,X2)|~arg2(sK50_skl(X0),X3)|subr(sK53_skl(X3,X0,sK50_skl(X0)),rprs_0)|~attr(X0,X4)|~member(X5,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X4,X5))),
% 72.34/9.89 inference(resolution,[status(thm)],[f21091,f10695])).
% 72.34/9.89 fof(f21093,plain,(
% 72.34/9.89 ![X0,X1,X2,X3,X4,X5,X6]: (~attr(X0,X1)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X1,X2)|subr(sK53_skl(X0,X0,sK50_skl(X0)),rprs_0)|~attr(X0,X3)|~member(X4,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X3,X4)|~attr(X0,X5)|~member(X6,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X5,X6))),
% 72.34/9.89 inference(resolution,[status(thm)],[f21092,f10696])).
% 72.34/9.89 fof(f21095,plain,(
% 72.34/9.89 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~attr(X0,X1)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X1,X2)|~attr(X0,X3)|~member(X4,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X3,X4)|~attr(X0,X5)|~member(X6,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X5,X6)|~arg1(sK53_skl(X0,X0,sK50_skl(X0)),X7)|~arg2(sK53_skl(X0,X0,sK50_skl(X0)),X8)|~attr(X7,X9)|~attr(X7,X10)|~obj(X11,X7)|~sub(X9,familiename_1_1)|~sub(X10,eigenname_1_1)|~sub(X8,X12)|~val(X9,mandela_0)|~val(X10,nelson_0)|~sQ0_spl)),
% 72.34/9.89 inference(resolution,[status(thm)],[f21093,f21052])).
% 72.34/9.89 fof(f23598,plain,(
% 72.34/9.89 ![X0,X1,X2,X3,X4]: (~arg1(sK50_skl(X0),X1)|~arg2(sK50_skl(X0),X2)|arg1(sK53_skl(X2,X1,sK50_skl(X0)),X1)|~attr(X0,X3)|~member(X4,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X3,X4))),
% 72.34/9.89 inference(resolution,[status(thm)],[f10708,f10697])).
% 72.34/9.89 fof(f23607,plain,(
% 72.34/9.89 ![X0,X1,X2,X3,X4,X5]: (~arg2(sK50_skl(X0),X1)|arg1(sK53_skl(X1,X0,sK50_skl(X0)),X0)|~attr(X0,X2)|~member(X3,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X2,X3)|~attr(X0,X4)|~member(X5,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X4,X5))),
% 72.34/9.89 inference(resolution,[status(thm)],[f23598,f10695])).
% 72.34/9.89 fof(f23608,plain,(
% 72.34/9.89 ![X0,X1,X2,X3,X4,X5,X6]: (arg1(sK53_skl(X0,X0,sK50_skl(X0)),X0)|~attr(X0,X1)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X1,X2)|~attr(X0,X3)|~member(X4,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X3,X4)|~attr(X0,X5)|~member(X6,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X5,X6))),
% 72.34/9.89 inference(resolution,[status(thm)],[f23607,f10696])).
% 72.34/9.89 fof(f23611,plain,(
% 72.34/9.89 ![X0,X1,X2,X3,X4]: (arg1(sK53_skl(X0,X0,sK50_skl(X0)),X0)|~attr(X0,X1)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X1,X2)|~attr(X0,X3)|~sub(X3,eigenname_1_1)|~attr(X0,X4)|~sub(X4,eigenname_1_1))),
% 72.34/9.89 inference(resolution,[status(thm)],[f23608,f10191])).
% 72.34/9.89 fof(f23616,plain,(
% 72.34/9.89 ![X0,X1,X2,X3]: (arg1(sK53_skl(X0,X0,sK50_skl(X0)),X0)|~attr(X0,X1)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X1,X2)|~attr(X0,X3)|~sub(X3,eigenname_1_1)|~attr(X0,c295))),
% 72.34/9.89 inference(resolution,[status(thm)],[f23611,f20822])).
% 72.34/9.89 fof(f23617,plain,(
% 72.34/9.89 ![X0,X1,X2]: (arg1(sK53_skl(X0,X0,sK50_skl(X0)),X0)|~attr(X0,X1)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X1,X2)|~attr(X0,c295)|~attr(X0,c295))),
% 72.34/9.89 inference(resolution,[status(thm)],[f23616,f20822])).
% 72.34/9.89 fof(f23618,plain,(
% 72.34/9.89 ![X0,X1,X2]: (arg1(sK53_skl(X0,X0,sK50_skl(X0)),X0)|~attr(X0,X1)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X1,X2)|~attr(X0,c295))),
% 72.34/9.89 inference(duplicate_literals_removal,[status(thm)],[f23617])).
% 72.34/9.89 fof(f23619,plain,(
% 72.34/9.89 ![X0,X1]: (arg1(sK53_skl(c294,c294,sK50_skl(c294)),c294)|~attr(c294,X0)|~member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X0,X1))),
% 72.34/9.89 inference(resolution,[status(thm)],[f23618,f20818])).
% 72.34/9.89 fof(f23620,definition,(
% 72.34/9.89 sQ6_spl <=> (arg1(sK53_skl(c294,c294,sK50_skl(c294)),c294))),
% 72.34/9.89 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 72.34/9.89 fof(f23621,plain,(
% 72.34/9.89 arg1(sK53_skl(c294,c294,sK50_skl(c294)),c294)|~sQ6_spl),
% 72.34/9.89 inference(component_clause,[status(thm)],[f23620])).
% 72.34/9.89 fof(f23623,definition,(
% 72.34/9.89 ![X0,X1]: (sQ7_spl <=> (~attr(c294,X0)|~member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X0,X1)))),
% 72.34/9.89 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 72.34/9.89 fof(f23624,plain,(
% 72.34/9.89 ![X0,X1]: (~attr(c294,X0)|~member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X0,X1)|~sQ7_spl)),
% 72.34/9.89 inference(component_clause,[status(thm)],[f23623])).
% 72.34/9.89 fof(f23626,plain,(
% 72.34/9.89 sQ6_spl|sQ7_spl),
% 72.34/9.89 inference(split_clause,[status(thm)],[f23619,f23620,f23623])).
% 72.34/9.89 fof(f23627,plain,(
% 72.34/9.89 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~attr(c294,X0)|~member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X0,X1)|~attr(c294,X2)|~member(X3,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X2,X3)|~attr(c294,X4)|~member(X5,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X4,X5)|~arg2(sK53_skl(c294,c294,sK50_skl(c294)),X6)|~attr(c294,X7)|~attr(c294,X8)|~obj(X9,c294)|~sub(X7,familiename_1_1)|~sub(X8,eigenname_1_1)|~sub(X6,X10)|~val(X7,mandela_0)|~val(X8,nelson_0)|~sQ6_spl|~sQ0_spl)),
% 72.34/9.89 inference(resolution,[status(thm)],[f23621,f21095])).
% 72.34/9.89 fof(f23631,definition,(
% 72.34/9.89 ![X6,X10]: (sQ8_spl <=> (~arg2(sK53_skl(c294,c294,sK50_skl(c294)),X6)|~sub(X6,X10)))),
% 72.34/9.89 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 72.34/9.89 fof(f23632,plain,(
% 72.34/9.89 ![X0,X1]: (~arg2(sK53_skl(c294,c294,sK50_skl(c294)),X0)|~sub(X0,X1)|~sQ8_spl)),
% 72.34/9.89 inference(component_clause,[status(thm)],[f23631])).
% 72.34/9.89 fof(f23634,definition,(
% 72.34/9.89 ![X7]: (sQ9_spl <=> (~attr(c294,X7)|~sub(X7,familiename_1_1)|~val(X7,mandela_0)))),
% 72.34/9.89 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 72.34/9.89 fof(f23635,plain,(
% 72.34/9.89 ![X0]: (~attr(c294,X0)|~sub(X0,familiename_1_1)|~val(X0,mandela_0)|~sQ9_spl)),
% 72.34/9.89 inference(component_clause,[status(thm)],[f23634])).
% 72.34/9.89 fof(f23637,definition,(
% 72.34/9.89 ![X8]: (sQ10_spl <=> (~attr(c294,X8)|~sub(X8,eigenname_1_1)|~val(X8,nelson_0)))),
% 72.34/9.89 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 72.34/9.89 fof(f23638,plain,(
% 72.34/9.89 ![X0]: (~attr(c294,X0)|~sub(X0,eigenname_1_1)|~val(X0,nelson_0)|~sQ10_spl)),
% 72.34/9.89 inference(component_clause,[status(thm)],[f23637])).
% 72.34/9.89 fof(f23640,definition,(
% 72.34/9.89 ![X9]: (sQ11_spl <=> (~obj(X9,c294)))),
% 72.34/9.89 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 72.34/9.89 fof(f23641,plain,(
% 72.34/9.89 ![X0]: (~obj(X0,c294)|~sQ11_spl)),
% 72.34/9.89 inference(component_clause,[status(thm)],[f23640])).
% 72.34/9.89 fof(f23643,plain,(
% 72.34/9.89 sQ7_spl|sQ8_spl|sQ9_spl|sQ10_spl|sQ11_spl|~sQ6_spl|~sQ0_spl),
% 72.34/9.89 inference(split_clause,[status(thm)],[f23627,f23623,f23631,f23634,f23637,f23640,f23620,f21051])).
% 72.34/9.89 fof(f23644,definition,(
% 72.34/9.89 sQ12_spl <=> (attr(c294,c295))),
% 72.34/9.89 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 72.34/9.89 fof(f23646,plain,(
% 72.34/9.89 ~attr(c294,c295)|sQ12_spl),
% 72.34/9.89 inference(component_clause,[status(thm)],[f23644])).
% 72.34/9.89 fof(f23651,definition,(
% 72.34/9.89 sQ14_spl <=> (arg1(sK50_skl(c294),c294))),
% 72.34/9.89 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 72.34/9.89 fof(f23653,plain,(
% 72.34/9.89 ~arg1(sK50_skl(c294),c294)|sQ14_spl),
% 72.34/9.89 inference(component_clause,[status(thm)],[f23651])).
% 72.34/9.89 fof(f23654,definition,(
% 72.34/9.89 sQ15_spl <=> (arg2(sK50_skl(c294),c294))),
% 72.34/9.89 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 72.34/9.89 fof(f23656,plain,(
% 72.34/9.89 ~arg2(sK50_skl(c294),c294)|sQ15_spl),
% 72.34/9.89 inference(component_clause,[status(thm)],[f23654])).
% 72.34/9.89 fof(f23964,plain,(
% 72.34/9.89 ![X0,X1]: (~attr(c294,X0)|~member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X0,X1)|~sQ11_spl)),
% 72.34/9.89 inference(resolution,[status(thm)],[f23641,f10702])).
% 72.34/9.89 fof(f23979,plain,(
% 72.34/9.89 $false|sQ12_spl),
% 72.34/9.89 inference(forward_subsumption_resolution,[status(thm)],[f23646,f20818])).
% 72.34/9.89 fof(f23980,plain,(
% 72.34/9.89 sQ12_spl),
% 72.34/9.89 inference(contradiction_clause,[status(thm)],[f23979])).
% 72.34/9.89 fof(f23982,plain,(
% 72.34/9.89 ~attr(c294,c296)|~val(c296,mandela_0)|~sQ9_spl),
% 72.34/9.89 inference(resolution,[status(thm)],[f23635,f20824])).
% 72.34/9.89 fof(f23990,definition,(
% 72.34/9.89 sQ22_spl <=> (attr(c294,c296))),
% 72.34/9.89 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 72.34/9.89 fof(f23992,plain,(
% 72.34/9.89 ~attr(c294,c296)|sQ22_spl),
% 72.34/9.89 inference(component_clause,[status(thm)],[f23990])).
% 72.34/9.89 fof(f23993,definition,(
% 72.34/9.89 sQ23_spl <=> (val(c296,mandela_0))),
% 72.34/9.89 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 72.34/9.89 fof(f23995,plain,(
% 72.34/9.89 ~val(c296,mandela_0)|sQ23_spl),
% 72.34/9.89 inference(component_clause,[status(thm)],[f23993])).
% 72.34/9.89 fof(f23996,plain,(
% 72.34/9.89 ~sQ22_spl|~sQ23_spl|~sQ9_spl),
% 72.34/9.89 inference(split_clause,[status(thm)],[f23982,f23990,f23993,f23634])).
% 72.34/9.95 fof(f23997,plain,(
% 72.34/9.95 $false|sQ23_spl),
% 72.34/9.95 inference(forward_subsumption_resolution,[status(thm)],[f23995,f20825])).
% 72.34/9.95 fof(f23998,plain,(
% 72.34/9.95 sQ23_spl),
% 72.34/9.95 inference(contradiction_clause,[status(thm)],[f23997])).
% 72.34/9.95 fof(f23999,plain,(
% 72.34/9.95 $false|sQ22_spl),
% 72.34/9.95 inference(forward_subsumption_resolution,[status(thm)],[f23992,f20819])).
% 72.34/9.95 fof(f24000,plain,(
% 72.34/9.95 sQ22_spl),
% 72.34/9.95 inference(contradiction_clause,[status(thm)],[f23999])).
% 72.34/9.95 fof(f24005,plain,(
% 72.34/9.95 ~attr(c294,c295)|~val(c295,nelson_0)|~sQ10_spl),
% 72.34/9.95 inference(resolution,[status(thm)],[f23638,f20822])).
% 72.34/9.95 fof(f24006,plain,(
% 72.34/9.95 ~sQ12_spl|~sQ3_spl|~sQ10_spl),
% 72.34/9.95 inference(split_clause,[status(thm)],[f24005,f23644,f21063,f23637])).
% 72.34/9.95 fof(f24008,plain,(
% 72.34/9.95 ![X0]: (~attr(c294,X0)|~sub(X0,eigenname_1_1)|~sQ7_spl)),
% 72.34/9.95 inference(resolution,[status(thm)],[f23624,f10191])).
% 72.34/9.95 fof(f24009,plain,(
% 72.34/9.95 ~attr(c294,c295)|~sQ7_spl),
% 72.34/9.95 inference(resolution,[status(thm)],[f24008,f20822])).
% 72.34/9.95 fof(f24010,plain,(
% 72.34/9.95 ~sQ12_spl|~sQ7_spl),
% 72.34/9.95 inference(split_clause,[status(thm)],[f24009,f23644,f23623])).
% 72.34/9.95 fof(f24025,plain,(
% 72.34/9.95 ![X0,X1]: (~attr(c294,X0)|~member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X0,X1)|sQ15_spl)),
% 72.34/9.95 inference(resolution,[status(thm)],[f23656,f10696])).
% 72.34/9.95 fof(f24026,plain,(
% 72.34/9.95 sQ7_spl|sQ15_spl),
% 72.34/9.95 inference(split_clause,[status(thm)],[f24025,f23623,f23654])).
% 72.34/9.95 fof(f24034,plain,(
% 72.34/9.95 ![X0,X1]: (~attr(c294,X0)|~member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X0,X1)|sQ14_spl)),
% 72.34/9.95 inference(resolution,[status(thm)],[f23653,f10695])).
% 72.34/9.95 fof(f24035,plain,(
% 72.34/9.95 sQ7_spl|sQ14_spl),
% 72.34/9.95 inference(split_clause,[status(thm)],[f24034,f23623,f23651])).
% 72.34/9.95 fof(f24036,plain,(
% 72.34/9.95 ![X0]: (~sub(c294,X0)|~arg1(sK50_skl(c294),c294)|~arg2(sK50_skl(c294),c294)|~subs(sK50_skl(c294),hei__337en_1_1)|~sQ8_spl)),
% 72.34/9.95 inference(resolution,[status(thm)],[f23632,f10709])).
% 72.34/9.95 fof(f24037,definition,(
% 72.34/9.95 ![X0]: (sQ26_spl <=> (~sub(c294,X0)))),
% 72.34/9.95 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 72.34/9.95 fof(f24038,plain,(
% 72.34/9.95 ![X0]: (~sub(c294,X0)|~sQ26_spl)),
% 72.34/9.95 inference(component_clause,[status(thm)],[f24037])).
% 72.34/9.95 fof(f24040,definition,(
% 72.34/9.95 sQ27_spl <=> (subs(sK50_skl(c294),hei__337en_1_1))),
% 72.34/9.95 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 72.34/9.95 fof(f24042,plain,(
% 72.34/9.95 ~subs(sK50_skl(c294),hei__337en_1_1)|sQ27_spl),
% 72.34/9.95 inference(component_clause,[status(thm)],[f24040])).
% 72.34/9.95 fof(f24043,plain,(
% 72.34/9.95 sQ26_spl|~sQ14_spl|~sQ15_spl|~sQ27_spl|~sQ8_spl),
% 72.34/9.95 inference(split_clause,[status(thm)],[f24036,f24037,f23651,f23654,f24040,f23631])).
% 72.34/9.95 fof(f24044,plain,(
% 72.34/9.95 $false|~sQ26_spl),
% 72.34/9.95 inference(backward_subsumption_resolution,[status(thm)],[f20821,f24038])).
% 72.34/9.95 fof(f24045,plain,(
% 72.34/9.95 ~sQ26_spl),
% 72.34/9.95 inference(contradiction_clause,[status(thm)],[f24044])).
% 72.34/9.95 fof(f24056,plain,(
% 72.34/9.95 ![X0,X1]: (~attr(c294,X0)|~member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X0,X1)|sQ27_spl)),
% 72.34/9.95 inference(resolution,[status(thm)],[f24042,f10697])).
% 72.34/9.95 fof(f24058,plain,(
% 72.34/9.95 sQ7_spl|sQ27_spl),
% 72.34/9.95 inference(split_clause,[status(thm)],[f24056,f23623,f24040])).
% 72.34/9.95 fof(f24059,plain,(
% 72.34/9.95 sQ7_spl|~sQ11_spl),
% 72.34/9.95 inference(split_clause,[status(thm)],[f23964,f23623,f23640])).
% 72.34/9.95 fof(f24060,plain,(
% 72.34/9.95 $false),
% 72.34/9.95 inference(sat_refutation,[status(thm)],[f21057,f21068,f21079,f21081,f21083,f23626,f23643,f23980,f23996,f23998,f24000,f24006,f24010,f24026,f24035,f24043,f24045,f24058,f24059])).
% 72.34/9.95 % SZS output end CNFRefutation for theBenchmark.p
% 50.15/10.00 % Elapsed time: 9.492386 seconds
% 50.15/10.00 % CPU time: 72.936648 seconds
% 50.15/10.00 % Total memory used: 631.356 MB
% 50.15/10.00 % Net memory used: 615.876 MB
%------------------------------------------------------------------------------