%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : RNG126+4 : TPTP v8.1.2. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n027.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 13:58:02 EDT 2023 % Result : Theorem 46.27s 7.13s % Output : Proof 153.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : RNG126+4 : TPTP v8.1.2. Released v4.0.0. % 0.00/0.11 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.10/0.31 % Computer : n027.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Sun Aug 27 02:17:05 EDT 2023 % 0.10/0.31 % CPUTime : % 0.16/0.59 ________ _____ % 0.16/0.59 ___ __ \_________(_)________________________________ % 0.16/0.59 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.16/0.59 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.16/0.59 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.16/0.59 % 0.16/0.59 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.16/0.59 (2023-06-19) % 0.16/0.59 % 0.16/0.59 (c) Philipp Rümmer, 2009-2023 % 0.16/0.59 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.16/0.59 Amanda Stjerna. % 0.16/0.59 Free software under BSD-3-Clause. % 0.16/0.59 % 0.16/0.59 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.16/0.59 % 0.16/0.59 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.16/0.61 Running up to 7 provers in parallel. % 0.16/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.16/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.16/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.16/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.16/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.16/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.16/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 4.04/1.36 Prover 4: Preprocessing ... % 4.04/1.37 Prover 1: Preprocessing ... % 4.04/1.41 Prover 3: Preprocessing ... % 4.04/1.41 Prover 5: Preprocessing ... % 4.04/1.41 Prover 2: Preprocessing ... % 4.04/1.41 Prover 0: Preprocessing ... % 4.04/1.41 Prover 6: Preprocessing ... % 15.12/2.90 Prover 3: Constructing countermodel ... % 15.12/2.93 Prover 1: Constructing countermodel ... % 15.12/2.94 Prover 6: Proving ... % 15.12/2.97 Prover 5: Proving ... % 16.48/3.12 Prover 2: Proving ... % 17.67/3.28 Prover 4: Constructing countermodel ... % 18.65/3.44 Prover 0: Proving ... % 46.27/7.12 Prover 0: proved (6475ms) % 46.27/7.13 % 46.27/7.13 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 46.27/7.13 % 46.27/7.13 Prover 3: stopped % 46.51/7.14 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 46.51/7.14 Prover 6: stopped % 46.51/7.14 Prover 5: stopped % 46.51/7.16 Prover 2: stopped % 46.51/7.17 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 46.51/7.17 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 46.51/7.17 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 46.51/7.17 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 48.26/7.42 Prover 7: Preprocessing ... % 48.26/7.43 Prover 10: Preprocessing ... % 48.26/7.46 Prover 13: Preprocessing ... % 48.26/7.51 Prover 8: Preprocessing ... % 48.62/7.53 Prover 11: Preprocessing ... % 50.75/7.72 Prover 10: Constructing countermodel ... % 51.22/7.81 Prover 13: Warning: ignoring some quantifiers % 51.22/7.84 Prover 13: Constructing countermodel ... % 52.57/8.00 Prover 7: Constructing countermodel ... % 52.57/8.10 Prover 11: Constructing countermodel ... % 52.57/8.11 Prover 8: Warning: ignoring some quantifiers % 52.57/8.12 Prover 8: Constructing countermodel ... % 81.91/11.77 Prover 13: stopped % 81.91/11.79 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 82.48/11.90 Prover 16: Preprocessing ... % 82.48/12.06 Prover 16: Warning: ignoring some quantifiers % 82.48/12.07 Prover 16: Constructing countermodel ... % 114.13/15.98 Prover 1: stopped % 114.13/15.98 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 114.13/16.06 Prover 19: Preprocessing ... % 115.67/16.36 Prover 19: Warning: ignoring some quantifiers % 115.67/16.37 Prover 19: Constructing countermodel ... % 122.36/17.12 Prover 16: stopped % 140.14/19.56 Prover 19: stopped % 151.36/21.41 Prover 4: Found proof (size 287) % 151.36/21.41 Prover 4: proved (20779ms) % 151.36/21.41 Prover 7: stopped % 151.36/21.41 Prover 10: stopped % 151.36/21.43 Prover 11: stopped % 151.36/21.46 Prover 8: stopped % 151.36/21.46 % 151.36/21.46 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 151.36/21.46 % 151.93/21.51 % SZS output start Proof for theBenchmark % 151.93/21.51 Assumptions after simplification: % 151.93/21.51 --------------------------------- % 151.93/21.51 % 151.93/21.51 (mAMDistr) % 151.97/21.56 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 151.97/21.56 $i] : ( ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v1, v0) = v3) | ~ % 151.97/21.56 (sdtpldt0(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : % 151.97/21.56 ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? % 151.97/21.56 [v12: $i] : ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v9, v0) = v14 & % 151.97/21.56 sdtasdt0(v0, v9) = v10 & sdtasdt0(v0, v2) = v12 & sdtasdt0(v0, v1) = v11 & % 151.97/21.56 sdtpldt0(v11, v12) = v13 & sdtpldt0(v1, v2) = v9 & aElement0(v2) = v8 & % 151.97/21.56 aElement0(v1) = v7 & aElement0(v0) = v6 & $i(v14) & $i(v13) & $i(v12) & % 151.97/21.56 $i(v11) & $i(v10) & $i(v9) & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | % 151.97/21.56 (v14 = v5 & v13 = v10)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 151.97/21.56 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ % 151.97/21.56 (sdtasdt0(v0, v1) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) % 151.97/21.56 | ~ $i(v0) | ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? % 151.97/21.56 [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : % 151.97/21.56 (sdtasdt0(v9, v0) = v11 & sdtasdt0(v2, v0) = v13 & sdtasdt0(v1, v0) = v12 & % 151.97/21.56 sdtasdt0(v0, v9) = v10 & sdtpldt0(v12, v13) = v14 & sdtpldt0(v1, v2) = v9 % 151.97/21.56 & aElement0(v2) = v8 & aElement0(v1) = v7 & aElement0(v0) = v6 & $i(v14) & % 151.97/21.56 $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) & ( ~ (v8 = 0) | ~ (v7 = % 151.97/21.56 0) | ~ (v6 = 0) | (v14 = v11 & v10 = v5)))) & ! [v0: $i] : ! [v1: % 151.97/21.56 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (sdtasdt0(v3, v0) = v4) % 151.97/21.56 | ~ (sdtpldt0(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: % 151.97/21.56 any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? [v9: $i] : ? [v10: % 151.97/21.56 $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : % 151.97/21.56 (sdtasdt0(v2, v0) = v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v3) = v8 & % 151.97/21.56 sdtasdt0(v0, v2) = v10 & sdtasdt0(v0, v1) = v9 & sdtpldt0(v12, v13) = v14 % 151.97/21.56 & sdtpldt0(v9, v10) = v11 & aElement0(v2) = v7 & aElement0(v1) = v6 & % 151.97/21.56 aElement0(v0) = v5 & $i(v14) & $i(v13) & $i(v12) & $i(v11) & $i(v10) & % 151.97/21.56 $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | (v14 = v4 & % 151.97/21.56 v11 = v8)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 151.97/21.56 ! [v4: $i] : ( ~ (sdtasdt0(v0, v3) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ % 151.97/21.56 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] % 151.97/21.56 : ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : % 151.97/21.56 ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v3, v0) = v11 & sdtasdt0(v2, v0) = % 151.97/21.56 v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v2) = v9 & sdtasdt0(v0, v1) = % 151.97/21.56 v8 & sdtpldt0(v12, v13) = v14 & sdtpldt0(v8, v9) = v10 & aElement0(v2) = % 151.97/21.56 v7 & aElement0(v1) = v6 & aElement0(v0) = v5 & $i(v14) & $i(v13) & $i(v12) % 151.97/21.56 & $i(v11) & $i(v10) & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ % 151.97/21.56 (v5 = 0) | (v14 = v11 & v10 = v4)))) % 151.97/21.56 % 151.97/21.56 (mDefDvs) % 151.97/21.57 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (aDivisorOf0(v1, v0) = % 151.97/21.57 v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? % 151.97/21.57 [v4: any] : (doDivides0(v1, v0) = v4 & aElement0(v1) = v3 & ( ~ (v4 = 0) | % 151.97/21.57 ~ (v3 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ % 151.97/21.57 (doDivides0(v1, v0) = v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | % 151.97/21.57 ? [v3: any] : ? [v4: any] : (aDivisorOf0(v1, v0) = v3 & aElement0(v1) = v4 % 151.97/21.57 & ( ~ (v3 = 0) | (v4 = 0 & v2 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! % 151.97/21.57 [v2: any] : ( ~ (aElement0(v1) = v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ % 151.97/21.57 $i(v0) | ? [v3: any] : ? [v4: any] : (aDivisorOf0(v1, v0) = v3 & % 151.97/21.57 doDivides0(v1, v0) = v4 & ( ~ (v3 = 0) | (v4 = 0 & v2 = 0)))) & ! [v0: % 151.97/21.57 $i] : ! [v1: $i] : ( ~ (aDivisorOf0(v1, v0) = 0) | ~ (aElement0(v0) = 0) | % 151.97/21.57 ~ $i(v1) | ~ $i(v0) | (doDivides0(v1, v0) = 0 & aElement0(v1) = 0)) & ! % 151.97/21.57 [v0: $i] : ! [v1: $i] : ( ~ (doDivides0(v1, v0) = 0) | ~ (aElement0(v0) = 0) % 151.97/21.57 | ~ $i(v1) | ~ $i(v0) | ? [v2: any] : ? [v3: any] : (aDivisorOf0(v1, v0) % 151.97/21.57 = v3 & aElement0(v1) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0: $i] : ! % 151.97/21.57 [v1: $i] : ( ~ (aElement0(v1) = 0) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ % 151.97/21.57 $i(v0) | ? [v2: any] : ? [v3: any] : (aDivisorOf0(v1, v0) = v3 & % 151.97/21.57 doDivides0(v1, v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 151.97/21.57 % 151.97/21.57 (mDefIdeal) % 151.97/21.58 ! [v0: $i] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 151.97/21.58 $i] : ( ~ (aSet0(v0) = v1) | ~ (aElementOf0(v2, v0) = 0) | ~ (sdtasdt0(v3, % 151.97/21.58 v2) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v0) | ? [v5: int] : ? [v6: % 151.97/21.58 any] : (( ~ (v5 = 0) & aIdeal0(v0) = v5) | (aElementOf0(v4, v0) = v6 & % 151.97/21.58 aElement0(v3) = v5 & ( ~ (v5 = 0) | v6 = 0)))) & ! [v0: $i] : ! [v1: % 151.97/21.58 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 151.97/21.58 (aSet0(v0) = v1) | ~ (aElementOf0(v2, v0) = 0) | ~ (sdtpldt0(v2, v3) = v4) % 151.97/21.58 | ~ $i(v3) | ~ $i(v2) | ~ $i(v0) | ? [v5: int] : ? [v6: any] : (( ~ (v5 % 151.97/21.58 = 0) & aIdeal0(v0) = v5) | (aElementOf0(v4, v0) = v6 & aElementOf0(v3, % 151.97/21.58 v0) = v5 & ( ~ (v5 = 0) | v6 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! % 151.97/21.58 [v2: $i] : ! [v3: $i] : ( ~ (aIdeal0(v0) = 0) | ~ (aElementOf0(v1, v0) = 0) % 151.97/21.58 | ~ (sdtasdt0(v2, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 151.97/21.58 any] : ? [v5: any] : (aElementOf0(v3, v0) = v5 & aElement0(v2) = v4 & ( ~ % 151.97/21.58 (v4 = 0) | v5 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 151.97/21.58 $i] : ( ~ (aIdeal0(v0) = 0) | ~ (aElementOf0(v1, v0) = 0) | ~ % 151.97/21.58 (sdtpldt0(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : % 151.97/21.58 ? [v5: any] : (aElementOf0(v3, v0) = v5 & aElementOf0(v2, v0) = v4 & ( ~ % 151.97/21.58 (v4 = 0) | v5 = 0))) & ! [v0: $i] : ! [v1: MultipleValueBool] : ! % 151.97/21.58 [v2: $i] : ! [v3: $i] : ( ~ (aSet0(v0) = v1) | ~ (aElementOf0(v3, v0) = 0) | % 151.97/21.58 ~ (aElementOf0(v2, v0) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v0) | ? [v4: % 151.97/21.58 any] : ? [v5: int] : ((v5 = 0 & aElementOf0(v4, v0) = 0 & sdtpldt0(v2, % 151.97/21.58 v3) = v4 & $i(v4)) | ( ~ (v4 = 0) & aIdeal0(v0) = v4))) & ! [v0: $i] % 151.97/21.58 : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ( ~ (aSet0(v0) = % 151.97/21.58 v1) | ~ (aElementOf0(v2, v0) = 0) | ~ (aElement0(v3) = 0) | ~ $i(v3) | % 151.97/21.58 ~ $i(v2) | ~ $i(v0) | ? [v4: any] : ? [v5: int] : ((v5 = 0 & % 151.97/21.58 aElementOf0(v4, v0) = 0 & sdtasdt0(v3, v2) = v4 & $i(v4)) | ( ~ (v4 = 0) % 151.97/21.58 & aIdeal0(v0) = v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 151.97/21.58 (aIdeal0(v0) = 0) | ~ (aElementOf0(v2, v0) = 0) | ~ (aElementOf0(v1, v0) = % 151.97/21.58 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : (aElementOf0(v3, % 151.97/21.58 v0) = 0 & sdtpldt0(v1, v2) = v3 & $i(v3))) & ! [v0: $i] : ! [v1: $i] : % 151.97/21.58 ! [v2: $i] : ( ~ (aIdeal0(v0) = 0) | ~ (aElementOf0(v1, v0) = 0) | ~ % 151.97/21.58 (aElement0(v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : % 151.97/21.58 (aElementOf0(v3, v0) = 0 & sdtasdt0(v2, v1) = v3 & $i(v3))) & ! [v0: $i] : % 151.97/21.58 ! [v1: int] : (v1 = 0 | ~ (aIdeal0(v0) = v1) | ~ $i(v0) | ? [v2: int] : ? % 151.97/21.58 [v3: $i] : ? [v4: int] : ? [v5: $i] : ? [v6: int] : ? [v7: $i] : ? [v8: % 151.97/21.58 int] : ? [v9: $i] : ? [v10: int] : ? [v11: $i] : ? [v12: int] : % 151.97/21.58 ($i(v9) & $i(v5) & $i(v3) & ((v4 = 0 & aElementOf0(v3, v0) = 0 & ((v10 = 0 & % 151.97/21.58 ~ (v12 = 0) & aElementOf0(v11, v0) = v12 & aElementOf0(v9, v0) = % 151.97/21.59 0 & sdtpldt0(v3, v9) = v11 & $i(v11)) | (v6 = 0 & ~ (v8 = 0) & % 151.97/21.59 aElementOf0(v7, v0) = v8 & sdtasdt0(v5, v3) = v7 & aElement0(v5) = % 151.97/21.59 0 & $i(v7)))) | ( ~ (v2 = 0) & aSet0(v0) = v2)))) & ! [v0: $i] : % 151.97/21.59 ! [v1: int] : (v1 = 0 | ~ (aSet0(v0) = v1) | ~ $i(v0) | ? [v2: int] : ( ~ % 151.97/21.59 (v2 = 0) & aIdeal0(v0) = v2)) & ! [v0: $i] : ( ~ (aIdeal0(v0) = 0) | ~ % 151.97/21.59 $i(v0) | aSet0(v0) = 0) & ! [v0: $i] : ( ~ (aSet0(v0) = 0) | ~ $i(v0) | ? % 151.97/21.59 [v1: int] : ? [v2: $i] : ? [v3: int] : ? [v4: $i] : ? [v5: int] : ? % 151.97/21.59 [v6: $i] : ? [v7: int] : ? [v8: $i] : ? [v9: int] : ? [v10: $i] : ? % 151.97/21.59 [v11: int] : ($i(v8) & $i(v4) & $i(v2) & ((v3 = 0 & aElementOf0(v2, v0) = 0 % 151.97/21.59 & ((v9 = 0 & ~ (v11 = 0) & aElementOf0(v10, v0) = v11 & % 151.97/21.59 aElementOf0(v8, v0) = 0 & sdtpldt0(v2, v8) = v10 & $i(v10)) | (v5 % 151.97/21.59 = 0 & ~ (v7 = 0) & aElementOf0(v6, v0) = v7 & sdtasdt0(v4, v2) = % 151.97/21.59 v6 & aElement0(v4) = 0 & $i(v6)))) | (v1 = 0 & aIdeal0(v0) = 0)))) % 151.97/21.59 % 151.97/21.59 (mEucSort) % 151.97/21.59 $i(sz00) & ! [v0: $i] : ! [v1: $i] : (v0 = sz00 | ~ (sbrdtbr0(v0) = v1) | % 151.97/21.59 ~ $i(v0) | ? [v2: any] : ? [v3: any] : (aNaturalNumber0(v1) = v3 & % 151.97/21.59 aElement0(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0: $i] : (v0 = sz00 | % 151.97/21.59 ~ (aElement0(v0) = 0) | ~ $i(v0) | ? [v1: $i] : (sbrdtbr0(v0) = v1 & % 151.97/21.59 aNaturalNumber0(v1) = 0 & $i(v1))) % 151.97/21.59 % 151.97/21.59 (mMulAsso) % 151.97/21.59 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 151.97/21.59 (sdtasdt0(v3, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) % 151.97/21.59 | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? % 151.97/21.59 [v9: $i] : (sdtasdt0(v1, v2) = v8 & sdtasdt0(v0, v8) = v9 & aElement0(v2) = % 151.97/21.59 v7 & aElement0(v1) = v6 & aElement0(v0) = v5 & $i(v9) & $i(v8) & ( ~ (v7 = % 151.97/21.59 0) | ~ (v6 = 0) | ~ (v5 = 0) | v9 = v4))) & ! [v0: $i] : ! [v1: % 151.97/21.59 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (sdtasdt0(v1, v2) = v3) % 151.97/21.59 | ~ (sdtasdt0(v0, v3) = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: % 151.97/21.59 any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? [v9: $i] : % 151.97/21.59 (sdtasdt0(v8, v2) = v9 & sdtasdt0(v0, v1) = v8 & aElement0(v2) = v7 & % 151.97/21.59 aElement0(v1) = v6 & aElement0(v0) = v5 & $i(v9) & $i(v8) & ( ~ (v7 = 0) | % 151.97/21.59 ~ (v6 = 0) | ~ (v5 = 0) | v9 = v4))) % 151.97/21.59 % 151.97/21.59 (mMulComm) % 151.97/21.59 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v1, v0) = v2) | ~ % 151.97/21.59 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 151.97/21.59 (sdtasdt0(v0, v1) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & $i(v5) & % 151.97/21.59 ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) & ! [v0: $i] : ! [v1: $i] : ! % 151.97/21.59 [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] % 151.97/21.59 : ? [v4: any] : ? [v5: $i] : (sdtasdt0(v1, v0) = v5 & aElement0(v1) = v4 & % 151.97/21.59 aElement0(v0) = v3 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 151.97/21.59 % 151.97/21.59 (mSortsB) % 151.97/21.59 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 151.97/21.59 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 151.97/21.59 (aElement0(v2) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & ( ~ (v4 = 0) % 151.97/21.59 | ~ (v3 = 0) | v5 = 0))) % 151.97/21.59 % 151.97/21.59 (mSortsB_02) % 151.97/21.60 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 151.97/21.60 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 151.97/21.60 (aElement0(v2) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & ( ~ (v4 = 0) % 151.97/21.60 | ~ (v3 = 0) | v5 = 0))) % 151.97/21.60 % 151.97/21.60 (m__) % 151.97/21.60 $i(xc) & $i(xb) & $i(xa) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 151.97/21.60 int] : ( ~ (v3 = 0) & slsdtgt0(xb) = v1 & slsdtgt0(xa) = v0 & sdtpldt1(v0, % 151.97/21.60 v1) = v2 & aElementOf0(xc, v2) = v3 & $i(v2) & $i(v1) & $i(v0) & ! [v4: % 151.97/21.60 $i] : ! [v5: int] : ! [v6: $i] : (v5 = 0 | ~ (aElementOf0(v4, v1) = v5) % 151.97/21.60 | ~ (sdtasdt0(xb, v6) = v4) | ~ $i(v6) | ~ $i(v4) | ? [v7: int] : ( ~ % 151.97/21.60 (v7 = 0) & aElement0(v6) = v7)) & ! [v4: $i] : ! [v5: int] : ! [v6: % 151.97/21.60 $i] : (v5 = 0 | ~ (aElementOf0(v4, v1) = v5) | ~ (aElement0(v6) = 0) | % 151.97/21.60 ~ $i(v6) | ~ $i(v4) | ? [v7: $i] : ( ~ (v7 = v4) & sdtasdt0(xb, v6) = v7 % 151.97/21.60 & $i(v7))) & ! [v4: $i] : ! [v5: int] : ! [v6: $i] : (v5 = 0 | ~ % 151.97/21.60 (aElementOf0(v4, v0) = v5) | ~ (sdtasdt0(xa, v6) = v4) | ~ $i(v6) | ~ % 151.97/21.60 $i(v4) | ? [v7: int] : ( ~ (v7 = 0) & aElement0(v6) = v7)) & ! [v4: $i] % 151.97/21.60 : ! [v5: int] : ! [v6: $i] : (v5 = 0 | ~ (aElementOf0(v4, v0) = v5) | ~ % 151.97/21.60 (aElement0(v6) = 0) | ~ $i(v6) | ~ $i(v4) | ? [v7: $i] : ( ~ (v7 = v4) % 151.97/21.60 & sdtasdt0(xa, v6) = v7 & $i(v7))) & ! [v4: $i] : ! [v5: $i] : ( ~ % 151.97/21.60 (sdtpldt0(v4, v5) = xc) | ~ $i(v5) | ~ $i(v4) | ? [v6: any] : ? [v7: % 151.97/21.60 any] : (aElementOf0(v5, v1) = v7 & aElementOf0(v4, v0) = v6 & ( ~ (v7 = % 151.97/21.60 0) | ~ (v6 = 0)))) & ! [v4: $i] : ( ~ (aElementOf0(v4, v1) = 0) | % 151.97/21.60 ~ $i(v4) | ? [v5: $i] : (sdtasdt0(xb, v5) = v4 & aElement0(v5) = 0 & % 151.97/21.60 $i(v5))) & ! [v4: $i] : ( ~ (aElementOf0(v4, v0) = 0) | ~ $i(v4) | ? % 151.97/21.60 [v5: $i] : (sdtasdt0(xa, v5) = v4 & aElement0(v5) = 0 & $i(v5)))) % 151.97/21.60 % 151.97/21.60 (m__2091) % 151.97/21.60 aElement0(xb) = 0 & aElement0(xa) = 0 & $i(xb) & $i(xa) % 151.97/21.60 % 151.97/21.60 (m__2129) % 152.41/21.63 $i(xc) & $i(xb) & $i(xa) & ? [v0: $i] : ? [v1: $i] : (aGcdOfAnd0(xc, xa, xb) % 152.41/21.63 = 0 & aDivisorOf0(xc, xb) = 0 & aDivisorOf0(xc, xa) = 0 & doDivides0(xc, xb) % 152.41/21.63 = 0 & doDivides0(xc, xa) = 0 & sdtasdt0(xc, v1) = xa & sdtasdt0(xc, v0) = xb % 152.41/21.63 & aElement0(v1) = 0 & aElement0(v0) = 0 & aElement0(xc) = 0 & $i(v1) & % 152.41/21.63 $i(v0) & ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (doDivides0(v2, xc) = v3) % 152.41/21.63 | ~ $i(v2) | ? [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: any] : % 152.41/21.63 ? [v8: any] : (aDivisorOf0(v2, xb) = v8 & aDivisorOf0(v2, xa) = v6 & % 152.41/21.63 doDivides0(v2, xb) = v7 & doDivides0(v2, xa) = v5 & aElement0(v2) = v4 & % 152.41/21.63 (( ~ (v8 = 0) & ~ (v7 = 0) & ! [v9: $i] : ( ~ (sdtasdt0(v2, v9) = xb) % 152.41/21.63 | ~ $i(v9) | ? [v10: int] : ( ~ (v10 = 0) & aElement0(v9) = % 152.41/21.63 v10)) & ! [v9: $i] : ( ~ (aElement0(v9) = 0) | ~ $i(v9) | ? % 152.41/21.63 [v10: $i] : ( ~ (v10 = xb) & sdtasdt0(v2, v9) = v10 & $i(v10)))) | % 152.41/21.63 ( ~ (v6 = 0) & ( ~ (v4 = 0) | ( ~ (v5 = 0) & ! [v9: $i] : ( ~ % 152.41/21.63 (sdtasdt0(v2, v9) = xa) | ~ $i(v9) | ? [v10: int] : ( ~ (v10 % 152.41/21.63 = 0) & aElement0(v9) = v10)) & ! [v9: $i] : ( ~ % 152.41/21.63 (aElement0(v9) = 0) | ~ $i(v9) | ? [v10: $i] : ( ~ (v10 = % 152.41/21.63 xa) & sdtasdt0(v2, v9) = v10 & $i(v10))))))))) & ! [v2: % 152.41/21.63 $i] : ! [v3: any] : ( ~ (aDivisorOf0(v2, xb) = v3) | ~ $i(v2) | ? [v4: % 152.41/21.63 any] : ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : ? % 152.41/21.63 [v9: $i] : ? [v10: int] : ? [v11: $i] : (aDivisorOf0(v2, xa) = v6 & % 152.41/21.63 doDivides0(v2, xc) = v8 & doDivides0(v2, xb) = v7 & doDivides0(v2, xa) = % 152.41/21.63 v5 & aElement0(v2) = v4 & $i(v9) & ((v11 = xc & v10 = 0 & v8 = 0 & % 152.41/21.63 sdtasdt0(v2, v9) = xc & aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v3 = % 152.41/21.63 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? % 152.41/21.63 [v13: int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! [v12: $i] % 152.41/21.63 : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = % 152.41/21.63 xb) & sdtasdt0(v2, v12) = v13 & $i(v13)))) | ( ~ (v6 = 0) & ( % 152.41/21.63 ~ (v4 = 0) | ( ~ (v5 = 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) % 152.41/21.63 = xa) | ~ $i(v12) | ? [v13: int] : ( ~ (v13 = 0) & % 152.41/21.63 aElement0(v12) = v13)) & ! [v12: $i] : ( ~ (aElement0(v12) % 152.41/21.63 = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = xa) & % 152.41/21.63 sdtasdt0(v2, v12) = v13 & $i(v13))))))))) & ! [v2: $i] : ! % 152.41/21.63 [v3: any] : ( ~ (aDivisorOf0(v2, xa) = v3) | ~ $i(v2) | ? [v4: any] : ? % 152.41/21.63 [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? % 152.41/21.63 [v10: int] : ? [v11: $i] : (aDivisorOf0(v2, xb) = v7 & doDivides0(v2, xc) % 152.41/21.63 = v8 & doDivides0(v2, xb) = v6 & doDivides0(v2, xa) = v5 & aElement0(v2) % 152.41/21.63 = v4 & $i(v9) & ((v11 = xc & v10 = 0 & v8 = 0 & sdtasdt0(v2, v9) = xc & % 152.41/21.63 aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v6 = 0) & ! [v12: $i] : ( ~ % 152.41/21.63 (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? [v13: int] : ( ~ (v13 = % 152.41/21.63 0) & aElement0(v12) = v13)) & ! [v12: $i] : ( ~ % 152.41/21.63 (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = xb) % 152.41/21.63 & sdtasdt0(v2, v12) = v13 & $i(v13)))) | ( ~ (v3 = 0) & ( ~ (v4 % 152.41/21.63 = 0) | ( ~ (v5 = 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) = % 152.41/21.63 xa) | ~ $i(v12) | ? [v13: int] : ( ~ (v13 = 0) & % 152.41/21.63 aElement0(v12) = v13)) & ! [v12: $i] : ( ~ (aElement0(v12) % 152.41/21.63 = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = xa) & % 152.41/21.63 sdtasdt0(v2, v12) = v13 & $i(v13))))))))) & ! [v2: $i] : ! % 152.41/21.63 [v3: MultipleValueBool] : ( ~ (doDivides0(v2, xc) = v3) | ~ $i(v2) | ? % 152.41/21.63 [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : ? % 152.41/21.63 [v9: $i] : ? [v10: int] : ? [v11: $i] : ($i(v9) & ((v11 = xc & v10 = 0 & % 152.41/21.63 sdtasdt0(v2, v9) = xc & aElement0(v9) = 0) | (aDivisorOf0(v2, xb) = % 152.41/21.63 v8 & aDivisorOf0(v2, xa) = v6 & doDivides0(v2, xb) = v7 & % 152.41/21.63 doDivides0(v2, xa) = v5 & aElement0(v2) = v4 & (( ~ (v8 = 0) & ~ % 152.41/21.63 (v7 = 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ % 152.41/21.63 $i(v12) | ? [v13: int] : ( ~ (v13 = 0) & aElement0(v12) = % 152.41/21.63 v13)) & ! [v12: $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) % 152.41/21.63 | ? [v13: $i] : ( ~ (v13 = xb) & sdtasdt0(v2, v12) = v13 & % 152.41/21.63 $i(v13)))) | ( ~ (v6 = 0) & ( ~ (v4 = 0) | ( ~ (v5 = 0) & ! % 152.41/21.63 [v12: $i] : ( ~ (sdtasdt0(v2, v12) = xa) | ~ $i(v12) | ? % 152.41/21.63 [v13: int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! % 152.41/21.63 [v12: $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: % 152.41/21.63 $i] : ( ~ (v13 = xa) & sdtasdt0(v2, v12) = v13 & % 152.41/21.63 $i(v13))))))))))) & ! [v2: $i] : ! [v3: any] : ( ~ % 152.41/21.63 (doDivides0(v2, xb) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: any] : ? % 152.41/21.63 [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? [v10: int] : ? % 152.41/21.63 [v11: $i] : (aDivisorOf0(v2, xb) = v7 & aDivisorOf0(v2, xa) = v6 & % 152.41/21.63 doDivides0(v2, xc) = v8 & doDivides0(v2, xa) = v5 & aElement0(v2) = v4 & % 152.41/21.63 $i(v9) & ((v11 = xc & v10 = 0 & v8 = 0 & sdtasdt0(v2, v9) = xc & % 152.41/21.63 aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v3 = 0) & ! [v12: $i] : ( ~ % 152.41/21.63 (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? [v13: int] : ( ~ (v13 = % 152.41/21.63 0) & aElement0(v12) = v13)) & ! [v12: $i] : ( ~ % 152.41/21.63 (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = xb) % 152.41/21.63 & sdtasdt0(v2, v12) = v13 & $i(v13)))) | ( ~ (v6 = 0) & ( ~ (v4 % 152.41/21.63 = 0) | ( ~ (v5 = 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) = % 152.41/21.63 xa) | ~ $i(v12) | ? [v13: int] : ( ~ (v13 = 0) & % 152.41/21.63 aElement0(v12) = v13)) & ! [v12: $i] : ( ~ (aElement0(v12) % 152.41/21.63 = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = xa) & % 152.41/21.63 sdtasdt0(v2, v12) = v13 & $i(v13))))))))) & ! [v2: $i] : ! % 152.41/21.63 [v3: any] : ( ~ (doDivides0(v2, xa) = v3) | ~ $i(v2) | ? [v4: any] : ? % 152.41/21.63 [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? % 152.41/21.63 [v10: int] : ? [v11: $i] : (aDivisorOf0(v2, xb) = v7 & aDivisorOf0(v2, % 152.41/21.63 xa) = v5 & doDivides0(v2, xc) = v8 & doDivides0(v2, xb) = v6 & % 152.41/21.63 aElement0(v2) = v4 & $i(v9) & ((v11 = xc & v10 = 0 & v8 = 0 & % 152.41/21.63 sdtasdt0(v2, v9) = xc & aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v6 = % 152.41/21.63 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? % 152.41/21.63 [v13: int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! [v12: $i] % 152.41/21.63 : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = % 152.41/21.63 xb) & sdtasdt0(v2, v12) = v13 & $i(v13)))) | ( ~ (v5 = 0) & ( % 152.41/21.63 ~ (v4 = 0) | ( ~ (v3 = 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) % 152.41/21.63 = xa) | ~ $i(v12) | ? [v13: int] : ( ~ (v13 = 0) & % 152.41/21.63 aElement0(v12) = v13)) & ! [v12: $i] : ( ~ (aElement0(v12) % 152.41/21.63 = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = xa) & % 152.41/21.63 sdtasdt0(v2, v12) = v13 & $i(v13))))))))) & ! [v2: $i] : ! % 152.41/21.63 [v3: any] : ( ~ (aElement0(v2) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: % 152.41/21.63 any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? % 152.41/21.63 [v10: int] : ? [v11: $i] : (aDivisorOf0(v2, xb) = v7 & aDivisorOf0(v2, % 152.41/21.63 xa) = v5 & doDivides0(v2, xc) = v8 & doDivides0(v2, xb) = v6 & % 152.41/21.63 doDivides0(v2, xa) = v4 & $i(v9) & ((v11 = xc & v10 = 0 & v8 = 0 & % 152.41/21.63 sdtasdt0(v2, v9) = xc & aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v6 = % 152.41/21.63 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? % 152.41/21.63 [v13: int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! [v12: $i] % 152.41/21.63 : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = % 152.41/21.63 xb) & sdtasdt0(v2, v12) = v13 & $i(v13)))) | ( ~ (v5 = 0) & ( % 152.41/21.63 ~ (v3 = 0) | ( ~ (v4 = 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) % 152.41/21.63 = xa) | ~ $i(v12) | ? [v13: int] : ( ~ (v13 = 0) & % 152.41/21.63 aElement0(v12) = v13)) & ! [v12: $i] : ( ~ (aElement0(v12) % 152.41/21.63 = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = xa) & % 152.41/21.63 sdtasdt0(v2, v12) = v13 & $i(v13)))))))))) % 152.41/21.63 % 152.41/21.63 (m__2174) % 152.41/21.64 $i(xI) & $i(xb) & $i(xa) & ? [v0: $i] : ? [v1: $i] : (slsdtgt0(xb) = v1 & % 152.41/21.64 slsdtgt0(xa) = v0 & aIdeal0(xI) = 0 & sdtpldt1(v0, v1) = xI & aSet0(xI) = 0 % 152.41/21.64 & $i(v1) & $i(v0) & ! [v2: $i] : ! [v3: int] : ! [v4: $i] : ! [v5: $i] : % 152.41/21.64 (v3 = 0 | ~ (aElementOf0(v2, xI) = v3) | ~ (sdtpldt0(v4, v5) = v2) | ~ % 152.41/21.64 $i(v5) | ~ $i(v4) | ~ $i(v2) | ? [v6: any] : ? [v7: any] : % 152.41/21.64 (aElementOf0(v5, v1) = v7 & aElementOf0(v4, v0) = v6 & ( ~ (v7 = 0) | ~ % 152.41/21.64 (v6 = 0)))) & ! [v2: $i] : ! [v3: int] : ! [v4: $i] : (v3 = 0 | ~ % 152.41/21.64 (aElementOf0(v2, v1) = v3) | ~ (sdtasdt0(xb, v4) = v2) | ~ $i(v4) | ~ % 152.41/21.64 $i(v2) | ? [v5: int] : ( ~ (v5 = 0) & aElement0(v4) = v5)) & ! [v2: $i] % 152.41/21.64 : ! [v3: int] : ! [v4: $i] : (v3 = 0 | ~ (aElementOf0(v2, v1) = v3) | ~ % 152.41/21.64 (aElement0(v4) = 0) | ~ $i(v4) | ~ $i(v2) | ? [v5: $i] : ( ~ (v5 = v2) % 152.41/21.64 & sdtasdt0(xb, v4) = v5 & $i(v5))) & ! [v2: $i] : ! [v3: int] : ! % 152.41/21.64 [v4: $i] : (v3 = 0 | ~ (aElementOf0(v2, v0) = v3) | ~ (sdtasdt0(xa, v4) = % 152.41/21.64 v2) | ~ $i(v4) | ~ $i(v2) | ? [v5: int] : ( ~ (v5 = 0) & % 152.41/21.64 aElement0(v4) = v5)) & ! [v2: $i] : ! [v3: int] : ! [v4: $i] : (v3 = % 152.41/21.64 0 | ~ (aElementOf0(v2, v0) = v3) | ~ (aElement0(v4) = 0) | ~ $i(v4) | % 152.41/21.64 ~ $i(v2) | ? [v5: $i] : ( ~ (v5 = v2) & sdtasdt0(xa, v4) = v5 & $i(v5))) % 152.41/21.64 & ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (aElementOf0(v2, xI) = 0) | % 152.41/21.64 ~ (sdtasdt0(v3, v2) = v4) | ~ $i(v3) | ~ $i(v2) | ? [v5: any] : ? [v6: % 152.41/21.64 any] : (aElementOf0(v4, xI) = v6 & aElement0(v3) = v5 & ( ~ (v5 = 0) | % 152.41/21.64 v6 = 0))) & ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 152.41/21.64 (aElementOf0(v2, xI) = 0) | ~ (sdtpldt0(v2, v3) = v4) | ~ $i(v3) | ~ % 152.41/21.64 $i(v2) | ? [v5: any] : ? [v6: any] : (aElementOf0(v4, xI) = v6 & % 152.41/21.64 aElementOf0(v3, xI) = v5 & ( ~ (v5 = 0) | v6 = 0))) & ! [v2: $i] : ! % 152.41/21.64 [v3: $i] : ( ~ (aElementOf0(v3, xI) = 0) | ~ (aElementOf0(v2, xI) = 0) | ~ % 152.41/21.64 $i(v3) | ~ $i(v2) | ? [v4: $i] : (aElementOf0(v4, xI) = 0 & sdtpldt0(v2, % 152.41/21.64 v3) = v4 & $i(v4))) & ! [v2: $i] : ! [v3: $i] : ( ~ (aElementOf0(v2, % 152.41/21.64 xI) = 0) | ~ (aElement0(v3) = 0) | ~ $i(v3) | ~ $i(v2) | ? [v4: % 152.41/21.64 $i] : (aElementOf0(v4, xI) = 0 & sdtasdt0(v3, v2) = v4 & $i(v4))) & ! % 152.41/21.64 [v2: $i] : ( ~ (aElementOf0(v2, v1) = 0) | ~ $i(v2) | ? [v3: $i] : % 152.41/21.64 (sdtasdt0(xb, v3) = v2 & aElement0(v3) = 0 & $i(v3))) & ! [v2: $i] : ( ~ % 152.41/21.64 (aElementOf0(v2, v0) = 0) | ~ $i(v2) | ? [v3: $i] : (sdtasdt0(xa, v3) = % 152.41/21.64 v2 & aElement0(v3) = 0 & $i(v3))) & ! [v2: $i] : ( ~ (aElementOf0(v2, % 152.41/21.64 xI) = 0) | ~ $i(v2) | ? [v3: $i] : ? [v4: $i] : (aElementOf0(v4, % 152.41/21.64 v1) = 0 & aElementOf0(v3, v0) = 0 & sdtpldt0(v3, v4) = v2 & $i(v4) & % 152.41/21.64 $i(v3)))) % 152.41/21.64 % 152.41/21.64 (m__2203) % 152.41/21.64 $i(xb) & $i(xa) & $i(sz00) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 152.41/21.64 $i] : ? [v4: $i] : ? [v5: $i] : (slsdtgt0(xb) = v1 & slsdtgt0(xa) = v0 & % 152.41/21.64 aElementOf0(xb, v1) = 0 & aElementOf0(xa, v0) = 0 & aElementOf0(sz00, v1) = % 152.41/21.64 0 & aElementOf0(sz00, v0) = 0 & sdtasdt0(xb, v3) = sz00 & sdtasdt0(xb, v2) = % 152.41/21.64 xb & sdtasdt0(xa, v5) = sz00 & sdtasdt0(xa, v4) = xa & aElement0(v5) = 0 & % 152.41/21.64 aElement0(v4) = 0 & aElement0(v3) = 0 & aElement0(v2) = 0 & $i(v5) & $i(v4) % 152.41/21.64 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 152.41/21.64 % 152.41/21.64 (m__2228) % 152.41/21.65 $i(xb) & $i(xa) & $i(sz00) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 152.41/21.65 $i] : ? [v4: $i] : ? [v5: $i] : ( ~ (v3 = sz00) & slsdtgt0(xb) = v1 & % 152.41/21.65 slsdtgt0(xa) = v0 & sdtpldt1(v0, v1) = v2 & aElementOf0(v5, v1) = 0 & % 152.41/21.65 aElementOf0(v4, v0) = 0 & aElementOf0(v3, v2) = 0 & sdtpldt0(v4, v5) = v3 & % 152.41/21.65 $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ! [v6: $i] : ! [v7: % 152.41/21.65 int] : ! [v8: $i] : (v7 = 0 | ~ (aElementOf0(v6, v1) = v7) | ~ % 152.41/21.65 (sdtasdt0(xb, v8) = v6) | ~ $i(v8) | ~ $i(v6) | ? [v9: int] : ( ~ (v9 = % 152.41/21.65 0) & aElement0(v8) = v9)) & ! [v6: $i] : ! [v7: int] : ! [v8: $i] : % 152.41/21.65 (v7 = 0 | ~ (aElementOf0(v6, v1) = v7) | ~ (aElement0(v8) = 0) | ~ $i(v8) % 152.41/21.65 | ~ $i(v6) | ? [v9: $i] : ( ~ (v9 = v6) & sdtasdt0(xb, v8) = v9 & % 152.41/21.65 $i(v9))) & ! [v6: $i] : ! [v7: int] : ! [v8: $i] : (v7 = 0 | ~ % 152.41/21.65 (aElementOf0(v6, v0) = v7) | ~ (sdtasdt0(xa, v8) = v6) | ~ $i(v8) | ~ % 152.41/21.65 $i(v6) | ? [v9: int] : ( ~ (v9 = 0) & aElement0(v8) = v9)) & ! [v6: $i] % 152.41/21.65 : ! [v7: int] : ! [v8: $i] : (v7 = 0 | ~ (aElementOf0(v6, v0) = v7) | ~ % 152.41/21.65 (aElement0(v8) = 0) | ~ $i(v8) | ~ $i(v6) | ? [v9: $i] : ( ~ (v9 = v6) % 152.41/21.65 & sdtasdt0(xa, v8) = v9 & $i(v9))) & ! [v6: $i] : ( ~ (aElementOf0(v6, % 152.41/21.65 v1) = 0) | ~ $i(v6) | ? [v7: $i] : (sdtasdt0(xb, v7) = v6 & % 152.41/21.65 aElement0(v7) = 0 & $i(v7))) & ! [v6: $i] : ( ~ (aElementOf0(v6, v0) = % 152.41/21.65 0) | ~ $i(v6) | ? [v7: $i] : (sdtasdt0(xa, v7) = v6 & aElement0(v7) = % 152.41/21.65 0 & $i(v7)))) % 152.41/21.65 % 152.41/21.65 (m__2273) % 152.41/21.65 $i(xu) & $i(xI) & $i(xb) & $i(xa) & $i(sz00) & ? [v0: $i] : ? [v1: $i] : ? % 152.41/21.65 [v2: $i] : ? [v3: $i] : ? [v4: $i] : ( ~ (xu = sz00) & slsdtgt0(xb) = v1 & % 152.41/21.65 slsdtgt0(xa) = v0 & sbrdtbr0(xu) = v2 & aElementOf0(v4, v1) = 0 & % 152.41/21.65 aElementOf0(v3, v0) = 0 & aElementOf0(xu, xI) = 0 & sdtpldt0(v3, v4) = xu & % 152.41/21.65 $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ! [v5: $i] : ! [v6: % 152.41/21.65 MultipleValueBool] : ! [v7: $i] : ! [v8: $i] : (v5 = sz00 | ~ % 152.41/21.65 (aElementOf0(v5, xI) = v6) | ~ (sdtpldt0(v7, v8) = v5) | ~ $i(v8) | ~ % 152.41/21.65 $i(v7) | ~ $i(v5) | ? [v9: any] : ? [v10: int] : (( ~ (v10 = 0) & % 152.41/21.65 iLess0(v9, v2) = v10 & sbrdtbr0(v5) = v9 & $i(v9)) | (aElementOf0(v8, % 152.41/21.65 v1) = v10 & aElementOf0(v7, v0) = v9 & ( ~ (v10 = 0) | ~ (v9 = % 152.41/21.65 0))))) & ! [v5: $i] : ! [v6: $i] : (v5 = sz00 | ~ (sbrdtbr0(v5) % 152.41/21.65 = v6) | ~ $i(v5) | ? [v7: any] : ? [v8: any] : (iLess0(v6, v2) = v8 & % 152.41/21.65 aElementOf0(v5, xI) = v7 & ( ~ (v8 = 0) | ( ~ (v7 = 0) & ! [v9: $i] : % 152.41/21.65 ! [v10: $i] : ( ~ (sdtpldt0(v9, v10) = v5) | ~ $i(v10) | ~ $i(v9) % 152.41/21.65 | ? [v11: any] : ? [v12: any] : (aElementOf0(v10, v1) = v12 & % 152.41/21.65 aElementOf0(v9, v0) = v11 & ( ~ (v12 = 0) | ~ (v11 = 0)))))))) % 152.41/21.65 & ! [v5: $i] : (v5 = sz00 | ~ (aElementOf0(v5, xI) = 0) | ~ $i(v5) | ? % 152.41/21.65 [v6: $i] : ? [v7: int] : ( ~ (v7 = 0) & iLess0(v6, v2) = v7 & % 152.41/21.65 sbrdtbr0(v5) = v6 & $i(v6)))) % 152.41/21.65 % 152.41/21.65 (m__2373) % 152.41/21.65 $i(xu) & $i(xb) & $i(xa) & ? [v0: $i] : ? [v1: $i] : (aDivisorOf0(xu, xb) = % 152.41/21.65 0 & aDivisorOf0(xu, xa) = 0 & doDivides0(xu, xb) = 0 & doDivides0(xu, xa) = % 152.41/21.65 0 & sdtasdt0(xu, v1) = xa & sdtasdt0(xu, v0) = xb & aElement0(v1) = 0 & % 152.41/21.65 aElement0(v0) = 0 & $i(v1) & $i(v0)) % 152.41/21.65 % 152.41/21.65 (m__2744) % 152.41/21.65 $i(xu) & $i(xc) & ? [v0: $i] : (sdtasdt0(xu, v0) = xc & aElement0(v0) = 0 & % 152.41/21.65 $i(v0)) % 152.41/21.65 % 152.41/21.65 (function-axioms) % 152.41/21.66 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 152.41/21.66 [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (aGcdOfAnd0(v4, v3, v2) = v1) | ~ % 152.41/21.66 (aGcdOfAnd0(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 152.41/21.66 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 152.41/21.66 (sdteqdtlpzmzozddtrp0(v4, v3, v2) = v1) | ~ (sdteqdtlpzmzozddtrp0(v4, v3, % 152.41/21.66 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 152.41/21.66 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (misRelativelyPrime0(v3, v2) = v1) | % 152.41/21.66 ~ (misRelativelyPrime0(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 152.41/21.66 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 152.41/21.66 (aDivisorOf0(v3, v2) = v1) | ~ (aDivisorOf0(v3, v2) = v0)) & ! [v0: % 152.41/21.66 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 152.41/21.66 : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ (doDivides0(v3, v2) = v0)) & ! % 152.41/21.66 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 152.41/21.66 $i] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) & ! % 152.41/21.66 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 152.41/21.66 (sdtasasdt0(v3, v2) = v1) | ~ (sdtasasdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 152.41/21.66 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtpldt1(v3, v2) = v1) | % 152.41/21.66 ~ (sdtpldt1(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 152.41/21.66 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 152.41/21.66 (aElementOf0(v3, v2) = v1) | ~ (aElementOf0(v3, v2) = v0)) & ! [v0: $i] : % 152.41/21.66 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) % 152.41/21.66 | ~ (sdtasdt0(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 152.41/21.66 [v3: $i] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 152.41/21.66 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (slsdtgt0(v2) = v1) % 152.41/21.66 | ~ (slsdtgt0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = % 152.41/21.66 v0 | ~ (sbrdtbr0(v2) = v1) | ~ (sbrdtbr0(v2) = v0)) & ! [v0: % 152.41/21.66 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 152.41/21.66 ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = v0)) & ! [v0: % 152.41/21.66 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 152.41/21.66 ~ (aIdeal0(v2) = v1) | ~ (aIdeal0(v2) = v0)) & ! [v0: MultipleValueBool] : % 152.41/21.66 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aSet0(v2) = v1) | ~ % 152.41/21.66 (aSet0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 152.41/21.66 (smndt0(v2) = v1) | ~ (smndt0(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 152.41/21.66 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aElement0(v2) = v1) | % 152.41/21.66 ~ (aElement0(v2) = v0)) % 152.41/21.66 % 152.41/21.66 Further assumptions not needed in the proof: % 152.41/21.66 -------------------------------------------- % 152.41/21.66 mAddAsso, mAddComm, mAddInvr, mAddZero, mCancel, mChineseRemainder, mDefDiv, % 152.41/21.66 mDefGCD, mDefMod, mDefPrIdeal, mDefRel, mDefSInt, mDefSSum, mDivision, mEOfElem, % 152.41/21.66 mElmSort, mIdeInt, mIdeSum, mMulMnOne, mMulUnit, mMulZero, mNatLess, mNatSort, % 152.41/21.66 mPrIdeal, mSetEq, mSetSort, mSortsC, mSortsC_01, mSortsU, mUnNeZr, m__2110 % 152.41/21.66 % 152.41/21.66 Those formulas are unsatisfiable: % 152.41/21.66 --------------------------------- % 152.41/21.66 % 152.41/21.66 Begin of proof % 152.41/21.66 | % 152.41/21.66 | ALPHA: (mMulComm) implies: % 152.41/21.66 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | % 152.41/21.66 | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 152.41/21.66 | (sdtasdt0(v1, v0) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & % 152.41/21.66 | $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 152.41/21.66 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v1, v0) = v2) | % 152.41/21.66 | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 152.41/21.66 | (sdtasdt0(v0, v1) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & % 152.41/21.66 | $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 152.41/21.66 | % 152.41/21.66 | ALPHA: (mMulAsso) implies: % 152.41/21.67 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 152.41/21.67 | ~ (sdtasdt0(v3, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | % 152.41/21.67 | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : % 152.41/21.67 | ? [v8: $i] : ? [v9: $i] : (sdtasdt0(v1, v2) = v8 & sdtasdt0(v0, v8) % 152.41/21.67 | = v9 & aElement0(v2) = v7 & aElement0(v1) = v6 & aElement0(v0) = v5 % 152.41/21.67 | & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v9 = % 152.41/21.67 | v4))) % 152.41/21.67 | % 152.41/21.67 | ALPHA: (mAMDistr) implies: % 152.41/21.67 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 152.41/21.67 | ~ (sdtasdt0(v3, v0) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ $i(v2) | % 152.41/21.67 | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : % 152.41/21.67 | ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] % 152.41/21.67 | : ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v2, v0) = v13 & % 152.41/21.67 | sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v3) = v8 & sdtasdt0(v0, v2) = % 152.41/21.67 | v10 & sdtasdt0(v0, v1) = v9 & sdtpldt0(v12, v13) = v14 & % 152.41/21.67 | sdtpldt0(v9, v10) = v11 & aElement0(v2) = v7 & aElement0(v1) = v6 & % 152.41/21.67 | aElement0(v0) = v5 & $i(v14) & $i(v13) & $i(v12) & $i(v11) & % 152.41/21.67 | $i(v10) & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = % 152.41/21.67 | 0) | (v14 = v4 & v11 = v8)))) % 152.41/21.67 | % 152.41/21.67 | ALPHA: (mDefIdeal) implies: % 152.41/21.67 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (aIdeal0(v0) = 0) | ~ % 152.41/21.67 | (aElementOf0(v1, v0) = 0) | ~ (aElement0(v2) = 0) | ~ $i(v2) | ~ % 152.41/21.67 | $i(v1) | ~ $i(v0) | ? [v3: $i] : (aElementOf0(v3, v0) = 0 & % 152.41/21.67 | sdtasdt0(v2, v1) = v3 & $i(v3))) % 152.41/21.67 | % 152.41/21.67 | ALPHA: (mEucSort) implies: % 152.41/21.67 | (6) ! [v0: $i] : ! [v1: $i] : (v0 = sz00 | ~ (sbrdtbr0(v0) = v1) | ~ % 152.41/21.67 | $i(v0) | ? [v2: any] : ? [v3: any] : (aNaturalNumber0(v1) = v3 & % 152.41/21.67 | aElement0(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 152.41/21.67 | % 152.41/21.67 | ALPHA: (mDefDvs) implies: % 152.41/21.67 | (7) ! [v0: $i] : ! [v1: $i] : ( ~ (doDivides0(v1, v0) = 0) | ~ % 152.41/21.67 | (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: any] : ? [v3: % 152.41/21.67 | any] : (aDivisorOf0(v1, v0) = v3 & aElement0(v1) = v2 & ( ~ (v2 = % 152.41/21.67 | 0) | v3 = 0))) % 152.41/21.67 | (8) ! [v0: $i] : ! [v1: $i] : ( ~ (aDivisorOf0(v1, v0) = 0) | ~ % 152.41/21.67 | (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | (doDivides0(v1, v0) = 0 % 152.41/21.67 | & aElement0(v1) = 0)) % 152.41/21.67 | (9) ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (doDivides0(v1, v0) = % 152.41/21.67 | v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] % 152.41/21.67 | : ? [v4: any] : (aDivisorOf0(v1, v0) = v3 & aElement0(v1) = v4 & ( ~ % 152.41/21.67 | (v3 = 0) | (v4 = 0 & v2 = 0)))) % 152.41/21.67 | % 152.41/21.67 | ALPHA: (m__2091) implies: % 152.41/21.67 | (10) aElement0(xa) = 0 % 152.41/21.67 | (11) aElement0(xb) = 0 % 152.41/21.67 | % 152.41/21.67 | ALPHA: (m__2129) implies: % 152.79/21.69 | (12) ? [v0: $i] : ? [v1: $i] : (aGcdOfAnd0(xc, xa, xb) = 0 & % 152.79/21.69 | aDivisorOf0(xc, xb) = 0 & aDivisorOf0(xc, xa) = 0 & doDivides0(xc, % 152.79/21.69 | xb) = 0 & doDivides0(xc, xa) = 0 & sdtasdt0(xc, v1) = xa & % 152.79/21.69 | sdtasdt0(xc, v0) = xb & aElement0(v1) = 0 & aElement0(v0) = 0 & % 152.79/21.69 | aElement0(xc) = 0 & $i(v1) & $i(v0) & ! [v2: $i] : ! [v3: int] : % 152.79/21.69 | (v3 = 0 | ~ (doDivides0(v2, xc) = v3) | ~ $i(v2) | ? [v4: any] : % 152.79/21.69 | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : % 152.79/21.69 | (aDivisorOf0(v2, xb) = v8 & aDivisorOf0(v2, xa) = v6 & % 152.79/21.69 | doDivides0(v2, xb) = v7 & doDivides0(v2, xa) = v5 & % 152.79/21.69 | aElement0(v2) = v4 & (( ~ (v8 = 0) & ~ (v7 = 0) & ! [v9: $i] : % 152.79/21.69 | ( ~ (sdtasdt0(v2, v9) = xb) | ~ $i(v9) | ? [v10: int] : ( % 152.79/21.69 | ~ (v10 = 0) & aElement0(v9) = v10)) & ! [v9: $i] : ( ~ % 152.79/21.69 | (aElement0(v9) = 0) | ~ $i(v9) | ? [v10: $i] : ( ~ (v10 % 152.79/21.69 | = xb) & sdtasdt0(v2, v9) = v10 & $i(v10)))) | ( ~ (v6 % 152.79/21.69 | = 0) & ( ~ (v4 = 0) | ( ~ (v5 = 0) & ! [v9: $i] : ( ~ % 152.79/21.69 | (sdtasdt0(v2, v9) = xa) | ~ $i(v9) | ? [v10: int] : % 152.79/21.69 | ( ~ (v10 = 0) & aElement0(v9) = v10)) & ! [v9: $i] : % 152.79/21.69 | ( ~ (aElement0(v9) = 0) | ~ $i(v9) | ? [v10: $i] : ( ~ % 152.79/21.69 | (v10 = xa) & sdtasdt0(v2, v9) = v10 & % 152.79/21.69 | $i(v10))))))))) & ! [v2: $i] : ! [v3: any] : ( ~ % 152.79/21.69 | (aDivisorOf0(v2, xb) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: % 152.79/21.69 | any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] % 152.79/21.69 | : ? [v10: int] : ? [v11: $i] : (aDivisorOf0(v2, xa) = v6 & % 152.79/21.69 | doDivides0(v2, xc) = v8 & doDivides0(v2, xb) = v7 & % 152.79/21.69 | doDivides0(v2, xa) = v5 & aElement0(v2) = v4 & $i(v9) & ((v11 = % 152.79/21.69 | xc & v10 = 0 & v8 = 0 & sdtasdt0(v2, v9) = xc & % 152.79/21.69 | aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v3 = 0) & ! [v12: % 152.79/21.69 | $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? [v13: % 152.79/21.69 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! [v12: % 152.79/21.69 | $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] % 152.79/21.69 | : ( ~ (v13 = xb) & sdtasdt0(v2, v12) = v13 & $i(v13)))) | % 152.79/21.69 | ( ~ (v6 = 0) & ( ~ (v4 = 0) | ( ~ (v5 = 0) & ! [v12: $i] : ( % 152.79/21.69 | ~ (sdtasdt0(v2, v12) = xa) | ~ $i(v12) | ? [v13: % 152.79/21.69 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! % 152.79/21.69 | [v12: $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? % 152.79/21.69 | [v13: $i] : ( ~ (v13 = xa) & sdtasdt0(v2, v12) = v13 & % 152.79/21.69 | $i(v13))))))))) & ! [v2: $i] : ! [v3: any] : ( ~ % 152.79/21.69 | (aDivisorOf0(v2, xa) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: % 152.79/21.69 | any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] % 152.79/21.69 | : ? [v10: int] : ? [v11: $i] : (aDivisorOf0(v2, xb) = v7 & % 152.79/21.69 | doDivides0(v2, xc) = v8 & doDivides0(v2, xb) = v6 & % 152.79/21.69 | doDivides0(v2, xa) = v5 & aElement0(v2) = v4 & $i(v9) & ((v11 = % 152.79/21.69 | xc & v10 = 0 & v8 = 0 & sdtasdt0(v2, v9) = xc & % 152.79/21.69 | aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v6 = 0) & ! [v12: % 152.79/21.69 | $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? [v13: % 152.79/21.69 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! [v12: % 152.79/21.69 | $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] % 152.79/21.69 | : ( ~ (v13 = xb) & sdtasdt0(v2, v12) = v13 & $i(v13)))) | % 152.79/21.69 | ( ~ (v3 = 0) & ( ~ (v4 = 0) | ( ~ (v5 = 0) & ! [v12: $i] : ( % 152.79/21.69 | ~ (sdtasdt0(v2, v12) = xa) | ~ $i(v12) | ? [v13: % 152.79/21.69 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! % 152.79/21.69 | [v12: $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? % 152.79/21.69 | [v13: $i] : ( ~ (v13 = xa) & sdtasdt0(v2, v12) = v13 & % 152.79/21.69 | $i(v13))))))))) & ! [v2: $i] : ! [v3: % 152.79/21.69 | MultipleValueBool] : ( ~ (doDivides0(v2, xc) = v3) | ~ $i(v2) | % 152.79/21.69 | ? [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: % 152.79/21.69 | any] : ? [v9: $i] : ? [v10: int] : ? [v11: $i] : ($i(v9) & % 152.79/21.69 | ((v11 = xc & v10 = 0 & sdtasdt0(v2, v9) = xc & aElement0(v9) = % 152.79/21.69 | 0) | (aDivisorOf0(v2, xb) = v8 & aDivisorOf0(v2, xa) = v6 & % 152.79/21.69 | doDivides0(v2, xb) = v7 & doDivides0(v2, xa) = v5 & % 152.79/21.69 | aElement0(v2) = v4 & (( ~ (v8 = 0) & ~ (v7 = 0) & ! [v12: % 152.79/21.69 | $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? % 152.79/21.69 | [v13: int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & % 152.79/21.69 | ! [v12: $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? % 152.79/21.69 | [v13: $i] : ( ~ (v13 = xb) & sdtasdt0(v2, v12) = v13 & % 152.79/21.69 | $i(v13)))) | ( ~ (v6 = 0) & ( ~ (v4 = 0) | ( ~ (v5 = % 152.79/21.69 | 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) = xa) | % 152.79/21.69 | ~ $i(v12) | ? [v13: int] : ( ~ (v13 = 0) & % 152.79/21.69 | aElement0(v12) = v13)) & ! [v12: $i] : ( ~ % 152.79/21.69 | (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] : % 152.79/21.69 | ( ~ (v13 = xa) & sdtasdt0(v2, v12) = v13 & % 152.79/21.69 | $i(v13))))))))))) & ! [v2: $i] : ! [v3: any] : % 152.79/21.69 | ( ~ (doDivides0(v2, xb) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: % 152.79/21.69 | any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] % 152.79/21.69 | : ? [v10: int] : ? [v11: $i] : (aDivisorOf0(v2, xb) = v7 & % 152.79/21.69 | aDivisorOf0(v2, xa) = v6 & doDivides0(v2, xc) = v8 & % 152.79/21.69 | doDivides0(v2, xa) = v5 & aElement0(v2) = v4 & $i(v9) & ((v11 = % 152.79/21.69 | xc & v10 = 0 & v8 = 0 & sdtasdt0(v2, v9) = xc & % 152.79/21.69 | aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v3 = 0) & ! [v12: % 152.79/21.69 | $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? [v13: % 152.79/21.69 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! [v12: % 152.79/21.69 | $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] % 152.79/21.69 | : ( ~ (v13 = xb) & sdtasdt0(v2, v12) = v13 & $i(v13)))) | % 152.79/21.69 | ( ~ (v6 = 0) & ( ~ (v4 = 0) | ( ~ (v5 = 0) & ! [v12: $i] : ( % 152.79/21.69 | ~ (sdtasdt0(v2, v12) = xa) | ~ $i(v12) | ? [v13: % 152.79/21.69 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! % 152.79/21.69 | [v12: $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? % 152.79/21.69 | [v13: $i] : ( ~ (v13 = xa) & sdtasdt0(v2, v12) = v13 & % 152.79/21.69 | $i(v13))))))))) & ! [v2: $i] : ! [v3: any] : ( ~ % 152.79/21.69 | (doDivides0(v2, xa) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: % 152.79/21.69 | any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] % 152.79/21.69 | : ? [v10: int] : ? [v11: $i] : (aDivisorOf0(v2, xb) = v7 & % 152.79/21.69 | aDivisorOf0(v2, xa) = v5 & doDivides0(v2, xc) = v8 & % 152.79/21.69 | doDivides0(v2, xb) = v6 & aElement0(v2) = v4 & $i(v9) & ((v11 = % 152.79/21.69 | xc & v10 = 0 & v8 = 0 & sdtasdt0(v2, v9) = xc & % 152.79/21.69 | aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v6 = 0) & ! [v12: % 152.79/21.69 | $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? [v13: % 152.79/21.69 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! [v12: % 152.79/21.69 | $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] % 152.79/21.69 | : ( ~ (v13 = xb) & sdtasdt0(v2, v12) = v13 & $i(v13)))) | % 152.79/21.69 | ( ~ (v5 = 0) & ( ~ (v4 = 0) | ( ~ (v3 = 0) & ! [v12: $i] : ( % 152.79/21.69 | ~ (sdtasdt0(v2, v12) = xa) | ~ $i(v12) | ? [v13: % 152.79/21.69 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! % 152.79/21.69 | [v12: $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? % 152.79/21.69 | [v13: $i] : ( ~ (v13 = xa) & sdtasdt0(v2, v12) = v13 & % 152.79/21.69 | $i(v13))))))))) & ! [v2: $i] : ! [v3: any] : ( ~ % 152.79/21.69 | (aElement0(v2) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: any] : % 152.79/21.69 | ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? [v10: % 152.79/21.69 | int] : ? [v11: $i] : (aDivisorOf0(v2, xb) = v7 & % 152.79/21.69 | aDivisorOf0(v2, xa) = v5 & doDivides0(v2, xc) = v8 & % 152.79/21.69 | doDivides0(v2, xb) = v6 & doDivides0(v2, xa) = v4 & $i(v9) & % 152.79/21.69 | ((v11 = xc & v10 = 0 & v8 = 0 & sdtasdt0(v2, v9) = xc & % 152.79/21.69 | aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v6 = 0) & ! [v12: % 152.79/21.69 | $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? [v13: % 152.79/21.69 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! [v12: % 152.79/21.69 | $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] % 152.79/21.69 | : ( ~ (v13 = xb) & sdtasdt0(v2, v12) = v13 & $i(v13)))) | % 152.79/21.69 | ( ~ (v5 = 0) & ( ~ (v3 = 0) | ( ~ (v4 = 0) & ! [v12: $i] : ( % 152.79/21.69 | ~ (sdtasdt0(v2, v12) = xa) | ~ $i(v12) | ? [v13: % 152.79/21.69 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! % 152.79/21.69 | [v12: $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? % 152.79/21.69 | [v13: $i] : ( ~ (v13 = xa) & sdtasdt0(v2, v12) = v13 & % 152.79/21.69 | $i(v13)))))))))) % 152.79/21.69 | % 152.79/21.69 | ALPHA: (m__2174) implies: % 152.79/21.70 | (13) ? [v0: $i] : ? [v1: $i] : (slsdtgt0(xb) = v1 & slsdtgt0(xa) = v0 & % 152.79/21.70 | aIdeal0(xI) = 0 & sdtpldt1(v0, v1) = xI & aSet0(xI) = 0 & $i(v1) & % 152.79/21.70 | $i(v0) & ! [v2: $i] : ! [v3: int] : ! [v4: $i] : ! [v5: $i] : % 152.79/21.70 | (v3 = 0 | ~ (aElementOf0(v2, xI) = v3) | ~ (sdtpldt0(v4, v5) = v2) % 152.79/21.70 | | ~ $i(v5) | ~ $i(v4) | ~ $i(v2) | ? [v6: any] : ? [v7: any] % 152.79/21.70 | : (aElementOf0(v5, v1) = v7 & aElementOf0(v4, v0) = v6 & ( ~ (v7 = % 152.79/21.70 | 0) | ~ (v6 = 0)))) & ! [v2: $i] : ! [v3: int] : ! [v4: % 152.79/21.70 | $i] : (v3 = 0 | ~ (aElementOf0(v2, v1) = v3) | ~ (sdtasdt0(xb, % 152.79/21.70 | v4) = v2) | ~ $i(v4) | ~ $i(v2) | ? [v5: int] : ( ~ (v5 = % 152.79/21.70 | 0) & aElement0(v4) = v5)) & ! [v2: $i] : ! [v3: int] : ! % 152.79/21.70 | [v4: $i] : (v3 = 0 | ~ (aElementOf0(v2, v1) = v3) | ~ % 152.79/21.70 | (aElement0(v4) = 0) | ~ $i(v4) | ~ $i(v2) | ? [v5: $i] : ( ~ % 152.79/21.70 | (v5 = v2) & sdtasdt0(xb, v4) = v5 & $i(v5))) & ! [v2: $i] : ! % 152.79/21.70 | [v3: int] : ! [v4: $i] : (v3 = 0 | ~ (aElementOf0(v2, v0) = v3) | % 152.79/21.70 | ~ (sdtasdt0(xa, v4) = v2) | ~ $i(v4) | ~ $i(v2) | ? [v5: int] : % 152.79/21.70 | ( ~ (v5 = 0) & aElement0(v4) = v5)) & ! [v2: $i] : ! [v3: int] : % 152.79/21.70 | ! [v4: $i] : (v3 = 0 | ~ (aElementOf0(v2, v0) = v3) | ~ % 152.79/21.70 | (aElement0(v4) = 0) | ~ $i(v4) | ~ $i(v2) | ? [v5: $i] : ( ~ % 152.79/21.70 | (v5 = v2) & sdtasdt0(xa, v4) = v5 & $i(v5))) & ! [v2: $i] : ! % 152.79/21.70 | [v3: $i] : ! [v4: $i] : ( ~ (aElementOf0(v2, xI) = 0) | ~ % 152.79/21.70 | (sdtasdt0(v3, v2) = v4) | ~ $i(v3) | ~ $i(v2) | ? [v5: any] : % 152.79/21.70 | ? [v6: any] : (aElementOf0(v4, xI) = v6 & aElement0(v3) = v5 & ( ~ % 152.79/21.70 | (v5 = 0) | v6 = 0))) & ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 152.79/21.70 | : ( ~ (aElementOf0(v2, xI) = 0) | ~ (sdtpldt0(v2, v3) = v4) | ~ % 152.79/21.70 | $i(v3) | ~ $i(v2) | ? [v5: any] : ? [v6: any] : % 152.79/21.70 | (aElementOf0(v4, xI) = v6 & aElementOf0(v3, xI) = v5 & ( ~ (v5 = % 152.79/21.70 | 0) | v6 = 0))) & ! [v2: $i] : ! [v3: $i] : ( ~ % 152.79/21.70 | (aElementOf0(v3, xI) = 0) | ~ (aElementOf0(v2, xI) = 0) | ~ % 152.79/21.70 | $i(v3) | ~ $i(v2) | ? [v4: $i] : (aElementOf0(v4, xI) = 0 & % 152.79/21.70 | sdtpldt0(v2, v3) = v4 & $i(v4))) & ! [v2: $i] : ! [v3: $i] : ( % 152.79/21.70 | ~ (aElementOf0(v2, xI) = 0) | ~ (aElement0(v3) = 0) | ~ $i(v3) | % 152.79/21.70 | ~ $i(v2) | ? [v4: $i] : (aElementOf0(v4, xI) = 0 & sdtasdt0(v3, % 152.79/21.70 | v2) = v4 & $i(v4))) & ! [v2: $i] : ( ~ (aElementOf0(v2, v1) = % 152.79/21.70 | 0) | ~ $i(v2) | ? [v3: $i] : (sdtasdt0(xb, v3) = v2 & % 152.79/21.70 | aElement0(v3) = 0 & $i(v3))) & ! [v2: $i] : ( ~ % 152.79/21.70 | (aElementOf0(v2, v0) = 0) | ~ $i(v2) | ? [v3: $i] : % 152.79/21.70 | (sdtasdt0(xa, v3) = v2 & aElement0(v3) = 0 & $i(v3))) & ! [v2: % 152.79/21.70 | $i] : ( ~ (aElementOf0(v2, xI) = 0) | ~ $i(v2) | ? [v3: $i] : ? % 152.79/21.70 | [v4: $i] : (aElementOf0(v4, v1) = 0 & aElementOf0(v3, v0) = 0 & % 152.79/21.70 | sdtpldt0(v3, v4) = v2 & $i(v4) & $i(v3)))) % 152.79/21.70 | % 152.79/21.70 | ALPHA: (m__2203) implies: % 152.79/21.70 | (14) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 152.79/21.70 | ? [v5: $i] : (slsdtgt0(xb) = v1 & slsdtgt0(xa) = v0 & aElementOf0(xb, % 152.79/21.70 | v1) = 0 & aElementOf0(xa, v0) = 0 & aElementOf0(sz00, v1) = 0 & % 152.79/21.70 | aElementOf0(sz00, v0) = 0 & sdtasdt0(xb, v3) = sz00 & sdtasdt0(xb, % 152.79/21.70 | v2) = xb & sdtasdt0(xa, v5) = sz00 & sdtasdt0(xa, v4) = xa & % 152.79/21.70 | aElement0(v5) = 0 & aElement0(v4) = 0 & aElement0(v3) = 0 & % 152.79/21.70 | aElement0(v2) = 0 & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & % 152.79/21.70 | $i(v0)) % 152.79/21.70 | % 152.79/21.70 | ALPHA: (m__2228) implies: % 152.79/21.70 | (15) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 152.79/21.70 | ? [v5: $i] : ( ~ (v3 = sz00) & slsdtgt0(xb) = v1 & slsdtgt0(xa) = v0 & % 152.79/21.70 | sdtpldt1(v0, v1) = v2 & aElementOf0(v5, v1) = 0 & aElementOf0(v4, % 152.79/21.70 | v0) = 0 & aElementOf0(v3, v2) = 0 & sdtpldt0(v4, v5) = v3 & $i(v5) % 152.79/21.70 | & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ! [v6: $i] : ! [v7: % 152.79/21.70 | int] : ! [v8: $i] : (v7 = 0 | ~ (aElementOf0(v6, v1) = v7) | ~ % 152.79/21.70 | (sdtasdt0(xb, v8) = v6) | ~ $i(v8) | ~ $i(v6) | ? [v9: int] : ( % 152.79/21.70 | ~ (v9 = 0) & aElement0(v8) = v9)) & ! [v6: $i] : ! [v7: int] : % 152.79/21.70 | ! [v8: $i] : (v7 = 0 | ~ (aElementOf0(v6, v1) = v7) | ~ % 152.79/21.70 | (aElement0(v8) = 0) | ~ $i(v8) | ~ $i(v6) | ? [v9: $i] : ( ~ % 152.79/21.70 | (v9 = v6) & sdtasdt0(xb, v8) = v9 & $i(v9))) & ! [v6: $i] : ! % 152.79/21.70 | [v7: int] : ! [v8: $i] : (v7 = 0 | ~ (aElementOf0(v6, v0) = v7) | % 152.79/21.70 | ~ (sdtasdt0(xa, v8) = v6) | ~ $i(v8) | ~ $i(v6) | ? [v9: int] : % 152.79/21.70 | ( ~ (v9 = 0) & aElement0(v8) = v9)) & ! [v6: $i] : ! [v7: int] : % 152.79/21.70 | ! [v8: $i] : (v7 = 0 | ~ (aElementOf0(v6, v0) = v7) | ~ % 152.79/21.70 | (aElement0(v8) = 0) | ~ $i(v8) | ~ $i(v6) | ? [v9: $i] : ( ~ % 152.79/21.70 | (v9 = v6) & sdtasdt0(xa, v8) = v9 & $i(v9))) & ! [v6: $i] : ( ~ % 152.79/21.70 | (aElementOf0(v6, v1) = 0) | ~ $i(v6) | ? [v7: $i] : % 152.79/21.70 | (sdtasdt0(xb, v7) = v6 & aElement0(v7) = 0 & $i(v7))) & ! [v6: % 152.79/21.70 | $i] : ( ~ (aElementOf0(v6, v0) = 0) | ~ $i(v6) | ? [v7: $i] : % 152.79/21.70 | (sdtasdt0(xa, v7) = v6 & aElement0(v7) = 0 & $i(v7)))) % 152.79/21.70 | % 152.79/21.70 | ALPHA: (m__2273) implies: % 152.79/21.70 | (16) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 152.79/21.70 | ( ~ (xu = sz00) & slsdtgt0(xb) = v1 & slsdtgt0(xa) = v0 & sbrdtbr0(xu) % 152.79/21.70 | = v2 & aElementOf0(v4, v1) = 0 & aElementOf0(v3, v0) = 0 & % 152.79/21.70 | aElementOf0(xu, xI) = 0 & sdtpldt0(v3, v4) = xu & $i(v4) & $i(v3) & % 152.79/21.70 | $i(v2) & $i(v1) & $i(v0) & ! [v5: $i] : ! [v6: MultipleValueBool] % 152.79/21.70 | : ! [v7: $i] : ! [v8: $i] : (v5 = sz00 | ~ (aElementOf0(v5, xI) = % 152.79/21.70 | v6) | ~ (sdtpldt0(v7, v8) = v5) | ~ $i(v8) | ~ $i(v7) | ~ % 152.79/21.70 | $i(v5) | ? [v9: any] : ? [v10: int] : (( ~ (v10 = 0) & % 152.79/21.70 | iLess0(v9, v2) = v10 & sbrdtbr0(v5) = v9 & $i(v9)) | % 152.79/21.70 | (aElementOf0(v8, v1) = v10 & aElementOf0(v7, v0) = v9 & ( ~ (v10 % 152.79/21.70 | = 0) | ~ (v9 = 0))))) & ! [v5: $i] : ! [v6: $i] : (v5 = % 152.79/21.70 | sz00 | ~ (sbrdtbr0(v5) = v6) | ~ $i(v5) | ? [v7: any] : ? [v8: % 152.79/21.70 | any] : (iLess0(v6, v2) = v8 & aElementOf0(v5, xI) = v7 & ( ~ (v8 % 152.79/21.70 | = 0) | ( ~ (v7 = 0) & ! [v9: $i] : ! [v10: $i] : ( ~ % 152.79/21.70 | (sdtpldt0(v9, v10) = v5) | ~ $i(v10) | ~ $i(v9) | ? % 152.79/21.70 | [v11: any] : ? [v12: any] : (aElementOf0(v10, v1) = v12 & % 152.79/21.70 | aElementOf0(v9, v0) = v11 & ( ~ (v12 = 0) | ~ (v11 = % 152.79/21.70 | 0)))))))) & ! [v5: $i] : (v5 = sz00 | ~ % 152.79/21.70 | (aElementOf0(v5, xI) = 0) | ~ $i(v5) | ? [v6: $i] : ? [v7: int] % 152.79/21.70 | : ( ~ (v7 = 0) & iLess0(v6, v2) = v7 & sbrdtbr0(v5) = v6 & % 152.79/21.70 | $i(v6)))) % 152.79/21.70 | % 152.79/21.70 | ALPHA: (m__2373) implies: % 152.79/21.70 | (17) ? [v0: $i] : ? [v1: $i] : (aDivisorOf0(xu, xb) = 0 & aDivisorOf0(xu, % 152.79/21.70 | xa) = 0 & doDivides0(xu, xb) = 0 & doDivides0(xu, xa) = 0 & % 152.79/21.70 | sdtasdt0(xu, v1) = xa & sdtasdt0(xu, v0) = xb & aElement0(v1) = 0 & % 152.79/21.70 | aElement0(v0) = 0 & $i(v1) & $i(v0)) % 152.79/21.70 | % 152.79/21.70 | ALPHA: (m__2744) implies: % 152.79/21.70 | (18) $i(xu) % 152.79/21.70 | (19) ? [v0: $i] : (sdtasdt0(xu, v0) = xc & aElement0(v0) = 0 & $i(v0)) % 152.79/21.70 | % 152.79/21.70 | ALPHA: (m__) implies: % 152.79/21.71 | (20) $i(xa) % 152.79/21.71 | (21) $i(xb) % 152.79/21.71 | (22) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: int] : ( ~ (v3 = 0) % 152.79/21.71 | & slsdtgt0(xb) = v1 & slsdtgt0(xa) = v0 & sdtpldt1(v0, v1) = v2 & % 152.79/21.71 | aElementOf0(xc, v2) = v3 & $i(v2) & $i(v1) & $i(v0) & ! [v4: $i] : % 152.79/21.71 | ! [v5: int] : ! [v6: $i] : (v5 = 0 | ~ (aElementOf0(v4, v1) = v5) % 152.79/21.71 | | ~ (sdtasdt0(xb, v6) = v4) | ~ $i(v6) | ~ $i(v4) | ? [v7: % 152.79/21.71 | int] : ( ~ (v7 = 0) & aElement0(v6) = v7)) & ! [v4: $i] : ! % 152.79/21.71 | [v5: int] : ! [v6: $i] : (v5 = 0 | ~ (aElementOf0(v4, v1) = v5) | % 152.79/21.71 | ~ (aElement0(v6) = 0) | ~ $i(v6) | ~ $i(v4) | ? [v7: $i] : ( ~ % 152.79/21.71 | (v7 = v4) & sdtasdt0(xb, v6) = v7 & $i(v7))) & ! [v4: $i] : ! % 152.79/21.71 | [v5: int] : ! [v6: $i] : (v5 = 0 | ~ (aElementOf0(v4, v0) = v5) | % 152.79/21.71 | ~ (sdtasdt0(xa, v6) = v4) | ~ $i(v6) | ~ $i(v4) | ? [v7: int] : % 152.79/21.71 | ( ~ (v7 = 0) & aElement0(v6) = v7)) & ! [v4: $i] : ! [v5: int] : % 152.79/21.71 | ! [v6: $i] : (v5 = 0 | ~ (aElementOf0(v4, v0) = v5) | ~ % 152.79/21.71 | (aElement0(v6) = 0) | ~ $i(v6) | ~ $i(v4) | ? [v7: $i] : ( ~ % 152.79/21.71 | (v7 = v4) & sdtasdt0(xa, v6) = v7 & $i(v7))) & ! [v4: $i] : ! % 152.79/21.71 | [v5: $i] : ( ~ (sdtpldt0(v4, v5) = xc) | ~ $i(v5) | ~ $i(v4) | ? % 152.79/21.71 | [v6: any] : ? [v7: any] : (aElementOf0(v5, v1) = v7 & % 152.79/21.71 | aElementOf0(v4, v0) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0)))) & ! % 152.79/21.71 | [v4: $i] : ( ~ (aElementOf0(v4, v1) = 0) | ~ $i(v4) | ? [v5: $i] : % 152.79/21.71 | (sdtasdt0(xb, v5) = v4 & aElement0(v5) = 0 & $i(v5))) & ! [v4: % 152.79/21.71 | $i] : ( ~ (aElementOf0(v4, v0) = 0) | ~ $i(v4) | ? [v5: $i] : % 152.79/21.71 | (sdtasdt0(xa, v5) = v4 & aElement0(v5) = 0 & $i(v5)))) % 152.79/21.71 | % 152.79/21.71 | ALPHA: (function-axioms) implies: % 152.79/21.71 | (23) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 152.79/21.71 | : (v1 = v0 | ~ (aElement0(v2) = v1) | ~ (aElement0(v2) = v0)) % 152.79/21.71 | (24) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (slsdtgt0(v2) % 152.79/21.71 | = v1) | ~ (slsdtgt0(v2) = v0)) % 152.79/21.71 | (25) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 152.79/21.71 | (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 152.79/21.71 | (26) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 152.79/21.71 | : ! [v3: $i] : (v1 = v0 | ~ (aElementOf0(v3, v2) = v1) | ~ % 152.79/21.71 | (aElementOf0(v3, v2) = v0)) % 152.79/21.71 | (27) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 152.79/21.71 | (sdtpldt1(v3, v2) = v1) | ~ (sdtpldt1(v3, v2) = v0)) % 152.79/21.71 | % 152.79/21.71 | DELTA: instantiating (19) with fresh symbol all_34_0 gives: % 152.79/21.71 | (28) sdtasdt0(xu, all_34_0) = xc & aElement0(all_34_0) = 0 & $i(all_34_0) % 152.79/21.71 | % 152.79/21.71 | ALPHA: (28) implies: % 152.79/21.71 | (29) $i(all_34_0) % 152.79/21.71 | (30) aElement0(all_34_0) = 0 % 152.79/21.71 | (31) sdtasdt0(xu, all_34_0) = xc % 152.79/21.71 | % 152.79/21.71 | DELTA: instantiating (17) with fresh symbols all_36_0, all_36_1 gives: % 152.79/21.71 | (32) aDivisorOf0(xu, xb) = 0 & aDivisorOf0(xu, xa) = 0 & doDivides0(xu, xb) % 152.79/21.71 | = 0 & doDivides0(xu, xa) = 0 & sdtasdt0(xu, all_36_0) = xa & % 152.79/21.71 | sdtasdt0(xu, all_36_1) = xb & aElement0(all_36_0) = 0 & % 152.79/21.71 | aElement0(all_36_1) = 0 & $i(all_36_0) & $i(all_36_1) % 152.79/21.71 | % 152.79/21.71 | ALPHA: (32) implies: % 152.79/21.71 | (33) $i(all_36_1) % 152.79/21.71 | (34) $i(all_36_0) % 152.79/21.71 | (35) sdtasdt0(xu, all_36_1) = xb % 152.79/21.71 | (36) sdtasdt0(xu, all_36_0) = xa % 152.79/21.71 | (37) doDivides0(xu, xa) = 0 % 152.79/21.71 | (38) doDivides0(xu, xb) = 0 % 152.79/21.71 | (39) aDivisorOf0(xu, xa) = 0 % 152.79/21.71 | (40) aDivisorOf0(xu, xb) = 0 % 152.79/21.71 | % 152.79/21.71 | DELTA: instantiating (14) with fresh symbols all_38_0, all_38_1, all_38_2, % 152.79/21.71 | all_38_3, all_38_4, all_38_5 gives: % 152.79/21.71 | (41) slsdtgt0(xb) = all_38_4 & slsdtgt0(xa) = all_38_5 & aElementOf0(xb, % 152.79/21.71 | all_38_4) = 0 & aElementOf0(xa, all_38_5) = 0 & aElementOf0(sz00, % 152.79/21.71 | all_38_4) = 0 & aElementOf0(sz00, all_38_5) = 0 & sdtasdt0(xb, % 152.79/21.71 | all_38_2) = sz00 & sdtasdt0(xb, all_38_3) = xb & sdtasdt0(xa, % 152.79/21.71 | all_38_0) = sz00 & sdtasdt0(xa, all_38_1) = xa & aElement0(all_38_0) % 152.79/21.71 | = 0 & aElement0(all_38_1) = 0 & aElement0(all_38_2) = 0 & % 152.79/21.71 | aElement0(all_38_3) = 0 & $i(all_38_0) & $i(all_38_1) & $i(all_38_2) & % 152.79/21.71 | $i(all_38_3) & $i(all_38_4) & $i(all_38_5) % 152.79/21.71 | % 152.79/21.71 | ALPHA: (41) implies: % 152.79/21.71 | (42) $i(all_38_3) % 152.79/21.71 | (43) $i(all_38_2) % 152.79/21.71 | (44) $i(all_38_1) % 152.79/21.71 | (45) $i(all_38_0) % 152.79/21.71 | (46) sdtasdt0(xa, all_38_1) = xa % 152.79/21.71 | (47) sdtasdt0(xa, all_38_0) = sz00 % 152.79/21.71 | (48) sdtasdt0(xb, all_38_3) = xb % 152.79/21.71 | (49) sdtasdt0(xb, all_38_2) = sz00 % 152.79/21.71 | (50) slsdtgt0(xa) = all_38_5 % 152.79/21.71 | (51) slsdtgt0(xb) = all_38_4 % 152.79/21.71 | % 152.79/21.71 | DELTA: instantiating (16) with fresh symbols all_43_0, all_43_1, all_43_2, % 152.79/21.71 | all_43_3, all_43_4 gives: % 152.79/21.72 | (52) ~ (xu = sz00) & slsdtgt0(xb) = all_43_3 & slsdtgt0(xa) = all_43_4 & % 152.79/21.72 | sbrdtbr0(xu) = all_43_2 & aElementOf0(all_43_0, all_43_3) = 0 & % 152.79/21.72 | aElementOf0(all_43_1, all_43_4) = 0 & aElementOf0(xu, xI) = 0 & % 152.79/21.72 | sdtpldt0(all_43_1, all_43_0) = xu & $i(all_43_0) & $i(all_43_1) & % 152.79/21.72 | $i(all_43_2) & $i(all_43_3) & $i(all_43_4) & ! [v0: $i] : ! [v1: % 152.79/21.72 | MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v0 = sz00 | ~ % 152.79/21.72 | (aElementOf0(v0, xI) = v1) | ~ (sdtpldt0(v2, v3) = v0) | ~ $i(v3) % 152.79/21.72 | | ~ $i(v2) | ~ $i(v0) | ? [v4: any] : ? [v5: int] : (( ~ (v5 = % 152.79/21.72 | 0) & iLess0(v4, all_43_2) = v5 & sbrdtbr0(v0) = v4 & $i(v4)) | % 152.79/21.72 | (aElementOf0(v3, all_43_3) = v5 & aElementOf0(v2, all_43_4) = v4 & % 152.79/21.72 | ( ~ (v5 = 0) | ~ (v4 = 0))))) & ! [v0: $i] : ! [v1: $i] : (v0 % 152.79/21.72 | = sz00 | ~ (sbrdtbr0(v0) = v1) | ~ $i(v0) | ? [v2: any] : ? [v3: % 152.79/21.72 | any] : (iLess0(v1, all_43_2) = v3 & aElementOf0(v0, xI) = v2 & ( ~ % 152.79/21.72 | (v3 = 0) | ( ~ (v2 = 0) & ! [v4: $i] : ! [v5: $i] : ( ~ % 152.79/21.72 | (sdtpldt0(v4, v5) = v0) | ~ $i(v5) | ~ $i(v4) | ? [v6: % 152.79/21.72 | any] : ? [v7: any] : (aElementOf0(v5, all_43_3) = v7 & % 152.79/21.72 | aElementOf0(v4, all_43_4) = v6 & ( ~ (v7 = 0) | ~ (v6 = % 152.79/21.72 | 0)))))))) & ! [v0: $i] : (v0 = sz00 | ~ % 152.79/21.72 | (aElementOf0(v0, xI) = 0) | ~ $i(v0) | ? [v1: $i] : ? [v2: int] : % 152.79/21.72 | ( ~ (v2 = 0) & iLess0(v1, all_43_2) = v2 & sbrdtbr0(v0) = v1 & % 152.79/21.72 | $i(v1))) % 152.79/21.72 | % 152.79/21.72 | ALPHA: (52) implies: % 152.79/21.72 | (53) ~ (xu = sz00) % 152.79/21.72 | (54) $i(all_43_1) % 152.79/21.72 | (55) $i(all_43_0) % 152.79/21.72 | (56) sdtpldt0(all_43_1, all_43_0) = xu % 152.79/21.72 | (57) aElementOf0(xu, xI) = 0 % 152.79/21.72 | (58) aElementOf0(all_43_1, all_43_4) = 0 % 152.79/21.72 | (59) aElementOf0(all_43_0, all_43_3) = 0 % 152.79/21.72 | (60) sbrdtbr0(xu) = all_43_2 % 152.79/21.72 | (61) slsdtgt0(xa) = all_43_4 % 152.79/21.72 | (62) slsdtgt0(xb) = all_43_3 % 152.79/21.72 | (63) ! [v0: $i] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : % 152.79/21.72 | (v0 = sz00 | ~ (aElementOf0(v0, xI) = v1) | ~ (sdtpldt0(v2, v3) = % 152.79/21.72 | v0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v0) | ? [v4: any] : ? [v5: % 152.79/21.72 | int] : (( ~ (v5 = 0) & iLess0(v4, all_43_2) = v5 & sbrdtbr0(v0) = % 152.79/21.72 | v4 & $i(v4)) | (aElementOf0(v3, all_43_3) = v5 & aElementOf0(v2, % 152.79/21.72 | all_43_4) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0))))) % 152.79/21.72 | % 152.79/21.72 | DELTA: instantiating (15) with fresh symbols all_46_0, all_46_1, all_46_2, % 152.79/21.72 | all_46_3, all_46_4, all_46_5 gives: % 152.79/21.72 | (64) ~ (all_46_2 = sz00) & slsdtgt0(xb) = all_46_4 & slsdtgt0(xa) = % 152.79/21.72 | all_46_5 & sdtpldt1(all_46_5, all_46_4) = all_46_3 & % 152.79/21.72 | aElementOf0(all_46_0, all_46_4) = 0 & aElementOf0(all_46_1, all_46_5) % 152.79/21.72 | = 0 & aElementOf0(all_46_2, all_46_3) = 0 & sdtpldt0(all_46_1, % 152.79/21.72 | all_46_0) = all_46_2 & $i(all_46_0) & $i(all_46_1) & $i(all_46_2) & % 152.79/21.72 | $i(all_46_3) & $i(all_46_4) & $i(all_46_5) & ! [v0: $i] : ! [v1: % 152.79/21.72 | int] : ! [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_46_4) = v1) | % 152.79/21.72 | ~ (sdtasdt0(xb, v2) = v0) | ~ $i(v2) | ~ $i(v0) | ? [v3: int] : % 152.79/21.72 | ( ~ (v3 = 0) & aElement0(v2) = v3)) & ! [v0: $i] : ! [v1: int] : % 152.79/21.72 | ! [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_46_4) = v1) | ~ % 152.79/21.72 | (aElement0(v2) = 0) | ~ $i(v2) | ~ $i(v0) | ? [v3: $i] : ( ~ (v3 % 152.79/21.72 | = v0) & sdtasdt0(xb, v2) = v3 & $i(v3))) & ! [v0: $i] : ! [v1: % 152.79/21.72 | int] : ! [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_46_5) = v1) | % 152.79/21.72 | ~ (sdtasdt0(xa, v2) = v0) | ~ $i(v2) | ~ $i(v0) | ? [v3: int] : % 152.79/21.72 | ( ~ (v3 = 0) & aElement0(v2) = v3)) & ! [v0: $i] : ! [v1: int] : % 152.79/21.72 | ! [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_46_5) = v1) | ~ % 152.79/21.72 | (aElement0(v2) = 0) | ~ $i(v2) | ~ $i(v0) | ? [v3: $i] : ( ~ (v3 % 152.79/21.72 | = v0) & sdtasdt0(xa, v2) = v3 & $i(v3))) & ! [v0: $i] : ( ~ % 152.79/21.72 | (aElementOf0(v0, all_46_4) = 0) | ~ $i(v0) | ? [v1: $i] : % 152.79/21.72 | (sdtasdt0(xb, v1) = v0 & aElement0(v1) = 0 & $i(v1))) & ! [v0: $i] % 152.79/21.72 | : ( ~ (aElementOf0(v0, all_46_5) = 0) | ~ $i(v0) | ? [v1: $i] : % 152.79/21.72 | (sdtasdt0(xa, v1) = v0 & aElement0(v1) = 0 & $i(v1))) % 152.79/21.72 | % 152.79/21.72 | ALPHA: (64) implies: % 152.79/21.72 | (65) $i(all_46_3) % 152.79/21.72 | (66) sdtpldt1(all_46_5, all_46_4) = all_46_3 % 152.79/21.72 | (67) slsdtgt0(xa) = all_46_5 % 152.79/21.72 | (68) slsdtgt0(xb) = all_46_4 % 152.79/21.72 | % 152.79/21.72 | DELTA: instantiating (22) with fresh symbols all_49_0, all_49_1, all_49_2, % 152.79/21.72 | all_49_3 gives: % 152.79/21.73 | (69) ~ (all_49_0 = 0) & slsdtgt0(xb) = all_49_2 & slsdtgt0(xa) = all_49_3 % 152.79/21.73 | & sdtpldt1(all_49_3, all_49_2) = all_49_1 & aElementOf0(xc, all_49_1) % 152.79/21.73 | = all_49_0 & $i(all_49_1) & $i(all_49_2) & $i(all_49_3) & ! [v0: $i] % 152.79/21.73 | : ! [v1: int] : ! [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_49_2) % 152.79/21.73 | = v1) | ~ (sdtasdt0(xb, v2) = v0) | ~ $i(v2) | ~ $i(v0) | ? % 152.79/21.73 | [v3: int] : ( ~ (v3 = 0) & aElement0(v2) = v3)) & ! [v0: $i] : ! % 152.79/21.73 | [v1: int] : ! [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_49_2) = % 152.79/21.73 | v1) | ~ (aElement0(v2) = 0) | ~ $i(v2) | ~ $i(v0) | ? [v3: $i] % 152.79/21.73 | : ( ~ (v3 = v0) & sdtasdt0(xb, v2) = v3 & $i(v3))) & ! [v0: $i] : % 152.79/21.73 | ! [v1: int] : ! [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_49_3) = % 152.79/21.73 | v1) | ~ (sdtasdt0(xa, v2) = v0) | ~ $i(v2) | ~ $i(v0) | ? [v3: % 152.79/21.73 | int] : ( ~ (v3 = 0) & aElement0(v2) = v3)) & ! [v0: $i] : ! [v1: % 152.79/21.73 | int] : ! [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_49_3) = v1) | % 152.79/21.73 | ~ (aElement0(v2) = 0) | ~ $i(v2) | ~ $i(v0) | ? [v3: $i] : ( ~ % 152.79/21.73 | (v3 = v0) & sdtasdt0(xa, v2) = v3 & $i(v3))) & ! [v0: $i] : ! % 152.79/21.73 | [v1: $i] : ( ~ (sdtpldt0(v0, v1) = xc) | ~ $i(v1) | ~ $i(v0) | ? % 152.79/21.73 | [v2: any] : ? [v3: any] : (aElementOf0(v1, all_49_2) = v3 & % 152.79/21.73 | aElementOf0(v0, all_49_3) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & % 152.79/21.73 | ! [v0: $i] : ( ~ (aElementOf0(v0, all_49_2) = 0) | ~ $i(v0) | ? [v1: % 152.79/21.73 | $i] : (sdtasdt0(xb, v1) = v0 & aElement0(v1) = 0 & $i(v1))) & ! % 152.79/21.73 | [v0: $i] : ( ~ (aElementOf0(v0, all_49_3) = 0) | ~ $i(v0) | ? [v1: % 152.79/21.73 | $i] : (sdtasdt0(xa, v1) = v0 & aElement0(v1) = 0 & $i(v1))) % 152.79/21.73 | % 152.79/21.73 | ALPHA: (69) implies: % 152.79/21.73 | (70) ~ (all_49_0 = 0) % 152.79/21.73 | (71) aElementOf0(xc, all_49_1) = all_49_0 % 152.79/21.73 | (72) sdtpldt1(all_49_3, all_49_2) = all_49_1 % 152.79/21.73 | (73) slsdtgt0(xa) = all_49_3 % 152.79/21.73 | (74) slsdtgt0(xb) = all_49_2 % 152.79/21.73 | % 152.79/21.73 | DELTA: instantiating (13) with fresh symbols all_52_0, all_52_1 gives: % 152.79/21.73 | (75) slsdtgt0(xb) = all_52_0 & slsdtgt0(xa) = all_52_1 & aIdeal0(xI) = 0 & % 152.79/21.73 | sdtpldt1(all_52_1, all_52_0) = xI & aSet0(xI) = 0 & $i(all_52_0) & % 152.79/21.73 | $i(all_52_1) & ! [v0: $i] : ! [v1: int] : ! [v2: $i] : ! [v3: $i] % 152.79/21.73 | : (v1 = 0 | ~ (aElementOf0(v0, xI) = v1) | ~ (sdtpldt0(v2, v3) = v0) % 152.79/21.73 | | ~ $i(v3) | ~ $i(v2) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : % 152.79/21.73 | (aElementOf0(v3, all_52_0) = v5 & aElementOf0(v2, all_52_1) = v4 & ( % 152.79/21.73 | ~ (v5 = 0) | ~ (v4 = 0)))) & ! [v0: $i] : ! [v1: int] : ! % 152.79/21.73 | [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_52_0) = v1) | ~ % 152.79/21.73 | (sdtasdt0(xb, v2) = v0) | ~ $i(v2) | ~ $i(v0) | ? [v3: int] : ( ~ % 152.79/21.73 | (v3 = 0) & aElement0(v2) = v3)) & ! [v0: $i] : ! [v1: int] : ! % 152.79/21.73 | [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_52_0) = v1) | ~ % 152.79/21.73 | (aElement0(v2) = 0) | ~ $i(v2) | ~ $i(v0) | ? [v3: $i] : ( ~ (v3 % 152.79/21.73 | = v0) & sdtasdt0(xb, v2) = v3 & $i(v3))) & ! [v0: $i] : ! [v1: % 152.79/21.73 | int] : ! [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_52_1) = v1) | % 152.79/21.73 | ~ (sdtasdt0(xa, v2) = v0) | ~ $i(v2) | ~ $i(v0) | ? [v3: int] : % 152.79/21.73 | ( ~ (v3 = 0) & aElement0(v2) = v3)) & ! [v0: $i] : ! [v1: int] : % 152.79/21.73 | ! [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_52_1) = v1) | ~ % 152.79/21.73 | (aElement0(v2) = 0) | ~ $i(v2) | ~ $i(v0) | ? [v3: $i] : ( ~ (v3 % 152.79/21.73 | = v0) & sdtasdt0(xa, v2) = v3 & $i(v3))) & ! [v0: $i] : ! [v1: % 152.79/21.73 | $i] : ! [v2: $i] : ( ~ (aElementOf0(v0, xI) = 0) | ~ (sdtasdt0(v1, % 152.79/21.73 | v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] % 152.79/21.73 | : (aElementOf0(v2, xI) = v4 & aElement0(v1) = v3 & ( ~ (v3 = 0) | v4 % 152.79/21.73 | = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 152.79/21.73 | (aElementOf0(v0, xI) = 0) | ~ (sdtpldt0(v0, v1) = v2) | ~ $i(v1) | % 152.79/21.73 | ~ $i(v0) | ? [v3: any] : ? [v4: any] : (aElementOf0(v2, xI) = v4 % 152.79/21.73 | & aElementOf0(v1, xI) = v3 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0: % 152.79/21.73 | $i] : ! [v1: $i] : ( ~ (aElementOf0(v1, xI) = 0) | ~ % 152.79/21.73 | (aElementOf0(v0, xI) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: $i] : % 152.79/21.73 | (aElementOf0(v2, xI) = 0 & sdtpldt0(v0, v1) = v2 & $i(v2))) & ! % 152.79/21.73 | [v0: $i] : ! [v1: $i] : ( ~ (aElementOf0(v0, xI) = 0) | ~ % 152.79/21.73 | (aElement0(v1) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: $i] : % 152.79/21.73 | (aElementOf0(v2, xI) = 0 & sdtasdt0(v1, v0) = v2 & $i(v2))) & ! % 152.79/21.73 | [v0: $i] : ( ~ (aElementOf0(v0, all_52_0) = 0) | ~ $i(v0) | ? [v1: % 152.79/21.73 | $i] : (sdtasdt0(xb, v1) = v0 & aElement0(v1) = 0 & $i(v1))) & ! % 152.79/21.73 | [v0: $i] : ( ~ (aElementOf0(v0, all_52_1) = 0) | ~ $i(v0) | ? [v1: % 152.79/21.73 | $i] : (sdtasdt0(xa, v1) = v0 & aElement0(v1) = 0 & $i(v1))) & ! % 152.79/21.73 | [v0: $i] : ( ~ (aElementOf0(v0, xI) = 0) | ~ $i(v0) | ? [v1: $i] : % 152.79/21.73 | ? [v2: $i] : (aElementOf0(v2, all_52_0) = 0 & aElementOf0(v1, % 152.79/21.73 | all_52_1) = 0 & sdtpldt0(v1, v2) = v0 & $i(v2) & $i(v1))) % 152.79/21.73 | % 152.79/21.73 | ALPHA: (75) implies: % 152.79/21.73 | (76) sdtpldt1(all_52_1, all_52_0) = xI % 152.79/21.73 | (77) aIdeal0(xI) = 0 % 152.79/21.73 | (78) slsdtgt0(xa) = all_52_1 % 152.79/21.73 | (79) slsdtgt0(xb) = all_52_0 % 152.79/21.73 | % 152.79/21.73 | DELTA: instantiating (12) with fresh symbols all_55_0, all_55_1 gives: % 152.79/21.75 | (80) aGcdOfAnd0(xc, xa, xb) = 0 & aDivisorOf0(xc, xb) = 0 & aDivisorOf0(xc, % 152.79/21.75 | xa) = 0 & doDivides0(xc, xb) = 0 & doDivides0(xc, xa) = 0 & % 152.79/21.75 | sdtasdt0(xc, all_55_0) = xa & sdtasdt0(xc, all_55_1) = xb & % 152.79/21.75 | aElement0(all_55_0) = 0 & aElement0(all_55_1) = 0 & aElement0(xc) = 0 % 152.79/21.75 | & $i(all_55_0) & $i(all_55_1) & ! [v0: $i] : ! [v1: int] : (v1 = 0 | % 152.79/21.75 | ~ (doDivides0(v0, xc) = v1) | ~ $i(v0) | ? [v2: any] : ? [v3: % 152.79/21.75 | any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : % 152.79/21.75 | (aDivisorOf0(v0, xb) = v6 & aDivisorOf0(v0, xa) = v4 & % 152.79/21.75 | doDivides0(v0, xb) = v5 & doDivides0(v0, xa) = v3 & aElement0(v0) % 152.79/21.75 | = v2 & (( ~ (v6 = 0) & ~ (v5 = 0) & ! [v7: $i] : ( ~ % 152.79/21.75 | (sdtasdt0(v0, v7) = xb) | ~ $i(v7) | ? [v8: int] : ( ~ (v8 % 152.79/21.75 | = 0) & aElement0(v7) = v8)) & ! [v7: $i] : ( ~ % 152.79/21.75 | (aElement0(v7) = 0) | ~ $i(v7) | ? [v8: $i] : ( ~ (v8 = % 152.79/21.75 | xb) & sdtasdt0(v0, v7) = v8 & $i(v8)))) | ( ~ (v4 = 0) & % 152.79/21.75 | ( ~ (v2 = 0) | ( ~ (v3 = 0) & ! [v7: $i] : ( ~ (sdtasdt0(v0, % 152.79/21.75 | v7) = xa) | ~ $i(v7) | ? [v8: int] : ( ~ (v8 = 0) % 152.79/21.75 | & aElement0(v7) = v8)) & ! [v7: $i] : ( ~ % 152.79/21.75 | (aElement0(v7) = 0) | ~ $i(v7) | ? [v8: $i] : ( ~ (v8 % 152.79/21.75 | = xa) & sdtasdt0(v0, v7) = v8 & $i(v8))))))))) & ! % 152.79/21.75 | [v0: $i] : ! [v1: any] : ( ~ (aDivisorOf0(v0, xb) = v1) | ~ $i(v0) | % 152.79/21.75 | ? [v2: any] : ? [v3: any] : ? [v4: any] : ? [v5: any] : ? [v6: % 152.79/21.75 | any] : ? [v7: $i] : ? [v8: int] : ? [v9: $i] : (aDivisorOf0(v0, % 152.79/21.75 | xa) = v4 & doDivides0(v0, xc) = v6 & doDivides0(v0, xb) = v5 & % 152.79/21.75 | doDivides0(v0, xa) = v3 & aElement0(v0) = v2 & $i(v7) & ((v9 = xc % 152.79/21.75 | & v8 = 0 & v6 = 0 & sdtasdt0(v0, v7) = xc & aElement0(v7) = 0) % 152.79/21.75 | | ( ~ (v5 = 0) & ~ (v1 = 0) & ! [v10: $i] : ( ~ (sdtasdt0(v0, % 152.79/21.75 | v10) = xb) | ~ $i(v10) | ? [v11: int] : ( ~ (v11 = 0) % 152.79/21.75 | & aElement0(v10) = v11)) & ! [v10: $i] : ( ~ % 152.79/21.75 | (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: $i] : ( ~ (v11 % 152.79/21.75 | = xb) & sdtasdt0(v0, v10) = v11 & $i(v11)))) | ( ~ (v4 = % 152.79/21.75 | 0) & ( ~ (v2 = 0) | ( ~ (v3 = 0) & ! [v10: $i] : ( ~ % 152.79/21.75 | (sdtasdt0(v0, v10) = xa) | ~ $i(v10) | ? [v11: int] : % 152.79/21.75 | ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! [v10: $i] : % 152.79/21.75 | ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: $i] : ( ~ % 152.79/21.75 | (v11 = xa) & sdtasdt0(v0, v10) = v11 & $i(v11))))))))) % 152.79/21.75 | & ! [v0: $i] : ! [v1: any] : ( ~ (aDivisorOf0(v0, xa) = v1) | ~ % 152.79/21.75 | $i(v0) | ? [v2: any] : ? [v3: any] : ? [v4: any] : ? [v5: any] : % 152.79/21.75 | ? [v6: any] : ? [v7: $i] : ? [v8: int] : ? [v9: $i] : % 152.79/21.75 | (aDivisorOf0(v0, xb) = v5 & doDivides0(v0, xc) = v6 & doDivides0(v0, % 152.79/21.75 | xb) = v4 & doDivides0(v0, xa) = v3 & aElement0(v0) = v2 & $i(v7) % 152.79/21.75 | & ((v9 = xc & v8 = 0 & v6 = 0 & sdtasdt0(v0, v7) = xc & % 152.79/21.75 | aElement0(v7) = 0) | ( ~ (v5 = 0) & ~ (v4 = 0) & ! [v10: $i] % 152.79/21.75 | : ( ~ (sdtasdt0(v0, v10) = xb) | ~ $i(v10) | ? [v11: int] : % 152.79/21.75 | ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! [v10: $i] : ( ~ % 152.79/21.75 | (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: $i] : ( ~ (v11 % 152.79/21.75 | = xb) & sdtasdt0(v0, v10) = v11 & $i(v11)))) | ( ~ (v1 = % 152.79/21.75 | 0) & ( ~ (v2 = 0) | ( ~ (v3 = 0) & ! [v10: $i] : ( ~ % 152.79/21.75 | (sdtasdt0(v0, v10) = xa) | ~ $i(v10) | ? [v11: int] : % 152.79/21.75 | ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! [v10: $i] : % 152.79/21.75 | ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: $i] : ( ~ % 152.79/21.75 | (v11 = xa) & sdtasdt0(v0, v10) = v11 & $i(v11))))))))) % 152.79/21.75 | & ! [v0: $i] : ! [v1: MultipleValueBool] : ( ~ (doDivides0(v0, xc) = % 152.79/21.75 | v1) | ~ $i(v0) | ? [v2: any] : ? [v3: any] : ? [v4: any] : ? % 152.79/21.75 | [v5: any] : ? [v6: any] : ? [v7: $i] : ? [v8: int] : ? [v9: $i] % 152.79/21.75 | : ($i(v7) & ((v9 = xc & v8 = 0 & sdtasdt0(v0, v7) = xc & % 152.79/21.75 | aElement0(v7) = 0) | (aDivisorOf0(v0, xb) = v6 & % 152.79/21.75 | aDivisorOf0(v0, xa) = v4 & doDivides0(v0, xb) = v5 & % 152.79/21.75 | doDivides0(v0, xa) = v3 & aElement0(v0) = v2 & (( ~ (v6 = 0) & % 152.79/21.75 | ~ (v5 = 0) & ! [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xb) % 152.79/21.75 | | ~ $i(v10) | ? [v11: int] : ( ~ (v11 = 0) & % 152.79/21.75 | aElement0(v10) = v11)) & ! [v10: $i] : ( ~ % 152.79/21.75 | (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: $i] : ( ~ % 152.79/21.75 | (v11 = xb) & sdtasdt0(v0, v10) = v11 & $i(v11)))) | ( % 152.79/21.75 | ~ (v4 = 0) & ( ~ (v2 = 0) | ( ~ (v3 = 0) & ! [v10: $i] : % 152.79/21.75 | ( ~ (sdtasdt0(v0, v10) = xa) | ~ $i(v10) | ? [v11: % 152.79/21.75 | int] : ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! % 152.79/21.75 | [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? % 152.79/21.75 | [v11: $i] : ( ~ (v11 = xa) & sdtasdt0(v0, v10) = v11 % 152.79/21.75 | & $i(v11))))))))))) & ! [v0: $i] : ! [v1: any] : % 152.79/21.75 | ( ~ (doDivides0(v0, xb) = v1) | ~ $i(v0) | ? [v2: any] : ? [v3: % 152.79/21.75 | any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: $i] : % 152.79/21.75 | ? [v8: int] : ? [v9: $i] : (aDivisorOf0(v0, xb) = v5 & % 152.79/21.75 | aDivisorOf0(v0, xa) = v4 & doDivides0(v0, xc) = v6 & % 152.79/21.75 | doDivides0(v0, xa) = v3 & aElement0(v0) = v2 & $i(v7) & ((v9 = xc % 152.79/21.75 | & v8 = 0 & v6 = 0 & sdtasdt0(v0, v7) = xc & aElement0(v7) = 0) % 152.79/21.75 | | ( ~ (v5 = 0) & ~ (v1 = 0) & ! [v10: $i] : ( ~ (sdtasdt0(v0, % 152.79/21.75 | v10) = xb) | ~ $i(v10) | ? [v11: int] : ( ~ (v11 = 0) % 152.79/21.75 | & aElement0(v10) = v11)) & ! [v10: $i] : ( ~ % 152.79/21.75 | (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: $i] : ( ~ (v11 % 152.79/21.75 | = xb) & sdtasdt0(v0, v10) = v11 & $i(v11)))) | ( ~ (v4 = % 152.79/21.75 | 0) & ( ~ (v2 = 0) | ( ~ (v3 = 0) & ! [v10: $i] : ( ~ % 152.79/21.75 | (sdtasdt0(v0, v10) = xa) | ~ $i(v10) | ? [v11: int] : % 152.79/21.75 | ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! [v10: $i] : % 152.79/21.75 | ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: $i] : ( ~ % 152.79/21.75 | (v11 = xa) & sdtasdt0(v0, v10) = v11 & $i(v11))))))))) % 152.79/21.75 | & ! [v0: $i] : ! [v1: any] : ( ~ (doDivides0(v0, xa) = v1) | ~ % 152.79/21.75 | $i(v0) | ? [v2: any] : ? [v3: any] : ? [v4: any] : ? [v5: any] : % 152.79/21.75 | ? [v6: any] : ? [v7: $i] : ? [v8: int] : ? [v9: $i] : % 152.79/21.75 | (aDivisorOf0(v0, xb) = v5 & aDivisorOf0(v0, xa) = v3 & % 152.79/21.75 | doDivides0(v0, xc) = v6 & doDivides0(v0, xb) = v4 & aElement0(v0) % 152.79/21.75 | = v2 & $i(v7) & ((v9 = xc & v8 = 0 & v6 = 0 & sdtasdt0(v0, v7) = % 152.79/21.75 | xc & aElement0(v7) = 0) | ( ~ (v5 = 0) & ~ (v4 = 0) & ! % 152.79/21.75 | [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xb) | ~ $i(v10) | ? % 152.79/21.75 | [v11: int] : ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! % 152.79/21.75 | [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: % 152.79/21.75 | $i] : ( ~ (v11 = xb) & sdtasdt0(v0, v10) = v11 & % 152.79/21.75 | $i(v11)))) | ( ~ (v3 = 0) & ( ~ (v2 = 0) | ( ~ (v1 = 0) & % 152.79/21.75 | ! [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xa) | ~ $i(v10) | % 152.79/21.75 | ? [v11: int] : ( ~ (v11 = 0) & aElement0(v10) = v11)) & % 152.79/21.75 | ! [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? % 152.79/21.75 | [v11: $i] : ( ~ (v11 = xa) & sdtasdt0(v0, v10) = v11 & % 152.79/21.75 | $i(v11))))))))) & ! [v0: $i] : ! [v1: any] : ( ~ % 152.79/21.75 | (aElement0(v0) = v1) | ~ $i(v0) | ? [v2: any] : ? [v3: any] : ? % 152.79/21.75 | [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: $i] : ? [v8: int] % 152.79/21.75 | : ? [v9: $i] : (aDivisorOf0(v0, xb) = v5 & aDivisorOf0(v0, xa) = v3 % 152.79/21.75 | & doDivides0(v0, xc) = v6 & doDivides0(v0, xb) = v4 & % 152.79/21.75 | doDivides0(v0, xa) = v2 & $i(v7) & ((v9 = xc & v8 = 0 & v6 = 0 & % 152.79/21.75 | sdtasdt0(v0, v7) = xc & aElement0(v7) = 0) | ( ~ (v5 = 0) & ~ % 152.79/21.75 | (v4 = 0) & ! [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xb) | ~ % 152.79/21.75 | $i(v10) | ? [v11: int] : ( ~ (v11 = 0) & aElement0(v10) = % 152.79/21.75 | v11)) & ! [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ % 152.79/21.75 | $i(v10) | ? [v11: $i] : ( ~ (v11 = xb) & sdtasdt0(v0, v10) % 152.79/21.75 | = v11 & $i(v11)))) | ( ~ (v3 = 0) & ( ~ (v1 = 0) | ( ~ (v2 % 152.79/21.75 | = 0) & ! [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xa) | ~ % 152.79/21.75 | $i(v10) | ? [v11: int] : ( ~ (v11 = 0) & aElement0(v10) % 152.79/21.75 | = v11)) & ! [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ % 152.79/21.75 | $i(v10) | ? [v11: $i] : ( ~ (v11 = xa) & sdtasdt0(v0, % 152.79/21.75 | v10) = v11 & $i(v11))))))))) % 152.79/21.75 | % 152.79/21.75 | ALPHA: (80) implies: % 152.79/21.75 | (81) $i(all_55_1) % 152.79/21.75 | (82) $i(all_55_0) % 152.79/21.75 | (83) sdtasdt0(xc, all_55_1) = xb % 152.79/21.75 | (84) sdtasdt0(xc, all_55_0) = xa % 152.79/21.75 | (85) ! [v0: $i] : ! [v1: any] : ( ~ (doDivides0(v0, xa) = v1) | ~ $i(v0) % 152.79/21.75 | | ? [v2: any] : ? [v3: any] : ? [v4: any] : ? [v5: any] : ? % 152.79/21.75 | [v6: any] : ? [v7: $i] : ? [v8: int] : ? [v9: $i] : % 152.79/21.75 | (aDivisorOf0(v0, xb) = v5 & aDivisorOf0(v0, xa) = v3 & % 152.79/21.75 | doDivides0(v0, xc) = v6 & doDivides0(v0, xb) = v4 & aElement0(v0) % 152.79/21.75 | = v2 & $i(v7) & ((v9 = xc & v8 = 0 & v6 = 0 & sdtasdt0(v0, v7) = % 152.79/21.75 | xc & aElement0(v7) = 0) | ( ~ (v5 = 0) & ~ (v4 = 0) & ! % 152.79/21.75 | [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xb) | ~ $i(v10) | ? % 152.79/21.75 | [v11: int] : ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! % 152.79/21.75 | [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: % 152.79/21.75 | $i] : ( ~ (v11 = xb) & sdtasdt0(v0, v10) = v11 & % 152.79/21.75 | $i(v11)))) | ( ~ (v3 = 0) & ( ~ (v2 = 0) | ( ~ (v1 = 0) & % 152.79/21.75 | ! [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xa) | ~ $i(v10) | % 152.79/21.75 | ? [v11: int] : ( ~ (v11 = 0) & aElement0(v10) = v11)) & % 152.79/21.75 | ! [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? % 152.79/21.75 | [v11: $i] : ( ~ (v11 = xa) & sdtasdt0(v0, v10) = v11 & % 152.79/21.75 | $i(v11))))))))) % 152.79/21.75 | (86) ! [v0: $i] : ! [v1: any] : ( ~ (doDivides0(v0, xb) = v1) | ~ $i(v0) % 152.79/21.75 | | ? [v2: any] : ? [v3: any] : ? [v4: any] : ? [v5: any] : ? % 152.79/21.75 | [v6: any] : ? [v7: $i] : ? [v8: int] : ? [v9: $i] : % 152.79/21.75 | (aDivisorOf0(v0, xb) = v5 & aDivisorOf0(v0, xa) = v4 & % 152.79/21.75 | doDivides0(v0, xc) = v6 & doDivides0(v0, xa) = v3 & aElement0(v0) % 152.79/21.75 | = v2 & $i(v7) & ((v9 = xc & v8 = 0 & v6 = 0 & sdtasdt0(v0, v7) = % 152.79/21.75 | xc & aElement0(v7) = 0) | ( ~ (v5 = 0) & ~ (v1 = 0) & ! % 152.79/21.75 | [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xb) | ~ $i(v10) | ? % 152.79/21.75 | [v11: int] : ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! % 152.79/21.75 | [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: % 152.79/21.75 | $i] : ( ~ (v11 = xb) & sdtasdt0(v0, v10) = v11 & % 152.79/21.75 | $i(v11)))) | ( ~ (v4 = 0) & ( ~ (v2 = 0) | ( ~ (v3 = 0) & % 152.79/21.75 | ! [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xa) | ~ $i(v10) | % 152.79/21.75 | ? [v11: int] : ( ~ (v11 = 0) & aElement0(v10) = v11)) & % 152.79/21.75 | ! [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? % 152.79/21.75 | [v11: $i] : ( ~ (v11 = xa) & sdtasdt0(v0, v10) = v11 & % 152.79/21.75 | $i(v11))))))))) % 152.79/21.75 | (87) ! [v0: $i] : ! [v1: any] : ( ~ (aDivisorOf0(v0, xa) = v1) | ~ % 152.79/21.75 | $i(v0) | ? [v2: any] : ? [v3: any] : ? [v4: any] : ? [v5: any] : % 152.79/21.75 | ? [v6: any] : ? [v7: $i] : ? [v8: int] : ? [v9: $i] : % 152.79/21.75 | (aDivisorOf0(v0, xb) = v5 & doDivides0(v0, xc) = v6 & doDivides0(v0, % 152.79/21.75 | xb) = v4 & doDivides0(v0, xa) = v3 & aElement0(v0) = v2 & $i(v7) % 152.79/21.75 | & ((v9 = xc & v8 = 0 & v6 = 0 & sdtasdt0(v0, v7) = xc & % 152.79/21.75 | aElement0(v7) = 0) | ( ~ (v5 = 0) & ~ (v4 = 0) & ! [v10: $i] % 152.79/21.75 | : ( ~ (sdtasdt0(v0, v10) = xb) | ~ $i(v10) | ? [v11: int] : % 152.79/21.75 | ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! [v10: $i] : ( ~ % 152.79/21.75 | (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: $i] : ( ~ (v11 % 152.79/21.75 | = xb) & sdtasdt0(v0, v10) = v11 & $i(v11)))) | ( ~ (v1 = % 152.79/21.75 | 0) & ( ~ (v2 = 0) | ( ~ (v3 = 0) & ! [v10: $i] : ( ~ % 152.79/21.75 | (sdtasdt0(v0, v10) = xa) | ~ $i(v10) | ? [v11: int] : % 152.79/21.75 | ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! [v10: $i] : % 152.79/21.75 | ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: $i] : ( ~ % 152.79/21.75 | (v11 = xa) & sdtasdt0(v0, v10) = v11 & $i(v11))))))))) % 152.79/21.76 | (88) ! [v0: $i] : ! [v1: any] : ( ~ (aDivisorOf0(v0, xb) = v1) | ~ % 152.79/21.76 | $i(v0) | ? [v2: any] : ? [v3: any] : ? [v4: any] : ? [v5: any] : % 152.79/21.76 | ? [v6: any] : ? [v7: $i] : ? [v8: int] : ? [v9: $i] : % 152.79/21.76 | (aDivisorOf0(v0, xa) = v4 & doDivides0(v0, xc) = v6 & doDivides0(v0, % 152.79/21.76 | xb) = v5 & doDivides0(v0, xa) = v3 & aElement0(v0) = v2 & $i(v7) % 152.79/21.76 | & ((v9 = xc & v8 = 0 & v6 = 0 & sdtasdt0(v0, v7) = xc & % 152.79/21.76 | aElement0(v7) = 0) | ( ~ (v5 = 0) & ~ (v1 = 0) & ! [v10: $i] % 152.79/21.76 | : ( ~ (sdtasdt0(v0, v10) = xb) | ~ $i(v10) | ? [v11: int] : % 152.79/21.76 | ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! [v10: $i] : ( ~ % 152.79/21.76 | (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: $i] : ( ~ (v11 % 152.79/21.76 | = xb) & sdtasdt0(v0, v10) = v11 & $i(v11)))) | ( ~ (v4 = % 152.79/21.76 | 0) & ( ~ (v2 = 0) | ( ~ (v3 = 0) & ! [v10: $i] : ( ~ % 152.79/21.76 | (sdtasdt0(v0, v10) = xa) | ~ $i(v10) | ? [v11: int] : % 152.79/21.76 | ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! [v10: $i] : % 152.79/21.76 | ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: $i] : ( ~ % 152.79/21.76 | (v11 = xa) & sdtasdt0(v0, v10) = v11 & $i(v11))))))))) % 152.79/21.76 | % 152.79/21.76 | GROUND_INST: instantiating (24) with all_46_5, all_49_3, xa, simplifying with % 152.79/21.76 | (67), (73) gives: % 152.79/21.76 | (89) all_49_3 = all_46_5 % 152.79/21.76 | % 152.79/21.76 | GROUND_INST: instantiating (24) with all_43_4, all_49_3, xa, simplifying with % 152.79/21.76 | (61), (73) gives: % 152.79/21.76 | (90) all_49_3 = all_43_4 % 152.79/21.76 | % 152.79/21.76 | GROUND_INST: instantiating (24) with all_46_5, all_52_1, xa, simplifying with % 152.79/21.76 | (67), (78) gives: % 152.79/21.76 | (91) all_52_1 = all_46_5 % 152.79/21.76 | % 152.79/21.76 | GROUND_INST: instantiating (24) with all_38_5, all_52_1, xa, simplifying with % 152.79/21.76 | (50), (78) gives: % 152.79/21.76 | (92) all_52_1 = all_38_5 % 152.79/21.76 | % 152.79/21.76 | GROUND_INST: instantiating (24) with all_43_3, all_46_4, xb, simplifying with % 152.79/21.76 | (62), (68) gives: % 152.79/21.76 | (93) all_46_4 = all_43_3 % 152.79/21.76 | % 152.79/21.76 | GROUND_INST: instantiating (24) with all_46_4, all_49_2, xb, simplifying with % 152.79/21.76 | (68), (74) gives: % 152.79/21.76 | (94) all_49_2 = all_46_4 % 152.79/21.76 | % 152.79/21.76 | GROUND_INST: instantiating (24) with all_49_2, all_52_0, xb, simplifying with % 152.79/21.76 | (74), (79) gives: % 152.79/21.76 | (95) all_52_0 = all_49_2 % 152.79/21.76 | % 152.79/21.76 | GROUND_INST: instantiating (24) with all_38_4, all_52_0, xb, simplifying with % 152.79/21.76 | (51), (79) gives: % 152.79/21.76 | (96) all_52_0 = all_38_4 % 152.79/21.76 | % 152.79/21.76 | COMBINE_EQS: (95), (96) imply: % 152.79/21.76 | (97) all_49_2 = all_38_4 % 152.79/21.76 | % 152.79/21.76 | SIMP: (97) implies: % 152.79/21.76 | (98) all_49_2 = all_38_4 % 152.79/21.76 | % 152.79/21.76 | COMBINE_EQS: (91), (92) imply: % 152.79/21.76 | (99) all_46_5 = all_38_5 % 152.79/21.76 | % 152.79/21.76 | SIMP: (99) implies: % 152.79/21.76 | (100) all_46_5 = all_38_5 % 152.79/21.76 | % 152.79/21.76 | COMBINE_EQS: (94), (98) imply: % 152.79/21.76 | (101) all_46_4 = all_38_4 % 152.79/21.76 | % 152.79/21.76 | SIMP: (101) implies: % 152.79/21.76 | (102) all_46_4 = all_38_4 % 152.79/21.76 | % 152.79/21.76 | COMBINE_EQS: (89), (90) imply: % 152.79/21.76 | (103) all_46_5 = all_43_4 % 152.79/21.76 | % 152.79/21.76 | SIMP: (103) implies: % 152.79/21.76 | (104) all_46_5 = all_43_4 % 152.79/21.76 | % 152.79/21.76 | COMBINE_EQS: (93), (102) imply: % 152.79/21.76 | (105) all_43_3 = all_38_4 % 152.79/21.76 | % 152.79/21.76 | SIMP: (105) implies: % 152.79/21.76 | (106) all_43_3 = all_38_4 % 152.79/21.76 | % 152.79/21.76 | COMBINE_EQS: (100), (104) imply: % 152.79/21.76 | (107) all_43_4 = all_38_5 % 152.79/21.76 | % 152.79/21.76 | COMBINE_EQS: (90), (107) imply: % 152.79/21.76 | (108) all_49_3 = all_38_5 % 152.79/21.76 | % 152.79/21.76 | REDUCE: (76), (92), (96) imply: % 152.79/21.76 | (109) sdtpldt1(all_38_5, all_38_4) = xI % 152.79/21.76 | % 152.79/21.76 | REDUCE: (72), (98), (108) imply: % 152.79/21.76 | (110) sdtpldt1(all_38_5, all_38_4) = all_49_1 % 152.79/21.76 | % 152.79/21.76 | REDUCE: (66), (100), (102) imply: % 152.79/21.76 | (111) sdtpldt1(all_38_5, all_38_4) = all_46_3 % 152.79/21.76 | % 152.79/21.76 | REDUCE: (59), (106) imply: % 152.79/21.76 | (112) aElementOf0(all_43_0, all_38_4) = 0 % 152.79/21.76 | % 152.79/21.76 | REDUCE: (58), (107) imply: % 152.79/21.76 | (113) aElementOf0(all_43_1, all_38_5) = 0 % 152.79/21.76 | % 152.79/21.76 | GROUND_INST: instantiating (27) with all_46_3, all_49_1, all_38_4, all_38_5, % 152.79/21.76 | simplifying with (110), (111) gives: % 152.79/21.76 | (114) all_49_1 = all_46_3 % 152.79/21.76 | % 152.79/21.76 | GROUND_INST: instantiating (27) with xI, all_49_1, all_38_4, all_38_5, % 152.79/21.76 | simplifying with (109), (110) gives: % 152.79/21.76 | (115) all_49_1 = xI % 152.79/21.76 | % 152.79/21.76 | COMBINE_EQS: (114), (115) imply: % 152.79/21.76 | (116) all_46_3 = xI % 152.79/21.76 | % 152.79/21.76 | SIMP: (116) implies: % 152.79/21.76 | (117) all_46_3 = xI % 152.79/21.76 | % 152.79/21.76 | REDUCE: (71), (115) imply: % 152.79/21.76 | (118) aElementOf0(xc, xI) = all_49_0 % 152.79/21.76 | % 152.79/21.76 | REDUCE: (65), (117) imply: % 152.79/21.76 | (119) $i(xI) % 152.79/21.76 | % 152.79/21.76 | GROUND_INST: instantiating (mSortsB) with all_43_1, all_43_0, xu, simplifying % 152.79/21.76 | with (54), (55), (56) gives: % 152.79/21.76 | (120) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_43_0) = % 152.79/21.76 | v1 & aElement0(all_43_1) = v0 & aElement0(xu) = v2 & ( ~ (v1 = 0) | % 152.79/21.76 | ~ (v0 = 0) | v2 = 0)) % 152.79/21.76 | % 152.79/21.76 | GROUND_INST: instantiating (3) with xu, all_34_0, all_55_0, xc, xa, % 152.79/21.76 | simplifying with (18), (29), (31), (82), (84) gives: % 152.79/21.76 | (121) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: % 152.79/21.76 | $i] : (sdtasdt0(all_34_0, all_55_0) = v3 & sdtasdt0(xu, v3) = v4 & % 152.79/21.76 | aElement0(all_55_0) = v2 & aElement0(all_34_0) = v1 & aElement0(xu) % 152.79/21.76 | = v0 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | % 152.79/21.76 | v4 = xa)) % 152.79/21.76 | % 152.79/21.77 | GROUND_INST: instantiating (3) with xu, all_34_0, all_55_1, xc, xb, % 152.79/21.77 | simplifying with (18), (29), (31), (81), (83) gives: % 152.79/21.77 | (122) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: % 152.79/21.77 | $i] : (sdtasdt0(all_34_0, all_55_1) = v3 & sdtasdt0(xu, v3) = v4 & % 152.79/21.77 | aElement0(all_55_1) = v2 & aElement0(all_34_0) = v1 & aElement0(xu) % 152.79/21.77 | = v0 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | % 152.79/21.77 | v4 = xb)) % 152.79/21.77 | % 152.79/21.77 | GROUND_INST: instantiating (4) with all_34_0, all_43_1, all_43_0, xu, xc, % 152.79/21.77 | simplifying with (29), (31), (54), (55), (56) gives: % 152.79/21.77 | (123) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: % 152.79/21.77 | $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? % 152.79/21.77 | [v9: $i] : (sdtasdt0(all_43_0, all_34_0) = v8 & sdtasdt0(all_43_1, % 152.79/21.77 | all_34_0) = v7 & sdtasdt0(all_34_0, all_43_0) = v5 & % 152.79/21.77 | sdtasdt0(all_34_0, all_43_1) = v4 & sdtasdt0(all_34_0, xu) = v3 & % 152.79/21.77 | sdtpldt0(v7, v8) = v9 & sdtpldt0(v4, v5) = v6 & aElement0(all_43_0) % 152.79/21.77 | = v2 & aElement0(all_43_1) = v1 & aElement0(all_34_0) = v0 & $i(v9) % 152.79/21.77 | & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & ( ~ (v2 = % 152.79/21.77 | 0) | ~ (v1 = 0) | ~ (v0 = 0) | (v9 = xc & v6 = v3))) % 152.79/21.77 | % 152.79/21.77 | GROUND_INST: instantiating (2) with all_34_0, xu, xc, simplifying with (18), % 152.79/21.77 | (29), (31) gives: % 152.79/21.77 | (124) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_34_0, xu) = % 152.79/21.77 | v2 & aElement0(all_34_0) = v0 & aElement0(xu) = v1 & $i(v2) & ( ~ % 152.79/21.77 | (v1 = 0) | ~ (v0 = 0) | v2 = xc)) % 152.79/21.77 | % 152.79/21.77 | GROUND_INST: instantiating (1) with xu, all_34_0, xc, simplifying with (18), % 152.79/21.77 | (29), (31) gives: % 152.79/21.77 | (125) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_34_0, xu) = % 152.79/21.77 | v2 & aElement0(all_34_0) = v1 & aElement0(xu) = v0 & $i(v2) & ( ~ % 152.79/21.77 | (v1 = 0) | ~ (v0 = 0) | v2 = xc)) % 152.79/21.77 | % 152.79/21.77 | GROUND_INST: instantiating (mSortsB_02) with xu, all_34_0, xc, simplifying % 152.79/21.77 | with (18), (29), (31) gives: % 152.79/21.77 | (126) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_34_0) = % 152.79/21.77 | v1 & aElement0(xu) = v0 & aElement0(xc) = v2 & ( ~ (v1 = 0) | ~ % 152.79/21.77 | (v0 = 0) | v2 = 0)) % 152.79/21.77 | % 152.79/21.77 | GROUND_INST: instantiating (3) with xu, all_36_1, all_38_2, xb, sz00, % 152.79/21.77 | simplifying with (18), (33), (35), (43), (49) gives: % 152.79/21.77 | (127) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: % 152.79/21.77 | $i] : (sdtasdt0(all_36_1, all_38_2) = v3 & sdtasdt0(xu, v3) = v4 & % 152.79/21.77 | aElement0(all_38_2) = v2 & aElement0(all_36_1) = v1 & aElement0(xu) % 152.79/21.77 | = v0 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | % 152.79/21.77 | v4 = sz00)) % 152.79/21.77 | % 152.79/21.77 | GROUND_INST: instantiating (3) with xu, all_36_1, all_38_3, xb, xb, % 152.79/21.77 | simplifying with (18), (33), (35), (42), (48) gives: % 152.79/21.77 | (128) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: % 152.79/21.77 | $i] : (sdtasdt0(all_36_1, all_38_3) = v3 & sdtasdt0(xu, v3) = v4 & % 152.79/21.77 | aElement0(all_38_3) = v2 & aElement0(all_36_1) = v1 & aElement0(xu) % 152.79/21.77 | = v0 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | % 152.79/21.77 | v4 = xb)) % 152.79/21.77 | % 152.79/21.77 | GROUND_INST: instantiating (2) with all_36_1, xu, xb, simplifying with (18), % 152.79/21.77 | (33), (35) gives: % 152.79/21.77 | (129) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_36_1, xu) = % 152.79/21.77 | v2 & aElement0(all_36_1) = v0 & aElement0(xu) = v1 & $i(v2) & ( ~ % 152.79/21.77 | (v1 = 0) | ~ (v0 = 0) | v2 = xb)) % 152.79/21.77 | % 152.79/21.77 | GROUND_INST: instantiating (1) with xu, all_36_1, xb, simplifying with (18), % 152.79/21.77 | (33), (35) gives: % 152.79/21.77 | (130) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_36_1, xu) = % 152.79/21.77 | v2 & aElement0(all_36_1) = v1 & aElement0(xu) = v0 & $i(v2) & ( ~ % 152.79/21.77 | (v1 = 0) | ~ (v0 = 0) | v2 = xb)) % 152.79/21.77 | % 152.79/21.77 | GROUND_INST: instantiating (mSortsB_02) with xu, all_36_1, xb, simplifying % 152.79/21.77 | with (18), (33), (35) gives: % 152.79/21.77 | (131) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_36_1) = % 152.79/21.77 | v1 & aElement0(xu) = v0 & aElement0(xb) = v2 & ( ~ (v1 = 0) | ~ % 152.79/21.77 | (v0 = 0) | v2 = 0)) % 152.79/21.77 | % 152.79/21.77 | GROUND_INST: instantiating (3) with xu, all_36_0, all_38_0, xa, sz00, % 152.79/21.77 | simplifying with (18), (34), (36), (45), (47) gives: % 152.79/21.77 | (132) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: % 152.79/21.77 | $i] : (sdtasdt0(all_36_0, all_38_0) = v3 & sdtasdt0(xu, v3) = v4 & % 152.79/21.77 | aElement0(all_38_0) = v2 & aElement0(all_36_0) = v1 & aElement0(xu) % 152.79/21.77 | = v0 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | % 152.79/21.77 | v4 = sz00)) % 152.79/21.77 | % 152.79/21.78 | GROUND_INST: instantiating (3) with xu, all_36_0, all_38_1, xa, xa, % 152.79/21.78 | simplifying with (18), (34), (36), (44), (46) gives: % 153.19/21.78 | (133) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: % 153.19/21.78 | $i] : (sdtasdt0(all_36_0, all_38_1) = v3 & sdtasdt0(xu, v3) = v4 & % 153.19/21.78 | aElement0(all_38_1) = v2 & aElement0(all_36_0) = v1 & aElement0(xu) % 153.19/21.78 | = v0 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | % 153.19/21.78 | v4 = xa)) % 153.19/21.78 | % 153.19/21.78 | GROUND_INST: instantiating (2) with all_36_0, xu, xa, simplifying with (18), % 153.19/21.78 | (34), (36) gives: % 153.19/21.78 | (134) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_36_0, xu) = % 153.19/21.78 | v2 & aElement0(all_36_0) = v0 & aElement0(xu) = v1 & $i(v2) & ( ~ % 153.19/21.78 | (v1 = 0) | ~ (v0 = 0) | v2 = xa)) % 153.19/21.78 | % 153.19/21.78 | GROUND_INST: instantiating (1) with xu, all_36_0, xa, simplifying with (18), % 153.19/21.78 | (34), (36) gives: % 153.19/21.78 | (135) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_36_0, xu) = % 153.19/21.78 | v2 & aElement0(all_36_0) = v1 & aElement0(xu) = v0 & $i(v2) & ( ~ % 153.19/21.78 | (v1 = 0) | ~ (v0 = 0) | v2 = xa)) % 153.19/21.78 | % 153.19/21.78 | GROUND_INST: instantiating (mSortsB_02) with xu, all_36_0, xa, simplifying % 153.19/21.78 | with (18), (34), (36) gives: % 153.19/21.78 | (136) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_36_0) = % 153.19/21.78 | v1 & aElement0(xu) = v0 & aElement0(xa) = v2 & ( ~ (v1 = 0) | ~ % 153.19/21.78 | (v0 = 0) | v2 = 0)) % 153.19/21.78 | % 153.19/21.78 | GROUND_INST: instantiating (63) with xu, 0, all_43_1, all_43_0, simplifying % 153.19/21.78 | with (18), (54), (55), (56), (57) gives: % 153.19/21.78 | (137) xu = sz00 | ? [v0: any] : ? [v1: int] : (( ~ (v1 = 0) & iLess0(v0, % 153.19/21.78 | all_43_2) = v1 & sbrdtbr0(xu) = v0 & $i(v0)) | % 153.19/21.78 | (aElementOf0(all_43_0, all_43_3) = v1 & aElementOf0(all_43_1, % 153.19/21.78 | all_43_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0)))) % 153.19/21.78 | % 153.19/21.78 | GROUND_INST: instantiating (5) with xI, xu, all_34_0, simplifying with (18), % 153.19/21.78 | (29), (30), (57), (77), (119) gives: % 153.19/21.78 | (138) ? [v0: $i] : (aElementOf0(v0, xI) = 0 & sdtasdt0(all_34_0, xu) = v0 % 153.19/21.78 | & $i(v0)) % 153.19/21.78 | % 153.19/21.78 | GROUND_INST: instantiating (6) with xu, all_43_2, simplifying with (18), (60) % 153.19/21.78 | gives: % 153.19/21.78 | (139) xu = sz00 | ? [v0: any] : ? [v1: any] : (aNaturalNumber0(all_43_2) % 153.19/21.78 | = v1 & aElement0(xu) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 153.19/21.78 | % 153.19/21.78 | GROUND_INST: instantiating (9) with xa, xu, 0, simplifying with (10), (18), % 153.19/21.78 | (20), (37) gives: % 153.19/21.78 | (140) ? [v0: any] : ? [v1: any] : (aDivisorOf0(xu, xa) = v0 & % 153.19/21.78 | aElement0(xu) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 153.19/21.78 | % 153.19/21.78 | GROUND_INST: instantiating (7) with xa, xu, simplifying with (10), (18), (20), % 153.19/21.78 | (37) gives: % 153.19/21.78 | (141) ? [v0: any] : ? [v1: any] : (aDivisorOf0(xu, xa) = v1 & % 153.19/21.78 | aElement0(xu) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 153.19/21.78 | % 153.19/21.78 | GROUND_INST: instantiating (85) with xu, 0, simplifying with (18), (37) gives: % 153.19/21.78 | (142) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? [v4: % 153.19/21.78 | any] : ? [v5: $i] : ? [v6: int] : ? [v7: $i] : (aDivisorOf0(xu, % 153.19/21.78 | xb) = v3 & aDivisorOf0(xu, xa) = v1 & doDivides0(xu, xc) = v4 & % 153.19/21.78 | doDivides0(xu, xb) = v2 & aElement0(xu) = v0 & $i(v5) & ((v7 = xc & % 153.19/21.78 | v6 = 0 & v4 = 0 & sdtasdt0(xu, v5) = xc & aElement0(v5) = 0) | % 153.19/21.78 | ( ~ (v3 = 0) & ~ (v2 = 0) & ! [v8: $i] : ( ~ (sdtasdt0(xu, v8) % 153.19/21.78 | = xb) | ~ $i(v8) | ? [v9: int] : ( ~ (v9 = 0) & % 153.19/21.78 | aElement0(v8) = v9)) & ! [v8: $i] : ( ~ (aElement0(v8) = % 153.19/21.78 | 0) | ~ $i(v8) | ? [v9: $i] : ( ~ (v9 = xb) & sdtasdt0(xu, % 153.19/21.78 | v8) = v9 & $i(v9)))) | ( ~ (v1 = 0) & ~ (v0 = 0)))) % 153.19/21.78 | % 153.19/21.78 | GROUND_INST: instantiating (9) with xb, xu, 0, simplifying with (11), (18), % 153.19/21.78 | (21), (38) gives: % 153.19/21.78 | (143) ? [v0: any] : ? [v1: any] : (aDivisorOf0(xu, xb) = v0 & % 153.19/21.78 | aElement0(xu) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 153.19/21.78 | % 153.19/21.78 | GROUND_INST: instantiating (7) with xb, xu, simplifying with (11), (18), (21), % 153.19/21.78 | (38) gives: % 153.19/21.78 | (144) ? [v0: any] : ? [v1: any] : (aDivisorOf0(xu, xb) = v1 & % 153.19/21.78 | aElement0(xu) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 153.19/21.78 | % 153.19/21.78 | GROUND_INST: instantiating (86) with xu, 0, simplifying with (18), (38) gives: % 153.19/21.79 | (145) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: % 153.19/21.79 | MultipleValueBool] : ? [v4: any] : ? [v5: $i] : ? [v6: int] : ? % 153.19/21.79 | [v7: $i] : (aDivisorOf0(xu, xb) = v3 & aDivisorOf0(xu, xa) = v2 & % 153.19/21.79 | doDivides0(xu, xc) = v4 & doDivides0(xu, xa) = v1 & aElement0(xu) = % 153.19/21.79 | v0 & $i(v5) & ((v7 = xc & v6 = 0 & v4 = 0 & sdtasdt0(xu, v5) = xc & % 153.19/21.79 | aElement0(v5) = 0) | ( ~ (v2 = 0) & ( ~ (v0 = 0) | ( ~ (v1 = 0) % 153.19/21.79 | & ! [v8: $i] : ( ~ (sdtasdt0(xu, v8) = xa) | ~ $i(v8) | % 153.19/21.79 | ? [v9: int] : ( ~ (v9 = 0) & aElement0(v8) = v9)) & ! % 153.19/21.79 | [v8: $i] : ( ~ (aElement0(v8) = 0) | ~ $i(v8) | ? [v9: % 153.19/21.79 | $i] : ( ~ (v9 = xa) & sdtasdt0(xu, v8) = v9 & % 153.19/21.79 | $i(v9)))))))) % 153.19/21.79 | % 153.19/21.79 | GROUND_INST: instantiating (87) with xu, 0, simplifying with (18), (39) gives: % 153.19/21.79 | (146) ? [v0: MultipleValueBool] : ? [v1: MultipleValueBool] : ? [v2: % 153.19/21.79 | any] : ? [v3: any] : ? [v4: any] : ? [v5: $i] : ? [v6: int] : % 153.19/21.79 | ? [v7: $i] : (aDivisorOf0(xu, xb) = v3 & doDivides0(xu, xc) = v4 & % 153.19/21.79 | doDivides0(xu, xb) = v2 & doDivides0(xu, xa) = v1 & aElement0(xu) = % 153.19/21.79 | v0 & $i(v5) & ((v7 = xc & v6 = 0 & v4 = 0 & sdtasdt0(xu, v5) = xc & % 153.19/21.79 | aElement0(v5) = 0) | ( ~ (v3 = 0) & ~ (v2 = 0) & ! [v8: $i] : % 153.19/21.79 | ( ~ (sdtasdt0(xu, v8) = xb) | ~ $i(v8) | ? [v9: int] : ( ~ % 153.19/21.79 | (v9 = 0) & aElement0(v8) = v9)) & ! [v8: $i] : ( ~ % 153.19/21.79 | (aElement0(v8) = 0) | ~ $i(v8) | ? [v9: $i] : ( ~ (v9 = xb) % 153.19/21.79 | & sdtasdt0(xu, v8) = v9 & $i(v9)))))) % 153.19/21.79 | % 153.19/21.79 | GROUND_INST: instantiating (8) with xb, xu, simplifying with (11), (18), (21), % 153.19/21.79 | (40) gives: % 153.19/21.79 | (147) doDivides0(xu, xb) = 0 & aElement0(xu) = 0 % 153.19/21.79 | % 153.19/21.79 | ALPHA: (147) implies: % 153.19/21.79 | (148) aElement0(xu) = 0 % 153.19/21.79 | % 153.19/21.79 | GROUND_INST: instantiating (88) with xu, 0, simplifying with (18), (40) gives: % 153.19/21.79 | (149) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: % 153.19/21.79 | MultipleValueBool] : ? [v4: any] : ? [v5: $i] : ? [v6: int] : ? % 153.19/21.79 | [v7: $i] : (aDivisorOf0(xu, xa) = v2 & doDivides0(xu, xc) = v4 & % 153.19/21.79 | doDivides0(xu, xb) = v3 & doDivides0(xu, xa) = v1 & aElement0(xu) = % 153.19/21.79 | v0 & $i(v5) & ((v7 = xc & v6 = 0 & v4 = 0 & sdtasdt0(xu, v5) = xc & % 153.19/21.79 | aElement0(v5) = 0) | ( ~ (v2 = 0) & ( ~ (v0 = 0) | ( ~ (v1 = 0) % 153.19/21.79 | & ! [v8: $i] : ( ~ (sdtasdt0(xu, v8) = xa) | ~ $i(v8) | % 153.19/21.79 | ? [v9: int] : ( ~ (v9 = 0) & aElement0(v8) = v9)) & ! % 153.19/21.79 | [v8: $i] : ( ~ (aElement0(v8) = 0) | ~ $i(v8) | ? [v9: % 153.19/21.79 | $i] : ( ~ (v9 = xa) & sdtasdt0(xu, v8) = v9 & % 153.19/21.79 | $i(v9)))))))) % 153.19/21.79 | % 153.19/21.79 | DELTA: instantiating (138) with fresh symbol all_114_0 gives: % 153.19/21.79 | (150) aElementOf0(all_114_0, xI) = 0 & sdtasdt0(all_34_0, xu) = all_114_0 & % 153.19/21.79 | $i(all_114_0) % 153.19/21.79 | % 153.19/21.79 | ALPHA: (150) implies: % 153.19/21.79 | (151) sdtasdt0(all_34_0, xu) = all_114_0 % 153.19/21.79 | (152) aElementOf0(all_114_0, xI) = 0 % 153.19/21.79 | % 153.19/21.79 | DELTA: instantiating (144) with fresh symbols all_358_0, all_358_1 gives: % 153.19/21.79 | (153) aDivisorOf0(xu, xb) = all_358_0 & aElement0(xu) = all_358_1 & ( ~ % 153.19/21.79 | (all_358_1 = 0) | all_358_0 = 0) % 153.19/21.79 | % 153.19/21.79 | ALPHA: (153) implies: % 153.19/21.79 | (154) aElement0(xu) = all_358_1 % 153.19/21.79 | % 153.19/21.79 | DELTA: instantiating (143) with fresh symbols all_360_0, all_360_1 gives: % 153.19/21.79 | (155) aDivisorOf0(xu, xb) = all_360_1 & aElement0(xu) = all_360_0 & ( ~ % 153.19/21.79 | (all_360_1 = 0) | all_360_0 = 0) % 153.19/21.79 | % 153.19/21.79 | ALPHA: (155) implies: % 153.19/21.79 | (156) aElement0(xu) = all_360_0 % 153.19/21.79 | % 153.19/21.79 | DELTA: instantiating (141) with fresh symbols all_362_0, all_362_1 gives: % 153.19/21.79 | (157) aDivisorOf0(xu, xa) = all_362_0 & aElement0(xu) = all_362_1 & ( ~ % 153.19/21.79 | (all_362_1 = 0) | all_362_0 = 0) % 153.19/21.79 | % 153.19/21.79 | ALPHA: (157) implies: % 153.19/21.79 | (158) aElement0(xu) = all_362_1 % 153.19/21.79 | % 153.19/21.79 | DELTA: instantiating (140) with fresh symbols all_724_0, all_724_1 gives: % 153.19/21.79 | (159) aDivisorOf0(xu, xa) = all_724_1 & aElement0(xu) = all_724_0 & ( ~ % 153.19/21.79 | (all_724_1 = 0) | all_724_0 = 0) % 153.19/21.79 | % 153.19/21.79 | ALPHA: (159) implies: % 153.19/21.79 | (160) aElement0(xu) = all_724_0 % 153.19/21.79 | % 153.19/21.79 | DELTA: instantiating (136) with fresh symbols all_1055_0, all_1055_1, % 153.19/21.79 | all_1055_2 gives: % 153.19/21.79 | (161) aElement0(all_36_0) = all_1055_1 & aElement0(xu) = all_1055_2 & % 153.19/21.79 | aElement0(xa) = all_1055_0 & ( ~ (all_1055_1 = 0) | ~ (all_1055_2 = % 153.19/21.79 | 0) | all_1055_0 = 0) % 153.19/21.79 | % 153.19/21.79 | ALPHA: (161) implies: % 153.19/21.79 | (162) aElement0(xu) = all_1055_2 % 153.19/21.79 | % 153.19/21.79 | DELTA: instantiating (131) with fresh symbols all_1068_0, all_1068_1, % 153.19/21.79 | all_1068_2 gives: % 153.19/21.79 | (163) aElement0(all_36_1) = all_1068_1 & aElement0(xu) = all_1068_2 & % 153.19/21.79 | aElement0(xb) = all_1068_0 & ( ~ (all_1068_1 = 0) | ~ (all_1068_2 = % 153.19/21.79 | 0) | all_1068_0 = 0) % 153.19/21.79 | % 153.19/21.79 | ALPHA: (163) implies: % 153.19/21.79 | (164) aElement0(xu) = all_1068_2 % 153.19/21.79 | % 153.19/21.79 | DELTA: instantiating (126) with fresh symbols all_1070_0, all_1070_1, % 153.19/21.79 | all_1070_2 gives: % 153.19/21.79 | (165) aElement0(all_34_0) = all_1070_1 & aElement0(xu) = all_1070_2 & % 153.19/21.79 | aElement0(xc) = all_1070_0 & ( ~ (all_1070_1 = 0) | ~ (all_1070_2 = % 153.19/21.79 | 0) | all_1070_0 = 0) % 153.19/21.79 | % 153.19/21.79 | ALPHA: (165) implies: % 153.19/21.79 | (166) aElement0(xu) = all_1070_2 % 153.19/21.79 | % 153.19/21.79 | DELTA: instantiating (120) with fresh symbols all_1076_0, all_1076_1, % 153.19/21.79 | all_1076_2 gives: % 153.19/21.79 | (167) aElement0(all_43_0) = all_1076_1 & aElement0(all_43_1) = all_1076_2 & % 153.19/21.79 | aElement0(xu) = all_1076_0 & ( ~ (all_1076_1 = 0) | ~ (all_1076_2 = % 153.19/21.79 | 0) | all_1076_0 = 0) % 153.19/21.79 | % 153.19/21.79 | ALPHA: (167) implies: % 153.19/21.79 | (168) aElement0(xu) = all_1076_0 % 153.19/21.79 | % 153.19/21.79 | DELTA: instantiating (134) with fresh symbols all_1094_0, all_1094_1, % 153.19/21.79 | all_1094_2 gives: % 153.19/21.79 | (169) sdtasdt0(all_36_0, xu) = all_1094_0 & aElement0(all_36_0) = % 153.19/21.79 | all_1094_2 & aElement0(xu) = all_1094_1 & $i(all_1094_0) & ( ~ % 153.19/21.79 | (all_1094_1 = 0) | ~ (all_1094_2 = 0) | all_1094_0 = xa) % 153.19/21.79 | % 153.19/21.79 | ALPHA: (169) implies: % 153.19/21.79 | (170) aElement0(xu) = all_1094_1 % 153.19/21.79 | % 153.19/21.79 | DELTA: instantiating (129) with fresh symbols all_1104_0, all_1104_1, % 153.19/21.79 | all_1104_2 gives: % 153.19/21.79 | (171) sdtasdt0(all_36_1, xu) = all_1104_0 & aElement0(all_36_1) = % 153.19/21.79 | all_1104_2 & aElement0(xu) = all_1104_1 & $i(all_1104_0) & ( ~ % 153.19/21.79 | (all_1104_1 = 0) | ~ (all_1104_2 = 0) | all_1104_0 = xb) % 153.19/21.79 | % 153.19/21.79 | ALPHA: (171) implies: % 153.19/21.79 | (172) aElement0(xu) = all_1104_1 % 153.19/21.79 | % 153.19/21.79 | DELTA: instantiating (124) with fresh symbols all_1106_0, all_1106_1, % 153.19/21.79 | all_1106_2 gives: % 153.19/21.79 | (173) sdtasdt0(all_34_0, xu) = all_1106_0 & aElement0(all_34_0) = % 153.19/21.79 | all_1106_2 & aElement0(xu) = all_1106_1 & $i(all_1106_0) & ( ~ % 153.19/21.79 | (all_1106_1 = 0) | ~ (all_1106_2 = 0) | all_1106_0 = xc) % 153.19/21.79 | % 153.19/21.79 | ALPHA: (173) implies: % 153.19/21.79 | (174) aElement0(xu) = all_1106_1 % 153.19/21.79 | (175) aElement0(all_34_0) = all_1106_2 % 153.19/21.79 | (176) sdtasdt0(all_34_0, xu) = all_1106_0 % 153.19/21.80 | (177) ~ (all_1106_1 = 0) | ~ (all_1106_2 = 0) | all_1106_0 = xc % 153.19/21.80 | % 153.19/21.80 | DELTA: instantiating (135) with fresh symbols all_1108_0, all_1108_1, % 153.19/21.80 | all_1108_2 gives: % 153.19/21.80 | (178) sdtasdt0(all_36_0, xu) = all_1108_0 & aElement0(all_36_0) = % 153.19/21.80 | all_1108_1 & aElement0(xu) = all_1108_2 & $i(all_1108_0) & ( ~ % 153.19/21.80 | (all_1108_1 = 0) | ~ (all_1108_2 = 0) | all_1108_0 = xa) % 153.19/21.80 | % 153.19/21.80 | ALPHA: (178) implies: % 153.19/21.80 | (179) aElement0(xu) = all_1108_2 % 153.19/21.80 | % 153.19/21.80 | DELTA: instantiating (130) with fresh symbols all_1120_0, all_1120_1, % 153.19/21.80 | all_1120_2 gives: % 153.19/21.80 | (180) sdtasdt0(all_36_1, xu) = all_1120_0 & aElement0(all_36_1) = % 153.19/21.80 | all_1120_1 & aElement0(xu) = all_1120_2 & $i(all_1120_0) & ( ~ % 153.19/21.80 | (all_1120_1 = 0) | ~ (all_1120_2 = 0) | all_1120_0 = xb) % 153.19/21.80 | % 153.19/21.80 | ALPHA: (180) implies: % 153.19/21.80 | (181) aElement0(xu) = all_1120_2 % 153.19/21.80 | % 153.19/21.80 | DELTA: instantiating (125) with fresh symbols all_1122_0, all_1122_1, % 153.19/21.80 | all_1122_2 gives: % 153.19/21.80 | (182) sdtasdt0(all_34_0, xu) = all_1122_0 & aElement0(all_34_0) = % 153.19/21.80 | all_1122_1 & aElement0(xu) = all_1122_2 & $i(all_1122_0) & ( ~ % 153.19/21.80 | (all_1122_1 = 0) | ~ (all_1122_2 = 0) | all_1122_0 = xc) % 153.19/21.80 | % 153.19/21.80 | ALPHA: (182) implies: % 153.19/21.80 | (183) aElement0(xu) = all_1122_2 % 153.19/21.80 | (184) aElement0(all_34_0) = all_1122_1 % 153.19/21.80 | (185) sdtasdt0(all_34_0, xu) = all_1122_0 % 153.19/21.80 | % 153.19/21.80 | DELTA: instantiating (128) with fresh symbols all_1164_0, all_1164_1, % 153.19/21.80 | all_1164_2, all_1164_3, all_1164_4 gives: % 153.19/21.80 | (186) sdtasdt0(all_36_1, all_38_3) = all_1164_1 & sdtasdt0(xu, all_1164_1) % 153.19/21.80 | = all_1164_0 & aElement0(all_38_3) = all_1164_2 & aElement0(all_36_1) % 153.19/21.80 | = all_1164_3 & aElement0(xu) = all_1164_4 & $i(all_1164_0) & % 153.19/21.80 | $i(all_1164_1) & ( ~ (all_1164_2 = 0) | ~ (all_1164_3 = 0) | ~ % 153.19/21.80 | (all_1164_4 = 0) | all_1164_0 = xb) % 153.19/21.80 | % 153.19/21.80 | ALPHA: (186) implies: % 153.19/21.80 | (187) aElement0(xu) = all_1164_4 % 153.19/21.80 | % 153.19/21.80 | DELTA: instantiating (127) with fresh symbols all_1186_0, all_1186_1, % 153.19/21.80 | all_1186_2, all_1186_3, all_1186_4 gives: % 153.19/21.80 | (188) sdtasdt0(all_36_1, all_38_2) = all_1186_1 & sdtasdt0(xu, all_1186_1) % 153.19/21.80 | = all_1186_0 & aElement0(all_38_2) = all_1186_2 & aElement0(all_36_1) % 153.19/21.80 | = all_1186_3 & aElement0(xu) = all_1186_4 & $i(all_1186_0) & % 153.19/21.80 | $i(all_1186_1) & ( ~ (all_1186_2 = 0) | ~ (all_1186_3 = 0) | ~ % 153.19/21.80 | (all_1186_4 = 0) | all_1186_0 = sz00) % 153.19/21.80 | % 153.19/21.80 | ALPHA: (188) implies: % 153.19/21.80 | (189) aElement0(xu) = all_1186_4 % 153.19/21.80 | % 153.19/21.80 | DELTA: instantiating (133) with fresh symbols all_1200_0, all_1200_1, % 153.19/21.80 | all_1200_2, all_1200_3, all_1200_4 gives: % 153.19/21.80 | (190) sdtasdt0(all_36_0, all_38_1) = all_1200_1 & sdtasdt0(xu, all_1200_1) % 153.19/21.80 | = all_1200_0 & aElement0(all_38_1) = all_1200_2 & aElement0(all_36_0) % 153.19/21.80 | = all_1200_3 & aElement0(xu) = all_1200_4 & $i(all_1200_0) & % 153.19/21.80 | $i(all_1200_1) & ( ~ (all_1200_2 = 0) | ~ (all_1200_3 = 0) | ~ % 153.19/21.80 | (all_1200_4 = 0) | all_1200_0 = xa) % 153.19/21.80 | % 153.19/21.80 | ALPHA: (190) implies: % 153.19/21.80 | (191) aElement0(xu) = all_1200_4 % 153.19/21.80 | % 153.19/21.80 | DELTA: instantiating (132) with fresh symbols all_1202_0, all_1202_1, % 153.19/21.80 | all_1202_2, all_1202_3, all_1202_4 gives: % 153.19/21.80 | (192) sdtasdt0(all_36_0, all_38_0) = all_1202_1 & sdtasdt0(xu, all_1202_1) % 153.19/21.80 | = all_1202_0 & aElement0(all_38_0) = all_1202_2 & aElement0(all_36_0) % 153.19/21.80 | = all_1202_3 & aElement0(xu) = all_1202_4 & $i(all_1202_0) & % 153.19/21.80 | $i(all_1202_1) & ( ~ (all_1202_2 = 0) | ~ (all_1202_3 = 0) | ~ % 153.19/21.80 | (all_1202_4 = 0) | all_1202_0 = sz00) % 153.19/21.80 | % 153.19/21.80 | ALPHA: (192) implies: % 153.19/21.80 | (193) aElement0(xu) = all_1202_4 % 153.19/21.80 | % 153.19/21.80 | DELTA: instantiating (122) with fresh symbols all_1314_0, all_1314_1, % 153.19/21.80 | all_1314_2, all_1314_3, all_1314_4 gives: % 153.19/21.80 | (194) sdtasdt0(all_34_0, all_55_1) = all_1314_1 & sdtasdt0(xu, all_1314_1) % 153.19/21.80 | = all_1314_0 & aElement0(all_55_1) = all_1314_2 & aElement0(all_34_0) % 153.19/21.80 | = all_1314_3 & aElement0(xu) = all_1314_4 & $i(all_1314_0) & % 153.19/21.80 | $i(all_1314_1) & ( ~ (all_1314_2 = 0) | ~ (all_1314_3 = 0) | ~ % 153.19/21.80 | (all_1314_4 = 0) | all_1314_0 = xb) % 153.19/21.80 | % 153.19/21.80 | ALPHA: (194) implies: % 153.19/21.80 | (195) aElement0(xu) = all_1314_4 % 153.19/21.80 | (196) aElement0(all_34_0) = all_1314_3 % 153.19/21.80 | % 153.19/21.80 | DELTA: instantiating (121) with fresh symbols all_1328_0, all_1328_1, % 153.19/21.80 | all_1328_2, all_1328_3, all_1328_4 gives: % 153.19/21.80 | (197) sdtasdt0(all_34_0, all_55_0) = all_1328_1 & sdtasdt0(xu, all_1328_1) % 153.19/21.80 | = all_1328_0 & aElement0(all_55_0) = all_1328_2 & aElement0(all_34_0) % 153.19/21.80 | = all_1328_3 & aElement0(xu) = all_1328_4 & $i(all_1328_0) & % 153.19/21.80 | $i(all_1328_1) & ( ~ (all_1328_2 = 0) | ~ (all_1328_3 = 0) | ~ % 153.19/21.80 | (all_1328_4 = 0) | all_1328_0 = xa) % 153.19/21.80 | % 153.19/21.80 | ALPHA: (197) implies: % 153.19/21.80 | (198) aElement0(xu) = all_1328_4 % 153.19/21.80 | (199) aElement0(all_34_0) = all_1328_3 % 153.19/21.80 | % 153.19/21.80 | DELTA: instantiating (146) with fresh symbols all_1802_0, all_1802_1, % 153.19/21.80 | all_1802_2, all_1802_3, all_1802_4, all_1802_5, all_1802_6, all_1802_7 % 153.19/21.80 | gives: % 153.19/21.80 | (200) aDivisorOf0(xu, xb) = all_1802_4 & doDivides0(xu, xc) = all_1802_3 & % 153.19/21.80 | doDivides0(xu, xb) = all_1802_5 & doDivides0(xu, xa) = all_1802_6 & % 153.19/21.80 | aElement0(xu) = all_1802_7 & $i(all_1802_2) & ((all_1802_0 = xc & % 153.19/21.80 | all_1802_1 = 0 & all_1802_3 = 0 & sdtasdt0(xu, all_1802_2) = xc & % 153.19/21.80 | aElement0(all_1802_2) = 0) | ( ~ (all_1802_4 = 0) & ~ % 153.19/21.80 | (all_1802_5 = 0) & ! [v0: $i] : ( ~ (sdtasdt0(xu, v0) = xb) | ~ % 153.19/21.80 | $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & aElement0(v0) = v1)) & % 153.19/21.80 | ! [v0: $i] : ( ~ (aElement0(v0) = 0) | ~ $i(v0) | ? [v1: $i] : % 153.19/21.80 | ( ~ (v1 = xb) & sdtasdt0(xu, v0) = v1 & $i(v1))))) % 153.19/21.80 | % 153.19/21.80 | ALPHA: (200) implies: % 153.19/21.80 | (201) aElement0(xu) = all_1802_7 % 153.19/21.80 | % 153.19/21.80 | DELTA: instantiating (123) with fresh symbols all_1804_0, all_1804_1, % 153.19/21.80 | all_1804_2, all_1804_3, all_1804_4, all_1804_5, all_1804_6, all_1804_7, % 153.19/21.80 | all_1804_8, all_1804_9 gives: % 153.19/21.80 | (202) sdtasdt0(all_43_0, all_34_0) = all_1804_1 & sdtasdt0(all_43_1, % 153.19/21.80 | all_34_0) = all_1804_2 & sdtasdt0(all_34_0, all_43_0) = all_1804_4 % 153.19/21.80 | & sdtasdt0(all_34_0, all_43_1) = all_1804_5 & sdtasdt0(all_34_0, xu) % 153.19/21.80 | = all_1804_6 & sdtpldt0(all_1804_2, all_1804_1) = all_1804_0 & % 153.19/21.80 | sdtpldt0(all_1804_5, all_1804_4) = all_1804_3 & aElement0(all_43_0) = % 153.19/21.80 | all_1804_7 & aElement0(all_43_1) = all_1804_8 & aElement0(all_34_0) = % 153.19/21.80 | all_1804_9 & $i(all_1804_0) & $i(all_1804_1) & $i(all_1804_2) & % 153.19/21.80 | $i(all_1804_3) & $i(all_1804_4) & $i(all_1804_5) & $i(all_1804_6) & ( % 153.19/21.80 | ~ (all_1804_7 = 0) | ~ (all_1804_8 = 0) | ~ (all_1804_9 = 0) | % 153.19/21.80 | (all_1804_0 = xc & all_1804_3 = all_1804_6)) % 153.19/21.80 | % 153.19/21.80 | ALPHA: (202) implies: % 153.19/21.80 | (203) aElement0(all_34_0) = all_1804_9 % 153.19/21.80 | (204) sdtasdt0(all_34_0, xu) = all_1804_6 % 153.19/21.80 | % 153.19/21.80 | DELTA: instantiating (145) with fresh symbols all_1838_0, all_1838_1, % 153.19/21.80 | all_1838_2, all_1838_3, all_1838_4, all_1838_5, all_1838_6, all_1838_7 % 153.19/21.80 | gives: % 153.19/21.81 | (205) aDivisorOf0(xu, xb) = all_1838_4 & aDivisorOf0(xu, xa) = all_1838_5 & % 153.19/21.81 | doDivides0(xu, xc) = all_1838_3 & doDivides0(xu, xa) = all_1838_6 & % 153.19/21.81 | aElement0(xu) = all_1838_7 & $i(all_1838_2) & ((all_1838_0 = xc & % 153.19/21.81 | all_1838_1 = 0 & all_1838_3 = 0 & sdtasdt0(xu, all_1838_2) = xc & % 153.19/21.81 | aElement0(all_1838_2) = 0) | ( ~ (all_1838_5 = 0) & ( ~ % 153.19/21.81 | (all_1838_7 = 0) | ( ~ (all_1838_6 = 0) & ! [v0: $i] : ( ~ % 153.19/21.81 | (sdtasdt0(xu, v0) = xa) | ~ $i(v0) | ? [v1: int] : ( ~ % 153.19/21.81 | (v1 = 0) & aElement0(v0) = v1)) & ! [v0: $i] : ( ~ % 153.19/21.81 | (aElement0(v0) = 0) | ~ $i(v0) | ? [v1: $i] : ( ~ (v1 = % 153.19/21.81 | xa) & sdtasdt0(xu, v0) = v1 & $i(v1))))))) % 153.19/21.81 | % 153.19/21.81 | ALPHA: (205) implies: % 153.19/21.81 | (206) aElement0(xu) = all_1838_7 % 153.19/21.81 | % 153.19/21.81 | DELTA: instantiating (149) with fresh symbols all_1846_0, all_1846_1, % 153.19/21.81 | all_1846_2, all_1846_3, all_1846_4, all_1846_5, all_1846_6, all_1846_7 % 153.19/21.81 | gives: % 153.19/21.81 | (207) aDivisorOf0(xu, xa) = all_1846_5 & doDivides0(xu, xc) = all_1846_3 & % 153.19/21.81 | doDivides0(xu, xb) = all_1846_4 & doDivides0(xu, xa) = all_1846_6 & % 153.19/21.81 | aElement0(xu) = all_1846_7 & $i(all_1846_2) & ((all_1846_0 = xc & % 153.19/21.81 | all_1846_1 = 0 & all_1846_3 = 0 & sdtasdt0(xu, all_1846_2) = xc & % 153.19/21.81 | aElement0(all_1846_2) = 0) | ( ~ (all_1846_5 = 0) & ( ~ % 153.19/21.81 | (all_1846_7 = 0) | ( ~ (all_1846_6 = 0) & ! [v0: $i] : ( ~ % 153.19/21.81 | (sdtasdt0(xu, v0) = xa) | ~ $i(v0) | ? [v1: int] : ( ~ % 153.19/21.81 | (v1 = 0) & aElement0(v0) = v1)) & ! [v0: $i] : ( ~ % 153.19/21.81 | (aElement0(v0) = 0) | ~ $i(v0) | ? [v1: $i] : ( ~ (v1 = % 153.19/21.81 | xa) & sdtasdt0(xu, v0) = v1 & $i(v1))))))) % 153.19/21.81 | % 153.19/21.81 | ALPHA: (207) implies: % 153.19/21.81 | (208) aElement0(xu) = all_1846_7 % 153.19/21.81 | % 153.19/21.81 | DELTA: instantiating (142) with fresh symbols all_2026_0, all_2026_1, % 153.19/21.81 | all_2026_2, all_2026_3, all_2026_4, all_2026_5, all_2026_6, all_2026_7 % 153.19/21.81 | gives: % 153.19/21.81 | (209) aDivisorOf0(xu, xb) = all_2026_4 & aDivisorOf0(xu, xa) = all_2026_6 & % 153.19/21.81 | doDivides0(xu, xc) = all_2026_3 & doDivides0(xu, xb) = all_2026_5 & % 153.19/21.81 | aElement0(xu) = all_2026_7 & $i(all_2026_2) & ((all_2026_0 = xc & % 153.19/21.81 | all_2026_1 = 0 & all_2026_3 = 0 & sdtasdt0(xu, all_2026_2) = xc & % 153.19/21.81 | aElement0(all_2026_2) = 0) | ( ~ (all_2026_4 = 0) & ~ % 153.19/21.81 | (all_2026_5 = 0) & ! [v0: $i] : ( ~ (sdtasdt0(xu, v0) = xb) | ~ % 153.19/21.81 | $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & aElement0(v0) = v1)) & % 153.19/21.81 | ! [v0: $i] : ( ~ (aElement0(v0) = 0) | ~ $i(v0) | ? [v1: $i] : % 153.19/21.81 | ( ~ (v1 = xb) & sdtasdt0(xu, v0) = v1 & $i(v1)))) | ( ~ % 153.19/21.81 | (all_2026_6 = 0) & ~ (all_2026_7 = 0))) % 153.19/21.81 | % 153.19/21.81 | ALPHA: (209) implies: % 153.19/21.81 | (210) aElement0(xu) = all_2026_7 % 153.19/21.81 | % 153.19/21.81 | BETA: splitting (137) gives: % 153.19/21.81 | % 153.19/21.81 | Case 1: % 153.19/21.81 | | % 153.19/21.81 | | (211) xu = sz00 % 153.19/21.81 | | % 153.19/21.81 | | REDUCE: (53), (211) imply: % 153.19/21.81 | | (212) $false % 153.19/21.81 | | % 153.19/21.81 | | CLOSE: (212) is inconsistent. % 153.19/21.81 | | % 153.19/21.81 | Case 2: % 153.19/21.81 | | % 153.19/21.81 | | (213) ? [v0: any] : ? [v1: int] : (( ~ (v1 = 0) & iLess0(v0, all_43_2) % 153.19/21.81 | | = v1 & sbrdtbr0(xu) = v0 & $i(v0)) | (aElementOf0(all_43_0, % 153.19/21.81 | | all_43_3) = v1 & aElementOf0(all_43_1, all_43_4) = v0 & ( ~ % 153.19/21.81 | | (v1 = 0) | ~ (v0 = 0)))) % 153.19/21.81 | | % 153.19/21.81 | | DELTA: instantiating (213) with fresh symbols all_2109_0, all_2109_1 gives: % 153.19/21.81 | | (214) ( ~ (all_2109_0 = 0) & iLess0(all_2109_1, all_43_2) = all_2109_0 & % 153.19/21.81 | | sbrdtbr0(xu) = all_2109_1 & $i(all_2109_1)) | % 153.19/21.81 | | (aElementOf0(all_43_0, all_43_3) = all_2109_0 & % 153.19/21.81 | | aElementOf0(all_43_1, all_43_4) = all_2109_1 & ( ~ (all_2109_0 = % 153.19/21.81 | | 0) | ~ (all_2109_1 = 0))) % 153.19/21.81 | | % 153.19/21.81 | | BETA: splitting (139) gives: % 153.19/21.81 | | % 153.19/21.81 | | Case 1: % 153.19/21.81 | | | % 153.19/21.81 | | | (215) xu = sz00 % 153.19/21.81 | | | % 153.19/21.81 | | | REDUCE: (53), (215) imply: % 153.19/21.81 | | | (216) $false % 153.19/21.81 | | | % 153.19/21.81 | | | CLOSE: (216) is inconsistent. % 153.19/21.81 | | | % 153.19/21.81 | | Case 2: % 153.19/21.81 | | | % 153.19/21.81 | | | (217) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(all_43_2) = v1 & % 153.19/21.81 | | | aElement0(xu) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 153.19/21.81 | | | % 153.19/21.81 | | | DELTA: instantiating (217) with fresh symbols all_2123_0, all_2123_1 % 153.19/21.81 | | | gives: % 153.19/21.81 | | | (218) aNaturalNumber0(all_43_2) = all_2123_0 & aElement0(xu) = % 153.19/21.81 | | | all_2123_1 & ( ~ (all_2123_1 = 0) | all_2123_0 = 0) % 153.19/21.81 | | | % 153.19/21.81 | | | ALPHA: (218) implies: % 153.19/21.81 | | | (219) aElement0(xu) = all_2123_1 % 153.19/21.81 | | | % 153.19/21.81 | | | BETA: splitting (214) gives: % 153.19/21.81 | | | % 153.19/21.81 | | | Case 1: % 153.19/21.81 | | | | % 153.19/21.81 | | | | % 153.19/21.81 | | | | GROUND_INST: instantiating (23) with all_724_0, all_1076_0, xu, % 153.19/21.81 | | | | simplifying with (160), (168) gives: % 153.19/21.81 | | | | (220) all_1076_0 = all_724_0 % 153.19/21.81 | | | | % 153.19/21.81 | | | | GROUND_INST: instantiating (23) with 0, all_1076_0, xu, simplifying with % 153.19/21.81 | | | | (148), (168) gives: % 153.19/21.81 | | | | (221) all_1076_0 = 0 % 153.19/21.81 | | | | % 153.19/21.81 | | | | GROUND_INST: instantiating (23) with all_1055_2, all_1094_1, xu, % 153.19/21.81 | | | | simplifying with (162), (170) gives: % 153.19/21.81 | | | | (222) all_1094_1 = all_1055_2 % 153.19/21.81 | | | | % 153.19/21.81 | | | | GROUND_INST: instantiating (23) with all_1094_1, all_1106_1, xu, % 153.19/21.81 | | | | simplifying with (170), (174) gives: % 153.19/21.81 | | | | (223) all_1106_1 = all_1094_1 % 153.19/21.81 | | | | % 153.19/21.81 | | | | GROUND_INST: instantiating (23) with all_1068_2, all_1106_1, xu, % 153.19/21.81 | | | | simplifying with (164), (174) gives: % 153.19/21.81 | | | | (224) all_1106_1 = all_1068_2 % 153.19/21.81 | | | | % 153.19/21.81 | | | | GROUND_INST: instantiating (23) with all_724_0, all_1106_1, xu, % 153.19/21.81 | | | | simplifying with (160), (174) gives: % 153.19/21.81 | | | | (225) all_1106_1 = all_724_0 % 153.19/21.81 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_362_1, all_1106_1, xu, % 153.19/21.82 | | | | simplifying with (158), (174) gives: % 153.19/21.82 | | | | (226) all_1106_1 = all_362_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1068_2, all_1120_2, xu, % 153.19/21.82 | | | | simplifying with (164), (181) gives: % 153.19/21.82 | | | | (227) all_1120_2 = all_1068_2 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_362_1, all_1164_4, xu, % 153.19/21.82 | | | | simplifying with (158), (187) gives: % 153.19/21.82 | | | | (228) all_1164_4 = all_362_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1164_4, all_1186_4, xu, % 153.19/21.82 | | | | simplifying with (187), (189) gives: % 153.19/21.82 | | | | (229) all_1186_4 = all_1164_4 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1104_1, all_1186_4, xu, % 153.19/21.82 | | | | simplifying with (172), (189) gives: % 153.19/21.82 | | | | (230) all_1186_4 = all_1104_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1120_2, all_1200_4, xu, % 153.19/21.82 | | | | simplifying with (181), (191) gives: % 153.19/21.82 | | | | (231) all_1200_4 = all_1120_2 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1120_2, all_1202_4, xu, % 153.19/21.82 | | | | simplifying with (181), (193) gives: % 153.19/21.82 | | | | (232) all_1202_4 = all_1120_2 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1108_2, all_1202_4, xu, % 153.19/21.82 | | | | simplifying with (179), (193) gives: % 153.19/21.82 | | | | (233) all_1202_4 = all_1108_2 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1106_1, all_1314_4, xu, % 153.19/21.82 | | | | simplifying with (174), (195) gives: % 153.19/21.82 | | | | (234) all_1314_4 = all_1106_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1070_2, all_1314_4, xu, % 153.19/21.82 | | | | simplifying with (166), (195) gives: % 153.19/21.82 | | | | (235) all_1314_4 = all_1070_2 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1164_4, all_1802_7, xu, % 153.19/21.82 | | | | simplifying with (187), (201) gives: % 153.19/21.82 | | | | (236) all_1802_7 = all_1164_4 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1122_2, all_1802_7, xu, % 153.19/21.82 | | | | simplifying with (183), (201) gives: % 153.19/21.82 | | | | (237) all_1802_7 = all_1122_2 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1164_4, all_1838_7, xu, % 153.19/21.82 | | | | simplifying with (187), (206) gives: % 153.19/21.82 | | | | (238) all_1838_7 = all_1164_4 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1802_7, all_1846_7, xu, % 153.19/21.82 | | | | simplifying with (201), (208) gives: % 153.19/21.82 | | | | (239) all_1846_7 = all_1802_7 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1328_4, all_1846_7, xu, % 153.19/21.82 | | | | simplifying with (198), (208) gives: % 153.19/21.82 | | | | (240) all_1846_7 = all_1328_4 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1838_7, all_2026_7, xu, % 153.19/21.82 | | | | simplifying with (206), (210) gives: % 153.19/21.82 | | | | (241) all_2026_7 = all_1838_7 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_358_1, all_2026_7, xu, % 153.19/21.82 | | | | simplifying with (154), (210) gives: % 153.19/21.82 | | | | (242) all_2026_7 = all_358_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1200_4, all_2123_1, xu, % 153.19/21.82 | | | | simplifying with (191), (219) gives: % 153.19/21.82 | | | | (243) all_2123_1 = all_1200_4 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_360_0, all_2123_1, xu, % 153.19/21.82 | | | | simplifying with (156), (219) gives: % 153.19/21.82 | | | | (244) all_2123_1 = all_360_0 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1122_1, all_1328_3, all_34_0, % 153.19/21.82 | | | | simplifying with (184), (199) gives: % 153.19/21.82 | | | | (245) all_1328_3 = all_1122_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1106_2, all_1328_3, all_34_0, % 153.19/21.82 | | | | simplifying with (175), (199) gives: % 153.19/21.82 | | | | (246) all_1328_3 = all_1106_2 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with 0, all_1804_9, all_34_0, % 153.19/21.82 | | | | simplifying with (30), (203) gives: % 153.19/21.82 | | | | (247) all_1804_9 = 0 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1314_3, all_1804_9, all_34_0, % 153.19/21.82 | | | | simplifying with (196), (203) gives: % 153.19/21.82 | | | | (248) all_1804_9 = all_1314_3 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (23) with all_1122_1, all_1804_9, all_34_0, % 153.19/21.82 | | | | simplifying with (184), (203) gives: % 153.19/21.82 | | | | (249) all_1804_9 = all_1122_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (25) with all_1122_0, all_1804_6, xu, % 153.19/21.82 | | | | all_34_0, simplifying with (185), (204) gives: % 153.19/21.82 | | | | (250) all_1804_6 = all_1122_0 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (25) with all_1106_0, all_1804_6, xu, % 153.19/21.82 | | | | all_34_0, simplifying with (176), (204) gives: % 153.19/21.82 | | | | (251) all_1804_6 = all_1106_0 % 153.19/21.82 | | | | % 153.19/21.82 | | | | GROUND_INST: instantiating (25) with all_114_0, all_1804_6, xu, % 153.19/21.82 | | | | all_34_0, simplifying with (151), (204) gives: % 153.19/21.82 | | | | (252) all_1804_6 = all_114_0 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (243), (244) imply: % 153.19/21.82 | | | | (253) all_1200_4 = all_360_0 % 153.19/21.82 | | | | % 153.19/21.82 | | | | SIMP: (253) implies: % 153.19/21.82 | | | | (254) all_1200_4 = all_360_0 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (241), (242) imply: % 153.19/21.82 | | | | (255) all_1838_7 = all_358_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | SIMP: (255) implies: % 153.19/21.82 | | | | (256) all_1838_7 = all_358_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (239), (240) imply: % 153.19/21.82 | | | | (257) all_1802_7 = all_1328_4 % 153.19/21.82 | | | | % 153.19/21.82 | | | | SIMP: (257) implies: % 153.19/21.82 | | | | (258) all_1802_7 = all_1328_4 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (238), (256) imply: % 153.19/21.82 | | | | (259) all_1164_4 = all_358_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | SIMP: (259) implies: % 153.19/21.82 | | | | (260) all_1164_4 = all_358_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (250), (251) imply: % 153.19/21.82 | | | | (261) all_1122_0 = all_1106_0 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (250), (252) imply: % 153.19/21.82 | | | | (262) all_1122_0 = all_114_0 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (248), (249) imply: % 153.19/21.82 | | | | (263) all_1314_3 = all_1122_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (247), (248) imply: % 153.19/21.82 | | | | (264) all_1314_3 = 0 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (237), (258) imply: % 153.19/21.82 | | | | (265) all_1328_4 = all_1122_2 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (236), (258) imply: % 153.19/21.82 | | | | (266) all_1328_4 = all_1164_4 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (245), (246) imply: % 153.19/21.82 | | | | (267) all_1122_1 = all_1106_2 % 153.19/21.82 | | | | % 153.19/21.82 | | | | SIMP: (267) implies: % 153.19/21.82 | | | | (268) all_1122_1 = all_1106_2 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (265), (266) imply: % 153.19/21.82 | | | | (269) all_1164_4 = all_1122_2 % 153.19/21.82 | | | | % 153.19/21.82 | | | | SIMP: (269) implies: % 153.19/21.82 | | | | (270) all_1164_4 = all_1122_2 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (263), (264) imply: % 153.19/21.82 | | | | (271) all_1122_1 = 0 % 153.19/21.82 | | | | % 153.19/21.82 | | | | SIMP: (271) implies: % 153.19/21.82 | | | | (272) all_1122_1 = 0 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (234), (235) imply: % 153.19/21.82 | | | | (273) all_1106_1 = all_1070_2 % 153.19/21.82 | | | | % 153.19/21.82 | | | | SIMP: (273) implies: % 153.19/21.82 | | | | (274) all_1106_1 = all_1070_2 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (232), (233) imply: % 153.19/21.82 | | | | (275) all_1120_2 = all_1108_2 % 153.19/21.82 | | | | % 153.19/21.82 | | | | SIMP: (275) implies: % 153.19/21.82 | | | | (276) all_1120_2 = all_1108_2 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (231), (254) imply: % 153.19/21.82 | | | | (277) all_1120_2 = all_360_0 % 153.19/21.82 | | | | % 153.19/21.82 | | | | SIMP: (277) implies: % 153.19/21.82 | | | | (278) all_1120_2 = all_360_0 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (229), (230) imply: % 153.19/21.82 | | | | (279) all_1164_4 = all_1104_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | SIMP: (279) implies: % 153.19/21.82 | | | | (280) all_1164_4 = all_1104_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (260), (270) imply: % 153.19/21.82 | | | | (281) all_1122_2 = all_358_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (270), (280) imply: % 153.19/21.82 | | | | (282) all_1122_2 = all_1104_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (228), (270) imply: % 153.19/21.82 | | | | (283) all_1122_2 = all_362_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (261), (262) imply: % 153.19/21.82 | | | | (284) all_1106_0 = all_114_0 % 153.19/21.82 | | | | % 153.19/21.82 | | | | SIMP: (284) implies: % 153.19/21.82 | | | | (285) all_1106_0 = all_114_0 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (268), (272) imply: % 153.19/21.82 | | | | (286) all_1106_2 = 0 % 153.19/21.82 | | | | % 153.19/21.82 | | | | SIMP: (286) implies: % 153.19/21.82 | | | | (287) all_1106_2 = 0 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (282), (283) imply: % 153.19/21.82 | | | | (288) all_1104_1 = all_362_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (281), (282) imply: % 153.19/21.82 | | | | (289) all_1104_1 = all_358_1 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (227), (276) imply: % 153.19/21.82 | | | | (290) all_1108_2 = all_1068_2 % 153.19/21.82 | | | | % 153.19/21.82 | | | | COMBINE_EQS: (276), (278) imply: % 153.19/21.82 | | | | (291) all_1108_2 = all_360_0 % 153.19/21.82 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (290), (291) imply: % 153.19/21.83 | | | | (292) all_1068_2 = all_360_0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | SIMP: (292) implies: % 153.19/21.83 | | | | (293) all_1068_2 = all_360_0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (225), (274) imply: % 153.19/21.83 | | | | (294) all_1070_2 = all_724_0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (223), (274) imply: % 153.19/21.83 | | | | (295) all_1094_1 = all_1070_2 % 153.19/21.83 | | | | % 153.19/21.83 | | | | SIMP: (295) implies: % 153.19/21.83 | | | | (296) all_1094_1 = all_1070_2 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (224), (274) imply: % 153.19/21.83 | | | | (297) all_1070_2 = all_1068_2 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (226), (274) imply: % 153.19/21.83 | | | | (298) all_1070_2 = all_362_1 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (288), (289) imply: % 153.19/21.83 | | | | (299) all_362_1 = all_358_1 % 153.19/21.83 | | | | % 153.19/21.83 | | | | SIMP: (299) implies: % 153.19/21.83 | | | | (300) all_362_1 = all_358_1 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (222), (296) imply: % 153.19/21.83 | | | | (301) all_1070_2 = all_1055_2 % 153.19/21.83 | | | | % 153.19/21.83 | | | | SIMP: (301) implies: % 153.19/21.83 | | | | (302) all_1070_2 = all_1055_2 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (220), (221) imply: % 153.19/21.83 | | | | (303) all_724_0 = 0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | SIMP: (303) implies: % 153.19/21.83 | | | | (304) all_724_0 = 0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (298), (302) imply: % 153.19/21.83 | | | | (305) all_1055_2 = all_362_1 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (297), (302) imply: % 153.19/21.83 | | | | (306) all_1068_2 = all_1055_2 % 153.19/21.83 | | | | % 153.19/21.83 | | | | SIMP: (306) implies: % 153.19/21.83 | | | | (307) all_1068_2 = all_1055_2 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (294), (302) imply: % 153.19/21.83 | | | | (308) all_1055_2 = all_724_0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (293), (307) imply: % 153.19/21.83 | | | | (309) all_1055_2 = all_360_0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | SIMP: (309) implies: % 153.19/21.83 | | | | (310) all_1055_2 = all_360_0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (305), (310) imply: % 153.19/21.83 | | | | (311) all_362_1 = all_360_0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | SIMP: (311) implies: % 153.19/21.83 | | | | (312) all_362_1 = all_360_0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (308), (310) imply: % 153.19/21.83 | | | | (313) all_724_0 = all_360_0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | SIMP: (313) implies: % 153.19/21.83 | | | | (314) all_724_0 = all_360_0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (304), (314) imply: % 153.19/21.83 | | | | (315) all_360_0 = 0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | SIMP: (315) implies: % 153.19/21.83 | | | | (316) all_360_0 = 0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (300), (312) imply: % 153.19/21.83 | | | | (317) all_360_0 = all_358_1 % 153.19/21.83 | | | | % 153.19/21.83 | | | | SIMP: (317) implies: % 153.19/21.83 | | | | (318) all_360_0 = all_358_1 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (316), (318) imply: % 153.19/21.83 | | | | (319) all_358_1 = 0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (310), (316) imply: % 153.19/21.83 | | | | (320) all_1055_2 = 0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (302), (320) imply: % 153.19/21.83 | | | | (321) all_1070_2 = 0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | COMBINE_EQS: (274), (321) imply: % 153.19/21.83 | | | | (322) all_1106_1 = 0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | BETA: splitting (177) gives: % 153.19/21.83 | | | | % 153.19/21.83 | | | | Case 1: % 153.19/21.83 | | | | | % 153.19/21.83 | | | | | (323) ~ (all_1106_1 = 0) % 153.19/21.83 | | | | | % 153.19/21.83 | | | | | REDUCE: (322), (323) imply: % 153.19/21.83 | | | | | (324) $false % 153.19/21.83 | | | | | % 153.19/21.83 | | | | | CLOSE: (324) is inconsistent. % 153.19/21.83 | | | | | % 153.19/21.83 | | | | Case 2: % 153.19/21.83 | | | | | % 153.19/21.83 | | | | | (325) ~ (all_1106_2 = 0) | all_1106_0 = xc % 153.19/21.83 | | | | | % 153.19/21.83 | | | | | BETA: splitting (325) gives: % 153.19/21.83 | | | | | % 153.19/21.83 | | | | | Case 1: % 153.19/21.83 | | | | | | % 153.19/21.83 | | | | | | (326) ~ (all_1106_2 = 0) % 153.19/21.83 | | | | | | % 153.19/21.83 | | | | | | REDUCE: (287), (326) imply: % 153.19/21.83 | | | | | | (327) $false % 153.19/21.83 | | | | | | % 153.19/21.83 | | | | | | CLOSE: (327) is inconsistent. % 153.19/21.83 | | | | | | % 153.19/21.83 | | | | | Case 2: % 153.19/21.83 | | | | | | % 153.19/21.83 | | | | | | (328) all_1106_0 = xc % 153.19/21.83 | | | | | | % 153.19/21.83 | | | | | | COMBINE_EQS: (285), (328) imply: % 153.19/21.83 | | | | | | (329) all_114_0 = xc % 153.19/21.83 | | | | | | % 153.19/21.83 | | | | | | REDUCE: (152), (329) imply: % 153.19/21.83 | | | | | | (330) aElementOf0(xc, xI) = 0 % 153.19/21.83 | | | | | | % 153.19/21.83 | | | | | | GROUND_INST: instantiating (26) with all_49_0, 0, xI, xc, % 153.19/21.83 | | | | | | simplifying with (118), (330) gives: % 153.19/21.83 | | | | | | (331) all_49_0 = 0 % 153.19/21.83 | | | | | | % 153.19/21.83 | | | | | | REDUCE: (70), (331) imply: % 153.19/21.83 | | | | | | (332) $false % 153.19/21.83 | | | | | | % 153.19/21.83 | | | | | | CLOSE: (332) is inconsistent. % 153.19/21.83 | | | | | | % 153.19/21.83 | | | | | End of split % 153.19/21.83 | | | | | % 153.19/21.83 | | | | End of split % 153.19/21.83 | | | | % 153.19/21.83 | | | Case 2: % 153.19/21.83 | | | | % 153.19/21.83 | | | | (333) aElementOf0(all_43_0, all_43_3) = all_2109_0 & % 153.19/21.83 | | | | aElementOf0(all_43_1, all_43_4) = all_2109_1 & ( ~ (all_2109_0 % 153.19/21.83 | | | | = 0) | ~ (all_2109_1 = 0)) % 153.19/21.83 | | | | % 153.19/21.83 | | | | ALPHA: (333) implies: % 153.19/21.83 | | | | (334) aElementOf0(all_43_1, all_43_4) = all_2109_1 % 153.19/21.83 | | | | (335) aElementOf0(all_43_0, all_43_3) = all_2109_0 % 153.19/21.83 | | | | (336) ~ (all_2109_0 = 0) | ~ (all_2109_1 = 0) % 153.19/21.83 | | | | % 153.19/21.83 | | | | REDUCE: (106), (335) imply: % 153.19/21.83 | | | | (337) aElementOf0(all_43_0, all_38_4) = all_2109_0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | REDUCE: (107), (334) imply: % 153.19/21.83 | | | | (338) aElementOf0(all_43_1, all_38_5) = all_2109_1 % 153.19/21.83 | | | | % 153.19/21.83 | | | | GROUND_INST: instantiating (26) with 0, all_2109_1, all_38_5, all_43_1, % 153.19/21.83 | | | | simplifying with (113), (338) gives: % 153.19/21.83 | | | | (339) all_2109_1 = 0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | GROUND_INST: instantiating (26) with 0, all_2109_0, all_38_4, all_43_0, % 153.19/21.83 | | | | simplifying with (112), (337) gives: % 153.19/21.83 | | | | (340) all_2109_0 = 0 % 153.19/21.83 | | | | % 153.19/21.83 | | | | BETA: splitting (336) gives: % 153.19/21.83 | | | | % 153.19/21.83 | | | | Case 1: % 153.19/21.83 | | | | | % 153.19/21.83 | | | | | (341) ~ (all_2109_0 = 0) % 153.19/21.83 | | | | | % 153.19/21.83 | | | | | REDUCE: (340), (341) imply: % 153.19/21.83 | | | | | (342) $false % 153.19/21.83 | | | | | % 153.19/21.83 | | | | | CLOSE: (342) is inconsistent. % 153.19/21.83 | | | | | % 153.19/21.83 | | | | Case 2: % 153.19/21.83 | | | | | % 153.19/21.83 | | | | | (343) ~ (all_2109_1 = 0) % 153.19/21.83 | | | | | % 153.19/21.83 | | | | | REDUCE: (339), (343) imply: % 153.19/21.83 | | | | | (344) $false % 153.19/21.83 | | | | | % 153.19/21.83 | | | | | CLOSE: (344) is inconsistent. % 153.19/21.83 | | | | | % 153.19/21.83 | | | | End of split % 153.19/21.83 | | | | % 153.19/21.83 | | | End of split % 153.19/21.83 | | | % 153.19/21.83 | | End of split % 153.19/21.83 | | % 153.19/21.83 | End of split % 153.19/21.83 | % 153.19/21.83 End of proof % 153.19/21.84 % SZS output end Proof for theBenchmark % 153.19/21.84 % 153.19/21.84 21241ms %------------------------------------------------------------------------------