%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : NUM476+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 : n019.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:01 EDT 2023 % Result : Theorem 12.91s 2.62s % Output : Proof 22.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUM476+1 : TPTP v8.1.2. Released v4.0.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n019.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Aug 25 09:11:13 EDT 2023 % 0.12/0.34 % CPUTime : % 0.20/0.59 ________ _____ % 0.20/0.59 ___ __ \_________(_)________________________________ % 0.20/0.59 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.59 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.59 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.59 % 0.20/0.59 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.59 (2023-06-19) % 0.20/0.59 % 0.20/0.59 (c) Philipp Rümmer, 2009-2023 % 0.20/0.59 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.59 Amanda Stjerna. % 0.20/0.59 Free software under BSD-3-Clause. % 0.20/0.59 % 0.20/0.59 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.59 % 0.20/0.59 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.20/0.61 Running up to 7 provers in parallel. % 0.20/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.77/1.16 Prover 1: Preprocessing ... % 2.77/1.16 Prover 4: Preprocessing ... % 3.44/1.20 Prover 3: Preprocessing ... % 3.44/1.20 Prover 0: Preprocessing ... % 3.44/1.20 Prover 6: Preprocessing ... % 3.44/1.20 Prover 2: Preprocessing ... % 3.44/1.21 Prover 5: Preprocessing ... % 7.98/1.92 Prover 1: Constructing countermodel ... % 8.21/1.93 Prover 3: Constructing countermodel ... % 8.82/2.05 Prover 6: Proving ... % 8.82/2.07 Prover 5: Constructing countermodel ... % 9.23/2.15 Prover 2: Proving ... % 9.93/2.31 Prover 4: Constructing countermodel ... % 11.10/2.38 Prover 0: Proving ... % 12.91/2.62 Prover 3: proved (1996ms) % 12.91/2.62 % 12.91/2.62 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 12.91/2.62 % 12.91/2.63 Prover 5: stopped % 12.91/2.64 Prover 6: stopped % 12.91/2.64 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 12.91/2.64 Prover 0: stopped % 12.91/2.66 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 12.91/2.66 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 12.91/2.66 Prover 2: stopped % 12.91/2.66 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 12.91/2.66 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 13.70/2.74 Prover 11: Preprocessing ... % 13.70/2.74 Prover 7: Preprocessing ... % 13.70/2.75 Prover 8: Preprocessing ... % 13.95/2.77 Prover 10: Preprocessing ... % 13.95/2.78 Prover 13: Preprocessing ... % 13.95/2.88 Prover 8: Warning: ignoring some quantifiers % 13.95/2.89 Prover 8: Constructing countermodel ... % 13.95/2.95 Prover 10: Constructing countermodel ... % 13.95/2.97 Prover 13: Constructing countermodel ... % 13.95/2.98 Prover 7: Constructing countermodel ... % 15.92/3.14 Prover 11: Constructing countermodel ... % 20.82/3.81 Prover 1: Found proof (size 377) % 20.82/3.82 Prover 1: proved (3207ms) % 20.82/3.82 Prover 13: stopped % 20.82/3.82 Prover 7: stopped % 20.82/3.82 Prover 11: stopped % 20.82/3.82 Prover 8: stopped % 20.82/3.82 Prover 10: stopped % 20.82/3.82 Prover 4: stopped % 20.82/3.82 % 20.82/3.82 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 20.82/3.82 % 21.21/3.85 % SZS output start Proof for theBenchmark % 21.21/3.85 Assumptions after simplification: % 21.21/3.85 --------------------------------- % 21.21/3.85 % 21.21/3.85 (mAMDistr) % 21.31/3.88 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 21.31/3.88 $i] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ % 21.31/3.88 (sdtpldt0(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : % 21.31/3.88 ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? % 21.31/3.88 [v12: $i] : ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v9, v0) = v11 & % 21.31/3.88 sdtasdt0(v2, v0) = v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v9) = v10 & % 21.31/3.88 sdtpldt0(v12, v13) = v14 & sdtpldt0(v1, v2) = v9 & aNaturalNumber0(v2) = % 21.31/3.88 v8 & aNaturalNumber0(v1) = v7 & aNaturalNumber0(v0) = v6 & $i(v14) & % 21.31/3.88 $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) & ( ~ (v8 = 0) | ~ (v7 = % 21.31/3.88 0) | ~ (v6 = 0) | (v14 = v11 & v10 = v5)))) % 21.31/3.88 % 21.31/3.88 (mAddComm) % 21.31/3.88 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 21.31/3.88 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 21.31/3.88 (sdtpldt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 % 21.31/3.88 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 21.31/3.88 % 21.31/3.88 (mDefDiff) % 21.31/3.88 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtmndt0(v1, v0) = v2) | ~ % 21.31/3.88 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 21.31/3.88 (sdtlseqdt0(v0, v1) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = % 21.31/3.88 v3 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0))) | ( ! [v3: $i] : (v3 = v2 % 21.31/3.88 | ~ (sdtpldt0(v0, v3) = v1) | ~ $i(v3) | ? [v4: int] : ( ~ (v4 = 0) & % 21.31/3.88 aNaturalNumber0(v3) = v4)) & ! [v3: $i] : ( ~ (sdtpldt0(v0, v2) = v3) % 21.31/3.88 | ~ $i(v2) | (v3 = v1 & aNaturalNumber0(v2) = 0)))) % 21.31/3.88 % 21.31/3.88 (mDefDiv) % 21.31/3.89 ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (doDivides0(v0, v1) = v2) | ~ % 21.31/3.89 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : (aNaturalNumber0(v1) = v4 % 21.31/3.89 & aNaturalNumber0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0))) | (( ~ (v2 = 0) % 21.31/3.89 | ? [v3: $i] : (sdtasdt0(v0, v3) = v1 & aNaturalNumber0(v3) = 0 & % 21.31/3.89 $i(v3))) & (v2 = 0 | ! [v3: $i] : ( ~ (sdtasdt0(v0, v3) = v1) | ~ % 21.31/3.89 $i(v3) | ? [v4: int] : ( ~ (v4 = 0) & aNaturalNumber0(v3) = v4))))) % 21.31/3.89 % 21.31/3.89 (mDefQuot) % 21.31/3.89 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v0 = sz00 | ~ % 21.31/3.89 (sdtsldt0(v1, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: % 21.31/3.89 any] : ? [v5: any] : (doDivides0(v0, v1) = v5 & aNaturalNumber0(v1) = v4 % 21.31/3.89 & aNaturalNumber0(v0) = v3 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0))) | % 21.31/3.89 ( ! [v3: $i] : (v3 = v2 | ~ (sdtasdt0(v0, v3) = v1) | ~ $i(v3) | ? [v4: % 21.31/3.89 int] : ( ~ (v4 = 0) & aNaturalNumber0(v3) = v4)) & ! [v3: $i] : ( ~ % 21.31/3.89 (sdtasdt0(v0, v2) = v3) | ~ $i(v2) | (v3 = v1 & aNaturalNumber0(v2) = % 21.31/3.89 0)))) % 21.31/3.89 % 21.31/3.89 (mDivTrans) % 21.31/3.89 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 21.31/3.89 (doDivides0(v0, v2) = v3) | ~ (doDivides0(v0, v1) = 0) | ~ $i(v2) | ~ % 21.31/3.89 $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: % 21.31/3.89 any] : (doDivides0(v1, v2) = v7 & aNaturalNumber0(v2) = v6 & % 21.31/3.89 aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v7 = 0) | ~ % 21.31/3.89 (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) % 21.31/3.89 % 21.31/3.89 (mMulAsso) % 21.31/3.89 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 21.31/3.89 (sdtasdt0(v3, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) % 21.31/3.89 | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? % 21.31/3.89 [v9: $i] : (sdtasdt0(v1, v2) = v8 & sdtasdt0(v0, v8) = v9 & % 21.31/3.89 aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & aNaturalNumber0(v0) % 21.31/3.89 = v5 & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v9 = % 21.31/3.89 v4))) % 21.31/3.89 % 21.31/3.89 (mMulCanc) % 21.31/3.89 $i(sz00) & ! [v0: $i] : (v0 = sz00 | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) % 21.31/3.89 | ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v2 = v1 | ~ % 21.31/3.89 (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | ~ % 21.31/3.89 $i(v1) | ? [v5: any] : ? [v6: any] : ? [v7: $i] : ? [v8: $i] : % 21.31/3.89 (sdtasdt0(v2, v0) = v8 & sdtasdt0(v1, v0) = v7 & aNaturalNumber0(v2) = v6 % 21.31/3.89 & aNaturalNumber0(v1) = v5 & $i(v8) & $i(v7) & ( ~ (v6 = 0) | ~ (v5 = % 21.31/3.89 0) | ( ~ (v8 = v7) & ~ (v4 = v3)))))) % 21.31/3.89 % 21.31/3.89 (mMulComm) % 21.31/3.90 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 21.31/3.90 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 21.31/3.90 (sdtasdt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 % 21.31/3.90 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 21.31/3.90 % 21.31/3.90 (mSortsB) % 21.31/3.90 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 21.31/3.90 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 21.31/3.90 (aNaturalNumber0(v2) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = % 21.31/3.90 v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 21.31/3.90 % 21.31/3.90 (mSortsB_02) % 21.31/3.90 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 21.31/3.90 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 21.31/3.90 (aNaturalNumber0(v2) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = % 21.31/3.90 v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 21.31/3.90 % 21.31/3.90 (m_AddZero) % 21.31/3.90 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtpldt0(sz00, v0) = v1) | ~ % 21.31/3.90 $i(v0) | ? [v2: any] : ? [v3: $i] : (sdtpldt0(v0, sz00) = v3 & % 21.31/3.90 aNaturalNumber0(v0) = v2 & $i(v3) & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) % 21.31/3.90 % 21.31/3.90 (m_MulZero) % 21.31/3.90 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtasdt0(sz00, v0) = v1) | ~ % 21.31/3.90 $i(v0) | ? [v2: any] : ? [v3: $i] : (sdtasdt0(v0, sz00) = v3 & % 21.31/3.90 aNaturalNumber0(v0) = v2 & $i(v3) & ( ~ (v2 = 0) | (v3 = sz00 & v1 = % 21.31/3.90 sz00)))) % 21.31/3.90 % 21.31/3.90 (m__) % 21.31/3.90 $i(xn) & $i(xm) & $i(xl) & $i(sz00) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] % 21.31/3.90 : ? [v3: int] : ( ~ (v3 = 0) & sdtsldt0(v1, xl) = v2 & sdtsldt0(xm, xl) = v0 % 21.31/3.90 & doDivides0(xl, xn) = v3 & sdtpldt0(xm, xn) = v1 & $i(v2) & $i(v1) & $i(v0) % 21.31/3.90 & (xl = sz00 | ? [v4: $i] : ? [v5: $i] : (sdtasdt0(xl, v0) = v4 & % 21.31/3.90 sdtpldt0(v4, xn) = v5 & $i(v5) & $i(v4) & ? [v6: $i] : (sdtmndt0(v2, % 21.31/3.90 v0) = v6 & sdtlseqdt0(v0, v2) = 0 & sdtasdt0(xl, v6) = xn & % 21.31/3.90 $i(v6))))) % 21.31/3.90 % 21.31/3.90 (m__1324) % 21.31/3.90 aNaturalNumber0(xn) = 0 & aNaturalNumber0(xm) = 0 & aNaturalNumber0(xl) = 0 & % 21.31/3.90 $i(xn) & $i(xm) & $i(xl) % 21.31/3.90 % 21.31/3.90 (m__1324_04) % 21.31/3.90 $i(xn) & $i(xm) & $i(xl) & ? [v0: $i] : (doDivides0(xl, v0) = 0 & % 21.31/3.90 doDivides0(xl, xm) = 0 & sdtpldt0(xm, xn) = v0 & $i(v0)) % 21.31/3.90 % 21.31/3.90 (function-axioms) % 21.31/3.91 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 21.31/3.91 (sdtsldt0(v3, v2) = v1) | ~ (sdtsldt0(v3, v2) = v0)) & ! [v0: % 21.31/3.91 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 21.31/3.91 : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ (doDivides0(v3, v2) = v0)) & ! % 21.31/3.91 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 21.31/3.91 $i] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) & ! % 21.31/3.91 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 21.31/3.91 (sdtmndt0(v3, v2) = v1) | ~ (sdtmndt0(v3, v2) = v0)) & ! [v0: % 21.31/3.91 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 21.31/3.91 : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ (sdtlseqdt0(v3, v2) = v0)) & ! % 21.31/3.91 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 21.31/3.91 (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 21.31/3.91 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | % 21.31/3.91 ~ (sdtpldt0(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 21.31/3.91 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) % 21.31/3.91 | ~ (aNaturalNumber0(v2) = v0)) % 21.31/3.91 % 21.31/3.91 Further assumptions not needed in the proof: % 21.31/3.91 -------------------------------------------- % 21.31/3.91 mAddAsso, mAddCanc, mDefLE, mDivSum, mIH, mIH_03, mLEAsym, mLENTr, mLERefl, % 21.31/3.91 mLETotal, mLETran, mMonAdd, mMonMul, mMonMul2, mNatSort, mSortsC, mSortsC_01, % 21.31/3.91 mZeroAdd, mZeroMul, m_MulUnit % 21.31/3.91 % 21.31/3.91 Those formulas are unsatisfiable: % 21.31/3.91 --------------------------------- % 21.31/3.91 % 21.31/3.91 Begin of proof % 21.31/3.91 | % 21.31/3.91 | ALPHA: (m_AddZero) implies: % 21.31/3.91 | (1) ! [v0: $i] : ! [v1: $i] : ( ~ (sdtpldt0(sz00, v0) = v1) | ~ $i(v0) | % 21.31/3.91 | ? [v2: any] : ? [v3: $i] : (sdtpldt0(v0, sz00) = v3 & % 21.31/3.91 | aNaturalNumber0(v0) = v2 & $i(v3) & ( ~ (v2 = 0) | (v3 = v0 & v1 = % 21.31/3.91 | v0)))) % 21.31/3.91 | % 21.31/3.91 | ALPHA: (m_MulZero) implies: % 21.31/3.91 | (2) ! [v0: $i] : ! [v1: $i] : ( ~ (sdtasdt0(sz00, v0) = v1) | ~ $i(v0) | % 21.31/3.91 | ? [v2: any] : ? [v3: $i] : (sdtasdt0(v0, sz00) = v3 & % 21.31/3.91 | aNaturalNumber0(v0) = v2 & $i(v3) & ( ~ (v2 = 0) | (v3 = sz00 & v1 % 21.31/3.91 | = sz00)))) % 21.31/3.91 | % 21.31/3.91 | ALPHA: (mMulCanc) implies: % 21.31/3.91 | (3) ! [v0: $i] : (v0 = sz00 | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) | % 21.31/3.91 | ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v2 = v1 | ~ % 21.31/3.91 | (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | % 21.31/3.91 | ~ $i(v1) | ? [v5: any] : ? [v6: any] : ? [v7: $i] : ? [v8: $i] % 21.31/3.91 | : (sdtasdt0(v2, v0) = v8 & sdtasdt0(v1, v0) = v7 & % 21.31/3.91 | aNaturalNumber0(v2) = v6 & aNaturalNumber0(v1) = v5 & $i(v8) & % 21.31/3.91 | $i(v7) & ( ~ (v6 = 0) | ~ (v5 = 0) | ( ~ (v8 = v7) & ~ (v4 = % 21.31/3.91 | v3)))))) % 21.31/3.91 | % 21.31/3.91 | ALPHA: (mDefQuot) implies: % 21.31/3.91 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v0 = sz00 | ~ (sdtsldt0(v1, % 21.31/3.91 | v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : % 21.31/3.91 | ? [v5: any] : (doDivides0(v0, v1) = v5 & aNaturalNumber0(v1) = v4 & % 21.31/3.91 | aNaturalNumber0(v0) = v3 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = % 21.31/3.91 | 0))) | ( ! [v3: $i] : (v3 = v2 | ~ (sdtasdt0(v0, v3) = v1) | % 21.31/3.91 | ~ $i(v3) | ? [v4: int] : ( ~ (v4 = 0) & aNaturalNumber0(v3) = % 21.31/3.91 | v4)) & ! [v3: $i] : ( ~ (sdtasdt0(v0, v2) = v3) | ~ $i(v2) | % 21.31/3.91 | (v3 = v1 & aNaturalNumber0(v2) = 0)))) % 21.31/3.91 | % 21.31/3.91 | ALPHA: (m__1324) implies: % 21.31/3.92 | (5) aNaturalNumber0(xl) = 0 % 21.31/3.92 | (6) aNaturalNumber0(xm) = 0 % 21.31/3.92 | (7) aNaturalNumber0(xn) = 0 % 21.31/3.92 | % 21.31/3.92 | ALPHA: (m__1324_04) implies: % 21.31/3.92 | (8) ? [v0: $i] : (doDivides0(xl, v0) = 0 & doDivides0(xl, xm) = 0 & % 21.31/3.92 | sdtpldt0(xm, xn) = v0 & $i(v0)) % 21.31/3.92 | % 21.31/3.92 | ALPHA: (m__) implies: % 21.31/3.92 | (9) $i(xl) % 21.31/3.92 | (10) $i(xm) % 21.31/3.92 | (11) $i(xn) % 21.31/3.92 | (12) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: int] : ( ~ (v3 = 0) % 21.31/3.92 | & sdtsldt0(v1, xl) = v2 & sdtsldt0(xm, xl) = v0 & doDivides0(xl, xn) % 21.62/3.92 | = v3 & sdtpldt0(xm, xn) = v1 & $i(v2) & $i(v1) & $i(v0) & (xl = sz00 % 21.62/3.92 | | ? [v4: $i] : ? [v5: $i] : (sdtasdt0(xl, v0) = v4 & % 21.62/3.92 | sdtpldt0(v4, xn) = v5 & $i(v5) & $i(v4) & ? [v6: $i] : % 21.62/3.92 | (sdtmndt0(v2, v0) = v6 & sdtlseqdt0(v0, v2) = 0 & sdtasdt0(xl, % 21.62/3.92 | v6) = xn & $i(v6))))) % 21.62/3.92 | % 21.62/3.92 | ALPHA: (function-axioms) implies: % 21.62/3.92 | (13) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 21.62/3.92 | : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = % 21.62/3.92 | v0)) % 21.62/3.92 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 21.62/3.92 | (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 21.62/3.92 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 21.62/3.92 | (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 21.62/3.92 | (16) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 21.62/3.92 | : ! [v3: $i] : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ % 21.62/3.92 | (sdtlseqdt0(v3, v2) = v0)) % 21.62/3.92 | (17) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 21.62/3.92 | : ! [v3: $i] : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ % 21.62/3.92 | (doDivides0(v3, v2) = v0)) % 21.62/3.92 | % 21.62/3.92 | DELTA: instantiating (8) with fresh symbol all_33_0 gives: % 21.62/3.92 | (18) doDivides0(xl, all_33_0) = 0 & doDivides0(xl, xm) = 0 & sdtpldt0(xm, % 21.62/3.92 | xn) = all_33_0 & $i(all_33_0) % 21.62/3.92 | % 21.62/3.92 | ALPHA: (18) implies: % 21.62/3.92 | (19) sdtpldt0(xm, xn) = all_33_0 % 21.62/3.92 | (20) doDivides0(xl, xm) = 0 % 21.62/3.92 | (21) doDivides0(xl, all_33_0) = 0 % 21.62/3.92 | % 21.62/3.92 | DELTA: instantiating (12) with fresh symbols all_35_0, all_35_1, all_35_2, % 21.62/3.92 | all_35_3 gives: % 21.62/3.93 | (22) ~ (all_35_0 = 0) & sdtsldt0(all_35_2, xl) = all_35_1 & sdtsldt0(xm, % 21.62/3.93 | xl) = all_35_3 & doDivides0(xl, xn) = all_35_0 & sdtpldt0(xm, xn) = % 21.62/3.93 | all_35_2 & $i(all_35_1) & $i(all_35_2) & $i(all_35_3) & (xl = sz00 | % 21.62/3.93 | ? [v0: $i] : ? [v1: $i] : (sdtasdt0(xl, all_35_3) = v0 & % 21.62/3.93 | sdtpldt0(v0, xn) = v1 & $i(v1) & $i(v0) & ? [v2: $i] : % 21.62/3.93 | (sdtmndt0(all_35_1, all_35_3) = v2 & sdtlseqdt0(all_35_3, % 21.62/3.93 | all_35_1) = 0 & sdtasdt0(xl, v2) = xn & $i(v2)))) % 21.62/3.93 | % 21.62/3.93 | ALPHA: (22) implies: % 21.62/3.93 | (23) ~ (all_35_0 = 0) % 21.62/3.93 | (24) $i(all_35_2) % 21.62/3.93 | (25) sdtpldt0(xm, xn) = all_35_2 % 21.62/3.93 | (26) doDivides0(xl, xn) = all_35_0 % 21.62/3.93 | (27) sdtsldt0(xm, xl) = all_35_3 % 21.62/3.93 | (28) sdtsldt0(all_35_2, xl) = all_35_1 % 21.62/3.93 | (29) xl = sz00 | ? [v0: $i] : ? [v1: $i] : (sdtasdt0(xl, all_35_3) = v0 & % 21.62/3.93 | sdtpldt0(v0, xn) = v1 & $i(v1) & $i(v0) & ? [v2: $i] : % 21.62/3.93 | (sdtmndt0(all_35_1, all_35_3) = v2 & sdtlseqdt0(all_35_3, all_35_1) % 21.62/3.93 | = 0 & sdtasdt0(xl, v2) = xn & $i(v2))) % 21.62/3.93 | % 21.62/3.93 | GROUND_INST: instantiating (14) with all_33_0, all_35_2, xn, xm, simplifying % 21.62/3.93 | with (19), (25) gives: % 21.62/3.93 | (30) all_35_2 = all_33_0 % 21.62/3.93 | % 21.62/3.93 | REDUCE: (28), (30) imply: % 21.62/3.93 | (31) sdtsldt0(all_33_0, xl) = all_35_1 % 21.62/3.93 | % 21.62/3.93 | REDUCE: (24), (30) imply: % 21.62/3.93 | (32) $i(all_33_0) % 21.62/3.93 | % 21.62/3.93 | GROUND_INST: instantiating (3) with xm, simplifying with (6), (10) gives: % 21.62/3.93 | (33) xm = sz00 | ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 21.62/3.93 | (v1 = v0 | ~ (sdtasdt0(xm, v1) = v3) | ~ (sdtasdt0(xm, v0) = v2) | % 21.62/3.93 | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: $i] : % 21.62/3.93 | ? [v7: $i] : (sdtasdt0(v1, xm) = v7 & sdtasdt0(v0, xm) = v6 & % 21.62/3.93 | aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & $i(v7) & % 21.62/3.93 | $i(v6) & ( ~ (v5 = 0) | ~ (v4 = 0) | ( ~ (v7 = v6) & ~ (v3 = % 21.62/3.93 | v2))))) % 21.62/3.93 | % 21.62/3.93 | GROUND_INST: instantiating (3) with xn, simplifying with (7), (11) gives: % 21.62/3.93 | (34) xn = sz00 | ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 21.62/3.93 | (v1 = v0 | ~ (sdtasdt0(xn, v1) = v3) | ~ (sdtasdt0(xn, v0) = v2) | % 21.62/3.93 | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: $i] : % 21.62/3.93 | ? [v7: $i] : (sdtasdt0(v1, xn) = v7 & sdtasdt0(v0, xn) = v6 & % 21.62/3.93 | aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & $i(v7) & % 21.62/3.93 | $i(v6) & ( ~ (v5 = 0) | ~ (v4 = 0) | ( ~ (v7 = v6) & ~ (v3 = % 21.62/3.93 | v2))))) % 21.62/3.93 | % 21.62/3.93 | GROUND_INST: instantiating (mAddComm) with xm, xn, all_33_0, simplifying with % 21.62/3.93 | (10), (11), (19) gives: % 21.62/3.93 | (35) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xn, xm) = v2 & % 21.62/3.93 | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xm) = v0 & $i(v2) & ( ~ % 21.62/3.93 | (v1 = 0) | ~ (v0 = 0) | v2 = all_33_0)) % 21.62/3.93 | % 21.62/3.93 | GROUND_INST: instantiating (mSortsB) with xm, xn, all_33_0, simplifying with % 21.62/3.93 | (10), (11), (19) gives: % 21.62/3.94 | (36) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 21.62/3.94 | (aNaturalNumber0(all_33_0) = v2 & aNaturalNumber0(xn) = v1 & % 21.62/3.94 | aNaturalNumber0(xm) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 21.62/3.94 | % 21.62/3.94 | GROUND_INST: instantiating (mDefDiv) with xl, xm, 0, simplifying with (9), % 21.62/3.94 | (10), (20) gives: % 21.62/3.94 | (37) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(xm) = v1 & % 21.62/3.94 | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) | ? [v0: % 21.62/3.94 | $i] : (sdtasdt0(xl, v0) = xm & aNaturalNumber0(v0) = 0 & $i(v0)) % 21.62/3.94 | % 21.62/3.94 | GROUND_INST: instantiating (mDivTrans) with xl, xm, xn, all_35_0, simplifying % 21.62/3.94 | with (9), (10), (11), (20), (26) gives: % 21.62/3.94 | (38) all_35_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: % 21.62/3.94 | any] : (doDivides0(xm, xn) = v3 & aNaturalNumber0(xn) = v2 & % 21.62/3.94 | aNaturalNumber0(xm) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v3 = 0) | % 21.62/3.94 | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 21.62/3.94 | % 21.62/3.94 | GROUND_INST: instantiating (mDefDiv) with xl, xn, all_35_0, simplifying with % 21.62/3.94 | (9), (11), (26) gives: % 21.62/3.94 | (39) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(xn) = v1 & % 21.62/3.94 | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) | (( ~ % 21.62/3.94 | (all_35_0 = 0) | ? [v0: $i] : (sdtasdt0(xl, v0) = xn & % 21.62/3.94 | aNaturalNumber0(v0) = 0 & $i(v0))) & (all_35_0 = 0 | ! [v0: $i] % 21.62/3.94 | : ( ~ (sdtasdt0(xl, v0) = xn) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 % 21.62/3.94 | = 0) & aNaturalNumber0(v0) = v1)))) % 21.62/3.94 | % 21.62/3.94 | GROUND_INST: instantiating (mDivTrans) with xl, all_33_0, xn, all_35_0, % 21.62/3.94 | simplifying with (9), (11), (21), (26), (32) gives: % 21.62/3.94 | (40) all_35_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: % 21.62/3.94 | any] : (doDivides0(all_33_0, xn) = v3 & aNaturalNumber0(all_33_0) = % 21.62/3.94 | v1 & aNaturalNumber0(xn) = v2 & aNaturalNumber0(xl) = v0 & ( ~ (v3 = % 21.62/3.94 | 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 21.62/3.94 | % 21.62/3.94 | GROUND_INST: instantiating (mDefDiv) with xl, all_33_0, 0, simplifying with % 21.62/3.94 | (9), (21), (32) gives: % 21.62/3.94 | (41) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(all_33_0) = v1 & % 21.62/3.94 | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) | ? [v0: % 21.62/3.94 | $i] : (sdtasdt0(xl, v0) = all_33_0 & aNaturalNumber0(v0) = 0 & % 21.62/3.94 | $i(v0)) % 21.62/3.94 | % 21.62/3.94 | GROUND_INST: instantiating (4) with xl, xm, all_35_3, simplifying with (9), % 21.62/3.94 | (10), (27) gives: % 21.62/3.94 | (42) xl = sz00 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 21.62/3.94 | (doDivides0(xl, xm) = v2 & aNaturalNumber0(xm) = v1 & % 21.62/3.94 | aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = % 21.62/3.94 | 0))) | ( ! [v0: any] : (v0 = all_35_3 | ~ (sdtasdt0(xl, v0) = % 21.62/3.94 | xm) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 21.62/3.94 | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( ~ (sdtasdt0(xl, % 21.62/3.94 | all_35_3) = v0) | ~ $i(all_35_3) | (v0 = xm & % 21.62/3.94 | aNaturalNumber0(all_35_3) = 0))) % 21.62/3.94 | % 21.62/3.94 | GROUND_INST: instantiating (4) with xl, all_33_0, all_35_1, simplifying with % 21.62/3.94 | (9), (31), (32) gives: % 21.62/3.94 | (43) xl = sz00 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 21.62/3.94 | (doDivides0(xl, all_33_0) = v2 & aNaturalNumber0(all_33_0) = v1 & % 21.62/3.94 | aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = % 21.62/3.94 | 0))) | ( ! [v0: any] : (v0 = all_35_1 | ~ (sdtasdt0(xl, v0) = % 21.62/3.94 | all_33_0) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 21.62/3.94 | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( ~ (sdtasdt0(xl, % 21.62/3.94 | all_35_1) = v0) | ~ $i(all_35_1) | (v0 = all_33_0 & % 21.62/3.94 | aNaturalNumber0(all_35_1) = 0))) % 21.62/3.94 | % 21.62/3.94 | DELTA: instantiating (36) with fresh symbols all_46_0, all_46_1, all_46_2 % 21.62/3.94 | gives: % 21.62/3.94 | (44) aNaturalNumber0(all_33_0) = all_46_0 & aNaturalNumber0(xn) = all_46_1 % 21.62/3.94 | & aNaturalNumber0(xm) = all_46_2 & ( ~ (all_46_1 = 0) | ~ (all_46_2 = % 21.62/3.94 | 0) | all_46_0 = 0) % 21.62/3.94 | % 21.62/3.94 | ALPHA: (44) implies: % 21.62/3.95 | (45) aNaturalNumber0(xm) = all_46_2 % 21.62/3.95 | (46) aNaturalNumber0(xn) = all_46_1 % 21.62/3.95 | (47) aNaturalNumber0(all_33_0) = all_46_0 % 21.62/3.95 | (48) ~ (all_46_1 = 0) | ~ (all_46_2 = 0) | all_46_0 = 0 % 21.62/3.95 | % 21.62/3.95 | DELTA: instantiating (35) with fresh symbols all_48_0, all_48_1, all_48_2 % 21.62/3.95 | gives: % 21.62/3.95 | (49) sdtpldt0(xn, xm) = all_48_0 & aNaturalNumber0(xn) = all_48_1 & % 21.62/3.95 | aNaturalNumber0(xm) = all_48_2 & $i(all_48_0) & ( ~ (all_48_1 = 0) | % 21.62/3.95 | ~ (all_48_2 = 0) | all_48_0 = all_33_0) % 21.62/3.95 | % 21.62/3.95 | ALPHA: (49) implies: % 21.62/3.95 | (50) aNaturalNumber0(xm) = all_48_2 % 21.62/3.95 | (51) aNaturalNumber0(xn) = all_48_1 % 21.62/3.95 | (52) sdtpldt0(xn, xm) = all_48_0 % 21.62/3.95 | (53) ~ (all_48_1 = 0) | ~ (all_48_2 = 0) | all_48_0 = all_33_0 % 21.62/3.95 | % 21.62/3.95 | BETA: splitting (38) gives: % 21.62/3.95 | % 21.62/3.95 | Case 1: % 21.62/3.95 | | % 21.62/3.95 | | (54) all_35_0 = 0 % 21.62/3.95 | | % 21.62/3.95 | | REDUCE: (23), (54) imply: % 21.62/3.95 | | (55) $false % 21.62/3.95 | | % 21.62/3.95 | | CLOSE: (55) is inconsistent. % 21.62/3.95 | | % 21.62/3.95 | Case 2: % 21.62/3.95 | | % 21.62/3.95 | | (56) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 21.62/3.95 | | (doDivides0(xm, xn) = v3 & aNaturalNumber0(xn) = v2 & % 21.62/3.95 | | aNaturalNumber0(xm) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v3 = 0) % 21.62/3.95 | | | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 21.62/3.95 | | % 21.62/3.95 | | DELTA: instantiating (56) with fresh symbols all_58_0, all_58_1, all_58_2, % 21.62/3.95 | | all_58_3 gives: % 21.62/3.95 | | (57) doDivides0(xm, xn) = all_58_0 & aNaturalNumber0(xn) = all_58_1 & % 21.62/3.95 | | aNaturalNumber0(xm) = all_58_2 & aNaturalNumber0(xl) = all_58_3 & ( % 21.62/3.95 | | ~ (all_58_0 = 0) | ~ (all_58_1 = 0) | ~ (all_58_2 = 0) | ~ % 21.62/3.95 | | (all_58_3 = 0)) % 21.62/3.95 | | % 21.62/3.95 | | ALPHA: (57) implies: % 21.62/3.95 | | (58) aNaturalNumber0(xl) = all_58_3 % 21.62/3.95 | | (59) aNaturalNumber0(xm) = all_58_2 % 21.62/3.95 | | (60) aNaturalNumber0(xn) = all_58_1 % 21.62/3.95 | | (61) doDivides0(xm, xn) = all_58_0 % 21.62/3.95 | | (62) ~ (all_58_0 = 0) | ~ (all_58_1 = 0) | ~ (all_58_2 = 0) | ~ % 21.62/3.95 | | (all_58_3 = 0) % 21.62/3.95 | | % 21.62/3.95 | | BETA: splitting (40) gives: % 21.62/3.95 | | % 21.62/3.95 | | Case 1: % 21.62/3.95 | | | % 21.62/3.95 | | | (63) all_35_0 = 0 % 21.62/3.95 | | | % 21.62/3.95 | | | REDUCE: (23), (63) imply: % 21.62/3.95 | | | (64) $false % 21.62/3.95 | | | % 21.62/3.95 | | | CLOSE: (64) is inconsistent. % 21.62/3.95 | | | % 21.62/3.95 | | Case 2: % 21.62/3.95 | | | % 21.62/3.95 | | | (65) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 21.62/3.95 | | | (doDivides0(all_33_0, xn) = v3 & aNaturalNumber0(all_33_0) = v1 & % 21.62/3.95 | | | aNaturalNumber0(xn) = v2 & aNaturalNumber0(xl) = v0 & ( ~ (v3 = % 21.62/3.95 | | | 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 21.62/3.95 | | | % 21.62/3.95 | | | DELTA: instantiating (65) with fresh symbols all_63_0, all_63_1, all_63_2, % 21.62/3.95 | | | all_63_3 gives: % 21.62/3.95 | | | (66) doDivides0(all_33_0, xn) = all_63_0 & aNaturalNumber0(all_33_0) = % 21.62/3.95 | | | all_63_2 & aNaturalNumber0(xn) = all_63_1 & aNaturalNumber0(xl) = % 21.62/3.95 | | | all_63_3 & ( ~ (all_63_0 = 0) | ~ (all_63_1 = 0) | ~ (all_63_2 = % 21.62/3.95 | | | 0) | ~ (all_63_3 = 0)) % 21.62/3.95 | | | % 21.62/3.95 | | | ALPHA: (66) implies: % 21.62/3.95 | | | (67) aNaturalNumber0(xl) = all_63_3 % 21.62/3.95 | | | (68) aNaturalNumber0(xn) = all_63_1 % 21.62/3.95 | | | (69) aNaturalNumber0(all_33_0) = all_63_2 % 21.62/3.95 | | | % 21.62/3.95 | | | GROUND_INST: instantiating (13) with 0, all_63_3, xl, simplifying with % 21.62/3.95 | | | (5), (67) gives: % 21.62/3.95 | | | (70) all_63_3 = 0 % 21.62/3.95 | | | % 21.62/3.95 | | | GROUND_INST: instantiating (13) with all_58_3, all_63_3, xl, simplifying % 21.62/3.95 | | | with (58), (67) gives: % 21.62/3.95 | | | (71) all_63_3 = all_58_3 % 21.62/3.95 | | | % 21.62/3.95 | | | GROUND_INST: instantiating (13) with all_46_2, all_48_2, xm, simplifying % 21.62/3.95 | | | with (45), (50) gives: % 21.62/3.95 | | | (72) all_48_2 = all_46_2 % 21.62/3.95 | | | % 21.62/3.95 | | | GROUND_INST: instantiating (13) with 0, all_58_2, xm, simplifying with % 21.62/3.95 | | | (6), (59) gives: % 21.62/3.95 | | | (73) all_58_2 = 0 % 21.62/3.95 | | | % 21.62/3.95 | | | GROUND_INST: instantiating (13) with all_48_2, all_58_2, xm, simplifying % 21.62/3.95 | | | with (50), (59) gives: % 21.62/3.95 | | | (74) all_58_2 = all_48_2 % 21.62/3.95 | | | % 21.62/3.95 | | | GROUND_INST: instantiating (13) with 0, all_48_1, xn, simplifying with % 21.62/3.95 | | | (7), (51) gives: % 21.62/3.95 | | | (75) all_48_1 = 0 % 21.62/3.95 | | | % 21.62/3.95 | | | GROUND_INST: instantiating (13) with all_48_1, all_58_1, xn, simplifying % 21.62/3.95 | | | with (51), (60) gives: % 21.62/3.95 | | | (76) all_58_1 = all_48_1 % 21.62/3.95 | | | % 21.62/3.95 | | | GROUND_INST: instantiating (13) with all_58_1, all_63_1, xn, simplifying % 21.62/3.95 | | | with (60), (68) gives: % 21.62/3.95 | | | (77) all_63_1 = all_58_1 % 21.62/3.95 | | | % 21.62/3.95 | | | GROUND_INST: instantiating (13) with all_46_1, all_63_1, xn, simplifying % 21.62/3.95 | | | with (46), (68) gives: % 21.62/3.96 | | | (78) all_63_1 = all_46_1 % 21.62/3.96 | | | % 21.62/3.96 | | | GROUND_INST: instantiating (13) with all_46_0, all_63_2, all_33_0, % 21.62/3.96 | | | simplifying with (47), (69) gives: % 21.62/3.96 | | | (79) all_63_2 = all_46_0 % 21.62/3.96 | | | % 21.62/3.96 | | | COMBINE_EQS: (77), (78) imply: % 21.62/3.96 | | | (80) all_58_1 = all_46_1 % 21.62/3.96 | | | % 21.62/3.96 | | | SIMP: (80) implies: % 21.62/3.96 | | | (81) all_58_1 = all_46_1 % 21.62/3.96 | | | % 21.62/3.96 | | | COMBINE_EQS: (70), (71) imply: % 21.62/3.96 | | | (82) all_58_3 = 0 % 21.62/3.96 | | | % 21.62/3.96 | | | COMBINE_EQS: (76), (81) imply: % 21.62/3.96 | | | (83) all_48_1 = all_46_1 % 21.62/3.96 | | | % 21.62/3.96 | | | SIMP: (83) implies: % 21.62/3.96 | | | (84) all_48_1 = all_46_1 % 21.62/3.96 | | | % 21.62/3.96 | | | COMBINE_EQS: (73), (74) imply: % 21.62/3.96 | | | (85) all_48_2 = 0 % 21.62/3.96 | | | % 21.62/3.96 | | | SIMP: (85) implies: % 21.62/3.96 | | | (86) all_48_2 = 0 % 21.62/3.96 | | | % 21.62/3.96 | | | COMBINE_EQS: (75), (84) imply: % 21.62/3.96 | | | (87) all_46_1 = 0 % 21.62/3.96 | | | % 21.62/3.96 | | | SIMP: (87) implies: % 21.62/3.96 | | | (88) all_46_1 = 0 % 21.62/3.96 | | | % 21.62/3.96 | | | COMBINE_EQS: (72), (86) imply: % 21.62/3.96 | | | (89) all_46_2 = 0 % 21.62/3.96 | | | % 21.62/3.96 | | | SIMP: (89) implies: % 21.62/3.96 | | | (90) all_46_2 = 0 % 21.62/3.96 | | | % 21.62/3.96 | | | COMBINE_EQS: (81), (88) imply: % 21.62/3.96 | | | (91) all_58_1 = 0 % 21.62/3.96 | | | % 21.62/3.96 | | | BETA: splitting (62) gives: % 21.62/3.96 | | | % 21.62/3.96 | | | Case 1: % 21.62/3.96 | | | | % 21.62/3.96 | | | | (92) ~ (all_58_0 = 0) % 21.62/3.96 | | | | % 21.62/3.96 | | | | BETA: splitting (48) gives: % 21.62/3.96 | | | | % 21.62/3.96 | | | | Case 1: % 21.62/3.96 | | | | | % 21.62/3.96 | | | | | (93) ~ (all_46_1 = 0) % 21.62/3.96 | | | | | % 21.62/3.96 | | | | | REDUCE: (88), (93) imply: % 21.62/3.96 | | | | | (94) $false % 21.62/3.96 | | | | | % 21.62/3.96 | | | | | CLOSE: (94) is inconsistent. % 21.62/3.96 | | | | | % 21.62/3.96 | | | | Case 2: % 21.62/3.96 | | | | | % 21.62/3.96 | | | | | (95) ~ (all_46_2 = 0) | all_46_0 = 0 % 21.62/3.96 | | | | | % 21.62/3.96 | | | | | BETA: splitting (37) gives: % 21.62/3.96 | | | | | % 21.62/3.96 | | | | | Case 1: % 21.62/3.96 | | | | | | % 21.62/3.96 | | | | | | (96) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(xm) = v1 & % 21.62/3.96 | | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 21.62/3.96 | | | | | | % 21.62/3.96 | | | | | | DELTA: instantiating (96) with fresh symbols all_79_0, all_79_1 % 21.62/3.96 | | | | | | gives: % 21.62/3.96 | | | | | | (97) aNaturalNumber0(xm) = all_79_0 & aNaturalNumber0(xl) = % 21.62/3.96 | | | | | | all_79_1 & ( ~ (all_79_0 = 0) | ~ (all_79_1 = 0)) % 21.62/3.96 | | | | | | % 21.62/3.96 | | | | | | ALPHA: (97) implies: % 21.62/3.96 | | | | | | (98) aNaturalNumber0(xl) = all_79_1 % 21.62/3.96 | | | | | | (99) aNaturalNumber0(xm) = all_79_0 % 21.62/3.96 | | | | | | (100) ~ (all_79_0 = 0) | ~ (all_79_1 = 0) % 21.62/3.96 | | | | | | % 21.62/3.96 | | | | | | GROUND_INST: instantiating (13) with 0, all_79_1, xl, simplifying % 21.62/3.96 | | | | | | with (5), (98) gives: % 21.62/3.96 | | | | | | (101) all_79_1 = 0 % 21.62/3.96 | | | | | | % 21.62/3.96 | | | | | | GROUND_INST: instantiating (13) with 0, all_79_0, xm, simplifying % 21.62/3.96 | | | | | | with (6), (99) gives: % 21.62/3.96 | | | | | | (102) all_79_0 = 0 % 21.62/3.96 | | | | | | % 21.62/3.96 | | | | | | BETA: splitting (100) gives: % 21.62/3.96 | | | | | | % 21.62/3.96 | | | | | | Case 1: % 21.62/3.96 | | | | | | | % 21.62/3.96 | | | | | | | (103) ~ (all_79_0 = 0) % 21.62/3.96 | | | | | | | % 21.62/3.96 | | | | | | | REDUCE: (102), (103) imply: % 21.62/3.96 | | | | | | | (104) $false % 21.62/3.96 | | | | | | | % 21.62/3.96 | | | | | | | CLOSE: (104) is inconsistent. % 21.62/3.96 | | | | | | | % 21.62/3.96 | | | | | | Case 2: % 21.62/3.96 | | | | | | | % 21.62/3.96 | | | | | | | (105) ~ (all_79_1 = 0) % 21.62/3.96 | | | | | | | % 21.62/3.96 | | | | | | | REDUCE: (101), (105) imply: % 21.83/3.96 | | | | | | | (106) $false % 21.83/3.96 | | | | | | | % 21.83/3.96 | | | | | | | CLOSE: (106) is inconsistent. % 21.83/3.96 | | | | | | | % 21.83/3.96 | | | | | | End of split % 21.83/3.96 | | | | | | % 21.83/3.96 | | | | | Case 2: % 21.83/3.96 | | | | | | % 21.83/3.96 | | | | | | (107) ? [v0: $i] : (sdtasdt0(xl, v0) = xm & aNaturalNumber0(v0) % 21.83/3.96 | | | | | | = 0 & $i(v0)) % 21.83/3.96 | | | | | | % 21.83/3.96 | | | | | | DELTA: instantiating (107) with fresh symbol all_79_0 gives: % 21.83/3.96 | | | | | | (108) sdtasdt0(xl, all_79_0) = xm & aNaturalNumber0(all_79_0) = 0 % 21.83/3.96 | | | | | | & $i(all_79_0) % 21.83/3.96 | | | | | | % 21.83/3.96 | | | | | | ALPHA: (108) implies: % 21.83/3.96 | | | | | | (109) $i(all_79_0) % 21.83/3.96 | | | | | | (110) aNaturalNumber0(all_79_0) = 0 % 21.83/3.96 | | | | | | (111) sdtasdt0(xl, all_79_0) = xm % 21.83/3.96 | | | | | | % 21.83/3.96 | | | | | | BETA: splitting (53) gives: % 21.83/3.96 | | | | | | % 21.83/3.96 | | | | | | Case 1: % 21.83/3.96 | | | | | | | % 21.83/3.96 | | | | | | | (112) ~ (all_48_1 = 0) % 21.83/3.96 | | | | | | | % 21.83/3.96 | | | | | | | REDUCE: (75), (112) imply: % 21.83/3.96 | | | | | | | (113) $false % 21.83/3.96 | | | | | | | % 21.83/3.96 | | | | | | | CLOSE: (113) is inconsistent. % 21.83/3.96 | | | | | | | % 21.83/3.96 | | | | | | Case 2: % 21.83/3.96 | | | | | | | % 21.83/3.96 | | | | | | | (114) ~ (all_48_2 = 0) | all_48_0 = all_33_0 % 21.83/3.96 | | | | | | | % 21.83/3.96 | | | | | | | BETA: splitting (39) gives: % 21.83/3.96 | | | | | | | % 21.83/3.96 | | | | | | | Case 1: % 21.83/3.96 | | | | | | | | % 21.83/3.96 | | | | | | | | (115) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(xn) = v1 % 21.83/3.96 | | | | | | | | & aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = % 21.83/3.96 | | | | | | | | 0))) % 21.83/3.96 | | | | | | | | % 21.83/3.96 | | | | | | | | DELTA: instantiating (115) with fresh symbols all_87_0, all_87_1 % 21.83/3.96 | | | | | | | | gives: % 21.83/3.96 | | | | | | | | (116) aNaturalNumber0(xn) = all_87_0 & aNaturalNumber0(xl) = % 21.83/3.96 | | | | | | | | all_87_1 & ( ~ (all_87_0 = 0) | ~ (all_87_1 = 0)) % 21.83/3.96 | | | | | | | | % 21.83/3.96 | | | | | | | | ALPHA: (116) implies: % 21.83/3.96 | | | | | | | | (117) aNaturalNumber0(xl) = all_87_1 % 21.83/3.96 | | | | | | | | (118) aNaturalNumber0(xn) = all_87_0 % 21.83/3.96 | | | | | | | | (119) ~ (all_87_0 = 0) | ~ (all_87_1 = 0) % 21.83/3.96 | | | | | | | | % 21.83/3.96 | | | | | | | | GROUND_INST: instantiating (13) with 0, all_87_1, xl, % 21.83/3.96 | | | | | | | | simplifying with (5), (117) gives: % 21.83/3.96 | | | | | | | | (120) all_87_1 = 0 % 21.83/3.96 | | | | | | | | % 21.83/3.96 | | | | | | | | GROUND_INST: instantiating (13) with 0, all_87_0, xn, % 21.83/3.96 | | | | | | | | simplifying with (7), (118) gives: % 21.83/3.96 | | | | | | | | (121) all_87_0 = 0 % 21.83/3.96 | | | | | | | | % 21.83/3.96 | | | | | | | | BETA: splitting (119) gives: % 21.83/3.96 | | | | | | | | % 21.83/3.96 | | | | | | | | Case 1: % 21.83/3.96 | | | | | | | | | % 21.83/3.96 | | | | | | | | | (122) ~ (all_87_0 = 0) % 21.83/3.96 | | | | | | | | | % 21.83/3.96 | | | | | | | | | REDUCE: (121), (122) imply: % 21.83/3.96 | | | | | | | | | (123) $false % 21.83/3.96 | | | | | | | | | % 21.83/3.96 | | | | | | | | | CLOSE: (123) is inconsistent. % 21.83/3.96 | | | | | | | | | % 21.83/3.96 | | | | | | | | Case 2: % 21.83/3.96 | | | | | | | | | % 21.83/3.96 | | | | | | | | | (124) ~ (all_87_1 = 0) % 21.83/3.96 | | | | | | | | | % 21.83/3.96 | | | | | | | | | REDUCE: (120), (124) imply: % 21.83/3.96 | | | | | | | | | (125) $false % 21.83/3.96 | | | | | | | | | % 21.83/3.96 | | | | | | | | | CLOSE: (125) is inconsistent. % 21.83/3.96 | | | | | | | | | % 21.83/3.96 | | | | | | | | End of split % 21.83/3.96 | | | | | | | | % 21.83/3.96 | | | | | | | Case 2: % 21.83/3.96 | | | | | | | | % 21.83/3.97 | | | | | | | | (126) ( ~ (all_35_0 = 0) | ? [v0: $i] : (sdtasdt0(xl, v0) = % 21.83/3.97 | | | | | | | | xn & aNaturalNumber0(v0) = 0 & $i(v0))) & (all_35_0 % 21.83/3.97 | | | | | | | | = 0 | ! [v0: $i] : ( ~ (sdtasdt0(xl, v0) = xn) | ~ % 21.83/3.97 | | | | | | | | $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 21.83/3.97 | | | | | | | | aNaturalNumber0(v0) = v1))) % 21.83/3.97 | | | | | | | | % 21.83/3.97 | | | | | | | | ALPHA: (126) implies: % 21.83/3.97 | | | | | | | | (127) all_35_0 = 0 | ! [v0: $i] : ( ~ (sdtasdt0(xl, v0) = % 21.83/3.97 | | | | | | | | xn) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 21.83/3.97 | | | | | | | | aNaturalNumber0(v0) = v1)) % 21.83/3.97 | | | | | | | | % 21.83/3.97 | | | | | | | | BETA: splitting (95) gives: % 21.83/3.97 | | | | | | | | % 21.83/3.97 | | | | | | | | Case 1: % 21.83/3.97 | | | | | | | | | % 21.83/3.97 | | | | | | | | | (128) ~ (all_46_2 = 0) % 21.83/3.97 | | | | | | | | | % 21.83/3.97 | | | | | | | | | REDUCE: (90), (128) imply: % 21.83/3.97 | | | | | | | | | (129) $false % 21.83/3.97 | | | | | | | | | % 21.83/3.97 | | | | | | | | | CLOSE: (129) is inconsistent. % 21.83/3.97 | | | | | | | | | % 21.83/3.97 | | | | | | | | Case 2: % 21.83/3.97 | | | | | | | | | % 21.83/3.97 | | | | | | | | | (130) all_46_0 = 0 % 21.83/3.97 | | | | | | | | | % 21.83/3.97 | | | | | | | | | REDUCE: (47), (130) imply: % 21.83/3.97 | | | | | | | | | (131) aNaturalNumber0(all_33_0) = 0 % 21.83/3.97 | | | | | | | | | % 21.83/3.97 | | | | | | | | | BETA: splitting (127) gives: % 21.83/3.97 | | | | | | | | | % 21.83/3.97 | | | | | | | | | Case 1: % 21.83/3.97 | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | (132) all_35_0 = 0 % 21.83/3.97 | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | REDUCE: (23), (132) imply: % 21.83/3.97 | | | | | | | | | | (133) $false % 21.83/3.97 | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | CLOSE: (133) is inconsistent. % 21.83/3.97 | | | | | | | | | | % 21.83/3.97 | | | | | | | | | Case 2: % 21.83/3.97 | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | (134) ! [v0: $i] : ( ~ (sdtasdt0(xl, v0) = xn) | ~ % 21.83/3.97 | | | | | | | | | | $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 21.83/3.97 | | | | | | | | | | aNaturalNumber0(v0) = v1)) % 21.83/3.97 | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | BETA: splitting (114) gives: % 21.83/3.97 | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | Case 1: % 21.83/3.97 | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | (135) ~ (all_48_2 = 0) % 21.83/3.97 | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | REDUCE: (86), (135) imply: % 21.83/3.97 | | | | | | | | | | | (136) $false % 21.83/3.97 | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | CLOSE: (136) is inconsistent. % 21.83/3.97 | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | Case 2: % 21.83/3.97 | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | (137) all_48_0 = all_33_0 % 21.83/3.97 | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | REDUCE: (52), (137) imply: % 21.83/3.97 | | | | | | | | | | | (138) sdtpldt0(xn, xm) = all_33_0 % 21.83/3.97 | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | BETA: splitting (41) gives: % 21.83/3.97 | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | Case 1: % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | (139) ? [v0: any] : ? [v1: any] : % 21.83/3.97 | | | | | | | | | | | | (aNaturalNumber0(all_33_0) = v1 & % 21.83/3.97 | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 % 21.83/3.97 | | | | | | | | | | | | = 0))) % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | DELTA: instantiating (139) with fresh symbols all_104_0, % 21.83/3.97 | | | | | | | | | | | | all_104_1 gives: % 21.83/3.97 | | | | | | | | | | | | (140) aNaturalNumber0(all_33_0) = all_104_0 & % 21.83/3.97 | | | | | | | | | | | | aNaturalNumber0(xl) = all_104_1 & ( ~ (all_104_0 = % 21.83/3.97 | | | | | | | | | | | | 0) | ~ (all_104_1 = 0)) % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | ALPHA: (140) implies: % 21.83/3.97 | | | | | | | | | | | | (141) aNaturalNumber0(xl) = all_104_1 % 21.83/3.97 | | | | | | | | | | | | (142) aNaturalNumber0(all_33_0) = all_104_0 % 21.83/3.97 | | | | | | | | | | | | (143) ~ (all_104_0 = 0) | ~ (all_104_1 = 0) % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_104_1, xl, % 21.83/3.97 | | | | | | | | | | | | simplifying with (5), (141) gives: % 21.83/3.97 | | | | | | | | | | | | (144) all_104_1 = 0 % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_104_0, all_33_0, % 21.83/3.97 | | | | | | | | | | | | simplifying with (131), (142) gives: % 21.83/3.97 | | | | | | | | | | | | (145) all_104_0 = 0 % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | BETA: splitting (143) gives: % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | Case 1: % 21.83/3.97 | | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | | (146) ~ (all_104_0 = 0) % 21.83/3.97 | | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | | REDUCE: (145), (146) imply: % 21.83/3.97 | | | | | | | | | | | | | (147) $false % 21.83/3.97 | | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | | CLOSE: (147) is inconsistent. % 21.83/3.97 | | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | Case 2: % 21.83/3.97 | | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | | (148) ~ (all_104_1 = 0) % 21.83/3.97 | | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | | REDUCE: (144), (148) imply: % 21.83/3.97 | | | | | | | | | | | | | (149) $false % 21.83/3.97 | | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | | CLOSE: (149) is inconsistent. % 21.83/3.97 | | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | End of split % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | Case 2: % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | (150) ? [v0: $i] : (sdtasdt0(xl, v0) = all_33_0 & % 21.83/3.97 | | | | | | | | | | | | aNaturalNumber0(v0) = 0 & $i(v0)) % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | DELTA: instantiating (150) with fresh symbol all_104_0 % 21.83/3.97 | | | | | | | | | | | | gives: % 21.83/3.97 | | | | | | | | | | | | (151) sdtasdt0(xl, all_104_0) = all_33_0 & % 21.83/3.97 | | | | | | | | | | | | aNaturalNumber0(all_104_0) = 0 & $i(all_104_0) % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | ALPHA: (151) implies: % 21.83/3.97 | | | | | | | | | | | | (152) $i(all_104_0) % 21.83/3.97 | | | | | | | | | | | | (153) aNaturalNumber0(all_104_0) = 0 % 21.83/3.97 | | | | | | | | | | | | (154) sdtasdt0(xl, all_104_0) = all_33_0 % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with xl, all_79_0, xm, % 21.83/3.97 | | | | | | | | | | | | simplifying with (9), (109), (111) gives: % 21.83/3.97 | | | | | | | | | | | | (155) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 21.83/3.97 | | | | | | | | | | | | (sdtasdt0(all_79_0, xl) = v2 & % 21.83/3.97 | | | | | | | | | | | | aNaturalNumber0(all_79_0) = v1 & % 21.83/3.97 | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v2) & ( ~ (v1 = 0) % 21.83/3.97 | | | | | | | | | | | | | ~ (v0 = 0) | v2 = xm)) % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with xl, all_104_0, % 21.83/3.97 | | | | | | | | | | | | all_33_0, simplifying with (9), (152), (154) % 21.83/3.97 | | | | | | | | | | | | gives: % 21.83/3.97 | | | | | | | | | | | | (156) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 21.83/3.97 | | | | | | | | | | | | (sdtasdt0(all_104_0, xl) = v2 & % 21.83/3.97 | | | | | | | | | | | | aNaturalNumber0(all_104_0) = v1 & % 21.83/3.97 | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v2) & ( ~ (v1 = 0) % 21.83/3.97 | | | | | | | | | | | | | ~ (v0 = 0) | v2 = all_33_0)) % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | DELTA: instantiating (156) with fresh symbols all_111_0, % 21.83/3.97 | | | | | | | | | | | | all_111_1, all_111_2 gives: % 21.83/3.97 | | | | | | | | | | | | (157) sdtasdt0(all_104_0, xl) = all_111_0 & % 21.83/3.97 | | | | | | | | | | | | aNaturalNumber0(all_104_0) = all_111_1 & % 21.83/3.97 | | | | | | | | | | | | aNaturalNumber0(xl) = all_111_2 & $i(all_111_0) & % 21.83/3.97 | | | | | | | | | | | | ( ~ (all_111_1 = 0) | ~ (all_111_2 = 0) | % 21.83/3.97 | | | | | | | | | | | | all_111_0 = all_33_0) % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | ALPHA: (157) implies: % 21.83/3.97 | | | | | | | | | | | | (158) aNaturalNumber0(xl) = all_111_2 % 21.83/3.97 | | | | | | | | | | | | (159) aNaturalNumber0(all_104_0) = all_111_1 % 21.83/3.97 | | | | | | | | | | | | (160) sdtasdt0(all_104_0, xl) = all_111_0 % 21.83/3.97 | | | | | | | | | | | | (161) ~ (all_111_1 = 0) | ~ (all_111_2 = 0) | % 21.83/3.97 | | | | | | | | | | | | all_111_0 = all_33_0 % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | DELTA: instantiating (155) with fresh symbols all_113_0, % 21.83/3.97 | | | | | | | | | | | | all_113_1, all_113_2 gives: % 21.83/3.97 | | | | | | | | | | | | (162) sdtasdt0(all_79_0, xl) = all_113_0 & % 21.83/3.97 | | | | | | | | | | | | aNaturalNumber0(all_79_0) = all_113_1 & % 21.83/3.97 | | | | | | | | | | | | aNaturalNumber0(xl) = all_113_2 & $i(all_113_0) & % 21.83/3.97 | | | | | | | | | | | | ( ~ (all_113_1 = 0) | ~ (all_113_2 = 0) | % 21.83/3.97 | | | | | | | | | | | | all_113_0 = xm) % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | ALPHA: (162) implies: % 21.83/3.97 | | | | | | | | | | | | (163) $i(all_113_0) % 21.83/3.97 | | | | | | | | | | | | (164) aNaturalNumber0(xl) = all_113_2 % 21.83/3.97 | | | | | | | | | | | | (165) aNaturalNumber0(all_79_0) = all_113_1 % 21.83/3.97 | | | | | | | | | | | | (166) sdtasdt0(all_79_0, xl) = all_113_0 % 21.83/3.97 | | | | | | | | | | | | (167) ~ (all_113_1 = 0) | ~ (all_113_2 = 0) | % 21.83/3.97 | | | | | | | | | | | | all_113_0 = xm % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.97 | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_113_2, xl, % 21.83/3.97 | | | | | | | | | | | | simplifying with (5), (164) gives: % 21.83/3.97 | | | | | | | | | | | | (168) all_113_2 = 0 % 21.83/3.97 | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_111_2, all_113_2, xl, % 21.83/3.98 | | | | | | | | | | | | simplifying with (158), (164) gives: % 21.83/3.98 | | | | | | | | | | | | (169) all_113_2 = all_111_2 % 21.83/3.98 | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_113_1, all_79_0, % 21.83/3.98 | | | | | | | | | | | | simplifying with (110), (165) gives: % 21.83/3.98 | | | | | | | | | | | | (170) all_113_1 = 0 % 21.83/3.98 | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_111_1, all_104_0, % 21.83/3.98 | | | | | | | | | | | | simplifying with (153), (159) gives: % 21.83/3.98 | | | | | | | | | | | | (171) all_111_1 = 0 % 21.83/3.98 | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | COMBINE_EQS: (168), (169) imply: % 21.83/3.98 | | | | | | | | | | | | (172) all_111_2 = 0 % 21.83/3.98 | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | SIMP: (172) implies: % 21.83/3.98 | | | | | | | | | | | | (173) all_111_2 = 0 % 21.83/3.98 | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | BETA: splitting (161) gives: % 21.83/3.98 | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | Case 1: % 21.83/3.98 | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | (174) ~ (all_111_1 = 0) % 21.83/3.98 | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | REDUCE: (171), (174) imply: % 21.83/3.98 | | | | | | | | | | | | | (175) $false % 21.83/3.98 | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | CLOSE: (175) is inconsistent. % 21.83/3.98 | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | Case 2: % 21.83/3.98 | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | (176) ~ (all_111_2 = 0) | all_111_0 = all_33_0 % 21.83/3.98 | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | BETA: splitting (176) gives: % 21.83/3.98 | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | Case 1: % 21.83/3.98 | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | (177) ~ (all_111_2 = 0) % 21.83/3.98 | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | REDUCE: (173), (177) imply: % 21.83/3.98 | | | | | | | | | | | | | | (178) $false % 21.83/3.98 | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | CLOSE: (178) is inconsistent. % 21.83/3.98 | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | Case 2: % 21.83/3.98 | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | (179) all_111_0 = all_33_0 % 21.83/3.98 | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | REDUCE: (160), (179) imply: % 21.83/3.98 | | | | | | | | | | | | | | (180) sdtasdt0(all_104_0, xl) = all_33_0 % 21.83/3.98 | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | BETA: splitting (167) gives: % 21.83/3.98 | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | Case 1: % 21.83/3.98 | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | (181) ~ (all_113_1 = 0) % 21.83/3.98 | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | REDUCE: (170), (181) imply: % 21.83/3.98 | | | | | | | | | | | | | | | (182) $false % 21.83/3.98 | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | CLOSE: (182) is inconsistent. % 21.83/3.98 | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | Case 2: % 21.83/3.98 | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | (183) ~ (all_113_2 = 0) | all_113_0 = xm % 21.83/3.98 | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | BETA: splitting (183) gives: % 21.83/3.98 | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | Case 1: % 21.83/3.98 | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | (184) ~ (all_113_2 = 0) % 21.83/3.98 | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | REDUCE: (168), (184) imply: % 21.83/3.98 | | | | | | | | | | | | | | | | (185) $false % 21.83/3.98 | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | CLOSE: (185) is inconsistent. % 21.83/3.98 | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | Case 2: % 21.83/3.98 | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | (186) all_113_0 = xm % 21.83/3.98 | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | REDUCE: (166), (186) imply: % 21.83/3.98 | | | | | | | | | | | | | | | | (187) sdtasdt0(all_79_0, xl) = xm % 21.83/3.98 | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | BETA: splitting (29) gives: % 21.83/3.98 | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | Case 1: % 21.83/3.98 | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | (188) xl = sz00 % 21.83/3.98 | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | REDUCE: (26), (188) imply: % 21.83/3.98 | | | | | | | | | | | | | | | | | (189) doDivides0(sz00, xn) = all_35_0 % 21.83/3.98 | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | REDUCE: (20), (188) imply: % 21.83/3.98 | | | | | | | | | | | | | | | | | (190) doDivides0(sz00, xm) = 0 % 21.83/3.98 | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | REDUCE: (180), (188) imply: % 21.83/3.98 | | | | | | | | | | | | | | | | | (191) sdtasdt0(all_104_0, sz00) = all_33_0 % 21.83/3.98 | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | REDUCE: (187), (188) imply: % 21.83/3.98 | | | | | | | | | | | | | | | | | (192) sdtasdt0(all_79_0, sz00) = xm % 21.83/3.98 | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | REDUCE: (154), (188) imply: % 21.83/3.98 | | | | | | | | | | | | | | | | | (193) sdtasdt0(sz00, all_104_0) = all_33_0 % 21.83/3.98 | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | REDUCE: (111), (188) imply: % 21.83/3.98 | | | | | | | | | | | | | | | | | (194) sdtasdt0(sz00, all_79_0) = xm % 21.83/3.98 | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | BETA: splitting (33) gives: % 21.83/3.98 | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | Case 1: % 21.83/3.98 | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | (195) xm = sz00 % 21.83/3.98 | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | REDUCE: (61), (195) imply: % 21.83/3.98 | | | | | | | | | | | | | | | | | | (196) doDivides0(sz00, xn) = all_58_0 % 21.83/3.98 | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | REDUCE: (190), (195) imply: % 21.83/3.98 | | | | | | | | | | | | | | | | | | (197) doDivides0(sz00, sz00) = 0 % 21.83/3.98 | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | REDUCE: (192), (195) imply: % 21.83/3.98 | | | | | | | | | | | | | | | | | | (198) sdtasdt0(all_79_0, sz00) = sz00 % 21.83/3.98 | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | REDUCE: (194), (195) imply: % 21.83/3.98 | | | | | | | | | | | | | | | | | | (199) sdtasdt0(sz00, all_79_0) = sz00 % 21.83/3.98 | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | REDUCE: (19), (195) imply: % 21.83/3.98 | | | | | | | | | | | | | | | | | | (200) sdtpldt0(sz00, xn) = all_33_0 % 21.83/3.98 | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | REDUCE: (10), (195) imply: % 21.83/3.98 | | | | | | | | | | | | | | | | | | (201) $i(sz00) % 21.83/3.98 | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (17) with all_35_0, all_58_0, xn, % 21.83/3.98 | | | | | | | | | | | | | | | | | | sz00, simplifying with (189), (196) gives: % 21.83/3.98 | | | | | | | | | | | | | | | | | | (202) all_58_0 = all_35_0 % 21.83/3.98 | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | BETA: splitting (34) gives: % 21.83/3.98 | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | Case 1: % 21.83/3.98 | | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | | (203) xn = sz00 % 21.83/3.98 | | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | | REDUCE: (189), (203) imply: % 21.83/3.98 | | | | | | | | | | | | | | | | | | | (204) doDivides0(sz00, sz00) = all_35_0 % 21.83/3.98 | | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (17) with 0, all_35_0, sz00, sz00, % 21.83/3.98 | | | | | | | | | | | | | | | | | | | simplifying with (197), (204) gives: % 21.83/3.98 | | | | | | | | | | | | | | | | | | | (205) all_35_0 = 0 % 21.83/3.98 | | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | | REDUCE: (23), (205) imply: % 21.83/3.98 | | | | | | | | | | | | | | | | | | | (206) $false % 21.83/3.98 | | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | | CLOSE: (206) is inconsistent. % 21.83/3.98 | | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | Case 2: % 21.83/3.98 | | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | | (207) ~ (xn = sz00) % 21.83/3.98 | | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (1) with xn, all_33_0, simplifying % 21.83/3.98 | | | | | | | | | | | | | | | | | | | with (11), (200) gives: % 21.83/3.98 | | | | | | | | | | | | | | | | | | | (208) ? [v0: any] : ? [v1: $i] : (sdtpldt0(xn, sz00) = % 21.83/3.98 | | | | | | | | | | | | | | | | | | | v1 & aNaturalNumber0(xn) = v0 & $i(v1) & ( ~ (v0 % 21.83/3.98 | | | | | | | | | | | | | | | | | | | = 0) | (v1 = xn & all_33_0 = xn))) % 21.83/3.98 | | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mMulAsso) with sz00, all_79_0, % 21.83/3.98 | | | | | | | | | | | | | | | | | | | all_104_0, sz00, all_33_0, simplifying with (109), % 21.83/3.98 | | | | | | | | | | | | | | | | | | | (152), (193), (199), (201) gives: % 21.83/3.98 | | | | | | | | | | | | | | | | | | | (209) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 21.83/3.98 | | | | | | | | | | | | | | | | | | | [v3: $i] : ? [v4: $i] : (sdtasdt0(all_79_0, % 21.83/3.98 | | | | | | | | | | | | | | | | | | | all_104_0) = v3 & sdtasdt0(sz00, v3) = v4 & % 21.83/3.98 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_104_0) = v2 & % 21.83/3.98 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_79_0) = v1 & % 21.83/3.98 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(sz00) = v0 & $i(v4) & $i(v3) & ( % 21.83/3.98 | | | | | | | | | | | | | | | | | | | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = % 21.83/3.98 | | | | | | | | | | | | | | | | | | | all_33_0)) % 21.83/3.98 | | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (2) with all_104_0, all_33_0, % 21.83/3.98 | | | | | | | | | | | | | | | | | | | simplifying with (152), (193) gives: % 21.83/3.98 | | | | | | | | | | | | | | | | | | | (210) ? [v0: any] : ? [v1: $i] : (sdtasdt0(all_104_0, % 21.83/3.98 | | | | | | | | | | | | | | | | | | | sz00) = v1 & aNaturalNumber0(all_104_0) = v0 & % 21.83/3.98 | | | | | | | | | | | | | | | | | | | $i(v1) & ( ~ (v0 = 0) | (v1 = sz00 & all_33_0 = % 21.83/3.98 | | | | | | | | | | | | | | | | | | | sz00))) % 21.83/3.98 | | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mMulAsso) with all_79_0, sz00, % 21.83/3.98 | | | | | | | | | | | | | | | | | | | all_104_0, sz00, all_33_0, simplifying with (109), % 21.83/3.98 | | | | | | | | | | | | | | | | | | | (152), (193), (198), (201) gives: % 21.83/3.98 | | | | | | | | | | | | | | | | | | | (211) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 21.83/3.98 | | | | | | | | | | | | | | | | | | | [v3: $i] : ? [v4: $i] : (sdtasdt0(all_79_0, v3) = % 21.83/3.98 | | | | | | | | | | | | | | | | | | | v4 & sdtasdt0(sz00, all_104_0) = v3 & % 21.83/3.98 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_104_0) = v2 & % 21.83/3.98 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_79_0) = v0 & % 21.83/3.98 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(sz00) = v1 & $i(v4) & $i(v3) & ( % 21.83/3.98 | | | | | | | | | | | | | | | | | | | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = % 21.83/3.98 | | | | | | | | | | | | | | | | | | | all_33_0)) % 21.83/3.98 | | | | | | | | | | | | | | | | | | | % 21.83/3.98 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (210) with fresh symbols all_176_0, % 21.83/3.98 | | | | | | | | | | | | | | | | | | | all_176_1 gives: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (212) sdtasdt0(all_104_0, sz00) = all_176_0 & % 21.83/3.99 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_104_0) = all_176_1 & % 21.83/3.99 | | | | | | | | | | | | | | | | | | | $i(all_176_0) & ( ~ (all_176_1 = 0) | (all_176_0 = % 21.83/3.99 | | | | | | | | | | | | | | | | | | | sz00 & all_33_0 = sz00)) % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | ALPHA: (212) implies: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (213) aNaturalNumber0(all_104_0) = all_176_1 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (214) sdtasdt0(all_104_0, sz00) = all_176_0 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (215) ~ (all_176_1 = 0) | (all_176_0 = sz00 & all_33_0 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | = sz00) % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (208) with fresh symbols all_178_0, % 21.83/3.99 | | | | | | | | | | | | | | | | | | | all_178_1 gives: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (216) sdtpldt0(xn, sz00) = all_178_0 & % 21.83/3.99 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xn) = all_178_1 & $i(all_178_0) & % 21.83/3.99 | | | | | | | | | | | | | | | | | | | ( ~ (all_178_1 = 0) | (all_178_0 = xn & all_33_0 = % 21.83/3.99 | | | | | | | | | | | | | | | | | | | xn)) % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | ALPHA: (216) implies: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (217) aNaturalNumber0(xn) = all_178_1 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (218) ~ (all_178_1 = 0) | (all_178_0 = xn & all_33_0 = % 21.83/3.99 | | | | | | | | | | | | | | | | | | | xn) % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (209) with fresh symbols all_182_0, % 21.83/3.99 | | | | | | | | | | | | | | | | | | | all_182_1, all_182_2, all_182_3, all_182_4 gives: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (219) sdtasdt0(all_79_0, all_104_0) = all_182_1 & % 21.83/3.99 | | | | | | | | | | | | | | | | | | | sdtasdt0(sz00, all_182_1) = all_182_0 & % 21.83/3.99 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_104_0) = all_182_2 & % 21.83/3.99 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_79_0) = all_182_3 & % 21.83/3.99 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(sz00) = all_182_4 & $i(all_182_0) % 21.83/3.99 | | | | | | | | | | | | | | | | | | | & $i(all_182_1) & ( ~ (all_182_2 = 0) | ~ % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (all_182_3 = 0) | ~ (all_182_4 = 0) | all_182_0 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | = all_33_0) % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | ALPHA: (219) implies: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (220) aNaturalNumber0(all_104_0) = all_182_2 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (211) with fresh symbols all_184_0, % 21.83/3.99 | | | | | | | | | | | | | | | | | | | all_184_1, all_184_2, all_184_3, all_184_4 gives: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (221) sdtasdt0(all_79_0, all_184_1) = all_184_0 & % 21.83/3.99 | | | | | | | | | | | | | | | | | | | sdtasdt0(sz00, all_104_0) = all_184_1 & % 21.83/3.99 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_104_0) = all_184_2 & % 21.83/3.99 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_79_0) = all_184_4 & % 21.83/3.99 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(sz00) = all_184_3 & $i(all_184_0) % 21.83/3.99 | | | | | | | | | | | | | | | | | | | & $i(all_184_1) & ( ~ (all_184_2 = 0) | ~ % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (all_184_3 = 0) | ~ (all_184_4 = 0) | all_184_0 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | = all_33_0) % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | ALPHA: (221) implies: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (222) aNaturalNumber0(all_104_0) = all_184_2 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_178_1, xn, % 21.83/3.99 | | | | | | | | | | | | | | | | | | | simplifying with (7), (217) gives: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (223) all_178_1 = 0 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_182_2, all_104_0, % 21.83/3.99 | | | | | | | | | | | | | | | | | | | simplifying with (153), (220) gives: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (224) all_182_2 = 0 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_182_2, all_184_2, % 21.83/3.99 | | | | | | | | | | | | | | | | | | | all_104_0, simplifying with (220), (222) gives: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (225) all_184_2 = all_182_2 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_176_1, all_184_2, % 21.83/3.99 | | | | | | | | | | | | | | | | | | | all_104_0, simplifying with (213), (222) gives: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (226) all_184_2 = all_176_1 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (15) with all_33_0, all_176_0, sz00, % 21.83/3.99 | | | | | | | | | | | | | | | | | | | all_104_0, simplifying with (191), (214) gives: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (227) all_176_0 = all_33_0 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (225), (226) imply: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (228) all_182_2 = all_176_1 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | SIMP: (228) implies: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (229) all_182_2 = all_176_1 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (224), (229) imply: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (230) all_176_1 = 0 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | BETA: splitting (215) gives: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | Case 1: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | (231) ~ (all_176_1 = 0) % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | REDUCE: (230), (231) imply: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | (232) $false % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | CLOSE: (232) is inconsistent. % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | Case 2: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | (233) all_176_0 = sz00 & all_33_0 = sz00 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | ALPHA: (233) implies: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | (234) all_176_0 = sz00 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (227), (234) imply: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | (235) all_33_0 = sz00 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | BETA: splitting (218) gives: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | Case 1: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | (236) ~ (all_178_1 = 0) % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | REDUCE: (223), (236) imply: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | (237) $false % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | CLOSE: (237) is inconsistent. % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | Case 2: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | (238) all_178_0 = xn & all_33_0 = xn % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | ALPHA: (238) implies: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | (239) all_33_0 = xn % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (235), (239) imply: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | (240) xn = sz00 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | REDUCE: (207), (240) imply: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | (241) $false % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | CLOSE: (241) is inconsistent. % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | End of split % 21.83/3.99 | | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | End of split % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | End of split % 21.83/3.99 | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | Case 2: % 21.83/3.99 | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | (242) ~ (xm = sz00) % 21.83/3.99 | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (2) with all_79_0, xm, simplifying % 21.83/3.99 | | | | | | | | | | | | | | | | | | with (109), (194) gives: % 21.83/3.99 | | | | | | | | | | | | | | | | | | (243) ? [v0: any] : ? [v1: $i] : (sdtasdt0(all_79_0, % 21.83/3.99 | | | | | | | | | | | | | | | | | | sz00) = v1 & aNaturalNumber0(all_79_0) = v0 & % 21.83/3.99 | | | | | | | | | | | | | | | | | | $i(v1) & ( ~ (v0 = 0) | (v1 = sz00 & xm = % 21.83/3.99 | | | | | | | | | | | | | | | | | | sz00))) % 21.83/3.99 | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | DELTA: instantiating (243) with fresh symbols all_174_0, % 21.83/3.99 | | | | | | | | | | | | | | | | | | all_174_1 gives: % 21.83/3.99 | | | | | | | | | | | | | | | | | | (244) sdtasdt0(all_79_0, sz00) = all_174_0 & % 21.83/3.99 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_79_0) = all_174_1 & % 21.83/3.99 | | | | | | | | | | | | | | | | | | $i(all_174_0) & ( ~ (all_174_1 = 0) | (all_174_0 = % 21.83/3.99 | | | | | | | | | | | | | | | | | | sz00 & xm = sz00)) % 21.83/3.99 | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | ALPHA: (244) implies: % 21.83/3.99 | | | | | | | | | | | | | | | | | | (245) aNaturalNumber0(all_79_0) = all_174_1 % 21.83/3.99 | | | | | | | | | | | | | | | | | | (246) ~ (all_174_1 = 0) | (all_174_0 = sz00 & xm = % 21.83/3.99 | | | | | | | | | | | | | | | | | | sz00) % 21.83/3.99 | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | BETA: splitting (246) gives: % 21.83/3.99 | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | Case 1: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (247) ~ (all_174_1 = 0) % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_174_1, all_79_0, % 21.83/3.99 | | | | | | | | | | | | | | | | | | | simplifying with (110), (245) gives: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (248) all_174_1 = 0 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | REDUCE: (247), (248) imply: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (249) $false % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | CLOSE: (249) is inconsistent. % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | Case 2: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (250) all_174_0 = sz00 & xm = sz00 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | ALPHA: (250) implies: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (251) xm = sz00 % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | REDUCE: (242), (251) imply: % 21.83/3.99 | | | | | | | | | | | | | | | | | | | (252) $false % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | | CLOSE: (252) is inconsistent. % 21.83/3.99 | | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | | End of split % 21.83/3.99 | | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | End of split % 21.83/3.99 | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | Case 2: % 21.83/3.99 | | | | | | | | | | | | | | | | | % 21.83/3.99 | | | | | | | | | | | | | | | | | (253) ~ (xl = sz00) % 21.83/4.00 | | | | | | | | | | | | | | | | | (254) ? [v0: $i] : ? [v1: $i] : (sdtasdt0(xl, % 21.83/4.00 | | | | | | | | | | | | | | | | | all_35_3) = v0 & sdtpldt0(v0, xn) = v1 & % 21.83/4.00 | | | | | | | | | | | | | | | | | $i(v1) & $i(v0) & ? [v2: $i] : % 21.83/4.00 | | | | | | | | | | | | | | | | | (sdtmndt0(all_35_1, all_35_3) = v2 & % 21.83/4.00 | | | | | | | | | | | | | | | | | sdtlseqdt0(all_35_3, all_35_1) = 0 & % 21.83/4.00 | | | | | | | | | | | | | | | | | sdtasdt0(xl, v2) = xn & $i(v2))) % 21.83/4.00 | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | DELTA: instantiating (254) with fresh symbols all_154_0, % 21.83/4.00 | | | | | | | | | | | | | | | | | all_154_1 gives: % 21.83/4.00 | | | | | | | | | | | | | | | | | (255) sdtasdt0(xl, all_35_3) = all_154_1 & % 21.83/4.00 | | | | | | | | | | | | | | | | | sdtpldt0(all_154_1, xn) = all_154_0 & % 21.83/4.00 | | | | | | | | | | | | | | | | | $i(all_154_0) & $i(all_154_1) & ? [v0: $i] : % 21.83/4.00 | | | | | | | | | | | | | | | | | (sdtmndt0(all_35_1, all_35_3) = v0 & % 21.83/4.00 | | | | | | | | | | | | | | | | | sdtlseqdt0(all_35_3, all_35_1) = 0 & % 21.83/4.00 | | | | | | | | | | | | | | | | | sdtasdt0(xl, v0) = xn & $i(v0)) % 21.83/4.00 | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | ALPHA: (255) implies: % 21.83/4.00 | | | | | | | | | | | | | | | | | (256) sdtpldt0(all_154_1, xn) = all_154_0 % 21.83/4.00 | | | | | | | | | | | | | | | | | (257) sdtasdt0(xl, all_35_3) = all_154_1 % 21.83/4.00 | | | | | | | | | | | | | | | | | (258) ? [v0: $i] : (sdtmndt0(all_35_1, all_35_3) = v0 & % 21.83/4.00 | | | | | | | | | | | | | | | | | sdtlseqdt0(all_35_3, all_35_1) = 0 & % 21.83/4.00 | | | | | | | | | | | | | | | | | sdtasdt0(xl, v0) = xn & $i(v0)) % 21.83/4.00 | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | DELTA: instantiating (258) with fresh symbol all_156_0 % 21.83/4.00 | | | | | | | | | | | | | | | | | gives: % 21.83/4.00 | | | | | | | | | | | | | | | | | (259) sdtmndt0(all_35_1, all_35_3) = all_156_0 & % 21.83/4.00 | | | | | | | | | | | | | | | | | sdtlseqdt0(all_35_3, all_35_1) = 0 & sdtasdt0(xl, % 21.83/4.00 | | | | | | | | | | | | | | | | | all_156_0) = xn & $i(all_156_0) % 21.83/4.00 | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | ALPHA: (259) implies: % 21.83/4.00 | | | | | | | | | | | | | | | | | (260) $i(all_156_0) % 21.83/4.00 | | | | | | | | | | | | | | | | | (261) sdtasdt0(xl, all_156_0) = xn % 21.83/4.00 | | | | | | | | | | | | | | | | | (262) sdtlseqdt0(all_35_3, all_35_1) = 0 % 21.83/4.00 | | | | | | | | | | | | | | | | | (263) sdtmndt0(all_35_1, all_35_3) = all_156_0 % 21.83/4.00 | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | BETA: splitting (42) gives: % 21.83/4.00 | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | Case 1: % 21.83/4.00 | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | (264) xl = sz00 % 21.83/4.00 | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | REDUCE: (253), (264) imply: % 21.83/4.00 | | | | | | | | | | | | | | | | | | (265) $false % 21.83/4.00 | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | CLOSE: (265) is inconsistent. % 21.83/4.00 | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | Case 2: % 21.83/4.00 | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | (266) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 21.83/4.00 | | | | | | | | | | | | | | | | | | (doDivides0(xl, xm) = v2 & aNaturalNumber0(xm) = % 21.83/4.00 | | | | | | | | | | | | | | | | | | v1 & aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | % 21.83/4.00 | | | | | | | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0))) | ( ! [v0: any] : % 21.83/4.00 | | | | | | | | | | | | | | | | | | (v0 = all_35_3 | ~ (sdtasdt0(xl, v0) = xm) | ~ % 21.83/4.00 | | | | | | | | | | | | | | | | | | $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 21.83/4.00 | | | | | | | | | | | | | | | | | | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( % 21.83/4.00 | | | | | | | | | | | | | | | | | | ~ (sdtasdt0(xl, all_35_3) = v0) | ~ % 21.83/4.00 | | | | | | | | | | | | | | | | | | $i(all_35_3) | (v0 = xm & % 21.83/4.00 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_3) = 0))) % 21.83/4.00 | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | BETA: splitting (43) gives: % 21.83/4.00 | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | Case 1: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | (267) xl = sz00 % 21.83/4.00 | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | REDUCE: (253), (267) imply: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | (268) $false % 21.83/4.00 | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | CLOSE: (268) is inconsistent. % 21.83/4.00 | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | Case 2: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | (269) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 21.83/4.00 | | | | | | | | | | | | | | | | | | | (doDivides0(xl, all_33_0) = v2 & % 21.83/4.00 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_33_0) = v1 & % 21.83/4.00 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | ~ (v1 % 21.83/4.00 | | | | | | | | | | | | | | | | | | | = 0) | ~ (v0 = 0))) | ( ! [v0: any] : (v0 = % 21.83/4.00 | | | | | | | | | | | | | | | | | | | all_35_1 | ~ (sdtasdt0(xl, v0) = all_33_0) | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 21.83/4.00 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( % 21.83/4.00 | | | | | | | | | | | | | | | | | | | ~ (sdtasdt0(xl, all_35_1) = v0) | ~ % 21.83/4.00 | | | | | | | | | | | | | | | | | | | $i(all_35_1) | (v0 = all_33_0 & % 21.83/4.00 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_1) = 0))) % 21.83/4.00 | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | BETA: splitting (266) gives: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | Case 1: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | (270) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | (doDivides0(xl, xm) = v2 & aNaturalNumber0(xm) = % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | v1 & aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0))) % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (270) with fresh symbols all_174_0, % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | all_174_1, all_174_2 gives: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | (271) doDivides0(xl, xm) = all_174_0 & % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xm) = all_174_1 & % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = all_174_2 & ( ~ (all_174_0 = % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | 0) | ~ (all_174_1 = 0) | ~ (all_174_2 = 0)) % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | ALPHA: (271) implies: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | (272) aNaturalNumber0(xl) = all_174_2 % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | (273) aNaturalNumber0(xm) = all_174_1 % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | (274) doDivides0(xl, xm) = all_174_0 % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | (275) ~ (all_174_0 = 0) | ~ (all_174_1 = 0) | ~ % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | (all_174_2 = 0) % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_174_2, xl, % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | simplifying with (5), (272) gives: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | (276) all_174_2 = 0 % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_174_1, xm, % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | simplifying with (6), (273) gives: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | (277) all_174_1 = 0 % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (17) with 0, all_174_0, xm, xl, % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | simplifying with (20), (274) gives: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | (278) all_174_0 = 0 % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | BETA: splitting (275) gives: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | Case 1: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | (279) ~ (all_174_0 = 0) % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | REDUCE: (278), (279) imply: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | (280) $false % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | CLOSE: (280) is inconsistent. % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | Case 2: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | (281) ~ (all_174_1 = 0) | ~ (all_174_2 = 0) % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | BETA: splitting (281) gives: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | Case 1: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | | (282) ~ (all_174_1 = 0) % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (277), (282) imply: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | | (283) $false % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | | CLOSE: (283) is inconsistent. % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | Case 2: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | | (284) ~ (all_174_2 = 0) % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (276), (284) imply: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | | (285) $false % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | | CLOSE: (285) is inconsistent. % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | End of split % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | End of split % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | Case 2: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | (286) ! [v0: any] : (v0 = all_35_3 | ~ (sdtasdt0(xl, % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | v0) = xm) | ~ $i(v0) | ? [v1: int] : ( ~ % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | (v1 = 0) & aNaturalNumber0(v0) = v1)) & ! % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | [v0: $i] : ( ~ (sdtasdt0(xl, all_35_3) = v0) | ~ % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | $i(all_35_3) | (v0 = xm & % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_3) = 0)) % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | ALPHA: (286) implies: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | (287) ! [v0: any] : (v0 = all_35_3 | ~ (sdtasdt0(xl, % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | v0) = xm) | ~ $i(v0) | ? [v1: int] : ( ~ % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | (v1 = 0) & aNaturalNumber0(v0) = v1)) % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (287) with all_79_0, simplifying % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | with (109), (111) gives: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | (288) all_79_0 = all_35_3 | ? [v0: int] : ( ~ (v0 = 0) % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | & aNaturalNumber0(all_79_0) = v0) % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | BETA: splitting (269) gives: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | Case 1: % 21.83/4.00 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | (289) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | (doDivides0(xl, all_33_0) = v2 & % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_33_0) = v1 & % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | ~ (v1 % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | = 0) | ~ (v0 = 0))) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (289) with fresh symbols all_174_0, % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | all_174_1, all_174_2 gives: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | (290) doDivides0(xl, all_33_0) = all_174_0 & % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_33_0) = all_174_1 & % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = all_174_2 & ( ~ (all_174_0 = % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | 0) | ~ (all_174_1 = 0) | ~ (all_174_2 = 0)) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | ALPHA: (290) implies: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | (291) aNaturalNumber0(xl) = all_174_2 % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | (292) aNaturalNumber0(all_33_0) = all_174_1 % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | (293) doDivides0(xl, all_33_0) = all_174_0 % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | (294) ~ (all_174_0 = 0) | ~ (all_174_1 = 0) | ~ % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | (all_174_2 = 0) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_174_2, xl, % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | simplifying with (5), (291) gives: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | (295) all_174_2 = 0 % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_174_1, all_33_0, % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | simplifying with (131), (292) gives: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | (296) all_174_1 = 0 % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (17) with 0, all_174_0, all_33_0, % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | xl, simplifying with (21), (293) gives: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | (297) all_174_0 = 0 % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | BETA: splitting (294) gives: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | Case 1: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | (298) ~ (all_174_0 = 0) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (297), (298) imply: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | (299) $false % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | CLOSE: (299) is inconsistent. % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | Case 2: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | (300) ~ (all_174_1 = 0) | ~ (all_174_2 = 0) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (300) gives: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | Case 1: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (301) ~ (all_174_1 = 0) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (296), (301) imply: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (302) $false % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (302) is inconsistent. % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | Case 2: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (303) ~ (all_174_2 = 0) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (295), (303) imply: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (304) $false % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (304) is inconsistent. % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | End of split % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | End of split % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | Case 2: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | (305) ! [v0: any] : (v0 = all_35_1 | ~ (sdtasdt0(xl, % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | v0) = all_33_0) | ~ $i(v0) | ? [v1: int] : % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | ( ~ (v1 = 0) & aNaturalNumber0(v0) = v1)) & ! % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | [v0: $i] : ( ~ (sdtasdt0(xl, all_35_1) = v0) | ~ % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | $i(all_35_1) | (v0 = all_33_0 & % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_1) = 0)) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | ALPHA: (305) implies: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | (306) ! [v0: any] : (v0 = all_35_1 | ~ (sdtasdt0(xl, % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | v0) = all_33_0) | ~ $i(v0) | ? [v1: int] : % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | ( ~ (v1 = 0) & aNaturalNumber0(v0) = v1)) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (306) with all_104_0, simplifying % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | with (152), (154) gives: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | (307) all_104_0 = all_35_1 | ? [v0: int] : ( ~ (v0 = 0) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | & aNaturalNumber0(all_104_0) = v0) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | BETA: splitting (307) gives: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | Case 1: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | (308) all_104_0 = all_35_1 % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (153), (308) imply: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | (309) aNaturalNumber0(all_35_1) = 0 % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (152), (308) imply: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | (310) $i(all_35_1) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (288) gives: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | Case 1: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (311) all_79_0 = all_35_3 % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (111), (311) imply: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (312) sdtasdt0(xl, all_35_3) = xm % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (110), (311) imply: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (313) aNaturalNumber0(all_35_3) = 0 % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (109), (311) imply: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (314) $i(all_35_3) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (15) with xm, all_154_1, all_35_3, % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | xl, simplifying with (257), (312) gives: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (315) all_154_1 = xm % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (256), (315) imply: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (316) sdtpldt0(xm, xn) = all_154_0 % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with all_33_0, all_154_0, xn, % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | xm, simplifying with (19), (316) gives: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (317) all_154_0 = all_33_0 % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mAMDistr) with xl, all_156_0, % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | all_35_3, xn, xm, all_33_0, simplifying with (9), % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (138), (260), (261), (312), (314) gives: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (318) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | : ? [v7: $i] : ? [v8: $i] : (sdtasdt0(v3, xl) = % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | v5 & sdtasdt0(all_156_0, xl) = v6 & % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(all_35_3, xl) = v7 & sdtasdt0(xl, v3) = % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | v4 & sdtpldt0(v6, v7) = v8 & sdtpldt0(all_156_0, % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | all_35_3) = v3 & aNaturalNumber0(all_156_0) = % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | v1 & aNaturalNumber0(all_35_3) = v2 & % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v8) & $i(v7) & % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | $i(v6) & $i(v5) & $i(v4) & $i(v3) & ( ~ (v2 = 0) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0) | (v8 = v5 & v4 = % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | all_33_0))) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mAMDistr) with xl, all_35_3, % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | all_156_0, xm, xn, all_33_0, simplifying with (9), % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (19), (260), (261), (312), (314) gives: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (319) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | : ? [v7: $i] : ? [v8: $i] : (sdtasdt0(v3, xl) = % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | v5 & sdtasdt0(all_156_0, xl) = v7 & % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(all_35_3, xl) = v6 & sdtasdt0(xl, v3) = % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | v4 & sdtpldt0(v6, v7) = v8 & sdtpldt0(all_35_3, % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | all_156_0) = v3 & aNaturalNumber0(all_156_0) = % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | v2 & aNaturalNumber0(all_35_3) = v1 & % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v8) & $i(v7) & % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | $i(v6) & $i(v5) & $i(v4) & $i(v3) & ( ~ (v2 = 0) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0) | (v8 = v5 & v4 = % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | all_33_0))) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (134) with all_156_0, simplifying % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | with (260), (261) gives: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (320) ? [v0: int] : ( ~ (v0 = 0) & % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_156_0) = v0) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with xl, all_156_0, xn, % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | simplifying with (9), (260), (261) gives: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (321) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (sdtasdt0(all_156_0, xl) = v2 & % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_156_0) = v1 & % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v2) & ( ~ (v1 = 0) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | | ~ (v0 = 0) | v2 = xn)) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mSortsB_02) with xl, all_156_0, xn, % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | simplifying with (9), (260), (261) gives: % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (322) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | (aNaturalNumber0(all_156_0) = v1 & % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xn) = v2 & aNaturalNumber0(xl) = % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mDefDiff) with all_35_3, all_35_1, % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | all_156_0, simplifying with (263), (310), (314) % 21.83/4.01 | | | | | | | | | | | | | | | | | | | | | | | gives: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (323) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (sdtlseqdt0(all_35_3, all_35_1) = v2 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_1) = v1 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_3) = v0 & ( ~ (v2 = 0) | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0))) | ( ! [v0: any] : % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (v0 = all_156_0 | ~ (sdtpldt0(all_35_3, v0) = % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | all_35_1) | ~ $i(v0) | ? [v1: int] : ( ~ % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (v1 = 0) & aNaturalNumber0(v0) = v1)) & ! % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | [v0: $i] : ( ~ (sdtpldt0(all_35_3, all_156_0) = % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | v0) | ~ $i(all_156_0) | (v0 = all_35_1 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_156_0) = 0))) % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (320) with fresh symbol all_209_0 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | gives: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (324) ~ (all_209_0 = 0) & aNaturalNumber0(all_156_0) = % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | all_209_0 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (324) implies: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (325) ~ (all_209_0 = 0) % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (326) aNaturalNumber0(all_156_0) = all_209_0 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (322) with fresh symbols all_211_0, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | all_211_1, all_211_2 gives: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (327) aNaturalNumber0(all_156_0) = all_211_1 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xn) = all_211_0 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = all_211_2 & ( ~ (all_211_1 = % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | 0) | ~ (all_211_2 = 0) | all_211_0 = 0) % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (327) implies: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (328) aNaturalNumber0(all_156_0) = all_211_1 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (321) with fresh symbols all_213_0, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | all_213_1, all_213_2 gives: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (329) sdtasdt0(all_156_0, xl) = all_213_0 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_156_0) = all_213_1 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = all_213_2 & $i(all_213_0) & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | ( ~ (all_213_1 = 0) | ~ (all_213_2 = 0) | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | all_213_0 = xn) % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (329) implies: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (330) aNaturalNumber0(all_156_0) = all_213_1 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (331) sdtasdt0(all_156_0, xl) = all_213_0 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (319) with fresh symbols all_215_0, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | all_215_1, all_215_2, all_215_3, all_215_4, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | all_215_5, all_215_6, all_215_7, all_215_8 gives: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (332) sdtasdt0(all_215_5, xl) = all_215_3 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(all_156_0, xl) = all_215_1 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(all_35_3, xl) = all_215_2 & sdtasdt0(xl, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | all_215_5) = all_215_4 & sdtpldt0(all_215_2, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | all_215_1) = all_215_0 & sdtpldt0(all_35_3, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | all_156_0) = all_215_5 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_156_0) = all_215_6 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_3) = all_215_7 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = all_215_8 & $i(all_215_0) & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | $i(all_215_1) & $i(all_215_2) & $i(all_215_3) & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | $i(all_215_4) & $i(all_215_5) & ( ~ (all_215_6 = % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | 0) | ~ (all_215_7 = 0) | ~ (all_215_8 = 0) | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (all_215_0 = all_215_3 & all_215_4 = all_33_0)) % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (332) implies: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (333) aNaturalNumber0(all_35_3) = all_215_7 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (334) aNaturalNumber0(all_156_0) = all_215_6 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (335) sdtpldt0(all_35_3, all_156_0) = all_215_5 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (336) sdtasdt0(all_156_0, xl) = all_215_1 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (318) with fresh symbols all_217_0, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | all_217_1, all_217_2, all_217_3, all_217_4, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | all_217_5, all_217_6, all_217_7, all_217_8 gives: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (337) sdtasdt0(all_217_5, xl) = all_217_3 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(all_156_0, xl) = all_217_2 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(all_35_3, xl) = all_217_1 & sdtasdt0(xl, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | all_217_5) = all_217_4 & sdtpldt0(all_217_2, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | all_217_1) = all_217_0 & sdtpldt0(all_156_0, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | all_35_3) = all_217_5 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_156_0) = all_217_7 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_3) = all_217_6 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = all_217_8 & $i(all_217_0) & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | $i(all_217_1) & $i(all_217_2) & $i(all_217_3) & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | $i(all_217_4) & $i(all_217_5) & ( ~ (all_217_6 = % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | 0) | ~ (all_217_7 = 0) | ~ (all_217_8 = 0) | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (all_217_0 = all_217_3 & all_217_4 = all_33_0)) % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (337) implies: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (338) aNaturalNumber0(all_35_3) = all_217_6 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (339) aNaturalNumber0(all_156_0) = all_217_7 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (340) sdtpldt0(all_156_0, all_35_3) = all_217_5 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | (341) sdtasdt0(all_156_0, xl) = all_217_2 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (323) gives: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (342) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (sdtlseqdt0(all_35_3, all_35_1) = v2 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_1) = v1 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_3) = v0 & ( ~ (v2 = 0) | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0))) % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (342) with fresh symbols all_222_0, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | all_222_1, all_222_2 gives: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (343) sdtlseqdt0(all_35_3, all_35_1) = all_222_0 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_1) = all_222_1 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_3) = all_222_2 & ( ~ % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (all_222_0 = 0) | ~ (all_222_1 = 0) | ~ % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (all_222_2 = 0)) % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (343) implies: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (344) aNaturalNumber0(all_35_3) = all_222_2 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (345) aNaturalNumber0(all_35_1) = all_222_1 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (346) sdtlseqdt0(all_35_3, all_35_1) = all_222_0 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (347) ~ (all_222_0 = 0) | ~ (all_222_1 = 0) | ~ % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (all_222_2 = 0) % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_222_2, all_35_3, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (313), (344) gives: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (348) all_222_2 = 0 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_217_6, all_222_2, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | all_35_3, simplifying with (338), (344) gives: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (349) all_222_2 = all_217_6 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_215_7, all_222_2, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | all_35_3, simplifying with (333), (344) gives: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (350) all_222_2 = all_215_7 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_222_1, all_35_1, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (309), (345) gives: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (351) all_222_1 = 0 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (16) with 0, all_222_0, all_35_1, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | all_35_3, simplifying with (262), (346) gives: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (352) all_222_0 = 0 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (349), (350) imply: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (353) all_217_6 = all_215_7 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (348), (349) imply: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (354) all_217_6 = 0 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (353), (354) imply: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (355) all_215_7 = 0 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (347) gives: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | (356) ~ (all_222_0 = 0) % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (352), (356) imply: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | (357) $false % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (357) is inconsistent. % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | (358) ~ (all_222_1 = 0) | ~ (all_222_2 = 0) % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (358) gives: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | | (359) ~ (all_222_1 = 0) % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (351), (359) imply: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | | (360) $false % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (360) is inconsistent. % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | | (361) ~ (all_222_2 = 0) % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (348), (361) imply: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | | (362) $false % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (362) is inconsistent. % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | End of split % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (363) ! [v0: any] : (v0 = all_156_0 | ~ % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (sdtpldt0(all_35_3, v0) = all_35_1) | ~ $i(v0) % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | | ? [v1: int] : ( ~ (v1 = 0) & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( ~ % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (sdtpldt0(all_35_3, all_156_0) = v0) | ~ % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | $i(all_156_0) | (v0 = all_35_1 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_156_0) = 0)) % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (363) implies: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (364) ! [v0: $i] : ( ~ (sdtpldt0(all_35_3, all_156_0) = % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | v0) | ~ $i(all_156_0) | (v0 = all_35_1 & % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_156_0) = 0)) % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_213_1, all_215_6, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | all_156_0, simplifying with (330), (334) gives: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (365) all_215_6 = all_213_1 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_211_1, all_215_6, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | all_156_0, simplifying with (328), (334) gives: % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | (366) all_215_6 = all_211_1 % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_215_6, all_217_7, % 21.83/4.02 | | | | | | | | | | | | | | | | | | | | | | | | all_156_0, simplifying with (334), (339) gives: % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | (367) all_217_7 = all_215_6 % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_209_0, all_217_7, % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | all_156_0, simplifying with (326), (339) gives: % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | (368) all_217_7 = all_209_0 % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (15) with all_215_1, all_217_2, xl, % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | all_156_0, simplifying with (336), (341) gives: % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | (369) all_217_2 = all_215_1 % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (15) with all_213_0, all_217_2, xl, % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | all_156_0, simplifying with (331), (341) gives: % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | (370) all_217_2 = all_213_0 % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (369), (370) imply: % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | (371) all_215_1 = all_213_0 % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (371) implies: % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | (372) all_215_1 = all_213_0 % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (367), (368) imply: % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | (373) all_215_6 = all_209_0 % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (373) implies: % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | (374) all_215_6 = all_209_0 % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (365), (366) imply: % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | (375) all_213_1 = all_211_1 % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (365), (374) imply: % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | (376) all_213_1 = all_209_0 % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (375), (376) imply: % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | (377) all_211_1 = all_209_0 % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (364) with all_215_5, simplifying % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | with (260), (335) gives: % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | (378) all_215_5 = all_35_1 & aNaturalNumber0(all_156_0) % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | = 0 % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (378) implies: % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | (379) aNaturalNumber0(all_156_0) = 0 % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mSortsB) with all_35_3, all_156_0, % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | all_215_5, simplifying with (260), (314), (335) % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | gives: % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | (380) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | (aNaturalNumber0(all_215_5) = v2 & % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_156_0) = v1 & % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_3) = v0 & ( ~ (v1 = 0) | % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | ~ (v0 = 0) | v2 = 0)) % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mSortsB) with all_156_0, all_35_3, % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | all_217_5, simplifying with (260), (314), (340) % 21.83/4.03 | | | | | | | | | | | | | | | | | | | | | | | | gives: % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (381) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (aNaturalNumber0(all_217_5) = v2 & % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_156_0) = v0 & % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_3) = v1 & ( ~ (v1 = 0) | % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | ~ (v0 = 0) | v2 = 0)) % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mSortsB_02) with all_156_0, xl, % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | all_213_0, simplifying with (9), (260), (331) % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | gives: % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (382) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (aNaturalNumber0(all_213_0) = v2 & % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_156_0) = v0 & % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v1 & ( ~ (v1 = 0) | ~ (v0 % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | = 0) | v2 = 0)) % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (381) with fresh symbols all_243_0, % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | all_243_1, all_243_2 gives: % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (383) aNaturalNumber0(all_217_5) = all_243_0 & % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_156_0) = all_243_2 & % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_3) = all_243_1 & ( ~ % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (all_243_1 = 0) | ~ (all_243_2 = 0) | all_243_0 % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | = 0) % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (383) implies: % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (384) aNaturalNumber0(all_156_0) = all_243_2 % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (380) with fresh symbols all_245_0, % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | all_245_1, all_245_2 gives: % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (385) aNaturalNumber0(all_215_5) = all_245_0 & % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_156_0) = all_245_1 & % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_3) = all_245_2 & ( ~ % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (all_245_1 = 0) | ~ (all_245_2 = 0) | all_245_0 % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | = 0) % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (385) implies: % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (386) aNaturalNumber0(all_156_0) = all_245_1 % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (382) with fresh symbols all_247_0, % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | all_247_1, all_247_2 gives: % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (387) aNaturalNumber0(all_213_0) = all_247_0 & % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_156_0) = all_247_2 & % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = all_247_1 & ( ~ (all_247_1 = % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | 0) | ~ (all_247_2 = 0) | all_247_0 = 0) % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (387) implies: % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (388) aNaturalNumber0(all_156_0) = all_247_2 % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_245_1, all_156_0, % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (379), (386) gives: % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (389) all_245_1 = 0 % 21.83/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_209_0, all_247_2, % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | all_156_0, simplifying with (326), (388) gives: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (390) all_247_2 = all_209_0 % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_245_1, all_247_2, % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | all_156_0, simplifying with (386), (388) gives: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (391) all_247_2 = all_245_1 % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_243_2, all_247_2, % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | all_156_0, simplifying with (384), (388) gives: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (392) all_247_2 = all_243_2 % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (391), (392) imply: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (393) all_245_1 = all_243_2 % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (393) implies: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (394) all_245_1 = all_243_2 % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (390), (392) imply: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (395) all_243_2 = all_209_0 % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (389), (394) imply: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (396) all_243_2 = 0 % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (396) implies: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (397) all_243_2 = 0 % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (395), (397) imply: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (398) all_209_0 = 0 % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (325), (398) imply: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | (399) $false % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (399) is inconsistent. % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | End of split % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | Case 2: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | (400) ? [v0: int] : ( ~ (v0 = 0) & % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_79_0) = v0) % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (400) with fresh symbol all_182_0 % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | gives: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | (401) ~ (all_182_0 = 0) & aNaturalNumber0(all_79_0) = % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | all_182_0 % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (401) implies: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | (402) ~ (all_182_0 = 0) % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | (403) aNaturalNumber0(all_79_0) = all_182_0 % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_182_0, all_79_0, % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | simplifying with (110), (403) gives: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | (404) all_182_0 = 0 % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (402), (404) imply: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | (405) $false % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (405) is inconsistent. % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | End of split % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | Case 2: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | (406) ? [v0: int] : ( ~ (v0 = 0) & % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_104_0) = v0) % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (406) with fresh symbol all_178_0 % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | gives: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | (407) ~ (all_178_0 = 0) & aNaturalNumber0(all_104_0) = % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | all_178_0 % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | ALPHA: (407) implies: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | (408) ~ (all_178_0 = 0) % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | (409) aNaturalNumber0(all_104_0) = all_178_0 % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_178_0, all_104_0, % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | simplifying with (153), (409) gives: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | (410) all_178_0 = 0 % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (408), (410) imply: % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | (411) $false % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | CLOSE: (411) is inconsistent. % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | End of split % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | End of split % 22.18/4.04 | | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | | End of split % 22.18/4.04 | | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | | End of split % 22.18/4.04 | | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | | End of split % 22.18/4.04 | | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | | End of split % 22.18/4.04 | | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | | End of split % 22.18/4.04 | | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | | End of split % 22.18/4.04 | | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | | End of split % 22.18/4.04 | | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | | End of split % 22.18/4.04 | | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | | End of split % 22.18/4.04 | | | | | | | | | | | % 22.18/4.04 | | | | | | | | | | End of split % 22.18/4.04 | | | | | | | | | | % 22.18/4.04 | | | | | | | | | End of split % 22.18/4.04 | | | | | | | | | % 22.18/4.04 | | | | | | | | End of split % 22.18/4.04 | | | | | | | | % 22.18/4.04 | | | | | | | End of split % 22.18/4.04 | | | | | | | % 22.18/4.04 | | | | | | End of split % 22.18/4.04 | | | | | | % 22.18/4.04 | | | | | End of split % 22.18/4.04 | | | | | % 22.18/4.04 | | | | End of split % 22.18/4.04 | | | | % 22.18/4.04 | | | Case 2: % 22.18/4.04 | | | | % 22.18/4.04 | | | | (412) ~ (all_58_1 = 0) | ~ (all_58_2 = 0) | ~ (all_58_3 = 0) % 22.18/4.04 | | | | % 22.18/4.04 | | | | BETA: splitting (412) gives: % 22.18/4.04 | | | | % 22.18/4.04 | | | | Case 1: % 22.18/4.04 | | | | | % 22.18/4.04 | | | | | (413) ~ (all_58_1 = 0) % 22.18/4.04 | | | | | % 22.18/4.04 | | | | | REDUCE: (91), (413) imply: % 22.18/4.04 | | | | | (414) $false % 22.18/4.04 | | | | | % 22.18/4.04 | | | | | CLOSE: (414) is inconsistent. % 22.18/4.04 | | | | | % 22.18/4.04 | | | | Case 2: % 22.18/4.04 | | | | | % 22.18/4.04 | | | | | (415) ~ (all_58_2 = 0) | ~ (all_58_3 = 0) % 22.18/4.04 | | | | | % 22.18/4.04 | | | | | BETA: splitting (415) gives: % 22.18/4.04 | | | | | % 22.18/4.04 | | | | | Case 1: % 22.18/4.04 | | | | | | % 22.18/4.04 | | | | | | (416) ~ (all_58_2 = 0) % 22.18/4.04 | | | | | | % 22.18/4.04 | | | | | | REDUCE: (73), (416) imply: % 22.18/4.04 | | | | | | (417) $false % 22.18/4.04 | | | | | | % 22.18/4.04 | | | | | | CLOSE: (417) is inconsistent. % 22.18/4.04 | | | | | | % 22.18/4.04 | | | | | Case 2: % 22.18/4.04 | | | | | | % 22.18/4.04 | | | | | | (418) ~ (all_58_3 = 0) % 22.18/4.04 | | | | | | % 22.18/4.04 | | | | | | REDUCE: (82), (418) imply: % 22.18/4.04 | | | | | | (419) $false % 22.18/4.04 | | | | | | % 22.18/4.04 | | | | | | CLOSE: (419) is inconsistent. % 22.18/4.04 | | | | | | % 22.18/4.04 | | | | | End of split % 22.18/4.04 | | | | | % 22.18/4.04 | | | | End of split % 22.18/4.04 | | | | % 22.18/4.04 | | | End of split % 22.18/4.04 | | | % 22.18/4.04 | | End of split % 22.18/4.04 | | % 22.18/4.04 | End of split % 22.18/4.04 | % 22.18/4.04 End of proof % 22.18/4.04 % SZS output end Proof for theBenchmark % 22.18/4.04 % 22.18/4.04 3450ms %------------------------------------------------------------------------------