%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR114+21 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:52 PM UTC 2026
% Result : Theorem 71.41s 9.92s
% Output : CNFRefutation 71.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 3
% Syntax : Number of formulae : 30 ( 10 unt; 0 def)
% Number of atoms : 185 ( 0 equ)
% Maximal formula atoms : 74 ( 6 avg)
% Number of connectives : 228 ( 73 ~; 59 |; 95 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 74 ( 9 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 17 ( 16 usr; 1 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 28 con; 0-2 aty)
% Number of variables : 55 ( 43 !; 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(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(c30,con)
& refer(c30,det)
& quant(c30,one)
& gener(c30,sp)
& fact(c30,real)
& etype(c30,int0)
& card(c30,int1)
& sort(c30,l)
& gener(restaurieren_1_1,ge)
& fact(restaurieren_1_1,real)
& sort(restaurieren_1_1,da)
& varia(c5,con)
& refer(c5,det)
& quant(c5,one)
& gener(c5,sp)
& fact(c5,real)
& etype(c5,int0)
& card(c5,int1)
& sort(c5,d)
& gener(c19,sp)
& fact(c19,real)
& sort(c19,da)
& 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(c13,varia_c)
& refer(c13,indet)
& quant(c13,one)
& gener(c13,sp)
& fact(c13,real)
& etype(c13,int0)
& card(c13,int1)
& sort(c13,na)
& varia(c12,con)
& refer(c12,det)
& quant(c12,one)
& gener(c12,sp)
& fact(c12,real)
& etype(c12,int0)
& card(c12,int1)
& sort(c12,io)
& sort(c12,d)
& sub(c5,kolosseum_1_1)
& loc(c5,c30)
& in(c30,c12)
& subs(c19,restaurieren_1_1)
& aff(c19,c5)
& val(c13,rom_0)
& sub(c13,name_1_1)
& sub(c12,stadt__1_1)
& attr(c12,c13) ),
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] :
( ~ 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(X1,stadt__1_1)
| ~ sub(X4,kolosseum_1_1)
| ~ loc(X3,X2)
| ~ subs(X3,stehen_1_1)
| ~ val(X0,rom_0)
| ~ scar(X3,X4)
| ~ in(X2,X1)
| ~ attr(X1,X0)
| ~ sub(X0,name_1_1) ),
inference(cnf_transformation,[status(thm)],[f20816]) ).
fof(f20818,plain,
attr(c12,c13),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20819,plain,
sub(c12,stadt__1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20820,plain,
sub(c13,name_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20821,plain,
val(c13,rom_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20824,plain,
in(c30,c12),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20825,plain,
loc(c5,c30),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20826,plain,
sub(c5,kolosseum_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20927,plain,
! [X0,X1,X2,X3] :
( ~ attr(X2,X3)
| ~ sub(X3,name_1_1)
| ~ sub(X2,stadt__1_1)
| ~ subs(X0,stehen_1_1)
| ~ val(X3,rom_0)
| ~ in(X1,X2)
| ~ scar(X0,c5)
| ~ loc(X0,X1) ),
inference(resolution,[status(thm)],[f20826,f20817]) ).
fof(f20955,plain,
! [X0,X1,X2] :
( ~ scar(X1,c5)
| ~ attr(c12,X2)
| ~ loc(X1,X0)
| ~ val(X2,rom_0)
| ~ sub(X2,name_1_1)
| ~ subs(X1,stehen_1_1)
| ~ in(X0,c12) ),
inference(resolution,[status(thm)],[f20819,f20927]) ).
fof(f20958,plain,
! [X0,X1] :
( ~ scar(X1,c5)
| ~ loc(X1,X0)
| ~ val(c13,rom_0)
| ~ sub(c13,name_1_1)
| ~ subs(X1,stehen_1_1)
| ~ in(X0,c12) ),
inference(resolution,[status(thm)],[f20955,f20818]) ).
fof(f20959,plain,
! [X0,X1] :
( ~ in(X1,c12)
| ~ subs(X0,stehen_1_1)
| ~ val(c13,rom_0)
| ~ loc(X0,X1)
| ~ scar(X0,c5) ),
inference(forward_subsumption_resolution,[status(thm)],[f20958,f20820]) ).
fof(f20960,plain,
! [X0,X1] :
( ~ subs(X0,stehen_1_1)
| ~ in(X1,c12)
| ~ scar(X0,c5)
| ~ loc(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f20959,f20821]) ).
fof(f20962,plain,
! [X0] :
( ~ loc(X0,c30)
| ~ subs(X0,stehen_1_1)
| ~ scar(X0,c5) ),
inference(resolution,[status(thm)],[f20960,f20824]) ).
fof(f20963,plain,
! [X0] :
( ~ loc(c5,X0)
| ~ loc(sK62_skl(X0,c5),c30)
| ~ subs(sK62_skl(X0,c5),stehen_1_1) ),
inference(resolution,[status(thm)],[f20962,f10804]) ).
fof(f20966,plain,
! [X0] :
( ~ loc(c5,X0)
| ~ loc(sK62_skl(X0,c5),c30) ),
inference(forward_subsumption_resolution,[status(thm)],[f20963,f10805]) ).
fof(f21854,plain,
~ loc(sK62_skl(c30,c5),c30),
inference(resolution,[status(thm)],[f20825,f20966]) ).
fof(f21855,plain,
~ loc(c5,c30),
inference(resolution,[status(thm)],[f21854,f10803]) ).
fof(f21862,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f21855,f20825]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR114+21 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.56 % Computer : n002.cluster.edu
% 0.10/0.56 % Model : x86_64 x86_64
% 0.10/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.56 % Memory : 8046.5625MB
% 0.10/0.56 % OS : Linux 6.8.0-71-generic
% 0.10/0.57 % CPULimit : 300
% 0.10/0.57 % WCLimit : 300
% 0.10/0.57 % DateTime : Mon Sep 21 15:07:18 UTC 2026
% 0.10/0.57 % CPUTime :
% 0.14/0.70 % Drodi V4.1.1
% 71.41/9.92 % Refutation found
% 71.41/9.92 % SZS status Theorem for theBenchmark: Theorem is valid
% 71.41/9.92 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 10.69/10.09 % Elapsed time: 9.507279 seconds
% 10.69/10.09 % CPU time: 73.791960 seconds
% 10.69/10.09 % Total memory used: 837.023 MB
% 10.69/10.09 % Net memory used: 804.098 MB
%------------------------------------------------------------------------------