%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : RNG119+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 : n007.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:57:59 EDT 2023 % Result : Theorem 30.96s 4.90s % Output : Proof 163.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : RNG119+4 : TPTP v8.1.2. Released v4.0.0. % 0.07/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.33 % Computer : n007.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Sun Aug 27 01:57:57 EDT 2023 % 0.13/0.33 % CPUTime : % 0.20/0.59 ________ _____ % 0.20/0.59 ___ __ \_________(_)________________________________ % 0.20/0.59 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.59 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.59 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.59 % 0.20/0.59 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.59 (2023-06-19) % 0.20/0.59 % 0.20/0.59 (c) Philipp Rümmer, 2009-2023 % 0.20/0.59 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.59 Amanda Stjerna. % 0.20/0.59 Free software under BSD-3-Clause. % 0.20/0.59 % 0.20/0.59 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.59 % 0.20/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.20/0.61 Running up to 7 provers in parallel. % 0.20/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.87/1.28 Prover 4: Preprocessing ... % 3.87/1.28 Prover 1: Preprocessing ... % 3.87/1.33 Prover 6: Preprocessing ... % 3.87/1.33 Prover 0: Preprocessing ... % 3.87/1.33 Prover 2: Preprocessing ... % 3.87/1.34 Prover 3: Preprocessing ... % 3.87/1.34 Prover 5: Preprocessing ... % 11.21/2.31 Prover 1: Constructing countermodel ... % 11.92/2.37 Prover 6: Proving ... % 12.14/2.42 Prover 5: Proving ... % 12.14/2.42 Prover 3: Constructing countermodel ... % 13.10/2.54 Prover 2: Proving ... % 13.10/2.61 Prover 4: Constructing countermodel ... % 13.74/2.71 Prover 0: Proving ... % 30.96/4.90 Prover 0: proved (4275ms) % 30.96/4.90 % 30.96/4.90 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 30.96/4.90 % 30.96/4.90 Prover 3: stopped % 30.96/4.90 Prover 5: stopped % 30.96/4.91 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 30.96/4.91 Prover 6: stopped % 30.96/4.91 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 31.14/4.92 Prover 2: stopped % 31.19/4.92 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 31.19/4.92 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 31.19/4.94 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 31.19/5.08 Prover 10: Preprocessing ... % 31.94/5.10 Prover 7: Preprocessing ... % 31.94/5.10 Prover 11: Preprocessing ... % 31.94/5.11 Prover 13: Preprocessing ... % 31.94/5.13 Prover 8: Preprocessing ... % 34.25/5.34 Prover 7: Constructing countermodel ... % 34.25/5.36 Prover 10: Constructing countermodel ... % 34.25/5.40 Prover 8: Warning: ignoring some quantifiers % 34.80/5.44 Prover 8: Constructing countermodel ... % 34.80/5.44 Prover 13: Warning: ignoring some quantifiers % 34.80/5.46 Prover 13: Constructing countermodel ... % 35.26/5.55 Prover 11: Constructing countermodel ... % 70.35/10.02 Prover 13: stopped % 70.35/10.02 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 70.35/10.07 Prover 16: Preprocessing ... % 70.98/10.26 Prover 16: Warning: ignoring some quantifiers % 71.81/10.27 Prover 16: Constructing countermodel ... % 114.33/15.74 Prover 16: stopped % 114.33/15.74 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 115.15/15.82 Prover 19: Preprocessing ... % 116.27/15.96 Prover 1: stopped % 117.46/16.14 Prover 19: Warning: ignoring some quantifiers % 117.88/16.17 Prover 19: Constructing countermodel ... % 141.25/19.47 Prover 19: stopped % 161.64/22.31 Prover 4: Found proof (size 307) % 161.64/22.31 Prover 4: proved (21690ms) % 161.64/22.31 Prover 8: stopped % 161.64/22.31 Prover 7: stopped % 161.64/22.31 Prover 10: stopped % 161.64/22.32 Prover 11: stopped % 161.64/22.32 % 161.64/22.32 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 161.64/22.32 % 161.64/22.35 % SZS output start Proof for theBenchmark % 162.19/22.35 Assumptions after simplification: % 162.19/22.35 --------------------------------- % 162.19/22.35 % 162.19/22.35 (mAMDistr) % 162.19/22.40 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 162.19/22.40 $i] : ( ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v1, v0) = v3) | ~ % 162.19/22.40 (sdtpldt0(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : % 162.19/22.40 ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? % 162.19/22.40 [v12: $i] : ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v9, v0) = v14 & % 162.19/22.40 sdtasdt0(v0, v9) = v10 & sdtasdt0(v0, v2) = v12 & sdtasdt0(v0, v1) = v11 & % 162.19/22.40 sdtpldt0(v11, v12) = v13 & sdtpldt0(v1, v2) = v9 & aElement0(v2) = v8 & % 162.19/22.40 aElement0(v1) = v7 & aElement0(v0) = v6 & $i(v14) & $i(v13) & $i(v12) & % 162.19/22.40 $i(v11) & $i(v10) & $i(v9) & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | % 162.19/22.40 (v14 = v5 & v13 = v10)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 162.19/22.40 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ % 162.19/22.40 (sdtasdt0(v0, v1) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) % 162.19/22.40 | ~ $i(v0) | ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? % 162.19/22.40 [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : % 162.19/22.40 (sdtasdt0(v9, v0) = v11 & sdtasdt0(v2, v0) = v13 & sdtasdt0(v1, v0) = v12 & % 162.19/22.40 sdtasdt0(v0, v9) = v10 & sdtpldt0(v12, v13) = v14 & sdtpldt0(v1, v2) = v9 % 162.19/22.40 & aElement0(v2) = v8 & aElement0(v1) = v7 & aElement0(v0) = v6 & $i(v14) & % 162.19/22.40 $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) & ( ~ (v8 = 0) | ~ (v7 = % 162.19/22.40 0) | ~ (v6 = 0) | (v14 = v11 & v10 = v5)))) & ! [v0: $i] : ! [v1: % 162.19/22.40 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (sdtasdt0(v3, v0) = v4) % 162.19/22.40 | ~ (sdtpldt0(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: % 162.19/22.40 any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? [v9: $i] : ? [v10: % 162.19/22.40 $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : % 162.19/22.40 (sdtasdt0(v2, v0) = v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v3) = v8 & % 162.19/22.40 sdtasdt0(v0, v2) = v10 & sdtasdt0(v0, v1) = v9 & sdtpldt0(v12, v13) = v14 % 162.19/22.40 & sdtpldt0(v9, v10) = v11 & aElement0(v2) = v7 & aElement0(v1) = v6 & % 162.19/22.40 aElement0(v0) = v5 & $i(v14) & $i(v13) & $i(v12) & $i(v11) & $i(v10) & % 162.19/22.40 $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | (v14 = v4 & % 162.19/22.40 v11 = v8)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 162.19/22.40 ! [v4: $i] : ( ~ (sdtasdt0(v0, v3) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ % 162.19/22.40 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] % 162.19/22.40 : ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : % 162.19/22.40 ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v3, v0) = v11 & sdtasdt0(v2, v0) = % 162.19/22.40 v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v2) = v9 & sdtasdt0(v0, v1) = % 162.19/22.40 v8 & sdtpldt0(v12, v13) = v14 & sdtpldt0(v8, v9) = v10 & aElement0(v2) = % 162.19/22.40 v7 & aElement0(v1) = v6 & aElement0(v0) = v5 & $i(v14) & $i(v13) & $i(v12) % 162.19/22.40 & $i(v11) & $i(v10) & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ % 162.19/22.40 (v5 = 0) | (v14 = v11 & v10 = v4)))) % 162.19/22.40 % 162.19/22.40 (mAddComm) % 162.19/22.40 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ % 162.19/22.40 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 162.19/22.40 (sdtpldt0(v0, v1) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & $i(v5) & % 162.19/22.40 ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) & ! [v0: $i] : ! [v1: $i] : ! % 162.19/22.40 [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] % 162.19/22.40 : ? [v4: any] : ? [v5: $i] : (sdtpldt0(v1, v0) = v5 & aElement0(v1) = v4 & % 162.19/22.40 aElement0(v0) = v3 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 162.19/22.40 % 162.19/22.40 (mAddZero) % 162.19/22.41 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtpldt0(v0, sz00) = v1) | ~ % 162.19/22.41 $i(v0) | ? [v2: any] : ? [v3: $i] : (sdtpldt0(sz00, v0) = v3 & % 162.19/22.41 aElement0(v0) = v2 & $i(v3) & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) & ! % 162.19/22.41 [v0: $i] : ! [v1: $i] : ( ~ (sdtpldt0(sz00, v0) = v1) | ~ $i(v0) | ? [v2: % 162.19/22.41 any] : ? [v3: $i] : (sdtpldt0(v0, sz00) = v3 & aElement0(v0) = v2 & % 162.19/22.41 $i(v3) & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) & ! [v0: $i] : ( ~ % 162.19/22.41 (aElement0(v0) = 0) | ~ $i(v0) | (sdtpldt0(v0, sz00) = v0 & sdtpldt0(sz00, % 162.19/22.41 v0) = v0)) % 162.19/22.41 % 162.19/22.41 (mDefDvs) % 162.19/22.41 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (aDivisorOf0(v1, v0) = % 162.19/22.41 v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? % 162.19/22.41 [v4: any] : (doDivides0(v1, v0) = v4 & aElement0(v1) = v3 & ( ~ (v4 = 0) | % 162.19/22.41 ~ (v3 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ % 162.19/22.41 (doDivides0(v1, v0) = v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | % 162.19/22.41 ? [v3: any] : ? [v4: any] : (aDivisorOf0(v1, v0) = v3 & aElement0(v1) = v4 % 162.19/22.41 & ( ~ (v3 = 0) | (v4 = 0 & v2 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! % 162.19/22.41 [v2: any] : ( ~ (aElement0(v1) = v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ % 162.19/22.41 $i(v0) | ? [v3: any] : ? [v4: any] : (aDivisorOf0(v1, v0) = v3 & % 162.19/22.41 doDivides0(v1, v0) = v4 & ( ~ (v3 = 0) | (v4 = 0 & v2 = 0)))) & ! [v0: % 162.19/22.41 $i] : ! [v1: $i] : ( ~ (aDivisorOf0(v1, v0) = 0) | ~ (aElement0(v0) = 0) | % 162.19/22.41 ~ $i(v1) | ~ $i(v0) | (doDivides0(v1, v0) = 0 & aElement0(v1) = 0)) & ! % 162.19/22.41 [v0: $i] : ! [v1: $i] : ( ~ (doDivides0(v1, v0) = 0) | ~ (aElement0(v0) = 0) % 162.19/22.41 | ~ $i(v1) | ~ $i(v0) | ? [v2: any] : ? [v3: any] : (aDivisorOf0(v1, v0) % 162.19/22.41 = v3 & aElement0(v1) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0: $i] : ! % 162.19/22.41 [v1: $i] : ( ~ (aElement0(v1) = 0) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ % 162.19/22.41 $i(v0) | ? [v2: any] : ? [v3: any] : (aDivisorOf0(v1, v0) = v3 & % 162.19/22.41 doDivides0(v1, v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 162.19/22.41 % 162.19/22.41 (mDefIdeal) % 162.53/22.43 ! [v0: $i] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 162.53/22.43 $i] : ( ~ (aSet0(v0) = v1) | ~ (aElementOf0(v2, v0) = 0) | ~ (sdtasdt0(v3, % 162.53/22.43 v2) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v0) | ? [v5: int] : ? [v6: % 162.53/22.43 any] : (( ~ (v5 = 0) & aIdeal0(v0) = v5) | (aElementOf0(v4, v0) = v6 & % 162.53/22.43 aElement0(v3) = v5 & ( ~ (v5 = 0) | v6 = 0)))) & ! [v0: $i] : ! [v1: % 162.53/22.43 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 162.53/22.43 (aSet0(v0) = v1) | ~ (aElementOf0(v2, v0) = 0) | ~ (sdtpldt0(v2, v3) = v4) % 162.53/22.43 | ~ $i(v3) | ~ $i(v2) | ~ $i(v0) | ? [v5: int] : ? [v6: any] : (( ~ (v5 % 162.53/22.43 = 0) & aIdeal0(v0) = v5) | (aElementOf0(v4, v0) = v6 & aElementOf0(v3, % 162.53/22.43 v0) = v5 & ( ~ (v5 = 0) | v6 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! % 162.53/22.43 [v2: $i] : ! [v3: $i] : ( ~ (aIdeal0(v0) = 0) | ~ (aElementOf0(v1, v0) = 0) % 162.53/22.43 | ~ (sdtasdt0(v2, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 162.53/22.43 any] : ? [v5: any] : (aElementOf0(v3, v0) = v5 & aElement0(v2) = v4 & ( ~ % 162.53/22.43 (v4 = 0) | v5 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 162.53/22.43 $i] : ( ~ (aIdeal0(v0) = 0) | ~ (aElementOf0(v1, v0) = 0) | ~ % 162.53/22.43 (sdtpldt0(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : % 162.53/22.43 ? [v5: any] : (aElementOf0(v3, v0) = v5 & aElementOf0(v2, v0) = v4 & ( ~ % 162.53/22.43 (v4 = 0) | v5 = 0))) & ! [v0: $i] : ! [v1: MultipleValueBool] : ! % 162.53/22.43 [v2: $i] : ! [v3: $i] : ( ~ (aSet0(v0) = v1) | ~ (aElementOf0(v3, v0) = 0) | % 162.53/22.43 ~ (aElementOf0(v2, v0) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v0) | ? [v4: % 162.53/22.43 any] : ? [v5: int] : ((v5 = 0 & aElementOf0(v4, v0) = 0 & sdtpldt0(v2, % 162.53/22.43 v3) = v4 & $i(v4)) | ( ~ (v4 = 0) & aIdeal0(v0) = v4))) & ! [v0: $i] % 162.53/22.43 : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ( ~ (aSet0(v0) = % 162.53/22.43 v1) | ~ (aElementOf0(v2, v0) = 0) | ~ (aElement0(v3) = 0) | ~ $i(v3) | % 162.53/22.43 ~ $i(v2) | ~ $i(v0) | ? [v4: any] : ? [v5: int] : ((v5 = 0 & % 162.53/22.43 aElementOf0(v4, v0) = 0 & sdtasdt0(v3, v2) = v4 & $i(v4)) | ( ~ (v4 = 0) % 162.53/22.43 & aIdeal0(v0) = v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 162.53/22.43 (aIdeal0(v0) = 0) | ~ (aElementOf0(v2, v0) = 0) | ~ (aElementOf0(v1, v0) = % 162.53/22.43 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : (aElementOf0(v3, % 162.53/22.43 v0) = 0 & sdtpldt0(v1, v2) = v3 & $i(v3))) & ! [v0: $i] : ! [v1: $i] : % 162.53/22.43 ! [v2: $i] : ( ~ (aIdeal0(v0) = 0) | ~ (aElementOf0(v1, v0) = 0) | ~ % 162.53/22.43 (aElement0(v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : % 162.53/22.43 (aElementOf0(v3, v0) = 0 & sdtasdt0(v2, v1) = v3 & $i(v3))) & ! [v0: $i] : % 162.53/22.43 ! [v1: int] : (v1 = 0 | ~ (aIdeal0(v0) = v1) | ~ $i(v0) | ? [v2: int] : ? % 162.53/22.43 [v3: $i] : ? [v4: int] : ? [v5: $i] : ? [v6: int] : ? [v7: $i] : ? [v8: % 162.53/22.43 int] : ? [v9: $i] : ? [v10: int] : ? [v11: $i] : ? [v12: int] : % 162.53/22.43 ($i(v9) & $i(v5) & $i(v3) & ((v4 = 0 & aElementOf0(v3, v0) = 0 & ((v10 = 0 & % 162.53/22.43 ~ (v12 = 0) & aElementOf0(v11, v0) = v12 & aElementOf0(v9, v0) = % 162.53/22.43 0 & sdtpldt0(v3, v9) = v11 & $i(v11)) | (v6 = 0 & ~ (v8 = 0) & % 162.53/22.43 aElementOf0(v7, v0) = v8 & sdtasdt0(v5, v3) = v7 & aElement0(v5) = % 162.53/22.43 0 & $i(v7)))) | ( ~ (v2 = 0) & aSet0(v0) = v2)))) & ! [v0: $i] : % 162.53/22.43 ! [v1: int] : (v1 = 0 | ~ (aSet0(v0) = v1) | ~ $i(v0) | ? [v2: int] : ( ~ % 162.53/22.43 (v2 = 0) & aIdeal0(v0) = v2)) & ! [v0: $i] : ( ~ (aIdeal0(v0) = 0) | ~ % 162.53/22.43 $i(v0) | aSet0(v0) = 0) & ! [v0: $i] : ( ~ (aSet0(v0) = 0) | ~ $i(v0) | ? % 162.53/22.43 [v1: int] : ? [v2: $i] : ? [v3: int] : ? [v4: $i] : ? [v5: int] : ? % 162.53/22.43 [v6: $i] : ? [v7: int] : ? [v8: $i] : ? [v9: int] : ? [v10: $i] : ? % 162.53/22.43 [v11: int] : ($i(v8) & $i(v4) & $i(v2) & ((v3 = 0 & aElementOf0(v2, v0) = 0 % 162.53/22.43 & ((v9 = 0 & ~ (v11 = 0) & aElementOf0(v10, v0) = v11 & % 162.53/22.43 aElementOf0(v8, v0) = 0 & sdtpldt0(v2, v8) = v10 & $i(v10)) | (v5 % 162.53/22.43 = 0 & ~ (v7 = 0) & aElementOf0(v6, v0) = v7 & sdtasdt0(v4, v2) = % 162.53/22.43 v6 & aElement0(v4) = 0 & $i(v6)))) | (v1 = 0 & aIdeal0(v0) = 0)))) % 162.53/22.43 % 162.53/22.43 (mDefRel) % 162.53/22.43 $i(sz10) & ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ % 162.53/22.43 (misRelativelyPrime0(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : % 162.53/22.43 ? [v4: any] : ? [v5: any] : (aGcdOfAnd0(sz10, v0, v1) = v5 & aElement0(v1) % 162.53/22.43 = v4 & aElement0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | (( ~ (v5 = 0) | % 162.53/22.43 v2 = 0) & ( ~ (v2 = 0) | v5 = 0))))) & ! [v0: $i] : ! [v1: $i] : % 162.53/22.43 ! [v2: any] : ( ~ (aGcdOfAnd0(sz10, v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? % 162.53/22.43 [v3: any] : ? [v4: any] : ? [v5: any] : (misRelativelyPrime0(v0, v1) = v5 % 162.53/22.43 & aElement0(v1) = v4 & aElement0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | % 162.53/22.43 (( ~ (v5 = 0) | v2 = 0) & ( ~ (v2 = 0) | v5 = 0))))) % 162.53/22.43 % 162.53/22.43 (mDivision) % 162.53/22.43 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = sz00 | ~ % 162.53/22.43 (sbrdtbr0(v1) = v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | ? % 162.53/22.43 [v3: int] : ? [v4: $i] : ? [v5: $i] : ? [v6: int] : ? [v7: int] : ? % 162.53/22.43 [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: any] : ($i(v5) & $i(v4) & % 162.53/22.43 ((v9 = v0 & v7 = 0 & v6 = 0 & iLess0(v10, v2) = v11 & sbrdtbr0(v5) = v10 & % 162.53/22.43 sdtasdt0(v4, v1) = v8 & sdtpldt0(v8, v5) = v0 & aElement0(v5) = 0 & % 162.53/22.43 aElement0(v4) = 0 & $i(v10) & $i(v8) & (v11 = 0 | v5 = sz00)) | ( ~ % 162.53/22.43 (v3 = 0) & aElement0(v1) = v3)))) & ! [v0: $i] : ! [v1: $i] : (v1 = % 162.53/22.43 sz00 | ~ (aElement0(v1) = 0) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ % 162.53/22.43 $i(v0) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] % 162.53/22.43 : ? [v7: any] : (iLess0(v6, v2) = v7 & sbrdtbr0(v4) = v6 & sbrdtbr0(v1) = % 162.53/22.43 v2 & sdtasdt0(v3, v1) = v5 & sdtpldt0(v5, v4) = v0 & aElement0(v4) = 0 & % 162.53/22.43 aElement0(v3) = 0 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & (v7 = 0 | % 162.53/22.43 v4 = sz00))) % 162.53/22.43 % 162.53/22.43 (mEOfElem) % 162.53/22.44 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (aSet0(v0) = 0) | ~ % 162.53/22.44 (aElement0(v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: int] : ( ~ (v3 = 0) & % 162.53/22.44 aElementOf0(v1, v0) = v3)) & ! [v0: $i] : ! [v1: $i] : ( ~ (aSet0(v0) = % 162.53/22.44 0) | ~ (aElementOf0(v1, v0) = 0) | ~ $i(v1) | ~ $i(v0) | aElement0(v1) % 162.53/22.44 = 0) % 162.53/22.44 % 162.53/22.44 (mEucSort) % 162.53/22.44 $i(sz00) & ! [v0: $i] : ! [v1: $i] : (v0 = sz00 | ~ (sbrdtbr0(v0) = v1) | % 162.53/22.44 ~ $i(v0) | ? [v2: any] : ? [v3: any] : (aNaturalNumber0(v1) = v3 & % 162.53/22.44 aElement0(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0: $i] : (v0 = sz00 | % 162.53/22.44 ~ (aElement0(v0) = 0) | ~ $i(v0) | ? [v1: $i] : (sbrdtbr0(v0) = v1 & % 162.53/22.44 aNaturalNumber0(v1) = 0 & $i(v1))) % 162.53/22.44 % 162.53/22.44 (mMulAsso) % 162.53/22.44 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 162.53/22.44 (sdtasdt0(v3, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) % 162.53/22.44 | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? % 162.53/22.44 [v9: $i] : (sdtasdt0(v1, v2) = v8 & sdtasdt0(v0, v8) = v9 & aElement0(v2) = % 162.53/22.44 v7 & aElement0(v1) = v6 & aElement0(v0) = v5 & $i(v9) & $i(v8) & ( ~ (v7 = % 162.53/22.44 0) | ~ (v6 = 0) | ~ (v5 = 0) | v9 = v4))) & ! [v0: $i] : ! [v1: % 162.53/22.44 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (sdtasdt0(v1, v2) = v3) % 162.53/22.44 | ~ (sdtasdt0(v0, v3) = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: % 162.53/22.44 any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? [v9: $i] : % 162.53/22.44 (sdtasdt0(v8, v2) = v9 & sdtasdt0(v0, v1) = v8 & aElement0(v2) = v7 & % 162.53/22.44 aElement0(v1) = v6 & aElement0(v0) = v5 & $i(v9) & $i(v8) & ( ~ (v7 = 0) | % 162.53/22.44 ~ (v6 = 0) | ~ (v5 = 0) | v9 = v4))) % 162.53/22.44 % 162.53/22.44 (mMulComm) % 162.53/22.44 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v1, v0) = v2) | ~ % 162.53/22.44 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 162.53/22.44 (sdtasdt0(v0, v1) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & $i(v5) & % 162.53/22.44 ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) & ! [v0: $i] : ! [v1: $i] : ! % 162.53/22.44 [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] % 162.53/22.44 : ? [v4: any] : ? [v5: $i] : (sdtasdt0(v1, v0) = v5 & aElement0(v1) = v4 & % 162.53/22.44 aElement0(v0) = v3 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 162.53/22.44 % 162.53/22.44 (mSortsB) % 162.53/22.44 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 162.53/22.44 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 162.53/22.44 (aElement0(v2) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & ( ~ (v4 = 0) % 162.53/22.44 | ~ (v3 = 0) | v5 = 0))) % 162.53/22.44 % 162.53/22.44 (mSortsB_02) % 162.53/22.45 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 162.53/22.45 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 162.53/22.45 (aElement0(v2) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & ( ~ (v4 = 0) % 162.53/22.45 | ~ (v3 = 0) | v5 = 0))) % 162.53/22.45 % 162.53/22.45 (mSortsC_01) % 162.53/22.45 aElement0(sz10) = 0 & $i(sz10) % 162.53/22.45 % 162.53/22.45 (mUnNeZr) % 162.53/22.45 ~ (sz10 = sz00) & $i(sz10) & $i(sz00) % 162.53/22.45 % 162.53/22.45 (m__) % 162.53/22.45 xr = sz00 & $i(sz00) % 162.53/22.45 % 162.53/22.45 (m__2091) % 162.53/22.45 aElement0(xb) = 0 & aElement0(xa) = 0 & $i(xb) & $i(xa) % 162.53/22.45 % 162.53/22.45 (m__2129) % 162.53/22.47 $i(xc) & $i(xb) & $i(xa) & ? [v0: $i] : ? [v1: $i] : (aGcdOfAnd0(xc, xa, xb) % 162.53/22.47 = 0 & aDivisorOf0(xc, xb) = 0 & aDivisorOf0(xc, xa) = 0 & doDivides0(xc, xb) % 162.53/22.47 = 0 & doDivides0(xc, xa) = 0 & sdtasdt0(xc, v1) = xa & sdtasdt0(xc, v0) = xb % 162.53/22.47 & aElement0(v1) = 0 & aElement0(v0) = 0 & aElement0(xc) = 0 & $i(v1) & % 162.53/22.47 $i(v0) & ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (doDivides0(v2, xc) = v3) % 162.53/22.47 | ~ $i(v2) | ? [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: any] : % 162.53/22.47 ? [v8: any] : (aDivisorOf0(v2, xb) = v8 & aDivisorOf0(v2, xa) = v6 & % 162.53/22.47 doDivides0(v2, xb) = v7 & doDivides0(v2, xa) = v5 & aElement0(v2) = v4 & % 162.53/22.47 (( ~ (v8 = 0) & ~ (v7 = 0) & ! [v9: $i] : ( ~ (sdtasdt0(v2, v9) = xb) % 162.53/22.47 | ~ $i(v9) | ? [v10: int] : ( ~ (v10 = 0) & aElement0(v9) = % 162.53/22.47 v10)) & ! [v9: $i] : ( ~ (aElement0(v9) = 0) | ~ $i(v9) | ? % 162.53/22.47 [v10: $i] : ( ~ (v10 = xb) & sdtasdt0(v2, v9) = v10 & $i(v10)))) | % 162.53/22.47 ( ~ (v6 = 0) & ( ~ (v4 = 0) | ( ~ (v5 = 0) & ! [v9: $i] : ( ~ % 162.53/22.47 (sdtasdt0(v2, v9) = xa) | ~ $i(v9) | ? [v10: int] : ( ~ (v10 % 162.53/22.47 = 0) & aElement0(v9) = v10)) & ! [v9: $i] : ( ~ % 162.53/22.47 (aElement0(v9) = 0) | ~ $i(v9) | ? [v10: $i] : ( ~ (v10 = % 162.53/22.47 xa) & sdtasdt0(v2, v9) = v10 & $i(v10))))))))) & ! [v2: % 162.53/22.47 $i] : ! [v3: any] : ( ~ (aDivisorOf0(v2, xb) = v3) | ~ $i(v2) | ? [v4: % 162.53/22.47 any] : ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : ? % 162.53/22.47 [v9: $i] : ? [v10: int] : ? [v11: $i] : (aDivisorOf0(v2, xa) = v6 & % 162.53/22.47 doDivides0(v2, xc) = v8 & doDivides0(v2, xb) = v7 & doDivides0(v2, xa) = % 162.53/22.47 v5 & aElement0(v2) = v4 & $i(v9) & ((v11 = xc & v10 = 0 & v8 = 0 & % 162.53/22.47 sdtasdt0(v2, v9) = xc & aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v3 = % 162.53/22.47 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? % 162.53/22.47 [v13: int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! [v12: $i] % 162.53/22.47 : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = % 162.53/22.47 xb) & sdtasdt0(v2, v12) = v13 & $i(v13)))) | ( ~ (v6 = 0) & ( % 162.53/22.47 ~ (v4 = 0) | ( ~ (v5 = 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) % 162.53/22.47 = xa) | ~ $i(v12) | ? [v13: int] : ( ~ (v13 = 0) & % 162.53/22.47 aElement0(v12) = v13)) & ! [v12: $i] : ( ~ (aElement0(v12) % 162.53/22.47 = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = xa) & % 162.53/22.47 sdtasdt0(v2, v12) = v13 & $i(v13))))))))) & ! [v2: $i] : ! % 162.53/22.47 [v3: any] : ( ~ (aDivisorOf0(v2, xa) = v3) | ~ $i(v2) | ? [v4: any] : ? % 162.53/22.47 [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? % 162.53/22.47 [v10: int] : ? [v11: $i] : (aDivisorOf0(v2, xb) = v7 & doDivides0(v2, xc) % 162.53/22.47 = v8 & doDivides0(v2, xb) = v6 & doDivides0(v2, xa) = v5 & aElement0(v2) % 162.53/22.47 = v4 & $i(v9) & ((v11 = xc & v10 = 0 & v8 = 0 & sdtasdt0(v2, v9) = xc & % 162.53/22.47 aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v6 = 0) & ! [v12: $i] : ( ~ % 162.53/22.47 (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? [v13: int] : ( ~ (v13 = % 162.53/22.47 0) & aElement0(v12) = v13)) & ! [v12: $i] : ( ~ % 162.53/22.47 (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = xb) % 162.53/22.47 & sdtasdt0(v2, v12) = v13 & $i(v13)))) | ( ~ (v3 = 0) & ( ~ (v4 % 162.53/22.47 = 0) | ( ~ (v5 = 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) = % 162.53/22.47 xa) | ~ $i(v12) | ? [v13: int] : ( ~ (v13 = 0) & % 162.53/22.47 aElement0(v12) = v13)) & ! [v12: $i] : ( ~ (aElement0(v12) % 162.53/22.47 = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = xa) & % 162.53/22.47 sdtasdt0(v2, v12) = v13 & $i(v13))))))))) & ! [v2: $i] : ! % 162.53/22.47 [v3: MultipleValueBool] : ( ~ (doDivides0(v2, xc) = v3) | ~ $i(v2) | ? % 162.75/22.47 [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : ? % 162.75/22.47 [v9: $i] : ? [v10: int] : ? [v11: $i] : ($i(v9) & ((v11 = xc & v10 = 0 & % 162.75/22.47 sdtasdt0(v2, v9) = xc & aElement0(v9) = 0) | (aDivisorOf0(v2, xb) = % 162.75/22.47 v8 & aDivisorOf0(v2, xa) = v6 & doDivides0(v2, xb) = v7 & % 162.75/22.47 doDivides0(v2, xa) = v5 & aElement0(v2) = v4 & (( ~ (v8 = 0) & ~ % 162.75/22.47 (v7 = 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ % 162.75/22.47 $i(v12) | ? [v13: int] : ( ~ (v13 = 0) & aElement0(v12) = % 162.75/22.47 v13)) & ! [v12: $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) % 162.75/22.47 | ? [v13: $i] : ( ~ (v13 = xb) & sdtasdt0(v2, v12) = v13 & % 162.75/22.47 $i(v13)))) | ( ~ (v6 = 0) & ( ~ (v4 = 0) | ( ~ (v5 = 0) & ! % 162.75/22.47 [v12: $i] : ( ~ (sdtasdt0(v2, v12) = xa) | ~ $i(v12) | ? % 162.75/22.47 [v13: int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! % 162.75/22.47 [v12: $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: % 162.75/22.47 $i] : ( ~ (v13 = xa) & sdtasdt0(v2, v12) = v13 & % 162.75/22.47 $i(v13))))))))))) & ! [v2: $i] : ! [v3: any] : ( ~ % 162.75/22.47 (doDivides0(v2, xb) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: any] : ? % 162.75/22.47 [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? [v10: int] : ? % 162.75/22.47 [v11: $i] : (aDivisorOf0(v2, xb) = v7 & aDivisorOf0(v2, xa) = v6 & % 162.75/22.47 doDivides0(v2, xc) = v8 & doDivides0(v2, xa) = v5 & aElement0(v2) = v4 & % 162.75/22.47 $i(v9) & ((v11 = xc & v10 = 0 & v8 = 0 & sdtasdt0(v2, v9) = xc & % 162.75/22.47 aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v3 = 0) & ! [v12: $i] : ( ~ % 162.75/22.47 (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? [v13: int] : ( ~ (v13 = % 162.75/22.47 0) & aElement0(v12) = v13)) & ! [v12: $i] : ( ~ % 162.75/22.47 (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = xb) % 162.75/22.47 & sdtasdt0(v2, v12) = v13 & $i(v13)))) | ( ~ (v6 = 0) & ( ~ (v4 % 162.75/22.47 = 0) | ( ~ (v5 = 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) = % 162.75/22.47 xa) | ~ $i(v12) | ? [v13: int] : ( ~ (v13 = 0) & % 162.75/22.47 aElement0(v12) = v13)) & ! [v12: $i] : ( ~ (aElement0(v12) % 162.75/22.47 = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = xa) & % 162.75/22.47 sdtasdt0(v2, v12) = v13 & $i(v13))))))))) & ! [v2: $i] : ! % 162.75/22.47 [v3: any] : ( ~ (doDivides0(v2, xa) = v3) | ~ $i(v2) | ? [v4: any] : ? % 162.75/22.47 [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? % 162.75/22.47 [v10: int] : ? [v11: $i] : (aDivisorOf0(v2, xb) = v7 & aDivisorOf0(v2, % 162.75/22.47 xa) = v5 & doDivides0(v2, xc) = v8 & doDivides0(v2, xb) = v6 & % 162.75/22.47 aElement0(v2) = v4 & $i(v9) & ((v11 = xc & v10 = 0 & v8 = 0 & % 162.75/22.47 sdtasdt0(v2, v9) = xc & aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v6 = % 162.75/22.47 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? % 162.75/22.47 [v13: int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! [v12: $i] % 162.75/22.47 : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = % 162.75/22.47 xb) & sdtasdt0(v2, v12) = v13 & $i(v13)))) | ( ~ (v5 = 0) & ( % 162.75/22.47 ~ (v4 = 0) | ( ~ (v3 = 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) % 162.75/22.47 = xa) | ~ $i(v12) | ? [v13: int] : ( ~ (v13 = 0) & % 162.75/22.47 aElement0(v12) = v13)) & ! [v12: $i] : ( ~ (aElement0(v12) % 162.75/22.47 = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = xa) & % 162.75/22.47 sdtasdt0(v2, v12) = v13 & $i(v13))))))))) & ! [v2: $i] : ! % 162.75/22.47 [v3: any] : ( ~ (aElement0(v2) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: % 162.75/22.47 any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? % 162.75/22.47 [v10: int] : ? [v11: $i] : (aDivisorOf0(v2, xb) = v7 & aDivisorOf0(v2, % 162.75/22.47 xa) = v5 & doDivides0(v2, xc) = v8 & doDivides0(v2, xb) = v6 & % 162.75/22.47 doDivides0(v2, xa) = v4 & $i(v9) & ((v11 = xc & v10 = 0 & v8 = 0 & % 162.75/22.47 sdtasdt0(v2, v9) = xc & aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v6 = % 162.75/22.47 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? % 162.75/22.47 [v13: int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! [v12: $i] % 162.75/22.47 : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = % 162.75/22.47 xb) & sdtasdt0(v2, v12) = v13 & $i(v13)))) | ( ~ (v5 = 0) & ( % 162.75/22.47 ~ (v3 = 0) | ( ~ (v4 = 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) % 162.75/22.47 = xa) | ~ $i(v12) | ? [v13: int] : ( ~ (v13 = 0) & % 162.75/22.47 aElement0(v12) = v13)) & ! [v12: $i] : ( ~ (aElement0(v12) % 162.75/22.47 = 0) | ~ $i(v12) | ? [v13: $i] : ( ~ (v13 = xa) & % 162.75/22.47 sdtasdt0(v2, v12) = v13 & $i(v13)))))))))) % 162.75/22.47 % 162.75/22.47 (m__2174) % 162.75/22.48 $i(xI) & $i(xb) & $i(xa) & ? [v0: $i] : ? [v1: $i] : (slsdtgt0(xb) = v1 & % 162.75/22.48 slsdtgt0(xa) = v0 & aIdeal0(xI) = 0 & sdtpldt1(v0, v1) = xI & aSet0(xI) = 0 % 162.75/22.48 & $i(v1) & $i(v0) & ! [v2: $i] : ! [v3: int] : ! [v4: $i] : ! [v5: $i] : % 162.75/22.48 (v3 = 0 | ~ (aElementOf0(v2, xI) = v3) | ~ (sdtpldt0(v4, v5) = v2) | ~ % 162.75/22.48 $i(v5) | ~ $i(v4) | ~ $i(v2) | ? [v6: any] : ? [v7: any] : % 162.75/22.48 (aElementOf0(v5, v1) = v7 & aElementOf0(v4, v0) = v6 & ( ~ (v7 = 0) | ~ % 162.75/22.48 (v6 = 0)))) & ! [v2: $i] : ! [v3: int] : ! [v4: $i] : (v3 = 0 | ~ % 162.75/22.48 (aElementOf0(v2, v1) = v3) | ~ (sdtasdt0(xb, v4) = v2) | ~ $i(v4) | ~ % 162.75/22.48 $i(v2) | ? [v5: int] : ( ~ (v5 = 0) & aElement0(v4) = v5)) & ! [v2: $i] % 162.75/22.48 : ! [v3: int] : ! [v4: $i] : (v3 = 0 | ~ (aElementOf0(v2, v1) = v3) | ~ % 162.75/22.48 (aElement0(v4) = 0) | ~ $i(v4) | ~ $i(v2) | ? [v5: $i] : ( ~ (v5 = v2) % 162.75/22.48 & sdtasdt0(xb, v4) = v5 & $i(v5))) & ! [v2: $i] : ! [v3: int] : ! % 162.75/22.48 [v4: $i] : (v3 = 0 | ~ (aElementOf0(v2, v0) = v3) | ~ (sdtasdt0(xa, v4) = % 162.75/22.48 v2) | ~ $i(v4) | ~ $i(v2) | ? [v5: int] : ( ~ (v5 = 0) & % 162.75/22.48 aElement0(v4) = v5)) & ! [v2: $i] : ! [v3: int] : ! [v4: $i] : (v3 = % 162.75/22.48 0 | ~ (aElementOf0(v2, v0) = v3) | ~ (aElement0(v4) = 0) | ~ $i(v4) | % 162.75/22.48 ~ $i(v2) | ? [v5: $i] : ( ~ (v5 = v2) & sdtasdt0(xa, v4) = v5 & $i(v5))) % 162.75/22.48 & ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (aElementOf0(v2, xI) = 0) | % 162.75/22.48 ~ (sdtasdt0(v3, v2) = v4) | ~ $i(v3) | ~ $i(v2) | ? [v5: any] : ? [v6: % 162.75/22.48 any] : (aElementOf0(v4, xI) = v6 & aElement0(v3) = v5 & ( ~ (v5 = 0) | % 162.75/22.48 v6 = 0))) & ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 162.75/22.48 (aElementOf0(v2, xI) = 0) | ~ (sdtpldt0(v2, v3) = v4) | ~ $i(v3) | ~ % 162.75/22.48 $i(v2) | ? [v5: any] : ? [v6: any] : (aElementOf0(v4, xI) = v6 & % 162.75/22.48 aElementOf0(v3, xI) = v5 & ( ~ (v5 = 0) | v6 = 0))) & ! [v2: $i] : ! % 162.75/22.48 [v3: $i] : ( ~ (aElementOf0(v3, xI) = 0) | ~ (aElementOf0(v2, xI) = 0) | ~ % 162.75/22.48 $i(v3) | ~ $i(v2) | ? [v4: $i] : (aElementOf0(v4, xI) = 0 & sdtpldt0(v2, % 162.75/22.48 v3) = v4 & $i(v4))) & ! [v2: $i] : ! [v3: $i] : ( ~ (aElementOf0(v2, % 162.75/22.48 xI) = 0) | ~ (aElement0(v3) = 0) | ~ $i(v3) | ~ $i(v2) | ? [v4: % 162.75/22.48 $i] : (aElementOf0(v4, xI) = 0 & sdtasdt0(v3, v2) = v4 & $i(v4))) & ! % 162.75/22.48 [v2: $i] : ( ~ (aElementOf0(v2, v1) = 0) | ~ $i(v2) | ? [v3: $i] : % 162.75/22.48 (sdtasdt0(xb, v3) = v2 & aElement0(v3) = 0 & $i(v3))) & ! [v2: $i] : ( ~ % 162.75/22.48 (aElementOf0(v2, v0) = 0) | ~ $i(v2) | ? [v3: $i] : (sdtasdt0(xa, v3) = % 162.75/22.48 v2 & aElement0(v3) = 0 & $i(v3))) & ! [v2: $i] : ( ~ (aElementOf0(v2, % 162.75/22.48 xI) = 0) | ~ $i(v2) | ? [v3: $i] : ? [v4: $i] : (aElementOf0(v4, % 162.75/22.48 v1) = 0 & aElementOf0(v3, v0) = 0 & sdtpldt0(v3, v4) = v2 & $i(v4) & % 162.75/22.48 $i(v3)))) % 162.75/22.48 % 162.75/22.48 (m__2203) % 162.75/22.48 $i(xb) & $i(xa) & $i(sz00) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 162.75/22.48 $i] : ? [v4: $i] : ? [v5: $i] : (slsdtgt0(xb) = v1 & slsdtgt0(xa) = v0 & % 162.75/22.48 aElementOf0(xb, v1) = 0 & aElementOf0(xa, v0) = 0 & aElementOf0(sz00, v1) = % 162.75/22.48 0 & aElementOf0(sz00, v0) = 0 & sdtasdt0(xb, v3) = sz00 & sdtasdt0(xb, v2) = % 162.75/22.48 xb & sdtasdt0(xa, v5) = sz00 & sdtasdt0(xa, v4) = xa & aElement0(v5) = 0 & % 162.75/22.48 aElement0(v4) = 0 & aElement0(v3) = 0 & aElement0(v2) = 0 & $i(v5) & $i(v4) % 162.75/22.48 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 162.75/22.48 % 162.75/22.48 (m__2228) % 162.75/22.49 $i(xb) & $i(xa) & $i(sz00) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 162.75/22.49 $i] : ? [v4: $i] : ? [v5: $i] : ( ~ (v3 = sz00) & slsdtgt0(xb) = v1 & % 162.75/22.49 slsdtgt0(xa) = v0 & sdtpldt1(v0, v1) = v2 & aElementOf0(v5, v1) = 0 & % 162.75/22.49 aElementOf0(v4, v0) = 0 & aElementOf0(v3, v2) = 0 & sdtpldt0(v4, v5) = v3 & % 162.75/22.49 $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ! [v6: $i] : ! [v7: % 162.75/22.49 int] : ! [v8: $i] : (v7 = 0 | ~ (aElementOf0(v6, v1) = v7) | ~ % 162.75/22.49 (sdtasdt0(xb, v8) = v6) | ~ $i(v8) | ~ $i(v6) | ? [v9: int] : ( ~ (v9 = % 162.75/22.49 0) & aElement0(v8) = v9)) & ! [v6: $i] : ! [v7: int] : ! [v8: $i] : % 162.75/22.49 (v7 = 0 | ~ (aElementOf0(v6, v1) = v7) | ~ (aElement0(v8) = 0) | ~ $i(v8) % 162.75/22.49 | ~ $i(v6) | ? [v9: $i] : ( ~ (v9 = v6) & sdtasdt0(xb, v8) = v9 & % 162.75/22.49 $i(v9))) & ! [v6: $i] : ! [v7: int] : ! [v8: $i] : (v7 = 0 | ~ % 162.75/22.49 (aElementOf0(v6, v0) = v7) | ~ (sdtasdt0(xa, v8) = v6) | ~ $i(v8) | ~ % 162.75/22.49 $i(v6) | ? [v9: int] : ( ~ (v9 = 0) & aElement0(v8) = v9)) & ! [v6: $i] % 162.75/22.49 : ! [v7: int] : ! [v8: $i] : (v7 = 0 | ~ (aElementOf0(v6, v0) = v7) | ~ % 162.75/22.49 (aElement0(v8) = 0) | ~ $i(v8) | ~ $i(v6) | ? [v9: $i] : ( ~ (v9 = v6) % 162.75/22.49 & sdtasdt0(xa, v8) = v9 & $i(v9))) & ! [v6: $i] : ( ~ (aElementOf0(v6, % 162.75/22.49 v1) = 0) | ~ $i(v6) | ? [v7: $i] : (sdtasdt0(xb, v7) = v6 & % 162.75/22.49 aElement0(v7) = 0 & $i(v7))) & ! [v6: $i] : ( ~ (aElementOf0(v6, v0) = % 162.75/22.49 0) | ~ $i(v6) | ? [v7: $i] : (sdtasdt0(xa, v7) = v6 & aElement0(v7) = % 162.75/22.49 0 & $i(v7)))) % 162.75/22.49 % 162.75/22.49 (m__2273) % 162.75/22.49 $i(xu) & $i(xI) & $i(xb) & $i(xa) & $i(sz00) & ? [v0: $i] : ? [v1: $i] : ? % 162.75/22.49 [v2: $i] : ? [v3: $i] : ? [v4: $i] : ( ~ (xu = sz00) & slsdtgt0(xb) = v1 & % 162.75/22.49 slsdtgt0(xa) = v0 & sbrdtbr0(xu) = v2 & aElementOf0(v4, v1) = 0 & % 162.75/22.49 aElementOf0(v3, v0) = 0 & aElementOf0(xu, xI) = 0 & sdtpldt0(v3, v4) = xu & % 162.75/22.49 $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ! [v5: $i] : ! [v6: % 162.75/22.49 MultipleValueBool] : ! [v7: $i] : ! [v8: $i] : (v5 = sz00 | ~ % 162.75/22.49 (aElementOf0(v5, xI) = v6) | ~ (sdtpldt0(v7, v8) = v5) | ~ $i(v8) | ~ % 162.75/22.49 $i(v7) | ~ $i(v5) | ? [v9: any] : ? [v10: int] : (( ~ (v10 = 0) & % 162.75/22.49 iLess0(v9, v2) = v10 & sbrdtbr0(v5) = v9 & $i(v9)) | (aElementOf0(v8, % 162.75/22.49 v1) = v10 & aElementOf0(v7, v0) = v9 & ( ~ (v10 = 0) | ~ (v9 = % 162.75/22.49 0))))) & ! [v5: $i] : ! [v6: $i] : (v5 = sz00 | ~ (sbrdtbr0(v5) % 162.75/22.49 = v6) | ~ $i(v5) | ? [v7: any] : ? [v8: any] : (iLess0(v6, v2) = v8 & % 162.75/22.49 aElementOf0(v5, xI) = v7 & ( ~ (v8 = 0) | ( ~ (v7 = 0) & ! [v9: $i] : % 162.75/22.49 ! [v10: $i] : ( ~ (sdtpldt0(v9, v10) = v5) | ~ $i(v10) | ~ $i(v9) % 162.75/22.49 | ? [v11: any] : ? [v12: any] : (aElementOf0(v10, v1) = v12 & % 162.75/22.49 aElementOf0(v9, v0) = v11 & ( ~ (v12 = 0) | ~ (v11 = 0)))))))) % 162.75/22.49 & ! [v5: $i] : (v5 = sz00 | ~ (aElementOf0(v5, xI) = 0) | ~ $i(v5) | ? % 162.75/22.49 [v6: $i] : ? [v7: int] : ( ~ (v7 = 0) & iLess0(v6, v2) = v7 & % 162.75/22.49 sbrdtbr0(v5) = v6 & $i(v6)))) % 162.75/22.49 % 162.75/22.49 (m__2383) % 162.75/22.50 $i(xu) & $i(xb) & $i(xa) & ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 162.75/22.50 [v3: any] : (aDivisorOf0(xu, xb) = v3 & aDivisorOf0(xu, xa) = v1 & % 162.75/22.50 doDivides0(xu, xb) = v2 & doDivides0(xu, xa) = v0 & (( ~ (v3 = 0) & ~ (v2 = % 162.75/22.50 0) & ! [v4: $i] : ( ~ (sdtasdt0(xu, v4) = xb) | ~ $i(v4) | ? [v5: % 162.75/22.50 int] : ( ~ (v5 = 0) & aElement0(v4) = v5)) & ! [v4: $i] : ( ~ % 162.75/22.50 (aElement0(v4) = 0) | ~ $i(v4) | ? [v5: $i] : ( ~ (v5 = xb) & % 162.75/22.50 sdtasdt0(xu, v4) = v5 & $i(v5)))) | ( ~ (v1 = 0) & ~ (v0 = 0) & ! % 162.75/22.50 [v4: $i] : ( ~ (sdtasdt0(xu, v4) = xa) | ~ $i(v4) | ? [v5: int] : ( ~ % 162.75/22.50 (v5 = 0) & aElement0(v4) = v5)) & ! [v4: $i] : ( ~ (aElement0(v4) = % 162.75/22.50 0) | ~ $i(v4) | ? [v5: $i] : ( ~ (v5 = xa) & sdtasdt0(xu, v4) = v5 % 162.75/22.50 & $i(v5)))))) % 162.75/22.50 % 162.75/22.50 (m__2416) % 162.75/22.50 $i(xu) & $i(xb) & $i(xa) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 162.75/22.50 $i] : (sdtasdt0(xb, v1) = v3 & sdtasdt0(xa, v0) = v2 & sdtpldt0(v2, v3) = xu % 162.75/22.50 & aElement0(v1) = 0 & aElement0(v0) = 0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 162.75/22.50 % 162.75/22.50 (m__2479) % 162.75/22.50 $i(xu) & $i(xa) & ? [v0: $i] : (doDivides0(xu, xa) = 0 & sdtasdt0(xu, v0) = % 162.75/22.50 xa & aElement0(v0) = 0 & $i(v0)) % 162.75/22.50 % 162.75/22.50 (m__2612) % 162.75/22.50 $i(xu) & $i(xb) & ? [v0: int] : ( ~ (v0 = 0) & doDivides0(xu, xb) = v0 & ! % 162.75/22.50 [v1: $i] : ( ~ (sdtasdt0(xu, v1) = xb) | ~ $i(v1) | ? [v2: int] : ( ~ (v2 % 162.75/22.50 = 0) & aElement0(v1) = v2)) & ! [v1: $i] : ( ~ (aElement0(v1) = 0) | % 162.75/22.50 ~ $i(v1) | ? [v2: $i] : ( ~ (v2 = xb) & sdtasdt0(xu, v1) = v2 & $i(v2)))) % 162.75/22.50 % 162.75/22.50 (m__2666) % 162.75/22.50 $i(xr) & $i(xq) & $i(xu) & $i(xb) & $i(sz00) & ? [v0: $i] : ? [v1: $i] : ? % 162.75/22.50 [v2: $i] : ? [v3: any] : (iLess0(v1, v2) = v3 & sbrdtbr0(xr) = v1 & % 162.75/22.50 sbrdtbr0(xu) = v2 & sdtasdt0(xq, xu) = v0 & sdtpldt0(v0, xr) = xb & % 162.75/22.50 aElement0(xr) = 0 & aElement0(xq) = 0 & $i(v2) & $i(v1) & $i(v0) & (v3 = 0 | % 162.75/22.50 xr = sz00)) % 162.75/22.50 % 162.75/22.50 (function-axioms) % 162.75/22.51 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 162.75/22.51 [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (aGcdOfAnd0(v4, v3, v2) = v1) | ~ % 162.75/22.51 (aGcdOfAnd0(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 162.75/22.51 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 162.75/22.51 (sdteqdtlpzmzozddtrp0(v4, v3, v2) = v1) | ~ (sdteqdtlpzmzozddtrp0(v4, v3, % 162.75/22.51 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 162.75/22.51 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (misRelativelyPrime0(v3, v2) = v1) | % 162.75/22.51 ~ (misRelativelyPrime0(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 162.75/22.51 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 162.75/22.51 (aDivisorOf0(v3, v2) = v1) | ~ (aDivisorOf0(v3, v2) = v0)) & ! [v0: % 162.75/22.51 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 162.75/22.51 : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ (doDivides0(v3, v2) = v0)) & ! % 162.75/22.51 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 162.75/22.51 $i] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) & ! % 162.75/22.51 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 162.75/22.51 (sdtasasdt0(v3, v2) = v1) | ~ (sdtasasdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 162.75/22.51 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtpldt1(v3, v2) = v1) | % 162.75/22.51 ~ (sdtpldt1(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 162.75/22.51 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 162.75/22.51 (aElementOf0(v3, v2) = v1) | ~ (aElementOf0(v3, v2) = v0)) & ! [v0: $i] : % 162.75/22.51 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) % 162.75/22.51 | ~ (sdtasdt0(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 162.75/22.51 [v3: $i] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 162.75/22.51 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (slsdtgt0(v2) = v1) % 162.75/22.51 | ~ (slsdtgt0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = % 162.75/22.51 v0 | ~ (sbrdtbr0(v2) = v1) | ~ (sbrdtbr0(v2) = v0)) & ! [v0: % 162.75/22.51 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 162.75/22.51 ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = v0)) & ! [v0: % 162.75/22.51 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 162.75/22.51 ~ (aIdeal0(v2) = v1) | ~ (aIdeal0(v2) = v0)) & ! [v0: MultipleValueBool] : % 162.75/22.51 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aSet0(v2) = v1) | ~ % 162.75/22.51 (aSet0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 162.75/22.51 (smndt0(v2) = v1) | ~ (smndt0(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 162.75/22.51 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aElement0(v2) = v1) | % 162.75/22.51 ~ (aElement0(v2) = v0)) % 162.75/22.51 % 162.75/22.51 Further assumptions not needed in the proof: % 162.75/22.51 -------------------------------------------- % 162.75/22.51 mAddAsso, mAddInvr, mCancel, mChineseRemainder, mDefDiv, mDefGCD, mDefMod, % 162.75/22.51 mDefPrIdeal, mDefSInt, mDefSSum, mElmSort, mIdeInt, mIdeSum, mMulMnOne, % 162.75/22.51 mMulUnit, mMulZero, mNatLess, mNatSort, mPrIdeal, mSetEq, mSetSort, mSortsC, % 162.75/22.51 mSortsU, m__2110 % 162.75/22.51 % 162.75/22.51 Those formulas are unsatisfiable: % 162.75/22.51 --------------------------------- % 162.75/22.51 % 162.75/22.51 Begin of proof % 162.75/22.51 | % 162.75/22.51 | ALPHA: (mSortsC_01) implies: % 162.75/22.51 | (1) aElement0(sz10) = 0 % 162.75/22.51 | % 162.75/22.51 | ALPHA: (mAddComm) implies: % 162.75/22.52 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | % 162.75/22.52 | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 162.75/22.52 | (sdtpldt0(v1, v0) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & % 162.75/22.52 | $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 162.75/22.52 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v1, v0) = v2) | % 162.75/22.52 | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 162.75/22.52 | (sdtpldt0(v0, v1) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & % 162.75/22.52 | $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 162.75/22.52 | % 162.75/22.52 | ALPHA: (mAddZero) implies: % 162.75/22.52 | (4) ! [v0: $i] : ! [v1: $i] : ( ~ (sdtpldt0(v0, sz00) = v1) | ~ $i(v0) | % 162.75/22.52 | ? [v2: any] : ? [v3: $i] : (sdtpldt0(sz00, v0) = v3 & aElement0(v0) % 162.75/22.52 | = v2 & $i(v3) & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) % 162.75/22.52 | % 162.75/22.52 | ALPHA: (mMulComm) implies: % 162.75/22.52 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | % 162.75/22.52 | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 162.75/22.52 | (sdtasdt0(v1, v0) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & % 162.75/22.52 | $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 162.75/22.52 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v1, v0) = v2) | % 162.75/22.52 | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 162.75/22.52 | (sdtasdt0(v0, v1) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & % 162.75/22.52 | $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 162.75/22.52 | % 162.75/22.52 | ALPHA: (mMulAsso) implies: % 162.75/22.52 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 162.75/22.52 | ~ (sdtasdt0(v3, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | % 162.75/22.52 | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : % 162.75/22.52 | ? [v8: $i] : ? [v9: $i] : (sdtasdt0(v1, v2) = v8 & sdtasdt0(v0, v8) % 162.75/22.52 | = v9 & aElement0(v2) = v7 & aElement0(v1) = v6 & aElement0(v0) = v5 % 162.75/22.52 | & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v9 = % 162.75/22.52 | v4))) % 162.75/22.52 | % 162.75/22.52 | ALPHA: (mAMDistr) implies: % 162.75/22.52 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 162.75/22.52 | ~ (sdtasdt0(v0, v3) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ $i(v2) | % 162.75/22.52 | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : % 162.75/22.52 | ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] % 162.75/22.52 | : ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v3, v0) = v11 & % 162.75/22.52 | sdtasdt0(v2, v0) = v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v2) % 162.75/22.52 | = v9 & sdtasdt0(v0, v1) = v8 & sdtpldt0(v12, v13) = v14 & % 162.75/22.52 | sdtpldt0(v8, v9) = v10 & aElement0(v2) = v7 & aElement0(v1) = v6 & % 162.75/22.52 | aElement0(v0) = v5 & $i(v14) & $i(v13) & $i(v12) & $i(v11) & % 162.75/22.52 | $i(v10) & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = % 162.75/22.52 | 0) | (v14 = v11 & v10 = v4)))) % 162.75/22.53 | (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 162.75/22.53 | ~ (sdtasdt0(v3, v0) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ $i(v2) | % 162.75/22.53 | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : % 162.75/22.53 | ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] % 162.75/22.53 | : ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v2, v0) = v13 & % 162.75/22.53 | sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v3) = v8 & sdtasdt0(v0, v2) = % 162.75/22.53 | v10 & sdtasdt0(v0, v1) = v9 & sdtpldt0(v12, v13) = v14 & % 162.75/22.53 | sdtpldt0(v9, v10) = v11 & aElement0(v2) = v7 & aElement0(v1) = v6 & % 162.75/22.53 | aElement0(v0) = v5 & $i(v14) & $i(v13) & $i(v12) & $i(v11) & % 162.75/22.53 | $i(v10) & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = % 162.75/22.53 | 0) | (v14 = v4 & v11 = v8)))) % 162.75/22.53 | % 162.75/22.53 | ALPHA: (mUnNeZr) implies: % 162.75/22.53 | (10) ~ (sz10 = sz00) % 162.75/22.53 | % 162.75/22.53 | ALPHA: (mEOfElem) implies: % 162.75/22.53 | (11) ! [v0: $i] : ! [v1: $i] : ( ~ (aSet0(v0) = 0) | ~ (aElementOf0(v1, % 162.75/22.53 | v0) = 0) | ~ $i(v1) | ~ $i(v0) | aElement0(v1) = 0) % 162.75/22.53 | % 162.75/22.53 | ALPHA: (mDefIdeal) implies: % 162.75/22.53 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 162.75/22.53 | (aIdeal0(v0) = 0) | ~ (aElementOf0(v1, v0) = 0) | ~ (sdtasdt0(v2, % 162.75/22.53 | v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : % 162.75/22.53 | ? [v5: any] : (aElementOf0(v3, v0) = v5 & aElement0(v2) = v4 & ( ~ % 162.75/22.53 | (v4 = 0) | v5 = 0))) % 162.75/22.53 | % 162.75/22.53 | ALPHA: (mEucSort) implies: % 162.75/22.53 | (13) ! [v0: $i] : ! [v1: $i] : (v0 = sz00 | ~ (sbrdtbr0(v0) = v1) | ~ % 162.75/22.53 | $i(v0) | ? [v2: any] : ? [v3: any] : (aNaturalNumber0(v1) = v3 & % 162.75/22.53 | aElement0(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 162.75/22.53 | % 162.75/22.53 | ALPHA: (mDivision) implies: % 162.75/22.53 | (14) ! [v0: $i] : ! [v1: $i] : (v1 = sz00 | ~ (aElement0(v1) = 0) | ~ % 162.75/22.53 | (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: $i] : ? [v3: % 162.75/22.53 | $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: any] : % 162.75/22.53 | (iLess0(v6, v2) = v7 & sbrdtbr0(v4) = v6 & sbrdtbr0(v1) = v2 & % 162.75/22.53 | sdtasdt0(v3, v1) = v5 & sdtpldt0(v5, v4) = v0 & aElement0(v4) = 0 % 162.75/22.53 | & aElement0(v3) = 0 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & % 162.75/22.53 | (v7 = 0 | v4 = sz00))) % 162.75/22.53 | % 162.75/22.53 | ALPHA: (mDefDvs) implies: % 162.75/22.53 | (15) ! [v0: $i] : ! [v1: $i] : ( ~ (doDivides0(v1, v0) = 0) | ~ % 162.75/22.53 | (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: any] : ? [v3: % 162.75/22.53 | any] : (aDivisorOf0(v1, v0) = v3 & aElement0(v1) = v2 & ( ~ (v2 = % 162.75/22.53 | 0) | v3 = 0))) % 162.75/22.53 | (16) ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (doDivides0(v1, v0) = % 162.75/22.53 | v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v3: % 162.75/22.53 | any] : ? [v4: any] : (aDivisorOf0(v1, v0) = v3 & aElement0(v1) = % 162.75/22.53 | v4 & ( ~ (v3 = 0) | (v4 = 0 & v2 = 0)))) % 162.75/22.53 | % 162.75/22.53 | ALPHA: (mDefRel) implies: % 162.75/22.53 | (17) $i(sz10) % 162.75/22.53 | % 162.75/22.53 | ALPHA: (m__2091) implies: % 162.75/22.53 | (18) aElement0(xa) = 0 % 162.75/22.53 | (19) aElement0(xb) = 0 % 162.75/22.53 | % 162.75/22.53 | ALPHA: (m__2129) implies: % 163.10/22.55 | (20) ? [v0: $i] : ? [v1: $i] : (aGcdOfAnd0(xc, xa, xb) = 0 & % 163.10/22.55 | aDivisorOf0(xc, xb) = 0 & aDivisorOf0(xc, xa) = 0 & doDivides0(xc, % 163.10/22.55 | xb) = 0 & doDivides0(xc, xa) = 0 & sdtasdt0(xc, v1) = xa & % 163.10/22.55 | sdtasdt0(xc, v0) = xb & aElement0(v1) = 0 & aElement0(v0) = 0 & % 163.10/22.55 | aElement0(xc) = 0 & $i(v1) & $i(v0) & ! [v2: $i] : ! [v3: int] : % 163.10/22.55 | (v3 = 0 | ~ (doDivides0(v2, xc) = v3) | ~ $i(v2) | ? [v4: any] : % 163.10/22.55 | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : % 163.10/22.55 | (aDivisorOf0(v2, xb) = v8 & aDivisorOf0(v2, xa) = v6 & % 163.10/22.55 | doDivides0(v2, xb) = v7 & doDivides0(v2, xa) = v5 & % 163.10/22.55 | aElement0(v2) = v4 & (( ~ (v8 = 0) & ~ (v7 = 0) & ! [v9: $i] : % 163.10/22.55 | ( ~ (sdtasdt0(v2, v9) = xb) | ~ $i(v9) | ? [v10: int] : ( % 163.10/22.55 | ~ (v10 = 0) & aElement0(v9) = v10)) & ! [v9: $i] : ( ~ % 163.10/22.55 | (aElement0(v9) = 0) | ~ $i(v9) | ? [v10: $i] : ( ~ (v10 % 163.10/22.55 | = xb) & sdtasdt0(v2, v9) = v10 & $i(v10)))) | ( ~ (v6 % 163.10/22.55 | = 0) & ( ~ (v4 = 0) | ( ~ (v5 = 0) & ! [v9: $i] : ( ~ % 163.10/22.55 | (sdtasdt0(v2, v9) = xa) | ~ $i(v9) | ? [v10: int] : % 163.10/22.55 | ( ~ (v10 = 0) & aElement0(v9) = v10)) & ! [v9: $i] : % 163.10/22.55 | ( ~ (aElement0(v9) = 0) | ~ $i(v9) | ? [v10: $i] : ( ~ % 163.10/22.55 | (v10 = xa) & sdtasdt0(v2, v9) = v10 & % 163.10/22.55 | $i(v10))))))))) & ! [v2: $i] : ! [v3: any] : ( ~ % 163.10/22.55 | (aDivisorOf0(v2, xb) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: % 163.10/22.55 | any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] % 163.10/22.55 | : ? [v10: int] : ? [v11: $i] : (aDivisorOf0(v2, xa) = v6 & % 163.10/22.55 | doDivides0(v2, xc) = v8 & doDivides0(v2, xb) = v7 & % 163.10/22.55 | doDivides0(v2, xa) = v5 & aElement0(v2) = v4 & $i(v9) & ((v11 = % 163.10/22.55 | xc & v10 = 0 & v8 = 0 & sdtasdt0(v2, v9) = xc & % 163.10/22.55 | aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v3 = 0) & ! [v12: % 163.10/22.55 | $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? [v13: % 163.10/22.55 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! [v12: % 163.10/22.55 | $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] % 163.10/22.55 | : ( ~ (v13 = xb) & sdtasdt0(v2, v12) = v13 & $i(v13)))) | % 163.10/22.55 | ( ~ (v6 = 0) & ( ~ (v4 = 0) | ( ~ (v5 = 0) & ! [v12: $i] : ( % 163.10/22.55 | ~ (sdtasdt0(v2, v12) = xa) | ~ $i(v12) | ? [v13: % 163.10/22.55 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! % 163.10/22.55 | [v12: $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? % 163.10/22.55 | [v13: $i] : ( ~ (v13 = xa) & sdtasdt0(v2, v12) = v13 & % 163.10/22.55 | $i(v13))))))))) & ! [v2: $i] : ! [v3: any] : ( ~ % 163.10/22.55 | (aDivisorOf0(v2, xa) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: % 163.10/22.55 | any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] % 163.10/22.55 | : ? [v10: int] : ? [v11: $i] : (aDivisorOf0(v2, xb) = v7 & % 163.10/22.55 | doDivides0(v2, xc) = v8 & doDivides0(v2, xb) = v6 & % 163.10/22.55 | doDivides0(v2, xa) = v5 & aElement0(v2) = v4 & $i(v9) & ((v11 = % 163.10/22.55 | xc & v10 = 0 & v8 = 0 & sdtasdt0(v2, v9) = xc & % 163.10/22.55 | aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v6 = 0) & ! [v12: % 163.10/22.55 | $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? [v13: % 163.10/22.55 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! [v12: % 163.10/22.55 | $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] % 163.10/22.55 | : ( ~ (v13 = xb) & sdtasdt0(v2, v12) = v13 & $i(v13)))) | % 163.10/22.55 | ( ~ (v3 = 0) & ( ~ (v4 = 0) | ( ~ (v5 = 0) & ! [v12: $i] : ( % 163.10/22.55 | ~ (sdtasdt0(v2, v12) = xa) | ~ $i(v12) | ? [v13: % 163.10/22.55 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! % 163.10/22.55 | [v12: $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? % 163.10/22.55 | [v13: $i] : ( ~ (v13 = xa) & sdtasdt0(v2, v12) = v13 & % 163.10/22.55 | $i(v13))))))))) & ! [v2: $i] : ! [v3: % 163.10/22.55 | MultipleValueBool] : ( ~ (doDivides0(v2, xc) = v3) | ~ $i(v2) | % 163.10/22.55 | ? [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: % 163.10/22.55 | any] : ? [v9: $i] : ? [v10: int] : ? [v11: $i] : ($i(v9) & % 163.10/22.55 | ((v11 = xc & v10 = 0 & sdtasdt0(v2, v9) = xc & aElement0(v9) = % 163.10/22.55 | 0) | (aDivisorOf0(v2, xb) = v8 & aDivisorOf0(v2, xa) = v6 & % 163.10/22.55 | doDivides0(v2, xb) = v7 & doDivides0(v2, xa) = v5 & % 163.10/22.55 | aElement0(v2) = v4 & (( ~ (v8 = 0) & ~ (v7 = 0) & ! [v12: % 163.10/22.55 | $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? % 163.10/22.55 | [v13: int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & % 163.10/22.55 | ! [v12: $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? % 163.10/22.55 | [v13: $i] : ( ~ (v13 = xb) & sdtasdt0(v2, v12) = v13 & % 163.10/22.55 | $i(v13)))) | ( ~ (v6 = 0) & ( ~ (v4 = 0) | ( ~ (v5 = % 163.10/22.55 | 0) & ! [v12: $i] : ( ~ (sdtasdt0(v2, v12) = xa) | % 163.10/22.55 | ~ $i(v12) | ? [v13: int] : ( ~ (v13 = 0) & % 163.10/22.55 | aElement0(v12) = v13)) & ! [v12: $i] : ( ~ % 163.10/22.55 | (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] : % 163.10/22.55 | ( ~ (v13 = xa) & sdtasdt0(v2, v12) = v13 & % 163.10/22.55 | $i(v13))))))))))) & ! [v2: $i] : ! [v3: any] : % 163.10/22.55 | ( ~ (doDivides0(v2, xb) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: % 163.10/22.55 | any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] % 163.10/22.55 | : ? [v10: int] : ? [v11: $i] : (aDivisorOf0(v2, xb) = v7 & % 163.10/22.55 | aDivisorOf0(v2, xa) = v6 & doDivides0(v2, xc) = v8 & % 163.10/22.55 | doDivides0(v2, xa) = v5 & aElement0(v2) = v4 & $i(v9) & ((v11 = % 163.10/22.55 | xc & v10 = 0 & v8 = 0 & sdtasdt0(v2, v9) = xc & % 163.10/22.55 | aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v3 = 0) & ! [v12: % 163.10/22.55 | $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? [v13: % 163.10/22.55 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! [v12: % 163.10/22.55 | $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] % 163.10/22.55 | : ( ~ (v13 = xb) & sdtasdt0(v2, v12) = v13 & $i(v13)))) | % 163.10/22.55 | ( ~ (v6 = 0) & ( ~ (v4 = 0) | ( ~ (v5 = 0) & ! [v12: $i] : ( % 163.10/22.55 | ~ (sdtasdt0(v2, v12) = xa) | ~ $i(v12) | ? [v13: % 163.10/22.55 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! % 163.10/22.55 | [v12: $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? % 163.10/22.55 | [v13: $i] : ( ~ (v13 = xa) & sdtasdt0(v2, v12) = v13 & % 163.10/22.55 | $i(v13))))))))) & ! [v2: $i] : ! [v3: any] : ( ~ % 163.10/22.55 | (doDivides0(v2, xa) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: % 163.10/22.55 | any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] % 163.10/22.55 | : ? [v10: int] : ? [v11: $i] : (aDivisorOf0(v2, xb) = v7 & % 163.10/22.55 | aDivisorOf0(v2, xa) = v5 & doDivides0(v2, xc) = v8 & % 163.10/22.55 | doDivides0(v2, xb) = v6 & aElement0(v2) = v4 & $i(v9) & ((v11 = % 163.10/22.55 | xc & v10 = 0 & v8 = 0 & sdtasdt0(v2, v9) = xc & % 163.10/22.55 | aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v6 = 0) & ! [v12: % 163.10/22.55 | $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? [v13: % 163.10/22.55 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! [v12: % 163.10/22.55 | $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] % 163.10/22.55 | : ( ~ (v13 = xb) & sdtasdt0(v2, v12) = v13 & $i(v13)))) | % 163.10/22.55 | ( ~ (v5 = 0) & ( ~ (v4 = 0) | ( ~ (v3 = 0) & ! [v12: $i] : ( % 163.10/22.55 | ~ (sdtasdt0(v2, v12) = xa) | ~ $i(v12) | ? [v13: % 163.10/22.55 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! % 163.10/22.55 | [v12: $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? % 163.10/22.55 | [v13: $i] : ( ~ (v13 = xa) & sdtasdt0(v2, v12) = v13 & % 163.10/22.55 | $i(v13))))))))) & ! [v2: $i] : ! [v3: any] : ( ~ % 163.10/22.55 | (aElement0(v2) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: any] : % 163.10/22.55 | ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? [v10: % 163.10/22.55 | int] : ? [v11: $i] : (aDivisorOf0(v2, xb) = v7 & % 163.10/22.55 | aDivisorOf0(v2, xa) = v5 & doDivides0(v2, xc) = v8 & % 163.10/22.55 | doDivides0(v2, xb) = v6 & doDivides0(v2, xa) = v4 & $i(v9) & % 163.10/22.55 | ((v11 = xc & v10 = 0 & v8 = 0 & sdtasdt0(v2, v9) = xc & % 163.10/22.55 | aElement0(v9) = 0) | ( ~ (v7 = 0) & ~ (v6 = 0) & ! [v12: % 163.10/22.55 | $i] : ( ~ (sdtasdt0(v2, v12) = xb) | ~ $i(v12) | ? [v13: % 163.10/22.55 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! [v12: % 163.10/22.55 | $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? [v13: $i] % 163.10/22.55 | : ( ~ (v13 = xb) & sdtasdt0(v2, v12) = v13 & $i(v13)))) | % 163.10/22.55 | ( ~ (v5 = 0) & ( ~ (v3 = 0) | ( ~ (v4 = 0) & ! [v12: $i] : ( % 163.10/22.55 | ~ (sdtasdt0(v2, v12) = xa) | ~ $i(v12) | ? [v13: % 163.10/22.55 | int] : ( ~ (v13 = 0) & aElement0(v12) = v13)) & ! % 163.10/22.55 | [v12: $i] : ( ~ (aElement0(v12) = 0) | ~ $i(v12) | ? % 163.10/22.55 | [v13: $i] : ( ~ (v13 = xa) & sdtasdt0(v2, v12) = v13 & % 163.10/22.55 | $i(v13)))))))))) % 163.10/22.55 | % 163.10/22.55 | ALPHA: (m__2174) implies: % 163.10/22.56 | (21) ? [v0: $i] : ? [v1: $i] : (slsdtgt0(xb) = v1 & slsdtgt0(xa) = v0 & % 163.10/22.56 | aIdeal0(xI) = 0 & sdtpldt1(v0, v1) = xI & aSet0(xI) = 0 & $i(v1) & % 163.10/22.56 | $i(v0) & ! [v2: $i] : ! [v3: int] : ! [v4: $i] : ! [v5: $i] : % 163.10/22.56 | (v3 = 0 | ~ (aElementOf0(v2, xI) = v3) | ~ (sdtpldt0(v4, v5) = v2) % 163.10/22.56 | | ~ $i(v5) | ~ $i(v4) | ~ $i(v2) | ? [v6: any] : ? [v7: any] % 163.10/22.56 | : (aElementOf0(v5, v1) = v7 & aElementOf0(v4, v0) = v6 & ( ~ (v7 = % 163.10/22.56 | 0) | ~ (v6 = 0)))) & ! [v2: $i] : ! [v3: int] : ! [v4: % 163.10/22.56 | $i] : (v3 = 0 | ~ (aElementOf0(v2, v1) = v3) | ~ (sdtasdt0(xb, % 163.10/22.56 | v4) = v2) | ~ $i(v4) | ~ $i(v2) | ? [v5: int] : ( ~ (v5 = % 163.10/22.56 | 0) & aElement0(v4) = v5)) & ! [v2: $i] : ! [v3: int] : ! % 163.10/22.56 | [v4: $i] : (v3 = 0 | ~ (aElementOf0(v2, v1) = v3) | ~ % 163.10/22.56 | (aElement0(v4) = 0) | ~ $i(v4) | ~ $i(v2) | ? [v5: $i] : ( ~ % 163.10/22.56 | (v5 = v2) & sdtasdt0(xb, v4) = v5 & $i(v5))) & ! [v2: $i] : ! % 163.10/22.56 | [v3: int] : ! [v4: $i] : (v3 = 0 | ~ (aElementOf0(v2, v0) = v3) | % 163.10/22.56 | ~ (sdtasdt0(xa, v4) = v2) | ~ $i(v4) | ~ $i(v2) | ? [v5: int] : % 163.10/22.56 | ( ~ (v5 = 0) & aElement0(v4) = v5)) & ! [v2: $i] : ! [v3: int] : % 163.10/22.56 | ! [v4: $i] : (v3 = 0 | ~ (aElementOf0(v2, v0) = v3) | ~ % 163.10/22.56 | (aElement0(v4) = 0) | ~ $i(v4) | ~ $i(v2) | ? [v5: $i] : ( ~ % 163.10/22.56 | (v5 = v2) & sdtasdt0(xa, v4) = v5 & $i(v5))) & ! [v2: $i] : ! % 163.10/22.56 | [v3: $i] : ! [v4: $i] : ( ~ (aElementOf0(v2, xI) = 0) | ~ % 163.10/22.56 | (sdtasdt0(v3, v2) = v4) | ~ $i(v3) | ~ $i(v2) | ? [v5: any] : % 163.10/22.56 | ? [v6: any] : (aElementOf0(v4, xI) = v6 & aElement0(v3) = v5 & ( ~ % 163.10/22.56 | (v5 = 0) | v6 = 0))) & ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 163.10/22.56 | : ( ~ (aElementOf0(v2, xI) = 0) | ~ (sdtpldt0(v2, v3) = v4) | ~ % 163.10/22.56 | $i(v3) | ~ $i(v2) | ? [v5: any] : ? [v6: any] : % 163.10/22.56 | (aElementOf0(v4, xI) = v6 & aElementOf0(v3, xI) = v5 & ( ~ (v5 = % 163.10/22.56 | 0) | v6 = 0))) & ! [v2: $i] : ! [v3: $i] : ( ~ % 163.10/22.56 | (aElementOf0(v3, xI) = 0) | ~ (aElementOf0(v2, xI) = 0) | ~ % 163.10/22.56 | $i(v3) | ~ $i(v2) | ? [v4: $i] : (aElementOf0(v4, xI) = 0 & % 163.10/22.56 | sdtpldt0(v2, v3) = v4 & $i(v4))) & ! [v2: $i] : ! [v3: $i] : ( % 163.10/22.56 | ~ (aElementOf0(v2, xI) = 0) | ~ (aElement0(v3) = 0) | ~ $i(v3) | % 163.10/22.56 | ~ $i(v2) | ? [v4: $i] : (aElementOf0(v4, xI) = 0 & sdtasdt0(v3, % 163.10/22.56 | v2) = v4 & $i(v4))) & ! [v2: $i] : ( ~ (aElementOf0(v2, v1) = % 163.10/22.56 | 0) | ~ $i(v2) | ? [v3: $i] : (sdtasdt0(xb, v3) = v2 & % 163.10/22.56 | aElement0(v3) = 0 & $i(v3))) & ! [v2: $i] : ( ~ % 163.10/22.56 | (aElementOf0(v2, v0) = 0) | ~ $i(v2) | ? [v3: $i] : % 163.10/22.56 | (sdtasdt0(xa, v3) = v2 & aElement0(v3) = 0 & $i(v3))) & ! [v2: % 163.10/22.56 | $i] : ( ~ (aElementOf0(v2, xI) = 0) | ~ $i(v2) | ? [v3: $i] : ? % 163.10/22.56 | [v4: $i] : (aElementOf0(v4, v1) = 0 & aElementOf0(v3, v0) = 0 & % 163.10/22.56 | sdtpldt0(v3, v4) = v2 & $i(v4) & $i(v3)))) % 163.10/22.56 | % 163.10/22.56 | ALPHA: (m__2203) implies: % 163.10/22.56 | (22) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 163.10/22.56 | ? [v5: $i] : (slsdtgt0(xb) = v1 & slsdtgt0(xa) = v0 & aElementOf0(xb, % 163.10/22.56 | v1) = 0 & aElementOf0(xa, v0) = 0 & aElementOf0(sz00, v1) = 0 & % 163.10/22.56 | aElementOf0(sz00, v0) = 0 & sdtasdt0(xb, v3) = sz00 & sdtasdt0(xb, % 163.10/22.56 | v2) = xb & sdtasdt0(xa, v5) = sz00 & sdtasdt0(xa, v4) = xa & % 163.10/22.56 | aElement0(v5) = 0 & aElement0(v4) = 0 & aElement0(v3) = 0 & % 163.10/22.56 | aElement0(v2) = 0 & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & % 163.10/22.56 | $i(v0)) % 163.10/22.56 | % 163.10/22.56 | ALPHA: (m__2228) implies: % 163.10/22.56 | (23) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 163.10/22.56 | ? [v5: $i] : ( ~ (v3 = sz00) & slsdtgt0(xb) = v1 & slsdtgt0(xa) = v0 & % 163.10/22.56 | sdtpldt1(v0, v1) = v2 & aElementOf0(v5, v1) = 0 & aElementOf0(v4, % 163.10/22.56 | v0) = 0 & aElementOf0(v3, v2) = 0 & sdtpldt0(v4, v5) = v3 & $i(v5) % 163.10/22.56 | & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ! [v6: $i] : ! [v7: % 163.10/22.56 | int] : ! [v8: $i] : (v7 = 0 | ~ (aElementOf0(v6, v1) = v7) | ~ % 163.10/22.56 | (sdtasdt0(xb, v8) = v6) | ~ $i(v8) | ~ $i(v6) | ? [v9: int] : ( % 163.10/22.56 | ~ (v9 = 0) & aElement0(v8) = v9)) & ! [v6: $i] : ! [v7: int] : % 163.10/22.56 | ! [v8: $i] : (v7 = 0 | ~ (aElementOf0(v6, v1) = v7) | ~ % 163.10/22.56 | (aElement0(v8) = 0) | ~ $i(v8) | ~ $i(v6) | ? [v9: $i] : ( ~ % 163.10/22.56 | (v9 = v6) & sdtasdt0(xb, v8) = v9 & $i(v9))) & ! [v6: $i] : ! % 163.10/22.56 | [v7: int] : ! [v8: $i] : (v7 = 0 | ~ (aElementOf0(v6, v0) = v7) | % 163.10/22.56 | ~ (sdtasdt0(xa, v8) = v6) | ~ $i(v8) | ~ $i(v6) | ? [v9: int] : % 163.10/22.56 | ( ~ (v9 = 0) & aElement0(v8) = v9)) & ! [v6: $i] : ! [v7: int] : % 163.10/22.56 | ! [v8: $i] : (v7 = 0 | ~ (aElementOf0(v6, v0) = v7) | ~ % 163.10/22.56 | (aElement0(v8) = 0) | ~ $i(v8) | ~ $i(v6) | ? [v9: $i] : ( ~ % 163.10/22.56 | (v9 = v6) & sdtasdt0(xa, v8) = v9 & $i(v9))) & ! [v6: $i] : ( ~ % 163.10/22.56 | (aElementOf0(v6, v1) = 0) | ~ $i(v6) | ? [v7: $i] : % 163.10/22.56 | (sdtasdt0(xb, v7) = v6 & aElement0(v7) = 0 & $i(v7))) & ! [v6: % 163.10/22.56 | $i] : ( ~ (aElementOf0(v6, v0) = 0) | ~ $i(v6) | ? [v7: $i] : % 163.10/22.56 | (sdtasdt0(xa, v7) = v6 & aElement0(v7) = 0 & $i(v7)))) % 163.10/22.56 | % 163.10/22.56 | ALPHA: (m__2273) implies: % 163.10/22.57 | (24) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 163.10/22.57 | ( ~ (xu = sz00) & slsdtgt0(xb) = v1 & slsdtgt0(xa) = v0 & sbrdtbr0(xu) % 163.10/22.57 | = v2 & aElementOf0(v4, v1) = 0 & aElementOf0(v3, v0) = 0 & % 163.10/22.57 | aElementOf0(xu, xI) = 0 & sdtpldt0(v3, v4) = xu & $i(v4) & $i(v3) & % 163.10/22.57 | $i(v2) & $i(v1) & $i(v0) & ! [v5: $i] : ! [v6: MultipleValueBool] % 163.10/22.57 | : ! [v7: $i] : ! [v8: $i] : (v5 = sz00 | ~ (aElementOf0(v5, xI) = % 163.10/22.57 | v6) | ~ (sdtpldt0(v7, v8) = v5) | ~ $i(v8) | ~ $i(v7) | ~ % 163.10/22.57 | $i(v5) | ? [v9: any] : ? [v10: int] : (( ~ (v10 = 0) & % 163.10/22.57 | iLess0(v9, v2) = v10 & sbrdtbr0(v5) = v9 & $i(v9)) | % 163.10/22.57 | (aElementOf0(v8, v1) = v10 & aElementOf0(v7, v0) = v9 & ( ~ (v10 % 163.10/22.57 | = 0) | ~ (v9 = 0))))) & ! [v5: $i] : ! [v6: $i] : (v5 = % 163.10/22.57 | sz00 | ~ (sbrdtbr0(v5) = v6) | ~ $i(v5) | ? [v7: any] : ? [v8: % 163.10/22.57 | any] : (iLess0(v6, v2) = v8 & aElementOf0(v5, xI) = v7 & ( ~ (v8 % 163.10/22.57 | = 0) | ( ~ (v7 = 0) & ! [v9: $i] : ! [v10: $i] : ( ~ % 163.10/22.57 | (sdtpldt0(v9, v10) = v5) | ~ $i(v10) | ~ $i(v9) | ? % 163.10/22.57 | [v11: any] : ? [v12: any] : (aElementOf0(v10, v1) = v12 & % 163.10/22.57 | aElementOf0(v9, v0) = v11 & ( ~ (v12 = 0) | ~ (v11 = % 163.10/22.57 | 0)))))))) & ! [v5: $i] : (v5 = sz00 | ~ % 163.10/22.57 | (aElementOf0(v5, xI) = 0) | ~ $i(v5) | ? [v6: $i] : ? [v7: int] % 163.10/22.57 | : ( ~ (v7 = 0) & iLess0(v6, v2) = v7 & sbrdtbr0(v5) = v6 & % 163.10/22.57 | $i(v6)))) % 163.10/22.57 | % 163.10/22.57 | ALPHA: (m__2383) implies: % 163.10/22.57 | (25) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 163.10/22.57 | (aDivisorOf0(xu, xb) = v3 & aDivisorOf0(xu, xa) = v1 & doDivides0(xu, % 163.10/22.57 | xb) = v2 & doDivides0(xu, xa) = v0 & (( ~ (v3 = 0) & ~ (v2 = 0) & % 163.10/22.57 | ! [v4: $i] : ( ~ (sdtasdt0(xu, v4) = xb) | ~ $i(v4) | ? [v5: % 163.10/22.57 | int] : ( ~ (v5 = 0) & aElement0(v4) = v5)) & ! [v4: $i] : ( % 163.10/22.57 | ~ (aElement0(v4) = 0) | ~ $i(v4) | ? [v5: $i] : ( ~ (v5 = % 163.10/22.57 | xb) & sdtasdt0(xu, v4) = v5 & $i(v5)))) | ( ~ (v1 = 0) & % 163.10/22.57 | ~ (v0 = 0) & ! [v4: $i] : ( ~ (sdtasdt0(xu, v4) = xa) | ~ % 163.10/22.57 | $i(v4) | ? [v5: int] : ( ~ (v5 = 0) & aElement0(v4) = v5)) & % 163.10/22.57 | ! [v4: $i] : ( ~ (aElement0(v4) = 0) | ~ $i(v4) | ? [v5: $i] : % 163.10/22.57 | ( ~ (v5 = xa) & sdtasdt0(xu, v4) = v5 & $i(v5)))))) % 163.10/22.57 | % 163.10/22.57 | ALPHA: (m__2416) implies: % 163.21/22.57 | (26) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (sdtasdt0(xb, % 163.21/22.57 | v1) = v3 & sdtasdt0(xa, v0) = v2 & sdtpldt0(v2, v3) = xu & % 163.21/22.57 | aElement0(v1) = 0 & aElement0(v0) = 0 & $i(v3) & $i(v2) & $i(v1) & % 163.21/22.57 | $i(v0)) % 163.21/22.57 | % 163.21/22.57 | ALPHA: (m__2479) implies: % 163.21/22.57 | (27) $i(xa) % 163.21/22.57 | (28) ? [v0: $i] : (doDivides0(xu, xa) = 0 & sdtasdt0(xu, v0) = xa & % 163.21/22.57 | aElement0(v0) = 0 & $i(v0)) % 163.21/22.57 | % 163.21/22.57 | ALPHA: (m__2612) implies: % 163.21/22.57 | (29) ? [v0: int] : ( ~ (v0 = 0) & doDivides0(xu, xb) = v0 & ! [v1: $i] : % 163.21/22.57 | ( ~ (sdtasdt0(xu, v1) = xb) | ~ $i(v1) | ? [v2: int] : ( ~ (v2 = % 163.21/22.57 | 0) & aElement0(v1) = v2)) & ! [v1: $i] : ( ~ (aElement0(v1) = % 163.21/22.57 | 0) | ~ $i(v1) | ? [v2: $i] : ( ~ (v2 = xb) & sdtasdt0(xu, v1) % 163.21/22.57 | = v2 & $i(v2)))) % 163.21/22.57 | % 163.21/22.57 | ALPHA: (m__2666) implies: % 163.21/22.57 | (30) $i(xb) % 163.21/22.57 | (31) $i(xu) % 163.21/22.57 | (32) $i(xq) % 163.21/22.57 | (33) $i(xr) % 163.21/22.57 | (34) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: any] : (iLess0(v1, % 163.21/22.57 | v2) = v3 & sbrdtbr0(xr) = v1 & sbrdtbr0(xu) = v2 & sdtasdt0(xq, % 163.21/22.57 | xu) = v0 & sdtpldt0(v0, xr) = xb & aElement0(xr) = 0 & % 163.21/22.57 | aElement0(xq) = 0 & $i(v2) & $i(v1) & $i(v0) & (v3 = 0 | xr = sz00)) % 163.21/22.57 | % 163.21/22.57 | ALPHA: (m__) implies: % 163.21/22.57 | (35) xr = sz00 % 163.21/22.57 | % 163.21/22.57 | ALPHA: (function-axioms) implies: % 163.21/22.57 | (36) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 163.21/22.57 | : (v1 = v0 | ~ (aElement0(v2) = v1) | ~ (aElement0(v2) = v0)) % 163.21/22.57 | (37) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (sbrdtbr0(v2) % 163.21/22.57 | = v1) | ~ (sbrdtbr0(v2) = v0)) % 163.21/22.57 | (38) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (slsdtgt0(v2) % 163.21/22.57 | = v1) | ~ (slsdtgt0(v2) = v0)) % 163.21/22.57 | (39) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 163.21/22.57 | (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 163.21/22.57 | (40) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 163.21/22.57 | (sdtpldt1(v3, v2) = v1) | ~ (sdtpldt1(v3, v2) = v0)) % 163.21/22.57 | (41) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 163.21/22.57 | : ! [v3: $i] : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ % 163.21/22.57 | (doDivides0(v3, v2) = v0)) % 163.21/22.57 | % 163.21/22.57 | DELTA: instantiating (28) with fresh symbol all_34_0 gives: % 163.21/22.57 | (42) doDivides0(xu, xa) = 0 & sdtasdt0(xu, all_34_0) = xa & % 163.21/22.57 | aElement0(all_34_0) = 0 & $i(all_34_0) % 163.21/22.57 | % 163.21/22.57 | ALPHA: (42) implies: % 163.21/22.57 | (43) $i(all_34_0) % 163.21/22.57 | (44) sdtasdt0(xu, all_34_0) = xa % 163.21/22.57 | (45) doDivides0(xu, xa) = 0 % 163.21/22.57 | % 163.21/22.57 | DELTA: instantiating (26) with fresh symbols all_36_0, all_36_1, all_36_2, % 163.21/22.57 | all_36_3 gives: % 163.21/22.58 | (46) sdtasdt0(xb, all_36_2) = all_36_0 & sdtasdt0(xa, all_36_3) = all_36_1 % 163.21/22.58 | & sdtpldt0(all_36_1, all_36_0) = xu & aElement0(all_36_2) = 0 & % 163.21/22.58 | aElement0(all_36_3) = 0 & $i(all_36_0) & $i(all_36_1) & $i(all_36_2) & % 163.21/22.58 | $i(all_36_3) % 163.21/22.58 | % 163.21/22.58 | ALPHA: (46) implies: % 163.21/22.58 | (47) $i(all_36_3) % 163.21/22.58 | (48) $i(all_36_2) % 163.21/22.58 | (49) $i(all_36_1) % 163.21/22.58 | (50) $i(all_36_0) % 163.21/22.58 | (51) sdtpldt0(all_36_1, all_36_0) = xu % 163.21/22.58 | (52) sdtasdt0(xa, all_36_3) = all_36_1 % 163.21/22.58 | (53) sdtasdt0(xb, all_36_2) = all_36_0 % 163.21/22.58 | % 163.21/22.58 | DELTA: instantiating (29) with fresh symbol all_38_0 gives: % 163.21/22.58 | (54) ~ (all_38_0 = 0) & doDivides0(xu, xb) = all_38_0 & ! [v0: $i] : ( ~ % 163.21/22.58 | (sdtasdt0(xu, v0) = xb) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 163.21/22.58 | aElement0(v0) = v1)) & ! [v0: $i] : ( ~ (aElement0(v0) = 0) | ~ % 163.21/22.58 | $i(v0) | ? [v1: $i] : ( ~ (v1 = xb) & sdtasdt0(xu, v0) = v1 & % 163.21/22.58 | $i(v1))) % 163.21/22.58 | % 163.21/22.58 | ALPHA: (54) implies: % 163.21/22.58 | (55) doDivides0(xu, xb) = all_38_0 % 163.21/22.58 | % 163.21/22.58 | DELTA: instantiating (34) with fresh symbols all_41_0, all_41_1, all_41_2, % 163.21/22.58 | all_41_3 gives: % 163.21/22.58 | (56) iLess0(all_41_2, all_41_1) = all_41_0 & sbrdtbr0(xr) = all_41_2 & % 163.21/22.58 | sbrdtbr0(xu) = all_41_1 & sdtasdt0(xq, xu) = all_41_3 & % 163.21/22.58 | sdtpldt0(all_41_3, xr) = xb & aElement0(xr) = 0 & aElement0(xq) = 0 & % 163.21/22.58 | $i(all_41_1) & $i(all_41_2) & $i(all_41_3) & (all_41_0 = 0 | xr = % 163.21/22.58 | sz00) % 163.21/22.58 | % 163.21/22.58 | ALPHA: (56) implies: % 163.21/22.58 | (57) $i(all_41_3) % 163.21/22.58 | (58) aElement0(xq) = 0 % 163.21/22.58 | (59) sdtpldt0(all_41_3, xr) = xb % 163.21/22.58 | (60) sdtasdt0(xq, xu) = all_41_3 % 163.21/22.58 | (61) sbrdtbr0(xu) = all_41_1 % 163.21/22.58 | % 163.21/22.58 | DELTA: instantiating (22) with fresh symbols all_43_0, all_43_1, all_43_2, % 163.21/22.58 | all_43_3, all_43_4, all_43_5 gives: % 163.21/22.58 | (62) slsdtgt0(xb) = all_43_4 & slsdtgt0(xa) = all_43_5 & aElementOf0(xb, % 163.21/22.58 | all_43_4) = 0 & aElementOf0(xa, all_43_5) = 0 & aElementOf0(sz00, % 163.21/22.58 | all_43_4) = 0 & aElementOf0(sz00, all_43_5) = 0 & sdtasdt0(xb, % 163.21/22.58 | all_43_2) = sz00 & sdtasdt0(xb, all_43_3) = xb & sdtasdt0(xa, % 163.21/22.58 | all_43_0) = sz00 & sdtasdt0(xa, all_43_1) = xa & aElement0(all_43_0) % 163.21/22.58 | = 0 & aElement0(all_43_1) = 0 & aElement0(all_43_2) = 0 & % 163.21/22.58 | aElement0(all_43_3) = 0 & $i(all_43_0) & $i(all_43_1) & $i(all_43_2) & % 163.21/22.58 | $i(all_43_3) & $i(all_43_4) & $i(all_43_5) % 163.21/22.58 | % 163.21/22.58 | ALPHA: (62) implies: % 163.21/22.58 | (63) $i(all_43_3) % 163.21/22.58 | (64) $i(all_43_2) % 163.21/22.58 | (65) $i(all_43_1) % 163.21/22.58 | (66) $i(all_43_0) % 163.21/22.58 | (67) sdtasdt0(xa, all_43_1) = xa % 163.21/22.58 | (68) sdtasdt0(xa, all_43_0) = sz00 % 163.21/22.58 | (69) sdtasdt0(xb, all_43_3) = xb % 163.21/22.58 | (70) sdtasdt0(xb, all_43_2) = sz00 % 163.21/22.58 | (71) slsdtgt0(xa) = all_43_5 % 163.21/22.58 | (72) slsdtgt0(xb) = all_43_4 % 163.21/22.58 | % 163.21/22.58 | DELTA: instantiating (25) with fresh symbols all_45_0, all_45_1, all_45_2, % 163.21/22.58 | all_45_3 gives: % 163.21/22.58 | (73) aDivisorOf0(xu, xb) = all_45_0 & aDivisorOf0(xu, xa) = all_45_2 & % 163.21/22.58 | doDivides0(xu, xb) = all_45_1 & doDivides0(xu, xa) = all_45_3 & (( ~ % 163.21/22.58 | (all_45_0 = 0) & ~ (all_45_1 = 0) & ! [v0: $i] : ( ~ % 163.21/22.58 | (sdtasdt0(xu, v0) = xb) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = % 163.21/22.58 | 0) & aElement0(v0) = v1)) & ! [v0: $i] : ( ~ (aElement0(v0) % 163.21/22.58 | = 0) | ~ $i(v0) | ? [v1: $i] : ( ~ (v1 = xb) & sdtasdt0(xu, % 163.21/22.58 | v0) = v1 & $i(v1)))) | ( ~ (all_45_2 = 0) & ~ (all_45_3 = % 163.21/22.58 | 0) & ! [v0: $i] : ( ~ (sdtasdt0(xu, v0) = xa) | ~ $i(v0) | ? % 163.21/22.58 | [v1: int] : ( ~ (v1 = 0) & aElement0(v0) = v1)) & ! [v0: $i] : % 163.21/22.58 | ( ~ (aElement0(v0) = 0) | ~ $i(v0) | ? [v1: $i] : ( ~ (v1 = xa) % 163.21/22.58 | & sdtasdt0(xu, v0) = v1 & $i(v1))))) % 163.21/22.58 | % 163.21/22.58 | ALPHA: (73) implies: % 163.21/22.58 | (74) doDivides0(xu, xa) = all_45_3 % 163.21/22.58 | (75) doDivides0(xu, xb) = all_45_1 % 163.21/22.58 | (76) aDivisorOf0(xu, xb) = all_45_0 % 163.21/22.58 | (77) ( ~ (all_45_0 = 0) & ~ (all_45_1 = 0) & ! [v0: $i] : ( ~ % 163.21/22.58 | (sdtasdt0(xu, v0) = xb) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) % 163.21/22.58 | & aElement0(v0) = v1)) & ! [v0: $i] : ( ~ (aElement0(v0) = 0) | % 163.21/22.58 | ~ $i(v0) | ? [v1: $i] : ( ~ (v1 = xb) & sdtasdt0(xu, v0) = v1 & % 163.21/22.58 | $i(v1)))) | ( ~ (all_45_2 = 0) & ~ (all_45_3 = 0) & ! [v0: $i] % 163.21/22.58 | : ( ~ (sdtasdt0(xu, v0) = xa) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = % 163.21/22.58 | 0) & aElement0(v0) = v1)) & ! [v0: $i] : ( ~ (aElement0(v0) = % 163.21/22.58 | 0) | ~ $i(v0) | ? [v1: $i] : ( ~ (v1 = xa) & sdtasdt0(xu, v0) % 163.21/22.58 | = v1 & $i(v1)))) % 163.21/22.58 | % 163.21/22.58 | DELTA: instantiating (24) with fresh symbols all_50_0, all_50_1, all_50_2, % 163.21/22.58 | all_50_3, all_50_4 gives: % 163.21/22.59 | (78) ~ (xu = sz00) & slsdtgt0(xb) = all_50_3 & slsdtgt0(xa) = all_50_4 & % 163.21/22.59 | sbrdtbr0(xu) = all_50_2 & aElementOf0(all_50_0, all_50_3) = 0 & % 163.21/22.59 | aElementOf0(all_50_1, all_50_4) = 0 & aElementOf0(xu, xI) = 0 & % 163.21/22.59 | sdtpldt0(all_50_1, all_50_0) = xu & $i(all_50_0) & $i(all_50_1) & % 163.21/22.59 | $i(all_50_2) & $i(all_50_3) & $i(all_50_4) & ! [v0: $i] : ! [v1: % 163.21/22.59 | MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v0 = sz00 | ~ % 163.21/22.59 | (aElementOf0(v0, xI) = v1) | ~ (sdtpldt0(v2, v3) = v0) | ~ $i(v3) % 163.21/22.59 | | ~ $i(v2) | ~ $i(v0) | ? [v4: any] : ? [v5: int] : (( ~ (v5 = % 163.21/22.59 | 0) & iLess0(v4, all_50_2) = v5 & sbrdtbr0(v0) = v4 & $i(v4)) | % 163.21/22.59 | (aElementOf0(v3, all_50_3) = v5 & aElementOf0(v2, all_50_4) = v4 & % 163.21/22.59 | ( ~ (v5 = 0) | ~ (v4 = 0))))) & ! [v0: $i] : ! [v1: $i] : (v0 % 163.21/22.59 | = sz00 | ~ (sbrdtbr0(v0) = v1) | ~ $i(v0) | ? [v2: any] : ? [v3: % 163.21/22.59 | any] : (iLess0(v1, all_50_2) = v3 & aElementOf0(v0, xI) = v2 & ( ~ % 163.21/22.59 | (v3 = 0) | ( ~ (v2 = 0) & ! [v4: $i] : ! [v5: $i] : ( ~ % 163.21/22.59 | (sdtpldt0(v4, v5) = v0) | ~ $i(v5) | ~ $i(v4) | ? [v6: % 163.21/22.59 | any] : ? [v7: any] : (aElementOf0(v5, all_50_3) = v7 & % 163.21/22.59 | aElementOf0(v4, all_50_4) = v6 & ( ~ (v7 = 0) | ~ (v6 = % 163.21/22.59 | 0)))))))) & ! [v0: $i] : (v0 = sz00 | ~ % 163.21/22.59 | (aElementOf0(v0, xI) = 0) | ~ $i(v0) | ? [v1: $i] : ? [v2: int] : % 163.21/22.59 | ( ~ (v2 = 0) & iLess0(v1, all_50_2) = v2 & sbrdtbr0(v0) = v1 & % 163.21/22.59 | $i(v1))) % 163.21/22.59 | % 163.21/22.59 | ALPHA: (78) implies: % 163.21/22.59 | (79) ~ (xu = sz00) % 163.21/22.59 | (80) $i(all_50_1) % 163.21/22.59 | (81) $i(all_50_0) % 163.21/22.59 | (82) sdtpldt0(all_50_1, all_50_0) = xu % 163.21/22.59 | (83) aElementOf0(xu, xI) = 0 % 163.21/22.59 | (84) sbrdtbr0(xu) = all_50_2 % 163.21/22.59 | (85) slsdtgt0(xa) = all_50_4 % 163.21/22.59 | (86) slsdtgt0(xb) = all_50_3 % 163.21/22.59 | % 163.21/22.59 | DELTA: instantiating (23) with fresh symbols all_53_0, all_53_1, all_53_2, % 163.21/22.59 | all_53_3, all_53_4, all_53_5 gives: % 163.21/22.59 | (87) ~ (all_53_2 = sz00) & slsdtgt0(xb) = all_53_4 & slsdtgt0(xa) = % 163.21/22.59 | all_53_5 & sdtpldt1(all_53_5, all_53_4) = all_53_3 & % 163.21/22.59 | aElementOf0(all_53_0, all_53_4) = 0 & aElementOf0(all_53_1, all_53_5) % 163.21/22.59 | = 0 & aElementOf0(all_53_2, all_53_3) = 0 & sdtpldt0(all_53_1, % 163.21/22.59 | all_53_0) = all_53_2 & $i(all_53_0) & $i(all_53_1) & $i(all_53_2) & % 163.21/22.59 | $i(all_53_3) & $i(all_53_4) & $i(all_53_5) & ! [v0: $i] : ! [v1: % 163.21/22.59 | int] : ! [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_53_4) = v1) | % 163.21/22.59 | ~ (sdtasdt0(xb, v2) = v0) | ~ $i(v2) | ~ $i(v0) | ? [v3: int] : % 163.21/22.59 | ( ~ (v3 = 0) & aElement0(v2) = v3)) & ! [v0: $i] : ! [v1: int] : % 163.21/22.59 | ! [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_53_4) = v1) | ~ % 163.21/22.59 | (aElement0(v2) = 0) | ~ $i(v2) | ~ $i(v0) | ? [v3: $i] : ( ~ (v3 % 163.21/22.59 | = v0) & sdtasdt0(xb, v2) = v3 & $i(v3))) & ! [v0: $i] : ! [v1: % 163.21/22.59 | int] : ! [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_53_5) = v1) | % 163.21/22.59 | ~ (sdtasdt0(xa, v2) = v0) | ~ $i(v2) | ~ $i(v0) | ? [v3: int] : % 163.21/22.59 | ( ~ (v3 = 0) & aElement0(v2) = v3)) & ! [v0: $i] : ! [v1: int] : % 163.21/22.59 | ! [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_53_5) = v1) | ~ % 163.21/22.59 | (aElement0(v2) = 0) | ~ $i(v2) | ~ $i(v0) | ? [v3: $i] : ( ~ (v3 % 163.21/22.59 | = v0) & sdtasdt0(xa, v2) = v3 & $i(v3))) & ! [v0: $i] : ( ~ % 163.21/22.59 | (aElementOf0(v0, all_53_4) = 0) | ~ $i(v0) | ? [v1: $i] : % 163.21/22.59 | (sdtasdt0(xb, v1) = v0 & aElement0(v1) = 0 & $i(v1))) & ! [v0: $i] % 163.21/22.59 | : ( ~ (aElementOf0(v0, all_53_5) = 0) | ~ $i(v0) | ? [v1: $i] : % 163.21/22.59 | (sdtasdt0(xa, v1) = v0 & aElement0(v1) = 0 & $i(v1))) % 163.21/22.59 | % 163.21/22.59 | ALPHA: (87) implies: % 163.21/22.59 | (88) $i(all_53_3) % 163.21/22.59 | (89) sdtpldt1(all_53_5, all_53_4) = all_53_3 % 163.21/22.59 | (90) slsdtgt0(xa) = all_53_5 % 163.21/22.59 | (91) slsdtgt0(xb) = all_53_4 % 163.21/22.59 | % 163.21/22.59 | DELTA: instantiating (21) with fresh symbols all_56_0, all_56_1 gives: % 163.21/22.60 | (92) slsdtgt0(xb) = all_56_0 & slsdtgt0(xa) = all_56_1 & aIdeal0(xI) = 0 & % 163.21/22.60 | sdtpldt1(all_56_1, all_56_0) = xI & aSet0(xI) = 0 & $i(all_56_0) & % 163.21/22.60 | $i(all_56_1) & ! [v0: $i] : ! [v1: int] : ! [v2: $i] : ! [v3: $i] % 163.21/22.60 | : (v1 = 0 | ~ (aElementOf0(v0, xI) = v1) | ~ (sdtpldt0(v2, v3) = v0) % 163.21/22.60 | | ~ $i(v3) | ~ $i(v2) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : % 163.21/22.60 | (aElementOf0(v3, all_56_0) = v5 & aElementOf0(v2, all_56_1) = v4 & ( % 163.21/22.60 | ~ (v5 = 0) | ~ (v4 = 0)))) & ! [v0: $i] : ! [v1: int] : ! % 163.21/22.60 | [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_56_0) = v1) | ~ % 163.21/22.60 | (sdtasdt0(xb, v2) = v0) | ~ $i(v2) | ~ $i(v0) | ? [v3: int] : ( ~ % 163.21/22.60 | (v3 = 0) & aElement0(v2) = v3)) & ! [v0: $i] : ! [v1: int] : ! % 163.21/22.60 | [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_56_0) = v1) | ~ % 163.21/22.60 | (aElement0(v2) = 0) | ~ $i(v2) | ~ $i(v0) | ? [v3: $i] : ( ~ (v3 % 163.21/22.60 | = v0) & sdtasdt0(xb, v2) = v3 & $i(v3))) & ! [v0: $i] : ! [v1: % 163.21/22.60 | int] : ! [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_56_1) = v1) | % 163.21/22.60 | ~ (sdtasdt0(xa, v2) = v0) | ~ $i(v2) | ~ $i(v0) | ? [v3: int] : % 163.21/22.60 | ( ~ (v3 = 0) & aElement0(v2) = v3)) & ! [v0: $i] : ! [v1: int] : % 163.21/22.60 | ! [v2: $i] : (v1 = 0 | ~ (aElementOf0(v0, all_56_1) = v1) | ~ % 163.21/22.60 | (aElement0(v2) = 0) | ~ $i(v2) | ~ $i(v0) | ? [v3: $i] : ( ~ (v3 % 163.21/22.60 | = v0) & sdtasdt0(xa, v2) = v3 & $i(v3))) & ! [v0: $i] : ! [v1: % 163.21/22.60 | $i] : ! [v2: $i] : ( ~ (aElementOf0(v0, xI) = 0) | ~ (sdtasdt0(v1, % 163.21/22.60 | v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] % 163.21/22.60 | : (aElementOf0(v2, xI) = v4 & aElement0(v1) = v3 & ( ~ (v3 = 0) | v4 % 163.21/22.60 | = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 163.21/22.60 | (aElementOf0(v0, xI) = 0) | ~ (sdtpldt0(v0, v1) = v2) | ~ $i(v1) | % 163.21/22.60 | ~ $i(v0) | ? [v3: any] : ? [v4: any] : (aElementOf0(v2, xI) = v4 % 163.21/22.60 | & aElementOf0(v1, xI) = v3 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0: % 163.21/22.60 | $i] : ! [v1: $i] : ( ~ (aElementOf0(v1, xI) = 0) | ~ % 163.21/22.60 | (aElementOf0(v0, xI) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: $i] : % 163.21/22.60 | (aElementOf0(v2, xI) = 0 & sdtpldt0(v0, v1) = v2 & $i(v2))) & ! % 163.21/22.60 | [v0: $i] : ! [v1: $i] : ( ~ (aElementOf0(v0, xI) = 0) | ~ % 163.21/22.60 | (aElement0(v1) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: $i] : % 163.21/22.60 | (aElementOf0(v2, xI) = 0 & sdtasdt0(v1, v0) = v2 & $i(v2))) & ! % 163.21/22.60 | [v0: $i] : ( ~ (aElementOf0(v0, all_56_0) = 0) | ~ $i(v0) | ? [v1: % 163.21/22.60 | $i] : (sdtasdt0(xb, v1) = v0 & aElement0(v1) = 0 & $i(v1))) & ! % 163.21/22.60 | [v0: $i] : ( ~ (aElementOf0(v0, all_56_1) = 0) | ~ $i(v0) | ? [v1: % 163.21/22.60 | $i] : (sdtasdt0(xa, v1) = v0 & aElement0(v1) = 0 & $i(v1))) & ! % 163.21/22.60 | [v0: $i] : ( ~ (aElementOf0(v0, xI) = 0) | ~ $i(v0) | ? [v1: $i] : % 163.21/22.60 | ? [v2: $i] : (aElementOf0(v2, all_56_0) = 0 & aElementOf0(v1, % 163.21/22.60 | all_56_1) = 0 & sdtpldt0(v1, v2) = v0 & $i(v2) & $i(v1))) % 163.21/22.60 | % 163.21/22.60 | ALPHA: (92) implies: % 163.21/22.60 | (93) aSet0(xI) = 0 % 163.21/22.60 | (94) sdtpldt1(all_56_1, all_56_0) = xI % 163.21/22.60 | (95) aIdeal0(xI) = 0 % 163.21/22.60 | (96) slsdtgt0(xa) = all_56_1 % 163.21/22.60 | (97) slsdtgt0(xb) = all_56_0 % 163.21/22.60 | % 163.21/22.60 | DELTA: instantiating (20) with fresh symbols all_59_0, all_59_1 gives: % 163.21/22.61 | (98) aGcdOfAnd0(xc, xa, xb) = 0 & aDivisorOf0(xc, xb) = 0 & aDivisorOf0(xc, % 163.21/22.61 | xa) = 0 & doDivides0(xc, xb) = 0 & doDivides0(xc, xa) = 0 & % 163.21/22.61 | sdtasdt0(xc, all_59_0) = xa & sdtasdt0(xc, all_59_1) = xb & % 163.21/22.61 | aElement0(all_59_0) = 0 & aElement0(all_59_1) = 0 & aElement0(xc) = 0 % 163.21/22.61 | & $i(all_59_0) & $i(all_59_1) & ! [v0: $i] : ! [v1: int] : (v1 = 0 | % 163.21/22.61 | ~ (doDivides0(v0, xc) = v1) | ~ $i(v0) | ? [v2: any] : ? [v3: % 163.21/22.61 | any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : % 163.21/22.61 | (aDivisorOf0(v0, xb) = v6 & aDivisorOf0(v0, xa) = v4 & % 163.21/22.61 | doDivides0(v0, xb) = v5 & doDivides0(v0, xa) = v3 & aElement0(v0) % 163.21/22.61 | = v2 & (( ~ (v6 = 0) & ~ (v5 = 0) & ! [v7: $i] : ( ~ % 163.21/22.61 | (sdtasdt0(v0, v7) = xb) | ~ $i(v7) | ? [v8: int] : ( ~ (v8 % 163.21/22.61 | = 0) & aElement0(v7) = v8)) & ! [v7: $i] : ( ~ % 163.21/22.61 | (aElement0(v7) = 0) | ~ $i(v7) | ? [v8: $i] : ( ~ (v8 = % 163.21/22.61 | xb) & sdtasdt0(v0, v7) = v8 & $i(v8)))) | ( ~ (v4 = 0) & % 163.21/22.61 | ( ~ (v2 = 0) | ( ~ (v3 = 0) & ! [v7: $i] : ( ~ (sdtasdt0(v0, % 163.21/22.61 | v7) = xa) | ~ $i(v7) | ? [v8: int] : ( ~ (v8 = 0) % 163.21/22.61 | & aElement0(v7) = v8)) & ! [v7: $i] : ( ~ % 163.21/22.61 | (aElement0(v7) = 0) | ~ $i(v7) | ? [v8: $i] : ( ~ (v8 % 163.21/22.61 | = xa) & sdtasdt0(v0, v7) = v8 & $i(v8))))))))) & ! % 163.21/22.61 | [v0: $i] : ! [v1: any] : ( ~ (aDivisorOf0(v0, xb) = v1) | ~ $i(v0) | % 163.21/22.61 | ? [v2: any] : ? [v3: any] : ? [v4: any] : ? [v5: any] : ? [v6: % 163.21/22.61 | any] : ? [v7: $i] : ? [v8: int] : ? [v9: $i] : (aDivisorOf0(v0, % 163.21/22.61 | xa) = v4 & doDivides0(v0, xc) = v6 & doDivides0(v0, xb) = v5 & % 163.21/22.61 | doDivides0(v0, xa) = v3 & aElement0(v0) = v2 & $i(v7) & ((v9 = xc % 163.21/22.61 | & v8 = 0 & v6 = 0 & sdtasdt0(v0, v7) = xc & aElement0(v7) = 0) % 163.21/22.61 | | ( ~ (v5 = 0) & ~ (v1 = 0) & ! [v10: $i] : ( ~ (sdtasdt0(v0, % 163.21/22.61 | v10) = xb) | ~ $i(v10) | ? [v11: int] : ( ~ (v11 = 0) % 163.21/22.61 | & aElement0(v10) = v11)) & ! [v10: $i] : ( ~ % 163.21/22.61 | (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: $i] : ( ~ (v11 % 163.21/22.61 | = xb) & sdtasdt0(v0, v10) = v11 & $i(v11)))) | ( ~ (v4 = % 163.21/22.61 | 0) & ( ~ (v2 = 0) | ( ~ (v3 = 0) & ! [v10: $i] : ( ~ % 163.21/22.61 | (sdtasdt0(v0, v10) = xa) | ~ $i(v10) | ? [v11: int] : % 163.21/22.61 | ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! [v10: $i] : % 163.21/22.61 | ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: $i] : ( ~ % 163.21/22.61 | (v11 = xa) & sdtasdt0(v0, v10) = v11 & $i(v11))))))))) % 163.21/22.61 | & ! [v0: $i] : ! [v1: any] : ( ~ (aDivisorOf0(v0, xa) = v1) | ~ % 163.21/22.61 | $i(v0) | ? [v2: any] : ? [v3: any] : ? [v4: any] : ? [v5: any] : % 163.21/22.61 | ? [v6: any] : ? [v7: $i] : ? [v8: int] : ? [v9: $i] : % 163.21/22.61 | (aDivisorOf0(v0, xb) = v5 & doDivides0(v0, xc) = v6 & doDivides0(v0, % 163.21/22.61 | xb) = v4 & doDivides0(v0, xa) = v3 & aElement0(v0) = v2 & $i(v7) % 163.21/22.61 | & ((v9 = xc & v8 = 0 & v6 = 0 & sdtasdt0(v0, v7) = xc & % 163.21/22.61 | aElement0(v7) = 0) | ( ~ (v5 = 0) & ~ (v4 = 0) & ! [v10: $i] % 163.21/22.61 | : ( ~ (sdtasdt0(v0, v10) = xb) | ~ $i(v10) | ? [v11: int] : % 163.21/22.61 | ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! [v10: $i] : ( ~ % 163.21/22.61 | (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: $i] : ( ~ (v11 % 163.21/22.61 | = xb) & sdtasdt0(v0, v10) = v11 & $i(v11)))) | ( ~ (v1 = % 163.21/22.61 | 0) & ( ~ (v2 = 0) | ( ~ (v3 = 0) & ! [v10: $i] : ( ~ % 163.21/22.61 | (sdtasdt0(v0, v10) = xa) | ~ $i(v10) | ? [v11: int] : % 163.21/22.61 | ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! [v10: $i] : % 163.21/22.61 | ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: $i] : ( ~ % 163.21/22.61 | (v11 = xa) & sdtasdt0(v0, v10) = v11 & $i(v11))))))))) % 163.21/22.61 | & ! [v0: $i] : ! [v1: MultipleValueBool] : ( ~ (doDivides0(v0, xc) = % 163.21/22.61 | v1) | ~ $i(v0) | ? [v2: any] : ? [v3: any] : ? [v4: any] : ? % 163.21/22.61 | [v5: any] : ? [v6: any] : ? [v7: $i] : ? [v8: int] : ? [v9: $i] % 163.21/22.61 | : ($i(v7) & ((v9 = xc & v8 = 0 & sdtasdt0(v0, v7) = xc & % 163.21/22.61 | aElement0(v7) = 0) | (aDivisorOf0(v0, xb) = v6 & % 163.21/22.61 | aDivisorOf0(v0, xa) = v4 & doDivides0(v0, xb) = v5 & % 163.21/22.61 | doDivides0(v0, xa) = v3 & aElement0(v0) = v2 & (( ~ (v6 = 0) & % 163.21/22.61 | ~ (v5 = 0) & ! [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xb) % 163.21/22.61 | | ~ $i(v10) | ? [v11: int] : ( ~ (v11 = 0) & % 163.21/22.61 | aElement0(v10) = v11)) & ! [v10: $i] : ( ~ % 163.21/22.61 | (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: $i] : ( ~ % 163.21/22.61 | (v11 = xb) & sdtasdt0(v0, v10) = v11 & $i(v11)))) | ( % 163.21/22.61 | ~ (v4 = 0) & ( ~ (v2 = 0) | ( ~ (v3 = 0) & ! [v10: $i] : % 163.21/22.61 | ( ~ (sdtasdt0(v0, v10) = xa) | ~ $i(v10) | ? [v11: % 163.21/22.61 | int] : ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! % 163.21/22.61 | [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? % 163.21/22.61 | [v11: $i] : ( ~ (v11 = xa) & sdtasdt0(v0, v10) = v11 % 163.21/22.61 | & $i(v11))))))))))) & ! [v0: $i] : ! [v1: any] : % 163.21/22.61 | ( ~ (doDivides0(v0, xb) = v1) | ~ $i(v0) | ? [v2: any] : ? [v3: % 163.21/22.61 | any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: $i] : % 163.21/22.61 | ? [v8: int] : ? [v9: $i] : (aDivisorOf0(v0, xb) = v5 & % 163.21/22.61 | aDivisorOf0(v0, xa) = v4 & doDivides0(v0, xc) = v6 & % 163.21/22.61 | doDivides0(v0, xa) = v3 & aElement0(v0) = v2 & $i(v7) & ((v9 = xc % 163.21/22.61 | & v8 = 0 & v6 = 0 & sdtasdt0(v0, v7) = xc & aElement0(v7) = 0) % 163.21/22.61 | | ( ~ (v5 = 0) & ~ (v1 = 0) & ! [v10: $i] : ( ~ (sdtasdt0(v0, % 163.21/22.61 | v10) = xb) | ~ $i(v10) | ? [v11: int] : ( ~ (v11 = 0) % 163.21/22.61 | & aElement0(v10) = v11)) & ! [v10: $i] : ( ~ % 163.21/22.61 | (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: $i] : ( ~ (v11 % 163.21/22.61 | = xb) & sdtasdt0(v0, v10) = v11 & $i(v11)))) | ( ~ (v4 = % 163.21/22.61 | 0) & ( ~ (v2 = 0) | ( ~ (v3 = 0) & ! [v10: $i] : ( ~ % 163.21/22.61 | (sdtasdt0(v0, v10) = xa) | ~ $i(v10) | ? [v11: int] : % 163.21/22.61 | ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! [v10: $i] : % 163.21/22.61 | ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: $i] : ( ~ % 163.21/22.61 | (v11 = xa) & sdtasdt0(v0, v10) = v11 & $i(v11))))))))) % 163.21/22.61 | & ! [v0: $i] : ! [v1: any] : ( ~ (doDivides0(v0, xa) = v1) | ~ % 163.21/22.61 | $i(v0) | ? [v2: any] : ? [v3: any] : ? [v4: any] : ? [v5: any] : % 163.21/22.61 | ? [v6: any] : ? [v7: $i] : ? [v8: int] : ? [v9: $i] : % 163.21/22.61 | (aDivisorOf0(v0, xb) = v5 & aDivisorOf0(v0, xa) = v3 & % 163.21/22.61 | doDivides0(v0, xc) = v6 & doDivides0(v0, xb) = v4 & aElement0(v0) % 163.21/22.61 | = v2 & $i(v7) & ((v9 = xc & v8 = 0 & v6 = 0 & sdtasdt0(v0, v7) = % 163.21/22.61 | xc & aElement0(v7) = 0) | ( ~ (v5 = 0) & ~ (v4 = 0) & ! % 163.21/22.61 | [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xb) | ~ $i(v10) | ? % 163.21/22.61 | [v11: int] : ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! % 163.21/22.61 | [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: % 163.21/22.61 | $i] : ( ~ (v11 = xb) & sdtasdt0(v0, v10) = v11 & % 163.21/22.61 | $i(v11)))) | ( ~ (v3 = 0) & ( ~ (v2 = 0) | ( ~ (v1 = 0) & % 163.21/22.61 | ! [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xa) | ~ $i(v10) | % 163.21/22.61 | ? [v11: int] : ( ~ (v11 = 0) & aElement0(v10) = v11)) & % 163.21/22.61 | ! [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? % 163.21/22.61 | [v11: $i] : ( ~ (v11 = xa) & sdtasdt0(v0, v10) = v11 & % 163.21/22.61 | $i(v11))))))))) & ! [v0: $i] : ! [v1: any] : ( ~ % 163.21/22.61 | (aElement0(v0) = v1) | ~ $i(v0) | ? [v2: any] : ? [v3: any] : ? % 163.21/22.61 | [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: $i] : ? [v8: int] % 163.21/22.61 | : ? [v9: $i] : (aDivisorOf0(v0, xb) = v5 & aDivisorOf0(v0, xa) = v3 % 163.21/22.61 | & doDivides0(v0, xc) = v6 & doDivides0(v0, xb) = v4 & % 163.21/22.61 | doDivides0(v0, xa) = v2 & $i(v7) & ((v9 = xc & v8 = 0 & v6 = 0 & % 163.21/22.61 | sdtasdt0(v0, v7) = xc & aElement0(v7) = 0) | ( ~ (v5 = 0) & ~ % 163.21/22.61 | (v4 = 0) & ! [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xb) | ~ % 163.21/22.61 | $i(v10) | ? [v11: int] : ( ~ (v11 = 0) & aElement0(v10) = % 163.21/22.61 | v11)) & ! [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ % 163.21/22.61 | $i(v10) | ? [v11: $i] : ( ~ (v11 = xb) & sdtasdt0(v0, v10) % 163.21/22.61 | = v11 & $i(v11)))) | ( ~ (v3 = 0) & ( ~ (v1 = 0) | ( ~ (v2 % 163.21/22.61 | = 0) & ! [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xa) | ~ % 163.21/22.61 | $i(v10) | ? [v11: int] : ( ~ (v11 = 0) & aElement0(v10) % 163.21/22.61 | = v11)) & ! [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ % 163.21/22.61 | $i(v10) | ? [v11: $i] : ( ~ (v11 = xa) & sdtasdt0(v0, % 163.21/22.61 | v10) = v11 & $i(v11))))))))) % 163.21/22.61 | % 163.21/22.61 | ALPHA: (98) implies: % 163.21/22.61 | (99) $i(all_59_0) % 163.21/22.61 | (100) aElement0(all_59_0) = 0 % 163.21/22.61 | (101) ! [v0: $i] : ! [v1: any] : ( ~ (doDivides0(v0, xa) = v1) | ~ % 163.21/22.61 | $i(v0) | ? [v2: any] : ? [v3: any] : ? [v4: any] : ? [v5: any] % 163.21/22.61 | : ? [v6: any] : ? [v7: $i] : ? [v8: int] : ? [v9: $i] : % 163.21/22.61 | (aDivisorOf0(v0, xb) = v5 & aDivisorOf0(v0, xa) = v3 & % 163.21/22.61 | doDivides0(v0, xc) = v6 & doDivides0(v0, xb) = v4 & aElement0(v0) % 163.21/22.61 | = v2 & $i(v7) & ((v9 = xc & v8 = 0 & v6 = 0 & sdtasdt0(v0, v7) = % 163.21/22.61 | xc & aElement0(v7) = 0) | ( ~ (v5 = 0) & ~ (v4 = 0) & ! % 163.21/22.61 | [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xb) | ~ $i(v10) | ? % 163.21/22.61 | [v11: int] : ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! % 163.21/22.61 | [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: % 163.21/22.61 | $i] : ( ~ (v11 = xb) & sdtasdt0(v0, v10) = v11 & % 163.21/22.61 | $i(v11)))) | ( ~ (v3 = 0) & ( ~ (v2 = 0) | ( ~ (v1 = 0) & % 163.21/22.61 | ! [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xa) | ~ $i(v10) % 163.21/22.61 | | ? [v11: int] : ( ~ (v11 = 0) & aElement0(v10) = % 163.21/22.61 | v11)) & ! [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ % 163.21/22.61 | $i(v10) | ? [v11: $i] : ( ~ (v11 = xa) & sdtasdt0(v0, % 163.21/22.61 | v10) = v11 & $i(v11))))))))) % 163.21/22.62 | (102) ! [v0: $i] : ! [v1: any] : ( ~ (doDivides0(v0, xb) = v1) | ~ % 163.21/22.62 | $i(v0) | ? [v2: any] : ? [v3: any] : ? [v4: any] : ? [v5: any] % 163.21/22.62 | : ? [v6: any] : ? [v7: $i] : ? [v8: int] : ? [v9: $i] : % 163.21/22.62 | (aDivisorOf0(v0, xb) = v5 & aDivisorOf0(v0, xa) = v4 & % 163.21/22.62 | doDivides0(v0, xc) = v6 & doDivides0(v0, xa) = v3 & aElement0(v0) % 163.21/22.62 | = v2 & $i(v7) & ((v9 = xc & v8 = 0 & v6 = 0 & sdtasdt0(v0, v7) = % 163.21/22.62 | xc & aElement0(v7) = 0) | ( ~ (v5 = 0) & ~ (v1 = 0) & ! % 163.21/22.62 | [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xb) | ~ $i(v10) | ? % 163.21/22.62 | [v11: int] : ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! % 163.21/22.62 | [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: % 163.21/22.62 | $i] : ( ~ (v11 = xb) & sdtasdt0(v0, v10) = v11 & % 163.21/22.62 | $i(v11)))) | ( ~ (v4 = 0) & ( ~ (v2 = 0) | ( ~ (v3 = 0) & % 163.21/22.62 | ! [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xa) | ~ $i(v10) % 163.21/22.62 | | ? [v11: int] : ( ~ (v11 = 0) & aElement0(v10) = % 163.21/22.62 | v11)) & ! [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ % 163.21/22.62 | $i(v10) | ? [v11: $i] : ( ~ (v11 = xa) & sdtasdt0(v0, % 163.21/22.62 | v10) = v11 & $i(v11))))))))) % 163.21/22.62 | (103) ! [v0: $i] : ! [v1: any] : ( ~ (aDivisorOf0(v0, xb) = v1) | ~ % 163.21/22.62 | $i(v0) | ? [v2: any] : ? [v3: any] : ? [v4: any] : ? [v5: any] % 163.21/22.62 | : ? [v6: any] : ? [v7: $i] : ? [v8: int] : ? [v9: $i] : % 163.21/22.62 | (aDivisorOf0(v0, xa) = v4 & doDivides0(v0, xc) = v6 & % 163.21/22.62 | doDivides0(v0, xb) = v5 & doDivides0(v0, xa) = v3 & aElement0(v0) % 163.21/22.62 | = v2 & $i(v7) & ((v9 = xc & v8 = 0 & v6 = 0 & sdtasdt0(v0, v7) = % 163.21/22.62 | xc & aElement0(v7) = 0) | ( ~ (v5 = 0) & ~ (v1 = 0) & ! % 163.21/22.62 | [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xb) | ~ $i(v10) | ? % 163.21/22.62 | [v11: int] : ( ~ (v11 = 0) & aElement0(v10) = v11)) & ! % 163.21/22.62 | [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ $i(v10) | ? [v11: % 163.21/22.62 | $i] : ( ~ (v11 = xb) & sdtasdt0(v0, v10) = v11 & % 163.21/22.62 | $i(v11)))) | ( ~ (v4 = 0) & ( ~ (v2 = 0) | ( ~ (v3 = 0) & % 163.21/22.62 | ! [v10: $i] : ( ~ (sdtasdt0(v0, v10) = xa) | ~ $i(v10) % 163.21/22.62 | | ? [v11: int] : ( ~ (v11 = 0) & aElement0(v10) = % 163.21/22.62 | v11)) & ! [v10: $i] : ( ~ (aElement0(v10) = 0) | ~ % 163.21/22.62 | $i(v10) | ? [v11: $i] : ( ~ (v11 = xa) & sdtasdt0(v0, % 163.21/22.62 | v10) = v11 & $i(v11))))))))) % 163.21/22.62 | % 163.21/22.62 | REDUCE: (35), (59) imply: % 163.21/22.62 | (104) sdtpldt0(all_41_3, sz00) = xb % 163.21/22.62 | % 163.21/22.62 | REDUCE: (33), (35) imply: % 163.21/22.62 | (105) $i(sz00) % 163.21/22.62 | % 163.21/22.62 | GROUND_INST: instantiating (37) with all_41_1, all_50_2, xu, simplifying with % 163.21/22.62 | (61), (84) gives: % 163.21/22.62 | (106) all_50_2 = all_41_1 % 163.21/22.62 | % 163.21/22.62 | GROUND_INST: instantiating (41) with 0, all_45_3, xa, xu, simplifying with % 163.21/22.62 | (45), (74) gives: % 163.21/22.62 | (107) all_45_3 = 0 % 163.21/22.62 | % 163.21/22.62 | GROUND_INST: instantiating (41) with all_38_0, all_45_1, xb, xu, simplifying % 163.21/22.62 | with (55), (75) gives: % 163.21/22.62 | (108) all_45_1 = all_38_0 % 163.21/22.62 | % 163.21/22.62 | GROUND_INST: instantiating (38) with all_50_4, all_53_5, xa, simplifying with % 163.21/22.62 | (85), (90) gives: % 163.21/22.62 | (109) all_53_5 = all_50_4 % 163.21/22.62 | % 163.21/22.62 | GROUND_INST: instantiating (38) with all_53_5, all_56_1, xa, simplifying with % 163.21/22.62 | (90), (96) gives: % 163.21/22.62 | (110) all_56_1 = all_53_5 % 163.21/22.62 | % 163.21/22.62 | GROUND_INST: instantiating (38) with all_43_5, all_56_1, xa, simplifying with % 163.21/22.62 | (71), (96) gives: % 163.21/22.62 | (111) all_56_1 = all_43_5 % 163.21/22.62 | % 163.21/22.62 | GROUND_INST: instantiating (38) with all_50_3, all_53_4, xb, simplifying with % 163.21/22.62 | (86), (91) gives: % 163.21/22.62 | (112) all_53_4 = all_50_3 % 163.21/22.62 | % 163.21/22.62 | GROUND_INST: instantiating (38) with all_53_4, all_56_0, xb, simplifying with % 163.21/22.62 | (91), (97) gives: % 163.21/22.62 | (113) all_56_0 = all_53_4 % 163.21/22.62 | % 163.21/22.62 | GROUND_INST: instantiating (38) with all_43_4, all_56_0, xb, simplifying with % 163.21/22.62 | (72), (97) gives: % 163.21/22.62 | (114) all_56_0 = all_43_4 % 163.21/22.62 | % 163.21/22.62 | COMBINE_EQS: (113), (114) imply: % 163.21/22.62 | (115) all_53_4 = all_43_4 % 163.21/22.62 | % 163.21/22.62 | SIMP: (115) implies: % 163.21/22.62 | (116) all_53_4 = all_43_4 % 163.21/22.62 | % 163.21/22.62 | COMBINE_EQS: (110), (111) imply: % 163.21/22.62 | (117) all_53_5 = all_43_5 % 163.21/22.62 | % 163.21/22.62 | SIMP: (117) implies: % 163.21/22.62 | (118) all_53_5 = all_43_5 % 163.21/22.62 | % 163.21/22.62 | COMBINE_EQS: (112), (116) imply: % 163.21/22.62 | (119) all_50_3 = all_43_4 % 163.21/22.62 | % 163.21/22.62 | COMBINE_EQS: (109), (118) imply: % 163.21/22.62 | (120) all_50_4 = all_43_5 % 163.21/22.62 | % 163.21/22.62 | REDUCE: (94), (111), (114) imply: % 163.21/22.62 | (121) sdtpldt1(all_43_5, all_43_4) = xI % 163.21/22.62 | % 163.21/22.62 | REDUCE: (89), (116), (118) imply: % 163.21/22.62 | (122) sdtpldt1(all_43_5, all_43_4) = all_53_3 % 163.21/22.62 | % 163.21/22.62 | BETA: splitting (77) gives: % 163.21/22.62 | % 163.21/22.62 | Case 1: % 163.21/22.62 | | % 163.46/22.62 | | (123) ~ (all_45_0 = 0) & ~ (all_45_1 = 0) & ! [v0: $i] : ( ~ % 163.46/22.62 | | (sdtasdt0(xu, v0) = xb) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) % 163.46/22.62 | | & aElement0(v0) = v1)) & ! [v0: $i] : ( ~ (aElement0(v0) = 0) % 163.46/22.62 | | | ~ $i(v0) | ? [v1: $i] : ( ~ (v1 = xb) & sdtasdt0(xu, v0) = v1 % 163.46/22.62 | | & $i(v1))) % 163.46/22.62 | | % 163.46/22.62 | | ALPHA: (123) implies: % 163.46/22.62 | | (124) ! [v0: $i] : ( ~ (aElement0(v0) = 0) | ~ $i(v0) | ? [v1: $i] : ( % 163.46/22.62 | | ~ (v1 = xb) & sdtasdt0(xu, v0) = v1 & $i(v1))) % 163.46/22.62 | | % 163.46/22.63 | | GROUND_INST: instantiating (40) with xI, all_53_3, all_43_4, all_43_5, % 163.46/22.63 | | simplifying with (121), (122) gives: % 163.46/22.63 | | (125) all_53_3 = xI % 163.46/22.63 | | % 163.46/22.63 | | REDUCE: (88), (125) imply: % 163.46/22.63 | | (126) $i(xI) % 163.46/22.63 | | % 163.46/22.63 | | GROUND_INST: instantiating (124) with xq, simplifying with (32), (58) gives: % 163.46/22.63 | | (127) ? [v0: $i] : ( ~ (v0 = xb) & sdtasdt0(xu, xq) = v0 & $i(v0)) % 163.46/22.63 | | % 163.46/22.63 | | GROUND_INST: instantiating (14) with all_59_0, sz10, simplifying with (1), % 163.46/22.63 | | (17), (99), (100) gives: % 163.46/22.63 | | (128) sz10 = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] % 163.46/22.63 | | : ? [v4: $i] : ? [v5: any] : (iLess0(v4, v0) = v5 & sbrdtbr0(v2) % 163.46/22.63 | | = v4 & sbrdtbr0(sz10) = v0 & sdtasdt0(v1, sz10) = v3 & % 163.46/22.63 | | sdtpldt0(v3, v2) = all_59_0 & aElement0(v2) = 0 & aElement0(v1) = % 163.46/22.63 | | 0 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & (v5 = 0 | v2 = % 163.46/22.63 | | sz00)) % 163.46/22.63 | | % 163.46/22.63 | | GROUND_INST: instantiating (mSortsB) with all_36_1, all_36_0, xu, % 163.46/22.63 | | simplifying with (49), (50), (51) gives: % 163.46/22.63 | | (129) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_36_0) = % 163.46/22.63 | | v1 & aElement0(all_36_1) = v0 & aElement0(xu) = v2 & ( ~ (v1 = 0) % 163.46/22.63 | | | ~ (v0 = 0) | v2 = 0)) % 163.46/22.63 | | % 163.46/22.63 | | GROUND_INST: instantiating (4) with all_41_3, xb, simplifying with (57), % 163.46/22.63 | | (104) gives: % 163.46/22.63 | | (130) ? [v0: any] : ? [v1: $i] : (sdtpldt0(sz00, all_41_3) = v1 & % 163.46/22.63 | | aElement0(all_41_3) = v0 & $i(v1) & ( ~ (v0 = 0) | (v1 = xb & % 163.46/22.63 | | all_41_3 = xb))) % 163.46/22.63 | | % 163.46/22.63 | | GROUND_INST: instantiating (3) with sz00, all_41_3, xb, simplifying with % 163.46/22.63 | | (57), (104), (105) gives: % 163.46/22.63 | | (131) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(sz00, % 163.46/22.63 | | all_41_3) = v2 & aElement0(all_41_3) = v1 & aElement0(sz00) = % 163.46/22.63 | | v0 & $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = xb)) % 163.46/22.63 | | % 163.46/22.63 | | GROUND_INST: instantiating (2) with all_41_3, sz00, xb, simplifying with % 163.46/22.63 | | (57), (104), (105) gives: % 163.46/22.63 | | (132) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(sz00, % 163.46/22.63 | | all_41_3) = v2 & aElement0(all_41_3) = v0 & aElement0(sz00) = % 163.46/22.63 | | v1 & $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = xb)) % 163.46/22.63 | | % 163.46/22.63 | | GROUND_INST: instantiating (mSortsB) with all_41_3, sz00, xb, simplifying % 163.46/22.63 | | with (57), (104), (105) gives: % 163.46/22.63 | | (133) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_41_3) = % 163.46/22.63 | | v0 & aElement0(xb) = v2 & aElement0(sz00) = v1 & ( ~ (v1 = 0) | % 163.46/22.63 | | ~ (v0 = 0) | v2 = 0)) % 163.46/22.63 | | % 163.46/22.63 | | GROUND_INST: instantiating (mSortsB) with all_50_1, all_50_0, xu, % 163.46/22.63 | | simplifying with (80), (81), (82) gives: % 163.46/22.63 | | (134) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_50_0) = % 163.46/22.63 | | v1 & aElement0(all_50_1) = v0 & aElement0(xu) = v2 & ( ~ (v1 = 0) % 163.46/22.63 | | | ~ (v0 = 0) | v2 = 0)) % 163.46/22.63 | | % 163.46/22.63 | | GROUND_INST: instantiating (9) with all_36_2, all_41_3, sz00, xb, all_36_0, % 163.46/22.63 | | simplifying with (48), (53), (57), (104), (105) gives: % 163.46/22.63 | | (135) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: % 163.46/22.63 | | $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? % 163.46/22.63 | | [v9: $i] : (sdtasdt0(all_41_3, all_36_2) = v7 & sdtasdt0(all_36_2, % 163.46/22.63 | | all_41_3) = v4 & sdtasdt0(all_36_2, xb) = v3 & % 163.46/22.63 | | sdtasdt0(all_36_2, sz00) = v5 & sdtasdt0(sz00, all_36_2) = v8 & % 163.46/22.63 | | sdtpldt0(v7, v8) = v9 & sdtpldt0(v4, v5) = v6 & % 163.46/22.63 | | aElement0(all_41_3) = v1 & aElement0(all_36_2) = v0 & % 163.46/22.63 | | aElement0(sz00) = v2 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) % 163.46/22.63 | | & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | % 163.46/22.63 | | (v9 = all_36_0 & v6 = v3))) % 163.46/22.63 | | % 163.46/22.63 | | GROUND_INST: instantiating (9) with all_43_3, all_41_3, sz00, xb, xb, % 163.46/22.63 | | simplifying with (57), (63), (69), (104), (105) gives: % 163.46/22.63 | | (136) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: % 163.46/22.63 | | $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? % 163.46/22.63 | | [v9: $i] : (sdtasdt0(all_43_3, all_41_3) = v4 & sdtasdt0(all_43_3, % 163.46/22.63 | | xb) = v3 & sdtasdt0(all_43_3, sz00) = v5 & sdtasdt0(all_41_3, % 163.46/22.63 | | all_43_3) = v7 & sdtasdt0(sz00, all_43_3) = v8 & sdtpldt0(v7, % 163.46/22.63 | | v8) = v9 & sdtpldt0(v4, v5) = v6 & aElement0(all_43_3) = v0 & % 163.46/22.63 | | aElement0(all_41_3) = v1 & aElement0(sz00) = v2 & $i(v9) & $i(v8) % 163.46/22.63 | | & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ % 163.46/22.63 | | (v1 = 0) | ~ (v0 = 0) | (v9 = xb & v6 = v3))) % 163.46/22.63 | | % 163.46/22.63 | | GROUND_INST: instantiating (9) with all_43_2, all_41_3, sz00, xb, sz00, % 163.46/22.63 | | simplifying with (57), (64), (70), (104), (105) gives: % 163.46/22.64 | | (137) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: % 163.46/22.64 | | $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? % 163.46/22.64 | | [v9: $i] : (sdtasdt0(all_43_2, all_41_3) = v4 & sdtasdt0(all_43_2, % 163.46/22.64 | | xb) = v3 & sdtasdt0(all_43_2, sz00) = v5 & sdtasdt0(all_41_3, % 163.46/22.64 | | all_43_2) = v7 & sdtasdt0(sz00, all_43_2) = v8 & sdtpldt0(v7, % 163.46/22.64 | | v8) = v9 & sdtpldt0(v4, v5) = v6 & aElement0(all_43_2) = v0 & % 163.46/22.64 | | aElement0(all_41_3) = v1 & aElement0(sz00) = v2 & $i(v9) & $i(v8) % 163.46/22.64 | | & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ % 163.46/22.64 | | (v1 = 0) | ~ (v0 = 0) | (v9 = sz00 & v6 = v3))) % 163.46/22.64 | | % 163.46/22.64 | | GROUND_INST: instantiating (7) with xu, all_34_0, all_43_0, xa, sz00, % 163.46/22.64 | | simplifying with (31), (43), (44), (66), (68) gives: % 163.46/22.64 | | (138) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: % 163.46/22.64 | | $i] : (sdtasdt0(all_34_0, all_43_0) = v3 & sdtasdt0(xu, v3) = v4 % 163.46/22.64 | | & aElement0(all_43_0) = v2 & aElement0(all_34_0) = v1 & % 163.46/22.64 | | aElement0(xu) = v0 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) % 163.46/22.64 | | | ~ (v0 = 0) | v4 = sz00)) % 163.46/22.64 | | % 163.46/22.64 | | GROUND_INST: instantiating (7) with xu, all_34_0, all_43_1, xa, xa, % 163.46/22.64 | | simplifying with (31), (43), (44), (65), (67) gives: % 163.46/22.64 | | (139) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: % 163.46/22.64 | | $i] : (sdtasdt0(all_34_0, all_43_1) = v3 & sdtasdt0(xu, v3) = v4 % 163.46/22.64 | | & aElement0(all_43_1) = v2 & aElement0(all_34_0) = v1 & % 163.46/22.64 | | aElement0(xu) = v0 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) % 163.46/22.64 | | | ~ (v0 = 0) | v4 = xa)) % 163.46/22.64 | | % 163.46/22.64 | | GROUND_INST: instantiating (7) with xu, all_34_0, all_36_3, xa, all_36_1, % 163.46/22.64 | | simplifying with (31), (43), (44), (47), (52) gives: % 163.46/22.64 | | (140) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: % 163.46/22.64 | | $i] : (sdtasdt0(all_34_0, all_36_3) = v3 & sdtasdt0(xu, v3) = v4 % 163.46/22.64 | | & aElement0(all_36_3) = v2 & aElement0(all_34_0) = v1 & % 163.46/22.64 | | aElement0(xu) = v0 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) % 163.46/22.64 | | | ~ (v0 = 0) | v4 = all_36_1)) % 163.46/22.64 | | % 163.46/22.64 | | GROUND_INST: instantiating (6) with all_34_0, xu, xa, simplifying with (31), % 163.46/22.64 | | (43), (44) gives: % 163.46/22.64 | | (141) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_34_0, xu) % 163.46/22.64 | | = v2 & aElement0(all_34_0) = v0 & aElement0(xu) = v1 & $i(v2) & ( % 163.46/22.64 | | ~ (v1 = 0) | ~ (v0 = 0) | v2 = xa)) % 163.46/22.64 | | % 163.46/22.64 | | GROUND_INST: instantiating (5) with xu, all_34_0, xa, simplifying with (31), % 163.46/22.64 | | (43), (44) gives: % 163.46/22.64 | | (142) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_34_0, xu) % 163.46/22.64 | | = v2 & aElement0(all_34_0) = v1 & aElement0(xu) = v0 & $i(v2) & ( % 163.46/22.64 | | ~ (v1 = 0) | ~ (v0 = 0) | v2 = xa)) % 163.46/22.64 | | % 163.46/22.64 | | GROUND_INST: instantiating (mSortsB_02) with xu, all_34_0, xa, simplifying % 163.46/22.64 | | with (31), (43), (44) gives: % 163.46/22.64 | | (143) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_34_0) = % 163.46/22.64 | | v1 & aElement0(xu) = v0 & aElement0(xa) = v2 & ( ~ (v1 = 0) | ~ % 163.46/22.64 | | (v0 = 0) | v2 = 0)) % 163.46/22.64 | | % 163.46/22.64 | | GROUND_INST: instantiating (8) with xq, all_50_1, all_50_0, xu, all_41_3, % 163.46/22.64 | | simplifying with (32), (60), (80), (81), (82) gives: % 163.46/22.64 | | (144) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: % 163.46/22.64 | | $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? % 163.46/22.64 | | [v9: $i] : (sdtasdt0(all_50_0, xq) = v8 & sdtasdt0(all_50_1, xq) = % 163.46/22.64 | | v7 & sdtasdt0(xq, all_50_0) = v4 & sdtasdt0(xq, all_50_1) = v3 & % 163.46/22.64 | | sdtasdt0(xu, xq) = v6 & sdtpldt0(v7, v8) = v9 & sdtpldt0(v3, v4) % 163.46/22.64 | | = v5 & aElement0(all_50_0) = v2 & aElement0(all_50_1) = v1 & % 163.46/22.64 | | aElement0(xq) = v0 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & % 163.46/22.64 | | $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | (v9 % 163.46/22.64 | | = v6 & v5 = all_41_3))) % 163.46/22.64 | | % 163.46/22.64 | | GROUND_INST: instantiating (8) with xq, all_36_1, all_36_0, xu, all_41_3, % 163.46/22.64 | | simplifying with (32), (49), (50), (51), (60) gives: % 163.46/22.64 | | (145) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: % 163.46/22.64 | | $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? % 163.46/22.64 | | [v9: $i] : (sdtasdt0(all_36_0, xq) = v8 & sdtasdt0(all_36_1, xq) = % 163.46/22.64 | | v7 & sdtasdt0(xq, all_36_0) = v4 & sdtasdt0(xq, all_36_1) = v3 & % 163.46/22.64 | | sdtasdt0(xu, xq) = v6 & sdtpldt0(v7, v8) = v9 & sdtpldt0(v3, v4) % 163.46/22.64 | | = v5 & aElement0(all_36_0) = v2 & aElement0(all_36_1) = v1 & % 163.46/22.64 | | aElement0(xq) = v0 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & % 163.46/22.64 | | $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | (v9 % 163.46/22.64 | | = v6 & v5 = all_41_3))) % 163.46/22.64 | | % 163.46/22.64 | | GROUND_INST: instantiating (6) with xu, xq, all_41_3, simplifying with (31), % 163.46/22.64 | | (32), (60) gives: % 163.46/22.64 | | (146) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(xu, xq) = v2 % 163.46/22.64 | | & aElement0(xq) = v1 & aElement0(xu) = v0 & $i(v2) & ( ~ (v1 = 0) % 163.46/22.64 | | | ~ (v0 = 0) | v2 = all_41_3)) % 163.46/22.64 | | % 163.46/22.64 | | GROUND_INST: instantiating (5) with xq, xu, all_41_3, simplifying with (31), % 163.46/22.64 | | (32), (60) gives: % 163.46/22.64 | | (147) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(xu, xq) = v2 % 163.46/22.64 | | & aElement0(xq) = v0 & aElement0(xu) = v1 & $i(v2) & ( ~ (v1 = 0) % 163.46/22.64 | | | ~ (v0 = 0) | v2 = all_41_3)) % 163.46/22.64 | | % 163.46/22.64 | | GROUND_INST: instantiating (mSortsB_02) with xq, xu, all_41_3, simplifying % 163.46/22.64 | | with (31), (32), (60) gives: % 163.46/22.64 | | (148) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_41_3) = % 163.46/22.64 | | v2 & aElement0(xq) = v0 & aElement0(xu) = v1 & ( ~ (v1 = 0) | ~ % 163.46/22.64 | | (v0 = 0) | v2 = 0)) % 163.46/22.64 | | % 163.46/22.64 | | GROUND_INST: instantiating (11) with xI, xu, simplifying with (31), (83), % 163.46/22.64 | | (93), (126) gives: % 163.46/22.64 | | (149) aElement0(xu) = 0 % 163.46/22.64 | | % 163.46/22.65 | | GROUND_INST: instantiating (12) with xI, xu, xq, all_41_3, simplifying with % 163.46/22.65 | | (31), (32), (60), (83), (95), (126) gives: % 163.46/22.65 | | (150) ? [v0: any] : ? [v1: any] : (aElementOf0(all_41_3, xI) = v1 & % 163.46/22.65 | | aElement0(xq) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 163.46/22.65 | | % 163.46/22.65 | | GROUND_INST: instantiating (13) with xu, all_41_1, simplifying with (31), % 163.46/22.65 | | (61) gives: % 163.46/22.65 | | (151) xu = sz00 | ? [v0: any] : ? [v1: any] : % 163.46/22.65 | | (aNaturalNumber0(all_41_1) = v1 & aElement0(xu) = v0 & ( ~ (v0 = 0) % 163.46/22.65 | | | v1 = 0)) % 163.46/22.65 | | % 163.46/22.65 | | GROUND_INST: instantiating (16) with xa, xu, 0, simplifying with (18), (27), % 163.46/22.65 | | (31), (45) gives: % 163.46/22.65 | | (152) ? [v0: any] : ? [v1: any] : (aDivisorOf0(xu, xa) = v0 & % 163.46/22.65 | | aElement0(xu) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 163.46/22.65 | | % 163.46/22.65 | | GROUND_INST: instantiating (15) with xa, xu, simplifying with (18), (27), % 163.46/22.65 | | (31), (45) gives: % 163.46/22.65 | | (153) ? [v0: any] : ? [v1: any] : (aDivisorOf0(xu, xa) = v1 & % 163.46/22.65 | | aElement0(xu) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 163.46/22.65 | | % 163.46/22.65 | | GROUND_INST: instantiating (101) with xu, 0, simplifying with (31), (45) % 163.46/22.65 | | gives: % 163.46/22.65 | | (154) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? [v4: % 163.46/22.65 | | any] : ? [v5: $i] : ? [v6: int] : ? [v7: $i] : % 163.46/22.65 | | (aDivisorOf0(xu, xb) = v3 & aDivisorOf0(xu, xa) = v1 & % 163.46/22.65 | | doDivides0(xu, xc) = v4 & doDivides0(xu, xb) = v2 & aElement0(xu) % 163.46/22.65 | | = v0 & $i(v5) & ((v7 = xc & v6 = 0 & v4 = 0 & sdtasdt0(xu, v5) = % 163.46/22.65 | | xc & aElement0(v5) = 0) | ( ~ (v3 = 0) & ~ (v2 = 0) & ! % 163.46/22.65 | | [v8: $i] : ( ~ (sdtasdt0(xu, v8) = xb) | ~ $i(v8) | ? [v9: % 163.46/22.65 | | int] : ( ~ (v9 = 0) & aElement0(v8) = v9)) & ! [v8: $i] % 163.46/22.65 | | : ( ~ (aElement0(v8) = 0) | ~ $i(v8) | ? [v9: $i] : ( ~ (v9 % 163.46/22.65 | | = xb) & sdtasdt0(xu, v8) = v9 & $i(v9)))) | ( ~ (v1 = % 163.46/22.65 | | 0) & ~ (v0 = 0)))) % 163.46/22.65 | | % 163.46/22.65 | | GROUND_INST: instantiating (16) with xb, xu, all_38_0, simplifying with % 163.46/22.65 | | (19), (30), (31), (55) gives: % 163.46/22.65 | | (155) ? [v0: any] : ? [v1: any] : (aDivisorOf0(xu, xb) = v0 & % 163.46/22.65 | | aElement0(xu) = v1 & ( ~ (v0 = 0) | (v1 = 0 & all_38_0 = 0))) % 163.46/22.65 | | % 163.46/22.65 | | GROUND_INST: instantiating (102) with xu, all_38_0, simplifying with (31), % 163.46/22.65 | | (55) gives: % 163.46/22.65 | | (156) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? [v4: % 163.46/22.65 | | any] : ? [v5: $i] : ? [v6: int] : ? [v7: $i] : % 163.46/22.65 | | (aDivisorOf0(xu, xb) = v3 & aDivisorOf0(xu, xa) = v2 & % 163.46/22.65 | | doDivides0(xu, xc) = v4 & doDivides0(xu, xa) = v1 & aElement0(xu) % 163.46/22.65 | | = v0 & $i(v5) & ((v7 = xc & v6 = 0 & v4 = 0 & sdtasdt0(xu, v5) = % 163.46/22.65 | | xc & aElement0(v5) = 0) | ( ~ (v3 = 0) & ~ (all_38_0 = 0) & % 163.46/22.65 | | ! [v8: $i] : ( ~ (sdtasdt0(xu, v8) = xb) | ~ $i(v8) | ? % 163.46/22.65 | | [v9: int] : ( ~ (v9 = 0) & aElement0(v8) = v9)) & ! [v8: % 163.46/22.65 | | $i] : ( ~ (aElement0(v8) = 0) | ~ $i(v8) | ? [v9: $i] : ( % 163.46/22.65 | | ~ (v9 = xb) & sdtasdt0(xu, v8) = v9 & $i(v9)))) | ( ~ (v2 % 163.46/22.65 | | = 0) & ( ~ (v0 = 0) | ( ~ (v1 = 0) & ! [v8: $i] : ( ~ % 163.46/22.65 | | (sdtasdt0(xu, v8) = xa) | ~ $i(v8) | ? [v9: int] : ( % 163.46/22.65 | | ~ (v9 = 0) & aElement0(v8) = v9)) & ! [v8: $i] : ( ~ % 163.46/22.65 | | (aElement0(v8) = 0) | ~ $i(v8) | ? [v9: $i] : ( ~ (v9 % 163.46/22.65 | | = xa) & sdtasdt0(xu, v8) = v9 & $i(v9)))))))) % 163.46/22.65 | | % 163.46/22.65 | | GROUND_INST: instantiating (103) with xu, all_45_0, simplifying with (31), % 163.46/22.65 | | (76) gives: % 163.58/22.65 | | (157) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? [v4: % 163.58/22.65 | | any] : ? [v5: $i] : ? [v6: int] : ? [v7: $i] : % 163.58/22.65 | | (aDivisorOf0(xu, xa) = v2 & doDivides0(xu, xc) = v4 & % 163.58/22.65 | | doDivides0(xu, xb) = v3 & doDivides0(xu, xa) = v1 & aElement0(xu) % 163.58/22.65 | | = v0 & $i(v5) & ((v7 = xc & v6 = 0 & v4 = 0 & sdtasdt0(xu, v5) = % 163.58/22.65 | | xc & aElement0(v5) = 0) | ( ~ (v3 = 0) & ~ (all_45_0 = 0) & % 163.58/22.65 | | ! [v8: $i] : ( ~ (sdtasdt0(xu, v8) = xb) | ~ $i(v8) | ? % 163.58/22.65 | | [v9: int] : ( ~ (v9 = 0) & aElement0(v8) = v9)) & ! [v8: % 163.58/22.65 | | $i] : ( ~ (aElement0(v8) = 0) | ~ $i(v8) | ? [v9: $i] : ( % 163.58/22.65 | | ~ (v9 = xb) & sdtasdt0(xu, v8) = v9 & $i(v9)))) | ( ~ (v2 % 163.58/22.65 | | = 0) & ( ~ (v0 = 0) | ( ~ (v1 = 0) & ! [v8: $i] : ( ~ % 163.58/22.65 | | (sdtasdt0(xu, v8) = xa) | ~ $i(v8) | ? [v9: int] : ( % 163.58/22.65 | | ~ (v9 = 0) & aElement0(v8) = v9)) & ! [v8: $i] : ( ~ % 163.58/22.65 | | (aElement0(v8) = 0) | ~ $i(v8) | ? [v9: $i] : ( ~ (v9 % 163.58/22.65 | | = xa) & sdtasdt0(xu, v8) = v9 & $i(v9)))))))) % 163.58/22.65 | | % 163.58/22.65 | | DELTA: instantiating (127) with fresh symbol all_233_0 gives: % 163.58/22.65 | | (158) ~ (all_233_0 = xb) & sdtasdt0(xu, xq) = all_233_0 & $i(all_233_0) % 163.58/22.65 | | % 163.58/22.65 | | ALPHA: (158) implies: % 163.58/22.65 | | (159) ~ (all_233_0 = xb) % 163.58/22.65 | | (160) sdtasdt0(xu, xq) = all_233_0 % 163.58/22.65 | | % 163.58/22.65 | | DELTA: instantiating (153) with fresh symbols all_337_0, all_337_1 gives: % 163.58/22.65 | | (161) aDivisorOf0(xu, xa) = all_337_0 & aElement0(xu) = all_337_1 & ( ~ % 163.58/22.65 | | (all_337_1 = 0) | all_337_0 = 0) % 163.58/22.65 | | % 163.58/22.65 | | ALPHA: (161) implies: % 163.58/22.65 | | (162) aElement0(xu) = all_337_1 % 163.58/22.65 | | % 163.58/22.65 | | DELTA: instantiating (152) with fresh symbols all_339_0, all_339_1 gives: % 163.58/22.65 | | (163) aDivisorOf0(xu, xa) = all_339_1 & aElement0(xu) = all_339_0 & ( ~ % 163.58/22.65 | | (all_339_1 = 0) | all_339_0 = 0) % 163.58/22.65 | | % 163.58/22.65 | | ALPHA: (163) implies: % 163.58/22.66 | | (164) aElement0(xu) = all_339_0 % 163.58/22.66 | | % 163.58/22.66 | | DELTA: instantiating (150) with fresh symbols all_1119_0, all_1119_1 gives: % 163.58/22.66 | | (165) aElementOf0(all_41_3, xI) = all_1119_0 & aElement0(xq) = all_1119_1 % 163.58/22.66 | | & ( ~ (all_1119_1 = 0) | all_1119_0 = 0) % 163.58/22.66 | | % 163.58/22.66 | | ALPHA: (165) implies: % 163.58/22.66 | | (166) aElement0(xq) = all_1119_1 % 163.58/22.66 | | % 163.58/22.66 | | DELTA: instantiating (155) with fresh symbols all_1211_0, all_1211_1 gives: % 163.58/22.66 | | (167) aDivisorOf0(xu, xb) = all_1211_1 & aElement0(xu) = all_1211_0 & ( ~ % 163.58/22.66 | | (all_1211_1 = 0) | (all_1211_0 = 0 & all_38_0 = 0)) % 163.58/22.66 | | % 163.58/22.66 | | ALPHA: (167) implies: % 163.58/22.66 | | (168) aElement0(xu) = all_1211_0 % 163.58/22.66 | | % 163.58/22.66 | | DELTA: instantiating (133) with fresh symbols all_1230_0, all_1230_1, % 163.58/22.66 | | all_1230_2 gives: % 163.58/22.66 | | (169) aElement0(all_41_3) = all_1230_2 & aElement0(xb) = all_1230_0 & % 163.58/22.66 | | aElement0(sz00) = all_1230_1 & ( ~ (all_1230_1 = 0) | ~ % 163.58/22.66 | | (all_1230_2 = 0) | all_1230_0 = 0) % 163.58/22.66 | | % 163.58/22.66 | | ALPHA: (169) implies: % 163.58/22.66 | | (170) aElement0(all_41_3) = all_1230_2 % 163.58/22.66 | | % 163.58/22.66 | | DELTA: instantiating (143) with fresh symbols all_1232_0, all_1232_1, % 163.58/22.66 | | all_1232_2 gives: % 163.58/22.66 | | (171) aElement0(all_34_0) = all_1232_1 & aElement0(xu) = all_1232_2 & % 163.58/22.66 | | aElement0(xa) = all_1232_0 & ( ~ (all_1232_1 = 0) | ~ (all_1232_2 % 163.58/22.66 | | = 0) | all_1232_0 = 0) % 163.58/22.66 | | % 163.58/22.66 | | ALPHA: (171) implies: % 163.58/22.66 | | (172) aElement0(xu) = all_1232_2 % 163.58/22.66 | | % 163.58/22.66 | | DELTA: instantiating (130) with fresh symbols all_1234_0, all_1234_1 gives: % 163.58/22.66 | | (173) sdtpldt0(sz00, all_41_3) = all_1234_0 & aElement0(all_41_3) = % 163.58/22.66 | | all_1234_1 & $i(all_1234_0) & ( ~ (all_1234_1 = 0) | (all_1234_0 = % 163.58/22.66 | | xb & all_41_3 = xb)) % 163.58/22.66 | | % 163.58/22.66 | | ALPHA: (173) implies: % 163.58/22.66 | | (174) aElement0(all_41_3) = all_1234_1 % 163.58/22.66 | | (175) ~ (all_1234_1 = 0) | (all_1234_0 = xb & all_41_3 = xb) % 163.58/22.66 | | % 163.58/22.66 | | DELTA: instantiating (129) with fresh symbols all_1237_0, all_1237_1, % 163.58/22.66 | | all_1237_2 gives: % 163.58/22.66 | | (176) aElement0(all_36_0) = all_1237_1 & aElement0(all_36_1) = all_1237_2 % 163.58/22.66 | | & aElement0(xu) = all_1237_0 & ( ~ (all_1237_1 = 0) | ~ % 163.58/22.66 | | (all_1237_2 = 0) | all_1237_0 = 0) % 163.58/22.66 | | % 163.58/22.66 | | ALPHA: (176) implies: % 163.58/22.66 | | (177) aElement0(xu) = all_1237_0 % 163.58/22.66 | | % 163.58/22.66 | | DELTA: instantiating (148) with fresh symbols all_1255_0, all_1255_1, % 163.58/22.66 | | all_1255_2 gives: % 163.58/22.66 | | (178) aElement0(all_41_3) = all_1255_0 & aElement0(xq) = all_1255_2 & % 163.58/22.66 | | aElement0(xu) = all_1255_1 & ( ~ (all_1255_1 = 0) | ~ (all_1255_2 % 163.58/22.66 | | = 0) | all_1255_0 = 0) % 163.58/22.66 | | % 163.58/22.66 | | ALPHA: (178) implies: % 163.58/22.66 | | (179) aElement0(xu) = all_1255_1 % 163.58/22.66 | | (180) aElement0(xq) = all_1255_2 % 163.58/22.66 | | (181) aElement0(all_41_3) = all_1255_0 % 163.58/22.66 | | (182) ~ (all_1255_1 = 0) | ~ (all_1255_2 = 0) | all_1255_0 = 0 % 163.58/22.66 | | % 163.58/22.66 | | DELTA: instantiating (134) with fresh symbols all_1257_0, all_1257_1, % 163.58/22.66 | | all_1257_2 gives: % 163.58/22.66 | | (183) aElement0(all_50_0) = all_1257_1 & aElement0(all_50_1) = all_1257_2 % 163.58/22.66 | | & aElement0(xu) = all_1257_0 & ( ~ (all_1257_1 = 0) | ~ % 163.58/22.66 | | (all_1257_2 = 0) | all_1257_0 = 0) % 163.58/22.66 | | % 163.58/22.66 | | ALPHA: (183) implies: % 163.58/22.66 | | (184) aElement0(xu) = all_1257_0 % 163.58/22.66 | | % 163.58/22.66 | | DELTA: instantiating (132) with fresh symbols all_1280_0, all_1280_1, % 163.58/22.66 | | all_1280_2 gives: % 163.58/22.66 | | (185) sdtpldt0(sz00, all_41_3) = all_1280_0 & aElement0(all_41_3) = % 163.58/22.66 | | all_1280_2 & aElement0(sz00) = all_1280_1 & $i(all_1280_0) & ( ~ % 163.58/22.66 | | (all_1280_1 = 0) | ~ (all_1280_2 = 0) | all_1280_0 = xb) % 163.58/22.66 | | % 163.58/22.66 | | ALPHA: (185) implies: % 163.58/22.66 | | (186) aElement0(all_41_3) = all_1280_2 % 163.58/22.66 | | % 163.58/22.66 | | DELTA: instantiating (142) with fresh symbols all_1284_0, all_1284_1, % 163.58/22.66 | | all_1284_2 gives: % 163.58/22.66 | | (187) sdtasdt0(all_34_0, xu) = all_1284_0 & aElement0(all_34_0) = % 163.58/22.66 | | all_1284_1 & aElement0(xu) = all_1284_2 & $i(all_1284_0) & ( ~ % 163.58/22.66 | | (all_1284_1 = 0) | ~ (all_1284_2 = 0) | all_1284_0 = xa) % 163.58/22.66 | | % 163.58/22.66 | | ALPHA: (187) implies: % 163.58/22.66 | | (188) aElement0(xu) = all_1284_2 % 163.58/22.66 | | % 163.58/22.66 | | DELTA: instantiating (141) with fresh symbols all_1286_0, all_1286_1, % 163.58/22.66 | | all_1286_2 gives: % 163.58/22.66 | | (189) sdtasdt0(all_34_0, xu) = all_1286_0 & aElement0(all_34_0) = % 163.58/22.66 | | all_1286_2 & aElement0(xu) = all_1286_1 & $i(all_1286_0) & ( ~ % 163.58/22.66 | | (all_1286_1 = 0) | ~ (all_1286_2 = 0) | all_1286_0 = xa) % 163.58/22.66 | | % 163.58/22.66 | | ALPHA: (189) implies: % 163.58/22.66 | | (190) aElement0(xu) = all_1286_1 % 163.58/22.66 | | % 163.58/22.66 | | DELTA: instantiating (131) with fresh symbols all_1296_0, all_1296_1, % 163.58/22.66 | | all_1296_2 gives: % 163.58/22.66 | | (191) sdtpldt0(sz00, all_41_3) = all_1296_0 & aElement0(all_41_3) = % 163.58/22.66 | | all_1296_1 & aElement0(sz00) = all_1296_2 & $i(all_1296_0) & ( ~ % 163.58/22.66 | | (all_1296_1 = 0) | ~ (all_1296_2 = 0) | all_1296_0 = xb) % 163.58/22.66 | | % 163.58/22.66 | | ALPHA: (191) implies: % 163.58/22.66 | | (192) aElement0(all_41_3) = all_1296_1 % 163.58/22.66 | | % 163.58/22.66 | | DELTA: instantiating (146) with fresh symbols all_1308_0, all_1308_1, % 163.58/22.66 | | all_1308_2 gives: % 163.58/22.66 | | (193) sdtasdt0(xu, xq) = all_1308_0 & aElement0(xq) = all_1308_1 & % 163.58/22.66 | | aElement0(xu) = all_1308_2 & $i(all_1308_0) & ( ~ (all_1308_1 = 0) % 163.58/22.66 | | | ~ (all_1308_2 = 0) | all_1308_0 = all_41_3) % 163.58/22.66 | | % 163.58/22.66 | | ALPHA: (193) implies: % 163.58/22.66 | | (194) aElement0(xu) = all_1308_2 % 163.58/22.66 | | (195) aElement0(xq) = all_1308_1 % 163.58/22.66 | | (196) sdtasdt0(xu, xq) = all_1308_0 % 163.58/22.66 | | (197) ~ (all_1308_1 = 0) | ~ (all_1308_2 = 0) | all_1308_0 = all_41_3 % 163.58/22.66 | | % 163.58/22.66 | | DELTA: instantiating (147) with fresh symbols all_1320_0, all_1320_1, % 163.58/22.66 | | all_1320_2 gives: % 163.58/22.66 | | (198) sdtasdt0(xu, xq) = all_1320_0 & aElement0(xq) = all_1320_2 & % 163.58/22.66 | | aElement0(xu) = all_1320_1 & $i(all_1320_0) & ( ~ (all_1320_1 = 0) % 163.58/22.66 | | | ~ (all_1320_2 = 0) | all_1320_0 = all_41_3) % 163.58/22.66 | | % 163.58/22.66 | | ALPHA: (198) implies: % 163.58/22.66 | | (199) aElement0(xu) = all_1320_1 % 163.58/22.66 | | (200) aElement0(xq) = all_1320_2 % 163.58/22.66 | | (201) sdtasdt0(xu, xq) = all_1320_0 % 163.58/22.66 | | % 163.58/22.66 | | DELTA: instantiating (138) with fresh symbols all_1386_0, all_1386_1, % 163.58/22.66 | | all_1386_2, all_1386_3, all_1386_4 gives: % 163.58/22.66 | | (202) sdtasdt0(all_34_0, all_43_0) = all_1386_1 & sdtasdt0(xu, % 163.58/22.66 | | all_1386_1) = all_1386_0 & aElement0(all_43_0) = all_1386_2 & % 163.58/22.66 | | aElement0(all_34_0) = all_1386_3 & aElement0(xu) = all_1386_4 & % 163.58/22.66 | | $i(all_1386_0) & $i(all_1386_1) & ( ~ (all_1386_2 = 0) | ~ % 163.58/22.66 | | (all_1386_3 = 0) | ~ (all_1386_4 = 0) | all_1386_0 = sz00) % 163.58/22.66 | | % 163.58/22.66 | | ALPHA: (202) implies: % 163.58/22.66 | | (203) aElement0(xu) = all_1386_4 % 163.58/22.66 | | % 163.58/22.66 | | DELTA: instantiating (140) with fresh symbols all_1476_0, all_1476_1, % 163.58/22.66 | | all_1476_2, all_1476_3, all_1476_4 gives: % 163.58/22.66 | | (204) sdtasdt0(all_34_0, all_36_3) = all_1476_1 & sdtasdt0(xu, % 163.58/22.66 | | all_1476_1) = all_1476_0 & aElement0(all_36_3) = all_1476_2 & % 163.58/22.66 | | aElement0(all_34_0) = all_1476_3 & aElement0(xu) = all_1476_4 & % 163.58/22.66 | | $i(all_1476_0) & $i(all_1476_1) & ( ~ (all_1476_2 = 0) | ~ % 163.58/22.66 | | (all_1476_3 = 0) | ~ (all_1476_4 = 0) | all_1476_0 = all_36_1) % 163.58/22.66 | | % 163.58/22.66 | | ALPHA: (204) implies: % 163.58/22.66 | | (205) aElement0(xu) = all_1476_4 % 163.58/22.66 | | % 163.58/22.66 | | DELTA: instantiating (139) with fresh symbols all_1478_0, all_1478_1, % 163.58/22.66 | | all_1478_2, all_1478_3, all_1478_4 gives: % 163.58/22.66 | | (206) sdtasdt0(all_34_0, all_43_1) = all_1478_1 & sdtasdt0(xu, % 163.58/22.66 | | all_1478_1) = all_1478_0 & aElement0(all_43_1) = all_1478_2 & % 163.58/22.66 | | aElement0(all_34_0) = all_1478_3 & aElement0(xu) = all_1478_4 & % 163.58/22.66 | | $i(all_1478_0) & $i(all_1478_1) & ( ~ (all_1478_2 = 0) | ~ % 163.58/22.66 | | (all_1478_3 = 0) | ~ (all_1478_4 = 0) | all_1478_0 = xa) % 163.58/22.66 | | % 163.58/22.66 | | ALPHA: (206) implies: % 163.58/22.66 | | (207) aElement0(xu) = all_1478_4 % 163.58/22.66 | | % 163.58/22.66 | | DELTA: instantiating (136) with fresh symbols all_1946_0, all_1946_1, % 163.58/22.66 | | all_1946_2, all_1946_3, all_1946_4, all_1946_5, all_1946_6, % 163.58/22.66 | | all_1946_7, all_1946_8, all_1946_9 gives: % 163.58/22.67 | | (208) sdtasdt0(all_43_3, all_41_3) = all_1946_5 & sdtasdt0(all_43_3, xb) % 163.58/22.67 | | = all_1946_6 & sdtasdt0(all_43_3, sz00) = all_1946_4 & % 163.58/22.67 | | sdtasdt0(all_41_3, all_43_3) = all_1946_2 & sdtasdt0(sz00, % 163.58/22.67 | | all_43_3) = all_1946_1 & sdtpldt0(all_1946_2, all_1946_1) = % 163.58/22.67 | | all_1946_0 & sdtpldt0(all_1946_5, all_1946_4) = all_1946_3 & % 163.58/22.67 | | aElement0(all_43_3) = all_1946_9 & aElement0(all_41_3) = all_1946_8 % 163.58/22.67 | | & aElement0(sz00) = all_1946_7 & $i(all_1946_0) & $i(all_1946_1) & % 163.58/22.67 | | $i(all_1946_2) & $i(all_1946_3) & $i(all_1946_4) & $i(all_1946_5) & % 163.58/22.67 | | $i(all_1946_6) & ( ~ (all_1946_7 = 0) | ~ (all_1946_8 = 0) | ~ % 163.58/22.67 | | (all_1946_9 = 0) | (all_1946_0 = xb & all_1946_3 = all_1946_6)) % 163.58/22.67 | | % 163.58/22.67 | | ALPHA: (208) implies: % 163.58/22.67 | | (209) aElement0(all_41_3) = all_1946_8 % 163.58/22.67 | | % 163.58/22.67 | | DELTA: instantiating (144) with fresh symbols all_1948_0, all_1948_1, % 163.58/22.67 | | all_1948_2, all_1948_3, all_1948_4, all_1948_5, all_1948_6, % 163.58/22.67 | | all_1948_7, all_1948_8, all_1948_9 gives: % 163.58/22.67 | | (210) sdtasdt0(all_50_0, xq) = all_1948_1 & sdtasdt0(all_50_1, xq) = % 163.58/22.67 | | all_1948_2 & sdtasdt0(xq, all_50_0) = all_1948_5 & sdtasdt0(xq, % 163.58/22.67 | | all_50_1) = all_1948_6 & sdtasdt0(xu, xq) = all_1948_3 & % 163.58/22.67 | | sdtpldt0(all_1948_2, all_1948_1) = all_1948_0 & % 163.58/22.67 | | sdtpldt0(all_1948_6, all_1948_5) = all_1948_4 & aElement0(all_50_0) % 163.58/22.67 | | = all_1948_7 & aElement0(all_50_1) = all_1948_8 & aElement0(xq) = % 163.58/22.67 | | all_1948_9 & $i(all_1948_0) & $i(all_1948_1) & $i(all_1948_2) & % 163.58/22.67 | | $i(all_1948_3) & $i(all_1948_4) & $i(all_1948_5) & $i(all_1948_6) & % 163.58/22.67 | | ( ~ (all_1948_7 = 0) | ~ (all_1948_8 = 0) | ~ (all_1948_9 = 0) | % 163.58/22.67 | | (all_1948_0 = all_1948_3 & all_1948_4 = all_41_3)) % 163.58/22.67 | | % 163.58/22.67 | | ALPHA: (210) implies: % 163.58/22.67 | | (211) aElement0(xq) = all_1948_9 % 163.58/22.67 | | (212) sdtasdt0(xu, xq) = all_1948_3 % 163.58/22.67 | | % 163.58/22.67 | | DELTA: instantiating (135) with fresh symbols all_1950_0, all_1950_1, % 163.58/22.67 | | all_1950_2, all_1950_3, all_1950_4, all_1950_5, all_1950_6, % 163.58/22.67 | | all_1950_7, all_1950_8, all_1950_9 gives: % 163.58/22.67 | | (213) sdtasdt0(all_41_3, all_36_2) = all_1950_2 & sdtasdt0(all_36_2, % 163.58/22.67 | | all_41_3) = all_1950_5 & sdtasdt0(all_36_2, xb) = all_1950_6 & % 163.58/22.67 | | sdtasdt0(all_36_2, sz00) = all_1950_4 & sdtasdt0(sz00, all_36_2) = % 163.58/22.67 | | all_1950_1 & sdtpldt0(all_1950_2, all_1950_1) = all_1950_0 & % 163.58/22.67 | | sdtpldt0(all_1950_5, all_1950_4) = all_1950_3 & aElement0(all_41_3) % 163.58/22.67 | | = all_1950_8 & aElement0(all_36_2) = all_1950_9 & aElement0(sz00) = % 163.58/22.67 | | all_1950_7 & $i(all_1950_0) & $i(all_1950_1) & $i(all_1950_2) & % 163.58/22.67 | | $i(all_1950_3) & $i(all_1950_4) & $i(all_1950_5) & $i(all_1950_6) & % 163.58/22.67 | | ( ~ (all_1950_7 = 0) | ~ (all_1950_8 = 0) | ~ (all_1950_9 = 0) | % 163.58/22.67 | | (all_1950_0 = all_36_0 & all_1950_3 = all_1950_6)) % 163.58/22.67 | | % 163.58/22.67 | | ALPHA: (213) implies: % 163.58/22.67 | | (214) aElement0(all_41_3) = all_1950_8 % 163.58/22.67 | | % 163.58/22.67 | | DELTA: instantiating (137) with fresh symbols all_1952_0, all_1952_1, % 163.58/22.67 | | all_1952_2, all_1952_3, all_1952_4, all_1952_5, all_1952_6, % 163.58/22.67 | | all_1952_7, all_1952_8, all_1952_9 gives: % 163.58/22.67 | | (215) sdtasdt0(all_43_2, all_41_3) = all_1952_5 & sdtasdt0(all_43_2, xb) % 163.58/22.67 | | = all_1952_6 & sdtasdt0(all_43_2, sz00) = all_1952_4 & % 163.58/22.67 | | sdtasdt0(all_41_3, all_43_2) = all_1952_2 & sdtasdt0(sz00, % 163.58/22.67 | | all_43_2) = all_1952_1 & sdtpldt0(all_1952_2, all_1952_1) = % 163.58/22.67 | | all_1952_0 & sdtpldt0(all_1952_5, all_1952_4) = all_1952_3 & % 163.58/22.67 | | aElement0(all_43_2) = all_1952_9 & aElement0(all_41_3) = all_1952_8 % 163.58/22.67 | | & aElement0(sz00) = all_1952_7 & $i(all_1952_0) & $i(all_1952_1) & % 163.58/22.67 | | $i(all_1952_2) & $i(all_1952_3) & $i(all_1952_4) & $i(all_1952_5) & % 163.58/22.67 | | $i(all_1952_6) & ( ~ (all_1952_7 = 0) | ~ (all_1952_8 = 0) | ~ % 163.58/22.67 | | (all_1952_9 = 0) | (all_1952_0 = sz00 & all_1952_3 = all_1952_6)) % 163.58/22.67 | | % 163.58/22.67 | | ALPHA: (215) implies: % 163.58/22.67 | | (216) aElement0(all_41_3) = all_1952_8 % 163.58/22.67 | | % 163.58/22.67 | | DELTA: instantiating (145) with fresh symbols all_1956_0, all_1956_1, % 163.58/22.67 | | all_1956_2, all_1956_3, all_1956_4, all_1956_5, all_1956_6, % 163.58/22.67 | | all_1956_7, all_1956_8, all_1956_9 gives: % 163.58/22.67 | | (217) sdtasdt0(all_36_0, xq) = all_1956_1 & sdtasdt0(all_36_1, xq) = % 163.58/22.67 | | all_1956_2 & sdtasdt0(xq, all_36_0) = all_1956_5 & sdtasdt0(xq, % 163.58/22.67 | | all_36_1) = all_1956_6 & sdtasdt0(xu, xq) = all_1956_3 & % 163.58/22.67 | | sdtpldt0(all_1956_2, all_1956_1) = all_1956_0 & % 163.58/22.67 | | sdtpldt0(all_1956_6, all_1956_5) = all_1956_4 & aElement0(all_36_0) % 163.58/22.67 | | = all_1956_7 & aElement0(all_36_1) = all_1956_8 & aElement0(xq) = % 163.58/22.67 | | all_1956_9 & $i(all_1956_0) & $i(all_1956_1) & $i(all_1956_2) & % 163.58/22.67 | | $i(all_1956_3) & $i(all_1956_4) & $i(all_1956_5) & $i(all_1956_6) & % 163.58/22.67 | | ( ~ (all_1956_7 = 0) | ~ (all_1956_8 = 0) | ~ (all_1956_9 = 0) | % 163.58/22.67 | | (all_1956_0 = all_1956_3 & all_1956_4 = all_41_3)) % 163.58/22.67 | | % 163.58/22.67 | | ALPHA: (217) implies: % 163.58/22.67 | | (218) aElement0(xq) = all_1956_9 % 163.58/22.67 | | (219) sdtasdt0(xu, xq) = all_1956_3 % 163.58/22.67 | | % 163.58/22.67 | | DELTA: instantiating (154) with fresh symbols all_2100_0, all_2100_1, % 163.58/22.67 | | all_2100_2, all_2100_3, all_2100_4, all_2100_5, all_2100_6, % 163.58/22.67 | | all_2100_7 gives: % 163.58/22.67 | | (220) aDivisorOf0(xu, xb) = all_2100_4 & aDivisorOf0(xu, xa) = all_2100_6 % 163.58/22.67 | | & doDivides0(xu, xc) = all_2100_3 & doDivides0(xu, xb) = all_2100_5 % 163.58/22.67 | | & aElement0(xu) = all_2100_7 & $i(all_2100_2) & ((all_2100_0 = xc & % 163.58/22.67 | | all_2100_1 = 0 & all_2100_3 = 0 & sdtasdt0(xu, all_2100_2) = xc % 163.58/22.67 | | & aElement0(all_2100_2) = 0) | ( ~ (all_2100_4 = 0) & ~ % 163.58/22.67 | | (all_2100_5 = 0) & ! [v0: $i] : ( ~ (sdtasdt0(xu, v0) = xb) | % 163.58/22.67 | | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & aElement0(v0) = v1)) % 163.58/22.67 | | & ! [v0: $i] : ( ~ (aElement0(v0) = 0) | ~ $i(v0) | ? [v1: % 163.58/22.67 | | $i] : ( ~ (v1 = xb) & sdtasdt0(xu, v0) = v1 & $i(v1)))) | ( % 163.58/22.67 | | ~ (all_2100_6 = 0) & ~ (all_2100_7 = 0))) % 163.58/22.67 | | % 163.58/22.67 | | ALPHA: (220) implies: % 163.58/22.67 | | (221) aElement0(xu) = all_2100_7 % 163.58/22.67 | | % 163.58/22.67 | | DELTA: instantiating (156) with fresh symbols all_2164_0, all_2164_1, % 163.58/22.67 | | all_2164_2, all_2164_3, all_2164_4, all_2164_5, all_2164_6, % 163.58/22.67 | | all_2164_7 gives: % 163.58/22.67 | | (222) aDivisorOf0(xu, xb) = all_2164_4 & aDivisorOf0(xu, xa) = all_2164_5 % 163.58/22.67 | | & doDivides0(xu, xc) = all_2164_3 & doDivides0(xu, xa) = all_2164_6 % 163.58/22.67 | | & aElement0(xu) = all_2164_7 & $i(all_2164_2) & ((all_2164_0 = xc & % 163.58/22.67 | | all_2164_1 = 0 & all_2164_3 = 0 & sdtasdt0(xu, all_2164_2) = xc % 163.58/22.67 | | & aElement0(all_2164_2) = 0) | ( ~ (all_2164_4 = 0) & ~ % 163.58/22.67 | | (all_38_0 = 0) & ! [v0: $i] : ( ~ (sdtasdt0(xu, v0) = xb) | ~ % 163.58/22.67 | | $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & aElement0(v0) = v1)) & % 163.58/22.67 | | ! [v0: $i] : ( ~ (aElement0(v0) = 0) | ~ $i(v0) | ? [v1: $i] % 163.58/22.67 | | : ( ~ (v1 = xb) & sdtasdt0(xu, v0) = v1 & $i(v1)))) | ( ~ % 163.58/22.67 | | (all_2164_5 = 0) & ( ~ (all_2164_7 = 0) | ( ~ (all_2164_6 = 0) % 163.58/22.67 | | & ! [v0: $i] : ( ~ (sdtasdt0(xu, v0) = xa) | ~ $i(v0) | % 163.58/22.67 | | ? [v1: int] : ( ~ (v1 = 0) & aElement0(v0) = v1)) & ! % 163.58/22.67 | | [v0: $i] : ( ~ (aElement0(v0) = 0) | ~ $i(v0) | ? [v1: % 163.58/22.67 | | $i] : ( ~ (v1 = xa) & sdtasdt0(xu, v0) = v1 & % 163.58/22.67 | | $i(v1))))))) % 163.58/22.67 | | % 163.58/22.67 | | ALPHA: (222) implies: % 163.58/22.67 | | (223) aElement0(xu) = all_2164_7 % 163.58/22.67 | | % 163.58/22.67 | | DELTA: instantiating (157) with fresh symbols all_2166_0, all_2166_1, % 163.58/22.67 | | all_2166_2, all_2166_3, all_2166_4, all_2166_5, all_2166_6, % 163.58/22.67 | | all_2166_7 gives: % 163.58/22.68 | | (224) aDivisorOf0(xu, xa) = all_2166_5 & doDivides0(xu, xc) = all_2166_3 % 163.58/22.68 | | & doDivides0(xu, xb) = all_2166_4 & doDivides0(xu, xa) = all_2166_6 % 163.58/22.68 | | & aElement0(xu) = all_2166_7 & $i(all_2166_2) & ((all_2166_0 = xc & % 163.58/22.68 | | all_2166_1 = 0 & all_2166_3 = 0 & sdtasdt0(xu, all_2166_2) = xc % 163.58/22.68 | | & aElement0(all_2166_2) = 0) | ( ~ (all_2166_4 = 0) & ~ % 163.58/22.68 | | (all_45_0 = 0) & ! [v0: $i] : ( ~ (sdtasdt0(xu, v0) = xb) | ~ % 163.58/22.68 | | $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & aElement0(v0) = v1)) & % 163.58/22.68 | | ! [v0: $i] : ( ~ (aElement0(v0) = 0) | ~ $i(v0) | ? [v1: $i] % 163.58/22.68 | | : ( ~ (v1 = xb) & sdtasdt0(xu, v0) = v1 & $i(v1)))) | ( ~ % 163.58/22.68 | | (all_2166_5 = 0) & ( ~ (all_2166_7 = 0) | ( ~ (all_2166_6 = 0) % 163.58/22.68 | | & ! [v0: $i] : ( ~ (sdtasdt0(xu, v0) = xa) | ~ $i(v0) | % 163.58/22.68 | | ? [v1: int] : ( ~ (v1 = 0) & aElement0(v0) = v1)) & ! % 163.58/22.68 | | [v0: $i] : ( ~ (aElement0(v0) = 0) | ~ $i(v0) | ? [v1: % 163.58/22.68 | | $i] : ( ~ (v1 = xa) & sdtasdt0(xu, v0) = v1 & % 163.58/22.68 | | $i(v1))))))) % 163.58/22.68 | | % 163.58/22.68 | | ALPHA: (224) implies: % 163.58/22.68 | | (225) aElement0(xu) = all_2166_7 % 163.58/22.68 | | % 163.58/22.68 | | BETA: splitting (151) gives: % 163.58/22.68 | | % 163.58/22.68 | | Case 1: % 163.58/22.68 | | | % 163.58/22.68 | | | (226) xu = sz00 % 163.58/22.68 | | | % 163.58/22.68 | | | REDUCE: (79), (226) imply: % 163.58/22.68 | | | (227) $false % 163.58/22.68 | | | % 163.58/22.68 | | | CLOSE: (227) is inconsistent. % 163.58/22.68 | | | % 163.58/22.68 | | Case 2: % 163.58/22.68 | | | % 163.58/22.68 | | | (228) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(all_41_1) = v1 & % 163.58/22.68 | | | aElement0(xu) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 163.58/22.68 | | | % 163.58/22.68 | | | DELTA: instantiating (228) with fresh symbols all_2284_0, all_2284_1 % 163.58/22.68 | | | gives: % 163.58/22.68 | | | (229) aNaturalNumber0(all_41_1) = all_2284_0 & aElement0(xu) = % 163.58/22.68 | | | all_2284_1 & ( ~ (all_2284_1 = 0) | all_2284_0 = 0) % 163.58/22.68 | | | % 163.58/22.68 | | | ALPHA: (229) implies: % 163.58/22.68 | | | (230) aElement0(xu) = all_2284_1 % 163.58/22.68 | | | % 163.58/22.68 | | | BETA: splitting (128) gives: % 163.58/22.68 | | | % 163.58/22.68 | | | Case 1: % 163.58/22.68 | | | | % 163.58/22.68 | | | | (231) sz10 = sz00 % 163.58/22.68 | | | | % 163.58/22.68 | | | | REDUCE: (10), (231) imply: % 163.58/22.68 | | | | (232) $false % 163.58/22.68 | | | | % 163.58/22.68 | | | | CLOSE: (232) is inconsistent. % 163.58/22.68 | | | | % 163.58/22.68 | | | Case 2: % 163.58/22.68 | | | | % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with 0, all_339_0, xu, simplifying with % 163.58/22.68 | | | | (149), (164) gives: % 163.58/22.68 | | | | (233) all_339_0 = 0 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_339_0, all_1211_0, xu, % 163.58/22.68 | | | | simplifying with (164), (168) gives: % 163.58/22.68 | | | | (234) all_1211_0 = all_339_0 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1211_0, all_1232_2, xu, % 163.58/22.68 | | | | simplifying with (168), (172) gives: % 163.58/22.68 | | | | (235) all_1232_2 = all_1211_0 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1232_2, all_1237_0, xu, % 163.58/22.68 | | | | simplifying with (172), (177) gives: % 163.58/22.68 | | | | (236) all_1237_0 = all_1232_2 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1237_0, all_1255_1, xu, % 163.58/22.68 | | | | simplifying with (177), (179) gives: % 163.58/22.68 | | | | (237) all_1255_1 = all_1237_0 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1255_1, all_1257_0, xu, % 163.58/22.68 | | | | simplifying with (179), (184) gives: % 163.58/22.68 | | | | (238) all_1257_0 = all_1255_1 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1386_4, all_1476_4, xu, % 163.58/22.68 | | | | simplifying with (203), (205) gives: % 163.58/22.68 | | | | (239) all_1476_4 = all_1386_4 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1308_2, all_1476_4, xu, % 163.58/22.68 | | | | simplifying with (194), (205) gives: % 163.58/22.68 | | | | (240) all_1476_4 = all_1308_2 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1386_4, all_1478_4, xu, % 163.58/22.68 | | | | simplifying with (203), (207) gives: % 163.58/22.68 | | | | (241) all_1478_4 = all_1386_4 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1478_4, all_2100_7, xu, % 163.58/22.68 | | | | simplifying with (207), (221) gives: % 163.58/22.68 | | | | (242) all_2100_7 = all_1478_4 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_2100_7, all_2164_7, xu, % 163.58/22.68 | | | | simplifying with (221), (223) gives: % 163.58/22.68 | | | | (243) all_2164_7 = all_2100_7 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1284_2, all_2164_7, xu, % 163.58/22.68 | | | | simplifying with (188), (223) gives: % 163.58/22.68 | | | | (244) all_2164_7 = all_1284_2 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1308_2, all_2166_7, xu, % 163.58/22.68 | | | | simplifying with (194), (225) gives: % 163.58/22.68 | | | | (245) all_2166_7 = all_1308_2 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1286_1, all_2166_7, xu, % 163.58/22.68 | | | | simplifying with (190), (225) gives: % 163.58/22.68 | | | | (246) all_2166_7 = all_1286_1 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1257_0, all_2166_7, xu, % 163.58/22.68 | | | | simplifying with (184), (225) gives: % 163.58/22.68 | | | | (247) all_2166_7 = all_1257_0 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_337_1, all_2166_7, xu, % 163.58/22.68 | | | | simplifying with (162), (225) gives: % 163.58/22.68 | | | | (248) all_2166_7 = all_337_1 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1476_4, all_2284_1, xu, % 163.58/22.68 | | | | simplifying with (205), (230) gives: % 163.58/22.68 | | | | (249) all_2284_1 = all_1476_4 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1320_1, all_2284_1, xu, % 163.58/22.68 | | | | simplifying with (199), (230) gives: % 163.58/22.68 | | | | (250) all_2284_1 = all_1320_1 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with 0, all_1255_2, xq, simplifying with % 163.58/22.68 | | | | (58), (180) gives: % 163.58/22.68 | | | | (251) all_1255_2 = 0 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1255_2, all_1308_1, xq, % 163.58/22.68 | | | | simplifying with (180), (195) gives: % 163.58/22.68 | | | | (252) all_1308_1 = all_1255_2 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1308_1, all_1320_2, xq, % 163.58/22.68 | | | | simplifying with (195), (200) gives: % 163.58/22.68 | | | | (253) all_1320_2 = all_1308_1 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1320_2, all_1948_9, xq, % 163.58/22.68 | | | | simplifying with (200), (211) gives: % 163.58/22.68 | | | | (254) all_1948_9 = all_1320_2 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1948_9, all_1956_9, xq, % 163.58/22.68 | | | | simplifying with (211), (218) gives: % 163.58/22.68 | | | | (255) all_1956_9 = all_1948_9 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1119_1, all_1956_9, xq, % 163.58/22.68 | | | | simplifying with (166), (218) gives: % 163.58/22.68 | | | | (256) all_1956_9 = all_1119_1 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1234_1, all_1280_2, all_41_3, % 163.58/22.68 | | | | simplifying with (174), (186) gives: % 163.58/22.68 | | | | (257) all_1280_2 = all_1234_1 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1946_8, all_1950_8, all_41_3, % 163.58/22.68 | | | | simplifying with (209), (214) gives: % 163.58/22.68 | | | | (258) all_1950_8 = all_1946_8 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1296_1, all_1950_8, all_41_3, % 163.58/22.68 | | | | simplifying with (192), (214) gives: % 163.58/22.68 | | | | (259) all_1950_8 = all_1296_1 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1280_2, all_1950_8, all_41_3, % 163.58/22.68 | | | | simplifying with (186), (214) gives: % 163.58/22.68 | | | | (260) all_1950_8 = all_1280_2 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1230_2, all_1950_8, all_41_3, % 163.58/22.68 | | | | simplifying with (170), (214) gives: % 163.58/22.68 | | | | (261) all_1950_8 = all_1230_2 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1946_8, all_1952_8, all_41_3, % 163.58/22.68 | | | | simplifying with (209), (216) gives: % 163.58/22.68 | | | | (262) all_1952_8 = all_1946_8 % 163.58/22.68 | | | | % 163.58/22.68 | | | | GROUND_INST: instantiating (36) with all_1255_0, all_1952_8, all_41_3, % 163.58/22.68 | | | | simplifying with (181), (216) gives: % 163.58/22.68 | | | | (263) all_1952_8 = all_1255_0 % 163.58/22.68 | | | | % 163.58/22.69 | | | | GROUND_INST: instantiating (39) with all_233_0, all_1948_3, xq, xu, % 163.58/22.69 | | | | simplifying with (160), (212) gives: % 163.58/22.69 | | | | (264) all_1948_3 = all_233_0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | GROUND_INST: instantiating (39) with all_1948_3, all_1956_3, xq, xu, % 163.58/22.69 | | | | simplifying with (212), (219) gives: % 163.58/22.69 | | | | (265) all_1956_3 = all_1948_3 % 163.58/22.69 | | | | % 163.58/22.69 | | | | GROUND_INST: instantiating (39) with all_1320_0, all_1956_3, xq, xu, % 163.58/22.69 | | | | simplifying with (201), (219) gives: % 163.58/22.69 | | | | (266) all_1956_3 = all_1320_0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | GROUND_INST: instantiating (39) with all_1308_0, all_1956_3, xq, xu, % 163.58/22.69 | | | | simplifying with (196), (219) gives: % 163.58/22.69 | | | | (267) all_1956_3 = all_1308_0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (249), (250) imply: % 163.58/22.69 | | | | (268) all_1476_4 = all_1320_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (268) implies: % 163.58/22.69 | | | | (269) all_1476_4 = all_1320_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (245), (246) imply: % 163.58/22.69 | | | | (270) all_1308_2 = all_1286_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (270) implies: % 163.58/22.69 | | | | (271) all_1308_2 = all_1286_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (246), (248) imply: % 163.58/22.69 | | | | (272) all_1286_1 = all_337_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (246), (247) imply: % 163.58/22.69 | | | | (273) all_1286_1 = all_1257_0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (243), (244) imply: % 163.58/22.69 | | | | (274) all_2100_7 = all_1284_2 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (274) implies: % 163.58/22.69 | | | | (275) all_2100_7 = all_1284_2 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (242), (275) imply: % 163.58/22.69 | | | | (276) all_1478_4 = all_1284_2 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (276) implies: % 163.58/22.69 | | | | (277) all_1478_4 = all_1284_2 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (265), (266) imply: % 163.58/22.69 | | | | (278) all_1948_3 = all_1320_0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (278) implies: % 163.58/22.69 | | | | (279) all_1948_3 = all_1320_0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (266), (267) imply: % 163.58/22.69 | | | | (280) all_1320_0 = all_1308_0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (255), (256) imply: % 163.58/22.69 | | | | (281) all_1948_9 = all_1119_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (281) implies: % 163.58/22.69 | | | | (282) all_1948_9 = all_1119_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (262), (263) imply: % 163.58/22.69 | | | | (283) all_1946_8 = all_1255_0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (283) implies: % 163.58/22.69 | | | | (284) all_1946_8 = all_1255_0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (259), (260) imply: % 163.58/22.69 | | | | (285) all_1296_1 = all_1280_2 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (259), (261) imply: % 163.58/22.69 | | | | (286) all_1296_1 = all_1230_2 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (258), (259) imply: % 163.58/22.69 | | | | (287) all_1946_8 = all_1296_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (287) implies: % 163.58/22.69 | | | | (288) all_1946_8 = all_1296_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (264), (279) imply: % 163.58/22.69 | | | | (289) all_1320_0 = all_233_0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (289) implies: % 163.58/22.69 | | | | (290) all_1320_0 = all_233_0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (254), (282) imply: % 163.58/22.69 | | | | (291) all_1320_2 = all_1119_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (291) implies: % 163.58/22.69 | | | | (292) all_1320_2 = all_1119_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (284), (288) imply: % 163.58/22.69 | | | | (293) all_1296_1 = all_1255_0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (293) implies: % 163.58/22.69 | | | | (294) all_1296_1 = all_1255_0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (241), (277) imply: % 163.58/22.69 | | | | (295) all_1386_4 = all_1284_2 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (295) implies: % 163.58/22.69 | | | | (296) all_1386_4 = all_1284_2 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (239), (269) imply: % 163.58/22.69 | | | | (297) all_1386_4 = all_1320_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (297) implies: % 163.58/22.69 | | | | (298) all_1386_4 = all_1320_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (240), (269) imply: % 163.58/22.69 | | | | (299) all_1320_1 = all_1308_2 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (296), (298) imply: % 163.58/22.69 | | | | (300) all_1320_1 = all_1284_2 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (300) implies: % 163.58/22.69 | | | | (301) all_1320_1 = all_1284_2 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (280), (290) imply: % 163.58/22.69 | | | | (302) all_1308_0 = all_233_0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (299), (301) imply: % 163.58/22.69 | | | | (303) all_1308_2 = all_1284_2 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (303) implies: % 163.58/22.69 | | | | (304) all_1308_2 = all_1284_2 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (253), (292) imply: % 163.58/22.69 | | | | (305) all_1308_1 = all_1119_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (305) implies: % 163.58/22.69 | | | | (306) all_1308_1 = all_1119_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (252), (306) imply: % 163.58/22.69 | | | | (307) all_1255_2 = all_1119_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (307) implies: % 163.58/22.69 | | | | (308) all_1255_2 = all_1119_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (271), (304) imply: % 163.58/22.69 | | | | (309) all_1286_1 = all_1284_2 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (309) implies: % 163.58/22.69 | | | | (310) all_1286_1 = all_1284_2 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (286), (294) imply: % 163.58/22.69 | | | | (311) all_1255_0 = all_1230_2 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (285), (294) imply: % 163.58/22.69 | | | | (312) all_1280_2 = all_1255_0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (312) implies: % 163.58/22.69 | | | | (313) all_1280_2 = all_1255_0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (272), (310) imply: % 163.58/22.69 | | | | (314) all_1284_2 = all_337_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (273), (310) imply: % 163.58/22.69 | | | | (315) all_1284_2 = all_1257_0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (314), (315) imply: % 163.58/22.69 | | | | (316) all_1257_0 = all_337_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (316) implies: % 163.58/22.69 | | | | (317) all_1257_0 = all_337_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (257), (313) imply: % 163.58/22.69 | | | | (318) all_1255_0 = all_1234_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (318) implies: % 163.58/22.69 | | | | (319) all_1255_0 = all_1234_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (238), (317) imply: % 163.58/22.69 | | | | (320) all_1255_1 = all_337_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (320) implies: % 163.58/22.69 | | | | (321) all_1255_1 = all_337_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (311), (319) imply: % 163.58/22.69 | | | | (322) all_1234_1 = all_1230_2 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (237), (321) imply: % 163.58/22.69 | | | | (323) all_1237_0 = all_337_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (323) implies: % 163.58/22.69 | | | | (324) all_1237_0 = all_337_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (251), (308) imply: % 163.58/22.69 | | | | (325) all_1119_1 = 0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (325) implies: % 163.58/22.69 | | | | (326) all_1119_1 = 0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (236), (324) imply: % 163.58/22.69 | | | | (327) all_1232_2 = all_337_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (327) implies: % 163.58/22.69 | | | | (328) all_1232_2 = all_337_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (235), (328) imply: % 163.58/22.69 | | | | (329) all_1211_0 = all_337_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (329) implies: % 163.58/22.69 | | | | (330) all_1211_0 = all_337_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (234), (330) imply: % 163.58/22.69 | | | | (331) all_339_0 = all_337_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | SIMP: (331) implies: % 163.58/22.69 | | | | (332) all_339_0 = all_337_1 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (233), (332) imply: % 163.58/22.69 | | | | (333) all_337_1 = 0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (321), (333) imply: % 163.58/22.69 | | | | (334) all_1255_1 = 0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (314), (333) imply: % 163.58/22.69 | | | | (335) all_1284_2 = 0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (304), (335) imply: % 163.58/22.69 | | | | (336) all_1308_2 = 0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | COMBINE_EQS: (306), (326) imply: % 163.58/22.69 | | | | (337) all_1308_1 = 0 % 163.58/22.69 | | | | % 163.58/22.69 | | | | BETA: splitting (182) gives: % 163.58/22.69 | | | | % 163.58/22.69 | | | | Case 1: % 163.58/22.69 | | | | | % 163.58/22.69 | | | | | (338) ~ (all_1255_1 = 0) % 163.58/22.69 | | | | | % 163.58/22.69 | | | | | REDUCE: (334), (338) imply: % 163.58/22.69 | | | | | (339) $false % 163.58/22.69 | | | | | % 163.58/22.69 | | | | | CLOSE: (339) is inconsistent. % 163.58/22.69 | | | | | % 163.58/22.69 | | | | Case 2: % 163.58/22.69 | | | | | % 163.58/22.69 | | | | | (340) ~ (all_1255_2 = 0) | all_1255_0 = 0 % 163.58/22.69 | | | | | % 163.58/22.69 | | | | | BETA: splitting (340) gives: % 163.58/22.69 | | | | | % 163.58/22.69 | | | | | Case 1: % 163.58/22.69 | | | | | | % 163.58/22.69 | | | | | | (341) ~ (all_1255_2 = 0) % 163.58/22.69 | | | | | | % 163.58/22.69 | | | | | | REDUCE: (251), (341) imply: % 163.58/22.69 | | | | | | (342) $false % 163.58/22.69 | | | | | | % 163.58/22.69 | | | | | | CLOSE: (342) is inconsistent. % 163.58/22.69 | | | | | | % 163.58/22.69 | | | | | Case 2: % 163.58/22.69 | | | | | | % 163.58/22.69 | | | | | | (343) all_1255_0 = 0 % 163.58/22.69 | | | | | | % 163.58/22.69 | | | | | | COMBINE_EQS: (311), (343) imply: % 163.58/22.69 | | | | | | (344) all_1230_2 = 0 % 163.58/22.69 | | | | | | % 163.58/22.69 | | | | | | COMBINE_EQS: (322), (344) imply: % 163.58/22.69 | | | | | | (345) all_1234_1 = 0 % 163.58/22.69 | | | | | | % 163.58/22.69 | | | | | | BETA: splitting (175) gives: % 163.58/22.69 | | | | | | % 163.58/22.69 | | | | | | Case 1: % 163.58/22.69 | | | | | | | % 163.58/22.69 | | | | | | | (346) ~ (all_1234_1 = 0) % 163.58/22.69 | | | | | | | % 163.58/22.69 | | | | | | | REDUCE: (345), (346) imply: % 163.58/22.69 | | | | | | | (347) $false % 163.58/22.69 | | | | | | | % 163.58/22.69 | | | | | | | CLOSE: (347) is inconsistent. % 163.58/22.69 | | | | | | | % 163.58/22.69 | | | | | | Case 2: % 163.58/22.69 | | | | | | | % 163.58/22.69 | | | | | | | (348) all_1234_0 = xb & all_41_3 = xb % 163.58/22.69 | | | | | | | % 163.58/22.69 | | | | | | | ALPHA: (348) implies: % 163.58/22.69 | | | | | | | (349) all_41_3 = xb % 163.58/22.69 | | | | | | | % 163.58/22.69 | | | | | | | BETA: splitting (197) gives: % 163.58/22.69 | | | | | | | % 163.58/22.69 | | | | | | | Case 1: % 163.58/22.69 | | | | | | | | % 163.58/22.69 | | | | | | | | (350) ~ (all_1308_1 = 0) % 163.58/22.69 | | | | | | | | % 163.58/22.69 | | | | | | | | REDUCE: (337), (350) imply: % 163.58/22.69 | | | | | | | | (351) $false % 163.58/22.69 | | | | | | | | % 163.58/22.69 | | | | | | | | CLOSE: (351) is inconsistent. % 163.58/22.69 | | | | | | | | % 163.58/22.69 | | | | | | | Case 2: % 163.58/22.69 | | | | | | | | % 163.58/22.69 | | | | | | | | (352) ~ (all_1308_2 = 0) | all_1308_0 = all_41_3 % 163.58/22.69 | | | | | | | | % 163.58/22.69 | | | | | | | | BETA: splitting (352) gives: % 163.58/22.69 | | | | | | | | % 163.58/22.69 | | | | | | | | Case 1: % 163.58/22.69 | | | | | | | | | % 163.58/22.69 | | | | | | | | | (353) ~ (all_1308_2 = 0) % 163.58/22.69 | | | | | | | | | % 163.58/22.69 | | | | | | | | | REDUCE: (336), (353) imply: % 163.58/22.69 | | | | | | | | | (354) $false % 163.58/22.69 | | | | | | | | | % 163.58/22.69 | | | | | | | | | CLOSE: (354) is inconsistent. % 163.58/22.69 | | | | | | | | | % 163.58/22.69 | | | | | | | | Case 2: % 163.58/22.69 | | | | | | | | | % 163.58/22.70 | | | | | | | | | (355) all_1308_0 = all_41_3 % 163.58/22.70 | | | | | | | | | % 163.58/22.70 | | | | | | | | | COMBINE_EQS: (302), (355) imply: % 163.58/22.70 | | | | | | | | | (356) all_233_0 = all_41_3 % 163.58/22.70 | | | | | | | | | % 163.58/22.70 | | | | | | | | | COMBINE_EQS: (349), (356) imply: % 163.58/22.70 | | | | | | | | | (357) all_233_0 = xb % 163.58/22.70 | | | | | | | | | % 163.58/22.70 | | | | | | | | | REDUCE: (159), (357) imply: % 163.58/22.70 | | | | | | | | | (358) $false % 163.58/22.70 | | | | | | | | | % 163.58/22.70 | | | | | | | | | CLOSE: (358) is inconsistent. % 163.58/22.70 | | | | | | | | | % 163.58/22.70 | | | | | | | | End of split % 163.58/22.70 | | | | | | | | % 163.58/22.70 | | | | | | | End of split % 163.58/22.70 | | | | | | | % 163.58/22.70 | | | | | | End of split % 163.58/22.70 | | | | | | % 163.58/22.70 | | | | | End of split % 163.58/22.70 | | | | | % 163.58/22.70 | | | | End of split % 163.58/22.70 | | | | % 163.58/22.70 | | | End of split % 163.58/22.70 | | | % 163.58/22.70 | | End of split % 163.58/22.70 | | % 163.58/22.70 | Case 2: % 163.58/22.70 | | % 163.58/22.70 | | (359) ~ (all_45_2 = 0) & ~ (all_45_3 = 0) & ! [v0: $i] : ( ~ % 163.58/22.70 | | (sdtasdt0(xu, v0) = xa) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) % 163.58/22.70 | | & aElement0(v0) = v1)) & ! [v0: $i] : ( ~ (aElement0(v0) = 0) % 163.58/22.70 | | | ~ $i(v0) | ? [v1: $i] : ( ~ (v1 = xa) & sdtasdt0(xu, v0) = v1 % 163.58/22.70 | | & $i(v1))) % 163.58/22.70 | | % 163.58/22.70 | | ALPHA: (359) implies: % 163.58/22.70 | | (360) ~ (all_45_3 = 0) % 163.58/22.70 | | % 163.58/22.70 | | REDUCE: (107), (360) imply: % 163.58/22.70 | | (361) $false % 163.58/22.70 | | % 163.58/22.70 | | CLOSE: (361) is inconsistent. % 163.58/22.70 | | % 163.58/22.70 | End of split % 163.58/22.70 | % 163.58/22.70 End of proof % 163.58/22.70 % SZS output end Proof for theBenchmark % 163.58/22.70 % 163.58/22.70 22103ms %------------------------------------------------------------------------------