%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : NUM498+3 : TPTP v8.1.2. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n024.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 11:48:11 EDT 2023 % Result : Theorem 77.46s 11.07s % Output : Proof 95.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM498+3 : TPTP v8.1.2. Released v4.0.0. % 0.07/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n024.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Aug 25 09:09:24 EDT 2023 % 0.13/0.35 % CPUTime : % 0.20/0.67 ________ _____ % 0.20/0.67 ___ __ \_________(_)________________________________ % 0.20/0.67 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.67 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.67 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.67 % 0.20/0.67 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.67 (2023-06-19) % 0.20/0.67 % 0.20/0.67 (c) Philipp Rümmer, 2009-2023 % 0.20/0.67 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.67 Amanda Stjerna. % 0.20/0.67 Free software under BSD-3-Clause. % 0.20/0.67 % 0.20/0.67 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.67 % 0.20/0.67 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.20/0.68 Running up to 7 provers in parallel. % 0.20/0.69 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.69 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.69 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.69 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.69 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.69 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.69 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.70/1.34 Prover 1: Preprocessing ... % 3.70/1.35 Prover 4: Preprocessing ... % 4.49/1.39 Prover 5: Preprocessing ... % 4.49/1.39 Prover 2: Preprocessing ... % 4.49/1.39 Prover 6: Preprocessing ... % 4.49/1.39 Prover 3: Preprocessing ... % 4.49/1.40 Prover 0: Preprocessing ... % 12.62/2.55 Prover 1: Constructing countermodel ... % 12.62/2.55 Prover 3: Constructing countermodel ... % 12.62/2.57 Prover 6: Proving ... % 13.76/2.72 Prover 5: Constructing countermodel ... % 17.17/3.14 Prover 2: Proving ... % 17.17/3.16 Prover 4: Constructing countermodel ... % 19.22/3.46 Prover 0: Proving ... % 72.08/10.37 Prover 2: stopped % 72.79/10.40 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 73.43/10.57 Prover 7: Preprocessing ... % 77.46/11.06 Prover 7: Constructing countermodel ... % 77.46/11.07 Prover 0: proved (10321ms) % 77.46/11.07 % 77.46/11.07 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 77.46/11.07 % 77.46/11.09 Prover 5: stopped % 77.46/11.09 Prover 3: stopped % 77.46/11.09 Prover 6: stopped % 77.46/11.10 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 77.46/11.10 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 77.46/11.10 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 77.46/11.10 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 78.95/11.26 Prover 11: Preprocessing ... % 79.57/11.30 Prover 10: Preprocessing ... % 79.57/11.32 Prover 8: Preprocessing ... % 79.57/11.33 Prover 13: Preprocessing ... % 80.34/11.47 Prover 10: Constructing countermodel ... % 80.87/11.54 Prover 8: Warning: ignoring some quantifiers % 81.43/11.55 Prover 8: Constructing countermodel ... % 81.43/11.60 Prover 13: Constructing countermodel ... % 83.78/11.86 Prover 11: Constructing countermodel ... % 94.74/13.28 Prover 7: Found proof (size 76) % 94.74/13.29 Prover 7: proved (2884ms) % 94.74/13.29 Prover 11: stopped % 94.74/13.29 Prover 8: stopped % 94.74/13.29 Prover 13: stopped % 94.74/13.29 Prover 10: stopped % 94.74/13.29 Prover 1: stopped % 94.74/13.30 Prover 4: stopped % 94.74/13.30 % 94.74/13.30 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 94.97/13.30 % 94.97/13.31 % SZS output start Proof for theBenchmark % 94.97/13.32 Assumptions after simplification: % 94.97/13.32 --------------------------------- % 94.97/13.32 % 94.97/13.32 (mAddComm) % 95.09/13.36 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ % 95.09/13.36 $i(v1) | ~ $i(v0) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | % 95.09/13.36 (sdtpldt0(v0, v1) = v2 & $i(v2))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 95.09/13.36 : ( ~ (sdtpldt0(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ aNaturalNumber0(v1) % 95.09/13.36 | ~ aNaturalNumber0(v0) | (sdtpldt0(v1, v0) = v2 & $i(v2))) % 95.09/13.36 % 95.09/13.36 (mDefPrime) % 95.09/13.37 $i(sz10) & $i(sz00) & ! [v0: $i] : ! [v1: $i] : (v1 = v0 | v1 = sz10 | ~ % 95.09/13.37 $i(v1) | ~ $i(v0) | ~ isPrime0(v0) | ~ doDivides0(v1, v0) | ~ % 95.09/13.37 aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [v0: $i] : (v0 = sz10 | % 95.09/13.37 v0 = sz00 | ~ $i(v0) | ~ aNaturalNumber0(v0) | isPrime0(v0) | ? [v1: $i] % 95.09/13.37 : ( ~ (v1 = v0) & ~ (v1 = sz10) & $i(v1) & doDivides0(v1, v0) & % 95.09/13.37 aNaturalNumber0(v1))) & ( ~ isPrime0(sz10) | ~ aNaturalNumber0(sz10)) & ( % 95.09/13.37 ~ isPrime0(sz00) | ~ aNaturalNumber0(sz00)) % 95.09/13.37 % 95.09/13.37 (mSortsC_01) % 95.09/13.37 ~ (sz10 = sz00) & $i(sz10) & $i(sz00) & aNaturalNumber0(sz10) % 95.09/13.37 % 95.09/13.37 (mZeroMul) % 95.09/13.37 $i(sz00) & ! [v0: $i] : ! [v1: $i] : (v1 = sz00 | v0 = sz00 | ~ % 95.09/13.37 (sdtasdt0(v0, v1) = sz00) | ~ $i(v1) | ~ $i(v0) | ~ aNaturalNumber0(v1) | % 95.09/13.37 ~ aNaturalNumber0(v0)) % 95.09/13.37 % 95.09/13.37 (m_MulUnit) % 95.09/13.37 $i(sz10) & ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (sdtasdt0(v0, sz10) = v1) % 95.09/13.38 | ~ $i(v0) | ~ aNaturalNumber0(v0)) & ! [v0: $i] : ! [v1: $i] : (v1 = v0 % 95.09/13.38 | ~ (sdtasdt0(sz10, v0) = v1) | ~ $i(v0) | ~ aNaturalNumber0(v0)) & ! % 95.09/13.38 [v0: $i] : ! [v1: $i] : ( ~ (sdtasdt0(v0, sz10) = v1) | ~ $i(v0) | ~ % 95.09/13.38 aNaturalNumber0(v0) | sdtasdt0(sz10, v0) = v0) & ! [v0: $i] : ! [v1: $i] : % 95.09/13.38 ( ~ (sdtasdt0(sz10, v0) = v1) | ~ $i(v0) | ~ aNaturalNumber0(v0) | % 95.09/13.38 sdtasdt0(v0, sz10) = v0) % 95.09/13.38 % 95.09/13.38 (m_MulZero) % 95.09/13.38 $i(sz00) & ! [v0: $i] : ! [v1: $i] : (v1 = sz00 | ~ (sdtasdt0(v0, sz00) = % 95.09/13.38 v1) | ~ $i(v0) | ~ aNaturalNumber0(v0)) & ! [v0: $i] : ! [v1: $i] : % 95.09/13.38 (v1 = sz00 | ~ (sdtasdt0(sz00, v0) = v1) | ~ $i(v0) | ~ % 95.09/13.38 aNaturalNumber0(v0)) & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtasdt0(v0, sz00) = % 95.09/13.38 v1) | ~ $i(v0) | ~ aNaturalNumber0(v0) | sdtasdt0(sz00, v0) = sz00) & ! % 95.09/13.38 [v0: $i] : ! [v1: $i] : ( ~ (sdtasdt0(sz00, v0) = v1) | ~ $i(v0) | ~ % 95.09/13.38 aNaturalNumber0(v0) | sdtasdt0(v0, sz00) = sz00) % 95.09/13.38 % 95.09/13.38 (m__) % 95.09/13.39 $i(xk) & $i(xp) & $i(xm) & $i(xn) & $i(sz10) & $i(sz00) & ~ doDivides0(xp, % 95.09/13.39 xm) & ~ doDivides0(xp, xn) & ! [v0: $i] : ( ~ (sdtasdt0(xp, v0) = xm) | ~ % 95.09/13.39 $i(v0) | ~ aNaturalNumber0(v0)) & ! [v0: $i] : ( ~ (sdtasdt0(xp, v0) = xn) % 95.09/13.39 | ~ $i(v0) | ~ aNaturalNumber0(v0)) & (xk = sz10 | xk = sz00) % 95.09/13.39 % 95.09/13.39 (m__1837) % 95.09/13.39 $i(xp) & $i(xm) & $i(xn) & aNaturalNumber0(xp) & aNaturalNumber0(xm) & % 95.09/13.39 aNaturalNumber0(xn) % 95.09/13.39 % 95.09/13.39 (m__1860) % 95.09/13.39 $i(xp) & $i(xm) & $i(xn) & $i(sz10) & $i(sz00) & ? [v0: $i] : ? [v1: $i] : ( % 95.09/13.39 ~ (xp = sz10) & ~ (xp = sz00) & sdtasdt0(xp, v1) = v0 & sdtasdt0(xn, xm) = % 95.09/13.39 v0 & $i(v1) & $i(v0) & isPrime0(xp) & doDivides0(xp, v0) & % 95.09/13.39 aNaturalNumber0(v1) & ! [v2: $i] : ! [v3: $i] : (v2 = xp | v2 = sz10 | ~ % 95.09/13.39 (sdtasdt0(v2, v3) = xp) | ~ $i(v3) | ~ $i(v2) | ~ aNaturalNumber0(v3) | % 95.09/13.39 ~ aNaturalNumber0(v2)) & ! [v2: $i] : (v2 = xp | v2 = sz10 | ~ $i(v2) | % 95.09/13.39 ~ doDivides0(v2, xp) | ~ aNaturalNumber0(v2))) % 95.09/13.39 % 95.09/13.40 (m__2287) % 95.09/13.40 $i(xp) & $i(xm) & $i(xn) & ? [v0: $i] : ? [v1: $i] : ( ~ (xp = xm) & ~ (xp % 95.09/13.40 = xn) & sdtpldt0(xm, v0) = xp & sdtpldt0(xn, v1) = xp & $i(v1) & $i(v0) & % 95.09/13.40 sdtlseqdt0(xm, xp) & sdtlseqdt0(xn, xp) & aNaturalNumber0(v1) & % 95.09/13.40 aNaturalNumber0(v0)) % 95.09/13.40 % 95.09/13.40 (m__2306) % 95.09/13.40 $i(xk) & $i(xp) & $i(xm) & $i(xn) & ? [v0: $i] : (sdtsldt0(v0, xp) = xk & % 95.09/13.40 sdtasdt0(xp, xk) = v0 & sdtasdt0(xn, xm) = v0 & $i(v0) & % 95.09/13.40 aNaturalNumber0(xk)) % 95.09/13.40 % 95.09/13.40 (function-axioms) % 95.09/13.41 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 95.09/13.41 (sdtsldt0(v3, v2) = v1) | ~ (sdtsldt0(v3, v2) = v0)) & ! [v0: $i] : ! % 95.09/13.41 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtmndt0(v3, v2) = v1) | % 95.09/13.41 ~ (sdtmndt0(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 95.09/13.41 [v3: $i] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 95.09/13.41 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 95.09/13.41 (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 95.09/13.41 % 95.09/13.41 Further assumptions not needed in the proof: % 95.09/13.41 -------------------------------------------- % 95.09/13.41 mAMDistr, mAddAsso, mAddCanc, mDefDiff, mDefDiv, mDefLE, mDefQuot, mDivAsso, % 95.09/13.41 mDivLE, mDivMin, mDivSum, mDivTrans, mIH, mIH_03, mLEAsym, mLENTr, mLERefl, % 95.09/13.41 mLETotal, mLETran, mMonAdd, mMonMul, mMonMul2, mMulAsso, mMulCanc, mMulComm, % 95.09/13.41 mNatSort, mPrimDiv, mSortsB, mSortsB_02, mSortsC, mZeroAdd, m_AddZero, m__1799, % 95.09/13.41 m__1870, m__2075 % 95.09/13.41 % 95.09/13.41 Those formulas are unsatisfiable: % 95.09/13.41 --------------------------------- % 95.09/13.41 % 95.09/13.41 Begin of proof % 95.09/13.41 | % 95.09/13.41 | ALPHA: (mSortsC_01) implies: % 95.09/13.41 | (1) aNaturalNumber0(sz10) % 95.09/13.41 | % 95.09/13.41 | ALPHA: (mAddComm) implies: % 95.09/13.41 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | % 95.09/13.41 | ~ $i(v1) | ~ $i(v0) | ~ aNaturalNumber0(v1) | ~ % 95.09/13.41 | aNaturalNumber0(v0) | (sdtpldt0(v1, v0) = v2 & $i(v2))) % 95.09/13.41 | % 95.09/13.41 | ALPHA: (m_MulUnit) implies: % 95.09/13.42 | (3) ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (sdtasdt0(sz10, v0) = v1) | % 95.09/13.42 | ~ $i(v0) | ~ aNaturalNumber0(v0)) % 95.09/13.42 | (4) ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (sdtasdt0(v0, sz10) = v1) | % 95.09/13.42 | ~ $i(v0) | ~ aNaturalNumber0(v0)) % 95.09/13.42 | % 95.09/13.42 | ALPHA: (m_MulZero) implies: % 95.09/13.42 | (5) ! [v0: $i] : ! [v1: $i] : (v1 = sz00 | ~ (sdtasdt0(v0, sz00) = v1) | % 95.09/13.42 | ~ $i(v0) | ~ aNaturalNumber0(v0)) % 95.09/13.42 | % 95.09/13.42 | ALPHA: (mZeroMul) implies: % 95.09/13.42 | (6) ! [v0: $i] : ! [v1: $i] : (v1 = sz00 | v0 = sz00 | ~ (sdtasdt0(v0, % 95.09/13.42 | v1) = sz00) | ~ $i(v1) | ~ $i(v0) | ~ aNaturalNumber0(v1) | ~ % 95.09/13.42 | aNaturalNumber0(v0)) % 95.09/13.42 | % 95.09/13.42 | ALPHA: (mDefPrime) implies: % 95.09/13.42 | (7) ~ isPrime0(sz10) | ~ aNaturalNumber0(sz10) % 95.09/13.42 | % 95.09/13.42 | ALPHA: (m__1837) implies: % 95.09/13.42 | (8) aNaturalNumber0(xn) % 95.09/13.42 | (9) aNaturalNumber0(xm) % 95.09/13.42 | (10) aNaturalNumber0(xp) % 95.09/13.42 | % 95.09/13.42 | ALPHA: (m__1860) implies: % 95.09/13.43 | (11) ? [v0: $i] : ? [v1: $i] : ( ~ (xp = sz10) & ~ (xp = sz00) & % 95.09/13.43 | sdtasdt0(xp, v1) = v0 & sdtasdt0(xn, xm) = v0 & $i(v1) & $i(v0) & % 95.09/13.43 | isPrime0(xp) & doDivides0(xp, v0) & aNaturalNumber0(v1) & ! [v2: % 95.09/13.43 | $i] : ! [v3: $i] : (v2 = xp | v2 = sz10 | ~ (sdtasdt0(v2, v3) = % 95.09/13.43 | xp) | ~ $i(v3) | ~ $i(v2) | ~ aNaturalNumber0(v3) | ~ % 95.09/13.43 | aNaturalNumber0(v2)) & ! [v2: $i] : (v2 = xp | v2 = sz10 | ~ % 95.09/13.43 | $i(v2) | ~ doDivides0(v2, xp) | ~ aNaturalNumber0(v2))) % 95.09/13.43 | % 95.09/13.43 | ALPHA: (m__2287) implies: % 95.09/13.43 | (12) ? [v0: $i] : ? [v1: $i] : ( ~ (xp = xm) & ~ (xp = xn) & % 95.09/13.43 | sdtpldt0(xm, v0) = xp & sdtpldt0(xn, v1) = xp & $i(v1) & $i(v0) & % 95.09/13.43 | sdtlseqdt0(xm, xp) & sdtlseqdt0(xn, xp) & aNaturalNumber0(v1) & % 95.09/13.43 | aNaturalNumber0(v0)) % 95.09/13.43 | % 95.09/13.43 | ALPHA: (m__2306) implies: % 95.09/13.43 | (13) ? [v0: $i] : (sdtsldt0(v0, xp) = xk & sdtasdt0(xp, xk) = v0 & % 95.09/13.43 | sdtasdt0(xn, xm) = v0 & $i(v0) & aNaturalNumber0(xk)) % 95.09/13.43 | % 95.09/13.43 | ALPHA: (m__) implies: % 95.09/13.43 | (14) ~ doDivides0(xp, xn) % 95.09/13.43 | (15) ~ doDivides0(xp, xm) % 95.09/13.43 | (16) $i(xn) % 95.09/13.43 | (17) $i(xm) % 95.09/13.43 | (18) xk = sz10 | xk = sz00 % 95.09/13.43 | % 95.09/13.43 | ALPHA: (function-axioms) implies: % 95.09/13.44 | (19) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 95.09/13.44 | (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 95.09/13.44 | % 95.09/13.44 | DELTA: instantiating (13) with fresh symbol all_41_0 gives: % 95.09/13.44 | (20) sdtsldt0(all_41_0, xp) = xk & sdtasdt0(xp, xk) = all_41_0 & % 95.09/13.44 | sdtasdt0(xn, xm) = all_41_0 & $i(all_41_0) & aNaturalNumber0(xk) % 95.09/13.44 | % 95.09/13.44 | ALPHA: (20) implies: % 95.09/13.44 | (21) sdtasdt0(xn, xm) = all_41_0 % 95.09/13.44 | (22) sdtasdt0(xp, xk) = all_41_0 % 95.09/13.44 | % 95.09/13.44 | DELTA: instantiating (12) with fresh symbols all_43_0, all_43_1 gives: % 95.09/13.44 | (23) ~ (xp = xm) & ~ (xp = xn) & sdtpldt0(xm, all_43_1) = xp & % 95.09/13.44 | sdtpldt0(xn, all_43_0) = xp & $i(all_43_0) & $i(all_43_1) & % 95.09/13.44 | sdtlseqdt0(xm, xp) & sdtlseqdt0(xn, xp) & aNaturalNumber0(all_43_0) & % 95.09/13.44 | aNaturalNumber0(all_43_1) % 95.09/13.44 | % 95.09/13.44 | ALPHA: (23) implies: % 95.09/13.44 | (24) ~ (xp = xn) % 95.09/13.44 | (25) aNaturalNumber0(all_43_1) % 95.09/13.44 | (26) $i(all_43_1) % 95.09/13.44 | (27) sdtpldt0(xm, all_43_1) = xp % 95.09/13.44 | % 95.09/13.44 | DELTA: instantiating (11) with fresh symbols all_45_0, all_45_1 gives: % 95.09/13.44 | (28) ~ (xp = sz10) & ~ (xp = sz00) & sdtasdt0(xp, all_45_0) = all_45_1 & % 95.09/13.45 | sdtasdt0(xn, xm) = all_45_1 & $i(all_45_0) & $i(all_45_1) & % 95.09/13.45 | isPrime0(xp) & doDivides0(xp, all_45_1) & aNaturalNumber0(all_45_0) & % 95.09/13.45 | ! [v0: $i] : ! [v1: $i] : (v0 = xp | v0 = sz10 | ~ (sdtasdt0(v0, v1) % 95.09/13.45 | = xp) | ~ $i(v1) | ~ $i(v0) | ~ aNaturalNumber0(v1) | ~ % 95.09/13.45 | aNaturalNumber0(v0)) & ! [v0: $i] : (v0 = xp | v0 = sz10 | ~ % 95.09/13.45 | $i(v0) | ~ doDivides0(v0, xp) | ~ aNaturalNumber0(v0)) % 95.09/13.45 | % 95.09/13.45 | ALPHA: (28) implies: % 95.09/13.45 | (29) doDivides0(xp, all_45_1) % 95.09/13.45 | (30) sdtasdt0(xn, xm) = all_45_1 % 95.09/13.45 | (31) ! [v0: $i] : ! [v1: $i] : (v0 = xp | v0 = sz10 | ~ (sdtasdt0(v0, % 95.09/13.45 | v1) = xp) | ~ $i(v1) | ~ $i(v0) | ~ aNaturalNumber0(v1) | ~ % 95.09/13.45 | aNaturalNumber0(v0)) % 95.09/13.45 | % 95.09/13.45 | BETA: splitting (7) gives: % 95.09/13.45 | % 95.09/13.45 | Case 1: % 95.09/13.45 | | % 95.09/13.45 | | (32) ~ aNaturalNumber0(sz10) % 95.09/13.45 | | % 95.09/13.45 | | PRED_UNIFY: (1), (32) imply: % 95.09/13.45 | | (33) $false % 95.09/13.45 | | % 95.09/13.45 | | CLOSE: (33) is inconsistent. % 95.09/13.45 | | % 95.09/13.45 | Case 2: % 95.09/13.45 | | % 95.09/13.45 | | % 95.09/13.45 | | GROUND_INST: instantiating (19) with all_41_0, all_45_1, xm, xn, simplifying % 95.09/13.45 | | with (21), (30) gives: % 95.09/13.45 | | (34) all_45_1 = all_41_0 % 95.09/13.45 | | % 95.09/13.45 | | PRED_UNIFY: (14), (29) imply: % 95.09/13.45 | | (35) ~ (all_45_1 = xn) % 95.09/13.45 | | % 95.09/13.45 | | PRED_UNIFY: (15), (29) imply: % 95.09/13.45 | | (36) ~ (all_45_1 = xm) % 95.09/13.45 | | % 95.09/13.45 | | REDUCE: (34), (36) imply: % 95.09/13.45 | | (37) ~ (all_41_0 = xm) % 95.09/13.45 | | % 95.09/13.45 | | REDUCE: (34), (35) imply: % 95.09/13.45 | | (38) ~ (all_41_0 = xn) % 95.09/13.45 | | % 95.09/13.46 | | GROUND_INST: instantiating (2) with xm, all_43_1, xp, simplifying with (9), % 95.09/13.46 | | (17), (25), (26), (27) gives: % 95.09/13.46 | | (39) sdtpldt0(all_43_1, xm) = xp & $i(xp) % 95.09/13.46 | | % 95.09/13.46 | | ALPHA: (39) implies: % 95.09/13.46 | | (40) $i(xp) % 95.09/13.46 | | % 95.09/13.46 | | GROUND_INST: instantiating (3) with xm, all_41_0, simplifying with (9), (17) % 95.09/13.46 | | gives: % 95.09/13.46 | | (41) all_41_0 = xm | ~ (sdtasdt0(sz10, xm) = all_41_0) % 95.09/13.46 | | % 95.09/13.46 | | GROUND_INST: instantiating (6) with xn, xm, simplifying with (8), (9), (16), % 95.09/13.46 | | (17) gives: % 95.09/13.46 | | (42) xm = sz00 | xn = sz00 | ~ (sdtasdt0(xn, xm) = sz00) % 95.09/13.46 | | % 95.09/13.46 | | GROUND_INST: instantiating (31) with xn, xm, simplifying with (8), (9), % 95.09/13.46 | | (16), (17) gives: % 95.09/13.46 | | (43) xp = xn | xn = sz10 | ~ (sdtasdt0(xn, xm) = xp) % 95.09/13.46 | | % 95.09/13.46 | | GROUND_INST: instantiating (4) with xp, all_41_0, simplifying with (10), % 95.09/13.46 | | (40) gives: % 95.09/13.46 | | (44) all_41_0 = xp | ~ (sdtasdt0(xp, sz10) = all_41_0) % 95.09/13.46 | | % 95.09/13.46 | | GROUND_INST: instantiating (5) with xp, all_41_0, simplifying with (10), % 95.09/13.46 | | (40) gives: % 95.09/13.46 | | (45) all_41_0 = sz00 | ~ (sdtasdt0(xp, sz00) = all_41_0) % 95.09/13.46 | | % 95.09/13.46 | | BETA: splitting (41) gives: % 95.09/13.46 | | % 95.09/13.46 | | Case 1: % 95.09/13.46 | | | % 95.09/13.46 | | | (46) ~ (sdtasdt0(sz10, xm) = all_41_0) % 95.09/13.46 | | | % 95.09/13.46 | | | PRED_UNIFY: (21), (46) imply: % 95.09/13.46 | | | (47) ~ (xn = sz10) % 95.09/13.46 | | | % 95.09/13.46 | | | BETA: splitting (43) gives: % 95.09/13.46 | | | % 95.09/13.46 | | | Case 1: % 95.09/13.46 | | | | % 95.09/13.46 | | | | (48) ~ (sdtasdt0(xn, xm) = xp) % 95.09/13.46 | | | | % 95.09/13.46 | | | | PRED_UNIFY: (21), (48) imply: % 95.09/13.46 | | | | (49) ~ (all_41_0 = xp) % 95.09/13.46 | | | | % 95.09/13.46 | | | | BETA: splitting (44) gives: % 95.09/13.46 | | | | % 95.09/13.46 | | | | Case 1: % 95.09/13.46 | | | | | % 95.09/13.46 | | | | | (50) ~ (sdtasdt0(xp, sz10) = all_41_0) % 95.09/13.46 | | | | | % 95.09/13.46 | | | | | PRED_UNIFY: (22), (50) imply: % 95.09/13.46 | | | | | (51) ~ (xk = sz10) % 95.09/13.46 | | | | | % 95.09/13.46 | | | | | BETA: splitting (18) gives: % 95.09/13.46 | | | | | % 95.09/13.46 | | | | | Case 1: % 95.09/13.46 | | | | | | % 95.09/13.46 | | | | | | (52) xk = sz00 % 95.09/13.46 | | | | | | % 95.09/13.46 | | | | | | REDUCE: (22), (52) imply: % 95.09/13.46 | | | | | | (53) sdtasdt0(xp, sz00) = all_41_0 % 95.09/13.46 | | | | | | % 95.09/13.46 | | | | | | BETA: splitting (45) gives: % 95.09/13.46 | | | | | | % 95.09/13.46 | | | | | | Case 1: % 95.09/13.46 | | | | | | | % 95.09/13.46 | | | | | | | (54) ~ (sdtasdt0(xp, sz00) = all_41_0) % 95.09/13.46 | | | | | | | % 95.09/13.46 | | | | | | | PRED_UNIFY: (53), (54) imply: % 95.09/13.46 | | | | | | | (55) $false % 95.09/13.46 | | | | | | | % 95.09/13.46 | | | | | | | CLOSE: (55) is inconsistent. % 95.09/13.46 | | | | | | | % 95.09/13.47 | | | | | | Case 2: % 95.09/13.47 | | | | | | | % 95.09/13.47 | | | | | | | (56) all_41_0 = sz00 % 95.09/13.47 | | | | | | | % 95.09/13.47 | | | | | | | REDUCE: (37), (56) imply: % 95.09/13.47 | | | | | | | (57) ~ (xm = sz00) % 95.09/13.47 | | | | | | | % 95.09/13.47 | | | | | | | SIMP: (57) implies: % 95.09/13.47 | | | | | | | (58) ~ (xm = sz00) % 95.09/13.47 | | | | | | | % 95.09/13.47 | | | | | | | REDUCE: (38), (56) imply: % 95.09/13.47 | | | | | | | (59) ~ (xn = sz00) % 95.09/13.47 | | | | | | | % 95.09/13.47 | | | | | | | SIMP: (59) implies: % 95.09/13.47 | | | | | | | (60) ~ (xn = sz00) % 95.09/13.47 | | | | | | | % 95.09/13.47 | | | | | | | REDUCE: (21), (56) imply: % 95.09/13.47 | | | | | | | (61) sdtasdt0(xn, xm) = sz00 % 95.09/13.47 | | | | | | | % 95.09/13.47 | | | | | | | BETA: splitting (42) gives: % 95.09/13.47 | | | | | | | % 95.09/13.47 | | | | | | | Case 1: % 95.09/13.47 | | | | | | | | % 95.09/13.47 | | | | | | | | (62) ~ (sdtasdt0(xn, xm) = sz00) % 95.09/13.47 | | | | | | | | % 95.09/13.47 | | | | | | | | PRED_UNIFY: (61), (62) imply: % 95.09/13.47 | | | | | | | | (63) $false % 95.09/13.47 | | | | | | | | % 95.09/13.47 | | | | | | | | CLOSE: (63) is inconsistent. % 95.09/13.47 | | | | | | | | % 95.09/13.47 | | | | | | | Case 2: % 95.09/13.47 | | | | | | | | % 95.09/13.47 | | | | | | | | (64) xm = sz00 | xn = sz00 % 95.09/13.47 | | | | | | | | % 95.09/13.47 | | | | | | | | BETA: splitting (64) gives: % 95.09/13.47 | | | | | | | | % 95.09/13.47 | | | | | | | | Case 1: % 95.09/13.47 | | | | | | | | | % 95.09/13.47 | | | | | | | | | (65) xm = sz00 % 95.09/13.47 | | | | | | | | | % 95.09/13.47 | | | | | | | | | REDUCE: (58), (65) imply: % 95.09/13.47 | | | | | | | | | (66) $false % 95.09/13.47 | | | | | | | | | % 95.09/13.47 | | | | | | | | | CLOSE: (66) is inconsistent. % 95.09/13.47 | | | | | | | | | % 95.09/13.47 | | | | | | | | Case 2: % 95.09/13.47 | | | | | | | | | % 95.09/13.47 | | | | | | | | | (67) xn = sz00 % 95.09/13.47 | | | | | | | | | % 95.09/13.47 | | | | | | | | | REDUCE: (60), (67) imply: % 95.09/13.47 | | | | | | | | | (68) $false % 95.09/13.47 | | | | | | | | | % 95.09/13.47 | | | | | | | | | CLOSE: (68) is inconsistent. % 95.09/13.47 | | | | | | | | | % 95.09/13.47 | | | | | | | | End of split % 95.09/13.47 | | | | | | | | % 95.09/13.47 | | | | | | | End of split % 95.09/13.47 | | | | | | | % 95.09/13.47 | | | | | | End of split % 95.09/13.47 | | | | | | % 95.09/13.47 | | | | | Case 2: % 95.09/13.47 | | | | | | % 95.09/13.47 | | | | | | (69) xk = sz10 % 95.09/13.47 | | | | | | % 95.09/13.47 | | | | | | REDUCE: (51), (69) imply: % 95.09/13.47 | | | | | | (70) $false % 95.09/13.47 | | | | | | % 95.09/13.47 | | | | | | CLOSE: (70) is inconsistent. % 95.09/13.47 | | | | | | % 95.09/13.47 | | | | | End of split % 95.09/13.47 | | | | | % 95.09/13.47 | | | | Case 2: % 95.09/13.47 | | | | | % 95.09/13.47 | | | | | (71) all_41_0 = xp % 95.09/13.47 | | | | | % 95.09/13.47 | | | | | REDUCE: (49), (71) imply: % 95.09/13.47 | | | | | (72) $false % 95.09/13.47 | | | | | % 95.09/13.47 | | | | | CLOSE: (72) is inconsistent. % 95.09/13.47 | | | | | % 95.09/13.47 | | | | End of split % 95.09/13.47 | | | | % 95.09/13.47 | | | Case 2: % 95.09/13.47 | | | | % 95.09/13.47 | | | | (73) xp = xn | xn = sz10 % 95.09/13.47 | | | | % 95.09/13.47 | | | | BETA: splitting (73) gives: % 95.09/13.47 | | | | % 95.09/13.47 | | | | Case 1: % 95.09/13.47 | | | | | % 95.09/13.47 | | | | | (74) xn = sz10 % 95.09/13.47 | | | | | % 95.09/13.47 | | | | | REDUCE: (47), (74) imply: % 95.09/13.47 | | | | | (75) $false % 95.09/13.47 | | | | | % 95.09/13.47 | | | | | CLOSE: (75) is inconsistent. % 95.09/13.47 | | | | | % 95.09/13.47 | | | | Case 2: % 95.09/13.47 | | | | | % 95.09/13.47 | | | | | (76) xp = xn % 95.09/13.47 | | | | | % 95.09/13.47 | | | | | REDUCE: (24), (76) imply: % 95.09/13.47 | | | | | (77) $false % 95.09/13.47 | | | | | % 95.09/13.47 | | | | | CLOSE: (77) is inconsistent. % 95.09/13.47 | | | | | % 95.09/13.47 | | | | End of split % 95.09/13.47 | | | | % 95.09/13.47 | | | End of split % 95.09/13.47 | | | % 95.09/13.47 | | Case 2: % 95.09/13.47 | | | % 95.09/13.47 | | | (78) all_41_0 = xm % 95.09/13.47 | | | % 95.09/13.47 | | | REDUCE: (37), (78) imply: % 95.09/13.47 | | | (79) $false % 95.09/13.47 | | | % 95.09/13.47 | | | CLOSE: (79) is inconsistent. % 95.09/13.47 | | | % 95.09/13.47 | | End of split % 95.09/13.47 | | % 95.09/13.47 | End of split % 95.09/13.47 | % 95.09/13.47 End of proof % 95.09/13.47 % SZS output end Proof for theBenchmark % 95.09/13.47 % 95.09/13.47 12807ms %------------------------------------------------------------------------------