%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR115+66 : 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:27 PM UTC 2026
% Result : Theorem 31.00s 4.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR115+66 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.34 % Computer : n003.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Mon Sep 21 15:08:46 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.23/0.48 % Drodi V4.1.1
% 31.00/4.43 % Refutation found
% 31.00/4.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 31.00/4.43 % SZS output start CNFRefutation for theBenchmark
% 31.00/4.43 fof(f20,axiom,(
% 31.00/4.43 (! [X0,X1] :( card(X0,X1)=> has_card_leq(X0,X1) ) )),
% 31.00/4.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.00/4.43 fof(f10188,conjecture,(
% 31.00/4.43 (? [X0,X1,X2,X3,X4,X5,X6] :( agt(X3,X2)& attr(X2,X1)& attr(X4,X5)& has_card_leq(X6,int1994)& sub(X0,firma_1_1)& sub(X1,name_1_1)& sub(X5,jahr__1_1)& subs(X3,n374bernehmen_1_1)& temp(X3,X4)& val(X1,bmw_0)& val(X5,X6) ) )),
% 31.00/4.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.00/4.43 fof(f10189,negated_conjecture,(
% 31.00/4.43 ~((? [X0,X1,X2,X3,X4,X5,X6] :( agt(X3,X2)& attr(X2,X1)& attr(X4,X5)& has_card_leq(X6,int1994)& sub(X0,firma_1_1)& sub(X1,name_1_1)& sub(X5,jahr__1_1)& subs(X3,n374bernehmen_1_1)& temp(X3,X4)& val(X1,bmw_0)& val(X5,X6) ) ))),
% 31.00/4.43 inference(negated_conjecture,[status(cth)],[f10188])).
% 31.00/4.43 fof(f10190,hypothesis,(
% 31.00/4.43 ( assoc(autobauer_1_1,automobil_1_1)& sub(autobauer_1_1,fabrikant_1_1)& attr(c103,c104)& prop(c103,britisch__1_1)& sub(c103,autobauer_1_1)& sub(c104,name_1_1)& val(c104,rover_0)& agt(c3,c86)& obj(c3,c103)& subs(c3,n374bernehmen_1_1)& temp(c3,c4)& attr(c4,c5)& sub(c5,jahr__1_1)& val(c5,c1)& attr(c86,c87)& sub(c86,firma_1_1)& sub(c87,name_1_1)& val(c87,bmw_0)& sort(autobauer_1_1,d)& sort(autobauer_1_1,io)& card(autobauer_1_1,int1)& etype(autobauer_1_1,int0)& fact(autobauer_1_1,real)& gener(autobauer_1_1,ge)& quant(autobauer_1_1,one)& refer(autobauer_1_1,refer_c)& varia(autobauer_1_1,varia_c)& sort(automobil_1_1,tq)& sort(fabrikant_1_1,d)& sort(fabrikant_1_1,io)& card(fabrikant_1_1,int1)& etype(fabrikant_1_1,int0)& fact(fabrikant_1_1,real)& gener(fabrikant_1_1,ge)& quant(fabrikant_1_1,one)& refer(fabrikant_1_1,refer_c)& varia(fabrikant_1_1,varia_c)& sort(c103,d)& sort(c103,io)& card(c103,int1)& etype(c103,int0)& fact(c103,real)& gener(c103,sp)& quant(c103,one)& refer(c103,det)& varia(c103,con)& sort(c104,na)& card(c104,int1)& etype(c104,int0)& fact(c104,real)& gener(c104,sp)& quant(c104,one)& refer(c104,indet)& varia(c104,varia_c)& sort(britisch__1_1,nq)& 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(rover_0,fe)& sort(c3,da)& fact(c3,real)& gener(c3,sp)& sort(c86,d)& sort(c86,io)& card(c86,int1)& etype(c86,int0)& fact(c86,real)& gener(c86,sp)& quant(c86,one)& refer(c86,det)& varia(c86,con)& sort(n374bernehmen_1_1,da)& fact(n374bernehmen_1_1,real)& gener(n374bernehmen_1_1,ge)& sort(c4,t)& card(c4,int1)& etype(c4,int0)& fact(c4,real)& gener(c4,sp)& quant(c4,one)& refer(c4,det)& varia(c4,con)& sort(c5,me)& sort(c5,oa)& sort(c5,ta)& card(c5,card_c)& etype(c5,etype_c)& fact(c5,real)& gener(c5,sp)& quant(c5,quant_c)& refer(c5,refer_c)& varia(c5,varia_c)& sort(jahr__1_1,me)& sort(jahr__1_1,oa)& sort(jahr__1_1,ta)& card(jahr__1_1,card_c)& etype(jahr__1_1,etype_c)& fact(jahr__1_1,real)& gener(jahr__1_1,ge)& quant(jahr__1_1,quant_c)& refer(jahr__1_1,refer_c)& varia(jahr__1_1,varia_c)& sort(c1,nu)& card(c1,int1994)& sort(c87,na)& card(c87,int1)& etype(c87,int0)& fact(c87,real)& gener(c87,sp)& quant(c87,one)& refer(c87,indet)& varia(c87,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) ) ),
% 31.00/4.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.00/4.43 fof(f10224,plain,(
% 31.00/4.43 ![X0,X1]: (~card(X0,X1)|has_card_leq(X0,X1))),
% 31.00/4.43 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 31.00/4.43 fof(f10225,plain,(
% 31.00/4.43 ![X0,X1]: (~card(X0,X1)|has_card_leq(X0,X1))),
% 31.00/4.43 inference(cnf_transformation,[status(thm)],[f10224])).
% 31.00/4.43 fof(f20815,plain,(
% 31.00/4.43 (![X0,X1,X2,X3,X4,X5,X6]: ((((((((((~agt(X3,X2)|~attr(X2,X1))|~attr(X4,X5))|~has_card_leq(X6,int1994))|~sub(X0,firma_1_1))|~sub(X1,name_1_1))|~sub(X5,jahr__1_1))|~subs(X3,n374bernehmen_1_1))|~temp(X3,X4))|~val(X1,bmw_0))|~val(X5,X6)))),
% 31.00/4.43 inference(pre_NNF_transformation,[status(thm)],[f10189])).
% 31.00/4.43 fof(f20816,plain,(
% 31.00/4.43 ![X5,X6]: ((![X1]: ((![X3,X4]: ((((((((![X2]: (~agt(X3,X2)|~attr(X2,X1)))|~attr(X4,X5))|~has_card_leq(X6,int1994))|(![X0]: ~sub(X0,firma_1_1)))|~sub(X1,name_1_1))|~sub(X5,jahr__1_1))|~subs(X3,n374bernehmen_1_1))|~temp(X3,X4)))|~val(X1,bmw_0)))|~val(X5,X6))),
% 31.00/4.43 inference(miniscoping,[status(thm)],[f20815])).
% 31.00/4.43 fof(f20817,plain,(
% 31.00/4.43 ![X0,X1,X2,X3,X4,X5,X6]: (~agt(X0,X1)|~attr(X1,X2)|~attr(X3,X4)|~has_card_leq(X5,int1994)|~sub(X6,firma_1_1)|~sub(X2,name_1_1)|~sub(X4,jahr__1_1)|~subs(X0,n374bernehmen_1_1)|~temp(X0,X3)|~val(X2,bmw_0)|~val(X4,X5))),
% 31.00/4.43 inference(cnf_transformation,[status(thm)],[f20816])).
% 31.00/4.43 fof(f20825,plain,(
% 31.00/4.43 agt(c3,c86)),
% 31.00/4.43 inference(cnf_transformation,[status(thm)],[f10190])).
% 31.00/4.43 fof(f20827,plain,(
% 31.00/4.43 subs(c3,n374bernehmen_1_1)),
% 31.00/4.43 inference(cnf_transformation,[status(thm)],[f10190])).
% 31.00/4.43 fof(f20828,plain,(
% 31.00/4.43 temp(c3,c4)),
% 31.00/4.43 inference(cnf_transformation,[status(thm)],[f10190])).
% 31.00/4.43 fof(f20829,plain,(
% 31.00/4.43 attr(c4,c5)),
% 31.00/4.43 inference(cnf_transformation,[status(thm)],[f10190])).
% 31.00/4.43 fof(f20830,plain,(
% 31.00/4.43 sub(c5,jahr__1_1)),
% 31.00/4.43 inference(cnf_transformation,[status(thm)],[f10190])).
% 31.00/4.43 fof(f20831,plain,(
% 31.00/4.43 val(c5,c1)),
% 31.00/4.43 inference(cnf_transformation,[status(thm)],[f10190])).
% 31.00/4.43 fof(f20832,plain,(
% 31.00/4.43 attr(c86,c87)),
% 31.00/4.43 inference(cnf_transformation,[status(thm)],[f10190])).
% 31.00/4.43 fof(f20833,plain,(
% 31.00/4.43 sub(c86,firma_1_1)),
% 31.00/4.43 inference(cnf_transformation,[status(thm)],[f10190])).
% 31.00/4.43 fof(f20834,plain,(
% 31.00/4.43 sub(c87,name_1_1)),
% 31.00/4.43 inference(cnf_transformation,[status(thm)],[f10190])).
% 31.00/4.43 fof(f20835,plain,(
% 31.00/4.43 val(c87,bmw_0)),
% 31.00/4.43 inference(cnf_transformation,[status(thm)],[f10190])).
% 31.00/4.43 fof(f20926,plain,(
% 31.00/4.43 card(c1,int1994)),
% 31.00/4.43 inference(cnf_transformation,[status(thm)],[f10190])).
% 31.00/4.43 fof(f20980,definition,(
% 31.00/4.43 ![X0,X1,X2,X3,X4,X5]: (sQ0_spl <=> (~agt(X0,X1)|~attr(X1,X2)|~attr(X3,X4)|~has_card_leq(X5,int1994)|~sub(X2,name_1_1)|~sub(X4,jahr__1_1)|~subs(X0,n374bernehmen_1_1)|~temp(X0,X3)|~val(X2,bmw_0)|~val(X4,X5)))),
% 31.00/4.43 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 31.00/4.43 fof(f20981,plain,(
% 31.00/4.43 ![X0,X1,X2,X3,X4,X5]: (~agt(X0,X1)|~attr(X1,X2)|~attr(X3,X4)|~has_card_leq(X5,int1994)|~sub(X2,name_1_1)|~sub(X4,jahr__1_1)|~subs(X0,n374bernehmen_1_1)|~temp(X0,X3)|~val(X2,bmw_0)|~val(X4,X5)|~sQ0_spl)),
% 31.00/4.43 inference(component_clause,[status(thm)],[f20980])).
% 31.00/4.43 fof(f20983,definition,(
% 31.00/4.43 ![X6]: (sQ1_spl <=> (~sub(X6,firma_1_1)))),
% 31.00/4.43 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 31.00/4.43 fof(f20984,plain,(
% 31.00/4.43 ![X0]: (~sub(X0,firma_1_1)|~sQ1_spl)),
% 31.00/4.43 inference(component_clause,[status(thm)],[f20983])).
% 31.00/4.43 fof(f20986,plain,(
% 31.00/4.43 sQ0_spl|sQ1_spl),
% 31.00/4.43 inference(split_clause,[status(thm)],[f20817,f20980,f20983])).
% 31.00/4.43 fof(f20995,plain,(
% 31.00/4.43 $false|~sQ1_spl),
% 31.00/4.43 inference(forward_subsumption_resolution,[status(thm)],[f20833,f20984])).
% 31.00/4.43 fof(f20996,plain,(
% 31.00/4.43 ~sQ1_spl),
% 31.00/4.43 inference(contradiction_clause,[status(thm)],[f20995])).
% 31.00/4.43 fof(f21007,definition,(
% 31.00/4.43 sQ5_spl <=> (sub(c87,name_1_1))),
% 31.00/4.43 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 31.00/4.43 fof(f21009,plain,(
% 31.00/4.43 ~sub(c87,name_1_1)|sQ5_spl),
% 31.00/4.43 inference(component_clause,[status(thm)],[f21007])).
% 31.00/4.43 fof(f21027,plain,(
% 31.00/4.43 has_card_leq(c1,int1994)),
% 31.00/4.43 inference(resolution,[status(thm)],[f10225,f20926])).
% 31.00/4.43 fof(f21039,definition,(
% 31.00/4.43 ![X0,X1]: (sQ10_spl <=> (~agt(c3,X0)|~attr(X0,X1)|~sub(X1,name_1_1)|~val(X1,bmw_0)))),
% 31.00/4.43 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 31.00/4.43 fof(f21040,plain,(
% 31.00/4.43 ![X0,X1]: (~agt(c3,X0)|~attr(X0,X1)|~sub(X1,name_1_1)|~val(X1,bmw_0)|~sQ10_spl)),
% 31.00/4.43 inference(component_clause,[status(thm)],[f21039])).
% 31.00/4.43 fof(f21045,definition,(
% 31.00/4.43 sQ12_spl <=> (subs(c3,n374bernehmen_1_1))),
% 31.00/4.43 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 31.00/4.43 fof(f21047,plain,(
% 31.00/4.43 ~subs(c3,n374bernehmen_1_1)|sQ12_spl),
% 31.00/4.43 inference(component_clause,[status(thm)],[f21045])).
% 31.00/4.43 fof(f21049,plain,(
% 31.00/4.43 $false|sQ12_spl),
% 31.00/4.43 inference(forward_subsumption_resolution,[status(thm)],[f21047,f20827])).
% 31.00/4.43 fof(f21050,plain,(
% 31.00/4.43 sQ12_spl),
% 31.00/4.43 inference(contradiction_clause,[status(thm)],[f21049])).
% 31.00/4.43 fof(f21052,plain,(
% 31.00/4.43 ![X0,X1,X2,X3]: (~agt(X0,X1)|~attr(X1,X2)|~has_card_leq(X3,int1994)|~sub(X2,name_1_1)|~sub(c5,jahr__1_1)|~subs(X0,n374bernehmen_1_1)|~temp(X0,c4)|~val(X2,bmw_0)|~val(c5,X3)|~sQ0_spl)),
% 31.00/4.53 inference(resolution,[status(thm)],[f20829,f20981])).
% 31.00/4.53 fof(f21058,definition,(
% 31.00/4.53 ![X1]: (sQ14_spl <=> (~has_card_leq(X1,int1994)|~val(c5,X1)))),
% 31.00/4.53 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 31.00/4.53 fof(f21059,plain,(
% 31.00/4.53 ![X0]: (~has_card_leq(X0,int1994)|~val(c5,X0)|~sQ14_spl)),
% 31.00/4.53 inference(component_clause,[status(thm)],[f21058])).
% 31.00/4.53 fof(f21064,definition,(
% 31.00/4.53 sQ16_spl <=> (sub(c5,jahr__1_1))),
% 31.00/4.53 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 31.00/4.53 fof(f21066,plain,(
% 31.00/4.53 ~sub(c5,jahr__1_1)|sQ16_spl),
% 31.00/4.53 inference(component_clause,[status(thm)],[f21064])).
% 31.00/4.53 fof(f21071,definition,(
% 31.00/4.53 ![X0,X1,X2]: (sQ18_spl <=> (~agt(X0,X1)|~attr(X1,X2)|~sub(X2,name_1_1)|~subs(X0,n374bernehmen_1_1)|~temp(X0,c4)|~val(X2,bmw_0)))),
% 31.00/4.53 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 31.00/4.53 fof(f21072,plain,(
% 31.00/4.53 ![X0,X1,X2]: (~agt(X0,X1)|~attr(X1,X2)|~sub(X2,name_1_1)|~subs(X0,n374bernehmen_1_1)|~temp(X0,c4)|~val(X2,bmw_0)|~sQ18_spl)),
% 31.00/4.53 inference(component_clause,[status(thm)],[f21071])).
% 31.00/4.53 fof(f21074,plain,(
% 31.00/4.53 sQ18_spl|sQ14_spl|~sQ16_spl|~sQ0_spl),
% 31.00/4.53 inference(split_clause,[status(thm)],[f21052,f21071,f21058,f21064,f20980])).
% 31.00/4.53 fof(f21099,definition,(
% 31.00/4.53 sQ24_spl <=> (val(c87,bmw_0))),
% 31.00/4.53 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 31.00/4.53 fof(f21101,plain,(
% 31.00/4.53 ~val(c87,bmw_0)|sQ24_spl),
% 31.00/4.53 inference(component_clause,[status(thm)],[f21099])).
% 31.00/4.53 fof(f21112,plain,(
% 31.00/4.53 $false|sQ24_spl),
% 31.00/4.53 inference(forward_subsumption_resolution,[status(thm)],[f21101,f20835])).
% 31.00/4.53 fof(f21113,plain,(
% 31.00/4.53 sQ24_spl),
% 31.00/4.53 inference(contradiction_clause,[status(thm)],[f21112])).
% 31.00/4.53 fof(f21119,plain,(
% 31.00/4.53 $false|sQ16_spl),
% 31.00/4.53 inference(forward_subsumption_resolution,[status(thm)],[f21066,f20830])).
% 31.00/4.53 fof(f21120,plain,(
% 31.00/4.53 sQ16_spl),
% 31.00/4.53 inference(contradiction_clause,[status(thm)],[f21119])).
% 31.00/4.53 fof(f21122,plain,(
% 31.00/4.53 ~val(c5,c1)|~sQ14_spl),
% 31.00/4.53 inference(resolution,[status(thm)],[f21059,f21027])).
% 31.00/4.53 fof(f21123,plain,(
% 31.00/4.53 $false|~sQ14_spl),
% 31.00/4.53 inference(forward_subsumption_resolution,[status(thm)],[f21122,f20831])).
% 31.00/4.53 fof(f21124,plain,(
% 31.00/4.53 ~sQ14_spl),
% 31.00/4.53 inference(contradiction_clause,[status(thm)],[f21123])).
% 31.00/4.53 fof(f21125,plain,(
% 31.00/4.53 ~agt(c3,c86)|~sub(c87,name_1_1)|~val(c87,bmw_0)|~sQ10_spl),
% 31.00/4.53 inference(resolution,[status(thm)],[f21040,f20832])).
% 31.00/4.53 fof(f21128,definition,(
% 31.00/4.53 sQ27_spl <=> (agt(c3,c86))),
% 31.00/4.53 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 31.00/4.53 fof(f21130,plain,(
% 31.00/4.53 ~agt(c3,c86)|sQ27_spl),
% 31.00/4.53 inference(component_clause,[status(thm)],[f21128])).
% 31.00/4.53 fof(f21131,plain,(
% 31.00/4.53 ~sQ27_spl|~sQ5_spl|~sQ24_spl|~sQ10_spl),
% 31.00/4.53 inference(split_clause,[status(thm)],[f21125,f21128,f21007,f21099,f21039])).
% 31.00/4.53 fof(f21142,plain,(
% 31.00/4.53 ![X0,X1]: (~agt(c3,X0)|~attr(X0,X1)|~sub(X1,name_1_1)|~subs(c3,n374bernehmen_1_1)|~val(X1,bmw_0)|~sQ18_spl)),
% 31.00/4.53 inference(resolution,[status(thm)],[f21072,f20828])).
% 31.00/4.53 fof(f21149,plain,(
% 31.00/4.53 sQ10_spl|~sQ12_spl|~sQ18_spl),
% 31.00/4.53 inference(split_clause,[status(thm)],[f21142,f21039,f21045,f21071])).
% 31.00/4.53 fof(f22005,plain,(
% 31.00/4.53 $false|sQ5_spl),
% 31.00/4.53 inference(forward_subsumption_resolution,[status(thm)],[f20834,f21009])).
% 31.00/4.53 fof(f22006,plain,(
% 31.00/4.53 sQ5_spl),
% 31.00/4.53 inference(contradiction_clause,[status(thm)],[f22005])).
% 31.00/4.53 fof(f22007,plain,(
% 31.00/4.53 $false|sQ27_spl),
% 31.00/4.53 inference(forward_subsumption_resolution,[status(thm)],[f21130,f20825])).
% 31.00/4.53 fof(f22008,plain,(
% 31.00/4.53 sQ27_spl),
% 31.00/4.53 inference(contradiction_clause,[status(thm)],[f22007])).
% 31.00/4.53 fof(f22009,plain,(
% 31.00/4.53 $false),
% 31.00/4.53 inference(sat_refutation,[status(thm)],[f20986,f20996,f21050,f21074,f21113,f21120,f21124,f21131,f21149,f22006,f22008])).
% 31.00/4.53 % SZS output end CNFRefutation for theBenchmark.p
% 31.00/4.53 % Elapsed time: 4.172775 seconds
% 31.00/4.53 % CPU time: 31.560858 seconds
% 31.00/4.53 % Total memory used: 560.700 MB
% 31.00/4.53 % Net memory used: 549.674 MB
%------------------------------------------------------------------------------