%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR115+81 : 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 : n026.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 20.63s 3.15s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR115+81 : 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.10/0.36 % Computer : n026.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 15:10:09 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.22/0.49 % Drodi V4.1.1
% 20.63/3.15 % Refutation found
% 20.63/3.15 % SZS status Theorem for theBenchmark: Theorem is valid
% 20.63/3.15 % SZS output start CNFRefutation for theBenchmark
% 20.63/3.15 fof(f10188,conjecture,(
% 20.63/3.15 (? [X0,X1,X2,X3,X4,X5,X6] :( agt(X4,X3)& attr(X0,X1)& attr(X3,X2)& attr(X5,X6)& sub(X1,name_1_1)& sub(X0,firma_1_1)& sub(X2,name_1_1)& subs(X4,n374bernehmen_1_1)& val(X1,bmw_0)& val(X2,bmw_0) ) )),
% 20.63/3.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.63/3.15 fof(f10189,negated_conjecture,(
% 20.63/3.15 ~((? [X0,X1,X2,X3,X4,X5,X6] :( agt(X4,X3)& attr(X0,X1)& attr(X3,X2)& attr(X5,X6)& sub(X1,name_1_1)& sub(X0,firma_1_1)& sub(X2,name_1_1)& subs(X4,n374bernehmen_1_1)& val(X1,bmw_0)& val(X2,bmw_0) ) ))),
% 20.63/3.15 inference(negated_conjecture,[status(cth)],[f10188])).
% 20.63/3.15 fof(f10190,hypothesis,(
% 20.63/3.15 ( pred(c12,getriebe__1_1)& pred(c16,rotornabe_1_1)& sub(c4,konstruktion_1_1)& agt(c45,c57)& modl(c45,sollen_0)& obj(c45,c62)& subs(c45,n374bernehmen_1_1)& attr(c57,c58)& sub(c57,firma_1_1)& sub(c58,name_1_1)& val(c58,bmw_0)& itms_p4(c62,c4,c12,c16)& attch(c9,c4)& subs(c9,motoranlage_1_1)& assoc(motoranlage_1_1,motor__1_1)& subs(motoranlage_1_1,anlage_1_1)& assoc(rotornabe_1_1,rotor_1_1)& sub(rotornabe_1_1,nabe_1_1)& sort(c12,d)& card(c12,cons(x_constant,cons(int1,nil)))& etype(c12,int1)& fact(c12,real)& gener(c12,gener_c)& quant(c12,mult)& refer(c12,indet)& varia(c12,varia_c)& sort(getriebe__1_1,d)& card(getriebe__1_1,int1)& etype(getriebe__1_1,int0)& fact(getriebe__1_1,real)& gener(getriebe__1_1,ge)& quant(getriebe__1_1,one)& refer(getriebe__1_1,refer_c)& varia(getriebe__1_1,varia_c)& sort(c16,o)& card(c16,cons(x_constant,cons(int1,nil)))& etype(c16,int1)& fact(c16,real)& gener(c16,gener_c)& quant(c16,mult)& refer(c16,indet)& varia(c16,varia_c)& sort(rotornabe_1_1,o)& card(rotornabe_1_1,int1)& etype(rotornabe_1_1,int0)& fact(rotornabe_1_1,real)& gener(rotornabe_1_1,ge)& quant(rotornabe_1_1,one)& refer(rotornabe_1_1,refer_c)& varia(rotornabe_1_1,varia_c)& sort(c4,d)& card(c4,int1)& etype(c4,int0)& fact(c4,real)& gener(c4,sp)& quant(c4,one)& refer(c4,det)& varia(c4,con)& sort(konstruktion_1_1,d)& card(konstruktion_1_1,int1)& etype(konstruktion_1_1,int0)& fact(konstruktion_1_1,real)& gener(konstruktion_1_1,ge)& quant(konstruktion_1_1,one)& refer(konstruktion_1_1,refer_c)& varia(konstruktion_1_1,varia_c)& sort(c45,da)& fact(c45,real)& gener(c45,sp)& sort(c57,d)& sort(c57,io)& card(c57,int1)& etype(c57,int0)& fact(c57,real)& gener(c57,sp)& quant(c57,one)& refer(c57,det)& varia(c57,con)& sort(sollen_0,md)& fact(sollen_0,real)& gener(sollen_0,gener_c)& sort(c62,o)& card(c62,int3)& etype(c62,int1)& fact(c62,real)& gener(c62,sp)& quant(c62,nfquant)& refer(c62,det)& varia(c62,con)& sort(n374bernehmen_1_1,da)& fact(n374bernehmen_1_1,real)& gener(n374bernehmen_1_1,ge)& sort(c58,na)& card(c58,int1)& etype(c58,int0)& fact(c58,real)& gener(c58,sp)& quant(c58,one)& refer(c58,indet)& varia(c58,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(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(bmw_0,fe)& sort(c9,as)& card(c9,int1)& etype(c9,int0)& fact(c9,real)& gener(c9,gener_c)& quant(c9,one)& refer(c9,refer_c)& varia(c9,varia_c)& sort(motoranlage_1_1,as)& card(motoranlage_1_1,int1)& etype(motoranlage_1_1,int0)& fact(motoranlage_1_1,real)& gener(motoranlage_1_1,ge)& quant(motoranlage_1_1,one)& refer(motoranlage_1_1,refer_c)& varia(motoranlage_1_1,varia_c)& sort(motor__1_1,d)& card(motor__1_1,int1)& etype(motor__1_1,int0)& fact(motor__1_1,real)& gener(motor__1_1,ge)& quant(motor__1_1,one)& refer(motor__1_1,refer_c)& varia(motor__1_1,varia_c)& sort(anlage_1_1,as)& card(anlage_1_1,int1)& etype(anlage_1_1,int0)& fact(anlage_1_1,real)& gener(anlage_1_1,ge)& quant(anlage_1_1,one)& refer(anlage_1_1,refer_c)& varia(anlage_1_1,varia_c)& sort(rotor_1_1,o)& card(rotor_1_1,int1)& etype(rotor_1_1,int0)& fact(rotor_1_1,real)& gener(rotor_1_1,ge)& quant(rotor_1_1,one)& refer(rotor_1_1,refer_c)& varia(rotor_1_1,varia_c)& sort(nabe_1_1,o)& card(nabe_1_1,int1)& etype(nabe_1_1,int0)& fact(nabe_1_1,real)& gener(nabe_1_1,ge)& quant(nabe_1_1,one)& refer(nabe_1_1,refer_c)& varia(nabe_1_1,varia_c) ) ),
% 20.63/3.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.63/3.15 fof(f20815,plain,(
% 20.63/3.15 (![X0,X1,X2,X3,X4,X5,X6]: (((((((((~agt(X4,X3)|~attr(X0,X1))|~attr(X3,X2))|~attr(X5,X6))|~sub(X1,name_1_1))|~sub(X0,firma_1_1))|~sub(X2,name_1_1))|~subs(X4,n374bernehmen_1_1))|~val(X1,bmw_0))|~val(X2,bmw_0)))),
% 20.63/3.15 inference(pre_NNF_transformation,[status(thm)],[f10189])).
% 20.63/3.15 fof(f20816,plain,(
% 20.63/3.15 ![X2]: ((![X1]: ((![X4]: (((![X0]: ((((![X3]: ((~agt(X4,X3)|~attr(X0,X1))|~attr(X3,X2)))|(![X5,X6]: ~attr(X5,X6)))|~sub(X1,name_1_1))|~sub(X0,firma_1_1)))|~sub(X2,name_1_1))|~subs(X4,n374bernehmen_1_1)))|~val(X1,bmw_0)))|~val(X2,bmw_0))),
% 20.63/3.15 inference(miniscoping,[status(thm)],[f20815])).
% 20.63/3.15 fof(f20817,plain,(
% 20.63/3.15 ![X0,X1,X2,X3,X4,X5,X6]: (~agt(X0,X1)|~attr(X2,X3)|~attr(X1,X4)|~attr(X5,X6)|~sub(X3,name_1_1)|~sub(X2,firma_1_1)|~sub(X4,name_1_1)|~subs(X0,n374bernehmen_1_1)|~val(X3,bmw_0)|~val(X4,bmw_0))),
% 20.63/3.15 inference(cnf_transformation,[status(thm)],[f20816])).
% 20.63/3.15 fof(f20821,plain,(
% 20.63/3.15 agt(c45,c57)),
% 20.63/3.15 inference(cnf_transformation,[status(thm)],[f10190])).
% 20.63/3.15 fof(f20824,plain,(
% 20.63/3.15 subs(c45,n374bernehmen_1_1)),
% 20.63/3.15 inference(cnf_transformation,[status(thm)],[f10190])).
% 20.63/3.15 fof(f20825,plain,(
% 20.63/3.15 attr(c57,c58)),
% 20.63/3.15 inference(cnf_transformation,[status(thm)],[f10190])).
% 20.63/3.15 fof(f20826,plain,(
% 20.63/3.15 sub(c57,firma_1_1)),
% 20.63/3.15 inference(cnf_transformation,[status(thm)],[f10190])).
% 20.63/3.15 fof(f20827,plain,(
% 20.63/3.15 sub(c58,name_1_1)),
% 20.63/3.15 inference(cnf_transformation,[status(thm)],[f10190])).
% 20.63/3.15 fof(f20828,plain,(
% 20.63/3.15 val(c58,bmw_0)),
% 20.63/3.15 inference(cnf_transformation,[status(thm)],[f10190])).
% 20.63/3.15 fof(f21019,definition,(
% 20.63/3.15 ![X0,X1,X4]: (sQ0_spl <=> (~agt(X0,X1)|~attr(X1,X4)|~sub(X4,name_1_1)|~subs(X0,n374bernehmen_1_1)|~val(X4,bmw_0)))),
% 20.63/3.15 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 20.63/3.15 fof(f21020,plain,(
% 20.63/3.15 ![X0,X1,X2]: (~agt(X0,X1)|~attr(X1,X2)|~sub(X2,name_1_1)|~subs(X0,n374bernehmen_1_1)|~val(X2,bmw_0)|~sQ0_spl)),
% 20.63/3.15 inference(component_clause,[status(thm)],[f21019])).
% 20.63/3.15 fof(f21022,definition,(
% 20.63/3.15 ![X2,X3]: (sQ1_spl <=> (~attr(X2,X3)|~sub(X3,name_1_1)|~sub(X2,firma_1_1)|~val(X3,bmw_0)))),
% 20.63/3.15 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 20.63/3.15 fof(f21023,plain,(
% 20.63/3.15 ![X0,X1]: (~attr(X0,X1)|~sub(X1,name_1_1)|~sub(X0,firma_1_1)|~val(X1,bmw_0)|~sQ1_spl)),
% 20.63/3.15 inference(component_clause,[status(thm)],[f21022])).
% 20.63/3.15 fof(f21025,definition,(
% 20.63/3.15 ![X5,X6]: (sQ2_spl <=> (~attr(X5,X6)))),
% 20.63/3.15 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 20.63/3.15 fof(f21026,plain,(
% 20.63/3.15 ![X0,X1]: (~attr(X0,X1)|~sQ2_spl)),
% 20.63/3.15 inference(component_clause,[status(thm)],[f21025])).
% 20.63/3.15 fof(f21028,plain,(
% 20.63/3.15 sQ0_spl|sQ1_spl|sQ2_spl),
% 20.63/3.15 inference(split_clause,[status(thm)],[f20817,f21019,f21022,f21025])).
% 20.63/3.15 fof(f21042,plain,(
% 20.63/3.15 $false|~sQ2_spl),
% 20.63/3.15 inference(forward_subsumption_resolution,[status(thm)],[f20825,f21026])).
% 20.63/3.15 fof(f21043,plain,(
% 20.63/3.15 ~sQ2_spl),
% 20.63/3.15 inference(contradiction_clause,[status(thm)],[f21042])).
% 20.63/3.15 fof(f21047,plain,(
% 20.63/3.15 ![X0,X1]: (~agt(X0,X1)|~attr(X1,c58)|~sub(c58,name_1_1)|~subs(X0,n374bernehmen_1_1)|~sQ0_spl)),
% 20.63/3.15 inference(resolution,[status(thm)],[f21020,f20828])).
% 20.63/3.15 fof(f21048,definition,(
% 20.63/3.15 ![X0,X1]: (sQ3_spl <=> (~agt(X0,X1)|~attr(X1,c58)|~subs(X0,n374bernehmen_1_1)))),
% 20.63/3.15 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 20.63/3.15 fof(f21049,plain,(
% 20.63/3.15 ![X0,X1]: (~agt(X0,X1)|~attr(X1,c58)|~subs(X0,n374bernehmen_1_1)|~sQ3_spl)),
% 20.63/3.15 inference(component_clause,[status(thm)],[f21048])).
% 20.63/3.15 fof(f21051,definition,(
% 20.63/3.15 sQ4_spl <=> (sub(c58,name_1_1))),
% 20.63/3.15 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 20.63/3.15 fof(f21053,plain,(
% 20.63/3.15 ~sub(c58,name_1_1)|sQ4_spl),
% 20.63/3.15 inference(component_clause,[status(thm)],[f21051])).
% 20.63/3.15 fof(f21054,plain,(
% 20.63/3.15 sQ3_spl|~sQ4_spl|~sQ0_spl),
% 20.63/3.15 inference(split_clause,[status(thm)],[f21047,f21048,f21051,f21019])).
% 20.63/3.15 fof(f21055,plain,(
% 20.63/3.15 $false|sQ4_spl),
% 20.63/3.15 inference(forward_subsumption_resolution,[status(thm)],[f21053,f20827])).
% 20.63/3.21 fof(f21056,plain,(
% 20.63/3.21 sQ4_spl),
% 20.63/3.21 inference(contradiction_clause,[status(thm)],[f21055])).
% 20.63/3.21 fof(f21057,plain,(
% 20.63/3.21 ![X0]: (~attr(X0,c58)|~sub(c58,name_1_1)|~sub(X0,firma_1_1)|~sQ1_spl)),
% 20.63/3.21 inference(resolution,[status(thm)],[f21023,f20828])).
% 20.63/3.21 fof(f21058,definition,(
% 20.63/3.21 ![X0]: (sQ5_spl <=> (~attr(X0,c58)|~sub(X0,firma_1_1)))),
% 20.63/3.21 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 20.63/3.21 fof(f21059,plain,(
% 20.63/3.21 ![X0]: (~attr(X0,c58)|~sub(X0,firma_1_1)|~sQ5_spl)),
% 20.63/3.21 inference(component_clause,[status(thm)],[f21058])).
% 20.63/3.21 fof(f21061,plain,(
% 20.63/3.21 sQ5_spl|~sQ4_spl|~sQ1_spl),
% 20.63/3.21 inference(split_clause,[status(thm)],[f21057,f21058,f21051,f21022])).
% 20.63/3.21 fof(f21065,plain,(
% 20.63/3.21 ~sub(c57,firma_1_1)|~sQ5_spl),
% 20.63/3.21 inference(resolution,[status(thm)],[f21059,f20825])).
% 20.63/3.21 fof(f21066,plain,(
% 20.63/3.21 $false|~sQ5_spl),
% 20.63/3.21 inference(forward_subsumption_resolution,[status(thm)],[f21065,f20826])).
% 20.63/3.21 fof(f21067,plain,(
% 20.63/3.21 ~sQ5_spl),
% 20.63/3.21 inference(contradiction_clause,[status(thm)],[f21066])).
% 20.63/3.21 fof(f21076,plain,(
% 20.63/3.21 ![X0]: (~agt(X0,c57)|~subs(X0,n374bernehmen_1_1)|~sQ3_spl)),
% 20.63/3.21 inference(resolution,[status(thm)],[f21049,f20825])).
% 20.63/3.21 fof(f21077,plain,(
% 20.63/3.21 ~agt(c45,c57)|~sQ3_spl),
% 20.63/3.21 inference(resolution,[status(thm)],[f21076,f20824])).
% 20.63/3.21 fof(f21079,plain,(
% 20.63/3.21 $false|~sQ3_spl),
% 20.63/3.21 inference(forward_subsumption_resolution,[status(thm)],[f21077,f20821])).
% 20.63/3.21 fof(f21080,plain,(
% 20.63/3.21 ~sQ3_spl),
% 20.63/3.21 inference(contradiction_clause,[status(thm)],[f21079])).
% 20.63/3.21 fof(f21081,plain,(
% 20.63/3.21 $false),
% 20.63/3.21 inference(sat_refutation,[status(thm)],[f21028,f21043,f21054,f21056,f21061,f21067,f21080])).
% 20.63/3.21 % SZS output end CNFRefutation for theBenchmark.p
% 4.23/3.23 % Elapsed time: 2.855727 seconds
% 4.23/3.23 % CPU time: 21.190151 seconds
% 4.23/3.23 % Total memory used: 519.152 MB
% 4.23/3.23 % Net memory used: 510.612 MB
%------------------------------------------------------------------------------