%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : CSR117+1 : TPTP v9.0.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Jul 24 11:19:52 AM UTC 2025
% Result : Theorem 100.52s 12.97s
% Output : CNFRefutation 100.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 29
% Syntax : Number of formulae : 98 ( 62 unt; 0 def)
% Number of atoms : 210 ( 10 equ)
% Maximal formula atoms : 18 ( 2 avg)
% Number of connectives : 180 ( 68 ~; 65 |; 36 &)
% ( 0 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 1 prp; 0-5 aty)
% Number of functors : 19 ( 19 usr; 17 con; 0-1 aty)
% Number of variables : 55 ( 1 sgn 10 !; 23 ?)
% Comments :
%------------------------------------------------------------------------------
fof(where,plain,
? [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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',where) ).
fof(where_negated,plain,
~ ? [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) ),
inference(negate_conjecture,[status(cth)],[where]) ).
cnf(29,plain,
( ~ s__Object(X0)
| ~ s__Object(X1)
| ~ s__SymbolicString(X2)
| ~ s__SymbolicString(X3)
| ~ s__SymbolicString(X4)
| ~ s__SymbolicString(X5)
| ~ s__capability(s__Flooding__t,s__located__m,X0)
| ~ is_instance(X1,s__OECDMemberEconomiesClass)
| ~ real(X6)
| ~ real(X7)
| ~ real(X8)
| ~ real(X9)
| ~ latlong(X0,X6,X7,X2,X3)
| ~ latlong(s__Moscow,X8,X9,X4,X5)
| to_int(X6) != to_int(X8)
| ~ int(X10)
| ~ capital_city(X0,X1)
| ~ look_different(X0,s__Moscow) ),
inference(cnf,[status(esa)],[where_negated]) ).
cnf(l0,plain,
( ~ s__Object(s__Copenhagen)
| ~ s__Object(s__Denmark)
| ~ s__SymbolicString(copenhagen)
| ~ s__SymbolicString(dk)
| ~ s__SymbolicString(moscow)
| ~ s__SymbolicString(ru)
| ~ s__capability(s__Flooding__t,s__located__m,s__Copenhagen)
| ~ is_instance(s__Denmark,s__OECDMemberEconomiesClass)
| ~ real('55.67631')
| ~ real('12.569355')
| ~ real('55.75695')
| ~ real('37.614975')
| ~ 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')
| ~ int('55')
| ~ capital_city(s__Copenhagen,s__Denmark)
| ~ look_different(s__Copenhagen,s__Moscow) ),
inference(instantiation,[status(thm)],[29]) ).
fof(latlong_s__Copenhagen,plain,
latlong(s__Copenhagen,'55.67631','12.569355',copenhagen,dk),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',latlong_s__Copenhagen) ).
cnf(153,plain,
latlong(s__Copenhagen,'55.67631','12.569355',copenhagen,dk),
inference(cnf,[status(esa)],[latlong_s__Copenhagen]) ).
cnf(l13,plain,
latlong(s__Copenhagen,'55.67631','12.569355',copenhagen,dk),
inference(instantiation,[status(thm)],[153]) ).
fof(kb_SUMO_MILO_701,plain,
! [A] :
( s__Region(A)
=> s__Object(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_MILO_701) ).
cnf(14,plain,
( ~ s__Region(X0)
| s__Object(X0) ),
inference(cnf,[status(esa)],[kb_SUMO_MILO_701]) ).
cnf(l2,plain,
( ~ s__Region(s__Copenhagen)
| s__Object(s__Copenhagen) ),
inference(instantiation,[status(thm)],[14]) ).
fof(latlong_s__Moscow,plain,
latlong(s__Moscow,'55.75695','37.614975',moscow,ru),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',latlong_s__Moscow) ).
cnf(173,plain,
latlong(s__Moscow,'55.75695','37.614975',moscow,ru),
inference(cnf,[status(esa)],[latlong_s__Moscow]) ).
cnf(l34,plain,
latlong(s__Moscow,'55.75695','37.614975',moscow,ru),
inference(instantiation,[status(thm)],[173]) ).
fof(ru_type,plain,
s__SymbolicString(ru),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ru_type) ).
cnf(172,plain,
s__SymbolicString(ru),
inference(cnf,[status(esa)],[ru_type]) ).
cnf(l3,plain,
s__SymbolicString(ru),
inference(instantiation,[status(thm)],[172]) ).
fof(flood_near_water,plain,
! [W,C] :
( ( s__WaterArea(W)
& s__City(C) )
=> ( s__orientation(C,W,s__Near)
=> s__capability(s__Flooding__t,s__located__m,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',flood_near_water) ).
cnf(28,plain,
( ~ s__City(X0)
| ~ s__WaterArea(X1)
| ~ s__orientation(X0,X1,s__Near)
| s__capability(s__Flooding__t,s__located__m,X0) ),
inference(cnf,[status(esa)],[flood_near_water]) ).
cnf(l1,plain,
( ~ s__City(s__Copenhagen)
| ~ s__WaterArea(sK15(s__Copenhagen))
| ~ s__orientation(s__Copenhagen,sK15(s__Copenhagen),s__Near)
| s__capability(s__Flooding__t,s__located__m,s__Copenhagen) ),
inference(instantiation,[status(thm)],[28]) ).
fof(kb_SUMO_MILO_Domains_9582,plain,
! [A] :
( s__BodyOfWater(A)
=> s__WaterArea(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_MILO_Domains_9582) ).
cnf(20,plain,
( ~ s__BodyOfWater(X0)
| s__WaterArea(X0) ),
inference(cnf,[status(esa)],[kb_SUMO_MILO_Domains_9582]) ).
cnf(l21,plain,
( ~ s__BodyOfWater(sK15(s__Copenhagen))
| s__WaterArea(sK15(s__Copenhagen)) ),
inference(instantiation,[status(thm)],[20]) ).
fof('55_type',plain,
int('55'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','55_type') ).
cnf(235,plain,
int('55'),
inference(cnf,[status(esa)],['55_type']) ).
cnf(l126,plain,
int('55'),
inference(instantiation,[status(thm)],[235]) ).
fof(s__Denmark_OECD,plain,
is_instance(s__Denmark,s__OECDMemberEconomiesClass),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s__Denmark_OECD) ).
cnf(40,plain,
is_instance(s__Denmark,s__OECDMemberEconomiesClass),
inference(cnf,[status(esa)],[s__Denmark_OECD]) ).
cnf(l33,plain,
is_instance(s__Denmark,s__OECDMemberEconomiesClass),
inference(instantiation,[status(thm)],[40]) ).
fof(copenhagen_long_type,plain,
real('12.569355'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',copenhagen_long_type) ).
cnf(150,plain,
real('12.569355'),
inference(cnf,[status(esa)],[copenhagen_long_type]) ).
cnf(l28,plain,
real('12.569355'),
inference(instantiation,[status(thm)],[150]) ).
cnf(l40,plain,
( ~ s__Region(s__Denmark)
| s__Object(s__Denmark) ),
inference(instantiation,[status(thm)],[14]) ).
fof(moscow_lat_type,plain,
real('55.75695'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',moscow_lat_type) ).
cnf(169,plain,
real('55.75695'),
inference(cnf,[status(esa)],[moscow_lat_type]) ).
cnf(l82,plain,
real('55.75695'),
inference(instantiation,[status(thm)],[169]) ).
fof(moscow_type,plain,
s__SymbolicString(moscow),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',moscow_type) ).
cnf(171,plain,
s__SymbolicString(moscow),
inference(cnf,[status(esa)],[moscow_type]) ).
cnf(l9,plain,
s__SymbolicString(moscow),
inference(instantiation,[status(thm)],[171]) ).
fof(coastal_cities_near_water,plain,
! [City] :
( s__City(City)
=> ( is_instance(City,s__CoastalCitiesClass)
=> ? [Sea] :
( s__Sea(Sea)
& s__orientation(City,Sea,s__Near) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',coastal_cities_near_water) ).
cnf(27,plain,
( ~ s__City(X0)
| ~ is_instance(X0,s__CoastalCitiesClass)
| s__orientation(X0,sK15(X0),s__Near) ),
inference(cnf,[status(esa)],[coastal_cities_near_water]) ).
cnf(l5,plain,
( ~ s__City(s__Copenhagen)
| ~ is_instance(s__Copenhagen,s__CoastalCitiesClass)
| s__orientation(s__Copenhagen,sK15(s__Copenhagen),s__Near) ),
inference(instantiation,[status(thm)],[27]) ).
fof(moscow_long_type,plain,
real('37.614975'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',moscow_long_type) ).
cnf(170,plain,
real('37.614975'),
inference(cnf,[status(esa)],[moscow_long_type]) ).
cnf(l12,plain,
real('37.614975'),
inference(instantiation,[status(thm)],[170]) ).
fof(kb_SUMO_MILO_6365,plain,
! [A] :
( s__GeographicArea(A)
=> s__Region(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_MILO_6365) ).
cnf(15,plain,
( ~ s__GeographicArea(X0)
| s__Region(X0) ),
inference(cnf,[status(esa)],[kb_SUMO_MILO_6365]) ).
cnf(l418,plain,
( ~ s__GeographicArea(s__Copenhagen)
| s__Region(s__Copenhagen) ),
inference(instantiation,[status(thm)],[15]) ).
fof(kb_SUMO_MILO_6345,plain,
! [A] :
( s__GeopoliticalArea(A)
=> s__GeographicArea(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_MILO_6345) ).
cnf(16,plain,
( ~ s__GeopoliticalArea(X0)
| s__GeographicArea(X0) ),
inference(cnf,[status(esa)],[kb_SUMO_MILO_6345]) ).
cnf(l425,plain,
( ~ s__GeopoliticalArea(s__Copenhagen)
| s__GeographicArea(s__Copenhagen) ),
inference(instantiation,[status(thm)],[16]) ).
fof(s__Copenhagen_s__Denmark,plain,
capital_city(s__Copenhagen,s__Denmark),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s__Copenhagen_s__Denmark) ).
cnf(102,plain,
capital_city(s__Copenhagen,s__Denmark),
inference(cnf,[status(esa)],[s__Copenhagen_s__Denmark]) ).
cnf(l35,plain,
capital_city(s__Copenhagen,s__Denmark),
inference(instantiation,[status(thm)],[102]) ).
fof(s__Copenhagen_type,plain,
s__City(s__Copenhagen),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s__Copenhagen_type) ).
cnf(101,plain,
s__City(s__Copenhagen),
inference(cnf,[status(esa)],[s__Copenhagen_type]) ).
cnf(l30,plain,
s__City(s__Copenhagen),
inference(instantiation,[status(thm)],[101]) ).
cnf(l11,plain,
s__City(s__Copenhagen),
inference(instantiation,[status(thm)],[101]) ).
fof(s__Copenhagen_not_s__Moscow,plain,
look_different(s__Copenhagen,s__Moscow),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s__Copenhagen_not_s__Moscow) ).
cnf(205,plain,
look_different(s__Copenhagen,s__Moscow),
inference(cnf,[status(esa)],[s__Copenhagen_not_s__Moscow]) ).
cnf(l4,plain,
look_different(s__Copenhagen,s__Moscow),
inference(instantiation,[status(thm)],[205]) ).
fof('55.67631_55',plain,
to_int('55.67631') = '55',
file('/export/starexec/sandbox/benchmark/theBenchmark.p','55.67631_55') ).
cnf(236,plain,
to_int('55.67631') = '55',
inference(cnf,[status(esa)],['55.67631_55']) ).
cnf(l48,plain,
to_int('55.67631') = '55',
inference(instantiation,[status(thm)],[236]) ).
fof(copenhagen_type,plain,
s__SymbolicString(copenhagen),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',copenhagen_type) ).
cnf(151,plain,
s__SymbolicString(copenhagen),
inference(cnf,[status(esa)],[copenhagen_type]) ).
cnf(l39,plain,
s__SymbolicString(copenhagen),
inference(instantiation,[status(thm)],[151]) ).
cnf(l42,plain,
( ~ s__GeographicArea(s__Denmark)
| s__Region(s__Denmark) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l75,plain,
( ~ s__GeopoliticalArea(s__Denmark)
| s__GeographicArea(s__Denmark) ),
inference(instantiation,[status(thm)],[16]) ).
fof('55.75695_55',plain,
to_int('55.75695') = '55',
file('/export/starexec/sandbox/benchmark/theBenchmark.p','55.75695_55') ).
cnf(237,plain,
to_int('55.75695') = '55',
inference(cnf,[status(esa)],['55.75695_55']) ).
cnf(l74,plain,
to_int('55.75695') = '55',
inference(instantiation,[status(thm)],[237]) ).
fof(copenhagen_coastal,plain,
is_instance(s__Copenhagen,s__CoastalCitiesClass),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',copenhagen_coastal) ).
cnf(34,plain,
is_instance(s__Copenhagen,s__CoastalCitiesClass),
inference(cnf,[status(esa)],[copenhagen_coastal]) ).
cnf(l10,plain,
is_instance(s__Copenhagen,s__CoastalCitiesClass),
inference(instantiation,[status(thm)],[34]) ).
fof(copenhagen_lat_type,plain,
real('55.67631'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',copenhagen_lat_type) ).
cnf(149,plain,
real('55.67631'),
inference(cnf,[status(esa)],[copenhagen_lat_type]) ).
cnf(l7,plain,
real('55.67631'),
inference(instantiation,[status(thm)],[149]) ).
fof(kb_SUMO_MILO_6428,plain,
! [A] :
( s__Nation(A)
=> s__GeopoliticalArea(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_MILO_6428) ).
cnf(17,plain,
( ~ s__Nation(X0)
| s__GeopoliticalArea(X0) ),
inference(cnf,[status(esa)],[kb_SUMO_MILO_6428]) ).
cnf(l230,plain,
( ~ s__Nation(s__Denmark)
| s__GeopoliticalArea(s__Denmark) ),
inference(instantiation,[status(thm)],[17]) ).
fof(kb_SUMO_MILO_6437,plain,
! [A] :
( s__City(A)
=> s__GeopoliticalArea(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_MILO_6437) ).
cnf(18,plain,
( ~ s__City(X0)
| s__GeopoliticalArea(X0) ),
inference(cnf,[status(esa)],[kb_SUMO_MILO_6437]) ).
cnf(l428,plain,
( ~ s__City(s__Copenhagen)
| s__GeopoliticalArea(s__Copenhagen) ),
inference(instantiation,[status(thm)],[18]) ).
fof(kb_SUMO_MILO_Domains_9679,plain,
! [A] :
( s__Sea(A)
=> s__BodyOfWater(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_MILO_Domains_9679) ).
cnf(21,plain,
( ~ s__Sea(X0)
| s__BodyOfWater(X0) ),
inference(cnf,[status(esa)],[kb_SUMO_MILO_Domains_9679]) ).
cnf(l24,plain,
( ~ s__Sea(sK15(s__Copenhagen))
| s__BodyOfWater(sK15(s__Copenhagen)) ),
inference(instantiation,[status(thm)],[21]) ).
fof(s__Denmark_type,plain,
s__Nation(s__Denmark),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s__Denmark_type) ).
cnf(39,plain,
s__Nation(s__Denmark),
inference(cnf,[status(esa)],[s__Denmark_type]) ).
cnf(l231,plain,
s__Nation(s__Denmark),
inference(instantiation,[status(thm)],[39]) ).
fof(dk_type,plain,
s__SymbolicString(dk),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dk_type) ).
cnf(152,plain,
s__SymbolicString(dk),
inference(cnf,[status(esa)],[dk_type]) ).
cnf(l25,plain,
s__SymbolicString(dk),
inference(instantiation,[status(thm)],[152]) ).
cnf(l440,plain,
s__City(s__Copenhagen),
inference(instantiation,[status(thm)],[101]) ).
cnf(26,plain,
( ~ s__City(X0)
| ~ is_instance(X0,s__CoastalCitiesClass)
| s__Sea(sK15(X0)) ),
inference(cnf,[status(esa)],[coastal_cities_near_water]) ).
cnf(l164,plain,
( ~ s__City(s__Copenhagen)
| ~ is_instance(s__Copenhagen,s__CoastalCitiesClass)
| s__Sea(sK15(s__Copenhagen)) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l296,plain,
s__City(s__Copenhagen),
inference(instantiation,[status(thm)],[101]) ).
cnf(l321,plain,
is_instance(s__Copenhagen,s__CoastalCitiesClass),
inference(instantiation,[status(thm)],[34]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l13,l2,l34,l3,l1,l21,l126,l33,l28,l40,l82,l9,l5,l12,l418,l425,l35,l30,l11,l4,l48,l39,l42,l75,l74,l10,l7,l230,l428,l24,l231,l25,l440,l164,l296,l321]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : CSR117+1 : TPTP v9.0.0. Released v4.1.0.
% 0.11/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n017.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sun Jul 20 08:30:19 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.36 % launching worker at depth: 10
% 0.18/0.46 % launching worker at depth: 11
% 8.98/1.48 % launching worker at depth: 12
% 100.52/12.97 % SZS status Theorem for theBenchmark
% 100.52/12.97 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------