%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR113+23 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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:19 PM UTC 2026
% Result : Theorem 54.06s 7.35s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR113+23 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n001.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 15:09:15 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.23/0.49 % Drodi V4.1.1
% 54.06/7.35 % Refutation found
% 54.06/7.35 % SZS status Theorem for theBenchmark: Theorem is valid
% 54.06/7.35 % SZS output start CNFRefutation for theBenchmark
% 54.06/7.35 fof(f1,axiom,(
% 54.06/7.35 (! [X0,X1] : member(X0,cons(X0,X1)) )),
% 54.06/7.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.06/7.35 fof(f2,axiom,(
% 54.06/7.35 (! [X0,X1,X2] :( member(X0,X2)=> member(X0,cons(X1,X2)) ) )),
% 54.06/7.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.06/7.35 fof(f160,axiom,(
% 54.06/7.35 (! [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) ) )) )),
% 54.06/7.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.06/7.35 fof(f10188,conjecture,(
% 54.06/7.35 (? [X0,X1,X2,X3] :( attr(X1,X0)& scar(X2,X3)& sub(X0,name_1_1)& val(X0,usa_0) ) )),
% 54.06/7.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.06/7.35 fof(f10189,negated_conjecture,(
% 54.06/7.35 ~((? [X0,X1,X2,X3] :( attr(X1,X0)& scar(X2,X3)& sub(X0,name_1_1)& val(X0,usa_0) ) ))),
% 54.06/7.35 inference(negated_conjecture,[status(cth)],[f10188])).
% 54.06/7.35 fof(f10190,hypothesis,(
% 54.06/7.35 ( pred(c43330,lef__350vre_1_1)& attr(c43332,c43333)& sub(c43332,mensch_1_1)& sub(c43333,eigenname_1_1)& val(c43333,c43334)& tupl(c43334,edouard_0,ren__351_0)& attr(c43341,c43342)& prop(c43341,de_1_1)& sub(c43341,mensch_1_1)& sub(c43342,familiename_1_1)& val(c43342,laboulaye_0)& pred(c43346,enkel__1_1)& attch(c43350,c43346)& sub(c43350,marquis_1_1)& attr(c43358,c43359)& prop(c43358,de_1_1)& sub(c43358,stadt__1_1)& sub(c43359,name_1_1)& val(c43359,lafayette_0)& pred(c43362,bartholdi_1_1)& attr(c43364,c43365)& sub(c43364,mensch_1_1)& sub(c43365,eigenname_1_1)& val(c43365,c43366)& tupl(c43366,fr__351d__351ric_0,auguste_0)& prop(c43375,jugendlich_1_1)& sub(c43375,k__374nstler_1_1)& attr(c43384,c43385)& sub(c43384,gebiet_1_1)& sub(c43385,name_1_1)& val(c43385,elsa__337_0)& obj(c43400,c43404)& subs(c43400,finanzierung_1_1)& sub(c43404,freiheitsstatue_1_1)& sub(c43411,geschenk__1_1)& attr(c43441,c43442)& sub(c43441,land_1_1)& sub(c43442,name_1_1)& val(c43442,usa_0)& obj(c43449,c43444)& subs(c43449,einweihung_1_1)& prop(c43461,c43325)& tupl_p17(c44809,c43332,c43330,c43341,c43346,c43358,c43364,c43362,c43375,c43384,c43375,c43400,c43411,c43441,c43449,c43451,c43461)& assoc(freiheitsstatue_1_1,freiheit_1_1)& sub(freiheitsstatue_1_1,statue_1_1)& chsp2(miterleben_1_1,c43325)& sort(c43330,o)& card(c43330,cons(x_constant,cons(int1,nil)))& etype(c43330,int1)& fact(c43330,real)& gener(c43330,gener_c)& quant(c43330,mult)& refer(c43330,indet)& varia(c43330,varia_c)& sort(lef__350vre_1_1,o)& card(lef__350vre_1_1,int1)& etype(lef__350vre_1_1,int0)& fact(lef__350vre_1_1,real)& gener(lef__350vre_1_1,ge)& quant(lef__350vre_1_1,one)& refer(lef__350vre_1_1,refer_c)& varia(lef__350vre_1_1,varia_c)& sort(c43332,d)& card(c43332,int1)& etype(c43332,int0)& fact(c43332,real)& gener(c43332,sp)& quant(c43332,one)& refer(c43332,det)& varia(c43332,con)& sort(c43333,na)& card(c43333,int1)& etype(c43333,int0)& fact(c43333,real)& gener(c43333,sp)& quant(c43333,one)& refer(c43333,indet)& varia(c43333,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(c43334,fe)& sort(edouard_0,fe)& sort(ren__351_0,fe)& sort(c43341,d)& card(c43341,int1)& etype(c43341,int0)& fact(c43341,real)& gener(c43341,sp)& quant(c43341,one)& refer(c43341,det)& varia(c43341,con)& sort(c43342,na)& card(c43342,int1)& etype(c43342,int0)& fact(c43342,real)& gener(c43342,sp)& quant(c43342,one)& refer(c43342,det)& varia(c43342,varia_c)& sort(de_1_1,gq)& 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(laboulaye_0,fe)& sort(c43346,d)& card(c43346,cons(x_constant,cons(int1,nil)))& etype(c43346,int1)& fact(c43346,real)& gener(c43346,sp)& quant(c43346,mult)& refer(c43346,det)& varia(c43346,con)& sort(enkel__1_1,d)& card(enkel__1_1,int1)& etype(enkel__1_1,int0)& fact(enkel__1_1,real)& gener(enkel__1_1,ge)& quant(enkel__1_1,one)& refer(enkel__1_1,refer_c)& varia(enkel__1_1,varia_c)& sort(c43350,o)& card(c43350,int1)& etype(c43350,int0)& fact(c43350,real)& gener(c43350,sp)& quant(c43350,one)& refer(c43350,det)& varia(c43350,con)& sort(marquis_1_1,o)& card(marquis_1_1,int1)& etype(marquis_1_1,int0)& fact(marquis_1_1,real)& gener(marquis_1_1,ge)& quant(marquis_1_1,one)& refer(marquis_1_1,refer_c)& varia(marquis_1_1,varia_c)& sort(c43358,d)& sort(c43358,io)& card(c43358,int1)& etype(c43358,int0)& fact(c43358,real)& gener(c43358,sp)& quant(c43358,one)& refer(c43358,det)& varia(c43358,con)& sort(c43359,na)& card(c43359,int1)& etype(c43359,int0)& fact(c43359,real)& gener(c43359,sp)& quant(c43359,one)& refer(c43359,det)& varia(c43359,varia_c)& sort(stadt__1_1,d)& sort(stadt__1_1,io)& card(stadt__1_1,int1)& etype(stadt__1_1,int0)& fact(stadt__1_1,real)& gener(stadt__1_1,ge)& quant(stadt__1_1,one)& refer(stadt__1_1,refer_c)& varia(stadt__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(lafayette_0,fe)& sort(c43362,o)& card(c43362,cons(x_constant,cons(int1,nil)))& etype(c43362,int1)& fact(c43362,real)& gener(c43362,gener_c)& quant(c43362,mult)& refer(c43362,indet)& varia(c43362,varia_c)& sort(bartholdi_1_1,o)& card(bartholdi_1_1,int1)& etype(bartholdi_1_1,int0)& fact(bartholdi_1_1,real)& gener(bartholdi_1_1,ge)& quant(bartholdi_1_1,one)& refer(bartholdi_1_1,refer_c)& varia(bartholdi_1_1,varia_c)& sort(c43364,d)& card(c43364,int1)& etype(c43364,int0)& fact(c43364,real)& gener(c43364,sp)& quant(c43364,one)& refer(c43364,det)& varia(c43364,con)& sort(c43365,na)& card(c43365,int1)& etype(c43365,int0)& fact(c43365,real)& gener(c43365,sp)& quant(c43365,one)& refer(c43365,indet)& varia(c43365,varia_c)& sort(c43366,fe)& sort(fr__351d__351ric_0,fe)& sort(auguste_0,fe)& sort(c43375,d)& card(c43375,int1)& etype(c43375,int0)& fact(c43375,real)& gener(c43375,sp)& quant(c43375,one)& refer(c43375,indet)& varia(c43375,varia_c)& sort(jugendlich_1_1,nq)& sort(k__374nstler_1_1,d)& card(k__374nstler_1_1,int1)& etype(k__374nstler_1_1,int0)& fact(k__374nstler_1_1,real)& gener(k__374nstler_1_1,ge)& quant(k__374nstler_1_1,one)& refer(k__374nstler_1_1,refer_c)& varia(k__374nstler_1_1,varia_c)& sort(c43384,d)& card(c43384,int1)& etype(c43384,int0)& fact(c43384,real)& gener(c43384,sp)& quant(c43384,one)& refer(c43384,det)& varia(c43384,con)& sort(c43385,na)& card(c43385,int1)& etype(c43385,int0)& fact(c43385,real)& gener(c43385,sp)& quant(c43385,one)& refer(c43385,indet)& varia(c43385,varia_c)& sort(gebiet_1_1,d)& card(gebiet_1_1,int1)& etype(gebiet_1_1,int0)& fact(gebiet_1_1,real)& gener(gebiet_1_1,ge)& quant(gebiet_1_1,one)& refer(gebiet_1_1,refer_c)& varia(gebiet_1_1,varia_c)& sort(elsa__337_0,fe)& sort(c43400,ad)& card(c43400,int1)& etype(c43400,int0)& fact(c43400,real)& gener(c43400,sp)& quant(c43400,one)& refer(c43400,det)& varia(c43400,con)& sort(c43404,d)& card(c43404,int1)& etype(c43404,int0)& fact(c43404,real)& gener(c43404,sp)& quant(c43404,one)& refer(c43404,det)& varia(c43404,con)& sort(finanzierung_1_1,ad)& card(finanzierung_1_1,int1)& etype(finanzierung_1_1,int0)& fact(finanzierung_1_1,real)& gener(finanzierung_1_1,ge)& quant(finanzierung_1_1,one)& refer(finanzierung_1_1,refer_c)& varia(finanzierung_1_1,varia_c)& sort(freiheitsstatue_1_1,d)& card(freiheitsstatue_1_1,int1)& etype(freiheitsstatue_1_1,int0)& fact(freiheitsstatue_1_1,real)& gener(freiheitsstatue_1_1,ge)& quant(freiheitsstatue_1_1,one)& refer(freiheitsstatue_1_1,refer_c)& varia(freiheitsstatue_1_1,varia_c)& sort(c43411,co)& card(c43411,card_c)& etype(c43411,etype_c)& fact(c43411,real)& gener(c43411,sp)& quant(c43411,quant_c)& refer(c43411,indet)& varia(c43411,varia_c)& sort(geschenk__1_1,co)& card(geschenk__1_1,card_c)& etype(geschenk__1_1,etype_c)& fact(geschenk__1_1,real)& gener(geschenk__1_1,ge)& quant(geschenk__1_1,quant_c)& refer(geschenk__1_1,refer_c)& varia(geschenk__1_1,varia_c)& sort(c43441,d)& sort(c43441,io)& card(c43441,int1)& etype(c43441,int0)& fact(c43441,real)& gener(c43441,sp)& quant(c43441,one)& refer(c43441,det)& varia(c43441,con)& sort(c43442,na)& card(c43442,int1)& etype(c43442,int0)& fact(c43442,real)& gener(c43442,sp)& quant(c43442,one)& refer(c43442,indet)& varia(c43442,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(usa_0,fe)& sort(c43449,ad)& card(c43449,int1)& etype(c43449,int0)& fact(c43449,real)& gener(c43449,sp)& quant(c43449,one)& refer(c43449,det)& varia(c43449,varia_c)& sort(c43444,co)& card(c43444,card_c)& etype(c43444,etype_c)& fact(c43444,real)& gener(c43444,sp)& quant(c43444,quant_c)& refer(c43444,det)& varia(c43444,varia_c)& sort(einweihung_1_1,ad)& card(einweihung_1_1,int1)& etype(einweihung_1_1,int0)& fact(einweihung_1_1,real)& gener(einweihung_1_1,ge)& quant(einweihung_1_1,one)& refer(einweihung_1_1,refer_c)& varia(einweihung_1_1,varia_c)& sort(c43461,o)& card(c43461,int1)& etype(c43461,int0)& fact(c43461,real)& gener(c43461,gener_c)& quant(c43461,one)& refer(c43461,refer_c)& varia(c43461,varia_c)& sort(c43325,tq)& sort(c44809,ent)& card(c44809,card_c)& etype(c44809,etype_c)& fact(c44809,real)& gener(c44809,gener_c)& quant(c44809,quant_c)& refer(c44809,refer_c)& varia(c44809,varia_c)& sort(c43451,o)& card(c43451,int1)& etype(c43451,int0)& fact(c43451,real)& gener(c43451,sp)& quant(c43451,one)& refer(c43451,det)& varia(c43451,varia_c)& sort(freiheit_1_1,as)& sort(freiheit_1_1,io)& card(freiheit_1_1,int1)& etype(freiheit_1_1,int0)& fact(freiheit_1_1,real)& gener(freiheit_1_1,ge)& quant(freiheit_1_1,one)& refer(freiheit_1_1,refer_c)& varia(freiheit_1_1,varia_c)& sort(statue_1_1,d)& card(statue_1_1,int1)& etype(statue_1_1,int0)& fact(statue_1_1,real)& gener(statue_1_1,ge)& quant(statue_1_1,one)& refer(statue_1_1,refer_c)& varia(statue_1_1,varia_c)& sort(miterleben_1_1,dn)& fact(miterleben_1_1,real)& gener(miterleben_1_1,ge) ) ),
% 54.06/7.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 54.06/7.35 fof(f10191,plain,(
% 54.06/7.35 ![X0,X1]: (member(X0,cons(X0,X1)))),
% 54.06/7.35 inference(cnf_transformation,[status(thm)],[f1])).
% 54.06/7.35 fof(f10192,plain,(
% 54.06/7.35 ![X0,X1,X2]: (~member(X0,X2)|member(X0,cons(X1,X2)))),
% 54.06/7.35 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 54.06/7.35 fof(f10193,plain,(
% 54.06/7.35 ![X0,X2]: (~member(X0,X2)|(![X1]: member(X0,cons(X1,X2))))),
% 54.06/7.35 inference(miniscoping,[status(thm)],[f10192])).
% 54.06/7.35 fof(f10194,plain,(
% 54.06/7.35 ![X0,X1,X2]: (~member(X0,X1)|member(X0,cons(X2,X1)))),
% 54.06/7.35 inference(cnf_transformation,[status(thm)],[f10193])).
% 54.06/7.35 fof(f10698,plain,(
% 54.06/7.35 ![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))))),
% 54.06/7.35 inference(pre_NNF_transformation,[status(thm)],[f160])).
% 54.06/7.35 fof(f10699,plain,(
% 54.06/7.35 ![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))))),
% 54.06/7.35 inference(miniscoping,[status(thm)],[f10698])).
% 54.06/7.35 fof(f10700,plain,(
% 54.06/7.35 ![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)))),
% 54.06/7.35 inference(skolemize,[status(esa),new_symbols(skolem,[sK51_skl]),skolemize(X3,sK51_skl(X2))],[f10699])).
% 54.06/7.35 fof(f10703,plain,(
% 54.06/7.35 ![X0,X1,X2]: (~attr(X0,X1)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X1,X2)|scar(sK51_skl(X0),X0))),
% 54.06/7.35 inference(cnf_transformation,[status(thm)],[f10700])).
% 54.06/7.35 fof(f20815,plain,(
% 54.06/7.35 (![X0,X1,X2,X3]: (((~attr(X1,X0)|~scar(X2,X3))|~sub(X0,name_1_1))|~val(X0,usa_0)))),
% 54.06/7.35 inference(pre_NNF_transformation,[status(thm)],[f10189])).
% 46.21/7.42 fof(f20816,plain,(
% 46.21/7.42 ![X0]: ((((![X1]: ~attr(X1,X0))|(![X2,X3]: ~scar(X2,X3)))|~sub(X0,name_1_1))|~val(X0,usa_0))),
% 46.21/7.42 inference(miniscoping,[status(thm)],[f20815])).
% 46.21/7.42 fof(f20817,plain,(
% 46.21/7.42 ![X0,X1,X2,X3]: (~attr(X0,X1)|~scar(X2,X3)|~sub(X1,name_1_1)|~val(X1,usa_0))),
% 46.21/7.42 inference(cnf_transformation,[status(thm)],[f20816])).
% 46.21/7.42 fof(f20853,plain,(
% 46.21/7.42 attr(c43441,c43442)),
% 46.21/7.42 inference(cnf_transformation,[status(thm)],[f10190])).
% 46.21/7.42 fof(f20855,plain,(
% 46.21/7.42 sub(c43442,name_1_1)),
% 46.21/7.42 inference(cnf_transformation,[status(thm)],[f10190])).
% 46.21/7.42 fof(f20856,plain,(
% 46.21/7.42 val(c43442,usa_0)),
% 46.21/7.42 inference(cnf_transformation,[status(thm)],[f10190])).
% 46.21/7.42 fof(f21264,definition,(
% 46.21/7.42 ![X0,X1]: (sQ0_spl <=> (~attr(X0,X1)|~sub(X1,name_1_1)|~val(X1,usa_0)))),
% 46.21/7.42 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 46.21/7.42 fof(f21265,plain,(
% 46.21/7.42 ![X0,X1]: (~attr(X0,X1)|~sub(X1,name_1_1)|~val(X1,usa_0)|~sQ0_spl)),
% 46.21/7.42 inference(component_clause,[status(thm)],[f21264])).
% 46.21/7.42 fof(f21267,definition,(
% 46.21/7.42 ![X2,X3]: (sQ1_spl <=> (~scar(X2,X3)))),
% 46.21/7.42 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 46.21/7.42 fof(f21268,plain,(
% 46.21/7.42 ![X0,X1]: (~scar(X0,X1)|~sQ1_spl)),
% 46.21/7.42 inference(component_clause,[status(thm)],[f21267])).
% 46.21/7.42 fof(f21270,plain,(
% 46.21/7.42 sQ0_spl|sQ1_spl),
% 46.21/7.42 inference(split_clause,[status(thm)],[f20817,f21264,f21267])).
% 46.21/7.42 fof(f21271,plain,(
% 46.21/7.42 ![X0]: (~attr(X0,c43442)|~val(c43442,usa_0)|~sQ0_spl)),
% 46.21/7.42 inference(resolution,[status(thm)],[f20855,f21265])).
% 46.21/7.42 fof(f21273,definition,(
% 46.21/7.42 ![X0]: (sQ2_spl <=> (~attr(X0,c43442)))),
% 46.21/7.42 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 46.21/7.42 fof(f21274,plain,(
% 46.21/7.42 ![X0]: (~attr(X0,c43442)|~sQ2_spl)),
% 46.21/7.42 inference(component_clause,[status(thm)],[f21273])).
% 46.21/7.42 fof(f21276,definition,(
% 46.21/7.42 sQ3_spl <=> (val(c43442,usa_0))),
% 46.21/7.42 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 46.21/7.42 fof(f21278,plain,(
% 46.21/7.42 ~val(c43442,usa_0)|sQ3_spl),
% 46.21/7.42 inference(component_clause,[status(thm)],[f21276])).
% 46.21/7.42 fof(f21279,plain,(
% 46.21/7.42 sQ2_spl|~sQ3_spl|~sQ0_spl),
% 46.21/7.42 inference(split_clause,[status(thm)],[f21271,f21273,f21276,f21264])).
% 46.21/7.42 fof(f21282,plain,(
% 46.21/7.42 ![X0,X1,X2]: (~attr(X0,X1)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X1,X2)|~sQ1_spl)),
% 46.21/7.42 inference(backward_subsumption_resolution,[status(thm)],[f10703,f21268])).
% 46.21/7.42 fof(f21291,plain,(
% 46.21/7.42 $false|sQ3_spl),
% 46.21/7.42 inference(forward_subsumption_resolution,[status(thm)],[f21278,f20856])).
% 46.21/7.42 fof(f21292,plain,(
% 46.21/7.42 sQ3_spl),
% 46.21/7.42 inference(contradiction_clause,[status(thm)],[f21291])).
% 46.21/7.42 fof(f21304,plain,(
% 46.21/7.42 $false|~sQ2_spl),
% 46.21/7.42 inference(backward_subsumption_resolution,[status(thm)],[f20853,f21274])).
% 46.21/7.42 fof(f21306,plain,(
% 46.21/7.42 ~sQ2_spl),
% 46.21/7.42 inference(contradiction_clause,[status(thm)],[f21304])).
% 46.21/7.42 fof(f21310,plain,(
% 46.21/7.42 ![X0,X1,X2]: (~member(X0,cons(familiename_1_1,cons(name_1_1,nil)))|~attr(X1,X2)|~sub(X2,X0)|~sQ1_spl)),
% 46.21/7.42 inference(resolution,[status(thm)],[f10194,f21282])).
% 46.21/7.42 fof(f21311,plain,(
% 46.21/7.42 ![X0]: (~member(name_1_1,cons(familiename_1_1,cons(name_1_1,nil)))|~attr(X0,c43442)|~sQ1_spl)),
% 46.21/7.42 inference(resolution,[status(thm)],[f21310,f20855])).
% 46.21/7.42 fof(f21312,definition,(
% 46.21/7.42 sQ4_spl <=> (member(name_1_1,cons(familiename_1_1,cons(name_1_1,nil))))),
% 46.21/7.42 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 46.21/7.42 fof(f21314,plain,(
% 46.21/7.42 ~member(name_1_1,cons(familiename_1_1,cons(name_1_1,nil)))|sQ4_spl),
% 46.21/7.42 inference(component_clause,[status(thm)],[f21312])).
% 46.21/7.42 fof(f21315,plain,(
% 46.21/7.42 ~sQ4_spl|sQ2_spl|~sQ1_spl),
% 46.21/7.42 inference(split_clause,[status(thm)],[f21311,f21312,f21273,f21267])).
% 46.21/7.42 fof(f21316,plain,(
% 46.21/7.42 ~member(name_1_1,cons(name_1_1,nil))|sQ4_spl),
% 46.21/7.42 inference(resolution,[status(thm)],[f21314,f10194])).
% 46.21/7.42 fof(f21317,plain,(
% 46.21/7.42 $false|sQ4_spl),
% 46.21/7.42 inference(forward_subsumption_resolution,[status(thm)],[f21316,f10191])).
% 46.21/7.42 fof(f21318,plain,(
% 46.21/7.42 sQ4_spl),
% 46.21/7.42 inference(contradiction_clause,[status(thm)],[f21317])).
% 46.21/7.42 fof(f21319,plain,(
% 46.21/7.42 $false),
% 46.21/7.42 inference(sat_refutation,[status(thm)],[f21270,f21279,f21292,f21306,f21315,f21318])).
% 46.21/7.42 % SZS output end CNFRefutation for theBenchmark.p
% 46.21/7.47 % Elapsed time: 7.109790 seconds
% 46.21/7.47 % CPU time: 54.863193 seconds
% 46.21/7.47 % Total memory used: 697.175 MB
% 46.21/7.47 % Net memory used: 638.436 MB
%------------------------------------------------------------------------------