%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : CSR117+1 : TPTP v9.0.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n013.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 : Sat Jun 21 05:04:14 AM UTC 2025
% Result : Theorem 0.20s 0.44s
% Output : Proof 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CSR117+1 : TPTP v9.0.0. Released v4.1.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n013.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 : Thu Jun 19 13:03:38 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.20/0.44 % SZS status Theorem
% 0.20/0.44 % SZS output start Proof
% 0.20/0.44 tff(s__capability_type, type, (
% 0.20/0.44 s__capability: ( $i * $i * $i ) > $o)).
% 0.20/0.44 tff(s__Copenhagen_type, type, (
% 0.20/0.44 s__Copenhagen: $i)).
% 0.20/0.44 tff(s__located__m_type, type, (
% 0.20/0.44 s__located__m: $i)).
% 0.20/0.44 tff(s__Flooding__t_type, type, (
% 0.20/0.44 s__Flooding__t: $i)).
% 0.20/0.44 tff(s__WaterArea_type, type, (
% 0.20/0.44 s__WaterArea: $i > $o)).
% 0.20/0.44 tff(tptp_fun_Sea_14_type, type, (
% 0.20/0.44 tptp_fun_Sea_14: $i > $i)).
% 0.20/0.44 tff(s__BodyOfWater_type, type, (
% 0.20/0.44 s__BodyOfWater: $i > $o)).
% 0.20/0.44 tff(s__Sea_type, type, (
% 0.20/0.44 s__Sea: $i > $o)).
% 0.20/0.44 tff(s__orientation_type, type, (
% 0.20/0.44 s__orientation: ( $i * $i * $i ) > $o)).
% 0.20/0.44 tff(s__Near_type, type, (
% 0.20/0.44 s__Near: $i)).
% 0.20/0.44 tff(s__City_type, type, (
% 0.20/0.44 s__City: $i > $o)).
% 0.20/0.44 tff(is_instance_type, type, (
% 0.20/0.44 is_instance: ( $i * $i ) > $o)).
% 0.20/0.44 tff(s__CoastalCitiesClass_type, type, (
% 0.20/0.44 s__CoastalCitiesClass: $i)).
% 0.20/0.44 tff(s__Object_type, type, (
% 0.20/0.44 s__Object: $i > $o)).
% 0.20/0.44 tff(s__Denmark_type, type, (
% 0.20/0.44 s__Denmark: $i)).
% 0.20/0.44 tff(s__Region_type, type, (
% 0.20/0.44 s__Region: $i > $o)).
% 0.20/0.44 tff(s__GeographicArea_type, type, (
% 0.20/0.44 s__GeographicArea: $i > $o)).
% 0.20/0.44 tff(s__GeopoliticalArea_type, type, (
% 0.20/0.44 s__GeopoliticalArea: $i > $o)).
% 0.20/0.44 tff(s__Nation_type, type, (
% 0.20/0.44 s__Nation: $i > $o)).
% 0.20/0.44 tff(to_int_type, type, (
% 0.20/0.44 to_int: $i > $i)).
% 0.20/0.44 tff(tptp_fun__55_75695__type, type, (
% 0.20/0.44 tptp_fun__55_75695_: $i)).
% 0.20/0.44 tff(tptp_fun__55_67631__type, type, (
% 0.20/0.44 tptp_fun__55_67631_: $i)).
% 0.20/0.44 tff(tptp_fun__55__type, type, (
% 0.20/0.44 tptp_fun__55_: $i)).
% 0.20/0.44 tff(look_different_type, type, (
% 0.20/0.44 look_different: ( $i * $i ) > $o)).
% 0.20/0.44 tff(s__Moscow_type, type, (
% 0.20/0.44 s__Moscow: $i)).
% 0.20/0.44 tff(latlong_type, type, (
% 0.20/0.44 latlong: ( $i * $i * $i * $i * $i ) > $o)).
% 0.20/0.44 tff(ru_type, type, (
% 0.20/0.44 ru: $i)).
% 0.20/0.44 tff(moscow_type, type, (
% 0.20/0.44 moscow: $i)).
% 0.20/0.44 tff(tptp_fun__37_614975__type, type, (
% 0.20/0.44 tptp_fun__37_614975_: $i)).
% 0.20/0.44 tff(s__SymbolicString_type, type, (
% 0.20/0.44 s__SymbolicString: $i > $o)).
% 0.20/0.44 tff(real_type, type, (
% 0.20/0.44 real: $i > $o)).
% 0.20/0.44 tff(dk_type, type, (
% 0.20/0.44 dk: $i)).
% 0.20/0.44 tff(copenhagen_type, type, (
% 0.20/0.44 copenhagen: $i)).
% 0.20/0.44 tff(tptp_fun__12_569355__type, type, (
% 0.20/0.44 tptp_fun__12_569355_: $i)).
% 0.20/0.44 tff(capital_city_type, type, (
% 0.20/0.44 capital_city: ( $i * $i ) > $o)).
% 0.20/0.44 tff(s__OECDMemberEconomiesClass_type, type, (
% 0.20/0.44 s__OECDMemberEconomiesClass: $i)).
% 0.20/0.44 tff(int_type, type, (
% 0.20/0.44 int: $i > $o)).
% 0.20/0.44 tff(tptp_fun_A_16_type, type, (
% 0.20/0.44 tptp_fun_A_16: $i)).
% 0.20/0.44 tff(1,plain,
% 0.20/0.44 (s__City(s__Copenhagen) <=> s__City(s__Copenhagen)),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(2,axiom,(s__City(s__Copenhagen)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','s__Copenhagen_type')).
% 0.20/0.44 tff(3,plain,
% 0.20/0.44 (s__City(s__Copenhagen)),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[2, 1])).
% 0.20/0.44 tff(4,plain,
% 0.20/0.44 (is_instance(s__Copenhagen, s__CoastalCitiesClass) <=> is_instance(s__Copenhagen, s__CoastalCitiesClass)),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(5,axiom,(is_instance(s__Copenhagen, s__CoastalCitiesClass)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','copenhagen_coastal')).
% 0.20/0.44 tff(6,plain,
% 0.20/0.44 (is_instance(s__Copenhagen, s__CoastalCitiesClass)),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[5, 4])).
% 0.20/0.44 tff(7,plain,
% 0.20/0.44 (^[City: $i] : refl(((~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)) | (~((~s__Sea(tptp_fun_Sea_14(City))) | (~s__orientation(City, tptp_fun_Sea_14(City), s__Near))))) <=> ((~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)) | (~((~s__Sea(tptp_fun_Sea_14(City))) | (~s__orientation(City, tptp_fun_Sea_14(City), s__Near))))))),
% 0.20/0.44 inference(bind,[status(th)],[])).
% 0.20/0.44 tff(8,plain,
% 0.20/0.44 (![City: $i] : ((~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)) | (~((~s__Sea(tptp_fun_Sea_14(City))) | (~s__orientation(City, tptp_fun_Sea_14(City), s__Near))))) <=> ![City: $i] : ((~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)) | (~((~s__Sea(tptp_fun_Sea_14(City))) | (~s__orientation(City, tptp_fun_Sea_14(City), s__Near)))))),
% 0.20/0.44 inference(quant_intro,[status(thm)],[7])).
% 0.20/0.44 tff(9,plain,
% 0.20/0.44 (^[City: $i] : rewrite(((~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)) | (s__Sea(tptp_fun_Sea_14(City)) & s__orientation(City, tptp_fun_Sea_14(City), s__Near))) <=> ((~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)) | (~((~s__Sea(tptp_fun_Sea_14(City))) | (~s__orientation(City, tptp_fun_Sea_14(City), s__Near))))))),
% 0.20/0.44 inference(bind,[status(th)],[])).
% 0.20/0.44 tff(10,plain,
% 0.20/0.44 (![City: $i] : ((~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)) | (s__Sea(tptp_fun_Sea_14(City)) & s__orientation(City, tptp_fun_Sea_14(City), s__Near))) <=> ![City: $i] : ((~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)) | (~((~s__Sea(tptp_fun_Sea_14(City))) | (~s__orientation(City, tptp_fun_Sea_14(City), s__Near)))))),
% 0.20/0.44 inference(quant_intro,[status(thm)],[9])).
% 0.20/0.44 tff(11,plain,
% 0.20/0.44 (^[City: $i] : rewrite(((s__Sea(tptp_fun_Sea_14(City)) & s__orientation(City, tptp_fun_Sea_14(City), s__Near)) | (~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass))) <=> ((~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)) | (s__Sea(tptp_fun_Sea_14(City)) & s__orientation(City, tptp_fun_Sea_14(City), s__Near))))),
% 0.20/0.44 inference(bind,[status(th)],[])).
% 0.20/0.44 tff(12,plain,
% 0.20/0.44 (![City: $i] : ((s__Sea(tptp_fun_Sea_14(City)) & s__orientation(City, tptp_fun_Sea_14(City), s__Near)) | (~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass))) <=> ![City: $i] : ((~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)) | (s__Sea(tptp_fun_Sea_14(City)) & s__orientation(City, tptp_fun_Sea_14(City), s__Near)))),
% 0.20/0.44 inference(quant_intro,[status(thm)],[11])).
% 0.20/0.44 tff(13,plain,
% 0.20/0.44 (![City: $i] : (?[Sea: $i] : (s__Sea(Sea) & s__orientation(City, Sea, s__Near)) | (~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass))) <=> ![City: $i] : (?[Sea: $i] : (s__Sea(Sea) & s__orientation(City, Sea, s__Near)) | (~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(14,plain,
% 0.20/0.44 (^[City: $i] : trans(monotonicity(rewrite((is_instance(City, s__CoastalCitiesClass) => ?[Sea: $i] : (s__Sea(Sea) & s__orientation(City, Sea, s__Near))) <=> ((~is_instance(City, s__CoastalCitiesClass)) | ?[Sea: $i] : (s__Sea(Sea) & s__orientation(City, Sea, s__Near)))), ((s__City(City) => (is_instance(City, s__CoastalCitiesClass) => ?[Sea: $i] : (s__Sea(Sea) & s__orientation(City, Sea, s__Near)))) <=> (s__City(City) => ((~is_instance(City, s__CoastalCitiesClass)) | ?[Sea: $i] : (s__Sea(Sea) & s__orientation(City, Sea, s__Near)))))), rewrite((s__City(City) => ((~is_instance(City, s__CoastalCitiesClass)) | ?[Sea: $i] : (s__Sea(Sea) & s__orientation(City, Sea, s__Near)))) <=> (?[Sea: $i] : (s__Sea(Sea) & s__orientation(City, Sea, s__Near)) | (~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)))), ((s__City(City) => (is_instance(City, s__CoastalCitiesClass) => ?[Sea: $i] : (s__Sea(Sea) & s__orientation(City, Sea, s__Near)))) <=> (?[Sea: $i] : (s__Sea(Sea) & s__orientation(City, Sea, s__Near)) | (~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)))))),
% 0.20/0.44 inference(bind,[status(th)],[])).
% 0.20/0.44 tff(15,plain,
% 0.20/0.44 (![City: $i] : (s__City(City) => (is_instance(City, s__CoastalCitiesClass) => ?[Sea: $i] : (s__Sea(Sea) & s__orientation(City, Sea, s__Near)))) <=> ![City: $i] : (?[Sea: $i] : (s__Sea(Sea) & s__orientation(City, Sea, s__Near)) | (~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)))),
% 0.20/0.44 inference(quant_intro,[status(thm)],[14])).
% 0.20/0.44 tff(16,axiom,(![City: $i] : (s__City(City) => (is_instance(City, s__CoastalCitiesClass) => ?[Sea: $i] : (s__Sea(Sea) & s__orientation(City, Sea, s__Near))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','coastal_cities_near_water')).
% 0.20/0.44 tff(17,plain,
% 0.20/0.44 (![City: $i] : (?[Sea: $i] : (s__Sea(Sea) & s__orientation(City, Sea, s__Near)) | (~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[16, 15])).
% 0.20/0.44 tff(18,plain,
% 0.20/0.44 (![City: $i] : (?[Sea: $i] : (s__Sea(Sea) & s__orientation(City, Sea, s__Near)) | (~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[17, 13])).
% 0.20/0.44 tff(19,plain,(
% 0.20/0.44 ![City: $i] : ((s__Sea(tptp_fun_Sea_14(City)) & s__orientation(City, tptp_fun_Sea_14(City), s__Near)) | (~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)))),
% 0.20/0.44 inference(skolemize,[status(sab)],[18])).
% 0.20/0.44 tff(20,plain,
% 0.20/0.44 (![City: $i] : ((~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)) | (s__Sea(tptp_fun_Sea_14(City)) & s__orientation(City, tptp_fun_Sea_14(City), s__Near)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[19, 12])).
% 0.20/0.44 tff(21,plain,
% 0.20/0.44 (![City: $i] : ((~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)) | (~((~s__Sea(tptp_fun_Sea_14(City))) | (~s__orientation(City, tptp_fun_Sea_14(City), s__Near)))))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[20, 10])).
% 0.20/0.44 tff(22,plain,
% 0.20/0.44 (![City: $i] : ((~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)) | (~((~s__Sea(tptp_fun_Sea_14(City))) | (~s__orientation(City, tptp_fun_Sea_14(City), s__Near)))))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[21, 8])).
% 0.20/0.44 tff(23,plain,
% 0.20/0.44 (((~![City: $i] : ((~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)) | (~((~s__Sea(tptp_fun_Sea_14(City))) | (~s__orientation(City, tptp_fun_Sea_14(City), s__Near)))))) | ((~s__City(s__Copenhagen)) | (~is_instance(s__Copenhagen, s__CoastalCitiesClass)) | (~((~s__Sea(tptp_fun_Sea_14(s__Copenhagen))) | (~s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near)))))) <=> ((~![City: $i] : ((~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)) | (~((~s__Sea(tptp_fun_Sea_14(City))) | (~s__orientation(City, tptp_fun_Sea_14(City), s__Near)))))) | (~s__City(s__Copenhagen)) | (~is_instance(s__Copenhagen, s__CoastalCitiesClass)) | (~((~s__Sea(tptp_fun_Sea_14(s__Copenhagen))) | (~s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near)))))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(24,plain,
% 0.20/0.44 ((~![City: $i] : ((~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)) | (~((~s__Sea(tptp_fun_Sea_14(City))) | (~s__orientation(City, tptp_fun_Sea_14(City), s__Near)))))) | ((~s__City(s__Copenhagen)) | (~is_instance(s__Copenhagen, s__CoastalCitiesClass)) | (~((~s__Sea(tptp_fun_Sea_14(s__Copenhagen))) | (~s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near)))))),
% 0.20/0.44 inference(quant_inst,[status(thm)],[])).
% 0.20/0.44 tff(25,plain,
% 0.20/0.44 ((~![City: $i] : ((~s__City(City)) | (~is_instance(City, s__CoastalCitiesClass)) | (~((~s__Sea(tptp_fun_Sea_14(City))) | (~s__orientation(City, tptp_fun_Sea_14(City), s__Near)))))) | (~s__City(s__Copenhagen)) | (~is_instance(s__Copenhagen, s__CoastalCitiesClass)) | (~((~s__Sea(tptp_fun_Sea_14(s__Copenhagen))) | (~s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near))))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[24, 23])).
% 0.20/0.44 tff(26,plain,
% 0.20/0.44 (~((~s__Sea(tptp_fun_Sea_14(s__Copenhagen))) | (~s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near)))),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[25, 22, 6, 3])).
% 0.20/0.44 tff(27,plain,
% 0.20/0.44 (((~s__Sea(tptp_fun_Sea_14(s__Copenhagen))) | (~s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near))) | s__Sea(tptp_fun_Sea_14(s__Copenhagen))),
% 0.20/0.44 inference(tautology,[status(thm)],[])).
% 0.20/0.44 tff(28,plain,
% 0.20/0.44 (s__Sea(tptp_fun_Sea_14(s__Copenhagen))),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[27, 26])).
% 0.20/0.45 tff(29,plain,
% 0.20/0.45 (^[A: $i] : refl((s__BodyOfWater(A) | (~s__Sea(A))) <=> (s__BodyOfWater(A) | (~s__Sea(A))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(30,plain,
% 0.20/0.45 (![A: $i] : (s__BodyOfWater(A) | (~s__Sea(A))) <=> ![A: $i] : (s__BodyOfWater(A) | (~s__Sea(A)))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[29])).
% 0.20/0.45 tff(31,plain,
% 0.20/0.45 (![A: $i] : (s__BodyOfWater(A) | (~s__Sea(A))) <=> ![A: $i] : (s__BodyOfWater(A) | (~s__Sea(A)))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(32,plain,
% 0.20/0.45 (^[A: $i] : rewrite((s__Sea(A) => s__BodyOfWater(A)) <=> (s__BodyOfWater(A) | (~s__Sea(A))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(33,plain,
% 0.20/0.45 (![A: $i] : (s__Sea(A) => s__BodyOfWater(A)) <=> ![A: $i] : (s__BodyOfWater(A) | (~s__Sea(A)))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[32])).
% 0.20/0.45 tff(34,axiom,(![A: $i] : (s__Sea(A) => s__BodyOfWater(A))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','kb_SUMO_MILO_Domains_9679')).
% 0.20/0.45 tff(35,plain,
% 0.20/0.45 (![A: $i] : (s__BodyOfWater(A) | (~s__Sea(A)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[34, 33])).
% 0.20/0.45 tff(36,plain,
% 0.20/0.45 (![A: $i] : (s__BodyOfWater(A) | (~s__Sea(A)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[35, 31])).
% 0.20/0.45 tff(37,plain,(
% 0.20/0.45 ![A: $i] : (s__BodyOfWater(A) | (~s__Sea(A)))),
% 0.20/0.45 inference(skolemize,[status(sab)],[36])).
% 0.20/0.45 tff(38,plain,
% 0.20/0.45 (![A: $i] : (s__BodyOfWater(A) | (~s__Sea(A)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[37, 30])).
% 0.20/0.45 tff(39,plain,
% 0.20/0.45 (((~![A: $i] : (s__BodyOfWater(A) | (~s__Sea(A)))) | (s__BodyOfWater(tptp_fun_Sea_14(s__Copenhagen)) | (~s__Sea(tptp_fun_Sea_14(s__Copenhagen))))) <=> ((~![A: $i] : (s__BodyOfWater(A) | (~s__Sea(A)))) | s__BodyOfWater(tptp_fun_Sea_14(s__Copenhagen)) | (~s__Sea(tptp_fun_Sea_14(s__Copenhagen))))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(40,plain,
% 0.20/0.45 ((~![A: $i] : (s__BodyOfWater(A) | (~s__Sea(A)))) | (s__BodyOfWater(tptp_fun_Sea_14(s__Copenhagen)) | (~s__Sea(tptp_fun_Sea_14(s__Copenhagen))))),
% 0.20/0.45 inference(quant_inst,[status(thm)],[])).
% 0.20/0.45 tff(41,plain,
% 0.20/0.45 ((~![A: $i] : (s__BodyOfWater(A) | (~s__Sea(A)))) | s__BodyOfWater(tptp_fun_Sea_14(s__Copenhagen)) | (~s__Sea(tptp_fun_Sea_14(s__Copenhagen)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[40, 39])).
% 0.20/0.45 tff(42,plain,
% 0.20/0.45 (s__BodyOfWater(tptp_fun_Sea_14(s__Copenhagen))),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[41, 38, 28])).
% 0.20/0.45 tff(43,plain,
% 0.20/0.45 (^[A: $i] : refl((s__WaterArea(A) | (~s__BodyOfWater(A))) <=> (s__WaterArea(A) | (~s__BodyOfWater(A))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(44,plain,
% 0.20/0.45 (![A: $i] : (s__WaterArea(A) | (~s__BodyOfWater(A))) <=> ![A: $i] : (s__WaterArea(A) | (~s__BodyOfWater(A)))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[43])).
% 0.20/0.45 tff(45,plain,
% 0.20/0.45 (![A: $i] : (s__WaterArea(A) | (~s__BodyOfWater(A))) <=> ![A: $i] : (s__WaterArea(A) | (~s__BodyOfWater(A)))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(46,plain,
% 0.20/0.45 (^[A: $i] : rewrite((s__BodyOfWater(A) => s__WaterArea(A)) <=> (s__WaterArea(A) | (~s__BodyOfWater(A))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(47,plain,
% 0.20/0.45 (![A: $i] : (s__BodyOfWater(A) => s__WaterArea(A)) <=> ![A: $i] : (s__WaterArea(A) | (~s__BodyOfWater(A)))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[46])).
% 0.20/0.45 tff(48,axiom,(![A: $i] : (s__BodyOfWater(A) => s__WaterArea(A))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','kb_SUMO_MILO_Domains_9582')).
% 0.20/0.45 tff(49,plain,
% 0.20/0.45 (![A: $i] : (s__WaterArea(A) | (~s__BodyOfWater(A)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[48, 47])).
% 0.20/0.45 tff(50,plain,
% 0.20/0.45 (![A: $i] : (s__WaterArea(A) | (~s__BodyOfWater(A)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[49, 45])).
% 0.20/0.45 tff(51,plain,(
% 0.20/0.45 ![A: $i] : (s__WaterArea(A) | (~s__BodyOfWater(A)))),
% 0.20/0.45 inference(skolemize,[status(sab)],[50])).
% 0.20/0.45 tff(52,plain,
% 0.20/0.45 (![A: $i] : (s__WaterArea(A) | (~s__BodyOfWater(A)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[51, 44])).
% 0.20/0.45 tff(53,plain,
% 0.20/0.45 (((~![A: $i] : (s__WaterArea(A) | (~s__BodyOfWater(A)))) | (s__WaterArea(tptp_fun_Sea_14(s__Copenhagen)) | (~s__BodyOfWater(tptp_fun_Sea_14(s__Copenhagen))))) <=> ((~![A: $i] : (s__WaterArea(A) | (~s__BodyOfWater(A)))) | s__WaterArea(tptp_fun_Sea_14(s__Copenhagen)) | (~s__BodyOfWater(tptp_fun_Sea_14(s__Copenhagen))))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(54,plain,
% 0.20/0.45 ((~![A: $i] : (s__WaterArea(A) | (~s__BodyOfWater(A)))) | (s__WaterArea(tptp_fun_Sea_14(s__Copenhagen)) | (~s__BodyOfWater(tptp_fun_Sea_14(s__Copenhagen))))),
% 0.20/0.45 inference(quant_inst,[status(thm)],[])).
% 0.20/0.45 tff(55,plain,
% 0.20/0.45 ((~![A: $i] : (s__WaterArea(A) | (~s__BodyOfWater(A)))) | s__WaterArea(tptp_fun_Sea_14(s__Copenhagen)) | (~s__BodyOfWater(tptp_fun_Sea_14(s__Copenhagen)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[54, 53])).
% 0.20/0.45 tff(56,plain,
% 0.20/0.45 (s__WaterArea(tptp_fun_Sea_14(s__Copenhagen))),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[55, 52, 42])).
% 0.20/0.45 tff(57,plain,
% 0.20/0.45 (((~s__Sea(tptp_fun_Sea_14(s__Copenhagen))) | (~s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near))) | s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near)),
% 0.20/0.45 inference(tautology,[status(thm)],[])).
% 0.20/0.45 tff(58,plain,
% 0.20/0.45 (s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near)),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[57, 26])).
% 0.20/0.45 tff(59,plain,
% 0.20/0.45 (^[W: $i, C: $i] : refl((s__capability(s__Flooding__t, s__located__m, C) | (~s__City(C)) | (~s__orientation(C, W, s__Near)) | (~s__WaterArea(W))) <=> (s__capability(s__Flooding__t, s__located__m, C) | (~s__City(C)) | (~s__orientation(C, W, s__Near)) | (~s__WaterArea(W))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(60,plain,
% 0.20/0.45 (![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__City(C)) | (~s__orientation(C, W, s__Near)) | (~s__WaterArea(W))) <=> ![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__City(C)) | (~s__orientation(C, W, s__Near)) | (~s__WaterArea(W)))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[59])).
% 0.20/0.45 tff(61,plain,
% 0.20/0.45 (^[W: $i, C: $i] : trans(monotonicity(trans(monotonicity(rewrite((s__WaterArea(W) & s__City(C)) <=> (~((~s__City(C)) | (~s__WaterArea(W))))), ((~(s__WaterArea(W) & s__City(C))) <=> (~(~((~s__City(C)) | (~s__WaterArea(W))))))), rewrite((~(~((~s__City(C)) | (~s__WaterArea(W))))) <=> ((~s__City(C)) | (~s__WaterArea(W)))), ((~(s__WaterArea(W) & s__City(C))) <=> ((~s__City(C)) | (~s__WaterArea(W))))), ((s__capability(s__Flooding__t, s__located__m, C) | (~s__orientation(C, W, s__Near)) | (~(s__WaterArea(W) & s__City(C)))) <=> (s__capability(s__Flooding__t, s__located__m, C) | (~s__orientation(C, W, s__Near)) | ((~s__City(C)) | (~s__WaterArea(W)))))), rewrite((s__capability(s__Flooding__t, s__located__m, C) | (~s__orientation(C, W, s__Near)) | ((~s__City(C)) | (~s__WaterArea(W)))) <=> (s__capability(s__Flooding__t, s__located__m, C) | (~s__City(C)) | (~s__orientation(C, W, s__Near)) | (~s__WaterArea(W)))), ((s__capability(s__Flooding__t, s__located__m, C) | (~s__orientation(C, W, s__Near)) | (~(s__WaterArea(W) & s__City(C)))) <=> (s__capability(s__Flooding__t, s__located__m, C) | (~s__City(C)) | (~s__orientation(C, W, s__Near)) | (~s__WaterArea(W)))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(62,plain,
% 0.20/0.45 (![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__orientation(C, W, s__Near)) | (~(s__WaterArea(W) & s__City(C)))) <=> ![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__City(C)) | (~s__orientation(C, W, s__Near)) | (~s__WaterArea(W)))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[61])).
% 0.20/0.45 tff(63,plain,
% 0.20/0.45 (![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__orientation(C, W, s__Near)) | (~(s__WaterArea(W) & s__City(C)))) <=> ![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__orientation(C, W, s__Near)) | (~(s__WaterArea(W) & s__City(C))))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(64,plain,
% 0.20/0.45 (^[W: $i, C: $i] : trans(monotonicity(rewrite((s__orientation(C, W, s__Near) => s__capability(s__Flooding__t, s__located__m, C)) <=> ((~s__orientation(C, W, s__Near)) | s__capability(s__Flooding__t, s__located__m, C))), (((s__WaterArea(W) & s__City(C)) => (s__orientation(C, W, s__Near) => s__capability(s__Flooding__t, s__located__m, C))) <=> ((s__WaterArea(W) & s__City(C)) => ((~s__orientation(C, W, s__Near)) | s__capability(s__Flooding__t, s__located__m, C))))), rewrite(((s__WaterArea(W) & s__City(C)) => ((~s__orientation(C, W, s__Near)) | s__capability(s__Flooding__t, s__located__m, C))) <=> (s__capability(s__Flooding__t, s__located__m, C) | (~s__orientation(C, W, s__Near)) | (~(s__WaterArea(W) & s__City(C))))), (((s__WaterArea(W) & s__City(C)) => (s__orientation(C, W, s__Near) => s__capability(s__Flooding__t, s__located__m, C))) <=> (s__capability(s__Flooding__t, s__located__m, C) | (~s__orientation(C, W, s__Near)) | (~(s__WaterArea(W) & s__City(C))))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(65,plain,
% 0.20/0.45 (![W: $i, C: $i] : ((s__WaterArea(W) & s__City(C)) => (s__orientation(C, W, s__Near) => s__capability(s__Flooding__t, s__located__m, C))) <=> ![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__orientation(C, W, s__Near)) | (~(s__WaterArea(W) & s__City(C))))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[64])).
% 0.20/0.45 tff(66,axiom,(![W: $i, C: $i] : ((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')).
% 0.20/0.45 tff(67,plain,
% 0.20/0.45 (![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__orientation(C, W, s__Near)) | (~(s__WaterArea(W) & s__City(C))))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[66, 65])).
% 0.20/0.45 tff(68,plain,
% 0.20/0.45 (![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__orientation(C, W, s__Near)) | (~(s__WaterArea(W) & s__City(C))))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[67, 63])).
% 0.20/0.45 tff(69,plain,(
% 0.20/0.45 ![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__orientation(C, W, s__Near)) | (~(s__WaterArea(W) & s__City(C))))),
% 0.20/0.45 inference(skolemize,[status(sab)],[68])).
% 0.20/0.45 tff(70,plain,
% 0.20/0.45 (![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__City(C)) | (~s__orientation(C, W, s__Near)) | (~s__WaterArea(W)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[69, 62])).
% 0.20/0.45 tff(71,plain,
% 0.20/0.45 (![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__City(C)) | (~s__orientation(C, W, s__Near)) | (~s__WaterArea(W)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[70, 60])).
% 0.20/0.45 tff(72,plain,
% 0.20/0.45 (((~![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__City(C)) | (~s__orientation(C, W, s__Near)) | (~s__WaterArea(W)))) | ((~s__City(s__Copenhagen)) | (~s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near)) | s__capability(s__Flooding__t, s__located__m, s__Copenhagen) | (~s__WaterArea(tptp_fun_Sea_14(s__Copenhagen))))) <=> ((~![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__City(C)) | (~s__orientation(C, W, s__Near)) | (~s__WaterArea(W)))) | (~s__City(s__Copenhagen)) | (~s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near)) | s__capability(s__Flooding__t, s__located__m, s__Copenhagen) | (~s__WaterArea(tptp_fun_Sea_14(s__Copenhagen))))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(73,plain,
% 0.20/0.45 ((s__capability(s__Flooding__t, s__located__m, s__Copenhagen) | (~s__City(s__Copenhagen)) | (~s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near)) | (~s__WaterArea(tptp_fun_Sea_14(s__Copenhagen)))) <=> ((~s__City(s__Copenhagen)) | (~s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near)) | s__capability(s__Flooding__t, s__located__m, s__Copenhagen) | (~s__WaterArea(tptp_fun_Sea_14(s__Copenhagen))))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(74,plain,
% 0.20/0.45 (((~![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__City(C)) | (~s__orientation(C, W, s__Near)) | (~s__WaterArea(W)))) | (s__capability(s__Flooding__t, s__located__m, s__Copenhagen) | (~s__City(s__Copenhagen)) | (~s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near)) | (~s__WaterArea(tptp_fun_Sea_14(s__Copenhagen))))) <=> ((~![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__City(C)) | (~s__orientation(C, W, s__Near)) | (~s__WaterArea(W)))) | ((~s__City(s__Copenhagen)) | (~s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near)) | s__capability(s__Flooding__t, s__located__m, s__Copenhagen) | (~s__WaterArea(tptp_fun_Sea_14(s__Copenhagen)))))),
% 0.20/0.45 inference(monotonicity,[status(thm)],[73])).
% 0.20/0.45 tff(75,plain,
% 0.20/0.45 (((~![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__City(C)) | (~s__orientation(C, W, s__Near)) | (~s__WaterArea(W)))) | (s__capability(s__Flooding__t, s__located__m, s__Copenhagen) | (~s__City(s__Copenhagen)) | (~s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near)) | (~s__WaterArea(tptp_fun_Sea_14(s__Copenhagen))))) <=> ((~![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__City(C)) | (~s__orientation(C, W, s__Near)) | (~s__WaterArea(W)))) | (~s__City(s__Copenhagen)) | (~s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near)) | s__capability(s__Flooding__t, s__located__m, s__Copenhagen) | (~s__WaterArea(tptp_fun_Sea_14(s__Copenhagen))))),
% 0.20/0.45 inference(transitivity,[status(thm)],[74, 72])).
% 0.20/0.45 tff(76,plain,
% 0.20/0.45 ((~![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__City(C)) | (~s__orientation(C, W, s__Near)) | (~s__WaterArea(W)))) | (s__capability(s__Flooding__t, s__located__m, s__Copenhagen) | (~s__City(s__Copenhagen)) | (~s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near)) | (~s__WaterArea(tptp_fun_Sea_14(s__Copenhagen))))),
% 0.20/0.45 inference(quant_inst,[status(thm)],[])).
% 0.20/0.45 tff(77,plain,
% 0.20/0.45 ((~![W: $i, C: $i] : (s__capability(s__Flooding__t, s__located__m, C) | (~s__City(C)) | (~s__orientation(C, W, s__Near)) | (~s__WaterArea(W)))) | (~s__City(s__Copenhagen)) | (~s__orientation(s__Copenhagen, tptp_fun_Sea_14(s__Copenhagen), s__Near)) | s__capability(s__Flooding__t, s__located__m, s__Copenhagen) | (~s__WaterArea(tptp_fun_Sea_14(s__Copenhagen)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[76, 75])).
% 0.20/0.45 tff(78,plain,
% 0.20/0.45 (s__capability(s__Flooding__t, s__located__m, s__Copenhagen) | (~s__WaterArea(tptp_fun_Sea_14(s__Copenhagen)))),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[77, 71, 3, 58])).
% 0.20/0.45 tff(79,plain,
% 0.20/0.45 (s__capability(s__Flooding__t, s__located__m, s__Copenhagen)),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[78, 56])).
% 0.20/0.45 tff(80,plain,
% 0.20/0.45 (s__Nation(s__Denmark) <=> s__Nation(s__Denmark)),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(81,axiom,(s__Nation(s__Denmark)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','s__Denmark_type')).
% 0.20/0.45 tff(82,plain,
% 0.20/0.45 (s__Nation(s__Denmark)),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[81, 80])).
% 0.20/0.45 tff(83,plain,
% 0.20/0.45 (^[A: $i] : refl((s__GeopoliticalArea(A) | (~s__Nation(A))) <=> (s__GeopoliticalArea(A) | (~s__Nation(A))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(84,plain,
% 0.20/0.45 (![A: $i] : (s__GeopoliticalArea(A) | (~s__Nation(A))) <=> ![A: $i] : (s__GeopoliticalArea(A) | (~s__Nation(A)))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[83])).
% 0.20/0.45 tff(85,plain,
% 0.20/0.45 (![A: $i] : (s__GeopoliticalArea(A) | (~s__Nation(A))) <=> ![A: $i] : (s__GeopoliticalArea(A) | (~s__Nation(A)))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(86,plain,
% 0.20/0.45 (^[A: $i] : rewrite((s__Nation(A) => s__GeopoliticalArea(A)) <=> (s__GeopoliticalArea(A) | (~s__Nation(A))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(87,plain,
% 0.20/0.45 (![A: $i] : (s__Nation(A) => s__GeopoliticalArea(A)) <=> ![A: $i] : (s__GeopoliticalArea(A) | (~s__Nation(A)))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[86])).
% 0.20/0.45 tff(88,axiom,(![A: $i] : (s__Nation(A) => s__GeopoliticalArea(A))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','kb_SUMO_MILO_6428')).
% 0.20/0.45 tff(89,plain,
% 0.20/0.45 (![A: $i] : (s__GeopoliticalArea(A) | (~s__Nation(A)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[88, 87])).
% 0.20/0.45 tff(90,plain,
% 0.20/0.45 (![A: $i] : (s__GeopoliticalArea(A) | (~s__Nation(A)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[89, 85])).
% 0.20/0.45 tff(91,plain,(
% 0.20/0.45 ![A: $i] : (s__GeopoliticalArea(A) | (~s__Nation(A)))),
% 0.20/0.45 inference(skolemize,[status(sab)],[90])).
% 0.20/0.45 tff(92,plain,
% 0.20/0.45 (![A: $i] : (s__GeopoliticalArea(A) | (~s__Nation(A)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[91, 84])).
% 0.20/0.45 tff(93,plain,
% 0.20/0.45 (((~![A: $i] : (s__GeopoliticalArea(A) | (~s__Nation(A)))) | (s__GeopoliticalArea(s__Denmark) | (~s__Nation(s__Denmark)))) <=> ((~![A: $i] : (s__GeopoliticalArea(A) | (~s__Nation(A)))) | s__GeopoliticalArea(s__Denmark) | (~s__Nation(s__Denmark)))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(94,plain,
% 0.20/0.45 ((~![A: $i] : (s__GeopoliticalArea(A) | (~s__Nation(A)))) | (s__GeopoliticalArea(s__Denmark) | (~s__Nation(s__Denmark)))),
% 0.20/0.45 inference(quant_inst,[status(thm)],[])).
% 0.20/0.45 tff(95,plain,
% 0.20/0.45 ((~![A: $i] : (s__GeopoliticalArea(A) | (~s__Nation(A)))) | s__GeopoliticalArea(s__Denmark) | (~s__Nation(s__Denmark))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[94, 93])).
% 0.20/0.45 tff(96,plain,
% 0.20/0.45 (s__GeopoliticalArea(s__Denmark)),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[95, 92, 82])).
% 0.20/0.45 tff(97,plain,
% 0.20/0.45 (^[A: $i] : refl((s__GeographicArea(A) | (~s__GeopoliticalArea(A))) <=> (s__GeographicArea(A) | (~s__GeopoliticalArea(A))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(98,plain,
% 0.20/0.45 (![A: $i] : (s__GeographicArea(A) | (~s__GeopoliticalArea(A))) <=> ![A: $i] : (s__GeographicArea(A) | (~s__GeopoliticalArea(A)))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[97])).
% 0.20/0.45 tff(99,plain,
% 0.20/0.45 (![A: $i] : (s__GeographicArea(A) | (~s__GeopoliticalArea(A))) <=> ![A: $i] : (s__GeographicArea(A) | (~s__GeopoliticalArea(A)))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(100,plain,
% 0.20/0.45 (^[A: $i] : rewrite((s__GeopoliticalArea(A) => s__GeographicArea(A)) <=> (s__GeographicArea(A) | (~s__GeopoliticalArea(A))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(101,plain,
% 0.20/0.45 (![A: $i] : (s__GeopoliticalArea(A) => s__GeographicArea(A)) <=> ![A: $i] : (s__GeographicArea(A) | (~s__GeopoliticalArea(A)))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[100])).
% 0.20/0.45 tff(102,axiom,(![A: $i] : (s__GeopoliticalArea(A) => s__GeographicArea(A))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','kb_SUMO_MILO_6345')).
% 0.20/0.45 tff(103,plain,
% 0.20/0.45 (![A: $i] : (s__GeographicArea(A) | (~s__GeopoliticalArea(A)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[102, 101])).
% 0.20/0.45 tff(104,plain,
% 0.20/0.45 (![A: $i] : (s__GeographicArea(A) | (~s__GeopoliticalArea(A)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[103, 99])).
% 0.20/0.45 tff(105,plain,(
% 0.20/0.45 ![A: $i] : (s__GeographicArea(A) | (~s__GeopoliticalArea(A)))),
% 0.20/0.45 inference(skolemize,[status(sab)],[104])).
% 0.20/0.45 tff(106,plain,
% 0.20/0.45 (![A: $i] : (s__GeographicArea(A) | (~s__GeopoliticalArea(A)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[105, 98])).
% 0.20/0.45 tff(107,plain,
% 0.20/0.45 (((~![A: $i] : (s__GeographicArea(A) | (~s__GeopoliticalArea(A)))) | (s__GeographicArea(s__Denmark) | (~s__GeopoliticalArea(s__Denmark)))) <=> ((~![A: $i] : (s__GeographicArea(A) | (~s__GeopoliticalArea(A)))) | s__GeographicArea(s__Denmark) | (~s__GeopoliticalArea(s__Denmark)))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(108,plain,
% 0.20/0.45 ((~![A: $i] : (s__GeographicArea(A) | (~s__GeopoliticalArea(A)))) | (s__GeographicArea(s__Denmark) | (~s__GeopoliticalArea(s__Denmark)))),
% 0.20/0.45 inference(quant_inst,[status(thm)],[])).
% 0.20/0.45 tff(109,plain,
% 0.20/0.45 ((~![A: $i] : (s__GeographicArea(A) | (~s__GeopoliticalArea(A)))) | s__GeographicArea(s__Denmark) | (~s__GeopoliticalArea(s__Denmark))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[108, 107])).
% 0.20/0.45 tff(110,plain,
% 0.20/0.45 (s__GeographicArea(s__Denmark)),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[109, 106, 96])).
% 0.20/0.45 tff(111,plain,
% 0.20/0.45 (^[A: $i] : refl((s__Region(A) | (~s__GeographicArea(A))) <=> (s__Region(A) | (~s__GeographicArea(A))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(112,plain,
% 0.20/0.45 (![A: $i] : (s__Region(A) | (~s__GeographicArea(A))) <=> ![A: $i] : (s__Region(A) | (~s__GeographicArea(A)))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[111])).
% 0.20/0.45 tff(113,plain,
% 0.20/0.45 (![A: $i] : (s__Region(A) | (~s__GeographicArea(A))) <=> ![A: $i] : (s__Region(A) | (~s__GeographicArea(A)))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(114,plain,
% 0.20/0.45 (^[A: $i] : rewrite((s__GeographicArea(A) => s__Region(A)) <=> (s__Region(A) | (~s__GeographicArea(A))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(115,plain,
% 0.20/0.45 (![A: $i] : (s__GeographicArea(A) => s__Region(A)) <=> ![A: $i] : (s__Region(A) | (~s__GeographicArea(A)))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[114])).
% 0.20/0.45 tff(116,axiom,(![A: $i] : (s__GeographicArea(A) => s__Region(A))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','kb_SUMO_MILO_6365')).
% 0.20/0.45 tff(117,plain,
% 0.20/0.45 (![A: $i] : (s__Region(A) | (~s__GeographicArea(A)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[116, 115])).
% 0.20/0.45 tff(118,plain,
% 0.20/0.45 (![A: $i] : (s__Region(A) | (~s__GeographicArea(A)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[117, 113])).
% 0.20/0.45 tff(119,plain,(
% 0.20/0.45 ![A: $i] : (s__Region(A) | (~s__GeographicArea(A)))),
% 0.20/0.45 inference(skolemize,[status(sab)],[118])).
% 0.20/0.45 tff(120,plain,
% 0.20/0.45 (![A: $i] : (s__Region(A) | (~s__GeographicArea(A)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[119, 112])).
% 0.20/0.45 tff(121,plain,
% 0.20/0.45 (((~![A: $i] : (s__Region(A) | (~s__GeographicArea(A)))) | (s__Region(s__Denmark) | (~s__GeographicArea(s__Denmark)))) <=> ((~![A: $i] : (s__Region(A) | (~s__GeographicArea(A)))) | s__Region(s__Denmark) | (~s__GeographicArea(s__Denmark)))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(122,plain,
% 0.20/0.46 ((~![A: $i] : (s__Region(A) | (~s__GeographicArea(A)))) | (s__Region(s__Denmark) | (~s__GeographicArea(s__Denmark)))),
% 0.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.46 tff(123,plain,
% 0.20/0.46 ((~![A: $i] : (s__Region(A) | (~s__GeographicArea(A)))) | s__Region(s__Denmark) | (~s__GeographicArea(s__Denmark))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[122, 121])).
% 0.20/0.46 tff(124,plain,
% 0.20/0.46 (s__Region(s__Denmark)),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[123, 120, 110])).
% 0.20/0.46 tff(125,plain,
% 0.20/0.46 (^[A: $i] : refl((s__Object(A) | (~s__Region(A))) <=> (s__Object(A) | (~s__Region(A))))),
% 0.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(126,plain,
% 0.20/0.46 (![A: $i] : (s__Object(A) | (~s__Region(A))) <=> ![A: $i] : (s__Object(A) | (~s__Region(A)))),
% 0.20/0.46 inference(quant_intro,[status(thm)],[125])).
% 0.20/0.46 tff(127,plain,
% 0.20/0.46 (![A: $i] : (s__Object(A) | (~s__Region(A))) <=> ![A: $i] : (s__Object(A) | (~s__Region(A)))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(128,plain,
% 0.20/0.46 (^[A: $i] : rewrite((s__Region(A) => s__Object(A)) <=> (s__Object(A) | (~s__Region(A))))),
% 0.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(129,plain,
% 0.20/0.46 (![A: $i] : (s__Region(A) => s__Object(A)) <=> ![A: $i] : (s__Object(A) | (~s__Region(A)))),
% 0.20/0.46 inference(quant_intro,[status(thm)],[128])).
% 0.20/0.46 tff(130,axiom,(![A: $i] : (s__Region(A) => s__Object(A))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','kb_SUMO_MILO_701')).
% 0.20/0.46 tff(131,plain,
% 0.20/0.46 (![A: $i] : (s__Object(A) | (~s__Region(A)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[130, 129])).
% 0.20/0.46 tff(132,plain,
% 0.20/0.46 (![A: $i] : (s__Object(A) | (~s__Region(A)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[131, 127])).
% 0.20/0.46 tff(133,plain,(
% 0.20/0.46 ![A: $i] : (s__Object(A) | (~s__Region(A)))),
% 0.20/0.46 inference(skolemize,[status(sab)],[132])).
% 0.20/0.46 tff(134,plain,
% 0.20/0.46 (![A: $i] : (s__Object(A) | (~s__Region(A)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[133, 126])).
% 0.20/0.46 tff(135,plain,
% 0.20/0.46 (((~![A: $i] : (s__Object(A) | (~s__Region(A)))) | (s__Object(s__Denmark) | (~s__Region(s__Denmark)))) <=> ((~![A: $i] : (s__Object(A) | (~s__Region(A)))) | s__Object(s__Denmark) | (~s__Region(s__Denmark)))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(136,plain,
% 0.20/0.46 ((~![A: $i] : (s__Object(A) | (~s__Region(A)))) | (s__Object(s__Denmark) | (~s__Region(s__Denmark)))),
% 0.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.46 tff(137,plain,
% 0.20/0.46 ((~![A: $i] : (s__Object(A) | (~s__Region(A)))) | s__Object(s__Denmark) | (~s__Region(s__Denmark))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[136, 135])).
% 0.20/0.46 tff(138,plain,
% 0.20/0.46 (s__Object(s__Denmark)),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[137, 134, 124])).
% 0.20/0.46 tff(139,plain,
% 0.20/0.46 (^[A: $i] : refl((s__GeopoliticalArea(A) | (~s__City(A))) <=> (s__GeopoliticalArea(A) | (~s__City(A))))),
% 0.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(140,plain,
% 0.20/0.46 (![A: $i] : (s__GeopoliticalArea(A) | (~s__City(A))) <=> ![A: $i] : (s__GeopoliticalArea(A) | (~s__City(A)))),
% 0.20/0.46 inference(quant_intro,[status(thm)],[139])).
% 0.20/0.46 tff(141,plain,
% 0.20/0.46 (![A: $i] : (s__GeopoliticalArea(A) | (~s__City(A))) <=> ![A: $i] : (s__GeopoliticalArea(A) | (~s__City(A)))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(142,plain,
% 0.20/0.46 (^[A: $i] : rewrite((s__City(A) => s__GeopoliticalArea(A)) <=> (s__GeopoliticalArea(A) | (~s__City(A))))),
% 0.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(143,plain,
% 0.20/0.46 (![A: $i] : (s__City(A) => s__GeopoliticalArea(A)) <=> ![A: $i] : (s__GeopoliticalArea(A) | (~s__City(A)))),
% 0.20/0.46 inference(quant_intro,[status(thm)],[142])).
% 0.20/0.46 tff(144,axiom,(![A: $i] : (s__City(A) => s__GeopoliticalArea(A))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','kb_SUMO_MILO_6437')).
% 0.20/0.46 tff(145,plain,
% 0.20/0.46 (![A: $i] : (s__GeopoliticalArea(A) | (~s__City(A)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[144, 143])).
% 0.20/0.46 tff(146,plain,
% 0.20/0.46 (![A: $i] : (s__GeopoliticalArea(A) | (~s__City(A)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[145, 141])).
% 0.20/0.46 tff(147,plain,(
% 0.20/0.46 ![A: $i] : (s__GeopoliticalArea(A) | (~s__City(A)))),
% 0.20/0.46 inference(skolemize,[status(sab)],[146])).
% 0.20/0.46 tff(148,plain,
% 0.20/0.46 (![A: $i] : (s__GeopoliticalArea(A) | (~s__City(A)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[147, 140])).
% 0.20/0.46 tff(149,plain,
% 0.20/0.46 (((~![A: $i] : (s__GeopoliticalArea(A) | (~s__City(A)))) | (s__GeopoliticalArea(s__Copenhagen) | (~s__City(s__Copenhagen)))) <=> ((~![A: $i] : (s__GeopoliticalArea(A) | (~s__City(A)))) | s__GeopoliticalArea(s__Copenhagen) | (~s__City(s__Copenhagen)))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(150,plain,
% 0.20/0.46 ((~![A: $i] : (s__GeopoliticalArea(A) | (~s__City(A)))) | (s__GeopoliticalArea(s__Copenhagen) | (~s__City(s__Copenhagen)))),
% 0.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.46 tff(151,plain,
% 0.20/0.46 ((~![A: $i] : (s__GeopoliticalArea(A) | (~s__City(A)))) | s__GeopoliticalArea(s__Copenhagen) | (~s__City(s__Copenhagen))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[150, 149])).
% 0.20/0.46 tff(152,plain,
% 0.20/0.46 (s__GeopoliticalArea(s__Copenhagen)),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[151, 148, 3])).
% 0.20/0.46 tff(153,plain,
% 0.20/0.46 (((~![A: $i] : (s__GeographicArea(A) | (~s__GeopoliticalArea(A)))) | (s__GeographicArea(s__Copenhagen) | (~s__GeopoliticalArea(s__Copenhagen)))) <=> ((~![A: $i] : (s__GeographicArea(A) | (~s__GeopoliticalArea(A)))) | s__GeographicArea(s__Copenhagen) | (~s__GeopoliticalArea(s__Copenhagen)))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(154,plain,
% 0.20/0.46 ((~![A: $i] : (s__GeographicArea(A) | (~s__GeopoliticalArea(A)))) | (s__GeographicArea(s__Copenhagen) | (~s__GeopoliticalArea(s__Copenhagen)))),
% 0.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.46 tff(155,plain,
% 0.20/0.46 ((~![A: $i] : (s__GeographicArea(A) | (~s__GeopoliticalArea(A)))) | s__GeographicArea(s__Copenhagen) | (~s__GeopoliticalArea(s__Copenhagen))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[154, 153])).
% 0.20/0.46 tff(156,plain,
% 0.20/0.46 (s__GeographicArea(s__Copenhagen)),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[155, 106, 152])).
% 0.20/0.46 tff(157,plain,
% 0.20/0.46 (((~![A: $i] : (s__Region(A) | (~s__GeographicArea(A)))) | (s__Region(s__Copenhagen) | (~s__GeographicArea(s__Copenhagen)))) <=> ((~![A: $i] : (s__Region(A) | (~s__GeographicArea(A)))) | s__Region(s__Copenhagen) | (~s__GeographicArea(s__Copenhagen)))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(158,plain,
% 0.20/0.46 ((~![A: $i] : (s__Region(A) | (~s__GeographicArea(A)))) | (s__Region(s__Copenhagen) | (~s__GeographicArea(s__Copenhagen)))),
% 0.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.46 tff(159,plain,
% 0.20/0.46 ((~![A: $i] : (s__Region(A) | (~s__GeographicArea(A)))) | s__Region(s__Copenhagen) | (~s__GeographicArea(s__Copenhagen))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[158, 157])).
% 0.20/0.46 tff(160,plain,
% 0.20/0.46 (s__Region(s__Copenhagen)),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[159, 120, 156])).
% 0.20/0.46 tff(161,plain,
% 0.20/0.46 (((~![A: $i] : (s__Object(A) | (~s__Region(A)))) | (s__Object(s__Copenhagen) | (~s__Region(s__Copenhagen)))) <=> ((~![A: $i] : (s__Object(A) | (~s__Region(A)))) | s__Object(s__Copenhagen) | (~s__Region(s__Copenhagen)))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(162,plain,
% 0.20/0.46 ((~![A: $i] : (s__Object(A) | (~s__Region(A)))) | (s__Object(s__Copenhagen) | (~s__Region(s__Copenhagen)))),
% 0.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.46 tff(163,plain,
% 0.20/0.46 ((~![A: $i] : (s__Object(A) | (~s__Region(A)))) | s__Object(s__Copenhagen) | (~s__Region(s__Copenhagen))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[162, 161])).
% 0.20/0.46 tff(164,plain,
% 0.20/0.46 (s__Object(s__Copenhagen)),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[163, 134, 160])).
% 0.20/0.46 tff(165,plain,
% 0.20/0.46 ((to_int(|'55.75695'|) = |'55'|) <=> (to_int(|'55.75695'|) = |'55'|)),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(166,axiom,(to_int(|'55.75695'|) = |'55'|), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''55.75695_55'')).
% 0.20/0.46 tff(167,plain,
% 0.20/0.46 (to_int(|'55.75695'|) = |'55'|),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[166, 165])).
% 0.20/0.46 tff(168,plain,
% 0.20/0.46 (|'55'| = to_int(|'55.75695'|)),
% 0.20/0.46 inference(symmetry,[status(thm)],[167])).
% 0.20/0.46 tff(169,plain,
% 0.20/0.46 ((to_int(|'55.67631'|) = |'55'|) <=> (to_int(|'55.67631'|) = |'55'|)),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(170,axiom,(to_int(|'55.67631'|) = |'55'|), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''55.67631_55'')).
% 0.20/0.46 tff(171,plain,
% 0.20/0.46 (to_int(|'55.67631'|) = |'55'|),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[170, 169])).
% 0.20/0.46 tff(172,plain,
% 0.20/0.46 (to_int(|'55.67631'|) = to_int(|'55.75695'|)),
% 0.20/0.46 inference(transitivity,[status(thm)],[171, 168])).
% 0.20/0.46 tff(173,plain,
% 0.20/0.46 (look_different(s__Copenhagen, s__Moscow) <=> look_different(s__Copenhagen, s__Moscow)),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(174,axiom,(look_different(s__Copenhagen, s__Moscow)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','s__Copenhagen_not_s__Moscow')).
% 0.20/0.46 tff(175,plain,
% 0.20/0.46 (look_different(s__Copenhagen, s__Moscow)),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[174, 173])).
% 0.20/0.46 tff(176,plain,
% 0.20/0.46 (latlong(s__Moscow, |'55.75695'|, |'37.614975'|, moscow, ru) <=> latlong(s__Moscow, |'55.75695'|, |'37.614975'|, moscow, ru)),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(177,axiom,(latlong(s__Moscow, |'55.75695'|, |'37.614975'|, moscow, ru)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','latlong_s__Moscow')).
% 0.20/0.46 tff(178,plain,
% 0.20/0.46 (latlong(s__Moscow, |'55.75695'|, |'37.614975'|, moscow, ru)),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[177, 176])).
% 0.20/0.46 tff(179,plain,
% 0.20/0.46 (s__SymbolicString(ru) <=> s__SymbolicString(ru)),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(180,axiom,(s__SymbolicString(ru)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','ru_type')).
% 0.20/0.46 tff(181,plain,
% 0.20/0.46 (s__SymbolicString(ru)),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[180, 179])).
% 0.20/0.46 tff(182,plain,
% 0.20/0.46 (s__SymbolicString(moscow) <=> s__SymbolicString(moscow)),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(183,axiom,(s__SymbolicString(moscow)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','moscow_type')).
% 0.20/0.46 tff(184,plain,
% 0.20/0.46 (s__SymbolicString(moscow)),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[183, 182])).
% 0.20/0.46 tff(185,plain,
% 0.20/0.46 (real(|'37.614975'|) <=> real(|'37.614975'|)),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(186,axiom,(real(|'37.614975'|)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','moscow_long_type')).
% 0.20/0.46 tff(187,plain,
% 0.20/0.46 (real(|'37.614975'|)),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[186, 185])).
% 0.20/0.46 tff(188,plain,
% 0.20/0.46 (real(|'55.75695'|) <=> real(|'55.75695'|)),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(189,axiom,(real(|'55.75695'|)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','moscow_lat_type')).
% 0.20/0.46 tff(190,plain,
% 0.20/0.46 (real(|'55.75695'|)),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[189, 188])).
% 0.20/0.46 tff(191,plain,
% 0.20/0.46 (latlong(s__Copenhagen, |'55.67631'|, |'12.569355'|, copenhagen, dk) <=> latlong(s__Copenhagen, |'55.67631'|, |'12.569355'|, copenhagen, dk)),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(192,axiom,(latlong(s__Copenhagen, |'55.67631'|, |'12.569355'|, copenhagen, dk)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','latlong_s__Copenhagen')).
% 0.20/0.46 tff(193,plain,
% 0.20/0.46 (latlong(s__Copenhagen, |'55.67631'|, |'12.569355'|, copenhagen, dk)),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[192, 191])).
% 0.20/0.46 tff(194,plain,
% 0.20/0.46 (s__SymbolicString(dk) <=> s__SymbolicString(dk)),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(195,axiom,(s__SymbolicString(dk)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','dk_type')).
% 0.20/0.46 tff(196,plain,
% 0.20/0.46 (s__SymbolicString(dk)),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[195, 194])).
% 0.20/0.46 tff(197,plain,
% 0.20/0.46 (s__SymbolicString(copenhagen) <=> s__SymbolicString(copenhagen)),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(198,axiom,(s__SymbolicString(copenhagen)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','copenhagen_type')).
% 0.20/0.46 tff(199,plain,
% 0.20/0.46 (s__SymbolicString(copenhagen)),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[198, 197])).
% 0.20/0.46 tff(200,plain,
% 0.20/0.46 (real(|'12.569355'|) <=> real(|'12.569355'|)),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(201,axiom,(real(|'12.569355'|)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','copenhagen_long_type')).
% 0.20/0.46 tff(202,plain,
% 0.20/0.46 (real(|'12.569355'|)),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[201, 200])).
% 0.20/0.46 tff(203,plain,
% 0.20/0.46 (real(|'55.67631'|) <=> real(|'55.67631'|)),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(204,axiom,(real(|'55.67631'|)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','copenhagen_lat_type')).
% 0.20/0.46 tff(205,plain,
% 0.20/0.46 (real(|'55.67631'|)),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[204, 203])).
% 0.20/0.46 tff(206,plain,
% 0.20/0.46 (capital_city(s__Copenhagen, s__Denmark) <=> capital_city(s__Copenhagen, s__Denmark)),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(207,axiom,(capital_city(s__Copenhagen, s__Denmark)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','s__Copenhagen_s__Denmark')).
% 0.20/0.46 tff(208,plain,
% 0.20/0.46 (capital_city(s__Copenhagen, s__Denmark)),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[207, 206])).
% 0.20/0.46 tff(209,plain,
% 0.20/0.46 (is_instance(s__Denmark, s__OECDMemberEconomiesClass) <=> is_instance(s__Denmark, s__OECDMemberEconomiesClass)),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(210,axiom,(is_instance(s__Denmark, s__OECDMemberEconomiesClass)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','s__Denmark_OECD')).
% 0.20/0.46 tff(211,plain,
% 0.20/0.46 (is_instance(s__Denmark, s__OECDMemberEconomiesClass)),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[210, 209])).
% 0.20/0.46 tff(212,plain,
% 0.20/0.46 (?[A: $i] : int(A) <=> ?[A: $i] : int(A)),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(213,axiom,(?[A: $i] : int(A)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','int_type')).
% 0.20/0.46 tff(214,plain,
% 0.20/0.46 (?[A: $i] : int(A)),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[213, 212])).
% 0.20/0.46 tff(215,plain,(
% 0.20/0.46 int(A!16)),
% 0.20/0.46 inference(skolemize,[status(sab)],[214])).
% 0.20/0.46 tff(216,plain,
% 0.20/0.46 (^[City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : refl(((~s__SymbolicString(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)) | (~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))) <=> ((~s__SymbolicString(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)) | (~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.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(217,plain,
% 0.20/0.46 (![City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : ((~s__SymbolicString(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)) | (~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))) <=> ![City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : ((~s__SymbolicString(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)) | (~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.20/0.46 inference(quant_intro,[status(thm)],[216])).
% 0.20/0.46 tff(218,plain,
% 0.20/0.46 (^[City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : trans(monotonicity(rewrite((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)) <=> (~((~s__SymbolicString(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)) | (~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))))), ((~(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))) <=> (~(~((~s__SymbolicString(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)) | (~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))))))), rewrite((~(~((~s__SymbolicString(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)) | (~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))))) <=> ((~s__SymbolicString(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)) | (~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)))), ((~(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))) <=> ((~s__SymbolicString(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)) | (~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.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(219,plain,
% 0.20/0.46 (![City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : (~(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))) <=> ![City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : ((~s__SymbolicString(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)) | (~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.20/0.46 inference(quant_intro,[status(thm)],[218])).
% 0.20/0.46 tff(220,plain,
% 0.20/0.46 ((~?[City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : (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))) <=> (~?[City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : (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.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(221,plain,
% 0.20/0.47 ((~?[City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : (((((((((((((((((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))) <=> (~?[City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : (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.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(222,axiom,(~?[City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : (((((((((((((((((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')).
% 0.20/0.47 tff(223,plain,
% 0.20/0.47 (~?[City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : (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.20/0.47 inference(modus_ponens,[status(thm)],[222, 221])).
% 0.20/0.47 tff(224,plain,
% 0.20/0.47 (~?[City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : (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.20/0.47 inference(modus_ponens,[status(thm)],[223, 220])).
% 0.20/0.47 tff(225,plain,
% 0.20/0.47 (~?[City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : (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.20/0.47 inference(modus_ponens,[status(thm)],[224, 220])).
% 0.20/0.47 tff(226,plain,
% 0.20/0.47 (~?[City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : (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.20/0.47 inference(modus_ponens,[status(thm)],[225, 220])).
% 0.20/0.47 tff(227,plain,
% 0.20/0.47 (^[City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : refl($oeq((~(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))), (~(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.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(228,plain,(
% 0.20/0.47 ![City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : (~(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.20/0.47 inference(nnf-neg,[status(sab)],[226, 227])).
% 0.20/0.47 tff(229,plain,
% 0.20/0.47 (![City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : ((~s__SymbolicString(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)) | (~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.20/0.47 inference(modus_ponens,[status(thm)],[228, 219])).
% 0.20/0.47 tff(230,plain,
% 0.20/0.47 (![City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : ((~s__SymbolicString(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)) | (~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.20/0.47 inference(modus_ponens,[status(thm)],[229, 217])).
% 0.20/0.47 tff(231,plain,
% 0.20/0.47 (((~![City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : ((~s__SymbolicString(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)) | (~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)))) | ((~s__SymbolicString(ru)) | (~int(A!16)) | (~real(|'55.75695'|)) | (~real(|'37.614975'|)) | (~s__SymbolicString(moscow)) | (~latlong(s__Moscow, |'55.75695'|, |'37.614975'|, moscow, ru)) | (~s__Object(s__Copenhagen)) | (~s__Object(s__Denmark)) | (~real(|'55.67631'|)) | (~real(|'12.569355'|)) | (~s__SymbolicString(copenhagen)) | (~s__SymbolicString(dk)) | (~is_instance(s__Denmark, s__OECDMemberEconomiesClass)) | (~capital_city(s__Copenhagen, s__Denmark)) | (~look_different(s__Copenhagen, s__Moscow)) | (~latlong(s__Copenhagen, |'55.67631'|, |'12.569355'|, copenhagen, dk)) | (~(to_int(|'55.67631'|) = to_int(|'55.75695'|))) | (~s__capability(s__Flooding__t, s__located__m, s__Copenhagen)))) <=> ((~![City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : ((~s__SymbolicString(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)) | (~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)))) | (~s__SymbolicString(ru)) | (~int(A!16)) | (~real(|'55.75695'|)) | (~real(|'37.614975'|)) | (~s__SymbolicString(moscow)) | (~latlong(s__Moscow, |'55.75695'|, |'37.614975'|, moscow, ru)) | (~s__Object(s__Copenhagen)) | (~s__Object(s__Denmark)) | (~real(|'55.67631'|)) | (~real(|'12.569355'|)) | (~s__SymbolicString(copenhagen)) | (~s__SymbolicString(dk)) | (~is_instance(s__Denmark, s__OECDMemberEconomiesClass)) | (~capital_city(s__Copenhagen, s__Denmark)) | (~look_different(s__Copenhagen, s__Moscow)) | (~latlong(s__Copenhagen, |'55.67631'|, |'12.569355'|, copenhagen, dk)) | (~(to_int(|'55.67631'|) = to_int(|'55.75695'|))) | (~s__capability(s__Flooding__t, s__located__m, s__Copenhagen)))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(232,plain,
% 0.20/0.47 (((~s__SymbolicString(ru)) | (~s__Object(s__Copenhagen)) | (~s__Object(s__Denmark)) | (~real(|'55.67631'|)) | (~real(|'12.569355'|)) | (~s__SymbolicString(copenhagen)) | (~s__SymbolicString(dk)) | (~int(A!16)) | (~real(|'55.75695'|)) | (~real(|'37.614975'|)) | (~s__SymbolicString(moscow)) | (~is_instance(s__Denmark, s__OECDMemberEconomiesClass)) | (~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)) | (~(to_int(|'55.67631'|) = to_int(|'55.75695'|))) | (~s__capability(s__Flooding__t, s__located__m, s__Copenhagen))) <=> ((~s__SymbolicString(ru)) | (~int(A!16)) | (~real(|'55.75695'|)) | (~real(|'37.614975'|)) | (~s__SymbolicString(moscow)) | (~latlong(s__Moscow, |'55.75695'|, |'37.614975'|, moscow, ru)) | (~s__Object(s__Copenhagen)) | (~s__Object(s__Denmark)) | (~real(|'55.67631'|)) | (~real(|'12.569355'|)) | (~s__SymbolicString(copenhagen)) | (~s__SymbolicString(dk)) | (~is_instance(s__Denmark, s__OECDMemberEconomiesClass)) | (~capital_city(s__Copenhagen, s__Denmark)) | (~look_different(s__Copenhagen, s__Moscow)) | (~latlong(s__Copenhagen, |'55.67631'|, |'12.569355'|, copenhagen, dk)) | (~(to_int(|'55.67631'|) = to_int(|'55.75695'|))) | (~s__capability(s__Flooding__t, s__located__m, s__Copenhagen)))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(233,plain,
% 0.20/0.47 (((~![City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : ((~s__SymbolicString(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)) | (~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)))) | ((~s__SymbolicString(ru)) | (~s__Object(s__Copenhagen)) | (~s__Object(s__Denmark)) | (~real(|'55.67631'|)) | (~real(|'12.569355'|)) | (~s__SymbolicString(copenhagen)) | (~s__SymbolicString(dk)) | (~int(A!16)) | (~real(|'55.75695'|)) | (~real(|'37.614975'|)) | (~s__SymbolicString(moscow)) | (~is_instance(s__Denmark, s__OECDMemberEconomiesClass)) | (~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)) | (~(to_int(|'55.67631'|) = to_int(|'55.75695'|))) | (~s__capability(s__Flooding__t, s__located__m, s__Copenhagen)))) <=> ((~![City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : ((~s__SymbolicString(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)) | (~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)))) | ((~s__SymbolicString(ru)) | (~int(A!16)) | (~real(|'55.75695'|)) | (~real(|'37.614975'|)) | (~s__SymbolicString(moscow)) | (~latlong(s__Moscow, |'55.75695'|, |'37.614975'|, moscow, ru)) | (~s__Object(s__Copenhagen)) | (~s__Object(s__Denmark)) | (~real(|'55.67631'|)) | (~real(|'12.569355'|)) | (~s__SymbolicString(copenhagen)) | (~s__SymbolicString(dk)) | (~is_instance(s__Denmark, s__OECDMemberEconomiesClass)) | (~capital_city(s__Copenhagen, s__Denmark)) | (~look_different(s__Copenhagen, s__Moscow)) | (~latlong(s__Copenhagen, |'55.67631'|, |'12.569355'|, copenhagen, dk)) | (~(to_int(|'55.67631'|) = to_int(|'55.75695'|))) | (~s__capability(s__Flooding__t, s__located__m, s__Copenhagen))))),
% 0.20/0.47 inference(monotonicity,[status(thm)],[232])).
% 0.20/0.47 tff(234,plain,
% 0.20/0.47 (((~![City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : ((~s__SymbolicString(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)) | (~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)))) | ((~s__SymbolicString(ru)) | (~s__Object(s__Copenhagen)) | (~s__Object(s__Denmark)) | (~real(|'55.67631'|)) | (~real(|'12.569355'|)) | (~s__SymbolicString(copenhagen)) | (~s__SymbolicString(dk)) | (~int(A!16)) | (~real(|'55.75695'|)) | (~real(|'37.614975'|)) | (~s__SymbolicString(moscow)) | (~is_instance(s__Denmark, s__OECDMemberEconomiesClass)) | (~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)) | (~(to_int(|'55.67631'|) = to_int(|'55.75695'|))) | (~s__capability(s__Flooding__t, s__located__m, s__Copenhagen)))) <=> ((~![City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : ((~s__SymbolicString(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)) | (~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)))) | (~s__SymbolicString(ru)) | (~int(A!16)) | (~real(|'55.75695'|)) | (~real(|'37.614975'|)) | (~s__SymbolicString(moscow)) | (~latlong(s__Moscow, |'55.75695'|, |'37.614975'|, moscow, ru)) | (~s__Object(s__Copenhagen)) | (~s__Object(s__Denmark)) | (~real(|'55.67631'|)) | (~real(|'12.569355'|)) | (~s__SymbolicString(copenhagen)) | (~s__SymbolicString(dk)) | (~is_instance(s__Denmark, s__OECDMemberEconomiesClass)) | (~capital_city(s__Copenhagen, s__Denmark)) | (~look_different(s__Copenhagen, s__Moscow)) | (~latlong(s__Copenhagen, |'55.67631'|, |'12.569355'|, copenhagen, dk)) | (~(to_int(|'55.67631'|) = to_int(|'55.75695'|))) | (~s__capability(s__Flooding__t, s__located__m, s__Copenhagen)))),
% 0.20/0.48 inference(transitivity,[status(thm)],[233, 231])).
% 0.20/0.48 tff(235,plain,
% 0.20/0.48 ((~![City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : ((~s__SymbolicString(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)) | (~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)))) | ((~s__SymbolicString(ru)) | (~s__Object(s__Copenhagen)) | (~s__Object(s__Denmark)) | (~real(|'55.67631'|)) | (~real(|'12.569355'|)) | (~s__SymbolicString(copenhagen)) | (~s__SymbolicString(dk)) | (~int(A!16)) | (~real(|'55.75695'|)) | (~real(|'37.614975'|)) | (~s__SymbolicString(moscow)) | (~is_instance(s__Denmark, s__OECDMemberEconomiesClass)) | (~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)) | (~(to_int(|'55.67631'|) = to_int(|'55.75695'|))) | (~s__capability(s__Flooding__t, s__located__m, s__Copenhagen)))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(236,plain,
% 0.20/0.48 ((~![City: $i, Nation: $i, CityLat: $i, CityLong: $i, CityName: $i, CityNation: $i, Latitude: $i, MoscowLat: $i, MoscowLong: $i, MoscowName: $i, MoscowNation: $i] : ((~s__SymbolicString(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)) | (~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)))) | (~s__SymbolicString(ru)) | (~int(A!16)) | (~real(|'55.75695'|)) | (~real(|'37.614975'|)) | (~s__SymbolicString(moscow)) | (~latlong(s__Moscow, |'55.75695'|, |'37.614975'|, moscow, ru)) | (~s__Object(s__Copenhagen)) | (~s__Object(s__Denmark)) | (~real(|'55.67631'|)) | (~real(|'12.569355'|)) | (~s__SymbolicString(copenhagen)) | (~s__SymbolicString(dk)) | (~is_instance(s__Denmark, s__OECDMemberEconomiesClass)) | (~capital_city(s__Copenhagen, s__Denmark)) | (~look_different(s__Copenhagen, s__Moscow)) | (~latlong(s__Copenhagen, |'55.67631'|, |'12.569355'|, copenhagen, dk)) | (~(to_int(|'55.67631'|) = to_int(|'55.75695'|))) | (~s__capability(s__Flooding__t, s__located__m, s__Copenhagen))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[235, 234])).
% 0.20/0.48 tff(237,plain,
% 0.20/0.48 ((~s__Object(s__Copenhagen)) | (~s__Object(s__Denmark)) | (~s__capability(s__Flooding__t, s__located__m, s__Copenhagen))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[236, 230, 215, 211, 208, 205, 202, 199, 196, 193, 190, 187, 184, 181, 178, 175, 172])).
% 0.20/0.48 tff(238,plain,
% 0.20/0.48 ($false),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[237, 164, 138, 79])).
% 0.20/0.48 % SZS output end Proof
% 0.20/0.49 % E exiting
%------------------------------------------------------------------------------