%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : RNG122+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 : n008.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 13:58:00 EDT 2023 % Result : Theorem 18.14s 3.27s % Output : Proof 50.83s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : RNG122+1 : TPTP v8.1.2. Released v4.0.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n008.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Aug 27 03:10:02 EDT 2023 % 0.13/0.34 % CPUTime : % 0.20/0.59 ________ _____ % 0.20/0.59 ___ __ \_________(_)________________________________ % 0.20/0.59 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.59 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.59 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.59 % 0.20/0.59 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.59 (2023-06-19) % 0.20/0.59 % 0.20/0.59 (c) Philipp Rümmer, 2009-2023 % 0.20/0.59 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.59 Amanda Stjerna. % 0.20/0.59 Free software under BSD-3-Clause. % 0.20/0.59 % 0.20/0.59 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.59 % 0.20/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.20/0.60 Running up to 7 provers in parallel. % 0.20/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.19/1.18 Prover 4: Preprocessing ... % 3.19/1.18 Prover 1: Preprocessing ... % 3.58/1.23 Prover 5: Preprocessing ... % 3.58/1.23 Prover 6: Preprocessing ... % 3.58/1.23 Prover 3: Preprocessing ... % 3.58/1.23 Prover 2: Preprocessing ... % 3.58/1.24 Prover 0: Preprocessing ... % 9.31/2.05 Prover 1: Constructing countermodel ... % 9.31/2.08 Prover 3: Constructing countermodel ... % 9.31/2.11 Prover 6: Proving ... % 9.31/2.11 Prover 5: Proving ... % 10.00/2.24 Prover 2: Proving ... % 10.00/2.26 Prover 4: Constructing countermodel ... % 11.00/2.36 Prover 0: Proving ... % 18.14/3.27 Prover 0: proved (2662ms) % 18.14/3.27 % 18.14/3.27 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.14/3.27 % 18.14/3.29 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 18.14/3.29 Prover 2: stopped % 18.14/3.29 Prover 3: stopped % 18.75/3.30 Prover 5: stopped % 18.75/3.31 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 18.75/3.31 Prover 6: stopped % 18.75/3.32 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 18.75/3.32 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 18.75/3.32 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 19.34/3.38 Prover 10: Preprocessing ... % 19.34/3.38 Prover 7: Preprocessing ... % 19.34/3.42 Prover 8: Preprocessing ... % 19.34/3.42 Prover 11: Preprocessing ... % 19.34/3.44 Prover 13: Preprocessing ... % 20.07/3.62 Prover 10: Constructing countermodel ... % 20.07/3.63 Prover 7: Constructing countermodel ... % 21.40/3.67 Prover 8: Warning: ignoring some quantifiers % 21.40/3.67 Prover 13: Warning: ignoring some quantifiers % 21.40/3.68 Prover 8: Constructing countermodel ... % 21.40/3.70 Prover 13: Constructing countermodel ... % 21.95/3.76 Prover 11: Constructing countermodel ... % 49.81/7.46 Prover 4: Found proof (size 321) % 49.81/7.46 Prover 4: proved (6848ms) % 49.81/7.47 Prover 13: stopped % 49.81/7.47 Prover 11: stopped % 49.81/7.47 Prover 8: stopped % 49.81/7.47 Prover 1: stopped % 49.81/7.47 Prover 7: stopped % 49.81/7.47 Prover 10: stopped % 49.81/7.47 % 49.81/7.47 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 49.81/7.47 % 50.44/7.54 % SZS output start Proof for theBenchmark % 50.44/7.54 Assumptions after simplification: % 50.44/7.54 --------------------------------- % 50.44/7.54 % 50.44/7.54 (mAMDistr) % 50.44/7.58 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 50.44/7.58 $i] : ( ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v1, v0) = v3) | ~ % 50.44/7.58 (sdtpldt0(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : % 50.44/7.58 ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? % 50.44/7.58 [v12: $i] : ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v9, v0) = v14 & % 50.44/7.58 sdtasdt0(v0, v9) = v10 & sdtasdt0(v0, v2) = v12 & sdtasdt0(v0, v1) = v11 & % 50.44/7.58 sdtpldt0(v11, v12) = v13 & sdtpldt0(v1, v2) = v9 & aElement0(v2) = v8 & % 50.44/7.58 aElement0(v1) = v7 & aElement0(v0) = v6 & $i(v14) & $i(v13) & $i(v12) & % 50.44/7.58 $i(v11) & $i(v10) & $i(v9) & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | % 50.44/7.58 (v14 = v5 & v13 = v10)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 50.44/7.58 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ % 50.44/7.58 (sdtasdt0(v0, v1) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) % 50.44/7.58 | ~ $i(v0) | ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? % 50.44/7.58 [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : % 50.44/7.58 (sdtasdt0(v9, v0) = v11 & sdtasdt0(v2, v0) = v13 & sdtasdt0(v1, v0) = v12 & % 50.44/7.58 sdtasdt0(v0, v9) = v10 & sdtpldt0(v12, v13) = v14 & sdtpldt0(v1, v2) = v9 % 50.44/7.58 & aElement0(v2) = v8 & aElement0(v1) = v7 & aElement0(v0) = v6 & $i(v14) & % 50.44/7.58 $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) & ( ~ (v8 = 0) | ~ (v7 = % 50.44/7.58 0) | ~ (v6 = 0) | (v14 = v11 & v10 = v5)))) & ! [v0: $i] : ! [v1: % 50.44/7.58 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (sdtasdt0(v3, v0) = v4) % 50.44/7.58 | ~ (sdtpldt0(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: % 50.44/7.58 any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? [v9: $i] : ? [v10: % 50.44/7.58 $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : % 50.44/7.58 (sdtasdt0(v2, v0) = v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v3) = v8 & % 50.44/7.58 sdtasdt0(v0, v2) = v10 & sdtasdt0(v0, v1) = v9 & sdtpldt0(v12, v13) = v14 % 50.44/7.58 & sdtpldt0(v9, v10) = v11 & aElement0(v2) = v7 & aElement0(v1) = v6 & % 50.44/7.58 aElement0(v0) = v5 & $i(v14) & $i(v13) & $i(v12) & $i(v11) & $i(v10) & % 50.44/7.58 $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | (v14 = v4 & % 50.44/7.58 v11 = v8)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 50.44/7.58 ! [v4: $i] : ( ~ (sdtasdt0(v0, v3) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ % 50.44/7.58 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] % 50.44/7.58 : ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : % 50.44/7.58 ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v3, v0) = v11 & sdtasdt0(v2, v0) = % 50.44/7.58 v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v2) = v9 & sdtasdt0(v0, v1) = % 50.44/7.58 v8 & sdtpldt0(v12, v13) = v14 & sdtpldt0(v8, v9) = v10 & aElement0(v2) = % 50.44/7.58 v7 & aElement0(v1) = v6 & aElement0(v0) = v5 & $i(v14) & $i(v13) & $i(v12) % 50.44/7.58 & $i(v11) & $i(v10) & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ % 50.44/7.58 (v5 = 0) | (v14 = v11 & v10 = v4)))) % 50.44/7.58 % 50.44/7.58 (mAddAsso) % 50.44/7.59 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 50.44/7.59 (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) % 50.44/7.59 | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? % 50.44/7.59 [v9: $i] : (sdtpldt0(v1, v2) = v8 & sdtpldt0(v0, v8) = v9 & aElement0(v2) = % 50.44/7.59 v7 & aElement0(v1) = v6 & aElement0(v0) = v5 & $i(v9) & $i(v8) & ( ~ (v7 = % 50.44/7.59 0) | ~ (v6 = 0) | ~ (v5 = 0) | v9 = v4))) & ! [v0: $i] : ! [v1: % 50.44/7.59 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (sdtpldt0(v1, v2) = v3) % 50.44/7.59 | ~ (sdtpldt0(v0, v3) = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: % 50.44/7.59 any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? [v9: $i] : % 50.44/7.59 (sdtpldt0(v8, v2) = v9 & sdtpldt0(v0, v1) = v8 & aElement0(v2) = v7 & % 50.44/7.59 aElement0(v1) = v6 & aElement0(v0) = v5 & $i(v9) & $i(v8) & ( ~ (v7 = 0) | % 50.44/7.59 ~ (v6 = 0) | ~ (v5 = 0) | v9 = v4))) % 50.44/7.59 % 50.44/7.59 (mAddComm) % 50.44/7.59 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ % 50.44/7.59 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 50.44/7.59 (sdtpldt0(v0, v1) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & $i(v5) & % 50.44/7.59 ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) & ! [v0: $i] : ! [v1: $i] : ! % 50.44/7.59 [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] % 50.44/7.59 : ? [v4: any] : ? [v5: $i] : (sdtpldt0(v1, v0) = v5 & aElement0(v1) = v4 & % 50.44/7.59 aElement0(v0) = v3 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 50.44/7.59 % 50.44/7.59 (mAddInvr) % 50.44/7.59 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ( ~ (smndt0(v0) = v1) | ~ $i(v0) | ? % 50.44/7.59 [v2: any] : ? [v3: $i] : ? [v4: $i] : (sdtpldt0(v1, v0) = v4 & % 50.44/7.59 sdtpldt0(v0, v1) = v3 & aElement0(v0) = v2 & $i(v4) & $i(v3) & ( ~ (v2 = % 50.44/7.59 0) | (v4 = sz00 & v3 = sz00)))) & ! [v0: $i] : ( ~ (aElement0(v0) = % 50.44/7.59 0) | ~ $i(v0) | ? [v1: $i] : (sdtpldt0(v1, v0) = sz00 & sdtpldt0(v0, v1) % 50.44/7.59 = sz00 & smndt0(v0) = v1 & $i(v1))) % 50.44/7.59 % 50.44/7.59 (mAddZero) % 50.83/7.59 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtpldt0(v0, sz00) = v1) | ~ % 50.83/7.59 $i(v0) | ? [v2: any] : ? [v3: $i] : (sdtpldt0(sz00, v0) = v3 & % 50.83/7.60 aElement0(v0) = v2 & $i(v3) & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) & ! % 50.83/7.60 [v0: $i] : ! [v1: $i] : ( ~ (sdtpldt0(sz00, v0) = v1) | ~ $i(v0) | ? [v2: % 50.83/7.60 any] : ? [v3: $i] : (sdtpldt0(v0, sz00) = v3 & aElement0(v0) = v2 & % 50.83/7.60 $i(v3) & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) & ! [v0: $i] : ( ~ % 50.83/7.60 (aElement0(v0) = 0) | ~ $i(v0) | (sdtpldt0(v0, sz00) = v0 & sdtpldt0(sz00, % 50.83/7.60 v0) = v0)) % 50.83/7.60 % 50.83/7.60 (mDefDvs) % 50.83/7.60 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (aDivisorOf0(v1, v0) = % 50.83/7.60 v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? % 50.83/7.60 [v4: any] : (doDivides0(v1, v0) = v4 & aElement0(v1) = v3 & ( ~ (v4 = 0) | % 50.83/7.60 ~ (v3 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ % 50.83/7.60 (doDivides0(v1, v0) = v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | % 50.83/7.60 ? [v3: any] : ? [v4: any] : (aDivisorOf0(v1, v0) = v3 & aElement0(v1) = v4 % 50.83/7.60 & ( ~ (v3 = 0) | (v4 = 0 & v2 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! % 50.83/7.60 [v2: any] : ( ~ (aElement0(v1) = v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ % 50.83/7.60 $i(v0) | ? [v3: any] : ? [v4: any] : (aDivisorOf0(v1, v0) = v3 & % 50.83/7.60 doDivides0(v1, v0) = v4 & ( ~ (v3 = 0) | (v4 = 0 & v2 = 0)))) & ! [v0: % 50.83/7.60 $i] : ! [v1: $i] : ( ~ (aDivisorOf0(v1, v0) = 0) | ~ (aElement0(v0) = 0) | % 50.83/7.60 ~ $i(v1) | ~ $i(v0) | (doDivides0(v1, v0) = 0 & aElement0(v1) = 0)) & ! % 50.83/7.60 [v0: $i] : ! [v1: $i] : ( ~ (doDivides0(v1, v0) = 0) | ~ (aElement0(v0) = 0) % 50.83/7.60 | ~ $i(v1) | ~ $i(v0) | ? [v2: any] : ? [v3: any] : (aDivisorOf0(v1, v0) % 50.83/7.60 = v3 & aElement0(v1) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0: $i] : ! % 50.83/7.60 [v1: $i] : ( ~ (aElement0(v1) = 0) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ % 50.83/7.60 $i(v0) | ? [v2: any] : ? [v3: any] : (aDivisorOf0(v1, v0) = v3 & % 50.83/7.60 doDivides0(v1, v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 50.83/7.60 % 50.83/7.60 (mDivision) % 50.83/7.60 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = sz00 | ~ % 50.83/7.60 (sbrdtbr0(v1) = v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | ? % 50.83/7.60 [v3: int] : ? [v4: $i] : ? [v5: $i] : ? [v6: int] : ? [v7: int] : ? % 50.83/7.60 [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: any] : ($i(v5) & $i(v4) & % 50.83/7.60 ((v9 = v0 & v7 = 0 & v6 = 0 & iLess0(v10, v2) = v11 & sbrdtbr0(v5) = v10 & % 50.83/7.60 sdtasdt0(v4, v1) = v8 & sdtpldt0(v8, v5) = v0 & aElement0(v5) = 0 & % 50.83/7.60 aElement0(v4) = 0 & $i(v10) & $i(v8) & (v11 = 0 | v5 = sz00)) | ( ~ % 50.83/7.60 (v3 = 0) & aElement0(v1) = v3)))) & ! [v0: $i] : ! [v1: $i] : (v1 = % 50.83/7.60 sz00 | ~ (aElement0(v1) = 0) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ % 50.83/7.60 $i(v0) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] % 50.83/7.60 : ? [v7: any] : (iLess0(v6, v2) = v7 & sbrdtbr0(v4) = v6 & sbrdtbr0(v1) = % 50.83/7.60 v2 & sdtasdt0(v3, v1) = v5 & sdtpldt0(v5, v4) = v0 & aElement0(v4) = 0 & % 50.83/7.60 aElement0(v3) = 0 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & (v7 = 0 | % 50.83/7.60 v4 = sz00))) % 50.83/7.60 % 50.83/7.60 (mEucSort) % 50.83/7.61 $i(sz00) & ! [v0: $i] : ! [v1: $i] : (v0 = sz00 | ~ (sbrdtbr0(v0) = v1) | % 50.83/7.61 ~ $i(v0) | ? [v2: any] : ? [v3: any] : (aNaturalNumber0(v1) = v3 & % 50.83/7.61 aElement0(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0: $i] : (v0 = sz00 | % 50.83/7.61 ~ (aElement0(v0) = 0) | ~ $i(v0) | ? [v1: $i] : (sbrdtbr0(v0) = v1 & % 50.83/7.61 aNaturalNumber0(v1) = 0 & $i(v1))) % 50.83/7.61 % 50.83/7.61 (mMulComm) % 50.83/7.61 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v1, v0) = v2) | ~ % 50.83/7.61 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 50.83/7.61 (sdtasdt0(v0, v1) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & $i(v5) & % 50.83/7.61 ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) & ! [v0: $i] : ! [v1: $i] : ! % 50.83/7.61 [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] % 50.83/7.61 : ? [v4: any] : ? [v5: $i] : (sdtasdt0(v1, v0) = v5 & aElement0(v1) = v4 & % 50.83/7.61 aElement0(v0) = v3 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 50.83/7.61 % 50.83/7.61 (mMulMnOne) % 50.83/7.61 $i(sz10) & ? [v0: $i] : (smndt0(sz10) = v0 & $i(v0) & ! [v1: $i] : ! [v2: % 50.83/7.61 $i] : ( ~ (sdtasdt0(v1, v0) = v2) | ~ $i(v1) | ? [v3: any] : ? [v4: $i] % 50.83/7.61 : ? [v5: $i] : (sdtasdt0(v0, v1) = v4 & smndt0(v1) = v5 & aElement0(v1) = % 50.83/7.61 v3 & $i(v5) & $i(v4) & ( ~ (v3 = 0) | (v5 = v2 & v4 = v2)))) & ! [v1: % 50.83/7.61 $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ $i(v1) | ? [v3: any] % 50.83/7.61 : ? [v4: $i] : ? [v5: $i] : (sdtasdt0(v1, v0) = v5 & smndt0(v1) = v4 & % 50.83/7.61 aElement0(v1) = v3 & $i(v5) & $i(v4) & ( ~ (v3 = 0) | (v5 = v2 & v4 = % 50.83/7.61 v2)))) & ! [v1: $i] : ! [v2: $i] : ( ~ (smndt0(v1) = v2) | ~ % 50.83/7.61 $i(v1) | ? [v3: any] : ? [v4: $i] : ? [v5: $i] : (sdtasdt0(v1, v0) = v5 % 50.83/7.61 & sdtasdt0(v0, v1) = v4 & aElement0(v1) = v3 & $i(v5) & $i(v4) & ( ~ (v3 % 50.83/7.61 = 0) | (v5 = v2 & v4 = v2)))) & ! [v1: $i] : ( ~ (aElement0(v1) = % 50.83/7.61 0) | ~ $i(v1) | ? [v2: $i] : (sdtasdt0(v1, v0) = v2 & sdtasdt0(v0, v1) % 50.83/7.61 = v2 & smndt0(v1) = v2 & $i(v2)))) % 50.83/7.61 % 50.83/7.61 (mSortsB) % 50.83/7.61 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 50.83/7.61 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 50.83/7.61 (aElement0(v2) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & ( ~ (v4 = 0) % 50.83/7.61 | ~ (v3 = 0) | v5 = 0))) % 50.83/7.61 % 50.83/7.61 (mSortsB_02) % 50.83/7.61 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 50.83/7.61 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 50.83/7.61 (aElement0(v2) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & ( ~ (v4 = 0) % 50.83/7.61 | ~ (v3 = 0) | v5 = 0))) % 50.83/7.61 % 50.83/7.61 (mSortsU) % 50.83/7.61 ! [v0: $i] : ! [v1: $i] : ( ~ (smndt0(v0) = v1) | ~ $i(v0) | ? [v2: any] : % 50.83/7.61 ? [v3: any] : (aElement0(v1) = v3 & aElement0(v0) = v2 & ( ~ (v2 = 0) | v3 % 50.83/7.61 = 0))) & ! [v0: $i] : ( ~ (aElement0(v0) = 0) | ~ $i(v0) | ? [v1: $i] % 50.83/7.61 : (smndt0(v0) = v1 & aElement0(v1) = 0 & $i(v1))) % 50.83/7.61 % 50.83/7.61 (m__) % 50.83/7.62 $i(xr) & $i(xq) & $i(xu) & $i(xb) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 50.83/7.62 ( ~ (v2 = xr) & sdtasdt0(xq, xu) = v0 & sdtpldt0(v1, xb) = v2 & smndt0(v0) = % 50.83/7.62 v1 & $i(v2) & $i(v1) & $i(v0)) % 50.83/7.62 % 50.83/7.62 (m__2091) % 50.83/7.62 aElement0(xb) = 0 & aElement0(xa) = 0 & $i(xb) & $i(xa) % 50.83/7.62 % 50.83/7.62 (m__2273) % 50.83/7.62 $i(xu) & $i(xI) & $i(sz00) & ? [v0: $i] : ( ~ (xu = sz00) & sbrdtbr0(xu) = v0 % 50.83/7.62 & aElementOf0(xu, xI) = 0 & $i(v0) & ! [v1: $i] : ! [v2: $i] : (v1 = sz00 % 50.83/7.62 | ~ (sbrdtbr0(v1) = v2) | ~ $i(v1) | ? [v3: any] : ? [v4: any] : % 50.83/7.62 (iLess0(v2, v0) = v4 & aElementOf0(v1, xI) = v3 & ( ~ (v4 = 0) | ~ (v3 = % 50.83/7.62 0)))) & ! [v1: $i] : (v1 = sz00 | ~ (aElementOf0(v1, xI) = 0) | ~ % 50.83/7.62 $i(v1) | ? [v2: $i] : ? [v3: int] : ( ~ (v3 = 0) & iLess0(v2, v0) = v3 & % 50.83/7.62 sbrdtbr0(v1) = v2 & $i(v2)))) % 50.83/7.62 % 50.83/7.62 (m__2416) % 50.83/7.62 $i(xu) & $i(xb) & $i(xa) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 50.83/7.62 $i] : (sdtasdt0(xb, v1) = v3 & sdtasdt0(xa, v0) = v2 & sdtpldt0(v2, v3) = xu % 50.83/7.62 & aElement0(v1) = 0 & aElement0(v0) = 0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 50.83/7.62 % 50.83/7.62 (m__2479) % 50.83/7.62 doDivides0(xu, xa) = 0 & $i(xu) & $i(xa) % 50.83/7.62 % 50.83/7.62 (m__2666) % 50.83/7.62 $i(xr) & $i(xq) & $i(xu) & $i(xb) & $i(sz00) & ? [v0: $i] : ? [v1: $i] : ? % 50.83/7.62 [v2: $i] : ? [v3: any] : (iLess0(v1, v2) = v3 & sbrdtbr0(xr) = v1 & % 50.83/7.62 sbrdtbr0(xu) = v2 & sdtasdt0(xq, xu) = v0 & sdtpldt0(v0, xr) = xb & % 50.83/7.62 aElement0(xr) = 0 & aElement0(xq) = 0 & $i(v2) & $i(v1) & $i(v0) & (v3 = 0 | % 50.83/7.62 xr = sz00)) % 50.83/7.62 % 50.83/7.62 (m__2673) % 50.83/7.62 ~ (xr = sz00) & $i(xr) & $i(sz00) % 50.83/7.62 % 50.83/7.62 (m__2690) % 50.83/7.62 $i(xq) & $i(xu) & $i(xI) & ? [v0: $i] : ? [v1: $i] : (aElementOf0(v1, xI) = % 50.83/7.62 0 & sdtasdt0(xq, xu) = v0 & smndt0(v0) = v1 & $i(v1) & $i(v0)) % 50.83/7.62 % 50.83/7.62 (function-axioms) % 50.83/7.63 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 50.83/7.63 [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (aGcdOfAnd0(v4, v3, v2) = v1) | ~ % 50.83/7.63 (aGcdOfAnd0(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 50.83/7.63 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 50.83/7.63 (sdteqdtlpzmzozddtrp0(v4, v3, v2) = v1) | ~ (sdteqdtlpzmzozddtrp0(v4, v3, % 50.83/7.63 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 50.83/7.63 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (misRelativelyPrime0(v3, v2) = v1) | % 50.83/7.63 ~ (misRelativelyPrime0(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 50.83/7.63 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 50.83/7.63 (aDivisorOf0(v3, v2) = v1) | ~ (aDivisorOf0(v3, v2) = v0)) & ! [v0: % 50.83/7.63 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 50.83/7.63 : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ (doDivides0(v3, v2) = v0)) & ! % 50.83/7.63 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 50.83/7.63 $i] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) & ! % 50.83/7.63 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 50.83/7.63 (sdtasasdt0(v3, v2) = v1) | ~ (sdtasasdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 50.83/7.63 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtpldt1(v3, v2) = v1) | % 50.83/7.63 ~ (sdtpldt1(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 50.83/7.63 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 50.83/7.63 (aElementOf0(v3, v2) = v1) | ~ (aElementOf0(v3, v2) = v0)) & ! [v0: $i] : % 50.83/7.63 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) % 50.83/7.63 | ~ (sdtasdt0(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 50.83/7.63 [v3: $i] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 50.83/7.63 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (slsdtgt0(v2) = v1) % 50.83/7.63 | ~ (slsdtgt0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = % 50.83/7.63 v0 | ~ (sbrdtbr0(v2) = v1) | ~ (sbrdtbr0(v2) = v0)) & ! [v0: % 50.83/7.63 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 50.83/7.63 ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = v0)) & ! [v0: % 50.83/7.63 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 50.83/7.63 ~ (aIdeal0(v2) = v1) | ~ (aIdeal0(v2) = v0)) & ! [v0: MultipleValueBool] : % 50.83/7.63 ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aSet0(v2) = v1) | ~ % 50.83/7.63 (aSet0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 50.83/7.63 (smndt0(v2) = v1) | ~ (smndt0(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 50.83/7.63 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aElement0(v2) = v1) | % 50.83/7.63 ~ (aElement0(v2) = v0)) % 50.83/7.63 % 50.83/7.63 Further assumptions not needed in the proof: % 50.83/7.63 -------------------------------------------- % 50.83/7.63 mCancel, mChineseRemainder, mDefDiv, mDefGCD, mDefIdeal, mDefMod, mDefPrIdeal, % 50.83/7.63 mDefRel, mDefSInt, mDefSSum, mEOfElem, mElmSort, mIdeInt, mIdeSum, mMulAsso, % 50.83/7.63 mMulUnit, mMulZero, mNatLess, mNatSort, mPrIdeal, mSetEq, mSetSort, mSortsC, % 50.83/7.63 mSortsC_01, mUnNeZr, m__2110, m__2129, m__2174, m__2203, m__2228, m__2383, % 50.83/7.63 m__2612, m__2699 % 50.83/7.63 % 50.83/7.63 Those formulas are unsatisfiable: % 50.83/7.63 --------------------------------- % 50.83/7.63 % 50.83/7.63 Begin of proof % 50.83/7.63 | % 50.83/7.63 | ALPHA: (mSortsU) implies: % 50.83/7.63 | (1) ! [v0: $i] : ! [v1: $i] : ( ~ (smndt0(v0) = v1) | ~ $i(v0) | ? [v2: % 50.83/7.63 | any] : ? [v3: any] : (aElement0(v1) = v3 & aElement0(v0) = v2 & ( % 50.83/7.63 | ~ (v2 = 0) | v3 = 0))) % 50.83/7.63 | % 50.83/7.63 | ALPHA: (mAddComm) implies: % 50.83/7.63 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | % 50.83/7.63 | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 50.83/7.63 | (sdtpldt0(v1, v0) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & % 50.83/7.63 | $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 50.83/7.64 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v1, v0) = v2) | % 50.83/7.64 | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 50.83/7.64 | (sdtpldt0(v0, v1) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & % 50.83/7.64 | $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 50.83/7.64 | % 50.83/7.64 | ALPHA: (mAddAsso) implies: % 50.83/7.64 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 50.83/7.64 | ~ (sdtpldt0(v1, v2) = v3) | ~ (sdtpldt0(v0, v3) = v4) | ~ $i(v2) | % 50.83/7.64 | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : % 50.83/7.64 | ? [v8: $i] : ? [v9: $i] : (sdtpldt0(v8, v2) = v9 & sdtpldt0(v0, v1) % 50.83/7.64 | = v8 & aElement0(v2) = v7 & aElement0(v1) = v6 & aElement0(v0) = v5 % 50.83/7.64 | & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v9 = % 50.83/7.64 | v4))) % 50.83/7.64 | % 50.83/7.64 | ALPHA: (mAddZero) implies: % 50.83/7.64 | (5) ! [v0: $i] : ( ~ (aElement0(v0) = 0) | ~ $i(v0) | (sdtpldt0(v0, sz00) % 50.83/7.64 | = v0 & sdtpldt0(sz00, v0) = v0)) % 50.83/7.64 | % 50.83/7.64 | ALPHA: (mAddInvr) implies: % 50.83/7.64 | (6) ! [v0: $i] : ! [v1: $i] : ( ~ (smndt0(v0) = v1) | ~ $i(v0) | ? [v2: % 50.83/7.64 | any] : ? [v3: $i] : ? [v4: $i] : (sdtpldt0(v1, v0) = v4 & % 50.83/7.64 | sdtpldt0(v0, v1) = v3 & aElement0(v0) = v2 & $i(v4) & $i(v3) & ( ~ % 50.83/7.64 | (v2 = 0) | (v4 = sz00 & v3 = sz00)))) % 50.83/7.64 | % 50.83/7.64 | ALPHA: (mMulComm) implies: % 50.83/7.64 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | % 50.83/7.64 | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 50.83/7.64 | (sdtasdt0(v1, v0) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & % 50.83/7.64 | $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 50.83/7.64 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v1, v0) = v2) | % 50.83/7.64 | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 50.83/7.64 | (sdtasdt0(v0, v1) = v5 & aElement0(v1) = v4 & aElement0(v0) = v3 & % 50.83/7.64 | $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 50.83/7.64 | % 50.83/7.64 | ALPHA: (mAMDistr) implies: % 50.83/7.64 | (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 50.83/7.64 | ~ (sdtasdt0(v0, v3) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ $i(v2) | % 50.83/7.64 | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : % 50.83/7.64 | ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] % 50.83/7.64 | : ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v3, v0) = v11 & % 50.83/7.64 | sdtasdt0(v2, v0) = v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v2) % 50.83/7.64 | = v9 & sdtasdt0(v0, v1) = v8 & sdtpldt0(v12, v13) = v14 & % 50.83/7.64 | sdtpldt0(v8, v9) = v10 & aElement0(v2) = v7 & aElement0(v1) = v6 & % 50.83/7.64 | aElement0(v0) = v5 & $i(v14) & $i(v13) & $i(v12) & $i(v11) & % 50.83/7.64 | $i(v10) & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = % 50.83/7.64 | 0) | (v14 = v11 & v10 = v4)))) % 50.83/7.65 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 50.83/7.65 | ( ~ (sdtasdt0(v3, v0) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ $i(v2) | % 50.83/7.65 | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : % 50.83/7.65 | ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: % 50.83/7.65 | $i] : ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v2, v0) = v13 & % 50.83/7.65 | sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v3) = v8 & sdtasdt0(v0, v2) % 50.83/7.65 | = v10 & sdtasdt0(v0, v1) = v9 & sdtpldt0(v12, v13) = v14 & % 50.83/7.65 | sdtpldt0(v9, v10) = v11 & aElement0(v2) = v7 & aElement0(v1) = v6 % 50.83/7.65 | & aElement0(v0) = v5 & $i(v14) & $i(v13) & $i(v12) & $i(v11) & % 50.83/7.65 | $i(v10) & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = % 50.83/7.65 | 0) | (v14 = v4 & v11 = v8)))) % 50.83/7.65 | % 50.83/7.65 | ALPHA: (mMulMnOne) implies: % 50.83/7.65 | (11) ? [v0: $i] : (smndt0(sz10) = v0 & $i(v0) & ! [v1: $i] : ! [v2: $i] % 50.83/7.65 | : ( ~ (sdtasdt0(v1, v0) = v2) | ~ $i(v1) | ? [v3: any] : ? [v4: % 50.83/7.65 | $i] : ? [v5: $i] : (sdtasdt0(v0, v1) = v4 & smndt0(v1) = v5 & % 50.83/7.65 | aElement0(v1) = v3 & $i(v5) & $i(v4) & ( ~ (v3 = 0) | (v5 = v2 & % 50.83/7.65 | v4 = v2)))) & ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, % 50.83/7.65 | v1) = v2) | ~ $i(v1) | ? [v3: any] : ? [v4: $i] : ? [v5: % 50.83/7.65 | $i] : (sdtasdt0(v1, v0) = v5 & smndt0(v1) = v4 & aElement0(v1) = % 50.83/7.65 | v3 & $i(v5) & $i(v4) & ( ~ (v3 = 0) | (v5 = v2 & v4 = v2)))) & % 50.83/7.65 | ! [v1: $i] : ! [v2: $i] : ( ~ (smndt0(v1) = v2) | ~ $i(v1) | ? % 50.83/7.65 | [v3: any] : ? [v4: $i] : ? [v5: $i] : (sdtasdt0(v1, v0) = v5 & % 50.83/7.65 | sdtasdt0(v0, v1) = v4 & aElement0(v1) = v3 & $i(v5) & $i(v4) & ( % 50.83/7.65 | ~ (v3 = 0) | (v5 = v2 & v4 = v2)))) & ! [v1: $i] : ( ~ % 50.83/7.65 | (aElement0(v1) = 0) | ~ $i(v1) | ? [v2: $i] : (sdtasdt0(v1, v0) % 50.83/7.65 | = v2 & sdtasdt0(v0, v1) = v2 & smndt0(v1) = v2 & $i(v2)))) % 50.83/7.65 | % 50.83/7.65 | ALPHA: (mEucSort) implies: % 50.83/7.65 | (12) ! [v0: $i] : ! [v1: $i] : (v0 = sz00 | ~ (sbrdtbr0(v0) = v1) | ~ % 50.83/7.65 | $i(v0) | ? [v2: any] : ? [v3: any] : (aNaturalNumber0(v1) = v3 & % 50.83/7.65 | aElement0(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 50.83/7.65 | % 50.83/7.65 | ALPHA: (mDivision) implies: % 50.83/7.65 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = sz00 | ~ % 50.83/7.65 | (sbrdtbr0(v1) = v2) | ~ (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) % 50.83/7.65 | | ? [v3: int] : ? [v4: $i] : ? [v5: $i] : ? [v6: int] : ? [v7: % 50.83/7.65 | int] : ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: any] : % 50.83/7.65 | ($i(v5) & $i(v4) & ((v9 = v0 & v7 = 0 & v6 = 0 & iLess0(v10, v2) = % 50.83/7.65 | v11 & sbrdtbr0(v5) = v10 & sdtasdt0(v4, v1) = v8 & % 50.83/7.65 | sdtpldt0(v8, v5) = v0 & aElement0(v5) = 0 & aElement0(v4) = 0 % 50.83/7.65 | & $i(v10) & $i(v8) & (v11 = 0 | v5 = sz00)) | ( ~ (v3 = 0) & % 50.83/7.65 | aElement0(v1) = v3)))) % 50.83/7.65 | % 50.83/7.65 | ALPHA: (mDefDvs) implies: % 50.83/7.65 | (14) ! [v0: $i] : ! [v1: $i] : ( ~ (doDivides0(v1, v0) = 0) | ~ % 50.83/7.65 | (aElement0(v0) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: any] : ? [v3: % 50.83/7.65 | any] : (aDivisorOf0(v1, v0) = v3 & aElement0(v1) = v2 & ( ~ (v2 = % 50.83/7.65 | 0) | v3 = 0))) % 50.83/7.65 | % 50.83/7.65 | ALPHA: (m__2091) implies: % 50.83/7.65 | (15) aElement0(xa) = 0 % 50.83/7.65 | (16) aElement0(xb) = 0 % 50.83/7.65 | % 50.83/7.65 | ALPHA: (m__2273) implies: % 50.83/7.65 | (17) ? [v0: $i] : ( ~ (xu = sz00) & sbrdtbr0(xu) = v0 & aElementOf0(xu, % 50.83/7.65 | xI) = 0 & $i(v0) & ! [v1: $i] : ! [v2: $i] : (v1 = sz00 | ~ % 50.83/7.65 | (sbrdtbr0(v1) = v2) | ~ $i(v1) | ? [v3: any] : ? [v4: any] : % 50.83/7.65 | (iLess0(v2, v0) = v4 & aElementOf0(v1, xI) = v3 & ( ~ (v4 = 0) | % 50.83/7.65 | ~ (v3 = 0)))) & ! [v1: $i] : (v1 = sz00 | ~ (aElementOf0(v1, % 50.83/7.65 | xI) = 0) | ~ $i(v1) | ? [v2: $i] : ? [v3: int] : ( ~ (v3 = % 50.83/7.65 | 0) & iLess0(v2, v0) = v3 & sbrdtbr0(v1) = v2 & $i(v2)))) % 50.83/7.65 | % 50.83/7.65 | ALPHA: (m__2416) implies: % 50.83/7.65 | (18) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (sdtasdt0(xb, % 50.83/7.66 | v1) = v3 & sdtasdt0(xa, v0) = v2 & sdtpldt0(v2, v3) = xu & % 50.83/7.66 | aElement0(v1) = 0 & aElement0(v0) = 0 & $i(v3) & $i(v2) & $i(v1) & % 50.83/7.66 | $i(v0)) % 50.83/7.66 | % 50.83/7.66 | ALPHA: (m__2479) implies: % 50.83/7.66 | (19) $i(xa) % 50.83/7.66 | (20) doDivides0(xu, xa) = 0 % 50.83/7.66 | % 50.83/7.66 | ALPHA: (m__2666) implies: % 50.83/7.66 | (21) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: any] : (iLess0(v1, % 50.83/7.66 | v2) = v3 & sbrdtbr0(xr) = v1 & sbrdtbr0(xu) = v2 & sdtasdt0(xq, % 50.83/7.66 | xu) = v0 & sdtpldt0(v0, xr) = xb & aElement0(xr) = 0 & % 50.83/7.66 | aElement0(xq) = 0 & $i(v2) & $i(v1) & $i(v0) & (v3 = 0 | xr = sz00)) % 50.83/7.66 | % 50.83/7.66 | ALPHA: (m__2673) implies: % 50.83/7.66 | (22) ~ (xr = sz00) % 50.83/7.66 | % 50.83/7.66 | ALPHA: (m__2690) implies: % 50.83/7.66 | (23) ? [v0: $i] : ? [v1: $i] : (aElementOf0(v1, xI) = 0 & sdtasdt0(xq, % 50.83/7.66 | xu) = v0 & smndt0(v0) = v1 & $i(v1) & $i(v0)) % 50.83/7.66 | % 50.83/7.66 | ALPHA: (m__) implies: % 50.83/7.66 | (24) $i(xb) % 50.83/7.66 | (25) $i(xu) % 50.83/7.66 | (26) $i(xq) % 50.83/7.66 | (27) $i(xr) % 50.83/7.66 | (28) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ( ~ (v2 = xr) & sdtasdt0(xq, % 50.83/7.66 | xu) = v0 & sdtpldt0(v1, xb) = v2 & smndt0(v0) = v1 & $i(v2) & % 50.83/7.66 | $i(v1) & $i(v0)) % 50.83/7.66 | % 50.83/7.66 | ALPHA: (function-axioms) implies: % 50.83/7.66 | (29) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 50.83/7.66 | : (v1 = v0 | ~ (aElement0(v2) = v1) | ~ (aElement0(v2) = v0)) % 50.83/7.66 | (30) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (smndt0(v2) = % 50.83/7.66 | v1) | ~ (smndt0(v2) = v0)) % 50.83/7.66 | (31) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (sbrdtbr0(v2) % 50.83/7.66 | = v1) | ~ (sbrdtbr0(v2) = v0)) % 50.83/7.66 | (32) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 50.83/7.66 | (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 50.83/7.66 | (33) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 50.83/7.66 | (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 50.83/7.66 | % 50.83/7.66 | DELTA: instantiating (23) with fresh symbols all_38_0, all_38_1 gives: % 50.83/7.66 | (34) aElementOf0(all_38_0, xI) = 0 & sdtasdt0(xq, xu) = all_38_1 & % 50.83/7.66 | smndt0(all_38_1) = all_38_0 & $i(all_38_0) & $i(all_38_1) % 50.83/7.66 | % 50.83/7.66 | ALPHA: (34) implies: % 50.83/7.66 | (35) smndt0(all_38_1) = all_38_0 % 50.83/7.66 | (36) sdtasdt0(xq, xu) = all_38_1 % 50.83/7.66 | % 50.83/7.66 | DELTA: instantiating (28) with fresh symbols all_42_0, all_42_1, all_42_2 % 50.83/7.66 | gives: % 50.83/7.66 | (37) ~ (all_42_0 = xr) & sdtasdt0(xq, xu) = all_42_2 & sdtpldt0(all_42_1, % 50.83/7.66 | xb) = all_42_0 & smndt0(all_42_2) = all_42_1 & $i(all_42_0) & % 50.83/7.66 | $i(all_42_1) & $i(all_42_2) % 50.83/7.66 | % 50.83/7.66 | ALPHA: (37) implies: % 50.83/7.66 | (38) ~ (all_42_0 = xr) % 50.83/7.66 | (39) $i(all_42_2) % 50.83/7.66 | (40) $i(all_42_1) % 50.83/7.66 | (41) smndt0(all_42_2) = all_42_1 % 50.83/7.66 | (42) sdtpldt0(all_42_1, xb) = all_42_0 % 50.83/7.66 | (43) sdtasdt0(xq, xu) = all_42_2 % 50.83/7.66 | % 50.83/7.66 | DELTA: instantiating (18) with fresh symbols all_46_0, all_46_1, all_46_2, % 50.83/7.66 | all_46_3 gives: % 50.83/7.66 | (44) sdtasdt0(xb, all_46_2) = all_46_0 & sdtasdt0(xa, all_46_3) = all_46_1 % 50.83/7.66 | & sdtpldt0(all_46_1, all_46_0) = xu & aElement0(all_46_2) = 0 & % 50.83/7.66 | aElement0(all_46_3) = 0 & $i(all_46_0) & $i(all_46_1) & $i(all_46_2) & % 50.83/7.66 | $i(all_46_3) % 50.83/7.66 | % 50.83/7.66 | ALPHA: (44) implies: % 50.83/7.66 | (45) $i(all_46_3) % 50.83/7.66 | (46) $i(all_46_2) % 50.83/7.66 | (47) $i(all_46_1) % 50.83/7.66 | (48) $i(all_46_0) % 50.83/7.66 | (49) aElement0(all_46_3) = 0 % 50.83/7.66 | (50) aElement0(all_46_2) = 0 % 50.83/7.66 | (51) sdtpldt0(all_46_1, all_46_0) = xu % 50.83/7.66 | (52) sdtasdt0(xa, all_46_3) = all_46_1 % 50.83/7.66 | (53) sdtasdt0(xb, all_46_2) = all_46_0 % 50.83/7.66 | % 50.83/7.66 | DELTA: instantiating (21) with fresh symbols all_50_0, all_50_1, all_50_2, % 50.83/7.66 | all_50_3 gives: % 50.83/7.67 | (54) iLess0(all_50_2, all_50_1) = all_50_0 & sbrdtbr0(xr) = all_50_2 & % 50.83/7.67 | sbrdtbr0(xu) = all_50_1 & sdtasdt0(xq, xu) = all_50_3 & % 50.83/7.67 | sdtpldt0(all_50_3, xr) = xb & aElement0(xr) = 0 & aElement0(xq) = 0 & % 50.83/7.67 | $i(all_50_1) & $i(all_50_2) & $i(all_50_3) & (all_50_0 = 0 | xr = % 50.83/7.67 | sz00) % 50.83/7.67 | % 50.83/7.67 | ALPHA: (54) implies: % 50.83/7.67 | (55) aElement0(xq) = 0 % 50.83/7.67 | (56) aElement0(xr) = 0 % 50.83/7.67 | (57) sdtpldt0(all_50_3, xr) = xb % 50.83/7.67 | (58) sdtasdt0(xq, xu) = all_50_3 % 50.83/7.67 | (59) sbrdtbr0(xu) = all_50_1 % 50.83/7.67 | (60) sbrdtbr0(xr) = all_50_2 % 50.83/7.67 | % 50.83/7.67 | DELTA: instantiating (17) with fresh symbol all_52_0 gives: % 50.83/7.67 | (61) ~ (xu = sz00) & sbrdtbr0(xu) = all_52_0 & aElementOf0(xu, xI) = 0 & % 50.83/7.67 | $i(all_52_0) & ! [v0: $i] : ! [v1: $i] : (v0 = sz00 | ~ % 50.83/7.67 | (sbrdtbr0(v0) = v1) | ~ $i(v0) | ? [v2: any] : ? [v3: any] : % 50.83/7.67 | (iLess0(v1, all_52_0) = v3 & aElementOf0(v0, xI) = v2 & ( ~ (v3 = 0) % 50.83/7.67 | | ~ (v2 = 0)))) & ! [v0: $i] : (v0 = sz00 | ~ % 50.83/7.67 | (aElementOf0(v0, xI) = 0) | ~ $i(v0) | ? [v1: $i] : ? [v2: int] : % 50.83/7.67 | ( ~ (v2 = 0) & iLess0(v1, all_52_0) = v2 & sbrdtbr0(v0) = v1 & % 50.83/7.67 | $i(v1))) % 50.83/7.67 | % 50.83/7.67 | ALPHA: (61) implies: % 50.83/7.67 | (62) ~ (xu = sz00) % 50.83/7.67 | (63) sbrdtbr0(xu) = all_52_0 % 50.83/7.67 | % 50.83/7.67 | DELTA: instantiating (11) with fresh symbol all_55_0 gives: % 50.83/7.67 | (64) smndt0(sz10) = all_55_0 & $i(all_55_0) & ! [v0: $i] : ! [v1: $i] : ( % 50.83/7.67 | ~ (sdtasdt0(v0, all_55_0) = v1) | ~ $i(v0) | ? [v2: any] : ? [v3: % 50.83/7.67 | $i] : ? [v4: $i] : (sdtasdt0(all_55_0, v0) = v3 & smndt0(v0) = v4 % 50.83/7.67 | & aElement0(v0) = v2 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | (v4 = v1 & % 50.83/7.67 | v3 = v1)))) & ! [v0: $i] : ! [v1: $i] : ( ~ % 50.83/7.67 | (sdtasdt0(all_55_0, v0) = v1) | ~ $i(v0) | ? [v2: any] : ? [v3: % 50.83/7.67 | $i] : ? [v4: $i] : (sdtasdt0(v0, all_55_0) = v4 & smndt0(v0) = v3 % 50.83/7.67 | & aElement0(v0) = v2 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | (v4 = v1 & % 50.83/7.67 | v3 = v1)))) & ! [v0: $i] : ! [v1: $i] : ( ~ (smndt0(v0) = % 50.83/7.67 | v1) | ~ $i(v0) | ? [v2: any] : ? [v3: $i] : ? [v4: $i] : % 50.83/7.67 | (sdtasdt0(v0, all_55_0) = v4 & sdtasdt0(all_55_0, v0) = v3 & % 50.83/7.67 | aElement0(v0) = v2 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | (v4 = v1 & % 50.83/7.67 | v3 = v1)))) & ! [v0: $i] : ( ~ (aElement0(v0) = 0) | ~ % 50.83/7.67 | $i(v0) | ? [v1: $i] : (sdtasdt0(v0, all_55_0) = v1 & % 50.83/7.67 | sdtasdt0(all_55_0, v0) = v1 & smndt0(v0) = v1 & $i(v1))) % 50.83/7.67 | % 50.83/7.67 | ALPHA: (64) implies: % 50.83/7.67 | (65) ! [v0: $i] : ! [v1: $i] : ( ~ (smndt0(v0) = v1) | ~ $i(v0) | ? % 50.83/7.67 | [v2: any] : ? [v3: $i] : ? [v4: $i] : (sdtasdt0(v0, all_55_0) = v4 % 50.83/7.67 | & sdtasdt0(all_55_0, v0) = v3 & aElement0(v0) = v2 & $i(v4) & % 50.83/7.67 | $i(v3) & ( ~ (v2 = 0) | (v4 = v1 & v3 = v1)))) % 50.83/7.67 | % 50.83/7.67 | GROUND_INST: instantiating (33) with all_42_2, all_50_3, xu, xq, simplifying % 50.83/7.67 | with (43), (58) gives: % 50.83/7.67 | (66) all_50_3 = all_42_2 % 50.83/7.67 | % 50.83/7.67 | GROUND_INST: instantiating (33) with all_38_1, all_50_3, xu, xq, simplifying % 50.83/7.67 | with (36), (58) gives: % 50.83/7.67 | (67) all_50_3 = all_38_1 % 50.83/7.67 | % 50.83/7.67 | GROUND_INST: instantiating (31) with all_50_1, all_52_0, xu, simplifying with % 50.83/7.67 | (59), (63) gives: % 50.83/7.67 | (68) all_52_0 = all_50_1 % 50.83/7.67 | % 50.83/7.67 | COMBINE_EQS: (66), (67) imply: % 50.83/7.67 | (69) all_42_2 = all_38_1 % 50.83/7.67 | % 50.83/7.67 | REDUCE: (57), (67) imply: % 50.83/7.67 | (70) sdtpldt0(all_38_1, xr) = xb % 50.83/7.67 | % 50.83/7.67 | REDUCE: (41), (69) imply: % 50.83/7.67 | (71) smndt0(all_38_1) = all_42_1 % 50.83/7.67 | % 50.83/7.67 | REDUCE: (39), (69) imply: % 50.83/7.67 | (72) $i(all_38_1) % 50.83/7.67 | % 50.83/7.67 | GROUND_INST: instantiating (30) with all_38_0, all_42_1, all_38_1, simplifying % 50.83/7.67 | with (35), (71) gives: % 50.83/7.67 | (73) all_42_1 = all_38_0 % 50.83/7.67 | % 50.83/7.67 | REDUCE: (42), (73) imply: % 50.83/7.67 | (74) sdtpldt0(all_38_0, xb) = all_42_0 % 50.83/7.67 | % 50.83/7.67 | REDUCE: (40), (73) imply: % 50.83/7.67 | (75) $i(all_38_0) % 50.83/7.67 | % 50.83/7.67 | GROUND_INST: instantiating (5) with xr, simplifying with (27), (56) gives: % 50.83/7.67 | (76) sdtpldt0(xr, sz00) = xr & sdtpldt0(sz00, xr) = xr % 50.83/7.67 | % 50.83/7.67 | ALPHA: (76) implies: % 50.83/7.67 | (77) sdtpldt0(sz00, xr) = xr % 50.83/7.67 | % 50.83/7.67 | GROUND_INST: instantiating (65) with all_38_1, all_38_0, simplifying with % 50.83/7.67 | (35), (72) gives: % 50.83/7.67 | (78) ? [v0: any] : ? [v1: $i] : ? [v2: $i] : (sdtasdt0(all_55_0, % 50.83/7.67 | all_38_1) = v1 & sdtasdt0(all_38_1, all_55_0) = v2 & % 50.83/7.67 | aElement0(all_38_1) = v0 & $i(v2) & $i(v1) & ( ~ (v0 = 0) | (v2 = % 50.83/7.67 | all_38_0 & v1 = all_38_0))) % 50.83/7.67 | % 50.83/7.68 | GROUND_INST: instantiating (6) with all_38_1, all_38_0, simplifying with (35), % 50.83/7.68 | (72) gives: % 50.83/7.68 | (79) ? [v0: any] : ? [v1: $i] : ? [v2: $i] : (sdtpldt0(all_38_0, % 50.83/7.68 | all_38_1) = v2 & sdtpldt0(all_38_1, all_38_0) = v1 & % 50.83/7.68 | aElement0(all_38_1) = v0 & $i(v2) & $i(v1) & ( ~ (v0 = 0) | (v2 = % 50.83/7.68 | sz00 & v1 = sz00))) % 50.83/7.68 | % 50.83/7.68 | GROUND_INST: instantiating (1) with all_38_1, all_38_0, simplifying with (35), % 50.83/7.68 | (72) gives: % 50.83/7.68 | (80) ? [v0: any] : ? [v1: any] : (aElement0(all_38_0) = v1 & % 50.83/7.68 | aElement0(all_38_1) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 50.83/7.68 | % 50.83/7.68 | GROUND_INST: instantiating (3) with xr, all_38_1, xb, simplifying with (27), % 50.83/7.68 | (70), (72) gives: % 50.83/7.68 | (81) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xr, all_38_1) = % 50.83/7.68 | v2 & aElement0(all_38_1) = v1 & aElement0(xr) = v0 & $i(v2) & ( ~ % 50.83/7.68 | (v1 = 0) | ~ (v0 = 0) | v2 = xb)) % 50.83/7.68 | % 50.83/7.68 | GROUND_INST: instantiating (2) with all_38_1, xr, xb, simplifying with (27), % 50.83/7.68 | (70), (72) gives: % 50.83/7.68 | (82) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xr, all_38_1) = % 50.83/7.68 | v2 & aElement0(all_38_1) = v0 & aElement0(xr) = v1 & $i(v2) & ( ~ % 50.83/7.68 | (v1 = 0) | ~ (v0 = 0) | v2 = xb)) % 50.83/7.68 | % 50.83/7.68 | GROUND_INST: instantiating (mSortsB) with all_38_1, xr, xb, simplifying with % 50.83/7.68 | (27), (70), (72) gives: % 50.83/7.68 | (83) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_38_1) = v0 % 50.83/7.68 | & aElement0(xr) = v1 & aElement0(xb) = v2 & ( ~ (v1 = 0) | ~ (v0 = % 50.83/7.68 | 0) | v2 = 0)) % 50.83/7.68 | % 50.83/7.68 | GROUND_INST: instantiating (4) with all_38_0, all_38_1, xr, xb, all_42_0, % 50.83/7.68 | simplifying with (27), (70), (72), (74), (75) gives: % 50.83/7.68 | (84) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: $i] % 50.83/7.68 | : (sdtpldt0(v3, xr) = v4 & sdtpldt0(all_38_0, all_38_1) = v3 & % 50.83/7.68 | aElement0(all_38_0) = v0 & aElement0(all_38_1) = v1 & aElement0(xr) % 50.83/7.68 | = v2 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | % 50.83/7.68 | v4 = all_42_0)) % 50.83/7.68 | % 50.83/7.68 | GROUND_INST: instantiating (3) with xb, all_38_0, all_42_0, simplifying with % 50.83/7.68 | (24), (74), (75) gives: % 50.83/7.68 | (85) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xb, all_38_0) = % 50.83/7.68 | v2 & aElement0(all_38_0) = v1 & aElement0(xb) = v0 & $i(v2) & ( ~ % 50.83/7.68 | (v1 = 0) | ~ (v0 = 0) | v2 = all_42_0)) % 50.83/7.68 | % 50.83/7.68 | GROUND_INST: instantiating (2) with all_38_0, xb, all_42_0, simplifying with % 50.83/7.68 | (24), (74), (75) gives: % 50.83/7.68 | (86) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xb, all_38_0) = % 50.83/7.68 | v2 & aElement0(all_38_0) = v0 & aElement0(xb) = v1 & $i(v2) & ( ~ % 50.83/7.68 | (v1 = 0) | ~ (v0 = 0) | v2 = all_42_0)) % 50.83/7.68 | % 50.83/7.68 | GROUND_INST: instantiating (mSortsB) with all_38_0, xb, all_42_0, simplifying % 50.83/7.68 | with (24), (74), (75) gives: % 50.83/7.68 | (87) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_42_0) = v2 % 50.83/7.68 | & aElement0(all_38_0) = v0 & aElement0(xb) = v1 & ( ~ (v1 = 0) | ~ % 50.83/7.68 | (v0 = 0) | v2 = 0)) % 50.83/7.68 | % 50.83/7.68 | GROUND_INST: instantiating (3) with all_46_0, all_46_1, xu, simplifying with % 50.83/7.68 | (47), (48), (51) gives: % 50.83/7.68 | (88) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(all_46_0, % 50.83/7.68 | all_46_1) = v2 & aElement0(all_46_0) = v0 & aElement0(all_46_1) = % 50.83/7.68 | v1 & $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = xu)) % 50.83/7.68 | % 50.83/7.68 | GROUND_INST: instantiating (2) with all_46_1, all_46_0, xu, simplifying with % 50.83/7.68 | (47), (48), (51) gives: % 50.83/7.68 | (89) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(all_46_0, % 50.83/7.68 | all_46_1) = v2 & aElement0(all_46_0) = v1 & aElement0(all_46_1) = % 50.83/7.68 | v0 & $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = xu)) % 50.83/7.68 | % 50.83/7.68 | GROUND_INST: instantiating (mSortsB) with all_46_1, all_46_0, xu, simplifying % 50.83/7.68 | with (47), (48), (51) gives: % 50.83/7.68 | (90) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_46_0) = v1 % 50.83/7.68 | & aElement0(all_46_1) = v0 & aElement0(xu) = v2 & ( ~ (v1 = 0) | ~ % 50.83/7.68 | (v0 = 0) | v2 = 0)) % 50.83/7.68 | % 50.83/7.68 | GROUND_INST: instantiating (8) with all_46_3, xa, all_46_1, simplifying with % 50.83/7.68 | (19), (45), (52) gives: % 50.83/7.68 | (91) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_46_3, xa) = % 50.83/7.68 | v2 & aElement0(all_46_3) = v0 & aElement0(xa) = v1 & $i(v2) & ( ~ % 50.83/7.68 | (v1 = 0) | ~ (v0 = 0) | v2 = all_46_1)) % 50.83/7.68 | % 50.83/7.68 | GROUND_INST: instantiating (7) with xa, all_46_3, all_46_1, simplifying with % 50.83/7.68 | (19), (45), (52) gives: % 50.83/7.68 | (92) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_46_3, xa) = % 50.83/7.68 | v2 & aElement0(all_46_3) = v1 & aElement0(xa) = v0 & $i(v2) & ( ~ % 50.83/7.68 | (v1 = 0) | ~ (v0 = 0) | v2 = all_46_1)) % 50.83/7.69 | % 50.83/7.69 | GROUND_INST: instantiating (mSortsB_02) with xa, all_46_3, all_46_1, % 50.83/7.69 | simplifying with (19), (45), (52) gives: % 50.83/7.69 | (93) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_46_1) = v2 % 50.83/7.69 | & aElement0(all_46_3) = v1 & aElement0(xa) = v0 & ( ~ (v1 = 0) | ~ % 50.83/7.69 | (v0 = 0) | v2 = 0)) % 50.83/7.69 | % 50.83/7.69 | GROUND_INST: instantiating (10) with all_46_2, all_38_1, xr, xb, all_46_0, % 50.83/7.69 | simplifying with (27), (46), (53), (70), (72) gives: % 50.83/7.69 | (94) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: $i] % 50.83/7.69 | : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] % 50.83/7.69 | : (sdtasdt0(all_46_2, all_38_1) = v4 & sdtasdt0(all_46_2, xr) = v5 & % 50.83/7.69 | sdtasdt0(all_46_2, xb) = v3 & sdtasdt0(all_38_1, all_46_2) = v7 & % 50.83/7.69 | sdtasdt0(xr, all_46_2) = v8 & sdtpldt0(v7, v8) = v9 & sdtpldt0(v4, % 50.83/7.69 | v5) = v6 & aElement0(all_46_2) = v0 & aElement0(all_38_1) = v1 & % 50.83/7.69 | aElement0(xr) = v2 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & % 50.83/7.69 | $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | (v9 = % 50.83/7.69 | all_46_0 & v6 = v3))) % 50.83/7.69 | % 50.83/7.69 | GROUND_INST: instantiating (8) with all_46_2, xb, all_46_0, simplifying with % 50.83/7.69 | (24), (46), (53) gives: % 50.83/7.69 | (95) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_46_2, xb) = % 50.83/7.69 | v2 & aElement0(all_46_2) = v0 & aElement0(xb) = v1 & $i(v2) & ( ~ % 50.83/7.69 | (v1 = 0) | ~ (v0 = 0) | v2 = all_46_0)) % 50.83/7.69 | % 50.83/7.69 | GROUND_INST: instantiating (7) with xb, all_46_2, all_46_0, simplifying with % 50.83/7.69 | (24), (46), (53) gives: % 50.83/7.69 | (96) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_46_2, xb) = % 50.83/7.69 | v2 & aElement0(all_46_2) = v1 & aElement0(xb) = v0 & $i(v2) & ( ~ % 50.83/7.69 | (v1 = 0) | ~ (v0 = 0) | v2 = all_46_0)) % 50.83/7.69 | % 50.83/7.69 | GROUND_INST: instantiating (mSortsB_02) with xb, all_46_2, all_46_0, % 50.83/7.69 | simplifying with (24), (46), (53) gives: % 50.83/7.69 | (97) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_46_0) = v2 % 50.83/7.69 | & aElement0(all_46_2) = v1 & aElement0(xb) = v0 & ( ~ (v1 = 0) | ~ % 50.83/7.69 | (v0 = 0) | v2 = 0)) % 50.83/7.69 | % 50.83/7.69 | GROUND_INST: instantiating (9) with xq, all_46_1, all_46_0, xu, all_38_1, % 50.83/7.69 | simplifying with (26), (36), (47), (48), (51) gives: % 50.83/7.69 | (98) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: $i] % 50.83/7.69 | : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] % 50.83/7.69 | : (sdtasdt0(all_46_0, xq) = v8 & sdtasdt0(all_46_1, xq) = v7 & % 50.83/7.69 | sdtasdt0(xq, all_46_0) = v4 & sdtasdt0(xq, all_46_1) = v3 & % 50.83/7.69 | sdtasdt0(xu, xq) = v6 & sdtpldt0(v7, v8) = v9 & sdtpldt0(v3, v4) = % 50.83/7.69 | v5 & aElement0(all_46_0) = v2 & aElement0(all_46_1) = v1 & % 50.83/7.69 | aElement0(xq) = v0 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & % 50.83/7.69 | $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | (v9 = % 50.83/7.69 | v6 & v5 = all_38_1))) % 50.83/7.69 | % 50.83/7.69 | GROUND_INST: instantiating (7) with xq, xu, all_38_1, simplifying with (25), % 50.83/7.69 | (26), (36) gives: % 50.83/7.69 | (99) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(xu, xq) = v2 & % 50.83/7.69 | aElement0(xq) = v0 & aElement0(xu) = v1 & $i(v2) & ( ~ (v1 = 0) | ~ % 50.83/7.69 | (v0 = 0) | v2 = all_38_1)) % 50.83/7.69 | % 50.83/7.69 | GROUND_INST: instantiating (mSortsB_02) with xq, xu, all_38_1, simplifying % 50.83/7.69 | with (25), (26), (36) gives: % 50.83/7.69 | (100) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aElement0(all_38_1) = % 50.83/7.69 | v2 & aElement0(xq) = v0 & aElement0(xu) = v1 & ( ~ (v1 = 0) | ~ % 50.83/7.69 | (v0 = 0) | v2 = 0)) % 50.83/7.69 | % 50.83/7.69 | GROUND_INST: instantiating (13) with all_46_3, xu, all_50_1, simplifying with % 50.83/7.69 | (25), (45), (49), (59) gives: % 50.83/7.69 | (101) xu = sz00 | ? [v0: int] : ? [v1: $i] : ? [v2: $i] : ? [v3: int] : % 50.83/7.69 | ? [v4: int] : ? [v5: $i] : ? [v6: int] : ? [v7: $i] : ? [v8: % 50.83/7.69 | any] : ($i(v2) & $i(v1) & ((v6 = all_46_3 & v4 = 0 & v3 = 0 & % 50.83/7.69 | iLess0(v7, all_50_1) = v8 & sbrdtbr0(v2) = v7 & sdtasdt0(v1, % 50.83/7.69 | xu) = v5 & sdtpldt0(v5, v2) = all_46_3 & aElement0(v2) = 0 & % 50.83/7.69 | aElement0(v1) = 0 & $i(v7) & $i(v5) & (v8 = 0 | v2 = sz00)) | ( % 50.83/7.69 | ~ (v0 = 0) & aElement0(xu) = v0))) % 50.83/7.69 | % 50.83/7.69 | GROUND_INST: instantiating (12) with xu, all_50_1, simplifying with (25), (59) % 50.83/7.69 | gives: % 50.83/7.69 | (102) xu = sz00 | ? [v0: any] : ? [v1: any] : (aNaturalNumber0(all_50_1) % 50.83/7.69 | = v1 & aElement0(xu) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 50.83/7.69 | % 50.83/7.69 | GROUND_INST: instantiating (12) with xr, all_50_2, simplifying with (27), (60) % 50.83/7.69 | gives: % 50.83/7.69 | (103) xr = sz00 | ? [v0: any] : ? [v1: any] : (aNaturalNumber0(all_50_2) % 50.83/7.69 | = v1 & aElement0(xr) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 50.83/7.69 | % 50.83/7.69 | GROUND_INST: instantiating (14) with xa, xu, simplifying with (15), (19), % 50.83/7.69 | (20), (25) gives: % 50.83/7.70 | (104) ? [v0: any] : ? [v1: any] : (aDivisorOf0(xu, xa) = v1 & % 50.83/7.70 | aElement0(xu) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 50.83/7.70 | % 50.83/7.70 | DELTA: instantiating (104) with fresh symbols all_226_0, all_226_1 gives: % 50.83/7.70 | (105) aDivisorOf0(xu, xa) = all_226_0 & aElement0(xu) = all_226_1 & ( ~ % 50.83/7.70 | (all_226_1 = 0) | all_226_0 = 0) % 50.83/7.70 | % 50.83/7.70 | ALPHA: (105) implies: % 50.83/7.70 | (106) aElement0(xu) = all_226_1 % 50.83/7.70 | % 50.83/7.70 | DELTA: instantiating (80) with fresh symbols all_332_0, all_332_1 gives: % 50.83/7.70 | (107) aElement0(all_38_0) = all_332_0 & aElement0(all_38_1) = all_332_1 & ( % 50.83/7.70 | ~ (all_332_1 = 0) | all_332_0 = 0) % 50.83/7.70 | % 50.83/7.70 | ALPHA: (107) implies: % 50.83/7.70 | (108) aElement0(all_38_1) = all_332_1 % 50.83/7.70 | (109) aElement0(all_38_0) = all_332_0 % 50.83/7.70 | (110) ~ (all_332_1 = 0) | all_332_0 = 0 % 50.83/7.70 | % 50.83/7.70 | DELTA: instantiating (100) with fresh symbols all_510_0, all_510_1, all_510_2 % 50.83/7.70 | gives: % 50.83/7.70 | (111) aElement0(all_38_1) = all_510_0 & aElement0(xq) = all_510_2 & % 50.83/7.70 | aElement0(xu) = all_510_1 & ( ~ (all_510_1 = 0) | ~ (all_510_2 = 0) % 50.83/7.70 | | all_510_0 = 0) % 50.83/7.70 | % 50.83/7.70 | ALPHA: (111) implies: % 50.83/7.70 | (112) aElement0(xu) = all_510_1 % 50.83/7.70 | (113) aElement0(xq) = all_510_2 % 50.83/7.70 | (114) aElement0(all_38_1) = all_510_0 % 50.83/7.70 | (115) ~ (all_510_1 = 0) | ~ (all_510_2 = 0) | all_510_0 = 0 % 50.83/7.70 | % 50.83/7.70 | DELTA: instantiating (97) with fresh symbols all_512_0, all_512_1, all_512_2 % 50.83/7.70 | gives: % 50.83/7.70 | (116) aElement0(all_46_0) = all_512_0 & aElement0(all_46_2) = all_512_1 & % 50.83/7.70 | aElement0(xb) = all_512_2 & ( ~ (all_512_1 = 0) | ~ (all_512_2 = 0) % 50.83/7.70 | | all_512_0 = 0) % 50.83/7.70 | % 50.83/7.70 | ALPHA: (116) implies: % 50.83/7.70 | (117) aElement0(xb) = all_512_2 % 50.83/7.70 | (118) aElement0(all_46_2) = all_512_1 % 50.83/7.70 | (119) aElement0(all_46_0) = all_512_0 % 50.83/7.70 | (120) ~ (all_512_1 = 0) | ~ (all_512_2 = 0) | all_512_0 = 0 % 50.83/7.70 | % 50.83/7.70 | DELTA: instantiating (93) with fresh symbols all_514_0, all_514_1, all_514_2 % 50.83/7.70 | gives: % 50.83/7.70 | (121) aElement0(all_46_1) = all_514_0 & aElement0(all_46_3) = all_514_1 & % 50.83/7.70 | aElement0(xa) = all_514_2 & ( ~ (all_514_1 = 0) | ~ (all_514_2 = 0) % 50.83/7.70 | | all_514_0 = 0) % 50.83/7.70 | % 50.83/7.70 | ALPHA: (121) implies: % 50.83/7.70 | (122) aElement0(xa) = all_514_2 % 50.83/7.70 | (123) aElement0(all_46_3) = all_514_1 % 50.83/7.70 | (124) aElement0(all_46_1) = all_514_0 % 50.83/7.70 | (125) ~ (all_514_1 = 0) | ~ (all_514_2 = 0) | all_514_0 = 0 % 50.83/7.70 | % 50.83/7.70 | DELTA: instantiating (90) with fresh symbols all_516_0, all_516_1, all_516_2 % 50.83/7.70 | gives: % 50.83/7.70 | (126) aElement0(all_46_0) = all_516_1 & aElement0(all_46_1) = all_516_2 & % 50.83/7.70 | aElement0(xu) = all_516_0 & ( ~ (all_516_1 = 0) | ~ (all_516_2 = 0) % 50.83/7.70 | | all_516_0 = 0) % 50.83/7.70 | % 50.83/7.70 | ALPHA: (126) implies: % 50.83/7.70 | (127) aElement0(xu) = all_516_0 % 50.83/7.70 | (128) aElement0(all_46_1) = all_516_2 % 50.83/7.70 | (129) aElement0(all_46_0) = all_516_1 % 50.83/7.70 | (130) ~ (all_516_1 = 0) | ~ (all_516_2 = 0) | all_516_0 = 0 % 50.83/7.70 | % 50.83/7.70 | DELTA: instantiating (83) with fresh symbols all_518_0, all_518_1, all_518_2 % 50.83/7.70 | gives: % 50.83/7.70 | (131) aElement0(all_38_1) = all_518_2 & aElement0(xr) = all_518_1 & % 50.83/7.70 | aElement0(xb) = all_518_0 & ( ~ (all_518_1 = 0) | ~ (all_518_2 = 0) % 50.83/7.70 | | all_518_0 = 0) % 50.83/7.70 | % 50.83/7.70 | ALPHA: (131) implies: % 50.83/7.70 | (132) aElement0(xb) = all_518_0 % 50.83/7.70 | (133) aElement0(all_38_1) = all_518_2 % 50.83/7.70 | % 50.83/7.70 | DELTA: instantiating (87) with fresh symbols all_520_0, all_520_1, all_520_2 % 50.83/7.70 | gives: % 50.83/7.70 | (134) aElement0(all_42_0) = all_520_0 & aElement0(all_38_0) = all_520_2 & % 50.83/7.70 | aElement0(xb) = all_520_1 & ( ~ (all_520_1 = 0) | ~ (all_520_2 = 0) % 50.83/7.70 | | all_520_0 = 0) % 50.83/7.70 | % 50.83/7.70 | ALPHA: (134) implies: % 50.83/7.70 | (135) aElement0(xb) = all_520_1 % 50.83/7.70 | (136) aElement0(all_38_0) = all_520_2 % 50.83/7.70 | % 50.83/7.70 | DELTA: instantiating (82) with fresh symbols all_524_0, all_524_1, all_524_2 % 50.83/7.70 | gives: % 50.83/7.70 | (137) sdtpldt0(xr, all_38_1) = all_524_0 & aElement0(all_38_1) = all_524_2 % 50.83/7.70 | & aElement0(xr) = all_524_1 & $i(all_524_0) & ( ~ (all_524_1 = 0) | % 50.83/7.70 | ~ (all_524_2 = 0) | all_524_0 = xb) % 50.83/7.70 | % 50.83/7.70 | ALPHA: (137) implies: % 50.83/7.70 | (138) aElement0(xr) = all_524_1 % 50.83/7.70 | (139) aElement0(all_38_1) = all_524_2 % 50.83/7.70 | % 50.83/7.70 | DELTA: instantiating (81) with fresh symbols all_526_0, all_526_1, all_526_2 % 50.83/7.70 | gives: % 50.83/7.70 | (140) sdtpldt0(xr, all_38_1) = all_526_0 & aElement0(all_38_1) = all_526_1 % 50.83/7.70 | & aElement0(xr) = all_526_2 & $i(all_526_0) & ( ~ (all_526_1 = 0) | % 50.83/7.70 | ~ (all_526_2 = 0) | all_526_0 = xb) % 50.83/7.70 | % 50.83/7.70 | ALPHA: (140) implies: % 50.83/7.70 | (141) aElement0(all_38_1) = all_526_1 % 50.83/7.70 | % 50.83/7.70 | DELTA: instantiating (92) with fresh symbols all_528_0, all_528_1, all_528_2 % 50.83/7.70 | gives: % 50.83/7.70 | (142) sdtasdt0(all_46_3, xa) = all_528_0 & aElement0(all_46_3) = all_528_1 % 50.83/7.70 | & aElement0(xa) = all_528_2 & $i(all_528_0) & ( ~ (all_528_1 = 0) | % 50.83/7.70 | ~ (all_528_2 = 0) | all_528_0 = all_46_1) % 50.83/7.70 | % 50.83/7.70 | ALPHA: (142) implies: % 50.83/7.70 | (143) aElement0(xa) = all_528_2 % 50.83/7.70 | (144) aElement0(all_46_3) = all_528_1 % 50.83/7.70 | % 50.83/7.70 | DELTA: instantiating (86) with fresh symbols all_530_0, all_530_1, all_530_2 % 50.83/7.70 | gives: % 50.83/7.70 | (145) sdtpldt0(xb, all_38_0) = all_530_0 & aElement0(all_38_0) = all_530_2 % 50.83/7.70 | & aElement0(xb) = all_530_1 & $i(all_530_0) & ( ~ (all_530_1 = 0) | % 50.83/7.70 | ~ (all_530_2 = 0) | all_530_0 = all_42_0) % 50.83/7.70 | % 50.83/7.70 | ALPHA: (145) implies: % 50.83/7.70 | (146) aElement0(xb) = all_530_1 % 50.83/7.70 | (147) aElement0(all_38_0) = all_530_2 % 50.83/7.70 | % 50.83/7.70 | DELTA: instantiating (85) with fresh symbols all_532_0, all_532_1, all_532_2 % 50.83/7.70 | gives: % 50.83/7.70 | (148) sdtpldt0(xb, all_38_0) = all_532_0 & aElement0(all_38_0) = all_532_1 % 50.83/7.70 | & aElement0(xb) = all_532_2 & $i(all_532_0) & ( ~ (all_532_1 = 0) | % 50.83/7.70 | ~ (all_532_2 = 0) | all_532_0 = all_42_0) % 50.83/7.70 | % 50.83/7.70 | ALPHA: (148) implies: % 50.83/7.70 | (149) aElement0(xb) = all_532_2 % 50.83/7.70 | (150) aElement0(all_38_0) = all_532_1 % 50.83/7.70 | % 50.83/7.70 | DELTA: instantiating (99) with fresh symbols all_534_0, all_534_1, all_534_2 % 50.83/7.70 | gives: % 50.83/7.70 | (151) sdtasdt0(xu, xq) = all_534_0 & aElement0(xq) = all_534_2 & % 50.83/7.70 | aElement0(xu) = all_534_1 & $i(all_534_0) & ( ~ (all_534_1 = 0) | ~ % 50.83/7.70 | (all_534_2 = 0) | all_534_0 = all_38_1) % 50.83/7.70 | % 50.83/7.70 | ALPHA: (151) implies: % 50.83/7.70 | (152) aElement0(xq) = all_534_2 % 50.83/7.70 | % 50.83/7.70 | DELTA: instantiating (96) with fresh symbols all_536_0, all_536_1, all_536_2 % 50.83/7.70 | gives: % 50.83/7.71 | (153) sdtasdt0(all_46_2, xb) = all_536_0 & aElement0(all_46_2) = all_536_1 % 50.83/7.71 | & aElement0(xb) = all_536_2 & $i(all_536_0) & ( ~ (all_536_1 = 0) | % 50.83/7.71 | ~ (all_536_2 = 0) | all_536_0 = all_46_0) % 50.83/7.71 | % 50.83/7.71 | ALPHA: (153) implies: % 50.83/7.71 | (154) aElement0(xb) = all_536_2 % 50.83/7.71 | (155) aElement0(all_46_2) = all_536_1 % 50.83/7.71 | % 50.83/7.71 | DELTA: instantiating (95) with fresh symbols all_538_0, all_538_1, all_538_2 % 50.83/7.71 | gives: % 50.83/7.71 | (156) sdtasdt0(all_46_2, xb) = all_538_0 & aElement0(all_46_2) = all_538_2 % 50.83/7.71 | & aElement0(xb) = all_538_1 & $i(all_538_0) & ( ~ (all_538_1 = 0) | % 50.83/7.71 | ~ (all_538_2 = 0) | all_538_0 = all_46_0) % 50.83/7.71 | % 50.83/7.71 | ALPHA: (156) implies: % 50.83/7.71 | (157) aElement0(xb) = all_538_1 % 50.83/7.71 | (158) aElement0(all_46_2) = all_538_2 % 50.83/7.71 | % 50.83/7.71 | DELTA: instantiating (91) with fresh symbols all_540_0, all_540_1, all_540_2 % 50.83/7.71 | gives: % 50.83/7.71 | (159) sdtasdt0(all_46_3, xa) = all_540_0 & aElement0(all_46_3) = all_540_2 % 50.83/7.71 | & aElement0(xa) = all_540_1 & $i(all_540_0) & ( ~ (all_540_1 = 0) | % 50.83/7.71 | ~ (all_540_2 = 0) | all_540_0 = all_46_1) % 50.83/7.71 | % 50.83/7.71 | ALPHA: (159) implies: % 50.83/7.71 | (160) aElement0(xa) = all_540_1 % 50.83/7.71 | (161) aElement0(all_46_3) = all_540_2 % 50.83/7.71 | % 50.83/7.71 | DELTA: instantiating (89) with fresh symbols all_542_0, all_542_1, all_542_2 % 50.83/7.71 | gives: % 50.83/7.71 | (162) sdtpldt0(all_46_0, all_46_1) = all_542_0 & aElement0(all_46_0) = % 50.83/7.71 | all_542_1 & aElement0(all_46_1) = all_542_2 & $i(all_542_0) & ( ~ % 50.83/7.71 | (all_542_1 = 0) | ~ (all_542_2 = 0) | all_542_0 = xu) % 50.83/7.71 | % 50.83/7.71 | ALPHA: (162) implies: % 50.83/7.71 | (163) aElement0(all_46_1) = all_542_2 % 50.83/7.71 | (164) aElement0(all_46_0) = all_542_1 % 50.83/7.71 | % 50.83/7.71 | DELTA: instantiating (88) with fresh symbols all_546_0, all_546_1, all_546_2 % 50.83/7.71 | gives: % 50.83/7.71 | (165) sdtpldt0(all_46_0, all_46_1) = all_546_0 & aElement0(all_46_0) = % 50.83/7.71 | all_546_2 & aElement0(all_46_1) = all_546_1 & $i(all_546_0) & ( ~ % 50.83/7.71 | (all_546_1 = 0) | ~ (all_546_2 = 0) | all_546_0 = xu) % 50.83/7.71 | % 50.83/7.71 | ALPHA: (165) implies: % 50.83/7.71 | (166) aElement0(all_46_1) = all_546_1 % 50.83/7.71 | (167) aElement0(all_46_0) = all_546_2 % 50.83/7.71 | % 50.83/7.71 | DELTA: instantiating (79) with fresh symbols all_548_0, all_548_1, all_548_2 % 50.83/7.71 | gives: % 50.83/7.71 | (168) sdtpldt0(all_38_0, all_38_1) = all_548_0 & sdtpldt0(all_38_1, % 50.83/7.71 | all_38_0) = all_548_1 & aElement0(all_38_1) = all_548_2 & % 50.83/7.71 | $i(all_548_0) & $i(all_548_1) & ( ~ (all_548_2 = 0) | (all_548_0 = % 50.83/7.71 | sz00 & all_548_1 = sz00)) % 50.83/7.71 | % 50.83/7.71 | ALPHA: (168) implies: % 50.83/7.71 | (169) aElement0(all_38_1) = all_548_2 % 50.83/7.71 | (170) sdtpldt0(all_38_0, all_38_1) = all_548_0 % 50.83/7.71 | (171) ~ (all_548_2 = 0) | (all_548_0 = sz00 & all_548_1 = sz00) % 50.83/7.71 | % 50.83/7.71 | DELTA: instantiating (78) with fresh symbols all_550_0, all_550_1, all_550_2 % 50.83/7.71 | gives: % 50.83/7.71 | (172) sdtasdt0(all_55_0, all_38_1) = all_550_1 & sdtasdt0(all_38_1, % 50.83/7.71 | all_55_0) = all_550_0 & aElement0(all_38_1) = all_550_2 & % 50.83/7.71 | $i(all_550_0) & $i(all_550_1) & ( ~ (all_550_2 = 0) | (all_550_0 = % 50.83/7.71 | all_38_0 & all_550_1 = all_38_0)) % 50.83/7.71 | % 50.83/7.71 | ALPHA: (172) implies: % 50.83/7.71 | (173) aElement0(all_38_1) = all_550_2 % 50.83/7.71 | % 50.83/7.71 | DELTA: instantiating (84) with fresh symbols all_558_0, all_558_1, all_558_2, % 50.83/7.71 | all_558_3, all_558_4 gives: % 50.83/7.71 | (174) sdtpldt0(all_558_1, xr) = all_558_0 & sdtpldt0(all_38_0, all_38_1) = % 50.83/7.71 | all_558_1 & aElement0(all_38_0) = all_558_4 & aElement0(all_38_1) = % 50.83/7.71 | all_558_3 & aElement0(xr) = all_558_2 & $i(all_558_0) & $i(all_558_1) % 50.83/7.71 | & ( ~ (all_558_2 = 0) | ~ (all_558_3 = 0) | ~ (all_558_4 = 0) | % 50.83/7.71 | all_558_0 = all_42_0) % 50.83/7.71 | % 50.83/7.71 | ALPHA: (174) implies: % 50.83/7.71 | (175) aElement0(xr) = all_558_2 % 50.83/7.71 | (176) aElement0(all_38_1) = all_558_3 % 50.83/7.71 | (177) aElement0(all_38_0) = all_558_4 % 50.83/7.71 | (178) sdtpldt0(all_38_0, all_38_1) = all_558_1 % 50.83/7.71 | (179) sdtpldt0(all_558_1, xr) = all_558_0 % 50.83/7.71 | (180) ~ (all_558_2 = 0) | ~ (all_558_3 = 0) | ~ (all_558_4 = 0) | % 50.83/7.71 | all_558_0 = all_42_0 % 50.83/7.71 | % 50.83/7.71 | DELTA: instantiating (98) with fresh symbols all_692_0, all_692_1, all_692_2, % 50.83/7.71 | all_692_3, all_692_4, all_692_5, all_692_6, all_692_7, all_692_8, % 50.83/7.71 | all_692_9 gives: % 50.83/7.71 | (181) sdtasdt0(all_46_0, xq) = all_692_1 & sdtasdt0(all_46_1, xq) = % 50.83/7.71 | all_692_2 & sdtasdt0(xq, all_46_0) = all_692_5 & sdtasdt0(xq, % 50.83/7.71 | all_46_1) = all_692_6 & sdtasdt0(xu, xq) = all_692_3 & % 50.83/7.71 | sdtpldt0(all_692_2, all_692_1) = all_692_0 & sdtpldt0(all_692_6, % 50.83/7.71 | all_692_5) = all_692_4 & aElement0(all_46_0) = all_692_7 & % 50.83/7.71 | aElement0(all_46_1) = all_692_8 & aElement0(xq) = all_692_9 & % 50.83/7.71 | $i(all_692_0) & $i(all_692_1) & $i(all_692_2) & $i(all_692_3) & % 50.83/7.71 | $i(all_692_4) & $i(all_692_5) & $i(all_692_6) & ( ~ (all_692_7 = 0) | % 50.83/7.71 | ~ (all_692_8 = 0) | ~ (all_692_9 = 0) | (all_692_0 = all_692_3 & % 50.83/7.71 | all_692_4 = all_38_1)) % 50.83/7.71 | % 50.83/7.71 | ALPHA: (181) implies: % 50.83/7.71 | (182) aElement0(all_46_1) = all_692_8 % 50.83/7.71 | (183) aElement0(all_46_0) = all_692_7 % 50.83/7.71 | % 50.83/7.71 | DELTA: instantiating (94) with fresh symbols all_694_0, all_694_1, all_694_2, % 50.83/7.71 | all_694_3, all_694_4, all_694_5, all_694_6, all_694_7, all_694_8, % 50.83/7.71 | all_694_9 gives: % 50.83/7.71 | (184) sdtasdt0(all_46_2, all_38_1) = all_694_5 & sdtasdt0(all_46_2, xr) = % 50.83/7.71 | all_694_4 & sdtasdt0(all_46_2, xb) = all_694_6 & sdtasdt0(all_38_1, % 50.83/7.71 | all_46_2) = all_694_2 & sdtasdt0(xr, all_46_2) = all_694_1 & % 50.83/7.71 | sdtpldt0(all_694_2, all_694_1) = all_694_0 & sdtpldt0(all_694_5, % 50.83/7.71 | all_694_4) = all_694_3 & aElement0(all_46_2) = all_694_9 & % 50.83/7.71 | aElement0(all_38_1) = all_694_8 & aElement0(xr) = all_694_7 & % 50.83/7.71 | $i(all_694_0) & $i(all_694_1) & $i(all_694_2) & $i(all_694_3) & % 50.83/7.71 | $i(all_694_4) & $i(all_694_5) & $i(all_694_6) & ( ~ (all_694_7 = 0) | % 50.83/7.71 | ~ (all_694_8 = 0) | ~ (all_694_9 = 0) | (all_694_0 = all_46_0 & % 50.83/7.71 | all_694_3 = all_694_6)) % 50.83/7.71 | % 50.83/7.71 | ALPHA: (184) implies: % 50.83/7.71 | (185) aElement0(xr) = all_694_7 % 50.83/7.71 | (186) aElement0(all_38_1) = all_694_8 % 50.83/7.71 | (187) aElement0(all_46_2) = all_694_9 % 50.83/7.71 | % 50.83/7.71 | BETA: splitting (103) gives: % 50.83/7.71 | % 50.83/7.71 | Case 1: % 50.83/7.71 | | % 50.83/7.71 | | (188) xr = sz00 % 50.83/7.71 | | % 50.83/7.71 | | REDUCE: (22), (188) imply: % 50.83/7.71 | | (189) $false % 50.83/7.72 | | % 50.83/7.72 | | CLOSE: (189) is inconsistent. % 50.83/7.72 | | % 50.83/7.72 | Case 2: % 50.83/7.72 | | % 50.83/7.72 | | (190) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(all_50_2) = v1 & % 50.83/7.72 | | aElement0(xr) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 50.83/7.72 | | % 50.83/7.72 | | DELTA: instantiating (190) with fresh symbols all_847_0, all_847_1 gives: % 50.83/7.72 | | (191) aNaturalNumber0(all_50_2) = all_847_0 & aElement0(xr) = all_847_1 & % 50.83/7.72 | | ( ~ (all_847_1 = 0) | all_847_0 = 0) % 50.83/7.72 | | % 50.83/7.72 | | ALPHA: (191) implies: % 50.83/7.72 | | (192) aElement0(xr) = all_847_1 % 50.83/7.72 | | % 50.83/7.72 | | BETA: splitting (102) gives: % 50.83/7.72 | | % 50.83/7.72 | | Case 1: % 50.83/7.72 | | | % 50.83/7.72 | | | (193) xu = sz00 % 50.83/7.72 | | | % 50.83/7.72 | | | REDUCE: (62), (193) imply: % 50.83/7.72 | | | (194) $false % 50.83/7.72 | | | % 50.83/7.72 | | | CLOSE: (194) is inconsistent. % 50.83/7.72 | | | % 50.83/7.72 | | Case 2: % 50.83/7.72 | | | % 50.83/7.72 | | | (195) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(all_50_1) = v1 & % 50.83/7.72 | | | aElement0(xu) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 50.83/7.72 | | | % 50.83/7.72 | | | DELTA: instantiating (195) with fresh symbols all_852_0, all_852_1 gives: % 50.83/7.72 | | | (196) aNaturalNumber0(all_50_1) = all_852_0 & aElement0(xu) = all_852_1 % 50.83/7.72 | | | & ( ~ (all_852_1 = 0) | all_852_0 = 0) % 50.83/7.72 | | | % 50.83/7.72 | | | ALPHA: (196) implies: % 50.83/7.72 | | | (197) aElement0(xu) = all_852_1 % 50.83/7.72 | | | % 50.83/7.72 | | | BETA: splitting (101) gives: % 50.83/7.72 | | | % 50.83/7.72 | | | Case 1: % 50.83/7.72 | | | | % 50.83/7.72 | | | | (198) xu = sz00 % 50.83/7.72 | | | | % 50.83/7.72 | | | | REDUCE: (62), (198) imply: % 50.83/7.72 | | | | (199) $false % 50.83/7.72 | | | | % 50.83/7.72 | | | | CLOSE: (199) is inconsistent. % 50.83/7.72 | | | | % 50.83/7.72 | | | Case 2: % 50.83/7.72 | | | | % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with 0, all_540_1, xa, simplifying with % 50.83/7.72 | | | | (15), (160) gives: % 50.83/7.72 | | | | (200) all_540_1 = 0 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_528_2, all_540_1, xa, % 50.83/7.72 | | | | simplifying with (143), (160) gives: % 50.83/7.72 | | | | (201) all_540_1 = all_528_2 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_514_2, all_540_1, xa, % 50.83/7.72 | | | | simplifying with (122), (160) gives: % 50.83/7.72 | | | | (202) all_540_1 = all_514_2 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with 0, all_530_1, xb, simplifying with % 50.83/7.72 | | | | (16), (146) gives: % 50.83/7.72 | | | | (203) all_530_1 = 0 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_512_2, all_532_2, xb, % 50.83/7.72 | | | | simplifying with (117), (149) gives: % 50.83/7.72 | | | | (204) all_532_2 = all_512_2 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_532_2, all_536_2, xb, % 50.83/7.72 | | | | simplifying with (149), (154) gives: % 50.83/7.72 | | | | (205) all_536_2 = all_532_2 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_520_1, all_536_2, xb, % 50.83/7.72 | | | | simplifying with (135), (154) gives: % 50.83/7.72 | | | | (206) all_536_2 = all_520_1 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_532_2, all_538_1, xb, % 50.83/7.72 | | | | simplifying with (149), (157) gives: % 50.83/7.72 | | | | (207) all_538_1 = all_532_2 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_530_1, all_538_1, xb, % 50.83/7.72 | | | | simplifying with (146), (157) gives: % 50.83/7.72 | | | | (208) all_538_1 = all_530_1 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_518_0, all_538_1, xb, % 50.83/7.72 | | | | simplifying with (132), (157) gives: % 50.83/7.72 | | | | (209) all_538_1 = all_518_0 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_516_0, all_852_1, xu, % 50.83/7.72 | | | | simplifying with (127), (197) gives: % 50.83/7.72 | | | | (210) all_852_1 = all_516_0 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_510_1, all_852_1, xu, % 50.83/7.72 | | | | simplifying with (112), (197) gives: % 50.83/7.72 | | | | (211) all_852_1 = all_510_1 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_226_1, all_852_1, xu, % 50.83/7.72 | | | | simplifying with (106), (197) gives: % 50.83/7.72 | | | | (212) all_852_1 = all_226_1 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with 0, all_534_2, xq, simplifying with % 50.83/7.72 | | | | (55), (152) gives: % 50.83/7.72 | | | | (213) all_534_2 = 0 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_510_2, all_534_2, xq, % 50.83/7.72 | | | | simplifying with (113), (152) gives: % 50.83/7.72 | | | | (214) all_534_2 = all_510_2 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_524_1, all_558_2, xr, % 50.83/7.72 | | | | simplifying with (138), (175) gives: % 50.83/7.72 | | | | (215) all_558_2 = all_524_1 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with 0, all_847_1, xr, simplifying with % 50.83/7.72 | | | | (56), (192) gives: % 50.83/7.72 | | | | (216) all_847_1 = 0 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_694_7, all_847_1, xr, % 50.83/7.72 | | | | simplifying with (185), (192) gives: % 50.83/7.72 | | | | (217) all_847_1 = all_694_7 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_558_2, all_847_1, xr, % 50.83/7.72 | | | | simplifying with (175), (192) gives: % 50.83/7.72 | | | | (218) all_847_1 = all_558_2 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_518_2, all_524_2, all_38_1, % 50.83/7.72 | | | | simplifying with (133), (139) gives: % 50.83/7.72 | | | | (219) all_524_2 = all_518_2 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_510_0, all_524_2, all_38_1, % 50.83/7.72 | | | | simplifying with (114), (139) gives: % 50.83/7.72 | | | | (220) all_524_2 = all_510_0 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_332_1, all_550_2, all_38_1, % 50.83/7.72 | | | | simplifying with (108), (173) gives: % 50.83/7.72 | | | | (221) all_550_2 = all_332_1 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_550_2, all_558_3, all_38_1, % 50.83/7.72 | | | | simplifying with (173), (176) gives: % 50.83/7.72 | | | | (222) all_558_3 = all_550_2 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_548_2, all_558_3, all_38_1, % 50.83/7.72 | | | | simplifying with (169), (176) gives: % 50.83/7.72 | | | | (223) all_558_3 = all_548_2 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_518_2, all_558_3, all_38_1, % 50.83/7.72 | | | | simplifying with (133), (176) gives: % 50.83/7.72 | | | | (224) all_558_3 = all_518_2 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_558_3, all_694_8, all_38_1, % 50.83/7.72 | | | | simplifying with (176), (186) gives: % 50.83/7.72 | | | | (225) all_694_8 = all_558_3 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_526_1, all_694_8, all_38_1, % 50.83/7.72 | | | | simplifying with (141), (186) gives: % 50.83/7.72 | | | | (226) all_694_8 = all_526_1 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_520_2, all_532_1, all_38_0, % 50.83/7.72 | | | | simplifying with (136), (150) gives: % 50.83/7.72 | | | | (227) all_532_1 = all_520_2 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_332_0, all_532_1, all_38_0, % 50.83/7.72 | | | | simplifying with (109), (150) gives: % 50.83/7.72 | | | | (228) all_532_1 = all_332_0 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_532_1, all_558_4, all_38_0, % 50.83/7.72 | | | | simplifying with (150), (177) gives: % 50.83/7.72 | | | | (229) all_558_4 = all_532_1 % 50.83/7.72 | | | | % 50.83/7.72 | | | | GROUND_INST: instantiating (29) with all_530_2, all_558_4, all_38_0, % 50.83/7.72 | | | | simplifying with (147), (177) gives: % 50.83/7.73 | | | | (230) all_558_4 = all_530_2 % 50.83/7.73 | | | | % 50.83/7.73 | | | | GROUND_INST: instantiating (29) with 0, all_528_1, all_46_3, simplifying % 50.83/7.73 | | | | with (49), (144) gives: % 50.83/7.73 | | | | (231) all_528_1 = 0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | GROUND_INST: instantiating (29) with all_528_1, all_540_2, all_46_3, % 50.83/7.73 | | | | simplifying with (144), (161) gives: % 50.83/7.73 | | | | (232) all_540_2 = all_528_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | GROUND_INST: instantiating (29) with all_514_1, all_540_2, all_46_3, % 50.83/7.73 | | | | simplifying with (123), (161) gives: % 50.83/7.73 | | | | (233) all_540_2 = all_514_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | GROUND_INST: instantiating (29) with 0, all_538_2, all_46_2, simplifying % 50.83/7.73 | | | | with (50), (158) gives: % 50.83/7.73 | | | | (234) all_538_2 = 0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | GROUND_INST: instantiating (29) with all_536_1, all_538_2, all_46_2, % 50.83/7.73 | | | | simplifying with (155), (158) gives: % 50.83/7.73 | | | | (235) all_538_2 = all_536_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | GROUND_INST: instantiating (29) with all_536_1, all_694_9, all_46_2, % 50.83/7.73 | | | | simplifying with (155), (187) gives: % 50.83/7.73 | | | | (236) all_694_9 = all_536_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | GROUND_INST: instantiating (29) with all_512_1, all_694_9, all_46_2, % 50.83/7.73 | | | | simplifying with (118), (187) gives: % 50.83/7.73 | | | | (237) all_694_9 = all_512_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | GROUND_INST: instantiating (29) with all_516_2, all_542_2, all_46_1, % 50.83/7.73 | | | | simplifying with (128), (163) gives: % 50.83/7.73 | | | | (238) all_542_2 = all_516_2 % 50.83/7.73 | | | | % 50.83/7.73 | | | | GROUND_INST: instantiating (29) with all_542_2, all_546_1, all_46_1, % 50.83/7.73 | | | | simplifying with (163), (166) gives: % 50.83/7.73 | | | | (239) all_546_1 = all_542_2 % 50.83/7.73 | | | | % 50.83/7.73 | | | | GROUND_INST: instantiating (29) with all_546_1, all_692_8, all_46_1, % 50.83/7.73 | | | | simplifying with (166), (182) gives: % 50.83/7.73 | | | | (240) all_692_8 = all_546_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | GROUND_INST: instantiating (29) with all_514_0, all_692_8, all_46_1, % 50.83/7.73 | | | | simplifying with (124), (182) gives: % 50.83/7.73 | | | | (241) all_692_8 = all_514_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | GROUND_INST: instantiating (29) with all_542_1, all_546_2, all_46_0, % 50.83/7.73 | | | | simplifying with (164), (167) gives: % 50.83/7.73 | | | | (242) all_546_2 = all_542_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | GROUND_INST: instantiating (29) with all_512_0, all_546_2, all_46_0, % 50.83/7.73 | | | | simplifying with (119), (167) gives: % 50.83/7.73 | | | | (243) all_546_2 = all_512_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | GROUND_INST: instantiating (29) with all_542_1, all_692_7, all_46_0, % 50.83/7.73 | | | | simplifying with (164), (183) gives: % 50.83/7.73 | | | | (244) all_692_7 = all_542_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | GROUND_INST: instantiating (29) with all_516_1, all_692_7, all_46_0, % 50.83/7.73 | | | | simplifying with (129), (183) gives: % 50.83/7.73 | | | | (245) all_692_7 = all_516_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | GROUND_INST: instantiating (32) with all_548_0, all_558_1, all_38_1, % 50.83/7.73 | | | | all_38_0, simplifying with (170), (178) gives: % 50.83/7.73 | | | | (246) all_558_1 = all_548_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (210), (211) imply: % 50.83/7.73 | | | | (247) all_516_0 = all_510_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (210), (212) imply: % 50.83/7.73 | | | | (248) all_516_0 = all_226_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (216), (217) imply: % 50.83/7.73 | | | | (249) all_694_7 = 0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (217), (218) imply: % 50.83/7.73 | | | | (250) all_694_7 = all_558_2 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (249), (250) imply: % 50.83/7.73 | | | | (251) all_558_2 = 0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (251) implies: % 50.83/7.73 | | | | (252) all_558_2 = 0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (225), (226) imply: % 50.83/7.73 | | | | (253) all_558_3 = all_526_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (253) implies: % 50.83/7.73 | | | | (254) all_558_3 = all_526_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (236), (237) imply: % 50.83/7.73 | | | | (255) all_536_1 = all_512_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (255) implies: % 50.83/7.73 | | | | (256) all_536_1 = all_512_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (244), (245) imply: % 50.83/7.73 | | | | (257) all_542_1 = all_516_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (257) implies: % 50.83/7.73 | | | | (258) all_542_1 = all_516_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (240), (241) imply: % 50.83/7.73 | | | | (259) all_546_1 = all_514_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (259) implies: % 50.83/7.73 | | | | (260) all_546_1 = all_514_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (215), (252) imply: % 50.83/7.73 | | | | (261) all_524_1 = 0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (222), (223) imply: % 50.83/7.73 | | | | (262) all_550_2 = all_548_2 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (262) implies: % 50.83/7.73 | | | | (263) all_550_2 = all_548_2 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (223), (224) imply: % 50.83/7.73 | | | | (264) all_548_2 = all_518_2 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (223), (254) imply: % 50.83/7.73 | | | | (265) all_548_2 = all_526_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (229), (230) imply: % 50.83/7.73 | | | | (266) all_532_1 = all_530_2 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (266) implies: % 50.83/7.73 | | | | (267) all_532_1 = all_530_2 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (221), (263) imply: % 50.83/7.73 | | | | (268) all_548_2 = all_332_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (268) implies: % 50.83/7.73 | | | | (269) all_548_2 = all_332_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (264), (265) imply: % 50.83/7.73 | | | | (270) all_526_1 = all_518_2 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (265), (269) imply: % 50.83/7.73 | | | | (271) all_526_1 = all_332_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (239), (260) imply: % 50.83/7.73 | | | | (272) all_542_2 = all_514_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (272) implies: % 50.83/7.73 | | | | (273) all_542_2 = all_514_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (242), (243) imply: % 50.83/7.73 | | | | (274) all_542_1 = all_512_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (274) implies: % 50.83/7.73 | | | | (275) all_542_1 = all_512_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (258), (275) imply: % 50.83/7.73 | | | | (276) all_516_1 = all_512_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (238), (273) imply: % 50.83/7.73 | | | | (277) all_516_2 = all_514_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (200), (201) imply: % 50.83/7.73 | | | | (278) all_528_2 = 0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (201), (202) imply: % 50.83/7.73 | | | | (279) all_528_2 = all_514_2 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (232), (233) imply: % 50.83/7.73 | | | | (280) all_528_1 = all_514_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (280) implies: % 50.83/7.73 | | | | (281) all_528_1 = all_514_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (208), (209) imply: % 50.83/7.73 | | | | (282) all_530_1 = all_518_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (282) implies: % 50.83/7.73 | | | | (283) all_530_1 = all_518_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (207), (209) imply: % 50.83/7.73 | | | | (284) all_532_2 = all_518_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (284) implies: % 50.83/7.73 | | | | (285) all_532_2 = all_518_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (234), (235) imply: % 50.83/7.73 | | | | (286) all_536_1 = 0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (286) implies: % 50.83/7.73 | | | | (287) all_536_1 = 0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (256), (287) imply: % 50.83/7.73 | | | | (288) all_512_1 = 0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (205), (206) imply: % 50.83/7.73 | | | | (289) all_532_2 = all_520_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (289) implies: % 50.83/7.73 | | | | (290) all_532_2 = all_520_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (213), (214) imply: % 50.83/7.73 | | | | (291) all_510_2 = 0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (228), (267) imply: % 50.83/7.73 | | | | (292) all_530_2 = all_332_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (227), (267) imply: % 50.83/7.73 | | | | (293) all_530_2 = all_520_2 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (285), (290) imply: % 50.83/7.73 | | | | (294) all_520_1 = all_518_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (204), (290) imply: % 50.83/7.73 | | | | (295) all_520_1 = all_512_2 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (203), (283) imply: % 50.83/7.73 | | | | (296) all_518_0 = 0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (296) implies: % 50.83/7.73 | | | | (297) all_518_0 = 0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (292), (293) imply: % 50.83/7.73 | | | | (298) all_520_2 = all_332_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (231), (281) imply: % 50.83/7.73 | | | | (299) all_514_1 = 0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (278), (279) imply: % 50.83/7.73 | | | | (300) all_514_2 = 0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (300) implies: % 50.83/7.73 | | | | (301) all_514_2 = 0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (270), (271) imply: % 50.83/7.73 | | | | (302) all_518_2 = all_332_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (302) implies: % 50.83/7.73 | | | | (303) all_518_2 = all_332_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (219), (220) imply: % 50.83/7.73 | | | | (304) all_518_2 = all_510_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (304) implies: % 50.83/7.73 | | | | (305) all_518_2 = all_510_0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (294), (295) imply: % 50.83/7.73 | | | | (306) all_518_0 = all_512_2 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (306) implies: % 50.83/7.73 | | | | (307) all_518_0 = all_512_2 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (297), (307) imply: % 50.83/7.73 | | | | (308) all_512_2 = 0 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (303), (305) imply: % 50.83/7.73 | | | | (309) all_510_0 = all_332_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (309) implies: % 50.83/7.73 | | | | (310) all_510_0 = all_332_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | COMBINE_EQS: (247), (248) imply: % 50.83/7.73 | | | | (311) all_510_1 = all_226_1 % 50.83/7.73 | | | | % 50.83/7.73 | | | | SIMP: (311) implies: % 50.83/7.74 | | | | (312) all_510_1 = all_226_1 % 50.83/7.74 | | | | % 50.83/7.74 | | | | COMBINE_EQS: (230), (292) imply: % 50.83/7.74 | | | | (313) all_558_4 = all_332_0 % 50.83/7.74 | | | | % 50.83/7.74 | | | | COMBINE_EQS: (223), (269) imply: % 50.83/7.74 | | | | (314) all_558_3 = all_332_1 % 50.83/7.74 | | | | % 50.83/7.74 | | | | REDUCE: (179), (246) imply: % 50.83/7.74 | | | | (315) sdtpldt0(all_548_0, xr) = all_558_0 % 50.83/7.74 | | | | % 50.83/7.74 | | | | BETA: splitting (125) gives: % 50.83/7.74 | | | | % 50.83/7.74 | | | | Case 1: % 50.83/7.74 | | | | | % 50.83/7.74 | | | | | (316) ~ (all_514_1 = 0) % 50.83/7.74 | | | | | % 50.83/7.74 | | | | | REDUCE: (299), (316) imply: % 50.83/7.74 | | | | | (317) $false % 50.83/7.74 | | | | | % 50.83/7.74 | | | | | CLOSE: (317) is inconsistent. % 50.83/7.74 | | | | | % 50.83/7.74 | | | | Case 2: % 50.83/7.74 | | | | | % 50.83/7.74 | | | | | (318) ~ (all_514_2 = 0) | all_514_0 = 0 % 50.83/7.74 | | | | | % 50.83/7.74 | | | | | BETA: splitting (120) gives: % 50.83/7.74 | | | | | % 50.83/7.74 | | | | | Case 1: % 50.83/7.74 | | | | | | % 50.83/7.74 | | | | | | (319) ~ (all_512_1 = 0) % 50.83/7.74 | | | | | | % 50.83/7.74 | | | | | | REDUCE: (288), (319) imply: % 50.83/7.74 | | | | | | (320) $false % 50.83/7.74 | | | | | | % 50.83/7.74 | | | | | | CLOSE: (320) is inconsistent. % 50.83/7.74 | | | | | | % 50.83/7.74 | | | | | Case 2: % 50.83/7.74 | | | | | | % 50.83/7.74 | | | | | | (321) ~ (all_512_2 = 0) | all_512_0 = 0 % 50.83/7.74 | | | | | | % 50.83/7.74 | | | | | | BETA: splitting (318) gives: % 50.83/7.74 | | | | | | % 50.83/7.74 | | | | | | Case 1: % 50.83/7.74 | | | | | | | % 50.83/7.74 | | | | | | | (322) ~ (all_514_2 = 0) % 50.83/7.74 | | | | | | | % 50.83/7.74 | | | | | | | REDUCE: (301), (322) imply: % 50.83/7.74 | | | | | | | (323) $false % 50.83/7.74 | | | | | | | % 50.83/7.74 | | | | | | | CLOSE: (323) is inconsistent. % 50.83/7.74 | | | | | | | % 50.83/7.74 | | | | | | Case 2: % 50.83/7.74 | | | | | | | % 50.83/7.74 | | | | | | | (324) all_514_0 = 0 % 50.83/7.74 | | | | | | | % 50.83/7.74 | | | | | | | COMBINE_EQS: (277), (324) imply: % 50.83/7.74 | | | | | | | (325) all_516_2 = 0 % 50.83/7.74 | | | | | | | % 50.83/7.74 | | | | | | | BETA: splitting (321) gives: % 50.83/7.74 | | | | | | | % 50.83/7.74 | | | | | | | Case 1: % 50.83/7.74 | | | | | | | | % 50.83/7.74 | | | | | | | | (326) ~ (all_512_2 = 0) % 50.83/7.74 | | | | | | | | % 50.83/7.74 | | | | | | | | REDUCE: (308), (326) imply: % 50.83/7.74 | | | | | | | | (327) $false % 50.83/7.74 | | | | | | | | % 50.83/7.74 | | | | | | | | CLOSE: (327) is inconsistent. % 50.83/7.74 | | | | | | | | % 50.83/7.74 | | | | | | | Case 2: % 50.83/7.74 | | | | | | | | % 50.83/7.74 | | | | | | | | (328) all_512_0 = 0 % 50.83/7.74 | | | | | | | | % 50.83/7.74 | | | | | | | | COMBINE_EQS: (276), (328) imply: % 50.83/7.74 | | | | | | | | (329) all_516_1 = 0 % 50.83/7.74 | | | | | | | | % 50.83/7.74 | | | | | | | | BETA: splitting (130) gives: % 50.83/7.74 | | | | | | | | % 50.83/7.74 | | | | | | | | Case 1: % 50.83/7.74 | | | | | | | | | % 50.83/7.74 | | | | | | | | | (330) ~ (all_516_1 = 0) % 50.83/7.74 | | | | | | | | | % 50.83/7.74 | | | | | | | | | REDUCE: (329), (330) imply: % 50.83/7.74 | | | | | | | | | (331) $false % 50.83/7.74 | | | | | | | | | % 50.83/7.74 | | | | | | | | | CLOSE: (331) is inconsistent. % 50.83/7.74 | | | | | | | | | % 50.83/7.74 | | | | | | | | Case 2: % 50.83/7.74 | | | | | | | | | % 50.83/7.74 | | | | | | | | | (332) ~ (all_516_2 = 0) | all_516_0 = 0 % 50.83/7.74 | | | | | | | | | % 50.83/7.74 | | | | | | | | | BETA: splitting (332) gives: % 50.83/7.74 | | | | | | | | | % 50.83/7.74 | | | | | | | | | Case 1: % 50.83/7.74 | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | (333) ~ (all_516_2 = 0) % 50.83/7.74 | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | REDUCE: (325), (333) imply: % 50.83/7.74 | | | | | | | | | | (334) $false % 50.83/7.74 | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | CLOSE: (334) is inconsistent. % 50.83/7.74 | | | | | | | | | | % 50.83/7.74 | | | | | | | | | Case 2: % 50.83/7.74 | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | (335) all_516_0 = 0 % 50.83/7.74 | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | COMBINE_EQS: (248), (335) imply: % 50.83/7.74 | | | | | | | | | | (336) all_226_1 = 0 % 50.83/7.74 | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | COMBINE_EQS: (312), (336) imply: % 50.83/7.74 | | | | | | | | | | (337) all_510_1 = 0 % 50.83/7.74 | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | BETA: splitting (115) gives: % 50.83/7.74 | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | Case 1: % 50.83/7.74 | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | (338) ~ (all_510_1 = 0) % 50.83/7.74 | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | REDUCE: (337), (338) imply: % 50.83/7.74 | | | | | | | | | | | (339) $false % 50.83/7.74 | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | CLOSE: (339) is inconsistent. % 50.83/7.74 | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | Case 2: % 50.83/7.74 | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | (340) ~ (all_510_2 = 0) | all_510_0 = 0 % 50.83/7.74 | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | BETA: splitting (340) gives: % 50.83/7.74 | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | Case 1: % 50.83/7.74 | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | (341) ~ (all_510_2 = 0) % 50.83/7.74 | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | REDUCE: (291), (341) imply: % 50.83/7.74 | | | | | | | | | | | | (342) $false % 50.83/7.74 | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | CLOSE: (342) is inconsistent. % 50.83/7.74 | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | Case 2: % 50.83/7.74 | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | (343) all_510_0 = 0 % 50.83/7.74 | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | COMBINE_EQS: (310), (343) imply: % 50.83/7.74 | | | | | | | | | | | | (344) all_332_1 = 0 % 50.83/7.74 | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | COMBINE_EQS: (269), (344) imply: % 50.83/7.74 | | | | | | | | | | | | (345) all_548_2 = 0 % 50.83/7.74 | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | COMBINE_EQS: (314), (344) imply: % 50.83/7.74 | | | | | | | | | | | | (346) all_558_3 = 0 % 50.83/7.74 | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | BETA: splitting (171) gives: % 50.83/7.74 | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | Case 1: % 50.83/7.74 | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | (347) ~ (all_548_2 = 0) % 50.83/7.74 | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | REDUCE: (345), (347) imply: % 50.83/7.74 | | | | | | | | | | | | | (348) $false % 50.83/7.74 | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | CLOSE: (348) is inconsistent. % 50.83/7.74 | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | Case 2: % 50.83/7.74 | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | (349) all_548_0 = sz00 & all_548_1 = sz00 % 50.83/7.74 | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | ALPHA: (349) implies: % 50.83/7.74 | | | | | | | | | | | | | (350) all_548_0 = sz00 % 50.83/7.74 | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | REDUCE: (315), (350) imply: % 50.83/7.74 | | | | | | | | | | | | | (351) sdtpldt0(sz00, xr) = all_558_0 % 50.83/7.74 | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | BETA: splitting (110) gives: % 50.83/7.74 | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | Case 1: % 50.83/7.74 | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | (352) ~ (all_332_1 = 0) % 50.83/7.74 | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | REDUCE: (344), (352) imply: % 50.83/7.74 | | | | | | | | | | | | | | (353) $false % 50.83/7.74 | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | CLOSE: (353) is inconsistent. % 50.83/7.74 | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | Case 2: % 50.83/7.74 | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | (354) all_332_0 = 0 % 50.83/7.74 | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | COMBINE_EQS: (313), (354) imply: % 50.83/7.74 | | | | | | | | | | | | | | (355) all_558_4 = 0 % 50.83/7.74 | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | BETA: splitting (180) gives: % 50.83/7.74 | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | Case 1: % 50.83/7.74 | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | (356) ~ (all_558_2 = 0) % 50.83/7.74 | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | REDUCE: (252), (356) imply: % 50.83/7.74 | | | | | | | | | | | | | | | (357) $false % 50.83/7.74 | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | CLOSE: (357) is inconsistent. % 50.83/7.74 | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | Case 2: % 50.83/7.74 | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | (358) ~ (all_558_3 = 0) | ~ (all_558_4 = 0) | % 50.83/7.74 | | | | | | | | | | | | | | | all_558_0 = all_42_0 % 50.83/7.74 | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | BETA: splitting (358) gives: % 50.83/7.74 | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | Case 1: % 50.83/7.74 | | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | | (359) ~ (all_558_3 = 0) % 50.83/7.74 | | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | | REDUCE: (346), (359) imply: % 50.83/7.74 | | | | | | | | | | | | | | | | (360) $false % 50.83/7.74 | | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | | CLOSE: (360) is inconsistent. % 50.83/7.74 | | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | Case 2: % 50.83/7.74 | | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | | (361) ~ (all_558_4 = 0) | all_558_0 = all_42_0 % 50.83/7.74 | | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | | BETA: splitting (361) gives: % 50.83/7.74 | | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | | Case 1: % 50.83/7.74 | | | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | | | (362) ~ (all_558_4 = 0) % 50.83/7.74 | | | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | | | REDUCE: (355), (362) imply: % 50.83/7.74 | | | | | | | | | | | | | | | | | (363) $false % 50.83/7.74 | | | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | | | CLOSE: (363) is inconsistent. % 50.83/7.74 | | | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | | Case 2: % 50.83/7.74 | | | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | | | (364) all_558_0 = all_42_0 % 50.83/7.74 | | | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | | | REDUCE: (351), (364) imply: % 50.83/7.74 | | | | | | | | | | | | | | | | | (365) sdtpldt0(sz00, xr) = all_42_0 % 50.83/7.74 | | | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with xr, all_42_0, xr, sz00, % 50.83/7.74 | | | | | | | | | | | | | | | | | simplifying with (77), (365) gives: % 50.83/7.74 | | | | | | | | | | | | | | | | | (366) all_42_0 = xr % 50.83/7.74 | | | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | | | REDUCE: (38), (366) imply: % 50.83/7.74 | | | | | | | | | | | | | | | | | (367) $false % 50.83/7.74 | | | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | | | CLOSE: (367) is inconsistent. % 50.83/7.74 | | | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | | End of split % 50.83/7.74 | | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | | End of split % 50.83/7.74 | | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | | End of split % 50.83/7.74 | | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | | End of split % 50.83/7.74 | | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | | End of split % 50.83/7.74 | | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | | End of split % 50.83/7.74 | | | | | | | | | | | % 50.83/7.74 | | | | | | | | | | End of split % 50.83/7.74 | | | | | | | | | | % 50.83/7.74 | | | | | | | | | End of split % 50.83/7.74 | | | | | | | | | % 50.83/7.74 | | | | | | | | End of split % 50.83/7.74 | | | | | | | | % 50.83/7.74 | | | | | | | End of split % 50.83/7.74 | | | | | | | % 50.83/7.74 | | | | | | End of split % 50.83/7.74 | | | | | | % 50.83/7.74 | | | | | End of split % 50.83/7.74 | | | | | % 50.83/7.74 | | | | End of split % 50.83/7.74 | | | | % 50.83/7.74 | | | End of split % 50.83/7.74 | | | % 50.83/7.74 | | End of split % 50.83/7.74 | | % 50.83/7.74 | End of split % 50.83/7.74 | % 50.83/7.74 End of proof % 50.83/7.74 % SZS output end Proof for theBenchmark % 50.83/7.74 % 50.83/7.74 7153ms %------------------------------------------------------------------------------