%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : CSR117+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n014.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 : Fri Sep 25 01:11:26 PM UTC 2026
% Result : Theorem 8.23s 1.80s
% Output : CNFRefutation 8.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 30
% Syntax : Number of formulae : 137 ( 62 unt; 0 def)
% Number of atoms : 441 ( 43 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 569 ( 265 ~; 254 |; 39 &)
% ( 0 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 20 ( 18 usr; 1 prp; 0-5 aty)
% Number of functors : 20 ( 20 usr; 18 con; 0-1 aty)
% Number of variables : 184 ( 0 sgn 158 !; 26 ?; 101 :)
% Comments :
%------------------------------------------------------------------------------
fof(f15,axiom,
! [X0] :
( s__Region(X0)
=> s__Object(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_MILO_701) ).
fof(f16,axiom,
! [X0] :
( s__GeographicArea(X0)
=> s__Region(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_MILO_6365) ).
fof(f17,axiom,
! [X0] :
( s__GeopoliticalArea(X0)
=> s__GeographicArea(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_MILO_6345) ).
fof(f18,axiom,
! [X0] :
( s__Nation(X0)
=> s__GeopoliticalArea(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_MILO_6428) ).
fof(f19,axiom,
! [X0] :
( s__City(X0)
=> s__GeopoliticalArea(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_MILO_6437) ).
fof(f21,axiom,
! [X0] :
( s__BodyOfWater(X0)
=> s__WaterArea(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_MILO_Domains_9582) ).
fof(f22,axiom,
! [X0] :
( s__Sea(X0)
=> s__BodyOfWater(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_MILO_Domains_9679) ).
fof(f27,axiom,
! [X0] :
( s__City(X0)
=> ( is_instance(X0,s__CoastalCitiesClass)
=> ? [X1] :
( s__orientation(X0,X1,s__Near)
& s__Sea(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',coastal_cities_near_water) ).
fof(f28,axiom,
! [X0,X1] :
( ( s__City(X1)
& s__WaterArea(X0) )
=> ( s__orientation(X1,X0,s__Near)
=> s__capability(s__Flooding__t,s__located__m,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',flood_near_water) ).
fof(f29,conjecture,
? [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) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',where) ).
fof(f30,negated_conjecture,
~ ? [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(negated_conjecture,[status(cth)],[f29]) ).
fof(f32,axiom,
? [X0] : int(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',int_type) ).
fof(f35,axiom,
is_instance(s__Copenhagen,s__CoastalCitiesClass),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',copenhagen_coastal) ).
fof(f40,axiom,
s__Nation(s__Denmark),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s__Denmark_type) ).
fof(f41,axiom,
is_instance(s__Denmark,s__OECDMemberEconomiesClass),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s__Denmark_OECD) ).
fof(f102,axiom,
s__City(s__Copenhagen),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s__Copenhagen_type) ).
fof(f103,axiom,
capital_city(s__Copenhagen,s__Denmark),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s__Copenhagen_s__Denmark) ).
fof(f150,axiom,
real('55.67631'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',copenhagen_lat_type) ).
fof(f151,axiom,
real('12.569355'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',copenhagen_long_type) ).
fof(f152,axiom,
s__SymbolicString(copenhagen),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',copenhagen_type) ).
fof(f153,axiom,
s__SymbolicString(dk),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dk_type) ).
fof(f154,axiom,
latlong(s__Copenhagen,'55.67631','12.569355',copenhagen,dk),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',latlong_s__Copenhagen) ).
fof(f170,axiom,
real('55.75695'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',moscow_lat_type) ).
fof(f171,axiom,
real('37.614975'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',moscow_long_type) ).
fof(f172,axiom,
s__SymbolicString(moscow),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',moscow_type) ).
fof(f173,axiom,
s__SymbolicString(ru),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ru_type) ).
fof(f174,axiom,
latlong(s__Moscow,'55.75695','37.614975',moscow,ru),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',latlong_s__Moscow) ).
fof(f206,axiom,
look_different(s__Copenhagen,s__Moscow),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s__Copenhagen_not_s__Moscow) ).
fof(f237,axiom,
to_int('55.67631') = '55',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','55.67631_55') ).
fof(f238,axiom,
to_int('55.75695') = '55',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','55.75695_55') ).
fof(f271,plain,
! [X0] :
( ~ s__Region(X0)
| s__Object(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f272,plain,
! [X0] :
( ~ s__GeographicArea(X0)
| s__Region(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f273,plain,
! [X0] :
( ~ s__GeopoliticalArea(X0)
| s__GeographicArea(X0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f274,plain,
! [X0] :
( ~ s__Nation(X0)
| s__GeopoliticalArea(X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f275,plain,
! [X0] :
( ~ s__City(X0)
| s__GeopoliticalArea(X0) ),
inference(ennf_transformation,[],[f19]) ).
fof(f277,plain,
! [X0] :
( ~ s__BodyOfWater(X0)
| s__WaterArea(X0) ),
inference(ennf_transformation,[],[f21]) ).
fof(f278,plain,
! [X0] :
( ~ s__Sea(X0)
| s__BodyOfWater(X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f280,plain,
! [X0] :
( ~ s__City(X0)
| ~ is_instance(X0,s__CoastalCitiesClass)
| ? [X1] :
( s__orientation(X0,X1,s__Near)
& s__Sea(X1) ) ),
inference(ennf_transformation,[],[f27]) ).
fof(f281,plain,
! [X0] :
( ~ s__City(X0)
| ~ is_instance(X0,s__CoastalCitiesClass)
| ? [X1] :
( s__orientation(X0,X1,s__Near)
& s__Sea(X1) ) ),
inference(flattening,[],[f280]) ).
fof(f282,plain,
! [X0,X1] :
( ~ s__City(X1)
| ~ s__WaterArea(X0)
| ~ s__orientation(X1,X0,s__Near)
| s__capability(s__Flooding__t,s__located__m,X1) ),
inference(ennf_transformation,[],[f28]) ).
fof(f283,plain,
! [X0,X1] :
( ~ s__City(X1)
| ~ s__WaterArea(X0)
| ~ s__orientation(X1,X0,s__Near)
| s__capability(s__Flooding__t,s__located__m,X1) ),
inference(flattening,[],[f282]) ).
fof(f284,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(ennf_transformation,[],[f30]) ).
fof(f330,plain,
! [X0] :
( ~ s__City(X0)
| ~ is_instance(X0,s__CoastalCitiesClass)
| ( s__orientation(X0,sK14(X0),s__Near)
& s__Sea(sK14(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X1,sK14(X0))],[f281]) ).
fof(f332,plain,
int(sK16),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(X0,sK16)],[f32]) ).
fof(f347,plain,
! [X0] :
( ~ s__Region(X0)
| s__Object(X0) ),
inference(cnf_transformation,[],[f271]) ).
fof(f348,plain,
! [X0] :
( ~ s__GeographicArea(X0)
| s__Region(X0) ),
inference(cnf_transformation,[],[f272]) ).
fof(f349,plain,
! [X0] :
( ~ s__GeopoliticalArea(X0)
| s__GeographicArea(X0) ),
inference(cnf_transformation,[],[f273]) ).
fof(f350,plain,
! [X0] :
( ~ s__Nation(X0)
| s__GeopoliticalArea(X0) ),
inference(cnf_transformation,[],[f274]) ).
fof(f351,plain,
! [X0] :
( ~ s__City(X0)
| s__GeopoliticalArea(X0) ),
inference(cnf_transformation,[],[f275]) ).
fof(f353,plain,
! [X0] :
( ~ s__BodyOfWater(X0)
| s__WaterArea(X0) ),
inference(cnf_transformation,[],[f277]) ).
fof(f354,plain,
! [X0] :
( ~ s__Sea(X0)
| s__BodyOfWater(X0) ),
inference(cnf_transformation,[],[f278]) ).
fof(f359,plain,
! [X0] :
( ~ s__City(X0)
| ~ is_instance(X0,s__CoastalCitiesClass)
| s__orientation(X0,sK14(X0),s__Near) ),
inference(cnf_transformation,[],[f330]) ).
fof(f360,plain,
! [X0] :
( ~ s__City(X0)
| ~ is_instance(X0,s__CoastalCitiesClass)
| s__Sea(sK14(X0)) ),
inference(cnf_transformation,[],[f330]) ).
fof(f361,plain,
! [X0,X1] :
( ~ s__City(X1)
| ~ s__WaterArea(X0)
| ~ s__orientation(X1,X0,s__Near)
| s__capability(s__Flooding__t,s__located__m,X1) ),
inference(cnf_transformation,[],[f283]) ).
fof(f362,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ 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,[],[f284]) ).
fof(f364,plain,
int(sK16),
inference(cnf_transformation,[],[f332]) ).
fof(f367,plain,
is_instance(s__Copenhagen,s__CoastalCitiesClass),
inference(cnf_transformation,[],[f35]) ).
fof(f372,plain,
s__Nation(s__Denmark),
inference(cnf_transformation,[],[f40]) ).
fof(f373,plain,
is_instance(s__Denmark,s__OECDMemberEconomiesClass),
inference(cnf_transformation,[],[f41]) ).
fof(f434,plain,
s__City(s__Copenhagen),
inference(cnf_transformation,[],[f102]) ).
fof(f435,plain,
capital_city(s__Copenhagen,s__Denmark),
inference(cnf_transformation,[],[f103]) ).
fof(f482,plain,
real('55.67631'),
inference(cnf_transformation,[],[f150]) ).
fof(f483,plain,
real('12.569355'),
inference(cnf_transformation,[],[f151]) ).
fof(f484,plain,
s__SymbolicString(copenhagen),
inference(cnf_transformation,[],[f152]) ).
fof(f485,plain,
s__SymbolicString(dk),
inference(cnf_transformation,[],[f153]) ).
fof(f486,plain,
latlong(s__Copenhagen,'55.67631','12.569355',copenhagen,dk),
inference(cnf_transformation,[],[f154]) ).
fof(f502,plain,
real('55.75695'),
inference(cnf_transformation,[],[f170]) ).
fof(f503,plain,
real('37.614975'),
inference(cnf_transformation,[],[f171]) ).
fof(f504,plain,
s__SymbolicString(moscow),
inference(cnf_transformation,[],[f172]) ).
fof(f505,plain,
s__SymbolicString(ru),
inference(cnf_transformation,[],[f173]) ).
fof(f506,plain,
latlong(s__Moscow,'55.75695','37.614975',moscow,ru),
inference(cnf_transformation,[],[f174]) ).
fof(f538,plain,
look_different(s__Copenhagen,s__Moscow),
inference(cnf_transformation,[],[f206]) ).
fof(f569,plain,
'55' = to_int('55.67631'),
inference(cnf_transformation,[],[f237]) ).
fof(f570,plain,
'55' = to_int('55.75695'),
inference(cnf_transformation,[],[f238]) ).
tcf(c_63,plain,
! [X0: $i] :
( s__Object(X0)
| ~ s__Region(X0) ),
inference(cnf_transformation,[],[f347]) ).
tcf(c_64,plain,
! [X0: $i] :
( s__Region(X0)
| ~ s__GeographicArea(X0) ),
inference(cnf_transformation,[],[f348]) ).
tcf(c_65,plain,
! [X0: $i] :
( s__GeographicArea(X0)
| ~ s__GeopoliticalArea(X0) ),
inference(cnf_transformation,[],[f349]) ).
tcf(c_66,plain,
! [X0: $i] :
( s__GeopoliticalArea(X0)
| ~ s__Nation(X0) ),
inference(cnf_transformation,[],[f350]) ).
tcf(c_67,plain,
! [X0: $i] :
( s__GeopoliticalArea(X0)
| ~ s__City(X0) ),
inference(cnf_transformation,[],[f351]) ).
tcf(c_69,plain,
! [X0: $i] :
( s__WaterArea(X0)
| ~ s__BodyOfWater(X0) ),
inference(cnf_transformation,[],[f353]) ).
tcf(c_70,plain,
! [X0: $i] :
( s__BodyOfWater(X0)
| ~ s__Sea(X0) ),
inference(cnf_transformation,[],[f354]) ).
tcf(c_75,plain,
! [X0: $i] :
( s__Sea(sK14(X0))
| ~ s__City(X0)
| ~ is_instance(X0,s__CoastalCitiesClass) ),
inference(cnf_transformation,[],[f360]) ).
tcf(c_76,plain,
! [X0: $i] :
( s__orientation(X0,sK14(X0),s__Near)
| ~ s__City(X0)
| ~ is_instance(X0,s__CoastalCitiesClass) ),
inference(cnf_transformation,[],[f359]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i] :
( s__capability(s__Flooding__t,s__located__m,X0)
| ~ s__WaterArea(X1)
| ~ s__City(X0)
| ~ s__orientation(X0,X1,s__Near) ),
inference(cnf_transformation,[],[f361]) ).
tcf(c_78,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] :
( ~ int(X10)
| ~ real(X6)
| ~ real(X3)
| ~ real(X1)
| ~ real(X0)
| ~ s__SymbolicString(X8)
| ~ s__SymbolicString(X7)
| ~ s__SymbolicString(X5)
| ~ s__SymbolicString(X4)
| ~ s__Object(X9)
| ~ s__Object(X2)
| ~ look_different(X2,s__Moscow)
| ~ is_instance(X9,s__OECDMemberEconomiesClass)
| ~ capital_city(X2,X9)
| ~ s__capability(s__Flooding__t,s__located__m,X2)
| ~ latlong(s__Moscow,X1,X6,X7,X8)
| ~ latlong(X2,X0,X3,X4,X5)
| ( to_int(X0) != to_int(X1) ) ),
inference(cnf_transformation,[],[f362]) ).
tcf(c_80,plain,
int(sK16),
inference(cnf_transformation,[],[f364]) ).
tcf(c_83,plain,
is_instance(s__Copenhagen,s__CoastalCitiesClass),
inference(cnf_transformation,[],[f367]) ).
tcf(c_88,plain,
s__Nation(s__Denmark),
inference(cnf_transformation,[],[f372]) ).
tcf(c_89,plain,
is_instance(s__Denmark,s__OECDMemberEconomiesClass),
inference(cnf_transformation,[],[f373]) ).
tcf(c_150,plain,
s__City(s__Copenhagen),
inference(cnf_transformation,[],[f434]) ).
tcf(c_151,plain,
capital_city(s__Copenhagen,s__Denmark),
inference(cnf_transformation,[],[f435]) ).
tcf(c_198,plain,
real('55.67631'),
inference(cnf_transformation,[],[f482]) ).
tcf(c_199,plain,
real('12.569355'),
inference(cnf_transformation,[],[f483]) ).
tcf(c_200,plain,
s__SymbolicString(copenhagen),
inference(cnf_transformation,[],[f484]) ).
tcf(c_201,plain,
s__SymbolicString(dk),
inference(cnf_transformation,[],[f485]) ).
tcf(c_202,plain,
latlong(s__Copenhagen,'55.67631','12.569355',copenhagen,dk),
inference(cnf_transformation,[],[f486]) ).
tcf(c_218,plain,
real('55.75695'),
inference(cnf_transformation,[],[f502]) ).
tcf(c_219,plain,
real('37.614975'),
inference(cnf_transformation,[],[f503]) ).
tcf(c_220,plain,
s__SymbolicString(moscow),
inference(cnf_transformation,[],[f504]) ).
tcf(c_221,plain,
s__SymbolicString(ru),
inference(cnf_transformation,[],[f505]) ).
tcf(c_222,plain,
latlong(s__Moscow,'55.75695','37.614975',moscow,ru),
inference(cnf_transformation,[],[f506]) ).
tcf(c_254,plain,
look_different(s__Copenhagen,s__Moscow),
inference(cnf_transformation,[],[f538]) ).
tcf(c_285,plain,
to_int('55.67631') = '55',
inference(cnf_transformation,[],[f569]) ).
tcf(c_286,plain,
to_int('55.75695') = '55',
inference(cnf_transformation,[],[f570]) ).
tcf(c_1067,plain,
! [X0: $i,X1: $i] :
( s__Object(X1)
| ~ s__GeographicArea(X0)
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_64,c_63]) ).
tcf(c_1068,plain,
! [X0: $i] :
( s__Object(X0)
| ~ s__GeographicArea(X0) ),
inference(unflattening,[status(thm)],[c_1067]) ).
tcf(c_1083,plain,
! [X0: $i,X1: $i] :
( s__WaterArea(X1)
| ~ s__Sea(X0)
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_70,c_69]) ).
tcf(c_1084,plain,
! [X0: $i] :
( s__WaterArea(X0)
| ~ s__Sea(X0) ),
inference(unflattening,[status(thm)],[c_1083]) ).
tcf(c_1105,plain,
! [X0: $i,X1: $i] :
( s__WaterArea(X1)
| ~ s__City(X0)
| ~ is_instance(X0,s__CoastalCitiesClass)
| ( sK14(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_1084,c_75]) ).
tcf(c_1106,plain,
! [X0: $i] :
( s__WaterArea(sK14(X0))
| ~ s__City(X0)
| ~ is_instance(X0,s__CoastalCitiesClass) ),
inference(unflattening,[status(thm)],[c_1105]) ).
tcf(c_1129,plain,
! [X0: $i,X1: $i] :
( s__Object(X1)
| ~ s__GeopoliticalArea(X0)
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_65,c_1068]) ).
tcf(c_1130,plain,
! [X0: $i] :
( s__Object(X0)
| ~ s__GeopoliticalArea(X0) ),
inference(unflattening,[status(thm)],[c_1129]) ).
tcf(c_1141,plain,
! [X0: $i,X1: $i,X2: $i] :
( s__capability(s__Flooding__t,s__located__m,X2)
| ~ s__WaterArea(X1)
| ~ s__City(X2)
| ~ s__City(X0)
| ~ is_instance(X0,s__CoastalCitiesClass)
| ( s__Near != s__Near )
| ( X0 != X2 )
| ( sK14(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_76,c_77]) ).
tcf(c_1142,plain,
! [X0: $i] :
( s__capability(s__Flooding__t,s__located__m,X0)
| ~ s__City(X0)
| ~ is_instance(X0,s__CoastalCitiesClass)
| ~ s__WaterArea(sK14(X0)) ),
inference(unflattening,[status(thm)],[c_1141]) ).
tcf(c_1144,plain,
! [X0: $i] :
( s__capability(s__Flooding__t,s__located__m,X0)
| ~ s__City(X0)
| ~ is_instance(X0,s__CoastalCitiesClass) ),
inference(global_subsumption_just,[status(thm)],[c_1142,c_1106,c_1142]) ).
tcf(c_1724,plain,
! [X0: $i] :
( s__GeopoliticalArea(X0)
| ( X0 != s__Denmark ) ),
inference(resolution_lifted,[status(thm)],[c_66,c_88]) ).
tcf(c_1725,plain,
s__GeopoliticalArea(s__Denmark),
inference(unflattening,[status(thm)],[c_1724]) ).
tcf(c_2023,plain,
! [X0: $i,X1: $i] :
( s__Object(X1)
| ~ s__City(X0)
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_67,c_1130]) ).
tcf(c_2024,plain,
! [X0: $i] :
( s__Object(X0)
| ~ s__City(X0) ),
inference(unflattening,[status(thm)],[c_2023]) ).
tcf(c_2069,plain,
! [X0: $i] :
( s__Object(X0)
| ( X0 != s__Denmark ) ),
inference(resolution_lifted,[status(thm)],[c_1130,c_1725]) ).
tcf(c_2070,plain,
s__Object(s__Denmark),
inference(unflattening,[status(thm)],[c_2069]) ).
tcf(c_3577,plain,
! [X0: $i] :
( s__Object(X0)
| ( X0 != s__Copenhagen ) ),
inference(resolution_lifted,[status(thm)],[c_2024,c_150]) ).
tcf(c_3578,plain,
s__Object(s__Copenhagen),
inference(unflattening,[status(thm)],[c_3577]) ).
tcf(c_3582,plain,
! [X0: $i] :
( s__capability(s__Flooding__t,s__located__m,X0)
| ~ is_instance(X0,s__CoastalCitiesClass)
| ( X0 != s__Copenhagen ) ),
inference(resolution_lifted,[status(thm)],[c_1144,c_150]) ).
tcf(c_3583,plain,
( s__capability(s__Flooding__t,s__located__m,s__Copenhagen)
| ~ is_instance(s__Copenhagen,s__CoastalCitiesClass) ),
inference(unflattening,[status(thm)],[c_3582]) ).
tcf(c_6091,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] :
( ~ real(X7)
| ~ real(X4)
| ~ real(X1)
| ~ real(X0)
| ~ s__SymbolicString(X9)
| ~ s__SymbolicString(X8)
| ~ s__SymbolicString(X6)
| ~ s__SymbolicString(X5)
| ~ s__Object(X10)
| ~ s__Object(X3)
| ~ look_different(X3,s__Moscow)
| ~ is_instance(X10,s__OECDMemberEconomiesClass)
| ~ capital_city(X3,X10)
| ~ s__capability(s__Flooding__t,s__located__m,X3)
| ~ latlong(s__Moscow,X1,X7,X8,X9)
| ~ latlong(X3,X0,X4,X5,X6)
| ( X2 != sK16 )
| ( to_int(X0) != to_int(X1) ) ),
inference(resolution_lifted,[status(thm)],[c_78,c_80]) ).
tcf(c_6092,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] :
( ~ real(X6)
| ~ real(X3)
| ~ real(X1)
| ~ real(X0)
| ~ s__SymbolicString(X8)
| ~ s__SymbolicString(X7)
| ~ s__SymbolicString(X5)
| ~ s__SymbolicString(X4)
| ~ s__Object(X9)
| ~ s__Object(X2)
| ~ look_different(X2,s__Moscow)
| ~ is_instance(X9,s__OECDMemberEconomiesClass)
| ~ capital_city(X2,X9)
| ~ s__capability(s__Flooding__t,s__located__m,X2)
| ~ latlong(s__Moscow,X1,X6,X7,X8)
| ~ latlong(X2,X0,X3,X4,X5)
| ( to_int(X0) != to_int(X1) ) ),
inference(unflattening,[status(thm)],[c_6091]) ).
tcf(c_8113,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_18656,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
( ~ real('37.614975')
| ~ real(X3)
| ~ real(X1)
| ~ real(X0)
| ~ s__SymbolicString(X7)
| ~ s__SymbolicString(X6)
| ~ s__SymbolicString(X5)
| ~ s__SymbolicString(X4)
| ~ s__Object(X8)
| ~ s__Object(X2)
| ~ look_different(X2,s__Moscow)
| ~ is_instance(X8,s__OECDMemberEconomiesClass)
| ~ capital_city(X2,X8)
| ~ s__capability(s__Flooding__t,s__located__m,X2)
| ~ latlong(s__Moscow,X1,'37.614975',X6,X7)
| ~ latlong(X2,X0,X3,X4,X5)
| ( to_int(X0) != to_int(X1) ) ),
inference(instantiation,[status(thm)],[c_6092]) ).
tcf(c_19482,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( ~ real('37.614975')
| ~ s__Object(s__Copenhagen)
| ~ real(X2)
| ~ real(X1)
| ~ real(X0)
| ~ s__SymbolicString(X6)
| ~ s__SymbolicString(X5)
| ~ s__SymbolicString(X4)
| ~ s__SymbolicString(X3)
| ~ s__Object(X7)
| ~ look_different(s__Copenhagen,s__Moscow)
| ~ capital_city(s__Copenhagen,X7)
| ~ is_instance(X7,s__OECDMemberEconomiesClass)
| ~ s__capability(s__Flooding__t,s__located__m,s__Copenhagen)
| ~ latlong(s__Moscow,X1,'37.614975',X5,X6)
| ~ latlong(s__Copenhagen,X0,X2,X3,X4)
| ( to_int(X0) != to_int(X1) ) ),
inference(instantiation,[status(thm)],[c_18656]) ).
tcf(c_21411,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( ~ real('37.614975')
| ~ s__Object(s__Denmark)
| ~ s__Object(s__Copenhagen)
| ~ real(X2)
| ~ real(X1)
| ~ real(X0)
| ~ s__SymbolicString(X6)
| ~ s__SymbolicString(X5)
| ~ s__SymbolicString(X4)
| ~ s__SymbolicString(X3)
| ~ look_different(s__Copenhagen,s__Moscow)
| ~ capital_city(s__Copenhagen,s__Denmark)
| ~ is_instance(s__Denmark,s__OECDMemberEconomiesClass)
| ~ s__capability(s__Flooding__t,s__located__m,s__Copenhagen)
| ~ latlong(s__Moscow,X1,'37.614975',X5,X6)
| ~ latlong(s__Copenhagen,X0,X2,X3,X4)
| ( to_int(X0) != to_int(X1) ) ),
inference(instantiation,[status(thm)],[c_19482]) ).
tcf(c_21684,plain,
! [X0: $i,X1: $i] :
( ( to_int('55.67631') = X1 )
| ( X1 != X0 )
| ( to_int('55.67631') != X0 ) ),
inference(instantiation,[status(thm)],[c_8113]) ).
tcf(c_22754,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ real('37.614975')
| ~ real('55.75695')
| ~ s__SymbolicString(ru)
| ~ s__SymbolicString(moscow)
| ~ s__Object(s__Denmark)
| ~ s__Object(s__Copenhagen)
| ~ real(X1)
| ~ real(X0)
| ~ s__SymbolicString(X3)
| ~ s__SymbolicString(X2)
| ~ look_different(s__Copenhagen,s__Moscow)
| ~ capital_city(s__Copenhagen,s__Denmark)
| ~ is_instance(s__Denmark,s__OECDMemberEconomiesClass)
| ~ s__capability(s__Flooding__t,s__located__m,s__Copenhagen)
| ~ latlong(s__Moscow,'55.75695','37.614975',moscow,ru)
| ~ latlong(s__Copenhagen,X0,X1,X2,X3)
| ( to_int(X0) != to_int('55.75695') ) ),
inference(instantiation,[status(thm)],[c_21411]) ).
tcf(c_22851,plain,
! [X0: $i] :
( ( to_int('55.67631') = X0 )
| ( X0 != '55' )
| ( to_int('55.67631') != '55' ) ),
inference(instantiation,[status(thm)],[c_21684]) ).
tcf(c_23714,plain,
( ~ real('37.614975')
| ~ real('55.75695')
| ~ real('12.569355')
| ~ real('55.67631')
| ~ s__SymbolicString(ru)
| ~ s__SymbolicString(moscow)
| ~ s__SymbolicString(dk)
| ~ s__SymbolicString(copenhagen)
| ~ s__Object(s__Denmark)
| ~ s__Object(s__Copenhagen)
| ~ look_different(s__Copenhagen,s__Moscow)
| ~ capital_city(s__Copenhagen,s__Denmark)
| ~ is_instance(s__Denmark,s__OECDMemberEconomiesClass)
| ~ s__capability(s__Flooding__t,s__located__m,s__Copenhagen)
| ~ latlong(s__Copenhagen,'55.67631','12.569355',copenhagen,dk)
| ~ latlong(s__Moscow,'55.75695','37.614975',moscow,ru)
| ( to_int('55.67631') != to_int('55.75695') ) ),
inference(instantiation,[status(thm)],[c_22754]) ).
tcf(c_23854,plain,
( ( to_int('55.67631') = to_int('55.75695') )
| ( to_int('55.75695') != '55' )
| ( to_int('55.67631') != '55' ) ),
inference(instantiation,[status(thm)],[c_22851]) ).
tcf(c_23855,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_23854,c_23714,c_3583,c_3578,c_2070,c_202,c_222,c_285,c_286,c_83,c_89,c_151,c_254,c_198,c_199,c_200,c_201,c_218,c_219,c_220,c_221]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR117+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.38 % Computer : n014.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Fri Sep 25 09:49:48 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.43
% 0.13/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.43
% 0.13/0.43 % Detected problem language: tptp
% 0.13/0.45 % Proving...
% 8.23/1.80 % SZS status Started for theBenchmark.p
% 8.23/1.80 % SZS status Theorem for theBenchmark.p
% 8.23/1.80
% 8.23/1.80 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.23/1.80
% 8.23/1.80 % ------ iProver source info
% 8.23/1.80
% 8.23/1.80 % git: date: 2026-07-19 20:42:38 +0200
% 8.23/1.80 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.23/1.80 % git: non_committed_changes: false
% 8.23/1.80
% 8.23/1.80 % ------ Parsing...
% 8.23/1.80 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 8.23/1.80
% 8.23/1.80 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e %
% 8.23/1.80
% 8.23/1.80 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 8.23/1.80
% 8.23/1.80 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 8.23/1.80 % ------ Proving...
% 8.23/1.80 % ------ Problem Properties
% 8.23/1.80
% 8.23/1.80 %
% 8.23/1.80 % clauses 929
% 8.23/1.80 % conjectures 0
% 8.23/1.80 % EPR 884
% 8.23/1.80 % Horn 929
% 8.23/1.80 % unary 881
% 8.23/1.80 % binary 47
% 8.23/1.80 % lits 992
% 8.23/1.80 % lits eq 595
% 8.23/1.80 % fd_pure 0
% 8.23/1.80 % fd_pseudo 0
% 8.23/1.80 % fd_cond 0
% 8.23/1.80 % fd_pseudo_cond 0
% 8.23/1.80 % AC symbols 0
% 8.23/1.80
% 8.23/1.80 % ------ Input Options Time Limit: Unbounded
% 8.23/1.80
% 8.23/1.80
% 8.23/1.80 % ------
% 8.23/1.80 % Current options:
% 8.23/1.80 % ------
% 8.23/1.80
% 8.23/1.80
% 8.23/1.80 %
% 8.23/1.80
% 8.23/1.80 % ------ Proving...
% 8.23/1.80 %
% 8.23/1.80
% 8.23/1.80 % SZS status Theorem for theBenchmark.p
% 8.23/1.80
% 8.23/1.80 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.23/1.81
% 8.23/1.81
%------------------------------------------------------------------------------