%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR117+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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:15:34 PM UTC 2026
% Result : Theorem 0.08s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR117+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n019.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 15:11:04 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.35 % 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
% 0.08/0.40 fof(f15,axiom,(
% 0.08/0.40 (! [A] :( s__Region(A)=> s__Object(A) ) )),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f16,axiom,(
% 0.08/0.40 (! [A] :( s__GeographicArea(A)=> s__Region(A) ) )),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f17,axiom,(
% 0.08/0.40 (! [A] :( s__GeopoliticalArea(A)=> s__GeographicArea(A) ) )),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f18,axiom,(
% 0.08/0.40 (! [A] :( s__Nation(A)=> s__GeopoliticalArea(A) ) )),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f19,axiom,(
% 0.08/0.40 (! [A] :( s__City(A)=> s__GeopoliticalArea(A) ) )),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f21,axiom,(
% 0.08/0.40 (! [A] :( s__BodyOfWater(A)=> s__WaterArea(A) ) )),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f22,axiom,(
% 0.08/0.40 (! [A] :( s__Sea(A)=> s__BodyOfWater(A) ) )),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f27,axiom,(
% 0.08/0.40 (! [City] :( s__City(City)=> ( is_instance(City,s__CoastalCitiesClass)=> (? [Sea] :( s__Sea(Sea)& s__orientation(City,Sea,s__Near) ) )) ) )),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f28,axiom,(
% 0.08/0.40 (! [W,C] :( ( s__WaterArea(W)& s__City(C) )=> ( s__orientation(C,W,s__Near)=> s__capability(s__Flooding__t,s__located__m,C) ) ) )),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f29,conjecture,(
% 0.08/0.40 (? [City,Nation,CityLat,CityLong,CityName,CityNation,Latitude,MoscowLat,MoscowLong,MoscowName,MoscowNation] :( s__Object(City)& s__Object(Nation)& real(CityLat)& real(CityLong)& s__SymbolicString(CityName)& s__SymbolicString(CityNation)& int(Latitude)& real(MoscowLat)& real(MoscowLong)& s__SymbolicString(MoscowName)& s__SymbolicString(MoscowNation)& is_instance(Nation,s__OECDMemberEconomiesClass)& capital_city(City,Nation)& look_different(City,s__Moscow)& latlong(City,CityLat,CityLong,CityName,CityNation)& latlong(s__Moscow,MoscowLat,MoscowLong,MoscowName,MoscowNation)& to_int(CityLat) = to_int(MoscowLat)& s__capability(s__Flooding__t,s__located__m,City) ) )),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f30,negated_conjecture,(
% 0.08/0.40 ~((? [City,Nation,CityLat,CityLong,CityName,CityNation,Latitude,MoscowLat,MoscowLong,MoscowName,MoscowNation] :( s__Object(City)& s__Object(Nation)& real(CityLat)& real(CityLong)& s__SymbolicString(CityName)& s__SymbolicString(CityNation)& int(Latitude)& real(MoscowLat)& real(MoscowLong)& s__SymbolicString(MoscowName)& s__SymbolicString(MoscowNation)& is_instance(Nation,s__OECDMemberEconomiesClass)& capital_city(City,Nation)& look_different(City,s__Moscow)& latlong(City,CityLat,CityLong,CityName,CityNation)& latlong(s__Moscow,MoscowLat,MoscowLong,MoscowName,MoscowNation)& to_int(CityLat) = to_int(MoscowLat)& s__capability(s__Flooding__t,s__located__m,City) ) ))),
% 0.08/0.40 inference(negated_conjecture,[status(cth)],[f29])).
% 0.08/0.40 fof(f35,axiom,(
% 0.08/0.40 is_instance(s__Copenhagen,s__CoastalCitiesClass) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f40,axiom,(
% 0.08/0.40 s__Nation(s__Denmark) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f41,axiom,(
% 0.08/0.40 is_instance(s__Denmark,s__OECDMemberEconomiesClass) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f102,axiom,(
% 0.08/0.40 s__City(s__Copenhagen) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f103,axiom,(
% 0.08/0.40 capital_city(s__Copenhagen,s__Denmark) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f150,axiom,(
% 0.08/0.40 real('55.67631') ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f151,axiom,(
% 0.08/0.40 real('12.569355') ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f152,axiom,(
% 0.08/0.40 s__SymbolicString(copenhagen) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f153,axiom,(
% 0.08/0.40 s__SymbolicString(dk) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f154,axiom,(
% 0.08/0.40 latlong(s__Copenhagen,'55.67631','12.569355',copenhagen,dk) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f170,axiom,(
% 0.08/0.40 real('55.75695') ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f171,axiom,(
% 0.08/0.40 real('37.614975') ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f172,axiom,(
% 0.08/0.40 s__SymbolicString(moscow) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f173,axiom,(
% 0.08/0.40 s__SymbolicString(ru) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f174,axiom,(
% 0.08/0.40 latlong(s__Moscow,'55.75695','37.614975',moscow,ru) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f206,axiom,(
% 0.08/0.40 look_different(s__Copenhagen,s__Moscow) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f237,axiom,(
% 0.08/0.40 to_int('55.67631') = '55' ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f238,axiom,(
% 0.08/0.40 to_int('55.75695') = '55' ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f239,axiom,(
% 0.08/0.40 int('60') ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f299,plain,(
% 0.08/0.40 ![A]: (~s__Region(A)|s__Object(A))),
% 0.08/0.40 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.08/0.40 fof(f300,plain,(
% 0.08/0.40 ![X0]: (~s__Region(X0)|s__Object(X0))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f299])).
% 0.08/0.40 fof(f301,plain,(
% 0.08/0.40 ![A]: (~s__GeographicArea(A)|s__Region(A))),
% 0.08/0.40 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.08/0.40 fof(f302,plain,(
% 0.08/0.40 ![X0]: (~s__GeographicArea(X0)|s__Region(X0))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f301])).
% 0.08/0.40 fof(f303,plain,(
% 0.08/0.40 ![A]: (~s__GeopoliticalArea(A)|s__GeographicArea(A))),
% 0.08/0.40 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.08/0.40 fof(f304,plain,(
% 0.08/0.40 ![X0]: (~s__GeopoliticalArea(X0)|s__GeographicArea(X0))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f303])).
% 0.08/0.40 fof(f305,plain,(
% 0.08/0.40 ![A]: (~s__Nation(A)|s__GeopoliticalArea(A))),
% 0.08/0.40 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.08/0.40 fof(f306,plain,(
% 0.08/0.40 ![X0]: (~s__Nation(X0)|s__GeopoliticalArea(X0))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f305])).
% 0.08/0.40 fof(f307,plain,(
% 0.08/0.40 ![A]: (~s__City(A)|s__GeopoliticalArea(A))),
% 0.08/0.40 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.08/0.40 fof(f308,plain,(
% 0.08/0.40 ![X0]: (~s__City(X0)|s__GeopoliticalArea(X0))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f307])).
% 0.08/0.40 fof(f311,plain,(
% 0.08/0.40 ![A]: (~s__BodyOfWater(A)|s__WaterArea(A))),
% 0.08/0.40 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.08/0.40 fof(f312,plain,(
% 0.08/0.40 ![X0]: (~s__BodyOfWater(X0)|s__WaterArea(X0))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f311])).
% 0.08/0.40 fof(f313,plain,(
% 0.08/0.40 ![A]: (~s__Sea(A)|s__BodyOfWater(A))),
% 0.08/0.40 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 0.08/0.40 fof(f314,plain,(
% 0.08/0.40 ![X0]: (~s__Sea(X0)|s__BodyOfWater(X0))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f313])).
% 0.08/0.40 fof(f320,plain,(
% 0.08/0.40 ![City]: (~s__City(City)|(~is_instance(City,s__CoastalCitiesClass)|(?[Sea]: (s__Sea(Sea)&s__orientation(City,Sea,s__Near)))))),
% 0.08/0.40 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.08/0.40 fof(f321,plain,(
% 0.08/0.40 ![City]: (~s__City(City)|(~is_instance(City,s__CoastalCitiesClass)|(s__Sea(sK14_skl(City))&s__orientation(City,sK14_skl(City),s__Near))))),
% 0.08/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(Sea,sK14_skl(City))],[f320])).
% 0.08/0.40 fof(f322,plain,(
% 0.08/0.40 ![X0]: (~s__City(X0)|~is_instance(X0,s__CoastalCitiesClass)|s__Sea(sK14_skl(X0)))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f321])).
% 0.08/0.40 fof(f323,plain,(
% 0.08/0.40 ![X0]: (~s__City(X0)|~is_instance(X0,s__CoastalCitiesClass)|s__orientation(X0,sK14_skl(X0),s__Near))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f321])).
% 0.08/0.40 fof(f324,plain,(
% 0.08/0.40 ![W,C]: ((~s__WaterArea(W)|~s__City(C))|(~s__orientation(C,W,s__Near)|s__capability(s__Flooding__t,s__located__m,C)))),
% 0.08/0.40 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.08/0.40 fof(f325,plain,(
% 0.08/0.40 ![X0,X1]: (~s__WaterArea(X0)|~s__City(X1)|~s__orientation(X1,X0,s__Near)|s__capability(s__Flooding__t,s__located__m,X1))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f324])).
% 0.08/0.40 fof(f326,plain,(
% 0.08/0.40 (![City,Nation,CityLat,CityLong,CityName,CityNation,Latitude,MoscowLat,MoscowLong,MoscowName,MoscowNation]: (((((((((((((((((~s__Object(City)|~s__Object(Nation))|~real(CityLat))|~real(CityLong))|~s__SymbolicString(CityName))|~s__SymbolicString(CityNation))|~int(Latitude))|~real(MoscowLat))|~real(MoscowLong))|~s__SymbolicString(MoscowName))|~s__SymbolicString(MoscowNation))|~is_instance(Nation,s__OECDMemberEconomiesClass))|~capital_city(City,Nation))|~look_different(City,s__Moscow))|~latlong(City,CityLat,CityLong,CityName,CityNation))|~latlong(s__Moscow,MoscowLat,MoscowLong,MoscowName,MoscowNation))|~to_int(CityLat)=to_int(MoscowLat))|~s__capability(s__Flooding__t,s__located__m,City)))),
% 0.08/0.40 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.08/0.40 fof(f327,plain,(
% 0.08/0.40 ![City]: ((![CityLat,MoscowLat]: ((![MoscowLong,MoscowName,MoscowNation]: ((![CityLong,CityName,CityNation]: (((![Nation]: ((((((((((((~s__Object(City)|~s__Object(Nation))|~real(CityLat))|~real(CityLong))|~s__SymbolicString(CityName))|~s__SymbolicString(CityNation))|(![Latitude]: ~int(Latitude)))|~real(MoscowLat))|~real(MoscowLong))|~s__SymbolicString(MoscowName))|~s__SymbolicString(MoscowNation))|~is_instance(Nation,s__OECDMemberEconomiesClass))|~capital_city(City,Nation)))|~look_different(City,s__Moscow))|~latlong(City,CityLat,CityLong,CityName,CityNation)))|~latlong(s__Moscow,MoscowLat,MoscowLong,MoscowName,MoscowNation)))|~to_int(CityLat)=to_int(MoscowLat)))|~s__capability(s__Flooding__t,s__located__m,City))),
% 0.08/0.40 inference(miniscoping,[status(thm)],[f326])).
% 0.08/0.40 fof(f328,plain,(
% 0.08/0.40 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~s__Object(X0)|~s__Object(X1)|~real(X2)|~real(X3)|~s__SymbolicString(X4)|~s__SymbolicString(X5)|~int(X6)|~real(X7)|~real(X8)|~s__SymbolicString(X9)|~s__SymbolicString(X10)|~is_instance(X1,s__OECDMemberEconomiesClass)|~capital_city(X0,X1)|~look_different(X0,s__Moscow)|~latlong(X0,X2,X3,X4,X5)|~latlong(s__Moscow,X7,X8,X9,X10)|~to_int(X2)=to_int(X7)|~s__capability(s__Flooding__t,s__located__m,X0))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f327])).
% 0.08/0.40 fof(f335,plain,(
% 0.08/0.40 is_instance(s__Copenhagen,s__CoastalCitiesClass)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f35])).
% 0.08/0.40 fof(f341,plain,(
% 0.08/0.40 s__Nation(s__Denmark)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f40])).
% 0.08/0.40 fof(f342,plain,(
% 0.08/0.40 is_instance(s__Denmark,s__OECDMemberEconomiesClass)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f41])).
% 0.08/0.40 fof(f403,plain,(
% 0.08/0.40 s__City(s__Copenhagen)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f102])).
% 0.08/0.40 fof(f404,plain,(
% 0.08/0.40 capital_city(s__Copenhagen,s__Denmark)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f103])).
% 0.08/0.40 fof(f451,plain,(
% 0.08/0.40 real('55.67631')),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f150])).
% 0.08/0.40 fof(f452,plain,(
% 0.08/0.40 real('12.569355')),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f151])).
% 0.08/0.40 fof(f453,plain,(
% 0.08/0.40 s__SymbolicString(copenhagen)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f152])).
% 0.08/0.40 fof(f454,plain,(
% 0.08/0.40 s__SymbolicString(dk)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f153])).
% 0.08/0.40 fof(f455,plain,(
% 0.08/0.40 latlong(s__Copenhagen,'55.67631','12.569355',copenhagen,dk)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f154])).
% 0.08/0.40 fof(f471,plain,(
% 0.08/0.40 real('55.75695')),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f170])).
% 0.08/0.40 fof(f472,plain,(
% 0.08/0.40 real('37.614975')),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f171])).
% 0.08/0.40 fof(f473,plain,(
% 0.08/0.40 s__SymbolicString(moscow)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f172])).
% 0.08/0.40 fof(f474,plain,(
% 0.08/0.40 s__SymbolicString(ru)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f173])).
% 0.08/0.40 fof(f475,plain,(
% 0.08/0.40 latlong(s__Moscow,'55.75695','37.614975',moscow,ru)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f174])).
% 0.08/0.40 fof(f507,plain,(
% 0.08/0.40 look_different(s__Copenhagen,s__Moscow)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f206])).
% 0.08/0.40 fof(f538,plain,(
% 0.08/0.40 to_int('55.67631')='55'),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f237])).
% 0.08/0.40 fof(f539,plain,(
% 0.08/0.40 to_int('55.75695')='55'),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f238])).
% 0.08/0.40 fof(f540,plain,(
% 0.08/0.40 int('60')),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f239])).
% 0.08/0.40 fof(f629,plain,(
% 0.08/0.40 s__GeopoliticalArea(s__Denmark)),
% 0.08/0.40 inference(resolution,[status(thm)],[f306,f341])).
% 0.08/0.40 fof(f649,plain,(
% 0.08/0.40 s__GeopoliticalArea(s__Copenhagen)),
% 0.08/0.40 inference(resolution,[status(thm)],[f403,f308])).
% 0.08/0.40 fof(f712,plain,(
% 0.08/0.40 ~s__City(s__Copenhagen)|s__orientation(s__Copenhagen,sK14_skl(s__Copenhagen),s__Near)),
% 0.08/0.40 inference(resolution,[status(thm)],[f335,f323])).
% 0.08/0.40 fof(f713,plain,(
% 0.08/0.40 ~s__City(s__Copenhagen)|s__Sea(sK14_skl(s__Copenhagen))),
% 0.08/0.40 inference(resolution,[status(thm)],[f335,f322])).
% 0.08/0.40 fof(f714,plain,(
% 0.08/0.40 s__orientation(s__Copenhagen,sK14_skl(s__Copenhagen),s__Near)),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f712,f403])).
% 0.08/0.40 fof(f715,plain,(
% 0.08/0.40 s__Sea(sK14_skl(s__Copenhagen))),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f713,f403])).
% 0.08/0.40 fof(f886,plain,(
% 0.08/0.40 s__GeographicArea(s__Denmark)),
% 0.08/0.40 inference(resolution,[status(thm)],[f629,f304])).
% 0.08/0.40 fof(f923,plain,(
% 0.08/0.40 s__GeographicArea(s__Copenhagen)),
% 0.08/0.40 inference(resolution,[status(thm)],[f649,f304])).
% 0.08/0.40 fof(f960,plain,(
% 0.08/0.40 s__Region(s__Denmark)),
% 0.08/0.40 inference(resolution,[status(thm)],[f886,f302])).
% 0.08/0.40 fof(f1000,plain,(
% 0.08/0.40 s__Region(s__Copenhagen)),
% 0.08/0.40 inference(resolution,[status(thm)],[f923,f302])).
% 0.08/0.40 fof(f1033,plain,(
% 0.08/0.40 s__Object(s__Denmark)),
% 0.08/0.40 inference(resolution,[status(thm)],[f960,f300])).
% 0.08/0.40 fof(f1052,plain,(
% 0.08/0.40 s__Object(s__Copenhagen)),
% 0.08/0.40 inference(resolution,[status(thm)],[f1000,f300])).
% 0.08/0.40 fof(f1212,plain,(
% 0.08/0.40 ![X0,X1,X2,X3,X4,X5,X6]: (~s__Object(X0)|~s__Object(X1)|~real(X2)|~real(X3)|~s__SymbolicString(X4)|~s__SymbolicString(X5)|~int(X6)|~real('55.75695')|~real('37.614975')|~s__SymbolicString(moscow)|~s__SymbolicString(ru)|~is_instance(X1,s__OECDMemberEconomiesClass)|~capital_city(X0,X1)|~look_different(X0,s__Moscow)|~latlong(X0,X2,X3,X4,X5)|~to_int(X2)=to_int('55.75695')|~s__capability(s__Flooding__t,s__located__m,X0))),
% 0.08/0.40 inference(resolution,[status(thm)],[f475,f328])).
% 0.08/0.40 fof(f1213,plain,(
% 0.08/0.40 ![X0,X1,X2,X3,X4,X5,X6]: (~s__Object(X0)|~s__Object(X1)|~real(X2)|~real(X3)|~s__SymbolicString(X4)|~s__SymbolicString(X5)|~int(X6)|~real('55.75695')|~real('37.614975')|~s__SymbolicString(moscow)|~s__SymbolicString(ru)|~is_instance(X1,s__OECDMemberEconomiesClass)|~capital_city(X0,X1)|~look_different(X0,s__Moscow)|~latlong(X0,X2,X3,X4,X5)|~to_int(X2)='55'|~s__capability(s__Flooding__t,s__located__m,X0))),
% 0.08/0.40 inference(forward_demodulation,[status(thm)],[f539,f1212])).
% 0.08/0.40 fof(f1214,plain,(
% 0.08/0.40 ![X0,X1,X2,X3,X4,X5,X6]: (~s__Object(X0)|~s__Object(X1)|~real(X2)|~real(X3)|~s__SymbolicString(X4)|~s__SymbolicString(X5)|~int(X6)|~real('37.614975')|~s__SymbolicString(moscow)|~s__SymbolicString(ru)|~is_instance(X1,s__OECDMemberEconomiesClass)|~capital_city(X0,X1)|~look_different(X0,s__Moscow)|~latlong(X0,X2,X3,X4,X5)|~to_int(X2)='55'|~s__capability(s__Flooding__t,s__located__m,X0))),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1213,f471])).
% 0.08/0.40 fof(f1215,plain,(
% 0.08/0.40 ![X0,X1,X2,X3,X4,X5,X6]: (~s__Object(X0)|~s__Object(X1)|~real(X2)|~real(X3)|~s__SymbolicString(X4)|~s__SymbolicString(X5)|~int(X6)|~s__SymbolicString(moscow)|~s__SymbolicString(ru)|~is_instance(X1,s__OECDMemberEconomiesClass)|~capital_city(X0,X1)|~look_different(X0,s__Moscow)|~latlong(X0,X2,X3,X4,X5)|~to_int(X2)='55'|~s__capability(s__Flooding__t,s__located__m,X0))),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1214,f472])).
% 0.08/0.40 fof(f1221,plain,(
% 0.08/0.40 ![X0,X1]: (~s__Object(s__Copenhagen)|~s__Object(X0)|~real('55.67631')|~real('12.569355')|~s__SymbolicString(copenhagen)|~s__SymbolicString(dk)|~int(X1)|~s__SymbolicString(moscow)|~s__SymbolicString(ru)|~is_instance(X0,s__OECDMemberEconomiesClass)|~capital_city(s__Copenhagen,X0)|~look_different(s__Copenhagen,s__Moscow)|~to_int('55.67631')='55'|~s__capability(s__Flooding__t,s__located__m,s__Copenhagen))),
% 0.08/0.40 inference(resolution,[status(thm)],[f1215,f455])).
% 0.08/0.40 fof(f1240,plain,(
% 0.08/0.40 ![X0,X1]: (~s__Object(s__Copenhagen)|~s__Object(X0)|~real('55.67631')|~real('12.569355')|~s__SymbolicString(copenhagen)|~s__SymbolicString(dk)|~int(X1)|~s__SymbolicString(moscow)|~s__SymbolicString(ru)|~is_instance(X0,s__OECDMemberEconomiesClass)|~capital_city(s__Copenhagen,X0)|~look_different(s__Copenhagen,s__Moscow)|~'55'='55'|~s__capability(s__Flooding__t,s__located__m,s__Copenhagen))),
% 0.08/0.40 inference(forward_demodulation,[status(thm)],[f538,f1221])).
% 0.08/0.40 fof(f1241,plain,(
% 0.08/0.40 ![X0,X1]: (~s__Object(s__Copenhagen)|~s__Object(X0)|~real('55.67631')|~real('12.569355')|~s__SymbolicString(copenhagen)|~s__SymbolicString(dk)|~int(X1)|~s__SymbolicString(moscow)|~s__SymbolicString(ru)|~is_instance(X0,s__OECDMemberEconomiesClass)|~capital_city(s__Copenhagen,X0)|~look_different(s__Copenhagen,s__Moscow)|~s__capability(s__Flooding__t,s__located__m,s__Copenhagen))),
% 0.08/0.40 inference(trivial_equality_resolution,[status(thm)],[f1240])).
% 0.08/0.40 fof(f1242,plain,(
% 0.08/0.40 ![X0,X1]: (~s__Object(X0)|~real('55.67631')|~real('12.569355')|~s__SymbolicString(copenhagen)|~s__SymbolicString(dk)|~int(X1)|~s__SymbolicString(moscow)|~s__SymbolicString(ru)|~is_instance(X0,s__OECDMemberEconomiesClass)|~capital_city(s__Copenhagen,X0)|~look_different(s__Copenhagen,s__Moscow)|~s__capability(s__Flooding__t,s__located__m,s__Copenhagen))),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1241,f1052])).
% 0.08/0.40 fof(f1256,plain,(
% 0.08/0.40 ![X0,X1]: (~s__Object(X0)|~real('12.569355')|~s__SymbolicString(copenhagen)|~s__SymbolicString(dk)|~int(X1)|~s__SymbolicString(moscow)|~s__SymbolicString(ru)|~is_instance(X0,s__OECDMemberEconomiesClass)|~capital_city(s__Copenhagen,X0)|~look_different(s__Copenhagen,s__Moscow)|~s__capability(s__Flooding__t,s__located__m,s__Copenhagen))),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1242,f451])).
% 0.08/0.40 fof(f1717,plain,(
% 0.08/0.40 ~s__WaterArea(sK14_skl(s__Copenhagen))|~s__City(s__Copenhagen)|s__capability(s__Flooding__t,s__located__m,s__Copenhagen)),
% 0.08/0.40 inference(resolution,[status(thm)],[f714,f325])).
% 0.08/0.40 fof(f1718,plain,(
% 0.08/0.40 ~s__WaterArea(sK14_skl(s__Copenhagen))|s__capability(s__Flooding__t,s__located__m,s__Copenhagen)),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1717,f403])).
% 0.08/0.40 fof(f1719,plain,(
% 0.08/0.40 s__BodyOfWater(sK14_skl(s__Copenhagen))),
% 0.08/0.40 inference(resolution,[status(thm)],[f715,f314])).
% 0.08/0.40 fof(f1720,plain,(
% 0.08/0.40 s__WaterArea(sK14_skl(s__Copenhagen))),
% 0.08/0.40 inference(resolution,[status(thm)],[f1719,f312])).
% 0.08/0.40 fof(f1721,plain,(
% 0.08/0.40 s__capability(s__Flooding__t,s__located__m,s__Copenhagen)),
% 0.08/0.40 inference(backward_subsumption_resolution,[status(thm)],[f1718,f1720])).
% 0.08/0.40 fof(f1724,plain,(
% 0.08/0.40 ![X0,X1]: (~s__Object(X0)|~real('12.569355')|~s__SymbolicString(copenhagen)|~s__SymbolicString(dk)|~int(X1)|~s__SymbolicString(moscow)|~s__SymbolicString(ru)|~is_instance(X0,s__OECDMemberEconomiesClass)|~capital_city(s__Copenhagen,X0)|~look_different(s__Copenhagen,s__Moscow))),
% 0.08/0.40 inference(backward_subsumption_resolution,[status(thm)],[f1256,f1721])).
% 0.08/0.40 fof(f1725,plain,(
% 0.08/0.40 ![X0,X1]: (~s__Object(X0)|~s__SymbolicString(copenhagen)|~s__SymbolicString(dk)|~int(X1)|~s__SymbolicString(moscow)|~s__SymbolicString(ru)|~is_instance(X0,s__OECDMemberEconomiesClass)|~capital_city(s__Copenhagen,X0)|~look_different(s__Copenhagen,s__Moscow))),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1724,f452])).
% 0.08/0.40 fof(f1726,plain,(
% 0.08/0.40 ![X0,X1]: (~s__Object(X0)|~s__SymbolicString(dk)|~int(X1)|~s__SymbolicString(moscow)|~s__SymbolicString(ru)|~is_instance(X0,s__OECDMemberEconomiesClass)|~capital_city(s__Copenhagen,X0)|~look_different(s__Copenhagen,s__Moscow))),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1725,f453])).
% 0.08/0.40 fof(f1728,plain,(
% 0.08/0.40 ![X0,X1]: (~s__Object(X0)|~s__SymbolicString(dk)|~int(X1)|~s__SymbolicString(moscow)|~s__SymbolicString(ru)|~is_instance(X0,s__OECDMemberEconomiesClass)|~capital_city(s__Copenhagen,X0))),
% 0.08/0.40 inference(resolution,[status(thm)],[f1726,f507])).
% 0.08/0.40 fof(f1730,plain,(
% 0.08/0.40 ![X0,X1]: (~s__Object(X0)|~int(X1)|~s__SymbolicString(moscow)|~s__SymbolicString(ru)|~is_instance(X0,s__OECDMemberEconomiesClass)|~capital_city(s__Copenhagen,X0))),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1728,f454])).
% 0.08/0.40 fof(f1731,plain,(
% 0.08/0.40 ![X0,X1]: (~s__Object(X0)|~int(X1)|~s__SymbolicString(ru)|~is_instance(X0,s__OECDMemberEconomiesClass)|~capital_city(s__Copenhagen,X0))),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1730,f473])).
% 0.08/0.40 fof(f1732,plain,(
% 0.08/0.40 ![X0]: (~s__Object(s__Denmark)|~int(X0)|~s__SymbolicString(ru)|~is_instance(s__Denmark,s__OECDMemberEconomiesClass))),
% 0.08/0.40 inference(resolution,[status(thm)],[f1731,f404])).
% 0.14/0.41 fof(f1733,plain,(
% 0.14/0.41 ![X0]: (~int(X0)|~s__SymbolicString(ru)|~is_instance(s__Denmark,s__OECDMemberEconomiesClass))),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1732,f1033])).
% 0.14/0.41 fof(f1734,plain,(
% 0.14/0.41 ![X0]: (~int(X0)|~is_instance(s__Denmark,s__OECDMemberEconomiesClass))),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1733,f474])).
% 0.14/0.41 fof(f1735,plain,(
% 0.14/0.41 ![X0]: (~int(X0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f1734,f342])).
% 0.14/0.41 fof(f1738,plain,(
% 0.14/0.41 $false),
% 0.14/0.41 inference(backward_subsumption_resolution,[status(thm)],[f540,f1735])).
% 0.14/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.45 % Elapsed time: 0.090893 seconds
% 0.14/0.45 % CPU time: 0.365297 seconds
% 0.14/0.45 % Total memory used: 78.428 MB
% 0.14/0.45 % Net memory used: 78.310 MB
%------------------------------------------------------------------------------