%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : NUM494+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 : n017.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:09 EDT 2023 % Result : Theorem 15.81s 2.71s % Output : Proof 24.98s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.07 % Problem : NUM494+1 : TPTP v8.1.2. Released v4.0.0. % 0.04/0.08 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.07/0.26 % Computer : n017.cluster.edu % 0.07/0.26 % Model : x86_64 x86_64 % 0.07/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.26 % Memory : 8042.1875MB % 0.07/0.26 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.26 % CPULimit : 300 % 0.07/0.26 % WCLimit : 300 % 0.07/0.26 % DateTime : Fri Aug 25 11:41:09 EDT 2023 % 0.07/0.26 % CPUTime : % 0.10/0.45 ________ _____ % 0.10/0.45 ___ __ \_________(_)________________________________ % 0.10/0.45 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.10/0.45 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.10/0.45 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.10/0.45 % 0.10/0.45 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.10/0.45 (2023-06-19) % 0.10/0.45 % 0.10/0.45 (c) Philipp Rümmer, 2009-2023 % 0.10/0.45 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.10/0.46 Amanda Stjerna. % 0.10/0.46 Free software under BSD-3-Clause. % 0.10/0.46 % 0.10/0.46 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.10/0.46 % 0.10/0.46 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.10/0.47 Running up to 7 provers in parallel. % 0.10/0.48 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.10/0.48 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.10/0.48 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.10/0.48 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.10/0.48 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.10/0.48 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.10/0.48 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.36/1.04 Prover 4: Preprocessing ... % 3.36/1.04 Prover 1: Preprocessing ... % 3.48/1.08 Prover 5: Preprocessing ... % 3.48/1.08 Prover 0: Preprocessing ... % 3.48/1.08 Prover 3: Preprocessing ... % 3.48/1.08 Prover 2: Preprocessing ... % 3.48/1.08 Prover 6: Preprocessing ... % 7.81/1.72 Prover 1: Constructing countermodel ... % 8.94/1.80 Prover 3: Constructing countermodel ... % 8.94/1.84 Prover 6: Proving ... % 9.94/1.95 Prover 5: Constructing countermodel ... % 10.28/2.03 Prover 2: Proving ... % 11.07/2.11 Prover 4: Constructing countermodel ... % 12.26/2.24 Prover 0: Proving ... % 15.81/2.70 Prover 3: proved (2225ms) % 15.81/2.70 % 15.81/2.71 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 15.81/2.71 % 15.81/2.71 Prover 5: stopped % 15.95/2.71 Prover 2: stopped % 15.95/2.71 Prover 0: stopped % 15.95/2.71 Prover 6: stopped % 15.95/2.71 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 15.95/2.71 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 16.01/2.72 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 16.01/2.72 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 16.01/2.72 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 16.01/2.79 Prover 7: Preprocessing ... % 16.70/2.82 Prover 13: Preprocessing ... % 16.70/2.82 Prover 8: Preprocessing ... % 16.70/2.82 Prover 11: Preprocessing ... % 16.70/2.83 Prover 10: Preprocessing ... % 17.37/2.95 Prover 10: Constructing countermodel ... % 17.37/2.98 Prover 7: Constructing countermodel ... % 18.07/2.98 Prover 8: Warning: ignoring some quantifiers % 18.12/2.99 Prover 8: Constructing countermodel ... % 18.12/3.00 Prover 13: Constructing countermodel ... % 19.90/3.25 Prover 11: Constructing countermodel ... % 24.09/3.81 Prover 10: Found proof (size 116) % 24.09/3.81 Prover 10: proved (1098ms) % 24.09/3.81 Prover 13: stopped % 24.09/3.81 Prover 11: stopped % 24.09/3.81 Prover 7: stopped % 24.09/3.81 Prover 8: stopped % 24.09/3.81 Prover 1: stopped % 24.09/3.81 Prover 4: stopped % 24.09/3.81 % 24.09/3.81 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 24.09/3.81 % 24.09/3.82 % SZS output start Proof for theBenchmark % 24.09/3.82 Assumptions after simplification: % 24.09/3.82 --------------------------------- % 24.48/3.82 % 24.48/3.82 (mAddAsso) % 24.48/3.85 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 24.48/3.85 (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) % 24.48/3.85 | ~ $i(v0) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ % 24.48/3.85 aNaturalNumber0(v0) | ? [v5: $i] : (sdtpldt0(v1, v2) = v5 & sdtpldt0(v0, % 24.48/3.85 v5) = v4 & $i(v5) & $i(v4))) % 24.48/3.85 % 24.48/3.85 (mAddCanc) % 24.61/3.85 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v2 = v1 % 24.61/3.85 | ~ (sdtpldt0(v0, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ $i(v2) | ~ % 24.61/3.85 $i(v1) | ~ $i(v0) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ % 24.61/3.85 aNaturalNumber0(v0) | ? [v5: $i] : ? [v6: $i] : ( ~ (v6 = v5) & % 24.61/3.85 sdtpldt0(v2, v0) = v6 & sdtpldt0(v1, v0) = v5 & $i(v6) & $i(v5))) & ! % 24.61/3.85 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v2 = v1 | ~ % 24.61/3.85 (sdtpldt0(v0, v2) = v3) | ~ (sdtpldt0(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) % 24.61/3.85 | ~ $i(v0) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ % 24.61/3.85 aNaturalNumber0(v0)) % 24.61/3.85 % 24.61/3.85 (mAddComm) % 24.61/3.86 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 24.61/3.86 $i(v1) | ~ $i(v0) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | % 24.61/3.86 (sdtpldt0(v1, v0) = v2 & $i(v2))) % 24.61/3.86 % 24.61/3.86 (mDefDiff) % 24.61/3.86 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v2 | ~ % 24.61/3.86 (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v3) = v1) | ~ $i(v3) | ~ $i(v1) % 24.61/3.86 | ~ $i(v0) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v3) | ~ % 24.61/3.86 aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [v0: $i] : ! [v1: $i] : % 24.61/3.86 ! [v2: $i] : ! [v3: $i] : (v3 = v1 | ~ (sdtmndt0(v1, v0) = v2) | ~ % 24.61/3.86 (sdtpldt0(v0, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 24.61/3.86 sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! % 24.61/3.86 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (sdtmndt0(v1, v0) = % 24.61/3.86 v2) | ~ (sdtpldt0(v0, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 24.61/3.86 sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | % 24.61/3.86 aNaturalNumber0(v2)) % 24.61/3.86 % 24.61/3.86 (mDefLE) % 24.61/3.86 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v2) = v1) | ~ % 24.61/3.86 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ aNaturalNumber0(v2) | ~ % 24.61/3.86 aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v0, v1)) & ! [v0: % 24.61/3.86 $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ sdtlseqdt0(v0, v1) | ~ % 24.61/3.86 aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v2: $i] : (sdtpldt0(v0, % 24.61/3.86 v2) = v1 & $i(v2) & aNaturalNumber0(v2))) % 24.61/3.86 % 24.61/3.86 (mMonAdd) % 24.61/3.86 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 24.61/3.86 (sdtpldt0(v0, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 24.61/3.86 sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ % 24.61/3.86 aNaturalNumber0(v0) | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ( ~ (v6 = % 24.61/3.86 v3) & ~ (v5 = v4) & sdtpldt0(v2, v1) = v5 & sdtpldt0(v2, v0) = v4 & % 24.61/3.86 sdtpldt0(v1, v2) = v6 & $i(v6) & $i(v5) & $i(v4) & sdtlseqdt0(v4, v5) & % 24.61/3.86 sdtlseqdt0(v3, v6))) % 24.61/3.86 % 24.61/3.86 (mSortsB) % 24.61/3.86 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 24.61/3.86 $i(v1) | ~ $i(v0) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | % 24.61/3.86 aNaturalNumber0(v2)) % 24.61/3.86 % 24.61/3.86 (m__) % 24.61/3.87 $i(xr) & $i(xp) & $i(xm) & $i(xn) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 24.61/3.87 ? [v3: $i] : (sdtpldt0(v2, xp) = v3 & sdtpldt0(v0, xp) = v1 & sdtpldt0(xr, xm) % 24.61/3.87 = v0 & sdtpldt0(xn, xm) = v2 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & (v3 = v1 % 24.61/3.87 | ~ sdtlseqdt0(v1, v3))) % 24.61/3.87 % 24.61/3.87 (m__1799) % 24.61/3.87 $i(xp) & $i(xm) & $i(xn) & ? [v0: $i] : ? [v1: $i] : (sdtpldt0(v0, xp) = v1 % 24.61/3.87 & sdtpldt0(xn, xm) = v0 & $i(v1) & $i(v0) & ! [v2: $i] : ! [v3: $i] : ! % 24.61/3.87 [v4: $i] : ! [v5: $i] : ! [v6: $i] : ( ~ (sdtpldt0(v5, v4) = v6) | ~ % 24.61/3.87 (sdtpldt0(v2, v3) = v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 24.61/3.87 isPrime0(v4) | ~ iLess0(v6, v1) | ~ aNaturalNumber0(v4) | ~ % 24.61/3.87 aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | doDivides0(v4, v3) | % 24.61/3.87 doDivides0(v4, v2) | ? [v7: $i] : (sdtasdt0(v2, v3) = v7 & $i(v7) & ~ % 24.61/3.87 doDivides0(v4, v7)))) % 24.61/3.87 % 24.61/3.87 (m__1837) % 24.61/3.87 $i(xp) & $i(xm) & $i(xn) & aNaturalNumber0(xp) & aNaturalNumber0(xm) & % 24.61/3.87 aNaturalNumber0(xn) % 24.61/3.87 % 24.61/3.87 (m__1870) % 24.61/3.87 $i(xp) & $i(xn) & sdtlseqdt0(xp, xn) % 24.61/3.87 % 24.61/3.87 (m__1883) % 24.61/3.87 sdtmndt0(xn, xp) = xr & $i(xr) & $i(xp) & $i(xn) % 24.61/3.87 % 24.61/3.87 (m__1894) % 24.61/3.87 ~ (xr = xn) & $i(xr) & $i(xn) & sdtlseqdt0(xr, xn) % 24.61/3.87 % 24.61/3.87 (function-axioms) % 24.61/3.87 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 24.61/3.87 (sdtsldt0(v3, v2) = v1) | ~ (sdtsldt0(v3, v2) = v0)) & ! [v0: $i] : ! % 24.61/3.87 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtmndt0(v3, v2) = v1) | % 24.61/3.87 ~ (sdtmndt0(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 24.61/3.87 [v3: $i] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 24.61/3.87 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 24.61/3.87 (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 24.61/3.87 % 24.61/3.87 Further assumptions not needed in the proof: % 24.61/3.87 -------------------------------------------- % 24.61/3.87 mAMDistr, mDefDiv, mDefPrime, mDefQuot, mDivAsso, mDivLE, mDivMin, mDivSum, % 24.61/3.87 mDivTrans, mIH, mIH_03, mLEAsym, mLENTr, mLERefl, mLETotal, mLETran, mMonMul, % 24.61/3.87 mMonMul2, mMulAsso, mMulCanc, mMulComm, mNatSort, mPrimDiv, mSortsB_02, mSortsC, % 24.61/3.87 mSortsC_01, mZeroAdd, mZeroMul, m_AddZero, m_MulUnit, m_MulZero, m__1860, % 24.61/3.87 m__1913 % 24.61/3.87 % 24.61/3.87 Those formulas are unsatisfiable: % 24.61/3.87 --------------------------------- % 24.61/3.87 % 24.61/3.87 Begin of proof % 24.61/3.87 | % 24.61/3.87 | ALPHA: (mAddCanc) implies: % 24.61/3.87 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 24.61/3.87 | (v2 = v1 | ~ (sdtpldt0(v0, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ % 24.61/3.87 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ aNaturalNumber0(v2) | ~ % 24.61/3.87 | aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5: $i] : ? [v6: % 24.61/3.87 | $i] : ( ~ (v6 = v5) & sdtpldt0(v2, v0) = v6 & sdtpldt0(v1, v0) = v5 % 24.61/3.87 | & $i(v6) & $i(v5))) % 24.61/3.87 | % 24.61/3.87 | ALPHA: (mDefLE) implies: % 24.61/3.88 | (2) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ sdtlseqdt0(v0, % 24.61/3.88 | v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v2: $i] % 24.61/3.88 | : (sdtpldt0(v0, v2) = v1 & $i(v2) & aNaturalNumber0(v2))) % 24.61/3.88 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v2) = v1) | % 24.61/3.88 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ aNaturalNumber0(v2) | ~ % 24.61/3.88 | aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v0, v1)) % 24.61/3.88 | % 24.61/3.88 | ALPHA: (mDefDiff) implies: % 24.61/3.88 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v2 | ~ % 24.61/3.88 | (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v3) = v1) | ~ $i(v3) | ~ % 24.61/3.88 | $i(v1) | ~ $i(v0) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v3) | % 24.61/3.88 | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 24.61/3.88 | % 24.61/3.88 | ALPHA: (m__1837) implies: % 24.61/3.88 | (5) aNaturalNumber0(xn) % 24.61/3.88 | (6) aNaturalNumber0(xm) % 24.61/3.88 | (7) aNaturalNumber0(xp) % 24.61/3.88 | % 24.61/3.88 | ALPHA: (m__1799) implies: % 24.61/3.88 | (8) ? [v0: $i] : ? [v1: $i] : (sdtpldt0(v0, xp) = v1 & sdtpldt0(xn, xm) = % 24.61/3.88 | v0 & $i(v1) & $i(v0) & ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 24.61/3.88 | [v5: $i] : ! [v6: $i] : ( ~ (sdtpldt0(v5, v4) = v6) | ~ % 24.61/3.88 | (sdtpldt0(v2, v3) = v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 24.61/3.88 | isPrime0(v4) | ~ iLess0(v6, v1) | ~ aNaturalNumber0(v4) | ~ % 24.61/3.88 | aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | doDivides0(v4, v3) | % 24.61/3.88 | doDivides0(v4, v2) | ? [v7: $i] : (sdtasdt0(v2, v3) = v7 & $i(v7) % 24.61/3.88 | & ~ doDivides0(v4, v7)))) % 24.61/3.88 | % 24.61/3.88 | ALPHA: (m__1870) implies: % 24.61/3.88 | (9) sdtlseqdt0(xp, xn) % 24.61/3.88 | % 24.61/3.88 | ALPHA: (m__1883) implies: % 24.61/3.88 | (10) sdtmndt0(xn, xp) = xr % 24.61/3.88 | % 24.61/3.88 | ALPHA: (m__1894) implies: % 24.61/3.88 | (11) ~ (xr = xn) % 24.61/3.88 | (12) sdtlseqdt0(xr, xn) % 24.61/3.88 | % 24.61/3.88 | ALPHA: (m__) implies: % 24.61/3.88 | (13) $i(xn) % 24.61/3.88 | (14) $i(xm) % 24.61/3.88 | (15) $i(xp) % 24.61/3.88 | (16) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (sdtpldt0(v2, % 24.61/3.88 | xp) = v3 & sdtpldt0(v0, xp) = v1 & sdtpldt0(xr, xm) = v0 & % 24.61/3.88 | sdtpldt0(xn, xm) = v2 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & (v3 = v1 % 24.61/3.88 | | ~ sdtlseqdt0(v1, v3))) % 24.61/3.88 | % 24.61/3.88 | ALPHA: (function-axioms) implies: % 24.61/3.88 | (17) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 24.61/3.88 | (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 24.61/3.88 | % 24.61/3.88 | DELTA: instantiating (16) with fresh symbols all_42_0, all_42_1, all_42_2, % 24.61/3.88 | all_42_3 gives: % 24.61/3.88 | (18) sdtpldt0(all_42_1, xp) = all_42_0 & sdtpldt0(all_42_3, xp) = all_42_2 % 24.61/3.88 | & sdtpldt0(xr, xm) = all_42_3 & sdtpldt0(xn, xm) = all_42_1 & % 24.61/3.88 | $i(all_42_0) & $i(all_42_1) & $i(all_42_2) & $i(all_42_3) & (all_42_0 % 24.61/3.88 | = all_42_2 | ~ sdtlseqdt0(all_42_2, all_42_0)) % 24.61/3.88 | % 24.61/3.88 | ALPHA: (18) implies: % 24.61/3.88 | (19) sdtpldt0(xn, xm) = all_42_1 % 24.61/3.88 | (20) sdtpldt0(xr, xm) = all_42_3 % 24.61/3.88 | (21) sdtpldt0(all_42_3, xp) = all_42_2 % 24.61/3.88 | (22) sdtpldt0(all_42_1, xp) = all_42_0 % 24.61/3.88 | (23) all_42_0 = all_42_2 | ~ sdtlseqdt0(all_42_2, all_42_0) % 24.61/3.88 | % 24.61/3.88 | DELTA: instantiating (8) with fresh symbols all_44_0, all_44_1 gives: % 24.61/3.89 | (24) sdtpldt0(all_44_1, xp) = all_44_0 & sdtpldt0(xn, xm) = all_44_1 & % 24.61/3.89 | $i(all_44_0) & $i(all_44_1) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 24.61/3.89 | : ! [v3: $i] : ! [v4: $i] : ( ~ (sdtpldt0(v3, v2) = v4) | ~ % 24.61/3.89 | (sdtpldt0(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 24.61/3.89 | isPrime0(v2) | ~ iLess0(v4, all_44_0) | ~ aNaturalNumber0(v2) | ~ % 24.61/3.89 | aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | doDivides0(v2, v1) | % 24.61/3.89 | doDivides0(v2, v0) | ? [v5: $i] : (sdtasdt0(v0, v1) = v5 & $i(v5) & % 24.61/3.89 | ~ doDivides0(v2, v5))) % 24.61/3.89 | % 24.61/3.89 | ALPHA: (24) implies: % 24.61/3.89 | (25) sdtpldt0(xn, xm) = all_44_1 % 24.61/3.89 | (26) sdtpldt0(all_44_1, xp) = all_44_0 % 24.61/3.89 | % 24.61/3.89 | GROUND_INST: instantiating (17) with all_42_1, all_44_1, xm, xn, simplifying % 24.61/3.89 | with (19), (25) gives: % 24.61/3.89 | (27) all_44_1 = all_42_1 % 24.61/3.89 | % 24.61/3.89 | REDUCE: (26), (27) imply: % 24.61/3.89 | (28) sdtpldt0(all_42_1, xp) = all_44_0 % 24.61/3.89 | % 24.61/3.89 | GROUND_INST: instantiating (17) with all_42_0, all_44_0, xp, all_42_1, % 24.61/3.89 | simplifying with (22), (28) gives: % 24.61/3.89 | (29) all_44_0 = all_42_0 % 24.61/3.89 | % 24.61/3.89 | GROUND_INST: instantiating (2) with xp, xn, simplifying with (5), (7), (9), % 24.61/3.89 | (13), (15) gives: % 24.61/3.89 | (30) ? [v0: $i] : (sdtpldt0(xp, v0) = xn & $i(v0) & aNaturalNumber0(v0)) % 24.61/3.89 | % 24.61/3.89 | GROUND_INST: instantiating (mSortsB) with xn, xm, all_42_1, simplifying with % 24.61/3.89 | (5), (6), (13), (14), (19) gives: % 24.61/3.89 | (31) aNaturalNumber0(all_42_1) % 24.61/3.89 | % 24.61/3.89 | GROUND_INST: instantiating (mAddComm) with xn, xm, all_42_1, simplifying with % 24.61/3.89 | (5), (6), (13), (14), (19) gives: % 24.61/3.89 | (32) sdtpldt0(xm, xn) = all_42_1 & $i(all_42_1) % 24.61/3.89 | % 24.61/3.89 | ALPHA: (32) implies: % 24.61/3.89 | (33) $i(all_42_1) % 24.61/3.89 | (34) sdtpldt0(xm, xn) = all_42_1 % 24.61/3.89 | % 24.61/3.89 | GROUND_INST: instantiating (mAddAsso) with xn, xm, xp, all_42_1, all_42_0, % 24.61/3.89 | simplifying with (5), (6), (7), (13), (14), (15), (19), (22) % 24.61/3.89 | gives: % 24.61/3.89 | (35) ? [v0: $i] : (sdtpldt0(xm, xp) = v0 & sdtpldt0(xn, v0) = all_42_0 & % 24.61/3.89 | $i(v0) & $i(all_42_0)) % 24.61/3.89 | % 24.61/3.89 | DELTA: instantiating (30) with fresh symbol all_69_0 gives: % 24.61/3.89 | (36) sdtpldt0(xp, all_69_0) = xn & $i(all_69_0) & aNaturalNumber0(all_69_0) % 24.61/3.89 | % 24.61/3.89 | ALPHA: (36) implies: % 24.61/3.89 | (37) aNaturalNumber0(all_69_0) % 24.61/3.89 | (38) $i(all_69_0) % 24.61/3.89 | (39) sdtpldt0(xp, all_69_0) = xn % 24.61/3.89 | % 24.61/3.89 | DELTA: instantiating (35) with fresh symbol all_71_0 gives: % 24.61/3.89 | (40) sdtpldt0(xm, xp) = all_71_0 & sdtpldt0(xn, all_71_0) = all_42_0 & % 24.61/3.89 | $i(all_71_0) & $i(all_42_0) % 24.61/3.89 | % 24.61/3.89 | ALPHA: (40) implies: % 24.61/3.89 | (41) sdtpldt0(xn, all_71_0) = all_42_0 % 24.61/3.89 | (42) sdtpldt0(xm, xp) = all_71_0 % 24.61/3.89 | % 24.61/3.89 | GROUND_INST: instantiating (mSortsB) with all_42_1, xp, all_42_0, simplifying % 24.61/3.89 | with (7), (15), (22), (31), (33) gives: % 24.61/3.89 | (43) aNaturalNumber0(all_42_0) % 24.61/3.89 | % 24.61/3.89 | GROUND_INST: instantiating (mAddAsso) with xm, xn, xp, all_42_1, all_42_0, % 24.61/3.89 | simplifying with (5), (6), (7), (13), (14), (15), (22), (34) % 24.61/3.89 | gives: % 24.61/3.89 | (44) ? [v0: $i] : (sdtpldt0(xm, v0) = all_42_0 & sdtpldt0(xn, xp) = v0 & % 24.61/3.89 | $i(v0) & $i(all_42_0)) % 24.61/3.89 | % 24.61/3.89 | GROUND_INST: instantiating (mSortsB) with xm, xp, all_71_0, simplifying with % 24.61/3.89 | (6), (7), (14), (15), (42) gives: % 24.61/3.89 | (45) aNaturalNumber0(all_71_0) % 24.61/3.89 | % 24.61/3.90 | GROUND_INST: instantiating (mAddComm) with xm, xp, all_71_0, simplifying with % 24.61/3.90 | (6), (7), (14), (15), (42) gives: % 24.61/3.90 | (46) sdtpldt0(xp, xm) = all_71_0 & $i(all_71_0) % 24.61/3.90 | % 24.61/3.90 | ALPHA: (46) implies: % 24.61/3.90 | (47) $i(all_71_0) % 24.61/3.90 | (48) sdtpldt0(xp, xm) = all_71_0 % 24.61/3.90 | % 24.61/3.90 | GROUND_INST: instantiating (mAddAsso) with xp, all_69_0, xm, xn, all_42_1, % 24.61/3.90 | simplifying with (6), (7), (14), (15), (19), (37), (38), (39) % 24.61/3.90 | gives: % 24.61/3.90 | (49) ? [v0: $i] : (sdtpldt0(all_69_0, xm) = v0 & sdtpldt0(xp, v0) = % 24.61/3.90 | all_42_1 & $i(v0) & $i(all_42_1)) % 24.61/3.90 | % 24.61/3.90 | GROUND_INST: instantiating (4) with xp, xn, xr, all_69_0, simplifying with % 24.61/3.90 | (5), (7), (9), (10), (13), (15), (37), (38), (39) gives: % 24.61/3.90 | (50) all_69_0 = xr % 24.61/3.90 | % 24.61/3.90 | GROUND_INST: instantiating (mAddComm) with xp, all_69_0, xn, simplifying with % 24.61/3.90 | (7), (15), (37), (38), (39) gives: % 24.61/3.90 | (51) sdtpldt0(all_69_0, xp) = xn & $i(xn) % 24.61/3.90 | % 24.61/3.90 | ALPHA: (51) implies: % 24.61/3.90 | (52) sdtpldt0(all_69_0, xp) = xn % 24.61/3.90 | % 24.61/3.90 | DELTA: instantiating (49) with fresh symbol all_91_0 gives: % 24.61/3.90 | (53) sdtpldt0(all_69_0, xm) = all_91_0 & sdtpldt0(xp, all_91_0) = all_42_1 % 24.61/3.90 | & $i(all_91_0) & $i(all_42_1) % 24.61/3.90 | % 24.61/3.90 | ALPHA: (53) implies: % 24.61/3.90 | (54) sdtpldt0(all_69_0, xm) = all_91_0 % 24.61/3.90 | % 24.61/3.90 | DELTA: instantiating (44) with fresh symbol all_93_0 gives: % 24.61/3.90 | (55) sdtpldt0(xm, all_93_0) = all_42_0 & sdtpldt0(xn, xp) = all_93_0 & % 24.61/3.90 | $i(all_93_0) & $i(all_42_0) % 24.61/3.90 | % 24.61/3.90 | ALPHA: (55) implies: % 24.61/3.90 | (56) $i(all_42_0) % 24.61/3.90 | % 24.61/3.90 | REDUCE: (50), (52) imply: % 24.61/3.90 | (57) sdtpldt0(xr, xp) = xn % 24.61/3.90 | % 24.61/3.90 | REDUCE: (50), (54) imply: % 24.61/3.90 | (58) sdtpldt0(xr, xm) = all_91_0 % 24.61/3.90 | % 24.61/3.90 | REDUCE: (39), (50) imply: % 24.61/3.90 | (59) sdtpldt0(xp, xr) = xn % 24.61/3.90 | % 24.61/3.90 | REDUCE: (38), (50) imply: % 24.61/3.90 | (60) $i(xr) % 24.61/3.90 | % 24.61/3.90 | REDUCE: (37), (50) imply: % 24.61/3.90 | (61) aNaturalNumber0(xr) % 24.61/3.90 | % 24.61/3.90 | GROUND_INST: instantiating (17) with all_42_3, all_91_0, xm, xr, simplifying % 24.61/3.90 | with (20), (58) gives: % 24.61/3.90 | (62) all_91_0 = all_42_3 % 24.61/3.90 | % 24.61/3.90 | GROUND_INST: instantiating (mAddAsso) with xr, xm, xp, all_42_3, all_42_2, % 24.61/3.90 | simplifying with (6), (7), (14), (15), (20), (21), (60), (61) % 24.61/3.90 | gives: % 24.61/3.90 | (63) ? [v0: $i] : (sdtpldt0(xr, v0) = all_42_2 & sdtpldt0(xm, xp) = v0 & % 24.61/3.90 | $i(v0) & $i(all_42_2)) % 24.61/3.90 | % 24.61/3.90 | GROUND_INST: instantiating (mMonAdd) with xr, xn, xm, all_42_3, simplifying % 24.61/3.90 | with (5), (6), (12), (13), (14), (20), (60), (61) gives: % 24.61/3.91 | (64) xr = xn | ? [v0: $i] : ? [v1: $i] : ? [v2: any] : ( ~ (v2 = % 24.61/3.91 | all_42_3) & ~ (v1 = v0) & sdtpldt0(xm, xr) = v0 & sdtpldt0(xm, % 24.61/3.91 | xn) = v1 & sdtpldt0(xn, xm) = v2 & $i(v2) & $i(v1) & $i(v0) & % 24.61/3.91 | sdtlseqdt0(v0, v1) & sdtlseqdt0(all_42_3, v2)) % 24.61/3.91 | % 24.61/3.91 | GROUND_INST: instantiating (mAddComm) with xr, xm, all_42_3, simplifying with % 24.61/3.91 | (6), (14), (20), (60), (61) gives: % 24.61/3.91 | (65) sdtpldt0(xm, xr) = all_42_3 & $i(all_42_3) % 24.61/3.91 | % 24.61/3.91 | ALPHA: (65) implies: % 24.61/3.91 | (66) sdtpldt0(xm, xr) = all_42_3 % 24.61/3.91 | % 24.61/3.91 | GROUND_INST: instantiating (3) with all_42_1, all_42_0, xp, simplifying with % 24.61/3.91 | (7), (15), (22), (31), (33), (43), (56) gives: % 24.61/3.91 | (67) sdtlseqdt0(all_42_1, all_42_0) % 24.61/3.91 | % 24.61/3.91 | GROUND_INST: instantiating (1) with xn, xm, all_71_0, all_42_1, all_42_0, % 24.61/3.91 | simplifying with (5), (6), (13), (14), (19), (41), (45), (47) % 24.61/3.91 | gives: % 24.61/3.91 | (68) all_71_0 = xm | ? [v0: $i] : ? [v1: $i] : ( ~ (v1 = v0) & % 24.61/3.91 | sdtpldt0(all_71_0, xn) = v1 & sdtpldt0(xm, xn) = v0 & $i(v1) & % 24.61/3.91 | $i(v0)) % 24.61/3.91 | % 24.61/3.91 | GROUND_INST: instantiating (mAddComm) with xn, all_71_0, all_42_0, simplifying % 24.61/3.91 | with (5), (13), (41), (45), (47) gives: % 24.61/3.91 | (69) sdtpldt0(all_71_0, xn) = all_42_0 & $i(all_42_0) % 24.61/3.91 | % 24.61/3.91 | ALPHA: (69) implies: % 24.61/3.91 | (70) sdtpldt0(all_71_0, xn) = all_42_0 % 24.61/3.91 | % 24.61/3.91 | GROUND_INST: instantiating (1) with xn, all_71_0, xm, all_42_0, all_42_1, % 24.61/3.91 | simplifying with (5), (6), (13), (14), (19), (41), (45), (47) % 24.61/3.91 | gives: % 24.61/3.91 | (71) all_71_0 = xm | ? [v0: $i] : ? [v1: $i] : ( ~ (v1 = v0) & % 24.61/3.91 | sdtpldt0(all_71_0, xn) = v0 & sdtpldt0(xm, xn) = v1 & $i(v1) & % 24.61/3.91 | $i(v0)) % 24.61/3.91 | % 24.61/3.91 | GROUND_INST: instantiating (mAddAsso) with xp, xr, all_71_0, xn, all_42_0, % 24.61/3.91 | simplifying with (7), (15), (41), (45), (47), (59), (60), (61) % 24.61/3.91 | gives: % 24.61/3.91 | (72) ? [v0: $i] : (sdtpldt0(xr, all_71_0) = v0 & sdtpldt0(xp, v0) = % 24.61/3.91 | all_42_0 & $i(v0) & $i(all_42_0)) % 24.61/3.91 | % 24.61/3.91 | GROUND_INST: instantiating (mAddAsso) with xr, xp, xm, xn, all_42_1, % 24.61/3.91 | simplifying with (6), (7), (14), (15), (19), (57), (60), (61) % 24.61/3.91 | gives: % 24.61/3.91 | (73) ? [v0: $i] : (sdtpldt0(xr, v0) = all_42_1 & sdtpldt0(xp, xm) = v0 & % 24.61/3.91 | $i(v0) & $i(all_42_1)) % 24.61/3.91 | % 24.61/3.91 | DELTA: instantiating (63) with fresh symbol all_135_0 gives: % 24.61/3.91 | (74) sdtpldt0(xr, all_135_0) = all_42_2 & sdtpldt0(xm, xp) = all_135_0 & % 24.61/3.91 | $i(all_135_0) & $i(all_42_2) % 24.61/3.91 | % 24.61/3.91 | ALPHA: (74) implies: % 24.61/3.91 | (75) sdtpldt0(xm, xp) = all_135_0 % 24.61/3.92 | (76) sdtpldt0(xr, all_135_0) = all_42_2 % 24.61/3.92 | % 24.61/3.92 | DELTA: instantiating (73) with fresh symbol all_151_0 gives: % 24.61/3.92 | (77) sdtpldt0(xr, all_151_0) = all_42_1 & sdtpldt0(xp, xm) = all_151_0 & % 24.61/3.92 | $i(all_151_0) & $i(all_42_1) % 24.61/3.92 | % 24.61/3.92 | ALPHA: (77) implies: % 24.61/3.92 | (78) sdtpldt0(xp, xm) = all_151_0 % 24.61/3.92 | (79) sdtpldt0(xr, all_151_0) = all_42_1 % 24.61/3.92 | % 24.61/3.92 | DELTA: instantiating (72) with fresh symbol all_155_0 gives: % 24.61/3.92 | (80) sdtpldt0(xr, all_71_0) = all_155_0 & sdtpldt0(xp, all_155_0) = % 24.61/3.92 | all_42_0 & $i(all_155_0) & $i(all_42_0) % 24.61/3.92 | % 24.61/3.92 | ALPHA: (80) implies: % 24.61/3.92 | (81) sdtpldt0(xr, all_71_0) = all_155_0 % 24.61/3.92 | % 24.61/3.92 | BETA: splitting (64) gives: % 24.61/3.92 | % 24.61/3.92 | Case 1: % 24.61/3.92 | | % 24.61/3.92 | | (82) xr = xn % 24.61/3.92 | | % 24.61/3.92 | | REDUCE: (11), (82) imply: % 24.61/3.92 | | (83) $false % 24.61/3.92 | | % 24.61/3.92 | | CLOSE: (83) is inconsistent. % 24.61/3.92 | | % 24.61/3.92 | Case 2: % 24.61/3.92 | | % 24.61/3.92 | | (84) ? [v0: $i] : ? [v1: $i] : ? [v2: any] : ( ~ (v2 = all_42_3) & ~ % 24.61/3.92 | | (v1 = v0) & sdtpldt0(xm, xr) = v0 & sdtpldt0(xm, xn) = v1 & % 24.61/3.92 | | sdtpldt0(xn, xm) = v2 & $i(v2) & $i(v1) & $i(v0) & sdtlseqdt0(v0, % 24.61/3.92 | | v1) & sdtlseqdt0(all_42_3, v2)) % 24.61/3.92 | | % 24.61/3.92 | | DELTA: instantiating (84) with fresh symbols all_167_0, all_167_1, all_167_2 % 24.61/3.92 | | gives: % 24.61/3.92 | | (85) ~ (all_167_0 = all_42_3) & ~ (all_167_1 = all_167_2) & % 24.61/3.92 | | sdtpldt0(xm, xr) = all_167_2 & sdtpldt0(xm, xn) = all_167_1 & % 24.61/3.92 | | sdtpldt0(xn, xm) = all_167_0 & $i(all_167_0) & $i(all_167_1) & % 24.61/3.92 | | $i(all_167_2) & sdtlseqdt0(all_167_2, all_167_1) & % 24.61/3.92 | | sdtlseqdt0(all_42_3, all_167_0) % 24.61/3.92 | | % 24.61/3.92 | | ALPHA: (85) implies: % 24.61/3.92 | | (86) ~ (all_167_1 = all_167_2) % 24.61/3.92 | | (87) sdtpldt0(xm, xn) = all_167_1 % 24.61/3.92 | | (88) sdtpldt0(xm, xr) = all_167_2 % 24.61/3.92 | | % 24.61/3.92 | | GROUND_INST: instantiating (17) with all_42_1, all_167_1, xn, xm, % 24.61/3.92 | | simplifying with (34), (87) gives: % 24.61/3.92 | | (89) all_167_1 = all_42_1 % 24.61/3.92 | | % 24.61/3.92 | | GROUND_INST: instantiating (17) with all_71_0, all_135_0, xp, xm, % 24.61/3.92 | | simplifying with (42), (75) gives: % 24.61/3.92 | | (90) all_135_0 = all_71_0 % 24.61/3.92 | | % 24.61/3.92 | | GROUND_INST: instantiating (17) with all_42_3, all_167_2, xr, xm, % 24.61/3.92 | | simplifying with (66), (88) gives: % 24.61/3.92 | | (91) all_167_2 = all_42_3 % 24.61/3.92 | | % 24.61/3.92 | | GROUND_INST: instantiating (17) with all_71_0, all_151_0, xm, xp, % 24.61/3.92 | | simplifying with (48), (78) gives: % 24.61/3.92 | | (92) all_151_0 = all_71_0 % 24.61/3.92 | | % 24.61/3.92 | | REDUCE: (86), (89), (91) imply: % 24.61/3.92 | | (93) ~ (all_42_1 = all_42_3) % 24.61/3.92 | | % 24.61/3.92 | | REDUCE: (79), (92) imply: % 24.61/3.92 | | (94) sdtpldt0(xr, all_71_0) = all_42_1 % 24.61/3.92 | | % 24.61/3.92 | | REDUCE: (76), (90) imply: % 24.61/3.92 | | (95) sdtpldt0(xr, all_71_0) = all_42_2 % 24.61/3.92 | | % 24.61/3.92 | | GROUND_INST: instantiating (17) with all_155_0, all_42_2, all_71_0, xr, % 24.61/3.92 | | simplifying with (81), (95) gives: % 24.61/3.92 | | (96) all_155_0 = all_42_2 % 24.61/3.92 | | % 24.61/3.92 | | GROUND_INST: instantiating (17) with all_155_0, all_42_1, all_71_0, xr, % 24.61/3.92 | | simplifying with (81), (94) gives: % 24.61/3.92 | | (97) all_155_0 = all_42_1 % 24.61/3.92 | | % 24.61/3.92 | | COMBINE_EQS: (96), (97) imply: % 24.61/3.92 | | (98) all_42_1 = all_42_2 % 24.61/3.92 | | % 24.61/3.92 | | SIMP: (98) implies: % 24.61/3.92 | | (99) all_42_1 = all_42_2 % 24.61/3.92 | | % 24.61/3.92 | | REDUCE: (93), (99) imply: % 24.61/3.92 | | (100) ~ (all_42_2 = all_42_3) % 24.61/3.92 | | % 24.61/3.92 | | REDUCE: (34), (99) imply: % 24.61/3.92 | | (101) sdtpldt0(xm, xn) = all_42_2 % 24.61/3.92 | | % 24.61/3.92 | | REDUCE: (67), (99) imply: % 24.61/3.92 | | (102) sdtlseqdt0(all_42_2, all_42_0) % 24.61/3.92 | | % 24.61/3.92 | | BETA: splitting (23) gives: % 24.61/3.92 | | % 24.61/3.92 | | Case 1: % 24.61/3.92 | | | % 24.61/3.92 | | | (103) ~ sdtlseqdt0(all_42_2, all_42_0) % 24.61/3.92 | | | % 24.61/3.92 | | | PRED_UNIFY: (102), (103) imply: % 24.61/3.92 | | | (104) $false % 24.61/3.92 | | | % 24.61/3.92 | | | CLOSE: (104) is inconsistent. % 24.61/3.92 | | | % 24.61/3.92 | | Case 2: % 24.61/3.92 | | | % 24.61/3.92 | | | (105) all_42_0 = all_42_2 % 24.61/3.92 | | | % 24.61/3.92 | | | REDUCE: (70), (105) imply: % 24.61/3.93 | | | (106) sdtpldt0(all_71_0, xn) = all_42_2 % 24.61/3.93 | | | % 24.61/3.93 | | | BETA: splitting (71) gives: % 24.61/3.93 | | | % 24.61/3.93 | | | Case 1: % 24.61/3.93 | | | | % 24.61/3.93 | | | | (107) all_71_0 = xm % 24.61/3.93 | | | | % 24.98/3.93 | | | | REDUCE: (95), (107) imply: % 24.98/3.93 | | | | (108) sdtpldt0(xr, xm) = all_42_2 % 24.98/3.93 | | | | % 24.98/3.93 | | | | GROUND_INST: instantiating (17) with all_42_3, all_42_2, xm, xr, % 24.98/3.93 | | | | simplifying with (20), (108) gives: % 24.98/3.93 | | | | (109) all_42_2 = all_42_3 % 24.98/3.93 | | | | % 24.98/3.93 | | | | REDUCE: (100), (109) imply: % 24.98/3.93 | | | | (110) $false % 24.98/3.93 | | | | % 24.98/3.93 | | | | CLOSE: (110) is inconsistent. % 24.98/3.93 | | | | % 24.98/3.93 | | | Case 2: % 24.98/3.93 | | | | % 24.98/3.93 | | | | (111) ~ (all_71_0 = xm) % 24.98/3.93 | | | | (112) ? [v0: $i] : ? [v1: $i] : ( ~ (v1 = v0) & sdtpldt0(all_71_0, % 24.98/3.93 | | | | xn) = v0 & sdtpldt0(xm, xn) = v1 & $i(v1) & $i(v0)) % 24.98/3.93 | | | | % 24.98/3.93 | | | | DELTA: instantiating (112) with fresh symbols all_195_0, all_195_1 % 24.98/3.93 | | | | gives: % 24.98/3.93 | | | | (113) ~ (all_195_0 = all_195_1) & sdtpldt0(all_71_0, xn) = all_195_1 % 24.98/3.93 | | | | & sdtpldt0(xm, xn) = all_195_0 & $i(all_195_0) & $i(all_195_1) % 24.98/3.93 | | | | % 24.98/3.93 | | | | ALPHA: (113) implies: % 24.98/3.93 | | | | (114) ~ (all_195_0 = all_195_1) % 24.98/3.93 | | | | (115) sdtpldt0(xm, xn) = all_195_0 % 24.98/3.93 | | | | (116) sdtpldt0(all_71_0, xn) = all_195_1 % 24.98/3.93 | | | | % 24.98/3.93 | | | | BETA: splitting (68) gives: % 24.98/3.93 | | | | % 24.98/3.93 | | | | Case 1: % 24.98/3.93 | | | | | % 24.98/3.93 | | | | | (117) all_71_0 = xm % 24.98/3.93 | | | | | % 24.98/3.93 | | | | | REDUCE: (111), (117) imply: % 24.98/3.93 | | | | | (118) $false % 24.98/3.93 | | | | | % 24.98/3.93 | | | | | CLOSE: (118) is inconsistent. % 24.98/3.93 | | | | | % 24.98/3.93 | | | | Case 2: % 24.98/3.93 | | | | | % 24.98/3.93 | | | | | (119) ? [v0: $i] : ? [v1: $i] : ( ~ (v1 = v0) & % 24.98/3.93 | | | | | sdtpldt0(all_71_0, xn) = v1 & sdtpldt0(xm, xn) = v0 & % 24.98/3.93 | | | | | $i(v1) & $i(v0)) % 24.98/3.93 | | | | | % 24.98/3.93 | | | | | DELTA: instantiating (119) with fresh symbols all_207_0, all_207_1 % 24.98/3.93 | | | | | gives: % 24.98/3.93 | | | | | (120) ~ (all_207_0 = all_207_1) & sdtpldt0(all_71_0, xn) = % 24.98/3.93 | | | | | all_207_0 & sdtpldt0(xm, xn) = all_207_1 & $i(all_207_0) & % 24.98/3.93 | | | | | $i(all_207_1) % 24.98/3.93 | | | | | % 24.98/3.93 | | | | | ALPHA: (120) implies: % 24.98/3.93 | | | | | (121) sdtpldt0(xm, xn) = all_207_1 % 24.98/3.93 | | | | | (122) sdtpldt0(all_71_0, xn) = all_207_0 % 24.98/3.93 | | | | | % 24.98/3.93 | | | | | GROUND_INST: instantiating (17) with all_195_0, all_207_1, xn, xm, % 24.98/3.93 | | | | | simplifying with (115), (121) gives: % 24.98/3.93 | | | | | (123) all_207_1 = all_195_0 % 24.98/3.93 | | | | | % 24.98/3.93 | | | | | GROUND_INST: instantiating (17) with all_42_2, all_207_1, xn, xm, % 24.98/3.93 | | | | | simplifying with (101), (121) gives: % 24.98/3.93 | | | | | (124) all_207_1 = all_42_2 % 24.98/3.93 | | | | | % 24.98/3.93 | | | | | GROUND_INST: instantiating (17) with all_195_1, all_207_0, xn, % 24.98/3.93 | | | | | all_71_0, simplifying with (116), (122) gives: % 24.98/3.93 | | | | | (125) all_207_0 = all_195_1 % 24.98/3.93 | | | | | % 24.98/3.93 | | | | | GROUND_INST: instantiating (17) with all_42_2, all_207_0, xn, % 24.98/3.93 | | | | | all_71_0, simplifying with (106), (122) gives: % 24.98/3.93 | | | | | (126) all_207_0 = all_42_2 % 24.98/3.93 | | | | | % 24.98/3.93 | | | | | COMBINE_EQS: (125), (126) imply: % 24.98/3.93 | | | | | (127) all_195_1 = all_42_2 % 24.98/3.93 | | | | | % 24.98/3.93 | | | | | COMBINE_EQS: (123), (124) imply: % 24.98/3.93 | | | | | (128) all_195_0 = all_42_2 % 24.98/3.93 | | | | | % 24.98/3.93 | | | | | SIMP: (128) implies: % 24.98/3.93 | | | | | (129) all_195_0 = all_42_2 % 24.98/3.93 | | | | | % 24.98/3.93 | | | | | REDUCE: (114), (127), (129) imply: % 24.98/3.93 | | | | | (130) $false % 24.98/3.93 | | | | | % 24.98/3.93 | | | | | CLOSE: (130) is inconsistent. % 24.98/3.93 | | | | | % 24.98/3.93 | | | | End of split % 24.98/3.93 | | | | % 24.98/3.93 | | | End of split % 24.98/3.93 | | | % 24.98/3.93 | | End of split % 24.98/3.93 | | % 24.98/3.93 | End of split % 24.98/3.93 | % 24.98/3.93 End of proof % 24.98/3.93 % SZS output end Proof for theBenchmark % 24.98/3.93 % 24.98/3.93 3476ms %------------------------------------------------------------------------------