%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : NUM466+2 : TPTP v8.1.2. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : 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:47:56 EDT 2023 % Result : Theorem 14.51s 2.89s % Output : Proof 22.00s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUM466+2 : TPTP v8.1.2. Released v4.0.0. % 0.00/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.33 % Computer : n008.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.33 % CPULimit : 300 % 0.14/0.33 % WCLimit : 300 % 0.14/0.33 % DateTime : Fri Aug 25 11:57:17 EDT 2023 % 0.14/0.33 % CPUTime : % 0.17/0.63 ________ _____ % 0.17/0.63 ___ __ \_________(_)________________________________ % 0.17/0.63 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.17/0.63 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.17/0.63 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.17/0.63 % 0.17/0.63 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.17/0.63 (2023-06-19) % 0.17/0.63 % 0.17/0.63 (c) Philipp Rümmer, 2009-2023 % 0.17/0.63 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.17/0.63 Amanda Stjerna. % 0.17/0.63 Free software under BSD-3-Clause. % 0.17/0.63 % 0.17/0.63 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.17/0.63 % 0.17/0.63 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.17/0.64 Running up to 7 provers in parallel. % 0.17/0.67 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.17/0.67 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.17/0.67 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.17/0.67 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.17/0.67 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.17/0.67 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.17/0.67 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.33/1.29 Prover 1: Preprocessing ... % 3.33/1.31 Prover 4: Preprocessing ... % 3.82/1.36 Prover 0: Preprocessing ... % 3.82/1.36 Prover 3: Preprocessing ... % 3.82/1.36 Prover 6: Preprocessing ... % 3.82/1.36 Prover 5: Preprocessing ... % 3.82/1.36 Prover 2: Preprocessing ... % 10.78/2.34 Prover 3: Constructing countermodel ... % 10.78/2.34 Prover 6: Proving ... % 10.78/2.35 Prover 1: Constructing countermodel ... % 11.34/2.47 Prover 5: Constructing countermodel ... % 13.59/2.73 Prover 2: Proving ... % 13.59/2.78 Prover 4: Constructing countermodel ... % 14.51/2.89 Prover 3: proved (2231ms) % 14.51/2.89 % 14.51/2.89 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 14.51/2.89 % 14.51/2.90 Prover 5: stopped % 14.51/2.90 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 14.51/2.90 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 14.51/2.91 Prover 6: stopped % 14.51/2.91 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 14.51/3.00 Prover 2: stopped % 14.51/3.00 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 15.43/3.04 Prover 7: Preprocessing ... % 15.43/3.05 Prover 0: Proving ... % 15.43/3.05 Prover 0: stopped % 15.43/3.06 Prover 8: Preprocessing ... % 15.83/3.07 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 16.08/3.11 Prover 10: Preprocessing ... % 16.08/3.11 Prover 11: Preprocessing ... % 16.32/3.21 Prover 13: Preprocessing ... % 17.54/3.34 Prover 7: Constructing countermodel ... % 18.53/3.45 Prover 8: Warning: ignoring some quantifiers % 18.53/3.45 Prover 10: Constructing countermodel ... % 18.53/3.48 Prover 8: Constructing countermodel ... % 19.20/3.63 Prover 13: Constructing countermodel ... % 19.20/3.70 Prover 1: Found proof (size 125) % 19.20/3.70 Prover 1: proved (3049ms) % 19.20/3.71 Prover 4: stopped % 19.20/3.71 Prover 8: stopped % 19.20/3.71 Prover 10: stopped % 19.20/3.71 Prover 7: stopped % 19.20/3.71 Prover 13: stopped % 20.52/3.83 Prover 11: Constructing countermodel ... % 20.94/3.86 Prover 11: stopped % 20.94/3.86 % 20.94/3.86 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 20.94/3.86 % 20.94/3.91 % SZS output start Proof for theBenchmark % 20.94/3.91 Assumptions after simplification: % 20.94/3.91 --------------------------------- % 20.94/3.91 % 20.94/3.91 (mMulAsso) % 21.45/3.96 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 21.45/3.96 (sdtasdt0(v3, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) % 21.45/3.96 | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? % 21.45/3.96 [v9: $i] : (sdtasdt0(v1, v2) = v8 & sdtasdt0(v0, v8) = v9 & % 21.45/3.96 aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & aNaturalNumber0(v0) % 21.45/3.96 = v5 & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v9 = % 21.45/3.96 v4))) % 21.45/3.96 % 21.45/3.96 (mMulComm) % 21.45/3.97 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 21.45/3.97 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 21.45/3.97 (sdtasdt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 % 21.45/3.97 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 21.45/3.97 % 21.45/3.97 (mSortsB_02) % 21.45/3.97 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 21.45/3.97 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 21.45/3.97 (aNaturalNumber0(v2) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = % 21.45/3.97 v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 21.45/3.97 % 21.45/3.97 (m__) % 21.45/3.98 $i(xn) & $i(xm) & $i(xl) & ? [v0: int] : ( ~ (v0 = 0) & doDivides0(xm, xn) = % 21.45/3.98 0 & doDivides0(xl, xn) = v0 & doDivides0(xl, xm) = 0 & ! [v1: $i] : ( ~ % 21.45/3.98 (sdtasdt0(xl, v1) = xn) | ~ $i(v1) | ? [v2: int] : ( ~ (v2 = 0) & % 21.45/3.98 aNaturalNumber0(v1) = v2)) & ? [v1: $i] : (sdtasdt0(xm, v1) = xn & % 21.45/3.98 aNaturalNumber0(v1) = 0 & $i(v1)) & ? [v1: $i] : (sdtasdt0(xl, v1) = xm & % 21.45/3.98 aNaturalNumber0(v1) = 0 & $i(v1))) % 21.45/3.98 % 21.45/3.98 (m__1218) % 21.45/3.98 aNaturalNumber0(xn) = 0 & aNaturalNumber0(xm) = 0 & aNaturalNumber0(xl) = 0 & % 21.45/3.98 $i(xn) & $i(xm) & $i(xl) % 21.45/3.98 % 21.45/3.98 (function-axioms) % 21.45/3.99 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 21.45/3.99 (sdtsldt0(v3, v2) = v1) | ~ (sdtsldt0(v3, v2) = v0)) & ! [v0: % 21.45/3.99 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 21.45/3.99 : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ (doDivides0(v3, v2) = v0)) & ! % 21.45/3.99 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 21.45/3.99 $i] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) & ! % 21.45/3.99 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 21.45/3.99 (sdtmndt0(v3, v2) = v1) | ~ (sdtmndt0(v3, v2) = v0)) & ! [v0: % 21.45/3.99 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 21.45/3.99 : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ (sdtlseqdt0(v3, v2) = v0)) & ! % 21.45/3.99 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 21.45/3.99 (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 21.45/3.99 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | % 21.45/3.99 ~ (sdtpldt0(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 21.45/3.99 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) % 21.45/3.99 | ~ (aNaturalNumber0(v2) = v0)) % 21.45/3.99 % 21.45/3.99 Further assumptions not needed in the proof: % 21.45/3.99 -------------------------------------------- % 21.45/3.99 mAMDistr, mAddAsso, mAddCanc, mAddComm, mDefDiff, mDefDiv, mDefLE, mDefQuot, % 21.45/3.99 mIH, mIH_03, mLEAsym, mLENTr, mLERefl, mLETotal, mLETran, mMonAdd, mMonMul, % 21.45/3.99 mMonMul2, mMulCanc, mNatSort, mSortsB, mSortsC, mSortsC_01, mZeroAdd, mZeroMul, % 21.45/3.99 m_AddZero, m_MulUnit, m_MulZero % 21.45/3.99 % 21.45/3.99 Those formulas are unsatisfiable: % 21.45/3.99 --------------------------------- % 21.45/3.99 % 21.45/3.99 Begin of proof % 21.45/3.99 | % 21.45/3.99 | ALPHA: (m__1218) implies: % 21.45/3.99 | (1) aNaturalNumber0(xl) = 0 % 21.45/3.99 | % 21.45/3.99 | ALPHA: (m__) implies: % 21.45/4.00 | (2) $i(xl) % 21.45/4.00 | (3) $i(xm) % 21.73/4.00 | (4) ? [v0: int] : ( ~ (v0 = 0) & doDivides0(xm, xn) = 0 & doDivides0(xl, % 21.73/4.00 | xn) = v0 & doDivides0(xl, xm) = 0 & ! [v1: $i] : ( ~ (sdtasdt0(xl, % 21.73/4.00 | v1) = xn) | ~ $i(v1) | ? [v2: int] : ( ~ (v2 = 0) & % 21.73/4.00 | aNaturalNumber0(v1) = v2)) & ? [v1: $i] : (sdtasdt0(xm, v1) = xn % 21.73/4.00 | & aNaturalNumber0(v1) = 0 & $i(v1)) & ? [v1: $i] : (sdtasdt0(xl, % 21.73/4.00 | v1) = xm & aNaturalNumber0(v1) = 0 & $i(v1))) % 21.73/4.00 | % 21.73/4.00 | ALPHA: (function-axioms) implies: % 21.73/4.00 | (5) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 21.73/4.00 | (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = % 21.73/4.00 | v0)) % 21.73/4.00 | % 21.73/4.00 | DELTA: instantiating (4) with fresh symbol all_31_0 gives: % 21.73/4.01 | (6) ~ (all_31_0 = 0) & doDivides0(xm, xn) = 0 & doDivides0(xl, xn) = % 21.73/4.01 | all_31_0 & doDivides0(xl, xm) = 0 & ! [v0: $i] : ( ~ (sdtasdt0(xl, v0) % 21.73/4.01 | = xn) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 21.73/4.01 | aNaturalNumber0(v0) = v1)) & ? [v0: $i] : (sdtasdt0(xm, v0) = xn & % 21.73/4.01 | aNaturalNumber0(v0) = 0 & $i(v0)) & ? [v0: $i] : (sdtasdt0(xl, v0) = % 21.73/4.01 | xm & aNaturalNumber0(v0) = 0 & $i(v0)) % 21.73/4.01 | % 21.73/4.01 | ALPHA: (6) implies: % 21.73/4.01 | (7) ! [v0: $i] : ( ~ (sdtasdt0(xl, v0) = xn) | ~ $i(v0) | ? [v1: int] : % 21.73/4.01 | ( ~ (v1 = 0) & aNaturalNumber0(v0) = v1)) % 21.73/4.01 | (8) ? [v0: $i] : (sdtasdt0(xl, v0) = xm & aNaturalNumber0(v0) = 0 & % 21.73/4.01 | $i(v0)) % 21.73/4.01 | (9) ? [v0: $i] : (sdtasdt0(xm, v0) = xn & aNaturalNumber0(v0) = 0 & % 21.73/4.01 | $i(v0)) % 21.73/4.01 | % 21.73/4.01 | DELTA: instantiating (9) with fresh symbol all_34_0 gives: % 21.73/4.01 | (10) sdtasdt0(xm, all_34_0) = xn & aNaturalNumber0(all_34_0) = 0 & % 21.73/4.01 | $i(all_34_0) % 21.73/4.01 | % 21.73/4.01 | ALPHA: (10) implies: % 21.73/4.01 | (11) $i(all_34_0) % 21.73/4.01 | (12) aNaturalNumber0(all_34_0) = 0 % 21.73/4.01 | (13) sdtasdt0(xm, all_34_0) = xn % 21.73/4.01 | % 21.73/4.01 | DELTA: instantiating (8) with fresh symbol all_36_0 gives: % 21.73/4.01 | (14) sdtasdt0(xl, all_36_0) = xm & aNaturalNumber0(all_36_0) = 0 & % 21.73/4.01 | $i(all_36_0) % 21.73/4.01 | % 21.73/4.01 | ALPHA: (14) implies: % 21.73/4.01 | (15) $i(all_36_0) % 21.73/4.01 | (16) aNaturalNumber0(all_36_0) = 0 % 21.73/4.01 | (17) sdtasdt0(xl, all_36_0) = xm % 21.73/4.01 | % 21.73/4.02 | GROUND_INST: instantiating (mMulComm) with xl, all_36_0, xm, simplifying with % 21.73/4.02 | (2), (15), (17) gives: % 21.73/4.02 | (18) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_36_0, xl) = % 21.73/4.02 | v2 & aNaturalNumber0(all_36_0) = v1 & aNaturalNumber0(xl) = v0 & % 21.73/4.02 | $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = xm)) % 21.73/4.02 | % 21.73/4.02 | GROUND_INST: instantiating (mMulAsso) with xl, all_36_0, all_34_0, xm, xn, % 21.73/4.02 | simplifying with (2), (11), (13), (15), (17) gives: % 21.73/4.02 | (19) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: $i] % 21.73/4.02 | : (sdtasdt0(all_36_0, all_34_0) = v3 & sdtasdt0(xl, v3) = v4 & % 21.73/4.02 | aNaturalNumber0(all_36_0) = v1 & aNaturalNumber0(all_34_0) = v2 & % 21.73/4.02 | aNaturalNumber0(xl) = v0 & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = % 21.73/4.02 | 0) | ~ (v0 = 0) | v4 = xn)) % 21.73/4.02 | % 21.73/4.02 | GROUND_INST: instantiating (mMulComm) with xm, all_34_0, xn, simplifying with % 21.73/4.02 | (3), (11), (13) gives: % 21.73/4.02 | (20) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_34_0, xm) = % 21.73/4.02 | v2 & aNaturalNumber0(all_34_0) = v1 & aNaturalNumber0(xm) = v0 & % 21.73/4.02 | $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = xn)) % 21.73/4.02 | % 21.73/4.02 | DELTA: instantiating (20) with fresh symbols all_43_0, all_43_1, all_43_2 % 21.73/4.02 | gives: % 21.73/4.02 | (21) sdtasdt0(all_34_0, xm) = all_43_0 & aNaturalNumber0(all_34_0) = % 21.73/4.03 | all_43_1 & aNaturalNumber0(xm) = all_43_2 & $i(all_43_0) & ( ~ % 21.73/4.03 | (all_43_1 = 0) | ~ (all_43_2 = 0) | all_43_0 = xn) % 21.73/4.03 | % 21.73/4.03 | ALPHA: (21) implies: % 21.73/4.03 | (22) aNaturalNumber0(all_34_0) = all_43_1 % 21.73/4.03 | % 21.73/4.03 | DELTA: instantiating (18) with fresh symbols all_45_0, all_45_1, all_45_2 % 21.73/4.03 | gives: % 21.73/4.03 | (23) sdtasdt0(all_36_0, xl) = all_45_0 & aNaturalNumber0(all_36_0) = % 21.73/4.03 | all_45_1 & aNaturalNumber0(xl) = all_45_2 & $i(all_45_0) & ( ~ % 21.73/4.03 | (all_45_1 = 0) | ~ (all_45_2 = 0) | all_45_0 = xm) % 21.73/4.03 | % 21.73/4.03 | ALPHA: (23) implies: % 21.73/4.03 | (24) aNaturalNumber0(xl) = all_45_2 % 21.73/4.03 | (25) aNaturalNumber0(all_36_0) = all_45_1 % 21.73/4.03 | (26) sdtasdt0(all_36_0, xl) = all_45_0 % 21.73/4.03 | (27) ~ (all_45_1 = 0) | ~ (all_45_2 = 0) | all_45_0 = xm % 21.73/4.03 | % 21.73/4.03 | DELTA: instantiating (19) with fresh symbols all_47_0, all_47_1, all_47_2, % 21.73/4.03 | all_47_3, all_47_4 gives: % 21.73/4.03 | (28) sdtasdt0(all_36_0, all_34_0) = all_47_1 & sdtasdt0(xl, all_47_1) = % 21.73/4.03 | all_47_0 & aNaturalNumber0(all_36_0) = all_47_3 & % 21.73/4.03 | aNaturalNumber0(all_34_0) = all_47_2 & aNaturalNumber0(xl) = all_47_4 % 21.73/4.03 | & $i(all_47_0) & $i(all_47_1) & ( ~ (all_47_2 = 0) | ~ (all_47_3 = 0) % 21.73/4.03 | | ~ (all_47_4 = 0) | all_47_0 = xn) % 21.73/4.03 | % 21.73/4.03 | ALPHA: (28) implies: % 21.73/4.03 | (29) $i(all_47_1) % 21.73/4.03 | (30) aNaturalNumber0(xl) = all_47_4 % 21.73/4.03 | (31) aNaturalNumber0(all_34_0) = all_47_2 % 21.73/4.03 | (32) aNaturalNumber0(all_36_0) = all_47_3 % 21.73/4.03 | (33) sdtasdt0(xl, all_47_1) = all_47_0 % 21.73/4.03 | (34) sdtasdt0(all_36_0, all_34_0) = all_47_1 % 21.73/4.03 | (35) ~ (all_47_2 = 0) | ~ (all_47_3 = 0) | ~ (all_47_4 = 0) | all_47_0 = % 21.73/4.03 | xn % 21.73/4.03 | % 21.73/4.04 | GROUND_INST: instantiating (5) with 0, all_47_4, xl, simplifying with (1), % 21.73/4.04 | (30) gives: % 21.73/4.04 | (36) all_47_4 = 0 % 21.73/4.04 | % 21.73/4.04 | GROUND_INST: instantiating (5) with all_45_2, all_47_4, xl, simplifying with % 21.73/4.04 | (24), (30) gives: % 21.73/4.04 | (37) all_47_4 = all_45_2 % 21.73/4.04 | % 21.73/4.04 | GROUND_INST: instantiating (5) with 0, all_47_2, all_34_0, simplifying with % 21.73/4.04 | (12), (31) gives: % 21.73/4.04 | (38) all_47_2 = 0 % 21.73/4.04 | % 21.73/4.04 | GROUND_INST: instantiating (5) with all_43_1, all_47_2, all_34_0, simplifying % 21.73/4.04 | with (22), (31) gives: % 21.73/4.04 | (39) all_47_2 = all_43_1 % 21.73/4.04 | % 21.73/4.04 | GROUND_INST: instantiating (5) with 0, all_47_3, all_36_0, simplifying with % 21.73/4.04 | (16), (32) gives: % 21.73/4.04 | (40) all_47_3 = 0 % 21.73/4.04 | % 21.73/4.04 | GROUND_INST: instantiating (5) with all_45_1, all_47_3, all_36_0, simplifying % 21.73/4.04 | with (25), (32) gives: % 21.73/4.04 | (41) all_47_3 = all_45_1 % 21.73/4.04 | % 21.73/4.04 | COMBINE_EQS: (38), (39) imply: % 21.73/4.04 | (42) all_43_1 = 0 % 21.73/4.04 | % 21.73/4.04 | SIMP: (42) implies: % 21.73/4.04 | (43) all_43_1 = 0 % 21.73/4.04 | % 21.73/4.04 | COMBINE_EQS: (40), (41) imply: % 21.73/4.04 | (44) all_45_1 = 0 % 21.73/4.04 | % 21.73/4.04 | SIMP: (44) implies: % 21.73/4.04 | (45) all_45_1 = 0 % 21.73/4.04 | % 21.73/4.04 | COMBINE_EQS: (36), (37) imply: % 21.73/4.04 | (46) all_45_2 = 0 % 21.73/4.04 | % 21.73/4.04 | SIMP: (46) implies: % 21.73/4.04 | (47) all_45_2 = 0 % 21.73/4.04 | % 21.73/4.04 | BETA: splitting (27) gives: % 21.73/4.04 | % 21.73/4.04 | Case 1: % 21.73/4.04 | | % 21.73/4.04 | | (48) ~ (all_45_1 = 0) % 21.73/4.04 | | % 21.73/4.04 | | REDUCE: (45), (48) imply: % 21.73/4.04 | | (49) $false % 21.73/4.05 | | % 21.73/4.05 | | CLOSE: (49) is inconsistent. % 21.73/4.05 | | % 21.73/4.05 | Case 2: % 21.73/4.05 | | % 21.73/4.05 | | (50) ~ (all_45_2 = 0) | all_45_0 = xm % 21.73/4.05 | | % 21.73/4.05 | | DELTA: instantiating (9) with fresh symbol all_72_0 gives: % 21.73/4.05 | | (51) sdtasdt0(xm, all_72_0) = xn & aNaturalNumber0(all_72_0) = 0 & % 21.73/4.05 | | $i(all_72_0) % 21.73/4.05 | | % 21.73/4.05 | | ALPHA: (51) implies: % 21.73/4.05 | | (52) $i(all_72_0) % 21.73/4.05 | | (53) sdtasdt0(xm, all_72_0) = xn % 21.73/4.05 | | % 21.73/4.05 | | BETA: splitting (35) gives: % 21.73/4.05 | | % 21.73/4.05 | | Case 1: % 21.73/4.05 | | | % 21.73/4.05 | | | (54) ~ (all_47_2 = 0) % 21.73/4.05 | | | % 21.73/4.05 | | | REDUCE: (38), (54) imply: % 21.73/4.05 | | | (55) $false % 21.73/4.05 | | | % 21.73/4.05 | | | CLOSE: (55) is inconsistent. % 21.73/4.05 | | | % 21.73/4.05 | | Case 2: % 21.73/4.05 | | | % 21.73/4.05 | | | (56) ~ (all_47_3 = 0) | ~ (all_47_4 = 0) | all_47_0 = xn % 21.73/4.05 | | | % 21.73/4.05 | | | DELTA: instantiating (8) with fresh symbol all_81_0 gives: % 21.73/4.05 | | | (57) sdtasdt0(xl, all_81_0) = xm & aNaturalNumber0(all_81_0) = 0 & % 21.73/4.05 | | | $i(all_81_0) % 21.73/4.05 | | | % 21.73/4.05 | | | ALPHA: (57) implies: % 21.73/4.05 | | | (58) $i(all_81_0) % 21.73/4.05 | | | (59) sdtasdt0(xl, all_81_0) = xm % 21.73/4.05 | | | % 21.73/4.05 | | | BETA: splitting (50) gives: % 21.73/4.05 | | | % 21.73/4.05 | | | Case 1: % 21.73/4.05 | | | | % 21.73/4.05 | | | | (60) ~ (all_45_2 = 0) % 21.73/4.05 | | | | % 21.73/4.05 | | | | REDUCE: (47), (60) imply: % 21.73/4.05 | | | | (61) $false % 21.73/4.05 | | | | % 21.73/4.05 | | | | CLOSE: (61) is inconsistent. % 21.73/4.05 | | | | % 21.73/4.05 | | | Case 2: % 21.73/4.05 | | | | % 21.73/4.05 | | | | (62) all_45_0 = xm % 21.73/4.05 | | | | % 21.73/4.05 | | | | REDUCE: (26), (62) imply: % 22.00/4.05 | | | | (63) sdtasdt0(all_36_0, xl) = xm % 22.00/4.05 | | | | % 22.00/4.06 | | | | BETA: splitting (56) gives: % 22.00/4.06 | | | | % 22.00/4.06 | | | | Case 1: % 22.00/4.06 | | | | | % 22.00/4.06 | | | | | (64) ~ (all_47_3 = 0) % 22.00/4.06 | | | | | % 22.00/4.06 | | | | | REDUCE: (40), (64) imply: % 22.00/4.06 | | | | | (65) $false % 22.00/4.06 | | | | | % 22.00/4.06 | | | | | CLOSE: (65) is inconsistent. % 22.00/4.06 | | | | | % 22.00/4.06 | | | | Case 2: % 22.00/4.06 | | | | | % 22.00/4.06 | | | | | (66) ~ (all_47_4 = 0) | all_47_0 = xn % 22.00/4.06 | | | | | % 22.00/4.06 | | | | | BETA: splitting (66) gives: % 22.00/4.06 | | | | | % 22.00/4.06 | | | | | Case 1: % 22.00/4.06 | | | | | | % 22.00/4.06 | | | | | | (67) ~ (all_47_4 = 0) % 22.00/4.06 | | | | | | % 22.00/4.06 | | | | | | REDUCE: (36), (67) imply: % 22.00/4.06 | | | | | | (68) $false % 22.00/4.06 | | | | | | % 22.00/4.06 | | | | | | CLOSE: (68) is inconsistent. % 22.00/4.06 | | | | | | % 22.00/4.06 | | | | | Case 2: % 22.00/4.06 | | | | | | % 22.00/4.06 | | | | | | (69) all_47_0 = xn % 22.00/4.06 | | | | | | % 22.00/4.06 | | | | | | REDUCE: (33), (69) imply: % 22.00/4.06 | | | | | | (70) sdtasdt0(xl, all_47_1) = xn % 22.00/4.06 | | | | | | % 22.00/4.06 | | | | | | GROUND_INST: instantiating (7) with all_47_1, simplifying with (29), % 22.00/4.06 | | | | | | (70) gives: % 22.00/4.06 | | | | | | (71) ? [v0: int] : ( ~ (v0 = 0) & aNaturalNumber0(all_47_1) = % 22.00/4.06 | | | | | | v0) % 22.00/4.06 | | | | | | % 22.00/4.06 | | | | | | GROUND_INST: instantiating (mMulComm) with xl, all_47_1, xn, % 22.00/4.06 | | | | | | simplifying with (2), (29), (70) gives: % 22.00/4.06 | | | | | | (72) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 22.00/4.06 | | | | | | (sdtasdt0(all_47_1, xl) = v2 & aNaturalNumber0(all_47_1) = % 22.00/4.06 | | | | | | v1 & aNaturalNumber0(xl) = v0 & $i(v2) & ( ~ (v1 = 0) | ~ % 22.00/4.06 | | | | | | (v0 = 0) | v2 = xn)) % 22.00/4.06 | | | | | | % 22.00/4.06 | | | | | | GROUND_INST: instantiating (mSortsB_02) with xl, all_47_1, xn, % 22.00/4.06 | | | | | | simplifying with (2), (29), (70) gives: % 22.00/4.07 | | | | | | (73) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 22.00/4.07 | | | | | | (aNaturalNumber0(all_47_1) = v1 & aNaturalNumber0(xn) = v2 & % 22.00/4.07 | | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 % 22.00/4.07 | | | | | | = 0)) % 22.00/4.07 | | | | | | % 22.00/4.07 | | | | | | GROUND_INST: instantiating (mMulAsso) with xl, all_81_0, all_34_0, % 22.00/4.07 | | | | | | xm, xn, simplifying with (2), (11), (13), (58), (59) % 22.00/4.07 | | | | | | gives: % 22.00/4.07 | | | | | | (74) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : % 22.00/4.07 | | | | | | ? [v4: $i] : (sdtasdt0(all_81_0, all_34_0) = v3 & % 22.00/4.07 | | | | | | sdtasdt0(xl, v3) = v4 & aNaturalNumber0(all_81_0) = v1 & % 22.00/4.07 | | | | | | aNaturalNumber0(all_34_0) = v2 & aNaturalNumber0(xl) = v0 % 22.00/4.07 | | | | | | & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = % 22.00/4.07 | | | | | | 0) | v4 = xn)) % 22.00/4.07 | | | | | | % 22.00/4.07 | | | | | | GROUND_INST: instantiating (mMulAsso) with xl, all_36_0, all_72_0, % 22.00/4.07 | | | | | | xm, xn, simplifying with (2), (15), (17), (52), (53) % 22.00/4.07 | | | | | | gives: % 22.00/4.07 | | | | | | (75) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : % 22.00/4.07 | | | | | | ? [v4: $i] : (sdtasdt0(all_36_0, all_72_0) = v3 & % 22.00/4.07 | | | | | | sdtasdt0(xl, v3) = v4 & aNaturalNumber0(all_72_0) = v2 & % 22.00/4.07 | | | | | | aNaturalNumber0(all_36_0) = v1 & aNaturalNumber0(xl) = v0 % 22.00/4.08 | | | | | | & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = % 22.00/4.08 | | | | | | 0) | v4 = xn)) % 22.00/4.08 | | | | | | % 22.00/4.08 | | | | | | GROUND_INST: instantiating (mMulAsso) with all_36_0, xl, all_34_0, % 22.00/4.08 | | | | | | xm, xn, simplifying with (2), (11), (13), (15), (63) % 22.00/4.08 | | | | | | gives: % 22.00/4.08 | | | | | | (76) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : % 22.00/4.08 | | | | | | ? [v4: $i] : (sdtasdt0(all_36_0, v3) = v4 & sdtasdt0(xl, % 22.00/4.08 | | | | | | all_34_0) = v3 & aNaturalNumber0(all_36_0) = v0 & % 22.00/4.08 | | | | | | aNaturalNumber0(all_34_0) = v2 & aNaturalNumber0(xl) = v1 % 22.00/4.08 | | | | | | & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = % 22.00/4.08 | | | | | | 0) | v4 = xn)) % 22.00/4.08 | | | | | | % 22.00/4.08 | | | | | | GROUND_INST: instantiating (mMulAsso) with all_36_0, xl, all_72_0, % 22.00/4.08 | | | | | | xm, xn, simplifying with (2), (15), (52), (53), (63) % 22.00/4.08 | | | | | | gives: % 22.00/4.08 | | | | | | (77) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : % 22.00/4.08 | | | | | | ? [v4: $i] : (sdtasdt0(all_36_0, v3) = v4 & sdtasdt0(xl, % 22.00/4.08 | | | | | | all_72_0) = v3 & aNaturalNumber0(all_72_0) = v2 & % 22.00/4.08 | | | | | | aNaturalNumber0(all_36_0) = v0 & aNaturalNumber0(xl) = v1 % 22.00/4.08 | | | | | | & $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = % 22.00/4.08 | | | | | | 0) | v4 = xn)) % 22.00/4.08 | | | | | | % 22.00/4.08 | | | | | | GROUND_INST: instantiating (mMulComm) with all_36_0, all_34_0, % 22.00/4.08 | | | | | | all_47_1, simplifying with (11), (15), (34) gives: % 22.00/4.08 | | | | | | (78) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 22.00/4.08 | | | | | | (sdtasdt0(all_34_0, all_36_0) = v2 & % 22.00/4.08 | | | | | | aNaturalNumber0(all_36_0) = v0 & aNaturalNumber0(all_34_0) % 22.00/4.08 | | | | | | = v1 & $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = % 22.00/4.09 | | | | | | all_47_1)) % 22.00/4.09 | | | | | | % 22.00/4.09 | | | | | | GROUND_INST: instantiating (mSortsB_02) with all_36_0, all_34_0, % 22.00/4.09 | | | | | | all_47_1, simplifying with (11), (15), (34) gives: % 22.00/4.09 | | | | | | (79) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 22.00/4.09 | | | | | | (aNaturalNumber0(all_47_1) = v2 & aNaturalNumber0(all_36_0) % 22.00/4.09 | | | | | | = v0 & aNaturalNumber0(all_34_0) = v1 & ( ~ (v1 = 0) | ~ % 22.00/4.09 | | | | | | (v0 = 0) | v2 = 0)) % 22.00/4.09 | | | | | | % 22.00/4.09 | | | | | | DELTA: instantiating (71) with fresh symbol all_104_0 gives: % 22.00/4.09 | | | | | | (80) ~ (all_104_0 = 0) & aNaturalNumber0(all_47_1) = all_104_0 % 22.00/4.09 | | | | | | % 22.00/4.09 | | | | | | ALPHA: (80) implies: % 22.00/4.09 | | | | | | (81) ~ (all_104_0 = 0) % 22.00/4.09 | | | | | | (82) aNaturalNumber0(all_47_1) = all_104_0 % 22.00/4.09 | | | | | | % 22.00/4.09 | | | | | | DELTA: instantiating (79) with fresh symbols all_106_0, all_106_1, % 22.00/4.09 | | | | | | all_106_2 gives: % 22.00/4.09 | | | | | | (83) aNaturalNumber0(all_47_1) = all_106_0 & % 22.00/4.09 | | | | | | aNaturalNumber0(all_36_0) = all_106_2 & % 22.00/4.09 | | | | | | aNaturalNumber0(all_34_0) = all_106_1 & ( ~ (all_106_1 = 0) % 22.00/4.09 | | | | | | | ~ (all_106_2 = 0) | all_106_0 = 0) % 22.00/4.09 | | | | | | % 22.00/4.09 | | | | | | ALPHA: (83) implies: % 22.00/4.09 | | | | | | (84) aNaturalNumber0(all_34_0) = all_106_1 % 22.00/4.09 | | | | | | (85) aNaturalNumber0(all_36_0) = all_106_2 % 22.00/4.09 | | | | | | (86) aNaturalNumber0(all_47_1) = all_106_0 % 22.00/4.09 | | | | | | (87) ~ (all_106_1 = 0) | ~ (all_106_2 = 0) | all_106_0 = 0 % 22.00/4.09 | | | | | | % 22.00/4.09 | | | | | | DELTA: instantiating (73) with fresh symbols all_108_0, all_108_1, % 22.00/4.09 | | | | | | all_108_2 gives: % 22.00/4.09 | | | | | | (88) aNaturalNumber0(all_47_1) = all_108_1 & aNaturalNumber0(xn) % 22.00/4.09 | | | | | | = all_108_0 & aNaturalNumber0(xl) = all_108_2 & ( ~ % 22.00/4.09 | | | | | | (all_108_1 = 0) | ~ (all_108_2 = 0) | all_108_0 = 0) % 22.00/4.09 | | | | | | % 22.00/4.09 | | | | | | ALPHA: (88) implies: % 22.00/4.09 | | | | | | (89) aNaturalNumber0(all_47_1) = all_108_1 % 22.00/4.09 | | | | | | % 22.00/4.09 | | | | | | DELTA: instantiating (72) with fresh symbols all_110_0, all_110_1, % 22.00/4.09 | | | | | | all_110_2 gives: % 22.00/4.09 | | | | | | (90) sdtasdt0(all_47_1, xl) = all_110_0 & % 22.00/4.09 | | | | | | aNaturalNumber0(all_47_1) = all_110_1 & aNaturalNumber0(xl) % 22.00/4.09 | | | | | | = all_110_2 & $i(all_110_0) & ( ~ (all_110_1 = 0) | ~ % 22.00/4.09 | | | | | | (all_110_2 = 0) | all_110_0 = xn) % 22.00/4.09 | | | | | | % 22.00/4.09 | | | | | | ALPHA: (90) implies: % 22.00/4.09 | | | | | | (91) aNaturalNumber0(all_47_1) = all_110_1 % 22.00/4.09 | | | | | | % 22.00/4.09 | | | | | | DELTA: instantiating (78) with fresh symbols all_112_0, all_112_1, % 22.00/4.09 | | | | | | all_112_2 gives: % 22.00/4.10 | | | | | | (92) sdtasdt0(all_34_0, all_36_0) = all_112_0 & % 22.00/4.10 | | | | | | aNaturalNumber0(all_36_0) = all_112_2 & % 22.00/4.10 | | | | | | aNaturalNumber0(all_34_0) = all_112_1 & $i(all_112_0) & ( ~ % 22.00/4.10 | | | | | | (all_112_1 = 0) | ~ (all_112_2 = 0) | all_112_0 = % 22.00/4.10 | | | | | | all_47_1) % 22.00/4.10 | | | | | | % 22.00/4.10 | | | | | | ALPHA: (92) implies: % 22.00/4.10 | | | | | | (93) aNaturalNumber0(all_34_0) = all_112_1 % 22.00/4.10 | | | | | | (94) aNaturalNumber0(all_36_0) = all_112_2 % 22.00/4.10 | | | | | | % 22.00/4.10 | | | | | | DELTA: instantiating (77) with fresh symbols all_120_0, all_120_1, % 22.00/4.10 | | | | | | all_120_2, all_120_3, all_120_4 gives: % 22.00/4.10 | | | | | | (95) sdtasdt0(all_36_0, all_120_1) = all_120_0 & sdtasdt0(xl, % 22.00/4.10 | | | | | | all_72_0) = all_120_1 & aNaturalNumber0(all_72_0) = % 22.00/4.10 | | | | | | all_120_2 & aNaturalNumber0(all_36_0) = all_120_4 & % 22.00/4.10 | | | | | | aNaturalNumber0(xl) = all_120_3 & $i(all_120_0) & % 22.00/4.10 | | | | | | $i(all_120_1) & ( ~ (all_120_2 = 0) | ~ (all_120_3 = 0) | % 22.00/4.10 | | | | | | ~ (all_120_4 = 0) | all_120_0 = xn) % 22.00/4.10 | | | | | | % 22.00/4.10 | | | | | | ALPHA: (95) implies: % 22.00/4.10 | | | | | | (96) aNaturalNumber0(all_36_0) = all_120_4 % 22.00/4.10 | | | | | | % 22.00/4.10 | | | | | | DELTA: instantiating (76) with fresh symbols all_122_0, all_122_1, % 22.00/4.10 | | | | | | all_122_2, all_122_3, all_122_4 gives: % 22.00/4.10 | | | | | | (97) sdtasdt0(all_36_0, all_122_1) = all_122_0 & sdtasdt0(xl, % 22.00/4.10 | | | | | | all_34_0) = all_122_1 & aNaturalNumber0(all_36_0) = % 22.00/4.10 | | | | | | all_122_4 & aNaturalNumber0(all_34_0) = all_122_2 & % 22.00/4.10 | | | | | | aNaturalNumber0(xl) = all_122_3 & $i(all_122_0) & % 22.00/4.10 | | | | | | $i(all_122_1) & ( ~ (all_122_2 = 0) | ~ (all_122_3 = 0) | % 22.00/4.10 | | | | | | ~ (all_122_4 = 0) | all_122_0 = xn) % 22.00/4.10 | | | | | | % 22.00/4.10 | | | | | | ALPHA: (97) implies: % 22.00/4.10 | | | | | | (98) aNaturalNumber0(all_34_0) = all_122_2 % 22.00/4.10 | | | | | | (99) aNaturalNumber0(all_36_0) = all_122_4 % 22.00/4.10 | | | | | | % 22.00/4.10 | | | | | | DELTA: instantiating (75) with fresh symbols all_124_0, all_124_1, % 22.00/4.10 | | | | | | all_124_2, all_124_3, all_124_4 gives: % 22.00/4.10 | | | | | | (100) sdtasdt0(all_36_0, all_72_0) = all_124_1 & sdtasdt0(xl, % 22.00/4.10 | | | | | | all_124_1) = all_124_0 & aNaturalNumber0(all_72_0) = % 22.00/4.10 | | | | | | all_124_2 & aNaturalNumber0(all_36_0) = all_124_3 & % 22.00/4.10 | | | | | | aNaturalNumber0(xl) = all_124_4 & $i(all_124_0) & % 22.00/4.10 | | | | | | $i(all_124_1) & ( ~ (all_124_2 = 0) | ~ (all_124_3 = 0) | % 22.00/4.10 | | | | | | ~ (all_124_4 = 0) | all_124_0 = xn) % 22.00/4.10 | | | | | | % 22.00/4.10 | | | | | | ALPHA: (100) implies: % 22.00/4.10 | | | | | | (101) aNaturalNumber0(all_36_0) = all_124_3 % 22.00/4.10 | | | | | | % 22.00/4.10 | | | | | | DELTA: instantiating (74) with fresh symbols all_126_0, all_126_1, % 22.00/4.10 | | | | | | all_126_2, all_126_3, all_126_4 gives: % 22.00/4.10 | | | | | | (102) sdtasdt0(all_81_0, all_34_0) = all_126_1 & sdtasdt0(xl, % 22.00/4.10 | | | | | | all_126_1) = all_126_0 & aNaturalNumber0(all_81_0) = % 22.00/4.10 | | | | | | all_126_3 & aNaturalNumber0(all_34_0) = all_126_2 & % 22.00/4.10 | | | | | | aNaturalNumber0(xl) = all_126_4 & $i(all_126_0) & % 22.00/4.10 | | | | | | $i(all_126_1) & ( ~ (all_126_2 = 0) | ~ (all_126_3 = 0) | % 22.00/4.10 | | | | | | ~ (all_126_4 = 0) | all_126_0 = xn) % 22.00/4.10 | | | | | | % 22.00/4.10 | | | | | | ALPHA: (102) implies: % 22.00/4.11 | | | | | | (103) aNaturalNumber0(all_34_0) = all_126_2 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | GROUND_INST: instantiating (5) with 0, all_112_1, all_34_0, % 22.00/4.11 | | | | | | simplifying with (12), (93) gives: % 22.00/4.11 | | | | | | (104) all_112_1 = 0 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | GROUND_INST: instantiating (5) with all_112_1, all_122_2, all_34_0, % 22.00/4.11 | | | | | | simplifying with (93), (98) gives: % 22.00/4.11 | | | | | | (105) all_122_2 = all_112_1 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | GROUND_INST: instantiating (5) with all_122_2, all_126_2, all_34_0, % 22.00/4.11 | | | | | | simplifying with (98), (103) gives: % 22.00/4.11 | | | | | | (106) all_126_2 = all_122_2 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | GROUND_INST: instantiating (5) with all_106_1, all_126_2, all_34_0, % 22.00/4.11 | | | | | | simplifying with (84), (103) gives: % 22.00/4.11 | | | | | | (107) all_126_2 = all_106_1 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | GROUND_INST: instantiating (5) with all_112_2, all_120_4, all_36_0, % 22.00/4.11 | | | | | | simplifying with (94), (96) gives: % 22.00/4.11 | | | | | | (108) all_120_4 = all_112_2 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | GROUND_INST: instantiating (5) with all_120_4, all_122_4, all_36_0, % 22.00/4.11 | | | | | | simplifying with (96), (99) gives: % 22.00/4.11 | | | | | | (109) all_122_4 = all_120_4 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | GROUND_INST: instantiating (5) with all_106_2, all_122_4, all_36_0, % 22.00/4.11 | | | | | | simplifying with (85), (99) gives: % 22.00/4.11 | | | | | | (110) all_122_4 = all_106_2 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | GROUND_INST: instantiating (5) with 0, all_124_3, all_36_0, % 22.00/4.11 | | | | | | simplifying with (16), (101) gives: % 22.00/4.11 | | | | | | (111) all_124_3 = 0 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | GROUND_INST: instantiating (5) with all_112_2, all_124_3, all_36_0, % 22.00/4.11 | | | | | | simplifying with (94), (101) gives: % 22.00/4.11 | | | | | | (112) all_124_3 = all_112_2 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | GROUND_INST: instantiating (5) with all_106_0, all_108_1, all_47_1, % 22.00/4.11 | | | | | | simplifying with (86), (89) gives: % 22.00/4.11 | | | | | | (113) all_108_1 = all_106_0 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | GROUND_INST: instantiating (5) with all_108_1, all_110_1, all_47_1, % 22.00/4.11 | | | | | | simplifying with (89), (91) gives: % 22.00/4.11 | | | | | | (114) all_110_1 = all_108_1 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | GROUND_INST: instantiating (5) with all_104_0, all_110_1, all_47_1, % 22.00/4.11 | | | | | | simplifying with (82), (91) gives: % 22.00/4.11 | | | | | | (115) all_110_1 = all_104_0 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | COMBINE_EQS: (106), (107) imply: % 22.00/4.11 | | | | | | (116) all_122_2 = all_106_1 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | SIMP: (116) implies: % 22.00/4.11 | | | | | | (117) all_122_2 = all_106_1 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | COMBINE_EQS: (111), (112) imply: % 22.00/4.11 | | | | | | (118) all_112_2 = 0 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | SIMP: (118) implies: % 22.00/4.11 | | | | | | (119) all_112_2 = 0 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | COMBINE_EQS: (105), (117) imply: % 22.00/4.11 | | | | | | (120) all_112_1 = all_106_1 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | SIMP: (120) implies: % 22.00/4.11 | | | | | | (121) all_112_1 = all_106_1 % 22.00/4.11 | | | | | | % 22.00/4.11 | | | | | | COMBINE_EQS: (109), (110) imply: % 22.00/4.12 | | | | | | (122) all_120_4 = all_106_2 % 22.00/4.12 | | | | | | % 22.00/4.12 | | | | | | SIMP: (122) implies: % 22.00/4.12 | | | | | | (123) all_120_4 = all_106_2 % 22.00/4.12 | | | | | | % 22.00/4.12 | | | | | | COMBINE_EQS: (108), (123) imply: % 22.00/4.12 | | | | | | (124) all_112_2 = all_106_2 % 22.00/4.12 | | | | | | % 22.00/4.12 | | | | | | SIMP: (124) implies: % 22.00/4.12 | | | | | | (125) all_112_2 = all_106_2 % 22.00/4.12 | | | | | | % 22.00/4.12 | | | | | | COMBINE_EQS: (104), (121) imply: % 22.00/4.12 | | | | | | (126) all_106_1 = 0 % 22.00/4.12 | | | | | | % 22.00/4.12 | | | | | | SIMP: (126) implies: % 22.00/4.12 | | | | | | (127) all_106_1 = 0 % 22.00/4.12 | | | | | | % 22.00/4.12 | | | | | | COMBINE_EQS: (119), (125) imply: % 22.00/4.12 | | | | | | (128) all_106_2 = 0 % 22.00/4.12 | | | | | | % 22.00/4.12 | | | | | | COMBINE_EQS: (114), (115) imply: % 22.00/4.12 | | | | | | (129) all_108_1 = all_104_0 % 22.00/4.12 | | | | | | % 22.00/4.12 | | | | | | SIMP: (129) implies: % 22.00/4.12 | | | | | | (130) all_108_1 = all_104_0 % 22.00/4.12 | | | | | | % 22.00/4.12 | | | | | | COMBINE_EQS: (113), (130) imply: % 22.00/4.12 | | | | | | (131) all_106_0 = all_104_0 % 22.00/4.12 | | | | | | % 22.00/4.12 | | | | | | SIMP: (131) implies: % 22.00/4.12 | | | | | | (132) all_106_0 = all_104_0 % 22.00/4.12 | | | | | | % 22.00/4.12 | | | | | | BETA: splitting (87) gives: % 22.00/4.12 | | | | | | % 22.00/4.12 | | | | | | Case 1: % 22.00/4.12 | | | | | | | % 22.00/4.12 | | | | | | | (133) ~ (all_106_1 = 0) % 22.00/4.12 | | | | | | | % 22.00/4.12 | | | | | | | REDUCE: (127), (133) imply: % 22.00/4.12 | | | | | | | (134) $false % 22.00/4.12 | | | | | | | % 22.00/4.12 | | | | | | | CLOSE: (134) is inconsistent. % 22.00/4.12 | | | | | | | % 22.00/4.12 | | | | | | Case 2: % 22.00/4.12 | | | | | | | % 22.00/4.12 | | | | | | | (135) ~ (all_106_2 = 0) | all_106_0 = 0 % 22.00/4.12 | | | | | | | % 22.00/4.12 | | | | | | | BETA: splitting (135) gives: % 22.00/4.12 | | | | | | | % 22.00/4.12 | | | | | | | Case 1: % 22.00/4.12 | | | | | | | | % 22.00/4.12 | | | | | | | | (136) ~ (all_106_2 = 0) % 22.00/4.12 | | | | | | | | % 22.00/4.12 | | | | | | | | REDUCE: (128), (136) imply: % 22.00/4.12 | | | | | | | | (137) $false % 22.00/4.12 | | | | | | | | % 22.00/4.12 | | | | | | | | CLOSE: (137) is inconsistent. % 22.00/4.12 | | | | | | | | % 22.00/4.12 | | | | | | | Case 2: % 22.00/4.12 | | | | | | | | % 22.00/4.12 | | | | | | | | (138) all_106_0 = 0 % 22.00/4.12 | | | | | | | | % 22.00/4.12 | | | | | | | | COMBINE_EQS: (132), (138) imply: % 22.00/4.12 | | | | | | | | (139) all_104_0 = 0 % 22.00/4.12 | | | | | | | | % 22.00/4.12 | | | | | | | | SIMP: (139) implies: % 22.00/4.12 | | | | | | | | (140) all_104_0 = 0 % 22.00/4.12 | | | | | | | | % 22.00/4.12 | | | | | | | | REDUCE: (81), (140) imply: % 22.00/4.12 | | | | | | | | (141) $false % 22.00/4.12 | | | | | | | | % 22.00/4.12 | | | | | | | | CLOSE: (141) is inconsistent. % 22.00/4.12 | | | | | | | | % 22.00/4.12 | | | | | | | End of split % 22.00/4.12 | | | | | | | % 22.00/4.12 | | | | | | End of split % 22.00/4.12 | | | | | | % 22.00/4.12 | | | | | End of split % 22.00/4.12 | | | | | % 22.00/4.12 | | | | End of split % 22.00/4.12 | | | | % 22.00/4.12 | | | End of split % 22.00/4.12 | | | % 22.00/4.12 | | End of split % 22.00/4.12 | | % 22.00/4.12 | End of split % 22.00/4.12 | % 22.00/4.12 End of proof % 22.00/4.13 % SZS output end Proof for theBenchmark % 22.00/4.13 % 22.00/4.13 3497ms %------------------------------------------------------------------------------