%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : NUM482+1 : TPTP v8.1.2. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n005.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 : Thu Aug 31 11:48:04 EDT 2023 % Result : Theorem 34.28s 5.39s % Output : Proof 152.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.13 % Problem : NUM482+1 : TPTP v8.1.2. Released v4.0.0. % 0.06/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.11/0.33 % Computer : n005.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Fri Aug 25 15:00:53 EDT 2023 % 0.11/0.33 % CPUTime : % 0.16/0.61 ________ _____ % 0.16/0.61 ___ __ \_________(_)________________________________ % 0.16/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.16/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.16/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.16/0.61 % 0.16/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.16/0.61 (2023-06-19) % 0.16/0.61 % 0.16/0.61 (c) Philipp Rümmer, 2009-2023 % 0.16/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.16/0.61 Amanda Stjerna. % 0.16/0.61 Free software under BSD-3-Clause. % 0.16/0.61 % 0.16/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.16/0.61 % 0.16/0.62 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.16/0.63 Running up to 7 provers in parallel. % 0.16/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.16/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.16/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.16/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.16/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.16/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.16/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 2.78/1.27 Prover 4: Preprocessing ... % 2.78/1.27 Prover 1: Preprocessing ... % 3.76/1.33 Prover 6: Preprocessing ... % 3.76/1.33 Prover 5: Preprocessing ... % 3.76/1.33 Prover 3: Preprocessing ... % 3.76/1.33 Prover 2: Preprocessing ... % 3.76/1.33 Prover 0: Preprocessing ... % 10.91/2.29 Prover 1: Constructing countermodel ... % 10.91/2.31 Prover 3: Constructing countermodel ... % 11.48/2.40 Prover 6: Proving ... % 11.82/2.43 Prover 5: Constructing countermodel ... % 12.78/2.55 Prover 3: gave up % 12.78/2.56 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 12.78/2.66 Prover 1: gave up % 13.68/2.67 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 13.68/2.71 Prover 7: Preprocessing ... % 13.68/2.73 Prover 8: Preprocessing ... % 15.21/2.86 Prover 2: Proving ... % 15.21/2.95 Prover 4: Constructing countermodel ... % 16.21/2.99 Prover 8: Warning: ignoring some quantifiers % 16.21/3.01 Prover 8: Constructing countermodel ... % 17.57/3.16 Prover 7: Constructing countermodel ... % 17.57/3.30 Prover 0: Proving ... % 19.25/3.44 Prover 8: gave up % 19.70/3.46 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 20.49/3.56 Prover 9: Preprocessing ... % 26.79/4.45 Prover 9: Constructing countermodel ... % 34.28/5.39 Prover 0: proved (4735ms) % 34.28/5.39 % 34.28/5.39 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 34.28/5.39 % 34.28/5.39 Prover 5: stopped % 34.28/5.39 Prover 2: stopped % 34.28/5.40 Prover 6: stopped % 34.28/5.40 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 34.28/5.40 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 34.28/5.40 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 34.28/5.40 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 34.28/5.40 Prover 9: stopped % 34.28/5.42 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 34.87/5.49 Prover 11: Preprocessing ... % 34.87/5.50 Prover 10: Preprocessing ... % 35.28/5.53 Prover 13: Preprocessing ... % 35.28/5.53 Prover 16: Preprocessing ... % 35.28/5.53 Prover 19: Preprocessing ... % 36.25/5.67 Prover 16: Constructing countermodel ... % 36.25/5.67 Prover 10: Constructing countermodel ... % 37.10/5.79 Prover 13: Constructing countermodel ... % 37.88/5.87 Prover 19: Warning: ignoring some quantifiers % 37.88/5.89 Prover 19: Constructing countermodel ... % 38.61/6.12 Prover 11: Constructing countermodel ... % 43.76/6.62 Prover 19: gave up % 74.46/10.64 Prover 13: stopped % 82.82/11.79 Prover 16: stopped % 151.11/23.58 Prover 11: Found proof (size 309) % 151.11/23.58 Prover 11: proved (18182ms) % 151.39/23.58 Prover 7: stopped % 151.39/23.58 Prover 4: stopped % 151.39/23.59 Prover 10: stopped % 151.39/23.59 % 151.39/23.59 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 151.39/23.59 % 151.39/23.63 % SZS output start Proof for theBenchmark % 151.39/23.64 Assumptions after simplification: % 151.39/23.64 --------------------------------- % 151.39/23.64 % 151.39/23.64 (mAMDistr) % 151.72/23.71 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 151.72/23.71 $i] : ( ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v1, v0) = v3) | ~ % 151.72/23.71 (sdtpldt0(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: int] : % 151.72/23.71 ? [v7: int] : ? [v8: int] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? % 151.72/23.71 [v12: $i] : ? [v13: $i] : ? [v14: $i] : ((v14 = v5 & v13 = v10 & % 151.72/23.71 sdtasdt0(v9, v0) = v5 & sdtasdt0(v0, v9) = v10 & sdtasdt0(v0, v2) = v12 % 151.72/23.71 & sdtasdt0(v0, v1) = v11 & sdtpldt0(v11, v12) = v10 & sdtpldt0(v1, v2) = % 151.72/23.71 v9 & $i(v12) & $i(v11) & $i(v10) & $i(v9) & $i(v5)) | ( ~ (v8 = 0) & % 151.72/23.71 aNaturalNumber0(v2) = v8) | ( ~ (v7 = 0) & aNaturalNumber0(v1) = v7) | ( % 151.72/23.71 ~ (v6 = 0) & aNaturalNumber0(v0) = v6))) & ! [v0: $i] : ! [v1: $i] : % 151.72/23.71 ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ (sdtasdt0(v0, v2) = % 151.72/23.71 v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ $i(v2) % 151.72/23.71 | ~ $i(v1) | ~ $i(v0) | ? [v6: int] : ? [v7: int] : ? [v8: int] : ? % 151.72/23.71 [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? % 151.72/23.71 [v14: $i] : ((v14 = v11 & v10 = v5 & sdtasdt0(v9, v0) = v11 & sdtasdt0(v2, % 151.72/23.71 v0) = v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v9) = v5 & % 151.72/23.71 sdtpldt0(v12, v13) = v11 & sdtpldt0(v1, v2) = v9 & $i(v13) & $i(v12) & % 151.72/23.71 $i(v11) & $i(v9) & $i(v5)) | ( ~ (v8 = 0) & aNaturalNumber0(v2) = v8) | % 151.72/23.71 ( ~ (v7 = 0) & aNaturalNumber0(v1) = v7) | ( ~ (v6 = 0) & % 151.72/23.71 aNaturalNumber0(v0) = v6))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 151.72/23.71 ! [v3: $i] : ! [v4: $i] : ( ~ (sdtasdt0(v3, v0) = v4) | ~ (sdtpldt0(v1, v2) % 151.72/23.71 = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : % 151.72/23.71 ? [v7: int] : ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? % 151.72/23.71 [v12: $i] : ? [v13: $i] : ? [v14: $i] : ((v14 = v4 & v11 = v8 & % 151.72/23.71 sdtasdt0(v2, v0) = v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v3) = v8 % 151.72/23.71 & sdtasdt0(v0, v2) = v10 & sdtasdt0(v0, v1) = v9 & sdtpldt0(v12, v13) = % 151.72/23.71 v4 & sdtpldt0(v9, v10) = v8 & $i(v13) & $i(v12) & $i(v10) & $i(v9) & % 151.72/23.71 $i(v8) & $i(v4)) | ( ~ (v7 = 0) & aNaturalNumber0(v2) = v7) | ( ~ (v6 = % 151.72/23.71 0) & aNaturalNumber0(v1) = v6) | ( ~ (v5 = 0) & aNaturalNumber0(v0) = % 151.72/23.71 v5))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 151.72/23.71 $i] : ( ~ (sdtasdt0(v0, v3) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ $i(v2) | % 151.72/23.71 ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : ? [v7: int] : ? [v8: % 151.72/23.71 $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: % 151.72/23.71 $i] : ? [v14: $i] : ((v14 = v11 & v10 = v4 & sdtasdt0(v3, v0) = v11 & % 151.72/23.71 sdtasdt0(v2, v0) = v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v2) = v9 % 151.72/23.71 & sdtasdt0(v0, v1) = v8 & sdtpldt0(v12, v13) = v11 & sdtpldt0(v8, v9) = % 151.72/23.71 v4 & $i(v13) & $i(v12) & $i(v11) & $i(v9) & $i(v8) & $i(v4)) | ( ~ (v7 = % 151.72/23.71 0) & aNaturalNumber0(v2) = v7) | ( ~ (v6 = 0) & aNaturalNumber0(v1) = % 151.72/23.71 v6) | ( ~ (v5 = 0) & aNaturalNumber0(v0) = v5))) % 151.72/23.71 % 151.72/23.72 (mAddCanc) % 151.72/23.73 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v2 = v1 % 151.72/23.73 | ~ (sdtpldt0(v2, v0) = v4) | ~ (sdtpldt0(v1, v0) = v3) | ~ $i(v2) | ~ % 151.72/23.73 $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : ? [v7: int] : ? [v8: % 151.72/23.73 $i] : ? [v9: $i] : (( ~ (v9 = v8) & ~ (v4 = v3) & sdtpldt0(v0, v2) = v9 % 151.72/23.73 & sdtpldt0(v0, v1) = v8 & $i(v9) & $i(v8)) | ( ~ (v7 = 0) & % 151.72/23.73 aNaturalNumber0(v2) = v7) | ( ~ (v6 = 0) & aNaturalNumber0(v1) = v6) | ( % 151.72/23.73 ~ (v5 = 0) & aNaturalNumber0(v0) = v5))) & ! [v0: $i] : ! [v1: $i] : % 151.72/23.73 ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v2 = v1 | ~ (sdtpldt0(v2, v0) = v4) % 151.72/23.73 | ~ (sdtpldt0(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: % 151.72/23.73 int] : ? [v6: int] : ? [v7: int] : ? [v8: $i] : ? [v9: $i] : (( ~ (v9 % 151.72/23.73 = v4) & ~ (v8 = v3) & sdtpldt0(v1, v0) = v9 & sdtpldt0(v0, v2) = v8 & % 151.72/23.73 $i(v9) & $i(v8)) | ( ~ (v7 = 0) & aNaturalNumber0(v2) = v7) | ( ~ (v6 = % 151.72/23.73 0) & aNaturalNumber0(v1) = v6) | ( ~ (v5 = 0) & aNaturalNumber0(v0) = % 151.72/23.73 v5))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 151.72/23.73 $i] : (v2 = v1 | ~ (sdtpldt0(v1, v0) = v4) | ~ (sdtpldt0(v0, v2) = v3) | % 151.72/23.73 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : ? [v7: % 151.72/23.73 int] : ? [v8: $i] : ? [v9: $i] : (( ~ (v9 = v4) & ~ (v8 = v3) & % 151.72/23.73 sdtpldt0(v2, v0) = v9 & sdtpldt0(v0, v1) = v8 & $i(v9) & $i(v8)) | ( ~ % 151.72/23.73 (v7 = 0) & aNaturalNumber0(v2) = v7) | ( ~ (v6 = 0) & % 151.72/23.73 aNaturalNumber0(v1) = v6) | ( ~ (v5 = 0) & aNaturalNumber0(v0) = v5))) & % 151.72/23.73 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v2 = v1 % 151.72/23.73 | ~ (sdtpldt0(v0, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ $i(v2) | ~ % 151.72/23.73 $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : ? [v7: int] : ? [v8: % 151.72/23.73 $i] : ? [v9: $i] : (( ~ (v9 = v8) & ~ (v4 = v3) & sdtpldt0(v2, v0) = v9 % 151.72/23.73 & sdtpldt0(v1, v0) = v8 & $i(v9) & $i(v8)) | ( ~ (v7 = 0) & % 151.72/23.73 aNaturalNumber0(v2) = v7) | ( ~ (v6 = 0) & aNaturalNumber0(v1) = v6) | ( % 151.72/23.73 ~ (v5 = 0) & aNaturalNumber0(v0) = v5))) & ! [v0: $i] : ! [v1: $i] : % 151.72/23.73 ! [v2: $i] : ! [v3: $i] : (v2 = v1 | ~ (sdtpldt0(v2, v0) = v3) | ~ % 151.72/23.73 (aNaturalNumber0(v1) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] % 151.72/23.73 : ? [v5: int] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : (( ~ (v8 = v3) & % 151.72/23.73 ~ (v7 = v6) & sdtpldt0(v1, v0) = v8 & sdtpldt0(v0, v2) = v7 & % 151.72/23.73 sdtpldt0(v0, v1) = v6 & $i(v8) & $i(v7) & $i(v6)) | ( ~ (v5 = 0) & % 151.72/23.73 aNaturalNumber0(v2) = v5) | ( ~ (v4 = 0) & aNaturalNumber0(v0) = v4))) & % 151.72/23.73 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v2 = v1 | ~ % 151.72/23.73 (sdtpldt0(v1, v0) = v3) | ~ (aNaturalNumber0(v2) = 0) | ~ $i(v2) | ~ % 151.72/23.73 $i(v1) | ~ $i(v0) | ? [v4: int] : ? [v5: int] : ? [v6: $i] : ? [v7: $i] % 151.72/23.73 : ? [v8: $i] : (( ~ (v8 = v3) & ~ (v7 = v6) & sdtpldt0(v2, v0) = v8 & % 151.72/23.73 sdtpldt0(v0, v2) = v7 & sdtpldt0(v0, v1) = v6 & $i(v8) & $i(v7) & % 151.72/23.73 $i(v6)) | ( ~ (v5 = 0) & aNaturalNumber0(v1) = v5) | ( ~ (v4 = 0) & % 151.72/23.73 aNaturalNumber0(v0) = v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 151.72/23.73 ! [v3: $i] : (v2 = v1 | ~ (sdtpldt0(v0, v2) = v3) | ~ (aNaturalNumber0(v1) = % 151.72/23.73 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ? [v5: int] : ? % 151.72/23.73 [v6: $i] : ? [v7: $i] : ? [v8: $i] : (( ~ (v8 = v7) & ~ (v6 = v3) & % 151.72/23.73 sdtpldt0(v2, v0) = v8 & sdtpldt0(v1, v0) = v7 & sdtpldt0(v0, v1) = v6 & % 151.72/23.73 $i(v8) & $i(v7) & $i(v6)) | ( ~ (v5 = 0) & aNaturalNumber0(v2) = v5) | ( % 151.72/23.73 ~ (v4 = 0) & aNaturalNumber0(v0) = v4))) & ! [v0: $i] : ! [v1: $i] : % 151.72/23.73 ! [v2: $i] : ! [v3: $i] : (v2 = v1 | ~ (sdtpldt0(v0, v1) = v3) | ~ % 151.72/23.73 (aNaturalNumber0(v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] % 151.72/23.73 : ? [v5: int] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : (( ~ (v8 = v7) & % 151.72/23.73 ~ (v6 = v3) & sdtpldt0(v2, v0) = v8 & sdtpldt0(v1, v0) = v7 & % 151.72/23.73 sdtpldt0(v0, v2) = v6 & $i(v8) & $i(v7) & $i(v6)) | ( ~ (v5 = 0) & % 151.72/23.73 aNaturalNumber0(v1) = v5) | ( ~ (v4 = 0) & aNaturalNumber0(v0) = v4))) & % 151.72/23.73 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ (aNaturalNumber0(v2) = % 151.72/23.73 0) | ~ (aNaturalNumber0(v1) = 0) | ~ (aNaturalNumber0(v0) = 0) | ~ % 151.72/23.73 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 151.72/23.73 ? [v6: $i] : ( ~ (v6 = v5) & ~ (v4 = v3) & sdtpldt0(v2, v0) = v6 & % 151.72/23.73 sdtpldt0(v1, v0) = v5 & sdtpldt0(v0, v2) = v4 & sdtpldt0(v0, v1) = v3 & % 151.72/23.73 $i(v6) & $i(v5) & $i(v4) & $i(v3))) % 151.72/23.73 % 151.72/23.73 (mDefDiv) % 151.72/23.74 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : ! [v3: $i] : (v2 = 0 | ~ % 151.72/23.74 (doDivides0(v0, v1) = v2) | ~ (sdtasdt0(v0, v3) = v1) | ~ $i(v3) | ~ % 151.72/23.74 $i(v1) | ~ $i(v0) | ? [v4: int] : ? [v5: int] : (( ~ (v5 = 0) & % 151.72/23.74 aNaturalNumber0(v1) = v5) | ( ~ (v4 = 0) & aNaturalNumber0(v3) = v4) | ( % 151.72/23.74 ~ (v4 = 0) & aNaturalNumber0(v0) = v4))) & ! [v0: $i] : ! [v1: $i] : % 151.72/23.74 ! [v2: int] : ! [v3: $i] : (v2 = 0 | ~ (doDivides0(v0, v1) = v2) | ~ % 151.72/23.74 (aNaturalNumber0(v3) = 0) | ~ $i(v3) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] % 151.72/23.74 : ? [v5: int] : (( ~ (v5 = 0) & aNaturalNumber0(v1) = v5) | ( ~ (v4 = v1) & % 151.72/23.74 sdtasdt0(v0, v3) = v4 & $i(v4)) | ( ~ (v4 = 0) & aNaturalNumber0(v0) = % 151.72/23.74 v4))) & ! [v0: $i] : ! [v1: $i] : ( ~ (doDivides0(v0, v1) = 0) | ~ % 151.72/23.74 $i(v1) | ~ $i(v0) | ? [v2: int] : ? [v3: int] : ? [v4: $i] : ? [v5: % 151.72/23.74 int] : ? [v6: $i] : ($i(v4) & ((v6 = v1 & v5 = 0 & sdtasdt0(v0, v4) = v1 % 151.72/23.74 & aNaturalNumber0(v4) = 0) | ( ~ (v3 = 0) & aNaturalNumber0(v1) = v3) % 151.72/23.74 | ( ~ (v2 = 0) & aNaturalNumber0(v0) = v2)))) % 151.72/23.74 % 151.72/23.74 (mDefPrime) % 151.72/23.74 $i(sz10) & $i(sz00) & ! [v0: $i] : ! [v1: $i] : (v1 = v0 | v1 = sz10 | ~ % 151.72/23.74 (isPrime0(v0) = 0) | ~ (doDivides0(v1, v0) = 0) | ~ $i(v1) | ~ $i(v0) | % 151.72/23.74 ? [v2: int] : (( ~ (v2 = 0) & aNaturalNumber0(v1) = v2) | ( ~ (v2 = 0) & % 151.72/23.74 aNaturalNumber0(v0) = v2))) & ! [v0: $i] : ! [v1: $i] : (v1 = v0 | v1 % 151.72/23.74 = sz10 | ~ (isPrime0(v0) = 0) | ~ (aNaturalNumber0(v1) = 0) | ~ $i(v1) | % 151.72/23.74 ~ $i(v0) | ? [v2: int] : (( ~ (v2 = 0) & doDivides0(v1, v0) = v2) | ( ~ (v2 % 151.72/23.74 = 0) & aNaturalNumber0(v0) = v2))) & ! [v0: $i] : ! [v1: int] : (v1 % 151.72/23.74 = 0 | v0 = sz10 | v0 = sz00 | ~ (isPrime0(v0) = v1) | ~ $i(v0) | ? [v2: % 151.72/23.74 int] : ? [v3: $i] : ? [v4: int] : ? [v5: int] : ($i(v3) & ((v5 = 0 & v4 % 151.72/23.74 = 0 & ~ (v3 = v0) & ~ (v3 = sz10) & doDivides0(v3, v0) = 0 & % 151.72/23.74 aNaturalNumber0(v3) = 0) | ( ~ (v2 = 0) & aNaturalNumber0(v0) = v2)))) % 151.72/23.74 & ! [v0: $i] : ( ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) | ? [v1: int] : ? % 151.72/23.74 [v2: $i] : ? [v3: int] : ? [v4: int] : ($i(v2) & (v0 = sz10 | v0 = sz00 | % 151.72/23.74 (v4 = 0 & v3 = 0 & ~ (v2 = v0) & ~ (v2 = sz10) & doDivides0(v2, v0) = % 151.72/23.74 0 & aNaturalNumber0(v2) = 0) | (v1 = 0 & isPrime0(v0) = 0)) & (( ~ (v1 % 151.72/23.74 = 0) & isPrime0(v0) = v1) | ( ~ (v0 = sz10) & ~ (v0 = sz00) & ! % 151.72/23.74 [v5: $i] : (v5 = v0 | v5 = sz10 | ~ (doDivides0(v5, v0) = 0) | ~ % 151.72/23.74 $i(v5) | ? [v6: int] : ( ~ (v6 = 0) & aNaturalNumber0(v5) = v6)) & % 151.72/23.74 ! [v5: $i] : (v5 = v0 | v5 = sz10 | ~ (aNaturalNumber0(v5) = 0) | ~ % 151.72/23.74 $i(v5) | ? [v6: int] : ( ~ (v6 = 0) & doDivides0(v5, v0) = v6)))))) % 151.72/23.74 & ( ~ (isPrime0(sz10) = 0) | ? [v0: int] : ( ~ (v0 = 0) & % 151.72/23.74 aNaturalNumber0(sz10) = v0)) & ( ~ (isPrime0(sz00) = 0) | ? [v0: int] : ( % 151.72/23.74 ~ (v0 = 0) & aNaturalNumber0(sz00) = v0)) % 151.72/23.74 % 151.72/23.74 (mMulCanc) % 151.72/23.75 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 151.72/23.75 : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v1, v0) = % 151.72/23.75 v3) | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 151.72/23.75 ? [v5: int] : ? [v6: int] : ? [v7: $i] : ? [v8: $i] : (( ~ (v8 = v7) & ~ % 151.72/23.75 (v4 = v3) & sdtasdt0(v0, v2) = v8 & sdtasdt0(v0, v1) = v7 & $i(v8) & % 151.72/23.75 $i(v7)) | ( ~ (v6 = 0) & aNaturalNumber0(v2) = v6) | ( ~ (v5 = 0) & % 151.72/23.75 aNaturalNumber0(v1) = v5))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 151.72/23.75 ! [v3: $i] : ! [v4: $i] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v2, v0) = v4) | % 151.72/23.75 ~ (sdtasdt0(v0, v1) = v3) | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v2) | ~ % 151.72/23.75 $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : ? [v7: $i] : ? [v8: $i] % 151.72/23.75 : (( ~ (v8 = v4) & ~ (v7 = v3) & sdtasdt0(v1, v0) = v8 & sdtasdt0(v0, v2) = % 151.72/23.75 v7 & $i(v8) & $i(v7)) | ( ~ (v6 = 0) & aNaturalNumber0(v2) = v6) | ( ~ % 151.72/23.75 (v5 = 0) & aNaturalNumber0(v1) = v5))) & ! [v0: $i] : ! [v1: $i] : ! % 151.72/23.75 [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v1, % 151.72/23.75 v0) = v4) | ~ (sdtasdt0(v0, v2) = v3) | ~ (aNaturalNumber0(v0) = 0) | % 151.72/23.75 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : ? [v7: $i] % 151.72/23.75 : ? [v8: $i] : (( ~ (v8 = v4) & ~ (v7 = v3) & sdtasdt0(v2, v0) = v8 & % 151.72/23.75 sdtasdt0(v0, v1) = v7 & $i(v8) & $i(v7)) | ( ~ (v6 = 0) & % 151.72/23.75 aNaturalNumber0(v2) = v6) | ( ~ (v5 = 0) & aNaturalNumber0(v1) = v5))) & % 151.72/23.75 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v2 = v1 % 151.72/23.75 | v0 = sz00 | ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ % 151.72/23.75 (aNaturalNumber0(v0) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] % 151.72/23.76 : ? [v6: int] : ? [v7: $i] : ? [v8: $i] : (( ~ (v8 = v7) & ~ (v4 = v3) & % 151.72/23.76 sdtasdt0(v2, v0) = v8 & sdtasdt0(v1, v0) = v7 & $i(v8) & $i(v7)) | ( ~ % 151.72/23.76 (v6 = 0) & aNaturalNumber0(v2) = v6) | ( ~ (v5 = 0) & % 151.72/23.76 aNaturalNumber0(v1) = v5))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 151.72/23.76 ! [v3: $i] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v2, v0) = v3) | ~ % 151.72/23.76 (aNaturalNumber0(v1) = 0) | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v2) | ~ % 151.72/23.76 $i(v1) | ~ $i(v0) | ? [v4: int] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] % 151.72/23.76 : (( ~ (v7 = v3) & ~ (v6 = v5) & sdtasdt0(v1, v0) = v7 & sdtasdt0(v0, v2) = % 151.72/23.76 v6 & sdtasdt0(v0, v1) = v5 & $i(v7) & $i(v6) & $i(v5)) | ( ~ (v4 = 0) & % 151.72/23.76 aNaturalNumber0(v2) = v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 151.72/23.76 ! [v3: $i] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v1, v0) = v3) | ~ % 151.72/23.76 (aNaturalNumber0(v2) = 0) | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v2) | ~ % 151.72/23.76 $i(v1) | ~ $i(v0) | ? [v4: int] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] % 151.72/23.76 : (( ~ (v7 = v3) & ~ (v6 = v5) & sdtasdt0(v2, v0) = v7 & sdtasdt0(v0, v2) = % 151.72/23.76 v6 & sdtasdt0(v0, v1) = v5 & $i(v7) & $i(v6) & $i(v5)) | ( ~ (v4 = 0) & % 151.72/23.76 aNaturalNumber0(v1) = v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 151.72/23.76 ! [v3: $i] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v0, v2) = v3) | ~ % 151.72/23.76 (aNaturalNumber0(v1) = 0) | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v2) | ~ % 151.72/23.76 $i(v1) | ~ $i(v0) | ? [v4: int] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] % 151.72/23.76 : (( ~ (v7 = v6) & ~ (v5 = v3) & sdtasdt0(v2, v0) = v7 & sdtasdt0(v1, v0) = % 151.72/23.76 v6 & sdtasdt0(v0, v1) = v5 & $i(v7) & $i(v6) & $i(v5)) | ( ~ (v4 = 0) & % 151.72/23.76 aNaturalNumber0(v2) = v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 151.72/23.76 ! [v3: $i] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v0, v1) = v3) | ~ % 151.72/23.76 (aNaturalNumber0(v2) = 0) | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v2) | ~ % 151.72/23.76 $i(v1) | ~ $i(v0) | ? [v4: int] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] % 151.72/23.76 : (( ~ (v7 = v6) & ~ (v5 = v3) & sdtasdt0(v2, v0) = v7 & sdtasdt0(v1, v0) = % 151.72/23.76 v6 & sdtasdt0(v0, v2) = v5 & $i(v7) & $i(v6) & $i(v5)) | ( ~ (v4 = 0) & % 151.72/23.76 aNaturalNumber0(v1) = v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 151.72/23.76 (v2 = v1 | v0 = sz00 | ~ (aNaturalNumber0(v2) = 0) | ~ (aNaturalNumber0(v1) % 151.72/23.76 = 0) | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 151.72/23.76 ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ( ~ (v6 = v5) & ~ % 151.72/23.76 (v4 = v3) & sdtasdt0(v2, v0) = v6 & sdtasdt0(v1, v0) = v5 & sdtasdt0(v0, % 151.72/23.76 v2) = v4 & sdtasdt0(v0, v1) = v3 & $i(v6) & $i(v5) & $i(v4) & $i(v3))) % 151.72/23.76 % 151.72/23.76 (mSortsC) % 151.72/23.76 aNaturalNumber0(sz00) = 0 & $i(sz00) % 151.72/23.76 % 151.72/23.76 (mSortsC_01) % 151.72/23.76 ~ (sz10 = sz00) & aNaturalNumber0(sz10) = 0 & $i(sz10) & $i(sz00) % 151.72/23.76 % 151.72/23.76 (m_AddZero) % 151.72/23.76 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtpldt0(v0, sz00) = v1) | ~ % 151.72/23.76 $i(v0) | ? [v2: int] : ? [v3: $i] : ((v3 = v0 & v1 = v0 & sdtpldt0(sz00, % 151.72/23.76 v0) = v0) | ( ~ (v2 = 0) & aNaturalNumber0(v0) = v2))) & ! [v0: $i] : % 151.72/23.76 ! [v1: $i] : ( ~ (sdtpldt0(sz00, v0) = v1) | ~ $i(v0) | ? [v2: int] : ? % 151.72/23.76 [v3: $i] : ((v3 = v0 & v1 = v0 & sdtpldt0(v0, sz00) = v0) | ( ~ (v2 = 0) & % 151.72/23.76 aNaturalNumber0(v0) = v2))) & ! [v0: $i] : ( ~ (aNaturalNumber0(v0) = % 151.72/23.76 0) | ~ $i(v0) | (sdtpldt0(v0, sz00) = v0 & sdtpldt0(sz00, v0) = v0)) % 151.72/23.76 % 151.72/23.76 (m_MulUnit) % 151.72/23.76 $i(sz10) & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtasdt0(v0, sz10) = v1) | ~ % 151.72/23.76 $i(v0) | ? [v2: int] : ? [v3: $i] : ((v3 = v0 & v1 = v0 & sdtasdt0(sz10, % 151.72/23.76 v0) = v0) | ( ~ (v2 = 0) & aNaturalNumber0(v0) = v2))) & ! [v0: $i] : % 151.72/23.76 ! [v1: $i] : ( ~ (sdtasdt0(sz10, v0) = v1) | ~ $i(v0) | ? [v2: int] : ? % 151.72/23.76 [v3: $i] : ((v3 = v0 & v1 = v0 & sdtasdt0(v0, sz10) = v0) | ( ~ (v2 = 0) & % 151.72/23.76 aNaturalNumber0(v0) = v2))) & ! [v0: $i] : ( ~ (aNaturalNumber0(v0) = % 151.72/23.76 0) | ~ $i(v0) | (sdtasdt0(v0, sz10) = v0 & sdtasdt0(sz10, v0) = v0)) % 151.72/23.76 % 151.72/23.76 (m__) % 151.72/23.76 isPrime0(xk) = 0 & $i(xk) & ! [v0: $i] : ( ~ (isPrime0(v0) = 0) | ~ $i(v0) | % 151.72/23.76 ? [v1: int] : ? [v2: int] : (( ~ (v2 = 0) & doDivides0(v0, xk) = v2) | ( ~ % 151.72/23.76 (v1 = 0) & aNaturalNumber0(v0) = v1))) & ! [v0: $i] : ( ~ % 151.72/23.76 (doDivides0(v0, xk) = 0) | ~ $i(v0) | ? [v1: int] : ? [v2: int] : (( ~ % 151.72/23.76 (v2 = 0) & isPrime0(v0) = v2) | ( ~ (v1 = 0) & aNaturalNumber0(v0) = % 151.72/23.76 v1))) & ! [v0: $i] : ( ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) | ? % 151.72/23.76 [v1: int] : ? [v2: int] : (( ~ (v2 = 0) & isPrime0(v0) = v2) | ( ~ (v1 = 0) % 151.72/23.76 & doDivides0(v0, xk) = v1))) % 151.72/23.76 % 151.72/23.76 (m__1716) % 151.72/23.76 aNaturalNumber0(xk) = 0 & $i(xk) % 151.72/23.76 % 151.72/23.76 (m__1716_04) % 151.72/23.76 ~ (xk = sz10) & ~ (xk = sz00) & $i(xk) & $i(sz10) & $i(sz00) % 151.72/23.76 % 151.72/23.76 (function-axioms) % 151.72/23.77 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 151.72/23.77 (sdtsldt0(v3, v2) = v1) | ~ (sdtsldt0(v3, v2) = v0)) & ! [v0: % 151.72/23.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 151.72/23.77 : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ (doDivides0(v3, v2) = v0)) & ! % 151.72/23.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 151.72/23.77 $i] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) & ! % 151.72/23.77 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 151.72/23.77 (sdtmndt0(v3, v2) = v1) | ~ (sdtmndt0(v3, v2) = v0)) & ! [v0: % 151.72/23.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 151.72/23.77 : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ (sdtlseqdt0(v3, v2) = v0)) & ! % 151.72/23.77 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 151.72/23.77 (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 151.72/23.77 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | % 151.72/23.77 ~ (sdtpldt0(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 151.72/23.77 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (isPrime0(v2) = v1) | ~ % 151.72/23.77 (isPrime0(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 151.72/23.77 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) % 151.72/23.77 | ~ (aNaturalNumber0(v2) = v0)) % 151.72/23.77 % 151.72/23.77 Further assumptions not needed in the proof: % 151.72/23.77 -------------------------------------------- % 151.72/23.77 mAddAsso, mAddComm, mDefDiff, mDefLE, mDefQuot, mDivAsso, mDivLE, mDivMin, % 151.72/23.77 mDivSum, mDivTrans, mIH, mIH_03, mLEAsym, mLENTr, mLERefl, mLETotal, mLETran, % 151.72/23.77 mMonAdd, mMonMul, mMonMul2, mMulAsso, mMulComm, mNatSort, mSortsB, mSortsB_02, % 151.72/23.77 mZeroAdd, mZeroMul, m_MulZero, m__1700 % 151.72/23.77 % 151.72/23.77 Those formulas are unsatisfiable: % 151.72/23.77 --------------------------------- % 151.72/23.77 % 151.72/23.77 Begin of proof % 151.72/23.77 | % 151.72/23.77 | ALPHA: (mSortsC) implies: % 151.72/23.77 | (1) aNaturalNumber0(sz00) = 0 % 151.72/23.77 | % 151.72/23.77 | ALPHA: (mSortsC_01) implies: % 151.72/23.77 | (2) ~ (sz10 = sz00) % 151.72/23.77 | (3) aNaturalNumber0(sz10) = 0 % 151.72/23.77 | % 151.72/23.77 | ALPHA: (m_AddZero) implies: % 151.72/23.77 | (4) ! [v0: $i] : ( ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) | (sdtpldt0(v0, % 151.72/23.77 | sz00) = v0 & sdtpldt0(sz00, v0) = v0)) % 151.72/23.77 | % 151.72/23.77 | ALPHA: (m_MulUnit) implies: % 151.72/23.77 | (5) ! [v0: $i] : ( ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) | (sdtasdt0(v0, % 151.72/23.77 | sz10) = v0 & sdtasdt0(sz10, v0) = v0)) % 151.72/23.77 | % 151.72/23.77 | ALPHA: (mAMDistr) implies: % 151.72/23.78 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 151.72/23.78 | ! [v5: $i] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | % 151.72/23.78 | ~ (sdtpldt0(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 151.72/23.78 | [v6: int] : ? [v7: int] : ? [v8: int] : ? [v9: $i] : ? [v10: $i] % 151.72/23.78 | : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : ((v14 = % 151.72/23.78 | v11 & v10 = v5 & sdtasdt0(v9, v0) = v11 & sdtasdt0(v2, v0) = v13 % 151.72/23.78 | & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v9) = v5 & sdtpldt0(v12, % 151.72/23.78 | v13) = v11 & sdtpldt0(v1, v2) = v9 & $i(v13) & $i(v12) & % 151.72/23.78 | $i(v11) & $i(v9) & $i(v5)) | ( ~ (v8 = 0) & aNaturalNumber0(v2) = % 151.72/23.78 | v8) | ( ~ (v7 = 0) & aNaturalNumber0(v1) = v7) | ( ~ (v6 = 0) & % 151.72/23.78 | aNaturalNumber0(v0) = v6))) % 151.72/23.78 | % 151.72/23.78 | ALPHA: (mAddCanc) implies: % 151.72/23.78 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ % 151.72/23.78 | (aNaturalNumber0(v2) = 0) | ~ (aNaturalNumber0(v1) = 0) | ~ % 151.72/23.78 | (aNaturalNumber0(v0) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 151.72/23.78 | [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ( ~ (v6 = v5) & % 151.72/23.78 | ~ (v4 = v3) & sdtpldt0(v2, v0) = v6 & sdtpldt0(v1, v0) = v5 & % 151.72/23.78 | sdtpldt0(v0, v2) = v4 & sdtpldt0(v0, v1) = v3 & $i(v6) & $i(v5) & % 151.72/23.78 | $i(v4) & $i(v3))) % 151.72/23.78 | % 151.72/23.78 | ALPHA: (mMulCanc) implies: % 151.72/23.78 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | v0 = sz00 | ~ % 151.72/23.78 | (aNaturalNumber0(v2) = 0) | ~ (aNaturalNumber0(v1) = 0) | ~ % 151.72/23.78 | (aNaturalNumber0(v0) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 151.72/23.78 | [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ( ~ (v6 = v5) & % 151.72/23.78 | ~ (v4 = v3) & sdtasdt0(v2, v0) = v6 & sdtasdt0(v1, v0) = v5 & % 151.72/23.78 | sdtasdt0(v0, v2) = v4 & sdtasdt0(v0, v1) = v3 & $i(v6) & $i(v5) & % 151.72/23.78 | $i(v4) & $i(v3))) % 151.72/23.78 | % 151.72/23.78 | ALPHA: (mDefDiv) implies: % 151.72/23.78 | (9) ! [v0: $i] : ! [v1: $i] : ! [v2: int] : ! [v3: $i] : (v2 = 0 | ~ % 151.72/23.78 | (doDivides0(v0, v1) = v2) | ~ (aNaturalNumber0(v3) = 0) | ~ $i(v3) % 151.72/23.78 | | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: int] : (( ~ (v5 = 0) % 151.72/23.78 | & aNaturalNumber0(v1) = v5) | ( ~ (v4 = v1) & sdtasdt0(v0, v3) = % 151.72/23.78 | v4 & $i(v4)) | ( ~ (v4 = 0) & aNaturalNumber0(v0) = v4))) % 151.72/23.78 | % 151.72/23.78 | ALPHA: (mDefPrime) implies: % 151.72/23.78 | (10) ! [v0: $i] : ! [v1: $i] : (v1 = v0 | v1 = sz10 | ~ (isPrime0(v0) = % 151.72/23.78 | 0) | ~ (aNaturalNumber0(v1) = 0) | ~ $i(v1) | ~ $i(v0) | ? % 151.72/23.78 | [v2: int] : (( ~ (v2 = 0) & doDivides0(v1, v0) = v2) | ( ~ (v2 = 0) % 151.72/23.78 | & aNaturalNumber0(v0) = v2))) % 151.72/23.78 | % 151.72/23.78 | ALPHA: (m__1716) implies: % 151.72/23.78 | (11) aNaturalNumber0(xk) = 0 % 151.72/23.78 | % 151.72/23.78 | ALPHA: (m__1716_04) implies: % 151.72/23.78 | (12) ~ (xk = sz00) % 151.72/23.78 | (13) ~ (xk = sz10) % 151.72/23.78 | (14) $i(sz00) % 151.72/23.78 | (15) $i(sz10) % 151.72/23.78 | % 151.72/23.78 | ALPHA: (m__) implies: % 151.72/23.78 | (16) $i(xk) % 151.72/23.78 | (17) isPrime0(xk) = 0 % 152.27/23.78 | (18) ! [v0: $i] : ( ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) | ? [v1: int] % 152.27/23.78 | : ? [v2: int] : (( ~ (v2 = 0) & isPrime0(v0) = v2) | ( ~ (v1 = 0) & % 152.27/23.78 | doDivides0(v0, xk) = v1))) % 152.27/23.79 | (19) ! [v0: $i] : ( ~ (isPrime0(v0) = 0) | ~ $i(v0) | ? [v1: int] : ? % 152.27/23.79 | [v2: int] : (( ~ (v2 = 0) & doDivides0(v0, xk) = v2) | ( ~ (v1 = 0) % 152.27/23.79 | & aNaturalNumber0(v0) = v1))) % 152.27/23.79 | % 152.27/23.79 | ALPHA: (function-axioms) implies: % 152.27/23.79 | (20) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 152.27/23.79 | : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = % 152.27/23.79 | v0)) % 152.27/23.79 | (21) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 152.27/23.79 | : (v1 = v0 | ~ (isPrime0(v2) = v1) | ~ (isPrime0(v2) = v0)) % 152.27/23.79 | (22) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 152.27/23.79 | (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 152.27/23.79 | (23) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 152.27/23.79 | (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 152.27/23.79 | (24) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 152.27/23.79 | : ! [v3: $i] : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ % 152.27/23.79 | (doDivides0(v3, v2) = v0)) % 152.27/23.79 | % 152.27/23.79 | GROUND_INST: instantiating (7) with sz10, sz00, sz10, simplifying with (1), % 152.27/23.79 | (3), (14), (15) gives: % 152.27/23.79 | (25) sz10 = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 152.27/23.79 | ( ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(sz10, sz10) = v3 & % 152.27/23.79 | sdtpldt0(sz10, sz10) = v1 & sdtpldt0(sz10, sz00) = v0 & % 152.27/23.79 | sdtpldt0(sz00, sz10) = v2 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.79 | % 152.27/23.79 | GROUND_INST: instantiating (7) with sz10, sz10, sz00, simplifying with (1), % 152.27/23.79 | (3), (14), (15) gives: % 152.27/23.79 | (26) sz10 = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 152.27/23.79 | ( ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(sz10, sz10) = v2 & % 152.27/23.79 | sdtpldt0(sz10, sz10) = v0 & sdtpldt0(sz10, sz00) = v1 & % 152.27/23.79 | sdtpldt0(sz00, sz10) = v3 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.79 | % 152.27/23.79 | GROUND_INST: instantiating (7) with sz00, sz00, sz10, simplifying with (1), % 152.27/23.79 | (3), (14), (15) gives: % 152.27/23.79 | (27) sz10 = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 152.27/23.79 | ( ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(sz10, sz00) = v3 & % 152.27/23.79 | sdtpldt0(sz00, sz10) = v1 & sdtpldt0(sz00, sz00) = v2 & % 152.27/23.79 | sdtpldt0(sz00, sz00) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.79 | % 152.27/23.79 | GROUND_INST: instantiating (7) with sz00, sz10, sz00, simplifying with (1), % 152.27/23.79 | (3), (14), (15) gives: % 152.27/23.80 | (28) sz10 = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 152.27/23.80 | ( ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(sz10, sz00) = v2 & % 152.27/23.80 | sdtpldt0(sz00, sz10) = v0 & sdtpldt0(sz00, sz00) = v3 & % 152.27/23.80 | sdtpldt0(sz00, sz00) = v1 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.80 | % 152.27/23.80 | GROUND_INST: instantiating (5) with sz10, simplifying with (3), (15) gives: % 152.27/23.80 | (29) sdtasdt0(sz10, sz10) = sz10 % 152.27/23.80 | % 152.27/23.80 | GROUND_INST: instantiating (4) with sz10, simplifying with (3), (15) gives: % 152.27/23.80 | (30) sdtpldt0(sz10, sz00) = sz10 & sdtpldt0(sz00, sz10) = sz10 % 152.27/23.80 | % 152.27/23.80 | ALPHA: (30) implies: % 152.27/23.80 | (31) sdtpldt0(sz10, sz00) = sz10 % 152.27/23.80 | % 152.27/23.80 | GROUND_INST: instantiating (8) with xk, sz10, xk, simplifying with (3), (11), % 152.27/23.80 | (15), (16) gives: % 152.27/23.80 | (32) xk = sz10 | xk = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? % 152.27/23.80 | [v3: $i] : ( ~ (v3 = v2) & ~ (v1 = v0) & sdtasdt0(xk, xk) = v3 & % 152.27/23.80 | sdtasdt0(xk, xk) = v1 & sdtasdt0(xk, sz10) = v0 & sdtasdt0(sz10, xk) % 152.27/23.80 | = v2 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.80 | % 152.27/23.80 | GROUND_INST: instantiating (7) with xk, sz10, xk, simplifying with (3), (11), % 152.27/23.80 | (15), (16) gives: % 152.27/23.80 | (33) xk = sz10 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( % 152.27/23.80 | ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(xk, xk) = v3 & sdtpldt0(xk, % 152.27/23.80 | xk) = v1 & sdtpldt0(xk, sz10) = v0 & sdtpldt0(sz10, xk) = v2 & % 152.27/23.80 | $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.80 | % 152.27/23.80 | GROUND_INST: instantiating (7) with xk, sz00, xk, simplifying with (1), (11), % 152.27/23.80 | (14), (16) gives: % 152.27/23.80 | (34) xk = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( % 152.27/23.80 | ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(xk, xk) = v3 & sdtpldt0(xk, % 152.27/23.80 | xk) = v1 & sdtpldt0(xk, sz00) = v0 & sdtpldt0(sz00, xk) = v2 & % 152.27/23.80 | $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.80 | % 152.27/23.80 | GROUND_INST: instantiating (8) with xk, xk, sz10, simplifying with (3), (11), % 152.27/23.80 | (15), (16) gives: % 152.27/23.80 | (35) xk = sz10 | xk = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? % 152.27/23.80 | [v3: $i] : ( ~ (v3 = v2) & ~ (v1 = v0) & sdtasdt0(xk, xk) = v2 & % 152.27/23.80 | sdtasdt0(xk, xk) = v0 & sdtasdt0(xk, sz10) = v1 & sdtasdt0(sz10, xk) % 152.27/23.80 | = v3 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.80 | % 152.27/23.81 | GROUND_INST: instantiating (7) with xk, xk, sz10, simplifying with (3), (11), % 152.27/23.81 | (15), (16) gives: % 152.27/23.81 | (36) xk = sz10 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( % 152.27/23.81 | ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(xk, xk) = v2 & sdtpldt0(xk, % 152.27/23.81 | xk) = v0 & sdtpldt0(xk, sz10) = v1 & sdtpldt0(sz10, xk) = v3 & % 152.27/23.81 | $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.81 | % 152.27/23.81 | GROUND_INST: instantiating (7) with sz10, sz10, xk, simplifying with (3), % 152.27/23.81 | (11), (15), (16) gives: % 152.27/23.81 | (37) xk = sz10 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( % 152.27/23.81 | ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(xk, sz10) = v3 & % 152.27/23.81 | sdtpldt0(sz10, xk) = v1 & sdtpldt0(sz10, sz10) = v2 & sdtpldt0(sz10, % 152.27/23.81 | sz10) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.81 | % 152.27/23.81 | GROUND_INST: instantiating (7) with sz10, xk, sz10, simplifying with (3), % 152.27/23.81 | (11), (15), (16) gives: % 152.27/23.81 | (38) xk = sz10 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( % 152.27/23.81 | ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(xk, sz10) = v2 & % 152.27/23.81 | sdtpldt0(sz10, xk) = v0 & sdtpldt0(sz10, sz10) = v3 & sdtpldt0(sz10, % 152.27/23.81 | sz10) = v1 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.81 | % 152.27/23.81 | GROUND_INST: instantiating (8) with xk, sz00, sz10, simplifying with (1), (3), % 152.27/23.81 | (11), (14), (15), (16) gives: % 152.27/23.81 | (39) xk = sz00 | sz10 = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? % 152.27/23.81 | [v3: $i] : ( ~ (v3 = v2) & ~ (v1 = v0) & sdtasdt0(xk, sz10) = v1 & % 152.27/23.81 | sdtasdt0(xk, sz00) = v0 & sdtasdt0(sz10, xk) = v3 & sdtasdt0(sz00, % 152.27/23.81 | xk) = v2 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.81 | % 152.27/23.81 | GROUND_INST: instantiating (7) with sz00, xk, sz10, simplifying with (1), (3), % 152.27/23.81 | (11), (14), (15), (16) gives: % 152.27/23.81 | (40) xk = sz10 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( % 152.27/23.81 | ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(xk, sz00) = v2 & % 152.27/23.81 | sdtpldt0(sz10, sz00) = v3 & sdtpldt0(sz00, xk) = v0 & sdtpldt0(sz00, % 152.27/23.81 | sz10) = v1 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.81 | % 152.27/23.81 | GROUND_INST: instantiating (7) with xk, sz00, sz10, simplifying with (1), (3), % 152.27/23.81 | (11), (14), (15), (16) gives: % 152.27/23.81 | (41) sz10 = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 152.27/23.81 | ( ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(xk, sz10) = v1 & sdtpldt0(xk, % 152.27/23.81 | sz00) = v0 & sdtpldt0(sz10, xk) = v3 & sdtpldt0(sz00, xk) = v2 & % 152.27/23.81 | $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.81 | % 152.27/23.81 | GROUND_INST: instantiating (7) with xk, xk, sz00, simplifying with (1), (11), % 152.27/23.81 | (14), (16) gives: % 152.27/23.81 | (42) xk = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( % 152.27/23.81 | ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(xk, xk) = v2 & sdtpldt0(xk, % 152.27/23.81 | xk) = v0 & sdtpldt0(xk, sz00) = v1 & sdtpldt0(sz00, xk) = v3 & % 152.27/23.81 | $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.81 | % 152.27/23.81 | GROUND_INST: instantiating (7) with sz10, xk, sz00, simplifying with (1), (3), % 152.27/23.81 | (11), (14), (15), (16) gives: % 152.27/23.82 | (43) xk = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( % 152.27/23.82 | ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(xk, sz10) = v2 & % 152.27/23.82 | sdtpldt0(sz10, xk) = v0 & sdtpldt0(sz10, sz00) = v1 & sdtpldt0(sz00, % 152.27/23.82 | sz10) = v3 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.82 | % 152.27/23.82 | GROUND_INST: instantiating (7) with xk, sz10, sz00, simplifying with (1), (3), % 152.27/23.82 | (11), (14), (15), (16) gives: % 152.27/23.82 | (44) sz10 = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 152.27/23.82 | ( ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(xk, sz10) = v0 & sdtpldt0(xk, % 152.27/23.82 | sz00) = v1 & sdtpldt0(sz10, xk) = v2 & sdtpldt0(sz00, xk) = v3 & % 152.27/23.82 | $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.82 | % 152.27/23.82 | GROUND_INST: instantiating (7) with sz00, sz00, xk, simplifying with (1), % 152.27/23.82 | (11), (14), (16) gives: % 152.27/23.82 | (45) xk = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( % 152.27/23.82 | ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(xk, sz00) = v3 & % 152.27/23.82 | sdtpldt0(sz00, xk) = v1 & sdtpldt0(sz00, sz00) = v2 & sdtpldt0(sz00, % 152.27/23.82 | sz00) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.82 | % 152.27/23.82 | GROUND_INST: instantiating (7) with sz00, xk, sz00, simplifying with (1), % 152.27/23.82 | (11), (14), (16) gives: % 152.27/23.82 | (46) xk = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( % 152.27/23.82 | ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(xk, sz00) = v2 & % 152.27/23.82 | sdtpldt0(sz00, xk) = v0 & sdtpldt0(sz00, sz00) = v3 & sdtpldt0(sz00, % 152.27/23.82 | sz00) = v1 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.27/23.82 | % 152.27/23.82 | GROUND_INST: instantiating (18) with xk, simplifying with (11), (16) gives: % 152.27/23.82 | (47) ? [v0: int] : ? [v1: int] : (( ~ (v1 = 0) & isPrime0(xk) = v1) | ( ~ % 152.27/23.82 | (v0 = 0) & doDivides0(xk, xk) = v0)) % 152.27/23.82 | % 152.27/23.82 | GROUND_INST: instantiating (5) with xk, simplifying with (11), (16) gives: % 152.27/23.82 | (48) sdtasdt0(xk, sz10) = xk & sdtasdt0(sz10, xk) = xk % 152.27/23.82 | % 152.27/23.82 | ALPHA: (48) implies: % 152.27/23.82 | (49) sdtasdt0(sz10, xk) = xk % 152.27/23.82 | (50) sdtasdt0(xk, sz10) = xk % 152.27/23.82 | % 152.27/23.82 | GROUND_INST: instantiating (4) with xk, simplifying with (11), (16) gives: % 152.27/23.82 | (51) sdtpldt0(xk, sz00) = xk & sdtpldt0(sz00, xk) = xk % 152.27/23.82 | % 152.27/23.82 | ALPHA: (51) implies: % 152.27/23.82 | (52) sdtpldt0(xk, sz00) = xk % 152.27/23.82 | % 152.27/23.82 | GROUND_INST: instantiating (10) with xk, sz00, simplifying with (1), (14), % 152.27/23.82 | (16), (17) gives: % 152.27/23.82 | (53) xk = sz00 | sz10 = sz00 | ? [v0: int] : (( ~ (v0 = 0) & % 152.27/23.82 | doDivides0(sz00, xk) = v0) | ( ~ (v0 = 0) & aNaturalNumber0(xk) = % 152.27/23.82 | v0)) % 152.27/23.82 | % 152.27/23.82 | GROUND_INST: instantiating (19) with xk, simplifying with (16), (17) gives: % 152.27/23.82 | (54) ? [v0: int] : ? [v1: int] : (( ~ (v1 = 0) & doDivides0(xk, xk) = v1) % 152.27/23.82 | | ( ~ (v0 = 0) & aNaturalNumber0(xk) = v0)) % 152.27/23.82 | % 152.27/23.82 | DELTA: instantiating (54) with fresh symbols all_57_0, all_57_1 gives: % 152.50/23.82 | (55) ( ~ (all_57_0 = 0) & doDivides0(xk, xk) = all_57_0) | ( ~ (all_57_1 = % 152.50/23.82 | 0) & aNaturalNumber0(xk) = all_57_1) % 152.50/23.82 | % 152.50/23.82 | DELTA: instantiating (47) with fresh symbols all_58_0, all_58_1 gives: % 152.50/23.82 | (56) ( ~ (all_58_0 = 0) & isPrime0(xk) = all_58_0) | ( ~ (all_58_1 = 0) & % 152.50/23.82 | doDivides0(xk, xk) = all_58_1) % 152.50/23.82 | % 152.50/23.82 | BETA: splitting (55) gives: % 152.50/23.82 | % 152.50/23.82 | Case 1: % 152.50/23.82 | | % 152.50/23.82 | | (57) ~ (all_57_0 = 0) & doDivides0(xk, xk) = all_57_0 % 152.50/23.82 | | % 152.50/23.82 | | ALPHA: (57) implies: % 152.50/23.82 | | (58) doDivides0(xk, xk) = all_57_0 % 152.50/23.82 | | % 152.50/23.82 | | BETA: splitting (26) gives: % 152.50/23.82 | | % 152.50/23.82 | | Case 1: % 152.50/23.82 | | | % 152.50/23.82 | | | (59) sz10 = sz00 % 152.50/23.82 | | | % 152.50/23.82 | | | REDUCE: (2), (59) imply: % 152.50/23.82 | | | (60) $false % 152.50/23.83 | | | % 152.50/23.83 | | | CLOSE: (60) is inconsistent. % 152.50/23.83 | | | % 152.50/23.83 | | Case 2: % 152.50/23.83 | | | % 152.50/23.83 | | | (61) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( ~ (v3 = % 152.50/23.83 | | | v2) & ~ (v1 = v0) & sdtpldt0(sz10, sz10) = v2 & % 152.50/23.83 | | | sdtpldt0(sz10, sz10) = v0 & sdtpldt0(sz10, sz00) = v1 & % 152.50/23.83 | | | sdtpldt0(sz00, sz10) = v3 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.50/23.83 | | | % 152.50/23.83 | | | DELTA: instantiating (61) with fresh symbols all_128_0, all_128_1, % 152.50/23.83 | | | all_128_2, all_128_3 gives: % 152.50/23.83 | | | (62) ~ (all_128_0 = all_128_1) & ~ (all_128_2 = all_128_3) & % 152.50/23.83 | | | sdtpldt0(sz10, sz10) = all_128_1 & sdtpldt0(sz10, sz10) = % 152.50/23.83 | | | all_128_3 & sdtpldt0(sz10, sz00) = all_128_2 & sdtpldt0(sz00, % 152.50/23.83 | | | sz10) = all_128_0 & $i(all_128_0) & $i(all_128_1) & % 152.50/23.83 | | | $i(all_128_2) & $i(all_128_3) % 152.50/23.83 | | | % 152.50/23.83 | | | ALPHA: (62) implies: % 152.50/23.83 | | | (63) $i(all_128_2) % 152.50/23.83 | | | (64) sdtpldt0(sz10, sz00) = all_128_2 % 152.50/23.83 | | | % 152.50/23.83 | | | BETA: splitting (28) gives: % 152.50/23.83 | | | % 152.50/23.83 | | | Case 1: % 152.50/23.83 | | | | % 152.50/23.83 | | | | (65) sz10 = sz00 % 152.50/23.83 | | | | % 152.50/23.83 | | | | REDUCE: (2), (65) imply: % 152.50/23.83 | | | | (66) $false % 152.50/23.83 | | | | % 152.50/23.83 | | | | CLOSE: (66) is inconsistent. % 152.50/23.83 | | | | % 152.50/23.83 | | | Case 2: % 152.50/23.83 | | | | % 152.50/23.83 | | | | (67) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( ~ (v3 % 152.50/23.83 | | | | = v2) & ~ (v1 = v0) & sdtpldt0(sz10, sz00) = v2 & % 152.50/23.83 | | | | sdtpldt0(sz00, sz10) = v0 & sdtpldt0(sz00, sz00) = v3 & % 152.50/23.83 | | | | sdtpldt0(sz00, sz00) = v1 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.50/23.83 | | | | % 152.50/23.83 | | | | DELTA: instantiating (67) with fresh symbols all_134_0, all_134_1, % 152.50/23.83 | | | | all_134_2, all_134_3 gives: % 152.50/23.83 | | | | (68) ~ (all_134_0 = all_134_1) & ~ (all_134_2 = all_134_3) & % 152.50/23.83 | | | | sdtpldt0(sz10, sz00) = all_134_1 & sdtpldt0(sz00, sz10) = % 152.50/23.83 | | | | all_134_3 & sdtpldt0(sz00, sz00) = all_134_0 & sdtpldt0(sz00, % 152.50/23.83 | | | | sz00) = all_134_2 & $i(all_134_0) & $i(all_134_1) & % 152.50/23.83 | | | | $i(all_134_2) & $i(all_134_3) % 152.50/23.83 | | | | % 152.50/23.83 | | | | ALPHA: (68) implies: % 152.50/23.83 | | | | (69) sdtpldt0(sz10, sz00) = all_134_1 % 152.50/23.83 | | | | % 152.50/23.83 | | | | BETA: splitting (25) gives: % 152.50/23.83 | | | | % 152.50/23.83 | | | | Case 1: % 152.50/23.83 | | | | | % 152.50/23.83 | | | | | (70) sz10 = sz00 % 152.50/23.83 | | | | | % 152.50/23.83 | | | | | REDUCE: (2), (70) imply: % 152.50/23.83 | | | | | (71) $false % 152.50/23.83 | | | | | % 152.50/23.83 | | | | | CLOSE: (71) is inconsistent. % 152.50/23.83 | | | | | % 152.50/23.83 | | | | Case 2: % 152.50/23.83 | | | | | % 152.50/23.83 | | | | | (72) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( ~ % 152.50/23.83 | | | | | (v3 = v2) & ~ (v1 = v0) & sdtpldt0(sz10, sz10) = v3 & % 152.50/23.83 | | | | | sdtpldt0(sz10, sz10) = v1 & sdtpldt0(sz10, sz00) = v0 & % 152.50/23.83 | | | | | sdtpldt0(sz00, sz10) = v2 & $i(v3) & $i(v2) & $i(v1) & % 152.50/23.83 | | | | | $i(v0)) % 152.50/23.83 | | | | | % 152.50/23.83 | | | | | DELTA: instantiating (72) with fresh symbols all_140_0, all_140_1, % 152.50/23.83 | | | | | all_140_2, all_140_3 gives: % 152.50/23.83 | | | | | (73) ~ (all_140_0 = all_140_1) & ~ (all_140_2 = all_140_3) & % 152.50/23.83 | | | | | sdtpldt0(sz10, sz10) = all_140_0 & sdtpldt0(sz10, sz10) = % 152.50/23.83 | | | | | all_140_2 & sdtpldt0(sz10, sz00) = all_140_3 & sdtpldt0(sz00, % 152.50/23.83 | | | | | sz10) = all_140_1 & $i(all_140_0) & $i(all_140_1) & % 152.50/23.83 | | | | | $i(all_140_2) & $i(all_140_3) % 152.50/23.83 | | | | | % 152.50/23.83 | | | | | ALPHA: (73) implies: % 152.50/23.83 | | | | | (74) sdtpldt0(sz10, sz00) = all_140_3 % 152.50/23.83 | | | | | % 152.50/23.83 | | | | | BETA: splitting (34) gives: % 152.50/23.83 | | | | | % 152.50/23.83 | | | | | Case 1: % 152.50/23.83 | | | | | | % 152.50/23.83 | | | | | | (75) xk = sz00 % 152.50/23.83 | | | | | | % 152.50/23.83 | | | | | | REDUCE: (12), (75) imply: % 152.50/23.83 | | | | | | (76) $false % 152.50/23.83 | | | | | | % 152.50/23.83 | | | | | | CLOSE: (76) is inconsistent. % 152.50/23.83 | | | | | | % 152.50/23.83 | | | | | Case 2: % 152.50/23.83 | | | | | | % 152.50/23.83 | | | | | | (77) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( ~ % 152.50/23.83 | | | | | | (v3 = v2) & ~ (v1 = v0) & sdtpldt0(xk, xk) = v3 & % 152.50/23.83 | | | | | | sdtpldt0(xk, xk) = v1 & sdtpldt0(xk, sz00) = v0 & % 152.50/23.83 | | | | | | sdtpldt0(sz00, xk) = v2 & $i(v3) & $i(v2) & $i(v1) & % 152.50/23.83 | | | | | | $i(v0)) % 152.50/23.83 | | | | | | % 152.50/23.83 | | | | | | DELTA: instantiating (77) with fresh symbols all_150_0, all_150_1, % 152.50/23.83 | | | | | | all_150_2, all_150_3 gives: % 152.50/23.83 | | | | | | (78) ~ (all_150_0 = all_150_1) & ~ (all_150_2 = all_150_3) & % 152.50/23.83 | | | | | | sdtpldt0(xk, xk) = all_150_0 & sdtpldt0(xk, xk) = all_150_2 % 152.50/23.83 | | | | | | & sdtpldt0(xk, sz00) = all_150_3 & sdtpldt0(sz00, xk) = % 152.50/23.83 | | | | | | all_150_1 & $i(all_150_0) & $i(all_150_1) & $i(all_150_2) & % 152.50/23.83 | | | | | | $i(all_150_3) % 152.50/23.83 | | | | | | % 152.50/23.83 | | | | | | ALPHA: (78) implies: % 152.50/23.83 | | | | | | (79) $i(all_150_3) % 152.50/23.83 | | | | | | (80) sdtpldt0(xk, sz00) = all_150_3 % 152.50/23.83 | | | | | | % 152.50/23.83 | | | | | | BETA: splitting (46) gives: % 152.50/23.83 | | | | | | % 152.50/23.83 | | | | | | Case 1: % 152.50/23.83 | | | | | | | % 152.50/23.83 | | | | | | | (81) xk = sz00 % 152.50/23.83 | | | | | | | % 152.50/23.83 | | | | | | | REDUCE: (12), (81) imply: % 152.50/23.83 | | | | | | | (82) $false % 152.50/23.83 | | | | | | | % 152.50/23.83 | | | | | | | CLOSE: (82) is inconsistent. % 152.50/23.83 | | | | | | | % 152.50/23.83 | | | | | | Case 2: % 152.50/23.83 | | | | | | | % 152.50/23.83 | | | | | | | (83) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( % 152.50/23.83 | | | | | | | ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(xk, sz00) = v2 & % 152.50/23.83 | | | | | | | sdtpldt0(sz00, xk) = v0 & sdtpldt0(sz00, sz00) = v3 & % 152.50/23.83 | | | | | | | sdtpldt0(sz00, sz00) = v1 & $i(v3) & $i(v2) & $i(v1) & % 152.50/23.83 | | | | | | | $i(v0)) % 152.50/23.83 | | | | | | | % 152.50/23.83 | | | | | | | DELTA: instantiating (83) with fresh symbols all_156_0, all_156_1, % 152.50/23.83 | | | | | | | all_156_2, all_156_3 gives: % 152.50/23.84 | | | | | | | (84) ~ (all_156_0 = all_156_1) & ~ (all_156_2 = all_156_3) & % 152.50/23.84 | | | | | | | sdtpldt0(xk, sz00) = all_156_1 & sdtpldt0(sz00, xk) = % 152.50/23.84 | | | | | | | all_156_3 & sdtpldt0(sz00, sz00) = all_156_0 & % 152.50/23.84 | | | | | | | sdtpldt0(sz00, sz00) = all_156_2 & $i(all_156_0) & % 152.50/23.84 | | | | | | | $i(all_156_1) & $i(all_156_2) & $i(all_156_3) % 152.50/23.84 | | | | | | | % 152.50/23.84 | | | | | | | ALPHA: (84) implies: % 152.50/23.84 | | | | | | | (85) sdtpldt0(xk, sz00) = all_156_1 % 152.50/23.84 | | | | | | | % 152.50/23.84 | | | | | | | BETA: splitting (27) gives: % 152.50/23.84 | | | | | | | % 152.50/23.84 | | | | | | | Case 1: % 152.50/23.84 | | | | | | | | % 152.50/23.84 | | | | | | | | (86) sz10 = sz00 % 152.50/23.84 | | | | | | | | % 152.50/23.84 | | | | | | | | REDUCE: (2), (86) imply: % 152.50/23.84 | | | | | | | | (87) $false % 152.50/23.84 | | | | | | | | % 152.50/23.84 | | | | | | | | CLOSE: (87) is inconsistent. % 152.50/23.84 | | | | | | | | % 152.50/23.84 | | | | | | | Case 2: % 152.50/23.84 | | | | | | | | % 152.50/23.84 | | | | | | | | (88) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 152.50/23.84 | | | | | | | | ( ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(sz10, sz00) = v3 % 152.50/23.84 | | | | | | | | & sdtpldt0(sz00, sz10) = v1 & sdtpldt0(sz00, sz00) = % 152.50/23.84 | | | | | | | | v2 & sdtpldt0(sz00, sz00) = v0 & $i(v3) & $i(v2) & % 152.50/23.84 | | | | | | | | $i(v1) & $i(v0)) % 152.50/23.84 | | | | | | | | % 152.50/23.84 | | | | | | | | DELTA: instantiating (88) with fresh symbols all_162_0, % 152.50/23.84 | | | | | | | | all_162_1, all_162_2, all_162_3 gives: % 152.50/23.84 | | | | | | | | (89) ~ (all_162_0 = all_162_1) & ~ (all_162_2 = all_162_3) % 152.50/23.84 | | | | | | | | & sdtpldt0(sz10, sz00) = all_162_0 & sdtpldt0(sz00, % 152.50/23.84 | | | | | | | | sz10) = all_162_2 & sdtpldt0(sz00, sz00) = all_162_1 & % 152.50/23.84 | | | | | | | | sdtpldt0(sz00, sz00) = all_162_3 & $i(all_162_0) & % 152.50/23.84 | | | | | | | | $i(all_162_1) & $i(all_162_2) & $i(all_162_3) % 152.50/23.84 | | | | | | | | % 152.50/23.84 | | | | | | | | ALPHA: (89) implies: % 152.50/23.84 | | | | | | | | (90) sdtpldt0(sz10, sz00) = all_162_0 % 152.50/23.84 | | | | | | | | % 152.50/23.84 | | | | | | | | BETA: splitting (33) gives: % 152.50/23.84 | | | | | | | | % 152.50/23.84 | | | | | | | | Case 1: % 152.50/23.84 | | | | | | | | | % 152.50/23.84 | | | | | | | | | (91) xk = sz10 % 152.50/23.84 | | | | | | | | | % 152.50/23.84 | | | | | | | | | REDUCE: (13), (91) imply: % 152.50/23.84 | | | | | | | | | (92) $false % 152.50/23.84 | | | | | | | | | % 152.50/23.84 | | | | | | | | | CLOSE: (92) is inconsistent. % 152.50/23.84 | | | | | | | | | % 152.50/23.84 | | | | | | | | Case 2: % 152.50/23.84 | | | | | | | | | % 152.50/23.84 | | | | | | | | | (93) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] % 152.50/23.84 | | | | | | | | | : ( ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(xk, xk) = v3 % 152.50/23.84 | | | | | | | | | & sdtpldt0(xk, xk) = v1 & sdtpldt0(xk, sz10) = v0 & % 152.50/23.84 | | | | | | | | | sdtpldt0(sz10, xk) = v2 & $i(v3) & $i(v2) & $i(v1) & % 152.50/23.84 | | | | | | | | | $i(v0)) % 152.50/23.84 | | | | | | | | | % 152.50/23.84 | | | | | | | | | DELTA: instantiating (93) with fresh symbols all_171_0, % 152.50/23.84 | | | | | | | | | all_171_1, all_171_2, all_171_3 gives: % 152.50/23.84 | | | | | | | | | (94) ~ (all_171_0 = all_171_1) & ~ (all_171_2 = % 152.50/23.84 | | | | | | | | | all_171_3) & sdtpldt0(xk, xk) = all_171_0 & % 152.50/23.84 | | | | | | | | | sdtpldt0(xk, xk) = all_171_2 & sdtpldt0(xk, sz10) = % 152.50/23.84 | | | | | | | | | all_171_3 & sdtpldt0(sz10, xk) = all_171_1 & % 152.50/23.84 | | | | | | | | | $i(all_171_0) & $i(all_171_1) & $i(all_171_2) & % 152.50/23.84 | | | | | | | | | $i(all_171_3) % 152.50/23.84 | | | | | | | | | % 152.50/23.84 | | | | | | | | | ALPHA: (94) implies: % 152.50/23.84 | | | | | | | | | (95) sdtpldt0(sz10, xk) = all_171_1 % 152.50/23.84 | | | | | | | | | % 152.50/23.84 | | | | | | | | | BETA: splitting (41) gives: % 152.50/23.84 | | | | | | | | | % 152.50/23.84 | | | | | | | | | Case 1: % 152.50/23.84 | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | (96) sz10 = sz00 % 152.50/23.84 | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | REDUCE: (2), (96) imply: % 152.50/23.84 | | | | | | | | | | (97) $false % 152.50/23.84 | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | CLOSE: (97) is inconsistent. % 152.50/23.84 | | | | | | | | | | % 152.50/23.84 | | | | | | | | | Case 2: % 152.50/23.84 | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | (98) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 152.50/23.84 | | | | | | | | | | $i] : ( ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(xk, % 152.50/23.84 | | | | | | | | | | sz10) = v1 & sdtpldt0(xk, sz00) = v0 & % 152.50/23.84 | | | | | | | | | | sdtpldt0(sz10, xk) = v3 & sdtpldt0(sz00, xk) = v2 % 152.50/23.84 | | | | | | | | | | & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.50/23.84 | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | DELTA: instantiating (98) with fresh symbols all_176_0, % 152.50/23.84 | | | | | | | | | | all_176_1, all_176_2, all_176_3 gives: % 152.50/23.84 | | | | | | | | | | (99) ~ (all_176_0 = all_176_1) & ~ (all_176_2 = % 152.50/23.84 | | | | | | | | | | all_176_3) & sdtpldt0(xk, sz10) = all_176_2 & % 152.50/23.84 | | | | | | | | | | sdtpldt0(xk, sz00) = all_176_3 & sdtpldt0(sz10, xk) % 152.50/23.84 | | | | | | | | | | = all_176_0 & sdtpldt0(sz00, xk) = all_176_1 & % 152.50/23.84 | | | | | | | | | | $i(all_176_0) & $i(all_176_1) & $i(all_176_2) & % 152.50/23.84 | | | | | | | | | | $i(all_176_3) % 152.50/23.84 | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | ALPHA: (99) implies: % 152.50/23.84 | | | | | | | | | | (100) sdtpldt0(sz10, xk) = all_176_0 % 152.50/23.84 | | | | | | | | | | (101) sdtpldt0(xk, sz00) = all_176_3 % 152.50/23.84 | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | BETA: splitting (38) gives: % 152.50/23.84 | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | Case 1: % 152.50/23.84 | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | (102) xk = sz10 % 152.50/23.84 | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | REDUCE: (13), (102) imply: % 152.50/23.84 | | | | | | | | | | | (103) $false % 152.50/23.84 | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | CLOSE: (103) is inconsistent. % 152.50/23.84 | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | Case 2: % 152.50/23.84 | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | (104) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 152.50/23.84 | | | | | | | | | | | $i] : ( ~ (v3 = v2) & ~ (v1 = v0) & % 152.50/23.84 | | | | | | | | | | | sdtpldt0(xk, sz10) = v2 & sdtpldt0(sz10, xk) = % 152.50/23.84 | | | | | | | | | | | v0 & sdtpldt0(sz10, sz10) = v3 & sdtpldt0(sz10, % 152.50/23.84 | | | | | | | | | | | sz10) = v1 & $i(v3) & $i(v2) & $i(v1) & % 152.50/23.84 | | | | | | | | | | | $i(v0)) % 152.50/23.84 | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | DELTA: instantiating (104) with fresh symbols all_181_0, % 152.50/23.84 | | | | | | | | | | | all_181_1, all_181_2, all_181_3 gives: % 152.50/23.84 | | | | | | | | | | | (105) ~ (all_181_0 = all_181_1) & ~ (all_181_2 = % 152.50/23.84 | | | | | | | | | | | all_181_3) & sdtpldt0(xk, sz10) = all_181_1 & % 152.50/23.84 | | | | | | | | | | | sdtpldt0(sz10, xk) = all_181_3 & sdtpldt0(sz10, % 152.50/23.84 | | | | | | | | | | | sz10) = all_181_0 & sdtpldt0(sz10, sz10) = % 152.50/23.84 | | | | | | | | | | | all_181_2 & $i(all_181_0) & $i(all_181_1) & % 152.50/23.84 | | | | | | | | | | | $i(all_181_2) & $i(all_181_3) % 152.50/23.84 | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | ALPHA: (105) implies: % 152.50/23.84 | | | | | | | | | | | (106) sdtpldt0(sz10, xk) = all_181_3 % 152.50/23.84 | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | BETA: splitting (44) gives: % 152.50/23.84 | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | Case 1: % 152.50/23.84 | | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | | (107) sz10 = sz00 % 152.50/23.84 | | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | | REDUCE: (2), (107) imply: % 152.50/23.84 | | | | | | | | | | | | (108) $false % 152.50/23.84 | | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | | CLOSE: (108) is inconsistent. % 152.50/23.84 | | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | Case 2: % 152.50/23.84 | | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | | (109) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 152.50/23.84 | | | | | | | | | | | | $i] : ( ~ (v3 = v2) & ~ (v1 = v0) & % 152.50/23.84 | | | | | | | | | | | | sdtpldt0(xk, sz10) = v0 & sdtpldt0(xk, sz00) = % 152.50/23.84 | | | | | | | | | | | | v1 & sdtpldt0(sz10, xk) = v2 & sdtpldt0(sz00, % 152.50/23.84 | | | | | | | | | | | | xk) = v3 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.50/23.84 | | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | | DELTA: instantiating (109) with fresh symbols all_186_0, % 152.50/23.84 | | | | | | | | | | | | all_186_1, all_186_2, all_186_3 gives: % 152.50/23.84 | | | | | | | | | | | | (110) ~ (all_186_0 = all_186_1) & ~ (all_186_2 = % 152.50/23.84 | | | | | | | | | | | | all_186_3) & sdtpldt0(xk, sz10) = all_186_3 & % 152.50/23.84 | | | | | | | | | | | | sdtpldt0(xk, sz00) = all_186_2 & sdtpldt0(sz10, % 152.50/23.84 | | | | | | | | | | | | xk) = all_186_1 & sdtpldt0(sz00, xk) = all_186_0 % 152.50/23.84 | | | | | | | | | | | | & $i(all_186_0) & $i(all_186_1) & $i(all_186_2) & % 152.50/23.84 | | | | | | | | | | | | $i(all_186_3) % 152.50/23.84 | | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | | ALPHA: (110) implies: % 152.50/23.84 | | | | | | | | | | | | (111) sdtpldt0(sz10, xk) = all_186_1 % 152.50/23.84 | | | | | | | | | | | | (112) sdtpldt0(xk, sz00) = all_186_2 % 152.50/23.84 | | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | | BETA: splitting (45) gives: % 152.50/23.84 | | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | | Case 1: % 152.50/23.84 | | | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | | | (113) xk = sz00 % 152.50/23.84 | | | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | | | REDUCE: (12), (113) imply: % 152.50/23.84 | | | | | | | | | | | | | (114) $false % 152.50/23.84 | | | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | | | CLOSE: (114) is inconsistent. % 152.50/23.84 | | | | | | | | | | | | | % 152.50/23.84 | | | | | | | | | | | | Case 2: % 152.50/23.84 | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | (115) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 152.50/23.85 | | | | | | | | | | | | | $i] : ( ~ (v3 = v2) & ~ (v1 = v0) & % 152.50/23.85 | | | | | | | | | | | | | sdtpldt0(xk, sz00) = v3 & sdtpldt0(sz00, xk) = % 152.50/23.85 | | | | | | | | | | | | | v1 & sdtpldt0(sz00, sz00) = v2 & sdtpldt0(sz00, % 152.50/23.85 | | | | | | | | | | | | | sz00) = v0 & $i(v3) & $i(v2) & $i(v1) & % 152.50/23.85 | | | | | | | | | | | | | $i(v0)) % 152.50/23.85 | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | DELTA: instantiating (115) with fresh symbols all_192_0, % 152.50/23.85 | | | | | | | | | | | | | all_192_1, all_192_2, all_192_3 gives: % 152.50/23.85 | | | | | | | | | | | | | (116) ~ (all_192_0 = all_192_1) & ~ (all_192_2 = % 152.50/23.85 | | | | | | | | | | | | | all_192_3) & sdtpldt0(xk, sz00) = all_192_0 & % 152.50/23.85 | | | | | | | | | | | | | sdtpldt0(sz00, xk) = all_192_2 & sdtpldt0(sz00, % 152.50/23.85 | | | | | | | | | | | | | sz00) = all_192_1 & sdtpldt0(sz00, sz00) = % 152.50/23.85 | | | | | | | | | | | | | all_192_3 & $i(all_192_0) & $i(all_192_1) & % 152.50/23.85 | | | | | | | | | | | | | $i(all_192_2) & $i(all_192_3) % 152.50/23.85 | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | ALPHA: (116) implies: % 152.50/23.85 | | | | | | | | | | | | | (117) sdtpldt0(xk, sz00) = all_192_0 % 152.50/23.85 | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | BETA: splitting (39) gives: % 152.50/23.85 | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | Case 1: % 152.50/23.85 | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | (118) xk = sz00 % 152.50/23.85 | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | REDUCE: (12), (118) imply: % 152.50/23.85 | | | | | | | | | | | | | | (119) $false % 152.50/23.85 | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | CLOSE: (119) is inconsistent. % 152.50/23.85 | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | Case 2: % 152.50/23.85 | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | (120) sz10 = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: % 152.50/23.85 | | | | | | | | | | | | | | $i] : ? [v3: $i] : ( ~ (v3 = v2) & ~ (v1 = v0) % 152.50/23.85 | | | | | | | | | | | | | | & sdtasdt0(xk, sz10) = v1 & sdtasdt0(xk, sz00) = % 152.50/23.85 | | | | | | | | | | | | | | v0 & sdtasdt0(sz10, xk) = v3 & sdtasdt0(sz00, % 152.50/23.85 | | | | | | | | | | | | | | xk) = v2 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.50/23.85 | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | BETA: splitting (36) gives: % 152.50/23.85 | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | Case 1: % 152.50/23.85 | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | (121) xk = sz10 % 152.50/23.85 | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | REDUCE: (13), (121) imply: % 152.50/23.85 | | | | | | | | | | | | | | | (122) $false % 152.50/23.85 | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | CLOSE: (122) is inconsistent. % 152.50/23.85 | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | Case 2: % 152.50/23.85 | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | (123) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 152.50/23.85 | | | | | | | | | | | | | | | $i] : ( ~ (v3 = v2) & ~ (v1 = v0) & % 152.50/23.85 | | | | | | | | | | | | | | | sdtpldt0(xk, xk) = v2 & sdtpldt0(xk, xk) = v0 & % 152.50/23.85 | | | | | | | | | | | | | | | sdtpldt0(xk, sz10) = v1 & sdtpldt0(sz10, xk) = % 152.50/23.85 | | | | | | | | | | | | | | | v3 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.50/23.85 | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | DELTA: instantiating (123) with fresh symbols all_202_0, % 152.50/23.85 | | | | | | | | | | | | | | | all_202_1, all_202_2, all_202_3 gives: % 152.50/23.85 | | | | | | | | | | | | | | | (124) ~ (all_202_0 = all_202_1) & ~ (all_202_2 = % 152.50/23.85 | | | | | | | | | | | | | | | all_202_3) & sdtpldt0(xk, xk) = all_202_1 & % 152.50/23.85 | | | | | | | | | | | | | | | sdtpldt0(xk, xk) = all_202_3 & sdtpldt0(xk, sz10) % 152.50/23.85 | | | | | | | | | | | | | | | = all_202_2 & sdtpldt0(sz10, xk) = all_202_0 & % 152.50/23.85 | | | | | | | | | | | | | | | $i(all_202_0) & $i(all_202_1) & $i(all_202_2) & % 152.50/23.85 | | | | | | | | | | | | | | | $i(all_202_3) % 152.50/23.85 | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | ALPHA: (124) implies: % 152.50/23.85 | | | | | | | | | | | | | | | (125) sdtpldt0(sz10, xk) = all_202_0 % 152.50/23.85 | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | BETA: splitting (40) gives: % 152.50/23.85 | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | Case 1: % 152.50/23.85 | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | (126) xk = sz10 % 152.50/23.85 | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | REDUCE: (13), (126) imply: % 152.50/23.85 | | | | | | | | | | | | | | | | (127) $false % 152.50/23.85 | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | CLOSE: (127) is inconsistent. % 152.50/23.85 | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | Case 2: % 152.50/23.85 | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | (128) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 152.50/23.85 | | | | | | | | | | | | | | | | $i] : ( ~ (v3 = v2) & ~ (v1 = v0) & % 152.50/23.85 | | | | | | | | | | | | | | | | sdtpldt0(xk, sz00) = v2 & sdtpldt0(sz10, sz00) = % 152.50/23.85 | | | | | | | | | | | | | | | | v3 & sdtpldt0(sz00, xk) = v0 & sdtpldt0(sz00, % 152.50/23.85 | | | | | | | | | | | | | | | | sz10) = v1 & $i(v3) & $i(v2) & $i(v1) & % 152.50/23.85 | | | | | | | | | | | | | | | | $i(v0)) % 152.50/23.85 | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | DELTA: instantiating (128) with fresh symbols all_208_0, % 152.50/23.85 | | | | | | | | | | | | | | | | all_208_1, all_208_2, all_208_3 gives: % 152.50/23.85 | | | | | | | | | | | | | | | | (129) ~ (all_208_0 = all_208_1) & ~ (all_208_2 = % 152.50/23.85 | | | | | | | | | | | | | | | | all_208_3) & sdtpldt0(xk, sz00) = all_208_1 & % 152.50/23.85 | | | | | | | | | | | | | | | | sdtpldt0(sz10, sz00) = all_208_0 & sdtpldt0(sz00, % 152.50/23.85 | | | | | | | | | | | | | | | | xk) = all_208_3 & sdtpldt0(sz00, sz10) = % 152.50/23.85 | | | | | | | | | | | | | | | | all_208_2 & $i(all_208_0) & $i(all_208_1) & % 152.50/23.85 | | | | | | | | | | | | | | | | $i(all_208_2) & $i(all_208_3) % 152.50/23.85 | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | ALPHA: (129) implies: % 152.50/23.85 | | | | | | | | | | | | | | | | (130) sdtpldt0(sz10, sz00) = all_208_0 % 152.50/23.85 | | | | | | | | | | | | | | | | (131) sdtpldt0(xk, sz00) = all_208_1 % 152.50/23.85 | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | BETA: splitting (43) gives: % 152.50/23.85 | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | Case 1: % 152.50/23.85 | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | (132) xk = sz00 % 152.50/23.85 | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | REDUCE: (12), (132) imply: % 152.50/23.85 | | | | | | | | | | | | | | | | | (133) $false % 152.50/23.85 | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | CLOSE: (133) is inconsistent. % 152.50/23.85 | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | Case 2: % 152.50/23.85 | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | (134) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 152.50/23.85 | | | | | | | | | | | | | | | | | $i] : ( ~ (v3 = v2) & ~ (v1 = v0) & % 152.50/23.85 | | | | | | | | | | | | | | | | | sdtpldt0(xk, sz10) = v2 & sdtpldt0(sz10, xk) = % 152.50/23.85 | | | | | | | | | | | | | | | | | v0 & sdtpldt0(sz10, sz00) = v1 & sdtpldt0(sz00, % 152.50/23.85 | | | | | | | | | | | | | | | | | sz10) = v3 & $i(v3) & $i(v2) & $i(v1) & % 152.50/23.85 | | | | | | | | | | | | | | | | | $i(v0)) % 152.50/23.85 | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | DELTA: instantiating (134) with fresh symbols all_214_0, % 152.50/23.85 | | | | | | | | | | | | | | | | | all_214_1, all_214_2, all_214_3 gives: % 152.50/23.85 | | | | | | | | | | | | | | | | | (135) ~ (all_214_0 = all_214_1) & ~ (all_214_2 = % 152.50/23.85 | | | | | | | | | | | | | | | | | all_214_3) & sdtpldt0(xk, sz10) = all_214_1 & % 152.50/23.85 | | | | | | | | | | | | | | | | | sdtpldt0(sz10, xk) = all_214_3 & sdtpldt0(sz10, % 152.50/23.85 | | | | | | | | | | | | | | | | | sz00) = all_214_2 & sdtpldt0(sz00, sz10) = % 152.50/23.85 | | | | | | | | | | | | | | | | | all_214_0 & $i(all_214_0) & $i(all_214_1) & % 152.50/23.85 | | | | | | | | | | | | | | | | | $i(all_214_2) & $i(all_214_3) % 152.50/23.85 | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | ALPHA: (135) implies: % 152.50/23.85 | | | | | | | | | | | | | | | | | (136) sdtpldt0(sz10, sz00) = all_214_2 % 152.50/23.85 | | | | | | | | | | | | | | | | | (137) sdtpldt0(sz10, xk) = all_214_3 % 152.50/23.85 | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | BETA: splitting (53) gives: % 152.50/23.85 | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | Case 1: % 152.50/23.85 | | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | | (138) xk = sz00 % 152.50/23.85 | | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | | REDUCE: (12), (138) imply: % 152.50/23.85 | | | | | | | | | | | | | | | | | | (139) $false % 152.50/23.85 | | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | | CLOSE: (139) is inconsistent. % 152.50/23.85 | | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | Case 2: % 152.50/23.85 | | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | | (140) sz10 = sz00 | ? [v0: int] : (( ~ (v0 = 0) & % 152.50/23.85 | | | | | | | | | | | | | | | | | | doDivides0(sz00, xk) = v0) | ( ~ (v0 = 0) & % 152.50/23.85 | | | | | | | | | | | | | | | | | | aNaturalNumber0(xk) = v0)) % 152.50/23.85 | | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | | BETA: splitting (42) gives: % 152.50/23.85 | | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | | Case 1: % 152.50/23.85 | | | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | | | (141) xk = sz00 % 152.50/23.85 | | | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | | | REDUCE: (12), (141) imply: % 152.50/23.85 | | | | | | | | | | | | | | | | | | | (142) $false % 152.50/23.85 | | | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | | | CLOSE: (142) is inconsistent. % 152.50/23.85 | | | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | | Case 2: % 152.50/23.85 | | | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | | | (143) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 152.50/23.85 | | | | | | | | | | | | | | | | | | | $i] : ( ~ (v3 = v2) & ~ (v1 = v0) & % 152.50/23.85 | | | | | | | | | | | | | | | | | | | sdtpldt0(xk, xk) = v2 & sdtpldt0(xk, xk) = v0 & % 152.50/23.85 | | | | | | | | | | | | | | | | | | | sdtpldt0(xk, sz00) = v1 & sdtpldt0(sz00, xk) = % 152.50/23.85 | | | | | | | | | | | | | | | | | | | v3 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.50/23.85 | | | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (143) with fresh symbols all_226_0, % 152.50/23.85 | | | | | | | | | | | | | | | | | | | all_226_1, all_226_2, all_226_3 gives: % 152.50/23.85 | | | | | | | | | | | | | | | | | | | (144) ~ (all_226_0 = all_226_1) & ~ (all_226_2 = % 152.50/23.85 | | | | | | | | | | | | | | | | | | | all_226_3) & sdtpldt0(xk, xk) = all_226_1 & % 152.50/23.85 | | | | | | | | | | | | | | | | | | | sdtpldt0(xk, xk) = all_226_3 & sdtpldt0(xk, sz00) % 152.50/23.85 | | | | | | | | | | | | | | | | | | | = all_226_2 & sdtpldt0(sz00, xk) = all_226_0 & % 152.50/23.85 | | | | | | | | | | | | | | | | | | | $i(all_226_0) & $i(all_226_1) & $i(all_226_2) & % 152.50/23.85 | | | | | | | | | | | | | | | | | | | $i(all_226_3) % 152.50/23.85 | | | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | | | ALPHA: (144) implies: % 152.50/23.85 | | | | | | | | | | | | | | | | | | | (145) sdtpldt0(xk, sz00) = all_226_2 % 152.50/23.85 | | | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | | | BETA: splitting (56) gives: % 152.50/23.85 | | | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | | | Case 1: % 152.50/23.85 | | | | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | | | | (146) ~ (all_58_0 = 0) & isPrime0(xk) = all_58_0 % 152.50/23.85 | | | | | | | | | | | | | | | | | | | | % 152.50/23.85 | | | | | | | | | | | | | | | | | | | | ALPHA: (146) implies: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | (147) ~ (all_58_0 = 0) % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | (148) isPrime0(xk) = all_58_0 % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (21) with 0, all_58_0, xk, % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | simplifying with (17), (148) gives: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | (149) all_58_0 = 0 % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | REDUCE: (147), (149) imply: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | (150) $false % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | CLOSE: (150) is inconsistent. % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | Case 2: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | (151) ~ (all_58_1 = 0) & doDivides0(xk, xk) = all_58_1 % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | ALPHA: (151) implies: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | (152) ~ (all_58_1 = 0) % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | (153) doDivides0(xk, xk) = all_58_1 % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | BETA: splitting (37) gives: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | Case 1: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | (154) xk = sz10 % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | REDUCE: (13), (154) imply: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | (155) $false % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | CLOSE: (155) is inconsistent. % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | Case 2: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | (156) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | $i] : ( ~ (v3 = v2) & ~ (v1 = v0) & % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | sdtpldt0(xk, sz10) = v3 & sdtpldt0(sz10, xk) = % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | v1 & sdtpldt0(sz10, sz10) = v2 & sdtpldt0(sz10, % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | sz10) = v0 & $i(v3) & $i(v2) & $i(v1) & % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | $i(v0)) % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (156) with fresh symbols all_242_0, % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | all_242_1, all_242_2, all_242_3 gives: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | (157) ~ (all_242_0 = all_242_1) & ~ (all_242_2 = % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | all_242_3) & sdtpldt0(xk, sz10) = all_242_0 & % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | sdtpldt0(sz10, xk) = all_242_2 & sdtpldt0(sz10, % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | sz10) = all_242_1 & sdtpldt0(sz10, sz10) = % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | all_242_3 & $i(all_242_0) & $i(all_242_1) & % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | $i(all_242_2) & $i(all_242_3) % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | ALPHA: (157) implies: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | (158) sdtpldt0(sz10, xk) = all_242_2 % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | BETA: splitting (35) gives: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | Case 1: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | (159) xk = sz00 % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (12), (159) imply: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | (160) $false % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | CLOSE: (160) is inconsistent. % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | Case 2: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | (161) xk = sz10 | ? [v0: $i] : ? [v1: $i] : ? [v2: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | $i] : ? [v3: $i] : ( ~ (v3 = v2) & ~ (v1 = v0) % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | & sdtasdt0(xk, xk) = v2 & sdtasdt0(xk, xk) = v0 % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | & sdtasdt0(xk, sz10) = v1 & sdtasdt0(sz10, xk) = % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | v3 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (32) gives: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | Case 1: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | (162) xk = sz00 % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (12), (162) imply: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | (163) $false % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (163) is inconsistent. % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | Case 2: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | (164) xk = sz10 | ? [v0: $i] : ? [v1: $i] : ? [v2: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | $i] : ? [v3: $i] : ( ~ (v3 = v2) & ~ (v1 = v0) % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | & sdtasdt0(xk, xk) = v3 & sdtasdt0(xk, xk) = v1 % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | & sdtasdt0(xk, sz10) = v0 & sdtasdt0(sz10, xk) = % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | v2 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (161) gives: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | (165) xk = sz10 % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (13), (165) imply: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | (166) $false % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (166) is inconsistent. % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | (167) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | $i] : ( ~ (v3 = v2) & ~ (v1 = v0) & % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(xk, xk) = v2 & sdtasdt0(xk, xk) = v0 & % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(xk, sz10) = v1 & sdtasdt0(sz10, xk) = % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | v3 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (167) with fresh symbols all_283_0, % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | all_283_1, all_283_2, all_283_3 gives: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | (168) ~ (all_283_0 = all_283_1) & ~ (all_283_2 = % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | all_283_3) & sdtasdt0(xk, xk) = all_283_1 & % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(xk, xk) = all_283_3 & sdtasdt0(xk, sz10) % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | = all_283_2 & sdtasdt0(sz10, xk) = all_283_0 & % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | $i(all_283_0) & $i(all_283_1) & $i(all_283_2) & % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | $i(all_283_3) % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (168) implies: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | (169) sdtasdt0(sz10, xk) = all_283_0 % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | (170) sdtasdt0(xk, sz10) = all_283_2 % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (120) gives: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | (171) sz10 = sz00 % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (2), (171) imply: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | (172) $false % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (172) is inconsistent. % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | (173) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | $i] : ( ~ (v3 = v2) & ~ (v1 = v0) & % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(xk, sz10) = v1 & sdtasdt0(xk, sz00) = % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | v0 & sdtasdt0(sz10, xk) = v3 & sdtasdt0(sz00, % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | xk) = v2 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (173) with fresh symbols all_289_0, % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | all_289_1, all_289_2, all_289_3 gives: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | (174) ~ (all_289_0 = all_289_1) & ~ (all_289_2 = % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | all_289_3) & sdtasdt0(xk, sz10) = all_289_2 & % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(xk, sz00) = all_289_3 & sdtasdt0(sz10, % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | xk) = all_289_0 & sdtasdt0(sz00, xk) = all_289_1 % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | & $i(all_289_0) & $i(all_289_1) & $i(all_289_2) & % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | $i(all_289_3) % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (174) implies: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | (175) sdtasdt0(sz10, xk) = all_289_0 % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | (176) sdtasdt0(xk, sz10) = all_289_2 % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (164) gives: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | | (177) xk = sz10 % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (13), (177) imply: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | | (178) $false % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (178) is inconsistent. % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | | (179) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | | $i] : ( ~ (v3 = v2) & ~ (v1 = v0) & % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(xk, xk) = v3 & sdtasdt0(xk, xk) = v1 & % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(xk, sz10) = v0 & sdtasdt0(sz10, xk) = % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | | v2 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (179) with fresh symbols all_295_0, % 152.50/23.86 | | | | | | | | | | | | | | | | | | | | | | | | | | all_295_1, all_295_2, all_295_3 gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | (180) ~ (all_295_0 = all_295_1) & ~ (all_295_2 = % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | all_295_3) & sdtasdt0(xk, xk) = all_295_0 & % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(xk, xk) = all_295_2 & sdtasdt0(xk, sz10) % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | = all_295_3 & sdtasdt0(sz10, xk) = all_295_1 & % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | $i(all_295_0) & $i(all_295_1) & $i(all_295_2) & % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | $i(all_295_3) % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (180) implies: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | (181) sdtasdt0(sz10, xk) = all_295_1 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | (182) sdtasdt0(xk, sz10) = all_295_3 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (140) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | (183) sz10 = sz00 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (2), (183) imply: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | (184) $false % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (184) is inconsistent. % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | (185) ? [v0: int] : (( ~ (v0 = 0) & doDivides0(sz00, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | xk) = v0) | ( ~ (v0 = 0) & % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xk) = v0)) % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (185) with fresh symbol all_300_0 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | (186) ( ~ (all_300_0 = 0) & doDivides0(sz00, xk) = % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | all_300_0) | ( ~ (all_300_0 = 0) & % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xk) = all_300_0) % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (186) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with sz10, all_140_3, sz00, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz10, simplifying with (31), (74) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (187) all_140_3 = sz10 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_140_3, all_162_0, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz00, sz10, simplifying with (74), (90) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (188) all_162_0 = all_140_3 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_162_0, all_208_0, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz00, sz10, simplifying with (90), (130) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (189) all_208_0 = all_162_0 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_134_1, all_208_0, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz00, sz10, simplifying with (69), (130) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (190) all_208_0 = all_134_1 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_140_3, all_214_2, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz00, sz10, simplifying with (74), (136) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (191) all_214_2 = all_140_3 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_128_2, all_214_2, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz00, sz10, simplifying with (64), (136) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (192) all_214_2 = all_128_2 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_171_1, all_202_0, xk, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz10, simplifying with (95), (125) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (193) all_202_0 = all_171_1 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_214_3, all_242_2, xk, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz10, simplifying with (137), (158) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (194) all_242_2 = all_214_3 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_202_0, all_242_2, xk, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz10, simplifying with (125), (158) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (195) all_242_2 = all_202_0 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_186_1, all_242_2, xk, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz10, simplifying with (111), (158) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (196) all_242_2 = all_186_1 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_181_3, all_242_2, xk, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz10, simplifying with (106), (158) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (197) all_242_2 = all_181_3 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_176_0, all_242_2, xk, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz10, simplifying with (100), (158) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (198) all_242_2 = all_176_0 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_150_3, all_186_2, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz00, xk, simplifying with (80), (112) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (199) all_186_2 = all_150_3 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_186_2, all_192_0, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz00, xk, simplifying with (112), (117) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (200) all_192_0 = all_186_2 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_176_3, all_192_0, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz00, xk, simplifying with (101), (117) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (201) all_192_0 = all_176_3 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_156_1, all_192_0, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz00, xk, simplifying with (85), (117) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (202) all_192_0 = all_156_1 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_176_3, all_208_1, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz00, xk, simplifying with (101), (131) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (203) all_208_1 = all_176_3 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_208_1, all_226_2, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz00, xk, simplifying with (131), (145) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (204) all_226_2 = all_208_1 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with xk, all_226_2, sz00, xk, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (52), (145) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (205) all_226_2 = xk % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (23) with all_289_0, all_295_1, xk, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz10, simplifying with (175), (181) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (206) all_295_1 = all_289_0 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (23) with all_283_0, all_295_1, xk, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz10, simplifying with (169), (181) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (207) all_295_1 = all_283_0 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (23) with xk, all_295_1, xk, sz10, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (49), (181) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (208) all_295_1 = xk % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (23) with all_283_2, all_289_2, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz10, xk, simplifying with (170), (176) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (209) all_289_2 = all_283_2 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (23) with all_289_2, all_295_3, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz10, xk, simplifying with (176), (182) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (210) all_295_3 = all_289_2 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (23) with xk, all_295_3, sz10, xk, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (50), (182) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (211) all_295_3 = xk % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (24) with all_57_0, all_58_1, xk, % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | xk, simplifying with (58), (153) gives: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (212) all_58_1 = all_57_0 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (206), (208) imply: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (213) all_289_0 = xk % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (206), (207) imply: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (214) all_289_0 = all_283_0 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (210), (211) imply: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (215) all_289_2 = xk % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (215) implies: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (216) all_289_2 = xk % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (213), (214) imply: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (217) all_283_0 = xk % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (217) implies: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (218) all_283_0 = xk % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (209), (216) imply: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (219) all_283_2 = xk % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (219) implies: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (220) all_283_2 = xk % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (194), (196) imply: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (221) all_214_3 = all_186_1 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (194), (195) imply: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (222) all_214_3 = all_202_0 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (194), (198) imply: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (223) all_214_3 = all_176_0 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (194), (197) imply: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (224) all_214_3 = all_181_3 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (204), (205) imply: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (225) all_208_1 = xk % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (225) implies: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (226) all_208_1 = xk % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (191), (192) imply: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (227) all_140_3 = all_128_2 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (227) implies: % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (228) all_140_3 = all_128_2 % 152.50/23.87 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (221), (222) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (229) all_202_0 = all_186_1 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (229) implies: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (230) all_202_0 = all_186_1 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (221), (224) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (231) all_186_1 = all_181_3 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (221), (223) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (232) all_186_1 = all_176_0 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (189), (190) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (233) all_162_0 = all_134_1 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (233) implies: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (234) all_162_0 = all_134_1 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (203), (226) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (235) all_176_3 = xk % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (235) implies: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (236) all_176_3 = xk % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (193), (230) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (237) all_186_1 = all_171_1 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (237) implies: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (238) all_186_1 = all_171_1 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (200), (202) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (239) all_186_2 = all_156_1 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (239) implies: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (240) all_186_2 = all_156_1 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (201), (202) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (241) all_176_3 = all_156_1 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (241) implies: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (242) all_176_3 = all_156_1 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (231), (238) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (243) all_181_3 = all_171_1 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (231), (232) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (244) all_181_3 = all_176_0 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (199), (240) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (245) all_156_1 = all_150_3 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (245) implies: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (246) all_156_1 = all_150_3 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (243), (244) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (247) all_176_0 = all_171_1 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (247) implies: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (248) all_176_0 = all_171_1 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (236), (242) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (249) all_156_1 = xk % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (249) implies: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (250) all_156_1 = xk % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (188), (234) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (251) all_140_3 = all_134_1 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (251) implies: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (252) all_140_3 = all_134_1 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (246), (250) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (253) all_150_3 = xk % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (187), (252) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (254) all_134_1 = sz10 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (228), (252) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (255) all_134_1 = all_128_2 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (254), (255) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (256) all_128_2 = sz10 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (152), (212) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (257) ~ (all_57_0 = 0) % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (6) with sz10, sz10, xk, sz10, xk, % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_171_1, simplifying with (15), (16), (29), % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (49), (95) gives: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (258) ? [v0: int] : ? [v1: int] : ? [v2: int] : ? % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | [v3: $i] : ? [v4: int] : ? [v5: $i] : ? [v6: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | $i] : ? [v7: $i] : ? [v8: $i] : ((v8 = v5 & v4 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | = all_171_1 & sdtasdt0(v3, sz10) = v5 & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(xk, sz10) = v7 & sdtasdt0(sz10, v3) = % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_171_1 & sdtasdt0(sz10, sz10) = v6 & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sdtpldt0(v6, v7) = v5 & sdtpldt0(sz10, xk) = % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | v3 & $i(v7) & $i(v6) & $i(v5) & $i(v3) & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | $i(all_171_1)) | ( ~ (v2 = 0) & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xk) = v2) | ( ~ (v1 = 0) & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(sz10) = v1) | ( ~ (v0 = 0) & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(sz10) = v0)) % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (9) with xk, xk, all_57_0, sz10, % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (3), (15), (16), (58) gives: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (259) all_57_0 = 0 | ? [v0: any] : ? [v1: int] : (( ~ % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (v1 = 0) & aNaturalNumber0(xk) = v1) | ( ~ (v0 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | = xk) & sdtasdt0(xk, sz10) = v0 & $i(v0)) | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | ( ~ (v0 = 0) & aNaturalNumber0(xk) = v0)) % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (258) with fresh symbols all_380_0, % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_380_1, all_380_2, all_380_3, all_380_4, % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_380_5, all_380_6, all_380_7, all_380_8 gives: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (260) (all_380_0 = all_380_3 & all_380_4 = all_171_1 & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(all_380_5, sz10) = all_380_3 & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(xk, sz10) = all_380_1 & sdtasdt0(sz10, % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_380_5) = all_171_1 & sdtasdt0(sz10, sz10) % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | = all_380_2 & sdtpldt0(all_380_2, all_380_1) = % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_380_3 & sdtpldt0(sz10, xk) = all_380_5 & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | $i(all_380_1) & $i(all_380_2) & $i(all_380_3) & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | $i(all_380_5) & $i(all_171_1)) | ( ~ (all_380_6 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | = 0) & aNaturalNumber0(xk) = all_380_6) | ( ~ % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (all_380_7 = 0) & aNaturalNumber0(sz10) = % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_380_7) | ( ~ (all_380_8 = 0) & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(sz10) = all_380_8) % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (260) gives: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (261) (all_380_0 = all_380_3 & all_380_4 = all_171_1 & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(all_380_5, sz10) = all_380_3 & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(xk, sz10) = all_380_1 & sdtasdt0(sz10, % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_380_5) = all_171_1 & sdtasdt0(sz10, sz10) % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | = all_380_2 & sdtpldt0(all_380_2, all_380_1) = % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_380_3 & sdtpldt0(sz10, xk) = all_380_5 & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | $i(all_380_1) & $i(all_380_2) & $i(all_380_3) & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | $i(all_380_5) & $i(all_171_1)) | ( ~ (all_380_6 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | = 0) & aNaturalNumber0(xk) = all_380_6) % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (261) gives: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (262) all_380_0 = all_380_3 & all_380_4 = all_171_1 & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(all_380_5, sz10) = all_380_3 & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(xk, sz10) = all_380_1 & sdtasdt0(sz10, % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_380_5) = all_171_1 & sdtasdt0(sz10, sz10) = % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_380_2 & sdtpldt0(all_380_2, all_380_1) = % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_380_3 & sdtpldt0(sz10, xk) = all_380_5 & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | $i(all_380_1) & $i(all_380_2) & $i(all_380_3) & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | $i(all_380_5) & $i(all_171_1) % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (262) implies: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (263) sdtasdt0(xk, sz10) = all_380_1 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (259) gives: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (264) all_57_0 = 0 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (257), (264) imply: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (265) $false % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (265) is inconsistent. % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (266) ? [v0: any] : ? [v1: int] : (( ~ (v1 = 0) & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xk) = v1) | ( ~ (v0 = xk) & % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(xk, sz10) = v0 & $i(v0)) | ( ~ (v0 = % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 0) & aNaturalNumber0(xk) = v0)) % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (266) with fresh symbols all_559_0, % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_559_1 gives: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (267) ( ~ (all_559_0 = 0) & aNaturalNumber0(xk) = % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_559_0) | ( ~ (all_559_1 = xk) & sdtasdt0(xk, % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz10) = all_559_1 & $i(all_559_1)) | ( ~ % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (all_559_1 = 0) & aNaturalNumber0(xk) = % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_559_1) % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (267) gives: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (268) ~ (all_559_0 = 0) & aNaturalNumber0(xk) = % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_559_0 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (268) implies: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (269) ~ (all_559_0 = 0) % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (270) aNaturalNumber0(xk) = all_559_0 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (20) with 0, all_559_0, xk, % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (11), (270) gives: % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (271) all_559_0 = 0 % 152.50/23.88 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (269), (271) imply: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (272) $false % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (272) is inconsistent. % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (273) ( ~ (all_559_1 = xk) & sdtasdt0(xk, sz10) = % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_559_1 & $i(all_559_1)) | ( ~ (all_559_1 = 0) % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | & aNaturalNumber0(xk) = all_559_1) % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (273) gives: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (274) ~ (all_559_1 = xk) & sdtasdt0(xk, sz10) = % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_559_1 & $i(all_559_1) % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (274) implies: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (275) ~ (all_559_1 = xk) % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (276) sdtasdt0(xk, sz10) = all_559_1 % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (23) with xk, all_559_1, sz10, xk, % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (50), (276) gives: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (277) all_559_1 = xk % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (23) with all_380_1, all_559_1, % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | sz10, xk, simplifying with (263), (276) gives: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (278) all_559_1 = all_380_1 % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (277), (278) imply: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (279) all_380_1 = xk % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (275), (277) imply: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (280) $false % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (280) is inconsistent. % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (281) ~ (all_559_1 = 0) & aNaturalNumber0(xk) = % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_559_1 % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (281) implies: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (282) ~ (all_559_1 = 0) % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (283) aNaturalNumber0(xk) = all_559_1 % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (20) with 0, all_559_1, xk, % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (11), (283) gives: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (284) all_559_1 = 0 % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (282), (284) imply: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (285) $false % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (285) is inconsistent. % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (286) ~ (all_380_6 = 0) & aNaturalNumber0(xk) = % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_380_6 % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (286) implies: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (287) ~ (all_380_6 = 0) % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (288) aNaturalNumber0(xk) = all_380_6 % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (20) with 0, all_380_6, xk, % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (11), (288) gives: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (289) all_380_6 = 0 % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (287), (289) imply: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (290) $false % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (290) is inconsistent. % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (291) ( ~ (all_380_7 = 0) & aNaturalNumber0(sz10) = % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_380_7) | ( ~ (all_380_8 = 0) & % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(sz10) = all_380_8) % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (291) gives: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (292) ~ (all_380_7 = 0) & aNaturalNumber0(sz10) = % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_380_7 % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (292) implies: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (293) ~ (all_380_7 = 0) % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (294) aNaturalNumber0(sz10) = all_380_7 % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (20) with 0, all_380_7, sz10, % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (3), (294) gives: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (295) all_380_7 = 0 % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (293), (295) imply: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (296) $false % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (296) is inconsistent. % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (297) ~ (all_380_8 = 0) & aNaturalNumber0(sz10) = % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_380_8 % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (297) implies: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (298) ~ (all_380_8 = 0) % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (299) aNaturalNumber0(sz10) = all_380_8 % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (20) with 0, all_380_8, sz10, % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (3), (299) gives: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (300) all_380_8 = 0 % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (298), (300) imply: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (301) $false % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (301) is inconsistent. % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (302) ~ (all_300_0 = 0) & aNaturalNumber0(xk) = % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_300_0 % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (302) implies: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (303) ~ (all_300_0 = 0) % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (304) aNaturalNumber0(xk) = all_300_0 % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (20) with 0, all_300_0, xk, % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (11), (304) gives: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (305) all_300_0 = 0 % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (303), (305) imply: % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (306) $false % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (306) is inconsistent. % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | | % 152.50/23.89 | | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | | % 152.50/23.89 | | | | | | | | | End of split % 152.50/23.89 | | | | | | | | | % 152.50/23.89 | | | | | | | | End of split % 152.50/23.89 | | | | | | | | % 152.50/23.89 | | | | | | | End of split % 152.50/23.89 | | | | | | | % 152.50/23.89 | | | | | | End of split % 152.50/23.89 | | | | | | % 152.50/23.89 | | | | | End of split % 152.50/23.89 | | | | | % 152.50/23.89 | | | | End of split % 152.50/23.89 | | | | % 152.50/23.89 | | | End of split % 152.50/23.89 | | | % 152.50/23.89 | | End of split % 152.50/23.89 | | % 152.50/23.89 | Case 2: % 152.50/23.89 | | % 152.50/23.89 | | (307) ~ (all_57_1 = 0) & aNaturalNumber0(xk) = all_57_1 % 152.50/23.89 | | % 152.50/23.89 | | ALPHA: (307) implies: % 152.50/23.89 | | (308) ~ (all_57_1 = 0) % 152.50/23.89 | | (309) aNaturalNumber0(xk) = all_57_1 % 152.50/23.89 | | % 152.50/23.89 | | GROUND_INST: instantiating (20) with 0, all_57_1, xk, simplifying with (11), % 152.50/23.89 | | (309) gives: % 152.50/23.89 | | (310) all_57_1 = 0 % 152.50/23.89 | | % 152.50/23.89 | | REDUCE: (308), (310) imply: % 152.50/23.89 | | (311) $false % 152.50/23.89 | | % 152.50/23.89 | | CLOSE: (311) is inconsistent. % 152.50/23.89 | | % 152.50/23.89 | End of split % 152.50/23.89 | % 152.50/23.89 End of proof % 152.50/23.89 % SZS output end Proof for theBenchmark % 152.50/23.89 % 152.50/23.89 23278ms %------------------------------------------------------------------------------