%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : CSR060+1 : TPTP v8.1.2. Released v3.4.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 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 : Wed Aug 30 21:37:00 EDT 2023 % Result : Theorem 13.61s 2.58s % Output : Proof 18.30s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : CSR060+1 : TPTP v8.1.2. Released v3.4.0. % 0.07/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.33 % Computer : n013.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.33 % CPULimit : 300 % 0.14/0.33 % WCLimit : 300 % 0.14/0.33 % DateTime : Mon Aug 28 10:34:31 EDT 2023 % 0.14/0.34 % CPUTime : % 0.19/0.59 ________ _____ % 0.19/0.59 ___ __ \_________(_)________________________________ % 0.19/0.59 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.59 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.59 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.59 % 0.19/0.59 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.59 (2023-06-19) % 0.19/0.59 % 0.19/0.59 (c) Philipp Rümmer, 2009-2023 % 0.19/0.59 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.59 Amanda Stjerna. % 0.19/0.59 Free software under BSD-3-Clause. % 0.19/0.59 % 0.19/0.59 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.59 % 0.19/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.19/0.61 Running up to 7 provers in parallel. % 0.19/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.68/1.20 Prover 1: Preprocessing ... % 3.68/1.20 Prover 4: Preprocessing ... % 3.68/1.23 Prover 3: Preprocessing ... % 3.68/1.23 Prover 0: Preprocessing ... % 3.68/1.23 Prover 6: Preprocessing ... % 3.68/1.23 Prover 5: Preprocessing ... % 3.68/1.24 Prover 2: Preprocessing ... % 7.47/1.72 Prover 5: Proving ... % 7.63/1.74 Prover 2: Proving ... % 7.63/1.86 Prover 3: Warning: ignoring some quantifiers % 7.63/1.88 Prover 1: Warning: ignoring some quantifiers % 8.68/1.90 Prover 3: Constructing countermodel ... % 8.68/1.91 Prover 6: Proving ... % 8.68/1.95 Prover 1: Constructing countermodel ... % 9.28/1.98 Prover 0: Proving ... % 9.28/2.00 Prover 4: Constructing countermodel ... % 12.18/2.36 Prover 3: gave up % 12.48/2.37 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 12.97/2.46 Prover 7: Preprocessing ... % 13.61/2.58 Prover 0: proved (1966ms) % 13.61/2.58 % 13.61/2.58 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.61/2.58 % 13.61/2.59 Prover 5: stopped % 13.61/2.59 Prover 6: stopped % 13.61/2.59 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 13.61/2.59 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 13.61/2.59 Prover 2: stopped % 13.61/2.60 Prover 1: gave up % 13.61/2.60 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 13.61/2.60 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 13.61/2.60 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 14.49/2.68 Prover 7: Constructing countermodel ... % 14.49/2.69 Prover 8: Preprocessing ... % 14.49/2.70 Prover 13: Preprocessing ... % 14.49/2.70 Prover 16: Preprocessing ... % 14.49/2.70 Prover 10: Preprocessing ... % 14.49/2.72 Prover 11: Preprocessing ... % 15.57/2.84 Prover 16: Warning: ignoring some quantifiers % 16.05/2.86 Prover 16: Constructing countermodel ... % 16.13/2.87 Prover 10: Constructing countermodel ... % 16.13/2.90 Prover 13: Warning: ignoring some quantifiers % 16.49/2.94 Prover 13: Constructing countermodel ... % 16.77/2.98 Prover 8: Warning: ignoring some quantifiers % 16.77/3.01 Prover 8: Constructing countermodel ... % 16.77/3.02 Prover 4: Found proof (size 138) % 16.77/3.02 Prover 4: proved (2395ms) % 16.77/3.02 Prover 16: stopped % 16.77/3.02 Prover 7: stopped % 16.77/3.02 Prover 8: stopped % 16.77/3.02 Prover 13: stopped % 16.77/3.02 Prover 10: stopped % 17.44/3.05 Prover 11: Constructing countermodel ... % 17.44/3.07 Prover 11: stopped % 17.44/3.07 % 17.44/3.07 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 17.44/3.07 % 17.68/3.10 % SZS output start Proof for theBenchmark % 17.68/3.10 Assumptions after simplification: % 17.68/3.10 --------------------------------- % 17.68/3.10 % 17.68/3.10 (just1) % 17.68/3.12 genlmt(c_ldscdemonstrationspindleheadmt, % 17.68/3.12 c_currentworlddatacollectormt_nonhomocentric) = 0 & % 17.68/3.12 $i(c_currentworlddatacollectormt_nonhomocentric) & % 17.68/3.12 $i(c_ldscdemonstrationspindleheadmt) % 17.68/3.12 % 17.68/3.12 (just11) % 17.68/3.13 genlmt(c_machinelearningspindleheadmt, c_cycnounlearnermt) = 0 & % 17.68/3.13 $i(c_machinelearningspindleheadmt) & $i(c_cycnounlearnermt) % 17.68/3.13 % 17.68/3.13 (just13) % 17.68/3.13 $i(c_tptpcol_16_27189) & $i(c_tptp_9_51) & $i(c_cityofbostonma) & % 17.68/3.13 $i(c_objectfoundinlocation) & $i(c_ship) & % 17.68/3.13 $i(c_currentworlddatacollectormt_nonhomocentric) & ? [v0: any] : ? [v1: $i] % 17.68/3.13 : (mtvisible(c_currentworlddatacollectormt_nonhomocentric) = v0 & % 17.68/3.13 f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, % 17.68/3.13 c_cityofbostonma) = v1 & $i(v1) & ! [v2: $i] : ! [v3: $i] : ( ~ (v0 = 0) % 17.68/3.13 | ~ (f_relationexistsallfn(v2, c_tptp_9_51, c_tptpcol_16_27189, v1) = v3) % 17.68/3.13 | ~ $i(v2) | ? [v4: any] : ? [v5: any] : (tptp_9_51(v3, v2) = v5 & % 17.68/3.13 isa(v2, v1) = v4 & ( ~ (v4 = 0) | v5 = 0))) & ! [v2: $i] : ( ~ (v0 = 0) % 17.68/3.13 | ~ (isa(v2, v1) = 0) | ~ $i(v2) | ? [v3: $i] : (tptp_9_51(v3, v2) = 0 % 17.68/3.13 & f_relationexistsallfn(v2, c_tptp_9_51, c_tptpcol_16_27189, v1) = v3 & % 17.68/3.13 $i(v3)))) % 17.68/3.13 % 17.68/3.13 (just14) % 17.68/3.13 $i(c_tptpcol_16_27189) & $i(c_tptp_9_51) & $i(c_cityofbostonma) & % 17.68/3.14 $i(c_objectfoundinlocation) & $i(c_ship) & % 17.68/3.14 $i(c_currentworlddatacollectormt_nonhomocentric) & ? [v0: any] : ? [v1: $i] % 17.68/3.14 : ? [v2: any] : (mtvisible(c_currentworlddatacollectormt_nonhomocentric) = v0 % 17.68/3.14 & f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, % 17.68/3.14 c_cityofbostonma) = v1 & relationexistsall(c_tptp_9_51, % 17.68/3.14 c_tptpcol_16_27189, v1) = v2 & $i(v1) & ( ~ (v0 = 0) | v2 = 0)) % 17.68/3.14 % 17.68/3.14 (just15) % 17.68/3.14 $i(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 17.68/3.14 & $i(c_cityofbostonma) & $i(c_objectfoundinlocation) & $i(c_ship) & ? [v0: % 17.68/3.14 $i] : (f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, % 17.68/3.14 c_cityofbostonma) = v0 & % 17.68/3.14 isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 17.68/3.14 v0) = 0 & $i(v0)) % 17.68/3.14 % 17.68/3.14 (just4) % 17.68/3.14 $i(c_machinelearningspindleheadmt) & $i(c_translation_0_885) & % 17.68/3.14 $i(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988) & ? [v0: $i] : ? % 17.68/3.14 [v1: $i] : ? [v2: $i] : % 17.68/3.14 (f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988) = v0 & % 17.68/3.14 f_urlreferentfn(v0) = v1 & f_contentmtofcdafromeventfn(v1, % 17.68/3.14 c_translation_0_885) = v2 & genlmt(v2, c_machinelearningspindleheadmt) = 0 % 17.68/3.14 & $i(v2) & $i(v1) & $i(v0)) % 17.68/3.14 % 17.68/3.14 (just5) % 17.68/3.14 genlmt(c_machinelearningspindleheadmt, c_miptdatabase19681997_termsmt) = 0 & % 17.68/3.14 $i(c_miptdatabase19681997_termsmt) & $i(c_machinelearningspindleheadmt) % 17.68/3.14 % 17.68/3.14 (just51) % 17.68/3.14 $i(c_cityofbostonma) & $i(c_objectfoundinlocation) & $i(c_ship) & ? [v0: $i] % 17.68/3.14 : (f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, % 17.68/3.14 c_cityofbostonma) = v0 & $i(v0) & ! [v1: $i] : ! [v2: int] : (v2 = 0 | % 17.68/3.14 ~ % 17.68/3.14 (subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(v1) % 17.68/3.14 = v2) | ~ $i(v1) | ? [v3: int] : ( ~ (v3 = 0) & isa(v1, v0) = v3)) & % 17.68/3.14 ! [v1: $i] : ( ~ (isa(v1, v0) = 0) | ~ $i(v1) | % 17.68/3.14 subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(v1) % 17.68/3.14 = 0)) % 17.68/3.14 % 17.68/3.14 (just52) % 17.68/3.14 $i(c_cityofbostonma) & $i(c_objectfoundinlocation) & $i(c_ship) & ? [v0: $i] % 17.68/3.14 : (f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, % 17.68/3.14 c_cityofbostonma) = v0 & $i(v0) & ! [v1: $i] : ! [v2: int] : (v2 = 0 | % 17.68/3.14 ~ (isa(v1, v0) = v2) | ~ $i(v1) | ? [v3: int] : ( ~ (v3 = 0) & % 17.68/3.14 subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(v1) % 17.68/3.14 = v3)) & ! [v1: $i] : ( ~ % 17.68/3.14 (subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(v1) % 17.68/3.14 = 0) | ~ $i(v1) | isa(v1, v0) = 0)) % 17.68/3.14 % 17.68/3.14 (just53) % 17.68/3.14 $i(c_tptpcol_16_27189) & ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ % 17.68/3.14 (tptpcol_16_27189(v0) = v1) | ~ $i(v0) | ? [v2: int] : ( ~ (v2 = 0) & % 17.68/3.14 isa(v0, c_tptpcol_16_27189) = v2)) & ! [v0: $i] : ( ~ (isa(v0, % 17.68/3.14 c_tptpcol_16_27189) = 0) | ~ $i(v0) | tptpcol_16_27189(v0) = 0) % 17.68/3.14 % 17.68/3.14 (just54) % 17.68/3.15 $i(c_tptpcol_16_27189) & ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (isa(v0, % 17.68/3.15 c_tptpcol_16_27189) = v1) | ~ $i(v0) | ? [v2: int] : ( ~ (v2 = 0) & % 17.68/3.15 tptpcol_16_27189(v0) = v2)) & ! [v0: $i] : ( ~ (tptpcol_16_27189(v0) = 0) % 17.68/3.15 | ~ $i(v0) | isa(v0, c_tptpcol_16_27189) = 0) % 17.68/3.15 % 17.68/3.15 (just6) % 17.68/3.15 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 17.68/3.15 (f_relationexistsallfn(v0, v2, v3, v1) = v4) | ~ $i(v3) | ~ $i(v2) | ~ % 17.68/3.15 $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : % 17.68/3.15 (relationexistsall(v2, v3, v1) = v6 & isa(v4, v3) = v7 & isa(v0, v1) = v5 & % 17.68/3.15 ( ~ (v6 = 0) | ~ (v5 = 0) | v7 = 0))) % 17.68/3.15 % 17.68/3.15 (just8) % 17.68/3.15 genlmt(c_miptdatabase19681997_termsmt, c_ldscgeneralcollectormt) = 0 & % 17.68/3.15 $i(c_ldscgeneralcollectormt) & $i(c_miptdatabase19681997_termsmt) % 17.68/3.15 % 17.68/3.15 (just86) % 17.68/3.15 ! [v0: $i] : ! [v1: $i] : ( ~ (genlmt(v0, v1) = 0) | ~ $i(v1) | ~ $i(v0) | % 17.68/3.15 ? [v2: any] : ? [v3: any] : (mtvisible(v1) = v3 & mtvisible(v0) = v2 & ( ~ % 17.68/3.15 (v2 = 0) | v3 = 0))) % 17.68/3.15 % 17.68/3.15 (just9) % 17.68/3.15 genlmt(c_ldscgeneralcollectormt, c_ldscdemonstrationspindleheadmt) = 0 & % 17.68/3.15 $i(c_ldscgeneralcollectormt) & $i(c_ldscdemonstrationspindleheadmt) % 17.68/3.15 % 17.68/3.15 (query60) % 17.68/3.15 $i(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 17.68/3.15 & $i(c_translation_0_885) & % 17.68/3.15 $i(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988) & ? [v0: $i] : ? % 17.68/3.15 [v1: $i] : ? [v2: $i] : (mtvisible(v2) = 0 & % 17.68/3.15 f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988) = v0 & % 17.68/3.15 f_urlreferentfn(v0) = v1 & f_contentmtofcdafromeventfn(v1, % 17.68/3.15 c_translation_0_885) = v2 & $i(v2) & $i(v1) & $i(v0) & ! [v3: $i] : ( ~ % 17.68/3.15 (tptpcol_16_27189(v3) = 0) | ~ $i(v3) | ? [v4: int] : ( ~ (v4 = 0) & % 17.68/3.15 tptp_9_51(v3, % 17.68/3.15 c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 17.68/3.15 = v4)) & ! [v3: $i] : ( ~ (tptp_9_51(v3, % 17.68/3.15 c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 17.68/3.15 = 0) | ~ $i(v3) | ? [v4: int] : ( ~ (v4 = 0) & tptpcol_16_27189(v3) = % 17.68/3.15 v4))) % 17.68/3.15 % 17.68/3.15 (function-axioms) % 17.68/3.16 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 17.68/3.16 $i] : (v1 = v0 | ~ (f_relationexistsallfn(v5, v4, v3, v2) = v1) | ~ % 17.68/3.16 (f_relationexistsallfn(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 17.68/3.16 ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = % 17.68/3.16 v0 | ~ (natargument(v4, v3, v2) = v1) | ~ (natargument(v4, v3, v2) = v0)) % 17.68/3.16 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = % 17.68/3.16 v0 | ~ (f_subcollectionofwithrelationtofn(v4, v3, v2) = v1) | ~ % 17.68/3.16 (f_subcollectionofwithrelationtofn(v4, v3, v2) = v0)) & ! [v0: % 17.68/3.16 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 17.68/3.16 : ! [v4: $i] : (v1 = v0 | ~ (relationexistsall(v4, v3, v2) = v1) | ~ % 17.68/3.16 (relationexistsall(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.68/3.16 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 17.68/3.16 (natfunction(v3, v2) = v1) | ~ (natfunction(v3, v2) = v0)) & ! [v0: % 17.68/3.16 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 17.68/3.16 : (v1 = v0 | ~ (subregions(v3, v2) = v1) | ~ (subregions(v3, v2) = v0)) & ! % 17.68/3.16 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 17.68/3.16 $i] : (v1 = v0 | ~ (geographicallysubsumes(v3, v2) = v1) | ~ % 17.68/3.16 (geographicallysubsumes(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 17.68/3.16 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 17.68/3.16 (geopoliticalsubdivision(v3, v2) = v1) | ~ (geopoliticalsubdivision(v3, v2) % 17.68/3.16 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 17.68/3.16 $i] : ! [v3: $i] : (v1 = v0 | ~ (objectfoundinlocation(v3, v2) = v1) | ~ % 17.68/3.16 (objectfoundinlocation(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.68/3.16 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (genls(v3, % 17.68/3.16 v2) = v1) | ~ (genls(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 17.68/3.16 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 17.68/3.16 (genlpreds(v3, v2) = v1) | ~ (genlpreds(v3, v2) = v0)) & ! [v0: % 17.68/3.16 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 17.68/3.16 : (v1 = v0 | ~ (genlinverse(v3, v2) = v1) | ~ (genlinverse(v3, v2) = v0)) & % 17.68/3.16 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 17.68/3.16 $i] : (v1 = v0 | ~ (disjointwith(v3, v2) = v1) | ~ (disjointwith(v3, v2) = % 17.68/3.16 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 17.68/3.16 $i] : ! [v3: $i] : (v1 = v0 | ~ (tptp_9_51(v3, v2) = v1) | ~ % 17.68/3.16 (tptp_9_51(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.68/3.16 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 17.68/3.16 (resultisaarg(v3, v2) = v1) | ~ (resultisaarg(v3, v2) = v0)) & ! [v0: % 17.68/3.16 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 17.68/3.16 : (v1 = v0 | ~ (isa(v3, v2) = v1) | ~ (isa(v3, v2) = v0)) & ! [v0: $i] : ! % 17.68/3.16 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 17.68/3.16 (f_contentmtofcdafromeventfn(v3, v2) = v1) | ~ % 17.68/3.16 (f_contentmtofcdafromeventfn(v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 17.68/3.16 ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 17.68/3.16 (genlmt(v3, v2) = v1) | ~ (genlmt(v3, v2) = v0)) & ! [v0: % 17.68/3.16 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 17.68/3.16 ~ (microtheory(v2) = v1) | ~ (microtheory(v2) = v0)) & ! [v0: % 17.68/3.16 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 17.68/3.16 ~ (computerdataartifact(v2) = v1) | ~ (computerdataartifact(v2) = v0)) & ! % 17.68/3.16 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 17.68/3.16 | ~ (uniformresourcelocator(v2) = v1) | ~ (uniformresourcelocator(v2) = % 17.68/3.16 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 17.68/3.16 $i] : (v1 = v0 | ~ (function_denotational(v2) = v1) | ~ % 17.68/3.16 (function_denotational(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.68/3.16 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (positiveinteger(v2) = v1) % 17.68/3.16 | ~ (positiveinteger(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.68/3.16 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (thing(v2) = v1) | ~ % 17.68/3.16 (thing(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 17.68/3.16 : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_7_26628(v2) = v1) | ~ % 17.68/3.16 (tptpcol_7_26628(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.68/3.16 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_16_27189(v2) = v1) % 17.68/3.16 | ~ (tptpcol_16_27189(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.68/3.16 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (ship(v2) = v1) | ~ % 17.68/3.16 (ship(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 17.68/3.16 ! [v2: $i] : (v1 = v0 | ~ (spatialthing_localized(v2) = v1) | ~ % 17.68/3.16 (spatialthing_localized(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.68/3.16 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ % 17.68/3.16 (spatialthing_nonsituational(v2) = v1) | ~ (spatialthing_nonsituational(v2) % 17.68/3.16 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 17.68/3.16 $i] : (v1 = v0 | ~ (collection(v2) = v1) | ~ (collection(v2) = v0)) & ! % 17.68/3.16 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 17.68/3.16 | ~ (binarypredicate(v2) = v1) | ~ (binarypredicate(v2) = v0)) & ! [v0: % 17.68/3.16 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 17.68/3.16 ~ (predicate(v2) = v1) | ~ (predicate(v2) = v0)) & ! [v0: % 17.68/3.16 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 17.68/3.16 ~ % 17.68/3.16 (subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(v2) % 17.68/3.16 = v1) | ~ % 17.68/3.16 (subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(v2) % 17.68/3.16 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 17.68/3.16 $i] : (v1 = v0 | ~ (mtvisible(v2) = v1) | ~ (mtvisible(v2) = v0)) & ! % 17.68/3.16 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 17.68/3.16 | ~ (transitivebinarypredicate(v2) = v1) | ~ % 17.68/3.16 (transitivebinarypredicate(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 17.68/3.16 $i] : (v1 = v0 | ~ (f_urlfn(v2) = v1) | ~ (f_urlfn(v2) = v0)) & ! [v0: % 17.68/3.16 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (f_urlreferentfn(v2) = v1) | % 17.68/3.16 ~ (f_urlreferentfn(v2) = v0)) % 17.68/3.16 % 17.68/3.16 Further assumptions not needed in the proof: % 17.68/3.16 -------------------------------------------- % 17.68/3.16 just10, just12, just16, just17, just18, just19, just2, just20, just21, just22, % 17.68/3.16 just23, just24, just25, just26, just27, just28, just29, just3, just30, just31, % 17.68/3.16 just32, just33, just34, just35, just36, just37, just38, just39, just40, just41, % 17.68/3.16 just42, just43, just44, just45, just46, just47, just48, just49, just50, just55, % 17.68/3.16 just56, just57, just58, just59, just60, just61, just62, just63, just64, just65, % 17.68/3.16 just66, just67, just68, just69, just7, just70, just71, just72, just73, just74, % 17.68/3.16 just75, just76, just77, just78, just79, just80, just81, just82, just83, just84, % 17.68/3.16 just85, just87, just88, just89, just90, just91, just92, just93, just94 % 17.68/3.16 % 17.68/3.16 Those formulas are unsatisfiable: % 17.68/3.16 --------------------------------- % 17.68/3.16 % 17.68/3.16 Begin of proof % 17.68/3.17 | % 17.68/3.17 | ALPHA: (just1) implies: % 17.68/3.17 | (1) genlmt(c_ldscdemonstrationspindleheadmt, % 17.68/3.17 | c_currentworlddatacollectormt_nonhomocentric) = 0 % 17.68/3.17 | % 17.68/3.17 | ALPHA: (just4) implies: % 17.68/3.17 | (2) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 17.68/3.17 | (f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988) = v0 & % 17.68/3.17 | f_urlreferentfn(v0) = v1 & f_contentmtofcdafromeventfn(v1, % 17.68/3.17 | c_translation_0_885) = v2 & genlmt(v2, % 17.68/3.17 | c_machinelearningspindleheadmt) = 0 & $i(v2) & $i(v1) & $i(v0)) % 17.68/3.17 | % 17.68/3.17 | ALPHA: (just5) implies: % 17.68/3.17 | (3) genlmt(c_machinelearningspindleheadmt, c_miptdatabase19681997_termsmt) % 17.68/3.17 | = 0 % 17.68/3.17 | % 17.68/3.17 | ALPHA: (just8) implies: % 17.68/3.17 | (4) $i(c_miptdatabase19681997_termsmt) % 17.68/3.17 | (5) genlmt(c_miptdatabase19681997_termsmt, c_ldscgeneralcollectormt) = 0 % 17.68/3.17 | % 17.68/3.17 | ALPHA: (just9) implies: % 17.68/3.17 | (6) $i(c_ldscdemonstrationspindleheadmt) % 17.68/3.17 | (7) $i(c_ldscgeneralcollectormt) % 17.68/3.17 | (8) genlmt(c_ldscgeneralcollectormt, c_ldscdemonstrationspindleheadmt) = 0 % 17.68/3.17 | % 17.68/3.17 | ALPHA: (just11) implies: % 17.68/3.17 | (9) $i(c_cycnounlearnermt) % 17.68/3.17 | (10) $i(c_machinelearningspindleheadmt) % 17.68/3.17 | (11) genlmt(c_machinelearningspindleheadmt, c_cycnounlearnermt) = 0 % 17.68/3.17 | % 17.68/3.17 | ALPHA: (just13) implies: % 17.68/3.17 | (12) ? [v0: any] : ? [v1: $i] : % 17.68/3.17 | (mtvisible(c_currentworlddatacollectormt_nonhomocentric) = v0 & % 17.68/3.17 | f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, % 17.68/3.17 | c_cityofbostonma) = v1 & $i(v1) & ! [v2: $i] : ! [v3: $i] : ( ~ % 17.68/3.17 | (v0 = 0) | ~ (f_relationexistsallfn(v2, c_tptp_9_51, % 17.68/3.17 | c_tptpcol_16_27189, v1) = v3) | ~ $i(v2) | ? [v4: any] : ? % 17.68/3.17 | [v5: any] : (tptp_9_51(v3, v2) = v5 & isa(v2, v1) = v4 & ( ~ (v4 = % 17.68/3.17 | 0) | v5 = 0))) & ! [v2: $i] : ( ~ (v0 = 0) | ~ (isa(v2, % 17.68/3.17 | v1) = 0) | ~ $i(v2) | ? [v3: $i] : (tptp_9_51(v3, v2) = 0 & % 17.68/3.17 | f_relationexistsallfn(v2, c_tptp_9_51, c_tptpcol_16_27189, v1) = % 17.68/3.17 | v3 & $i(v3)))) % 17.68/3.17 | % 17.68/3.17 | ALPHA: (just14) implies: % 17.68/3.17 | (13) $i(c_currentworlddatacollectormt_nonhomocentric) % 17.68/3.17 | (14) $i(c_tptp_9_51) % 17.68/3.17 | (15) ? [v0: any] : ? [v1: $i] : ? [v2: any] : % 17.68/3.17 | (mtvisible(c_currentworlddatacollectormt_nonhomocentric) = v0 & % 17.68/3.17 | f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, % 17.68/3.17 | c_cityofbostonma) = v1 & relationexistsall(c_tptp_9_51, % 17.68/3.17 | c_tptpcol_16_27189, v1) = v2 & $i(v1) & ( ~ (v0 = 0) | v2 = 0)) % 17.68/3.17 | % 17.68/3.17 | ALPHA: (just15) implies: % 17.68/3.17 | (16) ? [v0: $i] : (f_subcollectionofwithrelationtofn(c_ship, % 17.68/3.17 | c_objectfoundinlocation, c_cityofbostonma) = v0 & % 17.68/3.17 | isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 17.68/3.17 | v0) = 0 & $i(v0)) % 17.68/3.17 | % 17.68/3.17 | ALPHA: (just51) implies: % 17.68/3.17 | (17) ? [v0: $i] : (f_subcollectionofwithrelationtofn(c_ship, % 17.68/3.17 | c_objectfoundinlocation, c_cityofbostonma) = v0 & $i(v0) & ! [v1: % 17.68/3.17 | $i] : ! [v2: int] : (v2 = 0 | ~ % 17.68/3.17 | (subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(v1) % 17.68/3.17 | = v2) | ~ $i(v1) | ? [v3: int] : ( ~ (v3 = 0) & isa(v1, v0) = % 17.68/3.17 | v3)) & ! [v1: $i] : ( ~ (isa(v1, v0) = 0) | ~ $i(v1) | % 17.68/3.17 | subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(v1) % 17.68/3.17 | = 0)) % 17.68/3.17 | % 17.68/3.17 | ALPHA: (just52) implies: % 17.68/3.18 | (18) ? [v0: $i] : (f_subcollectionofwithrelationtofn(c_ship, % 17.68/3.18 | c_objectfoundinlocation, c_cityofbostonma) = v0 & $i(v0) & ! [v1: % 17.68/3.18 | $i] : ! [v2: int] : (v2 = 0 | ~ (isa(v1, v0) = v2) | ~ $i(v1) | % 17.68/3.18 | ? [v3: int] : ( ~ (v3 = 0) & % 17.68/3.18 | subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(v1) % 17.68/3.18 | = v3)) & ! [v1: $i] : ( ~ % 17.68/3.18 | (subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(v1) % 17.68/3.18 | = 0) | ~ $i(v1) | isa(v1, v0) = 0)) % 17.68/3.18 | % 17.68/3.18 | ALPHA: (just53) implies: % 17.68/3.18 | (19) ! [v0: $i] : ( ~ (isa(v0, c_tptpcol_16_27189) = 0) | ~ $i(v0) | % 17.68/3.18 | tptpcol_16_27189(v0) = 0) % 17.68/3.18 | % 17.68/3.18 | ALPHA: (just54) implies: % 17.68/3.18 | (20) $i(c_tptpcol_16_27189) % 17.68/3.18 | % 17.68/3.18 | ALPHA: (query60) implies: % 17.68/3.18 | (21) $i(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 17.68/3.18 | (22) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (mtvisible(v2) = 0 & % 17.68/3.18 | f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988) = v0 % 17.68/3.18 | & f_urlreferentfn(v0) = v1 & f_contentmtofcdafromeventfn(v1, % 17.68/3.18 | c_translation_0_885) = v2 & $i(v2) & $i(v1) & $i(v0) & ! [v3: $i] % 17.68/3.18 | : ( ~ (tptpcol_16_27189(v3) = 0) | ~ $i(v3) | ? [v4: int] : ( ~ % 17.68/3.18 | (v4 = 0) & tptp_9_51(v3, % 17.68/3.18 | c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 17.68/3.18 | = v4)) & ! [v3: $i] : ( ~ (tptp_9_51(v3, % 17.68/3.18 | c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 17.68/3.18 | = 0) | ~ $i(v3) | ? [v4: int] : ( ~ (v4 = 0) & % 17.68/3.18 | tptpcol_16_27189(v3) = v4))) % 17.68/3.18 | % 17.68/3.18 | ALPHA: (function-axioms) implies: % 17.68/3.18 | (23) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 17.68/3.18 | (f_urlreferentfn(v2) = v1) | ~ (f_urlreferentfn(v2) = v0)) % 17.68/3.18 | (24) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (f_urlfn(v2) = % 17.68/3.18 | v1) | ~ (f_urlfn(v2) = v0)) % 17.68/3.18 | (25) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 17.68/3.18 | : (v1 = v0 | ~ (mtvisible(v2) = v1) | ~ (mtvisible(v2) = v0)) % 17.68/3.18 | (26) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 17.68/3.18 | : (v1 = v0 | ~ (tptpcol_16_27189(v2) = v1) | ~ (tptpcol_16_27189(v2) % 17.68/3.18 | = v0)) % 17.68/3.18 | (27) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 17.68/3.18 | (f_contentmtofcdafromeventfn(v3, v2) = v1) | ~ % 17.68/3.18 | (f_contentmtofcdafromeventfn(v3, v2) = v0)) % 17.68/3.18 | (28) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 17.68/3.18 | : ! [v3: $i] : (v1 = v0 | ~ (isa(v3, v2) = v1) | ~ (isa(v3, v2) = % 17.68/3.18 | v0)) % 17.68/3.18 | (29) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 17.68/3.18 | : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (relationexistsall(v4, v3, % 17.68/3.18 | v2) = v1) | ~ (relationexistsall(v4, v3, v2) = v0)) % 17.68/3.18 | (30) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 17.68/3.18 | (v1 = v0 | ~ (f_subcollectionofwithrelationtofn(v4, v3, v2) = v1) | % 17.68/3.18 | ~ (f_subcollectionofwithrelationtofn(v4, v3, v2) = v0)) % 17.68/3.18 | % 17.68/3.18 | DELTA: instantiating (16) with fresh symbol all_79_0 gives: % 17.68/3.18 | (31) f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, % 17.68/3.18 | c_cityofbostonma) = all_79_0 & % 17.68/3.18 | isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 17.68/3.18 | all_79_0) = 0 & $i(all_79_0) % 17.68/3.18 | % 17.68/3.18 | ALPHA: (31) implies: % 17.68/3.18 | (32) isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 17.68/3.18 | all_79_0) = 0 % 17.68/3.18 | (33) f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, % 17.68/3.18 | c_cityofbostonma) = all_79_0 % 17.68/3.18 | % 17.68/3.18 | DELTA: instantiating (15) with fresh symbols all_81_0, all_81_1, all_81_2 % 17.68/3.18 | gives: % 17.68/3.18 | (34) mtvisible(c_currentworlddatacollectormt_nonhomocentric) = all_81_2 & % 17.68/3.18 | f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, % 17.68/3.18 | c_cityofbostonma) = all_81_1 & relationexistsall(c_tptp_9_51, % 17.68/3.18 | c_tptpcol_16_27189, all_81_1) = all_81_0 & $i(all_81_1) & ( ~ % 17.68/3.18 | (all_81_2 = 0) | all_81_0 = 0) % 17.68/3.18 | % 17.68/3.18 | ALPHA: (34) implies: % 17.68/3.18 | (35) $i(all_81_1) % 17.68/3.18 | (36) relationexistsall(c_tptp_9_51, c_tptpcol_16_27189, all_81_1) = % 17.68/3.18 | all_81_0 % 17.68/3.19 | (37) f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, % 17.68/3.19 | c_cityofbostonma) = all_81_1 % 17.68/3.19 | (38) mtvisible(c_currentworlddatacollectormt_nonhomocentric) = all_81_2 % 17.68/3.19 | (39) ~ (all_81_2 = 0) | all_81_0 = 0 % 17.68/3.19 | % 17.68/3.19 | DELTA: instantiating (2) with fresh symbols all_83_0, all_83_1, all_83_2 % 17.68/3.19 | gives: % 17.68/3.19 | (40) f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988) = % 17.68/3.19 | all_83_2 & f_urlreferentfn(all_83_2) = all_83_1 & % 17.68/3.19 | f_contentmtofcdafromeventfn(all_83_1, c_translation_0_885) = all_83_0 % 17.68/3.19 | & genlmt(all_83_0, c_machinelearningspindleheadmt) = 0 & $i(all_83_0) % 17.68/3.19 | & $i(all_83_1) & $i(all_83_2) % 17.68/3.19 | % 17.68/3.19 | ALPHA: (40) implies: % 17.68/3.19 | (41) genlmt(all_83_0, c_machinelearningspindleheadmt) = 0 % 17.68/3.19 | (42) f_contentmtofcdafromeventfn(all_83_1, c_translation_0_885) = all_83_0 % 17.68/3.19 | (43) f_urlreferentfn(all_83_2) = all_83_1 % 17.68/3.19 | (44) f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988) = % 17.68/3.19 | all_83_2 % 17.68/3.19 | % 17.68/3.19 | DELTA: instantiating (18) with fresh symbol all_85_0 gives: % 17.68/3.19 | (45) f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, % 17.68/3.19 | c_cityofbostonma) = all_85_0 & $i(all_85_0) & ! [v0: $i] : ! [v1: % 17.68/3.19 | int] : (v1 = 0 | ~ (isa(v0, all_85_0) = v1) | ~ $i(v0) | ? [v2: % 17.68/3.19 | int] : ( ~ (v2 = 0) & % 17.68/3.19 | subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(v0) % 17.68/3.19 | = v2)) & ! [v0: $i] : ( ~ % 17.68/3.19 | (subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(v0) % 17.68/3.19 | = 0) | ~ $i(v0) | isa(v0, all_85_0) = 0) % 17.68/3.19 | % 17.68/3.19 | ALPHA: (45) implies: % 17.68/3.19 | (46) f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, % 17.68/3.19 | c_cityofbostonma) = all_85_0 % 17.68/3.19 | % 17.68/3.19 | DELTA: instantiating (17) with fresh symbol all_88_0 gives: % 17.68/3.19 | (47) f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, % 17.68/3.19 | c_cityofbostonma) = all_88_0 & $i(all_88_0) & ! [v0: $i] : ! [v1: % 17.68/3.19 | int] : (v1 = 0 | ~ % 17.68/3.19 | (subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(v0) % 17.68/3.19 | = v1) | ~ $i(v0) | ? [v2: int] : ( ~ (v2 = 0) & isa(v0, % 17.68/3.19 | all_88_0) = v2)) & ! [v0: $i] : ( ~ (isa(v0, all_88_0) = 0) | % 17.68/3.19 | ~ $i(v0) | % 17.68/3.19 | subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(v0) % 17.68/3.19 | = 0) % 17.68/3.19 | % 17.68/3.19 | ALPHA: (47) implies: % 17.68/3.19 | (48) f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, % 17.68/3.19 | c_cityofbostonma) = all_88_0 % 17.68/3.19 | % 17.68/3.19 | DELTA: instantiating (22) with fresh symbols all_91_0, all_91_1, all_91_2 % 17.68/3.19 | gives: % 17.68/3.19 | (49) mtvisible(all_91_0) = 0 & % 17.68/3.19 | f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988) = % 17.68/3.19 | all_91_2 & f_urlreferentfn(all_91_2) = all_91_1 & % 17.68/3.19 | f_contentmtofcdafromeventfn(all_91_1, c_translation_0_885) = all_91_0 % 17.68/3.19 | & $i(all_91_0) & $i(all_91_1) & $i(all_91_2) & ! [v0: $i] : ( ~ % 17.68/3.19 | (tptpcol_16_27189(v0) = 0) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) % 17.68/3.19 | & tptp_9_51(v0, % 17.68/3.19 | c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 17.68/3.19 | = v1)) & ! [v0: $i] : ( ~ (tptp_9_51(v0, % 17.68/3.19 | c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 17.68/3.19 | = 0) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 17.68/3.19 | tptpcol_16_27189(v0) = v1)) % 17.68/3.19 | % 17.68/3.19 | ALPHA: (49) implies: % 17.68/3.19 | (50) $i(all_91_0) % 17.68/3.19 | (51) f_contentmtofcdafromeventfn(all_91_1, c_translation_0_885) = all_91_0 % 17.68/3.19 | (52) f_urlreferentfn(all_91_2) = all_91_1 % 17.68/3.19 | (53) f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988) = % 17.68/3.19 | all_91_2 % 17.68/3.19 | (54) mtvisible(all_91_0) = 0 % 17.68/3.19 | (55) ! [v0: $i] : ( ~ (tptp_9_51(v0, % 17.68/3.19 | c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 17.68/3.19 | = 0) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 17.68/3.19 | tptpcol_16_27189(v0) = v1)) % 17.68/3.19 | % 17.68/3.19 | DELTA: instantiating (12) with fresh symbols all_94_0, all_94_1 gives: % 17.68/3.19 | (56) mtvisible(c_currentworlddatacollectormt_nonhomocentric) = all_94_1 & % 17.68/3.19 | f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, % 17.68/3.19 | c_cityofbostonma) = all_94_0 & $i(all_94_0) & ! [v0: $i] : ! [v1: % 17.68/3.19 | $i] : ( ~ (all_94_1 = 0) | ~ (f_relationexistsallfn(v0, % 17.68/3.19 | c_tptp_9_51, c_tptpcol_16_27189, all_94_0) = v1) | ~ $i(v0) | % 17.68/3.19 | ? [v2: any] : ? [v3: any] : (tptp_9_51(v1, v0) = v3 & isa(v0, % 17.68/3.19 | all_94_0) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0: $i] : ( ~ % 17.68/3.19 | (all_94_1 = 0) | ~ (isa(v0, all_94_0) = 0) | ~ $i(v0) | ? [v1: % 17.68/3.19 | $i] : (tptp_9_51(v1, v0) = 0 & f_relationexistsallfn(v0, % 17.68/3.19 | c_tptp_9_51, c_tptpcol_16_27189, all_94_0) = v1 & $i(v1))) % 17.68/3.19 | % 17.68/3.19 | ALPHA: (56) implies: % 17.68/3.19 | (57) f_subcollectionofwithrelationtofn(c_ship, c_objectfoundinlocation, % 17.68/3.19 | c_cityofbostonma) = all_94_0 % 17.68/3.19 | (58) mtvisible(c_currentworlddatacollectormt_nonhomocentric) = all_94_1 % 17.68/3.20 | (59) ! [v0: $i] : ( ~ (all_94_1 = 0) | ~ (isa(v0, all_94_0) = 0) | ~ % 17.68/3.20 | $i(v0) | ? [v1: $i] : (tptp_9_51(v1, v0) = 0 & % 17.68/3.20 | f_relationexistsallfn(v0, c_tptp_9_51, c_tptpcol_16_27189, % 17.68/3.20 | all_94_0) = v1 & $i(v1))) % 17.68/3.20 | % 17.68/3.20 | GROUND_INST: instantiating (24) with all_83_2, all_91_2, % 17.68/3.20 | s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988, % 17.68/3.20 | simplifying with (44), (53) gives: % 17.68/3.20 | (60) all_91_2 = all_83_2 % 17.68/3.20 | % 17.68/3.20 | GROUND_INST: instantiating (30) with all_85_0, all_88_0, c_cityofbostonma, % 17.68/3.20 | c_objectfoundinlocation, c_ship, simplifying with (46), (48) % 17.68/3.20 | gives: % 17.68/3.20 | (61) all_88_0 = all_85_0 % 17.68/3.20 | % 17.68/3.20 | GROUND_INST: instantiating (30) with all_79_0, all_88_0, c_cityofbostonma, % 17.68/3.20 | c_objectfoundinlocation, c_ship, simplifying with (33), (48) % 17.68/3.20 | gives: % 17.68/3.20 | (62) all_88_0 = all_79_0 % 17.68/3.20 | % 17.68/3.20 | GROUND_INST: instantiating (30) with all_85_0, all_94_0, c_cityofbostonma, % 17.68/3.20 | c_objectfoundinlocation, c_ship, simplifying with (46), (57) % 17.68/3.20 | gives: % 17.68/3.20 | (63) all_94_0 = all_85_0 % 17.68/3.20 | % 17.68/3.20 | GROUND_INST: instantiating (30) with all_81_1, all_94_0, c_cityofbostonma, % 17.68/3.20 | c_objectfoundinlocation, c_ship, simplifying with (37), (57) % 17.68/3.20 | gives: % 17.68/3.20 | (64) all_94_0 = all_81_1 % 17.68/3.20 | % 17.68/3.20 | GROUND_INST: instantiating (25) with all_81_2, all_94_1, % 17.68/3.20 | c_currentworlddatacollectormt_nonhomocentric, simplifying with % 17.68/3.20 | (38), (58) gives: % 17.68/3.20 | (65) all_94_1 = all_81_2 % 17.68/3.20 | % 17.68/3.20 | COMBINE_EQS: (63), (64) imply: % 17.68/3.20 | (66) all_85_0 = all_81_1 % 17.68/3.20 | % 17.68/3.20 | SIMP: (66) implies: % 17.68/3.20 | (67) all_85_0 = all_81_1 % 17.68/3.20 | % 17.68/3.20 | COMBINE_EQS: (61), (62) imply: % 17.68/3.20 | (68) all_85_0 = all_79_0 % 17.68/3.20 | % 17.68/3.20 | SIMP: (68) implies: % 17.68/3.20 | (69) all_85_0 = all_79_0 % 17.68/3.20 | % 17.68/3.20 | COMBINE_EQS: (67), (69) imply: % 17.68/3.20 | (70) all_81_1 = all_79_0 % 17.68/3.20 | % 17.68/3.20 | COMBINE_EQS: (64), (70) imply: % 17.68/3.20 | (71) all_94_0 = all_79_0 % 17.68/3.20 | % 17.68/3.20 | REDUCE: (36), (70) imply: % 17.68/3.20 | (72) relationexistsall(c_tptp_9_51, c_tptpcol_16_27189, all_79_0) = % 17.68/3.20 | all_81_0 % 17.68/3.20 | % 17.68/3.20 | REDUCE: (52), (60) imply: % 17.68/3.20 | (73) f_urlreferentfn(all_83_2) = all_91_1 % 17.68/3.20 | % 17.68/3.20 | REDUCE: (35), (70) imply: % 17.68/3.20 | (74) $i(all_79_0) % 17.68/3.20 | % 17.68/3.20 | GROUND_INST: instantiating (23) with all_83_1, all_91_1, all_83_2, simplifying % 17.68/3.20 | with (43), (73) gives: % 17.68/3.20 | (75) all_91_1 = all_83_1 % 17.68/3.20 | % 17.68/3.20 | REDUCE: (51), (75) imply: % 17.68/3.20 | (76) f_contentmtofcdafromeventfn(all_83_1, c_translation_0_885) = all_91_0 % 17.68/3.20 | % 17.68/3.20 | GROUND_INST: instantiating (27) with all_83_0, all_91_0, c_translation_0_885, % 17.68/3.20 | all_83_1, simplifying with (42), (76) gives: % 17.68/3.20 | (77) all_91_0 = all_83_0 % 17.68/3.20 | % 17.68/3.20 | REDUCE: (54), (77) imply: % 17.68/3.20 | (78) mtvisible(all_83_0) = 0 % 17.68/3.20 | % 17.68/3.20 | REDUCE: (50), (77) imply: % 17.68/3.20 | (79) $i(all_83_0) % 17.68/3.20 | % 17.68/3.20 | GROUND_INST: instantiating (just86) with c_ldscdemonstrationspindleheadmt, % 17.68/3.20 | c_currentworlddatacollectormt_nonhomocentric, simplifying with % 17.68/3.20 | (1), (6), (13) gives: % 17.68/3.20 | (80) ? [v0: any] : ? [v1: any] : % 17.68/3.20 | (mtvisible(c_currentworlddatacollectormt_nonhomocentric) = v1 & % 17.68/3.20 | mtvisible(c_ldscdemonstrationspindleheadmt) = v0 & ( ~ (v0 = 0) | v1 % 17.68/3.20 | = 0)) % 17.68/3.20 | % 17.68/3.20 | GROUND_INST: instantiating (just86) with c_machinelearningspindleheadmt, % 17.68/3.20 | c_cycnounlearnermt, simplifying with (9), (10), (11) gives: % 17.68/3.21 | (81) ? [v0: any] : ? [v1: any] : % 17.68/3.21 | (mtvisible(c_machinelearningspindleheadmt) = v0 & % 17.68/3.21 | mtvisible(c_cycnounlearnermt) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 17.68/3.21 | % 17.68/3.21 | GROUND_INST: instantiating (just86) with c_machinelearningspindleheadmt, % 17.68/3.21 | c_miptdatabase19681997_termsmt, simplifying with (3), (4), (10) % 17.68/3.21 | gives: % 17.68/3.21 | (82) ? [v0: any] : ? [v1: any] : % 17.68/3.21 | (mtvisible(c_miptdatabase19681997_termsmt) = v1 & % 17.68/3.21 | mtvisible(c_machinelearningspindleheadmt) = v0 & ( ~ (v0 = 0) | v1 = % 17.68/3.21 | 0)) % 17.68/3.21 | % 17.68/3.21 | GROUND_INST: instantiating (just86) with c_miptdatabase19681997_termsmt, % 17.68/3.21 | c_ldscgeneralcollectormt, simplifying with (4), (5), (7) gives: % 17.68/3.21 | (83) ? [v0: any] : ? [v1: any] : (mtvisible(c_ldscgeneralcollectormt) = % 17.68/3.21 | v1 & mtvisible(c_miptdatabase19681997_termsmt) = v0 & ( ~ (v0 = 0) | % 17.68/3.21 | v1 = 0)) % 17.68/3.21 | % 17.68/3.21 | GROUND_INST: instantiating (just86) with c_ldscgeneralcollectormt, % 17.68/3.21 | c_ldscdemonstrationspindleheadmt, simplifying with (6), (7), (8) % 17.68/3.21 | gives: % 17.68/3.21 | (84) ? [v0: any] : ? [v1: any] : (mtvisible(c_ldscgeneralcollectormt) = % 17.68/3.21 | v0 & mtvisible(c_ldscdemonstrationspindleheadmt) = v1 & ( ~ (v0 = 0) % 17.68/3.21 | | v1 = 0)) % 17.68/3.21 | % 17.68/3.21 | GROUND_INST: instantiating (just86) with all_83_0, % 17.68/3.21 | c_machinelearningspindleheadmt, simplifying with (10), (41), (79) % 17.68/3.21 | gives: % 17.68/3.21 | (85) ? [v0: any] : ? [v1: any] : (mtvisible(all_83_0) = v0 & % 17.68/3.21 | mtvisible(c_machinelearningspindleheadmt) = v1 & ( ~ (v0 = 0) | v1 = % 17.68/3.21 | 0)) % 17.68/3.21 | % 17.68/3.21 | DELTA: instantiating (84) with fresh symbols all_117_0, all_117_1 gives: % 17.68/3.21 | (86) mtvisible(c_ldscgeneralcollectormt) = all_117_1 & % 17.68/3.21 | mtvisible(c_ldscdemonstrationspindleheadmt) = all_117_0 & ( ~ % 17.68/3.21 | (all_117_1 = 0) | all_117_0 = 0) % 17.68/3.21 | % 17.68/3.21 | ALPHA: (86) implies: % 17.68/3.21 | (87) mtvisible(c_ldscdemonstrationspindleheadmt) = all_117_0 % 17.68/3.21 | (88) mtvisible(c_ldscgeneralcollectormt) = all_117_1 % 17.68/3.21 | (89) ~ (all_117_1 = 0) | all_117_0 = 0 % 17.68/3.21 | % 17.68/3.21 | DELTA: instantiating (81) with fresh symbols all_121_0, all_121_1 gives: % 17.68/3.21 | (90) mtvisible(c_machinelearningspindleheadmt) = all_121_1 & % 17.68/3.21 | mtvisible(c_cycnounlearnermt) = all_121_0 & ( ~ (all_121_1 = 0) | % 17.68/3.21 | all_121_0 = 0) % 17.68/3.21 | % 17.68/3.21 | ALPHA: (90) implies: % 17.68/3.21 | (91) mtvisible(c_machinelearningspindleheadmt) = all_121_1 % 17.68/3.21 | % 17.68/3.21 | DELTA: instantiating (80) with fresh symbols all_125_0, all_125_1 gives: % 17.68/3.21 | (92) mtvisible(c_currentworlddatacollectormt_nonhomocentric) = all_125_0 & % 17.68/3.21 | mtvisible(c_ldscdemonstrationspindleheadmt) = all_125_1 & ( ~ % 17.68/3.21 | (all_125_1 = 0) | all_125_0 = 0) % 17.68/3.21 | % 17.68/3.21 | ALPHA: (92) implies: % 17.68/3.21 | (93) mtvisible(c_ldscdemonstrationspindleheadmt) = all_125_1 % 17.68/3.21 | (94) mtvisible(c_currentworlddatacollectormt_nonhomocentric) = all_125_0 % 17.68/3.21 | (95) ~ (all_125_1 = 0) | all_125_0 = 0 % 17.68/3.21 | % 17.68/3.21 | DELTA: instantiating (83) with fresh symbols all_127_0, all_127_1 gives: % 17.68/3.21 | (96) mtvisible(c_ldscgeneralcollectormt) = all_127_0 & % 17.68/3.21 | mtvisible(c_miptdatabase19681997_termsmt) = all_127_1 & ( ~ (all_127_1 % 17.68/3.21 | = 0) | all_127_0 = 0) % 17.68/3.21 | % 17.68/3.21 | ALPHA: (96) implies: % 17.68/3.21 | (97) mtvisible(c_miptdatabase19681997_termsmt) = all_127_1 % 17.68/3.21 | (98) mtvisible(c_ldscgeneralcollectormt) = all_127_0 % 17.68/3.21 | (99) ~ (all_127_1 = 0) | all_127_0 = 0 % 17.68/3.21 | % 17.68/3.21 | DELTA: instantiating (82) with fresh symbols all_129_0, all_129_1 gives: % 17.68/3.21 | (100) mtvisible(c_miptdatabase19681997_termsmt) = all_129_0 & % 17.68/3.21 | mtvisible(c_machinelearningspindleheadmt) = all_129_1 & ( ~ % 17.68/3.21 | (all_129_1 = 0) | all_129_0 = 0) % 17.68/3.21 | % 17.68/3.21 | ALPHA: (100) implies: % 17.68/3.21 | (101) mtvisible(c_machinelearningspindleheadmt) = all_129_1 % 17.68/3.21 | (102) mtvisible(c_miptdatabase19681997_termsmt) = all_129_0 % 17.68/3.21 | (103) ~ (all_129_1 = 0) | all_129_0 = 0 % 17.68/3.21 | % 17.68/3.21 | DELTA: instantiating (85) with fresh symbols all_131_0, all_131_1 gives: % 17.68/3.21 | (104) mtvisible(all_83_0) = all_131_1 & % 17.68/3.21 | mtvisible(c_machinelearningspindleheadmt) = all_131_0 & ( ~ % 17.68/3.21 | (all_131_1 = 0) | all_131_0 = 0) % 17.68/3.21 | % 17.68/3.21 | ALPHA: (104) implies: % 17.68/3.21 | (105) mtvisible(c_machinelearningspindleheadmt) = all_131_0 % 17.68/3.21 | (106) mtvisible(all_83_0) = all_131_1 % 17.68/3.21 | (107) ~ (all_131_1 = 0) | all_131_0 = 0 % 17.68/3.21 | % 17.68/3.21 | GROUND_INST: instantiating (25) with all_117_0, all_125_1, % 17.68/3.21 | c_ldscdemonstrationspindleheadmt, simplifying with (87), (93) % 17.68/3.21 | gives: % 17.68/3.21 | (108) all_125_1 = all_117_0 % 17.68/3.21 | % 17.68/3.21 | GROUND_INST: instantiating (25) with all_81_2, all_125_0, % 17.68/3.21 | c_currentworlddatacollectormt_nonhomocentric, simplifying with % 17.68/3.21 | (38), (94) gives: % 17.68/3.21 | (109) all_125_0 = all_81_2 % 17.68/3.21 | % 17.68/3.21 | GROUND_INST: instantiating (25) with all_129_1, all_131_0, % 17.68/3.21 | c_machinelearningspindleheadmt, simplifying with (101), (105) % 17.68/3.21 | gives: % 17.68/3.21 | (110) all_131_0 = all_129_1 % 17.68/3.21 | % 17.68/3.21 | GROUND_INST: instantiating (25) with all_121_1, all_131_0, % 17.68/3.21 | c_machinelearningspindleheadmt, simplifying with (91), (105) % 17.68/3.21 | gives: % 17.68/3.21 | (111) all_131_0 = all_121_1 % 17.68/3.21 | % 17.68/3.21 | GROUND_INST: instantiating (25) with all_127_1, all_129_0, % 17.68/3.21 | c_miptdatabase19681997_termsmt, simplifying with (97), (102) % 17.68/3.21 | gives: % 17.68/3.21 | (112) all_129_0 = all_127_1 % 17.68/3.21 | % 17.68/3.21 | GROUND_INST: instantiating (25) with all_117_1, all_127_0, % 17.68/3.21 | c_ldscgeneralcollectormt, simplifying with (88), (98) gives: % 17.68/3.21 | (113) all_127_0 = all_117_1 % 17.68/3.21 | % 17.68/3.22 | GROUND_INST: instantiating (25) with 0, all_131_1, all_83_0, simplifying with % 17.68/3.22 | (78), (106) gives: % 17.68/3.22 | (114) all_131_1 = 0 % 17.68/3.22 | % 17.68/3.22 | COMBINE_EQS: (110), (111) imply: % 17.68/3.22 | (115) all_129_1 = all_121_1 % 17.68/3.22 | % 17.68/3.22 | SIMP: (115) implies: % 17.68/3.22 | (116) all_129_1 = all_121_1 % 17.68/3.22 | % 17.68/3.22 | BETA: splitting (107) gives: % 17.68/3.22 | % 17.68/3.22 | Case 1: % 17.68/3.22 | | % 17.68/3.22 | | (117) ~ (all_131_1 = 0) % 17.68/3.22 | | % 17.68/3.22 | | REDUCE: (114), (117) imply: % 17.68/3.22 | | (118) $false % 17.68/3.22 | | % 17.68/3.22 | | CLOSE: (118) is inconsistent. % 17.68/3.22 | | % 17.68/3.22 | Case 2: % 17.68/3.22 | | % 17.68/3.22 | | (119) all_131_0 = 0 % 17.68/3.22 | | % 17.68/3.22 | | COMBINE_EQS: (111), (119) imply: % 17.68/3.22 | | (120) all_121_1 = 0 % 17.68/3.22 | | % 17.68/3.22 | | COMBINE_EQS: (116), (120) imply: % 17.68/3.22 | | (121) all_129_1 = 0 % 17.68/3.22 | | % 17.68/3.22 | | BETA: splitting (103) gives: % 17.68/3.22 | | % 17.68/3.22 | | Case 1: % 17.68/3.22 | | | % 17.68/3.22 | | | (122) ~ (all_129_1 = 0) % 17.68/3.22 | | | % 17.68/3.22 | | | REDUCE: (121), (122) imply: % 17.68/3.22 | | | (123) $false % 17.68/3.22 | | | % 17.68/3.22 | | | CLOSE: (123) is inconsistent. % 17.68/3.22 | | | % 17.68/3.22 | | Case 2: % 17.68/3.22 | | | % 17.68/3.22 | | | (124) all_129_0 = 0 % 17.68/3.22 | | | % 17.68/3.22 | | | COMBINE_EQS: (112), (124) imply: % 17.68/3.22 | | | (125) all_127_1 = 0 % 17.68/3.22 | | | % 17.68/3.22 | | | SIMP: (125) implies: % 17.68/3.22 | | | (126) all_127_1 = 0 % 17.68/3.22 | | | % 17.68/3.22 | | | BETA: splitting (99) gives: % 17.68/3.22 | | | % 17.68/3.22 | | | Case 1: % 17.68/3.22 | | | | % 17.68/3.22 | | | | (127) ~ (all_127_1 = 0) % 17.68/3.22 | | | | % 17.68/3.22 | | | | REDUCE: (126), (127) imply: % 17.68/3.22 | | | | (128) $false % 17.68/3.22 | | | | % 17.68/3.22 | | | | CLOSE: (128) is inconsistent. % 17.68/3.22 | | | | % 17.68/3.22 | | | Case 2: % 17.68/3.22 | | | | % 17.68/3.22 | | | | (129) all_127_0 = 0 % 17.68/3.22 | | | | % 17.68/3.22 | | | | COMBINE_EQS: (113), (129) imply: % 17.68/3.22 | | | | (130) all_117_1 = 0 % 17.68/3.22 | | | | % 17.68/3.22 | | | | BETA: splitting (89) gives: % 17.68/3.22 | | | | % 17.68/3.22 | | | | Case 1: % 17.68/3.22 | | | | | % 17.68/3.22 | | | | | (131) ~ (all_117_1 = 0) % 17.68/3.22 | | | | | % 17.68/3.22 | | | | | REDUCE: (130), (131) imply: % 17.68/3.22 | | | | | (132) $false % 17.68/3.22 | | | | | % 17.68/3.22 | | | | | CLOSE: (132) is inconsistent. % 17.68/3.22 | | | | | % 17.68/3.22 | | | | Case 2: % 17.68/3.22 | | | | | % 17.68/3.22 | | | | | (133) all_117_0 = 0 % 17.68/3.22 | | | | | % 17.68/3.22 | | | | | COMBINE_EQS: (108), (133) imply: % 17.68/3.22 | | | | | (134) all_125_1 = 0 % 17.68/3.22 | | | | | % 17.68/3.22 | | | | | BETA: splitting (95) gives: % 17.68/3.22 | | | | | % 17.68/3.22 | | | | | Case 1: % 17.68/3.22 | | | | | | % 17.68/3.22 | | | | | | (135) ~ (all_125_1 = 0) % 17.68/3.22 | | | | | | % 17.68/3.22 | | | | | | REDUCE: (134), (135) imply: % 17.68/3.22 | | | | | | (136) $false % 17.68/3.22 | | | | | | % 17.68/3.22 | | | | | | CLOSE: (136) is inconsistent. % 17.68/3.22 | | | | | | % 17.68/3.22 | | | | | Case 2: % 17.68/3.22 | | | | | | % 17.68/3.22 | | | | | | (137) all_125_0 = 0 % 17.68/3.22 | | | | | | % 17.68/3.22 | | | | | | COMBINE_EQS: (109), (137) imply: % 17.68/3.22 | | | | | | (138) all_81_2 = 0 % 17.68/3.22 | | | | | | % 17.68/3.22 | | | | | | SIMP: (138) implies: % 17.68/3.22 | | | | | | (139) all_81_2 = 0 % 17.68/3.22 | | | | | | % 17.68/3.22 | | | | | | COMBINE_EQS: (65), (139) imply: % 17.68/3.22 | | | | | | (140) all_94_1 = 0 % 17.68/3.22 | | | | | | % 17.68/3.22 | | | | | | BETA: splitting (39) gives: % 17.68/3.22 | | | | | | % 17.68/3.22 | | | | | | Case 1: % 17.68/3.22 | | | | | | | % 17.68/3.22 | | | | | | | (141) ~ (all_81_2 = 0) % 17.68/3.22 | | | | | | | % 17.68/3.22 | | | | | | | REDUCE: (139), (141) imply: % 17.68/3.22 | | | | | | | (142) $false % 17.68/3.22 | | | | | | | % 17.68/3.22 | | | | | | | CLOSE: (142) is inconsistent. % 17.68/3.22 | | | | | | | % 17.68/3.22 | | | | | | Case 2: % 17.68/3.22 | | | | | | | % 17.68/3.22 | | | | | | | (143) all_81_0 = 0 % 17.68/3.22 | | | | | | | % 17.68/3.22 | | | | | | | REDUCE: (72), (143) imply: % 17.68/3.22 | | | | | | | (144) relationexistsall(c_tptp_9_51, c_tptpcol_16_27189, % 17.68/3.22 | | | | | | | all_79_0) = 0 % 17.68/3.22 | | | | | | | % 17.68/3.22 | | | | | | | GROUND_INST: instantiating (59) with % 17.68/3.22 | | | | | | | c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 17.68/3.22 | | | | | | | simplifying with (21) gives: % 17.68/3.22 | | | | | | | (145) ~ (all_94_1 = 0) | ~ % 17.68/3.22 | | | | | | | (isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 17.68/3.22 | | | | | | | all_94_0) = 0) | ? [v0: $i] : (tptp_9_51(v0, % 17.68/3.22 | | | | | | | c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 17.68/3.22 | | | | | | | = 0 & % 17.68/3.22 | | | | | | | f_relationexistsallfn(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 17.68/3.22 | | | | | | | c_tptp_9_51, c_tptpcol_16_27189, all_94_0) = v0 & % 17.68/3.22 | | | | | | | $i(v0)) % 17.68/3.22 | | | | | | | % 17.68/3.22 | | | | | | | BETA: splitting (145) gives: % 17.68/3.22 | | | | | | | % 17.68/3.22 | | | | | | | Case 1: % 17.68/3.22 | | | | | | | | % 17.68/3.22 | | | | | | | | (146) ~ % 17.68/3.22 | | | | | | | | (isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 17.68/3.22 | | | | | | | | all_94_0) = 0) % 17.68/3.22 | | | | | | | | % 17.68/3.22 | | | | | | | | REDUCE: (71), (146) imply: % 17.68/3.22 | | | | | | | | (147) ~ % 17.68/3.22 | | | | | | | | (isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 17.68/3.22 | | | | | | | | all_79_0) = 0) % 17.68/3.22 | | | | | | | | % 17.68/3.22 | | | | | | | | PRED_UNIFY: (32), (147) imply: % 17.68/3.22 | | | | | | | | (148) $false % 17.68/3.22 | | | | | | | | % 17.68/3.22 | | | | | | | | CLOSE: (148) is inconsistent. % 17.68/3.22 | | | | | | | | % 17.68/3.22 | | | | | | | Case 2: % 17.68/3.22 | | | | | | | | % 17.68/3.22 | | | | | | | | (149) isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 17.68/3.22 | | | | | | | | all_94_0) = 0 % 17.68/3.22 | | | | | | | | (150) ~ (all_94_1 = 0) | ? [v0: $i] : (tptp_9_51(v0, % 17.68/3.22 | | | | | | | | c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 17.68/3.22 | | | | | | | | = 0 & % 17.68/3.22 | | | | | | | | f_relationexistsallfn(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 17.68/3.22 | | | | | | | | c_tptp_9_51, c_tptpcol_16_27189, all_94_0) = v0 & % 17.68/3.22 | | | | | | | | $i(v0)) % 17.68/3.22 | | | | | | | | % 17.68/3.22 | | | | | | | | BETA: splitting (150) gives: % 17.68/3.22 | | | | | | | | % 17.68/3.22 | | | | | | | | Case 1: % 17.68/3.22 | | | | | | | | | % 17.68/3.22 | | | | | | | | | (151) ~ (all_94_1 = 0) % 17.68/3.22 | | | | | | | | | % 17.68/3.22 | | | | | | | | | REDUCE: (140), (151) imply: % 17.68/3.22 | | | | | | | | | (152) $false % 17.68/3.22 | | | | | | | | | % 17.68/3.22 | | | | | | | | | CLOSE: (152) is inconsistent. % 17.68/3.22 | | | | | | | | | % 17.68/3.22 | | | | | | | | Case 2: % 17.68/3.22 | | | | | | | | | % 17.68/3.22 | | | | | | | | | (153) ? [v0: $i] : (tptp_9_51(v0, % 17.68/3.22 | | | | | | | | | c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 17.68/3.22 | | | | | | | | | = 0 & % 17.68/3.22 | | | | | | | | | f_relationexistsallfn(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 17.68/3.22 | | | | | | | | | c_tptp_9_51, c_tptpcol_16_27189, all_94_0) = v0 & % 17.68/3.22 | | | | | | | | | $i(v0)) % 17.68/3.22 | | | | | | | | | % 17.68/3.22 | | | | | | | | | DELTA: instantiating (153) with fresh symbol all_207_0 gives: % 17.68/3.22 | | | | | | | | | (154) tptp_9_51(all_207_0, % 17.68/3.22 | | | | | | | | | c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 17.68/3.22 | | | | | | | | | = 0 & % 17.68/3.22 | | | | | | | | | f_relationexistsallfn(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 17.68/3.22 | | | | | | | | | c_tptp_9_51, c_tptpcol_16_27189, all_94_0) = % 17.68/3.22 | | | | | | | | | all_207_0 & $i(all_207_0) % 17.68/3.22 | | | | | | | | | % 17.68/3.22 | | | | | | | | | ALPHA: (154) implies: % 17.68/3.22 | | | | | | | | | (155) $i(all_207_0) % 17.68/3.22 | | | | | | | | | (156) f_relationexistsallfn(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 17.68/3.23 | | | | | | | | | c_tptp_9_51, c_tptpcol_16_27189, all_94_0) = % 17.68/3.23 | | | | | | | | | all_207_0 % 17.68/3.23 | | | | | | | | | (157) tptp_9_51(all_207_0, % 17.68/3.23 | | | | | | | | | c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) % 17.68/3.23 | | | | | | | | | = 0 % 17.68/3.23 | | | | | | | | | % 17.68/3.23 | | | | | | | | | REDUCE: (71), (156) imply: % 17.68/3.23 | | | | | | | | | (158) f_relationexistsallfn(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 17.68/3.23 | | | | | | | | | c_tptp_9_51, c_tptpcol_16_27189, all_79_0) = % 17.68/3.23 | | | | | | | | | all_207_0 % 17.68/3.23 | | | | | | | | | % 17.68/3.23 | | | | | | | | | GROUND_INST: instantiating (just6) with % 17.68/3.23 | | | | | | | | | c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 17.68/3.23 | | | | | | | | | all_79_0, c_tptp_9_51, c_tptpcol_16_27189, % 17.68/3.23 | | | | | | | | | all_207_0, simplifying with (14), (20), (21), % 17.68/3.23 | | | | | | | | | (74), (158) gives: % 17.68/3.23 | | | | | | | | | (159) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 17.68/3.23 | | | | | | | | | (relationexistsall(c_tptp_9_51, c_tptpcol_16_27189, % 17.68/3.23 | | | | | | | | | all_79_0) = v1 & isa(all_207_0, % 17.68/3.23 | | | | | | | | | c_tptpcol_16_27189) = v2 & % 17.68/3.23 | | | | | | | | | isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 17.68/3.23 | | | | | | | | | all_79_0) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 % 17.68/3.23 | | | | | | | | | = 0)) % 17.68/3.23 | | | | | | | | | % 17.68/3.23 | | | | | | | | | GROUND_INST: instantiating (55) with all_207_0, simplifying % 17.68/3.23 | | | | | | | | | with (155), (157) gives: % 17.68/3.23 | | | | | | | | | (160) ? [v0: int] : ( ~ (v0 = 0) & % 17.68/3.23 | | | | | | | | | tptpcol_16_27189(all_207_0) = v0) % 17.68/3.23 | | | | | | | | | % 17.68/3.23 | | | | | | | | | DELTA: instantiating (160) with fresh symbol all_215_0 gives: % 17.68/3.23 | | | | | | | | | (161) ~ (all_215_0 = 0) & tptpcol_16_27189(all_207_0) = % 17.68/3.23 | | | | | | | | | all_215_0 % 17.68/3.23 | | | | | | | | | % 17.68/3.23 | | | | | | | | | ALPHA: (161) implies: % 17.68/3.23 | | | | | | | | | (162) ~ (all_215_0 = 0) % 18.30/3.23 | | | | | | | | | (163) tptpcol_16_27189(all_207_0) = all_215_0 % 18.30/3.23 | | | | | | | | | % 18.30/3.23 | | | | | | | | | DELTA: instantiating (159) with fresh symbols all_217_0, % 18.30/3.23 | | | | | | | | | all_217_1, all_217_2 gives: % 18.30/3.23 | | | | | | | | | (164) relationexistsall(c_tptp_9_51, c_tptpcol_16_27189, % 18.30/3.23 | | | | | | | | | all_79_0) = all_217_1 & isa(all_207_0, % 18.30/3.23 | | | | | | | | | c_tptpcol_16_27189) = all_217_0 & % 18.30/3.23 | | | | | | | | | isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 18.30/3.23 | | | | | | | | | all_79_0) = all_217_2 & ( ~ (all_217_1 = 0) | ~ % 18.30/3.23 | | | | | | | | | (all_217_2 = 0) | all_217_0 = 0) % 18.30/3.23 | | | | | | | | | % 18.30/3.23 | | | | | | | | | ALPHA: (164) implies: % 18.30/3.23 | | | | | | | | | (165) isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 18.30/3.23 | | | | | | | | | all_79_0) = all_217_2 % 18.30/3.23 | | | | | | | | | (166) isa(all_207_0, c_tptpcol_16_27189) = all_217_0 % 18.30/3.23 | | | | | | | | | (167) relationexistsall(c_tptp_9_51, c_tptpcol_16_27189, % 18.30/3.23 | | | | | | | | | all_79_0) = all_217_1 % 18.30/3.23 | | | | | | | | | (168) ~ (all_217_1 = 0) | ~ (all_217_2 = 0) | all_217_0 = % 18.30/3.23 | | | | | | | | | 0 % 18.30/3.23 | | | | | | | | | % 18.30/3.23 | | | | | | | | | GROUND_INST: instantiating (28) with 0, all_217_2, all_79_0, % 18.30/3.23 | | | | | | | | | c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802, % 18.30/3.23 | | | | | | | | | simplifying with (32), (165) gives: % 18.30/3.23 | | | | | | | | | (169) all_217_2 = 0 % 18.30/3.23 | | | | | | | | | % 18.30/3.23 | | | | | | | | | GROUND_INST: instantiating (29) with 0, all_217_1, all_79_0, % 18.30/3.23 | | | | | | | | | c_tptpcol_16_27189, c_tptp_9_51, simplifying with % 18.30/3.23 | | | | | | | | | (144), (167) gives: % 18.30/3.23 | | | | | | | | | (170) all_217_1 = 0 % 18.30/3.23 | | | | | | | | | % 18.30/3.23 | | | | | | | | | BETA: splitting (168) gives: % 18.30/3.23 | | | | | | | | | % 18.30/3.23 | | | | | | | | | Case 1: % 18.30/3.23 | | | | | | | | | | % 18.30/3.23 | | | | | | | | | | (171) ~ (all_217_1 = 0) % 18.30/3.23 | | | | | | | | | | % 18.30/3.23 | | | | | | | | | | REDUCE: (170), (171) imply: % 18.30/3.23 | | | | | | | | | | (172) $false % 18.30/3.23 | | | | | | | | | | % 18.30/3.23 | | | | | | | | | | CLOSE: (172) is inconsistent. % 18.30/3.23 | | | | | | | | | | % 18.30/3.23 | | | | | | | | | Case 2: % 18.30/3.23 | | | | | | | | | | % 18.30/3.23 | | | | | | | | | | (173) ~ (all_217_2 = 0) | all_217_0 = 0 % 18.30/3.23 | | | | | | | | | | % 18.30/3.23 | | | | | | | | | | BETA: splitting (173) gives: % 18.30/3.23 | | | | | | | | | | % 18.30/3.23 | | | | | | | | | | Case 1: % 18.30/3.23 | | | | | | | | | | | % 18.30/3.23 | | | | | | | | | | | (174) ~ (all_217_2 = 0) % 18.30/3.23 | | | | | | | | | | | % 18.30/3.23 | | | | | | | | | | | REDUCE: (169), (174) imply: % 18.30/3.23 | | | | | | | | | | | (175) $false % 18.30/3.23 | | | | | | | | | | | % 18.30/3.23 | | | | | | | | | | | CLOSE: (175) is inconsistent. % 18.30/3.23 | | | | | | | | | | | % 18.30/3.23 | | | | | | | | | | Case 2: % 18.30/3.23 | | | | | | | | | | | % 18.30/3.23 | | | | | | | | | | | (176) all_217_0 = 0 % 18.30/3.23 | | | | | | | | | | | % 18.30/3.23 | | | | | | | | | | | REDUCE: (166), (176) imply: % 18.30/3.23 | | | | | | | | | | | (177) isa(all_207_0, c_tptpcol_16_27189) = 0 % 18.30/3.23 | | | | | | | | | | | % 18.30/3.23 | | | | | | | | | | | GROUND_INST: instantiating (19) with all_207_0, simplifying % 18.30/3.23 | | | | | | | | | | | with (155), (177) gives: % 18.30/3.23 | | | | | | | | | | | (178) tptpcol_16_27189(all_207_0) = 0 % 18.30/3.23 | | | | | | | | | | | % 18.30/3.23 | | | | | | | | | | | GROUND_INST: instantiating (26) with all_215_0, 0, all_207_0, % 18.30/3.23 | | | | | | | | | | | simplifying with (163), (178) gives: % 18.30/3.23 | | | | | | | | | | | (179) all_215_0 = 0 % 18.30/3.23 | | | | | | | | | | | % 18.30/3.23 | | | | | | | | | | | REDUCE: (162), (179) imply: % 18.30/3.23 | | | | | | | | | | | (180) $false % 18.30/3.23 | | | | | | | | | | | % 18.30/3.23 | | | | | | | | | | | CLOSE: (180) is inconsistent. % 18.30/3.23 | | | | | | | | | | | % 18.30/3.23 | | | | | | | | | | End of split % 18.30/3.23 | | | | | | | | | | % 18.30/3.23 | | | | | | | | | End of split % 18.30/3.23 | | | | | | | | | % 18.30/3.23 | | | | | | | | End of split % 18.30/3.23 | | | | | | | | % 18.30/3.23 | | | | | | | End of split % 18.30/3.23 | | | | | | | % 18.30/3.23 | | | | | | End of split % 18.30/3.23 | | | | | | % 18.30/3.23 | | | | | End of split % 18.30/3.23 | | | | | % 18.30/3.23 | | | | End of split % 18.30/3.23 | | | | % 18.30/3.23 | | | End of split % 18.30/3.23 | | | % 18.30/3.23 | | End of split % 18.30/3.23 | | % 18.30/3.23 | End of split % 18.30/3.23 | % 18.30/3.23 End of proof % 18.30/3.23 % SZS output end Proof for theBenchmark % 18.30/3.23 % 18.30/3.23 2636ms %------------------------------------------------------------------------------