%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR113+18 : 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 : n010.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:18 PM UTC 2026
% Result : Theorem 18.36s 7.88s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR113+18 : 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.12/5.40 % Computer : n010.cluster.edu
% 0.12/5.40 % Model : x86_64 x86_64
% 0.12/5.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.40 % Memory : 8046.5625MB
% 0.12/5.40 % OS : Linux 6.8.0-71-generic
% 0.12/5.40 % CPULimit : 300
% 0.12/5.40 % WCLimit : 300
% 0.12/5.40 % DateTime : Mon Sep 21 15:03:15 UTC 2026
% 0.12/5.40 % CPUTime :
% 0.12/5.46 % Drodi V4.1.1
% 18.36/7.88 % Refutation found
% 18.36/7.88 % SZS status Theorem for theBenchmark: Theorem is valid
% 18.36/7.88 % SZS output start CNFRefutation for theBenchmark
% 18.36/7.88 fof(f10188,conjecture,(
% 18.36/7.88 (? [X0,X1,X2,X3,X4] :( attr(X2,X1)& loc(X3,X0)& scar(X3,X4)& sub(X1,name_1_1)& sub(X4,freiheitsstatue_1_1)& subs(X3,stehen_1_1)& val(X1,new_york_0) ) )),
% 18.36/7.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.36/7.88 fof(f10189,negated_conjecture,(
% 18.36/7.88 ~((? [X0,X1,X2,X3,X4] :( attr(X2,X1)& loc(X3,X0)& scar(X3,X4)& sub(X1,name_1_1)& sub(X4,freiheitsstatue_1_1)& subs(X3,stehen_1_1)& val(X1,new_york_0) ) ))),
% 18.36/7.88 inference(negated_conjecture,[status(cth)],[f10188])).
% 18.36/7.88 fof(f10190,hypothesis,(
% 18.36/7.88 ( supl(c34,bekannt_1_1,c35)& prop(c4,c34)& sub(c4,freiheitsstatue_1_1)& attr(c41,c42)& sub(c41,stadt__1_1)& sub(c42,name_1_1)& val(c42,new_york_0)& mexp(c44,c50)& semrel(c44,c8)& subs(c44,sehen_1_1)& vor(c53,c41)& loc(c8,c53)& scar(c8,c4)& subs(c8,stehen_1_1)& assoc(freiheitsstatue_1_1,freiheit_1_1)& sub(freiheitsstatue_1_1,statue_1_1)& sort(c34,tq)& sort(bekannt_1_1,nq)& sort(c35,o)& card(c35,card_c)& etype(c35,int1)& etype(c35,int2)& fact(c35,real)& gener(c35,gener_c)& quant(c35,quant_c)& refer(c35,refer_c)& varia(c35,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(freiheitsstatue_1_1,d)& card(freiheitsstatue_1_1,int1)& etype(freiheitsstatue_1_1,int0)& fact(freiheitsstatue_1_1,real)& gener(freiheitsstatue_1_1,ge)& quant(freiheitsstatue_1_1,one)& refer(freiheitsstatue_1_1,refer_c)& varia(freiheitsstatue_1_1,varia_c)& sort(c41,d)& sort(c41,io)& card(c41,int1)& etype(c41,int0)& fact(c41,real)& gener(c41,sp)& quant(c41,one)& refer(c41,det)& varia(c41,con)& sort(c42,na)& card(c42,int1)& etype(c42,int0)& fact(c42,real)& gener(c42,sp)& quant(c42,one)& refer(c42,indet)& varia(c42,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(new_york_0,fe)& sort(c44,dn)& fact(c44,real)& gener(c44,sp)& sort(c50,d)& card(c50,int1)& etype(c50,int0)& fact(c50,real)& gener(c50,sp)& quant(c50,one)& refer(c50,det)& varia(c50,varia_c)& sort(c8,st)& fact(c8,real)& gener(c8,sp)& sort(sehen_1_1,dn)& fact(sehen_1_1,real)& gener(sehen_1_1,ge)& sort(c53,l)& card(c53,int1)& etype(c53,int0)& fact(c53,real)& gener(c53,sp)& quant(c53,one)& refer(c53,det)& varia(c53,con)& sort(stehen_1_1,st)& fact(stehen_1_1,real)& gener(stehen_1_1,ge)& sort(freiheit_1_1,as)& sort(freiheit_1_1,io)& card(freiheit_1_1,int1)& etype(freiheit_1_1,int0)& fact(freiheit_1_1,real)& gener(freiheit_1_1,ge)& quant(freiheit_1_1,one)& refer(freiheit_1_1,refer_c)& varia(freiheit_1_1,varia_c)& sort(statue_1_1,d)& card(statue_1_1,int1)& etype(statue_1_1,int0)& fact(statue_1_1,real)& gener(statue_1_1,ge)& quant(statue_1_1,one)& refer(statue_1_1,refer_c)& varia(statue_1_1,varia_c) ) ),
% 18.36/7.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.36/7.88 fof(f20815,plain,(
% 18.36/7.88 (![X0,X1,X2,X3,X4]: ((((((~attr(X2,X1)|~loc(X3,X0))|~scar(X3,X4))|~sub(X1,name_1_1))|~sub(X4,freiheitsstatue_1_1))|~subs(X3,stehen_1_1))|~val(X1,new_york_0)))),
% 18.36/7.88 inference(pre_NNF_transformation,[status(thm)],[f10189])).
% 18.36/7.88 fof(f20816,plain,(
% 18.36/7.88 ![X1]: ((![X3]: ((![X4]: (((((![X2]: ~attr(X2,X1))|(![X0]: ~loc(X3,X0)))|~scar(X3,X4))|~sub(X1,name_1_1))|~sub(X4,freiheitsstatue_1_1)))|~subs(X3,stehen_1_1)))|~val(X1,new_york_0))),
% 18.36/7.88 inference(miniscoping,[status(thm)],[f20815])).
% 18.36/7.88 fof(f20817,plain,(
% 18.36/7.88 ![X0,X1,X2,X3,X4]: (~attr(X0,X1)|~loc(X2,X3)|~scar(X2,X4)|~sub(X1,name_1_1)|~sub(X4,freiheitsstatue_1_1)|~subs(X2,stehen_1_1)|~val(X1,new_york_0))),
% 18.36/7.88 inference(cnf_transformation,[status(thm)],[f20816])).
% 18.36/7.88 fof(f20820,plain,(
% 18.36/7.88 sub(c4,freiheitsstatue_1_1)),
% 18.36/7.88 inference(cnf_transformation,[status(thm)],[f10190])).
% 18.36/7.88 fof(f20821,plain,(
% 18.36/7.88 attr(c41,c42)),
% 18.36/7.88 inference(cnf_transformation,[status(thm)],[f10190])).
% 18.36/7.88 fof(f20823,plain,(
% 18.36/7.88 sub(c42,name_1_1)),
% 18.36/7.88 inference(cnf_transformation,[status(thm)],[f10190])).
% 18.36/7.88 fof(f20824,plain,(
% 18.36/7.88 val(c42,new_york_0)),
% 18.36/7.88 inference(cnf_transformation,[status(thm)],[f10190])).
% 18.36/7.88 fof(f20829,plain,(
% 18.36/7.88 loc(c8,c53)),
% 18.36/7.88 inference(cnf_transformation,[status(thm)],[f10190])).
% 18.36/7.88 fof(f20830,plain,(
% 18.36/7.88 scar(c8,c4)),
% 18.36/7.88 inference(cnf_transformation,[status(thm)],[f10190])).
% 18.36/7.88 fof(f20831,plain,(
% 18.36/7.88 subs(c8,stehen_1_1)),
% 18.36/7.88 inference(cnf_transformation,[status(thm)],[f10190])).
% 18.36/7.88 fof(f20976,definition,(
% 18.36/7.88 ![X0,X1]: (sQ0_spl <=> (~attr(X0,X1)|~sub(X1,name_1_1)|~val(X1,new_york_0)))),
% 18.36/7.88 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 18.36/7.88 fof(f20977,plain,(
% 18.36/7.88 ![X0,X1]: (~attr(X0,X1)|~sub(X1,name_1_1)|~val(X1,new_york_0)|~sQ0_spl)),
% 18.36/7.88 inference(component_clause,[status(thm)],[f20976])).
% 18.36/7.88 fof(f20979,definition,(
% 18.36/7.88 ![X2,X3,X4]: (sQ1_spl <=> (~loc(X2,X3)|~scar(X2,X4)|~sub(X4,freiheitsstatue_1_1)|~subs(X2,stehen_1_1)))),
% 18.36/7.88 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 18.36/7.88 fof(f20980,plain,(
% 18.36/7.88 ![X0,X1,X2]: (~loc(X0,X1)|~scar(X0,X2)|~sub(X2,freiheitsstatue_1_1)|~subs(X0,stehen_1_1)|~sQ1_spl)),
% 18.36/7.88 inference(component_clause,[status(thm)],[f20979])).
% 18.36/7.88 fof(f20982,plain,(
% 18.36/7.88 sQ0_spl|sQ1_spl),
% 18.36/7.88 inference(split_clause,[status(thm)],[f20817,f20976,f20979])).
% 18.36/7.88 fof(f20987,plain,(
% 18.36/7.88 ![X0]: (~attr(X0,c42)|~sub(c42,name_1_1)|~sQ0_spl)),
% 18.36/7.88 inference(resolution,[status(thm)],[f20824,f20977])).
% 18.36/7.88 fof(f20988,definition,(
% 18.36/7.88 ![X0]: (sQ2_spl <=> (~attr(X0,c42)))),
% 18.36/7.88 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 18.36/7.88 fof(f20989,plain,(
% 18.36/7.88 ![X0]: (~attr(X0,c42)|~sQ2_spl)),
% 18.36/7.88 inference(component_clause,[status(thm)],[f20988])).
% 18.36/7.88 fof(f20991,definition,(
% 18.36/7.88 sQ3_spl <=> (sub(c42,name_1_1))),
% 18.36/7.88 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 18.36/7.88 fof(f20993,plain,(
% 18.36/7.88 ~sub(c42,name_1_1)|sQ3_spl),
% 18.36/7.88 inference(component_clause,[status(thm)],[f20991])).
% 18.36/7.88 fof(f20994,plain,(
% 18.36/7.88 sQ2_spl|~sQ3_spl|~sQ0_spl),
% 18.36/7.88 inference(split_clause,[status(thm)],[f20987,f20988,f20991,f20976])).
% 18.36/7.88 fof(f21029,plain,(
% 18.36/7.88 $false|sQ3_spl),
% 18.36/7.88 inference(forward_subsumption_resolution,[status(thm)],[f20823,f20993])).
% 18.36/7.88 fof(f21030,plain,(
% 18.36/7.88 sQ3_spl),
% 18.36/7.88 inference(contradiction_clause,[status(thm)],[f21029])).
% 18.36/7.88 fof(f21033,plain,(
% 18.36/7.88 $false|~sQ2_spl),
% 18.36/7.88 inference(backward_subsumption_resolution,[status(thm)],[f20821,f20989])).
% 18.36/7.88 fof(f21034,plain,(
% 18.36/7.88 ~sQ2_spl),
% 18.36/7.88 inference(contradiction_clause,[status(thm)],[f21033])).
% 18.36/7.88 fof(f21062,plain,(
% 18.36/7.88 ![X0]: (~loc(c8,X0)|~sub(c4,freiheitsstatue_1_1)|~subs(c8,stehen_1_1)|~sQ1_spl)),
% 18.36/7.88 inference(resolution,[status(thm)],[f20830,f20980])).
% 18.36/7.88 fof(f21064,definition,(
% 18.36/7.88 ![X0]: (sQ4_spl <=> (~loc(c8,X0)))),
% 18.36/7.88 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 18.36/7.88 fof(f21065,plain,(
% 18.36/7.88 ![X0]: (~loc(c8,X0)|~sQ4_spl)),
% 18.36/7.88 inference(component_clause,[status(thm)],[f21064])).
% 18.36/7.88 fof(f21067,definition,(
% 18.36/7.88 sQ5_spl <=> (sub(c4,freiheitsstatue_1_1))),
% 18.36/7.88 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 18.36/7.88 fof(f21069,plain,(
% 18.36/7.88 ~sub(c4,freiheitsstatue_1_1)|sQ5_spl),
% 18.36/7.88 inference(component_clause,[status(thm)],[f21067])).
% 18.36/7.88 fof(f21070,definition,(
% 18.36/7.88 sQ6_spl <=> (subs(c8,stehen_1_1))),
% 18.36/7.88 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 18.36/7.88 fof(f21072,plain,(
% 18.36/7.88 ~subs(c8,stehen_1_1)|sQ6_spl),
% 18.36/7.88 inference(component_clause,[status(thm)],[f21070])).
% 18.36/7.88 fof(f21073,plain,(
% 18.36/7.88 sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ1_spl),
% 18.36/7.88 inference(split_clause,[status(thm)],[f21062,f21064,f21067,f21070,f20979])).
% 18.36/7.88 fof(f21078,plain,(
% 18.36/7.88 $false|sQ6_spl),
% 18.36/7.88 inference(forward_subsumption_resolution,[status(thm)],[f21072,f20831])).
% 18.36/7.88 fof(f21079,plain,(
% 18.36/7.88 sQ6_spl),
% 18.36/7.88 inference(contradiction_clause,[status(thm)],[f21078])).
% 18.36/7.88 fof(f21080,plain,(
% 18.36/7.88 $false|~sQ4_spl),
% 18.36/7.88 inference(backward_subsumption_resolution,[status(thm)],[f20829,f21065])).
% 18.36/7.88 fof(f21082,plain,(
% 18.36/7.88 ~sQ4_spl),
% 18.36/7.88 inference(contradiction_clause,[status(thm)],[f21080])).
% 18.36/7.88 fof(f21083,plain,(
% 18.36/7.88 $false|sQ5_spl),
% 18.36/7.88 inference(forward_subsumption_resolution,[status(thm)],[f21069,f20820])).
% 17.75/7.96 fof(f21084,plain,(
% 17.75/7.96 sQ5_spl),
% 17.75/7.96 inference(contradiction_clause,[status(thm)],[f21083])).
% 17.75/7.96 fof(f21085,plain,(
% 17.75/7.96 $false),
% 17.75/7.96 inference(sat_refutation,[status(thm)],[f20982,f20994,f21030,f21034,f21073,f21079,f21082,f21084])).
% 17.75/7.96 % SZS output end CNFRefutation for theBenchmark.p
% 17.75/7.98 % Elapsed time: 2.568225 seconds
% 17.75/7.98 % CPU time: 19.320218 seconds
% 17.75/7.98 % Total memory used: 521.036 MB
% 17.75/7.98 % Net memory used: 511.187 MB
%------------------------------------------------------------------------------