%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : NUM473+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 : n023.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:47:59 EDT 2023 % Result : Theorem 11.66s 2.29s % Output : Proof 19.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : NUM473+1 : TPTP v8.1.2. Released v4.0.0. % 0.11/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.31 % Computer : n023.cluster.edu % 0.12/0.31 % Model : x86_64 x86_64 % 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.31 % Memory : 8042.1875MB % 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.31 % CPULimit : 300 % 0.12/0.31 % WCLimit : 300 % 0.12/0.31 % DateTime : Fri Aug 25 08:03:27 EDT 2023 % 0.12/0.32 % CPUTime : % 0.17/0.57 ________ _____ % 0.17/0.57 ___ __ \_________(_)________________________________ % 0.17/0.57 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.17/0.57 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.17/0.57 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.17/0.57 % 0.17/0.57 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.17/0.57 (2023-06-19) % 0.17/0.57 % 0.17/0.57 (c) Philipp Rümmer, 2009-2023 % 0.17/0.57 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.17/0.57 Amanda Stjerna. % 0.17/0.57 Free software under BSD-3-Clause. % 0.17/0.57 % 0.17/0.57 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.17/0.57 % 0.17/0.57 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.63/0.59 Running up to 7 provers in parallel. % 0.70/0.61 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.70/0.61 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.70/0.61 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.70/0.61 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.70/0.61 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.70/0.61 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.70/0.61 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 2.86/1.13 Prover 4: Preprocessing ... % 2.86/1.13 Prover 1: Preprocessing ... % 2.86/1.17 Prover 2: Preprocessing ... % 2.86/1.17 Prover 6: Preprocessing ... % 2.86/1.17 Prover 0: Preprocessing ... % 2.86/1.17 Prover 5: Preprocessing ... % 2.86/1.17 Prover 3: Preprocessing ... % 7.37/1.74 Prover 1: Constructing countermodel ... % 7.37/1.76 Prover 3: Constructing countermodel ... % 8.23/1.83 Prover 6: Proving ... % 8.90/1.94 Prover 5: Constructing countermodel ... % 9.52/2.07 Prover 2: Proving ... % 10.55/2.17 Prover 4: Constructing countermodel ... % 11.15/2.28 Prover 0: Proving ... % 11.15/2.28 Prover 3: proved (1684ms) % 11.15/2.28 % 11.66/2.29 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.66/2.29 % 11.66/2.29 Prover 5: stopped % 11.66/2.29 Prover 6: stopped % 11.66/2.29 Prover 2: stopped % 11.66/2.29 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 11.66/2.29 Prover 0: stopped % 11.66/2.31 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 11.66/2.31 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 11.66/2.31 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 11.66/2.31 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 12.62/2.42 Prover 10: Preprocessing ... % 12.62/2.43 Prover 7: Preprocessing ... % 12.62/2.43 Prover 8: Preprocessing ... % 12.62/2.44 Prover 11: Preprocessing ... % 12.62/2.46 Prover 13: Preprocessing ... % 13.33/2.56 Prover 10: Constructing countermodel ... % 13.90/2.62 Prover 7: Constructing countermodel ... % 13.90/2.62 Prover 8: Warning: ignoring some quantifiers % 13.90/2.64 Prover 8: Constructing countermodel ... % 13.90/2.67 Prover 13: Constructing countermodel ... % 16.32/2.94 Prover 11: Constructing countermodel ... % 18.01/3.17 Prover 1: Found proof (size 347) % 18.01/3.17 Prover 1: proved (2577ms) % 18.01/3.17 Prover 11: stopped % 18.01/3.17 Prover 13: stopped % 18.01/3.17 Prover 7: stopped % 18.01/3.17 Prover 10: stopped % 18.01/3.17 Prover 4: stopped % 18.01/3.17 Prover 8: stopped % 18.01/3.17 % 18.01/3.17 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.01/3.17 % 18.01/3.19 % SZS output start Proof for theBenchmark % 18.01/3.20 Assumptions after simplification: % 18.01/3.20 --------------------------------- % 18.01/3.20 % 18.01/3.20 (mAddComm) % 18.64/3.22 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 18.64/3.22 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 18.64/3.22 (sdtpldt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 % 18.64/3.22 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 18.64/3.22 % 18.64/3.22 (mDefDiv) % 18.64/3.23 ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (doDivides0(v0, v1) = v2) | ~ % 18.64/3.23 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : (aNaturalNumber0(v1) = v4 % 18.64/3.23 & aNaturalNumber0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0))) | (( ~ (v2 = 0) % 18.64/3.23 | ? [v3: $i] : (sdtasdt0(v0, v3) = v1 & aNaturalNumber0(v3) = 0 & % 18.64/3.23 $i(v3))) & (v2 = 0 | ! [v3: $i] : ( ~ (sdtasdt0(v0, v3) = v1) | ~ % 18.64/3.23 $i(v3) | ? [v4: int] : ( ~ (v4 = 0) & aNaturalNumber0(v3) = v4))))) % 18.64/3.23 % 18.64/3.23 (mDefLE) % 18.64/3.23 ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (sdtlseqdt0(v0, v1) = v2) | ~ % 18.64/3.23 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : (aNaturalNumber0(v1) = v4 % 18.64/3.23 & aNaturalNumber0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0))) | (( ~ (v2 = 0) % 18.64/3.23 | ? [v3: $i] : (sdtpldt0(v0, v3) = v1 & aNaturalNumber0(v3) = 0 & % 18.64/3.23 $i(v3))) & (v2 = 0 | ! [v3: $i] : ( ~ (sdtpldt0(v0, v3) = v1) | ~ % 18.64/3.23 $i(v3) | ? [v4: int] : ( ~ (v4 = 0) & aNaturalNumber0(v3) = v4))))) % 18.64/3.23 % 18.64/3.23 (mDefQuot) % 18.64/3.23 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v0 = sz00 | ~ % 18.64/3.23 (sdtsldt0(v1, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: % 18.64/3.23 any] : ? [v5: any] : (doDivides0(v0, v1) = v5 & aNaturalNumber0(v1) = v4 % 18.64/3.23 & aNaturalNumber0(v0) = v3 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0))) | % 18.64/3.23 ( ! [v3: $i] : (v3 = v2 | ~ (sdtasdt0(v0, v3) = v1) | ~ $i(v3) | ? [v4: % 18.64/3.23 int] : ( ~ (v4 = 0) & aNaturalNumber0(v3) = v4)) & ! [v3: $i] : ( ~ % 18.64/3.23 (sdtasdt0(v0, v2) = v3) | ~ $i(v2) | (v3 = v1 & aNaturalNumber0(v2) = % 18.64/3.23 0)))) % 18.64/3.23 % 18.64/3.23 (mLEAsym) % 18.64/3.23 ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (sdtlseqdt0(v0, v1) = 0) | ~ $i(v1) % 18.64/3.23 | ~ $i(v0) | ? [v2: any] : ? [v3: any] : ? [v4: any] : (sdtlseqdt0(v1, % 18.64/3.23 v0) = v4 & aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v4 % 18.64/3.23 = 0) | ~ (v3 = 0) | ~ (v2 = 0)))) % 18.64/3.23 % 18.64/3.23 (mLETotal) % 18.64/3.24 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (sdtlseqdt0(v0, v1) = % 18.64/3.24 v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 18.64/3.24 (sdtlseqdt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = % 18.64/3.24 v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | (v5 = 0 & ~ (v1 = v0))))) % 18.64/3.24 % 18.64/3.24 (mMonMul) % 18.64/3.24 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 18.64/3.24 : ! [v5: any] : (v2 = v1 | v0 = sz00 | ~ (sdtlseqdt0(v3, v4) = v5) | ~ % 18.64/3.24 (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) % 18.64/3.24 | ~ $i(v0) | ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: any] : ? % 18.64/3.24 [v10: $i] : ? [v11: $i] : ? [v12: any] : (sdtlseqdt0(v10, v11) = v12 & % 18.64/3.24 sdtlseqdt0(v1, v2) = v9 & sdtasdt0(v2, v0) = v11 & sdtasdt0(v1, v0) = v10 % 18.64/3.24 & aNaturalNumber0(v2) = v8 & aNaturalNumber0(v1) = v7 & % 18.64/3.24 aNaturalNumber0(v0) = v6 & $i(v11) & $i(v10) & ( ~ (v9 = 0) | ~ (v8 = 0) % 18.64/3.24 | ~ (v7 = 0) | ~ (v6 = 0) | (v12 = 0 & v5 = 0 & ~ (v11 = v10) & ~ % 18.64/3.24 (v4 = v3))))) % 18.64/3.24 % 18.64/3.24 (mMulCanc) % 18.64/3.24 $i(sz00) & ! [v0: $i] : (v0 = sz00 | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) % 18.64/3.24 | ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v2 = v1 | ~ % 18.64/3.24 (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | ~ % 18.64/3.24 $i(v1) | ? [v5: any] : ? [v6: any] : ? [v7: $i] : ? [v8: $i] : % 18.64/3.24 (sdtasdt0(v2, v0) = v8 & sdtasdt0(v1, v0) = v7 & aNaturalNumber0(v2) = v6 % 18.64/3.24 & aNaturalNumber0(v1) = v5 & $i(v8) & $i(v7) & ( ~ (v6 = 0) | ~ (v5 = % 18.64/3.24 0) | ( ~ (v8 = v7) & ~ (v4 = v3)))))) % 18.64/3.24 % 18.64/3.24 (mMulComm) % 18.64/3.24 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 18.64/3.24 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 18.64/3.24 (sdtasdt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 % 18.64/3.24 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 18.64/3.24 % 18.64/3.24 (mSortsB) % 18.64/3.24 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 18.64/3.24 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 18.64/3.24 (aNaturalNumber0(v2) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = % 18.64/3.24 v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 18.64/3.24 % 18.64/3.24 (m__) % 18.64/3.24 $i(xq) & $i(xp) & ? [v0: int] : ( ~ (v0 = 0) & sdtlseqdt0(xp, xq) = v0) % 18.64/3.24 % 18.64/3.24 (m__1324) % 18.64/3.24 aNaturalNumber0(xn) = 0 & aNaturalNumber0(xm) = 0 & aNaturalNumber0(xl) = 0 & % 18.64/3.24 $i(xn) & $i(xm) & $i(xl) % 18.64/3.24 % 18.64/3.24 (m__1324_04) % 18.64/3.24 $i(xn) & $i(xm) & $i(xl) & ? [v0: $i] : (doDivides0(xl, v0) = 0 & % 18.64/3.24 doDivides0(xl, xm) = 0 & sdtpldt0(xm, xn) = v0 & $i(v0)) % 18.64/3.24 % 18.64/3.24 (m__1347) % 18.64/3.25 ~ (xl = sz00) & $i(xl) & $i(sz00) % 18.64/3.25 % 18.64/3.25 (m__1360) % 18.64/3.25 sdtsldt0(xm, xl) = xp & $i(xp) & $i(xm) & $i(xl) % 18.64/3.25 % 18.64/3.25 (m__1379) % 18.64/3.25 $i(xq) & $i(xn) & $i(xm) & $i(xl) & ? [v0: $i] : (sdtsldt0(v0, xl) = xq & % 18.64/3.25 sdtpldt0(xm, xn) = v0 & $i(v0)) % 18.64/3.25 % 18.64/3.25 (m__1409) % 18.64/3.25 $i(xn) & $i(xm) & ? [v0: $i] : (sdtlseqdt0(xm, v0) = 0 & sdtpldt0(xm, xn) = % 18.64/3.25 v0 & $i(v0)) % 18.64/3.25 % 18.64/3.25 (function-axioms) % 18.64/3.25 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 18.64/3.25 (sdtsldt0(v3, v2) = v1) | ~ (sdtsldt0(v3, v2) = v0)) & ! [v0: % 18.64/3.25 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 18.64/3.25 : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ (doDivides0(v3, v2) = v0)) & ! % 18.64/3.25 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 18.64/3.25 $i] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) & ! % 18.64/3.25 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 18.64/3.25 (sdtmndt0(v3, v2) = v1) | ~ (sdtmndt0(v3, v2) = v0)) & ! [v0: % 18.64/3.25 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 18.64/3.25 : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ (sdtlseqdt0(v3, v2) = v0)) & ! % 18.64/3.25 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 18.64/3.25 (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 18.64/3.25 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | % 18.64/3.25 ~ (sdtpldt0(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 18.64/3.25 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) % 18.64/3.25 | ~ (aNaturalNumber0(v2) = v0)) % 18.64/3.25 % 18.64/3.25 Further assumptions not needed in the proof: % 18.64/3.25 -------------------------------------------- % 18.64/3.25 mAMDistr, mAddAsso, mAddCanc, mDefDiff, mDivSum, mDivTrans, mIH, mIH_03, mLENTr, % 18.64/3.25 mLERefl, mLETran, mMonAdd, mMonMul2, mMulAsso, mNatSort, mSortsB_02, mSortsC, % 18.64/3.25 mSortsC_01, mZeroAdd, mZeroMul, m_AddZero, m_MulUnit, m_MulZero % 18.64/3.25 % 18.64/3.25 Those formulas are unsatisfiable: % 18.64/3.25 --------------------------------- % 18.64/3.25 % 18.64/3.25 Begin of proof % 18.64/3.25 | % 18.64/3.25 | ALPHA: (mMulCanc) implies: % 18.64/3.25 | (1) ! [v0: $i] : (v0 = sz00 | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) | % 18.64/3.25 | ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v2 = v1 | ~ % 18.64/3.25 | (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | % 18.64/3.25 | ~ $i(v1) | ? [v5: any] : ? [v6: any] : ? [v7: $i] : ? [v8: $i] % 18.64/3.25 | : (sdtasdt0(v2, v0) = v8 & sdtasdt0(v1, v0) = v7 & % 18.64/3.25 | aNaturalNumber0(v2) = v6 & aNaturalNumber0(v1) = v5 & $i(v8) & % 18.64/3.25 | $i(v7) & ( ~ (v6 = 0) | ~ (v5 = 0) | ( ~ (v8 = v7) & ~ (v4 = % 18.64/3.25 | v3)))))) % 18.64/3.25 | % 18.64/3.25 | ALPHA: (mMonMul) implies: % 18.64/3.26 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 18.64/3.26 | ! [v5: any] : (v2 = v1 | v0 = sz00 | ~ (sdtlseqdt0(v3, v4) = v5) | ~ % 18.64/3.26 | (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | ~ % 18.64/3.26 | $i(v1) | ~ $i(v0) | ? [v6: any] : ? [v7: any] : ? [v8: any] : ? % 18.64/3.26 | [v9: any] : ? [v10: $i] : ? [v11: $i] : ? [v12: any] : % 18.64/3.26 | (sdtlseqdt0(v10, v11) = v12 & sdtlseqdt0(v1, v2) = v9 & sdtasdt0(v2, % 18.64/3.26 | v0) = v11 & sdtasdt0(v1, v0) = v10 & aNaturalNumber0(v2) = v8 & % 18.64/3.26 | aNaturalNumber0(v1) = v7 & aNaturalNumber0(v0) = v6 & $i(v11) & % 18.64/3.26 | $i(v10) & ( ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | % 18.64/3.26 | (v12 = 0 & v5 = 0 & ~ (v11 = v10) & ~ (v4 = v3))))) % 18.64/3.26 | % 18.64/3.26 | ALPHA: (mDefQuot) implies: % 18.64/3.26 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v0 = sz00 | ~ (sdtsldt0(v1, % 18.64/3.26 | v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : % 18.64/3.26 | ? [v5: any] : (doDivides0(v0, v1) = v5 & aNaturalNumber0(v1) = v4 & % 18.64/3.26 | aNaturalNumber0(v0) = v3 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = % 18.64/3.26 | 0))) | ( ! [v3: $i] : (v3 = v2 | ~ (sdtasdt0(v0, v3) = v1) | % 18.64/3.26 | ~ $i(v3) | ? [v4: int] : ( ~ (v4 = 0) & aNaturalNumber0(v3) = % 18.64/3.26 | v4)) & ! [v3: $i] : ( ~ (sdtasdt0(v0, v2) = v3) | ~ $i(v2) | % 18.64/3.26 | (v3 = v1 & aNaturalNumber0(v2) = 0)))) % 18.64/3.26 | % 18.64/3.26 | ALPHA: (m__1324) implies: % 18.64/3.26 | (4) aNaturalNumber0(xl) = 0 % 18.64/3.26 | (5) aNaturalNumber0(xm) = 0 % 18.64/3.26 | (6) aNaturalNumber0(xn) = 0 % 18.64/3.26 | % 18.64/3.26 | ALPHA: (m__1324_04) implies: % 18.64/3.26 | (7) ? [v0: $i] : (doDivides0(xl, v0) = 0 & doDivides0(xl, xm) = 0 & % 18.64/3.26 | sdtpldt0(xm, xn) = v0 & $i(v0)) % 18.64/3.26 | % 18.64/3.26 | ALPHA: (m__1347) implies: % 18.64/3.26 | (8) ~ (xl = sz00) % 18.64/3.26 | % 18.64/3.26 | ALPHA: (m__1360) implies: % 18.64/3.26 | (9) sdtsldt0(xm, xl) = xp % 18.64/3.26 | % 18.64/3.26 | ALPHA: (m__1379) implies: % 18.64/3.26 | (10) $i(xl) % 18.64/3.26 | (11) ? [v0: $i] : (sdtsldt0(v0, xl) = xq & sdtpldt0(xm, xn) = v0 & $i(v0)) % 18.64/3.26 | % 18.64/3.26 | ALPHA: (m__1409) implies: % 18.64/3.26 | (12) $i(xm) % 18.64/3.26 | (13) $i(xn) % 18.64/3.26 | (14) ? [v0: $i] : (sdtlseqdt0(xm, v0) = 0 & sdtpldt0(xm, xn) = v0 & % 18.64/3.26 | $i(v0)) % 18.64/3.26 | % 18.64/3.26 | ALPHA: (m__) implies: % 18.64/3.26 | (15) $i(xp) % 18.64/3.26 | (16) $i(xq) % 18.64/3.26 | (17) ? [v0: int] : ( ~ (v0 = 0) & sdtlseqdt0(xp, xq) = v0) % 18.64/3.26 | % 18.64/3.26 | ALPHA: (function-axioms) implies: % 18.64/3.26 | (18) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 18.64/3.26 | : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = % 18.64/3.26 | v0)) % 18.64/3.26 | (19) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 18.64/3.26 | (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 18.64/3.27 | (20) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 18.64/3.27 | (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 18.64/3.27 | (21) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 18.64/3.27 | : ! [v3: $i] : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ % 18.64/3.27 | (sdtlseqdt0(v3, v2) = v0)) % 18.64/3.27 | (22) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 18.64/3.27 | : ! [v3: $i] : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ % 18.64/3.27 | (doDivides0(v3, v2) = v0)) % 18.64/3.27 | % 18.64/3.27 | DELTA: instantiating (17) with fresh symbol all_33_0 gives: % 18.64/3.27 | (23) ~ (all_33_0 = 0) & sdtlseqdt0(xp, xq) = all_33_0 % 18.64/3.27 | % 18.64/3.27 | ALPHA: (23) implies: % 18.64/3.27 | (24) ~ (all_33_0 = 0) % 18.64/3.27 | (25) sdtlseqdt0(xp, xq) = all_33_0 % 18.64/3.27 | % 18.64/3.27 | DELTA: instantiating (11) with fresh symbol all_35_0 gives: % 18.64/3.27 | (26) sdtsldt0(all_35_0, xl) = xq & sdtpldt0(xm, xn) = all_35_0 & % 18.64/3.27 | $i(all_35_0) % 18.64/3.27 | % 18.64/3.27 | ALPHA: (26) implies: % 18.64/3.27 | (27) sdtpldt0(xm, xn) = all_35_0 % 18.64/3.27 | (28) sdtsldt0(all_35_0, xl) = xq % 18.64/3.27 | % 18.64/3.27 | DELTA: instantiating (14) with fresh symbol all_37_0 gives: % 18.64/3.27 | (29) sdtlseqdt0(xm, all_37_0) = 0 & sdtpldt0(xm, xn) = all_37_0 & % 18.64/3.27 | $i(all_37_0) % 18.64/3.27 | % 18.64/3.27 | ALPHA: (29) implies: % 18.64/3.27 | (30) $i(all_37_0) % 18.64/3.27 | (31) sdtpldt0(xm, xn) = all_37_0 % 18.64/3.27 | (32) sdtlseqdt0(xm, all_37_0) = 0 % 18.64/3.27 | % 18.64/3.27 | DELTA: instantiating (7) with fresh symbol all_39_0 gives: % 18.64/3.27 | (33) doDivides0(xl, all_39_0) = 0 & doDivides0(xl, xm) = 0 & sdtpldt0(xm, % 18.64/3.27 | xn) = all_39_0 & $i(all_39_0) % 18.64/3.27 | % 18.64/3.27 | ALPHA: (33) implies: % 18.64/3.27 | (34) sdtpldt0(xm, xn) = all_39_0 % 18.64/3.27 | (35) doDivides0(xl, xm) = 0 % 18.64/3.27 | (36) doDivides0(xl, all_39_0) = 0 % 18.64/3.27 | % 18.64/3.27 | GROUND_INST: instantiating (19) with all_37_0, all_39_0, xn, xm, simplifying % 18.64/3.27 | with (31), (34) gives: % 18.64/3.27 | (37) all_39_0 = all_37_0 % 18.64/3.27 | % 18.64/3.27 | GROUND_INST: instantiating (19) with all_35_0, all_39_0, xn, xm, simplifying % 18.64/3.27 | with (27), (34) gives: % 18.64/3.27 | (38) all_39_0 = all_35_0 % 18.64/3.27 | % 18.64/3.27 | COMBINE_EQS: (37), (38) imply: % 18.64/3.27 | (39) all_37_0 = all_35_0 % 18.64/3.27 | % 18.64/3.27 | SIMP: (39) implies: % 18.64/3.27 | (40) all_37_0 = all_35_0 % 18.64/3.27 | % 18.64/3.27 | REDUCE: (36), (38) imply: % 18.64/3.27 | (41) doDivides0(xl, all_35_0) = 0 % 18.64/3.27 | % 18.64/3.27 | REDUCE: (32), (40) imply: % 18.64/3.27 | (42) sdtlseqdt0(xm, all_35_0) = 0 % 18.64/3.27 | % 18.64/3.27 | REDUCE: (30), (40) imply: % 18.64/3.27 | (43) $i(all_35_0) % 18.64/3.27 | % 18.64/3.27 | GROUND_INST: instantiating (1) with xl, simplifying with (4), (10) gives: % 18.64/3.28 | (44) xl = sz00 | ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 18.64/3.28 | (v1 = v0 | ~ (sdtasdt0(xl, v1) = v3) | ~ (sdtasdt0(xl, v0) = v2) | % 18.64/3.28 | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: $i] : % 18.64/3.28 | ? [v7: $i] : (sdtasdt0(v1, xl) = v7 & sdtasdt0(v0, xl) = v6 & % 18.64/3.28 | aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & $i(v7) & % 18.64/3.28 | $i(v6) & ( ~ (v5 = 0) | ~ (v4 = 0) | ( ~ (v7 = v6) & ~ (v3 = % 18.64/3.28 | v2))))) % 18.64/3.28 | % 18.64/3.28 | GROUND_INST: instantiating (mAddComm) with xm, xn, all_35_0, simplifying with % 18.64/3.28 | (12), (13), (27) gives: % 18.64/3.28 | (45) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xn, xm) = v2 & % 18.64/3.28 | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xm) = v0 & $i(v2) & ( ~ % 18.64/3.28 | (v1 = 0) | ~ (v0 = 0) | v2 = all_35_0)) % 18.64/3.28 | % 18.64/3.28 | GROUND_INST: instantiating (mSortsB) with xm, xn, all_35_0, simplifying with % 18.64/3.28 | (12), (13), (27) gives: % 18.64/3.28 | (46) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 18.64/3.28 | (aNaturalNumber0(all_35_0) = v2 & aNaturalNumber0(xn) = v1 & % 18.64/3.28 | aNaturalNumber0(xm) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 18.64/3.28 | % 18.64/3.28 | GROUND_INST: instantiating (mLEAsym) with xm, all_35_0, simplifying with (12), % 18.64/3.28 | (42), (43) gives: % 18.64/3.28 | (47) all_35_0 = xm | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 18.64/3.28 | (sdtlseqdt0(all_35_0, xm) = v2 & aNaturalNumber0(all_35_0) = v1 & % 18.64/3.28 | aNaturalNumber0(xm) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = % 18.64/3.28 | 0))) % 18.64/3.28 | % 18.64/3.28 | GROUND_INST: instantiating (mDefLE) with xm, all_35_0, 0, simplifying with % 18.64/3.28 | (12), (42), (43) gives: % 18.64/3.28 | (48) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(all_35_0) = v1 & % 18.64/3.28 | aNaturalNumber0(xm) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) | ? [v0: % 18.64/3.28 | $i] : (sdtpldt0(xm, v0) = all_35_0 & aNaturalNumber0(v0) = 0 & % 18.64/3.28 | $i(v0)) % 18.64/3.28 | % 18.64/3.28 | GROUND_INST: instantiating (mLETotal) with xp, xq, all_33_0, simplifying with % 18.64/3.28 | (15), (16), (25) gives: % 18.64/3.28 | (49) all_33_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 18.64/3.28 | (sdtlseqdt0(xq, xp) = v2 & aNaturalNumber0(xq) = v1 & % 18.64/3.28 | aNaturalNumber0(xp) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v2 = 0 & ~ % 18.64/3.28 | (xq = xp)))) % 18.64/3.28 | % 18.64/3.28 | GROUND_INST: instantiating (mDefDiv) with xl, xm, 0, simplifying with (10), % 18.64/3.28 | (12), (35) gives: % 18.64/3.28 | (50) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(xm) = v1 & % 18.64/3.28 | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) | ? [v0: % 18.64/3.28 | $i] : (sdtasdt0(xl, v0) = xm & aNaturalNumber0(v0) = 0 & $i(v0)) % 18.64/3.28 | % 18.64/3.28 | GROUND_INST: instantiating (mDefDiv) with xl, all_35_0, 0, simplifying with % 18.64/3.28 | (10), (41), (43) gives: % 18.64/3.28 | (51) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(all_35_0) = v1 & % 18.64/3.28 | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) | ? [v0: % 18.64/3.28 | $i] : (sdtasdt0(xl, v0) = all_35_0 & aNaturalNumber0(v0) = 0 & % 18.64/3.28 | $i(v0)) % 18.64/3.28 | % 18.64/3.28 | GROUND_INST: instantiating (3) with xl, xm, xp, simplifying with (9), (10), % 18.64/3.28 | (12) gives: % 18.64/3.29 | (52) xl = sz00 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 18.64/3.29 | (doDivides0(xl, xm) = v2 & aNaturalNumber0(xm) = v1 & % 18.64/3.29 | aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = % 18.64/3.29 | 0))) | ( ! [v0: $i] : (v0 = xp | ~ (sdtasdt0(xl, v0) = xm) | ~ % 18.64/3.29 | $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & aNaturalNumber0(v0) = v1)) % 18.64/3.29 | & ! [v0: $i] : ( ~ (sdtasdt0(xl, xp) = v0) | ~ $i(xp) | (v0 = xm & % 18.64/3.29 | aNaturalNumber0(xp) = 0))) % 18.64/3.29 | % 18.64/3.29 | GROUND_INST: instantiating (3) with xl, all_35_0, xq, simplifying with (10), % 18.64/3.29 | (28), (43) gives: % 18.64/3.29 | (53) xl = sz00 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 18.64/3.29 | (doDivides0(xl, all_35_0) = v2 & aNaturalNumber0(all_35_0) = v1 & % 18.64/3.29 | aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = % 18.64/3.29 | 0))) | ( ! [v0: $i] : (v0 = xq | ~ (sdtasdt0(xl, v0) = % 18.64/3.29 | all_35_0) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 18.64/3.29 | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( ~ (sdtasdt0(xl, xq) % 18.64/3.29 | = v0) | ~ $i(xq) | (v0 = all_35_0 & aNaturalNumber0(xq) = 0))) % 18.64/3.29 | % 18.64/3.29 | DELTA: instantiating (46) with fresh symbols all_50_0, all_50_1, all_50_2 % 18.64/3.29 | gives: % 18.64/3.29 | (54) aNaturalNumber0(all_35_0) = all_50_0 & aNaturalNumber0(xn) = all_50_1 % 18.64/3.29 | & aNaturalNumber0(xm) = all_50_2 & ( ~ (all_50_1 = 0) | ~ (all_50_2 = % 18.64/3.29 | 0) | all_50_0 = 0) % 18.64/3.29 | % 18.64/3.29 | ALPHA: (54) implies: % 18.64/3.29 | (55) aNaturalNumber0(xm) = all_50_2 % 18.64/3.29 | (56) aNaturalNumber0(xn) = all_50_1 % 18.64/3.29 | (57) aNaturalNumber0(all_35_0) = all_50_0 % 18.64/3.29 | (58) ~ (all_50_1 = 0) | ~ (all_50_2 = 0) | all_50_0 = 0 % 18.64/3.29 | % 18.64/3.29 | DELTA: instantiating (45) with fresh symbols all_52_0, all_52_1, all_52_2 % 18.64/3.29 | gives: % 18.64/3.29 | (59) sdtpldt0(xn, xm) = all_52_0 & aNaturalNumber0(xn) = all_52_1 & % 18.64/3.29 | aNaturalNumber0(xm) = all_52_2 & $i(all_52_0) & ( ~ (all_52_1 = 0) | % 18.64/3.29 | ~ (all_52_2 = 0) | all_52_0 = all_35_0) % 18.64/3.29 | % 18.64/3.29 | ALPHA: (59) implies: % 18.64/3.29 | (60) aNaturalNumber0(xm) = all_52_2 % 18.64/3.29 | (61) aNaturalNumber0(xn) = all_52_1 % 18.64/3.29 | % 18.64/3.29 | BETA: splitting (44) gives: % 18.64/3.29 | % 18.64/3.29 | Case 1: % 18.64/3.29 | | % 18.64/3.29 | | (62) xl = sz00 % 18.64/3.29 | | % 18.64/3.29 | | REDUCE: (8), (62) imply: % 18.64/3.29 | | (63) $false % 18.64/3.29 | | % 18.64/3.29 | | CLOSE: (63) is inconsistent. % 18.64/3.29 | | % 18.64/3.29 | Case 2: % 18.64/3.29 | | % 18.64/3.29 | | (64) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 18.64/3.29 | | ~ (sdtasdt0(xl, v1) = v3) | ~ (sdtasdt0(xl, v0) = v2) | ~ $i(v1) % 18.64/3.29 | | | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: $i] : ? [v7: % 18.64/3.29 | | $i] : (sdtasdt0(v1, xl) = v7 & sdtasdt0(v0, xl) = v6 & % 18.64/3.29 | | aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & $i(v7) & % 18.64/3.29 | | $i(v6) & ( ~ (v5 = 0) | ~ (v4 = 0) | ( ~ (v7 = v6) & ~ (v3 = % 18.64/3.29 | | v2))))) % 18.64/3.29 | | % 18.64/3.29 | | BETA: splitting (49) gives: % 18.64/3.29 | | % 18.64/3.29 | | Case 1: % 18.64/3.29 | | | % 18.64/3.29 | | | (65) all_33_0 = 0 % 18.64/3.29 | | | % 18.64/3.29 | | | REDUCE: (24), (65) imply: % 18.64/3.29 | | | (66) $false % 18.64/3.29 | | | % 18.64/3.29 | | | CLOSE: (66) is inconsistent. % 18.64/3.29 | | | % 18.64/3.29 | | Case 2: % 18.64/3.29 | | | % 18.64/3.29 | | | (67) ? [v0: any] : ? [v1: any] : ? [v2: any] : (sdtlseqdt0(xq, xp) = % 18.64/3.29 | | | v2 & aNaturalNumber0(xq) = v1 & aNaturalNumber0(xp) = v0 & ( ~ % 18.64/3.29 | | | (v1 = 0) | ~ (v0 = 0) | (v2 = 0 & ~ (xq = xp)))) % 18.64/3.29 | | | % 18.64/3.29 | | | DELTA: instantiating (67) with fresh symbols all_66_0, all_66_1, all_66_2 % 18.64/3.29 | | | gives: % 18.64/3.30 | | | (68) sdtlseqdt0(xq, xp) = all_66_0 & aNaturalNumber0(xq) = all_66_1 & % 18.64/3.30 | | | aNaturalNumber0(xp) = all_66_2 & ( ~ (all_66_1 = 0) | ~ (all_66_2 % 18.64/3.30 | | | = 0) | (all_66_0 = 0 & ~ (xq = xp))) % 18.64/3.30 | | | % 18.64/3.30 | | | ALPHA: (68) implies: % 18.64/3.30 | | | (69) aNaturalNumber0(xp) = all_66_2 % 18.64/3.30 | | | (70) aNaturalNumber0(xq) = all_66_1 % 19.03/3.30 | | | (71) sdtlseqdt0(xq, xp) = all_66_0 % 19.03/3.30 | | | (72) ~ (all_66_1 = 0) | ~ (all_66_2 = 0) | (all_66_0 = 0 & ~ (xq = % 19.03/3.30 | | | xp)) % 19.03/3.30 | | | % 19.03/3.30 | | | GROUND_INST: instantiating (18) with 0, all_52_2, xm, simplifying with % 19.03/3.30 | | | (5), (60) gives: % 19.03/3.30 | | | (73) all_52_2 = 0 % 19.03/3.30 | | | % 19.03/3.30 | | | GROUND_INST: instantiating (18) with all_50_2, all_52_2, xm, simplifying % 19.03/3.30 | | | with (55), (60) gives: % 19.03/3.30 | | | (74) all_52_2 = all_50_2 % 19.03/3.30 | | | % 19.03/3.30 | | | GROUND_INST: instantiating (18) with 0, all_52_1, xn, simplifying with % 19.03/3.30 | | | (6), (61) gives: % 19.03/3.30 | | | (75) all_52_1 = 0 % 19.03/3.30 | | | % 19.03/3.30 | | | GROUND_INST: instantiating (18) with all_50_1, all_52_1, xn, simplifying % 19.03/3.30 | | | with (56), (61) gives: % 19.03/3.30 | | | (76) all_52_1 = all_50_1 % 19.03/3.30 | | | % 19.03/3.30 | | | COMBINE_EQS: (75), (76) imply: % 19.03/3.30 | | | (77) all_50_1 = 0 % 19.03/3.30 | | | % 19.03/3.30 | | | COMBINE_EQS: (73), (74) imply: % 19.03/3.30 | | | (78) all_50_2 = 0 % 19.03/3.30 | | | % 19.03/3.30 | | | SIMP: (78) implies: % 19.03/3.30 | | | (79) all_50_2 = 0 % 19.03/3.30 | | | % 19.03/3.30 | | | BETA: splitting (52) gives: % 19.03/3.30 | | | % 19.03/3.30 | | | Case 1: % 19.03/3.30 | | | | % 19.03/3.30 | | | | (80) xl = sz00 % 19.03/3.30 | | | | % 19.03/3.30 | | | | REDUCE: (8), (80) imply: % 19.03/3.30 | | | | (81) $false % 19.03/3.30 | | | | % 19.03/3.30 | | | | CLOSE: (81) is inconsistent. % 19.03/3.30 | | | | % 19.03/3.30 | | | Case 2: % 19.03/3.30 | | | | % 19.03/3.30 | | | | (82) ? [v0: any] : ? [v1: any] : ? [v2: any] : (doDivides0(xl, xm) % 19.03/3.30 | | | | = v2 & aNaturalNumber0(xm) = v1 & aNaturalNumber0(xl) = v0 & ( % 19.03/3.30 | | | | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) | ( ! [v0: $i] : % 19.03/3.30 | | | | (v0 = xp | ~ (sdtasdt0(xl, v0) = xm) | ~ $i(v0) | ? [v1: % 19.03/3.30 | | | | int] : ( ~ (v1 = 0) & aNaturalNumber0(v0) = v1)) & ! [v0: % 19.03/3.30 | | | | $i] : ( ~ (sdtasdt0(xl, xp) = v0) | ~ $i(xp) | (v0 = xm & % 19.03/3.30 | | | | aNaturalNumber0(xp) = 0))) % 19.03/3.30 | | | | % 19.03/3.30 | | | | BETA: splitting (58) gives: % 19.03/3.30 | | | | % 19.03/3.30 | | | | Case 1: % 19.03/3.30 | | | | | % 19.03/3.30 | | | | | (83) ~ (all_50_1 = 0) % 19.03/3.30 | | | | | % 19.03/3.30 | | | | | REDUCE: (77), (83) imply: % 19.03/3.30 | | | | | (84) $false % 19.03/3.30 | | | | | % 19.03/3.30 | | | | | CLOSE: (84) is inconsistent. % 19.03/3.30 | | | | | % 19.03/3.30 | | | | Case 2: % 19.03/3.30 | | | | | % 19.03/3.30 | | | | | (85) ~ (all_50_2 = 0) | all_50_0 = 0 % 19.03/3.30 | | | | | % 19.03/3.30 | | | | | BETA: splitting (82) gives: % 19.03/3.30 | | | | | % 19.03/3.30 | | | | | Case 1: % 19.03/3.30 | | | | | | % 19.03/3.30 | | | | | | (86) ? [v0: any] : ? [v1: any] : ? [v2: any] : (doDivides0(xl, % 19.03/3.30 | | | | | | xm) = v2 & aNaturalNumber0(xm) = v1 & % 19.03/3.30 | | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ % 19.03/3.30 | | | | | | (v0 = 0))) % 19.03/3.30 | | | | | | % 19.03/3.30 | | | | | | DELTA: instantiating (86) with fresh symbols all_85_0, all_85_1, % 19.03/3.30 | | | | | | all_85_2 gives: % 19.03/3.30 | | | | | | (87) doDivides0(xl, xm) = all_85_0 & aNaturalNumber0(xm) = % 19.03/3.30 | | | | | | all_85_1 & aNaturalNumber0(xl) = all_85_2 & ( ~ (all_85_0 = % 19.03/3.30 | | | | | | 0) | ~ (all_85_1 = 0) | ~ (all_85_2 = 0)) % 19.03/3.30 | | | | | | % 19.03/3.30 | | | | | | ALPHA: (87) implies: % 19.03/3.30 | | | | | | (88) aNaturalNumber0(xl) = all_85_2 % 19.03/3.30 | | | | | | (89) aNaturalNumber0(xm) = all_85_1 % 19.03/3.30 | | | | | | (90) doDivides0(xl, xm) = all_85_0 % 19.03/3.30 | | | | | | (91) ~ (all_85_0 = 0) | ~ (all_85_1 = 0) | ~ (all_85_2 = 0) % 19.03/3.30 | | | | | | % 19.03/3.30 | | | | | | GROUND_INST: instantiating (18) with 0, all_85_2, xl, simplifying % 19.03/3.30 | | | | | | with (4), (88) gives: % 19.03/3.30 | | | | | | (92) all_85_2 = 0 % 19.03/3.30 | | | | | | % 19.03/3.30 | | | | | | GROUND_INST: instantiating (18) with 0, all_85_1, xm, simplifying % 19.03/3.30 | | | | | | with (5), (89) gives: % 19.03/3.30 | | | | | | (93) all_85_1 = 0 % 19.03/3.30 | | | | | | % 19.03/3.30 | | | | | | GROUND_INST: instantiating (22) with 0, all_85_0, xm, xl, % 19.03/3.30 | | | | | | simplifying with (35), (90) gives: % 19.03/3.30 | | | | | | (94) all_85_0 = 0 % 19.03/3.30 | | | | | | % 19.03/3.30 | | | | | | BETA: splitting (91) gives: % 19.03/3.30 | | | | | | % 19.03/3.30 | | | | | | Case 1: % 19.03/3.30 | | | | | | | % 19.03/3.30 | | | | | | | (95) ~ (all_85_0 = 0) % 19.03/3.30 | | | | | | | % 19.03/3.30 | | | | | | | REDUCE: (94), (95) imply: % 19.03/3.30 | | | | | | | (96) $false % 19.03/3.30 | | | | | | | % 19.03/3.30 | | | | | | | CLOSE: (96) is inconsistent. % 19.03/3.30 | | | | | | | % 19.03/3.30 | | | | | | Case 2: % 19.03/3.30 | | | | | | | % 19.03/3.30 | | | | | | | (97) ~ (all_85_1 = 0) | ~ (all_85_2 = 0) % 19.03/3.30 | | | | | | | % 19.03/3.30 | | | | | | | BETA: splitting (97) gives: % 19.03/3.30 | | | | | | | % 19.03/3.30 | | | | | | | Case 1: % 19.03/3.30 | | | | | | | | % 19.03/3.30 | | | | | | | | (98) ~ (all_85_1 = 0) % 19.03/3.30 | | | | | | | | % 19.03/3.30 | | | | | | | | REDUCE: (93), (98) imply: % 19.03/3.30 | | | | | | | | (99) $false % 19.03/3.30 | | | | | | | | % 19.03/3.30 | | | | | | | | CLOSE: (99) is inconsistent. % 19.03/3.30 | | | | | | | | % 19.03/3.30 | | | | | | | Case 2: % 19.03/3.30 | | | | | | | | % 19.03/3.30 | | | | | | | | (100) ~ (all_85_2 = 0) % 19.03/3.30 | | | | | | | | % 19.03/3.30 | | | | | | | | REDUCE: (92), (100) imply: % 19.03/3.30 | | | | | | | | (101) $false % 19.03/3.30 | | | | | | | | % 19.03/3.30 | | | | | | | | CLOSE: (101) is inconsistent. % 19.03/3.30 | | | | | | | | % 19.03/3.30 | | | | | | | End of split % 19.03/3.30 | | | | | | | % 19.03/3.30 | | | | | | End of split % 19.03/3.30 | | | | | | % 19.03/3.30 | | | | | Case 2: % 19.03/3.30 | | | | | | % 19.03/3.31 | | | | | | (102) ! [v0: $i] : (v0 = xp | ~ (sdtasdt0(xl, v0) = xm) | ~ % 19.03/3.31 | | | | | | $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 19.03/3.31 | | | | | | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( ~ % 19.03/3.31 | | | | | | (sdtasdt0(xl, xp) = v0) | ~ $i(xp) | (v0 = xm & % 19.03/3.31 | | | | | | aNaturalNumber0(xp) = 0)) % 19.03/3.31 | | | | | | % 19.03/3.31 | | | | | | ALPHA: (102) implies: % 19.03/3.31 | | | | | | (103) ! [v0: $i] : (v0 = xp | ~ (sdtasdt0(xl, v0) = xm) | ~ % 19.03/3.31 | | | | | | $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 19.03/3.31 | | | | | | aNaturalNumber0(v0) = v1)) % 19.03/3.31 | | | | | | % 19.03/3.31 | | | | | | BETA: splitting (50) gives: % 19.03/3.31 | | | | | | % 19.03/3.31 | | | | | | Case 1: % 19.03/3.31 | | | | | | | % 19.03/3.31 | | | | | | | (104) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(xm) = v1 & % 19.03/3.31 | | | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 19.03/3.31 | | | | | | | % 19.03/3.31 | | | | | | | DELTA: instantiating (104) with fresh symbols all_87_0, all_87_1 % 19.03/3.31 | | | | | | | gives: % 19.03/3.31 | | | | | | | (105) aNaturalNumber0(xm) = all_87_0 & aNaturalNumber0(xl) = % 19.03/3.31 | | | | | | | all_87_1 & ( ~ (all_87_0 = 0) | ~ (all_87_1 = 0)) % 19.03/3.31 | | | | | | | % 19.03/3.31 | | | | | | | ALPHA: (105) implies: % 19.03/3.31 | | | | | | | (106) aNaturalNumber0(xl) = all_87_1 % 19.03/3.31 | | | | | | | (107) aNaturalNumber0(xm) = all_87_0 % 19.03/3.31 | | | | | | | (108) ~ (all_87_0 = 0) | ~ (all_87_1 = 0) % 19.03/3.31 | | | | | | | % 19.03/3.31 | | | | | | | GROUND_INST: instantiating (18) with 0, all_87_1, xl, simplifying % 19.03/3.31 | | | | | | | with (4), (106) gives: % 19.03/3.31 | | | | | | | (109) all_87_1 = 0 % 19.03/3.31 | | | | | | | % 19.03/3.31 | | | | | | | GROUND_INST: instantiating (18) with 0, all_87_0, xm, simplifying % 19.03/3.31 | | | | | | | with (5), (107) gives: % 19.03/3.31 | | | | | | | (110) all_87_0 = 0 % 19.03/3.31 | | | | | | | % 19.03/3.31 | | | | | | | BETA: splitting (108) gives: % 19.03/3.31 | | | | | | | % 19.03/3.31 | | | | | | | Case 1: % 19.03/3.31 | | | | | | | | % 19.03/3.31 | | | | | | | | (111) ~ (all_87_0 = 0) % 19.03/3.31 | | | | | | | | % 19.03/3.31 | | | | | | | | REDUCE: (110), (111) imply: % 19.03/3.31 | | | | | | | | (112) $false % 19.03/3.31 | | | | | | | | % 19.03/3.31 | | | | | | | | CLOSE: (112) is inconsistent. % 19.03/3.31 | | | | | | | | % 19.03/3.31 | | | | | | | Case 2: % 19.03/3.31 | | | | | | | | % 19.03/3.31 | | | | | | | | (113) ~ (all_87_1 = 0) % 19.03/3.31 | | | | | | | | % 19.03/3.31 | | | | | | | | REDUCE: (109), (113) imply: % 19.03/3.31 | | | | | | | | (114) $false % 19.03/3.31 | | | | | | | | % 19.03/3.31 | | | | | | | | CLOSE: (114) is inconsistent. % 19.03/3.31 | | | | | | | | % 19.03/3.31 | | | | | | | End of split % 19.03/3.31 | | | | | | | % 19.03/3.31 | | | | | | Case 2: % 19.03/3.31 | | | | | | | % 19.03/3.31 | | | | | | | (115) ? [v0: $i] : (sdtasdt0(xl, v0) = xm & % 19.03/3.31 | | | | | | | aNaturalNumber0(v0) = 0 & $i(v0)) % 19.03/3.31 | | | | | | | % 19.03/3.31 | | | | | | | DELTA: instantiating (115) with fresh symbol all_87_0 gives: % 19.03/3.31 | | | | | | | (116) sdtasdt0(xl, all_87_0) = xm & aNaturalNumber0(all_87_0) = % 19.03/3.31 | | | | | | | 0 & $i(all_87_0) % 19.03/3.31 | | | | | | | % 19.03/3.31 | | | | | | | ALPHA: (116) implies: % 19.03/3.31 | | | | | | | (117) $i(all_87_0) % 19.03/3.31 | | | | | | | (118) aNaturalNumber0(all_87_0) = 0 % 19.03/3.31 | | | | | | | (119) sdtasdt0(xl, all_87_0) = xm % 19.03/3.31 | | | | | | | % 19.03/3.31 | | | | | | | BETA: splitting (85) gives: % 19.03/3.31 | | | | | | | % 19.03/3.31 | | | | | | | Case 1: % 19.03/3.31 | | | | | | | | % 19.03/3.31 | | | | | | | | (120) ~ (all_50_2 = 0) % 19.03/3.31 | | | | | | | | % 19.03/3.31 | | | | | | | | REDUCE: (79), (120) imply: % 19.03/3.31 | | | | | | | | (121) $false % 19.03/3.31 | | | | | | | | % 19.03/3.31 | | | | | | | | CLOSE: (121) is inconsistent. % 19.03/3.31 | | | | | | | | % 19.03/3.31 | | | | | | | Case 2: % 19.03/3.31 | | | | | | | | % 19.03/3.31 | | | | | | | | (122) all_50_0 = 0 % 19.03/3.31 | | | | | | | | % 19.03/3.31 | | | | | | | | REDUCE: (57), (122) imply: % 19.03/3.31 | | | | | | | | (123) aNaturalNumber0(all_35_0) = 0 % 19.03/3.31 | | | | | | | | % 19.03/3.31 | | | | | | | | BETA: splitting (53) gives: % 19.03/3.31 | | | | | | | | % 19.03/3.31 | | | | | | | | Case 1: % 19.03/3.31 | | | | | | | | | % 19.03/3.31 | | | | | | | | | (124) xl = sz00 % 19.03/3.31 | | | | | | | | | % 19.03/3.31 | | | | | | | | | REDUCE: (8), (124) imply: % 19.03/3.31 | | | | | | | | | (125) $false % 19.03/3.31 | | | | | | | | | % 19.03/3.31 | | | | | | | | | CLOSE: (125) is inconsistent. % 19.03/3.31 | | | | | | | | | % 19.03/3.31 | | | | | | | | Case 2: % 19.03/3.31 | | | | | | | | | % 19.03/3.31 | | | | | | | | | (126) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 19.03/3.31 | | | | | | | | | (doDivides0(xl, all_35_0) = v2 & % 19.03/3.31 | | | | | | | | | aNaturalNumber0(all_35_0) = v1 & % 19.03/3.31 | | | | | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | ~ (v1 = % 19.03/3.31 | | | | | | | | | 0) | ~ (v0 = 0))) | ( ! [v0: $i] : (v0 = xq | % 19.03/3.31 | | | | | | | | | ~ (sdtasdt0(xl, v0) = all_35_0) | ~ $i(v0) | ? % 19.03/3.31 | | | | | | | | | [v1: int] : ( ~ (v1 = 0) & aNaturalNumber0(v0) = % 19.03/3.31 | | | | | | | | | v1)) & ! [v0: $i] : ( ~ (sdtasdt0(xl, xq) = % 19.03/3.31 | | | | | | | | | v0) | ~ $i(xq) | (v0 = all_35_0 & % 19.03/3.31 | | | | | | | | | aNaturalNumber0(xq) = 0))) % 19.03/3.31 | | | | | | | | | % 19.03/3.31 | | | | | | | | | BETA: splitting (51) gives: % 19.03/3.31 | | | | | | | | | % 19.03/3.31 | | | | | | | | | Case 1: % 19.03/3.31 | | | | | | | | | | % 19.03/3.31 | | | | | | | | | | (127) ? [v0: any] : ? [v1: any] : % 19.03/3.31 | | | | | | | | | | (aNaturalNumber0(all_35_0) = v1 & % 19.03/3.31 | | | | | | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 % 19.03/3.31 | | | | | | | | | | = 0))) % 19.03/3.31 | | | | | | | | | | % 19.03/3.31 | | | | | | | | | | DELTA: instantiating (127) with fresh symbols all_103_0, % 19.03/3.31 | | | | | | | | | | all_103_1 gives: % 19.03/3.31 | | | | | | | | | | (128) aNaturalNumber0(all_35_0) = all_103_0 & % 19.03/3.31 | | | | | | | | | | aNaturalNumber0(xl) = all_103_1 & ( ~ (all_103_0 = % 19.03/3.31 | | | | | | | | | | 0) | ~ (all_103_1 = 0)) % 19.03/3.31 | | | | | | | | | | % 19.03/3.31 | | | | | | | | | | ALPHA: (128) implies: % 19.03/3.31 | | | | | | | | | | (129) aNaturalNumber0(xl) = all_103_1 % 19.03/3.31 | | | | | | | | | | (130) aNaturalNumber0(all_35_0) = all_103_0 % 19.03/3.31 | | | | | | | | | | (131) ~ (all_103_0 = 0) | ~ (all_103_1 = 0) % 19.03/3.31 | | | | | | | | | | % 19.03/3.31 | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_103_1, xl, % 19.03/3.31 | | | | | | | | | | simplifying with (4), (129) gives: % 19.03/3.31 | | | | | | | | | | (132) all_103_1 = 0 % 19.03/3.31 | | | | | | | | | | % 19.03/3.31 | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_103_0, all_35_0, % 19.03/3.31 | | | | | | | | | | simplifying with (123), (130) gives: % 19.03/3.31 | | | | | | | | | | (133) all_103_0 = 0 % 19.03/3.31 | | | | | | | | | | % 19.03/3.31 | | | | | | | | | | BETA: splitting (131) gives: % 19.03/3.31 | | | | | | | | | | % 19.03/3.31 | | | | | | | | | | Case 1: % 19.03/3.31 | | | | | | | | | | | % 19.03/3.31 | | | | | | | | | | | (134) ~ (all_103_0 = 0) % 19.03/3.31 | | | | | | | | | | | % 19.03/3.31 | | | | | | | | | | | REDUCE: (133), (134) imply: % 19.03/3.31 | | | | | | | | | | | (135) $false % 19.03/3.31 | | | | | | | | | | | % 19.03/3.31 | | | | | | | | | | | CLOSE: (135) is inconsistent. % 19.03/3.31 | | | | | | | | | | | % 19.03/3.31 | | | | | | | | | | Case 2: % 19.03/3.31 | | | | | | | | | | | % 19.03/3.31 | | | | | | | | | | | (136) ~ (all_103_1 = 0) % 19.03/3.31 | | | | | | | | | | | % 19.03/3.31 | | | | | | | | | | | REDUCE: (132), (136) imply: % 19.03/3.31 | | | | | | | | | | | (137) $false % 19.03/3.31 | | | | | | | | | | | % 19.03/3.31 | | | | | | | | | | | CLOSE: (137) is inconsistent. % 19.03/3.31 | | | | | | | | | | | % 19.03/3.31 | | | | | | | | | | End of split % 19.03/3.31 | | | | | | | | | | % 19.03/3.31 | | | | | | | | | Case 2: % 19.03/3.31 | | | | | | | | | | % 19.03/3.31 | | | | | | | | | | (138) ? [v0: $i] : (sdtasdt0(xl, v0) = all_35_0 & % 19.03/3.31 | | | | | | | | | | aNaturalNumber0(v0) = 0 & $i(v0)) % 19.03/3.31 | | | | | | | | | | % 19.03/3.31 | | | | | | | | | | DELTA: instantiating (138) with fresh symbol all_103_0 % 19.03/3.31 | | | | | | | | | | gives: % 19.03/3.32 | | | | | | | | | | (139) sdtasdt0(xl, all_103_0) = all_35_0 & % 19.03/3.32 | | | | | | | | | | aNaturalNumber0(all_103_0) = 0 & $i(all_103_0) % 19.03/3.32 | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | ALPHA: (139) implies: % 19.03/3.32 | | | | | | | | | | (140) $i(all_103_0) % 19.03/3.32 | | | | | | | | | | (141) aNaturalNumber0(all_103_0) = 0 % 19.03/3.32 | | | | | | | | | | (142) sdtasdt0(xl, all_103_0) = all_35_0 % 19.03/3.32 | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | BETA: splitting (48) gives: % 19.03/3.32 | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | Case 1: % 19.03/3.32 | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | (143) ? [v0: any] : ? [v1: any] : % 19.03/3.32 | | | | | | | | | | | (aNaturalNumber0(all_35_0) = v1 & % 19.03/3.32 | | | | | | | | | | | aNaturalNumber0(xm) = v0 & ( ~ (v1 = 0) | ~ (v0 % 19.03/3.32 | | | | | | | | | | | = 0))) % 19.03/3.32 | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | DELTA: instantiating (143) with fresh symbols all_107_0, % 19.03/3.32 | | | | | | | | | | | all_107_1 gives: % 19.03/3.32 | | | | | | | | | | | (144) aNaturalNumber0(all_35_0) = all_107_0 & % 19.03/3.32 | | | | | | | | | | | aNaturalNumber0(xm) = all_107_1 & ( ~ (all_107_0 = % 19.03/3.32 | | | | | | | | | | | 0) | ~ (all_107_1 = 0)) % 19.03/3.32 | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | ALPHA: (144) implies: % 19.03/3.32 | | | | | | | | | | | (145) aNaturalNumber0(xm) = all_107_1 % 19.03/3.32 | | | | | | | | | | | (146) aNaturalNumber0(all_35_0) = all_107_0 % 19.03/3.32 | | | | | | | | | | | (147) ~ (all_107_0 = 0) | ~ (all_107_1 = 0) % 19.03/3.32 | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_107_1, xm, % 19.03/3.32 | | | | | | | | | | | simplifying with (5), (145) gives: % 19.03/3.32 | | | | | | | | | | | (148) all_107_1 = 0 % 19.03/3.32 | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_107_0, all_35_0, % 19.03/3.32 | | | | | | | | | | | simplifying with (123), (146) gives: % 19.03/3.32 | | | | | | | | | | | (149) all_107_0 = 0 % 19.03/3.32 | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | BETA: splitting (147) gives: % 19.03/3.32 | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | Case 1: % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | (150) ~ (all_107_0 = 0) % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | REDUCE: (149), (150) imply: % 19.03/3.32 | | | | | | | | | | | | (151) $false % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | CLOSE: (151) is inconsistent. % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | Case 2: % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | (152) ~ (all_107_1 = 0) % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | REDUCE: (148), (152) imply: % 19.03/3.32 | | | | | | | | | | | | (153) $false % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | CLOSE: (153) is inconsistent. % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | End of split % 19.03/3.32 | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | Case 2: % 19.03/3.32 | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | (154) ? [v0: $i] : (sdtpldt0(xm, v0) = all_35_0 & % 19.03/3.32 | | | | | | | | | | | aNaturalNumber0(v0) = 0 & $i(v0)) % 19.03/3.32 | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | DELTA: instantiating (154) with fresh symbol all_107_0 % 19.03/3.32 | | | | | | | | | | | gives: % 19.03/3.32 | | | | | | | | | | | (155) sdtpldt0(xm, all_107_0) = all_35_0 & % 19.03/3.32 | | | | | | | | | | | aNaturalNumber0(all_107_0) = 0 & $i(all_107_0) % 19.03/3.32 | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | ALPHA: (155) implies: % 19.03/3.32 | | | | | | | | | | | (156) $i(all_107_0) % 19.03/3.32 | | | | | | | | | | | (157) sdtpldt0(xm, all_107_0) = all_35_0 % 19.03/3.32 | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | BETA: splitting (126) gives: % 19.03/3.32 | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | Case 1: % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | (158) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 19.03/3.32 | | | | | | | | | | | | (doDivides0(xl, all_35_0) = v2 & % 19.03/3.32 | | | | | | | | | | | | aNaturalNumber0(all_35_0) = v1 & % 19.03/3.32 | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | ~ (v1 % 19.03/3.32 | | | | | | | | | | | | = 0) | ~ (v0 = 0))) % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | DELTA: instantiating (158) with fresh symbols all_112_0, % 19.03/3.32 | | | | | | | | | | | | all_112_1, all_112_2 gives: % 19.03/3.32 | | | | | | | | | | | | (159) doDivides0(xl, all_35_0) = all_112_0 & % 19.03/3.32 | | | | | | | | | | | | aNaturalNumber0(all_35_0) = all_112_1 & % 19.03/3.32 | | | | | | | | | | | | aNaturalNumber0(xl) = all_112_2 & ( ~ (all_112_0 = % 19.03/3.32 | | | | | | | | | | | | 0) | ~ (all_112_1 = 0) | ~ (all_112_2 = 0)) % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | ALPHA: (159) implies: % 19.03/3.32 | | | | | | | | | | | | (160) aNaturalNumber0(xl) = all_112_2 % 19.03/3.32 | | | | | | | | | | | | (161) aNaturalNumber0(all_35_0) = all_112_1 % 19.03/3.32 | | | | | | | | | | | | (162) doDivides0(xl, all_35_0) = all_112_0 % 19.03/3.32 | | | | | | | | | | | | (163) ~ (all_112_0 = 0) | ~ (all_112_1 = 0) | ~ % 19.03/3.32 | | | | | | | | | | | | (all_112_2 = 0) % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_112_2, xl, % 19.03/3.32 | | | | | | | | | | | | simplifying with (4), (160) gives: % 19.03/3.32 | | | | | | | | | | | | (164) all_112_2 = 0 % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_112_1, all_35_0, % 19.03/3.32 | | | | | | | | | | | | simplifying with (123), (161) gives: % 19.03/3.32 | | | | | | | | | | | | (165) all_112_1 = 0 % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | GROUND_INST: instantiating (22) with 0, all_112_0, all_35_0, % 19.03/3.32 | | | | | | | | | | | | xl, simplifying with (41), (162) gives: % 19.03/3.32 | | | | | | | | | | | | (166) all_112_0 = 0 % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | BETA: splitting (163) gives: % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | Case 1: % 19.03/3.32 | | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | | (167) ~ (all_112_0 = 0) % 19.03/3.32 | | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | | REDUCE: (166), (167) imply: % 19.03/3.32 | | | | | | | | | | | | | (168) $false % 19.03/3.32 | | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | | CLOSE: (168) is inconsistent. % 19.03/3.32 | | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | Case 2: % 19.03/3.32 | | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | | (169) ~ (all_112_1 = 0) | ~ (all_112_2 = 0) % 19.03/3.32 | | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | | BETA: splitting (169) gives: % 19.03/3.32 | | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | | Case 1: % 19.03/3.32 | | | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | | | (170) ~ (all_112_1 = 0) % 19.03/3.32 | | | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | | | REDUCE: (165), (170) imply: % 19.03/3.32 | | | | | | | | | | | | | | (171) $false % 19.03/3.32 | | | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | | | CLOSE: (171) is inconsistent. % 19.03/3.32 | | | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | | Case 2: % 19.03/3.32 | | | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | | | (172) ~ (all_112_2 = 0) % 19.03/3.32 | | | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | | | REDUCE: (164), (172) imply: % 19.03/3.32 | | | | | | | | | | | | | | (173) $false % 19.03/3.32 | | | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | | | CLOSE: (173) is inconsistent. % 19.03/3.32 | | | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | | End of split % 19.03/3.32 | | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | End of split % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | Case 2: % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | (174) ! [v0: $i] : (v0 = xq | ~ (sdtasdt0(xl, v0) = % 19.03/3.32 | | | | | | | | | | | | all_35_0) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 % 19.03/3.32 | | | | | | | | | | | | = 0) & aNaturalNumber0(v0) = v1)) & ! [v0: % 19.03/3.32 | | | | | | | | | | | | $i] : ( ~ (sdtasdt0(xl, xq) = v0) | ~ $i(xq) | % 19.03/3.32 | | | | | | | | | | | | (v0 = all_35_0 & aNaturalNumber0(xq) = 0)) % 19.03/3.32 | | | | | | | | | | | | % 19.03/3.32 | | | | | | | | | | | | ALPHA: (174) implies: % 19.03/3.33 | | | | | | | | | | | | (175) ! [v0: $i] : (v0 = xq | ~ (sdtasdt0(xl, v0) = % 19.03/3.33 | | | | | | | | | | | | all_35_0) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 % 19.03/3.33 | | | | | | | | | | | | = 0) & aNaturalNumber0(v0) = v1)) % 19.03/3.33 | | | | | | | | | | | | % 19.03/3.33 | | | | | | | | | | | | GROUND_INST: instantiating (mAddComm) with xm, all_107_0, % 19.03/3.33 | | | | | | | | | | | | all_35_0, simplifying with (12), (156), (157) % 19.03/3.33 | | | | | | | | | | | | gives: % 19.03/3.33 | | | | | | | | | | | | (176) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 19.03/3.33 | | | | | | | | | | | | (sdtpldt0(all_107_0, xm) = v2 & % 19.03/3.33 | | | | | | | | | | | | aNaturalNumber0(all_107_0) = v1 & % 19.03/3.33 | | | | | | | | | | | | aNaturalNumber0(xm) = v0 & $i(v2) & ( ~ (v1 = 0) % 19.03/3.33 | | | | | | | | | | | | | ~ (v0 = 0) | v2 = all_35_0)) % 19.03/3.33 | | | | | | | | | | | | % 19.03/3.33 | | | | | | | | | | | | GROUND_INST: instantiating (103) with all_87_0, simplifying % 19.03/3.33 | | | | | | | | | | | | with (117), (119) gives: % 19.03/3.33 | | | | | | | | | | | | (177) all_87_0 = xp | ? [v0: int] : ( ~ (v0 = 0) & % 19.03/3.33 | | | | | | | | | | | | aNaturalNumber0(all_87_0) = v0) % 19.03/3.33 | | | | | | | | | | | | % 19.03/3.33 | | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with xl, all_87_0, xm, % 19.03/3.33 | | | | | | | | | | | | simplifying with (10), (117), (119) gives: % 19.03/3.33 | | | | | | | | | | | | (178) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 19.03/3.33 | | | | | | | | | | | | (sdtasdt0(all_87_0, xl) = v2 & % 19.03/3.33 | | | | | | | | | | | | aNaturalNumber0(all_87_0) = v1 & % 19.03/3.33 | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v2) & ( ~ (v1 = 0) % 19.03/3.33 | | | | | | | | | | | | | ~ (v0 = 0) | v2 = xm)) % 19.03/3.33 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | GROUND_INST: instantiating (64) with all_87_0, all_103_0, xm, % 19.03/3.34 | | | | | | | | | | | | all_35_0, simplifying with (117), (119), (140), % 19.03/3.34 | | | | | | | | | | | | (142) gives: % 19.03/3.34 | | | | | | | | | | | | (179) all_103_0 = all_87_0 | ? [v0: any] : ? [v1: any] % 19.03/3.34 | | | | | | | | | | | | : ? [v2: $i] : ? [v3: $i] : (sdtasdt0(all_103_0, % 19.03/3.34 | | | | | | | | | | | | xl) = v3 & sdtasdt0(all_87_0, xl) = v2 & % 19.03/3.34 | | | | | | | | | | | | aNaturalNumber0(all_103_0) = v1 & % 19.03/3.34 | | | | | | | | | | | | aNaturalNumber0(all_87_0) = v0 & $i(v3) & $i(v2) % 19.03/3.34 | | | | | | | | | | | | & ( ~ (v1 = 0) | ~ (v0 = 0) | ( ~ (v3 = v2) & % 19.03/3.34 | | | | | | | | | | | | ~ (all_35_0 = xm)))) % 19.03/3.34 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | GROUND_INST: instantiating (64) with all_103_0, all_87_0, % 19.03/3.34 | | | | | | | | | | | | all_35_0, xm, simplifying with (117), (119), % 19.03/3.34 | | | | | | | | | | | | (140), (142) gives: % 19.03/3.34 | | | | | | | | | | | | (180) all_103_0 = all_87_0 | ? [v0: any] : ? [v1: any] % 19.03/3.34 | | | | | | | | | | | | : ? [v2: $i] : ? [v3: $i] : (sdtasdt0(all_103_0, % 19.03/3.34 | | | | | | | | | | | | xl) = v2 & sdtasdt0(all_87_0, xl) = v3 & % 19.03/3.34 | | | | | | | | | | | | aNaturalNumber0(all_103_0) = v0 & % 19.03/3.34 | | | | | | | | | | | | aNaturalNumber0(all_87_0) = v1 & $i(v3) & $i(v2) % 19.03/3.34 | | | | | | | | | | | | & ( ~ (v1 = 0) | ~ (v0 = 0) | ( ~ (v3 = v2) & % 19.03/3.34 | | | | | | | | | | | | ~ (all_35_0 = xm)))) % 19.03/3.34 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | GROUND_INST: instantiating (175) with all_103_0, simplifying % 19.03/3.34 | | | | | | | | | | | | with (140), (142) gives: % 19.03/3.34 | | | | | | | | | | | | (181) all_103_0 = xq | ? [v0: int] : ( ~ (v0 = 0) & % 19.03/3.34 | | | | | | | | | | | | aNaturalNumber0(all_103_0) = v0) % 19.03/3.34 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with xl, all_103_0, % 19.03/3.34 | | | | | | | | | | | | all_35_0, simplifying with (10), (140), (142) % 19.03/3.34 | | | | | | | | | | | | gives: % 19.03/3.34 | | | | | | | | | | | | (182) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 19.03/3.34 | | | | | | | | | | | | (sdtasdt0(all_103_0, xl) = v2 & % 19.03/3.34 | | | | | | | | | | | | aNaturalNumber0(all_103_0) = v1 & % 19.03/3.34 | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v2) & ( ~ (v1 = 0) % 19.03/3.34 | | | | | | | | | | | | | ~ (v0 = 0) | v2 = all_35_0)) % 19.03/3.34 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | GROUND_INST: instantiating (mLETotal) with xq, xp, all_66_0, % 19.03/3.34 | | | | | | | | | | | | simplifying with (15), (16), (71) gives: % 19.03/3.34 | | | | | | | | | | | | (183) all_66_0 = 0 | ? [v0: any] : ? [v1: any] : ? % 19.03/3.34 | | | | | | | | | | | | [v2: any] : (sdtlseqdt0(xp, xq) = v2 & % 19.03/3.34 | | | | | | | | | | | | aNaturalNumber0(xq) = v0 & aNaturalNumber0(xp) = % 19.03/3.34 | | | | | | | | | | | | v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v2 = 0 & ~ % 19.03/3.34 | | | | | | | | | | | | (xq = xp)))) % 19.03/3.34 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | DELTA: instantiating (182) with fresh symbols all_117_0, % 19.03/3.34 | | | | | | | | | | | | all_117_1, all_117_2 gives: % 19.03/3.34 | | | | | | | | | | | | (184) sdtasdt0(all_103_0, xl) = all_117_0 & % 19.03/3.34 | | | | | | | | | | | | aNaturalNumber0(all_103_0) = all_117_1 & % 19.03/3.34 | | | | | | | | | | | | aNaturalNumber0(xl) = all_117_2 & $i(all_117_0) & % 19.03/3.34 | | | | | | | | | | | | ( ~ (all_117_1 = 0) | ~ (all_117_2 = 0) | % 19.03/3.34 | | | | | | | | | | | | all_117_0 = all_35_0) % 19.03/3.34 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | ALPHA: (184) implies: % 19.03/3.34 | | | | | | | | | | | | (185) aNaturalNumber0(xl) = all_117_2 % 19.03/3.34 | | | | | | | | | | | | (186) aNaturalNumber0(all_103_0) = all_117_1 % 19.03/3.34 | | | | | | | | | | | | (187) sdtasdt0(all_103_0, xl) = all_117_0 % 19.03/3.34 | | | | | | | | | | | | (188) ~ (all_117_1 = 0) | ~ (all_117_2 = 0) | % 19.03/3.34 | | | | | | | | | | | | all_117_0 = all_35_0 % 19.03/3.34 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | DELTA: instantiating (176) with fresh symbols all_119_0, % 19.03/3.34 | | | | | | | | | | | | all_119_1, all_119_2 gives: % 19.03/3.34 | | | | | | | | | | | | (189) sdtpldt0(all_107_0, xm) = all_119_0 & % 19.03/3.34 | | | | | | | | | | | | aNaturalNumber0(all_107_0) = all_119_1 & % 19.03/3.34 | | | | | | | | | | | | aNaturalNumber0(xm) = all_119_2 & $i(all_119_0) & % 19.03/3.34 | | | | | | | | | | | | ( ~ (all_119_1 = 0) | ~ (all_119_2 = 0) | % 19.03/3.34 | | | | | | | | | | | | all_119_0 = all_35_0) % 19.03/3.34 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | ALPHA: (189) implies: % 19.03/3.34 | | | | | | | | | | | | (190) aNaturalNumber0(xm) = all_119_2 % 19.03/3.34 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | DELTA: instantiating (178) with fresh symbols all_121_0, % 19.03/3.34 | | | | | | | | | | | | all_121_1, all_121_2 gives: % 19.03/3.34 | | | | | | | | | | | | (191) sdtasdt0(all_87_0, xl) = all_121_0 & % 19.03/3.34 | | | | | | | | | | | | aNaturalNumber0(all_87_0) = all_121_1 & % 19.03/3.34 | | | | | | | | | | | | aNaturalNumber0(xl) = all_121_2 & $i(all_121_0) & % 19.03/3.34 | | | | | | | | | | | | ( ~ (all_121_1 = 0) | ~ (all_121_2 = 0) | % 19.03/3.34 | | | | | | | | | | | | all_121_0 = xm) % 19.03/3.34 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | ALPHA: (191) implies: % 19.03/3.34 | | | | | | | | | | | | (192) aNaturalNumber0(xl) = all_121_2 % 19.03/3.34 | | | | | | | | | | | | (193) aNaturalNumber0(all_87_0) = all_121_1 % 19.03/3.34 | | | | | | | | | | | | (194) sdtasdt0(all_87_0, xl) = all_121_0 % 19.03/3.34 | | | | | | | | | | | | (195) ~ (all_121_1 = 0) | ~ (all_121_2 = 0) | % 19.03/3.34 | | | | | | | | | | | | all_121_0 = xm % 19.03/3.34 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_121_2, xl, % 19.03/3.34 | | | | | | | | | | | | simplifying with (4), (192) gives: % 19.03/3.34 | | | | | | | | | | | | (196) all_121_2 = 0 % 19.03/3.34 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | GROUND_INST: instantiating (18) with all_117_2, all_121_2, xl, % 19.03/3.34 | | | | | | | | | | | | simplifying with (185), (192) gives: % 19.03/3.34 | | | | | | | | | | | | (197) all_121_2 = all_117_2 % 19.03/3.34 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_119_2, xm, % 19.03/3.34 | | | | | | | | | | | | simplifying with (5), (190) gives: % 19.03/3.34 | | | | | | | | | | | | (198) all_119_2 = 0 % 19.03/3.34 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_121_1, all_87_0, % 19.03/3.34 | | | | | | | | | | | | simplifying with (118), (193) gives: % 19.03/3.34 | | | | | | | | | | | | (199) all_121_1 = 0 % 19.03/3.34 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_117_1, all_103_0, % 19.03/3.34 | | | | | | | | | | | | simplifying with (141), (186) gives: % 19.03/3.34 | | | | | | | | | | | | (200) all_117_1 = 0 % 19.03/3.34 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | COMBINE_EQS: (196), (197) imply: % 19.03/3.34 | | | | | | | | | | | | (201) all_117_2 = 0 % 19.03/3.34 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | BETA: splitting (177) gives: % 19.03/3.34 | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | Case 1: % 19.03/3.34 | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | (202) all_87_0 = xp % 19.03/3.34 | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | REDUCE: (194), (202) imply: % 19.03/3.34 | | | | | | | | | | | | | (203) sdtasdt0(xp, xl) = all_121_0 % 19.03/3.34 | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | REDUCE: (119), (202) imply: % 19.03/3.34 | | | | | | | | | | | | | (204) sdtasdt0(xl, xp) = xm % 19.03/3.34 | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | REDUCE: (118), (202) imply: % 19.03/3.34 | | | | | | | | | | | | | (205) aNaturalNumber0(xp) = 0 % 19.03/3.34 | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | BETA: splitting (195) gives: % 19.03/3.34 | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | Case 1: % 19.03/3.34 | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | | (206) ~ (all_121_1 = 0) % 19.03/3.34 | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | | REDUCE: (199), (206) imply: % 19.03/3.34 | | | | | | | | | | | | | | (207) $false % 19.03/3.34 | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | | CLOSE: (207) is inconsistent. % 19.03/3.34 | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | Case 2: % 19.03/3.34 | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | | (208) ~ (all_121_2 = 0) | all_121_0 = xm % 19.03/3.34 | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | | BETA: splitting (208) gives: % 19.03/3.34 | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | | Case 1: % 19.03/3.34 | | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | | | (209) ~ (all_121_2 = 0) % 19.03/3.34 | | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | | | REDUCE: (196), (209) imply: % 19.03/3.34 | | | | | | | | | | | | | | | (210) $false % 19.03/3.34 | | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | | | CLOSE: (210) is inconsistent. % 19.03/3.34 | | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | | Case 2: % 19.03/3.34 | | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | | | (211) all_121_0 = xm % 19.03/3.34 | | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | | | REDUCE: (203), (211) imply: % 19.03/3.34 | | | | | | | | | | | | | | | (212) sdtasdt0(xp, xl) = xm % 19.03/3.34 | | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | | | BETA: splitting (181) gives: % 19.03/3.34 | | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | | | Case 1: % 19.03/3.34 | | | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | | | | (213) all_103_0 = xq % 19.03/3.34 | | | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | | | | REDUCE: (187), (213) imply: % 19.03/3.34 | | | | | | | | | | | | | | | | (214) sdtasdt0(xq, xl) = all_117_0 % 19.03/3.34 | | | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | | | | REDUCE: (142), (213) imply: % 19.03/3.34 | | | | | | | | | | | | | | | | (215) sdtasdt0(xl, xq) = all_35_0 % 19.03/3.34 | | | | | | | | | | | | | | | | % 19.03/3.34 | | | | | | | | | | | | | | | | REDUCE: (141), (213) imply: % 19.03/3.34 | | | | | | | | | | | | | | | | (216) aNaturalNumber0(xq) = 0 % 19.03/3.34 | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | BETA: splitting (188) gives: % 19.03/3.35 | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | Case 1: % 19.03/3.35 | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | (217) ~ (all_117_1 = 0) % 19.03/3.35 | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | REDUCE: (200), (217) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | (218) $false % 19.03/3.35 | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | CLOSE: (218) is inconsistent. % 19.03/3.35 | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | Case 2: % 19.03/3.35 | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | (219) ~ (all_117_2 = 0) | all_117_0 = all_35_0 % 19.03/3.35 | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | BETA: splitting (219) gives: % 19.03/3.35 | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.35 | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | (220) ~ (all_117_2 = 0) % 19.03/3.35 | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | REDUCE: (201), (220) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | (221) $false % 19.03/3.35 | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | CLOSE: (221) is inconsistent. % 19.03/3.35 | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.35 | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | (222) all_117_0 = all_35_0 % 19.03/3.35 | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | REDUCE: (214), (222) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | (223) sdtasdt0(xq, xl) = all_35_0 % 19.03/3.35 | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (18) with all_66_2, 0, xp, % 19.03/3.35 | | | | | | | | | | | | | | | | | | simplifying with (69), (205) gives: % 19.03/3.35 | | | | | | | | | | | | | | | | | | (224) all_66_2 = 0 % 19.03/3.35 | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (18) with all_66_1, 0, xq, % 19.03/3.35 | | | | | | | | | | | | | | | | | | simplifying with (70), (216) gives: % 19.03/3.35 | | | | | | | | | | | | | | | | | | (225) all_66_1 = 0 % 19.03/3.35 | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | BETA: splitting (72) gives: % 19.03/3.35 | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | (226) ~ (all_66_1 = 0) % 19.03/3.35 | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | REDUCE: (225), (226) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | (227) $false % 19.03/3.35 | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | CLOSE: (227) is inconsistent. % 19.03/3.35 | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | (228) ~ (all_66_2 = 0) | (all_66_0 = 0 & ~ (xq = xp)) % 19.03/3.35 | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | BETA: splitting (183) gives: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | (229) all_66_0 = 0 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | REDUCE: (71), (229) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | (230) sdtlseqdt0(xq, xp) = 0 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | BETA: splitting (228) gives: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | (231) ~ (all_66_2 = 0) % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | REDUCE: (224), (231) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | (232) $false % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | CLOSE: (232) is inconsistent. % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | (233) all_66_0 = 0 & ~ (xq = xp) % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | ALPHA: (233) implies: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | (234) ~ (xq = xp) % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | BETA: splitting (180) gives: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | (235) all_103_0 = all_87_0 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (213), (235) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | (236) all_87_0 = xq % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (202), (236) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | (237) xq = xp % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | SIMP: (237) implies: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | (238) xq = xp % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (234), (238) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | (239) $false % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | CLOSE: (239) is inconsistent. % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | (240) ~ (all_103_0 = all_87_0) % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | (241) ? [v0: any] : ? [v1: any] : ? [v2: $i] : ? % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | [v3: $i] : (sdtasdt0(all_103_0, xl) = v2 & % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(all_87_0, xl) = v3 & % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_103_0) = v0 & % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_87_0) = v1 & $i(v3) & $i(v2) % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | & ( ~ (v1 = 0) | ~ (v0 = 0) | ( ~ (v3 = v2) & % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | ~ (all_35_0 = xm)))) % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (241) with fresh symbols all_188_0, % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | all_188_1, all_188_2, all_188_3 gives: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | (242) sdtasdt0(all_103_0, xl) = all_188_1 & % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(all_87_0, xl) = all_188_0 & % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_103_0) = all_188_3 & % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_87_0) = all_188_2 & % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | $i(all_188_0) & $i(all_188_1) & ( ~ (all_188_2 = % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | 0) | ~ (all_188_3 = 0) | ( ~ (all_188_0 = % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | all_188_1) & ~ (all_35_0 = xm))) % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | ALPHA: (242) implies: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | (243) $i(all_188_1) % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | (244) $i(all_188_0) % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | (245) aNaturalNumber0(all_87_0) = all_188_2 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | (246) aNaturalNumber0(all_103_0) = all_188_3 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | (247) sdtasdt0(all_87_0, xl) = all_188_0 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | (248) sdtasdt0(all_103_0, xl) = all_188_1 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (213), (248) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | (249) sdtasdt0(xq, xl) = all_188_1 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (202), (247) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | (250) sdtasdt0(xp, xl) = all_188_0 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (213), (246) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | (251) aNaturalNumber0(xq) = all_188_3 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (202), (245) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | (252) aNaturalNumber0(xp) = all_188_2 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (179) gives: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | (253) all_103_0 = all_87_0 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (213), (253) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | (254) all_87_0 = xq % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (202), (254) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | (255) xq = xp % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | SIMP: (255) implies: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | (256) xq = xp % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (234), (256) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | (257) $false % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (257) is inconsistent. % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | (258) ? [v0: any] : ? [v1: any] : ? [v2: $i] : ? % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | [v3: $i] : (sdtasdt0(all_103_0, xl) = v3 & % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(all_87_0, xl) = v2 & % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_103_0) = v1 & % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_87_0) = v0 & $i(v3) & $i(v2) % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | & ( ~ (v1 = 0) | ~ (v0 = 0) | ( ~ (v3 = v2) & % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | ~ (all_35_0 = xm)))) % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (258) with fresh symbols all_195_0, % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | all_195_1, all_195_2, all_195_3 gives: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | (259) sdtasdt0(all_103_0, xl) = all_195_0 & % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(all_87_0, xl) = all_195_1 & % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_103_0) = all_195_2 & % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_87_0) = all_195_3 & % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | $i(all_195_0) & $i(all_195_1) & ( ~ (all_195_2 = % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | 0) | ~ (all_195_3 = 0) | ( ~ (all_195_0 = % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | all_195_1) & ~ (all_35_0 = xm))) % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (259) implies: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | (260) aNaturalNumber0(all_87_0) = all_195_3 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | (261) aNaturalNumber0(all_103_0) = all_195_2 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | (262) sdtasdt0(all_87_0, xl) = all_195_1 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | (263) sdtasdt0(all_103_0, xl) = all_195_0 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | (264) ~ (all_195_2 = 0) | ~ (all_195_3 = 0) | ( ~ % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | (all_195_0 = all_195_1) & ~ (all_35_0 = xm)) % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (213), (263) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | (265) sdtasdt0(xq, xl) = all_195_0 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (202), (262) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | (266) sdtasdt0(xp, xl) = all_195_1 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (213), (261) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | (267) aNaturalNumber0(xq) = all_195_2 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (202), (260) imply: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | (268) aNaturalNumber0(xp) = all_195_3 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_195_3, xp, % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | simplifying with (205), (268) gives: % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | (269) all_195_3 = 0 % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (18) with all_188_2, all_195_3, xp, % 19.03/3.35 | | | | | | | | | | | | | | | | | | | | | | | simplifying with (252), (268) gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | (270) all_195_3 = all_188_2 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_195_2, xq, % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | simplifying with (216), (267) gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | (271) all_195_2 = 0 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (18) with all_188_3, all_195_2, xq, % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | simplifying with (251), (267) gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | (272) all_195_2 = all_188_3 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (20) with xm, all_195_1, xl, xp, % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | simplifying with (212), (266) gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | (273) all_195_1 = xm % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (20) with all_188_0, all_195_1, xl, % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | xp, simplifying with (250), (266) gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | (274) all_195_1 = all_188_0 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (20) with all_35_0, all_195_0, xl, % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | xq, simplifying with (223), (265) gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | (275) all_195_0 = all_35_0 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (20) with all_188_1, all_195_0, xl, % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | xq, simplifying with (249), (265) gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | (276) all_195_0 = all_188_1 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (275), (276) imply: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | (277) all_188_1 = all_35_0 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (273), (274) imply: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | (278) all_188_0 = xm % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (271), (272) imply: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | (279) all_188_3 = 0 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (269), (270) imply: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | (280) all_188_2 = 0 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (264) gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | (281) ~ (all_195_2 = 0) % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (271), (281) imply: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | (282) $false % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (282) is inconsistent. % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | (283) ~ (all_195_3 = 0) | ( ~ (all_195_0 = all_195_1) & % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | ~ (all_35_0 = xm)) % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (283) gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | (284) ~ (all_195_3 = 0) % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (269), (284) imply: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | (285) $false % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (285) is inconsistent. % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | (286) ~ (all_195_0 = all_195_1) & ~ (all_35_0 = xm) % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (286) implies: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | (287) ~ (all_195_0 = all_195_1) % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (273), (275), (287) imply: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | (288) ~ (all_35_0 = xm) % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (47) gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | (289) all_35_0 = xm % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (288), (289) imply: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | (290) $false % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (290) is inconsistent. % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | (291) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | (sdtlseqdt0(all_35_0, xm) = v2 & % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_0) = v1 & % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xm) = v0 & ( ~ (v2 = 0) | ~ (v1 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | = 0) | ~ (v0 = 0))) % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (291) with fresh symbols all_222_0, % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | all_222_1, all_222_2 gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | (292) sdtlseqdt0(all_35_0, xm) = all_222_0 & % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_0) = all_222_1 & % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xm) = all_222_2 & ( ~ (all_222_0 = % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | 0) | ~ (all_222_1 = 0) | ~ (all_222_2 = 0)) % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (292) implies: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | (293) aNaturalNumber0(xm) = all_222_2 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | (294) aNaturalNumber0(all_35_0) = all_222_1 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | (295) sdtlseqdt0(all_35_0, xm) = all_222_0 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | (296) ~ (all_222_0 = 0) | ~ (all_222_1 = 0) | ~ % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | (all_222_2 = 0) % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_222_2, xm, % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (5), (293) gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | (297) all_222_2 = 0 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_222_1, all_35_0, % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (123), (294) gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | (298) all_222_1 = 0 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (296) gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | (299) ~ (all_222_0 = 0) % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (2) with xl, xq, xp, all_35_0, xm, % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | all_222_0, simplifying with (10), (15), (16), % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | (204), (215), (295) gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | (300) xq = xp | xl = sz00 | ? [v0: any] : ? [v1: any] % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | : ? [v2: any] : ? [v3: any] : ? [v4: $i] : ? % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | [v5: $i] : ? [v6: any] : (sdtlseqdt0(v4, v5) = v6 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | & sdtlseqdt0(xq, xp) = v3 & sdtasdt0(xq, xl) = % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | v4 & sdtasdt0(xp, xl) = v5 & aNaturalNumber0(xq) % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | = v1 & aNaturalNumber0(xp) = v2 & % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v5) & $i(v4) & ( ~ % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | = 0) | (v6 = 0 & all_222_0 = 0 & ~ (v5 = % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | v4) & ~ (all_35_0 = xm)))) % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mDefLE) with all_35_0, xm, % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | all_222_0, simplifying with (12), (43), (295) % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | (301) ? [v0: any] : ? [v1: any] : % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | (aNaturalNumber0(all_35_0) = v0 & % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xm) = v1 & ( ~ (v1 = 0) | ~ (v0 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | = 0))) | (( ~ (all_222_0 = 0) | ? [v0: $i] % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | : (sdtpldt0(all_35_0, v0) = xm & % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(v0) = 0 & $i(v0))) & % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | (all_222_0 = 0 | ! [v0: $i] : ( ~ % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | (sdtpldt0(all_35_0, v0) = xm) | ~ $i(v0) | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | ? [v1: int] : ( ~ (v1 = 0) & % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(v0) = v1)))) % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (300) gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (302) xl = sz00 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (8), (302) imply: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (303) $false % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (303) is inconsistent. % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (304) xq = xp | ? [v0: any] : ? [v1: any] : ? [v2: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | any] : ? [v3: any] : ? [v4: $i] : ? [v5: $i] % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | : ? [v6: any] : (sdtlseqdt0(v4, v5) = v6 & % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | sdtlseqdt0(xq, xp) = v3 & sdtasdt0(xq, xl) = v4 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | & sdtasdt0(xp, xl) = v5 & aNaturalNumber0(xq) = % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | v1 & aNaturalNumber0(xp) = v2 & % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v5) & $i(v4) & ( ~ % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | = 0) | (v6 = 0 & all_222_0 = 0 & ~ (v5 = % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | v4) & ~ (all_35_0 = xm)))) % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (301) gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (305) ? [v0: any] : ? [v1: any] : % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (aNaturalNumber0(all_35_0) = v0 & % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xm) = v1 & ( ~ (v1 = 0) | ~ (v0 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | = 0))) % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (305) with fresh symbols all_247_0, % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_247_1 gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (306) aNaturalNumber0(all_35_0) = all_247_1 & % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xm) = all_247_0 & ( ~ (all_247_0 = % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 0) | ~ (all_247_1 = 0)) % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (306) implies: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (307) aNaturalNumber0(xm) = all_247_0 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (308) aNaturalNumber0(all_35_0) = all_247_1 % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (309) ~ (all_247_0 = 0) | ~ (all_247_1 = 0) % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_247_0, xm, % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (5), (307) gives: % 19.03/3.36 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (310) all_247_0 = 0 % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_247_1, all_35_0, % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (123), (308) gives: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (311) all_247_1 = 0 % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (309) gives: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (312) ~ (all_247_0 = 0) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (310), (312) imply: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (313) $false % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (313) is inconsistent. % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (314) ~ (all_247_1 = 0) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (311), (314) imply: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (315) $false % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (315) is inconsistent. % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (316) ( ~ (all_222_0 = 0) | ? [v0: $i] : % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (sdtpldt0(all_35_0, v0) = xm & % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(v0) = 0 & $i(v0))) & % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (all_222_0 = 0 | ! [v0: $i] : ( ~ % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (sdtpldt0(all_35_0, v0) = xm) | ~ $i(v0) | ? % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [v1: int] : ( ~ (v1 = 0) & aNaturalNumber0(v0) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | = v1))) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (316) implies: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (317) all_222_0 = 0 | ! [v0: $i] : ( ~ % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (sdtpldt0(all_35_0, v0) = xm) | ~ $i(v0) | ? % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [v1: int] : ( ~ (v1 = 0) & aNaturalNumber0(v0) = % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | v1)) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (304) gives: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (318) xq = xp % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (234), (318) imply: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (319) $false % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (319) is inconsistent. % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (320) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [v3: any] : ? [v4: $i] : ? [v5: $i] : ? [v6: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | any] : (sdtlseqdt0(v4, v5) = v6 & sdtlseqdt0(xq, % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | xp) = v3 & sdtasdt0(xq, xl) = v4 & % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | sdtasdt0(xp, xl) = v5 & aNaturalNumber0(xq) = v1 % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | & aNaturalNumber0(xp) = v2 & aNaturalNumber0(xl) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | = v0 & $i(v5) & $i(v4) & ( ~ (v3 = 0) | ~ (v2 = % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 0) | ~ (v1 = 0) | ~ (v0 = 0) | (v6 = 0 & % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_222_0 = 0 & ~ (v5 = v4) & ~ (all_35_0 % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | = xm)))) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (317) gives: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (321) all_222_0 = 0 % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (299), (321) imply: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (322) $false % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (322) is inconsistent. % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (320) with fresh symbols all_254_0, % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_254_1, all_254_2, all_254_3, all_254_4, % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_254_5, all_254_6 gives: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (323) sdtlseqdt0(all_254_2, all_254_1) = all_254_0 & % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | sdtlseqdt0(xq, xp) = all_254_3 & sdtasdt0(xq, xl) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | = all_254_2 & sdtasdt0(xp, xl) = all_254_1 & % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xq) = all_254_5 & % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xp) = all_254_4 & % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = all_254_6 & $i(all_254_1) & % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | $i(all_254_2) & ( ~ (all_254_3 = 0) | ~ % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (all_254_4 = 0) | ~ (all_254_5 = 0) | ~ % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (all_254_6 = 0) | (all_254_0 = 0 & all_222_0 = 0 % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | & ~ (all_254_1 = all_254_2) & ~ (all_35_0 = % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | xm))) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (323) implies: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (324) aNaturalNumber0(xl) = all_254_6 % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (325) aNaturalNumber0(xp) = all_254_4 % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (326) aNaturalNumber0(xq) = all_254_5 % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (327) sdtlseqdt0(xq, xp) = all_254_3 % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (328) ~ (all_254_3 = 0) | ~ (all_254_4 = 0) | ~ % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (all_254_5 = 0) | ~ (all_254_6 = 0) | (all_254_0 % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | = 0 & all_222_0 = 0 & ~ (all_254_1 = all_254_2) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | & ~ (all_35_0 = xm)) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_254_6, xl, % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (4), (324) gives: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (329) all_254_6 = 0 % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_254_4, xp, % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (205), (325) gives: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (330) all_254_4 = 0 % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_254_5, xq, % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (216), (326) gives: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (331) all_254_5 = 0 % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (21) with 0, all_254_3, xp, xq, % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (230), (327) gives: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (332) all_254_3 = 0 % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (328) gives: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (333) ~ (all_254_3 = 0) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (332), (333) imply: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (334) $false % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (334) is inconsistent. % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (335) ~ (all_254_4 = 0) | ~ (all_254_5 = 0) | ~ % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (all_254_6 = 0) | (all_254_0 = 0 & all_222_0 = 0 & % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ~ (all_254_1 = all_254_2) & ~ (all_35_0 = xm)) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (335) gives: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (336) ~ (all_254_4 = 0) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (330), (336) imply: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (337) $false % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (337) is inconsistent. % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (338) ~ (all_254_5 = 0) | ~ (all_254_6 = 0) | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (all_254_0 = 0 & all_222_0 = 0 & ~ (all_254_1 = % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_254_2) & ~ (all_35_0 = xm)) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (338) gives: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (339) ~ (all_254_5 = 0) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (331), (339) imply: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (340) $false % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (340) is inconsistent. % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (341) ~ (all_254_6 = 0) | (all_254_0 = 0 & all_222_0 = % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 0 & ~ (all_254_1 = all_254_2) & ~ (all_35_0 = % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | xm)) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (341) gives: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (342) ~ (all_254_6 = 0) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (329), (342) imply: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (343) $false % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (343) is inconsistent. % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (344) all_254_0 = 0 & all_222_0 = 0 & ~ (all_254_1 = % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_254_2) & ~ (all_35_0 = xm) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (344) implies: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (345) all_222_0 = 0 % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (299), (345) imply: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (346) $false % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (346) is inconsistent. % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | (347) ~ (all_222_1 = 0) | ~ (all_222_2 = 0) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (347) gives: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (348) ~ (all_222_1 = 0) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (298), (348) imply: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (349) $false % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (349) is inconsistent. % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (350) ~ (all_222_2 = 0) % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (297), (350) imply: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (351) $false % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (351) is inconsistent. % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | End of split % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | End of split % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | End of split % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | End of split % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | End of split % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | Case 2: % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | % 19.03/3.37 | | | | | | | | | | | | | | | | | | | | (352) ~ (all_66_0 = 0) % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | BETA: splitting (228) gives: % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | Case 1: % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | | % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | | (353) ~ (all_66_2 = 0) % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | | % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | | REDUCE: (224), (353) imply: % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | | (354) $false % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | | % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | | CLOSE: (354) is inconsistent. % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | | % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | Case 2: % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | | % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | | (355) all_66_0 = 0 & ~ (xq = xp) % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | | % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | | ALPHA: (355) implies: % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | | (356) all_66_0 = 0 % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | | % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | | REDUCE: (352), (356) imply: % 19.41/3.37 | | | | | | | | | | | | | | | | | | | | | (357) $false % 19.41/3.38 | | | | | | | | | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | | | | | | | | | CLOSE: (357) is inconsistent. % 19.41/3.38 | | | | | | | | | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | | | | | | | | End of split % 19.41/3.38 | | | | | | | | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | | | | | | | End of split % 19.41/3.38 | | | | | | | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | | | | | | End of split % 19.41/3.38 | | | | | | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | | | | | End of split % 19.41/3.38 | | | | | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | | | | End of split % 19.41/3.38 | | | | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | | | Case 2: % 19.41/3.38 | | | | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | | | | (358) ? [v0: int] : ( ~ (v0 = 0) & % 19.41/3.38 | | | | | | | | | | | | | | | | aNaturalNumber0(all_103_0) = v0) % 19.41/3.38 | | | | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | | | | DELTA: instantiating (358) with fresh symbol all_151_0 % 19.41/3.38 | | | | | | | | | | | | | | | | gives: % 19.41/3.38 | | | | | | | | | | | | | | | | (359) ~ (all_151_0 = 0) & aNaturalNumber0(all_103_0) = % 19.41/3.38 | | | | | | | | | | | | | | | | all_151_0 % 19.41/3.38 | | | | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | | | | ALPHA: (359) implies: % 19.41/3.38 | | | | | | | | | | | | | | | | (360) ~ (all_151_0 = 0) % 19.41/3.38 | | | | | | | | | | | | | | | | (361) aNaturalNumber0(all_103_0) = all_151_0 % 19.41/3.38 | | | | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_151_0, all_103_0, % 19.41/3.38 | | | | | | | | | | | | | | | | simplifying with (141), (361) gives: % 19.41/3.38 | | | | | | | | | | | | | | | | (362) all_151_0 = 0 % 19.41/3.38 | | | | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | | | | REDUCE: (360), (362) imply: % 19.41/3.38 | | | | | | | | | | | | | | | | (363) $false % 19.41/3.38 | | | | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | | | | CLOSE: (363) is inconsistent. % 19.41/3.38 | | | | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | | | End of split % 19.41/3.38 | | | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | | End of split % 19.41/3.38 | | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | End of split % 19.41/3.38 | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | Case 2: % 19.41/3.38 | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | (364) ? [v0: int] : ( ~ (v0 = 0) & % 19.41/3.38 | | | | | | | | | | | | | aNaturalNumber0(all_87_0) = v0) % 19.41/3.38 | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | DELTA: instantiating (364) with fresh symbol all_131_0 % 19.41/3.38 | | | | | | | | | | | | | gives: % 19.41/3.38 | | | | | | | | | | | | | (365) ~ (all_131_0 = 0) & aNaturalNumber0(all_87_0) = % 19.41/3.38 | | | | | | | | | | | | | all_131_0 % 19.41/3.38 | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | ALPHA: (365) implies: % 19.41/3.38 | | | | | | | | | | | | | (366) ~ (all_131_0 = 0) % 19.41/3.38 | | | | | | | | | | | | | (367) aNaturalNumber0(all_87_0) = all_131_0 % 19.41/3.38 | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | GROUND_INST: instantiating (18) with 0, all_131_0, all_87_0, % 19.41/3.38 | | | | | | | | | | | | | simplifying with (118), (367) gives: % 19.41/3.38 | | | | | | | | | | | | | (368) all_131_0 = 0 % 19.41/3.38 | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | REDUCE: (366), (368) imply: % 19.41/3.38 | | | | | | | | | | | | | (369) $false % 19.41/3.38 | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | | CLOSE: (369) is inconsistent. % 19.41/3.38 | | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | | End of split % 19.41/3.38 | | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | | End of split % 19.41/3.38 | | | | | | | | | | | % 19.41/3.38 | | | | | | | | | | End of split % 19.41/3.38 | | | | | | | | | | % 19.41/3.38 | | | | | | | | | End of split % 19.41/3.38 | | | | | | | | | % 19.41/3.38 | | | | | | | | End of split % 19.41/3.38 | | | | | | | | % 19.41/3.38 | | | | | | | End of split % 19.41/3.38 | | | | | | | % 19.41/3.38 | | | | | | End of split % 19.41/3.38 | | | | | | % 19.41/3.38 | | | | | End of split % 19.41/3.38 | | | | | % 19.41/3.38 | | | | End of split % 19.41/3.38 | | | | % 19.41/3.38 | | | End of split % 19.41/3.38 | | | % 19.41/3.38 | | End of split % 19.41/3.38 | | % 19.41/3.38 | End of split % 19.41/3.38 | % 19.41/3.38 End of proof % 19.41/3.38 % SZS output end Proof for theBenchmark % 19.41/3.38 % 19.41/3.38 2804ms %------------------------------------------------------------------------------