%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR114+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:54 PM UTC 2026
% Result : Theorem 87.85s 22.40s
% Output : CNFRefutation 87.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 14
% Syntax : Number of formulae : 69 ( 17 unt; 11 def)
% Number of atoms : 469 ( 0 equ)
% Maximal formula atoms : 273 ( 6 avg)
% Number of connectives : 506 ( 106 ~; 94 |; 294 &)
% ( 11 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 273 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 36 ( 35 usr; 12 prp; 0-2 aty)
% Number of functors : 69 ( 69 usr; 67 con; 0-2 aty)
% Number of variables : 60 ( 48 !; 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/sandbox2/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/sandbox2/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(eltern_1_1,varia_c)
& refer(eltern_1_1,refer_c)
& quant(eltern_1_1,one)
& gener(eltern_1_1,ge)
& fact(eltern_1_1,real)
& etype(eltern_1_1,int0)
& card(eltern_1_1,int1)
& sort(eltern_1_1,d)
& card(c1,int1970)
& sort(c1,nu)
& varia(jahr__1_1,varia_c)
& refer(jahr__1_1,refer_c)
& quant(jahr__1_1,quant_c)
& gener(jahr__1_1,ge)
& fact(jahr__1_1,real)
& etype(jahr__1_1,etype_c)
& card(jahr__1_1,card_c)
& sort(jahr__1_1,ta)
& sort(jahr__1_1,oa)
& sort(jahr__1_1,me)
& sort(rom_0,fe)
& varia(c5,varia_c)
& refer(c5,refer_c)
& quant(c5,quant_c)
& gener(c5,sp)
& fact(c5,real)
& etype(c5,etype_c)
& card(c5,card_c)
& sort(c5,ta)
& sort(c5,oa)
& sort(c5,me)
& 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(c400,varia_c)
& refer(c400,indet)
& quant(c400,one)
& gener(c400,sp)
& fact(c400,real)
& etype(c400,int0)
& card(c400,int1)
& sort(c400,na)
& varia(c399,con)
& refer(c399,det)
& quant(c399,one)
& gener(c399,sp)
& fact(c399,real)
& etype(c399,int0)
& card(c399,int1)
& sort(c399,io)
& sort(c399,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(c402,con)
& refer(c402,det)
& quant(c402,one)
& gener(c402,sp)
& fact(c402,real)
& etype(c402,int0)
& card(c402,int1)
& sort(c402,l)
& varia(c393,con)
& refer(c393,det)
& quant(c393,one)
& gener(c393,sp)
& fact(c393,real)
& etype(c393,int0)
& card(c393,int1)
& sort(c393,d)
& varia(konzert__1_1,varia_c)
& refer(konzert__1_1,refer_c)
& quant(konzert__1_1,one)
& gener(konzert__1_1,ge)
& fact(konzert__1_1,real)
& etype(konzert__1_1,int0)
& card(konzert__1_1,int1)
& sort(konzert__1_1,io)
& sort(konzert__1_1,d)
& sort(konzert__1_1,ad)
& varia(c403,con)
& refer(c403,det)
& quant(c403,one)
& gener(c403,sp)
& fact(c403,real)
& etype(c403,int0)
& card(c403,int1)
& sort(c403,l)
& gener(aufnehmen_1_1,ge)
& fact(aufnehmen_1_1,real)
& sort(aufnehmen_1_1,dn)
& varia(c389,con)
& refer(c389,det)
& quant(c389,one)
& gener(c389,sp)
& fact(c389,real)
& etype(c389,int0)
& card(c389,int1)
& sort(c389,io)
& sort(c389,d)
& sort(c389,ad)
& gener(c384,sp)
& fact(c384,real)
& sort(c384,dn)
& sort(italien_0,fe)
& varia(c35,varia_c)
& refer(c35,indet)
& quant(c35,one)
& gener(c35,sp)
& fact(c35,real)
& etype(c35,int0)
& card(c35,int1)
& sort(c35,na)
& varia(c34,con)
& refer(c34,det)
& quant(c34,one)
& gener(c34,sp)
& fact(c34,real)
& etype(c34,int0)
& card(c34,int1)
& sort(c34,io)
& sort(c34,d)
& varia(c4,con)
& refer(c4,det)
& quant(c4,one)
& gener(c4,sp)
& fact(c4,real)
& etype(c4,int0)
& card(c4,int1)
& sort(c4,t)
& gener(gehen_1_1,ge)
& fact(gehen_1_1,real)
& sort(gehen_1_1,da)
& varia(c38,con)
& refer(c38,det)
& quant(c38,one)
& gener(c38,sp)
& fact(c38,real)
& etype(c38,int0)
& card(c38,int1)
& sort(c38,l)
& varia(retro_1_1,varia_c)
& refer(retro_1_1,refer_c)
& quant(retro_1_1,one)
& gener(retro_1_1,sp)
& fact(retro_1_1,real)
& etype(retro_1_1,int0)
& card(retro_1_1,int1)
& sort(retro_1_1,l)
& varia(c37,con)
& refer(c37,det)
& quant(c37,one)
& gener(c37,sp)
& fact(c37,real)
& etype(c37,int0)
& card(c37,int1)
& sort(c37,l)
& gener(c3,sp)
& fact(c3,real)
& sort(c3,da)
& varia(sohn_1_1,varia_c)
& refer(sohn_1_1,refer_c)
& quant(sohn_1_1,one)
& gener(sohn_1_1,ge)
& fact(sohn_1_1,real)
& etype(sohn_1_1,int0)
& card(sohn_1_1,int1)
& sort(sohn_1_1,d)
& varia(c25,con)
& refer(c25,det)
& quant(c25,one)
& gener(c25,sp)
& fact(c25,real)
& etype(c25,int0)
& card(c25,int1)
& sort(c25,d)
& sort(schweiz_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(land_1_1,varia_c)
& refer(land_1_1,refer_c)
& quant(land_1_1,one)
& gener(land_1_1,ge)
& fact(land_1_1,real)
& etype(land_1_1,int0)
& card(land_1_1,int1)
& sort(land_1_1,io)
& sort(land_1_1,d)
& varia(c21,varia_c)
& refer(c21,indet)
& quant(c21,one)
& gener(c21,sp)
& fact(c21,real)
& etype(c21,int0)
& card(c21,int1)
& sort(c21,na)
& varia(c20,con)
& refer(c20,det)
& quant(c20,one)
& gener(c20,sp)
& fact(c20,real)
& etype(c20,int0)
& card(c20,int1)
& sort(c20,io)
& sort(c20,d)
& varia(c9,varia_c)
& refer(c9,det)
& quant(c9,mult)
& gener(c9,sp)
& fact(c9,real)
& etype(c9,int1)
& card(c9,cons(x_constant,cons(int1,nil)))
& sort(c9,d)
& varia(c13,varia_c)
& refer(c13,det)
& quant(c13,one)
& gener(c13,sp)
& fact(c13,real)
& etype(c13,int0)
& card(c13,int1)
& sort(c13,o)
& pred(c9,eltern_1_1)
& val(c5,c1)
& sub(c5,jahr__1_1)
& in(c403,c393)
& in(c402,c399)
& val(c400,rom_0)
& sub(c400,name_1_1)
& attr(c4,c5)
& sub(c399,stadt__1_1)
& attr(c399,c400)
& sub(c393,kolosseum_1_1)
& loc(c393,c402)
& sub(c389,konzert__1_1)
& loc(c389,c403)
& subs(c384,aufnehmen_1_1)
& obj(c384,c389)
& flp(c38,c20)
& flp(c37,c34)
& val(c35,italien_0)
& sub(c35,name_1_1)
& sub(c34,land_1_1)
& attr(c34,c35)
& temp(c3,c4)
& subs(c3,gehen_1_1)
& origl(c3,c38)
& loc(c3,retro_1_1)
& dircl(c3,c37)
& assoc(c3,c25)
& agt(c3,c9)
& sub(c25,sohn_1_1)
& val(c21,schweiz_0)
& sub(c21,name_1_1)
& sub(c20,land_1_1)
& attr(c20,c21)
& attch(c13,c9) ),
file('/export/starexec/sandbox2/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(X1,X0)
| loc(sK62_skl(X0,X1),X0) ),
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] :
( ~ loc(X1,X0)
| subs(sK62_skl(X0,X1),stehen_1_1) ),
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] :
( ~ sub(X4,stadt__1_1)
| ~ attr(X4,X1)
| ~ sub(X2,kolosseum_1_1)
| ~ in(X3,X4)
| ~ loc(X0,X3)
| ~ scar(X0,X2)
| ~ val(X1,rom_0)
| ~ sub(X1,name_1_1)
| ~ subs(X0,stehen_1_1) ),
inference(cnf_transformation,[status(thm)],[f20816]) ).
fof(f20827,plain,
loc(c3,retro_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20839,plain,
loc(c389,c403),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20841,plain,
loc(c393,c402),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20842,plain,
sub(c393,kolosseum_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20843,plain,
attr(c399,c400),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20844,plain,
sub(c399,stadt__1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20846,plain,
sub(c400,name_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20847,plain,
val(c400,rom_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20848,plain,
in(c402,c399),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f22624,plain,
subs(sK62_skl(c402,c393),stehen_1_1),
inference(resolution,[status(thm)],[f20841,f10805]) ).
fof(f22698,plain,
! [X0,X1,X2,X3] :
( ~ sub(X3,stadt__1_1)
| ~ attr(X3,X0)
| ~ sub(X1,kolosseum_1_1)
| ~ in(X2,X3)
| ~ loc(sK62_skl(c402,c393),X2)
| ~ scar(sK62_skl(c402,c393),X1)
| ~ val(X0,rom_0)
| ~ sub(X0,name_1_1) ),
inference(resolution,[status(thm)],[f22624,f20817]) ).
fof(f22704,definition,
! [X0,X2,X3] :
( sQ58_spl
<=> ( ~ sub(X3,stadt__1_1)
| ~ attr(X3,X0)
| ~ in(X2,X3)
| ~ loc(sK62_skl(c402,c393),X2)
| ~ val(X0,rom_0)
| ~ sub(X0,name_1_1) ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f22705,plain,
! [X0,X1,X2] :
( ~ sQ58_spl
| ~ sub(X0,name_1_1)
| ~ loc(sK62_skl(c402,c393),X2)
| ~ in(X2,X1)
| ~ sub(X1,stadt__1_1)
| ~ attr(X1,X0)
| ~ val(X0,rom_0) ),
inference(component_clause,[status(thm)],[f22704]) ).
fof(f22707,definition,
! [X1] :
( sQ59_spl
<=> ( ~ sub(X1,kolosseum_1_1)
| ~ scar(sK62_skl(c402,c393),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f22708,plain,
! [X0] :
( ~ sQ59_spl
| ~ scar(sK62_skl(c402,c393),X0)
| ~ sub(X0,kolosseum_1_1) ),
inference(component_clause,[status(thm)],[f22707]) ).
fof(f22710,plain,
( sQ59_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f22698,f22704,f22707]) ).
fof(f22739,plain,
( ~ sQ59_spl
| ~ loc(c393,c402)
| ~ sub(c393,kolosseum_1_1) ),
inference(resolution,[status(thm)],[f22708,f10804]) ).
fof(f22740,definition,
( sQ66_spl
<=> sub(c393,kolosseum_1_1) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f22742,plain,
( sQ66_spl
| ~ sub(c393,kolosseum_1_1) ),
inference(component_clause,[status(thm)],[f22740]) ).
fof(f22743,definition,
( sQ67_spl
<=> loc(c393,c402) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f22745,plain,
( sQ67_spl
| ~ loc(c393,c402) ),
inference(component_clause,[status(thm)],[f22743]) ).
fof(f22746,plain,
( ~ sQ59_spl
| ~ sQ67_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f22739,f22740,f22743,f22707]) ).
fof(f22747,plain,
( sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22745,f20841]) ).
fof(f22748,plain,
sQ67_spl,
inference(contradiction_clause,[status(thm)],[f22747]) ).
fof(f22749,plain,
( sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22742,f20842]) ).
fof(f22750,plain,
sQ66_spl,
inference(contradiction_clause,[status(thm)],[f22749]) ).
fof(f22787,plain,
! [X0,X1] :
( ~ sQ58_spl
| ~ sub(c400,name_1_1)
| ~ loc(sK62_skl(c402,c393),X1)
| ~ in(X1,X0)
| ~ sub(X0,stadt__1_1)
| ~ attr(X0,c400) ),
inference(resolution,[status(thm)],[f22705,f20847]) ).
fof(f22788,definition,
! [X0,X1] :
( sQ74_spl
<=> ( ~ loc(sK62_skl(c402,c393),X1)
| ~ in(X1,X0)
| ~ sub(X0,stadt__1_1)
| ~ attr(X0,c400) ) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f22789,plain,
! [X0,X1] :
( ~ sQ74_spl
| ~ loc(sK62_skl(c402,c393),X1)
| ~ in(X1,X0)
| ~ attr(X0,c400)
| ~ sub(X0,stadt__1_1) ),
inference(component_clause,[status(thm)],[f22788]) ).
fof(f22791,definition,
( sQ75_spl
<=> sub(c400,name_1_1) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f22793,plain,
( sQ75_spl
| ~ sub(c400,name_1_1) ),
inference(component_clause,[status(thm)],[f22791]) ).
fof(f22794,plain,
( ~ sQ58_spl
| ~ sQ75_spl
| sQ74_spl ),
inference(split_clause,[status(thm)],[f22787,f22788,f22791,f22704]) ).
fof(f22795,plain,
( sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22793,f20846]) ).
fof(f22796,plain,
sQ75_spl,
inference(contradiction_clause,[status(thm)],[f22795]) ).
fof(f22823,plain,
! [X0] :
( ~ sQ74_spl
| ~ loc(sK62_skl(c402,c393),X0)
| ~ in(X0,c399)
| ~ sub(c399,stadt__1_1) ),
inference(resolution,[status(thm)],[f22789,f20843]) ).
fof(f22824,definition,
( sQ76_spl
<=> sub(c399,stadt__1_1) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f22826,plain,
( sQ76_spl
| ~ sub(c399,stadt__1_1) ),
inference(component_clause,[status(thm)],[f22824]) ).
fof(f22827,definition,
! [X0] :
( sQ77_spl
<=> ( ~ loc(sK62_skl(c402,c393),X0)
| ~ in(X0,c399) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f22828,plain,
! [X0] :
( ~ sQ77_spl
| ~ loc(sK62_skl(c402,c393),X0)
| ~ in(X0,c399) ),
inference(component_clause,[status(thm)],[f22827]) ).
fof(f22830,plain,
( ~ sQ74_spl
| sQ77_spl
| ~ sQ76_spl ),
inference(split_clause,[status(thm)],[f22823,f22824,f22827,f22788]) ).
fof(f22831,plain,
( sQ76_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22826,f20844]) ).
fof(f22832,plain,
sQ76_spl,
inference(contradiction_clause,[status(thm)],[f22831]) ).
fof(f23021,definition,
( sQ96_spl
<=> loc(sK62_skl(c402,c393),c402) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f23023,plain,
( sQ96_spl
| ~ loc(sK62_skl(c402,c393),c402) ),
inference(component_clause,[status(thm)],[f23021]) ).
fof(f23031,plain,
( sQ96_spl
| ~ loc(c393,c402) ),
inference(resolution,[status(thm)],[f23023,f10803]) ).
fof(f23033,plain,
( sQ96_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f23031,f22743,f23021]) ).
fof(f29372,definition,
( sQ570_spl
<=> loc(c3,retro_1_1) ),
introduced(definition,[new_symbols(definition,[sQ570_spl])],[split_symbol_definition]) ).
fof(f29374,plain,
( sQ570_spl
| ~ loc(c3,retro_1_1) ),
inference(component_clause,[status(thm)],[f29372]) ).
fof(f29376,plain,
( sQ570_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29374,f20827]) ).
fof(f29377,plain,
sQ570_spl,
inference(contradiction_clause,[status(thm)],[f29376]) ).
fof(f30156,definition,
( sQ612_spl
<=> loc(c389,c403) ),
introduced(definition,[new_symbols(definition,[sQ612_spl])],[split_symbol_definition]) ).
fof(f30158,plain,
( sQ612_spl
| ~ loc(c389,c403) ),
inference(component_clause,[status(thm)],[f30156]) ).
fof(f30160,plain,
( sQ612_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30158,f20839]) ).
fof(f30161,plain,
sQ612_spl,
inference(contradiction_clause,[status(thm)],[f30160]) ).
fof(f33742,plain,
( ~ sQ77_spl
| ~ loc(sK62_skl(c402,c393),c402) ),
inference(resolution,[status(thm)],[f20848,f22828]) ).
fof(f33746,plain,
( ~ sQ77_spl
| ~ sQ96_spl ),
inference(split_clause,[status(thm)],[f33742,f23021,f22827]) ).
fof(f33754,plain,
$false,
inference(sat_refutation,[status(thm)],[f22710,f22746,f22748,f22750,f22794,f22796,f22830,f22832,f23033,f29377,f30161,f33746]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR114+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/10.99 % Computer : n004.cluster.edu
% 0.10/10.99 % Model : x86_64 x86_64
% 0.10/10.99 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.99 % Memory : 8046.5625MB
% 0.10/10.99 % OS : Linux 6.8.0-71-generic
% 0.10/10.99 % CPULimit : 300
% 0.10/10.99 % WCLimit : 300
% 0.10/10.99 % DateTime : Mon Sep 21 15:05:18 UTC 2026
% 0.10/10.99 % CPUTime :
% 0.32/11.22 % Drodi V4.1.1
% 87.85/22.40 % Refutation found
% 87.85/22.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 87.85/22.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.21/23.07 % Elapsed time: 12.056655 seconds
% 4.21/23.07 % CPU time: 89.635637 seconds
% 4.21/23.07 % Total memory used: 697.522 MB
% 4.21/23.07 % Net memory used: 669.220 MB
%------------------------------------------------------------------------------