%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : RNG070+2 : 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 13:57:40 EDT 2023 % Result : Theorem 12.73s 2.44s % Output : Proof 21.63s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : RNG070+2 : TPTP v8.1.2. Released v4.0.0. % 0.11/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.33 % Computer : n023.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Sun Aug 27 02:06:56 EDT 2023 % 0.13/0.33 % CPUTime : % 0.66/0.62 ________ _____ % 0.66/0.62 ___ __ \_________(_)________________________________ % 0.66/0.62 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.66/0.62 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.66/0.62 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.66/0.62 % 0.66/0.63 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.66/0.63 (2023-06-19) % 0.66/0.63 % 0.66/0.63 (c) Philipp Rümmer, 2009-2023 % 0.66/0.63 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.66/0.63 Amanda Stjerna. % 0.66/0.63 Free software under BSD-3-Clause. % 0.66/0.63 % 0.66/0.63 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.66/0.63 % 0.66/0.63 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.69/0.65 Running up to 7 provers in parallel. % 0.69/0.66 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.69/0.66 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.69/0.66 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.69/0.66 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.69/0.66 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.69/0.66 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.69/0.66 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 3.54/1.22 Prover 1: Preprocessing ... % 3.54/1.22 Prover 4: Preprocessing ... % 3.76/1.26 Prover 3: Preprocessing ... % 3.76/1.26 Prover 6: Preprocessing ... % 3.76/1.26 Prover 0: Preprocessing ... % 3.76/1.26 Prover 5: Preprocessing ... % 3.76/1.26 Prover 2: Preprocessing ... % 9.42/2.00 Prover 1: Constructing countermodel ... % 9.42/2.03 Prover 6: Proving ... % 9.42/2.04 Prover 3: Constructing countermodel ... % 11.15/2.23 Prover 5: Constructing countermodel ... % 11.78/2.33 Prover 4: Constructing countermodel ... % 12.73/2.43 Prover 2: Proving ... % 12.73/2.43 Prover 3: proved (1764ms) % 12.73/2.44 % 12.73/2.44 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 12.73/2.44 % 12.73/2.45 Prover 5: stopped % 12.73/2.45 Prover 6: stopped % 12.73/2.45 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 12.73/2.45 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 12.73/2.45 Prover 2: stopped % 12.73/2.46 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 12.73/2.46 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 12.73/2.50 Prover 0: Proving ... % 13.43/2.51 Prover 0: stopped % 13.43/2.54 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 13.43/2.58 Prover 11: Preprocessing ... % 14.01/2.61 Prover 8: Preprocessing ... % 14.01/2.61 Prover 7: Preprocessing ... % 14.01/2.63 Prover 10: Preprocessing ... % 14.01/2.63 Prover 13: Preprocessing ... % 15.79/2.85 Prover 8: Warning: ignoring some quantifiers % 15.79/2.85 Prover 8: Constructing countermodel ... % 15.79/2.86 Prover 10: Constructing countermodel ... % 15.79/2.86 Prover 13: Constructing countermodel ... % 15.79/2.87 Prover 7: Constructing countermodel ... % 17.42/3.05 Prover 11: Constructing countermodel ... % 20.47/3.46 Prover 1: Found proof (size 237) % 20.47/3.47 Prover 1: proved (2812ms) % 20.47/3.47 Prover 10: stopped % 20.47/3.47 Prover 4: stopped % 20.47/3.47 Prover 8: stopped % 20.47/3.47 Prover 11: stopped % 20.47/3.47 Prover 13: stopped % 20.87/3.48 Prover 7: stopped % 20.87/3.48 % 20.87/3.48 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 20.87/3.48 % 20.87/3.52 % SZS output start Proof for theBenchmark % 20.87/3.53 Assumptions after simplification: % 20.87/3.53 --------------------------------- % 20.87/3.53 % 20.87/3.53 (mDistr) % 20.87/3.55 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 21.22/3.55 $i] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ % 21.22/3.56 (sdtpldt0(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : % 21.22/3.56 ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? % 21.22/3.56 [v12: $i] : ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v11, v2) = v12 & % 21.22/3.56 sdtasdt0(v1, v2) = v13 & sdtasdt0(v0, v9) = v10 & sdtpldt0(v4, v13) = v14 % 21.22/3.56 & sdtpldt0(v1, v2) = v9 & sdtpldt0(v0, v1) = v11 & aScalar0(v2) = v8 & % 21.22/3.56 aScalar0(v1) = v7 & aScalar0(v0) = v6 & $i(v14) & $i(v13) & $i(v12) & % 21.22/3.56 $i(v11) & $i(v10) & $i(v9) & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | % 21.22/3.56 (v14 = v12 & v10 = v5)))) % 21.22/3.56 % 21.22/3.56 (mLEMon) % 21.22/3.56 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 21.22/3.56 $i] : ! [v6: int] : (v6 = 0 | ~ (sdtlseqdt0(v4, v5) = v6) | ~ % 21.22/3.56 (sdtpldt0(v1, v3) = v5) | ~ (sdtpldt0(v0, v2) = v4) | ~ $i(v3) | ~ $i(v2) % 21.22/3.56 | ~ $i(v1) | ~ $i(v0) | ? [v7: any] : ? [v8: any] : ? [v9: any] : ? % 21.22/3.56 [v10: any] : ? [v11: any] : ? [v12: any] : (sdtlseqdt0(v2, v3) = v12 & % 21.22/3.56 sdtlseqdt0(v0, v1) = v11 & aScalar0(v3) = v10 & aScalar0(v2) = v9 & % 21.22/3.56 aScalar0(v1) = v8 & aScalar0(v0) = v7 & ( ~ (v12 = 0) | ~ (v11 = 0) | ~ % 21.22/3.56 (v10 = 0) | ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0)))) % 21.22/3.56 % 21.22/3.56 (mLETot) % 21.22/3.56 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (sdtlseqdt0(v0, v1) = % 21.22/3.56 v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 21.22/3.56 (sdtlseqdt0(v1, v0) = v5 & aScalar0(v1) = v4 & aScalar0(v0) = v3 & ( ~ (v4 = % 21.22/3.56 0) | ~ (v3 = 0) | v5 = 0))) % 21.22/3.56 % 21.22/3.56 (mMulSc) % 21.22/3.56 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 21.22/3.56 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 21.22/3.56 (aScalar0(v2) = v5 & aScalar0(v1) = v4 & aScalar0(v0) = v3 & ( ~ (v4 = 0) | % 21.22/3.56 ~ (v3 = 0) | v5 = 0))) % 21.22/3.56 % 21.22/3.56 (mSqPos) % 21.22/3.56 $i(sz0z00) & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtasdt0(v0, v0) = v1) | ~ % 21.22/3.57 $i(v0) | ? [v2: any] : ? [v3: any] : (sdtlseqdt0(sz0z00, v1) = v3 & % 21.22/3.57 aScalar0(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 21.22/3.57 % 21.22/3.57 (mSumSc) % 21.22/3.57 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 21.22/3.57 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 21.22/3.57 (aScalar0(v2) = v5 & aScalar0(v1) = v4 & aScalar0(v0) = v3 & ( ~ (v4 = 0) | % 21.22/3.57 ~ (v3 = 0) | v5 = 0))) % 21.22/3.57 % 21.22/3.57 (m__) % 21.22/3.57 $i(xS) & $i(xP) & $i(xR) & ? [v0: $i] : ? [v1: $i] : ? [v2: int] : ( ~ (v2 % 21.22/3.57 = 0) & sdtlseqdt0(v0, v1) = v2 & sdtpldt0(xP, xP) = v1 & sdtpldt0(xR, xS) % 21.22/3.57 = v0 & $i(v1) & $i(v0)) % 21.22/3.57 % 21.22/3.57 (m__1892) % 21.22/3.57 sdtasdt0(xC, xG) = xR & aScalar0(xR) = 0 & $i(xR) & $i(xG) & $i(xC) % 21.22/3.57 % 21.22/3.57 (m__1911) % 21.22/3.57 sdtasdt0(xE, xH) = xP & aScalar0(xP) = 0 & $i(xP) & $i(xH) & $i(xE) % 21.22/3.57 % 21.22/3.57 (m__1930) % 21.22/3.57 sdtasdt0(xF, xD) = xS & aScalar0(xS) = 0 & $i(xS) & $i(xF) & $i(xD) % 21.22/3.57 % 21.22/3.57 (m__2004) % 21.22/3.57 $i(xN) & $i(xP) & ? [v0: $i] : (sdtlseqdt0(v0, xN) = 0 & sdtasdt0(xP, xP) = % 21.22/3.57 v0 & $i(v0)) % 21.22/3.57 % 21.22/3.57 (m__2104) % 21.22/3.57 $i(xS) & $i(xP) & $i(xR) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 21.22/3.57 $i] : ? [v4: $i] : (sdtlseqdt0(v1, v4) = 0 & sdtasdt0(xS, xS) = v3 & % 21.22/3.57 sdtasdt0(xP, xP) = v0 & sdtasdt0(xR, xR) = v2 & sdtpldt0(v2, v3) = v4 & % 21.22/3.57 sdtpldt0(v0, v0) = v1 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 21.22/3.57 % 21.22/3.57 (m__2405) % 21.22/3.57 $i(xS) & $i(xP) & $i(xR) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 21.22/3.57 $i] : (sdtlseqdt0(v1, v3) = 0 & sdtasdt0(v2, v2) = v3 & sdtasdt0(v0, v0) = % 21.22/3.57 v1 & sdtpldt0(xP, xP) = v0 & sdtpldt0(xR, xS) = v2 & $i(v3) & $i(v2) & % 21.22/3.57 $i(v1) & $i(v0)) % 21.22/3.57 % 21.22/3.57 (m__2590) % 21.22/3.57 $i(xS) & $i(xP) & $i(xR) & ? [v0: $i] : ? [v1: $i] : ? [v2: int] : ( ~ (v2 % 21.22/3.57 = 0) & sdtlseqdt0(v0, v1) = v2 & sdtpldt0(xP, xP) = v0 & sdtpldt0(xR, xS) % 21.22/3.57 = v1 & $i(v1) & $i(v0)) % 21.22/3.57 % 21.22/3.57 (function-axioms) % 21.31/3.58 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 21.31/3.58 (sdtasasdt0(v3, v2) = v1) | ~ (sdtasasdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 21.31/3.58 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtlbdtrb0(v3, v2) = v1) % 21.31/3.58 | ~ (sdtlbdtrb0(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 21.31/3.58 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 21.31/3.58 (sdtlseqdt0(v3, v2) = v1) | ~ (sdtlseqdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 21.31/3.58 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) | % 21.31/3.58 ~ (sdtasdt0(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 21.31/3.58 [v3: $i] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 21.31/3.58 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 21.31/3.58 [v3: $i] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) & % 21.31/3.58 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (sziznziztdt0(v2) = v1) % 21.31/3.58 | ~ (sziznziztdt0(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 21.31/3.58 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aVector0(v2) = v1) | ~ % 21.31/3.58 (aVector0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | % 21.31/3.58 ~ (aDimensionOf0(v2) = v1) | ~ (aDimensionOf0(v2) = v0)) & ! [v0: $i] : ! % 21.31/3.58 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (smndt0(v2) = v1) | ~ (smndt0(v2) = % 21.31/3.58 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 21.31/3.58 $i] : (v1 = v0 | ~ (aScalar0(v2) = v1) | ~ (aScalar0(v2) = v0)) & ! [v0: % 21.31/3.58 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (szszuzczcdt0(v2) = v1) | ~ % 21.31/3.58 (szszuzczcdt0(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 21.31/3.58 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) % 21.31/3.58 | ~ (aNaturalNumber0(v2) = v0)) % 21.31/3.58 % 21.31/3.58 Further assumptions not needed in the proof: % 21.31/3.58 -------------------------------------------- % 21.31/3.58 mArith, mDefInit, mDefSPN, mDefSPZ, mDimNat, mDistr2, mElmSc, mEqInit, mIH, % 21.31/3.58 mIHOrd, mLEASm, mLEMonM, mLERef, mLETrn, mLess, mMDNeg, mMNeg, mNatExtr, % 21.31/3.58 mNatSort, mNegSc, mPosMon, mSZeroSc, mScPr, mScSort, mScSqPos, mScZero, mSqrt, % 21.31/3.58 mSuccEqu, mSuccNat, mVcSort, mZeroNat, m__1652, m__1678, m__1678_01, m__1692, % 21.31/3.58 m__1709, m__1726, m__1746, m__1766, m__1783, m__1800, m__1820, m__1837, m__1854, % 21.31/3.58 m__1873, m__1949, m__1967 % 21.31/3.58 % 21.31/3.58 Those formulas are unsatisfiable: % 21.31/3.58 --------------------------------- % 21.31/3.58 % 21.31/3.58 Begin of proof % 21.31/3.58 | % 21.31/3.58 | ALPHA: (mSqPos) implies: % 21.31/3.58 | (1) ! [v0: $i] : ! [v1: $i] : ( ~ (sdtasdt0(v0, v0) = v1) | ~ $i(v0) | % 21.31/3.58 | ? [v2: any] : ? [v3: any] : (sdtlseqdt0(sz0z00, v1) = v3 & % 21.31/3.58 | aScalar0(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 21.31/3.58 | % 21.31/3.58 | ALPHA: (m__1892) implies: % 21.31/3.58 | (2) aScalar0(xR) = 0 % 21.31/3.58 | % 21.31/3.58 | ALPHA: (m__1911) implies: % 21.31/3.58 | (3) aScalar0(xP) = 0 % 21.31/3.58 | % 21.31/3.58 | ALPHA: (m__1930) implies: % 21.31/3.58 | (4) aScalar0(xS) = 0 % 21.31/3.58 | % 21.31/3.58 | ALPHA: (m__2004) implies: % 21.31/3.58 | (5) ? [v0: $i] : (sdtlseqdt0(v0, xN) = 0 & sdtasdt0(xP, xP) = v0 & $i(v0)) % 21.31/3.58 | % 21.31/3.58 | ALPHA: (m__2104) implies: % 21.31/3.59 | (6) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 21.31/3.59 | (sdtlseqdt0(v1, v4) = 0 & sdtasdt0(xS, xS) = v3 & sdtasdt0(xP, xP) = v0 % 21.31/3.59 | & sdtasdt0(xR, xR) = v2 & sdtpldt0(v2, v3) = v4 & sdtpldt0(v0, v0) = % 21.31/3.59 | v1 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 21.31/3.59 | % 21.31/3.59 | ALPHA: (m__2405) implies: % 21.31/3.59 | (7) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (sdtlseqdt0(v1, % 21.31/3.59 | v3) = 0 & sdtasdt0(v2, v2) = v3 & sdtasdt0(v0, v0) = v1 & % 21.31/3.59 | sdtpldt0(xP, xP) = v0 & sdtpldt0(xR, xS) = v2 & $i(v3) & $i(v2) & % 21.31/3.59 | $i(v1) & $i(v0)) % 21.31/3.59 | % 21.31/3.59 | ALPHA: (m__2590) implies: % 21.31/3.59 | (8) ? [v0: $i] : ? [v1: $i] : ? [v2: int] : ( ~ (v2 = 0) & % 21.31/3.59 | sdtlseqdt0(v0, v1) = v2 & sdtpldt0(xP, xP) = v0 & sdtpldt0(xR, xS) = % 21.31/3.59 | v1 & $i(v1) & $i(v0)) % 21.31/3.59 | % 21.31/3.59 | ALPHA: (m__) implies: % 21.31/3.59 | (9) $i(xR) % 21.31/3.59 | (10) $i(xP) % 21.31/3.59 | (11) $i(xS) % 21.31/3.59 | (12) ? [v0: $i] : ? [v1: $i] : ? [v2: int] : ( ~ (v2 = 0) & % 21.31/3.59 | sdtlseqdt0(v0, v1) = v2 & sdtpldt0(xP, xP) = v1 & sdtpldt0(xR, xS) = % 21.31/3.59 | v0 & $i(v1) & $i(v0)) % 21.31/3.59 | % 21.31/3.59 | ALPHA: (function-axioms) implies: % 21.31/3.59 | (13) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 21.31/3.59 | : (v1 = v0 | ~ (aScalar0(v2) = v1) | ~ (aScalar0(v2) = v0)) % 21.31/3.59 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 21.31/3.59 | (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 21.31/3.59 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 21.31/3.59 | (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 21.31/3.59 | (16) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 21.31/3.59 | : ! [v3: $i] : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ % 21.31/3.59 | (sdtlseqdt0(v3, v2) = v0)) % 21.31/3.59 | % 21.31/3.59 | DELTA: instantiating (5) with fresh symbol all_35_0 gives: % 21.31/3.59 | (17) sdtlseqdt0(all_35_0, xN) = 0 & sdtasdt0(xP, xP) = all_35_0 & % 21.31/3.59 | $i(all_35_0) % 21.31/3.59 | % 21.31/3.59 | ALPHA: (17) implies: % 21.31/3.59 | (18) sdtasdt0(xP, xP) = all_35_0 % 21.31/3.59 | % 21.31/3.59 | DELTA: instantiating (8) with fresh symbols all_45_0, all_45_1, all_45_2 % 21.31/3.59 | gives: % 21.31/3.59 | (19) ~ (all_45_0 = 0) & sdtlseqdt0(all_45_2, all_45_1) = all_45_0 & % 21.31/3.59 | sdtpldt0(xP, xP) = all_45_2 & sdtpldt0(xR, xS) = all_45_1 & % 21.31/3.59 | $i(all_45_1) & $i(all_45_2) % 21.31/3.59 | % 21.31/3.59 | ALPHA: (19) implies: % 21.31/3.59 | (20) ~ (all_45_0 = 0) % 21.31/3.59 | (21) sdtpldt0(xR, xS) = all_45_1 % 21.31/3.59 | (22) sdtpldt0(xP, xP) = all_45_2 % 21.31/3.59 | (23) sdtlseqdt0(all_45_2, all_45_1) = all_45_0 % 21.31/3.59 | % 21.31/3.59 | DELTA: instantiating (12) with fresh symbols all_47_0, all_47_1, all_47_2 % 21.31/3.59 | gives: % 21.31/3.59 | (24) ~ (all_47_0 = 0) & sdtlseqdt0(all_47_2, all_47_1) = all_47_0 & % 21.31/3.59 | sdtpldt0(xP, xP) = all_47_1 & sdtpldt0(xR, xS) = all_47_2 & % 21.31/3.59 | $i(all_47_1) & $i(all_47_2) % 21.31/3.59 | % 21.31/3.59 | ALPHA: (24) implies: % 21.31/3.60 | (25) ~ (all_47_0 = 0) % 21.31/3.60 | (26) $i(all_47_2) % 21.31/3.60 | (27) $i(all_47_1) % 21.31/3.60 | (28) sdtpldt0(xR, xS) = all_47_2 % 21.31/3.60 | (29) sdtpldt0(xP, xP) = all_47_1 % 21.31/3.60 | (30) sdtlseqdt0(all_47_2, all_47_1) = all_47_0 % 21.31/3.60 | % 21.31/3.60 | DELTA: instantiating (7) with fresh symbols all_49_0, all_49_1, all_49_2, % 21.31/3.60 | all_49_3 gives: % 21.31/3.60 | (31) sdtlseqdt0(all_49_2, all_49_0) = 0 & sdtasdt0(all_49_1, all_49_1) = % 21.31/3.60 | all_49_0 & sdtasdt0(all_49_3, all_49_3) = all_49_2 & sdtpldt0(xP, xP) % 21.31/3.60 | = all_49_3 & sdtpldt0(xR, xS) = all_49_1 & $i(all_49_0) & $i(all_49_1) % 21.31/3.60 | & $i(all_49_2) & $i(all_49_3) % 21.31/3.60 | % 21.31/3.60 | ALPHA: (31) implies: % 21.31/3.60 | (32) sdtpldt0(xR, xS) = all_49_1 % 21.31/3.60 | (33) sdtpldt0(xP, xP) = all_49_3 % 21.31/3.60 | (34) sdtasdt0(all_49_3, all_49_3) = all_49_2 % 21.31/3.60 | (35) sdtasdt0(all_49_1, all_49_1) = all_49_0 % 21.31/3.60 | % 21.31/3.60 | DELTA: instantiating (6) with fresh symbols all_51_0, all_51_1, all_51_2, % 21.31/3.60 | all_51_3, all_51_4 gives: % 21.31/3.60 | (36) sdtlseqdt0(all_51_3, all_51_0) = 0 & sdtasdt0(xS, xS) = all_51_1 & % 21.31/3.60 | sdtasdt0(xP, xP) = all_51_4 & sdtasdt0(xR, xR) = all_51_2 & % 21.31/3.60 | sdtpldt0(all_51_2, all_51_1) = all_51_0 & sdtpldt0(all_51_4, all_51_4) % 21.31/3.60 | = all_51_3 & $i(all_51_0) & $i(all_51_1) & $i(all_51_2) & $i(all_51_3) % 21.31/3.60 | & $i(all_51_4) % 21.31/3.60 | % 21.31/3.60 | ALPHA: (36) implies: % 21.31/3.60 | (37) sdtpldt0(all_51_4, all_51_4) = all_51_3 % 21.31/3.60 | (38) sdtasdt0(xR, xR) = all_51_2 % 21.31/3.60 | (39) sdtasdt0(xP, xP) = all_51_4 % 21.31/3.60 | (40) sdtasdt0(xS, xS) = all_51_1 % 21.31/3.60 | % 21.31/3.60 | GROUND_INST: instantiating (14) with all_47_2, all_49_1, xS, xR, simplifying % 21.31/3.60 | with (28), (32) gives: % 21.31/3.60 | (41) all_49_1 = all_47_2 % 21.31/3.60 | % 21.31/3.60 | GROUND_INST: instantiating (14) with all_45_1, all_49_1, xS, xR, simplifying % 21.31/3.60 | with (21), (32) gives: % 21.31/3.60 | (42) all_49_1 = all_45_1 % 21.31/3.60 | % 21.31/3.60 | GROUND_INST: instantiating (14) with all_47_1, all_49_3, xP, xP, simplifying % 21.31/3.60 | with (29), (33) gives: % 21.31/3.60 | (43) all_49_3 = all_47_1 % 21.31/3.60 | % 21.31/3.60 | GROUND_INST: instantiating (14) with all_45_2, all_49_3, xP, xP, simplifying % 21.31/3.60 | with (22), (33) gives: % 21.31/3.60 | (44) all_49_3 = all_45_2 % 21.31/3.60 | % 21.31/3.60 | GROUND_INST: instantiating (15) with all_35_0, all_51_4, xP, xP, simplifying % 21.31/3.60 | with (18), (39) gives: % 21.31/3.60 | (45) all_51_4 = all_35_0 % 21.31/3.60 | % 21.31/3.60 | COMBINE_EQS: (41), (42) imply: % 21.31/3.60 | (46) all_47_2 = all_45_1 % 21.31/3.60 | % 21.31/3.60 | SIMP: (46) implies: % 21.31/3.60 | (47) all_47_2 = all_45_1 % 21.31/3.60 | % 21.31/3.60 | COMBINE_EQS: (43), (44) imply: % 21.31/3.60 | (48) all_47_1 = all_45_2 % 21.31/3.60 | % 21.31/3.60 | SIMP: (48) implies: % 21.31/3.60 | (49) all_47_1 = all_45_2 % 21.31/3.60 | % 21.31/3.60 | REDUCE: (30), (47), (49) imply: % 21.31/3.60 | (50) sdtlseqdt0(all_45_1, all_45_2) = all_47_0 % 21.31/3.60 | % 21.31/3.60 | REDUCE: (35), (42) imply: % 21.31/3.60 | (51) sdtasdt0(all_45_1, all_45_1) = all_49_0 % 21.31/3.60 | % 21.31/3.60 | REDUCE: (34), (44) imply: % 21.31/3.60 | (52) sdtasdt0(all_45_2, all_45_2) = all_49_2 % 21.31/3.60 | % 21.31/3.60 | REDUCE: (37), (45) imply: % 21.31/3.60 | (53) sdtpldt0(all_35_0, all_35_0) = all_51_3 % 21.31/3.60 | % 21.31/3.60 | REDUCE: (27), (49) imply: % 21.31/3.60 | (54) $i(all_45_2) % 21.31/3.60 | % 21.31/3.60 | REDUCE: (26), (47) imply: % 21.31/3.60 | (55) $i(all_45_1) % 21.31/3.60 | % 21.31/3.61 | GROUND_INST: instantiating (mSumSc) with xR, xS, all_45_1, simplifying with % 21.31/3.61 | (9), (11), (21) gives: % 21.31/3.61 | (56) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aScalar0(all_45_1) = v2 % 21.31/3.61 | & aScalar0(xS) = v1 & aScalar0(xR) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) % 21.31/3.61 | | v2 = 0)) % 21.31/3.61 | % 21.31/3.61 | GROUND_INST: instantiating (mSumSc) with xP, xP, all_45_2, simplifying with % 21.31/3.61 | (10), (22) gives: % 21.31/3.61 | (57) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aScalar0(all_45_2) = v2 % 21.31/3.61 | & aScalar0(xP) = v1 & aScalar0(xP) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) % 21.31/3.61 | | v2 = 0)) % 21.31/3.61 | % 21.31/3.61 | GROUND_INST: instantiating (1) with xR, all_51_2, simplifying with (9), (38) % 21.31/3.61 | gives: % 21.31/3.61 | (58) ? [v0: any] : ? [v1: any] : (sdtlseqdt0(sz0z00, all_51_2) = v1 & % 21.31/3.61 | aScalar0(xR) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 21.31/3.61 | % 21.31/3.61 | GROUND_INST: instantiating (mMulSc) with xR, xR, all_51_2, simplifying with % 21.31/3.61 | (9), (38) gives: % 21.31/3.61 | (59) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aScalar0(all_51_2) = v2 % 21.31/3.61 | & aScalar0(xR) = v1 & aScalar0(xR) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) % 21.31/3.61 | | v2 = 0)) % 21.31/3.61 | % 21.31/3.61 | GROUND_INST: instantiating (mDistr) with xP, xP, xP, all_35_0, all_35_0, % 21.31/3.61 | all_51_3, simplifying with (10), (18), (53) gives: % 21.31/3.61 | (60) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: $i] % 21.31/3.61 | : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : % 21.31/3.61 | (sdtasdt0(v5, xP) = v6 & sdtasdt0(xP, v3) = v4 & sdtasdt0(xP, xP) = v7 % 21.31/3.61 | & sdtpldt0(all_35_0, v7) = v8 & sdtpldt0(xP, xP) = v5 & sdtpldt0(xP, % 21.31/3.61 | xP) = v3 & aScalar0(xP) = v2 & aScalar0(xP) = v1 & aScalar0(xP) = % 21.31/3.61 | v0 & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & ( ~ (v2 = % 21.31/3.61 | 0) | ~ (v1 = 0) | ~ (v0 = 0) | (v8 = v6 & v4 = all_51_3))) % 21.31/3.61 | % 21.31/3.61 | GROUND_INST: instantiating (1) with xP, all_35_0, simplifying with (10), (18) % 21.31/3.61 | gives: % 21.31/3.61 | (61) ? [v0: any] : ? [v1: any] : (sdtlseqdt0(sz0z00, all_35_0) = v1 & % 21.31/3.61 | aScalar0(xP) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 21.31/3.61 | % 21.31/3.61 | GROUND_INST: instantiating (mMulSc) with xP, xP, all_35_0, simplifying with % 21.31/3.61 | (10), (18) gives: % 21.31/3.61 | (62) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aScalar0(all_35_0) = v2 % 21.31/3.61 | & aScalar0(xP) = v1 & aScalar0(xP) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) % 21.31/3.61 | | v2 = 0)) % 21.31/3.61 | % 21.31/3.61 | GROUND_INST: instantiating (1) with xS, all_51_1, simplifying with (11), (40) % 21.31/3.61 | gives: % 21.31/3.61 | (63) ? [v0: any] : ? [v1: any] : (sdtlseqdt0(sz0z00, all_51_1) = v1 & % 21.31/3.61 | aScalar0(xS) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 21.31/3.61 | % 21.31/3.61 | GROUND_INST: instantiating (mMulSc) with xS, xS, all_51_1, simplifying with % 21.31/3.61 | (11), (40) gives: % 21.31/3.61 | (64) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aScalar0(all_51_1) = v2 % 21.31/3.61 | & aScalar0(xS) = v1 & aScalar0(xS) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) % 21.31/3.61 | | v2 = 0)) % 21.31/3.61 | % 21.31/3.62 | GROUND_INST: instantiating (1) with all_45_2, all_49_2, simplifying with (52), % 21.31/3.62 | (54) gives: % 21.52/3.62 | (65) ? [v0: any] : ? [v1: any] : (sdtlseqdt0(sz0z00, all_49_2) = v1 & % 21.52/3.62 | aScalar0(all_45_2) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 21.52/3.62 | % 21.52/3.62 | GROUND_INST: instantiating (mMulSc) with all_45_2, all_45_2, all_49_2, % 21.52/3.62 | simplifying with (52), (54) gives: % 21.52/3.62 | (66) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aScalar0(all_49_2) = v2 % 21.52/3.62 | & aScalar0(all_45_2) = v1 & aScalar0(all_45_2) = v0 & ( ~ (v1 = 0) | % 21.52/3.62 | ~ (v0 = 0) | v2 = 0)) % 21.52/3.62 | % 21.52/3.62 | GROUND_INST: instantiating (1) with all_45_1, all_49_0, simplifying with (51), % 21.52/3.62 | (55) gives: % 21.52/3.62 | (67) ? [v0: any] : ? [v1: any] : (sdtlseqdt0(sz0z00, all_49_0) = v1 & % 21.52/3.62 | aScalar0(all_45_1) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 21.52/3.62 | % 21.52/3.62 | GROUND_INST: instantiating (mMulSc) with all_45_1, all_45_1, all_49_0, % 21.52/3.62 | simplifying with (51), (55) gives: % 21.52/3.62 | (68) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aScalar0(all_49_0) = v2 % 21.52/3.62 | & aScalar0(all_45_1) = v1 & aScalar0(all_45_1) = v0 & ( ~ (v1 = 0) | % 21.52/3.62 | ~ (v0 = 0) | v2 = 0)) % 21.52/3.62 | % 21.52/3.62 | GROUND_INST: instantiating (mLEMon) with xP, xR, xP, xS, all_45_2, all_45_1, % 21.52/3.62 | all_45_0, simplifying with (9), (10), (11), (21), (22), (23) % 21.52/3.62 | gives: % 21.52/3.62 | (69) all_45_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: % 21.52/3.62 | any] : ? [v4: any] : ? [v5: any] : (sdtlseqdt0(xP, xS) = v5 & % 21.52/3.62 | sdtlseqdt0(xP, xR) = v4 & aScalar0(xS) = v3 & aScalar0(xP) = v2 & % 21.52/3.62 | aScalar0(xP) = v0 & aScalar0(xR) = v1 & ( ~ (v5 = 0) | ~ (v4 = 0) | % 21.52/3.62 | ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 21.52/3.62 | % 21.52/3.62 | GROUND_INST: instantiating (mLETot) with all_45_2, all_45_1, all_45_0, % 21.52/3.62 | simplifying with (23), (54), (55) gives: % 21.52/3.62 | (70) all_45_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 21.52/3.62 | (sdtlseqdt0(all_45_1, all_45_2) = v2 & aScalar0(all_45_1) = v1 & % 21.52/3.62 | aScalar0(all_45_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 21.52/3.62 | % 21.52/3.62 | GROUND_INST: instantiating (mLEMon) with xR, xP, xS, xP, all_45_1, all_45_2, % 21.52/3.62 | all_47_0, simplifying with (9), (10), (11), (21), (22), (50) % 21.52/3.62 | gives: % 21.52/3.62 | (71) all_47_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: % 21.52/3.62 | any] : ? [v4: any] : ? [v5: any] : (sdtlseqdt0(xS, xP) = v5 & % 21.52/3.62 | sdtlseqdt0(xR, xP) = v4 & aScalar0(xS) = v2 & aScalar0(xP) = v3 & % 21.52/3.62 | aScalar0(xP) = v1 & aScalar0(xR) = v0 & ( ~ (v5 = 0) | ~ (v4 = 0) | % 21.52/3.62 | ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 21.52/3.62 | % 21.52/3.62 | GROUND_INST: instantiating (mLETot) with all_45_1, all_45_2, all_47_0, % 21.52/3.62 | simplifying with (50), (54), (55) gives: % 21.52/3.63 | (72) all_47_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 21.52/3.63 | (sdtlseqdt0(all_45_2, all_45_1) = v2 & aScalar0(all_45_1) = v0 & % 21.52/3.63 | aScalar0(all_45_2) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 21.52/3.63 | % 21.52/3.63 | DELTA: instantiating (58) with fresh symbols all_86_0, all_86_1 gives: % 21.52/3.63 | (73) sdtlseqdt0(sz0z00, all_51_2) = all_86_0 & aScalar0(xR) = all_86_1 & ( % 21.52/3.63 | ~ (all_86_1 = 0) | all_86_0 = 0) % 21.52/3.63 | % 21.52/3.63 | ALPHA: (73) implies: % 21.52/3.63 | (74) aScalar0(xR) = all_86_1 % 21.52/3.63 | % 21.52/3.63 | DELTA: instantiating (67) with fresh symbols all_90_0, all_90_1 gives: % 21.52/3.63 | (75) sdtlseqdt0(sz0z00, all_49_0) = all_90_0 & aScalar0(all_45_1) = % 21.52/3.63 | all_90_1 & ( ~ (all_90_1 = 0) | all_90_0 = 0) % 21.52/3.63 | % 21.52/3.63 | ALPHA: (75) implies: % 21.52/3.63 | (76) aScalar0(all_45_1) = all_90_1 % 21.52/3.63 | % 21.52/3.63 | DELTA: instantiating (65) with fresh symbols all_92_0, all_92_1 gives: % 21.52/3.63 | (77) sdtlseqdt0(sz0z00, all_49_2) = all_92_0 & aScalar0(all_45_2) = % 21.52/3.63 | all_92_1 & ( ~ (all_92_1 = 0) | all_92_0 = 0) % 21.52/3.63 | % 21.52/3.63 | ALPHA: (77) implies: % 21.52/3.63 | (78) aScalar0(all_45_2) = all_92_1 % 21.52/3.63 | % 21.52/3.63 | DELTA: instantiating (63) with fresh symbols all_98_0, all_98_1 gives: % 21.52/3.63 | (79) sdtlseqdt0(sz0z00, all_51_1) = all_98_0 & aScalar0(xS) = all_98_1 & ( % 21.52/3.63 | ~ (all_98_1 = 0) | all_98_0 = 0) % 21.52/3.63 | % 21.52/3.63 | ALPHA: (79) implies: % 21.52/3.63 | (80) aScalar0(xS) = all_98_1 % 21.52/3.63 | % 21.52/3.63 | DELTA: instantiating (61) with fresh symbols all_100_0, all_100_1 gives: % 21.52/3.63 | (81) sdtlseqdt0(sz0z00, all_35_0) = all_100_0 & aScalar0(xP) = all_100_1 & % 21.52/3.63 | ( ~ (all_100_1 = 0) | all_100_0 = 0) % 21.52/3.63 | % 21.52/3.63 | ALPHA: (81) implies: % 21.52/3.63 | (82) aScalar0(xP) = all_100_1 % 21.52/3.63 | % 21.52/3.63 | DELTA: instantiating (59) with fresh symbols all_110_0, all_110_1, all_110_2 % 21.52/3.63 | gives: % 21.52/3.63 | (83) aScalar0(all_51_2) = all_110_0 & aScalar0(xR) = all_110_1 & % 21.52/3.63 | aScalar0(xR) = all_110_2 & ( ~ (all_110_1 = 0) | ~ (all_110_2 = 0) | % 21.52/3.63 | all_110_0 = 0) % 21.52/3.63 | % 21.52/3.63 | ALPHA: (83) implies: % 21.52/3.63 | (84) aScalar0(xR) = all_110_2 % 21.52/3.63 | (85) aScalar0(xR) = all_110_1 % 21.52/3.63 | % 21.52/3.63 | DELTA: instantiating (66) with fresh symbols all_116_0, all_116_1, all_116_2 % 21.52/3.63 | gives: % 21.52/3.63 | (86) aScalar0(all_49_2) = all_116_0 & aScalar0(all_45_2) = all_116_1 & % 21.52/3.63 | aScalar0(all_45_2) = all_116_2 & ( ~ (all_116_1 = 0) | ~ (all_116_2 = % 21.52/3.63 | 0) | all_116_0 = 0) % 21.52/3.63 | % 21.52/3.63 | ALPHA: (86) implies: % 21.52/3.63 | (87) aScalar0(all_45_2) = all_116_2 % 21.52/3.63 | (88) aScalar0(all_45_2) = all_116_1 % 21.52/3.63 | (89) ~ (all_116_1 = 0) | ~ (all_116_2 = 0) | all_116_0 = 0 % 21.52/3.63 | % 21.52/3.63 | DELTA: instantiating (62) with fresh symbols all_118_0, all_118_1, all_118_2 % 21.52/3.63 | gives: % 21.52/3.63 | (90) aScalar0(all_35_0) = all_118_0 & aScalar0(xP) = all_118_1 & % 21.52/3.63 | aScalar0(xP) = all_118_2 & ( ~ (all_118_1 = 0) | ~ (all_118_2 = 0) | % 21.52/3.63 | all_118_0 = 0) % 21.52/3.63 | % 21.52/3.63 | ALPHA: (90) implies: % 21.52/3.63 | (91) aScalar0(xP) = all_118_2 % 21.52/3.63 | (92) aScalar0(xP) = all_118_1 % 21.52/3.63 | % 21.52/3.63 | DELTA: instantiating (57) with fresh symbols all_124_0, all_124_1, all_124_2 % 21.52/3.63 | gives: % 21.52/3.63 | (93) aScalar0(all_45_2) = all_124_0 & aScalar0(xP) = all_124_1 & % 21.52/3.63 | aScalar0(xP) = all_124_2 & ( ~ (all_124_1 = 0) | ~ (all_124_2 = 0) | % 21.52/3.63 | all_124_0 = 0) % 21.52/3.63 | % 21.52/3.63 | ALPHA: (93) implies: % 21.52/3.63 | (94) aScalar0(xP) = all_124_2 % 21.52/3.63 | (95) aScalar0(xP) = all_124_1 % 21.52/3.63 | (96) aScalar0(all_45_2) = all_124_0 % 21.52/3.63 | (97) ~ (all_124_1 = 0) | ~ (all_124_2 = 0) | all_124_0 = 0 % 21.52/3.63 | % 21.52/3.63 | DELTA: instantiating (64) with fresh symbols all_126_0, all_126_1, all_126_2 % 21.52/3.63 | gives: % 21.52/3.63 | (98) aScalar0(all_51_1) = all_126_0 & aScalar0(xS) = all_126_1 & % 21.52/3.63 | aScalar0(xS) = all_126_2 & ( ~ (all_126_1 = 0) | ~ (all_126_2 = 0) | % 21.52/3.63 | all_126_0 = 0) % 21.52/3.63 | % 21.52/3.63 | ALPHA: (98) implies: % 21.52/3.63 | (99) aScalar0(xS) = all_126_2 % 21.52/3.63 | (100) aScalar0(xS) = all_126_1 % 21.52/3.63 | % 21.52/3.63 | DELTA: instantiating (56) with fresh symbols all_128_0, all_128_1, all_128_2 % 21.52/3.63 | gives: % 21.52/3.63 | (101) aScalar0(all_45_1) = all_128_0 & aScalar0(xS) = all_128_1 & % 21.52/3.63 | aScalar0(xR) = all_128_2 & ( ~ (all_128_1 = 0) | ~ (all_128_2 = 0) | % 21.52/3.63 | all_128_0 = 0) % 21.52/3.63 | % 21.52/3.63 | ALPHA: (101) implies: % 21.52/3.63 | (102) aScalar0(xR) = all_128_2 % 21.52/3.63 | (103) aScalar0(xS) = all_128_1 % 21.52/3.63 | (104) aScalar0(all_45_1) = all_128_0 % 21.52/3.63 | (105) ~ (all_128_1 = 0) | ~ (all_128_2 = 0) | all_128_0 = 0 % 21.52/3.63 | % 21.52/3.63 | DELTA: instantiating (68) with fresh symbols all_134_0, all_134_1, all_134_2 % 21.52/3.63 | gives: % 21.52/3.64 | (106) aScalar0(all_49_0) = all_134_0 & aScalar0(all_45_1) = all_134_1 & % 21.52/3.64 | aScalar0(all_45_1) = all_134_2 & ( ~ (all_134_1 = 0) | ~ (all_134_2 % 21.52/3.64 | = 0) | all_134_0 = 0) % 21.52/3.64 | % 21.52/3.64 | ALPHA: (106) implies: % 21.52/3.64 | (107) aScalar0(all_45_1) = all_134_2 % 21.52/3.64 | (108) aScalar0(all_45_1) = all_134_1 % 21.52/3.64 | % 21.52/3.64 | DELTA: instantiating (60) with fresh symbols all_140_0, all_140_1, all_140_2, % 21.52/3.64 | all_140_3, all_140_4, all_140_5, all_140_6, all_140_7, all_140_8 gives: % 21.52/3.64 | (109) sdtasdt0(all_140_3, xP) = all_140_2 & sdtasdt0(xP, all_140_5) = % 21.52/3.64 | all_140_4 & sdtasdt0(xP, xP) = all_140_1 & sdtpldt0(all_35_0, % 21.52/3.64 | all_140_1) = all_140_0 & sdtpldt0(xP, xP) = all_140_3 & % 21.52/3.64 | sdtpldt0(xP, xP) = all_140_5 & aScalar0(xP) = all_140_6 & % 21.52/3.64 | aScalar0(xP) = all_140_7 & aScalar0(xP) = all_140_8 & $i(all_140_0) & % 21.52/3.64 | $i(all_140_1) & $i(all_140_2) & $i(all_140_3) & $i(all_140_4) & % 21.52/3.64 | $i(all_140_5) & ( ~ (all_140_6 = 0) | ~ (all_140_7 = 0) | ~ % 21.52/3.64 | (all_140_8 = 0) | (all_140_0 = all_140_2 & all_140_4 = all_51_3)) % 21.52/3.64 | % 21.52/3.64 | ALPHA: (109) implies: % 21.52/3.64 | (110) aScalar0(xP) = all_140_8 % 21.63/3.64 | (111) aScalar0(xP) = all_140_7 % 21.63/3.64 | (112) aScalar0(xP) = all_140_6 % 21.63/3.64 | % 21.63/3.64 | BETA: splitting (71) gives: % 21.63/3.64 | % 21.63/3.64 | Case 1: % 21.63/3.64 | | % 21.63/3.64 | | (113) all_47_0 = 0 % 21.63/3.64 | | % 21.63/3.64 | | REDUCE: (25), (113) imply: % 21.63/3.64 | | (114) $false % 21.63/3.64 | | % 21.63/3.64 | | CLOSE: (114) is inconsistent. % 21.63/3.64 | | % 21.63/3.64 | Case 2: % 21.63/3.64 | | % 21.63/3.64 | | (115) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? [v4: % 21.63/3.64 | | any] : ? [v5: any] : (sdtlseqdt0(xS, xP) = v5 & sdtlseqdt0(xR, % 21.63/3.64 | | xP) = v4 & aScalar0(xS) = v2 & aScalar0(xP) = v3 & aScalar0(xP) % 21.63/3.64 | | = v1 & aScalar0(xR) = v0 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = % 21.63/3.64 | | 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 21.63/3.64 | | % 21.63/3.64 | | DELTA: instantiating (115) with fresh symbols all_152_0, all_152_1, % 21.63/3.64 | | all_152_2, all_152_3, all_152_4, all_152_5 gives: % 21.63/3.64 | | (116) sdtlseqdt0(xS, xP) = all_152_0 & sdtlseqdt0(xR, xP) = all_152_1 & % 21.63/3.64 | | aScalar0(xS) = all_152_3 & aScalar0(xP) = all_152_2 & aScalar0(xP) % 21.63/3.64 | | = all_152_4 & aScalar0(xR) = all_152_5 & ( ~ (all_152_0 = 0) | ~ % 21.63/3.64 | | (all_152_1 = 0) | ~ (all_152_2 = 0) | ~ (all_152_3 = 0) | ~ % 21.63/3.64 | | (all_152_4 = 0) | ~ (all_152_5 = 0)) % 21.63/3.64 | | % 21.63/3.64 | | ALPHA: (116) implies: % 21.63/3.64 | | (117) aScalar0(xR) = all_152_5 % 21.63/3.64 | | (118) aScalar0(xP) = all_152_4 % 21.63/3.64 | | (119) aScalar0(xP) = all_152_2 % 21.63/3.64 | | (120) aScalar0(xS) = all_152_3 % 21.63/3.64 | | % 21.63/3.64 | | BETA: splitting (69) gives: % 21.63/3.64 | | % 21.63/3.64 | | Case 1: % 21.63/3.64 | | | % 21.63/3.64 | | | (121) all_45_0 = 0 % 21.63/3.64 | | | % 21.63/3.64 | | | REDUCE: (20), (121) imply: % 21.63/3.64 | | | (122) $false % 21.63/3.64 | | | % 21.63/3.64 | | | CLOSE: (122) is inconsistent. % 21.63/3.64 | | | % 21.63/3.64 | | Case 2: % 21.63/3.64 | | | % 21.63/3.64 | | | (123) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? % 21.63/3.64 | | | [v4: any] : ? [v5: any] : (sdtlseqdt0(xP, xS) = v5 & % 21.63/3.64 | | | sdtlseqdt0(xP, xR) = v4 & aScalar0(xS) = v3 & aScalar0(xP) = v2 % 21.63/3.64 | | | & aScalar0(xP) = v0 & aScalar0(xR) = v1 & ( ~ (v5 = 0) | ~ (v4 % 21.63/3.64 | | | = 0) | ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = % 21.63/3.64 | | | 0))) % 21.63/3.64 | | | % 21.63/3.64 | | | DELTA: instantiating (123) with fresh symbols all_157_0, all_157_1, % 21.63/3.64 | | | all_157_2, all_157_3, all_157_4, all_157_5 gives: % 21.63/3.64 | | | (124) sdtlseqdt0(xP, xS) = all_157_0 & sdtlseqdt0(xP, xR) = all_157_1 & % 21.63/3.64 | | | aScalar0(xS) = all_157_2 & aScalar0(xP) = all_157_3 & % 21.63/3.64 | | | aScalar0(xP) = all_157_5 & aScalar0(xR) = all_157_4 & ( ~ % 21.63/3.64 | | | (all_157_0 = 0) | ~ (all_157_1 = 0) | ~ (all_157_2 = 0) | ~ % 21.63/3.64 | | | (all_157_3 = 0) | ~ (all_157_4 = 0) | ~ (all_157_5 = 0)) % 21.63/3.64 | | | % 21.63/3.64 | | | ALPHA: (124) implies: % 21.63/3.64 | | | (125) aScalar0(xR) = all_157_4 % 21.63/3.64 | | | (126) aScalar0(xP) = all_157_5 % 21.63/3.64 | | | (127) aScalar0(xP) = all_157_3 % 21.63/3.64 | | | (128) aScalar0(xS) = all_157_2 % 21.63/3.64 | | | % 21.63/3.64 | | | GROUND_INST: instantiating (13) with all_110_2, all_110_1, xR, simplifying % 21.63/3.64 | | | with (84), (85) gives: % 21.63/3.65 | | | (129) all_110_1 = all_110_2 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_110_1, all_128_2, xR, simplifying % 21.63/3.65 | | | with (85), (102) gives: % 21.63/3.65 | | | (130) all_128_2 = all_110_1 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_86_1, all_128_2, xR, simplifying % 21.63/3.65 | | | with (74), (102) gives: % 21.63/3.65 | | | (131) all_128_2 = all_86_1 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_110_2, all_152_5, xR, simplifying % 21.63/3.65 | | | with (84), (117) gives: % 21.63/3.65 | | | (132) all_152_5 = all_110_2 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with 0, all_157_4, xR, simplifying with % 21.63/3.65 | | | (2), (125) gives: % 21.63/3.65 | | | (133) all_157_4 = 0 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_152_5, all_157_4, xR, simplifying % 21.63/3.65 | | | with (117), (125) gives: % 21.63/3.65 | | | (134) all_157_4 = all_152_5 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_118_1, all_124_2, xP, simplifying % 21.63/3.65 | | | with (92), (94) gives: % 21.63/3.65 | | | (135) all_124_2 = all_118_1 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_124_2, all_140_8, xP, simplifying % 21.63/3.65 | | | with (94), (110) gives: % 21.63/3.65 | | | (136) all_140_8 = all_124_2 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_140_8, all_140_6, xP, simplifying % 21.63/3.65 | | | with (110), (112) gives: % 21.63/3.65 | | | (137) all_140_6 = all_140_8 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with 0, all_152_4, xP, simplifying with % 21.63/3.65 | | | (3), (118) gives: % 21.63/3.65 | | | (138) all_152_4 = 0 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_140_7, all_152_4, xP, simplifying % 21.63/3.65 | | | with (111), (118) gives: % 21.63/3.65 | | | (139) all_152_4 = all_140_7 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_124_2, all_152_4, xP, simplifying % 21.63/3.65 | | | with (94), (118) gives: % 21.63/3.65 | | | (140) all_152_4 = all_124_2 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_140_8, all_152_2, xP, simplifying % 21.63/3.65 | | | with (110), (119) gives: % 21.63/3.65 | | | (141) all_152_2 = all_140_8 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_124_1, all_152_2, xP, simplifying % 21.63/3.65 | | | with (95), (119) gives: % 21.63/3.65 | | | (142) all_152_2 = all_124_1 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_140_6, all_157_5, xP, simplifying % 21.63/3.65 | | | with (112), (126) gives: % 21.63/3.65 | | | (143) all_157_5 = all_140_6 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_100_1, all_157_5, xP, simplifying % 21.63/3.65 | | | with (82), (126) gives: % 21.63/3.65 | | | (144) all_157_5 = all_100_1 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_152_4, all_157_3, xP, simplifying % 21.63/3.65 | | | with (118), (127) gives: % 21.63/3.65 | | | (145) all_157_3 = all_152_4 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_118_2, all_157_3, xP, simplifying % 21.63/3.65 | | | with (91), (127) gives: % 21.63/3.65 | | | (146) all_157_3 = all_118_2 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_126_2, all_126_1, xS, simplifying % 21.63/3.65 | | | with (99), (100) gives: % 21.63/3.65 | | | (147) all_126_1 = all_126_2 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_126_1, all_128_1, xS, simplifying % 21.63/3.65 | | | with (100), (103) gives: % 21.63/3.65 | | | (148) all_128_1 = all_126_1 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with 0, all_152_3, xS, simplifying with % 21.63/3.65 | | | (4), (120) gives: % 21.63/3.65 | | | (149) all_152_3 = 0 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_126_1, all_152_3, xS, simplifying % 21.63/3.65 | | | with (100), (120) gives: % 21.63/3.65 | | | (150) all_152_3 = all_126_1 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_128_1, all_157_2, xS, simplifying % 21.63/3.65 | | | with (103), (128) gives: % 21.63/3.65 | | | (151) all_157_2 = all_128_1 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_98_1, all_157_2, xS, simplifying % 21.63/3.65 | | | with (80), (128) gives: % 21.63/3.65 | | | (152) all_157_2 = all_98_1 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_92_1, all_116_1, all_45_2, % 21.63/3.65 | | | simplifying with (78), (88) gives: % 21.63/3.65 | | | (153) all_116_1 = all_92_1 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_116_1, all_124_0, all_45_2, % 21.63/3.65 | | | simplifying with (88), (96) gives: % 21.63/3.65 | | | (154) all_124_0 = all_116_1 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_116_2, all_124_0, all_45_2, % 21.63/3.65 | | | simplifying with (87), (96) gives: % 21.63/3.65 | | | (155) all_124_0 = all_116_2 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_134_2, all_134_1, all_45_1, % 21.63/3.65 | | | simplifying with (107), (108) gives: % 21.63/3.65 | | | (156) all_134_1 = all_134_2 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_128_0, all_134_1, all_45_1, % 21.63/3.65 | | | simplifying with (104), (108) gives: % 21.63/3.65 | | | (157) all_134_1 = all_128_0 % 21.63/3.65 | | | % 21.63/3.65 | | | GROUND_INST: instantiating (13) with all_90_1, all_134_1, all_45_1, % 21.63/3.65 | | | simplifying with (76), (108) gives: % 21.63/3.65 | | | (158) all_134_1 = all_90_1 % 21.63/3.65 | | | % 21.63/3.65 | | | COMBINE_EQS: (151), (152) imply: % 21.63/3.65 | | | (159) all_128_1 = all_98_1 % 21.63/3.65 | | | % 21.63/3.65 | | | SIMP: (159) implies: % 21.63/3.65 | | | (160) all_128_1 = all_98_1 % 21.63/3.65 | | | % 21.63/3.65 | | | COMBINE_EQS: (145), (146) imply: % 21.63/3.65 | | | (161) all_152_4 = all_118_2 % 21.63/3.65 | | | % 21.63/3.65 | | | SIMP: (161) implies: % 21.63/3.65 | | | (162) all_152_4 = all_118_2 % 21.63/3.65 | | | % 21.63/3.65 | | | COMBINE_EQS: (133), (134) imply: % 21.63/3.65 | | | (163) all_152_5 = 0 % 21.63/3.65 | | | % 21.63/3.65 | | | SIMP: (163) implies: % 21.63/3.65 | | | (164) all_152_5 = 0 % 21.63/3.65 | | | % 21.63/3.65 | | | COMBINE_EQS: (143), (144) imply: % 21.63/3.65 | | | (165) all_140_6 = all_100_1 % 21.63/3.65 | | | % 21.63/3.65 | | | SIMP: (165) implies: % 21.63/3.65 | | | (166) all_140_6 = all_100_1 % 21.63/3.65 | | | % 21.63/3.65 | | | COMBINE_EQS: (141), (142) imply: % 21.63/3.65 | | | (167) all_140_8 = all_124_1 % 21.63/3.65 | | | % 21.63/3.65 | | | SIMP: (167) implies: % 21.63/3.65 | | | (168) all_140_8 = all_124_1 % 21.63/3.65 | | | % 21.63/3.65 | | | COMBINE_EQS: (149), (150) imply: % 21.63/3.65 | | | (169) all_126_1 = 0 % 21.63/3.65 | | | % 21.63/3.65 | | | SIMP: (169) implies: % 21.63/3.65 | | | (170) all_126_1 = 0 % 21.63/3.65 | | | % 21.63/3.65 | | | COMBINE_EQS: (138), (139) imply: % 21.63/3.65 | | | (171) all_140_7 = 0 % 21.63/3.65 | | | % 21.63/3.65 | | | COMBINE_EQS: (139), (140) imply: % 21.63/3.65 | | | (172) all_140_7 = all_124_2 % 21.63/3.65 | | | % 21.63/3.66 | | | COMBINE_EQS: (139), (162) imply: % 21.63/3.66 | | | (173) all_140_7 = all_118_2 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (132), (164) imply: % 21.63/3.66 | | | (174) all_110_2 = 0 % 21.63/3.66 | | | % 21.63/3.66 | | | SIMP: (174) implies: % 21.63/3.66 | | | (175) all_110_2 = 0 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (137), (166) imply: % 21.63/3.66 | | | (176) all_140_8 = all_100_1 % 21.63/3.66 | | | % 21.63/3.66 | | | SIMP: (176) implies: % 21.63/3.66 | | | (177) all_140_8 = all_100_1 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (171), (173) imply: % 21.63/3.66 | | | (178) all_118_2 = 0 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (172), (173) imply: % 21.63/3.66 | | | (179) all_124_2 = all_118_2 % 21.63/3.66 | | | % 21.63/3.66 | | | SIMP: (179) implies: % 21.63/3.66 | | | (180) all_124_2 = all_118_2 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (136), (168) imply: % 21.63/3.66 | | | (181) all_124_1 = all_124_2 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (168), (177) imply: % 21.63/3.66 | | | (182) all_124_1 = all_100_1 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (156), (158) imply: % 21.63/3.66 | | | (183) all_134_2 = all_90_1 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (156), (157) imply: % 21.63/3.66 | | | (184) all_134_2 = all_128_0 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (183), (184) imply: % 21.63/3.66 | | | (185) all_128_0 = all_90_1 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (148), (160) imply: % 21.63/3.66 | | | (186) all_126_1 = all_98_1 % 21.63/3.66 | | | % 21.63/3.66 | | | SIMP: (186) implies: % 21.63/3.66 | | | (187) all_126_1 = all_98_1 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (130), (131) imply: % 21.63/3.66 | | | (188) all_110_1 = all_86_1 % 21.63/3.66 | | | % 21.63/3.66 | | | SIMP: (188) implies: % 21.63/3.66 | | | (189) all_110_1 = all_86_1 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (147), (187) imply: % 21.63/3.66 | | | (190) all_126_2 = all_98_1 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (147), (170) imply: % 21.63/3.66 | | | (191) all_126_2 = 0 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (190), (191) imply: % 21.63/3.66 | | | (192) all_98_1 = 0 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (154), (155) imply: % 21.63/3.66 | | | (193) all_116_1 = all_116_2 % 21.63/3.66 | | | % 21.63/3.66 | | | SIMP: (193) implies: % 21.63/3.66 | | | (194) all_116_1 = all_116_2 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (181), (182) imply: % 21.63/3.66 | | | (195) all_124_2 = all_100_1 % 21.63/3.66 | | | % 21.63/3.66 | | | SIMP: (195) implies: % 21.63/3.66 | | | (196) all_124_2 = all_100_1 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (135), (180) imply: % 21.63/3.66 | | | (197) all_118_1 = all_118_2 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (135), (196) imply: % 21.63/3.66 | | | (198) all_118_1 = all_100_1 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (197), (198) imply: % 21.63/3.66 | | | (199) all_118_2 = all_100_1 % 21.63/3.66 | | | % 21.63/3.66 | | | SIMP: (199) implies: % 21.63/3.66 | | | (200) all_118_2 = all_100_1 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (178), (200) imply: % 21.63/3.66 | | | (201) all_100_1 = 0 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (153), (194) imply: % 21.63/3.66 | | | (202) all_116_2 = all_92_1 % 21.63/3.66 | | | % 21.63/3.66 | | | SIMP: (202) implies: % 21.63/3.66 | | | (203) all_116_2 = all_92_1 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (129), (189) imply: % 21.63/3.66 | | | (204) all_110_2 = all_86_1 % 21.63/3.66 | | | % 21.63/3.66 | | | SIMP: (204) implies: % 21.63/3.66 | | | (205) all_110_2 = all_86_1 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (175), (205) imply: % 21.63/3.66 | | | (206) all_86_1 = 0 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (198), (201) imply: % 21.63/3.66 | | | (207) all_118_1 = 0 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (135), (207) imply: % 21.63/3.66 | | | (208) all_124_2 = 0 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (182), (201) imply: % 21.63/3.66 | | | (209) all_124_1 = 0 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (155), (203) imply: % 21.63/3.66 | | | (210) all_124_0 = all_92_1 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (131), (206) imply: % 21.63/3.66 | | | (211) all_128_2 = 0 % 21.63/3.66 | | | % 21.63/3.66 | | | COMBINE_EQS: (160), (192) imply: % 21.63/3.66 | | | (212) all_128_1 = 0 % 21.63/3.66 | | | % 21.63/3.66 | | | BETA: splitting (105) gives: % 21.63/3.66 | | | % 21.63/3.66 | | | Case 1: % 21.63/3.66 | | | | % 21.63/3.66 | | | | (213) ~ (all_128_1 = 0) % 21.63/3.66 | | | | % 21.63/3.66 | | | | REDUCE: (212), (213) imply: % 21.63/3.66 | | | | (214) $false % 21.63/3.66 | | | | % 21.63/3.66 | | | | CLOSE: (214) is inconsistent. % 21.63/3.66 | | | | % 21.63/3.66 | | | Case 2: % 21.63/3.66 | | | | % 21.63/3.66 | | | | (215) ~ (all_128_2 = 0) | all_128_0 = 0 % 21.63/3.66 | | | | % 21.63/3.66 | | | | BETA: splitting (97) gives: % 21.63/3.66 | | | | % 21.63/3.66 | | | | Case 1: % 21.63/3.66 | | | | | % 21.63/3.66 | | | | | (216) ~ (all_124_1 = 0) % 21.63/3.66 | | | | | % 21.63/3.66 | | | | | REDUCE: (209), (216) imply: % 21.63/3.66 | | | | | (217) $false % 21.63/3.66 | | | | | % 21.63/3.66 | | | | | CLOSE: (217) is inconsistent. % 21.63/3.66 | | | | | % 21.63/3.66 | | | | Case 2: % 21.63/3.66 | | | | | % 21.63/3.66 | | | | | (218) ~ (all_124_2 = 0) | all_124_0 = 0 % 21.63/3.66 | | | | | % 21.63/3.66 | | | | | BETA: splitting (218) gives: % 21.63/3.66 | | | | | % 21.63/3.66 | | | | | Case 1: % 21.63/3.66 | | | | | | % 21.63/3.66 | | | | | | (219) ~ (all_124_2 = 0) % 21.63/3.66 | | | | | | % 21.63/3.66 | | | | | | REDUCE: (208), (219) imply: % 21.63/3.66 | | | | | | (220) $false % 21.63/3.66 | | | | | | % 21.63/3.66 | | | | | | CLOSE: (220) is inconsistent. % 21.63/3.66 | | | | | | % 21.63/3.66 | | | | | Case 2: % 21.63/3.66 | | | | | | % 21.63/3.66 | | | | | | (221) all_124_0 = 0 % 21.63/3.66 | | | | | | % 21.63/3.66 | | | | | | COMBINE_EQS: (210), (221) imply: % 21.63/3.66 | | | | | | (222) all_92_1 = 0 % 21.63/3.66 | | | | | | % 21.63/3.66 | | | | | | SIMP: (222) implies: % 21.63/3.66 | | | | | | (223) all_92_1 = 0 % 21.63/3.66 | | | | | | % 21.63/3.66 | | | | | | COMBINE_EQS: (203), (223) imply: % 21.63/3.66 | | | | | | (224) all_116_2 = 0 % 21.63/3.66 | | | | | | % 21.63/3.66 | | | | | | COMBINE_EQS: (153), (223) imply: % 21.63/3.66 | | | | | | (225) all_116_1 = 0 % 21.63/3.66 | | | | | | % 21.63/3.66 | | | | | | REDUCE: (78), (223) imply: % 21.63/3.66 | | | | | | (226) aScalar0(all_45_2) = 0 % 21.63/3.66 | | | | | | % 21.63/3.66 | | | | | | BETA: splitting (70) gives: % 21.63/3.66 | | | | | | % 21.63/3.66 | | | | | | Case 1: % 21.63/3.66 | | | | | | | % 21.63/3.66 | | | | | | | (227) all_45_0 = 0 % 21.63/3.66 | | | | | | | % 21.63/3.66 | | | | | | | REDUCE: (20), (227) imply: % 21.63/3.66 | | | | | | | (228) $false % 21.63/3.66 | | | | | | | % 21.63/3.66 | | | | | | | CLOSE: (228) is inconsistent. % 21.63/3.66 | | | | | | | % 21.63/3.66 | | | | | | Case 2: % 21.63/3.66 | | | | | | | % 21.63/3.66 | | | | | | | (229) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 21.63/3.66 | | | | | | | (sdtlseqdt0(all_45_1, all_45_2) = v2 & aScalar0(all_45_1) % 21.63/3.66 | | | | | | | = v1 & aScalar0(all_45_2) = v0 & ( ~ (v1 = 0) | ~ (v0 % 21.63/3.66 | | | | | | | = 0) | v2 = 0)) % 21.63/3.66 | | | | | | | % 21.63/3.66 | | | | | | | DELTA: instantiating (229) with fresh symbols all_239_0, % 21.63/3.66 | | | | | | | all_239_1, all_239_2 gives: % 21.63/3.66 | | | | | | | (230) sdtlseqdt0(all_45_1, all_45_2) = all_239_0 & % 21.63/3.66 | | | | | | | aScalar0(all_45_1) = all_239_1 & aScalar0(all_45_2) = % 21.63/3.66 | | | | | | | all_239_2 & ( ~ (all_239_1 = 0) | ~ (all_239_2 = 0) | % 21.63/3.66 | | | | | | | all_239_0 = 0) % 21.63/3.66 | | | | | | | % 21.63/3.66 | | | | | | | ALPHA: (230) implies: % 21.63/3.66 | | | | | | | (231) aScalar0(all_45_2) = all_239_2 % 21.63/3.66 | | | | | | | (232) aScalar0(all_45_1) = all_239_1 % 21.63/3.66 | | | | | | | (233) sdtlseqdt0(all_45_1, all_45_2) = all_239_0 % 21.63/3.66 | | | | | | | (234) ~ (all_239_1 = 0) | ~ (all_239_2 = 0) | all_239_0 = 0 % 21.63/3.66 | | | | | | | % 21.63/3.66 | | | | | | | BETA: splitting (72) gives: % 21.63/3.66 | | | | | | | % 21.63/3.66 | | | | | | | Case 1: % 21.63/3.66 | | | | | | | | % 21.63/3.66 | | | | | | | | (235) all_47_0 = 0 % 21.63/3.66 | | | | | | | | % 21.63/3.66 | | | | | | | | REDUCE: (25), (235) imply: % 21.63/3.66 | | | | | | | | (236) $false % 21.63/3.66 | | | | | | | | % 21.63/3.66 | | | | | | | | CLOSE: (236) is inconsistent. % 21.63/3.66 | | | | | | | | % 21.63/3.66 | | | | | | | Case 2: % 21.63/3.66 | | | | | | | | % 21.63/3.67 | | | | | | | | (237) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 21.63/3.67 | | | | | | | | (sdtlseqdt0(all_45_2, all_45_1) = v2 & % 21.63/3.67 | | | | | | | | aScalar0(all_45_1) = v0 & aScalar0(all_45_2) = v1 & ( % 21.63/3.67 | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 21.63/3.67 | | | | | | | | % 21.63/3.67 | | | | | | | | DELTA: instantiating (237) with fresh symbols all_260_0, % 21.63/3.67 | | | | | | | | all_260_1, all_260_2 gives: % 21.63/3.67 | | | | | | | | (238) sdtlseqdt0(all_45_2, all_45_1) = all_260_0 & % 21.63/3.67 | | | | | | | | aScalar0(all_45_1) = all_260_2 & aScalar0(all_45_2) = % 21.63/3.67 | | | | | | | | all_260_1 & ( ~ (all_260_1 = 0) | ~ (all_260_2 = 0) | % 21.63/3.67 | | | | | | | | all_260_0 = 0) % 21.63/3.67 | | | | | | | | % 21.63/3.67 | | | | | | | | ALPHA: (238) implies: % 21.63/3.67 | | | | | | | | (239) aScalar0(all_45_2) = all_260_1 % 21.63/3.67 | | | | | | | | (240) aScalar0(all_45_1) = all_260_2 % 21.63/3.67 | | | | | | | | % 21.63/3.67 | | | | | | | | BETA: splitting (215) gives: % 21.63/3.67 | | | | | | | | % 21.63/3.67 | | | | | | | | Case 1: % 21.63/3.67 | | | | | | | | | % 21.63/3.67 | | | | | | | | | (241) ~ (all_128_2 = 0) % 21.63/3.67 | | | | | | | | | % 21.63/3.67 | | | | | | | | | REDUCE: (211), (241) imply: % 21.63/3.67 | | | | | | | | | (242) $false % 21.63/3.67 | | | | | | | | | % 21.63/3.67 | | | | | | | | | CLOSE: (242) is inconsistent. % 21.63/3.67 | | | | | | | | | % 21.63/3.67 | | | | | | | | Case 2: % 21.63/3.67 | | | | | | | | | % 21.63/3.67 | | | | | | | | | (243) all_128_0 = 0 % 21.63/3.67 | | | | | | | | | % 21.63/3.67 | | | | | | | | | COMBINE_EQS: (185), (243) imply: % 21.63/3.67 | | | | | | | | | (244) all_90_1 = 0 % 21.63/3.67 | | | | | | | | | % 21.63/3.67 | | | | | | | | | REDUCE: (76), (244) imply: % 21.63/3.67 | | | | | | | | | (245) aScalar0(all_45_1) = 0 % 21.63/3.67 | | | | | | | | | % 21.63/3.67 | | | | | | | | | BETA: splitting (89) gives: % 21.63/3.67 | | | | | | | | | % 21.63/3.67 | | | | | | | | | Case 1: % 21.63/3.67 | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | (246) ~ (all_116_1 = 0) % 21.63/3.67 | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | REDUCE: (225), (246) imply: % 21.63/3.67 | | | | | | | | | | (247) $false % 21.63/3.67 | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | CLOSE: (247) is inconsistent. % 21.63/3.67 | | | | | | | | | | % 21.63/3.67 | | | | | | | | | Case 2: % 21.63/3.67 | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | (248) ~ (all_116_2 = 0) | all_116_0 = 0 % 21.63/3.67 | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | BETA: splitting (248) gives: % 21.63/3.67 | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | Case 1: % 21.63/3.67 | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | (249) ~ (all_116_2 = 0) % 21.63/3.67 | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | REDUCE: (224), (249) imply: % 21.63/3.67 | | | | | | | | | | | (250) $false % 21.63/3.67 | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | CLOSE: (250) is inconsistent. % 21.63/3.67 | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | Case 2: % 21.63/3.67 | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_239_2, all_260_1, % 21.63/3.67 | | | | | | | | | | | all_45_2, simplifying with (231), (239) gives: % 21.63/3.67 | | | | | | | | | | | (251) all_260_1 = all_239_2 % 21.63/3.67 | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_260_1, all_45_2, % 21.63/3.67 | | | | | | | | | | | simplifying with (226), (239) gives: % 21.63/3.67 | | | | | | | | | | | (252) all_260_1 = 0 % 21.63/3.67 | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_239_1, all_260_2, % 21.63/3.67 | | | | | | | | | | | all_45_1, simplifying with (232), (240) gives: % 21.63/3.67 | | | | | | | | | | | (253) all_260_2 = all_239_1 % 21.63/3.67 | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_260_2, all_45_1, % 21.63/3.67 | | | | | | | | | | | simplifying with (240), (245) gives: % 21.63/3.67 | | | | | | | | | | | (254) all_260_2 = 0 % 21.63/3.67 | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | GROUND_INST: instantiating (16) with all_47_0, all_239_0, % 21.63/3.67 | | | | | | | | | | | all_45_2, all_45_1, simplifying with (50), (233) % 21.63/3.67 | | | | | | | | | | | gives: % 21.63/3.67 | | | | | | | | | | | (255) all_239_0 = all_47_0 % 21.63/3.67 | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | COMBINE_EQS: (251), (252) imply: % 21.63/3.67 | | | | | | | | | | | (256) all_239_2 = 0 % 21.63/3.67 | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | COMBINE_EQS: (253), (254) imply: % 21.63/3.67 | | | | | | | | | | | (257) all_239_1 = 0 % 21.63/3.67 | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | SIMP: (257) implies: % 21.63/3.67 | | | | | | | | | | | (258) all_239_1 = 0 % 21.63/3.67 | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | BETA: splitting (234) gives: % 21.63/3.67 | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | Case 1: % 21.63/3.67 | | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | | (259) ~ (all_239_1 = 0) % 21.63/3.67 | | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | | REDUCE: (258), (259) imply: % 21.63/3.67 | | | | | | | | | | | | (260) $false % 21.63/3.67 | | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | | CLOSE: (260) is inconsistent. % 21.63/3.67 | | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | Case 2: % 21.63/3.67 | | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | | (261) ~ (all_239_2 = 0) | all_239_0 = 0 % 21.63/3.67 | | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | | BETA: splitting (261) gives: % 21.63/3.67 | | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | | Case 1: % 21.63/3.67 | | | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | | | (262) ~ (all_239_2 = 0) % 21.63/3.67 | | | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | | | REDUCE: (256), (262) imply: % 21.63/3.67 | | | | | | | | | | | | | (263) $false % 21.63/3.67 | | | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | | | CLOSE: (263) is inconsistent. % 21.63/3.67 | | | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | | Case 2: % 21.63/3.67 | | | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | | | (264) all_239_0 = 0 % 21.63/3.67 | | | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | | | COMBINE_EQS: (255), (264) imply: % 21.63/3.67 | | | | | | | | | | | | | (265) all_47_0 = 0 % 21.63/3.67 | | | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | | | REDUCE: (25), (265) imply: % 21.63/3.67 | | | | | | | | | | | | | (266) $false % 21.63/3.67 | | | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | | | CLOSE: (266) is inconsistent. % 21.63/3.67 | | | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | | End of split % 21.63/3.67 | | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | | End of split % 21.63/3.67 | | | | | | | | | | | % 21.63/3.67 | | | | | | | | | | End of split % 21.63/3.67 | | | | | | | | | | % 21.63/3.67 | | | | | | | | | End of split % 21.63/3.67 | | | | | | | | | % 21.63/3.67 | | | | | | | | End of split % 21.63/3.67 | | | | | | | | % 21.63/3.67 | | | | | | | End of split % 21.63/3.67 | | | | | | | % 21.63/3.67 | | | | | | End of split % 21.63/3.67 | | | | | | % 21.63/3.67 | | | | | End of split % 21.63/3.67 | | | | | % 21.63/3.67 | | | | End of split % 21.63/3.67 | | | | % 21.63/3.67 | | | End of split % 21.63/3.67 | | | % 21.63/3.67 | | End of split % 21.63/3.67 | | % 21.63/3.67 | End of split % 21.63/3.67 | % 21.63/3.67 End of proof % 21.63/3.67 % SZS output end Proof for theBenchmark % 21.63/3.67 % 21.63/3.67 3045ms %------------------------------------------------------------------------------