%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : CSR117+1 : TPTP v8.1.2. Released v4.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Aug 30 21:38:10 EDT 2023 % Result : Theorem 104.51s 16.76s % Output : Proof 104.98s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : CSR117+1 : TPTP v8.1.2. Released v4.1.0. % 0.07/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.35 % Computer : n017.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Mon Aug 28 13:42:42 EDT 2023 % 0.13/0.35 % CPUTime : % 0.20/0.61 ________ _____ % 0.20/0.61 ___ __ \_________(_)________________________________ % 0.20/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.61 % 0.20/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.61 (2023-06-19) % 0.20/0.61 % 0.20/0.61 (c) Philipp Rümmer, 2009-2023 % 0.20/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.61 Amanda Stjerna. % 0.20/0.61 Free software under BSD-3-Clause. % 0.20/0.61 % 0.20/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.61 % 0.20/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.20/0.63 Running up to 7 provers in parallel. % 0.20/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 4.07/1.33 Prover 1: Preprocessing ... % 4.07/1.33 Prover 4: Preprocessing ... % 4.69/1.37 Prover 2: Preprocessing ... % 4.69/1.37 Prover 5: Preprocessing ... % 4.69/1.37 Prover 3: Preprocessing ... % 4.69/1.37 Prover 6: Preprocessing ... % 4.69/1.37 Prover 0: Preprocessing ... % 9.61/2.03 Prover 5: Constructing countermodel ... % 9.78/2.10 Prover 2: Proving ... % 12.53/2.44 Prover 6: Proving ... % 12.53/2.46 Prover 3: Constructing countermodel ... % 12.88/2.60 Prover 1: Constructing countermodel ... % 14.94/2.79 Prover 0: Proving ... % 15.46/2.85 Prover 4: Constructing countermodel ... % 20.85/3.58 Prover 3: gave up % 20.85/3.59 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 22.12/3.74 Prover 7: Preprocessing ... % 24.60/4.10 Prover 7: Constructing countermodel ... % 27.39/4.53 Prover 1: gave up % 27.39/4.54 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 29.82/4.80 Prover 8: Preprocessing ... % 34.38/5.39 Prover 8: Warning: ignoring some quantifiers % 34.38/5.42 Prover 8: Constructing countermodel ... % 48.77/7.22 Prover 8: gave up % 48.77/7.25 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 49.83/7.43 Prover 9: Preprocessing ... % 54.29/8.00 Prover 9: Constructing countermodel ... % 90.32/12.64 Prover 2: stopped % 90.32/12.64 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 92.19/12.87 Prover 10: Preprocessing ... % 93.58/13.05 Prover 10: Constructing countermodel ... % 97.76/13.54 Prover 10: Found proof (size 39) % 97.76/13.54 Prover 10: proved (898ms) % 97.76/13.54 Prover 0: stopped % 97.76/13.54 Prover 9: stopped % 97.76/13.57 Prover 6: stopped % 98.65/13.71 Prover 7: stopped % 99.18/13.77 Prover 5: stopped % 104.51/16.75 Prover 4: stopped % 104.51/16.75 % 104.51/16.76 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 104.51/16.76 % 104.51/16.77 % SZS output start Proof for theBenchmark % 104.51/16.78 Assumptions after simplification: % 104.51/16.78 --------------------------------- % 104.51/16.78 % 104.51/16.78 (-35.306541_-35) % 104.66/16.82 to_int(-35.306541) = -35 & $i(-35) & $i(-35.306541) % 104.66/16.82 % 104.66/16.82 (-35_type) % 104.66/16.82 $i(-35) & int(-35) % 104.66/16.82 % 104.66/16.82 (55.67631_55) % 104.66/16.82 to_int(55.67631) = 55 & $i(55) & $i(55.67631) % 104.66/16.82 % 104.66/16.82 (55.75695_55) % 104.66/16.83 to_int(55.75695) = 55 & $i(55) & $i(55.75695) % 104.66/16.83 % 104.66/16.83 (coastal_cities_near_water) % 104.66/16.83 $i(s__CoastalCitiesClass) & $i(s__Near) & ! [v0: $i] : ( ~ $i(v0) | ~ % 104.66/16.83 is_instance(v0, s__CoastalCitiesClass) | ~ s__City(v0) | ? [v1: $i] : % 104.66/16.83 ($i(v1) & s__orientation(v0, v1, s__Near) & s__Sea(v1))) % 104.66/16.83 % 104.66/16.83 (copenhagen_coastal) % 104.66/16.83 $i(s__Copenhagen) & $i(s__CoastalCitiesClass) & is_instance(s__Copenhagen, % 104.66/16.83 s__CoastalCitiesClass) % 104.66/16.83 % 104.66/16.83 (copenhagen_lat_type) % 104.66/16.83 $i(55.67631) & real(55.67631) % 104.66/16.83 % 104.66/16.83 (copenhagen_long_type) % 104.66/16.83 $i(12.569355) & real(12.569355) % 104.66/16.83 % 104.66/16.83 (copenhagen_type) % 104.66/16.83 $i(copenhagen) & s__SymbolicString(copenhagen) % 104.66/16.83 % 104.66/16.83 (dk_type) % 104.66/16.83 $i(dk) & s__SymbolicString(dk) % 104.66/16.83 % 104.66/16.83 (flood_near_water) % 104.66/16.83 $i(s__located__m) & $i(s__Flooding__t) & $i(s__Near) & ! [v0: $i] : ! [v1: % 104.66/16.83 $i] : ( ~ $i(v1) | ~ $i(v0) | ~ s__orientation(v1, v0, s__Near) | ~ % 104.66/16.83 s__WaterArea(v0) | ~ s__City(v1) | s__capability(s__Flooding__t, % 104.66/16.83 s__located__m, v1)) % 104.66/16.83 % 104.66/16.84 (kb_SUMO_MILO_6345) % 104.66/16.84 ! [v0: $i] : ( ~ $i(v0) | ~ s__GeopoliticalArea(v0) | s__GeographicArea(v0)) % 104.66/16.84 % 104.66/16.84 (kb_SUMO_MILO_6365) % 104.66/16.84 ! [v0: $i] : ( ~ $i(v0) | ~ s__GeographicArea(v0) | s__Region(v0)) % 104.66/16.84 % 104.66/16.84 (kb_SUMO_MILO_6428) % 104.66/16.84 ! [v0: $i] : ( ~ $i(v0) | ~ s__Nation(v0) | s__GeopoliticalArea(v0)) % 104.66/16.84 % 104.66/16.84 (kb_SUMO_MILO_6437) % 104.66/16.84 ! [v0: $i] : ( ~ $i(v0) | ~ s__City(v0) | s__GeopoliticalArea(v0)) % 104.66/16.84 % 104.66/16.84 (kb_SUMO_MILO_701) % 104.66/16.84 ! [v0: $i] : ( ~ $i(v0) | ~ s__Region(v0) | s__Object(v0)) % 104.66/16.84 % 104.66/16.84 (kb_SUMO_MILO_Domains_9582) % 104.66/16.84 ! [v0: $i] : ( ~ $i(v0) | ~ s__BodyOfWater(v0) | s__WaterArea(v0)) % 104.66/16.84 % 104.66/16.84 (kb_SUMO_MILO_Domains_9679) % 104.66/16.84 ! [v0: $i] : ( ~ $i(v0) | ~ s__Sea(v0) | s__BodyOfWater(v0)) % 104.66/16.84 % 104.66/16.84 (latlong_s__Copenhagen) % 104.66/16.84 $i(dk) & $i(copenhagen) & $i(12.569355) & $i(55.67631) & $i(s__Copenhagen) & % 104.66/16.84 latlong(s__Copenhagen, 55.67631, 12.569355, copenhagen, dk) % 104.66/16.84 % 104.66/16.84 (latlong_s__Moscow) % 104.66/16.84 $i(ru) & $i(moscow) & $i(37.614975) & $i(55.75695) & $i(s__Moscow) & % 104.66/16.84 latlong(s__Moscow, 55.75695, 37.614975, moscow, ru) % 104.66/16.84 % 104.66/16.85 (moscow_lat_type) % 104.66/16.85 $i(55.75695) & real(55.75695) % 104.66/16.85 % 104.66/16.85 (moscow_long_type) % 104.66/16.85 $i(37.614975) & real(37.614975) % 104.66/16.85 % 104.66/16.85 (moscow_type) % 104.66/16.85 $i(moscow) & s__SymbolicString(moscow) % 104.66/16.85 % 104.66/16.85 (ru_type) % 104.66/16.85 $i(ru) & s__SymbolicString(ru) % 104.66/16.85 % 104.66/16.85 (s__Copenhagen_not_s__Moscow) % 104.66/16.85 $i(s__Copenhagen) & $i(s__Moscow) & look_different(s__Copenhagen, s__Moscow) % 104.66/16.85 % 104.66/16.85 (s__Copenhagen_s__Denmark) % 104.66/16.85 $i(s__Denmark) & $i(s__Copenhagen) & capital_city(s__Copenhagen, s__Denmark) % 104.66/16.85 % 104.66/16.85 (s__Copenhagen_type) % 104.66/16.85 $i(s__Copenhagen) & s__City(s__Copenhagen) % 104.66/16.85 % 104.66/16.85 (s__Denmark_OECD) % 104.66/16.85 $i(s__Denmark) & $i(s__OECDMemberEconomiesClass) & is_instance(s__Denmark, % 104.66/16.85 s__OECDMemberEconomiesClass) % 104.66/16.85 % 104.66/16.85 (s__Denmark_type) % 104.66/16.85 $i(s__Denmark) & s__Nation(s__Denmark) % 104.66/16.85 % 104.66/16.85 (where) % 104.66/16.86 $i(s__Moscow) & $i(s__OECDMemberEconomiesClass) & $i(s__located__m) & % 104.66/16.86 $i(s__Flooding__t) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 104.66/16.86 ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: % 104.66/16.86 $i] : ! [v10: $i] : ! [v11: $i] : ( ~ (to_int(v7) = v11) | ~ (to_int(v2) % 104.66/16.86 = v11) | ~ $i(v10) | ~ $i(v9) | ~ $i(v8) | ~ $i(v7) | ~ $i(v6) | ~ % 104.66/16.86 $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 104.66/16.86 latlong(v0, v2, v3, v4, v5) | ~ latlong(s__Moscow, v7, v8, v9, v10) | ~ % 104.66/16.86 look_different(v0, s__Moscow) | ~ capital_city(v0, v1) | ~ int(v6) | ~ % 104.66/16.86 real(v8) | ~ real(v7) | ~ real(v3) | ~ real(v2) | ~ % 104.66/16.86 s__capability(s__Flooding__t, s__located__m, v0) | ~ is_instance(v1, % 104.66/16.86 s__OECDMemberEconomiesClass) | ~ s__SymbolicString(v10) | ~ % 104.66/16.86 s__SymbolicString(v9) | ~ s__SymbolicString(v5) | ~ s__SymbolicString(v4) % 104.66/16.86 | ~ s__Object(v1) | ~ s__Object(v0)) % 104.66/16.86 % 104.66/16.86 Further assumptions not needed in the proof: % 104.66/16.86 -------------------------------------------- % 104.66/16.86 37.557121_37, 37.97615_37, 37_type, 38.725679_38, 38_type, 47.506225_47, % 104.66/16.86 47_type, 48.149245_48, 48.202548_48, 48.856925_48, 48_type, 49.609531_49, % 104.66/16.86 49_type, 50.079083_50, 50.848385_50, 50_type, 52.23537_52, 52.516074_52, % 104.66/16.86 52_type, 55_type, 60.17116_60, 60_type, at_type, athens_lat_type, % 104.66/16.86 athens_long_type, athens_type, au_type, be_type, berlin_lat_type, % 104.66/16.86 berlin_long_type, berlin_type, bratislava_lat_type, bratislava_long_type, % 104.66/16.86 bratislava_type, brussels_lat_type, brussels_long_type, brussels_type, % 104.66/16.86 budapest_lat_type, budapest_long_type, budapest_type, canberra_lat_type, % 104.66/16.86 canberra_long_type, canberra_type, coastal_cities_type, cz_type, de_type, % 104.66/16.86 fi_type, fr_type, gr_type, helsinki_lat_type, helsinki_long_type, helsinki_type, % 104.66/16.86 hu_type, int_not_real, int_not_s__CaseRole, int_not_s__Entity, % 104.66/16.86 int_not_s__Object, int_not_s__PositionalAttribute, int_not_s__SetOrClass, % 104.66/16.86 int_not_s__SymbolicString, int_type, kb_SUMO_MILO_12059, kb_SUMO_MILO_6391, % 104.66/16.86 kb_SUMO_MILO_7458, kb_SUMO_MILO_7487, kr_type, latlong_s__Athens, % 104.66/16.86 latlong_s__Berlin, latlong_s__Bratislava, latlong_s__Brussels, % 104.66/16.86 latlong_s__Budapest, latlong_s__Canberra, latlong_s__Helsinki, % 104.66/16.86 latlong_s__Lisbon, latlong_s__Luxembourg_City, latlong_s__Paris, % 104.66/16.86 latlong_s__Prague, latlong_s__Seoul, latlong_s__Vienna, latlong_s__Warsaw, % 104.66/16.86 lisbon_lat_type, lisbon_long_type, lisbon_type, lu_type, % 104.66/16.86 luxembourg_city_lat_type, luxembourg_city_long_type, luxembourg_city_type, % 104.66/16.86 oecd_type, paris_lat_type, paris_long_type, paris_type, pl_type, % 104.66/16.86 prague_lat_type, prague_long_type, prague_type, pt_type, real_not_s__CaseRole, % 104.66/16.86 real_not_s__Entity, real_not_s__Object, real_not_s__PositionalAttribute, % 104.66/16.86 real_not_s__SetOrClass, real_not_s__SymbolicString, real_type, % 104.66/16.86 s__Athens_not_s__Moscow, s__Athens_s__Greece, s__Athens_type, s__Australia_OECD, % 104.66/16.86 s__Australia_type, s__Austria_OECD, s__Austria_type, s__Belgium_OECD, % 104.66/16.86 s__Belgium_type, s__Berlin_not_s__Moscow, s__Berlin_s__Germany, s__Berlin_type, % 104.66/16.86 s__BodyOfWater_type, s__Bratislava_not_s__Moscow, s__Bratislava_s__Slovakia, % 104.66/16.86 s__Bratislava_type, s__Brussels_not_s__Moscow, s__Brussels_s__Belgium, % 104.66/16.86 s__Brussels_type, s__Budapest_not_s__Moscow, s__Budapest_s__Hungary, % 104.66/16.86 s__Budapest_type, s__Canberra_not_s__Moscow, s__Canberra_s__Australia, % 104.66/16.86 s__Canberra_type, s__CaseRole_not_s__Entity, s__CaseRole_not_s__Object, % 104.66/16.86 s__CaseRole_not_s__PositionalAttribute, s__CaseRole_not_s__SetOrClass, % 104.66/16.86 s__CaseRole_type, s__City_type, s__CzechRepublic_OECD, s__CzechRepublic_type, % 104.66/16.86 s__Entity_not_s__SetOrClass, s__Entity_type, s__Finland_OECD, s__Finland_type, % 104.66/16.86 s__France_OECD, s__France_type, s__GeographicArea_type, % 104.66/16.86 s__GeopoliticalArea_not_s__WaterArea, s__Germany_OECD, s__Germany_type, % 104.66/16.86 s__Greece_OECD, s__Greece_type, s__Helsinki_not_s__Moscow, % 104.66/16.86 s__Helsinki_s__Finland, s__Helsinki_type, s__Hungary_OECD, s__Hungary_type, % 104.66/16.86 s__Iceland_OECD, s__Iceland_type, s__Italy_OECD, s__Italy_type, % 104.66/16.86 s__Lisbon_not_s__Moscow, s__Lisbon_s__Portugal, s__Lisbon_type, % 104.66/16.86 s__Luxembourg_City_not_s__Moscow, s__Luxembourg_City_s__Luxembourg, % 104.66/16.86 s__Luxembourg_City_type, s__Luxembourg_OECD, s__Luxembourg_type, s__Mexico_OECD, % 104.66/16.86 s__Mexico_type, s__Moscow_type, s__Nation_not_s__City, s__Nation_type, % 104.66/16.86 s__Netherlands_OECD, s__Netherlands_type, s__NewZealand_OECD, % 104.66/16.86 s__NewZealand_type, s__Norway_OECD, s__Norway_type, s__Object_not_s__Entity, % 104.66/16.86 s__Object_not_s__SetOrClass, s__Object_type, s__Paris_not_s__Moscow, % 104.66/16.86 s__Paris_s__France, s__Paris_type, s__Poland_OECD, s__Poland_type, % 104.66/16.86 s__Portugal_OECD, s__Portugal_type, s__PositionalAttribute_not_s__Entity, % 104.66/16.86 s__PositionalAttribute_not_s__Object, s__PositionalAttribute_not_s__SetOrClass, % 104.66/16.86 s__PositionalAttribute_type, s__Prague_not_s__Moscow, % 104.66/16.86 s__Prague_s__CzechRepublic, s__Prague_type, s__Region_type, s__Sea_type, % 104.66/16.86 s__Seoul_not_s__Moscow, s__Seoul_s__SouthKorea, s__Seoul_type, % 104.66/16.86 s__SetOrClass_type, s__Slovakia_OECD, s__Slovakia_type, s__SouthKorea_OECD, % 104.66/16.86 s__SouthKorea_type, s__Spain_OECD, s__Spain_type, s__Sweden_OECD, % 104.66/16.86 s__Sweden_type, s__Switzerland_OECD, s__Switzerland_type, % 104.66/16.86 s__SymbolicString_not_s__CaseRole, s__SymbolicString_not_s__Entity, % 104.66/16.86 s__SymbolicString_not_s__Object, s__SymbolicString_not_s__PositionalAttribute, % 104.66/16.86 s__SymbolicString_not_s__SetOrClass, s__SymbolicString_type, % 104.66/16.86 s__SymmetricPositionalAttribute_type, s__UnitedKingdom_OECD, % 104.66/16.86 s__UnitedKingdom_type, s__UnitedStates_OECD, s__UnitedStates_type, % 104.66/16.86 s__Vienna_not_s__Moscow, s__Vienna_s__Austria, s__Vienna_type, % 104.66/16.86 s__Warsaw_not_s__Moscow, s__Warsaw_s__Poland, s__Warsaw_type, s__WaterArea_type, % 104.66/16.86 s__located__m_type, seoul_lat_type, seoul_long_type, seoul_type, sk_type, % 104.66/16.86 to_int_type, vienna_lat_type, vienna_long_type, vienna_type, warsaw_lat_type, % 104.66/16.86 warsaw_long_type, warsaw_type % 104.66/16.86 % 104.66/16.86 Those formulas are unsatisfiable: % 104.66/16.86 --------------------------------- % 104.66/16.86 % 104.66/16.86 Begin of proof % 104.66/16.87 | % 104.66/16.87 | ALPHA: (coastal_cities_near_water) implies: % 104.66/16.87 | (1) ! [v0: $i] : ( ~ $i(v0) | ~ is_instance(v0, s__CoastalCitiesClass) | % 104.66/16.87 | ~ s__City(v0) | ? [v1: $i] : ($i(v1) & s__orientation(v0, v1, % 104.66/16.87 | s__Near) & s__Sea(v1))) % 104.66/16.87 | % 104.66/16.87 | ALPHA: (flood_near_water) implies: % 104.66/16.87 | (2) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 104.66/16.87 | s__orientation(v1, v0, s__Near) | ~ s__WaterArea(v0) | ~ % 104.66/16.87 | s__City(v1) | s__capability(s__Flooding__t, s__located__m, v1)) % 104.66/16.87 | % 104.66/16.87 | ALPHA: (copenhagen_coastal) implies: % 104.66/16.87 | (3) is_instance(s__Copenhagen, s__CoastalCitiesClass) % 104.66/16.87 | % 104.66/16.87 | ALPHA: (s__Denmark_type) implies: % 104.66/16.87 | (4) s__Nation(s__Denmark) % 104.66/16.87 | % 104.66/16.87 | ALPHA: (s__Denmark_OECD) implies: % 104.66/16.87 | (5) is_instance(s__Denmark, s__OECDMemberEconomiesClass) % 104.66/16.87 | % 104.66/16.87 | ALPHA: (s__Copenhagen_type) implies: % 104.98/16.87 | (6) s__City(s__Copenhagen) % 104.98/16.87 | % 104.98/16.87 | ALPHA: (s__Copenhagen_s__Denmark) implies: % 104.98/16.88 | (7) capital_city(s__Copenhagen, s__Denmark) % 104.98/16.88 | (8) $i(s__Denmark) % 104.98/16.88 | % 104.98/16.88 | ALPHA: (copenhagen_lat_type) implies: % 104.98/16.88 | (9) real(55.67631) % 104.98/16.88 | % 104.98/16.88 | ALPHA: (copenhagen_long_type) implies: % 104.98/16.88 | (10) real(12.569355) % 104.98/16.88 | % 104.98/16.88 | ALPHA: (copenhagen_type) implies: % 104.98/16.88 | (11) s__SymbolicString(copenhagen) % 104.98/16.88 | % 104.98/16.88 | ALPHA: (dk_type) implies: % 104.98/16.88 | (12) s__SymbolicString(dk) % 104.98/16.88 | % 104.98/16.88 | ALPHA: (latlong_s__Copenhagen) implies: % 104.98/16.88 | (13) latlong(s__Copenhagen, 55.67631, 12.569355, copenhagen, dk) % 104.98/16.88 | (14) $i(12.569355) % 104.98/16.88 | (15) $i(copenhagen) % 104.98/16.88 | (16) $i(dk) % 104.98/16.88 | % 104.98/16.88 | ALPHA: (moscow_lat_type) implies: % 104.98/16.88 | (17) real(55.75695) % 104.98/16.88 | % 104.98/16.88 | ALPHA: (moscow_long_type) implies: % 104.98/16.88 | (18) real(37.614975) % 104.98/16.88 | % 104.98/16.88 | ALPHA: (moscow_type) implies: % 104.98/16.88 | (19) s__SymbolicString(moscow) % 104.98/16.88 | % 104.98/16.88 | ALPHA: (ru_type) implies: % 104.98/16.88 | (20) s__SymbolicString(ru) % 104.98/16.88 | % 104.98/16.88 | ALPHA: (latlong_s__Moscow) implies: % 104.98/16.88 | (21) latlong(s__Moscow, 55.75695, 37.614975, moscow, ru) % 104.98/16.88 | (22) $i(37.614975) % 104.98/16.88 | (23) $i(moscow) % 104.98/16.88 | (24) $i(ru) % 104.98/16.88 | % 104.98/16.88 | ALPHA: (s__Copenhagen_not_s__Moscow) implies: % 104.98/16.88 | (25) look_different(s__Copenhagen, s__Moscow) % 104.98/16.88 | (26) $i(s__Copenhagen) % 104.98/16.88 | % 104.98/16.88 | ALPHA: (-35_type) implies: % 104.98/16.88 | (27) int(-35) % 104.98/16.88 | % 104.98/16.88 | ALPHA: (-35.306541_-35) implies: % 104.98/16.88 | (28) $i(-35) % 104.98/16.88 | % 104.98/16.88 | ALPHA: (55.67631_55) implies: % 104.98/16.88 | (29) $i(55.67631) % 104.98/16.88 | (30) to_int(55.67631) = 55 % 104.98/16.88 | % 104.98/16.88 | ALPHA: (55.75695_55) implies: % 104.98/16.88 | (31) $i(55.75695) % 104.98/16.88 | (32) to_int(55.75695) = 55 % 104.98/16.88 | % 104.98/16.88 | ALPHA: (where) implies: % 104.98/16.89 | (33) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 104.98/16.89 | ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : % 104.98/16.89 | ! [v10: $i] : ! [v11: $i] : ( ~ (to_int(v7) = v11) | ~ (to_int(v2) = % 104.98/16.89 | v11) | ~ $i(v10) | ~ $i(v9) | ~ $i(v8) | ~ $i(v7) | ~ $i(v6) % 104.98/16.89 | | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 104.98/16.89 | $i(v0) | ~ latlong(v0, v2, v3, v4, v5) | ~ latlong(s__Moscow, v7, % 104.98/16.89 | v8, v9, v10) | ~ look_different(v0, s__Moscow) | ~ % 104.98/16.89 | capital_city(v0, v1) | ~ int(v6) | ~ real(v8) | ~ real(v7) | ~ % 104.98/16.89 | real(v3) | ~ real(v2) | ~ s__capability(s__Flooding__t, % 104.98/16.89 | s__located__m, v0) | ~ is_instance(v1, % 104.98/16.89 | s__OECDMemberEconomiesClass) | ~ s__SymbolicString(v10) | ~ % 104.98/16.89 | s__SymbolicString(v9) | ~ s__SymbolicString(v5) | ~ % 104.98/16.89 | s__SymbolicString(v4) | ~ s__Object(v1) | ~ s__Object(v0)) % 104.98/16.89 | % 104.98/16.89 | GROUND_INST: instantiating (kb_SUMO_MILO_6428) with s__Denmark, simplifying % 104.98/16.89 | with (4), (8) gives: % 104.98/16.89 | (34) s__GeopoliticalArea(s__Denmark) % 104.98/16.89 | % 104.98/16.89 | GROUND_INST: instantiating (kb_SUMO_MILO_6437) with s__Copenhagen, simplifying % 104.98/16.89 | with (6), (26) gives: % 104.98/16.89 | (35) s__GeopoliticalArea(s__Copenhagen) % 104.98/16.89 | % 104.98/16.89 | GROUND_INST: instantiating (1) with s__Copenhagen, simplifying with (3), (6), % 104.98/16.89 | (26) gives: % 104.98/16.89 | (36) ? [v0: $i] : ($i(v0) & s__orientation(s__Copenhagen, v0, s__Near) & % 104.98/16.89 | s__Sea(v0)) % 104.98/16.89 | % 104.98/16.89 | DELTA: instantiating (36) with fresh symbol all_85_0 gives: % 104.98/16.89 | (37) $i(all_85_0) & s__orientation(s__Copenhagen, all_85_0, s__Near) & % 104.98/16.89 | s__Sea(all_85_0) % 104.98/16.89 | % 104.98/16.89 | ALPHA: (37) implies: % 104.98/16.89 | (38) s__Sea(all_85_0) % 104.98/16.89 | (39) s__orientation(s__Copenhagen, all_85_0, s__Near) % 104.98/16.89 | (40) $i(all_85_0) % 104.98/16.89 | % 104.98/16.89 | GROUND_INST: instantiating (kb_SUMO_MILO_6345) with s__Copenhagen, simplifying % 104.98/16.89 | with (26), (35) gives: % 104.98/16.89 | (41) s__GeographicArea(s__Copenhagen) % 104.98/16.89 | % 104.98/16.89 | GROUND_INST: instantiating (kb_SUMO_MILO_6345) with s__Denmark, simplifying % 104.98/16.89 | with (8), (34) gives: % 104.98/16.89 | (42) s__GeographicArea(s__Denmark) % 104.98/16.89 | % 104.98/16.89 | GROUND_INST: instantiating (kb_SUMO_MILO_Domains_9679) with all_85_0, % 104.98/16.89 | simplifying with (38), (40) gives: % 104.98/16.89 | (43) s__BodyOfWater(all_85_0) % 104.98/16.89 | % 104.98/16.89 | GROUND_INST: instantiating (kb_SUMO_MILO_Domains_9582) with all_85_0, % 104.98/16.89 | simplifying with (40), (43) gives: % 104.98/16.89 | (44) s__WaterArea(all_85_0) % 104.98/16.89 | % 104.98/16.89 | GROUND_INST: instantiating (kb_SUMO_MILO_6365) with s__Copenhagen, simplifying % 104.98/16.89 | with (26), (41) gives: % 104.98/16.89 | (45) s__Region(s__Copenhagen) % 104.98/16.90 | % 104.98/16.90 | GROUND_INST: instantiating (kb_SUMO_MILO_6365) with s__Denmark, simplifying % 104.98/16.90 | with (8), (42) gives: % 104.98/16.90 | (46) s__Region(s__Denmark) % 104.98/16.90 | % 104.98/16.90 | GROUND_INST: instantiating (kb_SUMO_MILO_701) with s__Copenhagen, simplifying % 104.98/16.90 | with (26), (45) gives: % 104.98/16.90 | (47) s__Object(s__Copenhagen) % 104.98/16.90 | % 104.98/16.90 | GROUND_INST: instantiating (kb_SUMO_MILO_701) with s__Denmark, simplifying % 104.98/16.90 | with (8), (46) gives: % 104.98/16.90 | (48) s__Object(s__Denmark) % 104.98/16.90 | % 104.98/16.90 | GROUND_INST: instantiating (2) with all_85_0, s__Copenhagen, simplifying with % 104.98/16.90 | (6), (26), (39), (40), (44) gives: % 104.98/16.90 | (49) s__capability(s__Flooding__t, s__located__m, s__Copenhagen) % 104.98/16.90 | % 104.98/16.90 | GROUND_INST: instantiating (33) with s__Copenhagen, s__Denmark, 55.67631, % 104.98/16.90 | 12.569355, copenhagen, dk, -35, 55.75695, 37.614975, moscow, ru, % 104.98/16.90 | 55, simplifying with (5), (7), (8), (9), (10), (11), (12), (13), % 104.98/16.90 | (14), (15), (16), (17), (18), (19), (20), (21), (22), (23), (24), % 104.98/16.90 | (25), (26), (27), (28), (29), (30), (31), (32), (47), (48), (49) % 104.98/16.90 | gives: % 104.98/16.91 | (50) $false % 104.98/16.91 | % 104.98/16.91 | CLOSE: (50) is inconsistent. % 104.98/16.91 | % 104.98/16.91 End of proof % 104.98/16.91 % SZS output end Proof for theBenchmark % 104.98/16.91 % 104.98/16.91 16293ms %------------------------------------------------------------------------------