%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : RNG119+1 : TPTP v8.1.2. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n020.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 17.33s 3.08s % Output : Proof 57.98s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : RNG119+1 : TPTP v8.1.2. Released v4.0.0. % 0.00/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.35 % Computer : n020.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Sun Aug 27 01:30:44 EDT 2023 % 0.14/0.35 % CPUTime : % 0.20/0.62 ________ _____ % 0.20/0.62 ___ __ \_________(_)________________________________ % 0.20/0.62 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.62 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.62 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.62 % 0.20/0.62 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.62 (2023-06-19) % 0.20/0.62 % 0.20/0.62 (c) Philipp Rümmer, 2009-2023 % 0.20/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.62 Amanda Stjerna. % 0.20/0.62 Free software under BSD-3-Clause. % 0.20/0.62 % 0.20/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.62 % 0.20/0.62 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.20/0.63 Running up to 7 provers in parallel. % 0.20/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.23/1.16 Prover 4: Preprocessing ... % 3.23/1.16 Prover 1: Preprocessing ... % 3.23/1.20 Prover 5: Preprocessing ... % 3.23/1.20 Prover 3: Preprocessing ... % 3.23/1.20 Prover 6: Preprocessing ... % 3.23/1.20 Prover 0: Preprocessing ... % 3.23/1.20 Prover 2: Preprocessing ... % 9.20/2.04 Prover 1: Constructing countermodel ... % 9.20/2.06 Prover 3: Constructing countermodel ... % 9.20/2.08 Prover 6: Proving ... % 9.20/2.10 Prover 5: Proving ... % 9.20/2.15 Prover 2: Proving ... % 10.56/2.19 Prover 4: Constructing countermodel ... % 12.05/2.39 Prover 0: Proving ... % 16.73/3.08 Prover 0: proved (2419ms) % 16.73/3.08 % 17.33/3.08 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.33/3.08 % 17.33/3.09 Prover 3: stopped % 17.33/3.09 Prover 2: stopped % 17.33/3.10 Prover 6: stopped % 17.33/3.11 Prover 5: stopped % 17.33/3.11 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 17.33/3.11 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 17.33/3.11 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 17.33/3.11 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 17.33/3.11 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 18.36/3.25 Prover 8: Preprocessing ... % 18.36/3.25 Prover 7: Preprocessing ... % 18.36/3.26 Prover 11: Preprocessing ... % 18.36/3.27 Prover 13: Preprocessing ... % 18.36/3.28 Prover 10: Preprocessing ... % 19.02/3.41 Prover 10: Constructing countermodel ... % 19.02/3.44 Prover 7: Constructing countermodel ... % 19.02/3.44 Prover 8: Warning: ignoring some quantifiers % 19.02/3.45 Prover 13: Warning: ignoring some quantifiers % 19.02/3.45 Prover 8: Constructing countermodel ... % 19.02/3.46 Prover 13: Constructing countermodel ... % 21.39/3.69 Prover 11: Constructing countermodel ... % 56.15/8.26 Prover 4: Found proof (size 321) % 56.15/8.26 Prover 4: proved (7621ms) % 56.83/8.27 Prover 1: stopped % 56.83/8.27 Prover 8: stopped % 56.83/8.27 Prover 11: stopped % 56.83/8.27 Prover 7: stopped % 56.83/8.28 Prover 13: stopped % 56.91/8.29 Prover 10: stopped % 56.91/8.29 % 56.91/8.29 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.91/8.29 % 56.91/8.35 % SZS output start Proof for theBenchmark % 56.91/8.35 Assumptions after simplification: % 56.91/8.35 --------------------------------- % 56.91/8.35 % 56.91/8.35 (mAMDistr) % 56.91/8.40 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 56.91/8.40 $i] : ( ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v1, v0) = v3) | ~ % 56.91/8.40 (sdtpldt0(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : % 56.91/8.40 ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? % 56.91/8.40 [v12: $i] : ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v9, v0) = v14 & % 56.91/8.40 sdtasdt0(v0, v9) = v10 & sdtasdt0(v0, v2) = v12 & sdtasdt0(v0, v1) = v11 & % 56.91/8.40 sdtpldt0(v11, v12) = v13 & sdtpldt0(v1, v2) = v9 & aElement0(v2) = v8 & % 56.91/8.40 aElement0(v1) = v7 & aElement0(v0) = v6 & $i(v14) & $i(v13) & $i(v12) & % 56.91/8.40 $i(v11) & $i(v10) & $i(v9) & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | % 56.91/8.40 (v14 = v5 & v13 = v10)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 56.91/8.40 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ % 56.91/8.40 (sdtasdt0(v0, v1) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) % 56.91/8.40 | ~ $i(v0) | ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? % 56.91/8.40 [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : % 56.91/8.40 (sdtasdt0(v9, v0) = v11 & sdtasdt0(v2, v0) = v13 & sdtasdt0(v1, v0) = v12 & % 56.91/8.40 sdtasdt0(v0, v9) = v10 & sdtpldt0(v12, v13) = v14 & sdtpldt0(v1, v2) = v9 % 56.91/8.40 & aElement0(v2) = v8 & aElement0(v1) = v7 & aElement0(v0) = v6 & $i(v14) & % 56.91/8.40 $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) & ( ~ (v8 = 0) | ~ (v7 = % 56.91/8.40 0) | ~ (v6 = 0) | (v14 = v11 & v10 = v5)))) & ! [v0: $i] : ! [v1: % 56.91/8.40 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (sdtasdt0(v3, v0) = v4) % 56.91/8.40 | ~ (sdtpldt0(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: % 56.91/8.40 any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? [v9: $i] : ? [v10: % 56.91/8.40 $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : % 56.91/8.40 (sdtasdt0(v2, v0) = v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v3) = v8 & % 56.91/8.40 sdtasdt0(v0, v2) = v10 & sdtasdt0(v0, v1) = v9 & sdtpldt0(v12, v13) = v14 % 56.91/8.40 & sdtpldt0(v9, v10) = v11 & aElement0(v2) = v7 & aElement0(v1) = v6 & % 56.91/8.40 aElement0(v0) = v5 & $i(v14) & $i(v13) & $i(v12) & $i(v11) & $i(v10) & % 56.91/8.40 $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | (v14 = v4 & % 56.91/8.40 v11 = v8)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 56.91/8.40 ! [v4: $i] : ( ~ (sdtasdt0(v0, v3) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ % 56.91/8.40 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] % 56.91/8.40 : ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : % 56.91/8.40 ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v3, v0) = v11 & sdtasdt0(v2, v0) = % 56.91/8.40 v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v2) = v9 & sdtasdt0(v0, v1) = % 56.91/8.40 v8 & sdtpldt0(v12, v13) = v14 & sdtpldt0(v8, v9) = v10 & aElement0(v2) = % 56.91/8.40 v7 & aElement0(v1) = v6 & aElement0(v0) = v5 & $i(v14) & $i(v13) & $i(v12) % 56.91/8.40 & $i(v11) & $i(v10) & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ % 56.91/8.40 (v5 = 0) | (v14 = v11 & v10 = v4)))) % 56.91/8.40 % 56.91/8.40 (mAddComm) % 56.91/8.40 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ % 56.91/8.40 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 56.91/8.40 (sdtpldt0(v0, v1) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & $i(v5) & % 56.91/8.40 ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) & ! [v0: $i] : ! [v1: $i] : ! % 56.91/8.40 [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] % 56.91/8.40 : ? [v4: any] : ? [v5: $i] : (sdtpldt0(v1, v0) = v5 & aElement0(v1) = v4 & % 56.91/8.40 aElement0(v0) = v3 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 56.91/8.40 % 56.91/8.40 (mAddZero) % 56.91/8.40 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtpldt0(v0, sz00) = v1) | ~ % 56.91/8.40 $i(v0) | ? [v2: any] : ? [v3: $i] : (sdtpldt0(sz00, v0) = v3 & % 56.91/8.40 aElement0(v0) = v2 & $i(v3) & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) & ! % 56.91/8.40 [v0: $i] : ! [v1: $i] : ( ~ (sdtpldt0(sz00, v0) = v1) | ~ $i(v0) | ? [v2: % 56.91/8.40 any] : ? [v3: $i] : (sdtpldt0(v0, sz00) = v3 & aElement0(v0) = v2 & % 56.91/8.40 $i(v3) & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) & ! [v0: $i] : ( ~ % 56.91/8.40 (aElement0(v0) = 0) | ~ $i(v0) | (sdtpldt0(v0, sz00) = v0 & sdtpldt0(sz00, % 56.91/8.40 v0) = v0)) % 56.91/8.40 % 56.91/8.40 (mDefDiv) % 56.91/8.41 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : ! [v3: $i] : (v2 = 0 | ~ % 56.91/8.41 (doDivides0(v0, v1) = v2) | ~ (sdtasdt0(v0, v3) = v1) | ~ $i(v3) | ~ % 56.91/8.41 $i(v1) | ~ $i(v0) | ? [v4: int] : ? [v5: any] : (( ~ (v4 = 0) & % 56.91/8.41 aElement0(v3) = v4) | (aElement0(v1) = v5 & aElement0(v0) = v4 & ( ~ (v5 % 56.91/8.41 = 0) | ~ (v4 = 0))))) & ! [v0: $i] : ! [v1: $i] : ! [v2: int] : % 56.91/8.41 ! [v3: $i] : (v2 = 0 | ~ (doDivides0(v0, v1) = v2) | ~ (aElement0(v3) = 0) | % 56.91/8.41 ~ $i(v3) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : (( ~ (v4 = % 56.91/8.41 v1) & sdtasdt0(v0, v3) = v4 & $i(v4)) | (aElement0(v1) = v5 & % 56.91/8.41 aElement0(v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0))))) & ! [v0: $i] : ! % 56.91/8.41 [v1: $i] : ( ~ (doDivides0(v0, v1) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: any] % 56.91/8.41 : ? [v3: any] : ? [v4: $i] : ? [v5: int] : ? [v6: $i] : ($i(v4) & ((v6 = % 56.91/8.41 v1 & v5 = 0 & sdtasdt0(v0, v4) = v1 & aElement0(v4) = 0) | % 56.91/8.41 (aElement0(v1) = v3 & aElement0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = % 56.91/8.41 0)))))) % 56.91/8.41 % 56.91/8.41 (mDefDvs) % 56.91/8.41 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (aDivisorOf0(v1, v0) = % 56.91/8.41 v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? % 56.91/8.41 [v4: any] : (doDivides0(v1, v0) = v4 & aElement0(v1) = v3 & ( ~ (v4 = 0) | % 56.91/8.41 ~ (v3 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ % 56.91/8.41 (doDivides0(v1, v0) = v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | % 56.91/8.41 ? [v3: any] : ? [v4: any] : (aDivisorOf0(v1, v0) = v3 & aElement0(v1) = v4 % 56.91/8.41 & ( ~ (v3 = 0) | (v4 = 0 & v2 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! % 56.91/8.41 [v2: any] : ( ~ (aElement0(v1) = v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ % 56.91/8.41 $i(v0) | ? [v3: any] : ? [v4: any] : (aDivisorOf0(v1, v0) = v3 & % 56.91/8.41 doDivides0(v1, v0) = v4 & ( ~ (v3 = 0) | (v4 = 0 & v2 = 0)))) & ! [v0: % 56.91/8.41 $i] : ! [v1: $i] : ( ~ (aDivisorOf0(v1, v0) = 0) | ~ (aElement0(v0) = 0) | % 56.91/8.41 ~ $i(v1) | ~ $i(v0) | (doDivides0(v1, v0) = 0 & aElement0(v1) = 0)) & ! % 56.91/8.41 [v0: $i] : ! [v1: $i] : ( ~ (doDivides0(v1, v0) = 0) | ~ (aElement0(v0) = 0) % 56.91/8.41 | ~ $i(v1) | ~ $i(v0) | ? [v2: any] : ? [v3: any] : (aDivisorOf0(v1, v0) % 56.91/8.41 = v3 & aElement0(v1) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0: $i] : ! % 56.91/8.41 [v1: $i] : ( ~ (aElement0(v1) = 0) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ % 56.91/8.41 $i(v0) | ? [v2: any] : ? [v3: any] : (aDivisorOf0(v1, v0) = v3 & % 56.91/8.41 doDivides0(v1, v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 56.91/8.41 % 56.91/8.41 (mDefIdeal) % 57.32/8.42 ! [v0: $i] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 57.32/8.42 $i] : ( ~ (aSet0(v0) = v1) | ~ (aElementOf0(v2, v0) = 0) | ~ (sdtasdt0(v3, % 57.32/8.42 v2) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v0) | ? [v5: int] : ? [v6: % 57.32/8.42 any] : (( ~ (v5 = 0) & aIdeal0(v0) = v5) | (aElementOf0(v4, v0) = v6 & % 57.32/8.42 aElement0(v3) = v5 & ( ~ (v5 = 0) | v6 = 0)))) & ! [v0: $i] : ! [v1: % 57.32/8.42 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 57.32/8.42 (aSet0(v0) = v1) | ~ (aElementOf0(v2, v0) = 0) | ~ (sdtpldt0(v2, v3) = v4) % 57.32/8.42 | ~ $i(v3) | ~ $i(v2) | ~ $i(v0) | ? [v5: int] : ? [v6: any] : (( ~ (v5 % 57.32/8.42 = 0) & aIdeal0(v0) = v5) | (aElementOf0(v4, v0) = v6 & aElementOf0(v3, % 57.32/8.42 v0) = v5 & ( ~ (v5 = 0) | v6 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! % 57.32/8.42 [v2: $i] : ! [v3: $i] : ( ~ (aIdeal0(v0) = 0) | ~ (aElementOf0(v1, v0) = 0) % 57.32/8.42 | ~ (sdtasdt0(v2, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 57.32/8.42 any] : ? [v5: any] : (aElementOf0(v3, v0) = v5 & aElement0(v2) = v4 & ( ~ % 57.32/8.42 (v4 = 0) | v5 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 57.32/8.42 $i] : ( ~ (aIdeal0(v0) = 0) | ~ (aElementOf0(v1, v0) = 0) | ~ % 57.32/8.42 (sdtpldt0(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : % 57.32/8.42 ? [v5: any] : (aElementOf0(v3, v0) = v5 & aElementOf0(v2, v0) = v4 & ( ~ % 57.32/8.42 (v4 = 0) | v5 = 0))) & ! [v0: $i] : ! [v1: MultipleValueBool] : ! % 57.32/8.42 [v2: $i] : ! [v3: $i] : ( ~ (aSet0(v0) = v1) | ~ (aElementOf0(v3, v0) = 0) | % 57.32/8.42 ~ (aElementOf0(v2, v0) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v0) | ? [v4: % 57.32/8.42 any] : ? [v5: int] : ((v5 = 0 & aElementOf0(v4, v0) = 0 & sdtpldt0(v2, % 57.32/8.42 v3) = v4 & $i(v4)) | ( ~ (v4 = 0) & aIdeal0(v0) = v4))) & ! [v0: $i] % 57.32/8.42 : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ( ~ (aSet0(v0) = % 57.32/8.42 v1) | ~ (aElementOf0(v2, v0) = 0) | ~ (aElement0(v3) = 0) | ~ $i(v3) | % 57.32/8.42 ~ $i(v2) | ~ $i(v0) | ? [v4: any] : ? [v5: int] : ((v5 = 0 & % 57.32/8.42 aElementOf0(v4, v0) = 0 & sdtasdt0(v3, v2) = v4 & $i(v4)) | ( ~ (v4 = 0) % 57.32/8.42 & aIdeal0(v0) = v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 57.32/8.42 (aIdeal0(v0) = 0) | ~ (aElementOf0(v2, v0) = 0) | ~ (aElementOf0(v1, v0) = % 57.32/8.42 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : (aElementOf0(v3, % 57.32/8.42 v0) = 0 & sdtpldt0(v1, v2) = v3 & $i(v3))) & ! [v0: $i] : ! [v1: $i] : % 57.32/8.42 ! [v2: $i] : ( ~ (aIdeal0(v0) = 0) | ~ (aElementOf0(v1, v0) = 0) | ~ % 57.32/8.42 (aElement0(v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : % 57.32/8.42 (aElementOf0(v3, v0) = 0 & sdtasdt0(v2, v1) = v3 & $i(v3))) & ! [v0: $i] : % 57.32/8.42 ! [v1: int] : (v1 = 0 | ~ (aIdeal0(v0) = v1) | ~ $i(v0) | ? [v2: int] : ? % 57.32/8.42 [v3: $i] : ? [v4: int] : ? [v5: $i] : ? [v6: int] : ? [v7: $i] : ? [v8: % 57.32/8.42 int] : ? [v9: $i] : ? [v10: int] : ? [v11: $i] : ? [v12: int] : % 57.32/8.42 ($i(v9) & $i(v5) & $i(v3) & ((v4 = 0 & aElementOf0(v3, v0) = 0 & ((v10 = 0 & % 57.32/8.42 ~ (v12 = 0) & aElementOf0(v11, v0) = v12 & aElementOf0(v9, v0) = % 57.32/8.42 0 & sdtpldt0(v3, v9) = v11 & $i(v11)) | (v6 = 0 & ~ (v8 = 0) & % 57.32/8.42 aElementOf0(v7, v0) = v8 & sdtasdt0(v5, v3) = v7 & aElement0(v5) = % 57.32/8.42 0 & $i(v7)))) | ( ~ (v2 = 0) & aSet0(v0) = v2)))) & ! [v0: $i] : % 57.32/8.42 ! [v1: int] : (v1 = 0 | ~ (aSet0(v0) = v1) | ~ $i(v0) | ? [v2: int] : ( ~ % 57.32/8.42 (v2 = 0) & aIdeal0(v0) = v2)) & ! [v0: $i] : ( ~ (aIdeal0(v0) = 0) | ~ % 57.32/8.42 $i(v0) | aSet0(v0) = 0) & ! [v0: $i] : ( ~ (aSet0(v0) = 0) | ~ $i(v0) | ? % 57.32/8.42 [v1: int] : ? [v2: $i] : ? [v3: int] : ? [v4: $i] : ? [v5: int] : ? % 57.32/8.42 [v6: $i] : ? [v7: int] : ? [v8: $i] : ? [v9: int] : ? [v10: $i] : ? % 57.32/8.42 [v11: int] : ($i(v8) & $i(v4) & $i(v2) & ((v3 = 0 & aElementOf0(v2, v0) = 0 % 57.32/8.42 & ((v9 = 0 & ~ (v11 = 0) & aElementOf0(v10, v0) = v11 & % 57.32/8.42 aElementOf0(v8, v0) = 0 & sdtpldt0(v2, v8) = v10 & $i(v10)) | (v5 % 57.32/8.42 = 0 & ~ (v7 = 0) & aElementOf0(v6, v0) = v7 & sdtasdt0(v4, v2) = % 57.32/8.42 v6 & aElement0(v4) = 0 & $i(v6)))) | (v1 = 0 & aIdeal0(v0) = 0)))) % 57.32/8.42 % 57.32/8.42 (mDefRel) % 57.32/8.43 $i(sz10) & ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ % 57.32/8.43 (misRelativelyPrime0(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : % 57.32/8.43 ? [v4: any] : ? [v5: any] : (aGcdOfAnd0(sz10, v0, v1) = v5 & aElement0(v1) % 57.32/8.43 = v4 & aElement0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | (( ~ (v5 = 0) | % 57.32/8.43 v2 = 0) & ( ~ (v2 = 0) | v5 = 0))))) & ! [v0: $i] : ! [v1: $i] : % 57.32/8.43 ! [v2: any] : ( ~ (aGcdOfAnd0(sz10, v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? % 57.32/8.43 [v3: any] : ? [v4: any] : ? [v5: any] : (misRelativelyPrime0(v0, v1) = v5 % 57.32/8.43 & aElement0(v1) = v4 & aElement0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | % 57.32/8.43 (( ~ (v5 = 0) | v2 = 0) & ( ~ (v2 = 0) | v5 = 0))))) % 57.32/8.43 % 57.32/8.43 (mDivision) % 57.32/8.43 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = sz00 | ~ % 57.32/8.43 (sbrdtbr0(v1) = v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | ? % 57.32/8.43 [v3: int] : ? [v4: $i] : ? [v5: $i] : ? [v6: int] : ? [v7: int] : ? % 57.32/8.43 [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: any] : ($i(v5) & $i(v4) & % 57.32/8.43 ((v9 = v0 & v7 = 0 & v6 = 0 & iLess0(v10, v2) = v11 & sbrdtbr0(v5) = v10 & % 57.32/8.43 sdtasdt0(v4, v1) = v8 & sdtpldt0(v8, v5) = v0 & aElement0(v5) = 0 & % 57.32/8.43 aElement0(v4) = 0 & $i(v10) & $i(v8) & (v11 = 0 | v5 = sz00)) | ( ~ % 57.32/8.43 (v3 = 0) & aElement0(v1) = v3)))) & ! [v0: $i] : ! [v1: $i] : (v1 = % 57.32/8.43 sz00 | ~ (aElement0(v1) = 0) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ % 57.58/8.43 $i(v0) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] % 57.58/8.43 : ? [v7: any] : (iLess0(v6, v2) = v7 & sbrdtbr0(v4) = v6 & sbrdtbr0(v1) = % 57.58/8.43 v2 & sdtasdt0(v3, v1) = v5 & sdtpldt0(v5, v4) = v0 & aElement0(v4) = 0 & % 57.58/8.43 aElement0(v3) = 0 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & (v7 = 0 | % 57.58/8.43 v4 = sz00))) % 57.58/8.43 % 57.58/8.43 (mEucSort) % 57.58/8.43 $i(sz00) & ! [v0: $i] : ! [v1: $i] : (v0 = sz00 | ~ (sbrdtbr0(v0) = v1) | % 57.58/8.43 ~ $i(v0) | ? [v2: any] : ? [v3: any] : (aNaturalNumber0(v1) = v3 & % 57.58/8.43 aElement0(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0: $i] : (v0 = sz00 | % 57.58/8.43 ~ (aElement0(v0) = 0) | ~ $i(v0) | ? [v1: $i] : (sbrdtbr0(v0) = v1 & % 57.58/8.43 aNaturalNumber0(v1) = 0 & $i(v1))) % 57.58/8.43 % 57.58/8.43 (mMulComm) % 57.58/8.43 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v1, v0) = v2) | ~ % 57.58/8.43 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 57.58/8.43 (sdtasdt0(v0, v1) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & $i(v5) & % 57.58/8.43 ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) & ! [v0: $i] : ! [v1: $i] : ! % 57.58/8.43 [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] % 57.58/8.43 : ? [v4: any] : ? [v5: $i] : (sdtasdt0(v1, v0) = v5 & aElement0(v1) = v4 & % 57.58/8.43 aElement0(v0) = v3 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 57.58/8.43 % 57.58/8.43 (mPrIdeal) % 57.58/8.43 ! [v0: $i] : ! [v1: $i] : ( ~ (slsdtgt0(v0) = v1) | ~ $i(v0) | ? [v2: any] % 57.58/8.43 : ? [v3: any] : (aIdeal0(v1) = v3 & aElement0(v0) = v2 & ( ~ (v2 = 0) | v3 % 57.58/8.43 = 0))) & ! [v0: $i] : ( ~ (aElement0(v0) = 0) | ~ $i(v0) | ? [v1: $i] % 57.58/8.43 : (slsdtgt0(v0) = v1 & aIdeal0(v1) = 0 & $i(v1))) % 57.58/8.43 % 57.58/8.43 (mSortsB) % 57.58/8.43 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 57.58/8.43 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 57.58/8.43 (aElement0(v2) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & ( ~ (v4 = 0) % 57.58/8.43 | ~ (v3 = 0) | v5 = 0))) % 57.58/8.43 % 57.58/8.43 (mSortsB_02) % 57.58/8.44 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 57.58/8.44 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 57.58/8.44 (aElement0(v2) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & ( ~ (v4 = 0) % 57.58/8.44 | ~ (v3 = 0) | v5 = 0))) % 57.58/8.44 % 57.58/8.44 (mSortsC_01) % 57.58/8.44 aElement0(sz10) = 0 & $i(sz10) % 57.58/8.44 % 57.58/8.44 (mUnNeZr) % 57.58/8.44 ~ (sz10 = sz00) & $i(sz10) & $i(sz00) % 57.58/8.44 % 57.58/8.44 (m__) % 57.58/8.44 xr = sz00 & $i(sz00) % 57.58/8.44 % 57.58/8.44 (m__2091) % 57.58/8.44 aElement0(xb) = 0 & aElement0(xa) = 0 & $i(xb) & $i(xa) % 57.58/8.44 % 57.58/8.44 (m__2174) % 57.58/8.44 $i(xI) & $i(xb) & $i(xa) & ? [v0: $i] : ? [v1: $i] : (slsdtgt0(xb) = v1 & % 57.58/8.44 slsdtgt0(xa) = v0 & aIdeal0(xI) = 0 & sdtpldt1(v0, v1) = xI & $i(v1) & % 57.58/8.44 $i(v0)) % 57.58/8.44 % 57.58/8.44 (m__2203) % 57.58/8.44 $i(xb) & $i(xa) & $i(sz00) & ? [v0: $i] : ? [v1: $i] : (slsdtgt0(xb) = v1 & % 57.58/8.44 slsdtgt0(xa) = v0 & aElementOf0(xb, v1) = 0 & aElementOf0(xa, v0) = 0 & % 57.58/8.44 aElementOf0(sz00, v1) = 0 & aElementOf0(sz00, v0) = 0 & $i(v1) & $i(v0)) % 57.58/8.44 % 57.58/8.44 (m__2228) % 57.58/8.44 $i(xb) & $i(xa) & $i(sz00) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 57.58/8.44 $i] : ( ~ (v3 = sz00) & slsdtgt0(xb) = v1 & slsdtgt0(xa) = v0 & sdtpldt1(v0, % 57.58/8.44 v1) = v2 & aElementOf0(v3, v2) = 0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 57.58/8.44 % 57.58/8.44 (m__2273) % 57.58/8.44 $i(xu) & $i(xI) & $i(sz00) & ? [v0: $i] : ( ~ (xu = sz00) & sbrdtbr0(xu) = v0 % 57.58/8.44 & aElementOf0(xu, xI) = 0 & $i(v0) & ! [v1: $i] : ! [v2: $i] : (v1 = sz00 % 57.58/8.44 | ~ (sbrdtbr0(v1) = v2) | ~ $i(v1) | ? [v3: any] : ? [v4: any] : % 57.58/8.44 (iLess0(v2, v0) = v4 & aElementOf0(v1, xI) = v3 & ( ~ (v4 = 0) | ~ (v3 = % 57.58/8.44 0)))) & ! [v1: $i] : (v1 = sz00 | ~ (aElementOf0(v1, xI) = 0) | ~ % 57.58/8.44 $i(v1) | ? [v2: $i] : ? [v3: int] : ( ~ (v3 = 0) & iLess0(v2, v0) = v3 & % 57.58/8.44 sbrdtbr0(v1) = v2 & $i(v2)))) % 57.58/8.44 % 57.58/8.44 (m__2416) % 57.58/8.44 $i(xu) & $i(xb) & $i(xa) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 57.58/8.44 $i] : (sdtasdt0(xb, v1) = v3 & sdtasdt0(xa, v0) = v2 & sdtpldt0(v2, v3) = xu % 57.58/8.44 & aElement0(v1) = 0 & aElement0(v0) = 0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 57.58/8.44 % 57.58/8.44 (m__2479) % 57.58/8.44 doDivides0(xu, xa) = 0 & $i(xu) & $i(xa) % 57.58/8.44 % 57.58/8.44 (m__2612) % 57.58/8.44 $i(xu) & $i(xb) & ? [v0: int] : ( ~ (v0 = 0) & doDivides0(xu, xb) = v0) % 57.58/8.44 % 57.58/8.44 (m__2666) % 57.58/8.45 $i(xr) & $i(xq) & $i(xu) & $i(xb) & $i(sz00) & ? [v0: $i] : ? [v1: $i] : ? % 57.58/8.45 [v2: $i] : ? [v3: any] : (iLess0(v1, v2) = v3 & sbrdtbr0(xr) = v1 & % 57.58/8.45 sbrdtbr0(xu) = v2 & sdtasdt0(xq, xu) = v0 & sdtpldt0(v0, xr) = xb & % 57.58/8.45 aElement0(xr) = 0 & aElement0(xq) = 0 & $i(v2) & $i(v1) & $i(v0) & (v3 = 0 | % 57.58/8.45 xr = sz00)) % 57.58/8.45 % 57.58/8.45 (function-axioms) % 57.58/8.45 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 57.58/8.45 [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (aGcdOfAnd0(v4, v3, v2) = v1) | ~ % 57.58/8.45 (aGcdOfAnd0(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 57.58/8.45 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 57.58/8.45 (sdteqdtlpzmzozddtrp0(v4, v3, v2) = v1) | ~ (sdteqdtlpzmzozddtrp0(v4, v3, % 57.58/8.45 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 57.58/8.45 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (misRelativelyPrime0(v3, v2) = v1) | % 57.58/8.45 ~ (misRelativelyPrime0(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 57.58/8.45 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 57.58/8.45 (aDivisorOf0(v3, v2) = v1) | ~ (aDivisorOf0(v3, v2) = v0)) & ! [v0: % 57.58/8.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 57.58/8.45 : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ (doDivides0(v3, v2) = v0)) & ! % 57.58/8.45 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 57.58/8.45 $i] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) & ! % 57.58/8.45 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 57.58/8.45 (sdtasasdt0(v3, v2) = v1) | ~ (sdtasasdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 57.58/8.45 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtpldt1(v3, v2) = v1) | % 57.58/8.45 ~ (sdtpldt1(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 57.58/8.45 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 57.58/8.45 (aElementOf0(v3, v2) = v1) | ~ (aElementOf0(v3, v2) = v0)) & ! [v0: $i] : % 57.58/8.45 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) % 57.58/8.45 | ~ (sdtasdt0(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 57.58/8.45 [v3: $i] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 57.58/8.45 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (slsdtgt0(v2) = v1) % 57.58/8.45 | ~ (slsdtgt0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = % 57.58/8.45 v0 | ~ (sbrdtbr0(v2) = v1) | ~ (sbrdtbr0(v2) = v0)) & ! [v0: % 57.58/8.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 57.58/8.45 ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = v0)) & ! [v0: % 57.58/8.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 57.58/8.45 ~ (aIdeal0(v2) = v1) | ~ (aIdeal0(v2) = v0)) & ! [v0: MultipleValueBool] : % 57.58/8.45 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aSet0(v2) = v1) | ~ % 57.58/8.45 (aSet0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 57.58/8.45 (smndt0(v2) = v1) | ~ (smndt0(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 57.58/8.45 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aElement0(v2) = v1) | % 57.58/8.45 ~ (aElement0(v2) = v0)) % 57.58/8.45 % 57.58/8.45 Further assumptions not needed in the proof: % 57.58/8.45 -------------------------------------------- % 57.58/8.45 mAddAsso, mAddInvr, mCancel, mChineseRemainder, mDefGCD, mDefMod, mDefPrIdeal, % 57.58/8.45 mDefSInt, mDefSSum, mEOfElem, mElmSort, mIdeInt, mIdeSum, mMulAsso, mMulMnOne, % 57.58/8.45 mMulUnit, mMulZero, mNatLess, mNatSort, mSetEq, mSetSort, mSortsC, mSortsU, % 57.58/8.45 m__2110, m__2129, m__2383 % 57.58/8.45 % 57.58/8.45 Those formulas are unsatisfiable: % 57.58/8.45 --------------------------------- % 57.58/8.45 % 57.58/8.45 Begin of proof % 57.58/8.45 | % 57.58/8.45 | ALPHA: (mSortsC_01) implies: % 57.58/8.45 | (1) aElement0(sz10) = 0 % 57.58/8.45 | % 57.58/8.45 | ALPHA: (mAddComm) implies: % 57.58/8.46 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | % 57.58/8.46 | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 57.58/8.46 | (sdtpldt0(v1, v0) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & % 57.58/8.46 | $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 57.58/8.46 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v1, v0) = v2) | % 57.58/8.46 | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 57.58/8.46 | (sdtpldt0(v0, v1) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & % 57.58/8.46 | $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 57.58/8.46 | % 57.58/8.46 | ALPHA: (mAddZero) implies: % 57.58/8.46 | (4) ! [v0: $i] : ! [v1: $i] : ( ~ (sdtpldt0(v0, sz00) = v1) | ~ $i(v0) | % 57.58/8.46 | ? [v2: any] : ? [v3: $i] : (sdtpldt0(sz00, v0) = v3 & aElement0(v0) % 57.58/8.46 | = v2 & $i(v3) & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) % 57.58/8.46 | % 57.58/8.46 | ALPHA: (mMulComm) implies: % 57.58/8.46 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | % 57.58/8.46 | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 57.58/8.46 | (sdtasdt0(v1, v0) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & % 57.58/8.46 | $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 57.58/8.46 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v1, v0) = v2) | % 57.58/8.46 | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 57.58/8.46 | (sdtasdt0(v0, v1) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & % 57.58/8.46 | $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 57.58/8.46 | % 57.58/8.46 | ALPHA: (mAMDistr) implies: % 57.58/8.46 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 57.58/8.46 | ~ (sdtasdt0(v0, v3) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ $i(v2) | % 57.58/8.46 | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : % 57.58/8.46 | ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] % 57.58/8.46 | : ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v3, v0) = v11 & % 57.58/8.46 | sdtasdt0(v2, v0) = v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v2) % 57.58/8.46 | = v9 & sdtasdt0(v0, v1) = v8 & sdtpldt0(v12, v13) = v14 & % 57.58/8.46 | sdtpldt0(v8, v9) = v10 & aElement0(v2) = v7 & aElement0(v1) = v6 & % 57.58/8.46 | aElement0(v0) = v5 & $i(v14) & $i(v13) & $i(v12) & $i(v11) & % 57.58/8.46 | $i(v10) & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = % 57.58/8.46 | 0) | (v14 = v11 & v10 = v4)))) % 57.58/8.46 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 57.58/8.46 | ~ (sdtasdt0(v3, v0) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ $i(v2) | % 57.58/8.46 | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : % 57.58/8.46 | ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] % 57.58/8.46 | : ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v2, v0) = v13 & % 57.58/8.46 | sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v3) = v8 & sdtasdt0(v0, v2) = % 57.58/8.46 | v10 & sdtasdt0(v0, v1) = v9 & sdtpldt0(v12, v13) = v14 & % 57.58/8.46 | sdtpldt0(v9, v10) = v11 & aElement0(v2) = v7 & aElement0(v1) = v6 & % 57.58/8.46 | aElement0(v0) = v5 & $i(v14) & $i(v13) & $i(v12) & $i(v11) & % 57.58/8.46 | $i(v10) & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = % 57.58/8.46 | 0) | (v14 = v4 & v11 = v8)))) % 57.58/8.46 | % 57.58/8.46 | ALPHA: (mUnNeZr) implies: % 57.58/8.46 | (9) ~ (sz10 = sz00) % 57.58/8.46 | % 57.58/8.46 | ALPHA: (mDefIdeal) implies: % 57.58/8.46 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 57.58/8.46 | (aIdeal0(v0) = 0) | ~ (aElementOf0(v1, v0) = 0) | ~ (sdtasdt0(v2, % 57.58/8.46 | v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : % 57.58/8.46 | ? [v5: any] : (aElementOf0(v3, v0) = v5 & aElement0(v2) = v4 & ( ~ % 57.58/8.46 | (v4 = 0) | v5 = 0))) % 57.58/8.46 | % 57.58/8.46 | ALPHA: (mEucSort) implies: % 57.58/8.46 | (11) ! [v0: $i] : ! [v1: $i] : (v0 = sz00 | ~ (sbrdtbr0(v0) = v1) | ~ % 57.58/8.46 | $i(v0) | ? [v2: any] : ? [v3: any] : (aNaturalNumber0(v1) = v3 & % 57.58/8.46 | aElement0(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 57.58/8.46 | % 57.58/8.46 | ALPHA: (mDivision) implies: % 57.58/8.47 | (12) ! [v0: $i] : ! [v1: $i] : (v1 = sz00 | ~ (aElement0(v1) = 0) | ~ % 57.58/8.47 | (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: $i] : ? [v3: % 57.58/8.47 | $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: any] : % 57.58/8.47 | (iLess0(v6, v2) = v7 & sbrdtbr0(v4) = v6 & sbrdtbr0(v1) = v2 & % 57.58/8.47 | sdtasdt0(v3, v1) = v5 & sdtpldt0(v5, v4) = v0 & aElement0(v4) = 0 % 57.58/8.47 | & aElement0(v3) = 0 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & % 57.58/8.47 | (v7 = 0 | v4 = sz00))) % 57.58/8.47 | % 57.58/8.47 | ALPHA: (mDefDiv) implies: % 57.58/8.47 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: int] : ! [v3: $i] : (v2 = 0 | ~ % 57.58/8.47 | (doDivides0(v0, v1) = v2) | ~ (aElement0(v3) = 0) | ~ $i(v3) | ~ % 57.58/8.47 | $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : (( ~ (v4 = v1) & % 57.58/8.47 | sdtasdt0(v0, v3) = v4 & $i(v4)) | (aElement0(v1) = v5 & % 57.58/8.47 | aElement0(v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0))))) % 57.58/8.47 | % 57.58/8.47 | ALPHA: (mDefDvs) implies: % 57.58/8.47 | (14) ! [v0: $i] : ! [v1: $i] : ( ~ (doDivides0(v1, v0) = 0) | ~ % 57.58/8.47 | (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: any] : ? [v3: % 57.58/8.47 | any] : (aDivisorOf0(v1, v0) = v3 & aElement0(v1) = v2 & ( ~ (v2 = % 57.58/8.47 | 0) | v3 = 0))) % 57.58/8.47 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (doDivides0(v1, v0) = % 57.58/8.47 | v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v3: % 57.58/8.47 | any] : ? [v4: any] : (aDivisorOf0(v1, v0) = v3 & aElement0(v1) = % 57.58/8.47 | v4 & ( ~ (v3 = 0) | (v4 = 0 & v2 = 0)))) % 57.58/8.47 | % 57.58/8.47 | ALPHA: (mDefRel) implies: % 57.58/8.47 | (16) $i(sz10) % 57.58/8.47 | % 57.58/8.47 | ALPHA: (mPrIdeal) implies: % 57.58/8.48 | (17) ! [v0: $i] : ! [v1: $i] : ( ~ (slsdtgt0(v0) = v1) | ~ $i(v0) | ? % 57.58/8.48 | [v2: any] : ? [v3: any] : (aIdeal0(v1) = v3 & aElement0(v0) = v2 & % 57.58/8.48 | ( ~ (v2 = 0) | v3 = 0))) % 57.58/8.48 | % 57.58/8.48 | ALPHA: (m__2091) implies: % 57.58/8.48 | (18) aElement0(xa) = 0 % 57.58/8.48 | (19) aElement0(xb) = 0 % 57.58/8.48 | % 57.58/8.48 | ALPHA: (m__2174) implies: % 57.58/8.48 | (20) ? [v0: $i] : ? [v1: $i] : (slsdtgt0(xb) = v1 & slsdtgt0(xa) = v0 & % 57.58/8.48 | aIdeal0(xI) = 0 & sdtpldt1(v0, v1) = xI & $i(v1) & $i(v0)) % 57.58/8.48 | % 57.58/8.48 | ALPHA: (m__2203) implies: % 57.58/8.48 | (21) ? [v0: $i] : ? [v1: $i] : (slsdtgt0(xb) = v1 & slsdtgt0(xa) = v0 & % 57.58/8.48 | aElementOf0(xb, v1) = 0 & aElementOf0(xa, v0) = 0 & % 57.58/8.48 | aElementOf0(sz00, v1) = 0 & aElementOf0(sz00, v0) = 0 & $i(v1) & % 57.58/8.48 | $i(v0)) % 57.58/8.48 | % 57.58/8.48 | ALPHA: (m__2228) implies: % 57.58/8.48 | (22) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( ~ (v3 = % 57.58/8.48 | sz00) & slsdtgt0(xb) = v1 & slsdtgt0(xa) = v0 & sdtpldt1(v0, v1) = % 57.58/8.48 | v2 & aElementOf0(v3, v2) = 0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 57.58/8.48 | % 57.58/8.48 | ALPHA: (m__2273) implies: % 57.58/8.48 | (23) ? [v0: $i] : ( ~ (xu = sz00) & sbrdtbr0(xu) = v0 & aElementOf0(xu, % 57.58/8.48 | xI) = 0 & $i(v0) & ! [v1: $i] : ! [v2: $i] : (v1 = sz00 | ~ % 57.58/8.48 | (sbrdtbr0(v1) = v2) | ~ $i(v1) | ? [v3: any] : ? [v4: any] : % 57.58/8.48 | (iLess0(v2, v0) = v4 & aElementOf0(v1, xI) = v3 & ( ~ (v4 = 0) | % 57.58/8.48 | ~ (v3 = 0)))) & ! [v1: $i] : (v1 = sz00 | ~ (aElementOf0(v1, % 57.58/8.48 | xI) = 0) | ~ $i(v1) | ? [v2: $i] : ? [v3: int] : ( ~ (v3 = % 57.58/8.48 | 0) & iLess0(v2, v0) = v3 & sbrdtbr0(v1) = v2 & $i(v2)))) % 57.58/8.48 | % 57.58/8.48 | ALPHA: (m__2416) implies: % 57.58/8.48 | (24) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (sdtasdt0(xb, % 57.58/8.48 | v1) = v3 & sdtasdt0(xa, v0) = v2 & sdtpldt0(v2, v3) = xu & % 57.58/8.48 | aElement0(v1) = 0 & aElement0(v0) = 0 & $i(v3) & $i(v2) & $i(v1) & % 57.58/8.48 | $i(v0)) % 57.58/8.48 | % 57.58/8.48 | ALPHA: (m__2479) implies: % 57.58/8.48 | (25) $i(xa) % 57.58/8.48 | (26) doDivides0(xu, xa) = 0 % 57.58/8.48 | % 57.58/8.48 | ALPHA: (m__2612) implies: % 57.58/8.48 | (27) ? [v0: int] : ( ~ (v0 = 0) & doDivides0(xu, xb) = v0) % 57.58/8.48 | % 57.58/8.48 | ALPHA: (m__2666) implies: % 57.58/8.48 | (28) $i(xb) % 57.58/8.49 | (29) $i(xu) % 57.58/8.49 | (30) $i(xq) % 57.58/8.49 | (31) $i(xr) % 57.58/8.49 | (32) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: any] : (iLess0(v1, % 57.58/8.49 | v2) = v3 & sbrdtbr0(xr) = v1 & sbrdtbr0(xu) = v2 & sdtasdt0(xq, % 57.58/8.49 | xu) = v0 & sdtpldt0(v0, xr) = xb & aElement0(xr) = 0 & % 57.58/8.49 | aElement0(xq) = 0 & $i(v2) & $i(v1) & $i(v0) & (v3 = 0 | xr = sz00)) % 57.58/8.49 | % 57.58/8.49 | ALPHA: (m__) implies: % 57.58/8.49 | (33) xr = sz00 % 57.58/8.49 | % 57.58/8.49 | ALPHA: (function-axioms) implies: % 57.58/8.49 | (34) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 57.58/8.49 | : (v1 = v0 | ~ (aElement0(v2) = v1) | ~ (aElement0(v2) = v0)) % 57.58/8.49 | (35) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (sbrdtbr0(v2) % 57.58/8.49 | = v1) | ~ (sbrdtbr0(v2) = v0)) % 57.58/8.49 | (36) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (slsdtgt0(v2) % 57.58/8.49 | = v1) | ~ (slsdtgt0(v2) = v0)) % 57.58/8.49 | (37) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 57.58/8.49 | (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 57.58/8.49 | (38) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 57.58/8.49 | (sdtpldt1(v3, v2) = v1) | ~ (sdtpldt1(v3, v2) = v0)) % 57.58/8.49 | % 57.58/8.49 | DELTA: instantiating (27) with fresh symbol all_34_0 gives: % 57.58/8.49 | (39) ~ (all_34_0 = 0) & doDivides0(xu, xb) = all_34_0 % 57.58/8.49 | % 57.58/8.49 | ALPHA: (39) implies: % 57.58/8.49 | (40) ~ (all_34_0 = 0) % 57.58/8.49 | (41) doDivides0(xu, xb) = all_34_0 % 57.58/8.49 | % 57.58/8.49 | DELTA: instantiating (20) with fresh symbols all_38_0, all_38_1 gives: % 57.58/8.49 | (42) slsdtgt0(xb) = all_38_0 & slsdtgt0(xa) = all_38_1 & aIdeal0(xI) = 0 & % 57.58/8.49 | sdtpldt1(all_38_1, all_38_0) = xI & $i(all_38_0) & $i(all_38_1) % 57.58/8.49 | % 57.58/8.49 | ALPHA: (42) implies: % 57.58/8.49 | (43) sdtpldt1(all_38_1, all_38_0) = xI % 57.58/8.49 | (44) aIdeal0(xI) = 0 % 57.58/8.49 | (45) slsdtgt0(xa) = all_38_1 % 57.58/8.49 | (46) slsdtgt0(xb) = all_38_0 % 57.58/8.49 | % 57.58/8.49 | DELTA: instantiating (21) with fresh symbols all_40_0, all_40_1 gives: % 57.58/8.49 | (47) slsdtgt0(xb) = all_40_0 & slsdtgt0(xa) = all_40_1 & aElementOf0(xb, % 57.58/8.49 | all_40_0) = 0 & aElementOf0(xa, all_40_1) = 0 & aElementOf0(sz00, % 57.58/8.49 | all_40_0) = 0 & aElementOf0(sz00, all_40_1) = 0 & $i(all_40_0) & % 57.58/8.49 | $i(all_40_1) % 57.58/8.49 | % 57.58/8.49 | ALPHA: (47) implies: % 57.58/8.50 | (48) slsdtgt0(xb) = all_40_0 % 57.58/8.50 | % 57.58/8.50 | DELTA: instantiating (22) with fresh symbols all_42_0, all_42_1, all_42_2, % 57.58/8.50 | all_42_3 gives: % 57.58/8.50 | (49) ~ (all_42_0 = sz00) & slsdtgt0(xb) = all_42_2 & slsdtgt0(xa) = % 57.58/8.50 | all_42_3 & sdtpldt1(all_42_3, all_42_2) = all_42_1 & % 57.58/8.50 | aElementOf0(all_42_0, all_42_1) = 0 & $i(all_42_0) & $i(all_42_1) & % 57.58/8.50 | $i(all_42_2) & $i(all_42_3) % 57.58/8.50 | % 57.58/8.50 | ALPHA: (49) implies: % 57.58/8.50 | (50) $i(all_42_1) % 57.58/8.50 | (51) sdtpldt1(all_42_3, all_42_2) = all_42_1 % 57.58/8.50 | (52) slsdtgt0(xa) = all_42_3 % 57.58/8.50 | (53) slsdtgt0(xb) = all_42_2 % 57.58/8.50 | % 57.58/8.50 | DELTA: instantiating (24) with fresh symbols all_44_0, all_44_1, all_44_2, % 57.58/8.50 | all_44_3 gives: % 57.58/8.50 | (54) sdtasdt0(xb, all_44_2) = all_44_0 & sdtasdt0(xa, all_44_3) = all_44_1 % 57.58/8.50 | & sdtpldt0(all_44_1, all_44_0) = xu & aElement0(all_44_2) = 0 & % 57.58/8.50 | aElement0(all_44_3) = 0 & $i(all_44_0) & $i(all_44_1) & $i(all_44_2) & % 57.58/8.50 | $i(all_44_3) % 57.58/8.50 | % 57.58/8.50 | ALPHA: (54) implies: % 57.58/8.50 | (55) $i(all_44_3) % 57.58/8.50 | (56) $i(all_44_2) % 57.58/8.50 | (57) $i(all_44_1) % 57.58/8.50 | (58) $i(all_44_0) % 57.58/8.50 | (59) aElement0(all_44_3) = 0 % 57.58/8.50 | (60) aElement0(all_44_2) = 0 % 57.58/8.50 | (61) sdtpldt0(all_44_1, all_44_0) = xu % 57.58/8.50 | (62) sdtasdt0(xa, all_44_3) = all_44_1 % 57.58/8.50 | (63) sdtasdt0(xb, all_44_2) = all_44_0 % 57.58/8.50 | % 57.58/8.50 | DELTA: instantiating (32) with fresh symbols all_46_0, all_46_1, all_46_2, % 57.58/8.50 | all_46_3 gives: % 57.58/8.50 | (64) iLess0(all_46_2, all_46_1) = all_46_0 & sbrdtbr0(xr) = all_46_2 & % 57.58/8.50 | sbrdtbr0(xu) = all_46_1 & sdtasdt0(xq, xu) = all_46_3 & % 57.58/8.50 | sdtpldt0(all_46_3, xr) = xb & aElement0(xr) = 0 & aElement0(xq) = 0 & % 57.58/8.50 | $i(all_46_1) & $i(all_46_2) & $i(all_46_3) & (all_46_0 = 0 | xr = % 57.58/8.50 | sz00) % 57.58/8.50 | % 57.58/8.50 | ALPHA: (64) implies: % 57.58/8.50 | (65) $i(all_46_3) % 57.58/8.50 | (66) aElement0(xq) = 0 % 57.58/8.50 | (67) sdtpldt0(all_46_3, xr) = xb % 57.58/8.50 | (68) sdtasdt0(xq, xu) = all_46_3 % 57.58/8.50 | (69) sbrdtbr0(xu) = all_46_1 % 57.58/8.50 | % 57.58/8.50 | DELTA: instantiating (23) with fresh symbol all_48_0 gives: % 57.58/8.50 | (70) ~ (xu = sz00) & sbrdtbr0(xu) = all_48_0 & aElementOf0(xu, xI) = 0 & % 57.58/8.50 | $i(all_48_0) & ! [v0: $i] : ! [v1: $i] : (v0 = sz00 | ~ % 57.58/8.50 | (sbrdtbr0(v0) = v1) | ~ $i(v0) | ? [v2: any] : ? [v3: any] : % 57.58/8.50 | (iLess0(v1, all_48_0) = v3 & aElementOf0(v0, xI) = v2 & ( ~ (v3 = 0) % 57.58/8.50 | | ~ (v2 = 0)))) & ! [v0: $i] : (v0 = sz00 | ~ % 57.58/8.50 | (aElementOf0(v0, xI) = 0) | ~ $i(v0) | ? [v1: $i] : ? [v2: int] : % 57.58/8.50 | ( ~ (v2 = 0) & iLess0(v1, all_48_0) = v2 & sbrdtbr0(v0) = v1 & % 57.58/8.50 | $i(v1))) % 57.58/8.50 | % 57.58/8.50 | ALPHA: (70) implies: % 57.58/8.50 | (71) ~ (xu = sz00) % 57.58/8.50 | (72) aElementOf0(xu, xI) = 0 % 57.58/8.50 | (73) sbrdtbr0(xu) = all_48_0 % 57.58/8.50 | % 57.58/8.50 | REDUCE: (33), (67) imply: % 57.58/8.50 | (74) sdtpldt0(all_46_3, sz00) = xb % 57.58/8.50 | % 57.58/8.50 | REDUCE: (31), (33) imply: % 57.58/8.50 | (75) $i(sz00) % 57.58/8.50 | % 57.58/8.51 | GROUND_INST: instantiating (35) with all_46_1, all_48_0, xu, simplifying with % 57.58/8.51 | (69), (73) gives: % 57.58/8.51 | (76) all_48_0 = all_46_1 % 57.58/8.51 | % 57.58/8.51 | GROUND_INST: instantiating (36) with all_38_1, all_42_3, xa, simplifying with % 57.58/8.51 | (45), (52) gives: % 57.58/8.51 | (77) all_42_3 = all_38_1 % 57.58/8.51 | % 57.58/8.51 | GROUND_INST: instantiating (36) with all_40_0, all_42_2, xb, simplifying with % 57.58/8.51 | (48), (53) gives: % 57.58/8.51 | (78) all_42_2 = all_40_0 % 57.58/8.51 | % 57.58/8.51 | GROUND_INST: instantiating (36) with all_38_0, all_42_2, xb, simplifying with % 57.58/8.51 | (46), (53) gives: % 57.58/8.51 | (79) all_42_2 = all_38_0 % 57.58/8.51 | % 57.58/8.51 | COMBINE_EQS: (78), (79) imply: % 57.58/8.51 | (80) all_40_0 = all_38_0 % 57.58/8.51 | % 57.58/8.51 | SIMP: (80) implies: % 57.58/8.51 | (81) all_40_0 = all_38_0 % 57.58/8.51 | % 57.58/8.51 | REDUCE: (51), (77), (79) imply: % 57.58/8.51 | (82) sdtpldt1(all_38_1, all_38_0) = all_42_1 % 57.58/8.51 | % 57.58/8.51 | GROUND_INST: instantiating (38) with xI, all_42_1, all_38_0, all_38_1, % 57.58/8.51 | simplifying with (43), (82) gives: % 57.58/8.51 | (83) all_42_1 = xI % 57.58/8.51 | % 57.58/8.51 | REDUCE: (50), (83) imply: % 57.58/8.51 | (84) $i(xI) % 57.58/8.51 | % 57.58/8.51 | GROUND_INST: instantiating (12) with xa, sz10, simplifying with (1), (16), % 57.58/8.51 | (18), (25) gives: % 57.58/8.51 | (85) sz10 = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 57.58/8.51 | ? [v4: $i] : ? [v5: any] : (iLess0(v4, v0) = v5 & sbrdtbr0(v2) = v4 & % 57.58/8.51 | sbrdtbr0(sz10) = v0 & sdtasdt0(v1, sz10) = v3 & sdtpldt0(v3, v2) = % 57.58/8.51 | xa & aElement0(v2) = 0 & aElement0(v1) = 0 & $i(v4) & $i(v3) & % 57.58/8.51 | $i(v2) & $i(v1) & $i(v0) & (v5 = 0 | v2 = sz00)) % 57.58/8.51 | % 57.58/8.51 | GROUND_INST: instantiating (3) with all_44_0, all_44_1, xu, simplifying with % 57.58/8.51 | (57), (58), (61) gives: % 57.58/8.51 | (86) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(all_44_0, % 57.58/8.51 | all_44_1) = v2 & aElement0(all_44_0) = v0 & aElement0(all_44_1) = % 57.58/8.51 | v1 & $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = xu)) % 57.58/8.51 | % 57.58/8.51 | GROUND_INST: instantiating (2) with all_44_1, all_44_0, xu, simplifying with % 57.58/8.51 | (57), (58), (61) gives: % 57.58/8.51 | (87) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(all_44_0, % 57.58/8.51 | all_44_1) = v2 & aElement0(all_44_0) = v1 & aElement0(all_44_1) = % 57.58/8.51 | v0 & $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = xu)) % 57.58/8.51 | % 57.58/8.51 | GROUND_INST: instantiating (mSortsB) with all_44_1, all_44_0, xu, simplifying % 57.58/8.51 | with (57), (58), (61) gives: % 57.58/8.51 | (88) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_44_0) = v1 % 57.58/8.51 | & aElement0(all_44_1) = v0 & aElement0(xu) = v2 & ( ~ (v1 = 0) | ~ % 57.58/8.51 | (v0 = 0) | v2 = 0)) % 57.58/8.51 | % 57.58/8.51 | GROUND_INST: instantiating (4) with all_46_3, xb, simplifying with (65), (74) % 57.58/8.51 | gives: % 57.58/8.51 | (89) ? [v0: any] : ? [v1: $i] : (sdtpldt0(sz00, all_46_3) = v1 & % 57.58/8.51 | aElement0(all_46_3) = v0 & $i(v1) & ( ~ (v0 = 0) | (v1 = xb & % 57.58/8.51 | all_46_3 = xb))) % 57.58/8.51 | % 57.58/8.51 | GROUND_INST: instantiating (3) with sz00, all_46_3, xb, simplifying with (65), % 57.58/8.51 | (74), (75) gives: % 57.58/8.51 | (90) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(sz00, all_46_3) % 57.58/8.51 | = v2 & aElement0(all_46_3) = v1 & aElement0(sz00) = v0 & $i(v2) & ( % 57.58/8.51 | ~ (v1 = 0) | ~ (v0 = 0) | v2 = xb)) % 57.58/8.51 | % 57.58/8.51 | GROUND_INST: instantiating (2) with all_46_3, sz00, xb, simplifying with (65), % 57.58/8.51 | (74), (75) gives: % 57.58/8.51 | (91) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(sz00, all_46_3) % 57.58/8.51 | = v2 & aElement0(all_46_3) = v0 & aElement0(sz00) = v1 & $i(v2) & ( % 57.58/8.51 | ~ (v1 = 0) | ~ (v0 = 0) | v2 = xb)) % 57.58/8.51 | % 57.58/8.51 | GROUND_INST: instantiating (mSortsB) with all_46_3, sz00, xb, simplifying with % 57.58/8.51 | (65), (74), (75) gives: % 57.58/8.51 | (92) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_46_3) = v0 % 57.58/8.51 | & aElement0(xb) = v2 & aElement0(sz00) = v1 & ( ~ (v1 = 0) | ~ (v0 % 57.58/8.51 | = 0) | v2 = 0)) % 57.58/8.51 | % 57.98/8.51 | GROUND_INST: instantiating (6) with all_44_3, xa, all_44_1, simplifying with % 57.98/8.51 | (25), (55), (62) gives: % 57.98/8.51 | (93) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_44_3, xa) = % 57.98/8.51 | v2 & aElement0(all_44_3) = v0 & aElement0(xa) = v1 & $i(v2) & ( ~ % 57.98/8.51 | (v1 = 0) | ~ (v0 = 0) | v2 = all_44_1)) % 57.98/8.51 | % 57.98/8.51 | GROUND_INST: instantiating (5) with xa, all_44_3, all_44_1, simplifying with % 57.98/8.51 | (25), (55), (62) gives: % 57.98/8.51 | (94) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_44_3, xa) = % 57.98/8.51 | v2 & aElement0(all_44_3) = v1 & aElement0(xa) = v0 & $i(v2) & ( ~ % 57.98/8.51 | (v1 = 0) | ~ (v0 = 0) | v2 = all_44_1)) % 57.98/8.51 | % 57.98/8.51 | GROUND_INST: instantiating (mSortsB_02) with xa, all_44_3, all_44_1, % 57.98/8.51 | simplifying with (25), (55), (62) gives: % 57.98/8.51 | (95) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_44_1) = v2 % 57.98/8.51 | & aElement0(all_44_3) = v1 & aElement0(xa) = v0 & ( ~ (v1 = 0) | ~ % 57.98/8.51 | (v0 = 0) | v2 = 0)) % 57.98/8.51 | % 57.98/8.51 | GROUND_INST: instantiating (8) with all_44_2, all_46_3, sz00, xb, all_44_0, % 57.98/8.51 | simplifying with (56), (63), (65), (74), (75) gives: % 57.98/8.52 | (96) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: $i] % 57.98/8.52 | : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] % 57.98/8.52 | : (sdtasdt0(all_46_3, all_44_2) = v7 & sdtasdt0(all_44_2, all_46_3) = % 57.98/8.52 | v4 & sdtasdt0(all_44_2, xb) = v3 & sdtasdt0(all_44_2, sz00) = v5 & % 57.98/8.52 | sdtasdt0(sz00, all_44_2) = v8 & sdtpldt0(v7, v8) = v9 & sdtpldt0(v4, % 57.98/8.52 | v5) = v6 & aElement0(all_46_3) = v1 & aElement0(all_44_2) = v0 & % 57.98/8.52 | aElement0(sz00) = v2 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & % 57.98/8.52 | $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | (v9 = % 57.98/8.52 | all_44_0 & v6 = v3))) % 57.98/8.52 | % 57.98/8.52 | GROUND_INST: instantiating (6) with all_44_2, xb, all_44_0, simplifying with % 57.98/8.52 | (28), (56), (63) gives: % 57.98/8.52 | (97) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_44_2, xb) = % 57.98/8.52 | v2 & aElement0(all_44_2) = v0 & aElement0(xb) = v1 & $i(v2) & ( ~ % 57.98/8.52 | (v1 = 0) | ~ (v0 = 0) | v2 = all_44_0)) % 57.98/8.52 | % 57.98/8.52 | GROUND_INST: instantiating (5) with xb, all_44_2, all_44_0, simplifying with % 57.98/8.52 | (28), (56), (63) gives: % 57.98/8.52 | (98) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_44_2, xb) = % 57.98/8.52 | v2 & aElement0(all_44_2) = v1 & aElement0(xb) = v0 & $i(v2) & ( ~ % 57.98/8.52 | (v1 = 0) | ~ (v0 = 0) | v2 = all_44_0)) % 57.98/8.52 | % 57.98/8.52 | GROUND_INST: instantiating (mSortsB_02) with xb, all_44_2, all_44_0, % 57.98/8.52 | simplifying with (28), (56), (63) gives: % 57.98/8.52 | (99) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_44_0) = v2 % 57.98/8.52 | & aElement0(all_44_2) = v1 & aElement0(xb) = v0 & ( ~ (v1 = 0) | ~ % 57.98/8.52 | (v0 = 0) | v2 = 0)) % 57.98/8.52 | % 57.98/8.52 | GROUND_INST: instantiating (7) with xq, all_44_1, all_44_0, xu, all_46_3, % 57.98/8.52 | simplifying with (30), (57), (58), (61), (68) gives: % 57.98/8.52 | (100) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: % 57.98/8.52 | $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? % 57.98/8.52 | [v9: $i] : (sdtasdt0(all_44_0, xq) = v8 & sdtasdt0(all_44_1, xq) = v7 % 57.98/8.52 | & sdtasdt0(xq, all_44_0) = v4 & sdtasdt0(xq, all_44_1) = v3 & % 57.98/8.52 | sdtasdt0(xu, xq) = v6 & sdtpldt0(v7, v8) = v9 & sdtpldt0(v3, v4) = % 57.98/8.52 | v5 & aElement0(all_44_0) = v2 & aElement0(all_44_1) = v1 & % 57.98/8.52 | aElement0(xq) = v0 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & % 57.98/8.52 | $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | (v9 = % 57.98/8.52 | v6 & v5 = all_46_3))) % 57.98/8.52 | % 57.98/8.52 | GROUND_INST: instantiating (6) with xu, xq, all_46_3, simplifying with (29), % 57.98/8.52 | (30), (68) gives: % 57.98/8.52 | (101) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(xu, xq) = v2 & % 57.98/8.52 | aElement0(xq) = v1 & aElement0(xu) = v0 & $i(v2) & ( ~ (v1 = 0) | % 57.98/8.52 | ~ (v0 = 0) | v2 = all_46_3)) % 57.98/8.52 | % 57.98/8.52 | GROUND_INST: instantiating (5) with xq, xu, all_46_3, simplifying with (29), % 57.98/8.52 | (30), (68) gives: % 57.98/8.52 | (102) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(xu, xq) = v2 & % 57.98/8.52 | aElement0(xq) = v0 & aElement0(xu) = v1 & $i(v2) & ( ~ (v1 = 0) | % 57.98/8.52 | ~ (v0 = 0) | v2 = all_46_3)) % 57.98/8.52 | % 57.98/8.52 | GROUND_INST: instantiating (mSortsB_02) with xq, xu, all_46_3, simplifying % 57.98/8.52 | with (29), (30), (68) gives: % 57.98/8.52 | (103) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_46_3) = % 57.98/8.52 | v2 & aElement0(xq) = v0 & aElement0(xu) = v1 & ( ~ (v1 = 0) | ~ % 57.98/8.52 | (v0 = 0) | v2 = 0)) % 57.98/8.52 | % 57.98/8.52 | GROUND_INST: instantiating (10) with xI, xu, xq, all_46_3, simplifying with % 57.98/8.52 | (29), (30), (44), (68), (72), (84) gives: % 57.98/8.52 | (104) ? [v0: any] : ? [v1: any] : (aElementOf0(all_46_3, xI) = v1 & % 57.98/8.52 | aElement0(xq) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 57.98/8.52 | % 57.98/8.52 | GROUND_INST: instantiating (11) with xu, all_46_1, simplifying with (29), (69) % 57.98/8.52 | gives: % 57.98/8.52 | (105) xu = sz00 | ? [v0: any] : ? [v1: any] : (aNaturalNumber0(all_46_1) % 57.98/8.52 | = v1 & aElement0(xu) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 57.98/8.52 | % 57.98/8.52 | GROUND_INST: instantiating (15) with xa, xu, 0, simplifying with (18), (25), % 57.98/8.52 | (26), (29) gives: % 57.98/8.52 | (106) ? [v0: any] : ? [v1: any] : (aDivisorOf0(xu, xa) = v0 & % 57.98/8.52 | aElement0(xu) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 57.98/8.52 | % 57.98/8.52 | GROUND_INST: instantiating (14) with xa, xu, simplifying with (18), (25), % 57.98/8.52 | (26), (29) gives: % 57.98/8.52 | (107) ? [v0: any] : ? [v1: any] : (aDivisorOf0(xu, xa) = v1 & % 57.98/8.52 | aElement0(xu) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 57.98/8.52 | % 57.98/8.52 | GROUND_INST: instantiating (13) with xu, xb, all_34_0, xq, simplifying with % 57.98/8.52 | (28), (29), (30), (41), (66) gives: % 57.98/8.52 | (108) all_34_0 = 0 | ? [v0: any] : ? [v1: any] : (( ~ (v0 = xb) & % 57.98/8.52 | sdtasdt0(xu, xq) = v0 & $i(v0)) | (aElement0(xu) = v0 & % 57.98/8.52 | aElement0(xb) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0)))) % 57.98/8.52 | % 57.98/8.52 | GROUND_INST: instantiating (15) with xb, xu, all_34_0, simplifying with (19), % 57.98/8.52 | (28), (29), (41) gives: % 57.98/8.52 | (109) ? [v0: any] : ? [v1: any] : (aDivisorOf0(xu, xb) = v0 & % 57.98/8.52 | aElement0(xu) = v1 & ( ~ (v0 = 0) | (v1 = 0 & all_34_0 = 0))) % 57.98/8.52 | % 57.98/8.52 | GROUND_INST: instantiating (17) with xb, all_38_0, simplifying with (28), (46) % 57.98/8.52 | gives: % 57.98/8.53 | (110) ? [v0: any] : ? [v1: any] : (aIdeal0(all_38_0) = v1 & aElement0(xb) % 57.98/8.53 | = v0 & ( ~ (v0 = 0) | v1 = 0)) % 57.98/8.53 | % 57.98/8.53 | DELTA: instantiating (104) with fresh symbols all_212_0, all_212_1 gives: % 57.98/8.53 | (111) aElementOf0(all_46_3, xI) = all_212_0 & aElement0(xq) = all_212_1 & ( % 57.98/8.53 | ~ (all_212_1 = 0) | all_212_0 = 0) % 57.98/8.53 | % 57.98/8.53 | ALPHA: (111) implies: % 57.98/8.53 | (112) aElement0(xq) = all_212_1 % 57.98/8.53 | % 57.98/8.53 | DELTA: instantiating (110) with fresh symbols all_226_0, all_226_1 gives: % 57.98/8.53 | (113) aIdeal0(all_38_0) = all_226_0 & aElement0(xb) = all_226_1 & ( ~ % 57.98/8.53 | (all_226_1 = 0) | all_226_0 = 0) % 57.98/8.53 | % 57.98/8.53 | ALPHA: (113) implies: % 57.98/8.53 | (114) aElement0(xb) = all_226_1 % 57.98/8.53 | % 57.98/8.53 | DELTA: instantiating (107) with fresh symbols all_236_0, all_236_1 gives: % 57.98/8.53 | (115) aDivisorOf0(xu, xa) = all_236_0 & aElement0(xu) = all_236_1 & ( ~ % 57.98/8.53 | (all_236_1 = 0) | all_236_0 = 0) % 57.98/8.53 | % 57.98/8.53 | ALPHA: (115) implies: % 57.98/8.53 | (116) aElement0(xu) = all_236_1 % 57.98/8.53 | % 57.98/8.53 | DELTA: instantiating (106) with fresh symbols all_238_0, all_238_1 gives: % 57.98/8.53 | (117) aDivisorOf0(xu, xa) = all_238_1 & aElement0(xu) = all_238_0 & ( ~ % 57.98/8.53 | (all_238_1 = 0) | all_238_0 = 0) % 57.98/8.53 | % 57.98/8.53 | ALPHA: (117) implies: % 57.98/8.53 | (118) aElement0(xu) = all_238_0 % 57.98/8.53 | % 57.98/8.53 | DELTA: instantiating (109) with fresh symbols all_368_0, all_368_1 gives: % 57.98/8.53 | (119) aDivisorOf0(xu, xb) = all_368_1 & aElement0(xu) = all_368_0 & ( ~ % 57.98/8.53 | (all_368_1 = 0) | (all_368_0 = 0 & all_34_0 = 0)) % 57.98/8.53 | % 57.98/8.53 | ALPHA: (119) implies: % 57.98/8.53 | (120) aElement0(xu) = all_368_0 % 57.98/8.53 | % 57.98/8.53 | DELTA: instantiating (103) with fresh symbols all_370_0, all_370_1, all_370_2 % 57.98/8.53 | gives: % 57.98/8.53 | (121) aElement0(all_46_3) = all_370_0 & aElement0(xq) = all_370_2 & % 57.98/8.53 | aElement0(xu) = all_370_1 & ( ~ (all_370_1 = 0) | ~ (all_370_2 = 0) % 57.98/8.53 | | all_370_0 = 0) % 57.98/8.53 | % 57.98/8.53 | ALPHA: (121) implies: % 57.98/8.53 | (122) aElement0(xu) = all_370_1 % 57.98/8.53 | (123) aElement0(xq) = all_370_2 % 57.98/8.53 | (124) aElement0(all_46_3) = all_370_0 % 57.98/8.53 | (125) ~ (all_370_1 = 0) | ~ (all_370_2 = 0) | all_370_0 = 0 % 57.98/8.53 | % 57.98/8.53 | DELTA: instantiating (95) with fresh symbols all_372_0, all_372_1, all_372_2 % 57.98/8.53 | gives: % 57.98/8.53 | (126) aElement0(all_44_1) = all_372_0 & aElement0(all_44_3) = all_372_1 & % 57.98/8.53 | aElement0(xa) = all_372_2 & ( ~ (all_372_1 = 0) | ~ (all_372_2 = 0) % 57.98/8.53 | | all_372_0 = 0) % 57.98/8.53 | % 57.98/8.53 | ALPHA: (126) implies: % 57.98/8.53 | (127) aElement0(xa) = all_372_2 % 57.98/8.53 | (128) aElement0(all_44_3) = all_372_1 % 57.98/8.53 | (129) aElement0(all_44_1) = all_372_0 % 57.98/8.53 | (130) ~ (all_372_1 = 0) | ~ (all_372_2 = 0) | all_372_0 = 0 % 57.98/8.53 | % 57.98/8.53 | DELTA: instantiating (89) with fresh symbols all_374_0, all_374_1 gives: % 57.98/8.53 | (131) sdtpldt0(sz00, all_46_3) = all_374_0 & aElement0(all_46_3) = % 57.98/8.53 | all_374_1 & $i(all_374_0) & ( ~ (all_374_1 = 0) | (all_374_0 = xb & % 57.98/8.53 | all_46_3 = xb)) % 57.98/8.53 | % 57.98/8.53 | ALPHA: (131) implies: % 57.98/8.53 | (132) aElement0(all_46_3) = all_374_1 % 57.98/8.53 | (133) ~ (all_374_1 = 0) | (all_374_0 = xb & all_46_3 = xb) % 57.98/8.53 | % 57.98/8.53 | DELTA: instantiating (88) with fresh symbols all_376_0, all_376_1, all_376_2 % 57.98/8.53 | gives: % 57.98/8.53 | (134) aElement0(all_44_0) = all_376_1 & aElement0(all_44_1) = all_376_2 & % 57.98/8.53 | aElement0(xu) = all_376_0 & ( ~ (all_376_1 = 0) | ~ (all_376_2 = 0) % 57.98/8.53 | | all_376_0 = 0) % 57.98/8.53 | % 57.98/8.53 | ALPHA: (134) implies: % 57.98/8.53 | (135) aElement0(xu) = all_376_0 % 57.98/8.53 | (136) aElement0(all_44_1) = all_376_2 % 57.98/8.53 | (137) aElement0(all_44_0) = all_376_1 % 57.98/8.53 | (138) ~ (all_376_1 = 0) | ~ (all_376_2 = 0) | all_376_0 = 0 % 57.98/8.53 | % 57.98/8.53 | DELTA: instantiating (92) with fresh symbols all_378_0, all_378_1, all_378_2 % 57.98/8.53 | gives: % 57.98/8.53 | (139) aElement0(all_46_3) = all_378_2 & aElement0(xb) = all_378_0 & % 57.98/8.53 | aElement0(sz00) = all_378_1 & ( ~ (all_378_1 = 0) | ~ (all_378_2 = % 57.98/8.53 | 0) | all_378_0 = 0) % 57.98/8.53 | % 57.98/8.53 | ALPHA: (139) implies: % 57.98/8.53 | (140) aElement0(xb) = all_378_0 % 57.98/8.53 | (141) aElement0(all_46_3) = all_378_2 % 57.98/8.53 | % 57.98/8.53 | DELTA: instantiating (99) with fresh symbols all_382_0, all_382_1, all_382_2 % 57.98/8.53 | gives: % 57.98/8.53 | (142) aElement0(all_44_0) = all_382_0 & aElement0(all_44_2) = all_382_1 & % 57.98/8.53 | aElement0(xb) = all_382_2 & ( ~ (all_382_1 = 0) | ~ (all_382_2 = 0) % 57.98/8.53 | | all_382_0 = 0) % 57.98/8.53 | % 57.98/8.53 | ALPHA: (142) implies: % 57.98/8.53 | (143) aElement0(xb) = all_382_2 % 57.98/8.53 | (144) aElement0(all_44_2) = all_382_1 % 57.98/8.53 | (145) aElement0(all_44_0) = all_382_0 % 57.98/8.53 | (146) ~ (all_382_1 = 0) | ~ (all_382_2 = 0) | all_382_0 = 0 % 57.98/8.53 | % 57.98/8.53 | DELTA: instantiating (102) with fresh symbols all_384_0, all_384_1, all_384_2 % 57.98/8.53 | gives: % 57.98/8.53 | (147) sdtasdt0(xu, xq) = all_384_0 & aElement0(xq) = all_384_2 & % 57.98/8.53 | aElement0(xu) = all_384_1 & $i(all_384_0) & ( ~ (all_384_1 = 0) | ~ % 57.98/8.53 | (all_384_2 = 0) | all_384_0 = all_46_3) % 57.98/8.53 | % 57.98/8.53 | ALPHA: (147) implies: % 57.98/8.53 | (148) aElement0(xu) = all_384_1 % 57.98/8.53 | (149) aElement0(xq) = all_384_2 % 57.98/8.53 | (150) sdtasdt0(xu, xq) = all_384_0 % 57.98/8.53 | (151) ~ (all_384_1 = 0) | ~ (all_384_2 = 0) | all_384_0 = all_46_3 % 57.98/8.53 | % 57.98/8.53 | DELTA: instantiating (98) with fresh symbols all_386_0, all_386_1, all_386_2 % 57.98/8.53 | gives: % 57.98/8.53 | (152) sdtasdt0(all_44_2, xb) = all_386_0 & aElement0(all_44_2) = all_386_1 % 57.98/8.53 | & aElement0(xb) = all_386_2 & $i(all_386_0) & ( ~ (all_386_1 = 0) | % 57.98/8.53 | ~ (all_386_2 = 0) | all_386_0 = all_44_0) % 57.98/8.53 | % 57.98/8.53 | ALPHA: (152) implies: % 57.98/8.53 | (153) aElement0(xb) = all_386_2 % 57.98/8.53 | (154) aElement0(all_44_2) = all_386_1 % 57.98/8.53 | % 57.98/8.53 | DELTA: instantiating (101) with fresh symbols all_388_0, all_388_1, all_388_2 % 57.98/8.53 | gives: % 57.98/8.53 | (155) sdtasdt0(xu, xq) = all_388_0 & aElement0(xq) = all_388_1 & % 57.98/8.53 | aElement0(xu) = all_388_2 & $i(all_388_0) & ( ~ (all_388_1 = 0) | ~ % 57.98/8.53 | (all_388_2 = 0) | all_388_0 = all_46_3) % 57.98/8.53 | % 57.98/8.53 | ALPHA: (155) implies: % 57.98/8.53 | (156) aElement0(xu) = all_388_2 % 57.98/8.53 | (157) aElement0(xq) = all_388_1 % 57.98/8.53 | (158) sdtasdt0(xu, xq) = all_388_0 % 57.98/8.53 | % 57.98/8.53 | DELTA: instantiating (93) with fresh symbols all_390_0, all_390_1, all_390_2 % 57.98/8.53 | gives: % 57.98/8.53 | (159) sdtasdt0(all_44_3, xa) = all_390_0 & aElement0(all_44_3) = all_390_2 % 57.98/8.53 | & aElement0(xa) = all_390_1 & $i(all_390_0) & ( ~ (all_390_1 = 0) | % 57.98/8.53 | ~ (all_390_2 = 0) | all_390_0 = all_44_1) % 57.98/8.53 | % 57.98/8.53 | ALPHA: (159) implies: % 57.98/8.53 | (160) aElement0(xa) = all_390_1 % 57.98/8.53 | (161) aElement0(all_44_3) = all_390_2 % 57.98/8.53 | % 57.98/8.53 | DELTA: instantiating (91) with fresh symbols all_392_0, all_392_1, all_392_2 % 57.98/8.53 | gives: % 57.98/8.53 | (162) sdtpldt0(sz00, all_46_3) = all_392_0 & aElement0(all_46_3) = % 57.98/8.53 | all_392_2 & aElement0(sz00) = all_392_1 & $i(all_392_0) & ( ~ % 57.98/8.53 | (all_392_1 = 0) | ~ (all_392_2 = 0) | all_392_0 = xb) % 57.98/8.53 | % 57.98/8.53 | ALPHA: (162) implies: % 57.98/8.54 | (163) aElement0(all_46_3) = all_392_2 % 57.98/8.54 | % 57.98/8.54 | DELTA: instantiating (94) with fresh symbols all_394_0, all_394_1, all_394_2 % 57.98/8.54 | gives: % 57.98/8.54 | (164) sdtasdt0(all_44_3, xa) = all_394_0 & aElement0(all_44_3) = all_394_1 % 57.98/8.54 | & aElement0(xa) = all_394_2 & $i(all_394_0) & ( ~ (all_394_1 = 0) | % 57.98/8.54 | ~ (all_394_2 = 0) | all_394_0 = all_44_1) % 57.98/8.54 | % 57.98/8.54 | ALPHA: (164) implies: % 57.98/8.54 | (165) aElement0(xa) = all_394_2 % 57.98/8.54 | (166) aElement0(all_44_3) = all_394_1 % 57.98/8.54 | % 57.98/8.54 | DELTA: instantiating (90) with fresh symbols all_396_0, all_396_1, all_396_2 % 57.98/8.54 | gives: % 57.98/8.54 | (167) sdtpldt0(sz00, all_46_3) = all_396_0 & aElement0(all_46_3) = % 57.98/8.54 | all_396_1 & aElement0(sz00) = all_396_2 & $i(all_396_0) & ( ~ % 57.98/8.54 | (all_396_1 = 0) | ~ (all_396_2 = 0) | all_396_0 = xb) % 57.98/8.54 | % 57.98/8.54 | ALPHA: (167) implies: % 57.98/8.54 | (168) aElement0(all_46_3) = all_396_1 % 57.98/8.54 | % 57.98/8.54 | DELTA: instantiating (97) with fresh symbols all_398_0, all_398_1, all_398_2 % 57.98/8.54 | gives: % 57.98/8.54 | (169) sdtasdt0(all_44_2, xb) = all_398_0 & aElement0(all_44_2) = all_398_2 % 57.98/8.54 | & aElement0(xb) = all_398_1 & $i(all_398_0) & ( ~ (all_398_1 = 0) | % 57.98/8.54 | ~ (all_398_2 = 0) | all_398_0 = all_44_0) % 57.98/8.54 | % 57.98/8.54 | ALPHA: (169) implies: % 57.98/8.54 | (170) aElement0(xb) = all_398_1 % 57.98/8.54 | (171) aElement0(all_44_2) = all_398_2 % 57.98/8.54 | % 57.98/8.54 | DELTA: instantiating (87) with fresh symbols all_400_0, all_400_1, all_400_2 % 57.98/8.54 | gives: % 57.98/8.54 | (172) sdtpldt0(all_44_0, all_44_1) = all_400_0 & aElement0(all_44_0) = % 57.98/8.54 | all_400_1 & aElement0(all_44_1) = all_400_2 & $i(all_400_0) & ( ~ % 57.98/8.54 | (all_400_1 = 0) | ~ (all_400_2 = 0) | all_400_0 = xu) % 57.98/8.54 | % 57.98/8.54 | ALPHA: (172) implies: % 57.98/8.54 | (173) aElement0(all_44_1) = all_400_2 % 57.98/8.54 | (174) aElement0(all_44_0) = all_400_1 % 57.98/8.54 | % 57.98/8.54 | DELTA: instantiating (86) with fresh symbols all_402_0, all_402_1, all_402_2 % 57.98/8.54 | gives: % 57.98/8.54 | (175) sdtpldt0(all_44_0, all_44_1) = all_402_0 & aElement0(all_44_0) = % 57.98/8.54 | all_402_2 & aElement0(all_44_1) = all_402_1 & $i(all_402_0) & ( ~ % 57.98/8.54 | (all_402_1 = 0) | ~ (all_402_2 = 0) | all_402_0 = xu) % 57.98/8.54 | % 57.98/8.54 | ALPHA: (175) implies: % 57.98/8.54 | (176) aElement0(all_44_1) = all_402_1 % 57.98/8.54 | (177) aElement0(all_44_0) = all_402_2 % 57.98/8.54 | % 57.98/8.54 | DELTA: instantiating (96) with fresh symbols all_512_0, all_512_1, all_512_2, % 57.98/8.54 | all_512_3, all_512_4, all_512_5, all_512_6, all_512_7, all_512_8, % 57.98/8.54 | all_512_9 gives: % 57.98/8.54 | (178) sdtasdt0(all_46_3, all_44_2) = all_512_2 & sdtasdt0(all_44_2, % 57.98/8.54 | all_46_3) = all_512_5 & sdtasdt0(all_44_2, xb) = all_512_6 & % 57.98/8.54 | sdtasdt0(all_44_2, sz00) = all_512_4 & sdtasdt0(sz00, all_44_2) = % 57.98/8.54 | all_512_1 & sdtpldt0(all_512_2, all_512_1) = all_512_0 & % 57.98/8.54 | sdtpldt0(all_512_5, all_512_4) = all_512_3 & aElement0(all_46_3) = % 57.98/8.54 | all_512_8 & aElement0(all_44_2) = all_512_9 & aElement0(sz00) = % 57.98/8.54 | all_512_7 & $i(all_512_0) & $i(all_512_1) & $i(all_512_2) & % 57.98/8.54 | $i(all_512_3) & $i(all_512_4) & $i(all_512_5) & $i(all_512_6) & ( ~ % 57.98/8.54 | (all_512_7 = 0) | ~ (all_512_8 = 0) | ~ (all_512_9 = 0) | % 57.98/8.54 | (all_512_0 = all_44_0 & all_512_3 = all_512_6)) % 57.98/8.54 | % 57.98/8.54 | ALPHA: (178) implies: % 57.98/8.54 | (179) aElement0(all_44_2) = all_512_9 % 57.98/8.54 | (180) aElement0(all_46_3) = all_512_8 % 57.98/8.54 | % 57.98/8.54 | DELTA: instantiating (100) with fresh symbols all_514_0, all_514_1, all_514_2, % 57.98/8.54 | all_514_3, all_514_4, all_514_5, all_514_6, all_514_7, all_514_8, % 57.98/8.54 | all_514_9 gives: % 57.98/8.54 | (181) sdtasdt0(all_44_0, xq) = all_514_1 & sdtasdt0(all_44_1, xq) = % 57.98/8.54 | all_514_2 & sdtasdt0(xq, all_44_0) = all_514_5 & sdtasdt0(xq, % 57.98/8.54 | all_44_1) = all_514_6 & sdtasdt0(xu, xq) = all_514_3 & % 57.98/8.54 | sdtpldt0(all_514_2, all_514_1) = all_514_0 & sdtpldt0(all_514_6, % 57.98/8.54 | all_514_5) = all_514_4 & aElement0(all_44_0) = all_514_7 & % 57.98/8.54 | aElement0(all_44_1) = all_514_8 & aElement0(xq) = all_514_9 & % 57.98/8.54 | $i(all_514_0) & $i(all_514_1) & $i(all_514_2) & $i(all_514_3) & % 57.98/8.54 | $i(all_514_4) & $i(all_514_5) & $i(all_514_6) & ( ~ (all_514_7 = 0) | % 57.98/8.54 | ~ (all_514_8 = 0) | ~ (all_514_9 = 0) | (all_514_0 = all_514_3 & % 57.98/8.54 | all_514_4 = all_46_3)) % 57.98/8.54 | % 57.98/8.54 | ALPHA: (181) implies: % 57.98/8.54 | (182) aElement0(xq) = all_514_9 % 57.98/8.54 | (183) aElement0(all_44_1) = all_514_8 % 57.98/8.54 | (184) aElement0(all_44_0) = all_514_7 % 57.98/8.54 | (185) sdtasdt0(xu, xq) = all_514_3 % 57.98/8.54 | % 57.98/8.54 | BETA: splitting (105) gives: % 57.98/8.54 | % 57.98/8.54 | Case 1: % 57.98/8.54 | | % 57.98/8.54 | | (186) xu = sz00 % 57.98/8.54 | | % 57.98/8.54 | | REDUCE: (71), (186) imply: % 57.98/8.54 | | (187) $false % 57.98/8.54 | | % 57.98/8.54 | | CLOSE: (187) is inconsistent. % 57.98/8.54 | | % 57.98/8.54 | Case 2: % 57.98/8.54 | | % 57.98/8.54 | | (188) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(all_46_1) = v1 & % 57.98/8.54 | | aElement0(xu) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 57.98/8.54 | | % 57.98/8.54 | | DELTA: instantiating (188) with fresh symbols all_607_0, all_607_1 gives: % 57.98/8.54 | | (189) aNaturalNumber0(all_46_1) = all_607_0 & aElement0(xu) = all_607_1 & % 57.98/8.54 | | ( ~ (all_607_1 = 0) | all_607_0 = 0) % 57.98/8.54 | | % 57.98/8.54 | | ALPHA: (189) implies: % 57.98/8.54 | | (190) aElement0(xu) = all_607_1 % 57.98/8.54 | | % 57.98/8.54 | | BETA: splitting (108) gives: % 57.98/8.54 | | % 57.98/8.54 | | Case 1: % 57.98/8.54 | | | % 57.98/8.54 | | | (191) all_34_0 = 0 % 57.98/8.54 | | | % 57.98/8.54 | | | REDUCE: (40), (191) imply: % 57.98/8.54 | | | (192) $false % 57.98/8.54 | | | % 57.98/8.54 | | | CLOSE: (192) is inconsistent. % 57.98/8.54 | | | % 57.98/8.54 | | Case 2: % 57.98/8.54 | | | % 57.98/8.54 | | | (193) ? [v0: any] : ? [v1: any] : (( ~ (v0 = xb) & sdtasdt0(xu, xq) = % 57.98/8.54 | | | v0 & $i(v0)) | (aElement0(xu) = v0 & aElement0(xb) = v1 & ( ~ % 57.98/8.54 | | | (v1 = 0) | ~ (v0 = 0)))) % 57.98/8.54 | | | % 57.98/8.54 | | | DELTA: instantiating (193) with fresh symbols all_617_0, all_617_1 gives: % 57.98/8.54 | | | (194) ( ~ (all_617_1 = xb) & sdtasdt0(xu, xq) = all_617_1 & % 57.98/8.54 | | | $i(all_617_1)) | (aElement0(xu) = all_617_1 & aElement0(xb) = % 57.98/8.54 | | | all_617_0 & ( ~ (all_617_0 = 0) | ~ (all_617_1 = 0))) % 57.98/8.54 | | | % 57.98/8.54 | | | BETA: splitting (85) gives: % 57.98/8.54 | | | % 57.98/8.54 | | | Case 1: % 57.98/8.54 | | | | % 57.98/8.54 | | | | (195) sz10 = sz00 % 57.98/8.54 | | | | % 57.98/8.54 | | | | REDUCE: (9), (195) imply: % 57.98/8.54 | | | | (196) $false % 57.98/8.54 | | | | % 57.98/8.54 | | | | CLOSE: (196) is inconsistent. % 57.98/8.54 | | | | % 57.98/8.54 | | | Case 2: % 57.98/8.54 | | | | % 57.98/8.54 | | | | % 57.98/8.54 | | | | GROUND_INST: instantiating (34) with 0, all_394_2, xa, simplifying with % 57.98/8.54 | | | | (18), (165) gives: % 57.98/8.54 | | | | (197) all_394_2 = 0 % 57.98/8.54 | | | | % 57.98/8.54 | | | | GROUND_INST: instantiating (34) with all_390_1, all_394_2, xa, % 57.98/8.54 | | | | simplifying with (160), (165) gives: % 57.98/8.54 | | | | (198) all_394_2 = all_390_1 % 57.98/8.54 | | | | % 57.98/8.54 | | | | GROUND_INST: instantiating (34) with all_372_2, all_394_2, xa, % 57.98/8.54 | | | | simplifying with (127), (165) gives: % 57.98/8.54 | | | | (199) all_394_2 = all_372_2 % 57.98/8.54 | | | | % 57.98/8.54 | | | | GROUND_INST: instantiating (34) with 0, all_386_2, xb, simplifying with % 57.98/8.54 | | | | (19), (153) gives: % 57.98/8.54 | | | | (200) all_386_2 = 0 % 57.98/8.54 | | | | % 57.98/8.54 | | | | GROUND_INST: instantiating (34) with all_378_0, all_386_2, xb, % 57.98/8.55 | | | | simplifying with (140), (153) gives: % 57.98/8.55 | | | | (201) all_386_2 = all_378_0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_226_1, all_386_2, xb, % 57.98/8.55 | | | | simplifying with (114), (153) gives: % 57.98/8.55 | | | | (202) all_386_2 = all_226_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_386_2, all_398_1, xb, % 57.98/8.55 | | | | simplifying with (153), (170) gives: % 57.98/8.55 | | | | (203) all_398_1 = all_386_2 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_382_2, all_398_1, xb, % 57.98/8.55 | | | | simplifying with (143), (170) gives: % 57.98/8.55 | | | | (204) all_398_1 = all_382_2 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_236_1, all_370_1, xu, % 57.98/8.55 | | | | simplifying with (116), (122) gives: % 57.98/8.55 | | | | (205) all_370_1 = all_236_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_368_0, all_384_1, xu, % 57.98/8.55 | | | | simplifying with (120), (148) gives: % 57.98/8.55 | | | | (206) all_384_1 = all_368_0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_388_2, all_607_1, xu, % 57.98/8.55 | | | | simplifying with (156), (190) gives: % 57.98/8.55 | | | | (207) all_607_1 = all_388_2 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_384_1, all_607_1, xu, % 57.98/8.55 | | | | simplifying with (148), (190) gives: % 57.98/8.55 | | | | (208) all_607_1 = all_384_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_376_0, all_607_1, xu, % 57.98/8.55 | | | | simplifying with (135), (190) gives: % 57.98/8.55 | | | | (209) all_607_1 = all_376_0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_370_1, all_607_1, xu, % 57.98/8.55 | | | | simplifying with (122), (190) gives: % 57.98/8.55 | | | | (210) all_607_1 = all_370_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_238_0, all_607_1, xu, % 57.98/8.55 | | | | simplifying with (118), (190) gives: % 57.98/8.55 | | | | (211) all_607_1 = all_238_0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_370_2, all_384_2, xq, % 57.98/8.55 | | | | simplifying with (123), (149) gives: % 57.98/8.55 | | | | (212) all_384_2 = all_370_2 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_212_1, all_384_2, xq, % 57.98/8.55 | | | | simplifying with (112), (149) gives: % 57.98/8.55 | | | | (213) all_384_2 = all_212_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_370_2, all_388_1, xq, % 57.98/8.55 | | | | simplifying with (123), (157) gives: % 57.98/8.55 | | | | (214) all_388_1 = all_370_2 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with 0, all_514_9, xq, simplifying with % 57.98/8.55 | | | | (66), (182) gives: % 57.98/8.55 | | | | (215) all_514_9 = 0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_388_1, all_514_9, xq, % 57.98/8.55 | | | | simplifying with (157), (182) gives: % 57.98/8.55 | | | | (216) all_514_9 = all_388_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with 0, all_390_2, all_44_3, simplifying % 57.98/8.55 | | | | with (59), (161) gives: % 57.98/8.55 | | | | (217) all_390_2 = 0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_390_2, all_394_1, all_44_3, % 57.98/8.55 | | | | simplifying with (161), (166) gives: % 57.98/8.55 | | | | (218) all_394_1 = all_390_2 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_372_1, all_394_1, all_44_3, % 57.98/8.55 | | | | simplifying with (128), (166) gives: % 57.98/8.55 | | | | (219) all_394_1 = all_372_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with 0, all_398_2, all_44_2, simplifying % 57.98/8.55 | | | | with (60), (171) gives: % 57.98/8.55 | | | | (220) all_398_2 = 0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_386_1, all_398_2, all_44_2, % 57.98/8.55 | | | | simplifying with (154), (171) gives: % 57.98/8.55 | | | | (221) all_398_2 = all_386_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_386_1, all_512_9, all_44_2, % 57.98/8.55 | | | | simplifying with (154), (179) gives: % 57.98/8.55 | | | | (222) all_512_9 = all_386_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_382_1, all_512_9, all_44_2, % 57.98/8.55 | | | | simplifying with (144), (179) gives: % 57.98/8.55 | | | | (223) all_512_9 = all_382_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_402_1, all_514_8, all_44_1, % 57.98/8.55 | | | | simplifying with (176), (183) gives: % 57.98/8.55 | | | | (224) all_514_8 = all_402_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_400_2, all_514_8, all_44_1, % 57.98/8.55 | | | | simplifying with (173), (183) gives: % 57.98/8.55 | | | | (225) all_514_8 = all_400_2 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_376_2, all_514_8, all_44_1, % 57.98/8.55 | | | | simplifying with (136), (183) gives: % 57.98/8.55 | | | | (226) all_514_8 = all_376_2 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_372_0, all_514_8, all_44_1, % 57.98/8.55 | | | | simplifying with (129), (183) gives: % 57.98/8.55 | | | | (227) all_514_8 = all_372_0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_382_0, all_400_1, all_44_0, % 57.98/8.55 | | | | simplifying with (145), (174) gives: % 57.98/8.55 | | | | (228) all_400_1 = all_382_0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_400_1, all_402_2, all_44_0, % 57.98/8.55 | | | | simplifying with (174), (177) gives: % 57.98/8.55 | | | | (229) all_402_2 = all_400_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_402_2, all_514_7, all_44_0, % 57.98/8.55 | | | | simplifying with (177), (184) gives: % 57.98/8.55 | | | | (230) all_514_7 = all_402_2 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_376_1, all_514_7, all_44_0, % 57.98/8.55 | | | | simplifying with (137), (184) gives: % 57.98/8.55 | | | | (231) all_514_7 = all_376_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_370_0, all_392_2, all_46_3, % 57.98/8.55 | | | | simplifying with (124), (163) gives: % 57.98/8.55 | | | | (232) all_392_2 = all_370_0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_392_2, all_396_1, all_46_3, % 57.98/8.55 | | | | simplifying with (163), (168) gives: % 57.98/8.55 | | | | (233) all_396_1 = all_392_2 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_378_2, all_396_1, all_46_3, % 57.98/8.55 | | | | simplifying with (141), (168) gives: % 57.98/8.55 | | | | (234) all_396_1 = all_378_2 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_392_2, all_512_8, all_46_3, % 57.98/8.55 | | | | simplifying with (163), (180) gives: % 57.98/8.55 | | | | (235) all_512_8 = all_392_2 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (34) with all_374_1, all_512_8, all_46_3, % 57.98/8.55 | | | | simplifying with (132), (180) gives: % 57.98/8.55 | | | | (236) all_512_8 = all_374_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (37) with all_388_0, all_514_3, xq, xu, % 57.98/8.55 | | | | simplifying with (158), (185) gives: % 57.98/8.55 | | | | (237) all_514_3 = all_388_0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | GROUND_INST: instantiating (37) with all_384_0, all_514_3, xq, xu, % 57.98/8.55 | | | | simplifying with (150), (185) gives: % 57.98/8.55 | | | | (238) all_514_3 = all_384_0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (207), (208) imply: % 57.98/8.55 | | | | (239) all_388_2 = all_384_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (207), (211) imply: % 57.98/8.55 | | | | (240) all_388_2 = all_238_0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (207), (210) imply: % 57.98/8.55 | | | | (241) all_388_2 = all_370_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (207), (209) imply: % 57.98/8.55 | | | | (242) all_388_2 = all_376_0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (237), (238) imply: % 57.98/8.55 | | | | (243) all_388_0 = all_384_0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | SIMP: (243) implies: % 57.98/8.55 | | | | (244) all_388_0 = all_384_0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (230), (231) imply: % 57.98/8.55 | | | | (245) all_402_2 = all_376_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | SIMP: (245) implies: % 57.98/8.55 | | | | (246) all_402_2 = all_376_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (224), (225) imply: % 57.98/8.55 | | | | (247) all_402_1 = all_400_2 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (224), (227) imply: % 57.98/8.55 | | | | (248) all_402_1 = all_372_0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (224), (226) imply: % 57.98/8.55 | | | | (249) all_402_1 = all_376_2 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (215), (216) imply: % 57.98/8.55 | | | | (250) all_388_1 = 0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | SIMP: (250) implies: % 57.98/8.55 | | | | (251) all_388_1 = 0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (235), (236) imply: % 57.98/8.55 | | | | (252) all_392_2 = all_374_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | SIMP: (252) implies: % 57.98/8.55 | | | | (253) all_392_2 = all_374_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (222), (223) imply: % 57.98/8.55 | | | | (254) all_386_1 = all_382_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | SIMP: (254) implies: % 57.98/8.55 | | | | (255) all_386_1 = all_382_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (247), (249) imply: % 57.98/8.55 | | | | (256) all_400_2 = all_376_2 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (247), (248) imply: % 57.98/8.55 | | | | (257) all_400_2 = all_372_0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (229), (246) imply: % 57.98/8.55 | | | | (258) all_400_1 = all_376_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | SIMP: (258) implies: % 57.98/8.55 | | | | (259) all_400_1 = all_376_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (228), (259) imply: % 57.98/8.55 | | | | (260) all_382_0 = all_376_1 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (256), (257) imply: % 57.98/8.55 | | | | (261) all_376_2 = all_372_0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | SIMP: (261) implies: % 57.98/8.55 | | | | (262) all_376_2 = all_372_0 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (203), (204) imply: % 57.98/8.55 | | | | (263) all_386_2 = all_382_2 % 57.98/8.55 | | | | % 57.98/8.55 | | | | SIMP: (263) implies: % 57.98/8.55 | | | | (264) all_386_2 = all_382_2 % 57.98/8.55 | | | | % 57.98/8.55 | | | | COMBINE_EQS: (220), (221) imply: % 57.98/8.56 | | | | (265) all_386_1 = 0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | SIMP: (265) implies: % 57.98/8.56 | | | | (266) all_386_1 = 0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (233), (234) imply: % 57.98/8.56 | | | | (267) all_392_2 = all_378_2 % 57.98/8.56 | | | | % 57.98/8.56 | | | | SIMP: (267) implies: % 57.98/8.56 | | | | (268) all_392_2 = all_378_2 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (218), (219) imply: % 57.98/8.56 | | | | (269) all_390_2 = all_372_1 % 57.98/8.56 | | | | % 57.98/8.56 | | | | SIMP: (269) implies: % 57.98/8.56 | | | | (270) all_390_2 = all_372_1 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (197), (198) imply: % 57.98/8.56 | | | | (271) all_390_1 = 0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (198), (199) imply: % 57.98/8.56 | | | | (272) all_390_1 = all_372_2 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (232), (268) imply: % 57.98/8.56 | | | | (273) all_378_2 = all_370_0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (253), (268) imply: % 57.98/8.56 | | | | (274) all_378_2 = all_374_1 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (271), (272) imply: % 57.98/8.56 | | | | (275) all_372_2 = 0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | SIMP: (275) implies: % 57.98/8.56 | | | | (276) all_372_2 = 0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (217), (270) imply: % 57.98/8.56 | | | | (277) all_372_1 = 0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (214), (251) imply: % 57.98/8.56 | | | | (278) all_370_2 = 0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | SIMP: (278) implies: % 57.98/8.56 | | | | (279) all_370_2 = 0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (240), (242) imply: % 57.98/8.56 | | | | (280) all_376_0 = all_238_0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (239), (242) imply: % 57.98/8.56 | | | | (281) all_384_1 = all_376_0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | SIMP: (281) implies: % 57.98/8.56 | | | | (282) all_384_1 = all_376_0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (241), (242) imply: % 57.98/8.56 | | | | (283) all_376_0 = all_370_1 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (255), (266) imply: % 57.98/8.56 | | | | (284) all_382_1 = 0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | SIMP: (284) implies: % 57.98/8.56 | | | | (285) all_382_1 = 0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (201), (264) imply: % 57.98/8.56 | | | | (286) all_382_2 = all_378_0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (202), (264) imply: % 57.98/8.56 | | | | (287) all_382_2 = all_226_1 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (200), (264) imply: % 57.98/8.56 | | | | (288) all_382_2 = 0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (206), (282) imply: % 57.98/8.56 | | | | (289) all_376_0 = all_368_0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | SIMP: (289) implies: % 57.98/8.56 | | | | (290) all_376_0 = all_368_0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (212), (213) imply: % 57.98/8.56 | | | | (291) all_370_2 = all_212_1 % 57.98/8.56 | | | | % 57.98/8.56 | | | | SIMP: (291) implies: % 57.98/8.56 | | | | (292) all_370_2 = all_212_1 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (286), (288) imply: % 57.98/8.56 | | | | (293) all_378_0 = 0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (286), (287) imply: % 57.98/8.56 | | | | (294) all_378_0 = all_226_1 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (293), (294) imply: % 57.98/8.56 | | | | (295) all_226_1 = 0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | SIMP: (295) implies: % 57.98/8.56 | | | | (296) all_226_1 = 0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (273), (274) imply: % 57.98/8.56 | | | | (297) all_374_1 = all_370_0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (280), (290) imply: % 57.98/8.56 | | | | (298) all_368_0 = all_238_0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (283), (290) imply: % 57.98/8.56 | | | | (299) all_370_1 = all_368_0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | SIMP: (299) implies: % 57.98/8.56 | | | | (300) all_370_1 = all_368_0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (205), (300) imply: % 57.98/8.56 | | | | (301) all_368_0 = all_236_1 % 57.98/8.56 | | | | % 57.98/8.56 | | | | SIMP: (301) implies: % 57.98/8.56 | | | | (302) all_368_0 = all_236_1 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (279), (292) imply: % 57.98/8.56 | | | | (303) all_212_1 = 0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (298), (302) imply: % 57.98/8.56 | | | | (304) all_238_0 = all_236_1 % 57.98/8.56 | | | | % 57.98/8.56 | | | | SIMP: (304) implies: % 57.98/8.56 | | | | (305) all_238_0 = all_236_1 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (290), (302) imply: % 57.98/8.56 | | | | (306) all_376_0 = all_236_1 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (213), (303) imply: % 57.98/8.56 | | | | (307) all_384_2 = 0 % 57.98/8.56 | | | | % 57.98/8.56 | | | | COMBINE_EQS: (206), (302) imply: % 57.98/8.56 | | | | (308) all_384_1 = all_236_1 % 57.98/8.56 | | | | % 57.98/8.56 | | | | BETA: splitting (130) gives: % 57.98/8.56 | | | | % 57.98/8.56 | | | | Case 1: % 57.98/8.56 | | | | | % 57.98/8.56 | | | | | (309) ~ (all_372_1 = 0) % 57.98/8.56 | | | | | % 57.98/8.56 | | | | | REDUCE: (277), (309) imply: % 57.98/8.56 | | | | | (310) $false % 57.98/8.56 | | | | | % 57.98/8.56 | | | | | CLOSE: (310) is inconsistent. % 57.98/8.56 | | | | | % 57.98/8.56 | | | | Case 2: % 57.98/8.56 | | | | | % 57.98/8.56 | | | | | (311) ~ (all_372_2 = 0) | all_372_0 = 0 % 57.98/8.56 | | | | | % 57.98/8.56 | | | | | BETA: splitting (311) gives: % 57.98/8.56 | | | | | % 57.98/8.56 | | | | | Case 1: % 57.98/8.56 | | | | | | % 57.98/8.56 | | | | | | (312) ~ (all_372_2 = 0) % 57.98/8.56 | | | | | | % 57.98/8.56 | | | | | | REDUCE: (276), (312) imply: % 57.98/8.56 | | | | | | (313) $false % 57.98/8.56 | | | | | | % 57.98/8.56 | | | | | | CLOSE: (313) is inconsistent. % 57.98/8.56 | | | | | | % 57.98/8.56 | | | | | Case 2: % 57.98/8.56 | | | | | | % 57.98/8.56 | | | | | | (314) all_372_0 = 0 % 57.98/8.56 | | | | | | % 57.98/8.56 | | | | | | COMBINE_EQS: (262), (314) imply: % 57.98/8.56 | | | | | | (315) all_376_2 = 0 % 57.98/8.56 | | | | | | % 57.98/8.56 | | | | | | BETA: splitting (146) gives: % 57.98/8.56 | | | | | | % 57.98/8.56 | | | | | | Case 1: % 57.98/8.56 | | | | | | | % 57.98/8.56 | | | | | | | (316) ~ (all_382_1 = 0) % 57.98/8.56 | | | | | | | % 57.98/8.56 | | | | | | | REDUCE: (285), (316) imply: % 57.98/8.56 | | | | | | | (317) $false % 57.98/8.56 | | | | | | | % 57.98/8.56 | | | | | | | CLOSE: (317) is inconsistent. % 57.98/8.56 | | | | | | | % 57.98/8.56 | | | | | | Case 2: % 57.98/8.56 | | | | | | | % 57.98/8.56 | | | | | | | (318) ~ (all_382_2 = 0) | all_382_0 = 0 % 57.98/8.56 | | | | | | | % 57.98/8.56 | | | | | | | BETA: splitting (318) gives: % 57.98/8.56 | | | | | | | % 57.98/8.56 | | | | | | | Case 1: % 57.98/8.56 | | | | | | | | % 57.98/8.56 | | | | | | | | (319) ~ (all_382_2 = 0) % 57.98/8.56 | | | | | | | | % 57.98/8.56 | | | | | | | | REDUCE: (288), (319) imply: % 57.98/8.56 | | | | | | | | (320) $false % 57.98/8.56 | | | | | | | | % 57.98/8.56 | | | | | | | | CLOSE: (320) is inconsistent. % 57.98/8.56 | | | | | | | | % 57.98/8.56 | | | | | | | Case 2: % 57.98/8.56 | | | | | | | | % 57.98/8.56 | | | | | | | | (321) all_382_0 = 0 % 57.98/8.56 | | | | | | | | % 57.98/8.56 | | | | | | | | COMBINE_EQS: (260), (321) imply: % 57.98/8.56 | | | | | | | | (322) all_376_1 = 0 % 57.98/8.56 | | | | | | | | % 57.98/8.56 | | | | | | | | BETA: splitting (138) gives: % 57.98/8.56 | | | | | | | | % 57.98/8.56 | | | | | | | | Case 1: % 57.98/8.56 | | | | | | | | | % 57.98/8.56 | | | | | | | | | (323) ~ (all_376_1 = 0) % 57.98/8.56 | | | | | | | | | % 57.98/8.56 | | | | | | | | | REDUCE: (322), (323) imply: % 57.98/8.56 | | | | | | | | | (324) $false % 57.98/8.56 | | | | | | | | | % 57.98/8.56 | | | | | | | | | CLOSE: (324) is inconsistent. % 57.98/8.56 | | | | | | | | | % 57.98/8.56 | | | | | | | | Case 2: % 57.98/8.56 | | | | | | | | | % 57.98/8.56 | | | | | | | | | (325) ~ (all_376_2 = 0) | all_376_0 = 0 % 57.98/8.56 | | | | | | | | | % 57.98/8.56 | | | | | | | | | BETA: splitting (325) gives: % 57.98/8.56 | | | | | | | | | % 57.98/8.56 | | | | | | | | | Case 1: % 57.98/8.56 | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | (326) ~ (all_376_2 = 0) % 57.98/8.56 | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | REDUCE: (315), (326) imply: % 57.98/8.56 | | | | | | | | | | (327) $false % 57.98/8.56 | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | CLOSE: (327) is inconsistent. % 57.98/8.56 | | | | | | | | | | % 57.98/8.56 | | | | | | | | | Case 2: % 57.98/8.56 | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | (328) all_376_0 = 0 % 57.98/8.56 | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | COMBINE_EQS: (306), (328) imply: % 57.98/8.56 | | | | | | | | | | (329) all_236_1 = 0 % 57.98/8.56 | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | COMBINE_EQS: (205), (329) imply: % 57.98/8.56 | | | | | | | | | | (330) all_370_1 = 0 % 57.98/8.56 | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | COMBINE_EQS: (308), (329) imply: % 57.98/8.56 | | | | | | | | | | (331) all_384_1 = 0 % 57.98/8.56 | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | REDUCE: (116), (329) imply: % 57.98/8.56 | | | | | | | | | | (332) aElement0(xu) = 0 % 57.98/8.56 | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | BETA: splitting (194) gives: % 57.98/8.56 | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | Case 1: % 57.98/8.56 | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | (333) ~ (all_617_1 = xb) & sdtasdt0(xu, xq) = all_617_1 % 57.98/8.56 | | | | | | | | | | | & $i(all_617_1) % 57.98/8.56 | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | ALPHA: (333) implies: % 57.98/8.56 | | | | | | | | | | | (334) ~ (all_617_1 = xb) % 57.98/8.56 | | | | | | | | | | | (335) sdtasdt0(xu, xq) = all_617_1 % 57.98/8.56 | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | BETA: splitting (151) gives: % 57.98/8.56 | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | Case 1: % 57.98/8.56 | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | (336) ~ (all_384_1 = 0) % 57.98/8.56 | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | REDUCE: (331), (336) imply: % 57.98/8.56 | | | | | | | | | | | | (337) $false % 57.98/8.56 | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | CLOSE: (337) is inconsistent. % 57.98/8.56 | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | Case 2: % 57.98/8.56 | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | (338) ~ (all_384_2 = 0) | all_384_0 = all_46_3 % 57.98/8.56 | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | BETA: splitting (338) gives: % 57.98/8.56 | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | Case 1: % 57.98/8.56 | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | (339) ~ (all_384_2 = 0) % 57.98/8.56 | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | REDUCE: (307), (339) imply: % 57.98/8.56 | | | | | | | | | | | | | (340) $false % 57.98/8.56 | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | CLOSE: (340) is inconsistent. % 57.98/8.56 | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | Case 2: % 57.98/8.56 | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | (341) all_384_0 = all_46_3 % 57.98/8.56 | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | REDUCE: (150), (341) imply: % 57.98/8.56 | | | | | | | | | | | | | (342) sdtasdt0(xu, xq) = all_46_3 % 57.98/8.56 | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | BETA: splitting (125) gives: % 57.98/8.56 | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | Case 1: % 57.98/8.56 | | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | | (343) ~ (all_370_1 = 0) % 57.98/8.56 | | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | | REDUCE: (330), (343) imply: % 57.98/8.56 | | | | | | | | | | | | | | (344) $false % 57.98/8.56 | | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | | CLOSE: (344) is inconsistent. % 57.98/8.56 | | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | Case 2: % 57.98/8.56 | | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | | (345) ~ (all_370_2 = 0) | all_370_0 = 0 % 57.98/8.56 | | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | | BETA: splitting (345) gives: % 57.98/8.56 | | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | | Case 1: % 57.98/8.56 | | | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | | | (346) ~ (all_370_2 = 0) % 57.98/8.56 | | | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | | | REDUCE: (279), (346) imply: % 57.98/8.56 | | | | | | | | | | | | | | | (347) $false % 57.98/8.56 | | | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | | | CLOSE: (347) is inconsistent. % 57.98/8.56 | | | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | | Case 2: % 57.98/8.56 | | | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | | | (348) all_370_0 = 0 % 57.98/8.56 | | | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | | | COMBINE_EQS: (297), (348) imply: % 57.98/8.56 | | | | | | | | | | | | | | | (349) all_374_1 = 0 % 57.98/8.56 | | | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | | | BETA: splitting (133) gives: % 57.98/8.56 | | | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | | | Case 1: % 57.98/8.56 | | | | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | | | | (350) ~ (all_374_1 = 0) % 57.98/8.56 | | | | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | | | | REDUCE: (349), (350) imply: % 57.98/8.56 | | | | | | | | | | | | | | | | (351) $false % 57.98/8.56 | | | | | | | | | | | | | | | | % 57.98/8.56 | | | | | | | | | | | | | | | | CLOSE: (351) is inconsistent. % 57.98/8.56 | | | | | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | | | | | Case 2: % 57.98/8.57 | | | | | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | | | | | | (352) all_374_0 = xb & all_46_3 = xb % 57.98/8.57 | | | | | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | | | | | | ALPHA: (352) implies: % 57.98/8.57 | | | | | | | | | | | | | | | | (353) all_46_3 = xb % 57.98/8.57 | | | | | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | | | | | | REDUCE: (342), (353) imply: % 57.98/8.57 | | | | | | | | | | | | | | | | (354) sdtasdt0(xu, xq) = xb % 57.98/8.57 | | | | | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (37) with xb, all_617_1, xq, xu, % 57.98/8.57 | | | | | | | | | | | | | | | | simplifying with (335), (354) gives: % 57.98/8.57 | | | | | | | | | | | | | | | | (355) all_617_1 = xb % 57.98/8.57 | | | | | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | | | | | | REDUCE: (334), (355) imply: % 57.98/8.57 | | | | | | | | | | | | | | | | (356) $false % 57.98/8.57 | | | | | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | | | | | | CLOSE: (356) is inconsistent. % 57.98/8.57 | | | | | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | | | | | End of split % 57.98/8.57 | | | | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | | | | End of split % 57.98/8.57 | | | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | | | End of split % 57.98/8.57 | | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | | End of split % 57.98/8.57 | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | End of split % 57.98/8.57 | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | Case 2: % 57.98/8.57 | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | (357) aElement0(xu) = all_617_1 & aElement0(xb) = % 57.98/8.57 | | | | | | | | | | | all_617_0 & ( ~ (all_617_0 = 0) | ~ (all_617_1 = % 57.98/8.57 | | | | | | | | | | | 0)) % 57.98/8.57 | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | ALPHA: (357) implies: % 57.98/8.57 | | | | | | | | | | | (358) aElement0(xb) = all_617_0 % 57.98/8.57 | | | | | | | | | | | (359) aElement0(xu) = all_617_1 % 57.98/8.57 | | | | | | | | | | | (360) ~ (all_617_0 = 0) | ~ (all_617_1 = 0) % 57.98/8.57 | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | GROUND_INST: instantiating (34) with 0, all_617_0, xb, % 57.98/8.57 | | | | | | | | | | | simplifying with (19), (358) gives: % 57.98/8.57 | | | | | | | | | | | (361) all_617_0 = 0 % 57.98/8.57 | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | GROUND_INST: instantiating (34) with 0, all_617_1, xu, % 57.98/8.57 | | | | | | | | | | | simplifying with (332), (359) gives: % 57.98/8.57 | | | | | | | | | | | (362) all_617_1 = 0 % 57.98/8.57 | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | BETA: splitting (360) gives: % 57.98/8.57 | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | Case 1: % 57.98/8.57 | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | | (363) ~ (all_617_0 = 0) % 57.98/8.57 | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | | REDUCE: (361), (363) imply: % 57.98/8.57 | | | | | | | | | | | | (364) $false % 57.98/8.57 | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | | CLOSE: (364) is inconsistent. % 57.98/8.57 | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | Case 2: % 57.98/8.57 | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | | (365) ~ (all_617_1 = 0) % 57.98/8.57 | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | | REDUCE: (362), (365) imply: % 57.98/8.57 | | | | | | | | | | | | (366) $false % 57.98/8.57 | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | | CLOSE: (366) is inconsistent. % 57.98/8.57 | | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | | End of split % 57.98/8.57 | | | | | | | | | | | % 57.98/8.57 | | | | | | | | | | End of split % 57.98/8.57 | | | | | | | | | | % 57.98/8.57 | | | | | | | | | End of split % 57.98/8.57 | | | | | | | | | % 57.98/8.57 | | | | | | | | End of split % 57.98/8.57 | | | | | | | | % 57.98/8.57 | | | | | | | End of split % 57.98/8.57 | | | | | | | % 57.98/8.57 | | | | | | End of split % 57.98/8.57 | | | | | | % 57.98/8.57 | | | | | End of split % 57.98/8.57 | | | | | % 57.98/8.57 | | | | End of split % 57.98/8.57 | | | | % 57.98/8.57 | | | End of split % 57.98/8.57 | | | % 57.98/8.57 | | End of split % 57.98/8.57 | | % 57.98/8.57 | End of split % 57.98/8.57 | % 57.98/8.57 End of proof % 57.98/8.57 % SZS output end Proof for theBenchmark % 57.98/8.57 % 57.98/8.57 7948ms %------------------------------------------------------------------------------