%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : NUM492+1 : TPTP v8.1.2. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n008.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:07 EDT 2023 % Result : Theorem 12.19s 2.40s % Output : Proof 23.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.14 % Problem : NUM492+1 : TPTP v8.1.2. Released v4.0.0. % 0.00/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.36 % Computer : n008.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 300 % 0.14/0.36 % DateTime : Fri Aug 25 18:01:32 EDT 2023 % 0.14/0.36 % CPUTime : % 0.21/0.63 ________ _____ % 0.21/0.63 ___ __ \_________(_)________________________________ % 0.21/0.63 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.21/0.63 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.21/0.63 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.21/0.63 % 0.21/0.63 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.21/0.63 (2023-06-19) % 0.21/0.63 % 0.21/0.63 (c) Philipp Rümmer, 2009-2023 % 0.21/0.63 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.21/0.63 Amanda Stjerna. % 0.21/0.63 Free software under BSD-3-Clause. % 0.21/0.63 % 0.21/0.63 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.21/0.63 % 0.21/0.63 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.21/0.64 Running up to 7 provers in parallel. % 0.21/0.66 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.21/0.66 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.21/0.66 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.21/0.66 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.21/0.66 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.21/0.66 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.21/0.66 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.53/1.21 Prover 1: Preprocessing ... % 3.53/1.21 Prover 4: Preprocessing ... % 3.86/1.25 Prover 3: Preprocessing ... % 3.86/1.25 Prover 6: Preprocessing ... % 3.86/1.25 Prover 2: Preprocessing ... % 3.86/1.25 Prover 0: Preprocessing ... % 3.86/1.25 Prover 5: Preprocessing ... % 9.12/1.99 Prover 1: Constructing countermodel ... % 9.12/2.01 Prover 6: Proving ... % 9.60/2.04 Prover 3: Constructing countermodel ... % 9.84/2.10 Prover 5: Constructing countermodel ... % 12.19/2.39 Prover 3: proved (1730ms) % 12.19/2.39 % 12.19/2.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 12.19/2.40 % 12.19/2.40 Prover 5: stopped % 12.19/2.41 Prover 6: stopped % 12.19/2.42 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 12.19/2.42 Prover 2: Proving ... % 12.19/2.42 Prover 2: stopped % 12.19/2.43 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 12.19/2.43 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 12.19/2.43 Prover 4: Constructing countermodel ... % 12.19/2.43 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 13.18/2.53 Prover 0: Proving ... % 13.18/2.54 Prover 7: Preprocessing ... % 13.18/2.56 Prover 8: Preprocessing ... % 13.18/2.57 Prover 0: stopped % 13.18/2.57 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 13.18/2.57 Prover 10: Preprocessing ... % 13.79/2.63 Prover 11: Preprocessing ... % 14.35/2.70 Prover 13: Preprocessing ... % 14.35/2.74 Prover 10: Constructing countermodel ... % 15.09/2.83 Prover 7: Constructing countermodel ... % 15.09/2.84 Prover 8: Warning: ignoring some quantifiers % 15.09/2.86 Prover 8: Constructing countermodel ... % 16.22/3.00 Prover 13: Constructing countermodel ... % 17.34/3.10 Prover 11: Constructing countermodel ... % 22.17/3.81 Prover 1: Found proof (size 323) % 22.17/3.81 Prover 1: proved (3159ms) % 22.17/3.82 Prover 7: stopped % 22.17/3.82 Prover 8: stopped % 22.17/3.82 Prover 4: stopped % 22.17/3.82 Prover 10: Found proof (size 55) % 22.17/3.82 Prover 10: proved (1401ms) % 22.90/3.83 Prover 13: stopped % 22.90/3.83 Prover 11: stopped % 22.90/3.83 % 22.90/3.83 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 22.90/3.83 % 23.18/3.89 % SZS output start Proof for theBenchmark % 23.18/3.90 Assumptions after simplification: % 23.18/3.90 --------------------------------- % 23.18/3.90 % 23.18/3.90 (mAddAsso) % 23.18/3.92 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 23.18/3.92 (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) % 23.18/3.93 | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? % 23.18/3.93 [v9: $i] : (sdtpldt0(v1, v2) = v8 & sdtpldt0(v0, v8) = v9 & % 23.18/3.93 aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & aNaturalNumber0(v0) % 23.18/3.93 = v5 & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v9 = % 23.18/3.93 v4))) % 23.18/3.93 % 23.18/3.93 (mAddComm) % 23.18/3.93 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 23.18/3.93 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 23.18/3.93 (sdtpldt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 % 23.18/3.93 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 23.18/3.93 % 23.18/3.93 (mDefDiff) % 23.18/3.93 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtmndt0(v1, v0) = v2) | ~ % 23.18/3.93 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 23.18/3.93 (sdtlseqdt0(v0, v1) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = % 23.18/3.93 v3 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0))) | ( ! [v3: $i] : (v3 = v2 % 23.18/3.93 | ~ (sdtpldt0(v0, v3) = v1) | ~ $i(v3) | ? [v4: int] : ( ~ (v4 = 0) & % 23.18/3.93 aNaturalNumber0(v3) = v4)) & ! [v3: $i] : ( ~ (sdtpldt0(v0, v2) = v3) % 23.18/3.93 | ~ $i(v2) | (v3 = v1 & aNaturalNumber0(v2) = 0)))) % 23.18/3.93 % 23.18/3.93 (mDivMin) % 23.18/3.93 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (doDivides0(v0, % 23.18/3.93 v3) = 0) | ~ (sdtpldt0(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ % 23.18/3.93 $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: % 23.18/3.93 any] : (doDivides0(v0, v2) = v8 & doDivides0(v0, v1) = v7 & % 23.18/3.93 aNaturalNumber0(v2) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) % 23.18/3.93 = v4 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | v8 = 0))) % 23.18/3.93 % 23.18/3.93 (mDivTrans) % 23.18/3.93 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 23.18/3.93 (doDivides0(v0, v2) = v3) | ~ (doDivides0(v0, v1) = 0) | ~ $i(v2) | ~ % 23.18/3.93 $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: % 23.18/3.93 any] : (doDivides0(v1, v2) = v7 & aNaturalNumber0(v2) = v6 & % 23.18/3.93 aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v7 = 0) | ~ % 23.18/3.94 (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) % 23.18/3.94 % 23.18/3.94 (mLEAsym) % 23.18/3.94 ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (sdtlseqdt0(v0, v1) = 0) | ~ $i(v1) % 23.18/3.94 | ~ $i(v0) | ? [v2: any] : ? [v3: any] : ? [v4: any] : (sdtlseqdt0(v1, % 23.18/3.94 v0) = v4 & aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v4 % 23.18/3.94 = 0) | ~ (v3 = 0) | ~ (v2 = 0)))) % 23.18/3.94 % 23.18/3.94 (mMulComm) % 23.18/3.94 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 23.18/3.94 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 23.18/3.94 (sdtasdt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 % 23.18/3.94 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 23.18/3.94 % 23.18/3.94 (mSortsB) % 23.18/3.94 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 23.18/3.94 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 23.18/3.94 (aNaturalNumber0(v2) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = % 23.18/3.94 v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 23.18/3.94 % 23.18/3.94 (mSortsB_02) % 23.18/3.94 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 23.18/3.94 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 23.18/3.94 (aNaturalNumber0(v2) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = % 23.18/3.94 v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 23.18/3.94 % 23.18/3.94 (m__) % 23.18/3.94 $i(xr) & $i(xp) & $i(xm) & ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & % 23.18/3.94 doDivides0(xp, v0) = v1 & sdtasdt0(xr, xm) = v0 & $i(v0)) % 23.18/3.94 % 23.18/3.94 (m__1799) % 23.18/3.94 $i(xp) & $i(xm) & $i(xn) & ? [v0: $i] : ? [v1: $i] : (sdtpldt0(v0, xp) = v1 % 23.18/3.94 & sdtpldt0(xn, xm) = v0 & $i(v1) & $i(v0) & ! [v2: $i] : ! [v3: $i] : ! % 23.18/3.94 [v4: $i] : ! [v5: $i] : ( ~ (doDivides0(v4, v5) = 0) | ~ (sdtasdt0(v2, v3) % 23.18/3.94 = v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ? [v6: any] : ? [v7: any] % 23.18/3.94 : ? [v8: any] : ? [v9: any] : ? [v10: $i] : ? [v11: $i] : ? [v12: % 23.18/3.94 any] : ? [v13: any] : ? [v14: any] : (isPrime0(v4) = v9 & % 23.18/3.94 doDivides0(v4, v3) = v14 & doDivides0(v4, v2) = v13 & iLess0(v11, v1) = % 23.18/3.94 v12 & sdtpldt0(v10, v4) = v11 & sdtpldt0(v2, v3) = v10 & % 23.18/3.94 aNaturalNumber0(v4) = v8 & aNaturalNumber0(v3) = v7 & % 23.18/3.94 aNaturalNumber0(v2) = v6 & $i(v11) & $i(v10) & ( ~ (v12 = 0) | ~ (v9 = % 23.18/3.94 0) | ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | v14 = 0 | v13 = 0)))) % 23.18/3.94 % 23.18/3.94 (m__1837) % 23.18/3.94 aNaturalNumber0(xp) = 0 & aNaturalNumber0(xm) = 0 & aNaturalNumber0(xn) = 0 & % 23.18/3.94 $i(xp) & $i(xm) & $i(xn) % 23.18/3.94 % 23.18/3.94 (m__1860) % 23.18/3.94 $i(xp) & $i(xm) & $i(xn) & ? [v0: $i] : (isPrime0(xp) = 0 & doDivides0(xp, % 23.18/3.94 v0) = 0 & sdtasdt0(xn, xm) = v0 & $i(v0)) % 23.18/3.94 % 23.18/3.94 (m__1870) % 23.18/3.94 sdtlseqdt0(xp, xn) = 0 & $i(xp) & $i(xn) % 23.18/3.94 % 23.18/3.94 (m__1883) % 23.18/3.95 sdtmndt0(xn, xp) = xr & $i(xr) & $i(xp) & $i(xn) % 23.18/3.95 % 23.18/3.95 (m__1894) % 23.18/3.95 ~ (xr = xn) & sdtlseqdt0(xr, xn) = 0 & $i(xr) & $i(xn) % 23.18/3.95 % 23.18/3.95 (m__1924) % 23.18/3.95 sdtpldt0(xp, xr) = xn & $i(xr) & $i(xp) & $i(xn) % 23.18/3.95 % 23.18/3.95 (m__1951) % 23.18/3.95 $i(xr) & $i(xp) & $i(xm) & $i(xn) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 23.18/3.95 (sdtasdt0(xr, xm) = v2 & sdtasdt0(xp, xm) = v1 & sdtasdt0(xn, xm) = v0 & % 23.18/3.95 sdtpldt0(v1, v2) = v0 & $i(v2) & $i(v1) & $i(v0)) % 23.18/3.95 % 23.18/3.95 (m__1978) % 23.18/3.95 $i(xr) & $i(xp) & $i(xm) & $i(xn) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 23.18/3.95 (sdtmndt0(v1, v2) = v0 & sdtasdt0(xr, xm) = v0 & sdtasdt0(xp, xm) = v2 & % 23.18/3.95 sdtasdt0(xn, xm) = v1 & $i(v2) & $i(v1) & $i(v0)) % 23.18/3.95 % 23.18/3.95 (m__2001) % 23.18/3.95 $i(xp) & $i(xm) & $i(xn) & ? [v0: $i] : ? [v1: $i] : (doDivides0(xp, v1) = 0 % 23.18/3.95 & doDivides0(xp, v0) = 0 & sdtasdt0(xp, xm) = v1 & sdtasdt0(xn, xm) = v0 & % 23.18/3.95 $i(v1) & $i(v0)) % 23.18/3.95 % 23.18/3.95 (function-axioms) % 23.18/3.95 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 23.18/3.95 (sdtsldt0(v3, v2) = v1) | ~ (sdtsldt0(v3, v2) = v0)) & ! [v0: % 23.18/3.95 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 23.18/3.95 : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ (doDivides0(v3, v2) = v0)) & ! % 23.18/3.95 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 23.18/3.95 $i] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) & ! % 23.18/3.95 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 23.18/3.95 (sdtmndt0(v3, v2) = v1) | ~ (sdtmndt0(v3, v2) = v0)) & ! [v0: % 23.18/3.95 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 23.18/3.95 : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ (sdtlseqdt0(v3, v2) = v0)) & ! % 23.18/3.95 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 23.18/3.95 (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 23.18/3.95 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | % 23.18/3.95 ~ (sdtpldt0(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 23.18/3.95 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (isPrime0(v2) = v1) | ~ % 23.18/3.95 (isPrime0(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 23.18/3.95 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) % 23.18/3.95 | ~ (aNaturalNumber0(v2) = v0)) % 23.18/3.95 % 23.18/3.95 Further assumptions not needed in the proof: % 23.18/3.95 -------------------------------------------- % 23.18/3.95 mAMDistr, mAddCanc, mDefDiv, mDefLE, mDefPrime, mDefQuot, mDivAsso, mDivLE, % 23.18/3.95 mDivSum, mIH, mIH_03, mLENTr, mLERefl, mLETotal, mLETran, mMonAdd, mMonMul, % 23.18/3.95 mMonMul2, mMulAsso, mMulCanc, mNatSort, mPrimDiv, mSortsC, mSortsC_01, mZeroAdd, % 23.18/3.95 mZeroMul, m_AddZero, m_MulUnit, m_MulZero % 23.18/3.95 % 23.18/3.95 Those formulas are unsatisfiable: % 23.18/3.95 --------------------------------- % 23.18/3.95 % 23.18/3.95 Begin of proof % 23.18/3.95 | % 23.18/3.95 | ALPHA: (m__1837) implies: % 23.18/3.95 | (1) aNaturalNumber0(xn) = 0 % 23.18/3.95 | (2) aNaturalNumber0(xm) = 0 % 23.18/3.95 | (3) aNaturalNumber0(xp) = 0 % 23.18/3.95 | % 23.18/3.95 | ALPHA: (m__1799) implies: % 23.18/3.96 | (4) ? [v0: $i] : ? [v1: $i] : (sdtpldt0(v0, xp) = v1 & sdtpldt0(xn, xm) = % 23.18/3.96 | v0 & $i(v1) & $i(v0) & ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 23.18/3.96 | [v5: $i] : ( ~ (doDivides0(v4, v5) = 0) | ~ (sdtasdt0(v2, v3) = v5) % 23.18/3.96 | | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ? [v6: any] : ? [v7: any] : % 23.18/3.96 | ? [v8: any] : ? [v9: any] : ? [v10: $i] : ? [v11: $i] : ? % 23.18/3.96 | [v12: any] : ? [v13: any] : ? [v14: any] : (isPrime0(v4) = v9 & % 23.18/3.96 | doDivides0(v4, v3) = v14 & doDivides0(v4, v2) = v13 & iLess0(v11, % 23.18/3.96 | v1) = v12 & sdtpldt0(v10, v4) = v11 & sdtpldt0(v2, v3) = v10 & % 23.18/3.96 | aNaturalNumber0(v4) = v8 & aNaturalNumber0(v3) = v7 & % 23.18/3.96 | aNaturalNumber0(v2) = v6 & $i(v11) & $i(v10) & ( ~ (v12 = 0) | ~ % 23.18/3.96 | (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | v14 = 0 | % 23.18/3.96 | v13 = 0)))) % 23.18/3.96 | % 23.18/3.96 | ALPHA: (m__1860) implies: % 23.18/3.96 | (5) ? [v0: $i] : (isPrime0(xp) = 0 & doDivides0(xp, v0) = 0 & sdtasdt0(xn, % 23.18/3.96 | xm) = v0 & $i(v0)) % 23.18/3.96 | % 23.18/3.96 | ALPHA: (m__1870) implies: % 23.18/3.96 | (6) sdtlseqdt0(xp, xn) = 0 % 23.18/3.96 | % 23.18/3.96 | ALPHA: (m__1883) implies: % 23.18/3.96 | (7) sdtmndt0(xn, xp) = xr % 23.18/3.96 | % 23.18/3.96 | ALPHA: (m__1894) implies: % 23.18/3.96 | (8) ~ (xr = xn) % 23.18/3.96 | (9) sdtlseqdt0(xr, xn) = 0 % 23.18/3.96 | % 23.18/3.96 | ALPHA: (m__1924) implies: % 23.18/3.96 | (10) sdtpldt0(xp, xr) = xn % 23.18/3.96 | % 23.18/3.96 | ALPHA: (m__1951) implies: % 23.18/3.96 | (11) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (sdtasdt0(xr, xm) = v2 & % 23.18/3.96 | sdtasdt0(xp, xm) = v1 & sdtasdt0(xn, xm) = v0 & sdtpldt0(v1, v2) = % 23.18/3.96 | v0 & $i(v2) & $i(v1) & $i(v0)) % 23.18/3.96 | % 23.18/3.96 | ALPHA: (m__1978) implies: % 23.18/3.96 | (12) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (sdtmndt0(v1, v2) = v0 & % 23.18/3.96 | sdtasdt0(xr, xm) = v0 & sdtasdt0(xp, xm) = v2 & sdtasdt0(xn, xm) = % 23.18/3.96 | v1 & $i(v2) & $i(v1) & $i(v0)) % 23.18/3.96 | % 23.18/3.96 | ALPHA: (m__2001) implies: % 23.18/3.96 | (13) $i(xn) % 23.18/3.96 | (14) ? [v0: $i] : ? [v1: $i] : (doDivides0(xp, v1) = 0 & doDivides0(xp, % 23.18/3.96 | v0) = 0 & sdtasdt0(xp, xm) = v1 & sdtasdt0(xn, xm) = v0 & $i(v1) & % 23.18/3.96 | $i(v0)) % 23.18/3.96 | % 23.18/3.96 | ALPHA: (m__) implies: % 23.18/3.96 | (15) $i(xm) % 23.18/3.96 | (16) $i(xp) % 23.18/3.96 | (17) $i(xr) % 23.18/3.96 | (18) ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & doDivides0(xp, v0) = v1 & % 23.18/3.96 | sdtasdt0(xr, xm) = v0 & $i(v0)) % 23.18/3.96 | % 23.18/3.96 | ALPHA: (function-axioms) implies: % 23.18/3.96 | (19) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 23.18/3.96 | : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = % 23.18/3.96 | v0)) % 23.18/3.96 | (20) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 23.18/3.96 | (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 23.18/3.96 | (21) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 23.18/3.96 | : ! [v3: $i] : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ % 23.18/3.96 | (sdtlseqdt0(v3, v2) = v0)) % 23.18/3.96 | (22) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 23.18/3.96 | : ! [v3: $i] : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ % 23.18/3.96 | (doDivides0(v3, v2) = v0)) % 23.18/3.96 | % 23.53/3.96 | DELTA: instantiating (18) with fresh symbols all_38_0, all_38_1 gives: % 23.53/3.96 | (23) ~ (all_38_0 = 0) & doDivides0(xp, all_38_1) = all_38_0 & sdtasdt0(xr, % 23.53/3.96 | xm) = all_38_1 & $i(all_38_1) % 23.53/3.96 | % 23.53/3.96 | ALPHA: (23) implies: % 23.53/3.97 | (24) ~ (all_38_0 = 0) % 23.53/3.97 | (25) sdtasdt0(xr, xm) = all_38_1 % 23.53/3.97 | (26) doDivides0(xp, all_38_1) = all_38_0 % 23.53/3.97 | % 23.53/3.97 | DELTA: instantiating (5) with fresh symbol all_40_0 gives: % 23.53/3.97 | (27) isPrime0(xp) = 0 & doDivides0(xp, all_40_0) = 0 & sdtasdt0(xn, xm) = % 23.53/3.97 | all_40_0 & $i(all_40_0) % 23.53/3.97 | % 23.53/3.97 | ALPHA: (27) implies: % 23.53/3.97 | (28) sdtasdt0(xn, xm) = all_40_0 % 23.53/3.97 | % 23.53/3.97 | DELTA: instantiating (14) with fresh symbols all_42_0, all_42_1 gives: % 23.53/3.97 | (29) doDivides0(xp, all_42_0) = 0 & doDivides0(xp, all_42_1) = 0 & % 23.53/3.97 | sdtasdt0(xp, xm) = all_42_0 & sdtasdt0(xn, xm) = all_42_1 & % 23.53/3.97 | $i(all_42_0) & $i(all_42_1) % 23.53/3.97 | % 23.53/3.97 | ALPHA: (29) implies: % 23.53/3.97 | (30) $i(all_42_1) % 23.53/3.97 | (31) sdtasdt0(xn, xm) = all_42_1 % 23.53/3.97 | (32) sdtasdt0(xp, xm) = all_42_0 % 23.53/3.97 | (33) doDivides0(xp, all_42_1) = 0 % 23.53/3.97 | (34) doDivides0(xp, all_42_0) = 0 % 23.53/3.97 | % 23.53/3.97 | DELTA: instantiating (11) with fresh symbols all_44_0, all_44_1, all_44_2 % 23.53/3.97 | gives: % 23.53/3.97 | (35) sdtasdt0(xr, xm) = all_44_0 & sdtasdt0(xp, xm) = all_44_1 & % 23.53/3.97 | sdtasdt0(xn, xm) = all_44_2 & sdtpldt0(all_44_1, all_44_0) = all_44_2 % 23.53/3.97 | & $i(all_44_0) & $i(all_44_1) & $i(all_44_2) % 23.53/3.97 | % 23.53/3.97 | ALPHA: (35) implies: % 23.55/3.97 | (36) $i(all_44_1) % 23.55/3.97 | (37) $i(all_44_0) % 23.55/3.97 | (38) sdtpldt0(all_44_1, all_44_0) = all_44_2 % 23.55/3.97 | (39) sdtasdt0(xn, xm) = all_44_2 % 23.55/3.97 | (40) sdtasdt0(xp, xm) = all_44_1 % 23.55/3.97 | (41) sdtasdt0(xr, xm) = all_44_0 % 23.55/3.97 | % 23.55/3.97 | DELTA: instantiating (12) with fresh symbols all_46_0, all_46_1, all_46_2 % 23.55/3.97 | gives: % 23.55/3.97 | (42) sdtmndt0(all_46_1, all_46_0) = all_46_2 & sdtasdt0(xr, xm) = all_46_2 % 23.55/3.97 | & sdtasdt0(xp, xm) = all_46_0 & sdtasdt0(xn, xm) = all_46_1 & % 23.55/3.97 | $i(all_46_0) & $i(all_46_1) & $i(all_46_2) % 23.55/3.97 | % 23.55/3.97 | ALPHA: (42) implies: % 23.55/3.97 | (43) sdtasdt0(xn, xm) = all_46_1 % 23.55/3.97 | (44) sdtasdt0(xp, xm) = all_46_0 % 23.55/3.97 | (45) sdtasdt0(xr, xm) = all_46_2 % 23.55/3.97 | % 23.55/3.97 | DELTA: instantiating (4) with fresh symbols all_48_0, all_48_1 gives: % 23.55/3.97 | (46) sdtpldt0(all_48_1, xp) = all_48_0 & sdtpldt0(xn, xm) = all_48_1 & % 23.55/3.97 | $i(all_48_0) & $i(all_48_1) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 23.55/3.97 | : ! [v3: $i] : ( ~ (doDivides0(v2, v3) = 0) | ~ (sdtasdt0(v0, v1) = % 23.55/3.97 | v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: % 23.55/3.97 | any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? [v9: $i] : % 23.55/3.97 | ? [v10: any] : ? [v11: any] : ? [v12: any] : (isPrime0(v2) = v7 & % 23.55/3.97 | doDivides0(v2, v1) = v12 & doDivides0(v2, v0) = v11 & iLess0(v9, % 23.55/3.97 | all_48_0) = v10 & sdtpldt0(v8, v2) = v9 & sdtpldt0(v0, v1) = v8 % 23.55/3.97 | & aNaturalNumber0(v2) = v6 & aNaturalNumber0(v1) = v5 & % 23.55/3.97 | aNaturalNumber0(v0) = v4 & $i(v9) & $i(v8) & ( ~ (v10 = 0) | ~ % 23.55/3.97 | (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | v12 = 0 | % 23.55/3.97 | v11 = 0))) % 23.55/3.97 | % 23.55/3.97 | ALPHA: (46) implies: % 23.55/3.97 | (47) $i(all_48_1) % 23.55/3.97 | (48) sdtpldt0(xn, xm) = all_48_1 % 23.55/3.97 | (49) sdtpldt0(all_48_1, xp) = all_48_0 % 23.55/3.97 | (50) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 23.55/3.97 | (doDivides0(v2, v3) = 0) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | % 23.55/3.97 | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: any] : % 23.55/3.97 | ? [v7: any] : ? [v8: $i] : ? [v9: $i] : ? [v10: any] : ? [v11: % 23.55/3.97 | any] : ? [v12: any] : (isPrime0(v2) = v7 & doDivides0(v2, v1) = % 23.55/3.97 | v12 & doDivides0(v2, v0) = v11 & iLess0(v9, all_48_0) = v10 & % 23.55/3.97 | sdtpldt0(v8, v2) = v9 & sdtpldt0(v0, v1) = v8 & % 23.55/3.97 | aNaturalNumber0(v2) = v6 & aNaturalNumber0(v1) = v5 & % 23.55/3.97 | aNaturalNumber0(v0) = v4 & $i(v9) & $i(v8) & ( ~ (v10 = 0) | ~ % 23.55/3.97 | (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | v12 = 0 | % 23.55/3.97 | v11 = 0))) % 23.55/3.97 | % 23.55/3.98 | GROUND_INST: instantiating (20) with all_42_1, all_44_2, xm, xn, simplifying % 23.55/3.98 | with (31), (39) gives: % 23.55/3.98 | (51) all_44_2 = all_42_1 % 23.55/3.98 | % 23.55/3.98 | GROUND_INST: instantiating (20) with all_44_2, all_46_1, xm, xn, simplifying % 23.55/3.98 | with (39), (43) gives: % 23.55/3.98 | (52) all_46_1 = all_44_2 % 23.55/3.98 | % 23.55/3.98 | GROUND_INST: instantiating (20) with all_40_0, all_46_1, xm, xn, simplifying % 23.55/3.98 | with (28), (43) gives: % 23.55/3.98 | (53) all_46_1 = all_40_0 % 23.55/3.98 | % 23.55/3.98 | GROUND_INST: instantiating (20) with all_44_1, all_46_0, xm, xp, simplifying % 23.55/3.98 | with (40), (44) gives: % 23.55/3.98 | (54) all_46_0 = all_44_1 % 23.55/3.98 | % 23.55/3.98 | GROUND_INST: instantiating (20) with all_42_0, all_46_0, xm, xp, simplifying % 23.55/3.98 | with (32), (44) gives: % 23.55/3.98 | (55) all_46_0 = all_42_0 % 23.55/3.98 | % 23.55/3.98 | GROUND_INST: instantiating (20) with all_44_0, all_46_2, xm, xr, simplifying % 23.55/3.98 | with (41), (45) gives: % 23.55/3.98 | (56) all_46_2 = all_44_0 % 23.55/3.98 | % 23.55/3.98 | GROUND_INST: instantiating (20) with all_38_1, all_46_2, xm, xr, simplifying % 23.55/3.98 | with (25), (45) gives: % 23.55/3.98 | (57) all_46_2 = all_38_1 % 23.55/3.98 | % 23.55/3.98 | COMBINE_EQS: (54), (55) imply: % 23.55/3.98 | (58) all_44_1 = all_42_0 % 23.55/3.98 | % 23.55/3.98 | SIMP: (58) implies: % 23.55/3.98 | (59) all_44_1 = all_42_0 % 23.55/3.98 | % 23.55/3.98 | COMBINE_EQS: (52), (53) imply: % 23.55/3.98 | (60) all_44_2 = all_40_0 % 23.55/3.98 | % 23.55/3.98 | SIMP: (60) implies: % 23.55/3.98 | (61) all_44_2 = all_40_0 % 23.55/3.98 | % 23.55/3.98 | COMBINE_EQS: (56), (57) imply: % 23.55/3.98 | (62) all_44_0 = all_38_1 % 23.55/3.98 | % 23.55/3.98 | COMBINE_EQS: (51), (61) imply: % 23.55/3.98 | (63) all_42_1 = all_40_0 % 23.55/3.98 | % 23.55/3.98 | SIMP: (63) implies: % 23.55/3.98 | (64) all_42_1 = all_40_0 % 23.55/3.98 | % 23.55/3.98 | REDUCE: (33), (64) imply: % 23.55/3.98 | (65) doDivides0(xp, all_40_0) = 0 % 23.55/3.98 | % 23.55/3.98 | REDUCE: (38), (59), (61), (62) imply: % 23.55/3.98 | (66) sdtpldt0(all_42_0, all_38_1) = all_40_0 % 23.55/3.98 | % 23.55/3.98 | REDUCE: (37), (62) imply: % 23.55/3.98 | (67) $i(all_38_1) % 23.55/3.98 | % 23.55/3.98 | REDUCE: (36), (59) imply: % 23.55/3.98 | (68) $i(all_42_0) % 23.55/3.98 | % 23.55/3.98 | REDUCE: (30), (64) imply: % 23.55/3.98 | (69) $i(all_40_0) % 23.55/3.98 | % 23.55/3.98 | GROUND_INST: instantiating (mAddComm) with xn, xm, all_48_1, simplifying with % 23.55/3.98 | (13), (15), (48) gives: % 23.55/3.98 | (70) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xm, xn) = v2 & % 23.55/3.98 | aNaturalNumber0(xm) = v1 & aNaturalNumber0(xn) = v0 & $i(v2) & ( ~ % 23.55/3.98 | (v1 = 0) | ~ (v0 = 0) | v2 = all_48_1)) % 23.55/3.98 | % 23.55/3.98 | GROUND_INST: instantiating (mSortsB) with xn, xm, all_48_1, simplifying with % 23.55/3.98 | (13), (15), (48) gives: % 23.55/3.98 | (71) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 23.55/3.98 | (aNaturalNumber0(all_48_1) = v2 & aNaturalNumber0(xm) = v1 & % 23.55/3.98 | aNaturalNumber0(xn) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 23.55/3.98 | % 23.55/3.98 | GROUND_INST: instantiating (mAddAsso) with xp, xr, xm, xn, all_48_1, % 23.55/3.98 | simplifying with (10), (15), (16), (17), (48) gives: % 23.55/3.99 | (72) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: $i] % 23.55/3.99 | : (sdtpldt0(xr, xm) = v3 & sdtpldt0(xp, v3) = v4 & aNaturalNumber0(xr) % 23.55/3.99 | = v1 & aNaturalNumber0(xp) = v0 & aNaturalNumber0(xm) = v2 & $i(v4) % 23.55/3.99 | & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = % 23.55/3.99 | all_48_1)) % 23.55/3.99 | % 23.55/3.99 | GROUND_INST: instantiating (mAddComm) with xp, xr, xn, simplifying with (10), % 23.55/3.99 | (16), (17) gives: % 23.55/3.99 | (73) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xr, xp) = v2 & % 23.55/3.99 | aNaturalNumber0(xr) = v1 & aNaturalNumber0(xp) = v0 & $i(v2) & ( ~ % 23.55/3.99 | (v1 = 0) | ~ (v0 = 0) | v2 = xn)) % 23.55/3.99 | % 23.55/3.99 | GROUND_INST: instantiating (mSortsB) with xp, xr, xn, simplifying with (10), % 23.55/3.99 | (16), (17) gives: % 23.55/3.99 | (74) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aNaturalNumber0(xr) = v1 % 23.55/3.99 | & aNaturalNumber0(xp) = v0 & aNaturalNumber0(xn) = v2 & ( ~ (v1 = 0) % 23.55/3.99 | | ~ (v0 = 0) | v2 = 0)) % 23.55/3.99 | % 23.55/3.99 | GROUND_INST: instantiating (mAddComm) with all_42_0, all_38_1, all_40_0, % 23.55/3.99 | simplifying with (66), (67), (68) gives: % 23.55/3.99 | (75) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(all_38_1, % 23.55/3.99 | all_42_0) = v2 & aNaturalNumber0(all_42_0) = v0 & % 23.55/3.99 | aNaturalNumber0(all_38_1) = v1 & $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) % 23.55/3.99 | | v2 = all_40_0)) % 23.55/3.99 | % 23.55/3.99 | GROUND_INST: instantiating (mSortsB) with all_42_0, all_38_1, all_40_0, % 23.55/3.99 | simplifying with (66), (67), (68) gives: % 23.55/3.99 | (76) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 23.55/3.99 | (aNaturalNumber0(all_42_0) = v0 & aNaturalNumber0(all_40_0) = v2 & % 23.55/3.99 | aNaturalNumber0(all_38_1) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = % 23.55/3.99 | 0)) % 23.55/3.99 | % 23.55/3.99 | GROUND_INST: instantiating (mAddAsso) with xn, xm, xp, all_48_1, all_48_0, % 23.55/3.99 | simplifying with (13), (15), (16), (48), (49) gives: % 23.55/3.99 | (77) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: $i] % 23.55/3.99 | : (sdtpldt0(xm, xp) = v3 & sdtpldt0(xn, v3) = v4 & aNaturalNumber0(xp) % 23.55/3.99 | = v2 & aNaturalNumber0(xm) = v1 & aNaturalNumber0(xn) = v0 & $i(v4) % 23.55/3.99 | & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = % 23.55/3.99 | all_48_0)) % 23.55/3.99 | % 23.55/3.99 | GROUND_INST: instantiating (mAddComm) with all_48_1, xp, all_48_0, simplifying % 23.55/3.99 | with (16), (47), (49) gives: % 23.55/3.99 | (78) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xp, all_48_1) = % 23.55/3.99 | v2 & aNaturalNumber0(all_48_1) = v0 & aNaturalNumber0(xp) = v1 & % 23.55/3.99 | $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = all_48_0)) % 23.55/3.99 | % 23.55/3.99 | GROUND_INST: instantiating (mSortsB) with all_48_1, xp, all_48_0, simplifying % 23.55/3.99 | with (16), (47), (49) gives: % 23.55/3.99 | (79) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 23.55/3.99 | (aNaturalNumber0(all_48_0) = v2 & aNaturalNumber0(all_48_1) = v0 & % 23.55/3.99 | aNaturalNumber0(xp) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 23.55/3.99 | % 23.55/3.99 | GROUND_INST: instantiating (mMulComm) with xn, xm, all_40_0, simplifying with % 23.55/3.99 | (13), (15), (28) gives: % 23.55/3.99 | (80) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(xm, xn) = v2 & % 23.55/3.99 | aNaturalNumber0(xm) = v1 & aNaturalNumber0(xn) = v0 & $i(v2) & ( ~ % 23.55/3.99 | (v1 = 0) | ~ (v0 = 0) | v2 = all_40_0)) % 23.55/3.99 | % 23.55/3.99 | GROUND_INST: instantiating (mSortsB_02) with xn, xm, all_40_0, simplifying % 23.55/3.99 | with (13), (15), (28) gives: % 23.55/3.99 | (81) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 23.55/3.99 | (aNaturalNumber0(all_40_0) = v2 & aNaturalNumber0(xm) = v1 & % 23.55/3.99 | aNaturalNumber0(xn) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 23.55/3.99 | % 23.55/3.99 | GROUND_INST: instantiating (mMulComm) with xp, xm, all_42_0, simplifying with % 23.55/3.99 | (15), (16), (32) gives: % 23.55/3.99 | (82) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(xm, xp) = v2 & % 23.55/3.99 | aNaturalNumber0(xp) = v0 & aNaturalNumber0(xm) = v1 & $i(v2) & ( ~ % 23.55/3.99 | (v1 = 0) | ~ (v0 = 0) | v2 = all_42_0)) % 23.55/3.99 | % 23.55/3.99 | GROUND_INST: instantiating (mSortsB_02) with xp, xm, all_42_0, simplifying % 23.55/3.99 | with (15), (16), (32) gives: % 23.55/3.99 | (83) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 23.55/3.99 | (aNaturalNumber0(all_42_0) = v2 & aNaturalNumber0(xp) = v0 & % 23.55/4.00 | aNaturalNumber0(xm) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 23.55/4.00 | % 23.55/4.00 | GROUND_INST: instantiating (mMulComm) with xr, xm, all_38_1, simplifying with % 23.55/4.00 | (15), (17), (25) gives: % 23.55/4.00 | (84) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(xm, xr) = v2 & % 23.55/4.00 | aNaturalNumber0(xr) = v0 & aNaturalNumber0(xm) = v1 & $i(v2) & ( ~ % 23.55/4.00 | (v1 = 0) | ~ (v0 = 0) | v2 = all_38_1)) % 23.55/4.00 | % 23.55/4.00 | GROUND_INST: instantiating (mSortsB_02) with xr, xm, all_38_1, simplifying % 23.55/4.00 | with (15), (17), (25) gives: % 23.55/4.00 | (85) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 23.55/4.00 | (aNaturalNumber0(all_38_1) = v2 & aNaturalNumber0(xr) = v0 & % 23.55/4.00 | aNaturalNumber0(xm) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 23.55/4.00 | % 23.55/4.00 | GROUND_INST: instantiating (mLEAsym) with xr, xn, simplifying with (9), (13), % 23.55/4.00 | (17) gives: % 23.55/4.00 | (86) xr = xn | ? [v0: any] : ? [v1: any] : ? [v2: any] : (sdtlseqdt0(xn, % 23.55/4.00 | xr) = v2 & aNaturalNumber0(xr) = v0 & aNaturalNumber0(xn) = v1 & ( % 23.55/4.00 | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 23.55/4.00 | % 23.55/4.00 | GROUND_INST: instantiating (mDefDiff) with xp, xn, xr, simplifying with (7), % 23.55/4.00 | (13), (16) gives: % 23.55/4.00 | (87) ? [v0: any] : ? [v1: any] : ? [v2: any] : (sdtlseqdt0(xp, xn) = v2 % 23.55/4.00 | & aNaturalNumber0(xp) = v0 & aNaturalNumber0(xn) = v1 & ( ~ (v2 = 0) % 23.55/4.00 | | ~ (v1 = 0) | ~ (v0 = 0))) | ( ! [v0: $i] : (v0 = xr | ~ % 23.55/4.00 | (sdtpldt0(xp, v0) = xn) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) % 23.55/4.00 | & aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( ~ (sdtpldt0(xp, % 23.55/4.00 | xr) = v0) | ~ $i(xr) | (v0 = xn & aNaturalNumber0(xr) = 0))) % 23.55/4.00 | % 23.55/4.00 | GROUND_INST: instantiating (mDivTrans) with xp, all_40_0, all_38_1, all_38_0, % 23.55/4.00 | simplifying with (16), (26), (65), (67), (69) gives: % 23.55/4.00 | (88) all_38_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: % 23.55/4.00 | any] : (doDivides0(all_40_0, all_38_1) = v3 & % 23.55/4.00 | aNaturalNumber0(all_40_0) = v1 & aNaturalNumber0(all_38_1) = v2 & % 23.55/4.00 | aNaturalNumber0(xp) = v0 & ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) % 23.55/4.00 | | ~ (v0 = 0))) % 23.55/4.00 | % 23.55/4.00 | GROUND_INST: instantiating (50) with xn, xm, xp, all_40_0, simplifying with % 23.55/4.00 | (13), (15), (16), (28), (65) gives: % 23.71/4.00 | (89) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? [v4: % 23.71/4.00 | $i] : ? [v5: $i] : ? [v6: any] : ? [v7: any] : ? [v8: any] : % 23.71/4.00 | (isPrime0(xp) = v3 & doDivides0(xp, xm) = v8 & doDivides0(xp, xn) = v7 % 23.71/4.00 | & iLess0(v5, all_48_0) = v6 & sdtpldt0(v4, xp) = v5 & sdtpldt0(xn, % 23.71/4.00 | xm) = v4 & aNaturalNumber0(xp) = v2 & aNaturalNumber0(xm) = v1 & % 23.71/4.00 | aNaturalNumber0(xn) = v0 & $i(v5) & $i(v4) & ( ~ (v6 = 0) | ~ (v3 = % 23.71/4.00 | 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v8 = 0 | v7 = 0)) % 23.71/4.00 | % 23.71/4.00 | GROUND_INST: instantiating (mDivMin) with xp, all_42_0, all_38_1, all_40_0, % 23.71/4.00 | simplifying with (16), (65), (66), (67), (68) gives: % 23.71/4.00 | (90) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? [v4: % 23.71/4.00 | any] : (doDivides0(xp, all_42_0) = v3 & doDivides0(xp, all_38_1) = % 23.71/4.00 | v4 & aNaturalNumber0(all_42_0) = v1 & aNaturalNumber0(all_38_1) = v2 % 23.71/4.00 | & aNaturalNumber0(xp) = v0 & ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = % 23.71/4.00 | 0) | ~ (v0 = 0) | v4 = 0)) % 23.71/4.00 | % 23.71/4.00 | GROUND_INST: instantiating (mDivTrans) with xp, all_42_0, all_38_1, all_38_0, % 23.71/4.00 | simplifying with (16), (26), (34), (67), (68) gives: % 23.71/4.00 | (91) all_38_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: % 23.71/4.00 | any] : (doDivides0(all_42_0, all_38_1) = v3 & % 23.71/4.00 | aNaturalNumber0(all_42_0) = v1 & aNaturalNumber0(all_38_1) = v2 & % 23.71/4.00 | aNaturalNumber0(xp) = v0 & ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) % 23.71/4.00 | | ~ (v0 = 0))) % 23.71/4.00 | % 23.71/4.00 | GROUND_INST: instantiating (50) with xp, xm, xp, all_42_0, simplifying with % 23.71/4.00 | (15), (16), (32), (34) gives: % 23.71/4.00 | (92) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? [v4: % 23.71/4.00 | $i] : ? [v5: $i] : ? [v6: any] : ? [v7: any] : ? [v8: any] : % 23.71/4.00 | (isPrime0(xp) = v3 & doDivides0(xp, xp) = v7 & doDivides0(xp, xm) = v8 % 23.71/4.00 | & iLess0(v5, all_48_0) = v6 & sdtpldt0(v4, xp) = v5 & sdtpldt0(xp, % 23.71/4.00 | xm) = v4 & aNaturalNumber0(xp) = v2 & aNaturalNumber0(xp) = v0 & % 23.71/4.00 | aNaturalNumber0(xm) = v1 & $i(v5) & $i(v4) & ( ~ (v6 = 0) | ~ (v3 = % 23.71/4.00 | 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v8 = 0 | v7 = 0)) % 23.71/4.00 | % 23.71/4.00 | DELTA: instantiating (85) with fresh symbols all_60_0, all_60_1, all_60_2 % 23.71/4.00 | gives: % 23.71/4.00 | (93) aNaturalNumber0(all_38_1) = all_60_0 & aNaturalNumber0(xr) = all_60_2 % 23.71/4.00 | & aNaturalNumber0(xm) = all_60_1 & ( ~ (all_60_1 = 0) | ~ (all_60_2 = % 23.71/4.00 | 0) | all_60_0 = 0) % 23.71/4.00 | % 23.71/4.00 | ALPHA: (93) implies: % 23.71/4.00 | (94) aNaturalNumber0(xm) = all_60_1 % 23.71/4.00 | (95) aNaturalNumber0(xr) = all_60_2 % 23.71/4.00 | (96) aNaturalNumber0(all_38_1) = all_60_0 % 23.71/4.00 | (97) ~ (all_60_1 = 0) | ~ (all_60_2 = 0) | all_60_0 = 0 % 23.71/4.00 | % 23.71/4.00 | DELTA: instantiating (83) with fresh symbols all_62_0, all_62_1, all_62_2 % 23.71/4.00 | gives: % 23.71/4.00 | (98) aNaturalNumber0(all_42_0) = all_62_0 & aNaturalNumber0(xp) = all_62_2 % 23.71/4.00 | & aNaturalNumber0(xm) = all_62_1 & ( ~ (all_62_1 = 0) | ~ (all_62_2 = % 23.71/4.00 | 0) | all_62_0 = 0) % 23.71/4.00 | % 23.71/4.00 | ALPHA: (98) implies: % 23.71/4.01 | (99) aNaturalNumber0(xm) = all_62_1 % 23.71/4.01 | (100) aNaturalNumber0(xp) = all_62_2 % 23.71/4.01 | (101) aNaturalNumber0(all_42_0) = all_62_0 % 23.71/4.01 | (102) ~ (all_62_1 = 0) | ~ (all_62_2 = 0) | all_62_0 = 0 % 23.71/4.01 | % 23.71/4.01 | DELTA: instantiating (81) with fresh symbols all_64_0, all_64_1, all_64_2 % 23.71/4.01 | gives: % 23.71/4.01 | (103) aNaturalNumber0(all_40_0) = all_64_0 & aNaturalNumber0(xm) = all_64_1 % 23.71/4.01 | & aNaturalNumber0(xn) = all_64_2 & ( ~ (all_64_1 = 0) | ~ (all_64_2 % 23.71/4.01 | = 0) | all_64_0 = 0) % 23.71/4.01 | % 23.71/4.01 | ALPHA: (103) implies: % 23.71/4.01 | (104) aNaturalNumber0(xn) = all_64_2 % 23.71/4.01 | (105) aNaturalNumber0(xm) = all_64_1 % 23.71/4.01 | (106) ~ (all_64_1 = 0) | ~ (all_64_2 = 0) | all_64_0 = 0 % 23.71/4.01 | % 23.71/4.01 | DELTA: instantiating (79) with fresh symbols all_66_0, all_66_1, all_66_2 % 23.71/4.01 | gives: % 23.71/4.01 | (107) aNaturalNumber0(all_48_0) = all_66_0 & aNaturalNumber0(all_48_1) = % 23.71/4.01 | all_66_2 & aNaturalNumber0(xp) = all_66_1 & ( ~ (all_66_1 = 0) | ~ % 23.71/4.01 | (all_66_2 = 0) | all_66_0 = 0) % 23.71/4.01 | % 23.71/4.01 | ALPHA: (107) implies: % 23.71/4.01 | (108) aNaturalNumber0(xp) = all_66_1 % 23.71/4.01 | % 23.71/4.01 | DELTA: instantiating (76) with fresh symbols all_68_0, all_68_1, all_68_2 % 23.71/4.01 | gives: % 23.71/4.01 | (109) aNaturalNumber0(all_42_0) = all_68_2 & aNaturalNumber0(all_40_0) = % 23.71/4.01 | all_68_0 & aNaturalNumber0(all_38_1) = all_68_1 & ( ~ (all_68_1 = 0) % 23.71/4.01 | | ~ (all_68_2 = 0) | all_68_0 = 0) % 23.71/4.01 | % 23.71/4.01 | ALPHA: (109) implies: % 23.71/4.01 | (110) aNaturalNumber0(all_38_1) = all_68_1 % 23.71/4.01 | % 23.71/4.01 | DELTA: instantiating (74) with fresh symbols all_70_0, all_70_1, all_70_2 % 23.71/4.01 | gives: % 23.71/4.01 | (111) aNaturalNumber0(xr) = all_70_1 & aNaturalNumber0(xp) = all_70_2 & % 23.71/4.01 | aNaturalNumber0(xn) = all_70_0 & ( ~ (all_70_1 = 0) | ~ (all_70_2 = % 23.71/4.01 | 0) | all_70_0 = 0) % 23.71/4.01 | % 23.71/4.01 | ALPHA: (111) implies: % 23.71/4.01 | (112) aNaturalNumber0(xn) = all_70_0 % 23.71/4.01 | (113) aNaturalNumber0(xp) = all_70_2 % 23.71/4.01 | (114) aNaturalNumber0(xr) = all_70_1 % 23.71/4.01 | % 23.71/4.01 | DELTA: instantiating (71) with fresh symbols all_72_0, all_72_1, all_72_2 % 23.71/4.01 | gives: % 23.71/4.01 | (115) aNaturalNumber0(all_48_1) = all_72_0 & aNaturalNumber0(xm) = all_72_1 % 23.71/4.01 | & aNaturalNumber0(xn) = all_72_2 & ( ~ (all_72_1 = 0) | ~ (all_72_2 % 23.71/4.01 | = 0) | all_72_0 = 0) % 23.71/4.01 | % 23.71/4.01 | ALPHA: (115) implies: % 23.71/4.01 | (116) aNaturalNumber0(xn) = all_72_2 % 23.71/4.01 | (117) aNaturalNumber0(xm) = all_72_1 % 23.71/4.01 | % 23.71/4.01 | DELTA: instantiating (78) with fresh symbols all_74_0, all_74_1, all_74_2 % 23.71/4.01 | gives: % 23.71/4.01 | (118) sdtpldt0(xp, all_48_1) = all_74_0 & aNaturalNumber0(all_48_1) = % 23.71/4.01 | all_74_2 & aNaturalNumber0(xp) = all_74_1 & $i(all_74_0) & ( ~ % 23.71/4.01 | (all_74_1 = 0) | ~ (all_74_2 = 0) | all_74_0 = all_48_0) % 23.71/4.01 | % 23.71/4.01 | ALPHA: (118) implies: % 23.71/4.01 | (119) aNaturalNumber0(xp) = all_74_1 % 23.71/4.01 | % 23.71/4.01 | DELTA: instantiating (70) with fresh symbols all_76_0, all_76_1, all_76_2 % 23.71/4.01 | gives: % 23.71/4.01 | (120) sdtpldt0(xm, xn) = all_76_0 & aNaturalNumber0(xm) = all_76_1 & % 23.71/4.01 | aNaturalNumber0(xn) = all_76_2 & $i(all_76_0) & ( ~ (all_76_1 = 0) | % 23.71/4.01 | ~ (all_76_2 = 0) | all_76_0 = all_48_1) % 23.71/4.01 | % 23.71/4.01 | ALPHA: (120) implies: % 23.71/4.01 | (121) aNaturalNumber0(xn) = all_76_2 % 23.71/4.01 | (122) aNaturalNumber0(xm) = all_76_1 % 23.71/4.01 | % 23.71/4.01 | DELTA: instantiating (75) with fresh symbols all_78_0, all_78_1, all_78_2 % 23.71/4.01 | gives: % 23.71/4.01 | (123) sdtpldt0(all_38_1, all_42_0) = all_78_0 & aNaturalNumber0(all_42_0) = % 23.71/4.01 | all_78_2 & aNaturalNumber0(all_38_1) = all_78_1 & $i(all_78_0) & ( ~ % 23.71/4.01 | (all_78_1 = 0) | ~ (all_78_2 = 0) | all_78_0 = all_40_0) % 23.71/4.01 | % 23.71/4.01 | ALPHA: (123) implies: % 23.71/4.01 | (124) aNaturalNumber0(all_38_1) = all_78_1 % 23.71/4.01 | (125) aNaturalNumber0(all_42_0) = all_78_2 % 23.71/4.01 | % 23.71/4.01 | DELTA: instantiating (84) with fresh symbols all_80_0, all_80_1, all_80_2 % 23.71/4.01 | gives: % 23.71/4.01 | (126) sdtasdt0(xm, xr) = all_80_0 & aNaturalNumber0(xr) = all_80_2 & % 23.71/4.01 | aNaturalNumber0(xm) = all_80_1 & $i(all_80_0) & ( ~ (all_80_1 = 0) | % 23.71/4.01 | ~ (all_80_2 = 0) | all_80_0 = all_38_1) % 23.71/4.01 | % 23.71/4.01 | ALPHA: (126) implies: % 23.71/4.01 | (127) aNaturalNumber0(xm) = all_80_1 % 23.71/4.01 | (128) aNaturalNumber0(xr) = all_80_2 % 23.71/4.01 | % 23.71/4.01 | DELTA: instantiating (80) with fresh symbols all_82_0, all_82_1, all_82_2 % 23.71/4.01 | gives: % 23.71/4.01 | (129) sdtasdt0(xm, xn) = all_82_0 & aNaturalNumber0(xm) = all_82_1 & % 23.71/4.01 | aNaturalNumber0(xn) = all_82_2 & $i(all_82_0) & ( ~ (all_82_1 = 0) | % 23.71/4.01 | ~ (all_82_2 = 0) | all_82_0 = all_40_0) % 23.71/4.01 | % 23.71/4.01 | ALPHA: (129) implies: % 23.71/4.01 | (130) aNaturalNumber0(xn) = all_82_2 % 23.71/4.01 | (131) aNaturalNumber0(xm) = all_82_1 % 23.71/4.01 | % 23.71/4.01 | DELTA: instantiating (82) with fresh symbols all_84_0, all_84_1, all_84_2 % 23.71/4.01 | gives: % 23.71/4.01 | (132) sdtasdt0(xm, xp) = all_84_0 & aNaturalNumber0(xp) = all_84_2 & % 23.71/4.01 | aNaturalNumber0(xm) = all_84_1 & $i(all_84_0) & ( ~ (all_84_1 = 0) | % 23.71/4.01 | ~ (all_84_2 = 0) | all_84_0 = all_42_0) % 23.71/4.01 | % 23.71/4.01 | ALPHA: (132) implies: % 23.71/4.01 | (133) aNaturalNumber0(xm) = all_84_1 % 23.71/4.01 | (134) aNaturalNumber0(xp) = all_84_2 % 23.71/4.01 | % 23.71/4.01 | DELTA: instantiating (73) with fresh symbols all_86_0, all_86_1, all_86_2 % 23.71/4.01 | gives: % 23.71/4.01 | (135) sdtpldt0(xr, xp) = all_86_0 & aNaturalNumber0(xr) = all_86_1 & % 23.71/4.01 | aNaturalNumber0(xp) = all_86_2 & $i(all_86_0) & ( ~ (all_86_1 = 0) | % 23.71/4.01 | ~ (all_86_2 = 0) | all_86_0 = xn) % 23.71/4.01 | % 23.71/4.01 | ALPHA: (135) implies: % 23.71/4.01 | (136) aNaturalNumber0(xp) = all_86_2 % 23.71/4.01 | (137) aNaturalNumber0(xr) = all_86_1 % 23.71/4.01 | % 23.71/4.01 | DELTA: instantiating (90) with fresh symbols all_88_0, all_88_1, all_88_2, % 23.71/4.01 | all_88_3, all_88_4 gives: % 23.71/4.01 | (138) doDivides0(xp, all_42_0) = all_88_1 & doDivides0(xp, all_38_1) = % 23.71/4.01 | all_88_0 & aNaturalNumber0(all_42_0) = all_88_3 & % 23.71/4.01 | aNaturalNumber0(all_38_1) = all_88_2 & aNaturalNumber0(xp) = all_88_4 % 23.71/4.01 | & ( ~ (all_88_1 = 0) | ~ (all_88_2 = 0) | ~ (all_88_3 = 0) | ~ % 23.71/4.01 | (all_88_4 = 0) | all_88_0 = 0) % 23.71/4.01 | % 23.71/4.01 | ALPHA: (138) implies: % 23.71/4.01 | (139) aNaturalNumber0(xp) = all_88_4 % 23.71/4.01 | (140) aNaturalNumber0(all_38_1) = all_88_2 % 23.71/4.01 | (141) aNaturalNumber0(all_42_0) = all_88_3 % 23.71/4.01 | (142) doDivides0(xp, all_38_1) = all_88_0 % 23.71/4.01 | (143) doDivides0(xp, all_42_0) = all_88_1 % 23.71/4.01 | (144) ~ (all_88_1 = 0) | ~ (all_88_2 = 0) | ~ (all_88_3 = 0) | ~ % 23.71/4.01 | (all_88_4 = 0) | all_88_0 = 0 % 23.71/4.01 | % 23.71/4.01 | DELTA: instantiating (72) with fresh symbols all_90_0, all_90_1, all_90_2, % 23.71/4.01 | all_90_3, all_90_4 gives: % 23.71/4.01 | (145) sdtpldt0(xr, xm) = all_90_1 & sdtpldt0(xp, all_90_1) = all_90_0 & % 23.71/4.01 | aNaturalNumber0(xr) = all_90_3 & aNaturalNumber0(xp) = all_90_4 & % 23.71/4.01 | aNaturalNumber0(xm) = all_90_2 & $i(all_90_0) & $i(all_90_1) & ( ~ % 23.71/4.01 | (all_90_2 = 0) | ~ (all_90_3 = 0) | ~ (all_90_4 = 0) | all_90_0 = % 23.71/4.01 | all_48_1) % 23.71/4.01 | % 23.71/4.01 | ALPHA: (145) implies: % 23.71/4.01 | (146) aNaturalNumber0(xm) = all_90_2 % 23.71/4.01 | (147) aNaturalNumber0(xp) = all_90_4 % 23.71/4.01 | (148) aNaturalNumber0(xr) = all_90_3 % 23.71/4.01 | % 23.71/4.01 | DELTA: instantiating (77) with fresh symbols all_92_0, all_92_1, all_92_2, % 23.71/4.01 | all_92_3, all_92_4 gives: % 23.71/4.01 | (149) sdtpldt0(xm, xp) = all_92_1 & sdtpldt0(xn, all_92_1) = all_92_0 & % 23.71/4.01 | aNaturalNumber0(xp) = all_92_2 & aNaturalNumber0(xm) = all_92_3 & % 23.71/4.01 | aNaturalNumber0(xn) = all_92_4 & $i(all_92_0) & $i(all_92_1) & ( ~ % 23.71/4.01 | (all_92_2 = 0) | ~ (all_92_3 = 0) | ~ (all_92_4 = 0) | all_92_0 = % 23.71/4.01 | all_48_0) % 23.71/4.01 | % 23.71/4.01 | ALPHA: (149) implies: % 23.71/4.01 | (150) aNaturalNumber0(xn) = all_92_4 % 23.71/4.01 | (151) aNaturalNumber0(xm) = all_92_3 % 23.71/4.01 | (152) aNaturalNumber0(xp) = all_92_2 % 23.71/4.01 | % 23.71/4.01 | DELTA: instantiating (92) with fresh symbols all_94_0, all_94_1, all_94_2, % 23.71/4.01 | all_94_3, all_94_4, all_94_5, all_94_6, all_94_7, all_94_8 gives: % 23.71/4.02 | (153) isPrime0(xp) = all_94_5 & doDivides0(xp, xp) = all_94_1 & % 23.71/4.02 | doDivides0(xp, xm) = all_94_0 & iLess0(all_94_3, all_48_0) = all_94_2 % 23.71/4.02 | & sdtpldt0(all_94_4, xp) = all_94_3 & sdtpldt0(xp, xm) = all_94_4 & % 23.71/4.02 | aNaturalNumber0(xp) = all_94_6 & aNaturalNumber0(xp) = all_94_8 & % 23.71/4.02 | aNaturalNumber0(xm) = all_94_7 & $i(all_94_3) & $i(all_94_4) & ( ~ % 23.71/4.02 | (all_94_2 = 0) | ~ (all_94_5 = 0) | ~ (all_94_6 = 0) | ~ % 23.71/4.02 | (all_94_7 = 0) | ~ (all_94_8 = 0) | all_94_0 = 0 | all_94_1 = 0) % 23.71/4.02 | % 23.71/4.02 | ALPHA: (153) implies: % 23.71/4.02 | (154) aNaturalNumber0(xm) = all_94_7 % 23.71/4.02 | (155) aNaturalNumber0(xp) = all_94_8 % 23.71/4.02 | (156) aNaturalNumber0(xp) = all_94_6 % 23.71/4.02 | % 23.71/4.02 | DELTA: instantiating (89) with fresh symbols all_96_0, all_96_1, all_96_2, % 23.71/4.02 | all_96_3, all_96_4, all_96_5, all_96_6, all_96_7, all_96_8 gives: % 23.71/4.02 | (157) isPrime0(xp) = all_96_5 & doDivides0(xp, xm) = all_96_0 & % 23.71/4.02 | doDivides0(xp, xn) = all_96_1 & iLess0(all_96_3, all_48_0) = all_96_2 % 23.71/4.02 | & sdtpldt0(all_96_4, xp) = all_96_3 & sdtpldt0(xn, xm) = all_96_4 & % 23.71/4.02 | aNaturalNumber0(xp) = all_96_6 & aNaturalNumber0(xm) = all_96_7 & % 23.71/4.02 | aNaturalNumber0(xn) = all_96_8 & $i(all_96_3) & $i(all_96_4) & ( ~ % 23.71/4.02 | (all_96_2 = 0) | ~ (all_96_5 = 0) | ~ (all_96_6 = 0) | ~ % 23.71/4.02 | (all_96_7 = 0) | ~ (all_96_8 = 0) | all_96_0 = 0 | all_96_1 = 0) % 23.71/4.02 | % 23.71/4.02 | ALPHA: (157) implies: % 23.71/4.02 | (158) aNaturalNumber0(xn) = all_96_8 % 23.71/4.02 | (159) aNaturalNumber0(xm) = all_96_7 % 23.71/4.02 | (160) aNaturalNumber0(xp) = all_96_6 % 23.71/4.02 | % 23.71/4.02 | BETA: splitting (88) gives: % 23.71/4.02 | % 23.71/4.02 | Case 1: % 23.71/4.02 | | % 23.71/4.02 | | (161) all_38_0 = 0 % 23.71/4.02 | | % 23.71/4.02 | | REDUCE: (24), (161) imply: % 23.71/4.02 | | (162) $false % 23.71/4.02 | | % 23.71/4.02 | | CLOSE: (162) is inconsistent. % 23.71/4.02 | | % 23.71/4.02 | Case 2: % 23.71/4.02 | | % 23.71/4.02 | | (163) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 23.71/4.02 | | (doDivides0(all_40_0, all_38_1) = v3 & aNaturalNumber0(all_40_0) = % 23.71/4.02 | | v1 & aNaturalNumber0(all_38_1) = v2 & aNaturalNumber0(xp) = v0 & % 23.71/4.02 | | ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 23.71/4.02 | | % 23.71/4.02 | | DELTA: instantiating (163) with fresh symbols all_106_0, all_106_1, % 23.71/4.02 | | all_106_2, all_106_3 gives: % 23.71/4.02 | | (164) doDivides0(all_40_0, all_38_1) = all_106_0 & % 23.71/4.02 | | aNaturalNumber0(all_40_0) = all_106_2 & aNaturalNumber0(all_38_1) = % 23.71/4.02 | | all_106_1 & aNaturalNumber0(xp) = all_106_3 & ( ~ (all_106_0 = 0) | % 23.71/4.02 | | ~ (all_106_1 = 0) | ~ (all_106_2 = 0) | ~ (all_106_3 = 0)) % 23.71/4.02 | | % 23.71/4.02 | | ALPHA: (164) implies: % 23.71/4.02 | | (165) aNaturalNumber0(xp) = all_106_3 % 23.71/4.02 | | (166) aNaturalNumber0(all_38_1) = all_106_1 % 23.71/4.02 | | % 23.71/4.02 | | BETA: splitting (91) gives: % 23.71/4.02 | | % 23.71/4.02 | | Case 1: % 23.71/4.02 | | | % 23.71/4.02 | | | (167) all_38_0 = 0 % 23.71/4.02 | | | % 23.71/4.02 | | | REDUCE: (24), (167) imply: % 23.71/4.02 | | | (168) $false % 23.71/4.02 | | | % 23.71/4.02 | | | CLOSE: (168) is inconsistent. % 23.71/4.02 | | | % 23.71/4.02 | | Case 2: % 23.71/4.02 | | | % 23.71/4.02 | | | (169) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 23.71/4.02 | | | (doDivides0(all_42_0, all_38_1) = v3 & aNaturalNumber0(all_42_0) % 23.71/4.02 | | | = v1 & aNaturalNumber0(all_38_1) = v2 & aNaturalNumber0(xp) = % 23.71/4.02 | | | v0 & ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 23.71/4.02 | | | % 23.71/4.02 | | | DELTA: instantiating (169) with fresh symbols all_111_0, all_111_1, % 23.71/4.02 | | | all_111_2, all_111_3 gives: % 23.71/4.02 | | | (170) doDivides0(all_42_0, all_38_1) = all_111_0 & % 23.71/4.02 | | | aNaturalNumber0(all_42_0) = all_111_2 & aNaturalNumber0(all_38_1) % 23.71/4.02 | | | = all_111_1 & aNaturalNumber0(xp) = all_111_3 & ( ~ (all_111_0 = % 23.71/4.02 | | | 0) | ~ (all_111_1 = 0) | ~ (all_111_2 = 0) | ~ (all_111_3 % 23.71/4.02 | | | = 0)) % 23.71/4.02 | | | % 23.71/4.02 | | | ALPHA: (170) implies: % 23.71/4.02 | | | (171) aNaturalNumber0(xp) = all_111_3 % 23.71/4.02 | | | (172) aNaturalNumber0(all_38_1) = all_111_1 % 23.71/4.02 | | | (173) aNaturalNumber0(all_42_0) = all_111_2 % 23.71/4.02 | | | % 23.71/4.02 | | | BETA: splitting (86) gives: % 23.71/4.02 | | | % 23.71/4.02 | | | Case 1: % 23.71/4.02 | | | | % 23.71/4.02 | | | | (174) xr = xn % 23.71/4.02 | | | | % 23.71/4.02 | | | | REDUCE: (8), (174) imply: % 23.71/4.02 | | | | (175) $false % 23.71/4.02 | | | | % 23.71/4.02 | | | | CLOSE: (175) is inconsistent. % 23.71/4.02 | | | | % 23.71/4.02 | | | Case 2: % 23.71/4.02 | | | | % 23.71/4.02 | | | | (176) ? [v0: any] : ? [v1: any] : ? [v2: any] : (sdtlseqdt0(xn, % 23.71/4.02 | | | | xr) = v2 & aNaturalNumber0(xr) = v0 & aNaturalNumber0(xn) = % 23.71/4.02 | | | | v1 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 23.71/4.02 | | | | % 23.71/4.02 | | | | DELTA: instantiating (176) with fresh symbols all_116_0, all_116_1, % 23.71/4.02 | | | | all_116_2 gives: % 23.71/4.02 | | | | (177) sdtlseqdt0(xn, xr) = all_116_0 & aNaturalNumber0(xr) = % 23.71/4.02 | | | | all_116_2 & aNaturalNumber0(xn) = all_116_1 & ( ~ (all_116_0 = % 23.71/4.02 | | | | 0) | ~ (all_116_1 = 0) | ~ (all_116_2 = 0)) % 23.71/4.02 | | | | % 23.71/4.02 | | | | ALPHA: (177) implies: % 23.71/4.02 | | | | (178) aNaturalNumber0(xn) = all_116_1 % 23.71/4.02 | | | | (179) aNaturalNumber0(xr) = all_116_2 % 23.71/4.02 | | | | % 23.71/4.02 | | | | GROUND_INST: instantiating (19) with 0, all_72_2, xn, simplifying with % 23.71/4.02 | | | | (1), (116) gives: % 23.71/4.02 | | | | (180) all_72_2 = 0 % 23.71/4.02 | | | | % 23.71/4.02 | | | | GROUND_INST: instantiating (19) with all_72_2, all_76_2, xn, simplifying % 23.71/4.02 | | | | with (116), (121) gives: % 23.71/4.02 | | | | (181) all_76_2 = all_72_2 % 23.71/4.02 | | | | % 23.71/4.02 | | | | GROUND_INST: instantiating (19) with all_64_2, all_76_2, xn, simplifying % 23.71/4.02 | | | | with (104), (121) gives: % 23.71/4.02 | | | | (182) all_76_2 = all_64_2 % 23.71/4.02 | | | | % 23.71/4.02 | | | | GROUND_INST: instantiating (19) with all_72_2, all_92_4, xn, simplifying % 23.71/4.02 | | | | with (116), (150) gives: % 23.71/4.02 | | | | (183) all_92_4 = all_72_2 % 23.71/4.02 | | | | % 23.71/4.02 | | | | GROUND_INST: instantiating (19) with all_70_0, all_92_4, xn, simplifying % 23.71/4.02 | | | | with (112), (150) gives: % 23.71/4.02 | | | | (184) all_92_4 = all_70_0 % 23.71/4.02 | | | | % 23.71/4.02 | | | | GROUND_INST: instantiating (19) with all_92_4, all_96_8, xn, simplifying % 23.71/4.02 | | | | with (150), (158) gives: % 23.71/4.02 | | | | (185) all_96_8 = all_92_4 % 23.71/4.02 | | | | % 23.71/4.02 | | | | GROUND_INST: instantiating (19) with all_96_8, all_116_1, xn, % 23.71/4.02 | | | | simplifying with (158), (178) gives: % 23.71/4.02 | | | | (186) all_116_1 = all_96_8 % 23.71/4.02 | | | | % 23.71/4.02 | | | | GROUND_INST: instantiating (19) with all_82_2, all_116_1, xn, % 23.71/4.02 | | | | simplifying with (130), (178) gives: % 23.71/4.02 | | | | (187) all_116_1 = all_82_2 % 23.71/4.02 | | | | % 23.71/4.02 | | | | GROUND_INST: instantiating (19) with all_64_1, all_76_1, xm, simplifying % 23.71/4.02 | | | | with (105), (122) gives: % 23.71/4.02 | | | | (188) all_76_1 = all_64_1 % 23.71/4.02 | | | | % 23.71/4.02 | | | | GROUND_INST: instantiating (19) with 0, all_80_1, xm, simplifying with % 23.71/4.03 | | | | (2), (127) gives: % 23.71/4.03 | | | | (189) all_80_1 = 0 % 23.71/4.03 | | | | % 23.71/4.03 | | | | GROUND_INST: instantiating (19) with all_64_1, all_80_1, xm, simplifying % 23.71/4.03 | | | | with (105), (127) gives: % 23.71/4.03 | | | | (190) all_80_1 = all_64_1 % 23.71/4.03 | | | | % 23.71/4.03 | | | | GROUND_INST: instantiating (19) with all_76_1, all_82_1, xm, simplifying % 23.71/4.03 | | | | with (122), (131) gives: % 23.71/4.03 | | | | (191) all_82_1 = all_76_1 % 23.71/4.03 | | | | % 23.71/4.03 | | | | GROUND_INST: instantiating (19) with all_82_1, all_84_1, xm, simplifying % 23.71/4.03 | | | | with (131), (133) gives: % 23.71/4.03 | | | | (192) all_84_1 = all_82_1 % 23.71/4.03 | | | | % 23.71/4.03 | | | | GROUND_INST: instantiating (19) with all_76_1, all_90_2, xm, simplifying % 23.71/4.03 | | | | with (122), (146) gives: % 23.71/4.03 | | | | (193) all_90_2 = all_76_1 % 23.71/4.03 | | | | % 23.71/4.03 | | | | GROUND_INST: instantiating (19) with all_80_1, all_92_3, xm, simplifying % 23.71/4.03 | | | | with (127), (151) gives: % 23.71/4.03 | | | | (194) all_92_3 = all_80_1 % 23.71/4.03 | | | | % 23.71/4.03 | | | | GROUND_INST: instantiating (19) with all_62_1, all_92_3, xm, simplifying % 23.71/4.03 | | | | with (99), (151) gives: % 23.71/4.03 | | | | (195) all_92_3 = all_62_1 % 23.71/4.03 | | | | % 23.71/4.03 | | | | GROUND_INST: instantiating (19) with all_90_2, all_94_7, xm, simplifying % 23.71/4.03 | | | | with (146), (154) gives: % 23.71/4.03 | | | | (196) all_94_7 = all_90_2 % 23.71/4.03 | | | | % 23.71/4.03 | | | | GROUND_INST: instantiating (19) with all_72_1, all_94_7, xm, simplifying % 23.71/4.03 | | | | with (117), (154) gives: % 23.71/4.03 | | | | (197) all_94_7 = all_72_1 % 23.71/4.03 | | | | % 23.71/4.03 | | | | GROUND_INST: instantiating (19) with all_84_1, all_96_7, xm, simplifying % 23.71/4.03 | | | | with (133), (159) gives: % 23.71/4.03 | | | | (198) all_96_7 = all_84_1 % 23.71/4.03 | | | | % 23.71/4.03 | | | | GROUND_INST: instantiating (19) with all_60_1, all_96_7, xm, simplifying % 23.71/4.03 | | | | with (94), (159) gives: % 23.71/4.03 | | | | (199) all_96_7 = all_60_1 % 23.71/4.03 | | | | % 23.71/4.03 | | | | GROUND_INST: instantiating (19) with all_62_2, all_74_1, xp, simplifying % 23.71/4.03 | | | | with (100), (119) gives: % 23.71/4.03 | | | | (200) all_74_1 = all_62_2 % 23.71/4.03 | | | | % 23.71/4.03 | | | | GROUND_INST: instantiating (19) with all_66_1, all_84_2, xp, simplifying % 23.71/4.03 | | | | with (108), (134) gives: % 23.71/4.03 | | | | (201) all_84_2 = all_66_1 % 23.71/4.03 | | | | % 23.71/4.03 | | | | GROUND_INST: instantiating (19) with all_84_2, all_86_2, xp, simplifying % 23.71/4.03 | | | | with (134), (136) gives: % 23.71/4.03 | | | | (202) all_86_2 = all_84_2 % 23.71/4.03 | | | | % 23.71/4.03 | | | | GROUND_INST: instantiating (19) with all_86_2, all_88_4, xp, simplifying % 23.71/4.03 | | | | with (136), (139) gives: % 23.84/4.03 | | | | (203) all_88_4 = all_86_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_88_4, all_90_4, xp, simplifying % 23.84/4.03 | | | | with (139), (147) gives: % 23.84/4.03 | | | | (204) all_90_4 = all_88_4 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_90_4, all_92_2, xp, simplifying % 23.84/4.03 | | | | with (147), (152) gives: % 23.84/4.03 | | | | (205) all_92_2 = all_90_4 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_92_2, all_94_8, xp, simplifying % 23.84/4.03 | | | | with (152), (155) gives: % 23.84/4.03 | | | | (206) all_94_8 = all_92_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_74_1, all_94_6, xp, simplifying % 23.84/4.03 | | | | with (119), (156) gives: % 23.84/4.03 | | | | (207) all_94_6 = all_74_1 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_66_1, all_94_6, xp, simplifying % 23.84/4.03 | | | | with (108), (156) gives: % 23.84/4.03 | | | | (208) all_94_6 = all_66_1 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with 0, all_106_3, xp, simplifying with % 23.84/4.03 | | | | (3), (165) gives: % 23.84/4.03 | | | | (209) all_106_3 = 0 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_94_8, all_106_3, xp, % 23.84/4.03 | | | | simplifying with (155), (165) gives: % 23.84/4.03 | | | | (210) all_106_3 = all_94_8 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_96_6, all_111_3, xp, % 23.84/4.03 | | | | simplifying with (160), (171) gives: % 23.84/4.03 | | | | (211) all_111_3 = all_96_6 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_94_6, all_111_3, xp, % 23.84/4.03 | | | | simplifying with (156), (171) gives: % 23.84/4.03 | | | | (212) all_111_3 = all_94_6 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_70_2, all_111_3, xp, % 23.84/4.03 | | | | simplifying with (113), (171) gives: % 23.84/4.03 | | | | (213) all_111_3 = all_70_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_70_1, all_80_2, xr, simplifying % 23.84/4.03 | | | | with (114), (128) gives: % 23.84/4.03 | | | | (214) all_80_2 = all_70_1 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_80_2, all_86_1, xr, simplifying % 23.84/4.03 | | | | with (128), (137) gives: % 23.84/4.03 | | | | (215) all_86_1 = all_80_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_86_1, all_90_3, xr, simplifying % 23.84/4.03 | | | | with (137), (148) gives: % 23.84/4.03 | | | | (216) all_90_3 = all_86_1 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_90_3, all_116_2, xr, % 23.84/4.03 | | | | simplifying with (148), (179) gives: % 23.84/4.03 | | | | (217) all_116_2 = all_90_3 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_60_2, all_116_2, xr, % 23.84/4.03 | | | | simplifying with (95), (179) gives: % 23.84/4.03 | | | | (218) all_116_2 = all_60_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_78_1, all_88_2, all_38_1, % 23.84/4.03 | | | | simplifying with (124), (140) gives: % 23.84/4.03 | | | | (219) all_88_2 = all_78_1 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_60_0, all_88_2, all_38_1, % 23.84/4.03 | | | | simplifying with (96), (140) gives: % 23.84/4.03 | | | | (220) all_88_2 = all_60_0 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_88_2, all_106_1, all_38_1, % 23.84/4.03 | | | | simplifying with (140), (166) gives: % 23.84/4.03 | | | | (221) all_106_1 = all_88_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_106_1, all_111_1, all_38_1, % 23.84/4.03 | | | | simplifying with (166), (172) gives: % 23.84/4.03 | | | | (222) all_111_1 = all_106_1 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_68_1, all_111_1, all_38_1, % 23.84/4.03 | | | | simplifying with (110), (172) gives: % 23.84/4.03 | | | | (223) all_111_1 = all_68_1 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_62_0, all_88_3, all_42_0, % 23.84/4.03 | | | | simplifying with (101), (141) gives: % 23.84/4.03 | | | | (224) all_88_3 = all_62_0 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_88_3, all_111_2, all_42_0, % 23.84/4.03 | | | | simplifying with (141), (173) gives: % 23.84/4.03 | | | | (225) all_111_2 = all_88_3 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (19) with all_78_2, all_111_2, all_42_0, % 23.84/4.03 | | | | simplifying with (125), (173) gives: % 23.84/4.03 | | | | (226) all_111_2 = all_78_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (22) with all_38_0, all_88_0, all_38_1, xp, % 23.84/4.03 | | | | simplifying with (26), (142) gives: % 23.84/4.03 | | | | (227) all_88_0 = all_38_0 % 23.84/4.03 | | | | % 23.84/4.03 | | | | GROUND_INST: instantiating (22) with 0, all_88_1, all_42_0, xp, % 23.84/4.03 | | | | simplifying with (34), (143) gives: % 23.84/4.03 | | | | (228) all_88_1 = 0 % 23.84/4.03 | | | | % 23.84/4.03 | | | | COMBINE_EQS: (186), (187) imply: % 23.84/4.03 | | | | (229) all_96_8 = all_82_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | SIMP: (229) implies: % 23.84/4.03 | | | | (230) all_96_8 = all_82_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | COMBINE_EQS: (217), (218) imply: % 23.84/4.03 | | | | (231) all_90_3 = all_60_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | SIMP: (231) implies: % 23.84/4.03 | | | | (232) all_90_3 = all_60_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | COMBINE_EQS: (222), (223) imply: % 23.84/4.03 | | | | (233) all_106_1 = all_68_1 % 23.84/4.03 | | | | % 23.84/4.03 | | | | SIMP: (233) implies: % 23.84/4.03 | | | | (234) all_106_1 = all_68_1 % 23.84/4.03 | | | | % 23.84/4.03 | | | | COMBINE_EQS: (225), (226) imply: % 23.84/4.03 | | | | (235) all_88_3 = all_78_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | SIMP: (235) implies: % 23.84/4.03 | | | | (236) all_88_3 = all_78_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | COMBINE_EQS: (211), (212) imply: % 23.84/4.03 | | | | (237) all_96_6 = all_94_6 % 23.84/4.03 | | | | % 23.84/4.03 | | | | COMBINE_EQS: (211), (213) imply: % 23.84/4.03 | | | | (238) all_96_6 = all_70_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | COMBINE_EQS: (221), (234) imply: % 23.84/4.03 | | | | (239) all_88_2 = all_68_1 % 23.84/4.03 | | | | % 23.84/4.03 | | | | SIMP: (239) implies: % 23.84/4.03 | | | | (240) all_88_2 = all_68_1 % 23.84/4.03 | | | | % 23.84/4.03 | | | | COMBINE_EQS: (209), (210) imply: % 23.84/4.03 | | | | (241) all_94_8 = 0 % 23.84/4.03 | | | | % 23.84/4.03 | | | | SIMP: (241) implies: % 23.84/4.03 | | | | (242) all_94_8 = 0 % 23.84/4.03 | | | | % 23.84/4.03 | | | | COMBINE_EQS: (237), (238) imply: % 23.84/4.03 | | | | (243) all_94_6 = all_70_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | SIMP: (243) implies: % 23.84/4.03 | | | | (244) all_94_6 = all_70_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | COMBINE_EQS: (198), (199) imply: % 23.84/4.03 | | | | (245) all_84_1 = all_60_1 % 23.84/4.03 | | | | % 23.84/4.03 | | | | SIMP: (245) implies: % 23.84/4.03 | | | | (246) all_84_1 = all_60_1 % 23.84/4.03 | | | | % 23.84/4.03 | | | | COMBINE_EQS: (185), (230) imply: % 23.84/4.03 | | | | (247) all_92_4 = all_82_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | SIMP: (247) implies: % 23.84/4.03 | | | | (248) all_92_4 = all_82_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | COMBINE_EQS: (207), (244) imply: % 23.84/4.03 | | | | (249) all_74_1 = all_70_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | SIMP: (249) implies: % 23.84/4.03 | | | | (250) all_74_1 = all_70_2 % 23.84/4.03 | | | | % 23.84/4.03 | | | | COMBINE_EQS: (208), (244) imply: % 23.84/4.03 | | | | (251) all_70_2 = all_66_1 % 23.84/4.03 | | | | % 23.84/4.03 | | | | COMBINE_EQS: (196), (197) imply: % 23.84/4.03 | | | | (252) all_90_2 = all_72_1 % 23.84/4.03 | | | | % 23.84/4.03 | | | | SIMP: (252) implies: % 23.84/4.03 | | | | (253) all_90_2 = all_72_1 % 23.84/4.03 | | | | % 23.84/4.03 | | | | COMBINE_EQS: (206), (242) imply: % 23.84/4.04 | | | | (254) all_92_2 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (254) implies: % 23.84/4.04 | | | | (255) all_92_2 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (205), (255) imply: % 23.84/4.04 | | | | (256) all_90_4 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (256) implies: % 23.84/4.04 | | | | (257) all_90_4 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (194), (195) imply: % 23.84/4.04 | | | | (258) all_80_1 = all_62_1 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (258) implies: % 23.84/4.04 | | | | (259) all_80_1 = all_62_1 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (184), (248) imply: % 23.84/4.04 | | | | (260) all_82_2 = all_70_0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (183), (248) imply: % 23.84/4.04 | | | | (261) all_82_2 = all_72_2 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (193), (253) imply: % 23.84/4.04 | | | | (262) all_76_1 = all_72_1 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (262) implies: % 23.84/4.04 | | | | (263) all_76_1 = all_72_1 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (216), (232) imply: % 23.84/4.04 | | | | (264) all_86_1 = all_60_2 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (264) implies: % 23.84/4.04 | | | | (265) all_86_1 = all_60_2 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (204), (257) imply: % 23.84/4.04 | | | | (266) all_88_4 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (266) implies: % 23.84/4.04 | | | | (267) all_88_4 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (219), (220) imply: % 23.84/4.04 | | | | (268) all_78_1 = all_60_0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (219), (240) imply: % 23.84/4.04 | | | | (269) all_78_1 = all_68_1 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (224), (236) imply: % 23.84/4.04 | | | | (270) all_78_2 = all_62_0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (203), (267) imply: % 23.84/4.04 | | | | (271) all_86_2 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (271) implies: % 23.84/4.04 | | | | (272) all_86_2 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (215), (265) imply: % 23.84/4.04 | | | | (273) all_80_2 = all_60_2 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (273) implies: % 23.84/4.04 | | | | (274) all_80_2 = all_60_2 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (202), (272) imply: % 23.84/4.04 | | | | (275) all_84_2 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (275) implies: % 23.84/4.04 | | | | (276) all_84_2 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (192), (246) imply: % 23.84/4.04 | | | | (277) all_82_1 = all_60_1 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (277) implies: % 23.84/4.04 | | | | (278) all_82_1 = all_60_1 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (201), (276) imply: % 23.84/4.04 | | | | (279) all_66_1 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (279) implies: % 23.84/4.04 | | | | (280) all_66_1 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (191), (278) imply: % 23.84/4.04 | | | | (281) all_76_1 = all_60_1 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (281) implies: % 23.84/4.04 | | | | (282) all_76_1 = all_60_1 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (260), (261) imply: % 23.84/4.04 | | | | (283) all_72_2 = all_70_0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (283) implies: % 23.84/4.04 | | | | (284) all_72_2 = all_70_0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (190), (259) imply: % 23.84/4.04 | | | | (285) all_64_1 = all_62_1 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (285) implies: % 23.84/4.04 | | | | (286) all_64_1 = all_62_1 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (189), (259) imply: % 23.84/4.04 | | | | (287) all_62_1 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (214), (274) imply: % 23.84/4.04 | | | | (288) all_70_1 = all_60_2 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (288) implies: % 23.84/4.04 | | | | (289) all_70_1 = all_60_2 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (268), (269) imply: % 23.84/4.04 | | | | (290) all_68_1 = all_60_0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (188), (263) imply: % 23.84/4.04 | | | | (291) all_72_1 = all_64_1 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (263), (282) imply: % 23.84/4.04 | | | | (292) all_72_1 = all_60_1 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (181), (182) imply: % 23.84/4.04 | | | | (293) all_72_2 = all_64_2 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (293) implies: % 23.84/4.04 | | | | (294) all_72_2 = all_64_2 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (200), (250) imply: % 23.84/4.04 | | | | (295) all_70_2 = all_62_2 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (295) implies: % 23.84/4.04 | | | | (296) all_70_2 = all_62_2 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (291), (292) imply: % 23.84/4.04 | | | | (297) all_64_1 = all_60_1 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (297) implies: % 23.84/4.04 | | | | (298) all_64_1 = all_60_1 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (284), (294) imply: % 23.84/4.04 | | | | (299) all_70_0 = all_64_2 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (180), (284) imply: % 23.84/4.04 | | | | (300) all_70_0 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (299), (300) imply: % 23.84/4.04 | | | | (301) all_64_2 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (251), (296) imply: % 23.84/4.04 | | | | (302) all_66_1 = all_62_2 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (302) implies: % 23.84/4.04 | | | | (303) all_66_1 = all_62_2 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (280), (303) imply: % 23.84/4.04 | | | | (304) all_62_2 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (304) implies: % 23.84/4.04 | | | | (305) all_62_2 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (286), (298) imply: % 23.84/4.04 | | | | (306) all_62_1 = all_60_1 % 23.84/4.04 | | | | % 23.84/4.04 | | | | SIMP: (306) implies: % 23.84/4.04 | | | | (307) all_62_1 = all_60_1 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (287), (307) imply: % 23.84/4.04 | | | | (308) all_60_1 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | COMBINE_EQS: (298), (308) imply: % 23.84/4.04 | | | | (309) all_64_1 = 0 % 23.84/4.04 | | | | % 23.84/4.04 | | | | BETA: splitting (102) gives: % 23.84/4.04 | | | | % 23.84/4.04 | | | | Case 1: % 23.84/4.04 | | | | | % 23.84/4.04 | | | | | (310) ~ (all_62_1 = 0) % 23.84/4.04 | | | | | % 23.84/4.04 | | | | | REDUCE: (287), (310) imply: % 23.84/4.04 | | | | | (311) $false % 23.84/4.04 | | | | | % 23.84/4.04 | | | | | CLOSE: (311) is inconsistent. % 23.84/4.04 | | | | | % 23.84/4.04 | | | | Case 2: % 23.84/4.04 | | | | | % 23.84/4.04 | | | | | (312) ~ (all_62_2 = 0) | all_62_0 = 0 % 23.84/4.04 | | | | | % 23.84/4.04 | | | | | BETA: splitting (312) gives: % 23.84/4.04 | | | | | % 23.84/4.04 | | | | | Case 1: % 23.84/4.04 | | | | | | % 23.84/4.04 | | | | | | (313) ~ (all_62_2 = 0) % 23.84/4.04 | | | | | | % 23.84/4.04 | | | | | | REDUCE: (305), (313) imply: % 23.84/4.04 | | | | | | (314) $false % 23.84/4.04 | | | | | | % 23.84/4.04 | | | | | | CLOSE: (314) is inconsistent. % 23.84/4.04 | | | | | | % 23.84/4.04 | | | | | Case 2: % 23.84/4.04 | | | | | | % 23.84/4.04 | | | | | | (315) all_62_0 = 0 % 23.84/4.04 | | | | | | % 23.84/4.04 | | | | | | COMBINE_EQS: (224), (315) imply: % 23.84/4.04 | | | | | | (316) all_88_3 = 0 % 23.84/4.04 | | | | | | % 23.84/4.04 | | | | | | BETA: splitting (144) gives: % 23.84/4.04 | | | | | | % 23.84/4.04 | | | | | | Case 1: % 23.84/4.04 | | | | | | | % 23.84/4.04 | | | | | | | (317) ~ (all_88_1 = 0) % 23.84/4.04 | | | | | | | % 23.84/4.04 | | | | | | | REDUCE: (228), (317) imply: % 23.84/4.04 | | | | | | | (318) $false % 23.84/4.04 | | | | | | | % 23.84/4.04 | | | | | | | CLOSE: (318) is inconsistent. % 23.84/4.04 | | | | | | | % 23.84/4.04 | | | | | | Case 2: % 23.84/4.04 | | | | | | | % 23.84/4.04 | | | | | | | (319) ~ (all_88_2 = 0) | ~ (all_88_3 = 0) | ~ (all_88_4 = 0) % 23.84/4.04 | | | | | | | | all_88_0 = 0 % 23.84/4.04 | | | | | | | % 23.84/4.04 | | | | | | | BETA: splitting (87) gives: % 23.84/4.04 | | | | | | | % 23.84/4.04 | | | | | | | Case 1: % 23.84/4.04 | | | | | | | | % 23.84/4.04 | | | | | | | | (320) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 23.84/4.04 | | | | | | | | (sdtlseqdt0(xp, xn) = v2 & aNaturalNumber0(xp) = v0 & % 23.84/4.04 | | | | | | | | aNaturalNumber0(xn) = v1 & ( ~ (v2 = 0) | ~ (v1 = 0) % 23.84/4.04 | | | | | | | | | ~ (v0 = 0))) % 23.84/4.04 | | | | | | | | % 23.84/4.04 | | | | | | | | DELTA: instantiating (320) with fresh symbols all_170_0, % 23.84/4.04 | | | | | | | | all_170_1, all_170_2 gives: % 23.84/4.04 | | | | | | | | (321) sdtlseqdt0(xp, xn) = all_170_0 & aNaturalNumber0(xp) = % 23.84/4.04 | | | | | | | | all_170_2 & aNaturalNumber0(xn) = all_170_1 & ( ~ % 23.84/4.04 | | | | | | | | (all_170_0 = 0) | ~ (all_170_1 = 0) | ~ (all_170_2 % 23.84/4.04 | | | | | | | | = 0)) % 23.84/4.04 | | | | | | | | % 23.84/4.04 | | | | | | | | ALPHA: (321) implies: % 23.84/4.04 | | | | | | | | (322) aNaturalNumber0(xn) = all_170_1 % 23.84/4.04 | | | | | | | | (323) aNaturalNumber0(xp) = all_170_2 % 23.84/4.04 | | | | | | | | (324) sdtlseqdt0(xp, xn) = all_170_0 % 23.84/4.04 | | | | | | | | (325) ~ (all_170_0 = 0) | ~ (all_170_1 = 0) | ~ (all_170_2 % 23.84/4.04 | | | | | | | | = 0) % 23.84/4.04 | | | | | | | | % 23.84/4.04 | | | | | | | | BETA: splitting (106) gives: % 23.84/4.04 | | | | | | | | % 23.84/4.04 | | | | | | | | Case 1: % 23.84/4.04 | | | | | | | | | % 23.84/4.04 | | | | | | | | | (326) ~ (all_64_1 = 0) % 23.84/4.04 | | | | | | | | | % 23.84/4.04 | | | | | | | | | REDUCE: (309), (326) imply: % 23.84/4.04 | | | | | | | | | (327) $false % 23.84/4.04 | | | | | | | | | % 23.84/4.04 | | | | | | | | | CLOSE: (327) is inconsistent. % 23.84/4.04 | | | | | | | | | % 23.84/4.04 | | | | | | | | Case 2: % 23.84/4.04 | | | | | | | | | % 23.84/4.04 | | | | | | | | | (328) ~ (all_64_2 = 0) | all_64_0 = 0 % 23.84/4.04 | | | | | | | | | % 23.84/4.04 | | | | | | | | | BETA: splitting (328) gives: % 23.84/4.04 | | | | | | | | | % 23.84/4.04 | | | | | | | | | Case 1: % 23.84/4.04 | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | (329) ~ (all_64_2 = 0) % 23.84/4.04 | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | REDUCE: (301), (329) imply: % 23.84/4.04 | | | | | | | | | | (330) $false % 23.84/4.04 | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | CLOSE: (330) is inconsistent. % 23.84/4.04 | | | | | | | | | | % 23.84/4.04 | | | | | | | | | Case 2: % 23.84/4.04 | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | GROUND_INST: instantiating (19) with 0, all_170_1, xn, % 23.84/4.04 | | | | | | | | | | simplifying with (1), (322) gives: % 23.84/4.04 | | | | | | | | | | (331) all_170_1 = 0 % 23.84/4.04 | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | GROUND_INST: instantiating (19) with 0, all_170_2, xp, % 23.84/4.04 | | | | | | | | | | simplifying with (3), (323) gives: % 23.84/4.04 | | | | | | | | | | (332) all_170_2 = 0 % 23.84/4.04 | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | GROUND_INST: instantiating (21) with 0, all_170_0, xn, xp, % 23.84/4.04 | | | | | | | | | | simplifying with (6), (324) gives: % 23.84/4.04 | | | | | | | | | | (333) all_170_0 = 0 % 23.84/4.04 | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | BETA: splitting (325) gives: % 23.84/4.04 | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | Case 1: % 23.84/4.04 | | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | | (334) ~ (all_170_0 = 0) % 23.84/4.04 | | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | | REDUCE: (333), (334) imply: % 23.84/4.04 | | | | | | | | | | | (335) $false % 23.84/4.04 | | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | | CLOSE: (335) is inconsistent. % 23.84/4.04 | | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | Case 2: % 23.84/4.04 | | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | | (336) ~ (all_170_1 = 0) | ~ (all_170_2 = 0) % 23.84/4.04 | | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | | BETA: splitting (336) gives: % 23.84/4.04 | | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | | Case 1: % 23.84/4.04 | | | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | | | (337) ~ (all_170_1 = 0) % 23.84/4.04 | | | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | | | REDUCE: (331), (337) imply: % 23.84/4.04 | | | | | | | | | | | | (338) $false % 23.84/4.04 | | | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | | | CLOSE: (338) is inconsistent. % 23.84/4.04 | | | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | | Case 2: % 23.84/4.04 | | | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | | | (339) ~ (all_170_2 = 0) % 23.84/4.04 | | | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | | | REDUCE: (332), (339) imply: % 23.84/4.04 | | | | | | | | | | | | (340) $false % 23.84/4.04 | | | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | | | CLOSE: (340) is inconsistent. % 23.84/4.04 | | | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | | End of split % 23.84/4.04 | | | | | | | | | | | % 23.84/4.04 | | | | | | | | | | End of split % 23.84/4.04 | | | | | | | | | | % 23.84/4.04 | | | | | | | | | End of split % 23.84/4.04 | | | | | | | | | % 23.84/4.04 | | | | | | | | End of split % 23.84/4.04 | | | | | | | | % 23.84/4.04 | | | | | | | Case 2: % 23.84/4.04 | | | | | | | | % 23.84/4.04 | | | | | | | | (341) ! [v0: $i] : (v0 = xr | ~ (sdtpldt0(xp, v0) = xn) | % 23.84/4.04 | | | | | | | | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 23.84/4.04 | | | | | | | | aNaturalNumber0(v0) = v1)) & ! [v0: $i] : ( ~ % 23.84/4.04 | | | | | | | | (sdtpldt0(xp, xr) = v0) | ~ $i(xr) | (v0 = xn & % 23.84/4.04 | | | | | | | | aNaturalNumber0(xr) = 0)) % 23.84/4.05 | | | | | | | | % 23.84/4.05 | | | | | | | | ALPHA: (341) implies: % 23.84/4.05 | | | | | | | | (342) ! [v0: $i] : ( ~ (sdtpldt0(xp, xr) = v0) | ~ $i(xr) | % 23.84/4.05 | | | | | | | | (v0 = xn & aNaturalNumber0(xr) = 0)) % 23.84/4.05 | | | | | | | | % 23.84/4.05 | | | | | | | | GROUND_INST: instantiating (342) with xn, simplifying with (10), % 23.84/4.05 | | | | | | | | (17) gives: % 23.84/4.05 | | | | | | | | (343) aNaturalNumber0(xr) = 0 % 23.84/4.05 | | | | | | | | % 23.84/4.05 | | | | | | | | BETA: splitting (319) gives: % 23.84/4.05 | | | | | | | | % 23.84/4.05 | | | | | | | | Case 1: % 23.84/4.05 | | | | | | | | | % 23.84/4.05 | | | | | | | | | (344) ~ (all_88_2 = 0) % 23.84/4.05 | | | | | | | | | % 23.84/4.05 | | | | | | | | | REDUCE: (220), (344) imply: % 23.84/4.05 | | | | | | | | | (345) ~ (all_60_0 = 0) % 23.84/4.05 | | | | | | | | | % 23.84/4.05 | | | | | | | | | BETA: splitting (97) gives: % 23.84/4.05 | | | | | | | | | % 23.84/4.05 | | | | | | | | | Case 1: % 23.84/4.05 | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | (346) ~ (all_60_1 = 0) % 23.84/4.05 | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | REDUCE: (308), (346) imply: % 23.84/4.05 | | | | | | | | | | (347) $false % 23.84/4.05 | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | CLOSE: (347) is inconsistent. % 23.84/4.05 | | | | | | | | | | % 23.84/4.05 | | | | | | | | | Case 2: % 23.84/4.05 | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | (348) ~ (all_60_2 = 0) | all_60_0 = 0 % 23.84/4.05 | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | BETA: splitting (348) gives: % 23.84/4.05 | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | Case 1: % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | | (349) ~ (all_60_2 = 0) % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | | GROUND_INST: instantiating (19) with all_60_2, 0, xr, % 23.84/4.05 | | | | | | | | | | | simplifying with (95), (343) gives: % 23.84/4.05 | | | | | | | | | | | (350) all_60_2 = 0 % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | | REDUCE: (349), (350) imply: % 23.84/4.05 | | | | | | | | | | | (351) $false % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | | CLOSE: (351) is inconsistent. % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | Case 2: % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | | (352) all_60_0 = 0 % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | | REDUCE: (345), (352) imply: % 23.84/4.05 | | | | | | | | | | | (353) $false % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | | CLOSE: (353) is inconsistent. % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | End of split % 23.84/4.05 | | | | | | | | | | % 23.84/4.05 | | | | | | | | | End of split % 23.84/4.05 | | | | | | | | | % 23.84/4.05 | | | | | | | | Case 2: % 23.84/4.05 | | | | | | | | | % 23.84/4.05 | | | | | | | | | (354) ~ (all_88_3 = 0) | ~ (all_88_4 = 0) | all_88_0 = 0 % 23.84/4.05 | | | | | | | | | % 23.84/4.05 | | | | | | | | | BETA: splitting (354) gives: % 23.84/4.05 | | | | | | | | | % 23.84/4.05 | | | | | | | | | Case 1: % 23.84/4.05 | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | (355) ~ (all_88_3 = 0) % 23.84/4.05 | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | REDUCE: (316), (355) imply: % 23.84/4.05 | | | | | | | | | | (356) $false % 23.84/4.05 | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | CLOSE: (356) is inconsistent. % 23.84/4.05 | | | | | | | | | | % 23.84/4.05 | | | | | | | | | Case 2: % 23.84/4.05 | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | (357) ~ (all_88_4 = 0) | all_88_0 = 0 % 23.84/4.05 | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | BETA: splitting (357) gives: % 23.84/4.05 | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | Case 1: % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | | (358) ~ (all_88_4 = 0) % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | | REDUCE: (267), (358) imply: % 23.84/4.05 | | | | | | | | | | | (359) $false % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | | CLOSE: (359) is inconsistent. % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | Case 2: % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | | (360) all_88_0 = 0 % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | | COMBINE_EQS: (227), (360) imply: % 23.84/4.05 | | | | | | | | | | | (361) all_38_0 = 0 % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | | SIMP: (361) implies: % 23.84/4.05 | | | | | | | | | | | (362) all_38_0 = 0 % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | | REDUCE: (24), (362) imply: % 23.84/4.05 | | | | | | | | | | | (363) $false % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | | CLOSE: (363) is inconsistent. % 23.84/4.05 | | | | | | | | | | | % 23.84/4.05 | | | | | | | | | | End of split % 23.84/4.05 | | | | | | | | | | % 23.84/4.05 | | | | | | | | | End of split % 23.84/4.05 | | | | | | | | | % 23.84/4.05 | | | | | | | | End of split % 23.84/4.05 | | | | | | | | % 23.84/4.05 | | | | | | | End of split % 23.84/4.05 | | | | | | | % 23.84/4.05 | | | | | | End of split % 23.84/4.05 | | | | | | % 23.84/4.05 | | | | | End of split % 23.84/4.05 | | | | | % 23.84/4.05 | | | | End of split % 23.84/4.05 | | | | % 23.84/4.06 | | | End of split % 23.84/4.06 | | | % 23.84/4.06 | | End of split % 23.84/4.06 | | % 23.84/4.06 | End of split % 23.84/4.06 | % 23.84/4.06 End of proof % 23.84/4.06 % SZS output end Proof for theBenchmark % 23.84/4.06 % 23.84/4.06 3426ms %------------------------------------------------------------------------------