%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : CSR074+2 : TPTP v8.1.2. Released v3.4.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n021.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:14 EDT 2023 % Result : Theorem 85.33s 12.03s % Output : Proof 86.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.14 % Problem : CSR074+2 : TPTP v8.1.2. Released v3.4.0. % 0.00/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.35 % Computer : n021.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 300 % 0.14/0.36 % DateTime : Mon Aug 28 07:46:13 EDT 2023 % 0.14/0.36 % CPUTime : % 0.21/0.63 ________ _____ % 0.21/0.63 ___ __ \_________(_)________________________________ % 0.21/0.63 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.21/0.63 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.21/0.63 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.21/0.63 % 0.21/0.63 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.21/0.63 (2023-06-19) % 0.21/0.63 % 0.21/0.63 (c) Philipp Rümmer, 2009-2023 % 0.21/0.63 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.21/0.63 Amanda Stjerna. % 0.21/0.63 Free software under BSD-3-Clause. % 0.21/0.63 % 0.21/0.63 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.21/0.63 % 0.21/0.63 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.21/0.64 Running up to 7 provers in parallel. % 0.21/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.21/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.21/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.21/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.21/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.21/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.21/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 10.99/2.26 Prover 1: Preprocessing ... % 10.99/2.27 Prover 4: Preprocessing ... % 11.52/2.30 Prover 2: Preprocessing ... % 11.52/2.30 Prover 3: Preprocessing ... % 11.52/2.30 Prover 6: Preprocessing ... % 11.52/2.30 Prover 0: Preprocessing ... % 11.52/2.30 Prover 5: Preprocessing ... % 28.23/4.58 Prover 6: Constructing countermodel ... % 28.81/4.63 Prover 3: Constructing countermodel ... % 28.81/4.66 Prover 5: Proving ... % 28.81/4.71 Prover 2: Proving ... % 29.76/4.78 Prover 1: Constructing countermodel ... % 35.44/5.53 Prover 4: Constructing countermodel ... % 39.36/6.16 Prover 0: Proving ... % 84.91/12.02 Prover 4: Found proof (size 144) % 84.91/12.03 Prover 4: proved (11373ms) % 84.91/12.03 Prover 5: stopped % 84.91/12.03 Prover 6: stopped % 84.91/12.03 Prover 3: stopped % 85.33/12.03 Prover 2: stopped % 85.33/12.03 Prover 1: stopped % 85.33/12.03 Prover 0: stopped % 85.33/12.03 % 85.33/12.03 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 85.33/12.03 % 85.33/12.06 % SZS output start Proof for theBenchmark % 85.33/12.08 Assumptions after simplification: % 85.33/12.08 --------------------------------- % 85.33/12.08 % 85.33/12.08 (ax1_1) % 85.33/12.11 genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt) = 0 & % 85.33/12.11 $i(c_tptpgeo_spindleheadmt) & $i(c_tptpgeo_member8_mt) % 85.33/12.11 % 85.33/12.11 (ax1_1123) % 85.33/12.11 ! [v0: $i] : ! [v1: $i] : ( ~ (genlmt(v0, v1) = 0) | ~ $i(v1) | ~ $i(v0) | % 85.33/12.11 ? [v2: any] : ? [v3: any] : (mtvisible(v1) = v3 & mtvisible(v0) = v2 & ( ~ % 85.33/12.11 (v2 = 0) | v3 = 0))) % 85.33/12.11 % 85.33/12.11 (ax1_121) % 85.33/12.11 $i(c_georegion_l3_x4_y13) & $i(c_worldgeographymt) & ? [v0: any] : ? [v1: % 85.33/12.11 any] : (geolevel_3(c_georegion_l3_x4_y13) = v1 & % 85.33/12.11 mtvisible(c_worldgeographymt) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 85.33/12.11 % 85.33/12.11 (ax1_122) % 85.33/12.11 $i(c_georegion_l4_x27_y65) & $i(c_georegion_l4_x27_y64) & % 85.33/12.11 $i(c_tptpgeo_member7_mt) & ? [v0: any] : ? [v1: any] : % 85.33/12.11 (borderson(c_georegion_l4_x27_y64, c_georegion_l4_x27_y65) = v1 & % 85.33/12.11 mtvisible(c_tptpgeo_member7_mt) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 85.33/12.11 % 85.33/12.12 (ax1_128) % 85.33/12.12 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (inregion(v1, v0) = % 85.33/12.12 v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: int] : ( ~ (v3 = 0) & % 85.33/12.12 geographicalsubregions(v0, v1) = v3)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 85.33/12.12 (geographicalsubregions(v0, v1) = 0) | ~ $i(v1) | ~ $i(v0) | inregion(v1, % 85.33/12.12 v0) = 0) % 85.33/12.12 % 85.33/12.12 (ax1_188) % 85.33/12.12 $i(c_georegion_l4_x45_y72) & $i(c_georegion_l3_x15_y24) & % 85.33/12.12 $i(c_tptpgeo_member7_mt) & ? [v0: any] : ? [v1: any] : % 85.33/12.12 (mtvisible(c_tptpgeo_member7_mt) = v0 & % 85.33/12.12 geographicalsubregions(c_georegion_l3_x15_y24, c_georegion_l4_x45_y72) = v1 % 85.33/12.12 & ( ~ (v0 = 0) | v1 = 0)) % 85.33/12.12 % 85.33/12.12 (ax1_212) % 85.33/12.12 genlmt(c_tptpgeo_member3_mt, c_tptpgeo_spindleheadmt) = 0 & % 85.33/12.12 $i(c_tptpgeo_member3_mt) & $i(c_tptpgeo_spindleheadmt) % 85.33/12.12 % 85.33/12.12 (ax1_276) % 85.33/12.12 $i(c_georegion_l2_x5_y8) & $i(c_georegion_l3_x15_y24) & % 85.33/12.12 $i(c_tptpgeo_member7_mt) & ? [v0: any] : ? [v1: any] : % 85.33/12.12 (mtvisible(c_tptpgeo_member7_mt) = v0 & % 85.33/12.12 geographicalsubregions(c_georegion_l2_x5_y8, c_georegion_l3_x15_y24) = v1 & % 85.33/12.12 ( ~ (v0 = 0) | v1 = 0)) % 85.33/12.12 % 85.33/12.12 (ax1_292) % 85.33/12.12 $i(c_worldgeographymt) & $i(c_georegion_l1_x2_y0) & ? [v0: any] : ? [v1: % 85.33/12.12 any] : (geolevel_1(c_georegion_l1_x2_y0) = v1 & % 85.33/12.12 mtvisible(c_worldgeographymt) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 85.33/12.12 % 85.33/12.12 (ax1_321) % 85.33/12.12 $i(c_wanica_districtsuriname) & $i(c_worldgeographymt) & ? [v0: any] : ? % 85.33/12.12 [v1: any] : (state_geopolitical(c_wanica_districtsuriname) = v1 & % 85.33/12.12 mtvisible(c_worldgeographymt) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 85.33/12.12 % 85.33/12.12 (ax1_326) % 85.33/12.12 genlmt(c_tptpgeo_spindleheadmt, c_worldgeographymt) = 0 & % 85.33/12.12 $i(c_worldgeographymt) & $i(c_tptpgeo_spindleheadmt) % 85.33/12.12 % 85.33/12.12 (ax1_334) % 85.33/12.12 genlmt(c_worldgeographymt, c_geographymt) = 0 & $i(c_geographymt) & % 85.33/12.12 $i(c_worldgeographymt) % 85.33/12.12 % 85.33/12.12 (ax1_337) % 85.33/12.13 $i(c_georegion_l4_x14_y39) & $i(c_tptpgeo_member3_mt) & % 85.33/12.13 $i(c_georegion_l3_x4_y13) & ? [v0: any] : ? [v1: any] : % 85.33/12.13 (mtvisible(c_tptpgeo_member3_mt) = v0 & % 85.33/12.13 geographicalsubregions(c_georegion_l3_x4_y13, c_georegion_l4_x14_y39) = v1 & % 85.33/12.13 ( ~ (v0 = 0) | v1 = 0)) % 85.33/12.13 % 85.33/12.13 (ax1_369) % 85.33/12.13 genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member8_mt) = 0 & % 85.33/12.13 $i(c_tptpgeo_spindlecollectormt) & $i(c_tptpgeo_member8_mt) % 85.33/12.13 % 85.33/12.13 (ax1_464) % 85.33/12.13 $i(c_georegion_l4_x75_y75) & $i(c_worldgeographymt) & ? [v0: any] : ? [v1: % 85.33/12.13 any] : (geolevel_4(c_georegion_l4_x75_y75) = v1 & % 85.33/12.13 mtvisible(c_worldgeographymt) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 85.33/12.13 % 85.33/12.13 (ax1_472) % 85.33/12.13 $i(c_georegion_l3_x17_y24) & $i(c_georegion_l4_x53_y74) & % 85.33/12.13 $i(c_tptpgeo_member7_mt) & ? [v0: any] : ? [v1: any] : % 85.33/12.13 (mtvisible(c_tptpgeo_member7_mt) = v0 & % 85.33/12.13 geographicalsubregions(c_georegion_l3_x17_y24, c_georegion_l4_x53_y74) = v1 % 85.33/12.13 & ( ~ (v0 = 0) | v1 = 0)) % 85.33/12.13 % 85.33/12.13 (ax1_478) % 85.79/12.13 $i(c_georegion_l3_x17_y24) & $i(c_worldgeographymt) & ? [v0: any] : ? [v1: % 85.79/12.13 any] : (geolevel_3(c_georegion_l3_x17_y24) = v1 & % 85.79/12.13 mtvisible(c_worldgeographymt) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 85.79/12.13 % 85.79/12.13 (ax1_485) % 85.79/12.13 $i(c_georegion_l4_x29_y76) & $i(c_georegion_l4_x29_y75) & % 85.79/12.13 $i(c_tptpgeo_member7_mt) & ? [v0: any] : ? [v1: any] : % 85.79/12.13 (borderson(c_georegion_l4_x29_y75, c_georegion_l4_x29_y76) = v1 & % 85.79/12.13 mtvisible(c_tptpgeo_member7_mt) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 85.79/12.13 % 85.79/12.13 (ax1_63) % 85.79/12.13 genlmt(c_tptpgeo_member7_mt, c_tptpgeo_spindleheadmt) = 0 & % 85.79/12.13 $i(c_tptpgeo_member7_mt) & $i(c_tptpgeo_spindleheadmt) % 85.79/12.13 % 85.79/12.13 (ax1_82) % 85.79/12.13 $i(c_georegion_l4_x53_y74) & $i(c_geolocation_x53_y74) & % 85.79/12.13 $i(c_tptpgeo_member7_mt) & ? [v0: any] : ? [v1: any] : % 85.79/12.13 (inregion(c_geolocation_x53_y74, c_georegion_l4_x53_y74) = v1 & % 85.79/12.13 mtvisible(c_tptpgeo_member7_mt) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 85.79/12.13 % 85.79/12.13 (ax1_933) % 85.79/12.13 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 85.79/12.13 (inregion(v1, v2) = 0) | ~ (inregion(v0, v2) = v3) | ~ $i(v2) | ~ $i(v1) % 85.79/12.13 | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & inregion(v0, v1) = v4)) & ! % 85.79/12.13 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 85.79/12.13 (inregion(v0, v2) = v3) | ~ (inregion(v0, v1) = 0) | ~ $i(v2) | ~ $i(v1) % 85.79/12.13 | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & inregion(v1, v2) = v4)) & ! % 85.79/12.13 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (inregion(v1, v2) = 0) | ~ % 85.79/12.13 (inregion(v0, v1) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | inregion(v0, % 85.79/12.13 v2) = 0) % 85.79/12.13 % 85.79/12.13 (query124) % 85.79/12.14 $i(c_georegion_l3_x17_y24) & $i(c_geolocation_x53_y74) & % 85.79/12.14 $i(c_tptpgeo_member7_mt) & ? [v0: any] : ? [v1: any] : % 85.79/12.14 (geolevel_3(c_georegion_l3_x17_y24) = v1 & inregion(c_geolocation_x53_y74, % 85.79/12.14 c_georegion_l3_x17_y24) = v0 & mtvisible(c_tptpgeo_member7_mt) = 0 & ( ~ % 85.79/12.14 (v1 = 0) | ~ (v0 = 0))) % 85.79/12.14 % 85.79/12.14 (function-axioms) % 86.11/12.21 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 86.11/12.21 $i] : (v1 = v0 | ~ (f_relationallexistsfn(v5, v4, v3, v2) = v1) | ~ % 86.11/12.21 (f_relationallexistsfn(v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 86.11/12.21 ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ % 86.11/12.21 (f_relationexistsallfn(v5, v4, v3, v2) = v1) | ~ (f_relationexistsallfn(v5, % 86.11/12.21 v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 86.11/12.21 (natargument(v4, v3, v2) = v1) | ~ (natargument(v4, v3, v2) = v0)) & ! % 86.11/12.21 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | % 86.11/12.21 ~ (f_subcollectionofwithrelationtofn(v4, v3, v2) = v1) | ~ % 86.11/12.21 (f_subcollectionofwithrelationtofn(v4, v3, v2) = v0)) & ! [v0: $i] : ! % 86.11/12.21 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 86.11/12.21 (f_instancewithrelationtofn(v4, v3, v2) = v1) | ~ % 86.11/12.21 (f_instancewithrelationtofn(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] % 86.11/12.21 : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = % 86.11/12.21 v0 | ~ (relationallexists(v4, v3, v2) = v1) | ~ (relationallexists(v4, v3, % 86.11/12.21 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 86.11/12.21 [v4: $i] : (v1 = v0 | ~ (f_subcollectionofwithrelationtotypefn(v4, v3, v2) = % 86.11/12.21 v1) | ~ (f_subcollectionofwithrelationtotypefn(v4, v3, v2) = v0)) & ! % 86.11/12.21 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | % 86.11/12.21 ~ (f_subcollectionofwithrelationfromtypefn(v4, v3, v2) = v1) | ~ % 86.11/12.21 (f_subcollectionofwithrelationfromtypefn(v4, v3, v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 86.11/12.21 : ! [v4: $i] : (v1 = v0 | ~ (relationallinstance(v4, v3, v2) = v1) | ~ % 86.11/12.21 (relationallinstance(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | % 86.11/12.21 ~ (relationexistsall(v4, v3, v2) = v1) | ~ (relationexistsall(v4, v3, v2) % 86.11/12.21 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : ! [v3: $i] : (v1 = v0 | ~ (hasmembers(v3, v2) = v1) | ~ % 86.11/12.21 (hasmembers(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (products(v3, % 86.11/12.21 v2) = v1) | ~ (products(v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 86.11/12.21 ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 86.11/12.21 (subevents(v3, v2) = v1) | ~ (subevents(v3, v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 86.11/12.21 : (v1 = v0 | ~ (directionoftranslation_throughout(v3, v2) = v1) | ~ % 86.11/12.21 (directionoftranslation_throughout(v3, v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 86.11/12.21 : (v1 = v0 | ~ (orientation(v3, v2) = v1) | ~ (orientation(v3, v2) = v0)) & % 86.11/12.21 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 86.11/12.21 $i] : (v1 = v0 | ~ (airporthasiatacode(v3, v2) = v1) | ~ % 86.11/12.21 (airporthasiatacode(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 86.11/12.21 (subregions(v3, v2) = v1) | ~ (subregions(v3, v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 86.11/12.21 : (v1 = v0 | ~ (geographicallysubsumes(v3, v2) = v1) | ~ % 86.11/12.21 (geographicallysubsumes(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 86.11/12.21 (geopoliticalsubdivision(v3, v2) = v1) | ~ (geopoliticalsubdivision(v3, v2) % 86.11/12.21 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : ! [v3: $i] : (v1 = v0 | ~ (objectfoundinlocation(v3, v2) = v1) | ~ % 86.11/12.21 (objectfoundinlocation(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 86.11/12.21 (affiliatedwith(v3, v2) = v1) | ~ (affiliatedwith(v3, v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 86.11/12.21 : (v1 = v0 | ~ (natfunction(v3, v2) = v1) | ~ (natfunction(v3, v2) = v0)) & % 86.11/12.21 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptptypes_5_802(v3, v2) = v1) | ~ (tptptypes_5_802(v3, % 86.11/12.21 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 86.11/12.21 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (tptp_8_271(v3, v2) = v1) | ~ % 86.11/12.21 (tptp_8_271(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (few(v3, v2) % 86.11/12.21 = v1) | ~ (few(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 86.11/12.21 ! [v3: $i] : (v1 = v0 | ~ (f_citynamedfn(v3, v2) = v1) | ~ % 86.11/12.21 (f_citynamedfn(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 86.11/12.21 (tptp_9_51(v3, v2) = v1) | ~ (tptp_9_51(v3, v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 86.11/12.21 : (v1 = v0 | ~ (arg2isa(v3, v2) = v1) | ~ (arg2isa(v3, v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 86.11/12.21 : (v1 = v0 | ~ (tptptypes_8_823(v3, v2) = v1) | ~ (tptptypes_8_823(v3, v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : ! [v3: $i] : (v1 = v0 | ~ (tptp_8_968(v3, v2) = v1) | ~ % 86.11/12.21 (tptp_8_968(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (arg1isa(v3, % 86.11/12.21 v2) = v1) | ~ (arg1isa(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (no(v3, % 86.11/12.21 v2) = v1) | ~ (no(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 86.11/12.21 (tptptypes_9_824(v3, v2) = v1) | ~ (tptptypes_9_824(v3, v2) = v0)) & ! % 86.11/12.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptptypes_7_396(v3, v2) = v1) | ~ (tptptypes_7_396(v3, % 86.11/12.21 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 86.11/12.21 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (tptp_9_720(v3, v2) = v1) | ~ % 86.11/12.21 (tptp_9_720(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 86.11/12.21 (tptp_8_875(v3, v2) = v1) | ~ (tptp_8_875(v3, v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 86.11/12.21 : (v1 = v0 | ~ (tptptypes_7_691(v3, v2) = v1) | ~ (tptptypes_7_691(v3, v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : ! [v3: $i] : (v1 = v0 | ~ (tptptypes_6_818(v3, v2) = v1) | ~ % 86.11/12.21 (tptptypes_6_818(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 86.11/12.21 (tptptypes_7_819(v3, v2) = v1) | ~ (tptptypes_7_819(v3, v2) = v0)) & ! % 86.11/12.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 86.11/12.21 $i] : (v1 = v0 | ~ (prettystring(v3, v2) = v1) | ~ (prettystring(v3, v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : ! [v3: $i] : (v1 = v0 | ~ (tptptypes_8_400(v3, v2) = v1) | ~ % 86.11/12.21 (tptptypes_8_400(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 86.11/12.21 (tptptypes_9_401(v3, v2) = v1) | ~ (tptptypes_9_401(v3, v2) = v0)) & ! % 86.11/12.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 86.11/12.21 $i] : (v1 = v0 | ~ (borderson(v3, v2) = v1) | ~ (borderson(v3, v2) = v0)) % 86.11/12.21 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 86.11/12.21 [v3: $i] : (v1 = v0 | ~ (tptptypes_5_387(v3, v2) = v1) | ~ % 86.11/12.21 (tptptypes_5_387(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 86.11/12.21 (tptptypes_6_388(v3, v2) = v1) | ~ (tptptypes_6_388(v3, v2) = v0)) & ! % 86.11/12.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 86.11/12.21 $i] : (v1 = v0 | ~ (inregion(v3, v2) = v1) | ~ (inregion(v3, v2) = v0)) & % 86.11/12.21 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpofobject(v3, v2) = v1) | ~ (tptpofobject(v3, v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : ! [v3: $i] : (v1 = v0 | ~ (resultisaarg(v3, v2) = v1) | ~ % 86.11/12.21 (resultisaarg(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (isa(v3, v2) % 86.11/12.21 = v1) | ~ (isa(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 86.11/12.21 (tptptypes_7_389(v3, v2) = v1) | ~ (tptptypes_7_389(v3, v2) = v0)) & ! % 86.11/12.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptptypes_8_390(v3, v2) = v1) | ~ (tptptypes_8_390(v3, % 86.11/12.21 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 86.11/12.21 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (tptptypes_8_692(v3, v2) = v1) | ~ % 86.11/12.21 (tptptypes_8_692(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 86.11/12.21 (tptptypes_9_693(v3, v2) = v1) | ~ (tptptypes_9_693(v3, v2) = v0)) & ! % 86.11/12.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 86.11/12.21 $i] : (v1 = v0 | ~ (geographicalsubregions(v3, v2) = v1) | ~ % 86.11/12.21 (geographicalsubregions(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (most(v3, % 86.11/12.21 v2) = v1) | ~ (most(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 86.11/12.21 (subsetof(v3, v2) = v1) | ~ (subsetof(v3, v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 86.11/12.21 : (v1 = v0 | ~ (genlpreds(v3, v2) = v1) | ~ (genlpreds(v3, v2) = v0)) & ! % 86.11/12.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 86.11/12.21 $i] : (v1 = v0 | ~ (genlinverse(v3, v2) = v1) | ~ (genlinverse(v3, v2) = % 86.11/12.21 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 86.11/12.21 ~ (f_contentmtofcdafromeventfn(v3, v2) = v1) | ~ % 86.11/12.21 (f_contentmtofcdafromeventfn(v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 86.11/12.21 ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 86.11/12.21 (genls(v3, v2) = v1) | ~ (genls(v3, v2) = v0)) & ! [v0: MultipleValueBool] % 86.11/12.21 : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 86.11/12.21 (disjointwith(v3, v2) = v1) | ~ (disjointwith(v3, v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 86.11/12.21 : (v1 = v0 | ~ (genlmt(v3, v2) = v1) | ~ (genlmt(v3, v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (uniformresourcelocator(v2) = v1) | ~ (uniformresourcelocator(v2) = v0)) % 86.11/12.21 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 % 86.11/12.21 = v0 | ~ (predicate(v2) = v1) | ~ (predicate(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (function_denotational(v2) = v1) | ~ (function_denotational(v2) = v0)) & % 86.11/12.21 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = % 86.11/12.21 v0 | ~ (positiveinteger(v2) = v1) | ~ (positiveinteger(v2) = v0)) & ! % 86.11/12.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 86.11/12.21 | ~ (controlcharacterfreestring(v2) = v1) | ~ % 86.11/12.21 (controlcharacterfreestring(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ % 86.11/12.21 (subcollectionofwithrelationfromtypefnterroristhasmembersterroristgroup(v2) % 86.11/12.21 = v1) | ~ % 86.11/12.21 (subcollectionofwithrelationfromtypefnterroristhasmembersterroristgroup(v2) % 86.11/12.21 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (terrorist(v2) = v1) | ~ (terrorist(v2) = v0)) & ! % 86.11/12.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 86.11/12.21 | ~ (organization(v2) = v1) | ~ (organization(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (terroristgroup(v2) = v1) | ~ (terroristgroup(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (issuingaprescription(v2) = v1) | ~ (issuingaprescription(v2) = v0)) & ! % 86.11/12.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 86.11/12.21 | ~ (creationordestructionevent(v2) = v1) | ~ % 86.11/12.21 (creationordestructionevent(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ % 86.11/12.21 (correctivelensprescription(v2) = v1) | ~ (correctivelensprescription(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (pushingababycarriage(v2) = v1) | ~ % 86.11/12.21 (pushingababycarriage(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_16_10258(v2) = v1) % 86.11/12.21 | ~ (tptpcol_16_10258(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (unitvectorinterval(v2) = % 86.11/12.21 v1) | ~ (unitvectorinterval(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ % 86.11/12.21 (movement_translationevent(v2) = v1) | ~ (movement_translationevent(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_16_31868(v2) = v1) | ~ (tptpcol_16_31868(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_5_28674(v2) = v1) | ~ (tptpcol_5_28674(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_16_29490(v2) = v1) | ~ (tptpcol_16_29490(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ % 86.11/12.21 (subcollectionofwithrelationfromtypefnorientationvectororientationpartiallytangible(v2) % 86.11/12.21 = v1) | ~ % 86.11/12.21 (subcollectionofwithrelationfromtypefnorientationvectororientationpartiallytangible(v2) % 86.11/12.21 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (orientationvector(v2) = v1) | ~ (orientationvector(v2) % 86.11/12.21 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_16_8886(v2) = v1) | ~ (tptpcol_16_8886(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (airport_physical(v2) = v1) | ~ (airport_physical(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (stringoflengthfn3(v2) = v1) | ~ (stringoflengthfn3(v2) % 86.11/12.21 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (ship(v2) = v1) | ~ (ship(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (spatialthing_localized(v2) = v1) | ~ (spatialthing_localized(v2) = v0)) % 86.11/12.21 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 % 86.11/12.21 = v0 | ~ (binarypredicate(v2) = v1) | ~ (binarypredicate(v2) = v0)) & ! % 86.11/12.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 86.11/12.21 | ~ (tptpcol_7_7172(v2) = v1) | ~ (tptpcol_7_7172(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (tptpcol_16_7738(v2) = v1) | ~ (tptpcol_16_7738(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (relation(v2) = v1) | ~ (relation(v2) = v0)) & ! [v0: MultipleValueBool] % 86.11/12.21 : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ % 86.11/12.21 (tptpcol_16_27189(v2) = v1) | ~ (tptpcol_16_27189(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (city(v2) = v1) | ~ (city(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (razor(v2) = v1) | ~ % 86.11/12.21 (razor(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 86.11/12.21 : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_16_25972(v2) = v1) | ~ % 86.11/12.21 (tptpcol_16_25972(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (pushingwithopenhand(v2) = % 86.11/12.21 v1) | ~ (pushingwithopenhand(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_16_4451(v2) = % 86.11/12.21 v1) | ~ (tptpcol_16_4451(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (footballteam(v2) = v1) % 86.11/12.21 | ~ (footballteam(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (agent_generic(v2) = v1) | % 86.11/12.21 ~ (agent_generic(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (pushingwithfingers(v2) = % 86.11/12.21 v1) | ~ (pushingwithfingers(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_15_4027(v2) = % 86.11/12.21 v1) | ~ (tptpcol_15_4027(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_16_62187(v2) = % 86.11/12.21 v1) | ~ (tptpcol_16_62187(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_16_26939(v2) = % 86.11/12.21 v1) | ~ (tptpcol_16_26939(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpquantity(v2) = v1) % 86.11/12.21 | ~ (tptpquantity(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_14_118118(v2) = % 86.11/12.21 v1) | ~ (tptpcol_14_118118(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 86.11/12.21 [v2: $i] : (v1 = v0 | ~ (f_tptpquantityfn_6(v2) = v1) | ~ % 86.11/12.21 (f_tptpquantityfn_6(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_13_92263(v2) = v1) % 86.11/12.21 | ~ (tptpcol_13_92263(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (geolevel_4(v2) = v1) | ~ % 86.11/12.21 (geolevel_4(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_15_22076(v2) = v1) % 86.11/12.21 | ~ (tptpcol_15_22076(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 86.11/12.21 : (v1 = v0 | ~ (f_tptpquantityfn_2(v2) = v1) | ~ (f_tptpquantityfn_2(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_7_39939(v2) = v1) | ~ (tptpcol_7_39939(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_8_39940(v2) = v1) | ~ (tptpcol_8_39940(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_15_26925(v2) = v1) | ~ (tptpcol_15_26925(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_16_26926(v2) = v1) | ~ (tptpcol_16_26926(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_13_118117(v2) = v1) | ~ (tptpcol_13_118117(v2) % 86.11/12.21 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_5_90114(v2) = v1) | ~ (tptpcol_5_90114(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_16_72795(v2) = v1) | ~ (tptpcol_16_72795(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_8_114177(v2) = v1) | ~ (tptpcol_8_114177(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_15_50957(v2) = v1) | ~ (tptpcol_15_50957(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_16_50958(v2) = v1) | ~ (tptpcol_16_50958(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_6_71683(v2) = v1) | ~ (tptpcol_6_71683(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_11_72774(v2) = v1) | ~ (tptpcol_11_72774(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_12_72775(v2) = v1) | ~ (tptpcol_12_72775(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_5_110593(v2) = v1) | ~ (tptpcol_5_110593(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_4_90113(v2) = v1) | ~ (tptpcol_4_90113(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_10_93700(v2) = v1) | ~ (tptpcol_10_93700(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_9_93699(v2) = v1) | ~ (tptpcol_9_93699(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (aspatialthing(v2) = v1) | ~ (aspatialthing(v2) = v0)) % 86.11/12.21 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 % 86.11/12.21 = v0 | ~ (tptpcol_7_117762(v2) = v1) | ~ (tptpcol_7_117762(v2) = v0)) & ! % 86.11/12.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 86.11/12.21 | ~ (tptpcol_8_117763(v2) = v1) | ~ (tptpcol_8_117763(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (tptpcol_7_18437(v2) = v1) | ~ (tptpcol_7_18437(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (tptpcol_6_18436(v2) = v1) | ~ (tptpcol_6_18436(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (tptpcol_8_93698(v2) = v1) | ~ (tptpcol_8_93698(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (tptpcol_11_109125(v2) = v1) | ~ (tptpcol_11_109125(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (tptpcol_6_108546(v2) = v1) | ~ (tptpcol_6_108546(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (tptpcol_6_20484(v2) = v1) | ~ (tptpcol_6_20484(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (tptpcol_15_130931(v2) = v1) | ~ (tptpcol_15_130931(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (tptpcol_16_130933(v2) = v1) | ~ (tptpcol_16_130933(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (tptpcol_7_92163(v2) = v1) | ~ (tptpcol_7_92163(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (tptpcol_15_130923(v2) = v1) | ~ (tptpcol_15_130923(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (tptpcol_16_130924(v2) = v1) | ~ (tptpcol_16_130924(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (intangibleindividual(v2) = v1) | ~ (intangibleindividual(v2) = v0)) & ! % 86.11/12.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 86.11/12.21 | ~ % 86.11/12.21 (subcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent(v2) % 86.11/12.21 = v1) | ~ % 86.11/12.21 (subcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent(v2) % 86.11/12.21 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_13_26920(v2) = v1) | ~ (tptpcol_13_26920(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_14_26921(v2) = v1) | ~ (tptpcol_14_26921(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_3_65538(v2) = v1) | ~ (tptpcol_3_65538(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (reflexivebinarypredicate(v2) = v1) | ~ % 86.11/12.21 (reflexivebinarypredicate(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_7_21508(v2) = v1) % 86.11/12.21 | ~ (tptpcol_7_21508(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (hpkb_subnationalagent(v2) % 86.11/12.21 = v1) | ~ (hpkb_subnationalagent(v2) = v0)) & ! [v0: MultipleValueBool] % 86.11/12.21 : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ % 86.11/12.21 (state_geopolitical(v2) = v1) | ~ (state_geopolitical(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (geolevel_1(v2) = v1) | ~ (geolevel_1(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (spatialthing_nonsituational(v2) = v1) | ~ % 86.11/12.21 (spatialthing_nonsituational(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (militaryperson(v2) = % 86.11/12.21 v1) | ~ (militaryperson(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_15_72793(v2) = v1) % 86.11/12.21 | ~ (tptpcol_15_72793(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_9_26885(v2) = v1) % 86.11/12.21 | ~ (tptpcol_9_26885(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_10_26886(v2) = v1) % 86.11/12.21 | ~ (tptpcol_10_26886(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_16_92269(v2) = v1) % 86.11/12.21 | ~ (tptpcol_16_92269(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_15_109185(v2) = % 86.11/12.21 v1) | ~ (tptpcol_15_109185(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_6_26627(v2) = % 86.11/12.21 v1) | ~ (tptpcol_6_26627(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_12_118116(v2) = % 86.11/12.21 v1) | ~ (tptpcol_12_118116(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_8_18438(v2) = % 86.11/12.21 v1) | ~ (tptpcol_8_18438(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_15_30970(v2) = % 86.11/12.21 v1) | ~ (tptpcol_15_30970(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_16_30972(v2) = % 86.11/12.21 v1) | ~ (tptpcol_16_30972(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_14_109181(v2) = % 86.11/12.21 v1) | ~ (tptpcol_14_109181(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.21 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ % 86.11/12.21 (physicalorderingpredicate(v2) = v1) | ~ (physicalorderingpredicate(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_7_26628(v2) = v1) | ~ (tptpcol_7_26628(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_8_26629(v2) = v1) | ~ (tptpcol_8_26629(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_3_114688(v2) = v1) | ~ (tptpcol_3_114688(v2) = % 86.11/12.21 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 86.11/12.21 (f_contextofpcwfn(v2) = v1) | ~ (f_contextofpcwfn(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ % 86.11/12.21 (subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(v2) % 86.11/12.21 = v1) | ~ % 86.11/12.21 (subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(v2) % 86.11/12.21 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_4_65539(v2) = v1) | ~ (tptpcol_4_65539(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_5_69635(v2) = v1) | ~ (tptpcol_5_69635(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_3_16386(v2) = v1) | ~ (tptpcol_3_16386(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (geographicalregion(v2) = v1) | ~ % 86.11/12.21 (geographicalregion(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 86.11/12.21 (v1 = v0 | ~ (f_tptpquantityfn_21(v2) = v1) | ~ (f_tptpquantityfn_21(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_6_112641(v2) = v1) | ~ (tptpcol_6_112641(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (tptpcol_7_113665(v2) = v1) | ~ (tptpcol_7_113665(v2) = % 86.11/12.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.21 $i] : (v1 = v0 | ~ (artifact(v2) = v1) | ~ (artifact(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (tptpcol_13_18664(v2) = v1) | ~ (tptpcol_13_18664(v2) = v0)) & ! [v0: % 86.11/12.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.21 ~ (firstordercollection(v2) = v1) | ~ (firstordercollection(v2) = v0)) & ! % 86.11/12.21 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (f_tptpquantityfn_14(v2) % 86.11/12.21 = v1) | ~ (f_tptpquantityfn_14(v2) = v0)) & ! [v0: MultipleValueBool] : % 86.11/12.21 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (supplies(v2) = v1) | % 86.11/12.21 ~ (supplies(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.21 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ % 86.11/12.21 (inanimateobject_nonnatural(v2) = v1) | ~ (inanimateobject_nonnatural(v2) = % 86.11/12.22 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.22 $i] : (v1 = v0 | ~ (tptpcol_13_22071(v2) = v1) | ~ (tptpcol_13_22071(v2) = % 86.11/12.22 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.22 $i] : (v1 = v0 | ~ (tptpcol_14_22072(v2) = v1) | ~ (tptpcol_14_22072(v2) = % 86.11/12.22 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.22 $i] : (v1 = v0 | ~ (tptpcol_7_108547(v2) = v1) | ~ (tptpcol_7_108547(v2) = % 86.11/12.22 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.22 $i] : (v1 = v0 | ~ (tptpcol_8_109059(v2) = v1) | ~ (tptpcol_8_109059(v2) = % 86.11/12.22 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.22 $i] : (v1 = v0 | ~ (tptpcol_14_93774(v2) = v1) | ~ (tptpcol_14_93774(v2) = % 86.11/12.22 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.22 $i] : (v1 = v0 | ~ (tptpcol_15_93775(v2) = v1) | ~ (tptpcol_15_93775(v2) = % 86.11/12.22 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.22 $i] : (v1 = v0 | ~ (tptpcol_12_22055(v2) = v1) | ~ (tptpcol_12_22055(v2) = % 86.11/12.22 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.22 $i] : (v1 = v0 | ~ (runningshorts(v2) = v1) | ~ (runningshorts(v2) = v0)) % 86.11/12.22 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 % 86.11/12.22 = v0 | ~ (tptpcol_9_118019(v2) = v1) | ~ (tptpcol_9_118019(v2) = v0)) & ! % 86.11/12.22 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 86.11/12.22 | ~ (aspatialinformationstore(v2) = v1) | ~ (aspatialinformationstore(v2) % 86.11/12.22 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.22 $i] : (v1 = v0 | ~ (collection(v2) = v1) | ~ (collection(v2) = v0)) & ! % 86.11/12.22 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 86.11/12.22 | ~ (fixedordercollection(v2) = v1) | ~ (fixedordercollection(v2) = v0)) & % 86.11/12.22 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = % 86.11/12.22 v0 | ~ (tptpcol_8_92164(v2) = v1) | ~ (tptpcol_8_92164(v2) = v0)) & ! % 86.11/12.22 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 86.11/12.22 | ~ (tptpcol_9_92165(v2) = v1) | ~ (tptpcol_9_92165(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_1_1(v2) = v1) | ~ (tptpcol_1_1(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_2_2(v2) = v1) | ~ (tptpcol_2_2(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_11_26887(v2) = v1) | ~ (tptpcol_11_26887(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_12_26919(v2) = v1) | ~ (tptpcol_12_26919(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ % 86.11/12.22 (subcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription(v2) % 86.11/12.22 = v1) | ~ % 86.11/12.22 (subcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription(v2) % 86.11/12.22 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.22 $i] : (v1 = v0 | ~ (mathematicalorcomputationalthing(v2) = v1) | ~ % 86.11/12.22 (mathematicalorcomputationalthing(v2) = v0)) & ! [v0: MultipleValueBool] : % 86.11/12.22 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_10_118020(v2) % 86.11/12.22 = v1) | ~ (tptpcol_10_118020(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.22 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_11_118084(v2) = % 86.11/12.22 v1) | ~ (tptpcol_11_118084(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.22 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_0_0(v2) = v1) | % 86.11/12.22 ~ (tptpcol_0_0(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (geolevel_3(v2) = v1) | ~ % 86.11/12.22 (geolevel_3(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_4_24578(v2) = v1) % 86.11/12.22 | ~ (tptpcol_4_24578(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_5_24579(v2) = v1) % 86.11/12.22 | ~ (tptpcol_5_24579(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_5_106498(v2) = v1) % 86.11/12.22 | ~ (tptpcol_5_106498(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_12_109157(v2) = % 86.11/12.22 v1) | ~ (tptpcol_12_109157(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.22 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_13_109173(v2) = % 86.11/12.22 v1) | ~ (tptpcol_13_109173(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.22 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (mathematicalthing(v2) = % 86.11/12.22 v1) | ~ (mathematicalthing(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.22 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (setorcollection(v2) = % 86.11/12.22 v1) | ~ (setorcollection(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.22 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_11_18631(v2) = % 86.11/12.22 v1) | ~ (tptpcol_11_18631(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.22 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_12_18663(v2) = % 86.11/12.22 v1) | ~ (tptpcol_12_18663(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 86.11/12.22 [v2: $i] : (v1 = v0 | ~ (f_tptpquantityfn_13(v2) = v1) | ~ % 86.11/12.22 (f_tptpquantityfn_13(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_14_92264(v2) = v1) % 86.11/12.22 | ~ (tptpcol_14_92264(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_15_92268(v2) = v1) % 86.11/12.22 | ~ (tptpcol_15_92268(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_6_116738(v2) = v1) % 86.11/12.22 | ~ (tptpcol_6_116738(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (shavingrazor_manual(v2) = % 86.11/12.22 v1) | ~ (shavingrazor_manual(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.22 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_9_109060(v2) = % 86.11/12.22 v1) | ~ (tptpcol_9_109060(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.22 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_10_109061(v2) = % 86.11/12.22 v1) | ~ (tptpcol_10_109061(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.22 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ % 86.11/12.22 (executionbyfiringsquad(v2) = v1) | ~ (executionbyfiringsquad(v2) = v0)) & % 86.11/12.22 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = % 86.11/12.22 v0 | ~ (navypersonnel(v2) = v1) | ~ (navypersonnel(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_12_92262(v2) = v1) | ~ (tptpcol_12_92262(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (thing(v2) = v1) | ~ (thing(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.22 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ % 86.11/12.22 (computerdataartifact(v2) = v1) | ~ (computerdataartifact(v2) = v0)) & ! % 86.11/12.22 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 86.11/12.22 | ~ (applicationcontext(v2) = v1) | ~ (applicationcontext(v2) = v0)) & ! % 86.11/12.22 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (f_tptpquantityfn_1(v2) = % 86.11/12.22 v1) | ~ (f_tptpquantityfn_1(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.22 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (furpelt(v2) = v1) | ~ % 86.11/12.22 (furpelt(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_13_93766(v2) = v1) % 86.11/12.22 | ~ (tptpcol_13_93766(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_9_40196(v2) = v1) % 86.11/12.22 | ~ (tptpcol_9_40196(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_10_40324(v2) = v1) % 86.11/12.22 | ~ (tptpcol_10_40324(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_7_72707(v2) = v1) % 86.11/12.22 | ~ (tptpcol_7_72707(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_8_72708(v2) = v1) % 86.11/12.22 | ~ (tptpcol_8_72708(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_11_93764(v2) = v1) % 86.11/12.22 | ~ (tptpcol_11_93764(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_12_93765(v2) = v1) % 86.11/12.22 | ~ (tptpcol_12_93765(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_4_114689(v2) = v1) % 86.11/12.22 | ~ (tptpcol_4_114689(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_5_114690(v2) = v1) % 86.11/12.22 | ~ (tptpcol_5_114690(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_3_98305(v2) = v1) % 86.11/12.22 | ~ (tptpcol_3_98305(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_4_106497(v2) = v1) % 86.11/12.22 | ~ (tptpcol_4_106497(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_11_40388(v2) = v1) % 86.11/12.22 | ~ (tptpcol_11_40388(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ % 86.11/12.22 (marriagelicensedocument(v2) = v1) | ~ (marriagelicensedocument(v2) = v0)) % 86.11/12.22 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 % 86.11/12.22 = v0 | ~ (tptpcol_1_65536(v2) = v1) | ~ (tptpcol_1_65536(v2) = v0)) & ! % 86.11/12.22 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 86.11/12.22 | ~ (tptpcol_2_98304(v2) = v1) | ~ (tptpcol_2_98304(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_10_92166(v2) = v1) | ~ (tptpcol_10_92166(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_11_92230(v2) = v1) | ~ (tptpcol_11_92230(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (orderingpredicate(v2) = v1) | ~ (orderingpredicate(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_9_18439(v2) = v1) | ~ (tptpcol_9_18439(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_10_18567(v2) = v1) | ~ (tptpcol_10_18567(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_2_65537(v2) = v1) | ~ (tptpcol_2_65537(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_3_81921(v2) = v1) | ~ (tptpcol_3_81921(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (artsupplies(v2) = v1) | ~ (artsupplies(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (enduringthing_localized(v2) = v1) | ~ (enduringthing_localized(v2) = % 86.11/12.22 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.22 $i] : (v1 = v0 | ~ (location_underspecified(v2) = v1) | ~ % 86.11/12.22 (location_underspecified(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 86.11/12.22 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ % 86.11/12.22 (trajector_underspecified(v2) = v1) | ~ (trajector_underspecified(v2) = % 86.11/12.22 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.22 $i] : (v1 = v0 | ~ (individual(v2) = v1) | ~ (individual(v2) = v0)) & ! % 86.11/12.22 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 86.11/12.22 | ~ (partiallyintangibleindividual(v2) = v1) | ~ % 86.11/12.22 (partiallyintangibleindividual(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.22 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_10_22022(v2) = % 86.11/12.22 v1) | ~ (tptpcol_10_22022(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.22 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_11_22023(v2) = % 86.11/12.22 v1) | ~ (tptpcol_11_22023(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.22 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_5_20483(v2) = % 86.11/12.22 v1) | ~ (tptpcol_5_20483(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.22 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_13_72791(v2) = % 86.11/12.22 v1) | ~ (tptpcol_13_72791(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.22 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (tptpcol_14_72792(v2) = % 86.11/12.22 v1) | ~ (tptpcol_14_72792(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 86.11/12.22 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ % 86.11/12.22 (ridgeline_topographical(v2) = v1) | ~ (ridgeline_topographical(v2) = v0)) % 86.11/12.22 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 % 86.11/12.22 = v0 | ~ (tptpcol_4_16387(v2) = v1) | ~ (tptpcol_4_16387(v2) = v0)) & ! % 86.11/12.22 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 86.11/12.22 | ~ (tptpcol_5_16388(v2) = v1) | ~ (tptpcol_5_16388(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_8_22020(v2) = v1) | ~ (tptpcol_8_22020(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_9_22021(v2) = v1) | ~ (tptpcol_9_22021(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (transitivebinarypredicate(v2) = v1) | ~ (transitivebinarypredicate(v2) = % 86.11/12.22 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 86.11/12.22 $i] : (v1 = v0 | ~ (mtvisible(v2) = v1) | ~ (mtvisible(v2) = v0)) & ! % 86.11/12.22 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 86.11/12.22 | ~ (tptpcol_12_40420(v2) = v1) | ~ (tptpcol_12_40420(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_13_40421(v2) = v1) | ~ (tptpcol_13_40421(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_6_92162(v2) = v1) | ~ (tptpcol_6_92162(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_7_93186(v2) = v1) | ~ (tptpcol_7_93186(v2) = v0)) & ! [v0: $i] % 86.11/12.22 : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (f_urlfn(v2) = v1) | ~ % 86.11/12.22 (f_urlfn(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (f_urlreferentfn(v2) = v1) | ~ (f_urlreferentfn(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (microtheory(v2) = v1) | ~ (microtheory(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (inanimateobject(v2) = v1) | ~ (inanimateobject(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_9_72709(v2) = v1) | ~ (tptpcol_9_72709(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_10_72710(v2) = v1) | ~ (tptpcol_10_72710(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_14_40429(v2) = v1) | ~ (tptpcol_14_40429(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (tptpcol_15_40430(v2) = v1) | ~ (tptpcol_15_40430(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (partiallytangible(v2) = v1) | ~ (partiallytangible(v2) = v0)) & ! [v0: % 86.11/12.22 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 86.11/12.22 ~ (intangible(v2) = v1) | ~ (intangible(v2) = v0)) % 86.11/12.22 % 86.11/12.22 Further assumptions not needed in the proof: % 86.11/12.22 -------------------------------------------- % 86.11/12.22 ax1_10, ax1_100, ax1_1000, ax1_1001, ax1_1002, ax1_1003, ax1_1004, ax1_1005, % 86.11/12.22 ax1_1006, ax1_1007, ax1_1008, ax1_1009, ax1_101, ax1_1010, ax1_1011, ax1_1012, % 86.11/12.22 ax1_1013, ax1_1014, ax1_1015, ax1_1016, ax1_1017, ax1_1018, ax1_1019, ax1_102, % 86.11/12.22 ax1_1020, ax1_1021, ax1_1022, ax1_1023, ax1_1024, ax1_1025, ax1_1026, ax1_1027, % 86.11/12.22 ax1_1028, ax1_1029, ax1_103, ax1_1030, ax1_1031, ax1_1032, ax1_1033, ax1_1034, % 86.11/12.22 ax1_1035, ax1_1036, ax1_1037, ax1_1038, ax1_1039, ax1_104, ax1_1040, ax1_1041, % 86.11/12.22 ax1_1042, ax1_1043, ax1_1044, ax1_1045, ax1_1046, ax1_1047, ax1_1048, ax1_1049, % 86.11/12.22 ax1_105, ax1_1050, ax1_1051, ax1_1052, ax1_1053, ax1_1054, ax1_1055, ax1_1056, % 86.11/12.22 ax1_1057, ax1_1058, ax1_1059, ax1_106, ax1_1060, ax1_1061, ax1_1062, ax1_1063, % 86.11/12.22 ax1_1064, ax1_1065, ax1_1066, ax1_1067, ax1_1068, ax1_1069, ax1_107, ax1_1070, % 86.11/12.22 ax1_1071, ax1_1072, ax1_1073, ax1_1074, ax1_1075, ax1_1076, ax1_1077, ax1_1078, % 86.11/12.22 ax1_1079, ax1_108, ax1_1080, ax1_1081, ax1_1082, ax1_1083, ax1_1084, ax1_1085, % 86.11/12.22 ax1_1086, ax1_1087, ax1_1088, ax1_1089, ax1_109, ax1_1090, ax1_1091, ax1_1092, % 86.11/12.22 ax1_1093, ax1_1094, ax1_1095, ax1_1096, ax1_1097, ax1_1098, ax1_1099, ax1_11, % 86.11/12.22 ax1_110, ax1_1100, ax1_1101, ax1_1102, ax1_1103, ax1_1104, ax1_1105, ax1_1106, % 86.11/12.22 ax1_1107, ax1_1108, ax1_1109, ax1_111, ax1_1110, ax1_1111, ax1_1112, ax1_1113, % 86.11/12.22 ax1_1114, ax1_1115, ax1_1116, ax1_1117, ax1_1118, ax1_1119, ax1_112, ax1_1120, % 86.11/12.22 ax1_1121, ax1_1122, ax1_1124, ax1_1125, ax1_1126, ax1_1127, ax1_1128, ax1_1129, % 86.11/12.22 ax1_113, ax1_1130, ax1_1131, ax1_114, ax1_115, ax1_116, ax1_117, ax1_118, % 86.11/12.22 ax1_119, ax1_12, ax1_120, ax1_123, ax1_124, ax1_125, ax1_126, ax1_127, ax1_129, % 86.11/12.22 ax1_13, ax1_130, ax1_131, ax1_132, ax1_133, ax1_134, ax1_135, ax1_136, ax1_137, % 86.11/12.22 ax1_138, ax1_139, ax1_14, ax1_140, ax1_141, ax1_142, ax1_143, ax1_144, ax1_145, % 86.11/12.22 ax1_146, ax1_147, ax1_148, ax1_149, ax1_15, ax1_150, ax1_151, ax1_152, ax1_153, % 86.11/12.22 ax1_154, ax1_155, ax1_156, ax1_157, ax1_158, ax1_159, ax1_16, ax1_160, ax1_161, % 86.11/12.22 ax1_162, ax1_163, ax1_164, ax1_165, ax1_166, ax1_167, ax1_168, ax1_169, ax1_17, % 86.11/12.22 ax1_170, ax1_171, ax1_172, ax1_173, ax1_174, ax1_175, ax1_176, ax1_177, ax1_178, % 86.11/12.22 ax1_179, ax1_18, ax1_180, ax1_181, ax1_182, ax1_183, ax1_184, ax1_185, ax1_186, % 86.11/12.22 ax1_187, ax1_189, ax1_19, ax1_190, ax1_191, ax1_192, ax1_193, ax1_194, ax1_195, % 86.11/12.22 ax1_196, ax1_197, ax1_198, ax1_199, ax1_2, ax1_20, ax1_200, ax1_201, ax1_202, % 86.11/12.22 ax1_203, ax1_204, ax1_205, ax1_206, ax1_207, ax1_208, ax1_209, ax1_21, ax1_210, % 86.11/12.22 ax1_211, ax1_213, ax1_214, ax1_215, ax1_216, ax1_217, ax1_218, ax1_219, ax1_22, % 86.11/12.22 ax1_220, ax1_221, ax1_222, ax1_223, ax1_224, ax1_225, ax1_226, ax1_227, ax1_228, % 86.11/12.22 ax1_229, ax1_23, ax1_230, ax1_231, ax1_232, ax1_233, ax1_234, ax1_235, ax1_236, % 86.11/12.22 ax1_237, ax1_238, ax1_239, ax1_24, ax1_240, ax1_241, ax1_242, ax1_243, ax1_244, % 86.11/12.22 ax1_245, ax1_246, ax1_247, ax1_248, ax1_249, ax1_25, ax1_250, ax1_251, ax1_252, % 86.11/12.22 ax1_253, ax1_254, ax1_255, ax1_256, ax1_257, ax1_258, ax1_259, ax1_26, ax1_260, % 86.11/12.22 ax1_261, ax1_262, ax1_263, ax1_264, ax1_265, ax1_266, ax1_267, ax1_268, ax1_269, % 86.11/12.22 ax1_27, ax1_270, ax1_271, ax1_272, ax1_273, ax1_274, ax1_275, ax1_277, ax1_278, % 86.11/12.22 ax1_279, ax1_28, ax1_280, ax1_281, ax1_282, ax1_283, ax1_284, ax1_285, ax1_286, % 86.11/12.22 ax1_287, ax1_288, ax1_289, ax1_29, ax1_290, ax1_291, ax1_293, ax1_294, ax1_295, % 86.11/12.22 ax1_296, ax1_297, ax1_298, ax1_299, ax1_3, ax1_30, ax1_300, ax1_301, ax1_302, % 86.11/12.22 ax1_303, ax1_304, ax1_305, ax1_306, ax1_307, ax1_308, ax1_309, ax1_31, ax1_310, % 86.11/12.22 ax1_311, ax1_312, ax1_313, ax1_314, ax1_315, ax1_316, ax1_317, ax1_318, ax1_319, % 86.11/12.22 ax1_32, ax1_320, ax1_322, ax1_323, ax1_324, ax1_325, ax1_327, ax1_328, ax1_329, % 86.11/12.22 ax1_33, ax1_330, ax1_331, ax1_332, ax1_333, ax1_335, ax1_336, ax1_338, ax1_339, % 86.11/12.22 ax1_34, ax1_340, ax1_341, ax1_342, ax1_343, ax1_344, ax1_345, ax1_346, ax1_347, % 86.11/12.22 ax1_348, ax1_349, ax1_35, ax1_350, ax1_351, ax1_352, ax1_353, ax1_354, ax1_355, % 86.11/12.22 ax1_356, ax1_357, ax1_358, ax1_359, ax1_36, ax1_360, ax1_361, ax1_362, ax1_363, % 86.11/12.22 ax1_364, ax1_365, ax1_366, ax1_367, ax1_368, ax1_37, ax1_370, ax1_371, ax1_372, % 86.11/12.22 ax1_373, ax1_374, ax1_375, ax1_376, ax1_377, ax1_378, ax1_379, ax1_38, ax1_380, % 86.11/12.22 ax1_381, ax1_382, ax1_383, ax1_384, ax1_385, ax1_386, ax1_387, ax1_388, ax1_389, % 86.11/12.22 ax1_39, ax1_390, ax1_391, ax1_392, ax1_393, ax1_394, ax1_395, ax1_396, ax1_397, % 86.11/12.22 ax1_398, ax1_399, ax1_4, ax1_40, ax1_400, ax1_401, ax1_402, ax1_403, ax1_404, % 86.11/12.22 ax1_405, ax1_406, ax1_407, ax1_408, ax1_409, ax1_41, ax1_410, ax1_411, ax1_412, % 86.11/12.22 ax1_413, ax1_414, ax1_415, ax1_416, ax1_417, ax1_418, ax1_419, ax1_42, ax1_420, % 86.11/12.22 ax1_421, ax1_422, ax1_423, ax1_424, ax1_425, ax1_426, ax1_427, ax1_428, ax1_429, % 86.11/12.22 ax1_43, ax1_430, ax1_431, ax1_432, ax1_433, ax1_434, ax1_435, ax1_436, ax1_437, % 86.11/12.22 ax1_438, ax1_439, ax1_44, ax1_440, ax1_441, ax1_442, ax1_443, ax1_444, ax1_445, % 86.11/12.22 ax1_446, ax1_447, ax1_448, ax1_449, ax1_45, ax1_450, ax1_451, ax1_452, ax1_453, % 86.11/12.22 ax1_454, ax1_455, ax1_456, ax1_457, ax1_458, ax1_459, ax1_46, ax1_460, ax1_461, % 86.11/12.22 ax1_462, ax1_463, ax1_465, ax1_466, ax1_467, ax1_468, ax1_469, ax1_47, ax1_470, % 86.11/12.22 ax1_471, ax1_473, ax1_474, ax1_475, ax1_476, ax1_477, ax1_479, ax1_48, ax1_480, % 86.11/12.22 ax1_481, ax1_482, ax1_483, ax1_484, ax1_486, ax1_487, ax1_488, ax1_489, ax1_49, % 86.11/12.22 ax1_490, ax1_491, ax1_492, ax1_493, ax1_494, ax1_495, ax1_496, ax1_497, ax1_498, % 86.11/12.22 ax1_499, ax1_5, ax1_50, ax1_500, ax1_501, ax1_502, ax1_503, ax1_504, ax1_505, % 86.11/12.22 ax1_506, ax1_507, ax1_508, ax1_509, ax1_51, ax1_510, ax1_511, ax1_512, ax1_513, % 86.11/12.22 ax1_514, ax1_515, ax1_516, ax1_517, ax1_518, ax1_519, ax1_52, ax1_520, ax1_521, % 86.11/12.22 ax1_522, ax1_523, ax1_524, ax1_525, ax1_526, ax1_527, ax1_528, ax1_529, ax1_53, % 86.11/12.22 ax1_530, ax1_531, ax1_532, ax1_533, ax1_534, ax1_535, ax1_536, ax1_537, ax1_538, % 86.11/12.22 ax1_539, ax1_54, ax1_540, ax1_541, ax1_542, ax1_543, ax1_544, ax1_545, ax1_546, % 86.11/12.22 ax1_547, ax1_548, ax1_549, ax1_55, ax1_550, ax1_551, ax1_552, ax1_553, ax1_554, % 86.11/12.22 ax1_555, ax1_556, ax1_557, ax1_558, ax1_559, ax1_56, ax1_560, ax1_561, ax1_562, % 86.11/12.22 ax1_563, ax1_564, ax1_565, ax1_566, ax1_567, ax1_568, ax1_569, ax1_57, ax1_570, % 86.11/12.22 ax1_571, ax1_572, ax1_573, ax1_574, ax1_575, ax1_576, ax1_577, ax1_578, ax1_579, % 86.11/12.22 ax1_58, ax1_580, ax1_581, ax1_582, ax1_583, ax1_584, ax1_585, ax1_586, ax1_587, % 86.11/12.22 ax1_588, ax1_589, ax1_59, ax1_590, ax1_591, ax1_592, ax1_593, ax1_594, ax1_595, % 86.11/12.22 ax1_596, ax1_597, ax1_598, ax1_599, ax1_6, ax1_60, ax1_600, ax1_601, ax1_602, % 86.11/12.22 ax1_603, ax1_604, ax1_605, ax1_606, ax1_607, ax1_608, ax1_609, ax1_61, ax1_610, % 86.11/12.22 ax1_611, ax1_612, ax1_613, ax1_614, ax1_615, ax1_616, ax1_617, ax1_618, ax1_619, % 86.11/12.22 ax1_62, ax1_620, ax1_621, ax1_622, ax1_623, ax1_624, ax1_625, ax1_626, ax1_627, % 86.11/12.22 ax1_628, ax1_629, ax1_630, ax1_631, ax1_632, ax1_633, ax1_634, ax1_635, ax1_636, % 86.11/12.22 ax1_637, ax1_638, ax1_639, ax1_64, ax1_640, ax1_641, ax1_642, ax1_643, ax1_644, % 86.11/12.22 ax1_645, ax1_646, ax1_647, ax1_648, ax1_649, ax1_65, ax1_650, ax1_651, ax1_652, % 86.11/12.22 ax1_653, ax1_654, ax1_655, ax1_656, ax1_657, ax1_658, ax1_659, ax1_66, ax1_660, % 86.11/12.22 ax1_661, ax1_662, ax1_663, ax1_664, ax1_665, ax1_666, ax1_667, ax1_668, ax1_669, % 86.11/12.22 ax1_67, ax1_670, ax1_671, ax1_672, ax1_673, ax1_674, ax1_675, ax1_676, ax1_677, % 86.11/12.22 ax1_678, ax1_679, ax1_68, ax1_680, ax1_681, ax1_682, ax1_683, ax1_684, ax1_685, % 86.11/12.22 ax1_686, ax1_687, ax1_688, ax1_689, ax1_69, ax1_690, ax1_691, ax1_692, ax1_693, % 86.11/12.22 ax1_694, ax1_695, ax1_696, ax1_697, ax1_698, ax1_699, ax1_7, ax1_70, ax1_700, % 86.11/12.22 ax1_701, ax1_702, ax1_703, ax1_704, ax1_705, ax1_706, ax1_707, ax1_708, ax1_709, % 86.11/12.22 ax1_71, ax1_710, ax1_711, ax1_712, ax1_713, ax1_714, ax1_715, ax1_716, ax1_717, % 86.11/12.22 ax1_718, ax1_719, ax1_72, ax1_720, ax1_721, ax1_722, ax1_723, ax1_724, ax1_725, % 86.11/12.22 ax1_726, ax1_727, ax1_728, ax1_729, ax1_73, ax1_730, ax1_731, ax1_732, ax1_733, % 86.11/12.22 ax1_734, ax1_735, ax1_736, ax1_737, ax1_738, ax1_739, ax1_74, ax1_740, ax1_741, % 86.11/12.22 ax1_742, ax1_743, ax1_744, ax1_745, ax1_746, ax1_747, ax1_748, ax1_749, ax1_75, % 86.11/12.22 ax1_750, ax1_751, ax1_752, ax1_753, ax1_754, ax1_755, ax1_756, ax1_757, ax1_758, % 86.11/12.22 ax1_759, ax1_76, ax1_760, ax1_761, ax1_762, ax1_763, ax1_764, ax1_765, ax1_766, % 86.11/12.22 ax1_767, ax1_768, ax1_769, ax1_77, ax1_770, ax1_771, ax1_772, ax1_773, ax1_774, % 86.11/12.22 ax1_775, ax1_776, ax1_777, ax1_778, ax1_779, ax1_78, ax1_780, ax1_781, ax1_782, % 86.11/12.22 ax1_783, ax1_784, ax1_785, ax1_786, ax1_787, ax1_788, ax1_789, ax1_79, ax1_790, % 86.11/12.22 ax1_791, ax1_792, ax1_793, ax1_794, ax1_795, ax1_796, ax1_797, ax1_798, ax1_799, % 86.11/12.22 ax1_8, ax1_80, ax1_800, ax1_801, ax1_802, ax1_803, ax1_804, ax1_805, ax1_806, % 86.11/12.22 ax1_807, ax1_808, ax1_809, ax1_81, ax1_810, ax1_811, ax1_812, ax1_813, ax1_814, % 86.11/12.22 ax1_815, ax1_816, ax1_817, ax1_818, ax1_819, ax1_820, ax1_821, ax1_822, ax1_823, % 86.11/12.22 ax1_824, ax1_825, ax1_826, ax1_827, ax1_828, ax1_829, ax1_83, ax1_830, ax1_831, % 86.11/12.22 ax1_832, ax1_833, ax1_834, ax1_835, ax1_836, ax1_837, ax1_838, ax1_839, ax1_84, % 86.11/12.22 ax1_840, ax1_841, ax1_842, ax1_843, ax1_844, ax1_845, ax1_846, ax1_847, ax1_848, % 86.11/12.22 ax1_849, ax1_85, ax1_850, ax1_851, ax1_852, ax1_853, ax1_854, ax1_855, ax1_856, % 86.11/12.22 ax1_857, ax1_858, ax1_859, ax1_86, ax1_860, ax1_861, ax1_862, ax1_863, ax1_864, % 86.11/12.22 ax1_865, ax1_866, ax1_867, ax1_868, ax1_869, ax1_87, ax1_870, ax1_871, ax1_872, % 86.11/12.22 ax1_873, ax1_874, ax1_875, ax1_876, ax1_877, ax1_878, ax1_879, ax1_88, ax1_880, % 86.11/12.22 ax1_881, ax1_882, ax1_883, ax1_884, ax1_885, ax1_886, ax1_887, ax1_888, ax1_889, % 86.11/12.22 ax1_89, ax1_890, ax1_891, ax1_892, ax1_893, ax1_894, ax1_895, ax1_896, ax1_897, % 86.11/12.22 ax1_898, ax1_899, ax1_9, ax1_90, ax1_900, ax1_901, ax1_902, ax1_903, ax1_904, % 86.11/12.22 ax1_905, ax1_906, ax1_907, ax1_908, ax1_909, ax1_91, ax1_910, ax1_911, ax1_912, % 86.11/12.22 ax1_913, ax1_914, ax1_915, ax1_916, ax1_917, ax1_918, ax1_919, ax1_92, ax1_920, % 86.11/12.22 ax1_921, ax1_922, ax1_923, ax1_924, ax1_925, ax1_926, ax1_927, ax1_928, ax1_929, % 86.11/12.22 ax1_93, ax1_930, ax1_931, ax1_932, ax1_934, ax1_935, ax1_936, ax1_937, ax1_938, % 86.11/12.22 ax1_939, ax1_94, ax1_940, ax1_941, ax1_942, ax1_943, ax1_944, ax1_945, ax1_946, % 86.11/12.22 ax1_947, ax1_948, ax1_949, ax1_95, ax1_950, ax1_951, ax1_952, ax1_953, ax1_954, % 86.11/12.22 ax1_955, ax1_956, ax1_957, ax1_958, ax1_959, ax1_96, ax1_960, ax1_961, ax1_962, % 86.11/12.22 ax1_963, ax1_964, ax1_965, ax1_966, ax1_967, ax1_968, ax1_969, ax1_97, ax1_970, % 86.11/12.22 ax1_971, ax1_972, ax1_973, ax1_974, ax1_975, ax1_976, ax1_977, ax1_978, ax1_979, % 86.11/12.22 ax1_98, ax1_980, ax1_981, ax1_982, ax1_983, ax1_984, ax1_985, ax1_986, ax1_987, % 86.11/12.22 ax1_988, ax1_989, ax1_99, ax1_990, ax1_991, ax1_992, ax1_993, ax1_994, ax1_995, % 86.11/12.22 ax1_996, ax1_997, ax1_998, ax1_999 % 86.11/12.22 % 86.11/12.22 Those formulas are unsatisfiable: % 86.11/12.22 --------------------------------- % 86.11/12.22 % 86.11/12.22 Begin of proof % 86.11/12.22 | % 86.11/12.22 | ALPHA: (ax1_1) implies: % 86.11/12.22 | (1) genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt) = 0 % 86.11/12.22 | % 86.11/12.22 | ALPHA: (ax1_63) implies: % 86.11/12.22 | (2) genlmt(c_tptpgeo_member7_mt, c_tptpgeo_spindleheadmt) = 0 % 86.11/12.22 | % 86.11/12.22 | ALPHA: (ax1_82) implies: % 86.11/12.23 | (3) ? [v0: any] : ? [v1: any] : (inregion(c_geolocation_x53_y74, % 86.11/12.23 | c_georegion_l4_x53_y74) = v1 & mtvisible(c_tptpgeo_member7_mt) = v0 % 86.11/12.23 | & ( ~ (v0 = 0) | v1 = 0)) % 86.11/12.23 | % 86.11/12.23 | ALPHA: (ax1_121) implies: % 86.11/12.23 | (4) ? [v0: any] : ? [v1: any] : (geolevel_3(c_georegion_l3_x4_y13) = v1 & % 86.11/12.23 | mtvisible(c_worldgeographymt) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 86.11/12.23 | % 86.11/12.23 | ALPHA: (ax1_122) implies: % 86.11/12.23 | (5) ? [v0: any] : ? [v1: any] : (borderson(c_georegion_l4_x27_y64, % 86.11/12.23 | c_georegion_l4_x27_y65) = v1 & mtvisible(c_tptpgeo_member7_mt) = v0 % 86.11/12.23 | & ( ~ (v0 = 0) | v1 = 0)) % 86.11/12.23 | % 86.11/12.23 | ALPHA: (ax1_128) implies: % 86.11/12.23 | (6) ! [v0: $i] : ! [v1: $i] : ( ~ (geographicalsubregions(v0, v1) = 0) | % 86.11/12.23 | ~ $i(v1) | ~ $i(v0) | inregion(v1, v0) = 0) % 86.11/12.23 | % 86.11/12.23 | ALPHA: (ax1_188) implies: % 86.11/12.23 | (7) ? [v0: any] : ? [v1: any] : (mtvisible(c_tptpgeo_member7_mt) = v0 & % 86.11/12.23 | geographicalsubregions(c_georegion_l3_x15_y24, % 86.11/12.23 | c_georegion_l4_x45_y72) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 86.11/12.23 | % 86.11/12.23 | ALPHA: (ax1_212) implies: % 86.11/12.23 | (8) genlmt(c_tptpgeo_member3_mt, c_tptpgeo_spindleheadmt) = 0 % 86.11/12.23 | % 86.11/12.23 | ALPHA: (ax1_276) implies: % 86.11/12.23 | (9) ? [v0: any] : ? [v1: any] : (mtvisible(c_tptpgeo_member7_mt) = v0 & % 86.11/12.23 | geographicalsubregions(c_georegion_l2_x5_y8, c_georegion_l3_x15_y24) % 86.11/12.23 | = v1 & ( ~ (v0 = 0) | v1 = 0)) % 86.11/12.23 | % 86.11/12.23 | ALPHA: (ax1_292) implies: % 86.11/12.23 | (10) ? [v0: any] : ? [v1: any] : (geolevel_1(c_georegion_l1_x2_y0) = v1 & % 86.11/12.23 | mtvisible(c_worldgeographymt) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 86.11/12.23 | % 86.11/12.23 | ALPHA: (ax1_321) implies: % 86.11/12.23 | (11) ? [v0: any] : ? [v1: any] : % 86.11/12.23 | (state_geopolitical(c_wanica_districtsuriname) = v1 & % 86.11/12.23 | mtvisible(c_worldgeographymt) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 86.11/12.23 | % 86.11/12.23 | ALPHA: (ax1_326) implies: % 86.11/12.23 | (12) $i(c_tptpgeo_spindleheadmt) % 86.11/12.23 | (13) genlmt(c_tptpgeo_spindleheadmt, c_worldgeographymt) = 0 % 86.11/12.23 | % 86.11/12.23 | ALPHA: (ax1_334) implies: % 86.11/12.23 | (14) $i(c_geographymt) % 86.11/12.23 | (15) genlmt(c_worldgeographymt, c_geographymt) = 0 % 86.11/12.23 | % 86.11/12.23 | ALPHA: (ax1_337) implies: % 86.11/12.23 | (16) $i(c_tptpgeo_member3_mt) % 86.11/12.23 | % 86.11/12.23 | ALPHA: (ax1_369) implies: % 86.11/12.23 | (17) $i(c_tptpgeo_member8_mt) % 86.11/12.23 | % 86.11/12.23 | ALPHA: (ax1_464) implies: % 86.11/12.23 | (18) ? [v0: any] : ? [v1: any] : (geolevel_4(c_georegion_l4_x75_y75) = v1 % 86.11/12.23 | & mtvisible(c_worldgeographymt) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 86.11/12.23 | % 86.11/12.23 | ALPHA: (ax1_472) implies: % 86.11/12.23 | (19) $i(c_georegion_l4_x53_y74) % 86.11/12.23 | (20) ? [v0: any] : ? [v1: any] : (mtvisible(c_tptpgeo_member7_mt) = v0 & % 86.11/12.23 | geographicalsubregions(c_georegion_l3_x17_y24, % 86.11/12.23 | c_georegion_l4_x53_y74) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 86.11/12.23 | % 86.11/12.23 | ALPHA: (ax1_478) implies: % 86.11/12.23 | (21) $i(c_worldgeographymt) % 86.11/12.23 | (22) ? [v0: any] : ? [v1: any] : (geolevel_3(c_georegion_l3_x17_y24) = v1 % 86.11/12.23 | & mtvisible(c_worldgeographymt) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 86.11/12.23 | % 86.11/12.23 | ALPHA: (ax1_485) implies: % 86.11/12.23 | (23) ? [v0: any] : ? [v1: any] : (borderson(c_georegion_l4_x29_y75, % 86.11/12.23 | c_georegion_l4_x29_y76) = v1 & mtvisible(c_tptpgeo_member7_mt) = % 86.11/12.23 | v0 & ( ~ (v0 = 0) | v1 = 0)) % 86.11/12.23 | % 86.11/12.23 | ALPHA: (ax1_933) implies: % 86.11/12.23 | (24) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 86.11/12.23 | (inregion(v0, v2) = v3) | ~ (inregion(v0, v1) = 0) | ~ $i(v2) | ~ % 86.11/12.23 | $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & inregion(v1, v2) % 86.11/12.23 | = v4)) % 86.11/12.23 | % 86.11/12.23 | ALPHA: (query124) implies: % 86.11/12.23 | (25) $i(c_tptpgeo_member7_mt) % 86.11/12.23 | (26) $i(c_geolocation_x53_y74) % 86.11/12.23 | (27) $i(c_georegion_l3_x17_y24) % 86.11/12.23 | (28) ? [v0: any] : ? [v1: any] : (geolevel_3(c_georegion_l3_x17_y24) = v1 % 86.11/12.23 | & inregion(c_geolocation_x53_y74, c_georegion_l3_x17_y24) = v0 & % 86.11/12.23 | mtvisible(c_tptpgeo_member7_mt) = 0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 86.11/12.23 | % 86.11/12.23 | ALPHA: (function-axioms) implies: % 86.11/12.24 | (29) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 86.11/12.24 | : (v1 = v0 | ~ (mtvisible(v2) = v1) | ~ (mtvisible(v2) = v0)) % 86.11/12.24 | (30) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 86.11/12.24 | : (v1 = v0 | ~ (geolevel_3(v2) = v1) | ~ (geolevel_3(v2) = v0)) % 86.11/12.24 | (31) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 86.11/12.24 | : ! [v3: $i] : (v1 = v0 | ~ (inregion(v3, v2) = v1) | ~ % 86.11/12.24 | (inregion(v3, v2) = v0)) % 86.11/12.24 | % 86.11/12.24 | DELTA: instantiating (18) with fresh symbols all_819_0, all_819_1 gives: % 86.11/12.24 | (32) geolevel_4(c_georegion_l4_x75_y75) = all_819_0 & % 86.11/12.24 | mtvisible(c_worldgeographymt) = all_819_1 & ( ~ (all_819_1 = 0) | % 86.11/12.24 | all_819_0 = 0) % 86.11/12.24 | % 86.11/12.24 | ALPHA: (32) implies: % 86.11/12.24 | (33) mtvisible(c_worldgeographymt) = all_819_1 % 86.11/12.24 | % 86.11/12.24 | DELTA: instantiating (23) with fresh symbols all_823_0, all_823_1 gives: % 86.11/12.24 | (34) borderson(c_georegion_l4_x29_y75, c_georegion_l4_x29_y76) = all_823_0 % 86.11/12.24 | & mtvisible(c_tptpgeo_member7_mt) = all_823_1 & ( ~ (all_823_1 = 0) | % 86.11/12.24 | all_823_0 = 0) % 86.11/12.24 | % 86.11/12.24 | ALPHA: (34) implies: % 86.11/12.24 | (35) mtvisible(c_tptpgeo_member7_mt) = all_823_1 % 86.11/12.24 | % 86.11/12.24 | DELTA: instantiating (3) with fresh symbols all_825_0, all_825_1 gives: % 86.11/12.24 | (36) inregion(c_geolocation_x53_y74, c_georegion_l4_x53_y74) = all_825_0 & % 86.11/12.24 | mtvisible(c_tptpgeo_member7_mt) = all_825_1 & ( ~ (all_825_1 = 0) | % 86.11/12.24 | all_825_0 = 0) % 86.11/12.24 | % 86.11/12.24 | ALPHA: (36) implies: % 86.11/12.24 | (37) mtvisible(c_tptpgeo_member7_mt) = all_825_1 % 86.11/12.24 | (38) inregion(c_geolocation_x53_y74, c_georegion_l4_x53_y74) = all_825_0 % 86.11/12.24 | (39) ~ (all_825_1 = 0) | all_825_0 = 0 % 86.11/12.24 | % 86.11/12.24 | DELTA: instantiating (10) with fresh symbols all_833_0, all_833_1 gives: % 86.11/12.24 | (40) geolevel_1(c_georegion_l1_x2_y0) = all_833_0 & % 86.11/12.24 | mtvisible(c_worldgeographymt) = all_833_1 & ( ~ (all_833_1 = 0) | % 86.11/12.24 | all_833_0 = 0) % 86.11/12.24 | % 86.11/12.24 | ALPHA: (40) implies: % 86.11/12.24 | (41) mtvisible(c_worldgeographymt) = all_833_1 % 86.11/12.24 | % 86.11/12.24 | DELTA: instantiating (9) with fresh symbols all_839_0, all_839_1 gives: % 86.11/12.24 | (42) mtvisible(c_tptpgeo_member7_mt) = all_839_1 & % 86.11/12.24 | geographicalsubregions(c_georegion_l2_x5_y8, c_georegion_l3_x15_y24) = % 86.11/12.24 | all_839_0 & ( ~ (all_839_1 = 0) | all_839_0 = 0) % 86.11/12.24 | % 86.11/12.24 | ALPHA: (42) implies: % 86.11/12.24 | (43) mtvisible(c_tptpgeo_member7_mt) = all_839_1 % 86.11/12.24 | % 86.11/12.24 | DELTA: instantiating (4) with fresh symbols all_845_0, all_845_1 gives: % 86.11/12.24 | (44) geolevel_3(c_georegion_l3_x4_y13) = all_845_0 & % 86.11/12.24 | mtvisible(c_worldgeographymt) = all_845_1 & ( ~ (all_845_1 = 0) | % 86.11/12.24 | all_845_0 = 0) % 86.11/12.24 | % 86.11/12.24 | ALPHA: (44) implies: % 86.11/12.24 | (45) mtvisible(c_worldgeographymt) = all_845_1 % 86.11/12.24 | % 86.11/12.24 | DELTA: instantiating (11) with fresh symbols all_847_0, all_847_1 gives: % 86.11/12.24 | (46) state_geopolitical(c_wanica_districtsuriname) = all_847_0 & % 86.11/12.24 | mtvisible(c_worldgeographymt) = all_847_1 & ( ~ (all_847_1 = 0) | % 86.11/12.24 | all_847_0 = 0) % 86.11/12.24 | % 86.11/12.24 | ALPHA: (46) implies: % 86.11/12.24 | (47) mtvisible(c_worldgeographymt) = all_847_1 % 86.11/12.24 | % 86.11/12.24 | DELTA: instantiating (5) with fresh symbols all_851_0, all_851_1 gives: % 86.11/12.24 | (48) borderson(c_georegion_l4_x27_y64, c_georegion_l4_x27_y65) = all_851_0 % 86.11/12.24 | & mtvisible(c_tptpgeo_member7_mt) = all_851_1 & ( ~ (all_851_1 = 0) | % 86.11/12.24 | all_851_0 = 0) % 86.11/12.24 | % 86.11/12.24 | ALPHA: (48) implies: % 86.11/12.24 | (49) mtvisible(c_tptpgeo_member7_mt) = all_851_1 % 86.11/12.24 | % 86.11/12.24 | DELTA: instantiating (7) with fresh symbols all_855_0, all_855_1 gives: % 86.11/12.24 | (50) mtvisible(c_tptpgeo_member7_mt) = all_855_1 & % 86.11/12.24 | geographicalsubregions(c_georegion_l3_x15_y24, c_georegion_l4_x45_y72) % 86.11/12.24 | = all_855_0 & ( ~ (all_855_1 = 0) | all_855_0 = 0) % 86.11/12.24 | % 86.11/12.24 | ALPHA: (50) implies: % 86.11/12.24 | (51) mtvisible(c_tptpgeo_member7_mt) = all_855_1 % 86.11/12.24 | % 86.11/12.24 | DELTA: instantiating (22) with fresh symbols all_857_0, all_857_1 gives: % 86.11/12.24 | (52) geolevel_3(c_georegion_l3_x17_y24) = all_857_0 & % 86.11/12.24 | mtvisible(c_worldgeographymt) = all_857_1 & ( ~ (all_857_1 = 0) | % 86.11/12.24 | all_857_0 = 0) % 86.11/12.24 | % 86.11/12.24 | ALPHA: (52) implies: % 86.11/12.24 | (53) mtvisible(c_worldgeographymt) = all_857_1 % 86.11/12.24 | (54) geolevel_3(c_georegion_l3_x17_y24) = all_857_0 % 86.11/12.24 | (55) ~ (all_857_1 = 0) | all_857_0 = 0 % 86.11/12.24 | % 86.11/12.24 | DELTA: instantiating (20) with fresh symbols all_871_0, all_871_1 gives: % 86.11/12.24 | (56) mtvisible(c_tptpgeo_member7_mt) = all_871_1 & % 86.11/12.24 | geographicalsubregions(c_georegion_l3_x17_y24, c_georegion_l4_x53_y74) % 86.11/12.24 | = all_871_0 & ( ~ (all_871_1 = 0) | all_871_0 = 0) % 86.11/12.24 | % 86.11/12.24 | ALPHA: (56) implies: % 86.11/12.24 | (57) geographicalsubregions(c_georegion_l3_x17_y24, c_georegion_l4_x53_y74) % 86.11/12.24 | = all_871_0 % 86.11/12.24 | (58) mtvisible(c_tptpgeo_member7_mt) = all_871_1 % 86.11/12.24 | (59) ~ (all_871_1 = 0) | all_871_0 = 0 % 86.11/12.24 | % 86.11/12.24 | DELTA: instantiating (28) with fresh symbols all_873_0, all_873_1 gives: % 86.11/12.24 | (60) geolevel_3(c_georegion_l3_x17_y24) = all_873_0 & % 86.11/12.24 | inregion(c_geolocation_x53_y74, c_georegion_l3_x17_y24) = all_873_1 & % 86.11/12.24 | mtvisible(c_tptpgeo_member7_mt) = 0 & ( ~ (all_873_0 = 0) | ~ % 86.11/12.24 | (all_873_1 = 0)) % 86.11/12.24 | % 86.11/12.24 | ALPHA: (60) implies: % 86.11/12.24 | (61) mtvisible(c_tptpgeo_member7_mt) = 0 % 86.11/12.24 | (62) inregion(c_geolocation_x53_y74, c_georegion_l3_x17_y24) = all_873_1 % 86.11/12.24 | (63) geolevel_3(c_georegion_l3_x17_y24) = all_873_0 % 86.11/12.24 | (64) ~ (all_873_0 = 0) | ~ (all_873_1 = 0) % 86.11/12.24 | % 86.11/12.24 | GROUND_INST: instantiating (29) with all_839_1, all_851_1, % 86.11/12.24 | c_tptpgeo_member7_mt, simplifying with (43), (49) gives: % 86.11/12.24 | (65) all_851_1 = all_839_1 % 86.11/12.24 | % 86.11/12.24 | GROUND_INST: instantiating (29) with all_825_1, all_851_1, % 86.11/12.24 | c_tptpgeo_member7_mt, simplifying with (37), (49) gives: % 86.11/12.24 | (66) all_851_1 = all_825_1 % 86.11/12.24 | % 86.11/12.24 | GROUND_INST: instantiating (29) with 0, all_851_1, c_tptpgeo_member7_mt, % 86.11/12.25 | simplifying with (49), (61) gives: % 86.11/12.25 | (67) all_851_1 = 0 % 86.11/12.25 | % 86.11/12.25 | GROUND_INST: instantiating (29) with all_839_1, all_855_1, % 86.11/12.25 | c_tptpgeo_member7_mt, simplifying with (43), (51) gives: % 86.11/12.25 | (68) all_855_1 = all_839_1 % 86.11/12.25 | % 86.11/12.25 | GROUND_INST: instantiating (29) with all_855_1, all_871_1, % 86.11/12.25 | c_tptpgeo_member7_mt, simplifying with (51), (58) gives: % 86.11/12.25 | (69) all_871_1 = all_855_1 % 86.11/12.25 | % 86.11/12.25 | GROUND_INST: instantiating (29) with all_823_1, all_871_1, % 86.11/12.25 | c_tptpgeo_member7_mt, simplifying with (35), (58) gives: % 86.11/12.25 | (70) all_871_1 = all_823_1 % 86.11/12.25 | % 86.11/12.25 | GROUND_INST: instantiating (29) with all_845_1, all_847_1, c_worldgeographymt, % 86.11/12.25 | simplifying with (45), (47) gives: % 86.11/12.25 | (71) all_847_1 = all_845_1 % 86.11/12.25 | % 86.11/12.25 | GROUND_INST: instantiating (29) with all_819_1, all_847_1, c_worldgeographymt, % 86.11/12.25 | simplifying with (33), (47) gives: % 86.11/12.25 | (72) all_847_1 = all_819_1 % 86.11/12.25 | % 86.11/12.25 | GROUND_INST: instantiating (29) with all_847_1, all_857_1, c_worldgeographymt, % 86.11/12.25 | simplifying with (47), (53) gives: % 86.11/12.25 | (73) all_857_1 = all_847_1 % 86.11/12.25 | % 86.11/12.25 | GROUND_INST: instantiating (29) with all_833_1, all_857_1, c_worldgeographymt, % 86.11/12.25 | simplifying with (41), (53) gives: % 86.11/12.25 | (74) all_857_1 = all_833_1 % 86.11/12.25 | % 86.11/12.25 | GROUND_INST: instantiating (30) with all_857_0, all_873_0, % 86.11/12.25 | c_georegion_l3_x17_y24, simplifying with (54), (63) gives: % 86.11/12.25 | (75) all_873_0 = all_857_0 % 86.11/12.25 | % 86.11/12.25 | COMBINE_EQS: (69), (70) imply: % 86.11/12.25 | (76) all_855_1 = all_823_1 % 86.11/12.25 | % 86.11/12.25 | SIMP: (76) implies: % 86.11/12.25 | (77) all_855_1 = all_823_1 % 86.11/12.25 | % 86.11/12.25 | COMBINE_EQS: (73), (74) imply: % 86.11/12.25 | (78) all_847_1 = all_833_1 % 86.11/12.25 | % 86.11/12.25 | SIMP: (78) implies: % 86.11/12.25 | (79) all_847_1 = all_833_1 % 86.11/12.25 | % 86.11/12.25 | COMBINE_EQS: (68), (77) imply: % 86.11/12.25 | (80) all_839_1 = all_823_1 % 86.11/12.25 | % 86.11/12.25 | SIMP: (80) implies: % 86.11/12.25 | (81) all_839_1 = all_823_1 % 86.11/12.25 | % 86.11/12.25 | COMBINE_EQS: (66), (67) imply: % 86.11/12.25 | (82) all_825_1 = 0 % 86.11/12.25 | % 86.11/12.25 | COMBINE_EQS: (65), (66) imply: % 86.11/12.25 | (83) all_839_1 = all_825_1 % 86.11/12.25 | % 86.11/12.25 | SIMP: (83) implies: % 86.11/12.25 | (84) all_839_1 = all_825_1 % 86.11/12.25 | % 86.11/12.25 | COMBINE_EQS: (71), (79) imply: % 86.11/12.25 | (85) all_845_1 = all_833_1 % 86.11/12.25 | % 86.11/12.25 | COMBINE_EQS: (71), (72) imply: % 86.11/12.25 | (86) all_845_1 = all_819_1 % 86.11/12.25 | % 86.11/12.25 | COMBINE_EQS: (85), (86) imply: % 86.11/12.25 | (87) all_833_1 = all_819_1 % 86.11/12.25 | % 86.11/12.25 | COMBINE_EQS: (81), (84) imply: % 86.11/12.25 | (88) all_825_1 = all_823_1 % 86.11/12.25 | % 86.11/12.25 | SIMP: (88) implies: % 86.11/12.25 | (89) all_825_1 = all_823_1 % 86.11/12.25 | % 86.11/12.25 | COMBINE_EQS: (82), (89) imply: % 86.11/12.25 | (90) all_823_1 = 0 % 86.11/12.25 | % 86.11/12.25 | SIMP: (90) implies: % 86.11/12.25 | (91) all_823_1 = 0 % 86.11/12.25 | % 86.11/12.25 | COMBINE_EQS: (74), (87) imply: % 86.11/12.25 | (92) all_857_1 = all_819_1 % 86.11/12.25 | % 86.11/12.25 | COMBINE_EQS: (70), (91) imply: % 86.11/12.25 | (93) all_871_1 = 0 % 86.11/12.25 | % 86.11/12.25 | BETA: splitting (59) gives: % 86.11/12.25 | % 86.11/12.25 | Case 1: % 86.11/12.25 | | % 86.11/12.25 | | (94) ~ (all_871_1 = 0) % 86.11/12.25 | | % 86.11/12.25 | | REDUCE: (93), (94) imply: % 86.11/12.25 | | (95) $false % 86.11/12.25 | | % 86.11/12.25 | | CLOSE: (95) is inconsistent. % 86.11/12.25 | | % 86.11/12.25 | Case 2: % 86.11/12.25 | | % 86.11/12.25 | | (96) all_871_0 = 0 % 86.11/12.25 | | % 86.11/12.25 | | REDUCE: (57), (96) imply: % 86.11/12.25 | | (97) geographicalsubregions(c_georegion_l3_x17_y24, % 86.11/12.25 | | c_georegion_l4_x53_y74) = 0 % 86.11/12.25 | | % 86.11/12.25 | | BETA: splitting (39) gives: % 86.11/12.25 | | % 86.11/12.25 | | Case 1: % 86.11/12.25 | | | % 86.11/12.25 | | | (98) ~ (all_825_1 = 0) % 86.11/12.25 | | | % 86.11/12.25 | | | REDUCE: (82), (98) imply: % 86.11/12.25 | | | (99) $false % 86.11/12.25 | | | % 86.11/12.25 | | | CLOSE: (99) is inconsistent. % 86.11/12.25 | | | % 86.11/12.25 | | Case 2: % 86.11/12.25 | | | % 86.11/12.25 | | | (100) all_825_0 = 0 % 86.11/12.25 | | | % 86.11/12.25 | | | REDUCE: (38), (100) imply: % 86.11/12.25 | | | (101) inregion(c_geolocation_x53_y74, c_georegion_l4_x53_y74) = 0 % 86.11/12.25 | | | % 86.11/12.25 | | | GROUND_INST: instantiating (ax1_1123) with c_tptpgeo_member8_mt, % 86.11/12.25 | | | c_tptpgeo_spindleheadmt, simplifying with (1), (12), (17) % 86.11/12.25 | | | gives: % 86.11/12.25 | | | (102) ? [v0: any] : ? [v1: any] : (mtvisible(c_tptpgeo_spindleheadmt) % 86.11/12.25 | | | = v1 & mtvisible(c_tptpgeo_member8_mt) = v0 & ( ~ (v0 = 0) | v1 % 86.11/12.25 | | | = 0)) % 86.11/12.25 | | | % 86.11/12.25 | | | GROUND_INST: instantiating (ax1_1123) with c_tptpgeo_spindleheadmt, % 86.11/12.25 | | | c_worldgeographymt, simplifying with (12), (13), (21) gives: % 86.11/12.25 | | | (103) ? [v0: any] : ? [v1: any] : (mtvisible(c_worldgeographymt) = v1 % 86.11/12.25 | | | & mtvisible(c_tptpgeo_spindleheadmt) = v0 & ( ~ (v0 = 0) | v1 = % 86.11/12.25 | | | 0)) % 86.11/12.25 | | | % 86.11/12.25 | | | GROUND_INST: instantiating (ax1_1123) with c_tptpgeo_member7_mt, % 86.11/12.25 | | | c_tptpgeo_spindleheadmt, simplifying with (2), (12), (25) % 86.11/12.25 | | | gives: % 86.11/12.26 | | | (104) ? [v0: any] : ? [v1: any] : (mtvisible(c_tptpgeo_member7_mt) = % 86.11/12.26 | | | v0 & mtvisible(c_tptpgeo_spindleheadmt) = v1 & ( ~ (v0 = 0) | % 86.11/12.26 | | | v1 = 0)) % 86.11/12.26 | | | % 86.11/12.26 | | | GROUND_INST: instantiating (ax1_1123) with c_worldgeographymt, % 86.11/12.26 | | | c_geographymt, simplifying with (14), (15), (21) gives: % 86.11/12.26 | | | (105) ? [v0: any] : ? [v1: any] : (mtvisible(c_geographymt) = v1 & % 86.11/12.26 | | | mtvisible(c_worldgeographymt) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 86.11/12.26 | | | % 86.11/12.26 | | | GROUND_INST: instantiating (ax1_1123) with c_tptpgeo_member3_mt, % 86.11/12.26 | | | c_tptpgeo_spindleheadmt, simplifying with (8), (12), (16) % 86.11/12.26 | | | gives: % 86.11/12.26 | | | (106) ? [v0: any] : ? [v1: any] : (mtvisible(c_tptpgeo_member3_mt) = % 86.11/12.26 | | | v0 & mtvisible(c_tptpgeo_spindleheadmt) = v1 & ( ~ (v0 = 0) | % 86.11/12.26 | | | v1 = 0)) % 86.11/12.26 | | | % 86.11/12.26 | | | GROUND_INST: instantiating (6) with c_georegion_l3_x17_y24, % 86.11/12.26 | | | c_georegion_l4_x53_y74, simplifying with (19), (27), (97) % 86.11/12.26 | | | gives: % 86.11/12.26 | | | (107) inregion(c_georegion_l4_x53_y74, c_georegion_l3_x17_y24) = 0 % 86.11/12.26 | | | % 86.11/12.26 | | | GROUND_INST: instantiating (24) with c_geolocation_x53_y74, % 86.11/12.26 | | | c_georegion_l4_x53_y74, c_georegion_l3_x17_y24, all_873_1, % 86.11/12.26 | | | simplifying with (19), (26), (27), (62), (101) gives: % 86.11/12.26 | | | (108) all_873_1 = 0 | ? [v0: int] : ( ~ (v0 = 0) & % 86.11/12.26 | | | inregion(c_georegion_l4_x53_y74, c_georegion_l3_x17_y24) = v0) % 86.11/12.26 | | | % 86.11/12.26 | | | DELTA: instantiating (104) with fresh symbols all_1095_0, all_1095_1 % 86.11/12.26 | | | gives: % 86.11/12.26 | | | (109) mtvisible(c_tptpgeo_member7_mt) = all_1095_1 & % 86.11/12.26 | | | mtvisible(c_tptpgeo_spindleheadmt) = all_1095_0 & ( ~ (all_1095_1 % 86.11/12.26 | | | = 0) | all_1095_0 = 0) % 86.11/12.26 | | | % 86.11/12.26 | | | ALPHA: (109) implies: % 86.11/12.26 | | | (110) mtvisible(c_tptpgeo_spindleheadmt) = all_1095_0 % 86.11/12.26 | | | (111) mtvisible(c_tptpgeo_member7_mt) = all_1095_1 % 86.11/12.26 | | | (112) ~ (all_1095_1 = 0) | all_1095_0 = 0 % 86.11/12.26 | | | % 86.11/12.26 | | | DELTA: instantiating (105) with fresh symbols all_1097_0, all_1097_1 % 86.11/12.26 | | | gives: % 86.11/12.26 | | | (113) mtvisible(c_geographymt) = all_1097_0 & % 86.11/12.26 | | | mtvisible(c_worldgeographymt) = all_1097_1 & ( ~ (all_1097_1 = 0) % 86.11/12.26 | | | | all_1097_0 = 0) % 86.11/12.26 | | | % 86.11/12.26 | | | ALPHA: (113) implies: % 86.11/12.26 | | | (114) mtvisible(c_worldgeographymt) = all_1097_1 % 86.11/12.26 | | | % 86.11/12.26 | | | DELTA: instantiating (106) with fresh symbols all_1135_0, all_1135_1 % 86.11/12.26 | | | gives: % 86.11/12.26 | | | (115) mtvisible(c_tptpgeo_member3_mt) = all_1135_1 & % 86.11/12.26 | | | mtvisible(c_tptpgeo_spindleheadmt) = all_1135_0 & ( ~ (all_1135_1 % 86.11/12.26 | | | = 0) | all_1135_0 = 0) % 86.11/12.26 | | | % 86.11/12.26 | | | ALPHA: (115) implies: % 86.11/12.26 | | | (116) mtvisible(c_tptpgeo_spindleheadmt) = all_1135_0 % 86.11/12.26 | | | % 86.11/12.26 | | | DELTA: instantiating (103) with fresh symbols all_1179_0, all_1179_1 % 86.11/12.26 | | | gives: % 86.11/12.26 | | | (117) mtvisible(c_worldgeographymt) = all_1179_0 & % 86.11/12.26 | | | mtvisible(c_tptpgeo_spindleheadmt) = all_1179_1 & ( ~ (all_1179_1 % 86.11/12.26 | | | = 0) | all_1179_0 = 0) % 86.11/12.26 | | | % 86.11/12.26 | | | ALPHA: (117) implies: % 86.11/12.26 | | | (118) mtvisible(c_tptpgeo_spindleheadmt) = all_1179_1 % 86.11/12.26 | | | (119) mtvisible(c_worldgeographymt) = all_1179_0 % 86.11/12.26 | | | (120) ~ (all_1179_1 = 0) | all_1179_0 = 0 % 86.11/12.26 | | | % 86.11/12.26 | | | DELTA: instantiating (102) with fresh symbols all_1183_0, all_1183_1 % 86.11/12.26 | | | gives: % 86.11/12.26 | | | (121) mtvisible(c_tptpgeo_spindleheadmt) = all_1183_0 & % 86.11/12.26 | | | mtvisible(c_tptpgeo_member8_mt) = all_1183_1 & ( ~ (all_1183_1 = % 86.11/12.26 | | | 0) | all_1183_0 = 0) % 86.11/12.26 | | | % 86.11/12.26 | | | ALPHA: (121) implies: % 86.11/12.26 | | | (122) mtvisible(c_tptpgeo_spindleheadmt) = all_1183_0 % 86.11/12.26 | | | % 86.11/12.26 | | | BETA: splitting (108) gives: % 86.11/12.26 | | | % 86.11/12.26 | | | Case 1: % 86.11/12.26 | | | | % 86.11/12.26 | | | | (123) all_873_1 = 0 % 86.11/12.26 | | | | % 86.11/12.26 | | | | BETA: splitting (64) gives: % 86.11/12.26 | | | | % 86.11/12.26 | | | | Case 1: % 86.11/12.26 | | | | | % 86.11/12.26 | | | | | (124) ~ (all_873_0 = 0) % 86.11/12.26 | | | | | % 86.11/12.26 | | | | | REDUCE: (75), (124) imply: % 86.11/12.26 | | | | | (125) ~ (all_857_0 = 0) % 86.11/12.26 | | | | | % 86.11/12.26 | | | | | BETA: splitting (55) gives: % 86.11/12.26 | | | | | % 86.11/12.26 | | | | | Case 1: % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | | (126) ~ (all_857_1 = 0) % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | | REDUCE: (92), (126) imply: % 86.11/12.26 | | | | | | (127) ~ (all_819_1 = 0) % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | | GROUND_INST: instantiating (29) with all_1135_0, all_1179_1, % 86.11/12.26 | | | | | | c_tptpgeo_spindleheadmt, simplifying with (116), (118) % 86.11/12.26 | | | | | | gives: % 86.11/12.26 | | | | | | (128) all_1179_1 = all_1135_0 % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | | GROUND_INST: instantiating (29) with all_1179_1, all_1183_0, % 86.11/12.26 | | | | | | c_tptpgeo_spindleheadmt, simplifying with (118), (122) % 86.11/12.26 | | | | | | gives: % 86.11/12.26 | | | | | | (129) all_1183_0 = all_1179_1 % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | | GROUND_INST: instantiating (29) with all_1095_0, all_1183_0, % 86.11/12.26 | | | | | | c_tptpgeo_spindleheadmt, simplifying with (110), (122) % 86.11/12.26 | | | | | | gives: % 86.11/12.26 | | | | | | (130) all_1183_0 = all_1095_0 % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | | GROUND_INST: instantiating (29) with 0, all_1095_1, % 86.11/12.26 | | | | | | c_tptpgeo_member7_mt, simplifying with (61), (111) % 86.11/12.26 | | | | | | gives: % 86.11/12.26 | | | | | | (131) all_1095_1 = 0 % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | | GROUND_INST: instantiating (29) with all_819_1, all_1179_0, % 86.11/12.26 | | | | | | c_worldgeographymt, simplifying with (33), (119) gives: % 86.11/12.26 | | | | | | (132) all_1179_0 = all_819_1 % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | | GROUND_INST: instantiating (29) with all_1097_1, all_1179_0, % 86.11/12.26 | | | | | | c_worldgeographymt, simplifying with (114), (119) % 86.11/12.26 | | | | | | gives: % 86.11/12.26 | | | | | | (133) all_1179_0 = all_1097_1 % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | | COMBINE_EQS: (129), (130) imply: % 86.11/12.26 | | | | | | (134) all_1179_1 = all_1095_0 % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | | SIMP: (134) implies: % 86.11/12.26 | | | | | | (135) all_1179_1 = all_1095_0 % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | | COMBINE_EQS: (132), (133) imply: % 86.11/12.26 | | | | | | (136) all_1097_1 = all_819_1 % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | | COMBINE_EQS: (128), (135) imply: % 86.11/12.26 | | | | | | (137) all_1135_0 = all_1095_0 % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | | BETA: splitting (112) gives: % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | | Case 1: % 86.11/12.26 | | | | | | | % 86.11/12.26 | | | | | | | (138) ~ (all_1095_1 = 0) % 86.11/12.26 | | | | | | | % 86.11/12.26 | | | | | | | REDUCE: (131), (138) imply: % 86.11/12.26 | | | | | | | (139) $false % 86.11/12.26 | | | | | | | % 86.11/12.26 | | | | | | | CLOSE: (139) is inconsistent. % 86.11/12.26 | | | | | | | % 86.11/12.26 | | | | | | Case 2: % 86.11/12.26 | | | | | | | % 86.11/12.26 | | | | | | | (140) all_1095_0 = 0 % 86.11/12.26 | | | | | | | % 86.11/12.26 | | | | | | | COMBINE_EQS: (135), (140) imply: % 86.11/12.26 | | | | | | | (141) all_1179_1 = 0 % 86.11/12.26 | | | | | | | % 86.11/12.26 | | | | | | | BETA: splitting (120) gives: % 86.11/12.26 | | | | | | | % 86.11/12.26 | | | | | | | Case 1: % 86.11/12.26 | | | | | | | | % 86.11/12.26 | | | | | | | | (142) ~ (all_1179_1 = 0) % 86.11/12.26 | | | | | | | | % 86.11/12.26 | | | | | | | | REDUCE: (141), (142) imply: % 86.11/12.26 | | | | | | | | (143) $false % 86.11/12.26 | | | | | | | | % 86.11/12.26 | | | | | | | | CLOSE: (143) is inconsistent. % 86.11/12.26 | | | | | | | | % 86.11/12.26 | | | | | | | Case 2: % 86.11/12.26 | | | | | | | | % 86.11/12.26 | | | | | | | | (144) all_1179_0 = 0 % 86.11/12.26 | | | | | | | | % 86.11/12.26 | | | | | | | | COMBINE_EQS: (132), (144) imply: % 86.11/12.26 | | | | | | | | (145) all_819_1 = 0 % 86.11/12.26 | | | | | | | | % 86.11/12.26 | | | | | | | | SIMP: (145) implies: % 86.11/12.26 | | | | | | | | (146) all_819_1 = 0 % 86.11/12.26 | | | | | | | | % 86.11/12.26 | | | | | | | | REDUCE: (127), (146) imply: % 86.11/12.26 | | | | | | | | (147) $false % 86.11/12.26 | | | | | | | | % 86.11/12.26 | | | | | | | | CLOSE: (147) is inconsistent. % 86.11/12.26 | | | | | | | | % 86.11/12.26 | | | | | | | End of split % 86.11/12.26 | | | | | | | % 86.11/12.26 | | | | | | End of split % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | Case 2: % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | | (148) all_857_0 = 0 % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | | REDUCE: (125), (148) imply: % 86.11/12.26 | | | | | | (149) $false % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | | CLOSE: (149) is inconsistent. % 86.11/12.26 | | | | | | % 86.11/12.26 | | | | | End of split % 86.11/12.26 | | | | | % 86.11/12.26 | | | | Case 2: % 86.11/12.26 | | | | | % 86.11/12.26 | | | | | (150) ~ (all_873_1 = 0) % 86.11/12.26 | | | | | % 86.11/12.26 | | | | | REDUCE: (123), (150) imply: % 86.11/12.26 | | | | | (151) $false % 86.11/12.26 | | | | | % 86.11/12.26 | | | | | CLOSE: (151) is inconsistent. % 86.11/12.26 | | | | | % 86.11/12.26 | | | | End of split % 86.11/12.26 | | | | % 86.11/12.26 | | | Case 2: % 86.11/12.26 | | | | % 86.11/12.26 | | | | (152) ? [v0: int] : ( ~ (v0 = 0) & inregion(c_georegion_l4_x53_y74, % 86.11/12.26 | | | | c_georegion_l3_x17_y24) = v0) % 86.11/12.26 | | | | % 86.11/12.27 | | | | DELTA: instantiating (152) with fresh symbol all_1189_0 gives: % 86.11/12.27 | | | | (153) ~ (all_1189_0 = 0) & inregion(c_georegion_l4_x53_y74, % 86.11/12.27 | | | | c_georegion_l3_x17_y24) = all_1189_0 % 86.11/12.27 | | | | % 86.11/12.27 | | | | ALPHA: (153) implies: % 86.11/12.27 | | | | (154) ~ (all_1189_0 = 0) % 86.11/12.27 | | | | (155) inregion(c_georegion_l4_x53_y74, c_georegion_l3_x17_y24) = % 86.11/12.27 | | | | all_1189_0 % 86.11/12.27 | | | | % 86.11/12.27 | | | | GROUND_INST: instantiating (31) with 0, all_1189_0, % 86.11/12.27 | | | | c_georegion_l3_x17_y24, c_georegion_l4_x53_y74, simplifying % 86.11/12.27 | | | | with (107), (155) gives: % 86.11/12.27 | | | | (156) all_1189_0 = 0 % 86.11/12.27 | | | | % 86.11/12.27 | | | | REDUCE: (154), (156) imply: % 86.11/12.27 | | | | (157) $false % 86.11/12.27 | | | | % 86.11/12.27 | | | | CLOSE: (157) is inconsistent. % 86.11/12.27 | | | | % 86.11/12.27 | | | End of split % 86.11/12.27 | | | % 86.11/12.27 | | End of split % 86.11/12.27 | | % 86.11/12.27 | End of split % 86.11/12.27 | % 86.11/12.27 End of proof % 86.44/12.27 % SZS output end Proof for theBenchmark % 86.44/12.27 % 86.44/12.27 11639ms %------------------------------------------------------------------------------