%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : CSR117+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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 : Tue Sep 29 09:41:38 AM UTC 2026
% Result : Theorem 24.99s 3.41s
% Output : Proof 24.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR117+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.18 % Computer : n015.cluster.edu
% 0.06/0.18 % Model : x86_64 x86_64
% 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.18 % Memory : 8046.5625MB
% 0.06/0.18 % OS : Linux 6.8.0-71-generic
% 0.06/0.18 % CPULimit : 300
% 0.06/0.19 % WCLimit : 300
% 0.06/0.19 % DateTime : Mon Sep 28 23:36:47 UTC 2026
% 0.06/0.19 % CPUTime :
% 0.06/0.19 Running run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.99/3.41 Command-line arguments: --lhs-weight 9 --flip-ordering --complete-subsets --normalise-queue-percent 10 --cp-renormalise-threshold 10
% 24.99/3.41
% 24.99/3.41 % SZS status Theorem
% 24.99/3.41
% 24.99/3.47 % SZS output start Proof
% 24.99/3.47 Axiom 1 (copenhagen_lat_type): real(55.67631) = true.
% 24.99/3.47 Axiom 2 (moscow_lat_type): real(55.75695) = true.
% 24.99/3.47 Axiom 3 (copenhagen_long_type): real(12.569355) = true.
% 24.99/3.47 Axiom 4 (moscow_long_type): real(37.614975) = true.
% 24.99/3.47 Axiom 5 (copenhagen_type): s__SymbolicString(copenhagen) = true.
% 24.99/3.47 Axiom 6 (dk_type): s__SymbolicString(dk) = true.
% 24.99/3.47 Axiom 7 (moscow_type): s__SymbolicString(moscow) = true.
% 24.99/3.47 Axiom 8 (ru_type): s__SymbolicString(ru) = true.
% 24.99/3.47 Axiom 9 (s__Denmark_type): s__Nation(s__Denmark) = true.
% 24.99/3.47 Axiom 10 (s__Copenhagen_type): s__City(s__Copenhagen) = true.
% 24.99/3.47 Axiom 11 (48_type): int(48) = true.
% 24.99/3.47 Axiom 12 (55.67631_55): to_int(55.67631) = 55.
% 24.99/3.47 Axiom 13 (55.75695_55): to_int(55.75695) = 55.
% 24.99/3.47 Axiom 14 (copenhagen_coastal): is_instance(s__Copenhagen, s__CoastalCitiesClass) = true.
% 24.99/3.47 Axiom 15 (s__Denmark_OECD): is_instance(s__Denmark, s__OECDMemberEconomiesClass) = true.
% 24.99/3.47 Axiom 16 (s__Copenhagen_s__Denmark): capital_city(s__Copenhagen, s__Denmark) = true.
% 24.99/3.47 Axiom 17 (s__Copenhagen_not_s__Moscow): look_different(s__Copenhagen, s__Moscow) = true.
% 24.99/3.47 Axiom 18 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 24.99/3.47 Axiom 19 (latlong_s__Moscow): latlong(s__Moscow, 55.75695, 37.614975, moscow, ru) = true.
% 24.99/3.47 Axiom 20 (latlong_s__Copenhagen): latlong(s__Copenhagen, 55.67631, 12.569355, copenhagen, dk) = true.
% 24.99/3.47 Axiom 21 (kb_SUMO_MILO_6428): ifeq(s__Nation(X), true, s__GeopoliticalArea(X), true) = true.
% 24.99/3.47 Axiom 22 (kb_SUMO_MILO_6437): ifeq(s__City(X), true, s__GeopoliticalArea(X), true) = true.
% 24.99/3.47 Axiom 23 (kb_SUMO_MILO_6345): ifeq(s__GeopoliticalArea(X), true, s__GeographicArea(X), true) = true.
% 24.99/3.48 Axiom 24 (kb_SUMO_MILO_701): ifeq(s__Region(X), true, s__Object(X), true) = true.
% 24.99/3.48 Axiom 25 (kb_SUMO_MILO_Domains_9582): ifeq(s__BodyOfWater(X), true, s__WaterArea(X), true) = true.
% 24.99/3.48 Axiom 26 (kb_SUMO_MILO_Domains_9679): ifeq(s__Sea(X), true, s__BodyOfWater(X), true) = true.
% 24.99/3.48 Axiom 27 (kb_SUMO_MILO_6365): ifeq(s__GeographicArea(X), true, s__Region(X), true) = true.
% 24.99/3.48 Axiom 28 (coastal_cities_near_water): ifeq(is_instance(X, s__CoastalCitiesClass), true, ifeq(s__City(X), true, s__Sea(sea(X)), true), true) = true.
% 24.99/3.48 Axiom 29 (coastal_cities_near_water_1): ifeq(is_instance(X, s__CoastalCitiesClass), true, ifeq(s__City(X), true, s__orientation(X, sea(X), s__Near), true), true) = true.
% 24.99/3.48 Axiom 30 (flood_near_water): ifeq(s__orientation(X, Y, s__Near), true, ifeq(s__WaterArea(Y), true, ifeq(s__City(X), true, s__capability(s__Flooding__t, s__located__m, X), true), true), true) = true.
% 24.99/3.48
% 24.99/3.48 Goal 1 (where): tuple2(to_int(X), s__Object(Y), s__Object(Z), s__SymbolicString(W), s__SymbolicString(V), s__SymbolicString(U), s__SymbolicString(T), is_instance(Z, s__OECDMemberEconomiesClass), s__capability(s__Flooding__t, s__located__m, Y), real(X), real(S), real(X2), real(Y2), int(Z2), capital_city(Y, Z), look_different(Y, s__Moscow), latlong(Y, X, S, W, V), latlong(s__Moscow, X2, Y2, U, T)) = tuple2(to_int(X2), true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true).
% 24.99/3.48 The goal is true when:
% 24.99/3.48 X = 55.67631
% 24.99/3.48 Y = s__Copenhagen
% 24.99/3.48 Z = s__Denmark
% 24.99/3.48 W = copenhagen
% 24.99/3.48 V = dk
% 24.99/3.48 U = moscow
% 24.99/3.48 T = ru
% 24.99/3.48 S = 12.569355
% 24.99/3.48 X2 = 55.75695
% 24.99/3.48 Y2 = 37.614975
% 24.99/3.48 Z2 = 48
% 24.99/3.48
% 24.99/3.48 Proof:
% 24.99/3.48 tuple2(to_int(55.67631), s__Object(s__Copenhagen), s__Object(s__Denmark), s__SymbolicString(copenhagen), s__SymbolicString(dk), s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), s__capability(s__Flooding__t, s__located__m, s__Copenhagen), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), latlong(s__Copenhagen, 55.67631, 12.569355, copenhagen, dk), latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.48 = { by axiom 20 (latlong_s__Copenhagen) }
% 24.99/3.48 tuple2(to_int(55.67631), s__Object(s__Copenhagen), s__Object(s__Denmark), s__SymbolicString(copenhagen), s__SymbolicString(dk), s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), s__capability(s__Flooding__t, s__located__m, s__Copenhagen), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.48 = { by axiom 12 (55.67631_55) }
% 24.99/3.48 tuple2(55, s__Object(s__Copenhagen), s__Object(s__Denmark), s__SymbolicString(copenhagen), s__SymbolicString(dk), s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), s__capability(s__Flooding__t, s__located__m, s__Copenhagen), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.48 = { by axiom 18 (ifeq_axiom) R->L }
% 24.99/3.48 tuple2(55, ifeq(true, true, s__Object(s__Copenhagen), true), s__Object(s__Denmark), s__SymbolicString(copenhagen), s__SymbolicString(dk), s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), s__capability(s__Flooding__t, s__located__m, s__Copenhagen), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.48 = { by axiom 27 (kb_SUMO_MILO_6365) R->L }
% 24.99/3.48 tuple2(55, ifeq(ifeq(s__GeographicArea(s__Copenhagen), true, s__Region(s__Copenhagen), true), true, s__Object(s__Copenhagen), true), s__Object(s__Denmark), s__SymbolicString(copenhagen), s__SymbolicString(dk), s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), s__capability(s__Flooding__t, s__located__m, s__Copenhagen), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.48 = { by axiom 18 (ifeq_axiom) R->L }
% 24.99/3.48 tuple2(55, ifeq(ifeq(ifeq(true, true, s__GeographicArea(s__Copenhagen), true), true, s__Region(s__Copenhagen), true), true, s__Object(s__Copenhagen), true), s__Object(s__Denmark), s__SymbolicString(copenhagen), s__SymbolicString(dk), s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), s__capability(s__Flooding__t, s__located__m, s__Copenhagen), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.48 = { by axiom 22 (kb_SUMO_MILO_6437) R->L }
% 24.99/3.48 tuple2(55, ifeq(ifeq(ifeq(ifeq(s__City(s__Copenhagen), true, s__GeopoliticalArea(s__Copenhagen), true), true, s__GeographicArea(s__Copenhagen), true), true, s__Region(s__Copenhagen), true), true, s__Object(s__Copenhagen), true), s__Object(s__Denmark), s__SymbolicString(copenhagen), s__SymbolicString(dk), s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), s__capability(s__Flooding__t, s__located__m, s__Copenhagen), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.48 = { by axiom 10 (s__Copenhagen_type) }
% 24.99/3.48 tuple2(55, ifeq(ifeq(ifeq(ifeq(true, true, s__GeopoliticalArea(s__Copenhagen), true), true, s__GeographicArea(s__Copenhagen), true), true, s__Region(s__Copenhagen), true), true, s__Object(s__Copenhagen), true), s__Object(s__Denmark), s__SymbolicString(copenhagen), s__SymbolicString(dk), s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), s__capability(s__Flooding__t, s__located__m, s__Copenhagen), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.48 = { by axiom 18 (ifeq_axiom) }
% 24.99/3.48 tuple2(55, ifeq(ifeq(ifeq(s__GeopoliticalArea(s__Copenhagen), true, s__GeographicArea(s__Copenhagen), true), true, s__Region(s__Copenhagen), true), true, s__Object(s__Copenhagen), true), s__Object(s__Denmark), s__SymbolicString(copenhagen), s__SymbolicString(dk), s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), s__capability(s__Flooding__t, s__located__m, s__Copenhagen), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.48 = { by axiom 23 (kb_SUMO_MILO_6345) }
% 24.99/3.48 tuple2(55, ifeq(ifeq(true, true, s__Region(s__Copenhagen), true), true, s__Object(s__Copenhagen), true), s__Object(s__Denmark), s__SymbolicString(copenhagen), s__SymbolicString(dk), s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), s__capability(s__Flooding__t, s__located__m, s__Copenhagen), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.48 = { by axiom 18 (ifeq_axiom) }
% 24.99/3.48 tuple2(55, ifeq(s__Region(s__Copenhagen), true, s__Object(s__Copenhagen), true), s__Object(s__Denmark), s__SymbolicString(copenhagen), s__SymbolicString(dk), s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), s__capability(s__Flooding__t, s__located__m, s__Copenhagen), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.48 = { by axiom 24 (kb_SUMO_MILO_701) }
% 24.99/3.48 tuple2(55, true, s__Object(s__Denmark), s__SymbolicString(copenhagen), s__SymbolicString(dk), s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), s__capability(s__Flooding__t, s__located__m, s__Copenhagen), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.48 = { by axiom 5 (copenhagen_type) }
% 24.99/3.48 tuple2(55, true, s__Object(s__Denmark), true, s__SymbolicString(dk), s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), s__capability(s__Flooding__t, s__located__m, s__Copenhagen), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.48 = { by axiom 6 (dk_type) }
% 24.99/3.48 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), s__capability(s__Flooding__t, s__located__m, s__Copenhagen), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.48 = { by axiom 18 (ifeq_axiom) R->L }
% 24.99/3.48 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), ifeq(true, true, s__capability(s__Flooding__t, s__located__m, s__Copenhagen), true), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.48 = { by axiom 10 (s__Copenhagen_type) R->L }
% 24.99/3.48 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), ifeq(s__City(s__Copenhagen), true, s__capability(s__Flooding__t, s__located__m, s__Copenhagen), true), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.48 = { by axiom 18 (ifeq_axiom) R->L }
% 24.99/3.48 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), ifeq(true, true, ifeq(s__City(s__Copenhagen), true, s__capability(s__Flooding__t, s__located__m, s__Copenhagen), true), true), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.48 = { by axiom 25 (kb_SUMO_MILO_Domains_9582) R->L }
% 24.99/3.48 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), ifeq(ifeq(s__BodyOfWater(sea(s__Copenhagen)), true, s__WaterArea(sea(s__Copenhagen)), true), true, ifeq(s__City(s__Copenhagen), true, s__capability(s__Flooding__t, s__located__m, s__Copenhagen), true), true), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.48 = { by axiom 18 (ifeq_axiom) R->L }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), ifeq(ifeq(ifeq(true, true, s__BodyOfWater(sea(s__Copenhagen)), true), true, s__WaterArea(sea(s__Copenhagen)), true), true, ifeq(s__City(s__Copenhagen), true, s__capability(s__Flooding__t, s__located__m, s__Copenhagen), true), true), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.49 = { by axiom 28 (coastal_cities_near_water) R->L }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), ifeq(ifeq(ifeq(ifeq(is_instance(s__Copenhagen, s__CoastalCitiesClass), true, ifeq(s__City(s__Copenhagen), true, s__Sea(sea(s__Copenhagen)), true), true), true, s__BodyOfWater(sea(s__Copenhagen)), true), true, s__WaterArea(sea(s__Copenhagen)), true), true, ifeq(s__City(s__Copenhagen), true, s__capability(s__Flooding__t, s__located__m, s__Copenhagen), true), true), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.49 = { by axiom 10 (s__Copenhagen_type) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), ifeq(ifeq(ifeq(ifeq(is_instance(s__Copenhagen, s__CoastalCitiesClass), true, ifeq(true, true, s__Sea(sea(s__Copenhagen)), true), true), true, s__BodyOfWater(sea(s__Copenhagen)), true), true, s__WaterArea(sea(s__Copenhagen)), true), true, ifeq(s__City(s__Copenhagen), true, s__capability(s__Flooding__t, s__located__m, s__Copenhagen), true), true), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.49 = { by axiom 14 (copenhagen_coastal) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), ifeq(ifeq(ifeq(ifeq(true, true, ifeq(true, true, s__Sea(sea(s__Copenhagen)), true), true), true, s__BodyOfWater(sea(s__Copenhagen)), true), true, s__WaterArea(sea(s__Copenhagen)), true), true, ifeq(s__City(s__Copenhagen), true, s__capability(s__Flooding__t, s__located__m, s__Copenhagen), true), true), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.49 = { by axiom 18 (ifeq_axiom) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), ifeq(ifeq(ifeq(ifeq(true, true, s__Sea(sea(s__Copenhagen)), true), true, s__BodyOfWater(sea(s__Copenhagen)), true), true, s__WaterArea(sea(s__Copenhagen)), true), true, ifeq(s__City(s__Copenhagen), true, s__capability(s__Flooding__t, s__located__m, s__Copenhagen), true), true), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.49 = { by axiom 18 (ifeq_axiom) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), ifeq(ifeq(ifeq(s__Sea(sea(s__Copenhagen)), true, s__BodyOfWater(sea(s__Copenhagen)), true), true, s__WaterArea(sea(s__Copenhagen)), true), true, ifeq(s__City(s__Copenhagen), true, s__capability(s__Flooding__t, s__located__m, s__Copenhagen), true), true), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.49 = { by axiom 26 (kb_SUMO_MILO_Domains_9679) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), ifeq(ifeq(true, true, s__WaterArea(sea(s__Copenhagen)), true), true, ifeq(s__City(s__Copenhagen), true, s__capability(s__Flooding__t, s__located__m, s__Copenhagen), true), true), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.49 = { by axiom 18 (ifeq_axiom) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), ifeq(s__WaterArea(sea(s__Copenhagen)), true, ifeq(s__City(s__Copenhagen), true, s__capability(s__Flooding__t, s__located__m, s__Copenhagen), true), true), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.49 = { by axiom 18 (ifeq_axiom) R->L }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), ifeq(true, true, ifeq(s__WaterArea(sea(s__Copenhagen)), true, ifeq(s__City(s__Copenhagen), true, s__capability(s__Flooding__t, s__located__m, s__Copenhagen), true), true), true), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.49 = { by axiom 29 (coastal_cities_near_water_1) R->L }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), ifeq(ifeq(is_instance(s__Copenhagen, s__CoastalCitiesClass), true, ifeq(s__City(s__Copenhagen), true, s__orientation(s__Copenhagen, sea(s__Copenhagen), s__Near), true), true), true, ifeq(s__WaterArea(sea(s__Copenhagen)), true, ifeq(s__City(s__Copenhagen), true, s__capability(s__Flooding__t, s__located__m, s__Copenhagen), true), true), true), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.49 = { by axiom 10 (s__Copenhagen_type) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), ifeq(ifeq(is_instance(s__Copenhagen, s__CoastalCitiesClass), true, ifeq(true, true, s__orientation(s__Copenhagen, sea(s__Copenhagen), s__Near), true), true), true, ifeq(s__WaterArea(sea(s__Copenhagen)), true, ifeq(s__City(s__Copenhagen), true, s__capability(s__Flooding__t, s__located__m, s__Copenhagen), true), true), true), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.49 = { by axiom 14 (copenhagen_coastal) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), ifeq(ifeq(true, true, ifeq(true, true, s__orientation(s__Copenhagen, sea(s__Copenhagen), s__Near), true), true), true, ifeq(s__WaterArea(sea(s__Copenhagen)), true, ifeq(s__City(s__Copenhagen), true, s__capability(s__Flooding__t, s__located__m, s__Copenhagen), true), true), true), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.49 = { by axiom 18 (ifeq_axiom) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), ifeq(ifeq(true, true, s__orientation(s__Copenhagen, sea(s__Copenhagen), s__Near), true), true, ifeq(s__WaterArea(sea(s__Copenhagen)), true, ifeq(s__City(s__Copenhagen), true, s__capability(s__Flooding__t, s__located__m, s__Copenhagen), true), true), true), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.49 = { by axiom 18 (ifeq_axiom) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), ifeq(s__orientation(s__Copenhagen, sea(s__Copenhagen), s__Near), true, ifeq(s__WaterArea(sea(s__Copenhagen)), true, ifeq(s__City(s__Copenhagen), true, s__capability(s__Flooding__t, s__located__m, s__Copenhagen), true), true), true), real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.49 = { by axiom 30 (flood_near_water) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), true, real(55.67631), real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.49 = { by axiom 1 (copenhagen_lat_type) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), true, true, real(12.569355), real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.49 = { by axiom 3 (copenhagen_long_type) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), true, true, true, real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), look_different(s__Copenhagen, s__Moscow), true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.49 = { by axiom 17 (s__Copenhagen_not_s__Moscow) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), true, true, true, real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), true, true, latlong(s__Moscow, 55.75695, 37.614975, moscow, ru))
% 24.99/3.49 = { by axiom 19 (latlong_s__Moscow) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, s__SymbolicString(moscow), s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), true, true, true, real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), true, true, true)
% 24.99/3.49 = { by axiom 7 (moscow_type) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, true, s__SymbolicString(ru), is_instance(s__Denmark, s__OECDMemberEconomiesClass), true, true, true, real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), true, true, true)
% 24.99/3.49 = { by axiom 8 (ru_type) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, true, true, is_instance(s__Denmark, s__OECDMemberEconomiesClass), true, true, true, real(55.75695), real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), true, true, true)
% 24.99/3.49 = { by axiom 2 (moscow_lat_type) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, true, true, is_instance(s__Denmark, s__OECDMemberEconomiesClass), true, true, true, true, real(37.614975), int(48), capital_city(s__Copenhagen, s__Denmark), true, true, true)
% 24.99/3.49 = { by axiom 4 (moscow_long_type) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, true, true, is_instance(s__Denmark, s__OECDMemberEconomiesClass), true, true, true, true, true, int(48), capital_city(s__Copenhagen, s__Denmark), true, true, true)
% 24.99/3.49 = { by axiom 15 (s__Denmark_OECD) }
% 24.99/3.49 tuple2(55, true, s__Object(s__Denmark), true, true, true, true, true, true, true, true, true, true, int(48), capital_city(s__Copenhagen, s__Denmark), true, true, true)
% 24.99/3.49 = { by axiom 18 (ifeq_axiom) R->L }
% 24.99/3.49 tuple2(55, true, ifeq(true, true, s__Object(s__Denmark), true), true, true, true, true, true, true, true, true, true, true, int(48), capital_city(s__Copenhagen, s__Denmark), true, true, true)
% 24.99/3.49 = { by axiom 27 (kb_SUMO_MILO_6365) R->L }
% 24.99/3.49 tuple2(55, true, ifeq(ifeq(s__GeographicArea(s__Denmark), true, s__Region(s__Denmark), true), true, s__Object(s__Denmark), true), true, true, true, true, true, true, true, true, true, true, int(48), capital_city(s__Copenhagen, s__Denmark), true, true, true)
% 24.99/3.49 = { by axiom 18 (ifeq_axiom) R->L }
% 24.99/3.49 tuple2(55, true, ifeq(ifeq(ifeq(true, true, s__GeographicArea(s__Denmark), true), true, s__Region(s__Denmark), true), true, s__Object(s__Denmark), true), true, true, true, true, true, true, true, true, true, true, int(48), capital_city(s__Copenhagen, s__Denmark), true, true, true)
% 24.99/3.49 = { by axiom 21 (kb_SUMO_MILO_6428) R->L }
% 24.99/3.49 tuple2(55, true, ifeq(ifeq(ifeq(ifeq(s__Nation(s__Denmark), true, s__GeopoliticalArea(s__Denmark), true), true, s__GeographicArea(s__Denmark), true), true, s__Region(s__Denmark), true), true, s__Object(s__Denmark), true), true, true, true, true, true, true, true, true, true, true, int(48), capital_city(s__Copenhagen, s__Denmark), true, true, true)
% 24.99/3.49 = { by axiom 9 (s__Denmark_type) }
% 24.99/3.49 tuple2(55, true, ifeq(ifeq(ifeq(ifeq(true, true, s__GeopoliticalArea(s__Denmark), true), true, s__GeographicArea(s__Denmark), true), true, s__Region(s__Denmark), true), true, s__Object(s__Denmark), true), true, true, true, true, true, true, true, true, true, true, int(48), capital_city(s__Copenhagen, s__Denmark), true, true, true)
% 24.99/3.49 = { by axiom 18 (ifeq_axiom) }
% 24.99/3.49 tuple2(55, true, ifeq(ifeq(ifeq(s__GeopoliticalArea(s__Denmark), true, s__GeographicArea(s__Denmark), true), true, s__Region(s__Denmark), true), true, s__Object(s__Denmark), true), true, true, true, true, true, true, true, true, true, true, int(48), capital_city(s__Copenhagen, s__Denmark), true, true, true)
% 24.99/3.49 = { by axiom 23 (kb_SUMO_MILO_6345) }
% 24.99/3.49 tuple2(55, true, ifeq(ifeq(true, true, s__Region(s__Denmark), true), true, s__Object(s__Denmark), true), true, true, true, true, true, true, true, true, true, true, int(48), capital_city(s__Copenhagen, s__Denmark), true, true, true)
% 24.99/3.49 = { by axiom 18 (ifeq_axiom) }
% 24.99/3.49 tuple2(55, true, ifeq(s__Region(s__Denmark), true, s__Object(s__Denmark), true), true, true, true, true, true, true, true, true, true, true, int(48), capital_city(s__Copenhagen, s__Denmark), true, true, true)
% 24.99/3.49 = { by axiom 24 (kb_SUMO_MILO_701) }
% 24.99/3.50 tuple2(55, true, true, true, true, true, true, true, true, true, true, true, true, int(48), capital_city(s__Copenhagen, s__Denmark), true, true, true)
% 24.99/3.50 = { by axiom 16 (s__Copenhagen_s__Denmark) }
% 24.99/3.50 tuple2(55, true, true, true, true, true, true, true, true, true, true, true, true, int(48), true, true, true, true)
% 24.99/3.50 = { by axiom 11 (48_type) }
% 24.99/3.50 tuple2(55, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true)
% 24.99/3.50 = { by axiom 13 (55.75695_55) R->L }
% 24.99/3.50 tuple2(to_int(55.75695), true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true)
% 24.99/3.50 % SZS output end Proof
% 24.99/3.50
% 24.99/3.50 RESULT: Theorem (the conjecture is true).
%------------------------------------------------------------------------------