%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR117+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:14:15 PM UTC 2026
% Result : Theorem 0.08s 0.40s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 51
% Syntax : Number of formulae : 173 ( 62 unt; 22 def)
% Number of atoms : 491 ( 19 equ)
% Maximal formula atoms : 18 ( 2 avg)
% Number of connectives : 567 ( 249 ~; 247 |; 38 &)
% ( 22 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 42 ( 40 usr; 23 prp; 0-5 aty)
% Number of functors : 20 ( 20 usr; 18 con; 0-1 aty)
% Number of variables : 138 ( 114 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f15,axiom,
! [A] :
( s__Region(A)
=> s__Object(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A] :
( s__GeographicArea(A)
=> s__Region(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A] :
( s__GeopoliticalArea(A)
=> s__GeographicArea(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A] :
( s__Nation(A)
=> s__GeopoliticalArea(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A] :
( s__City(A)
=> s__GeopoliticalArea(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A] :
( s__BodyOfWater(A)
=> s__WaterArea(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [A] :
( s__Sea(A)
=> s__BodyOfWater(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [City] :
( s__City(City)
=> ( is_instance(City,s__CoastalCitiesClass)
=> ? [Sea] :
( s__orientation(City,Sea,s__Near)
& s__Sea(Sea) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [W,C] :
( ( s__City(C)
& s__WaterArea(W) )
=> ( s__orientation(C,W,s__Near)
=> s__capability(s__Flooding__t,s__located__m,C) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,conjecture,
? [City,Nation,CityLat,CityLong,CityName,CityNation,Latitude,MoscowLat,MoscowLong,MoscowName,MoscowNation] :
( s__capability(s__Flooding__t,s__located__m,City)
& to_int(CityLat) = to_int(MoscowLat)
& latlong(s__Moscow,MoscowLat,MoscowLong,MoscowName,MoscowNation)
& latlong(City,CityLat,CityLong,CityName,CityNation)
& look_different(City,s__Moscow)
& capital_city(City,Nation)
& is_instance(Nation,s__OECDMemberEconomiesClass)
& s__SymbolicString(MoscowNation)
& s__SymbolicString(MoscowName)
& real(MoscowLong)
& real(MoscowLat)
& int(Latitude)
& s__SymbolicString(CityNation)
& s__SymbolicString(CityName)
& real(CityLong)
& real(CityLat)
& s__Object(Nation)
& s__Object(City) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,negated_conjecture,
~ ? [City,Nation,CityLat,CityLong,CityName,CityNation,Latitude,MoscowLat,MoscowLong,MoscowName,MoscowNation] :
( s__capability(s__Flooding__t,s__located__m,City)
& to_int(CityLat) = to_int(MoscowLat)
& latlong(s__Moscow,MoscowLat,MoscowLong,MoscowName,MoscowNation)
& latlong(City,CityLat,CityLong,CityName,CityNation)
& look_different(City,s__Moscow)
& capital_city(City,Nation)
& is_instance(Nation,s__OECDMemberEconomiesClass)
& s__SymbolicString(MoscowNation)
& s__SymbolicString(MoscowName)
& real(MoscowLong)
& real(MoscowLat)
& int(Latitude)
& s__SymbolicString(CityNation)
& s__SymbolicString(CityName)
& real(CityLong)
& real(CityLat)
& s__Object(Nation)
& s__Object(City) ),
inference(negated_conjecture,[status(cth)],[f29]) ).
fof(f35,axiom,
is_instance(s__Copenhagen,s__CoastalCitiesClass),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
s__Nation(s__Denmark),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
is_instance(s__Denmark,s__OECDMemberEconomiesClass),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f102,axiom,
s__City(s__Copenhagen),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f103,axiom,
capital_city(s__Copenhagen,s__Denmark),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f150,axiom,
real('55.67631'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f151,axiom,
real('12.569355'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f152,axiom,
s__SymbolicString(copenhagen),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f153,axiom,
s__SymbolicString(dk),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f154,axiom,
latlong(s__Copenhagen,'55.67631','12.569355',copenhagen,dk),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f170,axiom,
real('55.75695'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f171,axiom,
real('37.614975'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f172,axiom,
s__SymbolicString(moscow),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f173,axiom,
s__SymbolicString(ru),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f174,axiom,
latlong(s__Moscow,'55.75695','37.614975',moscow,ru),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f206,axiom,
look_different(s__Copenhagen,s__Moscow),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f237,axiom,
to_int('55.67631') = '55',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f238,axiom,
to_int('55.75695') = '55',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f239,axiom,
int('60'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f299,plain,
! [A] :
( s__Object(A)
| ~ s__Region(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f300,plain,
! [X0] :
( s__Object(X0)
| ~ s__Region(X0) ),
inference(cnf_transformation,[status(thm)],[f299]) ).
fof(f301,plain,
! [A] :
( s__Region(A)
| ~ s__GeographicArea(A) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f302,plain,
! [X0] :
( s__Region(X0)
| ~ s__GeographicArea(X0) ),
inference(cnf_transformation,[status(thm)],[f301]) ).
fof(f303,plain,
! [A] :
( s__GeographicArea(A)
| ~ s__GeopoliticalArea(A) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f304,plain,
! [X0] :
( s__GeographicArea(X0)
| ~ s__GeopoliticalArea(X0) ),
inference(cnf_transformation,[status(thm)],[f303]) ).
fof(f305,plain,
! [A] :
( s__GeopoliticalArea(A)
| ~ s__Nation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f306,plain,
! [X0] :
( s__GeopoliticalArea(X0)
| ~ s__Nation(X0) ),
inference(cnf_transformation,[status(thm)],[f305]) ).
fof(f307,plain,
! [A] :
( s__GeopoliticalArea(A)
| ~ s__City(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f308,plain,
! [X0] :
( s__GeopoliticalArea(X0)
| ~ s__City(X0) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f311,plain,
! [A] :
( s__WaterArea(A)
| ~ s__BodyOfWater(A) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f312,plain,
! [X0] :
( s__WaterArea(X0)
| ~ s__BodyOfWater(X0) ),
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f313,plain,
! [A] :
( s__BodyOfWater(A)
| ~ s__Sea(A) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f314,plain,
! [X0] :
( s__BodyOfWater(X0)
| ~ s__Sea(X0) ),
inference(cnf_transformation,[status(thm)],[f313]) ).
fof(f320,plain,
! [City] :
( ? [Sea] :
( s__orientation(City,Sea,s__Near)
& s__Sea(Sea) )
| ~ is_instance(City,s__CoastalCitiesClass)
| ~ s__City(City) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f321,plain,
! [City] :
( ( s__orientation(City,sK14_skl(City),s__Near)
& s__Sea(sK14_skl(City)) )
| ~ is_instance(City,s__CoastalCitiesClass)
| ~ s__City(City) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(Sea,sK14_skl(City))],[f320]) ).
fof(f322,plain,
! [X0] :
( s__Sea(sK14_skl(X0))
| ~ is_instance(X0,s__CoastalCitiesClass)
| ~ s__City(X0) ),
inference(cnf_transformation,[status(thm)],[f321]) ).
fof(f323,plain,
! [X0] :
( s__orientation(X0,sK14_skl(X0),s__Near)
| ~ is_instance(X0,s__CoastalCitiesClass)
| ~ s__City(X0) ),
inference(cnf_transformation,[status(thm)],[f321]) ).
fof(f324,plain,
! [W,C] :
( s__capability(s__Flooding__t,s__located__m,C)
| ~ s__orientation(C,W,s__Near)
| ~ s__City(C)
| ~ s__WaterArea(W) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f325,plain,
! [X0,X1] :
( s__capability(s__Flooding__t,s__located__m,X1)
| ~ s__orientation(X1,X0,s__Near)
| ~ s__City(X1)
| ~ s__WaterArea(X0) ),
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f326,plain,
! [City,Nation,CityLat,CityLong,CityName,CityNation,Latitude,MoscowLat,MoscowLong,MoscowName,MoscowNation] :
( ~ s__capability(s__Flooding__t,s__located__m,City)
| to_int(CityLat) != to_int(MoscowLat)
| ~ latlong(s__Moscow,MoscowLat,MoscowLong,MoscowName,MoscowNation)
| ~ latlong(City,CityLat,CityLong,CityName,CityNation)
| ~ look_different(City,s__Moscow)
| ~ capital_city(City,Nation)
| ~ is_instance(Nation,s__OECDMemberEconomiesClass)
| ~ s__SymbolicString(MoscowNation)
| ~ s__SymbolicString(MoscowName)
| ~ real(MoscowLong)
| ~ real(MoscowLat)
| ~ int(Latitude)
| ~ s__SymbolicString(CityNation)
| ~ s__SymbolicString(CityName)
| ~ real(CityLong)
| ~ real(CityLat)
| ~ s__Object(Nation)
| ~ s__Object(City) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f327,plain,
! [City] :
( ~ s__capability(s__Flooding__t,s__located__m,City)
| ! [CityLat,MoscowLat] :
( to_int(CityLat) != to_int(MoscowLat)
| ! [MoscowLong,MoscowName,MoscowNation] :
( ~ latlong(s__Moscow,MoscowLat,MoscowLong,MoscowName,MoscowNation)
| ! [CityLong,CityName,CityNation] :
( ~ latlong(City,CityLat,CityLong,CityName,CityNation)
| ~ look_different(City,s__Moscow)
| ! [Nation] :
( ~ capital_city(City,Nation)
| ~ is_instance(Nation,s__OECDMemberEconomiesClass)
| ~ s__SymbolicString(MoscowNation)
| ~ s__SymbolicString(MoscowName)
| ~ real(MoscowLong)
| ~ real(MoscowLat)
| ! [Latitude] : ~ int(Latitude)
| ~ s__SymbolicString(CityNation)
| ~ s__SymbolicString(CityName)
| ~ real(CityLong)
| ~ real(CityLat)
| ~ s__Object(Nation)
| ~ s__Object(City) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f326]) ).
fof(f328,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
( ~ s__capability(s__Flooding__t,s__located__m,X0)
| to_int(X2) != to_int(X7)
| ~ latlong(s__Moscow,X7,X8,X9,X10)
| ~ latlong(X0,X2,X3,X4,X5)
| ~ look_different(X0,s__Moscow)
| ~ capital_city(X0,X1)
| ~ is_instance(X1,s__OECDMemberEconomiesClass)
| ~ s__SymbolicString(X10)
| ~ s__SymbolicString(X9)
| ~ real(X8)
| ~ real(X7)
| ~ int(X6)
| ~ s__SymbolicString(X5)
| ~ s__SymbolicString(X4)
| ~ real(X3)
| ~ real(X2)
| ~ s__Object(X1)
| ~ s__Object(X0) ),
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f335,plain,
is_instance(s__Copenhagen,s__CoastalCitiesClass),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f341,plain,
s__Nation(s__Denmark),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f342,plain,
is_instance(s__Denmark,s__OECDMemberEconomiesClass),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f403,plain,
s__City(s__Copenhagen),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f404,plain,
capital_city(s__Copenhagen,s__Denmark),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f451,plain,
real('55.67631'),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f452,plain,
real('12.569355'),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f453,plain,
s__SymbolicString(copenhagen),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f454,plain,
s__SymbolicString(dk),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f455,plain,
latlong(s__Copenhagen,'55.67631','12.569355',copenhagen,dk),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f471,plain,
real('55.75695'),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f472,plain,
real('37.614975'),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f473,plain,
s__SymbolicString(moscow),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f474,plain,
s__SymbolicString(ru),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f475,plain,
latlong(s__Moscow,'55.75695','37.614975',moscow,ru),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f507,plain,
look_different(s__Copenhagen,s__Moscow),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f538,plain,
to_int('55.67631') = '55',
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f539,plain,
to_int('55.75695') = '55',
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f540,plain,
int('60'),
inference(cnf_transformation,[status(thm)],[f239]) ).
fof(f602,definition,
! [X0,X1,X2,X3,X4,X5,X7,X8,X9,X10] :
( sQ0_spl
<=> ( ~ s__capability(s__Flooding__t,s__located__m,X0)
| to_int(X2) != to_int(X7)
| ~ latlong(s__Moscow,X7,X8,X9,X10)
| ~ latlong(X0,X2,X3,X4,X5)
| ~ look_different(X0,s__Moscow)
| ~ capital_city(X0,X1)
| ~ is_instance(X1,s__OECDMemberEconomiesClass)
| ~ s__SymbolicString(X10)
| ~ s__SymbolicString(X9)
| ~ real(X8)
| ~ real(X7)
| ~ s__SymbolicString(X5)
| ~ s__SymbolicString(X4)
| ~ real(X3)
| ~ real(X2)
| ~ s__Object(X1)
| ~ s__Object(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f603,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ sQ0_spl
| ~ s__capability(s__Flooding__t,s__located__m,X0)
| to_int(X2) != to_int(X6)
| ~ latlong(s__Moscow,X6,X7,X8,X9)
| ~ latlong(X0,X2,X3,X4,X5)
| ~ look_different(X0,s__Moscow)
| ~ capital_city(X0,X1)
| ~ is_instance(X1,s__OECDMemberEconomiesClass)
| ~ s__SymbolicString(X9)
| ~ s__SymbolicString(X8)
| ~ real(X7)
| ~ real(X6)
| ~ s__SymbolicString(X5)
| ~ s__SymbolicString(X4)
| ~ real(X3)
| ~ real(X2)
| ~ s__Object(X1)
| ~ s__Object(X0) ),
inference(component_clause,[status(thm)],[f602]) ).
fof(f605,definition,
! [X6] :
( sQ1_spl
<=> ~ int(X6) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f606,plain,
! [X0] :
( ~ sQ1_spl
| ~ int(X0) ),
inference(component_clause,[status(thm)],[f605]) ).
fof(f608,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f328,f602,f605]) ).
fof(f620,plain,
s__GeopoliticalArea(s__Denmark),
inference(resolution,[status(thm)],[f341,f306]) ).
fof(f624,plain,
( s__orientation(s__Copenhagen,sK14_skl(s__Copenhagen),s__Near)
| ~ s__City(s__Copenhagen) ),
inference(resolution,[status(thm)],[f335,f323]) ).
fof(f625,plain,
( s__Sea(sK14_skl(s__Copenhagen))
| ~ s__City(s__Copenhagen) ),
inference(resolution,[status(thm)],[f335,f322]) ).
fof(f626,definition,
( sQ2_spl
<=> s__City(s__Copenhagen) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f628,plain,
( sQ2_spl
| ~ s__City(s__Copenhagen) ),
inference(component_clause,[status(thm)],[f626]) ).
fof(f629,definition,
( sQ3_spl
<=> s__orientation(s__Copenhagen,sK14_skl(s__Copenhagen),s__Near) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f630,plain,
( ~ sQ3_spl
| s__orientation(s__Copenhagen,sK14_skl(s__Copenhagen),s__Near) ),
inference(component_clause,[status(thm)],[f629]) ).
fof(f632,plain,
( sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f624,f626,f629]) ).
fof(f633,definition,
( sQ4_spl
<=> s__Sea(sK14_skl(s__Copenhagen)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f634,plain,
( ~ sQ4_spl
| s__Sea(sK14_skl(s__Copenhagen)) ),
inference(component_clause,[status(thm)],[f633]) ).
fof(f636,plain,
( sQ4_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f625,f626,f633]) ).
fof(f637,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f628,f403]) ).
fof(f638,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f637]) ).
fof(f667,plain,
s__GeopoliticalArea(s__Copenhagen),
inference(resolution,[status(thm)],[f403,f308]) ).
fof(f732,plain,
s__GeographicArea(s__Denmark),
inference(resolution,[status(thm)],[f620,f304]) ).
fof(f1209,plain,
s__GeographicArea(s__Copenhagen),
inference(resolution,[status(thm)],[f667,f304]) ).
fof(f1290,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ0_spl
| ~ s__capability(s__Flooding__t,s__located__m,X0)
| to_int(X2) != to_int('55.75695')
| ~ latlong(X0,X2,X3,X4,X5)
| ~ look_different(X0,s__Moscow)
| ~ capital_city(X0,X1)
| ~ is_instance(X1,s__OECDMemberEconomiesClass)
| ~ s__SymbolicString(ru)
| ~ s__SymbolicString(moscow)
| ~ real('37.614975')
| ~ real('55.75695')
| ~ s__SymbolicString(X5)
| ~ s__SymbolicString(X4)
| ~ real(X3)
| ~ real(X2)
| ~ s__Object(X1)
| ~ s__Object(X0) ),
inference(resolution,[status(thm)],[f603,f475]) ).
fof(f1443,definition,
( sQ53_spl
<=> s__Object(s__Copenhagen) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1445,plain,
( sQ53_spl
| ~ s__Object(s__Copenhagen) ),
inference(component_clause,[status(thm)],[f1443]) ).
fof(f1446,definition,
( sQ54_spl
<=> s__Object(s__Denmark) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1448,plain,
( sQ54_spl
| ~ s__Object(s__Denmark) ),
inference(component_clause,[status(thm)],[f1446]) ).
fof(f1452,definition,
( sQ56_spl
<=> is_instance(s__Denmark,s__OECDMemberEconomiesClass) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1454,plain,
( sQ56_spl
| ~ is_instance(s__Denmark,s__OECDMemberEconomiesClass) ),
inference(component_clause,[status(thm)],[f1452]) ).
fof(f1455,definition,
( sQ57_spl
<=> look_different(s__Copenhagen,s__Moscow) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1457,plain,
( sQ57_spl
| ~ look_different(s__Copenhagen,s__Moscow) ),
inference(component_clause,[status(thm)],[f1455]) ).
fof(f1458,definition,
( sQ58_spl
<=> s__capability(s__Flooding__t,s__located__m,s__Copenhagen) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1677,definition,
( sQ127_spl
<=> real('55.75695') ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f1679,plain,
( sQ127_spl
| ~ real('55.75695') ),
inference(component_clause,[status(thm)],[f1677]) ).
fof(f1680,definition,
( sQ128_spl
<=> real('37.614975') ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f1682,plain,
( sQ128_spl
| ~ real('37.614975') ),
inference(component_clause,[status(thm)],[f1680]) ).
fof(f1683,definition,
( sQ129_spl
<=> s__SymbolicString(moscow) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f1685,plain,
( sQ129_spl
| ~ s__SymbolicString(moscow) ),
inference(component_clause,[status(thm)],[f1683]) ).
fof(f1686,definition,
( sQ130_spl
<=> s__SymbolicString(ru) ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f1688,plain,
( sQ130_spl
| ~ s__SymbolicString(ru) ),
inference(component_clause,[status(thm)],[f1686]) ).
fof(f1760,definition,
! [X0] :
( sQ153_spl
<=> ( ~ capital_city(s__Copenhagen,X0)
| ~ is_instance(X0,s__OECDMemberEconomiesClass)
| ~ s__Object(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f1761,plain,
! [X0] :
( ~ sQ153_spl
| ~ capital_city(s__Copenhagen,X0)
| ~ is_instance(X0,s__OECDMemberEconomiesClass)
| ~ s__Object(X0) ),
inference(component_clause,[status(thm)],[f1760]) ).
fof(f1763,definition,
( sQ154_spl
<=> real('55.67631') ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f1765,plain,
( sQ154_spl
| ~ real('55.67631') ),
inference(component_clause,[status(thm)],[f1763]) ).
fof(f1766,definition,
( sQ155_spl
<=> real('12.569355') ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f1768,plain,
( sQ155_spl
| ~ real('12.569355') ),
inference(component_clause,[status(thm)],[f1766]) ).
fof(f1769,definition,
( sQ156_spl
<=> s__SymbolicString(copenhagen) ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f1771,plain,
( sQ156_spl
| ~ s__SymbolicString(copenhagen) ),
inference(component_clause,[status(thm)],[f1769]) ).
fof(f1772,definition,
( sQ157_spl
<=> s__SymbolicString(dk) ),
introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition]) ).
fof(f1774,plain,
( sQ157_spl
| ~ s__SymbolicString(dk) ),
inference(component_clause,[status(thm)],[f1772]) ).
fof(f1893,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ195_spl
<=> ( ~ s__capability(s__Flooding__t,s__located__m,X0)
| to_int(X2) != to_int('55.75695')
| ~ latlong(X0,X2,X3,X4,X5)
| ~ look_different(X0,s__Moscow)
| ~ capital_city(X0,X1)
| ~ is_instance(X1,s__OECDMemberEconomiesClass)
| ~ s__SymbolicString(X5)
| ~ s__SymbolicString(X4)
| ~ real(X3)
| ~ real(X2)
| ~ s__Object(X1)
| ~ s__Object(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f1894,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ195_spl
| ~ s__capability(s__Flooding__t,s__located__m,X0)
| to_int(X2) != to_int('55.75695')
| ~ latlong(X0,X2,X3,X4,X5)
| ~ look_different(X0,s__Moscow)
| ~ capital_city(X0,X1)
| ~ is_instance(X1,s__OECDMemberEconomiesClass)
| ~ s__SymbolicString(X5)
| ~ s__SymbolicString(X4)
| ~ real(X3)
| ~ real(X2)
| ~ s__Object(X1)
| ~ s__Object(X0) ),
inference(component_clause,[status(thm)],[f1893]) ).
fof(f1896,plain,
( ~ sQ0_spl
| ~ sQ130_spl
| ~ sQ129_spl
| ~ sQ128_spl
| ~ sQ127_spl
| sQ195_spl ),
inference(split_clause,[status(thm)],[f1290,f1893,f1677,f1680,f1683,f1686,f602]) ).
fof(f1897,plain,
( sQ130_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1688,f474]) ).
fof(f1898,plain,
sQ130_spl,
inference(contradiction_clause,[status(thm)],[f1897]) ).
fof(f1899,plain,
( sQ129_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1685,f473]) ).
fof(f1900,plain,
sQ129_spl,
inference(contradiction_clause,[status(thm)],[f1899]) ).
fof(f1901,plain,
( sQ128_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1682,f472]) ).
fof(f1902,plain,
sQ128_spl,
inference(contradiction_clause,[status(thm)],[f1901]) ).
fof(f1903,plain,
( sQ127_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1679,f471]) ).
fof(f1904,plain,
sQ127_spl,
inference(contradiction_clause,[status(thm)],[f1903]) ).
fof(f1906,plain,
( ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f540,f606]) ).
fof(f1967,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f1906]) ).
fof(f1980,plain,
( sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1457,f507]) ).
fof(f1981,plain,
sQ57_spl,
inference(contradiction_clause,[status(thm)],[f1980]) ).
fof(f1996,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ195_spl
| ~ s__capability(s__Flooding__t,s__located__m,X0)
| to_int(X2) != '55'
| ~ latlong(X0,X2,X3,X4,X5)
| ~ look_different(X0,s__Moscow)
| ~ capital_city(X0,X1)
| ~ is_instance(X1,s__OECDMemberEconomiesClass)
| ~ s__SymbolicString(X5)
| ~ s__SymbolicString(X4)
| ~ real(X3)
| ~ real(X2)
| ~ s__Object(X1)
| ~ s__Object(X0) ),
inference(forward_demodulation,[status(thm)],[f539,f1894]) ).
fof(f2071,plain,
s__Region(s__Denmark),
inference(resolution,[status(thm)],[f732,f302]) ).
fof(f2410,plain,
( ~ sQ3_spl
| s__capability(s__Flooding__t,s__located__m,s__Copenhagen)
| ~ s__City(s__Copenhagen)
| ~ s__WaterArea(sK14_skl(s__Copenhagen)) ),
inference(resolution,[status(thm)],[f630,f325]) ).
fof(f2411,definition,
( sQ196_spl
<=> s__WaterArea(sK14_skl(s__Copenhagen)) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f2413,plain,
( sQ196_spl
| ~ s__WaterArea(sK14_skl(s__Copenhagen)) ),
inference(component_clause,[status(thm)],[f2411]) ).
fof(f2414,plain,
( ~ sQ3_spl
| sQ58_spl
| ~ sQ2_spl
| ~ sQ196_spl ),
inference(split_clause,[status(thm)],[f2410,f2411,f626,f1458,f629]) ).
fof(f2415,plain,
( ~ sQ4_spl
| s__BodyOfWater(sK14_skl(s__Copenhagen)) ),
inference(resolution,[status(thm)],[f634,f314]) ).
fof(f2432,plain,
s__Region(s__Copenhagen),
inference(resolution,[status(thm)],[f1209,f302]) ).
fof(f2467,plain,
! [X0] :
( ~ sQ195_spl
| ~ s__capability(s__Flooding__t,s__located__m,s__Copenhagen)
| to_int('55.67631') != '55'
| ~ look_different(s__Copenhagen,s__Moscow)
| ~ capital_city(s__Copenhagen,X0)
| ~ is_instance(X0,s__OECDMemberEconomiesClass)
| ~ s__SymbolicString(dk)
| ~ s__SymbolicString(copenhagen)
| ~ real('12.569355')
| ~ real('55.67631')
| ~ s__Object(X0)
| ~ s__Object(s__Copenhagen) ),
inference(resolution,[status(thm)],[f1996,f455]) ).
fof(f2570,definition,
( sQ221_spl
<=> to_int('55.67631') = '55' ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f2572,plain,
( sQ221_spl
| to_int('55.67631') != '55' ),
inference(component_clause,[status(thm)],[f2570]) ).
fof(f2573,plain,
( ~ sQ195_spl
| ~ sQ58_spl
| ~ sQ221_spl
| ~ sQ57_spl
| ~ sQ157_spl
| ~ sQ156_spl
| ~ sQ155_spl
| ~ sQ154_spl
| sQ153_spl
| ~ sQ53_spl ),
inference(split_clause,[status(thm)],[f2467,f1443,f1760,f1763,f1766,f1769,f1772,f1455,f2570,f1458,f1893]) ).
fof(f2713,plain,
s__Object(s__Denmark),
inference(resolution,[status(thm)],[f2071,f300]) ).
fof(f2732,plain,
( ~ sQ4_spl
| s__WaterArea(sK14_skl(s__Copenhagen)) ),
inference(resolution,[status(thm)],[f2415,f312]) ).
fof(f2771,plain,
s__Object(s__Copenhagen),
inference(resolution,[status(thm)],[f2432,f300]) ).
fof(f2772,plain,
( sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2771,f1445]) ).
fof(f2773,plain,
sQ53_spl,
inference(contradiction_clause,[status(thm)],[f2772]) ).
fof(f2824,plain,
( sQ157_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1774,f454]) ).
fof(f2825,plain,
sQ157_spl,
inference(contradiction_clause,[status(thm)],[f2824]) ).
fof(f2826,plain,
( sQ156_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1771,f453]) ).
fof(f2827,plain,
sQ156_spl,
inference(contradiction_clause,[status(thm)],[f2826]) ).
fof(f2828,plain,
( sQ155_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1768,f452]) ).
fof(f2829,plain,
sQ155_spl,
inference(contradiction_clause,[status(thm)],[f2828]) ).
fof(f2830,plain,
( sQ154_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1765,f451]) ).
fof(f2831,plain,
sQ154_spl,
inference(contradiction_clause,[status(thm)],[f2830]) ).
fof(f2920,plain,
( sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1454,f342]) ).
fof(f2921,plain,
sQ56_spl,
inference(contradiction_clause,[status(thm)],[f2920]) ).
fof(f2922,plain,
( sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1448,f2713]) ).
fof(f2923,plain,
sQ54_spl,
inference(contradiction_clause,[status(thm)],[f2922]) ).
fof(f2924,plain,
( sQ196_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2413,f2732]) ).
fof(f2925,plain,
( sQ196_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f2924]) ).
fof(f2926,plain,
( ~ sQ153_spl
| ~ is_instance(s__Denmark,s__OECDMemberEconomiesClass)
| ~ s__Object(s__Denmark) ),
inference(resolution,[status(thm)],[f1761,f404]) ).
fof(f2927,plain,
( ~ sQ153_spl
| ~ sQ56_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f2926,f1446,f1452,f1760]) ).
fof(f2929,plain,
( sQ221_spl
| '55' != '55' ),
inference(forward_demodulation,[status(thm)],[f538,f2572]) ).
fof(f2930,plain,
( sQ221_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2929]) ).
fof(f2931,plain,
sQ221_spl,
inference(contradiction_clause,[status(thm)],[f2930]) ).
fof(f2932,plain,
$false,
inference(sat_refutation,[status(thm)],[f608,f632,f636,f638,f1896,f1898,f1900,f1902,f1904,f1967,f1981,f2414,f2573,f2773,f2825,f2827,f2829,f2831,f2921,f2923,f2925,f2927,f2931]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR117+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n019.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 15:11:04 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.08/0.40 % Refutation found
% 0.08/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.45 % Elapsed time: 0.084758 seconds
% 0.13/0.45 % CPU time: 0.326818 seconds
% 0.13/0.45 % Total memory used: 52.336 MB
% 0.13/0.45 % Net memory used: 52.150 MB
%------------------------------------------------------------------------------