%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR112+1 : 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 : n018.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:17 PM UTC 2026
% Result : Theorem 70.67s 9.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR112+1 : 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.09/0.36 % Computer : n018.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 15:04:44 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.22/0.49 % Drodi V4.1.1
% 70.67/9.49 % Refutation found
% 70.67/9.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 70.67/9.49 % SZS output start CNFRefutation for theBenchmark
% 70.67/9.49 fof(f1,axiom,(
% 70.67/9.49 (! [X0,X1] : member(X0,cons(X0,X1)) )),
% 70.67/9.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 70.67/9.49 fof(f2,axiom,(
% 70.67/9.49 (! [X0,X1,X2] :( member(X0,X2)=> member(X0,cons(X1,X2)) ) )),
% 70.67/9.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 70.67/9.49 fof(f159,axiom,(
% 70.67/9.49 (! [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) ) )) )),
% 70.67/9.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 70.67/9.49 fof(f10188,conjecture,(
% 70.67/9.49 (? [X0,X1,X2,X3,X4,X5,X6,X7] :( arg1(X4,X5)& arg2(X4,X0)& attr(X7,X6)& pred(X2,linie_1_1)& pred(X3,u1_1_1)& sub(X1,bahn_1_1)& sub(X6,name_1_1)& subs(X4,hei__337en_1_1)& val(X6,u2_0) ) )),
% 70.67/9.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 70.67/9.49 fof(f10189,negated_conjecture,(
% 70.67/9.49 ~((? [X0,X1,X2,X3,X4,X5,X6,X7] :( arg1(X4,X5)& arg2(X4,X0)& attr(X7,X6)& pred(X2,linie_1_1)& pred(X3,u1_1_1)& sub(X1,bahn_1_1)& sub(X6,name_1_1)& subs(X4,hei__337en_1_1)& val(X6,u2_0) ) ))),
% 70.67/9.49 inference(negated_conjecture,[status(cth)],[f10188])).
% 70.67/9.49 fof(f10190,hypothesis,(
% 70.67/9.49 ( sub(c5909,bahn_1_1)& pred(c5910,linie_1_1)& pred(c5912,u1_1_1)& attr(c5919,c5920)& sub(c5919,einrichtung_1_2)& sub(c5920,name_1_1)& val(c5920,u2_0)& pred(c5921,u3_1_1)& sub(c5932,abstand_1_1)& pred(c5937,minute_1_1)& tupl_p9(c6138,c5901,c5909,c5910,c5912,c5919,c5921,c5932,c5937)& sort(c5909,io)& card(c5909,int1)& etype(c5909,int0)& fact(c5909,real)& gener(c5909,gener_c)& quant(c5909,one)& refer(c5909,refer_c)& varia(c5909,varia_c)& sort(bahn_1_1,io)& card(bahn_1_1,int1)& etype(bahn_1_1,int0)& fact(bahn_1_1,real)& gener(bahn_1_1,ge)& quant(bahn_1_1,one)& refer(bahn_1_1,refer_c)& varia(bahn_1_1,varia_c)& sort(c5910,d)& sort(c5910,io)& card(c5910,cons(x_constant,cons(int1,nil)))& etype(c5910,int1)& fact(c5910,real)& gener(c5910,gener_c)& quant(c5910,mult)& refer(c5910,indet)& varia(c5910,varia_c)& sort(linie_1_1,d)& sort(linie_1_1,io)& card(linie_1_1,int1)& etype(linie_1_1,int0)& fact(linie_1_1,real)& gener(linie_1_1,ge)& quant(linie_1_1,one)& refer(linie_1_1,refer_c)& varia(linie_1_1,varia_c)& sort(c5912,o)& card(c5912,cons(x_constant,cons(int1,nil)))& etype(c5912,int1)& fact(c5912,real)& gener(c5912,gener_c)& quant(c5912,mult)& refer(c5912,indet)& varia(c5912,varia_c)& sort(u1_1_1,o)& card(u1_1_1,int1)& etype(u1_1_1,int0)& fact(u1_1_1,real)& gener(u1_1_1,ge)& quant(u1_1_1,one)& refer(u1_1_1,refer_c)& varia(u1_1_1,varia_c)& sort(c5919,d)& sort(c5919,io)& card(c5919,int1)& etype(c5919,int1)& fact(c5919,real)& gener(c5919,sp)& quant(c5919,one)& refer(c5919,det)& varia(c5919,con)& sort(c5920,na)& card(c5920,int1)& etype(c5920,int0)& fact(c5920,real)& gener(c5920,sp)& quant(c5920,one)& refer(c5920,indet)& varia(c5920,varia_c)& sort(einrichtung_1_2,d)& sort(einrichtung_1_2,io)& card(einrichtung_1_2,card_c)& etype(einrichtung_1_2,int1)& fact(einrichtung_1_2,real)& gener(einrichtung_1_2,ge)& quant(einrichtung_1_2,quant_c)& refer(einrichtung_1_2,refer_c)& varia(einrichtung_1_2,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(u2_0,fe)& sort(c5921,o)& card(c5921,cons(x_constant,cons(int1,nil)))& etype(c5921,int1)& fact(c5921,real)& gener(c5921,gener_c)& quant(c5921,mult)& refer(c5921,indet)& varia(c5921,varia_c)& sort(u3_1_1,o)& card(u3_1_1,int1)& etype(u3_1_1,int0)& fact(u3_1_1,real)& gener(u3_1_1,ge)& quant(u3_1_1,one)& refer(u3_1_1,refer_c)& varia(u3_1_1,varia_c)& sort(c5932,io)& sort(c5932,na)& card(c5932,int1)& etype(c5932,int0)& fact(c5932,real)& gener(c5932,sp)& quant(c5932,one)& refer(c5932,det)& varia(c5932,con)& sort(abstand_1_1,io)& sort(abstand_1_1,na)& card(abstand_1_1,int1)& etype(abstand_1_1,int0)& fact(abstand_1_1,real)& gener(abstand_1_1,ge)& quant(abstand_1_1,one)& refer(abstand_1_1,refer_c)& varia(abstand_1_1,varia_c)& sort(c5937,me)& sort(c5937,oa)& sort(c5937,ta)& card(c5937,card_c)& etype(c5937,etype_c)& fact(c5937,real)& gener(c5937,gener_c)& quant(c5937,quant_c)& refer(c5937,refer_c)& varia(c5937,varia_c)& sort(minute_1_1,me)& sort(minute_1_1,oa)& sort(minute_1_1,ta)& card(minute_1_1,card_c)& etype(minute_1_1,etype_c)& fact(minute_1_1,real)& gener(minute_1_1,ge)& quant(minute_1_1,quant_c)& refer(minute_1_1,refer_c)& varia(minute_1_1,varia_c)& sort(c6138,ent)& card(c6138,card_c)& etype(c6138,etype_c)& fact(c6138,real)& gener(c6138,gener_c)& quant(c6138,quant_c)& refer(c6138,refer_c)& varia(c6138,varia_c)& sort(c5901,o)& card(c5901,int1)& etype(c5901,int0)& fact(c5901,real)& gener(c5901,sp)& quant(c5901,one)& refer(c5901,det)& varia(c5901,varia_c) ) ),
% 70.67/9.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 70.67/9.50 fof(f10191,plain,(
% 70.67/9.50 ![X0,X1]: (member(X0,cons(X0,X1)))),
% 70.67/9.50 inference(cnf_transformation,[status(thm)],[f1])).
% 70.67/9.50 fof(f10192,plain,(
% 70.67/9.50 ![X0,X1,X2]: (~member(X0,X2)|member(X0,cons(X1,X2)))),
% 70.67/9.50 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 70.67/9.50 fof(f10193,plain,(
% 70.67/9.50 ![X0,X2]: (~member(X0,X2)|(![X1]: member(X0,cons(X1,X2))))),
% 70.67/9.50 inference(miniscoping,[status(thm)],[f10192])).
% 70.67/9.50 fof(f10194,plain,(
% 70.67/9.50 ![X0,X1,X2]: (~member(X0,X1)|member(X0,cons(X2,X1)))),
% 70.67/9.50 inference(cnf_transformation,[status(thm)],[f10193])).
% 70.67/9.50 fof(f10692,plain,(
% 70.67/9.50 ![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))))),
% 70.67/9.50 inference(pre_NNF_transformation,[status(thm)],[f159])).
% 70.67/9.50 fof(f10693,plain,(
% 70.67/9.50 ![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))))),
% 70.67/9.50 inference(miniscoping,[status(thm)],[f10692])).
% 70.67/9.50 fof(f10694,plain,(
% 70.67/9.50 ![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)))),
% 70.67/9.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK50_skl]),skolemize(X3,sK50_skl(X2))],[f10693])).
% 70.67/9.50 fof(f10695,plain,(
% 70.67/9.50 ![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))),
% 70.67/9.50 inference(cnf_transformation,[status(thm)],[f10694])).
% 70.67/9.50 fof(f10696,plain,(
% 70.67/9.50 ![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))),
% 70.67/9.50 inference(cnf_transformation,[status(thm)],[f10694])).
% 70.67/9.50 fof(f10697,plain,(
% 70.67/9.50 ![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))),
% 70.67/9.50 inference(cnf_transformation,[status(thm)],[f10694])).
% 70.67/9.50 fof(f20815,plain,(
% 70.67/9.50 (![X0,X1,X2,X3,X4,X5,X6,X7]: ((((((((~arg1(X4,X5)|~arg2(X4,X0))|~attr(X7,X6))|~pred(X2,linie_1_1))|~pred(X3,u1_1_1))|~sub(X1,bahn_1_1))|~sub(X6,name_1_1))|~subs(X4,hei__337en_1_1))|~val(X6,u2_0)))),
% 70.67/9.50 inference(pre_NNF_transformation,[status(thm)],[f10189])).
% 70.67/9.50 fof(f20816,plain,(
% 70.67/9.50 ![X6]: ((![X4]: ((((((((![X5]: ~arg1(X4,X5))|(![X0]: ~arg2(X4,X0)))|(![X7]: ~attr(X7,X6)))|(![X2]: ~pred(X2,linie_1_1)))|(![X3]: ~pred(X3,u1_1_1)))|(![X1]: ~sub(X1,bahn_1_1)))|~sub(X6,name_1_1))|~subs(X4,hei__337en_1_1)))|~val(X6,u2_0))),
% 70.67/9.50 inference(miniscoping,[status(thm)],[f20815])).
% 70.67/9.50 fof(f20817,plain,(
% 70.67/9.50 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~arg1(X0,X1)|~arg2(X0,X2)|~attr(X3,X4)|~pred(X5,linie_1_1)|~pred(X6,u1_1_1)|~sub(X7,bahn_1_1)|~sub(X4,name_1_1)|~subs(X0,hei__337en_1_1)|~val(X4,u2_0))),
% 70.67/9.50 inference(cnf_transformation,[status(thm)],[f20816])).
% 70.67/9.50 fof(f20818,plain,(
% 70.67/9.50 sub(c5909,bahn_1_1)),
% 70.67/9.50 inference(cnf_transformation,[status(thm)],[f10190])).
% 70.67/9.50 fof(f20819,plain,(
% 70.67/9.50 pred(c5910,linie_1_1)),
% 70.67/9.50 inference(cnf_transformation,[status(thm)],[f10190])).
% 70.67/9.50 fof(f20820,plain,(
% 70.67/9.50 pred(c5912,u1_1_1)),
% 70.67/9.50 inference(cnf_transformation,[status(thm)],[f10190])).
% 70.67/9.50 fof(f20821,plain,(
% 70.67/9.50 attr(c5919,c5920)),
% 70.67/9.50 inference(cnf_transformation,[status(thm)],[f10190])).
% 70.67/9.50 fof(f20823,plain,(
% 70.67/9.50 sub(c5920,name_1_1)),
% 70.67/9.50 inference(cnf_transformation,[status(thm)],[f10190])).
% 70.67/9.50 fof(f20824,plain,(
% 70.67/9.50 val(c5920,u2_0)),
% 70.67/9.50 inference(cnf_transformation,[status(thm)],[f10190])).
% 70.67/9.50 fof(f21019,definition,(
% 70.67/9.50 ![X0,X1,X2]: (sQ0_spl <=> (~arg1(X0,X1)|~arg2(X0,X2)|~subs(X0,hei__337en_1_1)))),
% 70.67/9.50 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 70.67/9.50 fof(f21020,plain,(
% 70.67/9.50 ![X0,X1,X2]: (~arg1(X0,X1)|~arg2(X0,X2)|~subs(X0,hei__337en_1_1)|~sQ0_spl)),
% 70.67/9.50 inference(component_clause,[status(thm)],[f21019])).
% 70.67/9.50 fof(f21022,definition,(
% 70.67/9.50 ![X3,X4]: (sQ1_spl <=> (~attr(X3,X4)|~sub(X4,name_1_1)|~val(X4,u2_0)))),
% 70.67/9.50 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 70.67/9.50 fof(f21023,plain,(
% 70.67/9.50 ![X0,X1]: (~attr(X0,X1)|~sub(X1,name_1_1)|~val(X1,u2_0)|~sQ1_spl)),
% 70.67/9.50 inference(component_clause,[status(thm)],[f21022])).
% 70.67/9.50 fof(f21025,definition,(
% 70.67/9.50 ![X5]: (sQ2_spl <=> (~pred(X5,linie_1_1)))),
% 70.67/9.50 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 70.67/9.50 fof(f21026,plain,(
% 70.67/9.50 ![X0]: (~pred(X0,linie_1_1)|~sQ2_spl)),
% 70.67/9.50 inference(component_clause,[status(thm)],[f21025])).
% 70.67/9.50 fof(f21028,definition,(
% 70.67/9.50 ![X6]: (sQ3_spl <=> (~pred(X6,u1_1_1)))),
% 70.67/9.50 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 70.67/9.50 fof(f21029,plain,(
% 70.67/9.50 ![X0]: (~pred(X0,u1_1_1)|~sQ3_spl)),
% 70.67/9.50 inference(component_clause,[status(thm)],[f21028])).
% 70.67/9.50 fof(f21031,definition,(
% 70.67/9.50 ![X7]: (sQ4_spl <=> (~sub(X7,bahn_1_1)))),
% 70.67/9.50 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 70.67/9.50 fof(f21032,plain,(
% 70.67/9.50 ![X0]: (~sub(X0,bahn_1_1)|~sQ4_spl)),
% 70.67/9.50 inference(component_clause,[status(thm)],[f21031])).
% 70.67/9.50 fof(f21034,plain,(
% 70.67/9.50 sQ0_spl|sQ1_spl|sQ2_spl|sQ3_spl|sQ4_spl),
% 70.67/9.50 inference(split_clause,[status(thm)],[f20817,f21019,f21022,f21025,f21028,f21031])).
% 70.67/9.50 fof(f21035,plain,(
% 70.67/9.50 $false|~sQ4_spl),
% 70.67/9.50 inference(backward_subsumption_resolution,[status(thm)],[f20818,f21032])).
% 70.67/9.50 fof(f21036,plain,(
% 70.67/9.50 ~sQ4_spl),
% 70.67/9.50 inference(contradiction_clause,[status(thm)],[f21035])).
% 70.67/9.50 fof(f21037,plain,(
% 70.67/9.50 $false|~sQ3_spl),
% 70.67/9.50 inference(backward_subsumption_resolution,[status(thm)],[f20820,f21029])).
% 70.67/9.50 fof(f21038,plain,(
% 70.67/9.50 ~sQ3_spl),
% 70.67/9.50 inference(contradiction_clause,[status(thm)],[f21037])).
% 70.67/9.50 fof(f21039,plain,(
% 70.67/9.50 $false|~sQ2_spl),
% 70.67/9.50 inference(backward_subsumption_resolution,[status(thm)],[f20819,f21026])).
% 70.67/9.50 fof(f21040,plain,(
% 70.67/9.50 ~sQ2_spl),
% 70.67/9.50 inference(contradiction_clause,[status(thm)],[f21039])).
% 70.67/9.50 fof(f21046,definition,(
% 70.67/9.50 sQ5_spl <=> (sub(c5920,name_1_1))),
% 70.67/9.50 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 70.67/9.50 fof(f21048,plain,(
% 70.67/9.50 ~sub(c5920,name_1_1)|sQ5_spl),
% 70.67/9.50 inference(component_clause,[status(thm)],[f21046])).
% 70.67/9.50 fof(f21053,plain,(
% 70.67/9.50 $false|sQ5_spl),
% 70.67/9.50 inference(forward_subsumption_resolution,[status(thm)],[f21048,f20823])).
% 70.67/9.50 fof(f21054,plain,(
% 70.67/9.50 sQ5_spl),
% 70.67/9.50 inference(contradiction_clause,[status(thm)],[f21053])).
% 70.67/9.50 fof(f21245,definition,(
% 70.67/9.50 ![X4]: (sQ9_spl <=> (~member(X4,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(c5920,X4)))),
% 70.67/9.50 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 70.67/9.50 fof(f21246,plain,(
% 70.67/9.50 ![X0]: (~member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(c5920,X0)|~sQ9_spl)),
% 70.67/9.50 inference(component_clause,[status(thm)],[f21245])).
% 70.67/9.50 fof(f21249,plain,(
% 70.67/9.50 ![X0]: (~attr(X0,c5920)|~sub(c5920,name_1_1)|~sQ1_spl)),
% 70.67/9.50 inference(resolution,[status(thm)],[f21023,f20824])).
% 70.67/9.50 fof(f21250,definition,(
% 70.67/9.50 ![X0]: (sQ10_spl <=> (~attr(X0,c5920)))),
% 70.67/9.50 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 70.67/9.50 fof(f21251,plain,(
% 70.67/9.50 ![X0]: (~attr(X0,c5920)|~sQ10_spl)),
% 70.67/9.50 inference(component_clause,[status(thm)],[f21250])).
% 70.67/9.50 fof(f21253,plain,(
% 70.67/9.50 sQ10_spl|~sQ5_spl|~sQ1_spl),
% 70.67/9.50 inference(split_clause,[status(thm)],[f21249,f21250,f21046,f21022])).
% 70.67/9.50 fof(f21254,plain,(
% 70.67/9.50 $false|~sQ10_spl),
% 70.67/9.50 inference(backward_subsumption_resolution,[status(thm)],[f20821,f21251])).
% 70.67/9.50 fof(f21255,plain,(
% 70.67/9.50 ~sQ10_spl),
% 70.67/9.50 inference(contradiction_clause,[status(thm)],[f21254])).
% 70.67/9.50 fof(f21257,plain,(
% 70.67/9.50 ![X0,X1,X2,X3]: (~arg2(sK50_skl(X0),X1)|~subs(sK50_skl(X0),hei__337en_1_1)|~attr(X0,X2)|~member(X3,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X2,X3)|~sQ0_spl)),
% 71.40/9.56 inference(resolution,[status(thm)],[f21020,f10695])).
% 71.40/9.56 fof(f21258,plain,(
% 71.40/9.56 ![X0,X1,X2]: (~attr(X0,X1)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X1,X2)|~sQ0_spl)),
% 71.40/9.56 inference(backward_subsumption_resolution,[status(thm)],[f10696,f21259])).
% 71.40/9.56 fof(f21259,plain,(
% 71.40/9.56 ![X0,X1,X2,X3]: (~arg2(sK50_skl(X0),X1)|~attr(X0,X2)|~member(X3,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(X2,X3)|~sQ0_spl)),
% 71.40/9.56 inference(forward_subsumption_resolution,[status(thm)],[f21257,f10697])).
% 71.40/9.56 fof(f21260,plain,(
% 71.40/9.56 ![X0]: (~sub(c5920,X0)|~member(X0,cons(familiename_1_1,cons(name_1_1,nil)))|~sQ9_spl)),
% 71.40/9.56 inference(resolution,[status(thm)],[f21246,f10194])).
% 71.40/9.56 fof(f21262,plain,(
% 71.40/9.56 ![X0]: (~sub(c5920,X0)|~member(X0,cons(name_1_1,nil))|~sQ9_spl)),
% 71.40/9.56 inference(resolution,[status(thm)],[f21260,f10194])).
% 71.40/9.56 fof(f21265,plain,(
% 71.40/9.56 ~sub(c5920,name_1_1)|~sQ9_spl),
% 71.40/9.56 inference(resolution,[status(thm)],[f21262,f10191])).
% 71.40/9.56 fof(f21266,plain,(
% 71.40/9.56 ~sQ5_spl|~sQ9_spl),
% 71.40/9.56 inference(split_clause,[status(thm)],[f21265,f21046,f21245])).
% 71.40/9.56 fof(f21308,plain,(
% 71.40/9.56 ![X0]: (~member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))|~sub(c5920,X0)|~sQ0_spl)),
% 71.40/9.56 inference(resolution,[status(thm)],[f20821,f21258])).
% 71.40/9.56 fof(f21310,plain,(
% 71.40/9.56 sQ9_spl|~sQ0_spl),
% 71.40/9.56 inference(split_clause,[status(thm)],[f21308,f21245,f21019])).
% 71.40/9.56 fof(f21312,plain,(
% 71.40/9.56 $false),
% 71.40/9.56 inference(sat_refutation,[status(thm)],[f21034,f21036,f21038,f21040,f21054,f21253,f21255,f21266,f21310])).
% 71.40/9.56 % SZS output end CNFRefutation for theBenchmark.p
% 4.25/9.61 % Elapsed time: 9.233024 seconds
% 4.25/9.61 % CPU time: 71.724894 seconds
% 4.25/9.61 % Total memory used: 631.182 MB
% 4.25/9.61 % Net memory used: 603.558 MB
%------------------------------------------------------------------------------