%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : NUM467+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 : n012.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 10.50s 2.17s % Output : Proof 15.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.14 % Problem : NUM467+1 : TPTP v8.1.2. Released v4.0.0. % 0.00/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.15/0.36 % Computer : n012.cluster.edu % 0.15/0.36 % Model : x86_64 x86_64 % 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.36 % Memory : 8042.1875MB % 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.36 % CPULimit : 300 % 0.15/0.36 % WCLimit : 300 % 0.15/0.36 % DateTime : Fri Aug 25 14:02:56 EDT 2023 % 0.15/0.36 % CPUTime : % 0.22/0.60 ________ _____ % 0.22/0.60 ___ __ \_________(_)________________________________ % 0.22/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.22/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.22/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.22/0.60 % 0.22/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.22/0.60 (2023-06-19) % 0.22/0.60 % 0.22/0.60 (c) Philipp Rümmer, 2009-2023 % 0.22/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.22/0.60 Amanda Stjerna. % 0.22/0.60 Free software under BSD-3-Clause. % 0.22/0.60 % 0.22/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.22/0.60 % 0.22/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.22/0.61 Running up to 7 provers in parallel. % 0.22/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.22/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.22/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.22/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.22/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.22/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.22/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.81/1.14 Prover 1: Preprocessing ... % 2.81/1.14 Prover 4: Preprocessing ... % 3.44/1.17 Prover 5: Preprocessing ... % 3.44/1.17 Prover 0: Preprocessing ... % 3.44/1.17 Prover 2: Preprocessing ... % 3.44/1.17 Prover 6: Preprocessing ... % 3.44/1.17 Prover 3: Preprocessing ... % 7.72/1.77 Prover 1: Constructing countermodel ... % 7.72/1.82 Prover 3: Constructing countermodel ... % 7.72/1.82 Prover 6: Proving ... % 9.03/1.94 Prover 5: Constructing countermodel ... % 9.89/2.08 Prover 4: Constructing countermodel ... % 9.89/2.08 Prover 2: Proving ... % 10.50/2.16 Prover 3: proved (1538ms) % 10.50/2.16 % 10.50/2.17 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 10.50/2.17 % 10.50/2.17 Prover 5: stopped % 10.82/2.18 Prover 6: stopped % 10.82/2.19 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 10.82/2.19 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 10.82/2.19 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 10.82/2.20 Prover 0: Proving ... % 10.82/2.20 Prover 0: stopped % 10.82/2.21 Prover 2: stopped % 10.82/2.22 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 10.82/2.22 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 10.82/2.28 Prover 8: Preprocessing ... % 10.82/2.28 Prover 7: Preprocessing ... % 10.82/2.32 Prover 11: Preprocessing ... % 10.82/2.32 Prover 13: Preprocessing ... % 10.82/2.34 Prover 10: Preprocessing ... % 12.41/2.42 Prover 8: Warning: ignoring some quantifiers % 12.41/2.42 Prover 8: Constructing countermodel ... % 12.88/2.49 Prover 10: Constructing countermodel ... % 12.88/2.55 Prover 7: Constructing countermodel ... % 13.73/2.59 Prover 13: Constructing countermodel ... % 15.09/2.78 Prover 11: Constructing countermodel ... % 15.09/2.85 Prover 1: Found proof (size 249) % 15.09/2.85 Prover 1: proved (2230ms) % 15.09/2.85 Prover 13: stopped % 15.09/2.85 Prover 11: stopped % 15.09/2.85 Prover 7: stopped % 15.09/2.85 Prover 8: stopped % 15.09/2.85 Prover 10: stopped % 15.09/2.85 Prover 4: stopped % 15.70/2.86 % 15.70/2.86 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 15.70/2.86 % 15.84/2.89 % SZS output start Proof for theBenchmark % 15.84/2.89 Assumptions after simplification: % 15.84/2.89 --------------------------------- % 15.84/2.89 % 15.84/2.89 (mAMDistr) % 15.84/2.92 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 15.84/2.92 $i] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ % 15.84/2.92 (sdtpldt0(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : % 15.84/2.92 ? [v7: any] : ? [v8: any] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? % 15.84/2.92 [v12: $i] : ? [v13: $i] : ? [v14: $i] : (sdtasdt0(v9, v0) = v11 & % 15.84/2.92 sdtasdt0(v2, v0) = v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v9) = v10 & % 15.84/2.92 sdtpldt0(v12, v13) = v14 & sdtpldt0(v1, v2) = v9 & aNaturalNumber0(v2) = % 15.84/2.92 v8 & aNaturalNumber0(v1) = v7 & aNaturalNumber0(v0) = v6 & $i(v14) & % 15.84/2.92 $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) & ( ~ (v8 = 0) | ~ (v7 = % 15.84/2.92 0) | ~ (v6 = 0) | (v14 = v11 & v10 = v5)))) % 15.84/2.92 % 15.84/2.92 (mAddComm) % 15.84/2.92 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 15.84/2.92 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 15.84/2.92 (sdtpldt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 % 15.84/2.92 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 15.84/2.92 % 15.84/2.92 (mDefDiv) % 15.84/2.93 ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (doDivides0(v0, v1) = v2) | ~ % 15.84/2.93 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : (aNaturalNumber0(v1) = v4 % 15.84/2.93 & aNaturalNumber0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0))) | (( ~ (v2 = 0) % 15.84/2.93 | ? [v3: $i] : (sdtasdt0(v0, v3) = v1 & aNaturalNumber0(v3) = 0 & % 15.84/2.93 $i(v3))) & (v2 = 0 | ! [v3: $i] : ( ~ (sdtasdt0(v0, v3) = v1) | ~ % 15.84/2.93 $i(v3) | ? [v4: int] : ( ~ (v4 = 0) & aNaturalNumber0(v3) = v4))))) % 15.84/2.93 % 15.84/2.93 (mDivTrans) % 15.84/2.93 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 15.84/2.93 (doDivides0(v0, v2) = v3) | ~ (doDivides0(v0, v1) = 0) | ~ $i(v2) | ~ % 15.84/2.93 $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: % 15.84/2.93 any] : (doDivides0(v1, v2) = v7 & aNaturalNumber0(v2) = v6 & % 15.84/2.93 aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v7 = 0) | ~ % 15.84/2.93 (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) % 15.84/2.93 % 15.84/2.93 (mMulComm) % 15.84/2.93 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 15.84/2.93 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 15.84/2.93 (sdtasdt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 % 15.84/2.93 & $i(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 15.84/2.93 % 15.84/2.93 (mSortsB) % 15.84/2.94 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 15.84/2.94 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 15.84/2.94 (aNaturalNumber0(v2) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = % 15.84/2.94 v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 15.84/2.94 % 15.84/2.94 (mSortsB_02) % 15.84/2.94 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 15.84/2.94 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 15.84/2.94 (aNaturalNumber0(v2) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = % 15.84/2.94 v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 15.84/2.94 % 15.84/2.94 (m__) % 15.84/2.94 $i(xn) & $i(xm) & $i(xl) & ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & % 15.84/2.94 doDivides0(xl, v0) = v1 & sdtpldt0(xm, xn) = v0 & $i(v0)) % 15.84/2.94 % 15.84/2.94 (m__1240) % 15.84/2.94 aNaturalNumber0(xn) = 0 & aNaturalNumber0(xm) = 0 & aNaturalNumber0(xl) = 0 & % 15.84/2.94 $i(xn) & $i(xm) & $i(xl) % 15.84/2.94 % 15.84/2.94 (m__1240_04) % 15.84/2.94 doDivides0(xl, xn) = 0 & doDivides0(xl, xm) = 0 & $i(xn) & $i(xm) & $i(xl) % 15.84/2.94 % 15.84/2.94 (function-axioms) % 15.84/2.95 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 15.84/2.95 (sdtsldt0(v3, v2) = v1) | ~ (sdtsldt0(v3, v2) = v0)) & ! [v0: % 15.84/2.95 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 15.84/2.95 : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ (doDivides0(v3, v2) = v0)) & ! % 15.84/2.95 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 15.84/2.95 $i] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) & ! % 15.84/2.95 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 15.84/2.95 (sdtmndt0(v3, v2) = v1) | ~ (sdtmndt0(v3, v2) = v0)) & ! [v0: % 15.84/2.95 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 15.84/2.95 : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ (sdtlseqdt0(v3, v2) = v0)) & ! % 15.84/2.95 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 15.84/2.95 (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 15.84/2.95 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | % 15.84/2.95 ~ (sdtpldt0(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 15.84/2.95 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) % 15.84/2.95 | ~ (aNaturalNumber0(v2) = v0)) % 15.84/2.95 % 15.84/2.95 Further assumptions not needed in the proof: % 15.84/2.95 -------------------------------------------- % 15.84/2.95 mAddAsso, mAddCanc, mDefDiff, mDefLE, mDefQuot, mIH, mIH_03, mLEAsym, mLENTr, % 15.84/2.95 mLERefl, mLETotal, mLETran, mMonAdd, mMonMul, mMonMul2, mMulAsso, mMulCanc, % 15.84/2.95 mNatSort, mSortsC, mSortsC_01, mZeroAdd, mZeroMul, m_AddZero, m_MulUnit, % 15.84/2.95 m_MulZero % 15.84/2.95 % 15.84/2.95 Those formulas are unsatisfiable: % 15.84/2.95 --------------------------------- % 15.84/2.95 % 15.84/2.95 Begin of proof % 15.84/2.95 | % 15.84/2.95 | ALPHA: (m__1240) implies: % 15.84/2.95 | (1) aNaturalNumber0(xl) = 0 % 15.84/2.95 | (2) aNaturalNumber0(xm) = 0 % 15.84/2.95 | (3) aNaturalNumber0(xn) = 0 % 15.84/2.95 | % 15.84/2.95 | ALPHA: (m__1240_04) implies: % 15.84/2.95 | (4) doDivides0(xl, xm) = 0 % 15.84/2.95 | (5) doDivides0(xl, xn) = 0 % 15.84/2.95 | % 15.84/2.95 | ALPHA: (m__) implies: % 15.84/2.95 | (6) $i(xl) % 15.84/2.95 | (7) $i(xm) % 15.84/2.95 | (8) $i(xn) % 15.84/2.95 | (9) ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & doDivides0(xl, v0) = v1 & % 15.84/2.95 | sdtpldt0(xm, xn) = v0 & $i(v0)) % 15.84/2.95 | % 15.84/2.95 | ALPHA: (function-axioms) implies: % 15.84/2.95 | (10) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 15.84/2.95 | : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = % 15.84/2.95 | v0)) % 15.84/2.95 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 15.84/2.95 | (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 15.84/2.95 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 15.84/2.95 | (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 15.84/2.95 | % 15.84/2.95 | DELTA: instantiating (9) with fresh symbols all_32_0, all_32_1 gives: % 15.84/2.95 | (13) ~ (all_32_0 = 0) & doDivides0(xl, all_32_1) = all_32_0 & sdtpldt0(xm, % 15.84/2.95 | xn) = all_32_1 & $i(all_32_1) % 15.84/2.95 | % 15.84/2.95 | ALPHA: (13) implies: % 15.84/2.96 | (14) ~ (all_32_0 = 0) % 15.84/2.96 | (15) $i(all_32_1) % 15.84/2.96 | (16) sdtpldt0(xm, xn) = all_32_1 % 15.84/2.96 | (17) doDivides0(xl, all_32_1) = all_32_0 % 15.84/2.96 | % 15.84/2.96 | GROUND_INST: instantiating (mAddComm) with xm, xn, all_32_1, simplifying with % 15.84/2.96 | (7), (8), (16) gives: % 15.84/2.96 | (18) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtpldt0(xn, xm) = v2 & % 15.84/2.96 | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xm) = v0 & $i(v2) & ( ~ % 15.84/2.96 | (v1 = 0) | ~ (v0 = 0) | v2 = all_32_1)) % 15.84/2.96 | % 15.84/2.96 | GROUND_INST: instantiating (mSortsB) with xm, xn, all_32_1, simplifying with % 15.84/2.96 | (7), (8), (16) gives: % 15.84/2.96 | (19) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 15.84/2.96 | (aNaturalNumber0(all_32_1) = v2 & aNaturalNumber0(xn) = v1 & % 15.84/2.96 | aNaturalNumber0(xm) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 15.84/2.96 | % 15.84/2.96 | GROUND_INST: instantiating (mDefDiv) with xl, xm, 0, simplifying with (4), % 15.84/2.96 | (6), (7) gives: % 15.84/2.96 | (20) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(xm) = v1 & % 15.84/2.96 | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) | ? [v0: % 15.84/2.96 | $i] : (sdtasdt0(xl, v0) = xm & aNaturalNumber0(v0) = 0 & $i(v0)) % 15.84/2.96 | % 15.84/2.96 | GROUND_INST: instantiating (mDefDiv) with xl, xn, 0, simplifying with (5), % 15.84/2.96 | (6), (8) gives: % 15.84/2.96 | (21) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(xn) = v1 & % 15.84/2.96 | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) | ? [v0: % 15.84/2.96 | $i] : (sdtasdt0(xl, v0) = xn & aNaturalNumber0(v0) = 0 & $i(v0)) % 15.84/2.96 | % 15.84/2.96 | GROUND_INST: instantiating (mDivTrans) with xl, xn, all_32_1, all_32_0, % 15.84/2.96 | simplifying with (5), (6), (8), (15), (17) gives: % 15.84/2.96 | (22) all_32_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: % 15.84/2.96 | any] : (doDivides0(xn, all_32_1) = v3 & aNaturalNumber0(all_32_1) = % 15.84/2.96 | v2 & aNaturalNumber0(xn) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v3 = % 15.84/2.96 | 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 15.84/2.96 | % 15.84/2.96 | GROUND_INST: instantiating (mDivTrans) with xl, xm, all_32_1, all_32_0, % 15.84/2.96 | simplifying with (4), (6), (7), (15), (17) gives: % 15.84/2.96 | (23) all_32_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: % 15.84/2.96 | any] : (doDivides0(xm, all_32_1) = v3 & aNaturalNumber0(all_32_1) = % 15.84/2.96 | v2 & aNaturalNumber0(xm) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v3 = % 15.84/2.97 | 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 15.84/2.97 | % 15.84/2.97 | GROUND_INST: instantiating (mDefDiv) with xl, all_32_1, all_32_0, simplifying % 15.84/2.97 | with (6), (15), (17) gives: % 15.84/2.97 | (24) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(all_32_1) = v1 & % 15.84/2.97 | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) | (( ~ % 15.84/2.97 | (all_32_0 = 0) | ? [v0: $i] : (sdtasdt0(xl, v0) = all_32_1 & % 15.84/2.97 | aNaturalNumber0(v0) = 0 & $i(v0))) & (all_32_0 = 0 | ! [v0: $i] % 15.84/2.97 | : ( ~ (sdtasdt0(xl, v0) = all_32_1) | ~ $i(v0) | ? [v1: int] : ( % 15.84/2.97 | ~ (v1 = 0) & aNaturalNumber0(v0) = v1)))) % 15.84/2.97 | % 15.84/2.97 | DELTA: instantiating (19) with fresh symbols all_39_0, all_39_1, all_39_2 % 15.84/2.97 | gives: % 15.84/2.97 | (25) aNaturalNumber0(all_32_1) = all_39_0 & aNaturalNumber0(xn) = all_39_1 % 15.84/2.97 | & aNaturalNumber0(xm) = all_39_2 & ( ~ (all_39_1 = 0) | ~ (all_39_2 = % 15.84/2.97 | 0) | all_39_0 = 0) % 15.84/2.97 | % 15.84/2.97 | ALPHA: (25) implies: % 15.84/2.97 | (26) aNaturalNumber0(xm) = all_39_2 % 15.84/2.97 | (27) aNaturalNumber0(xn) = all_39_1 % 15.84/2.97 | (28) aNaturalNumber0(all_32_1) = all_39_0 % 15.84/2.97 | (29) ~ (all_39_1 = 0) | ~ (all_39_2 = 0) | all_39_0 = 0 % 15.84/2.97 | % 15.84/2.97 | DELTA: instantiating (18) with fresh symbols all_41_0, all_41_1, all_41_2 % 15.84/2.97 | gives: % 15.84/2.97 | (30) sdtpldt0(xn, xm) = all_41_0 & aNaturalNumber0(xn) = all_41_1 & % 15.84/2.97 | aNaturalNumber0(xm) = all_41_2 & $i(all_41_0) & ( ~ (all_41_1 = 0) | % 15.84/2.97 | ~ (all_41_2 = 0) | all_41_0 = all_32_1) % 15.84/2.97 | % 15.84/2.97 | ALPHA: (30) implies: % 15.84/2.97 | (31) aNaturalNumber0(xm) = all_41_2 % 15.84/2.97 | (32) aNaturalNumber0(xn) = all_41_1 % 15.84/2.97 | (33) sdtpldt0(xn, xm) = all_41_0 % 15.84/2.97 | (34) ~ (all_41_1 = 0) | ~ (all_41_2 = 0) | all_41_0 = all_32_1 % 15.84/2.97 | % 15.84/2.97 | BETA: splitting (23) gives: % 15.84/2.97 | % 15.84/2.97 | Case 1: % 15.84/2.97 | | % 15.84/2.97 | | (35) all_32_0 = 0 % 15.84/2.97 | | % 15.84/2.97 | | REDUCE: (14), (35) imply: % 15.84/2.97 | | (36) $false % 15.84/2.97 | | % 15.84/2.97 | | CLOSE: (36) is inconsistent. % 15.84/2.97 | | % 15.84/2.97 | Case 2: % 15.84/2.97 | | % 15.84/2.97 | | (37) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 15.84/2.97 | | (doDivides0(xm, all_32_1) = v3 & aNaturalNumber0(all_32_1) = v2 & % 15.84/2.97 | | aNaturalNumber0(xm) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v3 = 0) % 15.84/2.97 | | | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 15.84/2.97 | | % 15.84/2.97 | | DELTA: instantiating (37) with fresh symbols all_51_0, all_51_1, all_51_2, % 15.84/2.97 | | all_51_3 gives: % 15.84/2.97 | | (38) doDivides0(xm, all_32_1) = all_51_0 & aNaturalNumber0(all_32_1) = % 15.84/2.97 | | all_51_1 & aNaturalNumber0(xm) = all_51_2 & aNaturalNumber0(xl) = % 15.84/2.97 | | all_51_3 & ( ~ (all_51_0 = 0) | ~ (all_51_1 = 0) | ~ (all_51_2 = % 15.84/2.97 | | 0) | ~ (all_51_3 = 0)) % 15.84/2.97 | | % 15.84/2.97 | | ALPHA: (38) implies: % 15.84/2.97 | | (39) aNaturalNumber0(xl) = all_51_3 % 15.84/2.97 | | (40) aNaturalNumber0(xm) = all_51_2 % 15.84/2.97 | | (41) aNaturalNumber0(all_32_1) = all_51_1 % 15.84/2.97 | | % 15.84/2.97 | | BETA: splitting (22) gives: % 15.84/2.97 | | % 15.84/2.97 | | Case 1: % 15.84/2.97 | | | % 15.84/2.98 | | | (42) all_32_0 = 0 % 15.84/2.98 | | | % 15.84/2.98 | | | REDUCE: (14), (42) imply: % 15.84/2.98 | | | (43) $false % 15.84/2.98 | | | % 15.84/2.98 | | | CLOSE: (43) is inconsistent. % 15.84/2.98 | | | % 15.84/2.98 | | Case 2: % 15.84/2.98 | | | % 15.84/2.98 | | | (44) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 15.84/2.98 | | | (doDivides0(xn, all_32_1) = v3 & aNaturalNumber0(all_32_1) = v2 & % 15.84/2.98 | | | aNaturalNumber0(xn) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v3 = % 15.84/2.98 | | | 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 15.84/2.98 | | | % 15.84/2.98 | | | DELTA: instantiating (44) with fresh symbols all_56_0, all_56_1, all_56_2, % 15.84/2.98 | | | all_56_3 gives: % 15.84/2.98 | | | (45) doDivides0(xn, all_32_1) = all_56_0 & aNaturalNumber0(all_32_1) = % 15.84/2.98 | | | all_56_1 & aNaturalNumber0(xn) = all_56_2 & aNaturalNumber0(xl) = % 15.84/2.98 | | | all_56_3 & ( ~ (all_56_0 = 0) | ~ (all_56_1 = 0) | ~ (all_56_2 = % 15.84/2.98 | | | 0) | ~ (all_56_3 = 0)) % 15.84/2.98 | | | % 15.84/2.98 | | | ALPHA: (45) implies: % 15.84/2.98 | | | (46) aNaturalNumber0(xl) = all_56_3 % 15.84/2.98 | | | (47) aNaturalNumber0(xn) = all_56_2 % 15.84/2.98 | | | (48) aNaturalNumber0(all_32_1) = all_56_1 % 15.84/2.98 | | | % 15.84/2.98 | | | GROUND_INST: instantiating (10) with 0, all_56_3, xl, simplifying with % 15.84/2.98 | | | (1), (46) gives: % 15.84/2.98 | | | (49) all_56_3 = 0 % 15.84/2.98 | | | % 15.84/2.98 | | | GROUND_INST: instantiating (10) with all_51_3, all_56_3, xl, simplifying % 15.84/2.98 | | | with (39), (46) gives: % 15.84/2.98 | | | (50) all_56_3 = all_51_3 % 15.84/2.98 | | | % 15.84/2.98 | | | GROUND_INST: instantiating (10) with 0, all_51_2, xm, simplifying with % 15.84/2.98 | | | (2), (40) gives: % 15.84/2.98 | | | (51) all_51_2 = 0 % 15.84/2.98 | | | % 15.84/2.98 | | | GROUND_INST: instantiating (10) with all_41_2, all_51_2, xm, simplifying % 15.84/2.98 | | | with (31), (40) gives: % 15.84/2.98 | | | (52) all_51_2 = all_41_2 % 15.84/2.98 | | | % 15.84/2.98 | | | GROUND_INST: instantiating (10) with all_39_2, all_51_2, xm, simplifying % 15.84/2.98 | | | with (26), (40) gives: % 15.84/2.98 | | | (53) all_51_2 = all_39_2 % 15.84/2.98 | | | % 15.84/2.98 | | | GROUND_INST: instantiating (10) with all_39_1, all_41_1, xn, simplifying % 15.84/2.98 | | | with (27), (32) gives: % 15.84/2.98 | | | (54) all_41_1 = all_39_1 % 15.84/2.98 | | | % 15.84/2.98 | | | GROUND_INST: instantiating (10) with 0, all_56_2, xn, simplifying with % 15.84/2.98 | | | (3), (47) gives: % 15.84/2.98 | | | (55) all_56_2 = 0 % 15.84/2.98 | | | % 15.84/2.98 | | | GROUND_INST: instantiating (10) with all_41_1, all_56_2, xn, simplifying % 15.84/2.98 | | | with (32), (47) gives: % 15.84/2.98 | | | (56) all_56_2 = all_41_1 % 15.84/2.98 | | | % 15.84/2.98 | | | GROUND_INST: instantiating (10) with all_51_1, all_56_1, all_32_1, % 15.84/2.98 | | | simplifying with (41), (48) gives: % 15.84/2.98 | | | (57) all_56_1 = all_51_1 % 15.84/2.98 | | | % 15.84/2.98 | | | GROUND_INST: instantiating (10) with all_39_0, all_56_1, all_32_1, % 15.84/2.98 | | | simplifying with (28), (48) gives: % 15.84/2.98 | | | (58) all_56_1 = all_39_0 % 15.84/2.98 | | | % 15.84/2.98 | | | COMBINE_EQS: (57), (58) imply: % 15.84/2.98 | | | (59) all_51_1 = all_39_0 % 15.84/2.98 | | | % 15.84/2.98 | | | SIMP: (59) implies: % 15.84/2.98 | | | (60) all_51_1 = all_39_0 % 15.84/2.98 | | | % 15.84/2.98 | | | COMBINE_EQS: (55), (56) imply: % 15.84/2.98 | | | (61) all_41_1 = 0 % 15.84/2.98 | | | % 15.84/2.98 | | | SIMP: (61) implies: % 15.84/2.98 | | | (62) all_41_1 = 0 % 15.84/2.98 | | | % 15.84/2.98 | | | COMBINE_EQS: (49), (50) imply: % 15.84/2.98 | | | (63) all_51_3 = 0 % 15.84/2.98 | | | % 15.84/2.98 | | | COMBINE_EQS: (52), (53) imply: % 15.84/2.98 | | | (64) all_41_2 = all_39_2 % 15.84/2.98 | | | % 15.84/2.98 | | | COMBINE_EQS: (51), (52) imply: % 15.84/2.98 | | | (65) all_41_2 = 0 % 15.84/2.98 | | | % 15.84/2.98 | | | COMBINE_EQS: (54), (62) imply: % 15.84/2.98 | | | (66) all_39_1 = 0 % 15.84/2.98 | | | % 15.84/2.98 | | | SIMP: (66) implies: % 15.84/2.98 | | | (67) all_39_1 = 0 % 15.84/2.98 | | | % 15.84/2.98 | | | COMBINE_EQS: (64), (65) imply: % 15.84/2.98 | | | (68) all_39_2 = 0 % 15.84/2.98 | | | % 15.84/2.98 | | | SIMP: (68) implies: % 15.84/2.98 | | | (69) all_39_2 = 0 % 15.84/2.98 | | | % 15.84/2.98 | | | BETA: splitting (29) gives: % 15.84/2.98 | | | % 15.84/2.98 | | | Case 1: % 15.84/2.98 | | | | % 15.84/2.98 | | | | (70) ~ (all_39_1 = 0) % 15.84/2.98 | | | | % 15.84/2.98 | | | | REDUCE: (67), (70) imply: % 15.84/2.98 | | | | (71) $false % 15.84/2.98 | | | | % 15.84/2.98 | | | | CLOSE: (71) is inconsistent. % 15.84/2.98 | | | | % 15.84/2.98 | | | Case 2: % 15.84/2.98 | | | | % 15.84/2.99 | | | | (72) ~ (all_39_2 = 0) | all_39_0 = 0 % 15.84/2.99 | | | | % 15.84/2.99 | | | | BETA: splitting (21) gives: % 15.84/2.99 | | | | % 15.84/2.99 | | | | Case 1: % 15.84/2.99 | | | | | % 15.84/2.99 | | | | | (73) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(xn) = v1 & % 15.84/2.99 | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 15.84/2.99 | | | | | % 15.84/2.99 | | | | | DELTA: instantiating (73) with fresh symbols all_68_0, all_68_1 gives: % 15.84/2.99 | | | | | (74) aNaturalNumber0(xn) = all_68_0 & aNaturalNumber0(xl) = % 15.84/2.99 | | | | | all_68_1 & ( ~ (all_68_0 = 0) | ~ (all_68_1 = 0)) % 15.84/2.99 | | | | | % 15.84/2.99 | | | | | ALPHA: (74) implies: % 15.84/2.99 | | | | | (75) aNaturalNumber0(xl) = all_68_1 % 15.84/2.99 | | | | | (76) aNaturalNumber0(xn) = all_68_0 % 15.84/2.99 | | | | | (77) ~ (all_68_0 = 0) | ~ (all_68_1 = 0) % 15.84/2.99 | | | | | % 15.84/2.99 | | | | | GROUND_INST: instantiating (10) with 0, all_68_1, xl, simplifying with % 15.84/2.99 | | | | | (1), (75) gives: % 15.84/2.99 | | | | | (78) all_68_1 = 0 % 15.84/2.99 | | | | | % 15.84/2.99 | | | | | GROUND_INST: instantiating (10) with 0, all_68_0, xn, simplifying with % 15.84/2.99 | | | | | (3), (76) gives: % 15.84/2.99 | | | | | (79) all_68_0 = 0 % 15.84/2.99 | | | | | % 15.84/2.99 | | | | | BETA: splitting (77) gives: % 15.84/2.99 | | | | | % 15.84/2.99 | | | | | Case 1: % 15.84/2.99 | | | | | | % 15.84/2.99 | | | | | | (80) ~ (all_68_0 = 0) % 15.84/2.99 | | | | | | % 15.84/2.99 | | | | | | REDUCE: (79), (80) imply: % 15.84/2.99 | | | | | | (81) $false % 15.84/2.99 | | | | | | % 15.84/2.99 | | | | | | CLOSE: (81) is inconsistent. % 15.84/2.99 | | | | | | % 15.84/2.99 | | | | | Case 2: % 15.84/2.99 | | | | | | % 15.84/2.99 | | | | | | (82) ~ (all_68_1 = 0) % 15.84/2.99 | | | | | | % 15.84/2.99 | | | | | | REDUCE: (78), (82) imply: % 15.84/2.99 | | | | | | (83) $false % 15.84/2.99 | | | | | | % 15.84/2.99 | | | | | | CLOSE: (83) is inconsistent. % 15.84/2.99 | | | | | | % 15.84/2.99 | | | | | End of split % 15.84/2.99 | | | | | % 15.84/2.99 | | | | Case 2: % 15.84/2.99 | | | | | % 15.84/2.99 | | | | | (84) ? [v0: $i] : (sdtasdt0(xl, v0) = xn & aNaturalNumber0(v0) = 0 % 15.84/2.99 | | | | | & $i(v0)) % 15.84/2.99 | | | | | % 15.84/2.99 | | | | | DELTA: instantiating (84) with fresh symbol all_68_0 gives: % 15.84/2.99 | | | | | (85) sdtasdt0(xl, all_68_0) = xn & aNaturalNumber0(all_68_0) = 0 & % 15.84/2.99 | | | | | $i(all_68_0) % 15.84/2.99 | | | | | % 15.84/2.99 | | | | | ALPHA: (85) implies: % 15.84/2.99 | | | | | (86) $i(all_68_0) % 15.84/2.99 | | | | | (87) aNaturalNumber0(all_68_0) = 0 % 15.84/2.99 | | | | | (88) sdtasdt0(xl, all_68_0) = xn % 15.84/2.99 | | | | | % 15.84/2.99 | | | | | BETA: splitting (34) gives: % 15.84/2.99 | | | | | % 15.84/2.99 | | | | | Case 1: % 15.84/2.99 | | | | | | % 15.84/2.99 | | | | | | (89) ~ (all_41_1 = 0) % 15.84/2.99 | | | | | | % 15.84/2.99 | | | | | | REDUCE: (62), (89) imply: % 15.84/2.99 | | | | | | (90) $false % 15.84/2.99 | | | | | | % 15.84/2.99 | | | | | | CLOSE: (90) is inconsistent. % 15.84/2.99 | | | | | | % 15.84/2.99 | | | | | Case 2: % 15.84/2.99 | | | | | | % 15.84/2.99 | | | | | | (91) ~ (all_41_2 = 0) | all_41_0 = all_32_1 % 15.84/2.99 | | | | | | % 15.84/2.99 | | | | | | BETA: splitting (91) gives: % 15.84/2.99 | | | | | | % 15.84/2.99 | | | | | | Case 1: % 15.84/2.99 | | | | | | | % 15.84/2.99 | | | | | | | (92) ~ (all_41_2 = 0) % 15.84/2.99 | | | | | | | % 15.84/2.99 | | | | | | | REDUCE: (65), (92) imply: % 15.84/2.99 | | | | | | | (93) $false % 15.84/2.99 | | | | | | | % 15.84/2.99 | | | | | | | CLOSE: (93) is inconsistent. % 15.84/2.99 | | | | | | | % 15.84/2.99 | | | | | | Case 2: % 15.84/2.99 | | | | | | | % 15.84/2.99 | | | | | | | (94) all_41_0 = all_32_1 % 15.84/2.99 | | | | | | | % 15.84/2.99 | | | | | | | REDUCE: (33), (94) imply: % 15.84/2.99 | | | | | | | (95) sdtpldt0(xn, xm) = all_32_1 % 15.84/2.99 | | | | | | | % 15.84/2.99 | | | | | | | BETA: splitting (72) gives: % 15.84/2.99 | | | | | | | % 15.84/2.99 | | | | | | | Case 1: % 15.84/2.99 | | | | | | | | % 15.84/2.99 | | | | | | | | (96) ~ (all_39_2 = 0) % 15.84/2.99 | | | | | | | | % 15.84/2.99 | | | | | | | | REDUCE: (69), (96) imply: % 15.84/2.99 | | | | | | | | (97) $false % 15.84/2.99 | | | | | | | | % 15.84/2.99 | | | | | | | | CLOSE: (97) is inconsistent. % 15.84/2.99 | | | | | | | | % 15.84/2.99 | | | | | | | Case 2: % 15.84/2.99 | | | | | | | | % 15.84/2.99 | | | | | | | | (98) all_39_0 = 0 % 15.84/2.99 | | | | | | | | % 15.84/2.99 | | | | | | | | REDUCE: (28), (98) imply: % 15.84/2.99 | | | | | | | | (99) aNaturalNumber0(all_32_1) = 0 % 15.84/2.99 | | | | | | | | % 15.84/2.99 | | | | | | | | BETA: splitting (24) gives: % 15.84/2.99 | | | | | | | | % 15.84/2.99 | | | | | | | | Case 1: % 15.84/2.99 | | | | | | | | | % 15.84/2.99 | | | | | | | | | (100) ? [v0: any] : ? [v1: any] : % 15.84/2.99 | | | | | | | | | (aNaturalNumber0(all_32_1) = v1 & aNaturalNumber0(xl) % 15.84/2.99 | | | | | | | | | = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 15.84/2.99 | | | | | | | | | % 15.84/2.99 | | | | | | | | | DELTA: instantiating (100) with fresh symbols all_88_0, % 15.84/2.99 | | | | | | | | | all_88_1 gives: % 15.84/2.99 | | | | | | | | | (101) aNaturalNumber0(all_32_1) = all_88_0 & % 15.84/2.99 | | | | | | | | | aNaturalNumber0(xl) = all_88_1 & ( ~ (all_88_0 = 0) | % 15.84/2.99 | | | | | | | | | ~ (all_88_1 = 0)) % 15.84/2.99 | | | | | | | | | % 15.84/2.99 | | | | | | | | | ALPHA: (101) implies: % 15.84/2.99 | | | | | | | | | (102) aNaturalNumber0(xl) = all_88_1 % 15.84/2.99 | | | | | | | | | (103) aNaturalNumber0(all_32_1) = all_88_0 % 15.84/2.99 | | | | | | | | | (104) ~ (all_88_0 = 0) | ~ (all_88_1 = 0) % 15.84/3.00 | | | | | | | | | % 15.84/3.00 | | | | | | | | | GROUND_INST: instantiating (10) with 0, all_88_1, xl, % 15.84/3.00 | | | | | | | | | simplifying with (1), (102) gives: % 15.84/3.00 | | | | | | | | | (105) all_88_1 = 0 % 15.84/3.00 | | | | | | | | | % 15.84/3.00 | | | | | | | | | GROUND_INST: instantiating (10) with 0, all_88_0, all_32_1, % 15.84/3.00 | | | | | | | | | simplifying with (99), (103) gives: % 15.84/3.00 | | | | | | | | | (106) all_88_0 = 0 % 15.84/3.00 | | | | | | | | | % 15.84/3.00 | | | | | | | | | BETA: splitting (104) gives: % 15.84/3.00 | | | | | | | | | % 15.84/3.00 | | | | | | | | | Case 1: % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | (107) ~ (all_88_0 = 0) % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | REDUCE: (106), (107) imply: % 15.84/3.00 | | | | | | | | | | (108) $false % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | CLOSE: (108) is inconsistent. % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | Case 2: % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | (109) ~ (all_88_1 = 0) % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | REDUCE: (105), (109) imply: % 15.84/3.00 | | | | | | | | | | (110) $false % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | CLOSE: (110) is inconsistent. % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | End of split % 15.84/3.00 | | | | | | | | | % 15.84/3.00 | | | | | | | | Case 2: % 15.84/3.00 | | | | | | | | | % 15.84/3.00 | | | | | | | | | (111) ( ~ (all_32_0 = 0) | ? [v0: $i] : (sdtasdt0(xl, v0) % 15.84/3.00 | | | | | | | | | = all_32_1 & aNaturalNumber0(v0) = 0 & $i(v0))) & % 15.84/3.00 | | | | | | | | | (all_32_0 = 0 | ! [v0: $i] : ( ~ (sdtasdt0(xl, v0) = % 15.84/3.00 | | | | | | | | | all_32_1) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 % 15.84/3.00 | | | | | | | | | = 0) & aNaturalNumber0(v0) = v1))) % 15.84/3.00 | | | | | | | | | % 15.84/3.00 | | | | | | | | | ALPHA: (111) implies: % 15.84/3.00 | | | | | | | | | (112) all_32_0 = 0 | ! [v0: $i] : ( ~ (sdtasdt0(xl, v0) = % 15.84/3.00 | | | | | | | | | all_32_1) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = % 15.84/3.00 | | | | | | | | | 0) & aNaturalNumber0(v0) = v1)) % 15.84/3.00 | | | | | | | | | % 15.84/3.00 | | | | | | | | | BETA: splitting (20) gives: % 15.84/3.00 | | | | | | | | | % 15.84/3.00 | | | | | | | | | Case 1: % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | (113) ? [v0: any] : ? [v1: any] : (aNaturalNumber0(xm) % 15.84/3.00 | | | | | | | | | | = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | % 15.84/3.00 | | | | | | | | | | ~ (v0 = 0))) % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | DELTA: instantiating (113) with fresh symbols all_89_0, % 15.84/3.00 | | | | | | | | | | all_89_1 gives: % 15.84/3.00 | | | | | | | | | | (114) aNaturalNumber0(xm) = all_89_0 & % 15.84/3.00 | | | | | | | | | | aNaturalNumber0(xl) = all_89_1 & ( ~ (all_89_0 = 0) % 15.84/3.00 | | | | | | | | | | | ~ (all_89_1 = 0)) % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | ALPHA: (114) implies: % 15.84/3.00 | | | | | | | | | | (115) aNaturalNumber0(xl) = all_89_1 % 15.84/3.00 | | | | | | | | | | (116) aNaturalNumber0(xm) = all_89_0 % 15.84/3.00 | | | | | | | | | | (117) ~ (all_89_0 = 0) | ~ (all_89_1 = 0) % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | GROUND_INST: instantiating (10) with 0, all_89_1, xl, % 15.84/3.00 | | | | | | | | | | simplifying with (1), (115) gives: % 15.84/3.00 | | | | | | | | | | (118) all_89_1 = 0 % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | GROUND_INST: instantiating (10) with 0, all_89_0, xm, % 15.84/3.00 | | | | | | | | | | simplifying with (2), (116) gives: % 15.84/3.00 | | | | | | | | | | (119) all_89_0 = 0 % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | BETA: splitting (117) gives: % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | Case 1: % 15.84/3.00 | | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | | (120) ~ (all_89_0 = 0) % 15.84/3.00 | | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | | REDUCE: (119), (120) imply: % 15.84/3.00 | | | | | | | | | | | (121) $false % 15.84/3.00 | | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | | CLOSE: (121) is inconsistent. % 15.84/3.00 | | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | Case 2: % 15.84/3.00 | | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | | (122) ~ (all_89_1 = 0) % 15.84/3.00 | | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | | REDUCE: (118), (122) imply: % 15.84/3.00 | | | | | | | | | | | (123) $false % 15.84/3.00 | | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | | CLOSE: (123) is inconsistent. % 15.84/3.00 | | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | End of split % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | Case 2: % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | (124) ? [v0: $i] : (sdtasdt0(xl, v0) = xm & % 15.84/3.00 | | | | | | | | | | aNaturalNumber0(v0) = 0 & $i(v0)) % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | DELTA: instantiating (124) with fresh symbol all_89_0 gives: % 15.84/3.00 | | | | | | | | | | (125) sdtasdt0(xl, all_89_0) = xm & % 15.84/3.00 | | | | | | | | | | aNaturalNumber0(all_89_0) = 0 & $i(all_89_0) % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | ALPHA: (125) implies: % 15.84/3.00 | | | | | | | | | | (126) $i(all_89_0) % 15.84/3.00 | | | | | | | | | | (127) aNaturalNumber0(all_89_0) = 0 % 15.84/3.00 | | | | | | | | | | (128) sdtasdt0(xl, all_89_0) = xm % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | BETA: splitting (112) gives: % 15.84/3.00 | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | Case 1: % 15.84/3.00 | | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | | (129) all_32_0 = 0 % 15.84/3.00 | | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | | REDUCE: (14), (129) imply: % 15.84/3.00 | | | | | | | | | | | (130) $false % 15.84/3.00 | | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | | CLOSE: (130) is inconsistent. % 15.84/3.00 | | | | | | | | | | | % 15.84/3.00 | | | | | | | | | | Case 2: % 15.84/3.00 | | | | | | | | | | | % 15.84/3.01 | | | | | | | | | | | (131) ! [v0: $i] : ( ~ (sdtasdt0(xl, v0) = all_32_1) | % 15.84/3.01 | | | | | | | | | | | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 15.84/3.01 | | | | | | | | | | | aNaturalNumber0(v0) = v1)) % 15.84/3.01 | | | | | | | | | | | % 15.84/3.01 | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with xl, all_68_0, xn, % 15.84/3.01 | | | | | | | | | | | simplifying with (6), (86), (88) gives: % 15.84/3.01 | | | | | | | | | | | (132) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 15.84/3.01 | | | | | | | | | | | (sdtasdt0(all_68_0, xl) = v2 & % 15.84/3.01 | | | | | | | | | | | aNaturalNumber0(all_68_0) = v1 & % 15.84/3.01 | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v2) & ( ~ (v1 = 0) % 15.84/3.01 | | | | | | | | | | | | ~ (v0 = 0) | v2 = xn)) % 15.84/3.01 | | | | | | | | | | | % 15.84/3.01 | | | | | | | | | | | GROUND_INST: instantiating (mAMDistr) with xl, all_89_0, % 15.84/3.01 | | | | | | | | | | | all_68_0, xm, xn, all_32_1, simplifying with (6), % 15.84/3.01 | | | | | | | | | | | (16), (86), (88), (126), (128) gives: % 15.84/3.01 | | | | | | | | | | | (133) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 15.84/3.01 | | | | | | | | | | | [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] % 15.84/3.01 | | | | | | | | | | | : ? [v7: $i] : ? [v8: $i] : (sdtasdt0(v3, xl) = % 15.84/3.01 | | | | | | | | | | | v5 & sdtasdt0(all_89_0, xl) = v6 & % 15.84/3.01 | | | | | | | | | | | sdtasdt0(all_68_0, xl) = v7 & sdtasdt0(xl, v3) = % 15.84/3.01 | | | | | | | | | | | v4 & sdtpldt0(v6, v7) = v8 & sdtpldt0(all_89_0, % 15.84/3.01 | | | | | | | | | | | all_68_0) = v3 & aNaturalNumber0(all_89_0) = % 15.84/3.01 | | | | | | | | | | | v1 & aNaturalNumber0(all_68_0) = v2 & % 15.84/3.01 | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v8) & $i(v7) & % 15.84/3.01 | | | | | | | | | | | $i(v6) & $i(v5) & $i(v4) & $i(v3) & ( ~ (v2 = 0) % 15.84/3.01 | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0) | (v8 = v5 & v4 = % 15.84/3.01 | | | | | | | | | | | all_32_1))) % 15.84/3.01 | | | | | | | | | | | % 15.84/3.01 | | | | | | | | | | | GROUND_INST: instantiating (mAMDistr) with xl, all_68_0, % 15.84/3.01 | | | | | | | | | | | all_89_0, xn, xm, all_32_1, simplifying with (6), % 15.84/3.01 | | | | | | | | | | | (86), (88), (95), (126), (128) gives: % 15.84/3.01 | | | | | | | | | | | (134) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 15.84/3.01 | | | | | | | | | | | [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] % 15.84/3.01 | | | | | | | | | | | : ? [v7: $i] : ? [v8: $i] : (sdtasdt0(v3, xl) = % 15.84/3.01 | | | | | | | | | | | v5 & sdtasdt0(all_89_0, xl) = v7 & % 15.84/3.01 | | | | | | | | | | | sdtasdt0(all_68_0, xl) = v6 & sdtasdt0(xl, v3) = % 15.84/3.01 | | | | | | | | | | | v4 & sdtpldt0(v6, v7) = v8 & sdtpldt0(all_68_0, % 15.84/3.01 | | | | | | | | | | | all_89_0) = v3 & aNaturalNumber0(all_89_0) = % 15.84/3.01 | | | | | | | | | | | v2 & aNaturalNumber0(all_68_0) = v1 & % 15.84/3.01 | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v8) & $i(v7) & % 15.84/3.01 | | | | | | | | | | | $i(v6) & $i(v5) & $i(v4) & $i(v3) & ( ~ (v2 = 0) % 15.84/3.01 | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0) | (v8 = v5 & v4 = % 15.84/3.01 | | | | | | | | | | | all_32_1))) % 15.84/3.01 | | | | | | | | | | | % 15.84/3.01 | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with xl, all_89_0, xm, % 15.84/3.01 | | | | | | | | | | | simplifying with (6), (126), (128) gives: % 15.84/3.01 | | | | | | | | | | | (135) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 15.84/3.01 | | | | | | | | | | | (sdtasdt0(all_89_0, xl) = v2 & % 15.84/3.01 | | | | | | | | | | | aNaturalNumber0(all_89_0) = v1 & % 15.84/3.01 | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v2) & ( ~ (v1 = 0) % 15.84/3.01 | | | | | | | | | | | | ~ (v0 = 0) | v2 = xm)) % 15.84/3.01 | | | | | | | | | | | % 15.84/3.01 | | | | | | | | | | | DELTA: instantiating (135) with fresh symbols all_104_0, % 15.84/3.01 | | | | | | | | | | | all_104_1, all_104_2 gives: % 15.84/3.01 | | | | | | | | | | | (136) sdtasdt0(all_89_0, xl) = all_104_0 & % 15.84/3.01 | | | | | | | | | | | aNaturalNumber0(all_89_0) = all_104_1 & % 15.84/3.01 | | | | | | | | | | | aNaturalNumber0(xl) = all_104_2 & $i(all_104_0) & % 15.84/3.01 | | | | | | | | | | | ( ~ (all_104_1 = 0) | ~ (all_104_2 = 0) | % 15.84/3.01 | | | | | | | | | | | all_104_0 = xm) % 15.84/3.01 | | | | | | | | | | | % 15.84/3.01 | | | | | | | | | | | ALPHA: (136) implies: % 15.84/3.01 | | | | | | | | | | | (137) aNaturalNumber0(xl) = all_104_2 % 15.84/3.01 | | | | | | | | | | | (138) aNaturalNumber0(all_89_0) = all_104_1 % 15.84/3.01 | | | | | | | | | | | (139) sdtasdt0(all_89_0, xl) = all_104_0 % 15.84/3.01 | | | | | | | | | | | (140) ~ (all_104_1 = 0) | ~ (all_104_2 = 0) | % 15.84/3.01 | | | | | | | | | | | all_104_0 = xm % 15.84/3.01 | | | | | | | | | | | % 15.84/3.01 | | | | | | | | | | | DELTA: instantiating (132) with fresh symbols all_106_0, % 15.84/3.01 | | | | | | | | | | | all_106_1, all_106_2 gives: % 15.84/3.02 | | | | | | | | | | | (141) sdtasdt0(all_68_0, xl) = all_106_0 & % 15.84/3.02 | | | | | | | | | | | aNaturalNumber0(all_68_0) = all_106_1 & % 15.84/3.02 | | | | | | | | | | | aNaturalNumber0(xl) = all_106_2 & $i(all_106_0) & % 15.84/3.02 | | | | | | | | | | | ( ~ (all_106_1 = 0) | ~ (all_106_2 = 0) | % 15.84/3.02 | | | | | | | | | | | all_106_0 = xn) % 15.84/3.02 | | | | | | | | | | | % 15.84/3.02 | | | | | | | | | | | ALPHA: (141) implies: % 15.84/3.02 | | | | | | | | | | | (142) aNaturalNumber0(xl) = all_106_2 % 15.84/3.02 | | | | | | | | | | | (143) aNaturalNumber0(all_68_0) = all_106_1 % 15.84/3.02 | | | | | | | | | | | (144) sdtasdt0(all_68_0, xl) = all_106_0 % 15.84/3.02 | | | | | | | | | | | (145) ~ (all_106_1 = 0) | ~ (all_106_2 = 0) | % 15.84/3.02 | | | | | | | | | | | all_106_0 = xn % 15.84/3.02 | | | | | | | | | | | % 15.84/3.02 | | | | | | | | | | | DELTA: instantiating (134) with fresh symbols all_108_0, % 15.84/3.02 | | | | | | | | | | | all_108_1, all_108_2, all_108_3, all_108_4, % 15.84/3.02 | | | | | | | | | | | all_108_5, all_108_6, all_108_7, all_108_8 gives: % 15.84/3.02 | | | | | | | | | | | (146) sdtasdt0(all_108_5, xl) = all_108_3 & % 15.84/3.02 | | | | | | | | | | | sdtasdt0(all_89_0, xl) = all_108_1 & % 15.84/3.02 | | | | | | | | | | | sdtasdt0(all_68_0, xl) = all_108_2 & sdtasdt0(xl, % 15.84/3.02 | | | | | | | | | | | all_108_5) = all_108_4 & sdtpldt0(all_108_2, % 15.84/3.02 | | | | | | | | | | | all_108_1) = all_108_0 & sdtpldt0(all_68_0, % 15.84/3.02 | | | | | | | | | | | all_89_0) = all_108_5 & % 15.84/3.02 | | | | | | | | | | | aNaturalNumber0(all_89_0) = all_108_6 & % 15.84/3.02 | | | | | | | | | | | aNaturalNumber0(all_68_0) = all_108_7 & % 15.84/3.02 | | | | | | | | | | | aNaturalNumber0(xl) = all_108_8 & $i(all_108_0) & % 15.84/3.02 | | | | | | | | | | | $i(all_108_1) & $i(all_108_2) & $i(all_108_3) & % 15.84/3.02 | | | | | | | | | | | $i(all_108_4) & $i(all_108_5) & ( ~ (all_108_6 = % 15.84/3.02 | | | | | | | | | | | 0) | ~ (all_108_7 = 0) | ~ (all_108_8 = 0) | % 15.84/3.02 | | | | | | | | | | | (all_108_0 = all_108_3 & all_108_4 = all_32_1)) % 15.84/3.02 | | | | | | | | | | | % 15.84/3.02 | | | | | | | | | | | ALPHA: (146) implies: % 15.84/3.02 | | | | | | | | | | | (147) $i(all_108_5) % 15.84/3.02 | | | | | | | | | | | (148) aNaturalNumber0(xl) = all_108_8 % 15.84/3.02 | | | | | | | | | | | (149) aNaturalNumber0(all_68_0) = all_108_7 % 15.84/3.02 | | | | | | | | | | | (150) aNaturalNumber0(all_89_0) = all_108_6 % 15.84/3.02 | | | | | | | | | | | (151) sdtpldt0(all_68_0, all_89_0) = all_108_5 % 15.84/3.02 | | | | | | | | | | | (152) sdtpldt0(all_108_2, all_108_1) = all_108_0 % 15.84/3.02 | | | | | | | | | | | (153) sdtasdt0(xl, all_108_5) = all_108_4 % 15.84/3.02 | | | | | | | | | | | (154) sdtasdt0(all_68_0, xl) = all_108_2 % 15.84/3.02 | | | | | | | | | | | (155) sdtasdt0(all_89_0, xl) = all_108_1 % 15.84/3.02 | | | | | | | | | | | (156) sdtasdt0(all_108_5, xl) = all_108_3 % 15.84/3.02 | | | | | | | | | | | (157) ~ (all_108_6 = 0) | ~ (all_108_7 = 0) | ~ % 15.84/3.02 | | | | | | | | | | | (all_108_8 = 0) | (all_108_0 = all_108_3 & % 15.84/3.02 | | | | | | | | | | | all_108_4 = all_32_1) % 15.84/3.02 | | | | | | | | | | | % 15.84/3.02 | | | | | | | | | | | DELTA: instantiating (133) with fresh symbols all_110_0, % 15.84/3.02 | | | | | | | | | | | all_110_1, all_110_2, all_110_3, all_110_4, % 15.84/3.02 | | | | | | | | | | | all_110_5, all_110_6, all_110_7, all_110_8 gives: % 15.84/3.02 | | | | | | | | | | | (158) sdtasdt0(all_110_5, xl) = all_110_3 & % 15.84/3.02 | | | | | | | | | | | sdtasdt0(all_89_0, xl) = all_110_2 & % 15.84/3.02 | | | | | | | | | | | sdtasdt0(all_68_0, xl) = all_110_1 & sdtasdt0(xl, % 15.84/3.02 | | | | | | | | | | | all_110_5) = all_110_4 & sdtpldt0(all_110_2, % 15.84/3.02 | | | | | | | | | | | all_110_1) = all_110_0 & sdtpldt0(all_89_0, % 15.84/3.02 | | | | | | | | | | | all_68_0) = all_110_5 & % 15.84/3.02 | | | | | | | | | | | aNaturalNumber0(all_89_0) = all_110_7 & % 15.84/3.02 | | | | | | | | | | | aNaturalNumber0(all_68_0) = all_110_6 & % 15.84/3.02 | | | | | | | | | | | aNaturalNumber0(xl) = all_110_8 & $i(all_110_0) & % 15.84/3.02 | | | | | | | | | | | $i(all_110_1) & $i(all_110_2) & $i(all_110_3) & % 15.84/3.02 | | | | | | | | | | | $i(all_110_4) & $i(all_110_5) & ( ~ (all_110_6 = % 15.84/3.02 | | | | | | | | | | | 0) | ~ (all_110_7 = 0) | ~ (all_110_8 = 0) | % 15.84/3.02 | | | | | | | | | | | (all_110_0 = all_110_3 & all_110_4 = all_32_1)) % 15.84/3.02 | | | | | | | | | | | % 15.84/3.02 | | | | | | | | | | | ALPHA: (158) implies: % 15.84/3.02 | | | | | | | | | | | (159) aNaturalNumber0(xl) = all_110_8 % 15.84/3.02 | | | | | | | | | | | (160) aNaturalNumber0(all_68_0) = all_110_6 % 15.84/3.02 | | | | | | | | | | | (161) aNaturalNumber0(all_89_0) = all_110_7 % 15.84/3.02 | | | | | | | | | | | (162) sdtpldt0(all_89_0, all_68_0) = all_110_5 % 15.84/3.02 | | | | | | | | | | | (163) sdtasdt0(all_68_0, xl) = all_110_1 % 15.84/3.02 | | | | | | | | | | | (164) sdtasdt0(all_89_0, xl) = all_110_2 % 15.84/3.02 | | | | | | | | | | | % 15.84/3.02 | | | | | | | | | | | GROUND_INST: instantiating (10) with all_104_2, all_106_2, xl, % 15.84/3.02 | | | | | | | | | | | simplifying with (137), (142) gives: % 15.84/3.02 | | | | | | | | | | | (165) all_106_2 = all_104_2 % 15.84/3.02 | | | | | | | | | | | % 15.84/3.02 | | | | | | | | | | | GROUND_INST: instantiating (10) with 0, all_110_8, xl, % 15.84/3.02 | | | | | | | | | | | simplifying with (1), (159) gives: % 15.84/3.02 | | | | | | | | | | | (166) all_110_8 = 0 % 15.84/3.02 | | | | | | | | | | | % 15.84/3.02 | | | | | | | | | | | GROUND_INST: instantiating (10) with all_108_8, all_110_8, xl, % 15.84/3.02 | | | | | | | | | | | simplifying with (148), (159) gives: % 15.84/3.02 | | | | | | | | | | | (167) all_110_8 = all_108_8 % 15.84/3.02 | | | | | | | | | | | % 15.84/3.02 | | | | | | | | | | | GROUND_INST: instantiating (10) with all_106_2, all_110_8, xl, % 15.84/3.02 | | | | | | | | | | | simplifying with (142), (159) gives: % 15.84/3.02 | | | | | | | | | | | (168) all_110_8 = all_106_2 % 15.84/3.02 | | | | | | | | | | | % 15.84/3.02 | | | | | | | | | | | GROUND_INST: instantiating (10) with all_106_1, all_108_7, % 15.84/3.02 | | | | | | | | | | | all_68_0, simplifying with (143), (149) gives: % 15.84/3.02 | | | | | | | | | | | (169) all_108_7 = all_106_1 % 15.84/3.02 | | | | | | | | | | | % 15.84/3.02 | | | | | | | | | | | GROUND_INST: instantiating (10) with 0, all_110_6, all_68_0, % 15.84/3.02 | | | | | | | | | | | simplifying with (87), (160) gives: % 15.84/3.02 | | | | | | | | | | | (170) all_110_6 = 0 % 15.84/3.02 | | | | | | | | | | | % 15.84/3.02 | | | | | | | | | | | GROUND_INST: instantiating (10) with all_108_7, all_110_6, % 15.84/3.02 | | | | | | | | | | | all_68_0, simplifying with (149), (160) gives: % 15.84/3.02 | | | | | | | | | | | (171) all_110_6 = all_108_7 % 15.84/3.02 | | | | | | | | | | | % 15.84/3.02 | | | | | | | | | | | GROUND_INST: instantiating (10) with 0, all_108_6, all_89_0, % 15.84/3.02 | | | | | | | | | | | simplifying with (127), (150) gives: % 15.84/3.02 | | | | | | | | | | | (172) all_108_6 = 0 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | GROUND_INST: instantiating (10) with all_108_6, all_110_7, % 15.84/3.03 | | | | | | | | | | | all_89_0, simplifying with (150), (161) gives: % 15.84/3.03 | | | | | | | | | | | (173) all_110_7 = all_108_6 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | GROUND_INST: instantiating (10) with all_104_1, all_110_7, % 15.84/3.03 | | | | | | | | | | | all_89_0, simplifying with (138), (161) gives: % 15.84/3.03 | | | | | | | | | | | (174) all_110_7 = all_104_1 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | GROUND_INST: instantiating (12) with all_108_2, all_110_1, xl, % 15.84/3.03 | | | | | | | | | | | all_68_0, simplifying with (154), (163) gives: % 15.84/3.03 | | | | | | | | | | | (175) all_110_1 = all_108_2 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | GROUND_INST: instantiating (12) with all_106_0, all_110_1, xl, % 15.84/3.03 | | | | | | | | | | | all_68_0, simplifying with (144), (163) gives: % 15.84/3.03 | | | | | | | | | | | (176) all_110_1 = all_106_0 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | GROUND_INST: instantiating (12) with all_108_1, all_110_2, xl, % 15.84/3.03 | | | | | | | | | | | all_89_0, simplifying with (155), (164) gives: % 15.84/3.03 | | | | | | | | | | | (177) all_110_2 = all_108_1 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | GROUND_INST: instantiating (12) with all_104_0, all_110_2, xl, % 15.84/3.03 | | | | | | | | | | | all_89_0, simplifying with (139), (164) gives: % 15.84/3.03 | | | | | | | | | | | (178) all_110_2 = all_104_0 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | COMBINE_EQS: (175), (176) imply: % 15.84/3.03 | | | | | | | | | | | (179) all_108_2 = all_106_0 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | SIMP: (179) implies: % 15.84/3.03 | | | | | | | | | | | (180) all_108_2 = all_106_0 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | COMBINE_EQS: (177), (178) imply: % 15.84/3.03 | | | | | | | | | | | (181) all_108_1 = all_104_0 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | SIMP: (181) implies: % 15.84/3.03 | | | | | | | | | | | (182) all_108_1 = all_104_0 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | COMBINE_EQS: (170), (171) imply: % 15.84/3.03 | | | | | | | | | | | (183) all_108_7 = 0 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | SIMP: (183) implies: % 15.84/3.03 | | | | | | | | | | | (184) all_108_7 = 0 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | COMBINE_EQS: (173), (174) imply: % 15.84/3.03 | | | | | | | | | | | (185) all_108_6 = all_104_1 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | SIMP: (185) implies: % 15.84/3.03 | | | | | | | | | | | (186) all_108_6 = all_104_1 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | COMBINE_EQS: (166), (167) imply: % 15.84/3.03 | | | | | | | | | | | (187) all_108_8 = 0 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | COMBINE_EQS: (167), (168) imply: % 15.84/3.03 | | | | | | | | | | | (188) all_108_8 = all_106_2 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | COMBINE_EQS: (172), (186) imply: % 15.84/3.03 | | | | | | | | | | | (189) all_104_1 = 0 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | SIMP: (189) implies: % 15.84/3.03 | | | | | | | | | | | (190) all_104_1 = 0 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | COMBINE_EQS: (169), (184) imply: % 15.84/3.03 | | | | | | | | | | | (191) all_106_1 = 0 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | COMBINE_EQS: (187), (188) imply: % 15.84/3.03 | | | | | | | | | | | (192) all_106_2 = 0 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | SIMP: (192) implies: % 15.84/3.03 | | | | | | | | | | | (193) all_106_2 = 0 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | COMBINE_EQS: (165), (193) imply: % 15.84/3.03 | | | | | | | | | | | (194) all_104_2 = 0 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | SIMP: (194) implies: % 15.84/3.03 | | | | | | | | | | | (195) all_104_2 = 0 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | REDUCE: (152), (180), (182) imply: % 15.84/3.03 | | | | | | | | | | | (196) sdtpldt0(all_106_0, all_104_0) = all_108_0 % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | BETA: splitting (145) gives: % 15.84/3.03 | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | Case 1: % 15.84/3.03 | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | (197) ~ (all_106_1 = 0) % 15.84/3.03 | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | REDUCE: (191), (197) imply: % 15.84/3.03 | | | | | | | | | | | | (198) $false % 15.84/3.03 | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | CLOSE: (198) is inconsistent. % 15.84/3.03 | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | Case 2: % 15.84/3.03 | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | (199) ~ (all_106_2 = 0) | all_106_0 = xn % 15.84/3.03 | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | BETA: splitting (199) gives: % 15.84/3.03 | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | Case 1: % 15.84/3.03 | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | (200) ~ (all_106_2 = 0) % 15.84/3.03 | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | REDUCE: (193), (200) imply: % 15.84/3.03 | | | | | | | | | | | | | (201) $false % 15.84/3.03 | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | CLOSE: (201) is inconsistent. % 15.84/3.03 | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | Case 2: % 15.84/3.03 | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | (202) all_106_0 = xn % 15.84/3.03 | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | REDUCE: (196), (202) imply: % 15.84/3.03 | | | | | | | | | | | | | (203) sdtpldt0(xn, all_104_0) = all_108_0 % 15.84/3.03 | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | BETA: splitting (157) gives: % 15.84/3.03 | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | Case 1: % 15.84/3.03 | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | (204) ~ (all_108_6 = 0) % 15.84/3.03 | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | REDUCE: (172), (204) imply: % 15.84/3.03 | | | | | | | | | | | | | | (205) $false % 15.84/3.03 | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | CLOSE: (205) is inconsistent. % 15.84/3.03 | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | Case 2: % 15.84/3.03 | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | (206) ~ (all_108_7 = 0) | ~ (all_108_8 = 0) | % 15.84/3.03 | | | | | | | | | | | | | | (all_108_0 = all_108_3 & all_108_4 = all_32_1) % 15.84/3.03 | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | BETA: splitting (206) gives: % 15.84/3.03 | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | Case 1: % 15.84/3.03 | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | (207) ~ (all_108_7 = 0) % 15.84/3.03 | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | REDUCE: (184), (207) imply: % 15.84/3.03 | | | | | | | | | | | | | | | (208) $false % 15.84/3.03 | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | CLOSE: (208) is inconsistent. % 15.84/3.03 | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | Case 2: % 15.84/3.03 | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | (209) ~ (all_108_8 = 0) | (all_108_0 = all_108_3 & % 15.84/3.03 | | | | | | | | | | | | | | | all_108_4 = all_32_1) % 15.84/3.03 | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | BETA: splitting (140) gives: % 15.84/3.03 | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | Case 1: % 15.84/3.03 | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | (210) ~ (all_104_1 = 0) % 15.84/3.03 | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | REDUCE: (190), (210) imply: % 15.84/3.03 | | | | | | | | | | | | | | | | (211) $false % 15.84/3.03 | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | CLOSE: (211) is inconsistent. % 15.84/3.03 | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | Case 2: % 15.84/3.03 | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | (212) ~ (all_104_2 = 0) | all_104_0 = xm % 15.84/3.03 | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | BETA: splitting (212) gives: % 15.84/3.03 | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | Case 1: % 15.84/3.03 | | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | | (213) ~ (all_104_2 = 0) % 15.84/3.03 | | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | | REDUCE: (195), (213) imply: % 15.84/3.03 | | | | | | | | | | | | | | | | | (214) $false % 15.84/3.03 | | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | | CLOSE: (214) is inconsistent. % 15.84/3.03 | | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | Case 2: % 15.84/3.03 | | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | | (215) all_104_0 = xm % 15.84/3.03 | | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | | REDUCE: (203), (215) imply: % 15.84/3.03 | | | | | | | | | | | | | | | | | (216) sdtpldt0(xn, xm) = all_108_0 % 15.84/3.03 | | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | | BETA: splitting (209) gives: % 15.84/3.03 | | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | | Case 1: % 15.84/3.03 | | | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | | | (217) ~ (all_108_8 = 0) % 15.84/3.03 | | | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | | | REDUCE: (187), (217) imply: % 15.84/3.03 | | | | | | | | | | | | | | | | | | (218) $false % 15.84/3.03 | | | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | | | CLOSE: (218) is inconsistent. % 15.84/3.03 | | | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | | Case 2: % 15.84/3.03 | | | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | | | (219) all_108_0 = all_108_3 & all_108_4 = all_32_1 % 15.84/3.03 | | | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | | | ALPHA: (219) implies: % 15.84/3.03 | | | | | | | | | | | | | | | | | | (220) all_108_4 = all_32_1 % 15.84/3.03 | | | | | | | | | | | | | | | | | | (221) all_108_0 = all_108_3 % 15.84/3.03 | | | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | | | REDUCE: (153), (220) imply: % 15.84/3.03 | | | | | | | | | | | | | | | | | | (222) sdtasdt0(xl, all_108_5) = all_32_1 % 15.84/3.03 | | | | | | | | | | | | | | | | | | % 15.84/3.03 | | | | | | | | | | | | | | | | | | REDUCE: (216), (221) imply: % 15.84/3.03 | | | | | | | | | | | | | | | | | | (223) sdtpldt0(xn, xm) = all_108_3 % 15.84/3.03 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (11) with all_32_1, all_108_3, xm, % 15.84/3.04 | | | | | | | | | | | | | | | | | | xn, simplifying with (95), (223) gives: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (224) all_108_3 = all_32_1 % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | REDUCE: (156), (224) imply: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (225) sdtasdt0(all_108_5, xl) = all_32_1 % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mAddComm) with all_68_0, all_89_0, % 15.84/3.04 | | | | | | | | | | | | | | | | | | all_108_5, simplifying with (86), (126), (151) % 15.84/3.04 | | | | | | | | | | | | | | | | | | gives: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (226) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 15.84/3.04 | | | | | | | | | | | | | | | | | | (sdtpldt0(all_89_0, all_68_0) = v2 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_89_0) = v1 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_68_0) = v0 & $i(v2) & ( ~ % 15.84/3.04 | | | | | | | | | | | | | | | | | | (v1 = 0) | ~ (v0 = 0) | v2 = all_108_5)) % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mSortsB) with all_68_0, all_89_0, % 15.84/3.04 | | | | | | | | | | | | | | | | | | all_108_5, simplifying with (86), (126), (151) % 15.84/3.04 | | | | | | | | | | | | | | | | | | gives: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (227) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 15.84/3.04 | | | | | | | | | | | | | | | | | | (aNaturalNumber0(all_108_5) = v2 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_89_0) = v1 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_68_0) = v0 & ( ~ (v1 = 0) | % 15.84/3.04 | | | | | | | | | | | | | | | | | | ~ (v0 = 0) | v2 = 0)) % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mAddComm) with all_89_0, all_68_0, % 15.84/3.04 | | | | | | | | | | | | | | | | | | all_110_5, simplifying with (86), (126), (162) % 15.84/3.04 | | | | | | | | | | | | | | | | | | gives: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (228) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 15.84/3.04 | | | | | | | | | | | | | | | | | | (sdtpldt0(all_68_0, all_89_0) = v2 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_89_0) = v0 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_68_0) = v1 & $i(v2) & ( ~ % 15.84/3.04 | | | | | | | | | | | | | | | | | | (v1 = 0) | ~ (v0 = 0) | v2 = all_110_5)) % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mSortsB) with all_89_0, all_68_0, % 15.84/3.04 | | | | | | | | | | | | | | | | | | all_110_5, simplifying with (86), (126), (162) % 15.84/3.04 | | | | | | | | | | | | | | | | | | gives: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (229) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 15.84/3.04 | | | | | | | | | | | | | | | | | | (aNaturalNumber0(all_110_5) = v2 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_89_0) = v0 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_68_0) = v1 & ( ~ (v1 = 0) | % 15.84/3.04 | | | | | | | | | | | | | | | | | | ~ (v0 = 0) | v2 = 0)) % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (131) with all_108_5, simplifying % 15.84/3.04 | | | | | | | | | | | | | | | | | | with (147), (222) gives: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (230) ? [v0: int] : ( ~ (v0 = 0) & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_108_5) = v0) % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with xl, all_108_5, % 15.84/3.04 | | | | | | | | | | | | | | | | | | all_32_1, simplifying with (6), (147), (222) % 15.84/3.04 | | | | | | | | | | | | | | | | | | gives: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (231) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 15.84/3.04 | | | | | | | | | | | | | | | | | | (sdtasdt0(all_108_5, xl) = v2 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_108_5) = v1 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & $i(v2) & ( ~ (v1 = 0) % 15.84/3.04 | | | | | | | | | | | | | | | | | | | ~ (v0 = 0) | v2 = all_32_1)) % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mSortsB_02) with xl, all_108_5, % 15.84/3.04 | | | | | | | | | | | | | | | | | | all_32_1, simplifying with (6), (147), (222) % 15.84/3.04 | | | | | | | | | | | | | | | | | | gives: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (232) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 15.84/3.04 | | | | | | | | | | | | | | | | | | (aNaturalNumber0(all_108_5) = v1 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_32_1) = v2 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 % 15.84/3.04 | | | | | | | | | | | | | | | | | | = 0) | v2 = 0)) % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with all_108_5, xl, % 15.84/3.04 | | | | | | | | | | | | | | | | | | all_32_1, simplifying with (6), (147), (225) % 15.84/3.04 | | | | | | | | | | | | | | | | | | gives: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (233) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 15.84/3.04 | | | | | | | | | | | | | | | | | | (sdtasdt0(xl, all_108_5) = v2 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_108_5) = v0 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v1 & $i(v2) & ( ~ (v1 = 0) % 15.84/3.04 | | | | | | | | | | | | | | | | | | | ~ (v0 = 0) | v2 = all_32_1)) % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (mSortsB_02) with all_108_5, xl, % 15.84/3.04 | | | | | | | | | | | | | | | | | | all_32_1, simplifying with (6), (147), (225) % 15.84/3.04 | | | | | | | | | | | | | | | | | | gives: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (234) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 15.84/3.04 | | | | | | | | | | | | | | | | | | (aNaturalNumber0(all_108_5) = v0 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_32_1) = v2 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = v1 & ( ~ (v1 = 0) | ~ (v0 % 15.84/3.04 | | | | | | | | | | | | | | | | | | = 0) | v2 = 0)) % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | DELTA: instantiating (230) with fresh symbol all_179_0 % 15.84/3.04 | | | | | | | | | | | | | | | | | | gives: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (235) ~ (all_179_0 = 0) & aNaturalNumber0(all_108_5) = % 15.84/3.04 | | | | | | | | | | | | | | | | | | all_179_0 % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | ALPHA: (235) implies: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (236) ~ (all_179_0 = 0) % 15.84/3.04 | | | | | | | | | | | | | | | | | | (237) aNaturalNumber0(all_108_5) = all_179_0 % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | DELTA: instantiating (232) with fresh symbols all_183_0, % 15.84/3.04 | | | | | | | | | | | | | | | | | | all_183_1, all_183_2 gives: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (238) aNaturalNumber0(all_108_5) = all_183_1 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_32_1) = all_183_0 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = all_183_2 & ( ~ (all_183_1 = % 15.84/3.04 | | | | | | | | | | | | | | | | | | 0) | ~ (all_183_2 = 0) | all_183_0 = 0) % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | ALPHA: (238) implies: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (239) aNaturalNumber0(all_108_5) = all_183_1 % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | DELTA: instantiating (229) with fresh symbols all_185_0, % 15.84/3.04 | | | | | | | | | | | | | | | | | | all_185_1, all_185_2 gives: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (240) aNaturalNumber0(all_110_5) = all_185_0 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_89_0) = all_185_2 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_68_0) = all_185_1 & ( ~ % 15.84/3.04 | | | | | | | | | | | | | | | | | | (all_185_1 = 0) | ~ (all_185_2 = 0) | all_185_0 % 15.84/3.04 | | | | | | | | | | | | | | | | | | = 0) % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | ALPHA: (240) implies: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (241) aNaturalNumber0(all_68_0) = all_185_1 % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | DELTA: instantiating (227) with fresh symbols all_187_0, % 15.84/3.04 | | | | | | | | | | | | | | | | | | all_187_1, all_187_2 gives: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (242) aNaturalNumber0(all_108_5) = all_187_0 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_89_0) = all_187_1 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_68_0) = all_187_2 & ( ~ % 15.84/3.04 | | | | | | | | | | | | | | | | | | (all_187_1 = 0) | ~ (all_187_2 = 0) | all_187_0 % 15.84/3.04 | | | | | | | | | | | | | | | | | | = 0) % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | ALPHA: (242) implies: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (243) aNaturalNumber0(all_68_0) = all_187_2 % 15.84/3.04 | | | | | | | | | | | | | | | | | | (244) aNaturalNumber0(all_89_0) = all_187_1 % 15.84/3.04 | | | | | | | | | | | | | | | | | | (245) aNaturalNumber0(all_108_5) = all_187_0 % 15.84/3.04 | | | | | | | | | | | | | | | | | | (246) ~ (all_187_1 = 0) | ~ (all_187_2 = 0) | % 15.84/3.04 | | | | | | | | | | | | | | | | | | all_187_0 = 0 % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | DELTA: instantiating (234) with fresh symbols all_189_0, % 15.84/3.04 | | | | | | | | | | | | | | | | | | all_189_1, all_189_2 gives: % 15.84/3.04 | | | | | | | | | | | | | | | | | | (247) aNaturalNumber0(all_108_5) = all_189_2 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_32_1) = all_189_0 & % 15.84/3.04 | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = all_189_1 & ( ~ (all_189_1 = % 15.84/3.04 | | | | | | | | | | | | | | | | | | 0) | ~ (all_189_2 = 0) | all_189_0 = 0) % 15.84/3.04 | | | | | | | | | | | | | | | | | | % 15.84/3.04 | | | | | | | | | | | | | | | | | | ALPHA: (247) implies: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (248) aNaturalNumber0(all_108_5) = all_189_2 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | DELTA: instantiating (233) with fresh symbols all_195_0, % 15.84/3.05 | | | | | | | | | | | | | | | | | | all_195_1, all_195_2 gives: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (249) sdtasdt0(xl, all_108_5) = all_195_0 & % 15.84/3.05 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_108_5) = all_195_2 & % 15.84/3.05 | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = all_195_1 & $i(all_195_0) & % 15.84/3.05 | | | | | | | | | | | | | | | | | | ( ~ (all_195_1 = 0) | ~ (all_195_2 = 0) | % 15.84/3.05 | | | | | | | | | | | | | | | | | | all_195_0 = all_32_1) % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | ALPHA: (249) implies: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (250) aNaturalNumber0(all_108_5) = all_195_2 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | DELTA: instantiating (228) with fresh symbols all_199_0, % 15.84/3.05 | | | | | | | | | | | | | | | | | | all_199_1, all_199_2 gives: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (251) sdtpldt0(all_68_0, all_89_0) = all_199_0 & % 15.84/3.05 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_89_0) = all_199_2 & % 15.84/3.05 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_68_0) = all_199_1 & % 15.84/3.05 | | | | | | | | | | | | | | | | | | $i(all_199_0) & ( ~ (all_199_1 = 0) | ~ % 15.84/3.05 | | | | | | | | | | | | | | | | | | (all_199_2 = 0) | all_199_0 = all_110_5) % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | ALPHA: (251) implies: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (252) aNaturalNumber0(all_68_0) = all_199_1 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | DELTA: instantiating (226) with fresh symbols all_201_0, % 15.84/3.05 | | | | | | | | | | | | | | | | | | all_201_1, all_201_2 gives: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (253) sdtpldt0(all_89_0, all_68_0) = all_201_0 & % 15.84/3.05 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_89_0) = all_201_1 & % 15.84/3.05 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_68_0) = all_201_2 & % 15.84/3.05 | | | | | | | | | | | | | | | | | | $i(all_201_0) & ( ~ (all_201_1 = 0) | ~ % 15.84/3.05 | | | | | | | | | | | | | | | | | | (all_201_2 = 0) | all_201_0 = all_108_5) % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | ALPHA: (253) implies: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (254) aNaturalNumber0(all_68_0) = all_201_2 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | DELTA: instantiating (231) with fresh symbols all_203_0, % 15.84/3.05 | | | | | | | | | | | | | | | | | | all_203_1, all_203_2 gives: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (255) sdtasdt0(all_108_5, xl) = all_203_0 & % 15.84/3.05 | | | | | | | | | | | | | | | | | | aNaturalNumber0(all_108_5) = all_203_1 & % 15.84/3.05 | | | | | | | | | | | | | | | | | | aNaturalNumber0(xl) = all_203_2 & $i(all_203_0) & % 15.84/3.05 | | | | | | | | | | | | | | | | | | ( ~ (all_203_1 = 0) | ~ (all_203_2 = 0) | % 15.84/3.05 | | | | | | | | | | | | | | | | | | all_203_0 = all_32_1) % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | ALPHA: (255) implies: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (256) aNaturalNumber0(all_108_5) = all_203_1 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (10) with all_187_2, all_199_1, % 15.84/3.05 | | | | | | | | | | | | | | | | | | all_68_0, simplifying with (243), (252) gives: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (257) all_199_1 = all_187_2 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (10) with all_185_1, all_199_1, % 15.84/3.05 | | | | | | | | | | | | | | | | | | all_68_0, simplifying with (241), (252) gives: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (258) all_199_1 = all_185_1 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (10) with 0, all_201_2, all_68_0, % 15.84/3.05 | | | | | | | | | | | | | | | | | | simplifying with (87), (254) gives: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (259) all_201_2 = 0 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (10) with all_199_1, all_201_2, % 15.84/3.05 | | | | | | | | | | | | | | | | | | all_68_0, simplifying with (252), (254) gives: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (260) all_201_2 = all_199_1 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (10) with 0, all_187_1, all_89_0, % 15.84/3.05 | | | | | | | | | | | | | | | | | | simplifying with (127), (244) gives: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (261) all_187_1 = 0 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (10) with all_187_0, all_189_2, % 15.84/3.05 | | | | | | | | | | | | | | | | | | all_108_5, simplifying with (245), (248) gives: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (262) all_189_2 = all_187_0 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (10) with all_189_2, all_195_2, % 15.84/3.05 | | | | | | | | | | | | | | | | | | all_108_5, simplifying with (248), (250) gives: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (263) all_195_2 = all_189_2 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (10) with all_179_0, all_195_2, % 15.84/3.05 | | | | | | | | | | | | | | | | | | all_108_5, simplifying with (237), (250) gives: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (264) all_195_2 = all_179_0 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (10) with all_187_0, all_203_1, % 15.84/3.05 | | | | | | | | | | | | | | | | | | all_108_5, simplifying with (245), (256) gives: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (265) all_203_1 = all_187_0 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (10) with all_183_1, all_203_1, % 15.84/3.05 | | | | | | | | | | | | | | | | | | all_108_5, simplifying with (239), (256) gives: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (266) all_203_1 = all_183_1 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | COMBINE_EQS: (265), (266) imply: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (267) all_187_0 = all_183_1 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | SIMP: (267) implies: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (268) all_187_0 = all_183_1 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | COMBINE_EQS: (259), (260) imply: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (269) all_199_1 = 0 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | SIMP: (269) implies: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (270) all_199_1 = 0 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | COMBINE_EQS: (257), (258) imply: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (271) all_187_2 = all_185_1 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | COMBINE_EQS: (257), (270) imply: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (272) all_187_2 = 0 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | COMBINE_EQS: (263), (264) imply: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (273) all_189_2 = all_179_0 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | SIMP: (273) implies: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (274) all_189_2 = all_179_0 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | COMBINE_EQS: (262), (274) imply: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (275) all_187_0 = all_179_0 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | SIMP: (275) implies: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (276) all_187_0 = all_179_0 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | COMBINE_EQS: (268), (276) imply: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (277) all_183_1 = all_179_0 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | COMBINE_EQS: (271), (272) imply: % 15.84/3.05 | | | | | | | | | | | | | | | | | | (278) all_185_1 = 0 % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | BETA: splitting (246) gives: % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | Case 1: % 15.84/3.05 | | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | | (279) ~ (all_187_1 = 0) % 15.84/3.05 | | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | | REDUCE: (261), (279) imply: % 15.84/3.05 | | | | | | | | | | | | | | | | | | | (280) $false % 15.84/3.05 | | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | | CLOSE: (280) is inconsistent. % 15.84/3.05 | | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | Case 2: % 15.84/3.05 | | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | | (281) ~ (all_187_2 = 0) | all_187_0 = 0 % 15.84/3.05 | | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | | BETA: splitting (281) gives: % 15.84/3.05 | | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | | Case 1: % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | (282) ~ (all_187_2 = 0) % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | REDUCE: (272), (282) imply: % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | (283) $false % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | CLOSE: (283) is inconsistent. % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | | Case 2: % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | (284) all_187_0 = 0 % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (276), (284) imply: % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | (285) all_179_0 = 0 % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | SIMP: (285) implies: % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | (286) all_179_0 = 0 % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | REDUCE: (236), (286) imply: % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | (287) $false % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | CLOSE: (287) is inconsistent. % 15.84/3.05 | | | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | | End of split % 15.84/3.05 | | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | | End of split % 15.84/3.05 | | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | | End of split % 15.84/3.05 | | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | | End of split % 15.84/3.05 | | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | | End of split % 15.84/3.05 | | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | | End of split % 15.84/3.05 | | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | | End of split % 15.84/3.05 | | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | | End of split % 15.84/3.05 | | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | | End of split % 15.84/3.05 | | | | | | | | | | | % 15.84/3.05 | | | | | | | | | | End of split % 15.84/3.05 | | | | | | | | | | % 15.84/3.05 | | | | | | | | | End of split % 15.84/3.05 | | | | | | | | | % 15.84/3.05 | | | | | | | | End of split % 15.84/3.05 | | | | | | | | % 15.84/3.05 | | | | | | | End of split % 15.84/3.05 | | | | | | | % 15.84/3.05 | | | | | | End of split % 15.84/3.05 | | | | | | % 15.84/3.05 | | | | | End of split % 15.84/3.05 | | | | | % 15.84/3.05 | | | | End of split % 15.84/3.05 | | | | % 15.84/3.05 | | | End of split % 15.84/3.05 | | | % 15.84/3.05 | | End of split % 15.84/3.05 | | % 15.84/3.05 | End of split % 15.84/3.05 | % 15.84/3.05 End of proof % 15.84/3.05 % SZS output end Proof for theBenchmark % 15.84/3.05 % 15.84/3.06 2452ms %------------------------------------------------------------------------------