%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : RNG052+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 : n021.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:34 EDT 2023 % Result : Theorem 13.04s 2.47s % Output : Proof 21.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : RNG052+2 : TPTP v8.1.2. Released v4.0.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n021.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Aug 27 01:39:42 EDT 2023 % 0.13/0.34 % CPUTime : % 0.19/0.58 ________ _____ % 0.19/0.58 ___ __ \_________(_)________________________________ % 0.19/0.58 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.58 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.58 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.58 % 0.19/0.58 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.58 (2023-06-19) % 0.19/0.58 % 0.19/0.58 (c) Philipp Rümmer, 2009-2023 % 0.19/0.58 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.58 Amanda Stjerna. % 0.19/0.58 Free software under BSD-3-Clause. % 0.19/0.58 % 0.19/0.58 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.58 % 0.19/0.58 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.19/0.59 Running up to 7 provers in parallel. % 0.19/0.60 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.60 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.60 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.60 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.60 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.60 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.60 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.97/1.15 Prover 4: Preprocessing ... % 2.97/1.16 Prover 1: Preprocessing ... % 3.64/1.19 Prover 3: Preprocessing ... % 3.64/1.19 Prover 5: Preprocessing ... % 3.64/1.19 Prover 6: Preprocessing ... % 3.64/1.19 Prover 0: Preprocessing ... % 3.64/1.19 Prover 2: Preprocessing ... % 8.71/1.90 Prover 3: Constructing countermodel ... % 8.71/1.91 Prover 1: Constructing countermodel ... % 8.71/1.94 Prover 6: Proving ... % 10.72/2.14 Prover 5: Constructing countermodel ... % 10.72/2.18 Prover 4: Constructing countermodel ... % 11.17/2.24 Prover 2: Proving ... % 12.27/2.35 Prover 0: Proving ... % 13.04/2.47 Prover 3: proved (1870ms) % 13.04/2.47 % 13.04/2.47 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.04/2.47 % 13.04/2.47 Prover 5: stopped % 13.04/2.47 Prover 2: stopped % 13.04/2.48 Prover 0: stopped % 13.04/2.48 Prover 6: stopped % 13.04/2.48 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 13.04/2.48 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 13.04/2.48 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 13.04/2.48 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 13.04/2.48 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 13.92/2.58 Prover 8: Preprocessing ... % 13.92/2.59 Prover 10: Preprocessing ... % 13.92/2.61 Prover 13: Preprocessing ... % 13.92/2.61 Prover 7: Preprocessing ... % 13.92/2.63 Prover 11: Preprocessing ... % 15.48/2.78 Prover 8: Warning: ignoring some quantifiers % 15.48/2.79 Prover 10: Constructing countermodel ... % 15.48/2.80 Prover 8: Constructing countermodel ... % 16.04/2.86 Prover 13: Constructing countermodel ... % 16.30/2.87 Prover 7: Constructing countermodel ... % 17.81/3.10 Prover 11: Constructing countermodel ... % 20.37/3.42 Prover 1: Found proof (size 256) % 20.37/3.42 Prover 1: proved (2823ms) % 20.37/3.42 Prover 4: stopped % 20.37/3.42 Prover 11: stopped % 20.37/3.42 Prover 7: stopped % 20.37/3.42 Prover 10: stopped % 20.37/3.42 Prover 13: stopped % 20.37/3.42 Prover 8: stopped % 20.37/3.42 % 20.37/3.42 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 20.37/3.42 % 20.37/3.47 % SZS output start Proof for theBenchmark % 20.37/3.47 Assumptions after simplification: % 20.37/3.47 --------------------------------- % 20.37/3.47 % 20.37/3.47 (mDefInit) % 20.72/3.50 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ( ~ (sziznziztdt0(v0) = v1) | ~ $i(v0) % 20.72/3.50 | ? [v2: any] : ? [v3: $i] : (aVector0(v0) = v2 & aDimensionOf0(v0) = v3 & % 20.72/3.50 $i(v3) & ( ~ (v2 = 0) | v3 = sz00 | ( ! [v4: $i] : (v4 = v1 | ~ % 20.72/3.50 (aVector0(v4) = 0) | ~ $i(v4) | ? [v5: $i] : ? [v6: $i] : ? [v7: % 20.72/3.50 $i] : ( ~ (v7 = v6) & sdtlbdtrb0(v4, v5) = v6 & sdtlbdtrb0(v0, v5) % 20.72/3.50 = v7 & aNaturalNumber0(v5) = 0 & $i(v7) & $i(v6) & $i(v5)) | ? % 20.72/3.50 [v5: $i] : ? [v6: $i] : ( ~ (v6 = v3) & aDimensionOf0(v4) = v5 & % 20.72/3.50 szszuzczcdt0(v5) = v6 & $i(v6) & $i(v5))) & ! [v4: any] : ( ~ % 20.72/3.50 (aVector0(v1) = v4) | ~ $i(v1) | (v4 = 0 & ! [v5: $i] : ! [v6: % 20.72/3.50 $i] : ( ~ (sdtlbdtrb0(v0, v5) = v6) | ~ $i(v5) | ? [v7: any] : % 20.72/3.50 ? [v8: $i] : (sdtlbdtrb0(v1, v5) = v8 & aNaturalNumber0(v5) = % 20.72/3.50 v7 & $i(v8) & ( ~ (v7 = 0) | v8 = v6))) & ? [v5: $i] : % 20.72/3.50 (aDimensionOf0(v1) = v5 & szszuzczcdt0(v5) = v3 & $i(v5)))))))) % 20.72/3.50 % 20.72/3.50 (mDimNat) % 20.72/3.50 ! [v0: $i] : ( ~ (aVector0(v0) = 0) | ~ $i(v0) | ? [v1: $i] : % 20.72/3.50 (aDimensionOf0(v0) = v1 & aNaturalNumber0(v1) = 0 & $i(v1))) % 20.72/3.50 % 20.72/3.50 (mElmSc) % 20.72/3.50 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtlbdtrb0(v0, v1) = v2) | ~ % 20.72/3.50 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 20.72/3.50 (aVector0(v0) = v3 & aScalar0(v2) = v5 & aNaturalNumber0(v1) = v4 & ( ~ (v4 % 20.72/3.50 = 0) | ~ (v3 = 0) | v5 = 0))) % 20.72/3.50 % 20.72/3.50 (mEqInit) % 20.72/3.50 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 20.72/3.50 (sziznziztdt0(v1) = v3) | ~ (sziznziztdt0(v0) = v2) | ~ $i(v1) | ~ $i(v0) % 20.72/3.50 | ? [v4: any] : ? [v5: any] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? % 20.72/3.50 [v9: $i] : (aVector0(v1) = v5 & aVector0(v0) = v4 & aDimensionOf0(v3) = v9 & % 20.72/3.50 aDimensionOf0(v2) = v8 & aDimensionOf0(v1) = v7 & aDimensionOf0(v0) = v6 & % 20.72/3.50 $i(v9) & $i(v8) & $i(v7) & $i(v6) & ( ~ (v7 = v6) | ~ (v5 = 0) | ~ (v4 = % 20.72/3.50 0) | v9 = v8 | v6 = sz00))) % 20.72/3.50 % 20.72/3.50 (mIH) % 20.72/3.50 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (iLess0(v0, v1) = v2) % 20.72/3.50 | ~ (szszuzczcdt0(v0) = v1) | ~ $i(v0) | ? [v3: int] : ( ~ (v3 = 0) & % 20.72/3.50 aNaturalNumber0(v0) = v3)) % 20.72/3.50 % 20.72/3.50 (mLEMonM) % 20.72/3.50 $i(sz0z00) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 20.72/3.50 $i] : ! [v5: $i] : ! [v6: int] : (v6 = 0 | ~ (sdtlseqdt0(v4, v5) = v6) | % 20.72/3.50 ~ (sdtasdt0(v1, v3) = v5) | ~ (sdtasdt0(v0, v2) = v4) | ~ $i(v3) | ~ % 20.72/3.50 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v7: any] : ? [v8: any] : ? [v9: any] % 20.72/3.50 : ? [v10: any] : ? [v11: any] : ? [v12: any] : ? [v13: any] : % 20.72/3.50 (sdtlseqdt0(v2, v3) = v13 & sdtlseqdt0(v0, v1) = v11 & sdtlseqdt0(sz0z00, % 20.72/3.50 v2) = v12 & aScalar0(v3) = v10 & aScalar0(v2) = v9 & aScalar0(v1) = v8 & % 20.72/3.50 aScalar0(v0) = v7 & ( ~ (v13 = 0) | ~ (v12 = 0) | ~ (v11 = 0) | ~ (v10 % 20.72/3.50 = 0) | ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0)))) % 20.72/3.50 % 20.72/3.50 (mScSqPos) % 20.72/3.51 $i(sz0z00) & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtasasdt0(v0, v0) = v1) | ~ % 20.72/3.51 $i(v0) | ? [v2: any] : ? [v3: any] : (aVector0(v0) = v2 & % 20.72/3.51 sdtlseqdt0(sz0z00, v1) = v3 & ( ~ (v2 = 0) | v3 = 0))) % 20.72/3.51 % 20.72/3.51 (mSuccNat) % 20.72/3.51 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ( ~ (szszuzczcdt0(v0) = v1) | ~ $i(v0) % 20.72/3.51 | ? [v2: any] : ? [v3: any] : (aNaturalNumber0(v1) = v3 & % 20.72/3.51 aNaturalNumber0(v0) = v2 & ( ~ (v2 = 0) | (v3 = 0 & ~ (v1 = sz00))))) % 20.72/3.51 % 20.72/3.51 (m__) % 20.72/3.51 $i(xE) & $i(xD) & $i(xC) & ? [v0: $i] : ? [v1: $i] : ? [v2: int] : ( ~ (v2 % 20.72/3.51 = 0) & sdtlseqdt0(v0, v1) = v2 & sdtasdt0(xE, xE) = v0 & sdtasdt0(xC, xD) % 20.72/3.51 = v1 & $i(v1) & $i(v0)) % 20.72/3.51 % 20.72/3.51 (m__1652) % 20.72/3.51 $i(xs) & ? [v0: $i] : (aDimensionOf0(xs) = v0 & $i(v0) & ! [v1: $i] : ! % 20.72/3.51 [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: % 20.72/3.51 $i] : ! [v8: int] : (v8 = 0 | ~ (sdtasasdt0(v2, v2) = v6) | ~ % 20.72/3.51 (sdtasasdt0(v1, v2) = v3) | ~ (sdtasasdt0(v1, v1) = v5) | ~ % 20.72/3.51 (sdtlseqdt0(v4, v7) = v8) | ~ (sdtasdt0(v5, v6) = v7) | ~ (sdtasdt0(v3, % 20.72/3.51 v3) = v4) | ~ $i(v2) | ~ $i(v1) | ? [v9: any] : ? [v10: any] : ? % 20.72/3.51 [v11: $i] : ? [v12: $i] : ? [v13: any] : (aVector0(v2) = v10 & % 20.72/3.51 aVector0(v1) = v9 & aDimensionOf0(v2) = v12 & aDimensionOf0(v1) = v11 & % 20.72/3.51 iLess0(v11, v0) = v13 & $i(v12) & $i(v11) & ( ~ (v13 = 0) | ~ (v12 = % 20.72/3.51 v11) | ~ (v10 = 0) | ~ (v9 = 0))))) % 20.72/3.51 % 20.72/3.51 (m__1678) % 20.72/3.51 aVector0(xt) = 0 & aVector0(xs) = 0 & $i(xt) & $i(xs) % 20.72/3.51 % 20.72/3.51 (m__1678_01) % 20.72/3.51 $i(xt) & $i(xs) & ? [v0: $i] : (aDimensionOf0(xt) = v0 & aDimensionOf0(xs) = % 20.72/3.51 v0 & $i(v0)) % 20.72/3.51 % 20.72/3.51 (m__1692) % 20.72/3.51 $i(xs) & $i(sz00) & ? [v0: $i] : ( ~ (v0 = sz00) & aDimensionOf0(xs) = v0 & % 20.72/3.51 $i(v0)) % 20.72/3.51 % 20.72/3.51 (m__1709) % 20.72/3.51 $i(xp) & $i(xs) & ? [v0: $i] : ? [v1: $i] : (sziznziztdt0(xs) = xp & % 20.72/3.51 aVector0(xp) = 0 & aDimensionOf0(xp) = v0 & aDimensionOf0(xs) = v1 & % 20.72/3.51 szszuzczcdt0(v0) = v1 & $i(v1) & $i(v0) & ! [v2: $i] : ! [v3: $i] : ( ~ % 20.72/3.51 (sdtlbdtrb0(xp, v2) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: $i] : % 20.72/3.51 (sdtlbdtrb0(xs, v2) = v5 & aNaturalNumber0(v2) = v4 & $i(v5) & ( ~ (v4 = % 20.72/3.51 0) | v5 = v3)))) % 20.72/3.51 % 20.72/3.51 (m__1726) % 20.72/3.51 $i(xq) & $i(xt) & ? [v0: $i] : ? [v1: $i] : (sziznziztdt0(xt) = xq & % 20.72/3.51 aVector0(xq) = 0 & aDimensionOf0(xq) = v0 & aDimensionOf0(xt) = v1 & % 20.72/3.51 szszuzczcdt0(v0) = v1 & $i(v1) & $i(v0) & ! [v2: $i] : ! [v3: $i] : ( ~ % 20.72/3.51 (sdtlbdtrb0(xt, v2) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: $i] : % 20.72/3.51 (sdtlbdtrb0(xq, v2) = v5 & aNaturalNumber0(v2) = v4 & $i(v5) & ( ~ (v4 = % 20.72/3.51 0) | v5 = v3)))) % 20.72/3.51 % 20.72/3.51 (m__1746) % 20.72/3.51 $i(xA) & $i(xs) & ? [v0: $i] : (sdtlbdtrb0(xs, v0) = xA & aDimensionOf0(xs) = % 20.72/3.51 v0 & aScalar0(xA) = 0 & $i(v0)) % 20.72/3.51 % 20.72/3.51 (m__1766) % 20.72/3.51 $i(xB) & $i(xt) & ? [v0: $i] : (sdtlbdtrb0(xt, v0) = xB & aDimensionOf0(xt) = % 20.72/3.51 v0 & aScalar0(xB) = 0 & $i(v0)) % 20.72/3.51 % 20.72/3.51 (m__1783) % 20.72/3.51 sdtasasdt0(xp, xp) = xC & aScalar0(xC) = 0 & $i(xC) & $i(xp) % 20.72/3.51 % 20.72/3.51 (m__1800) % 20.72/3.51 sdtasasdt0(xq, xq) = xD & aScalar0(xD) = 0 & $i(xD) & $i(xq) % 20.72/3.51 % 20.72/3.51 (m__1820) % 20.72/3.51 sdtasasdt0(xp, xq) = xE & aScalar0(xE) = 0 & $i(xE) & $i(xq) & $i(xp) % 20.72/3.51 % 20.72/3.51 (function-axioms) % 20.72/3.52 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 20.72/3.52 (sdtasasdt0(v3, v2) = v1) | ~ (sdtasasdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 20.72/3.52 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtlbdtrb0(v3, v2) = v1) % 20.72/3.52 | ~ (sdtlbdtrb0(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 20.72/3.52 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 20.72/3.52 (sdtlseqdt0(v3, v2) = v1) | ~ (sdtlseqdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 20.72/3.52 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) | % 20.72/3.52 ~ (sdtasdt0(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 20.72/3.52 [v3: $i] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 20.72/3.52 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 20.72/3.52 [v3: $i] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) & % 20.72/3.52 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (sziznziztdt0(v2) = v1) % 20.72/3.52 | ~ (sziznziztdt0(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 20.72/3.52 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aVector0(v2) = v1) | ~ % 20.72/3.52 (aVector0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | % 20.72/3.52 ~ (aDimensionOf0(v2) = v1) | ~ (aDimensionOf0(v2) = v0)) & ! [v0: $i] : ! % 20.72/3.52 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (smndt0(v2) = v1) | ~ (smndt0(v2) = % 20.72/3.52 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 20.72/3.52 $i] : (v1 = v0 | ~ (aScalar0(v2) = v1) | ~ (aScalar0(v2) = v0)) & ! [v0: % 20.72/3.52 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (szszuzczcdt0(v2) = v1) | ~ % 20.72/3.52 (szszuzczcdt0(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 20.72/3.52 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) % 20.72/3.52 | ~ (aNaturalNumber0(v2) = v0)) % 20.72/3.52 % 20.72/3.52 Further assumptions not needed in the proof: % 20.72/3.52 -------------------------------------------- % 20.72/3.52 mArith, mDefSPN, mDefSPZ, mDistr, mDistr2, mIHOrd, mLEASm, mLEMon, mLERef, % 20.72/3.52 mLETot, mLETrn, mLess, mMDNeg, mMNeg, mMulSc, mNatExtr, mNatSort, mNegSc, % 20.72/3.52 mPosMon, mSZeroSc, mScPr, mScSort, mScZero, mSqPos, mSqrt, mSuccEqu, mSumSc, % 20.72/3.52 mVcSort, mZeroNat, m__1837, m__1854, m__1873, m__1892, m__1911, m__1930, m__1949 % 20.72/3.52 % 20.72/3.52 Those formulas are unsatisfiable: % 20.72/3.52 --------------------------------- % 20.72/3.52 % 20.72/3.52 Begin of proof % 20.72/3.52 | % 20.72/3.52 | ALPHA: (mSuccNat) implies: % 20.72/3.52 | (1) ! [v0: $i] : ! [v1: $i] : ( ~ (szszuzczcdt0(v0) = v1) | ~ $i(v0) | % 20.72/3.52 | ? [v2: any] : ? [v3: any] : (aNaturalNumber0(v1) = v3 & % 20.72/3.52 | aNaturalNumber0(v0) = v2 & ( ~ (v2 = 0) | (v3 = 0 & ~ (v1 = % 20.72/3.52 | sz00))))) % 20.72/3.52 | % 20.72/3.52 | ALPHA: (mLEMonM) implies: % 20.72/3.52 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 20.72/3.52 | ! [v5: $i] : ! [v6: int] : (v6 = 0 | ~ (sdtlseqdt0(v4, v5) = v6) | ~ % 20.72/3.52 | (sdtasdt0(v1, v3) = v5) | ~ (sdtasdt0(v0, v2) = v4) | ~ $i(v3) | ~ % 20.72/3.52 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v7: any] : ? [v8: any] : ? % 20.72/3.52 | [v9: any] : ? [v10: any] : ? [v11: any] : ? [v12: any] : ? [v13: % 20.72/3.52 | any] : (sdtlseqdt0(v2, v3) = v13 & sdtlseqdt0(v0, v1) = v11 & % 20.72/3.52 | sdtlseqdt0(sz0z00, v2) = v12 & aScalar0(v3) = v10 & aScalar0(v2) = % 20.72/3.52 | v9 & aScalar0(v1) = v8 & aScalar0(v0) = v7 & ( ~ (v13 = 0) | ~ % 20.72/3.52 | (v12 = 0) | ~ (v11 = 0) | ~ (v10 = 0) | ~ (v9 = 0) | ~ (v8 = % 20.72/3.52 | 0) | ~ (v7 = 0)))) % 20.72/3.52 | % 20.72/3.52 | ALPHA: (mDefInit) implies: % 20.72/3.52 | (3) ! [v0: $i] : ! [v1: $i] : ( ~ (sziznziztdt0(v0) = v1) | ~ $i(v0) | % 20.72/3.52 | ? [v2: any] : ? [v3: $i] : (aVector0(v0) = v2 & aDimensionOf0(v0) = % 20.72/3.52 | v3 & $i(v3) & ( ~ (v2 = 0) | v3 = sz00 | ( ! [v4: $i] : (v4 = v1 | % 20.72/3.52 | ~ (aVector0(v4) = 0) | ~ $i(v4) | ? [v5: $i] : ? [v6: $i] % 20.72/3.52 | : ? [v7: $i] : ( ~ (v7 = v6) & sdtlbdtrb0(v4, v5) = v6 & % 20.72/3.52 | sdtlbdtrb0(v0, v5) = v7 & aNaturalNumber0(v5) = 0 & $i(v7) % 20.72/3.52 | & $i(v6) & $i(v5)) | ? [v5: $i] : ? [v6: $i] : ( ~ (v6 = % 20.72/3.52 | v3) & aDimensionOf0(v4) = v5 & szszuzczcdt0(v5) = v6 & % 20.72/3.52 | $i(v6) & $i(v5))) & ! [v4: any] : ( ~ (aVector0(v1) = v4) % 20.72/3.52 | | ~ $i(v1) | (v4 = 0 & ! [v5: $i] : ! [v6: $i] : ( ~ % 20.72/3.52 | (sdtlbdtrb0(v0, v5) = v6) | ~ $i(v5) | ? [v7: any] : ? % 20.72/3.52 | [v8: $i] : (sdtlbdtrb0(v1, v5) = v8 & aNaturalNumber0(v5) % 20.72/3.52 | = v7 & $i(v8) & ( ~ (v7 = 0) | v8 = v6))) & ? [v5: $i] % 20.72/3.52 | : (aDimensionOf0(v1) = v5 & szszuzczcdt0(v5) = v3 & % 20.72/3.52 | $i(v5)))))))) % 20.72/3.52 | % 20.72/3.52 | ALPHA: (mEqInit) implies: % 20.72/3.52 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 20.72/3.52 | (sziznziztdt0(v1) = v3) | ~ (sziznziztdt0(v0) = v2) | ~ $i(v1) | ~ % 20.72/3.52 | $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: $i] : ? [v7: $i] : ? % 20.72/3.52 | [v8: $i] : ? [v9: $i] : (aVector0(v1) = v5 & aVector0(v0) = v4 & % 20.72/3.52 | aDimensionOf0(v3) = v9 & aDimensionOf0(v2) = v8 & aDimensionOf0(v1) % 20.72/3.52 | = v7 & aDimensionOf0(v0) = v6 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & % 20.72/3.52 | ( ~ (v7 = v6) | ~ (v5 = 0) | ~ (v4 = 0) | v9 = v8 | v6 = sz00))) % 20.72/3.52 | % 20.72/3.52 | ALPHA: (mScSqPos) implies: % 20.72/3.53 | (5) ! [v0: $i] : ! [v1: $i] : ( ~ (sdtasasdt0(v0, v0) = v1) | ~ $i(v0) | % 20.72/3.53 | ? [v2: any] : ? [v3: any] : (aVector0(v0) = v2 & sdtlseqdt0(sz0z00, % 20.72/3.53 | v1) = v3 & ( ~ (v2 = 0) | v3 = 0))) % 20.72/3.53 | % 20.72/3.53 | ALPHA: (m__1678) implies: % 20.72/3.53 | (6) aVector0(xs) = 0 % 20.72/3.53 | (7) aVector0(xt) = 0 % 20.72/3.53 | % 20.72/3.53 | ALPHA: (m__1652) implies: % 20.72/3.53 | (8) ? [v0: $i] : (aDimensionOf0(xs) = v0 & $i(v0) & ! [v1: $i] : ! [v2: % 20.72/3.53 | $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! % 20.72/3.53 | [v7: $i] : ! [v8: int] : (v8 = 0 | ~ (sdtasasdt0(v2, v2) = v6) | ~ % 20.72/3.53 | (sdtasasdt0(v1, v2) = v3) | ~ (sdtasasdt0(v1, v1) = v5) | ~ % 20.72/3.53 | (sdtlseqdt0(v4, v7) = v8) | ~ (sdtasdt0(v5, v6) = v7) | ~ % 20.72/3.53 | (sdtasdt0(v3, v3) = v4) | ~ $i(v2) | ~ $i(v1) | ? [v9: any] : ? % 20.72/3.53 | [v10: any] : ? [v11: $i] : ? [v12: $i] : ? [v13: any] : % 20.72/3.53 | (aVector0(v2) = v10 & aVector0(v1) = v9 & aDimensionOf0(v2) = v12 & % 20.72/3.53 | aDimensionOf0(v1) = v11 & iLess0(v11, v0) = v13 & $i(v12) & % 20.72/3.53 | $i(v11) & ( ~ (v13 = 0) | ~ (v12 = v11) | ~ (v10 = 0) | ~ (v9 % 20.72/3.53 | = 0))))) % 20.72/3.53 | % 20.72/3.53 | ALPHA: (m__1678_01) implies: % 20.72/3.53 | (9) ? [v0: $i] : (aDimensionOf0(xt) = v0 & aDimensionOf0(xs) = v0 & % 20.72/3.53 | $i(v0)) % 20.72/3.53 | % 20.72/3.53 | ALPHA: (m__1692) implies: % 20.72/3.53 | (10) ? [v0: $i] : ( ~ (v0 = sz00) & aDimensionOf0(xs) = v0 & $i(v0)) % 20.72/3.53 | % 20.72/3.53 | ALPHA: (m__1709) implies: % 20.72/3.53 | (11) ? [v0: $i] : ? [v1: $i] : (sziznziztdt0(xs) = xp & aVector0(xp) = 0 % 20.72/3.53 | & aDimensionOf0(xp) = v0 & aDimensionOf0(xs) = v1 & szszuzczcdt0(v0) % 20.72/3.53 | = v1 & $i(v1) & $i(v0) & ! [v2: $i] : ! [v3: $i] : ( ~ % 20.72/3.53 | (sdtlbdtrb0(xp, v2) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: $i] % 20.72/3.53 | : (sdtlbdtrb0(xs, v2) = v5 & aNaturalNumber0(v2) = v4 & $i(v5) & ( % 20.72/3.53 | ~ (v4 = 0) | v5 = v3)))) % 20.72/3.53 | % 20.72/3.53 | ALPHA: (m__1726) implies: % 20.72/3.53 | (12) ? [v0: $i] : ? [v1: $i] : (sziznziztdt0(xt) = xq & aVector0(xq) = 0 % 20.72/3.53 | & aDimensionOf0(xq) = v0 & aDimensionOf0(xt) = v1 & szszuzczcdt0(v0) % 20.72/3.53 | = v1 & $i(v1) & $i(v0) & ! [v2: $i] : ! [v3: $i] : ( ~ % 20.72/3.53 | (sdtlbdtrb0(xt, v2) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: $i] % 20.72/3.53 | : (sdtlbdtrb0(xq, v2) = v5 & aNaturalNumber0(v2) = v4 & $i(v5) & ( % 20.72/3.53 | ~ (v4 = 0) | v5 = v3)))) % 20.72/3.53 | % 20.72/3.53 | ALPHA: (m__1746) implies: % 20.72/3.53 | (13) $i(xs) % 20.72/3.53 | (14) ? [v0: $i] : (sdtlbdtrb0(xs, v0) = xA & aDimensionOf0(xs) = v0 & % 20.72/3.53 | aScalar0(xA) = 0 & $i(v0)) % 20.72/3.53 | % 20.72/3.53 | ALPHA: (m__1766) implies: % 20.72/3.53 | (15) $i(xt) % 20.72/3.53 | (16) ? [v0: $i] : (sdtlbdtrb0(xt, v0) = xB & aDimensionOf0(xt) = v0 & % 20.72/3.53 | aScalar0(xB) = 0 & $i(v0)) % 20.72/3.53 | % 20.72/3.53 | ALPHA: (m__1783) implies: % 20.72/3.53 | (17) sdtasasdt0(xp, xp) = xC % 20.72/3.53 | % 20.72/3.53 | ALPHA: (m__1800) implies: % 20.72/3.53 | (18) sdtasasdt0(xq, xq) = xD % 20.72/3.53 | % 20.72/3.53 | ALPHA: (m__1820) implies: % 20.72/3.53 | (19) $i(xp) % 20.72/3.53 | (20) $i(xq) % 20.72/3.53 | (21) sdtasasdt0(xp, xq) = xE % 20.72/3.53 | % 20.72/3.53 | ALPHA: (m__) implies: % 20.72/3.53 | (22) $i(xC) % 20.72/3.53 | (23) $i(xD) % 20.72/3.53 | (24) $i(xE) % 20.72/3.53 | (25) ? [v0: $i] : ? [v1: $i] : ? [v2: int] : ( ~ (v2 = 0) & % 20.72/3.53 | sdtlseqdt0(v0, v1) = v2 & sdtasdt0(xE, xE) = v0 & sdtasdt0(xC, xD) = % 20.72/3.53 | v1 & $i(v1) & $i(v0)) % 20.72/3.53 | % 20.72/3.53 | ALPHA: (function-axioms) implies: % 20.72/3.54 | (26) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 20.72/3.54 | : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = % 20.72/3.54 | v0)) % 20.72/3.54 | (27) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 20.72/3.54 | (aDimensionOf0(v2) = v1) | ~ (aDimensionOf0(v2) = v0)) % 20.72/3.54 | (28) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 20.72/3.54 | : (v1 = v0 | ~ (aVector0(v2) = v1) | ~ (aVector0(v2) = v0)) % 20.72/3.54 | % 20.72/3.54 | DELTA: instantiating (9) with fresh symbol all_33_0 gives: % 20.72/3.54 | (29) aDimensionOf0(xt) = all_33_0 & aDimensionOf0(xs) = all_33_0 & % 20.72/3.54 | $i(all_33_0) % 20.72/3.54 | % 20.72/3.54 | ALPHA: (29) implies: % 20.72/3.54 | (30) aDimensionOf0(xs) = all_33_0 % 20.72/3.54 | (31) aDimensionOf0(xt) = all_33_0 % 20.72/3.54 | % 20.72/3.54 | DELTA: instantiating (10) with fresh symbol all_35_0 gives: % 20.72/3.54 | (32) ~ (all_35_0 = sz00) & aDimensionOf0(xs) = all_35_0 & $i(all_35_0) % 20.72/3.54 | % 20.72/3.54 | ALPHA: (32) implies: % 20.72/3.54 | (33) ~ (all_35_0 = sz00) % 20.72/3.54 | (34) $i(all_35_0) % 20.72/3.54 | (35) aDimensionOf0(xs) = all_35_0 % 20.72/3.54 | % 20.72/3.54 | DELTA: instantiating (16) with fresh symbol all_37_0 gives: % 20.72/3.54 | (36) sdtlbdtrb0(xt, all_37_0) = xB & aDimensionOf0(xt) = all_37_0 & % 20.72/3.54 | aScalar0(xB) = 0 & $i(all_37_0) % 20.72/3.54 | % 20.72/3.54 | ALPHA: (36) implies: % 20.72/3.54 | (37) aDimensionOf0(xt) = all_37_0 % 20.72/3.54 | (38) sdtlbdtrb0(xt, all_37_0) = xB % 20.72/3.54 | % 20.72/3.54 | DELTA: instantiating (14) with fresh symbol all_39_0 gives: % 20.72/3.54 | (39) sdtlbdtrb0(xs, all_39_0) = xA & aDimensionOf0(xs) = all_39_0 & % 20.72/3.54 | aScalar0(xA) = 0 & $i(all_39_0) % 20.72/3.54 | % 20.72/3.54 | ALPHA: (39) implies: % 20.72/3.54 | (40) aDimensionOf0(xs) = all_39_0 % 20.72/3.54 | (41) sdtlbdtrb0(xs, all_39_0) = xA % 20.72/3.54 | % 20.72/3.54 | DELTA: instantiating (25) with fresh symbols all_41_0, all_41_1, all_41_2 % 20.72/3.54 | gives: % 20.72/3.54 | (42) ~ (all_41_0 = 0) & sdtlseqdt0(all_41_2, all_41_1) = all_41_0 & % 20.72/3.54 | sdtasdt0(xE, xE) = all_41_2 & sdtasdt0(xC, xD) = all_41_1 & % 20.72/3.54 | $i(all_41_1) & $i(all_41_2) % 20.72/3.54 | % 20.72/3.54 | ALPHA: (42) implies: % 20.72/3.54 | (43) ~ (all_41_0 = 0) % 20.72/3.54 | (44) sdtasdt0(xC, xD) = all_41_1 % 20.72/3.54 | (45) sdtasdt0(xE, xE) = all_41_2 % 20.72/3.54 | (46) sdtlseqdt0(all_41_2, all_41_1) = all_41_0 % 20.72/3.54 | % 20.72/3.54 | DELTA: instantiating (12) with fresh symbols all_43_0, all_43_1 gives: % 20.72/3.54 | (47) sziznziztdt0(xt) = xq & aVector0(xq) = 0 & aDimensionOf0(xq) = % 20.72/3.54 | all_43_1 & aDimensionOf0(xt) = all_43_0 & szszuzczcdt0(all_43_1) = % 20.72/3.54 | all_43_0 & $i(all_43_0) & $i(all_43_1) & ! [v0: $i] : ! [v1: $i] : ( % 20.72/3.54 | ~ (sdtlbdtrb0(xt, v0) = v1) | ~ $i(v0) | ? [v2: any] : ? [v3: $i] % 20.72/3.54 | : (sdtlbdtrb0(xq, v0) = v3 & aNaturalNumber0(v0) = v2 & $i(v3) & ( ~ % 20.72/3.54 | (v2 = 0) | v3 = v1))) % 20.72/3.54 | % 20.72/3.54 | ALPHA: (47) implies: % 20.72/3.54 | (48) $i(all_43_1) % 20.72/3.54 | (49) szszuzczcdt0(all_43_1) = all_43_0 % 20.72/3.54 | (50) aDimensionOf0(xt) = all_43_0 % 20.72/3.54 | (51) aDimensionOf0(xq) = all_43_1 % 20.72/3.54 | (52) aVector0(xq) = 0 % 20.72/3.54 | (53) sziznziztdt0(xt) = xq % 20.72/3.54 | % 20.72/3.54 | DELTA: instantiating (11) with fresh symbols all_46_0, all_46_1 gives: % 20.72/3.54 | (54) sziznziztdt0(xs) = xp & aVector0(xp) = 0 & aDimensionOf0(xp) = % 20.72/3.54 | all_46_1 & aDimensionOf0(xs) = all_46_0 & szszuzczcdt0(all_46_1) = % 20.72/3.54 | all_46_0 & $i(all_46_0) & $i(all_46_1) & ! [v0: $i] : ! [v1: $i] : ( % 20.72/3.54 | ~ (sdtlbdtrb0(xp, v0) = v1) | ~ $i(v0) | ? [v2: any] : ? [v3: $i] % 20.72/3.54 | : (sdtlbdtrb0(xs, v0) = v3 & aNaturalNumber0(v0) = v2 & $i(v3) & ( ~ % 20.72/3.54 | (v2 = 0) | v3 = v1))) % 20.72/3.54 | % 20.72/3.54 | ALPHA: (54) implies: % 20.72/3.54 | (55) $i(all_46_1) % 20.72/3.54 | (56) szszuzczcdt0(all_46_1) = all_46_0 % 20.72/3.54 | (57) aDimensionOf0(xs) = all_46_0 % 20.72/3.55 | (58) aDimensionOf0(xp) = all_46_1 % 20.72/3.55 | (59) aVector0(xp) = 0 % 20.72/3.55 | (60) sziznziztdt0(xs) = xp % 20.72/3.55 | % 20.72/3.55 | DELTA: instantiating (8) with fresh symbol all_49_0 gives: % 20.72/3.55 | (61) aDimensionOf0(xs) = all_49_0 & $i(all_49_0) & ! [v0: $i] : ! [v1: % 20.72/3.55 | $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! % 20.72/3.55 | [v6: $i] : ! [v7: int] : (v7 = 0 | ~ (sdtasasdt0(v1, v1) = v5) | ~ % 20.72/3.55 | (sdtasasdt0(v0, v1) = v2) | ~ (sdtasasdt0(v0, v0) = v4) | ~ % 20.72/3.55 | (sdtlseqdt0(v3, v6) = v7) | ~ (sdtasdt0(v4, v5) = v6) | ~ % 20.72/3.55 | (sdtasdt0(v2, v2) = v3) | ~ $i(v1) | ~ $i(v0) | ? [v8: any] : ? % 20.72/3.55 | [v9: any] : ? [v10: $i] : ? [v11: $i] : ? [v12: any] : % 20.72/3.55 | (aVector0(v1) = v9 & aVector0(v0) = v8 & aDimensionOf0(v1) = v11 & % 20.72/3.55 | aDimensionOf0(v0) = v10 & iLess0(v10, all_49_0) = v12 & $i(v11) & % 20.72/3.55 | $i(v10) & ( ~ (v12 = 0) | ~ (v11 = v10) | ~ (v9 = 0) | ~ (v8 = % 20.72/3.55 | 0)))) % 20.72/3.55 | % 20.72/3.55 | ALPHA: (61) implies: % 20.72/3.55 | (62) aDimensionOf0(xs) = all_49_0 % 20.72/3.55 | (63) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 20.72/3.55 | ! [v5: $i] : ! [v6: $i] : ! [v7: int] : (v7 = 0 | ~ (sdtasasdt0(v1, % 20.72/3.55 | v1) = v5) | ~ (sdtasasdt0(v0, v1) = v2) | ~ (sdtasasdt0(v0, % 20.72/3.55 | v0) = v4) | ~ (sdtlseqdt0(v3, v6) = v7) | ~ (sdtasdt0(v4, v5) % 20.72/3.55 | = v6) | ~ (sdtasdt0(v2, v2) = v3) | ~ $i(v1) | ~ $i(v0) | ? % 20.72/3.55 | [v8: any] : ? [v9: any] : ? [v10: $i] : ? [v11: $i] : ? [v12: % 20.72/3.55 | any] : (aVector0(v1) = v9 & aVector0(v0) = v8 & aDimensionOf0(v1) % 20.72/3.55 | = v11 & aDimensionOf0(v0) = v10 & iLess0(v10, all_49_0) = v12 & % 20.72/3.55 | $i(v11) & $i(v10) & ( ~ (v12 = 0) | ~ (v11 = v10) | ~ (v9 = 0) | % 20.72/3.55 | ~ (v8 = 0)))) % 20.72/3.55 | % 20.72/3.55 | GROUND_INST: instantiating (27) with all_39_0, all_46_0, xs, simplifying with % 20.72/3.55 | (40), (57) gives: % 20.72/3.55 | (64) all_46_0 = all_39_0 % 20.72/3.55 | % 20.72/3.55 | GROUND_INST: instantiating (27) with all_35_0, all_46_0, xs, simplifying with % 20.72/3.55 | (35), (57) gives: % 20.72/3.55 | (65) all_46_0 = all_35_0 % 20.72/3.55 | % 20.72/3.55 | GROUND_INST: instantiating (27) with all_46_0, all_49_0, xs, simplifying with % 20.72/3.55 | (57), (62) gives: % 20.72/3.55 | (66) all_49_0 = all_46_0 % 20.72/3.55 | % 20.72/3.55 | GROUND_INST: instantiating (27) with all_33_0, all_49_0, xs, simplifying with % 20.72/3.55 | (30), (62) gives: % 20.72/3.55 | (67) all_49_0 = all_33_0 % 20.72/3.55 | % 20.72/3.55 | GROUND_INST: instantiating (27) with all_37_0, all_43_0, xt, simplifying with % 20.72/3.55 | (37), (50) gives: % 20.72/3.55 | (68) all_43_0 = all_37_0 % 20.72/3.55 | % 20.72/3.55 | GROUND_INST: instantiating (27) with all_33_0, all_43_0, xt, simplifying with % 20.72/3.55 | (31), (50) gives: % 20.72/3.55 | (69) all_43_0 = all_33_0 % 20.72/3.55 | % 20.72/3.55 | COMBINE_EQS: (66), (67) imply: % 20.72/3.55 | (70) all_46_0 = all_33_0 % 20.72/3.55 | % 20.72/3.55 | SIMP: (70) implies: % 20.72/3.55 | (71) all_46_0 = all_33_0 % 20.72/3.55 | % 20.72/3.55 | COMBINE_EQS: (64), (65) imply: % 20.72/3.55 | (72) all_39_0 = all_35_0 % 20.72/3.55 | % 20.72/3.55 | COMBINE_EQS: (64), (71) imply: % 20.72/3.55 | (73) all_39_0 = all_33_0 % 20.72/3.55 | % 20.72/3.55 | COMBINE_EQS: (68), (69) imply: % 20.72/3.55 | (74) all_37_0 = all_33_0 % 20.72/3.55 | % 20.72/3.55 | SIMP: (74) implies: % 20.72/3.55 | (75) all_37_0 = all_33_0 % 20.72/3.55 | % 20.72/3.55 | COMBINE_EQS: (72), (73) imply: % 20.72/3.55 | (76) all_35_0 = all_33_0 % 20.72/3.55 | % 20.72/3.55 | SIMP: (76) implies: % 20.72/3.55 | (77) all_35_0 = all_33_0 % 20.72/3.55 | % 20.72/3.55 | REDUCE: (33), (77) imply: % 20.72/3.55 | (78) ~ (all_33_0 = sz00) % 20.72/3.55 | % 20.72/3.55 | REDUCE: (38), (75) imply: % 20.72/3.55 | (79) sdtlbdtrb0(xt, all_33_0) = xB % 20.72/3.55 | % 20.72/3.55 | REDUCE: (41), (73) imply: % 20.72/3.55 | (80) sdtlbdtrb0(xs, all_33_0) = xA % 20.72/3.55 | % 20.72/3.55 | REDUCE: (56), (71) imply: % 20.72/3.55 | (81) szszuzczcdt0(all_46_1) = all_33_0 % 20.72/3.55 | % 20.72/3.55 | REDUCE: (49), (69) imply: % 20.72/3.55 | (82) szszuzczcdt0(all_43_1) = all_33_0 % 20.72/3.55 | % 20.72/3.55 | REDUCE: (34), (77) imply: % 20.72/3.55 | (83) $i(all_33_0) % 20.72/3.55 | % 20.72/3.55 | GROUND_INST: instantiating (1) with all_43_1, all_33_0, simplifying with (48), % 20.72/3.55 | (82) gives: % 20.72/3.55 | (84) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(all_43_1) = v0 & % 20.72/3.55 | aNaturalNumber0(all_33_0) = v1 & ( ~ (v0 = 0) | (v1 = 0 & ~ % 20.72/3.55 | (all_33_0 = sz00)))) % 20.72/3.55 | % 20.72/3.55 | GROUND_INST: instantiating (1) with all_46_1, all_33_0, simplifying with (55), % 20.72/3.55 | (81) gives: % 20.72/3.55 | (85) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(all_46_1) = v0 & % 20.72/3.55 | aNaturalNumber0(all_33_0) = v1 & ( ~ (v0 = 0) | (v1 = 0 & ~ % 20.72/3.55 | (all_33_0 = sz00)))) % 20.72/3.55 | % 20.72/3.55 | GROUND_INST: instantiating (2) with xE, xC, xE, xD, all_41_2, all_41_1, % 20.72/3.55 | all_41_0, simplifying with (22), (23), (24), (44), (45), (46) % 20.72/3.55 | gives: % 20.72/3.55 | (86) all_41_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: % 20.72/3.55 | any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : (sdtlseqdt0(xE, % 20.72/3.56 | xD) = v6 & sdtlseqdt0(xE, xC) = v4 & sdtlseqdt0(sz0z00, xE) = v5 & % 20.72/3.56 | aScalar0(xE) = v2 & aScalar0(xE) = v0 & aScalar0(xD) = v3 & % 20.72/3.56 | aScalar0(xC) = v1 & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | ~ % 20.72/3.56 | (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 20.72/3.56 | % 20.72/3.56 | GROUND_INST: instantiating (mDimNat) with xs, simplifying with (6), (13) % 20.72/3.56 | gives: % 20.72/3.56 | (87) ? [v0: $i] : (aDimensionOf0(xs) = v0 & aNaturalNumber0(v0) = 0 & % 20.72/3.56 | $i(v0)) % 20.72/3.56 | % 20.72/3.56 | GROUND_INST: instantiating (mDimNat) with xt, simplifying with (7), (15) % 20.72/3.56 | gives: % 20.72/3.56 | (88) ? [v0: $i] : (aDimensionOf0(xt) = v0 & aNaturalNumber0(v0) = 0 & % 20.72/3.56 | $i(v0)) % 20.72/3.56 | % 20.72/3.56 | GROUND_INST: instantiating (mDimNat) with xp, simplifying with (19), (59) % 20.72/3.56 | gives: % 20.72/3.56 | (89) ? [v0: $i] : (aDimensionOf0(xp) = v0 & aNaturalNumber0(v0) = 0 & % 20.72/3.56 | $i(v0)) % 20.72/3.56 | % 20.72/3.56 | GROUND_INST: instantiating (mDimNat) with xq, simplifying with (20), (52) % 20.72/3.56 | gives: % 20.72/3.56 | (90) ? [v0: $i] : (aDimensionOf0(xq) = v0 & aNaturalNumber0(v0) = 0 & % 20.72/3.56 | $i(v0)) % 20.72/3.56 | % 20.72/3.56 | GROUND_INST: instantiating (mElmSc) with xs, all_33_0, xA, simplifying with % 20.72/3.56 | (13), (80), (83) gives: % 20.72/3.56 | (91) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aVector0(xs) = v0 & % 20.72/3.56 | aScalar0(xA) = v2 & aNaturalNumber0(all_33_0) = v1 & ( ~ (v1 = 0) | % 20.72/3.56 | ~ (v0 = 0) | v2 = 0)) % 20.72/3.56 | % 20.72/3.56 | GROUND_INST: instantiating (mElmSc) with xt, all_33_0, xB, simplifying with % 20.72/3.56 | (15), (79), (83) gives: % 20.72/3.56 | (92) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aVector0(xt) = v0 & % 20.72/3.56 | aScalar0(xB) = v2 & aNaturalNumber0(all_33_0) = v1 & ( ~ (v1 = 0) | % 20.72/3.56 | ~ (v0 = 0) | v2 = 0)) % 20.72/3.56 | % 20.72/3.56 | GROUND_INST: instantiating (3) with xs, xp, simplifying with (13), (60) gives: % 20.72/3.56 | (93) ? [v0: any] : ? [v1: $i] : (aVector0(xs) = v0 & aDimensionOf0(xs) = % 20.72/3.56 | v1 & $i(v1) & ( ~ (v0 = 0) | v1 = sz00 | ( ! [v2: $i] : (v2 = xp | % 20.72/3.56 | ~ (aVector0(v2) = 0) | ~ $i(v2) | ? [v3: $i] : ? [v4: $i] : % 20.72/3.56 | ? [v5: $i] : ( ~ (v5 = v4) & sdtlbdtrb0(v2, v3) = v4 & % 20.72/3.56 | sdtlbdtrb0(xs, v3) = v5 & aNaturalNumber0(v3) = 0 & $i(v5) & % 20.72/3.56 | $i(v4) & $i(v3)) | ? [v3: $i] : ? [v4: $i] : ( ~ (v4 = v1) % 20.72/3.56 | & aDimensionOf0(v2) = v3 & szszuzczcdt0(v3) = v4 & $i(v4) & % 20.72/3.56 | $i(v3))) & ! [v2: any] : ( ~ (aVector0(xp) = v2) | ~ % 20.72/3.56 | $i(xp) | (v2 = 0 & ! [v3: $i] : ! [v4: $i] : ( ~ % 20.72/3.56 | (sdtlbdtrb0(xs, v3) = v4) | ~ $i(v3) | ? [v5: any] : ? % 20.72/3.56 | [v6: $i] : (sdtlbdtrb0(xp, v3) = v6 & aNaturalNumber0(v3) % 20.72/3.56 | = v5 & $i(v6) & ( ~ (v5 = 0) | v6 = v4))) & ? [v3: $i] % 20.72/3.56 | : (aDimensionOf0(xp) = v3 & szszuzczcdt0(v3) = v1 & % 20.72/3.56 | $i(v3))))))) % 20.72/3.56 | % 20.72/3.56 | GROUND_INST: instantiating (4) with xs, xt, xp, xq, simplifying with (13), % 20.72/3.56 | (15), (53), (60) gives: % 20.72/3.56 | (94) ? [v0: any] : ? [v1: any] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] % 20.72/3.56 | : ? [v5: $i] : (aVector0(xt) = v1 & aVector0(xs) = v0 & % 20.72/3.56 | aDimensionOf0(xq) = v5 & aDimensionOf0(xp) = v4 & aDimensionOf0(xt) % 20.72/3.56 | = v3 & aDimensionOf0(xs) = v2 & $i(v5) & $i(v4) & $i(v3) & $i(v2) & % 20.72/3.56 | ( ~ (v3 = v2) | ~ (v1 = 0) | ~ (v0 = 0) | v5 = v4 | v2 = sz00)) % 20.72/3.56 | % 20.72/3.56 | GROUND_INST: instantiating (4) with xt, xs, xq, xp, simplifying with (13), % 20.72/3.56 | (15), (53), (60) gives: % 20.72/3.56 | (95) ? [v0: any] : ? [v1: any] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] % 20.72/3.56 | : ? [v5: $i] : (aVector0(xt) = v0 & aVector0(xs) = v1 & % 20.72/3.56 | aDimensionOf0(xq) = v4 & aDimensionOf0(xp) = v5 & aDimensionOf0(xt) % 20.72/3.56 | = v2 & aDimensionOf0(xs) = v3 & $i(v5) & $i(v4) & $i(v3) & $i(v2) & % 20.72/3.56 | ( ~ (v3 = v2) | ~ (v1 = 0) | ~ (v0 = 0) | v5 = v4 | v2 = sz00)) % 20.72/3.56 | % 20.72/3.56 | GROUND_INST: instantiating (3) with xt, xq, simplifying with (15), (53) gives: % 20.72/3.56 | (96) ? [v0: any] : ? [v1: $i] : (aVector0(xt) = v0 & aDimensionOf0(xt) = % 20.72/3.56 | v1 & $i(v1) & ( ~ (v0 = 0) | v1 = sz00 | ( ! [v2: $i] : (v2 = xq | % 20.72/3.56 | ~ (aVector0(v2) = 0) | ~ $i(v2) | ? [v3: $i] : ? [v4: $i] : % 20.72/3.56 | ? [v5: $i] : ( ~ (v5 = v4) & sdtlbdtrb0(v2, v3) = v4 & % 20.72/3.56 | sdtlbdtrb0(xt, v3) = v5 & aNaturalNumber0(v3) = 0 & $i(v5) & % 20.72/3.56 | $i(v4) & $i(v3)) | ? [v3: $i] : ? [v4: $i] : ( ~ (v4 = v1) % 20.72/3.56 | & aDimensionOf0(v2) = v3 & szszuzczcdt0(v3) = v4 & $i(v4) & % 20.72/3.56 | $i(v3))) & ! [v2: any] : ( ~ (aVector0(xq) = v2) | ~ % 20.72/3.56 | $i(xq) | (v2 = 0 & ! [v3: $i] : ! [v4: $i] : ( ~ % 20.72/3.56 | (sdtlbdtrb0(xt, v3) = v4) | ~ $i(v3) | ? [v5: any] : ? % 20.72/3.56 | [v6: $i] : (sdtlbdtrb0(xq, v3) = v6 & aNaturalNumber0(v3) % 20.72/3.56 | = v5 & $i(v6) & ( ~ (v5 = 0) | v6 = v4))) & ? [v3: $i] % 20.72/3.56 | : (aDimensionOf0(xq) = v3 & szszuzczcdt0(v3) = v1 & % 20.72/3.56 | $i(v3))))))) % 20.72/3.56 | % 20.72/3.56 | GROUND_INST: instantiating (63) with xp, xq, xE, all_41_2, xC, xD, all_41_1, % 20.72/3.56 | all_41_0, simplifying with (17), (18), (19), (20), (21), (44), % 20.72/3.56 | (45), (46) gives: % 20.72/3.56 | (97) all_41_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: $i] : ? [v3: $i] % 20.72/3.56 | : ? [v4: any] : (aVector0(xq) = v1 & aVector0(xp) = v0 & % 20.72/3.56 | aDimensionOf0(xq) = v3 & aDimensionOf0(xp) = v2 & iLess0(v2, % 20.72/3.56 | all_49_0) = v4 & $i(v3) & $i(v2) & ( ~ (v4 = 0) | ~ (v3 = v2) | % 20.72/3.56 | ~ (v1 = 0) | ~ (v0 = 0))) % 20.72/3.56 | % 20.72/3.56 | GROUND_INST: instantiating (5) with xq, xD, simplifying with (18), (20) gives: % 20.72/3.56 | (98) ? [v0: any] : ? [v1: any] : (aVector0(xq) = v0 & sdtlseqdt0(sz0z00, % 20.72/3.56 | xD) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 20.72/3.56 | % 20.72/3.56 | DELTA: instantiating (90) with fresh symbol all_64_0 gives: % 21.16/3.56 | (99) aDimensionOf0(xq) = all_64_0 & aNaturalNumber0(all_64_0) = 0 & % 21.16/3.56 | $i(all_64_0) % 21.16/3.56 | % 21.16/3.56 | ALPHA: (99) implies: % 21.16/3.56 | (100) aDimensionOf0(xq) = all_64_0 % 21.16/3.56 | % 21.16/3.56 | DELTA: instantiating (89) with fresh symbol all_66_0 gives: % 21.16/3.56 | (101) aDimensionOf0(xp) = all_66_0 & aNaturalNumber0(all_66_0) = 0 & % 21.16/3.56 | $i(all_66_0) % 21.16/3.56 | % 21.16/3.56 | ALPHA: (101) implies: % 21.16/3.56 | (102) aNaturalNumber0(all_66_0) = 0 % 21.16/3.56 | (103) aDimensionOf0(xp) = all_66_0 % 21.16/3.56 | % 21.16/3.56 | DELTA: instantiating (88) with fresh symbol all_68_0 gives: % 21.16/3.56 | (104) aDimensionOf0(xt) = all_68_0 & aNaturalNumber0(all_68_0) = 0 & % 21.16/3.56 | $i(all_68_0) % 21.16/3.56 | % 21.16/3.57 | ALPHA: (104) implies: % 21.16/3.57 | (105) aDimensionOf0(xt) = all_68_0 % 21.16/3.57 | % 21.16/3.57 | DELTA: instantiating (87) with fresh symbol all_70_0 gives: % 21.16/3.57 | (106) aDimensionOf0(xs) = all_70_0 & aNaturalNumber0(all_70_0) = 0 & % 21.16/3.57 | $i(all_70_0) % 21.16/3.57 | % 21.16/3.57 | ALPHA: (106) implies: % 21.16/3.57 | (107) aDimensionOf0(xs) = all_70_0 % 21.16/3.57 | % 21.16/3.57 | DELTA: instantiating (98) with fresh symbols all_74_0, all_74_1 gives: % 21.16/3.57 | (108) aVector0(xq) = all_74_1 & sdtlseqdt0(sz0z00, xD) = all_74_0 & ( ~ % 21.16/3.57 | (all_74_1 = 0) | all_74_0 = 0) % 21.16/3.57 | % 21.16/3.57 | ALPHA: (108) implies: % 21.16/3.57 | (109) aVector0(xq) = all_74_1 % 21.16/3.57 | % 21.16/3.57 | DELTA: instantiating (85) with fresh symbols all_86_0, all_86_1 gives: % 21.16/3.57 | (110) aNaturalNumber0(all_46_1) = all_86_1 & aNaturalNumber0(all_33_0) = % 21.16/3.57 | all_86_0 & ( ~ (all_86_1 = 0) | (all_86_0 = 0 & ~ (all_33_0 = % 21.16/3.57 | sz00))) % 21.16/3.57 | % 21.16/3.57 | ALPHA: (110) implies: % 21.16/3.57 | (111) aNaturalNumber0(all_46_1) = all_86_1 % 21.16/3.57 | % 21.16/3.57 | DELTA: instantiating (84) with fresh symbols all_88_0, all_88_1 gives: % 21.16/3.57 | (112) aNaturalNumber0(all_43_1) = all_88_1 & aNaturalNumber0(all_33_0) = % 21.16/3.57 | all_88_0 & ( ~ (all_88_1 = 0) | (all_88_0 = 0 & ~ (all_33_0 = % 21.16/3.57 | sz00))) % 21.16/3.57 | % 21.16/3.57 | ALPHA: (112) implies: % 21.16/3.57 | (113) aNaturalNumber0(all_43_1) = all_88_1 % 21.16/3.57 | % 21.16/3.57 | DELTA: instantiating (91) with fresh symbols all_90_0, all_90_1, all_90_2 % 21.16/3.57 | gives: % 21.16/3.57 | (114) aVector0(xs) = all_90_2 & aScalar0(xA) = all_90_0 & % 21.16/3.57 | aNaturalNumber0(all_33_0) = all_90_1 & ( ~ (all_90_1 = 0) | ~ % 21.16/3.57 | (all_90_2 = 0) | all_90_0 = 0) % 21.16/3.57 | % 21.16/3.57 | ALPHA: (114) implies: % 21.16/3.57 | (115) aVector0(xs) = all_90_2 % 21.16/3.57 | % 21.16/3.57 | DELTA: instantiating (92) with fresh symbols all_94_0, all_94_1, all_94_2 % 21.16/3.57 | gives: % 21.16/3.57 | (116) aVector0(xt) = all_94_2 & aScalar0(xB) = all_94_0 & % 21.16/3.57 | aNaturalNumber0(all_33_0) = all_94_1 & ( ~ (all_94_1 = 0) | ~ % 21.16/3.57 | (all_94_2 = 0) | all_94_0 = 0) % 21.16/3.57 | % 21.16/3.57 | ALPHA: (116) implies: % 21.16/3.57 | (117) aVector0(xt) = all_94_2 % 21.16/3.57 | % 21.16/3.57 | DELTA: instantiating (95) with fresh symbols all_98_0, all_98_1, all_98_2, % 21.16/3.57 | all_98_3, all_98_4, all_98_5 gives: % 21.16/3.57 | (118) aVector0(xt) = all_98_5 & aVector0(xs) = all_98_4 & aDimensionOf0(xq) % 21.16/3.57 | = all_98_1 & aDimensionOf0(xp) = all_98_0 & aDimensionOf0(xt) = % 21.16/3.57 | all_98_3 & aDimensionOf0(xs) = all_98_2 & $i(all_98_0) & $i(all_98_1) % 21.16/3.57 | & $i(all_98_2) & $i(all_98_3) & ( ~ (all_98_2 = all_98_3) | ~ % 21.16/3.57 | (all_98_4 = 0) | ~ (all_98_5 = 0) | all_98_0 = all_98_1 | all_98_3 % 21.16/3.57 | = sz00) % 21.16/3.57 | % 21.16/3.57 | ALPHA: (118) implies: % 21.16/3.57 | (119) aDimensionOf0(xs) = all_98_2 % 21.16/3.57 | (120) aDimensionOf0(xt) = all_98_3 % 21.16/3.57 | (121) aDimensionOf0(xp) = all_98_0 % 21.16/3.57 | (122) aDimensionOf0(xq) = all_98_1 % 21.16/3.57 | (123) aVector0(xs) = all_98_4 % 21.16/3.57 | (124) aVector0(xt) = all_98_5 % 21.16/3.57 | % 21.16/3.57 | DELTA: instantiating (94) with fresh symbols all_100_0, all_100_1, all_100_2, % 21.16/3.57 | all_100_3, all_100_4, all_100_5 gives: % 21.16/3.57 | (125) aVector0(xt) = all_100_4 & aVector0(xs) = all_100_5 & % 21.16/3.57 | aDimensionOf0(xq) = all_100_0 & aDimensionOf0(xp) = all_100_1 & % 21.16/3.57 | aDimensionOf0(xt) = all_100_2 & aDimensionOf0(xs) = all_100_3 & % 21.16/3.57 | $i(all_100_0) & $i(all_100_1) & $i(all_100_2) & $i(all_100_3) & ( ~ % 21.16/3.57 | (all_100_2 = all_100_3) | ~ (all_100_4 = 0) | ~ (all_100_5 = 0) | % 21.16/3.57 | all_100_0 = all_100_1 | all_100_3 = sz00) % 21.16/3.57 | % 21.16/3.57 | ALPHA: (125) implies: % 21.16/3.57 | (126) aDimensionOf0(xs) = all_100_3 % 21.16/3.57 | (127) aDimensionOf0(xt) = all_100_2 % 21.16/3.57 | (128) aDimensionOf0(xp) = all_100_1 % 21.16/3.57 | (129) aDimensionOf0(xq) = all_100_0 % 21.16/3.57 | (130) aVector0(xs) = all_100_5 % 21.16/3.57 | (131) aVector0(xt) = all_100_4 % 21.16/3.57 | (132) ~ (all_100_2 = all_100_3) | ~ (all_100_4 = 0) | ~ (all_100_5 = 0) % 21.16/3.57 | | all_100_0 = all_100_1 | all_100_3 = sz00 % 21.16/3.57 | % 21.16/3.57 | DELTA: instantiating (96) with fresh symbols all_102_0, all_102_1 gives: % 21.16/3.57 | (133) aVector0(xt) = all_102_1 & aDimensionOf0(xt) = all_102_0 & % 21.16/3.57 | $i(all_102_0) & ( ~ (all_102_1 = 0) | all_102_0 = sz00 | ( ! [v0: $i] % 21.16/3.57 | : (v0 = xq | ~ (aVector0(v0) = 0) | ~ $i(v0) | ? [v1: $i] : ? % 21.16/3.57 | [v2: $i] : ? [v3: $i] : ( ~ (v3 = v2) & sdtlbdtrb0(v0, v1) = % 21.16/3.57 | v2 & sdtlbdtrb0(xt, v1) = v3 & aNaturalNumber0(v1) = 0 & % 21.16/3.57 | $i(v3) & $i(v2) & $i(v1)) | ? [v1: $i] : ? [v2: any] : ( ~ % 21.16/3.57 | (v2 = all_102_0) & aDimensionOf0(v0) = v1 & szszuzczcdt0(v1) % 21.16/3.57 | = v2 & $i(v2) & $i(v1))) & ! [v0: any] : ( ~ (aVector0(xq) = % 21.16/3.57 | v0) | ~ $i(xq) | (v0 = 0 & ! [v1: $i] : ! [v2: $i] : ( ~ % 21.16/3.57 | (sdtlbdtrb0(xt, v1) = v2) | ~ $i(v1) | ? [v3: any] : ? % 21.16/3.57 | [v4: $i] : (sdtlbdtrb0(xq, v1) = v4 & aNaturalNumber0(v1) = % 21.16/3.57 | v3 & $i(v4) & ( ~ (v3 = 0) | v4 = v2))) & ? [v1: $i] : % 21.16/3.57 | (aDimensionOf0(xq) = v1 & szszuzczcdt0(v1) = all_102_0 & % 21.16/3.57 | $i(v1)))))) % 21.16/3.57 | % 21.16/3.57 | ALPHA: (133) implies: % 21.16/3.57 | (134) aDimensionOf0(xt) = all_102_0 % 21.16/3.57 | (135) aVector0(xt) = all_102_1 % 21.16/3.57 | (136) ~ (all_102_1 = 0) | all_102_0 = sz00 | ( ! [v0: $i] : (v0 = xq | ~ % 21.16/3.57 | (aVector0(v0) = 0) | ~ $i(v0) | ? [v1: $i] : ? [v2: $i] : ? % 21.16/3.57 | [v3: $i] : ( ~ (v3 = v2) & sdtlbdtrb0(v0, v1) = v2 & % 21.16/3.57 | sdtlbdtrb0(xt, v1) = v3 & aNaturalNumber0(v1) = 0 & $i(v3) & % 21.16/3.57 | $i(v2) & $i(v1)) | ? [v1: $i] : ? [v2: any] : ( ~ (v2 = % 21.16/3.57 | all_102_0) & aDimensionOf0(v0) = v1 & szszuzczcdt0(v1) = v2 & % 21.16/3.57 | $i(v2) & $i(v1))) & ! [v0: any] : ( ~ (aVector0(xq) = v0) | ~ % 21.16/3.57 | $i(xq) | (v0 = 0 & ! [v1: $i] : ! [v2: $i] : ( ~ % 21.16/3.57 | (sdtlbdtrb0(xt, v1) = v2) | ~ $i(v1) | ? [v3: any] : ? % 21.16/3.57 | [v4: $i] : (sdtlbdtrb0(xq, v1) = v4 & aNaturalNumber0(v1) = % 21.16/3.57 | v3 & $i(v4) & ( ~ (v3 = 0) | v4 = v2))) & ? [v1: $i] : % 21.16/3.57 | (aDimensionOf0(xq) = v1 & szszuzczcdt0(v1) = all_102_0 & % 21.16/3.57 | $i(v1))))) % 21.16/3.57 | % 21.16/3.57 | DELTA: instantiating (93) with fresh symbols all_104_0, all_104_1 gives: % 21.16/3.57 | (137) aVector0(xs) = all_104_1 & aDimensionOf0(xs) = all_104_0 & % 21.16/3.57 | $i(all_104_0) & ( ~ (all_104_1 = 0) | all_104_0 = sz00 | ( ! [v0: $i] % 21.16/3.57 | : (v0 = xp | ~ (aVector0(v0) = 0) | ~ $i(v0) | ? [v1: $i] : ? % 21.16/3.57 | [v2: $i] : ? [v3: $i] : ( ~ (v3 = v2) & sdtlbdtrb0(v0, v1) = % 21.16/3.57 | v2 & sdtlbdtrb0(xs, v1) = v3 & aNaturalNumber0(v1) = 0 & % 21.16/3.57 | $i(v3) & $i(v2) & $i(v1)) | ? [v1: $i] : ? [v2: any] : ( ~ % 21.16/3.57 | (v2 = all_104_0) & aDimensionOf0(v0) = v1 & szszuzczcdt0(v1) % 21.16/3.57 | = v2 & $i(v2) & $i(v1))) & ! [v0: any] : ( ~ (aVector0(xp) = % 21.16/3.57 | v0) | ~ $i(xp) | (v0 = 0 & ! [v1: $i] : ! [v2: $i] : ( ~ % 21.16/3.57 | (sdtlbdtrb0(xs, v1) = v2) | ~ $i(v1) | ? [v3: any] : ? % 21.16/3.57 | [v4: $i] : (sdtlbdtrb0(xp, v1) = v4 & aNaturalNumber0(v1) = % 21.16/3.57 | v3 & $i(v4) & ( ~ (v3 = 0) | v4 = v2))) & ? [v1: $i] : % 21.16/3.57 | (aDimensionOf0(xp) = v1 & szszuzczcdt0(v1) = all_104_0 & % 21.16/3.57 | $i(v1)))))) % 21.16/3.57 | % 21.16/3.57 | ALPHA: (137) implies: % 21.16/3.57 | (138) aDimensionOf0(xs) = all_104_0 % 21.16/3.57 | (139) aVector0(xs) = all_104_1 % 21.16/3.57 | % 21.16/3.57 | BETA: splitting (97) gives: % 21.16/3.57 | % 21.16/3.57 | Case 1: % 21.16/3.57 | | % 21.16/3.57 | | (140) all_41_0 = 0 % 21.16/3.57 | | % 21.16/3.57 | | REDUCE: (43), (140) imply: % 21.16/3.57 | | (141) $false % 21.16/3.58 | | % 21.16/3.58 | | CLOSE: (141) is inconsistent. % 21.16/3.58 | | % 21.16/3.58 | Case 2: % 21.16/3.58 | | % 21.16/3.58 | | (142) ? [v0: any] : ? [v1: any] : ? [v2: $i] : ? [v3: $i] : ? [v4: % 21.16/3.58 | | any] : (aVector0(xq) = v1 & aVector0(xp) = v0 & aDimensionOf0(xq) % 21.16/3.58 | | = v3 & aDimensionOf0(xp) = v2 & iLess0(v2, all_49_0) = v4 & % 21.16/3.58 | | $i(v3) & $i(v2) & ( ~ (v4 = 0) | ~ (v3 = v2) | ~ (v1 = 0) | ~ % 21.16/3.58 | | (v0 = 0))) % 21.16/3.58 | | % 21.16/3.58 | | DELTA: instantiating (142) with fresh symbols all_110_0, all_110_1, % 21.16/3.58 | | all_110_2, all_110_3, all_110_4 gives: % 21.16/3.58 | | (143) aVector0(xq) = all_110_3 & aVector0(xp) = all_110_4 & % 21.16/3.58 | | aDimensionOf0(xq) = all_110_1 & aDimensionOf0(xp) = all_110_2 & % 21.16/3.58 | | iLess0(all_110_2, all_49_0) = all_110_0 & $i(all_110_1) & % 21.16/3.58 | | $i(all_110_2) & ( ~ (all_110_0 = 0) | ~ (all_110_1 = all_110_2) | % 21.16/3.58 | | ~ (all_110_3 = 0) | ~ (all_110_4 = 0)) % 21.16/3.58 | | % 21.16/3.58 | | ALPHA: (143) implies: % 21.16/3.58 | | (144) iLess0(all_110_2, all_49_0) = all_110_0 % 21.16/3.58 | | (145) aDimensionOf0(xp) = all_110_2 % 21.16/3.58 | | (146) aDimensionOf0(xq) = all_110_1 % 21.16/3.58 | | (147) aVector0(xp) = all_110_4 % 21.16/3.58 | | (148) aVector0(xq) = all_110_3 % 21.16/3.58 | | (149) ~ (all_110_0 = 0) | ~ (all_110_1 = all_110_2) | ~ (all_110_3 = % 21.16/3.58 | | 0) | ~ (all_110_4 = 0) % 21.16/3.58 | | % 21.16/3.58 | | REDUCE: (67), (144) imply: % 21.16/3.58 | | (150) iLess0(all_110_2, all_33_0) = all_110_0 % 21.16/3.58 | | % 21.16/3.58 | | BETA: splitting (86) gives: % 21.16/3.58 | | % 21.16/3.58 | | Case 1: % 21.16/3.58 | | | % 21.16/3.58 | | | (151) all_41_0 = 0 % 21.16/3.58 | | | % 21.16/3.58 | | | REDUCE: (43), (151) imply: % 21.16/3.58 | | | (152) $false % 21.16/3.58 | | | % 21.16/3.58 | | | CLOSE: (152) is inconsistent. % 21.16/3.58 | | | % 21.16/3.58 | | Case 2: % 21.16/3.58 | | | % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (27) with all_98_2, all_100_3, xs, simplifying % 21.16/3.58 | | | with (119), (126) gives: % 21.16/3.58 | | | (153) all_100_3 = all_98_2 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (27) with all_70_0, all_100_3, xs, simplifying % 21.16/3.58 | | | with (107), (126) gives: % 21.16/3.58 | | | (154) all_100_3 = all_70_0 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (27) with all_33_0, all_104_0, xs, simplifying % 21.16/3.58 | | | with (30), (138) gives: % 21.16/3.58 | | | (155) all_104_0 = all_33_0 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (27) with all_98_2, all_104_0, xs, simplifying % 21.16/3.58 | | | with (119), (138) gives: % 21.16/3.58 | | | (156) all_104_0 = all_98_2 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (27) with all_33_0, all_98_3, xt, simplifying % 21.16/3.58 | | | with (31), (120) gives: % 21.16/3.58 | | | (157) all_98_3 = all_33_0 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (27) with all_98_3, all_100_2, xt, simplifying % 21.16/3.58 | | | with (120), (127) gives: % 21.16/3.58 | | | (158) all_100_2 = all_98_3 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (27) with all_100_2, all_102_0, xt, simplifying % 21.16/3.58 | | | with (127), (134) gives: % 21.16/3.58 | | | (159) all_102_0 = all_100_2 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (27) with all_68_0, all_102_0, xt, simplifying % 21.16/3.58 | | | with (105), (134) gives: % 21.16/3.58 | | | (160) all_102_0 = all_68_0 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (27) with all_66_0, all_100_1, xp, simplifying % 21.16/3.58 | | | with (103), (128) gives: % 21.16/3.58 | | | (161) all_100_1 = all_66_0 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (27) with all_46_1, all_110_2, xp, simplifying % 21.16/3.58 | | | with (58), (145) gives: % 21.16/3.58 | | | (162) all_110_2 = all_46_1 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (27) with all_100_1, all_110_2, xp, simplifying % 21.16/3.58 | | | with (128), (145) gives: % 21.16/3.58 | | | (163) all_110_2 = all_100_1 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (27) with all_98_0, all_110_2, xp, simplifying % 21.16/3.58 | | | with (121), (145) gives: % 21.16/3.58 | | | (164) all_110_2 = all_98_0 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (27) with all_64_0, all_100_0, xq, simplifying % 21.16/3.58 | | | with (100), (129) gives: % 21.16/3.58 | | | (165) all_100_0 = all_64_0 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (27) with all_43_1, all_110_1, xq, simplifying % 21.16/3.58 | | | with (51), (146) gives: % 21.16/3.58 | | | (166) all_110_1 = all_43_1 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (27) with all_100_0, all_110_1, xq, simplifying % 21.16/3.58 | | | with (129), (146) gives: % 21.16/3.58 | | | (167) all_110_1 = all_100_0 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (27) with all_98_1, all_110_1, xq, simplifying % 21.16/3.58 | | | with (122), (146) gives: % 21.16/3.58 | | | (168) all_110_1 = all_98_1 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (28) with 0, all_104_1, xs, simplifying with % 21.16/3.58 | | | (6), (139) gives: % 21.16/3.58 | | | (169) all_104_1 = 0 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (28) with all_100_5, all_104_1, xs, simplifying % 21.16/3.58 | | | with (130), (139) gives: % 21.16/3.58 | | | (170) all_104_1 = all_100_5 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (28) with all_98_4, all_104_1, xs, simplifying % 21.16/3.58 | | | with (123), (139) gives: % 21.16/3.58 | | | (171) all_104_1 = all_98_4 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (28) with all_90_2, all_104_1, xs, simplifying % 21.16/3.58 | | | with (115), (139) gives: % 21.16/3.58 | | | (172) all_104_1 = all_90_2 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (28) with 0, all_100_4, xt, simplifying with % 21.16/3.58 | | | (7), (131) gives: % 21.16/3.58 | | | (173) all_100_4 = 0 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (28) with all_98_5, all_100_4, xt, simplifying % 21.16/3.58 | | | with (124), (131) gives: % 21.16/3.58 | | | (174) all_100_4 = all_98_5 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (28) with all_100_4, all_102_1, xt, simplifying % 21.16/3.58 | | | with (131), (135) gives: % 21.16/3.58 | | | (175) all_102_1 = all_100_4 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (28) with all_94_2, all_102_1, xt, simplifying % 21.16/3.58 | | | with (117), (135) gives: % 21.16/3.58 | | | (176) all_102_1 = all_94_2 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (28) with 0, all_110_4, xp, simplifying with % 21.16/3.58 | | | (59), (147) gives: % 21.16/3.58 | | | (177) all_110_4 = 0 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (28) with 0, all_110_3, xq, simplifying with % 21.16/3.58 | | | (52), (148) gives: % 21.16/3.58 | | | (178) all_110_3 = 0 % 21.16/3.58 | | | % 21.16/3.58 | | | GROUND_INST: instantiating (28) with all_74_1, all_110_3, xq, simplifying % 21.16/3.58 | | | with (109), (148) gives: % 21.16/3.58 | | | (179) all_110_3 = all_74_1 % 21.16/3.58 | | | % 21.16/3.58 | | | COMBINE_EQS: (167), (168) imply: % 21.16/3.58 | | | (180) all_100_0 = all_98_1 % 21.16/3.58 | | | % 21.16/3.58 | | | SIMP: (180) implies: % 21.16/3.58 | | | (181) all_100_0 = all_98_1 % 21.16/3.58 | | | % 21.16/3.58 | | | COMBINE_EQS: (166), (168) imply: % 21.16/3.58 | | | (182) all_98_1 = all_43_1 % 21.16/3.58 | | | % 21.16/3.58 | | | COMBINE_EQS: (163), (164) imply: % 21.16/3.58 | | | (183) all_100_1 = all_98_0 % 21.16/3.58 | | | % 21.16/3.58 | | | SIMP: (183) implies: % 21.16/3.58 | | | (184) all_100_1 = all_98_0 % 21.16/3.58 | | | % 21.16/3.58 | | | COMBINE_EQS: (162), (164) imply: % 21.16/3.58 | | | (185) all_98_0 = all_46_1 % 21.16/3.58 | | | % 21.16/3.58 | | | COMBINE_EQS: (178), (179) imply: % 21.16/3.58 | | | (186) all_74_1 = 0 % 21.16/3.58 | | | % 21.16/3.58 | | | COMBINE_EQS: (155), (156) imply: % 21.16/3.58 | | | (187) all_98_2 = all_33_0 % 21.16/3.58 | | | % 21.16/3.58 | | | SIMP: (187) implies: % 21.16/3.58 | | | (188) all_98_2 = all_33_0 % 21.16/3.58 | | | % 21.16/3.58 | | | COMBINE_EQS: (169), (170) imply: % 21.16/3.58 | | | (189) all_100_5 = 0 % 21.16/3.58 | | | % 21.16/3.58 | | | COMBINE_EQS: (170), (172) imply: % 21.16/3.58 | | | (190) all_100_5 = all_90_2 % 21.16/3.58 | | | % 21.16/3.58 | | | COMBINE_EQS: (170), (171) imply: % 21.16/3.59 | | | (191) all_100_5 = all_98_4 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (159), (160) imply: % 21.16/3.59 | | | (192) all_100_2 = all_68_0 % 21.16/3.59 | | | % 21.16/3.59 | | | SIMP: (192) implies: % 21.16/3.59 | | | (193) all_100_2 = all_68_0 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (175), (176) imply: % 21.16/3.59 | | | (194) all_100_4 = all_94_2 % 21.16/3.59 | | | % 21.16/3.59 | | | SIMP: (194) implies: % 21.16/3.59 | | | (195) all_100_4 = all_94_2 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (165), (181) imply: % 21.16/3.59 | | | (196) all_98_1 = all_64_0 % 21.16/3.59 | | | % 21.16/3.59 | | | SIMP: (196) implies: % 21.16/3.59 | | | (197) all_98_1 = all_64_0 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (161), (184) imply: % 21.16/3.59 | | | (198) all_98_0 = all_66_0 % 21.16/3.59 | | | % 21.16/3.59 | | | SIMP: (198) implies: % 21.16/3.59 | | | (199) all_98_0 = all_66_0 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (158), (193) imply: % 21.16/3.59 | | | (200) all_98_3 = all_68_0 % 21.16/3.59 | | | % 21.16/3.59 | | | SIMP: (200) implies: % 21.16/3.59 | | | (201) all_98_3 = all_68_0 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (153), (154) imply: % 21.16/3.59 | | | (202) all_98_2 = all_70_0 % 21.16/3.59 | | | % 21.16/3.59 | | | SIMP: (202) implies: % 21.16/3.59 | | | (203) all_98_2 = all_70_0 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (173), (174) imply: % 21.16/3.59 | | | (204) all_98_5 = 0 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (174), (195) imply: % 21.16/3.59 | | | (205) all_98_5 = all_94_2 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (190), (191) imply: % 21.16/3.59 | | | (206) all_98_4 = all_90_2 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (189), (191) imply: % 21.16/3.59 | | | (207) all_98_4 = 0 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (185), (199) imply: % 21.16/3.59 | | | (208) all_66_0 = all_46_1 % 21.16/3.59 | | | % 21.16/3.59 | | | SIMP: (208) implies: % 21.16/3.59 | | | (209) all_66_0 = all_46_1 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (182), (197) imply: % 21.16/3.59 | | | (210) all_64_0 = all_43_1 % 21.16/3.59 | | | % 21.16/3.59 | | | SIMP: (210) implies: % 21.16/3.59 | | | (211) all_64_0 = all_43_1 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (188), (203) imply: % 21.16/3.59 | | | (212) all_70_0 = all_33_0 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (157), (201) imply: % 21.16/3.59 | | | (213) all_68_0 = all_33_0 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (206), (207) imply: % 21.16/3.59 | | | (214) all_90_2 = 0 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (204), (205) imply: % 21.16/3.59 | | | (215) all_94_2 = 0 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (154), (212) imply: % 21.16/3.59 | | | (216) all_100_3 = all_33_0 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (193), (213) imply: % 21.16/3.59 | | | (217) all_100_2 = all_33_0 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (161), (209) imply: % 21.16/3.59 | | | (218) all_100_1 = all_46_1 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (165), (211) imply: % 21.16/3.59 | | | (219) all_100_0 = all_43_1 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (176), (215) imply: % 21.16/3.59 | | | (220) all_102_1 = 0 % 21.16/3.59 | | | % 21.16/3.59 | | | COMBINE_EQS: (160), (213) imply: % 21.16/3.59 | | | (221) all_102_0 = all_33_0 % 21.27/3.59 | | | % 21.27/3.59 | | | REDUCE: (150), (162) imply: % 21.27/3.59 | | | (222) iLess0(all_46_1, all_33_0) = all_110_0 % 21.27/3.59 | | | % 21.27/3.59 | | | REDUCE: (102), (209) imply: % 21.27/3.59 | | | (223) aNaturalNumber0(all_46_1) = 0 % 21.27/3.59 | | | % 21.27/3.59 | | | BETA: splitting (132) gives: % 21.27/3.59 | | | % 21.27/3.59 | | | Case 1: % 21.27/3.59 | | | | % 21.27/3.59 | | | | (224) ~ (all_100_4 = 0) % 21.27/3.59 | | | | % 21.27/3.59 | | | | REDUCE: (173), (224) imply: % 21.27/3.59 | | | | (225) $false % 21.27/3.59 | | | | % 21.27/3.59 | | | | CLOSE: (225) is inconsistent. % 21.27/3.59 | | | | % 21.27/3.59 | | | Case 2: % 21.27/3.59 | | | | % 21.27/3.59 | | | | (226) ~ (all_100_2 = all_100_3) | ~ (all_100_5 = 0) | all_100_0 = % 21.27/3.59 | | | | all_100_1 | all_100_3 = sz00 % 21.27/3.59 | | | | % 21.27/3.59 | | | | BETA: splitting (136) gives: % 21.27/3.59 | | | | % 21.27/3.59 | | | | Case 1: % 21.27/3.59 | | | | | % 21.27/3.59 | | | | | (227) ~ (all_102_1 = 0) % 21.27/3.59 | | | | | % 21.27/3.59 | | | | | REDUCE: (220), (227) imply: % 21.27/3.59 | | | | | (228) $false % 21.27/3.59 | | | | | % 21.27/3.59 | | | | | CLOSE: (228) is inconsistent. % 21.27/3.59 | | | | | % 21.27/3.59 | | | | Case 2: % 21.27/3.59 | | | | | % 21.27/3.59 | | | | | (229) all_102_0 = sz00 | ( ! [v0: $i] : (v0 = xq | ~ (aVector0(v0) % 21.27/3.59 | | | | | = 0) | ~ $i(v0) | ? [v1: $i] : ? [v2: $i] : ? [v3: % 21.27/3.59 | | | | | $i] : ( ~ (v3 = v2) & sdtlbdtrb0(v0, v1) = v2 & % 21.27/3.59 | | | | | sdtlbdtrb0(xt, v1) = v3 & aNaturalNumber0(v1) = 0 & % 21.27/3.59 | | | | | $i(v3) & $i(v2) & $i(v1)) | ? [v1: $i] : ? [v2: any] % 21.27/3.59 | | | | | : ( ~ (v2 = all_102_0) & aDimensionOf0(v0) = v1 & % 21.27/3.59 | | | | | szszuzczcdt0(v1) = v2 & $i(v2) & $i(v1))) & ! [v0: % 21.27/3.59 | | | | | any] : ( ~ (aVector0(xq) = v0) | ~ $i(xq) | (v0 = 0 & ! % 21.27/3.59 | | | | | [v1: $i] : ! [v2: $i] : ( ~ (sdtlbdtrb0(xt, v1) = v2) % 21.27/3.59 | | | | | | ~ $i(v1) | ? [v3: any] : ? [v4: $i] : % 21.27/3.59 | | | | | (sdtlbdtrb0(xq, v1) = v4 & aNaturalNumber0(v1) = v3 & % 21.27/3.59 | | | | | $i(v4) & ( ~ (v3 = 0) | v4 = v2))) & ? [v1: $i] : % 21.27/3.59 | | | | | (aDimensionOf0(xq) = v1 & szszuzczcdt0(v1) = all_102_0 % 21.27/3.59 | | | | | & $i(v1))))) % 21.27/3.59 | | | | | % 21.27/3.59 | | | | | BETA: splitting (229) gives: % 21.27/3.59 | | | | | % 21.27/3.59 | | | | | Case 1: % 21.27/3.59 | | | | | | % 21.27/3.59 | | | | | | (230) all_102_0 = sz00 % 21.27/3.59 | | | | | | % 21.27/3.59 | | | | | | COMBINE_EQS: (221), (230) imply: % 21.27/3.59 | | | | | | (231) all_33_0 = sz00 % 21.27/3.59 | | | | | | % 21.27/3.59 | | | | | | REDUCE: (78), (231) imply: % 21.27/3.59 | | | | | | (232) $false % 21.27/3.59 | | | | | | % 21.27/3.59 | | | | | | CLOSE: (232) is inconsistent. % 21.27/3.59 | | | | | | % 21.27/3.59 | | | | | Case 2: % 21.27/3.59 | | | | | | % 21.27/3.59 | | | | | | (233) ~ (all_102_0 = sz00) % 21.27/3.59 | | | | | | (234) ! [v0: $i] : (v0 = xq | ~ (aVector0(v0) = 0) | ~ $i(v0) % 21.27/3.59 | | | | | | | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( ~ (v3 = v2) % 21.27/3.59 | | | | | | & sdtlbdtrb0(v0, v1) = v2 & sdtlbdtrb0(xt, v1) = v3 & % 21.27/3.59 | | | | | | aNaturalNumber0(v1) = 0 & $i(v3) & $i(v2) & $i(v1)) | % 21.27/3.59 | | | | | | ? [v1: $i] : ? [v2: any] : ( ~ (v2 = all_102_0) & % 21.27/3.59 | | | | | | aDimensionOf0(v0) = v1 & szszuzczcdt0(v1) = v2 & $i(v2) % 21.27/3.59 | | | | | | & $i(v1))) & ! [v0: any] : ( ~ (aVector0(xq) = v0) | % 21.27/3.59 | | | | | | ~ $i(xq) | (v0 = 0 & ! [v1: $i] : ! [v2: $i] : ( ~ % 21.27/3.59 | | | | | | (sdtlbdtrb0(xt, v1) = v2) | ~ $i(v1) | ? [v3: any] % 21.27/3.59 | | | | | | : ? [v4: $i] : (sdtlbdtrb0(xq, v1) = v4 & % 21.27/3.59 | | | | | | aNaturalNumber0(v1) = v3 & $i(v4) & ( ~ (v3 = 0) | % 21.27/3.59 | | | | | | v4 = v2))) & ? [v1: $i] : (aDimensionOf0(xq) = % 21.27/3.59 | | | | | | v1 & szszuzczcdt0(v1) = all_102_0 & $i(v1)))) % 21.27/3.59 | | | | | | % 21.27/3.59 | | | | | | ALPHA: (234) implies: % 21.27/3.59 | | | | | | (235) ! [v0: any] : ( ~ (aVector0(xq) = v0) | ~ $i(xq) | (v0 = % 21.27/3.59 | | | | | | 0 & ! [v1: $i] : ! [v2: $i] : ( ~ (sdtlbdtrb0(xt, v1) % 21.27/3.59 | | | | | | = v2) | ~ $i(v1) | ? [v3: any] : ? [v4: $i] : % 21.27/3.59 | | | | | | (sdtlbdtrb0(xq, v1) = v4 & aNaturalNumber0(v1) = v3 & % 21.27/3.59 | | | | | | $i(v4) & ( ~ (v3 = 0) | v4 = v2))) & ? [v1: $i] : % 21.27/3.59 | | | | | | (aDimensionOf0(xq) = v1 & szszuzczcdt0(v1) = all_102_0 % 21.27/3.59 | | | | | | & $i(v1)))) % 21.27/3.59 | | | | | | % 21.27/3.59 | | | | | | GROUND_INST: instantiating (235) with 0, simplifying with (20), (52) % 21.27/3.59 | | | | | | gives: % 21.27/3.59 | | | | | | (236) ! [v0: $i] : ! [v1: $i] : ( ~ (sdtlbdtrb0(xt, v0) = v1) | % 21.27/3.59 | | | | | | ~ $i(v0) | ? [v2: any] : ? [v3: $i] : (sdtlbdtrb0(xq, % 21.27/3.59 | | | | | | v0) = v3 & aNaturalNumber0(v0) = v2 & $i(v3) & ( ~ % 21.27/3.59 | | | | | | (v2 = 0) | v3 = v1))) & ? [v0: $i] : % 21.27/3.59 | | | | | | (aDimensionOf0(xq) = v0 & szszuzczcdt0(v0) = all_102_0 & % 21.27/3.59 | | | | | | $i(v0)) % 21.27/3.59 | | | | | | % 21.27/3.59 | | | | | | ALPHA: (236) implies: % 21.27/3.59 | | | | | | (237) ? [v0: $i] : (aDimensionOf0(xq) = v0 & szszuzczcdt0(v0) = % 21.27/3.59 | | | | | | all_102_0 & $i(v0)) % 21.27/3.59 | | | | | | % 21.27/3.59 | | | | | | DELTA: instantiating (237) with fresh symbol all_158_0 gives: % 21.27/3.59 | | | | | | (238) aDimensionOf0(xq) = all_158_0 & szszuzczcdt0(all_158_0) = % 21.27/3.59 | | | | | | all_102_0 & $i(all_158_0) % 21.27/3.59 | | | | | | % 21.27/3.59 | | | | | | ALPHA: (238) implies: % 21.27/3.59 | | | | | | (239) $i(all_158_0) % 21.27/3.59 | | | | | | (240) szszuzczcdt0(all_158_0) = all_102_0 % 21.27/3.59 | | | | | | (241) aDimensionOf0(xq) = all_158_0 % 21.27/3.59 | | | | | | % 21.27/3.59 | | | | | | REDUCE: (221), (240) imply: % 21.27/3.59 | | | | | | (242) szszuzczcdt0(all_158_0) = all_33_0 % 21.27/3.59 | | | | | | % 21.27/3.59 | | | | | | BETA: splitting (226) gives: % 21.27/3.59 | | | | | | % 21.27/3.59 | | | | | | Case 1: % 21.27/3.59 | | | | | | | % 21.27/3.59 | | | | | | | (243) ~ (all_100_5 = 0) % 21.27/3.59 | | | | | | | % 21.27/3.59 | | | | | | | REDUCE: (189), (243) imply: % 21.27/3.59 | | | | | | | (244) $false % 21.27/3.59 | | | | | | | % 21.27/3.59 | | | | | | | CLOSE: (244) is inconsistent. % 21.27/3.59 | | | | | | | % 21.27/3.59 | | | | | | Case 2: % 21.27/3.59 | | | | | | | % 21.27/3.59 | | | | | | | (245) ~ (all_100_2 = all_100_3) | all_100_0 = all_100_1 | % 21.27/3.59 | | | | | | | all_100_3 = sz00 % 21.27/3.59 | | | | | | | % 21.27/3.59 | | | | | | | BETA: splitting (245) gives: % 21.27/3.59 | | | | | | | % 21.27/3.59 | | | | | | | Case 1: % 21.27/3.59 | | | | | | | | % 21.27/3.59 | | | | | | | | (246) ~ (all_100_2 = all_100_3) % 21.27/3.59 | | | | | | | | % 21.27/3.59 | | | | | | | | REDUCE: (216), (217), (246) imply: % 21.27/3.59 | | | | | | | | (247) $false % 21.27/3.59 | | | | | | | | % 21.27/3.59 | | | | | | | | CLOSE: (247) is inconsistent. % 21.27/3.59 | | | | | | | | % 21.27/3.59 | | | | | | | Case 2: % 21.27/3.59 | | | | | | | | % 21.27/3.59 | | | | | | | | (248) all_100_2 = all_100_3 % 21.27/3.59 | | | | | | | | (249) all_100_0 = all_100_1 | all_100_3 = sz00 % 21.27/3.60 | | | | | | | | % 21.27/3.60 | | | | | | | | COMBINE_EQS: (217), (248) imply: % 21.27/3.60 | | | | | | | | (250) all_100_3 = all_33_0 % 21.27/3.60 | | | | | | | | % 21.27/3.60 | | | | | | | | BETA: splitting (249) gives: % 21.27/3.60 | | | | | | | | % 21.27/3.60 | | | | | | | | Case 1: % 21.27/3.60 | | | | | | | | | % 21.27/3.60 | | | | | | | | | (251) all_100_3 = sz00 % 21.27/3.60 | | | | | | | | | % 21.27/3.60 | | | | | | | | | COMBINE_EQS: (216), (251) imply: % 21.27/3.60 | | | | | | | | | (252) all_33_0 = sz00 % 21.27/3.60 | | | | | | | | | % 21.27/3.60 | | | | | | | | | REDUCE: (78), (252) imply: % 21.27/3.60 | | | | | | | | | (253) $false % 21.27/3.60 | | | | | | | | | % 21.27/3.60 | | | | | | | | | CLOSE: (253) is inconsistent. % 21.27/3.60 | | | | | | | | | % 21.27/3.60 | | | | | | | | Case 2: % 21.27/3.60 | | | | | | | | | % 21.27/3.60 | | | | | | | | | (254) all_100_0 = all_100_1 % 21.27/3.60 | | | | | | | | | % 21.27/3.60 | | | | | | | | | COMBINE_EQS: (219), (254) imply: % 21.27/3.60 | | | | | | | | | (255) all_100_1 = all_43_1 % 21.27/3.60 | | | | | | | | | % 21.27/3.60 | | | | | | | | | SIMP: (255) implies: % 21.27/3.60 | | | | | | | | | (256) all_100_1 = all_43_1 % 21.27/3.60 | | | | | | | | | % 21.27/3.60 | | | | | | | | | COMBINE_EQS: (218), (256) imply: % 21.27/3.60 | | | | | | | | | (257) all_46_1 = all_43_1 % 21.27/3.60 | | | | | | | | | % 21.27/3.60 | | | | | | | | | COMBINE_EQS: (162), (257) imply: % 21.27/3.60 | | | | | | | | | (258) all_110_2 = all_43_1 % 21.27/3.60 | | | | | | | | | % 21.27/3.60 | | | | | | | | | REDUCE: (222), (257) imply: % 21.27/3.60 | | | | | | | | | (259) iLess0(all_43_1, all_33_0) = all_110_0 % 21.27/3.60 | | | | | | | | | % 21.27/3.60 | | | | | | | | | REDUCE: (111), (257) imply: % 21.27/3.60 | | | | | | | | | (260) aNaturalNumber0(all_43_1) = all_86_1 % 21.27/3.60 | | | | | | | | | % 21.27/3.60 | | | | | | | | | REDUCE: (223), (257) imply: % 21.27/3.60 | | | | | | | | | (261) aNaturalNumber0(all_43_1) = 0 % 21.27/3.60 | | | | | | | | | % 21.27/3.60 | | | | | | | | | BETA: splitting (149) gives: % 21.27/3.60 | | | | | | | | | % 21.27/3.60 | | | | | | | | | Case 1: % 21.27/3.60 | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | (262) ~ (all_110_0 = 0) % 21.27/3.60 | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | GROUND_INST: instantiating (26) with all_88_1, 0, all_43_1, % 21.27/3.60 | | | | | | | | | | simplifying with (113), (261) gives: % 21.27/3.60 | | | | | | | | | | (263) all_88_1 = 0 % 21.27/3.60 | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | GROUND_INST: instantiating (26) with all_88_1, all_86_1, % 21.27/3.60 | | | | | | | | | | all_43_1, simplifying with (113), (260) gives: % 21.27/3.60 | | | | | | | | | | (264) all_88_1 = all_86_1 % 21.27/3.60 | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | GROUND_INST: instantiating (27) with all_43_1, all_158_0, xq, % 21.27/3.60 | | | | | | | | | | simplifying with (51), (241) gives: % 21.27/3.60 | | | | | | | | | | (265) all_158_0 = all_43_1 % 21.27/3.60 | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | COMBINE_EQS: (263), (264) imply: % 21.27/3.60 | | | | | | | | | | (266) all_86_1 = 0 % 21.27/3.60 | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | SIMP: (266) implies: % 21.27/3.60 | | | | | | | | | | (267) all_86_1 = 0 % 21.27/3.60 | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | GROUND_INST: instantiating (mIH) with all_43_1, all_33_0, % 21.27/3.60 | | | | | | | | | | all_110_0, simplifying with (48), (82), (259) % 21.27/3.60 | | | | | | | | | | gives: % 21.27/3.60 | | | | | | | | | | (268) all_110_0 = 0 | ? [v0: int] : ( ~ (v0 = 0) & % 21.27/3.60 | | | | | | | | | | aNaturalNumber0(all_43_1) = v0) % 21.27/3.60 | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | BETA: splitting (268) gives: % 21.27/3.60 | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | Case 1: % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | (269) all_110_0 = 0 % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | REDUCE: (262), (269) imply: % 21.27/3.60 | | | | | | | | | | | (270) $false % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | CLOSE: (270) is inconsistent. % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | Case 2: % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | (271) ? [v0: int] : ( ~ (v0 = 0) & % 21.27/3.60 | | | | | | | | | | | aNaturalNumber0(all_43_1) = v0) % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | DELTA: instantiating (271) with fresh symbol all_299_0 % 21.27/3.60 | | | | | | | | | | | gives: % 21.27/3.60 | | | | | | | | | | | (272) ~ (all_299_0 = 0) & aNaturalNumber0(all_43_1) = % 21.27/3.60 | | | | | | | | | | | all_299_0 % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | ALPHA: (272) implies: % 21.27/3.60 | | | | | | | | | | | (273) ~ (all_299_0 = 0) % 21.27/3.60 | | | | | | | | | | | (274) aNaturalNumber0(all_43_1) = all_299_0 % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | GROUND_INST: instantiating (26) with 0, all_299_0, all_43_1, % 21.27/3.60 | | | | | | | | | | | simplifying with (261), (274) gives: % 21.27/3.60 | | | | | | | | | | | (275) all_299_0 = 0 % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | REDUCE: (273), (275) imply: % 21.27/3.60 | | | | | | | | | | | (276) $false % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | CLOSE: (276) is inconsistent. % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | End of split % 21.27/3.60 | | | | | | | | | | % 21.27/3.60 | | | | | | | | | Case 2: % 21.27/3.60 | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | (277) ~ (all_110_1 = all_110_2) | ~ (all_110_3 = 0) | % 21.27/3.60 | | | | | | | | | | ~ (all_110_4 = 0) % 21.27/3.60 | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | BETA: splitting (277) gives: % 21.27/3.60 | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | Case 1: % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | (278) ~ (all_110_3 = 0) % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | REDUCE: (178), (278) imply: % 21.27/3.60 | | | | | | | | | | | (279) $false % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | CLOSE: (279) is inconsistent. % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | Case 2: % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | (280) ~ (all_110_1 = all_110_2) | ~ (all_110_4 = 0) % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | BETA: splitting (280) gives: % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | Case 1: % 21.27/3.60 | | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | | (281) ~ (all_110_4 = 0) % 21.27/3.60 | | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | | REDUCE: (177), (281) imply: % 21.27/3.60 | | | | | | | | | | | | (282) $false % 21.27/3.60 | | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | | CLOSE: (282) is inconsistent. % 21.27/3.60 | | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | Case 2: % 21.27/3.60 | | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | | (283) ~ (all_110_1 = all_110_2) % 21.27/3.60 | | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | | REDUCE: (166), (258), (283) imply: % 21.27/3.60 | | | | | | | | | | | | (284) $false % 21.27/3.60 | | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | | CLOSE: (284) is inconsistent. % 21.27/3.60 | | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | | End of split % 21.27/3.60 | | | | | | | | | | | % 21.27/3.60 | | | | | | | | | | End of split % 21.27/3.60 | | | | | | | | | | % 21.27/3.60 | | | | | | | | | End of split % 21.27/3.60 | | | | | | | | | % 21.27/3.60 | | | | | | | | End of split % 21.27/3.60 | | | | | | | | % 21.27/3.60 | | | | | | | End of split % 21.27/3.60 | | | | | | | % 21.27/3.60 | | | | | | End of split % 21.27/3.60 | | | | | | % 21.27/3.60 | | | | | End of split % 21.27/3.60 | | | | | % 21.27/3.60 | | | | End of split % 21.27/3.60 | | | | % 21.27/3.60 | | | End of split % 21.27/3.60 | | | % 21.27/3.60 | | End of split % 21.27/3.60 | | % 21.27/3.60 | End of split % 21.27/3.60 | % 21.27/3.60 End of proof % 21.27/3.60 % SZS output end Proof for theBenchmark % 21.27/3.60 % 21.27/3.60 3023ms %------------------------------------------------------------------------------