%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR114+25 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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:13:53 PM UTC 2026
% Result : Theorem 24.47s 3.70s
% Output : CNFRefutation 25.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 11
% Syntax : Number of formulae : 57 ( 15 unt; 8 def)
% Number of atoms : 383 ( 0 equ)
% Maximal formula atoms : 215 ( 6 avg)
% Number of connectives : 421 ( 95 ~; 81 |; 236 &)
% ( 8 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 215 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 37 ( 36 usr; 9 prp; 0-2 aty)
% Number of functors : 65 ( 65 usr; 63 con; 0-2 aty)
% Number of variables : 57 ( 45 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f180,axiom,
! [X0,X1] :
( loc(X0,X1)
=> ? [X2] :
( subs(X2,stehen_1_1)
& scar(X2,X0)
& loc(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10188,conjecture,
? [X0,X1,X2,X3,X4] :
( val(X1,rom_0)
& subs(X4,stehen_1_1)
& sub(X3,kolosseum_1_1)
& sub(X0,stadt__1_1)
& sub(X1,name_1_1)
& scar(X4,X3)
& loc(X4,X2)
& attr(X0,X1)
& in(X2,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10189,negated_conjecture,
~ ? [X0,X1,X2,X3,X4] :
( val(X1,rom_0)
& subs(X4,stehen_1_1)
& sub(X3,kolosseum_1_1)
& sub(X0,stadt__1_1)
& sub(X1,name_1_1)
& scar(X4,X3)
& loc(X4,X2)
& attr(X0,X1)
& in(X2,X0) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,hypothesis,
( varia(art_1_1,varia_c)
& refer(art_1_1,refer_c)
& quant(art_1_1,quant_c)
& gener(art_1_1,ge)
& fact(art_1_1,real)
& etype(art_1_1,int1)
& card(art_1_1,card_c)
& sort(art_1_1,ad)
& varia(c9853,varia_c)
& refer(c9853,det)
& quant(c9853,one)
& gener(c9853,sp)
& fact(c9853,real)
& etype(c9853,int1)
& card(c9853,int1)
& sort(c9853,ad)
& sort(spaet_1_1,mq)
& varia(anlage_1_1,varia_c)
& refer(anlage_1_1,refer_c)
& quant(anlage_1_1,one)
& gener(anlage_1_1,ge)
& fact(anlage_1_1,real)
& etype(anlage_1_1,int0)
& card(anlage_1_1,int1)
& sort(anlage_1_1,as)
& varia(technik__1_1,varia_c)
& refer(technik__1_1,refer_c)
& quant(technik__1_1,one)
& gener(technik__1_1,ge)
& fact(technik__1_1,real)
& etype(technik__1_1,int0)
& card(technik__1_1,int1)
& sort(technik__1_1,io)
& varia(man_1_1,varia_c)
& refer(man_1_1,refer_c)
& quant(man_1_1,one)
& gener(man_1_1,ge)
& fact(man_1_1,real)
& etype(man_1_1,int0)
& card(man_1_1,int1)
& sort(man_1_1,d)
& gener(geben_1_4,ge)
& fact(geben_1_4,real)
& sort(geben_1_4,da)
& varia(c9837,con)
& refer(c9837,det)
& quant(c9837,one)
& gener(c9837,sp)
& fact(c9837,real)
& etype(c9837,int0)
& card(c9837,int1)
& sort(c9837,io)
& gener(nicht_1_1,gener_c)
& fact(nicht_1_1,real)
& sort(nicht_1_1,md)
& sort(wie_1_1,mq)
& varia(c9847,varia_c)
& refer(c9847,det)
& quant(c9847,mult)
& gener(c9847,sp)
& fact(c9847,real)
& etype(c9847,int1)
& card(c9847,cons(x_constant,cons(int1,nil)))
& sort(c9847,as)
& varia(c9825,varia_c)
& refer(c9825,det)
& quant(c9825,one)
& gener(c9825,sp)
& fact(c9825,real)
& etype(c9825,int0)
& card(c9825,int1)
& sort(c9825,o)
& gener(haben_1_1,ge)
& fact(haben_1_1,real)
& sort(haben_1_1,st)
& varia(c4,varia_c)
& refer(c4,refer_c)
& quant(c4,one)
& gener(c4,ge)
& fact(c4,real)
& etype(c4,int0)
& card(c4,int1)
& sort(c4,d)
& gener(c24,sp)
& fact(c24,real)
& sort(c24,da)
& gener(c21,sp)
& fact(c21,real)
& sort(c21,st)
& varia(bau_1_1,varia_c)
& refer(bau_1_1,refer_c)
& quant(bau_1_1,one)
& gener(bau_1_1,ge)
& fact(bau_1_1,real)
& etype(bau_1_1,int0)
& card(bau_1_1,int1)
& sort(bau_1_1,d)
& varia(c20,varia_c)
& refer(c20,det)
& quant(c20,mult)
& gener(c20,sp)
& fact(c20,real)
& etype(c20,int1)
& card(c20,cons(x_constant,cons(int1,nil)))
& sort(c20,d)
& sort(rom_0,fe)
& varia(name_1_1,varia_c)
& refer(name_1_1,refer_c)
& quant(name_1_1,one)
& gener(name_1_1,ge)
& fact(name_1_1,real)
& etype(name_1_1,int0)
& card(name_1_1,int1)
& sort(name_1_1,na)
& varia(stadt__1_1,varia_c)
& refer(stadt__1_1,refer_c)
& quant(stadt__1_1,one)
& gener(stadt__1_1,ge)
& fact(stadt__1_1,real)
& etype(stadt__1_1,int0)
& card(stadt__1_1,int1)
& sort(stadt__1_1,io)
& sort(stadt__1_1,d)
& varia(c13132,varia_c)
& refer(c13132,indet)
& quant(c13132,one)
& gener(c13132,sp)
& fact(c13132,real)
& etype(c13132,int0)
& card(c13132,int1)
& sort(c13132,na)
& varia(c13131,con)
& refer(c13131,det)
& quant(c13131,one)
& gener(c13131,sp)
& fact(c13131,real)
& etype(c13131,int0)
& card(c13131,int1)
& sort(c13131,io)
& sort(c13131,d)
& varia(kolosseum_1_1,con)
& refer(kolosseum_1_1,det)
& quant(kolosseum_1_1,one)
& gener(kolosseum_1_1,sp)
& fact(kolosseum_1_1,real)
& etype(kolosseum_1_1,int0)
& card(kolosseum_1_1,int1)
& sort(kolosseum_1_1,d)
& varia(c13134,con)
& refer(c13134,det)
& quant(c13134,one)
& gener(c13134,sp)
& fact(c13134,real)
& etype(c13134,int0)
& card(c13134,int1)
& sort(c13134,l)
& varia(c13125,con)
& refer(c13125,det)
& quant(c13125,one)
& gener(c13125,sp)
& fact(c13125,real)
& etype(c13125,int0)
& card(c13125,int1)
& sort(c13125,d)
& varia(er_fahrung_1_1,varia_c)
& refer(er_fahrung_1_1,refer_c)
& quant(er_fahrung_1_1,one)
& gener(er_fahrung_1_1,ge)
& fact(er_fahrung_1_1,real)
& etype(er_fahrung_1_1,int0)
& card(er_fahrung_1_1,int1)
& sort(er_fahrung_1_1,io)
& sort(er_fahrung_1_1,as)
& varia(c11,varia_c)
& refer(c11,indet)
& quant(c11,mult)
& gener(c11,sp)
& fact(c11,nonreal)
& etype(c11,int1)
& card(c11,cons(x_constant,cons(int1,nil)))
& sort(c11,io)
& sort(c11,as)
& sort(c0,tq)
& gener(auskl__374geln_1_1,ge)
& fact(auskl__374geln_1_1,real)
& sort(auskl__374geln_1_1,dn)
& subs(c9853,art_1_1)
& attch(c9853,c9847)
& prop(c9847,spaet_1_1)
& preds(c9847,anlage_1_1)
& sub(c9837,technik__1_1)
& prop(c9837,c0)
& sub(c4,man_1_1)
& subs(c24,geben_1_4)
& obj(c24,c9837)
& modl(c24,nicht_1_1)
& mannr(c24,wie_1_1)
& circ(c24,c9847)
& benf(c24,c13125)
& agt(c24,c9825)
& subs(c21,haben_1_1)
& scar(c21,c4)
& reas(c21,c24)
& obj(c21,c11)
& assoc(c21,c20)
& pred(c20,bau_1_1)
& in(c13134,c13131)
& val(c13132,rom_0)
& sub(c13132,name_1_1)
& sub(c13131,stadt__1_1)
& attr(c13131,c13132)
& sub(c13125,kolosseum_1_1)
& loc(c13125,c13134)
& pred(c11,er_fahrung_1_1)
& chsp2(auskl__374geln_1_1,c0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10801,plain,
! [X0,X1] :
( ? [X2] :
( subs(X2,stehen_1_1)
& scar(X2,X0)
& loc(X2,X1) )
| ~ loc(X0,X1) ),
inference(pre_NNF_transformation,[status(thm)],[f180]) ).
fof(f10802,plain,
! [X0,X1] :
( ( subs(sK62_skl(X1,X0),stehen_1_1)
& scar(sK62_skl(X1,X0),X0)
& loc(sK62_skl(X1,X0),X1) )
| ~ loc(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62_skl]),skolemize(X2,sK62_skl(X1,X0))],[f10801]) ).
fof(f10803,plain,
! [X0,X1] :
( loc(sK62_skl(X1,X0),X1)
| ~ loc(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10802]) ).
fof(f10804,plain,
! [X0,X1] :
( scar(sK62_skl(X1,X0),X0)
| ~ loc(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10802]) ).
fof(f10805,plain,
! [X0,X1] :
( subs(sK62_skl(X1,X0),stehen_1_1)
| ~ loc(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10802]) ).
fof(f20815,plain,
! [X0,X1,X2,X3,X4] :
( ~ val(X1,rom_0)
| ~ subs(X4,stehen_1_1)
| ~ sub(X3,kolosseum_1_1)
| ~ sub(X0,stadt__1_1)
| ~ sub(X1,name_1_1)
| ~ scar(X4,X3)
| ~ loc(X4,X2)
| ~ attr(X0,X1)
| ~ in(X2,X0) ),
inference(pre_NNF_transformation,[status(thm)],[f10189]) ).
fof(f20816,plain,
! [X1] :
( ~ val(X1,rom_0)
| ! [X4] :
( ~ subs(X4,stehen_1_1)
| ! [X3] :
( ~ sub(X3,kolosseum_1_1)
| ! [X0] :
( ~ sub(X0,stadt__1_1)
| ~ sub(X1,name_1_1)
| ~ scar(X4,X3)
| ! [X2] :
( ~ loc(X4,X2)
| ~ attr(X0,X1)
| ~ in(X2,X0) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f20815]) ).
fof(f20817,plain,
! [X0,X1,X2,X3,X4] :
( ~ val(X2,rom_0)
| ~ subs(X3,stehen_1_1)
| ~ sub(X4,kolosseum_1_1)
| ~ sub(X1,stadt__1_1)
| ~ sub(X2,name_1_1)
| ~ scar(X3,X4)
| ~ loc(X3,X0)
| ~ attr(X1,X2)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f20816]) ).
fof(f20820,plain,
loc(c13125,c13134),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20821,plain,
sub(c13125,kolosseum_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20822,plain,
attr(c13131,c13132),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20823,plain,
sub(c13131,stadt__1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20824,plain,
sub(c13132,name_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20825,plain,
val(c13132,rom_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20826,plain,
in(c13134,c13131),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f21075,definition,
( sQ1_spl
<=> sub(c13132,name_1_1) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f21077,plain,
( sQ1_spl
| ~ sub(c13132,name_1_1) ),
inference(component_clause,[status(thm)],[f21075]) ).
fof(f21086,plain,
subs(sK62_skl(c13134,c13125),stehen_1_1),
inference(resolution,[status(thm)],[f20820,f10805]) ).
fof(f21088,plain,
! [X0,X1,X2,X3] :
( ~ val(X1,rom_0)
| ~ subs(X2,stehen_1_1)
| ~ sub(X3,kolosseum_1_1)
| ~ sub(X1,name_1_1)
| ~ scar(X2,X3)
| ~ loc(X2,X0)
| ~ attr(c13131,X1)
| ~ in(X0,c13131) ),
inference(resolution,[status(thm)],[f20823,f20817]) ).
fof(f21090,definition,
! [X0,X2,X3] :
( sQ3_spl
<=> ( ~ subs(X2,stehen_1_1)
| ~ sub(X3,kolosseum_1_1)
| ~ scar(X2,X3)
| ~ loc(X2,X0)
| ~ in(X0,c13131) ) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f21091,plain,
! [X0,X1,X2] :
( ~ sQ3_spl
| ~ subs(X1,stehen_1_1)
| ~ sub(X2,kolosseum_1_1)
| ~ scar(X1,X2)
| ~ loc(X1,X0)
| ~ in(X0,c13131) ),
inference(component_clause,[status(thm)],[f21090]) ).
fof(f21093,definition,
! [X1] :
( sQ4_spl
<=> ( ~ val(X1,rom_0)
| ~ sub(X1,name_1_1)
| ~ attr(c13131,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f21094,plain,
! [X0] :
( ~ sQ4_spl
| ~ val(X0,rom_0)
| ~ sub(X0,name_1_1)
| ~ attr(c13131,X0) ),
inference(component_clause,[status(thm)],[f21093]) ).
fof(f21096,plain,
( sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f21088,f21090,f21093]) ).
fof(f21097,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20824,f21077]) ).
fof(f21098,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f21097]) ).
fof(f21101,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sub(X1,kolosseum_1_1)
| ~ scar(sK62_skl(c13134,c13125),X1)
| ~ loc(sK62_skl(c13134,c13125),X0)
| ~ in(X0,c13131) ),
inference(resolution,[status(thm)],[f21086,f21091]) ).
fof(f21108,definition,
! [X2] :
( sQ6_spl
<=> ( ~ sub(X2,kolosseum_1_1)
| ~ scar(sK62_skl(c13134,c13125),X2) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f21109,plain,
! [X0] :
( ~ sQ6_spl
| ~ sub(X0,kolosseum_1_1)
| ~ scar(sK62_skl(c13134,c13125),X0) ),
inference(component_clause,[status(thm)],[f21108]) ).
fof(f21112,definition,
! [X0] :
( sQ7_spl
<=> ( ~ loc(sK62_skl(c13134,c13125),X0)
| ~ in(X0,c13131) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f21113,plain,
! [X0] :
( ~ sQ7_spl
| ~ loc(sK62_skl(c13134,c13125),X0)
| ~ in(X0,c13131) ),
inference(component_clause,[status(thm)],[f21112]) ).
fof(f21115,plain,
( ~ sQ3_spl
| sQ6_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f21101,f21112,f21108,f21090]) ).
fof(f21120,plain,
( ~ sQ4_spl
| ~ sub(c13132,name_1_1)
| ~ attr(c13131,c13132) ),
inference(resolution,[status(thm)],[f21094,f20825]) ).
fof(f21121,definition,
( sQ9_spl
<=> attr(c13131,c13132) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f21123,plain,
( sQ9_spl
| ~ attr(c13131,c13132) ),
inference(component_clause,[status(thm)],[f21121]) ).
fof(f21124,plain,
( ~ sQ4_spl
| ~ sQ1_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f21120,f21121,f21075,f21093]) ).
fof(f21125,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21123,f20822]) ).
fof(f21126,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f21125]) ).
fof(f21150,plain,
loc(sK62_skl(c13134,c13125),c13134),
inference(resolution,[status(thm)],[f10803,f20820]) ).
fof(f21220,plain,
( ~ sQ6_spl
| ~ sub(c13125,kolosseum_1_1)
| ~ loc(c13125,c13134) ),
inference(resolution,[status(thm)],[f10804,f21109]) ).
fof(f21230,definition,
( sQ24_spl
<=> loc(c13125,c13134) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f21232,plain,
( sQ24_spl
| ~ loc(c13125,c13134) ),
inference(component_clause,[status(thm)],[f21230]) ).
fof(f21237,definition,
( sQ26_spl
<=> sub(c13125,kolosseum_1_1) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f21239,plain,
( sQ26_spl
| ~ sub(c13125,kolosseum_1_1) ),
inference(component_clause,[status(thm)],[f21237]) ).
fof(f21240,plain,
( ~ sQ6_spl
| ~ sQ26_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f21220,f21230,f21237,f21108]) ).
fof(f21243,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21232,f20820]) ).
fof(f21244,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f21243]) ).
fof(f21245,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21239,f20821]) ).
fof(f21246,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f21245]) ).
fof(f21294,plain,
( ~ sQ7_spl
| ~ loc(sK62_skl(c13134,c13125),c13134) ),
inference(resolution,[status(thm)],[f21113,f20826]) ).
fof(f21295,plain,
( ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21294,f21150]) ).
fof(f21296,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f21295]) ).
fof(f21297,plain,
$false,
inference(sat_refutation,[status(thm)],[f21096,f21098,f21115,f21124,f21126,f21240,f21244,f21246,f21296]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR114+25 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n016.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 15:09:38 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.24/0.49 % Drodi V4.1.1
% 24.47/3.70 % Refutation found
% 24.47/3.70 % SZS status Theorem for theBenchmark: Theorem is valid
% 24.47/3.70 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 14.56/3.90 % Elapsed time: 3.517070 seconds
% 14.56/3.90 % CPU time: 25.652203 seconds
% 14.56/3.90 % Total memory used: 511.770 MB
% 14.56/3.90 % Net memory used: 505.537 MB
%------------------------------------------------------------------------------