%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR114+16 : 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 : n017.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:20 PM UTC 2026
% Result : Theorem 36.34s 5.29s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR114+16 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n017.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Mon Sep 21 14:59:42 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.38/0.64 % Drodi V4.1.1
% 36.34/5.29 % Refutation found
% 36.34/5.29 % SZS status Theorem for theBenchmark: Theorem is valid
% 36.34/5.29 % SZS output start CNFRefutation for theBenchmark
% 36.34/5.29 fof(f10188,conjecture,(
% 36.34/5.29 (? [X0,X1,X2,X3] :( attr(X0,X1)& scar(X3,X2)& sub(X1,name_1_1)& sub(X0,stadt__1_1)& val(X1,rom_0) ) )),
% 36.34/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.34/5.29 fof(f10189,negated_conjecture,(
% 36.34/5.29 ~((? [X0,X1,X2,X3] :( attr(X0,X1)& scar(X3,X2)& sub(X1,name_1_1)& sub(X0,stadt__1_1)& val(X1,rom_0) ) ))),
% 36.34/5.29 inference(negated_conjecture,[status(cth)],[f10188])).
% 36.34/5.29 fof(f10190,hypothesis,(
% 36.34/5.29 ( obj(c657,c660)& scar(c657,c43)& subs(c657,haben_1_1)& pred(c660,bewohner__1_1)& assoc(c672,c814)& scar(c672,c43)& semrel(c672,c657)& sspe(c672,c819)& subs(c672,geh__366ren_1_1)& sub(c814,provinz_1_1)& attr(c819,c820)& sub(c819,stadt__1_1)& sub(c820,name_1_1)& val(c820,rom_0)& sort(c657,st)& fact(c657,real)& gener(c657,sp)& sort(c660,d)& card(c660,int35895)& etype(c660,int1)& fact(c660,real)& gener(c660,sp)& quant(c660,nfquant)& refer(c660,indet)& varia(c660,varia_c)& sort(c43,abs)& sort(c43,co)& sort(c43,io)& sort(c43,mo)& sort(c43,ta)& sort(c43,re)& card(c43,card_c)& etype(c43,etype_c)& fact(c43,real)& gener(c43,sp)& quant(c43,quant_c)& refer(c43,det)& varia(c43,varia_c)& sort(haben_1_1,st)& fact(haben_1_1,real)& gener(haben_1_1,ge)& sort(bewohner__1_1,d)& card(bewohner__1_1,int1)& etype(bewohner__1_1,int0)& fact(bewohner__1_1,real)& gener(bewohner__1_1,ge)& quant(bewohner__1_1,one)& refer(bewohner__1_1,refer_c)& varia(bewohner__1_1,varia_c)& sort(c672,st)& fact(c672,real)& gener(c672,sp)& sort(c814,d)& sort(c814,io)& card(c814,int1)& etype(c814,int0)& fact(c814,real)& gener(c814,sp)& quant(c814,one)& refer(c814,det)& varia(c814,con)& sort(c819,d)& sort(c819,io)& card(c819,int1)& etype(c819,int0)& fact(c819,real)& gener(c819,sp)& quant(c819,one)& refer(c819,det)& varia(c819,con)& sort(geh__366ren_1_1,st)& fact(geh__366ren_1_1,real)& gener(geh__366ren_1_1,ge)& sort(provinz_1_1,d)& sort(provinz_1_1,io)& card(provinz_1_1,int1)& etype(provinz_1_1,int0)& fact(provinz_1_1,real)& gener(provinz_1_1,ge)& quant(provinz_1_1,one)& refer(provinz_1_1,refer_c)& varia(provinz_1_1,varia_c)& sort(c820,na)& card(c820,int1)& etype(c820,int0)& fact(c820,real)& gener(c820,sp)& quant(c820,one)& refer(c820,indet)& varia(c820,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(rom_0,fe) ) ),
% 36.34/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.34/5.29 fof(f20815,plain,(
% 36.34/5.29 (![X0,X1,X2,X3]: ((((~attr(X0,X1)|~scar(X3,X2))|~sub(X1,name_1_1))|~sub(X0,stadt__1_1))|~val(X1,rom_0)))),
% 36.34/5.29 inference(pre_NNF_transformation,[status(thm)],[f10189])).
% 36.34/5.29 fof(f20816,plain,(
% 36.34/5.29 ![X1]: ((![X0]: (((~attr(X0,X1)|(![X2,X3]: ~scar(X3,X2)))|~sub(X1,name_1_1))|~sub(X0,stadt__1_1)))|~val(X1,rom_0))),
% 36.34/5.29 inference(miniscoping,[status(thm)],[f20815])).
% 36.34/5.29 fof(f20817,plain,(
% 36.34/5.29 ![X0,X1,X2,X3]: (~attr(X0,X1)|~scar(X2,X3)|~sub(X1,name_1_1)|~sub(X0,stadt__1_1)|~val(X1,rom_0))),
% 36.34/5.29 inference(cnf_transformation,[status(thm)],[f20816])).
% 36.34/5.29 fof(f20823,plain,(
% 36.34/5.29 scar(c672,c43)),
% 36.34/5.29 inference(cnf_transformation,[status(thm)],[f10190])).
% 36.34/5.29 fof(f20828,plain,(
% 36.34/5.29 attr(c819,c820)),
% 36.34/5.29 inference(cnf_transformation,[status(thm)],[f10190])).
% 36.34/5.29 fof(f20829,plain,(
% 36.34/5.29 sub(c819,stadt__1_1)),
% 36.34/5.29 inference(cnf_transformation,[status(thm)],[f10190])).
% 36.34/5.29 fof(f20830,plain,(
% 36.34/5.29 sub(c820,name_1_1)),
% 36.34/5.29 inference(cnf_transformation,[status(thm)],[f10190])).
% 36.34/5.29 fof(f20831,plain,(
% 36.34/5.29 val(c820,rom_0)),
% 36.34/5.29 inference(cnf_transformation,[status(thm)],[f10190])).
% 36.34/5.29 fof(f20961,definition,(
% 36.34/5.29 ![X0,X1]: (sQ0_spl <=> (~attr(X0,X1)|~sub(X1,name_1_1)|~sub(X0,stadt__1_1)|~val(X1,rom_0)))),
% 36.34/5.29 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 36.34/5.29 fof(f20962,plain,(
% 36.34/5.29 ![X0,X1]: (~attr(X0,X1)|~sub(X1,name_1_1)|~sub(X0,stadt__1_1)|~val(X1,rom_0)|~sQ0_spl)),
% 36.34/5.35 inference(component_clause,[status(thm)],[f20961])).
% 36.34/5.35 fof(f20964,definition,(
% 36.34/5.35 ![X2,X3]: (sQ1_spl <=> (~scar(X2,X3)))),
% 36.34/5.35 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 36.34/5.35 fof(f20965,plain,(
% 36.34/5.35 ![X0,X1]: (~scar(X0,X1)|~sQ1_spl)),
% 36.34/5.35 inference(component_clause,[status(thm)],[f20964])).
% 36.34/5.35 fof(f20967,plain,(
% 36.34/5.35 sQ0_spl|sQ1_spl),
% 36.34/5.35 inference(split_clause,[status(thm)],[f20817,f20961,f20964])).
% 36.34/5.35 fof(f21064,plain,(
% 36.34/5.35 ![X0]: (~attr(X0,c820)|~sub(X0,stadt__1_1)|~val(c820,rom_0)|~sQ0_spl)),
% 36.34/5.35 inference(resolution,[status(thm)],[f20830,f20962])).
% 36.34/5.35 fof(f21074,definition,(
% 36.34/5.35 sQ18_spl <=> (val(c820,rom_0))),
% 36.34/5.35 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 36.34/5.35 fof(f21076,plain,(
% 36.34/5.35 ~val(c820,rom_0)|sQ18_spl),
% 36.34/5.35 inference(component_clause,[status(thm)],[f21074])).
% 36.34/5.35 fof(f21086,definition,(
% 36.34/5.35 ![X0]: (sQ21_spl <=> (~attr(X0,c820)|~sub(X0,stadt__1_1)))),
% 36.34/5.35 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 36.34/5.35 fof(f21087,plain,(
% 36.34/5.35 ![X0]: (~attr(X0,c820)|~sub(X0,stadt__1_1)|~sQ21_spl)),
% 36.34/5.35 inference(component_clause,[status(thm)],[f21086])).
% 36.34/5.35 fof(f21089,plain,(
% 36.34/5.35 sQ21_spl|~sQ18_spl|~sQ0_spl),
% 36.34/5.35 inference(split_clause,[status(thm)],[f21064,f21086,f21074,f20961])).
% 36.34/5.35 fof(f21099,plain,(
% 36.34/5.35 $false|sQ18_spl),
% 36.34/5.35 inference(forward_subsumption_resolution,[status(thm)],[f21076,f20831])).
% 36.34/5.35 fof(f21100,plain,(
% 36.34/5.35 sQ18_spl),
% 36.34/5.35 inference(contradiction_clause,[status(thm)],[f21099])).
% 36.34/5.35 fof(f21101,plain,(
% 36.34/5.35 $false|~sQ1_spl),
% 36.34/5.35 inference(backward_subsumption_resolution,[status(thm)],[f20823,f20965])).
% 36.34/5.35 fof(f21114,plain,(
% 36.34/5.35 ~sQ1_spl),
% 36.34/5.35 inference(contradiction_clause,[status(thm)],[f21101])).
% 36.34/5.35 fof(f21126,plain,(
% 36.34/5.35 ~attr(c819,c820)|~sQ21_spl),
% 36.34/5.35 inference(resolution,[status(thm)],[f21087,f20829])).
% 36.34/5.35 fof(f21128,plain,(
% 36.34/5.35 $false|~sQ21_spl),
% 36.34/5.35 inference(forward_subsumption_resolution,[status(thm)],[f21126,f20828])).
% 36.34/5.35 fof(f21129,plain,(
% 36.34/5.35 ~sQ21_spl),
% 36.34/5.35 inference(contradiction_clause,[status(thm)],[f21128])).
% 36.34/5.35 fof(f21130,plain,(
% 36.34/5.35 $false),
% 36.34/5.35 inference(sat_refutation,[status(thm)],[f20967,f21089,f21100,f21114,f21129])).
% 36.34/5.35 % SZS output end CNFRefutation for theBenchmark.p
% 1.02/5.55 % Elapsed time: 5.089760 seconds
% 1.02/5.55 % CPU time: 37.197263 seconds
% 1.02/5.55 % Total memory used: 584.962 MB
% 1.02/5.55 % Net memory used: 555.700 MB
%------------------------------------------------------------------------------