%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : NUM476+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 : n007.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:48:01 EDT 2023 % Result : Theorem 13.84s 2.60s % Output : Proof 23.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM476+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 : n007.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.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Fri Aug 25 15:17:10 EDT 2023 % 0.13/0.35 % CPUTime : % 0.20/0.63 ________ _____ % 0.20/0.63 ___ __ \_________(_)________________________________ % 0.20/0.63 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.63 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.63 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.63 % 0.20/0.63 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.63 (2023-06-19) % 0.20/0.63 % 0.20/0.63 (c) Philipp Rümmer, 2009-2023 % 0.20/0.63 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.63 Amanda Stjerna. % 0.20/0.63 Free software under BSD-3-Clause. % 0.20/0.63 % 0.20/0.63 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.63 % 0.20/0.63 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.20/0.64 Running up to 7 provers in parallel. % 0.20/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.20/0.66 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 3.18/1.22 Prover 4: Preprocessing ... % 3.18/1.22 Prover 1: Preprocessing ... % 3.82/1.26 Prover 3: Preprocessing ... % 3.82/1.26 Prover 2: Preprocessing ... % 3.82/1.26 Prover 6: Preprocessing ... % 3.82/1.26 Prover 5: Preprocessing ... % 3.82/1.26 Prover 0: Preprocessing ... % 8.06/1.89 Prover 1: Constructing countermodel ... % 8.73/1.94 Prover 3: Constructing countermodel ... % 8.73/1.96 Prover 6: Proving ... % 8.73/2.04 Prover 5: Constructing countermodel ... % 10.45/2.17 Prover 2: Proving ... % 11.14/2.22 Prover 4: Constructing countermodel ... % 11.68/2.31 Prover 0: Proving ... % 13.84/2.60 Prover 3: proved (1941ms) % 13.84/2.60 % 13.84/2.60 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.84/2.60 % 13.84/2.61 Prover 5: stopped % 13.84/2.61 Prover 6: stopped % 13.84/2.61 Prover 2: stopped % 13.84/2.62 Prover 0: stopped % 13.84/2.63 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 13.84/2.63 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 13.84/2.63 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 13.84/2.63 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 13.84/2.63 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 14.38/2.72 Prover 10: Preprocessing ... % 14.96/2.73 Prover 7: Preprocessing ... % 14.96/2.75 Prover 13: Preprocessing ... % 14.96/2.76 Prover 11: Preprocessing ... % 14.96/2.76 Prover 8: Preprocessing ... % 15.34/2.83 Prover 10: Constructing countermodel ... % 16.03/2.91 Prover 8: Warning: ignoring some quantifiers % 16.45/2.93 Prover 13: Constructing countermodel ... % 16.45/2.93 Prover 8: Constructing countermodel ... % 16.45/2.93 Prover 7: Constructing countermodel ... % 17.70/3.11 Prover 11: Constructing countermodel ... % 22.68/3.74 Prover 1: Found proof (size 325) % 22.68/3.74 Prover 1: proved (3093ms) % 22.68/3.74 Prover 11: stopped % 22.68/3.74 Prover 4: stopped % 22.68/3.74 Prover 10: stopped % 22.68/3.74 Prover 8: stopped % 22.68/3.74 Prover 7: stopped % 22.68/3.74 Prover 13: stopped % 22.68/3.74 % 22.68/3.74 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 22.68/3.74 % 22.68/3.77 % SZS output start Proof for theBenchmark % 22.68/3.77 Assumptions after simplification: % 22.68/3.77 --------------------------------- % 22.68/3.77 % 22.68/3.77 (mAMDistr) % 23.01/3.80 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 23.01/3.80 $i] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ % 23.01/3.80 (sdtpldt0(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : % 23.01/3.80 ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? % 23.01/3.80 [v12: $i] : ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v9, v0) = v11 & % 23.01/3.80 sdtasdt0(v2, v0) = v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v9) = v10 & % 23.01/3.80 sdtpldt0(v12, v13) = v14 & sdtpldt0(v1, v2) = v9 & aNaturalNumber0(v2) = % 23.01/3.80 v8 & aNaturalNumber0(v1) = v7 & aNaturalNumber0(v0) = v6 & $i(v14) & % 23.01/3.80 $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) & ( ~ (v8 = 0) | ~ (v7 = % 23.01/3.80 0) | ~ (v6 = 0) | (v14 = v11 & v10 = v5)))) % 23.01/3.80 % 23.01/3.80 (mAddAsso) % 23.01/3.80 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 23.01/3.80 (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) % 23.01/3.80 | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? % 23.01/3.80 [v9: $i] : (sdtpldt0(v1, v2) = v8 & sdtpldt0(v0, v8) = v9 & % 23.01/3.80 aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & aNaturalNumber0(v0) % 23.01/3.80 = v5 & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v9 = % 23.01/3.80 v4))) % 23.01/3.80 % 23.01/3.80 (mAddComm) % 23.01/3.80 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 23.01/3.80 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 23.01/3.80 (sdtpldt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 % 23.01/3.80 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 23.01/3.80 % 23.01/3.80 (mDefDiv) % 23.01/3.80 ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (doDivides0(v0, v1) = v2) | ~ % 23.01/3.80 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : (aNaturalNumber0(v1) = v4 % 23.01/3.80 & aNaturalNumber0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0))) | (( ~ (v2 = 0) % 23.01/3.80 | ? [v3: $i] : (sdtasdt0(v0, v3) = v1 & aNaturalNumber0(v3) = 0 & % 23.01/3.80 $i(v3))) & (v2 = 0 | ! [v3: $i] : ( ~ (sdtasdt0(v0, v3) = v1) | ~ % 23.01/3.80 $i(v3) | ? [v4: int] : ( ~ (v4 = 0) & aNaturalNumber0(v3) = v4))))) % 23.01/3.80 % 23.01/3.80 (mDivTrans) % 23.01/3.80 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 23.01/3.80 (doDivides0(v0, v2) = v3) | ~ (doDivides0(v0, v1) = 0) | ~ $i(v2) | ~ % 23.01/3.80 $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: % 23.01/3.80 any] : (doDivides0(v1, v2) = v7 & aNaturalNumber0(v2) = v6 & % 23.01/3.80 aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v7 = 0) | ~ % 23.01/3.80 (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) % 23.01/3.80 % 23.01/3.80 (mMulCanc) % 23.01/3.81 $i(sz00) & ! [v0: $i] : (v0 = sz00 | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) % 23.01/3.81 | ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v2 = v1 | ~ % 23.01/3.81 (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | ~ % 23.01/3.81 $i(v1) | ? [v5: any] : ? [v6: any] : ? [v7: $i] : ? [v8: $i] : % 23.01/3.81 (sdtasdt0(v2, v0) = v8 & sdtasdt0(v1, v0) = v7 & aNaturalNumber0(v2) = v6 % 23.01/3.81 & aNaturalNumber0(v1) = v5 & $i(v8) & $i(v7) & ( ~ (v6 = 0) | ~ (v5 = % 23.01/3.81 0) | ( ~ (v8 = v7) & ~ (v4 = v3)))))) % 23.01/3.81 % 23.01/3.81 (mMulComm) % 23.01/3.81 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 23.01/3.81 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 23.01/3.81 (sdtasdt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 % 23.01/3.81 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 23.01/3.81 % 23.01/3.81 (mSortsB) % 23.01/3.81 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 23.01/3.81 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 23.01/3.81 (aNaturalNumber0(v2) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = % 23.01/3.81 v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 23.01/3.81 % 23.01/3.81 (mSortsB_02) % 23.01/3.81 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 23.01/3.81 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 23.01/3.81 (aNaturalNumber0(v2) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = % 23.01/3.81 v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 23.01/3.81 % 23.01/3.81 (m_AddZero) % 23.01/3.81 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtpldt0(sz00, v0) = v1) | ~ % 23.01/3.81 $i(v0) | ? [v2: any] : ? [v3: $i] : (sdtpldt0(v0, sz00) = v3 & % 23.01/3.81 aNaturalNumber0(v0) = v2 & $i(v3) & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) % 23.01/3.81 % 23.01/3.81 (m_MulZero) % 23.01/3.81 $i(sz00) & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtasdt0(sz00, v0) = v1) | ~ % 23.01/3.81 $i(v0) | ? [v2: any] : ? [v3: $i] : (sdtasdt0(v0, sz00) = v3 & % 23.01/3.81 aNaturalNumber0(v0) = v2 & $i(v3) & ( ~ (v2 = 0) | (v3 = sz00 & v1 = % 23.01/3.81 sz00)))) % 23.01/3.81 % 23.01/3.81 (m__) % 23.01/3.81 $i(xn) & $i(xm) & $i(xl) & $i(sz00) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] % 23.01/3.81 : ? [v3: int] : ( ~ (v3 = 0) & sdtsldt0(v1, xl) = v2 & sdtsldt0(xm, xl) = v0 % 23.01/3.81 & doDivides0(xl, xn) = v3 & sdtpldt0(xm, xn) = v1 & $i(v2) & $i(v1) & $i(v0) % 23.01/3.81 & ! [v4: $i] : ( ~ (sdtasdt0(xl, v4) = xn) | ~ $i(v4) | ? [v5: int] : ( ~ % 23.01/3.81 (v5 = 0) & aNaturalNumber0(v4) = v5)) & (xl = sz00 | (sdtasdt0(xl, v0) = % 23.01/3.81 xm & aNaturalNumber0(v0) = 0 & ? [v4: $i] : (sdtmndt0(v2, v0) = v4 & % 23.01/3.81 sdtlseqdt0(v0, v2) = 0 & sdtasdt0(xl, v4) = xn & sdtasdt0(xl, v2) = v1 % 23.01/3.82 & sdtpldt0(v0, v4) = v2 & aNaturalNumber0(v4) = 0 & % 23.01/3.82 aNaturalNumber0(v2) = 0 & $i(v4) & ? [v5: $i] : (sdtpldt0(v0, v5) = % 23.01/3.82 v2 & aNaturalNumber0(v5) = 0 & $i(v5)))))) % 23.01/3.82 % 23.01/3.82 (m__1324) % 23.01/3.82 aNaturalNumber0(xn) = 0 & aNaturalNumber0(xm) = 0 & aNaturalNumber0(xl) = 0 & % 23.01/3.82 $i(xn) & $i(xm) & $i(xl) % 23.01/3.82 % 23.01/3.82 (m__1324_04) % 23.01/3.82 $i(xn) & $i(xm) & $i(xl) & ? [v0: $i] : (doDivides0(xl, v0) = 0 & % 23.01/3.82 doDivides0(xl, xm) = 0 & sdtpldt0(xm, xn) = v0 & $i(v0) & ? [v1: $i] : % 23.01/3.82 (sdtasdt0(xl, v1) = v0 & aNaturalNumber0(v1) = 0 & $i(v1)) & ? [v1: $i] : % 23.01/3.82 (sdtasdt0(xl, v1) = xm & aNaturalNumber0(v1) = 0 & $i(v1))) % 23.01/3.82 % 23.01/3.82 (function-axioms) % 23.01/3.82 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 23.01/3.82 (sdtsldt0(v3, v2) = v1) | ~ (sdtsldt0(v3, v2) = v0)) & ! [v0: % 23.01/3.82 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 23.01/3.82 : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ (doDivides0(v3, v2) = v0)) & ! % 23.01/3.82 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 23.01/3.82 $i] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) & ! % 23.01/3.82 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 23.01/3.82 (sdtmndt0(v3, v2) = v1) | ~ (sdtmndt0(v3, v2) = v0)) & ! [v0: % 23.01/3.82 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 23.01/3.82 : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ (sdtlseqdt0(v3, v2) = v0)) & ! % 23.01/3.82 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 23.01/3.82 (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 23.01/3.82 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | % 23.01/3.82 ~ (sdtpldt0(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 23.01/3.82 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) % 23.01/3.82 | ~ (aNaturalNumber0(v2) = v0)) % 23.01/3.82 % 23.01/3.82 Further assumptions not needed in the proof: % 23.01/3.82 -------------------------------------------- % 23.01/3.82 mAddCanc, mDefDiff, mDefLE, mDefQuot, mDivSum, mIH, mIH_03, mLEAsym, mLENTr, % 23.01/3.82 mLERefl, mLETotal, mLETran, mMonAdd, mMonMul, mMonMul2, mMulAsso, mNatSort, % 23.01/3.82 mSortsC, mSortsC_01, mZeroAdd, mZeroMul, m_MulUnit % 23.01/3.82 % 23.01/3.82 Those formulas are unsatisfiable: % 23.01/3.82 --------------------------------- % 23.01/3.82 % 23.01/3.82 Begin of proof % 23.01/3.82 | % 23.01/3.82 | ALPHA: (m_AddZero) implies: % 23.01/3.82 | (1) ! [v0: $i] : ! [v1: $i] : ( ~ (sdtpldt0(sz00, v0) = v1) | ~ $i(v0) | % 23.01/3.82 | ? [v2: any] : ? [v3: $i] : (sdtpldt0(v0, sz00) = v3 & % 23.01/3.82 | aNaturalNumber0(v0) = v2 & $i(v3) & ( ~ (v2 = 0) | (v3 = v0 & v1 = % 23.01/3.82 | v0)))) % 23.01/3.82 | % 23.01/3.82 | ALPHA: (m_MulZero) implies: % 23.01/3.82 | (2) ! [v0: $i] : ! [v1: $i] : ( ~ (sdtasdt0(sz00, v0) = v1) | ~ $i(v0) | % 23.01/3.82 | ? [v2: any] : ? [v3: $i] : (sdtasdt0(v0, sz00) = v3 & % 23.01/3.82 | aNaturalNumber0(v0) = v2 & $i(v3) & ( ~ (v2 = 0) | (v3 = sz00 & v1 % 23.01/3.82 | = sz00)))) % 23.01/3.82 | % 23.01/3.82 | ALPHA: (mMulCanc) implies: % 23.01/3.83 | (3) ! [v0: $i] : (v0 = sz00 | ~ (aNaturalNumber0(v0) = 0) | ~ $i(v0) | % 23.01/3.83 | ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v2 = v1 | ~ % 23.01/3.83 | (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | % 23.01/3.83 | ~ $i(v1) | ? [v5: any] : ? [v6: any] : ? [v7: $i] : ? [v8: $i] % 23.01/3.83 | : (sdtasdt0(v2, v0) = v8 & sdtasdt0(v1, v0) = v7 & % 23.01/3.83 | aNaturalNumber0(v2) = v6 & aNaturalNumber0(v1) = v5 & $i(v8) & % 23.01/3.83 | $i(v7) & ( ~ (v6 = 0) | ~ (v5 = 0) | ( ~ (v8 = v7) & ~ (v4 = % 23.01/3.83 | v3)))))) % 23.01/3.83 | % 23.01/3.83 | ALPHA: (m__1324) implies: % 23.01/3.83 | (4) aNaturalNumber0(xl) = 0 % 23.01/3.83 | (5) aNaturalNumber0(xm) = 0 % 23.01/3.83 | (6) aNaturalNumber0(xn) = 0 % 23.01/3.83 | % 23.01/3.83 | ALPHA: (m__1324_04) implies: % 23.01/3.83 | (7) ? [v0: $i] : (doDivides0(xl, v0) = 0 & doDivides0(xl, xm) = 0 & % 23.01/3.83 | sdtpldt0(xm, xn) = v0 & $i(v0) & ? [v1: $i] : (sdtasdt0(xl, v1) = v0 % 23.01/3.83 | & aNaturalNumber0(v1) = 0 & $i(v1)) & ? [v1: $i] : (sdtasdt0(xl, % 23.01/3.83 | v1) = xm & aNaturalNumber0(v1) = 0 & $i(v1))) % 23.01/3.83 | % 23.01/3.83 | ALPHA: (m__) implies: % 23.01/3.83 | (8) $i(xl) % 23.01/3.83 | (9) $i(xm) % 23.01/3.83 | (10) $i(xn) % 23.01/3.83 | (11) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: int] : ( ~ (v3 = 0) % 23.01/3.83 | & sdtsldt0(v1, xl) = v2 & sdtsldt0(xm, xl) = v0 & doDivides0(xl, xn) % 23.01/3.83 | = v3 & sdtpldt0(xm, xn) = v1 & $i(v2) & $i(v1) & $i(v0) & ! [v4: % 23.01/3.83 | $i] : ( ~ (sdtasdt0(xl, v4) = xn) | ~ $i(v4) | ? [v5: int] : ( ~ % 23.01/3.83 | (v5 = 0) & aNaturalNumber0(v4) = v5)) & (xl = sz00 | % 23.01/3.83 | (sdtasdt0(xl, v0) = xm & aNaturalNumber0(v0) = 0 & ? [v4: $i] : % 23.01/3.83 | (sdtmndt0(v2, v0) = v4 & sdtlseqdt0(v0, v2) = 0 & sdtasdt0(xl, % 23.01/3.83 | v4) = xn & sdtasdt0(xl, v2) = v1 & sdtpldt0(v0, v4) = v2 & % 23.01/3.83 | aNaturalNumber0(v4) = 0 & aNaturalNumber0(v2) = 0 & $i(v4) & % 23.01/3.83 | ? [v5: $i] : (sdtpldt0(v0, v5) = v2 & aNaturalNumber0(v5) = 0 % 23.01/3.83 | & $i(v5)))))) % 23.01/3.83 | % 23.01/3.83 | ALPHA: (function-axioms) implies: % 23.01/3.83 | (12) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 23.01/3.83 | : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = % 23.01/3.83 | v0)) % 23.01/3.83 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 23.01/3.83 | (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 23.01/3.83 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 23.01/3.83 | (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 23.01/3.83 | (15) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 23.01/3.83 | : ! [v3: $i] : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ % 23.01/3.83 | (doDivides0(v3, v2) = v0)) % 23.01/3.83 | % 23.01/3.83 | DELTA: instantiating (7) with fresh symbol all_33_0 gives: % 23.01/3.84 | (16) doDivides0(xl, all_33_0) = 0 & doDivides0(xl, xm) = 0 & sdtpldt0(xm, % 23.01/3.84 | xn) = all_33_0 & $i(all_33_0) & ? [v0: $i] : (sdtasdt0(xl, v0) = % 23.01/3.84 | all_33_0 & aNaturalNumber0(v0) = 0 & $i(v0)) & ? [v0: $i] : % 23.01/3.84 | (sdtasdt0(xl, v0) = xm & aNaturalNumber0(v0) = 0 & $i(v0)) % 23.01/3.84 | % 23.01/3.84 | ALPHA: (16) implies: % 23.01/3.84 | (17) sdtpldt0(xm, xn) = all_33_0 % 23.01/3.84 | (18) doDivides0(xl, xm) = 0 % 23.01/3.84 | (19) doDivides0(xl, all_33_0) = 0 % 23.01/3.84 | (20) ? [v0: $i] : (sdtasdt0(xl, v0) = xm & aNaturalNumber0(v0) = 0 & % 23.01/3.84 | $i(v0)) % 23.01/3.84 | (21) ? [v0: $i] : (sdtasdt0(xl, v0) = all_33_0 & aNaturalNumber0(v0) = 0 & % 23.01/3.84 | $i(v0)) % 23.01/3.84 | % 23.01/3.84 | DELTA: instantiating (11) with fresh symbols all_35_0, all_35_1, all_35_2, % 23.01/3.84 | all_35_3 gives: % 23.01/3.84 | (22) ~ (all_35_0 = 0) & sdtsldt0(all_35_2, xl) = all_35_1 & sdtsldt0(xm, % 23.01/3.84 | xl) = all_35_3 & doDivides0(xl, xn) = all_35_0 & sdtpldt0(xm, xn) = % 23.01/3.84 | all_35_2 & $i(all_35_1) & $i(all_35_2) & $i(all_35_3) & ! [v0: $i] : % 23.01/3.84 | ( ~ (sdtasdt0(xl, v0) = xn) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) % 23.01/3.84 | & aNaturalNumber0(v0) = v1)) & (xl = sz00 | (sdtasdt0(xl, % 23.01/3.84 | all_35_3) = xm & aNaturalNumber0(all_35_3) = 0 & ? [v0: $i] : % 23.01/3.84 | (sdtmndt0(all_35_1, all_35_3) = v0 & sdtlseqdt0(all_35_3, % 23.01/3.84 | all_35_1) = 0 & sdtasdt0(xl, v0) = xn & sdtasdt0(xl, all_35_1) % 23.01/3.84 | = all_35_2 & sdtpldt0(all_35_3, v0) = all_35_1 & % 23.01/3.84 | aNaturalNumber0(v0) = 0 & aNaturalNumber0(all_35_1) = 0 & $i(v0) % 23.01/3.84 | & ? [v1: $i] : (sdtpldt0(all_35_3, v1) = all_35_1 & % 23.01/3.84 | aNaturalNumber0(v1) = 0 & $i(v1))))) % 23.01/3.84 | % 23.01/3.84 | ALPHA: (22) implies: % 23.01/3.84 | (23) ~ (all_35_0 = 0) % 23.01/3.84 | (24) $i(all_35_3) % 23.01/3.84 | (25) $i(all_35_2) % 23.01/3.84 | (26) sdtpldt0(xm, xn) = all_35_2 % 23.01/3.84 | (27) doDivides0(xl, xn) = all_35_0 % 23.01/3.84 | (28) xl = sz00 | (sdtasdt0(xl, all_35_3) = xm & aNaturalNumber0(all_35_3) = % 23.01/3.84 | 0 & ? [v0: $i] : (sdtmndt0(all_35_1, all_35_3) = v0 & % 23.01/3.84 | sdtlseqdt0(all_35_3, all_35_1) = 0 & sdtasdt0(xl, v0) = xn & % 23.01/3.84 | sdtasdt0(xl, all_35_1) = all_35_2 & sdtpldt0(all_35_3, v0) = % 23.01/3.84 | all_35_1 & aNaturalNumber0(v0) = 0 & aNaturalNumber0(all_35_1) = 0 % 23.01/3.84 | & $i(v0) & ? [v1: $i] : (sdtpldt0(all_35_3, v1) = all_35_1 & % 23.01/3.84 | aNaturalNumber0(v1) = 0 & $i(v1)))) % 23.01/3.84 | (29) ! [v0: $i] : ( ~ (sdtasdt0(xl, v0) = xn) | ~ $i(v0) | ? [v1: int] : % 23.01/3.84 | ( ~ (v1 = 0) & aNaturalNumber0(v0) = v1)) % 23.01/3.84 | % 23.01/3.84 | DELTA: instantiating (20) with fresh symbol all_38_0 gives: % 23.01/3.84 | (30) sdtasdt0(xl, all_38_0) = xm & aNaturalNumber0(all_38_0) = 0 & % 23.01/3.84 | $i(all_38_0) % 23.01/3.84 | % 23.01/3.84 | ALPHA: (30) implies: % 23.01/3.84 | (31) $i(all_38_0) % 23.01/3.84 | (32) aNaturalNumber0(all_38_0) = 0 % 23.01/3.84 | (33) sdtasdt0(xl, all_38_0) = xm % 23.01/3.84 | % 23.01/3.84 | DELTA: instantiating (21) with fresh symbol all_40_0 gives: % 23.01/3.84 | (34) sdtasdt0(xl, all_40_0) = all_33_0 & aNaturalNumber0(all_40_0) = 0 & % 23.01/3.84 | $i(all_40_0) % 23.01/3.84 | % 23.01/3.84 | ALPHA: (34) implies: % 23.01/3.84 | (35) $i(all_40_0) % 23.01/3.84 | (36) aNaturalNumber0(all_40_0) = 0 % 23.01/3.85 | (37) sdtasdt0(xl, all_40_0) = all_33_0 % 23.01/3.85 | % 23.01/3.85 | GROUND_INST: instantiating (13) with all_33_0, all_35_2, xn, xm, simplifying % 23.01/3.85 | with (17), (26) gives: % 23.01/3.85 | (38) all_35_2 = all_33_0 % 23.01/3.85 | % 23.01/3.85 | REDUCE: (25), (38) imply: % 23.01/3.85 | (39) $i(all_33_0) % 23.01/3.85 | % 23.01/3.85 | GROUND_INST: instantiating (3) with xn, simplifying with (6), (10) gives: % 23.01/3.85 | (40) xn = sz00 | ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 23.01/3.85 | (v1 = v0 | ~ (sdtasdt0(xn, v1) = v3) | ~ (sdtasdt0(xn, v0) = v2) | % 23.01/3.85 | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: $i] : % 23.01/3.85 | ? [v7: $i] : (sdtasdt0(v1, xn) = v7 & sdtasdt0(v0, xn) = v6 & % 23.01/3.85 | aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & $i(v7) & % 23.01/3.85 | $i(v6) & ( ~ (v5 = 0) | ~ (v4 = 0) | ( ~ (v7 = v6) & ~ (v3 = % 23.01/3.85 | v2))))) % 23.01/3.85 | % 23.01/3.85 | GROUND_INST: instantiating (mAddComm) with xm, xn, all_33_0, simplifying with % 23.01/3.85 | (9), (10), (17) gives: % 23.01/3.85 | (41) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xn, xm) = v2 & % 23.01/3.85 | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xm) = v0 & $i(v2) & ( ~ % 23.01/3.85 | (v1 = 0) | ~ (v0 = 0) | v2 = all_33_0)) % 23.01/3.85 | % 23.01/3.85 | GROUND_INST: instantiating (mSortsB) with xm, xn, all_33_0, simplifying with % 23.01/3.85 | (9), (10), (17) gives: % 23.01/3.85 | (42) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 23.01/3.85 | (aNaturalNumber0(all_33_0) = v2 & aNaturalNumber0(xn) = v1 & % 23.01/3.85 | aNaturalNumber0(xm) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 23.01/3.85 | % 23.01/3.85 | GROUND_INST: instantiating (mMulComm) with xl, all_38_0, xm, simplifying with % 23.01/3.85 | (8), (31), (33) gives: % 23.01/3.85 | (43) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_38_0, xl) = % 23.01/3.85 | v2 & aNaturalNumber0(all_38_0) = v1 & aNaturalNumber0(xl) = v0 & % 23.01/3.85 | $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = xm)) % 23.01/3.85 | % 23.01/3.85 | GROUND_INST: instantiating (mMulComm) with xl, all_40_0, all_33_0, simplifying % 23.01/3.85 | with (8), (35), (37) gives: % 23.01/3.85 | (44) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_40_0, xl) = % 23.01/3.85 | v2 & aNaturalNumber0(all_40_0) = v1 & aNaturalNumber0(xl) = v0 & % 23.01/3.85 | $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = all_33_0)) % 23.01/3.85 | % 23.01/3.85 | GROUND_INST: instantiating (mSortsB_02) with xl, all_40_0, all_33_0, % 23.01/3.85 | simplifying with (8), (35), (37) gives: % 23.01/3.85 | (45) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 23.01/3.85 | (aNaturalNumber0(all_40_0) = v1 & aNaturalNumber0(all_33_0) = v2 & % 23.01/3.85 | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 23.01/3.85 | % 23.01/3.85 | GROUND_INST: instantiating (mDivTrans) with xl, xm, xn, all_35_0, simplifying % 23.01/3.85 | with (8), (9), (10), (18), (27) gives: % 23.01/3.85 | (46) all_35_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: % 23.01/3.85 | any] : (doDivides0(xm, xn) = v3 & aNaturalNumber0(xn) = v2 & % 23.01/3.85 | aNaturalNumber0(xm) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v3 = 0) | % 23.01/3.85 | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 23.01/3.85 | % 23.01/3.85 | GROUND_INST: instantiating (mDivTrans) with xl, all_33_0, xn, all_35_0, % 23.01/3.85 | simplifying with (8), (10), (19), (27), (39) gives: % 23.01/3.86 | (47) all_35_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: % 23.01/3.86 | any] : (doDivides0(all_33_0, xn) = v3 & aNaturalNumber0(all_33_0) = % 23.01/3.86 | v1 & aNaturalNumber0(xn) = v2 & aNaturalNumber0(xl) = v0 & ( ~ (v3 = % 23.01/3.86 | 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 23.01/3.86 | % 23.01/3.86 | DELTA: instantiating (45) with fresh symbols all_51_0, all_51_1, all_51_2 % 23.01/3.86 | gives: % 23.01/3.86 | (48) aNaturalNumber0(all_40_0) = all_51_1 & aNaturalNumber0(all_33_0) = % 23.01/3.86 | all_51_0 & aNaturalNumber0(xl) = all_51_2 & ( ~ (all_51_1 = 0) | ~ % 23.01/3.86 | (all_51_2 = 0) | all_51_0 = 0) % 23.01/3.86 | % 23.01/3.86 | ALPHA: (48) implies: % 23.01/3.86 | (49) aNaturalNumber0(xl) = all_51_2 % 23.01/3.86 | (50) aNaturalNumber0(all_33_0) = all_51_0 % 23.01/3.86 | (51) aNaturalNumber0(all_40_0) = all_51_1 % 23.01/3.86 | (52) ~ (all_51_1 = 0) | ~ (all_51_2 = 0) | all_51_0 = 0 % 23.01/3.86 | % 23.01/3.86 | DELTA: instantiating (42) with fresh symbols all_53_0, all_53_1, all_53_2 % 23.01/3.86 | gives: % 23.01/3.86 | (53) aNaturalNumber0(all_33_0) = all_53_0 & aNaturalNumber0(xn) = all_53_1 % 23.01/3.86 | & aNaturalNumber0(xm) = all_53_2 & ( ~ (all_53_1 = 0) | ~ (all_53_2 = % 23.01/3.86 | 0) | all_53_0 = 0) % 23.01/3.86 | % 23.01/3.86 | ALPHA: (53) implies: % 23.01/3.86 | (54) aNaturalNumber0(xm) = all_53_2 % 23.01/3.86 | (55) aNaturalNumber0(xn) = all_53_1 % 23.01/3.86 | (56) aNaturalNumber0(all_33_0) = all_53_0 % 23.01/3.86 | % 23.01/3.86 | DELTA: instantiating (44) with fresh symbols all_55_0, all_55_1, all_55_2 % 23.01/3.86 | gives: % 23.01/3.86 | (57) sdtasdt0(all_40_0, xl) = all_55_0 & aNaturalNumber0(all_40_0) = % 23.01/3.86 | all_55_1 & aNaturalNumber0(xl) = all_55_2 & $i(all_55_0) & ( ~ % 23.01/3.86 | (all_55_1 = 0) | ~ (all_55_2 = 0) | all_55_0 = all_33_0) % 23.01/3.86 | % 23.01/3.86 | ALPHA: (57) implies: % 23.01/3.86 | (58) aNaturalNumber0(xl) = all_55_2 % 23.01/3.86 | (59) aNaturalNumber0(all_40_0) = all_55_1 % 23.01/3.86 | (60) sdtasdt0(all_40_0, xl) = all_55_0 % 23.01/3.86 | (61) ~ (all_55_1 = 0) | ~ (all_55_2 = 0) | all_55_0 = all_33_0 % 23.01/3.86 | % 23.01/3.86 | DELTA: instantiating (41) with fresh symbols all_57_0, all_57_1, all_57_2 % 23.01/3.86 | gives: % 23.01/3.86 | (62) sdtpldt0(xn, xm) = all_57_0 & aNaturalNumber0(xn) = all_57_1 & % 23.01/3.86 | aNaturalNumber0(xm) = all_57_2 & $i(all_57_0) & ( ~ (all_57_1 = 0) | % 23.01/3.86 | ~ (all_57_2 = 0) | all_57_0 = all_33_0) % 23.01/3.86 | % 23.01/3.86 | ALPHA: (62) implies: % 23.01/3.86 | (63) $i(all_57_0) % 23.01/3.86 | (64) aNaturalNumber0(xm) = all_57_2 % 23.01/3.86 | (65) aNaturalNumber0(xn) = all_57_1 % 23.01/3.86 | (66) sdtpldt0(xn, xm) = all_57_0 % 23.01/3.86 | (67) ~ (all_57_1 = 0) | ~ (all_57_2 = 0) | all_57_0 = all_33_0 % 23.01/3.86 | % 23.01/3.86 | DELTA: instantiating (43) with fresh symbols all_59_0, all_59_1, all_59_2 % 23.01/3.86 | gives: % 23.01/3.86 | (68) sdtasdt0(all_38_0, xl) = all_59_0 & aNaturalNumber0(all_38_0) = % 23.01/3.86 | all_59_1 & aNaturalNumber0(xl) = all_59_2 & $i(all_59_0) & ( ~ % 23.01/3.86 | (all_59_1 = 0) | ~ (all_59_2 = 0) | all_59_0 = xm) % 23.01/3.86 | % 23.01/3.86 | ALPHA: (68) implies: % 23.01/3.86 | (69) $i(all_59_0) % 23.01/3.86 | (70) aNaturalNumber0(xl) = all_59_2 % 23.01/3.86 | (71) aNaturalNumber0(all_38_0) = all_59_1 % 23.01/3.86 | (72) sdtasdt0(all_38_0, xl) = all_59_0 % 23.01/3.86 | (73) ~ (all_59_1 = 0) | ~ (all_59_2 = 0) | all_59_0 = xm % 23.01/3.86 | % 23.01/3.86 | BETA: splitting (47) gives: % 23.01/3.86 | % 23.01/3.86 | Case 1: % 23.01/3.86 | | % 23.01/3.86 | | (74) all_35_0 = 0 % 23.01/3.86 | | % 23.01/3.86 | | REDUCE: (23), (74) imply: % 23.01/3.86 | | (75) $false % 23.01/3.86 | | % 23.01/3.86 | | CLOSE: (75) is inconsistent. % 23.01/3.86 | | % 23.01/3.86 | Case 2: % 23.01/3.86 | | % 23.01/3.86 | | (76) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 23.01/3.86 | | (doDivides0(all_33_0, xn) = v3 & aNaturalNumber0(all_33_0) = v1 & % 23.01/3.86 | | aNaturalNumber0(xn) = v2 & aNaturalNumber0(xl) = v0 & ( ~ (v3 = 0) % 23.01/3.86 | | | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 23.01/3.86 | | % 23.01/3.86 | | DELTA: instantiating (76) with fresh symbols all_69_0, all_69_1, all_69_2, % 23.01/3.86 | | all_69_3 gives: % 23.01/3.86 | | (77) doDivides0(all_33_0, xn) = all_69_0 & aNaturalNumber0(all_33_0) = % 23.01/3.86 | | all_69_2 & aNaturalNumber0(xn) = all_69_1 & aNaturalNumber0(xl) = % 23.01/3.86 | | all_69_3 & ( ~ (all_69_0 = 0) | ~ (all_69_1 = 0) | ~ (all_69_2 = % 23.01/3.86 | | 0) | ~ (all_69_3 = 0)) % 23.01/3.86 | | % 23.01/3.86 | | ALPHA: (77) implies: % 23.01/3.86 | | (78) aNaturalNumber0(xl) = all_69_3 % 23.01/3.86 | | (79) aNaturalNumber0(xn) = all_69_1 % 23.01/3.86 | | (80) aNaturalNumber0(all_33_0) = all_69_2 % 23.01/3.86 | | (81) doDivides0(all_33_0, xn) = all_69_0 % 23.01/3.86 | | (82) ~ (all_69_0 = 0) | ~ (all_69_1 = 0) | ~ (all_69_2 = 0) | ~ % 23.01/3.86 | | (all_69_3 = 0) % 23.01/3.86 | | % 23.01/3.86 | | BETA: splitting (46) gives: % 23.01/3.86 | | % 23.01/3.86 | | Case 1: % 23.01/3.86 | | | % 23.01/3.87 | | | (83) all_35_0 = 0 % 23.01/3.87 | | | % 23.01/3.87 | | | REDUCE: (23), (83) imply: % 23.01/3.87 | | | (84) $false % 23.01/3.87 | | | % 23.01/3.87 | | | CLOSE: (84) is inconsistent. % 23.01/3.87 | | | % 23.01/3.87 | | Case 2: % 23.01/3.87 | | | % 23.01/3.87 | | | (85) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 23.01/3.87 | | | (doDivides0(xm, xn) = v3 & aNaturalNumber0(xn) = v2 & % 23.01/3.87 | | | aNaturalNumber0(xm) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v3 = % 23.01/3.87 | | | 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 23.01/3.87 | | | % 23.01/3.87 | | | DELTA: instantiating (85) with fresh symbols all_74_0, all_74_1, all_74_2, % 23.01/3.87 | | | all_74_3 gives: % 23.01/3.87 | | | (86) doDivides0(xm, xn) = all_74_0 & aNaturalNumber0(xn) = all_74_1 & % 23.01/3.87 | | | aNaturalNumber0(xm) = all_74_2 & aNaturalNumber0(xl) = all_74_3 & % 23.01/3.87 | | | ( ~ (all_74_0 = 0) | ~ (all_74_1 = 0) | ~ (all_74_2 = 0) | ~ % 23.01/3.87 | | | (all_74_3 = 0)) % 23.01/3.87 | | | % 23.01/3.87 | | | ALPHA: (86) implies: % 23.01/3.87 | | | (87) aNaturalNumber0(xl) = all_74_3 % 23.01/3.87 | | | (88) aNaturalNumber0(xm) = all_74_2 % 23.01/3.87 | | | (89) aNaturalNumber0(xn) = all_74_1 % 23.01/3.87 | | | (90) doDivides0(xm, xn) = all_74_0 % 23.01/3.87 | | | (91) ~ (all_74_0 = 0) | ~ (all_74_1 = 0) | ~ (all_74_2 = 0) | ~ % 23.01/3.87 | | | (all_74_3 = 0) % 23.01/3.87 | | | % 23.01/3.87 | | | GROUND_INST: instantiating (12) with all_55_2, all_59_2, xl, simplifying % 23.01/3.87 | | | with (58), (70) gives: % 23.01/3.87 | | | (92) all_59_2 = all_55_2 % 23.01/3.87 | | | % 23.01/3.87 | | | GROUND_INST: instantiating (12) with 0, all_69_3, xl, simplifying with % 23.01/3.87 | | | (4), (78) gives: % 23.01/3.87 | | | (93) all_69_3 = 0 % 23.01/3.87 | | | % 23.01/3.87 | | | GROUND_INST: instantiating (12) with all_55_2, all_69_3, xl, simplifying % 23.01/3.87 | | | with (58), (78) gives: % 23.01/3.87 | | | (94) all_69_3 = all_55_2 % 23.01/3.87 | | | % 23.01/3.87 | | | GROUND_INST: instantiating (12) with all_59_2, all_74_3, xl, simplifying % 23.01/3.87 | | | with (70), (87) gives: % 23.01/3.87 | | | (95) all_74_3 = all_59_2 % 23.01/3.87 | | | % 23.01/3.87 | | | GROUND_INST: instantiating (12) with all_51_2, all_74_3, xl, simplifying % 23.01/3.87 | | | with (49), (87) gives: % 23.01/3.87 | | | (96) all_74_3 = all_51_2 % 23.01/3.87 | | | % 23.01/3.87 | | | GROUND_INST: instantiating (12) with 0, all_74_2, xm, simplifying with % 23.01/3.87 | | | (5), (88) gives: % 23.01/3.87 | | | (97) all_74_2 = 0 % 23.01/3.87 | | | % 23.01/3.87 | | | GROUND_INST: instantiating (12) with all_57_2, all_74_2, xm, simplifying % 23.01/3.87 | | | with (64), (88) gives: % 23.01/3.87 | | | (98) all_74_2 = all_57_2 % 23.01/3.87 | | | % 23.01/3.87 | | | GROUND_INST: instantiating (12) with all_53_2, all_74_2, xm, simplifying % 23.01/3.87 | | | with (54), (88) gives: % 23.01/3.87 | | | (99) all_74_2 = all_53_2 % 23.01/3.87 | | | % 23.01/3.87 | | | GROUND_INST: instantiating (12) with 0, all_69_1, xn, simplifying with % 23.01/3.87 | | | (6), (79) gives: % 23.01/3.87 | | | (100) all_69_1 = 0 % 23.01/3.87 | | | % 23.01/3.87 | | | GROUND_INST: instantiating (12) with all_53_1, all_69_1, xn, simplifying % 23.01/3.87 | | | with (55), (79) gives: % 23.01/3.87 | | | (101) all_69_1 = all_53_1 % 23.01/3.87 | | | % 23.01/3.87 | | | GROUND_INST: instantiating (12) with all_69_1, all_74_1, xn, simplifying % 23.01/3.87 | | | with (79), (89) gives: % 23.01/3.87 | | | (102) all_74_1 = all_69_1 % 23.01/3.87 | | | % 23.01/3.87 | | | GROUND_INST: instantiating (12) with all_57_1, all_74_1, xn, simplifying % 23.01/3.87 | | | with (65), (89) gives: % 23.01/3.87 | | | (103) all_74_1 = all_57_1 % 23.01/3.87 | | | % 23.01/3.87 | | | GROUND_INST: instantiating (12) with all_53_0, all_69_2, all_33_0, % 23.01/3.87 | | | simplifying with (56), (80) gives: % 23.01/3.87 | | | (104) all_69_2 = all_53_0 % 23.01/3.87 | | | % 23.01/3.87 | | | GROUND_INST: instantiating (12) with all_51_0, all_69_2, all_33_0, % 23.01/3.87 | | | simplifying with (50), (80) gives: % 23.01/3.87 | | | (105) all_69_2 = all_51_0 % 23.01/3.87 | | | % 23.01/3.87 | | | GROUND_INST: instantiating (12) with 0, all_59_1, all_38_0, simplifying % 23.01/3.87 | | | with (32), (71) gives: % 23.01/3.87 | | | (106) all_59_1 = 0 % 23.01/3.87 | | | % 23.01/3.87 | | | GROUND_INST: instantiating (12) with 0, all_55_1, all_40_0, simplifying % 23.01/3.87 | | | with (36), (59) gives: % 23.01/3.87 | | | (107) all_55_1 = 0 % 23.01/3.87 | | | % 23.01/3.87 | | | GROUND_INST: instantiating (12) with all_51_1, all_55_1, all_40_0, % 23.01/3.87 | | | simplifying with (51), (59) gives: % 23.01/3.87 | | | (108) all_55_1 = all_51_1 % 23.01/3.87 | | | % 23.01/3.87 | | | COMBINE_EQS: (102), (103) imply: % 23.01/3.87 | | | (109) all_69_1 = all_57_1 % 23.01/3.87 | | | % 23.01/3.87 | | | SIMP: (109) implies: % 23.01/3.87 | | | (110) all_69_1 = all_57_1 % 23.01/3.87 | | | % 23.01/3.87 | | | COMBINE_EQS: (97), (98) imply: % 23.01/3.87 | | | (111) all_57_2 = 0 % 23.01/3.87 | | | % 23.01/3.87 | | | COMBINE_EQS: (98), (99) imply: % 23.01/3.87 | | | (112) all_57_2 = all_53_2 % 23.01/3.87 | | | % 23.01/3.87 | | | COMBINE_EQS: (95), (96) imply: % 23.01/3.87 | | | (113) all_59_2 = all_51_2 % 23.01/3.87 | | | % 23.01/3.87 | | | SIMP: (113) implies: % 23.01/3.87 | | | (114) all_59_2 = all_51_2 % 23.01/3.87 | | | % 23.01/3.87 | | | COMBINE_EQS: (100), (110) imply: % 23.01/3.87 | | | (115) all_57_1 = 0 % 23.01/3.87 | | | % 23.01/3.87 | | | COMBINE_EQS: (101), (110) imply: % 23.01/3.87 | | | (116) all_57_1 = all_53_1 % 23.01/3.87 | | | % 23.01/3.87 | | | COMBINE_EQS: (104), (105) imply: % 23.01/3.87 | | | (117) all_53_0 = all_51_0 % 23.01/3.87 | | | % 23.01/3.87 | | | SIMP: (117) implies: % 23.01/3.87 | | | (118) all_53_0 = all_51_0 % 23.01/3.87 | | | % 23.01/3.87 | | | COMBINE_EQS: (93), (94) imply: % 23.01/3.87 | | | (119) all_55_2 = 0 % 23.01/3.87 | | | % 23.01/3.87 | | | SIMP: (119) implies: % 23.01/3.87 | | | (120) all_55_2 = 0 % 23.01/3.87 | | | % 23.01/3.87 | | | COMBINE_EQS: (92), (114) imply: % 23.01/3.87 | | | (121) all_55_2 = all_51_2 % 23.01/3.87 | | | % 23.01/3.87 | | | SIMP: (121) implies: % 23.01/3.87 | | | (122) all_55_2 = all_51_2 % 23.01/3.87 | | | % 23.01/3.87 | | | COMBINE_EQS: (115), (116) imply: % 23.01/3.87 | | | (123) all_53_1 = 0 % 23.01/3.87 | | | % 23.01/3.87 | | | COMBINE_EQS: (111), (112) imply: % 23.01/3.87 | | | (124) all_53_2 = 0 % 23.01/3.87 | | | % 23.01/3.87 | | | SIMP: (124) implies: % 23.01/3.87 | | | (125) all_53_2 = 0 % 23.01/3.87 | | | % 23.01/3.87 | | | COMBINE_EQS: (107), (108) imply: % 23.01/3.87 | | | (126) all_51_1 = 0 % 23.01/3.87 | | | % 23.01/3.87 | | | COMBINE_EQS: (120), (122) imply: % 23.01/3.87 | | | (127) all_51_2 = 0 % 23.01/3.87 | | | % 23.01/3.87 | | | SIMP: (127) implies: % 23.01/3.87 | | | (128) all_51_2 = 0 % 23.01/3.87 | | | % 23.01/3.88 | | | COMBINE_EQS: (114), (128) imply: % 23.01/3.88 | | | (129) all_59_2 = 0 % 23.01/3.88 | | | % 23.01/3.88 | | | COMBINE_EQS: (96), (128) imply: % 23.01/3.88 | | | (130) all_74_3 = 0 % 23.01/3.88 | | | % 23.01/3.88 | | | COMBINE_EQS: (103), (115) imply: % 23.01/3.88 | | | (131) all_74_1 = 0 % 23.01/3.88 | | | % 23.01/3.88 | | | BETA: splitting (91) gives: % 23.01/3.88 | | | % 23.01/3.88 | | | Case 1: % 23.01/3.88 | | | | % 23.01/3.88 | | | | (132) ~ (all_74_0 = 0) % 23.01/3.88 | | | | % 23.01/3.88 | | | | BETA: splitting (61) gives: % 23.01/3.88 | | | | % 23.01/3.88 | | | | Case 1: % 23.01/3.88 | | | | | % 23.01/3.88 | | | | | (133) ~ (all_55_1 = 0) % 23.01/3.88 | | | | | % 23.01/3.88 | | | | | REDUCE: (107), (133) imply: % 23.01/3.88 | | | | | (134) $false % 23.01/3.88 | | | | | % 23.01/3.88 | | | | | CLOSE: (134) is inconsistent. % 23.01/3.88 | | | | | % 23.01/3.88 | | | | Case 2: % 23.01/3.88 | | | | | % 23.01/3.88 | | | | | (135) ~ (all_55_2 = 0) | all_55_0 = all_33_0 % 23.01/3.88 | | | | | % 23.01/3.88 | | | | | DELTA: instantiating (20) with fresh symbol all_90_0 gives: % 23.01/3.88 | | | | | (136) sdtasdt0(xl, all_90_0) = xm & aNaturalNumber0(all_90_0) = 0 & % 23.01/3.88 | | | | | $i(all_90_0) % 23.01/3.88 | | | | | % 23.01/3.88 | | | | | ALPHA: (136) implies: % 23.01/3.88 | | | | | (137) $i(all_90_0) % 23.01/3.88 | | | | | (138) sdtasdt0(xl, all_90_0) = xm % 23.01/3.88 | | | | | % 23.01/3.88 | | | | | BETA: splitting (52) gives: % 23.01/3.88 | | | | | % 23.01/3.88 | | | | | Case 1: % 23.01/3.88 | | | | | | % 23.01/3.88 | | | | | | (139) ~ (all_51_1 = 0) % 23.01/3.88 | | | | | | % 23.01/3.88 | | | | | | REDUCE: (126), (139) imply: % 23.01/3.88 | | | | | | (140) $false % 23.01/3.88 | | | | | | % 23.01/3.88 | | | | | | CLOSE: (140) is inconsistent. % 23.01/3.88 | | | | | | % 23.01/3.88 | | | | | Case 2: % 23.01/3.88 | | | | | | % 23.01/3.88 | | | | | | (141) ~ (all_51_2 = 0) | all_51_0 = 0 % 23.01/3.88 | | | | | | % 23.01/3.88 | | | | | | BETA: splitting (141) gives: % 23.01/3.88 | | | | | | % 23.01/3.88 | | | | | | Case 1: % 23.01/3.88 | | | | | | | % 23.01/3.88 | | | | | | | (142) ~ (all_51_2 = 0) % 23.01/3.88 | | | | | | | % 23.01/3.88 | | | | | | | REDUCE: (128), (142) imply: % 23.01/3.88 | | | | | | | (143) $false % 23.01/3.88 | | | | | | | % 23.01/3.88 | | | | | | | CLOSE: (143) is inconsistent. % 23.01/3.88 | | | | | | | % 23.01/3.88 | | | | | | Case 2: % 23.01/3.88 | | | | | | | % 23.01/3.88 | | | | | | | (144) all_51_0 = 0 % 23.01/3.88 | | | | | | | % 23.01/3.88 | | | | | | | COMBINE_EQS: (105), (144) imply: % 23.01/3.88 | | | | | | | (145) all_69_2 = 0 % 23.01/3.88 | | | | | | | % 23.01/3.88 | | | | | | | REDUCE: (50), (144) imply: % 23.01/3.88 | | | | | | | (146) aNaturalNumber0(all_33_0) = 0 % 23.01/3.88 | | | | | | | % 23.01/3.88 | | | | | | | BETA: splitting (135) gives: % 23.01/3.88 | | | | | | | % 23.01/3.88 | | | | | | | Case 1: % 23.01/3.88 | | | | | | | | % 23.01/3.88 | | | | | | | | (147) ~ (all_55_2 = 0) % 23.01/3.88 | | | | | | | | % 23.01/3.88 | | | | | | | | REDUCE: (120), (147) imply: % 23.01/3.88 | | | | | | | | (148) $false % 23.01/3.88 | | | | | | | | % 23.01/3.88 | | | | | | | | CLOSE: (148) is inconsistent. % 23.01/3.88 | | | | | | | | % 23.01/3.88 | | | | | | | Case 2: % 23.01/3.88 | | | | | | | | % 23.01/3.88 | | | | | | | | (149) all_55_0 = all_33_0 % 23.01/3.88 | | | | | | | | % 23.01/3.88 | | | | | | | | REDUCE: (60), (149) imply: % 23.01/3.88 | | | | | | | | (150) sdtasdt0(all_40_0, xl) = all_33_0 % 23.01/3.88 | | | | | | | | % 23.01/3.88 | | | | | | | | BETA: splitting (73) gives: % 23.01/3.88 | | | | | | | | % 23.01/3.88 | | | | | | | | Case 1: % 23.01/3.88 | | | | | | | | | % 23.01/3.88 | | | | | | | | | (151) ~ (all_59_1 = 0) % 23.01/3.88 | | | | | | | | | % 23.01/3.88 | | | | | | | | | REDUCE: (106), (151) imply: % 23.01/3.88 | | | | | | | | | (152) $false % 23.01/3.88 | | | | | | | | | % 23.01/3.88 | | | | | | | | | CLOSE: (152) is inconsistent. % 23.01/3.88 | | | | | | | | | % 23.01/3.88 | | | | | | | | Case 2: % 23.01/3.88 | | | | | | | | | % 23.01/3.88 | | | | | | | | | (153) ~ (all_59_2 = 0) | all_59_0 = xm % 23.01/3.88 | | | | | | | | | % 23.01/3.88 | | | | | | | | | DELTA: instantiating (21) with fresh symbol all_111_0 gives: % 23.01/3.88 | | | | | | | | | (154) sdtasdt0(xl, all_111_0) = all_33_0 & % 23.01/3.88 | | | | | | | | | aNaturalNumber0(all_111_0) = 0 & $i(all_111_0) % 23.01/3.88 | | | | | | | | | % 23.01/3.88 | | | | | | | | | ALPHA: (154) implies: % 23.01/3.88 | | | | | | | | | (155) $i(all_111_0) % 23.01/3.88 | | | | | | | | | (156) aNaturalNumber0(all_111_0) = 0 % 23.01/3.88 | | | | | | | | | (157) sdtasdt0(xl, all_111_0) = all_33_0 % 23.01/3.88 | | | | | | | | | % 23.01/3.88 | | | | | | | | | BETA: splitting (153) gives: % 23.01/3.88 | | | | | | | | | % 23.01/3.88 | | | | | | | | | Case 1: % 23.01/3.88 | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | (158) ~ (all_59_2 = 0) % 23.01/3.88 | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | REDUCE: (129), (158) imply: % 23.01/3.88 | | | | | | | | | | (159) $false % 23.01/3.88 | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | CLOSE: (159) is inconsistent. % 23.01/3.88 | | | | | | | | | | % 23.01/3.88 | | | | | | | | | Case 2: % 23.01/3.88 | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | (160) all_59_0 = xm % 23.01/3.88 | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | REDUCE: (72), (160) imply: % 23.01/3.88 | | | | | | | | | | (161) sdtasdt0(all_38_0, xl) = xm % 23.01/3.88 | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | BETA: splitting (67) gives: % 23.01/3.88 | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | Case 1: % 23.01/3.88 | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | (162) ~ (all_57_1 = 0) % 23.01/3.88 | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | REDUCE: (115), (162) imply: % 23.01/3.88 | | | | | | | | | | | (163) $false % 23.01/3.88 | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | CLOSE: (163) is inconsistent. % 23.01/3.88 | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | Case 2: % 23.01/3.88 | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | (164) ~ (all_57_2 = 0) | all_57_0 = all_33_0 % 23.01/3.88 | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | BETA: splitting (164) gives: % 23.01/3.88 | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | Case 1: % 23.01/3.88 | | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | | (165) ~ (all_57_2 = 0) % 23.01/3.88 | | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | | REDUCE: (111), (165) imply: % 23.01/3.88 | | | | | | | | | | | | (166) $false % 23.01/3.88 | | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | | CLOSE: (166) is inconsistent. % 23.01/3.88 | | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | Case 2: % 23.01/3.88 | | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | | (167) all_57_0 = all_33_0 % 23.01/3.88 | | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | | REDUCE: (66), (167) imply: % 23.01/3.88 | | | | | | | | | | | | (168) sdtpldt0(xn, xm) = all_33_0 % 23.01/3.88 | | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | | BETA: splitting (82) gives: % 23.01/3.88 | | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | | Case 1: % 23.01/3.88 | | | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | | | (169) ~ (all_69_0 = 0) % 23.01/3.88 | | | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with xl, all_90_0, xm, % 23.01/3.88 | | | | | | | | | | | | | simplifying with (8), (137), (138) gives: % 23.01/3.88 | | | | | | | | | | | | | (170) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 23.01/3.88 | | | | | | | | | | | | | (sdtasdt0(all_90_0, xl) = v2 & % 23.01/3.88 | | | | | | | | | | | | | aNaturalNumber0(all_90_0) = v1 & % 23.01/3.88 | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v2) & ( ~ (v1 = 0) % 23.01/3.88 | | | | | | | | | | | | | | ~ (v0 = 0) | v2 = xm)) % 23.01/3.88 | | | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with xl, all_111_0, % 23.01/3.88 | | | | | | | | | | | | | all_33_0, simplifying with (8), (155), (157) % 23.01/3.88 | | | | | | | | | | | | | gives: % 23.01/3.88 | | | | | | | | | | | | | (171) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 23.01/3.88 | | | | | | | | | | | | | (sdtasdt0(all_111_0, xl) = v2 & % 23.01/3.88 | | | | | | | | | | | | | aNaturalNumber0(all_111_0) = v1 & % 23.01/3.88 | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v2) & ( ~ (v1 = 0) % 23.01/3.88 | | | | | | | | | | | | | | ~ (v0 = 0) | v2 = all_33_0)) % 23.01/3.88 | | | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | | | GROUND_INST: instantiating (mDefDiv) with xm, xn, all_74_0, % 23.01/3.88 | | | | | | | | | | | | | simplifying with (9), (10), (90) gives: % 23.01/3.88 | | | | | | | | | | | | | (172) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(xn) % 23.01/3.88 | | | | | | | | | | | | | = v1 & aNaturalNumber0(xm) = v0 & ( ~ (v1 = 0) | % 23.01/3.88 | | | | | | | | | | | | | ~ (v0 = 0))) | (( ~ (all_74_0 = 0) | ? [v0: % 23.01/3.88 | | | | | | | | | | | | | $i] : (sdtasdt0(xm, v0) = xn & % 23.01/3.88 | | | | | | | | | | | | | aNaturalNumber0(v0) = 0 & $i(v0))) & % 23.01/3.88 | | | | | | | | | | | | | (all_74_0 = 0 | ! [v0: $i] : ( ~ (sdtasdt0(xm, % 23.01/3.88 | | | | | | | | | | | | | v0) = xn) | ~ $i(v0) | ? [v1: int] : ( % 23.01/3.88 | | | | | | | | | | | | | ~ (v1 = 0) & aNaturalNumber0(v0) = v1)))) % 23.01/3.88 | | | | | | | | | | | | | % 23.01/3.88 | | | | | | | | | | | | | GROUND_INST: instantiating (mDefDiv) with all_33_0, xn, % 23.01/3.88 | | | | | | | | | | | | | all_69_0, simplifying with (10), (39), (81) gives: % 23.01/3.89 | | | | | | | | | | | | | (173) ? [v0: any] : ? [v1: any] : % 23.01/3.89 | | | | | | | | | | | | | (aNaturalNumber0(all_33_0) = v0 & % 23.01/3.89 | | | | | | | | | | | | | aNaturalNumber0(xn) = v1 & ( ~ (v1 = 0) | ~ (v0 % 23.01/3.89 | | | | | | | | | | | | | = 0))) | (( ~ (all_69_0 = 0) | ? [v0: $i] : % 23.01/3.89 | | | | | | | | | | | | | (sdtasdt0(all_33_0, v0) = xn & % 23.01/3.89 | | | | | | | | | | | | | aNaturalNumber0(v0) = 0 & $i(v0))) & % 23.01/3.89 | | | | | | | | | | | | | (all_69_0 = 0 | ! [v0: $i] : ( ~ % 23.01/3.89 | | | | | | | | | | | | | (sdtasdt0(all_33_0, v0) = xn) | ~ $i(v0) | % 23.01/3.89 | | | | | | | | | | | | | ? [v1: int] : ( ~ (v1 = 0) & % 23.01/3.89 | | | | | | | | | | | | | aNaturalNumber0(v0) = v1)))) % 23.01/3.89 | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | DELTA: instantiating (171) with fresh symbols all_138_0, % 23.01/3.89 | | | | | | | | | | | | | all_138_1, all_138_2 gives: % 23.01/3.89 | | | | | | | | | | | | | (174) sdtasdt0(all_111_0, xl) = all_138_0 & % 23.01/3.89 | | | | | | | | | | | | | aNaturalNumber0(all_111_0) = all_138_1 & % 23.01/3.89 | | | | | | | | | | | | | aNaturalNumber0(xl) = all_138_2 & $i(all_138_0) & % 23.01/3.89 | | | | | | | | | | | | | ( ~ (all_138_1 = 0) | ~ (all_138_2 = 0) | % 23.01/3.89 | | | | | | | | | | | | | all_138_0 = all_33_0) % 23.01/3.89 | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | ALPHA: (174) implies: % 23.01/3.89 | | | | | | | | | | | | | (175) aNaturalNumber0(xl) = all_138_2 % 23.01/3.89 | | | | | | | | | | | | | (176) aNaturalNumber0(all_111_0) = all_138_1 % 23.01/3.89 | | | | | | | | | | | | | (177) sdtasdt0(all_111_0, xl) = all_138_0 % 23.01/3.89 | | | | | | | | | | | | | (178) ~ (all_138_1 = 0) | ~ (all_138_2 = 0) | % 23.01/3.89 | | | | | | | | | | | | | all_138_0 = all_33_0 % 23.01/3.89 | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | DELTA: instantiating (170) with fresh symbols all_140_0, % 23.01/3.89 | | | | | | | | | | | | | all_140_1, all_140_2 gives: % 23.01/3.89 | | | | | | | | | | | | | (179) sdtasdt0(all_90_0, xl) = all_140_0 & % 23.01/3.89 | | | | | | | | | | | | | aNaturalNumber0(all_90_0) = all_140_1 & % 23.01/3.89 | | | | | | | | | | | | | aNaturalNumber0(xl) = all_140_2 & $i(all_140_0) & % 23.01/3.89 | | | | | | | | | | | | | ( ~ (all_140_1 = 0) | ~ (all_140_2 = 0) | % 23.01/3.89 | | | | | | | | | | | | | all_140_0 = xm) % 23.01/3.89 | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | ALPHA: (179) implies: % 23.01/3.89 | | | | | | | | | | | | | (180) aNaturalNumber0(xl) = all_140_2 % 23.01/3.89 | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | BETA: splitting (173) gives: % 23.01/3.89 | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | Case 1: % 23.01/3.89 | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | (181) ? [v0: any] : ? [v1: any] : % 23.01/3.89 | | | | | | | | | | | | | | (aNaturalNumber0(all_33_0) = v0 & % 23.01/3.89 | | | | | | | | | | | | | | aNaturalNumber0(xn) = v1 & ( ~ (v1 = 0) | ~ (v0 % 23.01/3.89 | | | | | | | | | | | | | | = 0))) % 23.01/3.89 | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | BETA: splitting (172) gives: % 23.01/3.89 | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | Case 1: % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | (182) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(xn) % 23.01/3.89 | | | | | | | | | | | | | | | = v1 & aNaturalNumber0(xm) = v0 & ( ~ (v1 = 0) | % 23.01/3.89 | | | | | | | | | | | | | | | ~ (v0 = 0))) % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | DELTA: instantiating (181) with fresh symbols all_146_0, % 23.01/3.89 | | | | | | | | | | | | | | | all_146_1 gives: % 23.01/3.89 | | | | | | | | | | | | | | | (183) aNaturalNumber0(all_33_0) = all_146_1 & % 23.01/3.89 | | | | | | | | | | | | | | | aNaturalNumber0(xn) = all_146_0 & ( ~ (all_146_0 = % 23.01/3.89 | | | | | | | | | | | | | | | 0) | ~ (all_146_1 = 0)) % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | ALPHA: (183) implies: % 23.01/3.89 | | | | | | | | | | | | | | | (184) aNaturalNumber0(xn) = all_146_0 % 23.01/3.89 | | | | | | | | | | | | | | | (185) aNaturalNumber0(all_33_0) = all_146_1 % 23.01/3.89 | | | | | | | | | | | | | | | (186) ~ (all_146_0 = 0) | ~ (all_146_1 = 0) % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | DELTA: instantiating (182) with fresh symbols all_148_0, % 23.01/3.89 | | | | | | | | | | | | | | | all_148_1 gives: % 23.01/3.89 | | | | | | | | | | | | | | | (187) aNaturalNumber0(xn) = all_148_0 & % 23.01/3.89 | | | | | | | | | | | | | | | aNaturalNumber0(xm) = all_148_1 & ( ~ (all_148_0 = % 23.01/3.89 | | | | | | | | | | | | | | | 0) | ~ (all_148_1 = 0)) % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | ALPHA: (187) implies: % 23.01/3.89 | | | | | | | | | | | | | | | (188) aNaturalNumber0(xn) = all_148_0 % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with 0, all_148_0, xn, % 23.01/3.89 | | | | | | | | | | | | | | | simplifying with (6), (188) gives: % 23.01/3.89 | | | | | | | | | | | | | | | (189) all_148_0 = 0 % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with all_146_0, all_148_0, xn, % 23.01/3.89 | | | | | | | | | | | | | | | simplifying with (184), (188) gives: % 23.01/3.89 | | | | | | | | | | | | | | | (190) all_148_0 = all_146_0 % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with 0, all_146_1, all_33_0, % 23.01/3.89 | | | | | | | | | | | | | | | simplifying with (146), (185) gives: % 23.01/3.89 | | | | | | | | | | | | | | | (191) all_146_1 = 0 % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | COMBINE_EQS: (189), (190) imply: % 23.01/3.89 | | | | | | | | | | | | | | | (192) all_146_0 = 0 % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | SIMP: (192) implies: % 23.01/3.89 | | | | | | | | | | | | | | | (193) all_146_0 = 0 % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | BETA: splitting (186) gives: % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | Case 1: % 23.01/3.89 | | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | | (194) ~ (all_146_0 = 0) % 23.01/3.89 | | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | | REDUCE: (193), (194) imply: % 23.01/3.89 | | | | | | | | | | | | | | | | (195) $false % 23.01/3.89 | | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | | CLOSE: (195) is inconsistent. % 23.01/3.89 | | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | Case 2: % 23.01/3.89 | | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | | (196) ~ (all_146_1 = 0) % 23.01/3.89 | | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | | REDUCE: (191), (196) imply: % 23.01/3.89 | | | | | | | | | | | | | | | | (197) $false % 23.01/3.89 | | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | | CLOSE: (197) is inconsistent. % 23.01/3.89 | | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | End of split % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | Case 2: % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | DELTA: instantiating (181) with fresh symbols all_146_0, % 23.01/3.89 | | | | | | | | | | | | | | | all_146_1 gives: % 23.01/3.89 | | | | | | | | | | | | | | | (198) aNaturalNumber0(all_33_0) = all_146_1 & % 23.01/3.89 | | | | | | | | | | | | | | | aNaturalNumber0(xn) = all_146_0 & ( ~ (all_146_0 = % 23.01/3.89 | | | | | | | | | | | | | | | 0) | ~ (all_146_1 = 0)) % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | ALPHA: (198) implies: % 23.01/3.89 | | | | | | | | | | | | | | | (199) aNaturalNumber0(xn) = all_146_0 % 23.01/3.89 | | | | | | | | | | | | | | | (200) aNaturalNumber0(all_33_0) = all_146_1 % 23.01/3.89 | | | | | | | | | | | | | | | (201) ~ (all_146_0 = 0) | ~ (all_146_1 = 0) % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with 0, all_146_0, xn, % 23.01/3.89 | | | | | | | | | | | | | | | simplifying with (6), (199) gives: % 23.01/3.89 | | | | | | | | | | | | | | | (202) all_146_0 = 0 % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with 0, all_146_1, all_33_0, % 23.01/3.89 | | | | | | | | | | | | | | | simplifying with (146), (200) gives: % 23.01/3.89 | | | | | | | | | | | | | | | (203) all_146_1 = 0 % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | BETA: splitting (201) gives: % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | Case 1: % 23.01/3.89 | | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | | (204) ~ (all_146_0 = 0) % 23.01/3.89 | | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | | REDUCE: (202), (204) imply: % 23.01/3.89 | | | | | | | | | | | | | | | | (205) $false % 23.01/3.89 | | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | | CLOSE: (205) is inconsistent. % 23.01/3.89 | | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | Case 2: % 23.01/3.89 | | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | | (206) ~ (all_146_1 = 0) % 23.01/3.89 | | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | | REDUCE: (203), (206) imply: % 23.01/3.89 | | | | | | | | | | | | | | | | (207) $false % 23.01/3.89 | | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | | CLOSE: (207) is inconsistent. % 23.01/3.89 | | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | End of split % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | End of split % 23.01/3.89 | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | Case 2: % 23.01/3.89 | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | (208) ( ~ (all_69_0 = 0) | ? [v0: $i] : % 23.01/3.89 | | | | | | | | | | | | | | (sdtasdt0(all_33_0, v0) = xn & % 23.01/3.89 | | | | | | | | | | | | | | aNaturalNumber0(v0) = 0 & $i(v0))) & (all_69_0 % 23.01/3.89 | | | | | | | | | | | | | | = 0 | ! [v0: $i] : ( ~ (sdtasdt0(all_33_0, v0) % 23.01/3.89 | | | | | | | | | | | | | | = xn) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = % 23.01/3.89 | | | | | | | | | | | | | | 0) & aNaturalNumber0(v0) = v1))) % 23.01/3.89 | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | ALPHA: (208) implies: % 23.01/3.89 | | | | | | | | | | | | | | (209) all_69_0 = 0 | ! [v0: $i] : ( ~ % 23.01/3.89 | | | | | | | | | | | | | | (sdtasdt0(all_33_0, v0) = xn) | ~ $i(v0) | ? % 23.01/3.89 | | | | | | | | | | | | | | [v1: int] : ( ~ (v1 = 0) & aNaturalNumber0(v0) = % 23.01/3.89 | | | | | | | | | | | | | | v1)) % 23.01/3.89 | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | BETA: splitting (172) gives: % 23.01/3.89 | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | Case 1: % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | (210) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(xn) % 23.01/3.89 | | | | | | | | | | | | | | | = v1 & aNaturalNumber0(xm) = v0 & ( ~ (v1 = 0) | % 23.01/3.89 | | | | | | | | | | | | | | | ~ (v0 = 0))) % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | DELTA: instantiating (210) with fresh symbols all_146_0, % 23.01/3.89 | | | | | | | | | | | | | | | all_146_1 gives: % 23.01/3.89 | | | | | | | | | | | | | | | (211) aNaturalNumber0(xn) = all_146_0 & % 23.01/3.89 | | | | | | | | | | | | | | | aNaturalNumber0(xm) = all_146_1 & ( ~ (all_146_0 = % 23.01/3.89 | | | | | | | | | | | | | | | 0) | ~ (all_146_1 = 0)) % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | ALPHA: (211) implies: % 23.01/3.89 | | | | | | | | | | | | | | | (212) aNaturalNumber0(xm) = all_146_1 % 23.01/3.89 | | | | | | | | | | | | | | | (213) aNaturalNumber0(xn) = all_146_0 % 23.01/3.89 | | | | | | | | | | | | | | | (214) ~ (all_146_0 = 0) | ~ (all_146_1 = 0) % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | BETA: splitting (209) gives: % 23.01/3.89 | | | | | | | | | | | | | | | % 23.01/3.89 | | | | | | | | | | | | | | | Case 1: % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | (215) all_69_0 = 0 % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | REDUCE: (169), (215) imply: % 23.01/3.90 | | | | | | | | | | | | | | | | (216) $false % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | CLOSE: (216) is inconsistent. % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | Case 2: % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with 0, all_146_1, xm, % 23.01/3.90 | | | | | | | | | | | | | | | | simplifying with (5), (212) gives: % 23.01/3.90 | | | | | | | | | | | | | | | | (217) all_146_1 = 0 % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with 0, all_146_0, xn, % 23.01/3.90 | | | | | | | | | | | | | | | | simplifying with (6), (213) gives: % 23.01/3.90 | | | | | | | | | | | | | | | | (218) all_146_0 = 0 % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | BETA: splitting (214) gives: % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | Case 1: % 23.01/3.90 | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | (219) ~ (all_146_0 = 0) % 23.01/3.90 | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | REDUCE: (218), (219) imply: % 23.01/3.90 | | | | | | | | | | | | | | | | | (220) $false % 23.01/3.90 | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | CLOSE: (220) is inconsistent. % 23.01/3.90 | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | Case 2: % 23.01/3.90 | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | (221) ~ (all_146_1 = 0) % 23.01/3.90 | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | REDUCE: (217), (221) imply: % 23.01/3.90 | | | | | | | | | | | | | | | | | (222) $false % 23.01/3.90 | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | CLOSE: (222) is inconsistent. % 23.01/3.90 | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | End of split % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | End of split % 23.01/3.90 | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | Case 2: % 23.01/3.90 | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | (223) ( ~ (all_74_0 = 0) | ? [v0: $i] : (sdtasdt0(xm, % 23.01/3.90 | | | | | | | | | | | | | | | v0) = xn & aNaturalNumber0(v0) = 0 & % 23.01/3.90 | | | | | | | | | | | | | | | $i(v0))) & (all_74_0 = 0 | ! [v0: $i] : ( ~ % 23.01/3.90 | | | | | | | | | | | | | | | (sdtasdt0(xm, v0) = xn) | ~ $i(v0) | ? [v1: % 23.01/3.90 | | | | | | | | | | | | | | | int] : ( ~ (v1 = 0) & aNaturalNumber0(v0) = % 23.01/3.90 | | | | | | | | | | | | | | | v1))) % 23.01/3.90 | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | ALPHA: (223) implies: % 23.01/3.90 | | | | | | | | | | | | | | | (224) all_74_0 = 0 | ! [v0: $i] : ( ~ (sdtasdt0(xm, v0) % 23.01/3.90 | | | | | | | | | | | | | | | = xn) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = % 23.01/3.90 | | | | | | | | | | | | | | | 0) & aNaturalNumber0(v0) = v1)) % 23.01/3.90 | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | BETA: splitting (224) gives: % 23.01/3.90 | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | Case 1: % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | (225) all_74_0 = 0 % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | REDUCE: (132), (225) imply: % 23.01/3.90 | | | | | | | | | | | | | | | | (226) $false % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | CLOSE: (226) is inconsistent. % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | Case 2: % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with 0, all_140_2, xl, % 23.01/3.90 | | | | | | | | | | | | | | | | simplifying with (4), (180) gives: % 23.01/3.90 | | | | | | | | | | | | | | | | (227) all_140_2 = 0 % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with all_138_2, all_140_2, xl, % 23.01/3.90 | | | | | | | | | | | | | | | | simplifying with (175), (180) gives: % 23.01/3.90 | | | | | | | | | | | | | | | | (228) all_140_2 = all_138_2 % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with 0, all_138_1, all_111_0, % 23.01/3.90 | | | | | | | | | | | | | | | | simplifying with (156), (176) gives: % 23.01/3.90 | | | | | | | | | | | | | | | | (229) all_138_1 = 0 % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | COMBINE_EQS: (227), (228) imply: % 23.01/3.90 | | | | | | | | | | | | | | | | (230) all_138_2 = 0 % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | BETA: splitting (178) gives: % 23.01/3.90 | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | Case 1: % 23.01/3.90 | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | (231) ~ (all_138_1 = 0) % 23.01/3.90 | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | REDUCE: (229), (231) imply: % 23.01/3.90 | | | | | | | | | | | | | | | | | (232) $false % 23.01/3.90 | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | CLOSE: (232) is inconsistent. % 23.01/3.90 | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | Case 2: % 23.01/3.90 | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | (233) ~ (all_138_2 = 0) | all_138_0 = all_33_0 % 23.01/3.90 | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | BETA: splitting (233) gives: % 23.01/3.90 | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | Case 1: % 23.01/3.90 | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | (234) ~ (all_138_2 = 0) % 23.01/3.90 | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | REDUCE: (230), (234) imply: % 23.01/3.90 | | | | | | | | | | | | | | | | | | (235) $false % 23.01/3.90 | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | CLOSE: (235) is inconsistent. % 23.01/3.90 | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | Case 2: % 23.01/3.90 | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | (236) all_138_0 = all_33_0 % 23.01/3.90 | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | REDUCE: (177), (236) imply: % 23.01/3.90 | | | | | | | | | | | | | | | | | | (237) sdtasdt0(all_111_0, xl) = all_33_0 % 23.01/3.90 | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | BETA: splitting (28) gives: % 23.01/3.90 | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | Case 1: % 23.01/3.90 | | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (238) xl = sz00 % 23.01/3.90 | | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | | REDUCE: (19), (238) imply: % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (239) doDivides0(sz00, all_33_0) = 0 % 23.01/3.90 | | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | | REDUCE: (27), (238) imply: % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (240) doDivides0(sz00, xn) = all_35_0 % 23.01/3.90 | | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | | REDUCE: (237), (238) imply: % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (241) sdtasdt0(all_111_0, sz00) = all_33_0 % 23.01/3.90 | | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | | REDUCE: (150), (238) imply: % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (242) sdtasdt0(all_40_0, sz00) = all_33_0 % 23.01/3.90 | | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | | REDUCE: (161), (238) imply: % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (243) sdtasdt0(all_38_0, sz00) = xm % 23.01/3.90 | | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | | REDUCE: (157), (238) imply: % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (244) sdtasdt0(sz00, all_111_0) = all_33_0 % 23.01/3.90 | | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | | REDUCE: (37), (238) imply: % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (245) sdtasdt0(sz00, all_40_0) = all_33_0 % 23.01/3.90 | | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | | REDUCE: (33), (238) imply: % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (246) sdtasdt0(sz00, all_38_0) = xm % 23.01/3.90 | | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (2) with all_38_0, xm, simplifying % 23.01/3.90 | | | | | | | | | | | | | | | | | | | with (31), (246) gives: % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (247) ? [v0: any] : ? [v1: $i] : (sdtasdt0(all_38_0, % 23.01/3.90 | | | | | | | | | | | | | | | | | | | sz00) = v1 & aNaturalNumber0(all_38_0) = v0 & % 23.01/3.90 | | | | | | | | | | | | | | | | | | | $i(v1) & ( ~ (v0 = 0) | (v1 = sz00 & xm = % 23.01/3.90 | | | | | | | | | | | | | | | | | | | sz00))) % 23.01/3.90 | | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (2) with all_40_0, all_33_0, % 23.01/3.90 | | | | | | | | | | | | | | | | | | | simplifying with (35), (245) gives: % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (248) ? [v0: any] : ? [v1: $i] : (sdtasdt0(all_40_0, % 23.01/3.90 | | | | | | | | | | | | | | | | | | | sz00) = v1 & aNaturalNumber0(all_40_0) = v0 & % 23.01/3.90 | | | | | | | | | | | | | | | | | | | $i(v1) & ( ~ (v0 = 0) | (v1 = sz00 & all_33_0 = % 23.01/3.90 | | | | | | | | | | | | | | | | | | | sz00))) % 23.01/3.90 | | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (2) with all_111_0, all_33_0, % 23.01/3.90 | | | | | | | | | | | | | | | | | | | simplifying with (155), (244) gives: % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (249) ? [v0: any] : ? [v1: $i] : (sdtasdt0(all_111_0, % 23.01/3.90 | | | | | | | | | | | | | | | | | | | sz00) = v1 & aNaturalNumber0(all_111_0) = v0 & % 23.01/3.90 | | | | | | | | | | | | | | | | | | | $i(v1) & ( ~ (v0 = 0) | (v1 = sz00 & all_33_0 = % 23.01/3.90 | | | | | | | | | | | | | | | | | | | sz00))) % 23.01/3.90 | | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (249) with fresh symbols all_185_0, % 23.01/3.90 | | | | | | | | | | | | | | | | | | | all_185_1 gives: % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (250) sdtasdt0(all_111_0, sz00) = all_185_0 & % 23.01/3.90 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_111_0) = all_185_1 & % 23.01/3.90 | | | | | | | | | | | | | | | | | | | $i(all_185_0) & ( ~ (all_185_1 = 0) | (all_185_0 = % 23.01/3.90 | | | | | | | | | | | | | | | | | | | sz00 & all_33_0 = sz00)) % 23.01/3.90 | | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | | ALPHA: (250) implies: % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (251) $i(all_185_0) % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (252) sdtasdt0(all_111_0, sz00) = all_185_0 % 23.01/3.90 | | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (248) with fresh symbols all_189_0, % 23.01/3.90 | | | | | | | | | | | | | | | | | | | all_189_1 gives: % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (253) sdtasdt0(all_40_0, sz00) = all_189_0 & % 23.01/3.90 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_40_0) = all_189_1 & % 23.01/3.90 | | | | | | | | | | | | | | | | | | | $i(all_189_0) & ( ~ (all_189_1 = 0) | (all_189_0 = % 23.01/3.90 | | | | | | | | | | | | | | | | | | | sz00 & all_33_0 = sz00)) % 23.01/3.90 | | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | | ALPHA: (253) implies: % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (254) aNaturalNumber0(all_40_0) = all_189_1 % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (255) sdtasdt0(all_40_0, sz00) = all_189_0 % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (256) ~ (all_189_1 = 0) | (all_189_0 = sz00 & all_33_0 % 23.01/3.90 | | | | | | | | | | | | | | | | | | | = sz00) % 23.01/3.90 | | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (247) with fresh symbols all_191_0, % 23.01/3.90 | | | | | | | | | | | | | | | | | | | all_191_1 gives: % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (257) sdtasdt0(all_38_0, sz00) = all_191_0 & % 23.01/3.90 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_38_0) = all_191_1 & % 23.01/3.90 | | | | | | | | | | | | | | | | | | | $i(all_191_0) & ( ~ (all_191_1 = 0) | (all_191_0 = % 23.01/3.90 | | | | | | | | | | | | | | | | | | | sz00 & xm = sz00)) % 23.01/3.90 | | | | | | | | | | | | | | | | | | | % 23.01/3.90 | | | | | | | | | | | | | | | | | | | ALPHA: (257) implies: % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (258) aNaturalNumber0(all_38_0) = all_191_1 % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (259) sdtasdt0(all_38_0, sz00) = all_191_0 % 23.01/3.90 | | | | | | | | | | | | | | | | | | | (260) ~ (all_191_1 = 0) | (all_191_0 = sz00 & xm = % 23.01/3.91 | | | | | | | | | | | | | | | | | | | sz00) % 23.01/3.91 | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with 0, all_191_1, all_38_0, % 23.01/3.91 | | | | | | | | | | | | | | | | | | | simplifying with (32), (258) gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | (261) all_191_1 = 0 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with 0, all_189_1, all_40_0, % 23.01/3.91 | | | | | | | | | | | | | | | | | | | simplifying with (36), (254) gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | (262) all_189_1 = 0 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with xm, all_191_0, sz00, % 23.01/3.91 | | | | | | | | | | | | | | | | | | | all_38_0, simplifying with (243), (259) gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | (263) all_191_0 = xm % 23.01/3.91 | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with all_33_0, all_189_0, sz00, % 23.01/3.91 | | | | | | | | | | | | | | | | | | | all_40_0, simplifying with (242), (255) gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | (264) all_189_0 = all_33_0 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with all_33_0, all_185_0, sz00, % 23.01/3.91 | | | | | | | | | | | | | | | | | | | all_111_0, simplifying with (241), (252) gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | (265) all_185_0 = all_33_0 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | BETA: splitting (260) gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | Case 1: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | (266) ~ (all_191_1 = 0) % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | REDUCE: (261), (266) imply: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | (267) $false % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | CLOSE: (267) is inconsistent. % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | Case 2: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | (268) all_191_0 = sz00 & xm = sz00 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | ALPHA: (268) implies: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | (269) all_191_0 = sz00 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (263), (269) imply: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | (270) xm = sz00 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | REDUCE: (90), (270) imply: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | (271) doDivides0(sz00, xn) = all_74_0 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | REDUCE: (17), (270) imply: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | (272) sdtpldt0(sz00, xn) = all_33_0 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | BETA: splitting (256) gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | Case 1: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | (273) ~ (all_189_1 = 0) % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | REDUCE: (262), (273) imply: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | (274) $false % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | CLOSE: (274) is inconsistent. % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | Case 2: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | (275) all_189_0 = sz00 & all_33_0 = sz00 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | ALPHA: (275) implies: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | (276) all_189_0 = sz00 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (264), (276) imply: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | (277) all_33_0 = sz00 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | REDUCE: (81), (277) imply: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | (278) doDivides0(sz00, xn) = all_69_0 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | REDUCE: (239), (277) imply: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | (279) doDivides0(sz00, sz00) = 0 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | REDUCE: (272), (277) imply: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | (280) sdtpldt0(sz00, xn) = sz00 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | REDUCE: (39), (277) imply: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | (281) $i(sz00) % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (15) with all_35_0, all_74_0, xn, % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | sz00, simplifying with (240), (271) gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | (282) all_74_0 = all_35_0 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (15) with all_69_0, all_74_0, xn, % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | sz00, simplifying with (271), (278) gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | (283) all_74_0 = all_69_0 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (282), (283) imply: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | (284) all_69_0 = all_35_0 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | BETA: splitting (40) gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | Case 1: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | (285) xn = sz00 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (240), (285) imply: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | (286) doDivides0(sz00, sz00) = all_35_0 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (15) with 0, all_35_0, sz00, sz00, % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | simplifying with (279), (286) gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | (287) all_35_0 = 0 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (23), (287) imply: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | (288) $false % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | CLOSE: (288) is inconsistent. % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | Case 2: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | (289) ~ (xn = sz00) % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mAddAsso) with sz00, xn, xn, sz00, % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | sz00, simplifying with (10), (280), (281) gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | (290) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | [v3: $i] : ? [v4: $i] : (sdtpldt0(xn, xn) = v3 & % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | sdtpldt0(sz00, v3) = v4 & aNaturalNumber0(xn) = % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | v2 & aNaturalNumber0(xn) = v1 & % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(sz00) = v0 & $i(v4) & $i(v3) & ( % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | sz00)) % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (1) with xn, sz00, simplifying with % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | (10), (280) gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | (291) ? [v0: any] : ? [v1: $i] : (sdtpldt0(xn, sz00) = % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | v1 & aNaturalNumber0(xn) = v0 & $i(v1) & ( ~ (v0 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | = 0) | (v1 = sz00 & xn = sz00))) % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (291) with fresh symbols all_235_0, % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | all_235_1 gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | (292) sdtpldt0(xn, sz00) = all_235_0 & % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xn) = all_235_1 & $i(all_235_0) & % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | ( ~ (all_235_1 = 0) | (all_235_0 = sz00 & xn = % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | sz00)) % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | ALPHA: (292) implies: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | (293) aNaturalNumber0(xn) = all_235_1 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | (294) ~ (all_235_1 = 0) | (all_235_0 = sz00 & xn = % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | sz00) % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (290) with fresh symbols all_255_0, % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | all_255_1, all_255_2, all_255_3, all_255_4 gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | (295) sdtpldt0(xn, xn) = all_255_1 & sdtpldt0(sz00, % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | all_255_1) = all_255_0 & aNaturalNumber0(xn) = % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | all_255_2 & aNaturalNumber0(xn) = all_255_3 & % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | aNaturalNumber0(sz00) = all_255_4 & $i(all_255_0) % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | & $i(all_255_1) & ( ~ (all_255_2 = 0) | ~ % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | (all_255_3 = 0) | ~ (all_255_4 = 0) | all_255_0 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | = sz00) % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | ALPHA: (295) implies: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | (296) aNaturalNumber0(xn) = all_255_3 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | (297) aNaturalNumber0(xn) = all_255_2 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (294) gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | Case 1: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | (298) ~ (all_235_1 = 0) % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with 0, all_255_3, xn, % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | simplifying with (6), (296) gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | (299) all_255_3 = 0 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with all_255_3, all_255_2, xn, % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | simplifying with (296), (297) gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | (300) all_255_2 = all_255_3 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with all_235_1, all_255_2, xn, % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | simplifying with (293), (297) gives: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | (301) all_255_2 = all_235_1 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (300), (301) imply: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | (302) all_255_3 = all_235_1 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | SIMP: (302) implies: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | (303) all_255_3 = all_235_1 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (299), (303) imply: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | (304) all_235_1 = 0 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (298), (304) imply: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | (305) $false % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (305) is inconsistent. % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | Case 2: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | (306) all_235_0 = sz00 & xn = sz00 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (306) implies: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | (307) xn = sz00 % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (289), (307) imply: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | (308) $false % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (308) is inconsistent. % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | End of split % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | End of split % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | End of split % 23.01/3.91 | | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | | End of split % 23.01/3.91 | | | | | | | | | | | | | | | | | | | % 23.01/3.91 | | | | | | | | | | | | | | | | | | Case 2: % 23.01/3.91 | | | | | | | | | | | | | | | | | | | % 23.01/3.92 | | | | | | | | | | | | | | | | | | | (309) sdtasdt0(xl, all_35_3) = xm & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_3) = 0 & ? [v0: $i] : % 23.01/3.92 | | | | | | | | | | | | | | | | | | | (sdtmndt0(all_35_1, all_35_3) = v0 & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | sdtlseqdt0(all_35_3, all_35_1) = 0 & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | sdtasdt0(xl, v0) = xn & sdtasdt0(xl, all_35_1) = % 23.01/3.92 | | | | | | | | | | | | | | | | | | | all_35_2 & sdtpldt0(all_35_3, v0) = all_35_1 & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(v0) = 0 & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_1) = 0 & $i(v0) & ? [v1: % 23.01/3.92 | | | | | | | | | | | | | | | | | | | $i] : (sdtpldt0(all_35_3, v1) = all_35_1 & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(v1) = 0 & $i(v1))) % 23.01/3.92 | | | | | | | | | | | | | | | | | | | % 23.01/3.92 | | | | | | | | | | | | | | | | | | | ALPHA: (309) implies: % 23.01/3.92 | | | | | | | | | | | | | | | | | | | (310) sdtasdt0(xl, all_35_3) = xm % 23.01/3.92 | | | | | | | | | | | | | | | | | | | (311) ? [v0: $i] : (sdtmndt0(all_35_1, all_35_3) = v0 & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | sdtlseqdt0(all_35_3, all_35_1) = 0 & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | sdtasdt0(xl, v0) = xn & sdtasdt0(xl, all_35_1) = % 23.01/3.92 | | | | | | | | | | | | | | | | | | | all_35_2 & sdtpldt0(all_35_3, v0) = all_35_1 & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(v0) = 0 & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_1) = 0 & $i(v0) & ? [v1: % 23.01/3.92 | | | | | | | | | | | | | | | | | | | $i] : (sdtpldt0(all_35_3, v1) = all_35_1 & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(v1) = 0 & $i(v1))) % 23.01/3.92 | | | | | | | | | | | | | | | | | | | % 23.01/3.92 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (311) with fresh symbol all_180_0 % 23.01/3.92 | | | | | | | | | | | | | | | | | | | gives: % 23.01/3.92 | | | | | | | | | | | | | | | | | | | (312) sdtmndt0(all_35_1, all_35_3) = all_180_0 & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | sdtlseqdt0(all_35_3, all_35_1) = 0 & sdtasdt0(xl, % 23.01/3.92 | | | | | | | | | | | | | | | | | | | all_180_0) = xn & sdtasdt0(xl, all_35_1) = % 23.01/3.92 | | | | | | | | | | | | | | | | | | | all_35_2 & sdtpldt0(all_35_3, all_180_0) = % 23.01/3.92 | | | | | | | | | | | | | | | | | | | all_35_1 & aNaturalNumber0(all_180_0) = 0 & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_1) = 0 & $i(all_180_0) & ? % 23.01/3.92 | | | | | | | | | | | | | | | | | | | [v0: $i] : (sdtpldt0(all_35_3, v0) = all_35_1 & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(v0) = 0 & $i(v0)) % 23.01/3.92 | | | | | | | | | | | | | | | | | | | % 23.01/3.92 | | | | | | | | | | | | | | | | | | | ALPHA: (312) implies: % 23.01/3.92 | | | | | | | | | | | | | | | | | | | (313) $i(all_180_0) % 23.01/3.92 | | | | | | | | | | | | | | | | | | | (314) aNaturalNumber0(all_180_0) = 0 % 23.01/3.92 | | | | | | | | | | | | | | | | | | | (315) sdtpldt0(all_35_3, all_180_0) = all_35_1 % 23.01/3.92 | | | | | | | | | | | | | | | | | | | (316) sdtasdt0(xl, all_180_0) = xn % 23.01/3.92 | | | | | | | | | | | | | | | | | | | % 23.01/3.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mAddComm) with all_35_3, all_180_0, % 23.01/3.92 | | | | | | | | | | | | | | | | | | | all_35_1, simplifying with (24), (313), (315) % 23.01/3.92 | | | | | | | | | | | | | | | | | | | gives: % 23.01/3.92 | | | | | | | | | | | | | | | | | | | (317) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 23.01/3.92 | | | | | | | | | | | | | | | | | | | (sdtpldt0(all_180_0, all_35_3) = v2 & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_180_0) = v1 & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_3) = v0 & $i(v2) & ( ~ % 23.01/3.92 | | | | | | | | | | | | | | | | | | | (v1 = 0) | ~ (v0 = 0) | v2 = all_35_1)) % 23.01/3.92 | | | | | | | | | | | | | | | | | | | % 23.01/3.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mAMDistr) with xl, all_180_0, % 23.01/3.92 | | | | | | | | | | | | | | | | | | | all_35_3, xn, xm, all_33_0, simplifying with (8), % 23.01/3.92 | | | | | | | | | | | | | | | | | | | (24), (168), (310), (313), (316) gives: % 23.01/3.92 | | | | | | | | | | | | | | | | | | | (318) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 23.01/3.92 | | | | | | | | | | | | | | | | | | | [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] % 23.01/3.92 | | | | | | | | | | | | | | | | | | | : ? [v7: $i] : ? [v8: $i] : (sdtasdt0(v3, xl) = % 23.01/3.92 | | | | | | | | | | | | | | | | | | | v5 & sdtasdt0(all_180_0, xl) = v6 & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | sdtasdt0(all_35_3, xl) = v7 & sdtasdt0(xl, v3) = % 23.01/3.92 | | | | | | | | | | | | | | | | | | | v4 & sdtpldt0(v6, v7) = v8 & sdtpldt0(all_180_0, % 23.01/3.92 | | | | | | | | | | | | | | | | | | | all_35_3) = v3 & aNaturalNumber0(all_180_0) = % 23.01/3.92 | | | | | | | | | | | | | | | | | | | v1 & aNaturalNumber0(all_35_3) = v2 & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v8) & $i(v7) & % 23.01/3.92 | | | | | | | | | | | | | | | | | | | $i(v6) & $i(v5) & $i(v4) & $i(v3) & ( ~ (v2 = 0) % 23.01/3.92 | | | | | | | | | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0) | (v8 = v5 & v4 = % 23.01/3.92 | | | | | | | | | | | | | | | | | | | all_33_0))) % 23.01/3.92 | | | | | | | | | | | | | | | | | | | % 23.59/3.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mAMDistr) with xl, all_35_3, % 23.59/3.92 | | | | | | | | | | | | | | | | | | | all_180_0, xm, xn, all_33_0, simplifying with (8), % 23.59/3.92 | | | | | | | | | | | | | | | | | | | (17), (24), (310), (313), (316) gives: % 23.59/3.92 | | | | | | | | | | | | | | | | | | | (319) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 23.59/3.92 | | | | | | | | | | | | | | | | | | | [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] % 23.59/3.92 | | | | | | | | | | | | | | | | | | | : ? [v7: $i] : ? [v8: $i] : (sdtasdt0(v3, xl) = % 23.59/3.92 | | | | | | | | | | | | | | | | | | | v5 & sdtasdt0(all_180_0, xl) = v7 & % 23.59/3.92 | | | | | | | | | | | | | | | | | | | sdtasdt0(all_35_3, xl) = v6 & sdtasdt0(xl, v3) = % 23.59/3.92 | | | | | | | | | | | | | | | | | | | v4 & sdtpldt0(v6, v7) = v8 & sdtpldt0(all_35_3, % 23.59/3.92 | | | | | | | | | | | | | | | | | | | all_180_0) = v3 & aNaturalNumber0(all_180_0) = % 23.59/3.92 | | | | | | | | | | | | | | | | | | | v2 & aNaturalNumber0(all_35_3) = v1 & % 23.59/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v8) & $i(v7) & % 23.59/3.92 | | | | | | | | | | | | | | | | | | | $i(v6) & $i(v5) & $i(v4) & $i(v3) & ( ~ (v2 = 0) % 23.59/3.92 | | | | | | | | | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0) | (v8 = v5 & v4 = % 23.59/3.92 | | | | | | | | | | | | | | | | | | | all_33_0))) % 23.59/3.92 | | | | | | | | | | | | | | | | | | | % 23.59/3.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (29) with all_180_0, simplifying % 23.59/3.92 | | | | | | | | | | | | | | | | | | | with (313), (316) gives: % 23.59/3.92 | | | | | | | | | | | | | | | | | | | (320) ? [v0: int] : ( ~ (v0 = 0) & % 23.59/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_180_0) = v0) % 23.59/3.92 | | | | | | | | | | | | | | | | | | | % 23.59/3.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with xl, all_180_0, xn, % 23.59/3.92 | | | | | | | | | | | | | | | | | | | simplifying with (8), (313), (316) gives: % 23.59/3.92 | | | | | | | | | | | | | | | | | | | (321) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 23.59/3.92 | | | | | | | | | | | | | | | | | | | (sdtasdt0(all_180_0, xl) = v2 & % 23.59/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_180_0) = v1 & % 23.59/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v2) & ( ~ (v1 = 0) % 23.59/3.92 | | | | | | | | | | | | | | | | | | | | ~ (v0 = 0) | v2 = xn)) % 23.59/3.92 | | | | | | | | | | | | | | | | | | | % 23.59/3.92 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (320) with fresh symbol all_221_0 % 23.59/3.92 | | | | | | | | | | | | | | | | | | | gives: % 23.59/3.92 | | | | | | | | | | | | | | | | | | | (322) ~ (all_221_0 = 0) & aNaturalNumber0(all_180_0) = % 23.59/3.92 | | | | | | | | | | | | | | | | | | | all_221_0 % 23.59/3.92 | | | | | | | | | | | | | | | | | | | % 23.59/3.92 | | | | | | | | | | | | | | | | | | | ALPHA: (322) implies: % 23.59/3.92 | | | | | | | | | | | | | | | | | | | (323) ~ (all_221_0 = 0) % 23.59/3.92 | | | | | | | | | | | | | | | | | | | (324) aNaturalNumber0(all_180_0) = all_221_0 % 23.59/3.92 | | | | | | | | | | | | | | | | | | | % 23.59/3.92 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (321) with fresh symbols all_225_0, % 23.59/3.92 | | | | | | | | | | | | | | | | | | | all_225_1, all_225_2 gives: % 23.59/3.92 | | | | | | | | | | | | | | | | | | | (325) sdtasdt0(all_180_0, xl) = all_225_0 & % 23.59/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_180_0) = all_225_1 & % 23.59/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = all_225_2 & $i(all_225_0) & % 23.59/3.92 | | | | | | | | | | | | | | | | | | | ( ~ (all_225_1 = 0) | ~ (all_225_2 = 0) | % 23.59/3.92 | | | | | | | | | | | | | | | | | | | all_225_0 = xn) % 23.59/3.92 | | | | | | | | | | | | | | | | | | | % 23.59/3.92 | | | | | | | | | | | | | | | | | | | ALPHA: (325) implies: % 23.59/3.92 | | | | | | | | | | | | | | | | | | | (326) aNaturalNumber0(all_180_0) = all_225_1 % 23.59/3.92 | | | | | | | | | | | | | | | | | | | % 23.59/3.92 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (317) with fresh symbols all_227_0, % 23.59/3.92 | | | | | | | | | | | | | | | | | | | all_227_1, all_227_2 gives: % 23.59/3.92 | | | | | | | | | | | | | | | | | | | (327) sdtpldt0(all_180_0, all_35_3) = all_227_0 & % 23.59/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_180_0) = all_227_1 & % 23.59/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_3) = all_227_2 & % 23.59/3.92 | | | | | | | | | | | | | | | | | | | $i(all_227_0) & ( ~ (all_227_1 = 0) | ~ % 23.59/3.92 | | | | | | | | | | | | | | | | | | | (all_227_2 = 0) | all_227_0 = all_35_1) % 23.59/3.92 | | | | | | | | | | | | | | | | | | | % 23.59/3.92 | | | | | | | | | | | | | | | | | | | ALPHA: (327) implies: % 23.59/3.92 | | | | | | | | | | | | | | | | | | | (328) aNaturalNumber0(all_180_0) = all_227_1 % 23.59/3.92 | | | | | | | | | | | | | | | | | | | % 23.59/3.92 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (319) with fresh symbols all_229_0, % 23.59/3.92 | | | | | | | | | | | | | | | | | | | all_229_1, all_229_2, all_229_3, all_229_4, % 23.59/3.92 | | | | | | | | | | | | | | | | | | | all_229_5, all_229_6, all_229_7, all_229_8 gives: % 23.59/3.92 | | | | | | | | | | | | | | | | | | | (329) sdtasdt0(all_229_5, xl) = all_229_3 & % 23.59/3.92 | | | | | | | | | | | | | | | | | | | sdtasdt0(all_180_0, xl) = all_229_1 & % 23.59/3.92 | | | | | | | | | | | | | | | | | | | sdtasdt0(all_35_3, xl) = all_229_2 & sdtasdt0(xl, % 23.59/3.92 | | | | | | | | | | | | | | | | | | | all_229_5) = all_229_4 & sdtpldt0(all_229_2, % 23.64/3.92 | | | | | | | | | | | | | | | | | | | all_229_1) = all_229_0 & sdtpldt0(all_35_3, % 23.64/3.92 | | | | | | | | | | | | | | | | | | | all_180_0) = all_229_5 & % 23.64/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_180_0) = all_229_6 & % 23.64/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_3) = all_229_7 & % 23.64/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = all_229_8 & $i(all_229_0) & % 23.64/3.92 | | | | | | | | | | | | | | | | | | | $i(all_229_1) & $i(all_229_2) & $i(all_229_3) & % 23.64/3.92 | | | | | | | | | | | | | | | | | | | $i(all_229_4) & $i(all_229_5) & ( ~ (all_229_6 = % 23.64/3.92 | | | | | | | | | | | | | | | | | | | 0) | ~ (all_229_7 = 0) | ~ (all_229_8 = 0) | % 23.64/3.92 | | | | | | | | | | | | | | | | | | | (all_229_0 = all_229_3 & all_229_4 = all_33_0)) % 23.64/3.92 | | | | | | | | | | | | | | | | | | | % 23.64/3.92 | | | | | | | | | | | | | | | | | | | ALPHA: (329) implies: % 23.64/3.92 | | | | | | | | | | | | | | | | | | | (330) aNaturalNumber0(all_180_0) = all_229_6 % 23.64/3.92 | | | | | | | | | | | | | | | | | | | % 23.64/3.92 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (318) with fresh symbols all_231_0, % 23.64/3.92 | | | | | | | | | | | | | | | | | | | all_231_1, all_231_2, all_231_3, all_231_4, % 23.64/3.92 | | | | | | | | | | | | | | | | | | | all_231_5, all_231_6, all_231_7, all_231_8 gives: % 23.64/3.92 | | | | | | | | | | | | | | | | | | | (331) sdtasdt0(all_231_5, xl) = all_231_3 & % 23.64/3.92 | | | | | | | | | | | | | | | | | | | sdtasdt0(all_180_0, xl) = all_231_2 & % 23.64/3.92 | | | | | | | | | | | | | | | | | | | sdtasdt0(all_35_3, xl) = all_231_1 & sdtasdt0(xl, % 23.64/3.92 | | | | | | | | | | | | | | | | | | | all_231_5) = all_231_4 & sdtpldt0(all_231_2, % 23.64/3.92 | | | | | | | | | | | | | | | | | | | all_231_1) = all_231_0 & sdtpldt0(all_180_0, % 23.64/3.92 | | | | | | | | | | | | | | | | | | | all_35_3) = all_231_5 & % 23.64/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_180_0) = all_231_7 & % 23.64/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_35_3) = all_231_6 & % 23.64/3.92 | | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = all_231_8 & $i(all_231_0) & % 23.64/3.92 | | | | | | | | | | | | | | | | | | | $i(all_231_1) & $i(all_231_2) & $i(all_231_3) & % 23.64/3.92 | | | | | | | | | | | | | | | | | | | $i(all_231_4) & $i(all_231_5) & ( ~ (all_231_6 = % 23.64/3.92 | | | | | | | | | | | | | | | | | | | 0) | ~ (all_231_7 = 0) | ~ (all_231_8 = 0) | % 23.64/3.92 | | | | | | | | | | | | | | | | | | | (all_231_0 = all_231_3 & all_231_4 = all_33_0)) % 23.64/3.92 | | | | | | | | | | | | | | | | | | | % 23.64/3.92 | | | | | | | | | | | | | | | | | | | ALPHA: (331) implies: % 23.64/3.92 | | | | | | | | | | | | | | | | | | | (332) aNaturalNumber0(all_180_0) = all_231_7 % 23.64/3.92 | | | | | | | | | | | | | | | | | | | % 23.64/3.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with all_225_1, all_227_1, % 23.64/3.92 | | | | | | | | | | | | | | | | | | | all_180_0, simplifying with (326), (328) gives: % 23.64/3.93 | | | | | | | | | | | | | | | | | | | (333) all_227_1 = all_225_1 % 23.64/3.93 | | | | | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with 0, all_229_6, all_180_0, % 23.64/3.93 | | | | | | | | | | | | | | | | | | | simplifying with (314), (330) gives: % 23.64/3.93 | | | | | | | | | | | | | | | | | | | (334) all_229_6 = 0 % 23.64/3.93 | | | | | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with all_225_1, all_229_6, % 23.64/3.93 | | | | | | | | | | | | | | | | | | | all_180_0, simplifying with (326), (330) gives: % 23.64/3.93 | | | | | | | | | | | | | | | | | | | (335) all_229_6 = all_225_1 % 23.64/3.93 | | | | | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with all_227_1, all_231_7, % 23.64/3.93 | | | | | | | | | | | | | | | | | | | all_180_0, simplifying with (328), (332) gives: % 23.64/3.93 | | | | | | | | | | | | | | | | | | | (336) all_231_7 = all_227_1 % 23.64/3.93 | | | | | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (12) with all_221_0, all_231_7, % 23.64/3.93 | | | | | | | | | | | | | | | | | | | all_180_0, simplifying with (324), (332) gives: % 23.64/3.93 | | | | | | | | | | | | | | | | | | | (337) all_231_7 = all_221_0 % 23.64/3.93 | | | | | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (336), (337) imply: % 23.64/3.93 | | | | | | | | | | | | | | | | | | | (338) all_227_1 = all_221_0 % 23.64/3.93 | | | | | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | | | | | SIMP: (338) implies: % 23.64/3.93 | | | | | | | | | | | | | | | | | | | (339) all_227_1 = all_221_0 % 23.64/3.93 | | | | | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (334), (335) imply: % 23.64/3.93 | | | | | | | | | | | | | | | | | | | (340) all_225_1 = 0 % 23.64/3.93 | | | | | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | | | | | SIMP: (340) implies: % 23.64/3.93 | | | | | | | | | | | | | | | | | | | (341) all_225_1 = 0 % 23.64/3.93 | | | | | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (333), (339) imply: % 23.64/3.93 | | | | | | | | | | | | | | | | | | | (342) all_225_1 = all_221_0 % 23.64/3.93 | | | | | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | | | | | SIMP: (342) implies: % 23.64/3.93 | | | | | | | | | | | | | | | | | | | (343) all_225_1 = all_221_0 % 23.64/3.93 | | | | | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (341), (343) imply: % 23.64/3.93 | | | | | | | | | | | | | | | | | | | (344) all_221_0 = 0 % 23.64/3.93 | | | | | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | | | | | REDUCE: (323), (344) imply: % 23.64/3.93 | | | | | | | | | | | | | | | | | | | (345) $false % 23.64/3.93 | | | | | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | | | | | CLOSE: (345) is inconsistent. % 23.64/3.93 | | | | | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | | | | End of split % 23.64/3.93 | | | | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | | | End of split % 23.64/3.93 | | | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | | End of split % 23.64/3.93 | | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | End of split % 23.64/3.93 | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | End of split % 23.64/3.93 | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | End of split % 23.64/3.93 | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | Case 2: % 23.64/3.93 | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | (346) ~ (all_69_1 = 0) | ~ (all_69_2 = 0) | ~ % 23.64/3.93 | | | | | | | | | | | | | (all_69_3 = 0) % 23.64/3.93 | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | BETA: splitting (346) gives: % 23.64/3.93 | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | Case 1: % 23.64/3.93 | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | (347) ~ (all_69_1 = 0) % 23.64/3.93 | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | REDUCE: (100), (347) imply: % 23.64/3.93 | | | | | | | | | | | | | | (348) $false % 23.64/3.93 | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | CLOSE: (348) is inconsistent. % 23.64/3.93 | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | Case 2: % 23.64/3.93 | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | (349) ~ (all_69_2 = 0) | ~ (all_69_3 = 0) % 23.64/3.93 | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | BETA: splitting (349) gives: % 23.64/3.93 | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | Case 1: % 23.64/3.93 | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | (350) ~ (all_69_2 = 0) % 23.64/3.93 | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | REDUCE: (145), (350) imply: % 23.64/3.93 | | | | | | | | | | | | | | | (351) $false % 23.64/3.93 | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | CLOSE: (351) is inconsistent. % 23.64/3.93 | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | Case 2: % 23.64/3.93 | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | (352) ~ (all_69_3 = 0) % 23.64/3.93 | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | REDUCE: (93), (352) imply: % 23.64/3.93 | | | | | | | | | | | | | | | (353) $false % 23.64/3.93 | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | | CLOSE: (353) is inconsistent. % 23.64/3.93 | | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | | End of split % 23.64/3.93 | | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | | End of split % 23.64/3.93 | | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | | End of split % 23.64/3.93 | | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | | End of split % 23.64/3.93 | | | | | | | | | | | % 23.64/3.93 | | | | | | | | | | End of split % 23.64/3.93 | | | | | | | | | | % 23.64/3.93 | | | | | | | | | End of split % 23.64/3.93 | | | | | | | | | % 23.64/3.93 | | | | | | | | End of split % 23.64/3.93 | | | | | | | | % 23.64/3.93 | | | | | | | End of split % 23.64/3.93 | | | | | | | % 23.64/3.93 | | | | | | End of split % 23.64/3.93 | | | | | | % 23.64/3.93 | | | | | End of split % 23.64/3.93 | | | | | % 23.64/3.93 | | | | End of split % 23.64/3.93 | | | | % 23.64/3.93 | | | Case 2: % 23.64/3.93 | | | | % 23.64/3.93 | | | | (354) ~ (all_74_1 = 0) | ~ (all_74_2 = 0) | ~ (all_74_3 = 0) % 23.64/3.93 | | | | % 23.64/3.93 | | | | BETA: splitting (354) gives: % 23.64/3.93 | | | | % 23.64/3.93 | | | | Case 1: % 23.64/3.93 | | | | | % 23.64/3.93 | | | | | (355) ~ (all_74_1 = 0) % 23.64/3.93 | | | | | % 23.64/3.93 | | | | | REDUCE: (131), (355) imply: % 23.64/3.93 | | | | | (356) $false % 23.64/3.93 | | | | | % 23.64/3.93 | | | | | CLOSE: (356) is inconsistent. % 23.64/3.93 | | | | | % 23.64/3.93 | | | | Case 2: % 23.64/3.93 | | | | | % 23.64/3.93 | | | | | (357) ~ (all_74_2 = 0) | ~ (all_74_3 = 0) % 23.64/3.93 | | | | | % 23.64/3.93 | | | | | BETA: splitting (357) gives: % 23.64/3.93 | | | | | % 23.64/3.93 | | | | | Case 1: % 23.64/3.93 | | | | | | % 23.64/3.93 | | | | | | (358) ~ (all_74_2 = 0) % 23.64/3.93 | | | | | | % 23.64/3.93 | | | | | | REDUCE: (97), (358) imply: % 23.64/3.93 | | | | | | (359) $false % 23.64/3.93 | | | | | | % 23.64/3.93 | | | | | | CLOSE: (359) is inconsistent. % 23.64/3.93 | | | | | | % 23.64/3.93 | | | | | Case 2: % 23.64/3.93 | | | | | | % 23.64/3.93 | | | | | | (360) ~ (all_74_3 = 0) % 23.64/3.93 | | | | | | % 23.64/3.93 | | | | | | REDUCE: (130), (360) imply: % 23.64/3.93 | | | | | | (361) $false % 23.64/3.93 | | | | | | % 23.64/3.93 | | | | | | CLOSE: (361) is inconsistent. % 23.64/3.93 | | | | | | % 23.64/3.93 | | | | | End of split % 23.64/3.93 | | | | | % 23.64/3.93 | | | | End of split % 23.64/3.93 | | | | % 23.64/3.93 | | | End of split % 23.64/3.93 | | | % 23.64/3.93 | | End of split % 23.64/3.93 | | % 23.64/3.93 | End of split % 23.64/3.93 | % 23.64/3.93 End of proof % 23.64/3.93 % SZS output end Proof for theBenchmark % 23.64/3.93 % 23.64/3.93 3300ms %------------------------------------------------------------------------------