%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR115+78 : 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 : n015.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:29 PM UTC 2026
% Result : Theorem 19.09s 2.93s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR115+78 : 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 : n015.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:10:51 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.21/0.48 % Drodi V4.1.1
% 19.09/2.93 % Refutation found
% 19.09/2.93 % SZS status Theorem for theBenchmark: Theorem is valid
% 19.09/2.93 % SZS output start CNFRefutation for theBenchmark
% 19.09/2.93 fof(f10188,conjecture,(
% 19.09/2.93 (? [X0,X1,X2,X3,X4,X5] :( attr(X2,X1)& attr(X4,X5)& obj(X3,X0)& sub(X0,firma_1_1)& sub(X1,name_1_1)& val(X1,bmw_0) ) )),
% 19.09/2.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.09/2.93 fof(f10189,negated_conjecture,(
% 19.09/2.93 ~((? [X0,X1,X2,X3,X4,X5] :( attr(X2,X1)& attr(X4,X5)& obj(X3,X0)& sub(X0,firma_1_1)& sub(X1,name_1_1)& val(X1,bmw_0) ) ))),
% 19.09/2.93 inference(negated_conjecture,[status(cth)],[f10188])).
% 19.09/2.93 fof(f10190,hypothesis,(
% 19.09/2.93 ( attr(c3868,c3869)& sub(c3868,erzeugnis_1_1)& sub(c3869,name_1_1)& val(c3869,mini_0)& attr(c4652,c4653)& sub(c4652,firma_1_1)& sub(c4653,name_1_1)& val(c4653,bmw_0)& pred(c48902,die_1_1)& sub(c48903,firma_1_1)& sub(c48916,sich_1_1)& attch(c48933,c48935)& attr(c48933,c48934)& sub(c48933,einrichtung_1_2)& sub(c48934,name_1_1)& val(c48934,mg_0)& sub(c48935,group_1_1)& attch(c48937,c48935)& attr(c48937,c48938)& sub(c48937,firma_1_1)& sub(c48938,name_1_1)& val(c48938,rover_0)& tupl_p5(c48992,c48902,c48903,c48916,c48935)& obj(c5513,c5557)& ornt(c5513,c5557)& semrel(c5513,c7)& subs(c5513,gehen_1_2)& attr(c5557,c5558)& attr(c5557,c5570)& sub(c5557,firma_1_1)& sub(c5557,land_1_1)& sub(c5558,name_1_1)& val(c5558,rover_0)& sub(c5570,name_1_1)& val(c5570,ford_0)& bei(c5573,c4652)& loc(c7,c5573)& scar(c7,c3868)& subs(c7,bleiben_1_2)& sort(c3868,co)& card(c3868,card_c)& etype(c3868,etype_c)& fact(c3868,real)& gener(c3868,sp)& quant(c3868,quant_c)& refer(c3868,det)& varia(c3868,con)& sort(c3869,na)& card(c3869,int1)& etype(c3869,int0)& fact(c3869,real)& gener(c3869,sp)& quant(c3869,one)& refer(c3869,indet)& varia(c3869,varia_c)& sort(erzeugnis_1_1,co)& card(erzeugnis_1_1,card_c)& etype(erzeugnis_1_1,etype_c)& fact(erzeugnis_1_1,real)& gener(erzeugnis_1_1,ge)& quant(erzeugnis_1_1,quant_c)& refer(erzeugnis_1_1,refer_c)& varia(erzeugnis_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(mini_0,fe)& sort(c4652,d)& sort(c4652,io)& card(c4652,int1)& etype(c4652,int0)& fact(c4652,real)& gener(c4652,sp)& quant(c4652,one)& refer(c4652,det)& varia(c4652,con)& sort(c4653,na)& card(c4653,int1)& etype(c4653,int0)& fact(c4653,real)& gener(c4653,sp)& quant(c4653,one)& refer(c4653,indet)& varia(c4653,varia_c)& sort(firma_1_1,d)& sort(firma_1_1,io)& card(firma_1_1,int1)& etype(firma_1_1,int0)& fact(firma_1_1,real)& gener(firma_1_1,ge)& quant(firma_1_1,one)& refer(firma_1_1,refer_c)& varia(firma_1_1,varia_c)& sort(bmw_0,fe)& sort(c48902,o)& card(c48902,int2000)& etype(c48902,int1)& fact(c48902,real)& gener(c48902,gener_c)& quant(c48902,nfquant)& refer(c48902,refer_c)& varia(c48902,varia_c)& sort(die_1_1,o)& card(die_1_1,int1)& etype(die_1_1,int0)& fact(die_1_1,real)& gener(die_1_1,ge)& quant(die_1_1,one)& refer(die_1_1,refer_c)& varia(die_1_1,varia_c)& sort(c48903,d)& sort(c48903,io)& card(c48903,int1)& etype(c48903,int0)& fact(c48903,real)& gener(c48903,gener_c)& quant(c48903,one)& refer(c48903,refer_c)& varia(c48903,varia_c)& sort(c48916,o)& card(c48916,int1)& etype(c48916,int0)& fact(c48916,real)& gener(c48916,gener_c)& quant(c48916,one)& refer(c48916,refer_c)& varia(c48916,varia_c)& sort(sich_1_1,o)& card(sich_1_1,int1)& etype(sich_1_1,int0)& fact(sich_1_1,real)& gener(sich_1_1,gener_c)& quant(sich_1_1,one)& refer(sich_1_1,refer_c)& varia(sich_1_1,varia_c)& sort(c48933,d)& sort(c48933,io)& card(c48933,int1)& etype(c48933,int1)& fact(c48933,real)& gener(c48933,sp)& quant(c48933,one)& refer(c48933,det)& varia(c48933,con)& sort(c48935,o)& card(c48935,int1)& etype(c48935,int0)& fact(c48935,real)& gener(c48935,sp)& quant(c48935,one)& refer(c48935,det)& varia(c48935,varia_c)& sort(c48934,na)& card(c48934,int1)& etype(c48934,int0)& fact(c48934,real)& gener(c48934,sp)& quant(c48934,one)& refer(c48934,indet)& varia(c48934,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(mg_0,fe)& sort(group_1_1,o)& card(group_1_1,int1)& etype(group_1_1,int0)& fact(group_1_1,real)& gener(group_1_1,ge)& quant(group_1_1,one)& refer(group_1_1,refer_c)& varia(group_1_1,varia_c)& sort(c48937,d)& sort(c48937,io)& card(c48937,int1)& etype(c48937,int0)& fact(c48937,real)& gener(c48937,sp)& quant(c48937,one)& refer(c48937,det)& varia(c48937,con)& sort(c48938,na)& card(c48938,int1)& etype(c48938,int0)& fact(c48938,real)& gener(c48938,sp)& quant(c48938,one)& refer(c48938,indet)& varia(c48938,varia_c)& sort(rover_0,fe)& sort(c48992,ent)& card(c48992,card_c)& etype(c48992,etype_c)& fact(c48992,real)& gener(c48992,gener_c)& quant(c48992,quant_c)& refer(c48992,refer_c)& varia(c48992,varia_c)& sort(c5513,dn)& fact(c5513,real)& gener(c5513,sp)& sort(c5557,d)& sort(c5557,io)& card(c5557,int1)& etype(c5557,int0)& fact(c5557,real)& gener(c5557,sp)& quant(c5557,one)& refer(c5557,det)& varia(c5557,varia_c)& sort(c7,st)& fact(c7,real)& gener(c7,sp)& sort(gehen_1_2,dn)& fact(gehen_1_2,real)& gener(gehen_1_2,ge)& sort(c5558,na)& card(c5558,int1)& etype(c5558,int0)& fact(c5558,real)& gener(c5558,sp)& quant(c5558,one)& refer(c5558,det)& varia(c5558,varia_c)& sort(c5570,na)& card(c5570,int1)& etype(c5570,int0)& fact(c5570,real)& gener(c5570,sp)& quant(c5570,one)& refer(c5570,indet)& varia(c5570,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(ford_0,fe)& sort(c5573,l)& card(c5573,int1)& etype(c5573,int0)& fact(c5573,real)& gener(c5573,sp)& quant(c5573,one)& refer(c5573,det)& varia(c5573,con)& sort(bleiben_1_2,st)& fact(bleiben_1_2,real)& gener(bleiben_1_2,ge) ) ),
% 19.09/2.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.09/2.93 fof(f20815,plain,(
% 19.09/2.93 (![X0,X1,X2,X3,X4,X5]: (((((~attr(X2,X1)|~attr(X4,X5))|~obj(X3,X0))|~sub(X0,firma_1_1))|~sub(X1,name_1_1))|~val(X1,bmw_0)))),
% 19.09/2.93 inference(pre_NNF_transformation,[status(thm)],[f10189])).
% 19.09/2.93 fof(f20816,plain,(
% 19.09/2.93 ![X1]: (((![X0]: ((((![X2]: ~attr(X2,X1))|(![X4,X5]: ~attr(X4,X5)))|(![X3]: ~obj(X3,X0)))|~sub(X0,firma_1_1)))|~sub(X1,name_1_1))|~val(X1,bmw_0))),
% 19.09/2.93 inference(miniscoping,[status(thm)],[f20815])).
% 19.09/2.93 fof(f20817,plain,(
% 19.09/2.93 ![X0,X1,X2,X3,X4,X5]: (~attr(X0,X1)|~attr(X2,X3)|~obj(X4,X5)|~sub(X5,firma_1_1)|~sub(X1,name_1_1)|~val(X1,bmw_0))),
% 19.09/2.93 inference(cnf_transformation,[status(thm)],[f20816])).
% 19.09/2.93 fof(f20822,plain,(
% 19.09/2.93 attr(c4652,c4653)),
% 19.09/2.93 inference(cnf_transformation,[status(thm)],[f10190])).
% 19.09/2.93 fof(f20824,plain,(
% 19.09/2.93 sub(c4653,name_1_1)),
% 19.09/2.93 inference(cnf_transformation,[status(thm)],[f10190])).
% 19.09/2.93 fof(f20825,plain,(
% 19.09/2.93 val(c4653,bmw_0)),
% 19.09/2.93 inference(cnf_transformation,[status(thm)],[f10190])).
% 19.09/2.93 fof(f20841,plain,(
% 19.09/2.93 obj(c5513,c5557)),
% 19.09/2.93 inference(cnf_transformation,[status(thm)],[f10190])).
% 19.09/2.93 fof(f20845,plain,(
% 19.09/2.93 attr(c5557,c5558)),
% 19.09/2.93 inference(cnf_transformation,[status(thm)],[f10190])).
% 19.09/2.93 fof(f20847,plain,(
% 19.09/2.93 sub(c5557,firma_1_1)),
% 19.09/2.93 inference(cnf_transformation,[status(thm)],[f10190])).
% 19.09/2.93 fof(f21117,definition,(
% 19.09/2.93 ![X0,X1]: (sQ0_spl <=> (~attr(X0,X1)|~sub(X1,name_1_1)|~val(X1,bmw_0)))),
% 19.09/2.93 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 19.09/2.93 fof(f21118,plain,(
% 19.09/2.93 ![X0,X1]: (~attr(X0,X1)|~sub(X1,name_1_1)|~val(X1,bmw_0)|~sQ0_spl)),
% 19.09/2.93 inference(component_clause,[status(thm)],[f21117])).
% 19.09/2.93 fof(f21120,definition,(
% 19.09/2.93 ![X2,X3]: (sQ1_spl <=> (~attr(X2,X3)))),
% 19.09/2.93 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 19.09/2.93 fof(f21121,plain,(
% 19.09/2.93 ![X0,X1]: (~attr(X0,X1)|~sQ1_spl)),
% 19.09/2.93 inference(component_clause,[status(thm)],[f21120])).
% 19.09/2.93 fof(f21123,definition,(
% 19.09/2.93 ![X4,X5]: (sQ2_spl <=> (~obj(X4,X5)|~sub(X5,firma_1_1)))),
% 19.09/2.93 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 19.09/2.93 fof(f21124,plain,(
% 19.09/2.93 ![X0,X1]: (~obj(X0,X1)|~sub(X1,firma_1_1)|~sQ2_spl)),
% 19.09/2.93 inference(component_clause,[status(thm)],[f21123])).
% 19.09/2.93 fof(f21126,plain,(
% 19.09/2.93 sQ0_spl|sQ1_spl|sQ2_spl),
% 19.09/2.99 inference(split_clause,[status(thm)],[f20817,f21117,f21120,f21123])).
% 19.09/2.99 fof(f21129,plain,(
% 19.09/2.99 ![X0]: (~obj(X0,c5557)|~sQ2_spl)),
% 19.09/2.99 inference(resolution,[status(thm)],[f20847,f21124])).
% 19.09/2.99 fof(f21156,plain,(
% 19.09/2.99 $false|~sQ2_spl),
% 19.09/2.99 inference(forward_subsumption_resolution,[status(thm)],[f20841,f21129])).
% 19.09/2.99 fof(f21157,plain,(
% 19.09/2.99 ~sQ2_spl),
% 19.09/2.99 inference(contradiction_clause,[status(thm)],[f21156])).
% 19.09/2.99 fof(f21162,plain,(
% 19.09/2.99 ![X0]: (~attr(X0,c4653)|~sub(c4653,name_1_1)|~sQ0_spl)),
% 19.09/2.99 inference(resolution,[status(thm)],[f21118,f20825])).
% 19.09/2.99 fof(f21163,definition,(
% 19.09/2.99 ![X0]: (sQ3_spl <=> (~attr(X0,c4653)))),
% 19.09/2.99 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 19.09/2.99 fof(f21164,plain,(
% 19.09/2.99 ![X0]: (~attr(X0,c4653)|~sQ3_spl)),
% 19.09/2.99 inference(component_clause,[status(thm)],[f21163])).
% 19.09/2.99 fof(f21166,definition,(
% 19.09/2.99 sQ4_spl <=> (sub(c4653,name_1_1))),
% 19.09/2.99 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 19.09/2.99 fof(f21168,plain,(
% 19.09/2.99 ~sub(c4653,name_1_1)|sQ4_spl),
% 19.09/2.99 inference(component_clause,[status(thm)],[f21166])).
% 19.09/2.99 fof(f21169,plain,(
% 19.09/2.99 sQ3_spl|~sQ4_spl|~sQ0_spl),
% 19.09/2.99 inference(split_clause,[status(thm)],[f21162,f21163,f21166,f21117])).
% 19.09/2.99 fof(f21170,plain,(
% 19.09/2.99 $false|sQ4_spl),
% 19.09/2.99 inference(forward_subsumption_resolution,[status(thm)],[f21168,f20824])).
% 19.09/2.99 fof(f21171,plain,(
% 19.09/2.99 sQ4_spl),
% 19.09/2.99 inference(contradiction_clause,[status(thm)],[f21170])).
% 19.09/2.99 fof(f21172,plain,(
% 19.09/2.99 $false|~sQ1_spl),
% 19.09/2.99 inference(backward_subsumption_resolution,[status(thm)],[f20845,f21121])).
% 19.09/2.99 fof(f21174,plain,(
% 19.09/2.99 ~sQ1_spl),
% 19.09/2.99 inference(contradiction_clause,[status(thm)],[f21172])).
% 19.09/2.99 fof(f21211,plain,(
% 19.09/2.99 $false|~sQ3_spl),
% 19.09/2.99 inference(forward_subsumption_resolution,[status(thm)],[f20822,f21164])).
% 19.09/2.99 fof(f21212,plain,(
% 19.09/2.99 ~sQ3_spl),
% 19.09/2.99 inference(contradiction_clause,[status(thm)],[f21211])).
% 19.09/2.99 fof(f21213,plain,(
% 19.09/2.99 $false),
% 19.09/2.99 inference(sat_refutation,[status(thm)],[f21126,f21157,f21169,f21171,f21174,f21212])).
% 19.09/2.99 % SZS output end CNFRefutation for theBenchmark.p
% 2.82/3.02 % Elapsed time: 2.657787 seconds
% 2.82/3.02 % CPU time: 19.540186 seconds
% 2.82/3.02 % Total memory used: 521.687 MB
% 2.82/3.02 % Net memory used: 515.300 MB
%------------------------------------------------------------------------------