%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : NUM461+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 : n024.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 11:47:54 EDT 2023 % Result : Theorem 12.39s 2.35s % Output : Proof 79.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM461+2 : TPTP v8.1.2. Released v4.0.0. % 0.07/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n024.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 : Fri Aug 25 10:06:09 EDT 2023 % 0.13/0.34 % CPUTime : % 0.20/0.62 ________ _____ % 0.20/0.62 ___ __ \_________(_)________________________________ % 0.20/0.62 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.62 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.62 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.62 % 0.20/0.62 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.62 (2023-06-19) % 0.20/0.62 % 0.20/0.62 (c) Philipp Rümmer, 2009-2023 % 0.20/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.62 Amanda Stjerna. % 0.20/0.62 Free software under BSD-3-Clause. % 0.20/0.62 % 0.20/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.62 % 0.20/0.62 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.20/0.63 Running up to 7 provers in parallel. % 0.20/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.91/1.08 Prover 4: Preprocessing ... % 2.91/1.08 Prover 1: Preprocessing ... % 3.23/1.11 Prover 6: Preprocessing ... % 3.23/1.11 Prover 0: Preprocessing ... % 3.23/1.11 Prover 2: Preprocessing ... % 3.23/1.11 Prover 5: Preprocessing ... % 3.23/1.12 Prover 3: Preprocessing ... % 6.50/1.57 Prover 1: Constructing countermodel ... % 6.50/1.60 Prover 3: Constructing countermodel ... % 6.50/1.60 Prover 6: Proving ... % 7.38/1.69 Prover 5: Constructing countermodel ... % 8.75/1.87 Prover 4: Constructing countermodel ... % 8.75/1.88 Prover 2: Proving ... % 8.75/1.99 Prover 0: Proving ... % 11.67/2.35 Prover 3: proved (1709ms) % 11.67/2.35 % 12.39/2.35 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 12.39/2.35 % 12.39/2.36 Prover 5: stopped % 12.39/2.36 Prover 2: stopped % 12.39/2.37 Prover 0: stopped % 12.39/2.37 Prover 6: stopped % 12.39/2.37 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 12.39/2.37 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 12.39/2.37 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 12.39/2.37 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 12.39/2.38 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 12.66/2.43 Prover 7: Preprocessing ... % 13.03/2.44 Prover 8: Preprocessing ... % 13.03/2.44 Prover 10: Preprocessing ... % 13.03/2.44 Prover 11: Preprocessing ... % 13.08/2.45 Prover 13: Preprocessing ... % 13.56/2.52 Prover 10: Constructing countermodel ... % 13.56/2.59 Prover 8: Warning: ignoring some quantifiers % 13.56/2.60 Prover 8: Constructing countermodel ... % 14.15/2.63 Prover 13: Constructing countermodel ... % 14.15/2.65 Prover 7: Constructing countermodel ... % 14.15/2.70 Prover 11: Constructing countermodel ... % 63.10/8.90 Prover 13: stopped % 63.10/8.95 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 63.72/8.97 Prover 16: Preprocessing ... % 64.22/9.09 Prover 16: Constructing countermodel ... % 78.17/10.87 Prover 4: Found proof (size 417) % 78.17/10.87 Prover 4: proved (10234ms) % 78.17/10.87 Prover 7: stopped % 78.17/10.88 Prover 10: stopped % 78.17/10.88 Prover 11: stopped % 78.17/10.88 Prover 8: stopped % 78.17/10.88 Prover 16: stopped % 78.17/10.88 Prover 1: stopped % 78.17/10.88 % 78.17/10.88 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 78.17/10.88 % 78.55/10.96 % SZS output start Proof for theBenchmark % 78.55/10.96 Assumptions after simplification: % 78.55/10.96 --------------------------------- % 78.55/10.96 % 78.55/10.96 (mAddAsso) % 78.55/10.99 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 78.55/10.99 (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) % 78.55/10.99 | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? % 78.55/10.99 [v9: $i] : (sdtpldt0(v1, v2) = v8 & sdtpldt0(v0, v8) = v9 & % 78.55/10.99 aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & aNaturalNumber0(v0) % 78.55/10.99 = v5 & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v9 = % 78.55/10.99 v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 78.55/10.99 $i] : ( ~ (sdtpldt0(v1, v2) = v3) | ~ (sdtpldt0(v0, v3) = v4) | ~ $i(v2) | % 78.55/10.99 ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: % 78.55/10.99 $i] : ? [v9: $i] : (sdtpldt0(v8, v2) = v9 & sdtpldt0(v0, v1) = v8 & % 78.55/10.99 aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & aNaturalNumber0(v0) % 78.55/10.99 = v5 & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v9 = % 78.55/10.99 v4))) % 78.55/10.99 % 78.55/10.99 (mAddCanc) % 78.55/11.01 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v2 = v1 % 78.55/11.01 | ~ (sdtpldt0(v2, v0) = v4) | ~ (sdtpldt0(v1, v0) = v3) | ~ $i(v2) | ~ % 78.55/11.01 $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: % 78.55/11.01 $i] : ? [v9: $i] : (sdtpldt0(v0, v2) = v9 & sdtpldt0(v0, v1) = v8 & % 78.55/11.01 aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & aNaturalNumber0(v0) % 78.55/11.01 = v5 & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ( ~ % 78.55/11.01 (v9 = v8) & ~ (v4 = v3))))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 78.55/11.01 : ! [v3: $i] : ! [v4: $i] : (v2 = v1 | ~ (sdtpldt0(v2, v0) = v4) | ~ % 78.55/11.01 (sdtpldt0(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : % 78.55/11.01 ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? [v9: $i] : (sdtpldt0(v1, v0) % 78.55/11.01 = v9 & sdtpldt0(v0, v2) = v8 & aNaturalNumber0(v2) = v7 & % 78.55/11.01 aNaturalNumber0(v1) = v6 & aNaturalNumber0(v0) = v5 & $i(v9) & $i(v8) & ( % 78.55/11.01 ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ( ~ (v9 = v4) & ~ (v8 = % 78.55/11.01 v3))))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 78.55/11.01 [v4: $i] : (v2 = v1 | ~ (sdtpldt0(v1, v0) = v4) | ~ (sdtpldt0(v0, v2) = v3) % 78.55/11.01 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: % 78.55/11.01 any] : ? [v8: $i] : ? [v9: $i] : (sdtpldt0(v2, v0) = v9 & sdtpldt0(v0, % 78.55/11.01 v1) = v8 & aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & % 78.55/11.01 aNaturalNumber0(v0) = v5 & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | % 78.55/11.01 ~ (v5 = 0) | ( ~ (v9 = v4) & ~ (v8 = v3))))) & ! [v0: $i] : ! [v1: % 78.55/11.01 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v2 = v1 | ~ (sdtpldt0(v0, % 78.55/11.01 v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ % 78.55/11.01 $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? [v9: % 78.55/11.01 $i] : (sdtpldt0(v2, v0) = v9 & sdtpldt0(v1, v0) = v8 & aNaturalNumber0(v2) % 78.55/11.01 = v7 & aNaturalNumber0(v1) = v6 & aNaturalNumber0(v0) = v5 & $i(v9) & % 78.55/11.01 $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ( ~ (v9 = v8) & ~ (v4 % 78.55/11.01 = v3))))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 78.55/11.01 (v2 = v1 | ~ (sdtpldt0(v2, v0) = v3) | ~ (aNaturalNumber0(v1) = 0) | ~ % 78.55/11.01 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: $i] : % 78.55/11.01 ? [v7: $i] : ? [v8: $i] : (sdtpldt0(v1, v0) = v8 & sdtpldt0(v0, v2) = v7 & % 78.55/11.01 sdtpldt0(v0, v1) = v6 & aNaturalNumber0(v2) = v5 & aNaturalNumber0(v0) = % 78.55/11.01 v4 & $i(v8) & $i(v7) & $i(v6) & ( ~ (v5 = 0) | ~ (v4 = 0) | ( ~ (v8 = v3) % 78.55/11.01 & ~ (v7 = v6))))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 78.55/11.01 $i] : (v2 = v1 | ~ (sdtpldt0(v1, v0) = v3) | ~ (aNaturalNumber0(v2) = 0) | % 78.55/11.01 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: % 78.55/11.01 $i] : ? [v7: $i] : ? [v8: $i] : (sdtpldt0(v2, v0) = v8 & sdtpldt0(v0, % 78.55/11.01 v2) = v7 & sdtpldt0(v0, v1) = v6 & aNaturalNumber0(v1) = v5 & % 78.55/11.01 aNaturalNumber0(v0) = v4 & $i(v8) & $i(v7) & $i(v6) & ( ~ (v5 = 0) | ~ % 78.55/11.01 (v4 = 0) | ( ~ (v8 = v3) & ~ (v7 = v6))))) & ! [v0: $i] : ! [v1: $i] % 78.55/11.01 : ! [v2: $i] : ! [v3: $i] : (v2 = v1 | ~ (sdtpldt0(v0, v2) = v3) | ~ % 78.55/11.01 (aNaturalNumber0(v1) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] % 78.55/11.01 : ? [v5: any] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : (sdtpldt0(v2, v0) % 78.55/11.01 = v8 & sdtpldt0(v1, v0) = v7 & sdtpldt0(v0, v1) = v6 & aNaturalNumber0(v2) % 78.55/11.01 = v5 & aNaturalNumber0(v0) = v4 & $i(v8) & $i(v7) & $i(v6) & ( ~ (v5 = 0) % 78.55/11.01 | ~ (v4 = 0) | ( ~ (v8 = v7) & ~ (v6 = v3))))) & ! [v0: $i] : ! [v1: % 78.55/11.01 $i] : ! [v2: $i] : ! [v3: $i] : (v2 = v1 | ~ (sdtpldt0(v0, v1) = v3) | ~ % 78.55/11.01 (aNaturalNumber0(v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] % 78.55/11.01 : ? [v5: any] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : (sdtpldt0(v2, v0) % 78.55/11.01 = v8 & sdtpldt0(v1, v0) = v7 & sdtpldt0(v0, v2) = v6 & aNaturalNumber0(v1) % 78.55/11.01 = v5 & aNaturalNumber0(v0) = v4 & $i(v8) & $i(v7) & $i(v6) & ( ~ (v5 = 0) % 78.55/11.01 | ~ (v4 = 0) | ( ~ (v8 = v7) & ~ (v6 = v3))))) & ! [v0: $i] : ! [v1: % 78.55/11.01 $i] : ! [v2: $i] : (v2 = v1 | ~ (aNaturalNumber0(v2) = 0) | ~ % 78.55/11.01 (aNaturalNumber0(v1) = 0) | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v2) | ~ % 78.55/11.01 $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : % 78.55/11.01 ( ~ (v6 = v5) & ~ (v4 = v3) & sdtpldt0(v2, v0) = v6 & sdtpldt0(v1, v0) = v5 % 78.55/11.01 & sdtpldt0(v0, v2) = v4 & sdtpldt0(v0, v1) = v3 & $i(v6) & $i(v5) & $i(v4) % 78.55/11.01 & $i(v3))) % 78.55/11.01 % 78.55/11.01 (mAddComm) % 78.55/11.01 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ % 78.55/11.01 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 78.55/11.01 (sdtpldt0(v0, v1) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 % 78.55/11.01 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) & ! [v0: $i] : ! [v1: % 78.55/11.01 $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? % 78.55/11.01 [v3: any] : ? [v4: any] : ? [v5: $i] : (sdtpldt0(v1, v0) = v5 & % 78.55/11.01 aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 & $i(v5) & ( ~ (v4 = % 78.55/11.01 0) | ~ (v3 = 0) | v5 = v2))) % 78.55/11.01 % 78.55/11.01 (mDefDiff) % 78.55/11.02 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v2 | ~ % 78.55/11.02 (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v3) = v1) | ~ $i(v3) | ~ $i(v1) % 78.55/11.02 | ~ $i(v0) | ? [v4: int] : ? [v5: any] : ? [v6: any] : (( ~ (v4 = 0) & % 78.55/11.02 aNaturalNumber0(v3) = v4) | (sdtlseqdt0(v0, v1) = v6 & % 78.55/11.02 aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v6 = 0) | ~ % 78.55/11.02 (v5 = 0) | ~ (v4 = 0))))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 78.55/11.02 ! [v3: $i] : (v3 = v2 | ~ (sdtmndt0(v1, v0) = v2) | ~ (aNaturalNumber0(v3) % 78.55/11.02 = 0) | ~ $i(v3) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : % 78.55/11.02 ? [v6: any] : (( ~ (v4 = v1) & sdtpldt0(v0, v3) = v4 & $i(v4)) | % 78.55/11.02 (sdtlseqdt0(v0, v1) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) % 78.55/11.02 = v4 & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0))))) & ! [v0: $i] : ! % 78.55/11.02 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v1 | ~ (sdtmndt0(v1, v0) = v2) | % 78.55/11.02 ~ (sdtpldt0(v0, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 78.55/11.02 any] : ? [v5: any] : ? [v6: any] : (sdtlseqdt0(v0, v1) = v6 & % 78.55/11.02 aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v6 = 0) | ~ % 78.55/11.02 (v5 = 0) | ~ (v4 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 78.55/11.02 [v3: int] : (v3 = 0 | ~ (sdtmndt0(v1, v0) = v2) | ~ (aNaturalNumber0(v2) = % 78.55/11.02 v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? % 78.55/11.02 [v6: any] : (sdtlseqdt0(v0, v1) = v6 & aNaturalNumber0(v1) = v5 & % 78.55/11.02 aNaturalNumber0(v0) = v4 & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) & % 78.55/11.02 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (sdtmndt0(v1, v0) = % 78.55/11.02 v2) | ~ (sdtpldt0(v0, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 78.55/11.02 [v4: int] : ? [v5: any] : ? [v6: any] : ((v4 = 0 & aNaturalNumber0(v2) = % 78.55/11.02 0) | (sdtlseqdt0(v0, v1) = v6 & aNaturalNumber0(v1) = v5 & % 78.55/11.02 aNaturalNumber0(v0) = v4 & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0))))) % 78.55/11.02 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: MultipleValueBool] : ( ~ % 78.55/11.02 (sdtmndt0(v1, v0) = v2) | ~ (aNaturalNumber0(v2) = v3) | ~ $i(v2) | ~ % 78.55/11.02 $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: any] : ((v4 = v1 % 78.55/11.02 & sdtpldt0(v0, v2) = v1) | (sdtlseqdt0(v0, v1) = v6 & % 78.55/11.02 aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v6 = 0) | ~ % 78.55/11.02 (v5 = 0) | ~ (v4 = 0))))) & ! [v0: $i] : ! [v1: $i] : ( ~ % 78.55/11.02 (sdtlseqdt0(v0, v1) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: any] : ? [v3: % 78.55/11.02 any] : ? [v4: $i] : (sdtmndt0(v1, v0) = v4 & aNaturalNumber0(v1) = v3 & % 78.55/11.02 aNaturalNumber0(v0) = v2 & $i(v4) & ( ~ (v3 = 0) | ~ (v2 = 0) | ( ! [v5: % 78.55/11.02 $i] : (v5 = v4 | ~ (sdtpldt0(v0, v5) = v1) | ~ $i(v5) | ? [v6: % 78.55/11.02 int] : ( ~ (v6 = 0) & aNaturalNumber0(v5) = v6)) & ! [v5: $i] : % 78.55/11.02 (v5 = v4 | ~ (aNaturalNumber0(v5) = 0) | ~ $i(v5) | ? [v6: $i] : ( % 78.55/11.02 ~ (v6 = v1) & sdtpldt0(v0, v5) = v6 & $i(v6))) & ! [v5: $i] : (v5 % 78.55/11.02 = v1 | ~ (sdtpldt0(v0, v4) = v5)) & ! [v5: int] : (v5 = 0 | ~ % 78.55/11.02 (aNaturalNumber0(v4) = v5)) & ! [v5: $i] : ( ~ (sdtpldt0(v0, v4) = % 78.55/11.02 v5) | aNaturalNumber0(v4) = 0) & ! [v5: MultipleValueBool] : ( ~ % 78.55/11.02 (aNaturalNumber0(v4) = v5) | sdtpldt0(v0, v4) = v1))))) % 78.55/11.02 % 78.55/11.02 (mLETran) % 78.55/11.03 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 78.55/11.03 (sdtlseqdt0(v1, v2) = 0) | ~ (sdtlseqdt0(v0, v2) = v3) | ~ $i(v2) | ~ % 78.55/11.03 $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: % 78.55/11.03 any] : (sdtlseqdt0(v0, v1) = v7 & aNaturalNumber0(v2) = v6 & % 78.55/11.03 aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v7 = 0) | ~ % 78.55/11.03 (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! % 78.55/11.03 [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (sdtlseqdt0(v0, v2) = v3) | ~ % 78.55/11.03 (sdtlseqdt0(v0, v1) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] % 78.55/11.03 : ? [v5: any] : ? [v6: any] : ? [v7: any] : (sdtlseqdt0(v1, v2) = v7 & % 78.55/11.03 aNaturalNumber0(v2) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) % 78.55/11.03 = v4 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) & ! [v0: % 78.55/11.03 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 78.55/11.03 (sdtlseqdt0(v0, v2) = v3) | ~ (aNaturalNumber0(v1) = 0) | ~ $i(v2) | ~ % 78.55/11.03 $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: % 78.55/11.03 any] : (sdtlseqdt0(v1, v2) = v7 & sdtlseqdt0(v0, v1) = v6 & % 78.55/11.03 aNaturalNumber0(v2) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v7 = 0) | ~ % 78.55/11.03 (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! % 78.55/11.03 [v2: $i] : ( ~ (sdtlseqdt0(v1, v2) = 0) | ~ (sdtlseqdt0(v0, v1) = 0) | ~ % 78.55/11.03 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] % 78.55/11.03 : ? [v6: any] : (sdtlseqdt0(v0, v2) = v6 & aNaturalNumber0(v2) = v5 & % 78.55/11.03 aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 & ( ~ (v5 = 0) | ~ % 78.55/11.03 (v4 = 0) | ~ (v3 = 0) | v6 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 78.55/11.03 $i] : ( ~ (sdtlseqdt0(v1, v2) = 0) | ~ (aNaturalNumber0(v0) = 0) | ~ % 78.55/11.03 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] % 78.55/11.03 : ? [v6: any] : (sdtlseqdt0(v0, v2) = v6 & sdtlseqdt0(v0, v1) = v5 & % 78.55/11.03 aNaturalNumber0(v2) = v4 & aNaturalNumber0(v1) = v3 & ( ~ (v5 = 0) | ~ % 78.55/11.03 (v4 = 0) | ~ (v3 = 0) | v6 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 78.55/11.03 $i] : ( ~ (sdtlseqdt0(v0, v1) = 0) | ~ (aNaturalNumber0(v2) = 0) | ~ % 78.55/11.03 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] % 78.55/11.03 : ? [v6: any] : (sdtlseqdt0(v1, v2) = v5 & sdtlseqdt0(v0, v2) = v6 & % 78.55/11.03 aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 & ( ~ (v5 = 0) | ~ % 78.55/11.03 (v4 = 0) | ~ (v3 = 0) | v6 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 78.55/11.03 $i] : ( ~ (aNaturalNumber0(v2) = 0) | ~ (aNaturalNumber0(v1) = 0) | ~ % 78.55/11.03 (aNaturalNumber0(v0) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] % 78.55/11.03 : ? [v4: any] : ? [v5: any] : (sdtlseqdt0(v1, v2) = v4 & sdtlseqdt0(v0, % 78.55/11.03 v2) = v5 & sdtlseqdt0(v0, v1) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = % 78.55/11.03 0))) % 78.55/11.03 % 78.55/11.03 (mSortsB) % 78.55/11.03 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 78.55/11.03 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 78.55/11.03 (aNaturalNumber0(v2) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = % 78.55/11.03 v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 78.55/11.03 % 78.55/11.03 (mSortsC) % 78.55/11.03 aNaturalNumber0(sz00) = 0 & $i(sz00) % 78.55/11.03 % 78.55/11.03 (mSortsC_01) % 78.55/11.03 ~ (sz10 = sz00) & aNaturalNumber0(sz10) = 0 & $i(sz10) & $i(sz00) % 78.55/11.03 % 78.55/11.03 (mZeroMul) % 78.55/11.03 $i(sz00) & ! [v0: $i] : ! [v1: $i] : (v1 = sz00 | v0 = sz00 | ~ % 78.55/11.03 (sdtasdt0(v0, v1) = sz00) | ~ $i(v1) | ~ $i(v0) | ? [v2: any] : ? [v3: % 78.55/11.03 any] : (aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v3 = 0) % 78.55/11.03 | ~ (v2 = 0)))) % 78.55/11.03 % 78.55/11.03 (m_AddZero) % 78.55/11.03 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtpldt0(v0, sz00) = v1) | ~ % 78.55/11.03 $i(v0) | ? [v2: any] : ? [v3: $i] : (sdtpldt0(sz00, v0) = v3 & % 78.55/11.03 aNaturalNumber0(v0) = v2 & $i(v3) & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) % 78.55/11.03 & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtpldt0(sz00, v0) = v1) | ~ $i(v0) | ? % 78.55/11.03 [v2: any] : ? [v3: $i] : (sdtpldt0(v0, sz00) = v3 & aNaturalNumber0(v0) = % 78.55/11.03 v2 & $i(v3) & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) & ! [v0: $i] : ( ~ % 78.55/11.03 (aNaturalNumber0(v0) = 0) | ~ $i(v0) | (sdtpldt0(v0, sz00) = v0 & % 78.55/11.03 sdtpldt0(sz00, v0) = v0)) % 78.55/11.03 % 78.55/11.03 (m_MulUnit) % 78.55/11.03 $i(sz10) & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtasdt0(v0, sz10) = v1) | ~ % 78.55/11.03 $i(v0) | ? [v2: any] : ? [v3: $i] : (sdtasdt0(sz10, v0) = v3 & % 78.55/11.03 aNaturalNumber0(v0) = v2 & $i(v3) & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) % 78.55/11.03 & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtasdt0(sz10, v0) = v1) | ~ $i(v0) | ? % 78.55/11.03 [v2: any] : ? [v3: $i] : (sdtasdt0(v0, sz10) = v3 & aNaturalNumber0(v0) = % 78.55/11.03 v2 & $i(v3) & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) & ! [v0: $i] : ( ~ % 78.55/11.04 (aNaturalNumber0(v0) = 0) | ~ $i(v0) | (sdtasdt0(v0, sz10) = v0 & % 78.55/11.04 sdtasdt0(sz10, v0) = v0)) % 78.55/11.04 % 78.55/11.04 (m__) % 78.55/11.04 $i(xm) & $i(xn) & $i(xl) & ? [v0: $i] : ? [v1: $i] : ? [v2: any] : ? [v3: % 78.55/11.04 $i] : ? [v4: $i] : ? [v5: any] : (sdtlseqdt0(v3, v4) = v5 & sdtlseqdt0(v0, % 78.55/11.04 v1) = v2 & sdtpldt0(xm, xn) = v1 & sdtpldt0(xm, xl) = v0 & sdtpldt0(xn, % 78.55/11.04 xm) = v4 & sdtpldt0(xl, xm) = v3 & $i(v4) & $i(v3) & $i(v1) & $i(v0) & (v4 % 78.55/11.04 = v3 | v1 = v0 | ( ~ (v5 = 0) & ! [v6: $i] : ( ~ (sdtpldt0(v3, v6) = v4) % 78.55/11.04 | ~ $i(v6) | ? [v7: int] : ( ~ (v7 = 0) & aNaturalNumber0(v6) = v7)) % 78.55/11.04 & ! [v6: $i] : ( ~ (aNaturalNumber0(v6) = 0) | ~ $i(v6) | ? [v7: $i] % 78.55/11.04 : ( ~ (v7 = v4) & sdtpldt0(v3, v6) = v7 & $i(v7)))) | ( ~ (v2 = 0) & % 78.55/11.04 ! [v6: $i] : ( ~ (sdtpldt0(v0, v6) = v1) | ~ $i(v6) | ? [v7: int] : ( % 78.55/11.04 ~ (v7 = 0) & aNaturalNumber0(v6) = v7)) & ! [v6: $i] : ( ~ % 78.55/11.04 (aNaturalNumber0(v6) = 0) | ~ $i(v6) | ? [v7: $i] : ( ~ (v7 = v1) & % 78.55/11.04 sdtpldt0(v0, v6) = v7 & $i(v7)))))) % 78.55/11.04 % 78.55/11.04 (m__840) % 78.55/11.04 aNaturalNumber0(xn) = 0 & aNaturalNumber0(xl) = 0 & $i(xn) & $i(xl) % 78.55/11.04 % 78.55/11.04 (m__840_03) % 78.55/11.04 $i(xn) & $i(xl) & ? [v0: $i] : ( ~ (xn = xl) & sdtlseqdt0(xl, xn) = 0 & % 78.55/11.04 sdtpldt0(xl, v0) = xn & aNaturalNumber0(v0) = 0 & $i(v0)) % 78.55/11.04 % 78.55/11.04 (m__873) % 78.55/11.04 aNaturalNumber0(xm) = 0 & $i(xm) % 78.55/11.04 % 78.55/11.04 (function-axioms) % 78.55/11.04 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 78.55/11.04 (sdtmndt0(v3, v2) = v1) | ~ (sdtmndt0(v3, v2) = v0)) & ! [v0: % 78.55/11.04 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 78.55/11.04 : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ (sdtlseqdt0(v3, v2) = v0)) & ! % 78.55/11.04 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 78.55/11.04 (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 78.55/11.04 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | % 78.55/11.04 ~ (sdtpldt0(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 78.55/11.04 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) % 78.55/11.04 | ~ (aNaturalNumber0(v2) = v0)) % 78.55/11.04 % 78.55/11.04 Further assumptions not needed in the proof: % 78.55/11.04 -------------------------------------------- % 78.55/11.04 mAMDistr, mDefLE, mLEAsym, mLERefl, mLETotal, mMulAsso, mMulCanc, mMulComm, % 78.55/11.04 mNatSort, mSortsB_02, mZeroAdd, m_MulZero % 78.55/11.04 % 78.55/11.04 Those formulas are unsatisfiable: % 78.55/11.04 --------------------------------- % 78.55/11.04 % 78.55/11.04 Begin of proof % 78.55/11.04 | % 78.55/11.04 | ALPHA: (mSortsC) implies: % 78.55/11.05 | (1) aNaturalNumber0(sz00) = 0 % 78.55/11.05 | % 78.55/11.05 | ALPHA: (mSortsC_01) implies: % 78.55/11.05 | (2) ~ (sz10 = sz00) % 78.55/11.05 | (3) aNaturalNumber0(sz10) = 0 % 78.55/11.05 | % 78.55/11.05 | ALPHA: (mAddComm) implies: % 78.55/11.05 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | % 78.55/11.05 | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 78.55/11.05 | (sdtpldt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & % 78.55/11.05 | aNaturalNumber0(v0) = v3 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 % 78.55/11.05 | = v2))) % 78.55/11.05 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v1, v0) = v2) | % 78.55/11.05 | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 78.55/11.05 | (sdtpldt0(v0, v1) = v5 & aNaturalNumber0(v1) = v4 & % 78.55/11.05 | aNaturalNumber0(v0) = v3 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 % 78.55/11.05 | = v2))) % 78.55/11.05 | % 78.55/11.05 | ALPHA: (mAddAsso) implies: % 78.55/11.05 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 78.55/11.05 | ~ (sdtpldt0(v1, v2) = v3) | ~ (sdtpldt0(v0, v3) = v4) | ~ $i(v2) | % 78.55/11.05 | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : % 78.55/11.05 | ? [v8: $i] : ? [v9: $i] : (sdtpldt0(v8, v2) = v9 & sdtpldt0(v0, v1) % 78.55/11.05 | = v8 & aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & % 78.55/11.05 | aNaturalNumber0(v0) = v5 & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 % 78.55/11.05 | = 0) | ~ (v5 = 0) | v9 = v4))) % 78.55/11.05 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 78.55/11.05 | ~ (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ $i(v2) | % 78.55/11.05 | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : % 78.55/11.05 | ? [v8: $i] : ? [v9: $i] : (sdtpldt0(v1, v2) = v8 & sdtpldt0(v0, v8) % 78.55/11.05 | = v9 & aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & % 78.55/11.05 | aNaturalNumber0(v0) = v5 & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 % 78.55/11.05 | = 0) | ~ (v5 = 0) | v9 = v4))) % 78.55/11.05 | % 78.55/11.05 | ALPHA: (m_AddZero) implies: % 78.55/11.05 | (8) ! [v0: $i] : ( ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) | (sdtpldt0(v0, % 78.55/11.05 | sz00) = v0 & sdtpldt0(sz00, v0) = v0)) % 78.55/11.05 | % 78.55/11.05 | ALPHA: (m_MulUnit) implies: % 78.55/11.05 | (9) $i(sz10) % 78.55/11.05 | % 78.55/11.05 | ALPHA: (mAddCanc) implies: % 78.55/11.06 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ % 78.55/11.06 | (aNaturalNumber0(v2) = 0) | ~ (aNaturalNumber0(v1) = 0) | ~ % 78.55/11.06 | (aNaturalNumber0(v0) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 78.55/11.06 | [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ( ~ (v6 = v5) & % 78.55/11.06 | ~ (v4 = v3) & sdtpldt0(v2, v0) = v6 & sdtpldt0(v1, v0) = v5 & % 78.55/11.06 | sdtpldt0(v0, v2) = v4 & sdtpldt0(v0, v1) = v3 & $i(v6) & $i(v5) & % 78.55/11.06 | $i(v4) & $i(v3))) % 78.55/11.06 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v2 = v1 | ~ % 78.55/11.06 | (sdtpldt0(v1, v0) = v3) | ~ (aNaturalNumber0(v2) = 0) | ~ $i(v2) | % 78.55/11.06 | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: $i] : % 78.55/11.06 | ? [v7: $i] : ? [v8: $i] : (sdtpldt0(v2, v0) = v8 & sdtpldt0(v0, v2) % 78.55/11.06 | = v7 & sdtpldt0(v0, v1) = v6 & aNaturalNumber0(v1) = v5 & % 78.55/11.06 | aNaturalNumber0(v0) = v4 & $i(v8) & $i(v7) & $i(v6) & ( ~ (v5 = 0) % 78.55/11.06 | | ~ (v4 = 0) | ( ~ (v8 = v3) & ~ (v7 = v6))))) % 78.55/11.06 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v2 = v1 | ~ % 78.55/11.06 | (sdtpldt0(v2, v0) = v3) | ~ (aNaturalNumber0(v1) = 0) | ~ $i(v2) | % 78.55/11.06 | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: $i] : % 78.55/11.06 | ? [v7: $i] : ? [v8: $i] : (sdtpldt0(v1, v0) = v8 & sdtpldt0(v0, v2) % 78.55/11.06 | = v7 & sdtpldt0(v0, v1) = v6 & aNaturalNumber0(v2) = v5 & % 78.55/11.06 | aNaturalNumber0(v0) = v4 & $i(v8) & $i(v7) & $i(v6) & ( ~ (v5 = 0) % 78.55/11.06 | | ~ (v4 = 0) | ( ~ (v8 = v3) & ~ (v7 = v6))))) % 78.55/11.06 | % 78.55/11.06 | ALPHA: (mZeroMul) implies: % 78.55/11.06 | (13) $i(sz00) % 78.55/11.06 | % 78.55/11.06 | ALPHA: (mDefDiff) implies: % 78.55/11.06 | (14) ! [v0: $i] : ! [v1: $i] : ( ~ (sdtlseqdt0(v0, v1) = 0) | ~ $i(v1) | % 78.55/11.06 | ~ $i(v0) | ? [v2: any] : ? [v3: any] : ? [v4: $i] : % 78.55/11.06 | (sdtmndt0(v1, v0) = v4 & aNaturalNumber0(v1) = v3 & % 78.55/11.06 | aNaturalNumber0(v0) = v2 & $i(v4) & ( ~ (v3 = 0) | ~ (v2 = 0) | ( % 78.55/11.06 | ! [v5: $i] : (v5 = v4 | ~ (sdtpldt0(v0, v5) = v1) | ~ $i(v5) % 78.55/11.06 | | ? [v6: int] : ( ~ (v6 = 0) & aNaturalNumber0(v5) = v6)) & % 78.55/11.06 | ! [v5: $i] : (v5 = v4 | ~ (aNaturalNumber0(v5) = 0) | ~ % 78.55/11.06 | $i(v5) | ? [v6: $i] : ( ~ (v6 = v1) & sdtpldt0(v0, v5) = v6 % 78.55/11.06 | & $i(v6))) & ! [v5: $i] : (v5 = v1 | ~ (sdtpldt0(v0, v4) % 78.55/11.06 | = v5)) & ! [v5: int] : (v5 = 0 | ~ (aNaturalNumber0(v4) % 78.55/11.06 | = v5)) & ! [v5: $i] : ( ~ (sdtpldt0(v0, v4) = v5) | % 78.55/11.06 | aNaturalNumber0(v4) = 0) & ! [v5: MultipleValueBool] : ( ~ % 78.55/11.06 | (aNaturalNumber0(v4) = v5) | sdtpldt0(v0, v4) = v1))))) % 78.55/11.06 | % 78.55/11.06 | ALPHA: (mLETran) implies: % 78.55/11.07 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtlseqdt0(v0, v1) = 0) % 78.55/11.07 | | ~ (aNaturalNumber0(v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 78.55/11.07 | ? [v3: any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : % 78.55/11.07 | (sdtlseqdt0(v1, v2) = v5 & sdtlseqdt0(v0, v2) = v6 & % 78.55/11.07 | aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 & ( ~ (v5 = 0) % 78.55/11.07 | | ~ (v4 = 0) | ~ (v3 = 0) | v6 = 0))) % 78.55/11.07 | (16) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtlseqdt0(v1, v2) = 0) % 78.55/11.07 | | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 78.55/11.07 | ? [v3: any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : % 78.55/11.07 | (sdtlseqdt0(v0, v2) = v6 & sdtlseqdt0(v0, v1) = v5 & % 78.55/11.07 | aNaturalNumber0(v2) = v4 & aNaturalNumber0(v1) = v3 & ( ~ (v5 = 0) % 78.55/11.07 | | ~ (v4 = 0) | ~ (v3 = 0) | v6 = 0))) % 78.55/11.07 | % 78.55/11.07 | ALPHA: (m__840) implies: % 78.55/11.07 | (17) aNaturalNumber0(xl) = 0 % 78.55/11.07 | (18) aNaturalNumber0(xn) = 0 % 78.55/11.07 | % 78.55/11.07 | ALPHA: (m__840_03) implies: % 78.55/11.07 | (19) ? [v0: $i] : ( ~ (xn = xl) & sdtlseqdt0(xl, xn) = 0 & sdtpldt0(xl, % 78.55/11.07 | v0) = xn & aNaturalNumber0(v0) = 0 & $i(v0)) % 78.55/11.07 | % 78.55/11.07 | ALPHA: (m__873) implies: % 78.55/11.07 | (20) aNaturalNumber0(xm) = 0 % 78.55/11.07 | % 78.55/11.07 | ALPHA: (m__) implies: % 78.55/11.07 | (21) $i(xl) % 78.55/11.07 | (22) $i(xn) % 78.55/11.07 | (23) $i(xm) % 78.55/11.07 | (24) ? [v0: $i] : ? [v1: $i] : ? [v2: any] : ? [v3: $i] : ? [v4: $i] : % 78.55/11.07 | ? [v5: any] : (sdtlseqdt0(v3, v4) = v5 & sdtlseqdt0(v0, v1) = v2 & % 78.55/11.07 | sdtpldt0(xm, xn) = v1 & sdtpldt0(xm, xl) = v0 & sdtpldt0(xn, xm) = % 78.55/11.07 | v4 & sdtpldt0(xl, xm) = v3 & $i(v4) & $i(v3) & $i(v1) & $i(v0) & (v4 % 78.55/11.07 | = v3 | v1 = v0 | ( ~ (v5 = 0) & ! [v6: $i] : ( ~ (sdtpldt0(v3, % 78.55/11.07 | v6) = v4) | ~ $i(v6) | ? [v7: int] : ( ~ (v7 = 0) & % 78.55/11.07 | aNaturalNumber0(v6) = v7)) & ! [v6: $i] : ( ~ % 78.55/11.07 | (aNaturalNumber0(v6) = 0) | ~ $i(v6) | ? [v7: $i] : ( ~ (v7 % 78.55/11.07 | = v4) & sdtpldt0(v3, v6) = v7 & $i(v7)))) | ( ~ (v2 = 0) & % 78.55/11.07 | ! [v6: $i] : ( ~ (sdtpldt0(v0, v6) = v1) | ~ $i(v6) | ? [v7: % 78.55/11.07 | int] : ( ~ (v7 = 0) & aNaturalNumber0(v6) = v7)) & ! [v6: % 78.55/11.07 | $i] : ( ~ (aNaturalNumber0(v6) = 0) | ~ $i(v6) | ? [v7: $i] % 78.55/11.07 | : ( ~ (v7 = v1) & sdtpldt0(v0, v6) = v7 & $i(v7)))))) % 78.55/11.07 | % 78.55/11.07 | ALPHA: (function-axioms) implies: % 78.55/11.07 | (25) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 78.55/11.07 | : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = % 78.55/11.07 | v0)) % 78.55/11.07 | (26) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 78.55/11.07 | (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 78.55/11.07 | % 78.55/11.07 | DELTA: instantiating (19) with fresh symbol all_24_0 gives: % 78.55/11.07 | (27) ~ (xn = xl) & sdtlseqdt0(xl, xn) = 0 & sdtpldt0(xl, all_24_0) = xn & % 78.55/11.07 | aNaturalNumber0(all_24_0) = 0 & $i(all_24_0) % 78.55/11.07 | % 78.55/11.07 | ALPHA: (27) implies: % 78.55/11.07 | (28) ~ (xn = xl) % 78.55/11.07 | (29) $i(all_24_0) % 78.55/11.07 | (30) aNaturalNumber0(all_24_0) = 0 % 78.55/11.08 | (31) sdtpldt0(xl, all_24_0) = xn % 78.55/11.08 | (32) sdtlseqdt0(xl, xn) = 0 % 78.55/11.08 | % 78.55/11.08 | DELTA: instantiating (24) with fresh symbols all_26_0, all_26_1, all_26_2, % 78.55/11.08 | all_26_3, all_26_4, all_26_5 gives: % 78.55/11.08 | (33) sdtlseqdt0(all_26_2, all_26_1) = all_26_0 & sdtlseqdt0(all_26_5, % 78.55/11.08 | all_26_4) = all_26_3 & sdtpldt0(xm, xn) = all_26_4 & sdtpldt0(xm, % 78.55/11.08 | xl) = all_26_5 & sdtpldt0(xn, xm) = all_26_1 & sdtpldt0(xl, xm) = % 78.55/11.08 | all_26_2 & $i(all_26_1) & $i(all_26_2) & $i(all_26_4) & $i(all_26_5) & % 78.55/11.08 | (all_26_1 = all_26_2 | all_26_4 = all_26_5 | ( ~ (all_26_0 = 0) & ! % 78.55/11.08 | [v0: $i] : ( ~ (sdtpldt0(all_26_2, v0) = all_26_1) | ~ $i(v0) | % 78.55/11.08 | ? [v1: int] : ( ~ (v1 = 0) & aNaturalNumber0(v0) = v1)) & ! % 78.55/11.08 | [v0: $i] : ( ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) | ? [v1: % 78.55/11.08 | any] : ( ~ (v1 = all_26_1) & sdtpldt0(all_26_2, v0) = v1 & % 78.55/11.08 | $i(v1)))) | ( ~ (all_26_3 = 0) & ! [v0: $i] : ( ~ % 78.55/11.08 | (sdtpldt0(all_26_5, v0) = all_26_4) | ~ $i(v0) | ? [v1: int] : % 78.55/11.08 | ( ~ (v1 = 0) & aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( ~ % 78.55/11.08 | (aNaturalNumber0(v0) = 0) | ~ $i(v0) | ? [v1: any] : ( ~ (v1 = % 78.55/11.08 | all_26_4) & sdtpldt0(all_26_5, v0) = v1 & $i(v1))))) % 78.55/11.08 | % 78.55/11.08 | ALPHA: (33) implies: % 78.55/11.08 | (34) sdtpldt0(xl, xm) = all_26_2 % 78.55/11.08 | (35) sdtpldt0(xn, xm) = all_26_1 % 78.55/11.08 | (36) sdtpldt0(xm, xl) = all_26_5 % 78.55/11.08 | (37) sdtpldt0(xm, xn) = all_26_4 % 78.55/11.08 | (38) all_26_1 = all_26_2 | all_26_4 = all_26_5 | ( ~ (all_26_0 = 0) & ! % 78.55/11.08 | [v0: $i] : ( ~ (sdtpldt0(all_26_2, v0) = all_26_1) | ~ $i(v0) | ? % 78.55/11.08 | [v1: int] : ( ~ (v1 = 0) & aNaturalNumber0(v0) = v1)) & ! [v0: % 78.55/11.08 | $i] : ( ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) | ? [v1: any] : ( % 78.55/11.08 | ~ (v1 = all_26_1) & sdtpldt0(all_26_2, v0) = v1 & $i(v1)))) | ( % 78.55/11.08 | ~ (all_26_3 = 0) & ! [v0: $i] : ( ~ (sdtpldt0(all_26_5, v0) = % 78.55/11.08 | all_26_4) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 78.55/11.08 | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( ~ % 78.55/11.08 | (aNaturalNumber0(v0) = 0) | ~ $i(v0) | ? [v1: any] : ( ~ (v1 = % 78.55/11.08 | all_26_4) & sdtpldt0(all_26_5, v0) = v1 & $i(v1)))) % 78.55/11.08 | % 78.55/11.08 | GROUND_INST: instantiating (10) with xn, xl, xn, simplifying with (17), (18), % 78.55/11.08 | (21), (22) gives: % 78.55/11.08 | (39) xn = xl | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( ~ % 78.55/11.08 | (v3 = v2) & ~ (v1 = v0) & sdtpldt0(xn, xn) = v3 & sdtpldt0(xn, xn) % 78.55/11.08 | = v1 & sdtpldt0(xn, xl) = v0 & sdtpldt0(xl, xn) = v2 & $i(v3) & % 78.55/11.08 | $i(v2) & $i(v1) & $i(v0)) % 78.55/11.08 | % 78.55/11.08 | GROUND_INST: instantiating (10) with xm, xn, xl, simplifying with (17), (18), % 78.55/11.08 | (20), (21), (22), (23) gives: % 78.55/11.08 | (40) xn = xl | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( ~ % 78.55/11.08 | (v3 = v2) & ~ (v1 = v0) & sdtpldt0(xm, xn) = v0 & sdtpldt0(xm, xl) % 78.55/11.08 | = v1 & sdtpldt0(xn, xm) = v2 & sdtpldt0(xl, xm) = v3 & $i(v3) & % 78.55/11.08 | $i(v2) & $i(v1) & $i(v0)) % 78.55/11.08 | % 78.55/11.09 | GROUND_INST: instantiating (10) with all_24_0, sz00, sz10, simplifying with % 78.55/11.09 | (1), (3), (9), (13), (29), (30) gives: % 78.55/11.09 | (41) sz10 = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 78.55/11.09 | ( ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(all_24_0, sz10) = v1 & % 78.55/11.09 | sdtpldt0(all_24_0, sz00) = v0 & sdtpldt0(sz10, all_24_0) = v3 & % 78.55/11.09 | sdtpldt0(sz00, all_24_0) = v2 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 78.55/11.09 | % 79.10/11.09 | GROUND_INST: instantiating (10) with all_24_0, sz10, sz00, simplifying with % 79.10/11.09 | (1), (3), (9), (13), (29), (30) gives: % 79.10/11.09 | (42) sz10 = sz00 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 79.10/11.09 | ( ~ (v3 = v2) & ~ (v1 = v0) & sdtpldt0(all_24_0, sz10) = v0 & % 79.10/11.09 | sdtpldt0(all_24_0, sz00) = v1 & sdtpldt0(sz10, all_24_0) = v2 & % 79.10/11.09 | sdtpldt0(sz00, all_24_0) = v3 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 79.10/11.09 | % 79.10/11.09 | GROUND_INST: instantiating (8) with all_24_0, simplifying with (29), (30) % 79.10/11.09 | gives: % 79.10/11.09 | (43) sdtpldt0(all_24_0, sz00) = all_24_0 & sdtpldt0(sz00, all_24_0) = % 79.10/11.09 | all_24_0 % 79.10/11.09 | % 79.10/11.09 | ALPHA: (43) implies: % 79.10/11.09 | (44) sdtpldt0(all_24_0, sz00) = all_24_0 % 79.10/11.09 | % 79.10/11.09 | GROUND_INST: instantiating (5) with xm, xl, all_26_2, simplifying with (21), % 79.10/11.09 | (23), (34) gives: % 79.10/11.09 | (45) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xm, xl) = v2 & % 79.10/11.09 | aNaturalNumber0(xm) = v0 & aNaturalNumber0(xl) = v1 & $i(v2) & ( ~ % 79.10/11.09 | (v1 = 0) | ~ (v0 = 0) | v2 = all_26_2)) % 79.10/11.09 | % 79.10/11.09 | GROUND_INST: instantiating (4) with xl, xm, all_26_2, simplifying with (21), % 79.10/11.09 | (23), (34) gives: % 79.10/11.09 | (46) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xm, xl) = v2 & % 79.10/11.09 | aNaturalNumber0(xm) = v1 & aNaturalNumber0(xl) = v0 & $i(v2) & ( ~ % 79.10/11.09 | (v1 = 0) | ~ (v0 = 0) | v2 = all_26_2)) % 79.10/11.09 | % 79.10/11.09 | GROUND_INST: instantiating (mSortsB) with xl, xm, all_26_2, simplifying with % 79.10/11.09 | (21), (23), (34) gives: % 79.10/11.09 | (47) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 79.10/11.09 | (aNaturalNumber0(all_26_2) = v2 & aNaturalNumber0(xm) = v1 & % 79.10/11.09 | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 79.10/11.09 | % 79.10/11.09 | GROUND_INST: instantiating (12) with all_24_0, xn, xl, xn, simplifying with % 79.10/11.09 | (18), (21), (22), (29), (31) gives: % 79.10/11.09 | (48) xn = xl | ? [v0: any] : ? [v1: any] : ? [v2: $i] : ? [v3: $i] : ? % 79.10/11.09 | [v4: $i] : (sdtpldt0(all_24_0, xn) = v2 & sdtpldt0(all_24_0, xl) = v3 % 79.10/11.09 | & sdtpldt0(xn, all_24_0) = v4 & aNaturalNumber0(all_24_0) = v0 & % 79.10/11.09 | aNaturalNumber0(xl) = v1 & $i(v4) & $i(v3) & $i(v2) & ( ~ (v1 = 0) | % 79.10/11.09 | ~ (v0 = 0) | ( ~ (v4 = xn) & ~ (v3 = v2)))) % 79.10/11.09 | % 79.10/11.09 | GROUND_INST: instantiating (11) with all_24_0, xl, xn, xn, simplifying with % 79.10/11.09 | (18), (21), (22), (29), (31) gives: % 79.10/11.09 | (49) xn = xl | ? [v0: any] : ? [v1: any] : ? [v2: $i] : ? [v3: $i] : ? % 79.10/11.09 | [v4: $i] : (sdtpldt0(all_24_0, xn) = v3 & sdtpldt0(all_24_0, xl) = v2 % 79.10/11.09 | & sdtpldt0(xn, all_24_0) = v4 & aNaturalNumber0(all_24_0) = v0 & % 79.10/11.09 | aNaturalNumber0(xl) = v1 & $i(v4) & $i(v3) & $i(v2) & ( ~ (v1 = 0) | % 79.10/11.09 | ~ (v0 = 0) | ( ~ (v4 = xn) & ~ (v3 = v2)))) % 79.10/11.09 | % 79.10/11.09 | GROUND_INST: instantiating (5) with all_24_0, xl, xn, simplifying with (21), % 79.10/11.09 | (29), (31) gives: % 79.10/11.09 | (50) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(all_24_0, xl) = % 79.10/11.09 | v2 & aNaturalNumber0(all_24_0) = v0 & aNaturalNumber0(xl) = v1 & % 79.10/11.09 | $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = xn)) % 79.10/11.09 | % 79.10/11.09 | GROUND_INST: instantiating (4) with xl, all_24_0, xn, simplifying with (21), % 79.10/11.09 | (29), (31) gives: % 79.10/11.09 | (51) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(all_24_0, xl) = % 79.10/11.09 | v2 & aNaturalNumber0(all_24_0) = v1 & aNaturalNumber0(xl) = v0 & % 79.10/11.09 | $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = xn)) % 79.10/11.09 | % 79.10/11.09 | GROUND_INST: instantiating (7) with xl, all_24_0, xm, xn, all_26_1, % 79.10/11.09 | simplifying with (21), (23), (29), (31), (35) gives: % 79.10/11.10 | (52) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: $i] % 79.10/11.10 | : (sdtpldt0(all_24_0, xm) = v3 & sdtpldt0(xl, v3) = v4 & % 79.10/11.10 | aNaturalNumber0(all_24_0) = v1 & aNaturalNumber0(xm) = v2 & % 79.10/11.10 | aNaturalNumber0(xl) = v0 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = % 79.10/11.10 | 0) | ~ (v0 = 0) | v4 = all_26_1)) % 79.10/11.10 | % 79.10/11.10 | GROUND_INST: instantiating (5) with xm, xn, all_26_1, simplifying with (22), % 79.10/11.10 | (23), (35) gives: % 79.10/11.10 | (53) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xm, xn) = v2 & % 79.10/11.10 | aNaturalNumber0(xm) = v0 & aNaturalNumber0(xn) = v1 & $i(v2) & ( ~ % 79.10/11.10 | (v1 = 0) | ~ (v0 = 0) | v2 = all_26_1)) % 79.10/11.10 | % 79.10/11.10 | GROUND_INST: instantiating (4) with xn, xm, all_26_1, simplifying with (22), % 79.10/11.10 | (23), (35) gives: % 79.10/11.10 | (54) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xm, xn) = v2 & % 79.10/11.10 | aNaturalNumber0(xm) = v1 & aNaturalNumber0(xn) = v0 & $i(v2) & ( ~ % 79.10/11.10 | (v1 = 0) | ~ (v0 = 0) | v2 = all_26_1)) % 79.10/11.10 | % 79.10/11.10 | GROUND_INST: instantiating (mSortsB) with xn, xm, all_26_1, simplifying with % 79.10/11.10 | (22), (23), (35) gives: % 79.10/11.10 | (55) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 79.10/11.10 | (aNaturalNumber0(all_26_1) = v2 & aNaturalNumber0(xm) = v1 & % 79.10/11.10 | aNaturalNumber0(xn) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 79.10/11.10 | % 79.10/11.10 | GROUND_INST: instantiating (5) with xl, xm, all_26_5, simplifying with (21), % 79.10/11.10 | (23), (36) gives: % 79.10/11.10 | (56) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xl, xm) = v2 & % 79.10/11.10 | aNaturalNumber0(xm) = v1 & aNaturalNumber0(xl) = v0 & $i(v2) & ( ~ % 79.10/11.10 | (v1 = 0) | ~ (v0 = 0) | v2 = all_26_5)) % 79.10/11.10 | % 79.10/11.10 | GROUND_INST: instantiating (4) with xm, xl, all_26_5, simplifying with (21), % 79.10/11.10 | (23), (36) gives: % 79.10/11.10 | (57) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xl, xm) = v2 & % 79.10/11.10 | aNaturalNumber0(xm) = v0 & aNaturalNumber0(xl) = v1 & $i(v2) & ( ~ % 79.10/11.10 | (v1 = 0) | ~ (v0 = 0) | v2 = all_26_5)) % 79.10/11.10 | % 79.10/11.10 | GROUND_INST: instantiating (mSortsB) with xm, xl, all_26_5, simplifying with % 79.10/11.10 | (21), (23), (36) gives: % 79.10/11.10 | (58) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 79.10/11.10 | (aNaturalNumber0(all_26_5) = v2 & aNaturalNumber0(xm) = v0 & % 79.10/11.10 | aNaturalNumber0(xl) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 79.10/11.10 | % 79.10/11.10 | GROUND_INST: instantiating (6) with xm, xl, all_24_0, xn, all_26_4, % 79.10/11.10 | simplifying with (21), (23), (29), (31), (37) gives: % 79.10/11.10 | (59) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: $i] % 79.10/11.10 | : (sdtpldt0(v3, all_24_0) = v4 & sdtpldt0(xm, xl) = v3 & % 79.10/11.10 | aNaturalNumber0(all_24_0) = v2 & aNaturalNumber0(xm) = v0 & % 79.10/11.10 | aNaturalNumber0(xl) = v1 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = % 79.10/11.10 | 0) | ~ (v0 = 0) | v4 = all_26_4)) % 79.10/11.10 | % 79.10/11.10 | GROUND_INST: instantiating (5) with xn, xm, all_26_4, simplifying with (22), % 79.10/11.10 | (23), (37) gives: % 79.10/11.10 | (60) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xn, xm) = v2 & % 79.10/11.10 | aNaturalNumber0(xm) = v1 & aNaturalNumber0(xn) = v0 & $i(v2) & ( ~ % 79.10/11.10 | (v1 = 0) | ~ (v0 = 0) | v2 = all_26_4)) % 79.10/11.10 | % 79.10/11.10 | GROUND_INST: instantiating (4) with xm, xn, all_26_4, simplifying with (22), % 79.10/11.10 | (23), (37) gives: % 79.10/11.10 | (61) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xn, xm) = v2 & % 79.10/11.10 | aNaturalNumber0(xm) = v0 & aNaturalNumber0(xn) = v1 & $i(v2) & ( ~ % 79.10/11.10 | (v1 = 0) | ~ (v0 = 0) | v2 = all_26_4)) % 79.10/11.10 | % 79.10/11.10 | GROUND_INST: instantiating (16) with all_24_0, xl, xn, simplifying with (21), % 79.10/11.10 | (22), (29), (30), (32) gives: % 79.10/11.10 | (62) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 79.10/11.10 | (sdtlseqdt0(all_24_0, xn) = v3 & sdtlseqdt0(all_24_0, xl) = v2 & % 79.10/11.10 | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | % 79.10/11.10 | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0)) % 79.10/11.10 | % 79.10/11.10 | GROUND_INST: instantiating (15) with xl, xn, all_24_0, simplifying with (21), % 79.10/11.10 | (22), (29), (30), (32) gives: % 79.10/11.10 | (63) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 79.10/11.10 | (sdtlseqdt0(xn, all_24_0) = v2 & sdtlseqdt0(xl, all_24_0) = v3 & % 79.10/11.10 | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | % 79.10/11.10 | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0)) % 79.10/11.10 | % 79.10/11.10 | GROUND_INST: instantiating (16) with xm, xl, xn, simplifying with (20), (21), % 79.10/11.10 | (22), (23), (32) gives: % 79.10/11.11 | (64) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 79.10/11.11 | (sdtlseqdt0(xm, xn) = v3 & sdtlseqdt0(xm, xl) = v2 & % 79.10/11.11 | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | % 79.10/11.11 | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0)) % 79.10/11.11 | % 79.10/11.11 | GROUND_INST: instantiating (15) with xl, xn, xm, simplifying with (20), (21), % 79.10/11.11 | (22), (23), (32) gives: % 79.10/11.11 | (65) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 79.10/11.11 | (sdtlseqdt0(xn, xm) = v2 & sdtlseqdt0(xl, xm) = v3 & % 79.10/11.11 | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | % 79.10/11.11 | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0)) % 79.10/11.11 | % 79.10/11.11 | GROUND_INST: instantiating (16) with xn, xl, xn, simplifying with (18), (21), % 79.10/11.11 | (22), (32) gives: % 79.10/11.11 | (66) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 79.10/11.11 | (sdtlseqdt0(xn, xn) = v3 & sdtlseqdt0(xn, xl) = v2 & % 79.10/11.11 | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | % 79.10/11.11 | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0)) % 79.10/11.11 | % 79.10/11.11 | GROUND_INST: instantiating (15) with xl, xn, xn, simplifying with (18), (21), % 79.10/11.11 | (22), (32) gives: % 79.10/11.11 | (67) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 79.10/11.11 | (sdtlseqdt0(xn, xn) = v2 & sdtlseqdt0(xl, xn) = v3 & % 79.10/11.11 | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | % 79.10/11.11 | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0)) % 79.10/11.11 | % 79.10/11.11 | GROUND_INST: instantiating (16) with xl, xl, xn, simplifying with (17), (21), % 79.10/11.11 | (22), (32) gives: % 79.10/11.11 | (68) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 79.10/11.11 | (sdtlseqdt0(xl, xn) = v3 & sdtlseqdt0(xl, xl) = v2 & % 79.10/11.11 | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | % 79.10/11.11 | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0)) % 79.10/11.11 | % 79.10/11.11 | GROUND_INST: instantiating (15) with xl, xn, xl, simplifying with (17), (21), % 79.10/11.11 | (22), (32) gives: % 79.10/11.11 | (69) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 79.10/11.11 | (sdtlseqdt0(xn, xl) = v2 & sdtlseqdt0(xl, xl) = v3 & % 79.10/11.11 | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | % 79.10/11.11 | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0)) % 79.10/11.11 | % 79.10/11.11 | GROUND_INST: instantiating (16) with sz10, xl, xn, simplifying with (3), (9), % 79.10/11.11 | (21), (22), (32) gives: % 79.10/11.11 | (70) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 79.10/11.11 | (sdtlseqdt0(sz10, xn) = v3 & sdtlseqdt0(sz10, xl) = v2 & % 79.10/11.11 | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | % 79.10/11.11 | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0)) % 79.10/11.11 | % 79.10/11.11 | GROUND_INST: instantiating (15) with xl, xn, sz10, simplifying with (3), (9), % 79.10/11.11 | (21), (22), (32) gives: % 79.10/11.11 | (71) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 79.10/11.11 | (sdtlseqdt0(xn, sz10) = v2 & sdtlseqdt0(xl, sz10) = v3 & % 79.10/11.11 | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | % 79.10/11.11 | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0)) % 79.10/11.11 | % 79.10/11.11 | GROUND_INST: instantiating (16) with sz00, xl, xn, simplifying with (1), (13), % 79.10/11.11 | (21), (22), (32) gives: % 79.10/11.11 | (72) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 79.10/11.11 | (sdtlseqdt0(sz00, xn) = v3 & sdtlseqdt0(sz00, xl) = v2 & % 79.10/11.11 | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | % 79.10/11.11 | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0)) % 79.10/11.11 | % 79.10/11.11 | GROUND_INST: instantiating (15) with xl, xn, sz00, simplifying with (1), (13), % 79.10/11.11 | (21), (22), (32) gives: % 79.10/11.11 | (73) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 79.10/11.11 | (sdtlseqdt0(xn, sz00) = v2 & sdtlseqdt0(xl, sz00) = v3 & % 79.10/11.11 | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v2 = 0) | % 79.10/11.11 | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0)) % 79.10/11.11 | % 79.10/11.11 | GROUND_INST: instantiating (14) with xl, xn, simplifying with (21), (22), (32) % 79.10/11.11 | gives: % 79.10/11.11 | (74) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtmndt0(xn, xl) = v2 & % 79.10/11.11 | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xl) = v0 & $i(v2) & ( ~ % 79.10/11.11 | (v1 = 0) | ~ (v0 = 0) | ( ! [v3: $i] : (v3 = v2 | ~ % 79.10/11.11 | (sdtpldt0(xl, v3) = xn) | ~ $i(v3) | ? [v4: int] : ( ~ (v4 = % 79.10/11.11 | 0) & aNaturalNumber0(v3) = v4)) & ! [v3: $i] : (v3 = v2 | % 79.10/11.11 | ~ (aNaturalNumber0(v3) = 0) | ~ $i(v3) | ? [v4: $i] : ( ~ % 79.10/11.11 | (v4 = xn) & sdtpldt0(xl, v3) = v4 & $i(v4))) & ! [v3: $i] : % 79.10/11.11 | (v3 = xn | ~ (sdtpldt0(xl, v2) = v3)) & ! [v3: int] : (v3 = 0 % 79.10/11.11 | | ~ (aNaturalNumber0(v2) = v3)) & ! [v3: $i] : ( ~ % 79.10/11.11 | (sdtpldt0(xl, v2) = v3) | aNaturalNumber0(v2) = 0) & ! [v3: % 79.10/11.11 | MultipleValueBool] : ( ~ (aNaturalNumber0(v2) = v3) | % 79.10/11.11 | sdtpldt0(xl, v2) = xn)))) % 79.10/11.11 | % 79.10/11.11 | DELTA: instantiating (47) with fresh symbols all_278_0, all_278_1, all_278_2 % 79.10/11.11 | gives: % 79.10/11.11 | (75) aNaturalNumber0(all_26_2) = all_278_0 & aNaturalNumber0(xm) = % 79.10/11.11 | all_278_1 & aNaturalNumber0(xl) = all_278_2 & ( ~ (all_278_1 = 0) | ~ % 79.10/11.11 | (all_278_2 = 0) | all_278_0 = 0) % 79.10/11.11 | % 79.10/11.11 | ALPHA: (75) implies: % 79.10/11.11 | (76) aNaturalNumber0(xl) = all_278_2 % 79.10/11.11 | % 79.10/11.11 | DELTA: instantiating (58) with fresh symbols all_306_0, all_306_1, all_306_2 % 79.10/11.11 | gives: % 79.10/11.11 | (77) aNaturalNumber0(all_26_5) = all_306_0 & aNaturalNumber0(xm) = % 79.10/11.11 | all_306_2 & aNaturalNumber0(xl) = all_306_1 & ( ~ (all_306_1 = 0) | ~ % 79.10/11.11 | (all_306_2 = 0) | all_306_0 = 0) % 79.10/11.11 | % 79.10/11.11 | ALPHA: (77) implies: % 79.10/11.12 | (78) aNaturalNumber0(xl) = all_306_1 % 79.10/11.12 | (79) aNaturalNumber0(xm) = all_306_2 % 79.10/11.12 | % 79.10/11.12 | DELTA: instantiating (55) with fresh symbols all_308_0, all_308_1, all_308_2 % 79.10/11.12 | gives: % 79.10/11.12 | (80) aNaturalNumber0(all_26_1) = all_308_0 & aNaturalNumber0(xm) = % 79.10/11.12 | all_308_1 & aNaturalNumber0(xn) = all_308_2 & ( ~ (all_308_1 = 0) | ~ % 79.10/11.12 | (all_308_2 = 0) | all_308_0 = 0) % 79.10/11.12 | % 79.10/11.12 | ALPHA: (80) implies: % 79.10/11.12 | (81) aNaturalNumber0(xm) = all_308_1 % 79.10/11.12 | % 79.10/11.12 | DELTA: instantiating (51) with fresh symbols all_474_0, all_474_1, all_474_2 % 79.10/11.12 | gives: % 79.10/11.12 | (82) sdtpldt0(all_24_0, xl) = all_474_0 & aNaturalNumber0(all_24_0) = % 79.10/11.12 | all_474_1 & aNaturalNumber0(xl) = all_474_2 & $i(all_474_0) & ( ~ % 79.10/11.12 | (all_474_1 = 0) | ~ (all_474_2 = 0) | all_474_0 = xn) % 79.10/11.12 | % 79.10/11.12 | ALPHA: (82) implies: % 79.10/11.12 | (83) aNaturalNumber0(xl) = all_474_2 % 79.10/11.12 | (84) aNaturalNumber0(all_24_0) = all_474_1 % 79.10/11.12 | % 79.10/11.12 | DELTA: instantiating (50) with fresh symbols all_476_0, all_476_1, all_476_2 % 79.10/11.12 | gives: % 79.10/11.12 | (85) sdtpldt0(all_24_0, xl) = all_476_0 & aNaturalNumber0(all_24_0) = % 79.10/11.12 | all_476_2 & aNaturalNumber0(xl) = all_476_1 & $i(all_476_0) & ( ~ % 79.10/11.12 | (all_476_1 = 0) | ~ (all_476_2 = 0) | all_476_0 = xn) % 79.10/11.12 | % 79.10/11.12 | ALPHA: (85) implies: % 79.10/11.12 | (86) aNaturalNumber0(xl) = all_476_1 % 79.10/11.12 | (87) aNaturalNumber0(all_24_0) = all_476_2 % 79.10/11.12 | % 79.10/11.12 | DELTA: instantiating (61) with fresh symbols all_478_0, all_478_1, all_478_2 % 79.10/11.12 | gives: % 79.10/11.12 | (88) sdtpldt0(xn, xm) = all_478_0 & aNaturalNumber0(xm) = all_478_2 & % 79.10/11.12 | aNaturalNumber0(xn) = all_478_1 & $i(all_478_0) & ( ~ (all_478_1 = 0) % 79.10/11.12 | | ~ (all_478_2 = 0) | all_478_0 = all_26_4) % 79.10/11.12 | % 79.10/11.12 | ALPHA: (88) implies: % 79.10/11.12 | (89) aNaturalNumber0(xm) = all_478_2 % 79.10/11.12 | (90) sdtpldt0(xn, xm) = all_478_0 % 79.10/11.12 | % 79.10/11.12 | DELTA: instantiating (46) with fresh symbols all_480_0, all_480_1, all_480_2 % 79.10/11.12 | gives: % 79.10/11.12 | (91) sdtpldt0(xm, xl) = all_480_0 & aNaturalNumber0(xm) = all_480_1 & % 79.10/11.12 | aNaturalNumber0(xl) = all_480_2 & $i(all_480_0) & ( ~ (all_480_1 = 0) % 79.10/11.12 | | ~ (all_480_2 = 0) | all_480_0 = all_26_2) % 79.10/11.12 | % 79.10/11.12 | ALPHA: (91) implies: % 79.10/11.12 | (92) aNaturalNumber0(xl) = all_480_2 % 79.10/11.12 | (93) aNaturalNumber0(xm) = all_480_1 % 79.10/11.12 | % 79.10/11.12 | DELTA: instantiating (45) with fresh symbols all_482_0, all_482_1, all_482_2 % 79.10/11.12 | gives: % 79.10/11.12 | (94) sdtpldt0(xm, xl) = all_482_0 & aNaturalNumber0(xm) = all_482_2 & % 79.10/11.12 | aNaturalNumber0(xl) = all_482_1 & $i(all_482_0) & ( ~ (all_482_1 = 0) % 79.10/11.12 | | ~ (all_482_2 = 0) | all_482_0 = all_26_2) % 79.10/11.12 | % 79.10/11.12 | ALPHA: (94) implies: % 79.10/11.12 | (95) aNaturalNumber0(xl) = all_482_1 % 79.10/11.12 | (96) aNaturalNumber0(xm) = all_482_2 % 79.10/11.12 | % 79.10/11.12 | DELTA: instantiating (57) with fresh symbols all_484_0, all_484_1, all_484_2 % 79.10/11.12 | gives: % 79.10/11.12 | (97) sdtpldt0(xl, xm) = all_484_0 & aNaturalNumber0(xm) = all_484_2 & % 79.10/11.12 | aNaturalNumber0(xl) = all_484_1 & $i(all_484_0) & ( ~ (all_484_1 = 0) % 79.10/11.12 | | ~ (all_484_2 = 0) | all_484_0 = all_26_5) % 79.10/11.12 | % 79.10/11.12 | ALPHA: (97) implies: % 79.10/11.12 | (98) aNaturalNumber0(xl) = all_484_1 % 79.10/11.12 | (99) aNaturalNumber0(xm) = all_484_2 % 79.10/11.12 | (100) sdtpldt0(xl, xm) = all_484_0 % 79.10/11.12 | % 79.10/11.12 | DELTA: instantiating (56) with fresh symbols all_486_0, all_486_1, all_486_2 % 79.10/11.12 | gives: % 79.10/11.12 | (101) sdtpldt0(xl, xm) = all_486_0 & aNaturalNumber0(xm) = all_486_1 & % 79.10/11.12 | aNaturalNumber0(xl) = all_486_2 & $i(all_486_0) & ( ~ (all_486_1 = 0) % 79.10/11.12 | | ~ (all_486_2 = 0) | all_486_0 = all_26_5) % 79.10/11.12 | % 79.10/11.12 | ALPHA: (101) implies: % 79.10/11.12 | (102) aNaturalNumber0(xl) = all_486_2 % 79.10/11.12 | (103) aNaturalNumber0(xm) = all_486_1 % 79.10/11.12 | (104) sdtpldt0(xl, xm) = all_486_0 % 79.10/11.12 | (105) ~ (all_486_1 = 0) | ~ (all_486_2 = 0) | all_486_0 = all_26_5 % 79.10/11.12 | % 79.10/11.12 | DELTA: instantiating (54) with fresh symbols all_488_0, all_488_1, all_488_2 % 79.10/11.12 | gives: % 79.10/11.12 | (106) sdtpldt0(xm, xn) = all_488_0 & aNaturalNumber0(xm) = all_488_1 & % 79.10/11.12 | aNaturalNumber0(xn) = all_488_2 & $i(all_488_0) & ( ~ (all_488_1 = 0) % 79.10/11.12 | | ~ (all_488_2 = 0) | all_488_0 = all_26_1) % 79.10/11.12 | % 79.10/11.12 | ALPHA: (106) implies: % 79.10/11.12 | (107) aNaturalNumber0(xn) = all_488_2 % 79.10/11.12 | (108) aNaturalNumber0(xm) = all_488_1 % 79.10/11.12 | % 79.10/11.12 | DELTA: instantiating (53) with fresh symbols all_490_0, all_490_1, all_490_2 % 79.10/11.12 | gives: % 79.10/11.12 | (109) sdtpldt0(xm, xn) = all_490_0 & aNaturalNumber0(xm) = all_490_2 & % 79.10/11.12 | aNaturalNumber0(xn) = all_490_1 & $i(all_490_0) & ( ~ (all_490_1 = 0) % 79.10/11.12 | | ~ (all_490_2 = 0) | all_490_0 = all_26_1) % 79.10/11.12 | % 79.10/11.12 | ALPHA: (109) implies: % 79.10/11.12 | (110) aNaturalNumber0(xn) = all_490_1 % 79.10/11.12 | (111) aNaturalNumber0(xm) = all_490_2 % 79.10/11.12 | % 79.10/11.12 | DELTA: instantiating (60) with fresh symbols all_492_0, all_492_1, all_492_2 % 79.10/11.12 | gives: % 79.10/11.12 | (112) sdtpldt0(xn, xm) = all_492_0 & aNaturalNumber0(xm) = all_492_1 & % 79.10/11.12 | aNaturalNumber0(xn) = all_492_2 & $i(all_492_0) & ( ~ (all_492_1 = 0) % 79.10/11.12 | | ~ (all_492_2 = 0) | all_492_0 = all_26_4) % 79.10/11.12 | % 79.10/11.12 | ALPHA: (112) implies: % 79.10/11.12 | (113) aNaturalNumber0(xn) = all_492_2 % 79.10/11.12 | (114) aNaturalNumber0(xm) = all_492_1 % 79.10/11.12 | (115) sdtpldt0(xn, xm) = all_492_0 % 79.10/11.12 | (116) ~ (all_492_1 = 0) | ~ (all_492_2 = 0) | all_492_0 = all_26_4 % 79.10/11.12 | % 79.10/11.12 | DELTA: instantiating (73) with fresh symbols all_494_0, all_494_1, all_494_2, % 79.10/11.12 | all_494_3 gives: % 79.10/11.12 | (117) sdtlseqdt0(xn, sz00) = all_494_1 & sdtlseqdt0(xl, sz00) = all_494_0 & % 79.10/11.12 | aNaturalNumber0(xn) = all_494_2 & aNaturalNumber0(xl) = all_494_3 & ( % 79.10/11.12 | ~ (all_494_1 = 0) | ~ (all_494_2 = 0) | ~ (all_494_3 = 0) | % 79.10/11.12 | all_494_0 = 0) % 79.10/11.12 | % 79.10/11.12 | ALPHA: (117) implies: % 79.10/11.12 | (118) aNaturalNumber0(xl) = all_494_3 % 79.10/11.12 | (119) aNaturalNumber0(xn) = all_494_2 % 79.10/11.12 | % 79.10/11.12 | DELTA: instantiating (72) with fresh symbols all_496_0, all_496_1, all_496_2, % 79.10/11.12 | all_496_3 gives: % 79.10/11.12 | (120) sdtlseqdt0(sz00, xn) = all_496_0 & sdtlseqdt0(sz00, xl) = all_496_1 & % 79.10/11.12 | aNaturalNumber0(xn) = all_496_2 & aNaturalNumber0(xl) = all_496_3 & ( % 79.10/11.12 | ~ (all_496_1 = 0) | ~ (all_496_2 = 0) | ~ (all_496_3 = 0) | % 79.10/11.12 | all_496_0 = 0) % 79.10/11.12 | % 79.10/11.12 | ALPHA: (120) implies: % 79.10/11.12 | (121) aNaturalNumber0(xl) = all_496_3 % 79.10/11.12 | (122) aNaturalNumber0(xn) = all_496_2 % 79.10/11.12 | % 79.10/11.12 | DELTA: instantiating (63) with fresh symbols all_498_0, all_498_1, all_498_2, % 79.10/11.12 | all_498_3 gives: % 79.10/11.13 | (123) sdtlseqdt0(xn, all_24_0) = all_498_1 & sdtlseqdt0(xl, all_24_0) = % 79.10/11.13 | all_498_0 & aNaturalNumber0(xn) = all_498_2 & aNaturalNumber0(xl) = % 79.10/11.13 | all_498_3 & ( ~ (all_498_1 = 0) | ~ (all_498_2 = 0) | ~ (all_498_3 % 79.10/11.13 | = 0) | all_498_0 = 0) % 79.10/11.13 | % 79.10/11.13 | ALPHA: (123) implies: % 79.10/11.13 | (124) aNaturalNumber0(xl) = all_498_3 % 79.10/11.13 | (125) aNaturalNumber0(xn) = all_498_2 % 79.10/11.13 | % 79.10/11.13 | DELTA: instantiating (62) with fresh symbols all_500_0, all_500_1, all_500_2, % 79.10/11.13 | all_500_3 gives: % 79.10/11.13 | (126) sdtlseqdt0(all_24_0, xn) = all_500_0 & sdtlseqdt0(all_24_0, xl) = % 79.10/11.13 | all_500_1 & aNaturalNumber0(xn) = all_500_2 & aNaturalNumber0(xl) = % 79.10/11.13 | all_500_3 & ( ~ (all_500_1 = 0) | ~ (all_500_2 = 0) | ~ (all_500_3 % 79.10/11.13 | = 0) | all_500_0 = 0) % 79.10/11.13 | % 79.10/11.13 | ALPHA: (126) implies: % 79.10/11.13 | (127) aNaturalNumber0(xl) = all_500_3 % 79.10/11.13 | (128) aNaturalNumber0(xn) = all_500_2 % 79.10/11.13 | % 79.10/11.13 | DELTA: instantiating (71) with fresh symbols all_502_0, all_502_1, all_502_2, % 79.10/11.13 | all_502_3 gives: % 79.10/11.13 | (129) sdtlseqdt0(xn, sz10) = all_502_1 & sdtlseqdt0(xl, sz10) = all_502_0 & % 79.10/11.13 | aNaturalNumber0(xn) = all_502_2 & aNaturalNumber0(xl) = all_502_3 & ( % 79.10/11.13 | ~ (all_502_1 = 0) | ~ (all_502_2 = 0) | ~ (all_502_3 = 0) | % 79.10/11.13 | all_502_0 = 0) % 79.10/11.13 | % 79.10/11.13 | ALPHA: (129) implies: % 79.10/11.13 | (130) aNaturalNumber0(xl) = all_502_3 % 79.10/11.13 | (131) aNaturalNumber0(xn) = all_502_2 % 79.10/11.13 | % 79.10/11.13 | DELTA: instantiating (69) with fresh symbols all_504_0, all_504_1, all_504_2, % 79.10/11.13 | all_504_3 gives: % 79.10/11.13 | (132) sdtlseqdt0(xn, xl) = all_504_1 & sdtlseqdt0(xl, xl) = all_504_0 & % 79.10/11.13 | aNaturalNumber0(xn) = all_504_2 & aNaturalNumber0(xl) = all_504_3 & ( % 79.10/11.13 | ~ (all_504_1 = 0) | ~ (all_504_2 = 0) | ~ (all_504_3 = 0) | % 79.10/11.13 | all_504_0 = 0) % 79.10/11.13 | % 79.10/11.13 | ALPHA: (132) implies: % 79.10/11.13 | (133) aNaturalNumber0(xl) = all_504_3 % 79.10/11.13 | (134) aNaturalNumber0(xn) = all_504_2 % 79.10/11.13 | % 79.10/11.13 | DELTA: instantiating (68) with fresh symbols all_506_0, all_506_1, all_506_2, % 79.10/11.13 | all_506_3 gives: % 79.10/11.13 | (135) sdtlseqdt0(xl, xn) = all_506_0 & sdtlseqdt0(xl, xl) = all_506_1 & % 79.10/11.13 | aNaturalNumber0(xn) = all_506_2 & aNaturalNumber0(xl) = all_506_3 & ( % 79.10/11.13 | ~ (all_506_1 = 0) | ~ (all_506_2 = 0) | ~ (all_506_3 = 0) | % 79.10/11.13 | all_506_0 = 0) % 79.10/11.13 | % 79.10/11.13 | ALPHA: (135) implies: % 79.10/11.13 | (136) aNaturalNumber0(xl) = all_506_3 % 79.10/11.13 | % 79.10/11.13 | DELTA: instantiating (70) with fresh symbols all_508_0, all_508_1, all_508_2, % 79.10/11.13 | all_508_3 gives: % 79.10/11.13 | (137) sdtlseqdt0(sz10, xn) = all_508_0 & sdtlseqdt0(sz10, xl) = all_508_1 & % 79.10/11.13 | aNaturalNumber0(xn) = all_508_2 & aNaturalNumber0(xl) = all_508_3 & ( % 79.10/11.13 | ~ (all_508_1 = 0) | ~ (all_508_2 = 0) | ~ (all_508_3 = 0) | % 79.10/11.13 | all_508_0 = 0) % 79.10/11.13 | % 79.10/11.13 | ALPHA: (137) implies: % 79.10/11.13 | (138) aNaturalNumber0(xl) = all_508_3 % 79.10/11.13 | (139) aNaturalNumber0(xn) = all_508_2 % 79.10/11.13 | % 79.10/11.13 | DELTA: instantiating (67) with fresh symbols all_510_0, all_510_1, all_510_2, % 79.10/11.13 | all_510_3 gives: % 79.10/11.13 | (140) sdtlseqdt0(xn, xn) = all_510_1 & sdtlseqdt0(xl, xn) = all_510_0 & % 79.10/11.13 | aNaturalNumber0(xn) = all_510_2 & aNaturalNumber0(xl) = all_510_3 & ( % 79.10/11.13 | ~ (all_510_1 = 0) | ~ (all_510_2 = 0) | ~ (all_510_3 = 0) | % 79.10/11.13 | all_510_0 = 0) % 79.10/11.13 | % 79.10/11.13 | ALPHA: (140) implies: % 79.10/11.13 | (141) aNaturalNumber0(xl) = all_510_3 % 79.10/11.13 | (142) aNaturalNumber0(xn) = all_510_2 % 79.10/11.13 | % 79.10/11.13 | DELTA: instantiating (65) with fresh symbols all_512_0, all_512_1, all_512_2, % 79.10/11.13 | all_512_3 gives: % 79.10/11.13 | (143) sdtlseqdt0(xn, xm) = all_512_1 & sdtlseqdt0(xl, xm) = all_512_0 & % 79.10/11.13 | aNaturalNumber0(xn) = all_512_2 & aNaturalNumber0(xl) = all_512_3 & ( % 79.10/11.13 | ~ (all_512_1 = 0) | ~ (all_512_2 = 0) | ~ (all_512_3 = 0) | % 79.10/11.13 | all_512_0 = 0) % 79.10/11.13 | % 79.10/11.13 | ALPHA: (143) implies: % 79.10/11.13 | (144) aNaturalNumber0(xl) = all_512_3 % 79.10/11.13 | (145) aNaturalNumber0(xn) = all_512_2 % 79.10/11.13 | % 79.10/11.13 | DELTA: instantiating (64) with fresh symbols all_514_0, all_514_1, all_514_2, % 79.10/11.13 | all_514_3 gives: % 79.10/11.13 | (146) sdtlseqdt0(xm, xn) = all_514_0 & sdtlseqdt0(xm, xl) = all_514_1 & % 79.10/11.13 | aNaturalNumber0(xn) = all_514_2 & aNaturalNumber0(xl) = all_514_3 & ( % 79.10/11.13 | ~ (all_514_1 = 0) | ~ (all_514_2 = 0) | ~ (all_514_3 = 0) | % 79.10/11.13 | all_514_0 = 0) % 79.10/11.13 | % 79.10/11.13 | ALPHA: (146) implies: % 79.10/11.13 | (147) aNaturalNumber0(xl) = all_514_3 % 79.10/11.13 | % 79.10/11.13 | DELTA: instantiating (66) with fresh symbols all_516_0, all_516_1, all_516_2, % 79.10/11.13 | all_516_3 gives: % 79.10/11.13 | (148) sdtlseqdt0(xn, xn) = all_516_0 & sdtlseqdt0(xn, xl) = all_516_1 & % 79.10/11.13 | aNaturalNumber0(xn) = all_516_2 & aNaturalNumber0(xl) = all_516_3 & ( % 79.10/11.13 | ~ (all_516_1 = 0) | ~ (all_516_2 = 0) | ~ (all_516_3 = 0) | % 79.10/11.13 | all_516_0 = 0) % 79.10/11.13 | % 79.10/11.13 | ALPHA: (148) implies: % 79.10/11.13 | (149) aNaturalNumber0(xl) = all_516_3 % 79.10/11.13 | % 79.10/11.13 | DELTA: instantiating (52) with fresh symbols all_520_0, all_520_1, all_520_2, % 79.10/11.13 | all_520_3, all_520_4 gives: % 79.10/11.13 | (150) sdtpldt0(all_24_0, xm) = all_520_1 & sdtpldt0(xl, all_520_1) = % 79.10/11.13 | all_520_0 & aNaturalNumber0(all_24_0) = all_520_3 & % 79.10/11.13 | aNaturalNumber0(xm) = all_520_2 & aNaturalNumber0(xl) = all_520_4 & % 79.10/11.13 | $i(all_520_0) & $i(all_520_1) & ( ~ (all_520_2 = 0) | ~ (all_520_3 = % 79.10/11.13 | 0) | ~ (all_520_4 = 0) | all_520_0 = all_26_1) % 79.10/11.13 | % 79.10/11.13 | ALPHA: (150) implies: % 79.10/11.13 | (151) aNaturalNumber0(xl) = all_520_4 % 79.10/11.13 | (152) aNaturalNumber0(xm) = all_520_2 % 79.10/11.13 | (153) aNaturalNumber0(all_24_0) = all_520_3 % 79.10/11.13 | % 79.10/11.13 | DELTA: instantiating (59) with fresh symbols all_522_0, all_522_1, all_522_2, % 79.10/11.13 | all_522_3, all_522_4 gives: % 79.10/11.13 | (154) sdtpldt0(all_522_1, all_24_0) = all_522_0 & sdtpldt0(xm, xl) = % 79.10/11.13 | all_522_1 & aNaturalNumber0(all_24_0) = all_522_2 & % 79.10/11.13 | aNaturalNumber0(xm) = all_522_4 & aNaturalNumber0(xl) = all_522_3 & % 79.10/11.13 | $i(all_522_0) & $i(all_522_1) & ( ~ (all_522_2 = 0) | ~ (all_522_3 = % 79.10/11.13 | 0) | ~ (all_522_4 = 0) | all_522_0 = all_26_4) % 79.10/11.13 | % 79.10/11.13 | ALPHA: (154) implies: % 79.10/11.13 | (155) aNaturalNumber0(xl) = all_522_3 % 79.10/11.13 | (156) aNaturalNumber0(xm) = all_522_4 % 79.10/11.13 | (157) aNaturalNumber0(all_24_0) = all_522_2 % 79.10/11.13 | (158) sdtpldt0(xm, xl) = all_522_1 % 79.10/11.13 | (159) sdtpldt0(all_522_1, all_24_0) = all_522_0 % 79.10/11.13 | (160) ~ (all_522_2 = 0) | ~ (all_522_3 = 0) | ~ (all_522_4 = 0) | % 79.10/11.13 | all_522_0 = all_26_4 % 79.10/11.13 | % 79.10/11.13 | DELTA: instantiating (74) with fresh symbols all_524_0, all_524_1, all_524_2 % 79.10/11.13 | gives: % 79.10/11.13 | (161) sdtmndt0(xn, xl) = all_524_0 & aNaturalNumber0(xn) = all_524_1 & % 79.10/11.13 | aNaturalNumber0(xl) = all_524_2 & $i(all_524_0) & ( ~ (all_524_1 = 0) % 79.10/11.13 | | ~ (all_524_2 = 0) | ( ! [v0: any] : (v0 = all_524_0 | ~ % 79.10/11.13 | (sdtpldt0(xl, v0) = xn) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = % 79.10/11.13 | 0) & aNaturalNumber0(v0) = v1)) & ! [v0: any] : (v0 = % 79.10/11.13 | all_524_0 | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) | ? [v1: % 79.10/11.13 | $i] : ( ~ (v1 = xn) & sdtpldt0(xl, v0) = v1 & $i(v1))) & ! % 79.10/11.13 | [v0: $i] : (v0 = xn | ~ (sdtpldt0(xl, all_524_0) = v0)) & ! % 79.10/11.13 | [v0: int] : (v0 = 0 | ~ (aNaturalNumber0(all_524_0) = v0)) & ! % 79.10/11.13 | [v0: $i] : ( ~ (sdtpldt0(xl, all_524_0) = v0) | % 79.10/11.13 | aNaturalNumber0(all_524_0) = 0) & ! [v0: MultipleValueBool] : % 79.10/11.13 | ( ~ (aNaturalNumber0(all_524_0) = v0) | sdtpldt0(xl, all_524_0) = % 79.10/11.13 | xn))) % 79.10/11.13 | % 79.10/11.13 | ALPHA: (161) implies: % 79.10/11.13 | (162) aNaturalNumber0(xl) = all_524_2 % 79.10/11.13 | (163) aNaturalNumber0(xn) = all_524_1 % 79.10/11.13 | % 79.10/11.13 | BETA: splitting (40) gives: % 79.10/11.13 | % 79.10/11.14 | Case 1: % 79.10/11.14 | | % 79.10/11.14 | | (164) xn = xl % 79.10/11.14 | | % 79.10/11.14 | | REDUCE: (28), (164) imply: % 79.10/11.14 | | (165) $false % 79.10/11.14 | | % 79.10/11.14 | | CLOSE: (165) is inconsistent. % 79.10/11.14 | | % 79.10/11.14 | Case 2: % 79.10/11.14 | | % 79.10/11.14 | | (166) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( ~ (v3 = % 79.10/11.14 | | v2) & ~ (v1 = v0) & sdtpldt0(xm, xn) = v0 & sdtpldt0(xm, xl) = % 79.10/11.14 | | v1 & sdtpldt0(xn, xm) = v2 & sdtpldt0(xl, xm) = v3 & $i(v3) & % 79.10/11.14 | | $i(v2) & $i(v1) & $i(v0)) % 79.10/11.14 | | % 79.10/11.14 | | DELTA: instantiating (166) with fresh symbols all_530_0, all_530_1, % 79.10/11.14 | | all_530_2, all_530_3 gives: % 79.10/11.14 | | (167) ~ (all_530_0 = all_530_1) & ~ (all_530_2 = all_530_3) & % 79.10/11.14 | | sdtpldt0(xm, xn) = all_530_3 & sdtpldt0(xm, xl) = all_530_2 & % 79.10/11.14 | | sdtpldt0(xn, xm) = all_530_1 & sdtpldt0(xl, xm) = all_530_0 & % 79.10/11.14 | | $i(all_530_0) & $i(all_530_1) & $i(all_530_2) & $i(all_530_3) % 79.10/11.14 | | % 79.10/11.14 | | ALPHA: (167) implies: % 79.10/11.14 | | (168) ~ (all_530_0 = all_530_1) % 79.10/11.14 | | (169) sdtpldt0(xl, xm) = all_530_0 % 79.10/11.14 | | (170) sdtpldt0(xn, xm) = all_530_1 % 79.10/11.14 | | % 79.10/11.14 | | BETA: splitting (42) gives: % 79.10/11.14 | | % 79.10/11.14 | | Case 1: % 79.10/11.14 | | | % 79.10/11.14 | | | (171) sz10 = sz00 % 79.10/11.14 | | | % 79.10/11.14 | | | REDUCE: (2), (171) imply: % 79.10/11.14 | | | (172) $false % 79.10/11.14 | | | % 79.10/11.14 | | | CLOSE: (172) is inconsistent. % 79.10/11.14 | | | % 79.10/11.14 | | Case 2: % 79.10/11.14 | | | % 79.10/11.14 | | | (173) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( ~ (v3 = % 79.10/11.14 | | | v2) & ~ (v1 = v0) & sdtpldt0(all_24_0, sz10) = v0 & % 79.10/11.14 | | | sdtpldt0(all_24_0, sz00) = v1 & sdtpldt0(sz10, all_24_0) = v2 & % 79.10/11.14 | | | sdtpldt0(sz00, all_24_0) = v3 & $i(v3) & $i(v2) & $i(v1) & % 79.10/11.14 | | | $i(v0)) % 79.10/11.14 | | | % 79.10/11.14 | | | DELTA: instantiating (173) with fresh symbols all_550_0, all_550_1, % 79.10/11.14 | | | all_550_2, all_550_3 gives: % 79.10/11.14 | | | (174) ~ (all_550_0 = all_550_1) & ~ (all_550_2 = all_550_3) & % 79.10/11.14 | | | sdtpldt0(all_24_0, sz10) = all_550_3 & sdtpldt0(all_24_0, sz00) = % 79.10/11.14 | | | all_550_2 & sdtpldt0(sz10, all_24_0) = all_550_1 & sdtpldt0(sz00, % 79.10/11.14 | | | all_24_0) = all_550_0 & $i(all_550_0) & $i(all_550_1) & % 79.10/11.14 | | | $i(all_550_2) & $i(all_550_3) % 79.10/11.14 | | | % 79.10/11.14 | | | ALPHA: (174) implies: % 79.10/11.14 | | | (175) $i(all_550_2) % 79.10/11.14 | | | (176) sdtpldt0(all_24_0, sz00) = all_550_2 % 79.10/11.14 | | | % 79.10/11.14 | | | BETA: splitting (41) gives: % 79.10/11.14 | | | % 79.10/11.14 | | | Case 1: % 79.10/11.14 | | | | % 79.10/11.14 | | | | (177) sz10 = sz00 % 79.10/11.14 | | | | % 79.10/11.14 | | | | REDUCE: (2), (177) imply: % 79.10/11.14 | | | | (178) $false % 79.10/11.14 | | | | % 79.10/11.14 | | | | CLOSE: (178) is inconsistent. % 79.10/11.14 | | | | % 79.10/11.14 | | | Case 2: % 79.10/11.14 | | | | % 79.10/11.14 | | | | (179) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( ~ (v3 % 79.10/11.14 | | | | = v2) & ~ (v1 = v0) & sdtpldt0(all_24_0, sz10) = v1 & % 79.10/11.14 | | | | sdtpldt0(all_24_0, sz00) = v0 & sdtpldt0(sz10, all_24_0) = v3 % 79.10/11.14 | | | | & sdtpldt0(sz00, all_24_0) = v2 & $i(v3) & $i(v2) & $i(v1) & % 79.10/11.14 | | | | $i(v0)) % 79.10/11.14 | | | | % 79.10/11.14 | | | | DELTA: instantiating (179) with fresh symbols all_565_0, all_565_1, % 79.10/11.14 | | | | all_565_2, all_565_3 gives: % 79.10/11.14 | | | | (180) ~ (all_565_0 = all_565_1) & ~ (all_565_2 = all_565_3) & % 79.10/11.14 | | | | sdtpldt0(all_24_0, sz10) = all_565_2 & sdtpldt0(all_24_0, sz00) % 79.10/11.14 | | | | = all_565_3 & sdtpldt0(sz10, all_24_0) = all_565_0 & % 79.10/11.14 | | | | sdtpldt0(sz00, all_24_0) = all_565_1 & $i(all_565_0) & % 79.10/11.14 | | | | $i(all_565_1) & $i(all_565_2) & $i(all_565_3) % 79.10/11.14 | | | | % 79.10/11.14 | | | | ALPHA: (180) implies: % 79.10/11.14 | | | | (181) sdtpldt0(all_24_0, sz00) = all_565_3 % 79.10/11.14 | | | | % 79.10/11.14 | | | | BETA: splitting (48) gives: % 79.10/11.14 | | | | % 79.10/11.14 | | | | Case 1: % 79.10/11.14 | | | | | % 79.10/11.14 | | | | | (182) xn = xl % 79.10/11.14 | | | | | % 79.10/11.14 | | | | | REDUCE: (28), (182) imply: % 79.10/11.14 | | | | | (183) $false % 79.10/11.14 | | | | | % 79.10/11.14 | | | | | CLOSE: (183) is inconsistent. % 79.10/11.14 | | | | | % 79.50/11.14 | | | | Case 2: % 79.50/11.14 | | | | | % 79.50/11.14 | | | | | (184) ? [v0: any] : ? [v1: any] : ? [v2: $i] : ? [v3: $i] : ? % 79.50/11.14 | | | | | [v4: $i] : (sdtpldt0(all_24_0, xn) = v2 & sdtpldt0(all_24_0, % 79.50/11.14 | | | | | xl) = v3 & sdtpldt0(xn, all_24_0) = v4 & % 79.50/11.14 | | | | | aNaturalNumber0(all_24_0) = v0 & aNaturalNumber0(xl) = v1 & % 79.50/11.14 | | | | | $i(v4) & $i(v3) & $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) | ( ~ % 79.50/11.14 | | | | | (v4 = xn) & ~ (v3 = v2)))) % 79.50/11.14 | | | | | % 79.50/11.14 | | | | | DELTA: instantiating (184) with fresh symbols all_600_0, all_600_1, % 79.50/11.14 | | | | | all_600_2, all_600_3, all_600_4 gives: % 79.50/11.14 | | | | | (185) sdtpldt0(all_24_0, xn) = all_600_2 & sdtpldt0(all_24_0, xl) = % 79.50/11.14 | | | | | all_600_1 & sdtpldt0(xn, all_24_0) = all_600_0 & % 79.50/11.14 | | | | | aNaturalNumber0(all_24_0) = all_600_4 & aNaturalNumber0(xl) = % 79.50/11.14 | | | | | all_600_3 & $i(all_600_0) & $i(all_600_1) & $i(all_600_2) & ( % 79.50/11.14 | | | | | ~ (all_600_3 = 0) | ~ (all_600_4 = 0) | ( ~ (all_600_0 = % 79.50/11.14 | | | | | xn) & ~ (all_600_1 = all_600_2))) % 79.50/11.14 | | | | | % 79.50/11.14 | | | | | ALPHA: (185) implies: % 79.50/11.14 | | | | | (186) aNaturalNumber0(xl) = all_600_3 % 79.50/11.14 | | | | | (187) aNaturalNumber0(all_24_0) = all_600_4 % 79.50/11.14 | | | | | % 79.50/11.14 | | | | | BETA: splitting (49) gives: % 79.50/11.14 | | | | | % 79.50/11.14 | | | | | Case 1: % 79.50/11.14 | | | | | | % 79.50/11.14 | | | | | | (188) xn = xl % 79.50/11.14 | | | | | | % 79.50/11.14 | | | | | | REDUCE: (28), (188) imply: % 79.50/11.14 | | | | | | (189) $false % 79.50/11.14 | | | | | | % 79.50/11.14 | | | | | | CLOSE: (189) is inconsistent. % 79.50/11.14 | | | | | | % 79.50/11.14 | | | | | Case 2: % 79.50/11.14 | | | | | | % 79.50/11.15 | | | | | | (190) ? [v0: any] : ? [v1: any] : ? [v2: $i] : ? [v3: $i] : % 79.50/11.15 | | | | | | ? [v4: $i] : (sdtpldt0(all_24_0, xn) = v3 & % 79.50/11.15 | | | | | | sdtpldt0(all_24_0, xl) = v2 & sdtpldt0(xn, all_24_0) = v4 % 79.50/11.15 | | | | | | & aNaturalNumber0(all_24_0) = v0 & aNaturalNumber0(xl) = % 79.50/11.15 | | | | | | v1 & $i(v4) & $i(v3) & $i(v2) & ( ~ (v1 = 0) | ~ (v0 = % 79.50/11.15 | | | | | | 0) | ( ~ (v4 = xn) & ~ (v3 = v2)))) % 79.50/11.15 | | | | | | % 79.50/11.15 | | | | | | DELTA: instantiating (190) with fresh symbols all_605_0, all_605_1, % 79.50/11.15 | | | | | | all_605_2, all_605_3, all_605_4 gives: % 79.50/11.15 | | | | | | (191) sdtpldt0(all_24_0, xn) = all_605_1 & sdtpldt0(all_24_0, xl) % 79.50/11.15 | | | | | | = all_605_2 & sdtpldt0(xn, all_24_0) = all_605_0 & % 79.50/11.15 | | | | | | aNaturalNumber0(all_24_0) = all_605_4 & aNaturalNumber0(xl) % 79.50/11.15 | | | | | | = all_605_3 & $i(all_605_0) & $i(all_605_1) & $i(all_605_2) % 79.50/11.15 | | | | | | & ( ~ (all_605_3 = 0) | ~ (all_605_4 = 0) | ( ~ (all_605_0 % 79.50/11.15 | | | | | | = xn) & ~ (all_605_1 = all_605_2))) % 79.50/11.15 | | | | | | % 79.50/11.15 | | | | | | ALPHA: (191) implies: % 79.50/11.15 | | | | | | (192) aNaturalNumber0(xl) = all_605_3 % 79.50/11.15 | | | | | | (193) aNaturalNumber0(all_24_0) = all_605_4 % 79.50/11.15 | | | | | | % 79.50/11.15 | | | | | | BETA: splitting (39) gives: % 79.50/11.15 | | | | | | % 79.50/11.15 | | | | | | Case 1: % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | (194) xn = xl % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | REDUCE: (28), (194) imply: % 79.50/11.15 | | | | | | | (195) $false % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | CLOSE: (195) is inconsistent. % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | Case 2: % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_484_1, all_496_3, xl, % 79.50/11.15 | | | | | | | simplifying with (98), (121) gives: % 79.50/11.15 | | | | | | | (196) all_496_3 = all_484_1 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_482_1, all_496_3, xl, % 79.50/11.15 | | | | | | | simplifying with (95), (121) gives: % 79.50/11.15 | | | | | | | (197) all_496_3 = all_482_1 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_480_2, all_496_3, xl, % 79.50/11.15 | | | | | | | simplifying with (92), (121) gives: % 79.50/11.15 | | | | | | | (198) all_496_3 = all_480_2 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_306_1, all_496_3, xl, % 79.50/11.15 | | | | | | | simplifying with (78), (121) gives: % 79.50/11.15 | | | | | | | (199) all_496_3 = all_306_1 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_496_3, all_498_3, xl, % 79.50/11.15 | | | | | | | simplifying with (121), (124) gives: % 79.50/11.15 | | | | | | | (200) all_498_3 = all_496_3 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_474_2, all_500_3, xl, % 79.50/11.15 | | | | | | | simplifying with (83), (127) gives: % 79.50/11.15 | | | | | | | (201) all_500_3 = all_474_2 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_498_3, all_502_3, xl, % 79.50/11.15 | | | | | | | simplifying with (124), (130) gives: % 79.50/11.15 | | | | | | | (202) all_502_3 = all_498_3 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_476_1, all_502_3, xl, % 79.50/11.15 | | | | | | | simplifying with (86), (130) gives: % 79.50/11.15 | | | | | | | (203) all_502_3 = all_476_1 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_500_3, all_506_3, xl, % 79.50/11.15 | | | | | | | simplifying with (127), (136) gives: % 79.50/11.15 | | | | | | | (204) all_506_3 = all_500_3 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_484_1, all_506_3, xl, % 79.50/11.15 | | | | | | | simplifying with (98), (136) gives: % 79.50/11.15 | | | | | | | (205) all_506_3 = all_484_1 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with 0, all_510_3, xl, simplifying % 79.50/11.15 | | | | | | | with (17), (141) gives: % 79.50/11.15 | | | | | | | (206) all_510_3 = 0 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_510_3, all_514_3, xl, % 79.50/11.15 | | | | | | | simplifying with (141), (147) gives: % 79.50/11.15 | | | | | | | (207) all_514_3 = all_510_3 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_508_3, all_514_3, xl, % 79.50/11.15 | | | | | | | simplifying with (138), (147) gives: % 79.50/11.15 | | | | | | | (208) all_514_3 = all_508_3 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_494_3, all_514_3, xl, % 79.50/11.15 | | | | | | | simplifying with (118), (147) gives: % 79.50/11.15 | | | | | | | (209) all_514_3 = all_494_3 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_306_1, all_514_3, xl, % 79.50/11.15 | | | | | | | simplifying with (78), (147) gives: % 79.50/11.15 | | | | | | | (210) all_514_3 = all_306_1 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_504_3, all_516_3, xl, % 79.50/11.15 | | | | | | | simplifying with (133), (149) gives: % 79.50/11.15 | | | | | | | (211) all_516_3 = all_504_3 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_498_3, all_516_3, xl, % 79.50/11.15 | | | | | | | simplifying with (124), (149) gives: % 79.50/11.15 | | | | | | | (212) all_516_3 = all_498_3 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_516_3, all_522_3, xl, % 79.50/11.15 | | | | | | | simplifying with (149), (155) gives: % 79.50/11.15 | | | | | | | (213) all_522_3 = all_516_3 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_520_4, all_524_2, xl, % 79.50/11.15 | | | | | | | simplifying with (151), (162) gives: % 79.50/11.15 | | | | | | | (214) all_524_2 = all_520_4 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_486_2, all_524_2, xl, % 79.50/11.15 | | | | | | | simplifying with (102), (162) gives: % 79.50/11.15 | | | | | | | (215) all_524_2 = all_486_2 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_522_3, all_600_3, xl, % 79.50/11.15 | | | | | | | simplifying with (155), (186) gives: % 79.50/11.15 | | | | | | | (216) all_600_3 = all_522_3 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_278_2, all_600_3, xl, % 79.50/11.15 | | | | | | | simplifying with (76), (186) gives: % 79.50/11.15 | | | | | | | (217) all_600_3 = all_278_2 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_524_2, all_605_3, xl, % 79.50/11.15 | | | | | | | simplifying with (162), (192) gives: % 79.50/11.15 | | | | | | | (218) all_605_3 = all_524_2 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_512_3, all_605_3, xl, % 79.50/11.15 | | | | | | | simplifying with (144), (192) gives: % 79.50/11.15 | | | | | | | (219) all_605_3 = all_512_3 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_506_3, all_605_3, xl, % 79.50/11.15 | | | | | | | simplifying with (136), (192) gives: % 79.50/11.15 | | | | | | | (220) all_605_3 = all_506_3 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with 0, all_494_2, xn, simplifying % 79.50/11.15 | | | | | | | with (18), (119) gives: % 79.50/11.15 | | | | | | | (221) all_494_2 = 0 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_500_2, all_502_2, xn, % 79.50/11.15 | | | | | | | simplifying with (128), (131) gives: % 79.50/11.15 | | | | | | | (222) all_502_2 = all_500_2 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_496_2, all_502_2, xn, % 79.50/11.15 | | | | | | | simplifying with (122), (131) gives: % 79.50/11.15 | | | | | | | (223) all_502_2 = all_496_2 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_494_2, all_502_2, xn, % 79.50/11.15 | | | | | | | simplifying with (119), (131) gives: % 79.50/11.15 | | | | | | | (224) all_502_2 = all_494_2 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_500_2, all_504_2, xn, % 79.50/11.15 | | | | | | | simplifying with (128), (134) gives: % 79.50/11.15 | | | | | | | (225) all_504_2 = all_500_2 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_490_1, all_504_2, xn, % 79.50/11.15 | | | | | | | simplifying with (110), (134) gives: % 79.50/11.15 | | | | | | | (226) all_504_2 = all_490_1 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_494_2, all_510_2, xn, % 79.50/11.15 | | | | | | | simplifying with (119), (142) gives: % 79.50/11.15 | | | | | | | (227) all_510_2 = all_494_2 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_492_2, all_510_2, xn, % 79.50/11.15 | | | | | | | simplifying with (113), (142) gives: % 79.50/11.15 | | | | | | | (228) all_510_2 = all_492_2 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_488_2, all_510_2, xn, % 79.50/11.15 | | | | | | | simplifying with (107), (142) gives: % 79.50/11.15 | | | | | | | (229) all_510_2 = all_488_2 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_510_2, all_512_2, xn, % 79.50/11.15 | | | | | | | simplifying with (142), (145) gives: % 79.50/11.15 | | | | | | | (230) all_512_2 = all_510_2 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_508_2, all_512_2, xn, % 79.50/11.15 | | | | | | | simplifying with (139), (145) gives: % 79.50/11.15 | | | | | | | (231) all_512_2 = all_508_2 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_510_2, all_524_1, xn, % 79.50/11.15 | | | | | | | simplifying with (142), (163) gives: % 79.50/11.15 | | | | | | | (232) all_524_1 = all_510_2 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_498_2, all_524_1, xn, % 79.50/11.15 | | | | | | | simplifying with (125), (163) gives: % 79.50/11.15 | | | | | | | (233) all_524_1 = all_498_2 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with 0, all_308_1, xm, simplifying % 79.50/11.15 | | | | | | | with (20), (81) gives: % 79.50/11.15 | | | | | | | (234) all_308_1 = 0 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_308_1, all_478_2, xm, % 79.50/11.15 | | | | | | | simplifying with (81), (89) gives: % 79.50/11.15 | | | | | | | (235) all_478_2 = all_308_1 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_478_2, all_482_2, xm, % 79.50/11.15 | | | | | | | simplifying with (89), (96) gives: % 79.50/11.15 | | | | | | | (236) all_482_2 = all_478_2 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_482_2, all_484_2, xm, % 79.50/11.15 | | | | | | | simplifying with (96), (99) gives: % 79.50/11.15 | | | | | | | (237) all_484_2 = all_482_2 % 79.50/11.15 | | | | | | | % 79.50/11.15 | | | | | | | GROUND_INST: instantiating (25) with all_482_2, all_486_1, xm, % 79.50/11.15 | | | | | | | simplifying with (96), (103) gives: % 79.50/11.16 | | | | | | | (238) all_486_1 = all_482_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (25) with all_484_2, all_488_1, xm, % 79.50/11.16 | | | | | | | simplifying with (99), (108) gives: % 79.50/11.16 | | | | | | | (239) all_488_1 = all_484_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (25) with all_488_1, all_490_2, xm, % 79.50/11.16 | | | | | | | simplifying with (108), (111) gives: % 79.50/11.16 | | | | | | | (240) all_490_2 = all_488_1 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (25) with all_486_1, all_492_1, xm, % 79.50/11.16 | | | | | | | simplifying with (103), (114) gives: % 79.50/11.16 | | | | | | | (241) all_492_1 = all_486_1 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (25) with all_480_1, all_492_1, xm, % 79.50/11.16 | | | | | | | simplifying with (93), (114) gives: % 79.50/11.16 | | | | | | | (242) all_492_1 = all_480_1 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (25) with all_520_2, all_522_4, xm, % 79.50/11.16 | | | | | | | simplifying with (152), (156) gives: % 79.50/11.16 | | | | | | | (243) all_522_4 = all_520_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (25) with all_490_2, all_522_4, xm, % 79.50/11.16 | | | | | | | simplifying with (111), (156) gives: % 79.50/11.16 | | | | | | | (244) all_522_4 = all_490_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (25) with all_306_2, all_522_4, xm, % 79.50/11.16 | | | | | | | simplifying with (79), (156) gives: % 79.50/11.16 | | | | | | | (245) all_522_4 = all_306_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (25) with all_522_2, all_600_4, % 79.50/11.16 | | | | | | | all_24_0, simplifying with (157), (187) gives: % 79.50/11.16 | | | | | | | (246) all_600_4 = all_522_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (25) with all_520_3, all_600_4, % 79.50/11.16 | | | | | | | all_24_0, simplifying with (153), (187) gives: % 79.50/11.16 | | | | | | | (247) all_600_4 = all_520_3 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (25) with all_474_1, all_600_4, % 79.50/11.16 | | | | | | | all_24_0, simplifying with (84), (187) gives: % 79.50/11.16 | | | | | | | (248) all_600_4 = all_474_1 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (25) with 0, all_605_4, all_24_0, % 79.50/11.16 | | | | | | | simplifying with (30), (193) gives: % 79.50/11.16 | | | | | | | (249) all_605_4 = 0 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (25) with all_600_4, all_605_4, % 79.50/11.16 | | | | | | | all_24_0, simplifying with (187), (193) gives: % 79.50/11.16 | | | | | | | (250) all_605_4 = all_600_4 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (25) with all_476_2, all_605_4, % 79.50/11.16 | | | | | | | all_24_0, simplifying with (87), (193) gives: % 79.50/11.16 | | | | | | | (251) all_605_4 = all_476_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (26) with all_484_0, all_486_0, xm, xl, % 79.50/11.16 | | | | | | | simplifying with (100), (104) gives: % 79.50/11.16 | | | | | | | (252) all_486_0 = all_484_0 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (26) with all_26_2, all_530_0, xm, xl, % 79.50/11.16 | | | | | | | simplifying with (34), (169) gives: % 79.50/11.16 | | | | | | | (253) all_530_0 = all_26_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (26) with all_486_0, all_530_0, xm, xl, % 79.50/11.16 | | | | | | | simplifying with (104), (169) gives: % 79.50/11.16 | | | | | | | (254) all_530_0 = all_486_0 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (26) with all_26_1, all_492_0, xm, xn, % 79.50/11.16 | | | | | | | simplifying with (35), (115) gives: % 79.50/11.16 | | | | | | | (255) all_492_0 = all_26_1 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (26) with all_492_0, all_530_1, xm, xn, % 79.50/11.16 | | | | | | | simplifying with (115), (170) gives: % 79.50/11.16 | | | | | | | (256) all_530_1 = all_492_0 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (26) with all_478_0, all_530_1, xm, xn, % 79.50/11.16 | | | | | | | simplifying with (90), (170) gives: % 79.50/11.16 | | | | | | | (257) all_530_1 = all_478_0 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (26) with all_26_5, all_522_1, xl, xm, % 79.50/11.16 | | | | | | | simplifying with (36), (158) gives: % 79.50/11.16 | | | | | | | (258) all_522_1 = all_26_5 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (26) with all_550_2, all_565_3, sz00, % 79.50/11.16 | | | | | | | all_24_0, simplifying with (176), (181) gives: % 79.50/11.16 | | | | | | | (259) all_565_3 = all_550_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | GROUND_INST: instantiating (26) with all_24_0, all_565_3, sz00, % 79.50/11.16 | | | | | | | all_24_0, simplifying with (44), (181) gives: % 79.50/11.16 | | | | | | | (260) all_565_3 = all_24_0 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (219), (220) imply: % 79.50/11.16 | | | | | | | (261) all_512_3 = all_506_3 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (218), (219) imply: % 79.50/11.16 | | | | | | | (262) all_524_2 = all_512_3 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | SIMP: (262) implies: % 79.50/11.16 | | | | | | | (263) all_524_2 = all_512_3 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (250), (251) imply: % 79.50/11.16 | | | | | | | (264) all_600_4 = all_476_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | SIMP: (264) implies: % 79.50/11.16 | | | | | | | (265) all_600_4 = all_476_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (249), (251) imply: % 79.50/11.16 | | | | | | | (266) all_476_2 = 0 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (216), (217) imply: % 79.50/11.16 | | | | | | | (267) all_522_3 = all_278_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | SIMP: (267) implies: % 79.50/11.16 | | | | | | | (268) all_522_3 = all_278_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (246), (248) imply: % 79.50/11.16 | | | | | | | (269) all_522_2 = all_474_1 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (246), (247) imply: % 79.50/11.16 | | | | | | | (270) all_522_2 = all_520_3 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (246), (265) imply: % 79.50/11.16 | | | | | | | (271) all_522_2 = all_476_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (259), (260) imply: % 79.50/11.16 | | | | | | | (272) all_550_2 = all_24_0 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (253), (254) imply: % 79.50/11.16 | | | | | | | (273) all_486_0 = all_26_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | SIMP: (273) implies: % 79.50/11.16 | | | | | | | (274) all_486_0 = all_26_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (256), (257) imply: % 79.50/11.16 | | | | | | | (275) all_492_0 = all_478_0 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | SIMP: (275) implies: % 79.50/11.16 | | | | | | | (276) all_492_0 = all_478_0 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (232), (233) imply: % 79.50/11.16 | | | | | | | (277) all_510_2 = all_498_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | SIMP: (277) implies: % 79.50/11.16 | | | | | | | (278) all_510_2 = all_498_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (214), (215) imply: % 79.50/11.16 | | | | | | | (279) all_520_4 = all_486_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (214), (263) imply: % 79.50/11.16 | | | | | | | (280) all_520_4 = all_512_3 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (269), (270) imply: % 79.50/11.16 | | | | | | | (281) all_520_3 = all_474_1 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (270), (271) imply: % 79.50/11.16 | | | | | | | (282) all_520_3 = all_476_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (213), (268) imply: % 79.50/11.16 | | | | | | | (283) all_516_3 = all_278_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | SIMP: (283) implies: % 79.50/11.16 | | | | | | | (284) all_516_3 = all_278_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (243), (245) imply: % 79.50/11.16 | | | | | | | (285) all_520_2 = all_306_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (243), (244) imply: % 79.50/11.16 | | | | | | | (286) all_520_2 = all_490_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (285), (286) imply: % 79.50/11.16 | | | | | | | (287) all_490_2 = all_306_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | SIMP: (287) implies: % 79.50/11.16 | | | | | | | (288) all_490_2 = all_306_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (281), (282) imply: % 79.50/11.16 | | | | | | | (289) all_476_2 = all_474_1 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | SIMP: (289) implies: % 79.50/11.16 | | | | | | | (290) all_476_2 = all_474_1 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (279), (280) imply: % 79.50/11.16 | | | | | | | (291) all_512_3 = all_486_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | SIMP: (291) implies: % 79.50/11.16 | | | | | | | (292) all_512_3 = all_486_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (211), (212) imply: % 79.50/11.16 | | | | | | | (293) all_504_3 = all_498_3 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (211), (284) imply: % 79.50/11.16 | | | | | | | (294) all_504_3 = all_278_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (208), (210) imply: % 79.50/11.16 | | | | | | | (295) all_508_3 = all_306_1 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (208), (209) imply: % 79.50/11.16 | | | | | | | (296) all_508_3 = all_494_3 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (207), (208) imply: % 79.50/11.16 | | | | | | | (297) all_510_3 = all_508_3 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | SIMP: (297) implies: % 79.50/11.16 | | | | | | | (298) all_510_3 = all_508_3 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (230), (231) imply: % 79.50/11.16 | | | | | | | (299) all_510_2 = all_508_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | SIMP: (299) implies: % 79.50/11.16 | | | | | | | (300) all_510_2 = all_508_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (261), (292) imply: % 79.50/11.16 | | | | | | | (301) all_506_3 = all_486_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | SIMP: (301) implies: % 79.50/11.16 | | | | | | | (302) all_506_3 = all_486_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (227), (300) imply: % 79.50/11.16 | | | | | | | (303) all_508_2 = all_494_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (228), (300) imply: % 79.50/11.16 | | | | | | | (304) all_508_2 = all_492_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (278), (300) imply: % 79.50/11.16 | | | | | | | (305) all_508_2 = all_498_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (229), (300) imply: % 79.50/11.16 | | | | | | | (306) all_508_2 = all_488_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (206), (298) imply: % 79.50/11.16 | | | | | | | (307) all_508_3 = 0 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | SIMP: (307) implies: % 79.50/11.16 | | | | | | | (308) all_508_3 = 0 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (303), (305) imply: % 79.50/11.16 | | | | | | | (309) all_498_2 = all_494_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (304), (305) imply: % 79.50/11.16 | | | | | | | (310) all_498_2 = all_492_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (305), (306) imply: % 79.50/11.16 | | | | | | | (311) all_498_2 = all_488_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (296), (308) imply: % 79.50/11.16 | | | | | | | (312) all_494_3 = 0 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (295), (296) imply: % 79.50/11.16 | | | | | | | (313) all_494_3 = all_306_1 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (205), (302) imply: % 79.50/11.16 | | | | | | | (314) all_486_2 = all_484_1 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (204), (302) imply: % 79.50/11.16 | | | | | | | (315) all_500_3 = all_486_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | SIMP: (315) implies: % 79.50/11.16 | | | | | | | (316) all_500_3 = all_486_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (225), (226) imply: % 79.50/11.16 | | | | | | | (317) all_500_2 = all_490_1 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | SIMP: (317) implies: % 79.50/11.16 | | | | | | | (318) all_500_2 = all_490_1 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | COMBINE_EQS: (293), (294) imply: % 79.50/11.16 | | | | | | | (319) all_498_3 = all_278_2 % 79.50/11.16 | | | | | | | % 79.50/11.16 | | | | | | | SIMP: (319) implies: % 79.50/11.17 | | | | | | | (320) all_498_3 = all_278_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (222), (223) imply: % 79.50/11.17 | | | | | | | (321) all_500_2 = all_496_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (321) implies: % 79.50/11.17 | | | | | | | (322) all_500_2 = all_496_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (223), (224) imply: % 79.50/11.17 | | | | | | | (323) all_496_2 = all_494_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (202), (203) imply: % 79.50/11.17 | | | | | | | (324) all_498_3 = all_476_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (324) implies: % 79.50/11.17 | | | | | | | (325) all_498_3 = all_476_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (318), (322) imply: % 79.50/11.17 | | | | | | | (326) all_496_2 = all_490_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (326) implies: % 79.50/11.17 | | | | | | | (327) all_496_2 = all_490_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (201), (316) imply: % 79.50/11.17 | | | | | | | (328) all_486_2 = all_474_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (328) implies: % 79.50/11.17 | | | | | | | (329) all_486_2 = all_474_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (309), (310) imply: % 79.50/11.17 | | | | | | | (330) all_494_2 = all_492_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (330) implies: % 79.50/11.17 | | | | | | | (331) all_494_2 = all_492_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (310), (311) imply: % 79.50/11.17 | | | | | | | (332) all_492_2 = all_488_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (200), (325) imply: % 79.50/11.17 | | | | | | | (333) all_496_3 = all_476_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (333) implies: % 79.50/11.17 | | | | | | | (334) all_496_3 = all_476_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (320), (325) imply: % 79.50/11.17 | | | | | | | (335) all_476_1 = all_278_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (323), (327) imply: % 79.50/11.17 | | | | | | | (336) all_494_2 = all_490_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (336) implies: % 79.50/11.17 | | | | | | | (337) all_494_2 = all_490_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (196), (197) imply: % 79.50/11.17 | | | | | | | (338) all_484_1 = all_482_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (338) implies: % 79.50/11.17 | | | | | | | (339) all_484_1 = all_482_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (197), (198) imply: % 79.50/11.17 | | | | | | | (340) all_482_1 = all_480_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (197), (199) imply: % 79.50/11.17 | | | | | | | (341) all_482_1 = all_306_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (197), (334) imply: % 79.50/11.17 | | | | | | | (342) all_482_1 = all_476_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (221), (337) imply: % 79.50/11.17 | | | | | | | (343) all_490_1 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (331), (337) imply: % 79.50/11.17 | | | | | | | (344) all_492_2 = all_490_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (344) implies: % 79.50/11.17 | | | | | | | (345) all_492_2 = all_490_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (312), (313) imply: % 79.50/11.17 | | | | | | | (346) all_306_1 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (346) implies: % 79.50/11.17 | | | | | | | (347) all_306_1 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (255), (276) imply: % 79.50/11.17 | | | | | | | (348) all_478_0 = all_26_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (241), (242) imply: % 79.50/11.17 | | | | | | | (349) all_486_1 = all_480_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (349) implies: % 79.50/11.17 | | | | | | | (350) all_486_1 = all_480_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (332), (345) imply: % 79.50/11.17 | | | | | | | (351) all_490_1 = all_488_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (351) implies: % 79.50/11.17 | | | | | | | (352) all_490_1 = all_488_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (343), (352) imply: % 79.50/11.17 | | | | | | | (353) all_488_2 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (353) implies: % 79.50/11.17 | | | | | | | (354) all_488_2 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (240), (288) imply: % 79.50/11.17 | | | | | | | (355) all_488_1 = all_306_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (355) implies: % 79.50/11.17 | | | | | | | (356) all_488_1 = all_306_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (239), (356) imply: % 79.50/11.17 | | | | | | | (357) all_484_2 = all_306_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (357) implies: % 79.50/11.17 | | | | | | | (358) all_484_2 = all_306_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (252), (274) imply: % 79.50/11.17 | | | | | | | (359) all_484_0 = all_26_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (238), (350) imply: % 79.50/11.17 | | | | | | | (360) all_482_2 = all_480_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (360) implies: % 79.50/11.17 | | | | | | | (361) all_482_2 = all_480_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (314), (329) imply: % 79.50/11.17 | | | | | | | (362) all_484_1 = all_474_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (362) implies: % 79.50/11.17 | | | | | | | (363) all_484_1 = all_474_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (339), (363) imply: % 79.50/11.17 | | | | | | | (364) all_482_1 = all_474_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (364) implies: % 79.50/11.17 | | | | | | | (365) all_482_1 = all_474_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (237), (358) imply: % 79.50/11.17 | | | | | | | (366) all_482_2 = all_306_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (366) implies: % 79.50/11.17 | | | | | | | (367) all_482_2 = all_306_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (340), (342) imply: % 79.50/11.17 | | | | | | | (368) all_480_2 = all_476_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (340), (341) imply: % 79.50/11.17 | | | | | | | (369) all_480_2 = all_306_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (340), (365) imply: % 79.50/11.17 | | | | | | | (370) all_480_2 = all_474_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (236), (361) imply: % 79.50/11.17 | | | | | | | (371) all_480_1 = all_478_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (361), (367) imply: % 79.50/11.17 | | | | | | | (372) all_480_1 = all_306_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (371), (372) imply: % 79.50/11.17 | | | | | | | (373) all_478_2 = all_306_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (373) implies: % 79.50/11.17 | | | | | | | (374) all_478_2 = all_306_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (369), (370) imply: % 79.50/11.17 | | | | | | | (375) all_474_2 = all_306_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (368), (370) imply: % 79.50/11.17 | | | | | | | (376) all_476_1 = all_474_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (376) implies: % 79.50/11.17 | | | | | | | (377) all_476_1 = all_474_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (235), (374) imply: % 79.50/11.17 | | | | | | | (378) all_308_1 = all_306_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (378) implies: % 79.50/11.17 | | | | | | | (379) all_308_1 = all_306_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (335), (377) imply: % 79.50/11.17 | | | | | | | (380) all_474_2 = all_278_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (380) implies: % 79.50/11.17 | | | | | | | (381) all_474_2 = all_278_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (266), (290) imply: % 79.50/11.17 | | | | | | | (382) all_474_1 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (375), (381) imply: % 79.50/11.17 | | | | | | | (383) all_306_1 = all_278_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (383) implies: % 79.50/11.17 | | | | | | | (384) all_306_1 = all_278_2 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (234), (379) imply: % 79.50/11.17 | | | | | | | (385) all_306_2 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (347), (384) imply: % 79.50/11.17 | | | | | | | (386) all_278_2 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (381), (386) imply: % 79.50/11.17 | | | | | | | (387) all_474_2 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (372), (385) imply: % 79.50/11.17 | | | | | | | (388) all_480_1 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (329), (387) imply: % 79.50/11.17 | | | | | | | (389) all_486_2 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (350), (388) imply: % 79.50/11.17 | | | | | | | (390) all_486_1 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (332), (354) imply: % 79.50/11.17 | | | | | | | (391) all_492_2 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (242), (388) imply: % 79.50/11.17 | | | | | | | (392) all_492_1 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (281), (382) imply: % 79.50/11.17 | | | | | | | (393) all_520_3 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (285), (385) imply: % 79.50/11.17 | | | | | | | (394) all_520_2 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (243), (394) imply: % 79.50/11.17 | | | | | | | (395) all_522_4 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (268), (386) imply: % 79.50/11.17 | | | | | | | (396) all_522_3 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (270), (393) imply: % 79.50/11.17 | | | | | | | (397) all_522_2 = 0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | COMBINE_EQS: (257), (348) imply: % 79.50/11.17 | | | | | | | (398) all_530_1 = all_26_1 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | REDUCE: (168), (253), (398) imply: % 79.50/11.17 | | | | | | | (399) ~ (all_26_1 = all_26_2) % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | SIMP: (399) implies: % 79.50/11.17 | | | | | | | (400) ~ (all_26_1 = all_26_2) % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | REDUCE: (159), (258) imply: % 79.50/11.17 | | | | | | | (401) sdtpldt0(all_26_5, all_24_0) = all_522_0 % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | BETA: splitting (116) gives: % 79.50/11.17 | | | | | | | % 79.50/11.17 | | | | | | | Case 1: % 79.50/11.17 | | | | | | | | % 79.50/11.17 | | | | | | | | (402) ~ (all_492_1 = 0) % 79.50/11.17 | | | | | | | | % 79.50/11.17 | | | | | | | | REDUCE: (392), (402) imply: % 79.50/11.17 | | | | | | | | (403) $false % 79.50/11.17 | | | | | | | | % 79.50/11.17 | | | | | | | | CLOSE: (403) is inconsistent. % 79.50/11.17 | | | | | | | | % 79.50/11.17 | | | | | | | Case 2: % 79.50/11.17 | | | | | | | | % 79.50/11.17 | | | | | | | | (404) ~ (all_492_2 = 0) | all_492_0 = all_26_4 % 79.50/11.17 | | | | | | | | % 79.50/11.17 | | | | | | | | BETA: splitting (404) gives: % 79.50/11.17 | | | | | | | | % 79.50/11.17 | | | | | | | | Case 1: % 79.50/11.17 | | | | | | | | | % 79.50/11.17 | | | | | | | | | (405) ~ (all_492_2 = 0) % 79.50/11.17 | | | | | | | | | % 79.50/11.17 | | | | | | | | | REDUCE: (391), (405) imply: % 79.50/11.17 | | | | | | | | | (406) $false % 79.50/11.17 | | | | | | | | | % 79.50/11.17 | | | | | | | | | CLOSE: (406) is inconsistent. % 79.50/11.17 | | | | | | | | | % 79.50/11.17 | | | | | | | | Case 2: % 79.50/11.17 | | | | | | | | | % 79.50/11.17 | | | | | | | | | (407) all_492_0 = all_26_4 % 79.50/11.17 | | | | | | | | | % 79.50/11.17 | | | | | | | | | COMBINE_EQS: (255), (407) imply: % 79.50/11.17 | | | | | | | | | (408) all_26_1 = all_26_4 % 79.50/11.17 | | | | | | | | | % 79.50/11.17 | | | | | | | | | REDUCE: (400), (408) imply: % 79.50/11.17 | | | | | | | | | (409) ~ (all_26_2 = all_26_4) % 79.50/11.17 | | | | | | | | | % 79.50/11.17 | | | | | | | | | SIMP: (409) implies: % 79.50/11.17 | | | | | | | | | (410) ~ (all_26_2 = all_26_4) % 79.50/11.17 | | | | | | | | | % 79.50/11.17 | | | | | | | | | BETA: splitting (160) gives: % 79.50/11.17 | | | | | | | | | % 79.50/11.17 | | | | | | | | | Case 1: % 79.50/11.17 | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | (411) ~ (all_522_2 = 0) % 79.50/11.17 | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | REDUCE: (397), (411) imply: % 79.50/11.17 | | | | | | | | | | (412) $false % 79.50/11.17 | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | CLOSE: (412) is inconsistent. % 79.50/11.17 | | | | | | | | | | % 79.50/11.17 | | | | | | | | | Case 2: % 79.50/11.17 | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | (413) ~ (all_522_3 = 0) | ~ (all_522_4 = 0) | all_522_0 % 79.50/11.17 | | | | | | | | | | = all_26_4 % 79.50/11.17 | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | BETA: splitting (413) gives: % 79.50/11.17 | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | Case 1: % 79.50/11.17 | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | (414) ~ (all_522_3 = 0) % 79.50/11.17 | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | REDUCE: (396), (414) imply: % 79.50/11.17 | | | | | | | | | | | (415) $false % 79.50/11.17 | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | CLOSE: (415) is inconsistent. % 79.50/11.17 | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | Case 2: % 79.50/11.17 | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | (416) ~ (all_522_4 = 0) | all_522_0 = all_26_4 % 79.50/11.17 | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | BETA: splitting (105) gives: % 79.50/11.17 | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | Case 1: % 79.50/11.17 | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | (417) ~ (all_486_1 = 0) % 79.50/11.17 | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | REDUCE: (390), (417) imply: % 79.50/11.17 | | | | | | | | | | | | (418) $false % 79.50/11.17 | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | CLOSE: (418) is inconsistent. % 79.50/11.17 | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | Case 2: % 79.50/11.17 | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | (419) ~ (all_486_2 = 0) | all_486_0 = all_26_5 % 79.50/11.17 | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | BETA: splitting (416) gives: % 79.50/11.17 | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | Case 1: % 79.50/11.17 | | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | | (420) ~ (all_522_4 = 0) % 79.50/11.17 | | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | | REDUCE: (395), (420) imply: % 79.50/11.17 | | | | | | | | | | | | | (421) $false % 79.50/11.17 | | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | | CLOSE: (421) is inconsistent. % 79.50/11.17 | | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | Case 2: % 79.50/11.17 | | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | | (422) all_522_0 = all_26_4 % 79.50/11.17 | | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | | REDUCE: (401), (422) imply: % 79.50/11.17 | | | | | | | | | | | | | (423) sdtpldt0(all_26_5, all_24_0) = all_26_4 % 79.50/11.17 | | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | | BETA: splitting (419) gives: % 79.50/11.17 | | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | | Case 1: % 79.50/11.17 | | | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | | | (424) ~ (all_486_2 = 0) % 79.50/11.17 | | | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | | | REDUCE: (389), (424) imply: % 79.50/11.17 | | | | | | | | | | | | | | (425) $false % 79.50/11.17 | | | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | | | CLOSE: (425) is inconsistent. % 79.50/11.17 | | | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | | Case 2: % 79.50/11.17 | | | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | | | (426) all_486_0 = all_26_5 % 79.50/11.17 | | | | | | | | | | | | | | % 79.50/11.17 | | | | | | | | | | | | | | COMBINE_EQS: (274), (426) imply: % 79.50/11.18 | | | | | | | | | | | | | | (427) all_26_2 = all_26_5 % 79.50/11.18 | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | REDUCE: (410), (427) imply: % 79.50/11.18 | | | | | | | | | | | | | | (428) ~ (all_26_4 = all_26_5) % 79.50/11.18 | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | SIMP: (428) implies: % 79.50/11.18 | | | | | | | | | | | | | | (429) ~ (all_26_4 = all_26_5) % 79.50/11.18 | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | BETA: splitting (38) gives: % 79.50/11.18 | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | Case 1: % 79.50/11.18 | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | (430) all_26_1 = all_26_2 % 79.50/11.18 | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | COMBINE_EQS: (408), (430) imply: % 79.50/11.18 | | | | | | | | | | | | | | | (431) all_26_2 = all_26_4 % 79.50/11.18 | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | SIMP: (431) implies: % 79.50/11.18 | | | | | | | | | | | | | | | (432) all_26_2 = all_26_4 % 79.50/11.18 | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | COMBINE_EQS: (427), (432) imply: % 79.50/11.18 | | | | | | | | | | | | | | | (433) all_26_4 = all_26_5 % 79.50/11.18 | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | SIMP: (433) implies: % 79.50/11.18 | | | | | | | | | | | | | | | (434) all_26_4 = all_26_5 % 79.50/11.18 | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | REDUCE: (429), (434) imply: % 79.50/11.18 | | | | | | | | | | | | | | | (435) $false % 79.50/11.18 | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | CLOSE: (435) is inconsistent. % 79.50/11.18 | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | Case 2: % 79.50/11.18 | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | (436) all_26_4 = all_26_5 | ( ~ (all_26_0 = 0) & ! [v0: % 79.50/11.18 | | | | | | | | | | | | | | | $i] : ( ~ (sdtpldt0(all_26_2, v0) = all_26_1) % 79.50/11.18 | | | | | | | | | | | | | | | | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 79.50/11.18 | | | | | | | | | | | | | | | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( % 79.50/11.18 | | | | | | | | | | | | | | | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) | ? % 79.50/11.18 | | | | | | | | | | | | | | | [v1: any] : ( ~ (v1 = all_26_1) & % 79.50/11.18 | | | | | | | | | | | | | | | sdtpldt0(all_26_2, v0) = v1 & $i(v1)))) | ( % 79.50/11.18 | | | | | | | | | | | | | | | ~ (all_26_3 = 0) & ! [v0: $i] : ( ~ % 79.50/11.18 | | | | | | | | | | | | | | | (sdtpldt0(all_26_5, v0) = all_26_4) | ~ % 79.50/11.18 | | | | | | | | | | | | | | | $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 79.50/11.18 | | | | | | | | | | | | | | | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( % 79.50/11.18 | | | | | | | | | | | | | | | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) | ? % 79.50/11.18 | | | | | | | | | | | | | | | [v1: any] : ( ~ (v1 = all_26_4) & % 79.50/11.18 | | | | | | | | | | | | | | | sdtpldt0(all_26_5, v0) = v1 & $i(v1)))) % 79.50/11.18 | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | BETA: splitting (436) gives: % 79.50/11.18 | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | Case 1: % 79.50/11.18 | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | (437) all_26_4 = all_26_5 % 79.50/11.18 | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | REDUCE: (429), (437) imply: % 79.50/11.18 | | | | | | | | | | | | | | | | (438) $false % 79.50/11.18 | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | CLOSE: (438) is inconsistent. % 79.50/11.18 | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | Case 2: % 79.50/11.18 | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | (439) ( ~ (all_26_0 = 0) & ! [v0: $i] : ( ~ % 79.50/11.18 | | | | | | | | | | | | | | | | (sdtpldt0(all_26_2, v0) = all_26_1) | ~ % 79.50/11.18 | | | | | | | | | | | | | | | | $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 79.50/11.18 | | | | | | | | | | | | | | | | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( % 79.50/11.18 | | | | | | | | | | | | | | | | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) | ? % 79.50/11.18 | | | | | | | | | | | | | | | | [v1: any] : ( ~ (v1 = all_26_1) & % 79.50/11.18 | | | | | | | | | | | | | | | | sdtpldt0(all_26_2, v0) = v1 & $i(v1)))) | ( % 79.50/11.18 | | | | | | | | | | | | | | | | ~ (all_26_3 = 0) & ! [v0: $i] : ( ~ % 79.50/11.18 | | | | | | | | | | | | | | | | (sdtpldt0(all_26_5, v0) = all_26_4) | ~ % 79.50/11.18 | | | | | | | | | | | | | | | | $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 79.50/11.18 | | | | | | | | | | | | | | | | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( % 79.50/11.18 | | | | | | | | | | | | | | | | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) | ? % 79.50/11.18 | | | | | | | | | | | | | | | | [v1: any] : ( ~ (v1 = all_26_4) & % 79.50/11.18 | | | | | | | | | | | | | | | | sdtpldt0(all_26_5, v0) = v1 & $i(v1)))) % 79.50/11.18 | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | BETA: splitting (439) gives: % 79.50/11.18 | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | Case 1: % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | | (440) ~ (all_26_0 = 0) & ! [v0: $i] : ( ~ % 79.50/11.18 | | | | | | | | | | | | | | | | | (sdtpldt0(all_26_2, v0) = all_26_1) | ~ $i(v0) % 79.50/11.18 | | | | | | | | | | | | | | | | | | ? [v1: int] : ( ~ (v1 = 0) & % 79.50/11.18 | | | | | | | | | | | | | | | | | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( ~ % 79.50/11.18 | | | | | | | | | | | | | | | | | (aNaturalNumber0(v0) = 0) | ~ $i(v0) | ? [v1: % 79.50/11.18 | | | | | | | | | | | | | | | | | any] : ( ~ (v1 = all_26_1) & % 79.50/11.18 | | | | | | | | | | | | | | | | | sdtpldt0(all_26_2, v0) = v1 & $i(v1))) % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | | ALPHA: (440) implies: % 79.50/11.18 | | | | | | | | | | | | | | | | | (441) ! [v0: $i] : ( ~ (aNaturalNumber0(v0) = 0) | ~ % 79.50/11.18 | | | | | | | | | | | | | | | | | $i(v0) | ? [v1: any] : ( ~ (v1 = all_26_1) & % 79.50/11.18 | | | | | | | | | | | | | | | | | sdtpldt0(all_26_2, v0) = v1 & $i(v1))) % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (441) with all_24_0, simplifying % 79.50/11.18 | | | | | | | | | | | | | | | | | with (29), (30) gives: % 79.50/11.18 | | | | | | | | | | | | | | | | | (442) ? [v0: any] : ( ~ (v0 = all_26_1) & % 79.50/11.18 | | | | | | | | | | | | | | | | | sdtpldt0(all_26_2, all_24_0) = v0 & $i(v0)) % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | | DELTA: instantiating (442) with fresh symbol all_883_0 % 79.50/11.18 | | | | | | | | | | | | | | | | | gives: % 79.50/11.18 | | | | | | | | | | | | | | | | | (443) ~ (all_883_0 = all_26_1) & sdtpldt0(all_26_2, % 79.50/11.18 | | | | | | | | | | | | | | | | | all_24_0) = all_883_0 & $i(all_883_0) % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | | ALPHA: (443) implies: % 79.50/11.18 | | | | | | | | | | | | | | | | | (444) ~ (all_883_0 = all_26_1) % 79.50/11.18 | | | | | | | | | | | | | | | | | (445) sdtpldt0(all_26_2, all_24_0) = all_883_0 % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | | REDUCE: (408), (444) imply: % 79.50/11.18 | | | | | | | | | | | | | | | | | (446) ~ (all_883_0 = all_26_4) % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | | REDUCE: (427), (445) imply: % 79.50/11.18 | | | | | | | | | | | | | | | | | (447) sdtpldt0(all_26_5, all_24_0) = all_883_0 % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (26) with all_26_4, all_883_0, % 79.50/11.18 | | | | | | | | | | | | | | | | | all_24_0, all_26_5, simplifying with (423), (447) % 79.50/11.18 | | | | | | | | | | | | | | | | | gives: % 79.50/11.18 | | | | | | | | | | | | | | | | | (448) all_883_0 = all_26_4 % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | | REDUCE: (446), (448) imply: % 79.50/11.18 | | | | | | | | | | | | | | | | | (449) $false % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | | CLOSE: (449) is inconsistent. % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | Case 2: % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | | (450) ~ (all_26_3 = 0) & ! [v0: $i] : ( ~ % 79.50/11.18 | | | | | | | | | | | | | | | | | (sdtpldt0(all_26_5, v0) = all_26_4) | ~ $i(v0) % 79.50/11.18 | | | | | | | | | | | | | | | | | | ? [v1: int] : ( ~ (v1 = 0) & % 79.50/11.18 | | | | | | | | | | | | | | | | | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( ~ % 79.50/11.18 | | | | | | | | | | | | | | | | | (aNaturalNumber0(v0) = 0) | ~ $i(v0) | ? [v1: % 79.50/11.18 | | | | | | | | | | | | | | | | | any] : ( ~ (v1 = all_26_4) & % 79.50/11.18 | | | | | | | | | | | | | | | | | sdtpldt0(all_26_5, v0) = v1 & $i(v1))) % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | | ALPHA: (450) implies: % 79.50/11.18 | | | | | | | | | | | | | | | | | (451) ! [v0: $i] : ( ~ (aNaturalNumber0(v0) = 0) | ~ % 79.50/11.18 | | | | | | | | | | | | | | | | | $i(v0) | ? [v1: any] : ( ~ (v1 = all_26_4) & % 79.50/11.18 | | | | | | | | | | | | | | | | | sdtpldt0(all_26_5, v0) = v1 & $i(v1))) % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (451) with all_24_0, simplifying % 79.50/11.18 | | | | | | | | | | | | | | | | | with (29), (30) gives: % 79.50/11.18 | | | | | | | | | | | | | | | | | (452) ? [v0: any] : ( ~ (v0 = all_26_4) & % 79.50/11.18 | | | | | | | | | | | | | | | | | sdtpldt0(all_26_5, all_24_0) = v0 & $i(v0)) % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | | DELTA: instantiating (452) with fresh symbol all_883_0 % 79.50/11.18 | | | | | | | | | | | | | | | | | gives: % 79.50/11.18 | | | | | | | | | | | | | | | | | (453) ~ (all_883_0 = all_26_4) & sdtpldt0(all_26_5, % 79.50/11.18 | | | | | | | | | | | | | | | | | all_24_0) = all_883_0 & $i(all_883_0) % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | | ALPHA: (453) implies: % 79.50/11.18 | | | | | | | | | | | | | | | | | (454) ~ (all_883_0 = all_26_4) % 79.50/11.18 | | | | | | | | | | | | | | | | | (455) sdtpldt0(all_26_5, all_24_0) = all_883_0 % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (26) with all_26_4, all_883_0, % 79.50/11.18 | | | | | | | | | | | | | | | | | all_24_0, all_26_5, simplifying with (423), (455) % 79.50/11.18 | | | | | | | | | | | | | | | | | gives: % 79.50/11.18 | | | | | | | | | | | | | | | | | (456) all_883_0 = all_26_4 % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | | REDUCE: (454), (456) imply: % 79.50/11.18 | | | | | | | | | | | | | | | | | (457) $false % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | | CLOSE: (457) is inconsistent. % 79.50/11.18 | | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | | End of split % 79.50/11.18 | | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | | End of split % 79.50/11.18 | | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | | End of split % 79.50/11.18 | | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | | End of split % 79.50/11.18 | | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | | End of split % 79.50/11.18 | | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | | End of split % 79.50/11.18 | | | | | | | | | | | % 79.50/11.18 | | | | | | | | | | End of split % 79.50/11.18 | | | | | | | | | | % 79.50/11.18 | | | | | | | | | End of split % 79.50/11.18 | | | | | | | | | % 79.50/11.18 | | | | | | | | End of split % 79.50/11.18 | | | | | | | | % 79.50/11.18 | | | | | | | End of split % 79.50/11.18 | | | | | | | % 79.50/11.19 | | | | | | End of split % 79.50/11.19 | | | | | | % 79.50/11.19 | | | | | End of split % 79.50/11.19 | | | | | % 79.50/11.19 | | | | End of split % 79.50/11.19 | | | | % 79.50/11.19 | | | End of split % 79.50/11.19 | | | % 79.50/11.19 | | End of split % 79.50/11.19 | | % 79.50/11.19 | End of split % 79.50/11.19 | % 79.50/11.19 End of proof % 79.50/11.19 % SZS output end Proof for theBenchmark % 79.50/11.19 % 79.50/11.19 10568ms %------------------------------------------------------------------------------