%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR114+19 : 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 : n020.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:21 PM UTC 2026
% Result : Theorem 73.73s 10.02s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR114+19 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.40 % Computer : n020.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Mon Sep 21 15:05:48 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.39/0.66 % Drodi V4.1.1
% 73.73/10.02 % Refutation found
% 73.73/10.02 % SZS status Theorem for theBenchmark: Theorem is valid
% 73.73/10.02 % SZS output start CNFRefutation for theBenchmark
% 73.73/10.02 fof(f180,axiom,(
% 73.73/10.02 (! [X0,X1] :( loc(X0,X1)=> (? [X2] :( loc(X2,X1)& scar(X2,X0)& subs(X2,stehen_1_1) ) )) )),
% 73.73/10.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 73.73/10.02 fof(f10188,conjecture,(
% 73.73/10.02 (? [X0,X1,X2,X3,X4] :( in(X2,X0)& attr(X0,X1)& loc(X4,X2)& scar(X4,X3)& sub(X1,name_1_1)& sub(X0,stadt__1_1)& sub(X3,kolosseum_1_1)& subs(X4,stehen_1_1)& val(X1,rom_0) ) )),
% 73.73/10.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 73.73/10.02 fof(f10189,negated_conjecture,(
% 73.73/10.02 ~((? [X0,X1,X2,X3,X4] :( in(X2,X0)& attr(X0,X1)& loc(X4,X2)& scar(X4,X3)& sub(X1,name_1_1)& sub(X0,stadt__1_1)& sub(X3,kolosseum_1_1)& subs(X4,stehen_1_1)& val(X1,rom_0) ) ))),
% 73.73/10.02 inference(negated_conjecture,[status(cth)],[f10188])).
% 73.73/10.02 fof(f10190,hypothesis,(
% 73.73/10.02 ( assoc(c10,c0)& assoc(c10,c130)& ctxt(c10,c171)& loc(c10,c170)& obj(c10,c150)& scar(c10,c127)& subs(c10,haben_1_1)& temp(c10,abend_2_1)& temp(c10,c135)& attr(c127,c128)& attr(c127,c129)& sub(c127,kirchenf__374rst_1_1)& sub(c128,eigenname_1_1)& val(c128,johannes_0)& sub(c129,familiename_1_1)& val(c129,paul_0)& sub(c135,freiertag_1_1)& loc(c140,c169)& sub(c140,kolosseum_1_1)& attr(c147,c148)& sub(c147,stadt__1_1)& sub(c148,name_1_1)& val(c148,rom_0)& prop(c150,althergebracht_1_1)& sub(c150,kreuzung_1_1)& in(c169,c147)& an(c170,c140)& subm(c171,c9)& pred(c9,gl__344ubig_2_1)& assoc(kreuzung_1_1,kreuz_1_1)& sub(kreuzung_1_1,weg_1_1)& chsp2(zelebrieren_1_1,c0)& sort(c10,st)& fact(c10,real)& gener(c10,sp)& sort(c0,tq)& sort(c130,oq)& card(c130,int2)& sort(c171,o)& card(c171,card_c)& etype(c171,int1)& fact(c171,real)& gener(c171,gener_c)& quant(c171,quant_c)& refer(c171,refer_c)& varia(c171,varia_c)& sort(c170,l)& card(c170,int1)& etype(c170,int0)& fact(c170,real)& gener(c170,sp)& quant(c170,one)& refer(c170,det)& varia(c170,con)& sort(c150,d)& card(c150,int1)& etype(c150,int0)& fact(c150,real)& gener(c150,sp)& quant(c150,one)& refer(c150,det)& varia(c150,con)& sort(c127,d)& card(c127,int1)& etype(c127,int0)& fact(c127,real)& gener(c127,sp)& quant(c127,one)& refer(c127,det)& varia(c127,varia_c)& sort(haben_1_1,st)& fact(haben_1_1,real)& gener(haben_1_1,ge)& sort(abend_2_1,t)& card(abend_2_1,int1)& etype(abend_2_1,int0)& fact(abend_2_1,real)& gener(abend_2_1,sp)& quant(abend_2_1,one)& refer(abend_2_1,refer_c)& varia(abend_2_1,varia_c)& sort(c135,ta)& card(c135,int1)& etype(c135,int0)& fact(c135,real)& gener(c135,sp)& quant(c135,one)& refer(c135,det)& varia(c135,con)& sort(c128,na)& card(c128,int1)& etype(c128,int0)& fact(c128,real)& gener(c128,sp)& quant(c128,one)& refer(c128,indet)& varia(c128,varia_c)& sort(c129,na)& card(c129,int1)& etype(c129,int0)& fact(c129,real)& gener(c129,sp)& quant(c129,one)& refer(c129,det)& varia(c129,varia_c)& sort(kirchenf__374rst_1_1,d)& card(kirchenf__374rst_1_1,int1)& etype(kirchenf__374rst_1_1,int0)& fact(kirchenf__374rst_1_1,real)& gener(kirchenf__374rst_1_1,ge)& quant(kirchenf__374rst_1_1,one)& refer(kirchenf__374rst_1_1,refer_c)& varia(kirchenf__374rst_1_1,varia_c)& sort(eigenname_1_1,na)& card(eigenname_1_1,int1)& etype(eigenname_1_1,int0)& fact(eigenname_1_1,real)& gener(eigenname_1_1,ge)& quant(eigenname_1_1,one)& refer(eigenname_1_1,refer_c)& varia(eigenname_1_1,varia_c)& sort(johannes_0,fe)& sort(familiename_1_1,na)& card(familiename_1_1,int1)& etype(familiename_1_1,int0)& fact(familiename_1_1,real)& gener(familiename_1_1,ge)& quant(familiename_1_1,one)& refer(familiename_1_1,refer_c)& varia(familiename_1_1,varia_c)& sort(paul_0,fe)& sort(freiertag_1_1,ta)& card(freiertag_1_1,int1)& etype(freiertag_1_1,int0)& fact(freiertag_1_1,real)& gener(freiertag_1_1,ge)& quant(freiertag_1_1,one)& refer(freiertag_1_1,refer_c)& varia(freiertag_1_1,varia_c)& sort(c140,d)& card(c140,int1)& etype(c140,int0)& fact(c140,real)& gener(c140,sp)& quant(c140,one)& refer(c140,det)& varia(c140,con)& sort(c169,l)& card(c169,int1)& etype(c169,int0)& fact(c169,real)& gener(c169,sp)& quant(c169,one)& refer(c169,det)& varia(c169,con)& sort(kolosseum_1_1,d)& card(kolosseum_1_1,int1)& etype(kolosseum_1_1,int0)& fact(kolosseum_1_1,real)& gener(kolosseum_1_1,sp)& quant(kolosseum_1_1,one)& refer(kolosseum_1_1,det)& varia(kolosseum_1_1,con)& sort(c147,d)& sort(c147,io)& card(c147,int1)& etype(c147,int0)& fact(c147,real)& gener(c147,sp)& quant(c147,one)& refer(c147,det)& varia(c147,con)& sort(c148,na)& card(c148,int1)& etype(c148,int0)& fact(c148,real)& gener(c148,sp)& quant(c148,one)& refer(c148,indet)& varia(c148,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)& sort(althergebracht_1_1,nq)& sort(kreuzung_1_1,d)& card(kreuzung_1_1,int1)& etype(kreuzung_1_1,int0)& fact(kreuzung_1_1,real)& gener(kreuzung_1_1,ge)& quant(kreuzung_1_1,one)& refer(kreuzung_1_1,refer_c)& varia(kreuzung_1_1,varia_c)& sort(c9,o)& card(c9,cons(x_constant,cons(int1,nil)))& etype(c9,int1)& fact(c9,real)& gener(c9,gener_c)& quant(c9,mult)& refer(c9,indet)& varia(c9,varia_c)& sort(gl__344ubig_2_1,o)& card(gl__344ubig_2_1,int1)& etype(gl__344ubig_2_1,int0)& fact(gl__344ubig_2_1,real)& gener(gl__344ubig_2_1,ge)& quant(gl__344ubig_2_1,one)& refer(gl__344ubig_2_1,refer_c)& varia(gl__344ubig_2_1,varia_c)& sort(kreuz_1_1,d)& sort(kreuz_1_1,io)& card(kreuz_1_1,int1)& etype(kreuz_1_1,int0)& fact(kreuz_1_1,real)& gener(kreuz_1_1,ge)& quant(kreuz_1_1,one)& refer(kreuz_1_1,refer_c)& varia(kreuz_1_1,varia_c)& sort(weg_1_1,d)& card(weg_1_1,int1)& etype(weg_1_1,int0)& fact(weg_1_1,real)& gener(weg_1_1,ge)& quant(weg_1_1,one)& refer(weg_1_1,refer_c)& varia(weg_1_1,varia_c)& sort(zelebrieren_1_1,da)& fact(zelebrieren_1_1,real)& gener(zelebrieren_1_1,ge) ) ),
% 73.73/10.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 73.73/10.02 fof(f10801,plain,(
% 73.73/10.02 ![X0,X1]: (~loc(X0,X1)|(?[X2]: ((loc(X2,X1)&scar(X2,X0))&subs(X2,stehen_1_1))))),
% 73.73/10.02 inference(pre_NNF_transformation,[status(thm)],[f180])).
% 73.73/10.02 fof(f10802,plain,(
% 73.73/10.02 ![X0,X1]: (~loc(X0,X1)|((loc(sK62_skl(X1,X0),X1)&scar(sK62_skl(X1,X0),X0))&subs(sK62_skl(X1,X0),stehen_1_1)))),
% 73.73/10.02 inference(skolemize,[status(esa),new_symbols(skolem,[sK62_skl]),skolemize(X2,sK62_skl(X1,X0))],[f10801])).
% 73.73/10.02 fof(f10803,plain,(
% 73.73/10.02 ![X0,X1]: (~loc(X0,X1)|loc(sK62_skl(X1,X0),X1))),
% 73.73/10.02 inference(cnf_transformation,[status(thm)],[f10802])).
% 73.73/10.02 fof(f10804,plain,(
% 73.73/10.02 ![X0,X1]: (~loc(X0,X1)|scar(sK62_skl(X1,X0),X0))),
% 73.73/10.02 inference(cnf_transformation,[status(thm)],[f10802])).
% 73.73/10.02 fof(f10805,plain,(
% 73.73/10.02 ![X0,X1]: (~loc(X0,X1)|subs(sK62_skl(X1,X0),stehen_1_1))),
% 73.73/10.02 inference(cnf_transformation,[status(thm)],[f10802])).
% 73.73/10.02 fof(f20815,plain,(
% 73.73/10.02 (![X0,X1,X2,X3,X4]: ((((((((~in(X2,X0)|~attr(X0,X1))|~loc(X4,X2))|~scar(X4,X3))|~sub(X1,name_1_1))|~sub(X0,stadt__1_1))|~sub(X3,kolosseum_1_1))|~subs(X4,stehen_1_1))|~val(X1,rom_0)))),
% 73.73/10.02 inference(pre_NNF_transformation,[status(thm)],[f10189])).
% 73.73/10.02 fof(f20816,plain,(
% 73.73/10.02 ![X1]: ((![X4]: ((![X3]: ((![X0]: ((((![X2]: ((~in(X2,X0)|~attr(X0,X1))|~loc(X4,X2)))|~scar(X4,X3))|~sub(X1,name_1_1))|~sub(X0,stadt__1_1)))|~sub(X3,kolosseum_1_1)))|~subs(X4,stehen_1_1)))|~val(X1,rom_0))),
% 73.73/10.02 inference(miniscoping,[status(thm)],[f20815])).
% 73.73/10.02 fof(f20817,plain,(
% 73.73/10.02 ![X0,X1,X2,X3,X4]: (~in(X0,X1)|~attr(X1,X2)|~loc(X3,X0)|~scar(X3,X4)|~sub(X2,name_1_1)|~sub(X1,stadt__1_1)|~sub(X4,kolosseum_1_1)|~subs(X3,stehen_1_1)|~val(X2,rom_0))),
% 73.73/10.02 inference(cnf_transformation,[status(thm)],[f20816])).
% 73.73/10.02 fof(f20835,plain,(
% 73.73/10.02 loc(c140,c169)),
% 73.73/10.02 inference(cnf_transformation,[status(thm)],[f10190])).
% 73.73/10.02 fof(f20836,plain,(
% 73.73/10.02 sub(c140,kolosseum_1_1)),
% 73.73/10.02 inference(cnf_transformation,[status(thm)],[f10190])).
% 73.73/10.02 fof(f20837,plain,(
% 73.73/10.02 attr(c147,c148)),
% 73.73/10.02 inference(cnf_transformation,[status(thm)],[f10190])).
% 73.73/10.02 fof(f20838,plain,(
% 73.73/10.02 sub(c147,stadt__1_1)),
% 73.73/10.02 inference(cnf_transformation,[status(thm)],[f10190])).
% 73.73/10.02 fof(f20839,plain,(
% 73.73/10.02 sub(c148,name_1_1)),
% 73.73/10.02 inference(cnf_transformation,[status(thm)],[f10190])).
% 73.73/10.02 fof(f20840,plain,(
% 73.73/10.02 val(c148,rom_0)),
% 73.73/10.02 inference(cnf_transformation,[status(thm)],[f10190])).
% 73.73/10.02 fof(f20843,plain,(
% 73.73/10.02 in(c169,c147)),
% 73.73/10.02 inference(cnf_transformation,[status(thm)],[f10190])).
% 73.73/10.02 fof(f21096,plain,(
% 73.73/10.02 ![X0,X1,X2,X3]: (~in(X0,X1)|~attr(X1,X2)|~loc(X3,X0)|~scar(X3,c140)|~sub(X2,name_1_1)|~sub(X1,stadt__1_1)|~subs(X3,stehen_1_1)|~val(X2,rom_0))),
% 73.73/10.02 inference(resolution,[status(thm)],[f20836,f20817])).
% 73.73/10.02 fof(f21097,plain,(
% 73.73/10.02 ![X0,X1,X2]: (~in(X0,X1)|~attr(X1,c148)|~loc(X2,X0)|~scar(X2,c140)|~sub(c148,name_1_1)|~sub(X1,stadt__1_1)|~subs(X2,stehen_1_1))),
% 73.73/10.02 inference(resolution,[status(thm)],[f20840,f21096])).
% 73.73/10.02 fof(f21099,definition,(
% 73.73/10.02 ![X0,X1,X2]: (sQ0_spl <=> (~in(X0,X1)|~attr(X1,c148)|~loc(X2,X0)|~scar(X2,c140)|~sub(X1,stadt__1_1)|~subs(X2,stehen_1_1)))),
% 73.73/10.02 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 73.73/10.02 fof(f21100,plain,(
% 73.73/10.02 ![X0,X1,X2]: (~in(X0,X1)|~attr(X1,c148)|~loc(X2,X0)|~scar(X2,c140)|~sub(X1,stadt__1_1)|~subs(X2,stehen_1_1)|~sQ0_spl)),
% 73.73/10.02 inference(component_clause,[status(thm)],[f21099])).
% 73.73/10.02 fof(f21102,definition,(
% 73.73/10.02 sQ1_spl <=> (sub(c148,name_1_1))),
% 73.73/10.02 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 73.73/10.02 fof(f21104,plain,(
% 73.73/10.02 ~sub(c148,name_1_1)|sQ1_spl),
% 73.73/10.02 inference(component_clause,[status(thm)],[f21102])).
% 73.73/10.02 fof(f21105,plain,(
% 73.73/10.02 sQ0_spl|~sQ1_spl),
% 73.73/10.02 inference(split_clause,[status(thm)],[f21097,f21099,f21102])).
% 73.73/10.02 fof(f21110,plain,(
% 73.73/10.02 $false|sQ1_spl),
% 73.73/10.02 inference(forward_subsumption_resolution,[status(thm)],[f21104,f20839])).
% 73.73/10.02 fof(f21111,plain,(
% 73.73/10.02 sQ1_spl),
% 73.73/10.02 inference(contradiction_clause,[status(thm)],[f21110])).
% 73.73/10.02 fof(f21118,plain,(
% 73.73/10.02 ![X0,X1]: (~in(X0,c147)|~loc(X1,X0)|~scar(X1,c140)|~sub(c147,stadt__1_1)|~subs(X1,stehen_1_1)|~sQ0_spl)),
% 73.73/10.02 inference(resolution,[status(thm)],[f20837,f21100])).
% 73.73/10.02 fof(f21122,definition,(
% 73.73/10.02 sQ4_spl <=> (sub(c147,stadt__1_1))),
% 73.73/10.02 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 73.73/10.02 fof(f21124,plain,(
% 73.73/10.02 ~sub(c147,stadt__1_1)|sQ4_spl),
% 73.73/10.02 inference(component_clause,[status(thm)],[f21122])).
% 73.73/10.02 fof(f21126,definition,(
% 73.73/10.02 ![X0,X1]: (sQ5_spl <=> (~in(X0,c147)|~loc(X1,X0)|~scar(X1,c140)|~subs(X1,stehen_1_1)))),
% 73.73/10.02 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 73.73/10.02 fof(f21127,plain,(
% 73.73/10.02 ![X0,X1]: (~in(X0,c147)|~loc(X1,X0)|~scar(X1,c140)|~subs(X1,stehen_1_1)|~sQ5_spl)),
% 73.73/10.02 inference(component_clause,[status(thm)],[f21126])).
% 73.73/10.02 fof(f21129,plain,(
% 73.73/10.02 sQ5_spl|~sQ4_spl|~sQ0_spl),
% 73.73/10.02 inference(split_clause,[status(thm)],[f21118,f21126,f21122,f21099])).
% 73.73/10.02 fof(f21130,plain,(
% 73.73/10.02 $false|sQ4_spl),
% 73.73/10.02 inference(forward_subsumption_resolution,[status(thm)],[f21124,f20838])).
% 73.73/10.02 fof(f21131,plain,(
% 73.73/10.02 sQ4_spl),
% 73.73/10.02 inference(contradiction_clause,[status(thm)],[f21130])).
% 73.73/10.02 fof(f21137,plain,(
% 73.73/10.02 ![X0,X1,X2]: (~loc(X0,X1)|~in(X2,c147)|~loc(sK62_skl(X1,X0),X2)|~scar(sK62_skl(X1,X0),c140)|~sQ5_spl)),
% 73.73/10.02 inference(resolution,[status(thm)],[f10805,f21127])).
% 73.73/10.02 fof(f21142,plain,(
% 73.73/10.02 ![X0,X1]: (~loc(c140,X0)|~loc(c140,X0)|~in(X1,c147)|~loc(sK62_skl(X0,c140),X1)|~sQ5_spl)),
% 73.73/10.02 inference(resolution,[status(thm)],[f10804,f21137])).
% 73.73/10.02 fof(f21145,plain,(
% 73.73/10.02 ![X0,X1]: (~loc(c140,X0)|~in(X1,c147)|~loc(sK62_skl(X0,c140),X1)|~sQ5_spl)),
% 73.73/10.02 inference(duplicate_literals_removal,[status(thm)],[f21142])).
% 73.73/10.02 fof(f21149,plain,(
% 73.73/10.02 ![X0]: (~loc(c140,X0)|~loc(sK62_skl(X0,c140),c169)|~sQ5_spl)),
% 73.73/10.02 inference(resolution,[status(thm)],[f21145,f20843])).
% 73.73/10.02 fof(f21150,plain,(
% 73.73/10.02 ~loc(c140,c169)|~loc(c140,c169)|~sQ5_spl),
% 73.73/10.02 inference(resolution,[status(thm)],[f21149,f10803])).
% 73.73/10.02 fof(f21152,definition,(
% 73.73/10.02 sQ6_spl <=> (loc(c140,c169))),
% 73.73/10.02 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 73.73/10.02 fof(f21154,plain,(
% 73.73/10.02 ~loc(c140,c169)|sQ6_spl),
% 73.73/10.02 inference(component_clause,[status(thm)],[f21152])).
% 73.73/10.02 fof(f21155,plain,(
% 73.73/10.02 ~sQ6_spl|~sQ5_spl),
% 73.73/10.02 inference(split_clause,[status(thm)],[f21150,f21152,f21126])).
% 73.73/10.02 fof(f21156,plain,(
% 73.73/10.02 $false|sQ6_spl),
% 73.73/10.02 inference(forward_subsumption_resolution,[status(thm)],[f21154,f20835])).
% 73.73/10.02 fof(f21157,plain,(
% 73.73/10.02 sQ6_spl),
% 73.73/10.02 inference(contradiction_clause,[status(thm)],[f21156])).
% 73.73/10.02 fof(f21158,plain,(
% 73.73/10.02 $false),
% 73.73/10.02 inference(sat_refutation,[status(thm)],[f21105,f21111,f21129,f21131,f21155,f21157])).
% 74.16/10.14 % SZS output end CNFRefutation for theBenchmark.p
% 1.61/10.23 % Elapsed time: 9.797508 seconds
% 1.61/10.23 % CPU time: 74.434853 seconds
% 1.61/10.23 % Total memory used: 612.513 MB
% 1.61/10.23 % Net memory used: 594.187 MB
%------------------------------------------------------------------------------