%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : RNG049+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 : n010.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:33 EDT 2023 % Result : Theorem 17.85s 3.23s % Output : Proof 32.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : RNG049+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.12/0.34 % Computer : n010.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Sun Aug 27 01:49:20 EDT 2023 % 0.12/0.34 % CPUTime : % 0.19/0.61 ________ _____ % 0.19/0.61 ___ __ \_________(_)________________________________ % 0.19/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.61 % 0.19/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.61 (2023-06-19) % 0.19/0.61 % 0.19/0.61 (c) Philipp Rümmer, 2009-2023 % 0.19/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.61 Amanda Stjerna. % 0.19/0.61 Free software under BSD-3-Clause. % 0.19/0.61 % 0.19/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.61 % 0.19/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.62 Running up to 7 provers in parallel. % 0.19/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.19/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 3.23/1.19 Prover 4: Preprocessing ... % 3.23/1.19 Prover 1: Preprocessing ... % 3.23/1.22 Prover 0: Preprocessing ... % 3.23/1.22 Prover 6: Preprocessing ... % 3.23/1.22 Prover 2: Preprocessing ... % 3.23/1.22 Prover 3: Preprocessing ... % 3.23/1.22 Prover 5: Preprocessing ... % 8.14/1.93 Prover 1: Constructing countermodel ... % 8.14/1.93 Prover 3: Constructing countermodel ... % 9.29/2.01 Prover 6: Proving ... % 9.71/2.11 Prover 5: Constructing countermodel ... % 10.77/2.22 Prover 4: Constructing countermodel ... % 11.11/2.34 Prover 2: Proving ... % 11.11/2.38 Prover 0: Proving ... % 17.85/3.22 Prover 0: proved (2594ms) % 17.85/3.23 % 17.85/3.23 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.85/3.23 % 17.85/3.24 Prover 6: stopped % 17.85/3.24 Prover 3: stopped % 17.85/3.24 Prover 5: stopped % 17.85/3.24 Prover 2: stopped % 17.85/3.24 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 17.85/3.24 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 17.85/3.24 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 17.85/3.25 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 18.50/3.26 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 19.60/3.41 Prover 10: Preprocessing ... % 19.60/3.41 Prover 7: Preprocessing ... % 19.60/3.42 Prover 8: Preprocessing ... % 19.60/3.42 Prover 13: Preprocessing ... % 19.60/3.45 Prover 11: Preprocessing ... % 20.72/3.56 Prover 10: Constructing countermodel ... % 21.03/3.61 Prover 8: Warning: ignoring some quantifiers % 21.03/3.61 Prover 8: Constructing countermodel ... % 21.37/3.64 Prover 7: Constructing countermodel ... % 21.37/3.66 Prover 13: Constructing countermodel ... % 23.31/3.92 Prover 11: Constructing countermodel ... % 23.64/4.02 Prover 10: gave up % 23.64/4.02 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 24.35/4.09 Prover 16: Preprocessing ... % 25.23/4.15 Prover 16: Constructing countermodel ... % 31.24/5.03 Prover 7: Found proof (size 195) % 31.24/5.03 Prover 7: proved (1795ms) % 31.24/5.03 Prover 13: stopped % 31.24/5.03 Prover 16: stopped % 31.24/5.03 Prover 11: stopped % 31.24/5.04 Prover 8: stopped % 31.24/5.04 Prover 4: stopped % 31.24/5.04 Prover 1: stopped % 31.24/5.04 % 31.24/5.04 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 31.24/5.04 % 31.24/5.05 % SZS output start Proof for theBenchmark % 31.24/5.06 Assumptions after simplification: % 31.24/5.06 --------------------------------- % 31.24/5.06 % 31.24/5.06 (mDefInit) % 31.24/5.09 $i(sz00) & ! [v0: $i] : ! [v1: $i] : (v1 = sz00 | ~ (aDimensionOf0(v0) = % 31.24/5.09 v1) | ~ $i(v0) | ~ aVector0(v0) | ? [v2: $i] : (sziznziztdt0(v0) = v2 & % 31.24/5.09 $i(v2) & ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ (sdtlbdtrb0(v2, v4) % 31.24/5.09 = v5) | ~ (aDimensionOf0(v2) = v3) | ~ $i(v4) | ~ % 31.24/5.09 aNaturalNumber0(v4) | (sdtlbdtrb0(v0, v4) = v5 & $i(v5))) & ! [v3: $i] % 31.24/5.09 : ! [v4: $i] : ! [v5: $i] : ( ~ (sdtlbdtrb0(v0, v4) = v5) | ~ % 31.24/5.09 (aDimensionOf0(v2) = v3) | ~ $i(v4) | ~ aNaturalNumber0(v4) | % 31.24/5.09 (sdtlbdtrb0(v2, v4) = v5 & $i(v5))) & ! [v3: $i] : ! [v4: $i] : (v3 = % 31.24/5.09 v2 | ~ (aDimensionOf0(v3) = v4) | ~ $i(v3) | ~ aVector0(v3) | ? [v5: % 31.24/5.09 $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ($i(v6) & (( ~ (v8 = % 31.24/5.09 v7) & sdtlbdtrb0(v3, v6) = v7 & sdtlbdtrb0(v0, v6) = v8 & $i(v8) % 31.24/5.09 & $i(v7) & aNaturalNumber0(v6)) | ( ~ (v5 = v1) & szszuzczcdt0(v4) % 31.24/5.09 = v5 & $i(v5))))) & ! [v3: $i] : ( ~ (aDimensionOf0(v2) = v3) | % 31.24/5.09 aVector0(v2)) & ! [v3: $i] : ( ~ (aDimensionOf0(v2) = v3) | % 31.24/5.09 (szszuzczcdt0(v3) = v1 & $i(v1))))) & ! [v0: $i] : ! [v1: $i] : ( ~ % 31.24/5.09 (sziznziztdt0(v0) = v1) | ~ $i(v0) | ~ aVector0(v0) | ? [v2: $i] : % 31.24/5.09 (aDimensionOf0(v0) = v2 & $i(v2) & (v2 = sz00 | ( ! [v3: $i] : ! [v4: $i] : % 31.24/5.09 ! [v5: $i] : ( ~ (sdtlbdtrb0(v1, v4) = v5) | ~ (aDimensionOf0(v1) = % 31.24/5.09 v3) | ~ $i(v4) | ~ $i(v1) | ~ aNaturalNumber0(v4) | % 31.24/5.09 (sdtlbdtrb0(v0, v4) = v5 & $i(v5))) & ! [v3: $i] : ! [v4: $i] : ! % 31.24/5.09 [v5: $i] : ( ~ (sdtlbdtrb0(v0, v4) = v5) | ~ (aDimensionOf0(v1) = v3) % 31.24/5.09 | ~ $i(v4) | ~ $i(v1) | ~ aNaturalNumber0(v4) | (sdtlbdtrb0(v1, % 31.24/5.09 v4) = v5 & $i(v5))) & ! [v3: $i] : ! [v4: $i] : (v3 = v1 | ~ % 31.24/5.09 (aDimensionOf0(v3) = v4) | ~ $i(v3) | ~ aVector0(v3) | ? [v5: $i] % 31.24/5.09 : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ($i(v6) & (( ~ (v8 = v7) % 31.24/5.09 & sdtlbdtrb0(v3, v6) = v7 & sdtlbdtrb0(v0, v6) = v8 & $i(v8) & % 31.24/5.09 $i(v7) & aNaturalNumber0(v6)) | ( ~ (v5 = v2) & % 31.24/5.09 szszuzczcdt0(v4) = v5 & $i(v5))))) & ! [v3: $i] : ( ~ % 31.24/5.09 (aDimensionOf0(v1) = v3) | ~ $i(v1) | szszuzczcdt0(v3) = v2) & ! % 31.24/5.09 [v3: $i] : ( ~ (aDimensionOf0(v1) = v3) | ~ $i(v1) | % 31.24/5.09 aVector0(v1)))))) % 31.24/5.09 % 31.24/5.09 (mDefSPN) % 31.24/5.10 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 31.24/5.10 : ! [v5: $i] : (v2 = sz00 | ~ (sdtlbdtrb0(v1, v2) = v4) | ~ (sdtlbdtrb0(v0, % 31.24/5.10 v2) = v3) | ~ (aDimensionOf0(v1) = v2) | ~ (aDimensionOf0(v0) = v2) | % 31.24/5.10 ~ (sdtasdt0(v3, v4) = v5) | ~ $i(v1) | ~ $i(v0) | ~ aVector0(v1) | ~ % 31.24/5.10 aVector0(v0) | ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : % 31.24/5.10 (sdtasasdt0(v7, v8) = v9 & sdtasasdt0(v0, v1) = v6 & sziznziztdt0(v1) = v8 & % 31.24/5.10 sziznziztdt0(v0) = v7 & sdtpldt0(v9, v5) = v6 & $i(v9) & $i(v8) & $i(v7) & % 31.24/5.10 $i(v6))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 31.24/5.10 $i] : ( ~ (sdtasasdt0(v2, v3) = v4) | ~ (sziznziztdt0(v1) = v3) | ~ % 31.24/5.10 (sziznziztdt0(v0) = v2) | ~ $i(v1) | ~ $i(v0) | ~ aVector0(v1) | ~ % 31.24/5.10 aVector0(v0) | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? % 31.24/5.10 [v9: $i] : ? [v10: $i] : ? [v11: $i] : (aDimensionOf0(v1) = v6 & $i(v6) & % 31.24/5.10 (v6 = sz00 | (v11 = v7 & sdtasasdt0(v0, v1) = v7 & sdtlbdtrb0(v1, v6) = v9 % 31.24/5.10 & sdtlbdtrb0(v0, v5) = v8 & aDimensionOf0(v0) = v5 & sdtasdt0(v8, v9) % 31.24/5.10 = v10 & sdtpldt0(v4, v10) = v7 & $i(v10) & $i(v9) & $i(v8) & $i(v7) & % 31.24/5.10 $i(v5)) | ( ~ (v6 = v5) & aDimensionOf0(v0) = v5 & $i(v5))))) & ! % 31.24/5.10 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ % 31.24/5.10 $i(v1) | ~ $i(v0) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v3: $i] : ? % 31.24/5.10 [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: % 31.24/5.10 $i] : ? [v10: $i] : ? [v11: $i] : (aDimensionOf0(v1) = v4 & $i(v4) & (v4 % 31.24/5.10 = sz00 | (v11 = v2 & sdtasasdt0(v5, v6) = v7 & sziznziztdt0(v1) = v6 & % 31.24/5.10 sziznziztdt0(v0) = v5 & sdtlbdtrb0(v1, v4) = v9 & sdtlbdtrb0(v0, v3) = % 31.24/5.10 v8 & aDimensionOf0(v0) = v3 & sdtasdt0(v8, v9) = v10 & sdtpldt0(v7, % 31.24/5.10 v10) = v2 & $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & % 31.24/5.10 $i(v3) & $i(v2)) | ( ~ (v4 = v3) & aDimensionOf0(v0) = v3 & $i(v3))))) % 31.24/5.10 % 31.24/5.10 (mDimNat) % 31.24/5.10 ! [v0: $i] : ! [v1: $i] : ( ~ (aDimensionOf0(v0) = v1) | ~ $i(v0) | ~ % 31.24/5.10 aVector0(v0) | aNaturalNumber0(v1)) % 31.24/5.10 % 31.24/5.10 (mElmSc) % 31.24/5.10 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtlbdtrb0(v0, v1) = v2) | ~ % 31.24/5.10 $i(v1) | ~ $i(v0) | ~ aVector0(v0) | ~ aNaturalNumber0(v1) | % 31.24/5.10 aScalar0(v2)) % 31.24/5.10 % 31.24/5.10 (mIH) % 31.24/5.10 ! [v0: $i] : ! [v1: $i] : ( ~ (szszuzczcdt0(v0) = v1) | ~ $i(v0) | ~ % 31.24/5.10 aNaturalNumber0(v0) | iLess0(v0, v1)) % 31.24/5.10 % 31.24/5.10 (mMDNeg) % 31.24/5.10 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 31.24/5.10 (smndt0(v1) = v3) | ~ (smndt0(v0) = v2) | ~ (sdtasdt0(v2, v3) = v4) | ~ % 31.24/5.10 $i(v1) | ~ $i(v0) | ~ aScalar0(v1) | ~ aScalar0(v0) | (sdtasdt0(v0, v1) = % 31.24/5.10 v4 & $i(v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 31.24/5.10 (sdtasdt0(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ aScalar0(v1) | ~ % 31.24/5.10 aScalar0(v0) | ? [v3: $i] : ? [v4: $i] : (smndt0(v1) = v4 & smndt0(v0) = % 31.24/5.10 v3 & sdtasdt0(v3, v4) = v2 & $i(v4) & $i(v3) & $i(v2))) % 31.24/5.10 % 31.24/5.10 (mMulSc) % 31.24/5.10 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 31.24/5.10 $i(v1) | ~ $i(v0) | ~ aScalar0(v1) | ~ aScalar0(v0) | aScalar0(v2)) % 31.24/5.10 % 31.24/5.10 (mPosMon) % 31.24/5.11 $i(sz0z00) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = % 31.24/5.11 v2) | ~ $i(v1) | ~ $i(v0) | ~ sdtlseqdt0(sz0z00, v1) | ~ % 31.24/5.11 sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ aScalar0(v0) | % 31.24/5.11 sdtlseqdt0(sz0z00, v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 31.24/5.11 (sdtasdt0(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ sdtlseqdt0(sz0z00, v1) % 31.24/5.11 | ~ sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v3: % 31.24/5.11 $i] : (sdtpldt0(v0, v1) = v3 & $i(v3) & sdtlseqdt0(sz0z00, v3))) & ! [v0: % 31.24/5.11 $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ $i(v1) | % 31.24/5.11 ~ $i(v0) | ~ sdtlseqdt0(sz0z00, v1) | ~ sdtlseqdt0(sz0z00, v0) | ~ % 31.24/5.11 aScalar0(v1) | ~ aScalar0(v0) | sdtlseqdt0(sz0z00, v2)) & ! [v0: $i] : ! % 31.24/5.11 [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | % 31.24/5.11 ~ sdtlseqdt0(sz0z00, v1) | ~ sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ % 31.24/5.11 aScalar0(v0) | ? [v3: $i] : (sdtasdt0(v0, v1) = v3 & $i(v3) & % 31.24/5.11 sdtlseqdt0(sz0z00, v3))) % 31.24/5.11 % 31.24/5.11 (mScPr) % 32.13/5.11 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasasdt0(v0, v1) = v2) | ~ % 32.13/5.11 $i(v1) | ~ $i(v0) | ~ aVector0(v1) | ~ aVector0(v0) | aScalar0(v2) | ? % 32.13/5.11 [v3: $i] : ? [v4: $i] : ( ~ (v4 = v3) & aDimensionOf0(v1) = v4 & % 32.13/5.11 aDimensionOf0(v0) = v3 & $i(v4) & $i(v3))) % 32.13/5.11 % 32.13/5.11 (m__) % 32.13/5.11 $i(xs) & $i(sz0z00) & ? [v0: $i] : (sdtasasdt0(xs, xs) = v0 & $i(v0) & ~ % 32.13/5.11 sdtlseqdt0(sz0z00, v0)) % 32.13/5.11 % 32.13/5.11 (m__1516) % 32.13/5.11 $i(xs) & $i(sz0z00) & ? [v0: $i] : (aDimensionOf0(xs) = v0 & $i(v0) & ! [v1: % 32.13/5.11 $i] : ! [v2: $i] : ( ~ (sdtasasdt0(v1, v1) = v2) | ~ $i(v1) | ~ % 32.13/5.11 aVector0(v1) | sdtlseqdt0(sz0z00, v2) | ? [v3: $i] : (aDimensionOf0(v1) = % 32.13/5.11 v3 & $i(v3) & ~ iLess0(v3, v0))) & ! [v1: $i] : ! [v2: $i] : ( ~ % 32.13/5.11 (aDimensionOf0(v1) = v2) | ~ $i(v1) | ~ aVector0(v1) | ~ iLess0(v2, v0) % 32.13/5.11 | ? [v3: $i] : (sdtasasdt0(v1, v1) = v3 & $i(v3) & sdtlseqdt0(sz0z00, % 32.13/5.11 v3)))) % 32.13/5.11 % 32.13/5.11 (m__1542) % 32.13/5.11 $i(xs) & aVector0(xs) % 32.13/5.11 % 32.13/5.11 (m__1542_01) % 32.13/5.11 $i(xs) & $i(sz00) & ? [v0: $i] : ( ~ (v0 = sz00) & aDimensionOf0(xs) = v0 & % 32.13/5.11 $i(v0)) % 32.13/5.11 % 32.13/5.11 (m__1568) % 32.13/5.11 $i(xs) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (sziznziztdt0(xs) = v0 & % 32.13/5.11 aDimensionOf0(v0) = v1 & aDimensionOf0(xs) = v2 & szszuzczcdt0(v1) = v2 & % 32.13/5.11 $i(v2) & $i(v1) & $i(v0) & aVector0(v0) & ! [v3: $i] : ! [v4: $i] : ( ~ % 32.13/5.11 (sdtlbdtrb0(v0, v3) = v4) | ~ $i(v3) | ~ aNaturalNumber0(v3) | % 32.13/5.11 (sdtlbdtrb0(xs, v3) = v4 & $i(v4))) & ! [v3: $i] : ! [v4: $i] : ( ~ % 32.13/5.11 (sdtlbdtrb0(xs, v3) = v4) | ~ $i(v3) | ~ aNaturalNumber0(v3) | % 32.13/5.11 (sdtlbdtrb0(v0, v3) = v4 & $i(v4)))) % 32.13/5.11 % 32.13/5.11 (m__1590) % 32.13/5.12 $i(xs) & $i(sz0z00) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 32.13/5.12 ? [v4: $i] : (sziznziztdt0(xs) = v0 & sdtlbdtrb0(xs, v2) = v3 & % 32.13/5.12 aDimensionOf0(v0) = v1 & aDimensionOf0(xs) = v2 & sdtasdt0(v3, v3) = v4 & % 32.13/5.12 szszuzczcdt0(v1) = v2 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & % 32.13/5.12 aVector0(v0) & sdtlseqdt0(sz0z00, v4) & ! [v5: $i] : ! [v6: $i] : ( ~ % 32.13/5.12 (sdtlbdtrb0(v0, v5) = v6) | ~ $i(v5) | ~ aNaturalNumber0(v5) | % 32.13/5.12 (sdtlbdtrb0(xs, v5) = v6 & $i(v6))) & ! [v5: $i] : ! [v6: $i] : ( ~ % 32.13/5.12 (sdtlbdtrb0(xs, v5) = v6) | ~ $i(v5) | ~ aNaturalNumber0(v5) | % 32.13/5.12 (sdtlbdtrb0(v0, v5) = v6 & $i(v6)))) % 32.13/5.12 % 32.13/5.12 (function-axioms) % 32.13/5.12 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 32.13/5.12 (sdtasasdt0(v3, v2) = v1) | ~ (sdtasasdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 32.13/5.12 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtlbdtrb0(v3, v2) = v1) % 32.13/5.12 | ~ (sdtlbdtrb0(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 32.13/5.12 ! [v3: $i] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = % 32.13/5.12 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 32.13/5.12 ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) & ! [v0: $i] : ! % 32.13/5.12 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (sziznziztdt0(v2) = v1) | ~ % 32.13/5.12 (sziznziztdt0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = % 32.13/5.12 v0 | ~ (aDimensionOf0(v2) = v1) | ~ (aDimensionOf0(v2) = v0)) & ! [v0: % 32.13/5.12 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (smndt0(v2) = v1) | ~ % 32.13/5.12 (smndt0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 32.13/5.12 (szszuzczcdt0(v2) = v1) | ~ (szszuzczcdt0(v2) = v0)) % 32.13/5.12 % 32.13/5.12 Further assumptions not needed in the proof: % 32.13/5.12 -------------------------------------------- % 32.13/5.12 mArith, mDefSPZ, mDistr, mDistr2, mEqInit, mIHOrd, mLEASm, mLEMon, mLEMonM, % 32.13/5.12 mLERef, mLETot, mLETrn, mLess, mMNeg, mNatExtr, mNatSort, mNegSc, mSZeroSc, % 32.13/5.12 mScSort, mScZero, mSqPos, mSqrt, mSuccEqu, mSuccNat, mSumSc, mVcSort, mZeroNat % 32.13/5.12 % 32.13/5.12 Those formulas are unsatisfiable: % 32.13/5.12 --------------------------------- % 32.13/5.12 % 32.13/5.12 Begin of proof % 32.13/5.12 | % 32.13/5.12 | ALPHA: (mMDNeg) implies: % 32.13/5.12 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | % 32.13/5.12 | ~ $i(v1) | ~ $i(v0) | ~ aScalar0(v1) | ~ aScalar0(v0) | ? [v3: % 32.13/5.12 | $i] : ? [v4: $i] : (smndt0(v1) = v4 & smndt0(v0) = v3 & % 32.13/5.12 | sdtasdt0(v3, v4) = v2 & $i(v4) & $i(v3) & $i(v2))) % 32.13/5.12 | % 32.13/5.12 | ALPHA: (mPosMon) implies: % 32.13/5.12 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | % 32.13/5.12 | ~ $i(v1) | ~ $i(v0) | ~ sdtlseqdt0(sz0z00, v1) | ~ % 32.13/5.12 | sdtlseqdt0(sz0z00, v0) | ~ aScalar0(v1) | ~ aScalar0(v0) | % 32.13/5.12 | sdtlseqdt0(sz0z00, v2)) % 32.13/5.12 | % 32.13/5.12 | ALPHA: (mDefInit) implies: % 32.13/5.13 | (3) ! [v0: $i] : ! [v1: $i] : ( ~ (sziznziztdt0(v0) = v1) | ~ $i(v0) | % 32.13/5.13 | ~ aVector0(v0) | ? [v2: $i] : (aDimensionOf0(v0) = v2 & $i(v2) & (v2 % 32.13/5.13 | = sz00 | ( ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ % 32.13/5.13 | (sdtlbdtrb0(v1, v4) = v5) | ~ (aDimensionOf0(v1) = v3) | ~ % 32.13/5.13 | $i(v4) | ~ $i(v1) | ~ aNaturalNumber0(v4) | (sdtlbdtrb0(v0, % 32.13/5.13 | v4) = v5 & $i(v5))) & ! [v3: $i] : ! [v4: $i] : ! [v5: % 32.13/5.13 | $i] : ( ~ (sdtlbdtrb0(v0, v4) = v5) | ~ (aDimensionOf0(v1) = % 32.13/5.13 | v3) | ~ $i(v4) | ~ $i(v1) | ~ aNaturalNumber0(v4) | % 32.13/5.13 | (sdtlbdtrb0(v1, v4) = v5 & $i(v5))) & ! [v3: $i] : ! [v4: % 32.13/5.13 | $i] : (v3 = v1 | ~ (aDimensionOf0(v3) = v4) | ~ $i(v3) | ~ % 32.13/5.13 | aVector0(v3) | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? % 32.13/5.13 | [v8: $i] : ($i(v6) & (( ~ (v8 = v7) & sdtlbdtrb0(v3, v6) = v7 % 32.13/5.13 | & sdtlbdtrb0(v0, v6) = v8 & $i(v8) & $i(v7) & % 32.13/5.13 | aNaturalNumber0(v6)) | ( ~ (v5 = v2) & szszuzczcdt0(v4) % 32.13/5.13 | = v5 & $i(v5))))) & ! [v3: $i] : ( ~ % 32.13/5.13 | (aDimensionOf0(v1) = v3) | ~ $i(v1) | szszuzczcdt0(v3) = v2) % 32.13/5.13 | & ! [v3: $i] : ( ~ (aDimensionOf0(v1) = v3) | ~ $i(v1) | % 32.13/5.13 | aVector0(v1)))))) % 32.13/5.13 | (4) ! [v0: $i] : ! [v1: $i] : (v1 = sz00 | ~ (aDimensionOf0(v0) = v1) | % 32.13/5.13 | ~ $i(v0) | ~ aVector0(v0) | ? [v2: $i] : (sziznziztdt0(v0) = v2 & % 32.13/5.13 | $i(v2) & ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ % 32.13/5.13 | (sdtlbdtrb0(v2, v4) = v5) | ~ (aDimensionOf0(v2) = v3) | ~ % 32.13/5.13 | $i(v4) | ~ aNaturalNumber0(v4) | (sdtlbdtrb0(v0, v4) = v5 & % 32.13/5.13 | $i(v5))) & ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ % 32.13/5.13 | (sdtlbdtrb0(v0, v4) = v5) | ~ (aDimensionOf0(v2) = v3) | ~ % 32.13/5.13 | $i(v4) | ~ aNaturalNumber0(v4) | (sdtlbdtrb0(v2, v4) = v5 & % 32.13/5.13 | $i(v5))) & ! [v3: $i] : ! [v4: $i] : (v3 = v2 | ~ % 32.13/5.13 | (aDimensionOf0(v3) = v4) | ~ $i(v3) | ~ aVector0(v3) | ? [v5: % 32.13/5.13 | $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ($i(v6) & (( ~ % 32.13/5.13 | (v8 = v7) & sdtlbdtrb0(v3, v6) = v7 & sdtlbdtrb0(v0, v6) = % 32.13/5.13 | v8 & $i(v8) & $i(v7) & aNaturalNumber0(v6)) | ( ~ (v5 = v1) % 32.13/5.13 | & szszuzczcdt0(v4) = v5 & $i(v5))))) & ! [v3: $i] : ( ~ % 32.13/5.13 | (aDimensionOf0(v2) = v3) | aVector0(v2)) & ! [v3: $i] : ( ~ % 32.13/5.13 | (aDimensionOf0(v2) = v3) | (szszuzczcdt0(v3) = v1 & $i(v1))))) % 32.13/5.13 | % 32.13/5.13 | ALPHA: (mDefSPN) implies: % 32.13/5.13 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasasdt0(v0, v1) = v2) % 32.13/5.13 | | ~ $i(v1) | ~ $i(v0) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v3: % 32.13/5.13 | $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? % 32.13/5.13 | [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : % 32.13/5.13 | (aDimensionOf0(v1) = v4 & $i(v4) & (v4 = sz00 | (v11 = v2 & % 32.13/5.13 | sdtasasdt0(v5, v6) = v7 & sziznziztdt0(v1) = v6 & % 32.13/5.13 | sziznziztdt0(v0) = v5 & sdtlbdtrb0(v1, v4) = v9 & % 32.13/5.13 | sdtlbdtrb0(v0, v3) = v8 & aDimensionOf0(v0) = v3 & sdtasdt0(v8, % 32.13/5.13 | v9) = v10 & sdtpldt0(v7, v10) = v2 & $i(v10) & $i(v9) & % 32.13/5.13 | $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v3) & $i(v2)) | ( ~ (v4 % 32.13/5.13 | = v3) & aDimensionOf0(v0) = v3 & $i(v3))))) % 32.13/5.13 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 32.13/5.13 | ! [v5: $i] : (v2 = sz00 | ~ (sdtlbdtrb0(v1, v2) = v4) | ~ % 32.13/5.13 | (sdtlbdtrb0(v0, v2) = v3) | ~ (aDimensionOf0(v1) = v2) | ~ % 32.13/5.13 | (aDimensionOf0(v0) = v2) | ~ (sdtasdt0(v3, v4) = v5) | ~ $i(v1) | % 32.13/5.13 | ~ $i(v0) | ~ aVector0(v1) | ~ aVector0(v0) | ? [v6: $i] : ? [v7: % 32.13/5.13 | $i] : ? [v8: $i] : ? [v9: $i] : (sdtasasdt0(v7, v8) = v9 & % 32.13/5.13 | sdtasasdt0(v0, v1) = v6 & sziznziztdt0(v1) = v8 & sziznziztdt0(v0) % 32.13/5.13 | = v7 & sdtpldt0(v9, v5) = v6 & $i(v9) & $i(v8) & $i(v7) & $i(v6))) % 32.13/5.13 | % 32.13/5.14 | ALPHA: (m__1542) implies: % 32.13/5.14 | (7) aVector0(xs) % 32.13/5.14 | % 32.13/5.14 | ALPHA: (m__1516) implies: % 32.13/5.14 | (8) ? [v0: $i] : (aDimensionOf0(xs) = v0 & $i(v0) & ! [v1: $i] : ! [v2: % 32.13/5.14 | $i] : ( ~ (sdtasasdt0(v1, v1) = v2) | ~ $i(v1) | ~ aVector0(v1) | % 32.13/5.14 | sdtlseqdt0(sz0z00, v2) | ? [v3: $i] : (aDimensionOf0(v1) = v3 & % 32.13/5.14 | $i(v3) & ~ iLess0(v3, v0))) & ! [v1: $i] : ! [v2: $i] : ( ~ % 32.13/5.14 | (aDimensionOf0(v1) = v2) | ~ $i(v1) | ~ aVector0(v1) | ~ % 32.13/5.14 | iLess0(v2, v0) | ? [v3: $i] : (sdtasasdt0(v1, v1) = v3 & $i(v3) & % 32.13/5.14 | sdtlseqdt0(sz0z00, v3)))) % 32.13/5.14 | % 32.13/5.14 | ALPHA: (m__1542_01) implies: % 32.13/5.14 | (9) ? [v0: $i] : ( ~ (v0 = sz00) & aDimensionOf0(xs) = v0 & $i(v0)) % 32.13/5.14 | % 32.13/5.14 | ALPHA: (m__1568) implies: % 32.13/5.14 | (10) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (sziznziztdt0(xs) = v0 & % 32.13/5.14 | aDimensionOf0(v0) = v1 & aDimensionOf0(xs) = v2 & szszuzczcdt0(v1) = % 32.13/5.14 | v2 & $i(v2) & $i(v1) & $i(v0) & aVector0(v0) & ! [v3: $i] : ! [v4: % 32.13/5.14 | $i] : ( ~ (sdtlbdtrb0(v0, v3) = v4) | ~ $i(v3) | ~ % 32.13/5.14 | aNaturalNumber0(v3) | (sdtlbdtrb0(xs, v3) = v4 & $i(v4))) & ! % 32.13/5.14 | [v3: $i] : ! [v4: $i] : ( ~ (sdtlbdtrb0(xs, v3) = v4) | ~ $i(v3) | % 32.13/5.14 | ~ aNaturalNumber0(v3) | (sdtlbdtrb0(v0, v3) = v4 & $i(v4)))) % 32.13/5.14 | % 32.13/5.14 | ALPHA: (m__1590) implies: % 32.13/5.14 | (11) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 32.13/5.14 | (sziznziztdt0(xs) = v0 & sdtlbdtrb0(xs, v2) = v3 & aDimensionOf0(v0) = % 32.13/5.14 | v1 & aDimensionOf0(xs) = v2 & sdtasdt0(v3, v3) = v4 & % 32.13/5.14 | szszuzczcdt0(v1) = v2 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & % 32.13/5.14 | aVector0(v0) & sdtlseqdt0(sz0z00, v4) & ! [v5: $i] : ! [v6: $i] : % 32.13/5.14 | ( ~ (sdtlbdtrb0(v0, v5) = v6) | ~ $i(v5) | ~ aNaturalNumber0(v5) | % 32.13/5.14 | (sdtlbdtrb0(xs, v5) = v6 & $i(v6))) & ! [v5: $i] : ! [v6: $i] : % 32.13/5.14 | ( ~ (sdtlbdtrb0(xs, v5) = v6) | ~ $i(v5) | ~ aNaturalNumber0(v5) | % 32.13/5.14 | (sdtlbdtrb0(v0, v5) = v6 & $i(v6)))) % 32.13/5.14 | % 32.13/5.14 | ALPHA: (m__) implies: % 32.13/5.14 | (12) $i(xs) % 32.13/5.14 | (13) ? [v0: $i] : (sdtasasdt0(xs, xs) = v0 & $i(v0) & ~ % 32.13/5.14 | sdtlseqdt0(sz0z00, v0)) % 32.13/5.14 | % 32.13/5.14 | ALPHA: (function-axioms) implies: % 32.13/5.14 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 32.13/5.14 | (aDimensionOf0(v2) = v1) | ~ (aDimensionOf0(v2) = v0)) % 32.13/5.14 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 32.13/5.14 | (sziznziztdt0(v2) = v1) | ~ (sziznziztdt0(v2) = v0)) % 32.13/5.14 | (16) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 32.13/5.14 | (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 32.13/5.14 | (17) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 32.13/5.14 | (sdtlbdtrb0(v3, v2) = v1) | ~ (sdtlbdtrb0(v3, v2) = v0)) % 32.13/5.15 | (18) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 32.13/5.15 | (sdtasasdt0(v3, v2) = v1) | ~ (sdtasasdt0(v3, v2) = v0)) % 32.13/5.15 | % 32.13/5.15 | DELTA: instantiating (13) with fresh symbol all_32_0 gives: % 32.13/5.15 | (19) sdtasasdt0(xs, xs) = all_32_0 & $i(all_32_0) & ~ sdtlseqdt0(sz0z00, % 32.13/5.15 | all_32_0) % 32.13/5.15 | % 32.13/5.15 | ALPHA: (19) implies: % 32.13/5.15 | (20) ~ sdtlseqdt0(sz0z00, all_32_0) % 32.13/5.15 | (21) sdtasasdt0(xs, xs) = all_32_0 % 32.13/5.15 | % 32.13/5.15 | DELTA: instantiating (9) with fresh symbol all_34_0 gives: % 32.13/5.15 | (22) ~ (all_34_0 = sz00) & aDimensionOf0(xs) = all_34_0 & $i(all_34_0) % 32.13/5.15 | % 32.13/5.15 | ALPHA: (22) implies: % 32.13/5.15 | (23) ~ (all_34_0 = sz00) % 32.13/5.15 | (24) aDimensionOf0(xs) = all_34_0 % 32.13/5.15 | % 32.13/5.15 | DELTA: instantiating (8) with fresh symbol all_36_0 gives: % 32.13/5.15 | (25) aDimensionOf0(xs) = all_36_0 & $i(all_36_0) & ! [v0: $i] : ! [v1: % 32.13/5.15 | $i] : ( ~ (sdtasasdt0(v0, v0) = v1) | ~ $i(v0) | ~ aVector0(v0) | % 32.13/5.15 | sdtlseqdt0(sz0z00, v1) | ? [v2: $i] : (aDimensionOf0(v0) = v2 & % 32.13/5.15 | $i(v2) & ~ iLess0(v2, all_36_0))) & ! [v0: $i] : ! [v1: $i] : ( % 32.13/5.15 | ~ (aDimensionOf0(v0) = v1) | ~ $i(v0) | ~ aVector0(v0) | ~ % 32.13/5.15 | iLess0(v1, all_36_0) | ? [v2: $i] : (sdtasasdt0(v0, v0) = v2 & % 32.13/5.15 | $i(v2) & sdtlseqdt0(sz0z00, v2))) % 32.13/5.15 | % 32.13/5.15 | ALPHA: (25) implies: % 32.13/5.15 | (26) aDimensionOf0(xs) = all_36_0 % 32.13/5.15 | (27) ! [v0: $i] : ! [v1: $i] : ( ~ (sdtasasdt0(v0, v0) = v1) | ~ $i(v0) % 32.13/5.15 | | ~ aVector0(v0) | sdtlseqdt0(sz0z00, v1) | ? [v2: $i] : % 32.13/5.15 | (aDimensionOf0(v0) = v2 & $i(v2) & ~ iLess0(v2, all_36_0))) % 32.13/5.15 | % 32.13/5.15 | DELTA: instantiating (10) with fresh symbols all_39_0, all_39_1, all_39_2 % 32.13/5.15 | gives: % 32.13/5.15 | (28) sziznziztdt0(xs) = all_39_2 & aDimensionOf0(all_39_2) = all_39_1 & % 32.13/5.15 | aDimensionOf0(xs) = all_39_0 & szszuzczcdt0(all_39_1) = all_39_0 & % 32.13/5.15 | $i(all_39_0) & $i(all_39_1) & $i(all_39_2) & aVector0(all_39_2) & ! % 32.13/5.15 | [v0: $i] : ! [v1: $i] : ( ~ (sdtlbdtrb0(all_39_2, v0) = v1) | ~ % 32.13/5.15 | $i(v0) | ~ aNaturalNumber0(v0) | (sdtlbdtrb0(xs, v0) = v1 & % 32.13/5.15 | $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtlbdtrb0(xs, v0) = % 32.13/5.15 | v1) | ~ $i(v0) | ~ aNaturalNumber0(v0) | (sdtlbdtrb0(all_39_2, % 32.13/5.15 | v0) = v1 & $i(v1))) % 32.13/5.15 | % 32.13/5.15 | ALPHA: (28) implies: % 32.13/5.15 | (29) aDimensionOf0(xs) = all_39_0 % 32.13/5.15 | (30) aDimensionOf0(all_39_2) = all_39_1 % 32.13/5.15 | (31) sziznziztdt0(xs) = all_39_2 % 32.13/5.15 | (32) ! [v0: $i] : ! [v1: $i] : ( ~ (sdtlbdtrb0(xs, v0) = v1) | ~ $i(v0) % 32.13/5.15 | | ~ aNaturalNumber0(v0) | (sdtlbdtrb0(all_39_2, v0) = v1 & $i(v1))) % 32.13/5.15 | % 32.13/5.15 | DELTA: instantiating (11) with fresh symbols all_42_0, all_42_1, all_42_2, % 32.13/5.15 | all_42_3, all_42_4 gives: % 32.13/5.15 | (33) sziznziztdt0(xs) = all_42_4 & sdtlbdtrb0(xs, all_42_2) = all_42_1 & % 32.13/5.15 | aDimensionOf0(all_42_4) = all_42_3 & aDimensionOf0(xs) = all_42_2 & % 32.13/5.15 | sdtasdt0(all_42_1, all_42_1) = all_42_0 & szszuzczcdt0(all_42_3) = % 32.13/5.15 | all_42_2 & $i(all_42_0) & $i(all_42_1) & $i(all_42_2) & $i(all_42_3) & % 32.13/5.15 | $i(all_42_4) & aVector0(all_42_4) & sdtlseqdt0(sz0z00, all_42_0) & ! % 32.13/5.15 | [v0: $i] : ! [v1: $i] : ( ~ (sdtlbdtrb0(all_42_4, v0) = v1) | ~ % 32.13/5.15 | $i(v0) | ~ aNaturalNumber0(v0) | (sdtlbdtrb0(xs, v0) = v1 & % 32.13/5.15 | $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtlbdtrb0(xs, v0) = % 32.13/5.15 | v1) | ~ $i(v0) | ~ aNaturalNumber0(v0) | (sdtlbdtrb0(all_42_4, % 32.13/5.15 | v0) = v1 & $i(v1))) % 32.13/5.15 | % 32.13/5.15 | ALPHA: (33) implies: % 32.13/5.15 | (34) sdtlseqdt0(sz0z00, all_42_0) % 32.13/5.15 | (35) aVector0(all_42_4) % 32.13/5.15 | (36) $i(all_42_4) % 32.13/5.15 | (37) $i(all_42_3) % 32.13/5.15 | (38) szszuzczcdt0(all_42_3) = all_42_2 % 32.13/5.15 | (39) sdtasdt0(all_42_1, all_42_1) = all_42_0 % 32.13/5.15 | (40) aDimensionOf0(xs) = all_42_2 % 32.13/5.15 | (41) aDimensionOf0(all_42_4) = all_42_3 % 32.13/5.15 | (42) sdtlbdtrb0(xs, all_42_2) = all_42_1 % 32.13/5.15 | (43) sziznziztdt0(xs) = all_42_4 % 32.13/5.15 | % 32.13/5.16 | GROUND_INST: instantiating (14) with all_36_0, all_39_0, xs, simplifying with % 32.13/5.16 | (26), (29) gives: % 32.13/5.16 | (44) all_39_0 = all_36_0 % 32.13/5.16 | % 32.13/5.16 | GROUND_INST: instantiating (14) with all_39_0, all_42_2, xs, simplifying with % 32.13/5.16 | (29), (40) gives: % 32.13/5.16 | (45) all_42_2 = all_39_0 % 32.13/5.16 | % 32.13/5.16 | GROUND_INST: instantiating (14) with all_34_0, all_42_2, xs, simplifying with % 32.13/5.16 | (24), (40) gives: % 32.13/5.16 | (46) all_42_2 = all_34_0 % 32.13/5.16 | % 32.13/5.16 | GROUND_INST: instantiating (14) with all_39_1, all_42_3, all_39_2, simplifying % 32.13/5.16 | with (30) gives: % 32.13/5.16 | (47) all_42_3 = all_39_1 | ~ (aDimensionOf0(all_39_2) = all_42_3) % 32.13/5.16 | % 32.13/5.16 | GROUND_INST: instantiating (15) with all_39_2, all_42_4, xs, simplifying with % 32.13/5.16 | (31), (43) gives: % 32.13/5.16 | (48) all_42_4 = all_39_2 % 32.13/5.16 | % 32.13/5.16 | COMBINE_EQS: (45), (46) imply: % 32.13/5.16 | (49) all_39_0 = all_34_0 % 32.13/5.16 | % 32.13/5.16 | SIMP: (49) implies: % 32.13/5.16 | (50) all_39_0 = all_34_0 % 32.13/5.16 | % 32.13/5.16 | COMBINE_EQS: (44), (50) imply: % 32.13/5.16 | (51) all_36_0 = all_34_0 % 32.13/5.16 | % 32.13/5.16 | SIMP: (51) implies: % 32.13/5.16 | (52) all_36_0 = all_34_0 % 32.13/5.16 | % 32.13/5.16 | REDUCE: (42), (46) imply: % 32.13/5.16 | (53) sdtlbdtrb0(xs, all_34_0) = all_42_1 % 32.13/5.16 | % 32.13/5.16 | REDUCE: (41), (48) imply: % 32.13/5.16 | (54) aDimensionOf0(all_39_2) = all_42_3 % 32.13/5.16 | % 32.13/5.16 | REDUCE: (38), (46) imply: % 32.13/5.16 | (55) szszuzczcdt0(all_42_3) = all_34_0 % 32.13/5.16 | % 32.13/5.16 | REDUCE: (36), (48) imply: % 32.13/5.16 | (56) $i(all_39_2) % 32.13/5.16 | % 32.13/5.16 | REDUCE: (35), (48) imply: % 32.13/5.16 | (57) aVector0(all_39_2) % 32.13/5.16 | % 32.13/5.16 | BETA: splitting (47) gives: % 32.13/5.16 | % 32.13/5.16 | Case 1: % 32.13/5.16 | | % 32.13/5.16 | | (58) ~ (aDimensionOf0(all_39_2) = all_42_3) % 32.13/5.16 | | % 32.13/5.16 | | PRED_UNIFY: (54), (58) imply: % 32.13/5.16 | | (59) $false % 32.13/5.16 | | % 32.13/5.16 | | CLOSE: (59) is inconsistent. % 32.13/5.16 | | % 32.13/5.16 | Case 2: % 32.13/5.16 | | % 32.13/5.16 | | (60) all_42_3 = all_39_1 % 32.13/5.16 | | % 32.13/5.16 | | REDUCE: (55), (60) imply: % 32.13/5.16 | | (61) szszuzczcdt0(all_39_1) = all_34_0 % 32.13/5.16 | | % 32.13/5.16 | | REDUCE: (37), (60) imply: % 32.13/5.16 | | (62) $i(all_39_1) % 32.13/5.16 | | % 32.13/5.16 | | GROUND_INST: instantiating (4) with xs, all_34_0, simplifying with (7), % 32.13/5.16 | | (12), (24) gives: % 32.13/5.16 | | (63) all_34_0 = sz00 | ? [v0: $i] : (sziznziztdt0(xs) = v0 & $i(v0) & ! % 32.13/5.16 | | [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (sdtlbdtrb0(v0, v2) = % 32.13/5.16 | | v3) | ~ (aDimensionOf0(v0) = v1) | ~ $i(v2) | ~ % 32.13/5.16 | | aNaturalNumber0(v2) | (sdtlbdtrb0(xs, v2) = v3 & $i(v3))) & ! % 32.13/5.16 | | [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (sdtlbdtrb0(xs, v2) = % 32.13/5.16 | | v3) | ~ (aDimensionOf0(v0) = v1) | ~ $i(v2) | ~ % 32.13/5.16 | | aNaturalNumber0(v2) | (sdtlbdtrb0(v0, v2) = v3 & $i(v3))) & ! % 32.13/5.16 | | [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (aDimensionOf0(v1) = v2) | % 32.13/5.16 | | ~ $i(v1) | ~ aVector0(v1) | ? [v3: any] : ? [v4: $i] : ? % 32.13/5.16 | | [v5: $i] : ? [v6: $i] : ($i(v4) & (( ~ (v6 = v5) & % 32.13/5.16 | | sdtlbdtrb0(v1, v4) = v5 & sdtlbdtrb0(xs, v4) = v6 & $i(v6) % 32.13/5.16 | | & $i(v5) & aNaturalNumber0(v4)) | ( ~ (v3 = all_34_0) & % 32.13/5.16 | | szszuzczcdt0(v2) = v3 & $i(v3))))) & ! [v1: $i] : ( ~ % 32.13/5.16 | | (aDimensionOf0(v0) = v1) | aVector0(v0)) & ! [v1: $i] : ( ~ % 32.13/5.16 | | (aDimensionOf0(v0) = v1) | (szszuzczcdt0(v1) = all_34_0 & % 32.13/5.16 | | $i(all_34_0)))) % 32.13/5.16 | | % 32.13/5.16 | | GROUND_INST: instantiating (mDimNat) with xs, all_34_0, simplifying with % 32.13/5.16 | | (7), (12), (24) gives: % 32.13/5.16 | | (64) aNaturalNumber0(all_34_0) % 32.13/5.16 | | % 32.13/5.16 | | GROUND_INST: instantiating (mDimNat) with all_39_2, all_39_1, simplifying % 32.13/5.16 | | with (30), (56), (57) gives: % 32.13/5.16 | | (65) aNaturalNumber0(all_39_1) % 32.13/5.16 | | % 32.13/5.16 | | GROUND_INST: instantiating (6) with xs, xs, all_34_0, all_42_1, all_42_1, % 32.13/5.16 | | all_42_0, simplifying with (7), (12), (24), (39), (53) gives: % 32.13/5.16 | | (66) all_34_0 = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 32.13/5.16 | | $i] : (sdtasasdt0(v1, v2) = v3 & sdtasasdt0(xs, xs) = v0 & % 32.13/5.16 | | sziznziztdt0(xs) = v2 & sziznziztdt0(xs) = v1 & sdtpldt0(v3, % 32.13/5.16 | | all_42_0) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 32.13/5.16 | | % 32.13/5.17 | | GROUND_INST: instantiating (3) with xs, all_39_2, simplifying with (7), % 32.13/5.17 | | (12), (31) gives: % 32.13/5.17 | | (67) ? [v0: $i] : (aDimensionOf0(xs) = v0 & $i(v0) & (v0 = sz00 | ( ! % 32.13/5.17 | | [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 32.13/5.17 | | (sdtlbdtrb0(all_39_2, v2) = v3) | ~ % 32.13/5.17 | | (aDimensionOf0(all_39_2) = v1) | ~ $i(v2) | ~ $i(all_39_2) % 32.13/5.17 | | | ~ aNaturalNumber0(v2) | (sdtlbdtrb0(xs, v2) = v3 & % 32.13/5.17 | | $i(v3))) & ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 32.13/5.17 | | (sdtlbdtrb0(xs, v2) = v3) | ~ (aDimensionOf0(all_39_2) = % 32.13/5.17 | | v1) | ~ $i(v2) | ~ $i(all_39_2) | ~ aNaturalNumber0(v2) % 32.13/5.17 | | | (sdtlbdtrb0(all_39_2, v2) = v3 & $i(v3))) & ! [v1: any] : % 32.13/5.17 | | ! [v2: $i] : (v1 = all_39_2 | ~ (aDimensionOf0(v1) = v2) | % 32.13/5.17 | | ~ $i(v1) | ~ aVector0(v1) | ? [v3: $i] : ? [v4: $i] : ? % 32.13/5.17 | | [v5: $i] : ? [v6: $i] : ($i(v4) & (( ~ (v6 = v5) & % 32.13/5.17 | | sdtlbdtrb0(v1, v4) = v5 & sdtlbdtrb0(xs, v4) = v6 & % 32.13/5.17 | | $i(v6) & $i(v5) & aNaturalNumber0(v4)) | ( ~ (v3 = v0) % 32.13/5.17 | | & szszuzczcdt0(v2) = v3 & $i(v3))))) & ! [v1: $i] : ( % 32.13/5.17 | | ~ (aDimensionOf0(all_39_2) = v1) | ~ $i(all_39_2) | % 32.13/5.17 | | szszuzczcdt0(v1) = v0) & ! [v1: $i] : ( ~ % 32.13/5.17 | | (aDimensionOf0(all_39_2) = v1) | ~ $i(all_39_2) | % 32.13/5.17 | | aVector0(all_39_2))))) % 32.13/5.17 | | % 32.13/5.17 | | GROUND_INST: instantiating (5) with xs, xs, all_32_0, simplifying with (7), % 32.13/5.17 | | (12), (21) gives: % 32.64/5.17 | | (68) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] % 32.64/5.17 | | : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: int] : % 32.64/5.17 | | (aDimensionOf0(xs) = v1 & $i(v1) & (v1 = sz00 | (v8 = all_32_0 & % 32.64/5.17 | | sdtasasdt0(v2, v3) = v4 & sziznziztdt0(xs) = v3 & % 32.64/5.17 | | sziznziztdt0(xs) = v2 & sdtlbdtrb0(xs, v1) = v6 & % 32.64/5.17 | | sdtlbdtrb0(xs, v0) = v5 & aDimensionOf0(xs) = v0 & % 32.64/5.17 | | sdtasdt0(v5, v6) = v7 & sdtpldt0(v4, v7) = all_32_0 & $i(v7) & % 32.64/5.17 | | $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v0) & % 32.64/5.17 | | $i(all_32_0)) | ( ~ (v1 = v0) & aDimensionOf0(xs) = v0 & % 32.64/5.17 | | $i(v0)))) % 32.64/5.17 | | % 32.64/5.17 | | GROUND_INST: instantiating (27) with xs, all_32_0, simplifying with (7), % 32.64/5.17 | | (12), (20), (21) gives: % 32.64/5.17 | | (69) ? [v0: $i] : (aDimensionOf0(xs) = v0 & $i(v0) & ~ iLess0(v0, % 32.64/5.17 | | all_36_0)) % 32.64/5.17 | | % 32.64/5.17 | | DELTA: instantiating (69) with fresh symbol all_62_0 gives: % 32.64/5.17 | | (70) aDimensionOf0(xs) = all_62_0 & $i(all_62_0) & ~ iLess0(all_62_0, % 32.64/5.17 | | all_36_0) % 32.64/5.17 | | % 32.64/5.17 | | ALPHA: (70) implies: % 32.64/5.17 | | (71) ~ iLess0(all_62_0, all_36_0) % 32.64/5.17 | | (72) aDimensionOf0(xs) = all_62_0 % 32.64/5.17 | | % 32.64/5.17 | | DELTA: instantiating (68) with fresh symbols all_65_0, all_65_1, all_65_2, % 32.64/5.17 | | all_65_3, all_65_4, all_65_5, all_65_6, all_65_7, all_65_8 gives: % 32.64/5.17 | | (73) aDimensionOf0(xs) = all_65_7 & $i(all_65_7) & (all_65_7 = sz00 | % 32.64/5.17 | | (all_65_0 = all_32_0 & sdtasasdt0(all_65_6, all_65_5) = all_65_4 & % 32.64/5.17 | | sziznziztdt0(xs) = all_65_5 & sziznziztdt0(xs) = all_65_6 & % 32.64/5.17 | | sdtlbdtrb0(xs, all_65_7) = all_65_2 & sdtlbdtrb0(xs, all_65_8) = % 32.64/5.17 | | all_65_3 & aDimensionOf0(xs) = all_65_8 & sdtasdt0(all_65_3, % 32.64/5.17 | | all_65_2) = all_65_1 & sdtpldt0(all_65_4, all_65_1) = all_32_0 % 32.64/5.17 | | & $i(all_65_1) & $i(all_65_2) & $i(all_65_3) & $i(all_65_4) & % 32.64/5.17 | | $i(all_65_5) & $i(all_65_6) & $i(all_65_8) & $i(all_32_0)) | ( ~ % 32.64/5.17 | | (all_65_7 = all_65_8) & aDimensionOf0(xs) = all_65_8 & % 32.64/5.17 | | $i(all_65_8))) % 32.64/5.17 | | % 32.64/5.17 | | ALPHA: (73) implies: % 32.64/5.17 | | (74) aDimensionOf0(xs) = all_65_7 % 32.64/5.17 | | (75) all_65_7 = sz00 | (all_65_0 = all_32_0 & sdtasasdt0(all_65_6, % 32.64/5.17 | | all_65_5) = all_65_4 & sziznziztdt0(xs) = all_65_5 & % 32.64/5.17 | | sziznziztdt0(xs) = all_65_6 & sdtlbdtrb0(xs, all_65_7) = all_65_2 % 32.64/5.17 | | & sdtlbdtrb0(xs, all_65_8) = all_65_3 & aDimensionOf0(xs) = % 32.64/5.17 | | all_65_8 & sdtasdt0(all_65_3, all_65_2) = all_65_1 & % 32.64/5.17 | | sdtpldt0(all_65_4, all_65_1) = all_32_0 & $i(all_65_1) & % 32.64/5.17 | | $i(all_65_2) & $i(all_65_3) & $i(all_65_4) & $i(all_65_5) & % 32.64/5.17 | | $i(all_65_6) & $i(all_65_8) & $i(all_32_0)) | ( ~ (all_65_7 = % 32.64/5.17 | | all_65_8) & aDimensionOf0(xs) = all_65_8 & $i(all_65_8)) % 32.64/5.17 | | % 32.64/5.17 | | DELTA: instantiating (67) with fresh symbol all_67_0 gives: % 32.64/5.17 | | (76) aDimensionOf0(xs) = all_67_0 & $i(all_67_0) & (all_67_0 = sz00 | ( ! % 32.64/5.17 | | [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtlbdtrb0(all_39_2, % 32.64/5.17 | | v1) = v2) | ~ (aDimensionOf0(all_39_2) = v0) | ~ $i(v1) % 32.64/5.17 | | | ~ $i(all_39_2) | ~ aNaturalNumber0(v1) | (sdtlbdtrb0(xs, % 32.64/5.17 | | v1) = v2 & $i(v2))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 32.64/5.17 | | $i] : ( ~ (sdtlbdtrb0(xs, v1) = v2) | ~ % 32.64/5.17 | | (aDimensionOf0(all_39_2) = v0) | ~ $i(v1) | ~ $i(all_39_2) | % 32.64/5.17 | | ~ aNaturalNumber0(v1) | (sdtlbdtrb0(all_39_2, v1) = v2 & % 32.64/5.17 | | $i(v2))) & ! [v0: any] : ! [v1: $i] : (v0 = all_39_2 | ~ % 32.64/5.17 | | (aDimensionOf0(v0) = v1) | ~ $i(v0) | ~ aVector0(v0) | ? % 32.64/5.17 | | [v2: any] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ($i(v3) % 32.64/5.17 | | & (( ~ (v5 = v4) & sdtlbdtrb0(v0, v3) = v4 & sdtlbdtrb0(xs, % 32.64/5.17 | | v3) = v5 & $i(v5) & $i(v4) & aNaturalNumber0(v3)) | ( % 32.64/5.17 | | ~ (v2 = all_67_0) & szszuzczcdt0(v1) = v2 & $i(v2))))) & % 32.64/5.17 | | ! [v0: $i] : ( ~ (aDimensionOf0(all_39_2) = v0) | ~ % 32.64/5.17 | | $i(all_39_2) | szszuzczcdt0(v0) = all_67_0) & ! [v0: $i] : ( % 32.64/5.17 | | ~ (aDimensionOf0(all_39_2) = v0) | ~ $i(all_39_2) | % 32.64/5.17 | | aVector0(all_39_2)))) % 32.64/5.17 | | % 32.64/5.17 | | ALPHA: (76) implies: % 32.64/5.17 | | (77) aDimensionOf0(xs) = all_67_0 % 32.64/5.18 | | (78) all_67_0 = sz00 | ( ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 32.64/5.18 | | (sdtlbdtrb0(all_39_2, v1) = v2) | ~ (aDimensionOf0(all_39_2) = % 32.64/5.18 | | v0) | ~ $i(v1) | ~ $i(all_39_2) | ~ aNaturalNumber0(v1) | % 32.64/5.18 | | (sdtlbdtrb0(xs, v1) = v2 & $i(v2))) & ! [v0: $i] : ! [v1: $i] % 32.64/5.18 | | : ! [v2: $i] : ( ~ (sdtlbdtrb0(xs, v1) = v2) | ~ % 32.64/5.18 | | (aDimensionOf0(all_39_2) = v0) | ~ $i(v1) | ~ $i(all_39_2) | % 32.64/5.18 | | ~ aNaturalNumber0(v1) | (sdtlbdtrb0(all_39_2, v1) = v2 & % 32.64/5.18 | | $i(v2))) & ! [v0: any] : ! [v1: $i] : (v0 = all_39_2 | ~ % 32.64/5.18 | | (aDimensionOf0(v0) = v1) | ~ $i(v0) | ~ aVector0(v0) | ? [v2: % 32.64/5.18 | | any] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ($i(v3) & (( % 32.64/5.18 | | ~ (v5 = v4) & sdtlbdtrb0(v0, v3) = v4 & sdtlbdtrb0(xs, v3) % 32.64/5.18 | | = v5 & $i(v5) & $i(v4) & aNaturalNumber0(v3)) | ( ~ (v2 = % 32.64/5.18 | | all_67_0) & szszuzczcdt0(v1) = v2 & $i(v2))))) & ! [v0: % 32.64/5.18 | | $i] : ( ~ (aDimensionOf0(all_39_2) = v0) | ~ $i(all_39_2) | % 32.64/5.18 | | szszuzczcdt0(v0) = all_67_0) & ! [v0: $i] : ( ~ % 32.64/5.18 | | (aDimensionOf0(all_39_2) = v0) | ~ $i(all_39_2) | % 32.64/5.18 | | aVector0(all_39_2))) % 32.64/5.18 | | % 32.64/5.18 | | REDUCE: (52), (71) imply: % 32.64/5.18 | | (79) ~ iLess0(all_62_0, all_34_0) % 32.64/5.18 | | % 32.64/5.18 | | BETA: splitting (63) gives: % 32.64/5.18 | | % 32.64/5.18 | | Case 1: % 32.64/5.18 | | | % 32.64/5.18 | | | (80) all_34_0 = sz00 % 32.64/5.18 | | | % 32.64/5.18 | | | REDUCE: (23), (80) imply: % 32.64/5.18 | | | (81) $false % 32.64/5.18 | | | % 32.64/5.18 | | | CLOSE: (81) is inconsistent. % 32.64/5.18 | | | % 32.64/5.18 | | Case 2: % 32.64/5.18 | | | % 32.64/5.18 | | | (82) ? [v0: $i] : (sziznziztdt0(xs) = v0 & $i(v0) & ! [v1: $i] : ! % 32.64/5.18 | | | [v2: $i] : ! [v3: $i] : ( ~ (sdtlbdtrb0(v0, v2) = v3) | ~ % 32.64/5.18 | | | (aDimensionOf0(v0) = v1) | ~ $i(v2) | ~ aNaturalNumber0(v2) % 32.64/5.18 | | | | (sdtlbdtrb0(xs, v2) = v3 & $i(v3))) & ! [v1: $i] : ! [v2: % 32.64/5.18 | | | $i] : ! [v3: $i] : ( ~ (sdtlbdtrb0(xs, v2) = v3) | ~ % 32.64/5.18 | | | (aDimensionOf0(v0) = v1) | ~ $i(v2) | ~ aNaturalNumber0(v2) % 32.64/5.18 | | | | (sdtlbdtrb0(v0, v2) = v3 & $i(v3))) & ! [v1: $i] : ! [v2: % 32.64/5.18 | | | $i] : (v1 = v0 | ~ (aDimensionOf0(v1) = v2) | ~ $i(v1) | ~ % 32.64/5.18 | | | aVector0(v1) | ? [v3: any] : ? [v4: $i] : ? [v5: $i] : ? % 32.64/5.18 | | | [v6: $i] : ($i(v4) & (( ~ (v6 = v5) & sdtlbdtrb0(v1, v4) = v5 % 32.64/5.18 | | | & sdtlbdtrb0(xs, v4) = v6 & $i(v6) & $i(v5) & % 32.64/5.18 | | | aNaturalNumber0(v4)) | ( ~ (v3 = all_34_0) & % 32.64/5.18 | | | szszuzczcdt0(v2) = v3 & $i(v3))))) & ! [v1: $i] : ( ~ % 32.64/5.18 | | | (aDimensionOf0(v0) = v1) | aVector0(v0)) & ! [v1: $i] : ( ~ % 32.64/5.18 | | | (aDimensionOf0(v0) = v1) | (szszuzczcdt0(v1) = all_34_0 & % 32.64/5.18 | | | $i(all_34_0)))) % 32.64/5.18 | | | % 32.64/5.18 | | | DELTA: instantiating (82) with fresh symbol all_76_0 gives: % 32.64/5.18 | | | (83) sziznziztdt0(xs) = all_76_0 & $i(all_76_0) & ! [v0: $i] : ! [v1: % 32.64/5.18 | | | $i] : ! [v2: $i] : ( ~ (sdtlbdtrb0(all_76_0, v1) = v2) | ~ % 32.64/5.18 | | | (aDimensionOf0(all_76_0) = v0) | ~ $i(v1) | ~ % 32.64/5.18 | | | aNaturalNumber0(v1) | (sdtlbdtrb0(xs, v1) = v2 & $i(v2))) & ! % 32.64/5.18 | | | [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtlbdtrb0(xs, v1) = % 32.64/5.18 | | | v2) | ~ (aDimensionOf0(all_76_0) = v0) | ~ $i(v1) | ~ % 32.64/5.18 | | | aNaturalNumber0(v1) | (sdtlbdtrb0(all_76_0, v1) = v2 & $i(v2))) % 32.64/5.18 | | | & ! [v0: any] : ! [v1: $i] : (v0 = all_76_0 | ~ % 32.64/5.18 | | | (aDimensionOf0(v0) = v1) | ~ $i(v0) | ~ aVector0(v0) | ? [v2: % 32.64/5.18 | | | any] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ($i(v3) & (( % 32.64/5.18 | | | ~ (v5 = v4) & sdtlbdtrb0(v0, v3) = v4 & sdtlbdtrb0(xs, v3) % 32.64/5.18 | | | = v5 & $i(v5) & $i(v4) & aNaturalNumber0(v3)) | ( ~ (v2 = % 32.64/5.18 | | | all_34_0) & szszuzczcdt0(v1) = v2 & $i(v2))))) & ! [v0: % 32.64/5.18 | | | $i] : ( ~ (aDimensionOf0(all_76_0) = v0) | aVector0(all_76_0)) & % 32.64/5.18 | | | ! [v0: $i] : ( ~ (aDimensionOf0(all_76_0) = v0) | % 32.64/5.18 | | | (szszuzczcdt0(v0) = all_34_0 & $i(all_34_0))) % 32.64/5.18 | | | % 32.64/5.18 | | | ALPHA: (83) implies: % 32.64/5.18 | | | (84) $i(all_76_0) % 32.64/5.18 | | | (85) sziznziztdt0(xs) = all_76_0 % 32.64/5.18 | | | % 32.64/5.18 | | | BETA: splitting (66) gives: % 32.64/5.18 | | | % 32.64/5.18 | | | Case 1: % 32.64/5.18 | | | | % 32.64/5.20 | | | | (86) all_34_0 = sz00 % 32.64/5.20 | | | | % 32.64/5.20 | | | | REDUCE: (23), (86) imply: % 32.64/5.20 | | | | (87) $false % 32.64/5.20 | | | | % 32.64/5.20 | | | | CLOSE: (87) is inconsistent. % 32.64/5.20 | | | | % 32.64/5.20 | | | Case 2: % 32.64/5.20 | | | | % 32.64/5.20 | | | | (88) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 32.64/5.20 | | | | (sdtasasdt0(v1, v2) = v3 & sdtasasdt0(xs, xs) = v0 & % 32.64/5.20 | | | | sziznziztdt0(xs) = v2 & sziznziztdt0(xs) = v1 & sdtpldt0(v3, % 32.64/5.20 | | | | all_42_0) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 32.64/5.20 | | | | % 32.64/5.20 | | | | DELTA: instantiating (88) with fresh symbols all_82_0, all_82_1, % 32.64/5.20 | | | | all_82_2, all_82_3 gives: % 32.64/5.20 | | | | (89) sdtasasdt0(all_82_2, all_82_1) = all_82_0 & sdtasasdt0(xs, xs) = % 32.64/5.20 | | | | all_82_3 & sziznziztdt0(xs) = all_82_1 & sziznziztdt0(xs) = % 32.64/5.20 | | | | all_82_2 & sdtpldt0(all_82_0, all_42_0) = all_82_3 & % 32.64/5.20 | | | | $i(all_82_0) & $i(all_82_1) & $i(all_82_2) & $i(all_82_3) % 32.64/5.20 | | | | % 32.64/5.20 | | | | ALPHA: (89) implies: % 32.64/5.20 | | | | (90) $i(all_82_0) % 32.64/5.20 | | | | (91) sziznziztdt0(xs) = all_82_2 % 32.64/5.20 | | | | (92) sziznziztdt0(xs) = all_82_1 % 32.64/5.20 | | | | (93) sdtasasdt0(all_82_2, all_82_1) = all_82_0 % 32.64/5.20 | | | | % 32.64/5.20 | | | | GROUND_INST: instantiating (14) with all_34_0, all_65_7, xs, simplifying % 32.64/5.20 | | | | with (24), (74) gives: % 32.64/5.20 | | | | (94) all_65_7 = all_34_0 % 32.64/5.20 | | | | % 32.64/5.20 | | | | GROUND_INST: instantiating (14) with all_65_7, all_67_0, xs, simplifying % 32.64/5.20 | | | | with (74), (77) gives: % 32.64/5.20 | | | | (95) all_67_0 = all_65_7 % 32.64/5.20 | | | | % 32.64/5.20 | | | | GROUND_INST: instantiating (14) with all_62_0, all_67_0, xs, simplifying % 32.64/5.20 | | | | with (72), (77) gives: % 32.64/5.20 | | | | (96) all_67_0 = all_62_0 % 32.64/5.20 | | | | % 32.64/5.20 | | | | GROUND_INST: instantiating (15) with all_39_2, all_82_2, xs, simplifying % 32.64/5.20 | | | | with (31), (91) gives: % 32.64/5.20 | | | | (97) all_82_2 = all_39_2 % 32.64/5.20 | | | | % 32.64/5.20 | | | | GROUND_INST: instantiating (15) with all_82_2, all_82_1, xs, simplifying % 32.64/5.20 | | | | with (91), (92) gives: % 32.64/5.20 | | | | (98) all_82_1 = all_82_2 % 32.64/5.20 | | | | % 32.64/5.20 | | | | GROUND_INST: instantiating (15) with all_76_0, all_82_1, xs, simplifying % 32.64/5.20 | | | | with (85), (92) gives: % 32.64/5.20 | | | | (99) all_82_1 = all_76_0 % 32.64/5.20 | | | | % 32.64/5.20 | | | | COMBINE_EQS: (98), (99) imply: % 32.64/5.20 | | | | (100) all_82_2 = all_76_0 % 32.64/5.20 | | | | % 32.64/5.20 | | | | SIMP: (100) implies: % 32.64/5.20 | | | | (101) all_82_2 = all_76_0 % 32.64/5.20 | | | | % 32.64/5.20 | | | | COMBINE_EQS: (97), (101) imply: % 32.64/5.20 | | | | (102) all_76_0 = all_39_2 % 32.64/5.20 | | | | % 32.64/5.21 | | | | SIMP: (102) implies: % 32.64/5.21 | | | | (103) all_76_0 = all_39_2 % 32.64/5.21 | | | | % 32.64/5.21 | | | | COMBINE_EQS: (95), (96) imply: % 32.64/5.21 | | | | (104) all_65_7 = all_62_0 % 32.64/5.21 | | | | % 32.64/5.21 | | | | SIMP: (104) implies: % 32.64/5.21 | | | | (105) all_65_7 = all_62_0 % 32.64/5.21 | | | | % 32.64/5.21 | | | | COMBINE_EQS: (94), (105) imply: % 32.64/5.21 | | | | (106) all_62_0 = all_34_0 % 32.64/5.21 | | | | % 32.64/5.21 | | | | SIMP: (106) implies: % 32.64/5.21 | | | | (107) all_62_0 = all_34_0 % 32.64/5.21 | | | | % 32.64/5.21 | | | | COMBINE_EQS: (96), (107) imply: % 32.64/5.21 | | | | (108) all_67_0 = all_34_0 % 32.64/5.21 | | | | % 32.64/5.21 | | | | COMBINE_EQS: (99), (103) imply: % 32.64/5.21 | | | | (109) all_82_1 = all_39_2 % 32.64/5.21 | | | | % 32.64/5.21 | | | | REDUCE: (93), (97), (109) imply: % 32.64/5.21 | | | | (110) sdtasasdt0(all_39_2, all_39_2) = all_82_0 % 32.64/5.21 | | | | % 32.64/5.21 | | | | REDUCE: (79), (107) imply: % 32.64/5.21 | | | | (111) ~ iLess0(all_34_0, all_34_0) % 32.64/5.21 | | | | % 32.64/5.21 | | | | BETA: splitting (75) gives: % 32.64/5.21 | | | | % 32.64/5.21 | | | | Case 1: % 32.64/5.21 | | | | | % 32.64/5.21 | | | | | (112) all_65_7 = sz00 % 32.64/5.21 | | | | | % 32.64/5.21 | | | | | COMBINE_EQS: (94), (112) imply: % 32.64/5.21 | | | | | (113) all_34_0 = sz00 % 32.64/5.21 | | | | | % 32.64/5.21 | | | | | REDUCE: (23), (113) imply: % 32.64/5.21 | | | | | (114) $false % 32.64/5.21 | | | | | % 32.64/5.21 | | | | | CLOSE: (114) is inconsistent. % 32.64/5.21 | | | | | % 32.64/5.21 | | | | Case 2: % 32.64/5.21 | | | | | % 32.64/5.21 | | | | | (115) ~ (all_65_7 = sz00) % 32.64/5.21 | | | | | (116) (all_65_0 = all_32_0 & sdtasasdt0(all_65_6, all_65_5) = % 32.64/5.21 | | | | | all_65_4 & sziznziztdt0(xs) = all_65_5 & sziznziztdt0(xs) = % 32.64/5.21 | | | | | all_65_6 & sdtlbdtrb0(xs, all_65_7) = all_65_2 & % 32.64/5.21 | | | | | sdtlbdtrb0(xs, all_65_8) = all_65_3 & aDimensionOf0(xs) = % 32.64/5.21 | | | | | all_65_8 & sdtasdt0(all_65_3, all_65_2) = all_65_1 & % 32.64/5.21 | | | | | sdtpldt0(all_65_4, all_65_1) = all_32_0 & $i(all_65_1) & % 32.64/5.21 | | | | | $i(all_65_2) & $i(all_65_3) & $i(all_65_4) & $i(all_65_5) & % 32.64/5.21 | | | | | $i(all_65_6) & $i(all_65_8) & $i(all_32_0)) | ( ~ (all_65_7 % 32.64/5.21 | | | | | = all_65_8) & aDimensionOf0(xs) = all_65_8 & % 32.64/5.21 | | | | | $i(all_65_8)) % 32.64/5.21 | | | | | % 32.64/5.21 | | | | | BETA: splitting (116) gives: % 32.64/5.21 | | | | | % 32.64/5.21 | | | | | Case 1: % 32.64/5.21 | | | | | | % 32.64/5.21 | | | | | | (117) all_65_0 = all_32_0 & sdtasasdt0(all_65_6, all_65_5) = % 32.64/5.21 | | | | | | all_65_4 & sziznziztdt0(xs) = all_65_5 & sziznziztdt0(xs) = % 32.64/5.21 | | | | | | all_65_6 & sdtlbdtrb0(xs, all_65_7) = all_65_2 & % 32.64/5.21 | | | | | | sdtlbdtrb0(xs, all_65_8) = all_65_3 & aDimensionOf0(xs) = % 32.64/5.21 | | | | | | all_65_8 & sdtasdt0(all_65_3, all_65_2) = all_65_1 & % 32.64/5.21 | | | | | | sdtpldt0(all_65_4, all_65_1) = all_32_0 & $i(all_65_1) & % 32.64/5.21 | | | | | | $i(all_65_2) & $i(all_65_3) & $i(all_65_4) & $i(all_65_5) & % 32.64/5.21 | | | | | | $i(all_65_6) & $i(all_65_8) & $i(all_32_0) % 32.64/5.21 | | | | | | % 32.64/5.21 | | | | | | ALPHA: (117) implies: % 32.64/5.21 | | | | | | (118) $i(all_65_8) % 32.64/5.21 | | | | | | (119) $i(all_65_6) % 32.64/5.21 | | | | | | (120) sdtpldt0(all_65_4, all_65_1) = all_32_0 % 32.64/5.21 | | | | | | (121) sdtasdt0(all_65_3, all_65_2) = all_65_1 % 32.64/5.21 | | | | | | (122) aDimensionOf0(xs) = all_65_8 % 32.64/5.21 | | | | | | (123) sdtlbdtrb0(xs, all_65_8) = all_65_3 % 32.64/5.21 | | | | | | (124) sdtlbdtrb0(xs, all_65_7) = all_65_2 % 32.64/5.21 | | | | | | (125) sziznziztdt0(xs) = all_65_6 % 32.64/5.21 | | | | | | (126) sziznziztdt0(xs) = all_65_5 % 32.64/5.21 | | | | | | (127) sdtasasdt0(all_65_6, all_65_5) = all_65_4 % 32.64/5.21 | | | | | | % 32.64/5.21 | | | | | | REDUCE: (94), (124) imply: % 32.64/5.21 | | | | | | (128) sdtlbdtrb0(xs, all_34_0) = all_65_2 % 32.64/5.21 | | | | | | % 32.64/5.21 | | | | | | BETA: splitting (78) gives: % 32.64/5.21 | | | | | | % 32.64/5.21 | | | | | | Case 1: % 32.64/5.21 | | | | | | | % 32.64/5.21 | | | | | | | (129) all_67_0 = sz00 % 32.64/5.21 | | | | | | | % 32.64/5.21 | | | | | | | COMBINE_EQS: (108), (129) imply: % 32.64/5.21 | | | | | | | (130) all_34_0 = sz00 % 32.64/5.21 | | | | | | | % 32.64/5.21 | | | | | | | REDUCE: (23), (130) imply: % 32.64/5.21 | | | | | | | (131) $false % 32.64/5.21 | | | | | | | % 32.64/5.21 | | | | | | | CLOSE: (131) is inconsistent. % 32.64/5.21 | | | | | | | % 32.64/5.21 | | | | | | Case 2: % 32.64/5.21 | | | | | | | % 32.64/5.21 | | | | | | | (132) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 32.64/5.21 | | | | | | | (sdtlbdtrb0(all_39_2, v1) = v2) | ~ % 32.64/5.21 | | | | | | | (aDimensionOf0(all_39_2) = v0) | ~ $i(v1) | ~ % 32.64/5.21 | | | | | | | $i(all_39_2) | ~ aNaturalNumber0(v1) | (sdtlbdtrb0(xs, % 32.64/5.21 | | | | | | | v1) = v2 & $i(v2))) & ! [v0: $i] : ! [v1: $i] : % 32.64/5.21 | | | | | | | ! [v2: $i] : ( ~ (sdtlbdtrb0(xs, v1) = v2) | ~ % 32.64/5.21 | | | | | | | (aDimensionOf0(all_39_2) = v0) | ~ $i(v1) | ~ % 32.64/5.21 | | | | | | | $i(all_39_2) | ~ aNaturalNumber0(v1) | % 32.64/5.21 | | | | | | | (sdtlbdtrb0(all_39_2, v1) = v2 & $i(v2))) & ! [v0: % 32.64/5.21 | | | | | | | any] : ! [v1: $i] : (v0 = all_39_2 | ~ % 32.64/5.21 | | | | | | | (aDimensionOf0(v0) = v1) | ~ $i(v0) | ~ aVector0(v0) % 32.64/5.21 | | | | | | | | ? [v2: any] : ? [v3: $i] : ? [v4: $i] : ? [v5: % 32.64/5.21 | | | | | | | $i] : ($i(v3) & (( ~ (v5 = v4) & sdtlbdtrb0(v0, v3) = % 32.64/5.21 | | | | | | | v4 & sdtlbdtrb0(xs, v3) = v5 & $i(v5) & $i(v4) & % 32.64/5.21 | | | | | | | aNaturalNumber0(v3)) | ( ~ (v2 = all_67_0) & % 32.64/5.21 | | | | | | | szszuzczcdt0(v1) = v2 & $i(v2))))) & ! [v0: $i] % 32.64/5.21 | | | | | | | : ( ~ (aDimensionOf0(all_39_2) = v0) | ~ $i(all_39_2) | % 32.64/5.21 | | | | | | | szszuzczcdt0(v0) = all_67_0) & ! [v0: $i] : ( ~ % 32.64/5.21 | | | | | | | (aDimensionOf0(all_39_2) = v0) | ~ $i(all_39_2) | % 32.64/5.21 | | | | | | | aVector0(all_39_2)) % 32.64/5.21 | | | | | | | % 32.64/5.21 | | | | | | | ALPHA: (132) implies: % 32.64/5.21 | | | | | | | (133) ! [v0: $i] : ( ~ (aDimensionOf0(all_39_2) = v0) | ~ % 32.64/5.21 | | | | | | | $i(all_39_2) | szszuzczcdt0(v0) = all_67_0) % 32.64/5.21 | | | | | | | (134) ! [v0: any] : ! [v1: $i] : (v0 = all_39_2 | ~ % 32.64/5.21 | | | | | | | (aDimensionOf0(v0) = v1) | ~ $i(v0) | ~ aVector0(v0) % 32.64/5.21 | | | | | | | | ? [v2: any] : ? [v3: $i] : ? [v4: $i] : ? [v5: % 32.64/5.21 | | | | | | | $i] : ($i(v3) & (( ~ (v5 = v4) & sdtlbdtrb0(v0, v3) = % 32.64/5.21 | | | | | | | v4 & sdtlbdtrb0(xs, v3) = v5 & $i(v5) & $i(v4) & % 32.64/5.21 | | | | | | | aNaturalNumber0(v3)) | ( ~ (v2 = all_67_0) & % 32.64/5.21 | | | | | | | szszuzczcdt0(v1) = v2 & $i(v2))))) % 32.64/5.21 | | | | | | | % 32.64/5.21 | | | | | | | GROUND_INST: instantiating (134) with xs, all_34_0, simplifying % 32.64/5.21 | | | | | | | with (7), (12), (24) gives: % 32.64/5.21 | | | | | | | (135) all_39_2 = xs | ? [v0: any] : ? [v1: $i] : ? [v2: $i] % 32.64/5.21 | | | | | | | : ? [v3: $i] : ($i(v1) & (( ~ (v3 = v2) & sdtlbdtrb0(xs, % 32.64/5.21 | | | | | | | v1) = v3 & sdtlbdtrb0(xs, v1) = v2 & $i(v3) & % 32.64/5.21 | | | | | | | $i(v2) & aNaturalNumber0(v1)) | ( ~ (v0 = all_67_0) % 32.64/5.21 | | | | | | | & szszuzczcdt0(all_34_0) = v0 & $i(v0)))) % 32.64/5.21 | | | | | | | % 32.64/5.21 | | | | | | | GROUND_INST: instantiating (133) with all_34_0, simplifying with % 32.64/5.21 | | | | | | | (56) gives: % 32.64/5.21 | | | | | | | (136) ~ (aDimensionOf0(all_39_2) = all_34_0) | % 32.64/5.21 | | | | | | | szszuzczcdt0(all_34_0) = all_67_0 % 32.64/5.21 | | | | | | | % 32.64/5.21 | | | | | | | GROUND_INST: instantiating (14) with all_34_0, all_65_8, xs, % 32.64/5.21 | | | | | | | simplifying with (24), (122) gives: % 32.64/5.21 | | | | | | | (137) all_65_8 = all_34_0 % 32.64/5.21 | | | | | | | % 32.64/5.22 | | | | | | | GROUND_INST: instantiating (17) with all_42_1, all_65_2, all_34_0, % 32.64/5.22 | | | | | | | xs, simplifying with (53), (128) gives: % 32.64/5.22 | | | | | | | (138) all_65_2 = all_42_1 % 32.64/5.22 | | | | | | | % 32.64/5.22 | | | | | | | GROUND_INST: instantiating (17) with all_65_2, all_65_3, all_34_0, % 32.64/5.22 | | | | | | | xs, simplifying with (128) gives: % 32.64/5.22 | | | | | | | (139) all_65_2 = all_65_3 | ~ (sdtlbdtrb0(xs, all_34_0) = % 32.64/5.22 | | | | | | | all_65_3) % 32.64/5.22 | | | | | | | % 32.64/5.22 | | | | | | | GROUND_INST: instantiating (15) with all_39_2, all_65_5, xs, % 32.64/5.22 | | | | | | | simplifying with (31), (126) gives: % 32.64/5.22 | | | | | | | (140) all_65_5 = all_39_2 % 32.64/5.22 | | | | | | | % 32.64/5.22 | | | | | | | GROUND_INST: instantiating (15) with all_65_6, all_65_5, xs, % 32.64/5.22 | | | | | | | simplifying with (125), (126) gives: % 32.64/5.22 | | | | | | | (141) all_65_5 = all_65_6 % 32.64/5.22 | | | | | | | % 32.64/5.22 | | | | | | | COMBINE_EQS: (140), (141) imply: % 32.64/5.22 | | | | | | | (142) all_65_6 = all_39_2 % 32.64/5.22 | | | | | | | % 32.64/5.22 | | | | | | | SIMP: (142) implies: % 32.64/5.22 | | | | | | | (143) all_65_6 = all_39_2 % 32.64/5.22 | | | | | | | % 32.64/5.22 | | | | | | | REDUCE: (127), (140), (143) imply: % 32.64/5.22 | | | | | | | (144) sdtasasdt0(all_39_2, all_39_2) = all_65_4 % 32.64/5.22 | | | | | | | % 32.64/5.22 | | | | | | | REDUCE: (123), (137) imply: % 32.64/5.22 | | | | | | | (145) sdtlbdtrb0(xs, all_34_0) = all_65_3 % 32.64/5.22 | | | | | | | % 32.64/5.22 | | | | | | | REDUCE: (121), (138) imply: % 32.64/5.22 | | | | | | | (146) sdtasdt0(all_65_3, all_42_1) = all_65_1 % 32.64/5.22 | | | | | | | % 32.64/5.22 | | | | | | | REDUCE: (118), (137) imply: % 32.64/5.22 | | | | | | | (147) $i(all_34_0) % 32.64/5.22 | | | | | | | % 32.64/5.22 | | | | | | | BETA: splitting (139) gives: % 32.64/5.22 | | | | | | | % 32.64/5.22 | | | | | | | Case 1: % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | (148) ~ (sdtlbdtrb0(xs, all_34_0) = all_65_3) % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | PRED_UNIFY: (145), (148) imply: % 32.64/5.22 | | | | | | | | (149) $false % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | CLOSE: (149) is inconsistent. % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | Case 2: % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | (150) all_65_2 = all_65_3 % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | COMBINE_EQS: (138), (150) imply: % 32.64/5.22 | | | | | | | | (151) all_65_3 = all_42_1 % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | REDUCE: (146), (151) imply: % 32.64/5.22 | | | | | | | | (152) sdtasdt0(all_42_1, all_42_1) = all_65_1 % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | GROUND_INST: instantiating (16) with all_42_0, all_65_1, % 32.64/5.22 | | | | | | | | all_42_1, all_42_1, simplifying with (39), (152) % 32.64/5.22 | | | | | | | | gives: % 32.64/5.22 | | | | | | | | (153) all_65_1 = all_42_0 % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | GROUND_INST: instantiating (18) with all_82_0, all_65_4, % 32.64/5.22 | | | | | | | | all_39_2, all_39_2, simplifying with (110), (144) % 32.64/5.22 | | | | | | | | gives: % 32.64/5.22 | | | | | | | | (154) all_82_0 = all_65_4 % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | REDUCE: (120), (153) imply: % 32.64/5.22 | | | | | | | | (155) sdtpldt0(all_65_4, all_42_0) = all_32_0 % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | REDUCE: (90), (154) imply: % 32.64/5.22 | | | | | | | | (156) $i(all_65_4) % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | GROUND_INST: instantiating (mIH) with all_34_0, all_34_0, % 32.64/5.22 | | | | | | | | simplifying with (64), (111), (147) gives: % 32.64/5.22 | | | | | | | | (157) ~ (szszuzczcdt0(all_34_0) = all_34_0) % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | GROUND_INST: instantiating (mElmSc) with xs, all_34_0, all_42_1, % 32.64/5.22 | | | | | | | | simplifying with (7), (12), (53), (64), (147) % 32.64/5.22 | | | | | | | | gives: % 32.64/5.22 | | | | | | | | (158) aScalar0(all_42_1) % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | GROUND_INST: instantiating (32) with all_34_0, all_42_1, % 32.64/5.22 | | | | | | | | simplifying with (53), (64), (147) gives: % 32.64/5.22 | | | | | | | | (159) sdtlbdtrb0(all_39_2, all_34_0) = all_42_1 & % 32.64/5.22 | | | | | | | | $i(all_42_1) % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | ALPHA: (159) implies: % 32.64/5.22 | | | | | | | | (160) $i(all_42_1) % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | GROUND_INST: instantiating (mIH) with all_39_1, all_34_0, % 32.64/5.22 | | | | | | | | simplifying with (61), (62), (65) gives: % 32.64/5.22 | | | | | | | | (161) iLess0(all_39_1, all_34_0) % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | GROUND_INST: instantiating (mScPr) with all_39_2, all_39_2, % 32.64/5.22 | | | | | | | | all_65_4, simplifying with (56), (57), (144) gives: % 32.64/5.22 | | | | | | | | (162) aScalar0(all_65_4) | ? [v0: $i] : ? [v1: $i] : ( ~ % 32.64/5.22 | | | | | | | | (v1 = v0) & aDimensionOf0(all_39_2) = v1 & % 32.64/5.22 | | | | | | | | aDimensionOf0(all_39_2) = v0 & $i(v1) & $i(v0)) % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | GROUND_INST: instantiating (5) with all_39_2, all_39_2, % 32.64/5.22 | | | | | | | | all_65_4, simplifying with (56), (57), (144) gives: % 32.64/5.22 | | | | | | | | (163) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 32.64/5.22 | | | | | | | | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : % 32.64/5.22 | | | | | | | | ? [v8: int] : (aDimensionOf0(all_39_2) = v1 & $i(v1) & % 32.64/5.22 | | | | | | | | (v1 = sz00 | (v8 = all_65_4 & sdtasasdt0(v2, v3) = v4 % 32.64/5.22 | | | | | | | | & sziznziztdt0(all_39_2) = v3 & % 32.64/5.22 | | | | | | | | sziznziztdt0(all_39_2) = v2 & % 32.64/5.22 | | | | | | | | sdtlbdtrb0(all_39_2, v1) = v6 & % 32.64/5.22 | | | | | | | | sdtlbdtrb0(all_39_2, v0) = v5 & % 32.64/5.22 | | | | | | | | aDimensionOf0(all_39_2) = v0 & sdtasdt0(v5, v6) = % 32.64/5.22 | | | | | | | | v7 & sdtpldt0(v4, v7) = all_65_4 & $i(v7) & % 32.64/5.22 | | | | | | | | $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & % 32.64/5.22 | | | | | | | | $i(v0) & $i(all_65_4)) | ( ~ (v1 = v0) & % 32.64/5.22 | | | | | | | | aDimensionOf0(all_39_2) = v0 & $i(v0)))) % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | GROUND_INST: instantiating (27) with all_39_2, all_65_4, % 32.64/5.22 | | | | | | | | simplifying with (56), (57), (144) gives: % 32.64/5.22 | | | | | | | | (164) sdtlseqdt0(sz0z00, all_65_4) | ? [v0: $i] : % 32.64/5.22 | | | | | | | | (aDimensionOf0(all_39_2) = v0 & $i(v0) & ~ iLess0(v0, % 32.64/5.22 | | | | | | | | all_36_0)) % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | DELTA: instantiating (163) with fresh symbols all_119_0, % 32.64/5.22 | | | | | | | | all_119_1, all_119_2, all_119_3, all_119_4, all_119_5, % 32.64/5.22 | | | | | | | | all_119_6, all_119_7, all_119_8 gives: % 32.64/5.22 | | | | | | | | (165) aDimensionOf0(all_39_2) = all_119_7 & $i(all_119_7) & % 32.64/5.22 | | | | | | | | (all_119_7 = sz00 | (all_119_0 = all_65_4 & % 32.64/5.22 | | | | | | | | sdtasasdt0(all_119_6, all_119_5) = all_119_4 & % 32.64/5.22 | | | | | | | | sziznziztdt0(all_39_2) = all_119_5 & % 32.64/5.22 | | | | | | | | sziznziztdt0(all_39_2) = all_119_6 & % 32.64/5.22 | | | | | | | | sdtlbdtrb0(all_39_2, all_119_7) = all_119_2 & % 32.64/5.22 | | | | | | | | sdtlbdtrb0(all_39_2, all_119_8) = all_119_3 & % 32.64/5.22 | | | | | | | | aDimensionOf0(all_39_2) = all_119_8 & % 32.64/5.22 | | | | | | | | sdtasdt0(all_119_3, all_119_2) = all_119_1 & % 32.64/5.22 | | | | | | | | sdtpldt0(all_119_4, all_119_1) = all_65_4 & % 32.64/5.22 | | | | | | | | $i(all_119_1) & $i(all_119_2) & $i(all_119_3) & % 32.64/5.22 | | | | | | | | $i(all_119_4) & $i(all_119_5) & $i(all_119_6) & % 32.64/5.22 | | | | | | | | $i(all_119_8) & $i(all_65_4)) | ( ~ (all_119_7 = % 32.64/5.22 | | | | | | | | all_119_8) & aDimensionOf0(all_39_2) = all_119_8 % 32.64/5.22 | | | | | | | | & $i(all_119_8))) % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | ALPHA: (165) implies: % 32.64/5.22 | | | | | | | | (166) aDimensionOf0(all_39_2) = all_119_7 % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | BETA: splitting (136) gives: % 32.64/5.22 | | | | | | | | % 32.64/5.22 | | | | | | | | Case 1: % 32.64/5.22 | | | | | | | | | % 32.64/5.22 | | | | | | | | | (167) ~ (aDimensionOf0(all_39_2) = all_34_0) % 32.64/5.22 | | | | | | | | | % 32.64/5.22 | | | | | | | | | BETA: splitting (162) gives: % 32.64/5.22 | | | | | | | | | % 32.64/5.22 | | | | | | | | | Case 1: % 32.64/5.22 | | | | | | | | | | % 32.64/5.22 | | | | | | | | | | (168) aScalar0(all_65_4) % 32.64/5.22 | | | | | | | | | | % 32.64/5.22 | | | | | | | | | | GROUND_INST: instantiating (14) with all_39_1, all_119_7, % 32.64/5.22 | | | | | | | | | | all_39_2, simplifying with (30), (166) gives: % 32.64/5.22 | | | | | | | | | | (169) all_119_7 = all_39_1 % 32.64/5.22 | | | | | | | | | | % 32.64/5.22 | | | | | | | | | | PRED_UNIFY: (24), (167) imply: % 32.64/5.22 | | | | | | | | | | (170) ~ (all_39_2 = xs) % 32.64/5.22 | | | | | | | | | | % 32.64/5.22 | | | | | | | | | | BETA: splitting (164) gives: % 32.64/5.22 | | | | | | | | | | % 32.64/5.22 | | | | | | | | | | Case 1: % 32.64/5.22 | | | | | | | | | | | % 32.64/5.22 | | | | | | | | | | | (171) sdtlseqdt0(sz0z00, all_65_4) % 32.64/5.22 | | | | | | | | | | | % 32.64/5.22 | | | | | | | | | | | BETA: splitting (135) gives: % 32.64/5.22 | | | | | | | | | | | % 32.64/5.22 | | | | | | | | | | | Case 1: % 32.64/5.22 | | | | | | | | | | | | % 32.64/5.22 | | | | | | | | | | | | (172) all_39_2 = xs % 32.64/5.22 | | | | | | | | | | | | % 32.64/5.22 | | | | | | | | | | | | REDUCE: (170), (172) imply: % 32.64/5.22 | | | | | | | | | | | | (173) $false % 32.64/5.22 | | | | | | | | | | | | % 32.64/5.22 | | | | | | | | | | | | CLOSE: (173) is inconsistent. % 32.64/5.22 | | | | | | | | | | | | % 32.64/5.22 | | | | | | | | | | | Case 2: % 32.64/5.22 | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | (174) ? [v0: any] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 32.64/5.23 | | | | | | | | | | | | $i] : ($i(v1) & (( ~ (v3 = v2) & sdtlbdtrb0(xs, % 32.64/5.23 | | | | | | | | | | | | v1) = v3 & sdtlbdtrb0(xs, v1) = v2 & % 32.64/5.23 | | | | | | | | | | | | $i(v3) & $i(v2) & aNaturalNumber0(v1)) | ( ~ % 32.64/5.23 | | | | | | | | | | | | (v0 = all_67_0) & szszuzczcdt0(all_34_0) = % 32.64/5.23 | | | | | | | | | | | | v0 & $i(v0)))) % 32.64/5.23 | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | DELTA: instantiating (174) with fresh symbols all_159_0, % 32.64/5.23 | | | | | | | | | | | | all_159_1, all_159_2, all_159_3 gives: % 32.64/5.23 | | | | | | | | | | | | (175) $i(all_159_2) & (( ~ (all_159_0 = all_159_1) & % 32.64/5.23 | | | | | | | | | | | | sdtlbdtrb0(xs, all_159_2) = all_159_0 & % 32.64/5.23 | | | | | | | | | | | | sdtlbdtrb0(xs, all_159_2) = all_159_1 & % 32.64/5.23 | | | | | | | | | | | | $i(all_159_0) & $i(all_159_1) & % 32.64/5.23 | | | | | | | | | | | | aNaturalNumber0(all_159_2)) | ( ~ (all_159_3 = % 32.64/5.23 | | | | | | | | | | | | all_67_0) & szszuzczcdt0(all_34_0) = % 32.64/5.23 | | | | | | | | | | | | all_159_3 & $i(all_159_3))) % 32.64/5.23 | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | ALPHA: (175) implies: % 32.64/5.23 | | | | | | | | | | | | (176) ( ~ (all_159_0 = all_159_1) & sdtlbdtrb0(xs, % 32.64/5.23 | | | | | | | | | | | | all_159_2) = all_159_0 & sdtlbdtrb0(xs, % 32.64/5.23 | | | | | | | | | | | | all_159_2) = all_159_1 & $i(all_159_0) & % 32.64/5.23 | | | | | | | | | | | | $i(all_159_1) & aNaturalNumber0(all_159_2)) | ( % 32.64/5.23 | | | | | | | | | | | | ~ (all_159_3 = all_67_0) & % 32.64/5.23 | | | | | | | | | | | | szszuzczcdt0(all_34_0) = all_159_3 & % 32.64/5.23 | | | | | | | | | | | | $i(all_159_3)) % 32.64/5.23 | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | BETA: splitting (176) gives: % 32.64/5.23 | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | Case 1: % 32.64/5.23 | | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | | (177) ~ (all_159_0 = all_159_1) & sdtlbdtrb0(xs, % 32.64/5.23 | | | | | | | | | | | | | all_159_2) = all_159_0 & sdtlbdtrb0(xs, % 32.64/5.23 | | | | | | | | | | | | | all_159_2) = all_159_1 & $i(all_159_0) & % 32.64/5.23 | | | | | | | | | | | | | $i(all_159_1) & aNaturalNumber0(all_159_2) % 32.64/5.23 | | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | | ALPHA: (177) implies: % 32.64/5.23 | | | | | | | | | | | | | (178) ~ (all_159_0 = all_159_1) % 32.64/5.23 | | | | | | | | | | | | | (179) sdtlbdtrb0(xs, all_159_2) = all_159_1 % 32.64/5.23 | | | | | | | | | | | | | (180) sdtlbdtrb0(xs, all_159_2) = all_159_0 % 32.64/5.23 | | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | | GROUND_INST: instantiating (17) with all_159_1, all_159_0, % 32.64/5.23 | | | | | | | | | | | | | all_159_2, xs, simplifying with (179), (180) % 32.64/5.23 | | | | | | | | | | | | | gives: % 32.64/5.23 | | | | | | | | | | | | | (181) all_159_0 = all_159_1 % 32.64/5.23 | | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | | REDUCE: (178), (181) imply: % 32.64/5.23 | | | | | | | | | | | | | (182) $false % 32.64/5.23 | | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | | CLOSE: (182) is inconsistent. % 32.64/5.23 | | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | Case 2: % 32.64/5.23 | | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | | GROUND_INST: instantiating (mMulSc) with all_42_1, all_42_1, % 32.64/5.23 | | | | | | | | | | | | | all_42_0, simplifying with (39), (158), (160) % 32.64/5.23 | | | | | | | | | | | | | gives: % 32.64/5.23 | | | | | | | | | | | | | (183) aScalar0(all_42_0) % 32.64/5.23 | | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | | GROUND_INST: instantiating (1) with all_42_1, all_42_1, % 32.64/5.23 | | | | | | | | | | | | | all_42_0, simplifying with (39), (158), (160) % 32.64/5.23 | | | | | | | | | | | | | gives: % 32.64/5.23 | | | | | | | | | | | | | (184) ? [v0: $i] : ? [v1: $i] : (smndt0(all_42_1) = v1 % 32.64/5.23 | | | | | | | | | | | | | & smndt0(all_42_1) = v0 & sdtasdt0(v0, v1) = % 32.64/5.23 | | | | | | | | | | | | | all_42_0 & $i(v1) & $i(v0) & $i(all_42_0)) % 32.64/5.23 | | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | | DELTA: instantiating (184) with fresh symbols all_179_0, % 32.64/5.23 | | | | | | | | | | | | | all_179_1 gives: % 32.64/5.23 | | | | | | | | | | | | | (185) smndt0(all_42_1) = all_179_0 & smndt0(all_42_1) = % 32.64/5.23 | | | | | | | | | | | | | all_179_1 & sdtasdt0(all_179_1, all_179_0) = % 32.64/5.23 | | | | | | | | | | | | | all_42_0 & $i(all_179_0) & $i(all_179_1) & % 32.64/5.23 | | | | | | | | | | | | | $i(all_42_0) % 32.64/5.23 | | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | | ALPHA: (185) implies: % 32.64/5.23 | | | | | | | | | | | | | (186) $i(all_42_0) % 32.64/5.23 | | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | | GROUND_INST: instantiating (2) with all_65_4, all_42_0, % 32.64/5.23 | | | | | | | | | | | | | all_32_0, simplifying with (20), (34), (155), % 32.64/5.23 | | | | | | | | | | | | | (156), (168), (171), (183), (186) gives: % 32.64/5.23 | | | | | | | | | | | | | (187) $false % 32.64/5.23 | | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | | CLOSE: (187) is inconsistent. % 32.64/5.23 | | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | | End of split % 32.64/5.23 | | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | End of split % 32.64/5.23 | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | Case 2: % 32.64/5.23 | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | (188) ? [v0: $i] : (aDimensionOf0(all_39_2) = v0 & % 32.64/5.23 | | | | | | | | | | | $i(v0) & ~ iLess0(v0, all_36_0)) % 32.64/5.23 | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | DELTA: instantiating (188) with fresh symbol all_150_0 % 32.64/5.23 | | | | | | | | | | | gives: % 32.64/5.23 | | | | | | | | | | | (189) aDimensionOf0(all_39_2) = all_150_0 & % 32.64/5.23 | | | | | | | | | | | $i(all_150_0) & ~ iLess0(all_150_0, all_36_0) % 32.64/5.23 | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | ALPHA: (189) implies: % 32.64/5.23 | | | | | | | | | | | (190) ~ iLess0(all_150_0, all_36_0) % 32.64/5.23 | | | | | | | | | | | (191) aDimensionOf0(all_39_2) = all_150_0 % 32.64/5.23 | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | REDUCE: (52), (190) imply: % 32.64/5.23 | | | | | | | | | | | (192) ~ iLess0(all_150_0, all_34_0) % 32.64/5.23 | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | GROUND_INST: instantiating (14) with all_39_1, all_150_0, % 32.64/5.23 | | | | | | | | | | | all_39_2, simplifying with (30), (191) gives: % 32.64/5.23 | | | | | | | | | | | (193) all_150_0 = all_39_1 % 32.64/5.23 | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | PRED_UNIFY: (161), (192) imply: % 32.64/5.23 | | | | | | | | | | | (194) ~ (all_150_0 = all_39_1) % 32.64/5.23 | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | REDUCE: (193), (194) imply: % 32.64/5.23 | | | | | | | | | | | (195) $false % 32.64/5.23 | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | | CLOSE: (195) is inconsistent. % 32.64/5.23 | | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | End of split % 32.64/5.23 | | | | | | | | | | % 32.64/5.23 | | | | | | | | | Case 2: % 32.64/5.23 | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | (196) ? [v0: $i] : ? [v1: $i] : ( ~ (v1 = v0) & % 32.64/5.23 | | | | | | | | | | aDimensionOf0(all_39_2) = v1 & % 32.64/5.23 | | | | | | | | | | aDimensionOf0(all_39_2) = v0 & $i(v1) & $i(v0)) % 32.64/5.23 | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | DELTA: instantiating (196) with fresh symbols all_142_0, % 32.64/5.23 | | | | | | | | | | all_142_1 gives: % 32.64/5.23 | | | | | | | | | | (197) ~ (all_142_0 = all_142_1) & % 32.64/5.23 | | | | | | | | | | aDimensionOf0(all_39_2) = all_142_0 & % 32.64/5.23 | | | | | | | | | | aDimensionOf0(all_39_2) = all_142_1 & $i(all_142_0) % 32.64/5.23 | | | | | | | | | | & $i(all_142_1) % 32.64/5.23 | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | ALPHA: (197) implies: % 32.64/5.23 | | | | | | | | | | (198) ~ (all_142_0 = all_142_1) % 32.64/5.23 | | | | | | | | | | (199) aDimensionOf0(all_39_2) = all_142_1 % 32.64/5.23 | | | | | | | | | | (200) aDimensionOf0(all_39_2) = all_142_0 % 32.64/5.23 | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | GROUND_INST: instantiating (14) with all_39_1, all_142_1, % 32.64/5.23 | | | | | | | | | | all_39_2, simplifying with (30), (199) gives: % 32.64/5.23 | | | | | | | | | | (201) all_142_1 = all_39_1 % 32.64/5.23 | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | GROUND_INST: instantiating (14) with all_142_1, all_142_0, % 32.64/5.23 | | | | | | | | | | all_39_2, simplifying with (199), (200) gives: % 32.64/5.23 | | | | | | | | | | (202) all_142_0 = all_142_1 % 32.64/5.23 | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | GROUND_INST: instantiating (14) with all_119_7, all_142_0, % 32.64/5.23 | | | | | | | | | | all_39_2, simplifying with (166), (200) gives: % 32.64/5.23 | | | | | | | | | | (203) all_142_0 = all_119_7 % 32.64/5.23 | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | COMBINE_EQS: (202), (203) imply: % 32.64/5.23 | | | | | | | | | | (204) all_142_1 = all_119_7 % 32.64/5.23 | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | SIMP: (204) implies: % 32.64/5.23 | | | | | | | | | | (205) all_142_1 = all_119_7 % 32.64/5.23 | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | COMBINE_EQS: (201), (205) imply: % 32.64/5.23 | | | | | | | | | | (206) all_119_7 = all_39_1 % 32.64/5.23 | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | SIMP: (206) implies: % 32.64/5.23 | | | | | | | | | | (207) all_119_7 = all_39_1 % 32.64/5.23 | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | COMBINE_EQS: (203), (207) imply: % 32.64/5.23 | | | | | | | | | | (208) all_142_0 = all_39_1 % 32.64/5.23 | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | REDUCE: (198), (201), (208) imply: % 32.64/5.23 | | | | | | | | | | (209) $false % 32.64/5.23 | | | | | | | | | | % 32.64/5.23 | | | | | | | | | | CLOSE: (209) is inconsistent. % 32.64/5.23 | | | | | | | | | | % 32.64/5.23 | | | | | | | | | End of split % 32.64/5.23 | | | | | | | | | % 32.64/5.23 | | | | | | | | Case 2: % 32.64/5.23 | | | | | | | | | % 32.64/5.23 | | | | | | | | | (210) szszuzczcdt0(all_34_0) = all_67_0 % 32.64/5.23 | | | | | | | | | % 32.64/5.23 | | | | | | | | | REDUCE: (108), (210) imply: % 32.64/5.23 | | | | | | | | | (211) szszuzczcdt0(all_34_0) = all_34_0 % 32.64/5.23 | | | | | | | | | % 32.64/5.23 | | | | | | | | | PRED_UNIFY: (157), (211) imply: % 32.64/5.23 | | | | | | | | | (212) $false % 32.64/5.23 | | | | | | | | | % 32.64/5.23 | | | | | | | | | CLOSE: (212) is inconsistent. % 32.64/5.23 | | | | | | | | | % 32.64/5.23 | | | | | | | | End of split % 32.64/5.23 | | | | | | | | % 32.64/5.23 | | | | | | | End of split % 32.64/5.23 | | | | | | | % 32.64/5.23 | | | | | | End of split % 32.64/5.23 | | | | | | % 32.64/5.23 | | | | | Case 2: % 32.64/5.23 | | | | | | % 32.64/5.23 | | | | | | (213) ~ (all_65_7 = all_65_8) & aDimensionOf0(xs) = all_65_8 & % 32.64/5.23 | | | | | | $i(all_65_8) % 32.64/5.23 | | | | | | % 32.64/5.23 | | | | | | ALPHA: (213) implies: % 32.64/5.24 | | | | | | (214) ~ (all_65_7 = all_65_8) % 32.64/5.24 | | | | | | (215) aDimensionOf0(xs) = all_65_8 % 32.64/5.24 | | | | | | % 32.64/5.24 | | | | | | REDUCE: (94), (214) imply: % 32.64/5.24 | | | | | | (216) ~ (all_65_8 = all_34_0) % 32.64/5.24 | | | | | | % 32.64/5.24 | | | | | | SIMP: (216) implies: % 32.64/5.24 | | | | | | (217) ~ (all_65_8 = all_34_0) % 32.64/5.24 | | | | | | % 32.64/5.24 | | | | | | GROUND_INST: instantiating (14) with all_34_0, all_65_8, xs, % 32.64/5.24 | | | | | | simplifying with (24), (215) gives: % 32.64/5.24 | | | | | | (218) all_65_8 = all_34_0 % 32.64/5.24 | | | | | | % 32.64/5.24 | | | | | | REDUCE: (217), (218) imply: % 32.64/5.24 | | | | | | (219) $false % 32.64/5.24 | | | | | | % 32.64/5.24 | | | | | | CLOSE: (219) is inconsistent. % 32.64/5.24 | | | | | | % 32.64/5.24 | | | | | End of split % 32.64/5.24 | | | | | % 32.64/5.24 | | | | End of split % 32.64/5.24 | | | | % 32.64/5.24 | | | End of split % 32.64/5.24 | | | % 32.64/5.24 | | End of split % 32.64/5.24 | | % 32.64/5.24 | End of split % 32.64/5.24 | % 32.64/5.24 End of proof % 32.64/5.24 % SZS output end Proof for theBenchmark % 32.64/5.24 % 32.64/5.24 4625ms %------------------------------------------------------------------------------