%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : NUM480+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 : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 11:48:03 EDT 2023 % Result : Theorem 16.40s 3.09s % Output : Proof 29.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUM480+1 : TPTP v8.1.2. Released v4.0.0. % 0.10/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.10/0.33 % Computer : n003.cluster.edu % 0.10/0.33 % Model : x86_64 x86_64 % 0.10/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.33 % Memory : 8042.1875MB % 0.10/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.33 % CPULimit : 300 % 0.10/0.33 % WCLimit : 300 % 0.10/0.33 % DateTime : Fri Aug 25 15:35:23 EDT 2023 % 0.10/0.33 % CPUTime : % 0.16/0.61 ________ _____ % 0.16/0.61 ___ __ \_________(_)________________________________ % 0.16/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.16/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.16/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.16/0.61 % 0.16/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.16/0.61 (2023-06-19) % 0.16/0.61 % 0.16/0.61 (c) Philipp Rümmer, 2009-2023 % 0.16/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.16/0.61 Amanda Stjerna. % 0.16/0.61 Free software under BSD-3-Clause. % 0.16/0.61 % 0.16/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.16/0.61 % 0.16/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.16/0.62 Running up to 7 provers in parallel. % 0.16/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.16/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.16/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.16/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.16/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.16/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.16/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.61/1.29 Prover 1: Preprocessing ... % 3.61/1.29 Prover 4: Preprocessing ... % 3.61/1.34 Prover 5: Preprocessing ... % 3.61/1.34 Prover 2: Preprocessing ... % 3.61/1.34 Prover 3: Preprocessing ... % 3.61/1.34 Prover 6: Preprocessing ... % 3.61/1.35 Prover 0: Preprocessing ... % 10.83/2.35 Prover 1: Constructing countermodel ... % 10.83/2.36 Prover 3: Constructing countermodel ... % 10.83/2.38 Prover 6: Proving ... % 11.95/2.50 Prover 5: Constructing countermodel ... % 13.04/2.64 Prover 2: Proving ... % 13.04/2.79 Prover 4: Constructing countermodel ... % 15.16/2.94 Prover 0: Proving ... % 15.81/3.08 Prover 3: proved (2439ms) % 15.81/3.08 % 16.40/3.09 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 16.40/3.09 % 16.40/3.09 Prover 5: stopped % 16.40/3.09 Prover 2: stopped % 16.40/3.10 Prover 6: stopped % 16.40/3.11 Prover 0: stopped % 16.40/3.11 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 16.40/3.11 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 16.40/3.11 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 16.40/3.11 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 16.40/3.14 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 17.42/3.25 Prover 8: Preprocessing ... % 17.42/3.28 Prover 11: Preprocessing ... % 17.42/3.29 Prover 7: Preprocessing ... % 17.42/3.29 Prover 10: Preprocessing ... % 17.42/3.41 Prover 13: Preprocessing ... % 19.33/3.54 Prover 10: Constructing countermodel ... % 19.33/3.56 Prover 8: Warning: ignoring some quantifiers % 19.33/3.57 Prover 8: Constructing countermodel ... % 20.09/3.61 Prover 7: Constructing countermodel ... % 20.09/3.67 Prover 13: Constructing countermodel ... % 23.01/4.06 Prover 11: Constructing countermodel ... % 27.43/4.60 Prover 1: Found proof (size 446) % 27.43/4.61 Prover 1: proved (3974ms) % 27.43/4.61 Prover 13: stopped % 27.43/4.61 Prover 10: stopped % 27.43/4.61 Prover 11: stopped % 27.43/4.61 Prover 7: stopped % 27.43/4.61 Prover 8: stopped % 27.43/4.61 Prover 4: stopped % 27.43/4.61 % 27.43/4.61 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 27.43/4.61 % 28.01/4.72 % SZS output start Proof for theBenchmark % 28.01/4.73 Assumptions after simplification: % 28.01/4.73 --------------------------------- % 28.01/4.73 % 28.01/4.73 (mDefDiv) % 28.20/4.77 ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (doDivides0(v0, v1) = v2) | ~ % 28.20/4.78 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : (aNaturalNumber0(v1) = v4 % 28.20/4.78 & aNaturalNumber0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0))) | (( ~ (v2 = 0) % 28.20/4.78 | ? [v3: $i] : (sdtasdt0(v0, v3) = v1 & aNaturalNumber0(v3) = 0 & % 28.20/4.78 $i(v3))) & (v2 = 0 | ! [v3: $i] : ( ~ (sdtasdt0(v0, v3) = v1) | ~ % 28.20/4.78 $i(v3) | ? [v4: int] : ( ~ (v4 = 0) & aNaturalNumber0(v3) = v4))))) % 28.20/4.78 % 28.20/4.78 (mDefQuot) % 28.20/4.78 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v0 = sz00 | ~ % 28.20/4.78 (sdtsldt0(v1, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: % 28.20/4.78 any] : ? [v5: any] : (doDivides0(v0, v1) = v5 & aNaturalNumber0(v1) = v4 % 28.20/4.78 & aNaturalNumber0(v0) = v3 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0))) | % 28.20/4.78 ( ! [v3: $i] : (v3 = v2 | ~ (sdtasdt0(v0, v3) = v1) | ~ $i(v3) | ? [v4: % 28.20/4.78 int] : ( ~ (v4 = 0) & aNaturalNumber0(v3) = v4)) & ! [v3: $i] : ( ~ % 28.20/4.78 (sdtasdt0(v0, v2) = v3) | ~ $i(v2) | (v3 = v1 & aNaturalNumber0(v2) = % 28.20/4.78 0)))) % 28.20/4.78 % 28.20/4.78 (mDivTrans) % 28.20/4.79 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 28.20/4.79 (doDivides0(v0, v2) = v3) | ~ (doDivides0(v0, v1) = 0) | ~ $i(v2) | ~ % 28.20/4.79 $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: % 28.20/4.79 any] : (doDivides0(v1, v2) = v7 & aNaturalNumber0(v2) = v6 & % 28.20/4.79 aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v7 = 0) | ~ % 28.20/4.79 (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) % 28.20/4.79 % 28.20/4.79 (mMulAsso) % 28.20/4.79 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 28.20/4.79 (sdtasdt0(v3, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) % 28.20/4.79 | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? % 28.20/4.79 [v9: $i] : (sdtasdt0(v1, v2) = v8 & sdtasdt0(v0, v8) = v9 & % 28.20/4.79 aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & aNaturalNumber0(v0) % 28.20/4.79 = v5 & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v9 = % 28.20/4.79 v4))) % 28.20/4.79 % 28.20/4.79 (mMulCanc) % 28.20/4.79 $i(sz00) & ! [v0: $i] : (v0 = sz00 | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) % 28.20/4.79 | ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v2 = v1 | ~ % 28.20/4.79 (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | ~ % 28.20/4.79 $i(v1) | ? [v5: any] : ? [v6: any] : ? [v7: $i] : ? [v8: $i] : % 28.20/4.79 (sdtasdt0(v2, v0) = v8 & sdtasdt0(v1, v0) = v7 & aNaturalNumber0(v2) = v6 % 28.20/4.79 & aNaturalNumber0(v1) = v5 & $i(v8) & $i(v7) & ( ~ (v6 = 0) | ~ (v5 = % 28.20/4.79 0) | ( ~ (v8 = v7) & ~ (v4 = v3)))))) % 28.20/4.79 % 28.20/4.79 (mMulComm) % 28.20/4.80 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 28.20/4.80 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 28.20/4.80 (sdtasdt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 % 28.20/4.80 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 28.20/4.80 % 28.20/4.80 (mSortsB_02) % 28.20/4.80 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 28.20/4.80 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 28.20/4.80 (aNaturalNumber0(v2) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = % 28.20/4.80 v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 28.20/4.80 % 28.20/4.80 (m__) % 28.20/4.80 $i(xn) & $i(xm) & $i(xl) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 28.20/4.80 $i] : ( ~ (v3 = v1) & sdtsldt0(v2, xl) = v3 & sdtsldt0(xm, xl) = v0 & % 28.20/4.80 sdtasdt0(xn, v0) = v1 & sdtasdt0(xn, xm) = v2 & $i(v3) & $i(v2) & $i(v1) & % 28.20/4.80 $i(v0)) % 28.20/4.80 % 28.20/4.80 (m__1524) % 28.20/4.80 aNaturalNumber0(xm) = 0 & aNaturalNumber0(xl) = 0 & $i(xm) & $i(xl) % 28.20/4.80 % 28.20/4.80 (m__1524_04) % 28.20/4.80 ~ (xl = sz00) & doDivides0(xl, xm) = 0 & $i(xm) & $i(xl) & $i(sz00) % 28.20/4.80 % 28.20/4.80 (m__1553) % 28.20/4.80 aNaturalNumber0(xn) = 0 & $i(xn) % 28.20/4.80 % 28.20/4.80 (m__1594) % 28.20/4.80 $i(xn) & $i(xm) & $i(xl) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 28.20/4.80 $i] : ? [v4: $i] : (sdtsldt0(v3, xl) = v4 & sdtsldt0(xm, xl) = v1 & % 28.20/4.80 sdtasdt0(v0, v1) = v2 & sdtasdt0(xn, xm) = v3 & sdtasdt0(xl, v4) = v2 & % 28.20/4.80 sdtasdt0(xl, xn) = v0 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 28.20/4.80 % 28.20/4.80 (function-axioms) % 28.20/4.81 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 28.20/4.81 (sdtsldt0(v3, v2) = v1) | ~ (sdtsldt0(v3, v2) = v0)) & ! [v0: % 28.20/4.81 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 28.20/4.81 : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ (doDivides0(v3, v2) = v0)) & ! % 28.20/4.81 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 28.20/4.81 $i] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) & ! % 28.20/4.81 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 28.20/4.81 (sdtmndt0(v3, v2) = v1) | ~ (sdtmndt0(v3, v2) = v0)) & ! [v0: % 28.20/4.81 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 28.20/4.81 : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ (sdtlseqdt0(v3, v2) = v0)) & ! % 28.20/4.81 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 28.20/4.81 (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 28.20/4.81 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | % 28.20/4.81 ~ (sdtpldt0(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 28.20/4.81 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) % 28.20/4.81 | ~ (aNaturalNumber0(v2) = v0)) % 28.20/4.81 % 28.20/4.81 Further assumptions not needed in the proof: % 28.20/4.81 -------------------------------------------- % 28.20/4.81 mAMDistr, mAddAsso, mAddCanc, mAddComm, mDefDiff, mDefLE, mDivLE, mDivMin, % 28.20/4.81 mDivSum, mIH, mIH_03, mLEAsym, mLENTr, mLERefl, mLETotal, mLETran, mMonAdd, % 28.20/4.81 mMonMul, mMonMul2, mNatSort, mSortsB, mSortsC, mSortsC_01, mZeroAdd, mZeroMul, % 28.20/4.81 m_AddZero, m_MulUnit, m_MulZero % 28.20/4.81 % 28.20/4.81 Those formulas are unsatisfiable: % 28.20/4.81 --------------------------------- % 28.20/4.81 % 28.20/4.81 Begin of proof % 28.20/4.81 | % 28.20/4.81 | ALPHA: (mMulCanc) implies: % 28.20/4.81 | (1) ! [v0: $i] : (v0 = sz00 | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) | % 28.20/4.81 | ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v2 = v1 | ~ % 28.20/4.81 | (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | % 28.20/4.81 | ~ $i(v1) | ? [v5: any] : ? [v6: any] : ? [v7: $i] : ? [v8: $i] % 28.20/4.81 | : (sdtasdt0(v2, v0) = v8 & sdtasdt0(v1, v0) = v7 & % 28.20/4.81 | aNaturalNumber0(v2) = v6 & aNaturalNumber0(v1) = v5 & $i(v8) & % 28.20/4.81 | $i(v7) & ( ~ (v6 = 0) | ~ (v5 = 0) | ( ~ (v8 = v7) & ~ (v4 = % 28.20/4.81 | v3)))))) % 28.20/4.81 | % 28.20/4.81 | ALPHA: (mDefQuot) implies: % 28.20/4.82 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v0 = sz00 | ~ (sdtsldt0(v1, % 28.20/4.82 | v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : % 28.20/4.82 | ? [v5: any] : (doDivides0(v0, v1) = v5 & aNaturalNumber0(v1) = v4 & % 28.20/4.82 | aNaturalNumber0(v0) = v3 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = % 28.20/4.82 | 0))) | ( ! [v3: $i] : (v3 = v2 | ~ (sdtasdt0(v0, v3) = v1) | % 28.20/4.82 | ~ $i(v3) | ? [v4: int] : ( ~ (v4 = 0) & aNaturalNumber0(v3) = % 28.20/4.82 | v4)) & ! [v3: $i] : ( ~ (sdtasdt0(v0, v2) = v3) | ~ $i(v2) | % 28.20/4.82 | (v3 = v1 & aNaturalNumber0(v2) = 0)))) % 28.20/4.82 | % 28.20/4.82 | ALPHA: (m__1524) implies: % 28.20/4.82 | (3) aNaturalNumber0(xl) = 0 % 28.20/4.82 | (4) aNaturalNumber0(xm) = 0 % 28.20/4.82 | % 28.20/4.82 | ALPHA: (m__1524_04) implies: % 28.20/4.82 | (5) ~ (xl = sz00) % 28.20/4.82 | (6) doDivides0(xl, xm) = 0 % 28.20/4.82 | % 28.20/4.82 | ALPHA: (m__1553) implies: % 28.20/4.82 | (7) aNaturalNumber0(xn) = 0 % 28.20/4.82 | % 28.20/4.82 | ALPHA: (m__1594) implies: % 28.20/4.82 | (8) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 28.20/4.82 | (sdtsldt0(v3, xl) = v4 & sdtsldt0(xm, xl) = v1 & sdtasdt0(v0, v1) = v2 % 28.20/4.82 | & sdtasdt0(xn, xm) = v3 & sdtasdt0(xl, v4) = v2 & sdtasdt0(xl, xn) = % 28.20/4.82 | v0 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 28.20/4.82 | % 28.20/4.82 | ALPHA: (m__) implies: % 28.20/4.82 | (9) $i(xl) % 28.20/4.82 | (10) $i(xm) % 28.20/4.82 | (11) $i(xn) % 28.20/4.82 | (12) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( ~ (v3 = v1) % 28.20/4.82 | & sdtsldt0(v2, xl) = v3 & sdtsldt0(xm, xl) = v0 & sdtasdt0(xn, v0) = % 28.20/4.82 | v1 & sdtasdt0(xn, xm) = v2 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 28.20/4.82 | % 28.20/4.82 | ALPHA: (function-axioms) implies: % 28.20/4.82 | (13) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 28.20/4.82 | : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = % 28.20/4.82 | v0)) % 28.20/4.82 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 28.20/4.82 | (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 28.20/4.83 | (15) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 28.20/4.83 | : ! [v3: $i] : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ % 28.20/4.83 | (doDivides0(v3, v2) = v0)) % 28.20/4.83 | (16) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 28.20/4.83 | (sdtsldt0(v3, v2) = v1) | ~ (sdtsldt0(v3, v2) = v0)) % 28.20/4.83 | % 28.20/4.83 | DELTA: instantiating (12) with fresh symbols all_35_0, all_35_1, all_35_2, % 28.20/4.83 | all_35_3 gives: % 28.20/4.83 | (17) ~ (all_35_0 = all_35_2) & sdtsldt0(all_35_1, xl) = all_35_0 & % 28.20/4.83 | sdtsldt0(xm, xl) = all_35_3 & sdtasdt0(xn, all_35_3) = all_35_2 & % 28.20/4.83 | sdtasdt0(xn, xm) = all_35_1 & $i(all_35_0) & $i(all_35_1) & % 28.20/4.83 | $i(all_35_2) & $i(all_35_3) % 28.20/4.83 | % 28.20/4.83 | ALPHA: (17) implies: % 28.20/4.83 | (18) ~ (all_35_0 = all_35_2) % 28.20/4.83 | (19) sdtasdt0(xn, xm) = all_35_1 % 28.20/4.83 | (20) sdtasdt0(xn, all_35_3) = all_35_2 % 28.20/4.83 | (21) sdtsldt0(xm, xl) = all_35_3 % 28.20/4.83 | (22) sdtsldt0(all_35_1, xl) = all_35_0 % 28.20/4.83 | % 28.20/4.83 | DELTA: instantiating (8) with fresh symbols all_37_0, all_37_1, all_37_2, % 28.20/4.83 | all_37_3, all_37_4 gives: % 28.20/4.83 | (23) sdtsldt0(all_37_1, xl) = all_37_0 & sdtsldt0(xm, xl) = all_37_3 & % 28.20/4.83 | sdtasdt0(all_37_4, all_37_3) = all_37_2 & sdtasdt0(xn, xm) = all_37_1 % 28.20/4.83 | & sdtasdt0(xl, all_37_0) = all_37_2 & sdtasdt0(xl, xn) = all_37_4 & % 28.20/4.83 | $i(all_37_0) & $i(all_37_1) & $i(all_37_2) & $i(all_37_3) & % 28.20/4.83 | $i(all_37_4) % 28.20/4.83 | % 28.20/4.83 | ALPHA: (23) implies: % 28.20/4.83 | (24) $i(all_37_4) % 28.20/4.83 | (25) $i(all_37_3) % 28.20/4.83 | (26) $i(all_37_1) % 28.20/4.83 | (27) $i(all_37_0) % 28.20/4.83 | (28) sdtasdt0(xl, xn) = all_37_4 % 28.20/4.83 | (29) sdtasdt0(xl, all_37_0) = all_37_2 % 28.20/4.83 | (30) sdtasdt0(xn, xm) = all_37_1 % 28.20/4.83 | (31) sdtasdt0(all_37_4, all_37_3) = all_37_2 % 28.20/4.83 | (32) sdtsldt0(xm, xl) = all_37_3 % 28.20/4.83 | (33) sdtsldt0(all_37_1, xl) = all_37_0 % 28.20/4.83 | % 28.20/4.83 | GROUND_INST: instantiating (14) with all_35_1, all_37_1, xm, xn, simplifying % 28.20/4.83 | with (19), (30) gives: % 28.20/4.83 | (34) all_37_1 = all_35_1 % 28.20/4.83 | % 28.20/4.83 | GROUND_INST: instantiating (16) with all_35_3, all_37_3, xl, xm, simplifying % 28.20/4.83 | with (21), (32) gives: % 28.20/4.83 | (35) all_37_3 = all_35_3 % 28.20/4.83 | % 28.20/4.84 | REDUCE: (33), (34) imply: % 28.20/4.84 | (36) sdtsldt0(all_35_1, xl) = all_37_0 % 28.20/4.84 | % 28.20/4.84 | REDUCE: (31), (35) imply: % 28.20/4.84 | (37) sdtasdt0(all_37_4, all_35_3) = all_37_2 % 28.20/4.84 | % 28.20/4.84 | REDUCE: (26), (34) imply: % 28.20/4.84 | (38) $i(all_35_1) % 28.20/4.84 | % 28.20/4.84 | REDUCE: (25), (35) imply: % 28.20/4.84 | (39) $i(all_35_3) % 28.20/4.84 | % 28.20/4.84 | GROUND_INST: instantiating (16) with all_35_0, all_37_0, xl, all_35_1, % 28.20/4.84 | simplifying with (22), (36) gives: % 28.20/4.84 | (40) all_37_0 = all_35_0 % 28.20/4.84 | % 28.20/4.84 | REDUCE: (29), (40) imply: % 28.20/4.84 | (41) sdtasdt0(xl, all_35_0) = all_37_2 % 28.20/4.84 | % 28.20/4.84 | REDUCE: (27), (40) imply: % 28.20/4.84 | (42) $i(all_35_0) % 28.20/4.84 | % 28.20/4.84 | GROUND_INST: instantiating (1) with xl, simplifying with (3), (9) gives: % 28.20/4.84 | (43) xl = sz00 | ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 28.20/4.84 | (v1 = v0 | ~ (sdtasdt0(xl, v1) = v3) | ~ (sdtasdt0(xl, v0) = v2) | % 28.20/4.84 | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: $i] : % 28.20/4.84 | ? [v7: $i] : (sdtasdt0(v1, xl) = v7 & sdtasdt0(v0, xl) = v6 & % 28.20/4.84 | aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & $i(v7) & % 28.20/4.84 | $i(v6) & ( ~ (v5 = 0) | ~ (v4 = 0) | ( ~ (v7 = v6) & ~ (v3 = % 28.20/4.84 | v2))))) % 28.20/4.84 | % 28.20/4.84 | GROUND_INST: instantiating (mMulComm) with xl, xn, all_37_4, simplifying with % 28.20/4.84 | (9), (11), (28) gives: % 28.20/4.84 | (44) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(xn, xl) = v2 & % 28.20/4.84 | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xl) = v0 & $i(v2) & ( ~ % 28.20/4.84 | (v1 = 0) | ~ (v0 = 0) | v2 = all_37_4)) % 28.20/4.84 | % 28.20/4.84 | GROUND_INST: instantiating (mSortsB_02) with xl, xn, all_37_4, simplifying % 28.20/4.84 | with (9), (11), (28) gives: % 28.20/4.84 | (45) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 28.20/4.84 | (aNaturalNumber0(all_37_4) = v2 & aNaturalNumber0(xn) = v1 & % 28.20/4.84 | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 28.20/4.84 | % 28.20/4.84 | GROUND_INST: instantiating (mMulComm) with xl, all_35_0, all_37_2, simplifying % 28.20/4.84 | with (9), (41), (42) gives: % 28.20/4.84 | (46) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_35_0, xl) = % 28.20/4.84 | v2 & aNaturalNumber0(all_35_0) = v1 & aNaturalNumber0(xl) = v0 & % 28.20/4.84 | $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = all_37_2)) % 28.20/4.84 | % 28.20/4.85 | GROUND_INST: instantiating (mSortsB_02) with xl, all_35_0, all_37_2, % 28.20/4.85 | simplifying with (9), (41), (42) gives: % 28.20/4.85 | (47) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 28.20/4.85 | (aNaturalNumber0(all_37_2) = v2 & aNaturalNumber0(all_35_0) = v1 & % 28.20/4.85 | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 28.20/4.85 | % 28.20/4.85 | GROUND_INST: instantiating (mMulComm) with xn, xm, all_35_1, simplifying with % 28.20/4.85 | (10), (11), (19) gives: % 28.20/4.85 | (48) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(xm, xn) = v2 & % 28.20/4.85 | aNaturalNumber0(xn) = v0 & aNaturalNumber0(xm) = v1 & $i(v2) & ( ~ % 28.20/4.85 | (v1 = 0) | ~ (v0 = 0) | v2 = all_35_1)) % 28.20/4.85 | % 28.20/4.85 | GROUND_INST: instantiating (mSortsB_02) with xn, xm, all_35_1, simplifying % 28.20/4.85 | with (10), (11), (19) gives: % 28.20/4.85 | (49) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 28.20/4.85 | (aNaturalNumber0(all_35_1) = v2 & aNaturalNumber0(xn) = v0 & % 28.20/4.85 | aNaturalNumber0(xm) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 28.20/4.85 | % 28.20/4.85 | GROUND_INST: instantiating (mMulComm) with xn, all_35_3, all_35_2, simplifying % 28.20/4.85 | with (11), (20), (39) gives: % 28.20/4.85 | (50) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_35_3, xn) = % 28.20/4.85 | v2 & aNaturalNumber0(all_35_3) = v1 & aNaturalNumber0(xn) = v0 & % 28.20/4.85 | $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = all_35_2)) % 28.20/4.85 | % 28.20/4.85 | GROUND_INST: instantiating (mSortsB_02) with xn, all_35_3, all_35_2, % 28.20/4.85 | simplifying with (11), (20), (39) gives: % 28.20/4.85 | (51) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 28.20/4.85 | (aNaturalNumber0(all_35_2) = v2 & aNaturalNumber0(all_35_3) = v1 & % 28.20/4.85 | aNaturalNumber0(xn) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 28.20/4.85 | % 28.20/4.85 | GROUND_INST: instantiating (mMulAsso) with xl, xn, all_35_3, all_37_4, % 28.20/4.85 | all_37_2, simplifying with (9), (11), (28), (37), (39) gives: % 28.20/4.85 | (52) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: $i] % 28.20/4.85 | : (sdtasdt0(xn, all_35_3) = v3 & sdtasdt0(xl, v3) = v4 & % 28.20/4.85 | aNaturalNumber0(all_35_3) = v2 & aNaturalNumber0(xn) = v1 & % 28.20/4.85 | aNaturalNumber0(xl) = v0 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = % 28.20/4.86 | 0) | ~ (v0 = 0) | v4 = all_37_2)) % 28.20/4.86 | % 28.20/4.86 | GROUND_INST: instantiating (mMulComm) with all_37_4, all_35_3, all_37_2, % 28.20/4.86 | simplifying with (24), (37), (39) gives: % 28.20/4.86 | (53) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_35_3, % 28.20/4.86 | all_37_4) = v2 & aNaturalNumber0(all_37_4) = v0 & % 28.20/4.86 | aNaturalNumber0(all_35_3) = v1 & $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) % 28.20/4.86 | | v2 = all_37_2)) % 28.20/4.86 | % 28.20/4.86 | GROUND_INST: instantiating (mSortsB_02) with all_37_4, all_35_3, all_37_2, % 28.20/4.86 | simplifying with (24), (37), (39) gives: % 28.20/4.86 | (54) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 28.20/4.86 | (aNaturalNumber0(all_37_2) = v2 & aNaturalNumber0(all_37_4) = v0 & % 28.20/4.86 | aNaturalNumber0(all_35_3) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = % 28.20/4.86 | 0)) % 28.20/4.86 | % 28.20/4.86 | GROUND_INST: instantiating (mDefDiv) with xl, xm, 0, simplifying with (6), % 28.20/4.86 | (9), (10) gives: % 28.20/4.86 | (55) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(xm) = v1 & % 28.20/4.86 | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) | ? [v0: % 28.20/4.86 | $i] : (sdtasdt0(xl, v0) = xm & aNaturalNumber0(v0) = 0 & $i(v0)) % 28.20/4.86 | % 28.20/4.86 | GROUND_INST: instantiating (2) with xl, xm, all_35_3, simplifying with (9), % 28.20/4.86 | (10), (21) gives: % 28.20/4.86 | (56) xl = sz00 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 28.20/4.86 | (doDivides0(xl, xm) = v2 & aNaturalNumber0(xm) = v1 & % 28.20/4.86 | aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = % 28.20/4.86 | 0))) | ( ! [v0: any] : (v0 = all_35_3 | ~ (sdtasdt0(xl, v0) = % 28.20/4.86 | xm) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 28.20/4.86 | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( ~ (sdtasdt0(xl, % 28.20/4.86 | all_35_3) = v0) | ~ $i(all_35_3) | (v0 = xm & % 28.20/4.86 | aNaturalNumber0(all_35_3) = 0))) % 28.20/4.86 | % 28.20/4.86 | GROUND_INST: instantiating (2) with xl, all_35_1, all_35_0, simplifying with % 28.20/4.86 | (9), (22), (38) gives: % 28.20/4.87 | (57) xl = sz00 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 28.20/4.87 | (doDivides0(xl, all_35_1) = v2 & aNaturalNumber0(all_35_1) = v1 & % 28.20/4.87 | aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = % 28.20/4.87 | 0))) | ( ! [v0: any] : (v0 = all_35_0 | ~ (sdtasdt0(xl, v0) = % 28.20/4.87 | all_35_1) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 28.20/4.87 | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( ~ (sdtasdt0(xl, % 28.20/4.87 | all_35_0) = v0) | ~ $i(all_35_0) | (v0 = all_35_1 & % 28.20/4.87 | aNaturalNumber0(all_35_0) = 0))) % 28.20/4.87 | % 28.20/4.87 | DELTA: instantiating (54) with fresh symbols all_52_0, all_52_1, all_52_2 % 28.20/4.87 | gives: % 28.20/4.87 | (58) aNaturalNumber0(all_37_2) = all_52_0 & aNaturalNumber0(all_37_4) = % 28.20/4.87 | all_52_2 & aNaturalNumber0(all_35_3) = all_52_1 & ( ~ (all_52_1 = 0) | % 28.20/4.87 | ~ (all_52_2 = 0) | all_52_0 = 0) % 28.20/4.87 | % 28.20/4.87 | ALPHA: (58) implies: % 28.20/4.87 | (59) aNaturalNumber0(all_35_3) = all_52_1 % 28.20/4.87 | (60) aNaturalNumber0(all_37_4) = all_52_2 % 28.20/4.87 | (61) aNaturalNumber0(all_37_2) = all_52_0 % 28.20/4.87 | (62) ~ (all_52_1 = 0) | ~ (all_52_2 = 0) | all_52_0 = 0 % 28.20/4.87 | % 28.20/4.87 | DELTA: instantiating (51) with fresh symbols all_54_0, all_54_1, all_54_2 % 28.20/4.87 | gives: % 28.20/4.87 | (63) aNaturalNumber0(all_35_2) = all_54_0 & aNaturalNumber0(all_35_3) = % 28.20/4.87 | all_54_1 & aNaturalNumber0(xn) = all_54_2 & ( ~ (all_54_1 = 0) | ~ % 28.20/4.87 | (all_54_2 = 0) | all_54_0 = 0) % 28.20/4.87 | % 28.20/4.87 | ALPHA: (63) implies: % 28.20/4.87 | (64) aNaturalNumber0(xn) = all_54_2 % 28.20/4.87 | (65) aNaturalNumber0(all_35_3) = all_54_1 % 28.20/4.87 | % 28.20/4.87 | DELTA: instantiating (49) with fresh symbols all_56_0, all_56_1, all_56_2 % 28.20/4.87 | gives: % 28.20/4.87 | (66) aNaturalNumber0(all_35_1) = all_56_0 & aNaturalNumber0(xn) = all_56_2 % 28.20/4.87 | & aNaturalNumber0(xm) = all_56_1 & ( ~ (all_56_1 = 0) | ~ (all_56_2 = % 28.20/4.87 | 0) | all_56_0 = 0) % 28.20/4.87 | % 28.20/4.87 | ALPHA: (66) implies: % 28.20/4.87 | (67) aNaturalNumber0(xm) = all_56_1 % 28.20/4.87 | (68) aNaturalNumber0(xn) = all_56_2 % 28.20/4.87 | % 28.20/4.87 | DELTA: instantiating (47) with fresh symbols all_58_0, all_58_1, all_58_2 % 28.20/4.87 | gives: % 28.20/4.87 | (69) aNaturalNumber0(all_37_2) = all_58_0 & aNaturalNumber0(all_35_0) = % 28.20/4.87 | all_58_1 & aNaturalNumber0(xl) = all_58_2 & ( ~ (all_58_1 = 0) | ~ % 28.20/4.87 | (all_58_2 = 0) | all_58_0 = 0) % 28.20/4.87 | % 28.20/4.87 | ALPHA: (69) implies: % 28.20/4.87 | (70) aNaturalNumber0(xl) = all_58_2 % 28.20/4.87 | (71) aNaturalNumber0(all_35_0) = all_58_1 % 28.20/4.87 | (72) aNaturalNumber0(all_37_2) = all_58_0 % 28.20/4.87 | % 28.20/4.87 | DELTA: instantiating (45) with fresh symbols all_60_0, all_60_1, all_60_2 % 28.20/4.87 | gives: % 28.20/4.87 | (73) aNaturalNumber0(all_37_4) = all_60_0 & aNaturalNumber0(xn) = all_60_1 % 28.20/4.87 | & aNaturalNumber0(xl) = all_60_2 & ( ~ (all_60_1 = 0) | ~ (all_60_2 = % 28.20/4.87 | 0) | all_60_0 = 0) % 28.20/4.87 | % 28.20/4.87 | ALPHA: (73) implies: % 28.20/4.87 | (74) aNaturalNumber0(xl) = all_60_2 % 28.20/4.87 | (75) aNaturalNumber0(xn) = all_60_1 % 28.20/4.88 | (76) aNaturalNumber0(all_37_4) = all_60_0 % 28.20/4.88 | (77) ~ (all_60_1 = 0) | ~ (all_60_2 = 0) | all_60_0 = 0 % 28.20/4.88 | % 28.20/4.88 | DELTA: instantiating (44) with fresh symbols all_62_0, all_62_1, all_62_2 % 28.20/4.88 | gives: % 28.20/4.88 | (78) sdtasdt0(xn, xl) = all_62_0 & aNaturalNumber0(xn) = all_62_1 & % 28.20/4.88 | aNaturalNumber0(xl) = all_62_2 & $i(all_62_0) & ( ~ (all_62_1 = 0) | % 28.20/4.88 | ~ (all_62_2 = 0) | all_62_0 = all_37_4) % 28.20/4.88 | % 28.20/4.88 | ALPHA: (78) implies: % 28.20/4.88 | (79) $i(all_62_0) % 28.20/4.88 | (80) aNaturalNumber0(xl) = all_62_2 % 28.20/4.88 | (81) aNaturalNumber0(xn) = all_62_1 % 28.20/4.88 | (82) sdtasdt0(xn, xl) = all_62_0 % 28.20/4.88 | (83) ~ (all_62_1 = 0) | ~ (all_62_2 = 0) | all_62_0 = all_37_4 % 28.20/4.88 | % 28.20/4.88 | DELTA: instantiating (50) with fresh symbols all_64_0, all_64_1, all_64_2 % 28.20/4.88 | gives: % 28.20/4.88 | (84) sdtasdt0(all_35_3, xn) = all_64_0 & aNaturalNumber0(all_35_3) = % 28.20/4.88 | all_64_1 & aNaturalNumber0(xn) = all_64_2 & $i(all_64_0) & ( ~ % 28.20/4.88 | (all_64_1 = 0) | ~ (all_64_2 = 0) | all_64_0 = all_35_2) % 28.20/4.88 | % 28.20/4.88 | ALPHA: (84) implies: % 28.20/4.88 | (85) aNaturalNumber0(xn) = all_64_2 % 28.20/4.88 | (86) aNaturalNumber0(all_35_3) = all_64_1 % 28.20/4.88 | (87) sdtasdt0(all_35_3, xn) = all_64_0 % 28.20/4.88 | (88) ~ (all_64_1 = 0) | ~ (all_64_2 = 0) | all_64_0 = all_35_2 % 28.20/4.88 | % 28.20/4.88 | DELTA: instantiating (46) with fresh symbols all_66_0, all_66_1, all_66_2 % 28.20/4.88 | gives: % 28.20/4.88 | (89) sdtasdt0(all_35_0, xl) = all_66_0 & aNaturalNumber0(all_35_0) = % 28.20/4.88 | all_66_1 & aNaturalNumber0(xl) = all_66_2 & $i(all_66_0) & ( ~ % 28.20/4.88 | (all_66_1 = 0) | ~ (all_66_2 = 0) | all_66_0 = all_37_2) % 28.20/4.88 | % 28.20/4.88 | ALPHA: (89) implies: % 28.20/4.88 | (90) aNaturalNumber0(xl) = all_66_2 % 28.20/4.88 | (91) aNaturalNumber0(all_35_0) = all_66_1 % 28.20/4.88 | (92) sdtasdt0(all_35_0, xl) = all_66_0 % 28.20/4.88 | % 28.20/4.88 | DELTA: instantiating (48) with fresh symbols all_68_0, all_68_1, all_68_2 % 28.20/4.88 | gives: % 28.20/4.88 | (93) sdtasdt0(xm, xn) = all_68_0 & aNaturalNumber0(xn) = all_68_2 & % 28.20/4.88 | aNaturalNumber0(xm) = all_68_1 & $i(all_68_0) & ( ~ (all_68_1 = 0) | % 28.20/4.88 | ~ (all_68_2 = 0) | all_68_0 = all_35_1) % 28.20/4.88 | % 28.20/4.88 | ALPHA: (93) implies: % 28.20/4.88 | (94) aNaturalNumber0(xm) = all_68_1 % 28.20/4.88 | (95) aNaturalNumber0(xn) = all_68_2 % 28.20/4.88 | (96) sdtasdt0(xm, xn) = all_68_0 % 28.20/4.88 | (97) ~ (all_68_1 = 0) | ~ (all_68_2 = 0) | all_68_0 = all_35_1 % 28.20/4.88 | % 28.20/4.88 | DELTA: instantiating (53) with fresh symbols all_70_0, all_70_1, all_70_2 % 28.20/4.88 | gives: % 28.20/4.88 | (98) sdtasdt0(all_35_3, all_37_4) = all_70_0 & aNaturalNumber0(all_37_4) = % 28.20/4.88 | all_70_2 & aNaturalNumber0(all_35_3) = all_70_1 & $i(all_70_0) & ( ~ % 28.20/4.88 | (all_70_1 = 0) | ~ (all_70_2 = 0) | all_70_0 = all_37_2) % 28.20/4.88 | % 28.20/4.88 | ALPHA: (98) implies: % 28.20/4.88 | (99) aNaturalNumber0(all_35_3) = all_70_1 % 28.20/4.88 | (100) aNaturalNumber0(all_37_4) = all_70_2 % 28.20/4.88 | (101) sdtasdt0(all_35_3, all_37_4) = all_70_0 % 28.20/4.88 | % 28.20/4.88 | DELTA: instantiating (52) with fresh symbols all_72_0, all_72_1, all_72_2, % 28.20/4.88 | all_72_3, all_72_4 gives: % 28.20/4.89 | (102) sdtasdt0(xn, all_35_3) = all_72_1 & sdtasdt0(xl, all_72_1) = all_72_0 % 28.20/4.89 | & aNaturalNumber0(all_35_3) = all_72_2 & aNaturalNumber0(xn) = % 28.20/4.89 | all_72_3 & aNaturalNumber0(xl) = all_72_4 & $i(all_72_0) & % 28.20/4.89 | $i(all_72_1) & ( ~ (all_72_2 = 0) | ~ (all_72_3 = 0) | ~ (all_72_4 % 28.20/4.89 | = 0) | all_72_0 = all_37_2) % 28.20/4.89 | % 28.20/4.89 | ALPHA: (102) implies: % 28.20/4.89 | (103) $i(all_72_1) % 28.20/4.89 | (104) aNaturalNumber0(xl) = all_72_4 % 28.20/4.89 | (105) aNaturalNumber0(xn) = all_72_3 % 28.20/4.89 | (106) aNaturalNumber0(all_35_3) = all_72_2 % 28.20/4.90 | (107) sdtasdt0(xl, all_72_1) = all_72_0 % 28.20/4.90 | (108) sdtasdt0(xn, all_35_3) = all_72_1 % 28.20/4.90 | (109) ~ (all_72_2 = 0) | ~ (all_72_3 = 0) | ~ (all_72_4 = 0) | all_72_0 % 28.20/4.90 | = all_37_2 % 28.20/4.90 | % 28.20/4.90 | BETA: splitting (43) gives: % 28.20/4.90 | % 28.20/4.90 | Case 1: % 28.20/4.90 | | % 28.20/4.90 | | (110) xl = sz00 % 28.20/4.90 | | % 28.20/4.90 | | REDUCE: (5), (110) imply: % 28.20/4.90 | | (111) $false % 28.20/4.90 | | % 28.20/4.90 | | CLOSE: (111) is inconsistent. % 28.20/4.90 | | % 28.20/4.90 | Case 2: % 28.20/4.90 | | % 28.20/4.90 | | (112) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 28.20/4.90 | | ~ (sdtasdt0(xl, v1) = v3) | ~ (sdtasdt0(xl, v0) = v2) | ~ % 28.20/4.90 | | $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: $i] : % 28.20/4.90 | | ? [v7: $i] : (sdtasdt0(v1, xl) = v7 & sdtasdt0(v0, xl) = v6 & % 28.20/4.90 | | aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & $i(v7) & % 28.20/4.90 | | $i(v6) & ( ~ (v5 = 0) | ~ (v4 = 0) | ( ~ (v7 = v6) & ~ (v3 = % 28.20/4.90 | | v2))))) % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with 0, all_62_2, xl, simplifying with (3), % 28.20/4.90 | | (80) gives: % 28.20/4.90 | | (113) all_62_2 = 0 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_62_2, all_66_2, xl, simplifying % 28.20/4.90 | | with (80), (90) gives: % 28.20/4.90 | | (114) all_66_2 = all_62_2 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_58_2, all_66_2, xl, simplifying % 28.20/4.90 | | with (70), (90) gives: % 28.20/4.90 | | (115) all_66_2 = all_58_2 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_62_2, all_72_4, xl, simplifying % 28.20/4.90 | | with (80), (104) gives: % 28.20/4.90 | | (116) all_72_4 = all_62_2 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_60_2, all_72_4, xl, simplifying % 28.20/4.90 | | with (74), (104) gives: % 28.20/4.90 | | (117) all_72_4 = all_60_2 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with 0, all_68_1, xm, simplifying with (4), % 28.20/4.90 | | (94) gives: % 28.20/4.90 | | (118) all_68_1 = 0 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_56_1, all_68_1, xm, simplifying % 28.20/4.90 | | with (67), (94) gives: % 28.20/4.90 | | (119) all_68_1 = all_56_1 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with 0, all_62_1, xn, simplifying with (7), % 28.20/4.90 | | (81) gives: % 28.20/4.90 | | (120) all_62_1 = 0 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_56_2, all_64_2, xn, simplifying % 28.20/4.90 | | with (68), (85) gives: % 28.20/4.90 | | (121) all_64_2 = all_56_2 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_54_2, all_68_2, xn, simplifying % 28.20/4.90 | | with (64), (95) gives: % 28.20/4.90 | | (122) all_68_2 = all_54_2 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_68_2, all_72_3, xn, simplifying % 28.20/4.90 | | with (95), (105) gives: % 28.20/4.90 | | (123) all_72_3 = all_68_2 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_64_2, all_72_3, xn, simplifying % 28.20/4.90 | | with (85), (105) gives: % 28.20/4.90 | | (124) all_72_3 = all_64_2 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_62_1, all_72_3, xn, simplifying % 28.20/4.90 | | with (81), (105) gives: % 28.20/4.90 | | (125) all_72_3 = all_62_1 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_60_1, all_72_3, xn, simplifying % 28.20/4.90 | | with (75), (105) gives: % 28.20/4.90 | | (126) all_72_3 = all_60_1 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_52_1, all_64_1, all_35_3, % 28.20/4.90 | | simplifying with (59), (86) gives: % 28.20/4.90 | | (127) all_64_1 = all_52_1 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_64_1, all_70_1, all_35_3, % 28.20/4.90 | | simplifying with (86), (99) gives: % 28.20/4.90 | | (128) all_70_1 = all_64_1 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_70_1, all_72_2, all_35_3, % 28.20/4.90 | | simplifying with (99), (106) gives: % 28.20/4.90 | | (129) all_72_2 = all_70_1 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_54_1, all_72_2, all_35_3, % 28.20/4.90 | | simplifying with (65), (106) gives: % 28.20/4.90 | | (130) all_72_2 = all_54_1 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_58_1, all_66_1, all_35_0, % 28.20/4.90 | | simplifying with (71), (91) gives: % 28.20/4.90 | | (131) all_66_1 = all_58_1 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_60_0, all_70_2, all_37_4, % 28.20/4.90 | | simplifying with (76), (100) gives: % 28.20/4.90 | | (132) all_70_2 = all_60_0 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_52_2, all_70_2, all_37_4, % 28.20/4.90 | | simplifying with (60), (100) gives: % 28.20/4.90 | | (133) all_70_2 = all_52_2 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (13) with all_52_0, all_58_0, all_37_2, % 28.20/4.90 | | simplifying with (61), (72) gives: % 28.20/4.90 | | (134) all_58_0 = all_52_0 % 28.20/4.90 | | % 28.20/4.90 | | GROUND_INST: instantiating (14) with all_35_2, all_72_1, all_35_3, xn, % 28.20/4.90 | | simplifying with (20), (108) gives: % 28.20/4.90 | | (135) all_72_1 = all_35_2 % 28.20/4.90 | | % 28.20/4.90 | | COMBINE_EQS: (129), (130) imply: % 28.20/4.90 | | (136) all_70_1 = all_54_1 % 28.20/4.90 | | % 28.20/4.90 | | SIMP: (136) implies: % 28.20/4.90 | | (137) all_70_1 = all_54_1 % 28.20/4.90 | | % 28.20/4.90 | | COMBINE_EQS: (125), (126) imply: % 28.20/4.90 | | (138) all_62_1 = all_60_1 % 28.20/4.90 | | % 28.20/4.90 | | SIMP: (138) implies: % 28.20/4.90 | | (139) all_62_1 = all_60_1 % 28.20/4.90 | | % 28.20/4.90 | | COMBINE_EQS: (124), (126) imply: % 28.20/4.90 | | (140) all_64_2 = all_60_1 % 28.20/4.90 | | % 28.20/4.90 | | SIMP: (140) implies: % 28.20/4.90 | | (141) all_64_2 = all_60_1 % 28.20/4.90 | | % 28.20/4.90 | | COMBINE_EQS: (123), (126) imply: % 28.20/4.90 | | (142) all_68_2 = all_60_1 % 28.20/4.90 | | % 28.20/4.90 | | SIMP: (142) implies: % 28.20/4.91 | | (143) all_68_2 = all_60_1 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (116), (117) imply: % 28.20/4.91 | | (144) all_62_2 = all_60_2 % 28.20/4.91 | | % 28.20/4.91 | | SIMP: (144) implies: % 28.20/4.91 | | (145) all_62_2 = all_60_2 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (128), (137) imply: % 28.20/4.91 | | (146) all_64_1 = all_54_1 % 28.20/4.91 | | % 28.20/4.91 | | SIMP: (146) implies: % 28.20/4.91 | | (147) all_64_1 = all_54_1 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (132), (133) imply: % 28.20/4.91 | | (148) all_60_0 = all_52_2 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (118), (119) imply: % 28.20/4.91 | | (149) all_56_1 = 0 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (122), (143) imply: % 28.20/4.91 | | (150) all_60_1 = all_54_2 % 28.20/4.91 | | % 28.20/4.91 | | SIMP: (150) implies: % 28.20/4.91 | | (151) all_60_1 = all_54_2 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (114), (115) imply: % 28.20/4.91 | | (152) all_62_2 = all_58_2 % 28.20/4.91 | | % 28.20/4.91 | | SIMP: (152) implies: % 28.20/4.91 | | (153) all_62_2 = all_58_2 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (127), (147) imply: % 28.20/4.91 | | (154) all_54_1 = all_52_1 % 28.20/4.91 | | % 28.20/4.91 | | SIMP: (154) implies: % 28.20/4.91 | | (155) all_54_1 = all_52_1 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (121), (141) imply: % 28.20/4.91 | | (156) all_60_1 = all_56_2 % 28.20/4.91 | | % 28.20/4.91 | | SIMP: (156) implies: % 28.20/4.91 | | (157) all_60_1 = all_56_2 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (120), (139) imply: % 28.20/4.91 | | (158) all_60_1 = 0 % 28.20/4.91 | | % 28.20/4.91 | | SIMP: (158) implies: % 28.20/4.91 | | (159) all_60_1 = 0 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (113), (145) imply: % 28.20/4.91 | | (160) all_60_2 = 0 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (145), (153) imply: % 28.20/4.91 | | (161) all_60_2 = all_58_2 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (151), (157) imply: % 28.20/4.91 | | (162) all_56_2 = all_54_2 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (157), (159) imply: % 28.20/4.91 | | (163) all_56_2 = 0 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (160), (161) imply: % 28.20/4.91 | | (164) all_58_2 = 0 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (162), (163) imply: % 28.20/4.91 | | (165) all_54_2 = 0 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (121), (163) imply: % 28.20/4.91 | | (166) all_64_2 = 0 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (122), (165) imply: % 28.20/4.91 | | (167) all_68_2 = 0 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (117), (160) imply: % 28.20/4.91 | | (168) all_72_4 = 0 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (126), (159) imply: % 28.20/4.91 | | (169) all_72_3 = 0 % 28.20/4.91 | | % 28.20/4.91 | | COMBINE_EQS: (130), (155) imply: % 28.20/4.91 | | (170) all_72_2 = all_52_1 % 28.20/4.91 | | % 28.20/4.91 | | REDUCE: (107), (135) imply: % 28.20/4.91 | | (171) sdtasdt0(xl, all_35_2) = all_72_0 % 28.20/4.91 | | % 28.20/4.91 | | REDUCE: (103), (135) imply: % 28.20/4.91 | | (172) $i(all_35_2) % 28.20/4.91 | | % 28.20/4.91 | | BETA: splitting (97) gives: % 28.20/4.91 | | % 28.20/4.91 | | Case 1: % 28.20/4.91 | | | % 28.20/4.91 | | | (173) ~ (all_68_1 = 0) % 28.20/4.91 | | | % 28.20/4.91 | | | REDUCE: (118), (173) imply: % 28.20/4.91 | | | (174) $false % 28.20/4.91 | | | % 28.20/4.91 | | | CLOSE: (174) is inconsistent. % 28.20/4.91 | | | % 28.20/4.91 | | Case 2: % 28.20/4.91 | | | % 28.20/4.91 | | | (175) ~ (all_68_2 = 0) | all_68_0 = all_35_1 % 28.20/4.91 | | | % 28.20/4.91 | | | BETA: splitting (56) gives: % 28.20/4.91 | | | % 28.20/4.91 | | | Case 1: % 28.20/4.91 | | | | % 28.20/4.91 | | | | (176) xl = sz00 % 28.20/4.91 | | | | % 28.20/4.91 | | | | REDUCE: (5), (176) imply: % 28.20/4.91 | | | | (177) $false % 28.20/4.91 | | | | % 28.20/4.91 | | | | CLOSE: (177) is inconsistent. % 28.20/4.91 | | | | % 28.20/4.91 | | | Case 2: % 28.20/4.91 | | | | % 28.20/4.91 | | | | (178) ? [v0: any] : ? [v1: any] : ? [v2: any] : (doDivides0(xl, % 28.20/4.91 | | | | xm) = v2 & aNaturalNumber0(xm) = v1 & aNaturalNumber0(xl) = % 28.20/4.91 | | | | v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) | ( ! [v0: % 28.20/4.91 | | | | any] : (v0 = all_35_3 | ~ (sdtasdt0(xl, v0) = xm) | ~ % 28.20/4.91 | | | | $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & aNaturalNumber0(v0) % 28.20/4.91 | | | | = v1)) & ! [v0: $i] : ( ~ (sdtasdt0(xl, all_35_3) = v0) % 28.20/4.91 | | | | | ~ $i(all_35_3) | (v0 = xm & aNaturalNumber0(all_35_3) = % 28.20/4.91 | | | | 0))) % 28.20/4.91 | | | | % 28.20/4.91 | | | | BETA: splitting (178) gives: % 28.20/4.91 | | | | % 28.20/4.91 | | | | Case 1: % 28.20/4.91 | | | | | % 28.20/4.92 | | | | | (179) ? [v0: any] : ? [v1: any] : ? [v2: any] : (doDivides0(xl, % 28.20/4.92 | | | | | xm) = v2 & aNaturalNumber0(xm) = v1 & aNaturalNumber0(xl) % 28.20/4.92 | | | | | = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 28.20/4.92 | | | | | % 28.20/4.92 | | | | | DELTA: instantiating (179) with fresh symbols all_100_0, all_100_1, % 28.20/4.92 | | | | | all_100_2 gives: % 28.20/4.92 | | | | | (180) doDivides0(xl, xm) = all_100_0 & aNaturalNumber0(xm) = % 28.20/4.92 | | | | | all_100_1 & aNaturalNumber0(xl) = all_100_2 & ( ~ (all_100_0 % 28.20/4.92 | | | | | = 0) | ~ (all_100_1 = 0) | ~ (all_100_2 = 0)) % 28.20/4.92 | | | | | % 28.20/4.92 | | | | | ALPHA: (180) implies: % 28.20/4.92 | | | | | (181) aNaturalNumber0(xl) = all_100_2 % 28.20/4.92 | | | | | (182) aNaturalNumber0(xm) = all_100_1 % 28.20/4.92 | | | | | (183) doDivides0(xl, xm) = all_100_0 % 28.20/4.92 | | | | | (184) ~ (all_100_0 = 0) | ~ (all_100_1 = 0) | ~ (all_100_2 = 0) % 28.20/4.92 | | | | | % 28.20/4.92 | | | | | GROUND_INST: instantiating (13) with 0, all_100_2, xl, simplifying % 28.20/4.92 | | | | | with (3), (181) gives: % 28.20/4.92 | | | | | (185) all_100_2 = 0 % 28.20/4.92 | | | | | % 28.20/4.92 | | | | | GROUND_INST: instantiating (13) with 0, all_100_1, xm, simplifying % 28.20/4.92 | | | | | with (4), (182) gives: % 28.20/4.92 | | | | | (186) all_100_1 = 0 % 28.20/4.92 | | | | | % 28.20/4.92 | | | | | GROUND_INST: instantiating (15) with 0, all_100_0, xm, xl, simplifying % 28.20/4.92 | | | | | with (6), (183) gives: % 28.20/4.92 | | | | | (187) all_100_0 = 0 % 28.20/4.92 | | | | | % 28.20/4.92 | | | | | BETA: splitting (184) gives: % 28.20/4.92 | | | | | % 28.20/4.92 | | | | | Case 1: % 28.20/4.92 | | | | | | % 28.20/4.92 | | | | | | (188) ~ (all_100_0 = 0) % 28.20/4.92 | | | | | | % 28.20/4.92 | | | | | | REDUCE: (187), (188) imply: % 28.20/4.92 | | | | | | (189) $false % 28.20/4.92 | | | | | | % 28.20/4.92 | | | | | | CLOSE: (189) is inconsistent. % 28.20/4.92 | | | | | | % 28.20/4.92 | | | | | Case 2: % 28.20/4.92 | | | | | | % 28.20/4.92 | | | | | | (190) ~ (all_100_1 = 0) | ~ (all_100_2 = 0) % 28.20/4.92 | | | | | | % 28.20/4.92 | | | | | | BETA: splitting (190) gives: % 28.20/4.92 | | | | | | % 28.20/4.92 | | | | | | Case 1: % 28.20/4.92 | | | | | | | % 28.20/4.92 | | | | | | | (191) ~ (all_100_1 = 0) % 28.20/4.92 | | | | | | | % 28.20/4.92 | | | | | | | REDUCE: (186), (191) imply: % 28.20/4.92 | | | | | | | (192) $false % 28.20/4.92 | | | | | | | % 28.20/4.92 | | | | | | | CLOSE: (192) is inconsistent. % 28.20/4.92 | | | | | | | % 28.20/4.92 | | | | | | Case 2: % 28.20/4.92 | | | | | | | % 28.20/4.92 | | | | | | | (193) ~ (all_100_2 = 0) % 28.20/4.92 | | | | | | | % 28.20/4.92 | | | | | | | REDUCE: (185), (193) imply: % 28.20/4.92 | | | | | | | (194) $false % 28.20/4.92 | | | | | | | % 28.20/4.92 | | | | | | | CLOSE: (194) is inconsistent. % 28.20/4.92 | | | | | | | % 28.20/4.92 | | | | | | End of split % 28.20/4.92 | | | | | | % 28.20/4.92 | | | | | End of split % 28.20/4.92 | | | | | % 28.20/4.92 | | | | Case 2: % 28.20/4.92 | | | | | % 28.20/4.92 | | | | | (195) ! [v0: any] : (v0 = all_35_3 | ~ (sdtasdt0(xl, v0) = xm) | % 28.20/4.92 | | | | | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 28.20/4.92 | | | | | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( ~ % 28.20/4.92 | | | | | (sdtasdt0(xl, all_35_3) = v0) | ~ $i(all_35_3) | (v0 = xm % 28.20/4.92 | | | | | & aNaturalNumber0(all_35_3) = 0)) % 28.20/4.92 | | | | | % 28.20/4.92 | | | | | ALPHA: (195) implies: % 28.20/4.92 | | | | | (196) ! [v0: any] : (v0 = all_35_3 | ~ (sdtasdt0(xl, v0) = xm) | % 28.20/4.92 | | | | | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 28.20/4.92 | | | | | aNaturalNumber0(v0) = v1)) % 28.20/4.92 | | | | | % 28.20/4.92 | | | | | BETA: splitting (55) gives: % 28.20/4.92 | | | | | % 28.20/4.92 | | | | | Case 1: % 28.20/4.92 | | | | | | % 28.20/4.92 | | | | | | (197) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(xm) = v1 & % 28.20/4.92 | | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 28.20/4.92 | | | | | | % 28.20/4.92 | | | | | | DELTA: instantiating (197) with fresh symbols all_102_0, all_102_1 % 28.20/4.92 | | | | | | gives: % 28.20/4.92 | | | | | | (198) aNaturalNumber0(xm) = all_102_0 & aNaturalNumber0(xl) = % 28.20/4.92 | | | | | | all_102_1 & ( ~ (all_102_0 = 0) | ~ (all_102_1 = 0)) % 28.20/4.92 | | | | | | % 28.20/4.92 | | | | | | ALPHA: (198) implies: % 28.20/4.92 | | | | | | (199) aNaturalNumber0(xl) = all_102_1 % 28.20/4.92 | | | | | | (200) aNaturalNumber0(xm) = all_102_0 % 28.20/4.92 | | | | | | (201) ~ (all_102_0 = 0) | ~ (all_102_1 = 0) % 28.20/4.92 | | | | | | % 28.20/4.92 | | | | | | GROUND_INST: instantiating (13) with 0, all_102_1, xl, simplifying % 28.20/4.92 | | | | | | with (3), (199) gives: % 28.20/4.92 | | | | | | (202) all_102_1 = 0 % 28.20/4.92 | | | | | | % 28.20/4.92 | | | | | | GROUND_INST: instantiating (13) with 0, all_102_0, xm, simplifying % 28.20/4.92 | | | | | | with (4), (200) gives: % 28.20/4.92 | | | | | | (203) all_102_0 = 0 % 28.20/4.92 | | | | | | % 28.20/4.92 | | | | | | BETA: splitting (201) gives: % 28.20/4.92 | | | | | | % 28.20/4.92 | | | | | | Case 1: % 28.20/4.92 | | | | | | | % 28.20/4.92 | | | | | | | (204) ~ (all_102_0 = 0) % 28.20/4.92 | | | | | | | % 28.20/4.92 | | | | | | | REDUCE: (203), (204) imply: % 28.20/4.92 | | | | | | | (205) $false % 28.20/4.92 | | | | | | | % 28.20/4.92 | | | | | | | CLOSE: (205) is inconsistent. % 28.20/4.92 | | | | | | | % 28.20/4.92 | | | | | | Case 2: % 28.20/4.92 | | | | | | | % 28.20/4.92 | | | | | | | (206) ~ (all_102_1 = 0) % 28.20/4.92 | | | | | | | % 28.20/4.92 | | | | | | | REDUCE: (202), (206) imply: % 28.20/4.92 | | | | | | | (207) $false % 28.20/4.92 | | | | | | | % 28.20/4.92 | | | | | | | CLOSE: (207) is inconsistent. % 28.20/4.92 | | | | | | | % 28.20/4.92 | | | | | | End of split % 28.20/4.92 | | | | | | % 28.20/4.92 | | | | | Case 2: % 28.20/4.92 | | | | | | % 28.20/4.93 | | | | | | (208) ? [v0: $i] : (sdtasdt0(xl, v0) = xm & aNaturalNumber0(v0) % 28.20/4.93 | | | | | | = 0 & $i(v0)) % 28.20/4.93 | | | | | | % 28.20/4.93 | | | | | | DELTA: instantiating (208) with fresh symbol all_102_0 gives: % 28.20/4.93 | | | | | | (209) sdtasdt0(xl, all_102_0) = xm & aNaturalNumber0(all_102_0) = % 28.20/4.93 | | | | | | 0 & $i(all_102_0) % 28.20/4.93 | | | | | | % 28.20/4.93 | | | | | | ALPHA: (209) implies: % 28.20/4.93 | | | | | | (210) $i(all_102_0) % 28.20/4.93 | | | | | | (211) aNaturalNumber0(all_102_0) = 0 % 28.20/4.93 | | | | | | (212) sdtasdt0(xl, all_102_0) = xm % 28.20/4.93 | | | | | | % 28.20/4.93 | | | | | | BETA: splitting (77) gives: % 28.20/4.93 | | | | | | % 28.20/4.93 | | | | | | Case 1: % 28.20/4.93 | | | | | | | % 28.20/4.93 | | | | | | | (213) ~ (all_60_1 = 0) % 28.20/4.93 | | | | | | | % 28.20/4.93 | | | | | | | REDUCE: (159), (213) imply: % 28.20/4.93 | | | | | | | (214) $false % 28.20/4.93 | | | | | | | % 28.20/4.93 | | | | | | | CLOSE: (214) is inconsistent. % 28.20/4.93 | | | | | | | % 28.20/4.93 | | | | | | Case 2: % 28.20/4.93 | | | | | | | % 28.20/4.93 | | | | | | | (215) ~ (all_60_2 = 0) | all_60_0 = 0 % 28.20/4.93 | | | | | | | % 28.20/4.93 | | | | | | | BETA: splitting (175) gives: % 28.20/4.93 | | | | | | | % 28.20/4.93 | | | | | | | Case 1: % 28.20/4.93 | | | | | | | | % 28.20/4.93 | | | | | | | | (216) ~ (all_68_2 = 0) % 28.20/4.93 | | | | | | | | % 28.20/4.93 | | | | | | | | REDUCE: (167), (216) imply: % 28.20/4.93 | | | | | | | | (217) $false % 28.20/4.93 | | | | | | | | % 28.20/4.93 | | | | | | | | CLOSE: (217) is inconsistent. % 28.20/4.93 | | | | | | | | % 28.20/4.93 | | | | | | | Case 2: % 28.20/4.93 | | | | | | | | % 28.20/4.93 | | | | | | | | (218) all_68_0 = all_35_1 % 28.20/4.93 | | | | | | | | % 28.20/4.93 | | | | | | | | REDUCE: (96), (218) imply: % 28.20/4.93 | | | | | | | | (219) sdtasdt0(xm, xn) = all_35_1 % 28.20/4.93 | | | | | | | | % 28.20/4.93 | | | | | | | | BETA: splitting (83) gives: % 28.20/4.93 | | | | | | | | % 28.20/4.93 | | | | | | | | Case 1: % 28.20/4.93 | | | | | | | | | % 28.20/4.93 | | | | | | | | | (220) ~ (all_62_1 = 0) % 28.20/4.93 | | | | | | | | | % 28.20/4.93 | | | | | | | | | REDUCE: (120), (220) imply: % 28.20/4.93 | | | | | | | | | (221) $false % 28.20/4.93 | | | | | | | | | % 28.20/4.93 | | | | | | | | | CLOSE: (221) is inconsistent. % 28.20/4.93 | | | | | | | | | % 28.20/4.93 | | | | | | | | Case 2: % 28.20/4.93 | | | | | | | | | % 28.20/4.93 | | | | | | | | | (222) ~ (all_62_2 = 0) | all_62_0 = all_37_4 % 28.20/4.93 | | | | | | | | | % 28.20/4.93 | | | | | | | | | BETA: splitting (222) gives: % 28.20/4.93 | | | | | | | | | % 28.20/4.93 | | | | | | | | | Case 1: % 28.20/4.93 | | | | | | | | | | % 28.20/4.93 | | | | | | | | | | (223) ~ (all_62_2 = 0) % 28.20/4.93 | | | | | | | | | | % 28.20/4.93 | | | | | | | | | | REDUCE: (113), (223) imply: % 28.20/4.93 | | | | | | | | | | (224) $false % 28.20/4.93 | | | | | | | | | | % 28.20/4.93 | | | | | | | | | | CLOSE: (224) is inconsistent. % 28.20/4.93 | | | | | | | | | | % 28.20/4.93 | | | | | | | | | Case 2: % 28.20/4.93 | | | | | | | | | | % 28.20/4.93 | | | | | | | | | | (225) all_62_0 = all_37_4 % 28.20/4.93 | | | | | | | | | | % 28.20/4.93 | | | | | | | | | | REDUCE: (82), (225) imply: % 28.20/4.93 | | | | | | | | | | (226) sdtasdt0(xn, xl) = all_37_4 % 28.20/4.93 | | | | | | | | | | % 28.20/4.93 | | | | | | | | | | BETA: splitting (215) gives: % 28.20/4.93 | | | | | | | | | | % 28.20/4.93 | | | | | | | | | | Case 1: % 28.20/4.93 | | | | | | | | | | | % 28.20/4.93 | | | | | | | | | | | (227) ~ (all_60_2 = 0) % 28.20/4.93 | | | | | | | | | | | % 28.20/4.93 | | | | | | | | | | | REDUCE: (160), (227) imply: % 28.20/4.93 | | | | | | | | | | | (228) $false % 28.20/4.93 | | | | | | | | | | | % 28.20/4.93 | | | | | | | | | | | CLOSE: (228) is inconsistent. % 28.20/4.93 | | | | | | | | | | | % 28.20/4.93 | | | | | | | | | | Case 2: % 28.20/4.93 | | | | | | | | | | | % 28.20/4.93 | | | | | | | | | | | (229) all_60_0 = 0 % 28.20/4.93 | | | | | | | | | | | % 28.20/4.93 | | | | | | | | | | | COMBINE_EQS: (148), (229) imply: % 28.20/4.93 | | | | | | | | | | | (230) all_52_2 = 0 % 28.20/4.93 | | | | | | | | | | | % 28.20/4.93 | | | | | | | | | | | SIMP: (230) implies: % 28.20/4.93 | | | | | | | | | | | (231) all_52_2 = 0 % 28.20/4.93 | | | | | | | | | | | % 28.20/4.93 | | | | | | | | | | | GROUND_INST: instantiating (112) with all_35_0, all_35_2, % 28.20/4.93 | | | | | | | | | | | all_37_2, all_72_0, simplifying with (41), (42), % 28.20/4.93 | | | | | | | | | | | (171), (172) gives: % 28.20/4.93 | | | | | | | | | | | (232) all_35_0 = all_35_2 | ? [v0: any] : ? [v1: any] % 28.20/4.93 | | | | | | | | | | | : ? [v2: $i] : ? [v3: $i] : (sdtasdt0(all_35_0, % 28.20/4.93 | | | | | | | | | | | xl) = v2 & sdtasdt0(all_35_2, xl) = v3 & % 28.20/4.93 | | | | | | | | | | | aNaturalNumber0(all_35_0) = v0 & % 28.20/4.93 | | | | | | | | | | | aNaturalNumber0(all_35_2) = v1 & $i(v3) & $i(v2) % 28.20/4.93 | | | | | | | | | | | & ( ~ (v1 = 0) | ~ (v0 = 0) | ( ~ (v3 = v2) & % 28.20/4.93 | | | | | | | | | | | ~ (all_72_0 = all_37_2)))) % 28.20/4.93 | | | | | | | | | | | % 28.20/4.93 | | | | | | | | | | | GROUND_INST: instantiating (112) with all_35_2, all_35_0, % 28.20/4.93 | | | | | | | | | | | all_72_0, all_37_2, simplifying with (41), (42), % 28.20/4.93 | | | | | | | | | | | (171), (172) gives: % 28.20/4.93 | | | | | | | | | | | (233) all_35_0 = all_35_2 | ? [v0: any] : ? [v1: any] % 28.20/4.93 | | | | | | | | | | | : ? [v2: $i] : ? [v3: $i] : (sdtasdt0(all_35_0, % 28.20/4.93 | | | | | | | | | | | xl) = v3 & sdtasdt0(all_35_2, xl) = v2 & % 28.20/4.93 | | | | | | | | | | | aNaturalNumber0(all_35_0) = v1 & % 28.20/4.93 | | | | | | | | | | | aNaturalNumber0(all_35_2) = v0 & $i(v3) & $i(v2) % 28.20/4.93 | | | | | | | | | | | & ( ~ (v1 = 0) | ~ (v0 = 0) | ( ~ (v3 = v2) & % 28.20/4.93 | | | | | | | | | | | ~ (all_72_0 = all_37_2)))) % 28.20/4.93 | | | | | | | | | | | % 28.20/4.93 | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with xl, all_35_2, % 28.20/4.93 | | | | | | | | | | | all_72_0, simplifying with (9), (171), (172) % 28.20/4.93 | | | | | | | | | | | gives: % 28.20/4.93 | | | | | | | | | | | (234) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 28.20/4.93 | | | | | | | | | | | (sdtasdt0(all_35_2, xl) = v2 & % 28.20/4.93 | | | | | | | | | | | aNaturalNumber0(all_35_2) = v1 & % 28.20/4.93 | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v2) & ( ~ (v1 = 0) % 28.20/4.93 | | | | | | | | | | | | ~ (v0 = 0) | v2 = all_72_0)) % 28.20/4.93 | | | | | | | | | | | % 28.20/4.94 | | | | | | | | | | | GROUND_INST: instantiating (mSortsB_02) with xl, all_35_2, % 28.20/4.94 | | | | | | | | | | | all_72_0, simplifying with (9), (171), (172) % 28.20/4.94 | | | | | | | | | | | gives: % 28.20/4.94 | | | | | | | | | | | (235) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 28.20/4.94 | | | | | | | | | | | (aNaturalNumber0(all_72_0) = v2 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(all_35_2) = v1 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 % 28.20/4.94 | | | | | | | | | | | = 0) | v2 = 0)) % 28.20/4.94 | | | | | | | | | | | % 28.20/4.94 | | | | | | | | | | | GROUND_INST: instantiating (196) with all_102_0, simplifying % 28.20/4.94 | | | | | | | | | | | with (210), (212) gives: % 28.20/4.94 | | | | | | | | | | | (236) all_102_0 = all_35_3 | ? [v0: int] : ( ~ (v0 = 0) % 28.20/4.94 | | | | | | | | | | | & aNaturalNumber0(all_102_0) = v0) % 28.20/4.94 | | | | | | | | | | | % 28.20/4.94 | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with xl, all_102_0, xm, % 28.20/4.94 | | | | | | | | | | | simplifying with (9), (210), (212) gives: % 28.20/4.94 | | | | | | | | | | | (237) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 28.20/4.94 | | | | | | | | | | | (sdtasdt0(all_102_0, xl) = v2 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(all_102_0) = v1 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v2) & ( ~ (v1 = 0) % 28.20/4.94 | | | | | | | | | | | | ~ (v0 = 0) | v2 = xm)) % 28.20/4.94 | | | | | | | | | | | % 28.20/4.94 | | | | | | | | | | | GROUND_INST: instantiating (mMulAsso) with xl, all_102_0, xn, % 28.20/4.94 | | | | | | | | | | | xm, all_35_1, simplifying with (9), (11), (210), % 28.20/4.94 | | | | | | | | | | | (212), (219) gives: % 28.20/4.94 | | | | | | | | | | | (238) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 28.20/4.94 | | | | | | | | | | | [v3: $i] : ? [v4: $i] : (sdtasdt0(all_102_0, xn) % 28.20/4.94 | | | | | | | | | | | = v3 & sdtasdt0(xl, v3) = v4 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(all_102_0) = v1 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(xn) = v2 & aNaturalNumber0(xl) = % 28.20/4.94 | | | | | | | | | | | v0 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = % 28.20/4.94 | | | | | | | | | | | 0) | ~ (v0 = 0) | v4 = all_35_1)) % 28.20/4.94 | | | | | | | | | | | % 28.20/4.94 | | | | | | | | | | | GROUND_INST: instantiating (mMulAsso) with xn, xl, all_35_3, % 28.20/4.94 | | | | | | | | | | | all_37_4, all_37_2, simplifying with (9), (11), % 28.20/4.94 | | | | | | | | | | | (37), (39), (226) gives: % 28.20/4.94 | | | | | | | | | | | (239) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 28.20/4.94 | | | | | | | | | | | [v3: $i] : ? [v4: $i] : (sdtasdt0(xn, v3) = v4 & % 28.20/4.94 | | | | | | | | | | | sdtasdt0(xl, all_35_3) = v3 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(all_35_3) = v2 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(xn) = v0 & aNaturalNumber0(xl) = % 28.20/4.94 | | | | | | | | | | | v1 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = % 28.20/4.94 | | | | | | | | | | | 0) | ~ (v0 = 0) | v4 = all_37_2)) % 28.20/4.94 | | | | | | | | | | | % 28.20/4.94 | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with all_35_3, xn, % 28.20/4.94 | | | | | | | | | | | all_64_0, simplifying with (11), (39), (87) gives: % 28.20/4.94 | | | | | | | | | | | (240) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 28.20/4.94 | | | | | | | | | | | (sdtasdt0(xn, all_35_3) = v2 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(all_35_3) = v0 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(xn) = v1 & $i(v2) & ( ~ (v1 = 0) % 28.20/4.94 | | | | | | | | | | | | ~ (v0 = 0) | v2 = all_64_0)) % 28.20/4.94 | | | | | | | | | | | % 28.20/4.94 | | | | | | | | | | | GROUND_INST: instantiating (mSortsB_02) with all_35_3, xn, % 28.20/4.94 | | | | | | | | | | | all_64_0, simplifying with (11), (39), (87) gives: % 28.20/4.94 | | | | | | | | | | | (241) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 28.20/4.94 | | | | | | | | | | | (aNaturalNumber0(all_64_0) = v2 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(all_35_3) = v0 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(xn) = v1 & ( ~ (v1 = 0) | ~ (v0 % 28.20/4.94 | | | | | | | | | | | = 0) | v2 = 0)) % 28.20/4.94 | | | | | | | | | | | % 28.20/4.94 | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with all_35_3, all_37_4, % 28.20/4.94 | | | | | | | | | | | all_70_0, simplifying with (24), (39), (101) % 28.20/4.94 | | | | | | | | | | | gives: % 28.20/4.94 | | | | | | | | | | | (242) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 28.20/4.94 | | | | | | | | | | | (sdtasdt0(all_37_4, all_35_3) = v2 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(all_37_4) = v1 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(all_35_3) = v0 & $i(v2) & ( ~ % 28.20/4.94 | | | | | | | | | | | (v1 = 0) | ~ (v0 = 0) | v2 = all_70_0)) % 28.20/4.94 | | | | | | | | | | | % 28.20/4.94 | | | | | | | | | | | GROUND_INST: instantiating (mSortsB_02) with all_35_3, % 28.20/4.94 | | | | | | | | | | | all_37_4, all_70_0, simplifying with (24), (39), % 28.20/4.94 | | | | | | | | | | | (101) gives: % 28.20/4.94 | | | | | | | | | | | (243) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 28.20/4.94 | | | | | | | | | | | (aNaturalNumber0(all_70_0) = v2 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(all_37_4) = v1 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(all_35_3) = v0 & ( ~ (v1 = 0) | % 28.20/4.94 | | | | | | | | | | | ~ (v0 = 0) | v2 = 0)) % 28.20/4.94 | | | | | | | | | | | % 28.20/4.94 | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with all_35_0, xl, % 28.20/4.94 | | | | | | | | | | | all_66_0, simplifying with (9), (42), (92) gives: % 28.20/4.94 | | | | | | | | | | | (244) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 28.20/4.94 | | | | | | | | | | | (sdtasdt0(xl, all_35_0) = v2 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(all_35_0) = v0 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(xl) = v1 & $i(v2) & ( ~ (v1 = 0) % 28.20/4.94 | | | | | | | | | | | | ~ (v0 = 0) | v2 = all_66_0)) % 28.20/4.94 | | | | | | | | | | | % 28.20/4.94 | | | | | | | | | | | GROUND_INST: instantiating (mSortsB_02) with all_35_0, xl, % 28.20/4.94 | | | | | | | | | | | all_66_0, simplifying with (9), (42), (92) gives: % 28.20/4.94 | | | | | | | | | | | (245) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 28.20/4.94 | | | | | | | | | | | (aNaturalNumber0(all_66_0) = v2 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(all_35_0) = v0 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(xl) = v1 & ( ~ (v1 = 0) | ~ (v0 % 28.20/4.94 | | | | | | | | | | | = 0) | v2 = 0)) % 28.20/4.94 | | | | | | | | | | | % 28.20/4.94 | | | | | | | | | | | DELTA: instantiating (245) with fresh symbols all_133_0, % 28.20/4.94 | | | | | | | | | | | all_133_1, all_133_2 gives: % 28.20/4.94 | | | | | | | | | | | (246) aNaturalNumber0(all_66_0) = all_133_0 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(all_35_0) = all_133_2 & % 28.20/4.94 | | | | | | | | | | | aNaturalNumber0(xl) = all_133_1 & ( ~ (all_133_1 = % 28.20/4.94 | | | | | | | | | | | 0) | ~ (all_133_2 = 0) | all_133_0 = 0) % 28.20/4.94 | | | | | | | | | | | % 28.20/4.94 | | | | | | | | | | | ALPHA: (246) implies: % 28.20/4.94 | | | | | | | | | | | (247) aNaturalNumber0(xl) = all_133_1 % 28.20/4.94 | | | | | | | | | | | (248) aNaturalNumber0(all_35_0) = all_133_2 % 28.20/4.94 | | | | | | | | | | | % 28.20/4.94 | | | | | | | | | | | DELTA: instantiating (235) with fresh symbols all_135_0, % 28.20/4.94 | | | | | | | | | | | all_135_1, all_135_2 gives: % 28.20/4.95 | | | | | | | | | | | (249) aNaturalNumber0(all_72_0) = all_135_0 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(all_35_2) = all_135_1 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(xl) = all_135_2 & ( ~ (all_135_1 = % 28.20/4.95 | | | | | | | | | | | 0) | ~ (all_135_2 = 0) | all_135_0 = 0) % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | ALPHA: (249) implies: % 28.20/4.95 | | | | | | | | | | | (250) aNaturalNumber0(xl) = all_135_2 % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | DELTA: instantiating (243) with fresh symbols all_137_0, % 28.20/4.95 | | | | | | | | | | | all_137_1, all_137_2 gives: % 28.20/4.95 | | | | | | | | | | | (251) aNaturalNumber0(all_70_0) = all_137_0 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(all_37_4) = all_137_1 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(all_35_3) = all_137_2 & ( ~ % 28.20/4.95 | | | | | | | | | | | (all_137_1 = 0) | ~ (all_137_2 = 0) | all_137_0 % 28.20/4.95 | | | | | | | | | | | = 0) % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | ALPHA: (251) implies: % 28.20/4.95 | | | | | | | | | | | (252) aNaturalNumber0(all_35_3) = all_137_2 % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | DELTA: instantiating (241) with fresh symbols all_139_0, % 28.20/4.95 | | | | | | | | | | | all_139_1, all_139_2 gives: % 28.20/4.95 | | | | | | | | | | | (253) aNaturalNumber0(all_64_0) = all_139_0 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(all_35_3) = all_139_2 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(xn) = all_139_1 & ( ~ (all_139_1 = % 28.20/4.95 | | | | | | | | | | | 0) | ~ (all_139_2 = 0) | all_139_0 = 0) % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | ALPHA: (253) implies: % 28.20/4.95 | | | | | | | | | | | (254) aNaturalNumber0(xn) = all_139_1 % 28.20/4.95 | | | | | | | | | | | (255) aNaturalNumber0(all_35_3) = all_139_2 % 28.20/4.95 | | | | | | | | | | | (256) aNaturalNumber0(all_64_0) = all_139_0 % 28.20/4.95 | | | | | | | | | | | (257) ~ (all_139_1 = 0) | ~ (all_139_2 = 0) | % 28.20/4.95 | | | | | | | | | | | all_139_0 = 0 % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | DELTA: instantiating (234) with fresh symbols all_141_0, % 28.20/4.95 | | | | | | | | | | | all_141_1, all_141_2 gives: % 28.20/4.95 | | | | | | | | | | | (258) sdtasdt0(all_35_2, xl) = all_141_0 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(all_35_2) = all_141_1 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(xl) = all_141_2 & $i(all_141_0) & % 28.20/4.95 | | | | | | | | | | | ( ~ (all_141_1 = 0) | ~ (all_141_2 = 0) | % 28.20/4.95 | | | | | | | | | | | all_141_0 = all_72_0) % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | ALPHA: (258) implies: % 28.20/4.95 | | | | | | | | | | | (259) aNaturalNumber0(xl) = all_141_2 % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | DELTA: instantiating (244) with fresh symbols all_143_0, % 28.20/4.95 | | | | | | | | | | | all_143_1, all_143_2 gives: % 28.20/4.95 | | | | | | | | | | | (260) sdtasdt0(xl, all_35_0) = all_143_0 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(all_35_0) = all_143_2 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(xl) = all_143_1 & $i(all_143_0) & % 28.20/4.95 | | | | | | | | | | | ( ~ (all_143_1 = 0) | ~ (all_143_2 = 0) | % 28.20/4.95 | | | | | | | | | | | all_143_0 = all_66_0) % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | ALPHA: (260) implies: % 28.20/4.95 | | | | | | | | | | | (261) aNaturalNumber0(xl) = all_143_1 % 28.20/4.95 | | | | | | | | | | | (262) aNaturalNumber0(all_35_0) = all_143_2 % 28.20/4.95 | | | | | | | | | | | (263) sdtasdt0(xl, all_35_0) = all_143_0 % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | DELTA: instantiating (240) with fresh symbols all_145_0, % 28.20/4.95 | | | | | | | | | | | all_145_1, all_145_2 gives: % 28.20/4.95 | | | | | | | | | | | (264) sdtasdt0(xn, all_35_3) = all_145_0 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(all_35_3) = all_145_2 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(xn) = all_145_1 & $i(all_145_0) & % 28.20/4.95 | | | | | | | | | | | ( ~ (all_145_1 = 0) | ~ (all_145_2 = 0) | % 28.20/4.95 | | | | | | | | | | | all_145_0 = all_64_0) % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | ALPHA: (264) implies: % 28.20/4.95 | | | | | | | | | | | (265) aNaturalNumber0(xn) = all_145_1 % 28.20/4.95 | | | | | | | | | | | (266) aNaturalNumber0(all_35_3) = all_145_2 % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | DELTA: instantiating (242) with fresh symbols all_147_0, % 28.20/4.95 | | | | | | | | | | | all_147_1, all_147_2 gives: % 28.20/4.95 | | | | | | | | | | | (267) sdtasdt0(all_37_4, all_35_3) = all_147_0 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(all_37_4) = all_147_1 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(all_35_3) = all_147_2 & % 28.20/4.95 | | | | | | | | | | | $i(all_147_0) & ( ~ (all_147_1 = 0) | ~ % 28.20/4.95 | | | | | | | | | | | (all_147_2 = 0) | all_147_0 = all_70_0) % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | ALPHA: (267) implies: % 28.20/4.95 | | | | | | | | | | | (268) aNaturalNumber0(all_35_3) = all_147_2 % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | DELTA: instantiating (237) with fresh symbols all_149_0, % 28.20/4.95 | | | | | | | | | | | all_149_1, all_149_2 gives: % 28.20/4.95 | | | | | | | | | | | (269) sdtasdt0(all_102_0, xl) = all_149_0 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(all_102_0) = all_149_1 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(xl) = all_149_2 & $i(all_149_0) & % 28.20/4.95 | | | | | | | | | | | ( ~ (all_149_1 = 0) | ~ (all_149_2 = 0) | % 28.20/4.95 | | | | | | | | | | | all_149_0 = xm) % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | ALPHA: (269) implies: % 28.20/4.95 | | | | | | | | | | | (270) aNaturalNumber0(xl) = all_149_2 % 28.20/4.95 | | | | | | | | | | | (271) aNaturalNumber0(all_102_0) = all_149_1 % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | DELTA: instantiating (239) with fresh symbols all_151_0, % 28.20/4.95 | | | | | | | | | | | all_151_1, all_151_2, all_151_3, all_151_4 gives: % 28.20/4.95 | | | | | | | | | | | (272) sdtasdt0(xn, all_151_1) = all_151_0 & sdtasdt0(xl, % 28.20/4.95 | | | | | | | | | | | all_35_3) = all_151_1 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(all_35_3) = all_151_2 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(xn) = all_151_4 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(xl) = all_151_3 & $i(all_151_0) & % 28.20/4.95 | | | | | | | | | | | $i(all_151_1) & ( ~ (all_151_2 = 0) | ~ % 28.20/4.95 | | | | | | | | | | | (all_151_3 = 0) | ~ (all_151_4 = 0) | all_151_0 % 28.20/4.95 | | | | | | | | | | | = all_37_2) % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | ALPHA: (272) implies: % 28.20/4.95 | | | | | | | | | | | (273) $i(all_151_1) % 28.20/4.95 | | | | | | | | | | | (274) $i(all_151_0) % 28.20/4.95 | | | | | | | | | | | (275) aNaturalNumber0(xl) = all_151_3 % 28.20/4.95 | | | | | | | | | | | (276) aNaturalNumber0(xn) = all_151_4 % 28.20/4.95 | | | | | | | | | | | (277) aNaturalNumber0(all_35_3) = all_151_2 % 28.20/4.95 | | | | | | | | | | | (278) sdtasdt0(xl, all_35_3) = all_151_1 % 28.20/4.95 | | | | | | | | | | | (279) sdtasdt0(xn, all_151_1) = all_151_0 % 28.20/4.95 | | | | | | | | | | | (280) ~ (all_151_2 = 0) | ~ (all_151_3 = 0) | ~ % 28.20/4.95 | | | | | | | | | | | (all_151_4 = 0) | all_151_0 = all_37_2 % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | DELTA: instantiating (238) with fresh symbols all_153_0, % 28.20/4.95 | | | | | | | | | | | all_153_1, all_153_2, all_153_3, all_153_4 gives: % 28.20/4.95 | | | | | | | | | | | (281) sdtasdt0(all_102_0, xn) = all_153_1 & sdtasdt0(xl, % 28.20/4.95 | | | | | | | | | | | all_153_1) = all_153_0 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(all_102_0) = all_153_3 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(xn) = all_153_2 & % 28.20/4.95 | | | | | | | | | | | aNaturalNumber0(xl) = all_153_4 & $i(all_153_0) & % 28.20/4.95 | | | | | | | | | | | $i(all_153_1) & ( ~ (all_153_2 = 0) | ~ % 28.20/4.95 | | | | | | | | | | | (all_153_3 = 0) | ~ (all_153_4 = 0) | all_153_0 % 28.20/4.95 | | | | | | | | | | | = all_35_1) % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | ALPHA: (281) implies: % 28.20/4.95 | | | | | | | | | | | (282) $i(all_153_1) % 28.20/4.95 | | | | | | | | | | | (283) aNaturalNumber0(xl) = all_153_4 % 28.20/4.95 | | | | | | | | | | | (284) aNaturalNumber0(xn) = all_153_2 % 28.20/4.95 | | | | | | | | | | | (285) aNaturalNumber0(all_102_0) = all_153_3 % 28.20/4.95 | | | | | | | | | | | (286) sdtasdt0(all_102_0, xn) = all_153_1 % 28.20/4.95 | | | | | | | | | | | % 28.20/4.95 | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_141_2, xl, % 28.20/4.95 | | | | | | | | | | | simplifying with (3), (259) gives: % 28.20/4.95 | | | | | | | | | | | (287) all_141_2 = 0 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_133_1, all_149_2, xl, % 28.20/4.96 | | | | | | | | | | | simplifying with (247), (270) gives: % 28.20/4.96 | | | | | | | | | | | (288) all_149_2 = all_133_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_141_2, all_151_3, xl, % 28.20/4.96 | | | | | | | | | | | simplifying with (259), (275) gives: % 28.20/4.96 | | | | | | | | | | | (289) all_151_3 = all_141_2 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_135_2, all_151_3, xl, % 28.20/4.96 | | | | | | | | | | | simplifying with (250), (275) gives: % 28.20/4.96 | | | | | | | | | | | (290) all_151_3 = all_135_2 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_149_2, all_153_4, xl, % 28.20/4.96 | | | | | | | | | | | simplifying with (270), (283) gives: % 28.20/4.96 | | | | | | | | | | | (291) all_153_4 = all_149_2 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_143_1, all_153_4, xl, % 28.20/4.96 | | | | | | | | | | | simplifying with (261), (283) gives: % 28.20/4.96 | | | | | | | | | | | (292) all_153_4 = all_143_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_141_2, all_153_4, xl, % 28.20/4.96 | | | | | | | | | | | simplifying with (259), (283) gives: % 28.20/4.96 | | | | | | | | | | | (293) all_153_4 = all_141_2 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_145_1, xn, % 28.20/4.96 | | | | | | | | | | | simplifying with (7), (265) gives: % 28.20/4.96 | | | | | | | | | | | (294) all_145_1 = 0 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_145_1, all_151_4, xn, % 28.20/4.96 | | | | | | | | | | | simplifying with (265), (276) gives: % 28.20/4.96 | | | | | | | | | | | (295) all_151_4 = all_145_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_151_4, all_153_2, xn, % 28.20/4.96 | | | | | | | | | | | simplifying with (276), (284) gives: % 28.20/4.96 | | | | | | | | | | | (296) all_153_2 = all_151_4 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_139_1, all_153_2, xn, % 28.20/4.96 | | | | | | | | | | | simplifying with (254), (284) gives: % 28.20/4.96 | | | | | | | | | | | (297) all_153_2 = all_139_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_145_2, all_147_2, % 28.20/4.96 | | | | | | | | | | | all_35_3, simplifying with (266), (268) gives: % 28.20/4.96 | | | | | | | | | | | (298) all_147_2 = all_145_2 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_139_2, all_147_2, % 28.20/4.96 | | | | | | | | | | | all_35_3, simplifying with (255), (268) gives: % 28.20/4.96 | | | | | | | | | | | (299) all_147_2 = all_139_2 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_137_2, all_147_2, % 28.20/4.96 | | | | | | | | | | | all_35_3, simplifying with (252), (268) gives: % 28.20/4.96 | | | | | | | | | | | (300) all_147_2 = all_137_2 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_52_1, all_151_2, % 28.20/4.96 | | | | | | | | | | | all_35_3, simplifying with (59), (277) gives: % 28.20/4.96 | | | | | | | | | | | (301) all_151_2 = all_52_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_145_2, all_151_2, % 28.20/4.96 | | | | | | | | | | | all_35_3, simplifying with (266), (277) gives: % 28.20/4.96 | | | | | | | | | | | (302) all_151_2 = all_145_2 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_58_1, all_143_2, % 28.20/4.96 | | | | | | | | | | | all_35_0, simplifying with (71), (262) gives: % 28.20/4.96 | | | | | | | | | | | (303) all_143_2 = all_58_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_133_2, all_143_2, % 28.20/4.96 | | | | | | | | | | | all_35_0, simplifying with (248), (262) gives: % 28.20/4.96 | | | | | | | | | | | (304) all_143_2 = all_133_2 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_153_3, all_102_0, % 28.20/4.96 | | | | | | | | | | | simplifying with (211), (285) gives: % 28.20/4.96 | | | | | | | | | | | (305) all_153_3 = 0 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_149_1, all_153_3, % 28.20/4.96 | | | | | | | | | | | all_102_0, simplifying with (271), (285) gives: % 28.20/4.96 | | | | | | | | | | | (306) all_153_3 = all_149_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | GROUND_INST: instantiating (14) with all_37_2, all_143_0, % 28.20/4.96 | | | | | | | | | | | all_35_0, xl, simplifying with (41), (263) gives: % 28.20/4.96 | | | | | | | | | | | (307) all_143_0 = all_37_2 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | COMBINE_EQS: (296), (297) imply: % 28.20/4.96 | | | | | | | | | | | (308) all_151_4 = all_139_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | SIMP: (308) implies: % 28.20/4.96 | | | | | | | | | | | (309) all_151_4 = all_139_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | COMBINE_EQS: (305), (306) imply: % 28.20/4.96 | | | | | | | | | | | (310) all_149_1 = 0 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | COMBINE_EQS: (291), (292) imply: % 28.20/4.96 | | | | | | | | | | | (311) all_149_2 = all_143_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | SIMP: (311) implies: % 28.20/4.96 | | | | | | | | | | | (312) all_149_2 = all_143_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | COMBINE_EQS: (292), (293) imply: % 28.20/4.96 | | | | | | | | | | | (313) all_143_1 = all_141_2 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | COMBINE_EQS: (301), (302) imply: % 28.20/4.96 | | | | | | | | | | | (314) all_145_2 = all_52_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | SIMP: (314) implies: % 28.20/4.96 | | | | | | | | | | | (315) all_145_2 = all_52_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | COMBINE_EQS: (289), (290) imply: % 28.20/4.96 | | | | | | | | | | | (316) all_141_2 = all_135_2 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | SIMP: (316) implies: % 28.20/4.96 | | | | | | | | | | | (317) all_141_2 = all_135_2 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | COMBINE_EQS: (295), (309) imply: % 28.20/4.96 | | | | | | | | | | | (318) all_145_1 = all_139_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | SIMP: (318) implies: % 28.20/4.96 | | | | | | | | | | | (319) all_145_1 = all_139_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | COMBINE_EQS: (288), (312) imply: % 28.20/4.96 | | | | | | | | | | | (320) all_143_1 = all_133_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | SIMP: (320) implies: % 28.20/4.96 | | | | | | | | | | | (321) all_143_1 = all_133_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | COMBINE_EQS: (299), (300) imply: % 28.20/4.96 | | | | | | | | | | | (322) all_139_2 = all_137_2 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | COMBINE_EQS: (298), (299) imply: % 28.20/4.96 | | | | | | | | | | | (323) all_145_2 = all_139_2 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | SIMP: (323) implies: % 28.20/4.96 | | | | | | | | | | | (324) all_145_2 = all_139_2 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | COMBINE_EQS: (294), (319) imply: % 28.20/4.96 | | | | | | | | | | | (325) all_139_1 = 0 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | SIMP: (325) implies: % 28.20/4.96 | | | | | | | | | | | (326) all_139_1 = 0 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | COMBINE_EQS: (315), (324) imply: % 28.20/4.96 | | | | | | | | | | | (327) all_139_2 = all_52_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | SIMP: (327) implies: % 28.20/4.96 | | | | | | | | | | | (328) all_139_2 = all_52_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | COMBINE_EQS: (313), (321) imply: % 28.20/4.96 | | | | | | | | | | | (329) all_141_2 = all_133_1 % 28.20/4.96 | | | | | | | | | | | % 28.20/4.96 | | | | | | | | | | | SIMP: (329) implies: % 29.07/4.96 | | | | | | | | | | | (330) all_141_2 = all_133_1 % 29.07/4.96 | | | | | | | | | | | % 29.07/4.96 | | | | | | | | | | | COMBINE_EQS: (303), (304) imply: % 29.07/4.96 | | | | | | | | | | | (331) all_133_2 = all_58_1 % 29.07/4.96 | | | | | | | | | | | % 29.07/4.96 | | | | | | | | | | | COMBINE_EQS: (287), (317) imply: % 29.07/4.96 | | | | | | | | | | | (332) all_135_2 = 0 % 29.07/4.96 | | | | | | | | | | | % 29.07/4.96 | | | | | | | | | | | COMBINE_EQS: (317), (330) imply: % 29.07/4.96 | | | | | | | | | | | (333) all_135_2 = all_133_1 % 29.07/4.96 | | | | | | | | | | | % 29.07/4.96 | | | | | | | | | | | COMBINE_EQS: (322), (328) imply: % 29.07/4.96 | | | | | | | | | | | (334) all_137_2 = all_52_1 % 29.07/4.96 | | | | | | | | | | | % 29.07/4.96 | | | | | | | | | | | SIMP: (334) implies: % 29.07/4.96 | | | | | | | | | | | (335) all_137_2 = all_52_1 % 29.07/4.96 | | | | | | | | | | | % 29.07/4.96 | | | | | | | | | | | COMBINE_EQS: (332), (333) imply: % 29.07/4.96 | | | | | | | | | | | (336) all_133_1 = 0 % 29.07/4.97 | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | COMBINE_EQS: (309), (326) imply: % 29.07/4.97 | | | | | | | | | | | (337) all_151_4 = 0 % 29.07/4.97 | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | COMBINE_EQS: (290), (332) imply: % 29.07/4.97 | | | | | | | | | | | (338) all_151_3 = 0 % 29.07/4.97 | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | BETA: splitting (236) gives: % 29.07/4.97 | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | Case 1: % 29.07/4.97 | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | (339) all_102_0 = all_35_3 % 29.07/4.97 | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | REDUCE: (286), (339) imply: % 29.07/4.97 | | | | | | | | | | | | (340) sdtasdt0(all_35_3, xn) = all_153_1 % 29.07/4.97 | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | REDUCE: (212), (339) imply: % 29.07/4.97 | | | | | | | | | | | | (341) sdtasdt0(xl, all_35_3) = xm % 29.07/4.97 | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | REDUCE: (211), (339) imply: % 29.07/4.97 | | | | | | | | | | | | (342) aNaturalNumber0(all_35_3) = 0 % 29.07/4.97 | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_52_1, 0, all_35_3, % 29.07/4.97 | | | | | | | | | | | | simplifying with (59), (342) gives: % 29.07/4.97 | | | | | | | | | | | | (343) all_52_1 = 0 % 29.07/4.97 | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | GROUND_INST: instantiating (14) with all_151_1, xm, all_35_3, % 29.07/4.97 | | | | | | | | | | | | xl, simplifying with (278), (341) gives: % 29.07/4.97 | | | | | | | | | | | | (344) all_151_1 = xm % 29.07/4.97 | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | GROUND_INST: instantiating (14) with all_64_0, all_153_1, xn, % 29.07/4.97 | | | | | | | | | | | | all_35_3, simplifying with (87), (340) gives: % 29.07/4.97 | | | | | | | | | | | | (345) all_153_1 = all_64_0 % 29.07/4.97 | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | COMBINE_EQS: (127), (343) imply: % 29.07/4.97 | | | | | | | | | | | | (346) all_64_1 = 0 % 29.07/4.97 | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | COMBINE_EQS: (170), (343) imply: % 29.07/4.97 | | | | | | | | | | | | (347) all_72_2 = 0 % 29.07/4.97 | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | COMBINE_EQS: (328), (343) imply: % 29.07/4.97 | | | | | | | | | | | | (348) all_139_2 = 0 % 29.07/4.97 | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | COMBINE_EQS: (301), (343) imply: % 29.07/4.97 | | | | | | | | | | | | (349) all_151_2 = 0 % 29.07/4.97 | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | REDUCE: (279), (344) imply: % 29.07/4.97 | | | | | | | | | | | | (350) sdtasdt0(xn, xm) = all_151_0 % 29.07/4.97 | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | REDUCE: (282), (345) imply: % 29.07/4.97 | | | | | | | | | | | | (351) $i(all_64_0) % 29.07/4.97 | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | BETA: splitting (62) gives: % 29.07/4.97 | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | Case 1: % 29.07/4.97 | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | (352) ~ (all_52_1 = 0) % 29.07/4.97 | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | REDUCE: (343), (352) imply: % 29.07/4.97 | | | | | | | | | | | | | (353) $false % 29.07/4.97 | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | CLOSE: (353) is inconsistent. % 29.07/4.97 | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | Case 2: % 29.07/4.97 | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | (354) ~ (all_52_2 = 0) | all_52_0 = 0 % 29.07/4.97 | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | BETA: splitting (257) gives: % 29.07/4.97 | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | Case 1: % 29.07/4.97 | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | (355) ~ (all_139_1 = 0) % 29.07/4.97 | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | REDUCE: (326), (355) imply: % 29.07/4.97 | | | | | | | | | | | | | | (356) $false % 29.07/4.97 | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | CLOSE: (356) is inconsistent. % 29.07/4.97 | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | Case 2: % 29.07/4.97 | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | (357) ~ (all_139_2 = 0) | all_139_0 = 0 % 29.07/4.97 | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | BETA: splitting (357) gives: % 29.07/4.97 | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | Case 1: % 29.07/4.97 | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | (358) ~ (all_139_2 = 0) % 29.07/4.97 | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | REDUCE: (348), (358) imply: % 29.07/4.97 | | | | | | | | | | | | | | | (359) $false % 29.07/4.97 | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | CLOSE: (359) is inconsistent. % 29.07/4.97 | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | Case 2: % 29.07/4.97 | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | (360) all_139_0 = 0 % 29.07/4.97 | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | REDUCE: (256), (360) imply: % 29.07/4.97 | | | | | | | | | | | | | | | (361) aNaturalNumber0(all_64_0) = 0 % 29.07/4.97 | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | BETA: splitting (88) gives: % 29.07/4.97 | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | Case 1: % 29.07/4.97 | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | (362) ~ (all_64_1 = 0) % 29.07/4.97 | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | REDUCE: (346), (362) imply: % 29.07/4.97 | | | | | | | | | | | | | | | | (363) $false % 29.07/4.97 | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | CLOSE: (363) is inconsistent. % 29.07/4.97 | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | Case 2: % 29.07/4.97 | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | (364) ~ (all_64_2 = 0) | all_64_0 = all_35_2 % 29.07/4.97 | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | BETA: splitting (364) gives: % 29.07/4.97 | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | Case 1: % 29.07/4.97 | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | (365) ~ (all_64_2 = 0) % 29.07/4.97 | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | REDUCE: (166), (365) imply: % 29.07/4.97 | | | | | | | | | | | | | | | | | (366) $false % 29.07/4.97 | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | CLOSE: (366) is inconsistent. % 29.07/4.97 | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | Case 2: % 29.07/4.97 | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | (367) all_64_0 = all_35_2 % 29.07/4.97 | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | REDUCE: (361), (367) imply: % 29.07/4.97 | | | | | | | | | | | | | | | | | (368) aNaturalNumber0(all_35_2) = 0 % 29.07/4.97 | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | BETA: splitting (109) gives: % 29.07/4.97 | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | Case 1: % 29.07/4.97 | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | (369) ~ (all_72_2 = 0) % 29.07/4.97 | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | REDUCE: (347), (369) imply: % 29.07/4.97 | | | | | | | | | | | | | | | | | | (370) $false % 29.07/4.97 | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | CLOSE: (370) is inconsistent. % 29.07/4.97 | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | Case 2: % 29.07/4.97 | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | (371) ~ (all_72_3 = 0) | ~ (all_72_4 = 0) | all_72_0 = % 29.07/4.97 | | | | | | | | | | | | | | | | | | all_37_2 % 29.07/4.97 | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | BETA: splitting (354) gives: % 29.07/4.97 | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | Case 1: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | (372) ~ (all_52_2 = 0) % 29.07/4.97 | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | REDUCE: (231), (372) imply: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | (373) $false % 29.07/4.97 | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | CLOSE: (373) is inconsistent. % 29.07/4.97 | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | Case 2: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | (374) all_52_0 = 0 % 29.07/4.97 | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | REDUCE: (61), (374) imply: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | (375) aNaturalNumber0(all_37_2) = 0 % 29.07/4.97 | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | BETA: splitting (371) gives: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | Case 1: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | (376) ~ (all_72_3 = 0) % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | REDUCE: (169), (376) imply: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | (377) $false % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | CLOSE: (377) is inconsistent. % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | Case 2: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | (378) ~ (all_72_4 = 0) | all_72_0 = all_37_2 % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | BETA: splitting (280) gives: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | Case 1: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | (379) ~ (all_151_2 = 0) % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | REDUCE: (349), (379) imply: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | (380) $false % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | CLOSE: (380) is inconsistent. % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | Case 2: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | (381) ~ (all_151_3 = 0) | ~ (all_151_4 = 0) | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | all_151_0 = all_37_2 % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | BETA: splitting (378) gives: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | Case 1: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | (382) ~ (all_72_4 = 0) % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (168), (382) imply: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | (383) $false % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | CLOSE: (383) is inconsistent. % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | Case 2: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | (384) all_72_0 = all_37_2 % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (171), (384) imply: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | (385) sdtasdt0(xl, all_35_2) = all_37_2 % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (232) gives: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | Case 1: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | (386) all_35_0 = all_35_2 % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (18), (386) imply: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | (387) $false % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (387) is inconsistent. % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | Case 2: % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | (388) ? [v0: any] : ? [v1: any] : ? [v2: $i] : ? % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | [v3: $i] : (sdtasdt0(all_35_0, xl) = v2 & % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(all_35_2, xl) = v3 & % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_0) = v0 & % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_2) = v1 & $i(v3) & $i(v2) % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | & ( ~ (v1 = 0) | ~ (v0 = 0) | ( ~ (v3 = v2) & % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | ~ (all_72_0 = all_37_2)))) % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (388) with fresh symbols all_255_0, % 29.07/4.97 | | | | | | | | | | | | | | | | | | | | | | | all_255_1, all_255_2, all_255_3 gives: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | (389) sdtasdt0(all_35_0, xl) = all_255_1 & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(all_35_2, xl) = all_255_0 & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_0) = all_255_3 & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_2) = all_255_2 & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | $i(all_255_0) & $i(all_255_1) & ( ~ (all_255_2 = % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | 0) | ~ (all_255_3 = 0) | ( ~ (all_255_0 = % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | all_255_1) & ~ (all_72_0 = all_37_2))) % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (389) implies: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | (390) aNaturalNumber0(all_35_2) = all_255_2 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | (391) aNaturalNumber0(all_35_0) = all_255_3 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | (392) ~ (all_255_2 = 0) | ~ (all_255_3 = 0) | ( ~ % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | (all_255_0 = all_255_1) & ~ (all_72_0 = % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | all_37_2)) % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (233) gives: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | (393) all_35_0 = all_35_2 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (18), (393) imply: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | (394) $false % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (394) is inconsistent. % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | (395) ? [v0: any] : ? [v1: any] : ? [v2: $i] : ? % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | [v3: $i] : (sdtasdt0(all_35_0, xl) = v3 & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(all_35_2, xl) = v2 & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_0) = v1 & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_2) = v0 & $i(v3) & $i(v2) % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | & ( ~ (v1 = 0) | ~ (v0 = 0) | ( ~ (v3 = v2) & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | ~ (all_72_0 = all_37_2)))) % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (395) with fresh symbols all_269_0, % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | all_269_1, all_269_2, all_269_3 gives: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | (396) sdtasdt0(all_35_0, xl) = all_269_0 & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(all_35_2, xl) = all_269_1 & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_0) = all_269_2 & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_2) = all_269_3 & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | $i(all_269_0) & $i(all_269_1) & ( ~ (all_269_2 = % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | 0) | ~ (all_269_3 = 0) | ( ~ (all_269_0 = % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | all_269_1) & ~ (all_72_0 = all_37_2))) % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (396) implies: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | (397) aNaturalNumber0(all_35_2) = all_269_3 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | (398) aNaturalNumber0(all_35_0) = all_269_2 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (381) gives: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | (399) ~ (all_151_3 = 0) % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (338), (399) imply: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | (400) $false % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (400) is inconsistent. % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | (401) ~ (all_151_4 = 0) | all_151_0 = all_37_2 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (401) gives: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | (402) ~ (all_151_4 = 0) % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (337), (402) imply: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | (403) $false % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (403) is inconsistent. % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | (404) all_151_0 = all_37_2 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (350), (404) imply: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | (405) sdtasdt0(xn, xm) = all_37_2 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (274), (404) imply: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | (406) $i(all_37_2) % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_255_2, all_269_3, % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | all_35_2, simplifying with (390), (397) gives: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | (407) all_269_3 = all_255_2 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_269_3, all_35_2, % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (368), (397) gives: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | (408) all_269_3 = 0 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_58_1, all_269_2, % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | all_35_0, simplifying with (71), (398) gives: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | (409) all_269_2 = all_58_1 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_255_3, all_269_2, % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | all_35_0, simplifying with (391), (398) gives: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | (410) all_269_2 = all_255_3 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with all_35_1, all_37_2, xm, % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | xn, simplifying with (19), (405) gives: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | (411) all_37_2 = all_35_1 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (409), (410) imply: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | (412) all_255_3 = all_58_1 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (407), (408) imply: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | (413) all_255_2 = 0 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (413) implies: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | (414) all_255_2 = 0 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (384), (411) imply: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | (415) all_72_0 = all_35_1 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (41), (411) imply: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | (416) sdtasdt0(xl, all_35_0) = all_35_1 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (385), (411) imply: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | (417) sdtasdt0(xl, all_35_2) = all_35_1 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (375), (411) imply: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | (418) aNaturalNumber0(all_35_1) = 0 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (392) gives: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | (419) ~ (all_255_2 = 0) % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (414), (419) imply: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | (420) $false % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (420) is inconsistent. % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | (421) ~ (all_255_3 = 0) | ( ~ (all_255_0 = all_255_1) & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | ~ (all_72_0 = all_37_2)) % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (421) gives: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (422) ~ (all_255_3 = 0) % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (412), (422) imply: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (423) ~ (all_58_1 = 0) % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (57) gives: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (424) xl = sz00 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (5), (424) imply: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (425) $false % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (425) is inconsistent. % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (426) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (doDivides0(xl, all_35_1) = v2 & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_1) = v1 & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | ~ (v1 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | = 0) | ~ (v0 = 0))) | ( ! [v0: any] : (v0 = % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_35_0 | ~ (sdtasdt0(xl, v0) = all_35_1) | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ~ (sdtasdt0(xl, all_35_0) = v0) | ~ % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | $i(all_35_0) | (v0 = all_35_1 & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_0) = 0))) % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (426) gives: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (427) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (doDivides0(xl, all_35_1) = v2 & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_1) = v1 & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | ~ (v1 % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | = 0) | ~ (v0 = 0))) % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (427) with fresh symbols all_306_0, % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_306_1, all_306_2 gives: % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (428) doDivides0(xl, all_35_1) = all_306_0 & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_1) = all_306_1 & % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = all_306_2 & ( ~ (all_306_0 = % 29.07/4.98 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 0) | ~ (all_306_1 = 0) | ~ (all_306_2 = 0)) % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (428) implies: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (429) aNaturalNumber0(xl) = all_306_2 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (430) aNaturalNumber0(all_35_1) = all_306_1 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (431) doDivides0(xl, all_35_1) = all_306_0 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (432) ~ (all_306_0 = 0) | ~ (all_306_1 = 0) | ~ % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (all_306_2 = 0) % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_306_2, xl, % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (3), (429) gives: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (433) all_306_2 = 0 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_306_1, all_35_1, % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (418), (430) gives: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (434) all_306_1 = 0 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (432) gives: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (435) ~ (all_306_0 = 0) % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mDivTrans) with xl, xm, all_35_1, % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_306_0, simplifying with (6), (9), (10), (38), % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (431) gives: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (436) all_306_0 = 0 | ? [v0: any] : ? [v1: any] : ? % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [v2: any] : ? [v3: any] : (doDivides0(xm, % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_35_1) = v3 & aNaturalNumber0(all_35_1) = % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | v2 & aNaturalNumber0(xm) = v1 & % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v3 = 0) | ~ (v2 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mDefDiv) with xl, all_35_1, % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_306_0, simplifying with (9), (38), (431) % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | gives: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (437) ? [v0: any] : ? [v1: any] : % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (aNaturalNumber0(all_35_1) = v1 & % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | = 0))) | (( ~ (all_306_0 = 0) | ? [v0: $i] % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | : (sdtasdt0(xl, v0) = all_35_1 & % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(v0) = 0 & $i(v0))) & % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (all_306_0 = 0 | ! [v0: $i] : ( ~ (sdtasdt0(xl, % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | v0) = all_35_1) | ~ $i(v0) | ? [v1: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | int] : ( ~ (v1 = 0) & aNaturalNumber0(v0) % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | = v1)))) % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (437) gives: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (438) ? [v0: any] : ? [v1: any] : % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (aNaturalNumber0(all_35_1) = v1 & % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | = 0))) % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (438) with fresh symbols all_326_0, % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_326_1 gives: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (439) aNaturalNumber0(all_35_1) = all_326_0 & % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = all_326_1 & ( ~ (all_326_0 = % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 0) | ~ (all_326_1 = 0)) % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (439) implies: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (440) aNaturalNumber0(xl) = all_326_1 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (441) aNaturalNumber0(all_35_1) = all_326_0 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (442) ~ (all_326_0 = 0) | ~ (all_326_1 = 0) % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (436) gives: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (443) all_306_0 = 0 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (435), (443) imply: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (444) $false % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (444) is inconsistent. % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (445) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [v3: any] : (doDivides0(xm, all_35_1) = v3 & % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_1) = v2 & % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xm) = v1 & aNaturalNumber0(xl) = % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | v0 & ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ~ (v0 = 0))) % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (445) with fresh symbols all_331_0, % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_331_1, all_331_2, all_331_3 gives: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (446) doDivides0(xm, all_35_1) = all_331_0 & % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_1) = all_331_1 & % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xm) = all_331_2 & % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = all_331_3 & ( ~ (all_331_0 = % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 0) | ~ (all_331_1 = 0) | ~ (all_331_2 = 0) | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ~ (all_331_3 = 0)) % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (446) implies: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (447) aNaturalNumber0(xl) = all_331_3 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (448) aNaturalNumber0(all_35_1) = all_331_1 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_331_3, xl, % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (3), (447) gives: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (449) all_331_3 = 0 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_326_1, all_331_3, xl, % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (440), (447) gives: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (450) all_331_3 = all_326_1 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_331_1, all_35_1, % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (418), (448) gives: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (451) all_331_1 = 0 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_326_0, all_331_1, % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_35_1, simplifying with (441), (448) gives: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (452) all_331_1 = all_326_0 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (451), (452) imply: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (453) all_326_0 = 0 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (449), (450) imply: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (454) all_326_1 = 0 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (454) implies: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (455) all_326_1 = 0 % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (442) gives: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (456) ~ (all_326_0 = 0) % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (453), (456) imply: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (457) $false % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (457) is inconsistent. % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (458) ~ (all_326_1 = 0) % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (455), (458) imply: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (459) $false % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (459) is inconsistent. % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (460) ( ~ (all_306_0 = 0) | ? [v0: $i] : (sdtasdt0(xl, % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | v0) = all_35_1 & aNaturalNumber0(v0) = 0 & % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | $i(v0))) & (all_306_0 = 0 | ! [v0: $i] : ( ~ % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (sdtasdt0(xl, v0) = all_35_1) | ~ $i(v0) | ? % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [v1: int] : ( ~ (v1 = 0) & aNaturalNumber0(v0) % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | = v1))) % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/4.99 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (460) implies: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (461) all_306_0 = 0 | ! [v0: $i] : ( ~ (sdtasdt0(xl, % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | v0) = all_35_1) | ~ $i(v0) | ? [v1: int] : % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ( ~ (v1 = 0) & aNaturalNumber0(v0) = v1)) % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (461) gives: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (462) all_306_0 = 0 % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (435), (462) imply: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (463) $false % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (463) is inconsistent. % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (464) ! [v0: $i] : ( ~ (sdtasdt0(xl, v0) = all_35_1) | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(v0) = v1)) % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (464) with all_35_2, simplifying % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | with (172), (417) gives: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (465) ? [v0: int] : ( ~ (v0 = 0) & % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_2) = v0) % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (465) with fresh symbol all_335_0 % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | gives: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (466) ~ (all_335_0 = 0) & aNaturalNumber0(all_35_2) = % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_335_0 % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (466) implies: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (467) ~ (all_335_0 = 0) % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (468) aNaturalNumber0(all_35_2) = all_335_0 % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_335_0, all_35_2, % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (368), (468) gives: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (469) all_335_0 = 0 % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (467), (469) imply: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (470) $false % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (470) is inconsistent. % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (471) ~ (all_306_1 = 0) | ~ (all_306_2 = 0) % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (471) gives: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (472) ~ (all_306_1 = 0) % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (434), (472) imply: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (473) $false % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (473) is inconsistent. % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (474) ~ (all_306_2 = 0) % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (433), (474) imply: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (475) $false % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (475) is inconsistent. % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (476) ! [v0: any] : (v0 = all_35_0 | ~ (sdtasdt0(xl, % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | v0) = all_35_1) | ~ $i(v0) | ? [v1: int] : % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ( ~ (v1 = 0) & aNaturalNumber0(v0) = v1)) & ! % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [v0: $i] : ( ~ (sdtasdt0(xl, all_35_0) = v0) | ~ % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | $i(all_35_0) | (v0 = all_35_1 & % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_0) = 0)) % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (476) implies: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (477) ! [v0: $i] : ( ~ (sdtasdt0(xl, all_35_0) = v0) | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ~ $i(all_35_0) | (v0 = all_35_1 & % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_0) = 0)) % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (477) with all_35_1, simplifying % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | with (42), (416) gives: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (478) aNaturalNumber0(all_35_0) = 0 % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_58_1, 0, all_35_0, % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (71), (478) gives: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (479) all_58_1 = 0 % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (423), (479) imply: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (480) $false % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (480) is inconsistent. % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (481) ~ (all_255_0 = all_255_1) & ~ (all_72_0 = % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_37_2) % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (481) implies: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (482) ~ (all_72_0 = all_37_2) % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (411), (415), (482) imply: % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (483) $false % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (483) is inconsistent. % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | End of split % 29.07/5.00 | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | Case 2: % 29.07/5.00 | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | (484) ? [v0: int] : ( ~ (v0 = 0) & % 29.07/5.00 | | | | | | | | | | | | aNaturalNumber0(all_102_0) = v0) % 29.07/5.00 | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | DELTA: instantiating (484) with fresh symbol all_167_0 % 29.07/5.00 | | | | | | | | | | | | gives: % 29.07/5.00 | | | | | | | | | | | | (485) ~ (all_167_0 = 0) & aNaturalNumber0(all_102_0) = % 29.07/5.00 | | | | | | | | | | | | all_167_0 % 29.07/5.00 | | | | | | | | | | | | % 29.07/5.00 | | | | | | | | | | | | ALPHA: (485) implies: % 29.07/5.01 | | | | | | | | | | | | (486) ~ (all_167_0 = 0) % 29.07/5.01 | | | | | | | | | | | | (487) aNaturalNumber0(all_102_0) = all_167_0 % 29.07/5.01 | | | | | | | | | | | | % 29.07/5.01 | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_167_0, all_102_0, % 29.07/5.01 | | | | | | | | | | | | simplifying with (211), (487) gives: % 29.07/5.01 | | | | | | | | | | | | (488) all_167_0 = 0 % 29.07/5.01 | | | | | | | | | | | | % 29.07/5.01 | | | | | | | | | | | | REDUCE: (486), (488) imply: % 29.07/5.01 | | | | | | | | | | | | (489) $false % 29.07/5.01 | | | | | | | | | | | | % 29.07/5.01 | | | | | | | | | | | | CLOSE: (489) is inconsistent. % 29.07/5.01 | | | | | | | | | | | | % 29.07/5.01 | | | | | | | | | | | End of split % 29.07/5.01 | | | | | | | | | | | % 29.07/5.01 | | | | | | | | | | End of split % 29.07/5.01 | | | | | | | | | | % 29.07/5.01 | | | | | | | | | End of split % 29.07/5.01 | | | | | | | | | % 29.07/5.01 | | | | | | | | End of split % 29.07/5.01 | | | | | | | | % 29.07/5.01 | | | | | | | End of split % 29.07/5.01 | | | | | | | % 29.07/5.01 | | | | | | End of split % 29.07/5.01 | | | | | | % 29.07/5.01 | | | | | End of split % 29.07/5.01 | | | | | % 29.07/5.01 | | | | End of split % 29.07/5.01 | | | | % 29.07/5.01 | | | End of split % 29.07/5.01 | | | % 29.07/5.01 | | End of split % 29.07/5.01 | | % 29.07/5.01 | End of split % 29.07/5.01 | % 29.07/5.01 End of proof % 29.07/5.01 % SZS output end Proof for theBenchmark % 29.07/5.01 % 29.07/5.01 4400ms %------------------------------------------------------------------------------